author  paulson 
Fri, 30 Jun 2000 12:51:30 +0200  
changeset 9211  6236c5285bd8 
parent 9180  3bda56c0d70d 
child 9907  473a6604da94 
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 

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

9 
(*Useful examples: singletonI RS subst_elem, subst_elem RSN (2,IntI) *) 
5137  10 
Goal "[ b:A; a=b ] ==> a:A"; 
825
76d9575950f2
Added Krzysztof's theorems subst_elem, not_emptyI, not_emptyE
lcp
parents:
775
diff
changeset

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

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

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

14 

2469  15 

0  16 
(*** Bounded universal quantifier ***) 
17 

9211  18 
val prems= Goalw [Ball_def] 
19 
"[ !!x. x:A ==> P(x) ] ==> ALL x:A. P(x)"; 

20 
by (REPEAT (ares_tac (prems @ [allI,impI]) 1)) ; 

21 
qed "ballI"; 

0  22 

9211  23 
Goalw [Ball_def] "[ ALL x:A. P(x); x: A ] ==> P(x)"; 
24 
by (etac (spec RS mp) 1); 

25 
by (assume_tac 1) ; 

26 
qed "bspec"; 

0  27 

9211  28 
val major::prems= Goalw [Ball_def] 
29 
"[ ALL x:A. P(x); P(x) ==> Q; x~:A ==> Q ] ==> Q"; 

30 
by (rtac (major RS allE) 1); 

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

32 
qed "ballE"; 

0  33 

34 
(*Used in the datatype package*) 

9180  35 
Goal "[ x: A; ALL x:A. P(x) ] ==> P(x)"; 
36 
by (REPEAT (ares_tac [bspec] 1)) ; 

37 
qed "rev_bspec"; 

0  38 

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

9180  40 
val major::prems= Goal 
41 
"[ ALL x:A. P(x); x~:A ==> Q; P(x) ==> Q ] ==> Q"; 

42 
by (rtac (major RS ballE) 1); 

43 
by (REPEAT (eresolve_tac prems 1)) ; 

44 
qed "rev_ballE"; 

0  45 

2469  46 
AddSIs [ballI]; 
47 
AddEs [rev_ballE]; 

7531  48 
AddXDs [bspec]; 
2469  49 

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

52 

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

9180  54 
Goal "(ALL x:A. P) <> ((EX x. x:A) > P)"; 
55 
by (simp_tac (simpset() addsimps [Ball_def]) 1) ; 

56 
qed "ball_triv"; 

3425  57 
Addsimps [ball_triv]; 
0  58 

59 
(*Congruence rule for rewriting*) 

9211  60 
val prems= Goalw [Ball_def] 
61 
"[ A=A'; !!x. x:A' ==> P(x) <> P'(x) ] ==> Ball(A,P) <> Ball(A',P')"; 

62 
by (simp_tac (FOL_ss addsimps prems) 1) ; 

63 
qed "ball_cong"; 

0  64 

65 
(*** Bounded existential quantifier ***) 

66 

6287  67 
Goalw [Bex_def] "[ P(x); x: A ] ==> EX x:A. P(x)"; 
68 
by (Blast_tac 1); 

69 
qed "bexI"; 

70 

71 
(*The best argument order when there is only one x:A*) 

72 
Goalw [Bex_def] "[ x:A; P(x) ] ==> EX x:A. P(x)"; 

73 
by (Blast_tac 1); 

74 
qed "rev_bexI"; 

0  75 

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

9180  77 
val prems= Goal "[ ALL x:A. ~P(x) ==> P(a); a: A ] ==> EX x:A. P(x)"; 
78 
by (rtac classical 1); 

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

80 
qed "bexCI"; 

0  81 

9211  82 
val major::prems= Goalw [Bex_def] 
0  83 
"[ EX x:A. P(x); !!x. [ x:A; P(x) ] ==> Q \ 
9211  84 
\ ] ==> Q"; 
85 
by (rtac (major RS exE) 1); 

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

87 
qed "bexE"; 

0  88 

2469  89 
AddIs [bexI]; 
90 
AddSEs [bexE]; 

91 

