tm: comparison thys/UTM.thy

equal deleted inserted replaced

-:d5a0e25c4742
+:a9003e6d0463
 (* Title: thys/UTM.thy
 Author: Jian Xu, Xingyuan Zhang, and Christian Urban
 *)
-header {* Construction of a Universal Turing Machine *}
+chapter {* Construction of a Universal Turing Machine *}
 theory UTM
-imports Recursive Abacus UF GCD Turing_Hoare
+imports Recursive Abacus UF HOL.GCD Turing_Hoare
 begin
 section {* Wang coding of input arguments *}
 text {*
 "wcode_backto_standard_pos ires rs (l, r) = (wcode_backto_standard_pos_B ires rs (l, r) \<or>
 wcode_backto_standard_pos_O ires rs (l, r))"
 declare wcode_backto_standard_pos.simps[simp del]
-lemma [simp]: "<0::nat> = [Oc]"
-apply(simp add: tape_of_nat_abv tape_of_nat_list.simps)
-done
-lemma tape_of_Suc_nat: "<Suc (a ::nat)> = replicate a Oc @ [Oc, Oc]"
-apply(simp only: tape_of_nat_abv exp_ind, simp)
-done
-lemma [simp]: "length (<a::nat>) = Suc a"
-apply(simp add: tape_of_nat_abv tape_of_nat_list.simps)
-done
-lemma [simp]: "<[a::nat]> = <a>"
-apply(simp add: tape_of_nat_abv tape_of_nl_abv
-tape_of_nat_list.simps)
-done
 lemma bin_wc_eq: "bl_bin xs = bl2wc xs"
 proof(induct xs)
 show " bl_bin [] = bl2wc []"
 apply(simp add: bl_bin.simps)
 done
 apply(case_tac a, simp_all add: bl_bin.simps bl2wc.simps)
 apply(simp_all add: bl2nat.simps bl2nat_double)
 done
 qed
-lemma bl_bin_nat_Suc:
-"bl_bin (<Suc a>) = bl_bin (<a>) + 2^(Suc a)"
-apply(simp add: tape_of_nat_abv bl_bin.simps)
-apply(induct a, auto simp: bl_bin.simps)
-done
-lemma [simp]: " rev (a\<up>(aa)) = a\<up>(aa)"
-apply(simp)
-done
 lemma tape_of_nl_append_one: "lm \<noteq> [] \<Longrightarrow>  <lm @ [a]> = <lm> @ Bk # Oc\<up>Suc a"
 apply(induct lm, auto simp: tape_of_nl_cons split:if_splits)
 done
 lemma tape_of_nl_rev: "rev (<lm::nat list>) = (<rev lm>)"
 apply(induct lm, simp, auto)
 apply(auto simp: tape_of_nl_cons tape_of_nl_append_one split: if_splits)
 apply(simp add: exp_ind[THEN sym])
 done
-lemma [simp]: "a\<up>(Suc 0) = [a]"
+lemma exp_1[simp]: "a\<up>(Suc 0) = [a]"
 by(simp)
 lemma tape_of_nl_cons_app1: "(<a # xs @ [b]>) = (Oc\<up>(Suc a) @ Bk # (<xs@ [b]>))"
-apply(case_tac xs, simp add: tape_of_nl_abv tape_of_nat_list.simps tape_of_nat_abv)
+apply(case_tac xs; simp add: tape_of_list_def tape_of_nat_list.simps tape_of_nat_def)
-apply(simp add: tape_of_nl_abv  tape_of_nat_list.simps tape_of_nat_abv)
 done
 lemma bl_bin_bk_oc[simp]:
 "bl_bin (xs @ [Bk, Oc]) =
 bl_bin xs + 2*2^(length xs)"
 using bl2nat_cons_oc[of "xs @ [Bk]"]
 apply(simp add: bl2nat_cons_bk bl2wc.simps)
 done
 lemma tape_of_nat[simp]: "(<a::nat>) = Oc\<up>(Suc a)"
-apply(simp add: tape_of_nat_abv)
+apply(simp add: tape_of_nat_def)
 done
 lemma tape_of_nl_cons_app2: "(<c # xs @ [b]>) = (<c # xs> @ Bk # Oc\<up>(Suc b))"
-proof(induct "length xs" arbitrary: xs c,
+proof(induct "length xs" arbitrary: xs c, simp add: tape_of_list_def)
-simp add: tape_of_nl_abv  tape_of_nat_list.simps)
 fix x xs c
 assume ind: "\<And>xs c. x = length xs \<Longrightarrow> <c # xs @ [b]> =
 <c # xs> @ Bk # Oc\<up>(Suc b)"
 and h: "Suc x = length (xs::nat list)"
 show "<c # xs @ [b]> = <c # xs> @ Bk # Oc\<up>(Suc b)"
-proof(case_tac xs, simp add: tape_of_nl_abv  tape_of_nat_list.simps)
+proof(case_tac xs, simp add: tape_of_list_def  tape_of_nat_list.simps)
 fix a list
 assume g: "xs = a # list"
 hence k: "<a # list @ [b]> =  <a # list> @ Bk # Oc\<up>(Suc b)"
 apply(rule_tac ind)
 using h
 apply(simp)
 done
 from g and k show "<c # xs @ [b]> = <c # xs> @ Bk # Oc\<up>(Suc b)"
-apply(simp add: tape_of_nl_abv tape_of_nat_list.simps)
+apply(simp add: tape_of_list_def tape_of_nat_list.simps)
 done
 qed
 qed
-lemma [simp]: "length (<aa # a # list>) = Suc (Suc aa) + length (<a # list>)"
+lemma length_2_elems[simp]: "length (<aa # a # list>) = Suc (Suc aa) + length (<a # list>)"
-apply(simp add: tape_of_nl_abv tape_of_nat_list.simps)
+apply(simp add: tape_of_list_def tape_of_nat_list.simps)
 done
