--- a/thys/recursive.thy	Tue Feb 05 12:41:00 2013 +0000
+++ b/thys/recursive.thy	Wed Feb 06 02:25:00 2013 +0000
@@ -4841,6 +4841,24 @@
 apply(simp_all add: length_append)
 done
 
+lemma recursive_compile_to_tm_correct2: 
+  assumes "rec_ci recf = (ap, ary, fp)" 
+  and     "rec_calc_rel recf args r"
+  and     "length args = k"
+  and     "tp = tm_of (ap [+] dummy_abc k)"
+  shows "\<exists> m n. {\<lambda>tp. tp = ([Bk, Bk], <args>)}
+             (tp @ (shift (mopup k) (length tp div 2)))
+             {\<lambda>tp. tp = (Bk \<up> m, Oc \<up> (Suc r) @ Bk \<up> n)}"
+using recursive_compile_to_tm_correct[where ires="[]" and rn="0", OF assms(1-3) _ assms(4)]
+apply(simp add: Hoare_halt_def)
+apply(drule_tac x="layout_of (ap [+] dummy_abc k)" in meta_spec)
+apply(auto)
+apply(rule_tac x="m + 2" in exI)
+apply(rule_tac x="l" in exI)
+apply(rule_tac x="stp" in exI)
+apply(auto)
+by (metis append_Nil2 replicate_app_Cons_same)
+
 lemma [simp]:
   "list_all (\<lambda>(acn, s). s \<le> Suc (Suc (Suc (Suc (Suc (Suc (2 * n))))))) xs \<Longrightarrow>
   list_all (\<lambda>(acn, s). s \<le> Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (2 * n))))))))) xs"