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