0  92 
(*We do not even have (EX x:A. True) <> True unless A is nonempty!!*) 
9180  93 
Goal "(EX x:A. P) <> ((EX x. x:A) & P)"; 
94 
by (simp_tac (simpset() addsimps [Bex_def]) 1) ; 

95 
qed "bex_triv"; 

3425  96 
Addsimps [bex_triv]; 
0  97 

9211  98 
val prems= Goalw [Bex_def] 
0  99 
"[ A=A'; !!x. x:A' ==> P(x) <> P'(x) \ 
9211  100 
\ ] ==> Bex(A,P) <> Bex(A',P')"; 
101 
by (simp_tac (FOL_ss addsimps prems addcongs [conj_cong]) 1) ; 

102 
qed "bex_cong"; 

0  103 

2469  104 
Addcongs [ball_cong, bex_cong]; 
105 

106 

0  107 
(*** Rules for subsets ***) 
108 

9211  109 
val prems= Goalw [subset_def] 
110 
"(!!x. x:A ==> x:B) ==> A <= B"; 

111 
by (REPEAT (ares_tac (prems @ [ballI]) 1)) ; 

112 
qed "subsetI"; 

0  113 

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

9211  115 
Goalw [subset_def] "[ A <= B; c:A ] ==> c:B"; 
116 
by (etac bspec 1); 

117 
by (assume_tac 1) ; 

118 
qed "subsetD"; 

0  119 

120 
(*Classical elimination rule*) 

9211  121 
val major::prems= Goalw [subset_def] 
122 
"[ A <= B; c~:A ==> P; c:B ==> P ] ==> P"; 

123 
by (rtac (major RS ballE) 1); 

124 
by (REPEAT (eresolve_tac prems 1)) ; 

125 
qed "subsetCE"; 

0  126 

2469  127 
AddSIs [subsetI]; 
128 
AddEs [subsetCE, subsetD]; 

129 

130 

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

133 

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

9180  135 
Goal "[ c:A; A<=B ] ==> c:B"; 
136 
by (Blast_tac 1); 

137 
qed "rev_subsetD"; 

0  138 

6111  139 
(*Converts A<=B to x:A ==> x:B*) 
140 
fun impOfSubs th = th RSN (2, rev_subsetD); 

141 

9180  142 
Goal "[ A <= B; c ~: B ] ==> c ~: A"; 
143 
by (Blast_tac 1); 

144 
qed "contra_subsetD"; 

1889  145 

9180  146 
Goal "[ c ~: B; A <= B ] ==> c ~: A"; 
147 
by (Blast_tac 1); 

148 
qed "rev_contra_subsetD"; 

1889  149 

9180  150 
Goal "A <= A"; 
151 
by (Blast_tac 1); 

152 
qed "subset_refl"; 

0  153 

2469  154 
Addsimps [subset_refl]; 
155 

9180  156 
Goal "[ A<=B; B<=C ] ==> A<=C"; 
157 
by (Blast_tac 1); 

158 
qed "subset_trans"; 

0  159 

435  160 
(*Useful for proving A<=B by rewriting in some cases*) 
9211  161 
Goalw [subset_def,Ball_def] 
162 
"A<=B <> (ALL x. x:A > x:B)"; 

163 
by (rtac iff_refl 1) ; 

164 
qed "subset_iff"; 

435  165 

0  166 

167 
(*** Rules for equality ***) 

168 

169 
(*Antisymmetry of the subset relation*) 

9180  170 
Goal "[ A <= B; B <= A ] ==> A = B"; 
171 
by (REPEAT (ares_tac [conjI, extension RS iffD2] 1)) ; 

172 
qed "equalityI"; 

0  173 

2493  174 
AddIs [equalityI]; 
175 

9180  176 
val [prem] = Goal "(!!x. x:A <> x:B) ==> A = B"; 
177 
by (rtac equalityI 1); 

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

179 
qed "equality_iffI"; 

0  180 

2469  181 
bind_thm ("equalityD1", extension RS iffD1 RS conjunct1); 
182 
bind_thm ("equalityD2", extension RS iffD1 RS conjunct2); 

0  183 

