author wenzelm Mon, 16 Jan 2017 21:33:09 +0100 changeset 64908 f94ad67a0f6e parent 64907 354bfbb27fbb child 64909 8007f10195af
clarified classical rules;
```--- a/src/HOL/Isar_Examples/Higher_Order_Logic.thy	Mon Jan 16 21:20:30 2017 +0100
+++ b/src/HOL/Isar_Examples/Higher_Order_Logic.thy	Mon Jan 16 21:33:09 2017 +0100
@@ -312,27 +312,21 @@
\<comment> \<open>predicate definition and hypothetical context\<close>
begin

-theorem 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
+  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)
assume "\<not> A"
-  with \<open>\<not> \<not> A\<close> show ?thesis by (rule contradiction)
+  with \<open>\<not> \<not> A\<close> show False by (rule contradiction)
qed

lemma tertium_non_datur: "A \<or> \<not> A"
@@ -379,6 +373,29 @@
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"
@@ -493,9 +510,10 @@
qed

thm classical
-  Peirce's_Law