author  lcp 
Mon, 31 Oct 1994 16:39:20 +0100  
changeset 664  ba39b4984f5a 
parent 516  1957113f0d7d 
child 688  4dddc8d0c384 
permissions  rwrr 
0  1 
(* Title: ZF/zf.ML 
2 
ID: $Id$ 

3 
Author: Lawrence C Paulson and Martin D Coen, CU Computer Laboratory 

435  4 
Copyright 1994 University of Cambridge 
0  5 

6 
Basic introduction and elimination rules for ZermeloFraenkel Set Theory 

7 
*) 

8 

9 
open ZF; 

10 

11 
signature ZF_LEMMAS = 

12 
sig 

516  13 
val ballE : thm 
14 
val ballI : thm 

15 
val ball_cong : thm 

16 
val ball_simp : thm 

17 
val ball_tac : int > tactic 

18 
val bexCI : thm 

19 
val bexE : thm 

20 
val bexI : thm 

21 
val bex_cong : thm 

22 
val bspec : thm 

23 
val CollectD1 : thm 

24 
val CollectD2 : thm 

25 
val CollectE : thm 

26 
val CollectI : thm 

435  27 
val Collect_cong : thm 
516  28 
val emptyE : thm 
435  29 
val empty_subsetI : thm 
30 
val equalityCE : thm 

31 
val equalityD1 : thm 

32 
val equalityD2 : thm 

516  33 
val equalityE : thm 
34 
val equalityI : thm 

435  35 
val equality_iffI : thm 
516  36 
val equals0D : thm 
37 
val equals0I : thm 

38 
val InterD : thm 

39 
val InterE : thm 

40 
val InterI : thm 

41 
val Inter_iff : thm 

42 
val INT_E : thm 

43 
val INT_I : thm 

44 
val INT_cong : thm 

45 
val lemmas_cs : claset 

46 
val PowD : thm 

47 
val PowI : thm 

48 
val RepFunE : thm 

49 
val RepFunI : thm 

435  50 
val RepFun_eqI : thm 
51 
val RepFun_cong : thm 

485  52 
val RepFun_iff : thm 
516  53 
val ReplaceE : thm 
54 
val ReplaceE2 : thm 

55 
val ReplaceI : thm 

435  56 
val Replace_iff : thm 
57 
val Replace_cong : thm 

516  58 
val rev_ballE : thm 
59 
val rev_bspec : thm 

435  60 
val rev_subsetD : thm 
61 
val separation : thm 

62 
val setup_induction : thm 

63 
val set_mp_tac : int > tactic 

516  64 
val subsetCE : thm 
65 
val subsetD : thm 

66 
val subsetI : thm 

435  67 
val subset_iff : thm 
68 
val subset_refl : thm 

69 
val subset_trans : thm 

516  70 
val UnionE : thm 
71 
val UnionI : thm 

72 
val Union_in_Pow : thm 

73 
val UN_E : thm 

74 
val UN_I : thm 

75 
val UN_cong : thm 

0  76 
end; 
77 

78 

79 
structure ZF_Lemmas : ZF_LEMMAS = 

80 
struct 

81 

82 
(*** Bounded universal quantifier ***) 

83 

84 
val ballI = prove_goalw ZF.thy [Ball_def] 

85 
"[ !!x. x:A ==> P(x) ] ==> ALL x:A. P(x)" 

86 
(fn prems=> [ (REPEAT (ares_tac (prems @ [allI,impI]) 1)) ]); 

87 

88 
val bspec = prove_goalw ZF.thy [Ball_def] 

89 
"[ ALL x:A. P(x); x: A ] ==> P(x)" 

90 
(fn major::prems=> 

91 
[ (rtac (major RS spec RS mp) 1), 

92 
(resolve_tac prems 1) ]); 

93 

94 
val ballE = prove_goalw ZF.thy [Ball_def] 

37  95 
"[ ALL x:A. P(x); P(x) ==> Q; x~:A ==> Q ] ==> Q" 
0  96 
(fn major::prems=> 
97 
[ (rtac (major RS allE) 1), 

98 
(REPEAT (eresolve_tac (prems@[asm_rl,impCE]) 1)) ]); 

99 

100 
(*Used in the datatype package*) 

