# HG changeset patch
# User Christian Urban <christian dot urban at kcl dot ac dot uk>
# Date 1366922225 -3600
# Node ID 696081f445c2d465a07c744494ffee9a59b5fb3e
# Parent  ac3309722536f885763ef5354ed02273d1fb6773
added improved Recsursive function theory (not yet finished)

diff -r ac3309722536 -r 696081f445c2 paper.pdf
Binary file paper.pdf has changed
diff -r ac3309722536 -r 696081f445c2 scala/ex.scala
--- a/scala/ex.scala	Wed Apr 24 09:49:00 2013 +0100
+++ b/scala/ex.scala	Thu Apr 25 21:37:05 2013 +0100
@@ -6,12 +6,12 @@
 import comp2._
 
 val Lg = {
- val lgR = Le o (Power o (Id(3, 1), Id(3, 2)), Id(3, 0))
- val conR1 = Conj o (Less o (Const(1) o (Id(2, 0), Id(2, 0))), 
+  val lgR = Le o (Power o (Id(3, 1), Id(3, 2)), Id(3, 0))
+  val conR1 = Conj o (Less o (Const(1) o (Id(2, 0), Id(2, 0))), 
                      Less o (Const(1) o (Id(2, 0), Id(2, 1))))
- val conR2 = Not o (conR1)
- Add o (recs.Mult o (conR1, Maxr(lgR) o (Id(2, 0), Id(2, 1), Id(2, 0))), 
-        recs.Mult o (conR2, Const(0) o (Id(2, 0)))) 
+  val conR2 = Not o (conR1)
+  Add o (recs.Mult o (conR1, Maxr(lgR) o (Id(2, 0), Id(2, 1), Id(2, 0))), 
+         recs.Mult o (conR2, Const(0) o (Id(2, 0)))) 
 }
 
 
@@ -103,10 +103,8 @@
 println("(<=5) 6: " + (Less o (Id(1, 0), Const(5))).eval(6))
 println("Max (<=9): " + Maxr(Le o (Id(1, 0), Const(9))).eval(10))
 println("Max (>=9): " + Maxr(Le o (Const(9), Id(1, 0))).eval(8))
-println("Min (>=9): " + Minr(Le o (Const(9), Id(1, 0))).eval(10))
-println("Min (<=9): " + Minr(Le o (Id(1, 0), Const(9))).eval(10))
-println("Min (>=9): " + Minr(Le o (Const(9), Id(1, 0))).eval(8))
-//println("Lg 4 2: " + Lg.eval(4, 2))
+println("test")
+println("Lg 4 2: " + Lg.eval(4, 2))
 
 // compilation of rec to abacus tests
 def test_comp2(f: Rec, ns: Int*) = {
diff -r ac3309722536 -r 696081f445c2 thys/Rec_Def.thy
--- a/thys/Rec_Def.thy	Wed Apr 24 09:49:00 2013 +0100
+++ b/thys/Rec_Def.thy	Thu Apr 25 21:37:05 2013 +0100
@@ -9,14 +9,10 @@
               |  Pr nat recf recf
               |  Mn nat recf 
 
-definition pred_of_nl :: "nat list \<Rightarrow> nat list"
-  where
-  "pred_of_nl xs = butlast xs @ [last xs - 1]"
-
 function rec_exec :: "recf \<Rightarrow> nat list \<Rightarrow> nat"
   where
   "rec_exec z xs = 0" |
-  "rec_exec s xs = (Suc (xs ! 0))" |
+  "rec_exec s xs = Suc (xs ! 0)" |
   "rec_exec (id m n) xs = (xs ! n)" |
   "rec_exec (Cn n f gs) xs = 
      rec_exec f (map (\<lambda> a. rec_exec a xs) gs)" | 
@@ -31,32 +27,33 @@
 apply(auto simp add: less_Suc_eq_le intro: trans_le_add2 list_size_estimation')
 done
 
-inductive terminate :: "recf \<Rightarrow> nat list \<Rightarrow> bool"
-  where
-  termi_z: "terminate z [n]"
-| termi_s: "terminate s [n]"
-| termi_id: "\<lbrakk>n < m; length xs = m\<rbrakk> \<Longrightarrow> terminate (id m n) xs"
-| termi_cn: "\<lbrakk>terminate f (map (\<lambda>g. rec_exec g xs) gs); 
-              \<forall>g \<in> set gs. terminate g xs; length xs = n\<rbrakk> \<Longrightarrow> terminate (Cn n f gs) xs"
-| termi_pr: "\<lbrakk>\<forall> y < x. terminate g (xs @ y # [rec_exec (Pr n f g) (xs @ [y])]);
-              terminate f xs;
+inductive 
+  terminates :: "recf \<Rightarrow> nat list \<Rightarrow> bool"
+where
+  termi_z: "terminates z [n]"
+| termi_s: "terminates s [n]"
+| termi_id: "\<lbrakk>n < m; length xs = m\<rbrakk> \<Longrightarrow> terminates (id m n) xs"
+| termi_cn: "\<lbrakk>terminates f (map (\<lambda>g. rec_exec g xs) gs); 
+              \<forall>g \<in> set gs. terminates g xs; length xs = n\<rbrakk> \<Longrightarrow> terminates (Cn n f gs) xs"
+| termi_pr: "\<lbrakk>\<forall> y < x. terminates g (xs @ y # [rec_exec (Pr n f g) (xs @ [y])]);
+              terminates f xs;
               length xs = n\<rbrakk> 
-              \<Longrightarrow> terminate (Pr n f g) (xs @ [x])"
-| termi_mn: "\<lbrakk>length xs = n; terminate f (xs @ [r]); 
+              \<Longrightarrow> terminates (Pr n f g) (xs @ [x])"
+| termi_mn: "\<lbrakk>length xs = n; terminates f (xs @ [r]); 
               rec_exec f (xs @ [r]) = 0;
-              \<forall> i < r. terminate f (xs @ [i]) \<and> rec_exec f (xs @ [i]) > 0\<rbrakk> \<Longrightarrow> terminate (Mn n f) xs"
+              \<forall> i < r. terminates f (xs @ [i]) \<and> rec_exec f (xs @ [i]) > 0\<rbrakk> \<Longrightarrow> terminates (Mn n f) xs"
 
 
-inductive_cases terminate_pr_reverse: "terminate (Pr n f g) xs"
+inductive_cases terminates_pr_reverse: "terminates (Pr n f g) xs"
 
-inductive_cases terminate_z_reverse[elim!]: "terminate z xs"
+inductive_cases terminates_z_reverse[elim!]: "terminates z xs"
 
-inductive_cases terminate_s_reverse[elim!]: "terminate s xs"
+inductive_cases terminates_s_reverse[elim!]: "terminates s xs"
 
-inductive_cases terminate_id_reverse[elim!]: "terminate (id m n) xs"
+inductive_cases terminates_id_reverse[elim!]: "terminates (id m n) xs"
 
-inductive_cases terminate_cn_reverse[elim!]: "terminate (Cn n f gs) xs"
+inductive_cases terminates_cn_reverse[elim!]: "terminates (Cn n f gs) xs"
 
-inductive_cases terminate_mn_reverse[elim!]:"terminate (Mn n f) xs"
+inductive_cases terminates_mn_reverse[elim!]:"terminates (Mn n f) xs"
 
 end
\ No newline at end of file
diff -r ac3309722536 -r 696081f445c2 thys/Recs.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/thys/Recs.thy	Thu Apr 25 21:37:05 2013 +0100
@@ -0,0 +1,549 @@
+theory Recs
+imports Main Fact "~~/src/HOL/Number_Theory/Primes"
+begin
+
+lemma if_zero_one [simp]:
+  "(if P then 1 else 0) = (0::nat) \<longleftrightarrow> \<not> P"
+  "(if P then 0 else 1) = (0::nat) \<longleftrightarrow> P"
+  "(0::nat) < (if P then 1 else 0) = P"
+by (simp_all)
+
+lemma nth:
+  "(x # xs) ! 0 = x"
+  "(x # y # xs) ! 1 = y"
+  "(x # y # z # xs) ! 2 = z"
+  "(x # y # z # u # xs) ! 3 = u"
+by (simp_all)
+
+lemma setprod_atMost_Suc[simp]: "(\<Prod>i \<le> Suc n. f i) = (\<Prod>i \<le> n. f i) * f(Suc n)"
+by(simp add:atMost_Suc mult_ac)
+
+lemma setprod_lessThan_Suc[simp]: "(\<Prod>i < Suc n. f i) = (\<Prod>i < n. f i) * f n"
+by (simp add:lessThan_Suc mult_ac)
+
+lemma setsum_add_nat_ivl2: "n \<le> p  \<Longrightarrow>
+  setsum f {..<n} + setsum f {n..p} = setsum f {..p::nat}"
+apply(subst setsum_Un_disjoint[symmetric])
+apply(auto simp add: ivl_disj_un_one)
+done
+
+
+lemma setsum_eq_zero [simp]:
+  fixes n::nat
+  shows "(\<Sum>i < n. f i) = (0::nat) \<longleftrightarrow> (\<forall>i < n. f i = 0)" 
+        "(\<Sum>i \<le> n. f i) = (0::nat) \<longleftrightarrow> (\<forall>i \<le> n. f i = 0)" 
+by (auto)
+
+lemma setprod_eq_zero [simp]:
+  fixes n::nat
+  shows "(\<Prod>i < n. f i) = (0::nat) \<longleftrightarrow> (\<exists>i < n. f i = 0)" 
+        "(\<Prod>i \<le> n. f i) = (0::nat) \<longleftrightarrow> (\<exists>i \<le> n. f i = 0)" 
+by (auto)
+
+lemma setsum_one_less:
+  fixes n::nat
+  assumes "\<forall>i < n. f i \<le> 1" 
+  shows "(\<Sum>i < n. f i) \<le> n"  
+using assms
+by (induct n) (auto)
+
+lemma setsum_least_eq:
+  fixes n p::nat
+  assumes h0: "p \<le> n"
+  assumes h1: "\<forall>i \<in> {..<p}. f i = 1"
+  assumes h2: "\<forall>i \<in> {p..n}. f i = 0"
+  shows "(\<Sum>i \<le> n. f i) = p"  
+proof -
+  have eq_p: "(\<Sum>i \<in> {..<p}. f i) = p" 
+    using h1 by (induct p) (simp_all)
+  have eq_zero: "(\<Sum>i \<in> {p..n}. f i) = 0" 
+    using h2 by auto
+  have "(\<Sum>i \<le> n. f i) = (\<Sum>i \<in> {..<p}. f i) + (\<Sum>i \<in> {p..n}. f i)"
+    using h0 by (simp add: setsum_add_nat_ivl2) 
+  also have "... = (\<Sum>i \<in> {..<p}. f i)" using eq_zero by simp
+  finally show "(\<Sum>i \<le> n. f i) = p" using eq_p by simp
+qed
+
+lemma setprod_one_le:
+  fixes n::nat
+  assumes "\<forall>i \<le> n. f i \<le> (1::nat)" 
+  shows "(\<Prod>i \<le> n. f i) \<le> 1" 
+using assms
+apply(induct n) 
+apply(auto)
+by (metis One_nat_def eq_iff le_0_eq le_SucE mult_0 nat_mult_1)
+
+lemma setprod_greater_zero:
+  fixes n::nat
+  assumes "\<forall>i \<le> n. f i \<ge> (0::nat)" 
+  shows "(\<Prod>i \<le> n. f i) \<ge> 0" 
+using assms
+by (induct n) (auto)
+
+lemma setprod_eq_one:
+  fixes n::nat
+  assumes "\<forall>i \<le> n. f i = Suc 0" 
+  shows "(\<Prod>i \<le> n. f i) = Suc 0" 
+using assms
+by (induct n) (auto)
+
+lemma setsum_cut_off_less:
+  fixes n::nat
+  assumes h1: "m \<le> n"
+  and     h2: "\<forall>i \<in> {m..<n}. f i = 0"
+  shows "(\<Sum>i < n. f i) = (\<Sum>i < m. f i)"
+proof -
+  have eq_zero: "(\<Sum>i \<in> {m..<n}. f i) = 0" 
+    using h2 by auto
+  have "(\<Sum>i < n. f i) = (\<Sum>i \<in> {..<m}. f i) + (\<Sum>i \<in> {m..<n}. f i)"
+    using h1 by (metis atLeast0LessThan le0 setsum_add_nat_ivl) 
+  also have "... = (\<Sum>i \<in> {..<m}. f i)" using eq_zero by simp
+  finally show "(\<Sum>i < n. f i) = (\<Sum>i < m. f i)" by simp
+qed
+
+lemma setsum_cut_off_le:
+  fixes n::nat
+  assumes h1: "m \<le> n"
+  and     h2: "\<forall>i \<in> {m..n}. f i = 0"
+  shows "(\<Sum>i \<le> n. f i) = (\<Sum>i < m. f i)"
+proof -
+  have eq_zero: "(\<Sum>i \<in> {m..n}. f i) = 0" 
+    using h2 by auto
+  have "(\<Sum>i \<le> n. f i) = (\<Sum>i \<in> {..<m}. f i) + (\<Sum>i \<in> {m..n}. f i)"
+    using h1 by (simp add: setsum_add_nat_ivl2)
+  also have "... = (\<Sum>i \<in> {..<m}. f i)" using eq_zero by simp
+  finally show "(\<Sum>i \<le> n. f i) = (\<Sum>i < m. f i)" by simp
+qed
+
+lemma setprod_one [simp]:
+  fixes n::nat
+  shows "(\<Prod>i < n. Suc 0) = Suc 0"
+        "(\<Prod>i \<le> n. Suc 0) = Suc 0"
+by (induct n) (simp_all)
+
+
+datatype recf =  z
+              |  s
+              |  id nat nat
+              |  Cn nat recf "recf list"
+              |  Pr nat recf recf
+              |  Mn nat recf 
+
+fun arity :: "recf \<Rightarrow> nat"
+  where
+  "arity z = 1" 
+| "arity s = 1"
+| "arity (id m n) = m"
+| "arity (Cn n f gs) = n"
+| "arity (Pr n f g) = Suc n"
+| "arity (Mn n f) = n"
+
+abbreviation
+  "CN f gs \<equiv> Cn (arity (hd gs)) f gs"
+
+abbreviation
+  "PR f g \<equiv> Pr (arity f) f g"
+
+fun rec_eval :: "recf \<Rightarrow> nat list \<Rightarrow> nat"
+  where
+  "rec_eval z xs = 0" 
+| "rec_eval s xs = Suc (xs ! 0)" 
+| "rec_eval (id m n) xs = xs ! n" 
+| "rec_eval (Cn n f gs) xs = rec_eval f (map (\<lambda>x. rec_eval x xs) gs)" 
+| "rec_eval (Pr n f g) (0 # xs) = rec_eval f xs"
+| "rec_eval (Pr n f g) (Suc x # xs) = 
+     rec_eval g (x # (rec_eval (Pr n f g) (x # xs)) # xs)"
+| "rec_eval (Mn n f) xs = (LEAST x. rec_eval f (x # xs) = 0)"
+
+inductive 
+  terminates :: "recf \<Rightarrow> nat list \<Rightarrow> bool"
+where
+  termi_z: "terminates z [n]"
+| termi_s: "terminates s [n]"
+| termi_id: "\<lbrakk>n < m; length xs = m\<rbrakk> \<Longrightarrow> terminates (id m n) xs"
+| termi_cn: "\<lbrakk>terminates f (map (\<lambda>g. rec_eval g xs) gs); 
+              \<forall>g \<in> set gs. terminates g xs; length xs = n\<rbrakk> \<Longrightarrow> terminates (Cn n f gs) xs"
+| termi_pr: "\<lbrakk>\<forall> y < x. terminates g (y # (rec_eval (Pr n f g) (y # xs) # xs));
+              terminates f xs;
+              length xs = n\<rbrakk> 
+              \<Longrightarrow> terminates (Pr n f g) (xs @ [x])"
+| termi_mn: "\<lbrakk>length xs = n; terminates f (r # xs); 
+              rec_eval f (r # xs) = 0;
+              \<forall> i < r. terminates f (i # xs) \<and> rec_eval f (i # xs) > 0\<rbrakk> \<Longrightarrow> terminates (Mn n f) xs"
+
+
+section {* Recursive Function Definitions *}
+
+text {*
+  @{text "constn n"} is the recursive function which computes 
+  natural number @{text "n"}.
+*}
+fun constn :: "nat \<Rightarrow> recf"
+  where
+  "constn 0 = z"  |
+  "constn (Suc n) = CN s [constn n]"
+
+definition
+  "rec_swap f = CN f [id 2 1, id 2 0]"
+
+definition
+  "rec_add = PR (id 1 0) (CN s [id 3 1])"
+
+definition 
+  "rec_mult = PR z (CN rec_add [id 3 1, id 3 2])"
+
+definition 
+  "rec_power_swap = PR (constn 1) (CN rec_mult [id 3 1, id 3 2])"
+
+definition
+  "rec_power = rec_swap rec_power_swap"
+
+definition
+  "rec_fact = PR (constn 1) (CN rec_mult [CN s [id 3 0], id 3 1])"
+
+definition 
+  "rec_pred = CN (PR z (id 3 0)) [id 1 0, id 1 0]"
+
+definition 
+  "rec_minus_swap = (PR (id 1 0) (CN rec_pred [id 3 1]))"
+
+definition
+  "rec_minus = rec_swap rec_minus_swap"
+
+text {* Sign function returning 1 when the input argument is greater than @{text "0"}. *}
+definition 
+  "rec_sign = CN rec_minus [constn 1, CN rec_minus [constn 1, id 1 0]]"
+
+definition 
+  "rec_not = CN rec_minus [constn 1, id 1 0]"
+
+text {*
+  @{text "rec_eq"} compares two arguments: returns @{text "1"}
+  if they are equal; @{text "0"} otherwise. *}
+definition 
+  "rec_eq = CN rec_minus 
+             [CN (constn 1) [id 2 0], 
+              CN rec_add [rec_minus, rec_swap rec_minus]]"
+
+definition 
+  "rec_noteq = CN rec_not [rec_eq]"
+
+definition 
+  "rec_conj = CN rec_sign [rec_mult]"
+
+definition 
+  "rec_disj = CN rec_sign [rec_add]"
+
+definition 
+  "rec_imp = CN rec_disj [CN rec_not [id 2 0], id 2 1]"
+
+text {*
+  @{text "rec_less"} compares two arguments and returns @{text "1"} if
+  the first is less than the second; otherwise returns @{text "0"}. *}
+definition 
+  "rec_less = CN rec_sign [rec_swap rec_minus]"
+
+definition 
+  "rec_le = CN rec_disj [rec_less, rec_eq]"
+
+text {* Sigma and Accum for function with one and two arguments *}
+
+definition 
+  "rec_sigma1 f = PR (CN f [z, id 1 0]) (CN rec_add [id 3 1, CN f [s, id 3 2]])"
+
+definition 
+  "rec_sigma2 f = PR (CN f [z, id 2 0, id 2 1]) (CN rec_add [id 4 1, CN f [s, id 4 2, id 4 3]])"
+
+definition 
+  "rec_accum1 f = PR (CN f [z, id 1 0]) (CN rec_mult [id 3 1, CN f [s, id 3 2]])"
+
+definition 
+  "rec_accum2 f = PR (CN f [z, id 2 0, id 2 1]) (CN rec_mult [id 4 1, CN f [s, id 4 2, id 4 3]])"
+
+text {* Bounded quantifiers for one and two arguments *}
+
+definition
+  "rec_all1 f = CN rec_sign [rec_accum1 f]"
+
+definition
+  "rec_all2 f = CN rec_sign [rec_accum2 f]"
+
+definition
+  "rec_ex1 f = CN rec_sign [rec_sigma1 f]"
+
+definition
+  "rec_ex2 f = CN rec_sign [rec_sigma2 f]"
+
+text {* Dvd *}
+
+definition 
+  "rec_dvd_swap = CN (rec_ex2 (CN rec_eq [id 3 2, CN rec_mult [id 3 1, id 3 0]])) [id 2 0, id 2 1, id 2 0]"  
+
+definition 
+  "rec_dvd = rec_swap rec_dvd_swap" 
+
+section {* Correctness of Recursive Functions *}
+
+lemma constn_lemma [simp]: 
+  "rec_eval (constn n) xs = n"
+by (induct n) (simp_all)
+
+lemma swap_lemma [simp]:
+  "rec_eval (rec_swap f) [x, y] = rec_eval f [y, x]"
+by (simp add: rec_swap_def)
+
+lemma add_lemma [simp]: 
+  "rec_eval rec_add [x, y] =  x + y"
+by (induct x) (simp_all add: rec_add_def)
+
+lemma mult_lemma [simp]: 
+  "rec_eval rec_mult [x, y] = x * y"
+by (induct x) (simp_all add: rec_mult_def)
+
+lemma power_swap_lemma [simp]: 
+  "rec_eval rec_power_swap [y, x] = x ^ y"
+by (induct y) (simp_all add: rec_power_swap_def)
+
+lemma power_lemma [simp]: 
+  "rec_eval rec_power [x, y] = x ^ y"
+by (simp add: rec_power_def)
+
+lemma fact_lemma [simp]: 
+  "rec_eval rec_fact [x] = fact x"
+by (induct x) (simp_all add: rec_fact_def)
+
+lemma pred_lemma [simp]: 
+  "rec_eval rec_pred [x] =  x - 1"
+by (induct x) (simp_all add: rec_pred_def)
+
+lemma minus_swap_lemma [simp]: 
+  "rec_eval rec_minus_swap [x, y] = y - x"
+by (induct x) (simp_all add: rec_minus_swap_def)
+
+lemma minus_lemma [simp]: 
+  "rec_eval rec_minus [x, y] = x - y"
+by (simp add: rec_minus_def)
+
+lemma sign_lemma [simp]: 
+  "rec_eval rec_sign [x] = (if x = 0 then 0 else 1)"
+by (simp add: rec_sign_def)
+
+lemma not_lemma [simp]: 
+  "rec_eval rec_not [x] = (if x = 0 then 1 else 0)"
+by (simp add: rec_not_def)
+
+lemma eq_lemma [simp]: 
+  "rec_eval rec_eq [x, y] = (if x = y then 1 else 0)"
+by (simp add: rec_eq_def)
+
+lemma noteq_lemma [simp]: 
+  "rec_eval rec_noteq [x, y] = (if x \<noteq> y then 1 else 0)"
+by (simp add: rec_noteq_def)
+
+lemma conj_lemma [simp]: 
+  "rec_eval rec_conj [x, y] = (if x = 0 \<or> y = 0 then 0 else 1)"
+by (simp add: rec_conj_def)
+
+lemma disj_lemma [simp]: 
+  "rec_eval rec_disj [x, y] = (if x = 0 \<and> y = 0 then 0 else 1)"
+by (simp add: rec_disj_def)
+
+lemma imp_lemma [simp]: 
+  "rec_eval rec_imp [x, y] = (if 0 < x \<and> y = 0 then 0 else 1)"
+by (simp add: rec_imp_def)
+
+lemma less_lemma [simp]: 
+  "rec_eval rec_less [x, y] = (if x < y then 1 else 0)"
+by (simp add: rec_less_def)
+
+lemma le_lemma [simp]: 
+  "rec_eval rec_le [x, y] = (if (x \<le> y) then 1 else 0)"
+by(simp add: rec_le_def)
+
+
+lemma sigma1_lemma [simp]: 
+  shows "rec_eval (rec_sigma1 f) [x, y] = (\<Sum> z \<le> x. (rec_eval f)  [z, y])"
+by (induct x) (simp_all add: rec_sigma1_def)
+
+lemma sigma2_lemma [simp]: 
+  shows "rec_eval (rec_sigma2 f) [x, y1, y2] = (\<Sum> z \<le> x. (rec_eval f)  [z, y1, y2])"
+by (induct x) (simp_all add: rec_sigma2_def)
+
+lemma accum1_lemma [simp]: 
+  shows "rec_eval (rec_accum1 f) [x, y] = (\<Prod> z \<le> x. (rec_eval f)  [z, y])"
+by (induct x) (simp_all add: rec_accum1_def)
+
+lemma accum2_lemma [simp]: 
+  shows "rec_eval (rec_accum2 f) [x, y1, y2] = (\<Prod> z \<le> x. (rec_eval f)  [z, y1, y2])"
+by (induct x) (simp_all add: rec_accum2_def)
+
+lemma ex1_lemma [simp]:
+ "rec_eval (rec_ex1 f) [x, y] = (if (\<exists>z \<le> x. 0 < rec_eval f [z, y]) then 1 else 0)"
+by (simp add: rec_ex1_def)
+
+lemma ex2_lemma [simp]:
+ "rec_eval (rec_ex2 f) [x, y1, y2] = (if (\<exists>z \<le> x. 0 < rec_eval f [z, y1, y2]) then 1 else 0)"
+by (simp add: rec_ex2_def)
+
+lemma all1_lemma [simp]:
+ "rec_eval (rec_all1 f) [x, y] = (if (\<forall>z \<le> x. 0 < rec_eval f [z, y]) then 1 else 0)"
+by (simp add: rec_all1_def)
+
+lemma all2_lemma [simp]:
+ "rec_eval (rec_all2 f) [x, y1, y2] = (if (\<forall>z \<le> x. 0 < rec_eval f [z, y1, y2]) then 1 else 0)"
+by (simp add: rec_all2_def)
+
+
+lemma dvd_alt_def:
+  "(x dvd y) = (\<exists>k\<le>y. y = x * (k::nat))"
+apply(auto simp add: dvd_def)
+apply(case_tac x)
+apply(auto)
+done
+
+lemma dvd_swap_lemma [simp]:
+  "rec_eval rec_dvd_swap [x, y] = (if y dvd x then 1 else 0)"
+unfolding dvd_alt_def
+by (auto simp add: rec_dvd_swap_def)
+
+lemma dvd_lemma [simp]:
+  "rec_eval rec_dvd [x, y] = (if x dvd y then 1 else 0)"
+by (simp add: rec_dvd_def)
+
+definition 
+  "rec_prime = 
+    (let conj1 = CN rec_less [constn 1, id 1 0] in
+     let disj  = CN rec_disj [CN rec_eq [id 2 0, constn 1], rec_eq] in
+     let imp   = CN rec_imp [rec_dvd, disj] in
+     let conj2 = CN (rec_all1 imp) [id 1 0, id 1 0] in
+     CN rec_conj [conj1, conj2])"
+
+lemma prime_alt_def:
+  fixes p::nat
+  shows "prime p = (1 < p \<and> (\<forall>m \<le> p. m dvd p \<longrightarrow> m = 1 \<or> m = p))"
+apply(auto simp add: prime_nat_def dvd_def)
+by (metis One_nat_def le_neq_implies_less less_SucI less_Suc_eq_0_disj less_Suc_eq_le mult_is_0 n_less_n_mult_m not_less_eq_eq)
+
+lemma prime_lemma [simp]: 
+  "rec_eval rec_prime [x] = (if prime x then 1 else 0)"
+by (simp add: rec_prime_def Let_def prime_alt_def)
+
+
+fun Minr :: "(nat list \<Rightarrow> bool) \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat"
+  where "Minr R x y = (let setx = {z | z. z \<le> x \<and> R [z, y]} in 
+                        if (setx = {}) then (Suc x) else (Min setx))"
+
+definition
+  "rec_minr f = rec_sigma (rec_accum (CN rec_not [f]))"
+
+lemma minr_lemma [simp]:
+shows "rec_eval (rec_minr f) [x, y] = Minr (\<lambda>xs. (0 < rec_eval f xs)) x y"
+apply(simp only: rec_minr_def)
+apply(simp only: sigma_lemma)
+apply(simp only: accum_lemma)
+apply(subst rec_eval.simps)
+apply(simp only: map.simps nth)
+apply(simp only: Minr.simps Let_def)
+apply(auto simp del: not_lemma)
+apply(simp)
+apply(simp only: not_lemma sign_lemma)
+apply(rule sym)
+apply(rule Min_eqI)
+apply(auto)[1]
+apply(simp)
+apply(subst setsum_cut_off_le[where m="ya"])
+apply(simp)
+apply(simp)
+apply(metis Icc_subset_Ici_iff atLeast_def in_mono le_refl mem_Collect_eq)
+apply(rule setsum_one_less)
+apply(default)
+apply(rule impI)
+apply(rule setprod_one_le)
+apply(auto split: if_splits)[1]
+apply(simp)
+apply(rule conjI)
+apply(subst setsum_cut_off_le[where m="xa"])
+apply(simp)
+apply(simp)
+apply (metis Icc_subset_Ici_iff atLeast_def in_mono le_refl mem_Collect_eq)
+apply(rule le_trans)
+apply(rule setsum_one_less)
+apply(default)
+apply(rule impI)
+apply(rule setprod_one_le)
+apply(auto split: if_splits)[1]
+apply(simp)
+apply(subgoal_tac "\<exists>l. l = (LEAST z. 0 < rec_eval f [z, y])")
+defer
+apply metis
+apply(erule exE)
+apply(subgoal_tac "l \<le> x")
+defer
+apply (metis not_leE not_less_Least order_trans)
+apply(subst setsum_least_eq)
+apply(rotate_tac 3)
+apply(assumption)
+prefer 3
+apply (metis LeastI_ex)
+apply(auto)[1]
+apply(subgoal_tac "a < (LEAST z. 0 < rec_eval f [z, y])")
+prefer 2
+apply(auto)[1]
+apply(rotate_tac 5)
+apply(drule not_less_Least)
+apply(auto)[1]
+apply(auto)
+by (metis (mono_tags) LeastI_ex)
+
+(*
+lemma prime_alt_iff:
+  fixes x::nat
+  shows "prime x \<longleftrightarrow> 1 < x \<and> (\<forall>u < x. \<forall>v < x. x \<noteq> u * v)"
+unfolding prime_nat_simp dvd_def
+apply(auto)
+by (smt n_less_m_mult_n nat_mult_commute)
+
+lemma prime_alt2_iff:
+  fixes x::nat
+  shows "prime x \<longleftrightarrow> 1 < x \<and> (\<forall>u \<le> x - 1. \<forall>v \<le> x - 1. x \<noteq> u * v)"
+unfolding prime_alt_iff
+sorry
+*)
+
+definition
+  "rec_prime = CN rec_conj 
+                 [CN rec_less [constn 1, id 1 0], 
+                  CN (rec_all (CN (rec_all2 (CN rec_noteq [id 3 2, CN rec_mult [id 3 1, id 3 0]])) 
+                                   [CN rec_pred [id 2 1], id 2 0, id 2 1]))
+                      [CN rec_pred [id 1 0], id 1 0]]"
+
+lemma prime_lemma [simp]: 
+  "rec_eval rec_prime [x] = (if prime x then 1 else 0)"
+apply(rule trans)
+apply(simp add: rec_prime_def)
+apply(simp only: prime_nat_def dvd_def)
+apply(auto)
+apply(drule_tac x="m" in spec)
+apply(auto)
+apply(case_tac m)
+apply(auto)
+apply(case_tac nat)
+apply(auto)
+apply(case_tac k)
+apply(auto)
+apply(case_tac nat)
+apply(auto)
+done
+
+lemma if_zero [simp]:
+  "(0::nat) < (if P then 1 else 0) = P"
+by (simp)
+
+lemma if_cong:
+  "P = Q \<Longrightarrow> (if P then 1 else (0::nat)) = (if Q then 1 else 0)"
+by simp
+
+
+
+
+end
\ No newline at end of file
diff -r ac3309722536 -r 696081f445c2 thys/Recursive.thy
--- a/thys/Recursive.thy	Wed Apr 24 09:49:00 2013 +0100
+++ b/thys/Recursive.thy	Thu Apr 25 21:37:05 2013 +0100
@@ -329,7 +329,7 @@
       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_exec.simps[simp del]
+declare rec_eval.simps[simp del]
 
 lemma abc_comp_commute: "(A [+] B) [+] C = A [+] (B [+] C)"
 apply(auto simp: abc_comp.simps abc_shift.simps)
@@ -339,24 +339,24 @@
 
 
 lemma compile_z_correct: 
-  "\<lbrakk>rec_ci z = (ap, arity, fp); rec_exec z [n] = r\<rbrakk> \<Longrightarrow> 
+  "\<lbrakk>rec_ci z = (ap, arity, fp); rec_eval 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_exec.simps)
+                 numeral_2_eq_2 abc_fetch.simps abc_step_l.simps rec_eval.simps)
 done
 
 lemma compile_s_correct: 
-  "\<lbrakk>rec_ci s = (ap, arity, fp); rec_exec s [n] = r\<rbrakk> \<Longrightarrow> 
+  "\<lbrakk>rec_ci s = (ap, arity, fp); rec_eval 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_exec.simps)
+apply(auto simp: rec_ci.simps rec_ci_s_def compile_s_correct' rec_eval.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_exec (recf.id (length args) n) args # 0 # anything}"
+  {\<lambda>nl. nl = args @ rec_eval (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)}"
@@ -364,12 +364,12 @@
     by(rule_tac addition_correct, auto simp: numeral_2_eq_2 nth_append)
   thus "?thesis"
     using assms
-    by(simp add: addition_inv.simps rec_exec.simps 
+    by(simp add: addition_inv.simps rec_eval.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_exec (recf.id m n) xs = r\<rbrakk>
+  "\<lbrakk>n < m; length xs = m; rec_ci (recf.id m n) = (ap, arity, fp); rec_eval (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
@@ -391,8 +391,8 @@
 done
 
 lemma param_pattern: 
-  "\<lbrakk>terminate f xs; rec_ci f = (p, arity, fp)\<rbrakk> \<Longrightarrow> length xs = arity"
-apply(induct arbitrary: p arity fp rule: terminate.induct)
+  "\<lbrakk>terminates f xs; rec_ci f = (p, arity, fp)\<rbrakk> \<Longrightarrow> length xs = arity"
+apply(induct arbitrary: p arity fp rule: terminates.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)
@@ -590,11 +590,11 @@
 
 lemma [simp]:
   "\<lbrakk>length xs < gf; gf \<le> ft; n < length gs\<rbrakk>
-  \<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_exec (gs ! n) xs, 0 := 0] =
-  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_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_exec (gs ! n) xs"]
+  \<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)
+  [ft + n - length xs := rec_eval (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"
+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)"
+                             "0 \<up> (length gs - n) @ 0 # 0 \<up> length xs @ anything" "ft + n - length xs" "rec_eval (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)
@@ -602,14 +602,14 @@
 
 lemma compile_cn_gs_correct':
   assumes
-  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_exec g xs # 0 \<up> (xb - Suc xa) @ xc}))"
+  g_cond: "\<forall>g\<in>set (take 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}))"
   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_exec i xs) (take n gs) @ 0\<up>(length gs - n) @ 0 \<up> Suc (length xs) @ anything}"
+                    map (\<lambda>i. rec_eval i xs) (take n gs) @ 0\<up>(length gs - n) @ 0 \<up> Suc (length xs) @ anything}"
   using g_cond
 proof(induct n)
   case 0
@@ -624,17 +624,17 @@
 next
   case (Suc n)
   have ind': "\<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_exec g xs # 0 \<up> (xb - Suc xa) @ xc})) \<Longrightarrow>
+     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})) \<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_exec 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_eval 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).
-     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}))"
+     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}))"
     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_exec 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_eval 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"
