69 (*The best argument order when there is only one x:A*) |
69 (*The best argument order when there is only one x:A*) |
70 Goalw [Bex_def] "[| x:A; P(x) |] ==> ? x:A. P(x)"; |
70 Goalw [Bex_def] "[| x:A; P(x) |] ==> ? x:A. P(x)"; |
71 by (Blast_tac 1); |
71 by (Blast_tac 1); |
72 qed "rev_bexI"; |
72 qed "rev_bexI"; |
73 |
73 |
74 qed_goal "bexCI" Set.thy |
74 val prems = goal Set.thy |
75 "[| ! x:A. ~P(x) ==> P(a); a:A |] ==> ? x:A. P(x)" (fn prems => |
75 "[| ! x:A. ~P(x) ==> P(a); a:A |] ==> ? x:A. P(x)"; |
76 [ (rtac classical 1), |
76 by (rtac classical 1); |
77 (REPEAT (ares_tac (prems@[bexI,ballI,notI,notE]) 1)) ]); |
77 by (REPEAT (ares_tac (prems@[bexI,ballI,notI,notE]) 1)) ; |
|
78 qed "bexCI"; |
78 |
79 |
79 val major::prems = Goalw [Bex_def] |
80 val major::prems = Goalw [Bex_def] |
80 "[| ? x:A. P(x); !!x. [| x:A; P(x) |] ==> Q |] ==> Q"; |
81 "[| ? x:A. P(x); !!x. [| x:A; P(x) |] ==> Q |] ==> Q"; |
81 by (rtac (major RS exE) 1); |
82 by (rtac (major RS exE) 1); |
82 by (REPEAT (eresolve_tac (prems @ [asm_rl,conjE]) 1)); |
83 by (REPEAT (eresolve_tac (prems @ [asm_rl,conjE]) 1)); |
137 Goalw [subset_def] "[| A <= B; c:A |] ==> c:B"; |
138 Goalw [subset_def] "[| A <= B; c:A |] ==> c:B"; |
138 by (Blast_tac 1); |
139 by (Blast_tac 1); |
139 qed "subsetD"; |
140 qed "subsetD"; |
140 |
141 |
141 (*The same, with reversed premises for use with etac -- cf rev_mp*) |
142 (*The same, with reversed premises for use with etac -- cf rev_mp*) |
142 qed_goal "rev_subsetD" Set.thy "[| c:A; A <= B |] ==> c:B" |
143 Goal "[| c:A; A <= B |] ==> c:B"; |
143 (fn prems=> [ (REPEAT (resolve_tac (prems@[subsetD]) 1)) ]); |
144 by (REPEAT (ares_tac [subsetD] 1)) ; |
|
145 qed "rev_subsetD"; |
144 |
146 |
145 (*Converts A<=B to x:A ==> x:B*) |
147 (*Converts A<=B to x:A ==> x:B*) |
146 fun impOfSubs th = th RSN (2, rev_subsetD); |
148 fun impOfSubs th = th RSN (2, rev_subsetD); |
147 |
149 |
148 qed_goal "contra_subsetD" Set.thy "!!c. [| A <= B; c ~: B |] ==> c ~: A" |
150 Goal "[| A <= B; c ~: B |] ==> c ~: A"; |
149 (fn prems=> [ (REPEAT (eresolve_tac [asm_rl, contrapos, subsetD] 1)) ]); |
151 by (REPEAT (eresolve_tac [asm_rl, contrapos, subsetD] 1)) ; |
150 |
152 qed "contra_subsetD"; |
151 qed_goal "rev_contra_subsetD" Set.thy "!!c. [| c ~: B; A <= B |] ==> c ~: A" |
153 |
152 (fn prems=> [ (REPEAT (eresolve_tac [asm_rl, contrapos, subsetD] 1)) ]); |
154 Goal "[| c ~: B; A <= B |] ==> c ~: A"; |
|
155 by (REPEAT (eresolve_tac [asm_rl, contrapos, subsetD] 1)) ; |
|
156 qed "rev_contra_subsetD"; |
153 |
157 |
154 (*Classical elimination rule*) |
158 (*Classical elimination rule*) |
155 val major::prems = Goalw [subset_def] |
159 val major::prems = Goalw [subset_def] |
156 "[| A <= B; c~:A ==> P; c:B ==> P |] ==> P"; |
160 "[| A <= B; c~:A ==> P; c:B ==> P |] ==> P"; |
157 by (rtac (major RS ballE) 1); |
161 by (rtac (major RS ballE) 1); |
162 fun set_mp_tac i = etac subsetCE i THEN mp_tac i; |
166 fun set_mp_tac i = etac subsetCE i THEN mp_tac i; |
163 |
167 |
164 AddSIs [subsetI]; |
168 AddSIs [subsetI]; |
165 AddEs [subsetD, subsetCE]; |
169 AddEs [subsetD, subsetCE]; |
166 |
170 |
167 qed_goal "subset_refl" Set.thy "A <= (A::'a set)" |
171 Goal "A <= (A::'a set)"; |
168 (fn _=> [Fast_tac 1]); (*Blast_tac would try order_refl and fail*) |
172 by (Fast_tac 1); |
|
173 qed "subset_refl"; (*Blast_tac would try order_refl and fail*) |
169 |
174 |
170 Goal "[| A<=B; B<=C |] ==> A<=(C::'a set)"; |
175 Goal "[| A<=B; B<=C |] ==> A<=(C::'a set)"; |
171 by (Blast_tac 1); |
176 by (Blast_tac 1); |
172 qed "subset_trans"; |
177 qed "subset_trans"; |
173 |
178 |
240 Addsimps [ball_UNIV, bex_UNIV]; |
245 Addsimps [ball_UNIV, bex_UNIV]; |
241 |
246 |
242 |
247 |
243 section "The empty set -- {}"; |
248 section "The empty set -- {}"; |
244 |
249 |
245 qed_goalw "empty_iff" Set.thy [empty_def] "(c : {}) = False" |
250 Goalw [empty_def] "(c : {}) = False"; |
246 (fn _ => [ (Blast_tac 1) ]); |
251 by (Blast_tac 1) ; |
|
252 qed "empty_iff"; |
247 |
253 |
248 Addsimps [empty_iff]; |
254 Addsimps [empty_iff]; |
249 |
255 |
250 qed_goal "emptyE" Set.thy "!!a. a:{} ==> P" |
256 Goal "a:{} ==> P"; |
251 (fn _ => [Full_simp_tac 1]); |
257 by (Full_simp_tac 1); |
|
258 qed "emptyE"; |
252 |
259 |
253 AddSEs [emptyE]; |
260 AddSEs [emptyE]; |
254 |
261 |
255 qed_goal "empty_subsetI" Set.thy "{} <= A" |
262 Goal "{} <= A"; |
256 (fn _ => [ (Blast_tac 1) ]); |
263 by (Blast_tac 1) ; |
|
264 qed "empty_subsetI"; |
257 |
265 |
258 (*One effect is to delete the ASSUMPTION {} <= A*) |
266 (*One effect is to delete the ASSUMPTION {} <= A*) |
259 AddIffs [empty_subsetI]; |
267 AddIffs [empty_subsetI]; |
260 |
268 |
261 qed_goal "equals0I" Set.thy "[| !!y. y:A ==> False |] ==> A={}" |
269 val [prem]= goal Set.thy "[| !!y. y:A ==> False |] ==> A={}"; |
262 (fn [prem]=> |
270 by (blast_tac (claset() addIs [prem RS FalseE]) 1) ; |
263 [ (blast_tac (claset() addIs [prem RS FalseE]) 1) ]); |
271 qed "equals0I"; |
264 |
272 |
265 (*Use for reasoning about disjointness: A Int B = {} *) |
273 (*Use for reasoning about disjointness: A Int B = {} *) |
266 qed_goal "equals0D" Set.thy "!!a. A={} ==> a ~: A" |
274 Goal "A={} ==> a ~: A"; |
267 (fn _ => [ (Blast_tac 1) ]); |
275 by (Blast_tac 1) ; |
|
276 qed "equals0D"; |
268 |
277 |
269 AddDs [equals0D, sym RS equals0D]; |
278 AddDs [equals0D, sym RS equals0D]; |
270 |
279 |
271 Goalw [Ball_def] "Ball {} P = True"; |
280 Goalw [Ball_def] "Ball {} P = True"; |
272 by (Simp_tac 1); |
281 by (Simp_tac 1); |
284 |
293 |
285 |
294 |
286 |
295 |
287 section "The Powerset operator -- Pow"; |
296 section "The Powerset operator -- Pow"; |
288 |
297 |
289 qed_goalw "Pow_iff" Set.thy [Pow_def] "(A : Pow(B)) = (A <= B)" |
298 Goalw [Pow_def] "(A : Pow(B)) = (A <= B)"; |
290 (fn _ => [ (Asm_simp_tac 1) ]); |
299 by (Asm_simp_tac 1); |
|
300 qed "Pow_iff"; |
291 |
301 |
292 AddIffs [Pow_iff]; |
302 AddIffs [Pow_iff]; |
293 |
303 |
294 qed_goalw "PowI" Set.thy [Pow_def] "!!A B. A <= B ==> A : Pow(B)" |
304 Goalw [Pow_def] "!!A B. A <= B ==> A : Pow(B)"; |
295 (fn _ => [ (etac CollectI 1) ]); |
305 by (etac CollectI 1); |
296 |
306 qed "PowI"; |
297 qed_goalw "PowD" Set.thy [Pow_def] "!!A B. A : Pow(B) ==> A<=B" |
307 |
298 (fn _=> [ (etac CollectD 1) ]); |
308 Goalw [Pow_def] "!!A B. A : Pow(B) ==> A<=B"; |
|
309 by (etac CollectD 1); |
|
310 qed "PowD"; |
|
311 |
299 |
312 |
300 val Pow_bottom = empty_subsetI RS PowI; (* {}: Pow(B) *) |
313 val Pow_bottom = empty_subsetI RS PowI; (* {}: Pow(B) *) |
301 val Pow_top = subset_refl RS PowI; (* A : Pow(A) *) |
314 val Pow_top = subset_refl RS PowI; (* A : Pow(A) *) |
302 |
315 |
303 |
316 |
339 Goal "c:B ==> c : A Un B"; |
352 Goal "c:B ==> c : A Un B"; |
340 by (Asm_simp_tac 1); |
353 by (Asm_simp_tac 1); |
341 qed "UnI2"; |
354 qed "UnI2"; |
342 |
355 |
343 (*Classical introduction rule: no commitment to A vs B*) |
356 (*Classical introduction rule: no commitment to A vs B*) |
344 qed_goal "UnCI" Set.thy "(c~:B ==> c:A) ==> c : A Un B" |
357 |
345 (fn prems=> |
358 val prems= goal Set.thy "(c~:B ==> c:A) ==> c : A Un B"; |
346 [ (Simp_tac 1), |
359 by (Simp_tac 1); |
347 (REPEAT (ares_tac (prems@[disjCI]) 1)) ]); |
360 by (REPEAT (ares_tac (prems@[disjCI]) 1)) ; |
|
361 qed "UnCI"; |
348 |
362 |
349 val major::prems = Goalw [Un_def] |
363 val major::prems = Goalw [Un_def] |
350 "[| c : A Un B; c:A ==> P; c:B ==> P |] ==> P"; |
364 "[| c : A Un B; c:A ==> P; c:B ==> P |] ==> P"; |
351 by (rtac (major RS CollectD RS disjE) 1); |
365 by (rtac (major RS CollectD RS disjE) 1); |
352 by (REPEAT (eresolve_tac prems 1)); |
366 by (REPEAT (eresolve_tac prems 1)); |
390 qed_goalw "Diff_iff" Set.thy [set_diff_def] "(c : A-B) = (c:A & c~:B)" |
404 qed_goalw "Diff_iff" Set.thy [set_diff_def] "(c : A-B) = (c:A & c~:B)" |
391 (fn _ => [ (Blast_tac 1) ]); |
405 (fn _ => [ (Blast_tac 1) ]); |
392 |
406 |
393 Addsimps [Diff_iff]; |
407 Addsimps [Diff_iff]; |
394 |
408 |
395 qed_goal "DiffI" Set.thy "!!c. [| c : A; c ~: B |] ==> c : A - B" |
409 Goal "[| c : A; c ~: B |] ==> c : A - B"; |
396 (fn _=> [ Asm_simp_tac 1 ]); |
410 by (Asm_simp_tac 1) ; |
397 |
411 qed "DiffI"; |
398 qed_goal "DiffD1" Set.thy "!!c. c : A - B ==> c : A" |
412 |
399 (fn _=> [ (Asm_full_simp_tac 1) ]); |
413 Goal "c : A - B ==> c : A"; |
400 |
414 by (Asm_full_simp_tac 1) ; |
401 qed_goal "DiffD2" Set.thy "!!c. [| c : A - B; c : B |] ==> P" |
415 qed "DiffD1"; |
402 (fn _=> [ (Asm_full_simp_tac 1) ]); |
416 |
403 |
417 Goal "[| c : A - B; c : B |] ==> P"; |
404 qed_goal "DiffE" Set.thy "[| c : A - B; [| c:A; c~:B |] ==> P |] ==> P" |
418 by (Asm_full_simp_tac 1) ; |
405 (fn prems=> |
419 qed "DiffD2"; |
406 [ (resolve_tac prems 1), |
420 |
407 (REPEAT (ares_tac (prems RL [DiffD1, DiffD2 RS notI]) 1)) ]); |
421 val prems= goal Set.thy "[| c : A - B; [| c:A; c~:B |] ==> P |] ==> P"; |
|
422 by (resolve_tac prems 1); |
|
423 by (REPEAT (ares_tac (prems RL [DiffD1, DiffD2 RS notI]) 1)) ; |
|
424 qed "DiffE"; |
408 |
425 |
409 AddSIs [DiffI]; |
426 AddSIs [DiffI]; |
410 AddSEs [DiffE]; |
427 AddSEs [DiffE]; |
411 |
428 |
412 |
429 |
415 qed_goalw "insert_iff" Set.thy [insert_def] "a : insert b A = (a=b | a:A)" |
432 qed_goalw "insert_iff" Set.thy [insert_def] "a : insert b A = (a=b | a:A)" |
416 (fn _ => [Blast_tac 1]); |
433 (fn _ => [Blast_tac 1]); |
417 |
434 |
418 Addsimps [insert_iff]; |
435 Addsimps [insert_iff]; |
419 |
436 |
420 qed_goal "insertI1" Set.thy "a : insert a B" |
437 val _ = goal Set.thy "a : insert a B"; |
421 (fn _ => [Simp_tac 1]); |
438 by (Simp_tac 1); |
422 |
439 qed "insertI1"; |
423 qed_goal "insertI2" Set.thy "!!a. a : B ==> a : insert b B" |
440 |
424 (fn _=> [Asm_simp_tac 1]); |
441 Goal "!!a. a : B ==> a : insert b B"; |
425 |
442 by (Asm_simp_tac 1); |
426 qed_goalw "insertE" Set.thy [insert_def] |
443 qed "insertI2"; |
427 "[| a : insert b A; a=b ==> P; a:A ==> P |] ==> P" |
444 |
428 (fn major::prems=> |
445 val major::prems = Goalw [insert_def] |
429 [ (rtac (major RS UnE) 1), |
446 "[| a : insert b A; a=b ==> P; a:A ==> P |] ==> P"; |
430 (REPEAT (eresolve_tac (prems @ [CollectE]) 1)) ]); |
447 by (rtac (major RS UnE) 1); |
|
448 by (REPEAT (eresolve_tac (prems @ [CollectE]) 1)); |
|
449 qed "insertE"; |
431 |
450 |
432 (*Classical introduction rule*) |
451 (*Classical introduction rule*) |
433 qed_goal "insertCI" Set.thy "(a~:B ==> a=b) ==> a: insert b B" |
452 val prems= goal Set.thy "(a~:B ==> a=b) ==> a: insert b B"; |
434 (fn prems=> |
453 by (Simp_tac 1); |
435 [ (Simp_tac 1), |
454 by (REPEAT (ares_tac (prems@[disjCI]) 1)) ; |
436 (REPEAT (ares_tac (prems@[disjCI]) 1)) ]); |
455 qed "insertCI"; |
437 |
456 |
438 AddSIs [insertCI]; |
457 AddSIs [insertCI]; |
439 AddSEs [insertE]; |
458 AddSEs [insertE]; |
440 |
459 |
441 section "Singletons, using insert"; |
460 section "Singletons, using insert"; |
442 |
461 |
443 qed_goal "singletonI" Set.thy "a : {a}" |
462 Goal "a : {a}"; |
444 (fn _=> [ (rtac insertI1 1) ]); |
463 by (rtac insertI1 1) ; |
|
464 qed "singletonI"; |
445 |
465 |
446 Goal "b : {a} ==> b=a"; |
466 Goal "b : {a} ==> b=a"; |
447 by (Blast_tac 1); |
467 by (Blast_tac 1); |
448 qed "singletonD"; |
468 qed "singletonD"; |
449 |
469 |
450 bind_thm ("singletonE", make_elim singletonD); |
470 bind_thm ("singletonE", make_elim singletonD); |
451 |
471 |
452 qed_goal "singleton_iff" thy "(b : {a}) = (b=a)" |
472 Goal "(b : {a}) = (b=a)"; |
453 (fn _ => [Blast_tac 1]); |
473 by (Blast_tac 1); |
|
474 qed "singleton_iff"; |
454 |
475 |
455 Goal "{a}={b} ==> a=b"; |
476 Goal "{a}={b} ==> a=b"; |
456 by (blast_tac (claset() addEs [equalityE]) 1); |
477 by (blast_tac (claset() addEs [equalityE]) 1); |
457 qed "singleton_inject"; |
478 qed "singleton_inject"; |
458 |
479 |