101 
val rev_bspec = prove_goal ZF.thy 

102 
"!!x A P. [ x: A; ALL x:A. P(x) ] ==> P(x)" 

103 
(fn _ => 

104 
[ REPEAT (ares_tac [bspec] 1) ]); 

105 

106 
(*Instantiates x first: better for automatic theorem proving?*) 

107 
val rev_ballE = prove_goal ZF.thy 

37  108 
"[ ALL x:A. P(x); x~:A ==> Q; P(x) ==> Q ] ==> Q" 
0  109 
(fn major::prems=> 
110 
[ (rtac (major RS ballE) 1), 

111 
(REPEAT (eresolve_tac prems 1)) ]); 

112 

113 
(*Takes assumptions ALL x:A.P(x) and a:A; creates assumption P(a)*) 

114 
val ball_tac = dtac bspec THEN' assume_tac; 

115 

116 
(*Trival rewrite rule; (ALL x:A.P)<>P holds only if A is nonempty!*) 

6
8ce8c4d13d4d
Installation of new simplifier for ZF. Deleted all congruence rules not
lcp
parents:
0
diff
changeset

117 
val ball_simp = prove_goal ZF.thy "(ALL x:A. True) <> True" 
8ce8c4d13d4d
Installation of new simplifier for ZF. Deleted all congruence rules not
lcp
parents:
0
diff
changeset

118 
(fn _=> [ (REPEAT (ares_tac [TrueI,ballI,iffI] 1)) ]); 
0  119 

120 
(*Congruence rule for rewriting*) 

121 
val ball_cong = prove_goalw ZF.thy [Ball_def] 

6
8ce8c4d13d4d
Installation of new simplifier for ZF. Deleted all congruence rules not
lcp
parents:
0
diff
changeset

122 
"[ A=A'; !!x. x:A' ==> P(x) <> P'(x) ] ==> Ball(A,P) <> Ball(A',P')" 
8ce8c4d13d4d
Installation of new simplifier for ZF. Deleted all congruence rules not
lcp
parents:
0
diff
changeset

123 
(fn prems=> [ (simp_tac (FOL_ss addsimps prems) 1) ]); 
0  124 

125 
(*** Bounded existential quantifier ***) 

126 

127 
val bexI = prove_goalw ZF.thy [Bex_def] 

128 
"[ P(x); x: A ] ==> EX x:A. P(x)" 

129 
(fn prems=> [ (REPEAT (ares_tac (prems @ [exI,conjI]) 1)) ]); 

130 

131 
(*Not of the general form for such rules; ~EX has become ALL~ *) 

132 
val bexCI = prove_goal ZF.thy 

133 
"[ ALL x:A. ~P(x) ==> P(a); a: A ] ==> EX x:A.P(x)" 

134 
(fn prems=> 

135 
[ (rtac classical 1), 

136 
(REPEAT (ares_tac (prems@[bexI,ballI,notI,notE]) 1)) ]); 

137 

138 
val bexE = prove_goalw ZF.thy [Bex_def] 

139 
"[ EX x:A. P(x); !!x. [ x:A; P(x) ] ==> Q \ 

140 
\ ] ==> Q" 

141 
(fn major::prems=> 

142 
[ (rtac (major RS exE) 1), 

143 
(REPEAT (eresolve_tac (prems @ [asm_rl,conjE]) 1)) ]); 

144 

145 
(*We do not even have (EX x:A. True) <> True unless A is nonempty!!*) 

146 

147 
val bex_cong = prove_goalw ZF.thy [Bex_def] 

148 
"[ A=A'; !!x. x:A' ==> P(x) <> P'(x) \ 

6
8ce8c4d13d4d
Installation of new simplifier for ZF. Deleted all congruence rules not
lcp
parents:
0
diff
changeset

149 
\ ] ==> Bex(A,P) <> Bex(A',P')" 
8ce8c4d13d4d
Installation of new simplifier for ZF. Deleted all congruence rules not
lcp
parents:
0
diff
changeset

150 
(fn prems=> [ (simp_tac (FOL_ss addsimps prems addcongs [conj_cong]) 1) ]); 
0  151 

152 
(*** Rules for subsets ***) 

153 

