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