
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




