diff -r e9ef4ada308b -r d8e6f0798e23 thys/UF.thy
--- a/thys/UF.thy	Thu Mar 14 20:43:43 2013 +0000
+++ b/thys/UF.thy	Wed Mar 27 09:47:02 2013 +0000
@@ -158,60 +158,6 @@
   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]
 
@@ -280,7 +226,6 @@
                                                        else 1)"
 by(induct_tac y, auto simp: rec_exec.simps sg_lemma rec_conj_def mult_lemma)
 
-
 text {*
   Correctness of @{text "rec_disj"}.
   *}
@@ -2948,190 +2893,6 @@
   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)
-        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]
 
@@ -3141,11 +2902,6 @@
     @{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
@@ -3283,12 +3039,6 @@
 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}, 
@@ -3303,38 +3053,61 @@
     @{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
+lemma primerec_terminate: 
+  "\<lbrakk>primerec f x; length xs = x\<rbrakk> \<Longrightarrow> terminate f xs"
+proof(induct arbitrary: xs rule: primerec.induct)
+  fix xs
+  assume "length (xs::nat list) = Suc 0"  thus "terminate z xs"
+    by(case_tac xs, auto intro: termi_z)
+next
+  fix xs
+  assume "length (xs::nat list) = Suc 0" thus "terminate s xs"
+    by(case_tac xs, auto intro: termi_s)
+next
+  fix n m xs
+  assume "n < m" "length (xs::nat list) = m"  thus "terminate (id m n) xs"
+    by(erule_tac termi_id, simp)
+next
+  fix f k gs m n xs
+  assume ind: "\<forall>i<length gs. primerec (gs ! i) m \<and> (\<forall>x. length x = m \<longrightarrow> terminate (gs ! i) x)"
+  and ind2: "\<And> xs. length xs = k \<Longrightarrow> terminate f xs"
+  and h: "primerec f k"  "length gs = k" "m = n" "length (xs::nat list) = m"
+  have "terminate f (map (\<lambda>g. rec_exec g xs) gs)"
+    using ind2[of "(map (\<lambda>g. rec_exec g xs) gs)"] h
+    by simp
+  moreover have "\<forall>g\<in>set gs. terminate g xs"
+    using ind h
+    by(auto simp: set_conv_nth)
+  ultimately show "terminate (Cn n f gs) xs"
+    using h
+    by(rule_tac termi_cn, auto)
+next
+  fix f n g m xs
+  assume ind1: "\<And>xs. length xs = n \<Longrightarrow> terminate f xs"
+  and ind2: "\<And>xs. length xs = Suc (Suc n) \<Longrightarrow> terminate g xs"
+  and h: "primerec f n" " primerec g (Suc (Suc n))" " m = Suc n" "length (xs::nat list) = m"
+  have "\<forall>y<last xs. terminate g (butlast xs @ [y, rec_exec (Pr n f g) (butlast xs @ [y])])"
+    using h
+    apply(auto) 
+    by(rule_tac ind2, simp)
+  moreover have "terminate f (butlast xs)"
+    using ind1[of "butlast xs"] h
+    by simp
+ moreover have "length (butlast xs) = n"
+   using h by simp
+ ultimately have "terminate (Pr n f g) (butlast xs @ [last xs])"
+   by(rule_tac termi_pr, simp_all)
+ thus "terminate (Pr n f g) xs"
+   using h
+   by(case_tac "xs = []", auto)
+qed
 
 text {*
   The following lemma gives the correctness of @{text "rec_halt"}.
   It says: if @{text "rec_halt"} calculates that the TM coded by @{text "m"}
   will reach a standard final configuration after @{text "t"} steps of execution, 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 {*
@@ -3370,11 +3143,6 @@
   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 {*
@@ -3393,77 +3161,42 @@
 done
 
 lemma [simp]: 
-  "\<lbrakk>ys \<noteq> [];  k < length ys\<rbrakk> \<Longrightarrow>
+  "\<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)
+lemma terminate_halt_lemma: 
+  "\<lbrakk>rec_exec rec_nonstop ([m, r] @ [t]) = 0; 
+     \<forall>i<t. 0 < rec_exec rec_nonstop ([m, r] @ [i])\<rbrakk> \<Longrightarrow> terminate rec_halt [m, r]"
+apply(simp add: rec_halt_def)
+apply(rule_tac termi_mn, auto)
+apply(rule_tac [!] primerec_terminate, 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)))"
+
+lemma F_lemma: "rec_exec rec_halt [m, r] = t \<Longrightarrow> rec_exec rec_F [m, r] = (valu (rght (conf m r t)))"
+by(simp add: rec_F_def rec_exec.simps value_lemma right_lemma conf_lemma halt_lemma)
+
+lemma terminate_F_lemma: "terminate rec_halt [m, r] \<Longrightarrow> terminate rec_F [m, r]"
 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)
+apply(rule_tac termi_cn, auto)
+apply(rule_tac primerec_terminate, auto)
+apply(rule_tac termi_cn, auto)
+apply(rule_tac primerec_terminate, auto)
+apply(rule_tac termi_cn, auto)
+apply(rule_tac primerec_terminate, auto)
+apply(rule_tac [!] termi_id, auto)
 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 *}
 
