author  paulson 
Mon, 11 Mar 1996 14:19:12 +0100  
changeset 1568  630d881b51bd 
parent 1461  6bcb44e4d6e5 
child 1611  35e0fd1b1775 
permissions  rwrr 
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 ==> (AB) Int C = CB"; 
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 "AA = 0"; 

111 
by (fast_tac eq_cs 1); 

760  112 
qed "Diff_cancel"; 
0  113 

114 
goal ZF.thy "0A = 0"; 

115 
by (fast_tac eq_cs 1); 

760  116 
qed "empty_Diff"; 
0  117 

118 
goal ZF.thy "A0 = A"; 

119 
by (fast_tac eq_cs 1); 

760  120 
qed "Diff_0"; 
0  121 

787  122 
goal ZF.thy "AB=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 (BA) = 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 (BA) = 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(CA) = A"; 
0  145 
by (fast_tac eq_cs 1); 
760  146 
qed "double_complement"; 
0  147 

268  148 
goal ZF.thy "(A Un B)  (BA) = 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) = (AB) Int (AC)"; 

158 
by (fast_tac eq_cs 1); 

760  159 
qed "Diff_Un"; 
0  160 

161 
goal ZF.thy "A  (B Int C) = (AB) Un (AC)"; 

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 

1568  193 
goal ZF.thy "!!A B. [ z:A; z:B ] ==> Inter(A) Un Inter(B) <= Inter(A Int B)"; 
194 
by (fast_tac ZF_cs 1); 

195 
qed "Inter_Un_subset"; 

196 

0  197 
(* A good challenge: Inter is illbehaved on the empty set *) 
198 
goal ZF.thy "!!A B. [ a:A; b:B ] ==> Inter(A Un B) = Inter(A) Int Inter(B)"; 

199 
by (fast_tac eq_cs 1); 

760  200 
qed "Inter_Un_distrib"; 
0  201 

202 
goal ZF.thy "Union({b}) = b"; 

203 
by (fast_tac eq_cs 1); 

760  204 
qed "Union_singleton"; 
0  205 

206 
goal ZF.thy "Inter({b}) = b"; 

207 
by (fast_tac eq_cs 1); 

760  208 
qed "Inter_singleton"; 
0  209 

210 
(** Unions and Intersections of Families **) 

211 

212 
goal ZF.thy "Union(A) = (UN x:A. x)"; 

213 
by (fast_tac eq_cs 1); 

760  214 
qed "Union_eq_UN"; 
0  215 

216 
goalw ZF.thy [Inter_def] "Inter(A) = (INT x:A. x)"; 

217 
by (fast_tac eq_cs 1); 

760  218 
qed "Inter_eq_INT"; 
0  219 

517  220 
goal ZF.thy "(UN i:0. A(i)) = 0"; 
221 
by (fast_tac eq_cs 1); 

760  222 
qed "UN_0"; 
517  223 

0  224 
(*Halmos, Naive Set Theory, page 35.*) 
225 
goal ZF.thy "B Int (UN i:I. A(i)) = (UN i:I. B Int A(i))"; 

226 
by (fast_tac eq_cs 1); 

760  227 
qed "Int_UN_distrib"; 
0  228 

229 
goal ZF.thy "!!A B. i:I ==> B Un (INT i:I. A(i)) = (INT i:I. B Un A(i))"; 

230 
by (fast_tac eq_cs 1); 

760  231 
qed "Un_INT_distrib"; 
0  232 

233 
goal ZF.thy 

234 
"(UN i:I. A(i)) Int (UN j:J. B(j)) = (UN i:I. UN j:J. A(i) Int B(j))"; 

235 
by (fast_tac eq_cs 1); 

760  236 
qed "Int_UN_distrib2"; 
0  237 

238 
goal ZF.thy 

239 
"!!I J. [ i:I; j:J ] ==> \ 

240 
\ (INT i:I. A(i)) Un (INT j:J. B(j)) = (INT i:I. INT j:J. A(i) Un B(j))"; 

241 
by (fast_tac eq_cs 1); 

760  242 
qed "Un_INT_distrib2"; 
0  243 

435  244 
goal ZF.thy "!!A. a: A ==> (UN y:A. c) = c"; 
245 
by (fast_tac eq_cs 1); 

760  246 
qed "UN_constant"; 
0  247 

