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