# HG changeset patch
# User Christian Urban <christian dot urban at kcl dot ac dot uk>
# Date 1361424879 0
# Node ID f1ecb4a68a5400046b6d21bc37137751c2d43736
# Parent  5974111de158ce69fde8ad48952459d15d9f9348
renamed sete definition to adjust and old special case of adjust to adjust0

diff -r 5974111de158 -r f1ecb4a68a54 Paper/Paper.thy
--- a/Paper/Paper.thy	Thu Feb 21 05:33:57 2013 +0000
+++ b/Paper/Paper.thy	Thu Feb 21 05:34:39 2013 +0000
@@ -65,6 +65,7 @@
   tcontra ("contra") and
   code_tcontra ("code contra") and
   steps0 ("steps") and
+  adjust0 ("adjust") and
   exponent ("_\<^bsup>_\<^esup>") and
   tcopy ("copy") and 
   tape_of ("\<langle>_\<rangle>") and 
@@ -163,6 +164,11 @@
   and   "layout_of ((Goto l)#is) = 1#(layout_of is)"
 by(auto simp add: layout_of.simps length_of.simps)
 
+
+lemma adjust_simps:
+  shows "adjust0 p = map (\<lambda>(a, s). (a, if s = 0 then (Suc (length p div 2)) else s)) p"
+by(simp add: adjust.simps)
+
 fun clear :: "nat \<Rightarrow> nat \<Rightarrow> abc_prog"
   where
   "clear n e = [Dec n e, Goto 0]"
@@ -552,7 +558,7 @@
   \begin{center}
   \begin{tabular}{@ {}l@ {\hspace{1mm}}c@ {\hspace{1mm}}l@ {}}
   @{thm (lhs) shift.simps} @{text "\<equiv>"} @{thm (rhs) shift.simps}\\
-  @{thm (lhs) adjust.simps} @{text "\<equiv>"} @{thm (rhs) adjust.simps}\\
+  @{thm (lhs) adjust_simps} @{text "\<equiv>"} @{thm (rhs) adjust_simps}\\
   \end{tabular}
   \end{center}
 
diff -r 5974111de158 -r f1ecb4a68a54 paper.pdf
Binary file paper.pdf has changed
diff -r 5974111de158 -r f1ecb4a68a54 thys/Abacus.thy
--- a/thys/Abacus.thy	Thu Feb 21 05:33:57 2013 +0000
+++ b/thys/Abacus.thy	Thu Feb 21 05:34:39 2013 +0000
@@ -147,14 +147,6 @@
               (R, 17), (W0, 13), (L, 15), (L, 14), (R, 16), (L, 14),
               (R, 0), (W0, 16)]"
 
-text {*
-  @{text "sete tp e"} attaches the termination edges (edges leading to state @{text "0"}) 
-  of TM @{text "tp"} to the intruction labelled by @{text "e"}.
-  *}
-
-fun sete :: "instr list \<Rightarrow> nat \<Rightarrow> instr list"
-  where
-  "sete tp e = map (\<lambda> (action, state). (action, if state = 0 then e else state)) tp"
 
 text {*
   @{text "tdec ss n label"} returns the TM which simulates the execution of 
@@ -165,7 +157,7 @@
 
 fun tdec :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> instr list"
   where
-  "tdec ss n e = shift (findnth n) (ss - 1) @ sete (shift (shift tdec_b (2 * n)) (ss - 1)) e"
+  "tdec ss n e = shift (findnth n) (ss - 1) @ adjust (shift (shift tdec_b (2 * n)) (ss - 1)) e"
  
 text {*
   @{text "tgoto f(label)"} returns the TM simulating the execution of Abacus instruction
@@ -255,7 +247,8 @@
 
 lemma ci_length : "length (ci ns n ai) div 2 = length_of ai"
 apply(auto simp: ci.simps tinc_b_def tdec_b_def length_findnth
-                 split: abc_inst.splits)
+                 split: abc_inst.splits simp del: adjust.simps)
+
 done
 
 subsection {* Representation of Abacus memory by TM tapes *}
@@ -2118,7 +2111,7 @@
 qed
     
 subsection{* Crsp of Dec n e*}
-declare sete.simps[simp del]
+declare adjust.simps[simp del]
 
 type_synonym dec_inv_t = "(nat * nat list) \<Rightarrow> config \<Rightarrow> cell list \<Rightarrow>  bool"
 
@@ -2223,13 +2216,13 @@
 lemma [simp]:
   "fetch (ci ly (start_of ly as) (Dec n e)) (Suc (2 * n)) Bk = (W1,  start_of ly as + 2 *n)"
 apply(auto simp: fetch.simps length_ci_dec)
-apply(auto simp: ci.simps nth_append length_findnth sete.simps shift.simps tdec_b_def)
+apply(auto simp: ci.simps nth_append length_findnth adjust.simps shift.simps tdec_b_def)
 using startof_not0[of ly as] by simp
 
 lemma [simp]:
   "fetch (ci ly (start_of ly as) (Dec n e)) (Suc (2 * n)) Oc = (R,  Suc (start_of ly as) + 2 *n)"
 apply(auto simp: fetch.simps length_ci_dec)
-apply(auto simp: ci.simps nth_append length_findnth sete.simps shift.simps tdec_b_def)
+apply(auto simp: ci.simps nth_append length_findnth adjust.simps shift.simps tdec_b_def)
 done
 
 lemma [simp]: 
@@ -2379,7 +2372,7 @@
 lemma [simp]:"fetch (ci (ly) (start_of ly as) (Dec n e)) (Suc (2 * n))  Oc
   = (R, start_of ly as + 2*n + 1)"
 apply(auto simp: ci.simps findnth.simps fetch.simps
-                  nth_of.simps shift.simps nth_append tdec_b_def length_findnth sete.simps)
+                  nth_of.simps shift.simps nth_append tdec_b_def length_findnth adjust.simps)
 done
 
 lemma [simp]: "(start_of ly as = 0) = False"
