author | nipkow |
Mon, 04 Mar 1996 14:37:33 +0100 | |
changeset 1531 | e5eb247ad13c |
parent 1465 | 5d7a7e439cec |
child 1548 | afe750876848 |
permissions | -rw-r--r-- |
1465 | 1 |
(* Title: HOL/equalities |
923 | 2 |
ID: $Id$ |
1465 | 3 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
923 | 4 |
Copyright 1994 University of Cambridge |
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 |
||
1531 | 13 |
goal Set.thy "{x.False} = {}"; |
14 |
by(fast_tac eq_cs 1); |
|
15 |
qed "Collect_False_empty"; |
|
16 |
Addsimps [Collect_False_empty]; |
|
17 |
||
18 |
goal Set.thy "(A <= {}) = (A = {})"; |
|
19 |
by(fast_tac eq_cs 1); |
|
20 |
qed "subset_empty"; |
|
21 |
Addsimps [subset_empty]; |
|
22 |
||
923 | 23 |
(** The membership relation, : **) |
24 |
||
25 |
goal Set.thy "x ~: {}"; |
|
26 |
by(fast_tac set_cs 1); |
|
27 |
qed "in_empty"; |
|
1531 | 28 |
Addsimps[in_empty]; |
923 | 29 |
|
30 |
goal Set.thy "x : insert y A = (x=y | x:A)"; |
|
31 |
by(fast_tac set_cs 1); |
|
32 |
qed "in_insert"; |
|
1531 | 33 |
Addsimps[in_insert]; |
923 | 34 |
|
35 |
(** insert **) |
|
36 |
||
1531 | 37 |
(*NOT SUITABLE FOR REWRITING since {a} == insert a {}*) |
38 |
goal Set.thy "insert a A = {a} Un A"; |
|
39 |
by(fast_tac eq_cs 1); |
|
40 |
qed "insert_is_Un"; |
|
41 |
||
1179
7678408f9751
Added insert_not_empty, UN_empty and UN_insert (to set_ss).
nipkow
parents:
923
diff
changeset
|
42 |
goal Set.thy "insert a A ~= {}"; |
7678408f9751
Added insert_not_empty, UN_empty and UN_insert (to set_ss).
nipkow
parents:
923
diff
changeset
|
43 |
by (fast_tac (set_cs addEs [equalityCE]) 1); |
7678408f9751
Added insert_not_empty, UN_empty and UN_insert (to set_ss).
nipkow
parents:
923
diff
changeset
|
44 |
qed"insert_not_empty"; |
1531 | 45 |
Addsimps[insert_not_empty]; |
1179
7678408f9751
Added insert_not_empty, UN_empty and UN_insert (to set_ss).
nipkow
parents:
923
diff
changeset
|
46 |
|
7678408f9751
Added insert_not_empty, UN_empty and UN_insert (to set_ss).
nipkow
parents:
923
diff
changeset
|
47 |
bind_thm("empty_not_insert",insert_not_empty RS not_sym); |
1531 | 48 |
Addsimps[empty_not_insert]; |
1179
7678408f9751
Added insert_not_empty, UN_empty and UN_insert (to set_ss).
nipkow
parents:
923
diff
changeset
|
49 |
|
923 | 50 |
goal Set.thy "!!a. a:A ==> insert a A = A"; |
51 |
by (fast_tac eq_cs 1); |
|
52 |
qed "insert_absorb"; |
|
53 |
||
1531 | 54 |
goal Set.thy "insert x (insert x A) = insert x A"; |
55 |
by(fast_tac eq_cs 1); |
|
56 |
qed "insert_absorb2"; |
|
57 |
Addsimps [insert_absorb2]; |
|
58 |
||
923 | 59 |
goal Set.thy "(insert x A <= B) = (x:B & A <= B)"; |
60 |
by (fast_tac set_cs 1); |
|
61 |
qed "insert_subset"; |
|
1531 | 62 |
Addsimps[insert_subset]; |
63 |
||
64 |
(* use new B rather than (A-{a}) to avoid infinite unfolding *) |
|
65 |
goal Set.thy "!!a. a:A ==> ? B. A = insert a B & a ~: B"; |
|
66 |
by(res_inst_tac [("x","A-{a}")] exI 1); |
|
67 |
by(fast_tac eq_cs 1); |
|
68 |
qed "mk_disjoint_insert"; |
|
923 | 69 |
|
70 |
(** Image **) |
|
71 |
||
72 |
goal Set.thy "f``{} = {}"; |
|
73 |
by (fast_tac eq_cs 1); |
|
74 |
qed "image_empty"; |
|
1531 | 75 |
Addsimps[image_empty]; |
923 | 76 |
|
77 |
goal Set.thy "f``insert a B = insert (f a) (f``B)"; |
|
78 |
by (fast_tac eq_cs 1); |
|
79 |
qed "image_insert"; |
|
1531 | 80 |
Addsimps[image_insert]; |
923 | 81 |
|
82 |
(** Binary Intersection **) |
|
83 |
||
84 |
goal Set.thy "A Int A = A"; |
|
85 |
by (fast_tac eq_cs 1); |
|
86 |
qed "Int_absorb"; |
|
1531 | 87 |
Addsimps[Int_absorb]; |
923 | 88 |
|
89 |
goal Set.thy "A Int B = B Int A"; |
|
90 |
by (fast_tac eq_cs 1); |
|
91 |
qed "Int_commute"; |
|
92 |
||
93 |
goal Set.thy "(A Int B) Int C = A Int (B Int C)"; |
|
94 |
by (fast_tac eq_cs 1); |
|
95 |
qed "Int_assoc"; |
|
96 |
||
97 |
goal Set.thy "{} Int B = {}"; |
|
98 |
by (fast_tac eq_cs 1); |
|
99 |
qed "Int_empty_left"; |
|
1531 | 100 |
Addsimps[Int_empty_left]; |
923 | 101 |
|
102 |
goal Set.thy "A Int {} = {}"; |
|
103 |
by (fast_tac eq_cs 1); |
|
104 |
qed "Int_empty_right"; |
|
1531 | 105 |
Addsimps[Int_empty_right]; |
106 |
||
107 |
goal Set.thy "UNIV Int B = B"; |
|
108 |
by (fast_tac eq_cs 1); |
|
109 |
qed "Int_UNIV_left"; |
|
110 |
Addsimps[Int_UNIV_left]; |
|
111 |
||
112 |
goal Set.thy "A Int UNIV = A"; |
|
113 |
by (fast_tac eq_cs 1); |
|
114 |
qed "Int_UNIV_right"; |
|
115 |
Addsimps[Int_UNIV_right]; |
|
923 | 116 |
|
117 |
goal Set.thy "A Int (B Un C) = (A Int B) Un (A Int C)"; |
|
118 |
by (fast_tac eq_cs 1); |
|
119 |
qed "Int_Un_distrib"; |
|
120 |
||
121 |
goal Set.thy "(A<=B) = (A Int B = A)"; |
|
122 |
by (fast_tac (eq_cs addSEs [equalityE]) 1); |
|
123 |
qed "subset_Int_eq"; |
|
124 |
||
1531 | 125 |
goal Set.thy "(A Int B = UNIV) = (A = UNIV & B = UNIV)"; |
126 |
by (fast_tac (eq_cs addEs [equalityCE]) 1); |
|
127 |
qed "Int_UNIV"; |
|
128 |
Addsimps[Int_UNIV]; |
|
129 |
||
923 | 130 |
(** Binary Union **) |
131 |
||
132 |
goal Set.thy "A Un A = A"; |
|
133 |
by (fast_tac eq_cs 1); |
|
134 |
qed "Un_absorb"; |
|
1531 | 135 |
Addsimps[Un_absorb]; |
923 | 136 |
|
137 |
goal Set.thy "A Un B = B Un A"; |
|
138 |
by (fast_tac eq_cs 1); |
|
139 |
qed "Un_commute"; |
|
140 |
||
141 |
goal Set.thy "(A Un B) Un C = A Un (B Un C)"; |
|
142 |
by (fast_tac eq_cs 1); |
|
143 |
qed "Un_assoc"; |
|
144 |
||
145 |
goal Set.thy "{} Un B = B"; |
|
146 |
by(fast_tac eq_cs 1); |
|
147 |
qed "Un_empty_left"; |
|
1531 | 148 |
Addsimps[Un_empty_left]; |
923 | 149 |
|
150 |
goal Set.thy "A Un {} = A"; |
|
151 |
by(fast_tac eq_cs 1); |
|
152 |
qed "Un_empty_right"; |
|
1531 | 153 |
Addsimps[Un_empty_right]; |
154 |
||
155 |
goal Set.thy "UNIV Un B = UNIV"; |
|
156 |
by(fast_tac eq_cs 1); |
|
157 |
qed "Un_UNIV_left"; |
|
158 |
Addsimps[Un_UNIV_left]; |
|
159 |
||
160 |
goal Set.thy "A Un UNIV = UNIV"; |
|
161 |
by(fast_tac eq_cs 1); |
|
162 |
qed "Un_UNIV_right"; |
|
163 |
Addsimps[Un_UNIV_right]; |
|
923 | 164 |
|
165 |
goal Set.thy "insert a B Un C = insert a (B Un C)"; |
|
166 |
by(fast_tac eq_cs 1); |
|
167 |
qed "Un_insert_left"; |
|
168 |
||
169 |
goal Set.thy "(A Int B) Un C = (A Un C) Int (B Un C)"; |
|
170 |
by (fast_tac eq_cs 1); |
|
171 |
qed "Un_Int_distrib"; |
|
172 |
||
173 |
goal Set.thy |
|
174 |
"(A Int B) Un (B Int C) Un (C Int A) = (A Un B) Int (B Un C) Int (C Un A)"; |
|
175 |
by (fast_tac eq_cs 1); |
|
176 |
qed "Un_Int_crazy"; |
|
177 |
||
178 |
goal Set.thy "(A<=B) = (A Un B = B)"; |
|
179 |
by (fast_tac (eq_cs addSEs [equalityE]) 1); |
|
180 |
qed "subset_Un_eq"; |
|
181 |
||
182 |
goal Set.thy "(A <= insert b C) = (A <= C | b:A & A-{b} <= C)"; |
|
183 |
by (fast_tac eq_cs 1); |
|
184 |
qed "subset_insert_iff"; |
|
185 |
||
186 |
goal Set.thy "(A Un B = {}) = (A = {} & B = {})"; |
|
187 |
by (fast_tac (eq_cs addEs [equalityCE]) 1); |
|
188 |
qed "Un_empty"; |
|
1531 | 189 |
Addsimps[Un_empty]; |
923 | 190 |
|
191 |
(** Simple properties of Compl -- complement of a set **) |
|
192 |
||
193 |
goal Set.thy "A Int Compl(A) = {}"; |
|
194 |
by (fast_tac eq_cs 1); |
|
195 |
qed "Compl_disjoint"; |
|
1531 | 196 |
Addsimps[Compl_disjoint]; |
923 | 197 |
|
1531 | 198 |
goal Set.thy "A Un Compl(A) = UNIV"; |
923 | 199 |
by (fast_tac eq_cs 1); |
200 |
qed "Compl_partition"; |
|
201 |
||
202 |
goal Set.thy "Compl(Compl(A)) = A"; |
|
203 |
by (fast_tac eq_cs 1); |
|
204 |
qed "double_complement"; |
|
1531 | 205 |
Addsimps[double_complement]; |
923 | 206 |
|
207 |
goal Set.thy "Compl(A Un B) = Compl(A) Int Compl(B)"; |
|
208 |
by (fast_tac eq_cs 1); |
|
209 |
qed "Compl_Un"; |
|
210 |
||
211 |
goal Set.thy "Compl(A Int B) = Compl(A) Un Compl(B)"; |
|
212 |
by (fast_tac eq_cs 1); |
|
213 |
qed "Compl_Int"; |
|
214 |
||
215 |
goal Set.thy "Compl(UN x:A. B(x)) = (INT x:A. Compl(B(x)))"; |
|
216 |
by (fast_tac eq_cs 1); |
|
217 |
qed "Compl_UN"; |
|
218 |
||
219 |
goal Set.thy "Compl(INT x:A. B(x)) = (UN x:A. Compl(B(x)))"; |
|
220 |
by (fast_tac eq_cs 1); |
|
221 |
qed "Compl_INT"; |
|
222 |
||
223 |
(*Halmos, Naive Set Theory, page 16.*) |
|
224 |
||
225 |
goal Set.thy "((A Int B) Un C = A Int (B Un C)) = (C<=A)"; |
|
226 |
by (fast_tac (eq_cs addSEs [equalityE]) 1); |
|
227 |
qed "Un_Int_assoc_eq"; |
|
228 |
||
229 |
||
230 |
(** Big Union and Intersection **) |
|
231 |
||
232 |
goal Set.thy "Union({}) = {}"; |
|
233 |
by (fast_tac eq_cs 1); |
|
234 |
qed "Union_empty"; |
|
1531 | 235 |
Addsimps[Union_empty]; |
236 |
||
237 |
goal Set.thy "Union(UNIV) = UNIV"; |
|
238 |
by (fast_tac eq_cs 1); |
|
239 |
qed "Union_UNIV"; |
|
240 |
Addsimps[Union_UNIV]; |
|
923 | 241 |
|
242 |
goal Set.thy "Union(insert a B) = a Un Union(B)"; |
|
243 |
by (fast_tac eq_cs 1); |
|
244 |
qed "Union_insert"; |
|
1531 | 245 |
Addsimps[Union_insert]; |
923 | 246 |
|
247 |
goal Set.thy "Union(A Un B) = Union(A) Un Union(B)"; |
|
248 |
by (fast_tac eq_cs 1); |
|
249 |
qed "Union_Un_distrib"; |
|
1531 | 250 |
Addsimps[Union_Un_distrib]; |
923 | 251 |
|
252 |
goal Set.thy "Union(A Int B) <= Union(A) Int Union(B)"; |
|
253 |
by (fast_tac set_cs 1); |
|
254 |
qed "Union_Int_subset"; |
|
255 |
||
256 |
val prems = goal Set.thy |
|
257 |
"(Union(C) Int A = {}) = (! B:C. B Int A = {})"; |
|
258 |
by (fast_tac (eq_cs addSEs [equalityE]) 1); |
|
259 |
qed "Union_disjoint"; |
|
260 |
||
1531 | 261 |
goal Set.thy "Inter({}) = UNIV"; |
262 |
by (fast_tac eq_cs 1); |
|
263 |
qed "Inter_empty"; |
|
264 |
Addsimps[Inter_empty]; |
|
265 |
||
266 |
goal Set.thy "Inter(UNIV) = {}"; |
|
267 |
by (fast_tac eq_cs 1); |
|
268 |
qed "Inter_UNIV"; |
|
269 |
Addsimps[Inter_UNIV]; |
|
270 |
||
271 |
goal Set.thy "Inter(insert a B) = a Int Inter(B)"; |
|
272 |
by (fast_tac eq_cs 1); |
|
273 |
qed "Inter_insert"; |
|
274 |
Addsimps[Inter_insert]; |
|
275 |
||
276 |
(* Why does fast_tac fail??? |
|
277 |
goal Set.thy "Inter(A Int B) = Inter(A) Int Inter(B)"; |
|
278 |
by (fast_tac eq_cs 1); |
|
279 |
qed "Inter_Int_distrib"; |
|
280 |
Addsimps[Inter_Int_distrib]; |
|
281 |
*) |
|
282 |
||
923 | 283 |
goal Set.thy "Inter(A Un B) = Inter(A) Int Inter(B)"; |
284 |
by (best_tac eq_cs 1); |
|
285 |
qed "Inter_Un_distrib"; |
|
286 |
||
287 |
(** Unions and Intersections of Families **) |
|
288 |
||
289 |
(*Basic identities*) |
|
290 |
||
1179
7678408f9751
Added insert_not_empty, UN_empty and UN_insert (to set_ss).
nipkow
parents:
923
diff
changeset
|
291 |
goal Set.thy "(UN x:{}. B x) = {}"; |
7678408f9751
Added insert_not_empty, UN_empty and UN_insert (to set_ss).
nipkow
parents:
923
diff
changeset
|
292 |
by (fast_tac eq_cs 1); |
7678408f9751
Added insert_not_empty, UN_empty and UN_insert (to set_ss).
nipkow
parents:
923
diff
changeset
|
293 |
qed "UN_empty"; |
1531 | 294 |
Addsimps[UN_empty]; |
295 |
||
296 |
goal Set.thy "(UN x:UNIV. B x) = (UN x. B x)"; |
|
297 |
by (fast_tac eq_cs 1); |
|
298 |
qed "UN_UNIV"; |
|
299 |
Addsimps[UN_UNIV]; |
|
300 |
||
301 |
goal Set.thy "(INT x:{}. B x) = UNIV"; |
|
302 |
by (fast_tac eq_cs 1); |
|
303 |
qed "INT_empty"; |
|
304 |
Addsimps[INT_empty]; |
|
305 |
||
306 |
goal Set.thy "(INT x:UNIV. B x) = (INT x. B x)"; |
|
307 |
by (fast_tac eq_cs 1); |
|
308 |
qed "INT_UNIV"; |
|
309 |
Addsimps[INT_UNIV]; |
|
1179
7678408f9751
Added insert_not_empty, UN_empty and UN_insert (to set_ss).
nipkow
parents:
923
diff
changeset
|
310 |
|
7678408f9751
Added insert_not_empty, UN_empty and UN_insert (to set_ss).
nipkow
parents:
923
diff
changeset
|
311 |
goal Set.thy "(UN x:insert a A. B x) = B a Un UNION A B"; |
7678408f9751
Added insert_not_empty, UN_empty and UN_insert (to set_ss).
nipkow
parents:
923
diff
changeset
|
312 |
by (fast_tac eq_cs 1); |
7678408f9751
Added insert_not_empty, UN_empty and UN_insert (to set_ss).
nipkow
parents:
923
diff
changeset
|
313 |
qed "UN_insert"; |
1531 | 314 |
Addsimps[UN_insert]; |
315 |
||
316 |
goal Set.thy "(INT x:insert a A. B x) = B a Int INTER A B"; |
|
317 |
by (fast_tac eq_cs 1); |
|
318 |
qed "INT_insert"; |
|
319 |
Addsimps[INT_insert]; |
|
1179
7678408f9751
Added insert_not_empty, UN_empty and UN_insert (to set_ss).
nipkow
parents:
923
diff
changeset
|
320 |
|
923 | 321 |
goal Set.thy "Union(range(f)) = (UN x.f(x))"; |
322 |
by (fast_tac eq_cs 1); |
|
323 |
qed "Union_range_eq"; |
|
324 |
||
325 |
goal Set.thy "Inter(range(f)) = (INT x.f(x))"; |
|
326 |
by (fast_tac eq_cs 1); |
|
327 |
qed "Inter_range_eq"; |
|
328 |
||
329 |
goal Set.thy "Union(B``A) = (UN x:A. B(x))"; |
|
330 |
by (fast_tac eq_cs 1); |
|
331 |
qed "Union_image_eq"; |
|
332 |
||
333 |
goal Set.thy "Inter(B``A) = (INT x:A. B(x))"; |
|
334 |
by (fast_tac eq_cs 1); |
|
335 |
qed "Inter_image_eq"; |
|
336 |
||
337 |
goal Set.thy "!!A. a: A ==> (UN y:A. c) = c"; |
|
338 |
by (fast_tac eq_cs 1); |
|
339 |
qed "UN_constant"; |
|
340 |
||
341 |
goal Set.thy "!!A. a: A ==> (INT y:A. c) = c"; |
|
342 |
by (fast_tac eq_cs 1); |
|
343 |
qed "INT_constant"; |
|
344 |
||
345 |
goal Set.thy "(UN x.B) = B"; |
|
346 |
by (fast_tac eq_cs 1); |
|
347 |
qed "UN1_constant"; |
|
1531 | 348 |
Addsimps[UN1_constant]; |
923 | 349 |
|
350 |
goal Set.thy "(INT x.B) = B"; |
|
351 |
by (fast_tac eq_cs 1); |
|
352 |
qed "INT1_constant"; |
|
1531 | 353 |
Addsimps[INT1_constant]; |
923 | 354 |
|
355 |
goal Set.thy "(UN x:A. B(x)) = Union({Y. ? x:A. Y=B(x)})"; |
|
356 |
by (fast_tac eq_cs 1); |
|
357 |
qed "UN_eq"; |
|
358 |
||
359 |
(*Look: it has an EXISTENTIAL quantifier*) |
|
360 |
goal Set.thy "(INT x:A. B(x)) = Inter({Y. ? x:A. Y=B(x)})"; |
|
361 |
by (fast_tac eq_cs 1); |
|
362 |
qed "INT_eq"; |
|
363 |
||
364 |
(*Distributive laws...*) |
|
365 |
||
366 |
goal Set.thy "A Int Union(B) = (UN C:B. A Int C)"; |
|
367 |
by (fast_tac eq_cs 1); |
|
368 |
qed "Int_Union"; |
|
369 |
||
370 |
(* Devlin, Fundamentals of Contemporary Set Theory, page 12, exercise 5: |
|
371 |
Union of a family of unions **) |
|
372 |
goal Set.thy "(UN x:C. A(x) Un B(x)) = Union(A``C) Un Union(B``C)"; |
|
373 |
by (fast_tac eq_cs 1); |
|
374 |
qed "Un_Union_image"; |
|
375 |
||
376 |
(*Equivalent version*) |
|
377 |
goal Set.thy "(UN i:I. A(i) Un B(i)) = (UN i:I. A(i)) Un (UN i:I. B(i))"; |
|
378 |
by (fast_tac eq_cs 1); |
|
379 |
qed "UN_Un_distrib"; |
|
380 |
||
381 |
goal Set.thy "A Un Inter(B) = (INT C:B. A Un C)"; |
|
382 |
by (fast_tac eq_cs 1); |
|
383 |
qed "Un_Inter"; |
|
384 |
||
385 |
goal Set.thy "(INT x:C. A(x) Int B(x)) = Inter(A``C) Int Inter(B``C)"; |
|
386 |
by (best_tac eq_cs 1); |
|
387 |
qed "Int_Inter_image"; |
|
388 |
||
389 |
(*Equivalent version*) |
|
390 |
goal Set.thy "(INT i:I. A(i) Int B(i)) = (INT i:I. A(i)) Int (INT i:I. B(i))"; |
|
391 |
by (fast_tac eq_cs 1); |
|
392 |
qed "INT_Int_distrib"; |
|
393 |
||
394 |
(*Halmos, Naive Set Theory, page 35.*) |
|
395 |
goal Set.thy "B Int (UN i:I. A(i)) = (UN i:I. B Int A(i))"; |
|
396 |
by (fast_tac eq_cs 1); |
|
397 |
qed "Int_UN_distrib"; |
|
398 |
||
399 |
goal Set.thy "B Un (INT i:I. A(i)) = (INT i:I. B Un A(i))"; |
|
400 |
by (fast_tac eq_cs 1); |
|
401 |
qed "Un_INT_distrib"; |
|
402 |
||
403 |
goal Set.thy |
|
404 |
"(UN i:I. A(i)) Int (UN j:J. B(j)) = (UN i:I. UN j:J. A(i) Int B(j))"; |
|
405 |
by (fast_tac eq_cs 1); |
|
406 |
qed "Int_UN_distrib2"; |
|
407 |
||
408 |
goal Set.thy |
|
409 |
"(INT i:I. A(i)) Un (INT j:J. B(j)) = (INT i:I. INT j:J. A(i) Un B(j))"; |
|
410 |
by (fast_tac eq_cs 1); |
|
411 |
qed "Un_INT_distrib2"; |
|
412 |
||
413 |
(** Simple properties of Diff -- set difference **) |
|
414 |
||
415 |
goal Set.thy "A-A = {}"; |
|
416 |
by (fast_tac eq_cs 1); |
|
417 |
qed "Diff_cancel"; |
|
1531 | 418 |
Addsimps[Diff_cancel]; |
923 | 419 |
|
420 |
goal Set.thy "{}-A = {}"; |
|
421 |
by (fast_tac eq_cs 1); |
|
422 |
qed "empty_Diff"; |
|
1531 | 423 |
Addsimps[empty_Diff]; |
923 | 424 |
|
425 |
goal Set.thy "A-{} = A"; |
|
426 |
by (fast_tac eq_cs 1); |
|
427 |
qed "Diff_empty"; |
|
1531 | 428 |
Addsimps[Diff_empty]; |
429 |
||
430 |
goal Set.thy "A-UNIV = {}"; |
|
431 |
by (fast_tac eq_cs 1); |
|
432 |
qed "Diff_UNIV"; |
|
433 |
Addsimps[Diff_UNIV]; |
|
434 |
||
435 |
goal Set.thy "!!x. x~:A ==> A - insert x B = A-B"; |
|
436 |
by(fast_tac eq_cs 1); |
|
437 |
qed "Diff_insert0"; |
|
438 |
Addsimps [Diff_insert0]; |
|
923 | 439 |
|
440 |
(*NOT SUITABLE FOR REWRITING since {a} == insert a 0*) |
|
441 |
goal Set.thy "A - insert a B = A - B - {a}"; |
|
442 |
by (fast_tac eq_cs 1); |
|
443 |
qed "Diff_insert"; |
|
444 |
||
445 |
(*NOT SUITABLE FOR REWRITING since {a} == insert a 0*) |
|
446 |
goal Set.thy "A - insert a B = A - {a} - B"; |
|
447 |
by (fast_tac eq_cs 1); |
|
448 |
qed "Diff_insert2"; |
|
449 |
||
1531 | 450 |
goal Set.thy "insert x A - B = (if x:B then A-B else insert x (A-B))"; |
451 |
by(simp_tac (!simpset setloop split_tac[expand_if]) 1); |
|
452 |
by(fast_tac eq_cs 1); |
|
453 |
qed "insert_Diff_if"; |
|
454 |
||
455 |
goal Set.thy "!!x. x:B ==> insert x A - B = A-B"; |
|
456 |
by(fast_tac eq_cs 1); |
|
457 |
qed "insert_Diff1"; |
|
458 |
Addsimps [insert_Diff1]; |
|
459 |
||
923 | 460 |
val prems = goal Set.thy "a:A ==> insert a (A-{a}) = A"; |
461 |
by (fast_tac (eq_cs addSIs prems) 1); |
|
462 |
qed "insert_Diff"; |
|
463 |
||
464 |
goal Set.thy "A Int (B-A) = {}"; |
|
465 |
by (fast_tac eq_cs 1); |
|
466 |
qed "Diff_disjoint"; |
|
1531 | 467 |
Addsimps[Diff_disjoint]; |
923 | 468 |
|
469 |
goal Set.thy "!!A. A<=B ==> A Un (B-A) = B"; |
|
470 |
by (fast_tac eq_cs 1); |
|
471 |
qed "Diff_partition"; |
|
472 |
||
473 |
goal Set.thy "!!A. [| A<=B; B<= C |] ==> (B - (C - A)) = (A :: 'a set)"; |
|
474 |
by (fast_tac eq_cs 1); |
|
475 |
qed "double_diff"; |
|
476 |
||
477 |
goal Set.thy "A - (B Un C) = (A-B) Int (A-C)"; |
|
478 |
by (fast_tac eq_cs 1); |
|
479 |
qed "Diff_Un"; |
|
480 |
||
481 |
goal Set.thy "A - (B Int C) = (A-B) Un (A-C)"; |
|
482 |
by (fast_tac eq_cs 1); |
|
483 |
qed "Diff_Int"; |
|
484 |
||
1531 | 485 |
(* Congruence rule for set comprehension *) |
486 |
val prems = goal Set.thy |
|
487 |
"[| !!x. P x = Q x; !!x. Q x ==> f x = g x |] ==> \ |
|
488 |
\ {f x |x. P x} = {g x|x. Q x}"; |
|
489 |
by(simp_tac (!simpset addsimps prems) 1); |
|
490 |
br set_ext 1; |
|
491 |
br iffI 1; |
|
492 |
by(fast_tac (eq_cs addss (!simpset addsimps prems)) 1); |
|
493 |
be CollectE 1; |
|
494 |
be exE 1; |
|
495 |
by(Asm_simp_tac 1); |
|
496 |
be conjE 1; |
|
497 |
by(rtac exI 1 THEN rtac conjI 1 THEN atac 2); |
|
498 |
by(asm_simp_tac (!simpset addsimps prems) 1); |
|
499 |
qed "Collect_cong1"; |
|
500 |
||
501 |
Addsimps[subset_UNIV, empty_subsetI, subset_refl]; |