tm: comparison thys/Recursive.thy

equal deleted inserted replaced

-:89ed51d72e4a
+:aea02b5a58d2
 fun addition :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> abc_prog"
 where
 "addition m n p = [Dec m 4, Inc n, Inc p, Goto 0, Dec p 7, Inc m, Goto 4]"
-(* moves register m to register n *)
 fun mv_box :: "nat \<Rightarrow> nat \<Rightarrow> abc_prog"
 where
 "mv_box m n = [Dec m 3, Inc n, Goto 0]"
 text {* The compilation of @{text "z"}-operator. *}
 "rec_ci_z \<equiv> [Goto 1]"
 text {* The compilation of @{text "s"}-operator. *}
 definition rec_ci_s :: "abc_inst list"
 where
-"rec_ci_s \<equiv> addition 0 1 2 [+] [Inc 1]"
+"rec_ci_s \<equiv> (addition 0 1 2 [+] [Inc 1])"
 text {* The compilation of @{text "id i j"}-operator *}
 fun rec_ci_id :: "nat \<Rightarrow> nat \<Rightarrow> abc_inst list"
 where
 fun empty_boxes :: "nat \<Rightarrow> abc_inst list"
 where
 "empty_boxes 0 = []" |
 "empty_boxes (Suc n) = empty_boxes n [+] [Dec n 2, Goto 0]"
-fun cn_merge_gs :: "(abc_inst list \<times> nat \<times> nat) list \<Rightarrow> nat \<Rightarrow> abc_inst list"
+fun cn_merge_gs ::
+"(abc_inst list \<times> nat \<times> nat) list \<Rightarrow> nat \<Rightarrow> abc_inst list"
 where
 "cn_merge_gs [] p = []" |
 "cn_merge_gs (g # gs) p =
 (let (gprog, gpara, gn) = g in
 gprog [+] mv_box gpara p [+] cn_merge_gs gs (Suc p))"
 mv_box.simps[simp del] addition.simps[simp del]
 declare abc_steps_l.simps[simp del] abc_fetch.simps[simp del]
 abc_step_l.simps[simp del]
-fun addition_inv :: "nat \<times> nat list \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat list \<Rightarrow> bool"
+inductive_cases terminate_pr_reverse: "terminate (Pr n f g) xs"
+inductive_cases terminate_z_reverse[elim!]: "terminate z xs"
+inductive_cases terminate_s_reverse[elim!]: "terminate s xs"
+inductive_cases terminate_id_reverse[elim!]: "terminate (id m n) xs"
+inductive_cases terminate_cn_reverse[elim!]: "terminate (Cn n f gs) xs"
+inductive_cases terminate_mn_reverse[elim!]:"terminate (Mn n f) xs"
+fun addition_inv :: "nat \<times> nat list \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow>
+nat list \<Rightarrow> bool"
 where
 "addition_inv (as, lm') m n p lm =
 (let sn = lm ! n in
 let sm = lm ! m in
 lm ! p = 0 \<and>
 else if as = 5 then 2
 else if as = 6 then 1
 else if as = 4 then 0
 else 0)"
-fun addition_measure :: "((nat \<times> nat list) \<times> nat \<times> nat) \<Rightarrow> (nat \<times> nat \<times> nat)"
+fun addition_measure :: "((nat \<times> nat list) \<times> nat \<times> nat) \<Rightarrow>
+(nat \<times> nat \<times> nat)"
 where
 "addition_measure ((as, lm), m, p) =
 (addition_stage1 (as, lm) m p,
 addition_stage2 (as, lm) m p,
 addition_stage3 (as, lm) m p)"
-definition addition_LE :: "(((nat \<times> nat list) \<times> nat \<times> nat) \<times> ((nat \<times> nat list) \<times> nat \<times> nat)) set"
+definition addition_LE :: "(((nat \<times> nat list) \<times> nat \<times> nat) \<times>
+((nat \<times> nat list) \<times> nat \<times> nat)) set"
 where "addition_LE \<equiv> (inv_image lex_triple addition_measure)"
 lemma [simp]: "wf addition_LE"
-by(auto simp: wf_inv_image addition_LE_def lex_triple_def lex_pair_def)
+by(auto simp: wf_inv_image addition_LE_def lex_triple_def
+lex_pair_def)
 declare addition_inv.simps[simp del]
 lemma addition_inv_init:
 "\<lbrakk>m \<noteq> n; max m n < p; length lm > p; lm ! p = 0\<rbrakk> \<Longrightarrow>
 apply(auto)
 done
 qed
 lemma compile_s_correct':
