diff -r 4f303da0cd2a -r a0bcf886b8ef utm/UF.thy
--- a/utm/UF.thy	Mon Mar 04 21:01:55 2013 +0000
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,4873 +0,0 @@
-theory UF
-imports Main rec_def turing_basic 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 
-  interpreter of Turing Machines. Once the correctness of @{text "rec_F"} is established,
-  UTM can easil be obtained by compling @{text "rec_F"} into the corresponding Turing Machine.
-*}
-
-section {* Univeral Function *}
-
-subsection {* The construction of component functions *}
-
-text {*
-  This section constructs a set of component functions used to construct @{text "rec_F"}.
-  *}
-
-text {*
-  The recursive function used to do arithmatic addition.
-*}
-definition rec_add :: "recf"
-  where
-  "rec_add \<equiv>  Pr 1 (id 1 0) (Cn 3 s [id 3 2])"
-
-text {*
-  The recursive function used to do arithmatic multiplication.
-*}
-definition rec_mult :: "recf"
-  where
-  "rec_mult = Pr 1 z (Cn 3 rec_add [id 3 0, id 3 2])"
-
-text {*
-  The recursive function used to do arithmatic precede.
-*}
-definition rec_pred :: "recf"
-  where
-  "rec_pred = Cn 1 (Pr 1 z (id 3 1)) [id 1 0, id 1 0]"
-
-text {*
-  The recursive function used to do arithmatic subtraction.
-*}
-definition rec_minus :: "recf" 
-  where
-  "rec_minus = Pr 1 (id 1 0) (Cn 3 rec_pred [id 3 2])"
-
-text {*
-  @{text "constn n"} is the recursive function which computes 
-  nature number @{text "n"}.
-*}
-fun constn :: "nat \<Rightarrow> recf"
-  where
-  "constn 0 = z"  |
-  "constn (Suc n) = Cn 1 s [constn n]"
-
-
-text {*
-  Signal function, which returns 1 when the input argument is greater than @{text "0"}.
-*}
-definition rec_sg :: "recf"
-  where
-  "rec_sg = Cn 1 rec_minus [constn 1, 
-                  Cn 1 rec_minus [constn 1, id 1 0]]"
-
-text {*
-  @{text "rec_less"} compares its two arguments, returns @{text "1"} if
-  the first is less than the second; otherwise returns @{text "0"}.
-  *}
-definition rec_less :: "recf"
-  where
-  "rec_less = Cn 2 rec_sg [Cn 2 rec_minus [id 2 1, id 2 0]]"
-
-text {*
-  @{text "rec_not"} inverse its argument: returns @{text "1"} when the
-  argument is @{text "0"}; returns @{text "0"} otherwise.
-  *}
-definition rec_not :: "recf"
-  where
-  "rec_not = Cn 1 rec_minus [constn 1, id 1 0]"
-
-text {*
-  @{text "rec_eq"} compares its two arguments: returns @{text "1"}
-  if they are equal; return @{text "0"} otherwise.
-  *}
-definition rec_eq :: "recf"
-  where
-  "rec_eq = Cn 2 rec_minus [Cn 2 (constn 1) [id 2 0], 
-             Cn 2 rec_add [Cn 2 rec_minus [id 2 0, id 2 1], 
-               Cn 2 rec_minus [id 2 1, id 2 0]]]"
-
-text {*
-  @{text "rec_conj"} computes the conjunction of its two arguments, 
-  returns @{text "1"} if both of them are non-zero; returns @{text "0"}
-  otherwise.
-  *}
-definition rec_conj :: "recf"
-  where
-  "rec_conj = Cn 2 rec_sg [Cn 2 rec_mult [id 2 0, id 2 1]] "
-
-text {*
-  @{text "rec_disj"} computes the disjunction of its two arguments, 
-  returns @{text "0"} if both of them are zero; returns @{text "0"}
-  otherwise.
-  *}
-definition rec_disj :: "recf"
-  where
-  "rec_disj = Cn 2 rec_sg [Cn 2 rec_add [id 2 0, id 2 1]]"
-
-
-text {*
-  Computes the arity of recursive function.
-  *}
-
-fun arity :: "recf \<Rightarrow> nat"
-  where
-  "arity z = 1" 
-| "arity s = 1"
-| "arity (id m n) = m"
-| "arity (Cn n f gs) = n"
-| "arity (Pr n f g) = Suc n"
-| "arity (Mn n f) = n"
-
-text {*
-  @{text "get_fstn_args n (Suc k)"} returns
-  @{text "[id n 0, id n 1, id n 2, \<dots>, id n k]"}, 
-  the effect of which is to take out the first @{text "Suc k"} 
-  arguments out of the @{text "n"} input arguments.
-  *}
-
-fun get_fstn_args :: "nat \<Rightarrow>  nat \<Rightarrow> recf list"
-  where
-  "get_fstn_args n 0 = []"
-| "get_fstn_args n (Suc y) = get_fstn_args n y @ [id n y]"
-
-text {*
-  @{text "rec_sigma f"} returns the recursive functions which 
-  sums up the results of @{text "f"}:
-  \[
-  (rec\_sigma f)(x, y) = f(x, 0) + f(x, 1) + \cdots + f(x, y)
-  \]
-*}
-fun rec_sigma :: "recf \<Rightarrow> recf"
-  where
-  "rec_sigma rf = 
-       (let vl = arity rf in 
-          Pr (vl - 1) (Cn (vl - 1) rf (get_fstn_args (vl - 1) (vl - 1) @ 
-                    [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 {*
-  @{text "rec_exec"} is the interpreter function for
-  reursive functions. The function is defined such that 
-  it always returns meaningful results for primitive recursive 
-  functions.
-  *}
-function rec_exec :: "recf \<Rightarrow> nat list \<Rightarrow> nat"
-  where
-  "rec_exec z xs = 0" |
-  "rec_exec s xs = (Suc (xs ! 0))" |
-  "rec_exec (id m n) xs = (xs ! n)" |
-  "rec_exec (Cn n f gs) xs = 
-             (let ys = (map (\<lambda> a. rec_exec a xs) gs) in 
-                                  rec_exec f ys)" | 
-  "rec_exec (Pr n f g) xs = 
-     (if last xs = 0 then 
-                  rec_exec f (butlast xs)
-      else rec_exec g (butlast xs @ [last xs - 1] @
-            [rec_exec (Pr n f g) (butlast xs @ [last xs - 1])]))" |
-  "rec_exec (Mn n f) xs = (LEAST x. rec_exec f (xs @ [x]) = 0)"
-by pat_completeness auto
-termination
-proof 
-  show "wf (measures [\<lambda> (r, xs). size r, (\<lambda> (r, xs). last xs)])" 
-    by auto
-next
-  fix n f gs xs x
-  assume "(x::recf) \<in> set gs" 
-  thus "((x, xs), Cn n f gs, xs) \<in> 
-    measures [\<lambda>(r, xs). size r, \<lambda>(r, xs). last xs]"
-    by(induct gs, auto)
-next
-  fix n f gs xs x
-  assume "x = map (\<lambda>a. rec_exec a xs) gs"
-    "\<And>x. x \<in> set gs \<Longrightarrow> rec_exec_dom (x, xs)" 
-  thus "((f, x), Cn n f gs, xs) \<in> 
-    measures [\<lambda>(r, xs). size r, \<lambda>(r, xs). last xs]"
-    by(auto)
-next
-  fix n f g xs
-  show "((f, butlast xs), Pr n f g, xs) \<in>
-    measures [\<lambda>(r, xs). size r, \<lambda>(r, xs). last xs]"
-    by auto
-next
-  fix n f g xs
-  assume "last xs \<noteq> (0::nat)" thus 
-    "((Pr n f g, butlast xs @ [last xs - 1]), Pr n f g, xs) 
-    \<in> measures [\<lambda>(r, xs). size r, \<lambda>(r, xs). last xs]"
-    by auto
-next
-  fix n f g xs
-  show "((g, butlast xs @ [last xs - 1] @ [rec_exec (Pr n f g) (butlast xs @ [last xs - 1])]), 
-    Pr n f g, xs) \<in> measures [\<lambda>(r, xs). size r, \<lambda>(r, xs). last xs]"
-    by auto
-next
-  fix n f xs x
-  show "((f, xs @ [x]), Mn n f, xs) \<in> 
-    measures [\<lambda>(r, xs). size r, \<lambda>(r, xs). last xs]"
-    by auto
-qed
-
-declare rec_exec.simps[simp del] constn.simps[simp del]
-
-text {*
-  Correctness of @{text "rec_add"}.
-  *}
-lemma add_lemma: "\<And> x y. rec_exec rec_add [x, y] =  x + y"
-by(induct_tac y, auto simp: rec_add_def rec_exec.simps)
-
-text {*
-  Correctness of @{text "rec_mult"}.
-  *}
-lemma mult_lemma: "\<And> x y. rec_exec rec_mult [x, y] = x * y"
-by(induct_tac y, auto simp: rec_mult_def rec_exec.simps add_lemma)
-
-text {*
-  Correctness of @{text "rec_pred"}.
-  *}
-lemma pred_lemma: "\<And> x. rec_exec rec_pred [x] =  x - 1"
-by(induct_tac x, auto simp: rec_pred_def rec_exec.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)
-
-text {*
-  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)
-
-text {*
-  Correctness of @{text "rec_eq"}.
-  *}
-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_exec.simps rec_eq_def constn_lemma add_lemma minus_lemma)
-
-text {*
-  Correctness of @{text "rec_conj"}.
-  *}
-lemma conj_lemma: "\<And> x y. rec_exec rec_conj [x, y] = (if x = 0 \<or> y = 0 then 0 
-                                                       else 1)"
-by(induct_tac y, auto simp: rec_exec.simps sg_lemma rec_conj_def mult_lemma)
-
-
-text {*
-  Correctness of @{text "rec_disj"}.
-  *}
-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" |
-prime_cn[intro!]: "\<lbrakk>primerec f k; length gs = k; 
-  \<forall> i < length gs. primerec (gs ! i) m; m = n\<rbrakk> 
-  \<Longrightarrow> primerec (Cn n f gs) m" |
-prime_pr[intro!]: "\<lbrakk>primerec f n; 
-  primerec g (Suc (Suc n)); m = Suc n\<rbrakk> 
-  \<Longrightarrow> primerec (Pr n f g) m" 
-
-inductive_cases prime_cn_reverse'[elim]: "primerec (Cn n f gs) n" 
-inductive_cases prime_mn_reverse: "primerec (Mn n f) m" 
-inductive_cases prime_z_reverse[elim]: "primerec z n"
-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)) "
-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)"
-    by auto
-qed
-
-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_exec (Pr n f g) (xs @ [0]) = rec_exec f xs"
-by(simp add: rec_exec.simps)
-
-lemma rec_pr_0_simp_rewrite_single_param: "
-  rec_exec (Pr n f g) [0] = rec_exec f []"
-by(simp add: rec_exec.simps)
-
-lemma rec_pr_Suc_simp_rewrite: 
-  "rec_exec (Pr n f g) (xs @ [Suc x]) =
-                       rec_exec g (xs @ [x] @ 
-                        [rec_exec (Pr n f g) (xs @ [x])])"
-by(simp add: rec_exec.simps)
-
-lemma rec_pr_Suc_simp_rewrite_single_param: 
-  "rec_exec (Pr n f g) ([Suc x]) =
-           rec_exec g ([x] @ [rec_exec (Pr n f g) ([x])])"
-by(simp add: rec_exec.simps)
-
-lemma Sigma_0_simp_rewrite_single_param:
-  "Sigma f [0] = f [0]"
-by(simp add: Sigma.simps)
-
-lemma Sigma_0_simp_rewrite:
-  "Sigma f (xs @ [0]) = f (xs @ [0])"
-by(simp add: Sigma.simps)
-
-lemma Sigma_Suc_simp_rewrite: 
-  "Sigma f (xs @ [Suc x]) = Sigma f (xs @ [x]) + f (xs @ [Suc x])"
-by(simp add: Sigma.simps)
-
-lemma Sigma_Suc_simp_rewrite_single: 
-  "Sigma f ([Suc x]) = Sigma f ([x]) + f ([Suc x])"
-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_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_exec.simps 
-             take_Suc_conv_app_nth)
-qed
-    
-lemma [simp]: "primerec f n \<Longrightarrow> arity f = n"
-  apply(case_tac f)
-  apply(auto simp: arity.simps )
-  apply(erule_tac prime_mn_reverse)
-  done
-
-lemma rec_sigma_Suc_simp_rewrite: 
-  "primerec f (Suc (length xs))
-    \<Longrightarrow> rec_exec (rec_sigma f) (xs @ [Suc x]) = 
-    rec_exec (rec_sigma f) (xs @ [x]) + rec_exec f (xs @ [Suc x])"
-  apply(induct x)
-  apply(auto simp: rec_sigma.simps Let_def rec_pr_Suc_simp_rewrite
-                   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_exec (rec_sigma rg) (xs @ [x]) = Sigma (rec_exec rg) (xs @ [x])"
-apply(induct x)
-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 {*
-  @{text "rec_accum f (x1, x2, \<dots>, xn, k) = 
-           f(x1, x2, \<dots>, xn, 0) * 
-           f(x1, x2, \<dots>, xn, 1) *
-               \<dots> 
-           f(x1, x2, \<dots>, xn, k)"}
-*}
-fun rec_accum :: "recf \<Rightarrow> recf"
-  where
-  "rec_accum rf = 
-       (let vl = arity rf in 
-          Pr (vl - 1) (Cn (vl - 1) rf (get_fstn_args (vl - 1) (vl - 1) @ 
-                     [Cn (vl - 1) (constn 0) [id (vl - 1) 0]])) 
-             (Cn (Suc vl) rec_mult [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 {*
-  @{text "Accum"} is the formal specification of @{text "rec_accum"}.
-  *}
-function Accum :: "(nat list \<Rightarrow> nat) \<Rightarrow> nat list \<Rightarrow> nat"
-  where
-  "Accum f xs = (if last xs = 0 then f xs 
-                     else (Accum f (butlast xs @ [last xs - 1]) *
-                       f xs))"
-by pat_completeness auto
-termination
-proof
-  show "wf (measure (\<lambda> (f, xs). last xs))"
-    by auto
-next
-  fix f xs
-  assume "last xs \<noteq> (0::nat)"
-  thus "((f, butlast xs @ [last xs - 1]), f, xs) \<in> 
-            measure (\<lambda>(f, xs). last xs)"
-    by auto
-qed
-
-lemma rec_accum_Suc_simp_rewrite: 
-  "primerec f (Suc (length xs))
-    \<Longrightarrow> rec_exec (rec_accum f) (xs @ [Suc x]) = 
-    rec_exec (rec_accum f) (xs @ [x]) * rec_exec f (xs @ [Suc x])"
-  apply(induct x)
-  apply(auto simp: rec_sigma.simps Let_def rec_pr_Suc_simp_rewrite
-                   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_exec (rec_accum rg) (xs @ [x]) = Accum (rec_exec rg) (xs @ [x])"
-apply(induct x)
-apply(auto simp: rec_exec.simps rec_sigma.simps Let_def 
-                     get_fstn_args_take)
-done
-
-declare rec_accum.simps [simp del]
-
-text {*
-  @{text "rec_all t f (x1, x2, \<dots>, xn)"} 
-  computes the charactrization function of the following FOL formula:
-  @{text "(\<forall> x \<le> t(x1, x2, \<dots>, xn). (f(x1, x2, \<dots>, xn, x) > 0))"}
-*}
-fun rec_all :: "recf \<Rightarrow> recf \<Rightarrow> recf"
-  where
-  "rec_all rt rf = 
-    (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_exec (rec_accum rf) (xs @ [x]) = 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_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
-
-text {*
-  The correctness of @{text "rec_all"}.
-  *}
-lemma all_lemma: 
-  "\<lbrakk>primerec rf (Suc (length xs));
-    primerec rt (length xs)\<rbrakk>
-  \<Longrightarrow> rec_exec (rec_all rt rf) xs = (if (\<forall> x \<le> (rec_exec rt xs). 0 < rec_exec rf (xs @ [x])) then 1
-                                                                                              else 0)"
-apply(auto simp: rec_all.simps)
-apply(simp add: rec_exec.simps map_append get_fstn_args_take split: if_splits)
-apply(drule_tac x = "rec_exec rt xs" in rec_accum_ex)
-apply(case_tac "rec_exec (rec_accum rf) (xs @ [rec_exec rt xs]) = 0", simp_all)
-apply(erule_tac exE, erule_tac x = t in allE, simp)
-apply(simp add: rec_exec.simps map_append get_fstn_args_take)
-apply(drule_tac x = "rec_exec rt xs" in rec_accum_ex)
-apply(case_tac "rec_exec (rec_accum rf) (xs @ [rec_exec rt xs]) = 0", simp, simp)
-apply(erule_tac x = x in allE, simp)
-done
-
-text {*
-  @{text "rec_ex t f (x1, x2, \<dots>, xn)"} 
-  computes the charactrization function of the following FOL formula:
-  @{text "(\<exists> x \<le> t(x1, x2, \<dots>, xn). (f(x1, x2, \<dots>, xn, x) > 0))"}
-*}
-fun rec_ex :: "recf \<Rightarrow> recf \<Rightarrow> recf"
-  where
-  "rec_ex rt rf = 
-       (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_exec (rec_sigma rf) (xs @ [x]) = 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_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_exec (rec_ex rt rf) xs =
-    (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_exec.simps map_append get_fstn_args_take 
-            split: if_splits)
-apply(drule_tac x = "rec_exec rt xs" in rec_sigma_ex, simp)
-apply(drule_tac x = "rec_exec rt xs" in rec_sigma_ex, simp)
-done
-
-text {*
-  Defintiion of @{text "Min[R]"} on page 77 of Boolos's book.
-*}
-
-fun Minr :: "(nat list \<Rightarrow> bool) \<Rightarrow> nat list \<Rightarrow> nat \<Rightarrow> nat"
-  where "Minr Rr xs w = (let setx = {y | y. (y \<le> w) \<and> Rr (xs @ [y])} in 
-                        if (setx = {}) then (Suc w)
-                                       else (Min setx))"
-
-declare Minr.simps[simp del] rec_all.simps[simp del]
-
-text {*
-  The following is a set of auxilliary lemmas about @{text "Minr"}.
-*}
-lemma Minr_range: "Minr Rr xs w \<le> w \<or> Minr Rr xs w = Suc w"
-apply(auto simp: Minr.simps)
-apply(subgoal_tac "Min {x. x \<le> w \<and> Rr (xs @ [x])} \<le> x")
-apply(erule_tac order_trans, simp)
-apply(rule_tac Min_le, auto)
-done
-
-lemma [simp]: "{x. x \<le> Suc w \<and> Rr (xs @ [x])}
-    = (if Rr (xs @ [Suc w]) then insert (Suc w) 
-                              {x. x \<le> w \<and> Rr (xs @ [x])}
-      else {x. x \<le> w \<and> Rr (xs @ [x])})"
-by(auto, case_tac "x = Suc w", auto)
-
-lemma [simp]: "Minr Rr xs w \<le> w \<Longrightarrow> Minr Rr xs (Suc w) = Minr Rr xs w"
-apply(simp add: Minr.simps, auto)
-apply(case_tac "\<forall>x\<le>w. \<not> Rr (xs @ [x])", auto)
-done
-
-lemma [simp]: "\<forall>x\<le>w. \<not> Rr (xs @ [x]) \<Longrightarrow>  
-                           {x. x \<le> w \<and> Rr (xs @ [x])} = {} "
-by auto
-
-lemma [simp]: "\<lbrakk>Minr Rr xs w = Suc w; Rr (xs @ [Suc w])\<rbrakk> \<Longrightarrow> 
-                                       Minr Rr xs (Suc w) = Suc w"
-apply(simp add: Minr.simps)
-apply(case_tac "\<forall>x\<le>w. \<not> Rr (xs @ [x])", auto)
-done
- 
-lemma [simp]: "\<lbrakk>Minr Rr xs w = Suc w; \<not> Rr (xs @ [Suc w])\<rbrakk> \<Longrightarrow> 
-                                   Minr Rr xs (Suc w) = Suc (Suc w)"
-apply(simp add: Minr.simps)
-apply(case_tac "\<forall>x\<le>w. \<not> Rr (xs @ [x])", auto)
-apply(subgoal_tac "Min {x. x \<le> w \<and> Rr (xs @ [x])} \<in> 
-                                {x. x \<le> w \<and> Rr (xs @ [x])}", simp)
-apply(rule_tac Min_in, auto)
-done
-
-lemma Minr_Suc_simp: 
-   "Minr Rr xs (Suc w) = 
-      (if Minr Rr xs w \<le> w then Minr Rr xs w
-       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_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)) (Cn (Suc vl) 
-              rec_not [Cn (Suc vl) rf 
-                    (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)
-
-lemma length_app:
-  "(length (get_fstn_args (arity rf - Suc 0)
-                           (arity rf - Suc 0)
-   @ [Cn (arity rf - Suc 0) (constn 0)
-           [recf.id (arity rf - Suc 0) 0]]))
-    = (Suc (arity rf - Suc 0))"
-  apply(simp)
-done
-
-lemma primerec_accum: "primerec (rec_accum rf) n \<Longrightarrow> primerec rf n"
-apply(auto simp: rec_accum.simps Let_def)
-apply(erule_tac prime_pr_reverse, simp)
-apply(erule_tac prime_cn_reverse, simp only: length_app)
-done
-
-lemma primerec_all: "primerec (rec_all rt rf) n \<Longrightarrow>
-                       primerec rt n \<and> primerec rf (Suc n)"
-apply(simp add: rec_all.simps Let_def)
-apply(erule_tac prime_cn_reverse, simp)
-apply(erule_tac prime_cn_reverse, simp)
-apply(erule_tac x = n in allE, simp add: nth_append primerec_accum)
-done
-
-lemma min_Suc_Suc[simp]: "min (Suc (Suc x)) x = x"
- by auto
-
-declare numeral_3_eq_3[simp]
-
-lemma [intro]: "primerec rec_pred (Suc 0)"
-apply(simp add: rec_pred_def)
-apply(rule_tac prime_cn, auto)
-apply(case_tac i, auto intro: prime_id)
-done
-
-lemma [intro]: "primerec rec_minus (Suc (Suc 0))"
-  apply(auto simp: rec_minus_def)
-  done
-
-lemma [intro]: "primerec (constn n) (Suc 0)"
-  apply(induct n)
-  apply(auto simp: constn.simps intro: prime_z prime_cn prime_s)
-  done
-
-lemma [intro]: "primerec rec_sg (Suc 0)" 
-  apply(simp add: rec_sg_def)
-  apply(rule_tac k = "Suc (Suc 0)" in prime_cn, auto)
-  apply(case_tac i, auto)
-  apply(case_tac ia, auto intro: prime_id)
-  done
-
-lemma [simp]: "length (get_fstn_args m n) = n"
-  apply(induct n)
-  apply(auto simp: get_fstn_args.simps)
-  done
-
-lemma  primerec_getpren[elim]: "\<lbrakk>i < n; n \<le> m\<rbrakk> \<Longrightarrow> primerec (get_fstn_args m n ! i) m"
-apply(induct n, auto simp: get_fstn_args.simps)
-apply(case_tac "i = n", auto simp: nth_append intro: prime_id)
-done
-
-lemma [intro]: "primerec rec_add (Suc (Suc 0))"
-apply(simp add: rec_add_def)
-apply(rule_tac prime_pr, auto)
-done
-
-lemma [intro]:"primerec rec_mult (Suc (Suc 0))"
-apply(simp add: rec_mult_def )
-apply(rule_tac prime_pr, auto intro: prime_z)
-apply(case_tac i, auto intro: prime_id)
-done  
-
-lemma [elim]: "\<lbrakk>primerec rf n; n \<ge> Suc (Suc 0)\<rbrakk>   \<Longrightarrow> 
-                        primerec (rec_accum rf) n"
-apply(auto simp: rec_accum.simps)
-apply(simp add: nth_append, auto)
-apply(case_tac i, auto intro: prime_id)
-apply(auto simp: nth_append)
-done
-
-lemma primerec_all_iff: 
-  "\<lbrakk>primerec rt n; primerec rf (Suc n); n > 0\<rbrakk> \<Longrightarrow> 
-                                 primerec (rec_all rt rf) n"
-  apply(simp add: rec_all.simps, auto)
-  apply(auto, simp add: nth_append, auto)
-  done
-
-lemma [simp]: "Rr (xs @ [0]) \<Longrightarrow> 
-                   Min {x. x = (0::nat) \<and> Rr (xs @ [x])} = 0"
-by(rule_tac Min_eqI, simp, simp, simp)
-
-lemma [intro]: "primerec rec_not (Suc 0)"
-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_exec rf (xs @ [uu])} \<le> w;
-       x \<le> w; 0 < rec_exec rf (xs @ [x])\<rbrakk>
-      \<Longrightarrow>  False"
-apply(subgoal_tac "finite {uu. uu \<le> w \<and> 0 < rec_exec rf (xs @ [uu])}")
-apply(subgoal_tac "{uu. uu \<le> w \<and> 0 < rec_exec rf (xs @ [uu])} \<noteq> {}")
-apply(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_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_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) @ 
-                [recf.id (Suc (Suc (length xs))) 
-    (Suc ((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_exec (rec_all ?rt ?rf)) (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_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)))"
-  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 ind:
-    "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_exec (rec_all ?rt ?rf))
-         (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_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: "
-  \<lbrakk>primerec rf (Suc (length xs))\<rbrakk> 
-     \<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_exec (rec_Minr rf) (xs @ [w]) = 
-    Minr (\<lambda> args. (0 < rec_exec rf args)) xs w"
-    apply(simp add: rec_exec.simps rec_Minr.simps arity.simps Let_def 
-                    sigma_lemma all_lemma)
-    apply(rule_tac  sigma_minr_lemma)
-    apply(simp add: h)
-    done
-qed
-    
-text {* 
-  @{text "rec_le"} is the comparasion function 
-  which compares its two arguments, testing whether the 
-  first is less or equal to the second.
-  *}
-definition rec_le :: "recf"
-  where
-  "rec_le = Cn (Suc (Suc 0)) rec_disj [rec_less, rec_eq]"
-
-text {*
-  The correctness of @{text "rec_le"}.
-  *}
-lemma le_lemma: 
-  "\<And>x y. rec_exec rec_le [x, y] = (if (x \<le> y) then 1 else 0)"
-by(auto simp: rec_le_def rec_exec.simps)
-
-text {*
-  Defintiion of @{text "Max[Rr]"} on page 77 of Boolos's book.
-*}
-
-fun Maxr :: "(nat list \<Rightarrow> bool) \<Rightarrow> nat list \<Rightarrow> nat \<Rightarrow> nat"
-  where
-  "Maxr Rr xs w = (let setx = {y. y \<le> w \<and> Rr (xs @[y])} in 
-                  if setx = {} then 0
-                  else Max setx)"
-
-text {*
-  @{text "rec_maxr"} is the recursive function 
-  used to implementation @{text "Maxr"}.
-  *}
-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
-                  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
-                  let rf = Cn (Suc (Suc vl)) rec_disj [rf1, rf2] in
-                  let rq = rec_all rt rf  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)]))"
-
-declare rec_maxr.simps[simp del] Maxr.simps[simp del] 
-declare le_lemma[simp]
-lemma [simp]: "(min (Suc (Suc (Suc (x)))) (x)) = x"
-by simp
-
-declare numeral_2_eq_2[simp]
-
-lemma [intro]: "primerec rec_disj (Suc (Suc 0))"
-  apply(simp add: rec_disj_def, auto)
-  apply(auto)
-  apply(case_tac ia, auto intro: prime_id)
-  done
-
-lemma [intro]: "primerec rec_less (Suc (Suc 0))"
-  apply(simp add: rec_less_def, auto)
-  apply(auto)
-  apply(case_tac ia , auto intro: prime_id)
-  done
-
-lemma [intro]: "primerec rec_eq (Suc (Suc 0))"
-  apply(simp add: rec_eq_def)
-  apply(rule_tac prime_cn, auto)
-  apply(case_tac i, auto)
-  apply(case_tac ia, auto)
-  apply(case_tac [!] i, auto intro: prime_id)
-  done
-
-lemma [intro]: "primerec rec_le (Suc (Suc 0))"
-  apply(simp add: rec_le_def)
-  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]"
-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)"
-apply(auto simp: Maxr.simps)
-apply(rule_tac max_absorb1)
-apply(subgoal_tac "(Max {y. y \<le> w \<and> Rr (xs @ [y])} \<le> (Suc w)) =
-  (\<forall>a\<in>{y. y \<le> w \<and> Rr (xs @ [y])}. a \<le> (Suc w))", simp)
-apply(rule_tac Max_le_iff, 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"
-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"
-apply(induct w)
-apply(simp add: Sigma.simps, simp)
-apply(simp add: Sigma.simps)
-done
-
-lemma Sigma_max_point: "\<lbrakk>\<forall> k < ma. f (xs @ [k]) = 1;
-        \<forall> k \<ge> ma. f (xs @ [k]) = 0; ma \<le> w\<rbrakk>
-    \<Longrightarrow> Sigma f (xs @ [w]) = ma"
-apply(induct w, auto)
-apply(rule_tac Sigma_0, simp)
-apply(simp add: Sigma_Suc_simp_rewrite)
-apply(case_tac "ma = Suc w", auto)
-done
-
-lemma Sigma_Max_lemma: 
-  assumes prrf: "primerec rf (Suc (length xs))"
-  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_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 
-    (Suc (Suc (Suc (length xs)))) ((Suc (length xs)))]"
-  let ?rf2 = "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))))])"
-  let ?rf3 = "Cn (Suc (Suc (Suc (length xs)))) rec_not [?rf2]"
-  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_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_exec ?notrq) ((xs@[w])@[w]) = 0"
-      apply(rule_tac Sigma_0)
-      apply(auto simp: rec_exec.simps all_lemma
-                       get_fstn_args_take nth_append h)
-      done
-    thus "UF.Sigma (rec_exec ?notrq)
-      (xs @ [w, w]) = 0"
-      by simp
-  next
-    fix x
-    assume h: "x \<le> w" "0 < rec_exec rf (xs @ [x])"
-    hence "\<exists> ma. Max {y. y \<le> w \<and> 0 < rec_exec rf (xs @ [y])} = ma"
-      by auto
-    from this obtain ma where k1: 
-      "Max {y. y \<le> w \<and> 0 < rec_exec rf (xs @ [y])} = ma" ..
-    hence k2: "ma \<le> w \<and> 0 < rec_exec rf (xs @ [ma])"
-      using h
-      apply(subgoal_tac
-        "Max {y. y \<le> w \<and> 0 < rec_exec rf (xs @ [y])} \<in>  {y. y \<le> w \<and> 0 < rec_exec rf (xs @ [y])}")
-      apply(erule_tac CollectE, simp)
-      apply(rule_tac Max_in, auto)
-      done
-    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_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_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_exec.simps all_lemma get_fstn_args_take nth_append)
-      apply(subgoal_tac "x \<le> Max {y. y \<le> w \<and> 0 < rec_exec rf (xs @ [y])}",
-        simp add: k1)
-      apply(rule_tac Max_ge, auto)
-      using prrf
-      apply(case_tac i, auto)
-      apply(case_tac ia, auto simp: h nth_append)
-      done 
-    from k3 k4 k1 have "Sigma (rec_exec ?notrq) ((xs @ [w]) @ [w]) = ma"
-      apply(rule_tac Sigma_max_point, simp, simp, simp add: k2)
-      done
-    from k1 and this show "Sigma (rec_exec ?notrq) (xs @ [w, w]) =
-      Max {y. y \<le> w \<and> 0 < rec_exec rf (xs @ [y])}"
-      by simp
-  qed  
-qed
-
-text {*
-  The correctness of @{text "rec_maxr"}.
-  *}
-lemma Maxr_lemma:
- assumes h: "primerec rf (Suc (length xs))"
- shows   "rec_exec (rec_maxr rf) (xs @ [w]) = 
-            Maxr (\<lambda> args. 0 < rec_exec rf args) xs w"
-proof -
-  from h have "arity rf = Suc (length xs)"
-    by auto
-  thus "?thesis"
-  proof(simp add: rec_exec.simps rec_maxr.simps nth_append get_fstn_args_take)
-    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)))]"
-    let ?rf2 = "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))))])"
-    let ?rf3 = "Cn (Suc (Suc (Suc (length xs)))) rec_not [?rf2]"
-    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]"
-    have prt: "primerec ?rt (Suc (Suc (length xs)))"
-      by(auto intro: prime_id)
-    have prrf: "primerec ?rf (Suc (Suc (Suc (length xs))))"
-      apply(auto)
-      apply(case_tac i, auto)
-      apply(case_tac ia, auto intro: prime_id)
-      apply(simp add: h)
-      apply(simp add: nth_append, auto intro: prime_id)
-      done
-    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_exec (rec_sigma ?notrq) ((xs @ [w]) @ [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_exec (rec_sigma ?notrq)
-     (xs @ [w, 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] = (let Rr = 
-                         (\<lambda> zs. ((zs ! (Suc 0) * zs ! (Suc (Suc 0))
-                                 \<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"}:
-  *}
-lemma [elim!]: "y > 0 \<Longrightarrow> quo [x, y] = x div y"
-proof(simp add: quo.simps Maxr.simps, auto,
-      rule_tac Max_eqI, simp, auto)
-  fix xa ya
-  assume h: "y * ya \<le> x"  "y > 0"
-  hence "(y * ya) div y \<le> x div y"
-    by(insert div_le_mono[of "y * ya" x y], simp)
-  from this and h show "ya \<le> x div y" by simp
-next
-  fix xa
-  show "y * (x div y) \<le> x"
-    apply(subgoal_tac "y * (x div y) + x mod y = x")
-    apply(rule_tac k = "x mod y" in add_leD1, simp)
-    apply(simp)
-    done
-qed
-
-lemma [intro]: "quo [x, 0] = 0"
-by(simp add: quo.simps Maxr.simps)
-
-lemma quo_div: "quo [x, y] = x div y"  
-by(case_tac "y=0", auto)
-
-text {*
-  @{text "rec_noteq"} is the recursive function testing whether its
-  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))]]"
-
-text {*
-  The correctness of @{text "rec_noteq"}.
-  *}
-lemma noteq_lemma: 
-  "\<And> x y. rec_exec rec_noteq [x, y] = 
-               (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"}
-  *}
-definition rec_quo :: "recf"
-  where
-  "rec_quo = (let rR = Cn (Suc (Suc (Suc 0))) rec_conj
-              [Cn (Suc (Suc (Suc 0))) rec_le 
-               [Cn (Suc (Suc (Suc 0))) rec_mult 
-                  [id (Suc (Suc (Suc 0))) (Suc 0), 
-                     id (Suc (Suc (Suc 0))) ((Suc (Suc 0)))],
-                id (Suc (Suc (Suc 0))) (0)], 
-                Cn (Suc (Suc (Suc 0))) rec_noteq 
-                         [id (Suc (Suc (Suc 0))) (Suc (0)),
-                Cn (Suc (Suc (Suc 0))) (constn 0) 
-                              [id (Suc (Suc (Suc 0))) (0)]]] 
-              in Cn (Suc (Suc 0)) (rec_maxr rR)) [id (Suc (Suc 0)) 
-                           (0),id (Suc (Suc 0)) (Suc (0)), 
-                                   id (Suc (Suc 0)) (0)]"
-
-lemma [intro]: "primerec rec_conj (Suc (Suc 0))"
-  apply(simp add: rec_conj_def)
-  apply(rule_tac prime_cn, auto)+
-  apply(case_tac i, auto intro: prime_id)
-  done
-
-lemma [intro]: "primerec rec_noteq (Suc (Suc 0))"
-apply(simp add: rec_noteq_def)
-apply(rule_tac prime_cn, auto)+
-apply(case_tac i, auto intro: prime_id)
-done
-
-
-lemma quo_lemma1: "rec_exec rec_quo [x, y] = quo [x, y]"
-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_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_exec (rec_maxr ?rR) ([x, y,  x]) =
-             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_exec ?rR args = 0 then False
-                           else True) [x, y] x = quo [x, y]"
-    apply(simp add: rec_exec.simps)
-    apply(simp add: Maxr.simps quo.simps, auto)
-    done
-  from g1 and g2 show 
-    "rec_exec (rec_maxr ?rR) ([x, y,  x]) = quo [x, y]"
-    by simp
-qed
-
-text {*
-  The correctness of @{text "quo"}.
-  *}
-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 
-  the reminder function.
-  *}
-definition rec_mod :: "recf"
-  where
-  "rec_mod = Cn (Suc (Suc 0)) rec_minus [id (Suc (Suc 0)) (0), 
-               Cn (Suc (Suc 0)) rec_mult [rec_quo, id (Suc (Suc 0))
-                                                     (Suc (0))]]"
-
-text {*
-  The correctness of @{text "rec_mod"}:
-  *}
-lemma mod_lemma: "\<And> x y. rec_exec rec_mod [x, y] = (x mod y)"
-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
-
-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
-  page 79 of Boolos's book.
-  *}
-fun Embranch :: "(ftype * rtype) list \<Rightarrow> nat list \<Rightarrow> nat"
-  where
-  "Embranch [] xs = 0" |
-  "Embranch (gc # gcs) xs = (
-                   let (g, c) = gc in 
-                   if c xs then g xs else Embranch gcs xs)"
-
-fun rec_embranch' :: "(recf * recf) list \<Rightarrow> nat \<Rightarrow> recf"
-  where
-  "rec_embranch' [] vl = Cn vl z [id vl (vl - 1)]" |
-  "rec_embranch' ((rg, rc) # rgcs) vl = Cn vl rec_add
-                   [Cn vl rec_mult [rg, rc], rec_embranch' rgcs vl]"
-
-text {*
-  @{text "rec_embrach"} is the recursive function used to implement
-  @{text "Embranch"}.
-  *}
-fun rec_embranch :: "(recf * recf) list \<Rightarrow> recf"
-  where
-  "rec_embranch ((rg, rc) # rgcs) = 
-         (let vl = arity rg in 
-          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_exec (rcs ! j) xs = 0;
-    length rgs = length rcs;  
-  rcs \<noteq> []; 
-  list_all (\<lambda> rf. primerec rf (length xs)) (rgs @ rcs)\<rbrakk>  \<Longrightarrow> 
-  rec_exec (rec_embranch (zip rgs rcs)) xs = 0"
-proof(induct rcs arbitrary: rgs, simp, case_tac rgs, simp)
-  fix a rcs rgs aa list
-  assume ind: 
-    "\<And>rgs. \<lbrakk>\<forall>j<length rcs. rec_exec (rcs ! j) xs = 0; 
-             length rgs = length rcs; rcs \<noteq> []; 
-            list_all (\<lambda>rf. primerec rf (length xs)) (rgs @ rcs)\<rbrakk> \<Longrightarrow> 
-                      rec_exec (rec_embranch (zip rgs rcs)) xs = 0"
-  and h:  "\<forall>j<length (a # rcs). rec_exec ((a # rcs) ! j) xs = 0"
-  "length rgs = length (a # rcs)" 
-    "a # rcs \<noteq> []" 
-    "list_all (\<lambda>rf. primerec rf (length xs)) (rgs @ a # rcs)"
-    "rgs = aa # list"
-  have g: "rcs \<noteq> [] \<Longrightarrow> rec_exec (rec_embranch (zip list rcs)) xs = 0"
-    using h
-    by(rule_tac ind, auto)
-  show "rec_exec (rec_embranch (zip rgs (a # rcs))) xs = 0"
-  proof(case_tac "rcs = []", simp)
-    show "rec_exec (rec_embranch (zip rgs [a])) xs = 0"
-      using h
-      apply(simp add: rec_embranch.simps rec_exec.simps)
-      apply(erule_tac x = 0 in allE, simp)
-      done
-  next
-    assume "rcs \<noteq> []"
-    hence "rec_exec (rec_embranch (zip list rcs)) xs = 0"
-      using g by simp
-    thus "rec_exec (rec_embranch (zip rgs (a # rcs))) xs = 0"
-      using h
-      apply(simp add: rec_embranch.simps rec_exec.simps)
-      apply(case_tac rcs,
-        auto simp: rec_exec.simps rec_embranch.simps)
-      apply(case_tac list,
-        auto simp: rec_exec.simps rec_embranch.simps)
-      done
-  qed
-qed     
- 
-
-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_exec (rec_embranch ((a, aa) # zip rgs list)) xs
-         = rec_exec (rec_embranch (zip rgs list)) xs"
-apply(simp add: rec_exec.simps rec_embranch.simps)
-apply(case_tac "zip rgs list", simp, case_tac ab, 
-  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
-
-lemma zip_null_iff: "\<lbrakk>length xs = k; length ys = k; zip xs ys = []\<rbrakk> \<Longrightarrow> xs = [] \<and> ys = []"
-apply(case_tac xs, simp, simp)
-apply(case_tac ys, simp, simp)
-done
-
-lemma zip_null_gr: "\<lbrakk>length xs = k; length ys = k; zip xs ys \<noteq> []\<rbrakk> \<Longrightarrow> 0 < k"
-apply(case_tac xs, simp, simp)
-done
-
-lemma Embranch_0:  
-  "\<lbrakk>length rgs = k; length rcs = k; k > 0; 
-  \<forall> j < k. rec_exec (rcs ! j) xs = 0\<rbrakk> \<Longrightarrow>
-  Embranch (zip (map rec_exec rgs) (map (\<lambda>r args. 0 < rec_exec r args) rcs)) xs = 0"
-proof(induct rgs arbitrary: rcs k, simp, simp)
-  fix a rgs rcs k
-  assume ind: 
-    "\<And>rcs k. \<lbrakk>length rgs = k; length rcs = k; 0 < k; \<forall>j<k. rec_exec (rcs ! j) xs = 0\<rbrakk> 
-    \<Longrightarrow> Embranch (zip (map rec_exec rgs) (map (\<lambda>r args. 0 < rec_exec r args) rcs)) xs = 0"
-  and h: "Suc (length rgs) = k" "length rcs = k"
-    "\<forall>j<k. rec_exec (rcs ! j) xs = 0"
-  from h show  
-    "Embranch (zip (rec_exec a # map rec_exec rgs) 
-           (map (\<lambda>r args. 0 < rec_exec r args) rcs)) xs = 0"
-    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)
-    apply(rule_tac ind, simp, simp, simp, auto)
-    apply(erule_tac x = "Suc j" in allE, simp)
-    done
-qed
-
-text {*
-  The correctness of @{text "rec_embranch"}.
-  *}
-lemma embranch_lemma:
-  assumes branch_num:
-  "length rgs = n" "length rcs = n" "n > 0"
-  and partition: 
-  "(\<exists> i < n. (rec_exec (rcs ! i) xs = 1 \<and> (\<forall> j < n. j \<noteq> i \<longrightarrow> 
-                                      rec_exec (rcs ! j) xs = 0)))"
-  and prime_all: "list_all (\<lambda> rf. primerec rf (length xs)) (rgs @ rcs)"
-  shows "rec_exec (rec_embranch (zip rgs rcs)) xs =
-                  Embranch (zip (map rec_exec rgs) 
-                     (map (\<lambda> r args. 0 < rec_exec r args) rcs)) xs"
-  using branch_num partition prime_all
-proof(induct rgs arbitrary: rcs n, simp)
-  fix a rgs rcs n
-  assume ind: 
-    "\<And>rcs n. \<lbrakk>length rgs = n; length rcs = n; 0 < n;
-    \<exists>i<n. rec_exec (rcs ! i) xs = 1 \<and> (\<forall>j<n. j \<noteq> i \<longrightarrow> rec_exec (rcs ! j) xs = 0);
-    list_all (\<lambda>rf. primerec rf (length xs)) (rgs @ rcs)\<rbrakk>
-    \<Longrightarrow> rec_exec (rec_embranch (zip rgs rcs)) xs =
-    Embranch (zip (map rec_exec rgs) (map (\<lambda>r args. 0 < rec_exec r args) rcs)) xs"
-  and h: "length (a # rgs) = n" "length (rcs::recf list) = n" "0 < n"
-         " \<exists>i<n. rec_exec (rcs ! i) xs = 1 \<and> 
-         (\<forall>j<n. j \<noteq> i \<longrightarrow> rec_exec (rcs ! j) xs = 0)" 
-    "list_all (\<lambda>rf. primerec rf (length xs)) ((a # rgs) @ rcs)"
-  from h show "rec_exec (rec_embranch (zip (a # rgs) rcs)) xs =
-    Embranch (zip (map rec_exec (a # rgs)) (map (\<lambda>r args. 
-                0 < rec_exec r args) rcs)) xs"
-    apply(case_tac rcs, simp, simp)
-    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_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_exec ((aa # list) ! i) xs = Suc 0 \<and> 
-          (\<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_exec aa xs = 0" "rcs = aa # list" "zip rgs list \<noteq> []"
-    have "rec_exec (rec_embranch ((a, aa) # zip rgs list)) xs
-        = rec_exec (rec_embranch (zip rgs list)) xs"
-      apply(rule embranch_exec_0, simp_all add: g)
-      done
-    from g and this show "rec_exec (rec_embranch ((a, aa) # zip rgs list)) xs =
-         Embranch ((rec_exec a, \<lambda>args. 0 < rec_exec aa args) # 
-           zip (map rec_exec rgs) (map (\<lambda>r args. 0 < rec_exec r args) list)) xs"
-      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(auto)
-      apply(case_tac i, simp, simp)
-      apply(rule_tac x = nat in exI, simp)
-      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_exec ((aa # list) ! i) xs = Suc 0 \<and> 
-      (\<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_exec aa xs \<noteq> 0" "zip rgs list = []"
-    thus "rec_exec (rec_embranch ((a, aa) # zip rgs list)) xs = 
-        Embranch ((rec_exec a, \<lambda>args. 0 < rec_exec aa args) # 
-       zip (map rec_exec rgs) (map (\<lambda>r args. 0 < rec_exec r args) list)) xs"
-      apply(subgoal_tac "rgs = [] \<and> list = []", simp)
-      prefer 2
-      apply(rule_tac zip_null_iff, simp, simp, simp)
-      apply(simp add: rec_exec.simps rec_embranch.simps Embranch.simps, auto)
-      done
-  next
-    fix aa list
-    assume g: "Suc (length rgs) = n" "Suc (length list) = n"
-      "\<exists>i<n. rec_exec ((aa # list) ! i) xs = Suc 0 \<and>  
-           (\<forall>j<n. j \<noteq> i \<longrightarrow> rec_exec ((aa # list) ! j) xs = 0)"
-      "primerec a (length xs) \<and> list_all (\<lambda>rf. primerec rf (length xs)) rgs
-      \<and> primerec aa (length xs) \<and> list_all (\<lambda>rf. primerec rf (length xs)) list"
-      "rcs = aa # list" "rec_exec aa xs \<noteq> 0" "zip rgs list \<noteq> []"
-    have "rec_exec aa xs =  Suc 0"
-      using g
-      apply(case_tac "rec_exec aa xs", simp, auto)
-      done      
-    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_exec (rec_embranch (zip rgs list)) xs = 0"
-      proof(rule embranch_all0)
-        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)
-          apply(erule_tac x = 0 in allE, simp)
-          done
-      next
-        show "length rgs = length list"
-          using g
-          apply(case_tac n, simp, simp)
-          done
-      next
-        show "list \<noteq> []"
-          using g
-          apply(case_tac list, simp, simp)
-          done
-      next
-        show "list_all (\<lambda>rf. primerec rf (length xs)) (rgs @ list)"
-          using g
-          apply auto
-          done
-      qed
-      ultimately show "rec_exec (rec_embranch' (zip rgs list) (length xs)) xs = 0"
-        by simp
-    qed
-    moreover have 
-      "Embranch (zip (map rec_exec rgs) 
-          (map (\<lambda>r args. 0 < rec_exec r args) list)) xs = 0"
-      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)
-      apply(case_tac i, simp)
-      apply(erule_tac x = "Suc j" in allE, simp)
-      apply(simp)
-      apply(rule_tac x = 0 in allE, auto)
-      done
-    moreover have "arity a = length xs"
-      using g
-      apply(auto)
-      done
-    ultimately show "rec_exec (rec_embranch ((a, aa) # zip rgs list)) xs = 
-      Embranch ((rec_exec a, \<lambda>args. 0 < rec_exec aa args) #
-           zip (map rec_exec rgs) (map (\<lambda>r args. 0 < rec_exec r args) list)) xs"
-      apply(simp add: rec_exec.simps rec_embranch.simps Embranch.simps)
-      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)
-
-lemma primerec_all2: "primerec (rec_all rt rf) n \<Longrightarrow> 
-  primerec rf (Suc n)"
-by(insert primerec_all[of rt rf n], simp)
-
-text {*
-  @{text "rec_prime"} is the recursive function used to implement
-  @{text "Prime"}.
-  *}
-definition rec_prime :: "recf"
-  where
-  "rec_prime = Cn (Suc 0) rec_conj 
-  [Cn (Suc 0) rec_less [constn 1, id (Suc 0) (0)],
-        rec_all (Cn 1 rec_minus [id 1 0, constn 1]) 
-       (rec_all (Cn 2 rec_minus [id 2 0, Cn 2 (constn 1) 
-  [id 2 0]]) (Cn 3 rec_noteq 
-       [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_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_exec (Cn 2 rec_minus [recf.id 2 0, Cn 2 (constn (Suc 0)) [recf.id 2 0]]) ([x, k]). 
-  0 < rec_exec (Cn 3 rec_noteq [Cn 3 rec_mult [recf.id 3 (Suc 0), recf.id 3 2], recf.id 3 0])
-  ([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_exec rec_prime [x] = (if Prime x then 1 else 0)"
-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_exec (rec_all ?rt2 ?rf2) ([x]) = 
-        (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(case_tac ia, auto simp: numeral_3_eq_3)
-      done
-  next
-    show "primerec (Cn (Suc 0) rec_minus
-             [recf.id (Suc 0) 0, constn (Suc 0)]) (Suc 0)"
-      apply(auto)
-      apply(case_tac i, auto)
-      done
-  qed
-  from h1 show 
-   "(Suc 0 < x \<longrightarrow>  (rec_exec (rec_all ?rt2 ?rf2) [x] = 0 \<longrightarrow> 
-    \<not> Prime x) \<and>
-     (0 < rec_exec (rec_all ?rt2 ?rf2) [x] \<longrightarrow> Prime x)) \<and>
-    (\<not> Suc 0 < x \<longrightarrow> \<not> Prime x \<and> (rec_exec (rec_all ?rt2 ?rf2) [x] = 0
-    \<longrightarrow> \<not> Prime x))"
-    apply(auto simp:rec_exec.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"
-      apply(simp add: rec_exec.simps split: if_splits)
-      apply(simp add: Prime.simps, auto)
-      apply(erule_tac x = u in allE, auto)
-      apply(case_tac u, 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"
-    thus "False"
-      apply(simp add: Prime.simps)
-      done
-  next
-    fix k
-    assume "rec_exec (rec_all ?rt1 ?rf1)
-      [x, k] = 0" "k \<le> x - Suc 0" "Prime x"
-    thus "False"
-      apply(simp add: exec_tmp rec_exec.simps Prime.simps split: if_splits)
-      done
-  next
-    fix k
-    assume "rec_exec (rec_all ?rt1 ?rf1)
-      [x, k] = 0" "k \<le> x - Suc 0" "Prime x"
-    thus "False"
-      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]])"
-
-text {*
-  The recursive function used to implment factorization.
-  *}
-definition rec_fac :: "recf"
-  where
-  "rec_fac = Cn 1 rec_dummyfac [id 1 0, id 1 0]"
-
-text {*
-  Formal specification of factorization.
-  *}
-fun fac :: "nat \<Rightarrow> nat"  ("_!" [100] 99)
-  where
-  "fac 0 = 1" |
-  "fac (Suc x) = (Suc x) * fac x"
-
-lemma [simp]: "rec_exec rec_dummyfac [0, 0] = Suc 0"
-by(simp add: rec_dummyfac_def rec_exec.simps)
-
-lemma rec_cn_simp: "rec_exec (Cn n f gs) xs = 
-                (let rgs = map (\<lambda> g. rec_exec g xs) gs in
-                 rec_exec f rgs)"
-by(simp add: rec_exec.simps)
-
-lemma rec_id_simp: "rec_exec (id m n) xs = xs ! n" 
-  by(simp add: rec_exec.simps)
-
-lemma fac_dummy: "rec_exec rec_dummyfac [x, y] = y !"
-apply(induct y)
-apply(auto simp: rec_dummyfac_def rec_exec.simps)
-done
-
-text {*
-  The correctness of @{text "rec_fac"}.
-  *}
-lemma fac_lemma: "rec_exec rec_fac [x] =  x!"
-apply(simp add: rec_fac_def rec_exec.simps fac_dummy)
-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}"
-
-declare Np.simps[simp del] rec_Minr.simps[simp del]
-
-text {*
-  @{text "rec_np"} is the recursive function used to implement
-  @{text "Np"}.
-  *}
-definition rec_np :: "recf"
-  where
-  "rec_np = (let Rr = Cn 2 rec_conj [Cn 2 rec_less [id 2 0, id 2 1], 
-  Cn 2 rec_prime [id 2 1]]
-             in Cn 1 (rec_Minr Rr) [id 1 0, Cn 1 s [rec_fac]])"
-
-lemma [simp]: "n < Suc (n!)"
-apply(induct n, simp)
-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))"
- by(auto simp: Prime.simps)
-
-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(rule_tac x = u in exI, simp, auto)
-done
-
-lemma [intro]: "0 < n!"
-apply(induct n)
-apply(auto simp: fac.simps)
-done
-
-lemma fac_Suc: "Suc n! =  (Suc n) * (n!)" by(simp add: fac.simps)
-
-lemma fac_dvd: "\<lbrakk>0 < q; q \<le> n\<rbrakk> \<Longrightarrow> q dvd n!"
-apply(induct n, simp)
-apply(case_tac "q \<le> n", simp add: fac_Suc)
-apply(subgoal_tac "q = Suc n", simp only: fac_Suc)
-apply(rule_tac dvd_mult2, simp, simp)
-done
-
-lemma fac_dvd2: "\<lbrakk>Suc 0 < q; q dvd n!; q \<le> n\<rbrakk> \<Longrightarrow> \<not> q dvd Suc (n!)"
-proof(auto simp: dvd_def)
-  fix k ka
-  assume h1: "Suc 0 < q" "q \<le> n"
-  and h2: "Suc (q * k) = q * ka"
-  have "k < ka"
-  proof - 
-    have "q * k < q * ka" 
-      using h2 by arith
-    thus "k < ka"
-      using h1
-      by(auto)
-  qed
-  hence "\<exists>d. d > 0 \<and>  ka = d + k"  
-    by(rule_tac x = "ka - k" in exI, simp)
-  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"
-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)"  
-  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)" ..
-  thus "?thesis"
-  proof(cases "q > n")
-    case True thus "?thesis"
-      using k
-      apply(rule_tac x = q in exI, auto)
-      apply(rule_tac dvd_imp_le, auto)
-      done
-  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.simps)
-      hence "q dvd n!"
-        using g 
-        apply(rule_tac fac_dvd, auto)
-        done
-      hence "\<not> q dvd Suc (n!)"
-        using g j
-        by(rule_tac fac_dvd2, auto)
-      thus "?thesis"
-        using k by simp
-    qed
-  qed
-qed
-  
-lemma Suc_Suc_induct[elim!]: "\<lbrakk>i < Suc (Suc 0); 
-  primerec (ys ! 0) n; primerec (ys ! 1) n\<rbrakk> \<Longrightarrow> primerec (ys ! i) n"
-by(case_tac i, auto)
-
-lemma [intro]: "primerec rec_prime (Suc 0)"
-apply(auto simp: rec_prime_def, auto)
-apply(rule_tac primerec_all_iff, auto, auto)
-apply(rule_tac primerec_all_iff, auto, auto simp:  
-  numeral_2_eq_2 numeral_3_eq_3)
-done
-
-text {*
-  The correctness of @{text "rec_np"}.
-  *}
-lemma np_lemma: "rec_exec rec_np [x] = Np x"
-proof(auto simp: rec_np_def rec_exec.simps Let_def fac_lemma)
-  let ?rr = "(Cn 2 rec_conj [Cn 2 rec_less [recf.id 2 0,
-    recf.id 2 (Suc 0)], Cn 2 rec_prime [recf.id 2 (Suc 0)]])"
-  let ?R = "\<lambda> zs. zs ! 0 < zs ! 1 \<and> Prime (zs ! 1)"
-  have g1: "rec_exec (rec_Minr ?rr) ([x] @ [Suc (x!)]) = 
-    Minr (\<lambda> args. 0 < rec_exec ?rr args) [x] (Suc (x!))"
-    by(rule_tac Minr_lemma, auto simp: rec_exec.simps
-      prime_lemma, auto simp:  numeral_2_eq_2 numeral_3_eq_3)
-  have g2: "Minr (\<lambda> args. 0 < rec_exec ?rr args) [x] (Suc (x!)) = Np x"
-    using prime_ex[of x]
-    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}
-    = {y. y \<le> Suc (x!) \<and> x < y \<and> Prime y}", auto)
-    done
-  from g1 and g2 show "rec_exec (rec_Minr ?rr) ([x, Suc (x!)]) = Np x"
-    by simp
-qed
-
-text {*
-  @{text "rec_power"} is the recursive function used to implement
-  power function.
-  *}
-definition rec_power :: "recf"
-  where
-  "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_exec rec_power [x, y] = x^y"
-  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"
-  where
-  "Pi 0 = 2" |
-  "Pi (Suc x) = Np (Pi x)"
-
-definition rec_dummy_pi :: "recf"
-  where
-  "rec_dummy_pi = Pr 1 (constn 2) (Cn 3 rec_np [id 3 2])"
-
-text {*
-  @{text "rec_pi"} is the recursive function used to implement
-  @{text "Pi"}.
-  *}
-definition rec_pi :: "recf"
-  where
-  "rec_pi = Cn 1 rec_dummy_pi [id 1 0, id 1 0]"
-
-lemma pi_dummy_lemma: "rec_exec rec_dummy_pi [x, y] = Pi y"
-apply(induct y)
-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_exec rec_pi [x] = Pi x"
-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)"
-
-declare loR.simps[simp del]
-
-text {*
-  @{text "Lo"} specifies the @{text "lo"} function given on page 79 of 
-  Boolos's book. It is one of the two notions of integeral logarithmatic
-  operation on that page. The other is @{text "lg"}.
-  *}
-fun lo :: " nat \<Rightarrow> nat \<Rightarrow> nat"
-  where 
-  "lo x y  = (if x > 1 \<and> y > 1 \<and> {u. loR [x, y, u]} \<noteq> {} then Max {u. loR [x, y, u]}
-                                                         else 0)"
-
-declare lo.simps[simp del]
-
-lemma [elim]: "primerec rf n \<Longrightarrow> n > 0"
-apply(induct rule: primerec.induct, auto)
-done
-
-lemma primerec_sigma[intro!]:  
-  "\<lbrakk>n > Suc 0; primerec rf n\<rbrakk> \<Longrightarrow> 
-  primerec (rec_sigma rf) n"
-apply(simp add: rec_sigma.simps)
-apply(auto, auto simp: nth_append)
-done
-
-lemma [intro!]:  "\<lbrakk>primerec rf n; n > 0\<rbrakk> \<Longrightarrow> primerec (rec_maxr rf) n"
-apply(simp add: rec_maxr.simps)
-apply(rule_tac prime_cn, auto)
-apply(rule_tac primerec_all_iff, auto, auto simp: nth_append)
-done
-
-lemma Suc_Suc_Suc_induct[elim!]: 
-  "\<lbrakk>i < Suc (Suc (Suc (0::nat))); primerec (ys ! 0) n;
-  primerec (ys ! 1) n;  
-  primerec (ys ! 2) n\<rbrakk> \<Longrightarrow> primerec (ys ! i) n"
-apply(case_tac i, auto, case_tac nat, simp, simp add: numeral_2_eq_2)
-done
-
-lemma [intro]: "primerec rec_quo (Suc (Suc 0))"
-apply(simp add: rec_quo_def)
-apply(tactic {* resolve_tac [@{thm prime_cn}, 
-    @{thm prime_id}] 1*}, auto+)+
-done
-
-lemma [intro]: "primerec rec_mod (Suc (Suc 0))"
-apply(simp add: rec_mod_def)
-apply(tactic {* resolve_tac [@{thm prime_cn}, 
-    @{thm prime_id}] 1*}, auto+)+
-done
-
-lemma [intro]: "primerec rec_power (Suc (Suc 0))"
-apply(simp add: rec_power_def  numeral_2_eq_2 numeral_3_eq_3)
-apply(tactic {* resolve_tac [@{thm prime_cn}, 
-    @{thm prime_id}, @{thm prime_pr}] 1*}, auto+)+
-done
-
-text {*
-  @{text "rec_lo"} is the recursive function used to implement @{text "Lo"}.
-*}
-definition rec_lo :: "recf"
-  where
-  "rec_lo = (let rR = Cn 3 rec_eq [Cn 3 rec_mod [id 3 0, 
-               Cn 3 rec_power [id 3 1, id 3 2]], 
-                     Cn 3 (constn 0) [id 3 1]] in
-             let rb =  Cn 2 (rec_maxr rR) [id 2 0, id 2 1, id 2 0] in 
-             let rcond = Cn 2 rec_conj [Cn 2 rec_less [Cn 2 (constn 1)
-                                             [id 2 0], id 2 0], 
-                                        Cn 2 rec_less [Cn 2 (constn 1)
-                                                [id 2 0], id 2 1]] in 
-             let rcond2 = Cn 2 rec_minus 
-                              [Cn 2 (constn 1) [id 2 0], rcond] 
-             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_exec rec_lo [x, y] = Maxr loR [x, y] x"
-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_exec (rec_maxr ?rR) ([x, y] @ [x]) =
-    Maxr (\<lambda> args. 0 < rec_exec ?rR args) [x, y] x"
-    by(rule_tac Maxr_lemma, auto simp: rec_exec.simps
-      mod_lemma power_lemma, auto simp: numeral_2_eq_2 numeral_3_eq_3)
-  have "Maxr loR [x, y] x =  Maxr (\<lambda> args. 0 < rec_exec ?rR args) [x, y] x"
-    apply(simp add: rec_exec.simps mod_lemma power_lemma)
-    apply(simp add: Maxr.simps loR.simps)
-    done
-  from h and this show "rec_exec (rec_maxr ?rR) [x, y, x] = 
-    Maxr loR [x, y] x"
-    apply(simp)
-    done
-qed
-
-lemma [simp]: "Max {ya. ya = 0 \<and> loR [0, y, ya]} = 0"
-apply(rule_tac Max_eqI, auto simp: loR.simps)
-done
-
-lemma [simp]: "Suc 0 < y \<Longrightarrow> Suc (Suc 0) < y * y"
-apply(induct y, simp)
-apply(case_tac y, simp, simp)
-done
-
-lemma less_mult: "\<lbrakk>x > 0; y > Suc 0\<rbrakk> \<Longrightarrow> x < y * x"
-apply(case_tac y, simp, simp)
-done
-
-lemma x_less_exp: "\<lbrakk>y > Suc 0\<rbrakk> \<Longrightarrow> x < y^x"
-apply(induct x, simp, simp)
-apply(case_tac x, simp, auto)
-apply(rule_tac y = "y* y^nat" in le_less_trans, simp)
-apply(rule_tac less_mult, auto)
-done
-
-lemma le_mult: "y \<noteq> (0::nat) \<Longrightarrow> x \<le> x * y"  
-  by(induct y, simp, simp)
-
-lemma uplimit_loR:  "\<lbrakk>Suc 0 < x; Suc 0 < y; loR [x, y, xa]\<rbrakk> \<Longrightarrow> 
-  xa \<le> x"
-apply(simp add: loR.simps)
-apply(rule_tac classical, auto)
-apply(subgoal_tac "xa < y^xa")
-apply(subgoal_tac "y^xa \<le> y^xa * q", simp)
-apply(rule_tac le_mult, case_tac q, simp, simp)
-apply(rule_tac x_less_exp, simp)
-done
-
-lemma [simp]: "\<lbrakk>xa \<le> x; loR [x, y, xa]; Suc 0 < x; Suc 0 < y\<rbrakk> \<Longrightarrow>
-  {u. loR [x, y, u]} = {ya. ya \<le> x \<and> loR [x, y, ya]}"
-apply(rule_tac Collect_cong, auto)
-apply(erule_tac uplimit_loR, simp, simp)
-done
-
-lemma Maxr_lo: "\<lbrakk>Suc 0 < x; Suc 0 < y\<rbrakk> \<Longrightarrow>
-  Maxr loR [x, y] x = lo x y" 
-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_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_exec rec_lo [x, y] = lo x y"
-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_exec rec_lo [x, y] = lo x y"
-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_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"
-  where
-  "lgR [x, y, u] = (y^u \<le> x)"
-
-text {*
-  @{text "lg"} specifies the @{text "lg"} function given on page 79 of 
-  Boolos's book. It is one of the two notions of integeral logarithmatic
-  operation on that page. The other is @{text "lo"}.
-  *}
-fun lg :: "nat \<Rightarrow> nat \<Rightarrow> nat"
-  where
-  "lg x y = (if x > 1 \<and> y > 1 \<and> {u. lgR [x, y, u]} \<noteq> {} then 
-                 Max {u. lgR [x, y, u]}
-              else 0)"
-
-declare lg.simps[simp del] lgR.simps[simp del]
-
-text {*
-  @{text "rec_lg"} is the recursive function used to implement @{text "lg"}.
-  *}
-definition rec_lg :: "recf"
-  where
-  "rec_lg = (let rec_lgR = Cn 3 rec_le
-  [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], 
-                            Cn 2 rec_less [Cn 2 (constn 1) 
-                                 [id 2 0], id 2 1]] in 
-  let conR2 = Cn 2 rec_not [conR1] in 
-        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_exec rec_lg [x, y] = Maxr lgR [x, y] x"
-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_exec (rec_maxr ?rR) ([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_exec ?rR args)) [x, y] x"
-    apply(simp add: rec_exec.simps power_lemma)
-    apply(simp add: Maxr.simps lgR.simps)
-    done 
-  ultimately show "rec_exec (rec_maxr ?rR) [x, y, x] = Maxr lgR [x, y] x"
-    by simp
-qed
-
-lemma [simp]: "\<lbrakk>Suc 0 < y; lgR [x, y, xa]\<rbrakk> \<Longrightarrow> xa \<le> x"
-apply(simp add: lgR.simps)
-apply(subgoal_tac "y^xa > xa", simp)
-apply(erule x_less_exp)
-done
-
-lemma [simp]: "\<lbrakk>Suc 0 < x; Suc 0 < y; lgR [x, y, xa]\<rbrakk> \<Longrightarrow>
-           {u. lgR [x, y, u]} =  {ya. ya \<le> x \<and> lgR [x, y, ya]}"
-apply(rule_tac Collect_cong, auto)
-done
-
-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_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_exec rec_lg [x, y] = lg x y"
-apply(simp add: rec_exec.simps rec_lg_def Let_def lg.simps)
-done
-
-lemma lg_lemma''': "\<not> Suc 0 < y \<Longrightarrow> rec_exec rec_lg [x, y] = lg x y"
-apply(simp add: rec_exec.simps rec_lg_def Let_def lg.simps)
-done
-
-text {*
-  The correctness of @{text "rec_lg"}.
-  *}
-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 {*
-  @{text "Entry sr i"} returns the @{text "i"}-th entry of a list of natural 
-  numbers encoded by number @{text "sr"} using Godel's coding.
-  *}
-fun Entry :: "nat \<Rightarrow> nat \<Rightarrow> nat"
-  where
-  "Entry sr i = lo sr (Pi (Suc i))"
-
-text {*
-  @{text "rec_entry"} is the recursive function used to implement
-  @{text "Entry"}.
-  *}
-definition rec_entry:: "recf"
-  where
-  "rec_entry = Cn 2 rec_lo [id 2 0, Cn 2 rec_pi [Cn 2 s [id 2 1]]]"
-
-declare Pi.simps[simp del]
-
-text {*
-  The correctness of @{text "rec_entry"}.
-  *}
-lemma entry_lemma: "rec_exec rec_entry [str, i] = Entry str i"
-  by(simp add: rec_entry_def  rec_exec.simps lo_lemma pi_lemma)
-
-
-subsection {* The construction of F *}
-
-text {*
-  Using the auxilliary functions obtained in last section, 
-  we are going to contruct the function @{text "F"}, 
-  which is an interpreter of Turing Machines.
-  *}
-
-fun listsum2 :: "nat list \<Rightarrow> nat \<Rightarrow> nat"
-  where
-  "listsum2 xs 0 = 0"
-| "listsum2 xs (Suc n) = listsum2 xs n + xs ! n"
-
-fun rec_listsum2 :: "nat \<Rightarrow> nat \<Rightarrow> recf"
-  where
-  "rec_listsum2 vl 0 = Cn vl z [id vl 0]"
-| "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_exec (rec_listsum2 vl n) xs = listsum2 xs n"
-apply(induct n, simp_all)
-apply(simp_all add: rec_exec.simps rec_listsum2.simps listsum2.simps)
-done
-
-fun strt' :: "nat list \<Rightarrow> nat \<Rightarrow> nat"
-  where
-  "strt' xs 0 = 0"
-| "strt' xs (Suc n) = (let dbound = listsum2 xs n + n in 
-                       strt' xs n + (2^(xs ! n + dbound) - 2^dbound))"
-
-fun rec_strt' :: "nat \<Rightarrow> nat \<Rightarrow> recf"
-  where
-  "rec_strt' vl 0 = Cn vl z [id vl 0]"
-| "rec_strt' vl (Suc n) = (let rec_dbound =
-  Cn vl rec_add [rec_listsum2 vl n, Cn vl (constn n) [id vl 0]]
-  in Cn vl rec_add [rec_strt' vl n, Cn vl rec_minus 
-  [Cn vl rec_power [Cn vl (constn 2) [id vl 0], Cn vl rec_add
-  [id vl (n), rec_dbound]], 
-  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_exec (rec_strt' vl n) xs = strt' xs n"
-apply(induct n)
-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 
-  this definition generalises the original one to deal with multiple input arguments.
-  *}
-fun strt :: "nat list \<Rightarrow> nat"
-  where
-  "strt xs = (let ys = map Suc xs in 
-              strt' ys (length ys))"
-
-fun rec_map :: "recf \<Rightarrow> nat \<Rightarrow> recf list"
-  where
-  "rec_map rf vl = map (\<lambda> i. Cn vl rf [id vl (i)]) [0..<vl]"
-
-text {*
-  @{text "rec_strt"} is the recursive function used to implement @{text "strt"}.
-  *}
-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_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_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_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_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_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_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_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_exec.simps nth_append)
-      done
-    ultimately show "?thesis"
-      by simp
-  qed
-next
-  fix vl xs
-  assume "length xs = Suc vl"
-  thus "\<exists>ys y. xs = ys @ [y]"
-    apply(rule_tac x = "butlast xs" in exI, rule_tac x = "last xs" in exI)
-    apply(subgoal_tac "xs \<noteq> []", auto)
-    done
-qed
-
-text {*
-  The correctness of @{text "rec_strt"}.
-  *}
-lemma strt_lemma: "length xs = vl \<Longrightarrow> 
-  rec_exec (rec_strt vl) xs = strt xs"
-apply(simp add: strt.simps rec_exec.simps strt'_lemma)
-apply(subgoal_tac "(map ((\<lambda>a. rec_exec a xs) \<circ> (\<lambda>i. Cn vl s [recf.id vl (i)])) [0..<vl])
-                  = map Suc xs", auto)
-apply(rule map_s_lemma, simp)
-done
-
-text {*
-  The @{text "scan"} function on page 90 of B book.
-  *}
-fun scan :: "nat \<Rightarrow> nat"
-  where
-  "scan r = r mod 2"
-
-text {*
-  @{text "rec_scan"} is the implemention of @{text "scan"}.
-  *}
-definition rec_scan :: "recf"
-  where "rec_scan = Cn 1 rec_mod [id 1 0, constn 2]"
-
-text {*
-  The correctness of @{text "scan"}.
-  *}
-lemma scan_lemma: "rec_exec rec_scan [r] = r mod 2"
-  by(simp add: rec_exec.simps rec_scan_def mod_lemma)
-
-fun newleft0 :: "nat list \<Rightarrow> nat"
-  where
-  "newleft0 [p, r] = p"
-
-definition rec_newleft0 :: "recf"
-  where
-  "rec_newleft0 = id 2 0"
-
-fun newrgt0 :: "nat list \<Rightarrow> nat"
-  where
-  "newrgt0 [p, r] = r - scan r"
-
-definition rec_newrgt0 :: "recf"
-  where
-  "rec_newrgt0 = Cn 2 rec_minus [id 2 1, Cn 2 rec_scan [id 2 1]]"
-
-(*newleft1, newrgt1: left rgt number after execute on step*)
-fun newleft1 :: "nat list \<Rightarrow> nat"
-  where
-  "newleft1 [p, r] = p"
-
-definition rec_newleft1 :: "recf"
-  where
-  "rec_newleft1 = id 2 0"
-
-fun newrgt1 :: "nat list \<Rightarrow> nat"
-  where
-  "newrgt1 [p, r] = r + 1 - scan r"
-
-definition rec_newrgt1 :: "recf"
-  where
-  "rec_newrgt1 = 
-  Cn 2 rec_minus [Cn 2 rec_add [id 2 1, Cn 2 (constn 1) [id 2 0]], 
-                  Cn 2 rec_scan [id 2 1]]"
-
-fun newleft2 :: "nat list \<Rightarrow> nat"
-  where
-  "newleft2 [p, r] = p div 2"
-
-definition rec_newleft2 :: "recf" 
-  where
-  "rec_newleft2 = Cn 2 rec_quo [id 2 0, Cn 2 (constn 2) [id 2 0]]"
-
-fun newrgt2 :: "nat list \<Rightarrow> nat"
-  where
-  "newrgt2 [p, r] = 2 * r + p mod 2"
-
-definition rec_newrgt2 :: "recf"
-  where
-  "rec_newrgt2 =
-    Cn 2 rec_add [Cn 2 rec_mult [Cn 2 (constn 2) [id 2 0], id 2 1],                     
-                 Cn 2 rec_mod [id 2 0, Cn 2 (constn 2) [id 2 0]]]"
-
-fun newleft3 :: "nat list \<Rightarrow> nat"
-  where
-  "newleft3 [p, r] = 2 * p + r mod 2"
-
-definition rec_newleft3 :: "recf"
-  where
-  "rec_newleft3 = 
-  Cn 2 rec_add [Cn 2 rec_mult [Cn 2 (constn 2) [id 2 0], id 2 0], 
-                Cn 2 rec_mod [id 2 1, Cn 2 (constn 2) [id 2 0]]]"
-
-fun newrgt3 :: "nat list \<Rightarrow> nat"
-  where
-  "newrgt3 [p, r] = r div 2"
-
-definition rec_newrgt3 :: "recf"
-  where
-  "rec_newrgt3 = Cn 2 rec_quo [id 2 1, Cn 2 (constn 2) [id 2 0]]"
-
-text {*
-  The @{text "new_left"} function on page 91 of B book.
-  *}
-fun newleft :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat"
-  where
-  "newleft p r a = (if a = 0 \<or> a = 1 then newleft0 [p, r] 
-                    else if a = 2 then newleft2 [p, r]
-                    else if a = 3 then newleft3 [p, r]
-                    else p)"
-
-text {*
-  @{text "rec_newleft"} is the recursive function used to 
-  implement @{text "newleft"}.
-  *}
-definition rec_newleft :: "recf" 
-  where
-  "rec_newleft =
-  (let g0 = 
-      Cn 3 rec_newleft0 [id 3 0, id 3 1] in 
-  let g1 = Cn 3 rec_newleft2 [id 3 0, id 3 1] in 
-  let g2 = Cn 3 rec_newleft3 [id 3 0, id 3 1] in 
-  let g3 = id 3 0 in
-  let r0 = Cn 3 rec_disj
-          [Cn 3 rec_eq [id 3 2, Cn 3 (constn 0) [id 3 0]],
-           Cn 3 rec_eq [id 3 2, Cn 3 (constn 1) [id 3 0]]] in 
-  let r1 = Cn 3 rec_eq [id 3 2, Cn 3 (constn 2) [id 3 0]] in 
-  let r2 = Cn 3 rec_eq [id 3 2, Cn 3 (constn 3) [id 3 0]] in
-  let r3 = Cn 3 rec_less [Cn 3 (constn 3) [id 3 0], id 3 2] in 
-  let gs = [g0, g1, g2, g3] in 
-  let rs = [r0, r1, r2, r3] in 
-  rec_embranch (zip gs rs))"
-
-declare newleft.simps[simp del]
-
-
-lemma Suc_Suc_Suc_Suc_induct: 
-  "\<lbrakk>i < Suc (Suc (Suc (Suc 0))); i = 0 \<Longrightarrow>  P i;
-    i = 1 \<Longrightarrow> P i; i =2 \<Longrightarrow> P i; 
-    i =3 \<Longrightarrow> P i\<rbrakk> \<Longrightarrow> P i"
-apply(case_tac i, simp, case_tac nat, simp, 
-      case_tac nata, simp, case_tac natb, simp, simp)
-done
-
-declare quo_lemma2[simp] mod_lemma[simp]
-
-text {*
-  The correctness of @{text "rec_newleft"}.
-  *}
-lemma newleft_lemma: 
-  "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]]"
-  thm embranch_lemma
-  have k1: "rec_exec (rec_embranch (zip ?rgs ?rrs)) [p, r, a]
-                         = Embranch (zip (map rec_exec ?rgs) (map (\<lambda>r args. 0 < rec_exec r args) ?rrs)) [p, r, a]"
-    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_exec.simps)
-    apply(erule_tac [!] Suc_Suc_Suc_Suc_induct, auto simp: rec_exec.simps)
-    done
-  have k2: "Embranch (zip (map rec_exec ?rgs) (map (\<lambda>r args. 0 < rec_exec r args) ?rrs)) [p, r, a] = newleft p r a"
-    apply(simp add: Embranch.simps)
-    apply(simp add: rec_exec.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_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 
-  compute the right number.
-  *}
-fun newrght :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat"
-  where
-  "newrght p r a  = (if a = 0 then newrgt0 [p, r]
-                    else if a = 1 then newrgt1 [p, r]
-                    else if a = 2 then newrgt2 [p, r]
-                    else if a = 3 then newrgt3 [p, r]
-                    else r)"
-
-text {*
-  @{text "rec_newrght"} is the recursive function used to implement 
-  @{text "newrgth"}.
-  *}
-definition rec_newrght :: "recf" 
-  where
-  "rec_newrght =
-  (let g0 = Cn 3 rec_newrgt0 [id 3 0, id 3 1] in 
-  let g1 = Cn 3 rec_newrgt1 [id 3 0, id 3 1] in 
-  let g2 = Cn 3 rec_newrgt2 [id 3 0, id 3 1] in 
-  let g3 = Cn 3 rec_newrgt3 [id 3 0, id 3 1] in
-  let g4 = id 3 1 in 
-  let r0 = Cn 3 rec_eq [id 3 2, Cn 3 (constn 0) [id 3 0]] in 
-  let r1 = Cn 3 rec_eq [id 3 2, Cn 3 (constn 1) [id 3 0]] in 
-  let r2 = Cn 3 rec_eq [id 3 2, Cn 3 (constn 2) [id 3 0]] in
-  let r3 = Cn 3 rec_eq [id 3 2, Cn 3 (constn 3) [id 3 0]] in
-  let r4 = Cn 3 rec_less [Cn 3 (constn 3) [id 3 0], id 3 2] in 
-  let gs = [g0, g1, g2, g3, g4] in 
-  let rs = [r0, r1, r2, r3, r4] in 
-  rec_embranch (zip gs rs))"
-declare newrght.simps[simp del]
-
-lemma numeral_4_eq_4: "4 = Suc 3"
-by auto
-
-lemma Suc_5_induct: 
-  "\<lbrakk>i < Suc (Suc (Suc (Suc (Suc 0)))); i = 0 \<Longrightarrow> P 0;
-  i = 1 \<Longrightarrow> P 1; i = 2 \<Longrightarrow> P 2; i = 3 \<Longrightarrow> P 3; i = 4 \<Longrightarrow> P 4\<rbrakk> \<Longrightarrow> P i"
-apply(case_tac i, auto)
-apply(case_tac nat, auto)
-apply(case_tac nata, auto simp: numeral_2_eq_2)
-apply(case_tac nat, auto simp: numeral_3_eq_3 numeral_4_eq_4)
-done
-
-lemma [intro]: "primerec rec_scan (Suc 0)"
-apply(auto simp: rec_scan_def, auto)
-done
-
-text {*
-  The correctness of @{text "rec_newrght"}.
-  *}
-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"
-  let ?r3 = "\<lambda> zs. zs ! 2 = 3"
-  let ?r4 = "\<lambda> zs. zs ! 2 > 3"
-  let ?gs = "map (\<lambda> g. (\<lambda> zs. g [zs ! 0, zs ! 1])) ?gs'"
-  let ?rs = "[?r0, ?r1, ?r2, ?r3, ?r4]"
-  let ?rgs = 
- "[Cn 3 rec_newrgt0 [recf.id 3 0, recf.id 3 1],
-    Cn 3 rec_newrgt1 [recf.id 3 0, recf.id 3 1],
-     Cn 3 rec_newrgt2 [recf.id 3 0, recf.id 3 1], 
-      Cn 3 rec_newrgt3 [recf.id 3 0, recf.id 3 1], recf.id 3 1]"
-  let ?rrs = 
- "[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_exec (rec_embranch (zip ?rgs ?rrs)) [p, r, a]
-    = Embranch (zip (map rec_exec ?rgs) (map (\<lambda>r args. 0 < rec_exec r args) ?rrs)) [p, r, a]"
-    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
-    apply(case_tac "a = 1", rule_tac x = "Suc 0" in exI)
-    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_exec.simps)
-    apply(erule_tac [!] Suc_5_induct, auto simp: rec_exec.simps)
-    done
-  have k2: "Embranch (zip (map rec_exec ?rgs)
-    (map (\<lambda>r args. 0 < rec_exec r args) ?rrs)) [p, r, a] = newrght p r a"
-    apply(auto simp:Embranch.simps rec_exec.simps)
-    apply(auto simp: newrght.simps rec_newrgt3_def rec_newrgt2_def
-                     rec_newrgt1_def rec_newrgt0_def rec_exec.simps
-                     scan_lemma)
-    done
-  from k1 and k2 show 
-    "rec_exec (rec_embranch (zip ?rgs ?rrs)) [p, r, a] =      
-                                    newrght p r a" by simp
-qed
-
-declare Entry.simps[simp del]
-
-text {*
-  The @{text "actn"} function given on page 92 of B book, which is used to 
-  fetch Turing Machine intructions. 
-  In @{text "actn m q r"}, @{text "m"} is the Godel coding of a Turing Machine,
-  @{text "q"} is the current state of Turing Machine, @{text "r"} is the
-  right number of Turing Machine tape.
-  *}
-fun actn :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat"
-  where
-  "actn m q r = (if q \<noteq> 0 then Entry m (4*(q - 1) + 2 * scan r)
-                 else 4)"
-
-text {*
-  @{text "rec_actn"} is the recursive function used to implement @{text "actn"}
-  *}
-definition rec_actn :: "recf"
-  where
-  "rec_actn = 
-  Cn 3 rec_add [Cn 3 rec_mult 
-        [Cn 3 rec_entry [id 3 0, Cn 3 rec_add [Cn 3 rec_mult 
-                                 [Cn 3 (constn 4) [id 3 0], 
-                Cn 3 rec_minus [id 3 1, Cn 3 (constn 1) [id 3 0]]], 
-                   Cn 3 rec_mult [Cn 3 (constn 2) [id 3 0],
-                      Cn 3 rec_scan [id 3 2]]]], 
-            Cn 3 rec_noteq [id 3 1, Cn 3 (constn 0) [id 3 0]]], 
-                             Cn 3 rec_mult [Cn 3 (constn 4) [id 3 0], 
-             Cn 3 rec_eq [id 3 1, Cn 3 (constn 0) [id 3 0]]]] "
-
-text {*
-  The correctness of @{text "actn"}.
-  *}
-lemma actn_lemma: "rec_exec rec_actn [m, q, r] = actn m q r"
-  by(auto simp: rec_actn_def rec_exec.simps entry_lemma scan_lemma)
-
-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)"
-
-definition rec_newstat :: "recf"
-  where
-  "rec_newstat = Cn 3 rec_add 
-    [Cn 3 rec_mult [Cn 3 rec_entry [id 3 0, 
-           Cn 3 rec_add [Cn 3 rec_mult [Cn 3 (constn 4) [id 3 0], 
-           Cn 3 rec_minus [id 3 1, Cn 3 (constn 1) [id 3 0]]], 
-           Cn 3 rec_add [Cn 3 rec_mult [Cn 3 (constn 2) [id 3 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_exec rec_newstat [m, q, r] = newstat m q r"
-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*}
-
-fun trpl :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat"
-  where
-  "trpl p q r = (Pi 0)^p * (Pi 1)^q * (Pi 2)^r"
-
-definition rec_trpl :: "recf"
-  where
-  "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_exec rec_trpl [p, q, r] = trpl p q r"
-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)"
-
-fun stat :: "nat \<Rightarrow> nat"
-  where
-  "stat c = lo c (Pi 1)"
-
-fun rght :: "nat \<Rightarrow> nat"
-  where
-  "rght c = lo c (Pi 2)"
-
-thm Prime.simps
-
-fun inpt :: "nat \<Rightarrow> nat list \<Rightarrow> nat"
-  where
-  "inpt m xs = trpl 0 1 (strt xs)"
-
-fun newconf :: "nat \<Rightarrow> nat \<Rightarrow> nat"
-  where
-  "newconf m c = trpl (newleft (left c) (rght c) 
-                        (actn m (stat c) (rght c)))
-                        (newstat m (stat c) (rght c)) 
-                        (newrght (left c) (rght c) 
-                              (actn m (stat c) (rght c)))"
-  
-declare left.simps[simp del] stat.simps[simp del] rght.simps[simp del]
-        inpt.simps[simp del] newconf.simps[simp del]
-
-definition rec_left :: "recf"
-  where
-  "rec_left = Cn 1 rec_lo [id 1 0, constn (Pi 0)]"
-
-definition rec_right :: "recf"
-  where
-  "rec_right = Cn 1 rec_lo [id 1 0, constn (Pi 2)]"
-
-definition rec_stat :: "recf"
-  where
-  "rec_stat = Cn 1 rec_lo [id 1 0, constn (Pi 1)]"
-
-definition rec_inpt :: "nat \<Rightarrow> recf"
-  where
-  "rec_inpt vl = Cn vl rec_trpl 
-                  [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_exec rec_left [c] = left c"
-by(simp add: rec_exec.simps rec_left_def left.simps lo_lemma)
-      
-lemma right_lemma: "rec_exec rec_right [c] = rght c"
-by(simp add: rec_exec.simps rec_right_def rght.simps lo_lemma)
-
-lemma stat_lemma: "rec_exec rec_stat [c] = stat c"
-by(simp add: rec_exec.simps rec_stat_def stat.simps lo_lemma)
- 
-declare rec_strt.simps[simp del] strt.simps[simp del]
-
-lemma map_cons_eq: 
-  "(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_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"
-apply(induct vl arbitrary: xs, simp)
-apply(subgoal_tac "\<exists> ys y. xs = ys @ [y]", auto)
-proof -
-  fix ys y
-  assume ind: 
-    "\<And>xs. length (ys::nat list) = length (xs::nat list) \<Longrightarrow>
-            map (\<lambda>i. xs ! (i - Suc 0)) [Suc 0..<length xs] @
-                                [xs ! (length xs - Suc 0)] = xs"
-  and h: "Suc 0 \<le> length (ys::nat list)"
-  have "map (\<lambda>i. ys ! (i - Suc 0)) [Suc 0..<length ys] @ 
-                                   [ys ! (length ys - Suc 0)] = ys"
-    apply(rule_tac ind, simp)
-    done
-  moreover have 
-    "map (\<lambda>i. (ys @ [y]) ! (i - Suc 0)) [Suc 0..<length ys]
-      = map (\<lambda>i. ys ! (i - Suc 0)) [Suc 0..<length ys]"
-    apply(rule map_ext)
-    using h
-    apply(auto simp: nth_append)
-    done
-  ultimately show "map (\<lambda>i. (ys @ [y]) ! (i - Suc 0)) 
-        [Suc 0..<length ys] @ [(ys @ [y]) ! (length ys - Suc 0)] = ys"
-    apply(simp del: map_eq_conv add: nth_append, auto)
-    using h
-    apply(simp)
-    done
-next
-  fix vl xs
-  assume "Suc vl = length (xs::nat list)"
-  thus "\<exists>ys y. xs = ys @ [y]"
-    apply(rule_tac x = "butlast xs" in exI, 
-          rule_tac x = "last xs" in exI)
-    apply(case_tac "xs \<noteq> []", auto)
-    done
-qed
-
-lemma [elim]: 
-  "Suc 0 \<le> length xs \<Longrightarrow> 
-     (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_exec.simps)
-using list_map_eq[of "length xs" xs]
-apply(simp)
-done
-
-    
-lemma inpt_lemma:
-  "\<lbrakk>Suc (length xs) = vl\<rbrakk> \<Longrightarrow> 
-            rec_exec (rec_inpt vl) (m # xs) = inpt m xs"
-apply(auto simp: rec_exec.simps rec_inpt_def 
-                 trpl_lemma inpt.simps strt_lemma)
-apply(subgoal_tac
-  "(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
-
-definition rec_newconf:: "recf"
-  where
-  "rec_newconf = 
-    Cn 2 rec_trpl 
-        [Cn 2 rec_newleft [Cn 2 rec_left [id 2 1], 
-                           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]]],
-          Cn 2 rec_newstat [id 2 0, 
-                            Cn 2 rec_stat [id 2 1], 
-                            Cn 2 rec_right [id 2 1]],
-           Cn 2 rec_newrght [Cn 2 rec_left [id 2 1], 
-                             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_exec rec_newconf [m ,c] = newconf m c"
-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]
-
-text {*
-  @{text "conf m r k"} computes the TM configuration after @{text "k"} steps of execution
-  of TM coded as @{text "m"} starting from the initial configuration where the left number equals @{text "0"}, 
-  right number equals @{text "r"}. 
-  *}
-fun conf :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat"
-  where
-  "conf m r 0 = trpl 0 (Suc 0) r"
-| "conf m r (Suc t) = newconf m (conf m r t)"
-
-declare conf.simps[simp del]
-
-text {*
-  @{text "conf"} is implemented by the following recursive function @{text "rec_conf"}.
-  *}
-definition rec_conf :: "recf"
-  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_exec rec_conf [m, r, Suc t] =
-         rec_exec rec_newconf [m, rec_exec rec_conf [m, r, t]]"
-proof -
-  have "rec_exec rec_conf ([m, r] @ [Suc t]) = 
-          rec_exec rec_newconf [m, rec_exec rec_conf [m, r, t]]"
-    by(simp only: rec_conf_def rec_pr_Suc_simp_rewrite,
-        simp add: rec_exec.simps)
-  thus "rec_exec rec_conf [m, r, Suc t] =
-                rec_exec rec_newconf [m, rec_exec rec_conf [m, r, t]]"
-    by simp
-qed
-
-text {*
-  The correctness of @{text "rec_conf"}.
-  *}
-lemma conf_lemma: 
-  "rec_exec rec_conf [m, r, t] = conf m r t"
-apply(induct t)
-apply(simp add: rec_conf_def rec_exec.simps conf.simps inpt_lemma trpl_lemma)
-apply(simp add: conf_step conf.simps)
-done
-
-text {*
-  @{text "NSTD c"} returns true if the configureation coded by @{text "c"} is no a stardard
-  final configuration.
-  *}
-fun NSTD :: "nat \<Rightarrow> bool"
-  where
-  "NSTD c = (stat c \<noteq> 0 \<or> left c \<noteq> 0 \<or> 
-             rght c \<noteq> 2^(lg (rght c + 1) 2) - 1 \<or> rght c = 0)"
-
-text {*
-  @{text "rec_NSTD"} is the recursive function implementing @{text "NSTD"}.
-  *}
-definition rec_NSTD :: "recf"
-  where
-  "rec_NSTD =
-     Cn 1 rec_disj [
-          Cn 1 rec_disj [
-             Cn 1 rec_disj 
-                [Cn 1 rec_noteq [rec_stat, constn 0], 
-                 Cn 1 rec_noteq [rec_left, constn 0]] , 
-              Cn 1 rec_noteq [rec_right,  
-                              Cn 1 rec_minus [Cn 1 rec_power 
-                                 [constn 2, Cn 1 rec_lg 
-                                    [Cn 1 rec_add        
-                                     [rec_right, constn 1], 
-                                            constn 2]], constn 1]]],
-               Cn 1 rec_eq [rec_right, constn 0]]"
-
-lemma NSTD_lemma1: "rec_exec rec_NSTD [c] = Suc 0 \<or>
-                   rec_exec rec_NSTD [c] = 0"
-by(simp add: rec_exec.simps rec_NSTD_def)
-
-declare NSTD.simps[simp del]
-lemma NSTD_lemma2': "(rec_exec rec_NSTD [c] = Suc 0) \<Longrightarrow> NSTD c"
-apply(simp add: rec_exec.simps rec_NSTD_def stat_lemma left_lemma 
-                lg_lemma right_lemma power_lemma NSTD.simps eq_lemma)
-apply(auto)
-apply(case_tac "0 < left c", simp, simp)
-done
-
-lemma NSTD_lemma2'': 
-  "NSTD c \<Longrightarrow> (rec_exec rec_NSTD [c] = Suc 0)"
-apply(simp add: rec_exec.simps rec_NSTD_def stat_lemma 
-         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_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_exec rec_NSTD [c] = nstd c"
-using NSTD_lemma1
-apply(simp add: NSTD_lemma2, auto)
-done
-
-text{* 
-  @{text "nonstep m r t"} means afer @{text "t"} steps of execution, the TM coded by @{text "m"}
-  is not at a stardard final configuration.
-  *}
-fun nonstop :: "nat \<Rightarrow> nat  \<Rightarrow> nat \<Rightarrow> nat"
-  where
-  "nonstop m r t = nstd (conf m r t)"
-
-text {*
-  @{text "rec_nonstop"} is the recursive function implementing @{text "nonstop"}.
-  *}
-definition rec_nonstop :: "recf"
-  where
-  "rec_nonstop = Cn 3 rec_NSTD [rec_conf]"
-
-text {*
-  The correctness of @{text "rec_nonstop"}.
-  *}
-lemma nonstop_lemma: 
-  "rec_exec rec_nonstop [m, r, t] = nonstop m r t"
-apply(simp add: rec_exec.simps rec_nonstop_def nstd_lemma conf_lemma)
-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
-  using @{text "Mn"} combinator. So it is the only non-primitive recursive function 
-  needs to be used in the construction of the universal function @{text "F"}.
-  *}
-
-definition rec_halt :: "recf"
-  where
-  "rec_halt = Mn (Suc (Suc 0)) (rec_nonstop)"
-
-declare nonstop.simps[simp del]
-
-lemma primerec_not0: "primerec f n \<Longrightarrow> n > 0"
-by(induct f n rule: primerec.induct, auto)
-
-lemma [elim]: "primerec f 0 \<Longrightarrow> RR"
-apply(drule_tac primerec_not0, simp)
-done
-
-lemma [simp]: "length xs = Suc n \<Longrightarrow> length (butlast xs) = n"
-apply(subgoal_tac "\<exists> y ys. xs = ys @ [y]", auto)
-apply(rule_tac x = "last xs" in exI)
-apply(rule_tac x = "butlast xs" in exI)
-apply(case_tac "xs = []", auto)
-done
-
-text {*
-  The lemma relates the interpreter of primitive fucntions with
-  the calculation relation of general recursive functions. 
-  *}
-lemma prime_rel_exec_eq: "primerec r (length xs) 
-           \<Longrightarrow> rec_calc_rel r xs rs = (rec_exec r xs = rs)"
-proof(induct r xs arbitrary: rs rule: rec_exec.induct, simp_all)
-  fix xs rs
-  assume "primerec z (length (xs::nat list))"
-  hence "length xs = Suc 0" by(erule_tac prime_z_reverse, simp)
-  thus "rec_calc_rel z xs rs = (rec_exec z xs = rs)"
-    apply(case_tac xs, simp, auto)
-    apply(erule_tac calc_z_reverse, simp add: rec_exec.simps)
-    apply(simp add: rec_exec.simps, rule_tac calc_z)
-    done
-next
-  fix xs rs
-  assume "primerec s (length (xs::nat list))"
-  hence "length xs = Suc 0" ..
-  thus "rec_calc_rel s xs rs = (rec_exec s xs = rs)"
-    by(case_tac xs, auto simp: rec_exec.simps intro: calc_s 
-                         elim: calc_s_reverse)
-next
-  fix m n xs rs
-  assume "primerec (recf.id m n) (length (xs::nat list))"
-  thus
-    "rec_calc_rel (recf.id m n) xs rs =
-                   (rec_exec (recf.id m n) xs = rs)"
-    apply(erule_tac prime_id_reverse)
-    apply(simp add: rec_exec.simps, auto)
-    apply(erule_tac calc_id_reverse, simp)
-    apply(rule_tac calc_id, auto)
-    done
-next
-  fix n f gs xs rs
-  assume ind1:
-    "\<And>x rs. \<lbrakk>x \<in> set gs; primerec x (length xs)\<rbrakk> \<Longrightarrow>
-                rec_calc_rel x xs rs = (rec_exec x xs = rs)"
-    and ind2: 
-    "\<And>x rs. \<lbrakk>x = map (\<lambda>a. rec_exec a xs) gs; 
-             primerec f (length gs)\<rbrakk> \<Longrightarrow> 
-            rec_calc_rel f (map (\<lambda>a. rec_exec a xs) gs) rs = 
-           (rec_exec f (map (\<lambda>a. rec_exec a xs) gs) = rs)"
-    and h: "primerec (Cn n f gs) (length xs)"
-  show "rec_calc_rel (Cn n f gs) xs rs = 
-                   (rec_exec (Cn n f gs) xs = rs)"
-  proof(auto simp: rec_exec.simps, erule_tac calc_cn_reverse, auto)
-    fix ys
-    assume g1:"\<forall>k<length gs. rec_calc_rel (gs ! k) xs (ys ! k)"
-      and g2: "length ys = length gs"
-      and g3: "rec_calc_rel f ys rs"
-    have "rec_calc_rel f (map (\<lambda>a. rec_exec a xs) gs) rs =
-                  (rec_exec f (map (\<lambda>a. rec_exec a xs) gs) = rs)"
-      apply(rule_tac ind2, auto)
-      using h
-      apply(erule_tac prime_cn_reverse, simp)
-      done
-    moreover have "ys = (map (\<lambda>a. rec_exec a xs) gs)"
-    proof(rule_tac nth_equalityI, auto simp: g2)
-      fix i
-      assume "i < length gs" thus "ys ! i = rec_exec (gs!i) xs"
-        using ind1[of "gs ! i" "ys ! i"] g1 h
-        apply(erule_tac prime_cn_reverse, simp)
-        done
-    qed     
-    ultimately show "rec_exec f (map (\<lambda>a. rec_exec a xs) gs) = rs"
-      using g3
-      by(simp)
-  next
-    from h show 
-      "rec_calc_rel (Cn n f gs) xs 
-                 (rec_exec f (map (\<lambda>a. rec_exec a xs) gs))"
-      apply(rule_tac rs = "(map (\<lambda>a. rec_exec a xs) gs)" in calc_cn, 
-            auto)
-      apply(erule_tac [!] prime_cn_reverse, auto)
-    proof -
-      fix k
-      assume "k < length gs" "primerec f (length gs)" 
-             "\<forall>i<length gs. primerec (gs ! i) (length xs)"
-      thus "rec_calc_rel (gs ! k) xs (rec_exec (gs ! k) xs)"
-        using ind1[of "gs!k" "(rec_exec (gs ! k) xs)"]
-        by(simp)
-    next
-      assume "primerec f (length gs)" 
-             "\<forall>i<length gs. primerec (gs ! i) (length xs)"
-      thus "rec_calc_rel f (map (\<lambda>a. rec_exec a xs) gs) 
-        (rec_exec f (map (\<lambda>a. rec_exec a xs) gs))"
-        using ind2[of "(map (\<lambda>a. rec_exec a xs) gs)" 
-                   "(rec_exec f (map (\<lambda>a. rec_exec a xs) gs))"]
-        by simp
-    qed
-  qed
-next
-  fix n f g xs rs
-  assume ind1: 
-    "\<And>rs. \<lbrakk>last xs = 0; primerec f (length xs - Suc 0)\<rbrakk> 
-    \<Longrightarrow> rec_calc_rel f (butlast xs) rs = 
-                     (rec_exec f (butlast xs) = rs)"
-  and ind2 : 
-    "\<And>rs. \<lbrakk>0 < last xs; 
-           primerec (Pr n f g) (Suc (length xs - Suc 0))\<rbrakk> \<Longrightarrow>
-           rec_calc_rel (Pr n f g) (butlast xs @ [last xs - Suc 0]) rs
-        = (rec_exec (Pr n f g) (butlast xs @ [last xs - Suc 0]) = rs)"
-  and ind3: 
-    "\<And>rs. \<lbrakk>0 < last xs; primerec g (Suc (Suc (length xs - Suc 0)))\<rbrakk>
-       \<Longrightarrow> rec_calc_rel g (butlast xs @
-                [last xs - Suc 0, rec_exec (Pr n f g)
-                 (butlast xs @ [last xs - Suc 0])]) rs = 
-              (rec_exec g (butlast xs @ [last xs - Suc 0,
-                 rec_exec (Pr n f g)  
-                  (butlast xs @ [last xs - Suc 0])]) = rs)"
-  and h: "primerec (Pr n f g) (length (xs::nat list))"
-  show "rec_calc_rel (Pr n f g) xs rs = (rec_exec (Pr n f g) xs = rs)"
-  proof(auto)
-    assume "rec_calc_rel (Pr n f g) xs rs"
-    thus "rec_exec (Pr n f g) xs = rs"
-    proof(erule_tac calc_pr_reverse)
-      fix l
-      assume g: "xs = l @ [0]"
-                "rec_calc_rel f l rs" 
-                "n = length l"
-      thus "rec_exec (Pr n f g) xs = rs"
-        using ind1[of rs] h
-        apply(simp add: rec_exec.simps, 
-                  erule_tac prime_pr_reverse, simp)
-        done
-    next
-      fix l y ry
-      assume d:"xs = l @ [Suc y]" 
-               "rec_calc_rel (Pr (length l) f g) (l @ [y]) ry"
-               "n = length l" 
-               "rec_calc_rel g (l @ [y, ry]) rs"
-      moreover hence "primerec g (Suc (Suc n))" using h
-      proof(erule_tac prime_pr_reverse)
-        assume "primerec g (Suc (Suc n))" "length xs = Suc n"
-        thus "?thesis" by simp      
-      qed  
-      ultimately show "rec_exec (Pr n f g) xs = rs"
-        apply(simp)
-        using ind3[of rs]
-        apply(simp add: rec_pr_Suc_simp_rewrite)
-        using ind2[of ry] h
-        apply(simp)
-        done
-    qed
-  next
-    show "rec_calc_rel (Pr n f g) xs (rec_exec (Pr n f g) xs)"
-    proof -
-      have "rec_calc_rel (Pr n f g) (butlast xs @ [last xs])
-                 (rec_exec (Pr n f g) (butlast xs @ [last xs]))"
-        using h
-        apply(erule_tac prime_pr_reverse, simp)
-        apply(case_tac "last xs", simp)
-        apply(rule_tac calc_pr_zero, simp)
-        using ind1[of "rec_exec (Pr n f g) (butlast xs @ [0])"]
-        apply(simp add: rec_exec.simps, simp, simp, simp)
-        thm calc_pr_ind
-        apply(rule_tac rk = "rec_exec (Pr n f g)
-               (butlast xs@[last xs - Suc 0])" in calc_pr_ind)
-        using ind2[of "rec_exec (Pr n f g)
-                 (butlast xs @ [last xs - Suc 0])"] h
-        apply(simp, simp, simp)
-      proof -
-        fix nat
-        assume "length xs = Suc n" 
-               "primerec g (Suc (Suc n))" 
-               "last xs = Suc nat"
-        thus 
-          "rec_calc_rel g (butlast xs @ [nat, rec_exec (Pr n f g) 
-            (butlast xs @ [nat])]) (rec_exec (Pr n f g) (butlast xs @ [Suc nat]))"
-          using ind3[of "rec_exec (Pr n f g)
-                                  (butlast xs @ [Suc nat])"]
-          apply(simp add: rec_exec.simps)
-          done
-      qed
-      thus "rec_calc_rel (Pr n f g) xs (rec_exec (Pr n f g) xs)"
-        using h
-        apply(erule_tac prime_pr_reverse, simp)
-        apply(subgoal_tac "butlast xs @ [last xs] = xs", simp)
-        apply(case_tac xs, simp, simp)
-        done
-    qed
-  qed
-next
-  fix n f xs rs
-  assume "primerec (Mn n f) (length (xs::nat list))" 
-  thus "rec_calc_rel (Mn n f) xs rs = (rec_exec (Mn n f) xs = rs)"
-    by(erule_tac prime_mn_reverse)
-qed
-        
-declare numeral_2_eq_2[simp] numeral_3_eq_3[simp]
-
-lemma [intro]: "primerec rec_right (Suc 0)"
-apply(simp add: rec_right_def rec_lo_def Let_def)
-apply(tactic {* resolve_tac [@{thm prime_cn}, 
-    @{thm prime_id}, @{thm prime_pr}] 1*}, auto+)+
-done
-
-lemma [simp]: 
-"rec_calc_rel rec_right [r] rs = (rec_exec rec_right [r] = rs)"
-apply(rule_tac prime_rel_exec_eq, auto)
-done
-
-lemma [intro]:  "primerec rec_pi (Suc 0)"
-apply(simp add: rec_pi_def rec_dummy_pi_def 
-                rec_np_def rec_fac_def rec_prime_def
-                rec_Minr.simps Let_def get_fstn_args.simps
-                arity.simps
-                rec_all.simps rec_sigma.simps rec_accum.simps)
-apply(tactic {* resolve_tac [@{thm prime_cn}, 
-    @{thm prime_id}, @{thm prime_pr}] 1*}, auto+)+
-apply(simp add: rec_dummyfac_def)
-apply(tactic {* resolve_tac [@{thm prime_cn}, 
-    @{thm prime_id}, @{thm prime_pr}] 1*}, auto+)+
-done
-
-lemma [intro]: "primerec rec_trpl (Suc (Suc (Suc 0)))"
-apply(simp add: rec_trpl_def)
-apply(tactic {* resolve_tac [@{thm prime_cn}, 
-    @{thm prime_id}, @{thm prime_pr}] 1*}, auto+)+
-done
-
-lemma [intro!]: "\<lbrakk>0 < vl; n \<le> vl\<rbrakk> \<Longrightarrow> primerec (rec_listsum2 vl n) vl"
-apply(induct n)
-apply(simp_all add: rec_strt'.simps Let_def rec_listsum2.simps)
-apply(tactic {* resolve_tac [@{thm prime_cn}, 
-    @{thm prime_id}, @{thm prime_pr}] 1*}, auto+)+
-done
-
-lemma [elim]: "\<lbrakk>0 < vl; n \<le> vl\<rbrakk> \<Longrightarrow> primerec (rec_strt' vl n) vl"
-apply(induct n)
-apply(simp_all add: rec_strt'.simps Let_def)
-apply(tactic {* resolve_tac [@{thm prime_cn}, 
-    @{thm prime_id}, @{thm prime_pr}] 1*}, auto+)
-done
-
-lemma [elim]: "vl > 0 \<Longrightarrow> primerec (rec_strt vl) vl"
-apply(simp add: rec_strt.simps rec_strt'.simps)
-apply(tactic {* resolve_tac [@{thm prime_cn}, 
-    @{thm prime_id}, @{thm prime_pr}] 1*}, auto+)+
-done
-
-lemma [elim]: 
-  "i < vl \<Longrightarrow> primerec ((map (\<lambda>i. recf.id (Suc vl) (i)) 
-        [Suc 0..<vl] @ [recf.id (Suc vl) (vl)]) ! i) (Suc vl)"
-apply(induct i, auto simp: nth_append)
-done
-
-lemma [intro]: "primerec rec_newleft0 ((Suc (Suc 0)))"
-apply(simp add: rec_newleft_def rec_embranch.simps 
-                Let_def arity.simps rec_newleft0_def
-                rec_newleft1_def rec_newleft2_def rec_newleft3_def)
-apply(tactic {* resolve_tac [@{thm prime_cn}, 
-    @{thm prime_id}, @{thm prime_pr}] 1*}, auto+)+
-done
-
-lemma [intro]: "primerec rec_newleft1 ((Suc (Suc 0)))"
-apply(simp add: rec_newleft_def rec_embranch.simps 
-                Let_def arity.simps rec_newleft0_def
-                rec_newleft1_def rec_newleft2_def rec_newleft3_def)
-apply(tactic {* resolve_tac [@{thm prime_cn}, 
-    @{thm prime_id}, @{thm prime_pr}] 1*}, auto+)+
-done
-
-lemma [intro]: "primerec rec_newleft2 ((Suc (Suc 0)))"
-apply(simp add: rec_newleft_def rec_embranch.simps 
-                Let_def arity.simps rec_newleft0_def
-                rec_newleft1_def rec_newleft2_def rec_newleft3_def)
-apply(tactic {* resolve_tac [@{thm prime_cn}, 
-    @{thm prime_id}, @{thm prime_pr}] 1*}, auto+)+
-done
-
-lemma [intro]: "primerec rec_newleft3 ((Suc (Suc 0)))"
-apply(simp add: rec_newleft_def rec_embranch.simps 
-                Let_def arity.simps rec_newleft0_def
-                rec_newleft1_def rec_newleft2_def rec_newleft3_def)
-apply(tactic {* resolve_tac [@{thm prime_cn}, 
-    @{thm prime_id}, @{thm prime_pr}] 1*}, auto+)+
-done
-
-lemma [intro]: "primerec rec_newleft (Suc (Suc (Suc 0)))"
-apply(simp add: rec_newleft_def rec_embranch.simps 
-                Let_def arity.simps)
-apply(rule_tac prime_cn, auto+)
-done
-
-lemma [intro]: "primerec rec_left (Suc 0)"
-apply(simp add: rec_left_def rec_lo_def rec_entry_def Let_def)
-apply(tactic {* resolve_tac [@{thm prime_cn}, 
-    @{thm prime_id}, @{thm prime_pr}] 1*}, auto+)+
-done
-
-lemma [intro]: "primerec rec_actn (Suc (Suc (Suc 0)))"
-apply(simp add: rec_left_def rec_lo_def rec_entry_def
-                Let_def rec_actn_def)
-apply(tactic {* resolve_tac [@{thm prime_cn}, 
-    @{thm prime_id}, @{thm prime_pr}] 1*}, auto+)+
-done
-
-lemma [intro]: "primerec rec_stat (Suc 0)"
-apply(simp add: rec_left_def rec_lo_def rec_entry_def Let_def 
-                rec_actn_def rec_stat_def)
-apply(tactic {* resolve_tac [@{thm prime_cn}, 
-    @{thm prime_id}, @{thm prime_pr}] 1*}, auto+)+
-done
-
-lemma [intro]: "primerec rec_newstat (Suc (Suc (Suc 0)))"
-apply(simp add: rec_left_def rec_lo_def rec_entry_def 
-                Let_def rec_actn_def rec_stat_def rec_newstat_def)
-apply(tactic {* resolve_tac [@{thm prime_cn}, 
-    @{thm prime_id}, @{thm prime_pr}] 1*}, auto+)+
-done
-
-lemma [intro]: "primerec rec_newrght (Suc (Suc (Suc 0)))"
-apply(simp add: rec_newrght_def rec_embranch.simps
-                Let_def arity.simps rec_newrgt0_def 
-                rec_newrgt1_def rec_newrgt2_def rec_newrgt3_def)
-apply(tactic {* resolve_tac [@{thm prime_cn}, 
-    @{thm prime_id}, @{thm prime_pr}] 1*}, auto+)+
-done
-
-lemma [intro]: "primerec rec_newconf (Suc (Suc 0))"
-apply(simp add: rec_newconf_def)
-apply(tactic {* resolve_tac [@{thm prime_cn}, 
-    @{thm prime_id}, @{thm prime_pr}] 1*}, auto+)+
-done
-
-lemma [intro]: "0 < vl \<Longrightarrow> primerec (rec_inpt (Suc vl)) (Suc vl)"
-apply(simp add: rec_inpt_def)
-apply(tactic {* resolve_tac [@{thm prime_cn}, 
-    @{thm prime_id}, @{thm prime_pr}] 1*}, auto+)+
-done
-
-lemma [intro]: "primerec rec_conf (Suc (Suc (Suc 0)))"
-apply(simp add: rec_conf_def)
-apply(tactic {* resolve_tac [@{thm prime_cn}, 
-    @{thm prime_id}, @{thm prime_pr}] 1*}, auto+)+
-apply(auto simp: numeral_4_eq_4)
-done
-
-lemma [simp]: 
-  "rec_calc_rel rec_conf [m, r, t] rs = 
-                   (rec_exec rec_conf [m, r, t] = rs)"
-apply(rule_tac prime_rel_exec_eq, auto)
-done
-
-lemma [intro]: "primerec rec_lg (Suc (Suc 0))"
-apply(simp add: rec_lg_def Let_def)
-apply(tactic {* resolve_tac [@{thm prime_cn}, 
-    @{thm prime_id}, @{thm prime_pr}] 1*}, auto+)+
-done
-
-lemma [intro]:  "primerec rec_nonstop (Suc (Suc (Suc 0)))"
-apply(simp add: rec_nonstop_def rec_NSTD_def rec_stat_def
-     rec_lo_def Let_def rec_left_def rec_right_def rec_newconf_def
-     rec_newstat_def)
-apply(tactic {* resolve_tac [@{thm prime_cn}, 
-    @{thm prime_id}, @{thm prime_pr}] 1*}, auto+)+
-done
-
-lemma nonstop_eq[simp]: 
-  "rec_calc_rel rec_nonstop [m, r, t] rs = 
-                (rec_exec rec_nonstop [m, r, t] = rs)"
-apply(rule prime_rel_exec_eq, auto)
-done
-
-lemma halt_lemma': 
-  "rec_calc_rel rec_halt [m, r] t = 
-  (rec_calc_rel rec_nonstop [m, r, t] 0 \<and> 
-  (\<forall> t'< t. 
-      (\<exists> y. rec_calc_rel rec_nonstop [m, r, t'] y \<and>
-            y \<noteq> 0)))"
-apply(auto simp: rec_halt_def)
-apply(erule calc_mn_reverse, simp)
-apply(erule_tac calc_mn_reverse)
-apply(erule_tac x = t' in allE, simp)
-apply(rule_tac calc_mn, simp_all)
-done
-
-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, then it is indeed so.
-  *}
-lemma halt_lemma:
-  "rec_calc_rel (rec_halt) [m, r] t = 
-        (rec_exec rec_nonstop [m, r, t] = 0 \<and> 
-           (\<forall> t'< t. (\<exists> y. rec_exec rec_nonstop [m, r, t'] = y
-                    \<and> y \<noteq> 0)))"
-using halt_lemma'[of m  r t]
-by simp
-  
-text {*F: universal machine*}
-
-text {*
-  @{text "valu r"} extracts computing result out of the right number @{text "r"}.
-  *}
-fun valu :: "nat \<Rightarrow> nat"
-  where
-  "valu r = (lg (r + 1) 2) - 1"
-
-text {*
-  @{text "rec_valu"} is the recursive function implementing @{text "valu"}.
-*}
-definition rec_valu :: "recf"
-  where
-  "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_exec rec_valu [r] = valu r"
-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)
-apply(auto simp: prime_s)
-proof -
-  show "primerec rec_lg (Suc (Suc 0))" by auto
-next
-  show "Suc (Suc 0) = Suc (Suc 0)" by simp
-next
-  show "primerec (constn (Suc (Suc 0))) (Suc 0)" by auto
-qed
-
-lemma [simp]: "rec_calc_rel rec_valu [r] rs = 
-                         (rec_exec rec_valu [r] = rs)"
-apply(rule_tac prime_rel_exec_eq, auto)
-done
-
-declare valu.simps[simp del]
-
-text {*
-  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 
-                                      nth_append)
-done
-
-lemma [simp]: 
-  "\<lbrakk>ys \<noteq> [];  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 calc_rel_get_pren: 
-  "\<lbrakk>ys \<noteq> [];  k < length ys\<rbrakk> \<Longrightarrow> 
-  rec_calc_rel (get_fstn_args (length ys) (length ys) ! k) ys
-                                                            (ys ! k)"
-apply(simp)
-apply(rule_tac calc_id, auto)
-done
-
-lemma [elim]:
-  "\<lbrakk>xs \<noteq> []; k < Suc (length xs)\<rbrakk> \<Longrightarrow> 
-  rec_calc_rel (get_fstn_args (Suc (length xs)) 
-              (Suc (length xs)) ! k) (m # xs) ((m # xs) ! k)"
-using calc_rel_get_pren[of "m#xs" k]
-apply(simp)
-done
-
-text {*
-  The correctness of @{text "rec_F"}, halt case.
-  *}
-lemma  F_lemma: 
-  "rec_calc_rel rec_halt [m, r] t \<Longrightarrow>
-  rec_calc_rel rec_F [m, r] (valu (rght (conf m r t)))"
-apply(simp add: rec_F_def)
-apply(rule_tac  rs = "[rght (conf m r t)]" in calc_cn, 
-      auto simp: value_lemma)
-apply(rule_tac rs = "[conf m r t]" in calc_cn,
-      auto simp: right_lemma)
-apply(rule_tac rs = "[m, r, t]" in calc_cn, auto)
-apply(subgoal_tac " k = 0 \<or>  k = Suc 0 \<or> k = Suc (Suc 0)",
-      auto simp:nth_append)
-apply(rule_tac [1-2] calc_id, simp_all add: conf_lemma)
-done
-
-
-text {*
-  The correctness of @{text "rec_F"}, nonhalt case.
-  *}
-lemma F_lemma2: 
-  "\<forall> t. \<not> rec_calc_rel rec_halt [m, r] t \<Longrightarrow> 
-                \<forall> rs. \<not> rec_calc_rel rec_F [m, r] rs"
-apply(auto simp: rec_F_def)
-apply(erule_tac calc_cn_reverse, simp (no_asm_use))+
-proof -
-  fix rs rsa rsb rsc
-  assume h:
-    "\<forall>t. \<not> rec_calc_rel rec_halt [m, r] t" 
-    "length rsa = Suc 0" 
-    "rec_calc_rel rec_valu rsa rs" 
-    "length rsb = Suc 0" 
-    "rec_calc_rel rec_right rsb (rsa ! 0)"
-    "length rsc = (Suc (Suc (Suc 0)))"
-    "rec_calc_rel rec_conf rsc (rsb ! 0)"
-    and g: "\<forall>k<Suc (Suc (Suc 0)). rec_calc_rel ([recf.id (Suc (Suc 0)) 0, 
-          recf.id (Suc (Suc 0)) (Suc 0), rec_halt] ! k) [m, r] (rsc ! k)"
-  have "rec_calc_rel (rec_halt ) [m, r]
-                              (rsc ! (Suc (Suc 0)))"
-    using g
-    apply(erule_tac x = "(Suc (Suc 0))" in allE)
-    apply(simp add:nth_append)
-    done
-  thus "False"
-    using h
-    apply(erule_tac x = "ysb ! (Suc (Suc 0))" in allE, simp)
-    done
-qed
-
-
-subsection {* Coding function of TMs *}
-
-text {*
-  The purpose of this section is to get the coding function of Turing Machine, which is 
-  going to be named @{text "code"}.
-  *}
-
-fun bl2nat :: "block list \<Rightarrow> nat \<Rightarrow> nat"
-  where
-  "bl2nat [] n = 0"
-| "bl2nat (Bk#bl) n = bl2nat bl (Suc n)"
-| "bl2nat (Oc#bl) n = 2^n + bl2nat bl (Suc n)"
-
-fun bl2wc :: "block list \<Rightarrow> nat"
-  where
-  "bl2wc xs = bl2nat xs 0"
-
-fun trpl_code :: "t_conf \<Rightarrow> nat"
-  where
-  "trpl_code (st, l, r) = trpl (bl2wc l) st (bl2wc r)"
-
-declare bl2nat.simps[simp del] bl2wc.simps[simp del]
-        trpl_code.simps[simp del]
-
-fun action_map :: "taction \<Rightarrow> nat"
-  where
-  "action_map W0 = 0"
-| "action_map W1 = 1"
-| "action_map L = 2"
-| "action_map R = 3"
-| "action_map Nop = 4"
-
-fun action_map_iff :: "nat \<Rightarrow> taction"
-  where
-  "action_map_iff (0::nat) = W0"
-| "action_map_iff (Suc 0) = W1"
-| "action_map_iff (Suc (Suc 0)) = L"
-| "action_map_iff (Suc (Suc (Suc 0))) = R"
-| "action_map_iff n = Nop"
-
-fun block_map :: "block \<Rightarrow> nat"
-  where
-  "block_map Bk = 0"
-| "block_map Oc = 1"
-
-fun godel_code' :: "nat list \<Rightarrow> nat \<Rightarrow> nat"
-  where
-  "godel_code' [] n = 1"
-| "godel_code' (x#xs) n = (Pi n)^x * godel_code' xs (Suc n) "
-
-fun godel_code :: "nat list \<Rightarrow> nat"
-  where
-  "godel_code xs = (let lh = length xs in 
-                   2^lh * (godel_code' xs (Suc 0)))"
-
-fun modify_tprog :: "tprog \<Rightarrow> nat list"
-  where
-  "modify_tprog [] =  []"
-| "modify_tprog ((ac, ns)#nl) = action_map ac # ns # modify_tprog nl"
-
-text {*
-  @{text "code tp"} gives the Godel coding of TM program @{text "tp"}.
-  *}
-fun code :: "tprog \<Rightarrow> nat"
-  where 
-  "code tp = (let nl = modify_tprog tp in 
-              godel_code nl)"
-
-subsection {* Relating interperter functions to the execution of TMs *}
-
-lemma [simp]: "bl2wc [] = 0" by(simp add: bl2wc.simps bl2nat.simps)
-term trpl
-
-lemma [simp]: "\<lbrakk>fetch tp 0 b = (nact, ns)\<rbrakk> \<Longrightarrow> action_map nact = 4"
-apply(simp add: fetch.simps)
-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}"
-  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.simps)
-    done
-qed
-
-lemma Pi_not_0[simp]: "Pi n > 0"
-using Pi_gr_1[of n]
-by arith
-
-declare godel_code.simps[simp del]
-
-lemma [simp]: "0 < godel_code' nl n"
-apply(induct nl arbitrary: n)
-apply(auto simp: godel_code'.simps)
-done
-
-lemma godel_code_great: "godel_code nl > 0"
-apply(simp add: godel_code.simps)
-done
-
-lemma godel_code_eq_1: "(godel_code nl = 1) = (nl = [])"
-apply(auto simp: godel_code.simps)
-done
-
-lemma [elim]: 
-  "\<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
-
-term set_of
-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}"
-  have "finite ?setx" by simp
-  moreover have "?setx \<noteq> {}"
-    using prime_ex[of "Pi i"]
-    apply(auto)
-    done
-  ultimately show "Pi i < Min ?setx"
-    apply(simp add: Min_gr_iff)
-    done
-qed    
-
-lemma Pi_inc_gr: "i < j \<Longrightarrow> Pi i < Pi j"
-proof(induct j, simp)
-  fix j
-  assume ind: "i < j \<Longrightarrow> Pi i < Pi j"
-  and h: "i < Suc j"
-  from h show "Pi i < Pi (Suc j)"
-  proof(cases "i < j")
-    case True thus "?thesis"
-    proof -
-      assume "i < j"
-      hence "Pi i < Pi j" by(erule_tac ind)
-      moreover have "Pi j < Pi (Suc j)"
-        apply(simp add: Pi_inc)
-        done
-      ultimately show "?thesis"
-        by simp
-    qed
-  next
-    assume "i < Suc j" "\<not> i < j"
-    hence "i = j"
-      by arith
-    thus "Pi i < Pi (Suc j)"
-      apply(simp add: Pi_inc)
-      done
-  qed
-qed      
-
-lemma Pi_notEq: "i \<noteq> j \<Longrightarrow> Pi i \<noteq> Pi j"
-apply(case_tac "i < j")
-using Pi_inc_gr[of i j]
-apply(simp)
-using Pi_inc_gr[of j i]
-apply(simp)
-done
-
-lemma [intro]: "Prime (Suc (Suc 0))"
-apply(auto simp: Prime.simps)
-apply(case_tac u, simp, case_tac nat, simp, simp)
-done
-
-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}"
-  show "Prime (Min ?setx)"
-  proof -
-    have "finite ?setx" by simp
-    moreover have "?setx \<noteq> {}" 
-      using prime_ex[of "Pi n"]
-      apply(simp)
-      done
-    ultimately show "?thesis"
-      apply(drule_tac Min_in, simp, simp)
-      done
-  qed
-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 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)
-
-lemma coprime_dvd_mult_nat2: "\<lbrakk>coprime (k::nat) n; k dvd n * m\<rbrakk> \<Longrightarrow> k dvd m"
-apply(erule_tac coprime_dvd_mult_nat)
-apply(simp add: dvd_def, auto)
-apply(rule_tac x = ka in exI)
-apply(subgoal_tac "n * m = m * n", simp)
-apply(simp add: nat_mult_commute)
-done
-
-declare godel_code'.simps[simp del]
-
-lemma godel_code'_butlast_last_id' :
-  "godel_code' (ys @ [y]) (Suc j) = godel_code' ys (Suc j) * 
-                                Pi (Suc (length ys + j)) ^ y"
-proof(induct ys arbitrary: j, simp_all add: godel_code'.simps)
-qed  
-
-lemma godel_code'_butlast_last_id: 
-"xs \<noteq> [] \<Longrightarrow> godel_code' xs (Suc j) = 
-  godel_code' (butlast xs) (Suc j) * Pi (length xs + j)^(last xs)"
-apply(subgoal_tac "\<exists> ys y. xs = ys @ [y]")
-apply(erule_tac exE, erule_tac exE, simp add: 
-                            godel_code'_butlast_last_id')
-apply(rule_tac x = "butlast xs" in exI)
-apply(rule_tac x = "last xs" in exI, auto)
-done
-
-lemma godel_code'_not0: "godel_code' xs n \<noteq> 0"
-apply(induct xs, auto simp: godel_code'.simps)
-done
-
-lemma godel_code_append_cons: 
-  "length xs = i \<Longrightarrow> godel_code' (xs@y#ys) (Suc 0)
-    = godel_code' xs (Suc 0) * Pi (Suc i)^y * godel_code' ys (i + 2)"
-proof(induct "length xs" arbitrary: i y ys xs, simp add: godel_code'.simps,simp)
-  fix x xs i y ys
-  assume ind: 
-    "\<And>xs i y ys. \<lbrakk>x = i; length xs = i\<rbrakk> \<Longrightarrow> 
-       godel_code' (xs @ y # ys) (Suc 0) 
-     = godel_code' xs (Suc 0) * Pi (Suc i) ^ y * 
-                             godel_code' ys (Suc (Suc i))"
-  and h: "Suc x = i" 
-         "length (xs::nat list) = i"
-  have 
-    "godel_code' (butlast xs @ last xs # ((y::nat)#ys)) (Suc 0) = 
-        godel_code' (butlast xs) (Suc 0) * Pi (Suc (i - 1))^(last xs) 
-              * godel_code' (y#ys) (Suc (Suc (i - 1)))"
-    apply(rule_tac ind)
-    using h
-    by(auto)
-  moreover have 
-    "godel_code' xs (Suc 0)= godel_code' (butlast xs) (Suc 0) *
-                                                  Pi (i)^(last xs)"
-    using godel_code'_butlast_last_id[of xs] h
-    apply(case_tac "xs = []", simp, simp)
-    done 
-  moreover have "butlast xs @ last xs # y # ys = xs @ y # ys"
-    using h
-    apply(case_tac xs, auto)
-    done
-  ultimately show 
-    "godel_code' (xs @ y # ys) (Suc 0) =
-               godel_code' xs (Suc 0) * Pi (Suc i) ^ y *
-                    godel_code' ys (Suc (Suc i))"
-    using h
-    apply(simp add: godel_code'_not0 Pi_not_0)
-    apply(simp add: godel_code'.simps)
-    done
-qed
-
-lemma Pi_coprime_pre: 
-  "length ps \<le> i \<Longrightarrow> coprime (Pi (Suc i)) (godel_code' ps (Suc 0))"
-proof(induct "length ps" arbitrary: ps, simp add: godel_code'.simps)
-  fix x ps
-  assume ind: 
-    "\<And>ps. \<lbrakk>x = length ps; length ps \<le> i\<rbrakk> \<Longrightarrow>
-                  coprime (Pi (Suc i)) (godel_code' ps (Suc 0))"
-  and h: "Suc x = length ps"
-          "length (ps::nat list) \<le> i"
-  have g: "coprime (Pi (Suc i)) (godel_code' (butlast ps) (Suc 0))"
-    apply(rule_tac ind)
-    using h by auto
-  have k: "godel_code' ps (Suc 0) = 
-         godel_code' (butlast ps) (Suc 0) * Pi (length ps)^(last ps)"
-    using godel_code'_butlast_last_id[of ps 0] h 
-    by(case_tac ps, simp, simp)
-  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 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
-
-lemma Pi_coprime_suf: "i < j \<Longrightarrow> coprime (Pi i) (godel_code' ps j)"
-proof(induct "length ps" arbitrary: ps, simp add: godel_code'.simps)
-  fix x ps
-  assume ind: 
-    "\<And>ps. \<lbrakk>x = length ps; i < j\<rbrakk> \<Longrightarrow> 
-                    coprime (Pi i) (godel_code' ps j)"
-  and h: "Suc x = length (ps::nat list)" "i < j"
-  have g: "coprime (Pi i) (godel_code' (butlast ps) j)"
-    apply(rule ind) using h by auto
-  have k: "(godel_code' ps j) = godel_code' (butlast ps) j *
-                                 Pi (length ps + j - 1)^last ps"
-    using h godel_code'_butlast_last_id[of ps "j - 1"]
-    apply(case_tac "ps = []", simp, simp)
-    done
-  from g have
-    "coprime (Pi i) (godel_code' (butlast ps) j * 
-                          Pi (length ps + j - 1)^last ps)"
-    apply(rule_tac coprime_mult_nat, simp)
-    using  Pi_power_coprime[of i "length ps + j - 1" 1 "last ps"] h
-    apply(auto)
-    done
-  from k and this show "coprime (Pi i) (godel_code' ps j)"
-    by auto
-qed
-
-lemma godel_finite: 
-  "finite {u. Pi (Suc i) ^ u dvd godel_code' nl (Suc 0)}"
-proof(rule_tac n = "godel_code' nl (Suc 0)" in 
-                          bounded_nat_set_is_finite, auto, 
-      case_tac "ia < godel_code' nl (Suc 0)", auto)
-  fix ia 
-  assume g1: "Pi (Suc i) ^ ia dvd godel_code' nl (Suc 0)"
-    and g2: "\<not> ia < godel_code' nl (Suc 0)"
-  from g1 have "Pi (Suc i)^ia \<le> godel_code' nl (Suc 0)"
-    apply(erule_tac dvd_imp_le)
-    using  godel_code'_not0[of nl "Suc 0"] by simp
-  moreover have "ia < Pi (Suc i)^ia"
-    apply(rule x_less_exp)
-    using Pi_gr_1 by auto
-  ultimately show "False"
-    using g2
-    by(auto)
-qed
-
-
-lemma godel_code_in: 
-  "i < length nl \<Longrightarrow>  nl ! i  \<in> {u. Pi (Suc i) ^ u dvd
-                                     godel_code' nl (Suc 0)}"
-proof -
- assume h: "i<length nl"
-  hence "godel_code' (take i nl@(nl!i)#drop (Suc i) nl) (Suc 0)
-           = godel_code' (take i nl) (Suc 0) *  Pi (Suc i)^(nl!i) *
-                               godel_code' (drop (Suc i) nl) (i + 2)"
-    by(rule_tac godel_code_append_cons, simp)
-  moreover from h have "take i nl @ (nl ! i) # drop (Suc i) nl = nl"
-    using upd_conv_take_nth_drop[of i nl "nl ! i"]
-    apply(simp)
-    done
-  ultimately  show 
-    "nl ! i \<in> {u. Pi (Suc i) ^ u dvd godel_code' nl (Suc 0)}"
-    by(simp)
-qed
-     
-lemma godel_code'_get_nth:
-  "i < length nl \<Longrightarrow> Max {u. Pi (Suc i) ^ u dvd 
-                          godel_code' nl (Suc 0)} = nl ! i"
-proof(rule_tac Max_eqI)
-  let ?gc = "godel_code' nl (Suc 0)"
-  assume h: "i < length nl" thus "finite {u. Pi (Suc i) ^ u dvd ?gc}"
-    by (simp add: godel_finite)  
-next
-  fix y
-  let ?suf ="godel_code' (drop (Suc i) nl) (i + 2)"
-  let ?pref = "godel_code' (take i nl) (Suc 0)"
-  assume h: "i < length nl" 
-            "y \<in> {u. Pi (Suc i) ^ u dvd godel_code' nl (Suc 0)}"
-  moreover hence
-    "godel_code' (take i nl@(nl!i)#drop (Suc i) nl) (Suc 0)
-    = ?pref * Pi (Suc i)^(nl!i) * ?suf"
-    by(rule_tac godel_code_append_cons, simp)
-  moreover from h have "take i nl @ (nl!i) # drop (Suc i) nl = nl"
-    using upd_conv_take_nth_drop[of i nl "nl!i"]
-    by simp
-  ultimately show "y\<le>nl!i"
-  proof(simp)
-    let ?suf' = "godel_code' (drop (Suc i) nl) (Suc (Suc i))"
-    assume mult_dvd: 
-      "Pi (Suc i) ^ y dvd ?pref *  Pi (Suc i) ^ nl ! i * ?suf'"
-    hence "Pi (Suc i) ^ y dvd ?pref * Pi (Suc i) ^ nl ! i"
-    proof(rule_tac coprime_dvd_mult_nat)
-      show "coprime (Pi (Suc i)^y) ?suf'"
-      proof -
-        have "coprime (Pi (Suc i) ^ y) (?suf'^(Suc 0))"
-          apply(rule_tac coprime_exp2_nat)
-          apply(rule_tac  Pi_coprime_suf, simp)
-          done
-        thus "?thesis" by simp
-      qed
-    qed
-    hence "Pi (Suc i) ^ y dvd Pi (Suc i) ^ nl ! i"
-    proof(rule_tac coprime_dvd_mult_nat2)
-      show "coprime (Pi (Suc i) ^ y) ?pref"
-      proof -
-        have "coprime (Pi (Suc i)^y) (?pref^Suc 0)"
-          apply(rule_tac coprime_exp2_nat)
-          apply(rule_tac Pi_coprime_pre, simp)
-          done
-        thus "?thesis" by simp
-      qed
-    qed
-    hence "Pi (Suc i) ^ y \<le>  Pi (Suc i) ^ nl ! i "
-      apply(rule_tac dvd_imp_le, auto)
-      done
-    thus "y \<le> nl ! i"
-      apply(rule_tac power_le_imp_le_exp, auto)
-      done
-  qed
-next
-  assume h: "i<length nl"
-  thus "nl ! i \<in> {u. Pi (Suc i) ^ u dvd godel_code' nl (Suc 0)}"
-    by(rule_tac godel_code_in, simp)
-qed
-
-lemma [simp]: 
-  "{u. Pi (Suc i) ^ u dvd (Suc (Suc 0)) ^ length nl * 
-                                     godel_code' nl (Suc 0)} = 
-    {u. Pi (Suc i) ^ u dvd  godel_code' nl (Suc 0)}"
-apply(rule_tac Collect_cong, auto)
-apply(rule_tac n = " (Suc (Suc 0)) ^ length nl" in 
-                                 coprime_dvd_mult_nat2)
-proof -
-  fix u
-  show "coprime (Pi (Suc i) ^ u) ((Suc (Suc 0)) ^ length nl)"
-  proof(rule_tac coprime_exp2_nat)
-    have "Pi 0 = (2::nat)"
-      apply(simp add: Pi.simps)
-      done
-    moreover have "coprime (Pi (Suc i)) (Pi 0)"
-      apply(rule_tac Pi_coprime, simp)
-      done
-    ultimately show "coprime (Pi (Suc i)) (Suc (Suc 0))" by simp
-  qed
-qed
-  
-lemma godel_code_get_nth: 
-  "i < length nl \<Longrightarrow> 
-           Max {u. Pi (Suc i) ^ u dvd godel_code nl} = nl ! i"
-by(simp add: godel_code.simps godel_code'_get_nth)
-
-lemma "trpl l st r = godel_code' [l, st, r] 0"
-apply(simp add: trpl.simps godel_code'.simps)
-done
-
-lemma mod_dvd_simp: "(x mod y = (0::nat)) = (y dvd x)"
-by(simp add: dvd_def, auto)
-
-lemma dvd_power_le: "\<lbrakk>a > Suc 0; a ^ y dvd a ^ l\<rbrakk> \<Longrightarrow> y \<le> l"
-apply(case_tac "y \<le> l", simp, simp)
-apply(subgoal_tac "\<exists> d. y = l + d", auto simp: power_add)
-apply(rule_tac x = "y - l" in exI, simp)
-done
-
-
-lemma [elim]: "Pi n = 0 \<Longrightarrow> RR"
-  using Pi_not_0[of n] by simp
-
-lemma [elim]: "Pi n = Suc 0 \<Longrightarrow> RR"
-  using Pi_gr_1[of n] by simp
-
-lemma finite_power_dvd:
-  "\<lbrakk>(a::nat) > Suc 0; y \<noteq> 0\<rbrakk> \<Longrightarrow> finite {u. a^u dvd y}"
-apply(auto simp: dvd_def)
-apply(rule_tac n = y in bounded_nat_set_is_finite, auto)
-apply(case_tac k, simp,simp)
-apply(rule_tac trans_less_add1)
-apply(erule_tac x_less_exp)
-done
-
-lemma conf_decode1: "\<lbrakk>m \<noteq> n; m \<noteq> k; k \<noteq> n\<rbrakk> \<Longrightarrow> 
-  Max {u. Pi m ^ u dvd Pi m ^ l * Pi n ^ st * Pi k ^ r} = l"
-proof -
-  let ?setx = "{u. Pi m ^ u dvd Pi m ^ l * Pi n ^ st * Pi k ^ r}"
-  assume g: "m \<noteq> n" "m \<noteq> k" "k \<noteq> n"
-  show "Max ?setx = l"
-  proof(rule_tac Max_eqI)
-    show "finite ?setx"
-      apply(rule_tac finite_power_dvd, auto simp: Pi_gr_1)
-      done
-  next
-    fix y
-    assume h: "y \<in> ?setx"
-    have "Pi m ^ y dvd Pi m ^ l"
-    proof -
-      have "Pi m ^ y dvd Pi m ^ l * Pi n ^ st"
-        using h g
-        apply(rule_tac n = "Pi k^r" in coprime_dvd_mult_nat)
-        apply(rule Pi_power_coprime, simp, simp)
-        done
-      thus "Pi m^y dvd Pi m^l"
-        apply(rule_tac n = " Pi n ^ st" in coprime_dvd_mult_nat)
-        using g
-        apply(rule_tac Pi_power_coprime, simp, simp)
-        done
-    qed
-    thus "y \<le> (l::nat)"
-      apply(rule_tac a = "Pi m" in power_le_imp_le_exp)
-      apply(simp_all add: Pi_gr_1)
-      apply(rule_tac dvd_power_le, auto)
-      done
-  next
-    show "l \<in> ?setx" by simp
-  qed
-qed  
-
-lemma conf_decode2: 
-  "\<lbrakk>m \<noteq> n; m \<noteq> k; n \<noteq> k; 
-  \<not> Suc 0 < Pi m ^ l * Pi n ^ st * Pi k ^ r\<rbrakk> \<Longrightarrow> l = 0"
-apply(case_tac "Pi m ^ l * Pi n ^ st * Pi k ^ r", auto)
-done
-
-lemma [simp]: "left (trpl l st r) = l"
-apply(simp add: left.simps trpl.simps lo.simps 
-              loR.simps mod_dvd_simp, auto simp: conf_decode1)
-apply(case_tac "Pi 0 ^ l * Pi (Suc 0) ^ st * Pi (Suc (Suc 0)) ^ r",
-      auto)
-apply(erule_tac x = l in allE, auto)
-done   
-
-lemma [simp]: "stat (trpl l st r) = st"
-apply(simp add: stat.simps trpl.simps lo.simps 
-                loR.simps mod_dvd_simp, auto)
-apply(subgoal_tac "Pi 0 ^ l * Pi (Suc 0) ^ st * Pi (Suc (Suc 0)) ^ r
-               = Pi (Suc 0)^st * Pi 0 ^ l *  Pi (Suc (Suc 0)) ^ r")
-apply(simp (no_asm_simp) add: conf_decode1, simp)
-apply(case_tac "Pi 0 ^ l * Pi (Suc 0) ^ st * 
-                                  Pi (Suc (Suc 0)) ^ r", auto)
-apply(erule_tac x = st in allE, auto)
-done
-
-lemma [simp]: "rght (trpl l st r) = r"
-apply(simp add: rght.simps trpl.simps lo.simps 
-                loR.simps mod_dvd_simp, auto)
-apply(subgoal_tac "Pi 0 ^ l * Pi (Suc 0) ^ st * Pi (Suc (Suc 0)) ^ r
-               = Pi (Suc (Suc 0))^r * Pi 0 ^ l *  Pi (Suc 0) ^ st")
-apply(simp (no_asm_simp) add: conf_decode1, simp)
-apply(case_tac "Pi 0 ^ l * Pi (Suc 0) ^ st * Pi (Suc (Suc 0)) ^ r",
-       auto)
-apply(erule_tac x = r in allE, auto)
-done
-
-lemma max_lor:
-  "i < length nl \<Longrightarrow> Max {u. loR [godel_code nl, Pi (Suc i), u]} 
-                   = nl ! i"
-apply(simp add: loR.simps godel_code_get_nth mod_dvd_simp)
-done
-
-lemma godel_decode: 
-  "i < length nl \<Longrightarrow> Entry (godel_code nl) i = nl ! i"
-apply(auto simp: Entry.simps lo.simps max_lor)
-apply(erule_tac x = "nl!i" in allE)
-using max_lor[of i nl] godel_finite[of i nl]
-apply(simp)
-apply(drule_tac Max_in, auto simp: loR.simps 
-                   godel_code.simps mod_dvd_simp)
-using godel_code_in[of i nl]
-apply(simp)
-done
-
-lemma Four_Suc: "4 = Suc (Suc (Suc (Suc 0)))"
-by auto
-
-declare numeral_2_eq_2[simp del]
-
-lemma modify_tprog_fetch_even: 
-  "\<lbrakk>st \<le> length tp div 2; st > 0\<rbrakk> \<Longrightarrow>
-  modify_tprog tp ! (4 * (st - Suc 0) ) = 
-  action_map (fst (tp ! (2 * (st - Suc 0))))"
-proof(induct st arbitrary: tp, simp)
-  fix tp st
-  assume ind: 
-    "\<And>tp. \<lbrakk>st \<le> length tp div 2; 0 < st\<rbrakk> \<Longrightarrow> 
-     modify_tprog tp ! (4 * (st - Suc 0)) =
-               action_map (fst ((tp::tprog) ! (2 * (st - Suc 0))))"
-  and h: "Suc st \<le> length (tp::tprog) div 2" "0 < Suc st"
-  thus "modify_tprog tp ! (4 * (Suc st - Suc 0)) = 
-          action_map (fst (tp ! (2 * (Suc st - Suc 0))))"
-  proof(cases "st = 0")
-    case True thus "?thesis"
-      using h
-      apply(auto)
-      apply(cases tp, simp, case_tac a, simp add: modify_tprog.simps)
-      done
-  next
-    case False
-    assume g: "st \<noteq> 0"
-    hence "\<exists> aa ab ba bb tp'. tp = (aa, ab) # (ba, bb) # tp'"
-      using h
-      apply(case_tac tp, simp, case_tac list, simp, simp)
-      done
-    from this obtain aa ab ba bb tp' where g1: 
-      "tp = (aa, ab) # (ba, bb) # tp'" by blast
-    hence g2: 
-      "modify_tprog tp' ! (4 * (st - Suc 0)) = 
-      action_map (fst ((tp'::tprog) ! (2 * (st - Suc 0))))"
-      apply(rule_tac ind)
-      using h g by auto
-    thus "?thesis"
-      using g1 g
-      apply(case_tac st, simp, simp add: Four_Suc)
-      done
-  qed
-qed
-      
-lemma modify_tprog_fetch_odd: 
-  "\<lbrakk>st \<le> length tp div 2; st > 0\<rbrakk> \<Longrightarrow> 
-       modify_tprog tp ! (Suc (Suc (4 * (st - Suc 0)))) = 
-       action_map (fst (tp ! (Suc (2 * (st - Suc 0)))))"
-proof(induct st arbitrary: tp, simp)
-  fix tp st
-  assume ind: 
-    "\<And>tp. \<lbrakk>st \<le> length tp div 2; 0 < st\<rbrakk> \<Longrightarrow>  
-       modify_tprog tp ! Suc (Suc (4 * (st - Suc 0))) = 
-          action_map (fst (tp ! Suc (2 * (st - Suc 0))))"
-  and h: "Suc st \<le> length (tp::tprog) div 2" "0 < Suc st"
-  thus "modify_tprog tp ! Suc (Suc (4 * (Suc st - Suc 0))) 
-     = action_map (fst (tp ! Suc (2 * (Suc st - Suc 0))))"
-  proof(cases "st = 0")
-    case True thus "?thesis"
-      using h
-      apply(auto)
-      apply(cases tp, simp, case_tac a, simp add: modify_tprog.simps)
-      apply(case_tac list, simp, case_tac ab,
-             simp add: modify_tprog.simps)
-      done
-  next
-    case False
-    assume g: "st \<noteq> 0"
-    hence "\<exists> aa ab ba bb tp'. tp = (aa, ab) # (ba, bb) # tp'"
-      using h
-      apply(case_tac tp, simp, case_tac list, simp, simp)
-      done
-    from this obtain aa ab ba bb tp' where g1: 
-      "tp = (aa, ab) # (ba, bb) # tp'" by blast
-    hence g2: "modify_tprog tp' ! Suc (Suc (4 * (st  - Suc 0))) = 
-          action_map (fst (tp' ! Suc (2 * (st - Suc 0))))"
-      apply(rule_tac ind)
-      using h g by auto
-    thus "?thesis"
-      using g1 g
-      apply(case_tac st, simp, simp add: Four_Suc)
-      done
-  qed
-qed    
-         
-lemma modify_tprog_fetch_action:
-  "\<lbrakk>st \<le> length tp div 2; st > 0; b = 1 \<or> b = 0\<rbrakk> \<Longrightarrow> 
-      modify_tprog tp ! (4 * (st - Suc 0) + 2* b) =
-      action_map (fst (tp ! ((2 * (st - Suc 0)) + b)))"
-apply(erule_tac disjE, auto elim: modify_tprog_fetch_odd
-                                   modify_tprog_fetch_even)
-done 
-
-lemma length_modify: "length (modify_tprog tp) = 2 * length tp"
-apply(induct tp, auto)
-done
-
-declare fetch.simps[simp del]
-
-lemma fetch_action_eq: 
-  "\<lbrakk>block_map b = scan r; fetch tp st b = (nact, ns);
-   st \<le> length tp div 2\<rbrakk> \<Longrightarrow> actn (code tp) st r = action_map nact"
-proof(simp add: actn.simps, auto)
-  let ?i = "4 * (st - Suc 0) + 2 * (r mod 2)"
-  assume h: "block_map b = r mod 2" "fetch tp st b = (nact, ns)" 
-            "st \<le> length tp div 2" "0 < st"
-  have "?i < length (modify_tprog tp)"
-  proof -
-    have "length (modify_tprog tp) = 2 * length tp"
-      by(simp add: length_modify)
-    thus "?thesis"
-      using h
-      by(auto)
-  qed
-  hence 
-    "Entry (godel_code (modify_tprog tp))?i = 
-                                   (modify_tprog tp) ! ?i"
-    by(erule_tac godel_decode)
-   moreover have 
-    "modify_tprog tp ! ?i = 
-            action_map (fst (tp ! (2 * (st - Suc 0) + r mod 2)))"
-    apply(rule_tac  modify_tprog_fetch_action)
-    using h
-    by(auto)    
-  moreover have "(fst (tp ! (2 * (st - Suc 0) + r mod 2))) = nact"
-    using h
-    apply(simp add: fetch.simps nth_of.simps)
-    apply(case_tac b, auto simp: block_map.simps nth_of.simps split: if_splits)
-    done
-  ultimately show 
-    "Entry (godel_code (modify_tprog tp))
-                      (4 * (st - Suc 0) + 2 * (r mod 2))
-           = action_map nact" 
-    by simp
-qed
-
-lemma [simp]: "fetch tp 0 b = (nact, ns) \<Longrightarrow> ns = 0"
-by(simp add: fetch.simps)
-
-lemma Five_Suc: "5 = Suc 4" by simp
-
-lemma modify_tprog_fetch_state:
-  "\<lbrakk>st \<le> length tp div 2; st > 0; b = 1 \<or> b = 0\<rbrakk> \<Longrightarrow> 
-     modify_tprog tp ! Suc (4 * (st - Suc 0) + 2 * b) =
-  (snd (tp ! (2 * (st - Suc 0) + b)))"
-proof(induct st arbitrary: tp, simp)
-  fix st tp
-  assume ind: 
-    "\<And>tp. \<lbrakk>st \<le> length tp div 2; 0 < st; b = 1 \<or> b = 0\<rbrakk> \<Longrightarrow> 
-    modify_tprog tp ! Suc (4 * (st - Suc 0) + 2 * b) =
-                             snd (tp ! (2 * (st - Suc 0) + b))"
-  and h:
-    "Suc st \<le> length (tp::tprog) div 2" 
-    "0 < Suc st" 
-    "b = 1 \<or> b = 0"
-  show "modify_tprog tp ! Suc (4 * (Suc st - Suc 0) + 2 * b) =
-                             snd (tp ! (2 * (Suc st - Suc 0) + b))"
-  proof(cases "st = 0")
-    case True
-    thus "?thesis"
-      using h
-      apply(cases tp, simp, case_tac a, simp add: modify_tprog.simps)
-      apply(case_tac list, simp, case_tac ab, 
-                         simp add: modify_tprog.simps, auto)
-      done
-  next
-    case False
-    assume g: "st \<noteq> 0"
-    hence "\<exists> aa ab ba bb tp'. tp = (aa, ab) # (ba, bb) # tp'"
-      using h
-      apply(case_tac tp, simp, case_tac list, simp, simp)
-      done
-    from this obtain aa ab ba bb tp' where g1:
-      "tp = (aa, ab) # (ba, bb) # tp'" by blast
-    hence g2: 
-      "modify_tprog tp' ! Suc (4 * (st - Suc 0) + 2 * b) =
-                              snd (tp' ! (2 * (st - Suc 0) + b))"
-      apply(rule_tac ind)
-      using h g by auto
-    thus "?thesis"
-      using g1 g
-      apply(case_tac st, simp, simp)
-      done
-  qed
-qed
-  
-lemma fetch_state_eq:
-  "\<lbrakk>block_map b = scan r; 
-  fetch tp st b = (nact, ns);
-  st \<le> length tp div 2\<rbrakk> \<Longrightarrow> newstat (code tp) st r = ns"
-proof(simp add: newstat.simps, auto)
-  let ?i = "Suc (4 * (st - Suc 0) + 2 * (r mod 2))"
-  assume h: "block_map b = r mod 2" "fetch tp st b =
-             (nact, ns)" "st \<le> length tp div 2" "0 < st"
-  have "?i < length (modify_tprog tp)"
-  proof -
-    have "length (modify_tprog tp) = 2 * length tp"
-      apply(simp add: length_modify)
-      done
-    thus "?thesis"
-      using h
-      by(auto)
-  qed
-  hence "Entry (godel_code (modify_tprog tp)) (?i) = 
-                                  (modify_tprog tp) ! ?i"
-    by(erule_tac godel_decode)
-   moreover have 
-    "modify_tprog tp ! ?i =  
-               (snd (tp ! (2 * (st - Suc 0) + r mod 2)))"
-    apply(rule_tac  modify_tprog_fetch_state)
-    using h
-    by(auto)
-  moreover have "(snd (tp ! (2 * (st - Suc 0) + r mod 2))) = ns"
-    using h
-    apply(simp add: fetch.simps nth_of.simps)
-    apply(case_tac b, auto simp: block_map.simps nth_of.simps
-                                 split: if_splits)
-    done
-  ultimately show "Entry (godel_code (modify_tprog tp)) (?i)
-           = ns" 
-    by simp
-qed
-
-
-lemma [intro!]: 
-  "\<lbrakk>a = a'; b = b'; c = c'\<rbrakk> \<Longrightarrow> trpl a b c = trpl a' b' c'"
-by simp
-
-lemma [simp]: "bl2wc [Bk] = 0"
-by(simp add: bl2wc.simps bl2nat.simps)
-
-lemma bl2nat_double: "bl2nat xs (Suc n) = 2 * bl2nat xs n"
-proof(induct xs arbitrary: n)
-  case Nil thus "?case"
-    by(simp add: bl2nat.simps)
-next
-  case (Cons x xs) thus "?case"
-  proof -
-    assume ind: "\<And>n. bl2nat xs (Suc n) = 2 * bl2nat xs n "
-    show "bl2nat (x # xs) (Suc n) = 2 * bl2nat (x # xs) n"
-    proof(cases x)
-      case Bk thus "?thesis"
-        apply(simp add: bl2nat.simps)
-        using ind[of "Suc n"] by simp
-    next
-      case Oc thus "?thesis"
-        apply(simp add: bl2nat.simps)
-        using ind[of "Suc n"] by simp
-    qed
-  qed
-qed
-
-
-lemma [simp]: "c \<noteq> [] \<Longrightarrow> 2 * bl2wc (tl c) = bl2wc c - bl2wc c mod 2 "
-apply(case_tac c, simp, case_tac a)
-apply(auto simp: bl2wc.simps bl2nat.simps bl2nat_double)
-done
-
-lemma [simp]:
-  "c \<noteq> [] \<Longrightarrow> bl2wc (Oc # tl c) = Suc (bl2wc c) - bl2wc c mod 2 "
-apply(case_tac c, simp, case_tac a)
-apply(auto simp: bl2wc.simps bl2nat.simps bl2nat_double)
-done
-
-lemma [simp]: "bl2wc (Bk # c) = 2*bl2wc (c)"
-apply(simp add: bl2wc.simps bl2nat.simps bl2nat_double)
-done
-
-lemma [simp]: "bl2wc [Oc] = Suc 0"
- by(simp add: bl2wc.simps bl2nat.simps)
-
-lemma [simp]: "b \<noteq> [] \<Longrightarrow> bl2wc (tl b) = bl2wc b div 2"
-apply(case_tac b, simp, case_tac a)
-apply(auto simp: bl2wc.simps bl2nat.simps bl2nat_double)
-done
-
-lemma [simp]: "b \<noteq> [] \<Longrightarrow> bl2wc ([hd b]) = bl2wc b mod 2"
-apply(case_tac b, simp, case_tac a)
-apply(auto simp: bl2wc.simps bl2nat.simps bl2nat_double)
-done
-
-lemma [simp]: "\<lbrakk>b \<noteq> []; c \<noteq> []\<rbrakk> \<Longrightarrow> bl2wc (hd b # c) = 2 * bl2wc c + bl2wc b mod 2"
-apply(case_tac b, simp, case_tac a)
-apply(auto simp: bl2wc.simps bl2nat.simps bl2nat_double)
-done
-
-lemma [simp]: " 2 * (bl2wc c div 2) = bl2wc c - bl2wc c mod 2" 
-  by(simp add: mult_div_cancel)
-
-lemma [simp]: "bl2wc (Oc # list) mod 2 = Suc 0" 
-  by(simp add: bl2wc.simps bl2nat.simps bl2nat_double)
-
-
-declare code.simps[simp del]
-declare nth_of.simps[simp del]
-declare new_tape.simps[simp del]
-
-text {*
-  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 (tstep c tp) = 
-  rec_exec rec_newconf [code tp, trpl_code c]"
-apply(cases c, auto simp: tstep.simps)
-proof(case_tac "fetch tp a (case c of [] \<Rightarrow> Bk | x # xs \<Rightarrow> x)",
-      simp add: newconf.simps trpl_code.simps)
-  fix a b c aa ba
-  assume h: "(a::nat) \<le> length tp div 2" 
-    "fetch tp a (case c of [] \<Rightarrow> Bk | x # xs \<Rightarrow> x) = (aa, ba)"
-  moreover hence "actn (code tp) a (bl2wc c) = action_map aa"
-    apply(rule_tac b = "(case c of [] \<Rightarrow> Bk | x # xs \<Rightarrow> x)" 
-          in fetch_action_eq, auto)
-    apply(auto split: list.splits)
-    apply(case_tac ab, auto)
-    done
-  moreover from h have "(newstat (code tp) a (bl2wc c)) = ba"
-    apply(rule_tac b = "(case c of [] \<Rightarrow> Bk | x # xs \<Rightarrow> x)" 
-          in fetch_state_eq, auto split: list.splits)
-    apply(case_tac ab, auto)
-    done
-  ultimately show 
-    "trpl_code (ba, new_tape aa (b, c)) =
-    trpl (newleft (bl2wc b) (bl2wc c) (actn (code tp) a (bl2wc c))) 
-    (newstat (code tp) a (bl2wc c)) (newrght (bl2wc b) (bl2wc c) 
-     (actn  (code tp) a (bl2wc c)))"
-    by(auto simp: new_tape.simps trpl_code.simps 
-         newleft.simps newrght.simps split: taction.splits)
-qed
-
-lemma [simp]: "a\<^bsup>0\<^esup> = []"
-apply(simp add: exp_zero)
-done
-lemma [simp]: "bl2nat (Oc # Oc\<^bsup>x\<^esup>) 0 = (2 * 2 ^ x - Suc 0)"
-apply(induct x)
-apply(simp add: bl2nat.simps)
-apply(simp add: bl2nat.simps bl2nat_double exp_ind_def)
-done
-
-lemma [simp]: "bl2nat (Oc\<^bsup>y\<^esup>) 0 = 2^y - Suc 0"
-apply(induct y, auto simp: bl2nat.simps exp_ind_def bl2nat_double)
-apply(case_tac "(2::nat)^y", auto)
-done
-
-lemma [simp]: "bl2nat (Bk\<^bsup>l\<^esup>) n = 0"
-apply(induct l, auto simp: bl2nat.simps bl2nat_double exp_ind_def)
-done
-
-lemma bl2nat_cons_bk: "bl2nat (ks @ [Bk]) 0 = bl2nat ks 0"
-apply(induct ks, auto simp: bl2nat.simps split: block.splits)
-apply(case_tac a, auto simp: bl2nat.simps bl2nat_double)
-done
-
-lemma bl2nat_cons_oc:
-  "bl2nat (ks @ [Oc]) 0 =  bl2nat ks 0 + 2 ^ length ks"
-apply(induct ks, auto simp: bl2nat.simps split: block.splits)
-apply(case_tac a, auto simp: bl2nat.simps bl2nat_double)
-done
-
-lemma bl2nat_append: 
-  "bl2nat (xs @ ys) 0 = bl2nat xs 0 + bl2nat ys (length xs) "
-proof(induct "length xs" arbitrary: xs ys, simp add: bl2nat.simps)
-  fix x xs ys
-  assume ind: 
-    "\<And>xs ys. x = length xs \<Longrightarrow> 
-             bl2nat (xs @ ys) 0 = bl2nat xs 0 + bl2nat ys (length xs)"
-  and h: "Suc x = length (xs::block list)"
-  have "\<exists> ks k. xs = ks @ [k]" 
-    apply(rule_tac x = "butlast xs" in exI,
-      rule_tac x = "last xs" in exI)
-    using h
-    apply(case_tac xs, auto)
-    done
-  from this obtain ks k where "xs = ks @ [k]" by blast
-  moreover hence 
-    "bl2nat (ks @ (k # ys)) 0 = bl2nat ks 0 +
-                               bl2nat (k # ys) (length ks)"
-    apply(rule_tac ind) using h by simp
-  ultimately show "bl2nat (xs @ ys) 0 = 
-                  bl2nat xs 0 + bl2nat ys (length xs)"
-    apply(case_tac k, simp_all add: bl2nat.simps)
-    apply(simp_all only: bl2nat_cons_bk bl2nat_cons_oc)
-    done
-qed
-
-lemma bl2nat_exp:  "n \<noteq> 0 \<Longrightarrow> bl2nat bl n = 2^n * bl2nat bl 0"
-apply(induct bl)
-apply(auto simp: bl2nat.simps)
-apply(case_tac a, auto simp: bl2nat.simps bl2nat_double)
-done
-
-lemma nat_minus_eq: "\<lbrakk>a = b; c = d\<rbrakk> \<Longrightarrow> a - c = b - d"
-by auto
-
-lemma tape_of_nat_list_butlast_last:
-  "ys \<noteq> [] \<Longrightarrow> <ys @ [y]> = <ys> @ Bk # Oc\<^bsup>Suc y\<^esup>"
-apply(induct ys, simp, simp)
-apply(case_tac "ys = []", simp add: tape_of_nl_abv 
-                                    tape_of_nat_list.simps)
-apply(simp)
-done
-
-lemma listsum2_append:
-  "\<lbrakk>n \<le> length xs\<rbrakk> \<Longrightarrow> listsum2 (xs @ ys) n = listsum2 xs n"
-apply(induct n)
-apply(auto simp: listsum2.simps nth_append)
-done
-
-lemma strt'_append:  
-  "\<lbrakk>n \<le> length xs\<rbrakk> \<Longrightarrow> strt' xs n = strt' (xs @ ys) n"
-proof(induct n arbitrary: xs ys)
-  fix xs ys
-  show "strt' xs 0 = strt' (xs @ ys) 0" by(simp add: strt'.simps)
-next
-  fix n xs ys
-  assume ind: 
-    "\<And> xs ys. n \<le> length xs \<Longrightarrow> strt' xs n = strt' (xs @ ys) n"
-    and h: "Suc n \<le> length (xs::nat list)"
-  show "strt' xs (Suc n) = strt' (xs @ ys) (Suc n)"
-    using ind[of xs ys] h
-    apply(simp add: strt'.simps nth_append listsum2_append)
-    done
-qed
-    
-lemma length_listsum2_eq: 
-  "\<lbrakk>length (ys::nat list) = k\<rbrakk>
-       \<Longrightarrow> length (<ys>) = listsum2 (map Suc ys) k + k - 1"
-apply(induct k arbitrary: ys, simp_all add: listsum2.simps)
-apply(subgoal_tac "\<exists> xs x. ys = xs @ [x]", auto)
-proof -
-  fix xs x
-  assume ind: "\<And>ys. length ys = length xs \<Longrightarrow> length (<ys>) 
-    = listsum2 (map Suc ys) (length xs) + 
-      length (xs::nat list) - Suc 0"
-  have "length (<xs>) 
-    = listsum2 (map Suc xs) (length xs) + length xs - Suc 0"
-    apply(rule_tac ind, simp)
-    done
-  thus "length (<xs @ [x]>) =
-    Suc (listsum2 (map Suc xs @ [Suc x]) (length xs) + x + length xs)"
-    apply(case_tac "xs = []")
-    apply(simp add: tape_of_nl_abv listsum2.simps 
-      tape_of_nat_list.simps)
-    apply(simp add: tape_of_nat_list_butlast_last)
-    using listsum2_append[of "length xs" "map Suc xs" "[Suc x]"]
-    apply(simp)
-    done
-next
-  fix k ys
-  assume "length ys = Suc k" 
-  thus "\<exists>xs x. ys = xs @ [x]"
-    apply(rule_tac x = "butlast ys" in exI, 
-          rule_tac x = "last ys" in exI)
-    apply(case_tac ys, auto)
-    done
-qed  
-
-lemma tape_of_nat_list_length: 
-      "length (<(ys::nat list)>) = 
-              listsum2 (map Suc ys) (length ys) + length ys - 1"
-  using length_listsum2_eq[of ys "length ys"]
-  apply(simp)
-  done
-
-
-
-lemma [simp]:
- "trpl_code (steps (Suc 0, Bk\<^bsup>l\<^esup>, <lm>) tp 0) = 
-    rec_exec rec_conf [code tp, bl2wc (<lm>), 0]"
-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"}
-  with the multi-step execution of TMs.
-  *}
-lemma rec_t_eq_steps:
-  "turing_basic.t_correct tp \<Longrightarrow>
-  trpl_code (steps (Suc 0, Bk\<^bsup>l\<^esup>, <lm>) tp 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: 
-      "t_correct tp \<Longrightarrow> trpl_code (steps (Suc 0, Bk\<^bsup>l\<^esup>, <lm>) tp n) 
-      = rec_exec rec_conf [code tp, bl2wc (<lm>), n]"
-      and h: "t_correct tp"
-    show 
-      "trpl_code (steps (Suc 0, Bk\<^bsup>l\<^esup>, <lm>) tp (Suc n)) =
-      rec_exec rec_conf [code tp, bl2wc (<lm>), Suc n]"
-    proof(case_tac "steps (Suc 0, Bk\<^bsup>l\<^esup>, <lm>) tp  n", 
-        simp only: tstep_red conf_lemma conf.simps)
-      fix a b c
-      assume g: "steps (Suc 0, Bk\<^bsup>l\<^esup>, <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 (tstep (a, b, c) tp) = 
-        rec_exec rec_newconf [code tp, trpl_code (a, b, c)]"
-        apply(rule_tac rec_t_eq_step)
-        using h g
-        apply(simp add: s_keep)
-        done
-      ultimately show 
-        "trpl_code (tstep (a, b, c) tp) =
-            newconf (code tp) (conf (code tp) (bl2wc (<lm>)) n)"
-        by(simp add: newconf_lemma)
-    qed
-  qed
-qed
-
-lemma [simp]: "bl2wc (Bk\<^bsup>m\<^esup>) = 0"
-apply(induct m)
-apply(simp, simp)
-done
-
-lemma [simp]: "bl2wc (Oc\<^bsup>rs\<^esup>@Bk\<^bsup>n\<^esup>) = bl2wc (Oc\<^bsup>rs\<^esup>)"
-apply(induct rs, simp, 
-  simp add: bl2wc.simps bl2nat.simps bl2nat_double)
-done
-
-lemma lg_power: "x > Suc 0 \<Longrightarrow> lg (x ^ rs) x = rs"
-proof(simp add: lg.simps, auto)
-  fix xa
-  assume h: "Suc 0 < x"
-  show "Max {ya. ya \<le> x ^ rs \<and> lgR [x ^ rs, x, ya]} = rs"
-    apply(rule_tac Max_eqI, simp_all add: lgR.simps)
-    apply(simp add: h)
-    using x_less_exp[of x rs] h
-    apply(simp)
-    done
-next
-  assume "\<not> Suc 0 < x ^ rs" "Suc 0 < x" 
-  thus "rs = 0"
-    apply(case_tac "x ^ rs", simp, simp)
-    done
-next
-  assume "Suc 0 < x" "\<forall>xa. \<not> lgR [x ^ rs, x, xa]"
-  thus "rs = 0"
-    apply(simp only:lgR.simps)
-    apply(erule_tac x = rs in allE, simp)
-    done
-qed    
-
-text {*
-  The following lemma relates execution of TMs with 
-  the multi-step interpreter function @{text "rec_nonstop"}. Note,
-  @{text "rec_nonstop"} is constructed using @{text "rec_conf"}.
-  *}
-lemma nonstop_t_eq: 
-  "\<lbrakk>steps (Suc 0, Bk\<^bsup>l\<^esup>, <lm>) tp stp = (0, Bk\<^bsup>m\<^esup>, Oc\<^bsup>rs\<^esup> @ Bk\<^bsup>n\<^esup>); 
-  turing_basic.t_correct tp; 
-  rs > 0\<rbrakk> 
-  \<Longrightarrow> rec_exec rec_nonstop [code tp, bl2wc (<lm>), stp] = 0"
-proof(simp add: nonstop_lemma nonstop.simps nstd.simps)
-  assume h: "steps (Suc 0, Bk\<^bsup>l\<^esup>, <lm>) tp stp = (0, Bk\<^bsup>m\<^esup>, Oc\<^bsup>rs\<^esup> @ Bk\<^bsup>n\<^esup>)"
-  and tc_t: "turing_basic.t_correct tp" "rs > 0"
-  have g: "rec_exec rec_conf [code tp,  bl2wc (<lm>), stp] =
-                                        trpl_code (0, Bk\<^bsup>m\<^esup>, Oc\<^bsup>rs\<^esup>@Bk\<^bsup>n\<^esup>)"
-    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)
-    show "stat (conf (code tp) (bl2wc (<lm>)) stp) = 0"
-      using g
-      by(auto simp: conf_lemma trpl_code.simps)
-  next
-    show "left (conf (code tp) (bl2wc (<lm>)) stp) = 0"
-      using g
-      by(simp add: conf_lemma trpl_code.simps)
-  next
-    show "rght (conf (code tp) (bl2wc (<lm>)) stp) = 
-           2 ^ lg (Suc (rght (conf (code tp) (bl2wc (<lm>)) stp))) 2 - Suc 0"
-    using g h
-    proof(simp add: conf_lemma trpl_code.simps)
-      have "2 ^ lg (Suc (bl2wc (Oc\<^bsup>rs\<^esup>))) 2 = Suc (bl2wc (Oc\<^bsup>rs\<^esup>))"
-        apply(simp add: bl2wc.simps lg_power)
-        done
-      thus "bl2wc (Oc\<^bsup>rs\<^esup>) = 2 ^ lg (Suc (bl2wc (Oc\<^bsup>rs\<^esup>))) 2 - Suc 0"
-        apply(simp)
-        done
-    qed
-  next
-    show "0 < rght (conf (code tp) (bl2wc (<lm>)) stp)"
-      using g h tc_t
-      apply(simp add: conf_lemma trpl_code.simps bl2wc.simps
-                      bl2nat.simps)
-      apply(case_tac rs, simp, simp add: bl2nat.simps)
-      done
-  qed
-qed
-
-lemma [simp]: "actn m 0 r = 4"
-by(simp add: actn.simps)
-
-lemma [simp]: "newstat m 0 r = 0"
-by(simp add: newstat.simps)
- 
-declare exp_def[simp del]
-
-lemma halt_least_step: 
-  "\<lbrakk>steps (Suc 0, Bk\<^bsup>l\<^esup>, <lm>) tp stp = (0, Bk\<^bsup>m\<^esup>, Oc\<^bsup>rs \<^esup> @ Bk\<^bsup>n\<^esup>); 
-    turing_basic.t_correct tp; 
-    0<rs\<rbrakk> \<Longrightarrow>
-    \<exists> stp. (nonstop (code tp) (bl2wc (<lm>)) stp = 0 \<and>
-       (\<forall> stp'. nonstop (code tp) (bl2wc (<lm>)) stp' = 0 \<longrightarrow> stp \<le> stp'))"
-proof(induct stp, simp add: steps.simps, simp)
-  fix stp
-  assume ind: 
-    "steps (Suc 0, Bk\<^bsup>l\<^esup>, <lm>) tp stp = (0, Bk\<^bsup>m\<^esup>, Oc\<^bsup>rs\<^esup> @ Bk\<^bsup>n\<^esup>) \<Longrightarrow> 
-    \<exists>stp. nonstop (code tp) (bl2wc (<lm>)) stp = 0 \<and> 
-          (\<forall>stp'. nonstop (code tp) (bl2wc (<lm>)) stp' = 0 \<longrightarrow> stp \<le> stp')"
-  and h: 
-    "steps (Suc 0, Bk\<^bsup>l\<^esup>, <lm>) tp (Suc stp) = (0, Bk\<^bsup>m\<^esup>, Oc\<^bsup>rs\<^esup> @ Bk\<^bsup>n\<^esup>)"
-    "turing_basic.t_correct tp" 
-    "0 < rs"
-  from h show 
-    "\<exists>stp. nonstop (code tp) (bl2wc (<lm>)) stp = 0 
-    \<and> (\<forall>stp'. nonstop (code tp) (bl2wc (<lm>)) stp' = 0 \<longrightarrow> stp \<le> stp')"
-  proof(simp add: tstep_red, 
-      case_tac "steps (Suc 0, Bk\<^bsup>l\<^esup>, <lm>) tp stp", simp, 
-       case_tac a, simp add: tstep_0)
-    assume "steps (Suc 0, Bk\<^bsup>l\<^esup>, <lm>) tp stp = (0, Bk\<^bsup>m\<^esup>, Oc\<^bsup>rs\<^esup> @ Bk\<^bsup>n\<^esup>)"
-    thus "\<exists>stp. nonstop (code tp) (bl2wc (<lm>)) stp = 0 \<and> 
-      (\<forall>stp'. nonstop (code tp) (bl2wc (<lm>)) stp' = 0 \<longrightarrow> stp \<le> stp')"
-      apply(erule_tac ind)
-      done
-  next
-    fix a b c nat
-    assume "steps (Suc 0, Bk\<^bsup>l\<^esup>, <lm>) tp stp = (a, b, c)"
-      "a = Suc nat"
-    thus "\<exists>stp. nonstop (code tp) (bl2wc (<lm>)) stp = 0 \<and> 
-      (\<forall>stp'. nonstop (code tp) (bl2wc (<lm>)) stp' = 0 \<longrightarrow> stp \<le> stp')"
-      using h
-      apply(rule_tac x = "Suc stp" in exI, auto)
-      apply(drule_tac  nonstop_t_eq, simp_all add: nonstop_lemma)
-    proof -
-      fix stp'
-      assume g:"steps (Suc 0, Bk\<^bsup>l\<^esup>, <lm>) tp stp = (Suc nat, b, c)" 
-        "nonstop (code tp) (bl2wc (<lm>)) stp' = 0"
-      thus  "Suc stp \<le> stp'"
-      proof(case_tac "Suc stp \<le> stp'", simp, simp)
-        assume "\<not> Suc stp \<le> stp'"
-        hence "stp' \<le> stp" by simp
-        hence "\<not> isS0 (steps (Suc 0, Bk\<^bsup>l\<^esup>, <lm>) tp stp')"
-          using g
-          apply(case_tac "steps (Suc 0, Bk\<^bsup>l\<^esup>, <lm>) tp stp'",auto,
-            simp add: isS0_def)
-          apply(subgoal_tac "\<exists> n. stp = stp' + n", 
-            auto simp: steps_add steps_0)
-          apply(rule_tac x = "stp - stp'"  in exI, simp)
-          done         
-        hence "nonstop (code tp) (bl2wc (<lm>)) stp' = 1"
-        proof(case_tac "steps (Suc 0, Bk\<^bsup>l\<^esup>, <lm>) tp stp'",
-            simp add: isS0_def nonstop.simps)
-          fix a b c
-          assume k: 
-            "0 < a" "steps (Suc 0, Bk\<^bsup>l\<^esup>, <lm>) tp stp' = (a, b, c)"
-          thus " NSTD (conf (code tp) (bl2wc (<lm>)) stp')"
-            using rec_t_eq_steps[of tp l lm stp'] h
-          proof(simp add: conf_lemma)
-            assume "trpl_code (a, b, c) = conf (code tp) (bl2wc (<lm>)) stp'"
-            moreover have "NSTD (trpl_code (a, b, c))"
-              using k
-              apply(auto simp: trpl_code.simps NSTD.simps)
-              done
-            ultimately show "NSTD (conf (code tp) (bl2wc (<lm>)) stp')" by simp
-          qed
-        qed
-        thus "False" using g by simp
-      qed
-    qed
-  qed
-qed    
-
-lemma conf_trpl_ex: "\<exists> p q r. conf m (bl2wc (<lm>)) stp = trpl p q r"
-apply(induct stp, auto simp: conf.simps inpt.simps trpl.simps 
-  newconf.simps)
-apply(rule_tac x = 0 in exI, rule_tac x = 1 in exI, 
-  rule_tac x = "bl2wc (<lm>)" in exI)
-apply(simp)
-done
-  
-lemma nonstop_rgt_ex: 
-  "nonstop m (bl2wc (<lm>)) stpa = 0 \<Longrightarrow> \<exists> r. conf m (bl2wc (<lm>)) stpa = trpl 0 0 r"
-apply(auto simp: nonstop.simps NSTD.simps split: if_splits)
-using conf_trpl_ex[of m lm stpa]
-apply(auto)
-done
-
-lemma [elim]: "x > Suc 0 \<Longrightarrow> Max {u. x ^ u dvd x ^ r} = r"
-proof(rule_tac Max_eqI)
-  assume "x > Suc 0"
-  thus "finite {u. x ^ u dvd x ^ r}"
-    apply(rule_tac finite_power_dvd, auto)
-    done
-next
-  fix y 
-  assume "Suc 0 < x" "y \<in> {u. x ^ u dvd x ^ r}"
-  thus "y \<le> r"
-    apply(case_tac "y\<le> r", simp)
-    apply(subgoal_tac "\<exists> d. y = r + d")
-    apply(auto simp: power_add)
-    apply(rule_tac x = "y - r" in exI, simp)
-    done
-next
-  show "r \<in> {u. x ^ u dvd x ^ r}" by simp
-qed  
-
-lemma lo_power: "x > Suc 0 \<Longrightarrow> lo (x ^ r) x = r"
-apply(auto simp: lo.simps loR.simps mod_dvd_simp)
-apply(case_tac "x^r", simp_all)
-done
-
-lemma lo_rgt: "lo (trpl 0 0 r) (Pi 2) = r"
-apply(simp add: trpl.simps lo_power)
-done
-
-lemma conf_keep: 
-  "conf m lm stp = trpl 0 0 r  \<Longrightarrow>
-  conf m lm (stp + n) = trpl 0 0 r"
-apply(induct n)
-apply(auto simp: conf.simps  newconf.simps newleft.simps 
-  newrght.simps rght.simps lo_rgt)
-done
-
-lemma halt_state_keep_steps_add:
-  "\<lbrakk>nonstop m (bl2wc (<lm>)) stpa = 0\<rbrakk> \<Longrightarrow> 
-  conf m (bl2wc (<lm>)) stpa = conf m (bl2wc (<lm>)) (stpa + n)"
-apply(drule_tac nonstop_rgt_ex, auto simp: conf_keep)
-done
-
-lemma halt_state_keep: 
-  "\<lbrakk>nonstop m (bl2wc (<lm>)) stpa = 0; nonstop m (bl2wc (<lm>)) stpb = 0\<rbrakk> \<Longrightarrow>
-  conf m (bl2wc (<lm>)) stpa = conf m (bl2wc (<lm>)) stpb"
-apply(case_tac "stpa > stpb")
-using halt_state_keep_steps_add[of m lm stpb "stpa - stpb"] 
-apply simp
-using halt_state_keep_steps_add[of m lm stpa "stpb - stpa"]
-apply(simp)
-done
-
-text {*
-  The correntess of @{text "rec_F"} which relates the interpreter function @{text "rec_F"} with the
-  execution of of TMs.
-  *}
-lemma F_t_halt_eq: 
-  "\<lbrakk>steps (Suc 0, Bk\<^bsup>l\<^esup>, <lm>) tp stp = (0, Bk\<^bsup>m\<^esup>, Oc\<^bsup>rs\<^esup>@Bk\<^bsup>n\<^esup>); 
-    turing_basic.t_correct tp; 
-    0<rs\<rbrakk>
-   \<Longrightarrow> rec_calc_rel 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 -
-  fix stpa
-  assume h: 
-    "nonstop (code tp) (bl2wc (<lm>)) stpa = 0" 
-    "\<forall>stp'. nonstop (code tp) (bl2wc (<lm>)) stp' = 0 \<longrightarrow> stpa \<le> stp'" 
-    "nonstop (code tp) (bl2wc (<lm>)) stp = 0" 
-    "trpl_code (0, Bk\<^bsup>m\<^esup>, Oc\<^bsup>rs\<^esup> @ Bk\<^bsup>n\<^esup>) = conf (code tp) (bl2wc (<lm>)) stp"
-    "steps (Suc 0, Bk\<^bsup>l\<^esup>, <lm>) tp stp = (0, Bk\<^bsup>m\<^esup>, Oc\<^bsup>rs\<^esup> @ Bk\<^bsup>n\<^esup>)"
-  hence g1: "conf (code tp) (bl2wc (<lm>)) stpa = trpl_code (0, Bk\<^bsup>m\<^esup>, Oc\<^bsup>rs\<^esup> @ Bk\<^bsup>n\<^esup>)"
-    using halt_state_keep[of "code tp" lm stpa stp]
-    by(simp)
-  moreover have g2:
-    "rec_calc_rel rec_halt [code tp, (bl2wc (<lm>))] stpa"
-    using h
-    apply(simp add: halt_lemma nonstop_lemma, auto)
-    done
-  show  
-    "rec_calc_rel rec_F [code tp, (bl2wc (<lm>))] (rs - Suc 0)"
-  proof -
-    have 
-      "rec_calc_rel rec_F [code tp, (bl2wc (<lm>))] 
-                         (valu (rght (conf (code tp) (bl2wc (<lm>)) stpa)))"
-      apply(rule F_lemma) using g2 h by auto
-    moreover 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
-    ultimately show "?thesis" by simp
-  qed
-qed
-
-
-end
\ No newline at end of file