Session Universal_Turing_Machine

Theory Turing

(* Title: thys/Turing.thy
   Author: Jian Xu, Xingyuan Zhang, and Christian Urban
   Modifications: Sebastiaan Joosten
*)

chapter ‹Turing Machines›

theory Turing
  imports Main
begin

section ‹Basic definitions of Turing machine›

datatype action = W0 | W1 | L | R | Nop

datatype cell = Bk | Oc

type_synonym tape = "cell list × cell list"

type_synonym state = nat

type_synonym instr = "action × state"

type_synonym tprog = "instr list × nat"

type_synonym tprog0 = "instr list"

type_synonym config = "state × tape"

fun nth_of where
  "nth_of xs i = (if i  length xs then None else Some (xs ! i))"

lemma nth_of_map [simp]:
  shows "nth_of (map f p) n = (case (nth_of p n) of None  None | Some x  Some (f x))"
  by simp

fun 
  fetch :: "instr list  state  cell  instr"
  where
    "fetch p 0 b = (Nop, 0)"
  | "fetch p (Suc s) Bk = 
     (case nth_of p (2 * s) of
        Some i  i
      | None  (Nop, 0))"
  |"fetch p (Suc s) Oc = 
     (case nth_of p ((2 * s) + 1) of
         Some i  i
       | None  (Nop, 0))"

lemma fetch_Nil [simp]:
  shows "fetch [] s b = (Nop, 0)"
  by (cases s,force) (cases b;force)

fun 
  update :: "action  tape  tape"
  where 
    "update W0 (l, r) = (l, Bk # (tl r))" 
  | "update W1 (l, r) = (l, Oc # (tl r))"
  | "update L (l, r) = (if l = [] then ([], Bk # r) else (tl l, (hd l) # r))" 
  | "update R (l, r) = (if r = [] then (Bk # l, []) else ((hd r) # l, tl r))" 
  | "update Nop (l, r) = (l, r)"

abbreviation 
  "read r == if (r = []) then Bk else hd r"

fun step :: "config  tprog  config"
  where 
    "step (s, l, r) (p, off) = 
     (let (a, s') = fetch p (s - off) (read r) in (s', update a (l, r)))"

abbreviation
  "step0 c p  step c (p, 0)"

fun steps :: "config  tprog  nat  config"
  where
    "steps c p 0 = c" |
    "steps c p (Suc n) = steps (step c p) p n"

abbreviation
  "steps0 c p n  steps c (p, 0) n"

lemma step_red [simp]: 
  shows "steps c p (Suc n) = step (steps c p n) p"
  by (induct n arbitrary: c) (auto)

lemma steps_add [simp]: 
  shows "steps c p (m + n) = steps (steps c p m) p n"
  by (induct m arbitrary: c) (auto)

lemma step_0 [simp]: 
  shows "step (0, (l, r)) p = (0, (l, r))"
  by (cases p, simp)

lemma steps_0 [simp]: 
  shows "steps (0, (l, r)) p n = (0, (l, r))"
  by (induct n) (simp_all)

fun
  is_final :: "config  bool"
  where
    "is_final (s, l, r) = (s = 0)"

lemma is_final_eq: 
  shows "is_final (s, tp) = (s = 0)"
  by (cases tp) (auto)

lemma is_finalI [intro]:
  shows "is_final (0, tp)"
  by (simp add: is_final_eq)

lemma after_is_final:
  assumes "is_final c"
  shows "is_final (steps c p n)"
  using assms 
  by(induct n;cases c;auto)

lemma is_final:
  assumes a: "is_final (steps c p n1)"
    and b: "n1  n2"
  shows "is_final (steps c p n2)"
proof - 
  obtain n3 where eq: "n2 = n1 + n3" using b by (metis le_iff_add)
  from a show "is_final (steps c p n2)" unfolding eq
    by (simp add: after_is_final)
qed

lemma not_is_final:
  assumes a: "¬ is_final (steps c p n1)"
    and b: "n2  n1"
  shows "¬ is_final (steps c p n2)"
proof (rule notI)
  obtain n3 where eq: "n1 = n2 + n3" using b by (metis le_iff_add)
  assume "is_final (steps c p n2)"
  then have "is_final (steps c p n1)" unfolding eq
    by (simp add: after_is_final)
  with a show "False" by simp
qed

(* if the machine is in the halting state, there must have 
   been a state just before the halting state *)
lemma before_final: 
  assumes "steps0 (1, tp) A n = (0, tp')"
  shows " n'. ¬ is_final (steps0 (1, tp) A n')  steps0 (1, tp) A (Suc n') = (0, tp')"
  using assms
