imports Pure

(* Title: HOL/Isar_Examples/Higher_Order_Logic.thy Author: Makarius *) section ‹Foundations of HOL› theory Higher_Order_Logic imports Pure begin text ‹ The following theory development illustrates the foundations of Higher-Order Logic. The ``HOL'' logic that is given here resembles @{cite "Gordon:1985:HOL"} and its predecessor @{cite "church40"}, but the order of axiomatizations and defined connectives has be adapted to modern presentations of ‹λ›-calculus and Constructive Type Theory. Thus it fits nicely to the underlying Natural Deduction framework of Isabelle/Pure and Isabelle/Isar. › section ‹HOL syntax within Pure› class type default_sort type typedecl o instance o :: type .. instance "fun" :: (type, type) type .. judgment Trueprop :: "o ⇒ prop" ("_" 5) section ‹Minimal logic (axiomatization)› axiomatization imp :: "o ⇒ o ⇒ o" (infixr "⟶" 25) where impI [intro]: "(A ⟹ B) ⟹ A ⟶ B" and impE [dest, trans]: "A ⟶ B ⟹ A ⟹ B" axiomatization All :: "('a ⇒ o) ⇒ o" (binder "∀" 10) where allI [intro]: "(⋀x. P x) ⟹ ∀x. P x" and allE [dest]: "∀x. P x ⟹ P a" lemma atomize_imp [atomize]: "(A ⟹ B) ≡ Trueprop (A ⟶ B)" by standard (fact impI, fact impE) lemma atomize_all [atomize]: "(⋀x. P x) ≡ Trueprop (∀x. P x)" by standard (fact allI, fact allE) subsubsection ‹Derived connectives› definition False :: o where "False ≡ ∀A. A" lemma FalseE [elim]: assumes "False" shows A proof - from ‹False› have "∀A. A" by (simp only: False_def) then show A .. qed definition True :: o where "True ≡ False ⟶ False" lemma TrueI [intro]: True unfolding True_def .. definition not :: "o ⇒ o" ("¬ _" [40] 40) where "not ≡ λA. A ⟶ False" lemma notI [intro]: assumes "A ⟹ False" shows "¬ A" using assms unfolding not_def .. lemma notE [elim]: assumes "¬ A" and A shows B proof - from ‹¬ A› have "A ⟶ False" by (simp only: not_def) from this and ‹A› have "False" .. then show B .. qed lemma notE': "A ⟹ ¬ A ⟹ B" by (rule notE) lemmas contradiction = notE notE' ― ‹proof by contradiction in any order› definition conj :: "o ⇒ o ⇒ o" (infixr "∧" 35) where "A ∧ B ≡ ∀C. (A ⟶ B ⟶ C) ⟶ C" lemma conjI [intro]: assumes A and B shows "A ∧ B" unfolding conj_def proof fix C show "(A ⟶ B ⟶ C) ⟶ C" proof assume "A ⟶ B ⟶ C" also note ‹A› also note ‹B› finally show C . qed qed lemma conjE [elim]: assumes "A ∧ B" obtains A and B proof from ‹A ∧ B› have *: "(A ⟶ B ⟶ C) ⟶ C" for C unfolding conj_def .. show A proof - note * [of A] also have "A ⟶ B ⟶ A" proof assume A then show "B ⟶ A" .. qed finally show ?thesis . qed show B proof - note * [of B] also have "A ⟶ B ⟶ B" proof show "B ⟶ B" .. qed finally show ?thesis . qed qed definition disj :: "o ⇒ o ⇒ o" (infixr "∨" 30) where "A ∨ B ≡ ∀C. (A ⟶ C) ⟶ (B ⟶ C) ⟶ C" lemma disjI1 [intro]: assumes A shows "A ∨ B" unfolding disj_def proof fix C show "(A ⟶ C) ⟶ (B ⟶ C) ⟶ C" proof assume "A ⟶ C" from this and ‹A› have C .. then show "(B ⟶ C) ⟶ C" .. qed qed lemma disjI2 [intro]: assumes B shows "A ∨ B" unfolding disj_def proof fix C show "(A ⟶ C) ⟶ (B ⟶ C) ⟶ C" proof show "(B ⟶ C) ⟶ C" proof assume "B ⟶ C" from this and ‹B› show C .. qed qed qed lemma disjE [elim]: assumes "A ∨ B" obtains (a) A | (b) B proof - from ‹A ∨ B› have "(A ⟶ thesis) ⟶ (B ⟶ thesis) ⟶ thesis" unfolding disj_def .. also have "A ⟶ thesis" proof assume A then show thesis by (rule a) qed also have "B ⟶ thesis" proof assume B then show thesis by (rule b) qed finally show thesis . qed definition Ex :: "('a ⇒ o) ⇒ o" (binder "∃" 10) where "∃x. P x ≡ ∀C. (∀x. P x ⟶ C) ⟶ C" lemma exI [intro]: "P a ⟹ ∃x. P x" unfolding Ex_def proof fix C assume "P a" show "(∀x. P x ⟶ C) ⟶ C" proof assume "∀x. P x ⟶ C" then have "P a ⟶ C" .. from this and ‹P a› show C .. qed qed lemma exE [elim]: assumes "∃x. P x" obtains (that) x where "P x" proof - from ‹∃x. P x› have "(∀x. P x ⟶ thesis) ⟶ thesis" unfolding Ex_def .. also have "∀x. P x ⟶ thesis" proof fix x show "P x ⟶ thesis" proof assume "P x" then show thesis by (rule that) qed qed finally show thesis . qed subsubsection ‹Extensional equality› axiomatization equal :: "'a ⇒ 'a ⇒ o" (infixl "=" 50) where refl [intro]: "x = x" and subst: "x = y ⟹ P x ⟹ P y" abbreviation not_equal :: "'a ⇒ 'a ⇒ o" (infixl "≠" 50) where "x ≠ y ≡ ¬ (x = y)" abbreviation iff :: "o ⇒ o ⇒ o" (infixr "⟷" 25) where "A ⟷ B ≡ A = B" axiomatization where ext [intro]: "(⋀x. f x = g x) ⟹ f = g" and iff [intro]: "(A ⟹ B) ⟹ (B ⟹ A) ⟹ A ⟷ B" lemma sym [sym]: "y = x" if "x = y" using that by (rule subst) (rule refl) lemma [trans]: "x = y ⟹ P y ⟹ P x" by (rule subst) (rule sym) lemma [trans]: "P x ⟹ x = y ⟹ P y" by (rule subst) lemma arg_cong: "f x = f y" if "x = y" using that by (rule subst) (rule refl) lemma fun_cong: "f x = g x" if "f = g" using that by (rule subst) (rule refl) lemma trans [trans]: "x = y ⟹ y = z ⟹ x = z" by (rule subst) lemma iff1 [elim]: "A ⟷ B ⟹ A ⟹ B" by (rule subst) lemma iff2 [elim]: "A ⟷ B ⟹ B ⟹ A" by (rule subst) (rule sym) subsection ‹Cantor's Theorem› text ‹ Cantor's Theorem states that there is no surjection from a set to its powerset. The subsequent formulation uses elementary ‹λ›-calculus and predicate logic, with standard introduction and elimination rules. › lemma iff_contradiction: assumes *: "¬ A ⟷ A" shows C proof (rule notE) show "¬ A" proof assume A with * have "¬ A" .. from this and ‹A› show False .. qed with * show A .. qed theorem Cantor: "¬ (∃f :: 'a ⇒ 'a ⇒ o. ∀A. ∃x. A = f x)" proof assume "∃f :: 'a ⇒ 'a ⇒ o. ∀A. ∃x. A = f x" then obtain f :: "'a ⇒ 'a ⇒ o" where *: "∀A. ∃x. A = f x" .. let ?D = "λx. ¬ f x x" from * have "∃x. ?D = f x" .. then obtain a where "?D = f a" .. then have "?D a ⟷ f a a" using refl by (rule subst) then have "¬ f a a ⟷ f a a" . then show False by (rule iff_contradiction) qed subsection ‹Characterization of Classical Logic› text ‹ The subsequent rules of classical reasoning are all equivalent. › locale classical = assumes classical: "(¬ A ⟹ A) ⟹ A" ― ‹predicate definition and hypothetical context› begin lemma classical_contradiction: assumes "¬ A ⟹ False" shows A proof (rule classical) assume "¬ A" then have False by (rule assms) then show A .. qed lemma double_negation: assumes "¬ ¬ A" shows A proof (rule classical_contradiction) assume "¬ A" with ‹¬ ¬ A› show False by (rule contradiction) qed lemma 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 False by (rule contradiction) qed then have "A ∨ ¬ A" .. with ‹¬ (A ∨ ¬ A)› show False by (rule contradiction) qed qed lemma classical_cases: obtains A | "¬ A" using tertium_non_datur proof assume A then show thesis .. next assume "¬ A" then show thesis .. qed end lemma classical_if_cases: classical if cases: "⋀A C. (A ⟹ C) ⟹ (¬ A ⟹ C) ⟹ C" proof fix A assume *: "¬ A ⟹ A" show A proof (rule cases) assume A then show A . next assume "¬ A" then show A by (rule *) qed qed section ‹Peirce's Law› text ‹ Peirce's Law is another characterization of classical reasoning. Its statement only requires implication. › theorem (in classical) Peirce's_Law: "((A ⟶ B) ⟶ A) ⟶ A" proof assume *: "(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 * show A .. qed qed section ‹Hilbert's choice operator (axiomatization)› axiomatization Eps :: "('a ⇒ o) ⇒ 'a" where someI: "P x ⟹ P (Eps P)" syntax "_Eps" :: "pttrn ⇒ o ⇒ 'a" ("(3SOME _./ _)" [0, 10] 10) translations "SOME x. P" ⇌ "CONST Eps (λx. P)" text ‹ ┉ It follows a derivation of the classical law of tertium-non-datur by means of Hilbert's choice operator (due to Berghofer, Beeson, Harrison, based on a proof by Diaconescu). ┉ › theorem Diaconescu: "A ∨ ¬ A" proof - let ?P = "λx. (A ∧ x) ∨ ¬ x" let ?Q = "λx. (A ∧ ¬ x) ∨ x" have a: "?P (Eps ?P)" proof (rule someI) have "¬ False" .. then show "?P False" .. qed have b: "?Q (Eps ?Q)" proof (rule someI) have True .. then show "?Q True" .. qed from a show ?thesis proof assume "A ∧ Eps ?P" then have A .. then show ?thesis .. next assume "¬ Eps ?P" from b show ?thesis proof assume "A ∧ ¬ Eps ?Q" then have A .. then show ?thesis .. next assume "Eps ?Q" have neq: "?P ≠ ?Q" proof assume "?P = ?Q" then have "Eps ?P ⟷ Eps ?Q" by (rule arg_cong) also note ‹Eps ?Q› finally have "Eps ?P" . with ‹¬ Eps ?P› show False by (rule contradiction) qed have "¬ A" proof assume A have "?P = ?Q" proof (rule ext) show "?P x ⟷ ?Q x" for x proof assume "?P x" then show "?Q x" proof assume "¬ x" with ‹A› have "A ∧ ¬ x" .. then show ?thesis .. next assume "A ∧ x" then have x .. then show ?thesis .. qed next assume "?Q x" then show "?P x" proof assume "A ∧ ¬ x" then have "¬ x" .. then show ?thesis .. next assume x with ‹A› have "A ∧ x" .. then show ?thesis .. qed qed qed with neq show False by (rule contradiction) qed then show ?thesis .. qed qed qed text ‹ This means, the hypothetical predicate \<^const>‹classical› always holds unconditionally (with all consequences). › interpretation classical proof (rule classical_if_cases) fix A C assume *: "A ⟹ C" and **: "¬ A ⟹ C" from Diaconescu [of A] show C proof assume A then show C by (rule *) next assume "¬ A" then show C by (rule **) qed qed thm classical classical_contradiction double_negation tertium_non_datur classical_cases Peirce's_Law end