author | paulson |
Wed, 21 Aug 1996 11:43:37 +0200 | |
changeset 1932 | cc9f1ba8f29a |
parent 1924 | 0f1a583457da |
child 2469 | b50b8c0eec01 |
permissions | -rw-r--r-- |
1461 | 1 |
(* Title: ZF/AC/DC.ML |
2 |
ID: $Id$ |
|
3 |
Author: Krzysztof Grabczewski |
|
1196 | 4 |
|
5 |
The proofs concerning the Axiom of Dependent Choice |
|
6 |
*) |
|
7 |
||
8 |
open DC; |
|
9 |
||
10 |
(* ********************************************************************** *) |
|
1461 | 11 |
(* DC ==> DC(omega) *) |
12 |
(* *) |
|
13 |
(* The scheme of the proof: *) |
|
14 |
(* *) |
|
15 |
(* Assume DC. Let R and x satisfy the premise of DC(omega). *) |
|
16 |
(* *) |
|
17 |
(* Define XX and RR as follows: *) |
|
18 |
(* *) |
|
19 |
(* XX = (UN n:nat. {f:n->X. ALL k:n. <f``k, f`k> : R}) *) |
|
20 |
(* f RR g iff domain(g)=succ(domain(f)) & *) |
|
21 |
(* restrict(g, domain(f)) = f *) |
|
22 |
(* *) |
|
23 |
(* Then RR satisfies the hypotheses of DC. *) |
|
24 |
(* So applying DC: *) |
|
25 |
(* *) |
|
26 |
(* EX f:nat->XX. ALL n:nat. f`n RR f`succ(n) *) |
|
27 |
(* *) |
|
28 |
(* Thence *) |
|
29 |
(* *) |
|
30 |
(* ff = {<n, f`succ(n)`n>. n:nat} *) |
|
31 |
(* *) |
|
32 |
(* is the desired function. *) |
|
33 |
(* *) |
|
1196 | 34 |
(* ********************************************************************** *) |
35 |
||
36 |
goal thy "{z:XX*XX. domain(snd(z))=succ(domain(fst(z))) \ |
|
1461 | 37 |
\ & restrict(snd(z), domain(fst(z))) = fst(z)} <= XX*XX"; |
1196 | 38 |
by (fast_tac AC_cs 1); |
39 |
val lemma1_1 = result(); |
|
40 |
||
41 |
goal thy "!!X. ALL Y:Pow(X). Y lesspoll nat --> (EX x:X. <Y, x> : R) \ |
|
1461 | 42 |
\ ==> {z: (UN n:nat. {f:n->X. ALL k:n. <f``k, f`k> : R}) * \ |
43 |
\ (UN n:nat. {f:n->X. ALL k:n. <f``k, f`k> : R}). \ |
|
44 |
\ domain(snd(z))=succ(domain(fst(z))) \ |
|
45 |
\ & restrict(snd(z), domain(fst(z))) = fst(z)} ~= 0"; |
|
1207 | 46 |
by (etac ballE 1); |
1196 | 47 |
by (eresolve_tac [empty_subsetI RS PowI RSN (2, notE)] 2); |
48 |
by (eresolve_tac [nat_0I RS n_lesspoll_nat RSN (2, impE)] 1); |
|
1207 | 49 |
by (etac bexE 1); |
1196 | 50 |
by (res_inst_tac [("a","<0, {<0, x>}>")] not_emptyI 1); |
1207 | 51 |
by (rtac CollectI 1); |
52 |
by (rtac SigmaI 1); |
|
1196 | 53 |
by (fast_tac (AC_cs addSIs [nat_0I RS UN_I, empty_fun]) 1); |
54 |
by (fast_tac (AC_cs addSIs [nat_1I RS UN_I, singleton_fun RS Pi_type] |
|
1461 | 55 |
addss (AC_ss addsimps [[lepoll_refl, succI1] MRS lepoll_1_is_sing, |
56 |
apply_singleton_eq, image_0])) 1); |
|
1924
0f1a583457da
Corrected for new classical reasoner: redundant rules
paulson
parents:
1461
diff
changeset
|
57 |
by (asm_full_simp_tac (AC_ss addsimps [domain_0, restrict_0, domain_cons, |
1461 | 58 |
[lepoll_refl, succI1] MRS lepoll_1_is_sing]) 1); |
1196 | 59 |
val lemma1_2 = result(); |
60 |
||
61 |
goal thy "!!X. ALL Y:Pow(X). Y lesspoll nat --> (EX x:X. <Y, x> : R) \ |
|
1461 | 62 |
\ ==> range({z: (UN n:nat. {f:n->X. ALL k:n. <f``k, f`k> : R}) * \ |
63 |
\ (UN n:nat. {f:n->X. ALL k:n. <f``k, f`k> : R}). \ |
|
64 |
\ domain(snd(z))=succ(domain(fst(z))) \ |
|
65 |
\ & restrict(snd(z), domain(fst(z))) = fst(z)}) \ |
|
66 |
\ <= domain({z: (UN n:nat. {f:n->X. ALL k:n. <f``k, f`k> : R}) * \ |
|
67 |
\ (UN n:nat. {f:n->X. ALL k:n. <f``k, f`k> : R}). \ |
|
68 |
\ domain(snd(z))=succ(domain(fst(z))) \ |
|
69 |
\ & restrict(snd(z), domain(fst(z))) = fst(z)})"; |
|
1207 | 70 |
by (rtac range_subset_domain 1); |
71 |
by (rtac subsetI 2); |
|
72 |
by (etac CollectD1 2); |
|
73 |
by (etac UN_E 1); |
|
74 |
by (etac CollectE 1); |
|
1196 | 75 |
by (dresolve_tac [fun_is_rel RS image_subset RS PowI RSN (2, bspec)] 1 |
1461 | 76 |
THEN (assume_tac 1)); |
1196 | 77 |
by (eresolve_tac [[n_lesspoll_nat, nat_into_Ord RSN (2, image_Ord_lepoll)] |
1461 | 78 |
MRS lepoll_lesspoll_lesspoll RSN (2, impE)] 1 |
79 |
THEN REPEAT (assume_tac 1)); |
|
1207 | 80 |
by (etac bexE 1); |
1196 | 81 |
by (res_inst_tac [("x","cons(<n,x>, g)")] exI 1); |
1207 | 82 |
by (rtac CollectI 1); |
83 |
by (rtac SigmaI 1); |
|
1196 | 84 |
by (fast_tac AC_cs 1); |
1207 | 85 |
by (rtac UN_I 1); |
86 |
by (etac nat_succI 1); |
|
87 |
by (rtac CollectI 1); |
|
88 |
by (etac cons_fun_type2 1 THEN (assume_tac 1)); |
|
1196 | 89 |
by (fast_tac (AC_cs addSEs [succE] addss (AC_ss |
1461 | 90 |
addsimps [cons_image_n, cons_val_n, cons_image_k, cons_val_k])) 1); |
1196 | 91 |
by (asm_full_simp_tac (AC_ss |
1461 | 92 |
addsimps [domain_cons, domain_of_fun, succ_def, restrict_cons_eq]) 1); |
1196 | 93 |
val lemma1_3 = result(); |
94 |
||
95 |
goal thy "!!X. [| XX = (UN n:nat. {f:n->X. ALL k:n. <f``k, f`k> : R}); \ |
|
1461 | 96 |
\ RR = {z:XX*XX. domain(snd(z))=succ(domain(fst(z))) \ |
97 |
\ & restrict(snd(z), domain(fst(z))) = fst(z)}; \ |
|
98 |
\ ALL Y:Pow(X). Y lesspoll nat --> (EX x:X. <Y, x> : R) \ |
|
99 |
\ |] ==> RR <= XX*XX & RR ~= 0 & range(RR) <= domain(RR)"; |
|
1196 | 100 |
by (fast_tac (AC_cs addSIs [lemma1_1] addSEs [lemma1_2, lemma1_3]) 1); |
101 |
val lemma1 = result(); |
|
102 |
||
103 |
goal thy "!!f. [| <f,g> : {z:XX*XX. \ |
|
1461 | 104 |
\ domain(snd(z))=succ(domain(fst(z))) & Q(z)}; \ |
105 |
\ XX = (UN n:nat. {f:n->X. ALL k:n. <f``k, f`k> : R}); f:k->X \ |
|
106 |
\ |] ==> g:succ(k)->X"; |
|
1207 | 107 |
by (etac CollectE 1); |
108 |
by (dtac SigmaD2 1); |
|
1196 | 109 |
by (hyp_subst_tac 1); |
1207 | 110 |
by (etac UN_E 1); |
111 |
by (etac CollectE 1); |
|
1196 | 112 |
by (asm_full_simp_tac AC_ss 1); |
1207 | 113 |
by (dtac domain_of_fun 1); |
114 |
by (etac conjE 1); |
|
1196 | 115 |
by (forward_tac [domain_of_fun RS sym RS trans] 1 THEN (assume_tac 1)); |
116 |
by (fast_tac AC_cs 1); |
|
117 |
val lemma2_1 = result(); |
|
118 |
||
119 |
goal thy "!!X. [| XX = (UN n:nat. {f:n->X. ALL k:n. <f``k, f`k> : R}); \ |
|
1461 | 120 |
\ ALL n:nat. <f`n, f`succ(n)> : \ |
121 |
\ {z:XX*XX. domain(snd(z))=succ(domain(fst(z))) \ |
|
122 |
\ & restrict(snd(z), domain(fst(z))) = fst(z)}; \ |
|
123 |
\ f: nat -> XX; n:nat \ |
|
124 |
\ |] ==> EX k:nat. f`succ(n) : k -> X & n:k \ |
|
125 |
\ & <f`succ(n)``n, f`succ(n)`n> : R"; |
|
1207 | 126 |
by (etac nat_induct 1); |
1196 | 127 |
by (dresolve_tac [nat_1I RSN (2, apply_type)] 1); |
128 |
by (dresolve_tac [nat_0I RSN (2, bspec)] 1); |
|
129 |
by (asm_full_simp_tac AC_ss 1); |
|
1207 | 130 |
by (etac UN_E 1); |
131 |
by (etac CollectE 1); |
|
132 |
by (rtac bexI 1 THEN (assume_tac 2)); |
|
1196 | 133 |
by (fast_tac (AC_cs addSEs [nat_0_le RS leE, ltD, ltD RSN (2, bspec)] |
1461 | 134 |
addEs [sym RS trans RS succ_neq_0, domain_of_fun]) 1); |
1207 | 135 |
by (etac bexE 1); |
1196 | 136 |
by (dresolve_tac [nat_succI RSN (2, bspec)] 1 THEN (assume_tac 1)); |
1207 | 137 |
by (etac conjE 1); |
138 |
by (dtac lemma2_1 1 THEN REPEAT (assume_tac 1)); |
|
1196 | 139 |
by (hyp_subst_tac 1); |
140 |
by (dresolve_tac [nat_succI RS nat_succI RSN (2, apply_type)] 1 |
|
1461 | 141 |
THEN (assume_tac 1)); |
1207 | 142 |
by (etac UN_E 1); |
143 |
by (etac CollectE 1); |
|
1196 | 144 |
by (dresolve_tac [[domain_of_fun RS sym, domain_of_fun] MRS trans] 1 |
1461 | 145 |
THEN (assume_tac 1)); |
1196 | 146 |
by (fast_tac (AC_cs addSEs [nat_succI, nat_into_Ord RS succ_in_succ] |
1461 | 147 |
addSDs [nat_into_Ord RS succ_in_succ RSN (2, bspec)]) 1); |
1196 | 148 |
val lemma2 = result(); |
149 |
||
150 |
goal thy "!!X. [| XX = (UN n:nat. {f:n->X. ALL k:n. <f``k, f`k> : R}); \ |
|
1461 | 151 |
\ ALL n:nat. <f`n, f`succ(n)> : \ |
152 |
\ {z:XX*XX. domain(snd(z))=succ(domain(fst(z))) \ |
|
153 |
\ & restrict(snd(z), domain(fst(z))) = fst(z)}; \ |
|
154 |
\ f: nat -> XX; n:nat \ |
|
155 |
\ |] ==> ALL x:n. f`succ(n)`x = f`succ(x)`x"; |
|
1207 | 156 |
by (etac nat_induct 1); |
1196 | 157 |
by (fast_tac AC_cs 1); |
1207 | 158 |
by (rtac ballI 1); |
159 |
by (etac succE 1); |
|
160 |
by (rtac restrict_eq_imp_val_eq 1); |
|
1196 | 161 |
by (dresolve_tac [nat_succI RSN (2, bspec)] 1 THEN (assume_tac 1)); |
162 |
by (asm_full_simp_tac AC_ss 1); |
|
1207 | 163 |
by (dtac lemma2 1 THEN REPEAT (assume_tac 1)); |
1196 | 164 |
by (fast_tac (AC_cs addSDs [domain_of_fun]) 1); |
165 |
by (dres_inst_tac [("x","xa")] bspec 1 THEN (assume_tac 1)); |
|
166 |
by (eresolve_tac [sym RS trans RS sym] 1); |
|
167 |
by (resolve_tac [restrict_eq_imp_val_eq RS sym] 1); |
|
168 |
by (dresolve_tac [nat_succI RSN (2, bspec)] 1 THEN (assume_tac 1)); |
|
169 |
by (asm_full_simp_tac AC_ss 1); |
|
1207 | 170 |
by (dtac lemma2 1 THEN REPEAT (assume_tac 1)); |
1196 | 171 |
by (fast_tac (FOL_cs addSDs [domain_of_fun] |
1461 | 172 |
addSEs [bexE, nat_into_Ord RSN (2, OrdmemD) RS subsetD]) 1); |
1196 | 173 |
val lemma3_1 = result(); |
174 |
||
175 |
goal thy "!!n. ALL x:n. f`succ(n)`x = f`succ(x)`x \ |
|
1461 | 176 |
\ ==> {f`succ(x)`x. x:n} = {f`succ(n)`x. x:n}"; |
1196 | 177 |
by (asm_full_simp_tac AC_ss 1); |
178 |
val lemma3_2 = result(); |
|
179 |
||
180 |
goal thy "!!X. [| XX = (UN n:nat. {f:n->X. ALL k:n. <f``k, f`k> : R}); \ |
|
1461 | 181 |
\ ALL n:nat. <f`n, f`succ(n)> : \ |
182 |
\ {z:XX*XX. domain(snd(z))=succ(domain(fst(z))) \ |
|
183 |
\ & restrict(snd(z), domain(fst(z))) = fst(z)}; \ |
|
184 |
\ f: nat -> XX; n:nat \ |
|
185 |
\ |] ==> (lam x:nat. f`succ(x)`x) `` n = f`succ(n)``n"; |
|
1207 | 186 |
by (etac natE 1); |
1196 | 187 |
by (asm_full_simp_tac (AC_ss addsimps [image_0]) 1); |
188 |
by (resolve_tac [image_lam RS ssubst] 1); |
|
189 |
by (fast_tac (AC_cs addSEs [[nat_succI, Ord_nat] MRS OrdmemD]) 1); |
|
190 |
by (resolve_tac [lemma3_1 RS lemma3_2 RS ssubst] 1 |
|
1461 | 191 |
THEN REPEAT (assume_tac 1)); |
1196 | 192 |
by (fast_tac (AC_cs addSEs [nat_succI]) 1); |
193 |
by (dresolve_tac [nat_succI RSN (4, lemma2)] 1 |
|
1461 | 194 |
THEN REPEAT (assume_tac 1)); |
1924
0f1a583457da
Corrected for new classical reasoner: redundant rules
paulson
parents:
1461
diff
changeset
|
195 |
by (fast_tac (AC_cs addSEs [nat_into_Ord RSN (2, OrdmemD) RSN |
0f1a583457da
Corrected for new classical reasoner: redundant rules
paulson
parents:
1461
diff
changeset
|
196 |
(2, image_fun RS sym)]) 1); |
1196 | 197 |
val lemma3 = result(); |
198 |
||
199 |
goal thy "!!f. [| f:A->B; B<=C |] ==> f:A->C"; |
|
1207 | 200 |
by (rtac Pi_type 1 THEN (assume_tac 1)); |
1196 | 201 |
by (fast_tac (AC_cs addSEs [apply_type]) 1); |
202 |
val fun_type_gen = result(); |
|
203 |
||
204 |
goalw thy [DC_def, DC0_def] "!!Z. DC0 ==> DC(nat)"; |
|
205 |
by (REPEAT (resolve_tac [allI, impI] 1)); |
|
206 |
by (REPEAT (eresolve_tac [conjE, allE] 1)); |
|
207 |
by (eresolve_tac [[refl, refl] MRS lemma1 RSN (2, impE)] 1 |
|
1461 | 208 |
THEN (assume_tac 1)); |
1207 | 209 |
by (etac bexE 1); |
1196 | 210 |
by (res_inst_tac [("x","lam n:nat. f`succ(n)`n")] bexI 1); |
211 |
by (fast_tac (AC_cs addSIs [lam_type] addSDs [refl RS lemma2] |
|
1461 | 212 |
addSEs [fun_type_gen, apply_type]) 2); |
1207 | 213 |
by (rtac oallI 1); |
1196 | 214 |
by (forward_tac [ltD RSN (3, refl RS lemma2)] 1 |
1461 | 215 |
THEN assume_tac 2); |
1196 | 216 |
by (fast_tac (AC_cs addSEs [fun_type_gen]) 1); |
217 |
by (eresolve_tac [ltD RSN (3, refl RS lemma3) RS ssubst] 1 |
|
1461 | 218 |
THEN assume_tac 2); |
1196 | 219 |
by (fast_tac (AC_cs addSEs [fun_type_gen]) 1); |
220 |
by (fast_tac (AC_cs addss AC_ss) 1); |
|
221 |
qed "DC0_DC_nat"; |
|
222 |
||
223 |
(* ********************************************************************** *) |
|
1461 | 224 |
(* DC(omega) ==> DC *) |
225 |
(* *) |
|
226 |
(* The scheme of the proof: *) |
|
227 |
(* *) |
|
228 |
(* Assume DC(omega). Let R and x satisfy the premise of DC. *) |
|
229 |
(* *) |
|
230 |
(* Define XX and RR as follows: *) |
|
231 |
(* *) |
|
232 |
(* XX = (UN n:nat. *) |
|
233 |
(* {f:succ(n)->domain(R). ALL k:n. <f`k, f`succ(k)> : R}) *) |
|
234 |
(* RR = {z:Fin(XX)*XX. (domain(snd(z))=succ(UN f:fst(z). domain(f)) *) |
|
235 |
(* & (ALL f:fst(z). restrict(snd(z), domain(f)) = f)) | *) |
|
236 |
(* (~ (EX g:XX. domain(g)=succ(UN f:fst(z). domain(f)) *) |
|
237 |
(* & (ALL f:fst(z). restrict(g, domain(f)) = f)) & *) |
|
238 |
(* snd(z)={<0,x>})} *) |
|
239 |
(* *) |
|
240 |
(* Then XX and RR satisfy the hypotheses of DC(omega). *) |
|
241 |
(* So applying DC: *) |
|
242 |
(* *) |
|
243 |
(* EX f:nat->XX. ALL n:nat. f``n RR f`n *) |
|
244 |
(* *) |
|
245 |
(* Thence *) |
|
246 |
(* *) |
|
247 |
(* ff = {<n, f`n`n>. n:nat} *) |
|
248 |
(* *) |
|
249 |
(* is the desired function. *) |
|
250 |
(* *) |
|
1196 | 251 |
(* ********************************************************************** *) |
252 |
||
253 |
goalw thy [lesspoll_def, Finite_def] |
|
1461 | 254 |
"!!A. A lesspoll nat ==> Finite(A)"; |
1196 | 255 |
by (fast_tac (AC_cs addSDs [ltD, lepoll_imp_ex_le_eqpoll] |
1461 | 256 |
addSIs [Ord_nat]) 1); |
1196 | 257 |
val lesspoll_nat_is_Finite = result(); |
258 |
||
259 |
goal thy "!!n. n:nat ==> ALL A. (A eqpoll n & A <= X) --> A : Fin(X)"; |
|
1207 | 260 |
by (etac nat_induct 1); |
261 |
by (rtac allI 1); |
|
1196 | 262 |
by (fast_tac (AC_cs addSIs [Fin.emptyI] |
1461 | 263 |
addSDs [eqpoll_imp_lepoll RS lepoll_0_is_0]) 1); |
1207 | 264 |
by (rtac allI 1); |
265 |
by (rtac impI 1); |
|
266 |
by (etac conjE 1); |
|
1196 | 267 |
by (resolve_tac [eqpoll_succ_imp_not_empty RS not_emptyE] 1 |
1461 | 268 |
THEN (assume_tac 1)); |
1196 | 269 |
by (forward_tac [Diff_sing_eqpoll] 1 THEN (assume_tac 1)); |
1207 | 270 |
by (etac allE 1); |
271 |
by (etac impE 1); |
|
1196 | 272 |
by (fast_tac AC_cs 1); |
1207 | 273 |
by (dtac subsetD 1 THEN (assume_tac 1)); |
1196 | 274 |
by (dresolve_tac [Fin.consI] 1 THEN (assume_tac 1)); |
275 |
by (asm_full_simp_tac (AC_ss addsimps [cons_Diff]) 1); |
|
276 |
val Finite_Fin_lemma = result(); |
|
277 |
||
278 |
goalw thy [Finite_def] "!!A. [| Finite(A); A <= X |] ==> A : Fin(X)"; |
|
1207 | 279 |
by (etac bexE 1); |
280 |
by (dtac Finite_Fin_lemma 1); |
|
281 |
by (etac allE 1); |
|
282 |
by (etac impE 1); |
|
1196 | 283 |
by (assume_tac 2); |
284 |
by (fast_tac AC_cs 1); |
|
285 |
val Finite_Fin = result(); |
|
286 |
||
287 |
goal thy "!!x. x: X ==> {<0,x>}: (UN n:nat. \ |
|
1461 | 288 |
\ {f:succ(n)->X. ALL k:n. <f`k, f`succ(k)> : R})"; |
1196 | 289 |
by (fast_tac (AC_cs addSIs [nat_0I RS UN_I, singleton_fun RS Pi_type] |
1461 | 290 |
addss (AC_ss addsimps [[lepoll_refl, succI1] MRS lepoll_1_is_sing, |
291 |
apply_singleton_eq])) 1); |
|
1196 | 292 |
val singleton_in_funs = result(); |
293 |
||
294 |
goal thy |
|
1461 | 295 |
"!!X. [| XX = (UN n:nat. \ |
296 |
\ {f:succ(n)->domain(R). ALL k:n. <f`k, f`succ(k)> : R}); \ |
|
297 |
\ RR = {z:Fin(XX)*XX. (domain(snd(z))=succ(UN f:fst(z). domain(f)) \ |
|
298 |
\ & (ALL f:fst(z). restrict(snd(z), domain(f)) = f)) | \ |
|
299 |
\ (~ (EX g:XX. domain(g)=succ(UN f:fst(z). domain(f)) \ |
|
300 |
\ & (ALL f:fst(z). restrict(g, domain(f)) = f)) & snd(z)={<0,x>})}; \ |
|
301 |
\ range(R) <= domain(R); x:domain(R) \ |
|
302 |
\ |] ==> RR <= Pow(XX)*XX & \ |
|
303 |
\ (ALL Y:Pow(XX). Y lesspoll nat --> (EX x:XX. <Y,x>:RR))"; |
|
1207 | 304 |
by (rtac conjI 1); |
1932
cc9f1ba8f29a
Tidying: removing redundant args in classical reasoner calls
paulson
parents:
1924
diff
changeset
|
305 |
by (deepen_tac (ZF_cs addSEs [FinD RS PowI]) 0 1); |
1207 | 306 |
by (rtac ballI 1); |
307 |
by (rtac impI 1); |
|
1196 | 308 |
by (dresolve_tac [[lesspoll_nat_is_Finite, PowD] MRS Finite_Fin] 1 |
1461 | 309 |
THEN (assume_tac 1)); |
1196 | 310 |
by (excluded_middle_tac "EX g:XX. domain(g)=succ(UN f:Y. domain(f)) \ |
1461 | 311 |
\ & (ALL f:Y. restrict(g, domain(f)) = f)" 1); |
1196 | 312 |
by (fast_tac (AC_cs addss AC_ss) 2); |
313 |
by (fast_tac (FOL_cs addSEs [CollectE, singleton_in_funs] |
|
1461 | 314 |
addSIs [SigmaI] addIs [bexI] addss AC_ss) 1); |
1196 | 315 |
val lemma1 = result(); |
316 |
||
317 |
goal thy "!!f. [| f:nat->X; n:nat |] ==> \ |
|
1461 | 318 |
\ (UN x:f``succ(n). P(x)) = P(f`n) Un (UN x:f``n. P(x))"; |
1196 | 319 |
by (asm_full_simp_tac (AC_ss |
1461 | 320 |
addsimps [Ord_nat RSN (2, OrdmemD) RSN (2, image_fun), |
321 |
[nat_succI, Ord_nat] MRS OrdmemD RSN (2, image_fun)]) 1); |
|
1196 | 322 |
val UN_image_succ_eq = result(); |
323 |
||
324 |
goal thy "!!f. [| (UN x:f``n. P(x)) = y; P(f`n) = succ(y); \ |
|
1461 | 325 |
\ f:nat -> X; n:nat |] ==> (UN x:f``succ(n). P(x)) = succ(y)"; |
1196 | 326 |
by (asm_full_simp_tac (AC_ss addsimps [UN_image_succ_eq]) 1); |
327 |
by (fast_tac (AC_cs addSIs [equalityI]) 1); |
|
328 |
val UN_image_succ_eq_succ = result(); |
|
329 |
||
330 |
goal thy "!!f. [| f: (UN n:nat. {g:succ(n) -> D. P(g, n)}); \ |
|
1461 | 331 |
\ domain(f)=succ(x); x=y |] ==> f`y : D"; |
1196 | 332 |
by (fast_tac (AC_cs addEs [apply_type] |
1461 | 333 |
addSDs [[sym, domain_of_fun] MRS trans]) 1); |
1196 | 334 |
val apply_UN_type = result(); |
335 |
||
336 |
goal thy "!!f. [| f : nat -> X; n:nat |] ==> f``succ(n) = cons(f`n, f``n)"; |
|
337 |
by (asm_full_simp_tac (AC_ss |
|
1461 | 338 |
addsimps [nat_succI, Ord_nat RSN (2, OrdmemD), image_fun]) 1); |
1196 | 339 |
val image_fun_succ = result(); |
340 |
||
341 |
goal thy "!!f. [| domain(f`n) = succ(u); f : nat -> (UN n:nat. \ |
|
1461 | 342 |
\ {f:succ(n)->domain(R). ALL k:n. <f`k, f`succ(k)> : R}); \ |
343 |
\ u=k; n:nat \ |
|
344 |
\ |] ==> f`n : succ(k) -> domain(R)"; |
|
1207 | 345 |
by (dtac apply_type 1 THEN (assume_tac 1)); |
1196 | 346 |
by (fast_tac (AC_cs addEs [UN_E, domain_eq_imp_fun_type]) 1); |
347 |
val f_n_type = result(); |
|
348 |
||
349 |
goal thy "!!f. [| f : nat -> (UN n:nat. \ |
|
1461 | 350 |
\ {f:succ(n)->domain(R). ALL k:n. <f`k, f`succ(k)> : R}); \ |
351 |
\ domain(f`n) = succ(k); n:nat \ |
|
352 |
\ |] ==> ALL i:k. <f`n`i, f`n`succ(i)> : R"; |
|
1207 | 353 |
by (dtac apply_type 1 THEN (assume_tac 1)); |
354 |
by (etac UN_E 1); |
|
355 |
by (etac CollectE 1); |
|
1196 | 356 |
by (dresolve_tac [domain_of_fun RS sym RS trans] 1 THEN (assume_tac 1)); |
1207 | 357 |
by (dtac succ_eqD 1); |
1196 | 358 |
by (asm_full_simp_tac AC_ss 1); |
359 |
val f_n_pairs_in_R = result(); |
|
360 |
||
361 |
goalw thy [restrict_def] |
|
1461 | 362 |
"!!f. [| restrict(f, domain(x))=x; f:n->X; domain(x) <= n \ |
363 |
\ |] ==> restrict(cons(<n, y>, f), domain(x)) = x"; |
|
1196 | 364 |
by (eresolve_tac [sym RS trans RS sym] 1); |
1207 | 365 |
by (rtac fun_extension 1); |
1196 | 366 |
by (fast_tac (AC_cs addSIs [lam_type]) 1); |
367 |
by (fast_tac (AC_cs addSIs [lam_type]) 1); |
|
368 |
by (asm_full_simp_tac (AC_ss addsimps [subsetD RS cons_val_k]) 1); |
|
369 |
val restrict_cons_eq_restrict = result(); |
|
370 |
||
371 |
goal thy "!!f. [| ALL x:f``n. restrict(f`n, domain(x))=x; \ |
|
1461 | 372 |
\ f : nat -> (UN n:nat. \ |
373 |
\ {f:succ(n)->domain(R). ALL k:n. <f`k, f`succ(k)> : R}); \ |
|
374 |
\ n:nat; domain(f`n) = succ(n); \ |
|
375 |
\ (UN x:f``n. domain(x)) <= n |] \ |
|
376 |
\ ==> ALL x:f``succ(n). restrict(cons(<succ(n),y>, f`n), domain(x))=x"; |
|
1207 | 377 |
by (rtac ballI 1); |
1196 | 378 |
by (asm_full_simp_tac (AC_ss addsimps [image_fun_succ]) 1); |
1207 | 379 |
by (dtac f_n_type 1 THEN REPEAT (ares_tac [refl] 1)); |
380 |
by (etac consE 1); |
|
1196 | 381 |
by (asm_full_simp_tac (AC_ss addsimps [domain_of_fun, restrict_cons_eq]) 1); |
1207 | 382 |
by (dtac bspec 1 THEN (assume_tac 1)); |
1196 | 383 |
by (fast_tac (AC_cs addSEs [restrict_cons_eq_restrict]) 1); |
384 |
val all_in_image_restrict_eq = result(); |
|
385 |
||
386 |
goal thy "!!X. [| ALL b<nat. <f``b, f`b> : \ |
|
1461 | 387 |
\ {z:Fin(XX)*XX. (domain(snd(z))=succ(UN f:fst(z). domain(f)) \ |
388 |
\ & (ALL f:fst(z). restrict(snd(z), domain(f)) = f)) | \ |
|
389 |
\ (~ (EX g:XX. domain(g)=succ(UN f:fst(z). domain(f)) \ |
|
390 |
\ & (ALL f:fst(z). restrict(g, domain(f)) = f)) & snd(z)={<0,x>})}; \ |
|
391 |
\ XX = (UN n:nat. \ |
|
392 |
\ {f:succ(n)->domain(R). ALL k:n. <f`k, f`succ(k)> : R}); \ |
|
393 |
\ f: nat -> XX; range(R) <= domain(R); x:domain(R) \ |
|
394 |
\ |] ==> ALL b<nat. <f``b, f`b> : \ |
|
395 |
\ {z:Fin(XX)*XX. (domain(snd(z))=succ(UN f:fst(z). domain(f)) \ |
|
396 |
\ & (UN f:fst(z). domain(f)) = b \ |
|
397 |
\ & (ALL f:fst(z). restrict(snd(z), domain(f)) = f))}"; |
|
1207 | 398 |
by (rtac oallI 1); |
399 |
by (dtac ltD 1); |
|
400 |
by (etac nat_induct 1); |
|
1196 | 401 |
by (dresolve_tac [[nat_0I, Ord_nat] MRS ltI RSN (2, ospec)] 1); |
1200 | 402 |
by (fast_tac (FOL_cs addss |
1461 | 403 |
(ZF_ss addsimps [image_0, singleton_fun RS domain_of_fun, |
404 |
[lepoll_refl, succI1] MRS lepoll_1_is_sing, singleton_in_funs])) 1); |
|
1196 | 405 |
by (dresolve_tac [[nat_succI, Ord_nat] MRS ltI RSN (2, ospec)] 1 |
1461 | 406 |
THEN (assume_tac 1)); |
1196 | 407 |
by (REPEAT (eresolve_tac [conjE, CollectE, disjE] 1)); |
1200 | 408 |
by (fast_tac (FOL_cs addSEs [trans, subst_context] |
1461 | 409 |
addSIs [UN_image_succ_eq_succ] addss AC_ss) 1); |
1207 | 410 |
by (etac conjE 1); |
411 |
by (etac notE 1); |
|
1196 | 412 |
by (asm_full_simp_tac (AC_ss addsimps [UN_image_succ_eq_succ]) 1); |
1207 | 413 |
by (etac conjE 1); |
414 |
by (dtac apply_UN_type 1 THEN REPEAT (assume_tac 1)); |
|
415 |
by (etac domainE 1); |
|
416 |
by (etac domainE 1); |
|
1196 | 417 |
by (forward_tac [f_n_type] 1 THEN REPEAT (assume_tac 1)); |
418 |
by (res_inst_tac [("x","cons(<succ(xa), ya>, f`xa)")] bexI 1); |
|
419 |
by (fast_tac (FOL_cs |
|
1461 | 420 |
addEs [subst_context RSN (2, trans) RS domain_cons_eq_succ, |
421 |
subst_context, all_in_image_restrict_eq, trans, equalityD1]) 1); |
|
1207 | 422 |
by (rtac UN_I 1); |
423 |
by (etac nat_succI 1); |
|
424 |
by (rtac CollectI 1); |
|
1200 | 425 |
by (eresolve_tac [rangeI RSN (2, subsetD) RSN (2, cons_fun_type2)] 1 |
1461 | 426 |
THEN REPEAT (assume_tac 1)); |
1207 | 427 |
by (rtac ballI 1); |
428 |
by (etac succE 1); |
|
1196 | 429 |
by (asm_full_simp_tac (AC_ss addsimps [cons_val_n, cons_val_k]) 1); |
430 |
by (dresolve_tac [domain_of_fun RSN (2, f_n_pairs_in_R)] 1 |
|
1461 | 431 |
THEN REPEAT (assume_tac 1)); |
1207 | 432 |
by (dtac bspec 1 THEN (assume_tac 1)); |
1196 | 433 |
by (asm_full_simp_tac (AC_ss |
1461 | 434 |
addsimps [nat_into_Ord RS succ_in_succ, succI2, cons_val_k]) 1); |
1196 | 435 |
val simplify_recursion = result(); |
436 |
||
437 |
goal thy "!!X. [| XX = (UN n:nat. \ |
|
1461 | 438 |
\ {f:succ(n)->domain(R). ALL k:n. <f`k, f`succ(k)> : R}); \ |
439 |
\ ALL b<nat. <f``b, f`b> : \ |
|
440 |
\ {z:Fin(XX)*XX. (domain(snd(z))=succ(UN f:fst(z). domain(f)) \ |
|
441 |
\ & (UN f:fst(z). domain(f)) = b \ |
|
442 |
\ & (ALL f:fst(z). restrict(snd(z), domain(f)) = f))}; \ |
|
443 |
\ f: nat -> XX; range(R) <= domain(R); x:domain(R); n:nat \ |
|
444 |
\ |] ==> f`n : succ(n) -> domain(R) \ |
|
445 |
\ & (ALL i:n. <f`n`i, f`n`succ(i)>:R)"; |
|
1207 | 446 |
by (dtac ospec 1); |
1196 | 447 |
by (eresolve_tac [Ord_nat RSN (2, ltI)] 1); |
1207 | 448 |
by (etac CollectE 1); |
1196 | 449 |
by (asm_full_simp_tac AC_ss 1); |
1207 | 450 |
by (rtac conjI 1); |
1196 | 451 |
by (fast_tac (AC_cs |
1461 | 452 |
addSEs [trans RS domain_eq_imp_fun_type, subst_context]) 1); |
1200 | 453 |
by (fast_tac (FOL_cs |
1461 | 454 |
addSEs [conjE, f_n_pairs_in_R, trans, subst_context]) 1); |
1196 | 455 |
val lemma2 = result(); |
456 |
||
457 |
goal thy "!!n. [| XX = (UN n:nat. \ |
|
1461 | 458 |
\ {f:succ(n)->domain(R). ALL k:n. <f`k, f`succ(k)> : R}); \ |
459 |
\ ALL b<nat. <f``b, f`b> : \ |
|
460 |
\ {z:Fin(XX)*XX. (domain(snd(z))=succ(UN f:fst(z). domain(f)) \ |
|
461 |
\ & (UN f:fst(z). domain(f)) = b \ |
|
462 |
\ & (ALL f:fst(z). restrict(snd(z), domain(f)) = f))}; \ |
|
463 |
\ f : nat -> XX; n:nat; range(R) <= domain(R); x:domain(R) \ |
|
464 |
\ |] ==> f`n`n = f`succ(n)`n"; |
|
1196 | 465 |
by (forward_tac [lemma2 RS conjunct1 RS domain_of_fun] 1 |
1461 | 466 |
THEN REPEAT (assume_tac 1)); |
1196 | 467 |
by (dresolve_tac [[nat_succI, Ord_nat] MRS ltI RSN (2, ospec)] 1 |
1461 | 468 |
THEN (assume_tac 1)); |
1196 | 469 |
by (asm_full_simp_tac AC_ss 1); |
1207 | 470 |
by (REPEAT (etac conjE 1)); |
471 |
by (etac ballE 1); |
|
1196 | 472 |
by (eresolve_tac [restrict_eq_imp_val_eq RS sym] 1); |
473 |
by (fast_tac (AC_cs addSEs [ssubst]) 1); |
|
474 |
by (asm_full_simp_tac (AC_ss |
|
1461 | 475 |
addsimps [[nat_succI, Ord_nat] MRS OrdmemD RSN (2, image_fun)]) 1); |
1196 | 476 |
val lemma3 = result(); |
477 |
||
478 |
goalw thy [DC_def, DC0_def] "!!Z. DC(nat) ==> DC0"; |
|
479 |
by (REPEAT (resolve_tac [allI, impI] 1)); |
|
480 |
by (REPEAT (eresolve_tac [asm_rl, conjE, ex_in_domain RS exE, allE] 1)); |
|
481 |
by (eresolve_tac [[refl, refl] MRS lemma1 RSN (2, impE)] 1 |
|
1461 | 482 |
THEN REPEAT (assume_tac 1)); |
1207 | 483 |
by (etac bexE 1); |
1196 | 484 |
by (dresolve_tac [refl RSN (2, simplify_recursion)] 1 |
1461 | 485 |
THEN REPEAT (assume_tac 1)); |
1196 | 486 |
by (res_inst_tac [("x","lam n:nat. f`n`n")] bexI 1); |
1207 | 487 |
by (rtac lam_type 2); |
1196 | 488 |
by (eresolve_tac [[refl RS lemma2 RS conjunct1, succI1] MRS apply_type] 2 |
1461 | 489 |
THEN REPEAT (assume_tac 2)); |
1207 | 490 |
by (rtac ballI 1); |
1196 | 491 |
by (forward_tac [refl RS (nat_succI RSN (6, lemma2)) RS conjunct2] 1 |
1461 | 492 |
THEN REPEAT (assume_tac 1)); |
1196 | 493 |
by (dresolve_tac [refl RS lemma3] 1 THEN REPEAT (assume_tac 1)); |
494 |
by (asm_full_simp_tac (AC_ss addsimps [nat_succI]) 1); |
|
495 |
qed "DC_nat_DC0"; |
|
496 |
||
497 |
(* ********************************************************************** *) |
|
1461 | 498 |
(* ALL K. Card(K) --> DC(K) ==> WO3 *) |
1196 | 499 |
(* ********************************************************************** *) |
500 |
||
501 |
goalw thy [lesspoll_def] |
|
1461 | 502 |
"!!A. [| ~ A lesspoll B; C lesspoll B |] ==> A - C ~= 0"; |
1196 | 503 |
by (fast_tac (AC_cs addSDs [Diff_eq_0_iff RS iffD1 RS subset_imp_lepoll] |
1461 | 504 |
addSIs [eqpollI] addEs [notE] addSEs [eqpollE, lepoll_trans]) 1); |
1196 | 505 |
val lemma1 = result(); |
506 |
||
507 |
val [f_type, Ord_a, not_eq] = goalw thy [inj_def] |
|
1461 | 508 |
"[| f:a->X; Ord(a); (!!b c. [| b<c; c:a |] ==> f`b~=f`c) \ |
509 |
\ |] ==> f:inj(a, X)"; |
|
1196 | 510 |
by (resolve_tac [f_type RS CollectI] 1); |
511 |
by (REPEAT (resolve_tac [ballI,impI] 1)); |
|
512 |
by (resolve_tac [Ord_a RS Ord_in_Ord RS Ord_linear_lt] 1 |
|
1461 | 513 |
THEN (assume_tac 1)); |
1196 | 514 |
by (eres_inst_tac [("j","x")] (Ord_a RS Ord_in_Ord) 1); |
515 |
by (REPEAT (fast_tac (AC_cs addDs [not_eq, not_eq RS not_sym]) 1)); |
|
516 |
val fun_Ord_inj = result(); |
|
517 |
||
518 |
goal thy "!!a. [| f:X->Y; A<=X; a:A |] ==> f`a : f``A"; |
|
519 |
by (fast_tac (AC_cs addSEs [image_fun RS ssubst]) 1); |
|
520 |
val value_in_image = result(); |
|
521 |
||
522 |
goalw thy [DC_def, WO3_def] |
|
1461 | 523 |
"!!Z. ALL K. Card(K) --> DC(K) ==> WO3"; |
1207 | 524 |
by (rtac allI 1); |
1196 | 525 |
by (excluded_middle_tac "A lesspoll Hartog(A)" 1); |
526 |
by (fast_tac (AC_cs addSDs [lesspoll_imp_ex_lt_eqpoll] |
|
1461 | 527 |
addSIs [Ord_Hartog, leI RS le_imp_subset]) 2); |
1196 | 528 |
by (REPEAT (eresolve_tac [allE, impE] 1)); |
1207 | 529 |
by (rtac Card_Hartog 1); |
1196 | 530 |
by (eres_inst_tac [("x","A")] allE 1); |
531 |
by (eres_inst_tac [("x","{z:Pow(A)*A . fst(z) \ |
|
1461 | 532 |
\ lesspoll Hartog(A) & snd(z) ~: fst(z)}")] allE 1); |
1196 | 533 |
by (asm_full_simp_tac AC_ss 1); |
1207 | 534 |
by (etac impE 1); |
1196 | 535 |
by (fast_tac (AC_cs addEs [lemma1 RS not_emptyE]) 1); |
1207 | 536 |
by (etac bexE 1); |
1196 | 537 |
by (resolve_tac [exI RS (lepoll_def RS (def_imp_iff RS iffD2)) |
1461 | 538 |
RS (HartogI RS notE)] 1); |
1196 | 539 |
by (resolve_tac [Ord_Hartog RSN (2, fun_Ord_inj)] 1 THEN (assume_tac 1)); |
540 |
by (dresolve_tac [Ord_Hartog RSN (2, OrdmemD) RSN (2, |
|
1461 | 541 |
ltD RSN (3, value_in_image))] 1 |
542 |
THEN REPEAT (assume_tac 1)); |
|
1196 | 543 |
by (fast_tac (AC_cs addSDs [Ord_Hartog RSN (2, ltI) RSN (2, ospec)] |
1461 | 544 |
addEs [subst]) 1); |
1196 | 545 |
qed "DC_WO3"; |
546 |
||
547 |
(* ********************************************************************** *) |
|
1461 | 548 |
(* WO1 ==> ALL K. Card(K) --> DC(K) *) |
1196 | 549 |
(* ********************************************************************** *) |
550 |
||
551 |
goal thy |
|
1461 | 552 |
"!!a. [| Ord(a); b:a |] ==> (lam x:a. P(x))``b = (lam x:b. P(x))``b"; |
1207 | 553 |
by (rtac images_eq 1); |
1196 | 554 |
by (REPEAT (fast_tac (AC_cs addSEs [RepFunI, OrdmemD] |
1461 | 555 |
addSIs [lam_type]) 2)); |
1207 | 556 |
by (rtac ballI 1); |
1196 | 557 |
by (dresolve_tac [OrdmemD RS subsetD] 1 |
1461 | 558 |
THEN REPEAT (assume_tac 1)); |
1196 | 559 |
by (asm_full_simp_tac AC_ss 1); |
560 |
val lam_images_eq = result(); |
|
561 |
||
562 |
goalw thy [lesspoll_def] "!!K. [| Card(K); b:K |] ==> b lesspoll K"; |
|
563 |
by (asm_full_simp_tac (AC_ss addsimps [Card_iff_initial]) 1); |
|
564 |
by (fast_tac (AC_cs addSIs [le_imp_lepoll, ltI, leI]) 1); |
|
565 |
val in_Card_imp_lesspoll = result(); |
|
566 |
||
567 |
goal thy "(lam b:a. P(b)) : a -> {P(b). b:a}"; |
|
568 |
by (fast_tac (AC_cs addSIs [lam_type, RepFunI]) 1); |
|
569 |
val lam_type_RepFun = result(); |
|
570 |
||
571 |
goal thy "!!Z. [| ALL Y:Pow(X). Y lesspoll a --> (EX x:X. <Y, x> : R); \ |
|
1461 | 572 |
\ b:a; Z:Pow(X); Z lesspoll a |] \ |
573 |
\ ==> {x:X. <Z,x> : R} ~= 0"; |
|
1200 | 574 |
by (fast_tac (FOL_cs addEs [bexE, equals0D] |
1461 | 575 |
addSDs [bspec] addIs [CollectI]) 1); |
1196 | 576 |
val lemma_ = result(); |
577 |
||
578 |
goal thy "!!K. [| Card(K); well_ord(X,Q); \ |
|
1461 | 579 |
\ ALL Y:Pow(X). Y lesspoll K --> (EX x:X. <Y, x> : R); b:K |] \ |
580 |
\ ==> ff(b, X, Q, R) : {x:X. <(lam c:b. ff(c, X, Q, R))``b, x> : R}"; |
|
1196 | 581 |
by (res_inst_tac [("P","b:K")] impE 1 THEN TRYALL assume_tac); |
582 |
by (res_inst_tac [("i","b")] (Card_is_Ord RS Ord_in_Ord RS trans_induct) 1 |
|
1461 | 583 |
THEN REPEAT (assume_tac 1)); |
1207 | 584 |
by (rtac impI 1); |
1196 | 585 |
by (resolve_tac [ff_def RS def_transrec RS ssubst] 1); |
1207 | 586 |
by (etac the_first_in 1); |
1196 | 587 |
by (fast_tac AC_cs 1); |
588 |
by (asm_full_simp_tac (AC_ss |
|
1461 | 589 |
addsimps [[lam_type_RepFun, subset_refl] MRS image_fun]) 1); |
1207 | 590 |
by (etac lemma_ 1 THEN (assume_tac 1)); |
1196 | 591 |
by (fast_tac (AC_cs addSEs [RepFunE, impE, notE] |
1461 | 592 |
addEs [Card_is_Ord RSN (2, OrdmemD) RS subsetD]) 1); |
1196 | 593 |
by (fast_tac (AC_cs addSEs [[in_Card_imp_lesspoll, RepFun_lepoll] |
1461 | 594 |
MRS lepoll_lesspoll_lesspoll]) 1); |
1196 | 595 |
val lemma = result(); |
596 |
||
597 |
goalw thy [DC_def, WO1_def] |
|
1461 | 598 |
"!!Z. WO1 ==> ALL K. Card(K) --> DC(K)"; |
1196 | 599 |
by (REPEAT (resolve_tac [allI,impI] 1)); |
600 |
by (REPEAT (eresolve_tac [allE,exE,conjE] 1)); |
|
601 |
by (res_inst_tac [("x","lam b:K. ff(b, X, Ra, R)")] bexI 1); |
|
1207 | 602 |
by (rtac lam_type 2); |
1196 | 603 |
by (resolve_tac [lemma RS CollectD1] 2 THEN REPEAT (assume_tac 2)); |
604 |
by (asm_full_simp_tac (AC_ss |
|
1461 | 605 |
addsimps [[Card_is_Ord, ltD] MRS lam_images_eq]) 1); |
1196 | 606 |
by (fast_tac (AC_cs addSEs [ltE, lemma RS CollectD2]) 1); |
607 |
qed" WO1_DC_Card"; |
|
608 |