24 |
24 |
25 goal Set.thy "!!a. a:A ==> insert(a,A) = A"; |
25 goal Set.thy "!!a. a:A ==> insert(a,A) = A"; |
26 by (fast_tac eq_cs 1); |
26 by (fast_tac eq_cs 1); |
27 val insert_absorb = result(); |
27 val insert_absorb = result(); |
28 |
28 |
|
29 goal Set.thy "(insert(x,A) <= B) = (x:B & A <= B)"; |
|
30 by (fast_tac set_cs 1); |
|
31 val insert_subset = result(); |
|
32 |
29 (** Image **) |
33 (** Image **) |
30 |
34 |
31 goal Set.thy "f``{} = {}"; |
35 goal Set.thy "f``{} = {}"; |
32 by (fast_tac eq_cs 1); |
36 by (fast_tac eq_cs 1); |
33 val image_empty = result(); |
37 val image_empty = result(); |
271 goal Set.thy "A - (B Int C) = (A-B) Un (A-C)"; |
275 goal Set.thy "A - (B Int C) = (A-B) Un (A-C)"; |
272 by (fast_tac eq_cs 1); |
276 by (fast_tac eq_cs 1); |
273 val Diff_Int = result(); |
277 val Diff_Int = result(); |
274 |
278 |
275 val set_ss = set_ss addsimps |
279 val set_ss = set_ss addsimps |
276 [in_empty,in_insert, |
280 [in_empty,in_insert,insert_subset, |
277 Int_absorb,Int_empty_left,Int_empty_right, |
281 Int_absorb,Int_empty_left,Int_empty_right, |
278 Un_absorb,Un_empty_left,Un_empty_right, |
282 Un_absorb,Un_empty_left,Un_empty_right, |
279 constant_UN,image_empty, |
283 constant_UN,image_empty, |
280 Compl_disjoint,double_complement, |
284 Compl_disjoint,double_complement, |
281 Union_empty,Union_insert,empty_subsetI,subset_refl, |
285 Union_empty,Union_insert,empty_subsetI,subset_refl, |