193 addSIs [le_add2]) 1); |
193 addSIs [le_add2]) 1); |
194 qed_spec_mp "PROJ_case"; |
194 qed_spec_mp "PROJ_case"; |
195 |
195 |
196 (** COMP case **) |
196 (** COMP case **) |
197 |
197 |
198 Goal |
198 Goal "fs : lists(PRIMREC Int {f. EX kf. ALL l. f l < ack(kf, list_add l)}) \ |
199 "!!fs. fs : lists(PRIMREC Int {f. EX kf. ALL l. f l < ack(kf, list_add l)}) \ |
199 \ ==> EX k. ALL l. list_add (map(%f. f l) fs) < ack(k, list_add l)"; |
200 \ ==> EX k. ALL l. list_add (map(%f. f l) fs) < ack(k, list_add l)"; |
|
201 by (etac lists.induct 1); |
200 by (etac lists.induct 1); |
202 by (res_inst_tac [("x","0")] exI 1 THEN Asm_simp_tac 1); |
201 by (res_inst_tac [("x","0")] exI 1 THEN Asm_simp_tac 1); |
203 by Safe_tac; |
202 by Safe_tac; |
204 by (Asm_simp_tac 1); |
203 by (Asm_simp_tac 1); |
205 by (blast_tac (claset() addIs [add_less_mono, ack_add_bound, less_trans]) 1); |
204 by (blast_tac (claset() addIs [add_less_mono, ack_add_bound, less_trans]) 1); |
206 qed "COMP_map_lemma"; |
205 qed "COMP_map_lemma"; |
207 |
206 |
208 Goalw [COMP_def] |
207 Goalw [COMP_def] |
209 "!!g. [| ALL l. g l < ack(kg, list_add l); \ |
208 "[| ALL l. g l < ack(kg, list_add l); \ |
210 \ fs: lists(PRIMREC Int {f. EX kf. ALL l. f l < ack(kf, list_add l)}) \ |
209 \ fs: lists(PRIMREC Int {f. EX kf. ALL l. f l < ack(kf, list_add l)}) \ |
211 \ |] ==> EX k. ALL l. COMP g fs l < ack(k, list_add l)"; |
210 \ |] ==> EX k. ALL l. COMP g fs l < ack(k, list_add l)"; |
212 by (forward_tac [impOfSubs (Int_lower1 RS lists_mono)] 1); |
211 by (forward_tac [impOfSubs (Int_lower1 RS lists_mono)] 1); |
213 by (etac (COMP_map_lemma RS exE) 1); |
212 by (etac (COMP_map_lemma RS exE) 1); |
214 by (rtac exI 1); |
213 by (rtac exI 1); |
215 by (rtac allI 1); |
214 by (rtac allI 1); |
216 by (REPEAT (dtac spec 1)); |
215 by (REPEAT (dtac spec 1)); |
219 qed "COMP_case"; |
218 qed "COMP_case"; |
220 |
219 |
221 (** PREC case **) |
220 (** PREC case **) |
222 |
221 |
223 Goalw [PREC_def] |
222 Goalw [PREC_def] |
224 "!!f g. [| ALL l. f l + list_add l < ack(kf, list_add l); \ |
223 "[| ALL l. f l + list_add l < ack(kf, list_add l); \ |
225 \ ALL l. g l + list_add l < ack(kg, list_add l) \ |
224 \ ALL l. g l + list_add l < ack(kg, list_add l) \ |
226 \ |] ==> PREC f g l + list_add l < ack(Suc(kf+kg), list_add l)"; |
225 \ |] ==> PREC f g l + list_add l < ack(Suc(kf+kg), list_add l)"; |
227 by (exhaust_tac "l" 1); |
226 by (exhaust_tac "l" 1); |
228 by (ALLGOALS Asm_simp_tac); |
227 by (ALLGOALS Asm_simp_tac); |
229 by (blast_tac (claset() addIs [less_trans]) 1); |
228 by (blast_tac (claset() addIs [less_trans]) 1); |
230 by (etac ssubst 1); (*get rid of the needless assumption*) |
229 by (etac ssubst 1); (*get rid of the needless assumption*) |
231 by (induct_tac "a" 1); |
230 by (induct_tac "a" 1); |
242 by (Asm_simp_tac 1); |
241 by (Asm_simp_tac 1); |
243 by (rtac (le_add2 RS ack_le_mono1 RS le_less_trans) 1); |
242 by (rtac (le_add2 RS ack_le_mono1 RS le_less_trans) 1); |
244 by (etac ack_less_mono2 1); |
243 by (etac ack_less_mono2 1); |
245 qed "PREC_case_lemma"; |
244 qed "PREC_case_lemma"; |
246 |
245 |
247 Goal |
246 Goal "[| ALL l. f l < ack(kf, list_add l); \ |
248 "!!f g. [| ALL l. f l < ack(kf, list_add l); \ |
247 \ ALL l. g l < ack(kg, list_add l) \ |
249 \ ALL l. g l < ack(kg, list_add l) \ |
248 \ |] ==> EX k. ALL l. PREC f g l< ack(k, list_add l)"; |
250 \ |] ==> EX k. ALL l. PREC f g l< ack(k, list_add l)"; |
|
251 by (rtac exI 1); |
249 by (rtac exI 1); |
252 by (rtac allI 1); |
250 by (rtac allI 1); |
253 by (rtac ([le_add1, PREC_case_lemma] MRS le_less_trans) 1); |
251 by (rtac ([le_add1, PREC_case_lemma] MRS le_less_trans) 1); |
254 by (REPEAT (blast_tac (claset() addIs [ack_add_bound2]) 1)); |
252 by (REPEAT (blast_tac (claset() addIs [ack_add_bound2]) 1)); |
255 qed "PREC_case"; |
253 qed "PREC_case"; |