187 qed "setup_induction"; |
200 qed "setup_induction"; |
188 |
201 |
189 |
202 |
190 section "Set complement -- Compl"; |
203 section "Set complement -- Compl"; |
191 |
204 |
|
205 qed_goalw "Compl_iff" Set.thy [Compl_def] "(c : Compl(A)) = (c~:A)" |
|
206 (fn _ => [ (Fast_tac 1) ]); |
|
207 |
|
208 Addsimps [Compl_iff]; |
|
209 |
192 val prems = goalw Set.thy [Compl_def] |
210 val prems = goalw Set.thy [Compl_def] |
193 "[| c:A ==> False |] ==> c : Compl(A)"; |
211 "[| c:A ==> False |] ==> c : Compl(A)"; |
194 by (REPEAT (ares_tac (prems @ [CollectI,notI]) 1)); |
212 by (REPEAT (ares_tac (prems @ [CollectI,notI]) 1)); |
195 qed "ComplI"; |
213 qed "ComplI"; |
196 |
214 |
197 (*This form, with negated conclusion, works well with the Classical prover. |
215 (*This form, with negated conclusion, works well with the Classical prover. |
198 Negated assumptions behave like formulae on the right side of the notional |
216 Negated assumptions behave like formulae on the right side of the notional |
199 turnstile...*) |
217 turnstile...*) |
200 val major::prems = goalw Set.thy [Compl_def] |
218 val major::prems = goalw Set.thy [Compl_def] |
201 "[| c : Compl(A) |] ==> c~:A"; |
219 "c : Compl(A) ==> c~:A"; |
202 by (rtac (major RS CollectD) 1); |
220 by (rtac (major RS CollectD) 1); |
203 qed "ComplD"; |
221 qed "ComplD"; |
204 |
222 |
205 val ComplE = make_elim ComplD; |
223 val ComplE = make_elim ComplD; |
206 |
224 |
207 qed_goal "Compl_iff" Set.thy "(c : Compl(A)) = (c~:A)" |
225 AddSIs [ComplI]; |
208 (fn _ => [ (fast_tac (!claset addSIs [ComplI] addSEs [ComplE]) 1) ]); |
226 AddSEs [ComplE]; |
209 |
227 |
210 |
228 |
211 section "Binary union -- Un"; |
229 section "Binary union -- Un"; |
212 |
230 |
213 val prems = goalw Set.thy [Un_def] "c:A ==> c : A Un B"; |
231 qed_goalw "Un_iff" Set.thy [Un_def] "(c : A Un B) = (c:A | c:B)" |
214 by (REPEAT (resolve_tac (prems @ [CollectI,disjI1]) 1)); |
232 (fn _ => [ Fast_tac 1 ]); |
|
233 |
|
234 Addsimps [Un_iff]; |
|
235 |
|
236 goal Set.thy "!!c. c:A ==> c : A Un B"; |
|
237 by (Asm_simp_tac 1); |
215 qed "UnI1"; |
238 qed "UnI1"; |
216 |
239 |
217 val prems = goalw Set.thy [Un_def] "c:B ==> c : A Un B"; |
240 goal Set.thy "!!c. c:B ==> c : A Un B"; |
218 by (REPEAT (resolve_tac (prems @ [CollectI,disjI2]) 1)); |
241 by (Asm_simp_tac 1); |
219 qed "UnI2"; |
242 qed "UnI2"; |
220 |
243 |
221 (*Classical introduction rule: no commitment to A vs B*) |
244 (*Classical introduction rule: no commitment to A vs B*) |
222 qed_goal "UnCI" Set.thy "(c~:B ==> c:A) ==> c : A Un B" |
245 qed_goal "UnCI" Set.thy "(c~:B ==> c:A) ==> c : A Un B" |
223 (fn prems=> |
246 (fn prems=> |
224 [ (rtac classical 1), |
247 [ (Simp_tac 1), |
225 (REPEAT (ares_tac (prems@[UnI1,notI]) 1)), |
248 (REPEAT (ares_tac (prems@[disjCI]) 1)) ]); |
226 (REPEAT (ares_tac (prems@[UnI2,notE]) 1)) ]); |
|
227 |
249 |
228 val major::prems = goalw Set.thy [Un_def] |
250 val major::prems = goalw Set.thy [Un_def] |
229 "[| c : A Un B; c:A ==> P; c:B ==> P |] ==> P"; |
251 "[| c : A Un B; c:A ==> P; c:B ==> P |] ==> P"; |
230 by (rtac (major RS CollectD RS disjE) 1); |
252 by (rtac (major RS CollectD RS disjE) 1); |
231 by (REPEAT (eresolve_tac prems 1)); |
253 by (REPEAT (eresolve_tac prems 1)); |
232 qed "UnE"; |
254 qed "UnE"; |
233 |
255 |
234 qed_goal "Un_iff" Set.thy "(c : A Un B) = (c:A | c:B)" |
256 AddSIs [UnCI]; |
235 (fn _ => [ (fast_tac (!claset addSIs [UnCI] addSEs [UnE]) 1) ]); |
257 AddSEs [UnE]; |
236 |
258 |
237 |
259 |
238 section "Binary intersection -- Int"; |
260 section "Binary intersection -- Int"; |
239 |
261 |
240 val prems = goalw Set.thy [Int_def] |
262 qed_goalw "Int_iff" Set.thy [Int_def] "(c : A Int B) = (c:A & c:B)" |
241 "[| c:A; c:B |] ==> c : A Int B"; |
263 (fn _ => [ (Fast_tac 1) ]); |
242 by (REPEAT (resolve_tac (prems @ [CollectI,conjI]) 1)); |
264 |
|
265 Addsimps [Int_iff]; |
|
266 |
|
267 goal Set.thy "!!c. [| c:A; c:B |] ==> c : A Int B"; |
|
268 by (Asm_simp_tac 1); |
243 qed "IntI"; |
269 qed "IntI"; |
244 |
270 |
245 val [major] = goalw Set.thy [Int_def] "c : A Int B ==> c:A"; |
271 goal Set.thy "!!c. c : A Int B ==> c:A"; |
246 by (rtac (major RS CollectD RS conjunct1) 1); |
272 by (Asm_full_simp_tac 1); |
247 qed "IntD1"; |
273 qed "IntD1"; |
248 |
274 |
249 val [major] = goalw Set.thy [Int_def] "c : A Int B ==> c:B"; |
275 goal Set.thy "!!c. c : A Int B ==> c:B"; |
250 by (rtac (major RS CollectD RS conjunct2) 1); |
276 by (Asm_full_simp_tac 1); |
251 qed "IntD2"; |
277 qed "IntD2"; |
252 |
278 |
253 val [major,minor] = goal Set.thy |
279 val [major,minor] = goal Set.thy |
254 "[| c : A Int B; [| c:A; c:B |] ==> P |] ==> P"; |
280 "[| c : A Int B; [| c:A; c:B |] ==> P |] ==> P"; |
255 by (rtac minor 1); |
281 by (rtac minor 1); |
256 by (rtac (major RS IntD1) 1); |
282 by (rtac (major RS IntD1) 1); |
257 by (rtac (major RS IntD2) 1); |
283 by (rtac (major RS IntD2) 1); |
258 qed "IntE"; |
284 qed "IntE"; |
259 |
285 |
260 qed_goal "Int_iff" Set.thy "(c : A Int B) = (c:A & c:B)" |
286 AddSIs [IntI]; |
261 (fn _ => [ (fast_tac (!claset addSIs [IntI] addSEs [IntE]) 1) ]); |
287 AddSEs [IntE]; |
262 |
|
263 |
288 |
264 section "Set difference"; |
289 section "Set difference"; |
265 |
290 |
266 qed_goalw "DiffI" Set.thy [set_diff_def] |
291 qed_goalw "Diff_iff" Set.thy [set_diff_def] "(c : A-B) = (c:A & c~:B)" |
267 "[| c : A; c ~: B |] ==> c : A - B" |
292 (fn _ => [ (Fast_tac 1) ]); |
268 (fn prems=> [ (REPEAT (resolve_tac (prems @ [CollectI,conjI]) 1)) ]); |
293 |
269 |
294 Addsimps [Diff_iff]; |
270 qed_goalw "DiffD1" Set.thy [set_diff_def] |
295 |
271 "c : A - B ==> c : A" |
296 qed_goal "DiffI" Set.thy "!!c. [| c : A; c ~: B |] ==> c : A - B" |
272 (fn [major]=> [ (rtac (major RS CollectD RS conjunct1) 1) ]); |
297 (fn _=> [ Asm_simp_tac 1 ]); |
273 |
298 |
274 qed_goalw "DiffD2" Set.thy [set_diff_def] |
299 qed_goal "DiffD1" Set.thy "!!c. c : A - B ==> c : A" |
275 "[| c : A - B; c : B |] ==> P" |
300 (fn _=> [ (Asm_full_simp_tac 1) ]); |
276 (fn [major,minor]=> |
301 |
277 [rtac (minor RS (major RS CollectD RS conjunct2 RS notE)) 1]); |
302 qed_goal "DiffD2" Set.thy "!!c. [| c : A - B; c : B |] ==> P" |
278 |
303 (fn _=> [ (Asm_full_simp_tac 1) ]); |
279 qed_goal "DiffE" Set.thy |
304 |
280 "[| c : A - B; [| c:A; c~:B |] ==> P |] ==> P" |
305 qed_goal "DiffE" Set.thy "[| c : A - B; [| c:A; c~:B |] ==> P |] ==> P" |
281 (fn prems=> |
306 (fn prems=> |
282 [ (resolve_tac prems 1), |
307 [ (resolve_tac prems 1), |
283 (REPEAT (ares_tac (prems RL [DiffD1, DiffD2 RS notI]) 1)) ]); |
308 (REPEAT (ares_tac (prems RL [DiffD1, DiffD2 RS notI]) 1)) ]); |
284 |
309 |
285 qed_goal "Diff_iff" Set.thy "(c : A-B) = (c:A & c~:B)" |
310 AddSIs [DiffI]; |
286 (fn _ => [ (fast_tac (!claset addSIs [DiffI] addSEs [DiffE]) 1) ]); |
311 AddSEs [DiffE]; |
287 |
312 |
288 section "The empty set -- {}"; |
313 section "The empty set -- {}"; |
289 |
314 |
290 qed_goalw "emptyE" Set.thy [empty_def] "a:{} ==> P" |
315 qed_goalw "empty_iff" Set.thy [empty_def] "(c : {}) = False" |
291 (fn [prem] => [rtac (prem RS CollectD RS FalseE) 1]); |
316 (fn _ => [ (Fast_tac 1) ]); |
|
317 |
|
318 Addsimps [empty_iff]; |
|
319 |
|
320 qed_goal "emptyE" Set.thy "!!a. a:{} ==> P" |
|
321 (fn _ => [Full_simp_tac 1]); |
|
322 |
|
323 AddSEs [emptyE]; |
292 |
324 |
293 qed_goal "empty_subsetI" Set.thy "{} <= A" |
325 qed_goal "empty_subsetI" Set.thy "{} <= A" |
294 (fn _ => [ (REPEAT (ares_tac [equalityI,subsetI,emptyE] 1)) ]); |
326 (fn _ => [ (Fast_tac 1) ]); |
295 |
327 |
296 qed_goal "equals0I" Set.thy "[| !!y. y:A ==> False |] ==> A={}" |
328 qed_goal "equals0I" Set.thy "[| !!y. y:A ==> False |] ==> A={}" |
297 (fn prems=> |
329 (fn [prem]=> |
298 [ (REPEAT (ares_tac (prems@[empty_subsetI,subsetI,equalityI]) 1 |
330 [ (fast_tac (!claset addIs [prem RS FalseE]) 1) ]); |
299 ORELSE eresolve_tac (prems RL [FalseE]) 1)) ]); |
331 |
300 |
332 qed_goal "equals0D" Set.thy "!!a. [| A={}; a:A |] ==> P" |
301 qed_goal "equals0D" Set.thy "[| A={}; a:A |] ==> P" |
333 (fn _ => [ (Fast_tac 1) ]); |
302 (fn [major,minor]=> |
|
303 [ (rtac (minor RS (major RS equalityD1 RS subsetD RS emptyE)) 1) ]); |
|
304 |
|
305 qed_goal "empty_iff" Set.thy "(c : {}) = False" |
|
306 (fn _ => [ (fast_tac (!claset addSEs [emptyE]) 1) ]); |
|
307 |
334 |
308 goal Set.thy "Ball {} P = True"; |
335 goal Set.thy "Ball {} P = True"; |
309 by (simp_tac (HOL_ss addsimps [mem_Collect_eq, Ball_def, empty_def]) 1); |
336 by (simp_tac (HOL_ss addsimps [mem_Collect_eq, Ball_def, empty_def]) 1); |
310 qed "ball_empty"; |
337 qed "ball_empty"; |
311 |
338 |
315 Addsimps [ball_empty, bex_empty]; |
342 Addsimps [ball_empty, bex_empty]; |
316 |
343 |
317 |
344 |
318 section "Augmenting a set -- insert"; |
345 section "Augmenting a set -- insert"; |
319 |
346 |
320 qed_goalw "insertI1" Set.thy [insert_def] "a : insert a B" |
347 qed_goalw "insert_iff" Set.thy [insert_def] "a : insert b A = (a=b | a:A)" |
321 (fn _ => [rtac (CollectI RS UnI1) 1, rtac refl 1]); |
348 (fn _ => [Fast_tac 1]); |
322 |
349 |
323 qed_goalw "insertI2" Set.thy [insert_def] "a : B ==> a : insert b B" |
350 Addsimps [insert_iff]; |
324 (fn [prem]=> [ (rtac (prem RS UnI2) 1) ]); |
351 |
|
352 qed_goal "insertI1" Set.thy "a : insert a B" |
|
353 (fn _ => [Simp_tac 1]); |
|
354 |
|
355 qed_goal "insertI2" Set.thy "!!a. a : B ==> a : insert b B" |
|
356 (fn _=> [Asm_simp_tac 1]); |
325 |
357 |
326 qed_goalw "insertE" Set.thy [insert_def] |
358 qed_goalw "insertE" Set.thy [insert_def] |
327 "[| a : insert b A; a=b ==> P; a:A ==> P |] ==> P" |
359 "[| a : insert b A; a=b ==> P; a:A ==> P |] ==> P" |
328 (fn major::prems=> |
360 (fn major::prems=> |
329 [ (rtac (major RS UnE) 1), |
361 [ (rtac (major RS UnE) 1), |
330 (REPEAT (eresolve_tac (prems @ [CollectE]) 1)) ]); |
362 (REPEAT (eresolve_tac (prems @ [CollectE]) 1)) ]); |
331 |
363 |
332 qed_goal "insert_iff" Set.thy "a : insert b A = (a=b | a:A)" |
|
333 (fn _ => [fast_tac (!claset addIs [insertI1,insertI2] addSEs [insertE]) 1]); |
|
334 |
|
335 (*Classical introduction rule*) |
364 (*Classical introduction rule*) |
336 qed_goal "insertCI" Set.thy "(a~:B ==> a=b) ==> a: insert b B" |
365 qed_goal "insertCI" Set.thy "(a~:B ==> a=b) ==> a: insert b B" |
337 (fn [prem]=> |
366 (fn prems=> |
338 [ (rtac (disjCI RS (insert_iff RS iffD2)) 1), |
367 [ (Simp_tac 1), |
339 (etac prem 1) ]); |
368 (REPEAT (ares_tac (prems@[disjCI]) 1)) ]); |
|
369 |
|
370 AddSIs [insertCI]; |
|
371 AddSEs [insertE]; |
340 |
372 |
341 section "Singletons, using insert"; |
373 section "Singletons, using insert"; |
342 |
374 |
343 qed_goal "singletonI" Set.thy "a : {a}" |
375 qed_goal "singletonI" Set.thy "a : {a}" |
344 (fn _=> [ (rtac insertI1 1) ]); |
376 (fn _=> [ (rtac insertI1 1) ]); |
345 |
377 |
346 goalw Set.thy [insert_def] "!!a. b : {a} ==> b=a"; |
378 goal Set.thy "!!a. b : {a} ==> b=a"; |
347 by (fast_tac (!claset addSEs [emptyE,CollectE,UnE]) 1); |
379 by (Fast_tac 1); |
348 qed "singletonD"; |
380 qed "singletonD"; |
349 |
381 |
350 bind_thm ("singletonE", make_elim singletonD); |
382 bind_thm ("singletonE", make_elim singletonD); |
351 |
383 |
352 qed_goal "singleton_iff" thy "(b : {a}) = (b=a)" (fn _ => [ |
384 qed_goal "singleton_iff" thy "(b : {a}) = (b=a)" |
353 rtac iffI 1, |
385 (fn _ => [Fast_tac 1]); |
354 etac singletonD 1, |
386 |
355 hyp_subst_tac 1, |
387 goal Set.thy "!!a b. {a}={b} ==> a=b"; |
356 rtac singletonI 1]); |
388 by (fast_tac (!claset addEs [equalityE]) 1); |
357 |
|
358 val [major] = goal Set.thy "{a}={b} ==> a=b"; |
|
359 by (rtac (major RS equalityD1 RS subsetD RS singletonD) 1); |
|
360 by (rtac singletonI 1); |
|
361 qed "singleton_inject"; |
389 qed "singleton_inject"; |
|
390 |
|
391 AddSDs [singleton_inject]; |
362 |
392 |
363 |
393 |
364 section "The universal set -- UNIV"; |
394 section "The universal set -- UNIV"; |
365 |
395 |
366 qed_goal "UNIV_I" Set.thy "x : UNIV" |
396 qed_goal "UNIV_I" Set.thy "x : UNIV" |
393 qed "UN_cong"; |
431 qed "UN_cong"; |
394 |
432 |
395 |
433 |
396 section "Intersections of families -- INTER x:A. B(x) is Inter(B``A)"; |
434 section "Intersections of families -- INTER x:A. B(x) is Inter(B``A)"; |
397 |
435 |
|
436 goalw Set.thy [INTER_def] "(b: (INT x:A. B(x))) = (ALL x:A. b: B(x))"; |
|
437 by (Auto_tac()); |
|
438 qed "INT_iff"; |
|
439 |
|
440 Addsimps [INT_iff]; |
|
441 |
398 val prems = goalw Set.thy [INTER_def] |
442 val prems = goalw Set.thy [INTER_def] |
399 "(!!x. x:A ==> b: B(x)) ==> b : (INT x:A. B(x))"; |
443 "(!!x. x:A ==> b: B(x)) ==> b : (INT x:A. B(x))"; |
400 by (REPEAT (ares_tac ([CollectI,ballI] @ prems) 1)); |
444 by (REPEAT (ares_tac ([CollectI,ballI] @ prems) 1)); |
401 qed "INT_I"; |
445 qed "INT_I"; |
402 |
446 |
403 val major::prems = goalw Set.thy [INTER_def] |
447 goal Set.thy "!!b. [| b : (INT x:A. B(x)); a:A |] ==> b: B(a)"; |
404 "[| b : (INT x:A. B(x)); a:A |] ==> b: B(a)"; |
448 by (Auto_tac()); |
405 by (rtac (major RS CollectD RS bspec) 1); |
|
406 by (resolve_tac prems 1); |
|
407 qed "INT_D"; |
449 qed "INT_D"; |
408 |
450 |
409 (*"Classical" elimination -- by the Excluded Middle on a:A *) |
451 (*"Classical" elimination -- by the Excluded Middle on a:A *) |
410 val major::prems = goalw Set.thy [INTER_def] |
452 val major::prems = goalw Set.thy [INTER_def] |
411 "[| b : (INT x:A. B(x)); b: B(a) ==> R; a~:A ==> R |] ==> R"; |
453 "[| b : (INT x:A. B(x)); b: B(a) ==> R; a~:A ==> R |] ==> R"; |
412 by (rtac (major RS CollectD RS ballE) 1); |
454 by (rtac (major RS CollectD RS ballE) 1); |
413 by (REPEAT (eresolve_tac prems 1)); |
455 by (REPEAT (eresolve_tac prems 1)); |
414 qed "INT_E"; |
456 qed "INT_E"; |
|
457 |
|
458 AddSIs [INT_I]; |
|
459 AddEs [INT_D, INT_E]; |
415 |
460 |
416 val prems = goal Set.thy |
461 val prems = goal Set.thy |
417 "[| A=B; !!x. x:B ==> C(x) = D(x) |] ==> \ |
462 "[| A=B; !!x. x:B ==> C(x) = D(x) |] ==> \ |
418 \ (INT x:A. C(x)) = (INT x:B. D(x))"; |
463 \ (INT x:A. C(x)) = (INT x:B. D(x))"; |
419 by (REPEAT_FIRST (resolve_tac [INT_I,equalityI,subsetI])); |
464 by (REPEAT_FIRST (resolve_tac [INT_I,equalityI,subsetI])); |
422 qed "INT_cong"; |
467 qed "INT_cong"; |
423 |
468 |
424 |
469 |
425 section "Unions over a type; UNION1(B) = Union(range(B))"; |
470 section "Unions over a type; UNION1(B) = Union(range(B))"; |
426 |
471 |
|
472 goalw Set.thy [UNION1_def] "(b: (UN x. B(x))) = (EX x. b: B(x))"; |
|
473 by (Simp_tac 1); |
|
474 by (Fast_tac 1); |
|
475 qed "UN1_iff"; |
|
476 |
|
477 Addsimps [UN1_iff]; |
|
478 |
427 (*The order of the premises presupposes that A is rigid; b may be flexible*) |
479 (*The order of the premises presupposes that A is rigid; b may be flexible*) |
428 val prems = goalw Set.thy [UNION1_def] |
480 goal Set.thy "!!b. b: B(x) ==> b: (UN x. B(x))"; |
429 "b: B(x) ==> b: (UN x. B(x))"; |
481 by (Auto_tac()); |
430 by (REPEAT (resolve_tac (prems @ [TrueI, CollectI RS UN_I]) 1)); |
|
431 qed "UN1_I"; |
482 qed "UN1_I"; |
432 |
483 |
433 val major::prems = goalw Set.thy [UNION1_def] |
484 val major::prems = goalw Set.thy [UNION1_def] |
434 "[| b : (UN x. B(x)); !!x. b: B(x) ==> R |] ==> R"; |
485 "[| b : (UN x. B(x)); !!x. b: B(x) ==> R |] ==> R"; |
435 by (rtac (major RS UN_E) 1); |
486 by (rtac (major RS UN_E) 1); |
436 by (REPEAT (ares_tac prems 1)); |
487 by (REPEAT (ares_tac prems 1)); |
437 qed "UN1_E"; |
488 qed "UN1_E"; |
438 |
489 |
|
490 AddIs [UN1_I]; |
|
491 AddSEs [UN1_E]; |
|
492 |
439 |
493 |
440 section "Intersections over a type; INTER1(B) = Inter(range(B))"; |
494 section "Intersections over a type; INTER1(B) = Inter(range(B))"; |
|
495 |
|
496 goalw Set.thy [INTER1_def] "(b: (INT x. B(x))) = (ALL x. b: B(x))"; |
|
497 by (Simp_tac 1); |
|
498 by (Fast_tac 1); |
|
499 qed "INT1_iff"; |
|
500 |
|
501 Addsimps [INT1_iff]; |
441 |
502 |
442 val prems = goalw Set.thy [INTER1_def] |
503 val prems = goalw Set.thy [INTER1_def] |
443 "(!!x. b: B(x)) ==> b : (INT x. B(x))"; |
504 "(!!x. b: B(x)) ==> b : (INT x. B(x))"; |
444 by (REPEAT (ares_tac (INT_I::prems) 1)); |
505 by (REPEAT (ares_tac (INT_I::prems) 1)); |
445 qed "INT1_I"; |
506 qed "INT1_I"; |
446 |
507 |
447 val [major] = goalw Set.thy [INTER1_def] |
508 goal Set.thy "!!b. b : (INT x. B(x)) ==> b: B(a)"; |
448 "b : (INT x. B(x)) ==> b: B(a)"; |
509 by (Asm_full_simp_tac 1); |
449 by (rtac (TrueI RS (CollectI RS (major RS INT_D))) 1); |
|
450 qed "INT1_D"; |
510 qed "INT1_D"; |
451 |
511 |
|
512 AddSIs [INT1_I]; |
|
513 AddDs [INT1_D]; |
|
514 |
|
515 |
452 section "Union"; |
516 section "Union"; |
453 |
517 |
|
518 goalw Set.thy [Union_def] "(A : Union(C)) = (EX X:C. A:X)"; |
|
519 by (Fast_tac 1); |
|
520 qed "Union_iff"; |
|
521 |
|
522 Addsimps [Union_iff]; |
|
523 |
454 (*The order of the premises presupposes that C is rigid; A may be flexible*) |
524 (*The order of the premises presupposes that C is rigid; A may be flexible*) |
455 val prems = goalw Set.thy [Union_def] |
525 goal Set.thy "!!X. [| X:C; A:X |] ==> A : Union(C)"; |
456 "[| X:C; A:X |] ==> A : Union(C)"; |
526 by (Auto_tac()); |
457 by (REPEAT (resolve_tac (prems @ [UN_I]) 1)); |
|
458 qed "UnionI"; |
527 qed "UnionI"; |
459 |
528 |
460 val major::prems = goalw Set.thy [Union_def] |
529 val major::prems = goalw Set.thy [Union_def] |
461 "[| A : Union(C); !!X.[| A:X; X:C |] ==> R |] ==> R"; |
530 "[| A : Union(C); !!X.[| A:X; X:C |] ==> R |] ==> R"; |
462 by (rtac (major RS UN_E) 1); |
531 by (rtac (major RS UN_E) 1); |
463 by (REPEAT (ares_tac prems 1)); |
532 by (REPEAT (ares_tac prems 1)); |
464 qed "UnionE"; |
533 qed "UnionE"; |
465 |
534 |
|
535 AddIs [UnionI]; |
|
536 AddSEs [UnionE]; |
|
537 |
|
538 |
466 section "Inter"; |
539 section "Inter"; |
|
540 |
|
541 goalw Set.thy [Inter_def] "(A : Inter(C)) = (ALL X:C. A:X)"; |
|
542 by (Fast_tac 1); |
|
543 qed "Inter_iff"; |
|
544 |
|
545 Addsimps [Inter_iff]; |
467 |
546 |
468 val prems = goalw Set.thy [Inter_def] |
547 val prems = goalw Set.thy [Inter_def] |
469 "[| !!X. X:C ==> A:X |] ==> A : Inter(C)"; |
548 "[| !!X. X:C ==> A:X |] ==> A : Inter(C)"; |
470 by (REPEAT (ares_tac ([INT_I] @ prems) 1)); |
549 by (REPEAT (ares_tac ([INT_I] @ prems) 1)); |
471 qed "InterI"; |
550 qed "InterI"; |
472 |
551 |
473 (*A "destruct" rule -- every X in C contains A as an element, but |
552 (*A "destruct" rule -- every X in C contains A as an element, but |
474 A:X can hold when X:C does not! This rule is analogous to "spec". *) |
553 A:X can hold when X:C does not! This rule is analogous to "spec". *) |
475 val major::prems = goalw Set.thy [Inter_def] |
554 goal Set.thy "!!X. [| A : Inter(C); X:C |] ==> A:X"; |
476 "[| A : Inter(C); X:C |] ==> A:X"; |
555 by (Auto_tac()); |
477 by (rtac (major RS INT_D) 1); |
|
478 by (resolve_tac prems 1); |
|
479 qed "InterD"; |
556 qed "InterD"; |
480 |
557 |
481 (*"Classical" elimination rule -- does not require proving X:C *) |
558 (*"Classical" elimination rule -- does not require proving X:C *) |
482 val major::prems = goalw Set.thy [Inter_def] |
559 val major::prems = goalw Set.thy [Inter_def] |
483 "[| A : Inter(C); A:X ==> R; X~:C ==> R |] ==> R"; |
560 "[| A : Inter(C); A:X ==> R; X~:C ==> R |] ==> R"; |
484 by (rtac (major RS INT_E) 1); |
561 by (rtac (major RS INT_E) 1); |
485 by (REPEAT (eresolve_tac prems 1)); |
562 by (REPEAT (eresolve_tac prems 1)); |
486 qed "InterE"; |
563 qed "InterE"; |
487 |
564 |
|
565 AddSIs [InterI]; |
|
566 AddEs [InterD, InterE]; |
|
567 |
|
568 |
488 section "The Powerset operator -- Pow"; |
569 section "The Powerset operator -- Pow"; |
|
570 |
|
571 qed_goalw "Pow_iff" Set.thy [Pow_def] "(A : Pow(B)) = (A <= B)" |
|
572 (fn _ => [ (Asm_simp_tac 1) ]); |
|
573 |
|
574 AddIffs [Pow_iff]; |
489 |
575 |
490 qed_goalw "PowI" Set.thy [Pow_def] "!!A B. A <= B ==> A : Pow(B)" |
576 qed_goalw "PowI" Set.thy [Pow_def] "!!A B. A <= B ==> A : Pow(B)" |
491 (fn _ => [ (etac CollectI 1) ]); |
577 (fn _ => [ (etac CollectI 1) ]); |
492 |
578 |
493 qed_goalw "PowD" Set.thy [Pow_def] "!!A B. A : Pow(B) ==> A<=B" |
579 qed_goalw "PowD" Set.thy [Pow_def] "!!A B. A : Pow(B) ==> A<=B" |