author  paulson 
Fri, 03 Jan 1997 15:01:55 +0100  
changeset 2469  b50b8c0eec01 
parent 1902  e349b91cf197 
child 2493  bdeb5024353a 
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 

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

11 
(*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

12 
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

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

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

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

16 

2469  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 

2469  49 
AddSIs [ballI]; 
50 
AddEs [rev_ballE]; 

51 

0  52 
(*Takes assumptions ALL x:A.P(x) and a:A; creates assumption P(a)*) 
53 
val ball_tac = dtac bspec THEN' assume_tac; 

54 

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

775  56 
qed_goal "ball_simp" ZF.thy "(ALL x:A. True) <> True" 
2469  57 
(fn _=> [ Fast_tac 1 ]); 
58 

59 
Addsimps [ball_simp]; 

0  60 

61 
(*Congruence rule for rewriting*) 

775  62 
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

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

64 
(fn prems=> [ (simp_tac (FOL_ss addsimps prems) 1) ]); 
0  65 

66 
(*** Bounded existential quantifier ***) 

67 

775  68 
qed_goalw "bexI" ZF.thy [Bex_def] 
2469  69 
"!!P. [ P(x); x: A ] ==> EX x:A. P(x)" 
70 
(fn _=> [ Fast_tac 1 ]); 

0  71 

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

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

76 
[ (rtac classical 1), 

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

78 

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

82 
(fn major::prems=> 

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

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

85 

2469  86 
AddIs [bexI]; 
87 
AddSEs [bexE]; 

88 

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

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

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

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

2469  96 
Addcongs [ball_cong, bex_cong]; 
97 

98 

0  99 
(*** Rules for subsets ***) 
100 

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

104 

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

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

109 
(resolve_tac prems 1) ]); 

110 

111 
(*Classical elimination rule*) 

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

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

117 

2469  118 
AddSIs [subsetI]; 
119 
AddEs [subsetCE, subsetD]; 

120 

121 

0  122 
(*Takes assumptions A<=B; c:A and creates the assumption c:B *) 
123 
val set_mp_tac = dtac subsetD THEN' assume_tac; 

124 

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

775  126 
qed_goal "rev_subsetD" ZF.thy "!!A B c. [ c:A; A<=B ] ==> c:B" 
2469  127 
(fn _=> [ Fast_tac 1 ]); 
0  128 

1889  129 
qed_goal "contra_subsetD" ZF.thy "!!c. [ A <= B; c ~: B ] ==> c ~: A" 
2469  130 
(fn _=> [ Fast_tac 1 ]); 
1889  131 

132 
qed_goal "rev_contra_subsetD" ZF.thy "!!c. [ c ~: B; A <= B ] ==> c ~: A" 

2469  133 
(fn _=> [ Fast_tac 1 ]); 
1889  134 

775  135 
qed_goal "subset_refl" ZF.thy "A <= A" 
2469  136 
(fn _=> [ Fast_tac 1 ]); 
0  137 

2469  138 
Addsimps [subset_refl]; 
139 

140 
qed_goal "subset_trans" ZF.thy "!!A B C. [ A<=B; B<=C ] ==> A<=C" 

141 
(fn _=> [ Fast_tac 1 ]); 

0  142 

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

147 

0  148 

149 
(*** Rules for equality ***) 

150 

151 
(*Antisymmetry of the subset relation*) 

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

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

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

159 

2469  160 
bind_thm ("equalityD1", extension RS iffD1 RS conjunct1); 
161 
bind_thm ("equalityD2", extension RS iffD1 RS conjunct2); 

0  162 

775  163 
qed_goal "equalityE" ZF.thy 
0  164 
"[ A = B; [ A<=B; B<=A ] ==> P ] ==> P" 
165 
(fn prems=> 

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

167 

775  168 
qed_goal "equalityCE" ZF.thy 
37  169 
"[ A = B; [ c:A; c:B ] ==> P; [ c~:A; c~:B ] ==> P ] ==> P" 
0  170 
(fn major::prems=> 
171 
[ (rtac (major RS equalityE) 1), 

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

173 

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

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

176 
put universal quantifiers over the free variables in p. 

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

775  178 
qed_goal "setup_induction" ZF.thy 
0  179 
"[ p: A; !!z. z: A ==> p=z > R ] ==> R" 
180 
(fn prems=> 

181 
[ (rtac mp 1), 

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

183 

184 

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

186 

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

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

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

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

193 

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

775  195 
qed_goal "ReplaceI" ZF.thy 
485  196 
"[ P(x,b); x: A; !!y. P(x,y) ==> y=b ] ==> \ 
0  197 
\ b : {y. x:A, P(x,y)}" 
198 
(fn prems=> 

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

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

201 

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

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

206 
\ ] ==> R" 

207 
(fn prems=> 

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

209 
(etac conjE 2), 

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

211 

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

216 
\ ] ==> R" 

217 
(fn major::prems=> 

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

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

220 

2469  221 
AddIs [ReplaceI]; 
222 
AddSEs [ReplaceE2]; 

223 

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

226 
\ Replace(A,P) = Replace(B,Q)" 
0  227 
(fn prems=> 
228 
let val substprems = prems RL [subst, ssubst] 

229 
and iffprems = prems RL [iffD1,iffD2] 

230 
in [ (rtac equalityI 1), 

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

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

0  234 
end); 
235 

2469  236 
Addcongs [Replace_cong]; 
237 

0  238 
(*** Rules for RepFun ***) 
239 

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

243 

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

248 

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

252 
\ P" 

253 
(fn major::prems=> 

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

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

256 

2469  257 
AddIs [RepFunI]; 
258 
AddSEs [RepFunE]; 

259 

775  260 
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

261 
"[ A=B; !!x. x:B ==> f(x)=g(x) ] ==> RepFun(A,f) = RepFun(B,g)" 
2469  262 
(fn prems=> [ (simp_tac (!simpset addsimps prems) 1) ]); 
263 

264 
Addcongs [RepFun_cong]; 

0  265 

775  266 
qed_goalw "RepFun_iff" ZF.thy [Bex_def] 
485  267 
"b : {f(x). x:A} <> (EX x:A. b=f(x))" 
2469  268 
(fn _ => [Fast_tac 1]); 
485  269 

2469  270 
goal ZF.thy "{x.x:A} = A"; 
271 
by (fast_tac (!claset addSIs [equalityI]) 1); 

272 
qed "triv_RepFun"; 

273 

274 
Addsimps [RepFun_iff, triv_RepFun]; 

0  275 

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

277 

278 
(*Separation is derivable from Replacement*) 

775  279 
qed_goalw "separation" ZF.thy [Collect_def] 
0  280 
"a : {x:A. P(x)} <> a:A & P(a)" 
2469  281 
(fn _=> [Fast_tac 1]); 
282 

283 
Addsimps [separation]; 

0  284 

775  285 
qed_goal "CollectI" ZF.thy 
2469  286 
"!!P. [ a:A; P(a) ] ==> a : {x:A. P(x)}" 
287 
(fn _=> [ Asm_simp_tac 1 ]); 

0  288 

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

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

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

294 

2469  295 
qed_goal "CollectD1" ZF.thy "!!P. a : {x:A. P(x)} ==> a:A" 
296 
(fn _=> [ (etac CollectE 1), (assume_tac 1) ]); 

0  297 

2469  298 
qed_goal "CollectD2" ZF.thy "!!P. a : {x:A. P(x)} ==> P(a)" 
299 
(fn _=> [ (etac CollectE 1), (assume_tac 1) ]); 

0  300 

775  301 
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

302 
"[ A=B; !!x. x:B ==> P(x) <> Q(x) ] ==> Collect(A,P) = Collect(B,Q)" 
2469  303 
(fn prems=> [ (simp_tac (!simpset addsimps prems) 1) ]); 
304 

305 
AddSIs [CollectI]; 

306 
AddSEs [CollectE]; 

307 
Addcongs [Collect_cong]; 

0  308 

309 
(*** Rules for Unions ***) 

310 

2469  311 
Addsimps [Union_iff]; 
312 

0  313 
(*The order of the premises presupposes that C is rigid; A may be flexible*) 
2469  314 
qed_goal "UnionI" ZF.thy "!!C. [ B: C; A: B ] ==> A: Union(C)" 
315 
(fn _=> [ Simp_tac 1, Fast_tac 1 ]); 

0  316 

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

485  320 
[ (resolve_tac [Union_iff RS iffD1 RS bexE] 1), 
0  321 
(REPEAT (ares_tac prems 1)) ]); 
322 

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

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

325 

775  326 
qed_goalw "UN_iff" ZF.thy [Bex_def] 
485  327 
"b : (UN x:A. B(x)) <> (EX x:A. b : B(x))" 
2469  328 
(fn _=> [ Simp_tac 1, Fast_tac 1 ]); 
329 

330 
Addsimps [UN_iff]; 

485  331 

0  332 
(*The order of the premises presupposes that A is rigid; b may be flexible*) 
2469  333 
qed_goal "UN_I" ZF.thy "!!A B. [ a: A; b: B(a) ] ==> b: (UN x:A. B(x))" 
334 
(fn _=> [ Simp_tac 1, Fast_tac 1 ]); 

0  335 

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

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

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

341 

775  342 
qed_goal "UN_cong" ZF.thy 
435  343 
"[ A=B; !!x. x:B ==> C(x)=D(x) ] ==> (UN x:A.C(x)) = (UN x:B.D(x))" 
2469  344 
(fn prems=> [ (simp_tac (!simpset addsimps prems) 1) ]); 
345 

346 
(*No "Addcongs [UN_cong]" because UN is a combination of constants*) 

347 

348 
(* UN_E appears before UnionE so that it is tried first, to avoid expensive 

349 
calls to hyp_subst_tac. Cannot include UN_I as it is unsafe: would enlarge 

350 
the search space.*) 

351 
AddIs [UnionI]; 

352 
AddSEs [UN_E]; 

353 
AddSEs [UnionE]; 

354 

355 

356 
(*** Rules for Inter ***) 

357 

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

359 
qed_goalw "Inter_iff" ZF.thy [Inter_def,Ball_def] 

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

361 
(fn _=> [ Simp_tac 1, Fast_tac 1 ]); 

435  362 

2469  363 
(* Intersection is wellbehaved only if the family is nonempty! *) 
364 
qed_goalw "InterI" ZF.thy [Inter_def] 

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

366 
(fn prems=> [ fast_tac (!claset addIs prems) 1 ]); 

367 

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

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

370 
qed_goalw "InterD" ZF.thy [Inter_def] 

371 
"!!C. [ A : Inter(C); B : C ] ==> A : B" 

372 
(fn _=> [ Fast_tac 1 ]); 

373 

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

375 
qed_goalw "InterE" ZF.thy [Inter_def] 

376 
"[ A : Inter(C); A:B ==> R; B~:C ==> R ] ==> R" 

377 
(fn major::prems=> 

378 
[ (rtac (major RS CollectD2 RS ballE) 1), 

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

380 

381 
AddSIs [InterI]; 

382 
AddEs [InterD, make_elim InterD]; 

0  383 

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

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

386 

2469  387 
qed_goalw "INT_iff" ZF.thy [Inter_def] 
485  388 
"b : (INT x:A. B(x)) <> (ALL x:A. b : B(x)) & (EX x. x:A)" 
2469  389 
(fn _=> [ Simp_tac 1, Best_tac 1 ]); 
485  390 

775  391 
qed_goal "INT_I" ZF.thy 
0  392 
"[ !!x. x: A ==> b: B(x); a: A ] ==> b: (INT x:A. B(x))" 
2469  393 
(fn prems=> [ fast_tac (!claset addIs prems) 1 ]); 
0  394 

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

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

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

400 

775  401 
qed_goal "INT_cong" ZF.thy 
435  402 
"[ A=B; !!x. x:B ==> C(x)=D(x) ] ==> (INT x:A.C(x)) = (INT x:B.D(x))" 
2469  403 
(fn prems=> [ (simp_tac (!simpset addsimps prems) 1) ]); 
404 

405 
(*No "Addcongs [INT_cong]" because INT is a combination of constants*) 

435  406 

0  407 

408 
(*** Rules for Powersets ***) 

409 

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

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

2469  416 
AddSIs [PowI]; 
417 
AddSDs [PowD]; 

418 

0  419 

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

421 

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

423 
See Suppes, page 21.*) 

2469  424 
qed_goal "not_mem_empty" ZF.thy "a ~: 0" 
425 
(fn _=> 

426 
[ (cut_facts_tac [foundation] 1), 

427 
(best_tac (!claset addDs [equalityD2]) 1) ]); 

428 

429 
bind_thm ("emptyE", not_mem_empty RS notE); 

430 

431 
Addsimps [not_mem_empty]; 

432 
AddSEs [emptyE]; 

0  433 

775  434 
qed_goal "empty_subsetI" ZF.thy "0 <= A" 
2469  435 
(fn _=> [ Fast_tac 1 ]); 
436 

437 
Addsimps [empty_subsetI]; 

438 
AddSIs [empty_subsetI]; 

0  439 

775  440 
qed_goal "equals0I" ZF.thy "[ !!y. y:A ==> False ] ==> A=0" 
2469  441 
(fn prems=> [ fast_tac (!claset addIs [equalityI] addDs prems) 1 ]); 
0  442 

2469  443 
qed_goal "equals0D" ZF.thy "!!P. [ A=0; a:A ] ==> P" 
444 
(fn _=> [ Full_simp_tac 1, Fast_tac 1 ]); 

0  445 

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

446 
qed_goal "not_emptyI" ZF.thy "!!A a. a:A ==> A ~= 0" 
2469  447 
(fn _=> [ Fast_tac 1 ]); 
825
76d9575950f2
Added Krzysztof's theorems subst_elem, not_emptyI, not_emptyE
lcp
parents:
775
diff
changeset

448 

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

449 
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

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

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

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

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

454 

0  455 

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

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

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

460 
addSEs [CollectE, equalityCE]; 

461 

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

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

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

516  467 
(*Lemma for the inductive definition in Zorn.thy*) 
775  468 
qed_goal "Union_in_Pow" ZF.thy 
516  469 
"!!Y. Y : Pow(Pow(A)) ==> Union(Y) : Pow(A)" 
2469  470 
(fn _ => [Fast_tac 1]); 
1902
e349b91cf197
Added function for storing default claset in theory.
berghofe
parents:
1889
diff
changeset

471 