imports Pure

(* Title: HOL/ex/Higher_Order_Logic.thy Author: Gertrud Bauer and Markus Wenzel, TU Muenchen *) header {* Foundations of HOL *} theory Higher_Order_Logic imports Pure 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 *} class type default_sort type typedecl o instance o :: type .. instance "fun" :: (type, type) type .. subsubsection {* Basic logical connectives *} judgment Trueprop :: "o => prop" ("_" 5) axiomatization imp :: "o => o => o" (infixr "-->" 25) and All :: "('a => o) => o" (binder "∀" 10) where impI [intro]: "(A ==> B) ==> A --> B" and impE [dest, trans]: "A --> B ==> A ==> B" and allI [intro]: "(!!x. P x) ==> ∀x. P x" and allE [dest]: "∀x. P x ==> P a" subsubsection {* Extensional equality *} axiomatization equal :: "'a => 'a => o" (infixl "=" 50) where refl [intro]: "x = x" and subst: "x = y ==> P x ==> P y" axiomatization where ext [intro]: "(!!x. f x = g x) ==> f = g" and iff [intro]: "(A ==> B) ==> (B ==> A) ==> A = B" theorem sym [sym]: "x = y ==> y = x" proof - assume "x = y" then show "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 *} definition false :: o ("⊥") where "⊥ ≡ ∀A. A" definition true :: o ("\<top>") where "\<top> ≡ ⊥ --> ⊥" definition not :: "o => o" ("¬ _" [40] 40) where "not ≡ λA. A --> ⊥" definition conj :: "o => o => o" (infixr "∧" 35) where "conj ≡ λA B. ∀C. (A --> B --> C) --> C" definition disj :: "o => o => o" (infixr "∨" 30) where "disj ≡ λA B. ∀C. (A --> C) --> (B --> C) --> C" definition Ex :: "('a => o) => o" (binder "∃" 10) where "∃x. P x ≡ ∀C. (∀x. P x --> C) --> C" abbreviation not_equal :: "'a => 'a => o" (infixl "≠" 50) where "x ≠ y ≡ ¬ (x = y)" theorem falseE [elim]: "⊥ ==> A" proof (unfold false_def) assume "∀A. A" then show A .. qed theorem trueI [intro]: \<top> proof (unfold true_def) show "⊥ --> ⊥" .. qed theorem notI [intro]: "(A ==> ⊥) ==> ¬ A" proof (unfold not_def) assume "A ==> ⊥" then show "A --> ⊥" .. qed theorem notE [elim]: "¬ A ==> A ==> B" proof (unfold not_def) assume "A --> ⊥" also assume A finally have ⊥ .. then show 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 note `A` also note `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 then show "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 note `A` finally have C . then show "(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 note `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 then show C by (rule r1) qed also have "B --> C" proof assume B then show 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" then have "P a --> C" .. also note `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" then show 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 with `¬ A` show 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" with `¬ ¬ A` show ?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 then have "A ∨ ¬ A" .. with `¬ (A ∨ ¬ A)` show ⊥ by (rule contradiction) qed then have "A ∨ ¬ A" .. with `¬ (A ∨ ¬ A)` show ⊥ 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 then show ?thesis by (rule r1) next assume "¬ A" then show ?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 then show A . next assume "¬ A" then show A by (rule r) qed qed end