--- a/Paper.thy	Sat Jan 12 01:05:01 2013 +0000
+++ b/Paper.thy	Sat Jan 12 01:33:20 2013 +0000
@@ -71,6 +71,14 @@
 apply(auto simp add: tshift.simps)
 done
 
+lemma change_termi_state_def2:
+ "change_termi_state p  == 
+  (map (\<lambda> (a, s). (a, if s = 0 then Suc ((length s) div 2)) else s) t)"
+apply(rule eq_reflection)
+apply(auto simp add: change_termi_state.simps)
+done
+
+
 
 consts DUMMY::'a
 
@@ -85,7 +93,7 @@
   abc_lm_v ("lookup") and
   abc_lm_s ("set") and
   haltP ("stdhalt") and 
-  change-termi-state ("adjust") and
+  change_termi_state ("adjust") and
   tape_of_nat_list ("\<ulcorner>_\<urcorner>") and 
   DUMMY  ("\<^raw:\mbox{$\_$}>")
 

--- a/UTM.thy	Sat Jan 12 01:05:01 2013 +0000
+++ b/UTM.thy	Sat Jan 12 01:33:20 2013 +0000
@@ -1148,12 +1148,12 @@
 qed
     
 lemma [elim]: "t_ncorrect tp
-    \<Longrightarrow> t_ncorrect (abacus.tshift tp a)"
+    \<Longrightarrow> t_ncorrect (tshift tp a)"
 apply(simp add: t_ncorrect.simps shift_length)
 done
 
 lemma tshift_fetch: "\<lbrakk> fetch tp a b = (aa, st'); 0 < st'\<rbrakk>
