tm: comparison thys/UF.thy

equal deleted inserted replaced

-:89ed51d72e4a
+:aea02b5a58d2
 *)
 header {* Construction of a Universal Function *}
 theory UF
-imports Rec_Def GCD Abacus "~~/src/HOL/Number_Theory/Primes"
+imports Rec_Def GCD Abacus
 begin
 text {*
 This theory file constructs the Universal Function @{text "rec_F"}, which is the UTM defined
 in terms of recursive functions. This @{text "rec_F"} is essentially an
 [Cn (vl - 1) (constn 0) [id (vl - 1) 0]]))
 (Cn (Suc vl) rec_add [id (Suc vl) vl,
 Cn (Suc vl) rf (get_fstn_args (Suc vl) (vl - 1)
 @ [Cn (Suc vl) s [id (Suc vl) (vl - 1)]])]))"
+text {*
-declare rec_eval.simps[simp del] constn.simps[simp del]
+@{text "rec_exec"} is the interpreter function for
+reursive functions. The function is defined such that
+it always returns meaningful results for primitive recursive
-section {* Correctness of various recursive functions *}
+functions.
+*}
-lemma add_lemma: "rec_eval rec_add [x, y] =  x + y"
+declare rec_exec.simps[simp del] constn.simps[simp del]
-by(induct_tac y, auto simp: rec_add_def rec_eval.simps)
+text {*
-lemma mult_lemma: "rec_eval rec_mult [x, y] = x * y"
+Correctness of @{text "rec_add"}.
-by(induct_tac y, auto simp: rec_mult_def rec_eval.simps add_lemma)
+*}
+lemma add_lemma: "\<And> x y. rec_exec rec_add [x, y] =  x + y"
-lemma pred_lemma: "rec_eval rec_pred [x] =  x - 1"
+by(induct_tac y, auto simp: rec_add_def rec_exec.simps)
-by(induct_tac x, auto simp: rec_pred_def rec_eval.simps)
+text {*
-lemma minus_lemma: "rec_eval rec_minus [x, y] = x - y"
+Correctness of @{text "rec_mult"}.
-by(induct_tac y, auto simp: rec_eval.simps rec_minus_def pred_lemma)
+*}
+lemma mult_lemma: "\<And> x y. rec_exec rec_mult [x, y] = x * y"
-lemma sg_lemma: "rec_eval rec_sg [x] = (if x = 0 then 0 else 1)"
+by(induct_tac y, auto simp: rec_mult_def rec_exec.simps add_lemma)
-by(auto simp: rec_sg_def minus_lemma rec_eval.simps constn.simps)
+text {*
-lemma constn_lemma: "rec_eval (constn n) [x] = n"
+Correctness of @{text "rec_pred"}.
-by(induct n, auto simp: rec_eval.simps constn.simps)
+*}
+lemma pred_lemma: "\<And> x. rec_exec rec_pred [x] =  x - 1"
-lemma less_lemma: "rec_eval rec_less [x, y] = (if x < y then 1 else 0)"
+by(induct_tac x, auto simp: rec_pred_def rec_exec.simps)
-by(induct_tac y, auto simp: rec_eval.simps
+text {*
+Correctness of @{text "rec_minus"}.
+*}
+lemma minus_lemma: "\<And> x y. rec_exec rec_minus [x, y] = x - y"
+by(induct_tac y, auto simp: rec_exec.simps rec_minus_def pred_lemma)
+text {*
+Correctness of @{text "rec_sg"}.
+*}
+lemma sg_lemma: "\<And> x. 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)
+text {*
+Correctness of @{text "constn"}.
+*}
+lemma constn_lemma: "rec_exec (constn n) [x] = n"
+by(induct n, auto simp: rec_exec.simps constn.simps)
+text {*
+Correctness of @{text "rec_less"}.
+*}
+lemma less_lemma: "\<And> x y. rec_exec rec_less [x, y] =
+(if x < y then 1 else 0)"
+by(induct_tac y, auto simp: rec_exec.simps
 rec_less_def minus_lemma sg_lemma)
-lemma not_lemma: "rec_eval rec_not [x] = (if x = 0 then 1 else 0)"
+text {*
-by(induct_tac x, auto simp: rec_eval.simps rec_not_def
+Correctness of @{text "rec_not"}.
+*}
+lemma not_lemma:
+"\<And> x. rec_exec rec_not [x] = (if x = 0 then 1 else 0)"
+by(induct_tac x, auto simp: rec_exec.simps rec_not_def
 constn_lemma minus_lemma)
-lemma eq_lemma: "rec_eval rec_eq [x, y] = (if x = y then 1 else 0)"
+text {*
-by(induct_tac y, auto simp: rec_eval.simps rec_eq_def constn_lemma add_lemma minus_lemma)
+Correctness of @{text "rec_eq"}.
+*}
-lemma conj_lemma: "rec_eval rec_conj [x, y] = (if x = 0 \<or> y = 0 then 0 else 1)"
+lemma eq_lemma: "\<And> x y. rec_exec rec_eq [x, y] = (if x = y then 1 else 0)"
-by(induct_tac y, auto simp: rec_eval.simps sg_lemma rec_conj_def mult_lemma)
+by(induct_tac y, auto simp: rec_exec.simps rec_eq_def constn_lemma add_lemma minus_lemma)
-lemma disj_lemma: "rec_eval rec_disj [x, y] = (if x = 0 \<and> y = 0 then 0 else 1)"
+text {*
-by(induct_tac y, auto simp: rec_disj_def sg_lemma add_lemma rec_eval.simps)
+Correctness of @{text "rec_conj"}.
+*}
-declare mult_lemma[simp] add_lemma[simp] pred_lemma[simp]
+lemma conj_lemma: "\<And> x y. rec_exec rec_conj [x, y] = (if x = 0 \<or> y = 0 then 0
-minus_lemma[simp] sg_lemma[simp] constn_lemma[simp]
+else 1)"
-less_lemma[simp] not_lemma[simp] eq_lemma[simp]
+by(induct_tac y, auto simp: rec_exec.simps sg_lemma rec_conj_def mult_lemma)
-conj_lemma[simp] disj_lemma[simp]
+text {*
-text {*
+Correctness of @{text "rec_disj"}.
-@{text "primrec recf n"} is true iff @{text "recf"} is a primitive
+*}
-recursive function with arity @{text "n"}.
+lemma disj_lemma: "\<And> x y. 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)
+text {*
+@{text "primrec recf n"} is true iff
+@{text "recf"} is a primitive recursive function
+with arity @{text "n"}.
+*}
 inductive primerec :: "recf \<Rightarrow> nat \<Rightarrow> bool"
 where
 prime_z[intro]:  "primerec z (Suc 0)" |
 prime_s[intro]:  "primerec s (Suc 0)" |
 prime_id[intro!]: "\<lbrakk>n < m\<rbrakk> \<Longrightarrow> primerec (id m n) m" |
 inductive_cases prime_s_reverse[elim]: "primerec s n"
 inductive_cases prime_id_reverse[elim]: "primerec (id m n) k"
 inductive_cases prime_cn_reverse[elim]: "primerec (Cn n f gs) m"
 inductive_cases prime_pr_reverse[elim]: "primerec (Pr n f g) m"
+declare mult_lemma[simp] add_lemma[simp] pred_lemma[simp]
+minus_lemma[simp] sg_lemma[simp] constn_lemma[simp]
+less_lemma[simp] not_lemma[simp] eq_lemma[simp]
+conj_lemma[simp] disj_lemma[simp]
 text {*
 @{text "Sigma"} is the logical specification of
 the recursive function @{text "rec_sigma"}.
 *}
 function Sigma :: "(nat list \<Rightarrow> nat) \<Rightarrow> nat list \<Rightarrow> nat"
 where
 "Sigma g xs = (if last xs = 0 then g xs
-else (Sigma g (butlast xs @ [last xs - 1]) + g xs)) "
+else (Sigma g (butlast xs @ [last xs - 1]) +
+g xs)) "
 by pat_completeness auto
 termination
 proof
 show "wf (measure (\<lambda> (f, xs). last xs))" by auto
 next
 fix g xs
 assume "last (xs::nat list) \<noteq> 0"
-thus "((g, butlast xs @ [last xs - 1]), g, xs) \<in> measure (\<lambda>(f, xs). last xs)"
+thus "((g, butlast xs @ [last xs - 1]), g, xs)
+\<in> measure (\<lambda>(f, xs). last xs)"
 by auto
 qed
-declare rec_eval.simps[simp del] get_fstn_args.simps[simp del]
+declare rec_exec.simps[simp del] get_fstn_args.simps[simp del]
 arity.simps[simp del] Sigma.simps[simp del]
 rec_sigma.simps[simp del]
 lemma [simp]: "arity z = 1"
 by(simp add: arity.simps)
 lemma rec_pr_0_simp_rewrite: "
-rec_eval (Pr n f g) (xs @ [0]) = rec_eval f xs"
+rec_exec (Pr n f g) (xs @ [0]) = rec_exec f xs"
-by(simp add: rec_eval.simps)
+by(simp add: rec_exec.simps)
 lemma rec_pr_0_simp_rewrite_single_param: "
-rec_eval (Pr n f g) [0] = rec_eval f []"
+rec_exec (Pr n f g) [0] = rec_exec f []"
-by(simp add: rec_eval.simps)
+by(simp add: rec_exec.simps)
 lemma rec_pr_Suc_simp_rewrite:
-"rec_eval (Pr n f g) (xs @ [Suc x]) = rec_eval g (xs @ [x] @ [rec_eval (Pr n f g) (xs @ [x])])"
+"rec_exec (Pr n f g) (xs @ [Suc x]) =
-by(simp add: rec_eval.simps)
+rec_exec g (xs @ [x] @
+[rec_exec (Pr n f g) (xs @ [x])])"
+by(simp add: rec_exec.simps)
 lemma rec_pr_Suc_simp_rewrite_single_param:
-"rec_eval (Pr n f g) ([Suc x]) = rec_eval g ([x] @ [rec_eval (Pr n f g) ([x])])"
+"rec_exec (Pr n f g) ([Suc x]) =
-by(simp add: rec_eval.simps)
+rec_exec g ([x] @ [rec_exec (Pr n f g) ([x])])"
+by(simp add: rec_exec.simps)
 lemma Sigma_0_simp_rewrite_single_param:
 "Sigma f [0] = f [0]"
 by(simp add: Sigma.simps)
 lemma  [simp]: "(xs @ ys) ! (Suc (length xs)) = ys ! 1"
 by(simp add: nth_append)
 lemma get_fstn_args_take: "\<lbrakk>length xs = m; n \<le> m\<rbrakk> \<Longrightarrow>
-map (\<lambda> f. rec_eval f xs) (get_fstn_args m n)= take n xs"
+map (\<lambda> f. rec_exec 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_eval.simps
+by(simp add: get_fstn_args.simps rec_exec.simps
 take_Suc_conv_app_nth)
 qed
 lemma [simp]: "primerec f n \<Longrightarrow> arity f = n"
 apply(case_tac f)
 apply(erule_tac prime_mn_reverse)
 done
 lemma rec_sigma_Suc_simp_rewrite:
 "primerec f (Suc (length xs))
-\<Longrightarrow> rec_eval (rec_sigma f) (xs @ [Suc x]) =
+\<Longrightarrow> rec_exec (rec_sigma f) (xs @ [Suc x]) =
-rec_eval (rec_sigma f) (xs @ [x]) + rec_eval f (xs @ [Suc x])"
+rec_exec (rec_sigma f) (xs @ [x]) + rec_exec f (xs @ [Suc x])"
 apply(induct x)
 apply(auto simp: rec_sigma.simps Let_def rec_pr_Suc_simp_rewrite
-rec_eval.simps get_fstn_args_take)
+rec_exec.simps get_fstn_args_take)
 done
 text {*
 The correctness of @{text "rec_sigma"} with respect to its specification.
 *}
 lemma sigma_lemma:
 "primerec rg (Suc (length xs))
-\<Longrightarrow> rec_eval (rec_sigma rg) (xs @ [x]) = Sigma (rec_eval rg) (xs @ [x])"
+\<Longrightarrow> rec_exec (rec_sigma rg) (xs @ [x]) = Sigma (rec_exec rg) (xs @ [x])"
 apply(induct x)
