equal
deleted
inserted
replaced
602 qed "subset_iff"; |
602 qed "subset_iff"; |
603 |
603 |
604 goalw thy [psubset_def] "((A::'a set) <= B) = ((A < B) | (A=B))"; |
604 goalw thy [psubset_def] "((A::'a set) <= B) = ((A < B) | (A=B))"; |
605 by (Blast_tac 1); |
605 by (Blast_tac 1); |
606 qed "subset_iff_psubset_eq"; |
606 qed "subset_iff_psubset_eq"; |
|
607 |
|
608 goalw Set.thy [Pow_def] "Pow {} = {{}}"; |
|
609 by (Auto_tac()); |
|
610 qed "Pow_empty"; |
|
611 Addsimps [Pow_empty]; |
|
612 |
|
613 goal Set.thy "Pow (insert a A) = Pow A Un (insert a `` Pow A)"; |
|
614 by (Step_tac 1); |
|
615 be swap 1; |
|
616 by (res_inst_tac [("x", "x-{a}")] image_eqI 1); |
|
617 by (ALLGOALS Blast_tac); |
|
618 qed "Pow_insert"; |
607 |
619 |
608 |
620 |
609 (** Miniscoping: pushing in big Unions and Intersections **) |
621 (** Miniscoping: pushing in big Unions and Intersections **) |
610 local |
622 local |
611 fun prover s = prove_goal Set.thy s (fn _ => [Blast_tac 1]) |
623 fun prover s = prove_goal Set.thy s (fn _ => [Blast_tac 1]) |