# HG changeset patch
# User wenzelm
# Date 1484598030 -3600
# Node ID 354bfbb27fbbee8a54230aefcc15682e3b5edaae
# Parent  49549acbf0250233681e9f44fd533f15ea557510
misc tuning and updates according to Curry-Club Dec-2016;

diff -r 49549acbf025 -r 354bfbb27fbb src/HOL/Isar_Examples/Higher_Order_Logic.thy
--- a/src/HOL/Isar_Examples/Higher_Order_Logic.thy	Mon Jan 16 16:12:29 2017 +0100
+++ b/src/HOL/Isar_Examples/Higher_Order_Logic.thy	Mon Jan 16 21:20:30 2017 +0100
@@ -9,15 +9,17 @@
 begin
 
 text \<open>
-  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.
+  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>
 
 
-subsection \<open>Pure Logic\<close>
+section \<open>HOL syntax within Pure\<close>
 
 class type
 default_sort type
@@ -26,10 +28,10 @@
 instance o :: type ..
 instance "fun" :: (type, type) type ..
 
+judgment Trueprop :: "o \<Rightarrow> prop"  ("_" 5)
 
-subsubsection \<open>Basic logical connectives\<close>
 
-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"
@@ -39,79 +41,48 @@
   where allI [intro]: "(\<And>x. P x) \<Longrightarrow> \<forall>x. P x"
     and allE [dest]: "\<forall>x. P x \<Longrightarrow> P a"
 
-
-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 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"
+lemma atomize_imp [atomize]: "(A \<Longrightarrow> B) \<equiv> Trueprop (A \<longrightarrow> B)"
+  by standard (fact impI, fact impE)
 
-theorem sym [sym]:
-  assumes "x = y"
-  shows "y = x"
-  using assms 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)
-
-theorem trans [trans]: "x = y \<Longrightarrow> y = z \<Longrightarrow> x = z"
-  by (rule subst)
-
-theorem iff1 [elim]: "A \<longleftrightarrow> B \<Longrightarrow> A \<Longrightarrow> B"
-  by (rule subst)
-
-theorem iff2 [elim]: "A \<longleftrightarrow> B \<Longrightarrow> B \<Longrightarrow> A"
-  by (rule subst) (rule sym)
+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  ("\<bottom>")
-  where "\<bottom> \<equiv> \<forall>A. A"
+definition False :: o
+  where "False \<equiv> \<forall>A. A"
 
-theorem falseE [elim]:
-  assumes "\<bottom>"
+lemma FalseE [elim]:
+  assumes "False"
   shows A
 proof -
-  from \<open>\<bottom>\<close> have "\<forall>A. A" by (simp only: false_def)
+  from \<open>False\<close> have "\<forall>A. A" by (simp only: False_def)
   then show A ..
 qed
 
 
-definition true :: o  ("\<top>")
-  where "\<top> \<equiv> \<bottom> \<longrightarrow> \<bottom>"
+definition True :: o
+  where "True \<equiv> False \<longrightarrow> False"
 
-theorem trueI [intro]: \<top>
-  unfolding true_def ..
+lemma TrueI [intro]: True
+  unfolding True_def ..
 
 
 definition not :: "o \<Rightarrow> o"  ("\<not> _" [40] 40)
-  where "not \<equiv> \<lambda>A. A \<longrightarrow> \<bottom>"
+  where "not \<equiv> \<lambda>A. A \<longrightarrow> False"
 
-abbreviation not_equal :: "'a \<Rightarrow> 'a \<Rightarrow> o"  (infixl "\<noteq>" 50)
-  where "x \<noteq> y \<equiv> \<not> (x = y)"
-
-theorem notI [intro]:
-  assumes "A \<Longrightarrow> \<bottom>"
+lemma notI [intro]:
+  assumes "A \<Longrightarrow> False"
   shows "\<not> A"
   using assms unfolding not_def ..
 
-theorem notE [elim]:
+lemma notE [elim]:
   assumes "\<not> A" and A
   shows B
 proof -
-  from \<open>\<not> A\<close> have "A \<longrightarrow> \<bottom>" by (simp only: not_def)
-  from this and \<open>A\<close> have "\<bottom>" ..
+  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
 
@@ -122,9 +93,9 @@
 
 
 definition conj :: "o \<Rightarrow> o \<Rightarrow> o"  (infixr "\<and>" 35)
-  where "conj \<equiv> \<lambda>A B. \<forall>C. (A \<longrightarrow> B \<longrightarrow> C) \<longrightarrow> C"
+  where "A \<and> B \<equiv> \<forall>C. (A \<longrightarrow> B \<longrightarrow> C) \<longrightarrow> C"
 
-theorem conjI [intro]:
+lemma conjI [intro]:
   assumes A and B
   shows "A \<and> B"
   unfolding conj_def
@@ -139,7 +110,7 @@
   qed
 qed
 
-theorem conjE [elim]:
+lemma conjE [elim]:
   assumes "A \<and> B"
   obtains A and B
 proof
@@ -168,9 +139,9 @@
 
 
 definition disj :: "o \<Rightarrow> o \<Rightarrow> o"  (infixr "\<or>" 30)
