diff -r 4e50ff177348 -r 6e1c03614d36 thys/Abacus.thy
--- a/thys/Abacus.thy	Wed Dec 19 16:47:10 2018 +0100
+++ b/thys/Abacus.thy	Fri Dec 21 12:31:36 2018 +0100
@@ -285,8 +285,8 @@
 *}
 
 declare abc_step_l.simps[simp del] abc_steps_l.simps[simp del]
-lemma [simp]: "start_of ly as > 0"
-apply(simp add: start_of.simps)
+lemma start_of_nonzero[simp]: "start_of ly as > 0" "(start_of ly as = 0) = False"
+apply(auto simp: start_of.simps)
 done
 
 lemma abc_steps_l_0: "abc_steps_l ac ap 0 = ac"
@@ -461,7 +461,7 @@
 lemma map_of:  "n < length xs \<Longrightarrow> (map f xs) ! n = f (xs ! n)"
 by(auto)
 
-lemma [simp]: "length (tms_of aprog) = length aprog"
+lemma length_tms_of[simp]: "length (tms_of aprog) = length aprog"
 apply(auto simp: tms_of.simps tpairs_of.simps)
 done
 
@@ -504,7 +504,7 @@
            (x + y) mod 2 = 0"
 by(auto)
 
-lemma [simp]: "length (layout_of aprog) = length aprog"
+lemma length_layout_of[simp]: "length (layout_of aprog) = length aprog"
 by(auto simp: layout_of.simps)
 
 lemma start_of_ind: "\<lbrakk>as < length aprog; ly = layout_of aprog\<rbrakk> \<Longrightarrow> 
@@ -517,16 +517,13 @@
   concat (take (Suc n) xs) = concat (take n xs) @ (xs ! n)"
   using concat_suc.
 
-lemma [simp]: 
+lemma ci_in_set[simp]: 
   "\<lbrakk>as < length aprog; (abc_fetch as aprog) = Some ins\<rbrakk>
   \<Longrightarrow> ci (layout_of aprog) 
   (start_of (layout_of aprog) as) (ins) \<in> set (tms_of aprog)"
   by(insert ci_nth[of "layout_of aprog" aprog as], simp)
 
-lemma [simp]: "length (tms_of ap) = length ap"
-by(auto simp: tms_of.simps tpairs_of.simps)
-
-lemma [intro]:  "n < length ap \<Longrightarrow> length (tms_of ap ! n) mod 2 = 0"
+lemma length_tms_of_elem_even[intro]:  "n < length ap \<Longrightarrow> length (tms_of ap ! n) mod 2 = 0"
   apply(cases "ap ! n")
   by (auto simp: tms_of.simps tpairs_of.simps ci.simps length_findnth tinc_b_def tdec_b_def)
 
@@ -1125,43 +1122,20 @@
 
 declare findnth_inv.simps[simp del]
 
-lemma [simp]: 
+lemma x_is_2n_arith[simp]: 
   "\<lbrakk>x < Suc (Suc (2 * n)); Suc x mod 2 = Suc 0; \<not> x < 2 * n\<rbrakk>
  \<Longrightarrow> x = 2*n"
 by arith
 
-lemma [simp]: 
-  "\<lbrakk>0 < a; a < Suc (2 * n); a mod 2 = Suc 0\<rbrakk> 
-      \<Longrightarrow> fetch (findnth n) a Bk = (W1, a)"
-apply(case_tac a, simp_all)
-apply(induct n, auto simp: findnth.simps length_findnth nth_append)
-apply arith
-done
-
-lemma [simp]: 
-  "\<lbrakk>0 < a; a < Suc (2 * n); a mod 2 = Suc 0\<rbrakk> 
-      \<Longrightarrow> fetch (findnth n) a Oc = (R, Suc a)"
-apply(case_tac a, simp_all)
-apply(induct n, auto simp: findnth.simps length_findnth nth_append)
-apply(subgoal_tac "nat = 2 * n", simp)
-by arith
-
-lemma [simp]: 
-  "\<lbrakk>0 < a; a < Suc (2*n); a mod 2 \<noteq> Suc 0\<rbrakk>
-     \<Longrightarrow> fetch (findnth n) a Oc = (R, a)"
-apply(case_tac a, simp_all)
-apply(induct n, auto simp: findnth.simps length_findnth nth_append)
-apply(subgoal_tac "nat = Suc (2 * n)", simp)
-apply arith
-done
-
-lemma [simp]: 
-  "\<lbrakk>0 < a; a < Suc (2*n); a mod 2 \<noteq> Suc 0\<rbrakk>
-     \<Longrightarrow> fetch (findnth n) a Bk = (R, Suc a)"
-apply(case_tac a, simp_all)
-apply(induct n, auto simp: findnth.simps length_findnth nth_append)
-apply(subgoal_tac "nat = Suc (2 * n)", simp)
-by arith
+
+lemma between_sucs:"x < Suc n \<Longrightarrow> \<not> x < n \<Longrightarrow> x = n" by auto
+
+lemma fetch_findnth[simp]: 
+  "\<lbrakk>0 < a; a < Suc (2 * n); a mod 2 = Suc 0\<rbrakk> \<Longrightarrow> fetch (findnth n) a Oc = (R, Suc a)"
+  "\<lbrakk>0 < a; a < Suc (2 * n); a mod 2 \<noteq> Suc 0\<rbrakk> \<Longrightarrow> fetch (findnth n) a Oc = (R, a)"
+  "\<lbrakk>0 < a; a < Suc (2 * n); a mod 2 \<noteq> Suc 0\<rbrakk> \<Longrightarrow> fetch (findnth n) a Bk = (R, Suc a)"
+  "\<lbrakk>0 < a; a < Suc (2 * n); a mod 2 = Suc 0\<rbrakk> \<Longrightarrow> fetch (findnth n) a Bk = (W1, a)"
+by(cases a;induct n;force simp: length_findnth nth_append dest!:between_sucs)+
 
 declare at_begin_norm.simps[simp del] at_begin_fst_bwtn.simps[simp del] 
    at_begin_fst_awtn.simps[simp del] in_middle.simps[simp del] 
@@ -1179,27 +1153,27 @@
    inv_stop.simps[simp del] inv_locate_a.simps[simp del] 
    inv_locate_b.simps[simp del]
 
-lemma [intro]: "\<exists>rn. [Bk] = Bk \<up> rn"
-by (metis replicate_0 replicate_Suc)
-
-lemma [intro]:  "at_begin_norm (as, am) (q, aaa, []) ires
+lemma replicate_once[intro]: "\<exists>rn. [Bk] = Bk \<up> rn"
+by (metis replicate.simps)
+
+lemma at_begin_norm_Bk[intro]:  "at_begin_norm (as, am) (q, aaa, []) ires
              \<Longrightarrow> at_begin_norm (as, am) (q, aaa, [Bk]) ires"
 apply(simp add: at_begin_norm.simps, erule_tac exE, erule_tac exE)
 apply(rule_tac x = lm1 in exI, simp, auto)
 done
 
-lemma [intro]: "at_begin_fst_bwtn (as, am) (q, aaa, []) ires 
+lemma at_begin_fst_bwtn_Bk[intro]: "at_begin_fst_bwtn (as, am) (q, aaa, []) ires 
             \<Longrightarrow> at_begin_fst_bwtn (as, am) (q, aaa, [Bk]) ires"
 apply(simp only: at_begin_fst_bwtn.simps, erule_tac exE, erule_tac exE, erule_tac exE)
 apply(rule_tac x = "am @ 0\<up>tn" in exI, auto)
 done
 
-lemma [intro]: "at_begin_fst_awtn (as, am) (q, aaa, []) ires
+lemma at_begin_fst_awtn_Bk[intro]: "at_begin_fst_awtn (as, am) (q, aaa, []) ires
            \<Longrightarrow> at_begin_fst_awtn (as, am) (q, aaa, [Bk]) ires"
 apply(auto simp: at_begin_fst_awtn.simps)
 done 
 
-lemma [intro]: "inv_locate_a (as, am) (q, aaa, []) ires
+lemma inv_locate_a_Bk[intro]: "inv_locate_a (as, am) (q, aaa, []) ires
             \<Longrightarrow> inv_locate_a (as, am) (q, aaa, [Bk]) ires"
 apply(simp only: inv_locate_a.simps)
 apply(erule disj_forward)
@@ -1295,22 +1269,15 @@
 apply(case_tac [!] n, simp_all)
 done
 
-lemma [simp]: "(Oc # r = Bk \<up> rn) = False"
+lemma repeat_Bk_no_Oc[simp]: "(Oc # r = Bk \<up> rn) = False"
 apply(case_tac rn, simp_all)
 done
 
-lemma [simp]: "(\<exists>rna. Bk \<up> rn = Bk # Bk \<up> rna) \<or> rn = 0"
+lemma repeat_Bk[simp]: "(\<exists>rna. Bk \<up> rn = Bk # Bk \<up> rna) \<or> rn = 0"
 apply(case_tac rn, auto)
 done
 