9180  184 
val prems = Goal "[ A = B; [ A<=B; B<=A ] ==> P ] ==> P"; 
185 
by (DEPTH_SOLVE (resolve_tac (prems@[equalityD1,equalityD2]) 1)) ; 

186 
qed "equalityE"; 

0  187 

9180  188 
val major::prems= Goal 
189 
"[ A = B; [ c:A; c:B ] ==> P; [ c~:A; c~:B ] ==> P ] ==> P"; 

190 
by (rtac (major RS equalityE) 1); 

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

192 
qed "equalityCE"; 

0  193 

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

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

196 
put universal quantifiers over the free variables in p. 

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

9180  198 
val prems = Goal "[ p: A; !!z. z: A ==> p=z > R ] ==> R"; 
199 
by (rtac mp 1); 

200 
by (REPEAT (resolve_tac (refl::prems) 1)) ; 

201 
qed "setup_induction"; 

0  202 

203 

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

205 

9211  206 
Goalw [Replace_def] 
207 
"b : {y. x:A, P(x,y)} <> (EX x:A. P(x,b) & (ALL y. P(x,y) > y=b))"; 

208 
by (rtac (replacement RS iff_trans) 1); 

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

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

211 
qed "Replace_iff"; 

0  212 

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

9180  214 
val prems = Goal 
485  215 
"[ P(x,b); x: A; !!y. P(x,y) ==> y=b ] ==> \ 
9180  216 
\ b : {y. x:A, P(x,y)}"; 
217 
by (rtac (Replace_iff RS iffD2) 1); 

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

219 
qed "ReplaceI"; 

0  220 

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

9180  222 
val prems = Goal 
0  223 
"[ b : {y. x:A, P(x,y)}; \ 
224 
\ !!x. [ x: A; P(x,b); ALL y. P(x,y)>y=b ] ==> R \ 

9180  225 
\ ] ==> R"; 
226 
by (rtac (Replace_iff RS iffD1 RS bexE) 1); 

227 
by (etac conjE 2); 

228 
by (REPEAT (ares_tac prems 1)) ; 

229 
qed "ReplaceE"; 

0  230 

485  231 
(*As above but without the (generally useless) 3rd assumption*) 
9180  232 
val major::prems = Goal 
485  233 
"[ b : {y. x:A, P(x,y)}; \ 
234 
\ !!x. [ x: A; P(x,b) ] ==> R \ 

9180  235 
\ ] ==> R"; 
236 
by (rtac (major RS ReplaceE) 1); 

237 
by (REPEAT (ares_tac prems 1)) ; 

238 
qed "ReplaceE2"; 

485  239 

2469  240 
AddIs [ReplaceI]; 
241 
AddSEs [ReplaceE2]; 

242 

9180  243 
val prems = Goal 
0  244 
"[ A=B; !!x y. x:B ==> P(x,y) <> Q(x,y) ] ==> \ 
9180  245 
\ Replace(A,P) = Replace(B,Q)"; 
246 
by (rtac equalityI 1); 

247 
by (REPEAT 

248 
(eresolve_tac ((prems RL [subst, ssubst])@[asm_rl, ReplaceE, spec RS mp]) 1 ORELSE resolve_tac [subsetI, ReplaceI] 1 

249 
ORELSE (resolve_tac (prems RL [iffD1,iffD2]) 1 THEN assume_tac 2))); 

250 
qed "Replace_cong"; 

0  251 

2469  252 
Addcongs [Replace_cong]; 
253 

0  254 
(*** Rules for RepFun ***) 
255 

9211  256 
Goalw [RepFun_def] "a : A ==> f(a) : {f(x). x:A}"; 
257 
by (REPEAT (ares_tac [ReplaceI,refl] 1)) ; 

258 
qed "RepFunI"; 

0  259 

120  260 
(*Useful for coinduction proofs*) 
9180  261 
Goal "[ b=f(a); a : A ] ==> b : {f(x). x:A}"; 
262 
by (etac ssubst 1); 

263 
by (etac RepFunI 1) ; 

264 
qed "RepFun_eqI"; 

0  265 

