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