# HG changeset patch # User wenzelm # Date 1591621797 -7200 # Node ID e5df9c8d9d4b2a59e13210df2550e5ef4517a1aa # Parent 7b34a932eeb6aef1b354d1001135b495e0dccd52 clarified sessions: "Notable Examples in Isabelle/Pure"; diff -r 7b34a932eeb6 -r e5df9c8d9d4b NEWS --- a/NEWS Sat Jun 06 10:58:13 2020 +0200 +++ b/NEWS Mon Jun 08 15:09:57 2020 +0200 @@ -18,6 +18,9 @@ *** Pure *** +* Session Pure-Examples contains notable examples for Isabelle/Pure +(former entries of HOL-Isar_Examples). + * Definitions in locales produce rule which can be added as congruence rule to protect foundational terms during simplification. diff -r 7b34a932eeb6 -r e5df9c8d9d4b lib/html/library_index_content.template --- a/lib/html/library_index_content.template Sat Jun 06 10:58:13 2020 +0200 +++ b/lib/html/library_index_content.template Mon Jun 08 15:09:57 2020 +0200 @@ -46,7 +46,7 @@
  • Cube (The Lambda Cube)
    • -
  • The Pure logical framework
    • +
  • The Pure logical framework
  • Sources of Documentation
    • diff -r 7b34a932eeb6 -r e5df9c8d9d4b src/Doc/Isar_Ref/Framework.thy --- a/src/Doc/Isar_Ref/Framework.thy Sat Jun 06 10:58:13 2020 +0200 +++ b/src/Doc/Isar_Ref/Framework.thy Mon Jun 08 15:09:57 2020 +0200 @@ -93,7 +93,7 @@ \<^dir>\~~/src/HOL/Isar_Examples\. Some examples demonstrate how to start a fresh object-logic from Isabelle/Pure, and use Isar proofs from the very start, despite the lack of advanced proof tools at such an early stage (e.g.\ see - \<^file>\~~/src/HOL/Isar_Examples/Higher_Order_Logic.thy\). Isabelle/FOL @{cite + \<^file>\~~/src/Pure/Examples/Higher_Order_Logic.thy\). Isabelle/FOL @{cite "isabelle-logics"} and Isabelle/ZF @{cite "isabelle-ZF"} also work, but are much less developed. diff -r 7b34a932eeb6 -r e5df9c8d9d4b src/HOL/Isar_Examples/First_Order_Logic.thy --- a/src/HOL/Isar_Examples/First_Order_Logic.thy Sat Jun 06 10:58:13 2020 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,160 +0,0 @@ -(* Title: HOL/Isar_Examples/First_Order_Logic.thy - Author: Makarius -*) - -section \A simple formulation of First-Order Logic\ - -text \ - The subsequent theory development illustrates single-sorted intuitionistic - first-order logic with equality, formulated within the Pure framework. -\ - -theory First_Order_Logic - imports Pure -begin - -subsection \Abstract syntax\ - -typedecl i -typedecl o - -judgment Trueprop :: "o \ prop" ("_" 5) - - -subsection \Propositional logic\ - -axiomatization false :: o ("\") - where falseE [elim]: "\ \ A" - - -axiomatization imp :: "o \ o \ o" (infixr "\" 25) - where impI [intro]: "(A \ B) \ A \ B" - and mp [dest]: "A \ B \ A \ B" - - -axiomatization conj :: "o \ o \ o" (infixr "\" 35) - where conjI [intro]: "A \ B \ A \ B" - and conjD1: "A \ B \ A" - and conjD2: "A \ B \ B" - -theorem conjE [elim]: - assumes "A \ B" - obtains A and B -proof - from \A \ B\ show A - by (rule conjD1) - from \A \ B\ show B - by (rule conjD2) -qed - - -axiomatization disj :: "o \ o \ o" (infixr "\" 30) - where disjE [elim]: "A \ B \ (A \ C) \ (B \ C) \ C" - and disjI1 [intro]: "A \ A \ B" - and disjI2 [intro]: "B \ A \ B" - - -definition true :: o ("\") - where "\ \ \ \ \" - -theorem trueI [intro]: \ - unfolding true_def .. - - -definition not :: "o \ o" ("\ _" [40] 40) - where "\ A \ A \ \" - -theorem notI [intro]: "(A \ \) \ \ A" - unfolding not_def .. - -theorem notE [elim]: "\ A \ A \ B" - unfolding not_def -proof - - assume "A \ \" and A - then have \ .. - then show B .. -qed - - -definition iff :: "o \ o \ o" (infixr "\" 25) - where "A \ B \ (A \ B) \ (B \ A)" - -theorem iffI [intro]: - assumes "A \ B" - and "B \ A" - shows "A \ B" - unfolding iff_def -proof - from \A \ B\ show "A \ B" .. - from \B \ A\ show "B \ A" .. -qed - -theorem iff1 [elim]: - assumes "A \ B" and A - shows B -proof - - from \A \ B\ have "(A \ B) \ (B \ A)" - unfolding iff_def . - then have "A \ B" .. - from this and \A\ show B .. -qed - -theorem iff2 [elim]: - assumes "A \ B" and B - shows A -proof - - from \A \ B\ have "(A \ B) \ (B \ A)" - unfolding iff_def . - then have "B \ A" .. - from this and \B\ show A .. -qed - - -subsection \Equality\ - -axiomatization equal :: "i \ i \ o" (infixl "=" 50) - where refl [intro]: "x = x" - and subst: "x = y \ P x \ P y" - -theorem trans [trans]: "x = y \ y = z \ x = z" - by (rule subst) - -theorem sym [sym]: "x = y \ y = x" -proof - - assume "x = y" - from this and refl show "y = x" - by (rule subst) -qed - - -subsection \Quantifiers\ - -axiomatization All :: "(i \ o) \ o" (binder "\" 10) - where allI [intro]: "(\x. P x) \ \x. P x" - and allD [dest]: "\x. P x \ P a" - -axiomatization Ex :: "(i \ o) \ o" (binder "\" 10) - where exI [intro]: "P a \ \x. P x" - and exE [elim]: "\x. P x \ (\x. P x \ C) \ C" - - -lemma "(\x. P (f x)) \ (\y. P y)" -proof - assume "\x. P (f x)" - then obtain x where "P (f x)" .. - then show "\y. P y" .. -qed - -lemma "(\x. \y. R x y) \ (\y. \x. R x y)" -proof - assume "\x. \y. R x y" - then obtain x where "\y. R x y" .. - show "\y. \x. R x y" - proof - fix y - from \\y. R x y\ have "R x y" .. - then show "\x. R x y" .. - qed -qed - -end diff -r 7b34a932eeb6 -r e5df9c8d9d4b src/HOL/Isar_Examples/Higher_Order_Logic.thy --- a/src/HOL/Isar_Examples/Higher_Order_Logic.thy Sat Jun 06 10:58:13 2020 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,520 +0,0 @@ -(* 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" - for f g :: "'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 \ - \<^medskip> - 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). - \<^medskip> -\ - -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 diff -r 7b34a932eeb6 -r e5df9c8d9d4b src/HOL/ROOT --- a/src/HOL/ROOT Sat Jun 06 10:58:13 2020 +0200 +++ b/src/HOL/ROOT Mon Jun 08 15:09:57 2020 +0200 @@ -702,8 +702,6 @@ Mutilated_Checkerboard Puzzle Summation - First_Order_Logic - Higher_Order_Logic document_files "root.bib" "root.tex" diff -r 7b34a932eeb6 -r e5df9c8d9d4b src/Pure/Examples/First_Order_Logic.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Pure/Examples/First_Order_Logic.thy Mon Jun 08 15:09:57 2020 +0200 @@ -0,0 +1,160 @@ +(* Title: Pure/Examples/First_Order_Logic.thy + Author: Makarius +*) + +section \A simple formulation of First-Order Logic\ + +text \ + The subsequent theory development illustrates single-sorted intuitionistic + first-order logic with equality, formulated within the Pure framework. +\ + +theory First_Order_Logic + imports Pure +begin + +subsection \Abstract syntax\ + +typedecl i +typedecl o + +judgment Trueprop :: "o \ prop" ("_" 5) + + +subsection \Propositional logic\ + +axiomatization false :: o ("\") + where falseE [elim]: "\ \ A" + + +axiomatization imp :: "o \ o \ o" (infixr "\" 25) + where impI [intro]: "(A \ B) \ A \ B" + and mp [dest]: "A \ B \ A \ B" + + +axiomatization conj :: "o \ o \ o" (infixr "\" 35) + where conjI [intro]: "A \ B \ A \ B" + and conjD1: "A \ B \ A" + and conjD2: "A \ B \ B" + +theorem conjE [elim]: + assumes "A \ B" + obtains A and B +proof + from \A \ B\ show A + by (rule conjD1) + from \A \ B\ show B + by (rule conjD2) +qed + + +axiomatization disj :: "o \ o \ o" (infixr "\" 30) + where disjE [elim]: "A \ B \ (A \ C) \ (B \ C) \ C" + and disjI1 [intro]: "A \ A \ B" + and disjI2 [intro]: "B \ A \ B" + + +definition true :: o ("\") + where "\ \ \ \ \" + +theorem trueI [intro]: \ + unfolding true_def .. + + +definition not :: "o \ o" ("\ _" [40] 40) + where "\ A \ A \ \" + +theorem notI [intro]: "(A \ \) \ \ A" + unfolding not_def .. + +theorem notE [elim]: "\ A \ A \ B" + unfolding not_def +proof - + assume "A \ \" and A + then have \ .. + then show B .. +qed + + +definition iff :: "o \ o \ o" (infixr "\" 25) + where "A \ B \ (A \ B) \ (B \ A)" + +theorem iffI [intro]: + assumes "A \ B" + and "B \ A" + shows "A \ B" + unfolding iff_def +proof + from \A \ B\ show "A \ B" .. + from \B \ A\ show "B \ A" .. +qed + +theorem iff1 [elim]: + assumes "A \ B" and A + shows B +proof - + from \A \ B\ have "(A \ B) \ (B \ A)" + unfolding iff_def . + then have "A \ B" .. + from this and \A\ show B .. +qed + +theorem iff2 [elim]: + assumes "A \ B" and B + shows A +proof - + from \A \ B\ have "(A \ B) \ (B \ A)" + unfolding iff_def . + then have "B \ A" .. + from this and \B\ show A .. +qed + + +subsection \Equality\ + +axiomatization equal :: "i \ i \ o" (infixl "=" 50) + where refl [intro]: "x = x" + and subst: "x = y \ P x \ P y" + +theorem trans [trans]: "x = y \ y = z \ x = z" + by (rule subst) + +theorem sym [sym]: "x = y \ y = x" +proof - + assume "x = y" + from this and refl show "y = x" + by (rule subst) +qed + + +subsection \Quantifiers\ + +axiomatization All :: "(i \ o) \ o" (binder "\" 10) + where allI [intro]: "(\x. P x) \ \x. P x" + and allD [dest]: "\x. P x \ P a" + +axiomatization Ex :: "(i \ o) \ o" (binder "\" 10) + where exI [intro]: "P a \ \x. P x" + and exE [elim]: "\x. P x \ (\x. P x \ C) \ C" + + +lemma "(\x. P (f x)) \ (\y. P y)" +proof + assume "\x. P (f x)" + then obtain x where "P (f x)" .. + then show "\y. P y" .. +qed + +lemma "(\x. \y. R x y) \ (\y. \x. R x y)" +proof + assume "\x. \y. R x y" + then obtain x where "\y. R x y" .. + show "\y. \x. R x y" + proof + fix y + from \\y. R x y\ have "R x y" .. + then show "\x. R x y" .. + qed +qed + +end diff -r 7b34a932eeb6 -r e5df9c8d9d4b src/Pure/Examples/Higher_Order_Logic.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Pure/Examples/Higher_Order_Logic.thy Mon Jun 08 15:09:57 2020 +0200 @@ -0,0 +1,520 @@ +(* Title: Pure/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" + for f g :: "'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 \ + \<^medskip> + 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). + \<^medskip> +\ + +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 diff -r 7b34a932eeb6 -r e5df9c8d9d4b src/Pure/Examples/document/root.bib --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Pure/Examples/document/root.bib Mon Jun 08 15:09:57 2020 +0200 @@ -0,0 +1,15 @@ +@article{church40, + author = "Alonzo Church", + title = "A Formulation of the Simple Theory of Types", + journal = "Journal of Symbolic Logic", + year = 1940, + volume = 5, + pages = "56-68"} + +@TechReport{Gordon:1985:HOL, + author = {M. J. C. Gordon}, + title = {{HOL}: A machine oriented formulation of higher order logic}, + institution = {University of Cambridge Computer Laboratory}, + year = 1985, + number = 68 +} diff -r 7b34a932eeb6 -r e5df9c8d9d4b src/Pure/Examples/document/root.tex --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Pure/Examples/document/root.tex Mon Jun 08 15:09:57 2020 +0200 @@ -0,0 +1,24 @@ +\documentclass[11pt,a4paper]{article} +\usepackage[utf8]{inputenc} +\usepackage[T1]{fontenc} +\usepackage{ifthen,proof,amssymb,isabelle,isabellesym} + +\isabellestyle{literal} +\usepackage{pdfsetup}\urlstyle{rm} + + +\hyphenation{Isabelle} + +\begin{document} + +\title{Notable Examples in Isabelle/Pure} +\maketitle + +\parindent 0pt \parskip 0.5ex + +\input{session} + +\bibliographystyle{abbrv} +\bibliography{root} + +\end{document} diff -r 7b34a932eeb6 -r e5df9c8d9d4b src/Pure/ROOT --- a/src/Pure/ROOT Sat Jun 06 10:58:13 2020 +0200 +++ b/src/Pure/ROOT Mon Jun 08 15:09:57 2020 +0200 @@ -10,3 +10,14 @@ theories ML_Bootstrap (global) Sessions + +session "Pure-Examples" in Examples = Pure + + description " + Notable Examples in Isabelle/Pure. + " + theories + First_Order_Logic + Higher_Order_Logic + document_files + "root.bib" + "root.tex"