--- 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.
--- 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 @@
<li><a href="Cube/index.html">Cube (The Lambda Cube)</a></li>
- <li><a href="Pure/Pure/index.html">The Pure logical framework</a></li>
+ <li><a href="Pure/index.html">The Pure logical framework</a></li>
<li><a href="Doc/index.html">Sources of Documentation</a></li>
</ul>
--- 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>\<open>~~/src/HOL/Isar_Examples\<close>. 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>\<open>~~/src/HOL/Isar_Examples/Higher_Order_Logic.thy\<close>). Isabelle/FOL @{cite
+ \<^file>\<open>~~/src/Pure/Examples/Higher_Order_Logic.thy\<close>). Isabelle/FOL @{cite
"isabelle-logics"} and Isabelle/ZF @{cite "isabelle-ZF"} also work, but are
much less developed.
--- 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 \<open>A simple formulation of First-Order Logic\<close>
-
-text \<open>
- The subsequent theory development illustrates single-sorted intuitionistic
- first-order logic with equality, formulated within the Pure framework.
-\<close>
-
-theory First_Order_Logic
- imports Pure
-begin
-
-subsection \<open>Abstract syntax\<close>
-
-typedecl i
-typedecl o
-
-judgment Trueprop :: "o \<Rightarrow> prop" ("_" 5)
-
-
-subsection \<open>Propositional logic\<close>
-
-axiomatization false :: o ("\<bottom>")
- where falseE [elim]: "\<bottom> \<Longrightarrow> A"
-
-
-axiomatization imp :: "o \<Rightarrow> o \<Rightarrow> o" (infixr "\<longrightarrow>" 25)
- where impI [intro]: "(A \<Longrightarrow> B) \<Longrightarrow> A \<longrightarrow> B"
- and mp [dest]: "A \<longrightarrow> B \<Longrightarrow> A \<Longrightarrow> B"
-
-
-axiomatization conj :: "o \<Rightarrow> o \<Rightarrow> o" (infixr "\<and>" 35)
- where conjI [intro]: "A \<Longrightarrow> B \<Longrightarrow> A \<and> B"
- and conjD1: "A \<and> B \<Longrightarrow> A"
- and conjD2: "A \<and> B \<Longrightarrow> B"
-
-theorem conjE [elim]:
- assumes "A \<and> B"
- obtains A and B
-proof
- from \<open>A \<and> B\<close> show A
- by (rule conjD1)
- from \<open>A \<and> B\<close> show B
- by (rule conjD2)
-qed
-
-
-axiomatization disj :: "o \<Rightarrow> o \<Rightarrow> o" (infixr "\<or>" 30)
- where disjE [elim]: "A \<or> B \<Longrightarrow> (A \<Longrightarrow> C) \<Longrightarrow> (B \<Longrightarrow> C) \<Longrightarrow> C"
- and disjI1 [intro]: "A \<Longrightarrow> A \<or> B"
- and disjI2 [intro]: "B \<Longrightarrow> A \<or> B"
-
-
-definition true :: o ("\<top>")
- where "\<top> \<equiv> \<bottom> \<longrightarrow> \<bottom>"
-
-theorem trueI [intro]: \<top>
- unfolding true_def ..
-
-
-definition not :: "o \<Rightarrow> o" ("\<not> _" [40] 40)
- where "\<not> A \<equiv> A \<longrightarrow> \<bottom>"
-
-theorem notI [intro]: "(A \<Longrightarrow> \<bottom>) \<Longrightarrow> \<not> A"
- unfolding not_def ..
-
-theorem notE [elim]: "\<not> A \<Longrightarrow> A \<Longrightarrow> B"
- unfolding not_def
-proof -
- assume "A \<longrightarrow> \<bottom>" and A
- then have \<bottom> ..
- then show B ..
-qed
-
-
-definition iff :: "o \<Rightarrow> o \<Rightarrow> o" (infixr "\<longleftrightarrow>" 25)
- where "A \<longleftrightarrow> B \<equiv> (A \<longrightarrow> B) \<and> (B \<longrightarrow> A)"
-
-theorem iffI [intro]:
- assumes "A \<Longrightarrow> B"
- and "B \<Longrightarrow> A"
- shows "A \<longleftrightarrow> B"
- unfolding iff_def
-proof
- from \<open>A \<Longrightarrow> B\<close> show "A \<longrightarrow> B" ..
- from \<open>B \<Longrightarrow> A\<close> show "B \<longrightarrow> A" ..
-qed
-
-theorem iff1 [elim]:
- assumes "A \<longleftrightarrow> B" and A
- shows B
-proof -
- from \<open>A \<longleftrightarrow> B\<close> have "(A \<longrightarrow> B) \<and> (B \<longrightarrow> A)"
- unfolding iff_def .
- then have "A \<longrightarrow> B" ..
- from this and \<open>A\<close> show B ..
-qed
-
-theorem iff2 [elim]:
- assumes "A \<longleftrightarrow> B" and B
- shows A
-proof -
- from \<open>A \<longleftrightarrow> B\<close> have "(A \<longrightarrow> B) \<and> (B \<longrightarrow> A)"
- unfolding iff_def .
- then have "B \<longrightarrow> A" ..
- from this and \<open>B\<close> show A ..
-qed
-
-
-subsection \<open>Equality\<close>
-
-axiomatization equal :: "i \<Rightarrow> i \<Rightarrow> o" (infixl "=" 50)
- where refl [intro]: "x = x"
- and subst: "x = y \<Longrightarrow> P x \<Longrightarrow> P y"
-
-theorem trans [trans]: "x = y \<Longrightarrow> y = z \<Longrightarrow> x = z"
- by (rule subst)
-
-theorem sym [sym]: "x = y \<Longrightarrow> y = x"
-proof -
- assume "x = y"
- from this and refl show "y = x"
- by (rule subst)
-qed
-
-
-subsection \<open>Quantifiers\<close>
-
-axiomatization All :: "(i \<Rightarrow> o) \<Rightarrow> o" (binder "\<forall>" 10)
- where allI [intro]: "(\<And>x. P x) \<Longrightarrow> \<forall>x. P x"
- and allD [dest]: "\<forall>x. P x \<Longrightarrow> P a"
-
-axiomatization Ex :: "(i \<Rightarrow> o) \<Rightarrow> o" (binder "\<exists>" 10)
- where exI [intro]: "P a \<Longrightarrow> \<exists>x. P x"
- and exE [elim]: "\<exists>x. P x \<Longrightarrow> (\<And>x. P x \<Longrightarrow> C) \<Longrightarrow> C"
-
-
-lemma "(\<exists>x. P (f x)) \<longrightarrow> (\<exists>y. P y)"
-proof
- assume "\<exists>x. P (f x)"
- then obtain x where "P (f x)" ..
- then show "\<exists>y. P y" ..
-qed
-
-lemma "(\<exists>x. \<forall>y. R x y) \<longrightarrow> (\<forall>y. \<exists>x. R x y)"
-proof
- assume "\<exists>x. \<forall>y. R x y"
- then obtain x where "\<forall>y. R x y" ..
- show "\<forall>y. \<exists>x. R x y"
- proof
- fix y
- from \<open>\<forall>y. R x y\<close> have "R x y" ..
- then show "\<exists>x. R x y" ..
- qed
-qed
-
-end
--- 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 \<open>Foundations of HOL\<close>
-
-theory Higher_Order_Logic
- imports Pure
-begin
-
-text \<open>
- 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 \<open>\<lambda>\<close>-calculus and Constructive Type Theory. Thus it fits
- nicely to the underlying Natural Deduction framework of Isabelle/Pure and
- Isabelle/Isar.
-\<close>
-
-
-section \<open>HOL syntax within Pure\<close>
-
-class type
-default_sort type
-
-typedecl o
-instance o :: type ..
-instance "fun" :: (type, type) type ..
-
-judgment Trueprop :: "o \<Rightarrow> prop" ("_" 5)
-
-
-section \<open>Minimal logic (axiomatization)\<close>
-
-axiomatization imp :: "o \<Rightarrow> o \<Rightarrow> o" (infixr "\<longrightarrow>" 25)
- where impI [intro]: "(A \<Longrightarrow> B) \<Longrightarrow> A \<longrightarrow> B"
- and impE [dest, trans]: "A \<longrightarrow> B \<Longrightarrow> A \<Longrightarrow> B"
-
-axiomatization All :: "('a \<Rightarrow> o) \<Rightarrow> o" (binder "\<forall>" 10)
- where allI [intro]: "(\<And>x. P x) \<Longrightarrow> \<forall>x. P x"
- and allE [dest]: "\<forall>x. P x \<Longrightarrow> P a"
-
-lemma atomize_imp [atomize]: "(A \<Longrightarrow> B) \<equiv> Trueprop (A \<longrightarrow> B)"
- by standard (fact impI, fact impE)
-
-lemma atomize_all [atomize]: "(\<And>x. P x) \<equiv> Trueprop (\<forall>x. P x)"
- by standard (fact allI, fact allE)
-
-
-subsubsection \<open>Derived connectives\<close>
-
-definition False :: o
- where "False \<equiv> \<forall>A. A"
-
-lemma FalseE [elim]:
- assumes "False"
- shows A
-proof -
- from \<open>False\<close> have "\<forall>A. A" by (simp only: False_def)
- then show A ..
-qed
-
-
-definition True :: o
- where "True \<equiv> False \<longrightarrow> False"
-
-lemma TrueI [intro]: True
- unfolding True_def ..
-
-
-definition not :: "o \<Rightarrow> o" ("\<not> _" [40] 40)
- where "not \<equiv> \<lambda>A. A \<longrightarrow> False"
-
-lemma notI [intro]:
- assumes "A \<Longrightarrow> False"
- shows "\<not> A"
- using assms unfolding not_def ..
-
-lemma notE [elim]:
- assumes "\<not> A" and A
- shows B
-proof -
- from \<open>\<not> A\<close> have "A \<longrightarrow> False" by (simp only: not_def)
- from this and \<open>A\<close> have "False" ..
- then show B ..
-qed
-
-lemma notE': "A \<Longrightarrow> \<not> A \<Longrightarrow> B"
- by (rule notE)
-
-lemmas contradiction = notE notE' \<comment> \<open>proof by contradiction in any order\<close>
-
-
-definition conj :: "o \<Rightarrow> o \<Rightarrow> o" (infixr "\<and>" 35)
- where "A \<and> B \<equiv> \<forall>C. (A \<longrightarrow> B \<longrightarrow> C) \<longrightarrow> C"
-
-lemma conjI [intro]:
- assumes A and B
- shows "A \<and> B"
- unfolding conj_def
-proof
- fix C
- show "(A \<longrightarrow> B \<longrightarrow> C) \<longrightarrow> C"
- proof
- assume "A \<longrightarrow> B \<longrightarrow> C"
- also note \<open>A\<close>
- also note \<open>B\<close>
- finally show C .
- qed
-qed
-
-lemma conjE [elim]:
- assumes "A \<and> B"
- obtains A and B
-proof
- from \<open>A \<and> B\<close> have *: "(A \<longrightarrow> B \<longrightarrow> C) \<longrightarrow> C" for C
- unfolding conj_def ..
- show A
- proof -
- note * [of A]
- also have "A \<longrightarrow> B \<longrightarrow> A"
- proof
- assume A
- then show "B \<longrightarrow> A" ..
- qed
- finally show ?thesis .
- qed
- show B
- proof -
- note * [of B]
- also have "A \<longrightarrow> B \<longrightarrow> B"
- proof
- show "B \<longrightarrow> B" ..
- qed
- finally show ?thesis .
- qed
-qed
-
-
-definition disj :: "o \<Rightarrow> o \<Rightarrow> o" (infixr "\<or>" 30)
- where "A \<or> B \<equiv> \<forall>C. (A \<longrightarrow> C) \<longrightarrow> (B \<longrightarrow> C) \<longrightarrow> C"
-
-lemma disjI1 [intro]:
- assumes A
- shows "A \<or> B"
- unfolding disj_def
-proof
- fix C
- show "(A \<longrightarrow> C) \<longrightarrow> (B \<longrightarrow> C) \<longrightarrow> C"
- proof
- assume "A \<longrightarrow> C"
- from this and \<open>A\<close> have C ..
- then show "(B \<longrightarrow> C) \<longrightarrow> C" ..
- qed
-qed
-
-lemma disjI2 [intro]:
- assumes B
- shows "A \<or> B"
- unfolding disj_def
-proof
- fix C
- show "(A \<longrightarrow> C) \<longrightarrow> (B \<longrightarrow> C) \<longrightarrow> C"
- proof
- show "(B \<longrightarrow> C) \<longrightarrow> C"
- proof
- assume "B \<longrightarrow> C"
- from this and \<open>B\<close> show C ..
- qed
- qed
-qed
-
-lemma disjE [elim]:
- assumes "A \<or> B"
- obtains (a) A | (b) B
-proof -
- from \<open>A \<or> B\<close> have "(A \<longrightarrow> thesis) \<longrightarrow> (B \<longrightarrow> thesis) \<longrightarrow> thesis"
- unfolding disj_def ..
- also have "A \<longrightarrow> thesis"
- proof
- assume A
- then show thesis by (rule a)
- qed
- also have "B \<longrightarrow> thesis"
- proof
- assume B
- then show thesis by (rule b)
- qed
- finally show thesis .
-qed
-
-
-definition Ex :: "('a \<Rightarrow> o) \<Rightarrow> o" (binder "\<exists>" 10)
- where "\<exists>x. P x \<equiv> \<forall>C. (\<forall>x. P x \<longrightarrow> C) \<longrightarrow> C"
-
-lemma exI [intro]: "P a \<Longrightarrow> \<exists>x. P x"
- unfolding Ex_def
-proof
- fix C
- assume "P a"
- show "(\<forall>x. P x \<longrightarrow> C) \<longrightarrow> C"
- proof
- assume "\<forall>x. P x \<longrightarrow> C"
- then have "P a \<longrightarrow> C" ..
- from this and \<open>P a\<close> show C ..
- qed
-qed
-
-lemma exE [elim]:
- assumes "\<exists>x. P x"
- obtains (that) x where "P x"
-proof -
- from \<open>\<exists>x. P x\<close> have "(\<forall>x. P x \<longrightarrow> thesis) \<longrightarrow> thesis"
- unfolding Ex_def ..
- also have "\<forall>x. P x \<longrightarrow> thesis"
- proof
- fix x
- show "P x \<longrightarrow> thesis"
- proof
- assume "P x"
- then show thesis by (rule that)
- qed
- qed
- finally show thesis .
-qed
-
-
-subsubsection \<open>Extensional equality\<close>
-
-axiomatization equal :: "'a \<Rightarrow> 'a \<Rightarrow> o" (infixl "=" 50)
- where refl [intro]: "x = x"
- and subst: "x = y \<Longrightarrow> P x \<Longrightarrow> P y"
-
-abbreviation not_equal :: "'a \<Rightarrow> 'a \<Rightarrow> o" (infixl "\<noteq>" 50)
- where "x \<noteq> y \<equiv> \<not> (x = y)"
-
-abbreviation iff :: "o \<Rightarrow> o \<Rightarrow> o" (infixr "\<longleftrightarrow>" 25)
- where "A \<longleftrightarrow> B \<equiv> A = B"
-
-axiomatization
- where ext [intro]: "(\<And>x. f x = g x) \<Longrightarrow> f = g"
- and iff [intro]: "(A \<Longrightarrow> B) \<Longrightarrow> (B \<Longrightarrow> A) \<Longrightarrow> A \<longleftrightarrow> B"
- for f g :: "'a \<Rightarrow> 'b"
-
-lemma sym [sym]: "y = x" if "x = y"
- using that by (rule subst) (rule refl)
-
-lemma [trans]: "x = y \<Longrightarrow> P y \<Longrightarrow> P x"
- by (rule subst) (rule sym)
-
-lemma [trans]: "P x \<Longrightarrow> x = y \<Longrightarrow> 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 \<Longrightarrow> y = z \<Longrightarrow> x = z"
- by (rule subst)
-
-lemma iff1 [elim]: "A \<longleftrightarrow> B \<Longrightarrow> A \<Longrightarrow> B"
- by (rule subst)
-
-lemma iff2 [elim]: "A \<longleftrightarrow> B \<Longrightarrow> B \<Longrightarrow> A"
- by (rule subst) (rule sym)
-
-
-subsection \<open>Cantor's Theorem\<close>
-
-text \<open>
- Cantor's Theorem states that there is no surjection from a set to its
- powerset. The subsequent formulation uses elementary \<open>\<lambda>\<close>-calculus and
- predicate logic, with standard introduction and elimination rules.
-\<close>
-
-lemma iff_contradiction:
- assumes *: "\<not> A \<longleftrightarrow> A"
- shows C
-proof (rule notE)
- show "\<not> A"
- proof
- assume A
- with * have "\<not> A" ..
- from this and \<open>A\<close> show False ..
- qed
- with * show A ..
-qed
-
-theorem Cantor: "\<not> (\<exists>f :: 'a \<Rightarrow> 'a \<Rightarrow> o. \<forall>A. \<exists>x. A = f x)"
-proof
- assume "\<exists>f :: 'a \<Rightarrow> 'a \<Rightarrow> o. \<forall>A. \<exists>x. A = f x"
- then obtain f :: "'a \<Rightarrow> 'a \<Rightarrow> o" where *: "\<forall>A. \<exists>x. A = f x" ..
- let ?D = "\<lambda>x. \<not> f x x"
- from * have "\<exists>x. ?D = f x" ..
- then obtain a where "?D = f a" ..
- then have "?D a \<longleftrightarrow> f a a" using refl by (rule subst)
- then have "\<not> f a a \<longleftrightarrow> f a a" .
- then show False by (rule iff_contradiction)
-qed
-
-
-subsection \<open>Characterization of Classical Logic\<close>
-
-text \<open>
- The subsequent rules of classical reasoning are all equivalent.
-\<close>
-
-locale classical =
- assumes classical: "(\<not> A \<Longrightarrow> A) \<Longrightarrow> A"
- \<comment> \<open>predicate definition and hypothetical context\<close>
-begin
-
-lemma classical_contradiction:
- assumes "\<not> A \<Longrightarrow> False"
- shows A
-proof (rule classical)
- assume "\<not> A"
- then have False by (rule assms)
- then show A ..
-qed
-
-lemma double_negation:
- assumes "\<not> \<not> A"
- shows A
-proof (rule classical_contradiction)
- assume "\<not> A"
- with \<open>\<not> \<not> A\<close> show False by (rule contradiction)
-qed
-
-lemma tertium_non_datur: "A \<or> \<not> A"
-proof (rule double_negation)
- show "\<not> \<not> (A \<or> \<not> A)"
- proof
- assume "\<not> (A \<or> \<not> A)"
- have "\<not> A"
- proof
- assume A then have "A \<or> \<not> A" ..
- with \<open>\<not> (A \<or> \<not> A)\<close> show False by (rule contradiction)
- qed
- then have "A \<or> \<not> A" ..
- with \<open>\<not> (A \<or> \<not> A)\<close> show False by (rule contradiction)
- qed
-qed
-
-lemma classical_cases:
- obtains A | "\<not> A"
- using tertium_non_datur
-proof
- assume A
- then show thesis ..
-next
- assume "\<not> A"
- then show thesis ..
-qed
-
-end
-
-lemma classical_if_cases: classical
- if cases: "\<And>A C. (A \<Longrightarrow> C) \<Longrightarrow> (\<not> A \<Longrightarrow> C) \<Longrightarrow> C"
-proof
- fix A
- assume *: "\<not> A \<Longrightarrow> A"
- show A
- proof (rule cases)
- assume A
- then show A .
- next
- assume "\<not> A"
- then show A by (rule *)
- qed
-qed
-
-
-section \<open>Peirce's Law\<close>
-
-text \<open>
- Peirce's Law is another characterization of classical reasoning. Its
- statement only requires implication.
-\<close>
-
-theorem (in classical) Peirce's_Law: "((A \<longrightarrow> B) \<longrightarrow> A) \<longrightarrow> A"
-proof
- assume *: "(A \<longrightarrow> B) \<longrightarrow> A"
- show A
- proof (rule classical)
- assume "\<not> A"
- have "A \<longrightarrow> B"
- proof
- assume A
- with \<open>\<not> A\<close> show B by (rule contradiction)
- qed
- with * show A ..
- qed
-qed
-
-
-section \<open>Hilbert's choice operator (axiomatization)\<close>
-
-axiomatization Eps :: "('a \<Rightarrow> o) \<Rightarrow> 'a"
- where someI: "P x \<Longrightarrow> P (Eps P)"
-
-syntax "_Eps" :: "pttrn \<Rightarrow> o \<Rightarrow> 'a" ("(3SOME _./ _)" [0, 10] 10)
-translations "SOME x. P" \<rightleftharpoons> "CONST Eps (\<lambda>x. P)"
-
-text \<open>
- \<^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>
-\<close>
-
-theorem Diaconescu: "A \<or> \<not> A"
-proof -
- let ?P = "\<lambda>x. (A \<and> x) \<or> \<not> x"
- let ?Q = "\<lambda>x. (A \<and> \<not> x) \<or> x"
-
- have a: "?P (Eps ?P)"
- proof (rule someI)
- have "\<not> 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 \<and> Eps ?P"
- then have A ..
- then show ?thesis ..
- next
- assume "\<not> Eps ?P"
- from b show ?thesis
- proof
- assume "A \<and> \<not> Eps ?Q"
- then have A ..
- then show ?thesis ..
- next
- assume "Eps ?Q"
- have neq: "?P \<noteq> ?Q"
- proof
- assume "?P = ?Q"
- then have "Eps ?P \<longleftrightarrow> Eps ?Q" by (rule arg_cong)
- also note \<open>Eps ?Q\<close>
- finally have "Eps ?P" .
- with \<open>\<not> Eps ?P\<close> show False by (rule contradiction)
- qed
- have "\<not> A"
- proof
- assume A
- have "?P = ?Q"
- proof (rule ext)
- show "?P x \<longleftrightarrow> ?Q x" for x
- proof
- assume "?P x"
- then show "?Q x"
- proof
- assume "\<not> x"
- with \<open>A\<close> have "A \<and> \<not> x" ..
- then show ?thesis ..
- next
- assume "A \<and> x"
- then have x ..
- then show ?thesis ..
- qed
- next
- assume "?Q x"
- then show "?P x"
- proof
- assume "A \<and> \<not> x"
- then have "\<not> x" ..
- then show ?thesis ..
- next
- assume x
- with \<open>A\<close> have "A \<and> x" ..
- then show ?thesis ..
- qed
- qed
- qed
- with neq show False by (rule contradiction)
- qed
- then show ?thesis ..
- qed
- qed
-qed
-
-text \<open>
- This means, the hypothetical predicate \<^const>\<open>classical\<close> always holds
- unconditionally (with all consequences).
-\<close>
-
-interpretation classical
-proof (rule classical_if_cases)
- fix A C
- assume *: "A \<Longrightarrow> C"
- and **: "\<not> A \<Longrightarrow> C"
- from Diaconescu [of A] show C
- proof
- assume A
- then show C by (rule *)
- next
- assume "\<not> A"
- then show C by (rule **)
- qed
-qed
-
-thm classical
- classical_contradiction
- double_negation
- tertium_non_datur
- classical_cases
- Peirce's_Law
-
-end
--- 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"
--- /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 \<open>A simple formulation of First-Order Logic\<close>
+
+text \<open>
+ The subsequent theory development illustrates single-sorted intuitionistic
+ first-order logic with equality, formulated within the Pure framework.
+\<close>
+
+theory First_Order_Logic
+ imports Pure
+begin
+
+subsection \<open>Abstract syntax\<close>
+
+typedecl i
+typedecl o
+
+judgment Trueprop :: "o \<Rightarrow> prop" ("_" 5)
+
+
+subsection \<open>Propositional logic\<close>
+
+axiomatization false :: o ("\<bottom>")
+ where falseE [elim]: "\<bottom> \<Longrightarrow> A"
+
+
+axiomatization imp :: "o \<Rightarrow> o \<Rightarrow> o" (infixr "\<longrightarrow>" 25)
+ where impI [intro]: "(A \<Longrightarrow> B) \<Longrightarrow> A \<longrightarrow> B"
+ and mp [dest]: "A \<longrightarrow> B \<Longrightarrow> A \<Longrightarrow> B"
+
+
+axiomatization conj :: "o \<Rightarrow> o \<Rightarrow> o" (infixr "\<and>" 35)
+ where conjI [intro]: "A \<Longrightarrow> B \<Longrightarrow> A \<and> B"
+ and conjD1: "A \<and> B \<Longrightarrow> A"
+ and conjD2: "A \<and> B \<Longrightarrow> B"
+
+theorem conjE [elim]:
+ assumes "A \<and> B"
+ obtains A and B
+proof
+ from \<open>A \<and> B\<close> show A
+ by (rule conjD1)
+ from \<open>A \<and> B\<close> show B
+ by (rule conjD2)
+qed
+
+
+axiomatization disj :: "o \<Rightarrow> o \<Rightarrow> o" (infixr "\<or>" 30)
+ where disjE [elim]: "A \<or> B \<Longrightarrow> (A \<Longrightarrow> C) \<Longrightarrow> (B \<Longrightarrow> C) \<Longrightarrow> C"
+ and disjI1 [intro]: "A \<Longrightarrow> A \<or> B"
+ and disjI2 [intro]: "B \<Longrightarrow> A \<or> B"
+
+
+definition true :: o ("\<top>")
+ where "\<top> \<equiv> \<bottom> \<longrightarrow> \<bottom>"
+
+theorem trueI [intro]: \<top>
+ unfolding true_def ..
+
+
+definition not :: "o \<Rightarrow> o" ("\<not> _" [40] 40)
+ where "\<not> A \<equiv> A \<longrightarrow> \<bottom>"
+
+theorem notI [intro]: "(A \<Longrightarrow> \<bottom>) \<Longrightarrow> \<not> A"
+ unfolding not_def ..
+
+theorem notE [elim]: "\<not> A \<Longrightarrow> A \<Longrightarrow> B"
+ unfolding not_def
+proof -
+ assume "A \<longrightarrow> \<bottom>" and A
+ then have \<bottom> ..
+ then show B ..
+qed
+
+
+definition iff :: "o \<Rightarrow> o \<Rightarrow> o" (infixr "\<longleftrightarrow>" 25)
+ where "A \<longleftrightarrow> B \<equiv> (A \<longrightarrow> B) \<and> (B \<longrightarrow> A)"
+
+theorem iffI [intro]:
+ assumes "A \<Longrightarrow> B"
+ and "B \<Longrightarrow> A"
+ shows "A \<longleftrightarrow> B"
+ unfolding iff_def
+proof
+ from \<open>A \<Longrightarrow> B\<close> show "A \<longrightarrow> B" ..
+ from \<open>B \<Longrightarrow> A\<close> show "B \<longrightarrow> A" ..
+qed
+
+theorem iff1 [elim]:
+ assumes "A \<longleftrightarrow> B" and A
+ shows B
+proof -
+ from \<open>A \<longleftrightarrow> B\<close> have "(A \<longrightarrow> B) \<and> (B \<longrightarrow> A)"
+ unfolding iff_def .
+ then have "A \<longrightarrow> B" ..
+ from this and \<open>A\<close> show B ..
+qed
+
+theorem iff2 [elim]:
+ assumes "A \<longleftrightarrow> B" and B
+ shows A
+proof -
+ from \<open>A \<longleftrightarrow> B\<close> have "(A \<longrightarrow> B) \<and> (B \<longrightarrow> A)"
+ unfolding iff_def .
+ then have "B \<longrightarrow> A" ..
+ from this and \<open>B\<close> show A ..
+qed
+
+
+subsection \<open>Equality\<close>
+
+axiomatization equal :: "i \<Rightarrow> i \<Rightarrow> o" (infixl "=" 50)
+ where refl [intro]: "x = x"
+ and subst: "x = y \<Longrightarrow> P x \<Longrightarrow> P y"
+
+theorem trans [trans]: "x = y \<Longrightarrow> y = z \<Longrightarrow> x = z"
+ by (rule subst)
+
+theorem sym [sym]: "x = y \<Longrightarrow> y = x"
+proof -
+ assume "x = y"
+ from this and refl show "y = x"
+ by (rule subst)
+qed
+
+
+subsection \<open>Quantifiers\<close>
+
+axiomatization All :: "(i \<Rightarrow> o) \<Rightarrow> o" (binder "\<forall>" 10)
+ where allI [intro]: "(\<And>x. P x) \<Longrightarrow> \<forall>x. P x"
+ and allD [dest]: "\<forall>x. P x \<Longrightarrow> P a"
+
+axiomatization Ex :: "(i \<Rightarrow> o) \<Rightarrow> o" (binder "\<exists>" 10)
+ where exI [intro]: "P a \<Longrightarrow> \<exists>x. P x"
+ and exE [elim]: "\<exists>x. P x \<Longrightarrow> (\<And>x. P x \<Longrightarrow> C) \<Longrightarrow> C"
+
+
+lemma "(\<exists>x. P (f x)) \<longrightarrow> (\<exists>y. P y)"
+proof
+ assume "\<exists>x. P (f x)"
+ then obtain x where "P (f x)" ..
+ then show "\<exists>y. P y" ..
+qed
+
+lemma "(\<exists>x. \<forall>y. R x y) \<longrightarrow> (\<forall>y. \<exists>x. R x y)"
+proof
+ assume "\<exists>x. \<forall>y. R x y"
+ then obtain x where "\<forall>y. R x y" ..
+ show "\<forall>y. \<exists>x. R x y"
+ proof
+ fix y
+ from \<open>\<forall>y. R x y\<close> have "R x y" ..
+ then show "\<exists>x. R x y" ..
+ qed
+qed
+
+end
--- /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 \<open>Foundations of HOL\<close>
+
+theory Higher_Order_Logic
+ imports Pure
+begin
+
+text \<open>
+ 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 \<open>\<lambda>\<close>-calculus and Constructive Type Theory. Thus it fits
+ nicely to the underlying Natural Deduction framework of Isabelle/Pure and
+ Isabelle/Isar.
+\<close>
+
+
+section \<open>HOL syntax within Pure\<close>
+
+class type
+default_sort type
+
+typedecl o
+instance o :: type ..
+instance "fun" :: (type, type) type ..
+
+judgment Trueprop :: "o \<Rightarrow> prop" ("_" 5)
+
+
+section \<open>Minimal logic (axiomatization)\<close>
+
+axiomatization imp :: "o \<Rightarrow> o \<Rightarrow> o" (infixr "\<longrightarrow>" 25)
+ where impI [intro]: "(A \<Longrightarrow> B) \<Longrightarrow> A \<longrightarrow> B"
+ and impE [dest, trans]: "A \<longrightarrow> B \<Longrightarrow> A \<Longrightarrow> B"
+
+axiomatization All :: "('a \<Rightarrow> o) \<Rightarrow> o" (binder "\<forall>" 10)
+ where allI [intro]: "(\<And>x. P x) \<Longrightarrow> \<forall>x. P x"
+ and allE [dest]: "\<forall>x. P x \<Longrightarrow> P a"
+
+lemma atomize_imp [atomize]: "(A \<Longrightarrow> B) \<equiv> Trueprop (A \<longrightarrow> B)"
+ by standard (fact impI, fact impE)
+
+lemma atomize_all [atomize]: "(\<And>x. P x) \<equiv> Trueprop (\<forall>x. P x)"
+ by standard (fact allI, fact allE)
+
+
+subsubsection \<open>Derived connectives\<close>
+
+definition False :: o
+ where "False \<equiv> \<forall>A. A"
+
+lemma FalseE [elim]:
+ assumes "False"
+ shows A
+proof -
+ from \<open>False\<close> have "\<forall>A. A" by (simp only: False_def)
+ then show A ..
+qed
+
+
+definition True :: o
+ where "True \<equiv> False \<longrightarrow> False"
+
+lemma TrueI [intro]: True
+ unfolding True_def ..
+
+
+definition not :: "o \<Rightarrow> o" ("\<not> _" [40] 40)
+ where "not \<equiv> \<lambda>A. A \<longrightarrow> False"
+
+lemma notI [intro]:
+ assumes "A \<Longrightarrow> False"
+ shows "\<not> A"
+ using assms unfolding not_def ..
+
+lemma notE [elim]:
+ assumes "\<not> A" and A
+ shows B
+proof -
+ from \<open>\<not> A\<close> have "A \<longrightarrow> False" by (simp only: not_def)
+ from this and \<open>A\<close> have "False" ..
+ then show B ..
+qed
+
+lemma notE': "A \<Longrightarrow> \<not> A \<Longrightarrow> B"
+ by (rule notE)
+
+lemmas contradiction = notE notE' \<comment> \<open>proof by contradiction in any order\<close>
+
+
+definition conj :: "o \<Rightarrow> o \<Rightarrow> o" (infixr "\<and>" 35)
+ where "A \<and> B \<equiv> \<forall>C. (A \<longrightarrow> B \<longrightarrow> C) \<longrightarrow> C"
+
+lemma conjI [intro]:
+ assumes A and B
+ shows "A \<and> B"
+ unfolding conj_def
+proof
+ fix C
+ show "(A \<longrightarrow> B \<longrightarrow> C) \<longrightarrow> C"
+ proof
+ assume "A \<longrightarrow> B \<longrightarrow> C"
+ also note \<open>A\<close>
+ also note \<open>B\<close>
+ finally show C .
+ qed
+qed
+
+lemma conjE [elim]:
+ assumes "A \<and> B"
+ obtains A and B
+proof
+ from \<open>A \<and> B\<close> have *: "(A \<longrightarrow> B \<longrightarrow> C) \<longrightarrow> C" for C
+ unfolding conj_def ..
+ show A
+ proof -
+ note * [of A]
+ also have "A \<longrightarrow> B \<longrightarrow> A"
+ proof
+ assume A
+ then show "B \<longrightarrow> A" ..
+ qed
+ finally show ?thesis .
+ qed
+ show B
+ proof -
+ note * [of B]
+ also have "A \<longrightarrow> B \<longrightarrow> B"
+ proof
+ show "B \<longrightarrow> B" ..
+ qed
+ finally show ?thesis .
+ qed
+qed
+
+
+definition disj :: "o \<Rightarrow> o \<Rightarrow> o" (infixr "\<or>" 30)
+ where "A \<or> B \<equiv> \<forall>C. (A \<longrightarrow> C) \<longrightarrow> (B \<longrightarrow> C) \<longrightarrow> C"
+
+lemma disjI1 [intro]:
+ assumes A
+ shows "A \<or> B"
+ unfolding disj_def
+proof
+ fix C
+ show "(A \<longrightarrow> C) \<longrightarrow> (B \<longrightarrow> C) \<longrightarrow> C"
+ proof
+ assume "A \<longrightarrow> C"
+ from this and \<open>A\<close> have C ..
+ then show "(B \<longrightarrow> C) \<longrightarrow> C" ..
+ qed
+qed
+
+lemma disjI2 [intro]:
+ assumes B
+ shows "A \<or> B"
+ unfolding disj_def
+proof
+ fix C
+ show "(A \<longrightarrow> C) \<longrightarrow> (B \<longrightarrow> C) \<longrightarrow> C"
+ proof
+ show "(B \<longrightarrow> C) \<longrightarrow> C"
+ proof
+ assume "B \<longrightarrow> C"
+ from this and \<open>B\<close> show C ..
+ qed
+ qed
+qed
+
+lemma disjE [elim]:
+ assumes "A \<or> B"
+ obtains (a) A | (b) B
+proof -
+ from \<open>A \<or> B\<close> have "(A \<longrightarrow> thesis) \<longrightarrow> (B \<longrightarrow> thesis) \<longrightarrow> thesis"
+ unfolding disj_def ..
+ also have "A \<longrightarrow> thesis"
+ proof
+ assume A
+ then show thesis by (rule a)
+ qed
+ also have "B \<longrightarrow> thesis"
+ proof
+ assume B
+ then show thesis by (rule b)
+ qed
+ finally show thesis .
+qed
+
+
+definition Ex :: "('a \<Rightarrow> o) \<Rightarrow> o" (binder "\<exists>" 10)
+ where "\<exists>x. P x \<equiv> \<forall>C. (\<forall>x. P x \<longrightarrow> C) \<longrightarrow> C"
+
+lemma exI [intro]: "P a \<Longrightarrow> \<exists>x. P x"
+ unfolding Ex_def
+proof
+ fix C
+ assume "P a"
+ show "(\<forall>x. P x \<longrightarrow> C) \<longrightarrow> C"
+ proof
+ assume "\<forall>x. P x \<longrightarrow> C"
+ then have "P a \<longrightarrow> C" ..
+ from this and \<open>P a\<close> show C ..
+ qed
+qed
+
+lemma exE [elim]:
+ assumes "\<exists>x. P x"
+ obtains (that) x where "P x"
+proof -
+ from \<open>\<exists>x. P x\<close> have "(\<forall>x. P x \<longrightarrow> thesis) \<longrightarrow> thesis"
+ unfolding Ex_def ..
+ also have "\<forall>x. P x \<longrightarrow> thesis"
+ proof
+ fix x
+ show "P x \<longrightarrow> thesis"
+ proof
+ assume "P x"
+ then show thesis by (rule that)
+ qed
+ qed
+ finally show thesis .
+qed
+
+
+subsubsection \<open>Extensional equality\<close>
+
+axiomatization equal :: "'a \<Rightarrow> 'a \<Rightarrow> o" (infixl "=" 50)
+ where refl [intro]: "x = x"
+ and subst: "x = y \<Longrightarrow> P x \<Longrightarrow> P y"
+
+abbreviation not_equal :: "'a \<Rightarrow> 'a \<Rightarrow> o" (infixl "\<noteq>" 50)
+ where "x \<noteq> y \<equiv> \<not> (x = y)"
+
+abbreviation iff :: "o \<Rightarrow> o \<Rightarrow> o" (infixr "\<longleftrightarrow>" 25)
+ where "A \<longleftrightarrow> B \<equiv> A = B"
+
+axiomatization
+ where ext [intro]: "(\<And>x. f x = g x) \<Longrightarrow> f = g"
+ and iff [intro]: "(A \<Longrightarrow> B) \<Longrightarrow> (B \<Longrightarrow> A) \<Longrightarrow> A \<longleftrightarrow> B"
+ for f g :: "'a \<Rightarrow> 'b"
+
+lemma sym [sym]: "y = x" if "x = y"
+ using that by (rule subst) (rule refl)
+
+lemma [trans]: "x = y \<Longrightarrow> P y \<Longrightarrow> P x"
+ by (rule subst) (rule sym)
+
+lemma [trans]: "P x \<Longrightarrow> x = y \<Longrightarrow> 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 \<Longrightarrow> y = z \<Longrightarrow> x = z"
+ by (rule subst)
+
+lemma iff1 [elim]: "A \<longleftrightarrow> B \<Longrightarrow> A \<Longrightarrow> B"
+ by (rule subst)
+
+lemma iff2 [elim]: "A \<longleftrightarrow> B \<Longrightarrow> B \<Longrightarrow> A"
+ by (rule subst) (rule sym)
+
+
+subsection \<open>Cantor's Theorem\<close>
+
+text \<open>
+ Cantor's Theorem states that there is no surjection from a set to its
+ powerset. The subsequent formulation uses elementary \<open>\<lambda>\<close>-calculus and
+ predicate logic, with standard introduction and elimination rules.
+\<close>
+
+lemma iff_contradiction:
+ assumes *: "\<not> A \<longleftrightarrow> A"
+ shows C
+proof (rule notE)
+ show "\<not> A"
+ proof
+ assume A
+ with * have "\<not> A" ..
+ from this and \<open>A\<close> show False ..
+ qed
+ with * show A ..
+qed
+
+theorem Cantor: "\<not> (\<exists>f :: 'a \<Rightarrow> 'a \<Rightarrow> o. \<forall>A. \<exists>x. A = f x)"
+proof
+ assume "\<exists>f :: 'a \<Rightarrow> 'a \<Rightarrow> o. \<forall>A. \<exists>x. A = f x"
+ then obtain f :: "'a \<Rightarrow> 'a \<Rightarrow> o" where *: "\<forall>A. \<exists>x. A = f x" ..
+ let ?D = "\<lambda>x. \<not> f x x"
+ from * have "\<exists>x. ?D = f x" ..
+ then obtain a where "?D = f a" ..
+ then have "?D a \<longleftrightarrow> f a a" using refl by (rule subst)
+ then have "\<not> f a a \<longleftrightarrow> f a a" .
+ then show False by (rule iff_contradiction)
+qed
+
+
+subsection \<open>Characterization of Classical Logic\<close>
+
+text \<open>
+ The subsequent rules of classical reasoning are all equivalent.
+\<close>
+
+locale classical =
+ assumes classical: "(\<not> A \<Longrightarrow> A) \<Longrightarrow> A"
+ \<comment> \<open>predicate definition and hypothetical context\<close>
+begin
+
+lemma classical_contradiction:
+ assumes "\<not> A \<Longrightarrow> False"
+ shows A
+proof (rule classical)
+ assume "\<not> A"
+ then have False by (rule assms)
+ then show A ..
+qed
+
+lemma double_negation:
+ assumes "\<not> \<not> A"
+ shows A
+proof (rule classical_contradiction)
+ assume "\<not> A"
+ with \<open>\<not> \<not> A\<close> show False by (rule contradiction)
+qed
+
+lemma tertium_non_datur: "A \<or> \<not> A"
+proof (rule double_negation)
+ show "\<not> \<not> (A \<or> \<not> A)"
+ proof
+ assume "\<not> (A \<or> \<not> A)"
+ have "\<not> A"
+ proof
+ assume A then have "A \<or> \<not> A" ..
+ with \<open>\<not> (A \<or> \<not> A)\<close> show False by (rule contradiction)
+ qed
+ then have "A \<or> \<not> A" ..
+ with \<open>\<not> (A \<or> \<not> A)\<close> show False by (rule contradiction)
+ qed
+qed
+
+lemma classical_cases:
+ obtains A | "\<not> A"
+ using tertium_non_datur
+proof
+ assume A
+ then show thesis ..
+next
+ assume "\<not> A"
+ then show thesis ..
+qed
+
+end
+
+lemma classical_if_cases: classical
+ if cases: "\<And>A C. (A \<Longrightarrow> C) \<Longrightarrow> (\<not> A \<Longrightarrow> C) \<Longrightarrow> C"
+proof
+ fix A
+ assume *: "\<not> A \<Longrightarrow> A"
+ show A
+ proof (rule cases)
+ assume A
+ then show A .
+ next
+ assume "\<not> A"
+ then show A by (rule *)
+ qed
+qed
+
+
+section \<open>Peirce's Law\<close>
+
+text \<open>
+ Peirce's Law is another characterization of classical reasoning. Its
+ statement only requires implication.
+\<close>
+
+theorem (in classical) Peirce's_Law: "((A \<longrightarrow> B) \<longrightarrow> A) \<longrightarrow> A"
+proof
+ assume *: "(A \<longrightarrow> B) \<longrightarrow> A"
+ show A
+ proof (rule classical)
+ assume "\<not> A"
+ have "A \<longrightarrow> B"
+ proof
+ assume A
+ with \<open>\<not> A\<close> show B by (rule contradiction)
+ qed
+ with * show A ..
+ qed
+qed
+
+
+section \<open>Hilbert's choice operator (axiomatization)\<close>
+
+axiomatization Eps :: "('a \<Rightarrow> o) \<Rightarrow> 'a"
+ where someI: "P x \<Longrightarrow> P (Eps P)"
+
+syntax "_Eps" :: "pttrn \<Rightarrow> o \<Rightarrow> 'a" ("(3SOME _./ _)" [0, 10] 10)
+translations "SOME x. P" \<rightleftharpoons> "CONST Eps (\<lambda>x. P)"
+
+text \<open>
+ \<^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>
+\<close>
+
+theorem Diaconescu: "A \<or> \<not> A"
+proof -
+ let ?P = "\<lambda>x. (A \<and> x) \<or> \<not> x"
+ let ?Q = "\<lambda>x. (A \<and> \<not> x) \<or> x"
+
+ have a: "?P (Eps ?P)"
+ proof (rule someI)
+ have "\<not> 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 \<and> Eps ?P"
+ then have A ..
+ then show ?thesis ..
+ next
+ assume "\<not> Eps ?P"
+ from b show ?thesis
+ proof
+ assume "A \<and> \<not> Eps ?Q"
+ then have A ..
+ then show ?thesis ..
+ next
+ assume "Eps ?Q"
+ have neq: "?P \<noteq> ?Q"
+ proof
+ assume "?P = ?Q"
+ then have "Eps ?P \<longleftrightarrow> Eps ?Q" by (rule arg_cong)
+ also note \<open>Eps ?Q\<close>
+ finally have "Eps ?P" .
+ with \<open>\<not> Eps ?P\<close> show False by (rule contradiction)
+ qed
+ have "\<not> A"
+ proof
+ assume A
+ have "?P = ?Q"
+ proof (rule ext)
+ show "?P x \<longleftrightarrow> ?Q x" for x
+ proof
+ assume "?P x"
+ then show "?Q x"
+ proof
+ assume "\<not> x"
+ with \<open>A\<close> have "A \<and> \<not> x" ..
+ then show ?thesis ..
+ next
+ assume "A \<and> x"
+ then have x ..
+ then show ?thesis ..
+ qed
+ next
+ assume "?Q x"
+ then show "?P x"
+ proof
+ assume "A \<and> \<not> x"
+ then have "\<not> x" ..
+ then show ?thesis ..
+ next
+ assume x
+ with \<open>A\<close> have "A \<and> x" ..
+ then show ?thesis ..
+ qed
+ qed
+ qed
+ with neq show False by (rule contradiction)
+ qed
+ then show ?thesis ..
+ qed
+ qed
+qed
+
+text \<open>
+ This means, the hypothetical predicate \<^const>\<open>classical\<close> always holds
+ unconditionally (with all consequences).
+\<close>
+
+interpretation classical
+proof (rule classical_if_cases)
+ fix A C
+ assume *: "A \<Longrightarrow> C"
+ and **: "\<not> A \<Longrightarrow> C"
+ from Diaconescu [of A] show C
+ proof
+ assume A
+ then show C by (rule *)
+ next
+ assume "\<not> A"
+ then show C by (rule **)
+ qed
+qed
+
+thm classical
+ classical_contradiction
+ double_negation
+ tertium_non_datur
+ classical_cases
+ Peirce's_Law
+
+end
--- /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
+}
--- /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}
--- 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"