# HG changeset patch
# User Christian Urban <christian dot urban at kcl dot ac dot uk>
# Date 1360121846 0
# Node ID c3832c4963c4626d64547944efee03e277047799
# Parent  7dc064e64ab271a404942c51866342d98007b493
updated recursive

diff -r 7dc064e64ab2 -r c3832c4963c4 Paper/Paper.thy
--- a/Paper/Paper.thy	Wed Feb 06 02:42:52 2013 +0000
+++ b/Paper/Paper.thy	Wed Feb 06 03:37:26 2013 +0000
@@ -1322,7 +1322,7 @@
 section {* Conclusion *}
 
 text {*
-  We have formalised the main results from six chapters in the
+  We have formalised the main computability results from Chapters 3 to 8 in the
   textbook by Boolos et al \cite{Boolos87}.  Following in the
   footsteps of another paper \cite{Nipkow98} formalising the results
   from a semantics textbook, we could have titled our paper ``Boolos et al are
diff -r 7dc064e64ab2 -r c3832c4963c4 paper.pdf
Binary file paper.pdf has changed
diff -r 7dc064e64ab2 -r c3832c4963c4 thys/recursive.thy
--- a/thys/recursive.thy	Wed Feb 06 02:42:52 2013 +0000
+++ b/thys/recursive.thy	Wed Feb 06 03:37:26 2013 +0000
@@ -4824,6 +4824,13 @@
 apply(auto simp: crsp.simps start_of.simps)
 done
 
+(* cccc *)
+
+fun tm_of_rec :: "recf \<Rightarrow> instr list"
+where "tm_of_rec recf = (let (ap, k, fp) = rec_ci recf in
+                         let tp = tm_of (ap [+] dummy_abc k) in 
+                             tp @ (shift (mopup k) (length tp div 2)))"
+
 lemma recursive_compile_to_tm_correct: 
   "\<lbrakk>rec_ci recf = (ap, ary, fp); 
     rec_calc_rel recf args r;
@@ -4859,6 +4866,27 @@
 apply(auto)
 by (metis append_Nil2 replicate_app_Cons_same)
 
+lemma recursive_compile_to_tm_correct3: 
+  assumes "rec_calc_rel recf args r"
+  shows "\<exists> m n. {\<lambda>tp. tp = ([Bk, Bk], <args>)} tm_of_rec recf {\<lambda>tp. tp = (Bk \<up> m, <r> @ Bk \<up> n)}"
+using recursive_compile_to_tm_correct2[OF _ assms] 
+apply(auto)
+apply(case_tac "rec_ci recf")
+apply(auto)
+apply(drule_tac x="a" in meta_spec)
+apply(drule_tac x="b" in meta_spec)
+apply(drule_tac x="c" in meta_spec)
+apply(drule_tac x="length args" in meta_spec)
+apply(drule_tac x="tm_of (a [+] dummy_abc (length args))" in meta_spec)
+apply(auto)
+apply(rule_tac x="m" in exI)
+apply(rule_tac x="n" in exI)
+apply(simp add: tape_of_nat_abv)
+apply(subgoal_tac "b = length args")
+apply(simp)
+by (metis assms para_pattern)
+
+
 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"