18 |
36 |
19 goalw thy [uu_def] "domain(uu(f,b,g,d)) <= f`b"; |
37 goalw thy [uu_def] "domain(uu(f,b,g,d)) <= f`b"; |
20 by (fast_tac ZF_cs 1); |
38 by (fast_tac ZF_cs 1); |
21 val domain_uu_subset = result(); |
39 val domain_uu_subset = result(); |
22 |
40 |
23 goal thy "!!a. [| ALL b<a. f`b lepoll m; b<a |] \ |
41 goal thy "!! a. ALL b<a. f`b lepoll m ==> \ |
24 \ ==> domain(uu(f, b, g, d)) lepoll m"; |
42 \ ALL b<a. ALL g<a. ALL d<a. domain(uu(f,b,g,d)) lepoll m"; |
25 by (fast_tac (AC_cs addSEs |
43 by (fast_tac (AC_cs addSEs |
26 [domain_uu_subset RS subset_imp_lepoll RS lepoll_trans]) 1); |
44 [domain_uu_subset RS subset_imp_lepoll RS lepoll_trans]) 1); |
27 val domain_uu_lepoll_m = result(); |
|
28 |
|
29 goal thy "!! a. ALL b<a. f`b lepoll m ==> \ |
|
30 \ ALL b<a. ALL g<a. ALL d<a. domain(uu(f,b,g,d)) lepoll m"; |
|
31 by (fast_tac (AC_cs addEs [domain_uu_lepoll_m]) 1); |
|
32 val quant_domain_uu_lepoll_m = result(); |
45 val quant_domain_uu_lepoll_m = result(); |
33 |
46 |
34 (* used in case 2 *) |
|
35 goalw thy [uu_def] "uu(f,b,g,d) <= f`b * f`g"; |
47 goalw thy [uu_def] "uu(f,b,g,d) <= f`b * f`g"; |
36 by (fast_tac ZF_cs 1); |
48 by (fast_tac ZF_cs 1); |
37 val uu_subset1 = result(); |
49 val uu_subset1 = result(); |
38 |
50 |
39 goalw thy [uu_def] "uu(f,b,g,d) <= f`d"; |
51 goalw thy [uu_def] "uu(f,b,g,d) <= f`d"; |
40 by (fast_tac ZF_cs 1); |
52 by (fast_tac ZF_cs 1); |
41 val uu_subset2 = result(); |
53 val uu_subset2 = result(); |
42 |
54 |
43 goal thy "!! a. [| ALL b<a. f`b lepoll m; d<a |] ==> uu(f,b,g,d) lepoll m"; |
55 goal thy "!! a. [| ALL b<a. f`b lepoll m; d<a |] ==> uu(f,b,g,d) lepoll m"; |
44 by (fast_tac (AC_cs |
56 by (fast_tac (AC_cs |
45 addSEs [uu_subset2 RS subset_imp_lepoll RS lepoll_trans]) 1); |
57 addSEs [uu_subset2 RS subset_imp_lepoll RS lepoll_trans]) 1); |
46 val uu_lepoll_m = result(); |
58 val uu_lepoll_m = result(); |
47 |
59 |
48 (* ********************************************************************** *) |
60 (* ********************************************************************** *) |
49 (* Two cases for lemma ii *) |
61 (* Two cases for lemma ii *) |
50 (* ********************************************************************** *) |
62 (* ********************************************************************** *) |
51 goalw thy [lesspoll_def] |
63 goalw thy [lesspoll_def] |
52 "!! a f u. ALL b<a. ALL g<a. ALL d<a. u(f,b,g,d) lepoll m ==> \ |
64 "!! a f u. ALL b<a. ALL g<a. ALL d<a. u(f,b,g,d) lepoll m ==> \ |
53 \ (ALL b<a. f`b ~= 0 --> (EX g<a. EX d<a. u(f,b,g,d) ~= 0 & \ |
65 \ (ALL b<a. f`b ~= 0 --> (EX g<a. EX d<a. u(f,b,g,d) ~= 0 & \ |
54 \ u(f,b,g,d) lesspoll m)) | \ |
66 \ u(f,b,g,d) lesspoll m)) | \ |
55 \ (EX b<a. f`b ~= 0 & (ALL g<a. ALL d<a. u(f,b,g,d) ~= 0 --> \ |
67 \ (EX b<a. f`b ~= 0 & (ALL g<a. ALL d<a. u(f,b,g,d) ~= 0 --> \ |
56 \ u(f,b,g,d) eqpoll m))"; |
68 \ u(f,b,g,d) eqpoll m))"; |
|
69 by (asm_simp_tac OrdQuant_ss 1); |
57 by (fast_tac AC_cs 1); |
70 by (fast_tac AC_cs 1); |
58 val cases = result(); |
71 val cases = result(); |
59 |
72 |
60 (* ********************************************************************** *) |
73 (* ********************************************************************** *) |
61 (* Lemmas used in both cases *) |
74 (* Lemmas used in both cases *) |
62 (* ********************************************************************** *) |
75 (* ********************************************************************** *) |
63 goal thy "!!a f. Ord(a) ==> (UN b<a++a. f`b) = (UN b<a. f`b Un f`(a++b))"; |
76 goal thy "!!a C. Ord(a) ==> (UN b<a++a. C(b)) = (UN b<a. C(b) Un C(a++b))"; |
64 by (resolve_tac [equalityI] 1); |
77 by (fast_tac (AC_cs addSIs [equalityI] addIs [ltI] |
65 by (fast_tac (AC_cs addIs [ltI, OUN_I] addSEs [OUN_E] |
78 addSDs [lt_oadd_disj] |
66 addSDs [lt_oadd_disj]) 1); |
79 addSEs [lt_oadd1, oadd_lt_mono2]) 1); |
67 by (fast_tac (AC_cs addSEs [lt_oadd1, oadd_lt_mono2, OUN_E] |
|
68 addSIs [OUN_I]) 1); |
|
69 val UN_oadd = result(); |
80 val UN_oadd = result(); |
70 |
81 |
71 val [prem] = goal thy |
|
72 "(!!b. b<a ==> P(b)=Q(b)) ==> (UN b<a. P(b)) = (UN b<a. Q(b))"; |
|
73 by (fast_tac (ZF_cs addSIs [OUN_I, equalityI] |
|
74 addSEs [OUN_E, prem RS equalityD1 RS subsetD, |
|
75 prem RS sym RS equalityD1 RS subsetD]) 1); |
|
76 val UN_eq = result(); |
|
77 |
|
78 goal thy "!!a. b<a ==> b = (THE l. l<a & a ++ b = a ++ l)"; |
|
79 by (fast_tac (ZF_cs addSIs [the_equality RS sym] |
|
80 addIs [lt_Ord2, lt_Ord] |
|
81 addSEs [oadd_inject RS sym]) 1); |
|
82 val the_only_b = result(); |
|
83 |
|
84 goal thy "!!A. B <= A ==> B Un (A-B) = A"; |
|
85 by (fast_tac (ZF_cs addSIs [equalityI]) 1); |
|
86 val subset_imp_Un_Diff_eq = result(); |
|
87 |
82 |
88 (* ********************************************************************** *) |
83 (* ********************************************************************** *) |
89 (* Case 1 : lemmas *) |
84 (* Case 1 : lemmas *) |
90 (* ********************************************************************** *) |
85 (* ********************************************************************** *) |
91 |
86 |
92 goalw thy [vv1_def] "vv1(f,b,succ(m)) <= f`b"; |
87 goalw thy [vv1_def] "vv1(f,m,b) <= f`b"; |
93 by (resolve_tac [expand_if RS iffD2] 1); |
88 by (rtac (letI RS letI) 1); |
94 by (fast_tac (ZF_cs addSIs [domain_uu_subset]) 1); |
89 by (split_tac [expand_if] 1); |
|
90 by (simp_tac (ZF_ss addsimps [domain_uu_subset]) 1); |
95 val vv1_subset = result(); |
91 val vv1_subset = result(); |
96 |
92 |
97 (* ********************************************************************** *) |
93 (* ********************************************************************** *) |
98 (* Case 1 : Union of images is the whole "y" *) |
94 (* Case 1 : Union of images is the whole "y" *) |
99 (* ********************************************************************** *) |
95 (* ********************************************************************** *) |
100 goal thy "!! a f y. [| (UN b<a. f`b) = y; Ord(a); m:nat |] ==> \ |
96 goalw thy [gg1_def] |
101 \ (UN b<a++a. (lam b:a++a. if(b<a, vv1(f,b,succ(m)), \ |
97 "!! a f y. [| Ord(a); m:nat |] ==> \ |
102 \ ww1(f, THE l. l<a & b=a++l, succ(m)))) ` b) = y"; |
98 \ (UN b<a++a. gg1(f,a,m)`b) = (UN b<a. f`b)"; |
103 by (resolve_tac [UN_oadd RS ssubst] 1 THEN (atac 1)); |
99 by (asm_simp_tac |
104 by (eresolve_tac [subst] 1); |
100 (OrdQuant_ss addsimps [UN_oadd, lt_oadd1, |
105 by (resolve_tac [UN_eq] 1); |
101 oadd_le_self RS le_imp_not_lt, lt_Ord, |
106 by (forw_inst_tac [("i","a")] lt_oadd1 1 |
102 odiff_oadd_inverse, ltD, |
107 THEN (REPEAT (atac 1))); |
103 vv1_subset RS Diff_partition, ww1_def]) 1); |
108 by (forw_inst_tac [("j","a")] oadd_lt_mono2 1 |
104 val UN_gg1_eq = result(); |
109 THEN (REPEAT (atac 1))); |
105 |
110 by (asm_simp_tac (ZF_ss addsimps [ltD RS beta, |
106 goal thy "domain(gg1(f,a,m)) = a++a"; |
111 oadd_le_self RS le_imp_not_lt RS if_not_P, lt_Ord]) 1); |
107 by (simp_tac (ZF_ss addsimps [lam_funtype RS domain_of_fun, gg1_def]) 1); |
112 by (resolve_tac [the_only_b RS subst] 1 THEN (atac 1)); |
108 val domain_gg1 = result(); |
113 by (asm_simp_tac (ZF_ss |
|
114 addsimps [vv1_subset RS subset_imp_Un_Diff_eq, ltD, ww1_def]) 1); |
|
115 val UN_eq_y = result(); |
|
116 |
109 |
117 (* ********************************************************************** *) |
110 (* ********************************************************************** *) |
118 (* every value of defined function is less than or equipollent to m *) |
111 (* every value of defined function is less than or equipollent to m *) |
119 (* ********************************************************************** *) |
112 (* ********************************************************************** *) |
120 goal thy "!!a b. [| P(a, b); Ord(a); Ord(b); \ |
113 goal thy "!!a b. [| P(a, b); Ord(a); Ord(b); \ |
121 \ Least_a = (LEAST a. EX x. Ord(x) & P(a, x)) |] \ |
114 \ Least_a = (LEAST a. EX x. Ord(x) & P(a, x)) |] \ |
122 \ ==> P(Least_a, LEAST b. P(Least_a, b))"; |
115 \ ==> P(Least_a, LEAST b. P(Least_a, b))"; |
123 by (eresolve_tac [ssubst] 1); |
116 by (eresolve_tac [ssubst] 1); |
124 by (res_inst_tac [("Q","%z. P(z, LEAST b. P(z, b))")] LeastI2 1); |
117 by (res_inst_tac [("Q","%z. P(z, LEAST b. P(z, b))")] LeastI2 1); |
125 by (REPEAT (fast_tac (ZF_cs addSEs [LeastI]) 1)); |
118 by (REPEAT (fast_tac (ZF_cs addSEs [LeastI]) 1)); |
126 val nested_LeastI = result(); |
119 val nested_LeastI = result(); |
127 |
120 |
128 val nested_Least_instance = read_instantiate |
121 val nested_Least_instance = |
|
122 standard |
|
123 (read_instantiate |
129 [("P","%g d. domain(uu(f,b,g,d)) ~= 0 & \ |
124 [("P","%g d. domain(uu(f,b,g,d)) ~= 0 & \ |
130 \ domain(uu(f,b,g,d)) lesspoll succ(m)")] nested_LeastI; |
125 \ domain(uu(f,b,g,d)) lepoll m")] nested_LeastI); |
131 |
126 |
132 goalw thy [vv1_def] "!!a. [| ALL b<a. f`b ~=0 --> \ |
127 goalw thy [gg1_def] |
133 \ (EX g<a. EX d<a. domain(uu(f,b,g,d))~=0 & \ |
128 "!!a. [| Ord(a); m:nat; \ |
134 \ domain(uu(f,b,g,d)) lesspoll succ(m)); m:nat; b<a |] \ |
129 \ ALL b<a. f`b ~=0 --> \ |
135 \ ==> vv1(f,b,succ(m)) lesspoll succ(m)"; |
130 \ (EX g<a. EX d<a. domain(uu(f,b,g,d)) ~= 0 & \ |
136 by (resolve_tac [expand_if RS iffD2] 1); |
131 \ domain(uu(f,b,g,d)) lepoll m); \ |
|
132 \ ALL b<a. f`b lepoll succ(m); b<a++a \ |
|
133 \ |] ==> gg1(f,a,m)`b lepoll m"; |
|
134 by (asm_simp_tac OrdQuant_ss 1); |
|
135 by (safe_tac (OrdQuant_cs addSEs [lt_oadd_odiff_cases])); |
|
136 (*Case b<a : show vv1(f,m,b) lepoll m *) |
|
137 by (asm_simp_tac (ZF_ss addsimps [vv1_def, Let_def] |
|
138 setloop split_tac [expand_if]) 1); |
137 by (fast_tac (AC_cs addIs [nested_Least_instance RS conjunct2] |
139 by (fast_tac (AC_cs addIs [nested_Least_instance RS conjunct2] |
138 addSEs [lt_Ord] |
140 addSEs [lt_Ord] |
139 addSIs [empty_lepollI RS lepoll_imp_lesspoll_succ]) 1); |
141 addSIs [empty_lepollI]) 1); |
140 val vv1_lesspoll_succ = result(); |
142 (*Case a le b: show ww1(f,m,b--a) lepoll m *) |
141 |
143 by (asm_simp_tac (ZF_ss addsimps [ww1_def]) 1); |
142 goalw thy [vv1_def] "!!a. [| ALL b<a. f`b ~=0 --> \ |
144 by (excluded_middle_tac "f`(b--a) = 0" 1); |
143 \ (EX g<a. EX d<a. domain(uu(f,b,g,d))~=0 & \ |
145 by (asm_simp_tac (OrdQuant_ss addsimps [empty_lepollI]) 2); |
144 \ domain(uu(f,b,g,d)) lesspoll succ(m)); m:nat; b<a; f`b ~= 0 |] \ |
146 by (resolve_tac [Diff_lepoll] 1); |
145 \ ==> vv1(f,b,succ(m)) ~= 0"; |
147 by (fast_tac AC_cs 1); |
146 by (resolve_tac [expand_if RS iffD2] 1); |
148 by (rtac vv1_subset 1); |
147 by (resolve_tac [conjI] 1); |
149 by (dtac (ospec RS mp) 1); |
148 by (fast_tac ZF_cs 2); |
150 by (REPEAT (eresolve_tac [asm_rl, oexE] 1)); |
149 by (resolve_tac [impI] 1); |
|
150 by (eresolve_tac [oallE] 1); |
|
151 by (mp_tac 1); |
|
152 by (contr_tac 2); |
|
153 by (REPEAT (eresolve_tac [oexE] 1)); |
|
154 by (asm_simp_tac (ZF_ss |
151 by (asm_simp_tac (ZF_ss |
155 addsimps [lt_Ord, nested_Least_instance RS conjunct1]) 1); |
152 addsimps [vv1_def, Let_def, lt_Ord, |
156 val vv1_not_0 = result(); |
153 nested_Least_instance RS conjunct1]) 1); |
157 |
154 val gg1_lepoll_m = result(); |
158 goalw thy [ww1_def] "!!a. [| ALL b<a. f`b ~=0 --> \ |
|
159 \ (EX g<a. EX d<a. domain(uu(f,b,g,d))~=0 & \ |
|
160 \ domain(uu(f,b,g,d)) lesspoll succ(m)); \ |
|
161 \ ALL b<a. f`b lepoll succ(m); m:nat; b<a |] \ |
|
162 \ ==> ww1(f,b,succ(m)) lesspoll succ(m)"; |
|
163 by (excluded_middle_tac "f`b = 0" 1); |
|
164 by (asm_full_simp_tac (AC_ss |
|
165 addsimps [empty_lepollI RS lepoll_imp_lesspoll_succ]) 2); |
|
166 by (resolve_tac [Diff_lepoll RS lepoll_imp_lesspoll_succ] 1); |
|
167 by (fast_tac AC_cs 1); |
|
168 by (REPEAT (ares_tac [vv1_subset, vv1_not_0] 1)); |
|
169 val ww1_lesspoll_succ = result(); |
|
170 |
|
171 goal thy "!!a. [| Ord(a); m:nat; \ |
|
172 \ ALL b<a. f`b ~=0 --> (EX g<a. EX d<a. domain(uu(f,b,g,d))~=0 & \ |
|
173 \ domain(uu(f,b,g,d)) lesspoll succ(m)); \ |
|
174 \ ALL b<a. f`b lepoll succ(m) |] \ |
|
175 \ ==> ALL b<a++a. (lam b:a++a. if(b<a, vv1(f,b,succ(m)), \ |
|
176 \ ww1(f,THE l. l<a & b = a ++ l,succ(m))))`b lepoll m"; |
|
177 by (resolve_tac [oallI] 1); |
|
178 by (asm_full_simp_tac (ZF_ss addsimps [ltD RS beta]) 1); |
|
179 by (resolve_tac [lesspoll_succ_imp_lepoll] 1 THEN (atac 2)); |
|
180 by (resolve_tac [expand_if RS iffD2] 1); |
|
181 by (resolve_tac [conjI] 1); |
|
182 by (resolve_tac [impI] 1); |
|
183 by (forward_tac [lt_oadd_disj1] 2 THEN (REPEAT (atac 2))); |
|
184 by (resolve_tac [impI] 2); |
|
185 by (eresolve_tac [disjE] 2 THEN (fast_tac (ZF_cs addSEs [ltE]) 2)); |
|
186 by (asm_full_simp_tac (ZF_ss addsimps [vv1_lesspoll_succ]) 1); |
|
187 by (dresolve_tac [theI] 1); |
|
188 by (eresolve_tac [conjE] 1); |
|
189 by (resolve_tac [ww1_lesspoll_succ] 1 THEN (REPEAT (atac 1))); |
|
190 val all_sum_lepoll_m = result(); |
|
191 |
155 |
192 (* ********************************************************************** *) |
156 (* ********************************************************************** *) |
193 (* Case 2 : lemmas *) |
157 (* Case 2 : lemmas *) |
194 (* ********************************************************************** *) |
158 (* ********************************************************************** *) |
195 |
159 |
196 (* ********************************************************************** *) |
160 (* ********************************************************************** *) |
197 (* Case 2 : vv2_subset *) |
161 (* Case 2 : vv2_subset *) |
198 (* ********************************************************************** *) |
162 (* ********************************************************************** *) |
199 |
163 |
200 goalw thy [uu_def] "!!f. [| b<a; g<a; f`b~=0; f`g~=0; \ |
164 goalw thy [uu_def] "!!f. [| b<a; g<a; f`b~=0; f`g~=0; \ |
201 \ y*y <= y; (UN b<a. f`b)=y |] \ |
165 \ y*y <= y; (UN b<a. f`b)=y \ |
202 \ ==> EX d<a. uu(f,b,g,d)~=0"; |
166 \ |] ==> EX d<a. uu(f,b,g,d) ~= 0"; |
203 by (fast_tac (AC_cs addSIs [not_emptyI] |
167 by (fast_tac (AC_cs addSIs [not_emptyI] |
204 addSDs [SigmaI RSN (2, subsetD)] |
168 addSDs [SigmaI RSN (2, subsetD)] |
205 addSEs [not_emptyE]) 1); |
169 addSEs [not_emptyE]) 1); |
206 val ex_d_uu_not_empty = result(); |
170 val ex_d_uu_not_empty = result(); |
207 |
171 |
208 goal thy "!!f. [| b<a; g<a; f`b~=0; f`g~=0; \ |
172 goal thy "!!f. [| b<a; g<a; f`b~=0; f`g~=0; \ |
209 \ y*y<=y; (UN b<a. f`b)=y |] \ |
173 \ y*y<=y; (UN b<a. f`b)=y |] \ |
210 \ ==> uu(f,b,g,LEAST d. (uu(f,b,g,d) ~= 0)) ~= 0"; |
174 \ ==> uu(f,b,g,LEAST d. (uu(f,b,g,d) ~= 0)) ~= 0"; |
211 by (dresolve_tac [ex_d_uu_not_empty] 1 THEN (REPEAT (atac 1))); |
175 by (dresolve_tac [ex_d_uu_not_empty] 1 THEN REPEAT (assume_tac 1)); |
212 by (fast_tac (AC_cs addSEs [LeastI, lt_Ord]) 1); |
176 by (fast_tac (AC_cs addSEs [LeastI, lt_Ord]) 1); |
213 val uu_not_empty = result(); |
177 val uu_not_empty = result(); |
214 |
178 |
215 (* moved from ZF_aux.ML *) |
179 goal ZF.thy "!!r. [| r<=A*B; r~=0 |] ==> domain(r)~=0"; |
216 goal thy "!!r. [| r<=A*B; r~=0 |] ==> domain(r)~=0"; |
|
217 by (REPEAT (eresolve_tac [asm_rl, not_emptyE, subsetD RS SigmaE, |
180 by (REPEAT (eresolve_tac [asm_rl, not_emptyE, subsetD RS SigmaE, |
218 sym RSN (2, subst_elem) RS domainI RS not_emptyI] 1)); |
181 sym RSN (2, subst_elem) RS domainI RS not_emptyI] 1)); |
219 val not_empty_rel_imp_domain = result(); |
182 val not_empty_rel_imp_domain = result(); |
220 |
183 |
221 goal thy "!!f. [| b<a; g<a; f`b~=0; f`g~=0; \ |
184 goal thy "!!f. [| b<a; g<a; f`b~=0; f`g~=0; \ |
222 \ y*y <= y; (UN b<a. f`b)=y |] \ |
185 \ y*y <= y; (UN b<a. f`b)=y |] \ |
223 \ ==> (LEAST d. uu(f,b,g,d) ~= 0) < a"; |
186 \ ==> (LEAST d. uu(f,b,g,d) ~= 0) < a"; |
224 by (eresolve_tac [ex_d_uu_not_empty RS oexE] 1 |
187 by (eresolve_tac [ex_d_uu_not_empty RS oexE] 1 |
225 THEN (REPEAT (atac 1))); |
188 THEN REPEAT (assume_tac 1)); |
226 by (resolve_tac [Least_le RS lt_trans1] 1 |
189 by (resolve_tac [Least_le RS lt_trans1] 1 |
227 THEN (REPEAT (ares_tac [lt_Ord] 1))); |
190 THEN (REPEAT (ares_tac [lt_Ord] 1))); |
228 val Least_uu_not_empty_lt_a = result(); |
191 val Least_uu_not_empty_lt_a = result(); |
229 |
192 |
230 goal thy "!!B. [| B<=A; a~:B |] ==> B <= A-{a}"; |
193 goal ZF.thy "!!B. [| B<=A; a~:B |] ==> B <= A-{a}"; |
231 by (fast_tac ZF_cs 1); |
194 by (fast_tac ZF_cs 1); |
232 val subset_Diff_sing = result(); |
195 val subset_Diff_sing = result(); |
233 |
196 |
|
197 (*Could this be proved more directly?*) |
234 goal thy "!!A B. [| A lepoll m; m lepoll B; B <= A; m:nat |] ==> A=B"; |
198 goal thy "!!A B. [| A lepoll m; m lepoll B; B <= A; m:nat |] ==> A=B"; |
235 by (eresolve_tac [natE] 1); |
199 by (eresolve_tac [natE] 1); |
236 by (fast_tac (AC_cs addSDs [lepoll_0_is_0] addSIs [equalityI]) 1); |
200 by (fast_tac (AC_cs addSDs [lepoll_0_is_0] addSIs [equalityI]) 1); |
237 by (hyp_subst_tac 1); |
201 by (hyp_subst_tac 1); |
238 by (resolve_tac [equalityI] 1); |
202 by (resolve_tac [equalityI] 1); |
239 by (atac 2); |
203 by (assume_tac 2); |
240 by (resolve_tac [subsetI] 1); |
204 by (resolve_tac [subsetI] 1); |
241 by (excluded_middle_tac "?P" 1 THEN (atac 2)); |
205 by (excluded_middle_tac "?P" 1 THEN (assume_tac 2)); |
242 by (eresolve_tac [subset_Diff_sing RS subset_imp_lepoll RSN (2, |
206 by (eresolve_tac [subset_Diff_sing RS subset_imp_lepoll RSN (2, |
243 diff_sing_lepoll RSN (3, lepoll_trans RS lepoll_trans)) RS |
207 diff_sing_lepoll RSN (3, lepoll_trans RS lepoll_trans)) RS |
244 succ_lepoll_natE] 1 |
208 succ_lepoll_natE] 1 |
245 THEN (REPEAT (atac 1))); |
209 THEN REPEAT (assume_tac 1)); |
246 val supset_lepoll_imp_eq = result(); |
210 val supset_lepoll_imp_eq = result(); |
247 |
211 |
248 goalw thy [vv2_def] |
212 goal thy |
249 "!!a. [| ALL g<a. ALL d<a. domain(uu(f, b, g, d))~=0 --> \ |
213 "!!a. [| ALL g<a. ALL d<a. domain(uu(f, b, g, d))~=0 --> \ |
250 \ domain(uu(f, b, g, d)) eqpoll succ(m); \ |
214 \ domain(uu(f, b, g, d)) eqpoll succ(m); \ |
251 \ ALL b<a. f`b lepoll succ(m); y*y <= y; \ |
215 \ ALL b<a. f`b lepoll succ(m); y*y <= y; \ |
252 \ (UN b<a. f`b)=y; b<a; g<a; d<a; f`b~=0; f`g~=0; m:nat; aa:f`b |] \ |
216 \ (UN b<a. f`b)=y; b<a; g<a; d<a; f`b~=0; f`g~=0; m:nat; s:f`b |] \ |
253 \ ==> uu(f,b,g,LEAST d. uu(f,b,g,d)~=0) : f`b -> f`g"; |
217 \ ==> uu(f,b,g,LEAST d. uu(f,b,g,d)~=0) : f`b -> f`g"; |
254 by (eres_inst_tac [("x","g")] oallE 1 THEN (contr_tac 2)); |
218 by (eres_inst_tac [("x","g")] oallE 1 THEN (contr_tac 2)); |
255 by (eres_inst_tac [("P","%z. ?QQ(z) ~= 0 --> ?RR(z)")] oallE 1); |
219 by (eres_inst_tac [("P","%z. ?QQ(z) ~= 0 --> ?RR(z)")] oallE 1); |
256 by (eresolve_tac [impE] 1); |
220 by (eresolve_tac [impE] 1); |
257 by (eresolve_tac [uu_not_empty RS (uu_subset1 RS |
221 by (eresolve_tac [uu_not_empty RS (uu_subset1 RS not_empty_rel_imp_domain)] 1 |
258 not_empty_rel_imp_domain)] 1 |
222 THEN REPEAT (assume_tac 1)); |
259 THEN (REPEAT (atac 1))); |
|
260 by (eresolve_tac [Least_uu_not_empty_lt_a RSN (2, notE)] 2 |
223 by (eresolve_tac [Least_uu_not_empty_lt_a RSN (2, notE)] 2 |
261 THEN (TRYALL atac)); |
224 THEN (TRYALL assume_tac)); |
262 by (resolve_tac [eqpoll_sym RS eqpoll_imp_lepoll RS |
225 by (resolve_tac [eqpoll_sym RS eqpoll_imp_lepoll RS |
263 (Least_uu_not_empty_lt_a RSN (2, uu_lepoll_m) RSN (2, |
226 (Least_uu_not_empty_lt_a RSN (2, uu_lepoll_m) RSN (2, |
264 uu_subset1 RSN (4, rel_is_fun)))] 1 |
227 uu_subset1 RSN (4, rel_is_fun)))] 1 |
265 THEN (TRYALL atac)); |
228 THEN (TRYALL assume_tac)); |
266 by (resolve_tac [eqpoll_sym RS eqpoll_imp_lepoll RSN (2, |
229 by (resolve_tac [eqpoll_sym RS eqpoll_imp_lepoll RSN (2, |
267 supset_lepoll_imp_eq)] 1); |
230 supset_lepoll_imp_eq)] 1); |
268 by (REPEAT (fast_tac (AC_cs addSIs [domain_uu_subset, nat_succI]) 1)); |
231 by (REPEAT (fast_tac (AC_cs addSIs [domain_uu_subset, nat_succI]) 1)); |
269 val uu_Least_is_fun = result(); |
232 val uu_Least_is_fun = result(); |
270 |
233 |
271 goalw thy [vv2_def] |
234 goalw thy [vv2_def] |
272 "!!a. [| ALL g<a. ALL d<a. domain(uu(f, b, g, d))~=0 --> \ |
235 "!!a. [| ALL g<a. ALL d<a. domain(uu(f, b, g, d))~=0 --> \ |
273 \ domain(uu(f, b, g, d)) eqpoll succ(m); \ |
236 \ domain(uu(f, b, g, d)) eqpoll succ(m); \ |
274 \ ALL b<a. f`b lepoll succ(m); y*y <= y; \ |
237 \ ALL b<a. f`b lepoll succ(m); y*y <= y; \ |
275 \ (UN b<a. f`b)=y; b<a; g<a; m:nat; aa:f`b |] \ |
238 \ (UN b<a. f`b)=y; b<a; g<a; m:nat; s:f`b \ |
276 \ ==> vv2(f,b,g,aa) <= f`g"; |
239 \ |] ==> vv2(f,b,g,s) <= f`g"; |
277 by (fast_tac (FOL_cs addIs [expand_if RS iffD2] |
240 by (split_tac [expand_if] 1); |
278 addSEs [uu_Least_is_fun] |
241 by (fast_tac (FOL_cs addSEs [uu_Least_is_fun] |
279 addSIs [empty_subsetI, not_emptyI, |
242 addSIs [empty_subsetI, not_emptyI, |
280 singleton_subsetI, apply_type]) 1); |
243 singleton_subsetI, apply_type]) 1); |
281 val vv2_subset = result(); |
244 val vv2_subset = result(); |
282 |
245 |
283 (* ********************************************************************** *) |
246 (* ********************************************************************** *) |
284 (* Case 2 : Union of images is the whole "y" *) |
247 (* Case 2 : Union of images is the whole "y" *) |
285 (* ********************************************************************** *) |
248 (* ********************************************************************** *) |
286 goal thy "!!a. [| ALL g<a. ALL d<a. domain(uu(f,b,g,d)) ~= 0 --> \ |
249 goalw thy [gg2_def] |
287 \ domain(uu(f,b,g,d)) eqpoll succ(m); \ |
250 "!!a. [| ALL g<a. ALL d<a. domain(uu(f,b,g,d)) ~= 0 --> \ |
288 \ ALL b<a. f`b lepoll succ(m); y*y<=y; \ |
251 \ domain(uu(f,b,g,d)) eqpoll succ(m); \ |
289 \ (UN b<a.f`b)=y; Ord(a); m:nat; aa:f`b; b<a |] \ |
252 \ ALL b<a. f`b lepoll succ(m); y*y<=y; \ |
290 \ ==> (UN g<a++a. (lam g:a++a. if(g<a, vv2(f,b,g,aa), \ |
253 \ (UN b<a.f`b)=y; Ord(a); m:nat; s:f`b; b<a \ |
291 \ ww2(f,b,THE l. l<a & g=a++l,aa)))`g) = y"; |
254 \ |] ==> (UN g<a++a. gg2(f,a,b,s) ` g) = y"; |
292 by (resolve_tac [UN_oadd RS ssubst] 1 THEN (atac 1)); |
255 bd sym 1; |
293 by (resolve_tac [subst] 1 THEN (atac 1)); |
256 by (asm_simp_tac |
294 by (resolve_tac [UN_eq] 1); |
257 (OrdQuant_ss addsimps [UN_oadd, lt_oadd1, |
295 by (forw_inst_tac [("i","a"),("k","ba")] lt_oadd1 1 |
258 oadd_le_self RS le_imp_not_lt, lt_Ord, |
296 THEN (REPEAT (atac 1))); |
259 odiff_oadd_inverse, ww2_def, |
297 by (forw_inst_tac [("j","a"),("k","ba")] oadd_lt_mono2 1 |
260 standard (vv2_subset RS Diff_partition)]) 1); |
298 THEN (REPEAT (atac 1))); |
261 (*Omitting "standard" above causes "Failed congruence proof!" bug??*) |
299 by (asm_simp_tac (ZF_ss addsimps [ltD RS beta, |
262 val UN_gg2_eq = result(); |
300 oadd_le_self RS le_imp_not_lt RS if_not_P, lt_Ord]) 1); |
263 |
301 by (resolve_tac [the_only_b RS subst] 1 THEN (atac 1)); |
264 goal thy "domain(gg2(f,a,b,s)) = a++a"; |
302 by (asm_simp_tac (ZF_ss |
265 by (simp_tac (ZF_ss addsimps [lam_funtype RS domain_of_fun, gg2_def]) 1); |
303 addsimps [vv2_subset RS subset_imp_Un_Diff_eq, ltI, ww2_def]) 1); |
266 val domain_gg2 = result(); |
304 val UN_eq_y_2 = result(); |
|
305 |
267 |
306 (* ********************************************************************** *) |
268 (* ********************************************************************** *) |
307 (* every value of defined function is less than or equipollent to m *) |
269 (* every value of defined function is less than or equipollent to m *) |
308 (* ********************************************************************** *) |
270 (* ********************************************************************** *) |
309 |
271 |
310 goalw thy [vv2_def] |
272 goalw thy [vv2_def] |
311 "!!m. [| m:nat; m~=0 |] ==> vv2(f,b,g,aa) lesspoll succ(m)"; |
273 "!!m. [| m:nat; m~=0 |] ==> vv2(f,b,g,s) lepoll m"; |
312 by (resolve_tac [conjI RS (expand_if RS iffD2)] 1); |
274 by (asm_simp_tac (OrdQuant_ss |
313 by (asm_simp_tac (AC_ss |
275 addsimps [empty_lepollI] |
314 addsimps [empty_lepollI RS lepoll_imp_lesspoll_succ]) 2); |
276 setloop split_tac [expand_if]) 1); |
315 by (fast_tac (AC_cs |
277 by (fast_tac (AC_cs |
316 addSDs [le_imp_subset RS subset_imp_lepoll RS lepoll_0_is_0] |
278 addSDs [le_imp_subset RS subset_imp_lepoll RS lepoll_0_is_0] |
317 addSIs [singleton_eqpoll_1 RS eqpoll_imp_lepoll RS |
279 addSIs [singleton_eqpoll_1 RS eqpoll_imp_lepoll RS lepoll_trans, |
318 lepoll_trans RS lepoll_imp_lesspoll_succ, |
|
319 not_lt_imp_le RS le_imp_subset RS subset_imp_lepoll, |
280 not_lt_imp_le RS le_imp_subset RS subset_imp_lepoll, |
320 nat_into_Ord, nat_1I]) 1); |
281 nat_into_Ord, nat_1I]) 1); |
321 val vv2_lesspoll_succ = result(); |
282 val vv2_lepoll = result(); |
322 |
283 |
323 goalw thy [ww2_def] "!!m. [| ALL b<a. f`b lepoll succ(m); g<a; m:nat; \ |
284 goalw thy [ww2_def] |
324 \ vv2(f,b,g,d) <= f`g |] \ |
285 "!!m. [| ALL b<a. f`b lepoll succ(m); g<a; m:nat; vv2(f,b,g,d) <= f`g \ |
325 \ ==> ww2(f,b,g,d) lesspoll succ(m)"; |
286 \ |] ==> ww2(f,b,g,d) lepoll m"; |
326 by (excluded_middle_tac "f`g = 0" 1); |
287 by (excluded_middle_tac "f`g = 0" 1); |
327 by (asm_simp_tac (AC_ss |
288 by (asm_simp_tac (OrdQuant_ss |
328 addsimps [empty_lepollI RS lepoll_imp_lesspoll_succ]) 2); |
289 addsimps [empty_lepollI]) 2); |
329 by (dresolve_tac [ospec] 1 THEN (atac 1)); |
290 by (dresolve_tac [ospec] 1 THEN (assume_tac 1)); |
330 by (resolve_tac [Diff_lepoll RS lepoll_imp_lesspoll_succ] 1 |
291 by (resolve_tac [Diff_lepoll] 1 |
331 THEN (TRYALL atac)); |
292 THEN (TRYALL assume_tac)); |
332 by (asm_simp_tac (AC_ss addsimps [vv2_def, expand_if, not_emptyI]) 1); |
293 by (asm_simp_tac (OrdQuant_ss addsimps [vv2_def, expand_if, not_emptyI]) 1); |
333 val ww2_lesspoll_succ = result(); |
294 val ww2_lepoll = result(); |
334 |
295 |
335 goal thy "!!a. [| ALL g<a. ALL d<a. domain(uu(f,b,g,d)) ~= 0 --> \ |
296 goalw thy [gg2_def] |
336 \ domain(uu(f,b,g,d)) eqpoll succ(m); \ |
297 "!!a. [| ALL g<a. ALL d<a. domain(uu(f,b,g,d)) ~= 0 --> \ |
337 \ ALL b<a. f`b lepoll succ(m); y*y <= y; \ |
298 \ domain(uu(f,b,g,d)) eqpoll succ(m); \ |
338 \ (UN b<a. f`b)=y; b<a; aa:f`b; m:nat; m~= 0 |] \ |
299 \ ALL b<a. f`b lepoll succ(m); y*y <= y; \ |
339 \ ==> ALL ba<a++a. (lam g:a++a. if(g<a, vv2(f,b,g,aa), \ |
300 \ (UN b<a. f`b)=y; b<a; s:f`b; m:nat; m~= 0; g<a++a \ |
340 \ ww2(f,b,THE l. l<a & g=a++l,aa)))`ba lepoll m"; |
301 \ |] ==> gg2(f,a,b,s) ` g lepoll m"; |
341 by (resolve_tac [oallI] 1); |
302 by (asm_simp_tac OrdQuant_ss 1); |
342 by (asm_full_simp_tac AC_ss 1); |
303 by (safe_tac (OrdQuant_cs addSEs [lt_oadd_odiff_cases, lt_Ord2])); |
343 by (resolve_tac [lesspoll_succ_imp_lepoll] 1 THEN (atac 2)); |
304 by (asm_simp_tac (OrdQuant_ss addsimps [vv2_lepoll]) 1); |
344 by (resolve_tac [conjI RS (expand_if RS iffD2)] 1); |
305 by (asm_simp_tac (ZF_ss addsimps [ww2_lepoll, vv2_subset]) 1); |
345 by (asm_simp_tac (AC_ss addsimps [vv2_lesspoll_succ]) 1); |
306 val gg2_lepoll_m = result(); |
346 by (forward_tac [lt_oadd_disj1] 1 THEN (REPEAT (ares_tac [lt_Ord2] 1))); |
|
347 by (fast_tac (FOL_cs addSIs [ww2_lesspoll_succ, vv2_subset] |
|
348 addSDs [theI]) 1); |
|
349 val all_sum_lepoll_m_2 = result(); |
|
350 |
307 |
351 (* ********************************************************************** *) |
308 (* ********************************************************************** *) |
352 (* lemma ii *) |
309 (* lemma ii *) |
353 (* ********************************************************************** *) |
310 (* ********************************************************************** *) |
354 goalw thy [NN_def] |
311 goalw thy [NN_def] |
355 "!!y. [| succ(m) : NN(y); y*y <= y; m:nat; m~=0 |] ==> m : NN(y)"; |
312 "!!y. [| succ(m) : NN(y); y*y <= y; m:nat; m~=0 |] ==> m : NN(y)"; |
356 by (REPEAT (eresolve_tac [CollectE, exE, conjE] 1)); |
313 by (REPEAT (eresolve_tac [CollectE, exE, conjE] 1)); |
357 by (resolve_tac [quant_domain_uu_lepoll_m RS cases RS disjE] 1 |
314 by (resolve_tac [quant_domain_uu_lepoll_m RS cases RS disjE] 1 |
358 THEN (atac 1)); |
315 THEN (assume_tac 1)); |
359 (* case 1 *) |
316 (* case 1 *) |
360 by (resolve_tac [CollectI] 1); |
317 by (asm_full_simp_tac (ZF_ss addsimps [lesspoll_succ_iff]) 1); |
361 by (atac 1); |
318 by (res_inst_tac [("x","a++a")] exI 1); |
362 by (res_inst_tac [("x","a ++ a")] exI 1); |
319 by (fast_tac (OrdQuant_cs addSIs [Ord_oadd, domain_gg1, UN_gg1_eq, |
363 by (res_inst_tac [("x","lam b:a++a. if (b<a, vv1(f,b,succ(m)), \ |
320 gg1_lepoll_m]) 1); |
364 \ ww1(f,THE l. l<a & b=a++l,succ(m)))")] exI 1); |
|
365 by (fast_tac (FOL_cs addSIs [Ord_oadd, lam_funtype RS domain_of_fun, |
|
366 UN_eq_y, all_sum_lepoll_m]) 1); |
|
367 (* case 2 *) |
321 (* case 2 *) |
368 by (REPEAT (eresolve_tac [oexE, conjE] 1)); |
322 by (REPEAT (eresolve_tac [oexE, conjE] 1)); |
|
323 by (res_inst_tac [("A","f`?B")] not_emptyE 1 THEN (assume_tac 1)); |
369 by (resolve_tac [CollectI] 1); |
324 by (resolve_tac [CollectI] 1); |
370 by (eresolve_tac [succ_natD] 1); |
325 by (eresolve_tac [succ_natD] 1); |
371 by (res_inst_tac [("A","f`?B")] not_emptyE 1 THEN (atac 1)); |
|
372 by (res_inst_tac [("x","a++a")] exI 1); |
326 by (res_inst_tac [("x","a++a")] exI 1); |
373 by (res_inst_tac [("x","lam g:a++a. if (g<a, vv2(f,b,g,x), \ |
327 by (res_inst_tac [("x","gg2(f,a,b,x)")] exI 1); |
374 \ ww2(f,b,THE l. l<a & g=a++l,x))")] exI 1); |
328 (*Calling fast_tac might get rid of the res_inst_tac calls, but it |
375 by (fast_tac (FOL_cs addSIs [Ord_oadd, lam_funtype RS domain_of_fun, |
329 is just too slow.*) |
376 UN_eq_y_2, all_sum_lepoll_m_2]) 1); |
330 by (asm_simp_tac (OrdQuant_ss addsimps |
|
331 [Ord_oadd, domain_gg2, UN_gg2_eq, gg2_lepoll_m]) 1); |
377 val lemma_ii = result(); |
332 val lemma_ii = result(); |
378 |
333 |
379 |
334 |
380 (* ********************************************************************** *) |
335 (* ********************************************************************** *) |
381 (* lemma iv - p. 4 : *) |
336 (* lemma iv - p. 4 : *) |