41 goal thy "!!X. ALL Y:Pow(X). Y lesspoll nat --> (EX x:X. <Y, x> : R) \ |
41 goal thy "!!X. ALL Y:Pow(X). Y lesspoll nat --> (EX x:X. <Y, x> : R) \ |
42 \ ==> {z: (UN n:nat. {f:n->X. ALL k:n. <f``k, f`k> : R}) * \ |
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}). \ |
43 \ (UN n:nat. {f:n->X. ALL k:n. <f``k, f`k> : R}). \ |
44 \ domain(snd(z))=succ(domain(fst(z))) \ |
44 \ domain(snd(z))=succ(domain(fst(z))) \ |
45 \ & restrict(snd(z), domain(fst(z))) = fst(z)} ~= 0"; |
45 \ & restrict(snd(z), domain(fst(z))) = fst(z)} ~= 0"; |
46 by (eresolve_tac [ballE] 1); |
46 by (etac ballE 1); |
47 by (eresolve_tac [empty_subsetI RS PowI RSN (2, notE)] 2); |
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); |
48 by (eresolve_tac [nat_0I RS n_lesspoll_nat RSN (2, impE)] 1); |
49 by (eresolve_tac [bexE] 1); |
49 by (etac bexE 1); |
50 by (res_inst_tac [("a","<0, {<0, x>}>")] not_emptyI 1); |
50 by (res_inst_tac [("a","<0, {<0, x>}>")] not_emptyI 1); |
51 by (resolve_tac [CollectI] 1); |
51 by (rtac CollectI 1); |
52 by (resolve_tac [SigmaI] 1); |
52 by (rtac SigmaI 1); |
53 by (fast_tac (AC_cs addSIs [nat_0I RS UN_I, empty_fun]) 1); |
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] |
54 by (fast_tac (AC_cs addSIs [nat_1I RS UN_I, singleton_fun RS Pi_type] |
55 addss (AC_ss addsimps [[lepoll_refl, succI1] MRS lepoll_1_is_sing, |
55 addss (AC_ss addsimps [[lepoll_refl, succI1] MRS lepoll_1_is_sing, |
56 apply_singleton_eq, image_0])) 1); |
56 apply_singleton_eq, image_0])) 1); |
57 by (asm_full_simp_tac (AC_ss addsimps [domain_0, restrict_0, domain_sing, |
57 by (asm_full_simp_tac (AC_ss addsimps [domain_0, restrict_0, domain_sing, |
65 \ & restrict(snd(z), domain(fst(z))) = 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}) * \ |
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}). \ |
67 \ (UN n:nat. {f:n->X. ALL k:n. <f``k, f`k> : R}). \ |
68 \ domain(snd(z))=succ(domain(fst(z))) \ |
68 \ domain(snd(z))=succ(domain(fst(z))) \ |
69 \ & restrict(snd(z), domain(fst(z))) = fst(z)})"; |
69 \ & restrict(snd(z), domain(fst(z))) = fst(z)})"; |
70 by (resolve_tac [range_subset_domain] 1); |
70 by (rtac range_subset_domain 1); |
71 by (resolve_tac [subsetI] 2); |
71 by (rtac subsetI 2); |
72 by (eresolve_tac [CollectD1] 2); |
72 by (etac CollectD1 2); |
73 by (eresolve_tac [UN_E] 1); |
73 by (etac UN_E 1); |
74 by (eresolve_tac [CollectE] 1); |
74 by (etac CollectE 1); |
75 by (dresolve_tac [fun_is_rel RS image_subset RS PowI RSN (2, bspec)] 1 |
75 by (dresolve_tac [fun_is_rel RS image_subset RS PowI RSN (2, bspec)] 1 |
76 THEN (assume_tac 1)); |
76 THEN (assume_tac 1)); |
77 by (eresolve_tac [[n_lesspoll_nat, nat_into_Ord RSN (2, image_Ord_lepoll)] |
77 by (eresolve_tac [[n_lesspoll_nat, nat_into_Ord RSN (2, image_Ord_lepoll)] |
78 MRS lepoll_lesspoll_lesspoll RSN (2, impE)] 1 |
78 MRS lepoll_lesspoll_lesspoll RSN (2, impE)] 1 |
79 THEN REPEAT (assume_tac 1)); |
79 THEN REPEAT (assume_tac 1)); |
80 by (eresolve_tac [bexE] 1); |
80 by (etac bexE 1); |
81 by (res_inst_tac [("x","cons(<n,x>, g)")] exI 1); |
81 by (res_inst_tac [("x","cons(<n,x>, g)")] exI 1); |
82 by (resolve_tac [CollectI] 1); |
82 by (rtac CollectI 1); |
83 by (resolve_tac [SigmaI] 1); |
83 by (rtac SigmaI 1); |
84 by (fast_tac AC_cs 1); |
84 by (fast_tac AC_cs 1); |
85 by (resolve_tac [UN_I] 1); |
85 by (rtac UN_I 1); |
86 by (eresolve_tac [nat_succI] 1); |
86 by (etac nat_succI 1); |
87 by (resolve_tac [CollectI] 1); |
87 by (rtac CollectI 1); |
88 by (eresolve_tac [cons_fun_type2] 1 THEN (assume_tac 1)); |
88 by (etac cons_fun_type2 1 THEN (assume_tac 1)); |
89 by (fast_tac (AC_cs addSEs [succE] addss (AC_ss |
89 by (fast_tac (AC_cs addSEs [succE] addss (AC_ss |
90 addsimps [cons_image_n, cons_val_n, cons_image_k, cons_val_k])) 1); |
90 addsimps [cons_image_n, cons_val_n, cons_image_k, cons_val_k])) 1); |
91 by (asm_full_simp_tac (AC_ss |
91 by (asm_full_simp_tac (AC_ss |
92 addsimps [domain_cons, domain_of_fun, succ_def, restrict_cons_eq]) 1); |
92 addsimps [domain_cons, domain_of_fun, succ_def, restrict_cons_eq]) 1); |
93 val lemma1_3 = result(); |
93 val lemma1_3 = result(); |
102 |
102 |
103 goal thy "!!f. [| <f,g> : {z:XX*XX. \ |
103 goal thy "!!f. [| <f,g> : {z:XX*XX. \ |
104 \ domain(snd(z))=succ(domain(fst(z))) & Q(z)}; \ |
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 \ |
105 \ XX = (UN n:nat. {f:n->X. ALL k:n. <f``k, f`k> : R}); f:k->X \ |
106 \ |] ==> g:succ(k)->X"; |
106 \ |] ==> g:succ(k)->X"; |
107 by (eresolve_tac [CollectE] 1); |
107 by (etac CollectE 1); |
108 by (dresolve_tac [SigmaD2] 1); |
108 by (dtac SigmaD2 1); |
109 by (hyp_subst_tac 1); |
109 by (hyp_subst_tac 1); |
110 by (eresolve_tac [UN_E] 1); |
110 by (etac UN_E 1); |
111 by (eresolve_tac [CollectE] 1); |
111 by (etac CollectE 1); |
112 by (asm_full_simp_tac AC_ss 1); |
112 by (asm_full_simp_tac AC_ss 1); |
113 by (dresolve_tac [domain_of_fun] 1); |
113 by (dtac domain_of_fun 1); |
114 by (eresolve_tac [conjE] 1); |
114 by (etac conjE 1); |
115 by (forward_tac [domain_of_fun RS sym RS trans] 1 THEN (assume_tac 1)); |
115 by (forward_tac [domain_of_fun RS sym RS trans] 1 THEN (assume_tac 1)); |
116 by (fast_tac AC_cs 1); |
116 by (fast_tac AC_cs 1); |
117 val lemma2_1 = result(); |
117 val lemma2_1 = result(); |
118 |
118 |
119 goal thy "!!X. [| XX = (UN n:nat. {f:n->X. ALL k:n. <f``k, f`k> : R}); \ |
119 goal thy "!!X. [| XX = (UN n:nat. {f:n->X. ALL k:n. <f``k, f`k> : R}); \ |
121 \ {z:XX*XX. domain(snd(z))=succ(domain(fst(z))) \ |
121 \ {z:XX*XX. domain(snd(z))=succ(domain(fst(z))) \ |
122 \ & restrict(snd(z), domain(fst(z))) = fst(z)}; \ |
122 \ & restrict(snd(z), domain(fst(z))) = fst(z)}; \ |
123 \ f: nat -> XX; n:nat \ |
123 \ f: nat -> XX; n:nat \ |
124 \ |] ==> EX k:nat. f`succ(n) : k -> X & n:k \ |
124 \ |] ==> EX k:nat. f`succ(n) : k -> X & n:k \ |
125 \ & <f`succ(n)``n, f`succ(n)`n> : R"; |
125 \ & <f`succ(n)``n, f`succ(n)`n> : R"; |
126 by (eresolve_tac [nat_induct] 1); |
126 by (etac nat_induct 1); |
127 by (dresolve_tac [nat_1I RSN (2, apply_type)] 1); |
127 by (dresolve_tac [nat_1I RSN (2, apply_type)] 1); |
128 by (dresolve_tac [nat_0I RSN (2, bspec)] 1); |
128 by (dresolve_tac [nat_0I RSN (2, bspec)] 1); |
129 by (asm_full_simp_tac AC_ss 1); |
129 by (asm_full_simp_tac AC_ss 1); |
130 by (eresolve_tac [UN_E] 1); |
130 by (etac UN_E 1); |
131 by (eresolve_tac [CollectE] 1); |
131 by (etac CollectE 1); |
132 by (resolve_tac [bexI] 1 THEN (assume_tac 2)); |
132 by (rtac bexI 1 THEN (assume_tac 2)); |
133 by (fast_tac (AC_cs addSEs [nat_0_le RS leE, ltD, ltD RSN (2, bspec)] |
133 by (fast_tac (AC_cs addSEs [nat_0_le RS leE, ltD, ltD RSN (2, bspec)] |
134 addEs [sym RS trans RS succ_neq_0, domain_of_fun]) 1); |
134 addEs [sym RS trans RS succ_neq_0, domain_of_fun]) 1); |
135 by (eresolve_tac [bexE] 1); |
135 by (etac bexE 1); |
136 by (dresolve_tac [nat_succI RSN (2, bspec)] 1 THEN (assume_tac 1)); |
136 by (dresolve_tac [nat_succI RSN (2, bspec)] 1 THEN (assume_tac 1)); |
137 by (eresolve_tac [conjE] 1); |
137 by (etac conjE 1); |
138 by (dresolve_tac [lemma2_1] 1 THEN REPEAT (assume_tac 1)); |
138 by (dtac lemma2_1 1 THEN REPEAT (assume_tac 1)); |
139 by (hyp_subst_tac 1); |
139 by (hyp_subst_tac 1); |
140 by (dresolve_tac [nat_succI RS nat_succI RSN (2, apply_type)] 1 |
140 by (dresolve_tac [nat_succI RS nat_succI RSN (2, apply_type)] 1 |
141 THEN (assume_tac 1)); |
141 THEN (assume_tac 1)); |
142 by (eresolve_tac [UN_E] 1); |
142 by (etac UN_E 1); |
143 by (eresolve_tac [CollectE] 1); |
143 by (etac CollectE 1); |
144 by (dresolve_tac [[domain_of_fun RS sym, domain_of_fun] MRS trans] 1 |
144 by (dresolve_tac [[domain_of_fun RS sym, domain_of_fun] MRS trans] 1 |
145 THEN (assume_tac 1)); |
145 THEN (assume_tac 1)); |
146 by (fast_tac (AC_cs addSEs [nat_succI, nat_into_Ord RS succ_in_succ] |
146 by (fast_tac (AC_cs addSEs [nat_succI, nat_into_Ord RS succ_in_succ] |
147 addSDs [nat_into_Ord RS succ_in_succ RSN (2, bspec)]) 1); |
147 addSDs [nat_into_Ord RS succ_in_succ RSN (2, bspec)]) 1); |
148 val lemma2 = result(); |
148 val lemma2 = result(); |
151 \ ALL n:nat. <f`n, f`succ(n)> : \ |
151 \ ALL n:nat. <f`n, f`succ(n)> : \ |
152 \ {z:XX*XX. domain(snd(z))=succ(domain(fst(z))) \ |
152 \ {z:XX*XX. domain(snd(z))=succ(domain(fst(z))) \ |
153 \ & restrict(snd(z), domain(fst(z))) = fst(z)}; \ |
153 \ & restrict(snd(z), domain(fst(z))) = fst(z)}; \ |
154 \ f: nat -> XX; n:nat \ |
154 \ f: nat -> XX; n:nat \ |
155 \ |] ==> ALL x:n. f`succ(n)`x = f`succ(x)`x"; |
155 \ |] ==> ALL x:n. f`succ(n)`x = f`succ(x)`x"; |
156 by (eresolve_tac [nat_induct] 1); |
156 by (etac nat_induct 1); |
157 by (fast_tac AC_cs 1); |
157 by (fast_tac AC_cs 1); |
158 by (resolve_tac [ballI] 1); |
158 by (rtac ballI 1); |
159 by (eresolve_tac [succE] 1); |
159 by (etac succE 1); |
160 by (resolve_tac [restrict_eq_imp_val_eq] 1); |
160 by (rtac restrict_eq_imp_val_eq 1); |
161 by (dresolve_tac [nat_succI RSN (2, bspec)] 1 THEN (assume_tac 1)); |
161 by (dresolve_tac [nat_succI RSN (2, bspec)] 1 THEN (assume_tac 1)); |
162 by (asm_full_simp_tac AC_ss 1); |
162 by (asm_full_simp_tac AC_ss 1); |
163 by (dresolve_tac [lemma2] 1 THEN REPEAT (assume_tac 1)); |
163 by (dtac lemma2 1 THEN REPEAT (assume_tac 1)); |
164 by (fast_tac (AC_cs addSDs [domain_of_fun]) 1); |
164 by (fast_tac (AC_cs addSDs [domain_of_fun]) 1); |
165 by (dres_inst_tac [("x","xa")] bspec 1 THEN (assume_tac 1)); |
165 by (dres_inst_tac [("x","xa")] bspec 1 THEN (assume_tac 1)); |
166 by (eresolve_tac [sym RS trans RS sym] 1); |
166 by (eresolve_tac [sym RS trans RS sym] 1); |
167 by (resolve_tac [restrict_eq_imp_val_eq 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)); |
168 by (dresolve_tac [nat_succI RSN (2, bspec)] 1 THEN (assume_tac 1)); |
169 by (asm_full_simp_tac AC_ss 1); |
169 by (asm_full_simp_tac AC_ss 1); |
170 by (dresolve_tac [lemma2] 1 THEN REPEAT (assume_tac 1)); |
170 by (dtac lemma2 1 THEN REPEAT (assume_tac 1)); |
171 by (fast_tac (FOL_cs addSDs [domain_of_fun] |
171 by (fast_tac (FOL_cs addSDs [domain_of_fun] |
172 addSEs [bexE, nat_into_Ord RSN (2, OrdmemD) RS subsetD]) 1); |
172 addSEs [bexE, nat_into_Ord RSN (2, OrdmemD) RS subsetD]) 1); |
173 val lemma3_1 = result(); |
173 val lemma3_1 = result(); |
174 |
174 |
175 goal thy "!!n. ALL x:n. f`succ(n)`x = f`succ(x)`x \ |
175 goal thy "!!n. ALL x:n. f`succ(n)`x = f`succ(x)`x \ |
181 \ ALL n:nat. <f`n, f`succ(n)> : \ |
181 \ ALL n:nat. <f`n, f`succ(n)> : \ |
182 \ {z:XX*XX. domain(snd(z))=succ(domain(fst(z))) \ |
182 \ {z:XX*XX. domain(snd(z))=succ(domain(fst(z))) \ |
183 \ & restrict(snd(z), domain(fst(z))) = fst(z)}; \ |
183 \ & restrict(snd(z), domain(fst(z))) = fst(z)}; \ |
184 \ f: nat -> XX; n:nat \ |
184 \ f: nat -> XX; n:nat \ |
185 \ |] ==> (lam x:nat. f`succ(x)`x) `` n = f`succ(n)``n"; |
185 \ |] ==> (lam x:nat. f`succ(x)`x) `` n = f`succ(n)``n"; |
186 by (eresolve_tac [natE] 1); |
186 by (etac natE 1); |
187 by (asm_full_simp_tac (AC_ss addsimps [image_0]) 1); |
187 by (asm_full_simp_tac (AC_ss addsimps [image_0]) 1); |
188 by (resolve_tac [image_lam RS ssubst] 1); |
188 by (resolve_tac [image_lam RS ssubst] 1); |
189 by (fast_tac (AC_cs addSEs [[nat_succI, Ord_nat] MRS OrdmemD]) 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 |
190 by (resolve_tac [lemma3_1 RS lemma3_2 RS ssubst] 1 |
191 THEN REPEAT (assume_tac 1)); |
191 THEN REPEAT (assume_tac 1)); |
195 by (fast_tac (AC_cs addSEs [conjE, image_fun RS sym, |
195 by (fast_tac (AC_cs addSEs [conjE, image_fun RS sym, |
196 nat_into_Ord RSN (2, OrdmemD)]) 1); |
196 nat_into_Ord RSN (2, OrdmemD)]) 1); |
197 val lemma3 = result(); |
197 val lemma3 = result(); |
198 |
198 |
199 goal thy "!!f. [| f:A->B; B<=C |] ==> f:A->C"; |
199 goal thy "!!f. [| f:A->B; B<=C |] ==> f:A->C"; |
200 by (resolve_tac [Pi_type] 1 THEN (assume_tac 1)); |
200 by (rtac Pi_type 1 THEN (assume_tac 1)); |
201 by (fast_tac (AC_cs addSEs [apply_type]) 1); |
201 by (fast_tac (AC_cs addSEs [apply_type]) 1); |
202 val fun_type_gen = result(); |
202 val fun_type_gen = result(); |
203 |
203 |
204 goalw thy [DC_def, DC0_def] "!!Z. DC0 ==> DC(nat)"; |
204 goalw thy [DC_def, DC0_def] "!!Z. DC0 ==> DC(nat)"; |
205 by (REPEAT (resolve_tac [allI, impI] 1)); |
205 by (REPEAT (resolve_tac [allI, impI] 1)); |
206 by (REPEAT (eresolve_tac [conjE, allE] 1)); |
206 by (REPEAT (eresolve_tac [conjE, allE] 1)); |
207 by (eresolve_tac [[refl, refl] MRS lemma1 RSN (2, impE)] 1 |
207 by (eresolve_tac [[refl, refl] MRS lemma1 RSN (2, impE)] 1 |
208 THEN (assume_tac 1)); |
208 THEN (assume_tac 1)); |
209 by (eresolve_tac [bexE] 1); |
209 by (etac bexE 1); |
210 by (res_inst_tac [("x","lam n:nat. f`succ(n)`n")] bexI 1); |
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] |
211 by (fast_tac (AC_cs addSIs [lam_type] addSDs [refl RS lemma2] |
212 addSEs [fun_type_gen, apply_type]) 2); |
212 addSEs [fun_type_gen, apply_type]) 2); |
213 by (resolve_tac [oallI] 1); |
213 by (rtac oallI 1); |
214 by (forward_tac [ltD RSN (3, refl RS lemma2)] 1 |
214 by (forward_tac [ltD RSN (3, refl RS lemma2)] 1 |
215 THEN assume_tac 2); |
215 THEN assume_tac 2); |
216 by (fast_tac (AC_cs addSEs [fun_type_gen]) 1); |
216 by (fast_tac (AC_cs addSEs [fun_type_gen]) 1); |
217 by (eresolve_tac [ltD RSN (3, refl RS lemma3) RS ssubst] 1 |
217 by (eresolve_tac [ltD RSN (3, refl RS lemma3) RS ssubst] 1 |
218 THEN assume_tac 2); |
218 THEN assume_tac 2); |
255 by (fast_tac (AC_cs addSDs [ltD, lepoll_imp_ex_le_eqpoll] |
255 by (fast_tac (AC_cs addSDs [ltD, lepoll_imp_ex_le_eqpoll] |
256 addSIs [Ord_nat]) 1); |
256 addSIs [Ord_nat]) 1); |
257 val lesspoll_nat_is_Finite = result(); |
257 val lesspoll_nat_is_Finite = result(); |
258 |
258 |
259 goal thy "!!n. n:nat ==> ALL A. (A eqpoll n & A <= X) --> A : Fin(X)"; |
259 goal thy "!!n. n:nat ==> ALL A. (A eqpoll n & A <= X) --> A : Fin(X)"; |
260 by (eresolve_tac [nat_induct] 1); |
260 by (etac nat_induct 1); |
261 by (resolve_tac [allI] 1); |
261 by (rtac allI 1); |
262 by (fast_tac (AC_cs addSIs [Fin.emptyI] |
262 by (fast_tac (AC_cs addSIs [Fin.emptyI] |
263 addSDs [eqpoll_imp_lepoll RS lepoll_0_is_0]) 1); |
263 addSDs [eqpoll_imp_lepoll RS lepoll_0_is_0]) 1); |
264 by (resolve_tac [allI] 1); |
264 by (rtac allI 1); |
265 by (resolve_tac [impI] 1); |
265 by (rtac impI 1); |
266 by (eresolve_tac [conjE] 1); |
266 by (etac conjE 1); |
267 by (resolve_tac [eqpoll_succ_imp_not_empty RS not_emptyE] 1 |
267 by (resolve_tac [eqpoll_succ_imp_not_empty RS not_emptyE] 1 |
268 THEN (assume_tac 1)); |
268 THEN (assume_tac 1)); |
269 by (forward_tac [Diff_sing_eqpoll] 1 THEN (assume_tac 1)); |
269 by (forward_tac [Diff_sing_eqpoll] 1 THEN (assume_tac 1)); |
270 by (eresolve_tac [allE] 1); |
270 by (etac allE 1); |
271 by (eresolve_tac [impE] 1); |
271 by (etac impE 1); |
272 by (fast_tac AC_cs 1); |
272 by (fast_tac AC_cs 1); |
273 by (dresolve_tac [subsetD] 1 THEN (assume_tac 1)); |
273 by (dtac subsetD 1 THEN (assume_tac 1)); |
274 by (dresolve_tac [Fin.consI] 1 THEN (assume_tac 1)); |
274 by (dresolve_tac [Fin.consI] 1 THEN (assume_tac 1)); |
275 by (asm_full_simp_tac (AC_ss addsimps [cons_Diff]) 1); |
275 by (asm_full_simp_tac (AC_ss addsimps [cons_Diff]) 1); |
276 val Finite_Fin_lemma = result(); |
276 val Finite_Fin_lemma = result(); |
277 |
277 |
278 goalw thy [Finite_def] "!!A. [| Finite(A); A <= X |] ==> A : Fin(X)"; |
278 goalw thy [Finite_def] "!!A. [| Finite(A); A <= X |] ==> A : Fin(X)"; |
279 by (eresolve_tac [bexE] 1); |
279 by (etac bexE 1); |
280 by (dresolve_tac [Finite_Fin_lemma] 1); |
280 by (dtac Finite_Fin_lemma 1); |
281 by (eresolve_tac [allE] 1); |
281 by (etac allE 1); |
282 by (eresolve_tac [impE] 1); |
282 by (etac impE 1); |
283 by (assume_tac 2); |
283 by (assume_tac 2); |
284 by (fast_tac AC_cs 1); |
284 by (fast_tac AC_cs 1); |
285 val Finite_Fin = result(); |
285 val Finite_Fin = result(); |
286 |
286 |
287 goal thy "!!x. x: X ==> {<0,x>}: (UN n:nat. \ |
287 goal thy "!!x. x: X ==> {<0,x>}: (UN n:nat. \ |
299 \ (~ (EX g:XX. domain(g)=succ(UN f:fst(z). domain(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>})}; \ |
300 \ & (ALL f:fst(z). restrict(g, domain(f)) = f)) & snd(z)={<0,x>})}; \ |
301 \ range(R) <= domain(R); x:domain(R) \ |
301 \ range(R) <= domain(R); x:domain(R) \ |
302 \ |] ==> RR <= Pow(XX)*XX & \ |
302 \ |] ==> RR <= Pow(XX)*XX & \ |
303 \ (ALL Y:Pow(XX). Y lesspoll nat --> (EX x:XX. <Y,x>:RR))"; |
303 \ (ALL Y:Pow(XX). Y lesspoll nat --> (EX x:XX. <Y,x>:RR))"; |
304 by (resolve_tac [conjI] 1); |
304 by (rtac conjI 1); |
305 by (fast_tac (FOL_cs addSEs [FinD RS PowI, SigmaE, CollectE] |
305 by (fast_tac (FOL_cs addSEs [FinD RS PowI, SigmaE, CollectE] |
306 addSIs [subsetI, SigmaI]) 1); |
306 addSIs [subsetI, SigmaI]) 1); |
307 by (resolve_tac [ballI] 1); |
307 by (rtac ballI 1); |
308 by (resolve_tac [impI] 1); |
308 by (rtac impI 1); |
309 by (dresolve_tac [[lesspoll_nat_is_Finite, PowD] MRS Finite_Fin] 1 |
309 by (dresolve_tac [[lesspoll_nat_is_Finite, PowD] MRS Finite_Fin] 1 |
310 THEN (assume_tac 1)); |
310 THEN (assume_tac 1)); |
311 by (excluded_middle_tac "EX g:XX. domain(g)=succ(UN f:Y. domain(f)) \ |
311 by (excluded_middle_tac "EX g:XX. domain(g)=succ(UN f:Y. domain(f)) \ |
312 \ & (ALL f:Y. restrict(g, domain(f)) = f)" 1); |
312 \ & (ALL f:Y. restrict(g, domain(f)) = f)" 1); |
313 by (fast_tac (AC_cs addss AC_ss) 2); |
313 by (fast_tac (AC_cs addss AC_ss) 2); |
341 |
341 |
342 goal thy "!!f. [| domain(f`n) = succ(u); f : nat -> (UN n:nat. \ |
342 goal thy "!!f. [| domain(f`n) = succ(u); f : nat -> (UN n:nat. \ |
343 \ {f:succ(n)->domain(R). ALL k:n. <f`k, f`succ(k)> : R}); \ |
343 \ {f:succ(n)->domain(R). ALL k:n. <f`k, f`succ(k)> : R}); \ |
344 \ u=k; n:nat \ |
344 \ u=k; n:nat \ |
345 \ |] ==> f`n : succ(k) -> domain(R)"; |
345 \ |] ==> f`n : succ(k) -> domain(R)"; |
346 by (dresolve_tac [apply_type] 1 THEN (assume_tac 1)); |
346 by (dtac apply_type 1 THEN (assume_tac 1)); |
347 by (fast_tac (AC_cs addEs [UN_E, domain_eq_imp_fun_type]) 1); |
347 by (fast_tac (AC_cs addEs [UN_E, domain_eq_imp_fun_type]) 1); |
348 val f_n_type = result(); |
348 val f_n_type = result(); |
349 |
349 |
350 goal thy "!!f. [| f : nat -> (UN n:nat. \ |
350 goal thy "!!f. [| f : nat -> (UN n:nat. \ |
351 \ {f:succ(n)->domain(R). ALL k:n. <f`k, f`succ(k)> : R}); \ |
351 \ {f:succ(n)->domain(R). ALL k:n. <f`k, f`succ(k)> : R}); \ |
352 \ domain(f`n) = succ(k); n:nat \ |
352 \ domain(f`n) = succ(k); n:nat \ |
353 \ |] ==> ALL i:k. <f`n`i, f`n`succ(i)> : R"; |
353 \ |] ==> ALL i:k. <f`n`i, f`n`succ(i)> : R"; |
354 by (dresolve_tac [apply_type] 1 THEN (assume_tac 1)); |
354 by (dtac apply_type 1 THEN (assume_tac 1)); |
355 by (eresolve_tac [UN_E] 1); |
355 by (etac UN_E 1); |
356 by (eresolve_tac [CollectE] 1); |
356 by (etac CollectE 1); |
357 by (dresolve_tac [domain_of_fun RS sym RS trans] 1 THEN (assume_tac 1)); |
357 by (dresolve_tac [domain_of_fun RS sym RS trans] 1 THEN (assume_tac 1)); |
358 by (dresolve_tac [succ_eqD] 1); |
358 by (dtac succ_eqD 1); |
359 by (asm_full_simp_tac AC_ss 1); |
359 by (asm_full_simp_tac AC_ss 1); |
360 val f_n_pairs_in_R = result(); |
360 val f_n_pairs_in_R = result(); |
361 |
361 |
362 goalw thy [restrict_def] |
362 goalw thy [restrict_def] |
363 "!!f. [| restrict(f, domain(x))=x; f:n->X; domain(x) <= n \ |
363 "!!f. [| restrict(f, domain(x))=x; f:n->X; domain(x) <= n \ |
364 \ |] ==> restrict(cons(<n, y>, f), domain(x)) = x"; |
364 \ |] ==> restrict(cons(<n, y>, f), domain(x)) = x"; |
365 by (eresolve_tac [sym RS trans RS sym] 1); |
365 by (eresolve_tac [sym RS trans RS sym] 1); |
366 by (resolve_tac [fun_extension] 1); |
366 by (rtac fun_extension 1); |
367 by (fast_tac (AC_cs addSIs [lam_type]) 1); |
367 by (fast_tac (AC_cs addSIs [lam_type]) 1); |
368 by (fast_tac (AC_cs addSIs [lam_type]) 1); |
368 by (fast_tac (AC_cs addSIs [lam_type]) 1); |
369 by (asm_full_simp_tac (AC_ss addsimps [subsetD RS cons_val_k]) 1); |
369 by (asm_full_simp_tac (AC_ss addsimps [subsetD RS cons_val_k]) 1); |
370 val restrict_cons_eq_restrict = result(); |
370 val restrict_cons_eq_restrict = result(); |
371 |
371 |
373 \ f : nat -> (UN n:nat. \ |
373 \ f : nat -> (UN n:nat. \ |
374 \ {f:succ(n)->domain(R). ALL k:n. <f`k, f`succ(k)> : R}); \ |
374 \ {f:succ(n)->domain(R). ALL k:n. <f`k, f`succ(k)> : R}); \ |
375 \ n:nat; domain(f`n) = succ(n); \ |
375 \ n:nat; domain(f`n) = succ(n); \ |
376 \ (UN x:f``n. domain(x)) <= n |] \ |
376 \ (UN x:f``n. domain(x)) <= n |] \ |
377 \ ==> ALL x:f``succ(n). restrict(cons(<succ(n),y>, f`n), domain(x))=x"; |
377 \ ==> ALL x:f``succ(n). restrict(cons(<succ(n),y>, f`n), domain(x))=x"; |
378 by (resolve_tac [ballI] 1); |
378 by (rtac ballI 1); |
379 by (asm_full_simp_tac (AC_ss addsimps [image_fun_succ]) 1); |
379 by (asm_full_simp_tac (AC_ss addsimps [image_fun_succ]) 1); |
380 by (dresolve_tac [f_n_type] 1 THEN REPEAT (ares_tac [refl] 1)); |
380 by (dtac f_n_type 1 THEN REPEAT (ares_tac [refl] 1)); |
381 by (eresolve_tac [consE] 1); |
381 by (etac consE 1); |
382 by (asm_full_simp_tac (AC_ss addsimps [domain_of_fun, restrict_cons_eq]) 1); |
382 by (asm_full_simp_tac (AC_ss addsimps [domain_of_fun, restrict_cons_eq]) 1); |
383 by (dresolve_tac [bspec] 1 THEN (assume_tac 1)); |
383 by (dtac bspec 1 THEN (assume_tac 1)); |
384 by (fast_tac (AC_cs addSEs [restrict_cons_eq_restrict]) 1); |
384 by (fast_tac (AC_cs addSEs [restrict_cons_eq_restrict]) 1); |
385 val all_in_image_restrict_eq = result(); |
385 val all_in_image_restrict_eq = result(); |
386 |
386 |
387 goal thy "!!X. [| ALL b<nat. <f``b, f`b> : \ |
387 goal thy "!!X. [| ALL b<nat. <f``b, f`b> : \ |
388 \ {z:Fin(XX)*XX. (domain(snd(z))=succ(UN f:fst(z). domain(f)) \ |
388 \ {z:Fin(XX)*XX. (domain(snd(z))=succ(UN f:fst(z). domain(f)) \ |
394 \ f: nat -> XX; range(R) <= domain(R); x:domain(R) \ |
394 \ f: nat -> XX; range(R) <= domain(R); x:domain(R) \ |
395 \ |] ==> ALL b<nat. <f``b, f`b> : \ |
395 \ |] ==> ALL b<nat. <f``b, f`b> : \ |
396 \ {z:Fin(XX)*XX. (domain(snd(z))=succ(UN f:fst(z). domain(f)) \ |
396 \ {z:Fin(XX)*XX. (domain(snd(z))=succ(UN f:fst(z). domain(f)) \ |
397 \ & (UN f:fst(z). domain(f)) = b \ |
397 \ & (UN f:fst(z). domain(f)) = b \ |
398 \ & (ALL f:fst(z). restrict(snd(z), domain(f)) = f))}"; |
398 \ & (ALL f:fst(z). restrict(snd(z), domain(f)) = f))}"; |
399 by (resolve_tac [oallI] 1); |
399 by (rtac oallI 1); |
400 by (dresolve_tac [ltD] 1); |
400 by (dtac ltD 1); |
401 by (eresolve_tac [nat_induct] 1); |
401 by (etac nat_induct 1); |
402 by (dresolve_tac [[nat_0I, Ord_nat] MRS ltI RSN (2, ospec)] 1); |
402 by (dresolve_tac [[nat_0I, Ord_nat] MRS ltI RSN (2, ospec)] 1); |
403 by (fast_tac (FOL_cs addss |
403 by (fast_tac (FOL_cs addss |
404 (ZF_ss addsimps [image_0, singleton_fun RS domain_of_fun, |
404 (ZF_ss addsimps [image_0, singleton_fun RS domain_of_fun, |
405 [lepoll_refl, succI1] MRS lepoll_1_is_sing, singleton_in_funs])) 1); |
405 [lepoll_refl, succI1] MRS lepoll_1_is_sing, singleton_in_funs])) 1); |
406 by (dresolve_tac [[nat_succI, Ord_nat] MRS ltI RSN (2, ospec)] 1 |
406 by (dresolve_tac [[nat_succI, Ord_nat] MRS ltI RSN (2, ospec)] 1 |
407 THEN (assume_tac 1)); |
407 THEN (assume_tac 1)); |
408 by (REPEAT (eresolve_tac [conjE, CollectE, disjE] 1)); |
408 by (REPEAT (eresolve_tac [conjE, CollectE, disjE] 1)); |
409 by (fast_tac (FOL_cs addSEs [trans, subst_context] |
409 by (fast_tac (FOL_cs addSEs [trans, subst_context] |
410 addSIs [UN_image_succ_eq_succ] addss AC_ss) 1); |
410 addSIs [UN_image_succ_eq_succ] addss AC_ss) 1); |
411 by (eresolve_tac [conjE] 1); |
411 by (etac conjE 1); |
412 by (eresolve_tac [notE] 1); |
412 by (etac notE 1); |
413 by (asm_full_simp_tac (AC_ss addsimps [UN_image_succ_eq_succ]) 1); |
413 by (asm_full_simp_tac (AC_ss addsimps [UN_image_succ_eq_succ]) 1); |
414 by (eresolve_tac [conjE] 1); |
414 by (etac conjE 1); |
415 by (dresolve_tac [apply_UN_type] 1 THEN REPEAT (assume_tac 1)); |
415 by (dtac apply_UN_type 1 THEN REPEAT (assume_tac 1)); |
416 by (eresolve_tac [domainE] 1); |
416 by (etac domainE 1); |
417 by (eresolve_tac [domainE] 1); |
417 by (etac domainE 1); |
418 by (forward_tac [f_n_type] 1 THEN REPEAT (assume_tac 1)); |
418 by (forward_tac [f_n_type] 1 THEN REPEAT (assume_tac 1)); |
419 by (res_inst_tac [("x","cons(<succ(xa), ya>, f`xa)")] bexI 1); |
419 by (res_inst_tac [("x","cons(<succ(xa), ya>, f`xa)")] bexI 1); |
420 by (fast_tac (FOL_cs |
420 by (fast_tac (FOL_cs |
421 addEs [subst_context RSN (2, trans) RS domain_cons_eq_succ, |
421 addEs [subst_context RSN (2, trans) RS domain_cons_eq_succ, |
422 subst_context, all_in_image_restrict_eq, trans, equalityD1]) 1); |
422 subst_context, all_in_image_restrict_eq, trans, equalityD1]) 1); |
423 by (resolve_tac [UN_I] 1); |
423 by (rtac UN_I 1); |
424 by (eresolve_tac [nat_succI] 1); |
424 by (etac nat_succI 1); |
425 by (resolve_tac [CollectI] 1); |
425 by (rtac CollectI 1); |
426 by (eresolve_tac [rangeI RSN (2, subsetD) RSN (2, cons_fun_type2)] 1 |
426 by (eresolve_tac [rangeI RSN (2, subsetD) RSN (2, cons_fun_type2)] 1 |
427 THEN REPEAT (assume_tac 1)); |
427 THEN REPEAT (assume_tac 1)); |
428 by (resolve_tac [ballI] 1); |
428 by (rtac ballI 1); |
429 by (eresolve_tac [succE] 1); |
429 by (etac succE 1); |
430 by (asm_full_simp_tac (AC_ss addsimps [cons_val_n, cons_val_k]) 1); |
430 by (asm_full_simp_tac (AC_ss addsimps [cons_val_n, cons_val_k]) 1); |
431 by (dresolve_tac [domain_of_fun RSN (2, f_n_pairs_in_R)] 1 |
431 by (dresolve_tac [domain_of_fun RSN (2, f_n_pairs_in_R)] 1 |
432 THEN REPEAT (assume_tac 1)); |
432 THEN REPEAT (assume_tac 1)); |
433 by (dresolve_tac [bspec] 1 THEN (assume_tac 1)); |
433 by (dtac bspec 1 THEN (assume_tac 1)); |
434 by (asm_full_simp_tac (AC_ss |
434 by (asm_full_simp_tac (AC_ss |
435 addsimps [nat_into_Ord RS succ_in_succ, succI2, cons_val_k]) 1); |
435 addsimps [nat_into_Ord RS succ_in_succ, succI2, cons_val_k]) 1); |
436 val simplify_recursion = result(); |
436 val simplify_recursion = result(); |
437 |
437 |
438 goal thy "!!X. [| XX = (UN n:nat. \ |
438 goal thy "!!X. [| XX = (UN n:nat. \ |
442 \ & (UN f:fst(z). domain(f)) = b \ |
442 \ & (UN f:fst(z). domain(f)) = b \ |
443 \ & (ALL f:fst(z). restrict(snd(z), domain(f)) = f))}; \ |
443 \ & (ALL f:fst(z). restrict(snd(z), domain(f)) = f))}; \ |
444 \ f: nat -> XX; range(R) <= domain(R); x:domain(R); n:nat \ |
444 \ f: nat -> XX; range(R) <= domain(R); x:domain(R); n:nat \ |
445 \ |] ==> f`n : succ(n) -> domain(R) \ |
445 \ |] ==> f`n : succ(n) -> domain(R) \ |
446 \ & (ALL i:n. <f`n`i, f`n`succ(i)>:R)"; |
446 \ & (ALL i:n. <f`n`i, f`n`succ(i)>:R)"; |
447 by (dresolve_tac [ospec] 1); |
447 by (dtac ospec 1); |
448 by (eresolve_tac [Ord_nat RSN (2, ltI)] 1); |
448 by (eresolve_tac [Ord_nat RSN (2, ltI)] 1); |
449 by (eresolve_tac [CollectE] 1); |
449 by (etac CollectE 1); |
450 by (asm_full_simp_tac AC_ss 1); |
450 by (asm_full_simp_tac AC_ss 1); |
451 by (resolve_tac [conjI] 1); |
451 by (rtac conjI 1); |
452 by (fast_tac (AC_cs |
452 by (fast_tac (AC_cs |
453 addSEs [trans RS domain_eq_imp_fun_type, subst_context]) 1); |
453 addSEs [trans RS domain_eq_imp_fun_type, subst_context]) 1); |
454 by (fast_tac (FOL_cs |
454 by (fast_tac (FOL_cs |
455 addSEs [conjE, f_n_pairs_in_R, trans, subst_context]) 1); |
455 addSEs [conjE, f_n_pairs_in_R, trans, subst_context]) 1); |
456 val lemma2 = result(); |
456 val lemma2 = result(); |
466 by (forward_tac [lemma2 RS conjunct1 RS domain_of_fun] 1 |
466 by (forward_tac [lemma2 RS conjunct1 RS domain_of_fun] 1 |
467 THEN REPEAT (assume_tac 1)); |
467 THEN REPEAT (assume_tac 1)); |
468 by (dresolve_tac [[nat_succI, Ord_nat] MRS ltI RSN (2, ospec)] 1 |
468 by (dresolve_tac [[nat_succI, Ord_nat] MRS ltI RSN (2, ospec)] 1 |
469 THEN (assume_tac 1)); |
469 THEN (assume_tac 1)); |
470 by (asm_full_simp_tac AC_ss 1); |
470 by (asm_full_simp_tac AC_ss 1); |
471 by (REPEAT (eresolve_tac [conjE] 1)); |
471 by (REPEAT (etac conjE 1)); |
472 by (eresolve_tac [ballE] 1); |
472 by (etac ballE 1); |
473 by (eresolve_tac [restrict_eq_imp_val_eq RS sym] 1); |
473 by (eresolve_tac [restrict_eq_imp_val_eq RS sym] 1); |
474 by (fast_tac (AC_cs addSEs [ssubst]) 1); |
474 by (fast_tac (AC_cs addSEs [ssubst]) 1); |
475 by (asm_full_simp_tac (AC_ss |
475 by (asm_full_simp_tac (AC_ss |
476 addsimps [[nat_succI, Ord_nat] MRS OrdmemD RSN (2, image_fun)]) 1); |
476 addsimps [[nat_succI, Ord_nat] MRS OrdmemD RSN (2, image_fun)]) 1); |
477 val lemma3 = result(); |
477 val lemma3 = result(); |
479 goalw thy [DC_def, DC0_def] "!!Z. DC(nat) ==> DC0"; |
479 goalw thy [DC_def, DC0_def] "!!Z. DC(nat) ==> DC0"; |
480 by (REPEAT (resolve_tac [allI, impI] 1)); |
480 by (REPEAT (resolve_tac [allI, impI] 1)); |
481 by (REPEAT (eresolve_tac [asm_rl, conjE, ex_in_domain RS exE, allE] 1)); |
481 by (REPEAT (eresolve_tac [asm_rl, conjE, ex_in_domain RS exE, allE] 1)); |
482 by (eresolve_tac [[refl, refl] MRS lemma1 RSN (2, impE)] 1 |
482 by (eresolve_tac [[refl, refl] MRS lemma1 RSN (2, impE)] 1 |
483 THEN REPEAT (assume_tac 1)); |
483 THEN REPEAT (assume_tac 1)); |
484 by (eresolve_tac [bexE] 1); |
484 by (etac bexE 1); |
485 by (dresolve_tac [refl RSN (2, simplify_recursion)] 1 |
485 by (dresolve_tac [refl RSN (2, simplify_recursion)] 1 |
486 THEN REPEAT (assume_tac 1)); |
486 THEN REPEAT (assume_tac 1)); |
487 by (res_inst_tac [("x","lam n:nat. f`n`n")] bexI 1); |
487 by (res_inst_tac [("x","lam n:nat. f`n`n")] bexI 1); |
488 by (resolve_tac [lam_type] 2); |
488 by (rtac lam_type 2); |
489 by (eresolve_tac [[refl RS lemma2 RS conjunct1, succI1] MRS apply_type] 2 |
489 by (eresolve_tac [[refl RS lemma2 RS conjunct1, succI1] MRS apply_type] 2 |
490 THEN REPEAT (assume_tac 2)); |
490 THEN REPEAT (assume_tac 2)); |
491 by (resolve_tac [ballI] 1); |
491 by (rtac ballI 1); |
492 by (forward_tac [refl RS (nat_succI RSN (6, lemma2)) RS conjunct2] 1 |
492 by (forward_tac [refl RS (nat_succI RSN (6, lemma2)) RS conjunct2] 1 |
493 THEN REPEAT (assume_tac 1)); |
493 THEN REPEAT (assume_tac 1)); |
494 by (dresolve_tac [refl RS lemma3] 1 THEN REPEAT (assume_tac 1)); |
494 by (dresolve_tac [refl RS lemma3] 1 THEN REPEAT (assume_tac 1)); |
495 by (asm_full_simp_tac (AC_ss addsimps [nat_succI]) 1); |
495 by (asm_full_simp_tac (AC_ss addsimps [nat_succI]) 1); |
496 qed "DC_nat_DC0"; |
496 qed "DC_nat_DC0"; |
520 by (fast_tac (AC_cs addSEs [image_fun RS ssubst]) 1); |
520 by (fast_tac (AC_cs addSEs [image_fun RS ssubst]) 1); |
521 val value_in_image = result(); |
521 val value_in_image = result(); |
522 |
522 |
523 goalw thy [DC_def, WO3_def] |
523 goalw thy [DC_def, WO3_def] |
524 "!!Z. ALL K. Card(K) --> DC(K) ==> WO3"; |
524 "!!Z. ALL K. Card(K) --> DC(K) ==> WO3"; |
525 by (resolve_tac [allI] 1); |
525 by (rtac allI 1); |
526 by (excluded_middle_tac "A lesspoll Hartog(A)" 1); |
526 by (excluded_middle_tac "A lesspoll Hartog(A)" 1); |
527 by (fast_tac (AC_cs addSDs [lesspoll_imp_ex_lt_eqpoll] |
527 by (fast_tac (AC_cs addSDs [lesspoll_imp_ex_lt_eqpoll] |
528 addSIs [Ord_Hartog, leI RS le_imp_subset]) 2); |
528 addSIs [Ord_Hartog, leI RS le_imp_subset]) 2); |
529 by (REPEAT (eresolve_tac [allE, impE] 1)); |
529 by (REPEAT (eresolve_tac [allE, impE] 1)); |
530 by (resolve_tac [Card_Hartog] 1); |
530 by (rtac Card_Hartog 1); |
531 by (eres_inst_tac [("x","A")] allE 1); |
531 by (eres_inst_tac [("x","A")] allE 1); |
532 by (eres_inst_tac [("x","{z:Pow(A)*A . fst(z) \ |
532 by (eres_inst_tac [("x","{z:Pow(A)*A . fst(z) \ |
533 \ lesspoll Hartog(A) & snd(z) ~: fst(z)}")] allE 1); |
533 \ lesspoll Hartog(A) & snd(z) ~: fst(z)}")] allE 1); |
534 by (asm_full_simp_tac AC_ss 1); |
534 by (asm_full_simp_tac AC_ss 1); |
535 by (eresolve_tac [impE] 1); |
535 by (etac impE 1); |
536 by (fast_tac (AC_cs addEs [lemma1 RS not_emptyE]) 1); |
536 by (fast_tac (AC_cs addEs [lemma1 RS not_emptyE]) 1); |
537 by (eresolve_tac [bexE] 1); |
537 by (etac bexE 1); |
538 by (resolve_tac [exI RS (lepoll_def RS (def_imp_iff RS iffD2)) |
538 by (resolve_tac [exI RS (lepoll_def RS (def_imp_iff RS iffD2)) |
539 RS (HartogI RS notE)] 1); |
539 RS (HartogI RS notE)] 1); |
540 by (resolve_tac [Ord_Hartog RSN (2, fun_Ord_inj)] 1 THEN (assume_tac 1)); |
540 by (resolve_tac [Ord_Hartog RSN (2, fun_Ord_inj)] 1 THEN (assume_tac 1)); |
541 by (dresolve_tac [Ord_Hartog RSN (2, OrdmemD) RSN (2, |
541 by (dresolve_tac [Ord_Hartog RSN (2, OrdmemD) RSN (2, |
542 ltD RSN (3, value_in_image))] 1 |
542 ltD RSN (3, value_in_image))] 1 |
549 (* WO1 ==> ALL K. Card(K) --> DC(K) *) |
549 (* WO1 ==> ALL K. Card(K) --> DC(K) *) |
550 (* ********************************************************************** *) |
550 (* ********************************************************************** *) |
551 |
551 |
552 goal thy |
552 goal thy |
553 "!!a. [| Ord(a); b:a |] ==> (lam x:a. P(x))``b = (lam x:b. P(x))``b"; |
553 "!!a. [| Ord(a); b:a |] ==> (lam x:a. P(x))``b = (lam x:b. P(x))``b"; |
554 by (resolve_tac [images_eq] 1); |
554 by (rtac images_eq 1); |
555 by (REPEAT (fast_tac (AC_cs addSEs [RepFunI, OrdmemD] |
555 by (REPEAT (fast_tac (AC_cs addSEs [RepFunI, OrdmemD] |
556 addSIs [lam_type]) 2)); |
556 addSIs [lam_type]) 2)); |
557 by (resolve_tac [ballI] 1); |
557 by (rtac ballI 1); |
558 by (dresolve_tac [OrdmemD RS subsetD] 1 |
558 by (dresolve_tac [OrdmemD RS subsetD] 1 |
559 THEN REPEAT (assume_tac 1)); |
559 THEN REPEAT (assume_tac 1)); |
560 by (asm_full_simp_tac AC_ss 1); |
560 by (asm_full_simp_tac AC_ss 1); |
561 val lam_images_eq = result(); |
561 val lam_images_eq = result(); |
562 |
562 |
580 \ ALL Y:Pow(X). Y lesspoll K --> (EX x:X. <Y, x> : R); b:K |] \ |
580 \ ALL Y:Pow(X). Y lesspoll K --> (EX x:X. <Y, x> : R); b:K |] \ |
581 \ ==> ff(b, X, Q, R) : {x:X. <(lam c:b. ff(c, X, Q, R))``b, x> : R}"; |
581 \ ==> ff(b, X, Q, R) : {x:X. <(lam c:b. ff(c, X, Q, R))``b, x> : R}"; |
582 by (res_inst_tac [("P","b:K")] impE 1 THEN TRYALL assume_tac); |
582 by (res_inst_tac [("P","b:K")] impE 1 THEN TRYALL assume_tac); |
583 by (res_inst_tac [("i","b")] (Card_is_Ord RS Ord_in_Ord RS trans_induct) 1 |
583 by (res_inst_tac [("i","b")] (Card_is_Ord RS Ord_in_Ord RS trans_induct) 1 |
584 THEN REPEAT (assume_tac 1)); |
584 THEN REPEAT (assume_tac 1)); |
585 by (resolve_tac [impI] 1); |
585 by (rtac impI 1); |
586 by (resolve_tac [ff_def RS def_transrec RS ssubst] 1); |
586 by (resolve_tac [ff_def RS def_transrec RS ssubst] 1); |
587 by (eresolve_tac [the_first_in] 1); |
587 by (etac the_first_in 1); |
588 by (fast_tac AC_cs 1); |
588 by (fast_tac AC_cs 1); |
589 by (asm_full_simp_tac (AC_ss |
589 by (asm_full_simp_tac (AC_ss |
590 addsimps [[lam_type_RepFun, subset_refl] MRS image_fun]) 1); |
590 addsimps [[lam_type_RepFun, subset_refl] MRS image_fun]) 1); |
591 by (eresolve_tac [lemma_] 1 THEN (assume_tac 1)); |
591 by (etac lemma_ 1 THEN (assume_tac 1)); |
592 by (fast_tac (AC_cs addSEs [RepFunE, impE, notE] |
592 by (fast_tac (AC_cs addSEs [RepFunE, impE, notE] |
593 addEs [Card_is_Ord RSN (2, OrdmemD) RS subsetD]) 1); |
593 addEs [Card_is_Ord RSN (2, OrdmemD) RS subsetD]) 1); |
594 by (fast_tac (AC_cs addSEs [[in_Card_imp_lesspoll, RepFun_lepoll] |
594 by (fast_tac (AC_cs addSEs [[in_Card_imp_lesspoll, RepFun_lepoll] |
595 MRS lepoll_lesspoll_lesspoll]) 1); |
595 MRS lepoll_lesspoll_lesspoll]) 1); |
596 val lemma = result(); |
596 val lemma = result(); |
598 goalw thy [DC_def, WO1_def] |
598 goalw thy [DC_def, WO1_def] |
599 "!!Z. WO1 ==> ALL K. Card(K) --> DC(K)"; |
599 "!!Z. WO1 ==> ALL K. Card(K) --> DC(K)"; |
600 by (REPEAT (resolve_tac [allI,impI] 1)); |
600 by (REPEAT (resolve_tac [allI,impI] 1)); |
601 by (REPEAT (eresolve_tac [allE,exE,conjE] 1)); |
601 by (REPEAT (eresolve_tac [allE,exE,conjE] 1)); |
602 by (res_inst_tac [("x","lam b:K. ff(b, X, Ra, R)")] bexI 1); |
602 by (res_inst_tac [("x","lam b:K. ff(b, X, Ra, R)")] bexI 1); |
603 by (resolve_tac [lam_type] 2); |
603 by (rtac lam_type 2); |
604 by (resolve_tac [lemma RS CollectD1] 2 THEN REPEAT (assume_tac 2)); |
604 by (resolve_tac [lemma RS CollectD1] 2 THEN REPEAT (assume_tac 2)); |
605 by (asm_full_simp_tac (AC_ss |
605 by (asm_full_simp_tac (AC_ss |
606 addsimps [[Card_is_Ord, ltD] MRS lam_images_eq]) 1); |
606 addsimps [[Card_is_Ord, ltD] MRS lam_images_eq]) 1); |
607 by (fast_tac (AC_cs addSEs [ltE, lemma RS CollectD2]) 1); |
607 by (fast_tac (AC_cs addSEs [ltE, lemma RS CollectD2]) 1); |
608 qed" WO1_DC_Card"; |
608 qed" WO1_DC_Card"; |