# HG changeset patch
# User wenzelm
# Date 1001598108 -7200
# Node ID c8e98b9498b46c81dbe6035ebfc677d439b7546b
# Parent  bebeb3b9e88e0d9e1146cf4498665457cc2da201
derive tertium-non-datur by means of Hilbert's choice operator;

diff -r bebeb3b9e88e -r c8e98b9498b4 src/HOL/ex/Hilbert_Classical.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/ex/Hilbert_Classical.thy	Thu Sep 27 15:41:48 2001 +0200
@@ -0,0 +1,168 @@
+(*  Title:      HOL/ex/Hilbert_Classical.thy
+    ID:         $Id$
+    Author:     Stefan Berghofer and Markus Wenzel, TU Muenchen
+    License:    GPL (GNU GENERAL PUBLIC LICENSE)
+*)
+
+header {* Hilbert's choice and classical logic *}
+
+theory Hilbert_Classical = Main:
+
+text {*
+  Derivation of the classical law of tertium-non-datur by means of
+  Hilbert's choice operator (due to M. J. Beeson and J. Harrison).
+*}
+
+
+subsection {* Proof text *}
+
+theorem tnd: "P \<or> \<not> P"
+proof -
+  let ?A = "\<lambda>x. x = False \<or> x = True \<and> P"
+  let ?B = "\<lambda>x. x = False \<and> P \<or> x = True"
+  let ?f = "\<lambda>R. SOME y. R y"
+
+  have a: "?A (?f ?A)"
+  proof (rule someI)
+    have "False = False" ..
+    thus "?A False" ..
+  qed
+  have b: "?B (?f ?B)"
+  proof (rule someI)
+    have "True = True" ..
+    thus "?B True" ..
+  qed
+
+  from a show ?thesis
+  proof
+    assume fa: "?f ?A = False"
+    from b show ?thesis
+    proof
+      assume "?f ?B = False \<and> P"
+      hence P ..
+      thus ?thesis ..
+    next
+      assume fb: "?f ?B = True"
+      have neq: "?A \<noteq> ?B"
+      proof
+	assume "?A = ?B" hence eq: "?f ?A = ?f ?B" by (rule arg_cong)
+	from fa have "False = ?f ?A" ..
+	also note eq
+	also note fb
+	finally have "False = True" .
+	thus False by (rule False_neq_True)
+      qed
+      have "\<not> P"
+      proof
+	assume p: P
+	have "?A = ?B"
+	proof
+	  fix x
+	  show "?A x = ?B x"
+	  proof
+	    assume "?A x"
+	    thus "?B x"
+	    proof
+	      assume "x = False"
+	      from this and p
+	      have "x = False \<and> P" ..
+	      thus "?B x" ..
+	    next
+	      assume "x = True \<and> P"
+	      hence "x = True" ..
+	      thus "?B x" ..
+	    qed
+	  next
+	    assume "?B x"
+	    thus "?A x"
+	    proof
+	      assume "x = False \<and> P"
+	      hence "x = False" ..
+	      thus "?A x" ..
+	    next
+	      assume "x = True"
+	      from this and p
+	      have "x = True \<and> P" ..
+	      thus "?A x" ..
+	    qed
+	  qed
+	qed
+	with neq show False by contradiction
+      qed
+      thus ?thesis ..
+    qed
+  next
+    assume "?f ?A = True \<and> P" hence P ..
+    thus ?thesis ..
+  qed
+qed
+
+
+subsection {* Proof script *}
+
+theorem tnd': "P \<or> \<not> P"
+  apply (subgoal_tac
+    "(((SOME x. x = False \<or> x = True \<and> P) = False) \<or>
+      ((SOME x. x = False \<or> x = True \<and> P) = True) \<and> P) \<and>
+     (((SOME x. x = False \<and> P \<or> x = True) = False) \<and> P \<or>
+      ((SOME x. x = False \<and> P \<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)
+  apply (erule conjE)
+  apply (erule disjE)
+  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> P) \<noteq>
+     (\<lambda>x. (x = False) \<and> P \<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 (erule conjE)
+  apply (erule disjI1)
+  apply (rule disjI2)
+  apply (erule conjI)
+  apply assumption
+  done
+
+
+subsection {* Proof term of text *}
+
+text {*
+  @{prf [display] tnd}
+*}
+
+
+subsection {* Proof term of script *}
+
+text {*
+  @{prf [display] tnd'}
+*}
+
+end