Next: Boolean Functions Up: The Booleans Previous: The Booleans

## Boolean Definition

The file lib_bool gives the basic definition of the boolean type with its recursor and induction principle and propositional functions is_true and is_false which are used in the two characterisation theorems that true is not equal to false and that any boolean is either true or false.

``` ** Module lib_bool Imports lib_eq_basics
\$bool : Type(bool)
\$true : bool
\$false : bool
\$bool_elim :
{C_bool:bool->TYPE}(C_bool true)->(C_bool false)->{z:bool}C_bool z
** Label (!bool!) bool
** Label (!bool elim!) bool_elim
** Label (!bool true!) true
** Label (!bool false!) false
[[C_bool:bool->TYPE][f_true:C_bool true][f_false:C_bool false]
bool_elim C_bool f_true f_false true  ==>  f_true
|| bool_elim C_bool f_true f_false false  ==>  f_false]

Gen (!bool is true!) as bool_is_true = ... : bool->Type
Gen (!bool is false!) as bool_is_false = ... : bool->Type
Gen (!bool true injective!) as bool_true_injective = ... :
(Eq true true)->{P|Type}P->P
Gen (!bool false injective!) as bool_false_injective = ... :
(Eq false false)->{P|Type}P->P
bool_rec = ... : {T|Type}T->T->bool->T
bool_ind = ... : {P:bool->Prop}(P true)->(P false)->{b:bool}P b
bool_double_elim = ... :
{T:bool->bool->Type}(T true true)->(T true false)->(T false true)->
(T false false)->{x,y:bool}T x y
is_true = ... : bool->Prop
is_false = ... : bool->Prop
true_not_false = ... : not (Eq true false)
true_or_false = ... : {b:bool}(is_true b \/ is_false b)
```

Conor McBride
11/13/1998