-  where "disj \<equiv> \<lambda>A B. \<forall>C. (A \<longrightarrow> C) \<longrightarrow> (B \<longrightarrow> C) \<longrightarrow> C"
+  where "A \<or> B \<equiv> \<forall>C. (A \<longrightarrow> C) \<longrightarrow> (B \<longrightarrow> C) \<longrightarrow> C"
 
-theorem disjI1 [intro]:
+lemma disjI1 [intro]:
   assumes A
   shows "A \<or> B"
   unfolding disj_def
@@ -184,7 +155,7 @@
   qed
 qed
 
-theorem disjI2 [intro]:
+lemma disjI2 [intro]:
   assumes B
   shows "A \<or> B"
   unfolding disj_def
@@ -200,7 +171,7 @@
   qed
 qed
 
-theorem disjE [elim]:
+lemma disjE [elim]:
   assumes "A \<or> B"
   obtains (a) A | (b) B
 proof -
@@ -223,7 +194,7 @@
 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"
 
-theorem exI [intro]: "P a \<Longrightarrow> \<exists>x. P x"
+lemma exI [intro]: "P a \<Longrightarrow> \<exists>x. P x"
   unfolding Ex_def
 proof
   fix C
@@ -236,7 +207,7 @@
   qed
 qed
 
-theorem exE [elim]:
+lemma exE [elim]:
   assumes "\<exists>x. P x"
   obtains (that) x where "P x"
 proof -
@@ -255,6 +226,47 @@
 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"
+
+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>
@@ -271,7 +283,7 @@
   proof
     assume A
     with * have "\<not> A" ..
-    from this and \<open>A\<close> show \<bottom> ..
+    from this and \<open>A\<close> show False ..
   qed
   with * show A ..
 qed
@@ -285,11 +297,11 @@
   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 \<bottom> by (rule iff_contradiction)
+  then show False by (rule iff_contradiction)
 qed
 
 
-subsection \<open>Classical logic\<close>
+subsection \<open>Characterization of Classical Logic\<close>
 
 text \<open>
   The subsequent rules of classical reasoning are all equivalent.
@@ -297,8 +309,10 @@
 
 locale classical =
   assumes classical: "(\<not> A \<Longrightarrow> A) \<Longrightarrow> A"
+  \<comment> \<open>predicate definition and hypothetical context\<close>
+begin
 
-theorem (in classical) Peirce's_Law: "((A \<longrightarrow> B) \<longrightarrow> A) \<longrightarrow> A"
+theorem Peirce's_Law: "((A \<longrightarrow> B) \<longrightarrow> A) \<longrightarrow> A"
 proof
   assume *: "(A \<longrightarrow> B) \<longrightarrow> A"
   show A
@@ -313,7 +327,7 @@
   qed
 qed
 
-theorem (in classical) double_negation:
+lemma double_negation:
   assumes "\<not> \<not> A"
   shows A
 proof (rule classical)
@@ -321,7 +335,7 @@
   with \<open>\<not> \<not> A\<close> show ?thesis by (rule contradiction)
 qed
 
-theorem (in classical) tertium_non_datur: "A \<or> \<not> A"
+lemma tertium_non_datur: "A \<or> \<not> A"
 proof (rule double_negation)
   show "\<not> \<not> (A \<or> \<not> A)"
   proof
@@ -329,14 +343,14 @@
     have "\<not> A"
     proof
       assume A then have "A \<or> \<not> A" ..
-      with \<open>\<not> (A \<or> \<not> A)\<close> show \<bottom> by (rule contradiction)
+      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 \<bottom> by (rule contradiction)
+    with \<open>\<not> (A \<or> \<not> A)\<close> show False by (rule contradiction)
   qed
 qed
 
-theorem (in classical) classical_cases:
+lemma classical_cases:
   obtains A | "\<not> A"
   using tertium_non_datur
 proof
@@ -347,14 +361,15 @@
   then show thesis ..
 qed
 
-lemma
-  assumes classical_cases: "\<And>A C. (A \<Longrightarrow> C) \<Longrightarrow> (\<not> A \<Longrightarrow> C) \<Longrightarrow> C"
-  shows "PROP classical"
+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 classical_cases)
+  proof (rule cases)
     assume A
     then show A .
   next
@@ -363,4 +378,124 @@
   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 classical} 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
+  Peirce's_Law
+  double_negation
+  tertium_non_datur
+  classical_cases
+
 end
diff -r 49549acbf025 -r 354bfbb27fbb src/HOL/Isar_Examples/document/root.bib
--- a/src/HOL/Isar_Examples/document/root.bib	Mon Jan 16 16:12:29 2017 +0100
+++ b/src/HOL/Isar_Examples/document/root.bib	Mon Jan 16 21:20:30 2017 +0100
@@ -4,6 +4,14 @@
 @string{Springer="Springer-Verlag"}
 @string{TUM="TU Munich"}
 
+@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"}
+
 @Book{Concrete-Math,
   author = 	 {R. L. Graham and D. E. Knuth and O. Patashnik},
   title = 	 {Concrete Mathematics},