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