(* Title: thys/Abacus_Mopup.thy
   Author: Jian Xu, Xingyuan Zhang, and Christian Urban
*)

header {* 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 qa, 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>)"
apply(case_tac lm, simp_all add: tape_of_nl_abv  tape_of_nat_abv split: if_splits)
done

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>"
by (metis Suc_lessD append_Cons list.simps(2) nth_drop' replicate_Suc tape_of_nl_cons)

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_nl_abv tape_of_nat_abv replicate_Suc)
by (metis append_Nil2 append_eq_conv_conj drop_Suc_conv_tl 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_nl_abv)
by (metis append_Nil2 append_eq_conv_conj drop_Suc_conv_tl lessI replicate_Suc tape_of_nl_abv 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_nl_abv )
done

lemma [simp]: "<[]> = []"
apply(simp add: tape_of_nl_abv)
done

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_nl_abv tape_of_nat_abv)
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_nl_abv tape_of_nat_abv)
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)
apply(rule_tac rn = "Suc rn" in tape_of_ex1)
apply(case_tac a, simp)
apply(rule_tac x = rn in exI, rule_tac x = list in exI, simp)
apply(rule_tac x = rn in exI, rule_tac x = "nat # list" in exI)
apply(simp add: tape_of_nl_cons)
done

lemma [simp]: 
 "\<lbrakk>n < length lm; 
   mopup_aft_erase_c (2 * n + 4, 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_c.simps mopup_aft_erase_b.simps )
apply(case_tac ml, simp_all add: tape_of_nl_cons split: if_splits, auto)
apply(case_tac rn, simp_all)
done

lemma mopup_aft_erase_c_aft_erase_a[simp]: 
 "\<lbrakk>n < length lm; mopup_aft_erase_c (2 * n + 4, 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_aft_erase_c.simps mopup_aft_erase_a.simps )
apply(erule_tac exE)+
apply(erule conjE, erule conjE, erule disjE)
apply(subgoal_tac "ml = []", simp, case_tac rn, 
      simp, simp, rule conjI)
apply(rule_tac x = lnl in exI, rule_tac x = "Suc lnr" in exI, simp)
apply(rule_tac x = nat in exI, rule_tac x = "[]" in exI, simp)
apply(case_tac ml, simp, simp add: tape_of_nl_cons split: if_splits)
apply(rule_tac x = lnl in exI, rule_tac x = "Suc lnr" in exI, simp)
apply(rule_tac x = rn in exI, rule_tac x = "ml" in exI, simp)
done

