2517 by(rule_tac lm = args and stp = stp and am = "args @ rec_exec recf args # 0 \<up> m" |
2517 by(rule_tac lm = args and stp = stp and am = "args @ rec_exec recf args # 0 \<up> m" |
2518 in compile_correct_halt, auto simp: crsp.simps start_of.simps length_abc_comp abc_lm_v.simps) |
2518 in compile_correct_halt, auto simp: crsp.simps start_of.simps length_abc_comp abc_lm_v.simps) |
2519 qed |
2519 qed |
2520 |
2520 |
2521 lemma recursive_compile_to_tm_correct2: |
2521 lemma recursive_compile_to_tm_correct2: |
2522 assumes compile: "rec_ci recf = (ap, ary, fp)" |
2522 assumes termi: " terminate recf args" |
2523 and termi: " terminate recf args" |
|
2524 shows "\<exists> stp m l. steps0 (Suc 0, [Bk, Bk], <args>) (tm_of_rec recf) stp = |
2523 shows "\<exists> stp m l. steps0 (Suc 0, [Bk, Bk], <args>) (tm_of_rec recf) stp = |
2525 (0, Bk\<up>Suc (Suc m), Oc\<up>Suc (rec_exec recf args) @ Bk\<up>l)" |
2524 (0, Bk\<up>Suc (Suc m), Oc\<up>Suc (rec_exec recf args) @ Bk\<up>l)" |
2526 using recursive_compile_to_tm_correct1[of recf ap ary fp args "tm_of (ap [+] dummy_abc (length args))" "[]" 0] |
2525 proof(case_tac "rec_ci recf", simp add: tm_of_rec.simps) |
2527 assms param_pattern[of recf args ap ary fp] |
2526 fix ap ar fp |
2528 by(simp add: exp_suc replicate_Suc[THEN sym] del: replicate_Suc tm_of_rec_def) |
2527 assume "rec_ci recf = (ap, ar, fp)" |
|
2528 thus "\<exists>stp m l. steps0 (Suc 0, [Bk, Bk], <args>) |
|
2529 (tm_of (ap [+] dummy_abc ar) @ shift (mopup ar) (listsum (layout_of (ap [+] dummy_abc ar)))) stp = |
|
2530 (0, Bk # Bk # Bk \<up> m, Oc # Oc \<up> rec_exec recf args @ Bk \<up> l)" |
|
2531 using recursive_compile_to_tm_correct1[of recf ap ar fp args "tm_of (ap [+] dummy_abc (length args))" "[]" 0] |
|
2532 assms param_pattern[of recf args ap ar fp] |
|
2533 by(simp add: replicate_Suc[THEN sym] replicate_Suc_iff_anywhere del: replicate_Suc tm_of_rec_def, |
|
2534 simp add: exp_suc del: replicate_Suc) |
|
2535 qed |
2529 |
2536 |
2530 lemma recursive_compile_to_tm_correct3: |
2537 lemma recursive_compile_to_tm_correct3: |
2531 assumes compile: "rec_ci recf = (ap, ary, fp)" |
2538 assumes termi: "terminate recf args" |
2532 and termi: "terminate recf args" |
2539 shows "{\<lambda> tp. tp =([Bk, Bk], <args>)} (tm_of_rec recf) |
2533 shows "{\<lambda> (l, r). l = [Bk, Bk] \<and> r = <args>} (tm_of_rec recf) |
2540 {\<lambda> tp. \<exists> k l. tp = (Bk\<up> k, <rec_exec recf args> @ Bk \<up> l)}" |
2534 {\<lambda> (l, r). \<exists> m i. l = Bk\<up>(Suc (Suc m)) \<and> r = Oc\<up>Suc (rec_exec recf args) @ Bk \<up> i}" |
2541 using recursive_compile_to_tm_correct2[OF assms] |
2535 using recursive_compile_to_tm_correct2[of recf ap ary fp args] assms |
2542 apply(auto simp add: Hoare_halt_def) |
2536 apply(simp add: Hoare_halt_def, auto) |
2543 apply(rule_tac x = stp in exI) |
2537 apply(rule_tac x = stp in exI, simp) |
2544 apply(auto simp add: tape_of_nat_abv) |
2538 done |
2545 apply(rule_tac x = "Suc (Suc m)" in exI) |
|
2546 apply(simp) |
|
2547 done |
2539 |
2548 |
2540 lemma [simp]: |
2549 lemma [simp]: |
2541 "list_all (\<lambda>(acn, s). s \<le> Suc (Suc (Suc (Suc (Suc (Suc (2 * n))))))) xs \<Longrightarrow> |
2550 "list_all (\<lambda>(acn, s). s \<le> Suc (Suc (Suc (Suc (Suc (Suc (2 * n))))))) xs \<Longrightarrow> |
2542 list_all (\<lambda>(acn, s). s \<le> Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (2 * n))))))))) xs" |
2551 list_all (\<lambda>(acn, s). s \<le> Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (2 * n))))))))) xs" |
2543 apply(induct xs, simp, simp) |
2552 apply(induct xs, simp, simp) |