author | haftmann |
Wed, 21 Dec 2016 21:26:26 +0100 | |
changeset 64633 | 5ebcf6c525f1 |
parent 64474 | d072c8169c7c |
permissions | -rw-r--r-- |
39157
b98909faaea8
more explicit HOL-Proofs sessions, including former ex/Hilbert_Classical.thy which works in parallel mode without the antiquotation option "margin" (which is still critical);
wenzelm
parents:
32960
diff
changeset
|
1 |
(* Title: HOL/Proofs/ex/Hilbert_Classical.thy |
64473 | 2 |
Author: Stefan Berghofer |
3 |
Author: Makarius Wenzel |
|
11584
c8e98b9498b4
derive tertium-non-datur by means of Hilbert's choice operator;
wenzelm
parents:
diff
changeset
|
4 |
*) |
c8e98b9498b4
derive tertium-non-datur by means of Hilbert's choice operator;
wenzelm
parents:
diff
changeset
|
5 |
|
61986 | 6 |
section \<open>Hilbert's choice and classical logic\<close> |
11584
c8e98b9498b4
derive tertium-non-datur by means of Hilbert's choice operator;
wenzelm
parents:
diff
changeset
|
7 |
|
39157
b98909faaea8
more explicit HOL-Proofs sessions, including former ex/Hilbert_Classical.thy which works in parallel mode without the antiquotation option "margin" (which is still critical);
wenzelm
parents:
32960
diff
changeset
|
8 |
theory Hilbert_Classical |
64473 | 9 |
imports Main |
39157
b98909faaea8
more explicit HOL-Proofs sessions, including former ex/Hilbert_Classical.thy which works in parallel mode without the antiquotation option "margin" (which is still critical);
wenzelm
parents:
32960
diff
changeset
|
10 |
begin |
11584
c8e98b9498b4
derive tertium-non-datur by means of Hilbert's choice operator;
wenzelm
parents:
diff
changeset
|
11 |
|
61986 | 12 |
text \<open> |
11584
c8e98b9498b4
derive tertium-non-datur by means of Hilbert's choice operator;
wenzelm
parents:
diff
changeset
|
13 |
Derivation of the classical law of tertium-non-datur by means of |
c8e98b9498b4
derive tertium-non-datur by means of Hilbert's choice operator;
wenzelm
parents:
diff
changeset
|
14 |
Hilbert's choice operator (due to M. J. Beeson and J. Harrison). |
61986 | 15 |
\<close> |
11584
c8e98b9498b4
derive tertium-non-datur by means of Hilbert's choice operator;
wenzelm
parents:
diff
changeset
|
16 |
|
c8e98b9498b4
derive tertium-non-datur by means of Hilbert's choice operator;
wenzelm
parents:
diff
changeset
|
17 |
|
61986 | 18 |
subsection \<open>Proof text\<close> |
11584
c8e98b9498b4
derive tertium-non-datur by means of Hilbert's choice operator;
wenzelm
parents:
diff
changeset
|
19 |
|
64473 | 20 |
theorem tertium_non_datur: "A \<or> \<not> A" |
11584
c8e98b9498b4
derive tertium-non-datur by means of Hilbert's choice operator;
wenzelm
parents:
diff
changeset
|
21 |
proof - |
64474 | 22 |
let ?P = "\<lambda>x. (A \<and> x) \<or> \<not> x" |
23 |
let ?Q = "\<lambda>x. (A \<and> \<not> x) \<or> x" |
|
24 |
||
25 |
have a: "?P (Eps ?P)" |
|
26 |
proof (rule someI) |
|
27 |
have "\<not> False" .. |
|
28 |
then show "?P False" .. |
|
29 |
qed |
|
30 |
have b: "?Q (Eps ?Q)" |
|
31 |
proof (rule someI) |
|
32 |
have True .. |
|
33 |
then show "?Q True" .. |
|
34 |
qed |
|
35 |
||
36 |
from a show ?thesis |
|
37 |
proof |
|
38 |
assume "A \<and> Eps ?P" |
|
39 |
then have A .. |
|
40 |
then show ?thesis .. |
|
41 |
next |
|
42 |
assume "\<not> Eps ?P" |
|
43 |
from b show ?thesis |
|
44 |
proof |
|
45 |
assume "A \<and> \<not> Eps ?Q" |
|
46 |
then have A .. |
|
47 |
then show ?thesis .. |
|
48 |
next |
|
49 |
assume "Eps ?Q" |
|
50 |
have neq: "?P \<noteq> ?Q" |
|
51 |
proof |
|
52 |
assume "?P = ?Q" |
|
53 |
then have "Eps ?P \<longleftrightarrow> Eps ?Q" by (rule arg_cong) |
|
54 |
also note \<open>Eps ?Q\<close> |
|
55 |
finally have "Eps ?P" . |
|
56 |
with \<open>\<not> Eps ?P\<close> show False by contradiction |
|
57 |
qed |
|
58 |
have "\<not> A" |
|
59 |
proof |
|
60 |
assume A |
|
61 |
have "?P = ?Q" |
|
62 |
proof (rule ext) |
|
63 |
show "?P x \<longleftrightarrow> ?Q x" for x |
|
64 |
proof |
|
65 |
assume "?P x" |
|
66 |
then show "?Q x" |
|
67 |
proof |
|
68 |
assume "\<not> x" |
|
69 |
with \<open>A\<close> have "A \<and> \<not> x" .. |
|
70 |
then show ?thesis .. |
|
71 |
next |
|
72 |
assume "A \<and> x" |
|
73 |
then have x .. |
|
74 |
then show ?thesis .. |
|
75 |
qed |
|
76 |
next |
|
77 |
assume "?Q x" |
|
78 |
then show "?P x" |
|
79 |
proof |
|
80 |
assume "A \<and> \<not> x" |
|
81 |
then have "\<not> x" .. |
|
82 |
then show ?thesis .. |
|
83 |
next |
|
84 |
assume x |
|
85 |
with \<open>A\<close> have "A \<and> x" .. |
|
86 |
then show ?thesis .. |
|
87 |
qed |
|
88 |
qed |
|
89 |
qed |
|
90 |
with neq show False by contradiction |
|
91 |
qed |
|
92 |
then show ?thesis .. |
|
93 |
qed |
|
94 |
qed |
|
95 |
qed |
|
96 |
||
97 |
||
98 |
subsection \<open>Old proof text\<close> |
|
99 |
||
100 |
theorem tertium_non_datur1: "A \<or> \<not> A" |
|
101 |
proof - |
|
64473 | 102 |
let ?P = "\<lambda>x. (x \<longleftrightarrow> False) \<or> (x \<longleftrightarrow> True) \<and> A" |
103 |
let ?Q = "\<lambda>x. (x \<longleftrightarrow> False) \<and> A \<or> (x \<longleftrightarrow> True)" |
|
11584
c8e98b9498b4
derive tertium-non-datur by means of Hilbert's choice operator;
wenzelm
parents:
diff
changeset
|
104 |
|
11590 | 105 |
have a: "?P (Eps ?P)" |
11584
c8e98b9498b4
derive tertium-non-datur by means of Hilbert's choice operator;
wenzelm
parents:
diff
changeset
|
106 |
proof (rule someI) |
64473 | 107 |
show "?P False" using refl .. |
11584
c8e98b9498b4
derive tertium-non-datur by means of Hilbert's choice operator;
wenzelm
parents:
diff
changeset
|
108 |
qed |
11590 | 109 |
have b: "?Q (Eps ?Q)" |
11584
c8e98b9498b4
derive tertium-non-datur by means of Hilbert's choice operator;
wenzelm
parents:
diff
changeset
|
110 |
proof (rule someI) |
64473 | 111 |
show "?Q True" using refl .. |
11584
c8e98b9498b4
derive tertium-non-datur by means of Hilbert's choice operator;
wenzelm
parents:
diff
changeset
|
112 |
qed |
c8e98b9498b4
derive tertium-non-datur by means of Hilbert's choice operator;
wenzelm
parents:
diff
changeset
|
113 |
|
c8e98b9498b4
derive tertium-non-datur by means of Hilbert's choice operator;
wenzelm
parents:
diff
changeset
|
114 |
from a show ?thesis |
c8e98b9498b4
derive tertium-non-datur by means of Hilbert's choice operator;
wenzelm
parents:
diff
changeset
|
115 |
proof |
64473 | 116 |
assume "(Eps ?P \<longleftrightarrow> True) \<and> A" |
117 |
then have A .. |
|
118 |
then show ?thesis .. |
|
11590 | 119 |
next |
64473 | 120 |
assume P: "Eps ?P \<longleftrightarrow> False" |
11584
c8e98b9498b4
derive tertium-non-datur by means of Hilbert's choice operator;
wenzelm
parents:
diff
changeset
|
121 |
from b show ?thesis |
c8e98b9498b4
derive tertium-non-datur by means of Hilbert's choice operator;
wenzelm
parents:
diff
changeset
|
122 |
proof |
64473 | 123 |
assume "(Eps ?Q \<longleftrightarrow> False) \<and> A" |
124 |
then have A .. |
|
125 |
then show ?thesis .. |
|
11584
c8e98b9498b4
derive tertium-non-datur by means of Hilbert's choice operator;
wenzelm
parents:
diff
changeset
|
126 |
next |
64473 | 127 |
assume Q: "Eps ?Q \<longleftrightarrow> True" |
11590 | 128 |
have neq: "?P \<noteq> ?Q" |
11584
c8e98b9498b4
derive tertium-non-datur by means of Hilbert's choice operator;
wenzelm
parents:
diff
changeset
|
129 |
proof |
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
26828
diff
changeset
|
130 |
assume "?P = ?Q" |
64473 | 131 |
then have "Eps ?P \<longleftrightarrow> Eps ?Q" by (rule arg_cong) |
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
26828
diff
changeset
|
132 |
also note P |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
26828
diff
changeset
|
133 |
also note Q |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
26828
diff
changeset
|
134 |
finally show False by (rule False_neq_True) |
11584
c8e98b9498b4
derive tertium-non-datur by means of Hilbert's choice operator;
wenzelm
parents:
diff
changeset
|
135 |
qed |
11590 | 136 |
have "\<not> A" |
11584
c8e98b9498b4
derive tertium-non-datur by means of Hilbert's choice operator;
wenzelm
parents:
diff
changeset
|
137 |
proof |
64473 | 138 |
assume A |
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
26828
diff
changeset
|
139 |
have "?P = ?Q" |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
26828
diff
changeset
|
140 |
proof (rule ext) |
64473 | 141 |
show "?P x \<longleftrightarrow> ?Q x" for x |
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
26828
diff
changeset
|
142 |
proof |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
26828
diff
changeset
|
143 |
assume "?P x" |
64473 | 144 |
then show "?Q x" |
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
26828
diff
changeset
|
145 |
proof |
64473 | 146 |
assume "x \<longleftrightarrow> False" |
147 |
from this and \<open>A\<close> have "(x \<longleftrightarrow> False) \<and> A" .. |
|
148 |
then show ?thesis .. |
|
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
26828
diff
changeset
|
149 |
next |
64473 | 150 |
assume "(x \<longleftrightarrow> True) \<and> A" |
151 |
then have "x \<longleftrightarrow> True" .. |
|
152 |
then show ?thesis .. |
|
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
26828
diff
changeset
|
153 |
qed |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
26828
diff
changeset
|
154 |
next |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
26828
diff
changeset
|
155 |
assume "?Q x" |
64473 | 156 |
then show "?P x" |
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
26828
diff
changeset
|
157 |
proof |
64473 | 158 |
assume "(x \<longleftrightarrow> False) \<and> A" |
159 |
then have "x \<longleftrightarrow> False" .. |
|
160 |
then show ?thesis .. |
|
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
26828
diff
changeset
|
161 |
next |
64473 | 162 |
assume "x \<longleftrightarrow> True" |
163 |
from this and \<open>A\<close> have "(x \<longleftrightarrow> True) \<and> A" .. |
|
164 |
then show ?thesis .. |
|
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
26828
diff
changeset
|
165 |
qed |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
26828
diff
changeset
|
166 |
qed |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
26828
diff
changeset
|
167 |
qed |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
26828
diff
changeset
|
168 |
with neq show False by contradiction |
11584
c8e98b9498b4
derive tertium-non-datur by means of Hilbert's choice operator;
wenzelm
parents:
diff
changeset
|
169 |
qed |
64473 | 170 |
then show ?thesis .. |
11584
c8e98b9498b4
derive tertium-non-datur by means of Hilbert's choice operator;
wenzelm
parents:
diff
changeset
|
171 |
qed |
c8e98b9498b4
derive tertium-non-datur by means of Hilbert's choice operator;
wenzelm
parents:
diff
changeset
|
172 |
qed |
c8e98b9498b4
derive tertium-non-datur by means of Hilbert's choice operator;
wenzelm
parents:
diff
changeset
|
173 |
qed |
c8e98b9498b4
derive tertium-non-datur by means of Hilbert's choice operator;
wenzelm
parents:
diff
changeset
|
174 |
|
c8e98b9498b4
derive tertium-non-datur by means of Hilbert's choice operator;
wenzelm
parents:
diff
changeset
|
175 |
|
64474 | 176 |
subsection \<open>Old proof script\<close> |
11591 | 177 |
|
64474 | 178 |
theorem tertium_non_datur2: "A \<or> \<not> A" |
11584
c8e98b9498b4
derive tertium-non-datur by means of Hilbert's choice operator;
wenzelm
parents:
diff
changeset
|
179 |
apply (subgoal_tac |
64473 | 180 |
"(((SOME x. x = False \<or> x = True \<and> A) = False) \<or> |
11590 | 181 |
((SOME x. x = False \<or> x = True \<and> A) = True) \<and> A) \<and> |
64473 | 182 |
(((SOME x. x = False \<and> A \<or> x = True) = False) \<and> A \<or> |
11590 | 183 |
((SOME x. x = False \<and> A \<or> x = True) = True))") |
64473 | 184 |
prefer 2 |
185 |
apply (rule conjI) |
|
186 |
apply (rule someI) |
|
187 |
apply (rule disjI1) |
|
188 |
apply (rule refl) |
|
189 |
apply (rule someI) |
|
190 |
apply (rule disjI2) |
|
191 |
apply (rule refl) |
|
11584
c8e98b9498b4
derive tertium-non-datur by means of Hilbert's choice operator;
wenzelm
parents:
diff
changeset
|
192 |
apply (erule conjE) |
c8e98b9498b4
derive tertium-non-datur by means of Hilbert's choice operator;
wenzelm
parents:
diff
changeset
|
193 |
apply (erule disjE) |
64473 | 194 |
apply (erule disjE) |
195 |
apply (erule conjE) |
|
196 |
apply (erule disjI1) |
|
197 |
prefer 2 |
|
198 |
apply (erule conjE) |
|
199 |
apply (erule disjI1) |
|
11584
c8e98b9498b4
derive tertium-non-datur by means of Hilbert's choice operator;
wenzelm
parents:
diff
changeset
|
200 |
apply (subgoal_tac |
64473 | 201 |
"(\<lambda>x. (x = False) \<or> (x = True) \<and> A) \<noteq> |
202 |
(\<lambda>x. (x = False) \<and> A \<or> (x = True))") |
|
203 |
prefer 2 |
|
204 |
apply (rule notI) |
|
205 |
apply (drule_tac f = "\<lambda>y. SOME x. y x" in arg_cong) |
|
206 |
apply (drule trans, assumption) |
|
207 |
apply (drule sym) |
|
208 |
apply (drule trans, assumption) |
|
209 |
apply (erule False_neq_True) |
|
11584
c8e98b9498b4
derive tertium-non-datur by means of Hilbert's choice operator;
wenzelm
parents:
diff
changeset
|
210 |
apply (rule disjI2) |
c8e98b9498b4
derive tertium-non-datur by means of Hilbert's choice operator;
wenzelm
parents:
diff
changeset
|
211 |
apply (rule notI) |
c8e98b9498b4
derive tertium-non-datur by means of Hilbert's choice operator;
wenzelm
parents:
diff
changeset
|
212 |
apply (erule notE) |
c8e98b9498b4
derive tertium-non-datur by means of Hilbert's choice operator;
wenzelm
parents:
diff
changeset
|
213 |
apply (rule ext) |
c8e98b9498b4
derive tertium-non-datur by means of Hilbert's choice operator;
wenzelm
parents:
diff
changeset
|
214 |
apply (rule iffI) |
64473 | 215 |
apply (erule disjE) |
216 |
apply (rule disjI1) |
|
217 |
apply (erule conjI) |
|
218 |
apply assumption |
|
219 |
apply (erule conjE) |
|
220 |
apply (erule disjI2) |
|
11584
c8e98b9498b4
derive tertium-non-datur by means of Hilbert's choice operator;
wenzelm
parents:
diff
changeset
|
221 |
apply (erule disjE) |
64473 | 222 |
apply (erule conjE) |
223 |
apply (erule disjI1) |
|
11584
c8e98b9498b4
derive tertium-non-datur by means of Hilbert's choice operator;
wenzelm
parents:
diff
changeset
|
224 |
apply (rule disjI2) |
c8e98b9498b4
derive tertium-non-datur by means of Hilbert's choice operator;
wenzelm
parents:
diff
changeset
|
225 |
apply (erule conjI) |
c8e98b9498b4
derive tertium-non-datur by means of Hilbert's choice operator;
wenzelm
parents:
diff
changeset
|
226 |
apply assumption |
c8e98b9498b4
derive tertium-non-datur by means of Hilbert's choice operator;
wenzelm
parents:
diff
changeset
|
227 |
done |
c8e98b9498b4
derive tertium-non-datur by means of Hilbert's choice operator;
wenzelm
parents:
diff
changeset
|
228 |
|
c8e98b9498b4
derive tertium-non-datur by means of Hilbert's choice operator;
wenzelm
parents:
diff
changeset
|
229 |
|
64474 | 230 |
subsection \<open>Proof terms\<close> |
11584
c8e98b9498b4
derive tertium-non-datur by means of Hilbert's choice operator;
wenzelm
parents:
diff
changeset
|
231 |
|
64474 | 232 |
prf tertium_non_datur |
233 |
prf tertium_non_datur1 |
|
234 |
prf tertium_non_datur2 |
|
11584
c8e98b9498b4
derive tertium-non-datur by means of Hilbert's choice operator;
wenzelm
parents:
diff
changeset
|
235 |
|
c8e98b9498b4
derive tertium-non-datur by means of Hilbert's choice operator;
wenzelm
parents:
diff
changeset
|
236 |
end |