equal
deleted
inserted
replaced
4866 apply(auto) |
4866 apply(auto) |
4867 by (metis append_Nil2 replicate_app_Cons_same) |
4867 by (metis append_Nil2 replicate_app_Cons_same) |
4868 |
4868 |
4869 lemma recursive_compile_to_tm_correct3: |
4869 lemma recursive_compile_to_tm_correct3: |
4870 assumes "rec_calc_rel recf args r" |
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)}" |
4871 shows "{\<lambda>tp. tp = ([Bk, Bk], <args>)} tm_of_rec recf {\<lambda>tp. \<exists>k l. tp = (Bk \<up> k, <r> @ Bk \<up> l)}" |
4872 using recursive_compile_to_tm_correct2[OF _ assms] |
4872 using recursive_compile_to_tm_correct2[OF _ assms] |
4873 apply(auto) |
4873 apply(auto) |
4874 apply(case_tac "rec_ci recf") |
4874 apply(case_tac "rec_ci recf") |
4875 apply(auto) |
4875 apply(auto) |
4876 apply(drule_tac x="a" in meta_spec) |
4876 apply(drule_tac x="a" in meta_spec) |