author | wenzelm |
Thu, 27 Sep 2001 16:43:46 +0200 | |
changeset 11591 | 4b171ad4ff65 |
parent 11590 | 14ae6a86813d |
child 11635 | fd242f857508 |
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 |
License: GPL (GNU GENERAL PUBLIC LICENSE) |
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 |
|
c8e98b9498b4
derive tertium-non-datur by means of Hilbert's choice operator;
wenzelm
parents:
diff
changeset
|
7 |
header {* Hilbert's choice and classical logic *} |
c8e98b9498b4
derive tertium-non-datur by means of Hilbert's choice operator;
wenzelm
parents:
diff
changeset
|
8 |
|
c8e98b9498b4
derive tertium-non-datur by means of Hilbert's choice operator;
wenzelm
parents:
diff
changeset
|
9 |
theory Hilbert_Classical = Main: |
c8e98b9498b4
derive tertium-non-datur by means of Hilbert's choice operator;
wenzelm
parents:
diff
changeset
|
10 |
|
c8e98b9498b4
derive tertium-non-datur by means of Hilbert's choice operator;
wenzelm
parents:
diff
changeset
|
11 |
text {* |
c8e98b9498b4
derive tertium-non-datur by means of Hilbert's choice operator;
wenzelm
parents:
diff
changeset
|
12 |
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
|
13 |
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
|
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 |
|
c8e98b9498b4
derive tertium-non-datur by means of Hilbert's choice operator;
wenzelm
parents:
diff
changeset
|
17 |
subsection {* Proof text *} |
c8e98b9498b4
derive tertium-non-datur by means of Hilbert's choice operator;
wenzelm
parents:
diff
changeset
|
18 |
|
11591 | 19 |
theorem tnd: "A \<or> \<not> A" |
11584
c8e98b9498b4
derive tertium-non-datur by means of Hilbert's choice operator;
wenzelm
parents:
diff
changeset
|
20 |
proof - |
11590 | 21 |
let ?P = "\<lambda>X. X = False \<or> X = True \<and> A" |
22 |
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
|
23 |
|
11590 | 24 |
have a: "?P (Eps ?P)" |
11584
c8e98b9498b4
derive tertium-non-datur by means of Hilbert's choice operator;
wenzelm
parents:
diff
changeset
|
25 |
proof (rule someI) |
c8e98b9498b4
derive tertium-non-datur by means of Hilbert's choice operator;
wenzelm
parents:
diff
changeset
|
26 |
have "False = False" .. |
11590 | 27 |
thus "?P False" .. |
11584
c8e98b9498b4
derive tertium-non-datur by means of Hilbert's choice operator;
wenzelm
parents:
diff
changeset
|
28 |
qed |
11590 | 29 |
have b: "?Q (Eps ?Q)" |
11584
c8e98b9498b4
derive tertium-non-datur by means of Hilbert's choice operator;
wenzelm
parents:
diff
changeset
|
30 |
proof (rule someI) |
c8e98b9498b4
derive tertium-non-datur by means of Hilbert's choice operator;
wenzelm
parents:
diff
changeset
|
31 |
have "True = True" .. |
11590 | 32 |
thus "?Q True" .. |
11584
c8e98b9498b4
derive tertium-non-datur by means of Hilbert's choice operator;
wenzelm
parents:
diff
changeset
|
33 |
qed |
c8e98b9498b4
derive tertium-non-datur by means of Hilbert's choice operator;
wenzelm
parents:
diff
changeset
|
34 |
|
c8e98b9498b4
derive tertium-non-datur by means of Hilbert's choice operator;
wenzelm
parents:
diff
changeset
|
35 |
from a show ?thesis |
c8e98b9498b4
derive tertium-non-datur by means of Hilbert's choice operator;
wenzelm
parents:
diff
changeset
|
36 |
proof |
11590 | 37 |
assume "Eps ?P = True \<and> A" |
38 |
hence A .. |
|
39 |
thus ?thesis .. |
|
40 |
next |
|
41 |
assume P: "Eps ?P = False" |
|
11584
c8e98b9498b4
derive tertium-non-datur by means of Hilbert's choice operator;
wenzelm
parents:
diff
changeset
|
42 |
from b show ?thesis |
c8e98b9498b4
derive tertium-non-datur by means of Hilbert's choice operator;
wenzelm
parents:
diff
changeset
|
43 |
proof |
11590 | 44 |
assume "Eps ?Q = False \<and> A" |
45 |
hence A .. |
|
11584
c8e98b9498b4
derive tertium-non-datur by means of Hilbert's choice operator;
wenzelm
parents:
diff
changeset
|
46 |
thus ?thesis .. |
c8e98b9498b4
derive tertium-non-datur by means of Hilbert's choice operator;
wenzelm
parents:
diff
changeset
|
47 |
next |
11590 | 48 |
assume Q: "Eps ?Q = True" |
49 |
have neq: "?P \<noteq> ?Q" |
|
11584
c8e98b9498b4
derive tertium-non-datur by means of Hilbert's choice operator;
wenzelm
parents:
diff
changeset
|
50 |
proof |
11590 | 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" . |
|
11584
c8e98b9498b4
derive tertium-non-datur by means of Hilbert's choice operator;
wenzelm
parents:
diff
changeset
|
56 |
thus False by (rule False_neq_True) |
c8e98b9498b4
derive tertium-non-datur by means of Hilbert's choice operator;
wenzelm
parents:
diff
changeset
|
57 |
qed |
11590 | 58 |
have "\<not> A" |
11584
c8e98b9498b4
derive tertium-non-datur by means of Hilbert's choice operator;
wenzelm
parents:
diff
changeset
|
59 |
proof |
11590 | 60 |
assume a: A |
61 |
have "?P = ?Q" |
|
11584
c8e98b9498b4
derive tertium-non-datur by means of Hilbert's choice operator;
wenzelm
parents:
diff
changeset
|
62 |
proof |
11590 | 63 |
fix x show "?P x = ?Q x" |
11584
c8e98b9498b4
derive tertium-non-datur by means of Hilbert's choice operator;
wenzelm
parents:
diff
changeset
|
64 |
proof |
11590 | 65 |
assume "?P x" |
66 |
thus "?Q x" |
|
11584
c8e98b9498b4
derive tertium-non-datur by means of Hilbert's choice operator;
wenzelm
parents:
diff
changeset
|
67 |
proof |
c8e98b9498b4
derive tertium-non-datur by means of Hilbert's choice operator;
wenzelm
parents:
diff
changeset
|
68 |
assume "x = False" |
11590 | 69 |
from this and a have "x = False \<and> A" .. |
70 |
thus "?Q x" .. |
|
11584
c8e98b9498b4
derive tertium-non-datur by means of Hilbert's choice operator;
wenzelm
parents:
diff
changeset
|
71 |
next |
11590 | 72 |
assume "x = True \<and> A" |
11584
c8e98b9498b4
derive tertium-non-datur by means of Hilbert's choice operator;
wenzelm
parents:
diff
changeset
|
73 |
hence "x = True" .. |
11590 | 74 |
thus "?Q x" .. |
11584
c8e98b9498b4
derive tertium-non-datur by means of Hilbert's choice operator;
wenzelm
parents:
diff
changeset
|
75 |
qed |
c8e98b9498b4
derive tertium-non-datur by means of Hilbert's choice operator;
wenzelm
parents:
diff
changeset
|
76 |
next |
11590 | 77 |
assume "?Q x" |
78 |
thus "?P x" |
|
11584
c8e98b9498b4
derive tertium-non-datur by means of Hilbert's choice operator;
wenzelm
parents:
diff
changeset
|
79 |
proof |
11590 | 80 |
assume "x = False \<and> A" |
11584
c8e98b9498b4
derive tertium-non-datur by means of Hilbert's choice operator;
wenzelm
parents:
diff
changeset
|
81 |
hence "x = False" .. |
11590 | 82 |
thus "?P x" .. |
11584
c8e98b9498b4
derive tertium-non-datur by means of Hilbert's choice operator;
wenzelm
parents:
diff
changeset
|
83 |
next |
c8e98b9498b4
derive tertium-non-datur by means of Hilbert's choice operator;
wenzelm
parents:
diff
changeset
|
84 |
assume "x = True" |
11590 | 85 |
from this and a have "x = True \<and> A" .. |
86 |
thus "?P x" .. |
|
11584
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 |
qed |
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 |
with neq show False by contradiction |
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 |
thus ?thesis .. |
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 |
qed |
c8e98b9498b4
derive tertium-non-datur by means of Hilbert's choice operator;
wenzelm
parents:
diff
changeset
|
95 |
qed |
c8e98b9498b4
derive tertium-non-datur by means of Hilbert's choice operator;
wenzelm
parents:
diff
changeset
|
96 |
|
c8e98b9498b4
derive tertium-non-datur by means of Hilbert's choice operator;
wenzelm
parents:
diff
changeset
|
97 |
|
11591 | 98 |
subsection {* Proof term of text *} |
99 |
||
100 |
text {* |
|
101 |
{\small @{prf [display, margin = 80] tnd}} |
|
102 |
*} |
|
103 |
||
104 |
||
11584
c8e98b9498b4
derive tertium-non-datur by means of Hilbert's choice operator;
wenzelm
parents:
diff
changeset
|
105 |
subsection {* Proof script *} |
c8e98b9498b4
derive tertium-non-datur by means of Hilbert's choice operator;
wenzelm
parents:
diff
changeset
|
106 |
|
11590 | 107 |
theorem tnd': "A \<or> \<not> A" |
11584
c8e98b9498b4
derive tertium-non-datur by means of Hilbert's choice operator;
wenzelm
parents:
diff
changeset
|
108 |
apply (subgoal_tac |
11590 | 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))") |
|
11584
c8e98b9498b4
derive tertium-non-datur by means of Hilbert's choice operator;
wenzelm
parents:
diff
changeset
|
113 |
prefer 2 |
c8e98b9498b4
derive tertium-non-datur by means of Hilbert's choice operator;
wenzelm
parents:
diff
changeset
|
114 |
apply (rule conjI) |
c8e98b9498b4
derive tertium-non-datur by means of Hilbert's choice operator;
wenzelm
parents:
diff
changeset
|
115 |
apply (rule someI) |
c8e98b9498b4
derive tertium-non-datur by means of Hilbert's choice operator;
wenzelm
parents:
diff
changeset
|
116 |
apply (rule disjI1) |
c8e98b9498b4
derive tertium-non-datur by means of Hilbert's choice operator;
wenzelm
parents:
diff
changeset
|
117 |
apply (rule refl) |
c8e98b9498b4
derive tertium-non-datur by means of Hilbert's choice operator;
wenzelm
parents:
diff
changeset
|
118 |
apply (rule someI) |
c8e98b9498b4
derive tertium-non-datur by means of Hilbert's choice operator;
wenzelm
parents:
diff
changeset
|
119 |
apply (rule disjI2) |
c8e98b9498b4
derive tertium-non-datur by means of Hilbert's choice operator;
wenzelm
parents:
diff
changeset
|
120 |
apply (rule refl) |
c8e98b9498b4
derive tertium-non-datur by means of Hilbert's choice operator;
wenzelm
parents:
diff
changeset
|
121 |
apply (erule conjE) |
c8e98b9498b4
derive tertium-non-datur by means of Hilbert's choice operator;
wenzelm
parents:
diff
changeset
|
122 |
apply (erule disjE) |
c8e98b9498b4
derive tertium-non-datur by means of Hilbert's choice operator;
wenzelm
parents:
diff
changeset
|
123 |
apply (erule disjE) |
c8e98b9498b4
derive tertium-non-datur by means of Hilbert's choice operator;
wenzelm
parents:
diff
changeset
|
124 |
apply (erule conjE) |
c8e98b9498b4
derive tertium-non-datur by means of Hilbert's choice operator;
wenzelm
parents:
diff
changeset
|
125 |
apply (erule disjI1) |
c8e98b9498b4
derive tertium-non-datur by means of Hilbert's choice operator;
wenzelm
parents:
diff
changeset
|
126 |
prefer 2 |
c8e98b9498b4
derive tertium-non-datur by means of Hilbert's choice operator;
wenzelm
parents:
diff
changeset
|
127 |
apply (erule conjE) |
c8e98b9498b4
derive tertium-non-datur by means of Hilbert's choice operator;
wenzelm
parents:
diff
changeset
|
128 |
apply (erule disjI1) |
c8e98b9498b4
derive tertium-non-datur by means of Hilbert's choice operator;
wenzelm
parents:
diff
changeset
|
129 |
apply (subgoal_tac |
11590 | 130 |
"(\<lambda>x. (x = False) \<or> (x = True) \<and> A) \<noteq> |
131 |
(\<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
|
132 |
prefer 2 |
c8e98b9498b4
derive tertium-non-datur by means of Hilbert's choice operator;
wenzelm
parents:
diff
changeset
|
133 |
apply (rule notI) |
11590 | 134 |
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
|
135 |
apply (drule trans, assumption) |
c8e98b9498b4
derive tertium-non-datur by means of Hilbert's choice operator;
wenzelm
parents:
diff
changeset
|
136 |
apply (drule sym) |
c8e98b9498b4
derive tertium-non-datur by means of Hilbert's choice operator;
wenzelm
parents:
diff
changeset
|
137 |
apply (drule trans, assumption) |
c8e98b9498b4
derive tertium-non-datur by means of Hilbert's choice operator;
wenzelm
parents:
diff
changeset
|
138 |
apply (erule False_neq_True) |
c8e98b9498b4
derive tertium-non-datur by means of Hilbert's choice operator;
wenzelm
parents:
diff
changeset
|
139 |
apply (rule disjI2) |
c8e98b9498b4
derive tertium-non-datur by means of Hilbert's choice operator;
wenzelm
parents:
diff
changeset
|
140 |
apply (rule notI) |
c8e98b9498b4
derive tertium-non-datur by means of Hilbert's choice operator;
wenzelm
parents:
diff
changeset
|
141 |
apply (erule notE) |
c8e98b9498b4
derive tertium-non-datur by means of Hilbert's choice operator;
wenzelm
parents:
diff
changeset
|
142 |
apply (rule ext) |
c8e98b9498b4
derive tertium-non-datur by means of Hilbert's choice operator;
wenzelm
parents:
diff
changeset
|
143 |
apply (rule iffI) |
c8e98b9498b4
derive tertium-non-datur by means of Hilbert's choice operator;
wenzelm
parents:
diff
changeset
|
144 |
apply (erule disjE) |
c8e98b9498b4
derive tertium-non-datur by means of Hilbert's choice operator;
wenzelm
parents:
diff
changeset
|
145 |
apply (rule disjI1) |
c8e98b9498b4
derive tertium-non-datur by means of Hilbert's choice operator;
wenzelm
parents:
diff
changeset
|
146 |
apply (erule conjI) |
c8e98b9498b4
derive tertium-non-datur by means of Hilbert's choice operator;
wenzelm
parents:
diff
changeset
|
147 |
apply assumption |
c8e98b9498b4
derive tertium-non-datur by means of Hilbert's choice operator;
wenzelm
parents:
diff
changeset
|
148 |
apply (erule conjE) |
c8e98b9498b4
derive tertium-non-datur by means of Hilbert's choice operator;
wenzelm
parents:
diff
changeset
|
149 |
apply (erule disjI2) |
c8e98b9498b4
derive tertium-non-datur by means of Hilbert's choice operator;
wenzelm
parents:
diff
changeset
|
150 |
apply (erule disjE) |
c8e98b9498b4
derive tertium-non-datur by means of Hilbert's choice operator;
wenzelm
parents:
diff
changeset
|
151 |
apply (erule conjE) |
c8e98b9498b4
derive tertium-non-datur by means of Hilbert's choice operator;
wenzelm
parents:
diff
changeset
|
152 |
apply (erule disjI1) |
c8e98b9498b4
derive tertium-non-datur by means of Hilbert's choice operator;
wenzelm
parents:
diff
changeset
|
153 |
apply (rule disjI2) |
c8e98b9498b4
derive tertium-non-datur by means of Hilbert's choice operator;
wenzelm
parents:
diff
changeset
|
154 |
apply (erule conjI) |
c8e98b9498b4
derive tertium-non-datur by means of Hilbert's choice operator;
wenzelm
parents:
diff
changeset
|
155 |
apply assumption |
c8e98b9498b4
derive tertium-non-datur by means of Hilbert's choice operator;
wenzelm
parents:
diff
changeset
|
156 |
done |
c8e98b9498b4
derive tertium-non-datur by means of Hilbert's choice operator;
wenzelm
parents:
diff
changeset
|
157 |
|
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 |
subsection {* Proof term of script *} |
c8e98b9498b4
derive tertium-non-datur by means of Hilbert's choice operator;
wenzelm
parents:
diff
changeset
|
160 |
|
c8e98b9498b4
derive tertium-non-datur by means of Hilbert's choice operator;
wenzelm
parents:
diff
changeset
|
161 |
text {* |
11591 | 162 |
{\small @{prf [display, margin = 80] tnd'}} |
11584
c8e98b9498b4
derive tertium-non-datur by means of Hilbert's choice operator;
wenzelm
parents:
diff
changeset
|
163 |
*} |
c8e98b9498b4
derive tertium-non-datur by means of Hilbert's choice operator;
wenzelm
parents:
diff
changeset
|
164 |
|
c8e98b9498b4
derive tertium-non-datur by means of Hilbert's choice operator;
wenzelm
parents:
diff
changeset
|
165 |
end |