@@ -650,17 +650,17 @@
       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_exec i xs) (take n gs) @ 
-        rec_exec (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_eval i xs) (take n gs) @ 
+        rec_eval (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_exec 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_eval 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: "terminate (gs!n) xs"
+        have b: "terminates (gs!n) xs"
           using a g_newcond h x
           by(erule_tac x = "gs!n" in ballE, simp_all)
         hence c: "length xs = ga"
@@ -672,18 +672,18 @@
             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_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_exec i xs) 
-          (take n gs) @ rec_exec (gs ! n) xs # 0 \<up> (length gs - Suc n) @ 0 # 0 \<up> length xs @ anything}"
+          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)
+          {\<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}"
         proof(rule_tac abc_Hoare_plus_halt)
-          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_exec (gs!n) xs) # 0 \<up> (ft - Suc (length xs)) @ map (\<lambda>i. rec_exec i xs) 
+          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 
+                {\<lambda>nl. nl = xs @ (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}"
           proof -
             have 
-              "({\<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_exec (gs!n) xs) # 0 \<up> (gf - Suc 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})"
+              "({\<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} 
+            gp {\<lambda>nl. nl = xs @ (rec_eval (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})"
               using a g_newcond h x
               apply(erule_tac x = "gs!n" in ballE)
               apply(simp, simp)
@@ -694,33 +694,33 @@
           qed
         next
           show 
-            "{\<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}
+            "{\<lambda>nl. nl = xs @ 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}
             mv_box ga (ft + n)
-            {\<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}"
+            {\<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}"
           proof -
-            have "{\<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}
-              mv_box ga (ft + n) {\<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)
-              [ft + n := (xs @ rec_exec (gs ! n) xs # 0 \<up> (ft - Suc (length xs)) @ map (\<lambda>i. rec_exec i xs) (take n gs) @ 
+            have "{\<lambda>nl. nl = xs @ 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}
+              mv_box ga (ft + n) {\<lambda>nl. nl = (xs @ 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)
+              [ft + n := (xs @ 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) ! ga +
-              (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) !
+              (xs @ 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) !
                       (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_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 := (xs @ rec_exec (gs ! n) xs # 0 \<up> (ft - Suc (length xs)) @ map (\<lambda>i. rec_exec i xs) (take n gs) @ 
+            moreover have "(xs @ 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)
+              [ft + n := (xs @ 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) ! ga +
-              (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) !
+              (xs @ 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) !
                       (ft + n),  ga := 0]= 
-              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"
+              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"
               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"
@@ -732,7 +732,7 @@
         "{\<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_exec i xs) (take n gs) @ rec_exec (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_eval i xs) (take n gs) @ rec_eval (gs ! n) xs # 0 \<up> (length gs - Suc n) @ 0 # 0 \<up> length xs @ anything}"
         by simp
     qed
   next
@@ -740,7 +740,7 @@
     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_exec i xs) gs @ 0 \<up> Suc (length xs) @ anything}"
+        {\<lambda>nl. nl = xs @ 0 \<up> (ft - length xs) @ map (\<lambda>i. rec_eval i xs) gs @ 0 \<up> Suc (length xs) @ anything}"
       using ind
       by simp
     thus "?thesis"
@@ -751,14 +751,14 @@
     
 lemma compile_cn_gs_correct:
   assumes
-  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_exec g xs # 0 \<up> (xb - Suc xa) @ xc}))"
+  g_cond: "\<forall>g\<in>set 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}))"
   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_exec i xs) gs @ 0 \<up> Suc (length xs) @ anything}"
+                    map (\<lambda>i. rec_eval 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)
@@ -957,14 +957,14 @@
      
 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_exec i xs) gs @ 0 \<up> Suc (length xs) @ anything}
+  map (\<lambda>i. rec_eval 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_exec 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_eval 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_exec i xs) gs @ [0]) @ 
+  have "{\<lambda>nl. nl = [] @ xs @ (0\<up>(?ft - length xs) @  map (\<lambda>i. rec_eval 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_exec i xs) gs @ [0]) @ xs @ anything}"
+        {\<lambda>nl. nl = [] @ 0 \<up> (length xs) @ (0\<up>(?ft - length xs) @  map (\<lambda>i. rec_eval i xs) gs @ [0]) @ xs @ anything}"
     by(rule_tac mv_boxes_correct, auto)
   thus "?thesis"
     by(simp add: replicate_merge_anywhere)
@@ -978,15 +978,15 @@
 
 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_exec 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_eval 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_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}"