-lemma [simp]: "bl_bin (Oc\<up>(Suc aa) @ Bk # tape_of_nat_list (a # lista) @ [Bk, Oc]) =
+lemma bl_bin_addition[simp]: "bl_bin (Oc\<up>(Suc aa) @ Bk # tape_of_nat_list (a # lista) @ [Bk, Oc]) =
 bl_bin (Oc\<up>(Suc aa) @ Bk # tape_of_nat_list (a # lista)) +
 2* 2^(length (Oc\<up>(Suc aa) @ Bk # tape_of_nat_list (a # lista)))"
 using bl_bin_bk_oc[of "Oc\<up>(Suc aa) @ Bk # tape_of_nat_list (a # lista)"]
 apply(simp)
 done
 declare replicate_Suc[simp del]
-lemma [simp]:
+lemma bl_bin_2[simp]:
 "bl_bin (<aa # list>) + (4 * rs + 4) * 2 ^ (length (<aa # list>) - Suc 0)
 = bl_bin (Oc\<up>(Suc aa) @ Bk # <list @ [0]>) + rs * (2 * 2 ^ (aa + length (<list @ [0]>)))"
 apply(case_tac "list", simp add: add_mult_distrib)
 apply(simp add: tape_of_nl_cons_app2 add_mult_distrib)
-apply(simp add: tape_of_nl_abv tape_of_nat_list.simps)
+apply(simp add: tape_of_list_def tape_of_nat_list.simps)
 done
 lemma tape_of_nl_app_Suc: "((<list @ [Suc ab]>)) = (<list @ [ab]>) @ [Oc]"
 apply(induct list)
-apply(simp add: tape_of_nl_abv tape_of_nat_list.simps exp_ind)
+apply(simp add: tape_of_list_def tape_of_nat_list.simps exp_ind)
 apply(case_tac list)
-apply(simp_all add:tape_of_nl_abv tape_of_nat_list.simps exp_ind)
+apply(simp_all add:tape_of_list_def tape_of_nat_list.simps exp_ind)
 done
-lemma [simp]: "bl_bin (Oc # Oc\<up>(aa) @ Bk # <list @ [ab]> @ [Oc])
+lemma bl_bin_3[simp]: "bl_bin (Oc # Oc\<up>(aa) @ Bk # <list @ [ab]> @ [Oc])
 = bl_bin (Oc # Oc\<up>(aa) @ Bk # <list @ [ab]>) +
 2^(length (Oc # Oc\<up>(aa) @ Bk # <list @ [ab]>))"
 apply(simp add: bin_wc_eq)
 apply(simp add: bl2nat_cons_oc bl2wc.simps)
 using bl2nat_cons_oc[of "Oc # Oc\<up>(aa) @ Bk # <list @ [ab]>"]
 apply(simp)
 done
-lemma [simp]: "bl_bin (Oc # Oc\<up>(aa) @ Bk # <list @ [ab]>) + (4 * 2 ^ (aa + length (<list @ [ab]>)) +
+lemma bl_bin_4[simp]: "bl_bin (Oc # Oc\<up>(aa) @ Bk # <list @ [ab]>) + (4 * 2 ^ (aa + length (<list @ [ab]>)) +
 4 * (rs * 2 ^ (aa + length (<list @ [ab]>)))) =
 bl_bin (Oc # Oc\<up>(aa) @ Bk # <list @ [Suc ab]>) +
 rs * (2 * 2 ^ (aa + length (<list @ [Suc ab]>)))"
 apply(simp add: tape_of_nl_app_Suc)
 done
 wcode_double_case_step (st, l, r))"
 definition wcode_double_case_le :: "(config \<times> config) set"
 where "wcode_double_case_le \<equiv> (inv_image lex_pair wcode_double_case_measure)"
-lemma [intro]: "wf lex_pair"
+lemma wf_lex_pair[intro]: "wf lex_pair"
 by(auto intro:wf_lex_prod simp:lex_pair_def)
 lemma wf_wcode_double_case_le[intro]: "wf wcode_double_case_le"
 by(auto intro:wf_inv_image simp: wcode_double_case_le_def )
-lemma [simp]: "fetch t_wcode_main (Suc 0) Bk = (L, Suc 0)"
+lemma fetch_t_wcode_main[simp]:
-apply(simp add: t_wcode_main_def t_wcode_main_first_part_def
+"fetch t_wcode_main (Suc 0) Bk = (L, Suc 0)"
-fetch.simps nth_of.simps)
+"fetch t_wcode_main (Suc 0) Oc = (L, Suc (Suc 0))"
-done
+"fetch t_wcode_main (Suc (Suc 0)) Oc = (R, 3)"
+"fetch t_wcode_main (Suc (Suc 0)) Bk = (L, 7)"
-lemma [simp]: "fetch t_wcode_main (Suc 0) Oc = (L, Suc (Suc 0))"
+"fetch t_wcode_main (Suc (Suc (Suc 0))) Bk = (R, 4)"
-apply(simp add: t_wcode_main_def t_wcode_main_first_part_def
+"fetch t_wcode_main (Suc (Suc (Suc 0))) Oc = (W0, 3)"
-fetch.simps nth_of.simps)
+"fetch t_wcode_main 4 Bk = (R, 4)"
-done
+"fetch t_wcode_main 4 Oc = (R, 5)"
+"fetch t_wcode_main 5 Oc = (R, 5)"
-lemma [simp]: "fetch t_wcode_main (Suc (Suc 0)) Oc = (R, 3)"
+"fetch t_wcode_main 5 Bk = (W1, 6)"
-apply(simp add: t_wcode_main_def t_wcode_main_first_part_def
+"fetch t_wcode_main 6 Bk = (R, 13)"
-fetch.simps nth_of.simps)
+"fetch t_wcode_main 6 Oc = (L, 6)"
-done
+"fetch t_wcode_main 7 Oc = (R, 8)"
+"fetch t_wcode_main 7 Bk = (R, 0)"
-lemma [simp]: "fetch t_wcode_main (Suc (Suc (Suc 0))) Bk = (R, 4)"
+"fetch t_wcode_main 8 Bk = (R, 9)"
-apply(simp add: t_wcode_main_def t_wcode_main_first_part_def
+"fetch t_wcode_main 9 Bk = (R, 10)"
-fetch.simps nth_of.simps)
+"fetch t_wcode_main 9 Oc = (W0, 9)"
-done
+"fetch t_wcode_main 10 Bk = (R, 10)"
+"fetch t_wcode_main 10 Oc = (R, 11)"
-lemma [simp]: "fetch t_wcode_main (Suc (Suc (Suc 0))) Oc = (W0, 3)"
+"fetch t_wcode_main 11 Bk = (W1, 12)"
-apply(simp add: t_wcode_main_def t_wcode_main_first_part_def
+"fetch t_wcode_main 11 Oc = (R, 11)"
-fetch.simps nth_of.simps)
+"fetch t_wcode_main 12 Oc = (L, 12)"
-done
+"fetch t_wcode_main 12 Bk = (R, t_twice_len + 14)"
+by(auto simp: t_wcode_main_def t_wcode_main_first_part_def fetch.simps numeral)
-lemma [simp]: "fetch t_wcode_main 4 Bk = (R, 4)"
-apply(subgoal_tac "4 = Suc 3")
-apply(simp only: t_wcode_main_def t_wcode_main_first_part_def
-fetch.simps nth_of.simps, auto)
-done
-lemma [simp]: "fetch t_wcode_main 4 Oc = (R, 5)"
-apply(subgoal_tac "4 = Suc 3")
-apply(simp only: t_wcode_main_def t_wcode_main_first_part_def
-fetch.simps nth_of.simps, auto)
-done
-lemma [simp]: "fetch t_wcode_main 5 Oc = (R, 5)"
-apply(subgoal_tac "5 = Suc 4")
-apply(simp only: t_wcode_main_def t_wcode_main_first_part_def
-fetch.simps nth_of.simps, auto)
-done
-lemma [simp]: "fetch t_wcode_main 5 Bk = (W1, 6)"
-apply(subgoal_tac "5 = Suc 4")
-apply(simp only: t_wcode_main_def t_wcode_main_first_part_def
-fetch.simps nth_of.simps, auto)
-done
-lemma [simp]: "fetch t_wcode_main 6 Bk = (R, 13)"
-apply(subgoal_tac "6 = Suc 5")
-apply(simp only: t_wcode_main_def t_wcode_main_first_part_def
-fetch.simps nth_of.simps, auto)
-done
-lemma [simp]: "fetch t_wcode_main 6 Oc = (L, 6)"
-apply(subgoal_tac "6 = Suc 5")
-apply(simp only: t_wcode_main_def t_wcode_main_first_part_def
-fetch.simps nth_of.simps, auto)
-done
-lemma [elim]: "Bk\<up>(mr) = [] \<Longrightarrow> mr = 0"
-apply(case_tac mr, auto)
-done
-lemma [simp]: "wcode_on_left_moving_1 ires rs (b, []) = False"
-apply(simp add: wcode_on_left_moving_1.simps wcode_on_left_moving_1_B.simps
-wcode_on_left_moving_1_O.simps)
-done
 declare wcode_on_checking_1.simps[simp del]
 lemmas wcode_double_case_inv_simps =
 wcode_on_left_moving_1.simps wcode_on_left_moving_1_O.simps
 wcode_on_left_moving_1_B.simps wcode_on_checking_1.simps
 wcode_erase1.simps wcode_on_right_moving_1.simps
 wcode_goon_right_moving_1.simps wcode_backto_standard_pos.simps
-lemma [simp]: "wcode_on_left_moving_1 ires rs (b, r) \<Longrightarrow> b \<noteq> []"
+lemma wcode_on_left_moving_1[simp]:
-apply(simp add: wcode_double_case_inv_simps, auto)
+"wcode_on_left_moving_1 ires rs (b, []) = False"
-done
+"wcode_on_left_moving_1 ires rs (b, r) \<Longrightarrow> b \<noteq> []"
+by(auto simp: wcode_on_left_moving_1.simps wcode_on_left_moving_1_B.simps
+wcode_on_left_moving_1_O.simps)
-lemma [elim]: "\<lbrakk>wcode_on_left_moving_1 ires rs (b, Bk # list);
+lemma wcode_on_left_moving_1E[elim]: "\<lbrakk>wcode_on_left_moving_1 ires rs (b, Bk # list);
 tl b = aa \<and> hd b # Bk # list = ba\<rbrakk> \<Longrightarrow>
 wcode_on_left_moving_1 ires rs (aa, ba)"
 apply(simp only: wcode_on_left_moving_1.simps wcode_on_left_moving_1_O.simps
 wcode_on_left_moving_1_B.simps)
 apply(erule_tac disjE)
 apply(simp)
 done
 declare replicate_Suc[simp]
-lemma [elim]:
+lemma wcode_on_moving_1_Elim[elim]:
 "\<lbrakk>wcode_on_left_moving_1 ires rs (b, Oc # list); tl b = aa \<and> hd b # Oc # list = ba\<rbrakk>
 \<Longrightarrow> wcode_on_checking_1 ires rs (aa, ba)"
 apply(simp only: wcode_double_case_inv_simps)
 apply(erule_tac disjE)
 apply(erule_tac [!] exE)+
 apply(case_tac mr, simp, auto)
 done
-lemma [simp]: "wcode_on_checking_1 ires rs (b, []) = False"
+lemma wcode_on_checking_1_Elim[elim]: "\<lbrakk>wcode_on_checking_1 ires rs (b, Oc # ba);Oc # b = aa \<and> list = ba\<rbrakk>
-apply(auto simp: wcode_double_case_inv_simps)
-done
-lemma [simp]: "wcode_on_checking_1 ires rs (b, Bk # list) = False"
-apply(auto simp: wcode_double_case_inv_simps)
-done
-lemma [elim]: "\<lbrakk>wcode_on_checking_1 ires rs (b, Oc # ba);Oc # b = aa \<and> list = ba\<rbrakk>
 \<Longrightarrow> wcode_erase1 ires rs (aa, ba)"
 apply(simp only: wcode_double_case_inv_simps)
 apply(erule_tac exE)+
 apply(rule_tac x = ln in exI, rule_tac x = rn in exI, simp)
 done
+lemma wcode_on_checking_1_simp[simp]:
-lemma [simp]: "wcode_on_checking_1 ires rs (b, []) = False"
+"wcode_on_checking_1 ires rs (b, []) = False"
+"wcode_on_checking_1 ires rs (b, Bk # list) = False"
+by(auto simp: wcode_double_case_inv_simps)
+lemma wcode_erase1_nonempty_snd[simp]: "wcode_erase1 ires rs (b, []) = False"
 apply(simp add: wcode_double_case_inv_simps)
 done
-lemma [simp]: "wcode_on_checking_1 ires rs ([], Bk # list) = False"
+lemma wcode_on_right_moving_1_nonempty_snd[simp]: "wcode_on_right_moving_1 ires rs (b, []) = False"
 apply(simp add: wcode_double_case_inv_simps)
 done
-lemma [simp]: "wcode_erase1 ires rs (b, []) = False"
+lemma wcode_on_right_moving_1_BkE[elim]:
-apply(simp add: wcode_double_case_inv_simps)
+"\<lbrakk>wcode_on_right_moving_1 ires rs (b, Bk # ba);  Bk # b = aa \<and> list = b\<rbrakk> \<Longrightarrow>
-done
-lemma [simp]: "wcode_on_right_moving_1 ires rs (b, []) = False"
-apply(simp add: wcode_double_case_inv_simps)
-done
-lemma [simp]: "wcode_on_right_moving_1 ires rs (b, []) = False"
-apply(simp add: wcode_double_case_inv_simps)
-done
-lemma [elim]: "\<lbrakk>wcode_on_right_moving_1 ires rs (b, Bk # ba);  Bk # b = aa \<and> list = b\<rbrakk> \<Longrightarrow>
 wcode_on_right_moving_1 ires rs (aa, ba)"
 apply(simp only: wcode_double_case_inv_simps)
 apply(erule_tac exE)+
 apply(rule_tac x = "Suc ml" in exI, rule_tac x = "mr - Suc 0" in exI,
 rule_tac x = rn in exI)
 apply(simp)
 apply(case_tac mr, simp, simp)
 done
-lemma [elim]:
+lemma wcode_on_right_moving_1_OcE[elim]:
 "\<lbrakk>wcode_on_right_moving_1 ires rs (b, Oc # ba); Oc # b = aa \<and> list = ba\<rbrakk>
 \<Longrightarrow> wcode_goon_right_moving_1 ires rs (aa, ba)"
 apply(simp only: wcode_double_case_inv_simps)
 apply(erule_tac exE)+
 apply(rule_tac x = "Suc 0" in exI, rule_tac x = "rs" in exI,
 rule_tac x = "ml - Suc (Suc 0)" in exI, rule_tac x = rn in exI)
 apply(case_tac mr, simp_all)
 apply(case_tac ml, simp, case_tac nat, simp, simp)
 done
-lemma [simp]:
+lemma wcode_erase1_BkE[elim]: "\<lbrakk>wcode_erase1 ires rs (b, Bk # ba); Bk # b = aa \<and> list = ba; c = Bk # ba\<rbrakk>
-"wcode_on_right_moving_1 ires rs (b, []) \<Longrightarrow> False"
-apply(simp add: wcode_double_case_inv_simps)
-done
-lemma [elim]: "\<lbrakk>wcode_erase1 ires rs (b, Bk # ba); Bk # b = aa \<and> list = ba; c = Bk # ba\<rbrakk>
 \<Longrightarrow> wcode_on_right_moving_1 ires rs (aa, ba)"
 apply(simp only: wcode_double_case_inv_simps)
 apply(erule_tac exE)+
 apply(rule_tac x = "Suc 0" in exI, rule_tac x = "Suc (Suc ln)" in exI,
 rule_tac x = rn in exI, simp add: exp_ind del: replicate_Suc)
 done
-lemma [elim]: "\<lbrakk>wcode_erase1 ires rs (aa, Oc # list);  b = aa \<and> Bk # list = ba\<rbrakk> \<Longrightarrow>
+lemma wcode_erase1_OcE[elim]: "\<lbrakk>wcode_erase1 ires rs (aa, Oc # list);  b = aa \<and> Bk # list = ba\<rbrakk> \<Longrightarrow>
 wcode_erase1 ires rs (aa, ba)"
 apply(simp only: wcode_double_case_inv_simps)
 apply(erule_tac exE)+
 apply(rule_tac x = ln in exI, rule_tac x = rn in exI, auto)
 done
-lemma [elim]: "\<lbrakk>wcode_goon_right_moving_1 ires rs (aa, []); b = aa \<and> [Oc] = ba\<rbrakk>
+lemma wcode_goon_right_moving_1_emptyE[elim]: "\<lbrakk>wcode_goon_right_moving_1 ires rs (aa, []); b = aa \<and> [Oc] = ba\<rbrakk>
 \<Longrightarrow> wcode_backto_standard_pos ires rs (aa, ba)"
 apply(simp only: wcode_double_case_inv_simps)
 apply(erule_tac exE)+
 apply(rule_tac disjI2)
 apply(simp only:wcode_backto_standard_pos_O.simps)
 apply(rule_tac x = ml in exI, rule_tac x = "Suc 0" in exI, rule_tac x = ln in exI,
 rule_tac x = rn in exI, simp)
 done
-lemma [elim]:
+lemma wcode_goon_right_moving_1_BkE[elim]:
 "\<lbrakk>wcode_goon_right_moving_1 ires rs (aa, Bk # list);  b = aa \<and> Oc # list = ba\<rbrakk>
 \<Longrightarrow> wcode_backto_standard_pos ires rs (aa, ba)"
 apply(simp only: wcode_double_case_inv_simps)
 apply(erule_tac exE)+
 apply(rule_tac disjI2)
 apply(rule_tac x = ml in exI, rule_tac x = "Suc 0" in exI, rule_tac x = ln in exI,
 rule_tac x = "rn - Suc 0" in exI, simp)
 apply(case_tac mr, simp, case_tac rn, simp, simp_all)
 done
-lemma [elim]: "\<lbrakk>wcode_goon_right_moving_1 ires rs (b, Oc # ba);  Oc # b = aa \<and> list = ba\<rbrakk>
+lemma wcode_goon_right_moving_1_OcE[elim]: "\<lbrakk>wcode_goon_right_moving_1 ires rs (b, Oc # ba);  Oc # b = aa \<and> list = ba\<rbrakk>
 \<Longrightarrow> wcode_goon_right_moving_1 ires rs (aa, ba)"
 apply(simp only: wcode_double_case_inv_simps)
 apply(erule_tac exE)+
 apply(rule_tac x = "Suc ml" in exI, rule_tac x = "mr - Suc 0" in exI,
 rule_tac x = ln in exI, rule_tac x = rn in exI)
 apply(simp)
 apply(case_tac mr, simp, case_tac rn, simp_all)
 done
-lemma [elim]: "\<lbrakk>wcode_backto_standard_pos ires rs (b, []);  Bk # b = aa\<rbrakk> \<Longrightarrow> False"
-apply(auto simp: wcode_double_case_inv_simps wcode_backto_standard_pos_O.simps
+lemma wcode_backto_standard_pos_BkE[elim]: "\<lbrakk>wcode_backto_standard_pos ires rs (b, Bk # ba); Bk # b = aa \<and> list = ba\<rbrakk>
-wcode_backto_standard_pos_B.simps)
-done
-lemma [elim]: "\<lbrakk>wcode_backto_standard_pos ires rs (b, Bk # ba); Bk # b = aa \<and> list = ba\<rbrakk>
 \<Longrightarrow> wcode_before_double ires rs (aa, ba)"
 apply(simp only: wcode_double_case_inv_simps wcode_backto_standard_pos_B.simps
 wcode_backto_standard_pos_O.simps wcode_before_double.simps)
 apply(erule_tac disjE)
 apply(erule_tac exE)+
 apply(rule_tac x = ln in exI, rule_tac x = rn in exI, simp)
 apply(auto)
 apply(case_tac [!] mr, simp_all)
 done
-lemma [simp]: "wcode_backto_standard_pos ires rs ([], Oc # list) = False"
+lemma wcode_backto_standard_pos_no_Oc[simp]: "wcode_backto_standard_pos ires rs ([], Oc # list) = False"
 apply(auto simp: wcode_backto_standard_pos.simps wcode_backto_standard_pos_B.simps
 wcode_backto_standard_pos_O.simps)
 done
-lemma [simp]: "wcode_backto_standard_pos ires rs (b, []) = False"
+lemma wcode_backto_standard_pos_nonempty_snd[simp]: "wcode_backto_standard_pos ires rs (b, []) = False"
 apply(auto simp: wcode_backto_standard_pos.simps wcode_backto_standard_pos_B.simps
 wcode_backto_standard_pos_O.simps)
 done
-lemma [elim]: "\<lbrakk>wcode_backto_standard_pos ires rs (b, Oc # list); tl b = aa; hd b # Oc # list =  ba\<rbrakk>
+lemma wcode_backto_standard_pos_OcE[elim]: "\<lbrakk>wcode_backto_standard_pos ires rs (b, Oc # list); tl b = aa; hd b # Oc # list =  ba\<rbrakk>
 \<Longrightarrow> wcode_backto_standard_pos ires rs (aa, ba)"
 apply(simp only:  wcode_backto_standard_pos.simps wcode_backto_standard_pos_B.simps
 wcode_backto_standard_pos_O.simps)
 apply(erule_tac disjE)
 apply(simp)
 done
 thus "?thesis"
 by simp
 qed
-lemma t_twice_len_ge: "Suc 0 \<le> length t_twice div 2"
-apply(simp add: t_twice_def mopup.simps t_twice_compile_def)
-done
 declare start_of.simps[simp del]
 lemma twice_lemma: "rec_exec rec_twice [rs] = 2*rs"
 by(auto simp: rec_twice_def rec_exec.simps)
 show "tm_of abc_twice = tm_of (a [+] dummy_abc (length [rs]))"
 using h
 by(simp add: abc_twice_def)
 qed
 thus "?thesis"
-apply(simp add: tape_of_nl_abv tape_of_nat_list.simps tape_of_nat_abv rec_exec.simps twice_lemma)
+apply(simp add: tape_of_list_def tape_of_nat_def rec_exec.simps twice_lemma)
 done
 qed
 declare adjust.simps[simp]
 done
 qed
 declare tm_wf.simps[simp del]
-lemma [simp]: " tm_wf (t_twice_compile, 0)"
+lemma tm_wf_t_twice_compile [simp]: "tm_wf (t_twice_compile, 0)"
 apply(simp only: t_twice_compile_def)
 apply(rule_tac wf_tm_from_abacus, simp)
 done
 lemma t_twice_change_term_state:
 thus "?thesis"
 apply(simp add: t_twice_def t_twice_len_def)
 by metis
 qed
-lemma [intro]: "length t_wcode_main_first_part mod 2 = 0"
+lemma length_t_wcode_main_first_part_even[intro]: "length t_wcode_main_first_part mod 2 = 0"
 apply(auto simp: t_wcode_main_first_part_def)
 done
 lemma t_twice_append_pre:
 "steps0 (Suc 0, Bk # Bk # ires, Oc\<up>(Suc rs) @ Bk\<up>(n)) t_twice stp
 apply(rule_tac x = stp in exI, rule_tac x = ln in exI, rule_tac x = rn in exI)
 apply(simp)
 done
 lemma mopup_mod2: "length (mopup k) mod 2  = 0"
-apply(auto simp: mopup.simps)
+by(auto simp: mopup.simps)
-by arith
+lemma fetch_t_wcode_main_Oc[simp]: "fetch t_wcode_main (Suc (t_twice_len + length t_wcode_main_first_part div 2)) Oc
-lemma [simp]: "fetch t_wcode_main (Suc (t_twice_len + length t_wcode_main_first_part div 2)) Oc
 = (L, Suc 0)"
 apply(subgoal_tac "length (t_twice) mod 2 = 0")
 apply(simp add: t_wcode_main_def nth_append fetch.simps t_wcode_main_first_part_def
 nth_of.simps t_twice_len_def, auto)
 apply(simp add: t_twice_def t_twice_compile_def)
 apply(simp add: steps.simps step.simps exp_ind)
 apply(case_tac m, simp_all)
 apply(simp add: exp_ind[THEN sym])
 done
-lemma wcode_main_first_part_len:
+lemma wcode_main_first_part_len[simp]:
 "length t_wcode_main_first_part = 24"
 apply(simp add: t_wcode_main_first_part_def)
 done
 lemma wcode_double_case:
 definition wcode_fourtimes_case_le :: "(config \<times> config) set"
 where "wcode_fourtimes_case_le \<equiv> (inv_image lex_pair wcode_fourtimes_case_measure)"
 lemma wf_wcode_fourtimes_case_le[intro]: "wf wcode_fourtimes_case_le"
-by(auto intro:wf_inv_image simp: wcode_fourtimes_case_le_def)
+by(auto simp: wcode_fourtimes_case_le_def)
-lemma [simp]: "fetch t_wcode_main (Suc (Suc 0)) Bk = (L, 7)"
+lemma nonempty_snd [simp]:
-apply(simp add: t_wcode_main_def fetch.simps
+"wcode_on_left_moving_2 ires rs (b, []) = False"
-t_wcode_main_first_part_def nth_of.simps)
+"wcode_on_checking_2 ires rs (b, []) = False"
-done
+"wcode_goon_checking ires rs (b, []) = False"
+"wcode_right_move ires rs (b, []) = False"
-lemma [simp]: "fetch t_wcode_main 7 Oc = (R, 8)"
+"wcode_erase2 ires rs (b, []) = False"
-apply(subgoal_tac "7 = Suc 6")
+"wcode_on_right_moving_2 ires rs (b, []) = False"
-apply(simp only: t_wcode_main_def fetch.simps
+"wcode_backto_standard_pos_2 ires rs (b, []) = False"
-t_wcode_main_first_part_def nth_of.simps)
+"wcode_on_checking_2 ires rs (b, Oc # list) = False"
-apply(auto)
+by(auto simp: wcode_fourtimes_invs)
-done
+lemma wcode_on_left_moving_2[simp]:
-lemma [simp]: "fetch t_wcode_main 8 Bk = (R, 9)"
+"wcode_on_left_moving_2 ires rs (b, Bk # list) \<Longrightarrow>  wcode_on_left_moving_2 ires rs (tl b, hd b # Bk # list)"
-apply(subgoal_tac "8 = Suc 7")
-apply(simp only: t_wcode_main_def fetch.simps
-t_wcode_main_first_part_def nth_of.simps)
-apply(auto)
-done
-lemma [simp]: "fetch t_wcode_main 9 Bk = (R, 10)"
-apply(subgoal_tac "9 = Suc 8")
-apply(simp only: t_wcode_main_def fetch.simps
-t_wcode_main_first_part_def nth_of.simps)
-apply(auto)
-done
-lemma [simp]: "fetch t_wcode_main 9 Oc = (W0, 9)"
-apply(subgoal_tac "9 = Suc 8")
-apply(simp only: t_wcode_main_def fetch.simps
-t_wcode_main_first_part_def nth_of.simps)
-apply(auto)
-done
-lemma [simp]: "fetch t_wcode_main 10 Bk = (R, 10)"
-apply(subgoal_tac "10 = Suc 9")
-apply(simp only: t_wcode_main_def fetch.simps
-t_wcode_main_first_part_def nth_of.simps)
-apply(auto)
-done
-lemma [simp]: "fetch t_wcode_main 10 Oc = (R, 11)"
-apply(subgoal_tac "10 = Suc 9")
-apply(simp only: t_wcode_main_def fetch.simps
-t_wcode_main_first_part_def nth_of.simps)
-apply(auto)
-done
-lemma [simp]: "fetch t_wcode_main 11 Bk = (W1, 12)"
-apply(subgoal_tac "11 = Suc 10")
-apply(simp only: t_wcode_main_def fetch.simps
-t_wcode_main_first_part_def nth_of.simps)
-apply(auto)
-done
-lemma [simp]: "fetch t_wcode_main 11 Oc = (R, 11)"
-apply(subgoal_tac "11 = Suc 10")
-apply(simp only: t_wcode_main_def fetch.simps
-t_wcode_main_first_part_def nth_of.simps)
-apply(auto)
-done
-lemma [simp]: "fetch t_wcode_main 12 Oc = (L, 12)"
-apply(subgoal_tac "12 = Suc 11")
-apply(simp only: t_wcode_main_def fetch.simps
-t_wcode_main_first_part_def nth_of.simps)
-apply(auto)
-done
-lemma [simp]: "fetch t_wcode_main 12 Bk = (R, t_twice_len + 14)"
-apply(subgoal_tac "12 = Suc 11")
-apply(simp only: t_wcode_main_def fetch.simps
-t_wcode_main_first_part_def nth_of.simps)
-apply(auto)
-done
-lemma [simp]: "wcode_on_left_moving_2 ires rs (b, []) = False"
-apply(auto simp: wcode_fourtimes_invs)
-done
-lemma [simp]: "wcode_on_checking_2 ires rs (b, []) = False"
-apply(auto simp: wcode_fourtimes_invs)
-done
-lemma [simp]: "wcode_goon_checking ires rs (b, []) = False"
-apply(auto simp: wcode_fourtimes_invs)
-done
-lemma [simp]: "wcode_right_move ires rs (b, []) = False"
-apply(auto simp: wcode_fourtimes_invs)
-done
-lemma [simp]: "wcode_erase2 ires rs (b, []) = False"
-apply(auto simp: wcode_fourtimes_invs)
-done
-lemma [simp]: "wcode_on_right_moving_2 ires rs (b, []) = False"
-apply(auto simp: wcode_fourtimes_invs)
-done
-lemma [simp]: "wcode_backto_standard_pos_2 ires rs (b, []) = False"
-apply(auto simp: wcode_fourtimes_invs)
-done
-lemma [simp]: "wcode_on_left_moving_2 ires rs (b, Bk # list) \<Longrightarrow> b \<noteq> []"
-apply(simp add: wcode_fourtimes_invs, auto)
-done
-lemma [simp]: "wcode_on_left_moving_2 ires rs (b, Bk # list) \<Longrightarrow>  wcode_on_left_moving_2 ires rs (tl b, hd b # Bk # list)"
 apply(simp only: wcode_fourtimes_invs)
 apply(erule_tac disjE)
 apply(erule_tac exE)+
 apply(case_tac ml, simp)
 apply(rule_tac x = "mr - (Suc (Suc 0))" in exI, rule_tac x = rn in exI, simp)
 apply(rule_tac x = nat in exI, rule_tac x = "Suc mr" in exI, rule_tac x = rn in exI,
 simp add: replicate_Suc)
 apply(simp)
 done
-lemma [simp]: "wcode_on_checking_2 ires rs (b, Bk # list) \<Longrightarrow> b \<noteq> []"
+lemma wcode_goon_checking_via_2 [simp]: "wcode_on_checking_2 ires rs (b, Bk # list)
-apply(auto simp: wcode_fourtimes_invs)
-done
-lemma  [simp]: "wcode_on_checking_2 ires rs (b, Bk # list)
 \<Longrightarrow>   wcode_goon_checking ires rs (tl b, hd b # Bk # list)"
 apply(simp only: wcode_fourtimes_invs)
 apply(auto)
 done
-lemma [simp]: "wcode_goon_checking ires rs (b, Bk # list) = False"
+lemma wcode_erase2_via_move [simp]: "wcode_right_move ires rs (b, Bk # list) \<Longrightarrow>  wcode_erase2 ires rs (Bk # b, list)"
-apply(simp add: wcode_fourtimes_invs)
-done
-lemma [simp]: " wcode_right_move ires rs (b, Bk # list) \<Longrightarrow> b\<noteq> []"
-apply(simp add: wcode_fourtimes_invs)
-done
-lemma [simp]: "wcode_right_move ires rs (b, Bk # list) \<Longrightarrow>  wcode_erase2 ires rs (Bk # b, list)"
 apply(auto simp:wcode_fourtimes_invs )
 apply(rule_tac x = ln in exI, rule_tac x = rn in exI, simp)
 done
+lemma wcode_on_right_moving_2_via_erase2[simp]:
-lemma [simp]: "wcode_erase2 ires rs (b, Bk # list) \<Longrightarrow> b \<noteq> []"
+"wcode_erase2 ires rs (b, Bk # list) \<Longrightarrow> wcode_on_right_moving_2 ires rs (Bk # b, list)"
-apply(auto simp: wcode_fourtimes_invs)
-done
-lemma [simp]: "wcode_erase2 ires rs (b, Bk # list) \<Longrightarrow> wcode_on_right_moving_2 ires rs (Bk # b, list)"
 apply(auto simp:wcode_fourtimes_invs )
 apply(rule_tac x = "Suc (Suc 0)" in exI, simp add: exp_ind)
 apply(rule_tac x =  "Suc (Suc ln)" in exI, simp add: exp_ind del: replicate_Suc)
 done
-lemma [simp]: "wcode_on_right_moving_2 ires rs (b, Bk # list) \<Longrightarrow> b \<noteq> []"
+lemma wcode_on_right_moving_2_move_Bk[simp]: "wcode_on_right_moving_2 ires rs (b, Bk # list)
-apply(auto simp:wcode_fourtimes_invs )
-done
-lemma [simp]: "wcode_on_right_moving_2 ires rs (b, Bk # list)
 \<Longrightarrow> wcode_on_right_moving_2 ires rs (Bk # b, list)"
 apply(auto simp: wcode_fourtimes_invs)
 apply(rule_tac x = "Suc ml" in exI, simp)
 apply(rule_tac x = "mr - 1" in exI, case_tac mr,auto)
 done
-lemma [simp]: "wcode_goon_right_moving_2 ires rs (b, Bk # list) \<Longrightarrow> b \<noteq> []"
+lemma wcode_backto_standard_pos_2_via_right[simp]:
-apply(auto simp: wcode_fourtimes_invs)
+"wcode_goon_right_moving_2 ires rs (b, Bk # list) \<Longrightarrow>
-done
-lemma [simp]: "wcode_goon_right_moving_2 ires rs (b, Bk # list) \<Longrightarrow>
 wcode_backto_standard_pos_2 ires rs (b, Oc # list)"
 apply(simp add: wcode_fourtimes_invs, auto)
 apply(rule_tac x = ml in exI, auto)
 apply(rule_tac x = "Suc 0" in exI, simp)
 apply(case_tac mr, simp_all)
 apply(rule_tac x = "rn - 1" in exI, simp)
 apply(case_tac rn, simp, simp)
 done
-lemma  [simp]: "wcode_backto_standard_pos_2 ires rs (b, Bk # list) \<Longrightarrow>  b \<noteq> []"
+lemma wcode_on_checking_2_via_left[simp]: "wcode_on_left_moving_2 ires rs (b, Oc # list) \<Longrightarrow>
-apply(simp add: wcode_fourtimes_invs, auto)
-done
-lemma [simp]: "wcode_on_left_moving_2 ires rs (b, Oc # list) \<Longrightarrow> b \<noteq> []"
-apply(simp add: wcode_fourtimes_invs, auto)
-done
-lemma [simp]: "wcode_on_left_moving_2 ires rs (b, Oc # list) \<Longrightarrow>
 wcode_on_checking_2 ires rs (tl b, hd b # Oc # list)"
 apply(auto simp: wcode_fourtimes_invs)
 apply(case_tac [!] mr, simp_all)
 done
-lemma [simp]: "wcode_goon_right_moving_2 ires rs (b, []) \<Longrightarrow> b \<noteq> []"
+lemma wcode_backto_standard_pos_2_empty_via_right[simp]:
-apply(auto simp: wcode_fourtimes_invs)
+"wcode_goon_right_moving_2 ires rs (b, []) \<Longrightarrow>
-done
-lemma [simp]: "wcode_goon_right_moving_2 ires rs (b, []) \<Longrightarrow>
 wcode_backto_standard_pos_2 ires rs (b, [Oc])"
 apply(simp only: wcode_fourtimes_invs)
 apply(erule_tac exE)+
 apply(rule_tac disjI1)
 apply(rule_tac x = ml in exI, rule_tac x = "Suc 0" in exI,
 rule_tac x = ln in exI, rule_tac x = rn in exI, simp)
 done
-lemma "wcode_backto_standard_pos_2 ires rs (b, Bk # list)
+lemma wcode_goon_checking_cases[simp]: "wcode_goon_checking ires rs (b, Oc # list) \<Longrightarrow>
-\<Longrightarrow> (\<exists>ln. b = Bk # Bk\<up>(ln) @ Oc # ires) \<and> (\<exists>rn. list = Oc\<up>(Suc (Suc rs)) @ Bk\<up>(rn))"
-apply(auto simp: wcode_fourtimes_invs)
-apply(case_tac [!] mr, auto)
-done
-lemma [simp]: "wcode_on_checking_2 ires rs (b, Oc # list) \<Longrightarrow> False"
-apply(simp add: wcode_fourtimes_invs)
-done
-lemma [simp]: "wcode_goon_checking ires rs (b, Oc # list) \<Longrightarrow>
 (b = [] \<longrightarrow> wcode_right_move ires rs ([Oc], list)) \<and>
 (b \<noteq> [] \<longrightarrow> wcode_right_move ires rs (Oc # b, list))"
 apply(simp only: wcode_fourtimes_invs)
 apply(erule_tac exE)+
 apply(auto)
 done
-lemma [simp]: "wcode_right_move ires rs (b, Oc # list) = False"
+lemma wcode_right_move_no_Oc[simp]: "wcode_right_move ires rs (b, Oc # list) = False"
 apply(auto simp: wcode_fourtimes_invs)
 done
-lemma [simp]: " wcode_erase2 ires rs (b, Oc # list) \<Longrightarrow> b \<noteq> []"
+lemma wcode_erase2_Bk_via_Oc[simp]: "wcode_erase2 ires rs (b, Oc # list)
-apply(simp add: wcode_fourtimes_invs)
-done
-lemma [simp]: "wcode_erase2 ires rs (b, Oc # list)
 \<Longrightarrow> wcode_erase2 ires rs (b, Bk # list)"
 apply(auto simp: wcode_fourtimes_invs)
 done
-lemma [simp]: "wcode_on_right_moving_2 ires rs (b, Oc # list) \<Longrightarrow> b \<noteq> []"
+lemma wcode_goon_right_moving_2_Oc_move[simp]:
-apply(simp only: wcode_fourtimes_invs)
+"wcode_on_right_moving_2 ires rs (b, Oc # list)
-apply(auto)
-done
-lemma [simp]: "wcode_on_right_moving_2 ires rs (b, Oc # list)
 \<Longrightarrow> wcode_goon_right_moving_2 ires rs (Oc # b, list)"
 apply(auto simp: wcode_fourtimes_invs)
 apply(case_tac mr, simp_all)
 apply(rule_tac x = "Suc 0" in exI, auto)
 apply(rule_tac x = "ml - 2" in exI)
 apply(case_tac ml, simp, case_tac nat, simp_all)
 done
-lemma [simp]: "wcode_goon_right_moving_2 ires rs (b, Oc # list) \<Longrightarrow> b \<noteq> []"
+lemma wcode_backto_standard_pos_2_exists[simp]: "wcode_backto_standard_pos_2 ires rs (b, Bk # list)
-apply(simp only:wcode_fourtimes_invs, auto)
-done
-lemma [simp]: "wcode_backto_standard_pos_2 ires rs (b, Bk # list)
 \<Longrightarrow> (\<exists>ln. b = Bk # Bk\<up>(ln) @ Oc # ires) \<and> (\<exists>rn. list = Oc\<up>(Suc (Suc rs)) @ Bk\<up>(rn))"
 apply(simp add: wcode_fourtimes_invs, auto)
 apply(case_tac [!] mr, simp_all)
 done
-lemma [simp]: "wcode_on_checking_2 ires rs (b, Oc # list) = False"
+lemma wcode_goon_right_moving_2_move_Oc[simp]: "wcode_goon_right_moving_2 ires rs (b, Oc # list) \<Longrightarrow>
-apply(simp add: wcode_fourtimes_invs)
-done
-lemma [simp]: "wcode_goon_right_moving_2 ires rs (b, Oc # list) \<Longrightarrow>
 wcode_goon_right_moving_2 ires rs (Oc # b, list)"
 apply(simp only:wcode_fourtimes_invs, auto)
 apply(rule_tac x = "Suc ml" in exI, simp)
 apply(rule_tac x = "mr - 1" in exI)
 apply(case_tac mr, case_tac rn, auto)
 done
-lemma [simp]: "wcode_backto_standard_pos_2 ires rs (b, Oc # list) \<Longrightarrow> b \<noteq> []"
-apply(simp only: wcode_fourtimes_invs, auto)
+lemma wcode_backto_standard_pos_2_Oc_mv_hd[simp]:
-done
+"wcode_backto_standard_pos_2 ires rs (b, Oc # list)
-lemma [simp]: "wcode_backto_standard_pos_2 ires rs (b, Oc # list)
 \<Longrightarrow> wcode_backto_standard_pos_2 ires rs (tl b, hd b # Oc # list)"
 apply(simp only: wcode_fourtimes_invs)
 apply(erule_tac disjE)
 apply(erule_tac exE)+
 apply(case_tac ml, auto)
 apply(rule_tac x = nat in exI, auto)
 apply(rule_tac x = "Suc mr" in exI, simp)
 done
+lemma nonempty_fst[simp]:
+"wcode_on_left_moving_2 ires rs (b, Bk # list) \<Longrightarrow> b \<noteq> []"
+"wcode_on_checking_2 ires rs (b, Bk # list) \<Longrightarrow> b \<noteq> []"
+"wcode_goon_checking ires rs (b, Bk # list) = False"
+"wcode_right_move ires rs (b, Bk # list) \<Longrightarrow> b\<noteq> []"
+"wcode_erase2 ires rs (b, Bk # list) \<Longrightarrow> b \<noteq> []"
+"wcode_on_right_moving_2 ires rs (b, Bk # list) \<Longrightarrow> b \<noteq> []"
+"wcode_goon_right_moving_2 ires rs (b, Bk # list) \<Longrightarrow> b \<noteq> []"
+"wcode_backto_standard_pos_2 ires rs (b, Bk # list) \<Longrightarrow>  b \<noteq> []"
+"wcode_on_left_moving_2 ires rs (b, Oc # list) \<Longrightarrow> b \<noteq> []"
+"wcode_goon_right_moving_2 ires rs (b, []) \<Longrightarrow> b \<noteq> []"
+"wcode_erase2 ires rs (b, Oc # list) \<Longrightarrow> b \<noteq> []"
+"wcode_on_right_moving_2 ires rs (b, Oc # list) \<Longrightarrow> b \<noteq> []"
+"wcode_goon_right_moving_2 ires rs (b, Oc # list) \<Longrightarrow> b \<noteq> []"
+"wcode_backto_standard_pos_2 ires rs (b, Oc # list) \<Longrightarrow> b \<noteq> []"
+by(auto simp: wcode_fourtimes_invs)
 lemma wcode_fourtimes_case_first_correctness:
 shows "let P = (\<lambda> (st, l, r). st = t_twice_len + 14) in
 let Q = (\<lambda> (st, l, r). wcode_fourtimes_case_inv st ires rs (l, r)) in
 let f = (\<lambda> stp. steps0 (Suc 0, Bk # Bk\<up>(m) @ Oc # Bk # Oc # ires, Bk # Oc\<up>(Suc rs) @ Bk\<up>(n)) t_wcode_main stp) in
 definition t_fourtimes_len :: "nat"
 where
 "t_fourtimes_len = (length t_fourtimes div 2)"
-lemma t_fourtimes_len_gr:  "t_fourtimes_len > 0"
+lemma primerec_rec_fourtimes_1[intro]: "primerec rec_fourtimes (Suc 0)"
-apply(simp add: t_fourtimes_len_def t_fourtimes_def mopup.simps t_fourtimes_compile_def)
-done
-lemma [intro]: "primerec rec_fourtimes (Suc 0)"
 apply(auto simp: rec_fourtimes_def numeral_4_eq_4 constn.simps)
 by auto
 lemma fourtimes_lemma: "rec_exec rec_fourtimes [rs] = 4 * rs"
 by(simp add: rec_exec.simps rec_fourtimes_def)
 lemma t_fourtimes_correct:
 "\<exists>stp ln rn. steps0 (Suc 0, Bk # Bk # ires, Oc\<up>(Suc rs) @ Bk\<up>(n))
 (tm_of abc_fourtimes @ shift (mopup 1) (length (tm_of abc_fourtimes) div 2)) stp =
 (0, Bk\<up>(ln) @ Bk # Bk # ires, Oc\<up>(Suc (4 * rs)) @ Bk\<up>(rn))"
 show "tm_of abc_fourtimes = tm_of (a [+] dummy_abc (length [rs]))"
 using h
 by(simp add: abc_fourtimes_def)
 qed
 thus "?thesis"
-apply(simp add: tape_of_nl_abv tape_of_nat_list.simps tape_of_nat_abv fourtimes_lemma)
+apply(simp add: tape_of_list_def tape_of_nat_def fourtimes_lemma)
 done
 qed
 lemma wf_fourtimes[intro]: "tm_wf (t_fourtimes_compile, 0)"
 apply(simp only: t_fourtimes_compile_def)
 thus "?thesis"
 apply(simp add: t_fourtimes_def t_fourtimes_len_def)
 by metis
 qed
-lemma [intro]: "length t_twice mod 2 = 0"
+lemma length_t_twice_even[intro]: "is_even (length t_twice)"
-apply(auto simp: t_twice_def t_twice_compile_def)
+by(auto simp: t_twice_def t_twice_compile_def intro!:mopup_mod2)
-by (metis mopup_mod2)
 lemma t_fourtimes_append_pre:
 "steps0 (Suc 0, Bk # Bk # ires, Oc\<up>(Suc rs) @ Bk\<up>(n)) t_fourtimes stp
 = (Suc t_fourtimes_len, Bk\<up>(ln) @ Bk # Bk # ires, Oc\<up>(Suc (4 * rs)) @ Bk\<up>(rn))
 \<Longrightarrow> steps0 (Suc 0 + length (t_wcode_main_first_part @
 shift t_fourtimes (length (t_wcode_main_first_part @
 shift t_twice (length t_wcode_main_first_part div 2) @ [(L, 1), (L, 1)]) div 2) @ ([(L, 1), (L, 1)])) stp
 = ((Suc t_fourtimes_len) + length (t_wcode_main_first_part @
 shift t_twice (length t_wcode_main_first_part div 2) @ [(L, 1), (L, 1)]) div 2,
 Bk\<up>(ln) @ Bk # Bk # ires, Oc\<up>(Suc (4 * rs)) @ Bk\<up>(rn))"
-apply(rule_tac tm_append_shift_append_steps, simp_all)
+using length_t_twice_even
-apply(auto simp: t_wcode_main_first_part_def)
+by(intro tm_append_shift_append_steps, auto)
-done
+lemma split_26_even[simp]: "(26 + l::nat) div 2 = l div 2 + 13" by(simp)
-lemma [simp]: "length t_wcode_main_first_part = 24"
+lemma t_twice_len_plust_14[simp]: "t_twice_len + 14 =  14 + length (shift t_twice 12) div 2"
-apply(simp add: t_wcode_main_first_part_def)
-done
-lemma [simp]: "(26 + length t_twice) div 2 = (length t_twice) div 2 + 13"
-apply(simp add: t_twice_def t_twice_def)
-done
-lemma [simp]: "((26 + length (shift t_twice 12)) div 2)
-= (length (shift t_twice 12) div 2 + 13)"
-apply(simp add: t_twice_def)
-done
-lemma [simp]: "t_twice_len + 14 =  14 + length (shift t_twice 12) div 2"
 apply(simp add: t_twice_def t_twice_len_def)
 done
 lemma t_fourtimes_append:
 "\<exists> stp ln rn.
 apply(drule_tac t_fourtimes_append_pre)
 apply(rule_tac x = stp in exI, rule_tac x = ln in exI, rule_tac x = rn in exI)
 apply(simp add: t_twice_len_def)
 done
-lemma t_wcode_main_len: "length t_wcode_main = length t_twice + length t_fourtimes + 28"
-apply(simp add: t_wcode_main_def)
-done
-lemma even_twice_len: "length t_twice mod 2 = 0"
-apply(auto simp: t_twice_def t_twice_compile_def)
-by (metis mopup_mod2)
 lemma even_fourtimes_len: "length t_fourtimes mod 2 = 0"
 apply(auto simp: t_fourtimes_def t_fourtimes_compile_def)
 by (metis mopup_mod2)
-lemma [simp]: "2 * (length t_twice div 2) = length t_twice"
+lemma t_twice_even[simp]: "2 * (length t_twice div 2) = length t_twice"
-using even_twice_len
+using length_t_twice_even by arith
-by arith
+lemma t_fourtimes_even[simp]: "2 * (length t_fourtimes div 2) = length t_fourtimes"
-lemma [simp]: "2 * (length t_fourtimes div 2) = length t_fourtimes"
 using even_fourtimes_len
 by arith
-lemma [simp]: "fetch t_wcode_main (14 + length t_twice div 2 + t_fourtimes_len) Oc
+lemma fetch_t_wcode_14_Oc: "fetch t_wcode_main (14 + length t_twice div 2 + t_fourtimes_len) Oc
 = (L, Suc 0)"
 apply(subgoal_tac "14 = Suc 13")
 apply(simp only: fetch.simps add_Suc nth_of.simps t_wcode_main_def)
-apply(simp add:length_append length_shift Parity.two_times_even_div_two even_twice_len t_fourtimes_len_def nth_append)
+apply(simp add:length_t_twice_even t_fourtimes_len_def nth_append)
 by arith
-lemma [simp]: "fetch t_wcode_main (14 + length t_twice div 2 + t_fourtimes_len) Bk
+lemma fetch_t_wcode_14_Bk: "fetch t_wcode_main (14 + length t_twice div 2 + t_fourtimes_len) Bk
 = (L, Suc 0)"
 apply(subgoal_tac "14 = Suc 13")
 apply(simp only: fetch.simps add_Suc nth_of.simps t_wcode_main_def)
-apply(simp add:length_append length_shift Parity.two_times_even_div_two even_twice_len t_fourtimes_len_def nth_append)
+apply(simp add:length_t_twice_even t_fourtimes_len_def nth_append)
 by arith
-lemma [simp]: "fetch t_wcode_main (14 + length t_twice div 2 + t_fourtimes_len) b
+lemma fetch_t_wcode_14 [simp]: "fetch t_wcode_main (14 + length t_twice div 2 + t_fourtimes_len) b
 = (L, Suc 0)"
-apply(case_tac b, simp_all)
+apply(case_tac b, simp_all add:fetch_t_wcode_14_Bk fetch_t_wcode_14_Oc)
 done
 lemma wcode_jump2:
 "\<exists> stp ln rn. steps0 (t_twice_len + 14 + t_fourtimes_len
 , Bk # Bk # Bk\<up>(lnb) @ Oc # ires, Oc\<up>(Suc (4 * rs + 4)) @ Bk\<up>(rnb)) t_wcode_main stp =
 (Suc 0, Bk # Bk\<up>(lnc) @ Oc # ires, Bk # Oc\<up>(Suc (4*rs + 4)) @ Bk\<up>(rnc))"
 by blast
 from stp1 stp2 stp3 show "?thesis"
 apply(rule_tac x = "stpa + stpb + stpc" in exI,
 rule_tac x = lnc in exI, rule_tac x = rnc in exI)
-apply(simp add: steps_add)
+apply(simp)
 done
 qed
 fun wcode_on_left_moving_3_B :: "bin_inv_t"
 where
 lemmas wcode_halt_invs =
 wcode_on_left_moving_3_B.simps wcode_on_left_moving_3_O.simps
 wcode_on_checking_3.simps wcode_goon_checking_3.simps
 wcode_on_left_moving_3.simps wcode_stop.simps
-lemma [simp]: "fetch t_wcode_main 7 Bk = (R, 0)"
-apply(subgoal_tac "7 = Suc 6")
+lemma wcode_on_left_moving_3_mv_Bk[simp]: "wcode_on_left_moving_3 ires rs (b, Bk # list)
-apply(simp only: fetch.simps t_wcode_main_def nth_append nth_of.simps
-t_wcode_main_first_part_def)
-apply(auto)
-done
-lemma [simp]: "wcode_on_left_moving_3 ires rs (b, [])  = False"
-apply(simp only: wcode_halt_invs)
-apply(simp)
-done
-lemma [simp]: "wcode_on_checking_3 ires rs (b, []) = False"
-apply(simp add: wcode_halt_invs)
-done
-lemma [simp]: "wcode_goon_checking_3 ires rs (b, []) = False"
-apply(simp add: wcode_halt_invs)
-done
-lemma [simp]: "wcode_on_left_moving_3 ires rs (b, Bk # list)
 \<Longrightarrow> wcode_on_left_moving_3 ires rs (tl b, hd b # Bk # list)"
 apply(simp only: wcode_halt_invs)
 apply(erule_tac disjE)
 apply(erule_tac exE)+
 apply(case_tac ml, simp)
 apply(rule_tac x = nat in exI, rule_tac x = "Suc mr" in exI,
 rule_tac x = rn in exI, simp)
 apply(simp)
 done
-lemma [simp]: "wcode_goon_checking_3 ires rs (b, Bk # list) \<Longrightarrow>
+lemma wcode_goon_checking_3_cases[simp]: "wcode_goon_checking_3 ires rs (b, Bk # list) \<Longrightarrow>
 (b = [] \<longrightarrow> wcode_stop ires rs ([Bk], list)) \<and>
 (b \<noteq> [] \<longrightarrow> wcode_stop ires rs (Bk # b, list))"
 apply(auto simp: wcode_halt_invs)
 done
-lemma [simp]: "wcode_on_left_moving_3 ires rs (b, Oc # list) \<Longrightarrow> b \<noteq> []"
+lemma wcode_on_checking_3_mv_Oc[simp]: "wcode_on_left_moving_3 ires rs (b, Oc # list) \<Longrightarrow>
-apply(auto simp: wcode_halt_invs)
-done
-lemma [simp]: "wcode_on_left_moving_3 ires rs (b, Oc # list) \<Longrightarrow>
 wcode_on_checking_3 ires rs (tl b, hd b # Oc # list)"
 apply(simp add:wcode_halt_invs, auto)
 apply(case_tac [!] mr, simp_all)
 done
-lemma [simp]: "wcode_on_checking_3 ires rs (b, Oc # list) = False"
+lemma wcode_3_nonempty[simp]:
-apply(auto simp: wcode_halt_invs)
+"wcode_on_left_moving_3 ires rs (b, []) = False"
-done
+"wcode_on_checking_3 ires rs (b, []) = False"
+"wcode_goon_checking_3 ires rs (b, []) = False"
-lemma [simp]: "wcode_on_left_moving_3 ires rs (b, Bk # list) \<Longrightarrow> b \<noteq> []"
+"wcode_on_left_moving_3 ires rs (b, Oc # list) \<Longrightarrow> b \<noteq> []"
-apply(simp add: wcode_halt_invs, auto)
+"wcode_on_checking_3 ires rs (b, Oc # list) = False"
-done
+"wcode_on_left_moving_3 ires rs (b, Bk # list) \<Longrightarrow> b \<noteq> []"
+"wcode_on_checking_3 ires rs (b, Bk # list) \<Longrightarrow> b \<noteq> []"
-lemma [simp]: "wcode_on_checking_3 ires rs (b, Bk # list) \<Longrightarrow> b \<noteq> []"
+"wcode_goon_checking_3 ires rs (b, Oc # list) = False"
-apply(auto simp: wcode_halt_invs)
+by(auto simp: wcode_halt_invs)
-done
+lemma wcode_goon_checking_3_mv_Bk[simp]: "wcode_on_checking_3 ires rs (b, Bk # list) \<Longrightarrow>
-lemma [simp]: "wcode_on_checking_3 ires rs (b, Bk # list) \<Longrightarrow>
 wcode_goon_checking_3 ires rs (tl b, hd b # Bk # list)"
 apply(auto simp: wcode_halt_invs)
-done
-lemma [simp]: "wcode_goon_checking_3 ires rs (b, Oc # list) = False"
-apply(simp add: wcode_goon_checking_3.simps)
 done
 lemma t_halt_case_correctness:
 shows "let P = (\<lambda> (st, l, r). st = 0) in
 let Q = (\<lambda> (st, l, r). wcode_halt_case_inv st ires rs (l, r)) in
 apply(auto)
 done
 qed
 declare wcode_halt_case_inv.simps[simp del]
-lemma [intro]: "\<exists> xs. (<rev list @ [aa::nat]> :: cell list) = Oc # xs"
+lemma leading_Oc[intro]: "\<exists> xs. (<rev list @ [aa::nat]> :: cell list) = Oc # xs"
 apply(case_tac "rev list", simp)
 apply(simp add: tape_of_nl_cons)
 done
 lemma wcode_halt_case:
 apply(auto simp: wcode_halt_case_inv.simps wcode_stop.simps)
 apply(rule_tac x = na in exI, rule_tac x = ln in exI,
 rule_tac x = rn in exI, simp)
 done
-lemma bl_bin_one: "bl_bin [Oc] =  Suc 0"
+lemma bl_bin_one[simp]: "bl_bin [Oc] = 1"
 apply(simp add: bl_bin.simps)
 done
-lemma [simp]: "bl_bin [Oc] = 1"
+lemma twice_power[intro]: "2 * 2 ^ a = Suc (Suc (2 * bl_bin (Oc \<up> a)))"
-apply(simp add: bl_bin.simps)
-done
-lemma [intro]: "2 * 2 ^ a = Suc (Suc (2 * bl_bin (Oc \<up> a)))"
 apply(induct a, auto simp: bl_bin.simps)
 done
 declare replicate_Suc[simp del]
 lemma t_wcode_main_lemma_pre:
 (Suc 0, Bk # Bk\<up>(lna) @ rev (<a>) @ Bk # Bk # ires, Bk # Oc\<up>(Suc (2 * rs + 2)) @ Bk\<up>(rna))" by blast
 moreover have
 "\<exists>stp ln rn.
 steps0 (Suc 0,  Bk # Bk\<up>(lna) @ rev (<a::nat>) @ Bk # Bk # ires, Bk # Oc\<up>(Suc (2 * rs + 2)) @ Bk\<up>(rna)) t_wcode_main stp =
 (0, Bk # ires, Bk # Oc # Bk\<up>(ln) @ Bk # Bk # Oc\<up>(bl_bin (<a>) + (2*rs + 2)  * 2 ^ a) @ Bk\<up>(rn))"
-using ind2[of lna ires "2*rs + 2" rna] by(simp add: tape_of_nl_abv tape_of_nat_abv)
+using ind2[of lna ires "2*rs + 2" rna] by(simp add: tape_of_list_def tape_of_nat_def)
 from this obtain stpb lnb rnb where stp2:
 "steps0 (Suc 0,  Bk # Bk\<up>(lna) @ rev (<a>) @ Bk # Bk # ires, Bk # Oc\<up>(Suc (2 * rs + 2)) @ Bk\<up>(rna)) t_wcode_main stpb =
 (0, Bk # ires, Bk # Oc # Bk\<up>(lnb) @ Bk # Bk # Oc\<up>(bl_bin (<a>) + (2*rs + 2)  * 2 ^ a) @ Bk\<up>(rnb))"
 by blast
 from stp1 and stp2 show "?thesis"
 apply(rule_tac x = "stpa + stpb" in exI,
-rule_tac x = lnb in exI, rule_tac x = rnb in exI, simp add: tape_of_nat_abv)
+rule_tac x = lnb in exI, rule_tac x = rnb in exI, simp add: tape_of_nat_def)
 apply(simp add:  bl_bin.simps replicate_Suc)
 apply(auto)
 done
 qed
 qed
 wprepare_step (st, l, r))"
 definition wcode_prepare_le :: "(config \<times> config) set"
 where "wcode_prepare_le \<equiv> (inv_image lex_triple wcode_prepare_measure)"
-lemma [intro]: "wf lex_pair"
-by(auto intro:wf_lex_prod simp:lex_pair_def)
 lemma wf_wcode_prepare_le[intro]: "wf wcode_prepare_le"
 by(auto intro:wf_inv_image simp: wcode_prepare_le_def
 lex_triple_def)
 declare wprepare_add_one.simps[simp del] wprepare_goto_first_end.simps[simp del]
 wprepare_erase.simps wprepare_goto_start_pos.simps
 wprepare_loop_start.simps wprepare_loop_goon.simps
 wprepare_add_one2.simps
 declare wprepare_inv.simps[simp del]
-lemma [simp]: "fetch t_wcode_prepare (Suc 0) Bk = (W1, 2)"
-apply(simp add: fetch.simps t_wcode_prepare_def nth_of.simps)
+lemma fetch_t_wcode_prepare[simp]:
-done
+"fetch t_wcode_prepare (Suc 0) Bk = (W1, 2)"
+"fetch t_wcode_prepare (Suc 0) Oc = (L, 1)"
-lemma [simp]: "fetch t_wcode_prepare (Suc 0) Oc = (L, 1)"
+"fetch t_wcode_prepare (Suc (Suc 0)) Bk = (L, 3)"
-apply(simp add: fetch.simps t_wcode_prepare_def nth_of.simps)
+"fetch t_wcode_prepare (Suc (Suc 0)) Oc = (R, 2)"
-done
+"fetch t_wcode_prepare (Suc (Suc (Suc 0))) Bk = (R, 4)"
+"fetch t_wcode_prepare (Suc (Suc (Suc 0))) Oc = (W0, 3)"
-lemma [simp]: "fetch t_wcode_prepare (Suc (Suc 0)) Bk = (L, 3)"
+"fetch t_wcode_prepare 4 Bk = (R, 4)"
-apply(simp add: fetch.simps t_wcode_prepare_def nth_of.simps)
+"fetch t_wcode_prepare 4 Oc = (R, 5)"
-done
+"fetch t_wcode_prepare 5 Oc = (R, 5)"
+"fetch t_wcode_prepare 5 Bk = (R, 6)"
-lemma [simp]: "fetch t_wcode_prepare (Suc (Suc 0)) Oc = (R, 2)"
+"fetch t_wcode_prepare 6 Oc = (R, 5)"
-apply(simp add: fetch.simps t_wcode_prepare_def nth_of.simps)
+"fetch t_wcode_prepare 6 Bk = (R, 7)"
-done
+"fetch t_wcode_prepare 7 Oc = (L, 0)"
+"fetch t_wcode_prepare 7 Bk = (W1, 7)"
-lemma [simp]: "fetch t_wcode_prepare (Suc (Suc (Suc 0))) Bk = (R, 4)"
+unfolding fetch.simps t_wcode_prepare_def nth_of.simps
-apply(simp add: fetch.simps t_wcode_prepare_def nth_of.simps)
+numeral by auto
-done
+lemma wprepare_add_one_nonempty_snd[simp]: "lm \<noteq> [] \<Longrightarrow> wprepare_add_one m lm (b, []) = False"
-lemma [simp]: "fetch t_wcode_prepare (Suc (Suc (Suc 0))) Oc = (W0, 3)"
-apply(simp add: fetch.simps t_wcode_prepare_def nth_of.simps)
-done
-lemma [simp]: "fetch t_wcode_prepare 4 Bk = (R, 4)"
-apply(subgoal_tac "4 = Suc 3")
-apply(simp_all only: fetch.simps t_wcode_prepare_def nth_of.simps)
-apply(auto)
-done
-lemma [simp]: "fetch t_wcode_prepare 4 Oc = (R, 5)"
-apply(subgoal_tac "4 = Suc 3")
-apply(simp_all only: fetch.simps t_wcode_prepare_def nth_of.simps)
-apply(auto)
-done
-lemma [simp]: "fetch t_wcode_prepare 5 Oc = (R, 5)"
-apply(subgoal_tac "5 = Suc 4")
-apply(simp_all only: fetch.simps t_wcode_prepare_def nth_of.simps)
-apply(auto)
-done
-lemma [simp]: "fetch t_wcode_prepare 5 Bk = (R, 6)"
-apply(subgoal_tac "5 = Suc 4")
-apply(simp_all only: fetch.simps t_wcode_prepare_def nth_of.simps)
-apply(auto)
-done
-lemma [simp]: "fetch t_wcode_prepare 6 Oc = (R, 5)"
-apply(subgoal_tac "6 = Suc 5")
-apply(simp_all only: fetch.simps t_wcode_prepare_def nth_of.simps)
-apply(auto)
-done
-lemma [simp]: "fetch t_wcode_prepare 6 Bk = (R, 7)"
-apply(subgoal_tac "6 = Suc 5")
-apply(simp_all only: fetch.simps t_wcode_prepare_def nth_of.simps)
-apply(auto)
-done
-lemma [simp]: "fetch t_wcode_prepare 7 Oc = (L, 0)"
-apply(subgoal_tac "7 = Suc 6")
-apply(simp_all only: fetch.simps t_wcode_prepare_def nth_of.simps)
-apply(auto)
-done
-lemma [simp]: "fetch t_wcode_prepare 7 Bk = (W1, 7)"
-apply(subgoal_tac "7 = Suc 6")
-apply(simp_all only: fetch.simps t_wcode_prepare_def nth_of.simps)
-apply(auto)
-done
-lemma [simp]: "lm \<noteq> [] \<Longrightarrow> wprepare_add_one m lm (b, []) = False"
 apply(simp add: wprepare_invs)
 done
-lemma [simp]: "lm \<noteq> [] \<Longrightarrow> wprepare_goto_first_end m lm (b, []) = False"
+lemma wprepare_goto_first_end_nonempty_snd[simp]: "lm \<noteq> [] \<Longrightarrow> wprepare_goto_first_end m lm (b, []) = False"
 apply(simp add: wprepare_invs)
 done
-lemma [simp]: "lm \<noteq> [] \<Longrightarrow> wprepare_erase m lm (b, []) = False"
+lemma wprepare_erase_nonempty_snd[simp]: "lm \<noteq> [] \<Longrightarrow> wprepare_erase m lm (b, []) = False"
 apply(simp add: wprepare_invs)
 done
-lemma [simp]: "lm \<noteq> [] \<Longrightarrow> wprepare_goto_start_pos m lm (b, []) = False"
+lemma wprepare_goto_start_pos_nonempty_snd[simp]: "lm \<noteq> [] \<Longrightarrow> wprepare_goto_start_pos m lm (b, []) = False"
 apply(simp add: wprepare_invs)
 done
-lemma [simp]: "\<lbrakk>lm \<noteq> []; wprepare_loop_start m lm (b, [])\<rbrakk> \<Longrightarrow> b \<noteq> []"
+lemma wprepare_loop_start_empty_nonempty_fst[simp]: "\<lbrakk>lm \<noteq> []; wprepare_loop_start m lm (b, [])\<rbrakk> \<Longrightarrow> b \<noteq> []"
 apply(simp add: wprepare_invs)
 done
-lemma rev_eq: "rev xs = rev ys \<Longrightarrow> xs = ys"
+lemma rev_eq: "rev xs = rev ys \<Longrightarrow> xs = ys" by auto
-by auto
+lemma wprepare_loop_goon_Bk_empty_snd[simp]: "\<lbrakk>lm \<noteq> []; wprepare_loop_start m lm (b, [])\<rbrakk> \<Longrightarrow>
-lemma [simp]: "\<lbrakk>lm \<noteq> []; wprepare_loop_start m lm (b, [])\<rbrakk> \<Longrightarrow>
 wprepare_loop_goon m lm (Bk # b, [])"
 apply(simp only: wprepare_invs)
 apply(erule_tac disjE)
 apply(rule_tac disjI2)
 apply(simp add: wprepare_loop_start_on_rightmost.simps
 wprepare_loop_goon_on_rightmost.simps, auto)
 apply(rule_tac rev_eq, simp add: tape_of_nl_rev)
 done
-lemma [simp]: "\<lbrakk>lm \<noteq> []; wprepare_loop_goon m lm (b, [])\<rbrakk> \<Longrightarrow> b \<noteq> []"
+lemma wprepare_loop_goon_nonempty_fst[simp]: "\<lbrakk>lm \<noteq> []; wprepare_loop_goon m lm (b, [])\<rbrakk> \<Longrightarrow> b \<noteq> []"
 apply(simp only: wprepare_invs, auto)
 done
-lemma [simp]:"\<lbrakk>lm \<noteq> []; wprepare_loop_goon m lm (b, [])\<rbrakk> \<Longrightarrow>
+lemma wprepare_add_one2_Bk_empty[simp]:"\<lbrakk>lm \<noteq> []; wprepare_loop_goon m lm (b, [])\<rbrakk> \<Longrightarrow>
 wprepare_add_one2 m lm (Bk # b, [])"
 apply(simp only: wprepare_invs, auto split: if_splits)
 done
-lemma [simp]: "wprepare_add_one2 m lm (b, []) \<Longrightarrow> b \<noteq> []"
+lemma wprepare_add_one2_nonempty_fst[simp]: "wprepare_add_one2 m lm (b, []) \<Longrightarrow> b \<noteq> []"
 apply(simp only: wprepare_invs, auto)
 done
-lemma [simp]: "wprepare_add_one2 m lm (b, []) \<Longrightarrow> wprepare_add_one2 m lm (b, [Oc])"
+lemma wprepare_add_one2_Oc[simp]: "wprepare_add_one2 m lm (b, []) \<Longrightarrow> wprepare_add_one2 m lm (b, [Oc])"
 apply(simp only: wprepare_invs, auto)
 done
-lemma [simp]: "Bk # list = <(m::nat) # lm> @ ys = False"
+lemma Bk_not_tape_start[simp]: "(Bk # list = <(m::nat) # lm> @ ys) = False"
 apply(case_tac lm, auto simp: tape_of_nl_cons replicate_Suc)
 done
-lemma [simp]: "\<lbrakk>lm \<noteq> []; wprepare_add_one m lm (b, Bk # list)\<rbrakk>
+lemma wprepare_goto_first_end_cases[simp]:
+"\<lbrakk>lm \<noteq> []; wprepare_add_one m lm (b, Bk # list)\<rbrakk>
 \<Longrightarrow> (b = [] \<longrightarrow> wprepare_goto_first_end m lm ([], Oc # list)) \<and>
 (b \<noteq> [] \<longrightarrow> wprepare_goto_first_end m lm (b, Oc # list))"
 apply(simp only: wprepare_invs)
 apply(auto simp: tape_of_nl_cons split: if_splits)
 apply(rule_tac x = 0 in exI, simp add: replicate_Suc)
-apply(case_tac lm, simp, simp add: tape_of_nl_abv tape_of_nat_list.simps replicate_Suc)
+apply(case_tac lm, simp, simp add: tape_of_list_def tape_of_nat_list.simps replicate_Suc)
 done
-lemma [simp]: "wprepare_goto_first_end m lm (b, Bk # list) \<Longrightarrow> b \<noteq> []"
+lemma wprepare_goto_first_end_Bk_nonempty_fst[simp]:
+"wprepare_goto_first_end m lm (b, Bk # list) \<Longrightarrow> b \<noteq> []"
 apply(simp only: wprepare_invs , auto simp: replicate_Suc)
 done
 declare replicate_Suc[simp]
-lemma [simp]: "wprepare_goto_first_end m lm (b, Bk # list) \<Longrightarrow>
+lemma wprepare_erase_elem_Bk_rest[simp]: "wprepare_goto_first_end m lm (b, Bk # list) \<Longrightarrow>
 wprepare_erase m lm (tl b, hd b # Bk # list)"
 apply(simp only: wprepare_invs, auto)
 apply(case_tac mr, simp_all)
 apply(case_tac mr, auto)
 done
-lemma [simp]: "wprepare_erase m lm (b, Bk # list) \<Longrightarrow> b \<noteq> []"
+lemma wprepare_erase_Bk_nonempty_fst[simp]: "wprepare_erase m lm (b, Bk # list) \<Longrightarrow> b \<noteq> []"
 apply(simp only: wprepare_invs, auto)
 done
-lemma [simp]: "wprepare_erase m lm (b, Bk # list) \<Longrightarrow>
+lemma wprepare_goto_start_pos_Bk[simp]: "wprepare_erase m lm (b, Bk # list) \<Longrightarrow>
 wprepare_goto_start_pos m lm (Bk # b, list)"
 apply(simp only: wprepare_invs, auto)
 done
-lemma [simp]: "\<lbrakk>wprepare_add_one m lm (b, Bk # list)\<rbrakk> \<Longrightarrow> list \<noteq> []"
+lemma wprepare_add_one_Bk_nonempty_snd[simp]: "\<lbrakk>wprepare_add_one m lm (b, Bk # list)\<rbrakk> \<Longrightarrow> list \<noteq> []"
 apply(simp only: wprepare_invs)
-apply(case_tac lm, simp_all add: tape_of_nl_abv
+apply(case_tac lm, simp_all add: tape_of_list_def tape_of_nat_def, auto)
-tape_of_nat_list.simps tape_of_nat_abv, auto)
 done
-lemma [simp]: "\<lbrakk>lm \<noteq> [];  wprepare_goto_first_end m lm (b, Bk # list)\<rbrakk> \<Longrightarrow> list \<noteq> []"
+lemma wprepare_goto_first_end_nonempty_snd_tl[simp]:
+"\<lbrakk>lm \<noteq> [];  wprepare_goto_first_end m lm (b, Bk # list)\<rbrakk> \<Longrightarrow> list \<noteq> []"
 apply(simp only: wprepare_invs, auto)
 apply(case_tac mr, simp_all)
 done
-lemma [simp]: "\<lbrakk>lm \<noteq> [];  wprepare_goto_first_end m lm (b, Bk # list)\<rbrakk> \<Longrightarrow> b \<noteq> []"
+lemma wprepare_erase_Bk_nonempty_list[simp]: "\<lbrakk>lm \<noteq> []; wprepare_erase m lm (b, Bk # list)\<rbrakk> \<Longrightarrow> list \<noteq> []"
 apply(simp only: wprepare_invs, auto)
 done
-lemma [simp]: "\<lbrakk>lm \<noteq> []; wprepare_erase m lm (b, Bk # list)\<rbrakk> \<Longrightarrow> list \<noteq> []"
-apply(simp only: wprepare_invs, auto)
+lemma wprepare_goto_start_pos_Bk_nonempty[simp]: "\<lbrakk>lm \<noteq> [];  wprepare_goto_start_pos m lm (b, Bk # list)\<rbrakk> \<Longrightarrow> list \<noteq> []"
-done
+by(cases lm;cases list;simp only: wprepare_invs, auto)
-lemma [simp]: "\<lbrakk>lm \<noteq> []; wprepare_erase m lm (b, Bk # list)\<rbrakk> \<Longrightarrow> b \<noteq> []"
+lemma wprepare_goto_start_pos_Bk_nonempty_fst[simp]: "\<lbrakk>lm \<noteq> [];  wprepare_goto_start_pos m lm (b, Bk # list)\<rbrakk> \<Longrightarrow> b \<noteq> []"
-apply(simp only: wprepare_invs, auto)
-done
-lemma [simp]: "\<lbrakk>lm \<noteq> [];  wprepare_goto_start_pos m lm (b, Bk # list)\<rbrakk> \<Longrightarrow> list \<noteq> []"
-apply(simp only: wprepare_invs, auto)
-apply(case_tac lm, simp, case_tac list)
-apply(simp_all add: tape_of_nl_abv tape_of_nat_list.simps tape_of_nat_abv)
-done
-lemma [simp]: "\<lbrakk>lm \<noteq> [];  wprepare_goto_start_pos m lm (b, Bk # list)\<rbrakk> \<Longrightarrow> b \<noteq> []"
 apply(simp only: wprepare_invs)
 apply(auto)
 done
-lemma [simp]: "\<lbrakk>lm \<noteq> []; wprepare_loop_goon m lm (b, Bk # list)\<rbrakk> \<Longrightarrow> b \<noteq> []"
+lemma wprepare_loop_goon_Bk_nonempty[simp]: "\<lbrakk>lm \<noteq> []; wprepare_loop_goon m lm (b, Bk # list)\<rbrakk> \<Longrightarrow> b \<noteq> []"
 apply(simp only: wprepare_invs, auto)
 done
-lemma [simp]: "\<lbrakk>lm \<noteq> []; wprepare_loop_goon m lm (b, Bk # list)\<rbrakk> \<Longrightarrow>
+lemma wprepare_loop_goon_wprepare_add_one2_cases[simp]: "\<lbrakk>lm \<noteq> []; wprepare_loop_goon m lm (b, Bk # list)\<rbrakk> \<Longrightarrow>
 (list = [] \<longrightarrow> wprepare_add_one2 m lm (Bk # b, [])) \<and>
 (list \<noteq> [] \<longrightarrow> wprepare_add_one2 m lm (Bk # b, list))"
-apply(simp only: wprepare_invs, simp)
+unfolding wprepare_invs
-apply(case_tac list, simp_all split: if_splits, auto)
+apply(cases list;auto split:nat.split if_splits)
 apply(case_tac [1-3] mr, simp_all add: )
 apply(case_tac mr, simp_all)
 apply(case_tac [1-2] mr, simp_all add: )
-apply(case_tac rn, simp, case_tac nat, auto simp: )
+apply(case_tac rn, force, case_tac nat, auto simp: )
 done
-lemma [simp]: "wprepare_add_one2 m lm (b, Bk # list) \<Longrightarrow> b \<noteq> []"
+lemma wprepare_add_one2_nonempty[simp]: "wprepare_add_one2 m lm (b, Bk # list) \<Longrightarrow> b \<noteq> []"
 apply(simp only: wprepare_invs, simp)
 done
-lemma [simp]: "wprepare_add_one2 m lm (b, Bk # list) \<Longrightarrow>
+lemma wprepare_add_one2_cases[simp]: "wprepare_add_one2 m lm (b, Bk # list) \<Longrightarrow>
 (list = [] \<longrightarrow> wprepare_add_one2 m lm (b, [Oc])) \<and>
 (list \<noteq> [] \<longrightarrow> wprepare_add_one2 m lm (b, Oc # list))"
 apply(simp only:  wprepare_invs, auto)
 done
-lemma [simp]: "wprepare_goto_first_end m lm (b, Oc # list)
+lemma wprepare_goto_first_end_cases_Oc[simp]: "wprepare_goto_first_end m lm (b, Oc # list)
 \<Longrightarrow> (b = [] \<longrightarrow> wprepare_goto_first_end m lm ([Oc], list)) \<and>
 (b \<noteq> [] \<longrightarrow> wprepare_goto_first_end m lm (Oc # b, list))"
 apply(simp only:  wprepare_invs, auto)
 apply(rule_tac x = 1 in exI, auto)
 apply(case_tac mr, simp_all add: )
 apply(case_tac ml, simp_all add: )
 apply(rule_tac x = "Suc ml" in exI, simp_all add: )
 apply(rule_tac x = "mr - 1" in exI, simp)
 done
-lemma [simp]: "wprepare_erase m lm (b, Oc # list) \<Longrightarrow> b \<noteq> []"
+lemma wprepare_erase_nonempty[simp]: "wprepare_erase m lm (b, Oc # list) \<Longrightarrow> b \<noteq> []"
 apply(simp only: wprepare_invs, auto simp: )
 done
-lemma [simp]: "wprepare_erase m lm (b, Oc # list)
+lemma wprepare_erase_Bk[simp]: "wprepare_erase m lm (b, Oc # list)
 \<Longrightarrow> wprepare_erase m lm (b, Bk # list)"
 apply(simp  only:wprepare_invs, auto simp: )
 done
-lemma [simp]: "\<lbrakk>lm \<noteq> []; wprepare_goto_start_pos m lm (b, Bk # list)\<rbrakk>
+lemma wprepare_goto_start_pos_Bk_move[simp]: "\<lbrakk>lm \<noteq> []; wprepare_goto_start_pos m lm (b, Bk # list)\<rbrakk>
 \<Longrightarrow> wprepare_goto_start_pos m lm (Bk # b, list)"
 apply(simp only:wprepare_invs, auto)
 apply(case_tac [!] lm, simp, simp_all)
 done
-lemma [simp]: "wprepare_loop_start m lm (b, aa) \<Longrightarrow> b \<noteq> []"
+lemma wprepare_loop_start_b_nonempty[simp]: "wprepare_loop_start m lm (b, aa) \<Longrightarrow> b \<noteq> []"
 apply(simp only:wprepare_invs, auto)
 done
-lemma [elim]: "Bk # list = Oc\<up>(mr) @ Bk\<up>(rn)  \<Longrightarrow> \<exists>rn. list = Bk\<up>(rn)"
+lemma exists_exp_of_Bk[elim]: "Bk # list = Oc\<up>(mr) @ Bk\<up>(rn)  \<Longrightarrow> \<exists>rn. list = Bk\<up>(rn)"
 apply(case_tac mr, simp_all)
 apply(case_tac rn, simp_all)
 done
-lemma rev_equal_iff: "x = y \<Longrightarrow> rev x = rev y"
+lemma wprepare_loop_start_in_middle_Bk_False[simp]: "wprepare_loop_start_in_middle m lm (b, [Bk]) = False"
-by simp
-lemma tape_of_nl_false1:
-"lm \<noteq> [] \<Longrightarrow> rev b @ [Bk] \<noteq> Bk\<up>(ln) @ Oc # Oc\<up>(m) @ Bk # Bk # <lm::nat list>"
-apply(auto)
-apply(drule_tac rev_equal_iff, simp add: tape_of_nl_rev)
-apply(case_tac "rev lm")
-apply(case_tac [2] list, auto simp: tape_of_nl_abv tape_of_nat_list.simps tape_of_nat_abv)
-done
-lemma [simp]: "wprepare_loop_start_in_middle m lm (b, [Bk]) = False"
 apply(simp add: wprepare_loop_start_in_middle.simps, auto)
 apply(case_tac mr, simp_all add: )
 done
 declare wprepare_loop_start_in_middle.simps[simp del]
 declare wprepare_loop_start_on_rightmost.simps[simp del]
 wprepare_loop_goon_in_middle.simps[simp del]
 wprepare_loop_goon_on_rightmost.simps[simp del]
-lemma [simp]: "wprepare_loop_goon_in_middle m lm (Bk # b, []) = False"
+lemma wprepare_loop_goon_in_middle_Bk_False[simp]: "wprepare_loop_goon_in_middle m lm (Bk # b, []) = False"
 apply(simp add: wprepare_loop_goon_in_middle.simps, auto)
 done
-lemma [simp]: "\<lbrakk>lm \<noteq> []; wprepare_loop_start m lm (b, [Bk])\<rbrakk> \<Longrightarrow>
+lemma wprepare_loop_goon_Bk[simp]: "\<lbrakk>lm \<noteq> []; wprepare_loop_start m lm (b, [Bk])\<rbrakk> \<Longrightarrow>
 wprepare_loop_goon m lm (Bk # b, [])"
 apply(simp only: wprepare_invs, simp)
 apply(simp add: wprepare_loop_goon_on_rightmost.simps
 wprepare_loop_start_on_rightmost.simps, auto)
 apply(case_tac mr, simp_all add: )
 apply(rule_tac rev_eq)
 apply(simp add: tape_of_nl_rev)
 apply(simp add: exp_ind replicate_Suc[THEN sym] del: replicate_Suc)
 done
-lemma [simp]: "wprepare_loop_start_on_rightmost m lm (b, Bk # a # lista)
+lemma wprepare_loop_goon_in_middle_Bk_False2[simp]: "wprepare_loop_start_on_rightmost m lm (b, Bk # a # lista)
 \<Longrightarrow> wprepare_loop_goon_in_middle m lm (Bk # b, a # lista) = False"
 apply(auto simp: wprepare_loop_start_on_rightmost.simps
 wprepare_loop_goon_in_middle.simps)
 done
-lemma [simp]: "\<lbrakk>lm \<noteq> []; wprepare_loop_start_on_rightmost m lm (b, Bk # a # lista)\<rbrakk>
+lemma wprepare_loop_goon_on_rightbmost_Bk_False[simp]: "\<lbrakk>lm \<noteq> []; wprepare_loop_start_on_rightmost m lm (b, Bk # a # lista)\<rbrakk>
 \<Longrightarrow> wprepare_loop_goon_on_rightmost m lm (Bk # b, a # lista)"
 apply(simp only: wprepare_loop_start_on_rightmost.simps
 wprepare_loop_goon_on_rightmost.simps, auto)
 apply(case_tac mr, simp_all add: )
 apply(simp add: tape_of_nl_rev)
 apply(simp add: replicate_Suc[THEN sym] exp_ind del: replicate_Suc)
 done
-lemma [simp]: "\<lbrakk>lm \<noteq> []; wprepare_loop_start_in_middle m lm (b, Bk # a # lista)\<rbrakk>
+lemma wprepare_loop_goon_on_rightbmost_Bk_False_2[simp]: "\<lbrakk>lm \<noteq> []; wprepare_loop_start_in_middle m lm (b, Bk # a # lista)\<rbrakk>
 \<Longrightarrow> wprepare_loop_goon_on_rightmost m lm (Bk # b, a # lista) = False"
 apply(simp add: wprepare_loop_start_in_middle.simps
 wprepare_loop_goon_on_rightmost.simps, auto)
 apply(case_tac mr, simp_all add: )
 apply(case_tac  "lm1::nat list", simp_all, case_tac  list, simp)
-apply(simp add: tape_of_nl_abv tape_of_nat_list.simps tape_of_nat_abv )
+apply(simp add: tape_of_list_def tape_of_nat_list.simps tape_of_nat_def )
 apply(case_tac [!] rna, simp_all add: )
 apply(case_tac mr, simp_all add: )
 apply(case_tac lm1, simp, case_tac list, simp)
-apply(simp_all add: tape_of_nl_abv tape_of_nat_list.simps  tape_of_nat_abv)
+apply(simp_all add: tape_of_list_def tape_of_nat_list.simps  tape_of_nat_def)
 done
-lemma [simp]:
+lemma wprepare_loop_goon_in_middle_Bk_False3[simp]:
 "\<lbrakk>lm \<noteq> []; wprepare_loop_start_in_middle m lm (b, Bk # a # lista)\<rbrakk>
 \<Longrightarrow> wprepare_loop_goon_in_middle m lm (Bk # b, a # lista)"
 apply(simp add: wprepare_loop_start_in_middle.simps
 wprepare_loop_goon_in_middle.simps, auto)
 apply(rule_tac x = rn in exI, simp)
 apply(case_tac mr, simp_all add: )
 apply(case_tac lm1, simp)
 apply(rule_tac x = "Suc aa" in exI, simp)
 apply(rule_tac x = list in exI)
-apply(case_tac list, simp_all add: tape_of_nl_abv tape_of_nat_list.simps tape_of_nat_abv)
+apply(case_tac list, simp_all add: tape_of_list_def  tape_of_nat_def)
 done
-lemma [simp]: "\<lbrakk>lm \<noteq> []; wprepare_loop_start m lm (b, Bk # a # lista)\<rbrakk> \<Longrightarrow>
+lemma wprepare_loop_goon_Bk2[simp]: "\<lbrakk>lm \<noteq> []; wprepare_loop_start m lm (b, Bk # a # lista)\<rbrakk> \<Longrightarrow>
 wprepare_loop_goon m lm (Bk # b, a # lista)"
 apply(simp add: wprepare_loop_start.simps
 wprepare_loop_goon.simps)
 apply(erule_tac disjE, simp, auto)
 done
 \<Longrightarrow> (hd b = Oc \<longrightarrow> (b = [] \<longrightarrow> wprepare_add_one m lm ([], Bk # Oc # list)) \<and>
 (b \<noteq> [] \<longrightarrow> wprepare_add_one m lm (tl b, Oc # Oc # list))) \<and>
 (hd b \<noteq> Oc \<longrightarrow> (b = [] \<longrightarrow> wprepare_add_one m lm ([], Bk # Oc # list)) \<and>
 (b \<noteq> [] \<longrightarrow> wprepare_add_one m lm (tl b, hd b # Oc # list)))"
 apply(simp only: wprepare_add_one.simps, auto)
 done
-lemma [simp]: "wprepare_loop_start m lm (b, Oc # list) \<Longrightarrow> b \<noteq> []"
+lemma wprepare_loop_start_on_rightmost_Oc[simp]: "wprepare_loop_start_on_rightmost m lm (b, Oc # list) \<Longrightarrow>
-apply(simp)
-done
-lemma [simp]: "wprepare_loop_start_on_rightmost m lm (b, Oc # list) \<Longrightarrow>
 wprepare_loop_start_on_rightmost m lm (Oc # b, list)"
 apply(simp add: wprepare_loop_start_on_rightmost.simps, auto)
 apply(rule_tac x = rn in exI, auto)
 apply(case_tac mr, simp_all add: )
 done
-lemma [simp]: "wprepare_loop_start_in_middle m lm (b, Oc # list) \<Longrightarrow>
+lemma wprepare_loop_start_in_middle_Oc[simp]: "wprepare_loop_start_in_middle m lm (b, Oc # list) \<Longrightarrow>
 wprepare_loop_start_in_middle m lm (Oc # b, list)"
 apply(simp add: wprepare_loop_start_in_middle.simps, auto)
 apply(rule_tac x = rn in exI, auto)
 apply(case_tac mr, simp, simp add: )
 apply(rule_tac x = nat in exI, simp)
 wprepare_loop_start m lm (Oc # b, list)"
 apply(simp add: wprepare_loop_start.simps)
 apply(erule_tac disjE, simp_all )
 done
-lemma [simp]: "wprepare_loop_goon m lm (b, Oc # list) \<Longrightarrow> b \<noteq> []"
+lemma wprepare_loop_goon_Oc_nonempty[simp]: "wprepare_loop_goon m lm (b, Oc # list) \<Longrightarrow> b \<noteq> []"
 apply(simp add: wprepare_loop_goon.simps
 wprepare_loop_goon_in_middle.simps
 wprepare_loop_goon_on_rightmost.simps)
 apply(auto)
 done
-lemma [simp]: "wprepare_goto_start_pos m lm (b, Oc # list) \<Longrightarrow> b \<noteq> []"
+lemma wprepare_goto_start_pos_Oc_nonempty[simp]: "wprepare_goto_start_pos m lm (b, Oc # list) \<Longrightarrow> b \<noteq> []"
 apply(simp add: wprepare_goto_start_pos.simps)
 done
-lemma [simp]: "wprepare_loop_goon_on_rightmost m lm (b, Oc # list) = False"
+lemma wprepare_loop_goon_on_rightmost_Oc_False[simp]: "wprepare_loop_goon_on_rightmost m lm (b, Oc # list) = False"
 apply(simp add: wprepare_loop_goon_on_rightmost.simps)
 done
 lemma wprepare_loop1: "\<lbrakk>rev b @ Oc\<up>(mr) =  Oc\<up>(Suc m) @ Bk # Bk # <lm>;
 b \<noteq> []; 0 < mr; Oc # list = Oc\<up>(mr) @ Bk\<up>(rn)\<rbrakk>
 apply(case_tac mr, simp_all add: )
 apply(rule_tac x = nat in exI, simp)
 apply(rule_tac x = "a#lista" in exI, simp)
 done
-lemma [simp]: "wprepare_loop_goon_in_middle m lm (b, Oc # list) \<Longrightarrow>
+lemma wprepare_loop_goon_in_middle_cases[simp]: "wprepare_loop_goon_in_middle m lm (b, Oc # list) \<Longrightarrow>
 wprepare_loop_start_on_rightmost m lm (Oc # b, list) \<or>
 wprepare_loop_start_in_middle m lm (Oc # b, list)"
 apply(simp add: wprepare_loop_goon_in_middle.simps split: if_splits)
 apply(case_tac lm1, simp_all add: wprepare_loop1 wprepare_loop2)
 done
-lemma [simp]: "wprepare_loop_goon m lm (b, Oc # list)
+lemma wprepare_loop_start_Oc[simp]: "wprepare_loop_goon m lm (b, Oc # list)
 \<Longrightarrow>  wprepare_loop_start m lm (Oc # b, list)"
 apply(simp add: wprepare_loop_goon.simps
 wprepare_loop_start.simps)
 done
-lemma [simp]: "wprepare_add_one m lm (b, Oc # list)
+lemma wprepare_add_one_b[simp]: "wprepare_add_one m lm (b, Oc # list)
 \<Longrightarrow> b = [] \<longrightarrow> wprepare_add_one m lm ([], Bk # Oc # list)"
 apply(auto)
 apply(simp add: wprepare_add_one.simps)
 done
-lemma [simp]: "wprepare_goto_start_pos m [a] (b, Oc # list)
+lemma wprepare_loop_start_on_rightmost_Oc2[simp]: "wprepare_goto_start_pos m [a] (b, Oc # list)
 \<Longrightarrow> wprepare_loop_start_on_rightmost m [a] (Oc # b, list) "
 apply(auto simp: wprepare_goto_start_pos.simps
 wprepare_loop_start_on_rightmost.simps)
 apply(rule_tac x = rn in exI, simp)
 apply(simp add: replicate_Suc[THEN sym] exp_ind del: replicate_Suc)
 done
-lemma [simp]:  "wprepare_goto_start_pos m (a # aa # listaa) (b, Oc # list)
+lemma wprepare_loop_start_in_middle_2_Oc[simp]:  "wprepare_goto_start_pos m (a # aa # listaa) (b, Oc # list)
 \<Longrightarrow>wprepare_loop_start_in_middle m (a # aa # listaa) (Oc # b, list)"
 apply(auto simp: wprepare_goto_start_pos.simps
 wprepare_loop_start_in_middle.simps)
 apply(rule_tac x = rn in exI, simp)
 apply(simp add: exp_ind[THEN sym])
 apply(rule_tac x = a in exI, rule_tac x = "aa#listaa" in exI, simp)
 apply(simp add: tape_of_nl_cons)
 done
-lemma [simp]: "\<lbrakk>lm \<noteq> []; wprepare_goto_start_pos m lm (b, Oc # list)\<rbrakk>
+lemma wprepare_loop_start_Oc2[simp]: "\<lbrakk>lm \<noteq> []; wprepare_goto_start_pos m lm (b, Oc # list)\<rbrakk>
 \<Longrightarrow> wprepare_loop_start m lm (Oc # b, list)"
 apply(case_tac lm, simp_all)
 apply(case_tac lista, simp_all add: wprepare_loop_start.simps)
 done
-lemma [simp]: "wprepare_add_one2 m lm (b, Oc # list) \<Longrightarrow> b \<noteq> []"
+lemma wprepare_add_one2_Oc_nonempty[simp]: "wprepare_add_one2 m lm (b, Oc # list) \<Longrightarrow> b \<noteq> []"
 apply(auto simp: wprepare_add_one2.simps)
 done
 lemma add_one_2_stop:
 "wprepare_add_one2 m lm (b, Oc # list)
 \<Longrightarrow>  wprepare_stop m lm (tl b, hd b # Oc # list)"
-apply(simp add: wprepare_stop.simps wprepare_add_one2.simps)
+apply(simp add: wprepare_add_one2.simps)
 done
 declare wprepare_stop.simps[simp del]
 lemma wprepare_correctness:
 using h
 apply(rule_tac allI, rule_tac impI, case_tac "?f n",
 simp add: step_red step.simps)
 apply(case_tac c, simp, case_tac [2] aa)
 apply(simp_all add: wprepare_inv.simps wcode_prepare_le_def lex_triple_def lex_pair_def
-split: if_splits)
+split: if_splits) (* slow *)
 apply(simp_all add: start_2_goon  start_2_start
 add_one_2_add_one add_one_2_stop)
 apply(auto simp: wprepare_add_one2.simps)
 done
 next
 thus "?thesis"
 apply(auto)
 done
 qed
-lemma [intro]: "tm_wf (t_wcode_prepare, 0)"
+lemma tm_wf_t_wcode_prepare[intro]: "tm_wf (t_wcode_prepare, 0)"
 apply(simp add:tm_wf.simps t_wcode_prepare_def)
 done
-lemma t_correct_shift:
+lemma is_28_even[intro]: "(28 + (length t_twice_compile + length t_fourtimes_compile)) mod 2 = 0"
-"list_all (\<lambda>(acn, st). (st \<le> y)) tp \<Longrightarrow>
+by(auto simp: t_twice_compile_def t_fourtimes_compile_def)
-list_all (\<lambda>(acn, st). (st \<le> y + off)) (shift tp off) "
-apply(auto simp: List.list_all_length)
+lemma b_le_28[elim]: "(a, b) \<in> set t_wcode_main_first_part \<Longrightarrow>
-apply(erule_tac x = n in allE, simp add: length_shift)
-apply(case_tac "tp!n", auto simp: shift.simps)
-done
-lemma [intro]: "(28 + (length t_twice_compile + length t_fourtimes_compile)) mod 2 = 0"
-apply(auto simp: t_twice_compile_def t_fourtimes_compile_def)
-by arith
-lemma [elim]: "(a, b) \<in> set t_wcode_main_first_part \<Longrightarrow>
 b \<le> (28 + (length t_twice_compile + length t_fourtimes_compile)) div 2"
 apply(auto simp: t_wcode_main_first_part_def t_twice_def)
 done
-lemma tm_wf_change_termi: "tm_wf (tp, 0) \<Longrightarrow>
+lemma tm_wf_change_termi:
-list_all (\<lambda>(acn, st). (st \<le> Suc (length tp div 2))) (adjust0 tp)"
+assumes "tm_wf (tp, 0)"
-apply(auto simp: tm_wf.simps List.list_all_length)
+shows "list_all (\<lambda>(acn, st). (st \<le> Suc (length tp div 2))) (adjust0 tp)"
-apply(case_tac "tp!n", auto simp: adjust.simps split: if_splits)
+proof -
-apply(erule_tac x = "(a, b)" in ballE, auto)
+{ fix acn st n
-by (metis in_set_conv_nth)
+assume "tp ! n = (acn, st)" "n < length tp" "0 < st"
+hence "(acn, st)\<in>set tp" by (metis nth_mem)
+with assms tm_wf.simps have "st \<le> length tp div 2 + 0" by auto
+hence "st \<le> Suc (length tp div 2)" by auto
+}
+thus ?thesis
+by(auto simp: tm_wf.simps List.list_all_length adjust.simps split: if_splits prod.split)
+qed
 lemma tm_wf_shift:
 "list_all (\<lambda>(acn, st). (st \<le> y)) tp \<Longrightarrow>
 list_all (\<lambda>(acn, st). (st \<le> y + off)) (shift tp off) "
 apply(auto simp: tm_wf.simps List.list_all_length)
 apply(case_tac "tp!n", auto simp: shift.simps)
 done
 declare length_tp'[simp del]
-lemma [simp]: "length (mopup (Suc 0)) = 16"
+lemma length_mopup_1[simp]: "length (mopup (Suc 0)) = 16"
 apply(auto simp: mopup.simps)
 done
-lemma [elim]: "(a, b) \<in> set (shift (adjust0 t_twice_compile) 12) \<Longrightarrow>
+lemma twice_plus_28_elim[elim]: "(a, b) \<in> set (shift (adjust0 t_twice_compile) 12) \<Longrightarrow>
 b \<le> (28 + (length t_twice_compile + length t_fourtimes_compile)) div 2"
 apply(simp add: t_twice_compile_def t_fourtimes_compile_def)
 proof -
 assume g: "(a, b)
 \<in> set (shift
 moreover have "length (tm_of abc_twice) mod 2 = 0" by auto
 moreover have "length (tm_of abc_fourtimes) mod 2 = 0" by auto
 ultimately have "list_all (\<lambda>(acn, st). (st \<le> (60 + (length (tm_of abc_twice) + length (tm_of abc_fourtimes))) div 2))
 (shift (adjust0 t_twice_compile) 12)"
 proof(auto simp add: mod_ex1 del: adjust.simps)
-fix q qa
+assume "even (length (tm_of abc_twice))"
-assume h: "length (tm_of abc_twice) = 2 * q" "length (tm_of abc_fourtimes) = 2 * qa"
+then obtain q where q:"length (tm_of abc_twice) = 2 * q" by auto
+assume "even (length (tm_of abc_fourtimes))"
+then obtain qa where qa:"length (tm_of abc_fourtimes) = 2 * qa" by auto
+note h = q qa
 hence "list_all (\<lambda>(acn, st). st \<le> (18 + (q + qa)) + 12) (shift (adjust0 t_twice_compile) 12)"
 proof(rule_tac tm_wf_shift t_twice_compile_def)
 have "list_all (\<lambda>(acn, st). st \<le> Suc (length t_twice_compile div 2)) (adjust0 t_twice_compile)"
 by(rule_tac tm_wf_change_termi, auto)
 thus "list_all (\<lambda>(acn, st). st \<le> 18 + (q + qa)) (adjust0 t_twice_compile)"
 using h
 apply(simp add: t_twice_compile_def, auto simp: List.list_all_length)
 done
 qed
-thus "list_all (\<lambda>(acn, st). st \<le> 30 + (q + qa))
+thus "list_all (\<lambda>(acn, st). st \<le> 30 + (length (tm_of abc_twice) div 2 + length (tm_of abc_fourtimes) div 2))
-(shift
+(shift (adjust0 t_twice_compile) 12)" using h
-(adjust t_twice_compile (Suc (length t_twice_compile div 2))) 12)"
 by simp
 qed
 thus "b \<le> (60 + (length (tm_of abc_twice) + length (tm_of abc_fourtimes))) div 2"
 using g
 apply(auto simp:t_twice_compile_def)
 apply(simp add: Ball_set[THEN sym])
 apply(erule_tac x = "(a, b)" in ballE, simp, simp)
 done
 qed
-lemma [elim]: "(a, b) \<in> set (shift (adjust0 t_fourtimes_compile) (t_twice_len + 13))
+lemma length_plus_28_elim2[elim]: "(a, b) \<in> set (shift (adjust0 t_fourtimes_compile) (t_twice_len + 13))
 \<Longrightarrow> b \<le> (28 + (length t_twice_compile + length t_fourtimes_compile)) div 2"
 apply(simp add: t_twice_compile_def t_fourtimes_compile_def t_twice_len_def)
 proof -
 assume g: "(a, b)
 \<in> set (shift
-(adjust
+(adjust (tm_of abc_fourtimes @ shift (mopup (Suc 0)) (length (tm_of abc_fourtimes) div 2))
-(tm_of abc_fourtimes @
+(Suc ((length (tm_of abc_fourtimes) + 16) div 2)))
-shift (mopup (Suc 0)) (length (tm_of abc_fourtimes) div 2))
+(length t_twice div 2 + 13))"
-(Suc ((length (tm_of abc_fourtimes) + 16) div 2)))
-(length t_twice div 2 + 13))"
 moreover have "length (tm_of abc_twice) mod 2 = 0" by auto
 moreover have "length (tm_of abc_fourtimes) mod 2 = 0" by auto
 ultimately have "list_all (\<lambda>(acn, st). (st \<le> (60 + (length (tm_of abc_twice) + length (tm_of abc_fourtimes))) div 2))
 (shift (adjust0 (tm_of abc_fourtimes @ shift (mopup (Suc 0))
 (length (tm_of abc_fourtimes) div 2))) (length t_twice div 2 + 13))"
 proof(auto simp: mod_ex1 t_twice_def t_twice_compile_def)
-fix q qa
+assume "even (length (tm_of abc_twice))"
-assume h: "length (tm_of abc_twice) = 2 * q" "length (tm_of abc_fourtimes) = 2 * qa"
+then obtain q where q:"length (tm_of abc_twice) = 2 * q" by auto
+assume "even (length (tm_of abc_fourtimes))"
+then obtain qa where qa:"length (tm_of abc_fourtimes) = 2 * qa" by auto
+note h = q qa
 hence "list_all (\<lambda>(acn, st). st \<le> (9 + qa + (21 + q)))
 (shift (adjust0 (tm_of abc_fourtimes @ shift (mopup (Suc 0)) qa)) (21 + q))"
 proof(rule_tac tm_wf_shift t_twice_compile_def)
 have "list_all (\<lambda>(acn, st). st \<le> Suc (length (tm_of abc_fourtimes @ shift
 (mopup (Suc 0)) qa) div 2)) (adjust0 (tm_of abc_fourtimes @ shift (mopup (Suc 0)) qa))"
 2)))"
 using h
 apply(simp)
 done
 qed
-thus "list_all (\<lambda>(acn, st). st \<le> 30 + (q + qa))
+thus "list_all
-(shift
+(\<lambda>(acn, st). st \<le> 30 + (length (tm_of abc_twice) div 2 + length (tm_of abc_fourtimes) div 2))
-(adjust (tm_of abc_fourtimes @ shift (mopup (Suc 0)) qa)
+(shift
-(9 + qa))
+(adjust (tm_of abc_fourtimes @ shift (mopup (Suc 0)) (length (tm_of abc_fourtimes) div 2))
-(21 + q))"
+(9 + length (tm_of abc_fourtimes) div 2))
+(21 + length (tm_of abc_twice) div 2))"
 apply(subgoal_tac "qa + q = q + qa")
 apply(simp add: h)
 apply(simp)
 done
 qed
 apply(simp add: Ball_set[THEN sym])
 apply(erule_tac x = "(a, b)" in ballE, simp, simp)
 done
 qed
-lemma [intro]: "tm_wf (t_wcode_main, 0)"
+lemma tm_wf_t_wcode_main[intro]: "tm_wf (t_wcode_main, 0)"
-apply(auto simp: t_wcode_main_def tm_wf.simps
+by(auto simp: t_wcode_main_def tm_wf.simps
 t_twice_def t_fourtimes_def del: List.list_all_iff)
-done
 declare tm_comp.simps[simp del]
 lemma tm_wf_comp: "\<lbrakk>tm_wf (A, 0); tm_wf (B, 0)\<rbrakk> \<Longrightarrow> tm_wf (A |+| B, 0)"
-apply(auto simp: tm_wf.simps shift.simps adjust.simps tm_comp_length
+by(auto simp: tm_wf.simps shift.simps adjust.simps tm_comp_length
-tm_comp.simps)
+tm_comp.simps) auto
-done
-lemma [intro]: "tm_wf (t_wcode_prepare |+| t_wcode_main, 0)"
-apply(rule_tac tm_wf_comp, auto)
-done
 lemma prepare_mainpart_lemma:
 "args \<noteq> [] \<Longrightarrow>
 \<exists> stp ln rn. steps0 (Suc 0, [], <m # args>) (t_wcode_prepare |+| t_wcode_main) stp
 = (0,  Bk # Oc\<up>(Suc m), Bk # Oc # Bk\<up>(ln) @ Bk # Bk # Oc\<up>(bl_bin (<args>)) @ Bk\<up>(rn))"
 definition tinres :: "cell list \<Rightarrow> cell list \<Rightarrow> bool"
 where
 "tinres xs ys = (\<exists>n. xs = ys @ Bk \<up> n \<or> ys = xs @ Bk \<up> n)"
-lemma [simp]:  "tinres r r' \<Longrightarrow>
+lemma tinres_fetch_congr[simp]:  "tinres r r' \<Longrightarrow>
 fetch t ss (read r) =
 fetch t ss (read r')"
 apply(simp add: fetch.simps, auto split: if_splits simp: tinres_def)
 apply(case_tac [!] n, simp_all)
 done
-lemma [intro]: "\<exists> n. (a::cell)\<up>(n) = []"
+lemma nonempty_hd_tinres[simp]: "\<lbrakk>tinres r r'; r \<noteq> []; r' \<noteq> []\<rbrakk> \<Longrightarrow> hd r = hd r'"
-by auto
-lemma [simp]: "\<lbrakk>tinres r r'; r \<noteq> []; r' \<noteq> []\<rbrakk> \<Longrightarrow> hd r = hd r'"
 apply(auto simp: tinres_def)
 done
-lemma [intro]: "hd (Bk\<up>(Suc n)) = Bk"
+lemma tinres_nonempty[simp]:
-apply(simp add: )
+"\<lbrakk>tinres r []; r \<noteq> []\<rbrakk> \<Longrightarrow> hd r = Bk"
-done
+"\<lbrakk>tinres [] r'; r' \<noteq> []\<rbrakk> \<Longrightarrow> hd r' = Bk"
+"\<lbrakk>tinres r [];  r \<noteq> []\<rbrakk> \<Longrightarrow> tinres (tl r) []"
-lemma [simp]: "\<lbrakk>tinres r []; r \<noteq> []\<rbrakk> \<Longrightarrow> hd r = Bk"
+"tinres r r' \<Longrightarrow> tinres (b # r) (b # r')"
-apply(auto simp: tinres_def)
+by(auto simp: tinres_def)
-done
+lemma ex_move_tl[intro]: "\<exists>na. tl r = tl (r @ Bk\<up>(n)) @ Bk\<up>(na) \<or> tl (r @ Bk\<up>(n)) = tl r @ Bk\<up>(na)"
-lemma [simp]: "\<lbrakk>tinres [] r'; r' \<noteq> []\<rbrakk> \<Longrightarrow> hd r' = Bk"
-apply(auto simp: tinres_def)
-done
-lemma [intro]: "\<exists>na. tl r = tl (r @ Bk\<up>(n)) @ Bk\<up>(na) \<or> tl (r @ Bk\<up>(n)) = tl r @ Bk\<up>(na)"
 apply(case_tac r, simp)
 apply(case_tac n, simp, simp)
 apply(rule_tac x = nat in exI, simp)
 apply(rule_tac x = n in exI, simp)
 done
-lemma [simp]: "tinres r r' \<Longrightarrow> tinres (tl r) (tl r')"
+lemma tinres_tails[simp]: "tinres r r' \<Longrightarrow> tinres (tl r) (tl r')"
 apply(auto simp: tinres_def)
 apply(case_tac r', simp)
 apply(case_tac n, simp_all)
 apply(rule_tac x = nat in exI, simp)
 apply(rule_tac x = n in exI, simp)
 done
-lemma [simp]: "\<lbrakk>tinres r [];  r \<noteq> []\<rbrakk> \<Longrightarrow> tinres (tl r) []"
+lemma tinres_empty[simp]:
-apply(case_tac r, auto simp: tinres_def)
+"\<lbrakk>tinres [] r'\<rbrakk> \<Longrightarrow> tinres [] (tl r')"
-apply(case_tac n, simp_all add: )
+"tinres r [] \<Longrightarrow> tinres (Bk # tl r) [Bk]"
-apply(rule_tac x = nat in exI, simp)
+"tinres r [] \<Longrightarrow> tinres (Oc # tl r) [Oc]"
-done
+by(auto simp: tinres_def)
-lemma [simp]: "\<lbrakk>tinres [] r'\<rbrakk> \<Longrightarrow> tinres [] (tl r')"
+lemma tinres_step2:
-apply(case_tac r', auto simp: tinres_def)
+assumes "tinres r r'" "step0 (ss, l, r) t = (sa, la, ra)" "step0 (ss, l, r') t = (sb, lb, rb)"
-apply(case_tac n, simp_all add: )
+shows "la = lb \<and> tinres ra rb \<and> sa = sb"
-apply(rule_tac x = nat in exI, simp)
+proof (cases "fetch t ss (read r')")
-done
+case (Pair a b)
+have sa:"sa = sb" using assms Pair by(force simp: step.simps)
-lemma [simp]: "tinres r r' \<Longrightarrow> tinres (b # r) (b # r')"
+have "la = lb \<and> tinres ra rb" using assms Pair
-apply(auto simp: tinres_def)
+by(cases a, auto simp: step.simps split: if_splits)
-done
+thus ?thesis using sa by auto
+qed
-lemma [simp]: "tinres r [] \<Longrightarrow> tinres (Bk # tl r) [Bk]"
-apply(auto simp: tinres_def)
-done
-lemma [simp]: "tinres r [] \<Longrightarrow> tinres (Oc # tl r) [Oc]"
-apply(auto simp: tinres_def)
-done
-lemma tinres_step2:
-"\<lbrakk>tinres r r'; step0 (ss, l, r) t = (sa, la, ra); step0 (ss, l, r') t = (sb, lb, rb)\<rbrakk>
-\<Longrightarrow> la = lb \<and> tinres ra rb \<and> sa = sb"
-apply(case_tac "ss = 0", simp add: step_0)
-apply(simp add: step.simps [simp del], auto)
-apply(case_tac [!] "fetch t ss (read r')", simp)
-apply(auto simp: update.simps)
-apply(case_tac [!] a, auto split: if_splits)
-done
 lemma tinres_steps2:
 "\<lbrakk>tinres r r'; steps0 (ss, l, r) t stp = (sa, la, ra); steps0 (ss, l, r') t stp = (sb, lb, rb)\<rbrakk>
 \<Longrightarrow> la = lb \<and> tinres ra rb \<and> sa = sb"
 apply(induct stp arbitrary: sa la ra sb lb rb, simp add: steps.simps)
 "t_wcode_adjust = [(W1, 1), (R, 2), (Nop, 2), (R, 3), (R, 3), (R, 4),
 (L, 8), (L, 5), (L, 6), (W0, 5), (L, 6), (R, 7),
 (W1, 2), (Nop, 7), (L, 9), (W0, 8), (L, 9), (L, 10),
 (L, 11), (L, 10), (R, 0), (L, 11)]"
-lemma [simp]: "fetch t_wcode_adjust (Suc 0) Bk = (W1, 1)"
+lemma fetch_t_wcode_adjust[simp]:
-apply(simp add: fetch.simps t_wcode_adjust_def nth_of.simps)
+"fetch t_wcode_adjust (Suc 0) Bk = (W1, 1)"
-done
+"fetch t_wcode_adjust (Suc 0) Oc = (R, 2)"
+"fetch t_wcode_adjust (Suc (Suc 0)) Oc = (R, 3)"
-lemma [simp]: "fetch t_wcode_adjust (Suc 0) Oc = (R, 2)"
+"fetch t_wcode_adjust (Suc (Suc (Suc 0))) Oc = (R, 4)"
-apply(simp add: fetch.simps t_wcode_adjust_def nth_of.simps)
+"fetch t_wcode_adjust  (Suc (Suc (Suc 0))) Bk = (R, 3)"
-done
+"fetch t_wcode_adjust 4 Bk = (L, 8)"
+"fetch t_wcode_adjust 4 Oc = (L, 5)"
-lemma [simp]: "fetch t_wcode_adjust (Suc (Suc 0)) Oc = (R, 3)"
+"fetch t_wcode_adjust 5 Oc = (W0, 5)"
-apply(simp add: fetch.simps t_wcode_adjust_def nth_of.simps)
+"fetch t_wcode_adjust 5 Bk = (L, 6)"
-done
+"fetch t_wcode_adjust 6 Oc = (R, 7)"
+"fetch t_wcode_adjust 6 Bk = (L, 6)"
-lemma [simp]: "fetch t_wcode_adjust (Suc (Suc (Suc 0))) Oc = (R, 4)"
+"fetch t_wcode_adjust 7 Bk = (W1, 2)"
-apply(simp add: fetch.simps t_wcode_adjust_def nth_of.simps)
+"fetch t_wcode_adjust 8 Bk = (L, 9)"
-done
+"fetch t_wcode_adjust 8 Oc = (W0, 8)"
+"fetch t_wcode_adjust 9 Oc = (L, 10)"
-lemma [simp]: "fetch t_wcode_adjust  (Suc (Suc (Suc 0))) Bk = (R, 3)"
+"fetch t_wcode_adjust 9 Bk = (L, 9)"
-apply(simp add: fetch.simps t_wcode_adjust_def nth_of.simps)
+"fetch t_wcode_adjust 10 Bk = (L, 11)"
-done
+"fetch t_wcode_adjust 10 Oc = (L, 10)"
+"fetch t_wcode_adjust 11 Oc = (L, 11)"
-lemma [simp]: "fetch t_wcode_adjust 4 Bk = (L, 8)"
+"fetch t_wcode_adjust 11 Bk = (R, 0)"
-apply(simp add: fetch.simps t_wcode_adjust_def nth_of.simps numeral_4_eq_4)
+by(auto simp: fetch.simps t_wcode_adjust_def nth_of.simps numeral)
-done
-lemma [simp]: "fetch t_wcode_adjust 4 Oc = (L, 5)"
-apply(simp add: fetch.simps t_wcode_adjust_def nth_of.simps numeral_4_eq_4)
-done
-lemma [simp]: "fetch t_wcode_adjust 5 Oc = (W0, 5)"
-apply(simp only: fetch.simps t_wcode_adjust_def nth_of.simps numeral_5_eq_5, simp)
-done
-lemma [simp]: "fetch t_wcode_adjust 5 Bk = (L, 6)"
-apply(simp only: fetch.simps t_wcode_adjust_def nth_of.simps numeral_5_eq_5, auto)
-done
-lemma [simp]: "fetch t_wcode_adjust 6 Oc = (R, 7)"
-apply(simp add: fetch.simps t_wcode_adjust_def nth_of.simps numeral_6_eq_6)
-done
-lemma [simp]: "fetch t_wcode_adjust 6 Bk = (L, 6)"
-apply(simp add: fetch.simps t_wcode_adjust_def nth_of.simps numeral_6_eq_6)
-done
-lemma [simp]: "fetch t_wcode_adjust 7 Bk = (W1, 2)"
-apply(simp add: fetch.simps t_wcode_adjust_def nth_of.simps numeral_7_eq_7)
-done
-lemma [simp]: "fetch t_wcode_adjust 8 Bk = (L, 9)"
-apply(simp add: fetch.simps t_wcode_adjust_def nth_of.simps numeral_8_eq_8)
-done
-lemma [simp]: "fetch t_wcode_adjust 8 Oc = (W0, 8)"
-apply(simp add: fetch.simps t_wcode_adjust_def nth_of.simps numeral_8_eq_8)
-done
-lemma [simp]: "fetch t_wcode_adjust 9 Oc = (L, 10)"
-apply(simp add: fetch.simps t_wcode_adjust_def nth_of.simps numeral_9_eq_9)
-done
-lemma [simp]: "fetch t_wcode_adjust 9 Bk = (L, 9)"
-apply(simp add: fetch.simps t_wcode_adjust_def nth_of.simps numeral_9_eq_9)
-done
-lemma [simp]: "fetch t_wcode_adjust 10 Bk = (L, 11)"
-apply(simp add: fetch.simps t_wcode_adjust_def nth_of.simps  numeral_10_eq_10)
-done
-lemma [simp]: "fetch t_wcode_adjust 10 Oc = (L, 10)"
-apply(simp add: fetch.simps t_wcode_adjust_def nth_of.simps eval_nat_numeral)
-done
-lemma [simp]: "fetch t_wcode_adjust 11 Oc = (L, 11)"
-apply(simp add: fetch.simps t_wcode_adjust_def nth_of.simps eval_nat_numeral)
-done
-lemma [simp]: "fetch t_wcode_adjust 11 Bk = (R, 0)"
-apply(simp add: fetch.simps t_wcode_adjust_def nth_of.simps eval_nat_numeral)
-done
 fun wadjust_start :: "nat \<Rightarrow> nat \<Rightarrow> tape \<Rightarrow> bool"
 where
 "wadjust_start m rs (l, r) =
 (\<exists> ln rn. l = Bk # Oc\<up>(Suc m) \<and>
 wadjust_step rs (st, l, r))"
 definition wadjust_le :: "((nat \<times> config) \<times> nat \<times> config) set"
 where "wadjust_le \<equiv> (inv_image lex_square wadjust_measure)"
-lemma [intro]: "wf lex_square"
+lemma wf_lex_square[intro]: "wf lex_square"
 by(auto intro:wf_lex_prod simp: Abacus.lex_pair_def lex_square_def
 Abacus.lex_triple_def)
 lemma wf_wadjust_le[intro]: "wf wadjust_le"
 by(auto intro:wf_inv_image simp: wadjust_le_def
 Abacus.lex_triple_def Abacus.lex_pair_def)
-lemma [simp]: "wadjust_start m rs (c, []) = False"
+lemma wadjust_start_snd_nonempty[simp]: "wadjust_start m rs (c, []) = False"
 apply(auto simp: wadjust_start.simps)
 done
-lemma [simp]: "wadjust_loop_right_move m rs (c, []) \<Longrightarrow> c \<noteq> []"
+lemma wadjust_loop_right_move_fst_nonempty[simp]: "wadjust_loop_right_move m rs (c, []) \<Longrightarrow> c \<noteq> []"
 apply(auto simp: wadjust_loop_right_move.simps)
 done
-lemma [simp]: "wadjust_loop_right_move m rs (c, [])
+lemma wadjust_loop_check_fst_nonempty[simp]: "wadjust_loop_check m rs (c, []) \<Longrightarrow> c \<noteq> []"
-\<Longrightarrow>  wadjust_loop_check m rs (Bk # c, [])"
-apply(simp only: wadjust_loop_right_move.simps wadjust_loop_check.simps)
-apply(auto)
-done
-lemma [simp]: "wadjust_loop_check m rs (c, []) \<Longrightarrow> c \<noteq> []"
 apply(simp only: wadjust_loop_check.simps, auto)
 done
-lemma [simp]: "wadjust_loop_start m rs (c, []) = False"
+lemma wadjust_loop_start_snd_nonempty[simp]: "wadjust_loop_start m rs (c, []) = False"
 apply(simp add: wadjust_loop_start.simps)
 done
-lemma [simp]: "wadjust_loop_right_move m rs (c, []) \<Longrightarrow>
+lemma wadjust_erase2_singleton[simp]: "wadjust_loop_check m rs (c, []) \<Longrightarrow> wadjust_erase2 m rs (tl c, [hd c])"
-wadjust_loop_right_move m rs (Bk # c, [])"
-apply(simp only: wadjust_loop_right_move.simps)
-apply(erule_tac exE)+
-apply(auto)
-done
-lemma [simp]: "wadjust_loop_check m rs (c, []) \<Longrightarrow> wadjust_erase2 m rs (tl c, [hd c])"
 apply(simp only: wadjust_loop_check.simps wadjust_erase2.simps, auto)
 done
-lemma [simp]: " wadjust_loop_erase m rs (c, [])
+lemma wadjust_loop_on_left_moving_snd_nonempty[simp]:
-\<Longrightarrow> (c = [] \<longrightarrow> wadjust_loop_on_left_moving m rs ([], [Bk])) \<and>
+"wadjust_loop_on_left_moving m rs (c, []) = False"
-(c \<noteq> [] \<longrightarrow> wadjust_loop_on_left_moving m rs (tl c, [hd c]))"
+"wadjust_loop_right_move2 m rs (c, []) = False"
-apply(simp add: wadjust_loop_erase.simps)
+"wadjust_erase2 m rs ([], []) = False"
-done
+by(auto simp: wadjust_loop_on_left_moving.simps
+wadjust_loop_right_move2.simps
-lemma [simp]: "wadjust_loop_on_left_moving m rs (c, []) = False"
+wadjust_erase2.simps)
-apply(auto simp: wadjust_loop_on_left_moving.simps)
-done
+lemma wadjust_on_left_moving_B_Bk1[simp]: "wadjust_on_left_moving_B m rs
-lemma [simp]: "wadjust_loop_right_move2 m rs (c, []) = False"
-apply(auto simp: wadjust_loop_right_move2.simps)
-done
-lemma [simp]: "wadjust_erase2 m rs ([], []) = False"
-apply(auto simp: wadjust_erase2.simps)
-done
-lemma [simp]: "wadjust_on_left_moving_B m rs
 (Oc # Oc # Oc\<up>(rs) @ Bk # Oc # Oc\<up>(m), [Bk])"
 apply(simp add: wadjust_on_left_moving_B.simps, auto)
 done
-lemma [simp]: "wadjust_on_left_moving_B m rs
+lemma wadjust_on_left_moving_B_Bk2[simp]: "wadjust_on_left_moving_B m rs
 (Bk\<up>(n) @ Bk # Oc # Oc # Oc\<up>(rs) @ Bk # Oc # Oc\<up>(m), [Bk])"
 apply(simp add: wadjust_on_left_moving_B.simps , auto)
 apply(rule_tac x = "Suc n" in exI, simp add: exp_ind del: replicate_Suc)
 done
-lemma [simp]: "\<lbrakk>wadjust_erase2 m rs (c, []); c \<noteq> []\<rbrakk> \<Longrightarrow>
+lemma wadjust_on_left_moving_singleton[simp]: "\<lbrakk>wadjust_erase2 m rs (c, []); c \<noteq> []\<rbrakk> \<Longrightarrow>
 wadjust_on_left_moving m rs (tl c, [hd c])"
 apply(simp only: wadjust_erase2.simps)
 apply(erule_tac exE)+
 apply(case_tac ln, simp_all add:  wadjust_on_left_moving.simps)
 done
-lemma [simp]: "wadjust_erase2 m rs (c, [])
+lemma wadjust_erase2_cases[simp]: "wadjust_erase2 m rs (c, [])
 \<Longrightarrow> (c = [] \<longrightarrow> wadjust_on_left_moving m rs ([], [Bk])) \<and>
 (c \<noteq> [] \<longrightarrow> wadjust_on_left_moving m rs (tl c, [hd c]))"
 apply(auto)
 done
-lemma [simp]: "wadjust_on_left_moving m rs ([], []) = False"
+lemma wadjust_on_left_moving_nonempty[simp]:
-apply(simp add: wadjust_on_left_moving.simps
+"wadjust_on_left_moving m rs ([], []) = False"
+"wadjust_on_left_moving_O m rs (c, []) = False"
+apply(auto simp: wadjust_on_left_moving.simps
 wadjust_on_left_moving_O.simps wadjust_on_left_moving_B.simps)
 done
-lemma [simp]: "wadjust_on_left_moving_O m rs (c, []) = False"
+lemma wadjust_on_left_moving_B_singleton_Bk[simp]:
-apply(simp add: wadjust_on_left_moving_O.simps)
+" \<lbrakk>wadjust_on_left_moving_B m rs (c, []); c \<noteq> []; hd c = Bk\<rbrakk> \<Longrightarrow>
-done
-lemma [simp]: " \<lbrakk>wadjust_on_left_moving_B m rs (c, []); c \<noteq> []; hd c = Bk\<rbrakk> \<Longrightarrow>
 wadjust_on_left_moving_B m rs (tl c, [Bk])"
 apply(simp add: wadjust_on_left_moving_B.simps, auto)
 apply(case_tac [!] ln, simp_all)
 done
-lemma [simp]: "\<lbrakk>wadjust_on_left_moving_B m rs (c, []); c \<noteq> []; hd c = Oc\<rbrakk> \<Longrightarrow>
+lemma wadjust_on_left_moving_B_singleton_Oc[simp]:
+"\<lbrakk>wadjust_on_left_moving_B m rs (c, []); c \<noteq> []; hd c = Oc\<rbrakk> \<Longrightarrow>
 wadjust_on_left_moving_O m rs (tl c, [Oc])"
 apply(simp add: wadjust_on_left_moving_B.simps wadjust_on_left_moving_O.simps, auto)
 apply(case_tac [!] ln, simp_all add: )
 done
-lemma [simp]: "\<lbrakk>wadjust_on_left_moving m rs (c, []); c \<noteq> []\<rbrakk> \<Longrightarrow>
+lemma wadjust_on_left_moving_singleton2[simp]:
+"\<lbrakk>wadjust_on_left_moving m rs (c, []); c \<noteq> []\<rbrakk> \<Longrightarrow>
 wadjust_on_left_moving m rs (tl c, [hd c])"
 apply(simp add: wadjust_on_left_moving.simps)
 apply(case_tac "hd c", simp_all)
 done
-lemma [simp]: "wadjust_on_left_moving m rs (c, [])
+lemma wadjust_nonempty[simp]: "wadjust_goon_left_moving m rs (c, []) = False"
-\<Longrightarrow> (c = [] \<longrightarrow> wadjust_on_left_moving m rs ([], [Bk])) \<and>
+"wadjust_backto_standard_pos m rs (c, []) = False"
-(c \<noteq> [] \<longrightarrow> wadjust_on_left_moving m rs (tl c, [hd c]))"
+by(auto simp: wadjust_goon_left_moving.simps wadjust_goon_left_moving_B.simps
-apply(auto)
+wadjust_goon_left_moving_O.simps wadjust_backto_standard_pos.simps
-done
-lemma [simp]: "wadjust_goon_left_moving m rs (c, []) = False"
-apply(auto simp: wadjust_goon_left_moving.simps wadjust_goon_left_moving_B.simps
-wadjust_goon_left_moving_O.simps)
-done
-lemma [simp]: "wadjust_backto_standard_pos m rs (c, []) = False"
-apply(auto simp: wadjust_backto_standard_pos.simps
 wadjust_backto_standard_pos_B.simps wadjust_backto_standard_pos_O.simps)
-done
+lemma wadjust_loop_start_no_Bk[simp]: "wadjust_loop_start m rs (c, Bk # list) = False"
-lemma [simp]:
-"wadjust_start m rs (c, Bk # list) \<Longrightarrow>
-(c = [] \<longrightarrow> wadjust_start m rs ([], Oc # list)) \<and>
-(c \<noteq> [] \<longrightarrow> wadjust_start m rs (c, Oc # list))"
-apply(auto simp: wadjust_start.simps)
-done
-lemma [simp]: "wadjust_loop_start m rs (c, Bk # list) = False"
 apply(auto simp: wadjust_loop_start.simps)
 done
-lemma [simp]: "wadjust_loop_right_move m rs (c, b) \<Longrightarrow> c \<noteq> []"
+lemma wadjust_loop_right_move_Bk[simp]: "wadjust_loop_right_move m rs (c, Bk # list)
-apply(simp only: wadjust_loop_right_move.simps, auto)
-done
-lemma [simp]: "wadjust_loop_right_move m rs (c, Bk # list)
 \<Longrightarrow> wadjust_loop_right_move m rs (Bk # c, list)"
 apply(simp only: wadjust_loop_right_move.simps)
 apply(erule_tac exE)+
 apply(rule_tac x = ml in exI, simp)
 apply(rule_tac x = mr in exI, simp)
 apply(rule_tac x = "Suc nl" in exI, simp add: )
 apply(case_tac nr, simp, case_tac mr, simp_all add: )
 apply(rule_tac x = nat in exI, auto)
 done
-lemma [simp]: "wadjust_loop_check m rs (c, b) \<Longrightarrow> c \<noteq> []"
+lemma wadjust_loop_check_nonempty[simp]: "wadjust_loop_check m rs (c, b) \<Longrightarrow> c \<noteq> []"
 apply(simp only: wadjust_loop_check.simps, auto)
 done
-lemma [simp]: "wadjust_loop_check m rs (c, Bk # list)
+lemma wadjust_erase2_via_loop_check_Bk[simp]: "wadjust_loop_check m rs (c, Bk # list)
 \<Longrightarrow>  wadjust_erase2 m rs (tl c, hd c # Bk # list)"
 apply(auto simp: wadjust_loop_check.simps wadjust_erase2.simps)
 apply(case_tac [!] mr, simp_all)
 done
-lemma [simp]: "wadjust_loop_erase m rs (c, b) \<Longrightarrow> c \<noteq> []"
-apply(simp only: wadjust_loop_erase.simps, auto)
-done
 declare wadjust_loop_on_left_moving_O.simps[simp del]
 wadjust_loop_on_left_moving_B.simps[simp del]
-lemma [simp]: "\<lbrakk>wadjust_loop_erase m rs (c, Bk # list); hd c = Bk\<rbrakk>
+lemma wadjust_loop_on_left_moving_B_via_erase[simp]: "\<lbrakk>wadjust_loop_erase m rs (c, Bk # list); hd c = Bk\<rbrakk>
 \<Longrightarrow> wadjust_loop_on_left_moving_B m rs (tl c, Bk # Bk # list)"
 apply(simp only: wadjust_loop_erase.simps
 wadjust_loop_on_left_moving_B.simps)
 apply(erule_tac exE)+
 apply(rule_tac x = ml in exI, rule_tac x = mr in exI,
 rule_tac x = ln in exI, rule_tac x = 0 in exI, simp)
 apply(case_tac ln, simp_all add: , auto)
 apply(simp add: exp_ind [THEN sym])
 done
-lemma [simp]: "\<lbrakk>wadjust_loop_erase m rs (c, Bk # list); c \<noteq> []; hd c = Oc\<rbrakk> \<Longrightarrow>
+lemma wadjust_loop_on_left_moving_O_Bk_via_erase[simp]:
+"\<lbrakk>wadjust_loop_erase m rs (c, Bk # list); c \<noteq> []; hd c = Oc\<rbrakk> \<Longrightarrow>
 wadjust_loop_on_left_moving_O m rs (tl c, Oc # Bk # list)"
 apply(simp only: wadjust_loop_erase.simps wadjust_loop_on_left_moving_O.simps,
 auto)
 apply(case_tac [!] ln, simp_all add: )
 done
-lemma [simp]: "\<lbrakk>wadjust_loop_erase m rs (c, Bk # list); c \<noteq> []\<rbrakk> \<Longrightarrow>
+lemma wadjust_loop_on_left_moving_Bk_via_erase[simp]: "\<lbrakk>wadjust_loop_erase m rs (c, Bk # list); c \<noteq> []\<rbrakk> \<Longrightarrow>
 wadjust_loop_on_left_moving m rs (tl c, hd c # Bk # list)"
 apply(case_tac "hd c", simp_all add:wadjust_loop_on_left_moving.simps)
 done
-lemma [simp]: "wadjust_loop_on_left_moving m rs (c, b) \<Longrightarrow> c \<noteq> []"
-apply(simp add: wadjust_loop_on_left_moving.simps
+lemma wadjust_loop_on_left_moving_B_Bk_move[simp]:
-wadjust_loop_on_left_moving_O.simps wadjust_loop_on_left_moving_B.simps, auto)
+"\<lbrakk>wadjust_loop_on_left_moving_B m rs (c, Bk # list); hd c = Bk\<rbrakk>
-done
-lemma [simp]: "wadjust_loop_on_left_moving_O m rs (c, Bk # list) = False"
-apply(simp add: wadjust_loop_on_left_moving_O.simps)
-done
-lemma [simp]: "\<lbrakk>wadjust_loop_on_left_moving_B m rs (c, Bk # list); hd c = Bk\<rbrakk>
 \<Longrightarrow>  wadjust_loop_on_left_moving_B m rs (tl c, Bk # Bk # list)"
 apply(simp only: wadjust_loop_on_left_moving_B.simps)
 apply(erule_tac exE)+
 apply(rule_tac x = ml in exI, rule_tac x = mr in exI)
 apply(case_tac nl, simp_all add: , auto)
 apply(rule_tac x = "Suc nr" in exI, auto simp: )
 done
-lemma [simp]: "\<lbrakk>wadjust_loop_on_left_moving_B m rs (c, Bk # list); hd c = Oc\<rbrakk>
+lemma wadjust_loop_on_left_moving_O_Oc_move[simp]:
+"\<lbrakk>wadjust_loop_on_left_moving_B m rs (c, Bk # list); hd c = Oc\<rbrakk>
 \<Longrightarrow> wadjust_loop_on_left_moving_O m rs (tl c, Oc # Bk # list)"
 apply(simp only: wadjust_loop_on_left_moving_O.simps
 wadjust_loop_on_left_moving_B.simps)
 apply(erule_tac exE)+
 apply(rule_tac x = ml in exI, rule_tac x = mr in exI)
 apply(case_tac nl, simp_all add: , auto)
 done
-lemma [simp]: "wadjust_loop_on_left_moving m rs (c, Bk # list)
+lemma wadjust_loop_on_left_moving_O_noBk[simp]:
+"wadjust_loop_on_left_moving_O m rs (c, Bk # list) = False"
+apply(simp add: wadjust_loop_on_left_moving_O.simps)
+done
+lemma wadjust_loop_on_left_moving_Bk_move[simp]:
+"wadjust_loop_on_left_moving m rs (c, Bk # list)
 \<Longrightarrow> wadjust_loop_on_left_moving m rs (tl c, hd c # Bk # list)"
 apply(simp add: wadjust_loop_on_left_moving.simps)
 apply(case_tac "hd c", simp_all)
 done
-lemma [simp]: "wadjust_loop_right_move2 m rs (c, b) \<Longrightarrow> c \<noteq> []"
+lemma wadjust_loop_erase_nonempty[simp]: "wadjust_loop_erase m rs (c, b) \<Longrightarrow> c \<noteq> []"
-apply(simp only: wadjust_loop_right_move2.simps, auto)
+"wadjust_loop_on_left_moving m rs (c, b) \<Longrightarrow> c \<noteq> []"
-done
+"wadjust_loop_right_move2 m rs (c, b) \<Longrightarrow> c \<noteq> []"
+"wadjust_erase2 m rs (c, Bk # list) \<Longrightarrow> c \<noteq> []"
-lemma [simp]: "wadjust_loop_right_move2 m rs (c, Bk # list) \<Longrightarrow>  wadjust_loop_start m rs (c, Oc # list)"
+"wadjust_on_left_moving m rs (c,b) \<Longrightarrow> c \<noteq> []"
+"wadjust_on_left_moving_O m rs (c, Bk # list) = False"
+"wadjust_goon_left_moving m rs (c, b) \<Longrightarrow> c \<noteq> []"
+by(auto simp: wadjust_loop_erase.simps wadjust_loop_on_left_moving.simps
+wadjust_loop_on_left_moving_O.simps wadjust_loop_on_left_moving_B.simps
+wadjust_loop_right_move2.simps wadjust_erase2.simps
+wadjust_on_left_moving.simps
+wadjust_on_left_moving_O.simps
+wadjust_on_left_moving_B.simps wadjust_goon_left_moving.simps
+wadjust_goon_left_moving_B.simps
+wadjust_goon_left_moving_O.simps)
+lemma wadjust_loop_start_Oc_via_Bk_move[simp]:
+"wadjust_loop_right_move2 m rs (c, Bk # list) \<Longrightarrow>  wadjust_loop_start m rs (c, Oc # list)"
 apply(auto simp: wadjust_loop_right_move2.simps wadjust_loop_start.simps)
 apply(case_tac ln, simp_all add: )
 apply(rule_tac x = 0 in exI, simp)
 apply(rule_tac x = rn in exI, simp)
 apply(rule_tac x = "Suc ml" in exI, simp add: , auto)
 apply(rule_tac x = "Suc nat" in exI, simp add: exp_ind del: replicate_Suc)
 apply(rule_tac x = rn in exI, auto)
 apply(rule_tac x = "Suc ml" in exI, auto )
 done
-lemma [simp]: "wadjust_erase2 m rs (c, Bk # list) \<Longrightarrow> c \<noteq> []"
+lemma wadjust_on_left_moving_Bk_via_erase[simp]: "wadjust_erase2 m rs (c, Bk # list) \<Longrightarrow>
-apply(auto simp:wadjust_erase2.simps )
-done
-lemma [simp]: "wadjust_erase2 m rs (c, Bk # list) \<Longrightarrow>
 wadjust_on_left_moving m rs (tl c, hd c # Bk # list)"
 apply(auto simp: wadjust_erase2.simps)
 apply(case_tac ln, simp_all add:  wadjust_on_left_moving.simps
 wadjust_on_left_moving_O.simps wadjust_on_left_moving_B.simps)
 apply(auto)
 apply(rule_tac x = "(Suc (Suc rn))" in exI, simp add: )
 apply(rule_tac x = "Suc nat" in exI, simp add: exp_ind del: replicate_Suc)
 apply(rule_tac x = "(Suc (Suc rn))" in exI, simp add: )
 done
-lemma [simp]: "wadjust_on_left_moving m rs (c,b) \<Longrightarrow> c \<noteq> []"
-apply(simp only:wadjust_on_left_moving.simps
+lemma wadjust_on_left_moving_B_Bk_drop_one: "\<lbrakk>wadjust_on_left_moving_B m rs (c, Bk # list); hd c = Bk\<rbrakk>
-wadjust_on_left_moving_O.simps
-wadjust_on_left_moving_B.simps
-, auto)
-done
-lemma [simp]: "wadjust_on_left_moving_O m rs (c, Bk # list) = False"
-apply(simp add: wadjust_on_left_moving_O.simps)
-done
-lemma [simp]: "\<lbrakk>wadjust_on_left_moving_B m rs (c, Bk # list); hd c = Bk\<rbrakk>
 \<Longrightarrow> wadjust_on_left_moving_B m rs (tl c, Bk # Bk # list)"
 apply(auto simp: wadjust_on_left_moving_B.simps)
 apply(case_tac ln, simp_all)
 done
-lemma [simp]: "\<lbrakk>wadjust_on_left_moving_B m rs (c, Bk # list); hd c = Oc\<rbrakk>
+lemma wadjust_on_left_moving_B_Bk_drop_Oc: "\<lbrakk>wadjust_on_left_moving_B m rs (c, Bk # list); hd c = Oc\<rbrakk>
 \<Longrightarrow> wadjust_on_left_moving_O m rs (tl c, Oc # Bk # list)"
 apply(auto simp: wadjust_on_left_moving_O.simps
 wadjust_on_left_moving_B.simps)
 apply(case_tac ln, simp_all add: )
 done
-lemma [simp]: "wadjust_on_left_moving  m rs (c, Bk # list) \<Longrightarrow>
+lemma wadjust_on_left_moving_B_drop[simp]: "wadjust_on_left_moving  m rs (c, Bk # list) \<Longrightarrow>
 wadjust_on_left_moving m rs (tl c, hd c # Bk # list)"
-apply(simp add: wadjust_on_left_moving.simps)
+by(cases "hd c", auto simp:wadjust_on_left_moving.simps wadjust_on_left_moving_B_Bk_drop_one
-apply(case_tac "hd c", simp_all)
+wadjust_on_left_moving_B_Bk_drop_Oc)
-done
+lemma wadjust_goon_left_moving_O_no_Bk[simp]: "wadjust_goon_left_moving_O m rs (c, Bk # list) = False"
-lemma [simp]: "wadjust_goon_left_moving m rs (c, b) \<Longrightarrow> c \<noteq> []"
-apply(simp add: wadjust_goon_left_moving.simps
-wadjust_goon_left_moving_B.simps
-wadjust_goon_left_moving_O.simps , auto)
-done
-lemma [simp]: "wadjust_goon_left_moving_O m rs (c, Bk # list) = False"
 apply(simp add: wadjust_goon_left_moving_O.simps, auto)
 apply(case_tac mr, simp_all add: )
 done
-lemma [simp]: "\<lbrakk>wadjust_goon_left_moving_B m rs (c, Bk # list); hd c = Bk\<rbrakk>
+lemma wadjust_backto_standard_pos_via_left_Bk[simp]:
-\<Longrightarrow> wadjust_backto_standard_pos_B m rs (tl c, Bk # Bk # list)"
+"wadjust_goon_left_moving m rs (c, Bk # list) \<Longrightarrow>
-apply(auto simp: wadjust_goon_left_moving_B.simps
-wadjust_backto_standard_pos_B.simps )
-done
-lemma [simp]: "\<lbrakk>wadjust_goon_left_moving_B m rs (c, Bk # list); hd c = Oc\<rbrakk>
-\<Longrightarrow> wadjust_backto_standard_pos_O m rs (tl c, Oc # Bk # list)"
-apply(auto simp: wadjust_goon_left_moving_B.simps
-wadjust_backto_standard_pos_O.simps)
-done
-lemma [simp]: "wadjust_goon_left_moving m rs (c, Bk # list) \<Longrightarrow>
 wadjust_backto_standard_pos m rs (tl c, hd c # Bk # list)"
-apply(case_tac "hd c", simp_all add: wadjust_backto_standard_pos.simps
+by(case_tac "hd c", simp_all add: wadjust_backto_standard_pos.simps wadjust_goon_left_moving.simps
-wadjust_goon_left_moving.simps)
+wadjust_goon_left_moving_B.simps wadjust_backto_standard_pos_O.simps)
-done
+lemma wadjust_loop_right_move_Oc[simp]: "wadjust_loop_start m rs (c, Oc # list)
-lemma [simp]: "wadjust_backto_standard_pos m rs (c, Bk # list) \<Longrightarrow>
-(c = [] \<longrightarrow> wadjust_stop m rs ([Bk], list)) \<and> (c \<noteq> [] \<longrightarrow> wadjust_stop m rs (Bk # c, list))"
-apply(auto simp: wadjust_backto_standard_pos.simps
-wadjust_backto_standard_pos_B.simps
-wadjust_backto_standard_pos_O.simps wadjust_stop.simps)
-apply(case_tac [!] mr, simp_all add: )
-done
-lemma [simp]: "wadjust_start m rs (c, Oc # list)
-\<Longrightarrow> (c = [] \<longrightarrow> wadjust_loop_start m rs ([Oc], list)) \<and>
-(c \<noteq> [] \<longrightarrow> wadjust_loop_start m rs (Oc # c, list))"
-apply(auto simp:wadjust_loop_start.simps wadjust_start.simps )
-apply(rule_tac x = ln in exI, rule_tac x = rn in exI,
-rule_tac x = "Suc 0" in exI, simp)
-done
-lemma [simp]: "wadjust_loop_start m rs (c, b) \<Longrightarrow> c \<noteq> []"
-apply(simp add: wadjust_loop_start.simps, auto)
-done
-lemma [simp]: "wadjust_loop_start m rs (c, Oc # list)
 \<Longrightarrow> wadjust_loop_right_move m rs (Oc # c, list)"
 apply(simp add: wadjust_loop_start.simps wadjust_loop_right_move.simps, auto)
 apply(rule_tac x = ml in exI, rule_tac x = mr in exI,
 rule_tac x = 0 in exI, simp)
 apply(rule_tac x = "Suc ln" in exI, simp add: exp_ind del: replicate_Suc)
 done
-lemma [simp]: "wadjust_loop_right_move m rs (c, Oc # list) \<Longrightarrow>
+lemma wadjust_loop_check_Oc[simp]: "wadjust_loop_right_move m rs (c, Oc # list) \<Longrightarrow>
 wadjust_loop_check m rs (Oc # c, list)"
 apply(simp add: wadjust_loop_right_move.simps
 wadjust_loop_check.simps, auto)
 apply(rule_tac [!] x = ml in exI, simp_all add: exp_ind del: replicate_Suc, auto)
 apply(case_tac nl, simp_all add: exp_ind del: replicate_Suc)
 apply(rule_tac x = "mr - 1" in exI, case_tac mr, simp_all add: )
 apply(case_tac [!] nr, simp_all)
 done
-lemma [simp]: "wadjust_loop_check m rs (c, Oc # list) \<Longrightarrow>
+lemma wadjust_loop_erase_move_Oc[simp]: "wadjust_loop_check m rs (c, Oc # list) \<Longrightarrow>
 wadjust_loop_erase m rs (tl c, hd c # Oc # list)"
 apply(simp only: wadjust_loop_check.simps wadjust_loop_erase.simps)
 apply(erule_tac exE)+
 apply(rule_tac x = ml in exI, rule_tac x = mr in exI, auto)
 apply(case_tac mr, simp_all add: )
 done
-lemma [simp]: "wadjust_loop_erase m rs (c, Oc # list) \<Longrightarrow>
+lemma wadjust_loop_erase_Bk_via_Oc[simp]: "wadjust_loop_erase m rs (c, Oc # list) \<Longrightarrow>
 wadjust_loop_erase m rs (c, Bk # list)"
 apply(auto simp: wadjust_loop_erase.simps)
 done
-lemma [simp]: "wadjust_loop_on_left_moving_B m rs (c, Oc # list) = False"
+lemma wadjust_loop_on_left_moving_B_no_Oc[simp]: "wadjust_loop_on_left_moving_B m rs (c, Oc # list) = False"
 apply(auto simp: wadjust_loop_on_left_moving_B.simps)
 apply(case_tac nr, simp_all add: )
 done
-lemma [simp]: "wadjust_loop_on_left_moving m rs (c, Oc # list)
+lemma wadjust_loop_right_move2_via_left_moving[simp]:
+"wadjust_loop_on_left_moving m rs (c, Oc # list)
 \<Longrightarrow> wadjust_loop_right_move2 m rs (Oc # c, list)"
 apply(simp add:wadjust_loop_on_left_moving.simps)
 apply(auto simp: wadjust_loop_on_left_moving_O.simps
 wadjust_loop_right_move2.simps)
 done
-lemma [simp]: "wadjust_loop_right_move2 m rs (c, Oc # list) = False"
+lemma wadjust_loop_right_move2_no_Oc[simp]: "wadjust_loop_right_move2 m rs (c, Oc # list) = False"
 apply(auto simp: wadjust_loop_right_move2.simps )
 apply(case_tac ln, simp_all add: )
 done
-lemma [simp]: "wadjust_erase2 m rs (c, Oc # list)
+lemma wadjust_on_left_moving_B_no_Oc[simp]:
-\<Longrightarrow> (c = [] \<longrightarrow> wadjust_erase2 m rs ([], Bk # list))
+"wadjust_on_left_moving_B m rs (c, Oc # list) = False"
-\<and> (c \<noteq> [] \<longrightarrow> wadjust_erase2 m rs (c, Bk # list))"
-apply(auto simp: wadjust_erase2.simps )
-done
-lemma [simp]: "wadjust_on_left_moving_B m rs (c, Oc # list) = False"
 apply(auto simp: wadjust_on_left_moving_B.simps)
 done
-lemma [simp]: "\<lbrakk>wadjust_on_left_moving_O m rs (c, Oc # list); hd c = Bk\<rbrakk> \<Longrightarrow>
+lemma wadjust_goon_left_moving_B_Bk_Oc: "\<lbrakk>wadjust_on_left_moving_O m rs (c, Oc # list); hd c = Bk\<rbrakk> \<Longrightarrow>
 wadjust_goon_left_moving_B m rs (tl c, Bk # Oc # list)"
 apply(auto simp: wadjust_on_left_moving_O.simps
 wadjust_goon_left_moving_B.simps )
 done
-lemma [simp]: "\<lbrakk>wadjust_on_left_moving_O m rs (c, Oc # list); hd c = Oc\<rbrakk>
+lemma wadjust_goon_left_moving_O_Oc_Oc: "\<lbrakk>wadjust_on_left_moving_O m rs (c, Oc # list); hd c = Oc\<rbrakk>
 \<Longrightarrow> wadjust_goon_left_moving_O m rs (tl c, Oc # Oc # list)"
 apply(auto simp: wadjust_on_left_moving_O.simps
 wadjust_goon_left_moving_O.simps )
 apply(auto simp:  numeral_2_eq_2)
 done
-lemma [simp]: "wadjust_on_left_moving m rs (c, Oc # list) \<Longrightarrow>
+lemma wadjust_goon_left_moving_Oc[simp]: "wadjust_on_left_moving m rs (c, Oc # list) \<Longrightarrow>
 wadjust_goon_left_moving m rs (tl c, hd c # Oc # list)"
-apply(simp add: wadjust_on_left_moving.simps
+by(cases "hd c"; force simp: wadjust_on_left_moving.simps wadjust_goon_left_moving.simps
-wadjust_goon_left_moving.simps)
+wadjust_goon_left_moving_B_Bk_Oc wadjust_goon_left_moving_O_Oc_Oc)+
-apply(case_tac "hd c", simp_all)
-done
+lemma left_moving_Bk_Oc[simp]: "\<lbrakk>wadjust_goon_left_moving_O m rs (c, Oc # list); hd c = Bk\<rbrakk>
-lemma [simp]: "wadjust_on_left_moving m rs (c, Oc # list) \<Longrightarrow>
-wadjust_goon_left_moving m rs (tl c, hd c # Oc # list)"
-apply(simp add: wadjust_on_left_moving.simps
-wadjust_goon_left_moving.simps)
-apply(case_tac "hd c", simp_all)
-done
-lemma [simp]: "wadjust_goon_left_moving_B m rs (c, Oc # list) = False"
-apply(auto simp: wadjust_goon_left_moving_B.simps)
-done
-lemma [simp]: "\<lbrakk>wadjust_goon_left_moving_O m rs (c, Oc # list); hd c = Bk\<rbrakk>
 \<Longrightarrow> wadjust_goon_left_moving_B m rs (tl c, Bk # Oc # list)"
 apply(auto simp: wadjust_goon_left_moving_O.simps wadjust_goon_left_moving_B.simps)
 apply(case_tac [!] ml, auto simp: )
 done
-lemma  [simp]: "\<lbrakk>wadjust_goon_left_moving_O m rs (c, Oc # list); hd c = Oc\<rbrakk> \<Longrightarrow>
+lemma  left_moving_Oc_Oc[simp]: "\<lbrakk>wadjust_goon_left_moving_O m rs (c, Oc # list); hd c = Oc\<rbrakk> \<Longrightarrow>
 wadjust_goon_left_moving_O m rs (tl c, Oc # Oc # list)"
 apply(auto simp: wadjust_goon_left_moving_O.simps wadjust_goon_left_moving_B.simps)
 apply(rule_tac x = "ml - 1" in exI, simp)
 apply(case_tac ml, simp_all add: )
 apply(rule_tac x = "Suc mr" in exI, auto simp: )
 done
-lemma [simp]: "wadjust_goon_left_moving m rs (c, Oc # list) \<Longrightarrow>
+lemma wadjust_goon_left_moving_B_no_Oc[simp]:
+"wadjust_goon_left_moving_B m rs (c, Oc # list) = False"
+apply(auto simp: wadjust_goon_left_moving_B.simps)
+done
+lemma wadjust_goon_left_moving_Oc_move[simp]: "wadjust_goon_left_moving m rs (c, Oc # list) \<Longrightarrow>
 wadjust_goon_left_moving m rs (tl c, hd c # Oc # list)"
-apply(simp add: wadjust_goon_left_moving.simps)
+by(cases "hd c",auto simp: wadjust_goon_left_moving.simps)
-apply(case_tac "hd c", simp_all)
-done
+lemma wadjust_backto_standard_pos_B_no_Oc[simp]:
+"wadjust_backto_standard_pos_B m rs (c, Oc # list) = False"
-lemma [simp]: "wadjust_backto_standard_pos_B m rs (c, Oc # list) = False"
 apply(simp add: wadjust_backto_standard_pos_B.simps)
 done
-lemma [simp]: "wadjust_backto_standard_pos_O m rs (c, Bk # xs) = False"
+lemma wadjust_backto_standard_pos_O_no_Bk[simp]:
+"wadjust_backto_standard_pos_O m rs (c, Bk # xs) = False"
 apply(simp add: wadjust_backto_standard_pos_O.simps, auto)
 apply(case_tac mr, simp_all add: )
 done
-lemma [simp]: "wadjust_backto_standard_pos_O m rs ([], Oc # list) \<Longrightarrow>
+lemma wadjust_backto_standard_pos_B_Bk_Oc[simp]:
+"wadjust_backto_standard_pos_O m rs ([], Oc # list) \<Longrightarrow>
 wadjust_backto_standard_pos_B m rs ([], Bk # Oc # list)"
 apply(auto simp: wadjust_backto_standard_pos_O.simps
 wadjust_backto_standard_pos_B.simps)
 done
-lemma [simp]:
+lemma wadjust_backto_standard_pos_B_Bk_Oc_via_O[simp]:
 "\<lbrakk>wadjust_backto_standard_pos_O m rs (c, Oc # list); c \<noteq> []; hd c = Bk\<rbrakk>
 \<Longrightarrow> wadjust_backto_standard_pos_B m rs (tl c, Bk # Oc # list)"
 apply(simp add:wadjust_backto_standard_pos_O.simps
 wadjust_backto_standard_pos_B.simps, auto)
 done
-lemma [simp]: "\<lbrakk>wadjust_backto_standard_pos_O m rs (c, Oc # list); c \<noteq> []; hd c = Oc\<rbrakk>
+lemma wadjust_backto_standard_pos_B_Oc_Oc_via_O[simp]: "\<lbrakk>wadjust_backto_standard_pos_O m rs (c, Oc # list); c \<noteq> []; hd c = Oc\<rbrakk>
 \<Longrightarrow>  wadjust_backto_standard_pos_O m rs (tl c, Oc # Oc # list)"
 apply(simp add: wadjust_backto_standard_pos_O.simps, auto)
 apply(case_tac ml, simp_all add: , auto)
 done
-lemma [simp]: "wadjust_backto_standard_pos m rs (c, Oc # list)
+lemma wadjust_backto_standard_pos_cases[simp]: "wadjust_backto_standard_pos m rs (c, Oc # list)
 \<Longrightarrow> (c = [] \<longrightarrow> wadjust_backto_standard_pos m rs ([], Bk # Oc # list)) \<and>
 (c \<noteq> [] \<longrightarrow> wadjust_backto_standard_pos m rs (tl c, hd c # Oc # list))"
 apply(auto simp: wadjust_backto_standard_pos.simps)
 apply(case_tac "hd c", simp_all)
 done
-lemma [simp]: "wadjust_loop_right_move m rs (c, []) = False"
+lemma wadjust_loop_right_move_nonempty_snd[simp]: "wadjust_loop_right_move m rs (c, []) = False"
 apply(simp only: wadjust_loop_right_move.simps)
 apply(rule_tac iffI)
 apply(erule_tac exE)+
 apply(case_tac nr, simp_all add: )
 apply(case_tac mr, simp_all add: )
 done
-lemma [simp]: "wadjust_loop_erase m rs (c, []) = False"
+lemma wadjust_loop_erase_nonempty_snd[simp]: "wadjust_loop_erase m rs (c, []) = False"
 apply(simp only: wadjust_loop_erase.simps, auto)
 done
-lemma [simp]: "\<lbrakk>Suc (Suc rs) = a;  wadjust_loop_erase m rs (c, Bk # list)\<rbrakk>
+lemma wadjust_loop_erase_cases2[simp]: "\<lbrakk>Suc (Suc rs) = a;  wadjust_loop_erase m rs (c, Bk # list)\<rbrakk>
 \<Longrightarrow> a - length (takeWhile (\<lambda>a. a = Oc) (tl (dropWhile (\<lambda>a. a = Oc) (rev (tl c) @ hd c # Bk # list))))
 < a - length (takeWhile (\<lambda>a. a = Oc) (tl (dropWhile (\<lambda>a. a = Oc) (rev c @ Bk # list)))) \<or>
 a - length (takeWhile (\<lambda>a. a = Oc) (tl (dropWhile (\<lambda>a. a = Oc) (rev (tl c) @ hd c # Bk # list)))) =
 a - length (takeWhile (\<lambda>a. a = Oc) (tl (dropWhile (\<lambda>a. a = Oc) (rev c @ Bk # list))))"
 apply(simp only: wadjust_loop_erase.simps)
 apply(rule_tac disjI2)
 apply(case_tac c, simp, simp)
 done
-lemma [simp]:
+lemma dropWhile_exp1: "dropWhile (\<lambda>a. a = Oc) (Oc\<up>(n) @ xs) = dropWhile (\<lambda>a. a = Oc) xs"
+apply(induct n, simp_all add: )
+done
+lemma takeWhile_exp1: "takeWhile (\<lambda>a. a = Oc) (Oc\<up>(n) @ xs) = Oc\<up>(n) @ takeWhile (\<lambda>a. a = Oc) xs"
+apply(induct n, simp_all add: )
+done
+lemma wadjust_correctness_helper_1:
+assumes "Suc (Suc rs) = a" " wadjust_loop_right_move2 m rs (c, Bk # list)"
+shows "a - length (takeWhile (\<lambda>a. a = Oc) (tl (dropWhile (\<lambda>a. a = Oc) (rev c @ Oc # list))))
+< a - length (takeWhile (\<lambda>a. a = Oc) (tl (dropWhile (\<lambda>a. a = Oc) (rev c @ Bk # list))))"
+proof -
+have "ml + mr = Suc rs \<Longrightarrow> 0 < mr \<Longrightarrow>
+rs - (ml + length (takeWhile (\<lambda>a. a = Oc) list))
+< Suc rs -
+(ml +
+length
+(takeWhile (\<lambda>a. a = Oc)
+(Bk \<up> ln @ Bk # Bk # Oc \<up> mr @ Bk \<up> rn))) "
+for ml mr ln rn
+by(cases ln, auto)
+thus ?thesis using assms
+by (auto simp: wadjust_loop_right_move2.simps dropWhile_exp1 takeWhile_exp1)
+qed
+lemma wadjust_correctness_helper_2:
 "\<lbrakk>Suc (Suc rs) = a;  wadjust_loop_on_left_moving m rs (c, Bk # list)\<rbrakk>
 \<Longrightarrow> a - length (takeWhile (\<lambda>a. a = Oc) (tl (dropWhile (\<lambda>a. a = Oc) (rev (tl c) @ hd c # Bk # list))))
 < a - length (takeWhile (\<lambda>a. a = Oc) (tl (dropWhile (\<lambda>a. a = Oc) (rev c @ Bk # list)))) \<or>
 a - length (takeWhile (\<lambda>a. a = Oc) (tl (dropWhile (\<lambda>a. a = Oc) (rev (tl c) @ hd c # Bk # list)))) =
 a - length (takeWhile (\<lambda>a. a = Oc) (tl (dropWhile (\<lambda>a. a = Oc) (rev c @ Bk # list))))"
 apply(subgoal_tac "c \<noteq> []")
 apply(case_tac c, simp_all)
 done
-lemma dropWhile_exp1: "dropWhile (\<lambda>a. a = Oc) (Oc\<up>(n) @ xs) = dropWhile (\<lambda>a. a = Oc) xs"
+lemma wadjust_loop_check_empty_false[simp]: "wadjust_loop_check m rs ([], b) = False"
-apply(induct n, simp_all add: )
-done
-lemma takeWhile_exp1: "takeWhile (\<lambda>a. a = Oc) (Oc\<up>(n) @ xs) = Oc\<up>(n) @ takeWhile (\<lambda>a. a = Oc) xs"
-apply(induct n, simp_all add: )
-done
-lemma [simp]: "\<lbrakk>Suc (Suc rs) = a;  wadjust_loop_right_move2 m rs (c, Bk # list)\<rbrakk>
-\<Longrightarrow> a - length (takeWhile (\<lambda>a. a = Oc) (tl (dropWhile (\<lambda>a. a = Oc) (rev c @ Oc # list))))
-< a - length (takeWhile (\<lambda>a. a = Oc) (tl (dropWhile (\<lambda>a. a = Oc) (rev c @ Bk # list))))"
-apply(simp add: wadjust_loop_right_move2.simps, auto)
-apply(simp add: dropWhile_exp1 takeWhile_exp1)
-apply(case_tac ln, simp, simp add: )
-done
-lemma [simp]: "wadjust_loop_check m rs ([], b) = False"
 apply(simp add: wadjust_loop_check.simps)
 done
-lemma [simp]: "\<lbrakk>Suc (Suc rs) = a;  wadjust_loop_check m rs (c, Oc # list)\<rbrakk>
+lemma wadjust_loop_check_cases: "\<lbrakk>Suc (Suc rs) = a;  wadjust_loop_check m rs (c, Oc # list)\<rbrakk>
 \<Longrightarrow> a - length (takeWhile (\<lambda>a. a = Oc) (tl (dropWhile (\<lambda>a. a = Oc) (rev (tl c) @ hd c # Oc # list))))
 < a - length (takeWhile (\<lambda>a. a = Oc) (tl (dropWhile (\<lambda>a. a = Oc) (rev c @ Oc # list)))) \<or>
 a - length (takeWhile (\<lambda>a. a = Oc) (tl (dropWhile (\<lambda>a. a = Oc) (rev (tl c) @ hd c # Oc # list)))) =
 a - length (takeWhile (\<lambda>a. a = Oc) (tl (dropWhile (\<lambda>a. a = Oc) (rev c @ Oc # list))))"
 apply(case_tac "c", simp_all)
 done
-lemma [simp]:
+lemma wadjust_loop_erase_cases_or:
 "\<lbrakk>Suc (Suc rs) = a;  wadjust_loop_erase m rs (c, Oc # list)\<rbrakk>
 \<Longrightarrow> a - length (takeWhile (\<lambda>a. a = Oc) (tl (dropWhile (\<lambda>a. a = Oc) (rev c @ Bk # list))))
 < a - length (takeWhile (\<lambda>a. a = Oc) (tl (dropWhile (\<lambda>a. a = Oc) (rev c @ Oc # list)))) \<or>
 a - length (takeWhile (\<lambda>a. a = Oc) (tl (dropWhile (\<lambda>a. a = Oc) (rev c @ Bk # list)))) =
 a - length (takeWhile (\<lambda>a. a = Oc) (tl (dropWhile (\<lambda>a. a = Oc) (rev c @ Oc # list))))"
 apply(rule_tac disjI2)
 apply(auto)
 apply(simp add: dropWhile_exp1 takeWhile_exp1)
 done
+lemmas wadjust_correctness_helpers = wadjust_correctness_helper_2 wadjust_correctness_helper_1 wadjust_loop_erase_cases_or wadjust_loop_check_cases
 declare numeral_2_eq_2[simp del]
-lemma [simp]: "wadjust_start m rs (c, Bk # list)
+lemma wadjust_start_Oc[simp]: "wadjust_start m rs (c, Bk # list)
 \<Longrightarrow> wadjust_start m rs (c, Oc # list)"
 apply(auto simp: wadjust_start.simps)
 done
-lemma [simp]: "wadjust_backto_standard_pos m rs (c, Bk # list)
+lemma wadjust_stop_Bk[simp]: "wadjust_backto_standard_pos m rs (c, Bk # list)
 \<Longrightarrow> wadjust_stop m rs (Bk # c, list)"
 apply(auto simp: wadjust_backto_standard_pos.simps
 wadjust_stop.simps wadjust_backto_standard_pos_B.simps)
 done
-lemma [simp]: "wadjust_start m rs (c, Oc # list)
+lemma wadjust_loop_start_Oc[simp]: "wadjust_start m rs (c, Oc # list)
 \<Longrightarrow> wadjust_loop_start m rs (Oc # c, list)"
 apply(auto simp: wadjust_start.simps wadjust_loop_start.simps)
 apply(rule_tac x = ln in exI, simp)
 apply(rule_tac x = "rn" in exI, simp)
 apply(rule_tac x = 1 in exI, simp)
 done
-lemma [simp]:" wadjust_erase2 m rs (c, Oc # list)
+lemma erase2_Bk_if_Oc[simp]:" wadjust_erase2 m rs (c, Oc # list)
 \<Longrightarrow> wadjust_erase2 m rs (c, Bk # list)"
 apply(auto simp: wadjust_erase2.simps)
 done
 lemma wadjust_correctness:
 proof(rule_tac halt_lemma2)
 show "wf wadjust_le" by auto
 next
 show "\<forall> n. \<not> ?P (?f n) \<and> ?Q (?f n) \<longrightarrow>
 ?Q (?f (Suc n)) \<and> (?f (Suc n), ?f n) \<in> wadjust_le"
-apply(rule_tac allI, rule_tac impI, case_tac "?f n", simp)
+apply(rule_tac allI, rule_tac impI, case_tac "?f n")
-apply(simp add: step.simps)
+apply((case_tac d, case_tac [2] aa); simp add: step.simps)
-apply(case_tac d, case_tac [2] aa, simp_all)
 apply(simp_all only: wadjust_inv.simps split: if_splits)
 apply(simp_all)
 apply(simp_all add: wadjust_inv.simps wadjust_le_def
+wadjust_correctness_helpers
 Abacus.lex_triple_def Abacus.lex_pair_def lex_square_def  split: if_splits)
 done
 next
 show "?Q (?f 0)"
 apply(simp add: steps.simps wadjust_inv.simps wadjust_start.simps, auto)
 done
 thus"?thesis"
 apply(simp)
 done
 qed
-lemma [intro]: "tm_wf (t_wcode_adjust, 0)"
+lemma tm_wf_t_wcode_adjust[intro]: "tm_wf (t_wcode_adjust, 0)"
 apply(auto simp: t_wcode_adjust_def tm_wf.simps)
 done
-declare tm_comp.simps[simp del]
+lemma bl_bin_nonzero[simp]: "args \<noteq> [] \<Longrightarrow> bl_bin (<args::nat list>) > 0"
+by(cases args)
-lemma [simp]: "args \<noteq> [] \<Longrightarrow> bl_bin (<args::nat list>) > 0"
+(auto simp: tape_of_nl_cons bl_bin.simps)
-apply(case_tac args)
-apply(auto simp: tape_of_nl_cons bl_bin.simps split: if_splits)
-done
 lemma wcode_lemma_pre':
 "args \<noteq> [] \<Longrightarrow>
 \<exists> stp rn. steps0 (Suc 0, [], <m # args>)
 ((t_wcode_prepare |+| t_wcode_main) |+| t_wcode_adjust) stp
 lemma wcode_lemma:
 "args \<noteq> [] \<Longrightarrow>
 \<exists> stp ln rn. steps0 (Suc 0, [], <m # args>)  (t_wcode) stp =
 (0,  [Bk],  <[m ,bl_bin (<args>)]> @ Bk\<up>(rn))"
 using wcode_lemma_1[of args m]
-apply(simp add: t_wcode_def tape_of_nl_abv tape_of_nat_list.simps tape_of_nat_abv)
+apply(simp add: t_wcode_def tape_of_list_def tape_of_nat_list.simps tape_of_nat_def)
 done
 section {* The universal TM *}
 text {*
 definition UTM_pre :: "instr list"
 where
 "UTM_pre = t_wcode |+| t_utm"
 lemma tinres_step1:
-"\<lbrakk>tinres l l'; step (ss, l, r) (t, 0) = (sa, la, ra);
+assumes "tinres l l'" "step (ss, l, r) (t, 0) = (sa, la, ra)"
-step (ss, l', r) (t, 0) = (sb, lb, rb)\<rbrakk>
+"step (ss, l', r) (t, 0) = (sb, lb, rb)"
-\<Longrightarrow> tinres la lb \<and> ra = rb \<and> sa = sb"
+shows "tinres la lb \<and> ra = rb \<and> sa = sb"
-apply(case_tac ss, case_tac [!]r, case_tac [!] "a::cell")
+proof(cases "r")
-apply(auto simp: step.simps fetch.simps nth_of.simps
+case Nil
-split: if_splits )
+then show ?thesis using assms
-apply(case_tac [!] "t ! (2 * nat)",
+by (cases "(fetch t ss Bk)";cases "fst (fetch t ss Bk)";auto simp:step.simps split:if_splits)
-auto simp: tinres_def split: if_splits)
+next
-apply(case_tac [1-8] a, auto split: if_splits)
+case (Cons a list)
-apply(case_tac [!] "t ! (2 * nat)",
+then show ?thesis using assms
-auto simp: tinres_def split: if_splits)
+by (cases "(fetch t ss a)";cases "fst (fetch t ss a)";auto simp:step.simps split:if_splits)
-apply(case_tac [1-4] a, auto split: if_splits)
+qed
-apply(case_tac [!] "t ! Suc (2 * nat)",
-auto simp: if_splits)
-apply(case_tac [!] aa, auto split: if_splits)
-done
 lemma tinres_steps1:
 "\<lbrakk>tinres l l'; steps (ss, l, r) (t, 0) stp = (sa, la, ra);
 steps (ss, l', r) (t, 0) stp = (sb, lb, rb)\<rbrakk>
 \<Longrightarrow> tinres la lb \<and> ra = rb \<and> sa = sb"
 steps (ss, l', r) (t, 0) stp = (sb, lb, rb)\<rbrakk> \<Longrightarrow> tinres la lb \<and> ra = rb \<and> sa = sb"
 and h: " tinres l l'" "step (steps (ss, l, r) (t, 0) stp) (t, 0) = (sa, la, ra)"
 "step (steps (ss, l', r) (t, 0) stp) (t, 0) = (sb, lb, rb)" "steps (ss, l, r) (t, 0) stp = (a, b, c)"
 "steps (ss, l', r) (t, 0) stp = (aa, ba, ca)"
 have "tinres b ba \<and> c = ca \<and> a = aa"
-apply(rule_tac ind, simp_all add: h)
+using ind h by metis
-done
 thus "tinres la lb \<and> ra = rb \<and> sa = sb"
-apply(rule_tac l = b and l' = ba and r = c  and ss = a
+using tinres_step1 h by metis
-and t = t in tinres_step1)
-using h
-apply(simp, simp, simp)
-done
 qed
-lemma [simp]:
+lemma tinres_some_exp[simp]:
 "tinres (Bk \<up> m @ [Bk, Bk]) la \<Longrightarrow> \<exists>m. la = Bk \<up> m"
 apply(auto simp: tinres_def)
 apply(case_tac n, simp add: exp_ind)
 apply(rule_tac  x ="Suc (Suc m)" in exI, simp only: exp_ind, simp)
 apply(simp add: exp_ind del: replicate_Suc)
 using assms
 apply(case_tac rs, simp_all add: numeral_2_eq_2)
 done
 qed
-lemma [intro]: "tm_wf (t_wcode, 0)"
+lemma tm_wf_t_wcode[intro]: "tm_wf (t_wcode, 0)"
 apply(simp add: t_wcode_def)
 apply(rule_tac tm_wf_comp)
 apply(rule_tac tm_wf_comp, auto)
 done
-lemma [intro]: "tm_wf (t_utm, 0)"
-apply(simp only: t_utm_def F_tprog_def)
-apply(rule_tac wf_tm_from_abacus, auto)
-done
 lemma UTM_halt_lemma_pre:
 assumes wf_tm: "tm_wf (tp, 0)"
 and result: "0 < rs"
 and args: "args \<noteq> []"
 (\<lambda>(l, r). (\<exists>ln. l = Bk \<up> ln) \<and>
 (\<exists>rn. r = Oc \<up> rs @ Bk \<up> rn)) holds_for steps0 (Suc 0, [Bk],
 Oc # Oc \<up> code tp @ Bk # Oc # Oc \<up> bl_bin (<args>) @ Bk \<up> rn) t_utm n"
 using t_utm_halt_eq[of tp i "args" stp m rs k rn] assms
 apply(auto simp: bin_wc_eq)
-apply(rule_tac x = stpa in exI, simp add: tape_of_nl_abv tape_of_nat_abv)
+apply(rule_tac x = stpa in exI, simp add: tape_of_list_def tape_of_nat_def)
 done
 qed
 qed
 thus "?thesis"
 apply(auto simp: Hoare_halt_def UTM_pre_def)
 lemma nstd_case1: "0 < a \<Longrightarrow> NSTD (trpl_code (a, b, c))"
 apply(simp add: NSTD.simps trpl_code.simps)
 done
-lemma [simp]: "\<forall>m. b \<noteq> Bk\<up>(m) \<Longrightarrow> 0 < bl2wc b"
+lemma nonzero_bl2wc[simp]: "\<forall>m. b \<noteq> Bk\<up>(m) \<Longrightarrow> 0 < bl2wc b"
 apply(rule classical, simp)
 apply(induct b, erule_tac x = 0 in allE, simp)
 apply(simp add: bl2wc.simps, case_tac a, simp_all
 add: bl2nat.simps bl2nat_double)
 apply(case_tac "\<exists> m. b = Bk\<up>(m)",  erule exE)
 lemma nstd_case2: "\<forall>m. b \<noteq> Bk\<up>(m) \<Longrightarrow> NSTD (trpl_code (a, b, c))"
 apply(simp add: NSTD.simps trpl_code.simps)
 done
-lemma [elim]: "Suc (2 * x) = 2 * y \<Longrightarrow> RR"
+lemma even_not_odd[elim]: "Suc (2 * x) = 2 * y \<Longrightarrow> RR"
 apply(induct x arbitrary: y, simp, simp)
 apply(case_tac y, simp, simp)
 done
 declare replicate_Suc[simp del]
 apply(rule_tac tutm_uhalt, simp_all)
 done
 thus "False"
 using h
 apply(erule_tac x = n in allE)
-apply(simp add: tape_of_nl_abv bin_wc_eq tape_of_nat_abv)
+apply(simp add: tape_of_list_def bin_wc_eq tape_of_nat_def)
 done
 qed
 qed
 thus "?thesis"
 apply(simp add: Hoare_unhalt_def UTM_pre_def)
 show "\<exists>n. is_final (steps0 (Suc 0, [Bk], Oc \<up> Suc (code p) @ Bk # Oc \<up> Suc (bl_bin (<args>)) @ Bk \<up> rn) t_utm n) \<and>
 (\<lambda>(l, r). (\<exists>m. l = Bk \<up> m) \<and> (\<exists>n. r = Oc \<up> rs @ Bk \<up> n)) holds_for steps0
 (Suc 0, [Bk], Oc \<up> Suc (code p) @ Bk # Oc \<up> Suc (bl_bin (<args>)) @ Bk \<up> rn) t_utm n"
 using t_utm_halt_eq[of p i "args" stp m rs k rn] assms k
 apply(auto simp: bin_wc_eq, auto)
-apply(rule_tac x = stpa in exI, simp add: tape_of_nl_abv tape_of_nat_abv)
+apply(rule_tac x = stpa in exI, simp add: tape_of_list_def tape_of_nat_def)
 done
 qed
 next
 show "tm_wf0 t_wcode" by auto
 qed
 and args: "(args::nat list) \<noteq> []"
 and exec: "{(\<lambda>tp. tp = ([], <args>))} p {(\<lambda>tp. tp = (Bk\<up>m, <(n::nat)> @ Bk\<up>k))}"
 shows "{(\<lambda>tp. tp = ([], <code p # args>))} UTM {(\<lambda>tp. (\<exists> m k. tp = (Bk\<up>m, <n> @ Bk\<up>k)))}"
 using UTM_halt_lemma[OF assms(1) _ assms(2), where i="0"]
 using assms(3)
-apply(simp add: tape_of_nat_abv)
+apply(simp add: tape_of_nat_def)
 done
 lemma UTM_unhalt_lemma:
 assumes tm_wf: "tm_wf (p, 0)"
 and unhalt: "{(\<lambda>tp. tp = ([], <args>))} p \<up>"
 and args: "args \<noteq> []"
 shows "{(\<lambda>tp. tp = ([], <code p # args>))} UTM \<up>"
 using UTM_unhalt_lemma[OF assms(1), where i="0"]
 using assms(2-3)
-apply(simp add: tape_of_nat_abv)
+apply(simp add: tape_of_nat_def)
 done
 end

changeset 288	a9003e6d0463
parent 285	447b433b67fa
child 292	293e9c6f22e1