-apply(auto simp: rec_eval.simps rec_sigma.simps Let_def
+apply(auto simp: rec_exec.simps rec_sigma.simps Let_def
 get_fstn_args_take Sigma_0_simp_rewrite
 Sigma_Suc_simp_rewrite)
 done
 text {*
 by auto
 qed
 lemma rec_accum_Suc_simp_rewrite:
 "primerec f (Suc (length xs))
-\<Longrightarrow> rec_eval (rec_accum f) (xs @ [Suc x]) =
+\<Longrightarrow> rec_exec (rec_accum f) (xs @ [Suc x]) =
-rec_eval (rec_accum f) (xs @ [x]) * rec_eval f (xs @ [Suc x])"
+rec_exec (rec_accum f) (xs @ [x]) * rec_exec f (xs @ [Suc x])"
 apply(induct x)
 apply(auto simp: rec_sigma.simps Let_def rec_pr_Suc_simp_rewrite
-rec_eval.simps get_fstn_args_take)
+rec_exec.simps get_fstn_args_take)
 done
 text {*
 The correctness of @{text "rec_accum"} with respect to its specification.
 *}
 lemma accum_lemma :
 "primerec rg (Suc (length xs))
-\<Longrightarrow> rec_eval (rec_accum rg) (xs @ [x]) = Accum (rec_eval rg) (xs @ [x])"
+\<Longrightarrow> rec_exec (rec_accum rg) (xs @ [x]) = Accum (rec_exec rg) (xs @ [x])"
 apply(induct x)
-apply(auto simp: rec_eval.simps rec_sigma.simps Let_def
+apply(auto simp: rec_exec.simps rec_sigma.simps Let_def
 get_fstn_args_take)
 done
 declare rec_accum.simps [simp del]
 (let vl = arity rf in
 Cn (vl - 1) rec_sg [Cn (vl - 1) (rec_accum rf)
 (get_fstn_args (vl - 1) (vl - 1) @ [rt])])"
 lemma rec_accum_ex: "primerec rf (Suc (length xs)) \<Longrightarrow>
-(rec_eval (rec_accum rf) (xs @ [x]) = 0) =
+(rec_exec (rec_accum rf) (xs @ [x]) = 0) =
-(\<exists> t \<le> x. rec_eval rf (xs @ [t]) = 0)"
+(\<exists> t \<le> x. rec_exec rf (xs @ [t]) = 0)"
 apply(induct x, simp_all add: rec_accum_Suc_simp_rewrite)
-apply(simp add: rec_eval.simps rec_accum.simps get_fstn_args_take,
+apply(simp add: rec_exec.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)
 apply(rule_tac x = t in exI, simp)
 done
 The correctness of @{text "rec_all"}.
 *}
 lemma all_lemma:
 "\<lbrakk>primerec rf (Suc (length xs));
 primerec rt (length xs)\<rbrakk>
-\<Longrightarrow> rec_eval (rec_all rt rf) xs = (if (\<forall> x \<le> (rec_eval rt xs). 0 < rec_eval rf (xs @ [x])) then 1
+\<Longrightarrow> rec_exec (rec_all rt rf) xs = (if (\<forall> x \<le> (rec_exec rt xs). 0 < rec_exec rf (xs @ [x])) then 1
 else 0)"
 apply(auto simp: rec_all.simps)
-apply(simp add: rec_eval.simps map_append get_fstn_args_take split: if_splits)
+apply(simp add: rec_exec.simps map_append get_fstn_args_take split: if_splits)
-apply(drule_tac x = "rec_eval rt xs" in rec_accum_ex)
+apply(drule_tac x = "rec_exec rt xs" in rec_accum_ex)
-apply(case_tac "rec_eval (rec_accum rf) (xs @ [rec_eval rt xs]) = 0", simp_all)
+apply(case_tac "rec_exec (rec_accum rf) (xs @ [rec_exec rt xs]) = 0", simp_all)
 apply(erule_tac exE, erule_tac x = t in allE, simp)
-apply(simp add: rec_eval.simps map_append get_fstn_args_take)
+apply(simp add: rec_exec.simps map_append get_fstn_args_take)
-apply(drule_tac x = "rec_eval rt xs" in rec_accum_ex)
+apply(drule_tac x = "rec_exec rt xs" in rec_accum_ex)
-apply(case_tac "rec_eval (rec_accum rf) (xs @ [rec_eval rt xs]) = 0", simp, simp)
+apply(case_tac "rec_exec (rec_accum rf) (xs @ [rec_exec rt xs]) = 0", simp, simp)
 apply(erule_tac x = x in allE, simp)
 done
 text {*
 @{text "rec_ex t f (x1, x2, \<dots>, xn)"}
 (let vl = arity rf in
 Cn (vl - 1) rec_sg [Cn (vl - 1) (rec_sigma rf)
 (get_fstn_args (vl - 1) (vl - 1) @ [rt])])"
 lemma rec_sigma_ex: "primerec rf (Suc (length xs))
-\<Longrightarrow> (rec_eval (rec_sigma rf) (xs @ [x]) = 0) =
+\<Longrightarrow> (rec_exec (rec_sigma rf) (xs @ [x]) = 0) =
-(\<forall> t \<le> x. rec_eval rf (xs @ [t]) = 0)"
+(\<forall> t \<le> x. rec_exec rf (xs @ [t]) = 0)"
 apply(induct x, simp_all add: rec_sigma_Suc_simp_rewrite)
-apply(simp add: rec_eval.simps rec_sigma.simps
+apply(simp add: rec_exec.simps rec_sigma.simps
 get_fstn_args_take, auto)
 apply(case_tac "t = Suc x", simp_all)
 done
 text {*
 The correctness of @{text "ex_lemma"}.
 *}
 lemma ex_lemma:"
 \<lbrakk>primerec rf (Suc (length xs));
 primerec rt (length xs)\<rbrakk>
-\<Longrightarrow> (rec_eval (rec_ex rt rf) xs =
+\<Longrightarrow> (rec_exec (rec_ex rt rf) xs =
-(if (\<exists> x \<le> (rec_eval rt xs). 0 <rec_eval rf (xs @ [x])) then 1
+(if (\<exists> x \<le> (rec_exec rt xs). 0 <rec_exec rf (xs @ [x])) then 1
 else 0))"
-apply(auto simp: rec_ex.simps rec_eval.simps map_append get_fstn_args_take
+apply(auto simp: rec_ex.simps rec_exec.simps map_append get_fstn_args_take
 split: if_splits)
-apply(drule_tac x = "rec_eval 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_exec rt xs" in rec_sigma_ex, simp)
 done
 text {*
 Definition of @{text "Min[R]"} on page 77 of Boolos's book.
 *}
 else if (Rr (xs @ [Suc w])) then (Suc w)
 else Suc (Suc w))"
 by(insert Minr_range[of Rr xs w], auto)
 text {*
-@{text "rec_Minmr"} is the recursive function
+@{text "rec_Minr"} 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
 implement @{text "Minr Rr"}
 *}
 fun rec_Minr :: "recf \<Rightarrow> recf"
 where
 "rec_Minr rf =
 (let vl = arity rf
-in let rq = rec_all (id vl (vl - 1))
+in let rq = rec_all (id vl (vl - 1)) (Cn (Suc vl)
-(Cn (Suc vl) rec_not [Cn (Suc vl) rf
+rec_not [Cn (Suc vl) rf
-(get_fstn_args (Suc vl) (vl - 1) @ [id (Suc vl) vl])])
+(get_fstn_args (Suc vl) (vl - 1) @
+[id (Suc vl) (vl)])])
 in  rec_sigma rq)"
 lemma length_getpren_params[simp]: "length (get_fstn_args m n) = n"
 by(induct n, auto simp: get_fstn_args.simps)
 apply(simp add: rec_not_def)
 apply(rule prime_cn, auto)
 apply(case_tac i, auto intro: prime_id)
 done
-lemma Min_false1[simp]: "\<lbrakk>\<not> Min {uu. uu \<le> w \<and> 0 < rec_eval rf (xs @ [uu])} \<le> w;
+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_eval rf (xs @ [x])\<rbrakk>
+x \<le> w; 0 < rec_exec rf (xs @ [x])\<rbrakk>
 \<Longrightarrow>  False"
-apply(subgoal_tac "finite {uu. uu \<le> w \<and> 0 < rec_eval rf (xs @ [uu])}")
+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_eval rf (xs @ [uu])} \<noteq> {}")
+apply(subgoal_tac "{uu. uu \<le> w \<and> 0 < rec_exec rf (xs @ [uu])} \<noteq> {}")
 apply(simp add: Min_le_iff, simp)
 apply(rule_tac x = x in exI, simp)
 apply(simp)
 done
 lemma sigma_minr_lemma:
 assumes prrf:  "primerec rf (Suc (length xs))"
-shows "UF.Sigma (rec_eval (rec_all (recf.id (Suc (length xs)) (length xs))
+shows "UF.Sigma (rec_exec (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_eval rf args) xs w"
+Minr (\<lambda>args. 0 < rec_exec rf args) xs w"
 proof(induct w)
 let ?rt = "(recf.id (Suc (length xs)) ((length xs)))"
 let ?rf = "(Cn (Suc (Suc (length xs)))
 rec_not [Cn (Suc (Suc (length xs))) rf
 (get_fstn_args (Suc (Suc (length xs))) (length xs) @
 let ?rq = "(rec_all ?rt ?rf)"
 have prrf: "primerec ?rf (Suc (length (xs @ [0]))) \<and>
 primerec ?rt (length (xs @ [0]))"
 apply(auto simp: prrf nth_append)+
 done
-show "Sigma (rec_eval (rec_all ?rt ?rf)) (xs @ [0])
+show "Sigma (rec_exec (rec_all ?rt ?rf)) (xs @ [0])
-= Minr (\<lambda>args. 0 < rec_eval rf args) xs 0"
+= Minr (\<lambda>args. 0 < rec_exec rf args) xs 0"
 apply(simp add: Sigma.simps)
 apply(simp only: prrf all_lemma,
-auto simp: rec_eval.simps get_fstn_args_take Minr.simps)
+auto simp: rec_exec.simps get_fstn_args_take Minr.simps)
 apply(rule_tac Min_eqI, auto)
 done
 next
 fix w
 let ?rt = "(recf.id (Suc (length xs)) ((length xs)))"
 (get_fstn_args (Suc (Suc (length xs))) (length xs) @
 [recf.id (Suc (Suc (length xs)))
 (Suc ((length xs)))])])"
 let ?rq = "(rec_all ?rt ?rf)"
 assume ind:
-"Sigma (rec_eval (rec_all ?rt ?rf)) (xs @ [w]) = Minr (\<lambda>args. 0 < rec_eval rf args) xs w"
+"Sigma (rec_exec (rec_all ?rt ?rf)) (xs @ [w]) = Minr (\<lambda>args. 0 < rec_exec 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_eval (rec_all ?rt ?rf))
+show "UF.Sigma (rec_exec (rec_all ?rt ?rf))
 (xs @ [Suc w]) =
-Minr (\<lambda>args. 0 < rec_eval rf args) xs (Suc w)"
+Minr (\<lambda>args. 0 < rec_exec 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_eval.simps get_fstn_args_take Let_def Minr.simps split: if_splits)
+apply(auto simp: rec_exec.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)
 apply(drule_tac Min_false1, simp, simp, simp)
 done
 qed
 text {*
 The correctness of @{text "rec_Minr"}.
 *}
-lemma Minr_lemma:
+lemma Minr_lemma: "
-assumes h: "primerec rf (Suc (length xs))"
+\<lbrakk>primerec rf (Suc (length xs))\<rbrakk>
-shows "rec_eval (rec_Minr rf) (xs @ [w]) = Minr (\<lambda> args. (0 < rec_eval rf args)) xs w"
+\<Longrightarrow> rec_exec (rec_Minr rf) (xs @ [w]) =
+Minr (\<lambda> args. (0 < rec_exec rf args)) xs w"
 proof -
 let ?rt = "(recf.id (Suc (length xs)) ((length xs)))"
 let ?rf = "(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)))])])"
 let ?rq = "(rec_all ?rt ?rf)"
+assume h: "primerec rf (Suc (length xs))"
 have h1: "primerec ?rq (Suc (length xs))"
 apply(rule_tac primerec_all_iff)
 apply(auto simp: h nth_append)+
 done
 moreover have "arity rf = Suc (length xs)"
 using h by auto
-ultimately show "rec_eval (rec_Minr rf) (xs @ [w]) = Minr (\<lambda> args. (0 < rec_eval rf args)) xs w"
+ultimately show "rec_exec (rec_Minr rf) (xs @ [w]) =
-apply(simp add: rec_eval.simps rec_Minr.simps arity.simps Let_def
+Minr (\<lambda> args. (0 < rec_exec rf args)) xs w"
+apply(simp add: rec_exec.simps rec_Minr.simps arity.simps Let_def
 sigma_lemma all_lemma)
 apply(rule_tac  sigma_minr_lemma)
 apply(simp add: h)
 done
 qed
 text {*
 The correctness of @{text "rec_le"}.
 *}
 lemma le_lemma:
-"rec_eval rec_le [x, y] = (if (x \<le> y) then 1 else 0)"
+"\<And>x y. rec_exec rec_le [x, y] = (if (x \<le> y) then 1 else 0)"
-by(auto simp: rec_le_def rec_eval.simps)
+by(auto simp: rec_le_def rec_exec.simps)
 text {*
 Definition of @{text "Max[Rr]"} on page 77 of Boolos's book.
 *}
 fun rec_maxr :: "recf \<Rightarrow> recf"
 where
 "rec_maxr rr = (let vl = arity rr in
 let rt = id (Suc vl) (vl - 1) in
 let rf1 = Cn (Suc (Suc vl)) rec_le
-[id (Suc (Suc vl)) (Suc vl), id (Suc (Suc vl)) vl] in
+[id (Suc (Suc vl))
+((Suc vl)), id (Suc (Suc vl)) (vl)] in
 let rf2 = Cn (Suc (Suc vl)) rec_not
 [Cn (Suc (Suc vl))
 rr (get_fstn_args (Suc (Suc vl))
 (vl - 1) @
-[id (Suc (Suc vl)) (Suc vl)])] in
+[id (Suc (Suc vl)) ((Suc vl))])] in
 let rf = Cn (Suc (Suc vl)) rec_disj [rf1, rf2] in
 let Qf = Cn (Suc vl) rec_not [rec_all rt rf]
 in Cn vl (rec_sigma Qf) (get_fstn_args vl vl @
 [id vl (vl - 1)]))"
 apply(rule_tac prime_cn, auto)
 apply(case_tac i, auto)
 done
 lemma [simp]:
-"length ys = Suc n \<Longrightarrow> (take n ys @ [ys ! n, ys ! n]) = ys @ [ys ! n]"
+"length ys = Suc n \<Longrightarrow> (take n ys @ [ys ! n, ys ! n]) =
+ys @ [ys ! n]"
 apply(simp)
 apply(subgoal_tac "\<exists> xs y. ys = xs @ [y]", auto)
 apply(rule_tac x = "butlast ys" in exI, rule_tac x = "last ys" in exI)
 apply(case_tac "ys = []", simp_all)
 done
 lemma Maxr_Suc_simp:
-"Maxr Rr xs (Suc w) =(if Rr (xs @ [Suc w]) then Suc w else Maxr Rr xs w)"
+"Maxr Rr xs (Suc w) =(if Rr (xs @ [Suc w]) then Suc w
+else Maxr Rr xs w)"
 apply(auto simp: Maxr.simps Max.insert)
 apply(rule_tac Max_eqI, auto)
 done
 lemma [simp]: "min (Suc n) n = n" by simp
-lemma Sigma_0: "\<forall> i \<le> n. (f (xs @ [i]) = 0) \<Longrightarrow> Sigma f (xs @ [n]) = 0"
+lemma Sigma_0: "\<forall> i \<le> n. (f (xs @ [i]) = 0) \<Longrightarrow>
+Sigma f (xs @ [n]) = 0"
 apply(induct n, simp add: Sigma.simps)
 apply(simp add: Sigma_Suc_simp_rewrite)
 done
-lemma [elim]: "\<forall>k<Suc w. f (xs @ [k]) = Suc 0 \<Longrightarrow> Sigma f (xs @ [w]) = Suc w"
+lemma [elim]: "\<forall>k<Suc w. f (xs @ [k]) = Suc 0
+\<Longrightarrow> Sigma f (xs @ [w]) = Suc w"
 apply(induct w)
 apply(simp add: Sigma.simps, simp)
 apply(simp add: Sigma.simps)
 done
 apply(case_tac "ma = Suc w", auto)
 done
 lemma Sigma_Max_lemma:
 assumes prrf: "primerec rf (Suc (length xs))"
-shows "UF.Sigma (rec_eval (Cn (Suc (Suc (length xs))) rec_not
+shows "UF.Sigma (rec_exec (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
 [recf.id (Suc (Suc (Suc (length xs)))) (Suc (Suc (length xs))),
 recf.id (Suc (Suc (Suc (length xs)))) (Suc (length xs))],
 Cn (Suc (Suc (Suc (length xs)))) rec_not
 [Cn (Suc (Suc (Suc (length xs)))) rf
 (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_eval rf args) xs w"
+Maxr (\<lambda>args. 0 < rec_exec rf args) xs w"
 proof -
 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))))
 ((Suc (Suc (length xs)))), recf.id
 let ?rf = "Cn (Suc (Suc (Suc (length xs)))) rec_disj [?rf1, ?rf3]"
 let ?rq = "rec_all ?rt ?rf"
 let ?notrq = "Cn (Suc (Suc (length xs))) rec_not [?rq]"
 show "?thesis"
 proof(auto simp: Maxr.simps)