+  {\<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}"
 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_exec i xs) gs @ ((0 # xs) @ anything)}
+  hence "{\<lambda> nl. nl = [] @ 0\<up>length gs @ 0\<up>(?ft - length gs) @  map (\<lambda>i. rec_eval i xs) gs @ ((0 # xs) @ anything)}
        mv_boxes ?ft 0 (length gs)
-        {\<lambda> nl. nl = [] @ map (\<lambda>i. rec_exec i xs) gs @ 0\<up>(?ft - length gs) @ 0\<up>length gs @ ((0 # xs) @ anything)}"
+        {\<lambda> nl. nl = [] @ map (\<lambda>i. rec_eval 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
@@ -1007,29 +1007,29 @@
   "\<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_exec i xs) gs @
-  rec_exec (Cn (length xs) f gs) xs # 0 \<up> max (Suc (length xs))
+\<Longrightarrow>  {\<lambda>nl. nl = map (\<lambda>i. rec_eval i xs) gs @
+  rec_eval (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_exec i xs) 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))) - length gs) @
-               rec_exec (Cn (length xs) f gs) xs # 0 \<up> length gs @ xs @ anything}"
+               rec_eval (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_exec i xs) gs @ rec_exec (Cn (length xs) f gs) xs # 0 \<up> ?ft @ xs @ anything"
+  let ?lm= " map (\<lambda>i. rec_eval i xs) gs @ rec_eval (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_exec i xs) gs @
+    = map (\<lambda>i. rec_eval i xs) gs @
     0 \<up> (?ft - length gs) @
-    rec_exec (Cn (length xs) f gs) xs # 0 \<up> length gs @ xs @ anything"
+    rec_eval (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_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_exec (Cn (length xs) f gs) xs"]
+    using list_update_length[of "map (\<lambda>i. rec_eval i xs) gs @ rec_eval (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"]
     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"
@@ -1108,21 +1108,21 @@
 
 lemma clean_paras: 
   "ffp \<ge> length gs \<Longrightarrow>
-  {\<lambda>nl. nl = map (\<lambda>i. rec_exec i xs) 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))) - length gs) @
-  rec_exec (Cn (length xs) f gs) xs # 0 \<up> length gs @ xs @ anything}
+  rec_eval (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_exec (Cn (length xs) f gs) xs # 0 \<up> length gs @ xs @ anything}"
+  rec_eval (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_exec i xs) gs @ 0 \<up> (?ft - length gs) @
-    rec_exec (Cn (length xs) f gs) xs # 0 \<up> length gs @ xs @ anything"
+  let ?lm = "map (\<lambda>i. rec_eval i xs) gs @ 0 \<up> (?ft - length gs) @
+    rec_eval (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_exec (Cn (length xs) f gs) xs # 0 \<up> length gs @ xs @ anything"
+           =  0 \<up> ?ft @  rec_eval (Cn (length xs) f gs) xs # 0 \<up> length gs @ xs @ anything"
     using h
     by(simp add: replicate_merge_anywhere)
   ultimately show "?thesis"
@@ -1132,20 +1132,20 @@
 
 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_exec (Cn (length xs) f gs) xs # 0 \<up> length gs @ xs @ anything}
+  rec_eval (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_exec (Cn (length xs) f gs) xs #
+  rec_eval (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_exec (Cn (length xs) f gs) xs # 0 \<up> length gs @ xs @ anything"
+  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"
   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_exec (Cn (length xs) f gs) xs # 0 \<up> (?ft - (length xs)) @ 0 \<up> length gs @ xs @ anything"
+               =  0 \<up> length xs @ rec_eval (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)
@@ -1156,17 +1156,17 @@
 
 lemma restore_orgin_paras:
   "{\<lambda>nl. nl = 0 \<up> length xs @
-  rec_exec (Cn (length xs) f gs) xs #
+  rec_eval (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_exec (Cn (length xs) f gs) xs # 0 \<up> 
+  {\<lambda>nl. nl = xs @ rec_eval (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_exec (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_eval (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_exec (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_eval (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)
@@ -1174,14 +1174,14 @@
 
 lemma compile_cn_correct':
   assumes f_ind: 
-  "\<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_exec g xs) gs @ 0 \<up> (ffp - far) @ anything} fap
-                {\<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> anything r. rec_eval f (map (\<lambda>g. rec_eval g xs) gs) = rec_eval (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_eval g xs) gs @ rec_eval (Cn (length xs) f gs) xs # 0 \<up> (ffp - Suc far) @ anything}"
   and compile: "rec_ci f = (fap, far, ffp)"
-  and term_f: "terminate f (map (\<lambda>g. rec_exec g xs) gs)"
-  and g_cond: "\<forall>g\<in>set gs. terminate g xs \<and>
+  and term_f: "terminates f (map (\<lambda>g. rec_eval g xs) gs)"
+  and g_cond: "\<forall>g\<in>set 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_exec 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_eval 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)))) [+]
@@ -1191,7 +1191,7 @@
   (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_exec (Cn (length xs) f gs) xs # 
+  {\<lambda>nl. nl = xs @ rec_eval (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)))"
@@ -1204,8 +1204,8 @@
   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_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_exec i xs) gs @ 0\<up>(Suc (length xs)) @ anything"
+  let ?S = "\<lambda>nl. nl = xs @ rec_eval (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"
   show "{?P1} (?A [+] (?B [+] (?C [+] (?D [+] (?E [+] (?F [+] (?G [+] ?H))))))) {?S}"
   proof(rule_tac abc_Hoare_plus_halt)
     show "{?P1} ?A {?Q1}"
@@ -1213,13 +1213,13 @@
       by(rule_tac compile_cn_gs_correct, auto)
   next
     let ?Q2 = "\<lambda>nl. nl = 0 \<up> ?ft @
-                    map (\<lambda>i. rec_exec i xs) gs @ 0 # xs @ anything"
+                    map (\<lambda>i. rec_eval 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_exec i xs) gs @ 0\<up>?ft @ 0 # xs @ anything" 
+      let ?Q3 = "\<lambda> nl. nl = map (\<lambda>i. rec_eval 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"
@@ -1230,7 +1230,7 @@
         thus "{?Q2} ?C {?Q3}"
           by(erule_tac restore_new_paras)
       next
-        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"
+        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"
         have a: "far = length gs"
           using compile term_f
           by(drule_tac param_pattern, auto)
@@ -1241,23 +1241,23 @@
           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_exec g xs) gs @ 0 \<up> (ffp - far) @ 0\<up>(?ft - ffp + far) @ 0 # xs @ anything} fap
-            {\<lambda>nl. nl = map (\<lambda>g. rec_exec g xs) gs @ rec_exec (Cn (length xs) f gs) xs # 
+          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
+            {\<lambda>nl. nl = map (\<lambda>g. rec_eval g xs) gs @ rec_eval (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_exec.simps)
+            by(rule_tac f_ind, simp add: rec_eval.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_exec i xs) gs @
-               0\<up>(?ft - length gs) @ rec_exec (Cn (length xs) f gs) xs # 0\<up>(length gs)@ xs @ anything"
+          let ?Q5 = "\<lambda>nl. nl = map (\<lambda>i. rec_eval i xs) gs @
+               0\<up>(?ft - length gs) @ rec_eval (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_exec (Cn (length xs) f gs) xs # 0\<up>(length gs)@ xs @ anything"
+            let ?Q6 = "\<lambda>nl. nl = 0\<up>?ft @ rec_eval (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
@@ -1265,7 +1265,7 @@
               thus "{?Q5} ?F {?Q6}"
                 by(erule_tac clean_paras)
             next
-              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"
+              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"
               show "{?Q6} (?G [+] ?H) {?S}"
               proof(rule_tac abc_Hoare_plus_halt)
                 show "{?Q6} ?G {?Q7}"
@@ -1283,24 +1283,24 @@
 qed
 
 lemma compile_cn_correct:
-  assumes termi_f: "terminate f (map (\<lambda>g. rec_exec g xs) gs)"
+  assumes termi_f: "terminates f (map (\<lambda>g. rec_eval 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_exec g xs) gs @ 0 \<up> (fp - arity) @ anything} ap
-  {\<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}"
+  \<Longrightarrow> {\<lambda>nl. nl = map (\<lambda>g. rec_eval 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}"
   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_exec g xs # 0 \<up> (xb - Suc xa) @ xc}))"
+  "\<forall>g\<in>set 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}))"
   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_exec (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_eval (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_exec g xs) gs @ 0 \<up> (ffp - far) @ anything} fap
-    {\<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}"
+  then have f_newind: "\<And> anything .{\<lambda>nl. nl = map (\<lambda>g. rec_eval 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}"
     by(rule_tac f_ind, simp_all)
-  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}"
+  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}"
     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)
@@ -1319,9 +1319,9 @@
 
 lemma save_init_rs: 
   "\<lbrakk>length xs = n; ft = max (n+3) (max fft gft)\<rbrakk> 
-     \<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_exec f xs # 0 \<up> (ft - Suc n) @ anything}"
-using mv_box_correct[of n "Suc n" "xs @ rec_exec f xs # 0 \<up> (ft - n) @ anything"]
+     \<Longrightarrow>  {\<lambda>nl. nl = xs @ rec_eval 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}"
+using mv_box_correct[of n "Suc n" "xs @ rec_eval 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
@@ -1371,9 +1371,9 @@
 
 lemma [simp]:
   "length xs = 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_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_exec f xs # 0 \<up> (max (n + 3) (max fft gft) - Suc n) @ x # anything"]
+ \<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)
+    {\<lambda>nl. nl = xs @ 0 # rec_eval 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"]
 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)
@@ -1457,14 +1457,14 @@
 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_exec (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_eval (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_exec (Pr n f g) (xs @ [x - Suc y]) # 0 \<up> (ft - Suc (Suc n)) @ y # anything}"
+     {\<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}"
 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_exec (Pr (length xs) f g) (xs @ [x - Suc y]) #
+[of "(x - Suc y) # rec_eval (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
@@ -1516,7 +1516,7 @@
 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. terminate g (xs @ [y, rec_exec (Pr n f g) (xs @ [y])]);
+lemma [simp]: "\<lbrakk>rec_ci g = (gap, gar, gft); \<forall>y<x. terminates g (xs @ [y, rec_eval (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)
@@ -1563,14 +1563,14 @@
 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_exec_pr_0_simps: "rec_exec (Pr n f g) (xs @ [0]) = rec_exec f xs"
- by(simp add: rec_exec.simps)
+lemma rec_eval_pr_0_simps: "rec_eval (Pr n f g) (xs @ [0]) = rec_eval f xs"
+ by(simp add: rec_eval.simps)
 
-lemma rec_exec_pr_Suc_simps: "rec_exec (Pr n f g) (xs @ [Suc y])
-          = rec_exec g (xs @ [y, rec_exec (Pr n f g) (xs @ [y])])"
+lemma rec_eval_pr_Suc_simps: "rec_eval (Pr n f g) (xs @ [Suc y])
+          = rec_eval g (xs @ [y, rec_eval (Pr n f g) (xs @ [y])])"
 apply(induct y)
-apply(simp add: rec_exec.simps)
-apply(simp add: rec_exec.simps)
+apply(simp add: rec_eval.simps)
+apply(simp add: rec_eval.simps)
 done
 
 lemma [simp]: "Suc (max (n + 3) (max fft gft) - Suc (Suc (Suc n))) = max (n + 3) (max fft gft) - Suc (Suc n)"
@@ -1580,44 +1580,44 @@
   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_exec (Pr n f g) (xs @ [y]) # 0 \<up> (gft - gar) @ anything} gap
-  {\<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 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
+  {\<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})"
   and compile_g: "rec_ci g = (gap, gar, gft)"
-  and termi_g: "\<forall> y<x. terminate g (xs @ [y, rec_exec (Pr n f g) (xs @ [y])])"
+  and termi_g: "\<forall> y<x. terminates g (xs @ [y, rec_eval (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_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_exec (Pr n f g) (xs @ [x - y]) # 0 \<up> (ft - Suc (Suc n)) @ y # anything)"
+  "\<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)
+  code stp = (0, xs @ (x - y) # rec_eval (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_exec (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_eval (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_exec g (xs @ [x - Suc y, rec_exec (Pr n f g) (xs @ [x - Suc y])])
+          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)"
   proof -
-    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)
+    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)
       ((?A [+] (?B [+] ?C))) stp = (length (?A [+] (?B [+] ?C)),  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)"
+      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)"
     proof -
-      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}
+      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}
         (?A [+] (?B [+] ?C)) 
         {\<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}"
+        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}"
       proof(rule_tac abc_Hoare_plus_halt)
-        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}
+        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}
           [Dec ft (length gap + 7)] 
-          {\<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}"
+          {\<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}"
           using ft len
           by(simp)
       next
         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} 
+          "{\<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} 
           ?B [+] ?C
-          {\<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}"
+          {\<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}"
         proof(rule_tac abc_Hoare_plus_halt)
           have a: "gar = Suc (Suc n)" 
             using compile_g termi_g len less
@@ -1625,14 +1625,14 @@
           have b: "gft > gar"
             using compile_g
             by(erule_tac footprint_ge)
-          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_exec (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}"
+          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 
+                {\<lambda>nl. nl = xs @ (x - Suc y) # rec_eval (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}"
           proof -
             have 
-              "{\<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_exec (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> (gft - Suc gar) @ 0\<up>(ft - gft) @ y # anything}"
+              "{\<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_eval (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}"
               using g_ind less by simp
             thus "?thesis"
               using a b ft
@@ -1640,41 +1640,41 @@
           qed
         next
           show "{\<lambda>nl. nl = xs @ (x - Suc y) #
-                    rec_exec (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}
+                    rec_eval (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}
             [Inc n, Dec (Suc n) 3, Goto (Suc 0)]
-            {\<lambda>nl. nl = xs @ (x - y) # 0 # rec_exec g (xs @ [x - Suc y, rec_exec (Pr n f g) 
+            {\<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}"
             using len less
-            using adjust_paras[of xs n "x - Suc y" " rec_exec (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])]) # 
+            using adjust_paras[of xs n "x - Suc y" " rec_eval (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"]
             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_exec (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_eval (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_exec (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_eval (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_exec g (xs @ [x - Suc y, rec_exec (Pr n f g) (xs @ [x - Suc y])])
+          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)" ..
     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_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_exec g (xs @ [x - Suc y, rec_exec (Pr n f g) (xs @ [x - Suc y])]) # 
+    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)
+    ((?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])]) # 
     0 # 0 \<up> (ft - Suc (Suc (Suc n))) @ y # anything)"
     using len
     by(rule_tac loop_back, simp_all)
-  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])"
+  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])"
     using less
-    thm rec_exec.simps
-    apply(case_tac "x - y", simp_all add: rec_exec_pr_Suc_simps)
+    thm rec_eval.simps
+    apply(case_tac "x - y", simp_all add: rec_eval_pr_Suc_simps)
     by(subgoal_tac "nat = x - Suc y", simp, arith)    
   ultimately show "?thesis"
     using code ft
@@ -1682,21 +1682,21 @@
 qed
 
 lemma [simp]: 
-  "length xs = n \<Longrightarrow> abc_lm_s (xs @ x # rec_exec (Pr n f g) (xs @ [x]) # 0 \<up> (max (n + 3) 
+  "length xs = n \<Longrightarrow> abc_lm_s (xs @ x # rec_eval (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_exec (Pr n f g) (xs @ [x]) # 0 \<up> (max (n + 3) (max fft gft) - Suc n) @ anything"
+    xs @ x # rec_eval (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_exec (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_eval (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_exec (Pr (length xs) f g) (xs @ [x]) # 0 \<up> (max (length xs + 3)
+  "(xs @ x # rec_eval (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_exec (Pr (length xs) f g) (xs @ [x]) #
+using nth_append_length[of "xs @ x # rec_eval (Pr (length xs) f g) (xs @ [x]) #
   0 \<up> (max (length xs + 3) (max fft gft) - Suc (Suc (length xs)))" 0  anything]
 by(simp)
 
@@ -1704,12 +1704,12 @@
   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. 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_exec (Pr n f g) (xs @ [y]) # 0 \<up> (gft - gar) @ anything} gap
-  {\<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_exec (Pr n f g) (xs @ [x - y]) # 0 \<up> (max (n + 3) (max fft gft) - Suc (Suc n)) @ y # anything}
+  and termi_g: "\<forall> y<x. terminates g (xs @ [y, rec_eval (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
+  {\<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})"
+  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}
    ([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_exec (Pr n f g) (xs @ [x]) # 0 \<up> (max (n + 3) (max fft gft) - Suc n) @ anything}" 
+   {\<lambda>nl. nl = xs @ x # rec_eval (Pr n f g) (xs @ [x]) # 0 \<up> (max (n + 3) (max fft gft) - Suc n) @ anything}" 
   using less
 proof(induct y)
   case 0
@@ -1725,37 +1725,37 @@
   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_exec (Pr n f g) (xs @ [x - y]) # 0 \<up> (?ft - Suc (Suc n)) @ y # anything}
-         ?C {\<lambda>nl. nl = xs @ x # rec_exec (Pr n f g) (xs @ [x]) # 0 \<up> (?ft - Suc n) @ anything}" by fact 
+         {\<lambda>nl. nl = xs @ (x - y) # rec_eval (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 
   have less: "Suc y \<le> x" by fact
   have stp1: 
-    "\<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_exec (Pr n f g) (xs @ [x - y]) # 0 \<up> (?ft - Suc (Suc n)) @ y # anything)"
+    "\<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)
+    ?C stp  = (0, xs @ (x - y) # rec_eval (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_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_exec (Pr n f g) (xs @ [x - y]) # 0 \<up> (?ft - Suc (Suc n)) @ y # anything)" ..
+    "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)
+   ?C stp1 = (0, xs @ (x - y) # rec_eval (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_exec (Pr n f g) (xs @ [x - y]) # 0 \<up> (?ft - Suc (Suc n)) @ y # anything)
-    ?C stp = (length ?C, xs @ x # rec_exec (Pr n f g) (xs @ [x]) # 0 \<up> (?ft - Suc n) @ anything)"
+    "\<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)
+    ?C stp = (length ?C, xs @ x # rec_eval (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_exec (Pr n f g) 
+    by(auto simp: abc_Hoare_halt_def, case_tac "abc_steps_l (0, xs @ (x - y) # rec_eval (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_exec (Pr n f g) (xs @ [x - y]) # 0 \<up> (?ft - Suc (Suc n)) @ y # anything)
-    ?C stp2 = (length ?C, xs @ x # rec_exec (Pr n f g) (xs @ [x]) # 0 \<up> (?ft - Suc n) @ anything)" ..
+    "abc_steps_l (0, xs @ (x - y) # rec_eval (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)" ..
   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. terminate g (xs @ [y, rec_exec (Pr n f g) (xs @ [y])])"
+  assumes termi_g: "\<forall> y<x. terminates g (xs @ [y, rec_eval (Pr n f g) (xs @ [y])])"
   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_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: "terminate f xs"
-  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}"
+  "\<forall> y<x. (\<forall>anything. {\<lambda>nl. nl = xs @ y # rec_eval (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})"
+  and termi_f: "terminates 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 len: "length xs = n"
   and compile1: "rec_ci f = (fap, far, fft)"
   and compile2: "rec_ci g = (gap, gar, gft)"
@@ -1765,7 +1765,7 @@
   (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_exec (Pr n f g) (xs @ [x]) # 0 \<up> (max (n + 3) (max fft gft) - Suc n) @ anything}"
+  {\<lambda>nl. nl = xs @ x # rec_eval (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"
@@ -1775,14 +1775,14 @@
   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_exec (Pr n f g) (xs @ [x]) # 0 \<up> (?ft - Suc n) @ anything"
+  let ?S = "\<lambda>nl. nl = xs @ x # rec_eval (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_exec f xs # 0 \<up> (?ft - Suc n) @  x # anything"
+    let ?Q2 = "\<lambda>nl. nl = xs @ rec_eval f xs # 0 \<up> (?ft - Suc n) @  x # anything"
     have a: "?ft \<ge> fft"
       by arith
     have b: "far = n"
@@ -1794,7 +1794,7 @@
     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_exec f xs # 0 \<up> (fft - Suc far) @ 0\<up>(?ft - fft) @ x # anything}"
+            {\<lambda>nl. nl = xs @ rec_eval 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
@@ -1804,50 +1804,50 @@
         using b
         by(simp add: replicate_merge_anywhere)
     next
-      let ?Q3 = "\<lambda> nl. nl = xs @ 0 # rec_exec f xs # 0\<up>(?ft - Suc (Suc n)) @ x # anything"
+      let ?Q3 = "\<lambda> nl. nl = xs @ 0 # rec_eval 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_exec f xs # 0 \<up> (max (n + 3) (max fft gft) - 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 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_exec_pr_0_simps)
+          by(simp add: rec_eval_pr_0_simps)
       qed
     qed
   qed
 qed 
 
 lemma compile_pr_correct:
-  assumes g_ind: "\<forall>y<x. terminate g (xs @ [y, rec_exec (Pr n f g) (xs @ [y])]) \<and>
+  assumes g_ind: "\<forall>y<x. terminates g (xs @ [y, rec_eval (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_exec (Pr n f g) (xs @ [y]) # 0 \<up> (xb - xa) @ xc} x
-  {\<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: "terminate f xs"
+  (\<forall>xc. {\<lambda>nl. nl = xs @ y # rec_eval (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}))"
+  and termi_f: "terminates 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_exec 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_eval 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_exec (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_eval (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. (terminate g (xs @ [y, rec_exec (Pr n f g) (xs @ [y])]) \<and>
-     (\<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_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}))"
+    "\<forall>y<x. (terminates g (xs @ [y, rec_eval (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
+    {\<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}))"
     using g_ind h
     by(auto)
-  hence termi_g: "\<forall> y<x. terminate g (xs @ [y, rec_exec (Pr n f g) (xs @ [y])])"
+  hence termi_g: "\<forall> y<x. terminates g (xs @ [y, rec_eval (Pr n f g) (xs @ [y])])"
     by simp
   from g have g_newind: 
-    "\<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_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})"
+    "\<forall> y<x. (\<forall>anything. {\<lambda>nl. nl = xs @ y # rec_eval (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})"
     by auto
-  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}"
+  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}"
     using h
     by(rule_tac f_ind, simp)
   show "?thesis"
@@ -1984,20 +1984,20 @@
   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_exec f (xs @ [x]) # 0 \<up> (fft - Suc far) @ xc}))"
-  and exec_less: "rec_exec f (xs @ [x]) > 0"
+    {\<lambda>nl. nl = xs @ x # rec_eval f (xs @ [x]) # 0 \<up> (fft - Suc far) @ xc}))"
+  and exec_less: "rec_eval 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_exec f (xs @ [x]) # 0 \<up> (ft - Suc (Suc arity)) @ anything)"
+    (length fap, xs @ x # rec_eval 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_exec f (xs @ [x]) # 0 \<up> (ft - Suc (Suc arity)) @ anything)"
+      (length fap, xs @ x # rec_eval 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_exec f (xs @ [x]) # 0 \<up> (fft - Suc far) @ 0\<up>(ft - fft) @ anything}"
+            {\<lambda>nl. nl = xs @ x # rec_eval f (xs @ [x]) # 0 \<up> (fft - Suc far) @ 0\<up>(ft - fft) @ anything}"
         using ind by simp
       moreover have "fft > far"
         using compile
@@ -2008,17 +2008,17 @@
         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_exec f (xs @ [x]) # 0 \<up> (ft - Suc (Suc arity)) @ anything)" ..
+      (length fap, xs @ x # rec_eval 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_exec f (xs @ [x]) # 0 \<up> (ft - Suc (Suc arity)) @ anything) (fap @ B) stp =
+    "\<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 =
     (0, xs @ Suc x # 0 # 0 \<up> (ft - Suc (Suc arity)) @ anything)"
-    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_exec f (xs @ [x]) # 0 \<up> (ft - Suc (Suc arity)) @ anything) (fap @ B) stp, length fap, arity))"     
+    using mn_correct[of f fap far fft "rec_eval 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))"     
       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_exec 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_eval 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)
@@ -2038,8 +2038,8 @@
   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_exec f (xs @ [i]) # 0 \<up> (fft - Suc far) @ xc}))"
-  and exec_ge: "\<forall> i\<le>x. rec_exec f (xs @ [i]) > 0"
+    {\<lambda>nl. nl = xs @ i # rec_eval f (xs @ [i]) # 0 \<up> (fft - Suc far) @ xc}))"
+  and exec_ge: "\<forall> i\<le>x. rec_eval 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 = 
@@ -2052,12 +2052,12 @@
     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_exec f (xs @ [i]) # 0 \<up> (fft - Suc far) @ xc};
-               \<forall>i\<le>x. 0 < rec_exec f (xs @ [i])\<rbrakk> \<Longrightarrow> 
+  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};
+               \<forall>i\<le>x. 0 < rec_eval 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_exec f (xs @ [i])" by fact
+  have exec_ge: "\<forall>i\<le>Suc x. 0 < rec_eval 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_exec f (xs @ [i]) # 0 \<up> (fft - Suc far) @ xc}" by fact
+    {\<lambda>nl. nl = xs @ i # rec_eval 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 =
@@ -2074,8 +2074,8 @@
   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_exec f (xs @ [i]) # 0 \<up> (fft - Suc far) @ xc}))"
-  and exec_ge: "\<forall> i\<le>x. rec_exec f (xs @ [i]) > 0"
+    {\<lambda>nl. nl = xs @ i # rec_eval f (xs @ [i]) # 0 \<up> (fft - Suc far) @ xc}))"
+  and exec_ge: "\<forall> i\<le>x. rec_eval 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 = 
@@ -2092,17 +2092,17 @@
   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: "terminate f (xs @ [r])"
+  and termi_f: "terminates 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_exec f (xs @ [i]) # 0 \<up> (fft - Suc far) @ xc}))"
-  and exec_less: "\<forall> i<r. rec_exec f (xs @ [i]) > 0"
-  and exec: "rec_exec f (xs @ [r]) = 0"
+    {\<lambda>nl. nl = xs @ i # rec_eval f (xs @ [i]) # 0 \<up> (fft - Suc far) @ xc}))"
+  and exec_less: "\<forall> i<r. rec_eval f (xs @ [i]) > 0"
+  and exec: "rec_eval 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_exec (Mn arity f) xs # 0 \<up> (max (Suc arity) fft - Suc arity) @ anything}"
+    {\<lambda>nl. nl = xs @ rec_eval (Mn arity f) xs # 0 \<up> (max (Suc arity) fft - Suc arity) @ anything}"
 proof -
   have a: "far = Suc arity"
     using len compile termi_f
@@ -2117,13 +2117,13 @@
     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_exec f (xs @ [r]) # 0 \<up> (ft - Suc (Suc arity)) @ anything)"
+    (length fap, xs @ r # rec_eval 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_exec f (xs @ [r]) # 0 \<up> (ft - Suc (Suc arity)) @ anything)"
+      (length fap, xs @ r # rec_eval 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_exec f (xs @ [r]) # 0 \<up> (fft - Suc far) @ 0\<up>(ft - fft) @ anything}"
+            {\<lambda>nl. nl = xs @ r # rec_eval 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
@@ -2131,20 +2131,20 @@
         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_exec f (xs @ [r]) # 0 \<up> (ft - Suc (Suc arity)) @ anything)" ..
+      (length fap, xs @ r # rec_eval 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_exec f (xs @ [r]) # 0 \<up> (ft - Suc (Suc arity)) @ anything) (fap @ B) stp = 
-             (length fap + 5, xs @ r # rec_exec f (xs @ [r]) # 0 \<up> (ft - Suc (Suc arity)) @ anything)"
+    "\<exists> stp. abc_steps_l (length fap, xs @ r # rec_eval 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)"
     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_exec (Mn (length xs) f) xs = r"
+  moreover have "rec_eval (Mn (length xs) f) xs = r"
     using exec exec_less
-    apply(auto simp: rec_exec.simps Least_def)
+    apply(auto simp: rec_eval.simps Least_def)
     thm the_equality
     apply(rule_tac the_equality, auto)
     apply(metis exec_less less_not_refl3 linorder_not_less)
@@ -2158,18 +2158,18 @@
 
 lemma compile_mn_correct:
   assumes len: "length xs = n"
-  and termi_f: "terminate f (xs @ [r])"
+  and termi_f: "terminates 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_exec f (xs @ [r]) = 0"
+  and exec: "rec_eval f (xs @ [r]) = 0"
   and ind_all: 
-  "\<forall>i<r. terminate f (xs @ [i]) \<and>
+  "\<forall>i<r. terminates 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_exec f (xs @ [i]) # 0 \<up> (xb - Suc xa) @ xc})) \<and>
-  0 < rec_exec f (xs @ [i])"
+  (\<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>
+  0 < rec_eval 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_exec (Mn n f) xs # 0 \<up> (fp - Suc arity) @ anything}"
+  {\<lambda>nl. nl = xs @ rec_eval (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)"
@@ -2179,10 +2179,10 @@
     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_exec f (xs @ [i]) # 0 \<up> (fft - Suc far) @ xc}))"
+    {\<lambda>nl. nl = xs @ i # rec_eval f (xs @ [i]) # 0 \<up> (fft - Suc far) @ xc}))"
     using ind_all h
     by(auto)
-  have all_less: "\<forall> i<r. rec_exec f (xs @ [i]) > 0"
+  have all_less: "\<forall> i<r. rec_eval f (xs @ [i]) > 0"
     using ind_all by auto
   show "?thesis"
     using h compile f_newind newind_all all_less len termi_f exec
@@ -2191,10 +2191,10 @@
 qed
     
 lemma recursive_compile_correct:
-   "\<lbrakk>terminate recf args; rec_ci recf = (ap, arity, fp)\<rbrakk>
+   "\<lbrakk>terminates 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_exec recf args # 0\<up>(fp - Suc arity) @ anything}"
-apply(induct arbitrary: ap arity fp anything r rule: terminate.induct)
+         {\<lambda> nl. nl = args@ rec_eval recf args # 0\<up>(fp - Suc arity) @ anything}"
+apply(induct arbitrary: ap arity fp anything r rule: terminates.induct)
 apply(simp_all add: compile_s_correct compile_z_correct compile_id_correct 
                     compile_cn_correct compile_pr_correct compile_mn_correct)
 done
@@ -2323,8 +2323,8 @@
 
 lemma recursive_compile_correct_norm': 
   "\<lbrakk>rec_ci f = (ap, arity, ft);  
-    terminate f args\<rbrakk>
-  \<Longrightarrow> \<exists> stp rl. (abc_steps_l (0, args) ap stp) = (length ap, rl) \<and> abc_list_crsp (args @ [rec_exec f args]) rl"
+    terminates 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"
   using recursive_compile_correct[of f args ap arity ft "[]"]
 apply(auto simp: abc_Hoare_halt_def)
 apply(rule_tac x = n in exI)
@@ -2334,9 +2334,9 @@
 done
 
 lemma [simp]:
-  assumes a: "args @ [rec_exec f args] = lm @ 0 \<up> n"
+  assumes a: "args @ [rec_eval f args] = lm @ 0 \<up> n"
   and b: "length args < length lm"
-  shows "\<exists>m. lm = args @ rec_exec f args # 0 \<up> m"
+  shows "\<exists>m. lm = args @ rec_eval f args # 0 \<up> m"
 using assms
 apply(case_tac n, simp)
 apply(rule_tac x = 0 in exI, simp)
@@ -2344,9 +2344,9 @@
 done
 
 lemma [simp]: 
-"\<lbrakk>args @ [rec_exec f args] = lm @ 0 \<up> n; \<not> length args < length lm\<rbrakk>
+"\<lbrakk>args @ [rec_eval 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_exec f args # 0 \<up> m"
+  args @ rec_eval 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)
@@ -2355,16 +2355,16 @@
 
 lemma compile_append_dummy_correct: 
   assumes compile: "rec_ci f = (ap, ary, fp)"
-  and termi: "terminate f args"
-  shows "{\<lambda> nl. nl = args} (ap [+] dummy_abc (length args)) {\<lambda> nl. (\<exists> m. nl = args @ rec_exec f args # 0\<up>m)}"
+  and termi: "terminates 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)}"
 proof(rule_tac abc_Hoare_plus_halt)
-  show "{\<lambda>nl. nl = args} ap {\<lambda> nl. abc_list_crsp (args @ [rec_exec f args]) nl}"
+  show "{\<lambda>nl. nl = args} ap {\<lambda> nl. abc_list_crsp (args @ [rec_eval 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_exec f args])} dummy_abc (length args) 
-    {\<lambda>nl. \<exists>m. nl = args @ rec_exec f args # 0 \<up> m}"
+  show "{abc_list_crsp (args @ [rec_eval f args])} dummy_abc (length args) 
+    {\<lambda>nl. \<exists>m. nl = args @ rec_eval 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
@@ -2386,15 +2386,15 @@
   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_exec (gs!j) args # 0\<up>(ftj - Suc arj) @ anything}"
-  and all_termi: "\<forall> j<i. terminate (gs!j) args"
+  \<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}"
+  and all_termi: "\<forall> j<i. terminates (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_exec i args) (take i gs) @ 
+  let ?Q = "\<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"
   have "cn_merge_gs (map rec_ci gs) ?ft = 
     cn_merge_gs (map rec_ci (take i gs)) ?ft [+] (gap [+] 
@@ -2403,11 +2403,11 @@
   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_exec 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_eval 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_exec i args) (take i gs) @ 0 \<up> (length gs - i) @ 0 \<up> Suc (length args) @ anything"]
+        map (\<lambda>i. rec_eval 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
@@ -2424,7 +2424,7 @@
     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_exec i args) (take i gs) @ 0 \<up> (length gs - i) @ 0 \<up> Suc (length args) @ anything}"
+      map (\<lambda>i. rec_eval 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)
@@ -2435,7 +2435,7 @@
 
 lemma mn_unhalt_case':
   assumes compile: "rec_ci f = (a, b, c)"
-  and all_termi: "\<forall>i. terminate f (args @ [i]) \<and> 0 < rec_exec f (args @ [i])"
+  and all_termi: "\<forall>i. terminates f (args @ [i]) \<and> 0 < rec_eval 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}
@@ -2455,7 +2455,7 @@
   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_exec f (args @ [i]) # 0 \<up> (c - Suc (Suc (length args))) @ xc}"
+      {\<lambda>nl. nl = args @ i # rec_eval 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
@@ -2477,7 +2477,7 @@
     
 lemma mn_unhalt_case: 
   assumes compile: "rec_ci (Mn n f) = (ap, ar, ft) \<and> length args = ar"
-  and all_term: "\<forall> i. terminate f (args @ [i]) \<and> rec_exec f (args @ [i]) > 0"
+  and all_term: "\<forall> i. terminates f (args @ [i]) \<and> rec_eval 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)
@@ -2490,34 +2490,34 @@
 
 lemma recursive_compile_to_tm_correct1: 
   assumes  compile: "rec_ci recf = (ap, ary, fp)"
-  and termi: " terminate recf args"
+  and termi: " terminates 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_exec 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_eval recf args) @ Bk\<up>l)"
 proof -
-  have "{\<lambda>nl. nl = args} ap [+] dummy_abc (length args) {\<lambda>nl. \<exists>m. nl = args @ rec_exec recf args # 0 \<up> m}"
+  have "{\<lambda>nl. nl = args} ap [+] dummy_abc (length args) {\<lambda>nl. \<exists>m. nl = args @ rec_eval 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_exec recf args # 0\<up>m) "
+    (length (ap [+] dummy_abc (length args)), args @ rec_eval 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_exec recf args # 0 \<up> m"
+    by(rule_tac  lm = args and stp = stp and am = "args @ rec_eval 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: " terminate recf args"
+  assumes termi: " terminates 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_exec recf args) @ Bk\<up>l)"
+                     (0, Bk\<up>Suc (Suc m), Oc\<up>Suc (rec_eval 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_exec recf args @ Bk \<up> l)"
+    (0, Bk # Bk # Bk \<up> m, Oc # Oc \<up> rec_eval 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, 
@@ -2525,9 +2525,9 @@
 qed
 
 lemma recursive_compile_to_tm_correct3: 
-  assumes termi: "terminate recf args"
+  assumes termi: "terminates recf args"
   shows "{\<lambda> tp. tp =([Bk, Bk], <args>)} (tm_of_rec recf) 
-         {\<lambda> tp. \<exists> k l. tp = (Bk\<up> k, <rec_exec recf args> @ Bk \<up> l)}"
+         {\<lambda> tp. \<exists> k l. tp = (Bk\<up> k, <rec_eval 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)
diff -r ac3309722536 -r 696081f445c2 thys/UF.thy
--- a/thys/UF.thy	Wed Apr 24 09:49:00 2013 +0100
+++ b/thys/UF.thy	Thu Apr 25 21:37:05 2013 +0100
@@ -153,46 +153,46 @@
                         @ [Cn (Suc vl) s [id (Suc vl) (vl - 1)]])]))"
 
 
-declare rec_exec.simps[simp del] constn.simps[simp del]
+declare rec_eval.simps[simp del] constn.simps[simp del]
 
 
 section {* Correctness of various recursive functions *}
 
 
-lemma add_lemma: "rec_exec rec_add [x, y] =  x + y"
-by(induct_tac y, auto simp: rec_add_def rec_exec.simps)
-
-lemma mult_lemma: "rec_exec rec_mult [x, y] = x * y"
-by(induct_tac y, auto simp: rec_mult_def rec_exec.simps add_lemma)
-
-lemma pred_lemma: "rec_exec rec_pred [x] =  x - 1"
-by(induct_tac x, auto simp: rec_pred_def rec_exec.simps)
-
-lemma minus_lemma: "rec_exec rec_minus [x, y] = x - y"
-by(induct_tac y, auto simp: rec_exec.simps rec_minus_def pred_lemma)
-
-lemma sg_lemma: "rec_exec rec_sg [x] = (if x = 0 then 0 else 1)"
-by(auto simp: rec_sg_def minus_lemma rec_exec.simps constn.simps)
-
-lemma constn_lemma: "rec_exec (constn n) [x] = n"
-by(induct n, auto simp: rec_exec.simps constn.simps)
-
-lemma less_lemma: "rec_exec rec_less [x, y] = (if x < y then 1 else 0)"
-by(induct_tac y, auto simp: rec_exec.simps 
+lemma add_lemma: "rec_eval rec_add [x, y] =  x + y"
+by(induct_tac y, auto simp: rec_add_def rec_eval.simps)
+
+lemma mult_lemma: "rec_eval rec_mult [x, y] = x * y"
+by(induct_tac y, auto simp: rec_mult_def rec_eval.simps add_lemma)
+
+lemma pred_lemma: "rec_eval rec_pred [x] =  x - 1"
+by(induct_tac x, auto simp: rec_pred_def rec_eval.simps)
+
+lemma minus_lemma: "rec_eval rec_minus [x, y] = x - y"
+by(induct_tac y, auto simp: rec_eval.simps rec_minus_def pred_lemma)
+
+lemma sg_lemma: "rec_eval rec_sg [x] = (if x = 0 then 0 else 1)"
+by(auto simp: rec_sg_def minus_lemma rec_eval.simps constn.simps)
+
+lemma constn_lemma: "rec_eval (constn n) [x] = n"
+by(induct n, auto simp: rec_eval.simps constn.simps)
+
+lemma less_lemma: "rec_eval rec_less [x, y] = (if x < y then 1 else 0)"
+by(induct_tac y, auto simp: rec_eval.simps 
   rec_less_def minus_lemma sg_lemma)
 
-lemma not_lemma: "rec_exec rec_not [x] = (if x = 0 then 1 else 0)"
-by(induct_tac x, auto simp: rec_exec.simps rec_not_def
+lemma not_lemma: "rec_eval rec_not [x] = (if x = 0 then 1 else 0)"
+by(induct_tac x, auto simp: rec_eval.simps rec_not_def
   constn_lemma minus_lemma)
 
-lemma eq_lemma: "rec_exec rec_eq [x, y] = (if x = y then 1 else 0)"
-by(induct_tac y, auto simp: rec_exec.simps rec_eq_def constn_lemma add_lemma minus_lemma)
-
-lemma conj_lemma: "rec_exec rec_conj [x, y] = (if x = 0 \<or> y = 0 then 0 else 1)"
-by(induct_tac y, auto simp: rec_exec.simps sg_lemma rec_conj_def mult_lemma)
-
-lemma disj_lemma: "rec_exec rec_disj [x, y] = (if x = 0 \<and> y = 0 then 0 else 1)"
-by(induct_tac y, auto simp: rec_disj_def sg_lemma add_lemma rec_exec.simps)
+lemma eq_lemma: "rec_eval rec_eq [x, y] = (if x = y then 1 else 0)"
+by(induct_tac y, auto simp: rec_eval.simps rec_eq_def constn_lemma add_lemma minus_lemma)
+
+lemma conj_lemma: "rec_eval rec_conj [x, y] = (if x = 0 \<or> y = 0 then 0 else 1)"
+by(induct_tac y, auto simp: rec_eval.simps sg_lemma rec_conj_def mult_lemma)
+
+lemma disj_lemma: "rec_eval rec_disj [x, y] = (if x = 0 \<and> y = 0 then 0 else 1)"
+by(induct_tac y, auto simp: rec_disj_def sg_lemma add_lemma rec_eval.simps)
 
 declare mult_lemma[simp] add_lemma[simp] pred_lemma[simp] 
         minus_lemma[simp] sg_lemma[simp] constn_lemma[simp] 
@@ -246,7 +246,7 @@
     by auto
 qed
 
-declare rec_exec.simps[simp del] get_fstn_args.simps[simp del]
+declare rec_eval.simps[simp del] get_fstn_args.simps[simp del]
         arity.simps[simp del] Sigma.simps[simp del]
         rec_sigma.simps[simp del]
 
@@ -254,20 +254,20 @@
   by(simp add: arity.simps)
 
 lemma rec_pr_0_simp_rewrite: "
-  rec_exec (Pr n f g) (xs @ [0]) = rec_exec f xs"
-  by(simp add: rec_exec.simps)
+  rec_eval (Pr n f g) (xs @ [0]) = rec_eval f xs"
+  by(simp add: rec_eval.simps)
 
 lemma rec_pr_0_simp_rewrite_single_param: "
-  rec_exec (Pr n f g) [0] = rec_exec f []"
-  by(simp add: rec_exec.simps)
+  rec_eval (Pr n f g) [0] = rec_eval f []"
+  by(simp add: rec_eval.simps)
 
 lemma rec_pr_Suc_simp_rewrite: 
-  "rec_exec (Pr n f g) (xs @ [Suc x]) = rec_exec g (xs @ [x] @ [rec_exec (Pr n f g) (xs @ [x])])"
-by(simp add: rec_exec.simps)
+  "rec_eval (Pr n f g) (xs @ [Suc x]) = rec_eval g (xs @ [x] @ [rec_eval (Pr n f g) (xs @ [x])])"
+by(simp add: rec_eval.simps)
 
 lemma rec_pr_Suc_simp_rewrite_single_param: 
-  "rec_exec (Pr n f g) ([Suc x]) = rec_exec g ([x] @ [rec_exec (Pr n f g) ([x])])"
-by(simp add: rec_exec.simps)
+  "rec_eval (Pr n f g) ([Suc x]) = rec_eval g ([x] @ [rec_eval (Pr n f g) ([x])])"
+by(simp add: rec_eval.simps)
 
 lemma Sigma_0_simp_rewrite_single_param:
   "Sigma f [0] = f [0]"
@@ -289,13 +289,13 @@
 by(simp add: nth_append)
   
 lemma get_fstn_args_take: "\<lbrakk>length xs = m; n \<le> m\<rbrakk> \<Longrightarrow> 
-  map (\<lambda> f. rec_exec f xs) (get_fstn_args m n)= take n xs"
+  map (\<lambda> f. rec_eval f xs) (get_fstn_args m n)= take n xs"
 proof(induct n)
   case 0 thus "?case"
     by(simp add: get_fstn_args.simps)
 next
   case (Suc n) thus "?case"
-    by(simp add: get_fstn_args.simps rec_exec.simps 
+    by(simp add: get_fstn_args.simps rec_eval.simps 
              take_Suc_conv_app_nth)
 qed
     
@@ -307,11 +307,11 @@
 
 lemma rec_sigma_Suc_simp_rewrite: 
   "primerec f (Suc (length xs))
-    \<Longrightarrow> rec_exec (rec_sigma f) (xs @ [Suc x]) = 
-    rec_exec (rec_sigma f) (xs @ [x]) + rec_exec f (xs @ [Suc x])"
+    \<Longrightarrow> rec_eval (rec_sigma f) (xs @ [Suc x]) = 
+    rec_eval (rec_sigma f) (xs @ [x]) + rec_eval f (xs @ [Suc x])"
   apply(induct x)
   apply(auto simp: rec_sigma.simps Let_def rec_pr_Suc_simp_rewrite
-                   rec_exec.simps get_fstn_args_take)
+                   rec_eval.simps get_fstn_args_take)
   done      
 
 text {*
@@ -319,9 +319,9 @@
   *}
 lemma sigma_lemma: 
   "primerec rg (Suc (length xs))
-     \<Longrightarrow> rec_exec (rec_sigma rg) (xs @ [x]) = Sigma (rec_exec rg) (xs @ [x])"
+     \<Longrightarrow> rec_eval (rec_sigma rg) (xs @ [x]) = Sigma (rec_eval rg) (xs @ [x])"
 apply(induct x)
-apply(auto simp: rec_exec.simps rec_sigma.simps Let_def 
+apply(auto simp: rec_eval.simps rec_sigma.simps Let_def 
          get_fstn_args_take Sigma_0_simp_rewrite
          Sigma_Suc_simp_rewrite) 
 done
@@ -366,11 +366,11 @@
 
 lemma rec_accum_Suc_simp_rewrite: 
   "primerec f (Suc (length xs))
-    \<Longrightarrow> rec_exec (rec_accum f) (xs @ [Suc x]) = 
-    rec_exec (rec_accum f) (xs @ [x]) * rec_exec f (xs @ [Suc x])"
+    \<Longrightarrow> rec_eval (rec_accum f) (xs @ [Suc x]) = 
+    rec_eval (rec_accum f) (xs @ [x]) * rec_eval f (xs @ [Suc x])"
   apply(induct x)
   apply(auto simp: rec_sigma.simps Let_def rec_pr_Suc_simp_rewrite
-                   rec_exec.simps get_fstn_args_take)
+                   rec_eval.simps get_fstn_args_take)
   done  
 
 text {*
@@ -378,9 +378,9 @@
 *}
 lemma accum_lemma :
   "primerec rg (Suc (length xs))
-     \<Longrightarrow> rec_exec (rec_accum rg) (xs @ [x]) = Accum (rec_exec rg) (xs @ [x])"
+     \<Longrightarrow> rec_eval (rec_accum rg) (xs @ [x]) = Accum (rec_eval rg) (xs @ [x])"
 apply(induct x)
-apply(auto simp: rec_exec.simps rec_sigma.simps Let_def 
+apply(auto simp: rec_eval.simps rec_sigma.simps Let_def 
                      get_fstn_args_take)
 done
 
@@ -399,10 +399,10 @@
                  (get_fstn_args (vl - 1) (vl - 1) @ [rt])])"
 
 lemma rec_accum_ex: "primerec rf (Suc (length xs)) \<Longrightarrow>
-     (rec_exec (rec_accum rf) (xs @ [x]) = 0) = 
-      (\<exists> t \<le> x. rec_exec rf (xs @ [t]) = 0)"
+     (rec_eval (rec_accum rf) (xs @ [x]) = 0) = 
+      (\<exists> t \<le> x. rec_eval rf (xs @ [t]) = 0)"
 apply(induct x, simp_all add: rec_accum_Suc_simp_rewrite)
-apply(simp add: rec_exec.simps rec_accum.simps get_fstn_args_take, 
+apply(simp add: rec_eval.simps rec_accum.simps get_fstn_args_take, 
       auto)
 apply(rule_tac x = ta in exI, simp)
 apply(case_tac "t = Suc x", simp_all)
@@ -415,16 +415,16 @@
 lemma all_lemma: 
   "\<lbrakk>primerec rf (Suc (length xs));
     primerec rt (length xs)\<rbrakk>
-  \<Longrightarrow> rec_exec (rec_all rt rf) xs = (if (\<forall> x \<le> (rec_exec rt xs). 0 < rec_exec rf (xs @ [x])) then 1
+  \<Longrightarrow> rec_eval (rec_all rt rf) xs = (if (\<forall> x \<le> (rec_eval rt xs). 0 < rec_eval rf (xs @ [x])) then 1
                                                                                               else 0)"
 apply(auto simp: rec_all.simps)
-apply(simp add: rec_exec.simps map_append get_fstn_args_take split: if_splits)
-apply(drule_tac x = "rec_exec rt xs" in rec_accum_ex)
-apply(case_tac "rec_exec (rec_accum rf) (xs @ [rec_exec rt xs]) = 0", simp_all)
+apply(simp add: rec_eval.simps map_append get_fstn_args_take split: if_splits)
+apply(drule_tac x = "rec_eval rt xs" in rec_accum_ex)
+apply(case_tac "rec_eval (rec_accum rf) (xs @ [rec_eval rt xs]) = 0", simp_all)
 apply(erule_tac exE, erule_tac x = t in allE, simp)
-apply(simp add: rec_exec.simps map_append get_fstn_args_take)
-apply(drule_tac x = "rec_exec rt xs" in rec_accum_ex)
-apply(case_tac "rec_exec (rec_accum rf) (xs @ [rec_exec rt xs]) = 0", simp, simp)
+apply(simp add: rec_eval.simps map_append get_fstn_args_take)
+apply(drule_tac x = "rec_eval rt xs" in rec_accum_ex)
+apply(case_tac "rec_eval (rec_accum rf) (xs @ [rec_eval rt xs]) = 0", simp, simp)
 apply(erule_tac x = x in allE, simp)
 done
 
@@ -441,10 +441,10 @@
                   (get_fstn_args (vl - 1) (vl - 1) @ [rt])])"
 
 lemma rec_sigma_ex: "primerec rf (Suc (length xs))
-          \<Longrightarrow> (rec_exec (rec_sigma rf) (xs @ [x]) = 0) = 
-                          (\<forall> t \<le> x. rec_exec rf (xs @ [t]) = 0)"
+          \<Longrightarrow> (rec_eval (rec_sigma rf) (xs @ [x]) = 0) = 
+                          (\<forall> t \<le> x. rec_eval rf (xs @ [t]) = 0)"
 apply(induct x, simp_all add: rec_sigma_Suc_simp_rewrite)
-apply(simp add: rec_exec.simps rec_sigma.simps 
+apply(simp add: rec_eval.simps rec_sigma.simps 
                 get_fstn_args_take, auto)
 apply(case_tac "t = Suc x", simp_all)
 done
@@ -455,13 +455,13 @@
 lemma ex_lemma:"
   \<lbrakk>primerec rf (Suc (length xs));
    primerec rt (length xs)\<rbrakk>
-\<Longrightarrow> (rec_exec (rec_ex rt rf) xs =
-    (if (\<exists> x \<le> (rec_exec rt xs). 0 <rec_exec rf (xs @ [x])) then 1
+\<Longrightarrow> (rec_eval (rec_ex rt rf) xs =
+    (if (\<exists> x \<le> (rec_eval rt xs). 0 <rec_eval rf (xs @ [x])) then 1
      else 0))"
-apply(auto simp: rec_ex.simps rec_exec.simps map_append get_fstn_args_take 
+apply(auto simp: rec_ex.simps rec_eval.simps map_append get_fstn_args_take 
             split: if_splits)
-apply(drule_tac x = "rec_exec rt xs" in rec_sigma_ex, simp)
-apply(drule_tac x = "rec_exec rt xs" in rec_sigma_ex, simp)
+apply(drule_tac x = "rec_eval rt xs" in rec_sigma_ex, simp)
+apply(drule_tac x = "rec_eval rt xs" in rec_sigma_ex, simp)
 done
 
 text {*
@@ -523,7 +523,7 @@
 by(insert Minr_range[of Rr xs w], auto)
 
 text {* 
-  @{text "rec_Minr"} is the recursive function 
+  @{text "rec_Minmr"} is the recursive function 
   used to implement @{text "Minr"}:
   if @{text "Rr"} is implemented by a recursive function @{text "recf"},
   then @{text "rec_Minr recf"} is the recursive function used to 
@@ -637,11 +637,11 @@
 apply(case_tac i, auto intro: prime_id)
 done
 
-lemma Min_false1[simp]: "\<lbrakk>\<not> Min {uu. uu \<le> w \<and> 0 < rec_exec rf (xs @ [uu])} \<le> w;
-       x \<le> w; 0 < rec_exec rf (xs @ [x])\<rbrakk>
+lemma Min_false1[simp]: "\<lbrakk>\<not> Min {uu. uu \<le> w \<and> 0 < rec_eval rf (xs @ [uu])} \<le> w;
+       x \<le> w; 0 < rec_eval rf (xs @ [x])\<rbrakk>
       \<Longrightarrow>  False"
-apply(subgoal_tac "finite {uu. uu \<le> w \<and> 0 < rec_exec rf (xs @ [uu])}")
-apply(subgoal_tac "{uu. uu \<le> w \<and> 0 < rec_exec rf (xs @ [uu])} \<noteq> {}")
+apply(subgoal_tac "finite {uu. uu \<le> w \<and> 0 < rec_eval rf (xs @ [uu])}")
+apply(subgoal_tac "{uu. uu \<le> w \<and> 0 < rec_eval rf (xs @ [uu])} \<noteq> {}")
 apply(simp add: Min_le_iff, simp)
 apply(rule_tac x = x in exI, simp)
 apply(simp)
@@ -649,12 +649,12 @@
 
 lemma sigma_minr_lemma: 
   assumes prrf:  "primerec rf (Suc (length xs))"
-  shows "UF.Sigma (rec_exec (rec_all (recf.id (Suc (length xs)) (length xs))
+  shows "UF.Sigma (rec_eval (rec_all (recf.id (Suc (length xs)) (length xs))
      (Cn (Suc (Suc (length xs))) rec_not
       [Cn (Suc (Suc (length xs))) rf (get_fstn_args (Suc (Suc (length xs))) 
        (length xs) @ [recf.id (Suc (Suc (length xs))) (Suc (length xs))])])))
       (xs @ [w]) =
-       Minr (\<lambda>args. 0 < rec_exec rf args) xs w"
+       Minr (\<lambda>args. 0 < rec_eval rf args) xs w"
 proof(induct w)
   let ?rt = "(recf.id (Suc (length xs)) ((length xs)))"
   let ?rf = "(Cn (Suc (Suc (length xs))) 
@@ -667,11 +667,11 @@
         primerec ?rt (length (xs @ [0]))"
     apply(auto simp: prrf nth_append)+
     done
-  show "Sigma (rec_exec (rec_all ?rt ?rf)) (xs @ [0])
-       = Minr (\<lambda>args. 0 < rec_exec rf args) xs 0"
+  show "Sigma (rec_eval (rec_all ?rt ?rf)) (xs @ [0])
+       = Minr (\<lambda>args. 0 < rec_eval rf args) xs 0"
     apply(simp add: Sigma.simps)
     apply(simp only: prrf all_lemma,  
-          auto simp: rec_exec.simps get_fstn_args_take Minr.simps)
+          auto simp: rec_eval.simps get_fstn_args_take Minr.simps)
     apply(rule_tac Min_eqI, auto)
     done
 next
@@ -684,17 +684,17 @@
     (Suc ((length xs)))])])"
   let ?rq = "(rec_all ?rt ?rf)"
   assume ind:
-    "Sigma (rec_exec (rec_all ?rt ?rf)) (xs @ [w]) = Minr (\<lambda>args. 0 < rec_exec rf args) xs w"
+    "Sigma (rec_eval (rec_all ?rt ?rf)) (xs @ [w]) = Minr (\<lambda>args. 0 < rec_eval rf args) xs w"
   have prrf: "primerec ?rf (Suc (length (xs @ [Suc w]))) \<and>
         primerec ?rt (length (xs @ [Suc w]))"
     apply(auto simp: prrf nth_append)+
     done
-  show "UF.Sigma (rec_exec (rec_all ?rt ?rf))
+  show "UF.Sigma (rec_eval (rec_all ?rt ?rf))
          (xs @ [Suc w]) =
-        Minr (\<lambda>args. 0 < rec_exec rf args) xs (Suc w)"
+        Minr (\<lambda>args. 0 < rec_eval rf args) xs (Suc w)"
     apply(auto simp: Sigma_Suc_simp_rewrite ind Minr_Suc_simp)
     apply(simp_all only: prrf all_lemma)
-    apply(auto simp: rec_exec.simps get_fstn_args_take Let_def Minr.simps split: if_splits)
+    apply(auto simp: rec_eval.simps get_fstn_args_take Let_def Minr.simps split: if_splits)
     apply(drule_tac Min_false1, simp, simp, simp)
     apply(case_tac "x = Suc w", simp, simp)
     apply(drule_tac Min_false1, simp, simp, simp)
@@ -707,7 +707,7 @@
   *}
 lemma Minr_lemma: 
   assumes h: "primerec rf (Suc (length xs))" 
-  shows "rec_exec (rec_Minr rf) (xs @ [w]) = Minr (\<lambda> args. (0 < rec_exec rf args)) xs w"
+  shows "rec_eval (rec_Minr rf) (xs @ [w]) = Minr (\<lambda> args. (0 < rec_eval rf args)) xs w"
 proof -
   let ?rt = "(recf.id (Suc (length xs)) ((length xs)))"
   let ?rf = "(Cn (Suc (Suc (length xs))) 
@@ -722,8 +722,8 @@
     done
   moreover have "arity rf = Suc (length xs)"
     using h by auto
-  ultimately show "rec_exec (rec_Minr rf) (xs @ [w]) = Minr (\<lambda> args. (0 < rec_exec rf args)) xs w"
-    apply(simp add: rec_exec.simps rec_Minr.simps arity.simps Let_def 
+  ultimately show "rec_eval (rec_Minr rf) (xs @ [w]) = Minr (\<lambda> args. (0 < rec_eval rf args)) xs w"
+    apply(simp add: rec_eval.simps rec_Minr.simps arity.simps Let_def 
                     sigma_lemma all_lemma)
     apply(rule_tac  sigma_minr_lemma)
     apply(simp add: h)
@@ -743,8 +743,8 @@
   The correctness of @{text "rec_le"}.
   *}
 lemma le_lemma: 
-  "rec_exec rec_le [x, y] = (if (x \<le> y) then 1 else 0)"
-by(auto simp: rec_le_def rec_exec.simps)
+  "rec_eval rec_le [x, y] = (if (x \<le> y) then 1 else 0)"
+by(auto simp: rec_le_def rec_eval.simps)
 
 text {*
   Definition of @{text "Max[Rr]"} on page 77 of Boolos's book.
@@ -847,7 +847,7 @@
 
 lemma Sigma_Max_lemma: 
   assumes prrf: "primerec rf (Suc (length xs))"
-  shows "UF.Sigma (rec_exec (Cn (Suc (Suc (length xs))) rec_not
+  shows "UF.Sigma (rec_eval (Cn (Suc (Suc (length xs))) rec_not
   [rec_all (recf.id (Suc (Suc (length xs))) (length xs))
   (Cn (Suc (Suc (Suc (length xs)))) rec_disj
   [Cn (Suc (Suc (Suc (length xs)))) rec_le
@@ -858,7 +858,7 @@
   (get_fstn_args (Suc (Suc (Suc (length xs)))) (length xs) @ 
   [recf.id (Suc (Suc (Suc (length xs)))) (Suc (Suc (length xs)))])]])]))
   ((xs @ [w]) @ [w]) =
-       Maxr (\<lambda>args. 0 < rec_exec rf args) xs w"
+       Maxr (\<lambda>args. 0 < rec_eval rf args) xs w"
 proof -
   let ?rt = "(recf.id (Suc (Suc (length xs))) ((length xs)))"
   let ?rf1 = "Cn (Suc (Suc (Suc (length xs))))
@@ -876,7 +876,7 @@
   let ?notrq = "Cn (Suc (Suc (length xs))) rec_not [?rq]"
   show "?thesis"
   proof(auto simp: Maxr.simps)
-    assume h: "\<forall>x\<le>w. rec_exec rf (xs @ [x]) = 0"
+    assume h: "\<forall>x\<le>w. rec_eval rf (xs @ [x]) = 0"
     have "primerec ?rf (Suc (length (xs @ [w, i]))) \<and> 
           primerec ?rt (length (xs @ [w, i]))"
       using prrf
@@ -884,54 +884,54 @@
       apply(case_tac i, auto)
       apply(case_tac ia, auto simp: h nth_append)
       done
-    hence "Sigma (rec_exec ?notrq) ((xs@[w])@[w]) = 0"
+    hence "Sigma (rec_eval ?notrq) ((xs@[w])@[w]) = 0"
       apply(rule_tac Sigma_0)
-      apply(auto simp: rec_exec.simps all_lemma
+      apply(auto simp: rec_eval.simps all_lemma
                        get_fstn_args_take nth_append h)
       done
-    thus "UF.Sigma (rec_exec ?notrq)
+    thus "UF.Sigma (rec_eval ?notrq)
       (xs @ [w, w]) = 0"
       by simp
   next
     fix x
-    assume h: "x \<le> w" "0 < rec_exec rf (xs @ [x])"
-    hence "\<exists> ma. Max {y. y \<le> w \<and> 0 < rec_exec rf (xs @ [y])} = ma"
+    assume h: "x \<le> w" "0 < rec_eval rf (xs @ [x])"
+    hence "\<exists> ma. Max {y. y \<le> w \<and> 0 < rec_eval rf (xs @ [y])} = ma"
       by auto
     from this obtain ma where k1: 
-      "Max {y. y \<le> w \<and> 0 < rec_exec rf (xs @ [y])} = ma" ..
-    hence k2: "ma \<le> w \<and> 0 < rec_exec rf (xs @ [ma])"
+      "Max {y. y \<le> w \<and> 0 < rec_eval rf (xs @ [y])} = ma" ..
+    hence k2: "ma \<le> w \<and> 0 < rec_eval rf (xs @ [ma])"
       using h
       apply(subgoal_tac
-        "Max {y. y \<le> w \<and> 0 < rec_exec rf (xs @ [y])} \<in>  {y. y \<le> w \<and> 0 < rec_exec rf (xs @ [y])}")
+        "Max {y. y \<le> w \<and> 0 < rec_eval rf (xs @ [y])} \<in>  {y. y \<le> w \<and> 0 < rec_eval rf (xs @ [y])}")
       apply(erule_tac CollectE, simp)
       apply(rule_tac Max_in, auto)
       done
-    hence k3: "\<forall> k < ma. (rec_exec ?notrq (xs @ [w, k]) = 1)"
+    hence k3: "\<forall> k < ma. (rec_eval ?notrq (xs @ [w, k]) = 1)"
       apply(auto simp: nth_append)
       apply(subgoal_tac "primerec ?rf (Suc (length (xs @ [w, k]))) \<and> 
         primerec ?rt (length (xs @ [w, k]))")
-      apply(auto simp: rec_exec.simps all_lemma get_fstn_args_take nth_append)
+      apply(auto simp: rec_eval.simps all_lemma get_fstn_args_take nth_append)
       using prrf
       apply(case_tac i, auto)
       apply(case_tac ia, auto simp: h nth_append)
       done    
-    have k4: "\<forall> k \<ge> ma. (rec_exec ?notrq (xs @ [w, k]) = 0)"
+    have k4: "\<forall> k \<ge> ma. (rec_eval ?notrq (xs @ [w, k]) = 0)"
       apply(auto)
       apply(subgoal_tac "primerec ?rf (Suc (length (xs @ [w, k]))) \<and> 
         primerec ?rt (length (xs @ [w, k]))")
-      apply(auto simp: rec_exec.simps all_lemma get_fstn_args_take nth_append)
-      apply(subgoal_tac "x \<le> Max {y. y \<le> w \<and> 0 < rec_exec rf (xs @ [y])}",
+      apply(auto simp: rec_eval.simps all_lemma get_fstn_args_take nth_append)
+      apply(subgoal_tac "x \<le> Max {y. y \<le> w \<and> 0 < rec_eval rf (xs @ [y])}",
         simp add: k1)
       apply(rule_tac Max_ge, auto)
       using prrf
       apply(case_tac i, auto)
       apply(case_tac ia, auto simp: h nth_append)
       done 
-    from k3 k4 k1 have "Sigma (rec_exec ?notrq) ((xs @ [w]) @ [w]) = ma"
+    from k3 k4 k1 have "Sigma (rec_eval ?notrq) ((xs @ [w]) @ [w]) = ma"
       apply(rule_tac Sigma_max_point, simp, simp, simp add: k2)
       done
-    from k1 and this show "Sigma (rec_exec ?notrq) (xs @ [w, w]) =
-      Max {y. y \<le> w \<and> 0 < rec_exec rf (xs @ [y])}"
+    from k1 and this show "Sigma (rec_eval ?notrq) (xs @ [w, w]) =
+      Max {y. y \<le> w \<and> 0 < rec_eval rf (xs @ [y])}"
       by simp
   qed  
 qed
@@ -941,13 +941,13 @@
   *}
 lemma Maxr_lemma:
  assumes h: "primerec rf (Suc (length xs))"
- shows   "rec_exec (rec_maxr rf) (xs @ [w]) = 
-            Maxr (\<lambda> args. 0 < rec_exec rf args) xs w"
+ shows   "rec_eval (rec_maxr rf) (xs @ [w]) = 
+            Maxr (\<lambda> args. 0 < rec_eval rf args) xs w"
 proof -
   from h have "arity rf = Suc (length xs)"
     by auto
   thus "?thesis"
-  proof(simp add: rec_exec.simps rec_maxr.simps nth_append get_fstn_args_take)
+  proof(simp add: rec_eval.simps rec_maxr.simps nth_append get_fstn_args_take)
     let ?rt = "(recf.id (Suc (Suc (length xs))) ((length xs)))"
     let ?rf1 = "Cn (Suc (Suc (Suc (length xs))))
                      rec_le [recf.id (Suc (Suc (Suc (length xs)))) 
@@ -976,17 +976,17 @@
       by(erule_tac primerec_all_iff, auto)
     hence prnotrp: "primerec ?notrq (Suc (length ((xs @ [w]))))"
       by(rule_tac prime_cn, auto)
-    have g1: "rec_exec (rec_sigma ?notrq) ((xs @ [w]) @ [w]) 
-      = Maxr (\<lambda>args. 0 < rec_exec rf args) xs w"
+    have g1: "rec_eval (rec_sigma ?notrq) ((xs @ [w]) @ [w]) 
+      = Maxr (\<lambda>args. 0 < rec_eval rf args) xs w"
       using prnotrp
       using sigma_lemma
       apply(simp only: sigma_lemma)
       apply(rule_tac Sigma_Max_lemma)
       apply(simp add: h)
       done
-    thus "rec_exec (rec_sigma ?notrq)
+    thus "rec_eval (rec_sigma ?notrq)
      (xs @ [w, w]) =
-    Maxr (\<lambda>args. 0 < rec_exec rf args) xs w"
+    Maxr (\<lambda>args. 0 < rec_eval rf args) xs w"
       apply(simp)
       done
   qed
@@ -1042,8 +1042,8 @@
   The correctness of @{text "rec_noteq"}.
   *}
 lemma noteq_lemma: 
-  "rec_exec rec_noteq [x, y] = (if x \<noteq> y then 1 else 0)"
-by(simp add: rec_exec.simps rec_noteq_def)
+  "rec_eval rec_noteq [x, y] = (if x \<noteq> y then 1 else 0)"
+by(simp add: rec_eval.simps rec_noteq_def)
 
 declare noteq_lemma[simp]
 
@@ -1079,8 +1079,8 @@
 done
 
 
-lemma quo_lemma1: "rec_exec rec_quo [x, y] = quo [x, y]"
-proof(simp add: rec_exec.simps rec_quo_def)
+lemma quo_lemma1: "rec_eval rec_quo [x, y] = quo [x, y]"
+proof(simp add: rec_eval.simps rec_quo_def)
   let ?rR = "(Cn (Suc (Suc (Suc 0))) rec_conj
                [Cn (Suc (Suc (Suc 0))) rec_le
                    [Cn (Suc (Suc (Suc 0))) rec_mult 
@@ -1091,7 +1091,7 @@
                               [recf.id (Suc (Suc (Suc 0))) 
              (Suc (0)), Cn (Suc (Suc (Suc 0))) (constn 0) 
                       [recf.id (Suc (Suc (Suc 0))) (0)]]])"
-  have "rec_exec (rec_maxr ?rR) ([x, y]@ [ x]) = Maxr (\<lambda> args. 0 < rec_exec ?rR args) [x, y] x"
+  have "rec_eval (rec_maxr ?rR) ([x, y]@ [ x]) = Maxr (\<lambda> args. 0 < rec_eval ?rR args) [x, y] x"
   proof(rule_tac Maxr_lemma, simp)
     show "primerec ?rR (Suc (Suc (Suc 0)))"
       apply(auto)
@@ -1100,24 +1100,24 @@
       apply(case_tac i, auto)
       done
   qed
-  hence g1: "rec_exec (rec_maxr ?rR) ([x, y,  x]) =
-             Maxr (\<lambda> args. if rec_exec ?rR args = 0 then False
+  hence g1: "rec_eval (rec_maxr ?rR) ([x, y,  x]) =
+             Maxr (\<lambda> args. if rec_eval ?rR args = 0 then False
                            else True) [x, y] x" 
     by simp
-  have g2: "Maxr (\<lambda> args. if rec_exec ?rR args = 0 then False
+  have g2: "Maxr (\<lambda> args. if rec_eval ?rR args = 0 then False
                            else True) [x, y] x = quo [x, y]"
-    apply(simp add: rec_exec.simps)
+    apply(simp add: rec_eval.simps)
     apply(simp add: Maxr.simps quo.simps, auto)
     done
   from g1 and g2 show 
-    "rec_exec (rec_maxr ?rR) ([x, y,  x]) = quo [x, y]"
+    "rec_eval (rec_maxr ?rR) ([x, y,  x]) = quo [x, y]"
     by simp
 qed
 
 text {*
   The correctness of @{text "quo"}.
   *}
-lemma quo_lemma2: "rec_exec rec_quo [x, y] = x div y"
+lemma quo_lemma2: "rec_eval rec_quo [x, y] = x div y"
   using quo_lemma1[of x y] quo_div[of x y]
   by simp
  
@@ -1134,8 +1134,8 @@
 text {*
   The correctness of @{text "rec_mod"}:
   *}
-lemma mod_lemma: "rec_exec rec_mod [x, y] = (x mod y)"
-proof(simp add: rec_exec.simps rec_mod_def quo_lemma2)
+lemma mod_lemma: "rec_eval rec_mod [x, y] = (x mod y)"
+proof(simp add: rec_eval.simps rec_mod_def quo_lemma2)
   fix x y
   show "x - x div y * y = x mod (y::nat)"
     using mod_div_equality2[of y x]
@@ -1178,56 +1178,56 @@
 declare Embranch.simps[simp del] rec_embranch.simps[simp del]
 
 lemma embranch_all0: 
-  "\<lbrakk>\<forall> j < length rcs. rec_exec (rcs ! j) xs = 0;
+  "\<lbrakk>\<forall> j < length rcs. rec_eval (rcs ! j) xs = 0;
     length rgs = length rcs;  
   rcs \<noteq> []; 
   list_all (\<lambda> rf. primerec rf (length xs)) (rgs @ rcs)\<rbrakk>  \<Longrightarrow> 
-  rec_exec (rec_embranch (zip rgs rcs)) xs = 0"
+  rec_eval (rec_embranch (zip rgs rcs)) xs = 0"
 proof(induct rcs arbitrary: rgs, simp, case_tac rgs, simp)
   fix a rcs rgs aa list
   assume ind: 
-    "\<And>rgs. \<lbrakk>\<forall>j<length rcs. rec_exec (rcs ! j) xs = 0; 
+    "\<And>rgs. \<lbrakk>\<forall>j<length rcs. rec_eval (rcs ! j) xs = 0; 
              length rgs = length rcs; rcs \<noteq> []; 
             list_all (\<lambda>rf. primerec rf (length xs)) (rgs @ rcs)\<rbrakk> \<Longrightarrow> 
-                      rec_exec (rec_embranch (zip rgs rcs)) xs = 0"
-  and h:  "\<forall>j<length (a # rcs). rec_exec ((a # rcs) ! j) xs = 0"
+                      rec_eval (rec_embranch (zip rgs rcs)) xs = 0"
+  and h:  "\<forall>j<length (a # rcs). rec_eval ((a # rcs) ! j) xs = 0"
   "length rgs = length (a # rcs)" 
     "a # rcs \<noteq> []" 
     "list_all (\<lambda>rf. primerec rf (length xs)) (rgs @ a # rcs)"
     "rgs = aa # list"
-  have g: "rcs \<noteq> [] \<Longrightarrow> rec_exec (rec_embranch (zip list rcs)) xs = 0"
+  have g: "rcs \<noteq> [] \<Longrightarrow> rec_eval (rec_embranch (zip list rcs)) xs = 0"
     using h
     by(rule_tac ind, auto)
-  show "rec_exec (rec_embranch (zip rgs (a # rcs))) xs = 0"
+  show "rec_eval (rec_embranch (zip rgs (a # rcs))) xs = 0"
   proof(case_tac "rcs = []", simp)
-    show "rec_exec (rec_embranch (zip rgs [a])) xs = 0"
+    show "rec_eval (rec_embranch (zip rgs [a])) xs = 0"
       using h
-      apply(simp add: rec_embranch.simps rec_exec.simps)
+      apply(simp add: rec_embranch.simps rec_eval.simps)
       apply(erule_tac x = 0 in allE, simp)
       done
   next
     assume "rcs \<noteq> []"
-    hence "rec_exec (rec_embranch (zip list rcs)) xs = 0"
+    hence "rec_eval (rec_embranch (zip list rcs)) xs = 0"
       using g by simp
-    thus "rec_exec (rec_embranch (zip rgs (a # rcs))) xs = 0"
+    thus "rec_eval (rec_embranch (zip rgs (a # rcs))) xs = 0"
       using h
-      apply(simp add: rec_embranch.simps rec_exec.simps)
+      apply(simp add: rec_embranch.simps rec_eval.simps)
       apply(case_tac rcs,
-        auto simp: rec_exec.simps rec_embranch.simps)
+        auto simp: rec_eval.simps rec_embranch.simps)
       apply(case_tac list,
-        auto simp: rec_exec.simps rec_embranch.simps)
+        auto simp: rec_eval.simps rec_embranch.simps)
       done
   qed
 qed     
  
 
-lemma embranch_exec_0: "\<lbrakk>rec_exec aa xs = 0; zip rgs list \<noteq> []; 
+lemma embranch_exec_0: "\<lbrakk>rec_eval aa xs = 0; zip rgs list \<noteq> []; 
        list_all (\<lambda> rf. primerec rf (length xs)) ([a, aa] @ rgs @ list)\<rbrakk>
-       \<Longrightarrow> rec_exec (rec_embranch ((a, aa) # zip rgs list)) xs
-         = rec_exec (rec_embranch (zip rgs list)) xs"
-apply(simp add: rec_exec.simps rec_embranch.simps)
+       \<Longrightarrow> rec_eval (rec_embranch ((a, aa) # zip rgs list)) xs
+         = rec_eval (rec_embranch (zip rgs list)) xs"
+apply(simp add: rec_eval.simps rec_embranch.simps)
 apply(case_tac "zip rgs list", simp, case_tac ab, 
-  simp add: rec_embranch.simps rec_exec.simps)
+  simp add: rec_embranch.simps rec_eval.simps)
 apply(subgoal_tac "arity a = length xs", auto)
 apply(subgoal_tac "arity aaa = length xs", auto)
 apply(case_tac rgs, simp, case_tac list, simp, simp)
@@ -1244,18 +1244,18 @@
 
 lemma Embranch_0:  
   "\<lbrakk>length rgs = k; length rcs = k; k > 0; 
-  \<forall> j < k. rec_exec (rcs ! j) xs = 0\<rbrakk> \<Longrightarrow>
-  Embranch (zip (map rec_exec rgs) (map (\<lambda>r args. 0 < rec_exec r args) rcs)) xs = 0"
+  \<forall> j < k. rec_eval (rcs ! j) xs = 0\<rbrakk> \<Longrightarrow>
+  Embranch (zip (map rec_eval rgs) (map (\<lambda>r args. 0 < rec_eval r args) rcs)) xs = 0"
 proof(induct rgs arbitrary: rcs k, simp, simp)
   fix a rgs rcs k
   assume ind: 
-    "\<And>rcs k. \<lbrakk>length rgs = k; length rcs = k; 0 < k; \<forall>j<k. rec_exec (rcs ! j) xs = 0\<rbrakk> 
-    \<Longrightarrow> Embranch (zip (map rec_exec rgs) (map (\<lambda>r args. 0 < rec_exec r args) rcs)) xs = 0"
+    "\<And>rcs k. \<lbrakk>length rgs = k; length rcs = k; 0 < k; \<forall>j<k. rec_eval (rcs ! j) xs = 0\<rbrakk> 
+    \<Longrightarrow> Embranch (zip (map rec_eval rgs) (map (\<lambda>r args. 0 < rec_eval r args) rcs)) xs = 0"
   and h: "Suc (length rgs) = k" "length rcs = k"
-    "\<forall>j<k. rec_exec (rcs ! j) xs = 0"
+    "\<forall>j<k. rec_eval (rcs ! j) xs = 0"
   from h show  
-    "Embranch (zip (rec_exec a # map rec_exec rgs) 
-           (map (\<lambda>r args. 0 < rec_exec r args) rcs)) xs = 0"
+    "Embranch (zip (rec_eval a # map rec_eval rgs) 
+           (map (\<lambda>r args. 0 < rec_eval r args) rcs)) xs = 0"
     apply(case_tac rcs, simp, case_tac "rgs = []", simp)
     apply(simp add: Embranch.simps)
     apply(erule_tac x = 0 in allE, simp)
@@ -1273,51 +1273,51 @@
   assumes branch_num:
   "length rgs = n" "length rcs = n" "n > 0"
   and partition: 
-  "(\<exists> i < n. (rec_exec (rcs ! i) xs = 1 \<and> (\<forall> j < n. j \<noteq> i \<longrightarrow> 
-                                      rec_exec (rcs ! j) xs = 0)))"
+  "(\<exists> i < n. (rec_eval (rcs ! i) xs = 1 \<and> (\<forall> j < n. j \<noteq> i \<longrightarrow> 
+                                      rec_eval (rcs ! j) xs = 0)))"
   and prime_all: "list_all (\<lambda> rf. primerec rf (length xs)) (rgs @ rcs)"
-  shows "rec_exec (rec_embranch (zip rgs rcs)) xs =
-                  Embranch (zip (map rec_exec rgs) 
-                     (map (\<lambda> r args. 0 < rec_exec r args) rcs)) xs"
+  shows "rec_eval (rec_embranch (zip rgs rcs)) xs =
+                  Embranch (zip (map rec_eval rgs) 
+                     (map (\<lambda> r args. 0 < rec_eval r args) rcs)) xs"
   using branch_num partition prime_all
 proof(induct rgs arbitrary: rcs n, simp)
   fix a rgs rcs n
   assume ind: 
     "\<And>rcs n. \<lbrakk>length rgs = n; length rcs = n; 0 < n;
-    \<exists>i<n. rec_exec (rcs ! i) xs = 1 \<and> (\<forall>j<n. j \<noteq> i \<longrightarrow> rec_exec (rcs ! j) xs = 0);
+    \<exists>i<n. rec_eval (rcs ! i) xs = 1 \<and> (\<forall>j<n. j \<noteq> i \<longrightarrow> rec_eval (rcs ! j) xs = 0);
     list_all (\<lambda>rf. primerec rf (length xs)) (rgs @ rcs)\<rbrakk>
-    \<Longrightarrow> rec_exec (rec_embranch (zip rgs rcs)) xs =
-    Embranch (zip (map rec_exec rgs) (map (\<lambda>r args. 0 < rec_exec r args) rcs)) xs"
+    \<Longrightarrow> rec_eval (rec_embranch (zip rgs rcs)) xs =
+    Embranch (zip (map rec_eval rgs) (map (\<lambda>r args. 0 < rec_eval r args) rcs)) xs"
   and h: "length (a # rgs) = n" "length (rcs::recf list) = n" "0 < n"
-         " \<exists>i<n. rec_exec (rcs ! i) xs = 1 \<and> 
-         (\<forall>j<n. j \<noteq> i \<longrightarrow> rec_exec (rcs ! j) xs = 0)" 
+         " \<exists>i<n. rec_eval (rcs ! i) xs = 1 \<and> 
+         (\<forall>j<n. j \<noteq> i \<longrightarrow> rec_eval (rcs ! j) xs = 0)" 
     "list_all (\<lambda>rf. primerec rf (length xs)) ((a # rgs) @ rcs)"
-  from h show "rec_exec (rec_embranch (zip (a # rgs) rcs)) xs =
-    Embranch (zip (map rec_exec (a # rgs)) (map (\<lambda>r args. 
-                0 < rec_exec r args) rcs)) xs"
+  from h show "rec_eval (rec_embranch (zip (a # rgs) rcs)) xs =
+    Embranch (zip (map rec_eval (a # rgs)) (map (\<lambda>r args. 
+                0 < rec_eval r args) rcs)) xs"
     apply(case_tac rcs, simp, simp)
-    apply(case_tac "rec_exec aa xs = 0")
+    apply(case_tac "rec_eval aa xs = 0")
     apply(case_tac [!] "zip rgs list = []", simp)
-    apply(subgoal_tac "rgs = [] \<and> list = []", simp add: Embranch.simps rec_exec.simps rec_embranch.simps)
+    apply(subgoal_tac "rgs = [] \<and> list = []", simp add: Embranch.simps rec_eval.simps rec_embranch.simps)
     apply(rule_tac  zip_null_iff, simp, simp, simp)
   proof -
     fix aa list
     assume g:
       "Suc (length rgs) = n" "Suc (length list) = n" 
-      "\<exists>i<n. rec_exec ((aa # list) ! i) xs = Suc 0 \<and> 
-          (\<forall>j<n. j \<noteq> i \<longrightarrow> rec_exec ((aa # list) ! j) xs = 0)"
+      "\<exists>i<n. rec_eval ((aa # list) ! i) xs = Suc 0 \<and> 
+          (\<forall>j<n. j \<noteq> i \<longrightarrow> rec_eval ((aa # list) ! j) xs = 0)"
       "primerec a (length xs) \<and> 
       list_all (\<lambda>rf. primerec rf (length xs)) rgs \<and>
       primerec aa (length xs) \<and> 
       list_all (\<lambda>rf. primerec rf (length xs)) list"
-      "rec_exec aa xs = 0" "rcs = aa # list" "zip rgs list \<noteq> []"
-    have "rec_exec (rec_embranch ((a, aa) # zip rgs list)) xs
-        = rec_exec (rec_embranch (zip rgs list)) xs"
+      "rec_eval aa xs = 0" "rcs = aa # list" "zip rgs list \<noteq> []"
+    have "rec_eval (rec_embranch ((a, aa) # zip rgs list)) xs
+        = rec_eval (rec_embranch (zip rgs list)) xs"
       apply(rule embranch_exec_0, simp_all add: g)
       done
-    from g and this show "rec_exec (rec_embranch ((a, aa) # zip rgs list)) xs =
-         Embranch ((rec_exec a, \<lambda>args. 0 < rec_exec aa args) # 
-           zip (map rec_exec rgs) (map (\<lambda>r args. 0 < rec_exec r args) list)) xs"
+    from g and this show "rec_eval (rec_embranch ((a, aa) # zip rgs list)) xs =
+         Embranch ((rec_eval a, \<lambda>args. 0 < rec_eval aa args) # 
+           zip (map rec_eval rgs) (map (\<lambda>r args. 0 < rec_eval r args) list)) xs"
       apply(simp add: Embranch.simps)
       apply(rule_tac n = "n - Suc 0" in ind)
       apply(case_tac n, simp, simp)
@@ -1331,32 +1331,32 @@
   next
     fix aa list
     assume g: "Suc (length rgs) = n" "Suc (length list) = n"
-      "\<exists>i<n. rec_exec ((aa # list) ! i) xs = Suc 0 \<and> 
-      (\<forall>j<n. j \<noteq> i \<longrightarrow> rec_exec ((aa # list) ! j) xs = 0)"
+      "\<exists>i<n. rec_eval ((aa # list) ! i) xs = Suc 0 \<and> 
+      (\<forall>j<n. j \<noteq> i \<longrightarrow> rec_eval ((aa # list) ! j) xs = 0)"
       "primerec a (length xs) \<and> list_all (\<lambda>rf. primerec rf (length xs)) rgs \<and>
       primerec aa (length xs) \<and> list_all (\<lambda>rf. primerec rf (length xs)) list"
-    "rcs = aa # list" "rec_exec aa xs \<noteq> 0" "zip rgs list = []"
-    thus "rec_exec (rec_embranch ((a, aa) # zip rgs list)) xs = 
-        Embranch ((rec_exec a, \<lambda>args. 0 < rec_exec aa args) # 
-       zip (map rec_exec rgs) (map (\<lambda>r args. 0 < rec_exec r args) list)) xs"
+    "rcs = aa # list" "rec_eval aa xs \<noteq> 0" "zip rgs list = []"
+    thus "rec_eval (rec_embranch ((a, aa) # zip rgs list)) xs = 
+        Embranch ((rec_eval a, \<lambda>args. 0 < rec_eval aa args) # 
+       zip (map rec_eval rgs) (map (\<lambda>r args. 0 < rec_eval r args) list)) xs"
       apply(subgoal_tac "rgs = [] \<and> list = []", simp)
       prefer 2
       apply(rule_tac zip_null_iff, simp, simp, simp)
-      apply(simp add: rec_exec.simps rec_embranch.simps Embranch.simps, auto)
+      apply(simp add: rec_eval.simps rec_embranch.simps Embranch.simps, auto)
       done
   next
     fix aa list
     assume g: "Suc (length rgs) = n" "Suc (length list) = n"
-      "\<exists>i<n. rec_exec ((aa # list) ! i) xs = Suc 0 \<and>  
-           (\<forall>j<n. j \<noteq> i \<longrightarrow> rec_exec ((aa # list) ! j) xs = 0)"
+      "\<exists>i<n. rec_eval ((aa # list) ! i) xs = Suc 0 \<and>  
+           (\<forall>j<n. j \<noteq> i \<longrightarrow> rec_eval ((aa # list) ! j) xs = 0)"
       "primerec a (length xs) \<and> list_all (\<lambda>rf. primerec rf (length xs)) rgs
       \<and> primerec aa (length xs) \<and> list_all (\<lambda>rf. primerec rf (length xs)) list"
-      "rcs = aa # list" "rec_exec aa xs \<noteq> 0" "zip rgs list \<noteq> []"
-    have "rec_exec aa xs =  Suc 0"
+      "rcs = aa # list" "rec_eval aa xs \<noteq> 0" "zip rgs list \<noteq> []"
+    have "rec_eval aa xs =  Suc 0"
       using g
-      apply(case_tac "rec_exec aa xs", simp, auto)
+      apply(case_tac "rec_eval aa xs", simp, auto)
       done      
-    moreover have "rec_exec (rec_embranch' (zip rgs list) (length xs)) xs = 0"
+    moreover have "rec_eval (rec_embranch' (zip rgs list) (length xs)) xs = 0"
     proof -
       have "rec_embranch' (zip rgs list) (length xs) = rec_embranch (zip rgs list)"
         using g
@@ -1365,9 +1365,9 @@
         apply(subgoal_tac "arity aaa = length xs", simp, auto)
         apply(case_tac rgs, simp, simp, case_tac list, simp, simp)
         done
-      moreover have "rec_exec (rec_embranch (zip rgs list)) xs = 0"
+      moreover have "rec_eval (rec_embranch (zip rgs list)) xs = 0"
       proof(rule embranch_all0)
-        show " \<forall>j<length list. rec_exec (list ! j) xs = 0"
+        show " \<forall>j<length list. rec_eval (list ! j) xs = 0"
           using g
           apply(auto)
           apply(case_tac i, simp)
@@ -1391,12 +1391,12 @@
           apply auto
           done
       qed
-      ultimately show "rec_exec (rec_embranch' (zip rgs list) (length xs)) xs = 0"
+      ultimately show "rec_eval (rec_embranch' (zip rgs list) (length xs)) xs = 0"
         by simp
     qed
     moreover have 
-      "Embranch (zip (map rec_exec rgs) 
-          (map (\<lambda>r args. 0 < rec_exec r args) list)) xs = 0"
+      "Embranch (zip (map rec_eval rgs) 
+          (map (\<lambda>r args. 0 < rec_eval r args) list)) xs = 0"
       using g
       apply(rule_tac k = "length rgs" in Embranch_0)
       apply(simp, case_tac n, simp, simp)
@@ -1411,10 +1411,10 @@
       using g
       apply(auto)
       done
-    ultimately show "rec_exec (rec_embranch ((a, aa) # zip rgs list)) xs = 
-      Embranch ((rec_exec a, \<lambda>args. 0 < rec_exec aa args) #
-           zip (map rec_exec rgs) (map (\<lambda>r args. 0 < rec_exec r args) list)) xs"
-      apply(simp add: rec_exec.simps rec_embranch.simps Embranch.simps)
+    ultimately show "rec_eval (rec_embranch ((a, aa) # zip rgs list)) xs = 
+      Embranch ((rec_eval a, \<lambda>args. 0 < rec_eval aa args) #
+           zip (map rec_eval rgs) (map (\<lambda>r args. 0 < rec_eval r args) list)) xs"
+      apply(simp add: rec_eval.simps rec_embranch.simps Embranch.simps)
       done
   qed
 qed
@@ -1444,10 +1444,10 @@
 declare numeral_2_eq_2[simp del] numeral_3_eq_3[simp del]
 
 lemma exec_tmp: 
-  "rec_exec (rec_all (Cn 2 rec_minus [recf.id 2 0, Cn 2 (constn (Suc 0)) [recf.id 2 0]]) 
+  "rec_eval (rec_all (Cn 2 rec_minus [recf.id 2 0, Cn 2 (constn (Suc 0)) [recf.id 2 0]]) 
   (Cn 3 rec_noteq [Cn 3 rec_mult [recf.id 3 (Suc 0), recf.id 3 2], recf.id 3 0]))  [x, k] = 
-  ((if (\<forall>w\<le>rec_exec (Cn 2 rec_minus [recf.id 2 0, Cn 2 (constn (Suc 0)) [recf.id 2 0]]) ([x, k]). 
-  0 < rec_exec (Cn 3 rec_noteq [Cn 3 rec_mult [recf.id 3 (Suc 0), recf.id 3 2], recf.id 3 0])
+  ((if (\<forall>w\<le>rec_eval (Cn 2 rec_minus [recf.id 2 0, Cn 2 (constn (Suc 0)) [recf.id 2 0]]) ([x, k]). 
+  0 < rec_eval (Cn 3 rec_noteq [Cn 3 rec_mult [recf.id 3 (Suc 0), recf.id 3 2], recf.id 3 0])
   ([x, k] @ [w])) then 1 else 0))"
 apply(rule_tac all_lemma)
 apply(auto)
@@ -1458,8 +1458,8 @@
 text {*
   The correctness of @{text "Prime"}.
   *}
-lemma prime_lemma: "rec_exec rec_prime [x] = (if prime x then 1 else 0)"
-proof(simp add: rec_exec.simps rec_prime_def)
+lemma prime_lemma: "rec_eval rec_prime [x] = (if prime x then 1 else 0)"
+proof(simp add: rec_eval.simps rec_prime_def)
   let ?rt1 = "(Cn 2 rec_minus [recf.id 2 0, 
     Cn 2 (constn (Suc 0)) [recf.id 2 0]])"
   let ?rf1 = "(Cn 3 rec_noteq [Cn 3 rec_mult 
@@ -1467,8 +1467,8 @@
   let ?rt2 = "(Cn (Suc 0) rec_minus 
     [recf.id (Suc 0) 0, constn (Suc 0)])"
   let ?rf2 = "rec_all ?rt1 ?rf1"
-  have h1: "rec_exec (rec_all ?rt2 ?rf2) ([x]) = 
-        (if (\<forall>k\<le>rec_exec ?rt2 ([x]). 0 < rec_exec ?rf2 ([x] @ [k])) then 1 else 0)"
+  have h1: "rec_eval (rec_all ?rt2 ?rf2) ([x]) = 
+        (if (\<forall>k\<le>rec_eval ?rt2 ([x]). 0 < rec_eval ?rf2 ([x] @ [k])) then 1 else 0)"
   proof(rule_tac all_lemma, simp_all)
     show "primerec ?rf2 (Suc (Suc 0))"
       apply(rule_tac primerec_all_iff)
@@ -1484,18 +1484,18 @@
       done
   qed
   from h1 show 
-   "(Suc 0 < x \<longrightarrow>  (rec_exec (rec_all ?rt2 ?rf2) [x] = 0 \<longrightarrow> 
+   "(Suc 0 < x \<longrightarrow>  (rec_eval (rec_all ?rt2 ?rf2) [x] = 0 \<longrightarrow> 
     \<not> prime x) \<and>
-     (0 < rec_exec (rec_all ?rt2 ?rf2) [x] \<longrightarrow> prime x)) \<and>
-    (\<not> Suc 0 < x \<longrightarrow> \<not> prime x \<and> (rec_exec (rec_all ?rt2 ?rf2) [x] = 0
+     (0 < rec_eval (rec_all ?rt2 ?rf2) [x] \<longrightarrow> prime x)) \<and>
+    (\<not> Suc 0 < x \<longrightarrow> \<not> prime x \<and> (rec_eval (rec_all ?rt2 ?rf2) [x] = 0
     \<longrightarrow> \<not> prime x))"
-    apply(auto simp:rec_exec.simps)
-    apply(simp add: exec_tmp rec_exec.simps)
+    apply(auto simp:rec_eval.simps)
+    apply(simp add: exec_tmp rec_eval.simps)
   proof -
     assume "\<forall>k\<le>x - Suc 0. (0::nat) < (if \<forall>w\<le>x - Suc 0. 
            0 < (if k * w \<noteq> x then 1 else (0 :: nat)) then 1 else 0)" "Suc 0 < x"
     thus "prime x"
-      apply(simp add: rec_exec.simps split: if_splits)
+      apply(simp add: rec_eval.simps split: if_splits)
       apply(simp add: prime_nat_def dvd_def, auto)
       apply(erule_tac x = m in allE, auto)
       apply(case_tac m, simp, case_tac nat, simp, simp)
@@ -1507,16 +1507,16 @@
       by (simp add: prime_nat_def)
   next
     fix k
-    assume "rec_exec (rec_all ?rt1 ?rf1)
+    assume "rec_eval (rec_all ?rt1 ?rf1)
       [x, k] = 0" "k \<le> x - Suc 0" "prime x"
     thus "False"
-      by (auto simp add: exec_tmp rec_exec.simps prime_nat_def dvd_def split: if_splits)
+      by (auto simp add: exec_tmp rec_eval.simps prime_nat_def dvd_def split: if_splits)
   next
     fix k
-    assume "rec_exec (rec_all ?rt1 ?rf1)
+    assume "rec_eval (rec_all ?rt1 ?rf1)
       [x, k] = 0" "k \<le> x - Suc 0" "prime x"
     thus "False"
-      by(auto simp add: exec_tmp rec_exec.simps prime_nat_def dvd_def split: if_splits)
+      by(auto simp add: exec_tmp rec_eval.simps prime_nat_def dvd_def split: if_splits)
   qed
 qed
 
@@ -1539,26 +1539,26 @@
   "fac 0 = 1" |
   "fac (Suc x) = (Suc x) * fac x"
 
-lemma [simp]: "rec_exec rec_dummyfac [0, 0] = Suc 0"
-by(simp add: rec_dummyfac_def rec_exec.simps)
+lemma [simp]: "rec_eval rec_dummyfac [0, 0] = Suc 0"
+by(simp add: rec_dummyfac_def rec_eval.simps)
 
 lemma rec_cn_simp: 
-  "rec_exec (Cn n f gs) xs = (let rgs = map (\<lambda> g. rec_exec g xs) gs in rec_exec f rgs)"
-by(simp add: rec_exec.simps)
-
-lemma rec_id_simp: "rec_exec (id m n) xs = xs ! n" 
-  by(simp add: rec_exec.simps)
-
-lemma fac_dummy: "rec_exec rec_dummyfac [x, y] = y !"
+  "rec_eval (Cn n f gs) xs = (let rgs = map (\<lambda> g. rec_eval g xs) gs in rec_eval f rgs)"
+by(simp add: rec_eval.simps)
+
+lemma rec_id_simp: "rec_eval (id m n) xs = xs ! n" 
+  by(simp add: rec_eval.simps)
+
+lemma fac_dummy: "rec_eval rec_dummyfac [x, y] = y !"
 apply(induct y)
-apply(auto simp: rec_dummyfac_def rec_exec.simps)
+apply(auto simp: rec_dummyfac_def rec_eval.simps)
 done
 
 text {*
   The correctness of @{text "rec_fac"}.
   *}
-lemma fac_lemma: "rec_exec rec_fac [x] =  x!"
-apply(simp add: rec_fac_def rec_exec.simps fac_dummy)
+lemma fac_lemma: "rec_eval rec_fac [x] =  x!"
+apply(simp add: rec_fac_def rec_eval.simps fac_dummy)
 done
 
 declare fac.simps[simp del]
@@ -1686,25 +1686,25 @@
 text {*
   The correctness of @{text "rec_np"}.
   *}
-lemma np_lemma: "rec_exec rec_np [x] = Np x"
-proof(auto simp: rec_np_def rec_exec.simps Let_def fac_lemma)
+lemma np_lemma: "rec_eval rec_np [x] = Np x"
+proof(auto simp: rec_np_def rec_eval.simps Let_def fac_lemma)
   let ?rr = "(Cn 2 rec_conj [Cn 2 rec_less [recf.id 2 0,
     recf.id 2 (Suc 0)], Cn 2 rec_prime [recf.id 2 (Suc 0)]])"
   let ?R = "\<lambda> zs. zs ! 0 < zs ! 1 \<and> prime (zs ! 1)"
-  have g1: "rec_exec (rec_Minr ?rr) ([x] @ [Suc (x!)]) = 
-    Minr (\<lambda> args. 0 < rec_exec ?rr args) [x] (Suc (x!))"
-    by(rule_tac Minr_lemma, auto simp: rec_exec.simps
+  have g1: "rec_eval (rec_Minr ?rr) ([x] @ [Suc (x!)]) = 
+    Minr (\<lambda> args. 0 < rec_eval ?rr args) [x] (Suc (x!))"
+    by(rule_tac Minr_lemma, auto simp: rec_eval.simps
       prime_lemma, auto simp:  numeral_2_eq_2 numeral_3_eq_3)
-  have g2: "Minr (\<lambda> args. 0 < rec_exec ?rr args) [x] (Suc (x!)) = Np x"
+  have g2: "Minr (\<lambda> args. 0 < rec_eval ?rr args) [x] (Suc (x!)) = Np x"
     using prime_ex[of x]
-    apply(auto simp: Minr.simps Np.simps rec_exec.simps)
+    apply(auto simp: Minr.simps Np.simps rec_eval.simps)
     apply(erule_tac x = p in allE, simp add: prime_lemma)
     apply(simp add: prime_lemma split: if_splits)
     apply(subgoal_tac
    "{uu. (prime uu \<longrightarrow> (x < uu \<longrightarrow> uu \<le> Suc (x!)) \<and> x < uu) \<and> prime uu}
     = {y. y \<le> Suc (x!) \<and> x < y \<and> prime y}", auto)
     done
-  from g1 and g2 show "rec_exec (rec_Minr ?rr) ([x, Suc (x!)]) = Np x"
+  from g1 and g2 show "rec_eval (rec_Minr ?rr) ([x, Suc (x!)]) = Np x"
     by simp
 qed
 
@@ -1719,8 +1719,8 @@
 text {*
   The correctness of @{text "rec_power"}.
   *}
-lemma power_lemma: "rec_exec rec_power [x, y] = x^y"
-  by(induct y, auto simp: rec_exec.simps rec_power_def)
+lemma power_lemma: "rec_eval rec_power [x, y] = x^y"
+  by(induct y, auto simp: rec_eval.simps rec_power_def)
 
 text{*
   @{text "Pi k"} returns the @{text "k"}-th prime number.
@@ -1742,15 +1742,15 @@
   where
   "rec_pi = Cn 1 rec_dummy_pi [id 1 0, id 1 0]"
 
-lemma pi_dummy_lemma: "rec_exec rec_dummy_pi [x, y] = Pi y"
+lemma pi_dummy_lemma: "rec_eval rec_dummy_pi [x, y] = Pi y"
 apply(induct y)
-by(auto simp: rec_exec.simps rec_dummy_pi_def Pi.simps np_lemma)
+by(auto simp: rec_eval.simps rec_dummy_pi_def Pi.simps np_lemma)
 
 text {*
   The correctness of @{text "rec_pi"}.
   *}
-lemma pi_lemma: "rec_exec rec_pi [x] = Pi x"
-apply(simp add: rec_pi_def rec_exec.simps pi_dummy_lemma)
+lemma pi_lemma: "rec_eval rec_pi [x] = Pi x"
+apply(simp add: rec_pi_def rec_eval.simps pi_dummy_lemma)
 done
 
 fun loR :: "nat list \<Rightarrow> bool"
@@ -1833,23 +1833,23 @@
 
 lemma rec_lo_Maxr_lor:
   "\<lbrakk>Suc 0 < x; Suc 0 < y\<rbrakk> \<Longrightarrow>  
-        rec_exec rec_lo [x, y] = Maxr loR [x, y] x"
-proof(auto simp: rec_exec.simps rec_lo_def Let_def 
+        rec_eval rec_lo [x, y] = Maxr loR [x, y] x"
+proof(auto simp: rec_eval.simps rec_lo_def Let_def 
     numeral_2_eq_2 numeral_3_eq_3)
   let ?rR = "(Cn (Suc (Suc (Suc 0))) rec_eq
      [Cn (Suc (Suc (Suc 0))) rec_mod [recf.id (Suc (Suc (Suc 0))) 0,
      Cn (Suc (Suc (Suc 0))) rec_power [recf.id (Suc (Suc (Suc 0)))
      (Suc 0), recf.id (Suc (Suc (Suc 0))) (Suc (Suc 0))]],
      Cn (Suc (Suc (Suc 0))) (constn 0) [recf.id (Suc (Suc (Suc 0))) (Suc 0)]])"
-  have h: "rec_exec (rec_maxr ?rR) ([x, y] @ [x]) =
-    Maxr (\<lambda> args. 0 < rec_exec ?rR args) [x, y] x"
-    by(rule_tac Maxr_lemma, auto simp: rec_exec.simps
+  have h: "rec_eval (rec_maxr ?rR) ([x, y] @ [x]) =
+    Maxr (\<lambda> args. 0 < rec_eval ?rR args) [x, y] x"
+    by(rule_tac Maxr_lemma, auto simp: rec_eval.simps
       mod_lemma power_lemma, auto simp: numeral_2_eq_2 numeral_3_eq_3)
-  have "Maxr loR [x, y] x =  Maxr (\<lambda> args. 0 < rec_exec ?rR args) [x, y] x"
-    apply(simp add: rec_exec.simps mod_lemma power_lemma)
+  have "Maxr loR [x, y] x =  Maxr (\<lambda> args. 0 < rec_eval ?rR args) [x, y] x"
+    apply(simp add: rec_eval.simps mod_lemma power_lemma)
     apply(simp add: Maxr.simps loR.simps)
     done
-  from h and this show "rec_exec (rec_maxr ?rR) [x, y, x] = 
+  from h and this show "rec_eval (rec_maxr ?rR) [x, y, x] = 
     Maxr loR [x, y] x"
     apply(simp)
     done
@@ -1901,23 +1901,23 @@
 done
 
 lemma lo_lemma': "\<lbrakk>Suc 0 < x; Suc 0 < y\<rbrakk> \<Longrightarrow> 
-  rec_exec rec_lo [x, y] = lo x y"
+  rec_eval rec_lo [x, y] = lo x y"
 by(simp add: Maxr_lo  rec_lo_Maxr_lor)
 
-lemma lo_lemma'': "\<lbrakk>\<not> Suc 0 < x\<rbrakk> \<Longrightarrow> rec_exec rec_lo [x, y] = lo x y"
-apply(case_tac x, auto simp: rec_exec.simps rec_lo_def 
+lemma lo_lemma'': "\<lbrakk>\<not> Suc 0 < x\<rbrakk> \<Longrightarrow> rec_eval rec_lo [x, y] = lo x y"
+apply(case_tac x, auto simp: rec_eval.simps rec_lo_def 
   Let_def lo.simps)
 done
   
-lemma lo_lemma''': "\<lbrakk>\<not> Suc 0 < y\<rbrakk> \<Longrightarrow> rec_exec rec_lo [x, y] = lo x y"
-apply(case_tac y, auto simp: rec_exec.simps rec_lo_def 
+lemma lo_lemma''': "\<lbrakk>\<not> Suc 0 < y\<rbrakk> \<Longrightarrow> rec_eval rec_lo [x, y] = lo x y"
+apply(case_tac y, auto simp: rec_eval.simps rec_lo_def 
   Let_def lo.simps)
 done
 
 text {*
   The correctness of @{text "rec_lo"}:
 *}
-lemma lo_lemma: "rec_exec rec_lo [x, y] = lo x y" 
+lemma lo_lemma: "rec_eval rec_lo [x, y] = lo x y" 
 apply(case_tac "Suc 0 < x \<and> Suc 0 < y")
 apply(auto simp: lo_lemma' lo_lemma'' lo_lemma''')
 done
@@ -1954,24 +1954,24 @@
                     Cn 2 rec_mult [conR2, Cn 2 (constn 0) [id 2 0]]])"
 
 lemma lg_maxr: "\<lbrakk>Suc 0 < x; Suc 0 < y\<rbrakk> \<Longrightarrow> 
-                      rec_exec rec_lg [x, y] = Maxr lgR [x, y] x"
-proof(simp add: rec_exec.simps rec_lg_def Let_def)
+                      rec_eval rec_lg [x, y] = Maxr lgR [x, y] x"
+proof(simp add: rec_eval.simps rec_lg_def Let_def)
   assume h: "Suc 0 < x" "Suc 0 < y"
   let ?rR = "(Cn 3 rec_le [Cn 3 rec_power
                [recf.id 3 (Suc 0), recf.id 3 2], recf.id 3 0])"
-  have "rec_exec (rec_maxr ?rR) ([x, y] @ [x])
-              = Maxr ((\<lambda> args. 0 < rec_exec ?rR args)) [x, y] x" 
+  have "rec_eval (rec_maxr ?rR) ([x, y] @ [x])
+              = Maxr ((\<lambda> args. 0 < rec_eval ?rR args)) [x, y] x" 
   proof(rule Maxr_lemma)
     show "primerec (Cn 3 rec_le [Cn 3 rec_power 
               [recf.id 3 (Suc 0), recf.id 3 2], recf.id 3 0]) (Suc (length [x, y]))"
       apply(auto simp: numeral_3_eq_3)+
       done
   qed
-  moreover have "Maxr lgR [x, y] x = Maxr ((\<lambda> args. 0 < rec_exec ?rR args)) [x, y] x"
-    apply(simp add: rec_exec.simps power_lemma)
+  moreover have "Maxr lgR [x, y] x = Maxr ((\<lambda> args. 0 < rec_eval ?rR args)) [x, y] x"
+    apply(simp add: rec_eval.simps power_lemma)
     apply(simp add: Maxr.simps lgR.simps)
     done 
-  ultimately show "rec_exec (rec_maxr ?rR) [x, y, x] = Maxr lgR [x, y] x"
+  ultimately show "rec_eval (rec_maxr ?rR) [x, y, x] = Maxr lgR [x, y] x"
     by simp
 qed
 
@@ -1991,22 +1991,22 @@
 apply(erule_tac x = xa in allE, simp)
 done
 
-lemma lg_lemma': "\<lbrakk>Suc 0 < x; Suc 0 < y\<rbrakk> \<Longrightarrow> rec_exec rec_lg [x, y] = lg x y"
+lemma lg_lemma': "\<lbrakk>Suc 0 < x; Suc 0 < y\<rbrakk> \<Longrightarrow> rec_eval rec_lg [x, y] = lg x y"
 apply(simp add: maxr_lg lg_maxr)
 done
 
-lemma lg_lemma'': "\<not> Suc 0 < x \<Longrightarrow> rec_exec rec_lg [x, y] = lg x y"
-apply(simp add: rec_exec.simps rec_lg_def Let_def lg.simps)
+lemma lg_lemma'': "\<not> Suc 0 < x \<Longrightarrow> rec_eval rec_lg [x, y] = lg x y"
+apply(simp add: rec_eval.simps rec_lg_def Let_def lg.simps)
 done
 
-lemma lg_lemma''': "\<not> Suc 0 < y \<Longrightarrow> rec_exec rec_lg [x, y] = lg x y"
-apply(simp add: rec_exec.simps rec_lg_def Let_def lg.simps)
+lemma lg_lemma''': "\<not> Suc 0 < y \<Longrightarrow> rec_eval rec_lg [x, y] = lg x y"
+apply(simp add: rec_eval.simps rec_lg_def Let_def lg.simps)
 done
 
 text {*
   The correctness of @{text "rec_lg"}.
   *}
-lemma lg_lemma: "rec_exec rec_lg [x, y] = lg x y"
+lemma lg_lemma: "rec_eval rec_lg [x, y] = lg x y"
 apply(case_tac "Suc 0 < x \<and> Suc 0 < y", auto simp: 
                             lg_lemma' lg_lemma'' lg_lemma''')
 done
@@ -2032,8 +2032,8 @@
 text {*
   The correctness of @{text "rec_entry"}.
   *}
-lemma entry_lemma: "rec_exec rec_entry [str, i] = Entry str i"
-  by(simp add: rec_entry_def  rec_exec.simps lo_lemma pi_lemma)
+lemma entry_lemma: "rec_eval rec_entry [str, i] = Entry str i"
+  by(simp add: rec_entry_def  rec_eval.simps lo_lemma pi_lemma)
 
 
 subsection {* The construction of F *}
@@ -2057,9 +2057,9 @@
 declare listsum2.simps[simp del] rec_listsum2.simps[simp del]
 
 lemma listsum2_lemma: "\<lbrakk>length xs = vl; n \<le> vl\<rbrakk> \<Longrightarrow> 
-      rec_exec (rec_listsum2 vl n) xs = listsum2 xs n"
+      rec_eval (rec_listsum2 vl n) xs = listsum2 xs n"
 apply(induct n, simp_all)
-apply(simp_all add: rec_exec.simps rec_listsum2.simps listsum2.simps)
+apply(simp_all add: rec_eval.simps rec_listsum2.simps listsum2.simps)
 done
 
 fun strt' :: "nat list \<Rightarrow> nat \<Rightarrow> nat"
@@ -2081,9 +2081,9 @@
 declare strt'.simps[simp del] rec_strt'.simps[simp del]
 
 lemma strt'_lemma: "\<lbrakk>length xs = vl; n \<le> vl\<rbrakk> \<Longrightarrow> 
-  rec_exec (rec_strt' vl n) xs = strt' xs n"
+  rec_eval (rec_strt' vl n) xs = strt' xs n"
 apply(induct n)
-apply(simp_all add: rec_exec.simps rec_strt'.simps strt'.simps
+apply(simp_all add: rec_eval.simps rec_strt'.simps strt'.simps
   Let_def power_lemma listsum2_lemma)
 done
 
@@ -2108,30 +2108,30 @@
   "rec_strt vl = Cn vl (rec_strt' vl vl) (rec_map s vl)"
 
 lemma map_s_lemma: "length xs = vl \<Longrightarrow> 
-  map ((\<lambda>a. rec_exec a xs) \<circ> (\<lambda>i. Cn vl s [recf.id vl i]))
+  map ((\<lambda>a. rec_eval a xs) \<circ> (\<lambda>i. Cn vl s [recf.id vl i]))
   [0..<vl]
         = map Suc xs"
-apply(induct vl arbitrary: xs, simp, auto simp: rec_exec.simps)
+apply(induct vl arbitrary: xs, simp, auto simp: rec_eval.simps)
 apply(subgoal_tac "\<exists> ys y. xs = ys @ [y]", auto)
 proof -
   fix ys y
   assume ind: "\<And>xs. length xs = length (ys::nat list) \<Longrightarrow>
-      map ((\<lambda>a. rec_exec a xs) \<circ> (\<lambda>i. Cn (length ys) s 
+      map ((\<lambda>a. rec_eval a xs) \<circ> (\<lambda>i. Cn (length ys) s 
         [recf.id (length ys) (i)])) [0..<length ys] = map Suc xs"
   show
-    "map ((\<lambda>a. rec_exec a (ys @ [y])) \<circ> (\<lambda>i. Cn (Suc (length ys)) s 
+    "map ((\<lambda>a. rec_eval a (ys @ [y])) \<circ> (\<lambda>i. Cn (Suc (length ys)) s 
   [recf.id (Suc (length ys)) (i)])) [0..<length ys] = map Suc ys"
   proof -
-    have "map ((\<lambda>a. rec_exec a ys) \<circ> (\<lambda>i. Cn (length ys) s
+    have "map ((\<lambda>a. rec_eval a ys) \<circ> (\<lambda>i. Cn (length ys) s
         [recf.id (length ys) (i)])) [0..<length ys] = map Suc ys"
       apply(rule_tac ind, simp)
       done
     moreover have
-      "map ((\<lambda>a. rec_exec a (ys @ [y])) \<circ> (\<lambda>i. Cn (Suc (length ys)) s
+      "map ((\<lambda>a. rec_eval a (ys @ [y])) \<circ> (\<lambda>i. Cn (Suc (length ys)) s
            [recf.id (Suc (length ys)) (i)])) [0..<length ys]
-         = map ((\<lambda>a. rec_exec a ys) \<circ> (\<lambda>i. Cn (length ys) s 
+         = map ((\<lambda>a. rec_eval a ys) \<circ> (\<lambda>i. Cn (length ys) s 
                  [recf.id (length ys) (i)])) [0..<length ys]"
-      apply(rule_tac map_ext, auto simp: rec_exec.simps nth_append)
+      apply(rule_tac map_ext, auto simp: rec_eval.simps nth_append)
       done
     ultimately show "?thesis"
       by simp
@@ -2149,9 +2149,9 @@
   The correctness of @{text "rec_strt"}.
   *}
 lemma strt_lemma: "length xs = vl \<Longrightarrow> 
-  rec_exec (rec_strt vl) xs = strt xs"
-apply(simp add: strt.simps rec_exec.simps strt'_lemma)
-apply(subgoal_tac "(map ((\<lambda>a. rec_exec a xs) \<circ> (\<lambda>i. Cn vl s [recf.id vl (i)])) [0..<vl])
+  rec_eval (rec_strt vl) xs = strt xs"
+apply(simp add: strt.simps rec_eval.simps strt'_lemma)
+apply(subgoal_tac "(map ((\<lambda>a. rec_eval a xs) \<circ> (\<lambda>i. Cn vl s [recf.id vl (i)])) [0..<vl])
                   = map Suc xs", auto)
 apply(rule map_s_lemma, simp)
 done
@@ -2172,8 +2172,8 @@
 text {*
   The correctness of @{text "scan"}.
   *}
-lemma scan_lemma: "rec_exec rec_scan [r] = r mod 2"
-  by(simp add: rec_exec.simps rec_scan_def mod_lemma)
+lemma scan_lemma: "rec_eval rec_scan [r] = r mod 2"
+  by(simp add: rec_eval.simps rec_scan_def mod_lemma)
 
 fun newleft0 :: "nat list \<Rightarrow> nat"
   where
@@ -2295,7 +2295,7 @@
   The correctness of @{text "rec_newleft"}.
   *}
 lemma newleft_lemma: 
-  "rec_exec rec_newleft [p, r, a] = newleft p r a"
+  "rec_eval rec_newleft [p, r, a] = newleft p r a"
 proof(simp only: rec_newleft_def Let_def)
   let ?rgs = "[Cn 3 rec_newleft0 [recf.id 3 0, recf.id 3 1], Cn 3 rec_newleft2 
        [recf.id 3 0, recf.id 3 1], Cn 3 rec_newleft3 [recf.id 3 0, recf.id 3 1], recf.id 3 0]"
@@ -2305,8 +2305,8 @@
      Cn 3 rec_eq [recf.id 3 2, Cn 3 (constn 2) [recf.id 3 0]],
      Cn 3 rec_eq [recf.id 3 2, Cn 3 (constn 3) [recf.id 3 0]],
      Cn 3 rec_less [Cn 3 (constn 3) [recf.id 3 0], recf.id 3 2]]"
-  have k1: "rec_exec (rec_embranch (zip ?rgs ?rrs)) [p, r, a]
-                         = Embranch (zip (map rec_exec ?rgs) (map (\<lambda>r args. 0 < rec_exec r args) ?rrs)) [p, r, a]"
+  have k1: "rec_eval (rec_embranch (zip ?rgs ?rrs)) [p, r, a]
+                         = Embranch (zip (map rec_eval ?rgs) (map (\<lambda>r args. 0 < rec_eval r args) ?rrs)) [p, r, a]"
     apply(rule_tac embranch_lemma )
     apply(auto simp: numeral_3_eq_3 numeral_2_eq_2 rec_newleft0_def 
              rec_newleft1_def rec_newleft2_def rec_newleft3_def)+
@@ -2317,17 +2317,17 @@
     apply(case_tac "a = 3", rule_tac x = "2" in exI)
     prefer 2
     apply(case_tac "a > 3", rule_tac x = "3" in exI, auto)
-    apply(auto simp: rec_exec.simps)
-    apply(erule_tac [!] Suc_Suc_Suc_Suc_induct, auto simp: rec_exec.simps)
+    apply(auto simp: rec_eval.simps)
+    apply(erule_tac [!] Suc_Suc_Suc_Suc_induct, auto simp: rec_eval.simps)
     done
-  have k2: "Embranch (zip (map rec_exec ?rgs) (map (\<lambda>r args. 0 < rec_exec r args) ?rrs)) [p, r, a] = newleft p r a"
+  have k2: "Embranch (zip (map rec_eval ?rgs) (map (\<lambda>r args. 0 < rec_eval r args) ?rrs)) [p, r, a] = newleft p r a"
     apply(simp add: Embranch.simps)
-    apply(simp add: rec_exec.simps)
-    apply(auto simp: newleft.simps rec_newleft0_def rec_exec.simps
+    apply(simp add: rec_eval.simps)
+    apply(auto simp: newleft.simps rec_newleft0_def rec_eval.simps
                      rec_newleft1_def rec_newleft2_def rec_newleft3_def)
     done
   from k1 and k2 show 
-   "rec_exec (rec_embranch (zip ?rgs ?rrs)) [p, r, a] = newleft p r a"
+   "rec_eval (rec_embranch (zip ?rgs ?rrs)) [p, r, a] = newleft p r a"
     by simp
 qed
 
@@ -2384,7 +2384,7 @@
 text {*
   The correctness of @{text "rec_newrght"}.
   *}
-lemma newrght_lemma: "rec_exec rec_newrght [p, r, a] = newrght p r a"
+lemma newrght_lemma: "rec_eval rec_newrght [p, r, a] = newrght p r a"
 proof(simp only: rec_newrght_def Let_def)
   let ?gs' = "[newrgt0, newrgt1, newrgt2, newrgt3, \<lambda> zs. zs ! 1]"
   let ?r0 = "\<lambda> zs. zs ! 2 = 0"
@@ -2405,8 +2405,8 @@
      Cn 3 rec_eq [recf.id 3 2, Cn 3 (constn 3) [recf.id 3 0]], 
        Cn 3 rec_less [Cn 3 (constn 3) [recf.id 3 0], recf.id 3 2]]"
     
-  have k1: "rec_exec (rec_embranch (zip ?rgs ?rrs)) [p, r, a]
-    = Embranch (zip (map rec_exec ?rgs) (map (\<lambda>r args. 0 < rec_exec r args) ?rrs)) [p, r, a]"
+  have k1: "rec_eval (rec_embranch (zip ?rgs ?rrs)) [p, r, a]
+    = Embranch (zip (map rec_eval ?rgs) (map (\<lambda>r args. 0 < rec_eval r args) ?rrs)) [p, r, a]"
     apply(rule_tac embranch_lemma)
     apply(auto simp: numeral_3_eq_3 numeral_2_eq_2 rec_newrgt0_def 
              rec_newrgt1_def rec_newrgt2_def rec_newrgt3_def)+
@@ -2418,18 +2418,18 @@
     prefer 2
     apply(case_tac "a = 3", rule_tac x = "3" in exI)
     prefer 2
-    apply(case_tac "a > 3", rule_tac x = "4" in exI, auto simp: rec_exec.simps)
-    apply(erule_tac [!] Suc_5_induct, auto simp: rec_exec.simps)
+    apply(case_tac "a > 3", rule_tac x = "4" in exI, auto simp: rec_eval.simps)
+    apply(erule_tac [!] Suc_5_induct, auto simp: rec_eval.simps)
     done
-  have k2: "Embranch (zip (map rec_exec ?rgs)
-    (map (\<lambda>r args. 0 < rec_exec r args) ?rrs)) [p, r, a] = newrght p r a"
-    apply(auto simp:Embranch.simps rec_exec.simps)
+  have k2: "Embranch (zip (map rec_eval ?rgs)
+    (map (\<lambda>r args. 0 < rec_eval r args) ?rrs)) [p, r, a] = newrght p r a"
+    apply(auto simp:Embranch.simps rec_eval.simps)
     apply(auto simp: newrght.simps rec_newrgt3_def rec_newrgt2_def
-                     rec_newrgt1_def rec_newrgt0_def rec_exec.simps
+                     rec_newrgt1_def rec_newrgt0_def rec_eval.simps
                      scan_lemma)
     done
   from k1 and k2 show 
-    "rec_exec (rec_embranch (zip ?rgs ?rrs)) [p, r, a] =      
+    "rec_eval (rec_embranch (zip ?rgs ?rrs)) [p, r, a] =      
                                     newrght p r a" by simp
 qed
 
@@ -2466,8 +2466,8 @@
 text {*
   The correctness of @{text "actn"}.
   *}
-lemma actn_lemma: "rec_exec rec_actn [m, q, r] = actn m q r"
-  by(auto simp: rec_actn_def rec_exec.simps entry_lemma scan_lemma)
+lemma actn_lemma: "rec_eval rec_actn [m, q, r] = actn m q r"
+  by(auto simp: rec_actn_def rec_eval.simps entry_lemma scan_lemma)
 
 fun newstat :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat"
   where
@@ -2486,8 +2486,8 @@
            Cn 3 rec_mult [Cn 3 (constn 0) [id 3 0], 
            Cn 3 rec_eq [id 3 1, Cn 3 (constn 0) [id 3 0]]]] "
 
-lemma newstat_lemma: "rec_exec rec_newstat [m, q, r] = newstat m q r"
-by(auto simp:  rec_exec.simps entry_lemma scan_lemma rec_newstat_def)
+lemma newstat_lemma: "rec_eval rec_newstat [m, q, r] = newstat m q r"
+by(auto simp:  rec_eval.simps entry_lemma scan_lemma rec_newstat_def)
 
 declare newstat.simps[simp del] actn.simps[simp del]
 
@@ -2504,8 +2504,8 @@
         Cn 3 rec_power [Cn 3 (constn (Pi 1)) [id 3 0], id 3 1]],
         Cn 3 rec_power [Cn 3 (constn (Pi 2)) [id 3 0], id 3 2]]"
 declare trpl.simps[simp del]
-lemma trpl_lemma: "rec_exec rec_trpl [p, q, r] = trpl p q r"
-by(auto simp: rec_trpl_def rec_exec.simps power_lemma trpl.simps)
+lemma trpl_lemma: "rec_eval rec_trpl [p, q, r] = trpl p q r"
+by(auto simp: rec_trpl_def rec_eval.simps power_lemma trpl.simps)
 
 text{*left, stat, rght: decode func*}
 fun left :: "nat \<Rightarrow> nat"
@@ -2555,24 +2555,24 @@
                    Cn vl (rec_strt (vl - 1)) 
                         (map (\<lambda> i. id vl (i)) [1..<vl])]"
 
-lemma left_lemma: "rec_exec rec_left [c] = left c"
-by(simp add: rec_exec.simps rec_left_def left.simps lo_lemma)
+lemma left_lemma: "rec_eval rec_left [c] = left c"
+by(simp add: rec_eval.simps rec_left_def left.simps lo_lemma)
       
-lemma right_lemma: "rec_exec rec_right [c] = rght c"
-by(simp add: rec_exec.simps rec_right_def rght.simps lo_lemma)
-
-lemma stat_lemma: "rec_exec rec_stat [c] = stat c"
-by(simp add: rec_exec.simps rec_stat_def stat.simps lo_lemma)
+lemma right_lemma: "rec_eval rec_right [c] = rght c"
+by(simp add: rec_eval.simps rec_right_def rght.simps lo_lemma)
+
+lemma stat_lemma: "rec_eval rec_stat [c] = stat c"
+by(simp add: rec_eval.simps rec_stat_def stat.simps lo_lemma)
  
 declare rec_strt.simps[simp del] strt.simps[simp del]
 
 lemma map_cons_eq: 
-  "(map ((\<lambda>a. rec_exec a (m # xs)) \<circ> 
+  "(map ((\<lambda>a. rec_eval a (m # xs)) \<circ> 
     (\<lambda>i. recf.id (Suc (length xs)) (i))) 
           [Suc 0..<Suc (length xs)])
         = map (\<lambda> i. xs ! (i - 1)) [Suc 0..<Suc (length xs)]"
 apply(rule map_ext, auto)
-apply(auto simp: rec_exec.simps nth_append nth_Cons split: nat.split)
+apply(auto simp: rec_eval.simps nth_append nth_Cons split: nat.split)
 done
 
 lemma list_map_eq: 
@@ -2616,11 +2616,11 @@
 
 lemma [elim]: 
   "Suc 0 \<le> length xs \<Longrightarrow> 
-     (map ((\<lambda>a. rec_exec a (m # xs)) \<circ> 
+     (map ((\<lambda>a. rec_eval a (m # xs)) \<circ> 
          (\<lambda>i. recf.id (Suc (length xs)) (i))) 
              [Suc 0..<length xs] @ [(m # xs) ! length xs]) = xs"
 using map_cons_eq[of m xs]
-apply(simp del: map_eq_conv add: rec_exec.simps)
+apply(simp del: map_eq_conv add: rec_eval.simps)
 using list_map_eq[of "length xs" xs]
 apply(simp)
 done
@@ -2628,11 +2628,11 @@
     
 lemma inpt_lemma:
   "\<lbrakk>Suc (length xs) = vl\<rbrakk> \<Longrightarrow> 
-            rec_exec (rec_inpt vl) (m # xs) = inpt m xs"
-apply(auto simp: rec_exec.simps rec_inpt_def 
+            rec_eval (rec_inpt vl) (m # xs) = inpt m xs"
+apply(auto simp: rec_eval.simps rec_inpt_def 
                  trpl_lemma inpt.simps strt_lemma)
 apply(subgoal_tac
-  "(map ((\<lambda>a. rec_exec a (m # xs)) \<circ> 
+  "(map ((\<lambda>a. rec_eval a (m # xs)) \<circ> 
           (\<lambda>i. recf.id (Suc (length xs)) (i))) 
             [Suc 0..<length xs] @ [(m # xs) ! length xs]) = xs", simp)
 apply(auto, case_tac xs, auto)
@@ -2656,8 +2656,8 @@
                                    Cn 2 rec_stat [id 2 1], 
                              Cn 2 rec_right [id 2 1]]]]"
 
-lemma newconf_lemma: "rec_exec rec_newconf [m ,c] = newconf m c"
-by(auto simp: rec_newconf_def rec_exec.simps 
+lemma newconf_lemma: "rec_eval rec_newconf [m ,c] = newconf m c"
+by(auto simp: rec_newconf_def rec_eval.simps 
               trpl_lemma newleft_lemma left_lemma
               right_lemma stat_lemma newrght_lemma actn_lemma 
                newstat_lemma stat_lemma newconf.simps)
@@ -2685,15 +2685,15 @@
                   (Cn 4 rec_newconf [id 4 0, id 4 3])"
 
 lemma conf_step: 
-  "rec_exec rec_conf [m, r, Suc t] =
-         rec_exec rec_newconf [m, rec_exec rec_conf [m, r, t]]"
+  "rec_eval rec_conf [m, r, Suc t] =
+         rec_eval rec_newconf [m, rec_eval rec_conf [m, r, t]]"
 proof -
-  have "rec_exec rec_conf ([m, r] @ [Suc t]) = 
-          rec_exec rec_newconf [m, rec_exec rec_conf [m, r, t]]"
+  have "rec_eval rec_conf ([m, r] @ [Suc t]) = 
+          rec_eval rec_newconf [m, rec_eval rec_conf [m, r, t]]"
     by(simp only: rec_conf_def rec_pr_Suc_simp_rewrite,
-        simp add: rec_exec.simps)
-  thus "rec_exec rec_conf [m, r, Suc t] =
-                rec_exec rec_newconf [m, rec_exec rec_conf [m, r, t]]"
+        simp add: rec_eval.simps)
+  thus "rec_eval rec_conf [m, r, Suc t] =
+                rec_eval rec_newconf [m, rec_eval rec_conf [m, r, t]]"
     by simp
 qed
 
@@ -2701,9 +2701,9 @@
   The correctness of @{text "rec_conf"}.
   *}
 lemma conf_lemma: 
-  "rec_exec rec_conf [m, r, t] = conf m r t"
+  "rec_eval rec_conf [m, r, t] = conf m r t"
 apply(induct t)
-apply(simp add: rec_conf_def rec_exec.simps conf.simps inpt_lemma trpl_lemma)
+apply(simp add: rec_conf_def rec_eval.simps conf.simps inpt_lemma trpl_lemma)
 apply(simp add: conf_step conf.simps)
 done
 
@@ -2735,21 +2735,21 @@
                                             constn 2]], constn 1]]],
                Cn 1 rec_eq [rec_right, constn 0]]"
 
-lemma NSTD_lemma1: "rec_exec rec_NSTD [c] = Suc 0 \<or>
-                   rec_exec rec_NSTD [c] = 0"
-by(simp add: rec_exec.simps rec_NSTD_def)
+lemma NSTD_lemma1: "rec_eval rec_NSTD [c] = Suc 0 \<or>
+                   rec_eval rec_NSTD [c] = 0"
+by(simp add: rec_eval.simps rec_NSTD_def)
 
 declare NSTD.simps[simp del]
-lemma NSTD_lemma2': "(rec_exec rec_NSTD [c] = Suc 0) \<Longrightarrow> NSTD c"
-apply(simp add: rec_exec.simps rec_NSTD_def stat_lemma left_lemma 
+lemma NSTD_lemma2': "(rec_eval rec_NSTD [c] = Suc 0) \<Longrightarrow> NSTD c"
+apply(simp add: rec_eval.simps rec_NSTD_def stat_lemma left_lemma 
                 lg_lemma right_lemma power_lemma NSTD.simps eq_lemma)
 apply(auto)
 apply(case_tac "0 < left c", simp, simp)
 done
 
 lemma NSTD_lemma2'': 
-  "NSTD c \<Longrightarrow> (rec_exec rec_NSTD [c] = Suc 0)"
-apply(simp add: rec_exec.simps rec_NSTD_def stat_lemma 
+  "NSTD c \<Longrightarrow> (rec_eval rec_NSTD [c] = Suc 0)"
+apply(simp add: rec_eval.simps rec_NSTD_def stat_lemma 
          left_lemma lg_lemma right_lemma power_lemma NSTD.simps)
 apply(auto split: if_splits)
 done
@@ -2757,7 +2757,7 @@
 text {*
   The correctness of @{text "NSTD"}.
   *}
-lemma NSTD_lemma2: "(rec_exec rec_NSTD [c] = Suc 0) = NSTD c"
+lemma NSTD_lemma2: "(rec_eval rec_NSTD [c] = Suc 0) = NSTD c"
 using NSTD_lemma1
 apply(auto intro: NSTD_lemma2' NSTD_lemma2'')
 done
@@ -2766,7 +2766,7 @@
   where
   "nstd c = (if NSTD c then 1 else 0)"
 
-lemma nstd_lemma: "rec_exec rec_NSTD [c] = nstd c"
+lemma nstd_lemma: "rec_eval rec_NSTD [c] = nstd c"
 using NSTD_lemma1
 apply(simp add: NSTD_lemma2, auto)
 done
@@ -2790,8 +2790,8 @@
   The correctness of @{text "rec_nonstop"}.
   *}
 lemma nonstop_lemma: 
-  "rec_exec rec_nonstop [m, r, t] = nonstop m r t"
-apply(simp add: rec_exec.simps rec_nonstop_def nstd_lemma conf_lemma)
+  "rec_eval rec_nonstop [m, r, t] = nonstop m r t"
+apply(simp add: rec_eval.simps rec_nonstop_def nstd_lemma conf_lemma)
 done
 
 text{*
@@ -2985,51 +2985,51 @@
     @{thm prime_id}, @{thm prime_pr}] 1*}, auto+)+
 done
 
-lemma primerec_terminate: 
-  "\<lbrakk>primerec f x; length xs = x\<rbrakk> \<Longrightarrow> terminate f xs"
+lemma primerec_terminates: 
+  "\<lbrakk>primerec f x; length xs = x\<rbrakk> \<Longrightarrow> terminates f xs"
 proof(induct arbitrary: xs rule: primerec.induct)
   fix xs
-  assume "length (xs::nat list) = Suc 0"  thus "terminate z xs"
+  assume "length (xs::nat list) = Suc 0"  thus "terminates z xs"
     by(case_tac xs, auto intro: termi_z)
 next
   fix xs
-  assume "length (xs::nat list) = Suc 0" thus "terminate s xs"
+  assume "length (xs::nat list) = Suc 0" thus "terminates s xs"
     by(case_tac xs, auto intro: termi_s)
 next
   fix n m xs
-  assume "n < m" "length (xs::nat list) = m"  thus "terminate (id m n) xs"
+  assume "n < m" "length (xs::nat list) = m"  thus "terminates (id m n) xs"
     by(erule_tac termi_id, simp)
 next
   fix f k gs m n xs
-  assume ind: "\<forall>i<length gs. primerec (gs ! i) m \<and> (\<forall>x. length x = m \<longrightarrow> terminate (gs ! i) x)"
-  and ind2: "\<And> xs. length xs = k \<Longrightarrow> terminate f xs"
+  assume ind: "\<forall>i<length gs. primerec (gs ! i) m \<and> (\<forall>x. length x = m \<longrightarrow> terminates (gs ! i) x)"
+  and ind2: "\<And> xs. length xs = k \<Longrightarrow> terminates f xs"
   and h: "primerec f k"  "length gs = k" "m = n" "length (xs::nat list) = m"
-  have "terminate f (map (\<lambda>g. rec_exec g xs) gs)"
-    using ind2[of "(map (\<lambda>g. rec_exec g xs) gs)"] h
+  have "terminates f (map (\<lambda>g. rec_eval g xs) gs)"
+    using ind2[of "(map (\<lambda>g. rec_eval g xs) gs)"] h
     by simp
-  moreover have "\<forall>g\<in>set gs. terminate g xs"
+  moreover have "\<forall>g\<in>set gs. terminates g xs"
     using ind h
     by(auto simp: set_conv_nth)
-  ultimately show "terminate (Cn n f gs) xs"
+  ultimately show "terminates (Cn n f gs) xs"
     using h
     by(rule_tac termi_cn, auto)
 next
   fix f n g m xs
-  assume ind1: "\<And>xs. length xs = n \<Longrightarrow> terminate f xs"
-  and ind2: "\<And>xs. length xs = Suc (Suc n) \<Longrightarrow> terminate g xs"
+  assume ind1: "\<And>xs. length xs = n \<Longrightarrow> terminates f xs"
+  and ind2: "\<And>xs. length xs = Suc (Suc n) \<Longrightarrow> terminates g xs"
   and h: "primerec f n" " primerec g (Suc (Suc n))" " m = Suc n" "length (xs::nat list) = m"
-  have "\<forall>y<last xs. terminate g (butlast xs @ [y, rec_exec (Pr n f g) (butlast xs @ [y])])"
+  have "\<forall>y<last xs. terminates g (butlast xs @ [y, rec_eval (Pr n f g) (butlast xs @ [y])])"
     using h
     apply(auto) 
     by(rule_tac ind2, simp)
-  moreover have "terminate f (butlast xs)"
+  moreover have "terminates f (butlast xs)"
     using ind1[of "butlast xs"] h
     by simp
  moreover have "length (butlast xs) = n"
    using h by simp
- ultimately have "terminate (Pr n f g) (butlast xs @ [last xs])"
+ ultimately have "terminates (Pr n f g) (butlast xs @ [last xs])"
    by(rule_tac termi_pr, simp_all)
- thus "terminate (Pr n f g) xs"
+ thus "terminates (Pr n f g) xs"
    using h
    by(case_tac "xs = []", auto)
 qed
@@ -3061,8 +3061,8 @@
 text {*
   The correctness of @{text "rec_valu"}.
 *}
-lemma value_lemma: "rec_exec rec_valu [r] = valu r"
-apply(simp add: rec_exec.simps rec_valu_def lg_lemma)
+lemma value_lemma: "rec_eval rec_valu [r] = valu r"
+apply(simp add: rec_eval.simps rec_valu_def lg_lemma)
 done
 
 lemma [intro]: "primerec rec_valu (Suc 0)"
@@ -3101,12 +3101,12 @@
                                   id (length ys) (k)"
 by(erule_tac get_fstn_args_nth)
 
-lemma terminate_halt_lemma: 
-  "\<lbrakk>rec_exec rec_nonstop ([m, r] @ [t]) = 0; 
-     \<forall>i<t. 0 < rec_exec rec_nonstop ([m, r] @ [i])\<rbrakk> \<Longrightarrow> terminate rec_halt [m, r]"
+lemma terminates_halt_lemma: 
+  "\<lbrakk>rec_eval rec_nonstop ([m, r] @ [t]) = 0; 
+     \<forall>i<t. 0 < rec_eval rec_nonstop ([m, r] @ [i])\<rbrakk> \<Longrightarrow> terminates rec_halt [m, r]"
 apply(simp add: rec_halt_def)
 apply(rule_tac termi_mn, auto)
-apply(rule_tac [!] primerec_terminate, auto)
+apply(rule_tac [!] primerec_terminates, auto)
 done
 
 
@@ -3114,17 +3114,17 @@
   The correctness of @{text "rec_F"}, halt case.
   *}
 
-lemma F_lemma: "rec_exec rec_halt [m, r] = t \<Longrightarrow> rec_exec rec_F [m, r] = (valu (rght (conf m r t)))"
-by(simp add: rec_F_def rec_exec.simps value_lemma right_lemma conf_lemma halt_lemma)
-
-lemma terminate_F_lemma: "terminate rec_halt [m, r] \<Longrightarrow> terminate rec_F [m, r]"
+lemma F_lemma: "rec_eval rec_halt [m, r] = t \<Longrightarrow> rec_eval rec_F [m, r] = (valu (rght (conf m r t)))"
+by(simp add: rec_F_def rec_eval.simps value_lemma right_lemma conf_lemma halt_lemma)
+
+lemma terminates_F_lemma: "terminates rec_halt [m, r] \<Longrightarrow> terminates rec_F [m, r]"
 apply(simp add: rec_F_def)
 apply(rule_tac termi_cn, auto)
-apply(rule_tac primerec_terminate, auto)
+apply(rule_tac primerec_terminates, auto)
 apply(rule_tac termi_cn, auto)
-apply(rule_tac primerec_terminate, auto)
+apply(rule_tac primerec_terminates, auto)
 apply(rule_tac termi_cn, auto)
-apply(rule_tac primerec_terminate, auto)
+apply(rule_tac primerec_terminates, auto)
 apply(rule_tac [!] termi_id, auto)
 done
 
@@ -4001,7 +4001,7 @@
 lemma rec_t_eq_step: 
   "(\<lambda> (s, l, r). s \<le> length tp div 2) c \<Longrightarrow>
   trpl_code (step0 c tp) = 
-  rec_exec rec_newconf [code tp, trpl_code c]"
+  rec_eval rec_newconf [code tp, trpl_code c]"
   apply(cases c, simp)
 proof(case_tac "fetch tp a (read ca)",
     simp add: newconf.simps trpl_code.simps step.simps)
@@ -4163,8 +4163,8 @@
 
 lemma [simp]:
  "trpl_code (steps0 (Suc 0, Bk\<up>l, <lm>) tp 0) = 
-    rec_exec rec_conf [code tp, bl2wc (<lm>), 0]"
-apply(simp add: steps.simps rec_exec.simps conf_lemma  conf.simps 
+    rec_eval rec_conf [code tp, bl2wc (<lm>), 0]"
+apply(simp add: steps.simps rec_eval.simps conf_lemma  conf.simps 
                 inpt.simps trpl_code.simps bl2wc.simps)
 done
 
@@ -4212,7 +4212,7 @@
 lemma rec_t_eq_steps:
   "tm_wf (tp,0) \<Longrightarrow>
   trpl_code (steps0 (Suc 0, Bk\<up>l, <lm>) tp stp) = 
-  rec_exec rec_conf [code tp, bl2wc (<lm>), stp]"
+  rec_eval rec_conf [code tp, bl2wc (<lm>), stp]"
 proof(induct stp)
   case 0 thus "?case" by(simp)
 next
@@ -4220,11 +4220,11 @@
   proof -
     assume ind: 
       "tm_wf (tp,0) \<Longrightarrow> trpl_code (steps0 (Suc 0, Bk\<up> l, <lm>) tp n) 
-      = rec_exec rec_conf [code tp, bl2wc (<lm>), n]"
+      = rec_eval rec_conf [code tp, bl2wc (<lm>), n]"
       and h: "tm_wf (tp, 0)"
     show 
       "trpl_code (steps0 (Suc 0, Bk\<up> l, <lm>) tp (Suc n)) =
-      rec_exec rec_conf [code tp, bl2wc (<lm>), Suc n]"
+      rec_eval rec_conf [code tp, bl2wc (<lm>), Suc n]"
     proof(case_tac "steps0 (Suc 0, Bk\<up> l, <lm>) tp  n", 
         simp only: step_red conf_lemma conf.simps)
       fix a b c
@@ -4235,7 +4235,7 @@
         done
       moreover hence 
         "trpl_code (step0 (a, b, c) tp) = 
-        rec_exec rec_newconf [code tp, trpl_code (a, b, c)]"
+        rec_eval rec_newconf [code tp, trpl_code (a, b, c)]"
         apply(rule_tac rec_t_eq_step)
         using h g
         apply(simp add: state_in_range)
@@ -4293,11 +4293,11 @@
   "\<lbrakk>steps0 (Suc 0, Bk\<up>l, <lm>) tp stp = (0, Bk\<up> m, Oc\<up> rs @ Bk\<up> n); 
    tm_wf (tp, 0); 
   rs > 0\<rbrakk> 
-  \<Longrightarrow> rec_exec rec_nonstop [code tp, bl2wc (<lm>), stp] = 0"
+  \<Longrightarrow> rec_eval rec_nonstop [code tp, bl2wc (<lm>), stp] = 0"
 proof(simp add: nonstop_lemma nonstop.simps nstd.simps)
   assume h: "steps0 (Suc 0, Bk\<up>l, <lm>) tp stp = (0, Bk\<up> m, Oc\<up> rs @ Bk\<up> n)"
   and tc_t: "tm_wf (tp, 0)" "rs > 0"
-  have g: "rec_exec rec_conf [code tp,  bl2wc (<lm>), stp] =
+  have g: "rec_eval rec_conf [code tp,  bl2wc (<lm>), stp] =
                                         trpl_code (0, Bk\<up> m, Oc\<up> rs@Bk\<up> n)"
     using rec_t_eq_steps[of tp l lm stp] tc_t h
     by(simp)
@@ -4487,26 +4487,26 @@
   execution of of TMs.
   *}
 
-lemma terminate_halt: 
+lemma terminates_halt: 
   "\<lbrakk>steps0 (Suc 0, Bk\<up>l, <lm>) tp stp = (0, Bk\<up>m, Oc\<up>rs@Bk\<up>n); 
-    tm_wf (tp,0); 0<rs\<rbrakk> \<Longrightarrow> terminate rec_halt [code tp, (bl2wc (<lm>))]"
+    tm_wf (tp,0); 0<rs\<rbrakk> \<Longrightarrow> terminates rec_halt [code tp, (bl2wc (<lm>))]"
 apply(frule_tac halt_least_step, auto)
-thm terminate_halt_lemma
-apply(rule_tac t = stpa in terminate_halt_lemma)
+thm terminates_halt_lemma
+apply(rule_tac t = stpa in terminates_halt_lemma)
 apply(simp_all add: nonstop_lemma, auto)
 done
 
-lemma terminate_F: 
+lemma terminates_F: 
   "\<lbrakk>steps0 (Suc 0, Bk\<up>l, <lm>) tp stp = (0, Bk\<up>m, Oc\<up>rs@Bk\<up>n); 
-    tm_wf (tp,0); 0<rs\<rbrakk> \<Longrightarrow> terminate rec_F [code tp, (bl2wc (<lm>))]"
-apply(drule_tac terminate_halt, simp_all)
-apply(erule_tac terminate_F_lemma)
+    tm_wf (tp,0); 0<rs\<rbrakk> \<Longrightarrow> terminates rec_F [code tp, (bl2wc (<lm>))]"
+apply(drule_tac terminates_halt, simp_all)
+apply(erule_tac terminates_F_lemma)
 done
 
 lemma F_correct: 
   "\<lbrakk>steps0 (Suc 0, Bk\<up>l, <lm>) tp stp = (0, Bk\<up>m, Oc\<up>rs@Bk\<up>n); 
     tm_wf (tp,0); 0<rs\<rbrakk>
-   \<Longrightarrow> rec_exec rec_F [code tp, (bl2wc (<lm>))] = (rs - Suc 0)"
+   \<Longrightarrow> rec_eval rec_F [code tp, (bl2wc (<lm>))] = (rs - Suc 0)"
 apply(frule_tac halt_least_step, auto)
 apply(frule_tac  nonstop_t_eq, auto simp: nonstop_lemma)
 using rec_t_eq_steps[of tp l lm stp]
@@ -4523,11 +4523,11 @@
     using halt_state_keep[of "code tp" lm stpa stp]
     by(simp)
   moreover have g2:
-    "rec_exec rec_halt [code tp, (bl2wc (<lm>))] = stpa"
+    "rec_eval rec_halt [code tp, (bl2wc (<lm>))] = stpa"
     using h
-    by(auto simp: rec_exec.simps rec_halt_def nonstop_lemma intro!: Least_equality)
+    by(auto simp: rec_eval.simps rec_halt_def nonstop_lemma intro!: Least_equality)
   show  
-    "rec_exec rec_F [code tp, (bl2wc (<lm>))] = (rs - Suc 0)"
+    "rec_eval rec_F [code tp, (bl2wc (<lm>))] = (rs - Suc 0)"
   proof -
     have 
       "valu (rght (conf (code tp) (bl2wc (<lm>)) stpa)) = rs - Suc 0" 
@@ -4536,7 +4536,7 @@
         bl2wc.simps  bl2nat_append lg_power)
       done
     thus "?thesis" 
-      by(simp add: rec_exec.simps F_lemma g2)
+      by(simp add: rec_eval.simps F_lemma g2)
   qed
 qed
 
diff -r ac3309722536 -r 696081f445c2 thys/UTM.thy
--- a/thys/UTM.thy	Wed Apr 24 09:49:00 2013 +0100
+++ b/thys/UTM.thy	Thu Apr 25 21:37:05 2013 +0100
@@ -1216,8 +1216,8 @@
 
 declare start_of.simps[simp del]
 
-lemma twice_lemma: "rec_exec rec_twice [rs] = 2*rs"
-by(auto simp: rec_twice_def rec_exec.simps)
+lemma twice_lemma: "rec_eval rec_twice [rs] = 2*rs"
+by(auto simp: rec_twice_def rec_eval.simps)
 
 lemma t_twice_correct: 
   "\<exists>stp ln rn. steps0 (Suc 0, Bk # Bk # ires, Oc\<up>(Suc rs) @ Bk\<up>(n)) 
@@ -1227,13 +1227,13 @@
   fix a b c
   assume h: "rec_ci rec_twice = (a, b, c)"
   have "\<exists>stp m l. steps0 (Suc 0, Bk # Bk # ires, <[rs]> @ Bk\<up>(n)) (tm_of abc_twice @ shift (mopup (length [rs])) 
-    (length (tm_of abc_twice) div 2)) stp = (0, Bk\<up>(m) @ Bk # Bk # ires, Oc\<up>(Suc (rec_exec rec_twice [rs])) @ Bk\<up>(l))"
+    (length (tm_of abc_twice) div 2)) stp = (0, Bk\<up>(m) @ Bk # Bk # ires, Oc\<up>(Suc (rec_eval rec_twice [rs])) @ Bk\<up>(l))"
     thm  recursive_compile_to_tm_correct1
   proof(rule_tac recursive_compile_to_tm_correct1)
     show "rec_ci rec_twice = (a, b, c)" by (simp add: h)
   next
-    show "terminate rec_twice [rs]"
-      apply(rule_tac primerec_terminate, auto)
+    show "terminates rec_twice [rs]"
+      apply(rule_tac primerec_terminates, auto)
       apply(simp add: rec_twice_def, auto simp: constn.simps numeral_2_eq_2)
       by(auto)
   next
@@ -1242,7 +1242,7 @@
       by(simp add: abc_twice_def)
   qed
   thus "?thesis"
-    apply(simp add: tape_of_nl_abv tape_of_nat_list.simps tape_of_nat_abv rec_exec.simps twice_lemma)
+    apply(simp add: tape_of_nl_abv tape_of_nat_list.simps tape_of_nat_abv rec_eval.simps twice_lemma)
     done
 qed
 
@@ -2005,8 +2005,8 @@
 apply(auto simp: rec_fourtimes_def numeral_4_eq_4 constn.simps)
 by auto
 
-lemma fourtimes_lemma: "rec_exec rec_fourtimes [rs] = 4 * rs"
-by(simp add: rec_exec.simps rec_fourtimes_def)
+lemma fourtimes_lemma: "rec_eval rec_fourtimes [rs] = 4 * rs"
+by(simp add: rec_eval.simps rec_fourtimes_def)
 
 
 lemma t_fourtimes_correct: 
@@ -2017,13 +2017,13 @@
   fix a b c
   assume h: "rec_ci rec_fourtimes = (a, b, c)"
   have "\<exists>stp m l. steps0 (Suc 0, Bk # Bk # ires, <[rs]> @ Bk\<up>(n)) (tm_of abc_fourtimes @ shift (mopup (length [rs])) 
-    (length (tm_of abc_fourtimes) div 2)) stp = (0, Bk\<up>(m) @ Bk # Bk # ires, Oc\<up>(Suc (rec_exec rec_fourtimes [rs])) @ Bk\<up>(l))"
+    (length (tm_of abc_fourtimes) div 2)) stp = (0, Bk\<up>(m) @ Bk # Bk # ires, Oc\<up>(Suc (rec_eval rec_fourtimes [rs])) @ Bk\<up>(l))"
     thm recursive_compile_to_tm_correct1
   proof(rule_tac recursive_compile_to_tm_correct1)
     show "rec_ci rec_fourtimes = (a, b, c)" by (simp add: h)
   next
-    show "terminate rec_fourtimes [rs]"
-      apply(rule_tac primerec_terminate)
+    show "terminates rec_fourtimes [rs]"
+      apply(rule_tac primerec_terminates)
       by auto
   next
     show "tm_of abc_fourtimes = tm_of (a [+] dummy_abc (length [rs]))"
@@ -4729,19 +4729,19 @@
 proof -
   obtain ap arity fp where a: "rec_ci rec_F = (ap, arity, fp)"
     by (metis prod_cases3) 
-  moreover have b: "rec_exec rec_F [code tp, (bl2wc (<lm>))] = (rs - Suc 0)"
+  moreover have b: "rec_eval rec_F [code tp, (bl2wc (<lm>))] = (rs - Suc 0)"
     using assms
     apply(rule_tac F_correct, simp_all)
     done 
   have "\<exists> stp m l. steps0 (Suc 0, Bk # Bk # [], <[code tp, bl2wc (<lm>)]> @ Bk\<up>i)
     (F_tprog @ shift (mopup (length [code tp, bl2wc (<lm>)])) (length F_tprog div 2)) stp
-    = (0, Bk\<up>m @ Bk # Bk # [], Oc\<up>Suc (rec_exec rec_F [code tp, (bl2wc (<lm>))]) @ Bk\<up>l)"  
+    = (0, Bk\<up>m @ Bk # Bk # [], Oc\<up>Suc (rec_eval rec_F [code tp, (bl2wc (<lm>))]) @ Bk\<up>l)"  
   proof(rule_tac recursive_compile_to_tm_correct1)
     show "rec_ci rec_F = (ap, arity, fp)" using a by simp
   next
-    show "terminate rec_F [code tp, bl2wc (<lm>)]"
+    show "terminates rec_F [code tp, bl2wc (<lm>)]"
       using assms
-      by(rule_tac terminate_F, simp_all)
+      by(rule_tac terminates_F, simp_all)
   next
     show "F_tprog = tm_of (ap [+] dummy_abc (length [code tp, bl2wc (<lm>)]))"
       using a
@@ -4751,14 +4751,14 @@
   then obtain stp m l where 
     "steps0 (Suc 0, Bk # Bk # [], <[code tp, bl2wc (<lm>)]> @ Bk\<up>i)
     (F_tprog @ shift (mopup (length [code tp, (bl2wc (<lm>))])) (length F_tprog div 2)) stp
-    = (0, Bk\<up>m @ Bk # Bk # [], Oc\<up>Suc (rec_exec rec_F [code tp, (bl2wc (<lm>))]) @ Bk\<up>l)" by blast
+    = (0, Bk\<up>m @ Bk # Bk # [], Oc\<up>Suc (rec_eval rec_F [code tp, (bl2wc (<lm>))]) @ Bk\<up>l)" by blast
   hence "\<exists> m. steps0 (Suc 0, [Bk], <[code tp, bl2wc (<lm>)]> @ Bk\<up>i)
     (F_tprog @ shift (mopup 2) (length F_tprog div 2)) stp
     = (0, Bk\<up>m, Oc\<up>Suc (rs - 1) @ Bk\<up>l)"
   proof -
     assume g: "steps0 (Suc 0, [Bk, Bk], <[code tp, bl2wc (<lm>)]> @ Bk \<up> i)
       (F_tprog @ shift (mopup (length [code tp, bl2wc (<lm>)])) (length F_tprog div 2)) stp =
-      (0, Bk \<up> m @ [Bk, Bk], Oc \<up> Suc ((rec_exec rec_F [code tp, bl2wc (<lm>)])) @ Bk \<up> l)"
+      (0, Bk \<up> m @ [Bk, Bk], Oc \<up> Suc ((rec_eval rec_F [code tp, bl2wc (<lm>)])) @ Bk \<up> l)"
    moreover have "tinres [Bk, Bk] [Bk]"
      apply(auto simp: tinres_def)
      done
@@ -4936,7 +4936,7 @@
 done
 
 lemma NSTD_1: "\<not> TSTD (a, b, c)
-    \<Longrightarrow> rec_exec rec_NSTD [trpl_code (a, b, c)] = Suc 0"
+    \<Longrightarrow> rec_eval rec_NSTD [trpl_code (a, b, c)] = Suc 0"
   using NSTD_lemma1[of "trpl_code (a, b, c)"]
        NSTD_lemma2[of "trpl_code (a, b, c)"]
   apply(simp add: TSTD_def)
@@ -4949,10 +4949,10 @@
   "\<lbrakk>tm_wf (tp, 0);
   steps0 (Suc 0, Bk\<up>(l), <lm>) tp stp = (a, b, c);
   \<not> TSTD (a, b, c)\<rbrakk>
-  \<Longrightarrow> rec_exec rec_nonstop [code tp, bl2wc (<lm>), stp] = Suc 0"
-apply(simp add: rec_nonstop_def rec_exec.simps)
+  \<Longrightarrow> rec_eval rec_nonstop [code tp, bl2wc (<lm>), stp] = Suc 0"
+apply(simp add: rec_nonstop_def rec_eval.simps)
 apply(subgoal_tac 
-  "rec_exec rec_conf [code tp, bl2wc (<lm>), stp] =
+  "rec_eval rec_conf [code tp, bl2wc (<lm>), stp] =
   trpl_code (a, b, c)", simp)
 apply(erule_tac NSTD_1)
 using rec_t_eq_steps[of tp l lm stp]
@@ -4962,7 +4962,7 @@
 lemma nonstop_true:
   "\<lbrakk>tm_wf (tp, 0);
   \<forall> stp. (\<not> TSTD (steps0 (Suc 0, Bk\<up>(l), <lm>) tp stp))\<rbrakk>
-  \<Longrightarrow> \<forall>y. rec_exec rec_nonstop ([code tp, bl2wc (<lm>), y]) =  (Suc 0)"
+  \<Longrightarrow> \<forall>y. rec_eval rec_nonstop ([code tp, bl2wc (<lm>), y]) =  (Suc 0)"
 apply(rule_tac allI, erule_tac x = y in allE)
 apply(case_tac "steps0 (Suc 0, Bk\<up>(l), <lm>) tp y", simp)
 apply(rule_tac nonstop_t_uhalt_eq, simp_all)
@@ -5021,11 +5021,11 @@
           using e f
         proof(rule_tac mn_unhalt_case, auto simp: rec_halt_def)
           fix i
-          show "terminate rec_nonstop [code tp, bl2wc (<lm>), i]"
-            by(rule_tac primerec_terminate, auto)
+          show "terminates rec_nonstop [code tp, bl2wc (<lm>), i]"
+            by(rule_tac primerec_terminates, auto)
         next
           fix i
-          show "0 < rec_exec rec_nonstop [code tp, bl2wc (<lm>), i]"
+          show "0 < rec_eval rec_nonstop [code tp, bl2wc (<lm>), i]"
             using assms
             by(drule_tac nonstop_true, auto)
         qed
@@ -5035,22 +5035,22 @@
         assume "j<2" "rec_ci ([recf.id (Suc (Suc 0)) 0, recf.id (Suc (Suc 0)) (Suc 0), Mn (Suc (Suc 0)) rec_nonstop] ! j) = (apj, arj, ftj)"
         hence "{\<lambda>nl. nl = [code tp, bl2wc (<lm>)] @ 0 \<up> (ftj - arj) @ anything} apj
           {\<lambda>nl. nl = [code tp, bl2wc (<lm>)] @
-            rec_exec ([recf.id (Suc (Suc 0)) 0, recf.id (Suc (Suc 0)) (Suc 0), Mn (Suc (Suc 0)) rec_nonstop] ! j) [code tp, bl2wc (<lm>)] # 
+            rec_eval ([recf.id (Suc (Suc 0)) 0, recf.id (Suc (Suc 0)) (Suc 0), Mn (Suc (Suc 0)) rec_nonstop] ! j) [code tp, bl2wc (<lm>)] # 
                0 \<up> (ftj - Suc arj) @ anything}"
           apply(rule_tac recursive_compile_correct)
           apply(case_tac j, auto)
-          apply(rule_tac [!] primerec_terminate)
+          apply(rule_tac [!] primerec_terminates)
           by(auto)
         thus "{\<lambda>nl. nl = code tp # bl2wc (<lm>) # 0 \<up> (ftj - arj) @ anything} apj
-          {\<lambda>nl. nl = code tp # bl2wc (<lm>) # rec_exec ([recf.id (Suc (Suc 0)) 0, recf.id (Suc (Suc 0))
+          {\<lambda>nl. nl = code tp # bl2wc (<lm>) # rec_eval ([recf.id (Suc (Suc 0)) 0, recf.id (Suc (Suc 0))
           (Suc 0), Mn (Suc (Suc 0)) rec_nonstop] ! j) [code tp, bl2wc (<lm>)] # 0 \<up> (ftj - Suc arj) @ anything}"
           by simp
       next
         fix j
         assume "(j::nat) < 2"
-        thus "terminate ([recf.id (Suc (Suc 0)) 0, recf.id (Suc (Suc 0)) (Suc 0), Mn (Suc (Suc 0)) rec_nonstop] ! j)
+        thus "terminates ([recf.id (Suc (Suc 0)) 0, recf.id (Suc (Suc 0)) (Suc 0), Mn (Suc (Suc 0)) rec_nonstop] ! j)
           [code tp, bl2wc (<lm>)]"
-          by(case_tac j, auto intro!: primerec_terminate)
+          by(case_tac j, auto intro!: primerec_terminates)
       qed
       thus "{\<lambda>nl. nl = code tp # bl2wc (<lm>) # 0 \<up> (ft2 - Suc (Suc 0)) @ anything} ap2 \<up>"
         by simp