author  lcp 
Thu, 03 Nov 1994 11:58:16 +0100  
changeset 685  0727f0c0c4f0 
parent 536  5fbfa997f1b0 
child 760  f0200e91b272 
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); 

15 
val cons_eq = result(); 

16 

0  17 
goal ZF.thy "cons(a, cons(b, C)) = cons(b, cons(a, C))"; 
18 
by (fast_tac eq_cs 1); 

19 
val cons_commute = result(); 

20 

21 
goal ZF.thy "!!B. a: B ==> cons(a,B) = B"; 

22 
by (fast_tac eq_cs 1); 

23 
val cons_absorb = result(); 

24 

25 
goal ZF.thy "!!B. a: B ==> cons(a, B{a}) = B"; 

26 
by (fast_tac eq_cs 1); 

27 
val cons_Diff = result(); 

28 

29 
goal ZF.thy "!!C. [ a: C; ALL y:C. y=b ] ==> C = {b}"; 

30 
by (fast_tac eq_cs 1); 

31 
val equal_singleton_lemma = result(); 

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); 

39 
val Int_0 = result(); 

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); 

44 
val Int_cons = result(); 

45 

46 
goal ZF.thy "A Int A = A"; 

47 
by (fast_tac eq_cs 1); 

48 
val Int_absorb = result(); 

49 

50 
goal ZF.thy "A Int B = B Int A"; 

51 
by (fast_tac eq_cs 1); 

52 
val Int_commute = result(); 

53 

54 
goal ZF.thy "(A Int B) Int C = A Int (B Int C)"; 

55 
by (fast_tac eq_cs 1); 

56 
val Int_assoc = result(); 

57 

58 
goal ZF.thy "(A Un B) Int C = (A Int C) Un (B Int C)"; 

59 
by (fast_tac eq_cs 1); 

60 
val Int_Un_distrib = result(); 

61 

62 
goal ZF.thy "A<=B <> A Int B = A"; 

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

64 
val subset_Int_iff = result(); 

65 

435  66 
goal ZF.thy "A<=B <> B Int A = A"; 
67 
by (fast_tac (eq_cs addSEs [equalityE]) 1); 

68 
val subset_Int_iff2 = result(); 

69 

0  70 
(** Binary Union **) 
71 

72 
goal ZF.thy "0 Un A = A"; 

73 
by (fast_tac eq_cs 1); 

74 
val Un_0 = result(); 

75 

76 
goal ZF.thy "cons(a,B) Un C = cons(a, B Un C)"; 

77 
by (fast_tac eq_cs 1); 

78 
val Un_cons = result(); 

79 

80 
goal ZF.thy "A Un A = A"; 

81 
by (fast_tac eq_cs 1); 

82 
val Un_absorb = result(); 

83 

84 
goal ZF.thy "A Un B = B Un A"; 

85 
by (fast_tac eq_cs 1); 

86 
val Un_commute = result(); 

87 

88 
goal ZF.thy "(A Un B) Un C = A Un (B Un C)"; 

89 
by (fast_tac eq_cs 1); 

90 
val Un_assoc = result(); 

91 

92 
goal ZF.thy "(A Int B) Un C = (A Un C) Int (B Un C)"; 

93 
by (fast_tac eq_cs 1); 

94 
val Un_Int_distrib = result(); 

95 

96 
goal ZF.thy "A<=B <> A Un B = B"; 

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

98 
val subset_Un_iff = result(); 

99 

435  100 
goal ZF.thy "A<=B <> B Un A = B"; 
101 
by (fast_tac (eq_cs addSEs [equalityE]) 1); 

102 
val subset_Un_iff2 = result(); 

103 

0  104 
(** Simple properties of Diff  set difference **) 
105 

106 
goal ZF.thy "AA = 0"; 

107 
by (fast_tac eq_cs 1); 

108 
val Diff_cancel = result(); 

109 

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

111 
by (fast_tac eq_cs 1); 

112 
val empty_Diff = result(); 

113 

114 
goal ZF.thy "A0 = A"; 

115 
by (fast_tac eq_cs 1); 

116 
val Diff_0 = result(); 

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); 

121 
val Diff_cons = result(); 

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); 

126 
val Diff_cons2 = result(); 

127 

128 
goal ZF.thy "A Int (BA) = 0"; 

129 
by (fast_tac eq_cs 1); 

130 
val Diff_disjoint = result(); 

131 

132 
goal ZF.thy "!!A B. A<=B ==> A Un (BA) = B"; 

133 
by (fast_tac eq_cs 1); 

134 
val Diff_partition = result(); 

135 

268  136 
goal ZF.thy "!!A B. [ A<=B; B<=C ] ==> B(CA) = A"; 
0  137 
by (fast_tac eq_cs 1); 
138 
val double_complement = result(); 

139 

268  140 
goal ZF.thy "(A Un B)  (BA) = A"; 
141 
by (fast_tac eq_cs 1); 

142 
val double_complement_Un = result(); 

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); 

147 
val Un_Int_crazy = result(); 

148 

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

150 
by (fast_tac eq_cs 1); 

151 
val Diff_Un = result(); 

152 

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

154 
by (fast_tac eq_cs 1); 

155 
val Diff_Int = result(); 

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); 

160 
val Un_Int_assoc_iff = result(); 

161 

162 

163 
(** Big Union and Intersection **) 

164 

165 
goal ZF.thy "Union(0) = 0"; 

166 
by (fast_tac eq_cs 1); 

167 
val Union_0 = result(); 

168 

169 
goal ZF.thy "Union(cons(a,B)) = a Un Union(B)"; 

170 
by (fast_tac eq_cs 1); 

171 
val Union_cons = result(); 

172 

173 
goal ZF.thy "Union(A Un B) = Union(A) Un Union(B)"; 

