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|SET}{x:t}Eq (if b x x) x if_character = ... : {t|SET}{x,y,z|t}{b|bool}(Eq (if b x y) z)->or (Eq x z) (Eq y z) Eq_resp_if = ... : {t|SET}{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,t|SET}{f:s->t}{x,y:s}{b:bool}Eq (if b (f x) (f y)) (f (if b x y)) middle_four_if = ... : {A|SET}{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|SET}{a,b,c:A}{x:bool}Eq (if x (if x a b) c) (if x a c) reduce_if_right = ... : {A|SET}{a,b,c:A}{x:bool}Eq (if x a (if x b c)) (if x a c) if_prop = ... : {C|SET}{b:bool}((Eq b true)->C)->((Eq b false)->C)->C andalso_character = ... : {a,b:bool}iff (is_true (andalso a b)) (and (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)) (or (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)) (and (is_false a) (is_false b)) deMorgan' = ... : {a,b:bool} iff (is_false (andalso a b)) (or (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)