317 section "Singletons, using insert"; |
317 section "Singletons, using insert"; |
318 |
318 |
319 qed_goal "singletonI" Set.thy "a : {a}" |
319 qed_goal "singletonI" Set.thy "a : {a}" |
320 (fn _=> [ (rtac insertI1 1) ]); |
320 (fn _=> [ (rtac insertI1 1) ]); |
321 |
321 |
322 qed_goal "singletonE" Set.thy "[| a: {b}; a=b ==> P |] ==> P" |
|
323 (fn major::prems=> |
|
324 [ (rtac (major RS insertE) 1), |
|
325 (REPEAT (eresolve_tac (prems @ [emptyE]) 1)) ]); |
|
326 |
|
327 goalw Set.thy [insert_def] "!!a. b : {a} ==> b=a"; |
322 goalw Set.thy [insert_def] "!!a. b : {a} ==> b=a"; |
328 by (fast_tac (!claset addSEs [emptyE,CollectE,UnE]) 1); |
323 by (fast_tac (!claset addSEs [emptyE,CollectE,UnE]) 1); |
329 qed "singletonD"; |
324 qed "singletonD"; |
330 |
325 |
331 val singletonE = make_elim singletonD; |
326 bind_thm ("singletonE", make_elim singletonD); |
|
327 |
|
328 qed_goal "singleton_iff" thy "(b : {a}) = (b=a)" (fn _ => [ |
|
329 rtac iffI 1, |
|
330 etac singletonD 1, |
|
331 hyp_subst_tac 1, |
|
332 rtac singletonI 1]); |
332 |
333 |
333 val [major] = goal Set.thy "{a}={b} ==> a=b"; |
334 val [major] = goal Set.thy "{a}={b} ==> a=b"; |
334 by (rtac (major RS equalityD1 RS subsetD RS singletonD) 1); |
335 by (rtac (major RS equalityD1 RS subsetD RS singletonD) 1); |
335 by (rtac singletonI 1); |
336 by (rtac singletonI 1); |
336 qed "singleton_inject"; |
337 qed "singleton_inject"; |
465 qed_goalw "PowD" Set.thy [Pow_def] "!!A B. A : Pow(B) ==> A<=B" |
466 qed_goalw "PowD" Set.thy [Pow_def] "!!A B. A : Pow(B) ==> A<=B" |
466 (fn _=> [ (etac CollectD 1) ]); |
467 (fn _=> [ (etac CollectD 1) ]); |
467 |
468 |
468 val Pow_bottom = empty_subsetI RS PowI; (* {}: Pow(B) *) |
469 val Pow_bottom = empty_subsetI RS PowI; (* {}: Pow(B) *) |
469 val Pow_top = subset_refl RS PowI; (* A : Pow(A) *) |
470 val Pow_top = subset_refl RS PowI; (* A : Pow(A) *) |
|
471 |
|
472 |
|
473 |
|
474 (*** Set reasoning tools ***) |
|
475 |
|
476 |
|
477 val mem_simps = [ Un_iff, Int_iff, Compl_iff, Diff_iff, singleton_iff, |
|
478 mem_Collect_eq]; |
|
479 |
|
480 val mksimps_pairs = ("Ball",[bspec]) :: mksimps_pairs; |
|
481 |
|
482 simpset := !simpset addsimps mem_simps |
|
483 addcongs [ball_cong,bex_cong] |
|
484 setmksimps (mksimps mksimps_pairs); |