174 
by (fast_tac eq_cs 1); 

175 
val Union_Un_distrib = result(); 

176 

435  177 
goal ZF.thy "Union(A Int B) <= Union(A) Int Union(B)"; 
178 
by (fast_tac ZF_cs 1); 

179 
val Union_Int_subset = result(); 

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); 

183 
val Union_disjoint = result(); 

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); 

188 
val Inter_Un_distrib = result(); 

189 

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

191 
by (fast_tac eq_cs 1); 

192 
val Union_singleton = result(); 

193 

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

195 
by (fast_tac eq_cs 1); 

196 
val Inter_singleton = result(); 

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); 

202 
val Union_eq_UN = result(); 

203 

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

205 
by (fast_tac eq_cs 1); 

206 
val Inter_eq_INT = result(); 

207 

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

210 
val UN_0 = result(); 

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); 

215 
val Int_UN_distrib = result(); 

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); 

219 
val Un_INT_distrib = result(); 

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); 

224 
val Int_UN_distrib2 = result(); 

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); 

230 
val Un_INT_distrib2 = result(); 

231 

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

234 
val UN_constant = result(); 

0  235 

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

238 
val INT_constant = result(); 

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); 
245 
val UN_Un_distrib = result(); 

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); 
251 
val INT_Int_distrib = result(); 

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); 

257 
val Diff_UN = result(); 

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); 

261 
val Diff_INT = result(); 

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); 

267 
val Sigma_cons = result(); 

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); 

271 
val SUM_UN_distrib1 = result(); 

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); 
275 
val SUM_UN_distrib2 = result(); 

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); 
279 
val SUM_Un_distrib1 = result(); 

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); 
283 
val SUM_Un_distrib2 = result(); 

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); 

288 
val prod_Un_distrib2 = result(); 

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); 
292 
val SUM_Int_distrib1 = result(); 

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); 
297 
val SUM_Int_distrib2 = result(); 

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); 

302 
val prod_Int_distrib2 = result(); 

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); 

307 
val SUM_eq_UN = result(); 

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 

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

311 
val domain_of_prod = prove_goal ZF.thy "!!A B. b:B ==> domain(A*B) = A" 
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 

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

314 
val domain_0 = prove_goal ZF.thy "domain(0) = 0" 
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 

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

317 
val domain_cons = prove_goal ZF.thy 
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); 

323 
val domain_Un_eq = result(); 

324 

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

326 
by (fast_tac eq_cs 1); 

327 
val domain_Int_subset = result(); 

328 

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

330 
by (fast_tac eq_cs 1); 

331 
val domain_diff_subset = result(); 

332 

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

335 
val domain_converse = result(); 

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 

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

341 
val range_of_prod = prove_goal ZF.thy 
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 

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

345 
val range_0 = prove_goal ZF.thy "range(0) = 0" 
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 

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

348 
val range_cons = prove_goal ZF.thy 
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); 

354 
val range_Un_eq = result(); 

355 

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

435  357 
by (fast_tac ZF_cs 1); 
0  358 
val range_Int_subset = result(); 
359 

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

361 
by (fast_tac eq_cs 1); 

362 
val range_diff_subset = result(); 

363 

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

366 
val range_converse = result(); 

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 

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

370 
val field_of_prod = prove_goal ZF.thy "field(A*A) = A" 
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 

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

373 
val field_0 = prove_goal ZF.thy "field(0) = 0" 
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 

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

376 
val field_cons = prove_goal ZF.thy 
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); 

382 
val field_Un_eq = result(); 

383 

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

385 
by (fast_tac eq_cs 1); 

386 
val field_Int_subset = result(); 

387 

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

389 
by (fast_tac eq_cs 1); 

390 
val field_diff_subset = result(); 

391 

392 

435  393 
(** Image **) 
394 

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

396 
by (fast_tac eq_cs 1); 

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

397 
val image_0 = result(); 
435  398 

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

400 
by (fast_tac eq_cs 1); 

401 
val image_Un = result(); 

402 

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

404 
by (fast_tac ZF_cs 1); 

405 
val image_Int_subset = result(); 

406 

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

408 
by (fast_tac ZF_cs 1); 

409 
val image_Int_square_subset = result(); 

410 

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

412 
by (fast_tac eq_cs 1); 

413 
val image_Int_square = result(); 

414 

415 

416 
(** Inverse Image **) 

417 

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

419 
by (fast_tac eq_cs 1); 

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

420 
val vimage_0 = result(); 
435  421 

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

423 
by (fast_tac eq_cs 1); 

424 
val vimage_Un = result(); 

425 

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

427 
by (fast_tac ZF_cs 1); 

428 
val vimage_Int_subset = result(); 

429 

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

431 
by (fast_tac ZF_cs 1); 

432 
val vimage_Int_square_subset = result(); 

433 

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

435 
by (fast_tac eq_cs 1); 

436 
val vimage_Int_square = result(); 

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); 

443 
val converse_Un = result(); 

444 

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

446 
by (fast_tac eq_cs 1); 

447 
val converse_Int = result(); 

448 

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

450 
by (fast_tac eq_cs 1); 

451 
val converse_diff = result(); 

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); 

457 
val Un_Pow_subset = result(); 

458 

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

460 
by (fast_tac upair_cs 1); 

461 
val UN_Pow_subset = result(); 

462 

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

464 
by (fast_tac upair_cs 1); 

465 
val subset_Pow_Union = result(); 

466 

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

468 
by (fast_tac eq_cs 1); 

469 
val Union_Pow_eq = result(); 

470 

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

472 
by (fast_tac eq_cs 1); 

473 
val Int_Pow_eq = result(); 

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); 

477 
val INT_Pow_subset = result(); 

435  478 