2013-09-04 12:39:35 +00:00
|
|
|
|
Theorem and_comm (a b : Bool) : (a ∧ b) ⇒ (b ∧ a) :=
|
|
|
|
|
|
Discharge (λ H_ab, Conj (Conjunct2 H_ab) (Conjunct1 H_ab))
|
|
|
|
|
|
|
|
|
|
|
|
Theorem or_comm (a b : Bool) : (a ∨ b) ⇒ (b ∨ a) :=
|
|
|
|
|
|
Discharge (λ H_ab, DisjCases H_ab
|
|
|
|
|
|
(λ H_a, Disj2 b H_a)
|
2013-12-29 10:44:49 +00:00
|
|
|
|
(λ H_b, Disj1 H_b a))
|
2013-09-04 12:39:35 +00:00
|
|
|
|
|
|
|
|
|
|
(* ---------------------------------
|
|
|
|
|
|
(EM a) is the excluded middle a ∨ ¬a
|
|
|
|
|
|
(MT H H_na) is Modus Tollens with
|
|
|
|
|
|
H : (a ⇒ b) ⇒ a)
|
|
|
|
|
|
H_na : ¬a
|
|
|
|
|
|
produces
|
|
|
|
|
|
¬(a ⇒ b)
|
|
|
|
|
|
|
|
|
|
|
|
NotImp1 applied to
|
|
|
|
|
|
(MT H H_na) : ¬(a ⇒ b)
|
|
|
|
|
|
produces
|
|
|
|
|
|
a
|
|
|
|
|
|
----------------------------------- *)
|
|
|
|
|
|
Theorem pierce (a b : Bool) : ((a ⇒ b) ⇒ a) ⇒ a :=
|
|
|
|
|
|
Discharge (λ H, DisjCases (EM a)
|
|
|
|
|
|
(λ H_a, H_a)
|
|
|
|
|
|
(λ H_na, NotImp1 (MT H H_na)))
|
|
|
|
|
|
|
|
|
|
|
|
Show Environment 3
|
