author  wenzelm 
Wed, 05 Dec 2001 03:07:44 +0100  
changeset 12372  cd3a09c7dac9 
parent 11770  b6bb7a853dd2 
child 12836  5ef96e63fba6 
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); 
9907  13 
qed "subst_elem"; 
825
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]; 

48 

0  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!*) 

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

55 
qed "ball_triv"; 

3425  56 
Addsimps [ball_triv]; 
0  57 

58 
(*Congruence rule for rewriting*) 

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

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

62 
qed "ball_cong"; 

0  63 

64 
(*** Bounded existential quantifier ***) 

65 

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

68 
qed "bexI"; 

69 

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

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

72 
by (Blast_tac 1); 

73 
qed "rev_bexI"; 

0  74 

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

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

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

79 
qed "bexCI"; 

0  80 

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

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

86 
qed "bexE"; 

0  87 

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

90 

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

94 
qed "bex_triv"; 

3425  95 
Addsimps [bex_triv]; 
0  96 

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

101 
qed "bex_cong"; 

0  102 

2469  103 
Addcongs [ball_cong, bex_cong]; 
104 

105 

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

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

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

111 
qed "subsetI"; 

0  112 

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

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

116 
by (assume_tac 1) ; 

117 
qed "subsetD"; 

0  118 

119 
(*Classical elimination rule*) 

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

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

123 
by (REPEAT (eresolve_tac prems 1)) ; 

124 
qed "subsetCE"; 

0  125 

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

128 

129 

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

132 

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

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

136 
qed "rev_subsetD"; 

0  137 

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

140 

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

143 
qed "contra_subsetD"; 

1889  144 

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

147 
qed "rev_contra_subsetD"; 

1889  148 

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

151 
qed "subset_refl"; 

0  152 

2469  153 
Addsimps [subset_refl]; 
154 

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

157 
qed "subset_trans"; 

0  158 

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

162 
by (rtac iff_refl 1) ; 

163 
qed "subset_iff"; 

435  164 

0  165 

166 
(*** Rules for equality ***) 

167 

168 
(*Antisymmetry of the subset relation*) 

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

171 
qed "equalityI"; 

0  172 

2493  173 
AddIs [equalityI]; 
174 

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

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

178 
qed "equality_iffI"; 

0  179 

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

0  182 

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

185 
qed "equalityE"; 

0  186 

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

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

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

191 
qed "equalityCE"; 

0  192 

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

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

195 
put universal quantifiers over the free variables in p. 

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

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

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

200 
qed "setup_induction"; 

0  201 

202 

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

204 

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

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

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

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

210 
qed "Replace_iff"; 

0  211 

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

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

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

218 
qed "ReplaceI"; 

0  219 

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

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

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

226 
by (etac conjE 2); 

227 
by (REPEAT (ares_tac prems 1)) ; 

228 
qed "ReplaceE"; 

0  229 

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

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

236 
by (REPEAT (ares_tac prems 1)) ; 

237 
qed "ReplaceE2"; 

485  238 

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

241 

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

