11 val eq_cs = set_cs addSIs [equalityI]; |
11 val eq_cs = set_cs addSIs [equalityI]; |
12 |
12 |
13 section "{}"; |
13 section "{}"; |
14 |
14 |
15 goal Set.thy "{x.False} = {}"; |
15 goal Set.thy "{x.False} = {}"; |
16 by(fast_tac eq_cs 1); |
16 by (fast_tac eq_cs 1); |
17 qed "Collect_False_empty"; |
17 qed "Collect_False_empty"; |
18 Addsimps [Collect_False_empty]; |
18 Addsimps [Collect_False_empty]; |
19 |
19 |
20 goal Set.thy "(A <= {}) = (A = {})"; |
20 goal Set.thy "(A <= {}) = (A = {})"; |
21 by(fast_tac eq_cs 1); |
21 by (fast_tac eq_cs 1); |
22 qed "subset_empty"; |
22 qed "subset_empty"; |
23 Addsimps [subset_empty]; |
23 Addsimps [subset_empty]; |
24 |
24 |
25 section ":"; |
25 section ":"; |
26 |
26 |
27 goal Set.thy "x ~: {}"; |
27 goal Set.thy "x ~: {}"; |
28 by(fast_tac set_cs 1); |
28 by (fast_tac set_cs 1); |
29 qed "in_empty"; |
29 qed "in_empty"; |
30 Addsimps[in_empty]; |
30 Addsimps[in_empty]; |
31 |
31 |
32 goal Set.thy "x : insert y A = (x=y | x:A)"; |
32 goal Set.thy "x : insert y A = (x=y | x:A)"; |
33 by(fast_tac set_cs 1); |
33 by (fast_tac set_cs 1); |
34 qed "in_insert"; |
34 qed "in_insert"; |
35 Addsimps[in_insert]; |
35 Addsimps[in_insert]; |
36 |
36 |
37 section "insert"; |
37 section "insert"; |
38 |
38 |
39 (*NOT SUITABLE FOR REWRITING since {a} == insert a {}*) |
39 (*NOT SUITABLE FOR REWRITING since {a} == insert a {}*) |
40 goal Set.thy "insert a A = {a} Un A"; |
40 goal Set.thy "insert a A = {a} Un A"; |
41 by(fast_tac eq_cs 1); |
41 by (fast_tac eq_cs 1); |
42 qed "insert_is_Un"; |
42 qed "insert_is_Un"; |
43 |
43 |
44 goal Set.thy "insert a A ~= {}"; |
44 goal Set.thy "insert a A ~= {}"; |
45 by (fast_tac (set_cs addEs [equalityCE]) 1); |
45 by (fast_tac (set_cs addEs [equalityCE]) 1); |
46 qed"insert_not_empty"; |
46 qed"insert_not_empty"; |
52 goal Set.thy "!!a. a:A ==> insert a A = A"; |
52 goal Set.thy "!!a. a:A ==> insert a A = A"; |
53 by (fast_tac eq_cs 1); |
53 by (fast_tac eq_cs 1); |
54 qed "insert_absorb"; |
54 qed "insert_absorb"; |
55 |
55 |
56 goal Set.thy "insert x (insert x A) = insert x A"; |
56 goal Set.thy "insert x (insert x A) = insert x A"; |
57 by(fast_tac eq_cs 1); |
57 by (fast_tac eq_cs 1); |
58 qed "insert_absorb2"; |
58 qed "insert_absorb2"; |
59 Addsimps [insert_absorb2]; |
59 Addsimps [insert_absorb2]; |
60 |
60 |
61 goal Set.thy "(insert x A <= B) = (x:B & A <= B)"; |
61 goal Set.thy "(insert x A <= B) = (x:B & A <= B)"; |
62 by (fast_tac set_cs 1); |
62 by (fast_tac set_cs 1); |
63 qed "insert_subset"; |
63 qed "insert_subset"; |
64 Addsimps[insert_subset]; |
64 Addsimps[insert_subset]; |
65 |
65 |
66 (* use new B rather than (A-{a}) to avoid infinite unfolding *) |
66 (* use new B rather than (A-{a}) to avoid infinite unfolding *) |
67 goal Set.thy "!!a. a:A ==> ? B. A = insert a B & a ~: B"; |
67 goal Set.thy "!!a. a:A ==> ? B. A = insert a B & a ~: B"; |
68 by(res_inst_tac [("x","A-{a}")] exI 1); |
68 by (res_inst_tac [("x","A-{a}")] exI 1); |
69 by(fast_tac eq_cs 1); |
69 by (fast_tac eq_cs 1); |
70 qed "mk_disjoint_insert"; |
70 qed "mk_disjoint_insert"; |
71 |
71 |
72 section "''"; |
72 section "''"; |
73 |
73 |
74 goal Set.thy "f``{} = {}"; |
74 goal Set.thy "f``{} = {}"; |
143 goal Set.thy "(A Un B) Un C = A Un (B Un C)"; |
143 goal Set.thy "(A Un B) Un C = A Un (B Un C)"; |
144 by (fast_tac eq_cs 1); |
144 by (fast_tac eq_cs 1); |
145 qed "Un_assoc"; |
145 qed "Un_assoc"; |
146 |
146 |
147 goal Set.thy "{} Un B = B"; |
147 goal Set.thy "{} Un B = B"; |
148 by(fast_tac eq_cs 1); |
148 by (fast_tac eq_cs 1); |
149 qed "Un_empty_left"; |
149 qed "Un_empty_left"; |
150 Addsimps[Un_empty_left]; |
150 Addsimps[Un_empty_left]; |
151 |
151 |
152 goal Set.thy "A Un {} = A"; |
152 goal Set.thy "A Un {} = A"; |
153 by(fast_tac eq_cs 1); |
153 by (fast_tac eq_cs 1); |
154 qed "Un_empty_right"; |
154 qed "Un_empty_right"; |
155 Addsimps[Un_empty_right]; |
155 Addsimps[Un_empty_right]; |
156 |
156 |
157 goal Set.thy "UNIV Un B = UNIV"; |
157 goal Set.thy "UNIV Un B = UNIV"; |
158 by(fast_tac eq_cs 1); |
158 by (fast_tac eq_cs 1); |
159 qed "Un_UNIV_left"; |
159 qed "Un_UNIV_left"; |
160 Addsimps[Un_UNIV_left]; |
160 Addsimps[Un_UNIV_left]; |
161 |
161 |
162 goal Set.thy "A Un UNIV = UNIV"; |
162 goal Set.thy "A Un UNIV = UNIV"; |
163 by(fast_tac eq_cs 1); |
163 by (fast_tac eq_cs 1); |
164 qed "Un_UNIV_right"; |
164 qed "Un_UNIV_right"; |
165 Addsimps[Un_UNIV_right]; |
165 Addsimps[Un_UNIV_right]; |
166 |
166 |
167 goal Set.thy "insert a B Un C = insert a (B Un C)"; |
167 goal Set.thy "insert a B Un C = insert a (B Un C)"; |
168 by(fast_tac eq_cs 1); |
168 by (fast_tac eq_cs 1); |
169 qed "Un_insert_left"; |
169 qed "Un_insert_left"; |
170 |
170 |
171 goal Set.thy "(A Int B) Un C = (A Un C) Int (B Un C)"; |
171 goal Set.thy "(A Int B) Un C = (A Un C) Int (B Un C)"; |
172 by (fast_tac eq_cs 1); |
172 by (fast_tac eq_cs 1); |
173 qed "Un_Int_distrib"; |
173 qed "Un_Int_distrib"; |
435 by (fast_tac eq_cs 1); |
435 by (fast_tac eq_cs 1); |
436 qed "Diff_UNIV"; |
436 qed "Diff_UNIV"; |
437 Addsimps[Diff_UNIV]; |
437 Addsimps[Diff_UNIV]; |
438 |
438 |
439 goal Set.thy "!!x. x~:A ==> A - insert x B = A-B"; |
439 goal Set.thy "!!x. x~:A ==> A - insert x B = A-B"; |
440 by(fast_tac eq_cs 1); |
440 by (fast_tac eq_cs 1); |
441 qed "Diff_insert0"; |
441 qed "Diff_insert0"; |
442 Addsimps [Diff_insert0]; |
442 Addsimps [Diff_insert0]; |
443 |
443 |
444 (*NOT SUITABLE FOR REWRITING since {a} == insert a 0*) |
444 (*NOT SUITABLE FOR REWRITING since {a} == insert a 0*) |
445 goal Set.thy "A - insert a B = A - B - {a}"; |
445 goal Set.thy "A - insert a B = A - B - {a}"; |
450 goal Set.thy "A - insert a B = A - {a} - B"; |
450 goal Set.thy "A - insert a B = A - {a} - B"; |
451 by (fast_tac eq_cs 1); |
451 by (fast_tac eq_cs 1); |
452 qed "Diff_insert2"; |
452 qed "Diff_insert2"; |
453 |
453 |
454 goal Set.thy "insert x A - B = (if x:B then A-B else insert x (A-B))"; |
454 goal Set.thy "insert x A - B = (if x:B then A-B else insert x (A-B))"; |
455 by(simp_tac (!simpset setloop split_tac[expand_if]) 1); |
455 by (simp_tac (!simpset setloop split_tac[expand_if]) 1); |
456 by(fast_tac eq_cs 1); |
456 by (fast_tac eq_cs 1); |
457 qed "insert_Diff_if"; |
457 qed "insert_Diff_if"; |
458 |
458 |
459 goal Set.thy "!!x. x:B ==> insert x A - B = A-B"; |
459 goal Set.thy "!!x. x:B ==> insert x A - B = A-B"; |
460 by(fast_tac eq_cs 1); |
460 by (fast_tac eq_cs 1); |
461 qed "insert_Diff1"; |
461 qed "insert_Diff1"; |
462 Addsimps [insert_Diff1]; |
462 Addsimps [insert_Diff1]; |
463 |
463 |
464 val prems = goal Set.thy "a:A ==> insert a (A-{a}) = A"; |
464 val prems = goal Set.thy "a:A ==> insert a (A-{a}) = A"; |
465 by (fast_tac (eq_cs addSIs prems) 1); |
465 by (fast_tac (eq_cs addSIs prems) 1); |