author | paulson |
Thu, 04 Apr 1996 18:18:48 +0200 | |
changeset 1652 | 9b78ce58d6b1 |
parent 1611 | 35e0fd1b1775 |
child 1784 | 036a7f301623 |
permissions | -rw-r--r-- |
1461 | 1 |
(* Title: ZF/equalities |
0 | 2 |
ID: $Id$ |
1461 | 3 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
0 | 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 |
||
520 | 12 |
(* cons_def refers to Upair; reversing the equality LOOPS in rewriting!*) |
13 |
goal ZF.thy "{a} Un B = cons(a,B)"; |
|
14 |
by (fast_tac eq_cs 1); |
|
760 | 15 |
qed "cons_eq"; |
520 | 16 |
|
0 | 17 |
goal ZF.thy "cons(a, cons(b, C)) = cons(b, cons(a, C))"; |
18 |
by (fast_tac eq_cs 1); |
|
760 | 19 |
qed "cons_commute"; |
0 | 20 |
|
21 |
goal ZF.thy "!!B. a: B ==> cons(a,B) = B"; |
|
22 |
by (fast_tac eq_cs 1); |
|
760 | 23 |
qed "cons_absorb"; |
0 | 24 |
|
25 |
goal ZF.thy "!!B. a: B ==> cons(a, B-{a}) = B"; |
|
26 |
by (fast_tac eq_cs 1); |
|
760 | 27 |
qed "cons_Diff"; |
0 | 28 |
|
29 |
goal ZF.thy "!!C. [| a: C; ALL y:C. y=b |] ==> C = {b}"; |
|
30 |
by (fast_tac eq_cs 1); |
|
760 | 31 |
qed "equal_singleton_lemma"; |
0 | 32 |
val equal_singleton = ballI RSN (2,equal_singleton_lemma); |
33 |
||
34 |
||
35 |
(** Binary Intersection **) |
|
36 |
||
37 |
goal ZF.thy "0 Int A = 0"; |
|
38 |
by (fast_tac eq_cs 1); |
|
760 | 39 |
qed "Int_0"; |
0 | 40 |
|
41 |
(*NOT an equality, but it seems to belong here...*) |
|
42 |
goal ZF.thy "cons(a,B) Int C <= cons(a, B Int C)"; |
|
43 |
by (fast_tac eq_cs 1); |
|
760 | 44 |
qed "Int_cons"; |
0 | 45 |
|
46 |
goal ZF.thy "A Int A = A"; |
|
47 |
by (fast_tac eq_cs 1); |
|
760 | 48 |
qed "Int_absorb"; |
0 | 49 |
|
50 |
goal ZF.thy "A Int B = B Int A"; |
|
51 |
by (fast_tac eq_cs 1); |
|
760 | 52 |
qed "Int_commute"; |
0 | 53 |
|
54 |
goal ZF.thy "(A Int B) Int C = A Int (B Int C)"; |
|
55 |
by (fast_tac eq_cs 1); |
|
760 | 56 |
qed "Int_assoc"; |
0 | 57 |
|
58 |
goal ZF.thy "(A Un B) Int C = (A Int C) Un (B Int C)"; |
|
59 |
by (fast_tac eq_cs 1); |
|
760 | 60 |
qed "Int_Un_distrib"; |
0 | 61 |
|
62 |
goal ZF.thy "A<=B <-> A Int B = A"; |
|
63 |
by (fast_tac (eq_cs addSEs [equalityE]) 1); |
|
760 | 64 |
qed "subset_Int_iff"; |
0 | 65 |
|
435 | 66 |
goal ZF.thy "A<=B <-> B Int A = A"; |
67 |
by (fast_tac (eq_cs addSEs [equalityE]) 1); |
|
760 | 68 |
qed "subset_Int_iff2"; |
435 | 69 |
|
1035 | 70 |
goal ZF.thy "!!A B C. C<=A ==> (A-B) Int C = C-B"; |
71 |
by (fast_tac eq_cs 1); |
|
72 |
qed "Int_Diff_eq"; |
|
73 |
||
0 | 74 |
(** Binary Union **) |
75 |
||
76 |
goal ZF.thy "0 Un A = A"; |
|
77 |
by (fast_tac eq_cs 1); |
|
760 | 78 |
qed "Un_0"; |
0 | 79 |
|
80 |
goal ZF.thy "cons(a,B) Un C = cons(a, B Un C)"; |
|
81 |
by (fast_tac eq_cs 1); |
|
760 | 82 |
qed "Un_cons"; |
0 | 83 |
|
84 |
goal ZF.thy "A Un A = A"; |
|
85 |
by (fast_tac eq_cs 1); |
|
760 | 86 |
qed "Un_absorb"; |
0 | 87 |
|
88 |
goal ZF.thy "A Un B = B Un A"; |
|
89 |
by (fast_tac eq_cs 1); |
|
760 | 90 |
qed "Un_commute"; |
0 | 91 |
|
92 |
goal ZF.thy "(A Un B) Un C = A Un (B Un C)"; |
|
93 |
by (fast_tac eq_cs 1); |
|
760 | 94 |
qed "Un_assoc"; |
0 | 95 |
|
96 |
goal ZF.thy "(A Int B) Un C = (A Un C) Int (B Un C)"; |
|
97 |
by (fast_tac eq_cs 1); |
|
760 | 98 |
qed "Un_Int_distrib"; |
0 | 99 |
|
100 |
goal ZF.thy "A<=B <-> A Un B = B"; |
|
101 |
by (fast_tac (eq_cs addSEs [equalityE]) 1); |
|
760 | 102 |
qed "subset_Un_iff"; |
0 | 103 |
|
435 | 104 |
goal ZF.thy "A<=B <-> B Un A = B"; |
105 |
by (fast_tac (eq_cs addSEs [equalityE]) 1); |
|
760 | 106 |
qed "subset_Un_iff2"; |
435 | 107 |
|
0 | 108 |
(** Simple properties of Diff -- set difference **) |
109 |
||
110 |
goal ZF.thy "A-A = 0"; |
|
111 |
by (fast_tac eq_cs 1); |
|
760 | 112 |
qed "Diff_cancel"; |
0 | 113 |
|
114 |
goal ZF.thy "0-A = 0"; |
|
115 |
by (fast_tac eq_cs 1); |
|
760 | 116 |
qed "empty_Diff"; |
0 | 117 |
|
118 |
goal ZF.thy "A-0 = A"; |
|
119 |
by (fast_tac eq_cs 1); |
|
760 | 120 |
qed "Diff_0"; |
0 | 121 |
|
787 | 122 |
goal ZF.thy "A-B=0 <-> A<=B"; |
123 |
by (fast_tac (eq_cs addEs [equalityE]) 1); |
|
124 |
qed "Diff_eq_0_iff"; |
|
125 |
||
0 | 126 |
(*NOT SUITABLE FOR REWRITING since {a} == cons(a,0)*) |
127 |
goal ZF.thy "A - cons(a,B) = A - B - {a}"; |
|
128 |
by (fast_tac eq_cs 1); |
|
760 | 129 |
qed "Diff_cons"; |
0 | 130 |
|
131 |
(*NOT SUITABLE FOR REWRITING since {a} == cons(a,0)*) |
|
132 |
goal ZF.thy "A - cons(a,B) = A - {a} - B"; |
|
133 |
by (fast_tac eq_cs 1); |
|
760 | 134 |
qed "Diff_cons2"; |
0 | 135 |
|
136 |
goal ZF.thy "A Int (B-A) = 0"; |
|
137 |
by (fast_tac eq_cs 1); |
|
760 | 138 |
qed "Diff_disjoint"; |
0 | 139 |
|
140 |
goal ZF.thy "!!A B. A<=B ==> A Un (B-A) = B"; |
|
141 |
by (fast_tac eq_cs 1); |
|
760 | 142 |
qed "Diff_partition"; |
0 | 143 |
|
1611 | 144 |
goal ZF.thy "A <= B Un (A - B)"; |
145 |
by (fast_tac ZF_cs 1); |
|
146 |
qed "subset_Un_Diff"; |
|
147 |
||
268 | 148 |
goal ZF.thy "!!A B. [| A<=B; B<=C |] ==> B-(C-A) = A"; |
0 | 149 |
by (fast_tac eq_cs 1); |
760 | 150 |
qed "double_complement"; |
0 | 151 |
|
268 | 152 |
goal ZF.thy "(A Un B) - (B-A) = A"; |
153 |
by (fast_tac eq_cs 1); |
|
760 | 154 |
qed "double_complement_Un"; |
268 | 155 |
|
0 | 156 |
goal ZF.thy |
157 |
"(A Int B) Un (B Int C) Un (C Int A) = (A Un B) Int (B Un C) Int (C Un A)"; |
|
158 |
by (fast_tac eq_cs 1); |
|
760 | 159 |
qed "Un_Int_crazy"; |
0 | 160 |
|
161 |
goal ZF.thy "A - (B Un C) = (A-B) Int (A-C)"; |
|
162 |
by (fast_tac eq_cs 1); |
|
760 | 163 |
qed "Diff_Un"; |
0 | 164 |
|
165 |
goal ZF.thy "A - (B Int C) = (A-B) Un (A-C)"; |
|
166 |
by (fast_tac eq_cs 1); |
|
760 | 167 |
qed "Diff_Int"; |
0 | 168 |
|
169 |
(*Halmos, Naive Set Theory, page 16.*) |
|
170 |
goal ZF.thy "(A Int B) Un C = A Int (B Un C) <-> C<=A"; |
|
171 |
by (fast_tac (eq_cs addSEs [equalityE]) 1); |
|
760 | 172 |
qed "Un_Int_assoc_iff"; |
0 | 173 |
|
174 |
||
175 |
(** Big Union and Intersection **) |
|
176 |
||
177 |
goal ZF.thy "Union(0) = 0"; |
|
178 |
by (fast_tac eq_cs 1); |
|
760 | 179 |
qed "Union_0"; |
0 | 180 |
|
181 |
goal ZF.thy "Union(cons(a,B)) = a Un Union(B)"; |
|
182 |
by (fast_tac eq_cs 1); |
|
760 | 183 |
qed "Union_cons"; |
0 | 184 |
|
185 |
goal ZF.thy "Union(A Un B) = Union(A) Un Union(B)"; |
|
186 |
by (fast_tac eq_cs 1); |
|
760 | 187 |
qed "Union_Un_distrib"; |
0 | 188 |
|
435 | 189 |
goal ZF.thy "Union(A Int B) <= Union(A) Int Union(B)"; |
190 |
by (fast_tac ZF_cs 1); |
|
760 | 191 |
qed "Union_Int_subset"; |
435 | 192 |
|
0 | 193 |
goal ZF.thy "Union(C) Int A = 0 <-> (ALL B:C. B Int A = 0)"; |
194 |
by (fast_tac (eq_cs addSEs [equalityE]) 1); |
|
760 | 195 |
qed "Union_disjoint"; |
0 | 196 |
|
1652 | 197 |
goalw ZF.thy [Inter_def] "Inter(0) = 0"; |
198 |
by (fast_tac eq_cs 1); |
|
199 |
qed "Inter_0"; |
|
200 |
||
1568 | 201 |
goal ZF.thy "!!A B. [| z:A; z:B |] ==> Inter(A) Un Inter(B) <= Inter(A Int B)"; |
202 |
by (fast_tac ZF_cs 1); |
|
203 |
qed "Inter_Un_subset"; |
|
204 |
||
0 | 205 |
(* A good challenge: Inter is ill-behaved on the empty set *) |
206 |
goal ZF.thy "!!A B. [| a:A; b:B |] ==> Inter(A Un B) = Inter(A) Int Inter(B)"; |
|
207 |
by (fast_tac eq_cs 1); |
|
760 | 208 |
qed "Inter_Un_distrib"; |
0 | 209 |
|
210 |
goal ZF.thy "Union({b}) = b"; |
|
211 |
by (fast_tac eq_cs 1); |
|
760 | 212 |
qed "Union_singleton"; |
0 | 213 |
|
214 |
goal ZF.thy "Inter({b}) = b"; |
|
215 |
by (fast_tac eq_cs 1); |
|
760 | 216 |
qed "Inter_singleton"; |
0 | 217 |
|
218 |
(** Unions and Intersections of Families **) |
|
219 |
||
220 |
goal ZF.thy "Union(A) = (UN x:A. x)"; |
|
221 |
by (fast_tac eq_cs 1); |
|
760 | 222 |
qed "Union_eq_UN"; |
0 | 223 |
|
224 |
goalw ZF.thy [Inter_def] "Inter(A) = (INT x:A. x)"; |
|
225 |
by (fast_tac eq_cs 1); |
|
760 | 226 |
qed "Inter_eq_INT"; |
0 | 227 |
|
517 | 228 |
goal ZF.thy "(UN i:0. A(i)) = 0"; |
229 |
by (fast_tac eq_cs 1); |
|
760 | 230 |
qed "UN_0"; |
517 | 231 |
|
0 | 232 |
(*Halmos, Naive Set Theory, page 35.*) |
233 |
goal ZF.thy "B Int (UN i:I. A(i)) = (UN i:I. B Int A(i))"; |
|
234 |
by (fast_tac eq_cs 1); |
|
760 | 235 |
qed "Int_UN_distrib"; |
0 | 236 |
|
237 |
goal ZF.thy "!!A B. i:I ==> B Un (INT i:I. A(i)) = (INT i:I. B Un A(i))"; |
|
238 |
by (fast_tac eq_cs 1); |
|
760 | 239 |
qed "Un_INT_distrib"; |
0 | 240 |
|
241 |
goal ZF.thy |
|
242 |
"(UN i:I. A(i)) Int (UN j:J. B(j)) = (UN i:I. UN j:J. A(i) Int B(j))"; |
|
243 |
by (fast_tac eq_cs 1); |
|
760 | 244 |
qed "Int_UN_distrib2"; |
0 | 245 |
|
246 |
goal ZF.thy |
|
247 |
"!!I J. [| i:I; j:J |] ==> \ |
|
248 |
\ (INT i:I. A(i)) Un (INT j:J. B(j)) = (INT i:I. INT j:J. A(i) Un B(j))"; |
|
249 |
by (fast_tac eq_cs 1); |
|
760 | 250 |
qed "Un_INT_distrib2"; |
0 | 251 |
|
435 | 252 |
goal ZF.thy "!!A. a: A ==> (UN y:A. c) = c"; |
253 |
by (fast_tac eq_cs 1); |
|
760 | 254 |
qed "UN_constant"; |
0 | 255 |
|
435 | 256 |
goal ZF.thy "!!A. a: A ==> (INT y:A. c) = c"; |
257 |
by (fast_tac eq_cs 1); |
|
760 | 258 |
qed "INT_constant"; |
0 | 259 |
|
260 |
(** Devlin, Fundamentals of Contemporary Set Theory, page 12, exercise 5: |
|
261 |
Union of a family of unions **) |
|
262 |
||
192 | 263 |
goal ZF.thy "(UN i:I. A(i) Un B(i)) = (UN i:I. A(i)) Un (UN i:I. B(i))"; |
0 | 264 |
by (fast_tac eq_cs 1); |
760 | 265 |
qed "UN_Un_distrib"; |
0 | 266 |
|
267 |
goal ZF.thy |
|
268 |
"!!A B. i:I ==> \ |
|
192 | 269 |
\ (INT i:I. A(i) Int B(i)) = (INT i:I. A(i)) Int (INT i:I. B(i))"; |
0 | 270 |
by (fast_tac eq_cs 1); |
760 | 271 |
qed "INT_Int_distrib"; |
0 | 272 |
|
273 |
(** Devlin, page 12, exercise 5: Complements **) |
|
274 |
||
275 |
goal ZF.thy "!!A B. i:I ==> B - (UN i:I. A(i)) = (INT i:I. B - A(i))"; |
|
276 |
by (fast_tac eq_cs 1); |
|
760 | 277 |
qed "Diff_UN"; |
0 | 278 |
|
279 |
goal ZF.thy "!!A B. i:I ==> B - (INT i:I. A(i)) = (UN i:I. B - A(i))"; |
|
280 |
by (fast_tac eq_cs 1); |
|
760 | 281 |
qed "Diff_INT"; |
0 | 282 |
|
283 |
(** Unions and Intersections with General Sum **) |
|
284 |
||
1611 | 285 |
(*Not suitable for rewriting: LOOPS!*) |
520 | 286 |
goal ZF.thy "Sigma(cons(a,B), C) = ({a}*C(a)) Un Sigma(B,C)"; |
287 |
by (fast_tac eq_cs 1); |
|
1611 | 288 |
qed "Sigma_cons1"; |
289 |
||
290 |
(*Not suitable for rewriting: LOOPS!*) |
|
291 |
goal ZF.thy "A * cons(b,B) = A*{b} Un A*B"; |
|
292 |
by (fast_tac eq_cs 1); |
|
293 |
qed "Sigma_cons2"; |
|
294 |
||
295 |
goal ZF.thy "Sigma(succ(A), B) = ({A}*B(A)) Un Sigma(A,B)"; |
|
296 |
by (fast_tac eq_cs 1); |
|
297 |
qed "Sigma_succ1"; |
|
298 |
||
299 |
goal ZF.thy "A * succ(B) = A*{B} Un A*B"; |
|
300 |
by (fast_tac eq_cs 1); |
|
301 |
qed "Sigma_succ2"; |
|
520 | 302 |
|
182 | 303 |
goal ZF.thy "(SUM x:(UN y:A. C(y)). B(x)) = (UN y:A. SUM x:C(y). B(x))"; |
304 |
by (fast_tac eq_cs 1); |
|
760 | 305 |
qed "SUM_UN_distrib1"; |
182 | 306 |
|
192 | 307 |
goal ZF.thy "(SUM i:I. UN j:J. C(i,j)) = (UN j:J. SUM i:I. C(i,j))"; |
182 | 308 |
by (fast_tac eq_cs 1); |
760 | 309 |
qed "SUM_UN_distrib2"; |
182 | 310 |
|
192 | 311 |
goal ZF.thy "(SUM i:I Un J. C(i)) = (SUM i:I. C(i)) Un (SUM j:J. C(j))"; |
0 | 312 |
by (fast_tac eq_cs 1); |
760 | 313 |
qed "SUM_Un_distrib1"; |
0 | 314 |
|
192 | 315 |
goal ZF.thy "(SUM i:I. A(i) Un B(i)) = (SUM i:I. A(i)) Un (SUM i:I. B(i))"; |
0 | 316 |
by (fast_tac eq_cs 1); |
760 | 317 |
qed "SUM_Un_distrib2"; |
0 | 318 |
|
685 | 319 |
(*First-order version of the above, for rewriting*) |
320 |
goal ZF.thy "I * (A Un B) = I*A Un I*B"; |
|
1461 | 321 |
by (rtac SUM_Un_distrib2 1); |
760 | 322 |
qed "prod_Un_distrib2"; |
685 | 323 |
|
192 | 324 |
goal ZF.thy "(SUM i:I Int J. C(i)) = (SUM i:I. C(i)) Int (SUM j:J. C(j))"; |
0 | 325 |
by (fast_tac eq_cs 1); |
760 | 326 |
qed "SUM_Int_distrib1"; |
0 | 327 |
|
328 |
goal ZF.thy |
|
192 | 329 |
"(SUM i:I. A(i) Int B(i)) = (SUM i:I. A(i)) Int (SUM i:I. B(i))"; |
0 | 330 |
by (fast_tac eq_cs 1); |
760 | 331 |
qed "SUM_Int_distrib2"; |
0 | 332 |
|
685 | 333 |
(*First-order version of the above, for rewriting*) |
334 |
goal ZF.thy "I * (A Int B) = I*A Int I*B"; |
|
1461 | 335 |
by (rtac SUM_Int_distrib2 1); |
760 | 336 |
qed "prod_Int_distrib2"; |
685 | 337 |
|
192 | 338 |
(*Cf Aczel, Non-Well-Founded Sets, page 115*) |
339 |
goal ZF.thy "(SUM i:I. A(i)) = (UN i:I. {i} * A(i))"; |
|
340 |
by (fast_tac eq_cs 1); |
|
760 | 341 |
qed "SUM_eq_UN"; |
192 | 342 |
|
536
5fbfa997f1b0
ZF/domrange/domain_of_prod, domain_empty, etc: moved to equalities.ML where
lcp
parents:
520
diff
changeset
|
343 |
(** Domain **) |
5fbfa997f1b0
ZF/domrange/domain_of_prod, domain_empty, etc: moved to equalities.ML where
lcp
parents:
520
diff
changeset
|
344 |
|
760 | 345 |
qed_goal "domain_of_prod" ZF.thy "!!A B. b:B ==> domain(A*B) = A" |
536
5fbfa997f1b0
ZF/domrange/domain_of_prod, domain_empty, etc: moved to equalities.ML where
lcp
parents:
520
diff
changeset
|
346 |
(fn _ => [ fast_tac eq_cs 1 ]); |
5fbfa997f1b0
ZF/domrange/domain_of_prod, domain_empty, etc: moved to equalities.ML where
lcp
parents:
520
diff
changeset
|
347 |
|
760 | 348 |
qed_goal "domain_0" ZF.thy "domain(0) = 0" |
536
5fbfa997f1b0
ZF/domrange/domain_of_prod, domain_empty, etc: moved to equalities.ML where
lcp
parents:
520
diff
changeset
|
349 |
(fn _ => [ fast_tac eq_cs 1 ]); |
5fbfa997f1b0
ZF/domrange/domain_of_prod, domain_empty, etc: moved to equalities.ML where
lcp
parents:
520
diff
changeset
|
350 |
|
760 | 351 |
qed_goal "domain_cons" ZF.thy |
536
5fbfa997f1b0
ZF/domrange/domain_of_prod, domain_empty, etc: moved to equalities.ML where
lcp
parents:
520
diff
changeset
|
352 |
"domain(cons(<a,b>,r)) = cons(a, domain(r))" |
5fbfa997f1b0
ZF/domrange/domain_of_prod, domain_empty, etc: moved to equalities.ML where
lcp
parents:
520
diff
changeset
|
353 |
(fn _ => [ fast_tac eq_cs 1 ]); |
0 | 354 |
|
355 |
goal ZF.thy "domain(A Un B) = domain(A) Un domain(B)"; |
|
356 |
by (fast_tac eq_cs 1); |
|
760 | 357 |
qed "domain_Un_eq"; |
0 | 358 |
|
359 |
goal ZF.thy "domain(A Int B) <= domain(A) Int domain(B)"; |
|
360 |
by (fast_tac eq_cs 1); |
|
760 | 361 |
qed "domain_Int_subset"; |
0 | 362 |
|
363 |
goal ZF.thy "domain(A) - domain(B) <= domain(A - B)"; |
|
364 |
by (fast_tac eq_cs 1); |
|
1056 | 365 |
qed "domain_Diff_subset"; |
0 | 366 |
|
685 | 367 |
goal ZF.thy "domain(converse(r)) = range(r)"; |
368 |
by (fast_tac eq_cs 1); |
|
760 | 369 |
qed "domain_converse"; |
685 | 370 |
|
371 |
||
372 |
||
536
5fbfa997f1b0
ZF/domrange/domain_of_prod, domain_empty, etc: moved to equalities.ML where
lcp
parents:
520
diff
changeset
|
373 |
(** Range **) |
5fbfa997f1b0
ZF/domrange/domain_of_prod, domain_empty, etc: moved to equalities.ML where
lcp
parents:
520
diff
changeset
|
374 |
|
760 | 375 |
qed_goal "range_of_prod" ZF.thy |
536
5fbfa997f1b0
ZF/domrange/domain_of_prod, domain_empty, etc: moved to equalities.ML where
lcp
parents:
520
diff
changeset
|
376 |
"!!a A B. a:A ==> range(A*B) = B" |
5fbfa997f1b0
ZF/domrange/domain_of_prod, domain_empty, etc: moved to equalities.ML where
lcp
parents:
520
diff
changeset
|
377 |
(fn _ => [ fast_tac eq_cs 1 ]); |
5fbfa997f1b0
ZF/domrange/domain_of_prod, domain_empty, etc: moved to equalities.ML where
lcp
parents:
520
diff
changeset
|
378 |
|
760 | 379 |
qed_goal "range_0" ZF.thy "range(0) = 0" |
536
5fbfa997f1b0
ZF/domrange/domain_of_prod, domain_empty, etc: moved to equalities.ML where
lcp
parents:
520
diff
changeset
|
380 |
(fn _ => [ fast_tac eq_cs 1 ]); |
5fbfa997f1b0
ZF/domrange/domain_of_prod, domain_empty, etc: moved to equalities.ML where
lcp
parents:
520
diff
changeset
|
381 |
|
760 | 382 |
qed_goal "range_cons" ZF.thy |
536
5fbfa997f1b0
ZF/domrange/domain_of_prod, domain_empty, etc: moved to equalities.ML where
lcp
parents:
520
diff
changeset
|
383 |
"range(cons(<a,b>,r)) = cons(b, range(r))" |
5fbfa997f1b0
ZF/domrange/domain_of_prod, domain_empty, etc: moved to equalities.ML where
lcp
parents:
520
diff
changeset
|
384 |
(fn _ => [ fast_tac eq_cs 1 ]); |
5fbfa997f1b0
ZF/domrange/domain_of_prod, domain_empty, etc: moved to equalities.ML where
lcp
parents:
520
diff
changeset
|
385 |
|
0 | 386 |
goal ZF.thy "range(A Un B) = range(A) Un range(B)"; |
387 |
by (fast_tac eq_cs 1); |
|
760 | 388 |
qed "range_Un_eq"; |
0 | 389 |
|
390 |
goal ZF.thy "range(A Int B) <= range(A) Int range(B)"; |
|
435 | 391 |
by (fast_tac ZF_cs 1); |
760 | 392 |
qed "range_Int_subset"; |
0 | 393 |
|
394 |
goal ZF.thy "range(A) - range(B) <= range(A - B)"; |
|
395 |
by (fast_tac eq_cs 1); |
|
1056 | 396 |
qed "range_Diff_subset"; |
0 | 397 |
|
685 | 398 |
goal ZF.thy "range(converse(r)) = domain(r)"; |
399 |
by (fast_tac eq_cs 1); |
|
760 | 400 |
qed "range_converse"; |
685 | 401 |
|
536
5fbfa997f1b0
ZF/domrange/domain_of_prod, domain_empty, etc: moved to equalities.ML where
lcp
parents:
520
diff
changeset
|
402 |
(** Field **) |
5fbfa997f1b0
ZF/domrange/domain_of_prod, domain_empty, etc: moved to equalities.ML where
lcp
parents:
520
diff
changeset
|
403 |
|
760 | 404 |
qed_goal "field_of_prod" ZF.thy "field(A*A) = A" |
536
5fbfa997f1b0
ZF/domrange/domain_of_prod, domain_empty, etc: moved to equalities.ML where
lcp
parents:
520
diff
changeset
|
405 |
(fn _ => [ fast_tac eq_cs 1 ]); |
5fbfa997f1b0
ZF/domrange/domain_of_prod, domain_empty, etc: moved to equalities.ML where
lcp
parents:
520
diff
changeset
|
406 |
|
760 | 407 |
qed_goal "field_0" ZF.thy "field(0) = 0" |
536
5fbfa997f1b0
ZF/domrange/domain_of_prod, domain_empty, etc: moved to equalities.ML where
lcp
parents:
520
diff
changeset
|
408 |
(fn _ => [ fast_tac eq_cs 1 ]); |
5fbfa997f1b0
ZF/domrange/domain_of_prod, domain_empty, etc: moved to equalities.ML where
lcp
parents:
520
diff
changeset
|
409 |
|
760 | 410 |
qed_goal "field_cons" ZF.thy |
536
5fbfa997f1b0
ZF/domrange/domain_of_prod, domain_empty, etc: moved to equalities.ML where
lcp
parents:
520
diff
changeset
|
411 |
"field(cons(<a,b>,r)) = cons(a, cons(b, field(r)))" |
5fbfa997f1b0
ZF/domrange/domain_of_prod, domain_empty, etc: moved to equalities.ML where
lcp
parents:
520
diff
changeset
|
412 |
(fn _ => [ rtac equalityI 1, ALLGOALS (fast_tac ZF_cs) ]); |
5fbfa997f1b0
ZF/domrange/domain_of_prod, domain_empty, etc: moved to equalities.ML where
lcp
parents:
520
diff
changeset
|
413 |
|
0 | 414 |
goal ZF.thy "field(A Un B) = field(A) Un field(B)"; |
415 |
by (fast_tac eq_cs 1); |
|
760 | 416 |
qed "field_Un_eq"; |
0 | 417 |
|
418 |
goal ZF.thy "field(A Int B) <= field(A) Int field(B)"; |
|
419 |
by (fast_tac eq_cs 1); |
|
760 | 420 |
qed "field_Int_subset"; |
0 | 421 |
|
422 |
goal ZF.thy "field(A) - field(B) <= field(A - B)"; |
|
423 |
by (fast_tac eq_cs 1); |
|
1056 | 424 |
qed "field_Diff_subset"; |
0 | 425 |
|
426 |
||
435 | 427 |
(** Image **) |
428 |
||
429 |
goal ZF.thy "r``0 = 0"; |
|
430 |
by (fast_tac eq_cs 1); |
|
760 | 431 |
qed "image_0"; |
435 | 432 |
|
433 |
goal ZF.thy "r``(A Un B) = (r``A) Un (r``B)"; |
|
434 |
by (fast_tac eq_cs 1); |
|
760 | 435 |
qed "image_Un"; |
435 | 436 |
|
437 |
goal ZF.thy "r``(A Int B) <= (r``A) Int (r``B)"; |
|
438 |
by (fast_tac ZF_cs 1); |
|
760 | 439 |
qed "image_Int_subset"; |
435 | 440 |
|
441 |
goal ZF.thy "(r Int A*A)``B <= (r``B) Int A"; |
|
442 |
by (fast_tac ZF_cs 1); |
|
760 | 443 |
qed "image_Int_square_subset"; |
435 | 444 |
|
445 |
goal ZF.thy "!!r. B<=A ==> (r Int A*A)``B = (r``B) Int A"; |
|
446 |
by (fast_tac eq_cs 1); |
|
760 | 447 |
qed "image_Int_square"; |
435 | 448 |
|
449 |
||
450 |
(** Inverse Image **) |
|
451 |
||
452 |
goal ZF.thy "r-``0 = 0"; |
|
453 |
by (fast_tac eq_cs 1); |
|
760 | 454 |
qed "vimage_0"; |
435 | 455 |
|
456 |
goal ZF.thy "r-``(A Un B) = (r-``A) Un (r-``B)"; |
|
457 |
by (fast_tac eq_cs 1); |
|
760 | 458 |
qed "vimage_Un"; |
435 | 459 |
|
460 |
goal ZF.thy "r-``(A Int B) <= (r-``A) Int (r-``B)"; |
|
461 |
by (fast_tac ZF_cs 1); |
|
760 | 462 |
qed "vimage_Int_subset"; |
435 | 463 |
|
464 |
goal ZF.thy "(r Int A*A)-``B <= (r-``B) Int A"; |
|
465 |
by (fast_tac ZF_cs 1); |
|
760 | 466 |
qed "vimage_Int_square_subset"; |
435 | 467 |
|
468 |
goal ZF.thy "!!r. B<=A ==> (r Int A*A)-``B = (r-``B) Int A"; |
|
469 |
by (fast_tac eq_cs 1); |
|
760 | 470 |
qed "vimage_Int_square"; |
435 | 471 |
|
472 |
||
0 | 473 |
(** Converse **) |
474 |
||
475 |
goal ZF.thy "converse(A Un B) = converse(A) Un converse(B)"; |
|
476 |
by (fast_tac eq_cs 1); |
|
760 | 477 |
qed "converse_Un"; |
0 | 478 |
|
479 |
goal ZF.thy "converse(A Int B) = converse(A) Int converse(B)"; |
|
480 |
by (fast_tac eq_cs 1); |
|
760 | 481 |
qed "converse_Int"; |
0 | 482 |
|
483 |
goal ZF.thy "converse(A) - converse(B) = converse(A - B)"; |
|
484 |
by (fast_tac eq_cs 1); |
|
1056 | 485 |
qed "converse_Diff"; |
0 | 486 |
|
787 | 487 |
goal ZF.thy "converse(UN x:A. B(x)) = (UN x:A. converse(B(x)))"; |
488 |
by (fast_tac eq_cs 1); |
|
489 |
qed "converse_UN"; |
|
490 |
||
1652 | 491 |
(*Unfolding Inter avoids using excluded middle on A=0*) |
492 |
goalw ZF.thy [Inter_def] "converse(INT x:A. B(x)) = (INT x:A. converse(B(x)))"; |
|
493 |
by (fast_tac eq_cs 1); |
|
494 |
qed "converse_INT"; |
|
495 |
||
198 | 496 |
(** Pow **) |
497 |
||
498 |
goal ZF.thy "Pow(A) Un Pow(B) <= Pow(A Un B)"; |
|
499 |
by (fast_tac upair_cs 1); |
|
760 | 500 |
qed "Un_Pow_subset"; |
198 | 501 |
|
502 |
goal ZF.thy "(UN x:A. Pow(B(x))) <= Pow(UN x:A. B(x))"; |
|
503 |
by (fast_tac upair_cs 1); |
|
760 | 504 |
qed "UN_Pow_subset"; |
198 | 505 |
|
506 |
goal ZF.thy "A <= Pow(Union(A))"; |
|
507 |
by (fast_tac upair_cs 1); |
|
760 | 508 |
qed "subset_Pow_Union"; |
198 | 509 |
|
510 |
goal ZF.thy "Union(Pow(A)) = A"; |
|
511 |
by (fast_tac eq_cs 1); |
|
760 | 512 |
qed "Union_Pow_eq"; |
198 | 513 |
|
514 |
goal ZF.thy "Pow(A) Int Pow(B) = Pow(A Int B)"; |
|
515 |
by (fast_tac eq_cs 1); |
|
760 | 516 |
qed "Int_Pow_eq"; |
198 | 517 |
|
518 |
goal ZF.thy "!!x A. x:A ==> (INT x:A. Pow(B(x))) = Pow(INT x:A. B(x))"; |
|
519 |
by (fast_tac eq_cs 1); |
|
760 | 520 |
qed "INT_Pow_subset"; |
435 | 521 |
|
839 | 522 |
(** RepFun **) |
523 |
||
524 |
goal ZF.thy "{f(x).x:A}=0 <-> A=0"; |
|
525 |
by (fast_tac (eq_cs addSEs [equalityE]) 1); |
|
526 |
qed "RepFun_eq_0_iff"; |
|
527 |
||
528 |
goal ZF.thy "{f(x).x:0} = 0"; |
|
529 |
by (fast_tac eq_cs 1); |
|
530 |
qed "RepFun_0"; |
|
1611 | 531 |
|
532 |
(** Collect **) |
|
533 |
||
534 |
goal ZF.thy "Collect(A Un B, P) = Collect(A,P) Un Collect(B,P)"; |
|
535 |
by (fast_tac eq_cs 1); |
|
536 |
qed "Collect_Un"; |
|
537 |
||
538 |
goal ZF.thy "Collect(A Int B, P) = Collect(A,P) Int Collect(B,P)"; |
|
539 |
by (fast_tac eq_cs 1); |
|
540 |
qed "Collect_Int"; |
|
541 |
||
542 |
goal ZF.thy "Collect(A - B, P) = Collect(A,P) - Collect(B,P)"; |
|
543 |
by (fast_tac eq_cs 1); |
|
544 |
qed "Collect_Diff"; |
|
545 |
||
546 |
goal ZF.thy |
|
547 |
"{x:cons(a,B). P(x)} = if(P(a), cons(a, {x:B. P(x)}), {x:B. P(x)})"; |
|
548 |
by (simp_tac (FOL_ss setloop split_tac [expand_if]) 1); |
|
549 |
by (fast_tac eq_cs 1); |
|
550 |
qed "Collect_cons"; |
|
551 |