tm: comparison thys/Abacus.thy

equal deleted inserted replaced

-:4e50ff177348
+:6e1c03614d36
 The lemmas in this section lead to the correctness of
 the compilation of @{text "Inc n"} instruction.
 *}
 declare abc_step_l.simps[simp del] abc_steps_l.simps[simp del]
-lemma [simp]: "start_of ly as > 0"
+lemma start_of_nonzero[simp]: "start_of ly as > 0" "(start_of ly as = 0) = False"
-apply(simp add: start_of.simps)
+apply(auto simp: start_of.simps)
 done
 lemma abc_steps_l_0: "abc_steps_l ac ap 0 = ac"
 by(case_tac ac, simp add: abc_steps_l.simps)
 declare append_assoc[simp]
 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
 lemma ci_nth:
 "\<lbrakk>ly = layout_of aprog;
 lemma div_apart_iff: "\<lbrakk>x mod (2::nat) = 0; y mod 2 = 0\<rbrakk> \<Longrightarrow>
 (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>
 start_of ly (Suc as) = start_of ly as +
 length ((tms_of aprog) ! as) div 2"
 lemma concat_take_suc: "Suc n \<le> length xs \<Longrightarrow>
 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"
+lemma length_tms_of_elem_even[intro]:  "n < length ap \<Longrightarrow> length (tms_of ap ! n) mod 2 = 0"
-by(auto simp: tms_of.simps tpairs_of.simps)
-lemma [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)
 lemma compile_mod2: "length (concat (take n (tms_of ap))) mod 2 = 0"
 proof(induct n)
 lemma wf_findnth_LE: "wf findnth_LE"
 by(auto simp: findnth_LE_def lex_pair_def)
 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>
+lemma between_sucs:"x < Suc n \<Longrightarrow> \<not> x < n \<Longrightarrow> x = n" by auto
-\<Longrightarrow> fetch (findnth n) a Bk = (W1, a)"
-apply(case_tac a, simp_all)
+lemma fetch_findnth[simp]:
-apply(induct n, auto simp: findnth.simps length_findnth nth_append)
+"\<lbrakk>0 < a; a < Suc (2 * n); a mod 2 = Suc 0\<rbrakk> \<Longrightarrow> fetch (findnth n) a Oc = (R, Suc a)"
-apply arith
+"\<lbrakk>0 < a; a < Suc (2 * n); a mod 2 \<noteq> Suc 0\<rbrakk> \<Longrightarrow> fetch (findnth n) a Oc = (R, a)"
-done
+"\<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)"
-lemma [simp]:
+by(cases a;induct n;force simp: length_findnth nth_append dest!:between_sucs)+
-"\<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
 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]
 abc_lm_s.simps[simp del] abc_lm_v.simps[simp del]
 ci.simps[simp del] inv_after_move.simps[simp del]
 inv_check_left_moving_on_leftmost.simps[simp del]
 inv_after_left_moving.simps[simp del]
 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"
+lemma replicate_once[intro]: "\<exists>rn. [Bk] = Bk \<up> rn"
-by (metis replicate_0 replicate_Suc)
+by (metis replicate.simps)
-lemma [intro]:  "at_begin_norm (as, am) (q, aaa, []) ires
+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)
 defer
 apply(erule disj_forward, auto)
 apply(case_tac mr, simp_all)
 apply(case_tac lm2, simp_all add: tape_of_nl_cons split: if_splits, auto)
 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"
+lemma inv_locate_b_Oc_via_a[simp]:
-by auto
-lemma exp_ind: "a\<up>(Suc x) = a\<up>x @ [a]"
-apply(induct x, auto)
-done
-lemma [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
 at_begin_norm.simps at_begin_fst_bwtn.simps
 at_begin_fst_awtn.simps)
 done
 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)
 apply(rule_tac disjI1)
 apply(simp only: in_middle.simps at_begin_norm.simps)
 \<Longrightarrow> inv_locate_a (as, am) (Suc q, Bk # aaa, xs) ires"
 apply(case_tac "\<exists> n. xs = Bk\<up>n", simp, simp)
 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)+
 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,
 apply(auto)
 done
 (*inv: from locate_b to after_write*)