154 
val subsetI = prove_goalw ZF.thy [subset_def] 

155 
"(!!x.x:A ==> x:B) ==> A <= B" 

156 
(fn prems=> [ (REPEAT (ares_tac (prems @ [ballI]) 1)) ]); 

157 

158 
(*Rule in Modus Ponens style [was called subsetE] *) 

159 
val subsetD = prove_goalw ZF.thy [subset_def] "[ A <= B; c:A ] ==> c:B" 

160 
(fn major::prems=> 

161 
[ (rtac (major RS bspec) 1), 

162 
(resolve_tac prems 1) ]); 

163 

164 
(*Classical elimination rule*) 

165 
val subsetCE = prove_goalw ZF.thy [subset_def] 

37  166 
"[ A <= B; c~:A ==> P; c:B ==> P ] ==> P" 
0  167 
(fn major::prems=> 
168 
[ (rtac (major RS ballE) 1), 

169 
(REPEAT (eresolve_tac prems 1)) ]); 

170 

171 
(*Takes assumptions A<=B; c:A and creates the assumption c:B *) 

172 
val set_mp_tac = dtac subsetD THEN' assume_tac; 

173 

174 
(*Sometimes useful with premises in this order*) 

175 
val rev_subsetD = prove_goal ZF.thy "!!A B c. [ c:A; A<=B ] ==> c:B" 

176 
(fn _=> [REPEAT (ares_tac [subsetD] 1)]); 

177 

178 
val subset_refl = prove_goal ZF.thy "A <= A" 

179 
(fn _=> [ (rtac subsetI 1), atac 1 ]); 

180 

181 
val subset_trans = prove_goal ZF.thy "[ A<=B; B<=C ] ==> A<=C" 

182 
(fn prems=> [ (REPEAT (ares_tac ([subsetI]@(prems RL [subsetD])) 1)) ]); 

183 

435  184 
(*Useful for proving A<=B by rewriting in some cases*) 
185 
val subset_iff = prove_goalw ZF.thy [subset_def,Ball_def] 

186 
"A<=B <> (ALL x. x:A > x:B)" 

187 
(fn _=> [ (rtac iff_refl 1) ]); 

188 

0  189 

190 
(*** Rules for equality ***) 

191 

192 
(*Antisymmetry of the subset relation*) 

193 
val equalityI = prove_goal ZF.thy "[ A <= B; B <= A ] ==> A = B" 

194 
(fn prems=> [ (REPEAT (resolve_tac (prems@[conjI, extension RS iffD2]) 1)) ]); 

195 

196 
val equality_iffI = prove_goal ZF.thy "(!!x. x:A <> x:B) ==> A = B" 

197 
(fn [prem] => 

198 
[ (rtac equalityI 1), 

199 
(REPEAT (ares_tac [subsetI, prem RS iffD1, prem RS iffD2] 1)) ]); 

200 

201 
val equalityD1 = prove_goal ZF.thy "A = B ==> A<=B" 

202 
(fn prems=> 

203 
[ (rtac (extension RS iffD1 RS conjunct1) 1), 

204 
(resolve_tac prems 1) ]); 

205 

206 
val equalityD2 = prove_goal ZF.thy "A = B ==> B<=A" 

207 
(fn prems=> 

208 
[ (rtac (extension RS iffD1 RS conjunct2) 1), 

209 
(resolve_tac prems 1) ]); 

210 

211 
val equalityE = prove_goal ZF.thy 

212 
"[ A = B; [ A<=B; B<=A ] ==> P ] ==> P" 

213 
(fn prems=> 

214 
[ (DEPTH_SOLVE (resolve_tac (prems@[equalityD1,equalityD2]) 1)) ]); 

215 

216 
val equalityCE = prove_goal ZF.thy 

37  217 
"[ A = B; [ c:A; c:B ] ==> P; [ c~:A; c~:B ] ==> P ] ==> P" 
0  218 
(fn major::prems=> 
219 
[ (rtac (major RS equalityE) 1), 

220 
(REPEAT (contr_tac 1 ORELSE eresolve_tac ([asm_rl,subsetCE]@prems) 1)) ]); 

221 

