author | paulson |
Wed, 19 Mar 1997 10:49:26 +0100 | |
changeset 2815 | c05fa3ce5439 |
parent 2716 | 9e11a914156a |
child 2877 | 6476784dba1c |
permissions | -rw-r--r-- |
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 Zermelo-Fraenkel 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 |
(*Anti-symmetry 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 |
||
2493 | 155 |
AddIs [equalityI]; |
156 |
||
775 | 157 |
qed_goal "equality_iffI" ZF.thy "(!!x. x:A <-> x:B) ==> A = B" |
0 | 158 |
(fn [prem] => |
159 |
[ (rtac equalityI 1), |
|
160 |
(REPEAT (ares_tac [subsetI, prem RS iffD1, prem RS iffD2] 1)) ]); |
|
161 |
||
2469 | 162 |
bind_thm ("equalityD1", extension RS iffD1 RS conjunct1); |
163 |
bind_thm ("equalityD2", extension RS iffD1 RS conjunct2); |
|
0 | 164 |
|
775 | 165 |
qed_goal "equalityE" ZF.thy |
0 | 166 |
"[| A = B; [| A<=B; B<=A |] ==> P |] ==> P" |
167 |
(fn prems=> |
|
168 |
[ (DEPTH_SOLVE (resolve_tac (prems@[equalityD1,equalityD2]) 1)) ]); |
|
169 |
||
775 | 170 |
qed_goal "equalityCE" ZF.thy |
37 | 171 |
"[| A = B; [| c:A; c:B |] ==> P; [| c~:A; c~:B |] ==> P |] ==> P" |
0 | 172 |
(fn major::prems=> |
173 |
[ (rtac (major RS equalityE) 1), |
|
174 |
(REPEAT (contr_tac 1 ORELSE eresolve_tac ([asm_rl,subsetCE]@prems) 1)) ]); |
|
175 |
||
176 |
(*Lemma for creating induction formulae -- for "pattern matching" on p |
|
177 |
To make the induction hypotheses usable, apply "spec" or "bspec" to |
|
178 |
put universal quantifiers over the free variables in p. |
|
179 |
Would it be better to do subgoal_tac "ALL z. p = f(z) --> R(z)" ??*) |
|
775 | 180 |
qed_goal "setup_induction" ZF.thy |
0 | 181 |
"[| p: A; !!z. z: A ==> p=z --> R |] ==> R" |
182 |
(fn prems=> |
|
183 |
[ (rtac mp 1), |
|
184 |
(REPEAT (resolve_tac (refl::prems) 1)) ]); |
|
185 |
||
186 |
||
187 |
(*** Rules for Replace -- the derived form of replacement ***) |
|
188 |
||
775 | 189 |
qed_goalw "Replace_iff" ZF.thy [Replace_def] |
0 | 190 |
"b : {y. x:A, P(x,y)} <-> (EX x:A. P(x,b) & (ALL y. P(x,y) --> y=b))" |
191 |
(fn _=> |
|
192 |
[ (rtac (replacement RS iff_trans) 1), |
|
193 |
(REPEAT (ares_tac [refl,bex_cong,iffI,ballI,allI,conjI,impI,ex1I] 1 |
|
194 |
ORELSE eresolve_tac [conjE, spec RS mp, ex1_functional] 1)) ]); |
|
195 |
||
196 |
(*Introduction; there must be a unique y such that P(x,y), namely y=b. *) |
|
775 | 197 |
qed_goal "ReplaceI" ZF.thy |
485 | 198 |
"[| P(x,b); x: A; !!y. P(x,y) ==> y=b |] ==> \ |
0 | 199 |
\ b : {y. x:A, P(x,y)}" |
200 |
(fn prems=> |
|
201 |
[ (rtac (Replace_iff RS iffD2) 1), |
|
202 |
(REPEAT (ares_tac (prems@[bexI,conjI,allI,impI]) 1)) ]); |
|
203 |
||
204 |
(*Elimination; may asssume there is a unique y such that P(x,y), namely y=b. *) |
|
775 | 205 |
qed_goal "ReplaceE" ZF.thy |
0 | 206 |
"[| b : {y. x:A, P(x,y)}; \ |
207 |
\ !!x. [| x: A; P(x,b); ALL y. P(x,y)-->y=b |] ==> R \ |
|
208 |
\ |] ==> R" |
|
209 |
(fn prems=> |
|
210 |
[ (rtac (Replace_iff RS iffD1 RS bexE) 1), |
|
211 |
(etac conjE 2), |
|
212 |
(REPEAT (ares_tac prems 1)) ]); |
|
213 |
||
485 | 214 |
(*As above but without the (generally useless) 3rd assumption*) |
775 | 215 |
qed_goal "ReplaceE2" ZF.thy |
485 | 216 |
"[| b : {y. x:A, P(x,y)}; \ |
217 |
\ !!x. [| x: A; P(x,b) |] ==> R \ |
|
218 |
\ |] ==> R" |
|
219 |
(fn major::prems=> |
|
220 |
[ (rtac (major RS ReplaceE) 1), |
|
221 |
(REPEAT (ares_tac prems 1)) ]); |
|
222 |
||
2469 | 223 |
AddIs [ReplaceI]; |
224 |
AddSEs [ReplaceE2]; |
|
225 |
||
775 | 226 |
qed_goal "Replace_cong" ZF.thy |
0 | 227 |
"[| 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
|
228 |
\ Replace(A,P) = Replace(B,Q)" |
0 | 229 |
(fn prems=> |
230 |
let val substprems = prems RL [subst, ssubst] |
|
231 |
and iffprems = prems RL [iffD1,iffD2] |
|
232 |
in [ (rtac equalityI 1), |
|
1461 | 233 |
(REPEAT (eresolve_tac (substprems@[asm_rl, ReplaceE, spec RS mp]) 1 |
234 |
ORELSE resolve_tac [subsetI, ReplaceI] 1 |
|
235 |
ORELSE (resolve_tac iffprems 1 THEN assume_tac 2))) ] |
|
0 | 236 |
end); |
237 |
||
2469 | 238 |
Addcongs [Replace_cong]; |
239 |
||
0 | 240 |
(*** Rules for RepFun ***) |
241 |
||
775 | 242 |
qed_goalw "RepFunI" ZF.thy [RepFun_def] |
0 | 243 |
"!!a A. a : A ==> f(a) : {f(x). x:A}" |
244 |
(fn _ => [ (REPEAT (ares_tac [ReplaceI,refl] 1)) ]); |
|
245 |
||
120 | 246 |
(*Useful for coinduction proofs*) |
775 | 247 |
qed_goal "RepFun_eqI" ZF.thy |
0 | 248 |
"!!b a f. [| b=f(a); a : A |] ==> b : {f(x). x:A}" |
249 |
(fn _ => [ etac ssubst 1, etac RepFunI 1 ]); |
|
250 |
||
775 | 251 |
qed_goalw "RepFunE" ZF.thy [RepFun_def] |
0 | 252 |
"[| b : {f(x). x:A}; \ |
253 |
\ !!x.[| x:A; b=f(x) |] ==> P |] ==> \ |
|
254 |
\ P" |
|
255 |
(fn major::prems=> |
|
256 |
[ (rtac (major RS ReplaceE) 1), |
|
257 |
(REPEAT (ares_tac prems 1)) ]); |
|
258 |
||
2716 | 259 |
AddIs [RepFun_eqI]; |
2469 | 260 |
AddSEs [RepFunE]; |
261 |
||
775 | 262 |
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
|
263 |
"[| A=B; !!x. x:B ==> f(x)=g(x) |] ==> RepFun(A,f) = RepFun(B,g)" |
2469 | 264 |
(fn prems=> [ (simp_tac (!simpset addsimps prems) 1) ]); |
265 |
||
266 |
Addcongs [RepFun_cong]; |
|
0 | 267 |
|
775 | 268 |
qed_goalw "RepFun_iff" ZF.thy [Bex_def] |
485 | 269 |
"b : {f(x). x:A} <-> (EX x:A. b=f(x))" |
2469 | 270 |
(fn _ => [Fast_tac 1]); |
485 | 271 |
|
2469 | 272 |
goal ZF.thy "{x.x:A} = A"; |
2493 | 273 |
by (fast_tac (!claset) 1); |
2469 | 274 |
qed "triv_RepFun"; |
275 |
||
276 |
Addsimps [RepFun_iff, triv_RepFun]; |
|
0 | 277 |
|
278 |
(*** Rules for Collect -- forming a subset by separation ***) |
|
279 |
||
280 |
(*Separation is derivable from Replacement*) |
|
775 | 281 |
qed_goalw "separation" ZF.thy [Collect_def] |
0 | 282 |
"a : {x:A. P(x)} <-> a:A & P(a)" |
2469 | 283 |
(fn _=> [Fast_tac 1]); |
284 |
||
285 |
Addsimps [separation]; |
|
0 | 286 |
|
775 | 287 |
qed_goal "CollectI" ZF.thy |
2469 | 288 |
"!!P. [| a:A; P(a) |] ==> a : {x:A. P(x)}" |
289 |
(fn _=> [ Asm_simp_tac 1 ]); |
|
0 | 290 |
|
775 | 291 |
qed_goal "CollectE" ZF.thy |
0 | 292 |
"[| a : {x:A. P(x)}; [| a:A; P(a) |] ==> R |] ==> R" |
293 |
(fn prems=> |
|
294 |
[ (rtac (separation RS iffD1 RS conjE) 1), |
|
295 |
(REPEAT (ares_tac prems 1)) ]); |
|
296 |
||
2469 | 297 |
qed_goal "CollectD1" ZF.thy "!!P. a : {x:A. P(x)} ==> a:A" |
298 |
(fn _=> [ (etac CollectE 1), (assume_tac 1) ]); |
|
0 | 299 |
|
2469 | 300 |
qed_goal "CollectD2" ZF.thy "!!P. a : {x:A. P(x)} ==> P(a)" |
301 |
(fn _=> [ (etac CollectE 1), (assume_tac 1) ]); |
|
0 | 302 |
|
775 | 303 |
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
|
304 |
"[| A=B; !!x. x:B ==> P(x) <-> Q(x) |] ==> Collect(A,P) = Collect(B,Q)" |
2469 | 305 |
(fn prems=> [ (simp_tac (!simpset addsimps prems) 1) ]); |
306 |
||
307 |
AddSIs [CollectI]; |
|
308 |
AddSEs [CollectE]; |
|
309 |
Addcongs [Collect_cong]; |
|
0 | 310 |
|
311 |
(*** Rules for Unions ***) |
|
312 |
||
2469 | 313 |
Addsimps [Union_iff]; |
314 |
||
0 | 315 |
(*The order of the premises presupposes that C is rigid; A may be flexible*) |
2469 | 316 |
qed_goal "UnionI" ZF.thy "!!C. [| B: C; A: B |] ==> A: Union(C)" |
317 |
(fn _=> [ Simp_tac 1, Fast_tac 1 ]); |
|
0 | 318 |
|
775 | 319 |
qed_goal "UnionE" ZF.thy |
0 | 320 |
"[| A : Union(C); !!B.[| A: B; B: C |] ==> R |] ==> R" |
321 |
(fn prems=> |
|
485 | 322 |
[ (resolve_tac [Union_iff RS iffD1 RS bexE] 1), |
0 | 323 |
(REPEAT (ares_tac prems 1)) ]); |
324 |
||
325 |
(*** Rules for Unions of families ***) |
|
326 |
(* UN x:A. B(x) abbreviates Union({B(x). x:A}) *) |
|
327 |
||
775 | 328 |
qed_goalw "UN_iff" ZF.thy [Bex_def] |
485 | 329 |
"b : (UN x:A. B(x)) <-> (EX x:A. b : B(x))" |
2469 | 330 |
(fn _=> [ Simp_tac 1, Fast_tac 1 ]); |
331 |
||
332 |
Addsimps [UN_iff]; |
|
485 | 333 |
|
0 | 334 |
(*The order of the premises presupposes that A is rigid; b may be flexible*) |
2469 | 335 |
qed_goal "UN_I" ZF.thy "!!A B. [| a: A; b: B(a) |] ==> b: (UN x:A. B(x))" |
336 |
(fn _=> [ Simp_tac 1, Fast_tac 1 ]); |
|
0 | 337 |
|
775 | 338 |
qed_goal "UN_E" ZF.thy |
0 | 339 |
"[| b : (UN x:A. B(x)); !!x.[| x: A; b: B(x) |] ==> R |] ==> R" |
340 |
(fn major::prems=> |
|
341 |
[ (rtac (major RS UnionE) 1), |
|
342 |
(REPEAT (eresolve_tac (prems@[asm_rl, RepFunE, subst]) 1)) ]); |
|
343 |
||
775 | 344 |
qed_goal "UN_cong" ZF.thy |
435 | 345 |
"[| A=B; !!x. x:B ==> C(x)=D(x) |] ==> (UN x:A.C(x)) = (UN x:B.D(x))" |
2469 | 346 |
(fn prems=> [ (simp_tac (!simpset addsimps prems) 1) ]); |
347 |
||
348 |
(*No "Addcongs [UN_cong]" because UN is a combination of constants*) |
|
349 |
||
350 |
(* UN_E appears before UnionE so that it is tried first, to avoid expensive |
|
351 |
calls to hyp_subst_tac. Cannot include UN_I as it is unsafe: would enlarge |
|
352 |
the search space.*) |
|
353 |
AddIs [UnionI]; |
|
354 |
AddSEs [UN_E]; |
|
355 |
AddSEs [UnionE]; |
|
356 |
||
357 |
||
358 |
(*** Rules for Inter ***) |
|
359 |
||
360 |
(*Not obviously useful towards proving InterI, InterD, InterE*) |
|
361 |
qed_goalw "Inter_iff" ZF.thy [Inter_def,Ball_def] |
|
362 |
"A : Inter(C) <-> (ALL x:C. A: x) & (EX x. x:C)" |
|
363 |
(fn _=> [ Simp_tac 1, Fast_tac 1 ]); |
|
435 | 364 |
|
2469 | 365 |
(* Intersection is well-behaved only if the family is non-empty! *) |
2815
c05fa3ce5439
Improved intersection rule InterI: now truly safe, since the unsafeness is
paulson
parents:
2716
diff
changeset
|
366 |
qed_goal "InterI" ZF.thy |
c05fa3ce5439
Improved intersection rule InterI: now truly safe, since the unsafeness is
paulson
parents:
2716
diff
changeset
|
367 |
"[| !!x. x: C ==> A: x; EX c. c:C |] ==> A : Inter(C)" |
c05fa3ce5439
Improved intersection rule InterI: now truly safe, since the unsafeness is
paulson
parents:
2716
diff
changeset
|
368 |
(fn prems=> [ (simp_tac (!simpset addsimps [Inter_iff]) 1), |
c05fa3ce5439
Improved intersection rule InterI: now truly safe, since the unsafeness is
paulson
parents:
2716
diff
changeset
|
369 |
Cla.fast_tac (!claset addIs prems) 1 ]); |
2469 | 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 |
qed_goalw "InterD" ZF.thy [Inter_def] |
|
374 |
"!!C. [| A : Inter(C); B : C |] ==> A : B" |
|
375 |
(fn _=> [ Fast_tac 1 ]); |
|
376 |
||
377 |
(*"Classical" elimination rule -- does not require exhibiting B:C *) |
|
378 |
qed_goalw "InterE" ZF.thy [Inter_def] |
|
2716 | 379 |
"[| A : Inter(C); B~:C ==> R; A:B ==> R |] ==> R" |
2469 | 380 |
(fn major::prems=> |
381 |
[ (rtac (major RS CollectD2 RS ballE) 1), |
|
382 |
(REPEAT (eresolve_tac prems 1)) ]); |
|
383 |
||
384 |
AddSIs [InterI]; |
|
2716 | 385 |
AddEs [InterD, InterE]; |
0 | 386 |
|
387 |
(*** Rules for Intersections of families ***) |
|
388 |
(* INT x:A. B(x) abbreviates Inter({B(x). x:A}) *) |
|
389 |
||
2469 | 390 |
qed_goalw "INT_iff" ZF.thy [Inter_def] |
485 | 391 |
"b : (INT x:A. B(x)) <-> (ALL x:A. b : B(x)) & (EX x. x:A)" |
2469 | 392 |
(fn _=> [ Simp_tac 1, Best_tac 1 ]); |
485 | 393 |
|
775 | 394 |
qed_goal "INT_I" ZF.thy |
0 | 395 |
"[| !!x. x: A ==> b: B(x); a: A |] ==> b: (INT x:A. B(x))" |
2469 | 396 |
(fn prems=> [ fast_tac (!claset addIs prems) 1 ]); |
0 | 397 |
|
775 | 398 |
qed_goal "INT_E" ZF.thy |
0 | 399 |
"[| b : (INT x:A. B(x)); a: A |] ==> b : B(a)" |
400 |
(fn [major,minor]=> |
|
401 |
[ (rtac (major RS InterD) 1), |
|
402 |
(rtac (minor RS RepFunI) 1) ]); |
|
403 |
||
775 | 404 |
qed_goal "INT_cong" ZF.thy |
435 | 405 |
"[| A=B; !!x. x:B ==> C(x)=D(x) |] ==> (INT x:A.C(x)) = (INT x:B.D(x))" |
2469 | 406 |
(fn prems=> [ (simp_tac (!simpset addsimps prems) 1) ]); |
407 |
||
408 |
(*No "Addcongs [INT_cong]" because INT is a combination of constants*) |
|
435 | 409 |
|
0 | 410 |
|
411 |
(*** Rules for Powersets ***) |
|
412 |
||
775 | 413 |
qed_goal "PowI" ZF.thy "A <= B ==> A : Pow(B)" |
485 | 414 |
(fn [prem]=> [ (rtac (prem RS (Pow_iff RS iffD2)) 1) ]); |
0 | 415 |
|
775 | 416 |
qed_goal "PowD" ZF.thy "A : Pow(B) ==> A<=B" |
485 | 417 |
(fn [major]=> [ (rtac (major RS (Pow_iff RS iffD1)) 1) ]); |
0 | 418 |
|
2469 | 419 |
AddSIs [PowI]; |
420 |
AddSDs [PowD]; |
|
421 |
||
0 | 422 |
|
423 |
(*** Rules for the empty set ***) |
|
424 |
||
425 |
(*The set {x:0.False} is empty; by foundation it equals 0 |
|
426 |
See Suppes, page 21.*) |
|
2469 | 427 |
qed_goal "not_mem_empty" ZF.thy "a ~: 0" |
428 |
(fn _=> |
|
429 |
[ (cut_facts_tac [foundation] 1), |
|
430 |
(best_tac (!claset addDs [equalityD2]) 1) ]); |
|
431 |
||
432 |
bind_thm ("emptyE", not_mem_empty RS notE); |
|
433 |
||
434 |
Addsimps [not_mem_empty]; |
|
435 |
AddSEs [emptyE]; |
|
0 | 436 |
|
775 | 437 |
qed_goal "empty_subsetI" ZF.thy "0 <= A" |
2469 | 438 |
(fn _=> [ Fast_tac 1 ]); |
439 |
||
440 |
Addsimps [empty_subsetI]; |
|
441 |
AddSIs [empty_subsetI]; |
|
0 | 442 |
|
775 | 443 |
qed_goal "equals0I" ZF.thy "[| !!y. y:A ==> False |] ==> A=0" |
2493 | 444 |
(fn prems=> [ fast_tac (!claset addDs prems) 1 ]); |
0 | 445 |
|
2469 | 446 |
qed_goal "equals0D" ZF.thy "!!P. [| A=0; a:A |] ==> P" |
447 |
(fn _=> [ Full_simp_tac 1, Fast_tac 1 ]); |
|
0 | 448 |
|
825
76d9575950f2
Added Krzysztof's theorems subst_elem, not_emptyI, not_emptyE
lcp
parents:
775
diff
changeset
|
449 |
qed_goal "not_emptyI" ZF.thy "!!A a. a:A ==> A ~= 0" |
2469 | 450 |
(fn _=> [ Fast_tac 1 ]); |
825
76d9575950f2
Added Krzysztof's theorems subst_elem, not_emptyI, not_emptyE
lcp
parents:
775
diff
changeset
|
451 |
|
868
452f1e6ae3bc
Deleted semicolon at the end of the qed_goal line, which was preventing
lcp
parents:
854
diff
changeset
|
452 |
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
|
453 |
(fn [major,minor]=> |
76d9575950f2
Added Krzysztof's theorems subst_elem, not_emptyI, not_emptyE
lcp
parents:
775
diff
changeset
|
454 |
[ rtac ([major, equals0I] MRS swap) 1, |
76d9575950f2
Added Krzysztof's theorems subst_elem, not_emptyI, not_emptyE
lcp
parents:
775
diff
changeset
|
455 |
swap_res_tac [minor] 1, |
76d9575950f2
Added Krzysztof's theorems subst_elem, not_emptyI, not_emptyE
lcp
parents:
775
diff
changeset
|
456 |
assume_tac 1 ]); |
76d9575950f2
Added Krzysztof's theorems subst_elem, not_emptyI, not_emptyE
lcp
parents:
775
diff
changeset
|
457 |
|
0 | 458 |
|
748 | 459 |
(*** Cantor's Theorem: There is no surjection from a set to its powerset. ***) |
460 |
||
461 |
val cantor_cs = FOL_cs (*precisely the rules needed for the proof*) |
|
462 |
addSIs [ballI, CollectI, PowI, subsetI] addIs [bexI] |
|
463 |
addSEs [CollectE, equalityCE]; |
|
464 |
||
465 |
(*The search is undirected; similar proof attempts may fail. |
|
466 |
b represents ANY map, such as (lam x:A.b(x)): A->Pow(A). *) |
|
775 | 467 |
qed_goal "cantor" ZF.thy "EX S: Pow(A). ALL x:A. b(x) ~= S" |
2815
c05fa3ce5439
Improved intersection rule InterI: now truly safe, since the unsafeness is
paulson
parents:
2716
diff
changeset
|
468 |
(fn _ => [Cla.best_tac cantor_cs 1]); |
748 | 469 |
|
516 | 470 |
(*Lemma for the inductive definition in Zorn.thy*) |
775 | 471 |
qed_goal "Union_in_Pow" ZF.thy |
516 | 472 |
"!!Y. Y : Pow(Pow(A)) ==> Union(Y) : Pow(A)" |
2469 | 473 |
(fn _ => [Fast_tac 1]); |
1902
e349b91cf197
Added function for storing default claset in theory.
berghofe
parents:
1889
diff
changeset
|
474 |