435  248 
goal ZF.thy "!!A. a: A ==> (INT y:A. c) = c"; 
249 
by (fast_tac eq_cs 1); 

760  250 
qed "INT_constant"; 
0  251 

252 
(** Devlin, Fundamentals of Contemporary Set Theory, page 12, exercise 5: 

253 
Union of a family of unions **) 

254 

192  255 
goal ZF.thy "(UN i:I. A(i) Un B(i)) = (UN i:I. A(i)) Un (UN i:I. B(i))"; 
0  256 
by (fast_tac eq_cs 1); 
760  257 
qed "UN_Un_distrib"; 
0  258 

259 
goal ZF.thy 

260 
"!!A B. i:I ==> \ 

192  261 
\ (INT i:I. A(i) Int B(i)) = (INT i:I. A(i)) Int (INT i:I. B(i))"; 
0  262 
by (fast_tac eq_cs 1); 
760  263 
qed "INT_Int_distrib"; 
0  264 

265 
(** Devlin, page 12, exercise 5: Complements **) 

266 

267 
goal ZF.thy "!!A B. i:I ==> B  (UN i:I. A(i)) = (INT i:I. B  A(i))"; 

268 
by (fast_tac eq_cs 1); 

760  269 
qed "Diff_UN"; 
0  270 

271 
goal ZF.thy "!!A B. i:I ==> B  (INT i:I. A(i)) = (UN i:I. B  A(i))"; 

272 
by (fast_tac eq_cs 1); 

760  273 
qed "Diff_INT"; 
0  274 

275 
(** Unions and Intersections with General Sum **) 

276 

520  277 
goal ZF.thy "Sigma(cons(a,B), C) = ({a}*C(a)) Un Sigma(B,C)"; 
278 
by (fast_tac eq_cs 1); 

760  279 
qed "Sigma_cons"; 
520  280 

182  281 
goal ZF.thy "(SUM x:(UN y:A. C(y)). B(x)) = (UN y:A. SUM x:C(y). B(x))"; 
282 
by (fast_tac eq_cs 1); 

760  283 
qed "SUM_UN_distrib1"; 
182  284 

192  285 
goal ZF.thy "(SUM i:I. UN j:J. C(i,j)) = (UN j:J. SUM i:I. C(i,j))"; 
182  286 
by (fast_tac eq_cs 1); 
760  287 
qed "SUM_UN_distrib2"; 
182  288 

192  289 
goal ZF.thy "(SUM i:I Un J. C(i)) = (SUM i:I. C(i)) Un (SUM j:J. C(j))"; 
0  290 
by (fast_tac eq_cs 1); 
760  291 
qed "SUM_Un_distrib1"; 
0  292 

192  293 
goal ZF.thy "(SUM i:I. A(i) Un B(i)) = (SUM i:I. A(i)) Un (SUM i:I. B(i))"; 
0  294 
by (fast_tac eq_cs 1); 
760  295 
qed "SUM_Un_distrib2"; 
0  296 

685  297 
(*Firstorder version of the above, for rewriting*) 
298 
goal ZF.thy "I * (A Un B) = I*A Un I*B"; 

1461  299 
by (rtac SUM_Un_distrib2 1); 
760  300 
qed "prod_Un_distrib2"; 
685  301 

192  302 
goal ZF.thy "(SUM i:I Int J. C(i)) = (SUM i:I. C(i)) Int (SUM j:J. C(j))"; 
0  303 
by (fast_tac eq_cs 1); 
760  304 
qed "SUM_Int_distrib1"; 
0  305 

306 
goal ZF.thy 

192  307 
"(SUM i:I. A(i) Int B(i)) = (SUM i:I. A(i)) Int (SUM i:I. B(i))"; 
0  308 
by (fast_tac eq_cs 1); 
760  309 
qed "SUM_Int_distrib2"; 
0  310 

685  311 
(*Firstorder version of the above, for rewriting*) 
312 
goal ZF.thy "I * (A Int B) = I*A Int I*B"; 

1461  313 
by (rtac SUM_Int_distrib2 1); 
760  314 
qed "prod_Int_distrib2"; 
685  315 

192  316 
(*Cf Aczel, NonWellFounded Sets, page 115*) 
317 
goal ZF.thy "(SUM i:I. A(i)) = (UN i:I. {i} * A(i))"; 

318 
by (fast_tac eq_cs 1); 