-lemma [simp]: "(\<forall> x. a \<noteq> x) = False"
-by auto
-
-lemma exp_ind: "a\<up>(Suc x) = a\<up>x @ [a]"
-apply(induct x, auto)
-done
-
-lemma [simp]: 
+lemma inv_locate_b_Oc_via_a[simp]: 
       "inv_locate_a (as, lm) (q, l, Oc # r) ires
        \<Longrightarrow> inv_locate_b (as, lm) (q, Oc # l, r) ires"
 apply(simp only: inv_locate_a.simps inv_locate_b.simps in_middle.simps
@@ -1334,7 +1301,7 @@
 lemma length_equal: "xs = ys \<Longrightarrow> length xs = length ys"
 by auto
 
-lemma [simp]: "\<lbrakk>inv_locate_b (as, am) (q, aaa, Bk # xs) ires; 
+lemma inv_locate_a_Bk_via_b[simp]: "\<lbrakk>inv_locate_b (as, am) (q, aaa, Bk # xs) ires; 
                 \<not> (\<exists>n. xs = Bk\<up>n)\<rbrakk> 
        \<Longrightarrow> inv_locate_a (as, am) (Suc q, Bk # aaa, xs) ires"
 apply(simp add: inv_locate_b.simps inv_locate_a.simps)
@@ -1359,7 +1326,7 @@
 done
 
 
-lemma [simp]:  "inv_locate_b (as, am) (q, l, []) ires 
+lemma inv_locate_b_Bk[simp]:  "inv_locate_b (as, am) (q, l, []) ires 
            \<Longrightarrow>  inv_locate_b (as, am) (q, l, [Bk]) ires"
 apply(simp only: inv_locate_b.simps in_middle.simps)
 apply(erule exE)+
@@ -1371,68 +1338,31 @@
 
 (*inv: from locate_b to after_write*)
 
-lemma [simp]: "(a mod 2 \<noteq> Suc 0) = (a mod 2 = 0)  "
-by arith
-
-lemma [simp]: "(a mod 2 \<noteq> 0) = (a mod 2 = Suc 0)  "
-by arith
-
-lemma mod_ex1: "(a mod 2 = Suc 0) = (\<exists> q. a = Suc (2 * q))"
-by arith
-
-lemma mod_ex2: "(a mod (2::nat) = 0) = (\<exists> q. a = 2 * q)"
-by arith
-
-lemma [simp]: "(2*q - Suc 0) div 2 = (q - 1)"
-by arith
-
-lemma [simp]: "(Suc (2*q)) div 2 = q"
+lemma not_even_then_odd[simp]: "(a mod 2 \<noteq> 0) = (a mod 2 = Suc 0)  "
 by arith
 
-lemma mod_2: "x mod 2  = 0 \<or>  x mod 2 = Suc 0"
-by arith
-
-lemma [simp]: "x mod 2 = 0 \<Longrightarrow> Suc x mod 2 = Suc 0"
-by arith
-
-lemma [simp]: "x mod 2 = Suc 0 \<Longrightarrow> Suc x mod 2 = 0"
+lemma div_rounding_down[simp]: "(2*q - Suc 0) div 2 = (q - 1)" "(Suc (2*q)) div 2 = q"
+by arith+
+
+lemma even_plus_one_odd[simp]: "x mod 2 = 0 \<Longrightarrow> Suc x mod 2 = Suc 0"
 by arith
 
-lemma [simp]:  "inv_locate_b (as, am) (q, l, []) ires 
-           \<Longrightarrow>  inv_locate_b (as, am) (q, l, [Bk]) ires"
-apply(simp only: inv_locate_b.simps in_middle.simps)
-apply(erule exE)+
-apply(rule_tac x = lm1 in exI, rule_tac x = lm2 in exI, 
-      rule_tac x = tn in exI, rule_tac x = m in exI, 
-      rule_tac x = ml in exI, rule_tac x = mr in exI)
-apply(auto)
-done
+lemma odd_plus_one_even[simp]: "x mod 2 = Suc 0 \<Longrightarrow> Suc x mod 2 = 0"
+by arith
 
 lemma locate_b_2_locate_a[simp]: 
     "\<lbrakk>q > 0;  inv_locate_b (as, am) (q - Suc 0, aaa, Bk # xs) ires\<rbrakk>
    \<Longrightarrow>  inv_locate_a (as, am) (q, Bk # aaa, xs) ires"
 apply(insert locate_b_2_a [of as am "q - 1" aaa xs ires], simp)
-done
-
-
-lemma [simp]:  "inv_locate_b (as, am) (q, l, []) ires 
-           \<Longrightarrow>  inv_locate_b (as, am) (q, l, [Bk]) ires"
-apply(simp only: inv_locate_b.simps in_middle.simps)
-apply(erule exE)+
-apply(rule_tac x = lm1 in exI, rule_tac x = lm2 in exI, 
-      rule_tac x = tn in exI, rule_tac x = m in exI, 
-      rule_tac x = ml in exI, rule_tac x = mr in exI)
-apply(auto)
-done
+  done
 
 (*inv: from locate_b to after_write*)
 
-lemma [simp]:
+lemma findnth_inv_layout_of_via_crsp[simp]:
   "crsp (layout_of ap) (as, lm) (s, l, r) ires
   \<Longrightarrow> findnth_inv (layout_of ap) n (as, lm) (Suc 0, l, r) ires"
-apply(auto simp: crsp.simps findnth_inv.simps inv_locate_a.simps
+by(auto simp: crsp.simps findnth_inv.simps inv_locate_a.simps
                at_begin_norm.simps at_begin_fst_awtn.simps at_begin_fst_bwtn.simps)
-done
 
 lemma findnth_correct_pre: 
   assumes layout: "ly = layout_of ap"
@@ -1470,10 +1400,11 @@
   qed
 qed
             
-lemma [intro]: "inv_locate_a (as, lm) (0, Bk # Bk # ires, <lm> @ Bk \<up> x) ires"
+lemma inv_locate_aI[intro]: "inv_locate_a (as, lm) (0, Bk # Bk # ires, <lm> @ Bk \<up> x) ires"
 apply(auto simp: crsp.simps inv_locate_a.simps at_begin_norm.simps)
 done
-lemma [simp]: "crsp ly (as, lm) (s, l, r) ires \<Longrightarrow> inv_locate_a (as, lm) (0, l, r) ires"
+lemma inv_locate_a_via_crsp[simp]:
+ "crsp ly (as, lm) (s, l, r) ires \<Longrightarrow> inv_locate_a (as, lm) (0, l, r) ires"
 apply(auto simp: crsp.simps inv_locate_a.simps at_begin_norm.simps)
 done
 
@@ -1578,24 +1509,6 @@
 lemma wf_inc_le[intro]: "wf inc_LE"
 by(auto intro:wf_inv_image simp: inc_LE_def lex_triple_def lex_pair_def)
 
-lemma numeral_5_eq_5: "5 = Suc (Suc (Suc (Suc (Suc 0))))"
-by arith
-
-lemma numeral_6_eq_6: "6 = Suc (Suc (Suc (Suc (Suc 1))))"
-by arith
-
-lemma numeral_7_eq_7: "7 = Suc (Suc (Suc (Suc (Suc 2))))"
-by arith
-
-lemma numeral_8_eq_8: "8 = Suc (Suc (Suc (Suc (Suc 3))))"
-by arith
-
-lemma numeral_9_eq_9: "9 = Suc (Suc (Suc (Suc (Suc (Suc 3)))))"
-by arith
-
-lemma numeral_10_eq_10: "10 = Suc (Suc (Suc (Suc (Suc (Suc (Suc 3))))))"
-by arith
-
 lemma inv_locate_b_2_after_write[simp]: 
       "inv_locate_b (as, am) (n, aaa, Bk # xs) ires
       \<Longrightarrow> inv_after_write (as, abc_lm_s am n (Suc (abc_lm_v am n)))
@@ -1611,7 +1524,7 @@
   apply(drule_tac length_equal, simp)
   by (metis (no_types, lifting) add_diff_inverse_nat append.assoc append_eq_append_conv length_append length_replicate list.inject)
 
-lemma [simp]: "inv_locate_b (as, am) (n, aaa, []) ires \<Longrightarrow> 
+lemma inv_after_write_via_locate_b[simp]: "inv_locate_b (as, am) (n, aaa, []) ires \<Longrightarrow> 
      inv_after_write (as, abc_lm_s am n (Suc (abc_lm_v am n))) 
                      (s, aaa, [Oc]) ires"
 apply(insert inv_locate_b_2_after_write [of as am n aaa "[]"])
@@ -1620,52 +1533,49 @@
 
 
 (*inv: from after_write to after_move*)
-lemma [simp]: "inv_after_write (as, lm) (x, l, Oc # r) ires
+lemma inv_after_move_Oc_via_write[simp]: "inv_after_write (as, lm) (x, l, Oc # r) ires
                 \<Longrightarrow> inv_after_move (as, lm) (y, Oc # l, r) ires"
 apply(auto simp:inv_after_move.simps inv_after_write.simps split: if_splits)
 done
 
-lemma [simp]: "inv_after_write (as, abc_lm_s am n (Suc (abc_lm_v am n)
+lemma inv_after_write_Suc[simp]: "inv_after_write (as, abc_lm_s am n (Suc (abc_lm_v am n)
                 )) (x, aaa, Bk # xs) ires = False"
-apply(simp add: inv_after_write.simps )
-done
-
-lemma [simp]: 
  "inv_after_write (as, abc_lm_s am n (Suc (abc_lm_v am n))) 
                         (x, aaa, []) ires = False"
-apply(simp add: inv_after_write.simps )
+apply(auto simp: inv_after_write.simps )
 done
 
 (*inv: from after_move to after_clear*)
-lemma [simp]: "inv_after_move (as, lm) (s, l, Oc # r) ires
+lemma inv_after_clear_Bk_via_Oc[simp]: "inv_after_move (as, lm) (s, l, Oc # r) ires
                 \<Longrightarrow> inv_after_clear (as, lm) (s', l, Bk # r) ires"
 apply(auto simp: inv_after_move.simps inv_after_clear.simps split: if_splits)
 done
 
-(*inv: from after_move to on_leftmoving*)
-lemma [intro]: "Bk \<up> rn = Bk # Bk \<up> (rn - Suc 0) \<or> rn = 0"
-apply(case_tac rn, auto)
-done
 
 lemma inv_after_move_2_inv_on_left_moving[simp]:  
-   "inv_after_move (as, lm) (s, l, Bk # r) ires
-   \<Longrightarrow> (l = [] \<longrightarrow> 
+  assumes "inv_after_move (as, lm) (s, l, Bk # r) ires"
+  shows "(l = [] \<longrightarrow> 
          inv_on_left_moving (as, lm) (s', [], Bk # Bk # r) ires) \<and>
       (l \<noteq> [] \<longrightarrow> 
          inv_on_left_moving (as, lm) (s', tl l, hd l # Bk # r) ires)"
-apply(simp only: inv_after_move.simps inv_on_left_moving.simps)
-apply(subgoal_tac "l \<noteq> []", rule conjI, simp, rule impI, 
-                rule disjI1, simp only: inv_on_left_moving_norm.simps)
-apply(erule exE)+
-apply(subgoal_tac "lm2 = []")
-apply(rule_tac x = lm1 in exI, rule_tac x = lm2 in exI,  
-    rule_tac x = m in exI, rule_tac x = m in exI, 
-    rule_tac x = 1 in exI,  
-    rule_tac x = "rn - 1" in exI, auto)
-apply(auto split: if_splits)
-apply(case_tac [1-2] rn, simp_all)
-apply(case_tac [!] lm2, simp_all add: tape_of_nl_cons split: if_splits)
-done
+proof (cases l)
+  case (Cons a list)
+  from assms Cons show ?thesis
+    apply(simp only: inv_after_move.simps inv_on_left_moving.simps)
+    apply(rule conjI, force, rule impI, rule disjI1, simp only: inv_on_left_moving_norm.simps)
+    apply(erule exE)+
+    apply(subgoal_tac "lm2 = []")
+    apply(rule_tac x = lm1 in exI, rule_tac x = lm2 in exI,  
+        rule_tac x = m in exI, rule_tac x = m in exI, 
+        rule_tac x = 1 in exI,  
+        rule_tac x = "rn - 1" in exI) apply (auto split:if_splits)
+    apply(case_tac [1-2] rn, simp_all)
+    by(case_tac [!] lm2, simp_all add: tape_of_nl_cons split: if_splits)
+next
+  case Nil thus ?thesis using assms
+    unfolding inv_after_move.simps inv_on_left_moving.simps
+    by (auto split:if_splits)
+qed
 
 
 lemma inv_after_move_2_inv_on_left_moving_B[simp]: 
@@ -1684,11 +1594,6 @@
 apply(case_tac [!] lm2, auto simp: tape_of_nl_cons split: if_splits)
 done
 
-(*inv: from after_clear to on_right_moving*)
-lemma [simp]: "Oc # r = replicate rn Bk = False"
-apply(case_tac rn, simp, simp)
-done
-
 lemma inv_after_clear_2_inv_on_right_moving[simp]: 
      "inv_after_clear (as, lm) (x, l, Bk # r) ires
       \<Longrightarrow> inv_on_right_moving (as, lm) (y, Bk # l, r) ires"
@@ -1703,17 +1608,17 @@
 apply(case_tac [!] rn, simp_all)
 done
 
-lemma [simp]: "inv_after_clear (as, lm) (x, l, []) ires\<Longrightarrow> 
+lemma inv_after_clear_singleton_Bk[simp]: "inv_after_clear (as, lm) (x, l, []) ires\<Longrightarrow> 
                inv_after_clear (as, lm) (y, l, [Bk]) ires" 
 by(auto simp: inv_after_clear.simps)
 
-lemma [simp]: "inv_after_clear (as, lm) (x, l, []) ires
+lemma inv_on_right_moving_Bk[simp]: "inv_after_clear (as, lm) (x, l, []) ires
              \<Longrightarrow> inv_on_right_moving (as, lm) (y, Bk # l, []) ires"
 by(insert 
     inv_after_clear_2_inv_on_right_moving[of as lm n l "[]"], simp)
 
 (*inv: from on_right_moving to on_right_movign*)
-lemma [simp]: "inv_on_right_moving (as, lm) (x, l, Oc # r) ires
+lemma inv_on_right_moving_Oc[simp]: "inv_on_right_moving (as, lm) (x, l, Oc # r) ires
       \<Longrightarrow> inv_on_right_moving (as, lm) (y, Oc # l, r) ires"
 apply(auto simp: inv_on_right_moving.simps)
 apply(rule_tac x = lm1 in exI, rule_tac x = lm2 in exI, 
@@ -1735,31 +1640,31 @@
 apply(case_tac mr, auto simp: split: if_splits)
 done
       
-lemma [simp]: "inv_on_right_moving (as, lm) (x, l, []) ires\<Longrightarrow> 
+lemma inv_on_right_moving_singleton_Bk[simp]: "inv_on_right_moving (as, lm) (x, l, []) ires\<Longrightarrow> 
              inv_on_right_moving (as, lm) (y, l, [Bk]) ires"
 apply(auto simp: inv_on_right_moving.simps)
 apply(rule_tac x = lm1 in exI, rule_tac x = "[]" in exI, simp)
 done
 
 (*inv: from on_right_moving to after_write*)
-lemma [simp]: "inv_on_right_moving (as, lm) (x, l, []) ires
+lemma inv_after_write_singleton_Oc[simp]: "inv_on_right_moving (as, lm) (x, l, []) ires
        \<Longrightarrow> inv_after_write (as, lm) (y, l, [Oc]) ires"
 apply(rule_tac inv_on_right_moving_2_inv_on_right_moving, simp)
 done
 
 (*inv: from on_left_moving to on_left_moving*)
-lemma [simp]: "inv_on_left_moving_in_middle_B (as, lm) 
+lemma no_inv_on_left_moving_in_middle_B_Oc[simp]: "inv_on_left_moving_in_middle_B (as, lm) 
                (s, l, Oc # r) ires = False"
 apply(auto simp: inv_on_left_moving_in_middle_B.simps )
 done
 
-lemma [simp]: "inv_on_left_moving_norm (as, lm) (s, l, Bk # r) ires 
+lemma no_inv_on_left_moving_norm_Bk[simp]: "inv_on_left_moving_norm (as, lm) (s, l, Bk # r) ires 
              = False"
 apply(auto simp: inv_on_left_moving_norm.simps)
 apply(case_tac [!] mr, auto simp: )
 done
 
-lemma [simp]: 
+lemma inv_on_left_moving_in_middle_B_Bk[simp]: 
   "\<lbrakk>inv_on_left_moving_norm (as, lm) (s, l, Oc # r) ires;
     hd l = Bk; l \<noteq> []\<rbrakk> \<Longrightarrow> 
      inv_on_left_moving_in_middle_B (as, lm) (s, tl l, Bk # Oc # r) ires"
@@ -1773,7 +1678,7 @@
 apply(rule_tac [!] x = "Suc rn" in exI, simp_all)
 done
 
-lemma [simp]: "\<lbrakk>inv_on_left_moving_norm (as, lm) (s, l, Oc # r) ires; 
+lemma inv_on_left_moving_norm_Oc_Oc[simp]: "\<lbrakk>inv_on_left_moving_norm (as, lm) (s, l, Oc # r) ires; 
                 hd l = Oc; l \<noteq> []\<rbrakk>
             \<Longrightarrow> inv_on_left_moving_norm (as, lm) 
                                         (s, tl l, Oc # Oc # r) ires"
@@ -1785,13 +1690,13 @@
 apply(case_tac ml, auto simp: split: if_splits)
 done
 
-lemma [simp]: "inv_on_left_moving_norm (as, lm) (s, [], Oc # r) ires
+lemma inv_on_left_moving_in_middle_B_Bk_Oc[simp]: "inv_on_left_moving_norm (as, lm) (s, [], Oc # r) ires
      \<Longrightarrow> inv_on_left_moving_in_middle_B (as, lm) (s, [], Bk # Oc # r) ires"
 apply(auto simp: inv_on_left_moving_norm.simps 
                  inv_on_left_moving_in_middle_B.simps split: if_splits)
 done
 
-lemma [simp]:"inv_on_left_moving (as, lm) (s, l, Oc # r) ires
+lemma inv_on_left_moving_Oc_cases[simp]:"inv_on_left_moving (as, lm) (s, l, Oc # r) ires
     \<Longrightarrow> (l = [] \<longrightarrow> inv_on_left_moving (as, lm) (s, [], Bk # Oc # r) ires)
  \<and>  (l \<noteq> [] \<longrightarrow> inv_on_left_moving (as, lm) (s, tl l, hd l # Oc # r) ires)"
 apply(simp add: inv_on_left_moving.simps)
@@ -1809,22 +1714,22 @@
 apply(case_tac [!] lista, simp_all add: tape_of_nat_def tape_of_list_def)
 done
 
-lemma [simp]:
+lemma inv_check_left_moving_in_middle_no_Bk[simp]:
     "inv_check_left_moving_in_middle (as, lm) (s, l, Bk # r) ires= False"
 by(auto simp: inv_check_left_moving_in_middle.simps )
 
-lemma [simp]: 
+lemma inv_check_left_moving_on_leftmost_Bk_Bk[simp]: 
  "inv_on_left_moving_in_middle_B (as, lm) (s, [], Bk # r) ires\<Longrightarrow> 
   inv_check_left_moving_on_leftmost (as, lm) (s', [], Bk # Bk # r) ires"
 apply(auto simp: inv_on_left_moving_in_middle_B.simps 
                  inv_check_left_moving_on_leftmost.simps split: if_splits)
 done
 
-lemma [simp]: "inv_check_left_moving_on_leftmost (as, lm) 
+lemma inv_check_left_moving_on_leftmost_no_Oc[simp]: "inv_check_left_moving_on_leftmost (as, lm) 
                                        (s, list, Oc # r) ires= False"
 by(auto simp: inv_check_left_moving_on_leftmost.simps split: if_splits)
 
-lemma [simp]: "inv_on_left_moving_in_middle_B (as, lm) 
+lemma inv_check_left_moving_in_middle_Oc_Bk[simp]: "inv_on_left_moving_in_middle_B (as, lm) 
                                          (s, Oc # list, Bk # r) ires
  \<Longrightarrow> inv_check_left_moving_in_middle (as, lm) (s', list, Oc # Bk # r) ires"
 apply(auto simp: inv_on_left_moving_in_middle_B.simps 
@@ -1841,53 +1746,53 @@
 apply(case_tac a, simp, simp)
 done
 
-lemma [simp]: "inv_on_left_moving_norm (as, lm) (s, l, []) ires = False"
+lemma inv_on_left_moving_norm_no_empty[simp]: "inv_on_left_moving_norm (as, lm) (s, l, []) ires = False"
 apply(auto simp: inv_on_left_moving_norm.simps)
 done
 
-lemma [simp]: "inv_on_left_moving (as, lm) (s, l, []) ires\<Longrightarrow> 
+lemma inv_on_left_moving_Bk[simp]: "inv_on_left_moving (as, lm) (s, l, []) ires\<Longrightarrow> 
      inv_on_left_moving (as, lm) (6 + 2 * n, l, [Bk]) ires"
 apply(simp add: inv_on_left_moving.simps)
 apply(auto simp: inv_on_left_moving_in_middle_B.simps)
 done
 
-lemma [simp]: "inv_on_left_moving (as, lm) (s, l, []) ires = False"
+lemma inv_on_left_moving_no_empty[simp]: "inv_on_left_moving (as, lm) (s, l, []) ires = False"
 apply(simp add: inv_on_left_moving.simps)
 apply(simp add: inv_on_left_moving_in_middle_B.simps)
 done
 
-lemma [simp]: "inv_on_left_moving (as, lm) (s, l, []) ires
+lemma inv_on_left_moving_cases_left[simp]: "inv_on_left_moving (as, lm) (s, l, []) ires
  \<Longrightarrow> (l = [] \<longrightarrow> inv_check_left_moving (as, lm) (s', [], [Bk]) ires) \<and>
     (l \<noteq> [] \<longrightarrow> inv_check_left_moving (as, lm) (s', tl l, [hd l]) ires)"
 by simp
 
-lemma [intro]: "\<exists>rna. Bk # Bk \<up> rn = Bk \<up> rna"
-apply(rule_tac x = "Suc rn" in exI, simp)
-done
+lemma Bk_plus_one[intro]: "\<exists>rna. Bk # Bk \<up> rn = Bk \<up> rna"
+  apply(rule_tac x = "Suc rn" in exI, simp)
+  done
 
 lemma 
 inv_check_left_moving_in_middle_2_on_left_moving_in_middle_B[simp]:
-"inv_check_left_moving_in_middle (as, lm) (s, Bk # list, Oc # r) ires
-  \<Longrightarrow> inv_on_left_moving_in_middle_B (as, lm) (s', list, Bk # Oc # r) ires"
-apply(simp only: inv_check_left_moving_in_middle.simps 
-                 inv_on_left_moving_in_middle_B.simps)
-apply(erule_tac exE)+
-apply(rule_tac x = "rev (tl (rev lm1))" in exI, 
-      rule_tac x = "[hd (rev lm1)] @ lm2" in exI, auto)
-apply(case_tac [!] "rev lm1",simp_all add: tape_of_nat_def tape_of_list_def tape_of_nat_list.simps)
-apply(case_tac [!] a, simp_all)
-apply(case_tac [1] lm2, auto simp:tape_of_nat_def)
-apply(case_tac [3] lm2, auto simp:tape_of_nat_def)
-apply(case_tac [!] lista, simp_all add: tape_of_nat_def)
-done
-
-lemma [simp]: 
+assumes "inv_check_left_moving_in_middle (as, lm) (s, Bk # list, Oc # r) ires"
+shows "inv_on_left_moving_in_middle_B (as, lm) (s', list, Bk # Oc # r) ires"
+  using assms
+  apply(simp only: inv_check_left_moving_in_middle.simps 
+                   inv_on_left_moving_in_middle_B.simps)
+  apply(erule_tac exE)+
+  apply(rule_tac x = "rev (tl (rev lm1))" in exI, 
+        rule_tac x = "[hd (rev lm1)] @ lm2" in exI, auto)
+  apply(case_tac [!] "rev lm1",simp_all add: tape_of_nat_def tape_of_list_def tape_of_nat_list.simps)
+  apply(case_tac [!] a, simp_all)
+  apply(case_tac [1] lm2, auto simp:tape_of_nat_def)
+  apply(case_tac [3] lm2, auto simp:tape_of_nat_def)
+  apply(case_tac [!] lista, simp_all add: tape_of_nat_def)
+        done
+
+lemma inv_check_left_moving_in_middle_Bk_Oc[simp]: 
  "inv_check_left_moving_in_middle (as, lm) (s, [], Oc # r) ires\<Longrightarrow>
      inv_check_left_moving_in_middle (as, lm) (s', [Bk], Oc # r) ires"
 apply(auto simp: inv_check_left_moving_in_middle.simps )
 done
-
-lemma [simp]: 
+lemma inv_on_left_moving_in_middle_B_Bk_Oc_via_check[simp]: 
  "inv_check_left_moving_in_middle (as, lm) (s, [], Oc # r) ires
    \<Longrightarrow> inv_on_left_moving_in_middle_B (as, lm) (s', [], Bk # Oc # r) ires"
 apply(insert 
@@ -1895,7 +1800,7 @@
                   as lm n "[]" r], simp)
 done 
 
-lemma [simp]: "inv_check_left_moving_in_middle (as, lm) 
+lemma inv_on_left_moving_norm_Oc_Oc_via_middle[simp]: "inv_check_left_moving_in_middle (as, lm) 
                        (s, Oc # list, Oc # r) ires
    \<Longrightarrow> inv_on_left_moving_norm (as, lm) (s', list, Oc # Oc # r) ires"
 apply(auto simp: inv_check_left_moving_in_middle.simps 
@@ -1910,7 +1815,7 @@
 apply(case_tac [!] a, simp_all add: tape_of_nl_cons split: if_splits)
 done
 
-lemma [simp]: "inv_check_left_moving (as, lm) (s, l, Oc # r) ires
+lemma inv_check_left_moving_Oc_cases[simp]: "inv_check_left_moving (as, lm) (s, l, Oc # r) ires
 \<Longrightarrow> (l = [] \<longrightarrow> inv_on_left_moving (as, lm) (s', [], Bk # Oc # r) ires) \<and>
    (l \<noteq> [] \<longrightarrow> inv_on_left_moving (as, lm) (s', tl l, hd l # Oc # r) ires)"
 apply(case_tac l, 
@@ -1919,58 +1824,57 @@
 done
 
 (*inv: check_left_moving to after_left_moving*)
-lemma [simp]: "inv_check_left_moving (as, lm) (s, l, Bk # r) ires
+lemma inv_after_left_moving_Bk_via_check[simp]: "inv_check_left_moving (as, lm) (s, l, Bk # r) ires
                 \<Longrightarrow> inv_after_left_moving (as, lm) (s', Bk # l, r) ires"
 apply(auto simp: inv_check_left_moving.simps 
  inv_check_left_moving_on_leftmost.simps inv_after_left_moving.simps)
 done
 
 
-lemma [simp]:"inv_check_left_moving (as, lm) (s, l, []) ires
+lemma inv_after_left_moving_Bk_empty_via_check[simp]:"inv_check_left_moving (as, lm) (s, l, []) ires
       \<Longrightarrow> inv_after_left_moving (as, lm) (s', Bk # l, []) ires"
 by(simp add: inv_check_left_moving.simps  
 inv_check_left_moving_in_middle.simps 
 inv_check_left_moving_on_leftmost.simps)
 
 (*inv: after_left_moving to inv_stop*)
-lemma [simp]: "inv_after_left_moving (as, lm) (s, l, Bk # r) ires
+lemma inv_stop_Bk_move[simp]: "inv_after_left_moving (as, lm) (s, l, Bk # r) ires
        \<Longrightarrow> inv_stop (as, lm) (s', Bk # l, r) ires"
 apply(auto simp: inv_after_left_moving.simps inv_stop.simps)
 done
 
-lemma [simp]: "inv_after_left_moving (as, lm) (s, l, []) ires
+lemma inv_stop_Bk_empty[simp]: "inv_after_left_moving (as, lm) (s, l, []) ires
              \<Longrightarrow> inv_stop (as, lm) (s', Bk # l, []) ires"
 by(auto simp: inv_after_left_moving.simps)
 
 (*inv: stop to stop*)
-lemma [simp]: "inv_stop (as, lm) (x, l, r) ires \<Longrightarrow> 
+lemma inv_stop_indep_fst[simp]: "inv_stop (as, lm) (x, l, r) ires \<Longrightarrow> 
                inv_stop (as, lm) (y, l, r) ires"
 apply(simp add: inv_stop.simps)
 done
 
-lemma [simp]: "inv_after_clear (as, lm) (s, aaa, Oc # xs) ires= False"
+lemma inv_after_clear_no_Oc[simp]: "inv_after_clear (as, lm) (s, aaa, Oc # xs) ires= False"
 apply(auto simp: inv_after_clear.simps )
 done
 
-lemma [simp]: 
+lemma inv_after_left_moving_no_Oc[simp]: 
   "inv_after_left_moving (as, lm) (s, aaa, Oc # xs) ires = False"
 by(auto simp: inv_after_left_moving.simps  )
 
-lemma [simp]: "inv_after_clear (as, abc_lm_s lm n (Suc (abc_lm_v lm n))) (s, b, []) ires = False"
+lemma inv_after_clear_Suc_nonempty[simp]:
+  "inv_after_clear (as, abc_lm_s lm n (Suc (abc_lm_v lm n))) (s, b, []) ires = False"
 apply(auto simp: inv_after_clear.simps)
 done
 
-lemma [simp]: "inv_on_left_moving (as, abc_lm_s lm n (Suc (abc_lm_v lm n))) 
+lemma inv_on_left_moving_Suc_nonempty[simp]: "inv_on_left_moving (as, abc_lm_s lm n (Suc (abc_lm_v lm n))) 
            (s, b, Oc # list) ires \<Longrightarrow> b \<noteq> []"
 apply(auto simp: inv_on_left_moving.simps inv_on_left_moving_norm.simps split: if_splits)
 done
 
-lemma [simp]: "inv_check_left_moving (as, abc_lm_s lm n (Suc (abc_lm_v lm n))) (s, b, Oc # list) ires \<Longrightarrow> b \<noteq> []"
+lemma inv_check_left_moving_Suc_nonempty[simp]:
+  "inv_check_left_moving (as, abc_lm_s lm n (Suc (abc_lm_v lm n))) (s, b, Oc # list) ires \<Longrightarrow> b \<noteq> []"
 apply(auto simp: inv_check_left_moving.simps inv_check_left_moving_in_middle.simps split: if_splits)
-done
-
-lemma numeral_4_eq_4: "4 =  Suc (Suc (Suc (Suc 0)))"
-by arith
+  done
 
 lemma tinc_correct_pre:
   assumes layout: "ly = layout_of ap"
@@ -2003,12 +1907,12 @@
       apply(simp add: inc_inv.simps)
       apply(case_tac c, case_tac [2] aa)
       apply(auto simp: Let_def step.simps tinc_b_def split: if_splits)
-      apply(simp_all add: inc_inv.simps inc_LE_def lex_triple_def lex_pair_def inc_measure_def numeral_5_eq_5 numeral_2_eq_2 numeral_3_eq_3
-                          numeral_4_eq_4 numeral_6_eq_6 numeral_7_eq_7 numeral_8_eq_8 numeral_9_eq_9)         
+      apply(simp_all add: inc_inv.simps inc_LE_def lex_triple_def lex_pair_def inc_measure_def 
+                          numeral)         
       done
   qed
 qed
-         
+
 lemma tinc_correct: 
   assumes layout: "ly = layout_of ap"
   and inv_start: "inv_locate_a (as, lm) (n, l, r) ires"
@@ -2024,7 +1928,7 @@
 declare inv_locate_a.simps[simp del] abc_lm_s.simps[simp del]
         abc_lm_v.simps[simp del]
 
-lemma [simp]: "(4::nat) * n mod 2 = 0"
+lemma is_even_4[simp]: "(4::nat) * n mod 2 = 0"
 apply(arith)
 done
 
@@ -2194,19 +2098,62 @@
               else False)"
 
 declare fetch.simps[simp del]
-lemma [simp]:
+
+
+lemma x_plus_helpers:
+  "x + 4 = Suc (x + 3)"
+  "x + 5 = Suc (x + 4)"
+  "x + 6 = Suc (x + 5)"
+  "x + 7 = Suc (x + 6)"
+  "x + 8 = Suc (x + 7)"
+  "x + 9 = Suc (x + 8)"
+  "x + 10 = Suc (x + 9)"
+  "x + 11 = Suc (x + 10)"
+  "x + 12 = Suc (x + 11)"
+  "x + 13 = Suc (x + 12)"
+  "14 + x = Suc (x + 13)"
+  "15 + x = Suc (x + 14)"
+  "16 + x = Suc (x + 15)"
+  by auto
+
+lemma fetch_Dec[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 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 adjust.simps shift.simps tdec_b_def)
-done
-
-lemma [simp]: 
+  "fetch (ci (ly) (start_of ly as) (Dec n e)) (Suc (Suc (2 * n))) Oc
+     = (R, start_of ly as + 2*n + 2)"
+  "fetch (ci (ly) (start_of ly as) (Dec n e)) (Suc (Suc (2 * n))) Bk
+     = (L, start_of ly as + 2*n + 13)"
+  "fetch (ci (ly) (start_of ly as) (Dec n e)) (Suc (Suc (Suc (2 * n)))) Oc
+     = (R, start_of ly as + 2*n + 2)"
+  "fetch (ci (ly) (start_of ly as) (Dec n e)) (Suc (Suc (Suc (2 * n)))) Bk
+     = (L, start_of ly as + 2*n + 3)"
+  "fetch (ci (ly) (start_of ly as) (Dec n e)) (2 * n + 4) Oc = (W0, start_of ly as + 2*n + 3)"
+  "fetch (ci (ly) (start_of ly as) (Dec n e)) (2 * n + 4) Bk = (R, start_of ly as + 2*n + 4)"
+  "fetch (ci (ly) (start_of ly as) (Dec n e)) (2 * n + 5) Bk = (R, start_of ly as + 2*n + 5)"
+  "fetch (ci (ly) (start_of ly as) (Dec n e)) (2 * n + 6) Bk = (L, start_of ly as + 2*n + 6)"
+  "fetch (ci (ly) (start_of ly as) (Dec n e)) (2 * n + 6) Oc = (L, start_of ly as + 2*n + 7)"
+  "fetch (ci (ly) (start_of ly as) (Dec n e)) (2 * n + 7) Bk = (L, start_of ly as + 2*n + 10)"
+  "fetch (ci (ly) (start_of ly as) (Dec n e)) (2 * n + 8) Bk = (W1, start_of ly as + 2*n + 7)"
+  "fetch (ci (ly) (start_of ly as) (Dec n e)) (2 * n + 8) Oc = (R, start_of ly as + 2*n + 8)"
+  "fetch (ci (ly) (start_of ly as) (Dec n e)) (2 * n + 9) Bk = (L, start_of ly as + 2*n + 9)"
+  "fetch (ci (ly) (start_of ly as) (Dec n e)) (2 * n + 9) Oc = (R, start_of ly as + 2*n + 8)"
+  "fetch (ci (ly) (start_of ly as) (Dec n e)) (2 * n + 10) Bk = (R, start_of ly as + 2*n + 4)"
+  "fetch (ci (ly) (start_of ly as) (Dec n e)) (2 * n + 10) Oc = (W0, start_of ly as + 2*n + 9)"
+  "fetch (ci (ly) (start_of ly as) (Dec n e)) (2 * n + 11) Oc = (L, start_of ly as + 2*n + 10)"
+  "fetch (ci (ly) (start_of ly as) (Dec n e)) (2 * n + 11) Bk = (L, start_of ly as + 2*n + 11)"
+  "fetch (ci (ly) (start_of ly as) (Dec n e)) (2 * n + 12) Oc = (L, start_of ly as + 2*n + 10)"
+  "fetch (ci (ly) (start_of ly as) (Dec n e)) (2 * n + 12) Bk = (R, start_of ly as + 2*n + 12)"
+  "fetch (ci (ly) (start_of ly as) (Dec n e)) (2 * n + 13) Bk = (R, start_of ly as + 2*n + 16)"
+  "fetch (ci (ly) (start_of ly as) (Dec n e)) (14 + 2 * n) Oc = (L, start_of ly as + 2*n + 13)"
+  "fetch (ci (ly) (start_of ly as) (Dec n e)) (14 + 2 * n) Bk = (L, start_of ly as + 2*n + 14)"
+  "fetch (ci (ly) (start_of ly as) (Dec n e)) (15 + 2 * n) Oc = (L, start_of ly as + 2*n + 13)"
+  "fetch (ci (ly) (start_of ly as) (Dec n e)) (15 + 2 * n) Bk = (R, start_of ly as + 2*n + 15)"
+  "fetch (ci (ly) (start_of (ly) as) (Dec n e)) (16 + 2 * n) Bk = (R, start_of (ly) e)"
+  unfolding x_plus_helpers fetch.simps
+  by(auto simp: ci.simps findnth.simps 
+                  nth_of.simps shift.simps nth_append tdec_b_def length_findnth adjust.simps)
+
+lemma steps_start_of_invb_inv_locate_a1[simp]: 
   "\<lbrakk>r = [] \<or> hd r = Bk; inv_locate_a (as, lm) (n, l, r) ires\<rbrakk>
     \<Longrightarrow> \<exists>stp la ra.
   steps (start_of ly as + 2 * n, l, r) (ci ly (start_of ly as) (Dec n e), 
@@ -2217,7 +2164,7 @@
 apply(case_tac r, simp_all)
 done
 
-lemma [simp]: 
+lemma steps_start_of_invb_inv_locate_a2[simp]: 
   "\<lbrakk>inv_locate_a (as, lm) (n, l, r) ires; r \<noteq> [] \<and> hd r \<noteq> Bk\<rbrakk>
     \<Longrightarrow> \<exists>stp la ra.
   steps (start_of ly as + 2 * n, l, r) (ci ly (start_of ly as) (Dec n e), 
@@ -2333,278 +2280,32 @@
     by arith
 qed
     
-lemma [elim]: "\<lbrakk>abc_fetch as ap = Some (Dec n e); as < e; 
+lemma abc_fetch_contrE[elim]: "\<lbrakk>abc_fetch as ap = Some (Dec n e); as < e; 
   Suc (start_of (layout_of ap) as + 2 * n) = start_of (layout_of ap) e\<rbrakk> \<Longrightarrow> RR"
-apply(drule_tac start_of_ge, simp_all)
-apply(auto)
-done
-
-lemma [elim]: "\<lbrakk>abc_fetch as ap = Some (Dec n e); as > e;
+  by(drule_tac start_of_ge, auto)
+
+lemma abc_fetch_contrE2[elim]: "\<lbrakk>abc_fetch as ap = Some (Dec n e); as > e;
   Suc (start_of (layout_of ap) as + 2 * n) = start_of (layout_of ap) e\<rbrakk> \<Longrightarrow> RR"
 apply(drule_tac ly = "layout_of ap" in start_of_less[of])
 apply(arith)
 done
 
-lemma [elim]: "\<lbrakk>abc_fetch as ap = Some (Dec n e);
+lemma abc_fetch_contrE3[elim]: "\<lbrakk>abc_fetch as ap = Some (Dec n e);
   Suc (start_of (layout_of ap) as + 2 * n) = start_of (layout_of ap) e\<rbrakk> \<Longrightarrow> RR"
 apply(subgoal_tac "as = e \<or> as < e \<or> as > e", auto)
 done
 
-lemma [simp]:"fetch (ci (ly) (start_of ly as) (Dec n e)) (Suc (2 * n))  Oc
+lemma fetch_c_Oc[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 adjust.simps)
 done
 
-lemma [simp]: "(start_of ly as = 0) = False"
-apply(simp add: start_of.simps)
-done
-
-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: ci.simps findnth.simps fetch.simps
-                  nth_of.simps shift.simps nth_append tdec_b_def length_findnth adjust.simps)
-done
-
-lemma [simp]: 
-  "fetch (ci (ly) 
-                (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 adjust.simps)
-done
-
-
-lemma [simp]: "fetch (ci (ly) 
-                  (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 adjust.simps)
-done
-
-
-lemma [simp]: "fetch (ci (ly) 
-             (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 adjust.simps)
-done
-
-
-lemma [simp]: "fetch (ci (ly) (start_of ly as) (Dec n e)) 
-                             (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 adjust.simps)
-done
-
-lemma [simp]:
-     "fetch (ci (ly) 
-                      (start_of ly as) (Dec n e)) (2 * n + 4) Oc
-    = (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 adjust.simps)
-done
-
-lemma [simp]: "fetch (ci (ly) 
-                   (start_of ly as) (Dec n e)) (2 * n + 4) Bk
-    = (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 adjust.simps)
-done
-
-lemma [simp]:"fetch (ci (ly) 
-                          (start_of ly as) (Dec n e)) (2 * n + 5) Bk
-    = (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 adjust.simps)
-done
-
-
-lemma [simp]: 
-  "fetch (ci (ly)
-                (start_of ly as) (Dec n e)) (2 * n + 6) Bk
-    = (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 adjust.simps)
-done
-
-lemma [simp]: 
-  "fetch (ci (ly) (start_of ly as) 
-                      (Dec n e)) (2 * n + 6) Oc
-    = (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 adjust.simps)
-done
-
-lemma [simp]:"fetch (ci (ly) 
-             (start_of ly as) (Dec n e)) (2 * n + 7) Bk
-    = (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 adjust.simps)
-done
-
-lemma [simp]:
-  "fetch (ci (ly) 
-                   (start_of ly as) (Dec n e)) (2 * n + 8) Bk
-    = (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 adjust.simps)
-done
-
-
-lemma [simp]: 
-  "fetch (ci (ly) 
-                   (start_of ly as) (Dec n e)) (2 * n + 8) Oc
-    = (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 adjust.simps)
-done
-
-lemma [simp]: 
-  "fetch (ci (ly) 
-  (start_of ly as) (Dec n e)) (2 * n + 9) Bk
-  = (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 adjust.simps)
-done
-
-lemma [simp]: 
-  "fetch (ci (ly) 
-  (start_of ly as) (Dec n e)) (2 * n + 9) Oc
-  = (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 adjust.simps)
-done
-
-
-lemma [simp]: 
-  "fetch (ci (ly) 
-  (start_of ly as) (Dec n e)) (2 * n + 10) Bk
-  = (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 adjust.simps)
-done
-
-lemma [simp]: "fetch (ci (ly) 
-             (start_of ly as) (Dec n e)) (2 * n + 10) Oc
-    = (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 adjust.simps)
-done
-
-
-lemma [simp]: 
-  "fetch (ci (ly) 
-  (start_of ly as) (Dec n e)) (2 * n + 11) Oc
-  = (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 adjust.simps)
-done
-
-
-lemma [simp]: 
-  "fetch (ci (ly) 
-  (start_of ly as) (Dec n e)) (2 * n + 11) Bk
-  = (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 adjust.simps)
-done
-
-lemma [simp]:
-  "fetch (ci (ly) 
-  (start_of ly as) (Dec n e)) (2 * n + 12) Oc
-  = (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 adjust.simps)
-done
-
-
-lemma [simp]: 
-  "fetch (ci (ly) 
-  (start_of ly as) (Dec n e)) (2 * n + 12) Bk
-  = (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 adjust.simps)
-done
-
-lemma [simp]: 
-  "fetch (ci (ly) 
-  (start_of ly as) (Dec n e)) (2 * n + 13) Bk
-  = (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 adjust.simps)
-done
-
-
-lemma [simp]: 
-  "fetch (ci (ly) 
-  (start_of ly as) (Dec n e)) (14 + 2 * n) Oc
-  = (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 adjust.simps)
-done
-
-lemma [simp]: 
-  "fetch (ci (ly) 
-  (start_of ly as) (Dec n e)) (14 + 2 * n) Bk
-  = (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 adjust.simps)
-done
-
-lemma [simp]: 
-  "fetch (ci (ly) 
-  (start_of ly as) (Dec n e)) (15 + 2 * n)  Oc
-  = (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 adjust.simps)
-done
-
-lemma [simp]: 
-  "fetch (ci (ly) 
-  (start_of ly as) (Dec n e)) (15 + 2 * n)  Bk
- = (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 adjust.simps)
-done
-
-lemma [simp]: 
-  "abc_fetch as aprog = Some (Dec n e) \<Longrightarrow> 
-     fetch (ci (ly) (start_of (ly) as) 
-              (Dec n e)) (16 + 2 * n)  Bk
- = (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 adjust.simps)
-done
 
 declare dec_inv_1.simps[simp del]
 
 
-lemma [simp]: 
+lemma start_of_ineq1[simp]: 
  "\<lbrakk>abc_fetch as aprog = Some (Dec n e); ly = layout_of aprog\<rbrakk>
    \<Longrightarrow> (start_of ly e \<noteq> Suc (start_of ly as + 2 * n) \<and>
         start_of ly e \<noteq> Suc (Suc (start_of ly as + 2 * n)) \<and>  
@@ -2626,7 +2327,7 @@
 apply(case_tac "e = as", simp, simp)
 done
 
-lemma [simp]: "\<lbrakk>abc_fetch as aprog = Some (Dec n e); ly = layout_of aprog\<rbrakk>
+lemma start_of_ineq2[simp]: "\<lbrakk>abc_fetch as aprog = Some (Dec n e); ly = layout_of aprog\<rbrakk>
       \<Longrightarrow> (Suc (start_of ly as + 2 * n) \<noteq> start_of ly e \<and>
           Suc (Suc (start_of ly as + 2 * n)) \<noteq> start_of ly e \<and> 
           start_of ly as + 2 * n + 3 \<noteq> start_of ly e \<and> 
@@ -2647,15 +2348,15 @@
 apply(case_tac "e = as", simp, simp)
 done
 
-lemma [simp]: "inv_locate_b (as, lm) (n, [], []) ires = False"
+lemma inv_locate_b_nonempty[simp]: "inv_locate_b (as, lm) (n, [], []) ires = False"
 apply(auto simp: inv_locate_b.simps in_middle.simps split: if_splits)
 done
 
-lemma [simp]: "inv_locate_b (as, lm) (n, [], Bk # list) ires = False"
+lemma inv_locate_b_no_Bk[simp]: "inv_locate_b (as, lm) (n, [], Bk # list) ires = False"
 apply(auto simp: inv_locate_b.simps in_middle.simps split: if_splits)
 done
 
-lemma [simp]: 
+lemma dec_first_on_right_moving_Oc[simp]: 
  "\<lbrakk>dec_first_on_right_moving n (as, am) (s, aaa, Oc # xs) ires\<rbrakk>
    \<Longrightarrow> dec_first_on_right_moving n (as, am) (s', Oc # aaa, xs) ires"
 apply(simp only: dec_first_on_right_moving.simps)
@@ -2667,12 +2368,12 @@
 apply(case_tac [!] mr, auto)
 done
 
-lemma [simp]: 
+lemma dec_first_on_right_moving_Bk_nonempty[simp]: 
   "dec_first_on_right_moving n (as, am) (s, l, Bk # xs) ires \<Longrightarrow> l \<noteq> []"
 apply(auto simp: dec_first_on_right_moving.simps split: if_splits)
 done
 
-lemma [elim]: 
+lemma replicateE[elim]: 
   "\<lbrakk>\<not> length lm1 < length am; 
     am @ replicate (length lm1 - length am) 0 @ [0::nat] = 
                                                 lm1 @ m # lm2;
@@ -2682,7 +2383,7 @@
 apply(drule_tac length_equal, simp)
 done
 
-lemma [simp]: 
+lemma dec_after_clear_Bk_strip_hd[simp]: 
  "\<lbrakk>dec_first_on_right_moving n (as, 
                    abc_lm_s am n (abc_lm_v am n)) (s, l, Bk # xs) ires\<rbrakk>
 \<Longrightarrow> dec_after_clear (as, abc_lm_s am n 
@@ -2696,7 +2397,7 @@
 apply(case_tac [!] mr, auto)
 done
 
-lemma [simp]: 
+lemma dec_first_on_right_moving_dec_after_clear_cases[simp]: 
  "\<lbrakk>dec_first_on_right_moving n (as, 
                    abc_lm_s am n (abc_lm_v am n)) (s, l, []) ires\<rbrakk>
 \<Longrightarrow> (l = [] \<longrightarrow> dec_after_clear (as, 
@@ -2713,27 +2414,27 @@
 apply(auto simp: dec_first_on_right_moving.simps split: if_splits)
 done
 
-lemma [simp]: "\<lbrakk>dec_after_clear (as, am) (s, l, Oc # r) ires\<rbrakk>
+lemma dec_after_clear_Bk_via_Oc[simp]: "\<lbrakk>dec_after_clear (as, am) (s, l, Oc # r) ires\<rbrakk>
                 \<Longrightarrow> dec_after_clear (as, am) (s', l, Bk # r) ires"
 apply(auto simp: dec_after_clear.simps)
 done
 
-lemma [simp]: "\<lbrakk>dec_after_clear (as, am) (s, l, Bk # r) ires\<rbrakk>
+lemma dec_right_move_Bk_via_clear_Bk[simp]: "\<lbrakk>dec_after_clear (as, am) (s, l, Bk # r) ires\<rbrakk>
                 \<Longrightarrow> dec_right_move (as, am) (s', Bk # l, r) ires"
 apply(auto simp: dec_after_clear.simps dec_right_move.simps split: if_splits)
 done
 
-lemma [simp]: "\<lbrakk>dec_after_clear (as, am) (s, l, []) ires\<rbrakk>
+lemma dec_right_move_Bk_via_clear_empty[simp]: "\<lbrakk>dec_after_clear (as, am) (s, l, []) ires\<rbrakk>
              \<Longrightarrow> dec_right_move (as, am) (s', Bk # l, []) ires"
 apply(auto simp: dec_after_clear.simps dec_right_move.simps )
 done
 
-lemma [simp]: "\<lbrakk>dec_after_clear (as, am) (s, l, []) ires\<rbrakk>
+lemma dec_right_move_Bk_Bk_via_clear[simp]: "\<lbrakk>dec_after_clear (as, am) (s, l, []) ires\<rbrakk>
              \<Longrightarrow> dec_right_move (as, am) (s', Bk # l, [Bk]) ires"
 apply(auto simp: dec_after_clear.simps dec_right_move.simps split: if_splits)
 done
 
-lemma [simp]:"dec_right_move (as, am) (s, l, Oc # r) ires = False"
+lemma dec_right_move_no_Oc[simp]:"dec_right_move (as, am) (s, l, Oc # r) ires = False"
 apply(auto simp: dec_right_move.simps)
 done
               
@@ -2743,27 +2444,27 @@
 apply(auto simp: dec_right_move.simps dec_check_right_move.simps split: if_splits)
 done
 
-lemma [simp]: "(<lm::nat list> = []) = (lm = [])"
+lemma lm_iff_empty[simp]: "(<lm::nat list> = []) = (lm = [])"
 apply(case_tac lm, simp_all add: tape_of_nl_cons)
 done
 
-lemma [simp]: 
+lemma dec_right_move_asif_Bk_singleton[simp]: 
  "dec_right_move (as, am) (s, l, []) ires= 
   dec_right_move (as, am) (s, l, [Bk]) ires"
 apply(simp add: dec_right_move.simps)
 done
 
-lemma [simp]: "\<lbrakk>dec_right_move (as, am) (s, l, []) ires\<rbrakk>
+lemma dec_check_right_move_Bk_via_move[simp]: "\<lbrakk>dec_right_move (as, am) (s, l, []) ires\<rbrakk>
              \<Longrightarrow> dec_check_right_move (as, am) (s, Bk # l, []) ires"
 apply(insert dec_right_move_2_check_right_move[of as am s l "[]" s'], 
       simp)
 done
 
-lemma [simp]: "dec_check_right_move (as, am) (s, l, r) ires\<Longrightarrow> l \<noteq> []"
+lemma dec_check_right_move_nonempty[simp]: "dec_check_right_move (as, am) (s, l, r) ires\<Longrightarrow> l \<noteq> []"
 apply(auto simp: dec_check_right_move.simps split: if_splits)
 done
  
-lemma [simp]: "\<lbrakk>dec_check_right_move (as, am) (s, l, Oc # r) ires\<rbrakk>
+lemma dec_check_right_move_Oc_tail[simp]: "\<lbrakk>dec_check_right_move (as, am) (s, l, Oc # r) ires\<rbrakk>
              \<Longrightarrow> dec_after_write (as, am) (s', tl l, hd l # Oc # r) ires"
 apply(auto simp: dec_check_right_move.simps dec_after_write.simps)
 apply(rule_tac x = lm1 in exI, rule_tac x = lm2 in exI, 
@@ -2772,7 +2473,7 @@
 
 
 
-lemma [simp]: "\<lbrakk>dec_check_right_move (as, am) (s, l, Bk # r) ires\<rbrakk>
+lemma dec_left_move_Bk_tail[simp]: "\<lbrakk>dec_check_right_move (as, am) (s, l, Bk # r) ires\<rbrakk>
                 \<Longrightarrow> dec_left_move (as, am) (s', tl l, hd l # Bk # r) ires"
 apply(auto simp: dec_check_right_move.simps 
                  dec_left_move.simps inv_after_move.simps)
@@ -2781,35 +2482,35 @@
 apply(rule_tac [!] x = "(Suc rn)" in exI, simp_all)
 done
 
-lemma [simp]: "\<lbrakk>dec_check_right_move (as, am) (s, l, []) ires\<rbrakk>
+lemma dec_left_move_tail[simp]: "\<lbrakk>dec_check_right_move (as, am) (s, l, []) ires\<rbrakk>
              \<Longrightarrow> dec_left_move (as, am) (s', tl l, [hd l]) ires"
 apply(auto simp: dec_check_right_move.simps 
                  dec_left_move.simps inv_after_move.simps)
 apply(rule_tac x = lm1 in exI, rule_tac x = m in exI, auto)
 done
 
-lemma [simp]: "dec_left_move (as, am) (s, aaa, Oc # xs) ires = False"
+lemma dec_left_move_no_Oc[simp]: "dec_left_move (as, am) (s, aaa, Oc # xs) ires = False"
 apply(auto simp: dec_left_move.simps inv_after_move.simps)
 done
 
-lemma [simp]: "dec_left_move (as, am) (s, l, r) ires
+lemma dec_left_move_nonempty[simp]: "dec_left_move (as, am) (s, l, r) ires
              \<Longrightarrow> l \<noteq> []"
 apply(auto simp: dec_left_move.simps split: if_splits)
 done
 
-lemma [simp]: "inv_on_left_moving_in_middle_B (as, [m])
+lemma inv_on_left_moving_in_middle_B_Oc_Bk_Bks[simp]: "inv_on_left_moving_in_middle_B (as, [m])
   (s', Oc # Oc\<up>m @ Bk # Bk # ires, Bk # Bk\<up>rn) ires"
 apply(simp add: inv_on_left_moving_in_middle_B.simps)
 apply(rule_tac x = "[m]" in exI, auto)
 done
 
-lemma [simp]: "inv_on_left_moving_in_middle_B (as, [m])
+lemma inv_on_left_moving_in_middle_B_Oc_Bk_Bk[simp]: "inv_on_left_moving_in_middle_B (as, [m])
   (s', Oc # Oc\<up>m @ Bk # Bk # ires, [Bk]) ires"
 apply(simp add: inv_on_left_moving_in_middle_B.simps)
 done
 
 
-lemma [simp]: "lm1 \<noteq> [] \<Longrightarrow> 
+lemma inv_on_left_moving_in_middle_B_Oc_Bk_Bks_rev[simp]: "lm1 \<noteq> [] \<Longrightarrow> 
   inv_on_left_moving_in_middle_B (as, lm1 @ [m]) (s', 
   Oc # Oc\<up>m @ Bk # <rev lm1> @ Bk # Bk # ires, Bk # Bk\<up>rn) ires"
 apply(simp only: inv_on_left_moving_in_middle_B.simps)
@@ -2817,7 +2518,7 @@
 apply(simp add: tape_of_nl_cons split: if_splits)
 done
 
-lemma [simp]: "lm1 \<noteq> [] \<Longrightarrow> 
+lemma inv_on_left_moving_in_middle_B_Oc_Bk_Bk_rev[simp]: "lm1 \<noteq> [] \<Longrightarrow> 
   inv_on_left_moving_in_middle_B (as, lm1 @ [m]) (s', 
   Oc # Oc\<up> m @ Bk # <rev lm1> @ Bk # Bk # ires, [Bk]) ires"
 apply(simp only: inv_on_left_moving_in_middle_B.simps)
@@ -2825,17 +2526,17 @@
 apply(simp add: tape_of_nl_cons split: if_splits)
 done
 
-lemma [simp]: "dec_left_move (as, am) (s, l, Bk # r) ires
+lemma inv_on_left_moving_Bk_tail[simp]: "dec_left_move (as, am) (s, l, Bk # r) ires
        \<Longrightarrow> inv_on_left_moving (as, am) (s', tl l, hd l # Bk # r) ires"
 apply(auto simp: dec_left_move.simps inv_on_left_moving.simps split: if_splits)
 done
 
-lemma [simp]: "dec_left_move (as, am) (s, l, []) ires
+lemma inv_on_left_moving_tail[simp]: "dec_left_move (as, am) (s, l, []) ires
              \<Longrightarrow> inv_on_left_moving (as, am) (s', tl l, [hd l]) ires"
 apply(auto simp: dec_left_move.simps inv_on_left_moving.simps split: if_splits)
 done
 
-lemma [simp]: "dec_after_write (as, am) (s, l, Oc # r) ires
+lemma dec_on_right_moving_Oc_mv[simp]: "dec_after_write (as, am) (s, l, Oc # r) ires
        \<Longrightarrow> dec_on_right_moving (as, am) (s', Oc # l, r) ires"
 apply(auto simp: dec_after_write.simps dec_on_right_moving.simps)
 apply(rule_tac x = "lm1 @ [m]" in exI, rule_tac x = "tl lm2" in exI, 
@@ -2844,17 +2545,17 @@
 apply(case_tac lm2, auto split: if_splits simp: tape_of_nl_cons)
 done
 
-lemma [simp]: "dec_after_write (as, am) (s, l, Bk # r) ires
+lemma dec_after_write_Oc_via_Bk[simp]: "dec_after_write (as, am) (s, l, Bk # r) ires
        \<Longrightarrow> dec_after_write (as, am) (s', l, Oc # r) ires"
 apply(auto simp: dec_after_write.simps)
 done
 
-lemma [simp]: "dec_after_write (as, am) (s, aaa, []) ires
+lemma dec_after_write_Oc_empty[simp]: "dec_after_write (as, am) (s, aaa, []) ires
              \<Longrightarrow> dec_after_write (as, am) (s', aaa, [Oc]) ires"
 apply(auto simp: dec_after_write.simps)
 done
 
-lemma [simp]: "dec_on_right_moving (as, am) (s, l, Oc # r) ires
+lemma dec_on_right_moving_Oc_move[simp]: "dec_on_right_moving (as, am) (s, l, Oc # r) ires
        \<Longrightarrow> dec_on_right_moving (as, am) (s', Oc # l, r) ires"
 apply(simp only: dec_on_right_moving.simps)
 apply(erule_tac exE)+
@@ -2865,24 +2566,24 @@
 apply(case_tac mr, auto)
 done
 
-lemma [simp]: "dec_on_right_moving (as, am) (s, l, r) ires\<Longrightarrow>  l \<noteq> []"
+lemma dec_on_right_moving_nonempty[simp]: "dec_on_right_moving (as, am) (s, l, r) ires\<Longrightarrow>  l \<noteq> []"
 apply(auto simp: dec_on_right_moving.simps split: if_splits)
 done
 
-lemma [simp]: "dec_on_right_moving (as, am) (s, l, Bk # r) ires
+lemma dec_after_clear_Bk_tail[simp]: "dec_on_right_moving (as, am) (s, l, Bk # r) ires
       \<Longrightarrow>  dec_after_clear (as, am) (s', tl l, hd l # Bk # r) ires"
 apply(auto simp: dec_on_right_moving.simps dec_after_clear.simps)
 apply(case_tac [!] mr, auto split: if_splits)
 done
 
-lemma [simp]: "dec_on_right_moving (as, am) (s, l, []) ires
+lemma dec_after_clear_tail[simp]: "dec_on_right_moving (as, am) (s, l, []) ires
              \<Longrightarrow> dec_after_clear (as, am) (s', tl l, [hd l]) ires"
 apply(auto simp: dec_on_right_moving.simps dec_after_clear.simps)
 apply(simp_all split: if_splits)
 apply(rule_tac x = lm1 in exI, simp)
 done
 
-lemma [simp]: 
+lemma inv_stop_abc_lm_s_nonempty[simp]: 
  "inv_stop (as, abc_lm_s am n (abc_lm_v am n)) (s, l, r) ires \<Longrightarrow> l \<noteq> []"
 apply(auto simp: inv_stop.simps)
 done
@@ -2906,7 +2607,7 @@
       simp add: exp_ind del: replicate.simps, simp)
 done
 
-lemma [simp]: 
+lemma inv_on_left_moving_Bk_tl[simp]: 
  "\<lbrakk>inv_locate_b (as, am) (n, aaa, Bk # xs) ires; 
    abc_lm_v am n = 0\<rbrakk>
    \<Longrightarrow> inv_on_left_moving (as, abc_lm_s am n 0) 
@@ -2928,7 +2629,7 @@
 done
 
 
-lemma [simp]:
+lemma inv_on_left_moving_tl[simp]:
  "\<lbrakk>abc_lm_v am n = 0; inv_locate_b (as, am) (n, aaa, []) ires\<rbrakk>
    \<Longrightarrow> inv_on_left_moving (as, abc_lm_s am n 0) (s, tl aaa, [hd aaa]) ires"
 apply(simp add: inv_on_left_moving.simps)
@@ -2948,15 +2649,15 @@
 apply(case_tac [!] m, simp_all)
 done
 
-lemma [simp]: "\<lbrakk>am ! n = (0::nat); n < length am\<rbrakk> \<Longrightarrow> am[n := 0] = am"
+lemma update_zero_to_zero[simp]: "\<lbrakk>am ! n = (0::nat); n < length am\<rbrakk> \<Longrightarrow> am[n := 0] = am"
 apply(simp add: list_update_same_conv)
 done
 
-lemma  [intro]: "\<lbrakk>abc_lm_v (a # list) 0 = 0\<rbrakk> \<Longrightarrow> a = 0"
+lemma abc_lm_v_zero: "\<lbrakk>abc_lm_v (a # list) 0 = 0\<rbrakk> \<Longrightarrow> a = 0"
 apply(simp add: abc_lm_v.simps split: if_splits)
 done
 
-lemma [simp]: 
+lemma inv_locate_a_via_stop[simp]: 
  "inv_stop (as, abc_lm_s am n 0) 
           (start_of (layout_of aprog) e, aaa, Oc # xs) ires
   \<Longrightarrow> inv_locate_a (as, abc_lm_s am n 0) (0, aaa, Oc # xs) ires"
@@ -2965,7 +2666,7 @@
 apply(auto simp: inv_stop.simps at_begin_norm.simps)
 done
 
-lemma [simp]: 
+lemma inv_locate_b_cases_via_stop[simp]: 
  "\<lbrakk>inv_stop (as, abc_lm_s am n 0) 
           (start_of (layout_of aprog) e, aaa, Oc # xs) ires\<rbrakk>
   \<Longrightarrow> inv_locate_b (as, am) (0, Oc # aaa, xs) ires \<or> 
@@ -2987,16 +2688,11 @@
 apply(auto simp: inv_stop.simps abc_lm_s.simps)
 done
 
-lemma [simp]:
-  "fetch (ci (layout_of aprog) 
-       (start_of (layout_of aprog) as) (Dec n e)) 0 b = (Nop, 0)"
-by(simp add: fetch.simps)
-
 declare dec_inv_1.simps[simp del]
 
 declare inv_locate_n_b.simps [simp del]
 
-lemma [simp]:
+lemma inv_locate_n_b_Oc_via_at_begin_fst_bwtn[simp]:
   "\<lbrakk>0 < abc_lm_v am n; 0 < n; 
     at_begin_fst_bwtn (as, am) (n, aaa, Oc # xs) ires\<rbrakk>
  \<Longrightarrow> inv_locate_n_b (as, am) (n, Oc # aaa, xs) ires"
@@ -3008,21 +2704,7 @@
 apply(arith)
 done
 
-lemma [simp]: 
- "\<lbrakk>0 < abc_lm_v am n; 0 < n; 
-   at_begin_fst_awtn (as, am) (n, aaa, Oc # xs) ires\<rbrakk>
- \<Longrightarrow> inv_locate_n_b (as, am) (n, Oc # aaa, xs) ires"
-apply(simp only: at_begin_fst_awtn.simps inv_locate_n_b.simps )
-apply(erule exE)+
-apply(erule conjE)+
-apply(rule_tac x = lm1 in exI, rule_tac x = "[]" in exI, 
-      rule_tac x = "Suc tn" in exI, rule_tac x = 0 in exI)
-apply(simp add: exp_ind del: replicate.simps)
-apply(rule conjI)+
-apply(auto)
-done
-
-lemma [simp]:
+lemma dec_first_on_right_moving_Oc_via_inv_locate_n_b[simp]:
  "\<lbrakk>inv_locate_n_b (as, am) (n, aaa, Oc # xs) ires\<rbrakk>
  \<Longrightarrow> dec_first_on_right_moving n (as, abc_lm_s am n (abc_lm_v am n))  
                                       (s, Oc # aaa, xs) ires"
@@ -3049,24 +2731,20 @@
       simp add: Suc_diff_le exp_ind del: replicate.simps, simp)
 done
 
-lemma [simp]: "inv_on_left_moving (as, am) (s, [], r) ires 
+lemma inv_on_left_moving_nonempty[simp]: "inv_on_left_moving (as, am) (s, [], r) ires 
   = False"
 apply(simp add: inv_on_left_moving.simps inv_on_left_moving_norm.simps
                 inv_on_left_moving_in_middle_B.simps)
 done
 
-lemma [simp]: 
+lemma inv_check_left_moving_startof_nonempty[simp]: 
   "inv_check_left_moving (as, abc_lm_s am n 0)
   (start_of (layout_of aprog) as + 2 * n + 14, [], Oc # xs) ires
  = False"
 apply(simp add: inv_check_left_moving.simps inv_check_left_moving_in_middle.simps)
 done
 
-lemma [simp]: "inv_check_left_moving (as, abc_lm_s lm n (abc_lm_v lm n)) (s, [], Oc # list) ires = False"
-apply(simp add: inv_check_left_moving.simps inv_check_left_moving_in_middle.simps)
-done
-
-lemma [elim]: "\<lbrakk>abc_fetch as ap = Some (Dec n e);
+lemma start_of_lessE[elim]: "\<lbrakk>abc_fetch as ap = Some (Dec n e);
                 start_of (layout_of ap) as < start_of (layout_of ap) e; 
                 start_of (layout_of ap) e \<le> Suc (start_of (layout_of ap) as + 2 * n)\<rbrakk>
        \<Longrightarrow> RR"
@@ -3141,7 +2819,7 @@
   apply(rule_tac x = stp in exI, simp)
   done
 
-lemma [simp]:
+lemma crsp_abc_step_via_stop[simp]:
   "\<lbrakk>abc_lm_v lm n = 0;
   inv_stop (as, abc_lm_s lm n (abc_lm_v lm n)) (start_of ly e, lb, rb) ires\<rbrakk>
   \<Longrightarrow> crsp ly (abc_step_l (as, lm) (Some (Dec n e))) (start_of ly e, lb, rb) ires"
@@ -3301,20 +2979,20 @@
 lemma fix_add: "fetch ap ((x::nat) + 2*n) b = fetch ap (2*n + x) b"
   using Suc_1 add.commute by metis
 
-lemma [elim]: 
+lemma inv_locate_n_b_Bk_elim[elim]: 
  "\<lbrakk>0 < abc_lm_v am n; inv_locate_n_b (as, am) (n, aaa, Bk # xs) ires\<rbrakk> 
  \<Longrightarrow> RR"
 apply(auto simp: inv_locate_n_b.simps abc_lm_v.simps split: if_splits)
 apply(case_tac [!] m, auto)
-done
- 
-lemma [elim]:
+  done
+
+lemma inv_locate_n_b_nonemptyE[elim]:
  "\<lbrakk>0 < abc_lm_v am n; inv_locate_n_b (as, am) 
                                 (n, aaa, []) ires\<rbrakk> \<Longrightarrow> RR"
 apply(auto simp: inv_locate_n_b.simps abc_lm_v.simps split: if_splits)
 done
 
-lemma [simp]: "dec_after_write (as, am) (s, aa, r) ires
+lemma no_Ocs_dec_after_write[simp]: "dec_after_write (as, am) (s, aa, r) ires
            \<Longrightarrow> takeWhile (\<lambda>a. a = Oc) aa = []"
 apply(simp only : dec_after_write.simps)
 apply(erule exE)+
@@ -3323,7 +3001,7 @@
 apply(case_tac a, simp only: takeWhile.simps , simp_all split: if_splits)
 done
 
-lemma [simp]: 
+lemma fewer_Ocs_dec_on_right_moving[simp]: 
      "\<lbrakk>dec_on_right_moving (as, lm) (s, aa, []) ires; 
        length (takeWhile (\<lambda>a. a = Oc) (tl aa)) 
            \<noteq> length (takeWhile (\<lambda>a. a = Oc) aa) - Suc 0\<rbrakk>
@@ -3335,7 +3013,7 @@
 apply(case_tac mr, auto split: if_splits)
 done
 
-lemma [simp]: 
+lemma more_Ocs_dec_after_clear[simp]: 
   "dec_after_clear (as, abc_lm_s am n (abc_lm_v am n - Suc 0)) 
              (start_of (layout_of aprog) as + 2 * n + 9, aa, Bk # xs) ires
  \<Longrightarrow> length xs - Suc 0 < length xs + 
@@ -3346,21 +3024,24 @@
 apply(simp split: if_splits )
 done
 
-lemma [simp]: 
+lemma more_Ocs_dec_after_clear2[simp]: 
  "\<lbrakk>dec_after_clear (as, abc_lm_s am n (abc_lm_v am n - Suc 0))
        (start_of (layout_of aprog) as + 2 * n + 9, aa, []) ires\<rbrakk>
     \<Longrightarrow> Suc 0 < length (takeWhile (\<lambda>a. a = Oc) aa)"
 apply(simp add: dec_after_clear.simps split: if_splits)
 done
 
-lemma [elim]: 
-  "inv_check_left_moving (as, lm)
-  (s, [], Oc # xs) ires
+lemma inv_check_left_moving_nonemptyE[elim]: 
+  "inv_check_left_moving (as, lm) (s, [], Oc # xs) ires
  \<Longrightarrow> RR"
 apply(simp add: inv_check_left_moving.simps inv_check_left_moving_in_middle.simps)
 done
 
-lemma [simp]:
+lemma inv_check_left_moving_nonempty[simp]:
+  "inv_check_left_moving (as, lm) (s, [], Oc # list) ires = False"
+  by auto
+
+lemma inv_locate_n_b_Oc_via_at_begin_norm[simp]:
 "\<lbrakk>0 < abc_lm_v am n; 
   at_begin_norm (as, am) (n, aaa, Oc # xs) ires\<rbrakk>
   \<Longrightarrow> inv_locate_n_b (as, am) (n, Oc # aaa, xs) ires"
@@ -3372,7 +3053,7 @@
 apply(case_tac "lm2", auto simp: tape_of_nl_cons split: if_splits)
 done
 
-lemma [simp]: 
+lemma inv_locate_n_b_Oc_via_at_begin_fst_awtn[simp]: 
  "\<lbrakk>0 < abc_lm_v am n; 
    at_begin_fst_awtn (as, am) (n, aaa, Oc # xs) ires\<rbrakk>
  \<Longrightarrow> inv_locate_n_b (as, am) (n, Oc # aaa, xs) ires"
@@ -3386,13 +3067,13 @@
 apply(auto)
 done
 
-lemma [simp]: 
+lemma inv_locate_n_b_Oc_via_inv_locate_n_a[simp]: 
  "\<lbrakk>0 < abc_lm_v am n; inv_locate_a (as, am) (n, aaa, Oc # xs) ires\<rbrakk>
  \<Longrightarrow> inv_locate_n_b (as, am) (n, Oc#aaa, xs) ires"
 apply(auto simp: inv_locate_a.simps at_begin_fst_bwtn.simps)
 done
 
-lemma [simp]: 
+lemma more_Oc_dec_on_right_moving[simp]: 
  "\<lbrakk>dec_on_right_moving (as, am) (s, aa, Bk # xs) ires; 
    Suc (length (takeWhile (\<lambda>a. a = Oc) (tl aa)))
    \<noteq> length (takeWhile (\<lambda>a. a = Oc) aa)\<rbrakk>
@@ -3458,7 +3139,7 @@
   qed
 qed
 
-lemma [simp]: 
+lemma crsp_abc_step_l_start_of[simp]: 
   "\<lbrakk>inv_stop (as, abc_lm_s lm n (abc_lm_v lm n - Suc 0)) 
   (start_of (layout_of ap) as + 2 * n + 16, a, b) ires;
    abc_lm_v lm n > 0;
@@ -3647,10 +3328,7 @@
 apply(simp add: layout_of.simps)
 done
 
-lemma [simp]: "length (layout_of xs) = length xs"
-by(simp add: layout_of.simps)
-
-lemma [simp]:  
+lemma map_start_of_layout[simp]:  
   "map (start_of (layout_of xs @ [length_of x])) [0..<length xs] =  (map (start_of (layout_of xs)) [0..<length xs])"
 apply(auto)
 apply(simp add: layout_of.simps start_of.simps)
@@ -3698,7 +3376,7 @@
     done
 qed
 
-lemma [simp]: 
+lemma fetch_Nops[simp]: 
   "\<lbrakk>ly = layout_of ap; tp = tm_of ap\<rbrakk> \<Longrightarrow>
         fetch (tp @ [(Nop, 0), (Nop, 0)]) (start_of ly (length ap)) b = 
        (Nop, 0)"