author  paulson 
Fri, 16 Feb 1996 18:00:47 +0100  
changeset 1512  ce37c64244c0 
parent 1461  6bcb44e4d6e5 
child 1889  661603db8ee2 
permissions  rwrr 
1461  1 
(* Title: ZF/ZF.ML 
0  2 
ID: $Id$ 
1461  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 

825
76d9575950f2
Added Krzysztof's theorems subst_elem, not_emptyI, not_emptyE
lcp
parents:
775
diff
changeset

12 
(*Useful examples: singletonI RS subst_elem, subst_elem RSN (2,IntI) *) 
76d9575950f2
Added Krzysztof's theorems subst_elem, not_emptyI, not_emptyE
lcp
parents:
775
diff
changeset

13 
goal ZF.thy "!!a b A. [ b:A; a=b ] ==> a:A"; 
76d9575950f2
Added Krzysztof's theorems subst_elem, not_emptyI, not_emptyE
lcp
parents:
775
diff
changeset

14 
by (etac ssubst 1); 
76d9575950f2
Added Krzysztof's theorems subst_elem, not_emptyI, not_emptyE
lcp
parents:
775
diff
changeset

15 
by (assume_tac 1); 
76d9575950f2
Added Krzysztof's theorems subst_elem, not_emptyI, not_emptyE
lcp
parents:
775
diff
changeset

16 
val subst_elem = result(); 
76d9575950f2
Added Krzysztof's theorems subst_elem, not_emptyI, not_emptyE
lcp
parents:
775
diff
changeset

17 

0  18 
(*** Bounded universal quantifier ***) 
19 

775  20 
qed_goalw "ballI" ZF.thy [Ball_def] 
0  21 
"[ !!x. x:A ==> P(x) ] ==> ALL x:A. P(x)" 
22 
(fn prems=> [ (REPEAT (ares_tac (prems @ [allI,impI]) 1)) ]); 

23 

775  24 
qed_goalw "bspec" ZF.thy [Ball_def] 
0  25 
"[ ALL x:A. P(x); x: A ] ==> P(x)" 
26 
(fn major::prems=> 

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

28 
(resolve_tac prems 1) ]); 

29 

