--- 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
+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)
+proof (rule classical_contradiction)
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
+ classical_contradiction
double_negation
tertium_non_datur
classical_cases
+ Peirce's_Law
end