|
1 (* Title: ZF/equalities |
|
2 ID: $Id$ |
|
3 Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
|
4 Copyright 1992 University of Cambridge |
|
5 |
|
6 Set Theory examples: Union, Intersection, Inclusion, etc. |
|
7 (Thanks also to Philippe de Groote.) |
|
8 *) |
|
9 |
|
10 (** Finite Sets **) |
|
11 |
|
12 goal ZF.thy "cons(a, cons(b, C)) = cons(b, cons(a, C))"; |
|
13 by (fast_tac eq_cs 1); |
|
14 val cons_commute = result(); |
|
15 |
|
16 goal ZF.thy "!!B. a: B ==> cons(a,B) = B"; |
|
17 by (fast_tac eq_cs 1); |
|
18 val cons_absorb = result(); |
|
19 |
|
20 goal ZF.thy "!!B. a: B ==> cons(a, B-{a}) = B"; |
|
21 by (fast_tac eq_cs 1); |
|
22 val cons_Diff = result(); |
|
23 |
|
24 goal ZF.thy "!!C. [| a: C; ALL y:C. y=b |] ==> C = {b}"; |
|
25 by (fast_tac eq_cs 1); |
|
26 val equal_singleton_lemma = result(); |
|
27 val equal_singleton = ballI RSN (2,equal_singleton_lemma); |
|
28 |
|
29 |
|
30 (** Binary Intersection **) |
|
31 |
|
32 goal ZF.thy "0 Int A = 0"; |
|
33 by (fast_tac eq_cs 1); |
|
34 val Int_0 = result(); |
|
35 |
|
36 (*NOT an equality, but it seems to belong here...*) |
|
37 goal ZF.thy "cons(a,B) Int C <= cons(a, B Int C)"; |
|
38 by (fast_tac eq_cs 1); |
|
39 val Int_cons = result(); |
|
40 |
|
41 goal ZF.thy "A Int A = A"; |
|
42 by (fast_tac eq_cs 1); |
|
43 val Int_absorb = result(); |
|
44 |
|
45 goal ZF.thy "A Int B = B Int A"; |
|
46 by (fast_tac eq_cs 1); |
|
47 val Int_commute = result(); |
|
48 |
|
49 goal ZF.thy "(A Int B) Int C = A Int (B Int C)"; |
|
50 by (fast_tac eq_cs 1); |
|
51 val Int_assoc = result(); |
|
52 |
|
53 goal ZF.thy "(A Un B) Int C = (A Int C) Un (B Int C)"; |
|
54 by (fast_tac eq_cs 1); |
|
55 val Int_Un_distrib = result(); |
|
56 |
|
57 goal ZF.thy "A<=B <-> A Int B = A"; |
|
58 by (fast_tac (eq_cs addSEs [equalityE]) 1); |
|
59 val subset_Int_iff = result(); |
|
60 |
|
61 (** Binary Union **) |
|
62 |
|
63 goal ZF.thy "0 Un A = A"; |
|
64 by (fast_tac eq_cs 1); |
|
65 val Un_0 = result(); |
|
66 |
|
67 goal ZF.thy "cons(a,B) Un C = cons(a, B Un C)"; |
|
68 by (fast_tac eq_cs 1); |
|
69 val Un_cons = result(); |
|
70 |
|
71 goal ZF.thy "A Un A = A"; |
|
72 by (fast_tac eq_cs 1); |
|
73 val Un_absorb = result(); |
|
74 |
|
75 goal ZF.thy "A Un B = B Un A"; |
|
76 by (fast_tac eq_cs 1); |
|
77 val Un_commute = result(); |
|
78 |
|
79 goal ZF.thy "(A Un B) Un C = A Un (B Un C)"; |
|
80 by (fast_tac eq_cs 1); |
|
81 val Un_assoc = result(); |
|
82 |
|
83 goal ZF.thy "(A Int B) Un C = (A Un C) Int (B Un C)"; |
|
84 by (fast_tac eq_cs 1); |
|
85 val Un_Int_distrib = result(); |
|
86 |
|
87 goal ZF.thy "A<=B <-> A Un B = B"; |
|
88 by (fast_tac (eq_cs addSEs [equalityE]) 1); |
|
89 val subset_Un_iff = result(); |
|
90 |
|
91 (** Simple properties of Diff -- set difference **) |
|
92 |
|
93 goal ZF.thy "A-A = 0"; |
|
94 by (fast_tac eq_cs 1); |
|
95 val Diff_cancel = result(); |
|
96 |
|
97 goal ZF.thy "0-A = 0"; |
|
98 by (fast_tac eq_cs 1); |
|
99 val empty_Diff = result(); |
|
100 |
|
101 goal ZF.thy "A-0 = A"; |
|
102 by (fast_tac eq_cs 1); |
|
103 val Diff_0 = result(); |
|
104 |
|
105 (*NOT SUITABLE FOR REWRITING since {a} == cons(a,0)*) |
|
106 goal ZF.thy "A - cons(a,B) = A - B - {a}"; |
|
107 by (fast_tac eq_cs 1); |
|
108 val Diff_cons = result(); |
|
109 |
|
110 (*NOT SUITABLE FOR REWRITING since {a} == cons(a,0)*) |
|
111 goal ZF.thy "A - cons(a,B) = A - {a} - B"; |
|
112 by (fast_tac eq_cs 1); |
|
113 val Diff_cons2 = result(); |
|
114 |
|
115 goal ZF.thy "A Int (B-A) = 0"; |
|
116 by (fast_tac eq_cs 1); |
|
117 val Diff_disjoint = result(); |
|
118 |
|
119 goal ZF.thy "!!A B. A<=B ==> A Un (B-A) = B"; |
|
120 by (fast_tac eq_cs 1); |
|
121 val Diff_partition = result(); |
|
122 |
|
123 goal ZF.thy "!!A B. [| A<=B; B<= C |] ==> (B - (C-A)) = A"; |
|
124 by (fast_tac eq_cs 1); |
|
125 val double_complement = result(); |
|
126 |
|
127 goal ZF.thy |
|
128 "(A Int B) Un (B Int C) Un (C Int A) = (A Un B) Int (B Un C) Int (C Un A)"; |
|
129 by (fast_tac eq_cs 1); |
|
130 val Un_Int_crazy = result(); |
|
131 |
|
132 goal ZF.thy "A - (B Un C) = (A-B) Int (A-C)"; |
|
133 by (fast_tac eq_cs 1); |
|
134 val Diff_Un = result(); |
|
135 |
|
136 goal ZF.thy "A - (B Int C) = (A-B) Un (A-C)"; |
|
137 by (fast_tac eq_cs 1); |
|
138 val Diff_Int = result(); |
|
139 |
|
140 (*Halmos, Naive Set Theory, page 16.*) |
|
141 goal ZF.thy "(A Int B) Un C = A Int (B Un C) <-> C<=A"; |
|
142 by (fast_tac (eq_cs addSEs [equalityE]) 1); |
|
143 val Un_Int_assoc_iff = result(); |
|
144 |
|
145 |
|
146 (** Big Union and Intersection **) |
|
147 |
|
148 goal ZF.thy "Union(0) = 0"; |
|
149 by (fast_tac eq_cs 1); |
|
150 val Union_0 = result(); |
|
151 |
|
152 goal ZF.thy "Union(cons(a,B)) = a Un Union(B)"; |
|
153 by (fast_tac eq_cs 1); |
|
154 val Union_cons = result(); |
|
155 |
|
156 goal ZF.thy "Union(A Un B) = Union(A) Un Union(B)"; |
|
157 by (fast_tac eq_cs 1); |
|
158 val Union_Un_distrib = result(); |
|
159 |
|
160 goal ZF.thy "Union(C) Int A = 0 <-> (ALL B:C. B Int A = 0)"; |
|
161 by (fast_tac (eq_cs addSEs [equalityE]) 1); |
|
162 val Union_disjoint = result(); |
|
163 |
|
164 (* A good challenge: Inter is ill-behaved on the empty set *) |
|
165 goal ZF.thy "!!A B. [| a:A; b:B |] ==> Inter(A Un B) = Inter(A) Int Inter(B)"; |
|
166 by (fast_tac eq_cs 1); |
|
167 val Inter_Un_distrib = result(); |
|
168 |
|
169 goal ZF.thy "Union({b}) = b"; |
|
170 by (fast_tac eq_cs 1); |
|
171 val Union_singleton = result(); |
|
172 |
|
173 goal ZF.thy "Inter({b}) = b"; |
|
174 by (fast_tac eq_cs 1); |
|
175 val Inter_singleton = result(); |
|
176 |
|
177 (** Unions and Intersections of Families **) |
|
178 |
|
179 goal ZF.thy "Union(A) = (UN x:A. x)"; |
|
180 by (fast_tac eq_cs 1); |
|
181 val Union_eq_UN = result(); |
|
182 |
|
183 goalw ZF.thy [Inter_def] "Inter(A) = (INT x:A. x)"; |
|
184 by (fast_tac eq_cs 1); |
|
185 val Inter_eq_INT = result(); |
|
186 |
|
187 (*Halmos, Naive Set Theory, page 35.*) |
|
188 goal ZF.thy "B Int (UN i:I. A(i)) = (UN i:I. B Int A(i))"; |
|
189 by (fast_tac eq_cs 1); |
|
190 val Int_UN_distrib = result(); |
|
191 |
|
192 goal ZF.thy "!!A B. i:I ==> B Un (INT i:I. A(i)) = (INT i:I. B Un A(i))"; |
|
193 by (fast_tac eq_cs 1); |
|
194 val Un_INT_distrib = result(); |
|
195 |
|
196 goal ZF.thy |
|
197 "(UN i:I. A(i)) Int (UN j:J. B(j)) = (UN i:I. UN j:J. A(i) Int B(j))"; |
|
198 by (fast_tac eq_cs 1); |
|
199 val Int_UN_distrib2 = result(); |
|
200 |
|
201 goal ZF.thy |
|
202 "!!I J. [| i:I; j:J |] ==> \ |
|
203 \ (INT i:I. A(i)) Un (INT j:J. B(j)) = (INT i:I. INT j:J. A(i) Un B(j))"; |
|
204 by (fast_tac eq_cs 1); |
|
205 val Un_INT_distrib2 = result(); |
|
206 |
|
207 goal ZF.thy "!!A. [| a: A; ALL y:A. b(y)=b(a) |] ==> (UN y:A. b(y)) = b(a)"; |
|
208 by (fast_tac (eq_cs addSEs [equalityE]) 1); |
|
209 val UN_singleton_lemma = result(); |
|
210 val UN_singleton = ballI RSN (2,UN_singleton_lemma); |
|
211 |
|
212 goal ZF.thy "!!A. [| a: A; ALL y:A. b(y)=b(a) |] ==> (INT y:A. b(y)) = b(a)"; |
|
213 by (fast_tac (eq_cs addSEs [equalityE]) 1); |
|
214 val INT_singleton_lemma = result(); |
|
215 val INT_singleton = ballI RSN (2,INT_singleton_lemma); |
|
216 |
|
217 (** Devlin, Fundamentals of Contemporary Set Theory, page 12, exercise 5: |
|
218 Union of a family of unions **) |
|
219 |
|
220 goal ZF.thy "(UN i:I. A(x) Un B(x)) = (UN i:I. A(x)) Un (UN i:I. B(x))"; |
|
221 by (fast_tac eq_cs 1); |
|
222 val UN_Un_distrib = result(); |
|
223 |
|
224 goal ZF.thy |
|
225 "!!A B. i:I ==> \ |
|
226 \ (INT i:I. A(x) Int B(x)) = (INT i:I. A(x)) Int (INT i:I. B(x))"; |
|
227 by (fast_tac eq_cs 1); |
|
228 val INT_Int_distrib = result(); |
|
229 |
|
230 (** Devlin, page 12, exercise 5: Complements **) |
|
231 |
|
232 goal ZF.thy "!!A B. i:I ==> B - (UN i:I. A(i)) = (INT i:I. B - A(i))"; |
|
233 by (fast_tac eq_cs 1); |
|
234 val Diff_UN = result(); |
|
235 |
|
236 goal ZF.thy "!!A B. i:I ==> B - (INT i:I. A(i)) = (UN i:I. B - A(i))"; |
|
237 by (fast_tac eq_cs 1); |
|
238 val Diff_INT = result(); |
|
239 |
|
240 (** Unions and Intersections with General Sum **) |
|
241 |
|
242 goal ZF.thy "(SUM x:A Un B. C(x)) = (SUM x:A. C(x)) Un (SUM x:B. C(x))"; |
|
243 by (fast_tac eq_cs 1); |
|
244 val SUM_Un_distrib1 = result(); |
|
245 |
|
246 goal ZF.thy |
|
247 "(SUM i:I. A(x) Un B(x)) = (SUM i:I. A(x)) Un (SUM i:I. B(x))"; |
|
248 by (fast_tac eq_cs 1); |
|
249 val SUM_Un_distrib2 = result(); |
|
250 |
|
251 goal ZF.thy "(SUM x:A Int B. C(x)) = (SUM x:A. C(x)) Int (SUM x:B. C(x))"; |
|
252 by (fast_tac eq_cs 1); |
|
253 val SUM_Int_distrib1 = result(); |
|
254 |
|
255 goal ZF.thy |
|
256 "(SUM i:I. A(x) Int B(x)) = (SUM i:I. A(x)) Int (SUM i:I. B(x))"; |
|
257 by (fast_tac eq_cs 1); |
|
258 val SUM_Int_distrib2 = result(); |
|
259 |
|
260 (** Domain, Range and Field **) |
|
261 |
|
262 goal ZF.thy "domain(A Un B) = domain(A) Un domain(B)"; |
|
263 by (fast_tac eq_cs 1); |
|
264 val domain_Un_eq = result(); |
|
265 |
|
266 goal ZF.thy "domain(A Int B) <= domain(A) Int domain(B)"; |
|
267 by (fast_tac eq_cs 1); |
|
268 val domain_Int_subset = result(); |
|
269 |
|
270 goal ZF.thy "domain(A) - domain(B) <= domain(A - B)"; |
|
271 by (fast_tac eq_cs 1); |
|
272 val domain_diff_subset = result(); |
|
273 |
|
274 goal ZF.thy "range(A Un B) = range(A) Un range(B)"; |
|
275 by (fast_tac eq_cs 1); |
|
276 val range_Un_eq = result(); |
|
277 |
|
278 goal ZF.thy "range(A Int B) <= range(A) Int range(B)"; |
|
279 by (fast_tac eq_cs 1); |
|
280 val range_Int_subset = result(); |
|
281 |
|
282 goal ZF.thy "range(A) - range(B) <= range(A - B)"; |
|
283 by (fast_tac eq_cs 1); |
|
284 val range_diff_subset = result(); |
|
285 |
|
286 goal ZF.thy "field(A Un B) = field(A) Un field(B)"; |
|
287 by (fast_tac eq_cs 1); |
|
288 val field_Un_eq = result(); |
|
289 |
|
290 goal ZF.thy "field(A Int B) <= field(A) Int field(B)"; |
|
291 by (fast_tac eq_cs 1); |
|
292 val field_Int_subset = result(); |
|
293 |
|
294 goal ZF.thy "field(A) - field(B) <= field(A - B)"; |
|
295 by (fast_tac eq_cs 1); |
|
296 val field_diff_subset = result(); |
|
297 |
|
298 |
|
299 (** Converse **) |
|
300 |
|
301 goal ZF.thy "converse(A Un B) = converse(A) Un converse(B)"; |
|
302 by (fast_tac eq_cs 1); |
|
303 val converse_Un = result(); |
|
304 |
|
305 goal ZF.thy "converse(A Int B) = converse(A) Int converse(B)"; |
|
306 by (fast_tac eq_cs 1); |
|
307 val converse_Int = result(); |
|
308 |
|
309 goal ZF.thy "converse(A) - converse(B) = converse(A - B)"; |
|
310 by (fast_tac eq_cs 1); |
|
311 val converse_diff = result(); |
|
312 |