-"{\<lambda>nl. nl = n # 0 \<up> 2 @ anything}
+"{\<lambda>nl. nl = n # 0 \<up> 2 @ anything} addition 0 (Suc 0) 2 [+] [Inc (Suc 0)] {\<lambda>nl. nl = n # Suc n # 0 # anything}"
-addition 0 (Suc 0) 2 [+] [Inc (Suc 0)]
-{\<lambda>nl. nl = n # Suc n # 0 # anything}"
 proof(rule_tac abc_Hoare_plus_halt)
-show "{\<lambda>nl. nl = n # 0 \<up> 2 @ anything}
+show "{\<lambda>nl. nl = n # 0 \<up> 2 @ anything} addition 0 (Suc 0) 2 {\<lambda> nl. addition_inv (7, nl) 0 (Suc 0) 2 (n # 0 \<up> 2 @ anything)}"
-addition 0 (Suc 0) 2
-{\<lambda>nl. addition_inv (7, nl) 0 (Suc 0) 2 (n # 0 \<up> 2 @ anything)}"
 by(rule_tac addition_correct, auto simp: numeral_2_eq_2)
 next
-show "{\<lambda>nl. addition_inv (7, nl) 0 (Suc 0) 2 (n # 0 \<up> 2 @ anything)}
+show "{\<lambda>nl. addition_inv (7, nl) 0 (Suc 0) 2 (n # 0 \<up> 2 @ anything)} [Inc (Suc 0)] {\<lambda>nl. nl = n # Suc n # 0 # anything}"
-[Inc (Suc 0)]
-{\<lambda>nl. nl = n # Suc n # 0 # anything}"
 by(rule_tac abc_Hoare_haltI, rule_tac x = 1 in exI, auto simp: addition_inv.simps
 abc_steps_l.simps abc_step_l.simps abc_fetch.simps numeral_2_eq_2 abc_lm_s.simps abc_lm_v.simps)
 qed
-declare rec_eval.simps[simp del]
+declare rec_exec.simps[simp del]
 lemma abc_comp_commute: "(A [+] B) [+] C = A [+] (B [+] C)"
 apply(auto simp: abc_comp.simps abc_shift.simps)
 apply(case_tac x, auto)
 done
 lemma compile_z_correct:
-"\<lbrakk>rec_ci z = (ap, arity, fp); rec_eval z [n] = r\<rbrakk> \<Longrightarrow>
+"\<lbrakk>rec_ci z = (ap, arity, fp); rec_exec z [n] = r\<rbrakk> \<Longrightarrow>
 {\<lambda>nl. nl = n # 0 \<up> (fp - arity) @ anything} ap {\<lambda>nl. nl = n # r # 0 \<up> (fp - Suc arity) @ anything}"
 apply(rule_tac abc_Hoare_haltI)
 apply(rule_tac x = 1 in exI)
 apply(auto simp: abc_steps_l.simps rec_ci.simps rec_ci_z_def
-numeral_2_eq_2 abc_fetch.simps abc_step_l.simps rec_eval.simps)
+numeral_2_eq_2 abc_fetch.simps abc_step_l.simps rec_exec.simps)
 done
 lemma compile_s_correct:
-"\<lbrakk>rec_ci s = (ap, arity, fp); rec_eval s [n] = r\<rbrakk> \<Longrightarrow>
+"\<lbrakk>rec_ci s = (ap, arity, fp); rec_exec s [n] = r\<rbrakk> \<Longrightarrow>
 {\<lambda>nl. nl = n # 0 \<up> (fp - arity) @ anything} ap {\<lambda>nl. nl = n # r # 0 \<up> (fp - Suc arity) @ anything}"
-apply(auto simp: rec_ci.simps rec_ci_s_def compile_s_correct' rec_eval.simps)
+apply(auto simp: rec_ci.simps rec_ci_s_def compile_s_correct' rec_exec.simps)
 done
 lemma compile_id_correct':
 assumes "n < length args"
 shows "{\<lambda>nl. nl = args @ 0 \<up> 2 @ anything} addition n (length args) (Suc (length args))
-{\<lambda>nl. nl = args @ rec_eval (recf.id (length args) n) args # 0 # anything}"
+{\<lambda>nl. nl = args @ rec_exec (recf.id (length args) n) args # 0 # anything}"
 proof -
 have "{\<lambda>nl. nl = args @ 0 \<up> 2 @ anything} addition n (length args) (Suc (length args))
 {\<lambda>nl. addition_inv (7, nl) n (length args) (Suc (length args)) (args @ 0 \<up> 2 @ anything)}"
 using assms
 by(rule_tac addition_correct, auto simp: numeral_2_eq_2 nth_append)
 thus "?thesis"
 using assms
-by(simp add: addition_inv.simps rec_eval.simps
+by(simp add: addition_inv.simps rec_exec.simps
 nth_append numeral_2_eq_2 list_update_append)
 qed
 lemma compile_id_correct:
-"\<lbrakk>n < m; length xs = m; rec_ci (recf.id m n) = (ap, arity, fp); rec_eval (recf.id m n) xs = r\<rbrakk>
+"\<lbrakk>n < m; length xs = m; rec_ci (recf.id m n) = (ap, arity, fp); rec_exec (recf.id m n) xs = r\<rbrakk>
 \<Longrightarrow> {\<lambda>nl. nl = xs @ 0 \<up> (fp - arity) @ anything} ap {\<lambda>nl. nl = xs @ r # 0 \<up> (fp - Suc arity) @ anything}"
 apply(auto simp: rec_ci.simps rec_ci_id.simps compile_id_correct')
 done
 lemma cn_merge_gs_tl_app:
 apply(case_tac "rec_ci a1", case_tac "rec_ci a2", auto)
 apply(case_tac "rec_ci a", auto)
 done
 lemma param_pattern:
-"\<lbrakk>terminates f xs; rec_ci f = (p, arity, fp)\<rbrakk> \<Longrightarrow> length xs = arity"
+"\<lbrakk>terminate f xs; rec_ci f = (p, arity, fp)\<rbrakk> \<Longrightarrow> length xs = arity"
-apply(induct arbitrary: p arity fp rule: terminates.induct)
+apply(induct arbitrary: p arity fp rule: terminate.induct)
 apply(auto simp: rec_ci.simps)
 apply(case_tac "rec_ci f", simp)
 apply(case_tac "rec_ci f", case_tac "rec_ci g", simp)
 apply(case_tac "rec_ci f", case_tac "rec_ci gs", simp)
 done
 declare list_update.simps(2)[simp del]
 lemma [simp]:
 "\<lbrakk>length xs < gf; gf \<le> ft; n < length gs\<rbrakk>
-\<Longrightarrow> (rec_eval (gs ! n) xs # 0 \<up> (ft - Suc (length xs)) @ map (\<lambda>i. rec_eval i xs) (take n gs) @ 0 \<up> (length gs - n) @ 0 # 0 \<up> length xs @ anything)
+\<Longrightarrow> (rec_exec (gs ! n) xs # 0 \<up> (ft - Suc (length xs)) @ map (\<lambda>i. rec_exec i xs) (take n gs) @ 0 \<up> (length gs - n) @ 0 # 0 \<up> length xs @ anything)
-[ft + n - length xs := rec_eval (gs ! n) xs, 0 := 0] =
+[ft + n - length xs := rec_exec (gs ! n) xs, 0 := 0] =
-0 \<up> (ft - length xs) @ map (\<lambda>i. rec_eval i xs) (take n gs) @ rec_eval (gs ! n) xs # 0 \<up> (length gs - Suc n) @ 0 # 0 \<up> length xs @ anything"
+0 \<up> (ft - length xs) @ map (\<lambda>i. rec_exec i xs) (take n gs) @ rec_exec (gs ! n) xs # 0 \<up> (length gs - Suc n) @ 0 # 0 \<up> length xs @ anything"
-using list_update_append[of "rec_eval (gs ! n) xs # 0 \<up> (ft - Suc (length xs)) @ map (\<lambda>i. rec_eval i xs) (take n gs)"
+using list_update_append[of "rec_exec (gs ! n) xs # 0 \<up> (ft - Suc (length xs)) @ map (\<lambda>i. rec_exec i xs) (take n gs)"
-"0 \<up> (length gs - n) @ 0 # 0 \<up> length xs @ anything" "ft + n - length xs" "rec_eval (gs ! n) xs"]
+"0 \<up> (length gs - n) @ 0 # 0 \<up> length xs @ anything" "ft + n - length xs" "rec_exec (gs ! n) xs"]
 apply(auto)
 apply(case_tac "length gs - n", simp, simp add: list_update.simps replicate_Suc_iff_anywhere Suc_diff_Suc del: replicate_Suc)
 apply(simp add: list_update.simps)
 done
 lemma compile_cn_gs_correct':
 assumes
-g_cond: "\<forall>g\<in>set (take n gs). terminates g xs \<and>
+g_cond: "\<forall>g\<in>set (take n gs). terminate g xs \<and>
-(\<forall>x xa xb. rec_ci g = (x, xa, xb) \<longrightarrow> (\<forall>xc. {\<lambda>nl. nl = xs @ 0 \<up> (xb - xa) @ xc} x {\<lambda>nl. nl = xs @ rec_eval g xs # 0 \<up> (xb - Suc xa) @ xc}))"
+(\<forall>x xa xb. rec_ci g = (x, xa, xb) \<longrightarrow> (\<forall>xc. {\<lambda>nl. nl = xs @ 0 \<up> (xb - xa) @ xc} x {\<lambda>nl. nl = xs @ rec_exec g xs # 0 \<up> (xb - Suc xa) @ xc}))"
 and ft: "ft = max (Suc (length xs)) (Max (insert ffp ((\<lambda>(aprog, p, n). n) ` rec_ci ` set gs)))"
 shows
 "{\<lambda>nl. nl = xs @ 0 # 0 \<up> (ft + length gs) @ anything}
 cn_merge_gs (map rec_ci (take n gs)) ft
 {\<lambda>nl. nl = xs @ 0 \<up> (ft - length xs) @
-map (\<lambda>i. rec_eval i xs) (take n gs) @ 0\<up>(length gs - n) @ 0 \<up> Suc (length xs) @ anything}"
+map (\<lambda>i. rec_exec i xs) (take n gs) @ 0\<up>(length gs - n) @ 0 \<up> Suc (length xs) @ anything}"
 using g_cond
 proof(induct n)
 case 0
 have "ft > length xs"
 using ft
 replicate_Suc[THEN sym] del: replicate_Suc)
 done
 next
 case (Suc n)
 have ind': "\<forall>g\<in>set (take n gs).
-terminates g xs \<and> (\<forall>x xa xb. rec_ci g = (x, xa, xb) \<longrightarrow>
+terminate g xs \<and> (\<forall>x xa xb. rec_ci g = (x, xa, xb) \<longrightarrow>
-(\<forall>xc. {\<lambda>nl. nl = xs @ 0 \<up> (xb - xa) @ xc} x {\<lambda>nl. nl = xs @ rec_eval g xs # 0 \<up> (xb - Suc xa) @ xc})) \<Longrightarrow>
+(\<forall>xc. {\<lambda>nl. nl = xs @ 0 \<up> (xb - xa) @ xc} x {\<lambda>nl. nl = xs @ rec_exec g xs # 0 \<up> (xb - Suc xa) @ xc})) \<Longrightarrow>
 {\<lambda>nl. nl = xs @ 0 # 0 \<up> (ft + length gs) @ anything} cn_merge_gs (map rec_ci (take n gs)) ft
-{\<lambda>nl. nl = xs @ 0 \<up> (ft - length xs) @ map (\<lambda>i. rec_eval i xs) (take n gs) @ 0 \<up> (length gs - n) @ 0 \<up> Suc (length xs) @ anything}"
+{\<lambda>nl. nl = xs @ 0 \<up> (ft - length xs) @ map (\<lambda>i. rec_exec i xs) (take n gs) @ 0 \<up> (length gs - n) @ 0 \<up> Suc (length xs) @ anything}"
 by fact
 have g_newcond: "\<forall>g\<in>set (take (Suc n) gs).
-terminates g xs \<and> (\<forall>x xa xb. rec_ci g = (x, xa, xb) \<longrightarrow> (\<forall>xc. {\<lambda>nl. nl = xs @ 0 \<up> (xb - xa) @ xc} x {\<lambda>nl. nl = xs @ rec_eval g xs # 0 \<up> (xb - Suc xa) @ xc}))"
+terminate g xs \<and> (\<forall>x xa xb. rec_ci g = (x, xa, xb) \<longrightarrow> (\<forall>xc. {\<lambda>nl. nl = xs @ 0 \<up> (xb - xa) @ xc} x {\<lambda>nl. nl = xs @ rec_exec g xs # 0 \<up> (xb - Suc xa) @ xc}))"
 by fact
 from g_newcond have ind:
 "{\<lambda>nl. nl = xs @ 0 # 0 \<up> (ft + length gs) @ anything} cn_merge_gs (map rec_ci (take n gs)) ft
-{\<lambda>nl. nl = xs @ 0 \<up> (ft - length xs) @ map (\<lambda>i. rec_eval i xs) (take n gs) @ 0 \<up> (length gs - n) @ 0 \<up> Suc (length xs) @ anything}"
+{\<lambda>nl. nl = xs @ 0 \<up> (ft - length xs) @ map (\<lambda>i. rec_exec i xs) (take n gs) @ 0 \<up> (length gs - n) @ 0 \<up> Suc (length xs) @ anything}"
 apply(rule_tac ind', rule_tac ballI, erule_tac x = g in ballE, simp_all add: take_Suc)
 by(case_tac "n < length gs", simp add:take_Suc_conv_app_nth, simp)
 show "?case"
 proof(cases "n < length gs")
 case True
 moreover have "min (length gs) n = n"
 using h by simp
 moreover have
 "{\<lambda>nl. nl = xs @ 0 # 0 \<up> (ft + length gs) @ anything}
 cn_merge_gs (map rec_ci (take n gs)) ft [+] (gp [+] mv_box ga (ft + n))
-{\<lambda>nl. nl = xs @ 0 \<up> (ft - length xs) @ map (\<lambda>i. rec_eval i xs) (take n gs) @
+{\<lambda>nl. nl = xs @ 0 \<up> (ft - length xs) @ map (\<lambda>i. rec_exec i xs) (take n gs) @
-rec_eval (gs ! n) xs # 0 \<up> (length gs - Suc n) @ 0 # 0 \<up> length xs @ anything}"
+rec_exec (gs ! n) xs # 0 \<up> (length gs - Suc n) @ 0 # 0 \<up> length xs @ anything}"
 proof(rule_tac abc_Hoare_plus_halt)
 show "{\<lambda>nl. nl = xs @ 0 # 0 \<up> (ft + length gs) @ anything} cn_merge_gs (map rec_ci (take n gs)) ft
-{\<lambda>nl. nl = xs @ 0 \<up> (ft - length xs) @ map (\<lambda>i. rec_eval i xs) (take n gs) @ 0 \<up> (length gs - n) @ 0 \<up> Suc (length xs) @ anything}"
+{\<lambda>nl. nl = xs @ 0 \<up> (ft - length xs) @ map (\<lambda>i. rec_exec i xs) (take n gs) @ 0 \<up> (length gs - n) @ 0 \<up> Suc (length xs) @ anything}"
 using ind by simp
 next
 have x: "gs!n \<in> set (take (Suc n) gs)"
 using h
 by(simp add: take_Suc_conv_app_nth)
-have b: "terminates (gs!n) xs"
+have b: "terminate (gs!n) xs"
 using a g_newcond h x
 by(erule_tac x = "gs!n" in ballE, simp_all)
 hence c: "length xs = ga"
 using a param_pattern by metis
 have d: "gf > ga" using footprint_ge a by simp
 by(simp,  rule_tac min_max.le_supI2, rule_tac Max_ge, simp,
 rule_tac insertI2,
 rule_tac f = "(\<lambda>(aprog, p, n). n)" and x = "rec_ci (gs!n)" in image_eqI, simp,
 rule_tac x = "gs!n" in image_eqI, simp, simp)
 show "{\<lambda>nl. nl = xs @ 0 \<up> (ft - length xs) @
-map (\<lambda>i. rec_eval i xs) (take n gs) @ 0 \<up> (length gs - n) @ 0 \<up> Suc (length xs) @ anything} gp [+] mv_box ga (ft + n)
+map (\<lambda>i. rec_exec i xs) (take n gs) @ 0 \<up> (length gs - n) @ 0 \<up> Suc (length xs) @ anything} gp [+] mv_box ga (ft + n)
-{\<lambda>nl. nl = xs @ 0 \<up> (ft - length xs) @ map (\<lambda>i. rec_eval i xs)
+{\<lambda>nl. nl = xs @ 0 \<up> (ft - length xs) @ map (\<lambda>i. rec_exec i xs)
-(take n gs) @ rec_eval (gs ! n) xs # 0 \<up> (length gs - Suc n) @ 0 # 0 \<up> length xs @ anything}"
+(take n gs) @ rec_exec (gs ! n) xs # 0 \<up> (length gs - Suc n) @ 0 # 0 \<up> length xs @ anything}"
 proof(rule_tac abc_Hoare_plus_halt)
-show "{\<lambda>nl. nl = xs @ 0 \<up> (ft - length xs) @ map (\<lambda>i. rec_eval i xs) (take n gs) @ 0 \<up> (length gs - n) @ 0 \<up> Suc (length xs) @ anything} gp
+show "{\<lambda>nl. nl = xs @ 0 \<up> (ft - length xs) @ map (\<lambda>i. rec_exec i xs) (take n gs) @ 0 \<up> (length gs - n) @ 0 \<up> Suc (length xs) @ anything} gp
-{\<lambda>nl. nl = xs @ (rec_eval (gs!n) xs) # 0 \<up> (ft - Suc (length xs)) @ map (\<lambda>i. rec_eval i xs)
+{\<lambda>nl. nl = xs @ (rec_exec (gs!n) xs) # 0 \<up> (ft - Suc (length xs)) @ map (\<lambda>i. rec_exec i xs)
 (take n gs) @  0 \<up> (length gs - n) @ 0 # 0 \<up> length xs @ anything}"
 proof -
 have
-"({\<lambda>nl. nl = xs @ 0 \<up> (gf - ga) @ 0\<up>(ft - gf)@map (\<lambda>i. rec_eval i xs) (take n gs) @ 0 \<up> (length gs - n) @ 0 \<up> Suc (length xs) @ anything}
+"({\<lambda>nl. nl = xs @ 0 \<up> (gf - ga) @ 0\<up>(ft - gf)@map (\<lambda>i. rec_exec i xs) (take n gs) @ 0 \<up> (length gs - n) @ 0 \<up> Suc (length xs) @ anything}
-gp {\<lambda>nl. nl = xs @ (rec_eval (gs!n) xs) # 0 \<up> (gf - Suc ga) @
+gp {\<lambda>nl. nl = xs @ (rec_exec (gs!n) xs) # 0 \<up> (gf - Suc ga) @
-0\<up>(ft - gf)@map (\<lambda>i. rec_eval i xs) (take n gs) @ 0 \<up> (length gs - n) @ 0 \<up> Suc (length xs) @ anything})"
+0\<up>(ft - gf)@map (\<lambda>i. rec_exec i xs) (take n gs) @ 0 \<up> (length gs - n) @ 0 \<up> Suc (length xs) @ anything})"
 using a g_newcond h x
 apply(erule_tac x = "gs!n" in ballE)
 apply(simp, simp)
 done
 thus "?thesis"
 using a b c d e
 by(simp add: replicate_merge_anywhere)
 qed
 next
 show
-"{\<lambda>nl. nl = xs @ rec_eval (gs ! n) xs #
+"{\<lambda>nl. nl = xs @ rec_exec (gs ! n) xs #
-0 \<up> (ft - Suc (length xs)) @ map (\<lambda>i. rec_eval i xs) (take n gs) @ 0 \<up> (length gs - n) @ 0 # 0 \<up> length xs @ anything}
+0 \<up> (ft - Suc (length xs)) @ map (\<lambda>i. rec_exec i xs) (take n gs) @ 0 \<up> (length gs - n) @ 0 # 0 \<up> length xs @ anything}
 mv_box ga (ft + n)
-{\<lambda>nl. nl = xs @ 0 \<up> (ft - length xs) @ map (\<lambda>i. rec_eval i xs) (take n gs) @
+{\<lambda>nl. nl = xs @ 0 \<up> (ft - length xs) @ map (\<lambda>i. rec_exec i xs) (take n gs) @
-rec_eval (gs ! n) xs # 0 \<up> (length gs - Suc n) @ 0 # 0 \<up> length xs @ anything}"
+rec_exec (gs ! n) xs # 0 \<up> (length gs - Suc n) @ 0 # 0 \<up> length xs @ anything}"
 proof -
-have "{\<lambda>nl. nl = xs @ rec_eval (gs ! n) xs # 0 \<up> (ft - Suc (length xs)) @
+have "{\<lambda>nl. nl = xs @ rec_exec (gs ! n) xs # 0 \<up> (ft - Suc (length xs)) @
-map (\<lambda>i. rec_eval i xs) (take n gs) @ 0 \<up> (length gs - n) @ 0 # 0 \<up> length xs @ anything}
+map (\<lambda>i. rec_exec i xs) (take n gs) @ 0 \<up> (length gs - n) @ 0 # 0 \<up> length xs @ anything}
-mv_box ga (ft + n) {\<lambda>nl. nl = (xs @ rec_eval (gs ! n) xs # 0 \<up> (ft - Suc (length xs)) @
+mv_box ga (ft + n) {\<lambda>nl. nl = (xs @ rec_exec (gs ! n) xs # 0 \<up> (ft - Suc (length xs)) @
-map (\<lambda>i. rec_eval i xs) (take n gs) @ 0 \<up> (length gs - n) @ 0 # 0 \<up> length xs @ anything)
+map (\<lambda>i. rec_exec i xs) (take n gs) @ 0 \<up> (length gs - n) @ 0 # 0 \<up> length xs @ anything)
-[ft + n := (xs @ rec_eval (gs ! n) xs # 0 \<up> (ft - Suc (length xs)) @ map (\<lambda>i. rec_eval i xs) (take n gs) @
+[ft + n := (xs @ rec_exec (gs ! n) xs # 0 \<up> (ft - Suc (length xs)) @ map (\<lambda>i. rec_exec i xs) (take n gs) @
 0 \<up> (length gs - n) @ 0 # 0 \<up> length xs @ anything) ! ga +
-(xs @ rec_eval (gs ! n) xs # 0 \<up> (ft - Suc (length xs)) @
+(xs @ rec_exec (gs ! n) xs # 0 \<up> (ft - Suc (length xs)) @
-map (\<lambda>i. rec_eval i xs) (take n gs) @ 0 \<up> (length gs - n) @ 0 # 0 \<up> length xs @ anything) !
+map (\<lambda>i. rec_exec i xs) (take n gs) @ 0 \<up> (length gs - n) @ 0 # 0 \<up> length xs @ anything) !
 (ft + n),  ga := 0]}"
 using a c d e h
 apply(rule_tac mv_box_correct)
 apply(simp, arith, arith)
 done
-moreover have "(xs @ rec_eval (gs ! n) xs # 0 \<up> (ft - Suc (length xs)) @
+moreover have "(xs @ rec_exec (gs ! n) xs # 0 \<up> (ft - Suc (length xs)) @
-map (\<lambda>i. rec_eval i xs) (take n gs) @ 0 \<up> (length gs - n) @ 0 # 0 \<up> length xs @ anything)
+map (\<lambda>i. rec_exec i xs) (take n gs) @ 0 \<up> (length gs - n) @ 0 # 0 \<up> length xs @ anything)
-[ft + n := (xs @ rec_eval (gs ! n) xs # 0 \<up> (ft - Suc (length xs)) @ map (\<lambda>i. rec_eval i xs) (take n gs) @
+[ft + n := (xs @ rec_exec (gs ! n) xs # 0 \<up> (ft - Suc (length xs)) @ map (\<lambda>i. rec_exec i xs) (take n gs) @
 0 \<up> (length gs - n) @ 0 # 0 \<up> length xs @ anything) ! ga +
-(xs @ rec_eval (gs ! n) xs # 0 \<up> (ft - Suc (length xs)) @
+(xs @ rec_exec (gs ! n) xs # 0 \<up> (ft - Suc (length xs)) @
-map (\<lambda>i. rec_eval i xs) (take n gs) @ 0 \<up> (length gs - n) @ 0 # 0 \<up> length xs @ anything) !
+map (\<lambda>i. rec_exec i xs) (take n gs) @ 0 \<up> (length gs - n) @ 0 # 0 \<up> length xs @ anything) !
 (ft + n),  ga := 0]=
-xs @ 0 \<up> (ft - length xs) @ map (\<lambda>i. rec_eval i xs) (take n gs) @ rec_eval (gs ! n) xs # 0 \<up> (length gs - Suc n) @ 0 # 0 \<up> length xs @ anything"
+xs @ 0 \<up> (ft - length xs) @ map (\<lambda>i. rec_exec i xs) (take n gs) @ rec_exec (gs ! n) xs # 0 \<up> (length gs - Suc n) @ 0 # 0 \<up> length xs @ anything"
 using a c d e h
 by(simp add: list_update_append nth_append length_replicate split: if_splits del: list_update.simps(2), auto)
 ultimately show "?thesis"
 by(simp)
 qed
 qed
 ultimately show
 "{\<lambda>nl. nl = xs @ 0 # 0 \<up> (ft + length gs) @ anything}
 cn_merge_gs (map rec_ci (take n gs)) ft [+] (case rec_ci (gs ! n) of (gprog, gpara, gn) \<Rightarrow>
 gprog [+] mv_box gpara (ft + min (length gs) n))
-{\<lambda>nl. nl = xs @ 0 \<up> (ft - length xs) @ map (\<lambda>i. rec_eval i xs) (take n gs) @ rec_eval (gs ! n) xs # 0 \<up> (length gs - Suc n) @ 0 # 0 \<up> length xs @ anything}"
+{\<lambda>nl. nl = xs @ 0 \<up> (ft - length xs) @ map (\<lambda>i. rec_exec i xs) (take n gs) @ rec_exec (gs ! n) xs # 0 \<up> (length gs - Suc n) @ 0 # 0 \<up> length xs @ anything}"
 by simp
 qed
 next
 case False
 have h: "\<not> n < length gs" by fact
 hence ind':
 "{\<lambda>nl. nl = xs @ 0 # 0 \<up> (ft + length gs) @ anything} cn_merge_gs (map rec_ci gs) ft
-{\<lambda>nl. nl = xs @ 0 \<up> (ft - length xs) @ map (\<lambda>i. rec_eval i xs) gs @ 0 \<up> Suc (length xs) @ anything}"
+{\<lambda>nl. nl = xs @ 0 \<up> (ft - length xs) @ map (\<lambda>i. rec_exec i xs) gs @ 0 \<up> Suc (length xs) @ anything}"
 using ind
 by simp
 thus "?thesis"
 using h
 by(simp)
 qed
 qed
 lemma compile_cn_gs_correct:
 assumes
-g_cond: "\<forall>g\<in>set gs. terminates g xs \<and>
+g_cond: "\<forall>g\<in>set gs. terminate g xs \<and>
-(\<forall>x xa xb. rec_ci g = (x, xa, xb) \<longrightarrow> (\<forall>xc. {\<lambda>nl. nl = xs @ 0 \<up> (xb - xa) @ xc} x {\<lambda>nl. nl = xs @ rec_eval g xs # 0 \<up> (xb - Suc xa) @ xc}))"
+(\<forall>x xa xb. rec_ci g = (x, xa, xb) \<longrightarrow> (\<forall>xc. {\<lambda>nl. nl = xs @ 0 \<up> (xb - xa) @ xc} x {\<lambda>nl. nl = xs @ rec_exec g xs # 0 \<up> (xb - Suc xa) @ xc}))"
 and ft: "ft = max (Suc (length xs)) (Max (insert ffp ((\<lambda>(aprog, p, n). n) ` rec_ci ` set gs)))"
 shows
 "{\<lambda>nl. nl = xs @ 0 # 0 \<up> (ft + length gs) @ anything}
 cn_merge_gs (map rec_ci gs) ft
 {\<lambda>nl. nl = xs @ 0 \<up> (ft - length xs) @
-map (\<lambda>i. rec_eval i xs) gs @ 0 \<up> Suc (length xs) @ anything}"
+map (\<lambda>i. rec_exec i xs) gs @ 0 \<up> Suc (length xs) @ anything}"
 using assms
 using compile_cn_gs_correct'[of "length gs" gs xs ft ffp anything ]
 apply(auto)
 done
 by(simp add: mv_boxes.simps)
 qed
 lemma save_paras:
 "{\<lambda>nl. nl = xs @ 0 \<up> (max (Suc (length xs)) (Max (insert ffp ((\<lambda>(aprog, p, n). n) ` rec_ci ` set gs))) - length xs) @
-map (\<lambda>i. rec_eval i xs) gs @ 0 \<up> Suc (length xs) @ anything}
+map (\<lambda>i. rec_exec i xs) gs @ 0 \<up> Suc (length xs) @ anything}
 mv_boxes 0 (Suc (max (Suc (length xs)) (Max (insert ffp ((\<lambda>(aprog, p, n). n) ` rec_ci ` set gs))) + length gs)) (length xs)
-{\<lambda>nl. nl = 0 \<up> max (Suc (length xs)) (Max (insert ffp ((\<lambda>(aprog, p, n). n) ` rec_ci ` set gs))) @ map (\<lambda>i. rec_eval i xs) gs @ 0 # xs @ anything}"
+{\<lambda>nl. nl = 0 \<up> max (Suc (length xs)) (Max (insert ffp ((\<lambda>(aprog, p, n). n) ` rec_ci ` set gs))) @ map (\<lambda>i. rec_exec i xs) gs @ 0 # xs @ anything}"
 proof -
 let ?ft = "max (Suc (length xs)) (Max (insert ffp ((\<lambda>(aprog, p, n). n) ` rec_ci ` set gs)))"
-have "{\<lambda>nl. nl = [] @ xs @ (0\<up>(?ft - length xs) @  map (\<lambda>i. rec_eval i xs) gs @ [0]) @
+have "{\<lambda>nl. nl = [] @ xs @ (0\<up>(?ft - length xs) @  map (\<lambda>i. rec_exec i xs) gs @ [0]) @
 0 \<up> (length xs) @ anything} mv_boxes 0 (Suc ?ft + length gs) (length xs)
-{\<lambda>nl. nl = [] @ 0 \<up> (length xs) @ (0\<up>(?ft - length xs) @  map (\<lambda>i. rec_eval i xs) gs @ [0]) @ xs @ anything}"
+{\<lambda>nl. nl = [] @ 0 \<up> (length xs) @ (0\<up>(?ft - length xs) @  map (\<lambda>i. rec_exec i xs) gs @ [0]) @ xs @ anything}"
 by(rule_tac mv_boxes_correct, auto)
 thus "?thesis"
 by(simp add: replicate_merge_anywhere)
 qed
 apply(simp add: Max_ge_iff)
 done
 lemma restore_new_paras:
 "ffp \<ge> length gs
-\<Longrightarrow> {\<lambda>nl. nl = 0 \<up> max (Suc (length xs)) (Max (insert ffp ((\<lambda>(aprog, p, n). n) ` rec_ci ` set gs))) @ map (\<lambda>i. rec_eval i xs) gs @ 0 # xs @ anything}
+\<Longrightarrow> {\<lambda>nl. nl = 0 \<up> max (Suc (length xs)) (Max (insert ffp ((\<lambda>(aprog, p, n). n) ` rec_ci ` set gs))) @ map (\<lambda>i. rec_exec i xs) gs @ 0 # xs @ anything}
 mv_boxes (max (Suc (length xs)) (Max (insert ffp ((\<lambda>(aprog, p, n). n) ` rec_ci ` set gs)))) 0 (length gs)
-{\<lambda>nl. nl = map (\<lambda>i. rec_eval i xs) gs @ 0 \<up> max (Suc (length xs)) (Max (insert ffp ((\<lambda>(aprog, p, n). n) ` rec_ci ` set gs))) @ 0 # xs @ anything}"
+{\<lambda>nl. nl = map (\<lambda>i. rec_exec i xs) gs @ 0 \<up> max (Suc (length xs)) (Max (insert ffp ((\<lambda>(aprog, p, n). n) ` rec_ci ` set gs))) @ 0 # xs @ anything}"
 proof -
 let ?ft = "max (Suc (length xs)) (Max (insert ffp ((\<lambda>(aprog, p, n). n) ` rec_ci ` set gs)))"
 assume j: "ffp \<ge> length gs"
-hence "{\<lambda> nl. nl = [] @ 0\<up>length gs @ 0\<up>(?ft - length gs) @  map (\<lambda>i. rec_eval i xs) gs @ ((0 # xs) @ anything)}
+hence "{\<lambda> nl. nl = [] @ 0\<up>length gs @ 0\<up>(?ft - length gs) @  map (\<lambda>i. rec_exec i xs) gs @ ((0 # xs) @ anything)}
 mv_boxes ?ft 0 (length gs)
-{\<lambda> nl. nl = [] @ map (\<lambda>i. rec_eval i xs) gs @ 0\<up>(?ft - length gs) @ 0\<up>length gs @ ((0 # xs) @ anything)}"
+{\<lambda> nl. nl = [] @ map (\<lambda>i. rec_exec i xs) gs @ 0\<up>(?ft - length gs) @ 0\<up>length gs @ ((0 # xs) @ anything)}"
 by(rule_tac mv_boxes_correct2, auto)
 moreover have "?ft \<ge> length gs"
 using j
 by(auto)
 ultimately show "?thesis"
 lemma save_rs:
 "\<lbrakk>far = length gs;
 ffp \<le> max (Suc (length xs)) (Max (insert ffp ((\<lambda>(aprog, p, n). n) ` rec_ci ` set gs)));
 far < ffp\<rbrakk>
-\<Longrightarrow>  {\<lambda>nl. nl = map (\<lambda>i. rec_eval i xs) gs @
+\<Longrightarrow>  {\<lambda>nl. nl = map (\<lambda>i. rec_exec i xs) gs @
-rec_eval (Cn (length xs) f gs) xs # 0 \<up> max (Suc (length xs))
+rec_exec (Cn (length xs) f gs) xs # 0 \<up> max (Suc (length xs))
 (Max (insert ffp ((\<lambda>(aprog, p, n). n) ` rec_ci ` set gs))) @ xs @ anything}
 mv_box far (max (Suc (length xs)) (Max (insert ffp ((\<lambda>(aprog, p, n). n) ` rec_ci ` set gs))))
-{\<lambda>nl. nl = map (\<lambda>i. rec_eval i xs) gs @
+{\<lambda>nl. nl = map (\<lambda>i. rec_exec i xs) gs @
 0 \<up> (max (Suc (length xs)) (Max (insert ffp ((\<lambda>(aprog, p, n). n) ` rec_ci ` set gs))) - length gs) @
-rec_eval (Cn (length xs) f gs) xs # 0 \<up> length gs @ xs @ anything}"
+rec_exec (Cn (length xs) f gs) xs # 0 \<up> length gs @ xs @ anything}"
 proof -
 let ?ft = "max (Suc (length xs)) (Max (insert ffp ((\<lambda>(aprog, p, n). n) ` rec_ci ` set gs)))"
 thm mv_box_correct
-let ?lm= " map (\<lambda>i. rec_eval i xs) gs @ rec_eval (Cn (length xs) f gs) xs # 0 \<up> ?ft @ xs @ anything"
+let ?lm= " map (\<lambda>i. rec_exec i xs) gs @ rec_exec (Cn (length xs) f gs) xs # 0 \<up> ?ft @ xs @ anything"
 assume h: "far = length gs" "ffp \<le> ?ft" "far < ffp"
 hence "{\<lambda> nl. nl = ?lm} mv_box far ?ft {\<lambda> nl. nl = ?lm[?ft := ?lm!far + ?lm!?ft, far := 0]}"
 apply(rule_tac mv_box_correct)
 by(case_tac "rec_ci a", auto)
 moreover have "?lm[?ft := ?lm!far + ?lm!?ft, far := 0]
-= map (\<lambda>i. rec_eval i xs) gs @
+= map (\<lambda>i. rec_exec i xs) gs @
 0 \<up> (?ft - length gs) @
-rec_eval (Cn (length xs) f gs) xs # 0 \<up> length gs @ xs @ anything"
+rec_exec (Cn (length xs) f gs) xs # 0 \<up> length gs @ xs @ anything"
 using h
 apply(simp add: nth_append)
-using list_update_length[of "map (\<lambda>i. rec_eval i xs) gs @ rec_eval (Cn (length xs) f gs) xs #
+using list_update_length[of "map (\<lambda>i. rec_exec i xs) gs @ rec_exec (Cn (length xs) f gs) xs #
-0 \<up> (?ft - Suc (length gs))" 0 "0 \<up> length gs @ xs @ anything" "rec_eval (Cn (length xs) f gs) xs"]
+0 \<up> (?ft - Suc (length gs))" 0 "0 \<up> length gs @ xs @ anything" "rec_exec (Cn (length xs) f gs) xs"]
 apply(simp add: replicate_merge_anywhere replicate_Suc_iff_anywhere del: replicate_Suc)
 by(simp add: list_update_append list_update.simps replicate_Suc_iff_anywhere del: replicate_Suc)
 ultimately show "?thesis"
 by(simp)
 qed
 done
 lemma clean_paras:
 "ffp \<ge> length gs \<Longrightarrow>
-{\<lambda>nl. nl = map (\<lambda>i. rec_eval i xs) gs @
+{\<lambda>nl. nl = map (\<lambda>i. rec_exec i xs) gs @
 0 \<up> (max (Suc (length xs)) (Max (insert ffp ((\<lambda>(aprog, p, n). n) ` rec_ci ` set gs))) - length gs) @
-rec_eval (Cn (length xs) f gs) xs # 0 \<up> length gs @ xs @ anything}
+rec_exec (Cn (length xs) f gs) xs # 0 \<up> length gs @ xs @ anything}
 empty_boxes (length gs)
 {\<lambda>nl. nl = 0 \<up> max (Suc (length xs)) (Max (insert ffp ((\<lambda>(aprog, p, n). n) ` rec_ci ` set gs))) @
-rec_eval (Cn (length xs) f gs) xs # 0 \<up> length gs @ xs @ anything}"
+rec_exec (Cn (length xs) f gs) xs # 0 \<up> length gs @ xs @ anything}"
 proof-
 let ?ft = "max (Suc (length xs)) (Max (insert ffp ((\<lambda>(aprog, p, n). n) ` rec_ci ` set gs)))"
 assume h: "length gs \<le> ffp"
-let ?lm = "map (\<lambda>i. rec_eval i xs) gs @ 0 \<up> (?ft - length gs) @
+let ?lm = "map (\<lambda>i. rec_exec i xs) gs @ 0 \<up> (?ft - length gs) @
-rec_eval (Cn (length xs) f gs) xs # 0 \<up> length gs @ xs @ anything"
+rec_exec (Cn (length xs) f gs) xs # 0 \<up> length gs @ xs @ anything"
 have "{\<lambda> nl. nl = ?lm} empty_boxes (length gs) {\<lambda> nl. nl = 0\<up>length gs @ drop (length gs) ?lm}"
 by(rule_tac empty_boxes_correct, simp)
 moreover have "0\<up>length gs @ drop (length gs) ?lm
-=  0 \<up> ?ft @  rec_eval (Cn (length xs) f gs) xs # 0 \<up> length gs @ xs @ anything"
+=  0 \<up> ?ft @  rec_exec (Cn (length xs) f gs) xs # 0 \<up> length gs @ xs @ anything"
 using h
 by(simp add: replicate_merge_anywhere)
 ultimately show "?thesis"
 by metis
 qed
 lemma restore_rs:
 "{\<lambda>nl. nl = 0 \<up> max (Suc (length xs)) (Max (insert ffp ((\<lambda>(aprog, p, n). n) ` rec_ci ` set gs))) @
-rec_eval (Cn (length xs) f gs) xs # 0 \<up> length gs @ xs @ anything}
+rec_exec (Cn (length xs) f gs) xs # 0 \<up> length gs @ xs @ anything}
 mv_box (max (Suc (length xs)) (Max (insert ffp ((\<lambda>(aprog, p, n). n) ` rec_ci ` set gs)))) (length xs)
 {\<lambda>nl. nl = 0 \<up> length xs @
-rec_eval (Cn (length xs) f gs) xs #
+rec_exec (Cn (length xs) f gs) xs #
 0 \<up> (max (Suc (length xs)) (Max (insert ffp ((\<lambda>(aprog, p, n). n) ` rec_ci ` set gs))) - (length xs)) @
 0 \<up> length gs @ xs @ anything}"
 proof -
 let ?ft = "max (Suc (length xs)) (Max (insert ffp ((\<lambda>(aprog, p, n). n) ` rec_ci ` set gs)))"
-let ?lm = "0\<up>(length xs) @  0\<up>(?ft - (length xs)) @ rec_eval (Cn (length xs) f gs) xs # 0 \<up> length gs @ xs @ anything"
+let ?lm = "0\<up>(length xs) @  0\<up>(?ft - (length xs)) @ rec_exec (Cn (length xs) f gs) xs # 0 \<up> length gs @ xs @ anything"
 thm mv_box_correct
 have "{\<lambda> nl. nl = ?lm} mv_box ?ft (length xs) {\<lambda> nl. nl = ?lm[length xs := ?lm!?ft + ?lm!(length xs), ?ft := 0]}"
 by(rule_tac mv_box_correct, simp, simp)
 moreover have "?lm[length xs := ?lm!?ft + ?lm!(length xs), ?ft := 0]
-=  0 \<up> length xs @ rec_eval (Cn (length xs) f gs) xs # 0 \<up> (?ft - (length xs)) @ 0 \<up> length gs @ xs @ anything"
+=  0 \<up> length xs @ rec_exec (Cn (length xs) f gs) xs # 0 \<up> (?ft - (length xs)) @ 0 \<up> length gs @ xs @ anything"
 apply(auto simp: list_update_append nth_append)
 apply(case_tac ?ft, simp_all add: Suc_diff_le list_update.simps)
 apply(simp add: exp_suc replicate_Suc[THEN sym] del: replicate_Suc)
 done
 ultimately show "?thesis"
 by(simp add: replicate_merge_anywhere)
 qed
 lemma restore_orgin_paras:
 "{\<lambda>nl. nl = 0 \<up> length xs @
-rec_eval (Cn (length xs) f gs) xs #
+rec_exec (Cn (length xs) f gs) xs #
 0 \<up> (max (Suc (length xs)) (Max (insert ffp ((\<lambda>(aprog, p, n). n) ` rec_ci ` set gs))) - length xs) @ 0 \<up> length gs @ xs @ anything}
 mv_boxes (Suc (max (Suc (length xs)) (Max (insert ffp ((\<lambda>(aprog, p, n). n) ` rec_ci ` set gs))) + length gs)) 0 (length xs)
-{\<lambda>nl. nl = xs @ rec_eval (Cn (length xs) f gs) xs # 0 \<up>
+{\<lambda>nl. nl = xs @ rec_exec (Cn (length xs) f gs) xs # 0 \<up>
 (max (Suc (length xs)) (Max (insert ffp ((\<lambda>(aprog, p, n). n) ` rec_ci ` set gs))) + length gs) @ anything}"
 proof -
 let ?ft = "max (Suc (length xs)) (Max (insert ffp ((\<lambda>(aprog, p, n). n) ` rec_ci ` set gs)))"
 thm mv_boxes_correct2
-have "{\<lambda> nl. nl = [] @ 0\<up>(length xs) @ (rec_eval (Cn (length xs) f gs) xs # 0 \<up> (?ft - length xs) @ 0 \<up> length gs) @ xs @ anything}
+have "{\<lambda> nl. nl = [] @ 0\<up>(length xs) @ (rec_exec (Cn (length xs) f gs) xs # 0 \<up> (?ft - length xs) @ 0 \<up> length gs) @ xs @ anything}
 mv_boxes (Suc ?ft + length gs) 0 (length xs)
-{\<lambda> nl. nl = [] @ xs @ (rec_eval (Cn (length xs) f gs) xs # 0 \<up> (?ft - length xs) @ 0 \<up> length gs) @ 0\<up>length xs @ anything}"
+{\<lambda> nl. nl = [] @ xs @ (rec_exec (Cn (length xs) f gs) xs # 0 \<up> (?ft - length xs) @ 0 \<up> length gs) @ 0\<up>length xs @ anything}"
 by(rule_tac mv_boxes_correct2, auto)
 thus "?thesis"
 by(simp add: replicate_merge_anywhere)
 qed
 lemma compile_cn_correct':
 assumes f_ind:
-"\<And> anything r. rec_eval f (map (\<lambda>g. rec_eval g xs) gs) = rec_eval (Cn (length xs) f gs) xs \<Longrightarrow>
+"\<And> anything r. rec_exec f (map (\<lambda>g. rec_exec g xs) gs) = rec_exec (Cn (length xs) f gs) xs \<Longrightarrow>
-{\<lambda>nl. nl = map (\<lambda>g. rec_eval g xs) gs @ 0 \<up> (ffp - far) @ anything} fap
+{\<lambda>nl. nl = map (\<lambda>g. rec_exec g xs) gs @ 0 \<up> (ffp - far) @ anything} fap
-{\<lambda>nl. nl = map (\<lambda>g. rec_eval g xs) gs @ rec_eval (Cn (length xs) f gs) xs # 0 \<up> (ffp - Suc far) @ anything}"
+{\<lambda>nl. nl = map (\<lambda>g. rec_exec g xs) gs @ rec_exec (Cn (length xs) f gs) xs # 0 \<up> (ffp - Suc far) @ anything}"
 and compile: "rec_ci f = (fap, far, ffp)"
-and term_f: "terminates f (map (\<lambda>g. rec_eval g xs) gs)"
+and term_f: "terminate f (map (\<lambda>g. rec_exec g xs) gs)"
-and g_cond: "\<forall>g\<in>set gs. terminates g xs \<and>
+and g_cond: "\<forall>g\<in>set gs. terminate g xs \<and>
 (\<forall>x xa xb. rec_ci g = (x, xa, xb) \<longrightarrow>
-(\<forall>xc. {\<lambda>nl. nl = xs @ 0 \<up> (xb - xa) @ xc} x {\<lambda>nl. nl = xs @ rec_eval g xs # 0 \<up> (xb - Suc xa) @ xc}))"
+(\<forall>xc. {\<lambda>nl. nl = xs @ 0 \<up> (xb - xa) @ xc} x {\<lambda>nl. nl = xs @ rec_exec g xs # 0 \<up> (xb - Suc xa) @ xc}))"
 shows
 "{\<lambda>nl. nl = xs @ 0 # 0 \<up> (max (Suc (length xs)) (Max (insert ffp ((\<lambda>(aprog, p, n). n) ` rec_ci ` set gs))) + length gs) @ anything}
 cn_merge_gs (map rec_ci gs) (max (Suc (length xs)) (Max (insert ffp ((\<lambda>(aprog, p, n). n) ` rec_ci ` set gs)))) [+]
 (mv_boxes 0 (Suc (max (Suc (length xs)) (Max (insert ffp ((\<lambda>(aprog, p, n). n) ` rec_ci ` set gs))) + length gs)) (length xs) [+]
 (mv_boxes (max (Suc (length xs)) (Max (insert ffp ((\<lambda>(aprog, p, n). n) ` rec_ci ` set gs)))) 0 (length gs) [+]
 (fap [+] (mv_box far (max (Suc (length xs)) (Max (insert ffp ((\<lambda>(aprog, p, n). n) ` rec_ci ` set gs)))) [+]
 (empty_boxes (length gs) [+]
 (mv_box (max (Suc (length xs)) (Max (insert ffp ((\<lambda>(aprog, p, n). n) ` rec_ci ` set gs)))) (length xs) [+]
 mv_boxes (Suc (max (Suc (length xs)) (Max (insert ffp ((\<lambda>(aprog, p, n). n) ` rec_ci ` set gs))) + length gs)) 0 (length xs)))))))
-{\<lambda>nl. nl = xs @ rec_eval (Cn (length xs) f gs) xs #
+{\<lambda>nl. nl = xs @ rec_exec (Cn (length xs) f gs) xs #
 0 \<up> (max (Suc (length xs)) (Max (insert ffp ((\<lambda>(aprog, p, n). n) ` rec_ci ` set gs))) + length gs) @ anything}"
 proof -
 let ?ft = "max (Suc (length xs)) (Max (insert ffp ((\<lambda>(aprog, p, n). n) ` rec_ci ` set gs)))"
 let ?A = "cn_merge_gs (map rec_ci gs) ?ft"
 let ?B = "mv_boxes 0 (Suc (?ft+length gs)) (length xs)"
 let ?E = "mv_box far ?ft"
 let ?F = "empty_boxes (length gs)"
 let ?G = "mv_box ?ft (length xs)"
 let ?H = "mv_boxes (Suc (?ft + length gs)) 0 (length xs)"
 let ?P1 = "\<lambda>nl. nl = xs @ 0 # 0 \<up> (?ft + length gs) @ anything"
-let ?S = "\<lambda>nl. nl = xs @ rec_eval (Cn (length xs) f gs) xs # 0 \<up> (?ft + length gs) @ anything"
+let ?S = "\<lambda>nl. nl = xs @ rec_exec (Cn (length xs) f gs) xs # 0 \<up> (?ft + length gs) @ anything"
-let ?Q1 = "\<lambda> nl. nl = xs @ 0\<up>(?ft - length xs) @ map (\<lambda> i. rec_eval i xs) gs @ 0\<up>(Suc (length xs)) @ anything"
+let ?Q1 = "\<lambda> nl. nl = xs @ 0\<up>(?ft - length xs) @ map (\<lambda> i. rec_exec i xs) gs @ 0\<up>(Suc (length xs)) @ anything"
 show "{?P1} (?A [+] (?B [+] (?C [+] (?D [+] (?E [+] (?F [+] (?G [+] ?H))))))) {?S}"
 proof(rule_tac abc_Hoare_plus_halt)
 show "{?P1} ?A {?Q1}"
 using g_cond
 by(rule_tac compile_cn_gs_correct, auto)
 next
 let ?Q2 = "\<lambda>nl. nl = 0 \<up> ?ft @
-map (\<lambda>i. rec_eval i xs) gs @ 0 # xs @ anything"
+map (\<lambda>i. rec_exec i xs) gs @ 0 # xs @ anything"
 show "{?Q1} (?B [+] (?C [+] (?D [+] (?E [+] (?F [+] (?G [+] ?H)))))) {?S}"
 proof(rule_tac abc_Hoare_plus_halt)
 show "{?Q1} ?B {?Q2}"
 by(rule_tac save_paras)
 next
-let ?Q3 = "\<lambda> nl. nl = map (\<lambda>i. rec_eval i xs) gs @ 0\<up>?ft @ 0 # xs @ anything"
+let ?Q3 = "\<lambda> nl. nl = map (\<lambda>i. rec_exec i xs) gs @ 0\<up>?ft @ 0 # xs @ anything"
 show "{?Q2} (?C [+] (?D [+] (?E [+] (?F [+] (?G [+] ?H))))) {?S}"
 proof(rule_tac abc_Hoare_plus_halt)
 have "ffp \<ge> length gs"
 using compile term_f
 apply(subgoal_tac "length gs = far")
 apply(drule_tac footprint_ge, simp)
 by(drule_tac param_pattern, auto)
 thus "{?Q2} ?C {?Q3}"
 by(erule_tac restore_new_paras)
 next
-let ?Q4 = "\<lambda> nl. nl = map (\<lambda>i. rec_eval i xs) gs @ rec_eval (Cn (length xs) f gs) xs # 0\<up>?ft @ xs @ anything"
+let ?Q4 = "\<lambda> nl. nl = map (\<lambda>i. rec_exec i xs) gs @ rec_exec (Cn (length xs) f gs) xs # 0\<up>?ft @ xs @ anything"
 have a: "far = length gs"
 using compile term_f
 by(drule_tac param_pattern, auto)
 have b:"?ft \<ge> ffp"
 by auto
 have c: "ffp > far"
 using compile
 by(erule_tac footprint_ge)
 show "{?Q3} (?D [+] (?E [+] (?F [+] (?G [+] ?H)))) {?S}"
 proof(rule_tac abc_Hoare_plus_halt)
-have "{\<lambda>nl. nl = map (\<lambda>g. rec_eval g xs) gs @ 0 \<up> (ffp - far) @ 0\<up>(?ft - ffp + far) @ 0 # xs @ anything} fap
+have "{\<lambda>nl. nl = map (\<lambda>g. rec_exec g xs) gs @ 0 \<up> (ffp - far) @ 0\<up>(?ft - ffp + far) @ 0 # xs @ anything} fap
-{\<lambda>nl. nl = map (\<lambda>g. rec_eval g xs) gs @ rec_eval (Cn (length xs) f gs) xs #
+{\<lambda>nl. nl = map (\<lambda>g. rec_exec g xs) gs @ rec_exec (Cn (length xs) f gs) xs #
 0 \<up> (ffp - Suc far) @ 0\<up>(?ft - ffp + far) @ 0 # xs @ anything}"
-by(rule_tac f_ind, simp add: rec_eval.simps)
+by(rule_tac f_ind, simp add: rec_exec.simps)
 thus "{?Q3} fap {?Q4}"
 using a b c
 by(simp add: replicate_merge_anywhere,
 case_tac "?ft", simp_all add: exp_suc del: replicate_Suc)
 next
-let ?Q5 = "\<lambda>nl. nl = map (\<lambda>i. rec_eval i xs) gs @
+let ?Q5 = "\<lambda>nl. nl = map (\<lambda>i. rec_exec i xs) gs @
-0\<up>(?ft - length gs) @ rec_eval (Cn (length xs) f gs) xs # 0\<up>(length gs)@ xs @ anything"
+0\<up>(?ft - length gs) @ rec_exec (Cn (length xs) f gs) xs # 0\<up>(length gs)@ xs @ anything"
 show "{?Q4} (?E [+] (?F [+] (?G [+] ?H))) {?S}"
 proof(rule_tac abc_Hoare_plus_halt)
 from a b c show "{?Q4} ?E {?Q5}"
 by(erule_tac save_rs, simp_all)
 next
-let ?Q6 = "\<lambda>nl. nl = 0\<up>?ft @ rec_eval (Cn (length xs) f gs) xs # 0\<up>(length gs)@ xs @ anything"
+let ?Q6 = "\<lambda>nl. nl = 0\<up>?ft @ rec_exec (Cn (length xs) f gs) xs # 0\<up>(length gs)@ xs @ anything"
 show "{?Q5} (?F [+] (?G [+] ?H)) {?S}"
 proof(rule_tac abc_Hoare_plus_halt)
 have "length gs \<le> ffp" using a b c
 by simp
 thus "{?Q5} ?F {?Q6}"
 by(erule_tac clean_paras)
 next
-let ?Q7 = "\<lambda>nl. nl = 0\<up>length xs @ rec_eval (Cn (length xs) f gs) xs # 0\<up>(?ft - (length xs)) @ 0\<up>(length gs)@ xs @ anything"
+let ?Q7 = "\<lambda>nl. nl = 0\<up>length xs @ rec_exec (Cn (length xs) f gs) xs # 0\<up>(?ft - (length xs)) @ 0\<up>(length gs)@ xs @ anything"
 show "{?Q6} (?G [+] ?H) {?S}"
 proof(rule_tac abc_Hoare_plus_halt)
 show "{?Q6} ?G {?Q7}"
 by(rule_tac restore_rs)
 next
 qed
 qed
 qed
 lemma compile_cn_correct:
-assumes termi_f: "terminates f (map (\<lambda>g. rec_eval g xs) gs)"
+assumes termi_f: "terminate f (map (\<lambda>g. rec_exec g xs) gs)"
 and f_ind: "\<And>ap arity fp anything.
 rec_ci f = (ap, arity, fp)
-\<Longrightarrow> {\<lambda>nl. nl = map (\<lambda>g. rec_eval g xs) gs @ 0 \<up> (fp - arity) @ anything} ap
+\<Longrightarrow> {\<lambda>nl. nl = map (\<lambda>g. rec_exec g xs) gs @ 0 \<up> (fp - arity) @ anything} ap
-{\<lambda>nl. nl = map (\<lambda>g. rec_eval g xs) gs @ rec_eval f (map (\<lambda>g. rec_eval g xs) gs) # 0 \<up> (fp - Suc arity) @ anything}"
+{\<lambda>nl. nl = map (\<lambda>g. rec_exec g xs) gs @ rec_exec f (map (\<lambda>g. rec_exec g xs) gs) # 0 \<up> (fp - Suc arity) @ anything}"
 and g_cond:
-"\<forall>g\<in>set gs. terminates g xs \<and>
+"\<forall>g\<in>set gs. terminate g xs \<and>
-(\<forall>x xa xb. rec_ci g = (x, xa, xb) \<longrightarrow>   (\<forall>xc. {\<lambda>nl. nl = xs @ 0 \<up> (xb - xa) @ xc} x {\<lambda>nl. nl = xs @ rec_eval g xs # 0 \<up> (xb - Suc xa) @ xc}))"
+(\<forall>x xa xb. rec_ci g = (x, xa, xb) \<longrightarrow>   (\<forall>xc. {\<lambda>nl. nl = xs @ 0 \<up> (xb - xa) @ xc} x {\<lambda>nl. nl = xs @ rec_exec g xs # 0 \<up> (xb - Suc xa) @ xc}))"
 and compile: "rec_ci (Cn n f gs) = (ap, arity, fp)"
 and len: "length xs = n"
-shows "{\<lambda>nl. nl = xs @ 0 \<up> (fp - arity) @ anything} ap {\<lambda>nl. nl = xs @ rec_eval (Cn n f gs) xs # 0 \<up> (fp - Suc arity) @ anything}"
+shows "{\<lambda>nl. nl = xs @ 0 \<up> (fp - arity) @ anything} ap {\<lambda>nl. nl = xs @ rec_exec (Cn n f gs) xs # 0 \<up> (fp - Suc arity) @ anything}"
 proof(case_tac "rec_ci f")
 fix fap far ffp
 assume h: "rec_ci f = (fap, far, ffp)"
-then have f_newind: "\<And> anything .{\<lambda>nl. nl = map (\<lambda>g. rec_eval g xs) gs @ 0 \<up> (ffp - far) @ anything} fap
+then have f_newind: "\<And> anything .{\<lambda>nl. nl = map (\<lambda>g. rec_exec g xs) gs @ 0 \<up> (ffp - far) @ anything} fap
-{\<lambda>nl. nl = map (\<lambda>g. rec_eval g xs) gs @ rec_eval f (map (\<lambda>g. rec_eval g xs) gs) # 0 \<up> (ffp - Suc far) @ anything}"
+{\<lambda>nl. nl = map (\<lambda>g. rec_exec g xs) gs @ rec_exec f (map (\<lambda>g. rec_exec g xs) gs) # 0 \<up> (ffp - Suc far) @ anything}"
 by(rule_tac f_ind, simp_all)
-thus "{\<lambda>nl. nl = xs @ 0 \<up> (fp - arity) @ anything} ap {\<lambda>nl. nl = xs @ rec_eval (Cn n f gs) xs # 0 \<up> (fp - Suc arity) @ anything}"
+thus "{\<lambda>nl. nl = xs @ 0 \<up> (fp - arity) @ anything} ap {\<lambda>nl. nl = xs @ rec_exec (Cn n f gs) xs # 0 \<up> (fp - Suc arity) @ anything}"
 using compile len h termi_f g_cond
 apply(auto simp: rec_ci.simps abc_comp_commute)
 apply(rule_tac compile_cn_correct', simp_all)
 done
 qed
 lemma [simp]: "length xs < max (length xs + 3) (max fft gft)"
 by auto
 lemma save_init_rs:
 "\<lbrakk>length xs = n; ft = max (n+3) (max fft gft)\<rbrakk>
-\<Longrightarrow>  {\<lambda>nl. nl = xs @ rec_eval f xs # 0 \<up> (ft - n) @ anything} mv_box n (Suc n)
+\<Longrightarrow>  {\<lambda>nl. nl = xs @ rec_exec f xs # 0 \<up> (ft - n) @ anything} mv_box n (Suc n)
-{\<lambda>nl. nl = xs @ 0 # rec_eval f xs # 0 \<up> (ft - Suc n) @ anything}"
+{\<lambda>nl. nl = xs @ 0 # rec_exec f xs # 0 \<up> (ft - Suc n) @ anything}"
-using mv_box_correct[of n "Suc n" "xs @ rec_eval f xs # 0 \<up> (ft - n) @ anything"]
+using mv_box_correct[of n "Suc n" "xs @ rec_exec f xs # 0 \<up> (ft - n) @ anything"]
 apply(auto simp: list_update_append list_update.simps nth_append split: if_splits)
 apply(case_tac "(max (length xs + 3) (max fft gft))", simp_all add: list_update.simps Suc_diff_le)
 done
 lemma [simp]: "n + (2::nat) < max (n + 3) (max fft gft)"
 lemma [simp]: "Suc n < max (n + 3) (max fft gft)"
 by arith
 lemma [simp]:
 "length xs = n
-\<Longrightarrow> {\<lambda>nl. nl = xs @ rec_eval f xs # 0 \<up> (max (n + 3) (max fft gft) - Suc n) @ x # anything} mv_box n (Suc n)
+\<Longrightarrow> {\<lambda>nl. nl = xs @ rec_exec f xs # 0 \<up> (max (n + 3) (max fft gft) - Suc n) @ x # anything} mv_box n (Suc n)
-{\<lambda>nl. nl = xs @ 0 # rec_eval f xs # 0 \<up> (max (n + 3) (max fft gft) - Suc (Suc n)) @ x # anything}"
+{\<lambda>nl. nl = xs @ 0 # rec_exec f xs # 0 \<up> (max (n + 3) (max fft gft) - Suc (Suc n)) @ x # anything}"
-using mv_box_correct[of n "Suc n" "xs @ rec_eval f xs # 0 \<up> (max (n + 3) (max fft gft) - Suc n) @ x # anything"]
+using mv_box_correct[of n "Suc n" "xs @ rec_exec f xs # 0 \<up> (max (n + 3) (max fft gft) - Suc n) @ x # anything"]
 apply(simp add: nth_append list_update_append list_update.simps)
 apply(case_tac "max (n + 3) (max fft gft)", simp_all)
 apply(case_tac nat, simp_all add: Suc_diff_le list_update.simps)
 done
 lemma [simp]: "Suc (Suc (max (length xs + 3) (max fft gft) - Suc (Suc (length xs))))
 = max (length xs + 3) (max fft gft) - (length xs)"
 by arith
 lemma [simp]: "\<lbrakk>ft = max (n + 3) (max fft gft); length xs = n\<rbrakk> \<Longrightarrow>
-{\<lambda>nl. nl = xs @ (x - Suc y) # rec_eval (Pr n f g) (xs @ [x - Suc y]) # 0 \<up> (ft - Suc (Suc n)) @ Suc y # anything}
+{\<lambda>nl. nl = xs @ (x - Suc y) # rec_exec (Pr n f g) (xs @ [x - Suc y]) # 0 \<up> (ft - Suc (Suc n)) @ Suc y # anything}
 [Dec ft (length gap + 7)]
-{\<lambda>nl. nl = xs @ (x - Suc y) # rec_eval (Pr n f g) (xs @ [x - Suc y]) # 0 \<up> (ft - Suc (Suc n)) @ y # anything}"
+{\<lambda>nl. nl = xs @ (x - Suc y) # rec_exec (Pr n f g) (xs @ [x - Suc y]) # 0 \<up> (ft - Suc (Suc n)) @ y # anything}"
 apply(simp add: abc_Hoare_halt_def)
 apply(rule_tac x = 1 in exI)
 apply(auto simp: abc_steps_l.simps abc_step_l.simps abc_fetch.simps nth_append abc_lm_v.simps abc_lm_s.simps list_update_append)
 using list_update_length
-[of "(x - Suc y) # rec_eval (Pr (length xs) f g) (xs @ [x - Suc y]) #
+[of "(x - Suc y) # rec_exec (Pr (length xs) f g) (xs @ [x - Suc y]) #
 0 \<up> (max (length xs + 3) (max fft gft) - Suc (Suc (length xs)))" "Suc y" anything y]
 apply(simp)
 done
 lemma adjust_paras':
 "length xs = n \<Longrightarrow> {\<lambda>nl. nl = xs @ x # y # anything}  [Inc n, Dec (Suc n) 3, Goto (Suc 0)]
 {\<lambda>nl. nl = xs @ Suc x # 0 # anything}"
 using adjust_paras'[of xs n x y anything]
 by(simp add: abc_comp.simps abc_shift.simps numeral_2_eq_2 numeral_3_eq_3)
-lemma [simp]: "\<lbrakk>rec_ci g = (gap, gar, gft); \<forall>y<x. terminates g (xs @ [y, rec_eval (Pr n f g) (xs @ [y])]);
+lemma [simp]: "\<lbrakk>rec_ci g = (gap, gar, gft); \<forall>y<x. terminate g (xs @ [y, rec_exec (Pr n f g) (xs @ [y])]);
 length xs = n; Suc y\<le>x\<rbrakk> \<Longrightarrow> gar = Suc (Suc n)"
 apply(erule_tac x = y in allE, simp)
 apply(drule_tac param_pattern, auto)
 done
 apply(rule_tac x = "stp + 1" in exI)
 apply(simp only: abc_steps_add, simp)
 apply(simp add: abc_steps_l.simps abc_step_l.simps abc_fetch.simps nth_append abc_lm_v.simps abc_lm_s.simps)
 done
-lemma rec_eval_pr_0_simps: "rec_eval (Pr n f g) (xs @ [0]) = rec_eval f xs"
+lemma rec_exec_pr_0_simps: "rec_exec (Pr n f g) (xs @ [0]) = rec_exec f xs"
-by(simp add: rec_eval.simps)
+by(simp add: rec_exec.simps)
-lemma rec_eval_pr_Suc_simps: "rec_eval (Pr n f g) (xs @ [Suc y])
+lemma rec_exec_pr_Suc_simps: "rec_exec (Pr n f g) (xs @ [Suc y])
-= rec_eval g (xs @ [y, rec_eval (Pr n f g) (xs @ [y])])"
+= rec_exec g (xs @ [y, rec_exec (Pr n f g) (xs @ [y])])"
 apply(induct y)
-apply(simp add: rec_eval.simps)
+apply(simp add: rec_exec.simps)
-apply(simp add: rec_eval.simps)
+apply(simp add: rec_exec.simps)
 done
 lemma [simp]: "Suc (max (n + 3) (max fft gft) - Suc (Suc (Suc n))) = max (n + 3) (max fft gft) - Suc (Suc n)"
 by arith
 lemma pr_loop:
 assumes code: "code = ([Dec (max (n + 3) (max fft gft)) (length gap + 7)] [+] (gap [+] [Inc n, Dec (Suc n) 3, Goto (Suc 0)])) @
 [Dec (Suc (Suc n)) 0, Inc (Suc n), Goto (length gap + 4)]"
 and len: "length xs = n"
-and g_ind: "\<forall> y<x. (\<forall>anything. {\<lambda>nl. nl = xs @ y # rec_eval (Pr n f g) (xs @ [y]) # 0 \<up> (gft - gar) @ anything} gap
+and g_ind: "\<forall> y<x. (\<forall>anything. {\<lambda>nl. nl = xs @ y # rec_exec (Pr n f g) (xs @ [y]) # 0 \<up> (gft - gar) @ anything} gap
-{\<lambda>nl. nl = xs @ y # rec_eval (Pr n f g) (xs @ [y]) # rec_eval g (xs @ [y, rec_eval (Pr n f g) (xs @ [y])]) # 0 \<up> (gft - Suc gar) @ anything})"
+{\<lambda>nl. nl = xs @ y # rec_exec (Pr n f g) (xs @ [y]) # rec_exec g (xs @ [y, rec_exec (Pr n f g) (xs @ [y])]) # 0 \<up> (gft - Suc gar) @ anything})"
 and compile_g: "rec_ci g = (gap, gar, gft)"
-and termi_g: "\<forall> y<x. terminates g (xs @ [y, rec_eval (Pr n f g) (xs @ [y])])"
+and termi_g: "\<forall> y<x. terminate g (xs @ [y, rec_exec (Pr n f g) (xs @ [y])])"
 and ft: "ft = max (n + 3) (max fft gft)"
 and less: "Suc y \<le> x"
 shows
-"\<exists>stp. abc_steps_l (0, xs @ (x - Suc y) # rec_eval (Pr n f g) (xs @ [x - Suc y]) # 0 \<up> (ft - Suc (Suc n)) @ Suc y # anything)
+"\<exists>stp. abc_steps_l (0, xs @ (x - Suc y) # rec_exec (Pr n f g) (xs @ [x - Suc y]) # 0 \<up> (ft - Suc (Suc n)) @ Suc y # anything)
-code stp = (0, xs @ (x - y) # rec_eval (Pr n f g) (xs @ [x - y]) # 0 \<up> (ft - Suc (Suc n)) @ y # anything)"
+code stp = (0, xs @ (x - y) # rec_exec (Pr n f g) (xs @ [x - y]) # 0 \<up> (ft - Suc (Suc n)) @ y # anything)"
 proof -
 let ?A = "[Dec  ft (length gap + 7)]"
 let ?B = "gap"
 let ?C = "[Inc n, Dec (Suc n) 3, Goto (Suc 0)]"
 let ?D = "[Dec (Suc (Suc n)) 0, Inc (Suc n), Goto (length gap + 4)]"
-have "\<exists> stp. abc_steps_l (0, xs @ (x - Suc y) # rec_eval (Pr n f g) (xs @ [x - Suc y]) # 0 \<up> (ft - Suc (Suc n)) @ Suc y # anything)
+have "\<exists> stp. abc_steps_l (0, xs @ (x - Suc y) # rec_exec (Pr n f g) (xs @ [x - Suc y]) # 0 \<up> (ft - Suc (Suc n)) @ Suc y # anything)
 ((?A [+] (?B [+] ?C)) @ ?D) stp = (length (?A [+] (?B [+] ?C)),
-xs @ (x - y) # 0 # rec_eval g (xs @ [x - Suc y, rec_eval (Pr n f g) (xs @ [x - Suc y])])
+xs @ (x - y) # 0 # rec_exec g (xs @ [x - Suc y, rec_exec (Pr n f g) (xs @ [x - Suc y])])
 # 0 \<up> (ft - Suc (Suc (Suc n))) @ y # anything)"
 proof -
-have "\<exists> stp. abc_steps_l (0, xs @ (x - Suc y) # rec_eval (Pr n f g) (xs @ [x - Suc y]) # 0 \<up> (ft - Suc (Suc n)) @ Suc y # anything)
+have "\<exists> stp. abc_steps_l (0, xs @ (x - Suc y) # rec_exec (Pr n f g) (xs @ [x - Suc y]) # 0 \<up> (ft - Suc (Suc n)) @ Suc y # anything)
 ((?A [+] (?B [+] ?C))) stp = (length (?A [+] (?B [+] ?C)),  xs @ (x - y) # 0 #
-rec_eval g (xs @ [x - Suc y, rec_eval (Pr n f g) (xs @ [x - Suc y])]) # 0 \<up> (ft - Suc (Suc (Suc n))) @ y # anything)"
+rec_exec g (xs @ [x - Suc y, rec_exec (Pr n f g) (xs @ [x - Suc y])]) # 0 \<up> (ft - Suc (Suc (Suc n))) @ y # anything)"
 proof -
-have "{\<lambda> nl. nl = xs @ (x - Suc y) # rec_eval (Pr n f g) (xs @ [x - Suc y]) # 0 \<up> (ft - Suc (Suc n)) @ Suc y # anything}
+have "{\<lambda> nl. nl = xs @ (x - Suc y) # rec_exec (Pr n f g) (xs @ [x - Suc y]) # 0 \<up> (ft - Suc (Suc n)) @ Suc y # anything}
 (?A [+] (?B [+] ?C))
 {\<lambda> nl. nl = xs @ (x - y) # 0 #
-rec_eval g (xs @ [x - Suc y, rec_eval (Pr n f g) (xs @ [x - Suc y])]) # 0 \<up> (ft - Suc (Suc (Suc n))) @ y # anything}"
+rec_exec g (xs @ [x - Suc y, rec_exec (Pr n f g) (xs @ [x - Suc y])]) # 0 \<up> (ft - Suc (Suc (Suc n))) @ y # anything}"
 proof(rule_tac abc_Hoare_plus_halt)
-show "{\<lambda>nl. nl = xs @ (x - Suc y) # rec_eval (Pr n f g) (xs @ [x - Suc y]) # 0 \<up> (ft - Suc (Suc n)) @ Suc y # anything}
+show "{\<lambda>nl. nl = xs @ (x - Suc y) # rec_exec (Pr n f g) (xs @ [x - Suc y]) # 0 \<up> (ft - Suc (Suc n)) @ Suc y # anything}
 [Dec ft (length gap + 7)]
-{\<lambda>nl. nl = xs @ (x - Suc y) # rec_eval (Pr n f g) (xs @ [x - Suc y]) # 0 \<up> (ft - Suc (Suc n)) @ y # anything}"
+{\<lambda>nl. nl = xs @ (x - Suc y) # rec_exec (Pr n f g) (xs @ [x - Suc y]) # 0 \<up> (ft - Suc (Suc n)) @ y # anything}"
 using ft len
 by(simp)
 next
 show
-"{\<lambda>nl. nl = xs @ (x - Suc y) # rec_eval (Pr n f g) (xs @ [x - Suc y]) # 0 \<up> (ft - Suc (Suc n)) @ y # anything}
+"{\<lambda>nl. nl = xs @ (x - Suc y) # rec_exec (Pr n f g) (xs @ [x - Suc y]) # 0 \<up> (ft - Suc (Suc n)) @ y # anything}
 ?B [+] ?C
-{\<lambda>nl. nl = xs @ (x - y) # 0 # rec_eval g (xs @ [x - Suc y, rec_eval (Pr n f g) (xs @ [x - Suc y])]) # 0 \<up> (ft - Suc (Suc (Suc n))) @ y # anything}"
+{\<lambda>nl. nl = xs @ (x - y) # 0 # rec_exec g (xs @ [x - Suc y, rec_exec (Pr n f g) (xs @ [x - Suc y])]) # 0 \<up> (ft - Suc (Suc (Suc n))) @ y # anything}"
 proof(rule_tac abc_Hoare_plus_halt)
 have a: "gar = Suc (Suc n)"
 using compile_g termi_g len less
 by simp
 have b: "gft > gar"
 using compile_g
 by(erule_tac footprint_ge)
-show "{\<lambda>nl. nl = xs @ (x - Suc y) # rec_eval (Pr n f g) (xs @ [x - Suc y]) # 0 \<up> (ft - Suc (Suc n)) @ y # anything} gap
+show "{\<lambda>nl. nl = xs @ (x - Suc y) # rec_exec (Pr n f g) (xs @ [x - Suc y]) # 0 \<up> (ft - Suc (Suc n)) @ y # anything} gap
-{\<lambda>nl. nl = xs @ (x - Suc y) # rec_eval (Pr n f g) (xs @ [x - Suc y]) #
+{\<lambda>nl. nl = xs @ (x - Suc y) # rec_exec (Pr n f g) (xs @ [x - Suc y]) #
-rec_eval g (xs @ [x - Suc y, rec_eval (Pr n f g) (xs @ [x - Suc y])]) # 0 \<up> (ft - Suc (Suc (Suc n))) @ y # anything}"
+rec_exec g (xs @ [x - Suc y, rec_exec (Pr n f g) (xs @ [x - Suc y])]) # 0 \<up> (ft - Suc (Suc (Suc n))) @ y # anything}"
 proof -
 have
-"{\<lambda>nl. nl = xs @ (x - Suc y) # rec_eval (Pr n f g) (xs @ [x - Suc y]) # 0 \<up> (gft - gar) @ 0\<up>(ft - gft) @ y # anything} gap
+"{\<lambda>nl. nl = xs @ (x - Suc y) # rec_exec (Pr n f g) (xs @ [x - Suc y]) # 0 \<up> (gft - gar) @ 0\<up>(ft - gft) @ y # anything} gap
-{\<lambda>nl. nl = xs @ (x - Suc y) # rec_eval (Pr n f g) (xs @ [x - Suc y]) #
+{\<lambda>nl. nl = xs @ (x - Suc y) # rec_exec (Pr n f g) (xs @ [x - Suc y]) #
-rec_eval g (xs @ [(x - Suc y), rec_eval (Pr n f g) (xs @ [x - Suc y])]) # 0 \<up> (gft - Suc gar) @ 0\<up>(ft - gft) @ y # anything}"
+rec_exec g (xs @ [(x - Suc y), rec_exec (Pr n f g) (xs @ [x - Suc y])]) # 0 \<up> (gft - Suc gar) @ 0\<up>(ft - gft) @ y # anything}"
 using g_ind less by simp
 thus "?thesis"
 using a b ft
 by(simp add: replicate_merge_anywhere numeral_3_eq_3)
 qed
 next
 show "{\<lambda>nl. nl = xs @ (x - Suc y) #
-rec_eval (Pr n f g) (xs @ [x - Suc y]) #
+rec_exec (Pr n f g) (xs @ [x - Suc y]) #
-rec_eval g (xs @ [x - Suc y, rec_eval (Pr n f g) (xs @ [x - Suc y])]) # 0 \<up> (ft - Suc (Suc (Suc n))) @ y # anything}
+rec_exec g (xs @ [x - Suc y, rec_exec (Pr n f g) (xs @ [x - Suc y])]) # 0 \<up> (ft - Suc (Suc (Suc n))) @ y # anything}
 [Inc n, Dec (Suc n) 3, Goto (Suc 0)]
-{\<lambda>nl. nl = xs @ (x - y) # 0 # rec_eval g (xs @ [x - Suc y, rec_eval (Pr n f g)
+{\<lambda>nl. nl = xs @ (x - y) # 0 # rec_exec g (xs @ [x - Suc y, rec_exec (Pr n f g)
 (xs @ [x - Suc y])]) # 0 \<up> (ft - Suc (Suc (Suc n))) @ y # anything}"
 using len less
-using adjust_paras[of xs n "x - Suc y" " rec_eval (Pr n f g) (xs @ [x - Suc y])"
+using adjust_paras[of xs n "x - Suc y" " rec_exec (Pr n f g) (xs @ [x - Suc y])"
-" rec_eval g (xs @ [x - Suc y, rec_eval (Pr n f g) (xs @ [x - Suc y])]) #
+" rec_exec g (xs @ [x - Suc y, rec_exec (Pr n f g) (xs @ [x - Suc y])]) #
 0 \<up> (ft - Suc (Suc (Suc n))) @ y # anything"]
 by(simp add: Suc_diff_Suc)
 qed
 qed
 thus "?thesis"
-by(simp add: abc_Hoare_halt_def, auto, rule_tac x = na in exI, case_tac "abc_steps_l (0, xs @ (x - Suc y) # rec_eval (Pr n f g) (xs @ [x - Suc y]) #
+by(simp add: abc_Hoare_halt_def, auto, rule_tac x = na in exI, case_tac "abc_steps_l (0, xs @ (x - Suc y) # rec_exec (Pr n f g) (xs @ [x - Suc y]) #
 0 \<up> (ft - Suc (Suc n)) @ Suc y # anything)
 ([Dec ft (length gap + 7)] [+] (gap [+] [Inc n, Dec (Suc n) 3, Goto (Suc 0)])) na", simp)
 qed
-then obtain stpa where "abc_steps_l (0, xs @ (x - Suc y) # rec_eval (Pr n f g) (xs @ [x - Suc y]) # 0 \<up> (ft - Suc (Suc n)) @ Suc y # anything)
+then obtain stpa where "abc_steps_l (0, xs @ (x - Suc y) # rec_exec (Pr n f g) (xs @ [x - Suc y]) # 0 \<up> (ft - Suc (Suc n)) @ Suc y # anything)
 ((?A [+] (?B [+] ?C))) stpa = (length (?A [+] (?B [+] ?C)),
-xs @ (x - y) # 0 # rec_eval g (xs @ [x - Suc y, rec_eval (Pr n f g) (xs @ [x - Suc y])])
+xs @ (x - y) # 0 # rec_exec g (xs @ [x - Suc y, rec_exec (Pr n f g) (xs @ [x - Suc y])])
 # 0 \<up> (ft - Suc (Suc (Suc n))) @ y # anything)" ..
 thus "?thesis"
 by(erule_tac abc_append_frist_steps_halt_eq)
 qed
 moreover have
 "\<exists> stp. abc_steps_l (length (?A [+] (?B [+] ?C)),
-xs @ (x - y) # 0 # rec_eval g (xs @ [x - Suc y, rec_eval (Pr n f g) (xs @ [x - Suc y])]) # 0 \<up> (ft - Suc (Suc (Suc n))) @ y # anything)
+xs @ (x - y) # 0 # rec_exec g (xs @ [x - Suc y, rec_exec (Pr n f g) (xs @ [x - Suc y])]) # 0 \<up> (ft - Suc (Suc (Suc n))) @ y # anything)
-((?A [+] (?B [+] ?C)) @ ?D) stp  = (0, xs @ (x - y) # rec_eval g (xs @ [x - Suc y, rec_eval (Pr n f g) (xs @ [x - Suc y])]) #
+((?A [+] (?B [+] ?C)) @ ?D) stp  = (0, xs @ (x - y) # rec_exec g (xs @ [x - Suc y, rec_exec (Pr n f g) (xs @ [x - Suc y])]) #
 0 # 0 \<up> (ft - Suc (Suc (Suc n))) @ y # anything)"
 using len
 by(rule_tac loop_back, simp_all)
-moreover have "rec_eval g (xs @ [x - Suc y, rec_eval (Pr n f g) (xs @ [x - Suc y])]) = rec_eval (Pr n f g) (xs @ [x - y])"
+moreover have "rec_exec g (xs @ [x - Suc y, rec_exec (Pr n f g) (xs @ [x - Suc y])]) = rec_exec (Pr n f g) (xs @ [x - y])"
 using less
-thm rec_eval.simps
+thm rec_exec.simps
-apply(case_tac "x - y", simp_all add: rec_eval_pr_Suc_simps)
+apply(case_tac "x - y", simp_all add: rec_exec_pr_Suc_simps)
 by(subgoal_tac "nat = x - Suc y", simp, arith)
 ultimately show "?thesis"
 using code ft
 by(auto, rule_tac x = "stp + stpa" in exI, simp add: abc_steps_add replicate_Suc_iff_anywhere del: replicate_Suc)
 qed
 lemma [simp]:
-"length xs = n \<Longrightarrow> abc_lm_s (xs @ x # rec_eval (Pr n f g) (xs @ [x]) # 0 \<up> (max (n + 3)
+"length xs = n \<Longrightarrow> abc_lm_s (xs @ x # rec_exec (Pr n f g) (xs @ [x]) # 0 \<up> (max (n + 3)
 (max fft gft) - Suc (Suc n)) @ 0 # anything) (max (n + 3) (max fft gft)) 0 =
-xs @ x # rec_eval (Pr n f g) (xs @ [x]) # 0 \<up> (max (n + 3) (max fft gft) - Suc n) @ anything"
+xs @ x # rec_exec (Pr n f g) (xs @ [x]) # 0 \<up> (max (n + 3) (max fft gft) - Suc n) @ anything"
 apply(simp add: abc_lm_s.simps)
-using list_update_length[of "xs @ x # rec_eval (Pr n f g) (xs @ [x]) # 0 \<up> (max (n + 3) (max fft gft) - Suc (Suc n))"
+using list_update_length[of "xs @ x # rec_exec (Pr n f g) (xs @ [x]) # 0 \<up> (max (n + 3) (max fft gft) - Suc (Suc n))"
 0 anything 0]
 apply(auto simp: Suc_diff_Suc)
 apply(simp add: exp_suc[THEN sym] Suc_diff_Suc  del: replicate_Suc)
 done
 lemma [simp]:
-"(xs @ x # rec_eval (Pr (length xs) f g) (xs @ [x]) # 0 \<up> (max (length xs + 3)
+"(xs @ x # rec_exec (Pr (length xs) f g) (xs @ [x]) # 0 \<up> (max (length xs + 3)
 (max fft gft) - Suc (Suc (length xs))) @ 0 # anything) !
 max (length xs + 3) (max fft gft) = 0"
-using nth_append_length[of "xs @ x # rec_eval (Pr (length xs) f g) (xs @ [x]) #
+using nth_append_length[of "xs @ x # rec_exec (Pr (length xs) f g) (xs @ [x]) #
 0 \<up> (max (length xs + 3) (max fft gft) - Suc (Suc (length xs)))" 0  anything]
 by(simp)
 lemma pr_loop_correct:
 assumes less: "y \<le> x"
 and len: "length xs = n"
 and compile_g: "rec_ci g = (gap, gar, gft)"
-and termi_g: "\<forall> y<x. terminates g (xs @ [y, rec_eval (Pr n f g) (xs @ [y])])"
+and termi_g: "\<forall> y<x. terminate g (xs @ [y, rec_exec (Pr n f g) (xs @ [y])])"
-and g_ind: "\<forall> y<x. (\<forall>anything. {\<lambda>nl. nl = xs @ y # rec_eval (Pr n f g) (xs @ [y]) # 0 \<up> (gft - gar) @ anything} gap
+and g_ind: "\<forall> y<x. (\<forall>anything. {\<lambda>nl. nl = xs @ y # rec_exec (Pr n f g) (xs @ [y]) # 0 \<up> (gft - gar) @ anything} gap
-{\<lambda>nl. nl = xs @ y # rec_eval (Pr n f g) (xs @ [y]) # rec_eval g (xs @ [y, rec_eval (Pr n f g) (xs @ [y])]) # 0 \<up> (gft - Suc gar) @ anything})"
+{\<lambda>nl. nl = xs @ y # rec_exec (Pr n f g) (xs @ [y]) # rec_exec g (xs @ [y, rec_exec (Pr n f g) (xs @ [y])]) # 0 \<up> (gft - Suc gar) @ anything})"
-shows "{\<lambda>nl. nl = xs @ (x - y) # rec_eval (Pr n f g) (xs @ [x - y]) # 0 \<up> (max (n + 3) (max fft gft) - Suc (Suc n)) @ y # anything}
+shows "{\<lambda>nl. nl = xs @ (x - y) # rec_exec (Pr n f g) (xs @ [x - y]) # 0 \<up> (max (n + 3) (max fft gft) - Suc (Suc n)) @ y # anything}
 ([Dec (max (n + 3) (max fft gft)) (length gap + 7)] [+] (gap [+] [Inc n, Dec (Suc n) 3, Goto (Suc 0)])) @ [Dec (Suc (Suc n)) 0, Inc (Suc n), Goto (length gap + 4)]
-{\<lambda>nl. nl = xs @ x # rec_eval (Pr n f g) (xs @ [x]) # 0 \<up> (max (n + 3) (max fft gft) - Suc n) @ anything}"
+{\<lambda>nl. nl = xs @ x # rec_exec (Pr n f g) (xs @ [x]) # 0 \<up> (max (n + 3) (max fft gft) - Suc n) @ anything}"
 using less
 proof(induct y)
 case 0
 thus "?case"
 using len
 case (Suc y)
 let ?ft = "max (n + 3) (max fft gft)"
 let ?C = "[Dec (max (n + 3) (max fft gft)) (length gap + 7)] [+] (gap [+]
 [Inc n, Dec (Suc n) 3, Goto (Suc 0)]) @ [Dec (Suc (Suc n)) 0, Inc (Suc n), Goto (length gap + 4)]"
 have ind: "y \<le> x \<Longrightarrow>
-{\<lambda>nl. nl = xs @ (x - y) # rec_eval (Pr n f g) (xs @ [x - y]) # 0 \<up> (?ft - Suc (Suc n)) @ y # anything}
+{\<lambda>nl. nl = xs @ (x - y) # rec_exec (Pr n f g) (xs @ [x - y]) # 0 \<up> (?ft - Suc (Suc n)) @ y # anything}
-?C {\<lambda>nl. nl = xs @ x # rec_eval (Pr n f g) (xs @ [x]) # 0 \<up> (?ft - Suc n) @ anything}" by fact
+?C {\<lambda>nl. nl = xs @ x # rec_exec (Pr n f g) (xs @ [x]) # 0 \<up> (?ft - Suc n) @ anything}" by fact
 have less: "Suc y \<le> x" by fact
 have stp1:
-"\<exists> stp. abc_steps_l (0, xs @ (x - Suc y) # rec_eval (Pr n f g) (xs @ [x - Suc y]) # 0 \<up> (?ft - Suc (Suc n)) @ Suc y # anything)
+"\<exists> stp. abc_steps_l (0, xs @ (x - Suc y) # rec_exec (Pr n f g) (xs @ [x - Suc y]) # 0 \<up> (?ft - Suc (Suc n)) @ Suc y # anything)
-?C stp  = (0, xs @ (x - y) # rec_eval (Pr n f g) (xs @ [x - y]) # 0 \<up> (?ft - Suc (Suc n)) @ y # anything)"
+?C stp  = (0, xs @ (x - y) # rec_exec (Pr n f g) (xs @ [x - y]) # 0 \<up> (?ft - Suc (Suc n)) @ y # anything)"
 using assms less
 by(rule_tac  pr_loop, auto)
 then obtain stp1 where a:
-"abc_steps_l (0, xs @ (x - Suc y) # rec_eval (Pr n f g) (xs @ [x - Suc y]) # 0 \<up> (?ft - Suc (Suc n)) @ Suc y # anything)
+"abc_steps_l (0, xs @ (x - Suc y) # rec_exec (Pr n f g) (xs @ [x - Suc y]) # 0 \<up> (?ft - Suc (Suc n)) @ Suc y # anything)
-?C stp1 = (0, xs @ (x - y) # rec_eval (Pr n f g) (xs @ [x - y]) # 0 \<up> (?ft - Suc (Suc n)) @ y # anything)" ..
+?C stp1 = (0, xs @ (x - y) # rec_exec (Pr n f g) (xs @ [x - y]) # 0 \<up> (?ft - Suc (Suc n)) @ y # anything)" ..
 moreover have
-"\<exists> stp. abc_steps_l (0, xs @ (x - y) # rec_eval (Pr n f g) (xs @ [x - y]) # 0 \<up> (?ft - Suc (Suc n)) @ y # anything)
+"\<exists> stp. abc_steps_l (0, xs @ (x - y) # rec_exec (Pr n f g) (xs @ [x - y]) # 0 \<up> (?ft - Suc (Suc n)) @ y # anything)
-?C stp = (length ?C, xs @ x # rec_eval (Pr n f g) (xs @ [x]) # 0 \<up> (?ft - Suc n) @ anything)"
+?C stp = (length ?C, xs @ x # rec_exec (Pr n f g) (xs @ [x]) # 0 \<up> (?ft - Suc n) @ anything)"
 using ind less
-by(auto simp: abc_Hoare_halt_def, case_tac "abc_steps_l (0, xs @ (x - y) # rec_eval (Pr n f g)
+by(auto simp: abc_Hoare_halt_def, case_tac "abc_steps_l (0, xs @ (x - y) # rec_exec (Pr n f g)
 (xs @ [x - y]) # 0 \<up> (?ft - Suc (Suc n)) @ y # anything) ?C na", rule_tac x = na in exI, simp)
 then obtain stp2 where b:
-"abc_steps_l (0, xs @ (x - y) # rec_eval (Pr n f g) (xs @ [x - y]) # 0 \<up> (?ft - Suc (Suc n)) @ y # anything)
+"abc_steps_l (0, xs @ (x - y) # rec_exec (Pr n f g) (xs @ [x - y]) # 0 \<up> (?ft - Suc (Suc n)) @ y # anything)
-?C stp2 = (length ?C, xs @ x # rec_eval (Pr n f g) (xs @ [x]) # 0 \<up> (?ft - Suc n) @ anything)" ..
+?C stp2 = (length ?C, xs @ x # rec_exec (Pr n f g) (xs @ [x]) # 0 \<up> (?ft - Suc n) @ anything)" ..
 from a b show "?case"
 by(simp add: abc_Hoare_halt_def, rule_tac x = "stp1 + stp2" in exI, simp add: abc_steps_add)
 qed
 lemma compile_pr_correct':
-assumes termi_g: "\<forall> y<x. terminates g (xs @ [y, rec_eval (Pr n f g) (xs @ [y])])"
+assumes termi_g: "\<forall> y<x. terminate g (xs @ [y, rec_exec (Pr n f g) (xs @ [y])])"
 and g_ind:
-"\<forall> y<x. (\<forall>anything. {\<lambda>nl. nl = xs @ y # rec_eval (Pr n f g) (xs @ [y]) # 0 \<up> (gft - gar) @ anything} gap
+"\<forall> y<x. (\<forall>anything. {\<lambda>nl. nl = xs @ y # rec_exec (Pr n f g) (xs @ [y]) # 0 \<up> (gft - gar) @ anything} gap
-{\<lambda>nl. nl = xs @ y # rec_eval (Pr n f g) (xs @ [y]) # rec_eval g (xs @ [y, rec_eval (Pr n f g) (xs @ [y])]) # 0 \<up> (gft - Suc gar) @ anything})"
+{\<lambda>nl. nl = xs @ y # rec_exec (Pr n f g) (xs @ [y]) # rec_exec g (xs @ [y, rec_exec (Pr n f g) (xs @ [y])]) # 0 \<up> (gft - Suc gar) @ anything})"
-and termi_f: "terminates f xs"
+and termi_f: "terminate f xs"
-and f_ind: "\<And> anything. {\<lambda>nl. nl = xs @ 0 \<up> (fft - far) @ anything} fap {\<lambda>nl. nl = xs @ rec_eval f xs # 0 \<up> (fft - Suc far) @ anything}"
+and f_ind: "\<And> anything. {\<lambda>nl. nl = xs @ 0 \<up> (fft - far) @ anything} fap {\<lambda>nl. nl = xs @ rec_exec f xs # 0 \<up> (fft - Suc far) @ anything}"
 and len: "length xs = n"
 and compile1: "rec_ci f = (fap, far, fft)"
 and compile2: "rec_ci g = (gap, gar, gft)"
 shows
 "{\<lambda>nl. nl = xs @ x # 0 \<up> (max (n + 3) (max fft gft) - n) @ anything}
 mv_box n (max (n + 3) (max fft gft)) [+]
 (fap [+] (mv_box n (Suc n) [+]
 ([Dec (max (n + 3) (max fft gft)) (length gap + 7)] [+] (gap [+] [Inc n, Dec (Suc n) 3, Goto (Suc 0)]) @
 [Dec (Suc (Suc n)) 0, Inc (Suc n), Goto (length gap + 4)])))
-{\<lambda>nl. nl = xs @ x # rec_eval (Pr n f g) (xs @ [x]) # 0 \<up> (max (n + 3) (max fft gft) - Suc n) @ anything}"
+{\<lambda>nl. nl = xs @ x # rec_exec (Pr n f g) (xs @ [x]) # 0 \<up> (max (n + 3) (max fft gft) - Suc n) @ anything}"
 proof -
 let ?ft = "max (n+3) (max fft gft)"
 let ?A = "mv_box n ?ft"
 let ?B = "fap"
 let ?C = "mv_box n (Suc n)"
 let ?D = "[Dec ?ft (length gap + 7)]"
 let ?E = "gap [+] [Inc n, Dec (Suc n) 3, Goto (Suc 0)]"
 let ?F = "[Dec (Suc (Suc n)) 0, Inc (Suc n), Goto (length gap + 4)]"
 let ?P = "\<lambda>nl. nl = xs @ x # 0 \<up> (?ft - n) @ anything"
-let ?S = "\<lambda>nl. nl = xs @ x # rec_eval (Pr n f g) (xs @ [x]) # 0 \<up> (?ft - Suc n) @ anything"
+let ?S = "\<lambda>nl. nl = xs @ x # rec_exec (Pr n f g) (xs @ [x]) # 0 \<up> (?ft - Suc n) @ anything"
 let ?Q1 = "\<lambda>nl. nl = xs @ 0 \<up> (?ft - n) @  x # anything"
 show "{?P} (?A [+] (?B [+] (?C [+] (?D [+] ?E @ ?F)))) {?S}"
 proof(rule_tac abc_Hoare_plus_halt)
 show "{?P} ?A {?Q1}"
 using len by simp
 next
-let ?Q2 = "\<lambda>nl. nl = xs @ rec_eval f xs # 0 \<up> (?ft - Suc n) @  x # anything"
+let ?Q2 = "\<lambda>nl. nl = xs @ rec_exec f xs # 0 \<up> (?ft - Suc n) @  x # anything"
 have a: "?ft \<ge> fft"
 by arith
 have b: "far = n"
 using compile1 termi_f len
 by(drule_tac param_pattern, auto)
 using compile1
 by(simp add: footprint_ge)
 show "{?Q1} (?B [+] (?C [+] (?D [+] ?E @ ?F))) {?S}"
 proof(rule_tac abc_Hoare_plus_halt)
 have "{\<lambda>nl. nl = xs @ 0 \<up> (fft - far) @ 0\<up>(?ft - fft) @ x # anything} fap
-{\<lambda>nl. nl = xs @ rec_eval f xs # 0 \<up> (fft - Suc far) @ 0\<up>(?ft - fft) @ x # anything}"
+{\<lambda>nl. nl = xs @ rec_exec f xs # 0 \<up> (fft - Suc far) @ 0\<up>(?ft - fft) @ x # anything}"
 by(rule_tac f_ind)
 moreover have "fft - far + ?ft - fft = ?ft - far"
 using a b c by arith
 moreover have "fft - Suc n + ?ft - fft = ?ft - Suc n"
 using a b c by arith
 ultimately show "{?Q1} ?B {?Q2}"
 using b
 by(simp add: replicate_merge_anywhere)
 next
-let ?Q3 = "\<lambda> nl. nl = xs @ 0 # rec_eval f xs # 0\<up>(?ft - Suc (Suc n)) @ x # anything"
+let ?Q3 = "\<lambda> nl. nl = xs @ 0 # rec_exec f xs # 0\<up>(?ft - Suc (Suc n)) @ x # anything"
 show "{?Q2} (?C [+] (?D [+] ?E @ ?F)) {?S}"
 proof(rule_tac abc_Hoare_plus_halt)
 show "{?Q2} (?C) {?Q3}"
-using mv_box_correct[of n "Suc n" "xs @ rec_eval f xs # 0 \<up> (max (n + 3) (max fft gft) - Suc n) @ x # anything"]
+using mv_box_correct[of n "Suc n" "xs @ rec_exec f xs # 0 \<up> (max (n + 3) (max fft gft) - Suc n) @ x # anything"]
 using len
 by(auto)
 next
 show "{?Q3} (?D [+] ?E @ ?F) {?S}"
 using pr_loop_correct[of x x xs n g  gap gar gft f fft anything] assms
-by(simp add: rec_eval_pr_0_simps)
+by(simp add: rec_exec_pr_0_simps)
 qed
 qed
 qed
 qed
 lemma compile_pr_correct:
-assumes g_ind: "\<forall>y<x. terminates g (xs @ [y, rec_eval (Pr n f g) (xs @ [y])]) \<and>
+assumes g_ind: "\<forall>y<x. terminate g (xs @ [y, rec_exec (Pr n f g) (xs @ [y])]) \<and>
 (\<forall>x xa xb. rec_ci g = (x, xa, xb) \<longrightarrow>
-(\<forall>xc. {\<lambda>nl. nl = xs @ y # rec_eval (Pr n f g) (xs @ [y]) # 0 \<up> (xb - xa) @ xc} x
+(\<forall>xc. {\<lambda>nl. nl = xs @ y # rec_exec (Pr n f g) (xs @ [y]) # 0 \<up> (xb - xa) @ xc} x
-{\<lambda>nl. nl = xs @ y # rec_eval (Pr n f g) (xs @ [y]) # rec_eval g (xs @ [y, rec_eval (Pr n f g) (xs @ [y])]) # 0 \<up> (xb - Suc xa) @ xc}))"
+{\<lambda>nl. nl = xs @ y # rec_exec (Pr n f g) (xs @ [y]) # rec_exec g (xs @ [y, rec_exec (Pr n f g) (xs @ [y])]) # 0 \<up> (xb - Suc xa) @ xc}))"
-and termi_f: "terminates f xs"
+and termi_f: "terminate f xs"
 and f_ind:
 "\<And>ap arity fp anything.
-rec_ci f = (ap, arity, fp) \<Longrightarrow> {\<lambda>nl. nl = xs @ 0 \<up> (fp - arity) @ anything} ap {\<lambda>nl. nl = xs @ rec_eval f xs # 0 \<up> (fp - Suc arity) @ anything}"
+rec_ci f = (ap, arity, fp) \<Longrightarrow> {\<lambda>nl. nl = xs @ 0 \<up> (fp - arity) @ anything} ap {\<lambda>nl. nl = xs @ rec_exec f xs # 0 \<up> (fp - Suc arity) @ anything}"
 and len: "length xs = n"
 and compile: "rec_ci (Pr n f g) = (ap, arity, fp)"
-shows "{\<lambda>nl. nl = xs @ x # 0 \<up> (fp - arity) @ anything} ap {\<lambda>nl. nl = xs @ x # rec_eval (Pr n f g) (xs @ [x]) # 0 \<up> (fp - Suc arity) @ anything}"
+shows "{\<lambda>nl. nl = xs @ x # 0 \<up> (fp - arity) @ anything} ap {\<lambda>nl. nl = xs @ x # rec_exec (Pr n f g) (xs @ [x]) # 0 \<up> (fp - Suc arity) @ anything}"
 proof(case_tac "rec_ci f", case_tac "rec_ci g")
 fix fap far fft gap gar gft
 assume h: "rec_ci f = (fap, far, fft)" "rec_ci g = (gap, gar, gft)"
 have g:
-"\<forall>y<x. (terminates g (xs @ [y, rec_eval (Pr n f g) (xs @ [y])]) \<and>
+"\<forall>y<x. (terminate g (xs @ [y, rec_exec (Pr n f g) (xs @ [y])]) \<and>
-(\<forall>anything. {\<lambda>nl. nl = xs @ y # rec_eval (Pr n f g) (xs @ [y]) # 0 \<up> (gft - gar) @ anything} gap
+(\<forall>anything. {\<lambda>nl. nl = xs @ y # rec_exec (Pr n f g) (xs @ [y]) # 0 \<up> (gft - gar) @ anything} gap
-{\<lambda>nl. nl = xs @ y # rec_eval (Pr n f g) (xs @ [y]) # rec_eval g (xs @ [y, rec_eval (Pr n f g) (xs @ [y])]) # 0 \<up> (gft - Suc gar) @ anything}))"
+{\<lambda>nl. nl = xs @ y # rec_exec (Pr n f g) (xs @ [y]) # rec_exec g (xs @ [y, rec_exec (Pr n f g) (xs @ [y])]) # 0 \<up> (gft - Suc gar) @ anything}))"
 using g_ind h
 by(auto)
-hence termi_g: "\<forall> y<x. terminates g (xs @ [y, rec_eval (Pr n f g) (xs @ [y])])"
+hence termi_g: "\<forall> y<x. terminate g (xs @ [y, rec_exec (Pr n f g) (xs @ [y])])"
 by simp
 from g have g_newind:
-"\<forall> y<x. (\<forall>anything. {\<lambda>nl. nl = xs @ y # rec_eval (Pr n f g) (xs @ [y]) # 0 \<up> (gft - gar) @ anything} gap
+"\<forall> y<x. (\<forall>anything. {\<lambda>nl. nl = xs @ y # rec_exec (Pr n f g) (xs @ [y]) # 0 \<up> (gft - gar) @ anything} gap
-{\<lambda>nl. nl = xs @ y # rec_eval (Pr n f g) (xs @ [y]) # rec_eval g (xs @ [y, rec_eval (Pr n f g) (xs @ [y])]) # 0 \<up> (gft - Suc gar) @ anything})"
+{\<lambda>nl. nl = xs @ y # rec_exec (Pr n f g) (xs @ [y]) # rec_exec g (xs @ [y, rec_exec (Pr n f g) (xs @ [y])]) # 0 \<up> (gft - Suc gar) @ anything})"
 by auto
-have f_newind: "\<And> anything. {\<lambda>nl. nl = xs @ 0 \<up> (fft - far) @ anything} fap {\<lambda>nl. nl = xs @ rec_eval f xs # 0 \<up> (fft - Suc far) @ anything}"
+have f_newind: "\<And> anything. {\<lambda>nl. nl = xs @ 0 \<up> (fft - far) @ anything} fap {\<lambda>nl. nl = xs @ rec_exec f xs # 0 \<up> (fft - Suc far) @ anything}"
 using h
 by(rule_tac f_ind, simp)
 show "?thesis"
 using termi_f termi_g h compile
 apply(simp add: rec_ci.simps abc_comp_commute, auto)
 assumes B:  "B = [Dec (Suc arity) (length fap + 5), Dec (Suc arity) (length fap + 3), Goto (Suc (length fap)), Inc arity, Goto 0]"
 and ft: "ft = max (Suc arity) fft"
 and len: "length xs = arity"
 and far: "far = Suc arity"
 and ind: " (\<forall>xc. ({\<lambda>nl. nl = xs @ x # 0 \<up> (fft - far) @ xc} fap
-{\<lambda>nl. nl = xs @ x # rec_eval f (xs @ [x]) # 0 \<up> (fft - Suc far) @ xc}))"
+{\<lambda>nl. nl = xs @ x # rec_exec f (xs @ [x]) # 0 \<up> (fft - Suc far) @ xc}))"
-and exec_less: "rec_eval f (xs @ [x]) > 0"
+and exec_less: "rec_exec f (xs @ [x]) > 0"
 and compile: "rec_ci f = (fap, far, fft)"
 shows "\<exists> stp > 0. abc_steps_l (0, xs @ x # 0 \<up> (ft - Suc arity) @ anything) (fap @ B) stp =
 (0, xs @ Suc x # 0 \<up> (ft - Suc arity) @ anything)"
 proof -
 have "\<exists> stp. abc_steps_l (0, xs @ x # 0 \<up> (ft - Suc arity) @ anything) (fap @ B) stp =
-(length fap, xs @ x # rec_eval f (xs @ [x]) # 0 \<up> (ft - Suc (Suc arity)) @ anything)"
+(length fap, xs @ x # rec_exec f (xs @ [x]) # 0 \<up> (ft - Suc (Suc arity)) @ anything)"
 proof -
 have "\<exists> stp. abc_steps_l (0, xs @ x # 0 \<up> (ft - Suc arity) @ anything) fap stp =
-(length fap, xs @ x # rec_eval f (xs @ [x]) # 0 \<up> (ft - Suc (Suc arity)) @ anything)"
+(length fap, xs @ x # rec_exec f (xs @ [x]) # 0 \<up> (ft - Suc (Suc arity)) @ anything)"
 proof -
 have "{\<lambda>nl. nl = xs @ x # 0 \<up> (fft - far) @ 0\<up>(ft - fft) @ anything} fap
-{\<lambda>nl. nl = xs @ x # rec_eval f (xs @ [x]) # 0 \<up> (fft - Suc far) @ 0\<up>(ft - fft) @ anything}"
+{\<lambda>nl. nl = xs @ x # rec_exec f (xs @ [x]) # 0 \<up> (fft - Suc far) @ 0\<up>(ft - fft) @ anything}"
 using ind by simp
 moreover have "fft > far"
 using compile
 by(erule_tac footprint_ge)
 ultimately show "?thesis"
 using ft far
 apply(drule_tac abc_Hoare_haltE)
 by(simp add: replicate_merge_anywhere max_absorb2)
 qed
 then obtain stp where "abc_steps_l (0, xs @ x # 0 \<up> (ft - Suc arity) @ anything) fap stp =
-(length fap, xs @ x # rec_eval f (xs @ [x]) # 0 \<up> (ft - Suc (Suc arity)) @ anything)" ..
+(length fap, xs @ x # rec_exec f (xs @ [x]) # 0 \<up> (ft - Suc (Suc arity)) @ anything)" ..
 thus "?thesis"
 by(erule_tac abc_append_frist_steps_halt_eq)
 qed
 moreover have
-"\<exists> stp > 0. abc_steps_l (length fap, xs @ x # rec_eval f (xs @ [x]) # 0 \<up> (ft - Suc (Suc arity)) @ anything) (fap @ B) stp =
+"\<exists> stp > 0. abc_steps_l (length fap, xs @ x # rec_exec f (xs @ [x]) # 0 \<up> (ft - Suc (Suc arity)) @ anything) (fap @ B) stp =
 (0, xs @ Suc x # 0 # 0 \<up> (ft - Suc (Suc arity)) @ anything)"
-using mn_correct[of f fap far fft "rec_eval f (xs @ [x])" xs arity B
+using mn_correct[of f fap far fft "rec_exec f (xs @ [x])" xs arity B
-"(\<lambda>stp. (abc_steps_l (length fap, xs @ x # rec_eval f (xs @ [x]) # 0 \<up> (ft - Suc (Suc arity)) @ anything) (fap @ B) stp, length fap, arity))"
+"(\<lambda>stp. (abc_steps_l (length fap, xs @ x # rec_exec f (xs @ [x]) # 0 \<up> (ft - Suc (Suc arity)) @ anything) (fap @ B) stp, length fap, arity))"
 x "0 \<up> (ft - Suc (Suc arity)) @ anything" "(\<lambda>((as, lm), ss, arity). as = 0)"
-"(\<lambda>((as, lm), ss, aritya). mn_ind_inv (as, lm) (length fap) x (rec_eval f (xs @ [x])) (0 \<up> (ft - Suc (Suc arity)) @ anything) xs) "]
+"(\<lambda>((as, lm), ss, aritya). mn_ind_inv (as, lm) (length fap) x (rec_exec f (xs @ [x])) (0 \<up> (ft - Suc (Suc arity)) @ anything) xs) "]
 B compile  exec_less len
 apply(subgoal_tac "fap \<noteq> []", auto)
 apply(rule_tac x = stp in exI, auto simp: mn_ind_inv.simps)
 by(case_tac "stp = 0", simp_all add: abc_steps_l.simps)
 moreover have "fft > far"
 lemma mn_loop_correct':
 assumes B:  "B = [Dec (Suc arity) (length fap + 5), Dec (Suc arity) (length fap + 3), Goto (Suc (length fap)), Inc arity, Goto 0]"
 and ft: "ft = max (Suc arity) fft"
 and len: "length xs = arity"
 and ind_all: "\<forall>i\<le>x. (\<forall>xc. ({\<lambda>nl. nl = xs @ i # 0 \<up> (fft - far) @ xc} fap
-{\<lambda>nl. nl = xs @ i # rec_eval f (xs @ [i]) # 0 \<up> (fft - Suc far) @ xc}))"
+{\<lambda>nl. nl = xs @ i # rec_exec f (xs @ [i]) # 0 \<up> (fft - Suc far) @ xc}))"
-and exec_ge: "\<forall> i\<le>x. rec_eval f (xs @ [i]) > 0"
+and exec_ge: "\<forall> i\<le>x. rec_exec f (xs @ [i]) > 0"
 and compile: "rec_ci f = (fap, far, fft)"
 and far: "far = Suc arity"
 shows "\<exists> stp > x. abc_steps_l (0, xs @ 0 # 0 \<up> (ft - Suc arity) @ anything) (fap @ B) stp =
 (0, xs @ Suc x # 0 \<up> (ft - Suc arity) @ anything)"
 using ind_all exec_ge
 thus "?case"
 using assms
 by(rule_tac mn_loop, simp_all)
 next
 case (Suc x)
-have ind': "\<lbrakk>\<forall>i\<le>x. \<forall>xc. {\<lambda>nl. nl = xs @ i # 0 \<up> (fft - far) @ xc} fap {\<lambda>nl. nl = xs @ i # rec_eval f (xs @ [i]) # 0 \<up> (fft - Suc far) @ xc};
+have ind': "\<lbrakk>\<forall>i\<le>x. \<forall>xc. {\<lambda>nl. nl = xs @ i # 0 \<up> (fft - far) @ xc} fap {\<lambda>nl. nl = xs @ i # rec_exec f (xs @ [i]) # 0 \<up> (fft - Suc far) @ xc};
-\<forall>i\<le>x. 0 < rec_eval f (xs @ [i])\<rbrakk> \<Longrightarrow>
+\<forall>i\<le>x. 0 < rec_exec f (xs @ [i])\<rbrakk> \<Longrightarrow>
 \<exists>stp > x. abc_steps_l (0, xs @ 0 # 0 \<up> (ft - Suc arity) @ anything) (fap @ B) stp = (0, xs @ Suc x # 0 \<up> (ft - Suc arity) @ anything)" by fact
-have exec_ge: "\<forall>i\<le>Suc x. 0 < rec_eval f (xs @ [i])" by fact
+have exec_ge: "\<forall>i\<le>Suc x. 0 < rec_exec f (xs @ [i])" by fact
 have ind_all: "\<forall>i\<le>Suc x. \<forall>xc. {\<lambda>nl. nl = xs @ i # 0 \<up> (fft - far) @ xc} fap
-{\<lambda>nl. nl = xs @ i # rec_eval f (xs @ [i]) # 0 \<up> (fft - Suc far) @ xc}" by fact
+{\<lambda>nl. nl = xs @ i # rec_exec f (xs @ [i]) # 0 \<up> (fft - Suc far) @ xc}" by fact
 have ind: "\<exists>stp > x. abc_steps_l (0, xs @ 0 # 0 \<up> (ft - Suc arity) @ anything) (fap @ B) stp =
 (0, xs @ Suc x # 0 \<up> (ft - Suc arity) @ anything)" using ind' exec_ge ind_all by simp
 have stp: "\<exists> stp > 0. abc_steps_l (0, xs @ Suc x # 0 \<up> (ft - Suc arity) @ anything) (fap @ B) stp =
 (0, xs @ Suc (Suc x) # 0 \<up> (ft - Suc arity) @ anything)"
 using ind_all exec_ge B ft len far compile
 lemma mn_loop_correct:
 assumes B:  "B = [Dec (Suc arity) (length fap + 5), Dec (Suc arity) (length fap + 3), Goto (Suc (length fap)), Inc arity, Goto 0]"
 and ft: "ft = max (Suc arity) fft"
 and len: "length xs = arity"
 and ind_all: "\<forall>i\<le>x. (\<forall>xc. ({\<lambda>nl. nl = xs @ i # 0 \<up> (fft - far) @ xc} fap
-{\<lambda>nl. nl = xs @ i # rec_eval f (xs @ [i]) # 0 \<up> (fft - Suc far) @ xc}))"
+{\<lambda>nl. nl = xs @ i # rec_exec f (xs @ [i]) # 0 \<up> (fft - Suc far) @ xc}))"
-and exec_ge: "\<forall> i\<le>x. rec_eval f (xs @ [i]) > 0"
+and exec_ge: "\<forall> i\<le>x. rec_exec f (xs @ [i]) > 0"
 and compile: "rec_ci f = (fap, far, fft)"
 and far: "far = Suc arity"
 shows "\<exists> stp. abc_steps_l (0, xs @ 0 # 0 \<up> (ft - Suc arity) @ anything) (fap @ B) stp =
 (0, xs @ Suc x # 0 \<up> (ft - Suc arity) @ anything)"
 proof -
 lemma compile_mn_correct':
 assumes B:  "B = [Dec (Suc arity) (length fap + 5), Dec (Suc arity) (length fap + 3), Goto (Suc (length fap)), Inc arity, Goto 0]"
 and ft: "ft = max (Suc arity) fft"
 and len: "length xs = arity"
-and termi_f: "terminates f (xs @ [r])"
+and termi_f: "terminate f (xs @ [r])"
 and f_ind: "\<And>anything. {\<lambda>nl. nl = xs @ r # 0 \<up> (fft - far) @ anything} fap
 {\<lambda>nl. nl = xs @ r # 0 # 0 \<up> (fft - Suc far) @ anything}"
 and ind_all: "\<forall>i < r. (\<forall>xc. ({\<lambda>nl. nl = xs @ i # 0 \<up> (fft - far) @ xc} fap
-{\<lambda>nl. nl = xs @ i # rec_eval f (xs @ [i]) # 0 \<up> (fft - Suc far) @ xc}))"
+{\<lambda>nl. nl = xs @ i # rec_exec f (xs @ [i]) # 0 \<up> (fft - Suc far) @ xc}))"
-and exec_less: "\<forall> i<r. rec_eval f (xs @ [i]) > 0"
+and exec_less: "\<forall> i<r. rec_exec f (xs @ [i]) > 0"
-and exec: "rec_eval f (xs @ [r]) = 0"
+and exec: "rec_exec f (xs @ [r]) = 0"
 and compile: "rec_ci f = (fap, far, fft)"
 shows "{\<lambda>nl. nl = xs @ 0 \<up> (max (Suc arity) fft - arity) @ anything}
 fap @ B
-{\<lambda>nl. nl = xs @ rec_eval (Mn arity f) xs # 0 \<up> (max (Suc arity) fft - Suc arity) @ anything}"
+{\<lambda>nl. nl = xs @ rec_exec (Mn arity f) xs # 0 \<up> (max (Suc arity) fft - Suc arity) @ anything}"
 proof -
 have a: "far = Suc arity"
 using len compile termi_f
 by(drule_tac param_pattern, auto)
 have b: "fft > far"
 using assms a
 apply(case_tac r, rule_tac x = 0 in exI, simp add: abc_steps_l.simps, simp)
 by(rule_tac mn_loop_correct, auto)
 moreover have
 "\<exists> stp. abc_steps_l (0, xs @ r # 0 \<up> (ft - Suc arity) @ anything) (fap @ B) stp =
-(length fap, xs @ r # rec_eval f (xs @ [r]) # 0 \<up> (ft - Suc (Suc arity)) @ anything)"
+(length fap, xs @ r # rec_exec f (xs @ [r]) # 0 \<up> (ft - Suc (Suc arity)) @ anything)"
 proof -
 have "\<exists> stp. abc_steps_l (0, xs @ r # 0 \<up> (ft - Suc arity) @ anything) fap stp =
-(length fap, xs @ r # rec_eval f (xs @ [r]) # 0 \<up> (ft - Suc (Suc arity)) @ anything)"
+(length fap, xs @ r # rec_exec f (xs @ [r]) # 0 \<up> (ft - Suc (Suc arity)) @ anything)"
 proof -
 have "{\<lambda>nl. nl = xs @ r # 0 \<up> (fft - far) @ 0\<up>(ft - fft) @ anything} fap
-{\<lambda>nl. nl = xs @ r # rec_eval f (xs @ [r]) # 0 \<up> (fft - Suc far) @ 0\<up>(ft - fft) @ anything}"
+{\<lambda>nl. nl = xs @ r # rec_exec f (xs @ [r]) # 0 \<up> (fft - Suc far) @ 0\<up>(ft - fft) @ anything}"
 using f_ind exec by simp
 thus "?thesis"
 using ft a b
 apply(drule_tac abc_Hoare_haltE)
 by(simp add: replicate_merge_anywhere max_absorb2)
 qed
 then obtain stp where "abc_steps_l (0, xs @ r # 0 \<up> (ft - Suc arity) @ anything) fap stp =
-(length fap, xs @ r # rec_eval f (xs @ [r]) # 0 \<up> (ft - Suc (Suc arity)) @ anything)" ..
+(length fap, xs @ r # rec_exec f (xs @ [r]) # 0 \<up> (ft - Suc (Suc arity)) @ anything)" ..
 thus "?thesis"
 by(erule_tac abc_append_frist_steps_halt_eq)
 qed
 moreover have
-"\<exists> stp. abc_steps_l (length fap, xs @ r # rec_eval f (xs @ [r]) # 0 \<up> (ft - Suc (Suc arity)) @ anything) (fap @ B) stp =
+"\<exists> stp. abc_steps_l (length fap, xs @ r # rec_exec f (xs @ [r]) # 0 \<up> (ft - Suc (Suc arity)) @ anything) (fap @ B) stp =
-(length fap + 5, xs @ r # rec_eval f (xs @ [r]) # 0 \<up> (ft - Suc (Suc arity)) @ anything)"
+(length fap + 5, xs @ r # rec_exec f (xs @ [r]) # 0 \<up> (ft - Suc (Suc arity)) @ anything)"
 using ft a b len B exec
 apply(rule_tac x = 1 in exI, auto)
 by(auto simp: abc_steps_l.simps B abc_step_l.simps
 abc_fetch.simps nth_append max_absorb2 abc_lm_v.simps abc_lm_s.simps)
-moreover have "rec_eval (Mn (length xs) f) xs = r"
+moreover have "rec_exec (Mn (length xs) f) xs = r"
 using exec exec_less
-apply(auto simp: rec_eval.simps Least_def)
+apply(auto simp: rec_exec.simps Least_def)
 thm the_equality
 apply(rule_tac the_equality, auto)
 apply(metis exec_less less_not_refl3 linorder_not_less)
 by (metis le_neq_implies_less less_not_refl3)
 ultimately show "?thesis"
 by(simp add: abc_steps_add replicate_Suc_iff_anywhere max_absorb2 Suc_diff_Suc del: replicate_Suc)
 qed
 lemma compile_mn_correct:
 assumes len: "length xs = n"
-and termi_f: "terminates f (xs @ [r])"
+and termi_f: "terminate f (xs @ [r])"
 and f_ind: "\<And>ap arity fp anything. rec_ci f = (ap, arity, fp) \<Longrightarrow>
 {\<lambda>nl. nl = xs @ r # 0 \<up> (fp - arity) @ anything} ap {\<lambda>nl. nl = xs @ r # 0 # 0 \<up> (fp - Suc arity) @ anything}"
-and exec: "rec_eval f (xs @ [r]) = 0"
+and exec: "rec_exec f (xs @ [r]) = 0"
 and ind_all:
-"\<forall>i<r. terminates f (xs @ [i]) \<and>
+"\<forall>i<r. terminate f (xs @ [i]) \<and>
 (\<forall>x xa xb. rec_ci f = (x, xa, xb) \<longrightarrow>
-(\<forall>xc. {\<lambda>nl. nl = xs @ i # 0 \<up> (xb - xa) @ xc} x {\<lambda>nl. nl = xs @ i # rec_eval f (xs @ [i]) # 0 \<up> (xb - Suc xa) @ xc})) \<and>
+(\<forall>xc. {\<lambda>nl. nl = xs @ i # 0 \<up> (xb - xa) @ xc} x {\<lambda>nl. nl = xs @ i # rec_exec f (xs @ [i]) # 0 \<up> (xb - Suc xa) @ xc})) \<and>
-0 < rec_eval f (xs @ [i])"
+0 < rec_exec f (xs @ [i])"
 and compile: "rec_ci (Mn n f) = (ap, arity, fp)"
 shows "{\<lambda>nl. nl = xs @ 0 \<up> (fp - arity) @ anything} ap
-{\<lambda>nl. nl = xs @ rec_eval (Mn n f) xs # 0 \<up> (fp - Suc arity) @ anything}"
+{\<lambda>nl. nl = xs @ rec_exec (Mn n f) xs # 0 \<up> (fp - Suc arity) @ anything}"
 proof(case_tac "rec_ci f")
 fix fap far fft
 assume h: "rec_ci f = (fap, far, fft)"
 hence f_newind:
 "\<And>anything. {\<lambda>nl. nl = xs @ r # 0 \<up> (fft - far) @ anything} fap
 {\<lambda>nl. nl = xs @ r # 0 # 0 \<up> (fft - Suc far) @ anything}"
 by(rule_tac f_ind, simp)
 have newind_all:
 "\<forall>i < r. (\<forall>xc. ({\<lambda>nl. nl = xs @ i # 0 \<up> (fft - far) @ xc} fap
-{\<lambda>nl. nl = xs @ i # rec_eval f (xs @ [i]) # 0 \<up> (fft - Suc far) @ xc}))"
+{\<lambda>nl. nl = xs @ i # rec_exec f (xs @ [i]) # 0 \<up> (fft - Suc far) @ xc}))"
 using ind_all h
 by(auto)
-have all_less: "\<forall> i<r. rec_eval f (xs @ [i]) > 0"
+have all_less: "\<forall> i<r. rec_exec f (xs @ [i]) > 0"
 using ind_all by auto
 show "?thesis"
 using h compile f_newind newind_all all_less len termi_f exec
 apply(auto simp: rec_ci.simps)
 by(rule_tac compile_mn_correct', auto)
 qed
 lemma recursive_compile_correct:
-"\<lbrakk>terminates recf args; rec_ci recf = (ap, arity, fp)\<rbrakk>
+"\<lbrakk>terminate recf args; rec_ci recf = (ap, arity, fp)\<rbrakk>
 \<Longrightarrow> {\<lambda> nl. nl = args @ 0\<up>(fp - arity) @ anything} ap
-{\<lambda> nl. nl = args@ rec_eval recf args # 0\<up>(fp - Suc arity) @ anything}"
+{\<lambda> nl. nl = args@ rec_exec recf args # 0\<up>(fp - Suc arity) @ anything}"
-apply(induct arbitrary: ap arity fp anything r rule: terminates.induct)
+apply(induct arbitrary: ap arity fp anything r rule: terminate.induct)
 apply(simp_all add: compile_s_correct compile_z_correct compile_id_correct
 compile_cn_correct compile_pr_correct compile_mn_correct)
 done
 definition dummy_abc :: "nat \<Rightarrow> abc_inst list"
 by auto
 qed
 lemma recursive_compile_correct_norm':
 "\<lbrakk>rec_ci f = (ap, arity, ft);
-terminates f args\<rbrakk>
+terminate f args\<rbrakk>
-\<Longrightarrow> \<exists> stp rl. (abc_steps_l (0, args) ap stp) = (length ap, rl) \<and> abc_list_crsp (args @ [rec_eval f args]) rl"
+\<Longrightarrow> \<exists> stp rl. (abc_steps_l (0, args) ap stp) = (length ap, rl) \<and> abc_list_crsp (args @ [rec_exec f args]) rl"
 using recursive_compile_correct[of f args ap arity ft "[]"]
 apply(auto simp: abc_Hoare_halt_def)
 apply(rule_tac x = n in exI)
 apply(case_tac "abc_steps_l (0, args @ 0 \<up> (ft - arity)) ap n", auto)
 apply(drule_tac abc_list_crsp_steps, auto)
 apply(rule_tac list_crsp_simp2, auto)
 done
 lemma [simp]:
-assumes a: "args @ [rec_eval f args] = lm @ 0 \<up> n"
+assumes a: "args @ [rec_exec f args] = lm @ 0 \<up> n"
 and b: "length args < length lm"
-shows "\<exists>m. lm = args @ rec_eval f args # 0 \<up> m"
+shows "\<exists>m. lm = args @ rec_exec f args # 0 \<up> m"
 using assms
 apply(case_tac n, simp)
 apply(rule_tac x = 0 in exI, simp)
 apply(drule_tac length_equal, simp)
 done
 lemma [simp]:
-"\<lbrakk>args @ [rec_eval f args] = lm @ 0 \<up> n; \<not> length args < length lm\<rbrakk>
+"\<lbrakk>args @ [rec_exec f args] = lm @ 0 \<up> n; \<not> length args < length lm\<rbrakk>
 \<Longrightarrow> \<exists>m. (lm @ 0 \<up> (length args - length lm) @ [Suc 0])[length args := 0] =
-args @ rec_eval f args # 0 \<up> m"
+args @ rec_exec f args # 0 \<up> m"
 apply(case_tac n, simp_all add: exp_suc list_update_append list_update.simps del: replicate_Suc)
 apply(subgoal_tac "length args = Suc (length lm)", simp)
 apply(rule_tac x = "Suc (Suc 0)" in exI, simp)
 apply(drule_tac length_equal, simp, auto)
 done
 lemma compile_append_dummy_correct:
 assumes compile: "rec_ci f = (ap, ary, fp)"
-and termi: "terminates f args"
+and termi: "terminate f args"
-shows "{\<lambda> nl. nl = args} (ap [+] dummy_abc (length args)) {\<lambda> nl. (\<exists> m. nl = args @ rec_eval f args # 0\<up>m)}"
+shows "{\<lambda> nl. nl = args} (ap [+] dummy_abc (length args)) {\<lambda> nl. (\<exists> m. nl = args @ rec_exec f args # 0\<up>m)}"
 proof(rule_tac abc_Hoare_plus_halt)
-show "{\<lambda>nl. nl = args} ap {\<lambda> nl. abc_list_crsp (args @ [rec_eval f args]) nl}"
+show "{\<lambda>nl. nl = args} ap {\<lambda> nl. abc_list_crsp (args @ [rec_exec f args]) nl}"
 using compile termi recursive_compile_correct_norm'[of f ap ary fp args]
 apply(auto simp: abc_Hoare_halt_def)
 by(rule_tac x = stp in exI, simp)
 next
-show "{abc_list_crsp (args @ [rec_eval f args])} dummy_abc (length args)
+show "{abc_list_crsp (args @ [rec_exec f args])} dummy_abc (length args)
-{\<lambda>nl. \<exists>m. nl = args @ rec_eval f args # 0 \<up> m}"
+{\<lambda>nl. \<exists>m. nl = args @ rec_exec f args # 0 \<up> m}"
 apply(auto simp: dummy_abc_def abc_Hoare_halt_def)
 apply(rule_tac x = 3 in exI)
 by(auto simp: abc_steps_l.simps abc_list_crsp_def abc_step_l.simps numeral_3_eq_3 abc_fetch.simps
 abc_lm_v.simps nth_append abc_lm_s.simps)
 qed
 assumes compile1: "rec_ci (Cn n f gs) = (ap, ar, ft) \<and> length args = ar"
 and g: "i < length gs"
 and compile2: "rec_ci (gs!i) = (gap, gar, gft) \<and> gar = length args"
 and g_unhalt: "\<And> anything. {\<lambda> nl. nl = args @ 0\<up>(gft - gar) @ anything} gap \<up>"
 and g_ind: "\<And> apj arj ftj j anything. \<lbrakk>j < i; rec_ci (gs!j) = (apj, arj, ftj)\<rbrakk>
-\<Longrightarrow> {\<lambda> nl. nl = args @ 0\<up>(ftj - arj) @ anything} apj {\<lambda> nl. nl = args @ rec_eval (gs!j) args # 0\<up>(ftj - Suc arj) @ anything}"
+\<Longrightarrow> {\<lambda> nl. nl = args @ 0\<up>(ftj - arj) @ anything} apj {\<lambda> nl. nl = args @ rec_exec (gs!j) args # 0\<up>(ftj - Suc arj) @ anything}"
-and all_termi: "\<forall> j<i. terminates (gs!j) args"
+and all_termi: "\<forall> j<i. terminate (gs!j) args"
 shows "{\<lambda> nl. nl = args @ 0\<up>(ft - ar) @ anything} ap \<up>"
 using compile1
 apply(case_tac "rec_ci f", auto simp: rec_ci.simps abc_comp_commute)
 proof(rule_tac abc_Hoare_plus_unhalt1)
 fix fap far fft
 let ?ft = "max (Suc (length args)) (Max (insert fft ((\<lambda>(aprog, p, n). n) ` rec_ci ` set gs)))"
-let ?Q = "\<lambda>nl. nl = args @ 0\<up> (?ft - length args) @ map (\<lambda>i. rec_eval i args) (take i gs) @
+let ?Q = "\<lambda>nl. nl = args @ 0\<up> (?ft - length args) @ map (\<lambda>i. rec_exec i args) (take i gs) @
 0\<up>(length gs - i) @ 0\<up> Suc (length args) @ anything"
 have "cn_merge_gs (map rec_ci gs) ?ft =
 cn_merge_gs (map rec_ci (take i gs)) ?ft [+] (gap [+]
 mv_box gar (?ft + i)) [+]  cn_merge_gs (map rec_ci (drop (Suc i) gs)) (?ft + Suc i)"
 using g compile2 cn_merge_gs_split by simp
 thus "{\<lambda>nl. nl = args @ 0 # 0 \<up> (?ft + length gs) @ anything} (cn_merge_gs (map rec_ci gs) ?ft) \<up>"
 proof(simp, rule_tac abc_Hoare_plus_unhalt1, rule_tac abc_Hoare_plus_unhalt2,
 rule_tac abc_Hoare_plus_unhalt1)
-let ?Q_tmp = "\<lambda>nl. nl = args @ 0\<up> (gft - gar) @ 0\<up>(?ft - (length args) - (gft -gar)) @ map (\<lambda>i. rec_eval i args) (take i gs) @
+let ?Q_tmp = "\<lambda>nl. nl = args @ 0\<up> (gft - gar) @ 0\<up>(?ft - (length args) - (gft -gar)) @ map (\<lambda>i. rec_exec i args) (take i gs) @
 0\<up>(length gs - i) @ 0\<up> Suc (length args) @ anything"
 have a: "{?Q_tmp} gap \<up>"
 using g_unhalt[of "0 \<up> (?ft - (length args) - (gft - gar)) @
-map (\<lambda>i. rec_eval i args) (take i gs) @ 0 \<up> (length gs - i) @ 0 \<up> Suc (length args) @ anything"]
+map (\<lambda>i. rec_exec i args) (take i gs) @ 0 \<up> (length gs - i) @ 0 \<up> Suc (length args) @ anything"]
 by simp
 moreover have "?ft \<ge> gft"
 using g compile2
 apply(rule_tac min_max.le_supI2, rule_tac Max_ge, simp, rule_tac insertI2)
 apply(rule_tac  x = "rec_ci (gs ! i)" in image_eqI, simp)
 using a by simp
 next
 show "{\<lambda>nl. nl = args @ 0 # 0 \<up> (?ft + length gs) @ anything}
 cn_merge_gs (map rec_ci (take i gs)) ?ft
 {\<lambda>nl. nl = args @ 0 \<up> (?ft - length args) @
-map (\<lambda>i. rec_eval i args) (take i gs) @ 0 \<up> (length gs - i) @ 0 \<up> Suc (length args) @ anything}"
+map (\<lambda>i. rec_exec i args) (take i gs) @ 0 \<up> (length gs - i) @ 0 \<up> Suc (length args) @ anything}"
 using all_termi
 apply(rule_tac compile_cn_gs_correct', auto simp: set_conv_nth)
 by(drule_tac apj = x and arj = xa and  ftj = xb and j = ia and anything = xc in g_ind, auto)
 qed
 qed
 lemma mn_unhalt_case':
 assumes compile: "rec_ci f = (a, b, c)"
-and all_termi: "\<forall>i. terminates f (args @ [i]) \<and> 0 < rec_eval f (args @ [i])"
+and all_termi: "\<forall>i. terminate f (args @ [i]) \<and> 0 < rec_exec f (args @ [i])"
 and B: "B = [Dec (Suc (length args)) (length a + 5), Dec (Suc (length args)) (length a + 3),
 Goto (Suc (length a)), Inc (length args), Goto 0]"
 shows "{\<lambda>nl. nl = args @ 0 \<up> (max (Suc (length args)) c - length args) @ anything}
 a @ B \<up>"
 proof(rule_tac abc_Hoare_unhaltI, auto)
 = (0, args @ Suc n # 0\<up>(c - Suc (length args)) @ anything)"
 using assms a b c
 proof(rule_tac mn_loop_correct', auto)
 fix i xc
 show "{\<lambda>nl. nl = args @ i # 0 \<up> (c - Suc (length args)) @ xc} a
-{\<lambda>nl. nl = args @ i # rec_eval f (args @ [i]) # 0 \<up> (c - Suc (Suc (length args))) @ xc}"
+{\<lambda>nl. nl = args @ i # rec_exec f (args @ [i]) # 0 \<up> (c - Suc (Suc (length args))) @ xc}"
 using all_termi recursive_compile_correct[of f "args @ [i]" a b c xc] compile a
 by(simp)
 qed
 then obtain stp where d: "stp > n \<and> abc_steps_l (0, args @ 0 # 0\<up>(c - Suc (length args)) @ anything) (a @ B) stp
 = (0, args @ Suc n # 0\<up>(c - Suc (length args)) @ anything)" ..
 by(simp add: replicate_Suc_iff_anywhere Suc_diff_Suc del: replicate_Suc)
 qed
 lemma mn_unhalt_case:
 assumes compile: "rec_ci (Mn n f) = (ap, ar, ft) \<and> length args = ar"
-and all_term: "\<forall> i. terminates f (args @ [i]) \<and> rec_eval f (args @ [i]) > 0"
+and all_term: "\<forall> i. terminate f (args @ [i]) \<and> rec_exec f (args @ [i]) > 0"
 shows "{\<lambda> nl. nl = args @ 0\<up>(ft - ar) @ anything} ap \<up> "
 using assms
 apply(case_tac "rec_ci f", auto simp: rec_ci.simps abc_comp_commute)
 by(rule_tac mn_unhalt_case', simp_all)
 let tp = tm_of (ap [+] dummy_abc k) in
 tp @ (shift (mopup k) (length tp div 2)))"
 lemma recursive_compile_to_tm_correct1:
 assumes  compile: "rec_ci recf = (ap, ary, fp)"
-and termi: " terminates recf args"
+and termi: " terminate recf args"
 and tp: "tp = tm_of (ap [+] dummy_abc (length args))"
 shows "\<exists> stp m l. steps0 (Suc 0, Bk # Bk # ires, <args> @ Bk\<up>rn)
-(tp @ shift (mopup (length args)) (length tp div 2)) stp = (0, Bk\<up>m @ Bk # Bk # ires, Oc\<up>Suc (rec_eval recf args) @ Bk\<up>l)"
+(tp @ shift (mopup (length args)) (length tp div 2)) stp = (0, Bk\<up>m @ Bk # Bk # ires, Oc\<up>Suc (rec_exec recf args) @ Bk\<up>l)"
 proof -
-have "{\<lambda>nl. nl = args} ap [+] dummy_abc (length args) {\<lambda>nl. \<exists>m. nl = args @ rec_eval recf args # 0 \<up> m}"
+have "{\<lambda>nl. nl = args} ap [+] dummy_abc (length args) {\<lambda>nl. \<exists>m. nl = args @ rec_exec recf args # 0 \<up> m}"
 using compile termi compile
 by(rule_tac compile_append_dummy_correct, auto)
 then obtain stp m where h: "abc_steps_l (0, args) (ap [+] dummy_abc (length args)) stp =
-(length (ap [+] dummy_abc (length args)), args @ rec_eval recf args # 0\<up>m) "
+(length (ap [+] dummy_abc (length args)), args @ rec_exec recf args # 0\<up>m) "
 apply(simp add: abc_Hoare_halt_def, auto)
 by(case_tac "abc_steps_l (0, args) (ap [+] dummy_abc (length args)) n", auto)
 thus "?thesis"
 using assms tp
-by(rule_tac  lm = args and stp = stp and am = "args @ rec_eval recf args # 0 \<up> m"
+by(rule_tac  lm = args and stp = stp and am = "args @ rec_exec recf args # 0 \<up> m"
 in compile_correct_halt, auto simp: crsp.simps start_of.simps length_abc_comp abc_lm_v.simps)
 qed
 lemma recursive_compile_to_tm_correct2:
-assumes termi: " terminates recf args"
+assumes termi: " terminate recf args"
 shows "\<exists> stp m l. steps0 (Suc 0, [Bk, Bk], <args>) (tm_of_rec recf) stp =
-(0, Bk\<up>Suc (Suc m), Oc\<up>Suc (rec_eval recf args) @ Bk\<up>l)"
+(0, Bk\<up>Suc (Suc m), Oc\<up>Suc (rec_exec recf args) @ Bk\<up>l)"
 proof(case_tac "rec_ci recf", simp add: tm_of_rec.simps)
 fix ap ar fp
 assume "rec_ci recf = (ap, ar, fp)"
 thus "\<exists>stp m l. steps0 (Suc 0, [Bk, Bk], <args>)
 (tm_of (ap [+] dummy_abc ar) @ shift (mopup ar) (listsum (layout_of (ap [+] dummy_abc ar)))) stp =
-(0, Bk # Bk # Bk \<up> m, Oc # Oc \<up> rec_eval recf args @ Bk \<up> l)"
+(0, Bk # Bk # Bk \<up> m, Oc # Oc \<up> rec_exec recf args @ Bk \<up> l)"
 using recursive_compile_to_tm_correct1[of recf ap ar fp args "tm_of (ap [+] dummy_abc (length args))" "[]" 0]
 assms param_pattern[of recf args ap ar fp]
 by(simp add: replicate_Suc[THEN sym] replicate_Suc_iff_anywhere del: replicate_Suc tm_of_rec_def,
 simp add: exp_suc del: replicate_Suc)
 qed
 lemma recursive_compile_to_tm_correct3:
-assumes termi: "terminates recf args"
+assumes termi: "terminate recf args"
 shows "{\<lambda> tp. tp =([Bk, Bk], <args>)} (tm_of_rec recf)
-{\<lambda> tp. \<exists> k l. tp = (Bk\<up> k, <rec_eval recf args> @ Bk \<up> l)}"
+{\<lambda> tp. \<exists> k l. tp = (Bk\<up> k, <rec_exec recf args> @ Bk \<up> l)}"
 using recursive_compile_to_tm_correct2[OF assms]
 apply(auto simp add: Hoare_halt_def)
 apply(rule_tac x = stp in exI)
 apply(auto simp add: tape_of_nat_abv)
 apply(rule_tac x = "Suc (Suc m)" in exI)

changeset 248	aea02b5a58d2
parent 240	696081f445c2
child 285	447b433b67fa