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
[[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]

  bool_is_true = ... : bool->Type
  bool_is_false = ... : bool->Type
  bool_true_injective = ... : (Eq true true)->{P|Type}P->P
  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)