# HG changeset patch
# User wenzelm
# Date 1478551243 -3600
# Node ID d072c8169c7caa4e1cee79cc360648569c071774
# Parent  6eff987ab7186701538c5be0a5354930c54093f5
simplified main proof;

diff -r 6eff987ab718 -r d072c8169c7c src/HOL/Proofs/ex/Hilbert_Classical.thy
--- a/src/HOL/Proofs/ex/Hilbert_Classical.thy	Mon Nov 07 21:13:41 2016 +0100
+++ b/src/HOL/Proofs/ex/Hilbert_Classical.thy	Mon Nov 07 21:40:43 2016 +0100
@@ -19,6 +19,86 @@
 
 theorem tertium_non_datur: "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 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 contradiction
+      qed
+      then show ?thesis ..
+    qed
+  qed
+qed
+
+
+subsection \<open>Old proof text\<close>
+
+theorem tertium_non_datur1: "A \<or> \<not> A"
+proof -
   let ?P = "\<lambda>x. (x \<longleftrightarrow> False) \<or> (x \<longleftrightarrow> True) \<and> A"
   let ?Q = "\<lambda>x. (x \<longleftrightarrow> False) \<and> A \<or> (x \<longleftrightarrow> True)"
 
@@ -93,14 +173,9 @@
 qed
 
 
-subsection \<open>Proof term of text\<close>
-
-prf tertium_non_datur
+subsection \<open>Old proof script\<close>
 
-
-subsection \<open>Proof script\<close>
-
-theorem tertium_non_datur': "A \<or> \<not> A"
+theorem tertium_non_datur2: "A \<or> \<not> A"
   apply (subgoal_tac
       "(((SOME x. x = False \<or> x = True \<and> A) = False) \<or>
       ((SOME x. x = False \<or> x = True \<and> A) = True) \<and> A) \<and>
@@ -152,8 +227,10 @@
   done
 
 
-subsection \<open>Proof term of script\<close>
+subsection \<open>Proof terms\<close>
 
-prf tertium_non_datur'
+prf tertium_non_datur
+prf tertium_non_datur1
+prf tertium_non_datur2
 
 end