@@ -2390,7 +2383,7 @@
   (start_of ly as) (Dec n e)) (Suc (2 * n))  Bk
   = (W1, start_of ly as + 2*n)"
 apply(auto simp: ci.simps findnth.simps fetch.simps
-                  nth_of.simps shift.simps nth_append tdec_b_def length_findnth sete.simps)
+                  nth_of.simps shift.simps nth_append tdec_b_def length_findnth adjust.simps)
 done
 
 lemma [simp]: 
@@ -2398,7 +2391,7 @@
                 (start_of ly as) (Dec n e)) (Suc (Suc (2 * n)))  Oc
       = (R, start_of ly as + 2*n + 2)"
 apply(auto simp: ci.simps findnth.simps fetch.simps
-                  nth_of.simps shift.simps nth_append tdec_b_def length_findnth sete.simps)
+                  nth_of.simps shift.simps nth_append tdec_b_def length_findnth adjust.simps)
 done
 
 
@@ -2406,7 +2399,7 @@
                   (start_of ly as) (Dec n e)) (Suc (Suc (2 * n))) Bk
       = (L, start_of ly as + 2*n + 13)"
 apply(auto simp: ci.simps findnth.simps fetch.simps
-                  nth_of.simps shift.simps nth_append tdec_b_def length_findnth sete.simps)
+                  nth_of.simps shift.simps nth_append tdec_b_def length_findnth adjust.simps)
 done
 
 
@@ -2414,7 +2407,7 @@
              (start_of ly as) (Dec n e)) (Suc (Suc (Suc (2 * n))))  Oc
      = (R, start_of ly as + 2*n + 2)"
 apply(auto simp: ci.simps findnth.simps fetch.simps
-                  nth_of.simps shift.simps nth_append tdec_b_def length_findnth sete.simps)
+                  nth_of.simps shift.simps nth_append tdec_b_def length_findnth adjust.simps)
 done
 
 
@@ -2422,7 +2415,7 @@
                              (Suc (Suc (Suc (2 * n))))  Bk
      = (L, start_of ly as + 2*n + 3)"
 apply(auto simp: ci.simps findnth.simps fetch.simps
-                  nth_of.simps shift.simps nth_append tdec_b_def length_findnth sete.simps)
+                  nth_of.simps shift.simps nth_append tdec_b_def length_findnth adjust.simps)
 done
 
 lemma [simp]:
@@ -2431,7 +2424,7 @@
     = (W0, start_of ly as + 2*n + 3)"
 apply(subgoal_tac "2*n + 4 = Suc (2*n + 3)", simp only: fetch.simps)
 apply(auto simp: ci.simps findnth.simps fetch.simps
-                  nth_of.simps shift.simps nth_append tdec_b_def length_findnth sete.simps)
+                  nth_of.simps shift.simps nth_append tdec_b_def length_findnth adjust.simps)
 done
 
 lemma [simp]: "fetch (ci (ly) 
@@ -2439,7 +2432,7 @@
     = (R, start_of ly as + 2*n + 4)"
 apply(subgoal_tac "2*n + 4 = Suc (2*n + 3)", simp only: fetch.simps)
 apply(auto simp: ci.simps findnth.simps fetch.simps
-                  nth_of.simps shift.simps nth_append tdec_b_def length_findnth sete.simps)
+                  nth_of.simps shift.simps nth_append tdec_b_def length_findnth adjust.simps)
 done
 
 lemma [simp]:"fetch (ci (ly) 
@@ -2447,7 +2440,7 @@
     = (R, start_of ly as + 2*n + 5)"
 apply(subgoal_tac "2*n + 5 = Suc (2*n + 4)", simp only: fetch.simps)
 apply(auto simp: ci.simps findnth.simps fetch.simps
-                  nth_of.simps shift.simps nth_append tdec_b_def length_findnth sete.simps)
+                  nth_of.simps shift.simps nth_append tdec_b_def length_findnth adjust.simps)
 done
 
 
@@ -2457,7 +2450,7 @@
     = (L, start_of ly as + 2*n + 6)"
 apply(subgoal_tac "2*n + 6 = Suc (2*n + 5)", simp only: fetch.simps)
 apply(auto simp: ci.simps findnth.simps fetch.simps
-                  nth_of.simps shift.simps nth_append tdec_b_def length_findnth sete.simps)
+                  nth_of.simps shift.simps nth_append tdec_b_def length_findnth adjust.simps)
 done
 
 lemma [simp]: 
@@ -2466,7 +2459,7 @@
     = (L, start_of ly as + 2*n + 7)"
 apply(subgoal_tac "2*n + 6 = Suc (2*n + 5)", simp only: fetch.simps)
 apply(auto simp: ci.simps findnth.simps fetch.simps
-                  nth_of.simps shift.simps nth_append tdec_b_def length_findnth sete.simps)
+                  nth_of.simps shift.simps nth_append tdec_b_def length_findnth adjust.simps)
 done
 
 lemma [simp]:"fetch (ci (ly) 
