4839 apply(frule_tac tp = tp and n = k |
4839 apply(frule_tac tp = tp and n = k |
4840 and ires = ires in compile_correct_halt, simp_all add: length_append) |
4840 and ires = ires in compile_correct_halt, simp_all add: length_append) |
4841 apply(simp_all add: length_append) |
4841 apply(simp_all add: length_append) |
4842 done |
4842 done |
4843 |
4843 |
|
4844 lemma recursive_compile_to_tm_correct2: |
|
4845 assumes "rec_ci recf = (ap, ary, fp)" |
|
4846 and "rec_calc_rel recf args r" |
|
4847 and "length args = k" |
|
4848 and "tp = tm_of (ap [+] dummy_abc k)" |
|
4849 shows "\<exists> m n. {\<lambda>tp. tp = ([Bk, Bk], <args>)} |
|
4850 (tp @ (shift (mopup k) (length tp div 2))) |
|
4851 {\<lambda>tp. tp = (Bk \<up> m, Oc \<up> (Suc r) @ Bk \<up> n)}" |
|
4852 using recursive_compile_to_tm_correct[where ires="[]" and rn="0", OF assms(1-3) _ assms(4)] |
|
4853 apply(simp add: Hoare_halt_def) |
|
4854 apply(drule_tac x="layout_of (ap [+] dummy_abc k)" in meta_spec) |
|
4855 apply(auto) |
|
4856 apply(rule_tac x="m + 2" in exI) |
|
4857 apply(rule_tac x="l" in exI) |
|
4858 apply(rule_tac x="stp" in exI) |
|
4859 apply(auto) |
|
4860 by (metis append_Nil2 replicate_app_Cons_same) |
|
4861 |
4844 lemma [simp]: |
4862 lemma [simp]: |
4845 "list_all (\<lambda>(acn, s). s \<le> Suc (Suc (Suc (Suc (Suc (Suc (2 * n))))))) xs \<Longrightarrow> |
4863 "list_all (\<lambda>(acn, s). s \<le> Suc (Suc (Suc (Suc (Suc (Suc (2 * n))))))) xs \<Longrightarrow> |
4846 list_all (\<lambda>(acn, s). s \<le> Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (2 * n))))))))) xs" |
4864 list_all (\<lambda>(acn, s). s \<le> Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (2 * n))))))))) xs" |
4847 apply(induct xs, simp, simp) |
4865 apply(induct xs, simp, simp) |
4848 apply(case_tac a, simp) |
4866 apply(case_tac a, simp) |