775  30 
qed_goalw "ballE" ZF.thy [Ball_def] 
37  31 
"[ ALL x:A. P(x); P(x) ==> Q; x~:A ==> Q ] ==> Q" 
0  32 
(fn major::prems=> 
33 
[ (rtac (major RS allE) 1), 

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

35 

36 
(*Used in the datatype package*) 

775  37 
qed_goal "rev_bspec" ZF.thy 
0  38 
"!!x A P. [ x: A; ALL x:A. P(x) ] ==> P(x)" 
39 
(fn _ => 

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

41 

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

775  43 
qed_goal "rev_ballE" ZF.thy 
37  44 
"[ ALL x:A. P(x); x~:A ==> Q; P(x) ==> Q ] ==> Q" 
0  45 
(fn major::prems=> 
46 
[ (rtac (major RS ballE) 1), 

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

48 

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

50 
val ball_tac = dtac bspec THEN' assume_tac; 

51 

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

775  53 
qed_goal "ball_simp" ZF.thy "(ALL x:A. True) <> True" 
6
8ce8c4d13d4d
Installation of new simplifier for ZF. Deleted all congruence rules not
lcp
parents:
0
diff
changeset

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

56 
(*Congruence rule for rewriting*) 

775  57 
qed_goalw "ball_cong" ZF.thy [Ball_def] 
6
8ce8c4d13d4d
Installation of new simplifier for ZF. Deleted all congruence rules not
lcp
parents:
0
diff
changeset

58 
"[ 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

59 
(fn prems=> [ (simp_tac (FOL_ss addsimps prems) 1) ]); 
0  60 

61 
(*** Bounded existential quantifier ***) 

62 

775  63 
qed_goalw "bexI" ZF.thy [Bex_def] 
0  64 
"[ P(x); x: A ] ==> EX x:A. P(x)" 
65 
(fn prems=> [ (REPEAT (ares_tac (prems @ [exI,conjI]) 1)) ]); 

66 

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

775  68 
qed_goal "bexCI" ZF.thy 
0  69 
"[ ALL x:A. ~P(x) ==> P(a); a: A ] ==> EX x:A.P(x)" 
70 
(fn prems=> 

71 
[ (rtac classical 1), 

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

73 

775  74 
qed_goalw "bexE" ZF.thy [Bex_def] 
0  75 
"[ EX x:A. P(x); !!x. [ x:A; P(x) ] ==> Q \ 
76 
\ ] ==> Q" 

77 
(fn major::prems=> 

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

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

80 

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

82 

775  83 
qed_goalw "bex_cong" ZF.thy [Bex_def] 
0  84 
"[ 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

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

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

88 
(*** Rules for subsets ***) 

89 

775  90 
qed_goalw "subsetI" ZF.thy [subset_def] 
0  91 
"(!!x.x:A ==> x:B) ==> A <= B" 
92 
(fn prems=> [ (REPEAT (ares_tac (prems @ [ballI]) 1)) ]); 

93 

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

775  95 
qed_goalw "subsetD" ZF.thy [subset_def] "[ A <= B; c:A ] ==> c:B" 
0  96 
(fn major::prems=> 
97 
[ (rtac (major RS bspec) 1), 

98 
(resolve_tac prems 1) ]); 

99 

100 
(*Classical elimination rule*) 

775  101 
qed_goalw "subsetCE" ZF.thy [subset_def] 
37  102 
"[ A <= B; c~:A ==> P; c:B ==> P ] ==> P" 
0  103 
(fn major::prems=> 
104 
[ (rtac (major RS ballE) 1), 

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

106 

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

108 
val set_mp_tac = dtac subsetD THEN' assume_tac; 

109 

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

775  111 
qed_goal "rev_subsetD" ZF.thy "!!A B c. [ c:A; A<=B ] ==> c:B" 
0  112 
(fn _=> [REPEAT (ares_tac [subsetD] 1)]); 
113 

775  114 
qed_goal "subset_refl" ZF.thy "A <= A" 
0  115 
(fn _=> [ (rtac subsetI 1), atac 1 ]); 
116 

775  117 
qed_goal "subset_trans" ZF.thy "[ A<=B; B<=C ] ==> A<=C" 
0  118 
(fn prems=> [ (REPEAT (ares_tac ([subsetI]@(prems RL [subsetD])) 1)) ]); 
119 

435  120 
(*Useful for proving A<=B by rewriting in some cases*) 
775  121 
qed_goalw "subset_iff" ZF.thy [subset_def,Ball_def] 
435  122 
"A<=B <> (ALL x. x:A > x:B)" 
123 
(fn _=> [ (rtac iff_refl 1) ]); 

124 

0  125 

126 
(*** Rules for equality ***) 

127 

128 
(*Antisymmetry of the subset relation*) 

775  129 
qed_goal "equalityI" ZF.thy "[ A <= B; B <= A ] ==> A = B" 
0  130 
(fn prems=> [ (REPEAT (resolve_tac (prems@[conjI, extension RS iffD2]) 1)) ]); 
131 

775  132 
qed_goal "equality_iffI" ZF.thy "(!!x. x:A <> x:B) ==> A = B" 
0  133 
(fn [prem] => 
134 
[ (rtac equalityI 1), 

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

136 

775  137 
qed_goal "equalityD1" ZF.thy "A = B ==> A<=B" 
0  138 
(fn prems=> 
139 
[ (rtac (extension RS iffD1 RS conjunct1) 1), 

140 
(resolve_tac prems 1) ]); 

141 

775  142 
qed_goal "equalityD2" ZF.thy "A = B ==> B<=A" 
0  143 
(fn prems=> 
144 
[ (rtac (extension RS iffD1 RS conjunct2) 1), 

145 
(resolve_tac prems 1) ]); 

146 

775  147 
qed_goal "equalityE" ZF.thy 
0  148 
"[ A = B; [ A<=B; B<=A ] ==> P ] ==> P" 
149 
(fn prems=> 

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

151 

775  152 
qed_goal "equalityCE" ZF.thy 
37  153 
"[ A = B; [ c:A; c:B ] ==> P; [ c~:A; c~:B ] ==> P ] ==> P" 
0  154 
(fn major::prems=> 
155 
[ (rtac (major RS equalityE) 1), 

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

157 

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

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

160 
put universal quantifiers over the free variables in p. 

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

775  162 
qed_goal "setup_induction" ZF.thy 
0  163 
"[ p: A; !!z. z: A ==> p=z > R ] ==> R" 
164 
(fn prems=> 

165 
[ (rtac mp 1), 

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

167 

168 

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

170 

775  171 
qed_goalw "Replace_iff" ZF.thy [Replace_def] 
0  172 
"b : {y. x:A, P(x,y)} <> (EX x:A. P(x,b) & (ALL y. P(x,y) > y=b))" 
173 
(fn _=> 

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

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

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

177 

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

775  179 
qed_goal "ReplaceI" ZF.thy 
485  180 
"[ P(x,b); x: A; !!y. P(x,y) ==> y=b ] ==> \ 
0  181 
\ b : {y. x:A, P(x,y)}" 
182 
(fn prems=> 

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

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

185 

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

775  187 
qed_goal "ReplaceE" ZF.thy 
0  188 
"[ b : {y. x:A, P(x,y)}; \ 
189 
\ !!x. [ x: A; P(x,b); ALL y. P(x,y)>y=b ] ==> R \ 

190 
\ ] ==> R" 

191 
(fn prems=> 

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

193 
(etac conjE 2), 

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

195 

485  196 
(*As above but without the (generally useless) 3rd assumption*) 
775  197 
qed_goal "ReplaceE2" ZF.thy 
485  198 
"[ b : {y. x:A, P(x,y)}; \ 
199 
\ !!x. [ x: A; P(x,b) ] ==> R \ 

200 
\ ] ==> R" 

201 
(fn major::prems=> 

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

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

204 

775  205 
qed_goal "Replace_cong" ZF.thy 
0  206 
"[ 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

207 
\ Replace(A,P) = Replace(B,Q)" 
0  208 
(fn prems=> 
209 
let val substprems = prems RL [subst, ssubst] 

210 
and iffprems = prems RL [iffD1,iffD2] 

211 
in [ (rtac equalityI 1), 

1461  212 
(REPEAT (eresolve_tac (substprems@[asm_rl, ReplaceE, spec RS mp]) 1 
213 
ORELSE resolve_tac [subsetI, ReplaceI] 1 

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

0  215 
end); 
216 

217 
(*** Rules for RepFun ***) 

218 

775  219 
qed_goalw "RepFunI" ZF.thy [RepFun_def] 
0  220 
"!!a A. a : A ==> f(a) : {f(x). x:A}" 
221 
(fn _ => [ (REPEAT (ares_tac [ReplaceI,refl] 1)) ]); 

222 

120  223 
(*Useful for coinduction proofs*) 
775  224 
qed_goal "RepFun_eqI" ZF.thy 
0  225 
"!!b a f. [ b=f(a); a : A ] ==> b : {f(x). x:A}" 
226 
(fn _ => [ etac ssubst 1, etac RepFunI 1 ]); 

227 

775  228 
qed_goalw "RepFunE" ZF.thy [RepFun_def] 
0  229 
"[ b : {f(x). x:A}; \ 
230 
\ !!x.[ x:A; b=f(x) ] ==> P ] ==> \ 

231 
\ P" 

232 
(fn major::prems=> 

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

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

235 

775  236 
qed_goalw "RepFun_cong" ZF.thy [RepFun_def] 
6
8ce8c4d13d4d
Installation of new simplifier for ZF. Deleted all congruence rules not
lcp
parents:
0
diff
changeset

237 
"[ 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

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

775  240 
qed_goalw "RepFun_iff" ZF.thy [Bex_def] 
485  241 
"b : {f(x). x:A} <> (EX x:A. b=f(x))" 
242 
(fn _ => [ (fast_tac (FOL_cs addIs [RepFunI] addSEs [RepFunE]) 1) ]); 

243 

0  244 

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

246 

247 
(*Separation is derivable from Replacement*) 

775  248 
qed_goalw "separation" ZF.thy [Collect_def] 
0  249 
"a : {x:A. P(x)} <> a:A & P(a)" 
250 
(fn _=> [ (fast_tac (FOL_cs addIs [bexI,ReplaceI] 

1461  251 
addSEs [bexE,ReplaceE]) 1) ]); 
0  252 

775  253 
qed_goal "CollectI" ZF.thy 
0  254 
"[ a:A; P(a) ] ==> a : {x:A. P(x)}" 
255 
(fn prems=> 

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

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

258 

775  259 
qed_goal "CollectE" ZF.thy 
0  260 
"[ a : {x:A. P(x)}; [ a:A; P(a) ] ==> R ] ==> R" 
261 
(fn prems=> 

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

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

264 

775  265 
qed_goal "CollectD1" ZF.thy "a : {x:A. P(x)} ==> a:A" 
0  266 
(fn [major]=> 
267 
[ (rtac (major RS CollectE) 1), 

268 
(assume_tac 1) ]); 

269 

775  270 
qed_goal "CollectD2" ZF.thy "a : {x:A. P(x)} ==> P(a)" 
0  271 
(fn [major]=> 
272 
[ (rtac (major RS CollectE) 1), 

273 
(assume_tac 1) ]); 

274 

775  275 
qed_goalw "Collect_cong" ZF.thy [Collect_def] 
6
8ce8c4d13d4d
Installation of new simplifier for ZF. Deleted all congruence rules not
lcp
parents:
0
diff
changeset

276 
"[ 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

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

279 
(*** Rules for Unions ***) 

280 

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

775  282 
qed_goal "UnionI" ZF.thy "[ B: C; A: B ] ==> A: Union(C)" 
0  283 
(fn prems=> 
485  284 
[ (resolve_tac [Union_iff RS iffD2] 1), 
0  285 
(REPEAT (resolve_tac (prems @ [bexI]) 1)) ]); 
286 

775  287 
qed_goal "UnionE" ZF.thy 
0  288 
"[ A : Union(C); !!B.[ A: B; B: C ] ==> R ] ==> R" 
289 
(fn prems=> 

485  290 
[ (resolve_tac [Union_iff RS iffD1 RS bexE] 1), 
0  291 
(REPEAT (ares_tac prems 1)) ]); 
292 

293 
(*** Rules for Inter ***) 

294 

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

775  296 
qed_goalw "Inter_iff" ZF.thy [Inter_def,Ball_def] 
0  297 
"A : Inter(C) <> (ALL x:C. A: x) & (EX x. x:C)" 
298 
(fn _=> [ (rtac (separation RS iff_trans) 1), 

1461  299 
(fast_tac (FOL_cs addIs [UnionI] addSEs [UnionE]) 1) ]); 
0  300 

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

775  302 
qed_goalw "InterI" ZF.thy [Inter_def] 
0  303 
"[ !!x. x: C ==> A: x; c:C ] ==> A : Inter(C)" 
304 
(fn prems=> 

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

306 

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

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

775  309 
qed_goalw "InterD" ZF.thy [Inter_def] 
0  310 
"[ A : Inter(C); B : C ] ==> A : B" 
311 
(fn [major,minor]=> 

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

313 
(rtac minor 1) ]); 

314 

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

775  316 
qed_goalw "InterE" ZF.thy [Inter_def] 
37  317 
"[ A : Inter(C); A:B ==> R; B~:C ==> R ] ==> R" 
0  318 
(fn major::prems=> 
319 
[ (rtac (major RS CollectD2 RS ballE) 1), 

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

321 

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

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

324 

775  325 
qed_goalw "UN_iff" ZF.thy [Bex_def] 
485  326 
"b : (UN x:A. B(x)) <> (EX x:A. b : B(x))" 
327 
(fn _=> [ (fast_tac (FOL_cs addIs [UnionI, RepFunI] 

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

329 

0  330 
(*The order of the premises presupposes that A is rigid; b may be flexible*) 
775  331 
qed_goal "UN_I" ZF.thy "[ a: A; b: B(a) ] ==> b: (UN x:A. B(x))" 
0  332 
(fn prems=> 
333 
[ (REPEAT (resolve_tac (prems@[UnionI,RepFunI]) 1)) ]); 

334 

775  335 
qed_goal "UN_E" ZF.thy 
0  336 
"[ b : (UN x:A. B(x)); !!x.[ x: A; b: B(x) ] ==> R ] ==> R" 
337 
(fn major::prems=> 

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

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

340 

775  341 
qed_goal "UN_cong" ZF.thy 
435  342 
"[ A=B; !!x. x:B ==> C(x)=D(x) ] ==> (UN x:A.C(x)) = (UN x:B.D(x))" 
343 
(fn prems=> [ (simp_tac (FOL_ss addcongs [RepFun_cong] addsimps prems) 1) ]); 

344 

0  345 

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

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

348 

775  349 
qed_goal "INT_iff" ZF.thy 
485  350 
"b : (INT x:A. B(x)) <> (ALL x:A. b : B(x)) & (EX x. x:A)" 
351 
(fn _=> [ (simp_tac (FOL_ss addsimps [Inter_def, Ball_def, Bex_def, 

1461  352 
separation, Union_iff, RepFun_iff]) 1), 
353 
(fast_tac FOL_cs 1) ]); 

485  354 

775  355 
qed_goal "INT_I" ZF.thy 
0  356 
"[ !!x. x: A ==> b: B(x); a: A ] ==> b: (INT x:A. B(x))" 
357 
(fn prems=> 

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

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

360 

775  361 
qed_goal "INT_E" ZF.thy 
0  362 
"[ b : (INT x:A. B(x)); a: A ] ==> b : B(a)" 
363 
(fn [major,minor]=> 

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

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

366 

775  367 
qed_goal "INT_cong" ZF.thy 
435  368 
"[ A=B; !!x. x:B ==> C(x)=D(x) ] ==> (INT x:A.C(x)) = (INT x:B.D(x))" 
369 
(fn prems=> [ (simp_tac (FOL_ss addcongs [RepFun_cong] addsimps prems) 1) ]); 

370 

0  371 

372 
(*** Rules for Powersets ***) 

373 

775  374 
qed_goal "PowI" ZF.thy "A <= B ==> A : Pow(B)" 
485  375 
(fn [prem]=> [ (rtac (prem RS (Pow_iff RS iffD2)) 1) ]); 
0  376 

775  377 
qed_goal "PowD" ZF.thy "A : Pow(B) ==> A<=B" 
485  378 
(fn [major]=> [ (rtac (major RS (Pow_iff RS iffD1)) 1) ]); 
0  379 

380 

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

382 

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

384 
See Suppes, page 21.*) 

775  385 
qed_goal "emptyE" ZF.thy "a:0 ==> P" 
0  386 
(fn [major]=> 
387 
[ (rtac (foundation RS disjE) 1), 

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

389 
(rtac major 1), 

390 
(etac bexE 1), 

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

392 

775  393 
qed_goal "empty_subsetI" ZF.thy "0 <= A" 
0  394 
(fn _ => [ (REPEAT (ares_tac [equalityI,subsetI,emptyE] 1)) ]); 
395 

775  396 
qed_goal "equals0I" ZF.thy "[ !!y. y:A ==> False ] ==> A=0" 
0  397 
(fn prems=> 
398 
[ (REPEAT (ares_tac (prems@[empty_subsetI,subsetI,equalityI]) 1 

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

400 

775  401 
qed_goal "equals0D" ZF.thy "[ A=0; a:A ] ==> P" 
0  402 
(fn [major,minor]=> 
403 
[ (rtac (minor RS (major RS equalityD1 RS subsetD RS emptyE)) 1) ]); 

404 

825
76d9575950f2
Added Krzysztof's theorems subst_elem, not_emptyI, not_emptyE
lcp
parents:
775
diff
changeset

405 
qed_goal "not_emptyI" ZF.thy "!!A a. a:A ==> A ~= 0" 
76d9575950f2
Added Krzysztof's theorems subst_elem, not_emptyI, not_emptyE
lcp
parents:
775
diff
changeset

406 
(fn _ => [REPEAT (ares_tac [notI, equals0D] 1)]); 
76d9575950f2
Added Krzysztof's theorems subst_elem, not_emptyI, not_emptyE
lcp
parents:
775
diff
changeset

407 

868
452f1e6ae3bc
Deleted semicolon at the end of the qed_goal line, which was preventing
lcp
parents:
854
diff
changeset

408 
qed_goal "not_emptyE" ZF.thy "[ A ~= 0; !!x. x:A ==> R ] ==> R" 
825
76d9575950f2
Added Krzysztof's theorems subst_elem, not_emptyI, not_emptyE
lcp
parents:
775
diff
changeset

409 
(fn [major,minor]=> 
76d9575950f2
Added Krzysztof's theorems subst_elem, not_emptyI, not_emptyE
lcp
parents:
775
diff
changeset

410 
[ rtac ([major, equals0I] MRS swap) 1, 
76d9575950f2
Added Krzysztof's theorems subst_elem, not_emptyI, not_emptyE
lcp
parents:
775
diff
changeset

411 
swap_res_tac [minor] 1, 
76d9575950f2
Added Krzysztof's theorems subst_elem, not_emptyI, not_emptyE
lcp
parents:
775
diff
changeset

412 
assume_tac 1 ]); 
76d9575950f2
Added Krzysztof's theorems subst_elem, not_emptyI, not_emptyE
lcp
parents:
775
diff
changeset

413 

1016
2317b680fe58
Now the classical sets include UN_E, to avoid calling hyp_subst_tac
lcp
parents:
868
diff
changeset

414 
(*A claset that leaves <= formulae unchanged! 
2317b680fe58
Now the classical sets include UN_E, to avoid calling hyp_subst_tac
lcp
parents:
868
diff
changeset

415 
UN_E appears before UnionE so that it is tried first, to avoid expensive 
2317b680fe58
Now the classical sets include UN_E, to avoid calling hyp_subst_tac
lcp
parents:
868
diff
changeset

416 
calls to hyp_subst_tac. Cannot include UN_I as it is unsafe: 
2317b680fe58
Now the classical sets include UN_E, to avoid calling hyp_subst_tac
lcp
parents:
868
diff
changeset

417 
would enlarge the search space.*) 
688  418 
val subset0_cs = FOL_cs 
419 
addSIs [ballI, InterI, CollectI, PowI, empty_subsetI] 

0  420 
addIs [bexI, UnionI, ReplaceI, RepFunI] 
1016
2317b680fe58
Now the classical sets include UN_E, to avoid calling hyp_subst_tac
lcp
parents:
868
diff
changeset

421 
addSEs [bexE, make_elim PowD, UN_E, UnionE, ReplaceE2, RepFunE, 
1461  422 
CollectE, emptyE] 
688  423 
addEs [rev_ballE, InterD, make_elim InterD, subsetD]; 
424 

425 
(*Standard claset*) 

426 
val lemmas_cs = subset0_cs addSIs [subsetI] addEs [subsetCE]; 

0  427 

748  428 
(*** Cantor's Theorem: There is no surjection from a set to its powerset. ***) 
429 

430 
val cantor_cs = FOL_cs (*precisely the rules needed for the proof*) 

431 
addSIs [ballI, CollectI, PowI, subsetI] addIs [bexI] 

432 
addSEs [CollectE, equalityCE]; 

433 

434 
(*The search is undirected; similar proof attempts may fail. 

435 
b represents ANY map, such as (lam x:A.b(x)): A>Pow(A). *) 

775  436 
qed_goal "cantor" ZF.thy "EX S: Pow(A). ALL x:A. b(x) ~= S" 
748  437 
(fn _ => [best_tac cantor_cs 1]); 
438 

516  439 
(*Lemma for the inductive definition in Zorn.thy*) 
775  440 
qed_goal "Union_in_Pow" ZF.thy 
516  441 
"!!Y. Y : Pow(Pow(A)) ==> Union(Y) : Pow(A)" 
442 
(fn _ => [fast_tac lemmas_cs 1]); 