proof(induct n arbitrary: tp')
  case (0 tp')
  have asm: "steps0 (1, tp) A 0 = (0, tp')" by fact
  then show "n'. ¬ is_final (steps0 (1, tp) A n')  steps0 (1, tp) A (Suc n') = (0, tp')"
    by simp
next
  case (Suc n tp')
  have ih: "tp'. steps0 (1, tp) A n = (0, tp') 
    n'. ¬ is_final (steps0 (1, tp) A n')  steps0 (1, tp) A (Suc n') = (0, tp')" by fact
  have asm: "steps0 (1, tp) A (Suc n) = (0, tp')" by fact
  obtain s l r where cases: "steps0 (1, tp) A n = (s, l, r)"
    by (auto intro: is_final.cases)
  then show "n'. ¬ is_final (steps0 (1, tp) A n')  steps0 (1, tp) A (Suc n') = (0, tp')"
  proof (cases "s = 0")
    case True (* in halting state *)
    then have "steps0 (1, tp) A n = (0, tp')"
      using asm cases by (simp del: steps.simps)
    then show ?thesis using ih by simp
  next
    case False (* not in halting state *)
    then have "¬ is_final (steps0 (1, tp) A n)  steps0 (1, tp) A (Suc n) = (0, tp')"
      using asm cases by simp
    then show ?thesis by auto
  qed
qed

lemma least_steps: 
  assumes "steps0 (1, tp) A n = (0, tp')"
  shows " n'. (n'' < n'. ¬ is_final (steps0 (1, tp) A n''))  
               (n''  n'. is_final (steps0 (1, tp) A n''))"
proof -
  from before_final[OF assms] 
  obtain n' where
    before: "¬ is_final (steps0 (1, tp) A n')" and
    final: "steps0 (1, tp) A (Suc n') = (0, tp')" by auto
  from before
  have "n'' < Suc n'. ¬ is_final (steps0 (1, tp) A n'')"
    using not_is_final by auto
  moreover
  from final 
  have "n''  Suc n'. is_final (steps0 (1, tp) A n'')" 
    using is_final[of _ _ "Suc n'"] by (auto simp add: is_final_eq)
  ultimately
  show " n'. (n'' < n'. ¬ is_final (steps0 (1, tp) A n''))  (n''  n'. is_final (steps0 (1, tp) A n''))"
    by blast
qed



(* well-formedness of Turing machine programs *)
abbreviation "is_even n  (n::nat) mod 2 = 0"

fun 
  tm_wf :: "tprog  bool"
  where
    "tm_wf (p, off) = (length p  2  is_even (length p)  
                    ((a, s)  set p. s  length p div 2 + off  s  off))"

abbreviation
  "tm_wf0 p  tm_wf (p, 0)"

abbreviation exponent :: "'a  nat  'a list" ("_  _" [100, 99] 100)
  where "x  n == replicate n x"

lemma hd_repeat_cases:
  "P (hd (a  m @ r))  (m = 0  P (hd r))  (nat. m = Suc nat  P a)"
  by (cases m,auto)

class tape =
  fixes tape_of :: "'a  cell list" ("<_>" 100)


instantiation nat::tape begin
definition tape_of_nat where "tape_of_nat (n::nat)  Oc  (Suc n)"
instance by standard
end

type_synonym nat_list = "nat list"

instantiation list::(tape) tape begin
fun tape_of_nat_list :: "('a::tape) list  cell list" 
  where 
    "tape_of_nat_list [] = []" |
    "tape_of_nat_list [n] = <n>" |
    "tape_of_nat_list (n#ns) = <n> @ Bk # (tape_of_nat_list ns)"
definition tape_of_list where "tape_of_list  tape_of_nat_list"
instance by standard
end

instantiation prod:: (tape, tape) tape begin
fun tape_of_nat_prod :: "('a::tape) × ('b::tape)  cell list" 
  where "tape_of_nat_prod (n, m) = <n> @ [Bk] @ <m>" 
definition tape_of_prod where "tape_of_prod  tape_of_nat_prod"
instance by standard
end

fun 
  shift :: "instr list  nat  instr list"
  where
    "shift p n = (map (λ (a, s). (a, (if s = 0 then 0 else s + n))) p)"

fun 
  adjust :: "instr list  nat  instr list"
  where
    "adjust p e = map (λ (a, s). (a, if s = 0 then e else s)) p"

abbreviation
  "adjust0 p  adjust p (Suc (length p div 2))"

lemma length_shift [simp]: 
  shows "length (shift p n) = length p"
  by simp

lemma length_adjust [simp]: 
  shows "length (adjust p n) = length p"
  by (induct p) (auto)


(* composition of two Turing machines *)
fun
  tm_comp :: "instr list  instr list  instr list" ("_ |+| _" [0, 0] 100)
  where
    "tm_comp p1 p2 = ((adjust0 p1) @ (shift p2 (length p1 div 2)))"

lemma tm_comp_length:
  shows "length (A |+| B) = length A + length B"
  by auto

lemma tm_comp_wf[intro]: 
  "tm_wf (A, 0); tm_wf (B, 0)  tm_wf (A |+| B, 0)"
  by (fastforce)

lemma tm_comp_step: 
  assumes unfinal: "¬ is_final (step0 c A)"
  shows "step0 c (A |+| B) = step0 c A"
proof -
  obtain s l r where eq: "c = (s, l, r)" by (metis is_final.cases) 
  have "¬ is_final (step0 (s, l, r) A)" using unfinal eq by simp
  then have "case (fetch A s (read r)) of (a, s)  s  0"
    by (auto simp add: is_final_eq)
  then have "fetch (A |+| B) s (read r) = fetch A s (read r)"
    apply (cases "read r";cases s)
    by (auto simp: tm_comp_length nth_append)
  then show "step0 c (A |+| B) = step0 c A" by (simp add: eq) 
qed

lemma tm_comp_steps:  
  assumes "¬ is_final (steps0 c A n)" 
  shows "steps0 c (A |+| B) n = steps0 c A n"
  using assms
proof(induct n)
  case 0
  then show "steps0 c (A |+| B) 0 = steps0 c A 0" by auto
next 
  case (Suc n)
  have ih: "¬ is_final (steps0 c A n)  steps0 c (A |+| B) n = steps0 c A n" by fact
  have fin: "¬ is_final (steps0 c A (Suc n))" by fact
  then have fin1: "¬ is_final (step0 (steps0 c A n) A)" 
    by (auto simp only: step_red)
  then have fin2: "¬ is_final (steps0 c A n)"
    by (metis is_final_eq step_0 surj_pair) 

  have "steps0 c (A |+| B) (Suc n) = step0 (steps0 c (A |+| B) n) (A |+| B)" 
    by (simp only: step_red)
  also have "... = step0 (steps0 c A n) (A |+| B)" by (simp only: ih[OF fin2])
  also have "... = step0 (steps0 c A n) A" by (simp only: tm_comp_step[OF fin1])
  finally show "steps0 c (A |+| B) (Suc n) = steps0 c A (Suc n)"
    by (simp only: step_red)
qed

lemma tm_comp_fetch_in_A:
  assumes h1: "fetch A s x = (a, 0)"
    and h2: "s  length A div 2" 
    and h3: "s  0"
  shows "fetch (A |+| B) s x = (a, Suc (length A div 2))"
  using h1 h2 h3
  apply(cases s;cases x)
  by(auto simp: tm_comp_length nth_append)

lemma tm_comp_exec_after_first:
  assumes h1: "¬ is_final c" 
    and h2: "step0 c A = (0, tp)"
    and h3: "fst c  length A div 2"
  shows "step0 c (A |+| B) = (Suc (length A div 2), tp)"
  using h1 h2 h3
  apply(case_tac c)
  apply(auto simp del: tm_comp.simps)
   apply(case_tac "fetch A a Bk")
   apply(simp del: tm_comp.simps)
   apply(subst tm_comp_fetch_in_A;force)
  apply(case_tac "fetch A a (hd ca)")
  apply(simp del: tm_comp.simps)
  apply(subst tm_comp_fetch_in_A)
     apply(auto)[4]
  done

lemma step_in_range: 
  assumes h1: "¬ is_final (step0 c A)"
    and h2: "tm_wf (A, 0)"
  shows "fst (step0 c A)  length A div 2"
  using h1 h2
  apply(cases c;cases "fst c";cases "hd (snd (snd c))")
  by(auto simp add: Let_def case_prod_beta')

lemma steps_in_range: 
  assumes h1: "¬ is_final (steps0 (1, tp) A stp)"
    and h2: "tm_wf (A, 0)"
  shows "fst (steps0 (1, tp) A stp)  length A div 2"
  using h1
proof(induct stp)
  case 0
  then show "fst (steps0 (1, tp) A 0)  length A div 2" using h2
    by (auto)
next
  case (Suc stp)
  have ih: "¬ is_final (steps0 (1, tp) A stp)  fst (steps0 (1, tp) A stp)  length A div 2" by fact
  have h: "¬ is_final (steps0 (1, tp) A (Suc stp))" by fact
  from ih h h2 show "fst (steps0 (1, tp) A (Suc stp))  length A div 2"
    by (metis step_in_range step_red)
qed

(* if A goes into the final state, then A |+| B will go into the first state of B *)
lemma tm_comp_next: 
  assumes a_ht: "steps0 (1, tp) A n = (0, tp')"
    and a_wf: "tm_wf (A, 0)"
  obtains n' where "steps0 (1, tp) (A |+| B) n' = (Suc (length A div 2), tp')"
proof -
  assume a: "n. steps (1, tp) (A |+| B, 0) n = (Suc (length A div 2), tp')  thesis"
  obtain stp' where fin: "¬ is_final (steps0 (1, tp) A stp')" and h: "steps0 (1, tp) A (Suc stp') = (0, tp')"
    using before_final[OF a_ht] by blast
  from fin have h1:"steps0 (1, tp) (A |+| B) stp' = steps0 (1, tp) A stp'"
    by (rule tm_comp_steps)
  from h have h2: "step0 (steps0 (1, tp) A stp') A = (0, tp')"
    by (simp only: step_red)

  have "steps0 (1, tp) (A |+| B) (Suc stp') = step0 (steps0 (1, tp) (A |+| B) stp') (A |+| B)" 
    by (simp only: step_red)
  also have "... = step0 (steps0 (1, tp) A stp') (A |+| B)" using h1 by simp
  also have "... = (Suc (length A div 2), tp')" 
    by (rule tm_comp_exec_after_first[OF fin h2 steps_in_range[OF fin a_wf]])
  finally show thesis using a by blast
qed

lemma tm_comp_fetch_second_zero:
  assumes h1: "fetch B s x = (a, 0)"
    and hs: "tm_wf (A, 0)" "s  0"
  shows "fetch (A |+| B) (s + (length A div 2)) x = (a, 0)"
  using h1 hs
  by(cases x; cases s; fastforce simp: tm_comp_length nth_append)

lemma tm_comp_fetch_second_inst:
  assumes h1: "fetch B sa x = (a, s)"
    and hs: "tm_wf (A, 0)" "sa  0" "s  0"
  shows "fetch (A |+| B) (sa + length A div 2) x = (a, s + length A div 2)"
  using h1 hs
  by(cases x; cases sa; fastforce simp: tm_comp_length nth_append)


lemma tm_comp_second:
  assumes a_wf: "tm_wf (A, 0)"
    and steps: "steps0 (1, l, r) B stp = (s', l', r')"
  shows "steps0 (Suc (length A div 2), l, r)  (A |+| B) stp 
    = (if s' = 0 then 0 else s' + length A div 2, l', r')"
  using steps
proof(induct stp arbitrary: s' l' r')
  case 0
  then show ?case by simp
next
  case (Suc stp s' l' r')
  obtain s'' l'' r'' where a: "steps0 (1, l, r) B stp = (s'', l'', r'')"
    by (metis is_final.cases)
  then have ih1: "s'' = 0  steps0 (Suc (length A div 2), l, r) (A |+| B) stp = (0, l'', r'')"
    and ih2: "s''  0  steps0 (Suc (length A div 2), l, r) (A |+| B) stp = (s'' + length A div 2, l'', r'')"
    using Suc by (auto)
  have h: "steps0 (1, l, r) B (Suc stp) = (s', l', r')" by fact

  { assume "s'' = 0"
    then have ?case using a h ih1 by (simp del: steps.simps) 
  } moreover
  { assume as: "s''  0" "s' = 0"
    from as a h 
    have "step0 (s'', l'', r'') B = (0, l', r')" by (simp del: steps.simps)
    with as have ?case
      apply(cases "fetch B s'' (read r'')")
      by (auto simp add: tm_comp_fetch_second_zero[OF _ a_wf] ih2[OF as(1)]
          simp del: tm_comp.simps steps.simps)
  } moreover
  { assume as: "s''  0" "s'  0"
    from as a h
    have "step0 (s'', l'', r'') B = (s', l', r')" by (simp del: steps.simps)
    with as have ?case
      apply(simp add: ih2[OF as(1)] del: tm_comp.simps steps.simps)
      apply(case_tac "fetch B s'' (read r'')")
      apply(auto simp add: tm_comp_fetch_second_inst[OF _ a_wf as] simp del: tm_comp.simps)
      done
  }
  ultimately show ?case by blast
qed


lemma tm_comp_final:
  assumes "tm_wf (A, 0)"  
    and "steps0 (1, l, r) B stp = (0, l', r')"
  shows "steps0 (Suc (length A div 2), l, r)  (A |+| B) stp = (0, l', r')"
  using tm_comp_second[OF assms] by (simp)

end

Theory Turing_Hoare

(* Title: thys/Turing_Hoare.thy
   Author: Jian Xu, Xingyuan Zhang, and Christian Urban
   Modifications: Sebastiaan Joosten
*)

chapter ‹Hoare Rules for TMs›

theory Turing_Hoare
  imports Turing
begin


type_synonym assert = "tape  bool"

definition 
  assert_imp :: "assert  assert  bool" ("_  _" [0, 0] 100)
  where
    "P  Q  l r. P (l, r)  Q (l, r)"

lemma refl_assert[intro, simp]:
  "P  P"
  unfolding assert_imp_def by simp

fun 
  holds_for :: "(tape  bool)  config  bool" ("_ holds'_for _" [100, 99] 100)
  where
    "P holds_for (s, l, r) = P (l, r)"  

lemma is_final_holds[simp]:
  assumes "is_final c"
  shows "Q holds_for (steps c p n) = Q holds_for c"
  using assms 
  by(induct n;cases c,auto)

(* Hoare Rules *)

(* halting case *)
definition
  Hoare_halt :: "assert  tprog0  assert  bool" ("({(1_)}/ (_)/ {(1_)})" 50)
  where
    "{P} p {Q}  (tp. P tp  (n. is_final (steps0 (1, tp) p n)  Q holds_for (steps0 (1, tp) p n)))"

(* not halting case *)
definition
  Hoare_unhalt :: "assert  tprog0  bool" ("({(1_)}/ (_)) " 50)
  where
    "{P} p   tp. P tp  ( n . ¬ (is_final (steps0 (1, tp) p n)))"


lemma Hoare_haltI:
  assumes "l r. P (l, r)  n. is_final (steps0 (1, (l, r)) p n)  Q holds_for (steps0 (1, (l, r)) p n)"
  shows "{P} p {Q}"
  unfolding Hoare_halt_def 
  using assms by auto

lemma Hoare_unhaltI:
  assumes "l r n. P (l, r)  ¬ is_final (steps0 (1, (l, r)) p n)"
  shows "{P} p "
  unfolding Hoare_unhalt_def 
  using assms by auto




text ‹
  {P} A {Q}   {Q} B {S}  A well-formed
  -----------------------------------------
  {P} A |+| B {S}
›


lemma Hoare_plus_halt [case_names A_halt B_halt A_wf]: 
  assumes A_halt : "{P} A {Q}"
    and B_halt : "{Q} B {S}"
    and A_wf : "tm_wf (A, 0)"
  shows "{P} A |+| B {S}"
proof(rule Hoare_haltI)
  fix l r
  assume h: "P (l, r)"
  then obtain n1 l' r' 
    where "is_final (steps0 (1, l, r) A n1)"  
      and a1: "Q holds_for (steps0 (1, l, r) A n1)"
      and a2: "steps0 (1, l, r) A n1 = (0, l', r')"
    using A_halt unfolding Hoare_halt_def
    by (metis is_final_eq surj_pair) 
  then obtain n2 
    where "steps0 (1, l, r) (A |+| B) n2 = (Suc (length A div 2), l', r')"
    using A_wf by (rule_tac tm_comp_next) 
  moreover
  from a1 a2 have "Q (l', r')" by (simp)
  then obtain n3 l'' r''
    where "is_final (steps0 (1, l', r') B n3)" 
      and b1: "S holds_for (steps0 (1, l', r') B n3)"
      and b2: "steps0 (1, l', r') B n3 = (0, l'', r'')"
    using B_halt unfolding Hoare_halt_def 
    by (metis is_final_eq surj_pair) 
  then have "steps0 (Suc (length A div 2), l', r')  (A |+| B) n3 = (0, l'', r'')"
    using A_wf by (rule_tac tm_comp_final) 
  ultimately show 
    "n. is_final (steps0 (1, l, r) (A |+| B) n)  S holds_for (steps0 (1, l, r) (A |+| B) n)"
    using b1 b2 by (rule_tac x = "n2 + n3" in exI) (simp)
qed

text ‹
  {P} A {Q}   {Q} B loops   A well-formed
  ------------------------------------------
          {P} A |+| B  loops
›

lemma Hoare_plus_unhalt [case_names A_halt B_unhalt A_wf]:
  assumes A_halt: "{P} A {Q}"
    and B_uhalt: "{Q} B "
    and A_wf : "tm_wf (A, 0)"
  shows "{P} (A |+| B) "
proof(rule_tac Hoare_unhaltI)
  fix n l r 
  assume h: "P (l, r)"
  then obtain n1 l' r'
    where a: "is_final (steps0 (1, l, r) A n1)" 
      and b: "Q holds_for (steps0 (1, l, r) A n1)"
      and c: "steps0 (1, l, r) A n1 = (0, l', r')"
    using A_halt unfolding Hoare_halt_def 
    by (metis is_final_eq surj_pair) 
  then obtain n2 where eq: "steps0 (1, l, r) (A |+| B) n2 = (Suc (length A div 2), l', r')"
    using A_wf by (rule_tac tm_comp_next)
  then show "¬ is_final (steps0 (1, l, r) (A |+| B) n)"
  proof(cases "n2  n")
    case True
    from b c have "Q (l', r')" by simp
    then have " n. ¬ is_final (steps0 (1, l', r') B n)  "
      using B_uhalt unfolding Hoare_unhalt_def by simp
    then have "¬ is_final (steps0 (1, l', r') B (n - n2))" by auto
    then obtain s'' l'' r'' 
      where "steps0 (1, l', r') B (n - n2) = (s'', l'', r'')" 
        and "¬ is_final (s'', l'', r'')" by (metis surj_pair)
    then have "steps0 (Suc (length A div 2), l', r') (A |+| B) (n - n2) = (s''+ length A div 2, l'', r'')"
      using A_wf by (auto dest: tm_comp_second simp del: tm_wf.simps)
    then have "¬ is_final (steps0 (1, l, r) (A |+| B) (n2 + (n  - n2)))"
      using A_wf by (simp only: steps_add eq) simp
    then show "¬ is_final (steps0 (1, l, r) (A |+| B) n)" 
      using n2  n by simp
  next 
    case False
    then obtain n3 where "n = n2 - n3"
      using diff_le_self le_imp_diff_is_add nat_le_linear
        add.commute by metis
    moreover
    with eq show "¬ is_final (steps0 (1, l, r) (A |+| B) n)"
      by (simp add: not_is_final[where ?n1.0="n2"])
  qed
qed

lemma Hoare_consequence:
  assumes "P'  P" "{P} p {Q}" "Q  Q'"
  shows "{P'} p {Q'}"
  using assms
  unfolding Hoare_halt_def assert_imp_def
  by (metis holds_for.simps surj_pair)



end

Theory Uncomputable

(* Title: thys/Uncomputable.thy
   Author: Jian Xu, Xingyuan Zhang, and Christian Urban
   Modifications: Sebastiaan Joosten
*)

chapter ‹Undeciablity of the Halting Problem›

theory Uncomputable
  imports Turing_Hoare
begin

lemma numeral:
  shows "2 = Suc 1"
    and "3 = Suc 2"
    and "4 = Suc 3" 
    and "5 = Suc 4" 
    and "6 = Suc 5" 
    and "7 = Suc 6"
    and "8 = Suc 7" 
    and "9 = Suc 8" 
    and "10 = Suc 9"
    and "11 = Suc 10"
    and "12 = Suc 11"
  by simp_all

lemma gr1_conv_Suc:"Suc 0 < mr  ( nat. mr = Suc (Suc nat))" by presburger

text ‹The Copying TM, which duplicates its input.›

definition 
  tcopy_begin :: "instr list"
  where
    "tcopy_begin  [(W0, 0), (R, 2), (R, 3), (R, 2),
                 (W1, 3), (L, 4), (L, 4), (L, 0)]"

definition 
  tcopy_loop :: "instr list"
  where
    "tcopy_loop  [(R, 0), (R, 2),  (R, 3), (W0, 2),
                 (R, 3), (R, 4), (W1, 5), (R, 4),
                 (L, 6), (L, 5), (L, 6), (L, 1)]"

definition 
  tcopy_end :: "instr list"
  where
    "tcopy_end  [(L, 0), (R, 2), (W1, 3), (L, 4),
                (R, 2), (R, 2), (L, 5), (W0, 4),
                (R, 0), (L, 5)]"

definition 
  tcopy :: "instr list"
  where
    "tcopy  (tcopy_begin |+| tcopy_loop) |+| tcopy_end"


(* tcopy_begin *)

fun 
  inv_begin0 :: "nat  tape  bool" and
  inv_begin1 :: "nat  tape  bool" and
  inv_begin2 :: "nat  tape  bool" and
  inv_begin3 :: "nat  tape  bool" and
  inv_begin4 :: "nat  tape  bool"
  where
    "inv_begin0 n (l, r) = ((n > 1  (l, r) = (Oc  (n - 2), [Oc, Oc, Bk, Oc]))    
                          (n = 1  (l, r) = ([], [Bk, Oc, Bk, Oc])))"
  | "inv_begin1 n (l, r) = ((l, r) = ([], Oc  n))"
  | "inv_begin2 n (l, r) = ( i j. i > 0  i + j = n  (l, r) = (Oc  i, Oc  j))"
  | "inv_begin3 n (l, r) = (n > 0  (l, tl r) = (Bk # Oc  n, []))"
  | "inv_begin4 n (l, r) = (n > 0  (l, r) = (Oc  n, [Bk, Oc])  (l, r) = (Oc  (n - 1), [Oc, Bk, Oc]))"

fun inv_begin :: "nat  config  bool"
  where
    "inv_begin n (s, tp) = 
        (if s = 0 then inv_begin0 n tp else
         if s = 1 then inv_begin1 n tp else
         if s = 2 then inv_begin2 n tp else
         if s = 3 then inv_begin3 n tp else
         if s = 4 then inv_begin4 n tp 
         else False)"

lemma split_head_repeat[simp]:
  "Oc # list1 = Bk  j @ list2  j = 0  Oc # list1 = list2"
  "Bk # list1 = Oc  j @ list2  j = 0  Bk # list1 = list2"
  "Bk  j @ list2 = Oc # list1  j = 0  Oc # list1 = list2"
  "Oc  j @ list2 = Bk # list1  j = 0  Bk # list1 = list2"
  by(cases j;force)+

lemma inv_begin_step_E: "0 < i; 0 < j  
  ia>0. ia + j - Suc 0 = i + j  Oc # Oc  i = Oc  ia"
  by (rule_tac x = "Suc i" in exI, simp)

lemma inv_begin_step: 
  assumes "inv_begin n cf"
    and "n > 0"
  shows "inv_begin n (step0 cf tcopy_begin)"
  using assms
  unfolding tcopy_begin_def
  apply(cases cf)
  apply(auto simp: numeral split: if_splits elim:inv_begin_step_E)
  apply(cases "hd (snd (snd cf))";cases "(snd (snd cf))",auto)
  done

lemma inv_begin_steps: 
  assumes "inv_begin n cf"
    and "n > 0"
  shows "inv_begin n (steps0 cf tcopy_begin stp)"
  apply(induct stp)
   apply(simp add: assms)
  apply(auto simp del: steps.simps)
  apply(rule_tac inv_begin_step)
   apply(simp_all add: assms)
  done

lemma begin_partial_correctness:
  assumes "is_final (steps0 (1, [], Oc  n) tcopy_begin stp)"
  shows "0 < n  {inv_begin1 n} tcopy_begin {inv_begin0 n}"
proof(rule_tac Hoare_haltI)
  fix l r
  assume h: "0 < n" "inv_begin1 n (l, r)"
  have "inv_begin n (steps0 (1, [], Oc  n) tcopy_begin stp)"
    using h by (rule_tac inv_begin_steps) (simp_all)
  then show
    "stp. is_final (steps0 (1, l, r) tcopy_begin stp)  
    inv_begin0 n holds_for steps (1, l, r) (tcopy_begin, 0) stp"
    using h assms
    apply(rule_tac x = stp in exI)
    apply(case_tac "(steps0 (1, [], Oc  n) tcopy_begin stp)", simp)
    done
qed

fun measure_begin_state :: "config  nat"
  where
    "measure_begin_state (s, l, r) = (if s = 0 then 0 else 5 - s)"

fun measure_begin_step :: "config  nat"
  where
    "measure_begin_step (s, l, r) = 
        (if s = 2 then length r else
         if s = 3 then (if r = []  r = [Bk] then 1 else 0) else
         if s = 4 then length l 
         else 0)"

definition
  "measure_begin = measures [measure_begin_state, measure_begin_step]"

lemma wf_measure_begin:
  shows "wf measure_begin" 
  unfolding measure_begin_def 
  by auto

lemma measure_begin_induct [case_names Step]: 
  "n. ¬ P (f n)  (f (Suc n), (f n))  measure_begin  n. P (f n)"
  using wf_measure_begin
  by (metis wf_iff_no_infinite_down_chain)

lemma begin_halts: 
  assumes h: "x > 0"
  shows " stp. is_final (steps0 (1, [], Oc  x) tcopy_begin stp)"
proof (induct rule: measure_begin_induct) 
  case (Step n)
  have "¬ is_final (steps0 (1, [], Oc  x) tcopy_begin n)" by fact
  moreover
  have "inv_begin x (steps0 (1, [], Oc  x) tcopy_begin n)"
    by (rule_tac inv_begin_steps) (simp_all add:  h)
  moreover
  obtain s l r where eq: "(steps0 (1, [], Oc  x) tcopy_begin n) = (s, l, r)"
    by (metis measure_begin_state.cases)
  ultimately 
  have "(step0 (s, l, r) tcopy_begin, s, l, r)  measure_begin"
    apply(auto simp: measure_begin_def tcopy_begin_def numeral split: if_splits)
    apply(subgoal_tac "r = [Oc]")
     apply(auto)
    by (metis cell.exhaust list.exhaust list.sel(3))
  then 
  show "(steps0 (1, [], Oc  x) tcopy_begin (Suc n), steps0 (1, [], Oc  x) tcopy_begin n)  measure_begin"
    using eq by (simp only: step_red)
qed

lemma begin_correct: 
  shows "0 < n  {inv_begin1 n} tcopy_begin {inv_begin0 n}"
  using begin_partial_correctness begin_halts by blast

declare tm_comp.simps [simp del] 
declare adjust.simps[simp del] 
declare shift.simps[simp del]
declare tm_wf.simps[simp del]
declare step.simps[simp del]
declare steps.simps[simp del]

(* tcopy_loop *)

fun 
  inv_loop1_loop :: "nat  tape  bool" and
  inv_loop1_exit :: "nat  tape  bool" and
  inv_loop5_loop :: "nat  tape  bool" and
  inv_loop5_exit :: "nat  tape  bool" and
  inv_loop6_loop :: "nat  tape  bool" and
  inv_loop6_exit :: "nat  tape  bool"
  where
    "inv_loop1_loop n (l, r) = ( i j. i + j + 1 = n  (l, r) = (Oci, Oc#Oc#Bkj @ Ocj)  j > 0)"
  | "inv_loop1_exit n (l, r) = (0 < n  (l, r) = ([], Bk#Oc#Bkn @ Ocn))"
  | "inv_loop5_loop x (l, r) = 
     ( i j k t. i + j = Suc x  i > 0  j > 0  k + t = j  t > 0  (l, r) = (Ock@Bkj@Oci, Oct))"
  | "inv_loop5_exit x (l, r) = 
     ( i j. i + j = Suc x  i > 0  j > 0  (l, r) = (Bk(j - 1)@Oci, Bk # Ocj))"
  | "inv_loop6_loop x (l, r) = 
     ( i j k t. i + j = Suc x  i > 0  k + t + 1 = j  (l, r) = (Bkk @ Oci, Bk(Suc t) @ Ocj))"
  | "inv_loop6_exit x (l, r) = 
     ( i j. i + j = x  j > 0  (l, r) = (Oci, Oc#Bkj @ Ocj))"

fun 
  inv_loop0 :: "nat  tape  bool" and
  inv_loop1 :: "nat  tape  bool" and
  inv_loop2 :: "nat  tape  bool" and
  inv_loop3 :: "nat  tape  bool" and
  inv_loop4 :: "nat  tape  bool" and
  inv_loop5 :: "nat  tape  bool" and
  inv_loop6 :: "nat  tape  bool"
  where
    "inv_loop0 n (l, r) =  (0 < n  (l, r) = ([Bk], Oc # Bkn @ Ocn))"
  | "inv_loop1 n (l, r) = (inv_loop1_loop n (l, r)  inv_loop1_exit n (l, r))"
  | "inv_loop2 n (l, r) = ( i j any. i + j = n  n > 0  i > 0  j > 0  (l, r) = (Oci, any#Bkj@Ocj))"
  | "inv_loop3 n (l, r) = 
     ( i j k t. i + j = n  i > 0  j > 0   k + t = Suc j  (l, r) = (Bkk@Oci, Bkt@Ocj))"
  | "inv_loop4 n (l, r) = 
     ( i j k t. i + j = n  i > 0  j > 0   k + t = j  (l, r) = (Ock @ Bk(Suc j)@Oci, Oct))"
  | "inv_loop5 n (l, r) = (inv_loop5_loop n (l, r)  inv_loop5_exit n (l, r))"
  | "inv_loop6 n (l, r) = (inv_loop6_loop n (l, r)  inv_loop6_exit n (l, r))"

fun inv_loop :: "nat  config  bool"
  where
    "inv_loop x (s, l, r) = 
         (if s = 0 then inv_loop0 x (l, r)
          else if s = 1 then inv_loop1 x (l, r)
          else if s = 2 then inv_loop2 x (l, r)
          else if s = 3 then inv_loop3 x (l, r)
          else if s = 4 then inv_loop4 x (l, r)
          else if s = 5 then inv_loop5 x (l, r)
          else if s = 6 then inv_loop6 x (l, r)
          else False)"

declare inv_loop.simps[simp del] inv_loop1.simps[simp del]
  inv_loop2.simps[simp del] inv_loop3.simps[simp del] 
  inv_loop4.simps[simp del] inv_loop5.simps[simp del] 
  inv_loop6.simps[simp del]

lemma Bk_no_Oc_repeatE[elim]: "Bk # list = Oc  t  RR"
  by (cases t, auto)

lemma inv_loop3_Bk_empty_via_2[elim]: "0 < x; inv_loop2 x (b, [])  inv_loop3 x (Bk # b, [])"
  by (auto simp: inv_loop2.simps inv_loop3.simps)

lemma inv_loop3_Bk_empty[elim]: "0 < x; inv_loop3 x (b, [])  inv_loop3 x (Bk # b, [])"
  by (auto simp: inv_loop3.simps)

lemma inv_loop5_Oc_empty_via_4[elim]: "0 < x; inv_loop4 x (b, [])  inv_loop5 x (b, [Oc])"
  by(auto simp: inv_loop4.simps inv_loop5.simps;force)

lemma inv_loop1_Bk[elim]: "0 < x; inv_loop1 x (b, Bk # list)  list = Oc # Bk  x @ Oc  x"
  by (auto simp: inv_loop1.simps)

lemma inv_loop3_Bk_via_2[elim]: "0 < x; inv_loop2 x (b, Bk # list)  inv_loop3 x (Bk # b, list)"
  by(auto simp: inv_loop2.simps inv_loop3.simps;force)

lemma inv_loop3_Bk_move[elim]: "0 < x; inv_loop3 x (b, Bk # list)  inv_loop3 x (Bk # b, list)"
  apply(auto simp: inv_loop3.simps)
   apply (rename_tac i j k t)
   apply(rule_tac [!] x = i in exI, 
      rule_tac [!] x = j in exI, simp_all)
   apply(case_tac [!] t, auto)
  done

lemma inv_loop5_Oc_via_4_Bk[elim]: "0 < x; inv_loop4 x (b, Bk # list)  inv_loop5 x (b, Oc # list)"
  by (auto simp: inv_loop4.simps inv_loop5.simps)

lemma inv_loop6_Bk_via_5[elim]: "0 < x; inv_loop5 x ([], Bk # list)  inv_loop6 x ([], Bk # Bk # list)"
  by (auto simp: inv_loop6.simps inv_loop5.simps)

lemma inv_loop5_loop_no_Bk[simp]: "inv_loop5_loop x (b, Bk # list) = False"
  by (auto simp: inv_loop5.simps)

lemma inv_loop6_exit_no_Bk[simp]: "inv_loop6_exit x (b, Bk # list) = False"
  by (auto simp: inv_loop6.simps)

declare inv_loop5_loop.simps[simp del]  inv_loop5_exit.simps[simp del]
  inv_loop6_loop.simps[simp del]  inv_loop6_exit.simps[simp del]

lemma inv_loop6_loopBk_via_5[elim]:"0 < x; inv_loop5_exit x (b, Bk # list); b  []; hd b = Bk 
           inv_loop6_loop x (tl b, Bk # Bk # list)"
  apply(simp only: inv_loop5_exit.simps inv_loop6_loop.simps )
  apply(erule_tac exE)+
  apply(rename_tac i j)
  apply(rule_tac x = i in exI, 
      rule_tac x = j in exI,
      rule_tac x = "j - Suc (Suc 0)" in exI, 
      rule_tac x = "Suc 0" in exI, auto)
   apply(case_tac [!] j, simp_all)
   apply(case_tac [!] "j-1", simp_all)
  done

lemma inv_loop6_loop_no_Oc_Bk[simp]: "inv_loop6_loop x (b, Oc # Bk # list) = False"
  by (auto simp: inv_loop6_loop.simps)

lemma inv_loop6_exit_Oc_Bk_via_5[elim]: "x > 0; inv_loop5_exit x (b, Bk # list); b  []; hd b = Oc  
  inv_loop6_exit x (tl b, Oc # Bk # list)"
  apply(simp only: inv_loop5_exit.simps inv_loop6_exit.simps)
  apply(erule_tac exE)+
  apply(rule_tac x = "x - 1" in exI, rule_tac x = 1 in exI, simp)
  apply(rename_tac i j)
  apply(case_tac j;case_tac "j-1", auto)
  done

lemma inv_loop6_Bk_tail_via_5[elim]: "0 < x; inv_loop5 x (b, Bk # list); b  []  inv_loop6 x (tl b, hd b # Bk # list)"
  apply(simp add: inv_loop5.simps inv_loop6.simps)
  apply(cases "hd b", simp_all, auto)
  done

lemma inv_loop6_loop_Bk_Bk_drop[elim]: "0 < x; inv_loop6_loop x (b, Bk # list); b  []; hd b = Bk
               inv_loop6_loop x (tl b, Bk # Bk # list)"
  apply(simp only: inv_loop6_loop.simps)
  apply(erule_tac exE)+
  apply(rename_tac i j k t)
  apply(rule_tac x = i in exI, rule_tac x = j in exI, 
      rule_tac x = "k - 1" in exI, rule_tac x = "Suc t" in exI, auto)
   apply(case_tac [!] k, auto)
  done

lemma inv_loop6_exit_Oc_Bk_via_loop6[elim]: "0 < x; inv_loop6_loop x (b, Bk # list); b  []; hd b = Oc 
         inv_loop6_exit x (tl b, Oc # Bk # list)"
  apply(simp only: inv_loop6_loop.simps inv_loop6_exit.simps)
  apply(erule_tac exE)+
  apply(rename_tac i j k t)
  apply(rule_tac x = "i - 1" in exI, rule_tac x = j in exI, auto)
   apply(case_tac [!] k, auto)
  done

lemma inv_loop6_Bk_tail[elim]: "0 < x; inv_loop6 x (b, Bk # list); b  []  inv_loop6 x (tl b, hd b # Bk # list)"
  apply(simp add: inv_loop6.simps)
  apply(case_tac "hd b", simp_all, auto)
  done

lemma inv_loop2_Oc_via_1[elim]: "0 < x; inv_loop1 x (b, Oc # list)  inv_loop2 x (Oc # b, list)"
  apply(auto simp: inv_loop1.simps inv_loop2.simps,force)
  done

lemma inv_loop2_Bk_via_Oc[elim]: "0 < x; inv_loop2 x (b, Oc # list)  inv_loop2 x (b, Bk # list)"
  by (auto simp: inv_loop2.simps)

lemma inv_loop4_Oc_via_3[elim]: "0 < x; inv_loop3 x (b, Oc # list)  inv_loop4 x (Oc # b, list)"
  apply(auto simp: inv_loop3.simps inv_loop4.simps)
   apply(rename_tac i j)
   apply(rule_tac [!] x = i in exI, auto)
   apply(rule_tac [!] x = "Suc 0" in exI, rule_tac [!] x = "j - 1" in exI)
   apply(case_tac [!] j, auto)
  done

lemma inv_loop4_Oc_move[elim]:
  assumes "0 < x" "inv_loop4 x (b, Oc # list)"
  shows "inv_loop4 x (Oc # b, list)"
proof -
  from assms[unfolded inv_loop4.simps] obtain i j k t where
    "i + j = x"
    "0 < i" "0 < j" "k + t = j" "(b, Oc # list) = (Oc  k @ Bk  Suc j @ Oc  i, Oc  t)"
    by auto  
  thus ?thesis unfolding inv_loop4.simps
    apply(rule_tac [!] x = "i" in exI,rule_tac [!] x = "j" in exI)
    apply(rule_tac [!] x = "Suc k" in exI,rule_tac [!] x = "t - 1" in exI)
    by(cases t,auto)
qed

lemma inv_loop5_exit_no_Oc[simp]: "inv_loop5_exit x (b, Oc # list) = False"
  by (auto simp: inv_loop5_exit.simps)

lemma inv_loop5_exit_Bk_Oc_via_loop[elim]: " inv_loop5_loop x (b, Oc # list); b  []; hd b = Bk
   inv_loop5_exit x (tl b, Bk # Oc # list)"
  apply(simp only: inv_loop5_loop.simps inv_loop5_exit.simps)
  apply(erule_tac exE)+
  apply(rename_tac i j k t)
  apply(rule_tac x = i in exI)
  apply(case_tac k, auto)
  done

lemma inv_loop5_loop_Oc_Oc_drop[elim]: "inv_loop5_loop x (b, Oc # list); b  []; hd b = Oc 
            inv_loop5_loop x (tl b, Oc # Oc # list)"
  apply(simp only:  inv_loop5_loop.simps)
  apply(erule_tac exE)+
  apply(rename_tac i j k t)
  apply(rule_tac x = i in exI, rule_tac x = j in exI)
  apply(rule_tac x = "k - 1" in exI, rule_tac x = "Suc t" in exI)
  apply(case_tac k, auto)
  done

lemma inv_loop5_Oc_tl[elim]: "inv_loop5 x (b, Oc # list); b  []  inv_loop5 x (tl b, hd b # Oc # list)"
  apply(simp add: inv_loop5.simps)
  apply(cases "hd b", simp_all, auto)
  done

lemma inv_loop1_Bk_Oc_via_6[elim]: "0 < x; inv_loop6 x ([], Oc # list)  inv_loop1 x ([], Bk # Oc # list)"
  by(auto simp: inv_loop6.simps inv_loop1.simps inv_loop6_loop.simps inv_loop6_exit.simps)

lemma inv_loop1_Oc_via_6[elim]: "0 < x; inv_loop6 x (b, Oc # list); b  [] 
            inv_loop1 x (tl b, hd b # Oc # list)"
  by(auto simp: inv_loop6.simps inv_loop1.simps inv_loop6_loop.simps inv_loop6_exit.simps)


lemma inv_loop_nonempty[simp]:
  "inv_loop1 x (b, []) = False"
  "inv_loop2 x ([], b) = False"
  "inv_loop2 x (l', []) = False"
  "inv_loop3 x (b, []) = False"
  "inv_loop4 x ([], b) = False"
  "inv_loop5 x ([], list) = False"
  "inv_loop6 x ([], Bk # xs) = False"
  by (auto simp: inv_loop1.simps inv_loop2.simps inv_loop3.simps inv_loop4.simps 
      inv_loop5.simps inv_loop6.simps inv_loop5_exit.simps inv_loop5_loop.simps
      inv_loop6_loop.simps)

lemma inv_loop_nonemptyE[elim]:
  "inv_loop5 x (b, [])  RR" "inv_loop6 x (b, [])  RR" 
  "inv_loop1 x (b, Bk # list)  b = []"
  by (auto simp: inv_loop4.simps inv_loop5.simps inv_loop5_exit.simps inv_loop5_loop.simps
      inv_loop6.simps inv_loop6_exit.simps inv_loop6_loop.simps inv_loop1.simps)

lemma inv_loop6_Bk_Bk_drop[elim]: "inv_loop6 x ([], Bk # list)  inv_loop6 x ([], Bk # Bk # list)"
  by (simp)

lemma inv_loop_step: 
  "inv_loop x cf; x > 0  inv_loop x (step cf (tcopy_loop, 0))"
  apply(cases cf, cases "snd (snd cf)"; cases "hd (snd (snd cf))")
     apply(auto simp: inv_loop.simps step.simps tcopy_loop_def numeral split: if_splits)
  done

lemma inv_loop_steps:
  "inv_loop x cf; x > 0  inv_loop x (steps cf (tcopy_loop, 0) stp)"
  apply(induct stp, simp add: steps.simps, simp)
  apply(erule_tac inv_loop_step, simp)
  done

fun loop_stage :: "config  nat"
  where
    "loop_stage (s, l, r) = (if s = 0 then 0
                           else (Suc (length (takeWhile (λa. a = Oc) (rev l @ r)))))"

fun loop_state :: "config  nat"
  where
    "loop_state (s, l, r) = (if s = 2  hd r = Oc then 0
                           else if s = 1 then 1
                           else 10 - s)"

fun loop_step :: "config  nat"
  where
    "loop_step (s, l, r) = (if s = 3 then length r
                          else if s = 4 then length r
                          else if s = 5 then length l 
                          else if s = 6 then length l
                          else 0)"

definition measure_loop :: "(config × config) set"
  where
    "measure_loop = measures [loop_stage, loop_state, loop_step]"

lemma wf_measure_loop: "wf measure_loop"
  unfolding measure_loop_def
  by (auto)

lemma measure_loop_induct [case_names Step]: 
  "n. ¬ P (f n)  (f (Suc n), (f n))  measure_loop  n. P (f n)"
  using wf_measure_loop
  by (metis wf_iff_no_infinite_down_chain)

lemma inv_loop4_not_just_Oc[elim]: 
  "inv_loop4 x (l', []);
  length (takeWhile (λa. a = Oc) (rev l' @ [Oc]))  
  length (takeWhile (λa. a = Oc) (rev l'))
   RR"
  "inv_loop4 x (l', Bk # list);
   length (takeWhile (λa. a = Oc) (rev l' @ Oc # list))  
    length (takeWhile (λa. a = Oc) (rev l' @ Bk # list))
     RR"
   apply(auto simp: inv_loop4.simps)
  apply(rename_tac i j)
  apply(case_tac [!] j, simp_all add: List.takeWhile_tail)
  done

lemma takeWhile_replicate_append: 
  "P a  takeWhile P (ax @ ys) = ax @ takeWhile P ys"
  by (induct x, auto)

lemma takeWhile_replicate: 
  "P a  takeWhile P (ax) = ax"
  by (induct x, auto)

lemma inv_loop5_Bk_E[elim]: 
  "inv_loop5 x (l', Bk # list); l'  []; 
   length (takeWhile (λa. a = Oc) (rev (tl l') @ hd l' # Bk # list)) 
   length (takeWhile (λa. a = Oc) (rev l' @ Bk # list))
    RR"
  apply(cases "length list";cases "length list - 1"
      ,auto simp: inv_loop5.simps inv_loop5_exit.simps
      takeWhile_replicate_append takeWhile_replicate)
   apply(cases "length list - 2"; force simp add: List.takeWhile_tail)+
  done

lemma inv_loop1_hd_Oc[elim]: "inv_loop1 x (l', Oc # list)  hd list = Oc"
  by (auto simp: inv_loop1.simps)

lemma inv_loop6_not_just_Bk[dest!]: 
  "length (takeWhile P (rev (tl l') @ hd l' # list))  
  length (takeWhile P (rev l' @ list))
   l' = []"
  apply(cases l', simp_all)
  done

lemma inv_loop2_OcE[elim]:
  "inv_loop2 x (l', Oc # list); l'  []  
  length (takeWhile (λa. a = Oc) (rev l' @ Bk # list)) <
  length (takeWhile (λa. a = Oc) (rev l' @ Oc # list))"
  apply(auto simp: inv_loop2.simps takeWhile_tail takeWhile_replicate_append
      takeWhile_replicate)
  done

lemma loop_halts: 
  assumes h: "n > 0" "inv_loop n (1, l, r)"
  shows " stp. is_final (steps0 (1, l, r) tcopy_loop stp)"
proof (induct rule: measure_loop_induct) 
  case (Step stp)
  have "¬ is_final (steps0 (1, l, r) tcopy_loop stp)" by fact
  moreover
  have "inv_loop n (steps0 (1, l, r) tcopy_loop stp)"
    by (rule_tac inv_loop_steps) (simp_all only: h)
  moreover
  obtain s l' r' where eq: "(steps0 (1, l, r) tcopy_loop stp) = (s, l', r')"
    by (metis measure_begin_state.cases)
  ultimately 
  have "(step0 (s, l', r') tcopy_loop, s, l', r')  measure_loop"
    using h(1)
    apply(cases r';cases "hd r'")
       apply(auto simp: inv_loop.simps step.simps tcopy_loop_def numeral measure_loop_def split: if_splits)
    done
  then 
  show "(steps0 (1, l, r) tcopy_loop (Suc stp), steps0 (1, l, r) tcopy_loop stp)  measure_loop"
    using eq by (simp only: step_red)
qed

lemma loop_correct:
  assumes "0 < n"
  shows "{inv_loop1 n} tcopy_loop {inv_loop0 n}"
  using assms
proof(rule_tac Hoare_haltI)
  fix l r
  assume h: "0 < n" "inv_loop1 n (l, r)"
  then obtain stp where k: "is_final (steps0 (1, l, r) tcopy_loop stp)" 
    using loop_halts
    apply(simp add: inv_loop.simps)
    apply(blast)
    done
  moreover
  have "inv_loop n (steps0 (1, l, r) tcopy_loop stp)"
    using h 
    by (rule_tac inv_loop_steps) (simp_all add: inv_loop.simps)
  ultimately show
    "stp. is_final (steps0 (1, l, r) tcopy_loop stp)  
    inv_loop0 n holds_for steps0 (1, l, r) tcopy_loop stp"
    using h(1) 
    apply(rule_tac x = stp in exI)
    apply(case_tac "(steps0 (1, l, r) tcopy_loop stp)")
    apply(simp add: inv_loop.simps)
    done
qed




(* tcopy_end *)

fun
  inv_end5_loop :: "nat  tape  bool" and
  inv_end5_exit :: "nat  tape  bool" 
  where  
    "inv_end5_loop x (l, r) = 
     ( i j. i + j = x  x > 0  j > 0  l = Oci @ [Bk]  r = Ocj @ Bk # Ocx)"
  | "inv_end5_exit x (l, r) = (x > 0  l = []  r = Bk # Ocx @ Bk # Ocx)"

fun 
  inv_end0 :: "nat  tape   bool" and
  inv_end1 :: "nat  tape  bool" and
  inv_end2 :: "nat  tape  bool" and
  inv_end3 :: "nat  tape  bool" and
  inv_end4 :: "nat  tape  bool" and 
  inv_end5 :: "nat  tape  bool" 
  where
    "inv_end0 n (l, r) = (n > 0  (l, r) = ([Bk], Ocn @ Bk # Ocn))"
  | "inv_end1 n (l, r) = (n > 0  (l, r) = ([Bk], Oc # Bkn @ Ocn))"
  | "inv_end2 n (l, r) = ( i j. i + j = Suc n  n > 0  l = Oci @ [Bk]  r = Bkj @ Ocn)"
  | "inv_end3 n (l, r) =
     ( i j. n > 0  i + j = n  l = Oci @ [Bk]  r = Oc # Bkj@ Ocn)"
  | "inv_end4 n (l, r) = ( any. n > 0  l = Ocn @ [Bk]  r = any#Ocn)"
  | "inv_end5 n (l, r) = (inv_end5_loop n (l, r)  inv_end5_exit n (l, r))"

fun 
  inv_end :: "nat  config  bool"
  where
    "inv_end n (s, l, r) = (if s = 0 then inv_end0 n (l, r)
                          else if s = 1 then inv_end1 n (l, r)
                          else if s = 2 then inv_end2 n (l, r)
                          else if s = 3 then inv_end3 n (l, r)
                          else if s = 4 then inv_end4 n (l, r)
                          else if s = 5 then inv_end5 n (l, r)
                          else False)"

declare inv_end.simps[simp del] inv_end1.simps[simp del]
  inv_end0.simps[simp del] inv_end2.simps[simp del]
  inv_end3.simps[simp del] inv_end4.simps[simp del]
  inv_end5.simps[simp del]

lemma inv_end_nonempty[simp]:
  "inv_end1 x (b, []) = False"
  "inv_end1 x ([], list) = False"
  "inv_end2 x (b, []) = False"
  "inv_end3 x (b, []) = False"
  "inv_end4 x (b, []) = False"
  "inv_end5 x (b, []) = False"
  "inv_end5 x ([], Oc # list) = False"
  by (auto simp: inv_end1.simps inv_end2.simps inv_end3.simps inv_end4.simps inv_end5.simps)

lemma inv_end0_Bk_via_1[elim]: "0 < x; inv_end1 x (b, Bk # list); b  []
   inv_end0 x (tl b, hd b # Bk # list)"
  by (auto simp: inv_end1.simps inv_end0.simps)

lemma inv_end3_Oc_via_2[elim]: "0 < x; inv_end2 x (b, Bk # list) 
   inv_end3 x (b, Oc # list)"
  apply(auto simp: inv_end2.simps inv_end3.simps)
  by (metis Cons_replicate_eq One_nat_def Suc_inject Suc_pred add_Suc_right cell.distinct(1)
      empty_replicate list.sel(3) neq0_conv self_append_conv2 tl_append2 tl_replicate)

lemma inv_end2_Bk_via_3[elim]: "0 < x; inv_end3 x (b, Bk # list)  inv_end2 x (Bk # b, list)"
  by (auto simp: inv_end2.simps inv_end3.simps)

lemma inv_end5_Bk_via_4[elim]: "0 < x; inv_end4 x ([], Bk # list)  
  inv_end5 x ([], Bk # Bk # list)"
  by (auto simp: inv_end4.simps inv_end5.simps)

lemma inv_end5_Bk_tail_via_4[elim]: "0 < x; inv_end4 x (b, Bk # list); b  []  
  inv_end5 x (tl b, hd b # Bk # list)"
  apply(auto simp: inv_end4.simps inv_end5.simps)
  apply(rule_tac x = 1 in exI, simp)
  done

lemma inv_end0_Bk_via_5[elim]: "0 < x; inv_end5 x (b, Bk # list)  inv_end0 x (Bk # b, list)"
  by(auto simp: inv_end5.simps inv_end0.simps gr0_conv_Suc)

lemma inv_end2_Oc_via_1[elim]: "0 < x; inv_end1 x (b, Oc # list)  inv_end2 x (Oc # b, list)"
  by (auto simp: inv_end1.simps inv_end2.simps)

lemma inv_end4_Bk_Oc_via_2[elim]: "0 < x; inv_end2 x ([], Oc # list) 
               inv_end4 x ([], Bk # Oc # list)"
  by (auto simp: inv_end2.simps inv_end4.simps)

lemma inv_end4_Oc_via_2[elim]:  "0 < x; inv_end2 x (b, Oc # list); b  [] 
  inv_end4 x (tl b, hd b # Oc # list)"
  by(auto simp: inv_end2.simps inv_end4.simps gr0_conv_Suc)

lemma inv_end2_Oc_via_3[elim]: "0 < x; inv_end3 x (b, Oc # list)  inv_end2 x (Oc # b, list)"
  by (auto simp: inv_end2.simps inv_end3.simps)

lemma inv_end4_Bk_via_Oc[elim]: "0 < x; inv_end4 x (b, Oc # list)  inv_end4 x (b, Bk # list)"
  by (auto simp: inv_end2.simps inv_end4.simps)

lemma inv_end5_Bk_drop_Oc[elim]: "0 < x; inv_end5 x ([], Oc # list)  inv_end5 x ([], Bk # Oc # list)"
  by (auto simp: inv_end2.simps inv_end5.simps)

declare inv_end5_loop.simps[simp del]
  inv_end5_exit.simps[simp del]

lemma inv_end5_exit_no_Oc[simp]: "inv_end5_exit x (b, Oc # list) = False"
  by (auto simp: inv_end5_exit.simps)

lemma inv_end5_loop_no_Bk_Oc[simp]: "inv_end5_loop x (tl b, Bk # Oc # list) = False"
  by (auto simp: inv_end5_loop.simps)

lemma inv_end5_exit_Bk_Oc_via_loop[elim]:
  "0 < x; inv_end5_loop x (b, Oc # list); b  []; hd b = Bk 
  inv_end5_exit x (tl b, Bk # Oc # list)"
  apply(auto simp: inv_end5_loop.simps inv_end5_exit.simps)
  using hd_replicate apply fastforce
  by (metis cell.distinct(1) hd_append2 hd_replicate list.sel(3) self_append_conv2
      split_head_repeat(2))

lemma inv_end5_loop_Oc_Oc_drop[elim]: 
  "0 < x; inv_end5_loop x (b, Oc # list); b  []; hd b = Oc 
  inv_end5_loop x (tl b, Oc # Oc # list)"
  apply(simp only: inv_end5_loop.simps inv_end5_exit.simps)
  apply(erule_tac exE)+
  apply(rename_tac i j)
  apply(rule_tac x = "i - 1" in exI, 
      rule_tac x = "Suc j" in exI, auto)
   apply(case_tac [!] i, simp_all)
  done

lemma inv_end5_Oc_tail[elim]: "0 < x; inv_end5 x (b, Oc # list); b  []  
  inv_end5 x (tl b, hd b # Oc # list)"
  apply(simp add: inv_end2.simps inv_end5.simps)
  apply(case_tac "hd b", simp_all, auto)
  done

lemma inv_end_step:
  "x > 0; inv_end x cf  inv_end x (step cf (tcopy_end, 0))"
  apply(cases cf, cases "snd (snd cf)"; cases "hd (snd (snd cf))")
     apply(auto simp: inv_end.simps step.simps tcopy_end_def numeral split: if_splits)
  done

lemma inv_end_steps:
  "x > 0; inv_end x cf  inv_end x (steps cf (tcopy_end, 0) stp)"
  apply(induct stp, simp add:steps.simps, simp)
  apply(erule_tac inv_end_step, simp)
  done

fun end_state :: "config  nat"
  where
    "end_state (s, l, r) = 
       (if s = 0 then 0
        else if s = 1 then 5
        else if s = 2  s = 3 then 4
        else if s = 4 then 3 
        else if s = 5 then 2
        else 0)"

fun end_stage :: "config  nat"
  where
    "end_stage (s, l, r) = 
          (if s = 2  s = 3 then (length r) else 0)"

fun end_step :: "config  nat"
  where
    "end_step (s, l, r) = 
         (if s = 4 then (if hd r = Oc then 1 else 0)
          else if s = 5 then length l
          else if s = 2 then 1
          else if s = 3 then 0
          else 0)"

definition end_LE :: "(config × config) set"
  where
    "end_LE = measures [end_state, end_stage, end_step]"

lemma wf_end_le: "wf end_LE"
  unfolding end_LE_def by auto

lemma halt_lemma: 
  "wf LE; n. (¬ P (f n)  (f (Suc n), (f n))  LE)  n. P (f n)"
  by (metis wf_iff_no_infinite_down_chain)

lemma end_halt: 
  "x > 0; inv_end x (Suc 0, l, r)  
       stp. is_final (steps (Suc 0, l, r) (tcopy_end, 0) stp)"
proof(rule halt_lemma[OF wf_end_le])
  assume great: "0 < x"
    and inv_start: "inv_end x (Suc 0, l, r)"
  show "n. ¬ is_final (steps (Suc 0, l, r) (tcopy_end, 0) n)  
    (steps (Suc 0, l, r) (tcopy_end, 0) (Suc n), steps (Suc 0, l, r) (tcopy_end, 0) n)  end_LE"
  proof(rule_tac allI, rule_tac impI)
    fix n
    assume notfinal: "¬ is_final (steps (Suc 0, l, r) (tcopy_end, 0) n)"
    obtain s' l' r' where d: "steps (Suc 0, l, r) (tcopy_end, 0) n = (s', l', r')"
      apply(case_tac "steps (Suc 0, l, r) (tcopy_end, 0) n", auto)
      done
    hence "inv_end x (s', l', r')  s'  0"
      using great inv_start notfinal
      apply(drule_tac stp = n in inv_end_steps, auto)
      done
    hence "(step (s', l', r') (tcopy_end, 0), s', l', r')  end_LE"
      apply(cases r'; cases "hd r'")
         apply(auto simp: inv_end.simps step.simps tcopy_end_def numeral end_LE_def split: if_splits)
      done
    thus "(steps (Suc 0, l, r) (tcopy_end, 0) (Suc n), 
      steps (Suc 0, l, r) (tcopy_end, 0) n)  end_LE"
      using d
      by simp
  qed
qed

lemma end_correct:
  "n > 0  {inv_end1 n} tcopy_end {inv_end0 n}"
proof(rule_tac Hoare_haltI)
  fix l r
  assume h: "0 < n"
    "inv_end1 n (l, r)"
  then have " stp. is_final (steps0 (1, l, r) tcopy_end stp)"
    by (simp add: end_halt inv_end.simps)
  then obtain stp where "is_final (steps0 (1, l, r) tcopy_end stp)" ..
  moreover have "inv_end n (steps0 (1, l, r) tcopy_end stp)"
    apply(rule_tac inv_end_steps)
    using h by(simp_all add: inv_end.simps)
  ultimately show
    "stp. is_final (steps (1, l, r) (tcopy_end, 0) stp)  
    inv_end0 n holds_for steps (1, l, r) (tcopy_end, 0) stp"        
    using h
    apply(rule_tac x = stp in exI)
    apply(cases "(steps0 (1, l, r) tcopy_end stp)") 
    apply(simp add: inv_end.simps)
    done
qed

(* tcopy *)

lemma tm_wf_tcopy[intro]:
  "tm_wf (tcopy_begin, 0)"
  "tm_wf (tcopy_loop, 0)"
  "tm_wf (tcopy_end, 0)"
  by (auto simp: tm_wf.simps tcopy_end_def tcopy_loop_def tcopy_begin_def)

lemma tcopy_correct1: 
  assumes "0 < x"
  shows "{inv_begin1 x} tcopy {inv_end0 x}"
proof -
  have "{inv_begin1 x} tcopy_begin {inv_begin0 x}"
    by (metis assms begin_correct) 
  moreover 
  have "inv_begin0 x  inv_loop1 x"
    unfolding assert_imp_def
    unfolding inv_begin0.simps inv_loop1.simps
    unfolding inv_loop1_loop.simps inv_loop1_exit.simps
    apply(auto simp add: numeral Cons_eq_append_conv)
    by (rule_tac x = "Suc 0" in exI, auto)
  ultimately have "{inv_begin1 x} tcopy_begin {inv_loop1 x}"
    by (rule_tac Hoare_consequence) (auto)
  moreover
  have "{inv_loop1 x} tcopy_loop {inv_loop0 x}"
    by (metis assms loop_correct) 
  ultimately 
  have "{inv_begin1 x} (tcopy_begin |+| tcopy_loop) {inv_loop0 x}"
    by (rule_tac Hoare_plus_halt) (auto)
  moreover 
  have "{inv_end1 x} tcopy_end {inv_end0 x}"
    by (metis assms end_correct) 
  moreover 
  have "inv_loop0 x = inv_end1 x"
    by(auto simp: inv_end1.simps inv_loop1.simps assert_imp_def)
  ultimately 
  show "{inv_begin1 x} tcopy {inv_end0 x}"
    unfolding tcopy_def
    by (rule_tac Hoare_plus_halt) (auto)
qed

abbreviation (input)
  "pre_tcopy n  λtp. tp = ([]::cell list, Oc  (Suc n))"
abbreviation (input)
  "post_tcopy n  λtp. tp= ([Bk], <(n, n::nat)>)"

lemma tcopy_correct:
  shows "{pre_tcopy n} tcopy {post_tcopy n}"
proof -
  have "{inv_begin1 (Suc n)} tcopy {inv_end0 (Suc n)}"
    by (rule tcopy_correct1) (simp)
  moreover
  have "pre_tcopy n = inv_begin1 (Suc n)"
    by (auto)
  moreover
  have "inv_end0 (Suc n) = post_tcopy n"
    unfolding fun_eq_iff
    by (auto simp add: inv_end0.simps tape_of_nat_def tape_of_prod_def)
  ultimately
  show "{pre_tcopy n} tcopy {post_tcopy n}" 
    by simp
qed


section ‹The {\em Dithering} Turing Machine›

text ‹
  The {\em Dithering} TM, when the input is 1›, it will loop forever, otherwise, it will
  terminate.
›

definition dither :: "instr list"
  where
    "dither  [(W0, 1), (R, 2), (L, 1), (L, 0)] "

(* invariants of dither *)
abbreviation (input)
  "dither_halt_inv  λtp. k. tp = (Bk  k, <1::nat>)"

abbreviation (input)
  "dither_unhalt_inv  λtp. k. tp = (Bk  k, <0::nat>)"

lemma dither_loops_aux: 
  "(steps0 (1, Bk  m, [Oc]) dither stp = (1, Bk  m, [Oc]))  
   (steps0 (1, Bk  m, [Oc]) dither stp = (2, Oc # Bk  m, []))"
  apply(induct stp)
   apply(auto simp: steps.simps step.simps dither_def numeral)
  done

lemma dither_loops:
  shows "{dither_unhalt_inv} dither " 
  apply(rule Hoare_unhaltI)
  using dither_loops_aux
  apply(auto simp add: numeral tape_of_nat_def)
  by (metis Suc_neq_Zero is_final_eq)

lemma dither_halts_aux: 
  shows "steps0 (1, Bk  m, [Oc, Oc]) dither 2 = (0, Bk  m, [Oc, Oc])"
  unfolding dither_def
  by (simp add: steps.simps step.simps numeral)

lemma dither_halts:
  shows "{dither_halt_inv} dither {dither_halt_inv}" 
  apply(rule Hoare_haltI)
  using dither_halts_aux
  apply(auto simp add: tape_of_nat_def)
  by (metis (lifting, mono_tags) holds_for.simps is_final_eq)


section ‹The diagnal argument below shows the undecidability of Halting problem›

text halts tp x› means TM tp› terminates on input x›
  and the final configuration is standard.
›

definition halts :: "tprog0  nat list  bool"
  where
    "halts p ns  {(λtp. tp = ([], <ns>))} p {(λtp. (k n l. tp = (Bk  k,  <n::nat> @ Bk  l)))}"

lemma tm_wf0_tcopy[intro, simp]: "tm_wf0 tcopy"
  by (auto simp: tcopy_def)

lemma tm_wf0_dither[intro, simp]: "tm_wf0 dither"
  by (auto simp: tm_wf.simps dither_def)

text ‹
  The following locale specifies that TM H› can be used to solve 
  the {\em Halting Problem} and False› is going to be derived 
  under this locale. Therefore, the undecidability of {\em Halting Problem}
  is established. 
›

locale uncomputable = 
  (* The coding function of TM, interestingly, the detailed definition of this 
  funciton @{text "code"} does not affect the final result. *)
  fixes code :: "instr list  nat" 
    (* 
  The TM @{text "H"} is the one which is assummed being able to solve the Halting problem.
  *)
    and H :: "instr list"
  assumes h_wf[intro]: "tm_wf0 H"
    (*
  The following two assumptions specifies that @{text "H"} does solve the Halting problem.
  *)
    and h_case: 
    " M ns. halts M ns  {(λtp. tp = ([Bk], <(code M, ns)>))} H {(λtp. k. tp = (Bk  k, <0::nat>))}"
    and nh_case: 
    " M ns. ¬ halts M ns  {(λtp. tp = ([Bk], <(code M, ns)>))} H {(λtp. k. tp = (Bk  k, <1::nat>))}"
begin

(* invariants for H *)
abbreviation (input)
  "pre_H_inv M ns  λtp. tp = ([Bk], <(code M, ns::nat list)>)"

abbreviation (input)
  "post_H_halt_inv  λtp. k. tp = (Bk  k, <1::nat>)"

abbreviation (input)
  "post_H_unhalt_inv  λtp. k. tp = (Bk  k, <0::nat>)"


lemma H_halt_inv:
  assumes "¬ halts M ns" 
  shows "{pre_H_inv M ns} H {post_H_halt_inv}"
  using assms nh_case by auto

lemma H_unhalt_inv:
  assumes "halts M ns" 
  shows "{pre_H_inv M ns} H {post_H_unhalt_inv}"
  using assms h_case by auto

(* TM that produces the contradiction and its code *)

definition
  "tcontra  (tcopy |+| H) |+| dither"
abbreviation
  "code_tcontra  code tcontra"

(* assume tcontra does not halt on its code *)
lemma tcontra_unhalt: 
  assumes "¬ halts tcontra [code tcontra]"
  shows "False"
proof -
  (* invariants *)
  define P1 where "P1  λtp. tp = ([]::cell list, <code_tcontra>)"
  define P2 where "P2  λtp. tp = ([Bk], <(code_tcontra, code_tcontra)>)"
  define P3 where "P3  λtp. k. tp = (Bk  k, <1::nat>)"

(*
  {P1} tcopy {P2}  {P2} H {P3} 
  ----------------------------
     {P1} (tcopy |+| H) {P3}     {P3} dither {P3}
  ------------------------------------------------
                 {P1} tcontra {P3}
  *)

  have H_wf: "tm_wf0 (tcopy |+| H)" by auto

(* {P1} (tcopy |+| H) {P3} *)
  have first: "{P1} (tcopy |+| H) {P3}" 
  proof (cases rule: Hoare_plus_halt)
    case A_halt (* of tcopy *)
    show "{P1} tcopy {P2}" unfolding P1_def P2_def tape_of_nat_def
      by (rule tcopy_correct)
  next
    case B_halt (* of H *)
    show "{P2} H {P3}"
      unfolding P2_def P3_def 
      using H_halt_inv[OF assms]
      by (simp add: tape_of_prod_def tape_of_list_def)
  qed (simp)

(* {P3} dither {P3} *)
  have second: "{P3} dither {P3}" unfolding P3_def 
    by (rule dither_halts)

(* {P1} tcontra {P3} *)
  have "{P1} tcontra {P3}" 
    unfolding tcontra_def
    by (rule Hoare_plus_halt[OF first second H_wf])

  with assms show "False"
    unfolding P1_def P3_def
    unfolding halts_def
    unfolding Hoare_halt_def 
    apply(auto) apply(rename_tac n)
    apply(drule_tac x = n in spec)
    apply(case_tac "steps0 (Suc 0, [], <code tcontra>) tcontra n")
    apply(auto simp add: tape_of_list_def)
    by (metis append_Nil2 replicate_0)
qed

(* asumme tcontra halts on its code *)
lemma tcontra_halt: 
  assumes "halts tcontra [code tcontra]"
  shows "False"
proof - 
  (* invariants *)
  define P1 where "P1  λtp. tp = ([]::cell list, <code_tcontra>)"
  define P2 where "P2  λtp. tp = ([Bk], <(code_tcontra, code_tcontra)>)"
  define Q3 where "Q3  λtp. k. tp = (Bk  k, <0::nat>)"

(*
  {P1} tcopy {P2}  {P2} H {Q3} 
  ----------------------------
     {P1} (tcopy |+| H) {Q3}     {Q3} dither loops
  ------------------------------------------------
               {P1} tcontra loops
  *)

  have H_wf: "tm_wf0 (tcopy |+| H)" by auto

(* {P1} (tcopy |+| H) {Q3} *)
  have first: "{P1} (tcopy |+| H) {Q3}" 
  proof (cases rule: Hoare_plus_halt)
    case A_halt (* of tcopy *)
    show "{P1} tcopy {P2}" unfolding P1_def P2_def tape_of_nat_def
      by (rule tcopy_correct)
  next
    case B_halt (* of H *)
    then show "{P2} H {Q3}"
      unfolding P2_def Q3_def using H_unhalt_inv[OF assms]
      by(simp add: tape_of_prod_def tape_of_list_def)
  qed (simp)

(* {P3} dither loops *)
  have second: "{Q3} dither " unfolding Q3_def 
    by (rule dither_loops)

(* {P1} tcontra loops *)
  have "{P1} tcontra " 
    unfolding tcontra_def
    by (rule Hoare_plus_unhalt[OF first second H_wf])

  with assms show "False"
    unfolding P1_def
    unfolding halts_def
    unfolding Hoare_halt_def Hoare_unhalt_def
    by (auto simp add: tape_of_list_def)
qed


text False› can finally derived.
›

lemma false: "False"
  using tcontra_halt tcontra_unhalt 
  by auto

end

declare replicate_Suc[simp del]

end

Theory Abacus_Mopup

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

chapter ‹Mopup Turing Machine that deletes all "registers", except one›

theory Abacus_Mopup
  imports Uncomputable
begin

fun mopup_a :: "nat  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  [(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  instr list"
  where 
    "mopup n = mopup_a n @ shift mopup_b (2*n)"

type_synonym mopup_type = "config  nat list  nat  cell list  bool"

fun mopup_stop :: "mopup_type"
  where
    "mopup_stop (s, l, r) lm n ires= 
        ( ln rn. l = Bkln @ Bk # Bk # ires  r = <lm ! n> @ Bkrn)"

fun mopup_bef_erase_a :: "mopup_type"
  where
    "mopup_bef_erase_a (s, l, r) lm n ires= 
         ( ln m rn. l = Bkln @ Bk # Bk # ires  
                  r = Ocm@ Bk # <(drop ((s + 1) div 2) lm)> @ Bkrn)"

fun mopup_bef_erase_b :: "mopup_type"
  where
    "mopup_bef_erase_b (s, l, r) lm n ires = 
      ( ln m rn. l = Bkln @ Bk # Bk # ires  r = Bk # Ocm @ Bk # 
                                      <(drop (s div 2) lm)> @ Bkrn)"

fun mopup_jump_over1 :: "mopup_type"
  where
    "mopup_jump_over1 (s, l, r) lm n ires = 
      ( ln m1 m2 rn. m1 + m2 = Suc (lm ! n)  
        l = Ocm1 @ Bkln @ Bk # Bk # ires  
     (r = Ocm2 @ Bk # <(drop (Suc n) lm)> @ Bkrn  
     (r = Ocm2  (drop (Suc n) lm) = [])))"

fun mopup_aft_erase_a :: "mopup_type"
  where
    "mopup_aft_erase_a (s, l, r) lm n ires = 
      ( lnl lnr rn (ml::nat list) m. 
          m = Suc (lm ! n)  l = Bklnr @ Ocm @ Bklnl @ Bk # Bk # ires  
                                   (r = <ml> @ Bkrn))"

fun mopup_aft_erase_b :: "mopup_type"
  where
    "mopup_aft_erase_b (s, l, r) lm n ires= 
   ( lnl lnr rn (ml::nat list) m. 
      m = Suc (lm ! n)  
      l = Bklnr @ Ocm @ Bklnl @ Bk # Bk # ires  
     (r = Bk # <ml> @ Bkrn 
      r = Bk # Bk # <ml> @ Bkrn))"

fun mopup_aft_erase_c :: "mopup_type"
  where
    "mopup_aft_erase_c (s, l, r) lm n ires = 
 ( lnl lnr rn (ml::nat list) m. 
     m = Suc (lm ! n)  
     l = Bklnr @ Ocm @ Bklnl @ Bk # Bk # ires  
    (r = <ml> @ Bkrn  r = Bk # <ml> @ Bkrn))"

fun mopup_left_moving :: "mopup_type"
  where
    "mopup_left_moving (s, l, r) lm n ires = 
  ( lnl lnr rn m.
     m = Suc (lm ! n)  
   ((l = Bklnr @ Ocm @ Bklnl @ Bk # Bk # ires  r = Bkrn) 
    (l = Oc(m - 1) @ Bklnl @ Bk # Bk # ires  r = Oc # Bkrn)))"

fun mopup_jump_over2 :: "mopup_type"
  where
    "mopup_jump_over2 (s, l, r) lm n ires = 
     ( ln rn m1 m2.
          m1 + m2 = Suc (lm ! n) 
         r  [] 
         (hd r = Oc  (l = Ocm1 @ Bkln @ Bk # Bk # ires  r = Ocm2 @ Bkrn)) 
         (hd r = Bk  (l = Bkln @ Bk # ires  r = Bk # Oc(m1+m2)@ Bkrn)))"


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  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 mop_bef_length[simp]: "length (mopup_a n) = 4 * n"
  by(induct n, simp_all)

lemma mopup_a_nth: 
  "q < n; x < 4  mopup_a n ! (4 * q + x) = 
                             mopup_a (Suc q) ! ((4 * q) + x)"
proof(induct n)
  case (Suc n)
  then show ?case 
    by(cases "q < n";cases "q = n", auto simp add: nth_append)
qed auto

lemma fetch_bef_erase_a_o[simp]: 
  "0 < s; s  2 * n; s mod 2 = Suc 0
   (fetch (mopup_a n @ shift mopup_b (2 * n)) s Oc) = (W0, s + 1)"
  apply(subgoal_tac " q. s = 2*q + 1", auto)
   apply(subgoal_tac "length (mopup_a n) = 4*n")
    apply(auto simp: nth_append)
   apply(subgoal_tac "mopup_a n ! (4 * q + 1) = 
                      mopup_a (Suc q) ! ((4 * q) + 1)", 
      simp add: nth_append)
   apply(rule mopup_a_nth, auto)
  apply arith
  done

lemma fetch_bef_erase_a_b[simp]:
  "0 < s; s  2 * n; s mod 2 = Suc 0
     (fetch (mopup_a n @ shift mopup_b (2 * n)) s Bk) = (R, s + 2)"
  apply(subgoal_tac " q. s = 2*q + 1", auto)
   apply(subgoal_tac "length (mopup_a n) = 4*n")
    apply(auto simp: nth_append)
   apply(subgoal_tac "mopup_a n ! (4 * q + 0) = 
                       mopup_a (Suc q) ! ((4 * q + 0))", 
      simp add: nth_append)
   apply(rule mopup_a_nth, auto)
  apply arith
  done

lemma fetch_bef_erase_b_b: 
  assumes "n < length lm" "0 < s" "s  2 * n" "s mod 2 = 0"
  shows "(fetch (mopup_a n @ shift mopup_b (2 * n)) s Bk) = (R, s - 1)"
proof -
  from assms obtain q where q:"s = 2 * q" by auto
  then obtain nat where nat:"q = Suc nat" using assms(2) by (cases q, auto)
  from assms(3) mopup_a_nth[of nat n 2]
  have "mopup_a n ! (4 * nat + 2) = mopup_a (Suc nat) ! ((4 * nat) + 2)"
    unfolding nat q by auto
  thus ?thesis using assms nat q by (auto simp: nth_append)
qed

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: 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: 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: 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: 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: 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: 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: 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: 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: 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: 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: 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 mopup_bef_erase_b_Bk_via_a_Oc[simp]: 
  "mopup_bef_erase_a (s, l, Oc # xs) lm n ires  
  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)
  by (metis cell.distinct(1) hd_append list.sel(1) list.sel(3) tl_append2 tl_replicate)

lemma mopup_false1:
  "0 < s; s  2 * n; s mod 2 = Suc 0;  ¬ Suc s  2 * n 
   RR"
  apply(arith)
  done

lemma mopup_bef_erase_a_implies_two[simp]: 
  "n < length lm; 0 < s; s  2 * n; s mod 2 = Suc 0; 
   mopup_bef_erase_a (s, l, Oc # xs) lm n ires; r = Oc # xs
  (Suc s  2 * n  mopup_bef_erase_b (Suc s, l, Bk # xs) lm n ires)  
     (¬ Suc s  2 * n  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(Suc m)
                    else Oc(Suc m) @ Bk # <lm>)"
  by(cases lm, simp_all add: tape_of_list_def  tape_of_nat_def split: if_splits)

lemma drop_tape_of_cons: 
  "Suc q < length lm; x = lm ! q  <drop q lm> = Oc # Oc  x @ Bk # <drop (Suc q) lm>"
  using Suc_lessD append_Cons list.simps(2) Cons_nth_drop_Suc replicate_Suc tape_of_nl_cons
  by metis

lemma erase2jumpover1:
  "q < length list; 
             rn. <drop q list>  Oc # Oc  (list ! q) @ Bk # <drop (Suc q) list> @ Bk  rn
        <drop q list> = Oc # Oc  (list ! q)"
  apply(erule_tac x = 0 in allE, simp)
  apply(cases "Suc q < length list")
   apply(erule_tac notE)
   apply(rule_tac drop_tape_of_cons, simp_all)
  apply(subgoal_tac "length list = Suc q", auto)
  apply(subgoal_tac "drop q list = [list ! q]")
   apply(simp add: tape_of_nat_def tape_of_list_def replicate_Suc)
  by (metis append_Nil2 append_eq_conv_conj Cons_nth_drop_Suc lessI)

lemma erase2jumpover2:
  "q < length list; rn. <drop q list> @ Bk # Bk  n 
  Oc # Oc  (list ! q) @ Bk # <drop (Suc q) list> @ Bk  rn
   RR"
  apply(cases "Suc q < length list")
   apply(erule_tac x = "Suc n" in allE, simp)
   apply(erule_tac notE, simp add: replicate_Suc)
   apply(rule_tac drop_tape_of_cons, simp_all)
  apply(subgoal_tac "length list = Suc q", auto)
  apply(erule_tac x = "n" in allE, simp add: tape_of_list_def)
  by (metis append_Nil2 append_eq_conv_conj Cons_nth_drop_Suc lessI replicate_Suc tape_of_list_def tape_of_nl_cons)

lemma mod_ex1: "(a mod 2 = Suc 0) = ( q. a = Suc (2 * q))"
  by arith

declare replicate_Suc[simp]

lemma mopup_bef_erase_a_2_jump_over[simp]:
  "n < length lm; 0 < s; s mod 2 = Suc 0;  s  2 * n;
   mopup_bef_erase_a (s, l, Bk # xs) lm n ires; ¬ (Suc (Suc s)  2 * n) 
 mopup_jump_over1 (s', Bk # l, xs) lm n ires"
proof(cases n)
  case (Suc nat)
  assume assms: "n < length lm" "0 < s" "s mod 2 = Suc 0" "s  2 * n"
    "mopup_bef_erase_a (s, l, Bk # xs) lm n ires" "¬ (Suc (Suc s)  2 * n)"
  from assms obtain a lm' where Cons:"lm = Cons a lm'" by (cases lm,auto)
  from assms have n:"Suc s div 2 = n" by auto
  have [simp]:"s = Suc (2 * q)  q = nat" for q using assms Suc by presburger
  from assms obtain ln m rn where ln:"l = Bk  ln @ Bk # Bk # ires"
    and "Bk # xs = Oc  m @ Bk # <drop (Suc s div 2) lm> @ Bk  rn"
    by (auto simp: mopup_bef_erase_a.simps mopup_jump_over1.simps)
  hence xs:"xs = <drop n lm> @ Bk  rn" by(cases m;auto simp: n mod_ex1)
  have [intro]:"nat < length lm' 
    rna. xs  Oc # Oc  (lm' ! nat) @ Bk # <drop (Suc nat) lm'> @ Bk  rna 
    <drop nat lm'> @ Bk  rn = Oc # Oc  (lm' ! nat)"
    by(cases rn, auto elim: erase2jumpover1 erase2jumpover2 simp:xs Suc Cons)
  have [intro]:"<drop nat lm'>  Oc # Oc  (lm' ! nat) @ Bk # <drop (Suc nat) lm'> @ Bk  0  length lm'  Suc nat"
    using drop_tape_of_cons[of nat lm'] by fastforce
  from assms(1,3) have [intro!]:"
            0 + Suc (lm' ! nat) = Suc (lm' ! nat) 
            Bk # Bk  ln = Oc  0 @ Bk  Suc ln 
            ((rna. xs = Oc  Suc (lm' ! nat) @ Bk # <drop (Suc nat) lm'> @ Bk  rna) 
             xs = Oc  Suc (lm' ! nat)  length lm'  Suc nat)"
    by (auto simp:Cons ln xs Suc)
  from assms(1,3) show ?thesis unfolding Cons ln Suc
    by(auto simp: mopup_bef_erase_a.simps mopup_jump_over1.simps simp del:split_head_repeat)
qed auto


lemma Suc_Suc_div:  "0 < s; s mod 2 = Suc 0; Suc (Suc s)  2 * n
            (Suc (Suc (s div 2)))  n" by(arith)

lemma mopup_bef_erase_a_2_a[simp]: 
  assumes "n < length lm" "0 < s" "s mod 2 = Suc 0" 
    "mopup_bef_erase_a (s, l, Bk # xs) lm n ires"
    "Suc (Suc s)  2 * n"
  shows "mopup_bef_erase_a (Suc (Suc s), Bk # l, xs) lm n ires"
proof-
  from assms obtain rn m ln where
    rn:"l = Bk  ln @ Bk # Bk # ires" "Bk # xs = Oc  m @ Bk # <drop (Suc s div 2) lm> @ Bk  rn"
    by (auto simp: mopup_bef_erase_a.simps)
  hence m:"m = 0" using assms by (cases m,auto)
  hence d:"drop (Suc (Suc (s div 2))) lm  []"
    using assms(1,3,5) by auto arith
  hence "Bk # l = Bk  Suc ln @ Bk # Bk # ires 
    xs = Oc  Suc (lm ! (Suc s div 2)) @ Bk # <drop ((Suc (Suc s) + 1) div 2) lm> @ Bk  rn"
    using rn by(auto intro:drop_tape_of_cons simp:m) 
  thus ?thesis unfolding mopup_bef_erase_a.simps by blast
qed

lemma mopup_false2: 
  "0 < s; s  2 * n; 
   s mod 2 = Suc 0; Suc s  2 * n;
   ¬ Suc (Suc s)  2 * n  RR"
  by(arith)

lemma ariths[simp]: "0 < s; s  2 *n; s mod 2  Suc 0  
                                      (s - Suc 0) mod 2 = Suc 0"
  "0 < s; s  2 *n; s mod 2  Suc 0 
                                       s - Suc 0  2 * n"
  "0 < s; s  2 *n; s mod 2  Suc 0  ¬ s  Suc 0"
  by(arith)+

lemma take_suc[intro]:
  "lna. Bk # Bk  ln = Bk  lna"
  by(rule_tac x = "Suc ln" in exI, simp)


lemma mopup_bef_erase[simp]: "mopup_bef_erase_a (s, l, []) lm n ires  
                        mopup_bef_erase_a (s, l, [Bk]) lm n ires"
  "n < length lm; 0 < s; s  2 * n; s mod 2 = Suc 0; ¬ Suc (Suc s)  2 *n;
     mopup_bef_erase_a (s, l, []) lm n ires
      mopup_jump_over1 (s', Bk # l, []) lm n ires"
  "mopup_bef_erase_b (s, l, Oc # xs) lm n ires  l  []"
  "n < length lm; 0 < s; s  2 * n; 
               s mod 2  Suc 0; 
               mopup_bef_erase_b (s, l, Bk # xs) lm n ires; r = Bk # xs 
            mopup_bef_erase_a (s - Suc 0, Bk # l, xs) lm n ires"
  "mopup_bef_erase_b (s, l, []) lm n ires  
                   mopup_bef_erase_a (s - Suc 0, Bk # l, []) lm n ires"
  by(auto simp: mopup_bef_erase_b.simps mopup_bef_erase_a.simps)


lemma mopup_jump_over1_in_ctx[simp]:
  assumes "mopup_jump_over1 (Suc (2 * n), l, Oc # xs) lm n ires"
  shows "mopup_jump_over1 (Suc (2 * n), Oc # l, xs) lm n ires"
proof -
  from assms obtain ln m1 m2 rn where
    "m1 + m2 = Suc (lm ! n)"
    "l = Oc  m1 @ Bk  ln @ Bk # Bk # ires"
    "(Oc # xs = Oc  m2 @ Bk # <drop (Suc n) lm> @ Bk  rn 
         Oc # xs = Oc  m2  drop (Suc n) lm = [])" unfolding mopup_jump_over1.simps by blast
  thus ?thesis unfolding 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)
    by(cases "m2", auto)
qed

lemma mopup_jump_over1_2_aft_erase_a[simp]:  
  assumes "mopup_jump_over1 (Suc (2 * n), l, Bk # xs) lm n ires"
  shows "mopup_aft_erase_a (Suc (Suc (2 * n)), Bk # l, xs) lm n ires"
proof -
  from assms obtain ln m1 m2 rn where
    "m1 + m2 = Suc (lm ! n)"
    "l = Oc  m1 @ Bk  ln @ Bk # Bk # ires"
    "(Bk # xs = Oc  m2 @ Bk # <drop (Suc n) lm> @ Bk  rn 
        Bk # xs = Oc  m2  drop (Suc n) lm = [])" unfolding mopup_jump_over1.simps by blast
  thus ?thesis unfolding mopup_aft_erase_a.simps
    apply( rule_tac x = ln in exI, rule_tac x = "Suc 0" in exI,rule_tac x = rn in exI
        , rule_tac x = "drop (Suc n) lm" in exI)
    by(cases m2, auto)
qed

lemma mopup_aft_erase_a_via_jump_over1[simp]: 
  "mopup_jump_over1 (Suc (2 * n), l, []) lm n ires  
    mopup_aft_erase_a (Suc (Suc (2 * n)), Bk # l, []) lm n ires"
proof(rule mopup_jump_over1_2_aft_erase_a)
  assume a:"mopup_jump_over1 (Suc (2 * n), l, []) lm n ires"
  then obtain ln where ln:"length lm  Suc n  l = Oc # Oc  (lm ! n) @ Bk  ln @ Bk # Bk # ires"
    unfolding mopup_jump_over1.simps by auto
  show "mopup_jump_over1 (Suc (2 * n), l, [Bk]) lm n ires"
    unfolding 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)
    using a ln by(auto simp: mopup_jump_over1.simps tape_of_list_def )
qed

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

lemma mopup_aft_erase_b_via_a[simp]: 
  assumes "mopup_aft_erase_a (Suc (Suc (2 * n)), l, Oc # xs) lm n ires"
  shows "mopup_aft_erase_b (Suc (Suc (Suc (2 * n))), l, Bk # xs) lm n ires"
proof -
  from assms obtain lnl lnr rn ml where
    assms:
    "l = Bk  lnr @ Oc  Suc (lm ! n) @ Bk  lnl @ Bk # Bk # ires"
    "Oc # xs = <ml::nat list> @ Bk  rn"
    unfolding mopup_aft_erase_a.simps by auto
  then obtain a list where ml:"ml = a # list" by (cases ml,cases rn,auto)
  with assms show ?thesis unfolding mopup_aft_erase_b.simps
    apply(auto simp add: tape_of_nl_cons split: if_splits)
     apply(cases a, simp_all)
      apply(rule_tac x = rn in exI, rule_tac x = "[]" in exI, force)
     apply(rule_tac x = rn in exI, rule_tac x = "[a-1]" in exI)
     apply(cases "a"; force simp add: tape_of_list_def tape_of_nat_def) 
    apply(cases "a")
     apply(rule_tac x = rn in exI, rule_tac x = list in exI, force)
    apply(rule_tac x = rn in exI,rule_tac x = "(a-1) # list" in exI, simp add: tape_of_nl_cons)
    done
qed

lemma mopup_left_moving_via_aft_erase_a[simp]:
  assumes "mopup_aft_erase_a (Suc (Suc (2 * n)), l, Bk # xs) lm n ires"
  shows "mopup_left_moving (5 + 2 * n, tl l, hd l # Bk # xs) lm n ires"
proof-
  from assms[unfolded mopup_aft_erase_a.simps] obtain lnl lnr rn ml where
    "l = Bk  lnr @ Oc  Suc (lm ! n) @ Bk  lnl @ Bk # Bk # ires"
    "Bk # xs = <ml::nat list> @ Bk  rn"
    by auto
  thus ?thesis unfolding mopup_left_moving.simps
    by(cases lnr;cases ml,auto simp: tape_of_nl_cons)
qed

lemma mopup_aft_erase_a_nonempty[simp]:
  "mopup_aft_erase_a (Suc (Suc (2 * n)), l, xs) lm n ires  l  []"
  by(auto simp only: mopup_aft_erase_a.simps)

lemma mopup_left_moving_via_aft_erase_a_emptylst[simp]:
  assumes "mopup_aft_erase_a (Suc (Suc (2 * n)), l, []) lm n ires"
  shows "mopup_left_moving (5 + 2 * n, tl l, [hd l]) lm n ires"
proof -
  have [intro!]:"[Bk] = Bk  1" by auto
  from assms obtain lnl lnr where "l = Bk  lnr @ Oc # Oc  (lm ! n) @ Bk  lnl @ Bk # Bk # ires"
    unfolding mopup_aft_erase_a.simps by auto
  thus ?thesis by(case_tac lnr, auto simp add:mopup_left_moving.simps)
qed

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

lemma tape_of_ex1[intro]: 
  "rna ml. Oc  a @ Bk  rn = <ml::nat list> @ Bk  rna  Oc  a @ Bk  rn = Bk # <ml> @ Bk  rna"
  by(rule_tac x = rn in exI, rule_tac x = "if a = 0 then [] else [a-1]" in exI,
      simp add: tape_of_list_def tape_of_nat_def)

lemma mopup_aft_erase_b_via_c_helper: "rna ml. Oc  a @ Bk # <list::nat list> @ Bk  rn = 
  <ml> @ Bk  rna  Oc  a @ Bk # <list> @ Bk  rn = Bk # <ml::nat list> @ Bk  rna"
  apply(cases "list = []", simp add: replicate_Suc[THEN sym] del: replicate_Suc split_head_repeat)
   apply(rule_tac rn = "Suc rn" in tape_of_ex1)
  apply(cases 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 = "(a-1) # list" in exI)
  apply(simp add: tape_of_nl_cons)
  done

lemma mopup_aft_erase_b_via_c[simp]: 
  assumes "mopup_aft_erase_c (2 * n + 4, l, Oc # xs) lm n ires"
  shows "mopup_aft_erase_b (Suc (Suc (Suc (2 * n))), l, Bk # xs) lm n ires"
proof-
  from assms obtain lnl rn lnr ml where assms:
    "l = Bk  lnr @ Oc # Oc  (lm ! n) @ Bk  lnl @ Bk # Bk # ires"
    "Oc # xs = <ml::nat list> @ Bk  rn" unfolding mopup_aft_erase_c.simps by auto
  hence "Oc # xs = Bk  rn  False" by(cases rn,auto)
  thus ?thesis using assms unfolding mopup_aft_erase_b.simps
    by(cases ml)
      (auto simp add: tape_of_nl_cons split: if_splits intro:mopup_aft_erase_b_via_c_helper
        simp del:split_head_repeat)
qed

lemma mopup_aft_erase_c_aft_erase_a[simp]: 
  assumes "mopup_aft_erase_c (2 * n + 4, l, Bk # xs) lm n ires"
  shows "mopup_aft_erase_a (Suc (Suc (2 * n)), Bk # l, xs) lm n ires"
proof -
  from assms obtain lnl lnr rn ml where
    "l = Bk  lnr @ Oc  Suc (lm ! n) @ Bk  lnl @ Bk # Bk # ires"
    "(Bk # xs = <ml::nat list> @ Bk  rn  Bk # xs = Bk # <ml> @ Bk  rn)"
    unfolding mopup_aft_erase_c.simps by auto
  thus ?thesis unfolding mopup_aft_erase_a.simps
    apply(clarify)
    apply(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 (insert tape_of_list_empty,blast)
     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)
    apply(rule_tac x = rn in exI, rule_tac x = "ml" in exI, simp)
    done
qed

lemma mopup_aft_erase_a_via_c[simp]: 
  "mopup_aft_erase_c (2 * n + 4, l, []) lm n ires 
  mopup_aft_erase_a (Suc (Suc (2 * n)), Bk # l, []) lm n ires"
  by (rule mopup_aft_erase_c_aft_erase_a)
    (auto simp:mopup_aft_erase_c.simps)

lemma mopup_aft_erase_b_2_aft_erase_c[simp]:
  assumes "mopup_aft_erase_b (2 * n + 3, l, Bk # xs) lm n ires"
  shows "mopup_aft_erase_c (4 + 2 * n, Bk # l, xs) lm n ires"
proof -
  from assms obtain lnl lnr ml rn where
    "l = Bk  lnr @ Oc  Suc (lm ! n) @ Bk  lnl @ Bk # Bk # ires"
    "Bk # xs = Bk # <ml::nat list> @ Bk  rn  Bk # xs = Bk # Bk # <ml> @ Bk  rn"
    unfolding  mopup_aft_erase_b.simps by auto
  thus ?thesis unfolding mopup_aft_erase_c.simps
    by (rule_tac x = "lnl" in exI) auto
qed

lemma mopup_aft_erase_c_via_b[simp]: 
  "mopup_aft_erase_b (2 * n + 3, l, []) lm n ires 
  mopup_aft_erase_c (4 + 2 * n, Bk # l, []) lm n ires"
  by(auto simp add: mopup_aft_erase_b.simps intro:mopup_aft_erase_b_2_aft_erase_c)

lemma mopup_left_moving_nonempty[simp]: 
  "mopup_left_moving (2 * n + 5, l, Oc # xs) lm n ires  l  []"
  by(auto simp: mopup_left_moving.simps)

lemma exp_ind: "a(Suc x) = ax @ [a]"
  by(induct x, auto)

lemma mopup_jump_over2_via_left_moving[simp]:  
  "mopup_left_moving (2 * n + 5, l, Oc # xs) lm n ires
   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 (simp add: Cons_replicate_eq)
  apply(rename_tac Lnl lnr rn m)
  apply(cases "hd l", simp add:  )
   apply(cases "lm ! n", simp)
    apply(rule exI, rule_tac x = "length xs" 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(cases "lm ! n", simp)
   apply(case_tac Lnl, simp, simp)
  apply(rule_tac x = Lnl in exI, rule_tac x = "length xs" in exI, auto)
  apply(cases "lm ! n", simp)
   apply(case_tac Lnl, simp_all add: numeral_2_eq_2)
  done

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

lemma mopup_left_moving_hd_Bk[simp]:
  "mopup_left_moving (2 * n + 5, l, Bk # xs) lm n ires 
  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(rename_tac lnl Lnr rn m)
  apply(case_tac Lnr, auto)
  done

lemma mopup_left_moving_emptylist[simp]: 
  "mopup_left_moving (2 * n + 5, l, []) lm n ires
     mopup_left_moving (2 * n + 5, tl l, [hd l]) lm n ires"
  apply(simp only: mopup_left_moving.simps)
  apply(erule exE)+ apply(rename_tac lnl Lnr rn m)
  apply(case_tac Lnr, auto)
  apply(rule_tac x = 1 in exI, simp)
  done


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

lemma mopup_jump_over2_context[simp]: 
  "mopup_jump_over2 (2 * n + 6, l, Oc # xs) lm n ires
   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, erule conjE, erule_tac conjE)
  apply(rename_tac Ln Rn M1 M2)
  apply(case_tac M1, simp)
   apply(rule_tac x = Ln in exI, rule_tac x = Rn in exI, 
      rule_tac x = 0 in exI)
   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 = "M1-1" in exI, rule_tac x = "Suc M2" in exI, simp)
  done

lemma mopup_stop_via_jump_over2[simp]: 
  "mopup_jump_over2 (2 * n + 6, l, Bk # xs) lm n ires 
   mopup_stop (0, Bk # l, xs) lm n ires"
  apply(auto simp: mopup_jump_over2.simps mopup_stop.simps tape_of_nat_def)
  apply(simp add: exp_ind[THEN sym])
  done

lemma mopup_jump_over2_nonempty[simp]: "mopup_jump_over2 (2 * n + 6, l, []) lm n ires = False"
  by(auto simp: mopup_jump_over2.simps)

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

lemma mod_2: "x mod 2  = 0   x mod 2 = Suc 0"
  by arith


lemma mopup_inv_step:
  "n < length lm; mopup_inv (s, l, r) lm n ires
   mopup_inv (step (s, l, r) (mopup_a n @ shift mopup_b (2 * n), 0)) lm n ires"
  apply(cases r;cases "hd r")
     apply(auto split:if_splits simp add:step.simps mopupfetchs fetch.simps(1))
      apply(drule_tac mopup_false2, simp_all add: mopup_bef_erase_b.simps)
    apply(drule_tac mopup_false2, simp_all)
   apply(drule_tac mopup_false2, simp_all)
  by presburger

declare mopup_inv.simps[simp del]
lemma mopup_inv_steps: 
  "n < length lm; mopup_inv (s, l, r) lm n ires  
     mopup_inv (steps (s, l, r) (mopup_a n @ shift mopup_b (2 * n), 0)  stp) lm n ires"
proof(induct stp)
  case (Suc stp)
  then show ?case 
    by ( cases "steps (s, l, r) 
                (mopup_a n @ shift mopup_b (2 * n), 0) stp"
        , auto simp add: steps.simps intro:mopup_inv_step)
qed (auto simp add: steps.simps)

fun abc_mopup_stage1 :: "config  nat  nat"
  where
    "abc_mopup_stage1 (s, l, r) n = 
           (if s > 0  s  2*n then 6
            else if s = 2*n + 1 then 4
            else if s  2*n + 2  s  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  nat  nat"
  where
    "abc_mopup_stage2 (s, l, r) n = 
           (if s > 0  s  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  2*n + 2  s  2*n + 4 then length r
            else 0)"

fun abc_mopup_stage3 :: "config  nat  nat"
  where
    "abc_mopup_stage3 (s, l, r) n = 
          (if s > 0  s  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 [λ(c, n). abc_mopup_stage1 c n, 
                                 λ(c, n). abc_mopup_stage2 c n, 
                                 λ(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]: 
  "n. ¬ P (f n)  (f (Suc n), (f n))  abc_mopup_measure  n. P (f n)"
  using wf_abc_mopup_measure
  by (metis wf_iff_no_infinite_down_chain)

lemma mopup_erase_nonempty[simp]:
  "mopup_bef_erase_a (a, aa, []) lm n ires = False"
  "mopup_bef_erase_b (a, aa, []) lm n ires = False"
  "mopup_aft_erase_b (2 * n + 3, aa, []) lm n ires = False"
  by(auto simp: mopup_bef_erase_a.simps mopup_bef_erase_b.simps mopup_aft_erase_b.simps)

declare mopup_inv.simps[simp del]

lemma fetch_mopup_a_shift[simp]: 
  assumes "0 < q" "q  n"
  shows "fetch (mopup_a n @ shift mopup_b (2 * n)) (2*q) Bk = (R, 2*q - 1)"
proof(cases q)
  case (Suc nat) with assms
  have "mopup_a n ! (4 * nat + 2) = mopup_a (Suc nat) ! ((4 * nat) + 2)" using assms
    by (metis Suc_le_lessD add_2_eq_Suc' less_Suc_eq mopup_a_nth numeral_Bit0)
  then show ?thesis using assms Suc
    by(auto simp: fetch.simps nth_of.simps nth_append)
qed (insert assms,auto)

lemma mopup_halt:
  assumes 
    less: "n < length lm"
    and inv: "mopup_inv (Suc 0, l, r) lm n ires"
    and f: "f = (λ stp. (steps (Suc 0, l, r) (mopup_a n @ shift mopup_b (2 * n), 0) stp, n))"
    and P: "P = (λ (c, n). is_final c)"
  shows " stp. P (f stp)"
proof (induct rule: abc_mopup_measure_induct) 
  case (Step na)
  have h: "¬ P (f na)" by fact
  show "(f (Suc na), f na)  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)  abc_mopup_measure"
      apply(case_tac c;cases "hd c")
         apply(auto split:if_splits simp add:step.simps mopup_inv.simps mopup_bef_erase_b.simps)
      by (auto split:if_splits simp: mopupfetchs abc_mopup_measure_def )
    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)
       abc_mopup_measure"
      using g by simp
  qed
qed

lemma mopup_inv_start: 
  "n < length am  mopup_inv (Suc 0, Bk # Bk # ires, <am> @ Bk  k) am n ires"
  apply(cases am;auto simp: mopup_inv.simps mopup_bef_erase_a.simps mopup_jump_over1.simps)
    apply(auto simp: tape_of_nl_cons)
     apply(rule_tac x = "Suc (hd am)" in exI, rule_tac x = k in exI, simp)
    apply(cases k;cases n;force)
   apply(cases n; force)
  by(cases n; force split:if_splits)

lemma mopup_correct:
  assumes less: "n < length (am::nat list)"
    and rs: "am ! n = rs"
  shows " stp i j. (steps (Suc 0, Bk # Bk # ires, <am> @ Bk  k) (mopup_a n @ shift mopup_b (2 * n), 0) stp)
    = (0, Bki @ Bk # Bk # ires, Oc # Oc rs @ Bkj)"
  using less
proof -
  have a: "mopup_inv (Suc 0, Bk # Bk # ires, <am> @ Bk  k) am n ires"
    using less
    apply(simp add: mopup_inv_start)
    done    
  then have " stp. is_final (steps (Suc 0, Bk # Bk # ires, <am> @ Bk  k) (mopup_a n @ shift mopup_b (2 * n), 0) stp)"
    using less mopup_halt[of n am  "Bk # Bk # ires" "<am> @ Bk  k" ires
        "(λstp. (steps (Suc 0, Bk # Bk # ires, <am> @ Bk  k) (mopup_a n @ shift mopup_b (2 * n), 0) stp, n))"
        "(λ(c, n). is_final c)"]
    apply(simp)
    done
  from this obtain stp where b:
    "is_final (steps (Suc 0, Bk # Bk # ires, <am> @ Bk  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  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  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_def)
    done
qed

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

end

Theory Abacus

(* Title: thys/Abacus.thy
   Author: Jian Xu, Xingyuan Zhang, and Christian Urban
   Modifications: Sebastiaan Joosten
*)

chapter ‹Abacus Machines›

theory Abacus
  imports Turing_Hoare Abacus_Mopup
begin

declare replicate_Suc[simp add]

(* Abacus instructions *)

datatype abc_inst =
  Inc nat
  | Dec nat nat
  | Goto nat

type_synonym abc_prog = "abc_inst list"

type_synonym abc_state = nat

text ‹
  The memory of Abacus machine is defined as a list of contents, with 
  every units addressed by index into the list.
›
type_synonym abc_lm = "nat list"

text ‹
  Fetching contents out of memory. Units not represented by list elements are considered
  as having content 0›.
›
fun abc_lm_v :: "abc_lm  nat  nat"
  where 
    "abc_lm_v lm n = (if (n < length lm) then (lm!n) else 0)"         


text ‹
  Set the content of memory unit n› to value v›.
  am› is the Abacus memory before setting.
  If address n› is outside to scope of am›, am› 
  is extended so that n› becomes in scope.
›

fun abc_lm_s :: "abc_lm  nat  nat  abc_lm"
  where
    "abc_lm_s am n v = (if (n < length am) then (am[n:=v]) else 
                           am@ (replicate (n - length am) 0) @ [v])"


text ‹
  The configuration of Abaucs machines consists of its current state and its
  current memory:
›
type_synonym abc_conf = "abc_state × abc_lm"

text ‹
  Fetch instruction out of Abacus program:
›

fun abc_fetch :: "nat  abc_prog  abc_inst option" 
  where
    "abc_fetch s p = (if (s < length p) then Some (p ! s) else None)"

text ‹
  Single step execution of Abacus machine. If no instruction is feteched, 
  configuration does not change.
›
fun abc_step_l :: "abc_conf  abc_inst option  abc_conf"
  where
    "abc_step_l (s, lm) a = (case a of 
               None  (s, lm) |
               Some (Inc n)   (let nv = abc_lm_v lm n in
                       (s + 1, abc_lm_s lm n (nv + 1))) |
               Some (Dec n e)  (let nv = abc_lm_v lm n in
                       if (nv = 0) then (e, abc_lm_s lm n 0) 
                       else (s + 1,  abc_lm_s lm n (nv - 1))) |
               Some (Goto n)  (n, lm) 
               )"

text ‹
  Multi-step execution of Abacus machine.
›
fun abc_steps_l :: "abc_conf  abc_prog  nat  abc_conf"
  where
    "abc_steps_l (s, lm) p 0 = (s, lm)" |
    "abc_steps_l (s, lm) p (Suc n) = 
      abc_steps_l (abc_step_l (s, lm) (abc_fetch s p)) p n"

section ‹
  Compiling Abacus machines into Turing machines
›

subsection ‹
  Compiling functions
›

text findnth n› returns the TM which locates the represention of
  memory cell n› on the tape and changes representation of zero
  on the way.
›

fun findnth :: "nat  instr list"
  where
    "findnth 0 = []" |
    "findnth (Suc n) = (findnth n @ [(W1, 2 * n + 1), 
           (R, 2 * n + 2), (R, 2 * n + 3), (R, 2 * n + 2)])"

text tinc_b› returns the TM which increments the representation 
  of the memory cell under rw-head by one and move the representation 
  of cells afterwards to the right accordingly.
›

definition tinc_b :: "instr list"
  where
    "tinc_b  [(W1, 1), (R, 2), (W1, 3), (R, 2), (W1, 3), (R, 4), 
             (L, 7), (W0, 5), (R, 6), (W0, 5), (W1, 3), (R, 6),
             (L, 8), (L, 7), (R, 9), (L, 7), (R, 10), (W0, 9)]" 

text tinc ss n› returns the TM which simulates the execution of 
  Abacus instruction Inc n›, assuming that TM is located at
  location ss› in the final TM complied from the whole
  Abacus program.
›

fun tinc :: "nat  nat  instr list"
  where
    "tinc ss n = shift (findnth n @ shift tinc_b (2 * n)) (ss - 1)"

text tinc_b› returns the TM which decrements the representation 
  of the memory cell under rw-head by one and move the representation 
  of cells afterwards to the left accordingly.
›

definition tdec_b :: "instr list"
  where
    "tdec_b   [(W1, 1), (R, 2), (L, 14), (R, 3), (L, 4), (R, 3),
              (R, 5), (W0, 4), (R, 6), (W0, 5), (L, 7), (L, 8),
              (L, 11), (W0, 7), (W1, 8), (R, 9), (L, 10), (R, 9),
              (R, 5), (W0, 10), (L, 12), (L, 11), (R, 13), (L, 11),
              (R, 17), (W0, 13), (L, 15), (L, 14), (R, 16), (L, 14),
              (R, 0), (W0, 16)]"


text tdec ss n label› returns the TM which simulates the execution of 
  Abacus instruction Dec n label›, assuming that TM is located at
  location ss› in the final TM complied from the whole
  Abacus program.
›

fun tdec :: "nat  nat  nat  instr list"
  where
    "tdec ss n e = shift (findnth n) (ss - 1) @ adjust (shift (shift tdec_b (2 * n)) (ss - 1)) e"

text tgoto f(label)› returns the TM simulating the execution of Abacus instruction
  Goto label›, where f(label)› is the corresponding location of
  label› in the final TM compiled from the overall Abacus program.
›

fun tgoto :: "nat  instr list"
  where
    "tgoto n = [(Nop, n), (Nop, n)]"

text ‹
  The layout of the final TM compiled from an Abacus program is represented
  as a list of natural numbers, where the list element at index n› represents the 
  starting state of the TM simulating the execution of n›-th instruction
  in the Abacus program.
›

type_synonym layout = "nat list"

text length_of i› is the length of the 
  TM simulating the Abacus instruction i›.
›
fun length_of :: "abc_inst  nat"
  where
    "length_of i = (case i of 
                    Inc n    2 * n + 9 |
                    Dec n e  2 * n + 16 |
                    Goto n   1)"

text layout_of ap› returns the layout of Abacus program ap›.
›
fun layout_of :: "abc_prog  layout"
  where "layout_of ap = map length_of ap"


text start_of layout n› looks out the starting state of n›-th
  TM in the finall TM.
›

fun start_of :: "nat list  nat  nat"
  where
    "start_of ly x = (Suc (sum_list (take x ly))) "

text ci lo ss i› complies Abacus instruction i›
  assuming the TM of i› starts from state ss› 
  within the overal layout lo›.
›

fun ci :: "layout  nat  abc_inst  instr list"
  where
    "ci ly ss (Inc n) = tinc ss n"
  | "ci ly ss (Dec n e) = tdec ss n (start_of ly e)"
  | "ci ly ss (Goto n) = tgoto (start_of ly n)"

text tpairs_of ap› transfroms Abacus program ap› pairing
  every instruction with its starting state.
›

fun tpairs_of :: "abc_prog  (nat × abc_inst) list"
  where "tpairs_of ap = (zip (map (start_of (layout_of ap)) 
                         [0..<(length ap)]) ap)"

text tms_of ap› returns the list of TMs, where every one of them simulates
  the corresponding Abacus intruction in ap›.
›

fun tms_of :: "abc_prog  (instr list) list"
  where "tms_of ap = map (λ (n, tm). ci (layout_of ap) n tm) 
                         (tpairs_of ap)"

text tm_of ap› returns the final TM machine compiled from Abacus program ap›.
›
fun tm_of :: "abc_prog  instr list"
  where "tm_of ap = concat (tms_of ap)"

lemma length_findnth: 
  "length (findnth n) = 4 * n"
  by (induct n, auto)

lemma ci_length : "length (ci ns n ai) div 2 = length_of ai"
  apply(auto simp: ci.simps tinc_b_def tdec_b_def length_findnth
      split: abc_inst.splits simp del: adjust.simps)
  done

subsection ‹Representation of Abacus memory by TM tapes›

text crsp acf tcf› meams the abacus configuration acf›
  is corretly represented by the TM configuration tcf›.
›

fun crsp :: "layout  abc_conf  config  cell list  bool"
  where 
    "crsp ly (as, lm) (s, l, r) inres = 
           (s = start_of ly as  ( x. r = <lm> @ Bkx)  
            l = Bk # Bk # inres)"

declare crsp.simps[simp del]

text ‹
  The type of invarints expressing correspondence between 
  Abacus configuration and TM configuration.
›

type_synonym inc_inv_t = "abc_conf  config  cell list  bool"

declare tms_of.simps[simp del] tm_of.simps[simp del]
  layout_of.simps[simp del] abc_fetch.simps [simp del]  
  tpairs_of.simps[simp del] start_of.simps[simp del]
  ci.simps [simp del] length_of.simps[simp del] 
  layout_of.simps[simp del]

text ‹
  The lemmas in this section lead to the correctness of 
  the compilation of Inc n› instruction.
›

declare abc_step_l.simps[simp del] abc_steps_l.simps[simp del]
lemma start_of_nonzero[simp]: "start_of ly as > 0" "(start_of ly as = 0) = False"
   apply(auto simp: start_of.simps)
  done

lemma abc_steps_l_0: "abc_steps_l ac ap 0 = ac"
  by(cases ac, simp add: abc_steps_l.simps)

lemma abc_step_red: 
  "abc_steps_l (as, am) ap stp = (bs, bm)  
  abc_steps_l (as, am) ap (Suc stp) = abc_step_l (bs, bm) (abc_fetch bs ap) "
proof(induct stp arbitrary: as am bs bm)
  case 0
  thus "?case"
    by(simp add: abc_steps_l.simps abc_steps_l_0)
next
  case (Suc stp as am bs bm)
  have ind: "as am bs bm. abc_steps_l (as, am) ap stp = (bs, bm)  
    abc_steps_l (as, am) ap (Suc stp) = abc_step_l (bs, bm) (abc_fetch bs ap)"
    by fact
  have h:" abc_steps_l (as, am) ap (Suc stp) = (bs, bm)" by fact
  obtain as' am' where g: "abc_step_l (as, am) (abc_fetch as ap) = (as', am')"
    by(cases "abc_step_l (as, am) (abc_fetch as ap)", auto)
  then have "abc_steps_l (as', am') ap (Suc stp) = abc_step_l (bs, bm) (abc_fetch bs ap)"
    using h
    by(intro ind, simp add: abc_steps_l.simps)
  thus "?case"
    using g
    by(simp add: abc_steps_l.simps)
qed

lemma tm_shift_fetch: 
  "fetch A s b = (ac, ns); ns  0 
   fetch (shift A off) s b = (ac, ns + off)"
  apply(cases b;cases s)
     apply(auto simp: fetch.simps shift.simps)
  done

lemma tm_shift_eq_step:
  assumes exec: "step (s, l, r) (A, 0) = (s', l', r')"
    and notfinal: "s'  0"
  shows "step (s + off, l, r) (shift A off, off) = (s' + off, l', r')"
  using assms
  apply(simp add: step.simps)
  apply(cases "fetch A s (read r)", auto)
   apply(drule_tac [!] off = off in tm_shift_fetch, simp_all)
  done

declare step.simps[simp del] steps.simps[simp del] shift.simps[simp del]

lemma tm_shift_eq_steps: 
  assumes exec: "steps (s, l, r) (A, 0) stp = (s', l', r')"
    and notfinal: "s'  0"
  shows "steps (s + off, l, r) (shift A off, off) stp = (s' + off, l', r')"
  using exec notfinal
proof(induct stp arbitrary: s' l' r', simp add: steps.simps)
  fix stp s' l' r'
  assume ind: "s' l' r'. steps (s, l, r) (A, 0) stp = (s', l', r'); s'  0 
      steps (s + off, l, r) (shift A off, off) stp = (s' + off, l', r')"
    and h: " steps (s, l, r) (A, 0) (Suc stp) = (s', l', r')" "s'  0"
  obtain s1 l1 r1 where g: "steps (s, l, r) (A, 0) stp = (s1, l1, r1)" 
    apply(cases "steps (s, l, r) (A, 0) stp") by blast
  moreover then have "s1  0"
    using h
    apply(simp add: step_red)
    apply(cases "0 < s1", auto)
    done
  ultimately have "steps (s + off, l, r) (shift A off, off) stp =
                   (s1 + off, l1, r1)"
    apply(intro ind, simp_all)
    done
  thus "steps (s + off, l, r) (shift A off, off) (Suc stp) = (s' + off, l', r')"
    using h g assms
    apply(simp add: step_red)
    apply(intro tm_shift_eq_step, auto)
    done
qed

lemma startof_ge1[simp]: "Suc 0  start_of ly as"
  apply(simp add: start_of.simps)
  done

lemma start_of_Suc1: "ly = layout_of ap; 
       abc_fetch as ap = Some (Inc n)
        start_of ly (Suc as) = start_of ly as + 2 * n + 9"
  apply(auto simp: start_of.simps layout_of.simps  
      length_of.simps abc_fetch.simps 
      take_Suc_conv_app_nth split: if_splits)
  done

lemma start_of_Suc2:
  "ly = layout_of ap;
  abc_fetch as ap = Some (Dec n e)  
        start_of ly (Suc as) = 
            start_of ly as + 2 * n + 16"
  apply(auto simp: start_of.simps layout_of.simps  
      length_of.simps abc_fetch.simps 
      take_Suc_conv_app_nth split: if_splits)
  done

lemma start_of_Suc3:
  "ly = layout_of ap;
  abc_fetch as ap = Some (Goto n)  
  start_of ly (Suc as) = start_of ly as + 1"
  apply(auto simp: start_of.simps layout_of.simps  
      length_of.simps abc_fetch.simps 
      take_Suc_conv_app_nth split: if_splits)
  done

lemma length_ci_inc: 
  "length (ci ly ss (Inc n)) = 4*n + 18"
  apply(auto simp: ci.simps length_findnth tinc_b_def)
  done

lemma length_ci_dec: 
  "length (ci ly ss (Dec n e)) = 4*n + 32"
  apply(auto simp: ci.simps length_findnth tdec_b_def)
  done

lemma length_ci_goto: 
  "length (ci ly ss (Goto n )) = 2"
  apply(auto simp: ci.simps length_findnth tdec_b_def)
  done

lemma take_Suc_last[elim]: "Suc as  length xs  
            take (Suc as) xs = take as xs @ [xs ! as]"
proof(induct xs arbitrary: as)
  case (Cons a xs)
  then show ?case by ( simp, cases as;simp)
qed simp

lemma concat_suc: "Suc as  length xs  
       concat (take (Suc as) xs) = concat (take as xs) @ xs! as"
  apply(subgoal_tac "take (Suc as) xs = take as xs @ [xs ! as]", simp)
  by auto

lemma concat_drop_suc_iff: 
  "Suc n < length tps  concat (drop (Suc n) tps) = 
           tps ! Suc n @ concat (drop (Suc (Suc n)) tps)"
proof(induct tps arbitrary: n)
  case (Cons a tps)
  then show ?case 
    apply(cases tps, simp, simp)
    apply(cases n, simp, simp)
    done
qed simp

declare append_assoc[simp del]

lemma  tm_append:
  "n < length tps; tp = tps ! n  
   tp1 tp2. concat tps = tp1 @ tp @ tp2  tp1 = 
  concat (take n tps)  tp2 = concat (drop (Suc n) tps)"
  apply(rule_tac x = "concat (take n tps)" in exI)
  apply(rule_tac x = "concat (drop (Suc n) tps)" in exI)
  apply(auto)
proof(induct n)
  case 0
  then show ?case by(cases tps; simp)
next
  case (Suc n)
  then show ?case 
    apply(subgoal_tac "concat (take n tps) @ (tps ! n) = 
               concat (take (Suc n) tps)")
     apply(simp only: append_assoc[THEN sym], simp only: append_assoc)
     apply(subgoal_tac " concat (drop (Suc n) tps) = tps ! Suc n @ 
                  concat (drop (Suc (Suc n)) tps)")
      apply (metis append_take_drop_id concat_append)
     apply(rule concat_drop_suc_iff,force)
    by (simp add: concat_suc)
qed

declare append_assoc[simp]

lemma length_tms_of[simp]: "length (tms_of aprog) = length aprog"
  apply(auto simp: tms_of.simps tpairs_of.simps)
  done

lemma ci_nth: 
  "ly = layout_of aprog; 
  abc_fetch as aprog = Some ins
   ci ly (start_of ly as) ins = tms_of aprog ! as"
  apply(simp add: tms_of.simps tpairs_of.simps 
      abc_fetch.simps del: map_append split: if_splits)
  done

lemma t_split:"
        ly = layout_of aprog;
        abc_fetch as aprog = Some ins
        tp1 tp2. concat (tms_of aprog) = 
            tp1 @ (ci ly (start_of ly as) ins) @ tp2
             tp1 = concat (take as (tms_of aprog))  
              tp2 = concat (drop (Suc as) (tms_of aprog))"
  apply(insert tm_append[of "as" "tms_of aprog" 
        "ci ly (start_of ly as) ins"], simp)
  apply(subgoal_tac "ci ly (start_of ly as) ins = (tms_of aprog) ! as")
   apply(subgoal_tac "length (tms_of aprog) = length aprog")
    apply(simp add: abc_fetch.simps split: if_splits, simp)
  apply(intro ci_nth, auto)
  done

lemma div_apart: "x mod (2::nat) = 0; y mod 2 = 0 
           (x + y) div 2 = x div 2 + y div 2"
  by(auto)

lemma length_layout_of[simp]: "length (layout_of aprog) = length aprog"
  by(auto simp: layout_of.simps)

lemma length_tms_of_elem_even[intro]:  "n < length ap  length (tms_of ap ! n) mod 2 = 0"
  apply(cases "ap ! n")
  by (auto simp: tms_of.simps tpairs_of.simps ci.simps length_findnth tinc_b_def tdec_b_def)

lemma compile_mod2: "length (concat (take n (tms_of ap))) mod 2 = 0"
proof(induct n)
  case 0
  then show ?case by (auto simp add: take_Suc_conv_app_nth)
next
  case (Suc n)
  hence "n < length (tms_of ap)  is_even (length (concat (take (Suc n) (tms_of ap))))"
    unfolding take_Suc_conv_app_nth by fastforce
  with Suc show ?case by(cases "n < length (tms_of ap)", auto)
qed

lemma tpa_states:
  "tp = concat (take as (tms_of ap));
  as  length ap  
  start_of (layout_of ap) as = Suc (length tp div 2)"
proof(induct as arbitrary: tp)
  case 0
  thus "?case"
    by(simp add: start_of.simps)
next
  case (Suc as tp)
  have ind: "tp. tp = concat (take as (tms_of ap)); as  length ap 
    start_of (layout_of ap) as = Suc (length tp div 2)" by fact
  have tp: "tp = concat (take (Suc as) (tms_of ap))" by fact
  have le: "Suc as  length ap" by fact
  have a: "start_of (layout_of ap) as = Suc (length (concat (take as (tms_of ap))) div 2)"
    using le
    by(intro ind, simp_all)
  from a tp le show "?case"
    apply(simp add: start_of.simps take_Suc_conv_app_nth)
    apply(subgoal_tac "length (concat (take as (tms_of ap))) mod 2= 0")
     apply(subgoal_tac " length (tms_of ap ! as) mod 2 = 0")
      apply(simp add: Abacus.div_apart) 
      apply(simp add: layout_of.simps ci_length  tms_of.simps tpairs_of.simps)
     apply(auto  intro: compile_mod2)
    done
qed

declare fetch.simps[simp]
lemma append_append_fetch: 
  "length tp1 mod 2 = 0; length tp mod 2 = 0;
      length tp1 div 2 < a  a  length tp1 div 2 + length tp div 2
    fetch (tp1 @ tp @ tp2) a b = fetch tp (a - length tp1 div 2) b "
  apply(subgoal_tac " x. a = length tp1 div 2 + x", erule exE)
   apply(rename_tac x)
   apply(case_tac x, simp)
   apply(subgoal_tac "length tp1 div 2 + Suc nat = 
             Suc (length tp1 div 2 + nat)")
    apply(simp only: fetch.simps nth_of.simps, auto)
   apply(cases b, simp)
    apply(subgoal_tac "2 * (length tp1 div 2) = length tp1", simp)
     apply(subgoal_tac "2 * nat < length tp", simp add: nth_append, simp)
    apply(subgoal_tac "2 * (length tp1 div 2) = length tp1", simp)
    apply(subgoal_tac "2 * nat < length tp", simp add: nth_append, auto)
   apply(auto simp: nth_append)
  apply(rule_tac x = "a - length tp1 div 2" in exI, simp)
  done

lemma step_eq_fetch':
  assumes layout: "ly = layout_of ap"
    and compile: "tp = tm_of ap"
    and fetch: "abc_fetch as ap = Some ins"
    and range1: "s  start_of ly as"
    and range2: "s < start_of ly (Suc as)"
  shows "fetch tp s b = fetch (ci ly (start_of ly as) ins)
       (Suc s - start_of ly as) b "
proof -
  have "tp1 tp2. concat (tms_of ap) = tp1 @ ci ly (start_of ly as) ins @ tp2 
    tp1 = concat (take as (tms_of ap))  tp2 = concat (drop (Suc as) (tms_of ap))"
    using assms
    by(intro t_split, simp_all)
  then obtain tp1 tp2 where a: "concat (tms_of ap) = tp1 @ ci ly (start_of ly as) ins @ tp2 
    tp1 = concat (take as (tms_of ap))  tp2 = concat (drop (Suc as) (tms_of ap))" by blast
  then have b: "start_of (layout_of ap) as = Suc (length tp1 div 2)"
    using fetch
    by(intro tpa_states, simp, simp add: abc_fetch.simps split: if_splits)
  have "fetch (tp1 @ (ci ly (start_of ly as) ins) @ tp2)  s b = 
        fetch (ci ly (start_of ly as) ins) (s - length tp1 div 2) b"
  proof(intro append_append_fetch)
    show "length tp1 mod 2 = 0"
      using a
      by(auto, rule_tac compile_mod2)
  next
    show "length (ci ly (start_of ly as) ins) mod 2 = 0"
      by(cases ins, auto simp: ci.simps length_findnth tinc_b_def tdec_b_def)
  next
    show "length tp1 div 2 < s  s  
      length tp1 div 2 + length (ci ly (start_of ly as) ins) div 2"
    proof -
      have "length (ci ly (start_of ly as) ins) div 2 = length_of ins"
        using ci_length by simp
      moreover have "start_of ly (Suc as) = start_of ly as + length_of ins"
        using fetch layout
        apply(simp add: start_of.simps abc_fetch.simps List.take_Suc_conv_app_nth 
            split: if_splits)
        apply(simp add: layout_of.simps)
        done
      ultimately show "?thesis"
        using b layout range1 range2
        apply(simp)
        done
    qed
  qed
  thus "?thesis"
    using b layout a compile  
    apply(simp add: tm_of.simps)
    done
qed

lemma step_eq_fetch: 
  assumes layout: "ly = layout_of ap"
    and compile: "tp = tm_of ap"
    and abc_fetch: "abc_fetch as ap = Some ins" 
    and fetch: "fetch (ci ly (start_of ly as) ins)
       (Suc s - start_of ly as) b = (ac, ns)"
    and notfinal: "ns  0"
  shows "fetch tp s b = (ac, ns)"
proof -
  have "s  start_of ly as"
  proof(cases "s  start_of ly as")
    case True thus "?thesis" by simp
  next
    case False 
    have "¬ start_of ly as  s" by fact
    then have "Suc s - start_of ly as = 0"
      by arith
    then have "fetch (ci ly (start_of ly as) ins)
       (Suc s - start_of ly as) b = (Nop, 0)"
      by(simp add: fetch.simps)
    with notfinal fetch show "?thesis"
      by(simp)
  qed
  moreover have "s < start_of ly (Suc as)"
  proof(cases "s < start_of ly (Suc as)")
    case True thus "?thesis" by simp
  next
    case False
    have h: "¬ s < start_of ly (Suc as)"
      by fact
    then have "s > start_of ly as"
      using abc_fetch layout
      apply(simp add: start_of.simps abc_fetch.simps split: if_splits)
      apply(simp add: List.take_Suc_conv_app_nth, auto)
      apply(subgoal_tac "layout_of ap ! as > 0") 
       apply arith
      apply(simp add: layout_of.simps)
      apply(cases "ap!as", auto simp: length_of.simps)
      done
    from this and h have "fetch (ci ly (start_of ly as) ins) (Suc s - start_of ly as) b = (Nop, 0)"
      using abc_fetch layout
      apply(cases b;cases ins)
           apply(simp_all add:Suc_diff_le start_of_Suc2 start_of_Suc1 start_of_Suc3)
      by (simp_all only: length_ci_inc length_ci_dec length_ci_goto, auto)
    from fetch and notfinal this show "?thesis"by simp
  qed
  ultimately show "?thesis"
    using assms
    by(drule_tac b= b and ins = ins in step_eq_fetch', auto)
qed


lemma step_eq_in:
  assumes layout: "ly = layout_of ap"
    and compile: "tp = tm_of ap"
    and fetch: "abc_fetch as ap = Some ins"    
    and exec: "step (s, l, r) (ci ly (start_of ly as) ins, start_of ly as - 1) 
  = (s', l', r')"
    and notfinal: "s'  0"
  shows "step (s, l, r) (tp, 0) = (s', l', r')"
  using assms
  apply(simp add: step.simps)
  apply(cases "fetch (ci (layout_of ap) (start_of (layout_of ap) as) ins)
    (Suc s - start_of (layout_of ap) as) (read r)", simp)
  using layout
  apply(drule_tac s = s and b = "read r" and ac = a in step_eq_fetch, auto)
  done

lemma steps_eq_in:
  assumes layout: "ly = layout_of ap"
    and compile: "tp = tm_of ap"
    and crsp: "crsp ly (as, lm) (s, l, r) ires"
    and fetch: "abc_fetch as ap = Some ins"    
    and exec: "steps (s, l, r) (ci ly (start_of ly as) ins, start_of ly as - 1) stp 
  = (s', l', r')"
    and notfinal: "s'  0"
  shows "steps (s, l, r) (tp, 0) stp = (s', l', r')"
  using exec notfinal
proof(induct stp arbitrary: s' l' r', simp add: steps.simps)
  fix stp s' l' r'
  assume ind: 
    "s' l' r'. steps (s, l, r) (ci ly (start_of ly as) ins, start_of ly as - 1) stp = (s', l', r'); s'  0
               steps (s, l, r) (tp, 0) stp = (s', l', r')"
    and h: "steps (s, l, r) (ci ly (start_of ly as) ins, start_of ly as - 1) (Suc stp) = (s', l', r')" "s'  0"
  obtain s1 l1 r1 where g: "steps (s, l, r) (ci ly (start_of ly as) ins, start_of ly as - 1) stp = 
                        (s1, l1, r1)"
    apply(cases "steps (s, l, r) (ci ly (start_of ly as) ins, start_of ly as - 1) stp") by blast
  moreover hence "s1  0"
    using h
    apply(simp add: step_red)
    apply(cases "0 < s1", simp_all)
    done
  ultimately have "steps (s, l, r) (tp, 0) stp = (s1, l1, r1)"
    apply(rule_tac ind, auto)
    done
  thus "steps (s, l, r) (tp, 0) (Suc stp) = (s', l', r')"
    using h g assms
    apply(simp add: step_red)
    apply(rule_tac step_eq_in, auto)
    done
qed

lemma tm_append_fetch_first: 
  "fetch A s b = (ac, ns); ns  0  
    fetch (A @ B) s b = (ac, ns)"
  by(cases b;cases s;force simp: fetch.simps nth_append split: if_splits)

lemma tm_append_first_step_eq: 
  assumes "step (s, l, r) (A, off) = (s', l', r')"
    and "s'  0"
  shows "step (s, l, r) (A @ B, off) = (s', l', r')"
  using assms
  apply(simp add: step.simps)
  apply(cases "fetch A (s - off) (read r)")
  apply(frule_tac  B = B and b = "read r" in tm_append_fetch_first, auto)
  done

lemma tm_append_first_steps_eq: 
  assumes "steps (s, l, r) (A, off) stp = (s', l', r')"
    and "s'  0"
  shows "steps (s, l, r) (A @ B, off) stp = (s', l', r')"
  using assms
proof(induct stp arbitrary: s' l' r', simp add: steps.simps)
  fix stp s' l' r'
  assume ind: "s' l' r'. steps (s, l, r) (A, off) stp = (s', l', r'); s'  0
     steps (s, l, r) (A @ B, off) stp = (s', l', r')"
    and h: "steps (s, l, r) (A, off) (Suc stp) = (s', l', r')" "s'  0"
  obtain sa la ra where a: "steps (s, l, r) (A, off) stp = (sa, la, ra)"
    apply(cases "steps (s, l, r) (A, off) stp") by blast
  hence "steps (s, l, r) (A @ B, off) stp = (sa, la, ra)  sa  0"
    using h ind[of sa la ra]
    apply(cases sa, simp_all)
    done
  thus "steps (s, l, r) (A @ B, off) (Suc stp) = (s', l', r')"
    using h a
    apply(simp add: step_red)
    apply(intro tm_append_first_step_eq, simp_all)
    done
qed

lemma tm_append_second_fetch_eq:
  assumes
    even: "length A mod 2 = 0"
    and off: "off = length A div 2"
    and fetch: "fetch B s b = (ac, ns)"
    and notfinal: "ns  0"
  shows "fetch (A @ shift B off) (s + off) b = (ac, ns + off)"
  using assms
  by(cases b;cases s,auto simp: nth_append shift.simps split: if_splits)

lemma tm_append_second_step_eq: 
  assumes 
    exec: "step0 (s, l, r) B = (s', l', r')"
    and notfinal: "s'  0"
    and off: "off = length A div 2"
    and even: "length A mod 2 = 0"
  shows "step0 (s + off, l, r) (A @ shift B off) = (s' + off, l', r')"
  using assms
  apply(simp add: step.simps)
  apply(cases "fetch B s (read r)")
  apply(frule_tac tm_append_second_fetch_eq, simp_all, auto)
  done


lemma tm_append_second_steps_eq: 
  assumes 
    exec: "steps (s, l, r) (B, 0) stp = (s', l', r')"
    and notfinal: "s'  0"
    and off: "off = length A div 2"
    and even: "length A mod 2 = 0"
  shows "steps (s + off, l, r) (A @ shift B off, 0) stp = (s' + off, l', r')"
  using exec notfinal
proof(induct stp arbitrary: s' l' r')
  case 0
  thus "steps0 (s + off, l, r) (A @ shift B off) 0 = (s' + off, l', r')"
    by(simp add: steps.simps)
next
  case (Suc stp s' l' r')
  have ind: "s' l' r'. steps0 (s, l, r) B stp = (s', l', r'); s'  0  
    steps0 (s + off, l, r) (A @ shift B off) stp = (s' + off, l', r')"
    by fact
  have h: "steps0 (s, l, r) B (Suc stp) = (s', l', r')" by fact
  have k: "s'  0" by fact
  obtain s'' l'' r'' where a: "steps0 (s, l, r) B stp = (s'', l'', r'')"
    by (metis prod_cases3)
  then have b: "s''  0"
    using h k
    by(intro notI, auto)
  from a b have c: "steps0 (s + off, l, r) (A @ shift B off) stp