author | lcp |
Thu, 06 Apr 1995 11:49:42 +0200 | |
changeset 246 | 0f9230a24164 |
parent 205 | ccbbe1264c0f |
permissions | -rw-r--r-- |
0 | 1 |
(* Title: HOL/equalities |
2 |
ID: $Id$ |
|
3 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
|
76
fb4fe9f8c3cd
HOL/equalities: added some identities from ZF/equalities
lcp
parents:
57
diff
changeset
|
4 |
Copyright 1994 University of Cambridge |
0 | 5 |
|
6 |
Equalities involving union, intersection, inclusion, etc. |
|
7 |
*) |
|
8 |
||
9 |
writeln"File HOL/equalities"; |
|
10 |
||
11 |
val eq_cs = set_cs addSIs [equalityI]; |
|
12 |
||
76
fb4fe9f8c3cd
HOL/equalities: added some identities from ZF/equalities
lcp
parents:
57
diff
changeset
|
13 |
(** The membership relation, : **) |
27 | 14 |
|
15 |
goal Set.thy "x ~: {}"; |
|
16 |
by(fast_tac set_cs 1); |
|
171 | 17 |
qed "in_empty"; |
27 | 18 |
|
19 |
goal Set.thy "x : insert(y,A) = (x=y | x:A)"; |
|
20 |
by(fast_tac set_cs 1); |
|
171 | 21 |
qed "in_insert"; |
27 | 22 |
|
0 | 23 |
(** insert **) |
24 |
||
25 |
goal Set.thy "!!a. a:A ==> insert(a,A) = A"; |
|
26 |
by (fast_tac eq_cs 1); |
|
171 | 27 |
qed "insert_absorb"; |
0 | 28 |
|
57 | 29 |
goal Set.thy "(insert(x,A) <= B) = (x:B & A <= B)"; |
30 |
by (fast_tac set_cs 1); |
|
171 | 31 |
qed "insert_subset"; |
57 | 32 |
|
0 | 33 |
(** Image **) |
34 |
||
35 |
goal Set.thy "f``{} = {}"; |
|
36 |
by (fast_tac eq_cs 1); |
|
171 | 37 |
qed "image_empty"; |
0 | 38 |
|
39 |
goal Set.thy "f``insert(a,B) = insert(f(a), f``B)"; |
|
40 |
by (fast_tac eq_cs 1); |
|
171 | 41 |
qed "image_insert"; |
0 | 42 |
|
43 |
(** Binary Intersection **) |
|
44 |
||
45 |
goal Set.thy "A Int A = A"; |
|
46 |
by (fast_tac eq_cs 1); |
|
171 | 47 |
qed "Int_absorb"; |
0 | 48 |
|
49 |
goal Set.thy "A Int B = B Int A"; |
|
50 |
by (fast_tac eq_cs 1); |
|
171 | 51 |
qed "Int_commute"; |
0 | 52 |
|
53 |
goal Set.thy "(A Int B) Int C = A Int (B Int C)"; |
|
54 |
by (fast_tac eq_cs 1); |
|
171 | 55 |
qed "Int_assoc"; |
0 | 56 |
|
57 |
goal Set.thy "{} Int B = {}"; |
|
58 |
by (fast_tac eq_cs 1); |
|
171 | 59 |
qed "Int_empty_left"; |
0 | 60 |
|
61 |
goal Set.thy "A Int {} = {}"; |
|
62 |
by (fast_tac eq_cs 1); |
|
171 | 63 |
qed "Int_empty_right"; |
0 | 64 |
|
205 | 65 |
goal Set.thy "A Int (B Un C) = (A Int B) Un (A Int C)"; |
0 | 66 |
by (fast_tac eq_cs 1); |
171 | 67 |
qed "Int_Un_distrib"; |
0 | 68 |
|
69 |
goal Set.thy "(A<=B) = (A Int B = A)"; |
|
70 |
by (fast_tac (eq_cs addSEs [equalityE]) 1); |
|
171 | 71 |
qed "subset_Int_eq"; |
0 | 72 |
|
73 |
(** Binary Union **) |
|
74 |
||
75 |
goal Set.thy "A Un A = A"; |
|
76 |
by (fast_tac eq_cs 1); |
|
171 | 77 |
qed "Un_absorb"; |
0 | 78 |
|
79 |
goal Set.thy "A Un B = B Un A"; |
|
80 |
by (fast_tac eq_cs 1); |
|
171 | 81 |
qed "Un_commute"; |
0 | 82 |
|
83 |
goal Set.thy "(A Un B) Un C = A Un (B Un C)"; |
|
84 |
by (fast_tac eq_cs 1); |
|
171 | 85 |
qed "Un_assoc"; |
0 | 86 |
|
87 |
goal Set.thy "{} Un B = B"; |
|
88 |
by(fast_tac eq_cs 1); |
|
171 | 89 |
qed "Un_empty_left"; |
0 | 90 |
|
91 |
goal Set.thy "A Un {} = A"; |
|
92 |
by(fast_tac eq_cs 1); |
|
171 | 93 |
qed "Un_empty_right"; |
0 | 94 |
|
95 |
goal Set.thy "insert(a,B) Un C = insert(a,B Un C)"; |
|
96 |
by(fast_tac eq_cs 1); |
|
171 | 97 |
qed "Un_insert_left"; |
0 | 98 |
|
99 |
goal Set.thy "(A Int B) Un C = (A Un C) Int (B Un C)"; |
|
100 |
by (fast_tac eq_cs 1); |
|
171 | 101 |
qed "Un_Int_distrib"; |
0 | 102 |
|
103 |
goal Set.thy |
|
104 |
"(A Int B) Un (B Int C) Un (C Int A) = (A Un B) Int (B Un C) Int (C Un A)"; |
|
105 |
by (fast_tac eq_cs 1); |
|
171 | 106 |
qed "Un_Int_crazy"; |
0 | 107 |
|
108 |
goal Set.thy "(A<=B) = (A Un B = B)"; |
|
109 |
by (fast_tac (eq_cs addSEs [equalityE]) 1); |
|
171 | 110 |
qed "subset_Un_eq"; |
0 | 111 |
|
112 |
goal Set.thy "(A <= insert(b,C)) = (A <= C | b:A & A-{b} <= C)"; |
|
113 |
by (fast_tac eq_cs 1); |
|
171 | 114 |
qed "subset_insert_iff"; |
0 | 115 |
|
205 | 116 |
goal Set.thy "(A Un B = {}) = (A = {} & B = {})"; |
117 |
by (fast_tac (eq_cs addEs [equalityCE]) 1); |
|
118 |
qed "Un_empty"; |
|
119 |
||
0 | 120 |
(** Simple properties of Compl -- complement of a set **) |
121 |
||
122 |
goal Set.thy "A Int Compl(A) = {}"; |
|
123 |
by (fast_tac eq_cs 1); |
|
171 | 124 |
qed "Compl_disjoint"; |
0 | 125 |
|
126 |
goal Set.thy "A Un Compl(A) = {x.True}"; |
|
127 |
by (fast_tac eq_cs 1); |
|
171 | 128 |
qed "Compl_partition"; |
0 | 129 |
|
130 |
goal Set.thy "Compl(Compl(A)) = A"; |
|
131 |
by (fast_tac eq_cs 1); |
|
171 | 132 |
qed "double_complement"; |
0 | 133 |
|
134 |
goal Set.thy "Compl(A Un B) = Compl(A) Int Compl(B)"; |
|
135 |
by (fast_tac eq_cs 1); |
|
171 | 136 |
qed "Compl_Un"; |
0 | 137 |
|
138 |
goal Set.thy "Compl(A Int B) = Compl(A) Un Compl(B)"; |
|
139 |
by (fast_tac eq_cs 1); |
|
171 | 140 |
qed "Compl_Int"; |
0 | 141 |
|
142 |
goal Set.thy "Compl(UN x:A. B(x)) = (INT x:A. Compl(B(x)))"; |
|
143 |
by (fast_tac eq_cs 1); |
|
171 | 144 |
qed "Compl_UN"; |
0 | 145 |
|
146 |
goal Set.thy "Compl(INT x:A. B(x)) = (UN x:A. Compl(B(x)))"; |
|
147 |
by (fast_tac eq_cs 1); |
|
171 | 148 |
qed "Compl_INT"; |
0 | 149 |
|
150 |
(*Halmos, Naive Set Theory, page 16.*) |
|
151 |
||
152 |
goal Set.thy "((A Int B) Un C = A Int (B Un C)) = (C<=A)"; |
|
153 |
by (fast_tac (eq_cs addSEs [equalityE]) 1); |
|
171 | 154 |
qed "Un_Int_assoc_eq"; |
0 | 155 |
|
156 |
||
157 |
(** Big Union and Intersection **) |
|
158 |
||
159 |
goal Set.thy "Union({}) = {}"; |
|
160 |
by (fast_tac eq_cs 1); |
|
171 | 161 |
qed "Union_empty"; |
0 | 162 |
|
163 |
goal Set.thy "Union(insert(a,B)) = a Un Union(B)"; |
|
164 |
by (fast_tac eq_cs 1); |
|
171 | 165 |
qed "Union_insert"; |
0 | 166 |
|
167 |
goal Set.thy "Union(A Un B) = Union(A) Un Union(B)"; |
|
168 |
by (fast_tac eq_cs 1); |
|
171 | 169 |
qed "Union_Un_distrib"; |
0 | 170 |
|
76
fb4fe9f8c3cd
HOL/equalities: added some identities from ZF/equalities
lcp
parents:
57
diff
changeset
|
171 |
goal Set.thy "Union(A Int B) <= Union(A) Int Union(B)"; |
fb4fe9f8c3cd
HOL/equalities: added some identities from ZF/equalities
lcp
parents:
57
diff
changeset
|
172 |
by (fast_tac set_cs 1); |
171 | 173 |
qed "Union_Int_subset"; |
0 | 174 |
|
175 |
val prems = goal Set.thy |
|
176 |
"(Union(C) Int A = {}) = (! B:C. B Int A = {})"; |
|
177 |
by (fast_tac (eq_cs addSEs [equalityE]) 1); |
|
171 | 178 |
qed "Union_disjoint"; |
0 | 179 |
|
180 |
goal Set.thy "Inter(A Un B) = Inter(A) Int Inter(B)"; |
|
181 |
by (best_tac eq_cs 1); |
|
171 | 182 |
qed "Inter_Un_distrib"; |
0 | 183 |
|
184 |
(** Unions and Intersections of Families **) |
|
185 |
||
76
fb4fe9f8c3cd
HOL/equalities: added some identities from ZF/equalities
lcp
parents:
57
diff
changeset
|
186 |
(*Basic identities*) |
0 | 187 |
|
188 |
goal Set.thy "Union(range(f)) = (UN x.f(x))"; |
|
189 |
by (fast_tac eq_cs 1); |
|
171 | 190 |
qed "Union_range_eq"; |
0 | 191 |
|
192 |
goal Set.thy "Inter(range(f)) = (INT x.f(x))"; |
|
193 |
by (fast_tac eq_cs 1); |
|
171 | 194 |
qed "Inter_range_eq"; |
0 | 195 |
|
196 |
goal Set.thy "Union(B``A) = (UN x:A. B(x))"; |
|
197 |
by (fast_tac eq_cs 1); |
|
171 | 198 |
qed "Union_image_eq"; |
0 | 199 |
|
200 |
goal Set.thy "Inter(B``A) = (INT x:A. B(x))"; |
|
201 |
by (fast_tac eq_cs 1); |
|
171 | 202 |
qed "Inter_image_eq"; |
0 | 203 |
|
76
fb4fe9f8c3cd
HOL/equalities: added some identities from ZF/equalities
lcp
parents:
57
diff
changeset
|
204 |
goal Set.thy "!!A. a: A ==> (UN y:A. c) = c"; |
fb4fe9f8c3cd
HOL/equalities: added some identities from ZF/equalities
lcp
parents:
57
diff
changeset
|
205 |
by (fast_tac eq_cs 1); |
171 | 206 |
qed "UN_constant"; |
76
fb4fe9f8c3cd
HOL/equalities: added some identities from ZF/equalities
lcp
parents:
57
diff
changeset
|
207 |
|
fb4fe9f8c3cd
HOL/equalities: added some identities from ZF/equalities
lcp
parents:
57
diff
changeset
|
208 |
goal Set.thy "!!A. a: A ==> (INT y:A. c) = c"; |
fb4fe9f8c3cd
HOL/equalities: added some identities from ZF/equalities
lcp
parents:
57
diff
changeset
|
209 |
by (fast_tac eq_cs 1); |
171 | 210 |
qed "INT_constant"; |
76
fb4fe9f8c3cd
HOL/equalities: added some identities from ZF/equalities
lcp
parents:
57
diff
changeset
|
211 |
|
0 | 212 |
goal Set.thy "(UN x.B) = B"; |
213 |
by (fast_tac eq_cs 1); |
|
171 | 214 |
qed "UN1_constant"; |
76
fb4fe9f8c3cd
HOL/equalities: added some identities from ZF/equalities
lcp
parents:
57
diff
changeset
|
215 |
|
fb4fe9f8c3cd
HOL/equalities: added some identities from ZF/equalities
lcp
parents:
57
diff
changeset
|
216 |
goal Set.thy "(INT x.B) = B"; |
fb4fe9f8c3cd
HOL/equalities: added some identities from ZF/equalities
lcp
parents:
57
diff
changeset
|
217 |
by (fast_tac eq_cs 1); |
171 | 218 |
qed "INT1_constant"; |
76
fb4fe9f8c3cd
HOL/equalities: added some identities from ZF/equalities
lcp
parents:
57
diff
changeset
|
219 |
|
fb4fe9f8c3cd
HOL/equalities: added some identities from ZF/equalities
lcp
parents:
57
diff
changeset
|
220 |
goal Set.thy "(UN x:A. B(x)) = Union({Y. ? x:A. Y=B(x)})"; |
fb4fe9f8c3cd
HOL/equalities: added some identities from ZF/equalities
lcp
parents:
57
diff
changeset
|
221 |
by (fast_tac eq_cs 1); |
171 | 222 |
qed "UN_eq"; |
76
fb4fe9f8c3cd
HOL/equalities: added some identities from ZF/equalities
lcp
parents:
57
diff
changeset
|
223 |
|
fb4fe9f8c3cd
HOL/equalities: added some identities from ZF/equalities
lcp
parents:
57
diff
changeset
|
224 |
(*Look: it has an EXISTENTIAL quantifier*) |
fb4fe9f8c3cd
HOL/equalities: added some identities from ZF/equalities
lcp
parents:
57
diff
changeset
|
225 |
goal Set.thy "(INT x:A. B(x)) = Inter({Y. ? x:A. Y=B(x)})"; |
fb4fe9f8c3cd
HOL/equalities: added some identities from ZF/equalities
lcp
parents:
57
diff
changeset
|
226 |
by (fast_tac eq_cs 1); |
171 | 227 |
qed "INT_eq"; |
76
fb4fe9f8c3cd
HOL/equalities: added some identities from ZF/equalities
lcp
parents:
57
diff
changeset
|
228 |
|
fb4fe9f8c3cd
HOL/equalities: added some identities from ZF/equalities
lcp
parents:
57
diff
changeset
|
229 |
(*Distributive laws...*) |
fb4fe9f8c3cd
HOL/equalities: added some identities from ZF/equalities
lcp
parents:
57
diff
changeset
|
230 |
|
fb4fe9f8c3cd
HOL/equalities: added some identities from ZF/equalities
lcp
parents:
57
diff
changeset
|
231 |
goal Set.thy "A Int Union(B) = (UN C:B. A Int C)"; |
fb4fe9f8c3cd
HOL/equalities: added some identities from ZF/equalities
lcp
parents:
57
diff
changeset
|
232 |
by (fast_tac eq_cs 1); |
171 | 233 |
qed "Int_Union"; |
76
fb4fe9f8c3cd
HOL/equalities: added some identities from ZF/equalities
lcp
parents:
57
diff
changeset
|
234 |
|
fb4fe9f8c3cd
HOL/equalities: added some identities from ZF/equalities
lcp
parents:
57
diff
changeset
|
235 |
(* Devlin, Fundamentals of Contemporary Set Theory, page 12, exercise 5: |
fb4fe9f8c3cd
HOL/equalities: added some identities from ZF/equalities
lcp
parents:
57
diff
changeset
|
236 |
Union of a family of unions **) |
fb4fe9f8c3cd
HOL/equalities: added some identities from ZF/equalities
lcp
parents:
57
diff
changeset
|
237 |
goal Set.thy "(UN x:C. A(x) Un B(x)) = Union(A``C) Un Union(B``C)"; |
fb4fe9f8c3cd
HOL/equalities: added some identities from ZF/equalities
lcp
parents:
57
diff
changeset
|
238 |
by (fast_tac eq_cs 1); |
171 | 239 |
qed "Un_Union_image"; |
76
fb4fe9f8c3cd
HOL/equalities: added some identities from ZF/equalities
lcp
parents:
57
diff
changeset
|
240 |
|
fb4fe9f8c3cd
HOL/equalities: added some identities from ZF/equalities
lcp
parents:
57
diff
changeset
|
241 |
(*Equivalent version*) |
fb4fe9f8c3cd
HOL/equalities: added some identities from ZF/equalities
lcp
parents:
57
diff
changeset
|
242 |
goal Set.thy "(UN i:I. A(i) Un B(i)) = (UN i:I. A(i)) Un (UN i:I. B(i))"; |
fb4fe9f8c3cd
HOL/equalities: added some identities from ZF/equalities
lcp
parents:
57
diff
changeset
|
243 |
by (fast_tac eq_cs 1); |
171 | 244 |
qed "UN_Un_distrib"; |
76
fb4fe9f8c3cd
HOL/equalities: added some identities from ZF/equalities
lcp
parents:
57
diff
changeset
|
245 |
|
fb4fe9f8c3cd
HOL/equalities: added some identities from ZF/equalities
lcp
parents:
57
diff
changeset
|
246 |
goal Set.thy "A Un Inter(B) = (INT C:B. A Un C)"; |
fb4fe9f8c3cd
HOL/equalities: added some identities from ZF/equalities
lcp
parents:
57
diff
changeset
|
247 |
by (fast_tac eq_cs 1); |
171 | 248 |
qed "Un_Inter"; |
76
fb4fe9f8c3cd
HOL/equalities: added some identities from ZF/equalities
lcp
parents:
57
diff
changeset
|
249 |
|
fb4fe9f8c3cd
HOL/equalities: added some identities from ZF/equalities
lcp
parents:
57
diff
changeset
|
250 |
goal Set.thy "(INT x:C. A(x) Int B(x)) = Inter(A``C) Int Inter(B``C)"; |
fb4fe9f8c3cd
HOL/equalities: added some identities from ZF/equalities
lcp
parents:
57
diff
changeset
|
251 |
by (best_tac eq_cs 1); |
171 | 252 |
qed "Int_Inter_image"; |
76
fb4fe9f8c3cd
HOL/equalities: added some identities from ZF/equalities
lcp
parents:
57
diff
changeset
|
253 |
|
fb4fe9f8c3cd
HOL/equalities: added some identities from ZF/equalities
lcp
parents:
57
diff
changeset
|
254 |
(*Equivalent version*) |
fb4fe9f8c3cd
HOL/equalities: added some identities from ZF/equalities
lcp
parents:
57
diff
changeset
|
255 |
goal Set.thy "(INT i:I. A(i) Int B(i)) = (INT i:I. A(i)) Int (INT i:I. B(i))"; |
fb4fe9f8c3cd
HOL/equalities: added some identities from ZF/equalities
lcp
parents:
57
diff
changeset
|
256 |
by (fast_tac eq_cs 1); |
171 | 257 |
qed "INT_Int_distrib"; |
76
fb4fe9f8c3cd
HOL/equalities: added some identities from ZF/equalities
lcp
parents:
57
diff
changeset
|
258 |
|
fb4fe9f8c3cd
HOL/equalities: added some identities from ZF/equalities
lcp
parents:
57
diff
changeset
|
259 |
(*Halmos, Naive Set Theory, page 35.*) |
fb4fe9f8c3cd
HOL/equalities: added some identities from ZF/equalities
lcp
parents:
57
diff
changeset
|
260 |
goal Set.thy "B Int (UN i:I. A(i)) = (UN i:I. B Int A(i))"; |
fb4fe9f8c3cd
HOL/equalities: added some identities from ZF/equalities
lcp
parents:
57
diff
changeset
|
261 |
by (fast_tac eq_cs 1); |
171 | 262 |
qed "Int_UN_distrib"; |
76
fb4fe9f8c3cd
HOL/equalities: added some identities from ZF/equalities
lcp
parents:
57
diff
changeset
|
263 |
|
fb4fe9f8c3cd
HOL/equalities: added some identities from ZF/equalities
lcp
parents:
57
diff
changeset
|
264 |
goal Set.thy "B Un (INT i:I. A(i)) = (INT i:I. B Un A(i))"; |
fb4fe9f8c3cd
HOL/equalities: added some identities from ZF/equalities
lcp
parents:
57
diff
changeset
|
265 |
by (fast_tac eq_cs 1); |
171 | 266 |
qed "Un_INT_distrib"; |
76
fb4fe9f8c3cd
HOL/equalities: added some identities from ZF/equalities
lcp
parents:
57
diff
changeset
|
267 |
|
fb4fe9f8c3cd
HOL/equalities: added some identities from ZF/equalities
lcp
parents:
57
diff
changeset
|
268 |
goal Set.thy |
fb4fe9f8c3cd
HOL/equalities: added some identities from ZF/equalities
lcp
parents:
57
diff
changeset
|
269 |
"(UN i:I. A(i)) Int (UN j:J. B(j)) = (UN i:I. UN j:J. A(i) Int B(j))"; |
fb4fe9f8c3cd
HOL/equalities: added some identities from ZF/equalities
lcp
parents:
57
diff
changeset
|
270 |
by (fast_tac eq_cs 1); |
171 | 271 |
qed "Int_UN_distrib2"; |
76
fb4fe9f8c3cd
HOL/equalities: added some identities from ZF/equalities
lcp
parents:
57
diff
changeset
|
272 |
|
fb4fe9f8c3cd
HOL/equalities: added some identities from ZF/equalities
lcp
parents:
57
diff
changeset
|
273 |
goal Set.thy |
fb4fe9f8c3cd
HOL/equalities: added some identities from ZF/equalities
lcp
parents:
57
diff
changeset
|
274 |
"(INT i:I. A(i)) Un (INT j:J. B(j)) = (INT i:I. INT j:J. A(i) Un B(j))"; |
fb4fe9f8c3cd
HOL/equalities: added some identities from ZF/equalities
lcp
parents:
57
diff
changeset
|
275 |
by (fast_tac eq_cs 1); |
171 | 276 |
qed "Un_INT_distrib2"; |
0 | 277 |
|
278 |
(** Simple properties of Diff -- set difference **) |
|
279 |
||
280 |
goal Set.thy "A-A = {}"; |
|
281 |
by (fast_tac eq_cs 1); |
|
171 | 282 |
qed "Diff_cancel"; |
0 | 283 |
|
284 |
goal Set.thy "{}-A = {}"; |
|
285 |
by (fast_tac eq_cs 1); |
|
171 | 286 |
qed "empty_Diff"; |
0 | 287 |
|
288 |
goal Set.thy "A-{} = A"; |
|
289 |
by (fast_tac eq_cs 1); |
|
171 | 290 |
qed "Diff_empty"; |
0 | 291 |
|
292 |
(*NOT SUITABLE FOR REWRITING since {a} == insert(a,0)*) |
|
293 |
goal Set.thy "A - insert(a,B) = A - B - {a}"; |
|
294 |
by (fast_tac eq_cs 1); |
|
171 | 295 |
qed "Diff_insert"; |
0 | 296 |
|
297 |
(*NOT SUITABLE FOR REWRITING since {a} == insert(a,0)*) |
|
298 |
goal Set.thy "A - insert(a,B) = A - {a} - B"; |
|
299 |
by (fast_tac eq_cs 1); |
|
171 | 300 |
qed "Diff_insert2"; |
0 | 301 |
|
302 |
val prems = goal Set.thy "a:A ==> insert(a,A-{a}) = A"; |
|
303 |
by (fast_tac (eq_cs addSIs prems) 1); |
|
171 | 304 |
qed "insert_Diff"; |
0 | 305 |
|
306 |
goal Set.thy "A Int (B-A) = {}"; |
|
307 |
by (fast_tac eq_cs 1); |
|
171 | 308 |
qed "Diff_disjoint"; |
0 | 309 |
|
310 |
goal Set.thy "!!A. A<=B ==> A Un (B-A) = B"; |
|
311 |
by (fast_tac eq_cs 1); |
|
171 | 312 |
qed "Diff_partition"; |
76
fb4fe9f8c3cd
HOL/equalities: added some identities from ZF/equalities
lcp
parents:
57
diff
changeset
|
313 |
|
90
5c7a69cef18b
added parentheses made necessary by change of constrain's precedence
clasohm
parents:
76
diff
changeset
|
314 |
goal Set.thy "!!A. [| A<=B; B<= C |] ==> (B - (C - A)) = (A :: 'a set)"; |
0 | 315 |
by (fast_tac eq_cs 1); |
171 | 316 |
qed "double_diff"; |
76
fb4fe9f8c3cd
HOL/equalities: added some identities from ZF/equalities
lcp
parents:
57
diff
changeset
|
317 |
|
0 | 318 |
goal Set.thy "A - (B Un C) = (A-B) Int (A-C)"; |
319 |
by (fast_tac eq_cs 1); |
|
171 | 320 |
qed "Diff_Un"; |
0 | 321 |
|
322 |
goal Set.thy "A - (B Int C) = (A-B) Un (A-C)"; |
|
323 |
by (fast_tac eq_cs 1); |
|
171 | 324 |
qed "Diff_Int"; |
0 | 325 |
|
326 |
val set_ss = set_ss addsimps |
|
57 | 327 |
[in_empty,in_insert,insert_subset, |
27 | 328 |
Int_absorb,Int_empty_left,Int_empty_right, |
205 | 329 |
Un_absorb,Un_empty_left,Un_empty_right,Un_empty, |
76
fb4fe9f8c3cd
HOL/equalities: added some identities from ZF/equalities
lcp
parents:
57
diff
changeset
|
330 |
UN1_constant,image_empty, |
0 | 331 |
Compl_disjoint,double_complement, |
332 |
Union_empty,Union_insert,empty_subsetI,subset_refl, |
|
333 |
Diff_cancel,empty_Diff,Diff_empty,Diff_disjoint]; |