Boolean Theorems

This file contains various theorems about the above boolean functions, mostly proving that they have the expected meanings.

 ** Module lib_bool_thms Imports lib_bool_funs
  is_true_not_is_false = ... :
    {b:bool}iff (is_true b) (not (is_false b))
  bool_contrapos = ... :
    {a,b|bool}((is_true a)->is_true b)->(is_false b)->is_false a
  bool_contradiction = ... : {b|bool}(is_true b)->(is_false b)->absurd
  if_absorbs = ... : {b:bool}{t|Type}{x:t}Eq (if b x x) x
  if_character = ... :
    {t|Type}{x,y,z|t}{b|bool}(Eq (if b x y) z)->(Eq x z \/ Eq y z)
  Eq_resp_if = ... :
    {t|Type}{x,y,x',y'|t}(Eq x x')->(Eq y y')->{b:bool}
    Eq (if b x y) (if b x' y')
  if_inside = ... :
    {s|Type}{t|Type}{f:s->t}{x,y:s}{b:bool}
    Eq (if b (f x) (f y)) (f (if b x y))
  middle_four_if = ... :
    {A|Type}{a,b,c,d:A}{x,y:bool}
    Eq (if x (if y a b) (if y c d)) (if y (if x a c) (if x b d))
  reduce_if_left = ... :
    {A|Type}{a,b,c:A}{x:bool}Eq (if x (if x a b) c) (if x a c)
  reduce_if_right = ... :
    {A|Type}{a,b,c:A}{x:bool}Eq (if x a (if x b c)) (if x a c)
  if_prop = ... : {C|Type}{b:bool}((Eq b true)->C)->((Eq b false)->C)->C
  andalso_character = ... :
    {a,b:bool}iff (is_true (andalso a b)) (is_true a /\ is_true b)
  andalso_absorbs = ... : {b:bool}Eq (andalso b b) b
  andalso_commutes = ... : {b,c:bool}Eq (andalso b c) (andalso c b)
  andalso_false = ... : {b:bool}Eq (andalso b false) false
  andalso_true = ... : {b:bool}Eq (andalso b true) b
  inv_character = ... : {b:bool}iff (is_true (inv b)) (not (is_true b))
  inv_character' = ... : {a,b:bool}iff (Eq (inv a) b) (Eq a (inv b))
  inv_idemp = ... : {b:bool}Eq (inv (inv b)) b
  inv_is_true_is_false = ... :
    {n:bool}iff (is_true (inv n)) (is_false n)
  inv_is_false_is_true = ... :
    {n:bool}iff (is_false (inv n)) (is_true n)
  orelse_character = ... :
    {a,b:bool}iff (is_true (orelse a b)) (is_true a \/ is_true b)
  orelse_absorbs = ... : {b:bool}Eq (orelse b b) b
  orelse_assoc = ... :
    {a,b,c:bool}Eq (orelse (orelse a b) c) (orelse a (orelse b c))
  orelse_commutes = ... : {a,b:bool}Eq (orelse a b) (orelse b a)
  orelse_false = ... : {b:bool}Eq (orelse b false) b
  orelse_true = ... : {b:bool}Eq (orelse b true) true
  deMorgan = ... :
    {a,b:bool}iff (is_false (orelse a b)) (is_false a /\ is_false b)
  deMorgan' = ... :
    {a,b:bool}iff (is_false (andalso a b)) (is_false a \/ is_false b)
  implies_character = ... :
    {a,b:bool}iff (is_true (implies a b)) ((is_true a)->is_true b)
  implies_false = ... : {n:bool}is_true (implies false n)