@@ -2474,7 +2467,7 @@
     = (L, start_of ly as + 2*n + 10)"
 apply(subgoal_tac "2*n + 7 = Suc (2*n + 6)", simp only: fetch.simps)
 apply(auto simp: ci.simps findnth.simps fetch.simps
-                  nth_of.simps shift.simps nth_append tdec_b_def length_findnth sete.simps)
+                  nth_of.simps shift.simps nth_append tdec_b_def length_findnth adjust.simps)
 done
 
 lemma [simp]:
@@ -2483,7 +2476,7 @@
     = (W1, start_of ly as + 2*n + 7)"
 apply(subgoal_tac "2*n + 8 = Suc (2*n + 7)", simp only: fetch.simps)
 apply(auto simp: ci.simps findnth.simps fetch.simps
-                  nth_of.simps shift.simps nth_append tdec_b_def length_findnth sete.simps)
+                  nth_of.simps shift.simps nth_append tdec_b_def length_findnth adjust.simps)
 done
 
 
@@ -2493,7 +2486,7 @@
     = (R, start_of ly as + 2*n + 8)"
 apply(subgoal_tac "2*n + 8 = Suc (2*n + 7)", simp only: fetch.simps)
 apply(auto simp: ci.simps findnth.simps fetch.simps
-                  nth_of.simps shift.simps nth_append tdec_b_def length_findnth sete.simps)
+                  nth_of.simps shift.simps nth_append tdec_b_def length_findnth adjust.simps)
 done
 
 lemma [simp]: 
@@ -2502,7 +2495,7 @@
   = (L, start_of ly as + 2*n + 9)"
 apply(subgoal_tac "2*n + 9 = Suc (2*n + 8)", simp only: fetch.simps)
 apply(auto simp: ci.simps findnth.simps fetch.simps
-                  nth_of.simps shift.simps nth_append tdec_b_def length_findnth sete.simps)
+                  nth_of.simps shift.simps nth_append tdec_b_def length_findnth adjust.simps)
 done
 
 lemma [simp]: 
@@ -2511,7 +2504,7 @@
   = (R, start_of ly as + 2*n + 8)"
 apply(subgoal_tac "2*n + 9 = Suc (2*n + 8)", simp only: fetch.simps)
 apply(auto simp: ci.simps findnth.simps fetch.simps
-                  nth_of.simps shift.simps nth_append tdec_b_def length_findnth sete.simps)
+                  nth_of.simps shift.simps nth_append tdec_b_def length_findnth adjust.simps)
 done
 
 
@@ -2521,7 +2514,7 @@
   = (R, start_of ly as + 2*n + 4)" 
 apply(subgoal_tac "2*n + 10 = Suc (2*n + 9)", simp only: fetch.simps)
 apply(auto simp: ci.simps findnth.simps fetch.simps
-                  nth_of.simps shift.simps nth_append tdec_b_def length_findnth sete.simps)
+                  nth_of.simps shift.simps nth_append tdec_b_def length_findnth adjust.simps)
 done
 
 lemma [simp]: "fetch (ci (ly) 
@@ -2529,7 +2522,7 @@
     = (W0, start_of ly as + 2*n + 9)"
 apply(subgoal_tac "2*n + 10 = Suc (2*n + 9)", simp only: fetch.simps)
 apply(auto simp: ci.simps findnth.simps fetch.simps
-                  nth_of.simps shift.simps nth_append tdec_b_def length_findnth sete.simps)
+                  nth_of.simps shift.simps nth_append tdec_b_def length_findnth adjust.simps)
 done
 
 
@@ -2539,7 +2532,7 @@
   = (L, start_of ly as + 2*n + 10)"
 apply(subgoal_tac "2*n + 11 = Suc (2*n + 10)", simp only: fetch.simps)
 apply(auto simp: ci.simps findnth.simps fetch.simps
-                  nth_of.simps shift.simps nth_append tdec_b_def length_findnth sete.simps)
+                  nth_of.simps shift.simps nth_append tdec_b_def length_findnth adjust.simps)
 done
 
 
@@ -2549,7 +2542,7 @@
   = (L, start_of ly as + 2*n + 11)"
 apply(subgoal_tac "2*n + 11 = Suc (2*n + 10)", simp only: fetch.simps)
 apply(auto simp: ci.simps findnth.simps fetch.simps
-                  nth_of.simps shift.simps nth_append tdec_b_def length_findnth sete.simps)
+                  nth_of.simps shift.simps nth_append tdec_b_def length_findnth adjust.simps)
 done
 
 lemma [simp]:
@@ -2558,7 +2551,7 @@
   = (L, start_of ly as + 2*n + 10)"
 apply(subgoal_tac "2*n + 12 = Suc (2*n + 11)", simp only: fetch.simps)
 apply(auto simp: ci.simps findnth.simps fetch.simps
-                  nth_of.simps shift.simps nth_append tdec_b_def length_findnth sete.simps)
+                  nth_of.simps shift.simps nth_append tdec_b_def length_findnth adjust.simps)
 done
 
 
