author  clasohm 
Wed, 07 Dec 1994 13:12:04 +0100  
changeset 760  f0200e91b272 
parent 685  0727f0c0c4f0 
child 787  1affbb1c5f1f 
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 

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 (BA) = 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 (BA) = 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(CA) = A"; 
0  137 
by (fast_tac eq_cs 1); 
760  138 
qed "double_complement"; 
0  139 

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

150 
by (fast_tac eq_cs 1); 

760  151 
qed "Diff_Un"; 
0  152 

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

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