222 
(*Lemma for creating induction formulae  for "pattern matching" on p 

223 
To make the induction hypotheses usable, apply "spec" or "bspec" to 

224 
put universal quantifiers over the free variables in p. 

225 
Would it be better to do subgoal_tac "ALL z. p = f(z) > R(z)" ??*) 

226 
val setup_induction = prove_goal ZF.thy 

227 
"[ p: A; !!z. z: A ==> p=z > R ] ==> R" 

228 
(fn prems=> 

229 
[ (rtac mp 1), 

230 
(REPEAT (resolve_tac (refl::prems) 1)) ]); 

231 

232 

233 
(*** Rules for Replace  the derived form of replacement ***) 

234 

235 
val Replace_iff = prove_goalw ZF.thy [Replace_def] 

236 
"b : {y. x:A, P(x,y)} <> (EX x:A. P(x,b) & (ALL y. P(x,y) > y=b))" 

237 
(fn _=> 

238 
[ (rtac (replacement RS iff_trans) 1), 

239 
(REPEAT (ares_tac [refl,bex_cong,iffI,ballI,allI,conjI,impI,ex1I] 1 

240 
ORELSE eresolve_tac [conjE, spec RS mp, ex1_functional] 1)) ]); 

241 

242 
(*Introduction; there must be a unique y such that P(x,y), namely y=b. *) 

243 
val ReplaceI = prove_goal ZF.thy 

485  244 
"[ P(x,b); x: A; !!y. P(x,y) ==> y=b ] ==> \ 
0  245 
\ b : {y. x:A, P(x,y)}" 
246 
(fn prems=> 

247 
[ (rtac (Replace_iff RS iffD2) 1), 

248 
(REPEAT (ares_tac (prems@[bexI,conjI,allI,impI]) 1)) ]); 

249 

250 
(*Elimination; may asssume there is a unique y such that P(x,y), namely y=b. *) 

251 
val ReplaceE = prove_goal ZF.thy 

252 
"[ b : {y. x:A, P(x,y)}; \ 

253 
\ !!x. [ x: A; P(x,b); ALL y. P(x,y)>y=b ] ==> R \ 

254 
\ ] ==> R" 

255 
(fn prems=> 

256 
[ (rtac (Replace_iff RS iffD1 RS bexE) 1), 

257 
(etac conjE 2), 

258 
(REPEAT (ares_tac prems 1)) ]); 

259 

485  260 
(*As above but without the (generally useless) 3rd assumption*) 
261 
val ReplaceE2 = prove_goal ZF.thy 

262 
"[ b : {y. x:A, P(x,y)}; \ 

263 
\ !!x. [ x: A; P(x,b) ] ==> R \ 

264 
\ ] ==> R" 

265 
(fn major::prems=> 

266 
[ (rtac (major RS ReplaceE) 1), 

267 
(REPEAT (ares_tac prems 1)) ]); 

268 

0  269 
val Replace_cong = prove_goal ZF.thy 
270 
"[ A=B; !!x y. x:B ==> P(x,y) <> Q(x,y) ] ==> \ 

6
8ce8c4d13d4d
Installation of new simplifier for ZF. Deleted all congruence rules not
lcp
parents:
0
diff
changeset

271 
\ Replace(A,P) = Replace(B,Q)" 
0  272 
(fn prems=> 
273 
let val substprems = prems RL [subst, ssubst] 

274 
and iffprems = prems RL [iffD1,iffD2] 

275 
in [ (rtac equalityI 1), 

276 
(REPEAT (eresolve_tac (substprems@[asm_rl, ReplaceE, spec RS mp]) 1 

277 
ORELSE resolve_tac [subsetI, ReplaceI] 1 

278 
ORELSE (resolve_tac iffprems 1 THEN assume_tac 2))) ] 

279 
end); 

280 

281 
(*** Rules for RepFun ***) 

282 

283 
val RepFunI = prove_goalw ZF.thy [RepFun_def] 

284 
"!!a A. a : A ==> f(a) : {f(x). x:A}" 

285 
(fn _ => [ (REPEAT (ares_tac [ReplaceI,refl] 1)) ]); 

286 

120  287 
(*Useful for coinduction proofs*) 
0  288 
val RepFun_eqI = prove_goal ZF.thy 
289 
"!!b a f. [ b=f(a); a : A ] ==> b : {f(x). x:A}" 