@@ -2568,7 +2561,7 @@
   = (R, start_of ly as + 2*n + 12)"
 apply(subgoal_tac "2*n + 12 = Suc (2*n + 11)", simp only: fetch.simps)
 apply(auto simp: ci.simps findnth.simps fetch.simps
-                  nth_of.simps shift.simps nth_append tdec_b_def length_findnth sete.simps)
+                  nth_of.simps shift.simps nth_append tdec_b_def length_findnth adjust.simps)
 done
 
 lemma [simp]: 
@@ -2577,7 +2570,7 @@
   = (R, start_of ly as + 2*n + 16)"
 apply(subgoal_tac "2*n + 13 = Suc (2*n + 12)", simp only: fetch.simps)
 apply(auto simp: ci.simps findnth.simps fetch.simps
-                  nth_of.simps shift.simps nth_append tdec_b_def length_findnth sete.simps)
+                  nth_of.simps shift.simps nth_append tdec_b_def length_findnth adjust.simps)
 done
 
 
@@ -2587,7 +2580,7 @@
   = (L, start_of ly as + 2*n + 13)"
 apply(subgoal_tac "14 + 2*n = Suc (2*n + 13)", simp only: fetch.simps)
 apply(auto simp: ci.simps findnth.simps fetch.simps
-                  nth_of.simps shift.simps nth_append tdec_b_def length_findnth sete.simps)
+                  nth_of.simps shift.simps nth_append tdec_b_def length_findnth adjust.simps)
 done
 
 lemma [simp]: 
@@ -2596,7 +2589,7 @@
   = (L, start_of ly as + 2*n + 14)"
 apply(subgoal_tac "14 + 2*n = Suc (2*n + 13)", simp only: fetch.simps)
 apply(auto simp: ci.simps findnth.simps fetch.simps
-                  nth_of.simps shift.simps nth_append tdec_b_def length_findnth sete.simps)
+                  nth_of.simps shift.simps nth_append tdec_b_def length_findnth adjust.simps)
 done
 
 lemma [simp]: 
@@ -2605,7 +2598,7 @@
   = (L, start_of ly as + 2*n + 13)"
 apply(subgoal_tac "15 + 2*n = Suc (2*n + 14)", simp only: fetch.simps)
 apply(auto simp: ci.simps findnth.simps fetch.simps
-                  nth_of.simps shift.simps nth_append tdec_b_def length_findnth sete.simps)
+                  nth_of.simps shift.simps nth_append tdec_b_def length_findnth adjust.simps)
 done
 
 lemma [simp]: 
@@ -2614,7 +2607,7 @@
  = (R, start_of ly as + 2*n + 15)"
 apply(subgoal_tac "15 + 2*n = Suc (2*n + 14)", simp only: fetch.simps)
 apply(auto simp: ci.simps findnth.simps fetch.simps
-                  nth_of.simps shift.simps nth_append tdec_b_def length_findnth sete.simps)
+                  nth_of.simps shift.simps nth_append tdec_b_def length_findnth adjust.simps)
 done
 
 lemma [simp]: 
@@ -2624,7 +2617,7 @@
  = (R, start_of (ly) e)"
 apply(subgoal_tac "16 + 2*n = Suc (2*n + 15)", simp only: fetch.simps)
 apply(auto simp: ci.simps findnth.simps fetch.simps
-                  nth_of.simps shift.simps nth_append tdec_b_def length_findnth sete.simps)
+                  nth_of.simps shift.simps nth_append tdec_b_def length_findnth adjust.simps)
 done
 
 declare dec_inv_1.simps[simp del]
@@ -3533,7 +3526,7 @@
 proof(simp add: ci.simps)
   let ?off = "start_of ly as - Suc 0"
   let ?A = "findnth n"
-  let ?B = "sete (shift (shift tdec_b (2 * n)) ?off) (start_of ly e)"
+  let ?B = "adjust (shift (shift tdec_b (2 * n)) ?off) (start_of ly e)"
   have "\<exists> stp la ra. steps (s, l, r) (shift ?A ?off @ ?B, ?off) stp = (start_of ly as + 2*n, la, ra)
                     \<and> inv_locate_a (as, lm) (n, la, ra) ires"
   proof -
@@ -3693,7 +3686,7 @@
   "(map (length \<circ> (\<lambda>(xa, y). ci (layout_of xs @ [length_of x]) xa y)) (tpairs_of xs)) = 
   (map (length \<circ> (\<lambda>(x, y). ci (layout_of xs) x y)) (tpairs_of xs)) "
 apply(auto)
-apply(case_tac b, auto simp: ci.simps sete.simps)
+apply(case_tac b, auto simp: ci.simps adjust.simps)
 done
 
 lemma length_tp'[simp]: 
@@ -3721,7 +3714,7 @@
     using tp b
     apply(auto simp: layout_id_cons tm_of.simps tms_of.simps length_concat tpairs_id_cons map_length_ci)
     apply(case_tac x)
