Up to index of Isabelle/HOL/ex
theory Higher_Order_Logic(* Title: HOL/ex/Higher_Order_Logic.thy ID: $Id: Higher_Order_Logic.thy,v 1.6 2005/06/17 14:12:49 haftmann Exp $ Author: Gertrud Bauer and Markus Wenzel, TU Muenchen *) header {* Foundations of HOL *} theory Higher_Order_Logic imports CPure begin text {* The following theory development demonstrates Higher-Order Logic itself, represented directly within the Pure framework of Isabelle. The ``HOL'' logic given here is essentially that of Gordon \cite{Gordon:1985:HOL}, although we prefer to present basic concepts in a slightly more conventional manner oriented towards plain Natural Deduction. *} subsection {* Pure Logic *} classes type defaultsort type typedecl o arities o :: type fun :: (type, type) type subsubsection {* Basic logical connectives *} judgment Trueprop :: "o => prop" ("_" 5) consts imp :: "o => o => o" (infixr "-->" 25) All :: "('a => o) => o" (binder "∀" 10) axioms impI [intro]: "(A ==> B) ==> A --> B" impE [dest, trans]: "A --> B ==> A ==> B" allI [intro]: "(!!x. P x) ==> ∀x. P x" allE [dest]: "∀x. P x ==> P a" subsubsection {* Extensional equality *} consts equal :: "'a => 'a => o" (infixl "=" 50) axioms refl [intro]: "x = x" subst: "x = y ==> P x ==> P y" ext [intro]: "(!!x. f x = g x) ==> f = g" iff [intro]: "(A ==> B) ==> (B ==> A) ==> A = B" theorem sym [sym]: "x = y ==> y = x" proof - assume "x = y" thus "y = x" by (rule subst) (rule refl) qed lemma [trans]: "x = y ==> P y ==> P x" by (rule subst) (rule sym) lemma [trans]: "P x ==> x = y ==> P y" by (rule subst) theorem trans [trans]: "x = y ==> y = z ==> x = z" by (rule subst) theorem iff1 [elim]: "A = B ==> A ==> B" by (rule subst) theorem iff2 [elim]: "A = B ==> B ==> A" by (rule subst) (rule sym) subsubsection {* Derived connectives *} constdefs false :: o ("⊥") "⊥ ≡ ∀A. A" true :: o ("\<top>") "\<top> ≡ ⊥ --> ⊥" not :: "o => o" ("¬ _" [40] 40) "not ≡ λA. A --> ⊥" conj :: "o => o => o" (infixr "∧" 35) "conj ≡ λA B. ∀C. (A --> B --> C) --> C" disj :: "o => o => o" (infixr "∨" 30) "disj ≡ λA B. ∀C. (A --> C) --> (B --> C) --> C" Ex :: "('a => o) => o" (binder "∃" 10) "Ex ≡ λP. ∀C. (∀x. P x --> C) --> C" syntax "_not_equal" :: "'a => 'a => o" (infixl "≠" 50) translations "x ≠ y" \<rightleftharpoons> "¬ (x = y)" theorem falseE [elim]: "⊥ ==> A" proof (unfold false_def) assume "∀A. A" thus A .. qed theorem trueI [intro]: \<top> proof (unfold true_def) show "⊥ --> ⊥" .. qed theorem notI [intro]: "(A ==> ⊥) ==> ¬ A" proof (unfold not_def) assume "A ==> ⊥" thus "A --> ⊥" .. qed theorem notE [elim]: "¬ A ==> A ==> B" proof (unfold not_def) assume "A --> ⊥" also assume A finally have ⊥ .. thus B .. qed lemma notE': "A ==> ¬ A ==> B" by (rule notE) lemmas contradiction = notE notE' -- {* proof by contradiction in any order *} theorem conjI [intro]: "A ==> B ==> A ∧ B" proof (unfold conj_def) assume A and B show "∀C. (A --> B --> C) --> C" proof fix C show "(A --> B --> C) --> C" proof assume "A --> B --> C" also have A . also have B . finally show C . qed qed qed theorem conjE [elim]: "A ∧ B ==> (A ==> B ==> C) ==> C" proof (unfold conj_def) assume c: "∀C. (A --> B --> C) --> C" assume "A ==> B ==> C" moreover { from c have "(A --> B --> A) --> A" .. also have "A --> B --> A" proof assume A thus "B --> A" .. qed finally have A . } moreover { from c have "(A --> B --> B) --> B" .. also have "A --> B --> B" proof show "B --> B" .. qed finally have B . } ultimately show C . qed theorem disjI1 [intro]: "A ==> A ∨ B" proof (unfold disj_def) assume A show "∀C. (A --> C) --> (B --> C) --> C" proof fix C show "(A --> C) --> (B --> C) --> C" proof assume "A --> C" also have A . finally have C . thus "(B --> C) --> C" .. qed qed qed theorem disjI2 [intro]: "B ==> A ∨ B" proof (unfold disj_def) assume B show "∀C. (A --> C) --> (B --> C) --> C" proof fix C show "(A --> C) --> (B --> C) --> C" proof show "(B --> C) --> C" proof assume "B --> C" also have B . finally show C . qed qed qed qed theorem disjE [elim]: "A ∨ B ==> (A ==> C) ==> (B ==> C) ==> C" proof (unfold disj_def) assume c: "∀C. (A --> C) --> (B --> C) --> C" assume r1: "A ==> C" and r2: "B ==> C" from c have "(A --> C) --> (B --> C) --> C" .. also have "A --> C" proof assume A thus C by (rule r1) qed also have "B --> C" proof assume B thus C by (rule r2) qed finally show C . qed theorem exI [intro]: "P a ==> ∃x. P x" proof (unfold Ex_def) assume "P a" show "∀C. (∀x. P x --> C) --> C" proof fix C show "(∀x. P x --> C) --> C" proof assume "∀x. P x --> C" hence "P a --> C" .. also have "P a" . finally show C . qed qed qed theorem exE [elim]: "∃x. P x ==> (!!x. P x ==> C) ==> C" proof (unfold Ex_def) assume c: "∀C. (∀x. P x --> C) --> C" assume r: "!!x. P x ==> C" from c have "(∀x. P x --> C) --> C" .. also have "∀x. P x --> C" proof fix x show "P x --> C" proof assume "P x" thus C by (rule r) qed qed finally show C . qed subsection {* Classical logic *} locale classical = assumes classical: "(¬ A ==> A) ==> A" theorem (in classical) Peirce's_Law: "((A --> B) --> A) --> A" proof assume a: "(A --> B) --> A" show A proof (rule classical) assume "¬ A" have "A --> B" proof assume A thus B by (rule contradiction) qed with a show A .. qed qed theorem (in classical) double_negation: "¬ ¬ A ==> A" proof - assume "¬ ¬ A" show A proof (rule classical) assume "¬ A" thus ?thesis by (rule contradiction) qed qed theorem (in classical) tertium_non_datur: "A ∨ ¬ A" proof (rule double_negation) show "¬ ¬ (A ∨ ¬ A)" proof assume "¬ (A ∨ ¬ A)" have "¬ A" proof assume A hence "A ∨ ¬ A" .. thus ⊥ by (rule contradiction) qed hence "A ∨ ¬ A" .. thus ⊥ by (rule contradiction) qed qed theorem (in classical) classical_cases: "(A ==> C) ==> (¬ A ==> C) ==> C" proof - assume r1: "A ==> C" and r2: "¬ A ==> C" from tertium_non_datur show C proof assume A thus ?thesis by (rule r1) next assume "¬ A" thus ?thesis by (rule r2) qed qed lemma (in classical) "(¬ A ==> A) ==> A" (* FIXME *) proof - assume r: "¬ A ==> A" show A proof (rule classical_cases) assume A thus A . next assume "¬ A" thus A by (rule r) qed qed end
theorem sym:
x = y ==> y = x
lemma
[| x = y; P y |] ==> P x
lemma
[| P x; x = y |] ==> P y
theorem trans:
[| x = y; y = z |] ==> x = z
theorem iff1:
[| A = B; A |] ==> B
theorem iff2:
[| A = B; B |] ==> A
theorem falseE:
⊥ ==> A
theorem trueI:
\<top>
theorem notI:
(A ==> ⊥) ==> ¬ A
theorem notE:
[| ¬ A; A |] ==> B
lemma notE':
[| A; ¬ A |] ==> B
lemmas contradiction:
[| ¬ A; A |] ==> B
[| A; ¬ A |] ==> B
lemmas contradiction:
[| ¬ A; A |] ==> B
[| A; ¬ A |] ==> B
theorem conjI:
[| A; B |] ==> A ∧ B
theorem conjE:
[| A ∧ B; [| A; B |] ==> C |] ==> C
theorem disjI1:
A ==> A ∨ B
theorem disjI2:
B ==> A ∨ B
theorem disjE:
[| A ∨ B; A ==> C; B ==> C |] ==> C
theorem exI:
P a ==> ∃x. P x
theorem exE:
[| ∃x. P x; !!x. P x ==> C |] ==> C
theorem Peirce's_Law:
PROP classical ==> ((A --> B) --> A) --> A
theorem double_negation:
[| PROP classical; ¬ ¬ A |] ==> A
theorem tertium_non_datur:
PROP classical ==> A ∨ ¬ A
theorem classical_cases:
[| PROP classical; A ==> C; ¬ A ==> C |] ==> C
lemma
[| PROP classical; ¬ A ==> A |] ==> A