246 
by (REPEAT 

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

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

249 
qed "Replace_cong"; 

0  250 

2469  251 
Addcongs [Replace_cong]; 
252 

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

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

257 
qed "RepFunI"; 

0  258 

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

262 
by (etac RepFunI 1) ; 

263 
qed "RepFun_eqI"; 

0  264 

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

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

270 
by (REPEAT (ares_tac prems 1)) ; 

271 
qed "RepFunE"; 

0  272 

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

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

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

279 
qed "RepFun_cong"; 

2469  280 

281 
Addcongs [RepFun_cong]; 

0  282 

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

285 
qed "RepFun_iff"; 

485  286 

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

291 
Addsimps [RepFun_iff, triv_RepFun]; 

0  292 

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

294 

295 
(*Separation is derivable from Replacement*) 

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

298 
qed "separation"; 

2469  299 

300 
Addsimps [separation]; 

0  301 

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

304 
qed "CollectI"; 

305 

306 
val prems = Goal 

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

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

309 
by (REPEAT (ares_tac prems 1)) ; 

310 
qed "CollectE"; 

0  311 

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

314 
by (assume_tac 1) ; 

315 
qed "CollectD1"; 

0  316 

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

319 
by (assume_tac 1) ; 

320 
qed "CollectD2"; 

0  321 

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

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

325 
qed "Collect_cong"; 

2469  326 

327 
AddSIs [CollectI]; 

328 
AddSEs [CollectE]; 

329 
Addcongs [Collect_cong]; 

0  330 

331 
(*** Rules for Unions ***) 

332 

2469  333 
Addsimps [Union_iff]; 
334 

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

338 
by (Blast_tac 1) ; 

339 
qed "UnionI"; 

0  340 

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

343 
by (REPEAT (ares_tac prems 1)) ; 

344 
qed "UnionE"; 

0  345 

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

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

348 

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

351 
by (Blast_tac 1) ; 

352 
qed "UN_iff"; 

2469  353 

354 
Addsimps [UN_iff]; 

485  355 

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

359 
by (Blast_tac 1) ; 

360 
qed "UN_I"; 

0  361 

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

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

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

366 
qed "UN_E"; 

0  367 

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

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

371 
qed "UN_cong"; 

2469  372 

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

374 

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

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

377 
the search space.*) 

378 
AddIs [UnionI]; 

379 
AddSEs [UN_E]; 

380 
AddSEs [UnionE]; 

381 

382 

383 
(*** Rules for Inter ***) 

384 

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

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

388 
by (Simp_tac 1); 

389 
by (Blast_tac 1) ; 

390 
qed "Inter_iff"; 

435  391 

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

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

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

397 
qed "InterI"; 

2469  398 

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

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

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

403 
qed "InterD"; 

2469  404 

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

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

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

409 
by (REPEAT (eresolve_tac prems 1)) ; 

410 
qed "InterE"; 

2469  411 

412 
AddSIs [InterI]; 

2716  413 
AddEs [InterD, InterE]; 
0  414 

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

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

417 

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

420 
by (Best_tac 1) ; 

421 
qed "INT_iff"; 

485  422 

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

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

426 
qed "INT_I"; 

0  427 

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

430 
qed "INT_E"; 

0  431 

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

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

435 
qed "INT_cong"; 

2469  436 

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

435  438 

0  439 

440 
(*** Rules for Powersets ***) 

441 

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

444 
qed "PowI"; 

0  445 

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

448 
qed "PowD"; 

0  449 

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

452 

0  453 

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

455 

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

457 
See Suppes, page 21.*) 

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

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

461 
qed "not_mem_empty"; 

2469  462 

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

464 

465 
Addsimps [not_mem_empty]; 

466 
AddSEs [emptyE]; 

0  467 

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

470 
qed "empty_subsetI"; 

2469  471 

472 
Addsimps [empty_subsetI]; 

0  473 

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

476 
qed "equals0I"; 

0  477 

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

480 
qed "equals0D"; 

0  481 

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

483 

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

486 
qed "not_emptyI"; 

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

487 

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

490 
by (swap_res_tac [minor] 1); 

491 
by (assume_tac 1) ; 

492 
qed "not_emptyE"; 

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

493 

0  494 

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

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

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

499 
addSEs [CollectE, equalityCE]; 

500 

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

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

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

505 
qed "cantor"; 

748  506 

9907  507 
(*Lemma for the inductive definition in theory Zorn*) 
9180  508 
Goal "Y : Pow(Pow(A)) ==> Union(Y) : Pow(A)"; 
509 
by (Blast_tac 1); 

510 
qed "Union_in_Pow"; 

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

511 

9907  512 
Goal "(!!x. x:A ==> P(x)) == Trueprop (ALL x:A. P(x))"; 
11766  513 
by (simp_tac (simpset () addsimps [Ball_def, thm "atomize_all", thm "atomize_imp"]) 1); 
514 
qed "atomize_ball"; 