-    apply(auto simp: ci.simps tinc_b_def tdec_b_def length_findnth sete.simps length_of.simps
+    apply(auto simp: ci.simps tinc_b_def tdec_b_def length_findnth adjust.simps length_of.simps
                  split: abc_inst.splits)
     done
 qed
diff -r 5974111de158 -r f1ecb4a68a54 thys/Recursive.thy
--- a/thys/Recursive.thy	Thu Feb 21 05:33:57 2013 +0000
+++ b/thys/Recursive.thy	Thu Feb 21 05:34:39 2013 +0000
@@ -4909,7 +4909,7 @@
 lemma tms_any_less: 
   "\<lbrakk>k < length ap; (a, b) \<in> set (tms_of ap ! k)\<rbrakk> \<Longrightarrow> 
   b \<le> start_of (layout_of ap) (length ap)"
-apply(case_tac "ap!k", auto simp: tms_of.simps tpairs_of.simps ci.simps shift_append sete.simps)
+apply(case_tac "ap!k", auto simp: tms_of.simps tpairs_of.simps ci.simps shift_append adjust.simps)
 apply(erule_tac findnth_state_all_le1, simp_all)
 apply(erule_tac inc_state_all_le, simp_all)
 apply(erule_tac findnth_state_all_le2, simp_all)
@@ -4951,12 +4951,12 @@
       \<Longrightarrow> layout_of ap ! k = qa"
 apply(case_tac "ap ! k")
 apply(auto simp: layout_of.simps ci.simps 
-  length_of.simps tinc_b_def tdec_b_def length_findnth sete.simps)
+  length_of.simps tinc_b_def tdec_b_def length_findnth adjust.simps)
 done
 
 lemma [intro]: "length (ci ly y i) mod 2 = 0"
 apply(case_tac i, auto simp: ci.simps length_findnth
-  tinc_b_def sete.simps tdec_b_def)
+  tinc_b_def adjust.simps tdec_b_def)
 done
 
 lemma [intro]: "listsum (map (length \<circ> (\<lambda>(x, y). ci ly x y)) zs) mod 2 = 0"
diff -r 5974111de158 -r f1ecb4a68a54 thys/Turing.thy
--- a/thys/Turing.thy	Thu Feb 21 05:33:57 2013 +0000
+++ b/thys/Turing.thy	Thu Feb 21 05:34:39 2013 +0000
@@ -205,16 +205,19 @@
   "shift p n = (map (\<lambda> (a, s). (a, (if s = 0 then 0 else s + n))) p)"
 
 fun 
-  adjust :: "instr list \<Rightarrow> instr list"
+  adjust :: "instr list \<Rightarrow> nat \<Rightarrow> instr list"
 where
-  "adjust p = map (\<lambda> (a, s). (a, if s = 0 then (Suc (length p div 2)) else s)) p"
+  "adjust p e = map (\<lambda> (a, s). (a, if s = 0 then e else s)) p"
+
+abbreviation
+  "adjust0 p \<equiv> adjust p (Suc (length p div 2))"
 
 lemma length_shift [simp]: 
   shows "length (shift p n) = length p"
 by simp
 
 lemma length_adjust [simp]: 
-  shows "length (adjust p) = length p"
+  shows "length (adjust p n) = length p"
 by (induct p) (auto)
 
 
@@ -222,7 +225,7 @@
 fun
   tm_comp :: "instr list \<Rightarrow> instr list \<Rightarrow> instr list" ("_ |+| _" [0, 0] 100)
 where
-  "tm_comp p1 p2 = ((adjust p1) @ (shift p2 (length p1 div 2)))"
+  "tm_comp p1 p2 = ((adjust0 p1) @ (shift p2 (length p1 div 2)))"
 
 lemma tm_comp_length:
   shows "length (A |+| B) = length A + length B"
diff -r 5974111de158 -r f1ecb4a68a54 thys/UTM.thy
--- a/thys/UTM.thy	Thu Feb 21 05:33:57 2013 +0000
+++ b/thys/UTM.thy	Thu Feb 21 05:34:39 2013 +0000
@@ -543,7 +543,7 @@
 
 definition t_twice :: "instr list"
   where
-  "t_twice = adjust t_twice_compile"
+  "t_twice = adjust0 t_twice_compile"
 
 definition t_fourtimes_compile :: "instr list"
 where
@@ -551,7 +551,7 @@
 
 definition t_fourtimes :: "instr list"
   where
-  "t_fourtimes = adjust t_fourtimes_compile"
+  "t_fourtimes = adjust0 t_fourtimes_compile"
 
 definition t_twice_len :: "nat"
   where
@@ -1266,7 +1266,7 @@
 
 lemma adjust_fetch0: 
   "\<lbrakk>0 < a; a \<le> length ap div 2;  fetch ap a b = (aa, 0)\<rbrakk>
-  \<Longrightarrow> fetch (adjust ap) a b = (aa, Suc (length ap div 2))"
+  \<Longrightarrow> fetch (adjust0 ap) a b = (aa, Suc (length ap div 2))"
 apply(case_tac b, auto simp: fetch.simps nth_of.simps nth_map
                        split: if_splits)
 apply(case_tac [!] a, auto simp: fetch.simps nth_of.simps)
@@ -1274,7 +1274,7 @@
 
 lemma adjust_fetch_norm: 
   "\<lbrakk>st > 0;  st \<le> length tp div 2; fetch ap st b = (aa, ns); ns \<noteq> 0\<rbrakk>
- \<Longrightarrow>  fetch (Turing.adjust ap) st b = (aa, ns)"
+ \<Longrightarrow>  fetch (adjust0 ap) st b = (aa, ns)"
  apply(case_tac b, auto simp: fetch.simps nth_of.simps nth_map
                        split: if_splits)
 apply(case_tac [!] st, auto simp: fetch.simps nth_of.simps)
@@ -1286,7 +1286,7 @@
   assumes exec: "step0 (st,l,r) ap = (st', l', r')"
   and wf_tm: "tm_wf (ap, 0)"
   and notfinal: "st' > 0"