-lemma [simp]: "(a mod 2 \<noteq> Suc 0) = (a mod 2 = 0)  "
+lemma not_even_then_odd[simp]: "(a mod 2 \<noteq> 0) = (a mod 2 = Suc 0)  "
 by arith
-lemma [simp]: "(a mod 2 \<noteq> 0) = (a mod 2 = Suc 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 mod_ex1: "(a mod 2 = Suc 0) = (\<exists> q. a = Suc (2 * q))"
+lemma odd_plus_one_even[simp]: "x mod 2 = Suc 0 \<Longrightarrow> Suc x mod 2 = 0"
 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"
-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"
-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 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
 (*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"
 and crsp: "crsp ly (as, lm) (s, l, r) ires"
 and not0: "n > 0"
 apply(auto simp: mod_ex1 mod_ex2)
 done
 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
 lemma findnth_correct:
 assumes layout: "ly = layout_of ap"
 declare inc_inv.simps[simp del]
 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)))
 (s, aaa, Oc # xs) ires"
 apply(auto simp: in_middle.simps inv_after_write.simps
 apply(simp only: Suc_diff_le exp_ind)
 apply(subgoal_tac "lm2 = []", simp)
 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 "[]"])
 by(simp)
 (*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
+assumes "inv_after_move (as, lm) (s, l, Bk # r) ires"
-\<Longrightarrow> (l = [] \<longrightarrow>
+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)
+proof (cases l)
-apply(subgoal_tac "l \<noteq> []", rule conjI, simp, rule impI,
+case (Cons a list)
-rule disjI1, simp only: inv_on_left_moving_norm.simps)
+from assms Cons show ?thesis
-apply(erule exE)+
+apply(simp only: inv_after_move.simps inv_on_left_moving.simps)
-apply(subgoal_tac "lm2 = []")
+apply(rule conjI, force, rule impI, rule disjI1, simp only: inv_on_left_moving_norm.simps)
-apply(rule_tac x = lm1 in exI, rule_tac x = lm2 in exI,
+apply(erule exE)+
-rule_tac x = m in exI, rule_tac x = m in exI,
+apply(subgoal_tac "lm2 = []")
-rule_tac x = 1 in exI,
+apply(rule_tac x = lm1 in exI, rule_tac x = lm2 in exI,
-rule_tac x = "rn - 1" in exI, auto)
+rule_tac x = m in exI, rule_tac x = m in exI,
-apply(auto split: if_splits)
+rule_tac x = 1 in exI,
-apply(case_tac [1-2] rn, simp_all)
+rule_tac x = "rn - 1" in exI) apply (auto split:if_splits)
-apply(case_tac [!] lm2, simp_all add: tape_of_nl_cons split: if_splits)
+apply(case_tac [1-2] rn, simp_all)
-done
+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]:
 "inv_after_move (as, lm) (s, l, []) ires
 \<Longrightarrow> (l = [] \<longrightarrow> inv_on_left_moving (as, lm) (s', [], [Bk]) ires) \<and>
 rule_tac x = 1 in exI, rule_tac x = "rn - 1" in exI, simp, case_tac rn)
 apply(auto split: if_splits)
 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"
 apply(auto simp: inv_after_clear.simps inv_on_right_moving.simps )
 apply(subgoal_tac "lm2 \<noteq> []")
 apply(case_tac [!] "lm2::nat list", auto)
 apply(case_tac rn, auto split: if_splits simp: tape_of_nl_cons)
 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,
 rule_tac x = "ml + mr" in exI, simp)
 apply(rule_tac x = "Suc ml" in exI,
 \<Longrightarrow> inv_after_write (as, lm) (y, l, Oc # r) ires"
 apply(auto simp: inv_on_right_moving.simps inv_after_write.simps )
 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"
 apply(case_tac l, simp, simp)
 apply(simp only: inv_on_left_moving_norm.simps
 apply(case_tac [!] ml, auto)
 apply(auto simp: tape_of_nl_cons split: if_splits)
 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"
 apply(simp only: inv_on_left_moving_norm.simps)
 apply(erule exE)+
 rule_tac x = m in exI, rule_tac x = "ml - 1" in exI,
 rule_tac x = "Suc mr" in exI, rule_tac x = rn in exI, simp)
 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)
 apply(case_tac "l \<noteq> []", rule conjI, simp, simp)
 apply(case_tac "hd l", simp, simp, simp)
 inv_check_left_moving_on_leftmost.simps split: if_splits)
 apply(case_tac [!] "rev lm1", simp_all)
 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
 inv_check_left_moving_in_middle.simps  split: if_splits)
 done
 apply(simp add: inv_on_left_moving.simps inv_check_left_moving.simps)
 apply(case_tac l, simp, simp)
 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"
