| author | wenzelm |
| Thu, 27 Sep 2001 16:43:46 +0200 | |
| changeset 11591 | 4b171ad4ff65 |
| parent 11590 | 14ae6a86813d |
| child 11635 | fd242f857508 |
| permissions | -rw-r--r-- |
1 (* Title: HOL/ex/Hilbert_Classical.thy
2 ID: $Id$
3 Author: Stefan Berghofer and Markus Wenzel, TU Muenchen
4 License: GPL (GNU GENERAL PUBLIC LICENSE)
5 *)
7 header {* Hilbert's choice and classical logic *}
9 theory Hilbert_Classical = Main:
11 text {*
12 Derivation of the classical law of tertium-non-datur by means of
13 Hilbert's choice operator (due to M. J. Beeson and J. Harrison).
14 *}
17 subsection {* Proof text *}
19 theorem tnd: "A \<or> \<not> A"
20 proof -
21 let ?P = "\<lambda>X. X = False \<or> X = True \<and> A"
22 let ?Q = "\<lambda>X. X = False \<and> A \<or> X = True"
24 have a: "?P (Eps ?P)"
25 proof (rule someI)
26 have "False = False" ..
27 thus "?P False" ..
28 qed
29 have b: "?Q (Eps ?Q)"
30 proof (rule someI)
31 have "True = True" ..
32 thus "?Q True" ..
33 qed
35 from a show ?thesis
36 proof
37 assume "Eps ?P = True \<and> A"
38 hence A ..
39 thus ?thesis ..
40 next
41 assume P: "Eps ?P = False"
42 from b show ?thesis
43 proof
44 assume "Eps ?Q = False \<and> A"
45 hence A ..
46 thus ?thesis ..
47 next
48 assume Q: "Eps ?Q = True"
49 have neq: "?P \<noteq> ?Q"
50 proof
51 assume "?P = ?Q"
52 hence "Eps ?P = Eps ?Q" by (rule arg_cong)
53 also note P
54 also note Q
55 finally have "False = True" .
56 thus False by (rule False_neq_True)
57 qed
58 have "\<not> A"
59 proof
60 assume a: A
61 have "?P = ?Q"
62 proof
63 fix x show "?P x = ?Q x"
64 proof
65 assume "?P x"
66 thus "?Q x"
67 proof
68 assume "x = False"
69 from this and a have "x = False \<and> A" ..
70 thus "?Q x" ..
71 next
72 assume "x = True \<and> A"
73 hence "x = True" ..
74 thus "?Q x" ..
75 qed
76 next
77 assume "?Q x"
78 thus "?P x"
79 proof
80 assume "x = False \<and> A"
81 hence "x = False" ..
82 thus "?P x" ..
83 next
84 assume "x = True"
85 from this and a have "x = True \<and> A" ..
86 thus "?P x" ..
87 qed
88 qed
89 qed
90 with neq show False by contradiction
91 qed
92 thus ?thesis ..
93 qed
94 qed
95 qed
98 subsection {* Proof term of text *}
100 text {*
101 {\small @{prf [display, margin = 80] tnd}}
102 *}
105 subsection {* Proof script *}
107 theorem tnd': "A \<or> \<not> A"
108 apply (subgoal_tac
109 "(((SOME x. x = False \<or> x = True \<and> A) = False) \<or>
110 ((SOME x. x = False \<or> x = True \<and> A) = True) \<and> A) \<and>
111 (((SOME x. x = False \<and> A \<or> x = True) = False) \<and> A \<or>
112 ((SOME x. x = False \<and> A \<or> x = True) = True))")
113 prefer 2
114 apply (rule conjI)
115 apply (rule someI)
116 apply (rule disjI1)
117 apply (rule refl)
118 apply (rule someI)
119 apply (rule disjI2)
120 apply (rule refl)
121 apply (erule conjE)
122 apply (erule disjE)
123 apply (erule disjE)
124 apply (erule conjE)
125 apply (erule disjI1)
126 prefer 2
127 apply (erule conjE)
128 apply (erule disjI1)
129 apply (subgoal_tac
130 "(\<lambda>x. (x = False) \<or> (x = True) \<and> A) \<noteq>
131 (\<lambda>x. (x = False) \<and> A \<or> (x = True))")
132 prefer 2
133 apply (rule notI)
134 apply (drule_tac f = "\<lambda>y. SOME x. y x" in arg_cong)
135 apply (drule trans, assumption)
136 apply (drule sym)
137 apply (drule trans, assumption)
138 apply (erule False_neq_True)
139 apply (rule disjI2)
140 apply (rule notI)
141 apply (erule notE)
142 apply (rule ext)
143 apply (rule iffI)
144 apply (erule disjE)
145 apply (rule disjI1)
146 apply (erule conjI)
147 apply assumption
148 apply (erule conjE)
149 apply (erule disjI2)
150 apply (erule disjE)
151 apply (erule conjE)
152 apply (erule disjI1)
153 apply (rule disjI2)
154 apply (erule conjI)
155 apply assumption
156 done
159 subsection {* Proof term of script *}
161 text {*
162 {\small @{prf [display, margin = 80] tnd'}}
163 *}
165 end