760  319 
qed "SUM_eq_UN"; 
192  320 

536
5fbfa997f1b0
ZF/domrange/domain_of_prod, domain_empty, etc: moved to equalities.ML where
lcp
parents:
520
diff
changeset

321 
(** Domain **) 
5fbfa997f1b0
ZF/domrange/domain_of_prod, domain_empty, etc: moved to equalities.ML where
lcp
parents:
520
diff
changeset

322 

760  323 
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

324 
(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

325 

760  326 
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

327 
(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

328 

760  329 
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

330 
"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

331 
(fn _ => [ fast_tac eq_cs 1 ]); 
0  332 

333 
goal ZF.thy "domain(A Un B) = domain(A) Un domain(B)"; 

334 
by (fast_tac eq_cs 1); 

760  335 
qed "domain_Un_eq"; 
0  336 

337 
goal ZF.thy "domain(A Int B) <= domain(A) Int domain(B)"; 

338 
by (fast_tac eq_cs 1); 

760  339 
qed "domain_Int_subset"; 
0  340 

341 
goal ZF.thy "domain(A)  domain(B) <= domain(A  B)"; 

342 
by (fast_tac eq_cs 1); 

1056  343 
qed "domain_Diff_subset"; 
0  344 

685  345 
goal ZF.thy "domain(converse(r)) = range(r)"; 
346 
by (fast_tac eq_cs 1); 

760  347 
qed "domain_converse"; 
685  348 

349 

350 

536
5fbfa997f1b0
ZF/domrange/domain_of_prod, domain_empty, etc: moved to equalities.ML where
lcp
parents:
520
diff
changeset

351 
(** Range **) 
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_of_prod" ZF.thy 
536
5fbfa997f1b0
ZF/domrange/domain_of_prod, domain_empty, etc: moved to equalities.ML where
lcp
parents:
520
diff
changeset

354 
"!!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

355 
(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

356 

760  357 
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

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 

760  360 
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

361 
"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

362 
(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

363 

0  364 
goal ZF.thy "range(A Un B) = range(A) Un range(B)"; 
365 
by (fast_tac eq_cs 1); 

760  366 
qed "range_Un_eq"; 
0  367 

368 
goal ZF.thy "range(A Int B) <= range(A) Int range(B)"; 

435  369 
by (fast_tac ZF_cs 1); 
760  370 
qed "range_Int_subset"; 
0  371 

372 
goal ZF.thy "range(A)  range(B) <= range(A  B)"; 

373 
by (fast_tac eq_cs 1); 

1056  374 
qed "range_Diff_subset"; 
0  375 

685  376 
goal ZF.thy "range(converse(r)) = domain(r)"; 
377 
by (fast_tac eq_cs 1); 

760  378 
qed "range_converse"; 
685  379 

536
5fbfa997f1b0
ZF/domrange/domain_of_prod, domain_empty, etc: moved to equalities.ML where
lcp
parents:
520
diff
changeset

380 
(** Field **) 
5fbfa997f1b0
ZF/domrange/domain_of_prod, domain_empty, etc: moved to equalities.ML where
lcp
parents:
520
diff
changeset

381 

760  382 
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

383 
(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

384 

760  385 
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

386 
(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

387 

760  388 
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

389 
"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

390 
(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

391 

0  392 
goal ZF.thy "field(A Un B) = field(A) Un field(B)"; 
393 
by (fast_tac eq_cs 1); 

760  394 
qed "field_Un_eq"; 
0  395 

396 
goal ZF.thy "field(A Int B) <= field(A) Int field(B)"; 

397 
by (fast_tac eq_cs 1); 

760  398 
qed "field_Int_subset"; 
0  399 

400 
goal ZF.thy "field(A)  field(B) <= field(A  B)"; 

401 
by (fast_tac eq_cs 1); 

1056  402 
qed "field_Diff_subset"; 
0  403 

404 

435  405 
(** Image **) 
406 

407 
goal ZF.thy "r``0 = 0"; 

408 
by (fast_tac eq_cs 1); 

760  409 
qed "image_0"; 
435  410 

411 
goal ZF.thy "r``(A Un B) = (r``A) Un (r``B)"; 

412 
by (fast_tac eq_cs 1); 

760  413 
qed "image_Un"; 
435  414 

415 
goal ZF.thy "r``(A Int B) <= (r``A) Int (r``B)"; 

416 
by (fast_tac ZF_cs 1); 

760  417 
qed "image_Int_subset"; 
435  418 

419 
goal ZF.thy "(r Int A*A)``B <= (r``B) Int A"; 

420 
by (fast_tac ZF_cs 1); 

760  421 
qed "image_Int_square_subset"; 
435  422 

423 
goal ZF.thy "!!r. B<=A ==> (r Int A*A)``B = (r``B) Int A"; 

424 
by (fast_tac eq_cs 1); 

760  425 
qed "image_Int_square"; 
435  426 

427 

428 
(** Inverse Image **) 

429 

430 
goal ZF.thy "r``0 = 0"; 

431 
by (fast_tac eq_cs 1); 

760  432 
qed "vimage_0"; 
435  433 

434 
goal ZF.thy "r``(A Un B) = (r``A) Un (r``B)"; 

435 
by (fast_tac eq_cs 1); 

760  436 
qed "vimage_Un"; 
435  437 

438 
goal ZF.thy "r``(A Int B) <= (r``A) Int (r``B)"; 

439 
by (fast_tac ZF_cs 1); 

760  440 
qed "vimage_Int_subset"; 
435  441 

442 
goal ZF.thy "(r Int A*A)``B <= (r``B) Int A"; 

443 
by (fast_tac ZF_cs 1); 

760  444 
qed "vimage_Int_square_subset"; 
435  445 

446 
goal ZF.thy "!!r. B<=A ==> (r Int A*A)``B = (r``B) Int A"; 

447 
by (fast_tac eq_cs 1); 

760  448 
qed "vimage_Int_square"; 
435  449 

450 

0  451 
(** Converse **) 
452 

453 
goal ZF.thy "converse(A Un B) = converse(A) Un converse(B)"; 

454 
by (fast_tac eq_cs 1); 

760  455 
qed "converse_Un"; 
0  456 

457 
goal ZF.thy "converse(A Int B) = converse(A) Int converse(B)"; 

458 
by (fast_tac eq_cs 1); 

760  459 
qed "converse_Int"; 
0  460 

461 
goal ZF.thy "converse(A)  converse(B) = converse(A  B)"; 

462 
by (fast_tac eq_cs 1); 

1056  463 
qed "converse_Diff"; 
0  464 

787  465 
(*Does the analogue hold for INT?*) 
466 
goal ZF.thy "converse(UN x:A. B(x)) = (UN x:A. converse(B(x)))"; 

467 
by (fast_tac eq_cs 1); 

468 
qed "converse_UN"; 

469 

198  470 
(** Pow **) 
471 

472 
goal ZF.thy "Pow(A) Un Pow(B) <= Pow(A Un B)"; 

473 
by (fast_tac upair_cs 1); 

760  474 
qed "Un_Pow_subset"; 
198  475 

476 
goal ZF.thy "(UN x:A. Pow(B(x))) <= Pow(UN x:A. B(x))"; 

477 
by (fast_tac upair_cs 1); 

760  478 
qed "UN_Pow_subset"; 
198  479 

480 
goal ZF.thy "A <= Pow(Union(A))"; 

481 
by (fast_tac upair_cs 1); 

760  482 
qed "subset_Pow_Union"; 
198  483 

484 
goal ZF.thy "Union(Pow(A)) = A"; 

485 
by (fast_tac eq_cs 1); 

760  486 
qed "Union_Pow_eq"; 
198  487 

488 
goal ZF.thy "Pow(A) Int Pow(B) = Pow(A Int B)"; 

489 
by (fast_tac eq_cs 1); 

760  490 
qed "Int_Pow_eq"; 
198  491 

492 
goal ZF.thy "!!x A. x:A ==> (INT x:A. Pow(B(x))) = Pow(INT x:A. B(x))"; 

493 
by (fast_tac eq_cs 1); 

760  494 
qed "INT_Pow_subset"; 
435  495 

839  496 
(** RepFun **) 
497 

498 
goal ZF.thy "{f(x).x:A}=0 <> A=0"; 

499 
by (fast_tac (eq_cs addSEs [equalityE]) 1); 

500 
qed "RepFun_eq_0_iff"; 

501 

502 
goal ZF.thy "{f(x).x:0} = 0"; 

503 
by (fast_tac eq_cs 1); 

504 
qed "RepFun_0"; 