290 
(fn _ => [ etac ssubst 1, etac RepFunI 1 ]); 

291 

292 
val RepFunE = prove_goalw ZF.thy [RepFun_def] 

293 
"[ b : {f(x). x:A}; \ 

294 
\ !!x.[ x:A; b=f(x) ] ==> P ] ==> \ 

295 
\ P" 

296 
(fn major::prems=> 

297 
[ (rtac (major RS ReplaceE) 1), 

298 
(REPEAT (ares_tac prems 1)) ]); 

299 

300 
val RepFun_cong = prove_goalw ZF.thy [RepFun_def] 

6
8ce8c4d13d4d
Installation of new simplifier for ZF. Deleted all congruence rules not
lcp
parents:
0
diff
changeset

301 
"[ A=B; !!x. x:B ==> f(x)=g(x) ] ==> RepFun(A,f) = RepFun(B,g)" 
8ce8c4d13d4d
Installation of new simplifier for ZF. Deleted all congruence rules not
lcp
parents:
0
diff
changeset

302 
(fn prems=> [ (simp_tac (FOL_ss addcongs [Replace_cong] addsimps prems) 1) ]); 
0  303 

485  304 
val RepFun_iff = prove_goalw ZF.thy [Bex_def] 
305 
"b : {f(x). x:A} <> (EX x:A. b=f(x))" 

306 
(fn _ => [ (fast_tac (FOL_cs addIs [RepFunI] addSEs [RepFunE]) 1) ]); 

307 

0  308 

309 
(*** Rules for Collect  forming a subset by separation ***) 

310 

311 
(*Separation is derivable from Replacement*) 

312 
val separation = prove_goalw ZF.thy [Collect_def] 

313 
"a : {x:A. P(x)} <> a:A & P(a)" 

314 
(fn _=> [ (fast_tac (FOL_cs addIs [bexI,ReplaceI] 

315 
addSEs [bexE,ReplaceE]) 1) ]); 

316 

317 
val CollectI = prove_goal ZF.thy 

318 
"[ a:A; P(a) ] ==> a : {x:A. P(x)}" 

319 
(fn prems=> 

320 
[ (rtac (separation RS iffD2) 1), 

321 
(REPEAT (resolve_tac (prems@[conjI]) 1)) ]); 

322 

323 
val CollectE = prove_goal ZF.thy 

324 
"[ a : {x:A. P(x)}; [ a:A; P(a) ] ==> R ] ==> R" 

325 
(fn prems=> 

326 
[ (rtac (separation RS iffD1 RS conjE) 1), 

327 
(REPEAT (ares_tac prems 1)) ]); 

328 

329 
val CollectD1 = prove_goal ZF.thy "a : {x:A. P(x)} ==> a:A" 

330 
(fn [major]=> 

331 
[ (rtac (major RS CollectE) 1), 

332 
(assume_tac 1) ]); 

333 

334 
val CollectD2 = prove_goal ZF.thy "a : {x:A. P(x)} ==> P(a)" 

335 
(fn [major]=> 

336 
[ (rtac (major RS CollectE) 1), 

337 
(assume_tac 1) ]); 

338 

339 
val Collect_cong = prove_goalw ZF.thy [Collect_def] 

6
8ce8c4d13d4d
Installation of new simplifier for ZF. Deleted all congruence rules not
lcp
parents:
0
diff
changeset

340 
"[ A=B; !!x. x:B ==> P(x) <> Q(x) ] ==> Collect(A,P) = Collect(B,Q)" 
8ce8c4d13d4d
Installation of new simplifier for ZF. Deleted all congruence rules not
lcp
parents:
0
diff
changeset

341 
(fn prems=> [ (simp_tac (FOL_ss addcongs [Replace_cong] addsimps prems) 1) ]); 
0  342 

343 
(*** Rules for Unions ***) 

344 

345 
(*The order of the premises presupposes that C is rigid; A may be flexible*) 

346 
val UnionI = prove_goal ZF.thy "[ B: C; A: B ] ==> A: Union(C)" 

347 
(fn prems=> 

485  348 
[ (resolve_tac [Union_iff RS iffD2] 1), 
0  349 
(REPEAT (resolve_tac (prems @ [bexI]) 1)) ]); 
350 

