author  paulson 
Fri, 16 Feb 1996 18:00:47 +0100  
changeset 1512  ce37c64244c0 
parent 1461  6bcb44e4d6e5 
child 1568  630d881b51bd 
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 

193 
(* A good challenge: Inter is illbehaved 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 
(*Firstorder version of the above, for rewriting*) 
294 
goal ZF.thy "I * (A Un B) = I*A Un I*B"; 

1461  295 
by (rtac 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 
(*Firstorder version of the above, for rewriting*) 
308 
goal ZF.thy "I * (A Int B) = I*A Int I*B"; 

1461  309 
by (rtac SUM_Int_distrib2 1); 
760  310 
qed "prod_Int_distrib2"; 
685  311 

192  312 
(*Cf Aczel, NonWellFounded 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"; 