295 val [prem1,prem2] = goal LList.thy |
295 val [prem1,prem2] = goal LList.thy |
296 "[| !!x. h1(x) = sum_case (%u.NIL) (split(%z w. CONS z (h1 w))) (f x); \ |
296 "[| !!x. h1(x) = sum_case (%u.NIL) (split(%z w. CONS z (h1 w))) (f x); \ |
297 \ !!x. h2(x) = sum_case (%u.NIL) (split(%z w. CONS z (h2 w))) (f x) |]\ |
297 \ !!x. h2(x) = sum_case (%u.NIL) (split(%z w. CONS z (h2 w))) (f x) |]\ |
298 \ ==> h1=h2"; |
298 \ ==> h1=h2"; |
299 by (rtac (ntrunc_equality RS ext) 1); |
299 by (rtac (ntrunc_equality RS ext) 1); |
|
300 by (rename_tac "x k" 1); |
300 by (res_inst_tac [("x", "x")] spec 1); |
301 by (res_inst_tac [("x", "x")] spec 1); |
301 by (res_inst_tac [("n", "k")] less_induct 1); |
302 by (res_inst_tac [("n", "k")] less_induct 1); |
|
303 by (rename_tac "n" 1); |
302 by (rtac allI 1); |
304 by (rtac allI 1); |
|
305 by (rename_tac "y" 1); |
303 by (stac prem1 1); |
306 by (stac prem1 1); |
304 by (stac prem2 1); |
307 by (stac prem2 1); |
305 by (simp_tac (!simpset setloop (split_tac [expand_sum_case])) 1); |
308 by (simp_tac (!simpset setloop (split_tac [expand_sum_case])) 1); |
306 by (strip_tac 1); |
309 by (strip_tac 1); |
307 by (res_inst_tac [("n", "n")] natE 1); |
310 by (res_inst_tac [("n", "n")] natE 1); |
308 by (res_inst_tac [("n", "xb")] natE 2); |
311 by (rename_tac "m" 2); |
|
312 by (res_inst_tac [("n", "m")] natE 2); |
309 by (ALLGOALS(asm_simp_tac(!simpset addsimps |
313 by (ALLGOALS(asm_simp_tac(!simpset addsimps |
310 [ntrunc_0,ntrunc_one_CONS,ntrunc_CONS, less_Suc_eq]))); |
314 [ntrunc_0,ntrunc_one_CONS,ntrunc_CONS, less_Suc_eq]))); |
311 result(); |
315 result(); |
312 |
316 |
313 |
317 |