author | paulson |
Wed, 28 Jun 2000 12:34:08 +0200 | |
changeset 9180 | 3bda56c0d70d |
parent 7531 | 99c7e60d6b3f |
child 9211 | 6236c5285bd8 |
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 |
||
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 |
||
775 | 18 |
qed_goalw "ballI" ZF.thy [Ball_def] |
0 | 19 |
"[| !!x. x:A ==> P(x) |] ==> ALL x:A. P(x)" |
20 |
(fn prems=> [ (REPEAT (ares_tac (prems @ [allI,impI]) 1)) ]); |
|
21 |
||
775 | 22 |
qed_goalw "bspec" ZF.thy [Ball_def] |
0 | 23 |
"[| ALL x:A. P(x); x: A |] ==> P(x)" |
24 |
(fn major::prems=> |
|
25 |
[ (rtac (major RS spec RS mp) 1), |
|
26 |
(resolve_tac prems 1) ]); |
|
27 |
||
775 | 28 |
qed_goalw "ballE" ZF.thy [Ball_def] |
37 | 29 |
"[| ALL x:A. P(x); P(x) ==> Q; x~:A ==> Q |] ==> Q" |
0 | 30 |
(fn major::prems=> |
31 |
[ (rtac (major RS allE) 1), |
|
32 |
(REPEAT (eresolve_tac (prems@[asm_rl,impCE]) 1)) ]); |
|
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*) |
|
775 | 60 |
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
|
61 |
"[| 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
|
62 |
(fn prems=> [ (simp_tac (FOL_ss addsimps prems) 1) ]); |
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 |
|
775 | 81 |
qed_goalw "bexE" ZF.thy [Bex_def] |
0 | 82 |
"[| EX x:A. P(x); !!x. [| x:A; P(x) |] ==> Q \ |
83 |
\ |] ==> Q" |
|
84 |
(fn major::prems=> |
|
85 |
[ (rtac (major RS exE) 1), |
|
86 |
(REPEAT (eresolve_tac (prems @ [asm_rl,conjE]) 1)) ]); |
|
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 |
|
775 | 97 |
qed_goalw "bex_cong" ZF.thy [Bex_def] |
0 | 98 |
"[| 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
|
99 |
\ |] ==> Bex(A,P) <-> Bex(A',P')" |
8ce8c4d13d4d
Installation of new simplifier for ZF. Deleted all congruence rules not
lcp
parents:
0
diff
changeset
|
100 |
(fn prems=> [ (simp_tac (FOL_ss addsimps prems addcongs [conj_cong]) 1) ]); |
0 | 101 |
|
2469 | 102 |
Addcongs [ball_cong, bex_cong]; |
103 |
||
104 |
||
0 | 105 |
(*** Rules for subsets ***) |
106 |
||
775 | 107 |
qed_goalw "subsetI" ZF.thy [subset_def] |
3840 | 108 |
"(!!x. x:A ==> x:B) ==> A <= B" |
0 | 109 |
(fn prems=> [ (REPEAT (ares_tac (prems @ [ballI]) 1)) ]); |
110 |
||
111 |
(*Rule in Modus Ponens style [was called subsetE] *) |
|
775 | 112 |
qed_goalw "subsetD" ZF.thy [subset_def] "[| A <= B; c:A |] ==> c:B" |
0 | 113 |
(fn major::prems=> |
114 |
[ (rtac (major RS bspec) 1), |
|
115 |
(resolve_tac prems 1) ]); |
|
116 |
||
117 |
(*Classical elimination rule*) |
|
775 | 118 |
qed_goalw "subsetCE" ZF.thy [subset_def] |
37 | 119 |
"[| A <= B; c~:A ==> P; c:B ==> P |] ==> P" |
0 | 120 |
(fn major::prems=> |
121 |
[ (rtac (major RS ballE) 1), |
|
122 |
(REPEAT (eresolve_tac prems 1)) ]); |
|
123 |
||
2469 | 124 |
AddSIs [subsetI]; |
125 |
AddEs [subsetCE, subsetD]; |
|
126 |
||
127 |
||
0 | 128 |
(*Takes assumptions A<=B; c:A and creates the assumption c:B *) |
129 |
val set_mp_tac = dtac subsetD THEN' assume_tac; |
|
130 |
||
131 |
(*Sometimes useful with premises in this order*) |
|
9180 | 132 |
Goal "[| c:A; A<=B |] ==> c:B"; |
133 |
by (Blast_tac 1); |
|
134 |
qed "rev_subsetD"; |
|
0 | 135 |
|
6111 | 136 |
(*Converts A<=B to x:A ==> x:B*) |
137 |
fun impOfSubs th = th RSN (2, rev_subsetD); |
|
138 |
||
9180 | 139 |
Goal "[| A <= B; c ~: B |] ==> c ~: A"; |
140 |
by (Blast_tac 1); |
|
141 |
qed "contra_subsetD"; |
|
1889 | 142 |
|
9180 | 143 |
Goal "[| c ~: B; A <= B |] ==> c ~: A"; |
144 |
by (Blast_tac 1); |
|
145 |
qed "rev_contra_subsetD"; |
|
1889 | 146 |
|
9180 | 147 |
Goal "A <= A"; |
148 |
by (Blast_tac 1); |
|
149 |
qed "subset_refl"; |
|
0 | 150 |
|
2469 | 151 |
Addsimps [subset_refl]; |
152 |
||
9180 | 153 |
Goal "[| A<=B; B<=C |] ==> A<=C"; |
154 |
by (Blast_tac 1); |
|
155 |
qed "subset_trans"; |
|
0 | 156 |
|
435 | 157 |
(*Useful for proving A<=B by rewriting in some cases*) |
775 | 158 |
qed_goalw "subset_iff" ZF.thy [subset_def,Ball_def] |
435 | 159 |
"A<=B <-> (ALL x. x:A --> x:B)" |
160 |
(fn _=> [ (rtac iff_refl 1) ]); |
|
161 |
||
0 | 162 |
|
163 |
(*** Rules for equality ***) |
|
164 |
||
165 |
(*Anti-symmetry of the subset relation*) |
|
9180 | 166 |
Goal "[| A <= B; B <= A |] ==> A = B"; |
167 |
by (REPEAT (ares_tac [conjI, extension RS iffD2] 1)) ; |
|
168 |
qed "equalityI"; |
|
0 | 169 |
|
2493 | 170 |
AddIs [equalityI]; |
171 |
||
9180 | 172 |
val [prem] = Goal "(!!x. x:A <-> x:B) ==> A = B"; |
173 |
by (rtac equalityI 1); |
|
174 |
by (REPEAT (ares_tac [subsetI, prem RS iffD1, prem RS iffD2] 1)) ; |
|
175 |
qed "equality_iffI"; |
|
0 | 176 |
|
2469 | 177 |
bind_thm ("equalityD1", extension RS iffD1 RS conjunct1); |
178 |
bind_thm ("equalityD2", extension RS iffD1 RS conjunct2); |
|
0 | 179 |
|
9180 | 180 |
val prems = Goal "[| A = B; [| A<=B; B<=A |] ==> P |] ==> P"; |
181 |
by (DEPTH_SOLVE (resolve_tac (prems@[equalityD1,equalityD2]) 1)) ; |
|
182 |
qed "equalityE"; |
|
0 | 183 |
|
9180 | 184 |
val major::prems= Goal |
185 |
"[| A = B; [| c:A; c:B |] ==> P; [| c~:A; c~:B |] ==> P |] ==> P"; |
|
186 |
by (rtac (major RS equalityE) 1); |
|
187 |
by (REPEAT (contr_tac 1 ORELSE eresolve_tac ([asm_rl,subsetCE]@prems) 1)) ; |
|
188 |
qed "equalityCE"; |
|
0 | 189 |
|
190 |
(*Lemma for creating induction formulae -- for "pattern matching" on p |
|
191 |
To make the induction hypotheses usable, apply "spec" or "bspec" to |
|
192 |
put universal quantifiers over the free variables in p. |
|
193 |
Would it be better to do subgoal_tac "ALL z. p = f(z) --> R(z)" ??*) |
|
9180 | 194 |
val prems = Goal "[| p: A; !!z. z: A ==> p=z --> R |] ==> R"; |
195 |
by (rtac mp 1); |
|
196 |
by (REPEAT (resolve_tac (refl::prems) 1)) ; |
|
197 |
qed "setup_induction"; |
|
0 | 198 |
|
199 |
||
200 |
(*** Rules for Replace -- the derived form of replacement ***) |
|
201 |
||
775 | 202 |
qed_goalw "Replace_iff" ZF.thy [Replace_def] |
0 | 203 |
"b : {y. x:A, P(x,y)} <-> (EX x:A. P(x,b) & (ALL y. P(x,y) --> y=b))" |
204 |
(fn _=> |
|
205 |
[ (rtac (replacement RS iff_trans) 1), |
|
206 |
(REPEAT (ares_tac [refl,bex_cong,iffI,ballI,allI,conjI,impI,ex1I] 1 |
|
207 |
ORELSE eresolve_tac [conjE, spec RS mp, ex1_functional] 1)) ]); |
|
208 |
||
209 |
(*Introduction; there must be a unique y such that P(x,y), namely y=b. *) |
|
9180 | 210 |
val prems = Goal |
485 | 211 |
"[| P(x,b); x: A; !!y. P(x,y) ==> y=b |] ==> \ |
9180 | 212 |
\ b : {y. x:A, P(x,y)}"; |
213 |
by (rtac (Replace_iff RS iffD2) 1); |
|
214 |
by (REPEAT (ares_tac (prems@[bexI,conjI,allI,impI]) 1)) ; |
|
215 |
qed "ReplaceI"; |
|
0 | 216 |
|
217 |
(*Elimination; may asssume there is a unique y such that P(x,y), namely y=b. *) |
|
9180 | 218 |
val prems = Goal |
0 | 219 |
"[| b : {y. x:A, P(x,y)}; \ |
220 |
\ !!x. [| x: A; P(x,b); ALL y. P(x,y)-->y=b |] ==> R \ |
|
9180 | 221 |
\ |] ==> R"; |
222 |
by (rtac (Replace_iff RS iffD1 RS bexE) 1); |
|
223 |
by (etac conjE 2); |
|
224 |
by (REPEAT (ares_tac prems 1)) ; |
|
225 |
qed "ReplaceE"; |
|
0 | 226 |
|
485 | 227 |
(*As above but without the (generally useless) 3rd assumption*) |
9180 | 228 |
val major::prems = Goal |
485 | 229 |
"[| b : {y. x:A, P(x,y)}; \ |
230 |
\ !!x. [| x: A; P(x,b) |] ==> R \ |
|
9180 | 231 |
\ |] ==> R"; |
232 |
by (rtac (major RS ReplaceE) 1); |
|
233 |
by (REPEAT (ares_tac prems 1)) ; |
|
234 |
qed "ReplaceE2"; |
|
485 | 235 |
|
2469 | 236 |
AddIs [ReplaceI]; |
237 |
AddSEs [ReplaceE2]; |
|
238 |
||
9180 | 239 |
val prems = Goal |
0 | 240 |
"[| A=B; !!x y. x:B ==> P(x,y) <-> Q(x,y) |] ==> \ |
9180 | 241 |
\ Replace(A,P) = Replace(B,Q)"; |
242 |
by (rtac equalityI 1); |
|
243 |
by (REPEAT |
|
244 |
(eresolve_tac ((prems RL [subst, ssubst])@[asm_rl, ReplaceE, spec RS mp]) 1 ORELSE resolve_tac [subsetI, ReplaceI] 1 |
|
245 |
ORELSE (resolve_tac (prems RL [iffD1,iffD2]) 1 THEN assume_tac 2))); |
|
246 |
qed "Replace_cong"; |
|
0 | 247 |
|
2469 | 248 |
Addcongs [Replace_cong]; |
249 |
||
0 | 250 |
(*** Rules for RepFun ***) |
251 |
||
775 | 252 |
qed_goalw "RepFunI" ZF.thy [RepFun_def] |
0 | 253 |
"!!a A. a : A ==> f(a) : {f(x). x:A}" |
254 |
(fn _ => [ (REPEAT (ares_tac [ReplaceI,refl] 1)) ]); |
|
255 |
||
120 | 256 |
(*Useful for coinduction proofs*) |
9180 | 257 |
Goal "[| b=f(a); a : A |] ==> b : {f(x). x:A}"; |
258 |
by (etac ssubst 1); |
|
259 |
by (etac RepFunI 1) ; |
|
260 |
qed "RepFun_eqI"; |
|
0 | 261 |
|
775 | 262 |
qed_goalw "RepFunE" ZF.thy [RepFun_def] |
0 | 263 |
"[| b : {f(x). x:A}; \ |
264 |
\ !!x.[| x:A; b=f(x) |] ==> P |] ==> \ |
|
265 |
\ P" |
|
266 |
(fn major::prems=> |
|
267 |
[ (rtac (major RS ReplaceE) 1), |
|
268 |
(REPEAT (ares_tac prems 1)) ]); |
|
269 |
||
2716 | 270 |
AddIs [RepFun_eqI]; |
2469 | 271 |
AddSEs [RepFunE]; |
272 |
||
775 | 273 |
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
|
274 |
"[| A=B; !!x. x:B ==> f(x)=g(x) |] ==> RepFun(A,f) = RepFun(B,g)" |
4091 | 275 |
(fn prems=> [ (simp_tac (simpset() addsimps prems) 1) ]); |
2469 | 276 |
|
277 |
Addcongs [RepFun_cong]; |
|
0 | 278 |
|
775 | 279 |
qed_goalw "RepFun_iff" ZF.thy [Bex_def] |
485 | 280 |
"b : {f(x). x:A} <-> (EX x:A. b=f(x))" |
9180 | 281 |
(fn _ => [(Blast_tac 1)]); |
485 | 282 |
|
5067 | 283 |
Goal "{x. x:A} = A"; |
2877 | 284 |
by (Blast_tac 1); |
2469 | 285 |
qed "triv_RepFun"; |
286 |
||
287 |
Addsimps [RepFun_iff, triv_RepFun]; |
|
0 | 288 |
|
289 |
(*** Rules for Collect -- forming a subset by separation ***) |
|
290 |
||
291 |
(*Separation is derivable from Replacement*) |
|
775 | 292 |
qed_goalw "separation" ZF.thy [Collect_def] |
0 | 293 |
"a : {x:A. P(x)} <-> a:A & P(a)" |
9180 | 294 |
(fn _=> [(Blast_tac 1)]); |
2469 | 295 |
|
296 |
Addsimps [separation]; |
|
0 | 297 |
|
9180 | 298 |
Goal "[| a:A; P(a) |] ==> a : {x:A. P(x)}"; |
299 |
by (Asm_simp_tac 1); |
|
300 |
qed "CollectI"; |
|
301 |
||
302 |
val prems = Goal |
|
303 |
"[| a : {x:A. P(x)}; [| a:A; P(a) |] ==> R |] ==> R"; |
|
304 |
by (rtac (separation RS iffD1 RS conjE) 1); |
|
305 |
by (REPEAT (ares_tac prems 1)) ; |
|
306 |
qed "CollectE"; |
|
0 | 307 |
|
9180 | 308 |
Goal "a : {x:A. P(x)} ==> a:A"; |
309 |
by (etac CollectE 1); |
|
310 |
by (assume_tac 1) ; |
|
311 |
qed "CollectD1"; |
|
0 | 312 |
|
9180 | 313 |
Goal "a : {x:A. P(x)} ==> P(a)"; |
314 |
by (etac CollectE 1); |
|
315 |
by (assume_tac 1) ; |
|
316 |
qed "CollectD2"; |
|
0 | 317 |
|
775 | 318 |
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
|
319 |
"[| A=B; !!x. x:B ==> P(x) <-> Q(x) |] ==> Collect(A,P) = Collect(B,Q)" |
4091 | 320 |
(fn prems=> [ (simp_tac (simpset() addsimps prems) 1) ]); |
2469 | 321 |
|
322 |
AddSIs [CollectI]; |
|
323 |
AddSEs [CollectE]; |
|
324 |
Addcongs [Collect_cong]; |
|
0 | 325 |
|
326 |
(*** Rules for Unions ***) |
|
327 |
||
2469 | 328 |
Addsimps [Union_iff]; |
329 |
||
0 | 330 |
(*The order of the premises presupposes that C is rigid; A may be flexible*) |
9180 | 331 |
Goal "[| B: C; A: B |] ==> A: Union(C)"; |
332 |
by (Simp_tac 1); |
|
333 |
by (Blast_tac 1) ; |
|
334 |
qed "UnionI"; |
|
0 | 335 |
|
9180 | 336 |
val prems = Goal "[| A : Union(C); !!B.[| A: B; B: C |] ==> R |] ==> R"; |
337 |
by (resolve_tac [Union_iff RS iffD1 RS bexE] 1); |
|
338 |
by (REPEAT (ares_tac prems 1)) ; |
|
339 |
qed "UnionE"; |
|
0 | 340 |
|
341 |
(*** Rules for Unions of families ***) |
|
342 |
(* UN x:A. B(x) abbreviates Union({B(x). x:A}) *) |
|
343 |
||
775 | 344 |
qed_goalw "UN_iff" ZF.thy [Bex_def] |
485 | 345 |
"b : (UN x:A. B(x)) <-> (EX x:A. b : B(x))" |
2877 | 346 |
(fn _=> [ Simp_tac 1, Blast_tac 1 ]); |
2469 | 347 |
|
348 |
Addsimps [UN_iff]; |
|
485 | 349 |
|
0 | 350 |
(*The order of the premises presupposes that A is rigid; b may be flexible*) |
9180 | 351 |
Goal "[| a: A; b: B(a) |] ==> b: (UN x:A. B(x))"; |
352 |
by (Simp_tac 1); |
|
353 |
by (Blast_tac 1) ; |
|
354 |
qed "UN_I"; |
|
0 | 355 |
|
9180 | 356 |
val major::prems= Goal |
357 |
"[| b : (UN x:A. B(x)); !!x.[| x: A; b: B(x) |] ==> R |] ==> R"; |
|
358 |
by (rtac (major RS UnionE) 1); |
|
359 |
by (REPEAT (eresolve_tac (prems@[asm_rl, RepFunE, subst]) 1)) ; |
|
360 |
qed "UN_E"; |
|
0 | 361 |
|
9180 | 362 |
val prems = Goal |
363 |
"[| A=B; !!x. x:B ==> C(x)=D(x) |] ==> (UN x:A. C(x)) = (UN x:B. D(x))"; |
|
364 |
by (simp_tac (simpset() addsimps prems) 1) ; |
|
365 |
qed "UN_cong"; |
|
2469 | 366 |
|
367 |
(*No "Addcongs [UN_cong]" because UN is a combination of constants*) |
|
368 |
||
369 |
(* UN_E appears before UnionE so that it is tried first, to avoid expensive |
|
370 |
calls to hyp_subst_tac. Cannot include UN_I as it is unsafe: would enlarge |
|
371 |
the search space.*) |
|
372 |
AddIs [UnionI]; |
|
373 |
AddSEs [UN_E]; |
|
374 |
AddSEs [UnionE]; |
|
375 |
||
376 |
||
377 |
(*** Rules for Inter ***) |
|
378 |
||
379 |
(*Not obviously useful towards proving InterI, InterD, InterE*) |
|
380 |
qed_goalw "Inter_iff" ZF.thy [Inter_def,Ball_def] |
|
381 |
"A : Inter(C) <-> (ALL x:C. A: x) & (EX x. x:C)" |
|
2877 | 382 |
(fn _=> [ Simp_tac 1, Blast_tac 1 ]); |
435 | 383 |
|
2469 | 384 |
(* Intersection is well-behaved only if the family is non-empty! *) |
9180 | 385 |
val prems = Goal |
386 |
"[| !!x. x: C ==> A: x; EX c. c:C |] ==> A : Inter(C)"; |
|
387 |
by (simp_tac (simpset() addsimps [Inter_iff]) 1); |
|
388 |
by (blast_tac (claset() addIs prems) 1) ; |
|
389 |
qed "InterI"; |
|
2469 | 390 |
|
391 |
(*A "destruct" rule -- every B in C contains A as an element, but |
|
392 |
A:B can hold when B:C does not! This rule is analogous to "spec". *) |
|
393 |
qed_goalw "InterD" ZF.thy [Inter_def] |
|
394 |
"!!C. [| A : Inter(C); B : C |] ==> A : B" |
|
9180 | 395 |
(fn _=> [(Blast_tac 1)]); |
2469 | 396 |
|
397 |
(*"Classical" elimination rule -- does not require exhibiting B:C *) |
|
398 |
qed_goalw "InterE" ZF.thy [Inter_def] |
|
2716 | 399 |
"[| A : Inter(C); B~:C ==> R; A:B ==> R |] ==> R" |
2469 | 400 |
(fn major::prems=> |
401 |
[ (rtac (major RS CollectD2 RS ballE) 1), |
|
402 |
(REPEAT (eresolve_tac prems 1)) ]); |
|
403 |
||
404 |
AddSIs [InterI]; |
|
2716 | 405 |
AddEs [InterD, InterE]; |
0 | 406 |
|
407 |
(*** Rules for Intersections of families ***) |
|
408 |
(* INT x:A. B(x) abbreviates Inter({B(x). x:A}) *) |
|
409 |
||
2469 | 410 |
qed_goalw "INT_iff" ZF.thy [Inter_def] |
485 | 411 |
"b : (INT x:A. B(x)) <-> (ALL x:A. b : B(x)) & (EX x. x:A)" |
2469 | 412 |
(fn _=> [ Simp_tac 1, Best_tac 1 ]); |
485 | 413 |
|
9180 | 414 |
val prems = Goal |
415 |
"[| !!x. x: A ==> b: B(x); a: A |] ==> b: (INT x:A. B(x))"; |
|
416 |
by (blast_tac (claset() addIs prems) 1); |
|
417 |
qed "INT_I"; |
|
0 | 418 |
|
9180 | 419 |
Goal "[| b : (INT x:A. B(x)); a: A |] ==> b : B(a)"; |
420 |
by (Blast_tac 1); |
|
421 |
qed "INT_E"; |
|
0 | 422 |
|
9180 | 423 |
val prems = Goal |
424 |
"[| A=B; !!x. x:B ==> C(x)=D(x) |] ==> (INT x:A. C(x)) = (INT x:B. D(x))"; |
|
425 |
by (simp_tac (simpset() addsimps prems) 1) ; |
|
426 |
qed "INT_cong"; |
|
2469 | 427 |
|
428 |
(*No "Addcongs [INT_cong]" because INT is a combination of constants*) |
|
435 | 429 |
|
0 | 430 |
|
431 |
(*** Rules for Powersets ***) |
|
432 |
||
9180 | 433 |
Goal "A <= B ==> A : Pow(B)"; |
434 |
by (etac (Pow_iff RS iffD2) 1) ; |
|
435 |
qed "PowI"; |
|
0 | 436 |
|
9180 | 437 |
Goal "A : Pow(B) ==> A<=B"; |
438 |
by (etac (Pow_iff RS iffD1) 1) ; |
|
439 |
qed "PowD"; |
|
0 | 440 |
|
2469 | 441 |
AddSIs [PowI]; |
442 |
AddSDs [PowD]; |
|
443 |
||
0 | 444 |
|
445 |
(*** Rules for the empty set ***) |
|
446 |
||
447 |
(*The set {x:0.False} is empty; by foundation it equals 0 |
|
448 |
See Suppes, page 21.*) |
|
9180 | 449 |
Goal "a ~: 0"; |
450 |
by (cut_facts_tac [foundation] 1); |
|
451 |
by (best_tac (claset() addDs [equalityD2]) 1) ; |
|
452 |
qed "not_mem_empty"; |
|
2469 | 453 |
|
454 |
bind_thm ("emptyE", not_mem_empty RS notE); |
|
455 |
||
456 |
Addsimps [not_mem_empty]; |
|
457 |
AddSEs [emptyE]; |
|
0 | 458 |
|
9180 | 459 |
Goal "0 <= A"; |
460 |
by (Blast_tac 1); |
|
461 |
qed "empty_subsetI"; |
|
2469 | 462 |
|
463 |
Addsimps [empty_subsetI]; |
|
0 | 464 |
|
9180 | 465 |
val prems = Goal "[| !!y. y:A ==> False |] ==> A=0"; |
466 |
by (blast_tac (claset() addDs prems) 1) ; |
|
467 |
qed "equals0I"; |
|
0 | 468 |
|
9180 | 469 |
Goal "A=0 ==> a ~: A"; |
470 |
by (Blast_tac 1); |
|
471 |
qed "equals0D"; |
|
0 | 472 |
|
5467 | 473 |
AddDs [equals0D, sym RS equals0D]; |
5265
9d1d4c43c76d
Disjointness reasoning by AddEs [equals0E, sym RS equals0E]
paulson
parents:
5242
diff
changeset
|
474 |
|
9180 | 475 |
Goal "a:A ==> A ~= 0"; |
476 |
by (Blast_tac 1); |
|
477 |
qed "not_emptyI"; |
|
825
76d9575950f2
Added Krzysztof's theorems subst_elem, not_emptyI, not_emptyE
lcp
parents:
775
diff
changeset
|
478 |
|
9180 | 479 |
val [major,minor]= Goal "[| A ~= 0; !!x. x:A ==> R |] ==> R"; |
480 |
by (rtac ([major, equals0I] MRS swap) 1); |
|
481 |
by (swap_res_tac [minor] 1); |
|
482 |
by (assume_tac 1) ; |
|
483 |
qed "not_emptyE"; |
|
825
76d9575950f2
Added Krzysztof's theorems subst_elem, not_emptyI, not_emptyE
lcp
parents:
775
diff
changeset
|
484 |
|
0 | 485 |
|
748 | 486 |
(*** Cantor's Theorem: There is no surjection from a set to its powerset. ***) |
487 |
||
488 |
val cantor_cs = FOL_cs (*precisely the rules needed for the proof*) |
|
489 |
addSIs [ballI, CollectI, PowI, subsetI] addIs [bexI] |
|
490 |
addSEs [CollectE, equalityCE]; |
|
491 |
||
492 |
(*The search is undirected; similar proof attempts may fail. |
|
493 |
b represents ANY map, such as (lam x:A.b(x)): A->Pow(A). *) |
|
9180 | 494 |
Goal "EX S: Pow(A). ALL x:A. b(x) ~= S"; |
495 |
by (best_tac cantor_cs 1); |
|
496 |
qed "cantor"; |
|
748 | 497 |
|
516 | 498 |
(*Lemma for the inductive definition in Zorn.thy*) |
9180 | 499 |
Goal "Y : Pow(Pow(A)) ==> Union(Y) : Pow(A)"; |
500 |
by (Blast_tac 1); |
|
501 |
qed "Union_in_Pow"; |
|
1902
e349b91cf197
Added function for storing default claset in theory.
berghofe
parents:
1889
diff
changeset
|
502 |
|
6111 | 503 |
|
504 |
local |
|
505 |
val (bspecT, bspec') = make_new_spec bspec |
|
506 |
in |
|
507 |
||
508 |
fun RSbspec th = |
|
509 |
(case concl_of th of |
|
510 |
_ $ (Const("Ball",_) $ _ $ Abs(a,_,_)) => |
|
511 |
let val ca = cterm_of (#sign(rep_thm th)) (Var((a,0),bspecT)) |
|
512 |
in th RS forall_elim ca bspec' end |
|
513 |
| _ => raise THM("RSbspec",0,[th])); |
|
514 |
||
515 |
val normalize_thm_ZF = normalize_thm [RSspec,RSbspec,RSmp]; |
|
516 |
||
517 |
fun qed_spec_mp name = |
|
518 |
let val thm = normalize_thm_ZF (result()) |
|
519 |
in bind_thm(name, thm) end; |
|
520 |
||
521 |
fun qed_goal_spec_mp name thy s p = |
|
522 |
bind_thm (name, normalize_thm_ZF (prove_goal thy s p)); |
|
523 |
||
524 |
fun qed_goalw_spec_mp name thy defs s p = |
|
525 |
bind_thm (name, normalize_thm_ZF (prove_goalw thy defs s p)); |
|
526 |
||
527 |
end; |
|
528 |
||
529 |
||
530 |
(* attributes *) |
|
531 |
||
532 |
local |
|
533 |
||
534 |
fun gen_rulify x = |
|
535 |
Attrib.no_args (Drule.rule_attribute (K (normalize_thm_ZF))) x; |
|
536 |
||
537 |
in |
|
538 |
||
539 |
val attrib_setup = |
|
540 |
[Attrib.add_attributes |
|
541 |
[("rulify", (gen_rulify, gen_rulify), |
|
542 |
"put theorem into standard rule form")]]; |
|
543 |
||
544 |
end; |