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