--- a/README Fri Feb 15 07:42:47 2013 +0000
+++ b/README Fri Feb 15 14:05:26 2013 +0000
@@ -6,6 +6,8 @@
Turing.thy: Basic definitions of Turing machines.
Turing_Hoare.thy: Contains the Hoare rules
Uncomputable.thy: The existence of Turing uncomputable functions
+ Abacus_Mopup.thy: Mopup TM which is used when compiling Abacus
+ programs
Abacus.thy: Basic definitions of abacus machines (an intermediate
"language" for compiling recursive functions into
Turing machines)
--- a/ROOT.ML Fri Feb 15 07:42:47 2013 +0000
+++ b/ROOT.ML Fri Feb 15 14:05:26 2013 +0000
@@ -3,6 +3,7 @@
use_thys ["thys/Turing",
"thys/Turing_Hoare",
"thys/Uncomputable",
+ "thys/Abacus_Mopup",
"thys/Abacus",
"thys/Rec_Def",
"thys/Recursive",
Binary file paper.pdf has changed
--- a/thys/Abacus.thy Fri Feb 15 07:42:47 2013 +0000
+++ b/thys/Abacus.thy Fri Feb 15 14:05:26 2013 +0000
@@ -1,5 +1,11 @@
+(* Title: thys/Abacus.thy
+ Author: Jian Xu, Xingyuan Zhang, and Christian Urban
+*)
+
+header {* Abacus Machines *}
+
theory Abacus
-imports Uncomputable
+imports Turing_Hoare Abacus_Mopup
begin
declare replicate_Suc[simp add]
@@ -603,6 +609,7 @@
done
qed
+declare fetch.simps[simp]
lemma append_append_fetch:
"\<lbrakk>length tp1 mod 2 = 0; length tp mod 2 = 0;
length tp1 div 2 < a \<and> a \<le> length tp1 div 2 + length tp div 2\<rbrakk>
@@ -1248,12 +1255,6 @@
apply(erule disj_forward, auto)
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 locate_a_2_locate_a[simp]: "inv_locate_a (as, am) (q, aaa, Bk # xs) ires
\<Longrightarrow> inv_locate_a (as, am) (q, aaa, Oc # xs) ires"
apply(simp only: inv_locate_a.simps at_begin_norm.simps
@@ -2019,6 +2020,9 @@
apply(auto simp: inv_check_left_moving.simps inv_check_left_moving_in_middle.simps split: if_splits)
done
+lemma numeral_4_eq_4: "4 = Suc (Suc (Suc (Suc 0)))"
+by arith
+
lemma tinc_correct_pre:
assumes layout: "ly = layout_of ap"
and inv_start: "inv_locate_a (as, lm) (n, l, r) ires"
@@ -2049,14 +2053,13 @@
apply(simp add:Q)
apply(simp add: inc_inv.simps)
apply(case_tac c, case_tac [2] aa)
- apply(auto simp: Let_def step.simps tinc_b_def numeral_2_eq_2 numeral_3_eq_3 split: if_splits)
- apply(simp_all add: inc_inv.simps inc_LE_def lex_triple_def lex_pair_def inc_measure_def numeral_5_eq_5
- numeral_6_eq_6 numeral_7_eq_7 numeral_8_eq_8 numeral_9_eq_9)
+ apply(auto simp: Let_def step.simps tinc_b_def split: if_splits)
+ apply(simp_all add: inc_inv.simps inc_LE_def lex_triple_def lex_pair_def inc_measure_def numeral_5_eq_5 numeral_2_eq_2 numeral_3_eq_3
+ numeral_4_eq_4 numeral_6_eq_6 numeral_7_eq_7 numeral_8_eq_8 numeral_9_eq_9)
done
qed
qed
-
lemma tinc_correct:
assumes layout: "ly = layout_of ap"
and inv_start: "inv_locate_a (as, lm) (n, l, r) ires"
@@ -3756,817 +3759,6 @@
apply(simp_all add: start_of.simps fetch.simps nth_append)
done
-(********for mopup***********)
-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 = <abc_lm_v 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 (abc_lm_v 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 (abc_lm_v 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 (abc_lm_v 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 (abc_lm_v 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 (abc_lm_v 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 (abc_lm_v 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)
-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 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> abc_lm_v (a # list) (Suc q) @ Bk # <drop (Suc q) list> @ Bk \<up> rn\<rbrakk>
- \<Longrightarrow> <drop q list> = Oc # Oc \<up> abc_lm_v (a # list) (Suc 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 add: abc_lm_v.simps)
-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)
-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> abc_lm_v (a # list) (Suc 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)
-apply(rule_tac drop_tape_of_cons, simp_all add: abc_lm_v.simps)
-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 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 add: abc_lm_v.simps)
-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 (abc_lm_v lm (Suc (s div 2)))" in exI,
- rule_tac x = rn in exI, auto simp: mod_ex1)
-apply(rule_tac drop_tape_of_cons)
-apply arith
-apply(simp add: abc_lm_v.simps)
-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)
-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 (abc_lm_v lm n)" in exI,
- rule_tac x = 0 in exI, simp add: )
-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 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_all)
-apply(rule_tac x = rn in exI, rule_tac x = "list" in exI, simp)
-apply(rule_tac x = rn in exI)
-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, simp, simp add: tape_of_nl_cons split: if_splits)
-apply(auto)
-apply(case_tac ml, simp_all add: tape_of_nl_cons split: if_splits)
-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, simp)
-apply(rule_tac x = 1 in exI, simp)
-apply(case_tac ml, simp, simp)
-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)
-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)
-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 [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 "abc_lm_v 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], simp)
-apply(case_tac "abc_lm_v lm n", simp)
-apply(case_tac lnl, simp, simp)
-apply(rule_tac x = lnl in exI, rule_tac x = rn in exI)
-apply(rule_tac x = nat in exI, rule_tac x = "Suc (Suc 0)" in exI, simp)
-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, simp)
-apply(rule_tac x = lnl in exI, rule_tac x = nat in exI, simp)
-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)
-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
-
-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)
-done
-
-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 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 lex_triple_def lex_pair_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, simp_all add: abc_lm_v.simps)
-apply(case_tac k, simp, simp_all)
-done
-
-lemma mopup_correct:
- assumes less: "n < length (am::nat list)"
- and rs: "abc_lm_v 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
-
-(*we can use Hoare_plus here*)
-
-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
-
lemma length_tp:
"\<lbrakk>ly = layout_of ap; tp = tm_of ap\<rbrakk> \<Longrightarrow>
start_of ly (length ap) = Suc (length tp div 2)"
@@ -4595,7 +3787,7 @@
have "\<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 assms
- by(auto intro: mopup_correct)
+ by(rule_tac mopup_correct, auto simp: abc_lm_v.simps)
then obtain stpb i j where
"steps (Suc 0, Bk # Bk # ires, <am> @ Bk \<up> k) (mopup_a n @ shift mopup_b (2 * n), 0) stpb
= (0, Bk\<up>i @ Bk # Bk # ires, Oc # Oc\<up> rs @ Bk\<up>j)" by blast
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/thys/Abacus_Mopup.thy Fri Feb 15 14:05:26 2013 +0000
@@ -0,0 +1,868 @@
+(* 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 [simp]: "(a mod 2 \<noteq> Suc 0) = (a mod 2 = 0) "
+by arith
+
+lemma [simp]: "(a mod 2 \<noteq> 0) = (a mod 2 = Suc 0) "
+by arith
+
+
+lemma [simp]: "(2*q - Suc 0) div 2 = (q - 1)"
+by arith
+
+lemma [simp]: "(Suc (2*q)) div 2 = q"
+by arith
+*)
+lemma mod_2: "x mod 2 = 0 \<or> x mod 2 = Suc 0"
+by arith
+
+lemma 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
+
+(*we can use Hoare_plus here*)
+
+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
\ No newline at end of file