diff -r 89ed51d72e4a -r aea02b5a58d2 thys/UTM.thy
--- a/thys/UTM.thy	Thu May 02 12:49:15 2013 +0100
+++ b/thys/UTM.thy	Thu May 02 12:49:33 2013 +0100
@@ -1216,8 +1216,8 @@
 
 declare start_of.simps[simp del]
 
-lemma twice_lemma: "rec_eval rec_twice [rs] = 2*rs"
-by(auto simp: rec_twice_def rec_eval.simps)
+lemma twice_lemma: "rec_exec rec_twice [rs] = 2*rs"
+by(auto simp: rec_twice_def rec_exec.simps)
 
 lemma t_twice_correct: 
   "\<exists>stp ln rn. steps0 (Suc 0, Bk # Bk # ires, Oc\<up>(Suc rs) @ Bk\<up>(n)) 
@@ -1227,13 +1227,13 @@
   fix a b c
   assume h: "rec_ci rec_twice = (a, b, c)"
   have "\<exists>stp m l. steps0 (Suc 0, Bk # Bk # ires, <[rs]> @ Bk\<up>(n)) (tm_of abc_twice @ shift (mopup (length [rs])) 
-    (length (tm_of abc_twice) div 2)) stp = (0, Bk\<up>(m) @ Bk # Bk # ires, Oc\<up>(Suc (rec_eval rec_twice [rs])) @ Bk\<up>(l))"
+    (length (tm_of abc_twice) div 2)) stp = (0, Bk\<up>(m) @ Bk # Bk # ires, Oc\<up>(Suc (rec_exec rec_twice [rs])) @ Bk\<up>(l))"
     thm  recursive_compile_to_tm_correct1
   proof(rule_tac recursive_compile_to_tm_correct1)
     show "rec_ci rec_twice = (a, b, c)" by (simp add: h)
   next
-    show "terminates rec_twice [rs]"
-      apply(rule_tac primerec_terminates, auto)
+    show "terminate rec_twice [rs]"
+      apply(rule_tac primerec_terminate, auto)
       apply(simp add: rec_twice_def, auto simp: constn.simps numeral_2_eq_2)
       by(auto)
   next
@@ -1242,7 +1242,7 @@
       by(simp add: abc_twice_def)
   qed
   thus "?thesis"
-    apply(simp add: tape_of_nl_abv tape_of_nat_list.simps tape_of_nat_abv rec_eval.simps twice_lemma)
+    apply(simp add: tape_of_nl_abv tape_of_nat_list.simps tape_of_nat_abv rec_exec.simps twice_lemma)
     done
 qed
 
@@ -2005,8 +2005,8 @@
 apply(auto simp: rec_fourtimes_def numeral_4_eq_4 constn.simps)
 by auto
 
-lemma fourtimes_lemma: "rec_eval rec_fourtimes [rs] = 4 * rs"
-by(simp add: rec_eval.simps rec_fourtimes_def)
+lemma fourtimes_lemma: "rec_exec rec_fourtimes [rs] = 4 * rs"
+by(simp add: rec_exec.simps rec_fourtimes_def)
 
 
 lemma t_fourtimes_correct: 
@@ -2017,13 +2017,13 @@
   fix a b c
   assume h: "rec_ci rec_fourtimes = (a, b, c)"
   have "\<exists>stp m l. steps0 (Suc 0, Bk # Bk # ires, <[rs]> @ Bk\<up>(n)) (tm_of abc_fourtimes @ shift (mopup (length [rs])) 
-    (length (tm_of abc_fourtimes) div 2)) stp = (0, Bk\<up>(m) @ Bk # Bk # ires, Oc\<up>(Suc (rec_eval rec_fourtimes [rs])) @ Bk\<up>(l))"
+    (length (tm_of abc_fourtimes) div 2)) stp = (0, Bk\<up>(m) @ Bk # Bk # ires, Oc\<up>(Suc (rec_exec rec_fourtimes [rs])) @ Bk\<up>(l))"
     thm recursive_compile_to_tm_correct1
   proof(rule_tac recursive_compile_to_tm_correct1)
     show "rec_ci rec_fourtimes = (a, b, c)" by (simp add: h)
   next
-    show "terminates rec_fourtimes [rs]"
-      apply(rule_tac primerec_terminates)
+    show "terminate rec_fourtimes [rs]"
+      apply(rule_tac primerec_terminate)
       by auto
   next
     show "tm_of abc_fourtimes = tm_of (a [+] dummy_abc (length [rs]))"
@@ -4729,19 +4729,19 @@
 proof -
   obtain ap arity fp where a: "rec_ci rec_F = (ap, arity, fp)"
     by (metis prod_cases3) 
-  moreover have b: "rec_eval rec_F [code tp, (bl2wc (<lm>))] = (rs - Suc 0)"
+  moreover have b: "rec_exec rec_F [code tp, (bl2wc (<lm>))] = (rs - Suc 0)"
     using assms
     apply(rule_tac F_correct, simp_all)
     done 
   have "\<exists> stp m l. steps0 (Suc 0, Bk # Bk # [], <[code tp, bl2wc (<lm>)]> @ Bk\<up>i)
     (F_tprog @ shift (mopup (length [code tp, bl2wc (<lm>)])) (length F_tprog div 2)) stp
-    = (0, Bk\<up>m @ Bk # Bk # [], Oc\<up>Suc (rec_eval rec_F [code tp, (bl2wc (<lm>))]) @ Bk\<up>l)"  
+    = (0, Bk\<up>m @ Bk # Bk # [], Oc\<up>Suc (rec_exec rec_F [code tp, (bl2wc (<lm>))]) @ Bk\<up>l)"  
   proof(rule_tac recursive_compile_to_tm_correct1)
     show "rec_ci rec_F = (ap, arity, fp)" using a by simp
   next
-    show "terminates rec_F [code tp, bl2wc (<lm>)]"
+    show "terminate rec_F [code tp, bl2wc (<lm>)]"
       using assms
-      by(rule_tac terminates_F, simp_all)
+      by(rule_tac terminate_F, simp_all)
   next
     show "F_tprog = tm_of (ap [+] dummy_abc (length [code tp, bl2wc (<lm>)]))"
       using a
@@ -4751,14 +4751,14 @@
   then obtain stp m l where 
     "steps0 (Suc 0, Bk # Bk # [], <[code tp, bl2wc (<lm>)]> @ Bk\<up>i)
     (F_tprog @ shift (mopup (length [code tp, (bl2wc (<lm>))])) (length F_tprog div 2)) stp
-    = (0, Bk\<up>m @ Bk # Bk # [], Oc\<up>Suc (rec_eval rec_F [code tp, (bl2wc (<lm>))]) @ Bk\<up>l)" by blast
+    = (0, Bk\<up>m @ Bk # Bk # [], Oc\<up>Suc (rec_exec rec_F [code tp, (bl2wc (<lm>))]) @ Bk\<up>l)" by blast
   hence "\<exists> m. steps0 (Suc 0, [Bk], <[code tp, bl2wc (<lm>)]> @ Bk\<up>i)
     (F_tprog @ shift (mopup 2) (length F_tprog div 2)) stp
     = (0, Bk\<up>m, Oc\<up>Suc (rs - 1) @ Bk\<up>l)"
   proof -
     assume g: "steps0 (Suc 0, [Bk, Bk], <[code tp, bl2wc (<lm>)]> @ Bk \<up> i)
       (F_tprog @ shift (mopup (length [code tp, bl2wc (<lm>)])) (length F_tprog div 2)) stp =
-      (0, Bk \<up> m @ [Bk, Bk], Oc \<up> Suc ((rec_eval rec_F [code tp, bl2wc (<lm>)])) @ Bk \<up> l)"
+      (0, Bk \<up> m @ [Bk, Bk], Oc \<up> Suc ((rec_exec rec_F [code tp, bl2wc (<lm>)])) @ Bk \<up> l)"
    moreover have "tinres [Bk, Bk] [Bk]"
      apply(auto simp: tinres_def)
      done
@@ -4936,7 +4936,7 @@
 done
 
 lemma NSTD_1: "\<not> TSTD (a, b, c)
-    \<Longrightarrow> rec_eval rec_NSTD [trpl_code (a, b, c)] = Suc 0"
+    \<Longrightarrow> rec_exec rec_NSTD [trpl_code (a, b, c)] = Suc 0"
   using NSTD_lemma1[of "trpl_code (a, b, c)"]
        NSTD_lemma2[of "trpl_code (a, b, c)"]
   apply(simp add: TSTD_def)
@@ -4949,10 +4949,10 @@
   "\<lbrakk>tm_wf (tp, 0);
   steps0 (Suc 0, Bk\<up>(l), <lm>) tp stp = (a, b, c);
   \<not> TSTD (a, b, c)\<rbrakk>
-  \<Longrightarrow> rec_eval rec_nonstop [code tp, bl2wc (<lm>), stp] = Suc 0"
-apply(simp add: rec_nonstop_def rec_eval.simps)
+  \<Longrightarrow> rec_exec rec_nonstop [code tp, bl2wc (<lm>), stp] = Suc 0"
+apply(simp add: rec_nonstop_def rec_exec.simps)
 apply(subgoal_tac 
-  "rec_eval rec_conf [code tp, bl2wc (<lm>), stp] =
+  "rec_exec rec_conf [code tp, bl2wc (<lm>), stp] =
   trpl_code (a, b, c)", simp)
 apply(erule_tac NSTD_1)
 using rec_t_eq_steps[of tp l lm stp]
@@ -4962,7 +4962,7 @@
 lemma nonstop_true:
   "\<lbrakk>tm_wf (tp, 0);
   \<forall> stp. (\<not> TSTD (steps0 (Suc 0, Bk\<up>(l), <lm>) tp stp))\<rbrakk>
-  \<Longrightarrow> \<forall>y. rec_eval rec_nonstop ([code tp, bl2wc (<lm>), y]) =  (Suc 0)"
+  \<Longrightarrow> \<forall>y. rec_exec rec_nonstop ([code tp, bl2wc (<lm>), y]) =  (Suc 0)"
 apply(rule_tac allI, erule_tac x = y in allE)
 apply(case_tac "steps0 (Suc 0, Bk\<up>(l), <lm>) tp y", simp)
 apply(rule_tac nonstop_t_uhalt_eq, simp_all)
@@ -5021,11 +5021,11 @@
           using e f
         proof(rule_tac mn_unhalt_case, auto simp: rec_halt_def)
           fix i
-          show "terminates rec_nonstop [code tp, bl2wc (<lm>), i]"
-            by(rule_tac primerec_terminates, auto)
+          show "terminate rec_nonstop [code tp, bl2wc (<lm>), i]"
+            by(rule_tac primerec_terminate, auto)
         next
           fix i
-          show "0 < rec_eval rec_nonstop [code tp, bl2wc (<lm>), i]"
+          show "0 < rec_exec rec_nonstop [code tp, bl2wc (<lm>), i]"
             using assms
             by(drule_tac nonstop_true, auto)
         qed
@@ -5035,22 +5035,22 @@
         assume "j<2" "rec_ci ([recf.id (Suc (Suc 0)) 0, recf.id (Suc (Suc 0)) (Suc 0), Mn (Suc (Suc 0)) rec_nonstop] ! j) = (apj, arj, ftj)"
         hence "{\<lambda>nl. nl = [code tp, bl2wc (<lm>)] @ 0 \<up> (ftj - arj) @ anything} apj
           {\<lambda>nl. nl = [code tp, bl2wc (<lm>)] @
-            rec_eval ([recf.id (Suc (Suc 0)) 0, recf.id (Suc (Suc 0)) (Suc 0), Mn (Suc (Suc 0)) rec_nonstop] ! j) [code tp, bl2wc (<lm>)] # 
+            rec_exec ([recf.id (Suc (Suc 0)) 0, recf.id (Suc (Suc 0)) (Suc 0), Mn (Suc (Suc 0)) rec_nonstop] ! j) [code tp, bl2wc (<lm>)] # 
                0 \<up> (ftj - Suc arj) @ anything}"
           apply(rule_tac recursive_compile_correct)
           apply(case_tac j, auto)
-          apply(rule_tac [!] primerec_terminates)
+          apply(rule_tac [!] primerec_terminate)
           by(auto)
         thus "{\<lambda>nl. nl = code tp # bl2wc (<lm>) # 0 \<up> (ftj - arj) @ anything} apj
-          {\<lambda>nl. nl = code tp # bl2wc (<lm>) # rec_eval ([recf.id (Suc (Suc 0)) 0, recf.id (Suc (Suc 0))
+          {\<lambda>nl. nl = code tp # bl2wc (<lm>) # rec_exec ([recf.id (Suc (Suc 0)) 0, recf.id (Suc (Suc 0))
           (Suc 0), Mn (Suc (Suc 0)) rec_nonstop] ! j) [code tp, bl2wc (<lm>)] # 0 \<up> (ftj - Suc arj) @ anything}"
           by simp
       next
         fix j
         assume "(j::nat) < 2"
-        thus "terminates ([recf.id (Suc (Suc 0)) 0, recf.id (Suc (Suc 0)) (Suc 0), Mn (Suc (Suc 0)) rec_nonstop] ! j)
+        thus "terminate ([recf.id (Suc (Suc 0)) 0, recf.id (Suc (Suc 0)) (Suc 0), Mn (Suc (Suc 0)) rec_nonstop] ! j)
           [code tp, bl2wc (<lm>)]"
-          by(case_tac j, auto intro!: primerec_terminates)
+          by(case_tac j, auto intro!: primerec_terminate)
       qed
       thus "{\<lambda>nl. nl = code tp # bl2wc (<lm>) # 0 \<up> (ft2 - Suc (Suc 0)) @ anything} ap2 \<up>"
         by simp