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

## 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)
```

Lego
1998-06-15