31 (* *) |
31 (* *) |
32 (* is the desired function. *) |
32 (* is the desired function. *) |
33 (* *) |
33 (* *) |
34 (* ********************************************************************** *) |
34 (* ********************************************************************** *) |
35 |
35 |
36 goal thy "{z:XX*XX. domain(snd(z))=succ(domain(fst(z))) \ |
36 goal thy "{<z1,z2>:XX*XX. domain(z2)=succ(domain(z1)) \ |
37 \ & restrict(snd(z), domain(fst(z))) = fst(z)} <= XX*XX"; |
37 \ & restrict(z2, domain(z1)) = z1} <= XX*XX"; |
38 by (fast_tac AC_cs 1); |
38 by (Fast_tac 1); |
39 val lemma1_1 = result(); |
39 val lemma1_1 = result(); |
40 |
40 |
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 \ ==> {<z1,z2>: (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(z2)=succ(domain(z1)) \ |
45 \ & restrict(snd(z), domain(fst(z))) = fst(z)} ~= 0"; |
45 \ & restrict(z2, domain(z1)) = z1} ~= 0"; |
46 by (etac 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 (etac 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 (rtac CollectI 1); |
51 by (rtac CollectI 1); |
52 by (rtac 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 (!claset 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 br (nat_1I RS UN_I) 1; |
55 addss (AC_ss addsimps [[lepoll_refl, succI1] MRS lepoll_1_is_sing, |
55 by (fast_tac (!claset addSIs [singleton_fun RS Pi_type] |
56 apply_singleton_eq, image_0])) 1); |
56 addss (!simpset addsimps [singleton_0 RS sym])) 1); |
57 by (asm_full_simp_tac (AC_ss addsimps [domain_0, restrict_0, domain_cons, |
57 by (asm_full_simp_tac (!simpset addsimps [domain_0, domain_cons, |
58 [lepoll_refl, succI1] MRS lepoll_1_is_sing]) 1); |
58 singleton_0]) 1); |
59 val lemma1_2 = result(); |
59 val lemma1_2 = result(); |
60 |
60 |
61 goal thy "!!X. ALL Y:Pow(X). Y lesspoll nat --> (EX x:X. <Y, x> : R) \ |
61 goal thy "!!X. ALL Y:Pow(X). Y lesspoll nat --> (EX x:X. <Y, x> : R) \ |
62 \ ==> range({z: (UN n:nat. {f:n->X. ALL k:n. <f``k, f`k> : R}) * \ |
62 \ ==> range({<z1,z2>: (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}). \ |
63 \ (UN n:nat. {f:n->X. ALL k:n. <f``k, f`k> : R}). \ |
64 \ domain(snd(z))=succ(domain(fst(z))) \ |
64 \ domain(z2)=succ(domain(z1)) \ |
65 \ & restrict(snd(z), domain(fst(z))) = fst(z)}) \ |
65 \ & restrict(z2, domain(z1)) = z1}) \ |
66 \ <= domain({z: (UN n:nat. {f:n->X. ALL k:n. <f``k, f`k> : R}) * \ |
66 \ <= domain({<z1,z2>: (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(z2)=succ(domain(z1)) \ |
69 \ & restrict(snd(z), domain(fst(z))) = fst(z)})"; |
69 \ & restrict(z2, domain(z1)) = z1})"; |
70 by (rtac range_subset_domain 1); |
70 by (rtac range_subset_domain 1); |
71 by (rtac subsetI 2); |
71 by (rtac subsetI 2); |
72 by (etac CollectD1 2); |
72 by (etac CollectD1 2); |
73 by (etac UN_E 1); |
73 by (etac UN_E 1); |
74 by (etac CollectE 1); |
74 by (etac CollectE 1); |
79 THEN REPEAT (assume_tac 1)); |
79 THEN REPEAT (assume_tac 1)); |
80 by (etac 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 (rtac CollectI 1); |
82 by (rtac CollectI 1); |
83 by (rtac SigmaI 1); |
83 by (rtac SigmaI 1); |
84 by (fast_tac AC_cs 1); |
84 by (Fast_tac 1); |
85 by (rtac UN_I 1); |
85 by (rtac UN_I 1); |
86 by (etac nat_succI 1); |
86 by (etac nat_succI 1); |
87 by (rtac CollectI 1); |
87 by (rtac CollectI 1); |
88 by (etac 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 (!claset addSEs [succE] addss (!simpset |
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 (!simpset |
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(); |
94 |
94 |
95 goal thy "!!X. [| XX = (UN n:nat. {f:n->X. ALL k:n. <f``k, f`k> : R}); \ |
95 goal thy "!!X. [| XX = (UN n:nat. {f:n->X. ALL k:n. <f``k, f`k> : R}); \ |
96 \ RR = {z:XX*XX. domain(snd(z))=succ(domain(fst(z))) \ |
96 \ RR = {<z1,z2>:XX*XX. domain(z2)=succ(domain(z1)) \ |
97 \ & restrict(snd(z), domain(fst(z))) = fst(z)}; \ |
97 \ & restrict(z2, domain(z1)) = z1}; \ |
98 \ ALL Y:Pow(X). Y lesspoll nat --> (EX x:X. <Y, x> : R) \ |
98 \ ALL Y:Pow(X). Y lesspoll nat --> (EX x:X. <Y, x> : R) \ |
99 \ |] ==> RR <= XX*XX & RR ~= 0 & range(RR) <= domain(RR)"; |
99 \ |] ==> RR <= XX*XX & RR ~= 0 & range(RR) <= domain(RR)"; |
100 by (fast_tac (AC_cs addSIs [lemma1_1] addSEs [lemma1_2, lemma1_3]) 1); |
100 by (fast_tac (!claset addSIs [lemma1_1] addSEs [lemma1_2, lemma1_3]) 1); |
101 val lemma1 = result(); |
101 val lemma1 = result(); |
102 |
102 |
103 goal thy "!!f. [| <f,g> : {z:XX*XX. \ |
103 goal thy |
104 \ domain(snd(z))=succ(domain(fst(z))) & Q(z)}; \ |
104 "!!X.[| XX = (UN n:nat. {f:n->X. ALL k:n. <f``k, f`k> : R}); \ |
105 \ XX = (UN n:nat. {f:n->X. ALL k:n. <f``k, f`k> : R}); f:k->X \ |
|
106 \ |] ==> g:succ(k)->X"; |
|
107 by (etac CollectE 1); |
|
108 by (dtac SigmaD2 1); |
|
109 by (hyp_subst_tac 1); |
|
110 by (etac UN_E 1); |
|
111 by (etac CollectE 1); |
|
112 by (asm_full_simp_tac AC_ss 1); |
|
113 by (dtac domain_of_fun 1); |
|
114 by (etac conjE 1); |
|
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}); \ |
|
120 \ ALL n:nat. <f`n, f`succ(n)> : \ |
105 \ ALL n:nat. <f`n, f`succ(n)> : \ |
121 \ {z:XX*XX. domain(snd(z))=succ(domain(fst(z))) \ |
106 \ {<z1,z2>:XX*XX. domain(z2)=succ(domain(z1)) \ |
122 \ & restrict(snd(z), domain(fst(z))) = fst(z)}; \ |
107 \ & restrict(z2, domain(z1)) = z1}; \ |
123 \ f: nat -> XX; n:nat \ |
108 \ f: nat -> XX; n:nat \ |
124 \ |] ==> EX k:nat. f`succ(n) : k -> X & n:k \ |
109 \ |] ==> EX k:nat. f`succ(n) : k -> X & n:k \ |
125 \ & <f`succ(n)``n, f`succ(n)`n> : R"; |
110 \ & <f`succ(n)``n, f`succ(n)`n> : R"; |
126 by (etac nat_induct 1); |
111 by (etac nat_induct 1); |
127 by (dresolve_tac [nat_1I RSN (2, apply_type)] 1); |
112 by (dresolve_tac [nat_1I RSN (2, apply_type)] 1); |
128 by (dresolve_tac [nat_0I RSN (2, bspec)] 1); |
113 by (dresolve_tac [nat_0I RSN (2, bspec)] 1); |
129 by (asm_full_simp_tac AC_ss 1); |
114 by (Asm_full_simp_tac 1); |
130 by (etac UN_E 1); |
115 by (Step_tac 1); |
131 by (etac CollectE 1); |
|
132 by (rtac bexI 1 THEN (assume_tac 2)); |
116 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)] |
117 by (best_tac (!claset addIs [ltD] |
134 addEs [sym RS trans RS succ_neq_0, domain_of_fun]) 1); |
118 addSEs [nat_0_le RS leE] |
135 by (etac bexE 1); |
119 addEs [sym RS trans RS succ_neq_0, domain_of_fun] |
|
120 addss (!simpset)) 1); |
|
121 (** LEVEL 7 **) |
136 by (dresolve_tac [nat_succI RSN (2, bspec)] 1 THEN (assume_tac 1)); |
122 by (dresolve_tac [nat_succI RSN (2, bspec)] 1 THEN (assume_tac 1)); |
137 by (etac conjE 1); |
123 by (subgoal_tac "f ` succ(succ(x)) : succ(k)->X" 1); |
138 by (dtac lemma2_1 1 THEN REPEAT (assume_tac 1)); |
|
139 by (hyp_subst_tac 1); |
|
140 by (dresolve_tac [nat_succI RS nat_succI RSN (2, apply_type)] 1 |
124 by (dresolve_tac [nat_succI RS nat_succI RSN (2, apply_type)] 1 |
141 THEN (assume_tac 1)); |
125 THEN (assume_tac 1)); |
142 by (etac UN_E 1); |
126 by (Full_simp_tac 1); |
143 by (etac CollectE 1); |
127 by (Step_tac 1); |
144 by (dresolve_tac [[domain_of_fun RS sym, domain_of_fun] MRS trans] 1 |
128 by (forw_inst_tac [("a","succ(k)")] (domain_of_fun RS sym RS trans) 1 THEN |
145 THEN (assume_tac 1)); |
129 (assume_tac 1)); |
146 by (fast_tac (AC_cs addSEs [nat_succI, nat_into_Ord RS succ_in_succ] |
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] |
147 addSDs [nat_into_Ord RS succ_in_succ RSN (2, bspec)]) 1); |
133 addSDs [nat_into_Ord RS succ_in_succ RSN (2, bspec)]) 1); |
|
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); |
148 val lemma2 = result(); |
137 val lemma2 = result(); |
149 |
138 |
150 goal thy "!!X. [| XX = (UN n:nat. {f:n->X. ALL k:n. <f``k, f`k> : R}); \ |
139 goal thy |
|
140 "!!X.[| XX = (UN n:nat. {f:n->X. ALL k:n. <f``k, f`k> : R}); \ |
151 \ ALL n:nat. <f`n, f`succ(n)> : \ |
141 \ ALL n:nat. <f`n, f`succ(n)> : \ |
152 \ {z:XX*XX. domain(snd(z))=succ(domain(fst(z))) \ |
142 \ {<z1,z2>:XX*XX. domain(z2)=succ(domain(z1)) \ |
153 \ & restrict(snd(z), domain(fst(z))) = fst(z)}; \ |
143 \ & restrict(z2, domain(z1)) = z1}; \ |
154 \ f: nat -> XX; n:nat \ |
144 \ f: nat -> XX; n:nat \ |
155 \ |] ==> ALL x:n. f`succ(n)`x = f`succ(x)`x"; |
145 \ |] ==> ALL x:n. f`succ(n)`x = f`succ(x)`x"; |
156 by (etac nat_induct 1); |
146 by (etac nat_induct 1); |
157 by (fast_tac AC_cs 1); |
147 by (Fast_tac 1); |
158 by (rtac ballI 1); |
148 by (rtac ballI 1); |
159 by (etac succE 1); |
149 by (etac succE 1); |
160 by (rtac restrict_eq_imp_val_eq 1); |
150 by (rtac restrict_eq_imp_val_eq 1); |
161 by (dresolve_tac [nat_succI RSN (2, bspec)] 1 THEN (assume_tac 1)); |
151 by (dresolve_tac [nat_succI RSN (2, bspec)] 1 THEN (assume_tac 1)); |
162 by (asm_full_simp_tac AC_ss 1); |
152 by (Asm_full_simp_tac 1); |
163 by (dtac lemma2 1 THEN REPEAT (assume_tac 1)); |
153 by (dtac lemma2 1 THEN REPEAT (assume_tac 1)); |
164 by (fast_tac (AC_cs addSDs [domain_of_fun]) 1); |
154 by (fast_tac (!claset addSDs [domain_of_fun]) 1); |
165 by (dres_inst_tac [("x","xa")] bspec 1 THEN (assume_tac 1)); |
155 by (dres_inst_tac [("x","xa")] bspec 1 THEN (assume_tac 1)); |
166 by (eresolve_tac [sym RS trans RS sym] 1); |
156 by (eresolve_tac [sym RS trans RS sym] 1); |
167 by (resolve_tac [restrict_eq_imp_val_eq RS sym] 1); |
157 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)); |
158 by (dresolve_tac [nat_succI RSN (2, bspec)] 1 THEN (assume_tac 1)); |
169 by (asm_full_simp_tac AC_ss 1); |
159 by (Asm_full_simp_tac 1); |
170 by (dtac lemma2 1 THEN REPEAT (assume_tac 1)); |
160 by (dtac lemma2 1 THEN REPEAT (assume_tac 1)); |
171 by (fast_tac (FOL_cs addSDs [domain_of_fun] |
161 by (fast_tac (FOL_cs addSDs [domain_of_fun] |
172 addSEs [bexE, nat_into_Ord RSN (2, OrdmemD) RS subsetD]) 1); |
162 addSEs [bexE, nat_into_Ord RSN (2, OrdmemD) RS subsetD]) 1); |
173 val lemma3_1 = result(); |
163 val lemma3_1 = result(); |
174 |
164 |
175 goal thy "!!n. ALL x:n. f`succ(n)`x = f`succ(x)`x \ |
165 goal thy "!!n. ALL x:n. f`succ(n)`x = f`succ(x)`x \ |
176 \ ==> {f`succ(x)`x. x:n} = {f`succ(n)`x. x:n}"; |
166 \ ==> {f`succ(x)`x. x:n} = {f`succ(n)`x. x:n}"; |
177 by (asm_full_simp_tac AC_ss 1); |
167 by (Asm_full_simp_tac 1); |
178 val lemma3_2 = result(); |
168 val lemma3_2 = result(); |
179 |
169 |
180 goal thy "!!X. [| XX = (UN n:nat. {f:n->X. ALL k:n. <f``k, f`k> : R}); \ |
170 goal thy "!!X. [| XX = (UN n:nat. {f:n->X. ALL k:n. <f``k, f`k> : R}); \ |
181 \ ALL n:nat. <f`n, f`succ(n)> : \ |
171 \ ALL n:nat. <f`n, f`succ(n)> : \ |
182 \ {z:XX*XX. domain(snd(z))=succ(domain(fst(z))) \ |
172 \ {<z1,z2>:XX*XX. domain(z2)=succ(domain(z1)) \ |
183 \ & restrict(snd(z), domain(fst(z))) = fst(z)}; \ |
173 \ & restrict(z2, domain(z1)) = z1}; \ |
184 \ f: nat -> XX; n:nat \ |
174 \ f: nat -> XX; n:nat \ |
185 \ |] ==> (lam x:nat. f`succ(x)`x) `` n = f`succ(n)``n"; |
175 \ |] ==> (lam x:nat. f`succ(x)`x) `` n = f`succ(n)``n"; |
186 by (etac natE 1); |
176 by (etac natE 1); |
187 by (asm_full_simp_tac (AC_ss addsimps [image_0]) 1); |
177 by (asm_full_simp_tac (!simpset addsimps [image_0]) 1); |
188 by (resolve_tac [image_lam RS ssubst] 1); |
178 by (resolve_tac [image_lam RS ssubst] 1); |
189 by (fast_tac (AC_cs addSEs [[nat_succI, Ord_nat] MRS OrdmemD]) 1); |
179 by (fast_tac (!claset addSEs [[nat_succI, Ord_nat] MRS OrdmemD]) 1); |
190 by (resolve_tac [lemma3_1 RS lemma3_2 RS ssubst] 1 |
180 by (resolve_tac [lemma3_1 RS lemma3_2 RS ssubst] 1 |
191 THEN REPEAT (assume_tac 1)); |
181 THEN REPEAT (assume_tac 1)); |
192 by (fast_tac (AC_cs addSEs [nat_succI]) 1); |
182 by (fast_tac (!claset addSEs [nat_succI]) 1); |
193 by (dresolve_tac [nat_succI RSN (4, lemma2)] 1 |
183 by (dresolve_tac [nat_succI RSN (4, lemma2)] 1 |
194 THEN REPEAT (assume_tac 1)); |
184 THEN REPEAT (assume_tac 1)); |
195 by (fast_tac (AC_cs addSEs [nat_into_Ord RSN (2, OrdmemD) RSN |
185 by (fast_tac (!claset addSEs [nat_into_Ord RSN (2, OrdmemD) RSN |
196 (2, image_fun RS sym)]) 1); |
186 (2, image_fun RS sym)]) 1); |
197 val lemma3 = result(); |
187 val lemma3 = result(); |
198 |
188 |
199 goal thy "!!f. [| f:A->B; B<=C |] ==> f:A->C"; |
189 goal thy "!!f. [| f:A->B; B<=C |] ==> f:A->C"; |
200 by (rtac Pi_type 1 THEN (assume_tac 1)); |
190 by (rtac Pi_type 1 THEN (assume_tac 1)); |
201 by (fast_tac (AC_cs addSEs [apply_type]) 1); |
191 by (fast_tac (!claset addSEs [apply_type]) 1); |
202 val fun_type_gen = result(); |
192 val fun_type_gen = result(); |
203 |
193 |
204 goalw thy [DC_def, DC0_def] "!!Z. DC0 ==> DC(nat)"; |
194 goalw thy [DC_def, DC0_def] "!!Z. DC0 ==> DC(nat)"; |
205 by (REPEAT (resolve_tac [allI, impI] 1)); |
195 by (REPEAT (resolve_tac [allI, impI] 1)); |
206 by (REPEAT (eresolve_tac [conjE, allE] 1)); |
196 by (REPEAT (eresolve_tac [conjE, allE] 1)); |
207 by (eresolve_tac [[refl, refl] MRS lemma1 RSN (2, impE)] 1 |
197 by (eresolve_tac [[refl, refl] MRS lemma1 RSN (2, impE)] 1 |
208 THEN (assume_tac 1)); |
198 THEN (assume_tac 1)); |
209 by (etac bexE 1); |
199 by (etac bexE 1); |
210 by (res_inst_tac [("x","lam n:nat. f`succ(n)`n")] bexI 1); |
200 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] |
201 by (fast_tac (!claset addSIs [lam_type] addSDs [refl RS lemma2] |
212 addSEs [fun_type_gen, apply_type]) 2); |
202 addSEs [fun_type_gen, apply_type]) 2); |
213 by (rtac oallI 1); |
203 by (rtac oallI 1); |
214 by (forward_tac [ltD RSN (3, refl RS lemma2)] 1 |
204 by (forward_tac [ltD RSN (3, refl RS lemma2)] 1 |
215 THEN assume_tac 2); |
205 THEN assume_tac 2); |
216 by (fast_tac (AC_cs addSEs [fun_type_gen]) 1); |
206 by (fast_tac (!claset addSEs [fun_type_gen]) 1); |
217 by (eresolve_tac [ltD RSN (3, refl RS lemma3) RS ssubst] 1 |
207 by (eresolve_tac [ltD RSN (3, refl RS lemma3) RS ssubst] 1 |
218 THEN assume_tac 2); |
208 THEN assume_tac 2); |
219 by (fast_tac (AC_cs addSEs [fun_type_gen]) 1); |
209 by (fast_tac (!claset addSEs [fun_type_gen]) 1); |
220 by (fast_tac (AC_cs addss AC_ss) 1); |
210 by (fast_tac (!claset addss (!simpset)) 1); |
221 qed "DC0_DC_nat"; |
211 qed "DC0_DC_nat"; |
222 |
212 |
223 (* ********************************************************************** *) |
213 (* ********************************************************************** *) |
224 (* DC(omega) ==> DC *) |
214 (* DC(omega) ==> DC *) |
225 (* *) |
215 (* *) |
250 (* *) |
240 (* *) |
251 (* ********************************************************************** *) |
241 (* ********************************************************************** *) |
252 |
242 |
253 goalw thy [lesspoll_def, Finite_def] |
243 goalw thy [lesspoll_def, Finite_def] |
254 "!!A. A lesspoll nat ==> Finite(A)"; |
244 "!!A. A lesspoll nat ==> Finite(A)"; |
255 by (fast_tac (AC_cs addSDs [ltD, lepoll_imp_ex_le_eqpoll] |
245 by (fast_tac (!claset addSDs [ltD, lepoll_imp_ex_le_eqpoll] |
256 addSIs [Ord_nat]) 1); |
246 addSIs [Ord_nat]) 1); |
257 val lesspoll_nat_is_Finite = result(); |
247 val lesspoll_nat_is_Finite = result(); |
258 |
248 |
259 goal thy "!!n. n:nat ==> ALL A. (A eqpoll n & A <= X) --> A : Fin(X)"; |
249 goal thy "!!n. n:nat ==> ALL A. (A eqpoll n & A <= X) --> A : Fin(X)"; |
260 by (etac nat_induct 1); |
250 by (etac nat_induct 1); |
261 by (rtac allI 1); |
251 by (rtac allI 1); |
262 by (fast_tac (AC_cs addSIs [Fin.emptyI] |
252 by (fast_tac (!claset addSIs [Fin.emptyI] |
263 addSDs [eqpoll_imp_lepoll RS lepoll_0_is_0]) 1); |
253 addSDs [eqpoll_imp_lepoll RS lepoll_0_is_0]) 1); |
264 by (rtac allI 1); |
254 by (rtac allI 1); |
265 by (rtac impI 1); |
255 by (rtac impI 1); |
266 by (etac conjE 1); |
256 by (etac conjE 1); |
267 by (resolve_tac [eqpoll_succ_imp_not_empty RS not_emptyE] 1 |
257 by (resolve_tac [eqpoll_succ_imp_not_empty RS not_emptyE] 1 |
268 THEN (assume_tac 1)); |
258 THEN (assume_tac 1)); |
269 by (forward_tac [Diff_sing_eqpoll] 1 THEN (assume_tac 1)); |
259 by (forward_tac [Diff_sing_eqpoll] 1 THEN (assume_tac 1)); |
270 by (etac allE 1); |
260 by (etac allE 1); |
271 by (etac impE 1); |
261 by (etac impE 1); |
272 by (fast_tac AC_cs 1); |
262 by (Fast_tac 1); |
273 by (dtac subsetD 1 THEN (assume_tac 1)); |
263 by (dtac subsetD 1 THEN (assume_tac 1)); |
274 by (dresolve_tac [Fin.consI] 1 THEN (assume_tac 1)); |
264 by (dresolve_tac [Fin.consI] 1 THEN (assume_tac 1)); |
275 by (asm_full_simp_tac (AC_ss addsimps [cons_Diff]) 1); |
265 by (asm_full_simp_tac (!simpset addsimps [cons_Diff]) 1); |
276 val Finite_Fin_lemma = result(); |
266 val Finite_Fin_lemma = result(); |
277 |
267 |
278 goalw thy [Finite_def] "!!A. [| Finite(A); A <= X |] ==> A : Fin(X)"; |
268 goalw thy [Finite_def] "!!A. [| Finite(A); A <= X |] ==> A : Fin(X)"; |
279 by (etac bexE 1); |
269 by (etac bexE 1); |
280 by (dtac Finite_Fin_lemma 1); |
270 by (dtac Finite_Fin_lemma 1); |
281 by (etac allE 1); |
271 by (etac allE 1); |
282 by (etac impE 1); |
272 by (etac impE 1); |
283 by (assume_tac 2); |
273 by (assume_tac 2); |
284 by (fast_tac AC_cs 1); |
274 by (Fast_tac 1); |
285 val Finite_Fin = result(); |
275 val Finite_Fin = result(); |
286 |
276 |
287 goal thy "!!x. x: X ==> {<0,x>}: (UN n:nat. \ |
277 goal thy "!!x. x: X \ |
288 \ {f:succ(n)->X. ALL k:n. <f`k, f`succ(k)> : R})"; |
278 \ ==> {<0,x>}: (UN n:nat. {f:succ(n)->X. ALL k:n. <f`k, f`succ(k)> : R})"; |
289 by (fast_tac (AC_cs addSIs [nat_0I RS UN_I, singleton_fun RS Pi_type] |
279 br (nat_0I RS UN_I) 1; |
290 addss (AC_ss addsimps [[lepoll_refl, succI1] MRS lepoll_1_is_sing, |
280 by (fast_tac (!claset addSIs [singleton_fun RS Pi_type] |
291 apply_singleton_eq])) 1); |
281 addss (!simpset addsimps [singleton_0 RS sym])) 1); |
292 val singleton_in_funs = result(); |
282 val singleton_in_funs = result(); |
293 |
283 |
294 goal thy |
284 goal thy |
295 "!!X. [| XX = (UN n:nat. \ |
285 "!!X. [| XX = (UN n:nat. \ |
296 \ {f:succ(n)->domain(R). ALL k:n. <f`k, f`succ(k)> : R}); \ |
286 \ {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)) \ |
287 \ RR = {<z1,z2>:Fin(XX)*XX. (domain(z2)=succ(UN f:z1. domain(f)) \ |
298 \ & (ALL f:fst(z). restrict(snd(z), domain(f)) = f)) | \ |
288 \ & (ALL f:z1. restrict(z2, domain(f)) = f)) | \ |
299 \ (~ (EX g:XX. domain(g)=succ(UN f:fst(z). domain(f)) \ |
289 \ (~ (EX g:XX. domain(g)=succ(UN f:z1. domain(f)) \ |
300 \ & (ALL f:fst(z). restrict(g, domain(f)) = f)) & snd(z)={<0,x>})}; \ |
290 \ & (ALL f:z1. restrict(g, domain(f)) = f)) & z2={<0,x>})}; \ |
301 \ range(R) <= domain(R); x:domain(R) \ |
291 \ range(R) <= domain(R); x:domain(R) \ |
302 \ |] ==> RR <= Pow(XX)*XX & \ |
292 \ |] ==> RR <= Pow(XX)*XX & \ |
303 \ (ALL Y:Pow(XX). Y lesspoll nat --> (EX x:XX. <Y,x>:RR))"; |
293 \ (ALL Y:Pow(XX). Y lesspoll nat --> (EX x:XX. <Y,x>:RR))"; |
304 by (rtac conjI 1); |
294 by (rtac conjI 1); |
305 by (deepen_tac (ZF_cs addSEs [FinD RS PowI]) 0 1); |
295 by (deepen_tac (!claset addSEs [FinD RS PowI]) 0 1); |
306 by (rtac ballI 1); |
296 by (rtac ballI 1); |
307 by (rtac impI 1); |
297 by (rtac impI 1); |
308 by (dresolve_tac [[lesspoll_nat_is_Finite, PowD] MRS Finite_Fin] 1 |
298 by (dresolve_tac [[lesspoll_nat_is_Finite, PowD] MRS Finite_Fin] 1 |
309 THEN (assume_tac 1)); |
299 THEN (assume_tac 1)); |
310 by (excluded_middle_tac "EX g:XX. domain(g)=succ(UN f:Y. domain(f)) \ |
300 by (excluded_middle_tac "EX g:XX. domain(g)=succ(UN f:Y. domain(f)) \ |
311 \ & (ALL f:Y. restrict(g, domain(f)) = f)" 1); |
301 \ & (ALL f:Y. restrict(g, domain(f)) = f)" 1); |
312 by (fast_tac (AC_cs addss AC_ss) 2); |
302 by (fast_tac (!claset addss (!simpset)) 2); |
313 by (fast_tac (FOL_cs addSEs [CollectE, singleton_in_funs] |
303 by (step_tac (!claset delrules [domainE]) 1); |
314 addSIs [SigmaI] addIs [bexI] addss AC_ss) 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); |
315 val lemma1 = result(); |
307 val lemma1 = result(); |
316 |
308 |
317 goal thy "!!f. [| f:nat->X; n:nat |] ==> \ |
309 goal thy "!!f. [| f:nat->X; n:nat |] ==> \ |
318 \ (UN x:f``succ(n). P(x)) = P(f`n) Un (UN x:f``n. P(x))"; |
310 \ (UN x:f``succ(n). P(x)) = P(f`n) Un (UN x:f``n. P(x))"; |
319 by (asm_full_simp_tac (AC_ss |
311 by (asm_full_simp_tac (!simpset |
320 addsimps [Ord_nat RSN (2, OrdmemD) RSN (2, image_fun), |
312 addsimps [Ord_nat RSN (2, OrdmemD) RSN (2, image_fun), |
321 [nat_succI, Ord_nat] MRS OrdmemD RSN (2, image_fun)]) 1); |
313 [nat_succI, Ord_nat] MRS OrdmemD RSN (2, image_fun)]) 1); |
322 val UN_image_succ_eq = result(); |
314 val UN_image_succ_eq = result(); |
323 |
315 |
324 goal thy "!!f. [| (UN x:f``n. P(x)) = y; P(f`n) = succ(y); \ |
316 goal thy "!!f. [| (UN x:f``n. P(x)) = y; P(f`n) = succ(y); \ |
325 \ f:nat -> X; n:nat |] ==> (UN x:f``succ(n). P(x)) = succ(y)"; |
317 \ f:nat -> X; n:nat |] ==> (UN x:f``succ(n). P(x)) = succ(y)"; |
326 by (asm_full_simp_tac (AC_ss addsimps [UN_image_succ_eq]) 1); |
318 by (asm_full_simp_tac (!simpset addsimps [UN_image_succ_eq]) 1); |
327 by (fast_tac (AC_cs addSIs [equalityI]) 1); |
319 by (fast_tac (!claset addSIs [equalityI]) 1); |
328 val UN_image_succ_eq_succ = result(); |
320 val UN_image_succ_eq_succ = result(); |
329 |
321 |
330 goal thy "!!f. [| f: (UN n:nat. {g:succ(n) -> D. P(g, n)}); \ |
322 goal thy "!!f. [| f:succ(n) -> D; n:nat; \ |
331 \ domain(f)=succ(x); x=y |] ==> f`y : D"; |
323 \ domain(f)=succ(x); x=y |] ==> f`y : D"; |
332 by (fast_tac (AC_cs addEs [apply_type] |
324 by (fast_tac (!claset addEs [apply_type] |
333 addSDs [[sym, domain_of_fun] MRS trans]) 1); |
325 addSDs [[sym, domain_of_fun] MRS trans]) 1); |
334 val apply_UN_type = result(); |
326 val apply_domain_type = result(); |
335 |
327 |
336 goal thy "!!f. [| f : nat -> X; n:nat |] ==> f``succ(n) = cons(f`n, f``n)"; |
328 goal thy "!!f. [| f : nat -> X; n:nat |] ==> f``succ(n) = cons(f`n, f``n)"; |
337 by (asm_full_simp_tac (AC_ss |
329 by (asm_full_simp_tac (!simpset |
338 addsimps [nat_succI, Ord_nat RSN (2, OrdmemD), image_fun]) 1); |
330 addsimps [nat_succI, Ord_nat RSN (2, OrdmemD), image_fun]) 1); |
339 val image_fun_succ = result(); |
331 val image_fun_succ = result(); |
340 |
332 |
341 goal thy "!!f. [| domain(f`n) = succ(u); f : nat -> (UN n:nat. \ |
333 goal thy "!!f. [| domain(f`n) = succ(u); f : nat -> (UN n:nat. \ |
342 \ {f:succ(n)->domain(R). ALL k:n. <f`k, f`succ(k)> : R}); \ |
334 \ {f:succ(n)->domain(R). ALL k:n. <f`k, f`succ(k)> : R}); \ |
343 \ u=k; n:nat \ |
335 \ u=k; n:nat \ |
344 \ |] ==> f`n : succ(k) -> domain(R)"; |
336 \ |] ==> f`n : succ(k) -> domain(R)"; |
345 by (dtac apply_type 1 THEN (assume_tac 1)); |
337 by (dtac apply_type 1 THEN (assume_tac 1)); |
346 by (fast_tac (AC_cs addEs [UN_E, domain_eq_imp_fun_type]) 1); |
338 by (fast_tac (!claset addEs [UN_E, domain_eq_imp_fun_type]) 1); |
347 val f_n_type = result(); |
339 val f_n_type = result(); |
348 |
340 |
349 goal thy "!!f. [| f : nat -> (UN n:nat. \ |
341 goal thy "!!f. [| f : nat -> (UN n:nat. \ |
350 \ {f:succ(n)->domain(R). ALL k:n. <f`k, f`succ(k)> : R}); \ |
342 \ {f:succ(n)->domain(R). ALL k:n. <f`k, f`succ(k)> : R}); \ |
351 \ domain(f`n) = succ(k); n:nat \ |
343 \ domain(f`n) = succ(k); n:nat \ |
352 \ |] ==> ALL i:k. <f`n`i, f`n`succ(i)> : R"; |
344 \ |] ==> ALL i:k. <f`n`i, f`n`succ(i)> : R"; |
353 by (dtac apply_type 1 THEN (assume_tac 1)); |
345 by (dtac apply_type 1 THEN (assume_tac 1)); |
354 by (etac UN_E 1); |
346 by (etac UN_E 1); |
355 by (etac CollectE 1); |
347 by (etac CollectE 1); |
356 by (dresolve_tac [domain_of_fun RS sym RS trans] 1 THEN (assume_tac 1)); |
348 by (dresolve_tac [domain_of_fun RS sym RS trans] 1 THEN (assume_tac 1)); |
357 by (dtac succ_eqD 1); |
349 by (Asm_full_simp_tac 1); |
358 by (asm_full_simp_tac AC_ss 1); |
|
359 val f_n_pairs_in_R = result(); |
350 val f_n_pairs_in_R = result(); |
360 |
351 |
361 goalw thy [restrict_def] |
352 goalw thy [restrict_def] |
362 "!!f. [| restrict(f, domain(x))=x; f:n->X; domain(x) <= n \ |
353 "!!f. [| restrict(f, domain(x))=x; f:n->X; domain(x) <= n \ |
363 \ |] ==> restrict(cons(<n, y>, f), domain(x)) = x"; |
354 \ |] ==> restrict(cons(<n, y>, f), domain(x)) = x"; |
364 by (eresolve_tac [sym RS trans RS sym] 1); |
355 by (eresolve_tac [sym RS trans RS sym] 1); |
365 by (rtac fun_extension 1); |
356 by (rtac fun_extension 1); |
366 by (fast_tac (AC_cs addSIs [lam_type]) 1); |
357 by (fast_tac (!claset addSIs [lam_type]) 1); |
367 by (fast_tac (AC_cs addSIs [lam_type]) 1); |
358 by (fast_tac (!claset addSIs [lam_type]) 1); |
368 by (asm_full_simp_tac (AC_ss addsimps [subsetD RS cons_val_k]) 1); |
359 by (asm_full_simp_tac (!simpset addsimps [subsetD RS cons_val_k]) 1); |
369 val restrict_cons_eq_restrict = result(); |
360 val restrict_cons_eq_restrict = result(); |
370 |
361 |
371 goal thy "!!f. [| ALL x:f``n. restrict(f`n, domain(x))=x; \ |
362 goal thy "!!f. [| ALL x:f``n. restrict(f`n, domain(x))=x; \ |
372 \ f : nat -> (UN n:nat. \ |
363 \ f : nat -> (UN n:nat. \ |
373 \ {f:succ(n)->domain(R). ALL k:n. <f`k, f`succ(k)> : R}); \ |
364 \ {f:succ(n)->domain(R). ALL k:n. <f`k, f`succ(k)> : R}); \ |
374 \ n:nat; domain(f`n) = succ(n); \ |
365 \ n:nat; domain(f`n) = succ(n); \ |
375 \ (UN x:f``n. domain(x)) <= n |] \ |
366 \ (UN x:f``n. domain(x)) <= n |] \ |
376 \ ==> ALL x:f``succ(n). restrict(cons(<succ(n),y>, f`n), domain(x))=x"; |
367 \ ==> ALL x:f``succ(n). restrict(cons(<succ(n),y>, f`n), domain(x))=x"; |
377 by (rtac ballI 1); |
368 by (rtac ballI 1); |
378 by (asm_full_simp_tac (AC_ss addsimps [image_fun_succ]) 1); |
369 by (asm_full_simp_tac (!simpset addsimps [image_fun_succ]) 1); |
379 by (dtac f_n_type 1 THEN REPEAT (ares_tac [refl] 1)); |
370 by (dtac f_n_type 1 THEN REPEAT (ares_tac [refl] 1)); |
380 by (etac consE 1); |
371 by (etac disjE 1); |
381 by (asm_full_simp_tac (AC_ss addsimps [domain_of_fun, restrict_cons_eq]) 1); |
372 by (asm_full_simp_tac (!simpset addsimps [domain_of_fun, restrict_cons_eq]) 1); |
382 by (dtac bspec 1 THEN (assume_tac 1)); |
373 by (dtac bspec 1 THEN (assume_tac 1)); |
383 by (fast_tac (AC_cs addSEs [restrict_cons_eq_restrict]) 1); |
374 by (fast_tac (!claset addSEs [restrict_cons_eq_restrict]) 1); |
384 val all_in_image_restrict_eq = result(); |
375 val all_in_image_restrict_eq = result(); |
385 |
376 |
386 goal thy "!!X. [| ALL b<nat. <f``b, f`b> : \ |
377 goal thy |
387 \ {z:Fin(XX)*XX. (domain(snd(z))=succ(UN f:fst(z). domain(f)) \ |
378 "!!X.[| ALL b<nat. <f``b, f`b> : \ |
388 \ & (ALL f:fst(z). restrict(snd(z), domain(f)) = f)) | \ |
379 \ {<z1,z2>:Fin(XX)*XX. (domain(z2)=succ(UN f:z1. domain(f)) \ |
389 \ (~ (EX g:XX. domain(g)=succ(UN f:fst(z). domain(f)) \ |
380 \ & (ALL f:z1. restrict(z2, domain(f)) = f)) | \ |
390 \ & (ALL f:fst(z). restrict(g, domain(f)) = f)) & snd(z)={<0,x>})}; \ |
381 \ (~ (EX g:XX. domain(g)=succ(UN f:z1. domain(f)) \ |
|
382 \ & (ALL f:z1. restrict(g, domain(f)) = f)) & z2={<0,x>})}; \ |
391 \ XX = (UN n:nat. \ |
383 \ XX = (UN n:nat. \ |
392 \ {f:succ(n)->domain(R). ALL k:n. <f`k, f`succ(k)> : R}); \ |
384 \ {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) \ |
385 \ f: nat -> XX; range(R) <= domain(R); x:domain(R) \ |
394 \ |] ==> ALL b<nat. <f``b, f`b> : \ |
386 \ |] ==> ALL b<nat. <f``b, f`b> : \ |
395 \ {z:Fin(XX)*XX. (domain(snd(z))=succ(UN f:fst(z). domain(f)) \ |
387 \ {<z1,z2>:Fin(XX)*XX. (domain(z2)=succ(UN f:z1. domain(f)) \ |
396 \ & (UN f:fst(z). domain(f)) = b \ |
388 \ & (UN f:z1. domain(f)) = b \ |
397 \ & (ALL f:fst(z). restrict(snd(z), domain(f)) = f))}"; |
389 \ & (ALL f:z1. restrict(z2, domain(f)) = f))}"; |
398 by (rtac oallI 1); |
390 by (rtac oallI 1); |
399 by (dtac ltD 1); |
391 by (dtac ltD 1); |
400 by (etac nat_induct 1); |
392 by (etac nat_induct 1); |
401 by (dresolve_tac [[nat_0I, Ord_nat] MRS ltI RSN (2, ospec)] 1); |
393 by (dresolve_tac [[nat_0I, Ord_nat] MRS ltI RSN (2, ospec)] 1); |
402 by (fast_tac (FOL_cs addss |
394 by (fast_tac (FOL_cs addss |
403 (ZF_ss addsimps [image_0, singleton_fun RS domain_of_fun, |
395 (!simpset addsimps [image_0, singleton_fun RS domain_of_fun, |
404 [lepoll_refl, succI1] MRS lepoll_1_is_sing, singleton_in_funs])) 1); |
396 singleton_0, singleton_in_funs])) 1); |
|
397 (*induction step*) (** LEVEL 5 **) |
|
398 by (Full_simp_tac 1); |
405 by (dresolve_tac [[nat_succI, Ord_nat] MRS ltI RSN (2, ospec)] 1 |
399 by (dresolve_tac [[nat_succI, Ord_nat] MRS ltI RSN (2, ospec)] 1 |
406 THEN (assume_tac 1)); |
400 THEN (assume_tac 1)); |
407 by (REPEAT (eresolve_tac [conjE, CollectE, disjE] 1)); |
401 by (REPEAT (eresolve_tac [conjE, disjE] 1)); |
408 by (fast_tac (FOL_cs addSEs [trans, subst_context] |
402 by (fast_tac (FOL_cs addSEs [trans, subst_context] |
409 addSIs [UN_image_succ_eq_succ] addss AC_ss) 1); |
403 addSIs [UN_image_succ_eq_succ] addss (!simpset)) 1); |
410 by (etac conjE 1); |
404 by (etac conjE 1); |
411 by (etac notE 1); |
405 by (etac notE 1); |
412 by (asm_full_simp_tac (AC_ss addsimps [UN_image_succ_eq_succ]) 1); |
406 by (asm_full_simp_tac (!simpset addsimps [UN_image_succ_eq_succ]) 1); |
413 by (etac conjE 1); |
407 (** LEVEL 12 **) |
414 by (dtac apply_UN_type 1 THEN REPEAT (assume_tac 1)); |
408 by (REPEAT (eresolve_tac [conjE, bexE] 1)); |
|
409 by (dtac apply_domain_type 1 THEN REPEAT (assume_tac 1)); |
415 by (etac domainE 1); |
410 by (etac domainE 1); |
416 by (etac domainE 1); |
411 by (etac domainE 1); |
|
412 |
417 by (forward_tac [f_n_type] 1 THEN REPEAT (assume_tac 1)); |
413 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); |
414 by (res_inst_tac [("x","cons(<succ(xa), ya>, f`xa)")] bexI 1); |
419 by (fast_tac (FOL_cs |
415 by (fast_tac (FOL_cs |
420 addEs [subst_context RSN (2, trans) RS domain_cons_eq_succ, |
416 addEs [subst_context RSN (2, trans) RS domain_cons_eq_succ, |
421 subst_context, all_in_image_restrict_eq, trans, equalityD1]) 1); |
417 subst_context, all_in_image_restrict_eq, trans, equalityD1]) 1); |
424 by (rtac CollectI 1); |
420 by (rtac CollectI 1); |
425 by (eresolve_tac [rangeI RSN (2, subsetD) RSN (2, cons_fun_type2)] 1 |
421 by (eresolve_tac [rangeI RSN (2, subsetD) RSN (2, cons_fun_type2)] 1 |
426 THEN REPEAT (assume_tac 1)); |
422 THEN REPEAT (assume_tac 1)); |
427 by (rtac ballI 1); |
423 by (rtac ballI 1); |
428 by (etac succE 1); |
424 by (etac succE 1); |
429 by (asm_full_simp_tac (AC_ss addsimps [cons_val_n, cons_val_k]) 1); |
425 (** LEVEL 25 **) |
430 by (dresolve_tac [domain_of_fun RSN (2, f_n_pairs_in_R)] 1 |
426 by (dresolve_tac [domain_of_fun RSN (2, f_n_pairs_in_R)] 2 |
431 THEN REPEAT (assume_tac 1)); |
427 THEN REPEAT (assume_tac 2)); |
432 by (dtac bspec 1 THEN (assume_tac 1)); |
428 by (dtac bspec 2 THEN (assume_tac 2)); |
433 by (asm_full_simp_tac (AC_ss |
429 by (asm_full_simp_tac (!simpset |
434 addsimps [nat_into_Ord RS succ_in_succ, succI2, cons_val_k]) 1); |
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); |
435 val simplify_recursion = result(); |
432 val simplify_recursion = result(); |
436 |
433 |
|
434 |
437 goal thy "!!X. [| XX = (UN n:nat. \ |
435 goal thy "!!X. [| XX = (UN n:nat. \ |
438 \ {f:succ(n)->domain(R). ALL k:n. <f`k, f`succ(k)> : R}); \ |
436 \ {f:succ(n)->domain(R). ALL k:n. <f`k, f`succ(k)> : R}); \ |
439 \ ALL b<nat. <f``b, f`b> : \ |
437 \ ALL b<nat. <f``b, f`b> : \ |
440 \ {z:Fin(XX)*XX. (domain(snd(z))=succ(UN f:fst(z). domain(f)) \ |
438 \ {<z1,z2>:Fin(XX)*XX. (domain(z2)=succ(UN f:z1. domain(f)) \ |
441 \ & (UN f:fst(z). domain(f)) = b \ |
439 \ & (UN f:z1. domain(f)) = b \ |
442 \ & (ALL f:fst(z). restrict(snd(z), domain(f)) = f))}; \ |
440 \ & (ALL f:z1. restrict(z2, domain(f)) = f))}; \ |
443 \ f: nat -> XX; range(R) <= domain(R); x:domain(R); n:nat \ |
441 \ f: nat -> XX; range(R) <= domain(R); x:domain(R); n:nat \ |
444 \ |] ==> f`n : succ(n) -> domain(R) \ |
442 \ |] ==> f`n : succ(n) -> domain(R) \ |
445 \ & (ALL i:n. <f`n`i, f`n`succ(i)>:R)"; |
443 \ & (ALL i:n. <f`n`i, f`n`succ(i)>:R)"; |
446 by (dtac ospec 1); |
444 by (dtac ospec 1); |
447 by (eresolve_tac [Ord_nat RSN (2, ltI)] 1); |
445 by (eresolve_tac [Ord_nat RSN (2, ltI)] 1); |
448 by (etac CollectE 1); |
446 by (etac CollectE 1); |
449 by (asm_full_simp_tac AC_ss 1); |
447 by (Asm_full_simp_tac 1); |
450 by (rtac conjI 1); |
448 by (rtac conjI 1); |
451 by (fast_tac (AC_cs |
449 by (fast_tac (!claset |
452 addSEs [trans RS domain_eq_imp_fun_type, subst_context]) 1); |
450 addSEs [trans RS domain_eq_imp_fun_type, subst_context]) 1); |
453 by (fast_tac (FOL_cs |
451 by (fast_tac (FOL_cs addSEs [conjE, f_n_pairs_in_R, trans, subst_context]) 1); |
454 addSEs [conjE, f_n_pairs_in_R, trans, subst_context]) 1); |
|
455 val lemma2 = result(); |
452 val lemma2 = result(); |
456 |
453 |
457 goal thy "!!n. [| XX = (UN n:nat. \ |
454 goal thy "!!n. [| XX = (UN n:nat. \ |
458 \ {f:succ(n)->domain(R). ALL k:n. <f`k, f`succ(k)> : R}); \ |
455 \ {f:succ(n)->domain(R). ALL k:n. <f`k, f`succ(k)> : R}); \ |
459 \ ALL b<nat. <f``b, f`b> : \ |
456 \ ALL b<nat. <f``b, f`b> : \ |
460 \ {z:Fin(XX)*XX. (domain(snd(z))=succ(UN f:fst(z). domain(f)) \ |
457 \ {<z1,z2>:Fin(XX)*XX. (domain(z2)=succ(UN f:z1. domain(f)) \ |
461 \ & (UN f:fst(z). domain(f)) = b \ |
458 \ & (UN f:z1. domain(f)) = b \ |
462 \ & (ALL f:fst(z). restrict(snd(z), domain(f)) = f))}; \ |
459 \ & (ALL f:z1. restrict(z2, domain(f)) = f))}; \ |
463 \ f : nat -> XX; n:nat; range(R) <= domain(R); x:domain(R) \ |
460 \ f : nat -> XX; n:nat; range(R) <= domain(R); x:domain(R) \ |
464 \ |] ==> f`n`n = f`succ(n)`n"; |
461 \ |] ==> f`n`n = f`succ(n)`n"; |
465 by (forward_tac [lemma2 RS conjunct1 RS domain_of_fun] 1 |
462 by (forward_tac [lemma2 RS conjunct1 RS domain_of_fun] 1 |
466 THEN REPEAT (assume_tac 1)); |
463 THEN REPEAT (assume_tac 1)); |
467 by (dresolve_tac [[nat_succI, Ord_nat] MRS ltI RSN (2, ospec)] 1 |
464 by (dresolve_tac [[nat_succI, Ord_nat] MRS ltI RSN (2, ospec)] 1 |
468 THEN (assume_tac 1)); |
465 THEN (assume_tac 1)); |
469 by (asm_full_simp_tac AC_ss 1); |
466 by (Asm_full_simp_tac 1); |
470 by (REPEAT (etac conjE 1)); |
467 by (REPEAT (etac conjE 1)); |
471 by (etac ballE 1); |
468 by (etac ballE 1); |
472 by (eresolve_tac [restrict_eq_imp_val_eq RS sym] 1); |
469 by (eresolve_tac [restrict_eq_imp_val_eq RS sym] 1); |
473 by (fast_tac (AC_cs addSEs [ssubst]) 1); |
470 by (fast_tac (!claset addSEs [ssubst]) 1); |
474 by (asm_full_simp_tac (AC_ss |
471 by (asm_full_simp_tac (!simpset |
475 addsimps [[nat_succI, Ord_nat] MRS OrdmemD RSN (2, image_fun)]) 1); |
472 addsimps [[nat_succI, Ord_nat] MRS OrdmemD RSN (2, image_fun)]) 1); |
476 val lemma3 = result(); |
473 val lemma3 = result(); |
477 |
474 |
478 goalw thy [DC_def, DC0_def] "!!Z. DC(nat) ==> DC0"; |
475 goalw thy [DC_def, DC0_def] "!!Z. DC(nat) ==> DC0"; |
479 by (REPEAT (resolve_tac [allI, impI] 1)); |
476 by (REPEAT (resolve_tac [allI, impI] 1)); |
510 by (resolve_tac [f_type RS CollectI] 1); |
507 by (resolve_tac [f_type RS CollectI] 1); |
511 by (REPEAT (resolve_tac [ballI,impI] 1)); |
508 by (REPEAT (resolve_tac [ballI,impI] 1)); |
512 by (resolve_tac [Ord_a RS Ord_in_Ord RS Ord_linear_lt] 1 |
509 by (resolve_tac [Ord_a RS Ord_in_Ord RS Ord_linear_lt] 1 |
513 THEN (assume_tac 1)); |
510 THEN (assume_tac 1)); |
514 by (eres_inst_tac [("j","x")] (Ord_a RS Ord_in_Ord) 1); |
511 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)); |
512 by (REPEAT (fast_tac (!claset addDs [not_eq, not_eq RS not_sym]) 1)); |
516 val fun_Ord_inj = result(); |
513 val fun_Ord_inj = result(); |
517 |
514 |
518 goal thy "!!a. [| f:X->Y; A<=X; a:A |] ==> f`a : f``A"; |
515 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); |
516 by (fast_tac (!claset addSEs [image_fun RS ssubst]) 1); |
520 val value_in_image = result(); |
517 val value_in_image = result(); |
521 |
518 |
522 goalw thy [DC_def, WO3_def] |
519 goalw thy [DC_def, WO3_def] |
523 "!!Z. ALL K. Card(K) --> DC(K) ==> WO3"; |
520 "!!Z. ALL K. Card(K) --> DC(K) ==> WO3"; |
524 by (rtac allI 1); |
521 by (rtac allI 1); |
525 by (excluded_middle_tac "A lesspoll Hartog(A)" 1); |
522 by (excluded_middle_tac "A lesspoll Hartog(A)" 1); |
526 by (fast_tac (AC_cs addSDs [lesspoll_imp_ex_lt_eqpoll] |
523 by (fast_tac (!claset addSDs [lesspoll_imp_ex_lt_eqpoll] |
527 addSIs [Ord_Hartog, leI RS le_imp_subset]) 2); |
524 addSIs [Ord_Hartog, leI RS le_imp_subset]) 2); |
528 by (REPEAT (eresolve_tac [allE, impE] 1)); |
525 by (REPEAT (eresolve_tac [allE, impE] 1)); |
529 by (rtac Card_Hartog 1); |
526 by (rtac Card_Hartog 1); |
530 by (eres_inst_tac [("x","A")] allE 1); |
527 by (eres_inst_tac [("x","A")] allE 1); |
531 by (eres_inst_tac [("x","{z:Pow(A)*A . fst(z) \ |
528 by (eres_inst_tac [("x","{<z1,z2>:Pow(A)*A . z1 \ |
532 \ lesspoll Hartog(A) & snd(z) ~: fst(z)}")] allE 1); |
529 \ lesspoll Hartog(A) & z2 ~: z1}")] allE 1); |
533 by (asm_full_simp_tac AC_ss 1); |
530 by (Asm_full_simp_tac 1); |
534 by (etac impE 1); |
531 by (etac impE 1); |
535 by (fast_tac (AC_cs addEs [lemma1 RS not_emptyE]) 1); |
532 by (fast_tac (!claset addEs [lemma1 RS not_emptyE]) 1); |
536 by (etac bexE 1); |
533 by (etac bexE 1); |
537 by (resolve_tac [exI RS (lepoll_def RS (def_imp_iff RS iffD2)) |
534 by (resolve_tac [exI RS (lepoll_def RS (def_imp_iff RS iffD2)) |
538 RS (HartogI RS notE)] 1); |
535 RS (HartogI RS notE)] 1); |
539 by (resolve_tac [Ord_Hartog RSN (2, fun_Ord_inj)] 1 THEN (assume_tac 1)); |
536 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, |
537 by (dresolve_tac [Ord_Hartog RSN (2, OrdmemD) RSN (2, |
541 ltD RSN (3, value_in_image))] 1 |
538 ltD RSN (3, value_in_image))] 1 |
542 THEN REPEAT (assume_tac 1)); |
539 THEN REPEAT (assume_tac 1)); |
543 by (fast_tac (AC_cs addSDs [Ord_Hartog RSN (2, ltI) RSN (2, ospec)] |
540 by (fast_tac (!claset addSDs [Ord_Hartog RSN (2, ltI) RSN (2, ospec)] |
544 addEs [subst]) 1); |
541 addEs [subst]) 1); |
545 qed "DC_WO3"; |
542 qed "DC_WO3"; |
546 |
543 |
547 (* ********************************************************************** *) |
544 (* ********************************************************************** *) |
548 (* WO1 ==> ALL K. Card(K) --> DC(K) *) |
545 (* WO1 ==> ALL K. Card(K) --> DC(K) *) |
549 (* ********************************************************************** *) |
546 (* ********************************************************************** *) |
550 |
547 |
551 goal thy |
548 goal thy |
552 "!!a. [| Ord(a); b:a |] ==> (lam x:a. P(x))``b = (lam x:b. P(x))``b"; |
549 "!!a. [| Ord(a); b:a |] ==> (lam x:a. P(x))``b = (lam x:b. P(x))``b"; |
553 by (rtac images_eq 1); |
550 by (rtac images_eq 1); |
554 by (REPEAT (fast_tac (AC_cs addSEs [RepFunI, OrdmemD] |
551 by (REPEAT (fast_tac (!claset addSEs [RepFunI, OrdmemD] |
555 addSIs [lam_type]) 2)); |
552 addSIs [lam_type]) 2)); |
556 by (rtac ballI 1); |
553 by (rtac ballI 1); |
557 by (dresolve_tac [OrdmemD RS subsetD] 1 |
554 by (dresolve_tac [OrdmemD RS subsetD] 1 |
558 THEN REPEAT (assume_tac 1)); |
555 THEN REPEAT (assume_tac 1)); |
559 by (asm_full_simp_tac AC_ss 1); |
556 by (Asm_full_simp_tac 1); |
560 val lam_images_eq = result(); |
557 val lam_images_eq = result(); |
561 |
558 |
562 goalw thy [lesspoll_def] "!!K. [| Card(K); b:K |] ==> b lesspoll K"; |
559 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); |
560 by (asm_full_simp_tac (!simpset addsimps [Card_iff_initial]) 1); |
564 by (fast_tac (AC_cs addSIs [le_imp_lepoll, ltI, leI]) 1); |
561 by (fast_tac (!claset addSIs [le_imp_lepoll, ltI, leI]) 1); |
565 val in_Card_imp_lesspoll = result(); |
562 val in_Card_imp_lesspoll = result(); |
566 |
563 |
567 goal thy "(lam b:a. P(b)) : a -> {P(b). b:a}"; |
564 goal thy "(lam b:a. P(b)) : a -> {P(b). b:a}"; |
568 by (fast_tac (AC_cs addSIs [lam_type, RepFunI]) 1); |
565 by (fast_tac (!claset addSIs [lam_type, RepFunI]) 1); |
569 val lam_type_RepFun = result(); |
566 val lam_type_RepFun = result(); |
570 |
567 |
571 goal thy "!!Z. [| ALL Y:Pow(X). Y lesspoll a --> (EX x:X. <Y, x> : R); \ |
568 goal thy "!!Z. [| ALL Y:Pow(X). Y lesspoll a --> (EX x:X. <Y, x> : R); \ |
572 \ b:a; Z:Pow(X); Z lesspoll a |] \ |
569 \ b:a; Z:Pow(X); Z lesspoll a |] \ |
573 \ ==> {x:X. <Z,x> : R} ~= 0"; |
570 \ ==> {x:X. <Z,x> : R} ~= 0"; |