(* Title: thys/Abacus_Mopup.thy

   Author: Jian Xu, Xingyuan Zhang, and Christian Urban

   Modifications: Sebastiaan Joosten

*)

chapter {* Mopup Turing Machine that deletes all "registers", except one *}

theory Abacus_Mopup

imports Uncomputable

begin

fun mopup_a :: "nat \<Rightarrow> instr list"

  where

  "mopup_a 0 = []" |

  "mopup_a (Suc n) = mopup_a n @ 

       [(R, 2*n + 3), (W0, 2*n + 2), (R, 2*n + 1), (W1, 2*n + 2)]"

definition mopup_b :: "instr list"

  where

  "mopup_b \<equiv> [(R, 2), (R, 1), (L, 5), (W0, 3), (R, 4), (W0, 3),

            (R, 2), (W0, 3), (L, 5), (L, 6), (R, 0), (L, 6)]"

fun mopup :: "nat \<Rightarrow> instr list"

  where 

  "mopup n = mopup_a n @ shift mopup_b (2*n)"

type_synonym mopup_type = "config \<Rightarrow> nat list \<Rightarrow> nat \<Rightarrow> cell list \<Rightarrow> bool"

fun mopup_stop :: "mopup_type"

  where

  "mopup_stop (s, l, r) lm n ires= 

        (\<exists> ln rn. l = Bk\<up>ln @ Bk # Bk # ires \<and> r = <lm ! n> @ Bk\<up>rn)"

fun mopup_bef_erase_a :: "mopup_type"

  where

  "mopup_bef_erase_a (s, l, r) lm n ires= 

         (\<exists> ln m rn. l = Bk\<up>ln @ Bk # Bk # ires \<and> 

                  r = Oc\<up>m@ Bk # <(drop ((s + 1) div 2) lm)> @ Bk\<up>rn)"

fun mopup_bef_erase_b :: "mopup_type"

  where

  "mopup_bef_erase_b (s, l, r) lm n ires = 

      (\<exists> ln m rn. l = Bk\<up>ln @ Bk # Bk # ires \<and> r = Bk # Oc\<up>m @ Bk # 

                                      <(drop (s div 2) lm)> @ Bk\<up>rn)"

fun mopup_jump_over1 :: "mopup_type"

  where

  "mopup_jump_over1 (s, l, r) lm n ires = 

      (\<exists> ln m1 m2 rn. m1 + m2 = Suc (lm ! n) \<and> 

        l = Oc\<up>m1 @ Bk\<up>ln @ Bk # Bk # ires \<and> 

     (r = Oc\<up>m2 @ Bk # <(drop (Suc n) lm)> @ Bk\<up>rn \<or> 

     (r = Oc\<up>m2 \<and> (drop (Suc n) lm) = [])))"

fun mopup_aft_erase_a :: "mopup_type"

  where

  "mopup_aft_erase_a (s, l, r) lm n ires = 

      (\<exists> lnl lnr rn (ml::nat list) m. 

          m = Suc (lm ! n) \<and> l = Bk\<up>lnr @ Oc\<up>m @ Bk\<up>lnl @ Bk # Bk # ires \<and> 

                                   (r = <ml> @ Bk\<up>rn))"

fun mopup_aft_erase_b :: "mopup_type"

  where

  "mopup_aft_erase_b (s, l, r) lm n ires= 

   (\<exists> lnl lnr rn (ml::nat list) m. 

      m = Suc (lm ! n) \<and> 

      l = Bk\<up>lnr @ Oc\<up>m @ Bk\<up>lnl @ Bk # Bk # ires \<and> 

     (r = Bk # <ml> @ Bk\<up>rn \<or>

      r = Bk # Bk # <ml> @ Bk\<up>rn))"

fun mopup_aft_erase_c :: "mopup_type"

  where

  "mopup_aft_erase_c (s, l, r) lm n ires = 

 (\<exists> lnl lnr rn (ml::nat list) m. 

     m = Suc (lm ! n) \<and> 

     l = Bk\<up>lnr @ Oc\<up>m @ Bk\<up>lnl @ Bk # Bk # ires \<and> 

    (r = <ml> @ Bk\<up>rn \<or> r = Bk # <ml> @ Bk\<up>rn))"

fun mopup_left_moving :: "mopup_type"

  where

  "mopup_left_moving (s, l, r) lm n ires = 

  (\<exists> lnl lnr rn m.

     m = Suc (lm ! n) \<and> 

   ((l = Bk\<up>lnr @ Oc\<up>m @ Bk\<up>lnl @ Bk # Bk # ires \<and> r = Bk\<up>rn) \<or>

    (l = Oc\<up>(m - 1) @ Bk\<up>lnl @ Bk # Bk # ires \<and> r = Oc # Bk\<up>rn)))"

fun mopup_jump_over2 :: "mopup_type"

  where

  "mopup_jump_over2 (s, l, r) lm n ires = 

     (\<exists> ln rn m1 m2.

          m1 + m2 = Suc (lm ! n) 

        \<and> r \<noteq> [] 

        \<and> (hd r = Oc \<longrightarrow> (l = Oc\<up>m1 @ Bk\<up>ln @ Bk # Bk # ires \<and> r = Oc\<up>m2 @ Bk\<up>rn)) 

        \<and> (hd r = Bk \<longrightarrow> (l = Bk\<up>ln @ Bk # ires \<and> r = Bk # Oc\<up>(m1+m2)@ Bk\<up>rn)))"

fun mopup_inv :: "mopup_type"

  where

  "mopup_inv (s, l, r) lm n ires = 

      (if s = 0 then mopup_stop (s, l, r) lm n ires

       else if s \<le> 2*n then

               if s mod 2 = 1 then mopup_bef_erase_a (s, l, r) lm n ires

                   else mopup_bef_erase_b (s, l, r) lm n ires

            else if s = 2*n + 1 then 

                mopup_jump_over1 (s, l, r) lm n ires

            else if s = 2*n + 2 then mopup_aft_erase_a (s, l, r) lm n ires

            else if s = 2*n + 3 then mopup_aft_erase_b (s, l, r) lm n ires

            else if s = 2*n + 4 then mopup_aft_erase_c (s, l, r) lm n ires

            else if s = 2*n + 5 then mopup_left_moving (s, l, r) lm n ires

            else if s = 2*n + 6 then mopup_jump_over2 (s, l, r) lm n ires

            else False)"

lemma mopup_fetch_0[simp]: 

     "(fetch (mopup_a n @ shift mopup_b (2 * n)) 0 b) = (Nop, 0)"

by(simp add: fetch.simps)

lemma mop_bef_length[simp]: "length (mopup_a n) = 4 * n"

apply(induct n, simp_all add: mopup_a.simps)

done

lemma mopup_a_nth: 

  "\<lbrakk>q < n; x < 4\<rbrakk> \<Longrightarrow> mopup_a n ! (4 * q + x) = 

                             mopup_a (Suc q) ! ((4 * q) + x)"

apply(induct n, simp)

apply(case_tac "q < n", simp add: mopup_a.simps, auto)

apply(simp add: nth_append)

apply(subgoal_tac "q = n", simp)

apply(arith)

done

lemma fetch_bef_erase_a_o[simp]: 

 "\<lbrakk>0 < s; s \<le> 2 * n; s mod 2 = Suc 0\<rbrakk>

  \<Longrightarrow> (fetch (mopup_a n @ shift mopup_b (2 * n)) s Oc) = (W0, s + 1)"

apply(subgoal_tac "\<exists> q. s = 2*q + 1", auto)

apply(subgoal_tac "length (mopup_a n) = 4*n")

apply(auto simp: fetch.simps nth_of.simps nth_append)

apply(subgoal_tac "mopup_a n ! (4 * q + 1) = 

                      mopup_a (Suc q) ! ((4 * q) + 1)", 

      simp add: mopup_a.simps nth_append)

apply(rule mopup_a_nth, auto)

apply arith

done

lemma fetch_bef_erase_a_b[simp]:

  "\<lbrakk>0 < s; s \<le> 2 * n; s mod 2 = Suc 0\<rbrakk>

   \<Longrightarrow>  (fetch (mopup_a n @ shift mopup_b (2 * n)) s Bk) = (R, s + 2)"

apply(subgoal_tac "\<exists> q. s = 2*q + 1", auto)

apply(subgoal_tac "length (mopup_a n) = 4*n")

apply(auto simp: fetch.simps nth_of.simps nth_append)

apply(subgoal_tac "mopup_a n ! (4 * q + 0) = 

                       mopup_a (Suc q) ! ((4 * q + 0))", 

      simp add: mopup_a.simps nth_append)

apply(rule mopup_a_nth, auto)

apply arith

done

lemma fetch_bef_erase_b_b: 

  "\<lbrakk>n < length lm; 0 < s; s \<le> 2 * n; s mod 2 = 0\<rbrakk> \<Longrightarrow> 

     (fetch (mopup_a n @ shift mopup_b (2 * n)) s Bk) = (R, s - 1)"

apply(subgoal_tac "\<exists> q. s = 2 * q", auto)

apply(case_tac q, simp, simp)

apply(auto simp: fetch.simps nth_of.simps nth_append)

apply(subgoal_tac "mopup_a n ! (4 * nat + 2) = 

                     mopup_a (Suc nat) ! ((4 * nat) + 2)", 

      simp add: mopup_a.simps nth_append)

apply(rule mopup_a_nth, auto)

done

lemma fetch_jump_over1_o: 

 "fetch (mopup_a n @ shift mopup_b (2 * n)) (Suc (2 * n)) Oc

  = (R, Suc (2 * n))"

apply(subgoal_tac "length (mopup_a n) = 4 * n")

apply(auto simp: fetch.simps nth_of.simps mopup_b_def nth_append 

                 shift.simps)

done

lemma fetch_jump_over1_b: 

 "fetch (mopup_a n @ shift mopup_b (2 * n)) (Suc (2 * n)) Bk 

 = (R, Suc (Suc (2 * n)))"

apply(subgoal_tac "length (mopup_a n) = 4 * n")

apply(auto simp: fetch.simps nth_of.simps mopup_b_def 

                 nth_append shift.simps)

done

lemma fetch_aft_erase_a_o: 

 "fetch (mopup_a n @ shift mopup_b (2 * n)) (Suc (Suc (2 * n))) Oc 

 = (W0, Suc (2 * n + 2))"

apply(subgoal_tac "length (mopup_a n) = 4 * n")

apply(auto simp: fetch.simps nth_of.simps mopup_b_def 

                 nth_append shift.simps)

done

lemma fetch_aft_erase_a_b: 

 "fetch (mopup_a n @ shift mopup_b (2 * n)) (Suc (Suc (2 * n))) Bk

  = (L, Suc (2 * n + 4))"

apply(subgoal_tac "length (mopup_a n) = 4 * n")

apply(auto simp: fetch.simps nth_of.simps mopup_b_def 

                 nth_append shift.simps)

done

lemma fetch_aft_erase_b_b: 

 "fetch (mopup_a n @ shift mopup_b (2 * n)) (2*n + 3) Bk

  = (R, Suc (2 * n + 3))"

apply(subgoal_tac "length (mopup_a n) = 4 * n")

apply(subgoal_tac "2*n + 3 = Suc (2*n + 2)", simp only: fetch.simps)

apply(auto simp: nth_of.simps mopup_b_def nth_append shift.simps)

done

lemma fetch_aft_erase_c_o: 

 "fetch (mopup_a n @ shift mopup_b (2 * n)) (2 * n + 4) Oc 

 = (W0, Suc (2 * n + 2))"

apply(subgoal_tac "length (mopup_a n) = 4 * n")

apply(subgoal_tac "2*n + 4 = Suc (2*n + 3)", simp only: fetch.simps)

apply(auto simp: nth_of.simps mopup_b_def nth_append shift.simps)

done

lemma fetch_aft_erase_c_b: 

 "fetch (mopup_a n @ shift mopup_b (2 * n)) (2 * n + 4) Bk 

 = (R, Suc (2 * n + 1))"

apply(subgoal_tac "length (mopup_a n) = 4 * n")

apply(subgoal_tac "2*n + 4 = Suc (2*n + 3)", simp only: fetch.simps)

apply(auto simp: nth_of.simps mopup_b_def nth_append shift.simps)

done

lemma fetch_left_moving_o: 

 "(fetch (mopup_a n @ shift mopup_b (2 * n)) (2 * n + 5) Oc) 

 = (L, 2*n + 6)"

apply(subgoal_tac "length (mopup_a n) = 4 * n")

apply(subgoal_tac "2*n + 5 = Suc (2*n + 4)", simp only: fetch.simps)

apply(auto simp: nth_of.simps mopup_b_def nth_append shift.simps)

done

lemma fetch_left_moving_b: 

 "(fetch (mopup_a n @ shift mopup_b (2 * n)) (2 * n + 5) Bk)

  = (L, 2*n + 5)"

apply(subgoal_tac "length (mopup_a n) = 4 * n")

apply(subgoal_tac "2*n + 5 = Suc (2*n + 4)", simp only: fetch.simps)

apply(auto simp: nth_of.simps mopup_b_def nth_append shift.simps)

done

lemma fetch_jump_over2_b:

  "(fetch (mopup_a n @ shift mopup_b (2 * n)) (2 * n + 6) Bk) 

 = (R, 0)"

apply(subgoal_tac "length (mopup_a n) = 4 * n")

apply(subgoal_tac "2*n + 6 = Suc (2*n + 5)", simp only: fetch.simps)

apply(auto simp: nth_of.simps mopup_b_def nth_append shift.simps)

done

lemma fetch_jump_over2_o: 

"(fetch (mopup_a n @ shift mopup_b (2 * n)) (2 * n + 6) Oc) 

 = (L, 2*n + 6)"

apply(subgoal_tac "length (mopup_a n) = 4 * n")

apply(subgoal_tac "2*n + 6 = Suc (2*n + 5)", simp only: fetch.simps)

apply(auto simp: nth_of.simps mopup_b_def nth_append shift.simps)

done

lemmas mopupfetchs = 

fetch_bef_erase_a_o fetch_bef_erase_a_b fetch_bef_erase_b_b 

fetch_jump_over1_o fetch_jump_over1_b fetch_aft_erase_a_o 

fetch_aft_erase_a_b fetch_aft_erase_b_b fetch_aft_erase_c_o 

fetch_aft_erase_c_b fetch_left_moving_o fetch_left_moving_b 

fetch_jump_over2_b fetch_jump_over2_o

declare 

  mopup_jump_over2.simps[simp del] mopup_left_moving.simps[simp del]

  mopup_aft_erase_c.simps[simp del] mopup_aft_erase_b.simps[simp del] 

  mopup_aft_erase_a.simps[simp del] mopup_jump_over1.simps[simp del]

  mopup_bef_erase_a.simps[simp del] mopup_bef_erase_b.simps[simp del]

  mopup_stop.simps[simp del]

lemma [simp]: 

  "\<lbrakk>mopup_bef_erase_a (s, l, Oc # xs) lm n ires\<rbrakk> \<Longrightarrow> 

  mopup_bef_erase_b (Suc s, l, Bk # xs) lm n ires"

apply(auto simp: mopup_bef_erase_a.simps mopup_bef_erase_b.simps )

apply(rule_tac x = "m - 1" in exI, rule_tac x = rn in exI)

apply(case_tac m, simp, simp add: replicate_Suc)

done

lemma mopup_false1:

  "\<lbrakk>0 < s; s \<le> 2 * n; s mod 2 = Suc 0;  \<not> Suc s \<le> 2 * n\<rbrakk> 

  \<Longrightarrow> RR"

apply(arith)

done

lemma [simp]: 

 "\<lbrakk>n < length lm; 0 < s; s \<le> 2 * n; s mod 2 = Suc 0; 

   mopup_bef_erase_a (s, l, Oc # xs) lm n ires; r = Oc # xs\<rbrakk>

 \<Longrightarrow> (Suc s \<le> 2 * n \<longrightarrow> mopup_bef_erase_b (Suc s, l, Bk # xs) lm n ires)  \<and>

     (\<not> Suc s \<le> 2 * n \<longrightarrow> mopup_jump_over1 (Suc s, l, Bk # xs) lm n ires) "

apply(auto elim: mopup_false1)

done

lemma tape_of_nl_cons: "<m # lm> = (if lm = [] then Oc\<up>(Suc m)

                    else Oc\<up>(Suc m) @ Bk # <lm>)"

  by(case_tac lm, simp_all add: tape_of_list_def  tape_of_nat_def split: if_splits)

lemma drop_tape_of_cons: 

  "\<lbrakk>Suc q < length lm; x = lm ! q\<rbrakk> \<Longrightarrow> <drop q lm> = Oc # Oc \<up> x @ Bk # <drop (Suc q) lm>"

  using Suc_lessD append_Cons list.simps(2) Cons_nth_drop_Suc replicate_Suc tape_of_nl_cons

  by metis

lemma erase2jumpover1:

  "\<lbrakk>q < length list; 

             \<forall>rn. <drop q list> \<noteq> Oc # Oc \<up> (list ! q) @ Bk # <drop (Suc q) list> @ Bk \<up> rn\<rbrakk>

       \<Longrightarrow> <drop q list> = Oc # Oc \<up> (list ! q)"

apply(erule_tac x = 0 in allE, simp)

apply(case_tac "Suc q < length list")

apply(erule_tac notE)

apply(rule_tac drop_tape_of_cons, simp_all)

apply(subgoal_tac "length list = Suc q", auto)

apply(subgoal_tac "drop q list = [list ! q]")

apply(simp add: tape_of_nat_def tape_of_list_def replicate_Suc)

by (metis append_Nil2 append_eq_conv_conj Cons_nth_drop_Suc lessI)

lemma erase2jumpover2:

  "\<lbrakk>q < length list; \<forall>rn. <drop q list> @ Bk # Bk \<up> n \<noteq>

  Oc # Oc \<up> (list ! q) @ Bk # <drop (Suc q) list> @ Bk \<up> rn\<rbrakk>

  \<Longrightarrow> RR"

apply(case_tac "Suc q < length list")

apply(erule_tac x = "Suc n" in allE, simp)

apply(erule_tac notE, simp add: replicate_Suc)

apply(rule_tac drop_tape_of_cons, simp_all)

apply(subgoal_tac "length list = Suc q", auto)

apply(erule_tac x = "n" in allE, simp add: tape_of_list_def)

by (metis append_Nil2 append_eq_conv_conj Cons_nth_drop_Suc lessI replicate_Suc tape_of_list_def tape_of_nl_cons)

lemma mod_ex1: "(a mod 2 = Suc 0) = (\<exists> q. a = Suc (2 * q))"

by arith

declare replicate_Suc[simp]

lemma mopup_bef_erase_a_2_jump_over[simp]: 

 "\<lbrakk>n < length lm; 0 < s; s mod 2 = Suc 0;  s \<le> 2 * n;

   mopup_bef_erase_a (s, l, Bk # xs) lm n ires; \<not> (Suc (Suc s) \<le> 2 * n)\<rbrakk> 

\<Longrightarrow> mopup_jump_over1 (s', Bk # l, xs) lm n ires"

apply(auto simp: mopup_bef_erase_a.simps mopup_jump_over1.simps)

apply(case_tac m, auto simp: mod_ex1)

apply(subgoal_tac "n = Suc q", auto)

apply(rule_tac x = "Suc ln" in exI, rule_tac x = 0 in exI, auto)

apply(case_tac [!] lm, simp_all)

apply(case_tac [!] rn, auto elim: erase2jumpover1 erase2jumpover2)

apply(erule_tac x = 0 in allE, simp)

apply(rule_tac classical, simp)

apply(erule_tac notE)

apply(rule_tac drop_tape_of_cons, simp_all)

done

lemma Suc_Suc_div:  "\<lbrakk>0 < s; s mod 2 = Suc 0; Suc (Suc s) \<le> 2 * n\<rbrakk>

           \<Longrightarrow> (Suc (Suc (s div 2))) \<le> n"

apply(arith)

done

lemma mopup_bef_erase_a_2_a[simp]: 

 "\<lbrakk>n < length lm; 0 < s; s mod 2 = Suc 0; 

   mopup_bef_erase_a (s, l, Bk # xs) lm n ires; 

   Suc (Suc s) \<le> 2 * n\<rbrakk> \<Longrightarrow> 

   mopup_bef_erase_a (Suc (Suc s), Bk # l, xs) lm n ires"

apply(auto simp: mopup_bef_erase_a.simps)

apply(subgoal_tac "drop (Suc (Suc (s div 2))) lm \<noteq> []")

apply(case_tac m, simp_all)

apply(rule_tac x = "Suc ln" in exI, simp)

apply arith

apply(case_tac m, simp_all)

apply(rule_tac x = "Suc (lm ! (Suc s div 2))" in exI, simp)

apply(rule_tac x = rn in exI, simp)

apply(rule_tac drop_tape_of_cons, simp, auto)

done

lemma mopup_false2: 

 "\<lbrakk>0 < s; s \<le> 2 * n; 

   s mod 2 = Suc 0; Suc s \<noteq> 2 * n;

   \<not> Suc (Suc s) \<le> 2 * n\<rbrakk> \<Longrightarrow> RR"

apply(arith)

done

lemma [simp]: "mopup_bef_erase_a (s, l, []) lm n ires \<Longrightarrow> 

                        mopup_bef_erase_a (s, l, [Bk]) lm n ires"

apply(auto simp: mopup_bef_erase_a.simps)

done

lemma [simp]:

   "\<lbrakk>n < length lm; 0 < s; s \<le> 2 * n; s mod 2 = Suc 0; \<not> Suc (Suc s) \<le> 2 *n;

     mopup_bef_erase_a (s, l, []) lm n ires\<rbrakk>

    \<Longrightarrow>  mopup_jump_over1 (s', Bk # l, []) lm n ires"

by auto

lemma "mopup_bef_erase_b (s, l, Oc # xs) lm n ires \<Longrightarrow> l \<noteq> []"

apply(auto simp: mopup_bef_erase_b.simps)

done

lemma [simp]: "mopup_bef_erase_b (s, l, Oc # xs) lm n ires = False"

apply(auto simp: mopup_bef_erase_b.simps )

done

lemma [simp]: "\<lbrakk>0 < s; s \<le> 2 *n; s mod 2 \<noteq> Suc 0\<rbrakk> \<Longrightarrow> 

                                      (s - Suc 0) mod 2 = Suc 0"

apply(arith)

done

lemma [simp]: "\<lbrakk>0 < s; s \<le> 2 *n; s mod 2 \<noteq> Suc 0\<rbrakk> \<Longrightarrow>

                                       s - Suc 0 \<le> 2 * n"

apply(simp)

done

lemma [simp]: "\<lbrakk>0 < s; s \<le> 2 *n; s mod 2 \<noteq> Suc 0\<rbrakk> \<Longrightarrow> \<not> s \<le> Suc 0"

apply(arith)

done

lemma [simp]: "\<lbrakk>n < length lm; 0 < s; s \<le> 2 * n; 

               s mod 2 \<noteq> Suc 0; 

               mopup_bef_erase_b (s, l, Bk # xs) lm n ires; r = Bk # xs\<rbrakk> 

           \<Longrightarrow> mopup_bef_erase_a (s - Suc 0, Bk # l, xs) lm n ires"

apply(auto simp: mopup_bef_erase_b.simps mopup_bef_erase_a.simps)

apply(rule_tac x = "Suc ln" in exI, simp)

done

lemma [simp]: "\<lbrakk>mopup_bef_erase_b (s, l, []) lm n ires\<rbrakk> \<Longrightarrow> 

                   mopup_bef_erase_a (s - Suc 0, Bk # l, []) lm n ires"

apply(auto simp: mopup_bef_erase_b.simps mopup_bef_erase_a.simps)

done

lemma [simp]: 

   "\<lbrakk>n < length lm;

    mopup_jump_over1 (Suc (2 * n), l, Oc # xs) lm n ires;

    r = Oc # xs\<rbrakk>

  \<Longrightarrow> mopup_jump_over1 (Suc (2 * n), Oc # l, xs) lm n ires"

apply(auto simp: mopup_jump_over1.simps)

apply(rule_tac x = ln in exI, rule_tac x = "Suc m1" in exI,

       rule_tac x = "m2 - 1" in exI, simp)

apply(case_tac "m2", simp, simp)

apply(rule_tac x = ln in exI, rule_tac x = "Suc m1" in exI, 

      rule_tac x = "m2 - 1" in exI)

apply(case_tac m2, simp, simp)

done

lemma mopup_jump_over1_2_aft_erase_a[simp]:  

 "\<lbrakk>n < length lm; mopup_jump_over1 (Suc (2 * n), l, Bk # xs) lm n ires\<rbrakk>

  \<Longrightarrow> mopup_aft_erase_a (Suc (Suc (2 * n)), Bk # l, xs) lm n ires"

apply(simp only: mopup_jump_over1.simps mopup_aft_erase_a.simps)

apply(erule_tac exE)+

apply(rule_tac x = ln in exI, rule_tac x = "Suc 0" in exI)

apply(case_tac m2, simp)

apply(rule_tac x = rn in exI, rule_tac x = "drop (Suc n) lm" in exI, 

      simp)

apply(simp)

done

lemma [simp]: 

 "\<lbrakk>n < length lm; mopup_jump_over1 (Suc (2 * n), l, []) lm n ires\<rbrakk> \<Longrightarrow> 

    mopup_aft_erase_a (Suc (Suc (2 * n)), Bk # l, []) lm n ires"

apply(rule mopup_jump_over1_2_aft_erase_a, simp)

apply(auto simp: mopup_jump_over1.simps)

apply(rule_tac x = ln in exI, rule_tac x = "Suc (lm ! n)" in exI, 

      rule_tac x = 0 in exI, simp add: tape_of_list_def )

done

lemma [simp]: "<[]> = []" by(simp add: tape_of_list_def)

lemma [simp]: 

 "\<lbrakk>n < length lm; 

   mopup_aft_erase_a (Suc (Suc (2 * n)), l, Oc # xs) lm n ires\<rbrakk> 

 \<Longrightarrow> mopup_aft_erase_b (Suc (Suc (Suc (2 * n))), l, Bk # xs) lm n ires"

apply(auto simp: mopup_aft_erase_a.simps mopup_aft_erase_b.simps )

apply(case_tac ml)

apply(simp_all add: tape_of_nl_cons split: if_splits)

apply(case_tac rn, simp_all)

apply(case_tac a, simp_all)

apply(rule_tac x = rn in exI, rule_tac x = "[]" in exI, simp)

apply(rule_tac x = rn in exI, rule_tac x = "[nat]" in exI, simp)

apply(case_tac a, simp,  simp add: tape_of_list_def tape_of_nat_def)

apply(case_tac a, simp_all)

apply(rule_tac x = rn in exI, rule_tac x = "list" in exI, simp)

apply(rule_tac x = rn in exI, simp)

apply(rule_tac x = "nat # list" in exI, simp add: tape_of_nl_cons)

done

lemma [simp]:

  "mopup_aft_erase_a (Suc (Suc (2 * n)), l, Bk # xs) lm n ires \<Longrightarrow> l \<noteq> []"

apply(auto simp: mopup_aft_erase_a.simps)

done

lemma [simp]:

  "\<lbrakk>n < length lm;

    mopup_aft_erase_a (Suc (Suc (2 * n)), l, Bk # xs) lm n ires\<rbrakk>

  \<Longrightarrow> mopup_left_moving (5 + 2 * n, tl l, hd l # Bk # xs) lm n ires"

apply(simp only: mopup_aft_erase_a.simps mopup_left_moving.simps)

apply(erule exE)+

apply(case_tac lnr, simp)

apply(case_tac ml, auto simp: tape_of_nl_cons)

apply(case_tac ml, auto simp: tape_of_nl_cons)

apply(rule_tac x = "Suc rn" in exI, simp)

done

lemma [simp]:

  "mopup_aft_erase_a (Suc (Suc (2 * n)), l, []) lm n ires \<Longrightarrow> l \<noteq> []"

apply(simp only: mopup_aft_erase_a.simps)

apply(erule exE)+

apply(auto)

done

lemma [simp]:

  "\<lbrakk>n < length lm; mopup_aft_erase_a (Suc (Suc (2 * n)), l, []) lm n ires\<rbrakk>

  \<Longrightarrow> mopup_left_moving (5 + 2 * n, tl l, [hd l]) lm n ires"

apply(simp only: mopup_aft_erase_a.simps mopup_left_moving.simps)

apply(erule exE)+

apply(subgoal_tac "ml = [] \<and> rn = 0", erule conjE, erule conjE, simp)

apply(case_tac lnr, simp)

apply(rule_tac x = lnl in exI, auto)

apply(rule_tac x = 1 in exI, simp)

apply(case_tac ml, simp, simp add: tape_of_nl_cons split: if_splits)

done

lemma [simp]: "mopup_aft_erase_b (2 * n + 3, l, Oc # xs) lm n ires = False"

apply(auto simp: mopup_aft_erase_b.simps )

done

lemma tape_of_ex1[intro]: 

  "\<exists>rna ml. Oc \<up> a @ Bk \<up> rn = <ml::nat list> @ Bk \<up> rna \<or> Oc \<up> a @ Bk \<up> rn = Bk # <ml> @ Bk \<up> rna"

apply(case_tac a, simp_all)

apply(rule_tac x = rn in exI, rule_tac x = "[]" in exI, simp)

apply(rule_tac x = rn in exI, rule_tac x = "[nat]" in exI, simp)

apply(simp add: tape_of_list_def tape_of_nat_def)

done

lemma [intro]: "\<exists>rna ml. Oc \<up> a @ Bk # <list::nat list> @ Bk \<up> rn = 

  <ml> @ Bk \<up> rna \<or> Oc \<up> a @ Bk # <list> @ Bk \<up> rn = Bk # <ml::nat list> @ Bk \<up> rna"

apply(case_tac "list = []", simp add: replicate_Suc[THEN sym] del: replicate_Suc)