author  lcp 
Fri, 23 Dec 1994 16:51:10 +0100  
changeset 839  1aa6b351ca34 
parent 787  1affbb1c5f1f 
child 1035  279a4fd3c5ce 
permissions  rwrr 
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 "AA = 0"; 

107 
by (fast_tac eq_cs 1); 

760  108 
qed "Diff_cancel"; 
0  109 

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

111 
by (fast_tac eq_cs 1); 

760  112 
qed "empty_Diff"; 
0  113 

114 
goal ZF.thy "A0 = A"; 

115 
by (fast_tac eq_cs 1); 

760  116 
qed "Diff_0"; 
0  117 

787  118 
goal ZF.thy "AB=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 (BA) = 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 (BA) = 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(CA) = A"; 
0  141 
by (fast_tac eq_cs 1); 
760  142 
qed "double_complement"; 
0  143 

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

154 
by (fast_tac eq_cs 1); 

760  155 
qed "Diff_Un"; 
0  156 

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

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 illbehaved 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 
(*Firstorder 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 
(*Firstorder 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, NonWellFounded 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 

839  488 
(** RepFun **) 
489 

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

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

492 
qed "RepFun_eq_0_iff"; 

493 

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

495 
by (fast_tac eq_cs 1); 

496 
qed "RepFun_0"; 