4822 lemma [simp]: "crsp (layout_of (ap [+] dummy_abc k)) (0, args) |
4822 lemma [simp]: "crsp (layout_of (ap [+] dummy_abc k)) (0, args) |
4823 (Suc 0, Bk # Bk # ires, <args> @ Bk \<up> rn) ires" |
4823 (Suc 0, Bk # Bk # ires, <args> @ Bk \<up> rn) ires" |
4824 apply(auto simp: crsp.simps start_of.simps) |
4824 apply(auto simp: crsp.simps start_of.simps) |
4825 done |
4825 done |
4826 |
4826 |
|
4827 (* cccc *) |
|
4828 |
|
4829 fun tm_of_rec :: "recf \<Rightarrow> instr list" |
|
4830 where "tm_of_rec recf = (let (ap, k, fp) = rec_ci recf in |
|
4831 let tp = tm_of (ap [+] dummy_abc k) in |
|
4832 tp @ (shift (mopup k) (length tp div 2)))" |
|
4833 |
4827 lemma recursive_compile_to_tm_correct: |
4834 lemma recursive_compile_to_tm_correct: |
4828 "\<lbrakk>rec_ci recf = (ap, ary, fp); |
4835 "\<lbrakk>rec_ci recf = (ap, ary, fp); |
4829 rec_calc_rel recf args r; |
4836 rec_calc_rel recf args r; |
4830 length args = k; |
4837 length args = k; |
4831 ly = layout_of (ap [+] dummy_abc k); |
4838 ly = layout_of (ap [+] dummy_abc k); |
4857 apply(rule_tac x="l" in exI) |
4864 apply(rule_tac x="l" in exI) |
4858 apply(rule_tac x="stp" in exI) |
4865 apply(rule_tac x="stp" in exI) |
4859 apply(auto) |
4866 apply(auto) |
4860 by (metis append_Nil2 replicate_app_Cons_same) |
4867 by (metis append_Nil2 replicate_app_Cons_same) |
4861 |
4868 |
|
4869 lemma recursive_compile_to_tm_correct3: |
|
4870 assumes "rec_calc_rel recf args r" |
|
4871 shows "\<exists> m n. {\<lambda>tp. tp = ([Bk, Bk], <args>)} tm_of_rec recf {\<lambda>tp. tp = (Bk \<up> m, <r> @ Bk \<up> n)}" |
|
4872 using recursive_compile_to_tm_correct2[OF _ assms] |
|
4873 apply(auto) |
|
4874 apply(case_tac "rec_ci recf") |
|
4875 apply(auto) |
|
4876 apply(drule_tac x="a" in meta_spec) |
|
4877 apply(drule_tac x="b" in meta_spec) |
|
4878 apply(drule_tac x="c" in meta_spec) |
|
4879 apply(drule_tac x="length args" in meta_spec) |
|
4880 apply(drule_tac x="tm_of (a [+] dummy_abc (length args))" in meta_spec) |
|
4881 apply(auto) |
|
4882 apply(rule_tac x="m" in exI) |
|
4883 apply(rule_tac x="n" in exI) |
|
4884 apply(simp add: tape_of_nat_abv) |
|
4885 apply(subgoal_tac "b = length args") |
|
4886 apply(simp) |
|
4887 by (metis assms para_pattern) |
|
4888 |
|
4889 |
4862 lemma [simp]: |
4890 lemma [simp]: |
4863 "list_all (\<lambda>(acn, s). s \<le> Suc (Suc (Suc (Suc (Suc (Suc (2 * n))))))) xs \<Longrightarrow> |
4891 "list_all (\<lambda>(acn, s). s \<le> Suc (Suc (Suc (Suc (Suc (Suc (2 * n))))))) xs \<Longrightarrow> |
4864 list_all (\<lambda>(acn, s). s \<le> Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (2 * n))))))))) xs" |
4892 list_all (\<lambda>(acn, s). s \<le> Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (2 * n))))))))) xs" |
4865 apply(induct xs, simp, simp) |
4893 apply(induct xs, simp, simp) |
4866 apply(case_tac a, simp) |
4894 apply(case_tac a, simp) |