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