-       \<Longrightarrow> fetch (abacus.tshift tp (length tp1 div 2)) a b 
+       \<Longrightarrow> fetch (tshift tp (length tp1 div 2)) a b 
           = (aa, st' + length tp1 div 2)"
 apply(subgoal_tac "a > 0")
 apply(auto simp: fetch.simps nth_of.simps shift_length nth_map
@@ -1176,22 +1176,22 @@
   assume ind: "\<And>st' l' r'.
     \<lbrakk>a = st' \<and> b = l' \<and> c = r'; 0 < st'\<rbrakk>
     \<Longrightarrow> t_steps (st + length tp1 div 2, l, r) 
-    (abacus.tshift tp (length tp1 div 2), length tp1 div 2) stp = 
+    (tshift tp (length tp1 div 2), length tp1 div 2) stp = 
      (st' + length tp1 div 2, l', r')"
   and h: "tstep (a, b, c) tp = (st', l', r')" "0 < st'" "t_ncorrect tp1"  "t_ncorrect tp"
-  have k: "t_steps (st + length tp1 div 2, l, r) (abacus.tshift tp (length tp1 div 2),
+  have k: "t_steps (st + length tp1 div 2, l, r) (tshift tp (length tp1 div 2),
          length tp1 div 2) stp = (a + length tp1 div 2, b, c)"
     apply(rule_tac ind, simp)
     using h
     apply(case_tac a, simp_all add: tstep.simps fetch.simps)
     done
-  from h and this show "t_step (t_steps (st + length tp1 div 2, l, r) (abacus.tshift tp (length tp1 div 2), length tp1 div 2) stp)
-           (abacus.tshift tp (length tp1 div 2), length tp1 div 2) =
+  from h and this show "t_step (t_steps (st + length tp1 div 2, l, r) (tshift tp (length tp1 div 2), length tp1 div 2) stp)
+           (tshift tp (length tp1 div 2), length tp1 div 2) =
           (st' + length tp1 div 2, l', r')"
     apply(simp add: k)
     apply(simp add: tstep.simps t_step.simps)
     apply(case_tac "fetch tp a (case c of [] \<Rightarrow> Bk | x # xs \<Rightarrow> x)", simp)
-    apply(subgoal_tac "fetch (abacus.tshift tp (length tp1 div 2)) a
+    apply(subgoal_tac "fetch (tshift tp (length tp1 div 2)) a
                        (case c of [] \<Rightarrow> Bk | x # xs \<Rightarrow> x) = (aa, st' + length tp1 div 2)", simp)
     apply(simp add: tshift_fetch)
     done
@@ -1215,7 +1215,7 @@
     "t_ncorrect tp"
     "t_ncorrect tp2"
   from h have 
-    "\<exists>stp>0. t_steps (st + length tp1 div 2, l, r) (tp1 @ abacus.tshift tp (length tp1 div 2) @ tp2, 0) stp = 
+    "\<exists>stp>0. t_steps (st + length tp1 div 2, l, r) (tp1 @ tshift tp (length tp1 div 2) @ tp2, 0) stp = 
                             (st' + length tp1 div 2, l', r')"
     apply(rule_tac stp = stp in turing_shift, simp_all add: shift_length)
     apply(simp add: t_steps_steps_eq)
@@ -1225,7 +1225,7 @@
                   = (st' + length tp1 div 2, l', r')"
     apply(erule_tac exE)
     apply(rule_tac x = stp in exI, simp)
-    apply(subgoal_tac "length (tp1 @ abacus.tshift tp (length tp1 div 2) @ tp2) mod 2 = 0")
+    apply(subgoal_tac "length (tp1 @ tshift tp (length tp1 div 2) @ tp2) mod 2 = 0")
     apply(simp only: steps_eq)
     using h
     apply(auto simp: t_ncorrect.simps shift_length)
@@ -1407,7 +1407,7 @@
     done
 next
   show "t_ncorrect ((L, Suc 0) # (L, Suc 0) #
-       abacus.tshift t_fourtimes (t_twice_len + 13) @ [(L, Suc 0), (L, Suc 0)])"
+       tshift t_fourtimes (t_twice_len + 13) @ [(L, Suc 0), (L, Suc 0)])"
     using length_tm_even[of abc_fourtimes]
     apply(simp add: t_ncorrect.simps shift_length t_fourtimes_def)
     apply arith
@@ -2081,7 +2081,7 @@
     done
 next
   show "t_ncorrect (t_wcode_main_first_part @ 
-    abacus.tshift t_twice (length t_wcode_main_first_part div 2) @ 
+    tshift t_twice (length t_wcode_main_first_part div 2) @ 
     [(L, Suc 0), (L, Suc 0)])"
     apply(simp add: t_ncorrect.simps t_wcode_main_first_part_def shift_length
                     t_twice_def)
@@ -2107,13 +2107,13 @@
 apply(simp add: t_twice_def)
 done
 
-lemma [simp]: "((26 + length (abacus.tshift t_twice 12)) div 2)
-             = (length (abacus.tshift t_twice 12) div 2 + 13)"
+lemma [simp]: "((26 + length (tshift t_twice 12)) div 2)
+             = (length (tshift t_twice 12) div 2 + 13)"
 using tm_even[of abc_twice]
 apply(simp add: t_twice_def)
 done 
 
-lemma [simp]: "t_twice_len + 14 =  14 + length (abacus.tshift t_twice 12) div 2"
+lemma [simp]: "t_twice_len + 14 =  14 + length (tshift t_twice 12) div 2"
 using tm_even[of abc_twice]
 apply(simp add: t_twice_def t_twice_len_def shift_length)
 done
@@ -3351,13 +3351,13 @@
     done
   hence "list_all (\<lambda>(acn, s). s \<le>  Suc (length (tm_of abc_twice @ tMp (Suc 0)
     (start_of twice_ly (length abc_twice) - Suc 0)) div 2) + 12)
-     (abacus.tshift (change_termi_state (tm_of abc_twice @ tMp (Suc 0) 
+     (tshift (change_termi_state (tm_of abc_twice @ tMp (Suc 0) 
            (start_of twice_ly (length abc_twice) - Suc 0))) 12)"
     apply(rule_tac t_correct_shift, simp)
     done
   thus  "list_all (\<lambda>(acn, s). s \<le> 
            (60 + (length (tm_of abc_twice) + length (tm_of abc_fourtimes))) div 2)
-     (abacus.tshift (change_termi_state (tm_of abc_twice @ tMp (Suc 0)
+     (tshift (change_termi_state (tm_of abc_twice @ tMp (Suc 0)
                  (start_of twice_ly (length abc_twice) - Suc 0))) 12)"
     apply(simp)
     apply(simp add: list_all_length, auto)
@@ -3371,12 +3371,12 @@
     done
   hence "list_all (\<lambda>(acn, s). s \<le> Suc (length (tm_of abc_fourtimes @ tMp (Suc 0) 
     (start_of fourtimes_ly (length abc_fourtimes) - Suc 0)) div 2) + (t_twice_len + 13))
-    (abacus.tshift (change_termi_state (tm_of abc_fourtimes @ tMp (Suc 0) 
+    (tshift (change_termi_state (tm_of abc_fourtimes @ tMp (Suc 0) 
     (start_of fourtimes_ly (length abc_fourtimes) - Suc 0))) (t_twice_len + 13))"
     apply(rule_tac t_correct_shift, simp)
     done
   thus "list_all (\<lambda>(acn, s). s \<le> (60 + (length (tm_of abc_twice) + length (tm_of abc_fourtimes))) div 2)
-    (abacus.tshift (change_termi_state (tm_of abc_fourtimes @ tMp (Suc 0)
+    (tshift (change_termi_state (tm_of abc_fourtimes @ tMp (Suc 0)
     (start_of fourtimes_ly (length abc_fourtimes) - Suc 0))) (t_twice_len + 13))"
     apply(simp add: t_twice_len_def t_twice_def)
     using twice_len_even fourtimes_len_even

--- a/abacus.thy	Sat Jan 12 01:05:01 2013 +0000
+++ b/abacus.thy	Sat Jan 12 01:33:20 2013 +0000
@@ -6318,7 +6318,7 @@
     apply(rule_tac mopup_halt_bef, auto)
     done
   from h1 and h2 and h3 show 
-    "\<exists>stp. case t_steps tc (tm_of aprog @ abacus.tshift (mop_bef n @ abacus.tshift mp_up (2 * n))
+    "\<exists>stp. case t_steps tc (tm_of aprog @ tshift (mop_bef n @ tshift mp_up (2 * n))
     (start_of (layout_of aprog) (length aprog) - Suc 0), 0) stp of (s, ab)
     \<Rightarrow> s = 0 \<and> mopup_inv (0, ab) am n ires"
   proof(erule_tac exE, 

--- a/recursive.thy	Sat Jan 12 01:05:01 2013 +0000
+++ b/recursive.thy	Sat Jan 12 01:33:20 2013 +0000
@@ -4782,7 +4782,7 @@
 done
 
 lemma [elim]: "\<lbrakk>k < length ap; ap ! k = Inc n; 
-       (a, b) \<in> set (abacus.tshift (abacus.tshift tinc_b (2 * n)) 
+       (a, b) \<in> set (tshift (tshift tinc_b (2 * n)) 
                             (start_of (layout_of ap) k - Suc 0))\<rbrakk>
        \<Longrightarrow> b \<le> start_of (layout_of ap) (length ap)"
 apply(subgoal_tac "b \<le> start_of (layout_of ap) (Suc k)")
@@ -4794,7 +4794,7 @@
   layout_of.simps length_of.simps startof_not0)
 done
 
-lemma findnth_le[elim]: "(a, b) \<in> set (abacus.tshift (findnth n) (start_of (layout_of ap) k - Suc 0))
+lemma findnth_le[elim]: "(a, b) \<in> set (tshift (findnth n) (start_of (layout_of ap) k - Suc 0))
         \<Longrightarrow> b \<le> Suc (start_of (layout_of ap) k + 2 * n)"
 apply(induct n, simp add: findnth.simps tshift.simps)
 apply(simp add: findnth.simps tshift_append, auto)
@@ -4803,7 +4803,7 @@
 
 
 lemma  [elim]: "\<lbrakk>k < length ap; ap ! k = Inc n; (a, b) \<in> 
-  set (abacus.tshift (findnth n) (start_of (layout_of ap) k - Suc 0))\<rbrakk> 
+  set (tshift (findnth n) (start_of (layout_of ap) k - Suc 0))\<rbrakk> 
   \<Longrightarrow> b \<le> start_of (layout_of ap) (length ap)"
 apply(subgoal_tac "b \<le> start_of (layout_of ap) (Suc k)")
 apply(subgoal_tac "start_of (layout_of ap) (Suc k) \<le> start_of (layout_of ap) (length ap) ")
@@ -4831,7 +4831,7 @@
 
 lemma [elim]: "\<lbrakk>k < length ap; 
         ap ! k = Dec n e;
-         (a, b) \<in> set (abacus.tshift (findnth n) (start_of (layout_of ap) k - Suc 0))\<rbrakk>
+         (a, b) \<in> set (tshift (findnth n) (start_of (layout_of ap) k - Suc 0))\<rbrakk>
        \<Longrightarrow> b \<le> start_of (layout_of ap) (length ap)"
 apply(subgoal_tac "b \<le> start_of (layout_of ap) k + 2*n + 1 \<and> 
      start_of (layout_of ap) k + 2*n + 1 \<le>  start_of (layout_of ap) (Suc k) \<and>
@@ -4842,7 +4842,7 @@
 done
 
 thm length_of.simps
-lemma [elim]: "\<lbrakk>k < length ap; ap ! k = Dec n e; (a, b) \<in> set (abacus.tshift (abacus.tshift tdec_b (2 * n))
+lemma [elim]: "\<lbrakk>k < length ap; ap ! k = Dec n e; (a, b) \<in> set (tshift (tshift tdec_b (2 * n))
                   (start_of (layout_of ap) k - Suc 0))\<rbrakk>
        \<Longrightarrow> b \<le> start_of (layout_of ap) (length ap)"
 apply(subgoal_tac "2*n + start_of (layout_of ap) k + 16 \<le> start_of (layout_of ap) (length ap) \<and> start_of (layout_of ap) k > 0")