9211  266 
val major::prems= Goalw [RepFun_def] 
0  267 
"[ b : {f(x). x:A}; \ 
268 
\ !!x.[ x:A; b=f(x) ] ==> P ] ==> \ 

9211  269 
\ P"; 
270 
by (rtac (major RS ReplaceE) 1); 

271 
by (REPEAT (ares_tac prems 1)) ; 

272 
qed "RepFunE"; 

0  273 

2716  274 
AddIs [RepFun_eqI]; 
2469  275 
AddSEs [RepFunE]; 
276 

9211  277 
val prems= Goalw [RepFun_def] 
278 
"[ A=B; !!x. x:B ==> f(x)=g(x) ] ==> RepFun(A,f) = RepFun(B,g)"; 

279 
by (simp_tac (simpset() addsimps prems) 1) ; 

280 
qed "RepFun_cong"; 

2469  281 

282 
Addcongs [RepFun_cong]; 

0  283 

9211  284 
Goalw [Bex_def] "b : {f(x). x:A} <> (EX x:A. b=f(x))"; 
285 
by (Blast_tac 1); 

286 
qed "RepFun_iff"; 

485  287 

5067  288 
Goal "{x. x:A} = A"; 
2877  289 
by (Blast_tac 1); 
2469  290 
qed "triv_RepFun"; 
291 

292 
Addsimps [RepFun_iff, triv_RepFun]; 

0  293 

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

295 

296 
(*Separation is derivable from Replacement*) 

9211  297 
Goalw [Collect_def] "a : {x:A. P(x)} <> a:A & P(a)"; 
298 
by (Blast_tac 1); 

299 
qed "separation"; 

2469  300 

301 
Addsimps [separation]; 

0  302 

9180  303 
Goal "[ a:A; P(a) ] ==> a : {x:A. P(x)}"; 
304 
by (Asm_simp_tac 1); 

305 
qed "CollectI"; 

306 

307 
val prems = Goal 

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

309 
by (rtac (separation RS iffD1 RS conjE) 1); 

310 
by (REPEAT (ares_tac prems 1)) ; 

311 
qed "CollectE"; 

0  312 

9180  313 
Goal "a : {x:A. P(x)} ==> a:A"; 
314 
by (etac CollectE 1); 

315 
by (assume_tac 1) ; 

316 
qed "CollectD1"; 

0  317 

9180  318 
Goal "a : {x:A. P(x)} ==> P(a)"; 
319 
by (etac CollectE 1); 

320 
by (assume_tac 1) ; 

321 
qed "CollectD2"; 

0  322 

9211  323 
val prems= Goalw [Collect_def] 
324 
"[ A=B; !!x. x:B ==> P(x) <> Q(x) ] ==> Collect(A,P) = Collect(B,Q)"; 

325 
by (simp_tac (simpset() addsimps prems) 1) ; 

326 
qed "Collect_cong"; 

2469  327 

328 
AddSIs [CollectI]; 

329 
AddSEs [CollectE]; 

330 
Addcongs [Collect_cong]; 

0  331 

332 
(*** Rules for Unions ***) 

333 

2469  334 
Addsimps [Union_iff]; 
335 

0  336 
(*The order of the premises presupposes that C is rigid; A may be flexible*) 
9180  337 
Goal "[ B: C; A: B ] ==> A: Union(C)"; 
338 
by (Simp_tac 1); 

339 
by (Blast_tac 1) ; 

340 
qed "UnionI"; 

0  341 

9180  342 
val prems = Goal "[ A : Union(C); !!B.[ A: B; B: C ] ==> R ] ==> R"; 
343 
by (resolve_tac [Union_iff RS iffD1 RS bexE] 1); 

344 
by (REPEAT (ares_tac prems 1)) ; 

345 
qed "UnionE"; 

0  346 

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

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

349 

9211  350 
Goalw [Bex_def] "b : (UN x:A. B(x)) <> (EX x:A. b : B(x))"; 
351 
by (Simp_tac 1); 

352 
by (Blast_tac 1) ; 

353 
qed "UN_iff"; 

2469  354 

355 
Addsimps [UN_iff]; 

485  356 

