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