-assume h: "\<forall>x\<le>w. rec_eval rf (xs @ [x]) = 0"
+assume h: "\<forall>x\<le>w. rec_exec rf (xs @ [x]) = 0"
 have "primerec ?rf (Suc (length (xs @ [w, i]))) \<and>
 primerec ?rt (length (xs @ [w, i]))"
 using prrf
 apply(auto)
 apply(case_tac i, auto)
 apply(case_tac ia, auto simp: h nth_append)
 done
-hence "Sigma (rec_eval ?notrq) ((xs@[w])@[w]) = 0"
+hence "Sigma (rec_exec ?notrq) ((xs@[w])@[w]) = 0"
 apply(rule_tac Sigma_0)
-apply(auto simp: rec_eval.simps all_lemma
+apply(auto simp: rec_exec.simps all_lemma
 get_fstn_args_take nth_append h)
 done
-thus "UF.Sigma (rec_eval ?notrq)
+thus "UF.Sigma (rec_exec ?notrq)
 (xs @ [w, w]) = 0"
 by simp
 next
 fix x
-assume h: "x \<le> w" "0 < rec_eval rf (xs @ [x])"
+assume h: "x \<le> w" "0 < rec_exec rf (xs @ [x])"
-hence "\<exists> ma. Max {y. y \<le> w \<and> 0 < rec_eval rf (xs @ [y])} = ma"
+hence "\<exists> ma. Max {y. y \<le> w \<and> 0 < rec_exec rf (xs @ [y])} = ma"
 by auto
 from this obtain ma where k1:
-"Max {y. y \<le> w \<and> 0 < rec_eval rf (xs @ [y])} = ma" ..
+"Max {y. y \<le> w \<and> 0 < rec_exec rf (xs @ [y])} = ma" ..
-hence k2: "ma \<le> w \<and> 0 < rec_eval rf (xs @ [ma])"
+hence k2: "ma \<le> w \<and> 0 < rec_exec rf (xs @ [ma])"
 using h
 apply(subgoal_tac
-"Max {y. y \<le> w \<and> 0 < rec_eval rf (xs @ [y])} \<in>  {y. y \<le> w \<and> 0 < rec_eval rf (xs @ [y])}")
+"Max {y. y \<le> w \<and> 0 < rec_exec rf (xs @ [y])} \<in>  {y. y \<le> w \<and> 0 < rec_exec rf (xs @ [y])}")
 apply(erule_tac CollectE, simp)
 apply(rule_tac Max_in, auto)
 done
-hence k3: "\<forall> k < ma. (rec_eval ?notrq (xs @ [w, k]) = 1)"
+hence k3: "\<forall> k < ma. (rec_exec ?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_eval.simps all_lemma get_fstn_args_take nth_append)
+apply(auto simp: rec_exec.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_eval ?notrq (xs @ [w, k]) = 0)"
+have k4: "\<forall> k \<ge> ma. (rec_exec ?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_eval.simps all_lemma get_fstn_args_take nth_append)
+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_eval rf (xs @ [y])}",
+apply(subgoal_tac "x \<le> Max {y. y \<le> w \<and> 0 < rec_exec 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_eval ?notrq) ((xs @ [w]) @ [w]) = ma"
+from k3 k4 k1 have "Sigma (rec_exec ?notrq) ((xs @ [w]) @ [w]) = ma"
 apply(rule_tac Sigma_max_point, simp, simp, simp add: k2)
 done
-from k1 and this show "Sigma (rec_eval ?notrq) (xs @ [w, w]) =
+from k1 and this show "Sigma (rec_exec ?notrq) (xs @ [w, w]) =
-Max {y. y \<le> w \<and> 0 < rec_eval rf (xs @ [y])}"
+Max {y. y \<le> w \<and> 0 < rec_exec rf (xs @ [y])}"
 by simp
 qed
 qed
 text {*
 The correctness of @{text "rec_maxr"}.
 *}
 lemma Maxr_lemma:
 assumes h: "primerec rf (Suc (length xs))"
-shows   "rec_eval (rec_maxr rf) (xs @ [w]) =
+shows   "rec_exec (rec_maxr rf) (xs @ [w]) =
-Maxr (\<lambda> args. 0 < rec_eval rf args) xs w"
+Maxr (\<lambda> args. 0 < rec_exec rf args) xs w"
 proof -
 from h have "arity rf = Suc (length xs)"
 by auto
 thus "?thesis"
-proof(simp add: rec_eval.simps rec_maxr.simps nth_append get_fstn_args_take)
+proof(simp add: rec_exec.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))))
 ((Suc (Suc (length xs)))), recf.id
 (Suc (Suc (Suc (length xs)))) ((Suc (length xs)))]"
 from prt and prrf have prrq: "primerec ?rq
 (Suc (Suc (length xs)))"
 by(erule_tac primerec_all_iff, auto)
 hence prnotrp: "primerec ?notrq (Suc (length ((xs @ [w]))))"
 by(rule_tac prime_cn, auto)
-have g1: "rec_eval (rec_sigma ?notrq) ((xs @ [w]) @ [w])
+have g1: "rec_exec (rec_sigma ?notrq) ((xs @ [w]) @ [w])
-= Maxr (\<lambda>args. 0 < rec_eval rf args) xs w"
+= Maxr (\<lambda>args. 0 < rec_exec 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_eval (rec_sigma ?notrq)
+thus "rec_exec (rec_sigma ?notrq)
 (xs @ [w, w]) =
-Maxr (\<lambda>args. 0 < rec_eval rf args) xs w"
+Maxr (\<lambda>args. 0 < rec_exec rf args) xs w"
 apply(simp)
 done
 qed
 qed
 text {*
 @{text "quo"} is the formal specification of division.
 *}
 fun quo :: "nat list \<Rightarrow> nat"
 where
-"quo [x, y] =
+"quo [x, y] = (let Rr =
-(let Rr = (\<lambda> zs. ((zs ! (Suc 0) * zs ! (Suc (Suc 0)) \<le> zs ! 0) \<and> zs ! Suc 0 \<noteq> 0))
+(\<lambda> zs. ((zs ! (Suc 0) * zs ! (Suc (Suc 0))
-in Maxr Rr [x, y] x)"
+\<le> zs ! 0) \<and> zs ! Suc 0 \<noteq> (0::nat)))
+in Maxr Rr [x, y] x)"
 declare quo.simps[simp del]
 text {*
 The following lemmas shows more directly the menaing of @{text "quo"}:
 two arguments are not equal.
 *}
 definition rec_noteq:: "recf"
 where
 "rec_noteq = Cn (Suc (Suc 0)) rec_not [Cn (Suc (Suc 0))
-rec_eq [id (Suc (Suc 0)) (0), id (Suc (Suc 0)) ((Suc 0))]]"
+rec_eq [id (Suc (Suc 0)) (0), id (Suc (Suc 0))
+((Suc 0))]]"
 text {*
 The correctness of @{text "rec_noteq"}.
 *}
 lemma noteq_lemma:
-"rec_eval rec_noteq [x, y] = (if x \<noteq> y then 1 else 0)"
+"\<And> x y. rec_exec rec_noteq [x, y] =
-by(simp add: rec_eval.simps rec_noteq_def)
+(if x \<noteq> y then 1 else 0)"
+by(simp add: rec_exec.simps rec_noteq_def)
 declare noteq_lemma[simp]
 text {*
 @{text "rec_quo"} is the recursive function used to implement @{text "quo"}
 apply(rule_tac prime_cn, auto)+
 apply(case_tac i, auto intro: prime_id)
 done
-lemma quo_lemma1: "rec_eval rec_quo [x, y] = quo [x, y]"
+lemma quo_lemma1: "rec_exec rec_quo [x, y] = quo [x, y]"
-proof(simp add: rec_eval.simps rec_quo_def)
+proof(simp add: rec_exec.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
 [recf.id (Suc (Suc (Suc 0))) (Suc (0)),
 recf.id (Suc (Suc (Suc 0))) (Suc (Suc (0)))],
 recf.id (Suc (Suc (Suc 0))) (0)],
 Cn (Suc (Suc (Suc 0))) rec_noteq
 [recf.id (Suc (Suc (Suc 0)))
 (Suc (0)), Cn (Suc (Suc (Suc 0))) (constn 0)
 [recf.id (Suc (Suc (Suc 0))) (0)]]])"
-have "rec_eval (rec_maxr ?rR) ([x, y]@ [ x]) = Maxr (\<lambda> args. 0 < rec_eval ?rR args) [x, y] x"
+have "rec_exec (rec_maxr ?rR) ([x, y]@ [ x]) = Maxr (\<lambda> args. 0 < rec_exec ?rR args) [x, y] x"
 proof(rule_tac Maxr_lemma, simp)
 show "primerec ?rR (Suc (Suc (Suc 0)))"
 apply(auto)
 apply(case_tac i, auto)
 apply(case_tac [!] ia, auto)
 apply(case_tac i, auto)
 done
 qed
-hence g1: "rec_eval (rec_maxr ?rR) ([x, y,  x]) =
+hence g1: "rec_exec (rec_maxr ?rR) ([x, y,  x]) =
-Maxr (\<lambda> args. if rec_eval ?rR args = 0 then False
+Maxr (\<lambda> args. if rec_exec ?rR args = 0 then False
 else True) [x, y] x"
 by simp
-have g2: "Maxr (\<lambda> args. if rec_eval ?rR args = 0 then False
+have g2: "Maxr (\<lambda> args. if rec_exec ?rR args = 0 then False
 else True) [x, y] x = quo [x, y]"
-apply(simp add: rec_eval.simps)
+apply(simp add: rec_exec.simps)
 apply(simp add: Maxr.simps quo.simps, auto)
 done
 from g1 and g2 show
-"rec_eval (rec_maxr ?rR) ([x, y,  x]) = quo [x, y]"
+"rec_exec (rec_maxr ?rR) ([x, y,  x]) = quo [x, y]"
 by simp
 qed
 text {*
 The correctness of @{text "quo"}.
 *}
-lemma quo_lemma2: "rec_eval rec_quo [x, y] = x div y"
+lemma quo_lemma2: "rec_exec rec_quo [x, y] = x div y"
 using quo_lemma1[of x y] quo_div[of x y]
 by simp
 text {*
 @{text "rec_mod"} is the recursive function used to implement
 (Suc (0))]]"
 text {*
 The correctness of @{text "rec_mod"}:
 *}
-lemma mod_lemma: "rec_eval rec_mod [x, y] = (x mod y)"
+lemma mod_lemma: "\<And> x y. rec_exec rec_mod [x, y] = (x mod y)"
-proof(simp add: rec_eval.simps rec_mod_def quo_lemma2)
+proof(simp add: rec_exec.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]
 apply(subgoal_tac "y * (x div y) = (x div y ) * y", arith, simp)
 done
 qed
-section {* Embranch Function *}
+text{* lemmas for embranch function*}
 type_synonym ftype = "nat list \<Rightarrow> nat"
 type_synonym rtype = "nat list \<Rightarrow> bool"
 text {*
 The specifation of the mutli-way branching statement on
 rec_embranch' ((rg, rc) # rgcs) vl)"
 declare Embranch.simps[simp del] rec_embranch.simps[simp del]
 lemma embranch_all0:
-"\<lbrakk>\<forall> j < length rcs. rec_eval (rcs ! j) xs = 0;
+"\<lbrakk>\<forall> j < length rcs. rec_exec (rcs ! j) xs = 0;
 length rgs = length rcs;
 rcs \<noteq> [];
 list_all (\<lambda> rf. primerec rf (length xs)) (rgs @ rcs)\<rbrakk>  \<Longrightarrow>
-rec_eval (rec_embranch (zip rgs rcs)) xs = 0"
+rec_exec (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_eval (rcs ! j) xs = 0;
+"\<And>rgs. \<lbrakk>\<forall>j<length rcs. rec_exec (rcs ! j) xs = 0;
 length rgs = length rcs; rcs \<noteq> [];
 list_all (\<lambda>rf. primerec rf (length xs)) (rgs @ rcs)\<rbrakk> \<Longrightarrow>
-rec_eval (rec_embranch (zip rgs rcs)) xs = 0"
+rec_exec (rec_embranch (zip rgs rcs)) xs = 0"
-and h:  "\<forall>j<length (a # rcs). rec_eval ((a # rcs) ! j) xs = 0"
+and h:  "\<forall>j<length (a # rcs). rec_exec ((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_eval (rec_embranch (zip list rcs)) xs = 0"
+have g: "rcs \<noteq> [] \<Longrightarrow> rec_exec (rec_embranch (zip list rcs)) xs = 0"
 using h
 by(rule_tac ind, auto)
-show "rec_eval (rec_embranch (zip rgs (a # rcs))) xs = 0"
+show "rec_exec (rec_embranch (zip rgs (a # rcs))) xs = 0"
 proof(case_tac "rcs = []", simp)
-show "rec_eval (rec_embranch (zip rgs [a])) xs = 0"
+show "rec_exec (rec_embranch (zip rgs [a])) xs = 0"
 using h
-apply(simp add: rec_embranch.simps rec_eval.simps)
+apply(simp add: rec_embranch.simps rec_exec.simps)
 apply(erule_tac x = 0 in allE, simp)
 done
 next
 assume "rcs \<noteq> []"
-hence "rec_eval (rec_embranch (zip list rcs)) xs = 0"
+hence "rec_exec (rec_embranch (zip list rcs)) xs = 0"
 using g by simp
-thus "rec_eval (rec_embranch (zip rgs (a # rcs))) xs = 0"
+thus "rec_exec (rec_embranch (zip rgs (a # rcs))) xs = 0"
 using h
-apply(simp add: rec_embranch.simps rec_eval.simps)
+apply(simp add: rec_embranch.simps rec_exec.simps)
 apply(case_tac rcs,
-auto simp: rec_eval.simps rec_embranch.simps)
+auto simp: rec_exec.simps rec_embranch.simps)
 apply(case_tac list,
-auto simp: rec_eval.simps rec_embranch.simps)
+auto simp: rec_exec.simps rec_embranch.simps)
 done
 qed
 qed