0  357 
(*The order of the premises presupposes that A is rigid; b may be flexible*) 
9180  358 
Goal "[ a: A; b: B(a) ] ==> b: (UN x:A. B(x))"; 
359 
by (Simp_tac 1); 

360 
by (Blast_tac 1) ; 

361 
qed "UN_I"; 

0  362 

9180  363 
val major::prems= Goal 
364 
"[ b : (UN x:A. B(x)); !!x.[ x: A; b: B(x) ] ==> R ] ==> R"; 

365 
by (rtac (major RS UnionE) 1); 

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

367 
qed "UN_E"; 

0  368 

9180  369 
val prems = Goal 
370 
"[ A=B; !!x. x:B ==> C(x)=D(x) ] ==> (UN x:A. C(x)) = (UN x:B. D(x))"; 

371 
by (simp_tac (simpset() addsimps prems) 1) ; 

372 
qed "UN_cong"; 

2469  373 

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

375 

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

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

378 
the search space.*) 

379 
AddIs [UnionI]; 

380 
AddSEs [UN_E]; 

381 
AddSEs [UnionE]; 

382 

383 

384 
(*** Rules for Inter ***) 

385 

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

9211  387 
Goalw [Inter_def,Ball_def] 
388 
"A : Inter(C) <> (ALL x:C. A: x) & (EX x. x:C)"; 

389 
by (Simp_tac 1); 

390 
by (Blast_tac 1) ; 

391 
qed "Inter_iff"; 

435  392 

2469  393 
(* Intersection is wellbehaved only if the family is nonempty! *) 
9180  394 
val prems = Goal 
395 
"[ !!x. x: C ==> A: x; EX c. c:C ] ==> A : Inter(C)"; 

396 
by (simp_tac (simpset() addsimps [Inter_iff]) 1); 

397 
by (blast_tac (claset() addIs prems) 1) ; 

398 
qed "InterI"; 

2469  399 

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

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

9211  402 
Goalw [Inter_def] "[ A : Inter(C); B : C ] ==> A : B"; 
403 
by (Blast_tac 1); 

404 
qed "InterD"; 

2469  405 

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

9211  407 
val major::prems= Goalw [Inter_def] 
408 
"[ A : Inter(C); B~:C ==> R; A:B ==> R ] ==> R"; 

409 
by (rtac (major RS CollectD2 RS ballE) 1); 

410 
by (REPEAT (eresolve_tac prems 1)) ; 

411 
qed "InterE"; 

2469  412 

413 
AddSIs [InterI]; 

2716  414 
AddEs [InterD, InterE]; 
0  415 

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

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

418 

9211  419 
Goalw [Inter_def] "b : (INT x:A. B(x)) <> (ALL x:A. b : B(x)) & (EX x. x:A)"; 
420 
by (Simp_tac 1); 

421 
by (Best_tac 1) ; 

422 
qed "INT_iff"; 

485  423 

9180  424 
val prems = Goal 
425 
"[ !!x. x: A ==> b: B(x); a: A ] ==> b: (INT x:A. B(x))"; 

426 
by (blast_tac (claset() addIs prems) 1); 

427 
qed "INT_I"; 

0  428 

9180  429 
Goal "[ b : (INT x:A. B(x)); a: A ] ==> b : B(a)"; 
430 
by (Blast_tac 1); 

431 
qed "INT_E"; 

0  432 

9180  433 
val prems = Goal 
434 
"[ A=B; !!x. x:B ==> C(x)=D(x) ] ==> (INT x:A. C(x)) = (INT x:B. D(x))"; 

435 
by (simp_tac (simpset() addsimps prems) 1) ; 

436 
qed "INT_cong"; 

2469  437 

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

435  439 

0  440 

441 
(*** Rules for Powersets ***) 

442 

9180  443 
Goal "A <= B ==> A : Pow(B)"; 
444 
by (etac (Pow_iff RS iffD2) 1) ; 

445 
qed "PowI"; 

0  446 

9180  447 
Goal "A : Pow(B) ==> A<=B"; 
448 
by (etac (Pow_iff RS iffD1) 1) ; 

449 
qed "PowD"; 

