author | wenzelm |
Fri, 19 Jul 2013 17:35:12 +0200 | |
changeset 52709 | 0e4bacf21e77 |
parent 48985 | 5386df44a037 |
child 57512 | cc97b347b301 |
permissions | -rw-r--r-- |
16417 | 1 |
theory Basic imports Main begin |
10295 | 2 |
|
3 |
lemma conj_rule: "\<lbrakk> P; Q \<rbrakk> \<Longrightarrow> P \<and> (Q \<and> P)" |
|
4 |
apply (rule conjI) |
|
5 |
apply assumption |
|
6 |
apply (rule conjI) |
|
7 |
apply assumption |
|
8 |
apply assumption |
|
9 |
done |
|
10 |
||
11 |
||
12 |
lemma disj_swap: "P | Q \<Longrightarrow> Q | P" |
|
13 |
apply (erule disjE) |
|
14 |
apply (rule disjI2) |
|
15 |
apply assumption |
|
16 |
apply (rule disjI1) |
|
17 |
apply assumption |
|
18 |
done |
|
19 |
||
20 |
lemma conj_swap: "P \<and> Q \<Longrightarrow> Q \<and> P" |
|
21 |
apply (rule conjI) |
|
22 |
apply (drule conjunct2) |
|
23 |
apply assumption |
|
24 |
apply (drule conjunct1) |
|
25 |
apply assumption |
|
26 |
done |
|
27 |
||
28 |
lemma imp_uncurry: "P \<longrightarrow> Q \<longrightarrow> R \<Longrightarrow> P \<and> Q \<longrightarrow> R" |
|
29 |
apply (rule impI) |
|
30 |
apply (erule conjE) |
|
31 |
apply (drule mp) |
|
32 |
apply assumption |
|
33 |
apply (drule mp) |
|
34 |
apply assumption |
|
35 |
apply assumption |
|
36 |
done |
|
37 |
||
10957 | 38 |
text {* |
10843 | 39 |
by eliminates uses of assumption and done |
40 |
*} |
|
41 |
||
13550 | 42 |
lemma imp_uncurry': "P \<longrightarrow> Q \<longrightarrow> R \<Longrightarrow> P \<and> Q \<longrightarrow> R" |
10843 | 43 |
apply (rule impI) |
44 |
apply (erule conjE) |
|
45 |
apply (drule mp) |
|
46 |
apply assumption |
|
47 |
by (drule mp) |
|
48 |
||
49 |
||
10295 | 50 |
text {* |
51 |
substitution |
|
52 |
||
53 |
@{thm[display] ssubst} |
|
54 |
\rulename{ssubst} |
|
42209
bc7d938991e0
Deletion of all semicolons, because they interfere with Proof General
paulson
parents:
38798
diff
changeset
|
55 |
*} |
10295 | 56 |
|
57 |
lemma "\<lbrakk> x = f x; P(f x) \<rbrakk> \<Longrightarrow> P x" |
|
10843 | 58 |
by (erule ssubst) |
10295 | 59 |
|
60 |
text {* |
|
61 |
also provable by simp (re-orients) |
|
42209
bc7d938991e0
Deletion of all semicolons, because they interfere with Proof General
paulson
parents:
38798
diff
changeset
|
62 |
*} |
10295 | 63 |
|
11182 | 64 |
text {* |
65 |
the subst method |
|
66 |
||
67 |
@{thm[display] mult_commute} |
|
68 |
\rulename{mult_commute} |
|
69 |
||
70 |
this would fail: |
|
71 |
apply (simp add: mult_commute) |
|
42209
bc7d938991e0
Deletion of all semicolons, because they interfere with Proof General
paulson
parents:
38798
diff
changeset
|
72 |
*} |
11182 | 73 |
|
74 |
||
75 |
lemma "\<lbrakk>P x y z; Suc x < y\<rbrakk> \<Longrightarrow> f z = x*y" |
|
76 |
txt{* |
|
77 |
@{subgoals[display,indent=0,margin=65]} |
|
42209
bc7d938991e0
Deletion of all semicolons, because they interfere with Proof General
paulson
parents:
38798
diff
changeset
|
78 |
*} |
11182 | 79 |
apply (subst mult_commute) |
80 |
txt{* |
|
81 |
@{subgoals[display,indent=0,margin=65]} |
|
42209
bc7d938991e0
Deletion of all semicolons, because they interfere with Proof General
paulson
parents:
38798
diff
changeset
|
82 |
*} |
11182 | 83 |
oops |
84 |
||
85 |
(*exercise involving THEN*) |
|
86 |
lemma "\<lbrakk>P x y z; Suc x < y\<rbrakk> \<Longrightarrow> f z = x*y" |
|
87 |
apply (rule mult_commute [THEN ssubst]) |
|
88 |
oops |
|
89 |
||
90 |
||
91 |
lemma "\<lbrakk>x = f x; triple (f x) (f x) x\<rbrakk> \<Longrightarrow> triple x x x" |
|
10957 | 92 |
apply (erule ssubst) |
93 |
--{* @{subgoals[display,indent=0,margin=65]} *} |
|
94 |
back --{* @{subgoals[display,indent=0,margin=65]} *} |
|
95 |
back --{* @{subgoals[display,indent=0,margin=65]} *} |
|
96 |
back --{* @{subgoals[display,indent=0,margin=65]} *} |
|
97 |
back --{* @{subgoals[display,indent=0,margin=65]} *} |
|
10295 | 98 |
apply assumption |
99 |
done |
|
100 |
||
11182 | 101 |
lemma "\<lbrakk> x = f x; triple (f x) (f x) x \<rbrakk> \<Longrightarrow> triple x x x" |
10295 | 102 |
apply (erule ssubst, assumption) |
103 |
done |
|
104 |
||
10843 | 105 |
text{* |
10957 | 106 |
or better still |
10843 | 107 |
*} |
108 |
||
11182 | 109 |
lemma "\<lbrakk> x = f x; triple (f x) (f x) x \<rbrakk> \<Longrightarrow> triple x x x" |
10843 | 110 |
by (erule ssubst) |
111 |
||
112 |
||
11182 | 113 |
lemma "\<lbrakk> x = f x; triple (f x) (f x) x \<rbrakk> \<Longrightarrow> triple x x x" |
114 |
apply (erule_tac P="\<lambda>u. triple u u x" in ssubst) |
|
10843 | 115 |
apply (assumption) |
10295 | 116 |
done |
117 |
||
118 |
||
11182 | 119 |
lemma "\<lbrakk> x = f x; triple (f x) (f x) x \<rbrakk> \<Longrightarrow> triple x x x" |
120 |
by (erule_tac P="\<lambda>u. triple u u x" in ssubst) |
|
10843 | 121 |
|
122 |
||
10295 | 123 |
text {* |
124 |
negation |
|
125 |
||
126 |
@{thm[display] notI} |
|
127 |
\rulename{notI} |
|
128 |
||
129 |
@{thm[display] notE} |
|
130 |
\rulename{notE} |
|
131 |
||
132 |
@{thm[display] classical} |
|
133 |
\rulename{classical} |
|
134 |
||
135 |
@{thm[display] contrapos_pp} |
|
136 |
\rulename{contrapos_pp} |
|
137 |
||
11407 | 138 |
@{thm[display] contrapos_pn} |
139 |
\rulename{contrapos_pn} |
|
140 |
||
10295 | 141 |
@{thm[display] contrapos_np} |
142 |
\rulename{contrapos_np} |
|
143 |
||
144 |
@{thm[display] contrapos_nn} |
|
145 |
\rulename{contrapos_nn} |
|
42209
bc7d938991e0
Deletion of all semicolons, because they interfere with Proof General
paulson
parents:
38798
diff
changeset
|
146 |
*} |
10295 | 147 |
|
148 |
||
149 |
lemma "\<lbrakk>\<not>(P\<longrightarrow>Q); \<not>(R\<longrightarrow>Q)\<rbrakk> \<Longrightarrow> R" |
|
150 |
apply (erule_tac Q="R\<longrightarrow>Q" in contrapos_np) |
|
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32833
diff
changeset
|
151 |
--{* @{subgoals[display,indent=0,margin=65]} *} |
12390 | 152 |
apply (intro impI) |
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32833
diff
changeset
|
153 |
--{* @{subgoals[display,indent=0,margin=65]} *} |
10843 | 154 |
by (erule notE) |
10295 | 155 |
|
11080
22855d091249
various revisions in response to comments from Tobias
paulson
parents:
10957
diff
changeset
|
156 |
text {* |
22855d091249
various revisions in response to comments from Tobias
paulson
parents:
10957
diff
changeset
|
157 |
@{thm[display] disjCI} |
22855d091249
various revisions in response to comments from Tobias
paulson
parents:
10957
diff
changeset
|
158 |
\rulename{disjCI} |
42209
bc7d938991e0
Deletion of all semicolons, because they interfere with Proof General
paulson
parents:
38798
diff
changeset
|
159 |
*} |
11080
22855d091249
various revisions in response to comments from Tobias
paulson
parents:
10957
diff
changeset
|
160 |
|
10295 | 161 |
lemma "(P \<or> Q) \<and> R \<Longrightarrow> P \<or> Q \<and> R" |
12408 | 162 |
apply (intro disjCI conjI) |
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32833
diff
changeset
|
163 |
--{* @{subgoals[display,indent=0,margin=65]} *} |
10295 | 164 |
|
165 |
apply (elim conjE disjE) |
|
166 |
apply assumption |
|
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32833
diff
changeset
|
167 |
--{* @{subgoals[display,indent=0,margin=65]} *} |
10295 | 168 |
|
10843 | 169 |
by (erule contrapos_np, rule conjI) |
10957 | 170 |
text{* |
10295 | 171 |
proof\ {\isacharparenleft}prove{\isacharparenright}{\isacharcolon}\ step\ {\isadigit{6}}\isanewline |
172 |
\isanewline |
|
173 |
goal\ {\isacharparenleft}lemma{\isacharparenright}{\isacharcolon}\isanewline |
|
174 |
{\isacharparenleft}P\ {\isasymor}\ Q{\isacharparenright}\ {\isasymand}\ R\ {\isasymLongrightarrow}\ P\ {\isasymor}\ Q\ {\isasymand}\ R\isanewline |
|
175 |
\ {\isadigit{1}}{\isachardot}\ {\isasymlbrakk}R{\isacharsemicolon}\ Q{\isacharsemicolon}\ {\isasymnot}\ P{\isasymrbrakk}\ {\isasymLongrightarrow}\ Q\isanewline |
|
176 |
\ {\isadigit{2}}{\isachardot}\ {\isasymlbrakk}R{\isacharsemicolon}\ Q{\isacharsemicolon}\ {\isasymnot}\ P{\isasymrbrakk}\ {\isasymLongrightarrow}\ R |
|
177 |
*} |
|
178 |
||
179 |
||
11182 | 180 |
text{*rule_tac, etc.*} |
181 |
||
182 |
||
183 |
lemma "P&Q" |
|
184 |
apply (rule_tac P=P and Q=Q in conjI) |
|
185 |
oops |
|
186 |
||
187 |
||
13756 | 188 |
text{*unification failure trace *} |
189 |
||
52709
0e4bacf21e77
turned pattern unify flag into configuration option (global only);
wenzelm
parents:
48985
diff
changeset
|
190 |
declare [[unify_trace_failure = true]] |
13756 | 191 |
|
192 |
lemma "P(a, f(b, g(e,a), b), a) \<Longrightarrow> P(a, f(b, g(c,a), b), a)" |
|
193 |
txt{* |
|
194 |
@{subgoals[display,indent=0,margin=65]} |
|
195 |
apply assumption |
|
196 |
Clash: e =/= c |
|
197 |
||
198 |
Clash: == =/= Trueprop |
|
199 |
*} |
|
200 |
oops |
|
201 |
||
202 |
lemma "\<forall>x y. P(x,y) --> P(y,x)" |
|
203 |
apply auto |
|
204 |
txt{* |
|
205 |
@{subgoals[display,indent=0,margin=65]} |
|
206 |
apply assumption |
|
207 |
||
208 |
Clash: bound variable x (depth 1) =/= bound variable y (depth 0) |
|
209 |
||
210 |
Clash: == =/= Trueprop |
|
211 |
Clash: == =/= Trueprop |
|
212 |
*} |
|
213 |
oops |
|
214 |
||
52709
0e4bacf21e77
turned pattern unify flag into configuration option (global only);
wenzelm
parents:
48985
diff
changeset
|
215 |
declare [[unify_trace_failure = false]] |
13756 | 216 |
|
217 |
||
10295 | 218 |
text{*Quantifiers*} |
219 |
||
11080
22855d091249
various revisions in response to comments from Tobias
paulson
parents:
10957
diff
changeset
|
220 |
text {* |
22855d091249
various revisions in response to comments from Tobias
paulson
parents:
10957
diff
changeset
|
221 |
@{thm[display] allI} |
22855d091249
various revisions in response to comments from Tobias
paulson
parents:
10957
diff
changeset
|
222 |
\rulename{allI} |
22855d091249
various revisions in response to comments from Tobias
paulson
parents:
10957
diff
changeset
|
223 |
|
22855d091249
various revisions in response to comments from Tobias
paulson
parents:
10957
diff
changeset
|
224 |
@{thm[display] allE} |
22855d091249
various revisions in response to comments from Tobias
paulson
parents:
10957
diff
changeset
|
225 |
\rulename{allE} |
22855d091249
various revisions in response to comments from Tobias
paulson
parents:
10957
diff
changeset
|
226 |
|
22855d091249
various revisions in response to comments from Tobias
paulson
parents:
10957
diff
changeset
|
227 |
@{thm[display] spec} |
22855d091249
various revisions in response to comments from Tobias
paulson
parents:
10957
diff
changeset
|
228 |
\rulename{spec} |
42209
bc7d938991e0
Deletion of all semicolons, because they interfere with Proof General
paulson
parents:
38798
diff
changeset
|
229 |
*} |
11080
22855d091249
various revisions in response to comments from Tobias
paulson
parents:
10957
diff
changeset
|
230 |
|
10295 | 231 |
lemma "\<forall>x. P x \<longrightarrow> P x" |
232 |
apply (rule allI) |
|
10843 | 233 |
by (rule impI) |
10295 | 234 |
|
235 |
lemma "(\<forall>x. P \<longrightarrow> Q x) \<Longrightarrow> P \<longrightarrow> (\<forall>x. Q x)" |
|
10843 | 236 |
apply (rule impI, rule allI) |
10295 | 237 |
apply (drule spec) |
10843 | 238 |
by (drule mp) |
10957 | 239 |
|
11080
22855d091249
various revisions in response to comments from Tobias
paulson
parents:
10957
diff
changeset
|
240 |
text{*rename_tac*} |
10957 | 241 |
lemma "x < y \<Longrightarrow> \<forall>x y. P x (f y)" |
12390 | 242 |
apply (intro allI) |
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32833
diff
changeset
|
243 |
--{* @{subgoals[display,indent=0,margin=65]} *} |
10957 | 244 |
apply (rename_tac v w) |
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32833
diff
changeset
|
245 |
--{* @{subgoals[display,indent=0,margin=65]} *} |
10957 | 246 |
oops |
247 |
||
10295 | 248 |
|
10843 | 249 |
lemma "\<lbrakk>\<forall>x. P x \<longrightarrow> P (h x); P a\<rbrakk> \<Longrightarrow> P(h (h a))" |
10295 | 250 |
apply (frule spec) |
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32833
diff
changeset
|
251 |
--{* @{subgoals[display,indent=0,margin=65]} *} |
10295 | 252 |
apply (drule mp, assumption) |
253 |
apply (drule spec) |
|
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32833
diff
changeset
|
254 |
--{* @{subgoals[display,indent=0,margin=65]} *} |
10843 | 255 |
by (drule mp) |
10295 | 256 |
|
257 |
lemma "\<lbrakk>\<forall>x. P x \<longrightarrow> P (f x); P a\<rbrakk> \<Longrightarrow> P(f (f a))" |
|
258 |
by blast |
|
259 |
||
11234 | 260 |
|
261 |
text{* |
|
262 |
the existential quantifier*} |
|
263 |
||
264 |
text {* |
|
265 |
@{thm[display]"exI"} |
|
266 |
\rulename{exI} |
|
267 |
||
268 |
@{thm[display]"exE"} |
|
269 |
\rulename{exE} |
|
42209
bc7d938991e0
Deletion of all semicolons, because they interfere with Proof General
paulson
parents:
38798
diff
changeset
|
270 |
*} |
11234 | 271 |
|
272 |
||
273 |
text{* |
|
274 |
instantiating quantifiers explicitly by rule_tac and erule_tac*} |
|
275 |
||
276 |
lemma "\<lbrakk>\<forall>x. P x \<longrightarrow> P (h x); P a\<rbrakk> \<Longrightarrow> P(h (h a))" |
|
277 |
apply (frule spec) |
|
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32833
diff
changeset
|
278 |
--{* @{subgoals[display,indent=0,margin=65]} *} |
11234 | 279 |
apply (drule mp, assumption) |
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32833
diff
changeset
|
280 |
--{* @{subgoals[display,indent=0,margin=65]} *} |
11234 | 281 |
apply (drule_tac x = "h a" in spec) |
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32833
diff
changeset
|
282 |
--{* @{subgoals[display,indent=0,margin=65]} *} |
11234 | 283 |
by (drule mp) |
284 |
||
285 |
text {* |
|
286 |
@{thm[display]"dvd_def"} |
|
287 |
\rulename{dvd_def} |
|
42209
bc7d938991e0
Deletion of all semicolons, because they interfere with Proof General
paulson
parents:
38798
diff
changeset
|
288 |
*} |
11234 | 289 |
|
290 |
lemma mult_dvd_mono: "\<lbrakk>i dvd m; j dvd n\<rbrakk> \<Longrightarrow> i*j dvd (m*n :: nat)" |
|
291 |
apply (simp add: dvd_def) |
|
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32833
diff
changeset
|
292 |
--{* @{subgoals[display,indent=0,margin=65]} *} |
11234 | 293 |
apply (erule exE) |
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32833
diff
changeset
|
294 |
--{* @{subgoals[display,indent=0,margin=65]} *} |
11234 | 295 |
apply (erule exE) |
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32833
diff
changeset
|
296 |
--{* @{subgoals[display,indent=0,margin=65]} *} |
11407 | 297 |
apply (rename_tac l) |
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32833
diff
changeset
|
298 |
--{* @{subgoals[display,indent=0,margin=65]} *} |
11407 | 299 |
apply (rule_tac x="k*l" in exI) |
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32833
diff
changeset
|
300 |
--{* @{subgoals[display,indent=0,margin=65]} *} |
11234 | 301 |
apply simp |
302 |
done |
|
303 |
||
10957 | 304 |
text{* |
10843 | 305 |
Hilbert-epsilon theorems*} |
306 |
||
307 |
text{* |
|
11458 | 308 |
@{thm[display] the_equality[no_vars]} |
309 |
\rulename{the_equality} |
|
310 |
||
10843 | 311 |
@{thm[display] some_equality[no_vars]} |
312 |
\rulename{some_equality} |
|
313 |
||
314 |
@{thm[display] someI[no_vars]} |
|
315 |
\rulename{someI} |
|
316 |
||
317 |
@{thm[display] someI2[no_vars]} |
|
318 |
\rulename{someI2} |
|
319 |
||
11080
22855d091249
various revisions in response to comments from Tobias
paulson
parents:
10957
diff
changeset
|
320 |
@{thm[display] someI_ex[no_vars]} |
22855d091249
various revisions in response to comments from Tobias
paulson
parents:
10957
diff
changeset
|
321 |
\rulename{someI_ex} |
22855d091249
various revisions in response to comments from Tobias
paulson
parents:
10957
diff
changeset
|
322 |
|
10843 | 323 |
needed for examples |
324 |
||
325 |
@{thm[display] inv_def[no_vars]} |
|
326 |
\rulename{inv_def} |
|
327 |
||
328 |
@{thm[display] Least_def[no_vars]} |
|
329 |
\rulename{Least_def} |
|
330 |
||
331 |
@{thm[display] order_antisym[no_vars]} |
|
332 |
\rulename{order_antisym} |
|
333 |
*} |
|
334 |
||
335 |
||
11080
22855d091249
various revisions in response to comments from Tobias
paulson
parents:
10957
diff
changeset
|
336 |
lemma "inv Suc (Suc n) = n" |
10843 | 337 |
by (simp add: inv_def) |
338 |
||
339 |
text{*but we know nothing about inv Suc 0*} |
|
340 |
||
341 |
theorem Least_equality: |
|
342 |
"\<lbrakk> P (k::nat); \<forall>x. P x \<longrightarrow> k \<le> x \<rbrakk> \<Longrightarrow> (LEAST x. P(x)) = k" |
|
11456 | 343 |
apply (simp add: Least_def) |
10843 | 344 |
|
11458 | 345 |
txt{* |
10843 | 346 |
@{subgoals[display,indent=0,margin=65]} |
42209
bc7d938991e0
Deletion of all semicolons, because they interfere with Proof General
paulson
parents:
38798
diff
changeset
|
347 |
*} |
10843 | 348 |
|
11456 | 349 |
apply (rule the_equality) |
10843 | 350 |
|
351 |
txt{* |
|
352 |
@{subgoals[display,indent=0,margin=65]} |
|
353 |
||
354 |
first subgoal is existence; second is uniqueness |
|
42209
bc7d938991e0
Deletion of all semicolons, because they interfere with Proof General
paulson
parents:
38798
diff
changeset
|
355 |
*} |
10843 | 356 |
by (auto intro: order_antisym) |
357 |
||
358 |
||
359 |
theorem axiom_of_choice: |
|
11080
22855d091249
various revisions in response to comments from Tobias
paulson
parents:
10957
diff
changeset
|
360 |
"(\<forall>x. \<exists>y. P x y) \<Longrightarrow> \<exists>f. \<forall>x. P x (f x)" |
10843 | 361 |
apply (rule exI, rule allI) |
362 |
||
363 |
txt{* |
|
364 |
@{subgoals[display,indent=0,margin=65]} |
|
365 |
||
366 |
state after intro rules |
|
42209
bc7d938991e0
Deletion of all semicolons, because they interfere with Proof General
paulson
parents:
38798
diff
changeset
|
367 |
*} |
10843 | 368 |
apply (drule spec, erule exE) |
369 |
||
370 |
txt{* |
|
371 |
@{subgoals[display,indent=0,margin=65]} |
|
372 |
||
373 |
applying @text{someI} automatically instantiates |
|
374 |
@{term f} to @{term "\<lambda>x. SOME y. P x y"} |
|
42209
bc7d938991e0
Deletion of all semicolons, because they interfere with Proof General
paulson
parents:
38798
diff
changeset
|
375 |
*} |
10843 | 376 |
|
377 |
by (rule someI) |
|
378 |
||
379 |
(*both can be done by blast, which however hasn't been introduced yet*) |
|
42209
bc7d938991e0
Deletion of all semicolons, because they interfere with Proof General
paulson
parents:
38798
diff
changeset
|
380 |
lemma "[| P (k::nat); \<forall>x. P x \<longrightarrow> k \<le> x |] ==> (LEAST x. P(x)) = k" |
11154 | 381 |
apply (simp add: Least_def LeastM_def) |
42209
bc7d938991e0
Deletion of all semicolons, because they interfere with Proof General
paulson
parents:
38798
diff
changeset
|
382 |
by (blast intro: some_equality order_antisym) |
10843 | 383 |
|
13550 | 384 |
theorem axiom_of_choice': "(\<forall>x. \<exists>y. P x y) \<Longrightarrow> \<exists>f. \<forall>x. P x (f x)" |
10843 | 385 |
apply (rule exI [of _ "\<lambda>x. SOME y. P x y"]) |
42209
bc7d938991e0
Deletion of all semicolons, because they interfere with Proof General
paulson
parents:
38798
diff
changeset
|
386 |
by (blast intro: someI) |
10843 | 387 |
|
10957 | 388 |
text{*end of Epsilon section*} |
389 |
||
10843 | 390 |
|
10295 | 391 |
lemma "(\<exists>x. P x) \<or> (\<exists>x. Q x) \<Longrightarrow> \<exists>x. P x \<or> Q x" |
12390 | 392 |
apply (elim exE disjE) |
12408 | 393 |
apply (intro exI disjI1) |
10295 | 394 |
apply assumption |
12408 | 395 |
apply (intro exI disjI2) |
10295 | 396 |
apply assumption |
397 |
done |
|
398 |
||
399 |
lemma "(P\<longrightarrow>Q) \<or> (Q\<longrightarrow>P)" |
|
12390 | 400 |
apply (intro disjCI impI) |
401 |
apply (elim notE) |
|
402 |
apply (intro impI) |
|
10295 | 403 |
apply assumption |
404 |
done |
|
405 |
||
406 |
lemma "(P\<or>Q)\<and>(P\<or>R) \<Longrightarrow> P \<or> (Q\<and>R)" |
|
12390 | 407 |
apply (intro disjCI conjI) |
10295 | 408 |
apply (elim conjE disjE) |
409 |
apply blast |
|
410 |
apply blast |
|
411 |
apply blast |
|
412 |
apply blast |
|
413 |
(*apply elim*) |
|
414 |
done |
|
415 |
||
416 |
lemma "(\<exists>x. P \<and> Q x) \<Longrightarrow> P \<and> (\<exists>x. Q x)" |
|
417 |
apply (erule exE) |
|
418 |
apply (erule conjE) |
|
419 |
apply (rule conjI) |
|
420 |
apply assumption |
|
421 |
apply (rule exI) |
|
422 |
apply assumption |
|
423 |
done |
|
424 |
||
425 |
lemma "(\<exists>x. P x) \<and> (\<exists>x. Q x) \<Longrightarrow> \<exists>x. P x \<and> Q x" |
|
426 |
apply (erule conjE) |
|
427 |
apply (erule exE) |
|
428 |
apply (erule exE) |
|
429 |
apply (rule exI) |
|
430 |
apply (rule conjI) |
|
431 |
apply assumption |
|
432 |
oops |
|
433 |
||
11407 | 434 |
lemma "\<forall>y. R y y \<Longrightarrow> \<exists>x. \<forall>y. R x y" |
11080
22855d091249
various revisions in response to comments from Tobias
paulson
parents:
10957
diff
changeset
|
435 |
apply (rule exI) |
22855d091249
various revisions in response to comments from Tobias
paulson
parents:
10957
diff
changeset
|
436 |
--{* @{subgoals[display,indent=0,margin=65]} *} |
22855d091249
various revisions in response to comments from Tobias
paulson
parents:
10957
diff
changeset
|
437 |
apply (rule allI) |
22855d091249
various revisions in response to comments from Tobias
paulson
parents:
10957
diff
changeset
|
438 |
--{* @{subgoals[display,indent=0,margin=65]} *} |
22855d091249
various revisions in response to comments from Tobias
paulson
parents:
10957
diff
changeset
|
439 |
apply (drule spec) |
22855d091249
various revisions in response to comments from Tobias
paulson
parents:
10957
diff
changeset
|
440 |
--{* @{subgoals[display,indent=0,margin=65]} *} |
10295 | 441 |
oops |
442 |
||
11407 | 443 |
lemma "\<forall>x. \<exists>y. x=y" |
10295 | 444 |
apply (rule allI) |
445 |
apply (rule exI) |
|
446 |
apply (rule refl) |
|
447 |
done |
|
448 |
||
11407 | 449 |
lemma "\<exists>x. \<forall>y. x=y" |
10295 | 450 |
apply (rule exI) |
451 |
apply (rule allI) |
|
452 |
oops |
|
453 |
||
454 |
end |