+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
+assumes "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"
+shows "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
+using assms
-inv_on_left_moving_in_middle_B.simps)
+apply(simp only: inv_check_left_moving_in_middle.simps
-apply(erule_tac exE)+
+inv_on_left_moving_in_middle_B.simps)
-apply(rule_tac x = "rev (tl (rev lm1))" in exI,
+apply(erule_tac exE)+
-rule_tac x = "[hd (rev lm1)] @ lm2" in exI, auto)
+apply(rule_tac x = "rev (tl (rev lm1))" in exI,
-apply(case_tac [!] "rev lm1",simp_all add: tape_of_nat_def tape_of_list_def tape_of_nat_list.simps)
+rule_tac x = "[hd (rev lm1)] @ lm2" in exI, auto)
-apply(case_tac [!] a, simp_all)
+apply(case_tac [!] "rev lm1",simp_all add: tape_of_nat_def tape_of_list_def tape_of_nat_list.simps)
-apply(case_tac [1] lm2, auto simp:tape_of_nat_def)
+apply(case_tac [!] a, simp_all)
-apply(case_tac [3] lm2, auto simp:tape_of_nat_def)
+apply(case_tac [1] lm2, auto simp:tape_of_nat_def)
-apply(case_tac [!] lista, simp_all add: tape_of_nat_def)
+apply(case_tac [3] lm2, auto simp:tape_of_nat_def)
-done
+apply(case_tac [!] lista, simp_all add: tape_of_nat_def)
+done
-lemma [simp]:
+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 inv_on_left_moving_in_middle_B_Bk_Oc_via_check[simp]:
-lemma [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
 inv_check_left_moving_in_middle_2_on_left_moving_in_middle_B[of
 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
 inv_on_left_moving_norm.simps)
 apply(rule_tac x = "rev (tl (rev lm1))" in exI,
 apply(rule_tac [!] x = "Suc (Suc 0)" in exI, simp)
 apply(case_tac [!] "rev lm1", simp_all)
 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,
 auto simp: inv_check_left_moving.simps inv_on_left_moving.simps)
 apply(case_tac a, simp, simp)
 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
 lemma tinc_correct_pre:
 assumes layout: "ly = layout_of ap"
 and inv_start: "inv_locate_a (as, lm) (n, l, r) ires"
 and lm': "lm' = abc_lm_s lm n (Suc (abc_lm_v lm n))"
 thus  "Q (step (a, b, c) (tinc_b, 0)) \<and> (step (a, b, c) (tinc_b, 0), a, b, c) \<in> inc_LE"
 apply(simp add:Q)
 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
+apply(simp_all add: inc_inv.simps inc_LE_def lex_triple_def lex_pair_def inc_measure_def
-numeral_4_eq_4 numeral_6_eq_6 numeral_7_eq_7 numeral_8_eq_8 numeral_9_eq_9)
+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"
 and lm': "lm' = abc_lm_s lm n (Suc (abc_lm_v lm n))"
 shows "\<exists> stp l' r'. steps (Suc 0, l, r) (tinc_b, 0) stp = (10, l', r')
 done
 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
 lemma crsp_step_inc_pre:
 assumes layout: "ly = layout_of ap"
 else if s = ss + 2 * n + 15 then
 inv_after_left_moving (as, am'') (s, l, r) ires
 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)