351 
val UnionE = prove_goal ZF.thy 

352 
"[ A : Union(C); !!B.[ A: B; B: C ] ==> R ] ==> R" 

353 
(fn prems=> 

485  354 
[ (resolve_tac [Union_iff RS iffD1 RS bexE] 1), 
0  355 
(REPEAT (ares_tac prems 1)) ]); 
356 

357 
(*** Rules for Inter ***) 

358 

359 
(*Not obviously useful towards proving InterI, InterD, InterE*) 

360 
val Inter_iff = prove_goalw ZF.thy [Inter_def,Ball_def] 

361 
"A : Inter(C) <> (ALL x:C. A: x) & (EX x. x:C)" 

362 
(fn _=> [ (rtac (separation RS iff_trans) 1), 

363 
(fast_tac (FOL_cs addIs [UnionI] addSEs [UnionE]) 1) ]); 

364 

365 
(* Intersection is wellbehaved only if the family is nonempty! *) 

366 
val InterI = prove_goalw ZF.thy [Inter_def] 

367 
"[ !!x. x: C ==> A: x; c:C ] ==> A : Inter(C)" 

368 
(fn prems=> 

369 
[ (DEPTH_SOLVE (ares_tac ([CollectI,UnionI,ballI] @ prems) 1)) ]); 

370 

371 
(*A "destruct" rule  every B in C contains A as an element, but 

372 
A:B can hold when B:C does not! This rule is analogous to "spec". *) 

373 
val InterD = prove_goalw ZF.thy [Inter_def] 

374 
"[ A : Inter(C); B : C ] ==> A : B" 

375 
(fn [major,minor]=> 

376 
[ (rtac (major RS CollectD2 RS bspec) 1), 

377 
(rtac minor 1) ]); 

378 

379 
(*"Classical" elimination rule  does not require exhibiting B:C *) 

380 
val InterE = prove_goalw ZF.thy [Inter_def] 

37  381 
"[ A : Inter(C); A:B ==> R; B~:C ==> R ] ==> R" 
0  382 
(fn major::prems=> 
383 
[ (rtac (major RS CollectD2 RS ballE) 1), 

384 
(REPEAT (eresolve_tac prems 1)) ]); 

385 

386 
(*** Rules for Unions of families ***) 

387 
(* UN x:A. B(x) abbreviates Union({B(x). x:A}) *) 

388 

485  389 
val UN_iff = prove_goalw ZF.thy [Bex_def] 
390 
"b : (UN x:A. B(x)) <> (EX x:A. b : B(x))" 

391 
(fn _=> [ (fast_tac (FOL_cs addIs [UnionI, RepFunI] 

392 
addSEs [UnionE, RepFunE]) 1) ]); 

393 

0  394 
(*The order of the premises presupposes that A is rigid; b may be flexible*) 
395 
val UN_I = prove_goal ZF.thy "[ a: A; b: B(a) ] ==> b: (UN x:A. B(x))" 

396 
(fn prems=> 

397 
[ (REPEAT (resolve_tac (prems@[UnionI,RepFunI]) 1)) ]); 

398 

399 
val UN_E = prove_goal ZF.thy 

400 
"[ b : (UN x:A. B(x)); !!x.[ x: A; b: B(x) ] ==> R ] ==> R" 

401 
(fn major::prems=> 

402 
[ (rtac (major RS UnionE) 1), 

403 
(REPEAT (eresolve_tac (prems@[asm_rl, RepFunE, subst]) 1)) ]); 

404 

435  405 
val UN_cong = prove_goal ZF.thy 
406 
"[ A=B; !!x. x:B ==> C(x)=D(x) ] ==> (UN x:A.C(x)) = (UN x:B.D(x))" 

407 
(fn prems=> [ (simp_tac (FOL_ss addcongs [RepFun_cong] addsimps prems) 1) ]); 

408 

0  409 

410 
(*** Rules for Intersections of families ***) 

411 
(* INT x:A. B(x) abbreviates Inter({B(x). x:A}) *) 

412 

485  413 
val INT_iff = prove_goal ZF.thy 
414 
"b : (INT x:A. B(x)) <> (ALL x:A. b : B(x)) & (EX x. x:A)" 