0  450 

2469  451 
AddSIs [PowI]; 
452 
AddSDs [PowD]; 

453 

0  454 

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

456 

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

458 
See Suppes, page 21.*) 

9180  459 
Goal "a ~: 0"; 
460 
by (cut_facts_tac [foundation] 1); 

461 
by (best_tac (claset() addDs [equalityD2]) 1) ; 

462 
qed "not_mem_empty"; 

2469  463 

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

465 

466 
Addsimps [not_mem_empty]; 

467 
AddSEs [emptyE]; 

0  468 

9180  469 
Goal "0 <= A"; 
470 
by (Blast_tac 1); 

471 
qed "empty_subsetI"; 

2469  472 

473 
Addsimps [empty_subsetI]; 

0  474 

9180  475 
val prems = Goal "[ !!y. y:A ==> False ] ==> A=0"; 
476 
by (blast_tac (claset() addDs prems) 1) ; 

477 
qed "equals0I"; 

0  478 

9180  479 
Goal "A=0 ==> a ~: A"; 
480 
by (Blast_tac 1); 

481 
qed "equals0D"; 

0  482 

5467  483 
AddDs [equals0D, sym RS equals0D]; 
5265
9d1d4c43c76d
Disjointness reasoning by AddEs [equals0E, sym RS equals0E]
paulson
parents:
5242
diff
changeset

484 

9180  485 
Goal "a:A ==> A ~= 0"; 
486 
by (Blast_tac 1); 

487 
qed "not_emptyI"; 

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

488 

9180  489 
val [major,minor]= Goal "[ A ~= 0; !!x. x:A ==> R ] ==> R"; 
490 
by (rtac ([major, equals0I] MRS swap) 1); 

491 
by (swap_res_tac [minor] 1); 

492 
by (assume_tac 1) ; 

493 
qed "not_emptyE"; 

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

494 

0  495 

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

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

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

500 
addSEs [CollectE, equalityCE]; 

501 

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

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

9180  504 
Goal "EX S: Pow(A). ALL x:A. b(x) ~= S"; 
505 
by (best_tac cantor_cs 1); 

506 
qed "cantor"; 

748  507 

516  508 
(*Lemma for the inductive definition in Zorn.thy*) 
9180  509 
Goal "Y : Pow(Pow(A)) ==> Union(Y) : Pow(A)"; 
510 
by (Blast_tac 1); 

511 
qed "Union_in_Pow"; 

1902
e349b91cf197
Added function for storing default claset in theory.
berghofe
parents:
1889
diff
changeset

512 

6111  513 

514 
local 

515 
val (bspecT, bspec') = make_new_spec bspec 

516 
in 

517 

518 
fun RSbspec th = 

519 
(case concl_of th of 

520 
_ $ (Const("Ball",_) $ _ $ Abs(a,_,_)) => 

521 
let val ca = cterm_of (#sign(rep_thm th)) (Var((a,0),bspecT)) 

522 
in th RS forall_elim ca bspec' end 

523 
 _ => raise THM("RSbspec",0,[th])); 

524 

525 
val normalize_thm_ZF = normalize_thm [RSspec,RSbspec,RSmp]; 

526 

527 
fun qed_spec_mp name = 

528 
let val thm = normalize_thm_ZF (result()) 

529 
in bind_thm(name, thm) end; 

530 

531 
fun qed_goal_spec_mp name thy s p = 

532 
bind_thm (name, normalize_thm_ZF (prove_goal thy s p)); 

533 

534 
fun qed_goalw_spec_mp name thy defs s p = 

535 
bind_thm (name, normalize_thm_ZF (prove_goalw thy defs s p)); 

536 

537 
end; 

538 

539 

540 
(* attributes *) 

541 

542 
local 

543 

544 
fun gen_rulify x = 

545 
Attrib.no_args (Drule.rule_attribute (K (normalize_thm_ZF))) x; 

546 

547 
in 

548 

549 
val attrib_setup = 

550 
[Attrib.add_attributes 

551 
[("rulify", (gen_rulify, gen_rulify), 

552 
"put theorem into standard rule form")]]; 

553 

554 
end; 