author | clasohm |
Wed, 07 Dec 1994 13:12:04 +0100 | |
changeset 760 | f0200e91b272 |
parent 685 | 0727f0c0c4f0 |
child 787 | 1affbb1c5f1f |
permissions | -rw-r--r-- |
0 | 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 |
||
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 |
|
0 | 70 |
(** Binary Union **) |
71 |
||
72 |
goal ZF.thy "0 Un A = A"; |
|
73 |
by (fast_tac eq_cs 1); |
|
760 | 74 |
qed "Un_0"; |
0 | 75 |
|
76 |
goal ZF.thy "cons(a,B) Un C = cons(a, B Un C)"; |
|
77 |
by (fast_tac eq_cs 1); |
|
760 | 78 |
qed "Un_cons"; |
0 | 79 |
|
80 |
goal ZF.thy "A Un A = A"; |
|
81 |
by (fast_tac eq_cs 1); |
|
760 | 82 |
qed "Un_absorb"; |
0 | 83 |
|
84 |
goal ZF.thy "A Un B = B Un A"; |
|
85 |
by (fast_tac eq_cs 1); |
|
760 | 86 |
qed "Un_commute"; |
0 | 87 |
|
88 |
goal ZF.thy "(A Un B) Un C = A Un (B Un C)"; |
|
89 |
by (fast_tac eq_cs 1); |
|
760 | 90 |
qed "Un_assoc"; |
0 | 91 |
|
92 |
goal ZF.thy "(A Int B) Un C = (A Un C) Int (B Un C)"; |
|
93 |
by (fast_tac eq_cs 1); |
|
760 | 94 |
qed "Un_Int_distrib"; |
0 | 95 |
|
96 |
goal ZF.thy "A<=B <-> A Un B = B"; |
|
97 |
by (fast_tac (eq_cs addSEs [equalityE]) 1); |
|
760 | 98 |
qed "subset_Un_iff"; |
0 | 99 |
|
435 | 100 |
goal ZF.thy "A<=B <-> B Un A = B"; |
101 |
by (fast_tac (eq_cs addSEs [equalityE]) 1); |
|
760 | 102 |
qed "subset_Un_iff2"; |
435 | 103 |
|
0 | 104 |
(** Simple properties of Diff -- set difference **) |
105 |
||
106 |
goal ZF.thy "A-A = 0"; |
|
107 |
by (fast_tac eq_cs 1); |
|
760 | 108 |
qed "Diff_cancel"; |
0 | 109 |
|
110 |
goal ZF.thy "0-A = 0"; |
|
111 |
by (fast_tac eq_cs 1); |
|
760 | 112 |
qed "empty_Diff"; |
0 | 113 |
|
114 |
goal ZF.thy "A-0 = A"; |
|
115 |
by (fast_tac eq_cs 1); |
|
760 | 116 |
qed "Diff_0"; |
0 | 117 |
|
118 |
(*NOT SUITABLE FOR REWRITING since {a} == cons(a,0)*) |
|
119 |
goal ZF.thy "A - cons(a,B) = A - B - {a}"; |
|
120 |
by (fast_tac eq_cs 1); |
|
760 | 121 |
qed "Diff_cons"; |
0 | 122 |
|
123 |
(*NOT SUITABLE FOR REWRITING since {a} == cons(a,0)*) |
|
124 |
goal ZF.thy "A - cons(a,B) = A - {a} - B"; |
|
125 |
by (fast_tac eq_cs 1); |
|
760 | 126 |
qed "Diff_cons2"; |
0 | 127 |
|
128 |
goal ZF.thy "A Int (B-A) = 0"; |
|
129 |
by (fast_tac eq_cs 1); |
|
760 | 130 |
qed "Diff_disjoint"; |
0 | 131 |
|
132 |
goal ZF.thy "!!A B. A<=B ==> A Un (B-A) = B"; |
|
133 |
by (fast_tac eq_cs 1); |
|
760 | 134 |
qed "Diff_partition"; |
0 | 135 |
|
268 | 136 |
goal ZF.thy "!!A B. [| A<=B; B<=C |] ==> B-(C-A) = A"; |
0 | 137 |
by (fast_tac eq_cs 1); |
760 | 138 |
qed "double_complement"; |
0 | 139 |
|
268 | 140 |
goal ZF.thy "(A Un B) - (B-A) = A"; |
141 |
by (fast_tac eq_cs 1); |
|
760 | 142 |
qed "double_complement_Un"; |
268 | 143 |
|
0 | 144 |
goal ZF.thy |
145 |
"(A Int B) Un (B Int C) Un (C Int A) = (A Un B) Int (B Un C) Int (C Un A)"; |
|
146 |
by (fast_tac eq_cs 1); |
|
760 | 147 |
qed "Un_Int_crazy"; |
0 | 148 |
|
149 |
goal ZF.thy "A - (B Un C) = (A-B) Int (A-C)"; |
|
150 |
by (fast_tac eq_cs 1); |
|
760 | 151 |
qed "Diff_Un"; |
0 | 152 |
|
153 |
goal ZF.thy "A - (B Int C) = (A-B) Un (A-C)"; |
|
154 |
by (fast_tac eq_cs 1); |
|
760 | 155 |
qed "Diff_Int"; |
0 | 156 |
|
157 |
(*Halmos, Naive Set Theory, page 16.*) |
|
158 |
goal ZF.thy "(A Int B) Un C = A Int (B Un C) <-> C<=A"; |
|
159 |
by (fast_tac (eq_cs addSEs [equalityE]) 1); |
|
760 | 160 |
qed "Un_Int_assoc_iff"; |
0 | 161 |
|
162 |
||
163 |
(** Big Union and Intersection **) |
|
164 |
||
165 |
goal ZF.thy "Union(0) = 0"; |
|
166 |
by (fast_tac eq_cs 1); |
|
760 | 167 |
qed "Union_0"; |
0 | 168 |
|
169 |
goal ZF.thy "Union(cons(a,B)) = a Un Union(B)"; |
|
170 |
by (fast_tac eq_cs 1); |
|
760 | 171 |
qed "Union_cons"; |
0 | 172 |
|
173 |
goal ZF.thy "Union(A Un B) = Union(A) Un Union(B)"; |
|
174 |
by (fast_tac eq_cs 1); |
|
760 | 175 |
qed "Union_Un_distrib"; |
0 | 176 |
|
435 | 177 |
goal ZF.thy "Union(A Int B) <= Union(A) Int Union(B)"; |
178 |
by (fast_tac ZF_cs 1); |
|
760 | 179 |
qed "Union_Int_subset"; |
435 | 180 |
|
0 | 181 |
goal ZF.thy "Union(C) Int A = 0 <-> (ALL B:C. B Int A = 0)"; |
182 |
by (fast_tac (eq_cs addSEs [equalityE]) 1); |
|
760 | 183 |
qed "Union_disjoint"; |
0 | 184 |
|
185 |
(* A good challenge: Inter is ill-behaved on the empty set *) |
|
186 |
goal ZF.thy "!!A B. [| a:A; b:B |] ==> Inter(A Un B) = Inter(A) Int Inter(B)"; |
|
187 |
by (fast_tac eq_cs 1); |
|
760 | 188 |
qed "Inter_Un_distrib"; |
0 | 189 |
|
190 |
goal ZF.thy "Union({b}) = b"; |
|
191 |
by (fast_tac eq_cs 1); |
|
760 | 192 |
qed "Union_singleton"; |
0 | 193 |
|
194 |
goal ZF.thy "Inter({b}) = b"; |
|
195 |
by (fast_tac eq_cs 1); |
|
760 | 196 |
qed "Inter_singleton"; |
0 | 197 |
|
198 |
(** Unions and Intersections of Families **) |
|
199 |
||
200 |
goal ZF.thy "Union(A) = (UN x:A. x)"; |
|
201 |
by (fast_tac eq_cs 1); |
|
760 | 202 |
qed "Union_eq_UN"; |
0 | 203 |
|
204 |
goalw ZF.thy [Inter_def] "Inter(A) = (INT x:A. x)"; |
|
205 |
by (fast_tac eq_cs 1); |
|
760 | 206 |
qed "Inter_eq_INT"; |
0 | 207 |
|
517 | 208 |
goal ZF.thy "(UN i:0. A(i)) = 0"; |
209 |
by (fast_tac eq_cs 1); |
|
760 | 210 |
qed "UN_0"; |
517 | 211 |
|
0 | 212 |
(*Halmos, Naive Set Theory, page 35.*) |
213 |
goal ZF.thy "B Int (UN i:I. A(i)) = (UN i:I. B Int A(i))"; |
|
214 |
by (fast_tac eq_cs 1); |
|
760 | 215 |
qed "Int_UN_distrib"; |
0 | 216 |
|
217 |
goal ZF.thy "!!A B. i:I ==> B Un (INT i:I. A(i)) = (INT i:I. B Un A(i))"; |
|
218 |
by (fast_tac eq_cs 1); |
|
760 | 219 |
qed "Un_INT_distrib"; |
0 | 220 |
|
221 |
goal ZF.thy |
|
222 |
"(UN i:I. A(i)) Int (UN j:J. B(j)) = (UN i:I. UN j:J. A(i) Int B(j))"; |
|
223 |
by (fast_tac eq_cs 1); |
|
760 | 224 |
qed "Int_UN_distrib2"; |
0 | 225 |
|
226 |
goal ZF.thy |
|
227 |
"!!I J. [| i:I; j:J |] ==> \ |
|
228 |
\ (INT i:I. A(i)) Un (INT j:J. B(j)) = (INT i:I. INT j:J. A(i) Un B(j))"; |
|
229 |
by (fast_tac eq_cs 1); |
|
760 | 230 |
qed "Un_INT_distrib2"; |
0 | 231 |
|
435 | 232 |
goal ZF.thy "!!A. a: A ==> (UN y:A. c) = c"; |
233 |
by (fast_tac eq_cs 1); |
|
760 | 234 |
qed "UN_constant"; |
0 | 235 |
|
435 | 236 |
goal ZF.thy "!!A. a: A ==> (INT y:A. c) = c"; |
237 |
by (fast_tac eq_cs 1); |
|
760 | 238 |
qed "INT_constant"; |
0 | 239 |
|
240 |
(** Devlin, Fundamentals of Contemporary Set Theory, page 12, exercise 5: |
|
241 |
Union of a family of unions **) |
|
242 |
||
192 | 243 |
goal ZF.thy "(UN i:I. A(i) Un B(i)) = (UN i:I. A(i)) Un (UN i:I. B(i))"; |
0 | 244 |
by (fast_tac eq_cs 1); |
760 | 245 |
qed "UN_Un_distrib"; |
0 | 246 |
|
247 |
goal ZF.thy |
|
248 |
"!!A B. i:I ==> \ |
|
192 | 249 |
\ (INT i:I. A(i) Int B(i)) = (INT i:I. A(i)) Int (INT i:I. B(i))"; |
0 | 250 |
by (fast_tac eq_cs 1); |
760 | 251 |
qed "INT_Int_distrib"; |
0 | 252 |
|
253 |
(** Devlin, page 12, exercise 5: Complements **) |
|
254 |
||
255 |
goal ZF.thy "!!A B. i:I ==> B - (UN i:I. A(i)) = (INT i:I. B - A(i))"; |
|
256 |
by (fast_tac eq_cs 1); |
|
760 | 257 |
qed "Diff_UN"; |
0 | 258 |
|
259 |
goal ZF.thy "!!A B. i:I ==> B - (INT i:I. A(i)) = (UN i:I. B - A(i))"; |
|
260 |
by (fast_tac eq_cs 1); |
|
760 | 261 |
qed "Diff_INT"; |
0 | 262 |
|
263 |
(** Unions and Intersections with General Sum **) |
|
264 |
||
520 | 265 |
goal ZF.thy "Sigma(cons(a,B), C) = ({a}*C(a)) Un Sigma(B,C)"; |
266 |
by (fast_tac eq_cs 1); |
|
760 | 267 |
qed "Sigma_cons"; |
520 | 268 |
|
182 | 269 |
goal ZF.thy "(SUM x:(UN y:A. C(y)). B(x)) = (UN y:A. SUM x:C(y). B(x))"; |
270 |
by (fast_tac eq_cs 1); |
|
760 | 271 |
qed "SUM_UN_distrib1"; |
182 | 272 |
|
192 | 273 |
goal ZF.thy "(SUM i:I. UN j:J. C(i,j)) = (UN j:J. SUM i:I. C(i,j))"; |
182 | 274 |
by (fast_tac eq_cs 1); |
760 | 275 |
qed "SUM_UN_distrib2"; |
182 | 276 |
|
192 | 277 |
goal ZF.thy "(SUM i:I Un J. C(i)) = (SUM i:I. C(i)) Un (SUM j:J. C(j))"; |
0 | 278 |
by (fast_tac eq_cs 1); |
760 | 279 |
qed "SUM_Un_distrib1"; |
0 | 280 |
|
192 | 281 |
goal ZF.thy "(SUM i:I. A(i) Un B(i)) = (SUM i:I. A(i)) Un (SUM i:I. B(i))"; |
0 | 282 |
by (fast_tac eq_cs 1); |
760 | 283 |
qed "SUM_Un_distrib2"; |
0 | 284 |
|
685 | 285 |
(*First-order version of the above, for rewriting*) |
286 |
goal ZF.thy "I * (A Un B) = I*A Un I*B"; |
|
287 |
by (resolve_tac [SUM_Un_distrib2] 1); |
|
760 | 288 |
qed "prod_Un_distrib2"; |
685 | 289 |
|
192 | 290 |
goal ZF.thy "(SUM i:I Int J. C(i)) = (SUM i:I. C(i)) Int (SUM j:J. C(j))"; |
0 | 291 |
by (fast_tac eq_cs 1); |
760 | 292 |
qed "SUM_Int_distrib1"; |
0 | 293 |
|
294 |
goal ZF.thy |
|
192 | 295 |
"(SUM i:I. A(i) Int B(i)) = (SUM i:I. A(i)) Int (SUM i:I. B(i))"; |
0 | 296 |
by (fast_tac eq_cs 1); |
760 | 297 |
qed "SUM_Int_distrib2"; |
0 | 298 |
|
685 | 299 |
(*First-order version of the above, for rewriting*) |
300 |
goal ZF.thy "I * (A Int B) = I*A Int I*B"; |
|
301 |
by (resolve_tac [SUM_Int_distrib2] 1); |
|
760 | 302 |
qed "prod_Int_distrib2"; |
685 | 303 |
|
192 | 304 |
(*Cf Aczel, Non-Well-Founded Sets, page 115*) |
305 |
goal ZF.thy "(SUM i:I. A(i)) = (UN i:I. {i} * A(i))"; |
|
306 |
by (fast_tac eq_cs 1); |
|
760 | 307 |
qed "SUM_eq_UN"; |
192 | 308 |
|
536
5fbfa997f1b0
ZF/domrange/domain_of_prod, domain_empty, etc: moved to equalities.ML where
lcp
parents:
520
diff
changeset
|
309 |
(** Domain **) |
5fbfa997f1b0
ZF/domrange/domain_of_prod, domain_empty, etc: moved to equalities.ML where
lcp
parents:
520
diff
changeset
|
310 |
|
760 | 311 |
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
|
312 |
(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
|
313 |
|
760 | 314 |
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
|
315 |
(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
|
316 |
|
760 | 317 |
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
|
318 |
"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
|
319 |
(fn _ => [ fast_tac eq_cs 1 ]); |
0 | 320 |
|
321 |
goal ZF.thy "domain(A Un B) = domain(A) Un domain(B)"; |
|
322 |
by (fast_tac eq_cs 1); |
|
760 | 323 |
qed "domain_Un_eq"; |
0 | 324 |
|
325 |
goal ZF.thy "domain(A Int B) <= domain(A) Int domain(B)"; |
|
326 |
by (fast_tac eq_cs 1); |
|
760 | 327 |
qed "domain_Int_subset"; |
0 | 328 |
|
329 |
goal ZF.thy "domain(A) - domain(B) <= domain(A - B)"; |
|
330 |
by (fast_tac eq_cs 1); |
|
760 | 331 |
qed "domain_diff_subset"; |
0 | 332 |
|
685 | 333 |
goal ZF.thy "domain(converse(r)) = range(r)"; |
334 |
by (fast_tac eq_cs 1); |
|
760 | 335 |
qed "domain_converse"; |
685 | 336 |
|
337 |
||
338 |
||
536
5fbfa997f1b0
ZF/domrange/domain_of_prod, domain_empty, etc: moved to equalities.ML where
lcp
parents:
520
diff
changeset
|
339 |
(** Range **) |
5fbfa997f1b0
ZF/domrange/domain_of_prod, domain_empty, etc: moved to equalities.ML where
lcp
parents:
520
diff
changeset
|
340 |
|
760 | 341 |
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
|
342 |
"!!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
|
343 |
(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
|
344 |
|
760 | 345 |
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
|
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 "range_cons" ZF.thy |
536
5fbfa997f1b0
ZF/domrange/domain_of_prod, domain_empty, etc: moved to equalities.ML where
lcp
parents:
520
diff
changeset
|
349 |
"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
|
350 |
(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
|
351 |
|
0 | 352 |
goal ZF.thy "range(A Un B) = range(A) Un range(B)"; |
353 |
by (fast_tac eq_cs 1); |
|
760 | 354 |
qed "range_Un_eq"; |
0 | 355 |
|
356 |
goal ZF.thy "range(A Int B) <= range(A) Int range(B)"; |
|
435 | 357 |
by (fast_tac ZF_cs 1); |
760 | 358 |
qed "range_Int_subset"; |
0 | 359 |
|
360 |
goal ZF.thy "range(A) - range(B) <= range(A - B)"; |
|
361 |
by (fast_tac eq_cs 1); |
|
760 | 362 |
qed "range_diff_subset"; |
0 | 363 |
|
685 | 364 |
goal ZF.thy "range(converse(r)) = domain(r)"; |
365 |
by (fast_tac eq_cs 1); |
|
760 | 366 |
qed "range_converse"; |
685 | 367 |
|
536
5fbfa997f1b0
ZF/domrange/domain_of_prod, domain_empty, etc: moved to equalities.ML where
lcp
parents:
520
diff
changeset
|
368 |
(** Field **) |
5fbfa997f1b0
ZF/domrange/domain_of_prod, domain_empty, etc: moved to equalities.ML where
lcp
parents:
520
diff
changeset
|
369 |
|
760 | 370 |
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
|
371 |
(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
|
372 |
|
760 | 373 |
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
|
374 |
(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
|
375 |
|
760 | 376 |
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
|
377 |
"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
|
378 |
(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
|
379 |
|
0 | 380 |
goal ZF.thy "field(A Un B) = field(A) Un field(B)"; |
381 |
by (fast_tac eq_cs 1); |
|
760 | 382 |
qed "field_Un_eq"; |
0 | 383 |
|
384 |
goal ZF.thy "field(A Int B) <= field(A) Int field(B)"; |
|
385 |
by (fast_tac eq_cs 1); |
|
760 | 386 |
qed "field_Int_subset"; |
0 | 387 |
|
388 |
goal ZF.thy "field(A) - field(B) <= field(A - B)"; |
|
389 |
by (fast_tac eq_cs 1); |
|
760 | 390 |
qed "field_diff_subset"; |
0 | 391 |
|
392 |
||
435 | 393 |
(** Image **) |
394 |
||
395 |
goal ZF.thy "r``0 = 0"; |
|
396 |
by (fast_tac eq_cs 1); |
|
760 | 397 |
qed "image_0"; |
435 | 398 |
|
399 |
goal ZF.thy "r``(A Un B) = (r``A) Un (r``B)"; |
|
400 |
by (fast_tac eq_cs 1); |
|
760 | 401 |
qed "image_Un"; |
435 | 402 |
|
403 |
goal ZF.thy "r``(A Int B) <= (r``A) Int (r``B)"; |
|
404 |
by (fast_tac ZF_cs 1); |
|
760 | 405 |
qed "image_Int_subset"; |
435 | 406 |
|
407 |
goal ZF.thy "(r Int A*A)``B <= (r``B) Int A"; |
|
408 |
by (fast_tac ZF_cs 1); |
|
760 | 409 |
qed "image_Int_square_subset"; |
435 | 410 |
|
411 |
goal ZF.thy "!!r. B<=A ==> (r Int A*A)``B = (r``B) Int A"; |
|
412 |
by (fast_tac eq_cs 1); |
|
760 | 413 |
qed "image_Int_square"; |
435 | 414 |
|
415 |
||
416 |
(** Inverse Image **) |
|
417 |
||
418 |
goal ZF.thy "r-``0 = 0"; |
|
419 |
by (fast_tac eq_cs 1); |
|
760 | 420 |
qed "vimage_0"; |
435 | 421 |
|
422 |
goal ZF.thy "r-``(A Un B) = (r-``A) Un (r-``B)"; |
|
423 |
by (fast_tac eq_cs 1); |
|
760 | 424 |
qed "vimage_Un"; |
435 | 425 |
|
426 |
goal ZF.thy "r-``(A Int B) <= (r-``A) Int (r-``B)"; |
|
427 |
by (fast_tac ZF_cs 1); |
|
760 | 428 |
qed "vimage_Int_subset"; |
435 | 429 |
|
430 |
goal ZF.thy "(r Int A*A)-``B <= (r-``B) Int A"; |
|
431 |
by (fast_tac ZF_cs 1); |
|
760 | 432 |
qed "vimage_Int_square_subset"; |
435 | 433 |
|
434 |
goal ZF.thy "!!r. B<=A ==> (r Int A*A)-``B = (r-``B) Int A"; |
|
435 |
by (fast_tac eq_cs 1); |
|
760 | 436 |
qed "vimage_Int_square"; |
435 | 437 |
|
438 |
||
0 | 439 |
(** Converse **) |
440 |
||
441 |
goal ZF.thy "converse(A Un B) = converse(A) Un converse(B)"; |
|
442 |
by (fast_tac eq_cs 1); |
|
760 | 443 |
qed "converse_Un"; |
0 | 444 |
|
445 |
goal ZF.thy "converse(A Int B) = converse(A) Int converse(B)"; |
|
446 |
by (fast_tac eq_cs 1); |
|
760 | 447 |
qed "converse_Int"; |
0 | 448 |
|
449 |
goal ZF.thy "converse(A) - converse(B) = converse(A - B)"; |
|
450 |
by (fast_tac eq_cs 1); |
|
760 | 451 |
qed "converse_diff"; |
0 | 452 |
|
198 | 453 |
(** Pow **) |
454 |
||
455 |
goal ZF.thy "Pow(A) Un Pow(B) <= Pow(A Un B)"; |
|
456 |
by (fast_tac upair_cs 1); |
|
760 | 457 |
qed "Un_Pow_subset"; |
198 | 458 |
|
459 |
goal ZF.thy "(UN x:A. Pow(B(x))) <= Pow(UN x:A. B(x))"; |
|
460 |
by (fast_tac upair_cs 1); |
|
760 | 461 |
qed "UN_Pow_subset"; |
198 | 462 |
|
463 |
goal ZF.thy "A <= Pow(Union(A))"; |
|
464 |
by (fast_tac upair_cs 1); |
|
760 | 465 |
qed "subset_Pow_Union"; |
198 | 466 |
|
467 |
goal ZF.thy "Union(Pow(A)) = A"; |
|
468 |
by (fast_tac eq_cs 1); |
|
760 | 469 |
qed "Union_Pow_eq"; |
198 | 470 |
|
471 |
goal ZF.thy "Pow(A) Int Pow(B) = Pow(A Int B)"; |
|
472 |
by (fast_tac eq_cs 1); |
|
760 | 473 |
qed "Int_Pow_eq"; |
198 | 474 |
|
475 |
goal ZF.thy "!!x A. x:A ==> (INT x:A. Pow(B(x))) = Pow(INT x:A. B(x))"; |
|
476 |
by (fast_tac eq_cs 1); |
|
760 | 477 |
qed "INT_Pow_subset"; |
435 | 478 |