+"fetch (ci (ly) (start_of ly as) (Dec n e)) (Suc (Suc (2 * n))) Oc
-apply(auto simp: ci.simps nth_append length_findnth adjust.simps shift.simps tdec_b_def)
+= (R, start_of ly as + 2*n + 2)"
-done
+"fetch (ci (ly) (start_of ly as) (Dec n e)) (Suc (Suc (2 * n))) Bk
+= (L, start_of ly as + 2*n + 13)"
-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)"
+"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),
 start_of ly as - Suc 0) stp = (Suc (start_of ly as + 2 * n), la, ra) \<and>
 inv_locate_b (as, lm) (n, la, ra) ires"
 apply(rule_tac x = "Suc (Suc 0)" in exI)
 apply(auto simp: steps.simps step.simps length_ci_dec)
 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),
 start_of ly as - Suc 0) stp = (Suc (start_of ly as + 2 * n), la, ra) \<and>
 inv_locate_b (as, lm) (n, la, ra) ires"
 by(simp add: startof_Suc2)
 ultimately show "?thesis"
 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)
+by(drule_tac start_of_ge, auto)
-apply(auto)
-done
+lemma abc_fetch_contrE2[elim]: "\<lbrakk>abc_fetch as ap = Some (Dec n e); as > e;
-lemma [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>
 start_of ly e \<noteq> start_of ly as + 2 * n + 3 \<and>
 start_of ly e \<noteq> start_of ly as + 2 * n + 4 \<and>
 using start_of_ge[of as aprog n e ly] start_of_less[of e as ly]
 apply(case_tac "e < as", simp)
 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>
 start_of ly as + 2 * n + 4 \<noteq> start_of ly e \<and>
 start_of ly as + 2 * n + 5 \<noteq>start_of ly e \<and>
 using start_of_ge[of as aprog n e ly] start_of_less[of e as ly]
 apply(case_tac "e < as", simp, simp)
 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)
 apply(erule exE)+
 apply(rule_tac x = lm1 in exI, rule_tac x = lm2 in exI,
 apply(rule_tac x = "Suc ml" in exI,
 rule_tac x = "mr - 1" in exI, auto)
 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;
 0 < m\<rbrakk>
 \<Longrightarrow> RR"
 apply(subgoal_tac "lm2 = []", simp)
 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
 (abc_lm_v am n - Suc 0)) (s', tl l, hd l # Bk # xs) ires"
 apply(simp only: dec_first_on_right_moving.simps
 apply(rule_tac x = lm1 in exI, rule_tac x = lm2 in exI,
 rule_tac x = "m - 1" in exI, auto simp: )
 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,
 abc_lm_s am n (abc_lm_v am n - Suc 0)) (s', [], [Bk]) ires) \<and>
 (l \<noteq> [] \<longrightarrow> dec_after_clear (as, abc_lm_s am n
 apply(rule_tac x = lm1 in exI, rule_tac x = "m - 1" in exI, auto)
 apply(case_tac [1-2] m, auto)
 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
 lemma dec_right_move_2_check_right_move[simp]:
 "\<lbrakk>dec_right_move (as, am) (s, l, Bk # r) ires\<rbrakk>
 \<Longrightarrow> dec_check_right_move (as, am) (s', Bk # l, r) ires"
 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,
 rule_tac x = m in exI, auto)
 done
-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)
 apply(rule_tac x = lm1 in exI, rule_tac x = m in exI, auto split: if_splits)
 apply(case_tac [!] lm2, simp_all add: tape_of_nl_cons split: if_splits)
 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)
 apply(rule_tac x = "lm1 @ [m ]" in exI, rule_tac x = "[]" in exI, simp)
 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)
 apply(rule_tac x = "lm1 @ [m ]" in exI, rule_tac x = "[]" in exI, simp)
 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,
 rule_tac x = "hd lm2" in exI, simp)
 apply(rule_tac x = "Suc 0" in exI,rule_tac x =  "Suc (hd lm2)" in exI)
 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)+
 apply(erule conjE)+
 apply(rule_tac x = lm1 in exI, rule_tac x = lm2 in exI,
 rule_tac x = "m" in exI, rule_tac x = "Suc ml" in exI,
 rule_tac x = "mr - 1" in exI, simp)
 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
 lemma dec_false_1[simp]:
 apply(subgoal_tac "Suc (length lm1) - length am =
 Suc (length lm1 - length am)",
 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)
 (s, tl aaa, hd aaa # Bk # xs) ires"
 apply(simp add: inv_on_left_moving.simps)
 apply(simp only: exp_ind[THEN sym] replicate_Suc Nat.Suc_diff_le)
 apply(auto simp: inv_on_left_moving_in_middle_B.simps split: if_splits)
 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)
 apply(simp only: inv_locate_b.simps in_middle.simps)
 apply(erule_tac exE)+
 apply(simp_all only: exp_ind Nat.Suc_diff_le del: replicate_Suc, simp_all)
 apply(auto simp: inv_on_left_moving_in_middle_B.simps split: if_splits)
 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"
 apply(simp add: inv_locate_a.simps)
 apply(rule disjI1)
 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>
 inv_locate_b (as, abc_lm_s am n 0) (0, Oc # aaa, xs) ires"
 apply(simp)
 "inv_stop (as, abc_lm_s am n 0)
 (start_of (layout_of aprog) e, aaa, []) ires = False"
 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"
 apply(simp add: at_begin_fst_bwtn.simps inv_locate_n_b.simps )
 done
 lemma Suc_minus:"length am + tn = n
 \<Longrightarrow> Suc tn = Suc n - length am "
 apply(arith)
 done
-lemma [simp]:
+lemma dec_first_on_right_moving_Oc_via_inv_locate_n_b[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]:
 "\<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"
 apply(auto simp: inv_locate_n_b.simps dec_first_on_right_moving.simps
 abc_lm_s.simps abc_lm_v.simps)
 apply(rule_tac x = lm1 in exI, rule_tac x = lm2 in exI,
 rule_tac x = m in exI,
 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"
+lemma start_of_lessE[elim]: "\<lbrakk>abc_fetch as ap = Some (Dec n e);
-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);
 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"
 using start_of_less[of e as "layout_of ap"] start_of_ge[of as ap n e "layout_of ap"]
 apply(case_tac "as < e", simp)
 using assms
 apply(drule_tac crsp_step_dec_b_e_pre', auto)
 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"
 apply(auto simp: crsp.simps abc_step_l.simps inv_stop.simps)
 done
 by(auto intro:wf_inv_image simp:abc_dec_2_LE_def lex_square_def lex_triple_def lex_pair_def)
 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]:
+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)+
 apply(erule_tac conjE)+
 apply(case_tac aa, simp)
 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>
 \<Longrightarrow> length (takeWhile (\<lambda>a. a = Oc) (tl aa)) <
 length (takeWhile (\<lambda>a. a = Oc) aa) - Suc 0"
 apply(erule_tac exE)+
 apply(erule_tac conjE)+
 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 +
 length (takeWhile (\<lambda>a. a = Oc) aa)"
 apply(simp only: dec_after_clear.simps)
 apply(erule_tac exE)+
 apply(erule conjE)+
 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]:
+lemma inv_check_left_moving_nonemptyE[elim]:
-"inv_check_left_moving (as, lm)
+"inv_check_left_moving (as, lm) (s, [], Oc # xs) ires
-(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"
 apply(simp only: at_begin_norm.simps inv_locate_n_b.simps)
 apply(erule_tac exE)+
 apply(case_tac "length lm2", simp)
 apply(case_tac "lm2", simp, simp)
 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"
 apply(simp only: at_begin_fst_awtn.simps inv_locate_n_b.simps )
 apply(erule exE)+
 apply(simp add: exp_ind del: replicate.simps)
 apply(rule conjI)+
 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>
 \<Longrightarrow> Suc (length (takeWhile (\<lambda>a. a = Oc) (tl aa)))
 < length (takeWhile (\<lambda>a. a = Oc) aa)"
 done
 qed
 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;
 abc_fetch as ap = Some (Dec n e)\<rbrakk>
 \<Longrightarrow> crsp (layout_of ap) (abc_step_l (as, lm) (Some (Dec n e)))
 lemma layout_id_cons: "layout_of (ap @ [p]) = layout_of ap @ [length_of p]"
 apply(simp add: layout_of.simps)
 done
-lemma [simp]: "length (layout_of xs) = length xs"
+lemma map_start_of_layout[simp]:
-by(simp add: layout_of.simps)
-lemma [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)
 done
 apply(auto simp: ci.simps tinc_b_def tdec_b_def length_findnth adjust.simps length_of.simps
 split: abc_inst.splits)
 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)"
 apply(case_tac b)
 apply(simp_all add: start_of.simps fetch.simps nth_append)

changeset 290	6e1c03614d36
parent 288	a9003e6d0463
child 291	93db7414931d