-lemma embranch_exec_0: "\<lbrakk>rec_eval aa xs = 0; zip rgs list \<noteq> [];
+lemma embranch_exec_0: "\<lbrakk>rec_exec aa xs = 0; zip rgs list \<noteq> [];
 list_all (\<lambda> rf. primerec rf (length xs)) ([a, aa] @ rgs @ list)\<rbrakk>
-\<Longrightarrow> rec_eval (rec_embranch ((a, aa) # zip rgs list)) xs
+\<Longrightarrow> rec_exec (rec_embranch ((a, aa) # zip rgs list)) xs
-= rec_eval (rec_embranch (zip rgs list)) xs"
+= rec_exec (rec_embranch (zip rgs list)) xs"
-apply(simp add: rec_eval.simps rec_embranch.simps)
+apply(simp add: rec_exec.simps rec_embranch.simps)
 apply(case_tac "zip rgs list", simp, case_tac ab,
-simp add: rec_embranch.simps rec_eval.simps)
+simp add: rec_embranch.simps rec_exec.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)
 done
 apply(case_tac xs, simp, simp)
 done
 lemma Embranch_0:
 "\<lbrakk>length rgs = k; length rcs = k; k > 0;
-\<forall> j < k. rec_eval (rcs ! j) xs = 0\<rbrakk> \<Longrightarrow>
+\<forall> j < k. rec_exec (rcs ! j) xs = 0\<rbrakk> \<Longrightarrow>
-Embranch (zip (map rec_eval rgs) (map (\<lambda>r args. 0 < rec_eval r args) rcs)) xs = 0"
+Embranch (zip (map rec_exec rgs) (map (\<lambda>r args. 0 < rec_exec 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_eval (rcs ! j) xs = 0\<rbrakk>
+"\<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_eval rgs) (map (\<lambda>r args. 0 < rec_eval r args) rcs)) xs = 0"
+\<Longrightarrow> Embranch (zip (map rec_exec rgs) (map (\<lambda>r args. 0 < rec_exec r args) rcs)) xs = 0"
 and h: "Suc (length rgs) = k" "length rcs = k"
-"\<forall>j<k. rec_eval (rcs ! j) xs = 0"
+"\<forall>j<k. rec_exec (rcs ! j) xs = 0"
 from h show
-"Embranch (zip (rec_eval a # map rec_eval rgs)
+"Embranch (zip (rec_exec a # map rec_exec rgs)
-(map (\<lambda>r args. 0 < rec_eval r args) rcs)) xs = 0"
+(map (\<lambda>r args. 0 < rec_exec 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)
 apply(simp add: Embranch.simps)
 apply(erule_tac x = 0 in all_dupE, simp)
 *}
 lemma embranch_lemma:
 assumes branch_num:
 "length rgs = n" "length rcs = n" "n > 0"
 and partition:
-"(\<exists> i < n. (rec_eval (rcs ! i) xs = 1 \<and> (\<forall> j < n. j \<noteq> i \<longrightarrow>
+"(\<exists> i < n. (rec_exec (rcs ! i) xs = 1 \<and> (\<forall> j < n. j \<noteq> i \<longrightarrow>
-rec_eval (rcs ! j) xs = 0)))"
+rec_exec (rcs ! j) xs = 0)))"
 and prime_all: "list_all (\<lambda> rf. primerec rf (length xs)) (rgs @ rcs)"