lemma [simp]: 
 "\<lbrakk>n < length lm; mopup_aft_erase_c (2 * n + 4, l, []) lm n ires\<rbrakk> 
 \<Longrightarrow> mopup_aft_erase_a (Suc (Suc (2 * n)), Bk # l, []) lm n ires"
apply(rule mopup_aft_erase_c_aft_erase_a, simp)
apply(simp only: mopup_aft_erase_c.simps)
apply(erule exE)+
apply(rule_tac x = lnl in exI, rule_tac x = lnr in exI, simp add: )
apply(rule_tac x = 0 in exI, rule_tac x = "[]" in exI, simp)
done

lemma mopup_aft_erase_b_2_aft_erase_c[simp]:
  "\<lbrakk>n < length lm; mopup_aft_erase_b (2 * n + 3, l, Bk # xs) lm n ires\<rbrakk>  
 \<Longrightarrow> mopup_aft_erase_c (4 + 2 * n, Bk # l, xs) lm n ires"
apply(auto simp: mopup_aft_erase_b.simps mopup_aft_erase_c.simps)
apply(rule_tac x = "lnl" in exI, rule_tac x = "Suc lnr" in exI, simp)
apply(rule_tac x = "lnl" in exI, rule_tac x = "Suc lnr" in exI, simp)
done

lemma [simp]: 
 "\<lbrakk>n < length lm; mopup_aft_erase_b (2 * n + 3, l, []) lm n ires\<rbrakk> 
 \<Longrightarrow> mopup_aft_erase_c (4 + 2 * n, Bk # l, []) lm n ires"
apply(rule_tac mopup_aft_erase_b_2_aft_erase_c, simp)
apply(simp add: mopup_aft_erase_b.simps)
done

lemma [simp]: 
    "mopup_left_moving (2 * n + 5, l, Oc # xs) lm n ires \<Longrightarrow> l \<noteq> []"
apply(auto simp: mopup_left_moving.simps)
done

lemma exp_ind: "a\<up>(Suc x) = a\<up>x @ [a]"
apply(induct x, auto)
done

lemma [simp]:  
 "\<lbrakk>n < length lm; mopup_left_moving (2 * n + 5, l, Oc # xs) lm n ires\<rbrakk>
  \<Longrightarrow> mopup_jump_over2 (2 * n + 6, tl l, hd l # Oc # xs) lm n ires"
apply(simp only: mopup_left_moving.simps mopup_jump_over2.simps)
apply(erule_tac exE)+
apply(erule conjE, erule disjE, erule conjE)
apply(case_tac rn, simp, simp add: )
apply(case_tac "hd l", simp add:  )
apply(case_tac "lm ! n", simp)
apply(rule_tac x = "lnl" in exI, rule_tac x = rn in exI, 
      rule_tac x = "Suc 0" in exI, rule_tac x = 0 in exI)
apply(case_tac lnl, simp,simp,  simp add: exp_ind[THEN sym])
apply(case_tac "lm ! n", simp)
apply(case_tac lnl, simp, simp)
apply(rule_tac x = lnl in exI, rule_tac x = rn in exI, auto)
apply(case_tac "lm ! n", simp)
apply(case_tac lnl, simp_all add: numeral_2_eq_2)
done

lemma [simp]: "mopup_left_moving (2 * n + 5, l, xs) lm n ires \<Longrightarrow> l \<noteq> []"
apply(auto simp: mopup_left_moving.simps)
done

lemma [simp]:
  "\<lbrakk>n < length lm; mopup_left_moving (2 * n + 5, l, Bk # xs) lm n ires\<rbrakk> 
 \<Longrightarrow> mopup_left_moving (2 * n + 5, tl l, hd l # Bk # xs) lm n ires"
apply(simp only: mopup_left_moving.simps)
apply(erule exE)+
apply(case_tac lnr, auto)
apply(rule_tac x = "Suc rn" in exI, simp)
done

lemma [simp]: 
"\<lbrakk>n < length lm; mopup_left_moving (2 * n + 5, l, []) lm n ires\<rbrakk>
    \<Longrightarrow> mopup_left_moving (2 * n + 5, tl l, [hd l]) lm n ires"
apply(simp only: mopup_left_moving.simps)
apply(erule exE)+
apply(case_tac lnr, auto)
apply(rule_tac x = 1 in exI, simp)
done


lemma [simp]: 
 "mopup_jump_over2 (2 * n + 6, l, Oc # xs) lm n ires \<Longrightarrow> l \<noteq> []"
apply(auto simp: mopup_jump_over2.simps )
done

lemma [simp]: 
"\<lbrakk>n < length lm; mopup_jump_over2 (2 * n + 6, l, Oc # xs) lm n ires\<rbrakk>
 \<Longrightarrow>  mopup_jump_over2 (2 * n + 6, tl l, hd l # Oc # xs) lm n ires"
apply(simp only: mopup_jump_over2.simps)
apply(erule_tac exE)+
apply(simp add:  , erule conjE, erule_tac conjE)
apply(case_tac m1, simp)
apply(rule_tac x = ln in exI, rule_tac x = rn in exI, 
      rule_tac x = 0 in exI, simp)
apply(case_tac ln, simp, simp, simp only: exp_ind[THEN sym], simp)
apply(rule_tac x = ln in exI, rule_tac x = rn in exI, 
      rule_tac x = nat in exI, rule_tac x = "Suc m2" in exI, simp)
done

lemma [simp]: 
 "\<lbrakk>n < length lm; mopup_jump_over2 (2 * n + 6, l, Bk # xs) lm n ires\<rbrakk> 
  \<Longrightarrow> mopup_stop (0, Bk # l, xs) lm n ires"
apply(auto simp: mopup_jump_over2.simps mopup_stop.simps)
apply(simp_all add: tape_of_nat_abv exp_ind[THEN sym])
done

lemma [simp]: "mopup_jump_over2 (2 * n + 6, l, []) lm n ires = False"
apply(simp only: mopup_jump_over2.simps, simp)
done

declare fetch.simps[simp del]
lemma mod_ex2: "(a mod (2::nat) = 0) = (\<exists> q. a = 2 * q)"
by arith

lemma mod_2: "x mod 2  = 0 \<or>  x mod 2 = Suc 0"
by arith

lemma mopup_inv_step:
  "\<lbrakk>n < length lm; mopup_inv (s, l, r) lm n ires\<rbrakk>
  \<Longrightarrow> mopup_inv (step (s, l, r) (mopup_a n @ shift mopup_b (2 * n), 0)) lm n ires"
apply(case_tac r, case_tac [2] a)
apply(auto split:if_splits simp add:step.simps)
apply(simp_all add: mopupfetchs)
apply(drule_tac mopup_false2, simp_all)
apply(drule_tac mopup_false2, simp_all)
by (metis Suc_n_not_n mod2_Suc_Suc mod_ex1 mod_mult_self1_is_0)

declare mopup_inv.simps[simp del]
lemma mopup_inv_steps: 
"\<lbrakk>n < length lm; mopup_inv (s, l, r) lm n ires\<rbrakk> \<Longrightarrow> 
     mopup_inv (steps (s, l, r) (mopup_a n @ shift mopup_b (2 * n), 0)  stp) lm n ires"
apply(induct_tac stp, simp add: steps.simps)
apply(simp add: step_red)
apply(case_tac "steps (s, l, r) 
                (mopup_a n @ shift mopup_b (2 * n), 0) na", simp)
apply(rule_tac mopup_inv_step, simp, simp)
done

fun abc_mopup_stage1 :: "config \<Rightarrow> nat \<Rightarrow> nat"
  where
  "abc_mopup_stage1 (s, l, r) n = 
           (if s > 0 \<and> s \<le> 2*n then 6
            else if s = 2*n + 1 then 4
            else if s \<ge> 2*n + 2 \<and> s \<le> 2*n + 4 then 3
            else if s = 2*n + 5 then 2
            else if s = 2*n + 6 then 1
            else 0)"

fun abc_mopup_stage2 :: "config \<Rightarrow> nat \<Rightarrow> nat"
  where
  "abc_mopup_stage2 (s, l, r) n = 
           (if s > 0 \<and> s \<le> 2*n then length r
            else if s = 2*n + 1 then length r
            else if s = 2*n + 5 then length l
            else if s = 2*n + 6 then length l
            else if s \<ge> 2*n + 2 \<and> s \<le> 2*n + 4 then length r
            else 0)"

fun abc_mopup_stage3 :: "config \<Rightarrow> nat \<Rightarrow> nat"
  where
  "abc_mopup_stage3 (s, l, r) n = 
          (if s > 0 \<and> s \<le> 2*n then 
              if hd r = Bk then 0
              else 1
           else if s = 2*n + 2 then 1 
           else if s = 2*n + 3 then 0
           else if s = 2*n + 4 then 2
           else 0)"

definition
  "abc_mopup_measure = measures [\<lambda>(c, n). abc_mopup_stage1 c n, 
                                 \<lambda>(c, n). abc_mopup_stage2 c n, 
                                 \<lambda>(c, n). abc_mopup_stage3 c n]"

lemma wf_abc_mopup_measure:
  shows "wf abc_mopup_measure" 
unfolding abc_mopup_measure_def 
by auto

lemma abc_mopup_measure_induct [case_names Step]: 
  "\<lbrakk>\<And>n. \<not> P (f n) \<Longrightarrow> (f (Suc n), (f n)) \<in> abc_mopup_measure\<rbrakk> \<Longrightarrow> \<exists>n. P (f n)"
using wf_abc_mopup_measure
by (metis wf_iff_no_infinite_down_chain)

lemma [simp]: "mopup_bef_erase_a (a, aa, []) lm n ires = False"
apply(auto simp: mopup_bef_erase_a.simps)
done

lemma [simp]: "mopup_bef_erase_b (a, aa, []) lm n ires = False"
apply(auto simp: mopup_bef_erase_b.simps) 
done

lemma [simp]: "mopup_aft_erase_b (2 * n + 3, aa, []) lm n ires = False"
apply(auto simp: mopup_aft_erase_b.simps)
done

declare mopup_inv.simps[simp del]

lemma [simp]: 
  "\<lbrakk>0 < q; q \<le> n\<rbrakk> \<Longrightarrow> 
     (fetch (mopup_a n @ shift mopup_b (2 * n)) (2*q) Bk) = (R, 2*q - 1)"
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 [simp]: "(a mod 2 \<noteq> Suc 0) = (a mod 2 = 0)  "
by arith

lemma mopup_halt:
  assumes 
  less: "n < length lm"
  and inv: "mopup_inv (Suc 0, l, r) lm n ires"
  and f: "f = (\<lambda> stp. (steps (Suc 0, l, r) (mopup_a n @ shift mopup_b (2 * n), 0) stp, n))"
  and P: "P = (\<lambda> (c, n). is_final c)"
  shows "\<exists> stp. P (f stp)"
proof (induct rule: abc_mopup_measure_induct) 
  case (Step na)
  have h: "\<not> P (f na)" by fact
  show "(f (Suc na), f na) \<in> abc_mopup_measure"
  proof(simp add: f)
    obtain a b c where g:"steps (Suc 0, l, r) (mopup_a n @ shift mopup_b (2 * n), 0) na = (a, b, c)"
      apply(case_tac "steps (Suc 0, l, r) (mopup_a n @ shift mopup_b (2 * n), 0) na", auto)
      done
    then have "mopup_inv (a, b, c) lm n ires"
      using inv less mopup_inv_steps[of n lm "Suc 0" l r ires na]
      apply(simp)
      done
    moreover have "a > 0"
      using h g
      apply(simp add: f P)
      done
    ultimately 
    have "((step (a, b, c) (mopup_a n @ shift mopup_b (2 * n), 0), n), (a, b, c), n) \<in> abc_mopup_measure"
      apply(case_tac c, case_tac [2] aa)
      apply(auto split:if_splits simp add:step.simps mopup_inv.simps)
      apply(simp_all add: mopupfetchs abc_mopup_measure_def)
      done
    thus "((step (steps (Suc 0, l, r) (mopup_a n @ shift mopup_b (2 * n), 0) na) 
      (mopup_a n @ shift mopup_b (2 * n), 0), n),
      steps (Suc 0, l, r) (mopup_a n @ shift mopup_b (2 * n), 0) na, n)
      \<in> abc_mopup_measure"
      using g by simp
  qed
qed

lemma mopup_inv_start: 
  "n < length am \<Longrightarrow> mopup_inv (Suc 0, Bk # Bk # ires, <am> @ Bk \<up> k) am n ires"
apply(auto simp: mopup_inv.simps mopup_bef_erase_a.simps mopup_jump_over1.simps)
apply(case_tac [!] am, auto split: if_splits simp: tape_of_nl_cons)
apply(rule_tac x = "Suc a" in exI, rule_tac x = k in exI, simp)
apply(case_tac [!] n, auto)
apply(case_tac k, auto)
done
      
lemma mopup_correct:
  assumes less: "n < length (am::nat list)"
  and rs: "am ! n = rs"
  shows "\<exists> stp i j. (steps (Suc 0, Bk # Bk # ires, <am> @ Bk \<up> k) (mopup_a n @ shift mopup_b (2 * n), 0) stp)
    = (0, Bk\<up>i @ Bk # Bk # ires, Oc # Oc\<up> rs @ Bk\<up>j)"
using less
proof -
  have a: "mopup_inv (Suc 0, Bk # Bk # ires, <am> @ Bk \<up> k) am n ires"
    using less
    apply(simp add: mopup_inv_start)
    done    
  then have "\<exists> stp. is_final (steps (Suc 0, Bk # Bk # ires, <am> @ Bk \<up> k) (mopup_a n @ shift mopup_b (2 * n), 0) stp)"
    using less mopup_halt[of n am  "Bk # Bk # ires" "<am> @ Bk \<up> k" ires
      "(\<lambda>stp. (steps (Suc 0, Bk # Bk # ires, <am> @ Bk \<up> k) (mopup_a n @ shift mopup_b (2 * n), 0) stp, n))"
      "(\<lambda>(c, n). is_final c)"]
    apply(simp)
    done
  from this obtain stp where b:
    "is_final (steps (Suc 0, Bk # Bk # ires, <am> @ Bk \<up> k) (mopup_a n @ shift mopup_b (2 * n), 0) stp)" ..
  from a b have
    "mopup_inv (steps (Suc 0, Bk # Bk # ires, <am> @ Bk \<up> k) (mopup_a n @ shift mopup_b (2 * n), 0) stp)
    am n ires"
    apply(rule_tac mopup_inv_steps, simp_all add: less)
    done    
  from b and this show "?thesis"
    apply(rule_tac x = stp in exI, simp)
    apply(case_tac "steps (Suc 0, Bk # Bk # ires, <am> @ Bk \<up> k) 
      (mopup_a n @ shift mopup_b (2 * n), 0) stp")
    apply(simp add: mopup_inv.simps mopup_stop.simps rs)
    using rs
    apply(simp add: tape_of_nat_abv)
    done
qed

lemma wf_mopup[intro]: "tm_wf (mopup n, 0)"
apply(induct n, simp add: mopup.simps shift.simps mopup_b_def tm_wf.simps)
apply(auto simp: mopup.simps shift.simps mopup_b_def tm_wf.simps)
done

end