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