-- File: bool2

-- defines not, and, and or as boolean functions

Path "../lol"
Load "bool"

---------
-- not --
---------

Def not := \b:Bool. if b false true

Prove not_true  : not true = false

Prove not_false : not false = true

Prove not_is_false_ : @b:Bool. not b = false -> b = true

Prove not_is_true_ : @b:Bool. not b = true -> b = false

Prove not_not : @b:Bool. not (not b) = b


---------
-- and --
---------

-- Name in lemmas: and
Def (&&) := \a,b:Bool. if a b false : Bool->Bool->Bool

Prove true_and : @b:Bool. true && b = b

Prove false_and : @b:Bool. false && b = false

Prove and_true : @b:Bool. b && true = b

Prove and_false : @b:Bool. b && false = false

Prove and_comm : @b,c:Bool. b && c = c && b

Prove and_assoc : @b,c,d:Bool. (b&&c)&&d = b&&(c&&d)

Prove and_is_false_ : @b,c:Bool. b&&c = false -> b=false \/ c=false

Prove and_is_true_ : @b,c:Bool. b&&c = true -> b=true /\ c=true

--------
-- or --
--------

-- Name in lemmas: or
Def (||) := \a,b:Bool. if a true b : Bool->Bool->Bool

Prove true_or : @b:Bool. true || b = true

Prove false_or : @b:Bool. false || b = b

Prove or_true : @b:Bool. b || true = true

Prove or_false : @b:Bool. b || false = b

Prove or_comm : @b,c:Bool. b || c = c || b

Prove or_assoc : @b,c,d:Bool. (b||c)||d = b||(c||d)

Prove or_idemp : @b:Bool. b||b = b


Prove or_is_true_ : @b,c:Bool. b || c = true -> b=true \/ c=true

Prove or_is_false_ : @b,c:Bool. b || c = false -> b=false /\ c=false

Prove not_or : @b,c:Bool. not (b||c) = not b && not c

Prove not_and : @b,c:Bool. not (b&&c) = not b || not c