415 
(fn _=> [ (simp_tac (FOL_ss addsimps [Inter_def, Ball_def, Bex_def, 

416 
separation, Union_iff, RepFun_iff]) 1), 

417 
(fast_tac FOL_cs 1) ]); 

418 

0  419 
val INT_I = prove_goal ZF.thy 
420 
"[ !!x. x: A ==> b: B(x); a: A ] ==> b: (INT x:A. B(x))" 

421 
(fn prems=> 

422 
[ (REPEAT (ares_tac (prems@[InterI,RepFunI]) 1 

423 
ORELSE eresolve_tac [RepFunE,ssubst] 1)) ]); 

424 

425 
val INT_E = prove_goal ZF.thy 

426 
"[ b : (INT x:A. B(x)); a: A ] ==> b : B(a)" 

427 
(fn [major,minor]=> 

428 
[ (rtac (major RS InterD) 1), 

429 
(rtac (minor RS RepFunI) 1) ]); 

430 

435  431 
val INT_cong = prove_goal ZF.thy 
432 
"[ A=B; !!x. x:B ==> C(x)=D(x) ] ==> (INT x:A.C(x)) = (INT x:B.D(x))" 

433 
(fn prems=> [ (simp_tac (FOL_ss addcongs [RepFun_cong] addsimps prems) 1) ]); 

434 

0  435 

436 
(*** Rules for Powersets ***) 

437 

438 
val PowI = prove_goal ZF.thy "A <= B ==> A : Pow(B)" 

485  439 
(fn [prem]=> [ (rtac (prem RS (Pow_iff RS iffD2)) 1) ]); 
0  440 

441 
val PowD = prove_goal ZF.thy "A : Pow(B) ==> A<=B" 

485  442 
(fn [major]=> [ (rtac (major RS (Pow_iff RS iffD1)) 1) ]); 
0  443 

444 

445 
(*** Rules for the empty set ***) 

446 

447 
(*The set {x:0.False} is empty; by foundation it equals 0 

448 
See Suppes, page 21.*) 

449 
val emptyE = prove_goal ZF.thy "a:0 ==> P" 

450 
(fn [major]=> 

451 
[ (rtac (foundation RS disjE) 1), 

452 
(etac (equalityD2 RS subsetD RS CollectD2 RS FalseE) 1), 

453 
(rtac major 1), 

454 
(etac bexE 1), 

455 
(etac (CollectD2 RS FalseE) 1) ]); 

456 

457 
val empty_subsetI = prove_goal ZF.thy "0 <= A" 

458 
(fn _ => [ (REPEAT (ares_tac [equalityI,subsetI,emptyE] 1)) ]); 

459 

460 
val equals0I = prove_goal ZF.thy "[ !!y. y:A ==> False ] ==> A=0" 

461 
(fn prems=> 

462 
[ (REPEAT (ares_tac (prems@[empty_subsetI,subsetI,equalityI]) 1 

463 
ORELSE eresolve_tac (prems RL [FalseE]) 1)) ]); 

464 

465 
val equals0D = prove_goal ZF.thy "[ A=0; a:A ] ==> P" 

466 
(fn [major,minor]=> 

467 
[ (rtac (minor RS (major RS equalityD1 RS subsetD RS emptyE)) 1) ]); 

468 

469 
val lemmas_cs = FOL_cs 

470 
addSIs [ballI, InterI, CollectI, PowI, subsetI] 

471 
addIs [bexI, UnionI, ReplaceI, RepFunI] 

485  472 
addSEs [bexE, make_elim PowD, UnionE, ReplaceE2, RepFunE, 
0  473 
CollectE, emptyE] 
474 
addEs [rev_ballE, InterD, make_elim InterD, subsetD, subsetCE]; 

475 

516  476 
(*Lemma for the inductive definition in Zorn.thy*) 
477 
val Union_in_Pow = prove_goal ZF.thy 

478 
"!!Y. Y : Pow(Pow(A)) ==> Union(Y) : Pow(A)" 

479 
(fn _ => [fast_tac lemmas_cs 1]); 

480 

0  481 
end; 
482 

483 
open ZF_Lemmas; 