@@ -4860,10 +4593,26 @@
   execution of of TMs.
   *}
 
+lemma terminate_halt: 
+  "\<lbrakk>steps0 (Suc 0, Bk\<up>l, <lm>) tp stp = (0, Bk\<up>m, Oc\<up>rs@Bk\<up>n); 
+    tm_wf (tp,0); 0<rs\<rbrakk> \<Longrightarrow> terminate rec_halt [code tp, (bl2wc (<lm>))]"
+apply(frule_tac halt_least_step, auto)
+thm terminate_halt_lemma
+apply(rule_tac t = stpa in terminate_halt_lemma)
+apply(simp_all add: nonstop_lemma, auto)
+done
+
+lemma terminate_F: 
+  "\<lbrakk>steps0 (Suc 0, Bk\<up>l, <lm>) tp stp = (0, Bk\<up>m, Oc\<up>rs@Bk\<up>n); 
+    tm_wf (tp,0); 0<rs\<rbrakk> \<Longrightarrow> terminate rec_F [code tp, (bl2wc (<lm>))]"
+apply(drule_tac terminate_halt, simp_all)
+apply(erule_tac terminate_F_lemma)
+done
+
 lemma F_correct: 
   "\<lbrakk>steps0 (Suc 0, Bk\<up>l, <lm>) tp stp = (0, Bk\<up>m, Oc\<up>rs@Bk\<up>n); 
     tm_wf (tp,0); 0<rs\<rbrakk>
-   \<Longrightarrow> rec_calc_rel rec_F [code tp, (bl2wc (<lm>))] (rs - Suc 0)"
+   \<Longrightarrow> rec_exec rec_F [code tp, (bl2wc (<lm>))] = (rs - Suc 0)"
 apply(frule_tac halt_least_step, auto)
 apply(frule_tac  nonstop_t_eq, auto simp: nonstop_lemma)
 using rec_t_eq_steps[of tp l lm stp]
@@ -4880,24 +4629,20 @@
     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"
+    "rec_exec rec_halt [code tp, (bl2wc (<lm>))] = stpa"
     using h
-    apply(simp add: halt_lemma nonstop_lemma, auto)
-    done
+    by(auto simp: rec_exec.simps rec_halt_def nonstop_lemma intro!: Least_equality)
   show  
-    "rec_calc_rel rec_F [code tp, (bl2wc (<lm>))] (rs - Suc 0)"
+    "rec_exec 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
+    thus "?thesis" 
+      by(simp add: rec_exec.simps F_lemma g2)
   qed
 qed