# HG changeset patch
# User wenzelm
# Date 1478549621 -3600
# Node ID 6eff987ab7186701538c5be0a5354930c54093f5
# Parent  c2191352e908a40f7213d4bcc1089e4433f3a592
misc tuning and modernization;

diff -r c2191352e908 -r 6eff987ab718 src/HOL/Proofs/ex/Hilbert_Classical.thy
--- a/src/HOL/Proofs/ex/Hilbert_Classical.thy	Mon Nov 07 20:05:30 2016 +0100
+++ b/src/HOL/Proofs/ex/Hilbert_Classical.thy	Mon Nov 07 21:13:41 2016 +0100
@@ -1,11 +1,12 @@
 (*  Title:      HOL/Proofs/ex/Hilbert_Classical.thy
-    Author:     Stefan Berghofer and Markus Wenzel, TU Muenchen
+    Author:     Stefan Berghofer
+    Author:     Makarius Wenzel
 *)
 
 section \<open>Hilbert's choice and classical logic\<close>
 
 theory Hilbert_Classical
-imports Main
+  imports Main
 begin
 
 text \<open>
@@ -16,79 +17,77 @@
 
 subsection \<open>Proof text\<close>
 
-theorem tnd: "A \<or> \<not> A"
+theorem tertium_non_datur: "A \<or> \<not> A"
 proof -
-  let ?P = "\<lambda>X. X = False \<or> X = True \<and> A"
-  let ?Q = "\<lambda>X. X = False \<and> A \<or> X = True"
+  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)"
 
   have a: "?P (Eps ?P)"
   proof (rule someI)
-    have "False = False" ..
-    thus "?P False" ..
+    show "?P False" using refl ..
   qed
   have b: "?Q (Eps ?Q)"
   proof (rule someI)
-    have "True = True" ..
-    thus "?Q True" ..
+    show "?Q True" using refl ..
   qed
 
   from a show ?thesis
   proof
-    assume "Eps ?P = True \<and> A"
-    hence A ..
-    thus ?thesis ..
+    assume "(Eps ?P \<longleftrightarrow> True) \<and> A"
+    then have A ..
+    then show ?thesis ..
   next
-    assume P: "Eps ?P = False"
+    assume P: "Eps ?P \<longleftrightarrow> False"
     from b show ?thesis
     proof
-      assume "Eps ?Q = False \<and> A"
-      hence A ..
-      thus ?thesis ..
+      assume "(Eps ?Q \<longleftrightarrow> False) \<and> A"
+      then have A ..
+      then show ?thesis ..
     next
-      assume Q: "Eps ?Q = True"
+      assume Q: "Eps ?Q \<longleftrightarrow> True"
       have neq: "?P \<noteq> ?Q"
       proof
         assume "?P = ?Q"
-        hence "Eps ?P = Eps ?Q" by (rule arg_cong)
+        then have "Eps ?P \<longleftrightarrow> Eps ?Q" by (rule arg_cong)
         also note P
         also note Q
         finally show False by (rule False_neq_True)
       qed
       have "\<not> A"
       proof
-        assume a: A
+        assume A
         have "?P = ?Q"
         proof (rule ext)
-          fix x show "?P x = ?Q x"
+          show "?P x \<longleftrightarrow> ?Q x" for x
           proof
             assume "?P x"
-            thus "?Q x"
+            then show "?Q x"
             proof
-              assume "x = False"
-              from this and a have "x = False \<and> A" ..
-              thus "?Q x" ..
+              assume "x \<longleftrightarrow> False"
+              from this and \<open>A\<close> have "(x \<longleftrightarrow> False) \<and> A" ..
+              then show ?thesis ..
             next
-              assume "x = True \<and> A"
-              hence "x = True" ..
-              thus "?Q x" ..
+              assume "(x \<longleftrightarrow> True) \<and> A"
+              then have "x \<longleftrightarrow> True" ..
+              then show ?thesis ..
             qed
           next
             assume "?Q x"
-            thus "?P x"
+            then show "?P x"
             proof