-  shows "step0 (st, l, r) (adjust ap) = (st', l', r')"
+  shows "step0 (st, l, r) (adjust0 ap) = (st', l', r')"
   using assms
 proof -
   have "st > 0"
@@ -1300,7 +1300,7 @@
       nth_of.simps adjust.simps tm_wf.simps split: if_splits)
     apply(auto simp: mod_ex2)
     done    
-  ultimately have "fetch (adjust ap) st (read r) = fetch ap st (read r)"
+  ultimately have "fetch (adjust0 ap) st (read r) = fetch ap st (read r)"
     using assms
     apply(case_tac "fetch ap st (read r)")
     apply(drule_tac adjust_fetch_norm, simp_all)
@@ -1317,7 +1317,7 @@
   assumes exec: "steps0 (st,l,r) ap stp = (st', l', r')"
   and wf_tm: "tm_wf (ap, 0)"
   and notfinal: "st' > 0"
-  shows "steps0 (st, l, r) (adjust ap) stp = (st', l', r')"
+  shows "steps0 (st, l, r) (adjust0 ap) stp = (st', l', r')"
   using exec notfinal
 proof(induct stp arbitrary: st' l' r')
   case 0
@@ -1326,7 +1326,7 @@
 next
   case (Suc stp st' l' r')
   have ind: "\<And>st' l' r'. \<lbrakk>steps0 (st, l, r) ap stp = (st', l', r'); 0 < st'\<rbrakk> 
-    \<Longrightarrow> steps0 (st, l, r) (Turing.adjust ap) stp = (st', l', r')" by fact
+    \<Longrightarrow> steps0 (st, l, r) (adjust0 ap) stp = (st', l', r')" by fact
   have h: "steps0 (st, l, r) ap (Suc stp) = (st', l', r')" by fact
   have g:   "0 < st'" by fact
   obtain st'' l'' r'' where a: "steps0 (st, l, r) ap stp = (st'', l'', r'')"
@@ -1336,7 +1336,7 @@
     apply(simp add: step_red)
     apply(case_tac st'', auto)
     done
-  hence b: "steps0 (st, l, r) (Turing.adjust ap) stp = (st'', l'', r'')"
+  hence b: "steps0 (st, l, r) (adjust0 ap) stp = (st'', l'', r'')"
     using a
     by(rule_tac ind, simp_all)
   thus "?case"
@@ -1349,7 +1349,7 @@
 lemma adjust_halt_eq:
   assumes exec: "steps0 (1, l, r) ap stp = (0, l', r')"
   and tm_wf: "tm_wf (ap, 0)" 
-  shows "\<exists> stp. steps0 (Suc 0, l, r) (adjust ap) stp = 
+  shows "\<exists> stp. steps0 (Suc 0, l, r) (adjust0 ap) stp = 
         (Suc (length ap div 2), l', r')"
 proof -
   have "\<exists> stp. \<not> is_final (steps0 (1, l, r) ap stp) \<and> (steps0 (1, l, r) ap (Suc stp) = (0, l', r'))"
@@ -1358,7 +1358,7 @@
   then obtain stpa where a: 
     "\<not> is_final (steps0 (1, l, r) ap stpa) \<and> (steps0 (1, l, r) ap (Suc stpa) = (0, l', r'))" ..
   obtain sa la ra where b:"steps0 (1, l, r) ap stpa = (sa, la, ra)"  by (metis prod_cases3)
-  hence c: "steps0 (Suc 0, l, r) (adjust ap) stpa = (sa, la, ra)"
+  hence c: "steps0 (Suc 0, l, r) (adjust0 ap) stpa = (sa, la, ra)"
     using assms a
     apply(rule_tac adjust_steps_eq, simp_all)
     done
@@ -1371,7 +1371,7 @@
     using b a
     apply(simp add: step_red step.simps)
     done
-  have k: "fetch (adjust ap) sa (read ra) = (ac, Suc (length ap div 2))"
+  have k: "fetch (adjust0 ap) sa (read ra) = (ac, Suc (length ap div 2))"
     using a b c d e f
     apply(rule_tac adjust_fetch0, simp_all)
     done
@@ -1402,14 +1402,14 @@
     (tm_of abc_twice @ shift (mopup (Suc 0)) ((length (tm_of abc_twice) div 2))) stp =
     (0, Bk\<up>(ln) @ Bk # Bk # ires, Oc\<up>(Suc (2 * rs)) @ Bk\<up>(rn))" by blast
   hence "\<exists> stp. steps0 (Suc 0, Bk # Bk # ires, Oc\<up>(Suc rs) @ Bk\<up>(n))
-    (adjust t_twice_compile) stp
+    (adjust0 t_twice_compile) stp
      = (Suc (length t_twice_compile div 2), Bk\<up>(ln) @ Bk # Bk # ires, Oc\<up>(Suc (2 * rs)) @ Bk\<up>(rn))"
     apply(rule_tac stp = stp in adjust_halt_eq)
     apply(simp add: t_twice_compile_def, auto)
     done
   then obtain stpb where 
     "steps0 (Suc 0, Bk # Bk # ires, Oc\<up>(Suc rs) @ Bk\<up>(n))
-    (adjust t_twice_compile) stpb
+    (adjust0 t_twice_compile) stpb
      = (Suc (length t_twice_compile div 2), Bk\<up>(ln) @ Bk # Bk # ires, Oc\<up>(Suc (2 * rs)) @ Bk\<up>(rn))" ..
   thus "?thesis"
     apply(simp add: t_twice_def t_twice_len_def)
@@ -2079,14 +2079,14 @@
     (tm_of abc_fourtimes @ shift (mopup 1) ((length (tm_of abc_fourtimes) div 2))) stp =
     (0, Bk\<up>(ln) @ Bk # Bk # ires, Oc\<up>(Suc (4 * rs)) @ Bk\<up>(rn))" by blast
   hence "\<exists> stp. steps0 (Suc 0, Bk # Bk # ires, Oc\<up>(Suc rs) @ Bk\<up>(n))
-    (adjust t_fourtimes_compile) stp
+    (adjust0 t_fourtimes_compile) stp
      = (Suc (length t_fourtimes_compile div 2), Bk\<up>(ln) @ Bk # Bk # ires, Oc\<up>(Suc (4 * rs)) @ Bk\<up>(rn))"
     apply(rule_tac stp = stp in adjust_halt_eq)
     apply(simp add: t_fourtimes_compile_def, auto)
     done
   then obtain stpb where 
     "steps0 (Suc 0, Bk # Bk # ires, Oc\<up>(Suc rs) @ Bk\<up>(n))
-    (adjust t_fourtimes_compile) stpb
+    (adjust0 t_fourtimes_compile) stpb
      = (Suc (length t_fourtimes_compile div 2), Bk\<up>(ln) @ Bk # Bk # ires, Oc\<up>(Suc (4 * rs)) @ Bk\<up>(rn))" ..
   thus "?thesis"
     apply(simp add: t_fourtimes_def t_fourtimes_len_def)
@@ -3356,7 +3356,7 @@
 
 
 lemma tm_wf_change_termi: "tm_wf (tp, 0) \<Longrightarrow> 
-      list_all (\<lambda>(acn, st). (st \<le> Suc (length tp div 2))) (adjust tp)"
+      list_all (\<lambda>(acn, st). (st \<le> Suc (length tp div 2))) (adjust0 tp)"
 apply(auto simp: tm_wf.simps List.list_all_length)
 apply(case_tac "tp!n", auto simp: adjust.simps split: if_splits)
 apply(erule_tac x = "(a, b)" in ballE, auto)
@@ -3376,28 +3376,36 @@
 apply(auto simp: mopup.simps)
 done
 
-lemma [elim]: "(a, b) \<in> set (shift (Turing.adjust t_twice_compile) 12) \<Longrightarrow> 
+lemma [elim]: "(a, b) \<in> set (shift (adjust0 t_twice_compile) 12) \<Longrightarrow> 
   b \<le> (28 + (length t_twice_compile + length t_fourtimes_compile)) div 2"
 apply(simp add: t_twice_compile_def t_fourtimes_compile_def)
 proof -
-  assume g: "(a, b) \<in> set (shift (Turing.adjust (tm_of abc_twice @ shift (mopup (Suc 0)) (length (tm_of abc_twice) div 2))) 12)"
+  assume g: "(a, b)
+    \<in> set (shift
+            (adjust
+              (tm_of abc_twice @
+               shift (mopup (Suc 0)) (length (tm_of abc_twice) div 2))
+              (Suc ((length (tm_of abc_twice) + 16) div 2)))
+            12)"
   moreover have "length (tm_of abc_twice) mod 2 = 0" by auto
   moreover have "length (tm_of abc_fourtimes) mod 2 = 0" by auto
   ultimately have "list_all (\<lambda>(acn, st). (st \<le> (60 + (length (tm_of abc_twice) + length (tm_of abc_fourtimes))) div 2)) 
-    (shift (Turing.adjust t_twice_compile) 12)"
-  proof(auto simp: mod_ex1)
+    (shift (adjust0 t_twice_compile) 12)"
+  proof(auto simp add: mod_ex1 del: adjust.simps)
     fix q qa
     assume h: "length (tm_of abc_twice) = 2 * q" "length (tm_of abc_fourtimes) = 2 * qa"
-    hence "list_all (\<lambda>(acn, st). st \<le> (18 + (q + qa)) + 12) (shift (Turing.adjust t_twice_compile) 12)"
+    hence "list_all (\<lambda>(acn, st). st \<le> (18 + (q + qa)) + 12) (shift (adjust0 t_twice_compile) 12)"
     proof(rule_tac tm_wf_shift t_twice_compile_def)
-      have "list_all (\<lambda>(acn, st). st \<le> Suc (length t_twice_compile div 2)) (adjust t_twice_compile)"
+      have "list_all (\<lambda>(acn, st). st \<le> Suc (length t_twice_compile div 2)) (adjust0 t_twice_compile)"
         by(rule_tac tm_wf_change_termi, auto)
-      thus "list_all (\<lambda>(acn, st). st \<le> 18 + (q + qa)) (Turing.adjust t_twice_compile)"
+      thus "list_all (\<lambda>(acn, st). st \<le> 18 + (q + qa)) (adjust0 t_twice_compile)"
         using h
         apply(simp add: t_twice_compile_def, auto simp: List.list_all_length)
         done
     qed
-    thus "list_all (\<lambda>(acn, st). st \<le> 30 + (q + qa)) (shift (Turing.adjust t_twice_compile) 12)"
+    thus "list_all (\<lambda>(acn, st). st \<le> 30 + (q + qa))
+           (shift
+             (adjust t_twice_compile (Suc (length t_twice_compile div 2))) 12)"
       by simp
   qed
   thus "b \<le> (60 + (length (tm_of abc_twice) + length (tm_of abc_fourtimes))) div 2"
@@ -3408,37 +3416,50 @@
     done
 qed 
 
-lemma [elim]: "(a, b) \<in> set (shift (Turing.adjust t_fourtimes_compile) (t_twice_len + 13)) 
+lemma [elim]: "(a, b) \<in> set (shift (adjust0 t_fourtimes_compile) (t_twice_len + 13)) 
   \<Longrightarrow> b \<le> (28 + (length t_twice_compile + length t_fourtimes_compile)) div 2"
 apply(simp add: t_twice_compile_def t_fourtimes_compile_def t_twice_len_def)
 proof -
-  assume g: "(a, b) \<in> set (shift (Turing.adjust (tm_of abc_fourtimes @ shift (mopup (Suc 0))
-    (length (tm_of abc_fourtimes) div 2))) (length t_twice div 2 + 13))"
+  assume g: "(a, b)
+    \<in> set (shift
+            (adjust
+              (tm_of abc_fourtimes @
+               shift (mopup (Suc 0)) (length (tm_of abc_fourtimes) div 2))
+              (Suc ((length (tm_of abc_fourtimes) + 16) div 2)))
+            (length t_twice div 2 + 13))"
   moreover have "length (tm_of abc_twice) mod 2 = 0" by auto
   moreover have "length (tm_of abc_fourtimes) mod 2 = 0" by auto
   ultimately have "list_all (\<lambda>(acn, st). (st \<le> (60 + (length (tm_of abc_twice) + length (tm_of abc_fourtimes))) div 2)) 
-    (shift (Turing.adjust (tm_of abc_fourtimes @ shift (mopup (Suc 0))
+    (shift (adjust0 (tm_of abc_fourtimes @ shift (mopup (Suc 0))
     (length (tm_of abc_fourtimes) div 2))) (length t_twice div 2 + 13))"
   proof(auto simp: mod_ex1 t_twice_def t_twice_compile_def)
     fix q qa
     assume h: "length (tm_of abc_twice) = 2 * q" "length (tm_of abc_fourtimes) = 2 * qa"
     hence "list_all (\<lambda>(acn, st). st \<le> (9 + qa + (21 + q)))
-      (shift (Turing.adjust (tm_of abc_fourtimes @ shift (mopup (Suc 0)) qa)) (21 + q))"
+      (shift (adjust0 (tm_of abc_fourtimes @ shift (mopup (Suc 0)) qa)) (21 + q))"
     proof(rule_tac tm_wf_shift t_twice_compile_def)
       have "list_all (\<lambda>(acn, st). st \<le> Suc (length (tm_of abc_fourtimes @ shift 
-        (mopup (Suc 0)) qa) div 2)) (adjust (tm_of abc_fourtimes @ shift (mopup (Suc 0)) qa))"
+        (mopup (Suc 0)) qa) div 2)) (adjust0 (tm_of abc_fourtimes @ shift (mopup (Suc 0)) qa))"
         apply(rule_tac tm_wf_change_termi)
         using wf_fourtimes h
         apply(simp add: t_fourtimes_compile_def)
-        done        
-      thus "list_all (\<lambda>(acn, st). st \<le> 9 + qa) ((Turing.adjust (tm_of abc_fourtimes @ shift (mopup (Suc 0)) qa)))"
+        done
+      thus "list_all (\<lambda>(acn, st). st \<le> 9 + qa)
+        (adjust (tm_of abc_fourtimes @ shift (mopup (Suc 0)) qa)
+          (Suc (length (tm_of abc_fourtimes @ shift (mopup (Suc 0)) qa) div
+                2)))"
         using h
         apply(simp)
         done
     qed
-    thus "list_all (\<lambda>(acn, st). st \<le> 30 + (q + qa)) (shift (Turing.adjust (tm_of abc_fourtimes @ shift (mopup (Suc 0)) qa)) (21 + q))"
+    thus "list_all (\<lambda>(acn, st). st \<le> 30 + (q + qa))
+           (shift
+             (adjust (tm_of abc_fourtimes @ shift (mopup (Suc 0)) qa)
+               (9 + qa))
+             (21 + q))"
       apply(subgoal_tac "qa + q = q + qa")
-      apply(simp, simp)
+      apply(simp add: h)
+      apply(simp)
       done
   qed
   thus "b \<le> (60 + (length (tm_of abc_twice) + length (tm_of abc_fourtimes))) div 2"
@@ -3515,7 +3536,7 @@
     apply(auto simp: Hoare_halt_def)
     apply(rule_tac x = n in exI)
     apply(case_tac "(steps0 (Suc 0, [], <m # args>)
-      (Turing.adjust t_wcode_prepare @ shift t_wcode_main (length t_wcode_prepare div 2)) n)")
+      (adjust0 t_wcode_prepare @ shift t_wcode_main (length t_wcode_prepare div 2)) n)")
     apply(auto simp: tm_comp.simps)
     done
 qed
@@ -4613,7 +4634,7 @@
   *}
 definition t_wcode :: "instr list"
   where
-  "t_wcode = (t_wcode_prepare |+| t_wcode_main) |+| t_wcode_adjust"
+  "t_wcode = (t_wcode_prepare |+| t_wcode_main) |+| t_wcode_adjust        "
 
 
 text {*