-shows "rec_eval (rec_embranch (zip rgs rcs)) xs =
+shows "rec_exec (rec_embranch (zip rgs rcs)) xs =
-Embranch (zip (map rec_eval rgs)
+Embranch (zip (map rec_exec rgs)
-(map (\<lambda> r args. 0 < rec_eval r args) rcs)) xs"
+(map (\<lambda> r args. 0 < rec_exec 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_eval (rcs ! i) xs = 1 \<and> (\<forall>j<n. j \<noteq> i \<longrightarrow> rec_eval (rcs ! j) xs = 0);
+\<exists>i<n. rec_exec (rcs ! i) xs = 1 \<and> (\<forall>j<n. j \<noteq> i \<longrightarrow> rec_exec (rcs ! j) xs = 0);
 list_all (\<lambda>rf. primerec rf (length xs)) (rgs @ rcs)\<rbrakk>
-\<Longrightarrow> rec_eval (rec_embranch (zip rgs rcs)) xs =
+\<Longrightarrow> rec_exec (rec_embranch (zip rgs rcs)) xs =
-Embranch (zip (map rec_eval rgs) (map (\<lambda>r args. 0 < rec_eval r args) rcs)) xs"
+Embranch (zip (map rec_exec rgs) (map (\<lambda>r args. 0 < rec_exec r args) rcs)) xs"
 and h: "length (a # rgs) = n" "length (rcs::recf list) = n" "0 < n"
-" \<exists>i<n. rec_eval (rcs ! i) xs = 1 \<and>
+" \<exists>i<n. rec_exec (rcs ! i) xs = 1 \<and>
-(\<forall>j<n. j \<noteq> i \<longrightarrow> rec_eval (rcs ! j) xs = 0)"
+(\<forall>j<n. j \<noteq> i \<longrightarrow> rec_exec (rcs ! j) xs = 0)"
 "list_all (\<lambda>rf. primerec rf (length xs)) ((a # rgs) @ rcs)"
-from h show "rec_eval (rec_embranch (zip (a # rgs) rcs)) xs =
+from h show "rec_exec (rec_embranch (zip (a # rgs) rcs)) xs =
-Embranch (zip (map rec_eval (a # rgs)) (map (\<lambda>r args.
+Embranch (zip (map rec_exec (a # rgs)) (map (\<lambda>r args.
-0 < rec_eval r args) rcs)) xs"
+0 < rec_exec r args) rcs)) xs"
 apply(case_tac rcs, simp, simp)
-apply(case_tac "rec_eval aa xs = 0")
+apply(case_tac "rec_exec aa xs = 0")
 apply(case_tac [!] "zip rgs list = []", simp)
-apply(subgoal_tac "rgs = [] \<and> list = []", simp add: Embranch.simps rec_eval.simps rec_embranch.simps)
+apply(subgoal_tac "rgs = [] \<and> list = []", simp add: Embranch.simps rec_exec.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_eval ((aa # list) ! i) xs = Suc 0 \<and>
+"\<exists>i<n. rec_exec ((aa # list) ! i) xs = Suc 0 \<and>
-(\<forall>j<n. j \<noteq> i \<longrightarrow> rec_eval ((aa # list) ! j) xs = 0)"
+(\<forall>j<n. j \<noteq> i \<longrightarrow> rec_exec ((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_eval aa xs = 0" "rcs = aa # list" "zip rgs list \<noteq> []"
+"rec_exec aa xs = 0" "rcs = aa # list" "zip rgs list \<noteq> []"
-have "rec_eval (rec_embranch ((a, aa) # zip rgs list)) xs
+have "rec_exec (rec_embranch ((a, aa) # zip rgs list)) xs
-= rec_eval (rec_embranch (zip rgs list)) xs"
+= rec_exec (rec_embranch (zip rgs list)) xs"
 apply(rule embranch_exec_0, simp_all add: g)
 done
-from g and this show "rec_eval (rec_embranch ((a, aa) # zip rgs list)) xs =
+from g and this show "rec_exec (rec_embranch ((a, aa) # zip rgs list)) xs =
-Embranch ((rec_eval a, \<lambda>args. 0 < rec_eval aa args) #
+Embranch ((rec_exec a, \<lambda>args. 0 < rec_exec aa args) #
-zip (map rec_eval rgs) (map (\<lambda>r args. 0 < rec_eval r args) list)) xs"
+zip (map rec_exec rgs) (map (\<lambda>r args. 0 < rec_exec r args) list)) xs"
 apply(simp add: Embranch.simps)
 apply(rule_tac n = "n - Suc 0" in ind)
 apply(case_tac n, simp, simp)
 apply(case_tac n, simp, simp)
 apply(case_tac n, simp, simp add: zip_null_gr )
 apply(rule_tac allI, erule_tac x = "Suc j" in allE, simp)
 done
 next
 fix aa list
 assume g: "Suc (length rgs) = n" "Suc (length list) = n"
-"\<exists>i<n. rec_eval ((aa # list) ! i) xs = Suc 0 \<and>
+"\<exists>i<n. rec_exec ((aa # list) ! i) xs = Suc 0 \<and>
-(\<forall>j<n. j \<noteq> i \<longrightarrow> rec_eval ((aa # list) ! j) xs = 0)"
+(\<forall>j<n. j \<noteq> i \<longrightarrow> rec_exec ((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_eval aa xs \<noteq> 0" "zip rgs list = []"
+"rcs = aa # list" "rec_exec aa xs \<noteq> 0" "zip rgs list = []"
-thus "rec_eval (rec_embranch ((a, aa) # zip rgs list)) xs =
+thus "rec_exec (rec_embranch ((a, aa) # zip rgs list)) xs =
-Embranch ((rec_eval a, \<lambda>args. 0 < rec_eval aa args) #
+Embranch ((rec_exec a, \<lambda>args. 0 < rec_exec aa args) #
-zip (map rec_eval rgs) (map (\<lambda>r args. 0 < rec_eval r args) list)) xs"
+zip (map rec_exec rgs) (map (\<lambda>r args. 0 < rec_exec 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_eval.simps rec_embranch.simps Embranch.simps, auto)
+apply(simp add: rec_exec.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_eval ((aa # list) ! i) xs = Suc 0 \<and>
+"\<exists>i<n. rec_exec ((aa # list) ! i) xs = Suc 0 \<and>
-(\<forall>j<n. j \<noteq> i \<longrightarrow> rec_eval ((aa # list) ! j) xs = 0)"
+(\<forall>j<n. j \<noteq> i \<longrightarrow> rec_exec ((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_eval aa xs \<noteq> 0" "zip rgs list \<noteq> []"
+"rcs = aa # list" "rec_exec aa xs \<noteq> 0" "zip rgs list \<noteq> []"
-have "rec_eval aa xs =  Suc 0"
+have "rec_exec aa xs =  Suc 0"
 using g
-apply(case_tac "rec_eval aa xs", simp, auto)
+apply(case_tac "rec_exec aa xs", simp, auto)
 done
-moreover have "rec_eval (rec_embranch' (zip rgs list) (length xs)) xs = 0"
+moreover have "rec_exec (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
 apply(case_tac "zip rgs list", simp, case_tac ab)
 apply(simp add: rec_embranch.simps)
 apply(subgoal_tac "arity aaa = length xs", simp, auto)
 apply(case_tac rgs, simp, simp, case_tac list, simp, simp)
 done
-moreover have "rec_eval (rec_embranch (zip rgs list)) xs = 0"
+moreover have "rec_exec (rec_embranch (zip rgs list)) xs = 0"
 proof(rule embranch_all0)
-show " \<forall>j<length list. rec_eval (list ! j) xs = 0"
+show " \<forall>j<length list. rec_exec (list ! j) xs = 0"
 using g
 apply(auto)
 apply(case_tac i, simp)
 apply(erule_tac x = "Suc j" in allE, simp)
 apply(simp)
 show "list_all (\<lambda>rf. primerec rf (length xs)) (rgs @ list)"
 using g
 apply auto
 done
 qed
-ultimately show "rec_eval (rec_embranch' (zip rgs list) (length xs)) xs = 0"
+ultimately show "rec_exec (rec_embranch' (zip rgs list) (length xs)) xs = 0"
 by simp
 qed
 moreover have
-"Embranch (zip (map rec_eval rgs)
+"Embranch (zip (map rec_exec rgs)
-(map (\<lambda>r args. 0 < rec_eval r args) list)) xs = 0"
+(map (\<lambda>r args. 0 < rec_exec r args) list)) xs = 0"
 using g
 apply(rule_tac k = "length rgs" in Embranch_0)
 apply(simp, case_tac n, simp, simp)
 apply(case_tac rgs, simp, simp)
 apply(auto)
 done
 moreover have "arity a = length xs"
 using g
 apply(auto)
 done
-ultimately show "rec_eval (rec_embranch ((a, aa) # zip rgs list)) xs =
+ultimately show "rec_exec (rec_embranch ((a, aa) # zip rgs list)) xs =
-Embranch ((rec_eval a, \<lambda>args. 0 < rec_eval aa args) #
+Embranch ((rec_exec a, \<lambda>args. 0 < rec_exec aa args) #
-zip (map rec_eval rgs) (map (\<lambda>r args. 0 < rec_eval r args) list)) xs"
+zip (map rec_exec rgs) (map (\<lambda>r args. 0 < rec_exec r args) list)) xs"
-apply(simp add: rec_eval.simps rec_embranch.simps Embranch.simps)
+apply(simp add: rec_exec.simps rec_embranch.simps Embranch.simps)
 done
 qed
 qed
+text{*
+@{text "prime n"} means @{text "n"} is a prime number.
+*}
+fun Prime :: "nat \<Rightarrow> bool"
+where
+"Prime x = (1 < x \<and> (\<forall> u < x. (\<forall> v < x. u * v \<noteq> x)))"
+declare Prime.simps [simp del]
 lemma primerec_all1:
 "primerec (rec_all rt rf) n \<Longrightarrow> primerec rt n"
 by (simp add: primerec_all)
 [Cn 3 rec_mult [id 3 1, id 3 2], id 3 0]))]"
 declare numeral_2_eq_2[simp del] numeral_3_eq_3[simp del]
 lemma exec_tmp:
-"rec_eval (rec_all (Cn 2 rec_minus [recf.id 2 0, Cn 2 (constn (Suc 0)) [recf.id 2 0]])
+"rec_exec (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_eval (Cn 2 rec_minus [recf.id 2 0, Cn 2 (constn (Suc 0)) [recf.id 2 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_eval (Cn 3 rec_noteq [Cn 3 rec_mult [recf.id 3 (Suc 0), recf.id 3 2], recf.id 3 0])
+0 < rec_exec (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)
 apply(case_tac [!] i, auto)
 apply(case_tac ia, auto simp: numeral_3_eq_3 numeral_2_eq_2)
 done
 text {*
 The correctness of @{text "Prime"}.
 *}
-lemma prime_lemma: "rec_eval rec_prime [x] = (if prime x then 1 else 0)"
+lemma prime_lemma: "rec_exec rec_prime [x] = (if Prime x then 1 else 0)"
-proof(simp add: rec_eval.simps rec_prime_def)
+proof(simp add: rec_exec.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
 [recf.id 3 (Suc 0), recf.id 3 2], recf.id 3 (0)])"
 let ?rt2 = "(Cn (Suc 0) rec_minus
 [recf.id (Suc 0) 0, constn (Suc 0)])"
 let ?rf2 = "rec_all ?rt1 ?rf1"
-have h1: "rec_eval (rec_all ?rt2 ?rf2) ([x]) =
+have h1: "rec_exec (rec_all ?rt2 ?rf2) ([x]) =
-(if (\<forall>k\<le>rec_eval ?rt2 ([x]). 0 < rec_eval ?rf2 ([x] @ [k])) then 1 else 0)"
+(if (\<forall>k\<le>rec_exec ?rt2 ([x]). 0 < rec_exec ?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)
 apply(auto)
 apply(case_tac [!] i, auto simp: numeral_2_eq_2)
 apply(auto)
 apply(case_tac i, auto)
 done
 qed
 from h1 show
-"(Suc 0 < x \<longrightarrow>  (rec_eval (rec_all ?rt2 ?rf2) [x] = 0 \<longrightarrow>
+"(Suc 0 < x \<longrightarrow>  (rec_exec (rec_all ?rt2 ?rf2) [x] = 0 \<longrightarrow>
-\<not> prime x) \<and>
+\<not> Prime x) \<and>
-(0 < rec_eval (rec_all ?rt2 ?rf2) [x] \<longrightarrow> 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_eval (rec_all ?rt2 ?rf2) [x] = 0
+(\<not> Suc 0 < x \<longrightarrow> \<not> Prime x \<and> (rec_exec (rec_all ?rt2 ?rf2) [x] = 0
-\<longrightarrow> \<not> prime x))"
+\<longrightarrow> \<not> Prime x))"
-apply(auto simp:rec_eval.simps)
+apply(auto simp:rec_exec.simps)
-apply(simp add: exec_tmp rec_eval.simps)
+apply(simp add: exec_tmp rec_exec.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"
+thus "Prime x"
-apply(simp add: rec_eval.simps split: if_splits)
+apply(simp add: rec_exec.simps split: if_splits)
-apply(simp add: prime_nat_def dvd_def, auto)
+apply(simp add: Prime.simps, auto)
-apply(erule_tac x = m in allE, auto)
+apply(erule_tac x = u in allE, auto)
-apply(case_tac m, simp, case_tac nat, simp, simp)
+apply(case_tac u, simp, case_tac nat, simp, simp)
-apply(case_tac k, simp, case_tac nat, simp, simp)
+apply(case_tac v, simp, case_tac nat, simp, simp)
 done
 next
-assume "\<not> Suc 0 < x" "prime x"
+assume "\<not> Suc 0 < x" "Prime x"
 thus "False"
-by (simp add: prime_nat_def)
+apply(simp add: Prime.simps)
+done
 next
 fix k
-assume "rec_eval (rec_all ?rt1 ?rf1)
+assume "rec_exec (rec_all ?rt1 ?rf1)
-[x, k] = 0" "k \<le> x - Suc 0" "prime x"
+[x, k] = 0" "k \<le> x - Suc 0" "Prime x"
 thus "False"
-by (auto simp add: exec_tmp rec_eval.simps prime_nat_def dvd_def split: if_splits)
+apply(simp add: exec_tmp rec_exec.simps Prime.simps split: if_splits)
+done
 next
 fix k
-assume "rec_eval (rec_all ?rt1 ?rf1)
+assume "rec_exec (rec_all ?rt1 ?rf1)
-[x, k] = 0" "k \<le> x - Suc 0" "prime x"
+[x, k] = 0" "k \<le> x - Suc 0" "Prime x"
 thus "False"
-by(auto simp add: exec_tmp rec_eval.simps prime_nat_def dvd_def split: if_splits)
+apply(simp add: exec_tmp rec_exec.simps Prime.simps split: if_splits)
+done
 qed
 qed
 definition rec_dummyfac :: "recf"
 where
-"rec_dummyfac = Pr 1 (constn 1) (Cn 3 rec_mult [id 3 2, Cn 3 s [id 3 1]])"
+"rec_dummyfac = Pr 1 (constn 1)
+(Cn 3 rec_mult [id 3 2, Cn 3 s [id 3 1]])"
 text {*
 The recursive function used to implment factorization.
 *}
 definition rec_fac :: "recf"
 fun fac :: "nat \<Rightarrow> nat"  ("_!" [100] 99)
 where
 "fac 0 = 1" |
 "fac (Suc x) = (Suc x) * fac x"
-lemma [simp]: "rec_eval rec_dummyfac [0, 0] = Suc 0"
+lemma [simp]: "rec_exec rec_dummyfac [0, 0] = Suc 0"
-by(simp add: rec_dummyfac_def rec_eval.simps)
+by(simp add: rec_dummyfac_def rec_exec.simps)
-lemma rec_cn_simp:
+lemma rec_cn_simp: "rec_exec (Cn n f gs) xs =
-"rec_eval (Cn n f gs) xs = (let rgs = map (\<lambda> g. rec_eval g xs) gs in rec_eval f rgs)"
+(let rgs = map (\<lambda> g. rec_exec g xs) gs in
-by(simp add: rec_eval.simps)
+rec_exec f rgs)"
+by(simp add: rec_exec.simps)
-lemma rec_id_simp: "rec_eval (id m n) xs = xs ! n"
-by(simp add: rec_eval.simps)
+lemma rec_id_simp: "rec_exec (id m n) xs = xs ! n"
+by(simp add: rec_exec.simps)
-lemma fac_dummy: "rec_eval rec_dummyfac [x, y] = y !"
+lemma fac_dummy: "rec_exec rec_dummyfac [x, y] = y !"
 apply(induct y)
-apply(auto simp: rec_dummyfac_def rec_eval.simps)
+apply(auto simp: rec_dummyfac_def rec_exec.simps)
 done
 text {*
 The correctness of @{text "rec_fac"}.
 *}
-lemma fac_lemma: "rec_eval rec_fac [x] =  x!"
+lemma fac_lemma: "rec_exec rec_fac [x] =  x!"
-apply(simp add: rec_fac_def rec_eval.simps fac_dummy)
+apply(simp add: rec_fac_def rec_exec.simps fac_dummy)
 done
 declare fac.simps[simp del]
 text {*
 @{text "Np x"} returns the first prime number after @{text "x"}.
 *}
 fun Np ::"nat \<Rightarrow> nat"
 where
-"Np x = Min {y. y \<le> Suc (x!) \<and> x < y \<and> prime y}"
+"Np x = Min {y. y \<le> Suc (x!) \<and> x < y \<and> Prime y}"
 declare Np.simps[simp del] rec_Minr.simps[simp del]
 text {*
 @{text "rec_np"} is the recursive function used to implement
 apply(simp add: fac.simps)
 apply(case_tac n, auto simp: fac.simps)
 done
 lemma divsor_ex:
-"\<lbrakk>\<not> prime x; x > Suc 0\<rbrakk> \<Longrightarrow> (\<exists> u > Suc 0. (\<exists> v > Suc 0. u * v = x))"
+"\<lbrakk>\<not> Prime x; x > Suc 0\<rbrakk> \<Longrightarrow> (\<exists> u > Suc 0. (\<exists> v > Suc 0. u * v = x))"
-apply(auto simp: prime_nat_def dvd_def)
+by(auto simp: Prime.simps)
-by (metis Suc_lessI mult_0 nat_mult_commute neq0_conv)
+lemma divsor_prime_ex: "\<lbrakk>\<not> Prime x; x > Suc 0\<rbrakk> \<Longrightarrow>
+\<exists> p. Prime p \<and> p dvd x"
-lemma divsor_prime_ex: "\<lbrakk>\<not> prime x; x > Suc 0\<rbrakk> \<Longrightarrow>
-\<exists> p. prime p \<and> p dvd x"
 apply(induct x rule: wf_induct[where r = "measure (\<lambda> y. y)"], simp)
 apply(drule_tac divsor_ex, simp, auto)
 apply(erule_tac x = u in allE, simp)
-apply(case_tac "prime u", simp)
+apply(case_tac "Prime u", simp)
 apply(rule_tac x = u in exI, simp, auto)
 done
 lemma [intro]: "0 < n!"
 apply(induct n)
 from this obtain d where "d > 0 \<and> ka = d + k" ..
 from h2 and this and h1 show "False"
 by(simp add: add_mult_distrib2)
 qed
-lemma prime_ex: "\<exists> p. n < p \<and> p \<le> Suc (n!) \<and> prime p"
+lemma prime_ex: "\<exists> p. n < p \<and> p \<le> Suc (n!) \<and> Prime p"
-proof(cases "prime (n! + 1)")
+proof(cases "Prime (n! + 1)")
 case True thus "?thesis"
 by(rule_tac x = "Suc (n!)" in exI, simp)
 next
-assume h: "\<not> prime (n! + 1)"
+assume h: "\<not> Prime (n! + 1)"
-hence "\<exists> p. prime p \<and> p dvd (n! + 1)"
+hence "\<exists> p. Prime p \<and> p dvd (n! + 1)"
 by(erule_tac divsor_prime_ex, auto)
-from this obtain q where k: "prime q \<and> q dvd (n! + 1)" ..
+from this obtain q where k: "Prime q \<and> q dvd (n! + 1)" ..
 thus "?thesis"
 proof(cases "q > n")
 case True thus "?thesis"
 using k
 apply(rule_tac x = q in exI, auto)
 next
 case False thus "?thesis"
 proof -
 assume g: "\<not> n < q"
 have j: "q > Suc 0"
-using k by(case_tac q, auto simp: prime_nat_def dvd_def)
+using k by(case_tac q, auto simp: Prime.simps)
 hence "q dvd n!"
 using g
 apply(rule_tac fac_dvd, auto)
 done
 hence "\<not> q dvd Suc (n!)"
 done
 text {*
 The correctness of @{text "rec_np"}.
 *}
-lemma np_lemma: "rec_eval rec_np [x] = Np x"
+lemma np_lemma: "rec_exec rec_np [x] = Np x"
-proof(auto simp: rec_np_def rec_eval.simps Let_def fac_lemma)
+proof(auto simp: rec_np_def rec_exec.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)"
+let ?R = "\<lambda> zs. zs ! 0 < zs ! 1 \<and> Prime (zs ! 1)"
-have g1: "rec_eval (rec_Minr ?rr) ([x] @ [Suc (x!)]) =
+have g1: "rec_exec (rec_Minr ?rr) ([x] @ [Suc (x!)]) =
-Minr (\<lambda> args. 0 < rec_eval ?rr args) [x] (Suc (x!))"
+Minr (\<lambda> args. 0 < rec_exec ?rr args) [x] (Suc (x!))"
-by(rule_tac Minr_lemma, auto simp: rec_eval.simps
+by(rule_tac Minr_lemma, auto simp: rec_exec.simps
 prime_lemma, auto simp:  numeral_2_eq_2 numeral_3_eq_3)
-have g2: "Minr (\<lambda> args. 0 < rec_eval ?rr args) [x] (Suc (x!)) = Np x"
+have g2: "Minr (\<lambda> args. 0 < rec_exec ?rr args) [x] (Suc (x!)) = Np x"
 using prime_ex[of x]
-apply(auto simp: Minr.simps Np.simps rec_eval.simps)
+apply(auto simp: Minr.simps Np.simps rec_exec.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}
+"{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)
+= {y. y \<le> Suc (x!) \<and> x < y \<and> Prime y}", auto)
 done
-from g1 and g2 show "rec_eval (rec_Minr ?rr) ([x, Suc (x!)]) = Np x"
+from g1 and g2 show "rec_exec (rec_Minr ?rr) ([x, Suc (x!)]) = Np x"
 by simp
 qed
 text {*
 @{text "rec_power"} is the recursive function used to implement
 "rec_power = Pr 1 (constn 1) (Cn 3 rec_mult [id 3 0, id 3 2])"
 text {*
 The correctness of @{text "rec_power"}.
 *}
-lemma power_lemma: "rec_eval rec_power [x, y] = x^y"
+lemma power_lemma: "rec_exec rec_power [x, y] = x^y"
-by(induct y, auto simp: rec_eval.simps rec_power_def)
+by(induct y, auto simp: rec_exec.simps rec_power_def)
 text{*
 @{text "Pi k"} returns the @{text "k"}-th prime number.
 *}
 fun Pi :: "nat \<Rightarrow> nat"
 *}
 definition rec_pi :: "recf"
 where
 "rec_pi = Cn 1 rec_dummy_pi [id 1 0, id 1 0]"
-lemma pi_dummy_lemma: "rec_eval rec_dummy_pi [x, y] = Pi y"
+lemma pi_dummy_lemma: "rec_exec rec_dummy_pi [x, y] = Pi y"
 apply(induct y)
-by(auto simp: rec_eval.simps rec_dummy_pi_def Pi.simps np_lemma)
+by(auto simp: rec_exec.simps rec_dummy_pi_def Pi.simps np_lemma)
 text {*
 The correctness of @{text "rec_pi"}.
 *}
-lemma pi_lemma: "rec_eval rec_pi [x] = Pi x"
+lemma pi_lemma: "rec_exec rec_pi [x] = Pi x"
-apply(simp add: rec_pi_def rec_eval.simps pi_dummy_lemma)
+apply(simp add: rec_pi_def rec_exec.simps pi_dummy_lemma)
 done
 fun loR :: "nat list \<Rightarrow> bool"
 where
 "loR [x, y, u] = (x mod (y^u) = 0)"
 in Cn 2 rec_add [Cn 2 rec_mult [rb, rcond],
 Cn 2 rec_mult [Cn 2 (constn 0) [id 2 0], rcond2]])"
 lemma rec_lo_Maxr_lor:
 "\<lbrakk>Suc 0 < x; Suc 0 < y\<rbrakk> \<Longrightarrow>
-rec_eval rec_lo [x, y] = Maxr loR [x, y] x"
+rec_exec rec_lo [x, y] = Maxr loR [x, y] x"
-proof(auto simp: rec_eval.simps rec_lo_def Let_def
+proof(auto simp: rec_exec.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_eval (rec_maxr ?rR) ([x, y] @ [x]) =
+have h: "rec_exec (rec_maxr ?rR) ([x, y] @ [x]) =
-Maxr (\<lambda> args. 0 < rec_eval ?rR args) [x, y] x"
+Maxr (\<lambda> args. 0 < rec_exec ?rR args) [x, y] x"
-by(rule_tac Maxr_lemma, auto simp: rec_eval.simps
+by(rule_tac Maxr_lemma, auto simp: rec_exec.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_eval ?rR args) [x, y] x"
+have "Maxr loR [x, y] x =  Maxr (\<lambda> args. 0 < rec_exec ?rR args) [x, y] x"
-apply(simp add: rec_eval.simps mod_lemma power_lemma)
+apply(simp add: rec_exec.simps mod_lemma power_lemma)
 apply(simp add: Maxr.simps loR.simps)
 done
-from h and this show "rec_eval (rec_maxr ?rR) [x, y, x] =
+from h and this show "rec_exec (rec_maxr ?rR) [x, y, x] =
 Maxr loR [x, y] x"
 apply(simp)
 done
 qed
 apply(simp add: Maxr.simps lo.simps, auto)
 apply(erule_tac x = xa in allE, simp, simp add: uplimit_loR)
 done
 lemma lo_lemma': "\<lbrakk>Suc 0 < x; Suc 0 < y\<rbrakk> \<Longrightarrow>
-rec_eval rec_lo [x, y] = lo x y"
+rec_exec 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_eval rec_lo [x, y] = lo x y"
+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_eval.simps rec_lo_def
+apply(case_tac x, auto simp: rec_exec.simps rec_lo_def
 Let_def lo.simps)
 done
-lemma lo_lemma''': "\<lbrakk>\<not> Suc 0 < y\<rbrakk> \<Longrightarrow> rec_eval rec_lo [x, y] = lo x y"
+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_eval.simps rec_lo_def
+apply(case_tac y, auto simp: rec_exec.simps rec_lo_def
 Let_def lo.simps)
 done
 text {*
 The correctness of @{text "rec_lo"}:
 *}
-lemma lo_lemma: "rec_eval rec_lo [x, y] = lo x y"
+lemma lo_lemma: "rec_exec 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
 fun lgR :: "nat list \<Rightarrow> bool"
 text {*
 @{text "rec_lg"} is the recursive function used to implement @{text "lg"}.
 *}
 definition rec_lg :: "recf"
 where
-"rec_lg =
+"rec_lg = (let rec_lgR = Cn 3 rec_le
-(let rec_lgR = Cn 3 rec_le [Cn 3 rec_power [id 3 1, id 3 2], id 3 0] in
+[Cn 3 rec_power [id 3 1, id 3 2], id 3 0] in
-let conR1 = Cn 2 rec_conj [Cn 2 rec_less [Cn 2 (constn 1) [id 2 0], id 2 0],
+let conR1 = Cn 2 rec_conj [Cn 2 rec_less
-Cn 2 rec_less [Cn 2 (constn 1) [id 2 0], id 2 1]] in
+[Cn 2 (constn 1) [id 2 0], id 2 0],
-let conR2 = Cn 2 rec_not [conR1] in
+Cn 2 rec_less [Cn 2 (constn 1)
-Cn 2 rec_add [Cn 2 rec_mult [conR1, Cn 2 (rec_maxr rec_lgR)
+[id 2 0], id 2 1]] in
-[id 2 0, id 2 1, id 2 0]],
+let conR2 = Cn 2 rec_not [conR1] in
-Cn 2 rec_mult [conR2, Cn 2 (constn 0) [id 2 0]]])"
+Cn 2 rec_add [Cn 2 rec_mult
+[conR1, Cn 2 (rec_maxr rec_lgR)
+[id 2 0, id 2 1, id 2 0]],
+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_eval rec_lg [x, y] = Maxr lgR [x, y] x"
+rec_exec rec_lg [x, y] = Maxr lgR [x, y] x"
-proof(simp add: rec_eval.simps rec_lg_def Let_def)
+proof(simp add: rec_exec.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_eval (rec_maxr ?rR) ([x, y] @ [x])
+have "rec_exec (rec_maxr ?rR) ([x, y] @ [x])
-= Maxr ((\<lambda> args. 0 < rec_eval ?rR args)) [x, y] x"
+= Maxr ((\<lambda> args. 0 < rec_exec ?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_eval ?rR args)) [x, y] x"
+moreover have "Maxr lgR [x, y] x = Maxr ((\<lambda> args. 0 < rec_exec ?rR args)) [x, y] x"
-apply(simp add: rec_eval.simps power_lemma)
+apply(simp add: rec_exec.simps power_lemma)
 apply(simp add: Maxr.simps lgR.simps)
 done
-ultimately show "rec_eval (rec_maxr ?rR) [x, y, x] = Maxr lgR [x, y] x"
+ultimately show "rec_exec (rec_maxr ?rR) [x, y, x] = Maxr lgR [x, y] x"
 by simp
 qed
 lemma [simp]: "\<lbrakk>Suc 0 < y; lgR [x, y, xa]\<rbrakk> \<Longrightarrow> xa \<le> x"
 apply(simp add: lgR.simps)
 lemma maxr_lg: "\<lbrakk>Suc 0 < x; Suc 0 < y\<rbrakk> \<Longrightarrow> Maxr lgR [x, y] x = lg x y"
 apply(simp add: lg.simps Maxr.simps, auto)
 apply(erule_tac x = xa in allE, simp)
 done
-lemma lg_lemma': "\<lbrakk>Suc 0 < x; Suc 0 < y\<rbrakk> \<Longrightarrow> rec_eval rec_lg [x, y] = lg x y"
+lemma lg_lemma': "\<lbrakk>Suc 0 < x; Suc 0 < y\<rbrakk> \<Longrightarrow> rec_exec rec_lg [x, y] = lg x y"
 apply(simp add: maxr_lg lg_maxr)
 done
-lemma lg_lemma'': "\<not> Suc 0 < x \<Longrightarrow> rec_eval rec_lg [x, y] = lg x y"
+lemma lg_lemma'': "\<not> Suc 0 < x \<Longrightarrow> rec_exec rec_lg [x, y] = lg x y"
-apply(simp add: rec_eval.simps rec_lg_def Let_def lg.simps)
+apply(simp add: rec_exec.simps rec_lg_def Let_def lg.simps)
 done
-lemma lg_lemma''': "\<not> Suc 0 < y \<Longrightarrow> rec_eval rec_lg [x, y] = lg x y"
+lemma lg_lemma''': "\<not> Suc 0 < y \<Longrightarrow> rec_exec rec_lg [x, y] = lg x y"
-apply(simp add: rec_eval.simps rec_lg_def Let_def lg.simps)
+apply(simp add: rec_exec.simps rec_lg_def Let_def lg.simps)
 done
 text {*
 The correctness of @{text "rec_lg"}.
 *}
-lemma lg_lemma: "rec_eval rec_lg [x, y] = lg x y"
+lemma lg_lemma: "rec_exec 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
 text {*
 declare Pi.simps[simp del]
 text {*
 The correctness of @{text "rec_entry"}.
 *}
-lemma entry_lemma: "rec_eval rec_entry [str, i] = Entry str i"
+lemma entry_lemma: "rec_exec rec_entry [str, i] = Entry str i"
-by(simp add: rec_entry_def  rec_eval.simps lo_lemma pi_lemma)
+by(simp add: rec_entry_def  rec_exec.simps lo_lemma pi_lemma)
 subsection {* The construction of F *}
 text {*
 | "rec_listsum2 vl (Suc n) = Cn vl rec_add [rec_listsum2 vl n, id vl n]"
 declare listsum2.simps[simp del] rec_listsum2.simps[simp del]
 lemma listsum2_lemma: "\<lbrakk>length xs = vl; n \<le> vl\<rbrakk> \<Longrightarrow>
-rec_eval (rec_listsum2 vl n) xs = listsum2 xs n"
+rec_exec (rec_listsum2 vl n) xs = listsum2 xs n"
 apply(induct n, simp_all)
-apply(simp_all add: rec_eval.simps rec_listsum2.simps listsum2.simps)
+apply(simp_all add: rec_exec.simps rec_listsum2.simps listsum2.simps)
 done
 fun strt' :: "nat list \<Rightarrow> nat \<Rightarrow> nat"
 where
 "strt' xs 0 = 0"
 Cn vl rec_power [Cn vl (constn 2) [id vl 0], rec_dbound]]])"
 declare strt'.simps[simp del] rec_strt'.simps[simp del]
 lemma strt'_lemma: "\<lbrakk>length xs = vl; n \<le> vl\<rbrakk> \<Longrightarrow>
-rec_eval (rec_strt' vl n) xs = strt' xs n"
+rec_exec (rec_strt' vl n) xs = strt' xs n"
 apply(induct n)
-apply(simp_all add: rec_eval.simps rec_strt'.simps strt'.simps
+apply(simp_all add: rec_exec.simps rec_strt'.simps strt'.simps
 Let_def power_lemma listsum2_lemma)
 done
 text {*
 @{text "strt"} corresponds to the @{text "strt"} function on page 90 of B book, but
 fun rec_strt :: "nat \<Rightarrow> recf"
 where
 "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_eval a xs) \<circ> (\<lambda>i. Cn vl s [recf.id vl i]))
+map ((\<lambda>a. rec_exec 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_eval.simps)
+apply(induct vl arbitrary: xs, simp, auto simp: rec_exec.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_eval a xs) \<circ> (\<lambda>i. Cn (length ys) s
+map ((\<lambda>a. rec_exec 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_eval a (ys @ [y])) \<circ> (\<lambda>i. Cn (Suc (length ys)) s
+"map ((\<lambda>a. rec_exec 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_eval a ys) \<circ> (\<lambda>i. Cn (length ys) s
+have "map ((\<lambda>a. rec_exec 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_eval a (ys @ [y])) \<circ> (\<lambda>i. Cn (Suc (length ys)) s
+"map ((\<lambda>a. rec_exec a (ys @ [y])) \<circ> (\<lambda>i. Cn (Suc (length ys)) s
 [recf.id (Suc (length ys)) (i)])) [0..<length ys]
-= map ((\<lambda>a. rec_eval a ys) \<circ> (\<lambda>i. Cn (length ys) s
+= map ((\<lambda>a. rec_exec 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_eval.simps nth_append)
+apply(rule_tac map_ext, auto simp: rec_exec.simps nth_append)
 done
 ultimately show "?thesis"
 by simp
 qed
 next
 text {*
 The correctness of @{text "rec_strt"}.
 *}
 lemma strt_lemma: "length xs = vl \<Longrightarrow>
-rec_eval (rec_strt vl) xs = strt xs"
+rec_exec (rec_strt vl) xs = strt xs"
-apply(simp add: strt.simps rec_eval.simps strt'_lemma)
+apply(simp add: strt.simps rec_exec.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])
+apply(subgoal_tac "(map ((\<lambda>a. rec_exec 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
 text {*
 where "rec_scan = Cn 1 rec_mod [id 1 0, constn 2]"
 text {*
 The correctness of @{text "scan"}.
 *}
-lemma scan_lemma: "rec_eval rec_scan [r] = r mod 2"
+lemma scan_lemma: "rec_exec rec_scan [r] = r mod 2"
-by(simp add: rec_eval.simps rec_scan_def mod_lemma)
+by(simp add: rec_exec.simps rec_scan_def mod_lemma)
 fun newleft0 :: "nat list \<Rightarrow> nat"
 where
 "newleft0 [p, r] = p"
 text {*
 The correctness of @{text "rec_newleft"}.
 *}
 lemma newleft_lemma:
-"rec_eval rec_newleft [p, r, a] = newleft p r a"
+"rec_exec 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]"
 let ?rrs =
 "[Cn 3 rec_disj [Cn 3 rec_eq [recf.id 3 2, Cn 3 (constn 0)
 [recf.id 3 0]], Cn 3 rec_eq [recf.id 3 2, Cn 3 (constn 1) [recf.id 3 0]]],
 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_eval (rec_embranch (zip ?rgs ?rrs)) [p, r, a]
+have k1: "rec_exec (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]"
+= Embranch (zip (map rec_exec ?rgs) (map (\<lambda>r args. 0 < rec_exec 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)+
 apply(case_tac "a = 0 \<or> a = 1", rule_tac x = 0 in exI)
 prefer 2
 apply(case_tac "a = 2", rule_tac x = "Suc 0" in exI)
 prefer 2
 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_eval.simps)
+apply(auto simp: rec_exec.simps)
-apply(erule_tac [!] Suc_Suc_Suc_Suc_induct, auto simp: rec_eval.simps)
+apply(erule_tac [!] Suc_Suc_Suc_Suc_induct, auto simp: rec_exec.simps)
 done
-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"
+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"
 apply(simp add: Embranch.simps)
-apply(simp add: rec_eval.simps)
+apply(simp add: rec_exec.simps)
-apply(auto simp: newleft.simps rec_newleft0_def rec_eval.simps
+apply(auto simp: newleft.simps rec_newleft0_def rec_exec.simps
 rec_newleft1_def rec_newleft2_def rec_newleft3_def)
 done
 from k1 and k2 show
-"rec_eval (rec_embranch (zip ?rgs ?rrs)) [p, r, a] = newleft p r a"
+"rec_exec (rec_embranch (zip ?rgs ?rrs)) [p, r, a] = newleft p r a"
 by simp
 qed
 text {*
 The @{text "newrght"} function is one similar to @{text "newleft"}, but used to
 done
 text {*
 The correctness of @{text "rec_newrght"}.
 *}
-lemma newrght_lemma: "rec_eval rec_newrght [p, r, a] = newrght p r a"
+lemma newrght_lemma: "rec_exec 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"
 let ?r1 = "\<lambda> zs. zs ! 2 = 1"
 let ?r2 = "\<lambda> zs. zs ! 2 = 2"
 "[Cn 3 rec_eq [recf.id 3 2, Cn 3 (constn 0) [recf.id 3 0]], Cn 3 rec_eq [recf.id 3 2,
 Cn 3 (constn 1) [recf.id 3 0]], 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_eval (rec_embranch (zip ?rgs ?rrs)) [p, r, a]
+have k1: "rec_exec (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]"
+= Embranch (zip (map rec_exec ?rgs) (map (\<lambda>r args. 0 < rec_exec 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)+
 apply(case_tac "a = 0", rule_tac x = 0 in exI)
 prefer 2
 prefer 2
 apply(case_tac "a = 2", rule_tac x = "2" in exI)
 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_eval.simps)
+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_eval.simps)
+apply(erule_tac [!] Suc_5_induct, auto simp: rec_exec.simps)
 done
-have k2: "Embranch (zip (map rec_eval ?rgs)
+have k2: "Embranch (zip (map rec_exec ?rgs)
-(map (\<lambda>r args. 0 < rec_eval r args) ?rrs)) [p, r, a] = newrght p r a"
+(map (\<lambda>r args. 0 < rec_exec r args) ?rrs)) [p, r, a] = newrght p r a"
-apply(auto simp:Embranch.simps rec_eval.simps)
+apply(auto simp:Embranch.simps rec_exec.simps)
 apply(auto simp: newrght.simps rec_newrgt3_def rec_newrgt2_def
-rec_newrgt1_def rec_newrgt0_def rec_eval.simps
+rec_newrgt1_def rec_newrgt0_def rec_exec.simps
 scan_lemma)
 done
 from k1 and k2 show
-"rec_eval (rec_embranch (zip ?rgs ?rrs)) [p, r, a] =
+"rec_exec (rec_embranch (zip ?rgs ?rrs)) [p, r, a] =
 newrght p r a" by simp
 qed
 declare Entry.simps[simp del]
 Cn 3 rec_eq [id 3 1, Cn 3 (constn 0) [id 3 0]]]] "
 text {*
 The correctness of @{text "actn"}.
 *}
-lemma actn_lemma: "rec_eval rec_actn [m, q, r] = actn m q r"
+lemma actn_lemma: "rec_exec rec_actn [m, q, r] = actn m q r"
-by(auto simp: rec_actn_def rec_eval.simps entry_lemma scan_lemma)
+by(auto simp: rec_actn_def rec_exec.simps entry_lemma scan_lemma)
 fun newstat :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat"
 where
 "newstat m q r = (if q \<noteq> 0 then Entry m (4*(q - 1) + 2*scan r + 1)
 else 0)"
 Cn 3 rec_scan [id 3 2]], Cn 3 (constn 1) [id 3 0]]]],
 Cn 3 rec_noteq [id 3 1, Cn 3 (constn 0) [id 3 0]]],
 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_eval rec_newstat [m, q, r] = newstat m q r"
+lemma newstat_lemma: "rec_exec rec_newstat [m, q, r] = newstat m q r"
-by(auto simp:  rec_eval.simps entry_lemma scan_lemma rec_newstat_def)
+by(auto simp:  rec_exec.simps entry_lemma scan_lemma rec_newstat_def)
 declare newstat.simps[simp del] actn.simps[simp del]
 text{*code the configuration*}
 "rec_trpl = Cn 3 rec_mult [Cn 3 rec_mult
 [Cn 3 rec_power [Cn 3 (constn (Pi 0)) [id 3 0], id 3 0],
 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_eval rec_trpl [p, q, r] = trpl p q r"
+lemma trpl_lemma: "rec_exec rec_trpl [p, q, r] = trpl p q r"
-by(auto simp: rec_trpl_def rec_eval.simps power_lemma trpl.simps)
+by(auto simp: rec_trpl_def rec_exec.simps power_lemma trpl.simps)
 text{*left, stat, rght: decode func*}
 fun left :: "nat \<Rightarrow> nat"
 where
 "left c = lo c (Pi 0)"
 [Cn vl (constn 0) [id vl 0],
 Cn vl (constn 1) [id vl 0],
 Cn vl (rec_strt (vl - 1))
 (map (\<lambda> i. id vl (i)) [1..<vl])]"
-lemma left_lemma: "rec_eval rec_left [c] = left c"
+lemma left_lemma: "rec_exec rec_left [c] = left c"
-by(simp add: rec_eval.simps rec_left_def left.simps lo_lemma)
+by(simp add: rec_exec.simps rec_left_def left.simps lo_lemma)
-lemma right_lemma: "rec_eval rec_right [c] = rght c"
+lemma right_lemma: "rec_exec rec_right [c] = rght c"
-by(simp add: rec_eval.simps rec_right_def rght.simps lo_lemma)
+by(simp add: rec_exec.simps rec_right_def rght.simps lo_lemma)
-lemma stat_lemma: "rec_eval rec_stat [c] = stat c"
+lemma stat_lemma: "rec_exec rec_stat [c] = stat c"
-by(simp add: rec_eval.simps rec_stat_def stat.simps lo_lemma)
+by(simp add: rec_exec.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_eval a (m # xs)) \<circ>
+"(map ((\<lambda>a. rec_exec 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_eval.simps nth_append nth_Cons split: nat.split)
+apply(auto simp: rec_exec.simps nth_append nth_Cons split: nat.split)
 done
 lemma list_map_eq:
 "vl = length (xs::nat list) \<Longrightarrow> map (\<lambda> i. xs ! (i - 1))
 [Suc 0..<Suc vl] = xs"
 done
 qed
 lemma [elim]:
 "Suc 0 \<le> length xs \<Longrightarrow>
-(map ((\<lambda>a. rec_eval a (m # xs)) \<circ>
+(map ((\<lambda>a. rec_exec 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_eval.simps)
+apply(simp del: map_eq_conv add: rec_exec.simps)
 using list_map_eq[of "length xs" xs]
 apply(simp)
 done
 lemma inpt_lemma:
 "\<lbrakk>Suc (length xs) = vl\<rbrakk> \<Longrightarrow>
-rec_eval (rec_inpt vl) (m # xs) = inpt m xs"
+rec_exec (rec_inpt vl) (m # xs) = inpt m xs"
-apply(auto simp: rec_eval.simps rec_inpt_def
+apply(auto simp: rec_exec.simps rec_inpt_def
 trpl_lemma inpt.simps strt_lemma)
 apply(subgoal_tac
-"(map ((\<lambda>a. rec_eval a (m # xs)) \<circ>
+"(map ((\<lambda>a. rec_exec 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)
 done
 Cn 2 rec_right [id 2 1],
 Cn 2 rec_actn [id 2 0,
 Cn 2 rec_stat [id 2 1],
 Cn 2 rec_right [id 2 1]]]]"
-lemma newconf_lemma: "rec_eval rec_newconf [m ,c] = newconf m c"
+lemma newconf_lemma: "rec_exec rec_newconf [m ,c] = newconf m c"
-by(auto simp: rec_newconf_def rec_eval.simps
+by(auto simp: rec_newconf_def rec_exec.simps
 trpl_lemma newleft_lemma left_lemma
 right_lemma stat_lemma newrght_lemma actn_lemma
 newstat_lemma stat_lemma newconf.simps)
 declare newconf_lemma[simp]
 where
 "rec_conf = Pr 2 (Cn 2 rec_trpl [Cn 2 (constn 0) [id 2 0], Cn 2 (constn (Suc 0)) [id 2 0], id 2 1])
 (Cn 4 rec_newconf [id 4 0, id 4 3])"
 lemma conf_step:
-"rec_eval rec_conf [m, r, Suc t] =
+"rec_exec rec_conf [m, r, Suc t] =
-rec_eval rec_newconf [m, rec_eval rec_conf [m, r, t]]"
+rec_exec rec_newconf [m, rec_exec rec_conf [m, r, t]]"
 proof -
-have "rec_eval rec_conf ([m, r] @ [Suc t]) =
+have "rec_exec rec_conf ([m, r] @ [Suc t]) =
-rec_eval rec_newconf [m, rec_eval rec_conf [m, r, t]]"
+rec_exec rec_newconf [m, rec_exec rec_conf [m, r, t]]"
 by(simp only: rec_conf_def rec_pr_Suc_simp_rewrite,
-simp add: rec_eval.simps)
+simp add: rec_exec.simps)
-thus "rec_eval rec_conf [m, r, Suc t] =
+thus "rec_exec rec_conf [m, r, Suc t] =
-rec_eval rec_newconf [m, rec_eval rec_conf [m, r, t]]"
+rec_exec rec_newconf [m, rec_exec rec_conf [m, r, t]]"
 by simp
 qed
 text {*
 The correctness of @{text "rec_conf"}.
 *}
 lemma conf_lemma:
-"rec_eval rec_conf [m, r, t] = conf m r t"
+"rec_exec rec_conf [m, r, t] = conf m r t"
 apply(induct t)
-apply(simp add: rec_conf_def rec_eval.simps conf.simps inpt_lemma trpl_lemma)
+apply(simp add: rec_conf_def rec_exec.simps conf.simps inpt_lemma trpl_lemma)
 apply(simp add: conf_step conf.simps)
 done
 text {*
 @{text "NSTD c"} returns true if the configureation coded by @{text "c"} is no a stardard
 [Cn 1 rec_add
 [rec_right, constn 1],
 constn 2]], constn 1]]],
 Cn 1 rec_eq [rec_right, constn 0]]"
-lemma NSTD_lemma1: "rec_eval rec_NSTD [c] = Suc 0 \<or>
+lemma NSTD_lemma1: "rec_exec rec_NSTD [c] = Suc 0 \<or>
-rec_eval rec_NSTD [c] = 0"
+rec_exec rec_NSTD [c] = 0"
-by(simp add: rec_eval.simps rec_NSTD_def)
+by(simp add: rec_exec.simps rec_NSTD_def)
 declare NSTD.simps[simp del]
-lemma NSTD_lemma2': "(rec_eval rec_NSTD [c] = Suc 0) \<Longrightarrow> NSTD c"
+lemma NSTD_lemma2': "(rec_exec rec_NSTD [c] = Suc 0) \<Longrightarrow> NSTD c"
-apply(simp add: rec_eval.simps rec_NSTD_def stat_lemma left_lemma
+apply(simp add: rec_exec.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_eval rec_NSTD [c] = Suc 0)"
+"NSTD c \<Longrightarrow> (rec_exec rec_NSTD [c] = Suc 0)"
-apply(simp add: rec_eval.simps rec_NSTD_def stat_lemma
+apply(simp add: rec_exec.simps rec_NSTD_def stat_lemma
 left_lemma lg_lemma right_lemma power_lemma NSTD.simps)
 apply(auto split: if_splits)
 done
 text {*
 The correctness of @{text "NSTD"}.
 *}
-lemma NSTD_lemma2: "(rec_eval rec_NSTD [c] = Suc 0) = NSTD c"
+lemma NSTD_lemma2: "(rec_exec rec_NSTD [c] = Suc 0) = NSTD c"
 using NSTD_lemma1
 apply(auto intro: NSTD_lemma2' NSTD_lemma2'')
 done
 fun nstd :: "nat \<Rightarrow> nat"
 where
 "nstd c = (if NSTD c then 1 else 0)"
-lemma nstd_lemma: "rec_eval rec_NSTD [c] = nstd c"
+lemma nstd_lemma: "rec_exec rec_NSTD [c] = nstd c"
 using NSTD_lemma1
 apply(simp add: NSTD_lemma2, auto)
 done
 text{*
 text {*
 The correctness of @{text "rec_nonstop"}.
 *}
 lemma nonstop_lemma:
-"rec_eval rec_nonstop [m, r, t] = nonstop m r t"
+"rec_exec rec_nonstop [m, r, t] = nonstop m r t"
-apply(simp add: rec_eval.simps rec_nonstop_def nstd_lemma conf_lemma)
+apply(simp add: rec_exec.simps rec_nonstop_def nstd_lemma conf_lemma)
 done
 text{*
 @{text "rec_halt"} is the recursive function calculating the steps a TM needs to execute before
 to reach a stardard final configuration. This recursive function is the only one
 rec_newstat_def)
 apply(tactic {* resolve_tac [@{thm prime_cn},
 @{thm prime_id}, @{thm prime_pr}] 1*}, auto+)+
 done
-lemma primerec_terminates:
+lemma primerec_terminate:
-"\<lbrakk>primerec f x; length xs = x\<rbrakk> \<Longrightarrow> terminates f xs"
+"\<lbrakk>primerec f x; length xs = x\<rbrakk> \<Longrightarrow> terminate f xs"
 proof(induct arbitrary: xs rule: primerec.induct)
 fix xs
-assume "length (xs::nat list) = Suc 0"  thus "terminates z xs"
+assume "length (xs::nat list) = Suc 0"  thus "terminate z xs"
 by(case_tac xs, auto intro: termi_z)
 next
 fix xs
-assume "length (xs::nat list) = Suc 0" thus "terminates s xs"
+assume "length (xs::nat list) = Suc 0" thus "terminate s xs"
 by(case_tac xs, auto intro: termi_s)
 next
 fix n m xs
-assume "n < m" "length (xs::nat list) = m"  thus "terminates (id m n) xs"
+assume "n < m" "length (xs::nat list) = m"  thus "terminate (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> terminates (gs ! i) x)"
+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> terminates f xs"
+and ind2: "\<And> xs. length xs = k \<Longrightarrow> terminate f xs"
 and h: "primerec f k"  "length gs = k" "m = n" "length (xs::nat list) = m"
-have "terminates f (map (\<lambda>g. rec_eval g xs) gs)"
+have "terminate f (map (\<lambda>g. rec_exec g xs) gs)"
-using ind2[of "(map (\<lambda>g. rec_eval g xs) gs)"] h
+using ind2[of "(map (\<lambda>g. rec_exec g xs) gs)"] h
 by simp
-moreover have "\<forall>g\<in>set gs. terminates g xs"
+moreover have "\<forall>g\<in>set gs. terminate g xs"
 using ind h
 by(auto simp: set_conv_nth)
-ultimately show "terminates (Cn n f gs) xs"
+ultimately show "terminate (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> terminates f xs"
+assume ind1: "\<And>xs. length xs = n \<Longrightarrow> terminate f xs"
-and ind2: "\<And>xs. length xs = Suc (Suc n) \<Longrightarrow> terminates g xs"
+and ind2: "\<And>xs. length xs = Suc (Suc n) \<Longrightarrow> terminate 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. terminates g (butlast xs @ [y, rec_eval (Pr n f g) (butlast xs @ [y])])"
+have "\<forall>y<last xs. terminate g (butlast xs @ [y, rec_exec (Pr n f g) (butlast xs @ [y])])"
 using h
 apply(auto)
 by(rule_tac ind2, simp)
-moreover have "terminates f (butlast xs)"
+moreover have "terminate f (butlast xs)"
 using ind1[of "butlast xs"] h
 by simp
 moreover have "length (butlast xs) = n"
 using h by simp
-ultimately have "terminates (Pr n f g) (butlast xs @ [last xs])"
+ultimately have "terminate (Pr n f g) (butlast xs @ [last xs])"
 by(rule_tac termi_pr, simp_all)
-thus "terminates (Pr n f g) xs"
+thus "terminate (Pr n f g) xs"
 using h
 by(case_tac "xs = []", auto)
 qed
 text {*
 The following lemma gives the correctness of @{text "rec_halt"}.
 It says: if @{text "rec_halt"} calculates that the TM coded by @{text "m"}
-will reach a standard final configuration after @{text "t"} steps of execution,
+will reach a standard final configuration after @{text "t"} steps of execution, then it is indeed so.
-then it is indeed so.
 *}
 text {*F: universal machine*}
 text {*
 @{text "valu r"} extracts computing result out of the right number @{text "r"}.
 *}
 "rec_valu = Cn 1 rec_minus [Cn 1 rec_lg [s, constn 2], constn 1]"
 text {*
 The correctness of @{text "rec_valu"}.
 *}
-lemma value_lemma: "rec_eval rec_valu [r] = valu r"
+lemma value_lemma: "rec_exec rec_valu [r] = valu r"
-apply(simp add: rec_eval.simps rec_valu_def lg_lemma)
+apply(simp add: rec_exec.simps rec_valu_def lg_lemma)
 done
 lemma [intro]: "primerec rec_valu (Suc 0)"
 apply(simp add: rec_valu_def)
 apply(rule_tac k = "Suc (Suc 0)" in prime_cn)
 The definition of the universal function @{text "rec_F"}.
 *}
 definition rec_F :: "recf"
 where
 "rec_F = Cn (Suc (Suc 0)) rec_valu [Cn (Suc (Suc 0)) rec_right [Cn (Suc (Suc 0))
 rec_conf ([id (Suc (Suc 0)) 0, id (Suc (Suc 0)) (Suc 0), rec_halt])]]"
 lemma get_fstn_args_nth:
 "k < n \<Longrightarrow> (get_fstn_args m n ! k) = id m (k)"
 apply(induct n, simp)
 apply(case_tac "k = n", simp_all add: get_fstn_args.simps
 k < length ys\<rbrakk> \<Longrightarrow>
 (get_fstn_args (length ys) (length ys) ! k) =
 id (length ys) (k)"
 by(erule_tac get_fstn_args_nth)
-lemma terminates_halt_lemma:
+lemma terminate_halt_lemma:
-"\<lbrakk>rec_eval rec_nonstop ([m, r] @ [t]) = 0;
+"\<lbrakk>rec_exec rec_nonstop ([m, r] @ [t]) = 0;
-\<forall>i<t. 0 < rec_eval rec_nonstop ([m, r] @ [i])\<rbrakk> \<Longrightarrow> terminates rec_halt [m, r]"
+\<forall>i<t. 0 < rec_exec rec_nonstop ([m, r] @ [i])\<rbrakk> \<Longrightarrow> terminate rec_halt [m, r]"
 apply(simp add: rec_halt_def)
 apply(rule_tac termi_mn, auto)
-apply(rule_tac [!] primerec_terminates, auto)
+apply(rule_tac [!] primerec_terminate, auto)
 done
 text {*
 The correctness of @{text "rec_F"}, halt case.
 *}
-lemma F_lemma: "rec_eval rec_halt [m, r] = t \<Longrightarrow> rec_eval rec_F [m, r] = (valu (rght (conf m r t)))"
+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_eval.simps value_lemma right_lemma conf_lemma halt_lemma)
+by(simp add: rec_F_def rec_exec.simps value_lemma right_lemma conf_lemma halt_lemma)
-lemma terminates_F_lemma: "terminates rec_halt [m, r] \<Longrightarrow> terminates rec_F [m, r]"
+lemma terminate_F_lemma: "terminate rec_halt [m, r] \<Longrightarrow> terminate rec_F [m, r]"
 apply(simp add: rec_F_def)
 apply(rule_tac termi_cn, auto)
-apply(rule_tac primerec_terminates, auto)
+apply(rule_tac primerec_terminate, auto)
 apply(rule_tac termi_cn, auto)
-apply(rule_tac primerec_terminates, auto)
+apply(rule_tac primerec_terminate, auto)
 apply(rule_tac termi_cn, auto)
-apply(rule_tac primerec_terminates, auto)
+apply(rule_tac primerec_terminate, auto)
 apply(rule_tac [!] termi_id, auto)
 done
 text {*
 The correctness of @{text "rec_F"}, nonhalt case.
 done
 lemma Pi_gr_1[simp]: "Pi n > Suc 0"
 proof(induct n, auto simp: Pi.simps Np.simps)
 fix n
-let ?setx = "{y. y \<le> Suc (Pi n!) \<and> Pi n < y \<and> prime y}"
+let ?setx = "{y. y \<le> Suc (Pi n!) \<and> Pi n < y \<and> Prime y}"
 have "finite ?setx" by auto
 moreover have "?setx \<noteq> {}"
 using prime_ex[of "Pi n"]
 apply(auto)
 done
 ultimately show "Suc 0 < Min ?setx"
 apply(simp add: Min_gr_iff)
-apply(auto simp: prime_nat_def dvd_def)
+apply(auto simp: Prime.simps)
 done
 qed
 lemma Pi_not_0[simp]: "Pi n > 0"
 using Pi_gr_1[of n]
 "\<lbrakk>i < length nl; \<not> Suc 0 < godel_code nl\<rbrakk> \<Longrightarrow> nl ! i = 0"
 using godel_code_great[of nl] godel_code_eq_1[of nl]
 apply(simp)
 done
+lemma prime_coprime: "\<lbrakk>Prime x; Prime y; x\<noteq>y\<rbrakk> \<Longrightarrow> coprime x y"
+proof(simp only: Prime.simps coprime_nat, auto simp: dvd_def,
+rule_tac classical, simp)
+fix d k ka
+assume case_ka: "\<forall>u<d * ka. \<forall>v<d * ka. u * v \<noteq> d * ka"
+and case_k: "\<forall>u<d * k. \<forall>v<d * k. u * v \<noteq> d * k"
+and h: "(0::nat) < d" "d \<noteq> Suc 0" "Suc 0 < d * ka"
+"ka \<noteq> k" "Suc 0 < d * k"
+from h have "k > Suc 0 \<or> ka >Suc 0"
+apply(auto)
+apply(case_tac ka, simp, simp)
+apply(case_tac k, simp, simp)
+done
+from this show "False"
+proof(erule_tac disjE)
+assume  "(Suc 0::nat) < k"
+hence "k < d*k \<and> d < d*k"
+using h
+by(auto)
+thus "?thesis"
+using case_k
+apply(erule_tac x = d in allE)
+apply(simp)
+apply(erule_tac x = k in allE)
+apply(simp)
+done
+next
+assume "(Suc 0::nat) < ka"
+hence "ka < d * ka \<and> d < d*ka"
+using h by auto
+thus "?thesis"
+using case_ka
+apply(erule_tac x = d in allE)
+apply(simp)
+apply(erule_tac x = ka in allE)
+apply(simp)
+done
+qed
+qed
 lemma Pi_inc: "Pi (Suc i) > Pi i"
 proof(simp add: Pi.simps Np.simps)
-let ?setx = "{y. y \<le> Suc (Pi i!) \<and> Pi i < y \<and> prime y}"
+let ?setx = "{y. y \<le> Suc (Pi i!) \<and> Pi i < y \<and> Prime y}"
 have "finite ?setx" by simp
 moreover have "?setx \<noteq> {}"
 using prime_ex[of "Pi i"]
 apply(auto)
 done
 apply(simp)
 using Pi_inc_gr[of j i]
 apply(simp)
 done
-lemma [intro]: "prime (Suc (Suc 0))"
+lemma [intro]: "Prime (Suc (Suc 0))"
-apply(auto simp: prime_nat_def dvd_def)
+apply(auto simp: Prime.simps)
-apply(case_tac m, simp, case_tac k, simp, simp)
+apply(case_tac u, simp, case_tac nat, simp, simp)
 done
-lemma Prime_Pi[intro]: "prime (Pi n)"
+lemma Prime_Pi[intro]: "Prime (Pi n)"
 proof(induct n, auto simp: Pi.simps Np.simps)
 fix n
-let ?setx = "{y. y \<le> Suc (Pi n!) \<and> Pi n < y \<and> prime y}"
+let ?setx = "{y. y \<le> Suc (Pi n!) \<and> Pi n < y \<and> Prime y}"
-show "prime (Min ?setx)"
+show "Prime (Min ?setx)"
 proof -
 have "finite ?setx" by simp
 moreover have "?setx \<noteq> {}"
 using prime_ex[of "Pi n"]
 apply(simp)
 qed
 lemma Pi_coprime: "i \<noteq> j \<Longrightarrow> coprime (Pi i) (Pi j)"
 using Prime_Pi[of i]
 using Prime_Pi[of j]
-apply(rule_tac primes_coprime_nat, simp_all add: Pi_notEq)
+apply(rule_tac prime_coprime, simp_all add: Pi_notEq)
 done
 lemma Pi_power_coprime: "i \<noteq> j \<Longrightarrow> coprime ((Pi i)^m) ((Pi j)^n)"
 by(rule_tac coprime_exp2_nat, erule_tac Pi_coprime)
 from g have
 "coprime (Pi (Suc i)) (godel_code' (butlast ps) (Suc 0) *
 Pi (length ps)^(last ps)) "
 proof(rule_tac coprime_mult_nat, simp)
 show "coprime (Pi (Suc i)) (Pi (length ps) ^ last ps)"
-apply(rule_tac coprime_exp_nat, rule primes_coprime_nat, auto)
+apply(rule_tac coprime_exp_nat, rule prime_coprime, auto)
 using Pi_notEq[of "Suc i" "length ps"] h by simp
 qed
 from this and k show "coprime (Pi (Suc i)) (godel_code' ps (Suc 0))"
 by simp
 qed
 The lemma relates the one step execution of TMs with the interpreter function @{text "rec_newconf"}.
 *}
 lemma rec_t_eq_step:
 "(\<lambda> (s, l, r). s \<le> length tp div 2) c \<Longrightarrow>
 trpl_code (step0 c tp) =
-rec_eval rec_newconf [code tp, trpl_code c]"
+rec_exec 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)
 fix a b ca aa ba
 assume h: "(a::nat) \<le> length tp div 2"
 apply(simp)
 done
 lemma [simp]:
 "trpl_code (steps0 (Suc 0, Bk\<up>l, <lm>) tp 0) =
-rec_eval rec_conf [code tp, bl2wc (<lm>), 0]"
+rec_exec rec_conf [code tp, bl2wc (<lm>), 0]"
-apply(simp add: steps.simps rec_eval.simps conf_lemma  conf.simps
+apply(simp add: steps.simps rec_exec.simps conf_lemma  conf.simps
 inpt.simps trpl_code.simps bl2wc.simps)
 done
 text {*
 The following lemma relates the multi-step interpreter function @{text "rec_conf"}
 qed
 lemma rec_t_eq_steps:
 "tm_wf (tp,0) \<Longrightarrow>
 trpl_code (steps0 (Suc 0, Bk\<up>l, <lm>) tp stp) =
-rec_eval rec_conf [code tp, bl2wc (<lm>), stp]"
+rec_exec rec_conf [code tp, bl2wc (<lm>), stp]"
 proof(induct stp)
 case 0 thus "?case" by(simp)
 next
 case (Suc n) thus "?case"
 proof -
 assume ind:
 "tm_wf (tp,0) \<Longrightarrow> trpl_code (steps0 (Suc 0, Bk\<up> l, <lm>) tp n)
-= rec_eval rec_conf [code tp, bl2wc (<lm>), n]"
+= rec_exec 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_eval rec_conf [code tp, bl2wc (<lm>), Suc n]"
+rec_exec 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
 assume g: "steps0 (Suc 0, Bk\<up> l, <lm>) tp n = (a, b, c) "
 hence "conf (code tp) (bl2wc (<lm>)) n= trpl_code (a, b, c)"
 using ind h
 apply(simp add: conf_lemma)
 done
 moreover hence
 "trpl_code (step0 (a, b, c) tp) =
-rec_eval rec_newconf [code tp, trpl_code (a, b, c)]"
+rec_exec 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)
 done
 ultimately show
 lemma nonstop_t_eq:
 "\<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_eval rec_nonstop [code tp, bl2wc (<lm>), stp] = 0"
+\<Longrightarrow> rec_exec 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_eval rec_conf [code tp,  bl2wc (<lm>), stp] =
+have g: "rec_exec 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)
 thus "\<not> NSTD (conf (code tp) (bl2wc (<lm>)) stp)"
 proof(auto simp: NSTD.simps)
 text {*
 The correntess of @{text "rec_F"} which relates the interpreter function @{text "rec_F"} with the
 execution of of TMs.
 *}
-lemma terminates_halt:
+lemma terminate_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> terminates rec_halt [code tp, (bl2wc (<lm>))]"
+tm_wf (tp,0); 0<rs\<rbrakk> \<Longrightarrow> terminate rec_halt [code tp, (bl2wc (<lm>))]"
 apply(frule_tac halt_least_step, auto)
-thm terminates_halt_lemma
+thm terminate_halt_lemma
-apply(rule_tac t = stpa in terminates_halt_lemma)
+apply(rule_tac t = stpa in terminate_halt_lemma)
 apply(simp_all add: nonstop_lemma, auto)
 done
-lemma terminates_F:
+lemma terminate_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> terminates rec_F [code tp, (bl2wc (<lm>))]"
+tm_wf (tp,0); 0<rs\<rbrakk> \<Longrightarrow> terminate rec_F [code tp, (bl2wc (<lm>))]"
-apply(drule_tac terminates_halt, simp_all)
+apply(drule_tac terminate_halt, simp_all)
-apply(erule_tac terminates_F_lemma)
+apply(erule_tac terminate_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_eval rec_F [code tp, (bl2wc (<lm>))] = (rs - Suc 0)"
+\<Longrightarrow> rec_exec 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]
 apply(simp add: conf_lemma)
 proof -
 "steps0 (Suc 0, Bk\<up> l, <lm>) tp stp = (0, Bk\<up> m, Oc\<up> rs @ Bk\<up> n)"
 hence g1: "conf (code tp) (bl2wc (<lm>)) stpa = trpl_code (0, Bk\<up> m, Oc\<up> rs @ Bk\<up>n)"
 using halt_state_keep[of "code tp" lm stpa stp]
 by(simp)
 moreover have g2:
-"rec_eval rec_halt [code tp, (bl2wc (<lm>))] = stpa"
+"rec_exec rec_halt [code tp, (bl2wc (<lm>))] = stpa"
 using h
-by(auto simp: rec_eval.simps rec_halt_def nonstop_lemma intro!: Least_equality)
+by(auto simp: rec_exec.simps rec_halt_def nonstop_lemma intro!: Least_equality)
 show
-"rec_eval rec_F [code tp, (bl2wc (<lm>))] = (rs - Suc 0)"
+"rec_exec rec_F [code tp, (bl2wc (<lm>))] = (rs - Suc 0)"
 proof -
 have
 "valu (rght (conf (code tp) (bl2wc (<lm>)) stpa)) = rs - Suc 0"
 using g1
 apply(simp add: valu.simps trpl_code.simps
 bl2wc.simps  bl2nat_append lg_power)
 done
 thus "?thesis"
-by(simp add: rec_eval.simps F_lemma g2)
+by(simp add: rec_exec.simps F_lemma g2)
 qed
 qed
 end

changeset 248	aea02b5a58d2
parent 240	696081f445c2
child 250	745547bdc1c7