-              assume "x = False \<and> A"
-              hence "x = False" ..
-              thus "?P x" ..
+              assume "(x \<longleftrightarrow> False) \<and> A"
+              then have "x \<longleftrightarrow> False" ..
+              then show ?thesis ..
             next
-              assume "x = True"
-              from this and a have "x = True \<and> A" ..
-              thus "?P x" ..
+              assume "x \<longleftrightarrow> True"
+              from this and \<open>A\<close> have "(x \<longleftrightarrow> True) \<and> A" ..
+              then show ?thesis ..
             qed
           qed
         qed
         with neq show False by contradiction
       qed
-      thus ?thesis ..
+      then show ?thesis ..
     qed
   qed
 qed
@@ -96,57 +95,57 @@
 
 subsection \<open>Proof term of text\<close>
 
-prf tnd
+prf tertium_non_datur
 
 
 subsection \<open>Proof script\<close>
 
-theorem tnd': "A \<or> \<not> A"
+theorem tertium_non_datur': "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) = False) \<or>
       ((SOME x. x = False \<or> x = True \<and> A) = True) \<and> A) \<and>
-     (((SOME x. x = False \<and> A \<or> x = True) = False) \<and> A \<or>
+      (((SOME x. x = False \<and> A \<or> x = True) = False) \<and> A \<or>
       ((SOME x. x = False \<and> A \<or> x = True) = True))")
-  prefer 2
-  apply (rule conjI)
-  apply (rule someI)
-  apply (rule disjI1)
-  apply (rule refl)
-  apply (rule someI)
-  apply (rule disjI2)
-  apply (rule refl)
+   prefer 2
+   apply (rule conjI)
+    apply (rule someI)
+    apply (rule disjI1)
+    apply (rule refl)
+   apply (rule someI)
+   apply (rule disjI2)
+   apply (rule refl)
   apply (erule conjE)
   apply (erule disjE)
-  apply (erule disjE)
-  apply (erule conjE)
-  apply (erule disjI1)
-  prefer 2
-  apply (erule conjE)
-  apply (erule disjI1)
+   apply (erule disjE)
+    apply (erule conjE)
+    apply (erule disjI1)
+   prefer 2
+   apply (erule conjE)
+   apply (erule disjI1)
   apply (subgoal_tac
-    "(\<lambda>x. (x = False) \<or> (x = True) \<and> A) \<noteq>
-     (\<lambda>x. (x = False) \<and> A \<or> (x = True))")
-  prefer 2
-  apply (rule notI)
-  apply (drule_tac f = "\<lambda>y. SOME x. y x" in arg_cong)
-  apply (drule trans, assumption)
-  apply (drule sym)
-  apply (drule trans, assumption)
-  apply (erule False_neq_True)
+      "(\<lambda>x. (x = False) \<or> (x = True) \<and> A) \<noteq>
+      (\<lambda>x. (x = False) \<and> A \<or> (x = True))")
+   prefer 2
+   apply (rule notI)
+   apply (drule_tac f = "\<lambda>y. SOME x. y x" in arg_cong)
+   apply (drule trans, assumption)
+   apply (drule sym)
+   apply (drule trans, assumption)
+   apply (erule False_neq_True)
   apply (rule disjI2)
   apply (rule notI)
   apply (erule notE)
   apply (rule ext)
   apply (rule iffI)
+   apply (erule disjE)
+    apply (rule disjI1)
+    apply (erule conjI)
+    apply assumption
+   apply (erule conjE)
+   apply (erule disjI2)
   apply (erule disjE)
-  apply (rule disjI1)
-  apply (erule conjI)
-  apply assumption
-  apply (erule conjE)
-  apply (erule disjI2)
-  apply (erule disjE)
-  apply (erule conjE)
-  apply (erule disjI1)
+   apply (erule conjE)
+   apply (erule disjI1)
   apply (rule disjI2)
   apply (erule conjI)
   apply assumption
@@ -155,6 +154,6 @@
 
 subsection \<open>Proof term of script\<close>
 
-prf tnd'
+prf tertium_non_datur'
 
 end