Theory Multi_Single_TM_Translation

section ‹Translating Multitape TMs to Singletape TMs›

text ‹In this section we define the mapping from a multitape Turing machine to a singletape
       Turing machine. We further define soundness of the translation via several relations
      which establish a connection between configurations of both kinds of Turing machines.

  The translation works both for deterministic and non-deterministic TMs. Moreover,
  we verify a quadratic overhead in runtime. 
›

(* potential extension: add right-end marker, so that final phase can write original symbols of first tape onto tape, i.e.
   replace tuple-symbols by original symbols; this could be useful if TMs with output are considered, i.e., 
   where functions need to be computed *)

theory Multi_Single_TM_Translation
  imports  
    Multitape_TM
    Singletape_TM
    STM_Renaming
begin

subsection ‹Definition of the Translation›

datatype 'a tuple_symbol = NO_HAT "'a" | HAT "'a"
datatype ('a, 'k) st_tape_symbol = ST_LE ("⊢") | TUPLE "'k ⇒ 'a tuple_symbol" | INP "'a"
datatype 'a sym_or_bullet = SYM "'a" | BULLET ("∙")

datatype ('a,'q,'k) st_states = 
  R1 "'a sym_or_bullet" |
  R2 |
  S0 'q |
  S  "'q" "'k ⇒ 'a sym_or_bullet" |
  S1  "'q" "'k ⇒ 'a" |
  E0  "'q" "'k ⇒ 'a" "'k ⇒ dir" |
  E  "'q" "'k ⇒ 'a sym_or_bullet" "'k ⇒ dir" |
  Er "'q" "'k ⇒ 'a sym_or_bullet" "'k ⇒ dir" "'k set" |
  El "'q" "'k ⇒ 'a sym_or_bullet" "'k ⇒ dir" "'k set" |
  Em "'q" "'k ⇒ 'a sym_or_bullet" "'k ⇒ dir" "'k set"

type_synonym ('a,'q,'k)mt_rule = "'q × ('k ⇒ 'a) × 'q × ('k ⇒ 'a) × ('k ⇒ dir)" 

context multitape_tm
begin

definition R1_Set where "R1_Set = SYM ` Σ ∪ {∙}" 

definition gamma_set :: "('k ⇒ 'a tuple_symbol) set" where
  "gamma_set = (UNIV :: 'k set) → NO_HAT ` Γ ∪ HAT ` Γ" 

definition Γ' :: "('a, 'k) st_tape_symbol set" where 
  "Γ' = TUPLE ` gamma_set ∪ INP ` Σ ∪ {⊢}" 

definition "func_set = (UNIV :: 'k set) → SYM ` Γ ∪ {∙}" 

definition blank' :: "('a, 'k) st_tape_symbol" where "blank' = TUPLE (λ _. NO_HAT blank)" 
definition hatLE' :: "('a, 'k) st_tape_symbol" where "hatLE' = TUPLE (λ _. HAT LE)" 
definition encSym :: "'a ⇒ ('a, 'k) st_tape_symbol" where "encSym a = (TUPLE (λ i. if i = 0 then NO_HAT a else NO_HAT blank))" 

definition add_inp :: "('k ⇒ 'a tuple_symbol) ⇒ ('k ⇒ 'a sym_or_bullet) ⇒ ('k ⇒ 'a sym_or_bullet)" where
  "add_inp inp inp2 = (λ k. case inp k of HAT s ⇒ SYM s | _ ⇒ inp2 k)" 

definition project_inp :: "('k ⇒ 'a sym_or_bullet) ⇒ ('k ⇒ 'a)" where
  "project_inp inp = (λ k. case inp k of SYM s ⇒ s)" 

definition compute_idx_set :: "('k ⇒ 'a tuple_symbol) ⇒ ('k ⇒ 'a sym_or_bullet)  ⇒ 'k set" where
  "compute_idx_set tup ys = {i . tup i ∈ HAT ` Γ ∧ ys i ∈ SYM ` Γ}"

definition update_ys :: "('k ⇒ 'a tuple_symbol) ⇒ ('k ⇒ 'a sym_or_bullet)  ⇒ ('k ⇒ 'a sym_or_bullet)" where
  "update_ys tup ys = (λ k. if k ∈ (compute_idx_set tup ys) then ∙ else ys k)"

definition replace_sym :: "('k ⇒ 'a tuple_symbol) ⇒ ('k ⇒ 'a sym_or_bullet)  ⇒ ('k ⇒ 'a tuple_symbol)" where
  "replace_sym tup ys = (λ k. if k ∈ (compute_idx_set tup ys) 
                              then (case ys k of SYM a ⇒ NO_HAT a) 
                              else tup k)"

definition place_hats_to_dir :: "dir ⇒ ('k ⇒ 'a tuple_symbol) ⇒ ('k ⇒ dir) ⇒'k set ⇒ ('k ⇒ 'a tuple_symbol)" where
  "place_hats_to_dir dir tup ds I = (λ k. (case tup k of 
                                      NO_HAT a ⇒ if k ∈ I ∧ ds k = dir 
                                                  then HAT a
                                                  else NO_HAT a 
                                      | HAT a ⇒ HAT a )) "

definition place_hats_R :: "('k ⇒ 'a tuple_symbol) ⇒ ('k ⇒ dir) ⇒'k set ⇒ ('k ⇒ 'a tuple_symbol)" where
  "place_hats_R = place_hats_to_dir dir.R"

definition place_hats_M :: "('k ⇒ 'a tuple_symbol) ⇒ ('k ⇒ dir) ⇒'k set ⇒ ('k ⇒ 'a tuple_symbol)" where
  "place_hats_M = place_hats_to_dir dir.N"

definition place_hats_L :: "('k ⇒ 'a tuple_symbol) ⇒ ('k ⇒ dir) ⇒'k set ⇒ ('k ⇒ 'a tuple_symbol)" where
  "place_hats_L = place_hats_to_dir dir.L"

definition δ' :: 
  "(('a, 'q, 'k) st_states × ('a, 'k) st_tape_symbol × ('a, 'q, 'k) st_states × ('a, 'k) st_tape_symbol × dir)set"  
  where
    "δ' = ({(R1 ∙, ⊢, R1 ∙, ⊢, dir.R)}) 
    ∪ (λ x. (R1 ∙, INP x, R1 (SYM x), hatLE', dir.R)) ` Σ
    ∪ (λ (a,x). (R1 (SYM a), INP x, R1 (SYM x), encSym a, dir.R)) ` (Σ × Σ)
    ∪ {(R1 ∙, blank', R2, hatLE', dir.L)}
    ∪ (λ a. (R1 (SYM a), blank', R2, encSym a, dir.L)) ` Σ
    ∪ (λ x. (R2, x, R2, x, dir.L)) ` (Γ' - { ⊢ })
    ∪ {(R2, ⊢, S0 s, ⊢, dir.N)}
    ∪ (λ q. (S0 q, ⊢, S q (λ _. ∙), ⊢, dir.R)) ` (Q - {t,r})
    ∪ (λ (q,inp,t). (S q inp, TUPLE t, S q (add_inp t inp), TUPLE t, dir.R)) ` (Q × (func_set - (UNIV → SYM ` Γ)) × gamma_set)
    ∪ (λ (q,inp,a). (S q inp, a, S1 q (project_inp inp), a, dir.L)) ` (Q × (UNIV → SYM ` Γ) × (Γ' - { ⊢ }))
    ∪ (λ ((q,a,q',b,d),t). (S1 q a, t, E0 q' b d, t, dir.N)) ` (δ × Γ')
    ∪ (λ ((q,a,d),t). (E0 q a d, t, E q (SYM o a) d, t, dir.N)) ` ((Q × (UNIV → Γ) × UNIV) × Γ')
    ∪ (λ (q,d). (E q (λ _. ∙) d, ⊢, S0 q, ⊢, dir.N)) ` (Q × UNIV)
    ∪ (λ (q,ys,ds,t).   (E  q ys ds,   TUPLE t, Er q (update_ys t ys) ds (compute_idx_set t ys), TUPLE(replace_sym t ys), dir.R)) ` (Q × func_set × UNIV × gamma_set)
    ∪ (λ (q,ys,ds,I,t). (Er q ys ds I, TUPLE t, Em q ys ds I, TUPLE (place_hats_R t ds I), dir.L)) ` (Q × func_set × UNIV × UNIV × gamma_set)
    ∪ (λ (q,ys,ds,I,t). (Em q ys ds I, TUPLE t, El q ys ds I, TUPLE (place_hats_M t ds I), dir.L)) ` (Q × func_set × UNIV × UNIV × gamma_set)
    ∪ (λ (q,ys,ds,I,t). (El q ys ds I, TUPLE t, E  q ys ds,   TUPLE (place_hats_L t ds I), dir.N)) ` (Q × func_set × UNIV × UNIV × gamma_set)
    ∪ (λ (q,ys,ds,I).   (El q ys ds I, ⊢, E q ys ds, ⊢, dir.N)) ` (Q × func_set × UNIV × Pow(UNIV)) ― ‹ first switch into E state, so E phase is always finished in E state›
  "

definition "Q' = 
  R1 ` R1_Set ∪ {R2} ∪ 
  S0 ` Q ∪ (λ (q,inp). S q inp) ` (Q × func_set) ∪ (λ (q,a). S1 q a) ` (Q × (UNIV → Γ)) ∪
  (λ (q,a,d). E0 q a d) ` (Q × (UNIV → Γ) × UNIV) ∪ 
  (λ (q,a,d). E q a d) ` (Q × func_set × UNIV) ∪
  (λ (q,a,d,I). Er q a d I) ` (Q × func_set × UNIV × UNIV) ∪
  (λ (q,a,d,I). Em q a d I) ` (Q × func_set × UNIV × UNIV) ∪
  (λ (q,a,d,I). El q a d I) ` (Q × func_set × UNIV × UNIV)"

lemma compute_idx_range[simp,intro]:
  assumes "tup ∈ gamma_set"
  assumes "ys ∈ func_set"
  shows "compute_idx_set tup ys ∈ UNIV"
  by auto

lemma update_ys_range[simp,intro]:
  assumes "tup ∈ gamma_set"
  assumes "ys ∈ func_set"
  shows "update_ys tup ys ∈ func_set"
  by (insert assms, fastforce simp: update_ys_def func_set_def)

lemma replace_sym_range[simp,intro]:
  assumes "tup ∈ gamma_set"
  assumes "ys ∈ func_set"
  shows "replace_sym tup ys ∈ gamma_set"
proof -
  have "∀ k. (if k ∈ compute_idx_set tup ys then case ys k of SYM x ⇒ NO_HAT x else tup k) ∈ NO_HAT ` Γ ∪ HAT ` Γ"
    by(intro allI, insert assms, cases "k ∈ compute_idx_set tup ys", auto simp: func_set_def compute_idx_set_def gamma_set_def replace_sym_def)
  then show ?thesis
    using assms unfolding replace_sym_def gamma_set_def by blast
qed

lemma tup_hat_content:
  assumes "tup ∈ gamma_set"
  assumes "tup x = HAT a"
  shows "a ∈ Γ"
proof - 
  have "range tup ⊆ NO_HAT ` Γ ∪ HAT ` Γ" 
    using assms gamma_set_def by auto
  then show ?thesis 
    using assms(2)
    by (metis UNIV_I Un_iff image_iff image_subset_iff tuple_symbol.distinct(1) tuple_symbol.inject(2))
qed

lemma tup_no_hat_content:
  assumes "tup ∈ gamma_set"
  assumes "tup x = NO_HAT a"
  shows "a ∈ Γ"
proof - 
  have "range tup ⊆ NO_HAT ` Γ ∪ HAT ` Γ" 
    using assms gamma_set_def by auto
  then show ?thesis 
    using assms(2)
    by (metis UNIV_I Un_iff image_iff image_subset_iff tuple_symbol.inject(1) tuple_symbol.simps(4))
qed

lemma place_hats_to_dir_range[simp, intro]:
  assumes "tup ∈ gamma_set"
  shows "place_hats_to_dir d tup ds I ∈ gamma_set"
proof -
  have "∀ k. (case tup k of NO_HAT a ⇒ if k ∈ I ∧ ds k = d then HAT a else NO_HAT a | HAT x ⇒ HAT x)
    ∈  NO_HAT ` Γ ∪ HAT ` Γ"
  proof 
    fix k 
    show "(case tup k of NO_HAT a ⇒ if k ∈ I ∧ ds k = d then HAT a else NO_HAT a | HAT x ⇒ HAT x)
    ∈  NO_HAT ` Γ ∪ HAT ` Γ"
      by(cases "tup k", insert tup_hat_content[OF assms(1)] tup_no_hat_content[OF assms(1)], auto simp: gamma_set_def)
  qed
  then show ?thesis
    using assms
    unfolding place_hats_to_dir_def gamma_set_def
    by auto
qed

lemma place_hats_range[simp,intro]:
  assumes "tup ∈ gamma_set"
  shows "place_hats_R tup ds I ∈ gamma_set" and 
    "place_hats_L tup ds I ∈ gamma_set" and 
    "place_hats_M tup ds I ∈ gamma_set"
  by(insert assms, auto simp: place_hats_R_def place_hats_L_def place_hats_M_def)

lemma fin_R1_Set[intro,simp]: "finite R1_Set" 
  unfolding R1_Set_def using fin_Σ by auto

lemma fin_gamma_set[intro,simp]: "finite gamma_set" 
  unfolding gamma_set_def using fin_Γ 
  by (intro fin_funcsetI, auto)

lemma fin_Γ'[intro,simp]: "finite Γ'" 
  unfolding Γ'_def using fin_Σ by auto

lemma fin_func_set[simp,intro]: "finite func_set" 
  unfolding func_set_def using fin_Γ by auto

lemma memberships[simp,intro]: "⊢ ∈ Γ'" 
  "∙ ∈ R1_Set" 
  "x ∈ Σ ⟹ SYM x ∈ R1_Set" 
  "x ∈ Σ ⟹ encSym x ∈ Γ'"
  "blank' ∈ Γ'" 
  "hatLE' ∈ Γ'" 
  "x ∈ Σ ⟹ INP x ∈ Γ'" 
  "y ∈ gamma_set ⟹ TUPLE y ∈ Γ'" 
  "(λ_. ∙) ∈ func_set" 
  "f ∈ UNIV → SYM ` Γ ⟹ f ∈ func_set" 
  "g ∈ UNIV → Γ ⟹ SYM ∘ g ∈ func_set" 
  "f ∈ UNIV → SYM ` Γ ⟹ project_inp f k ∈ Γ" 
  unfolding R1_Set_def Γ'_def blank'_def hatLE'_def gamma_set_def encSym_def func_set_def project_inp_def
  using LE blank tm funcset_mem[of f UNIV "SYM ` Γ" k] by (auto split: sym_or_bullet.splits)

lemma add_inp_func_set[simp,intro]: "b ∈ gamma_set ⟹ a ∈ func_set ⟹ add_inp b a ∈ func_set"
  unfolding func_set_def gamma_set_def
proof
  fix x
  assume a: "a ∈ UNIV → SYM ` Γ ∪ {∙}" and b: "b ∈ UNIV → NO_HAT ` Γ ∪ HAT ` Γ" 
  from a have a: "a x ∈ SYM ` Γ ∪ {∙}" by auto
  from b have b: "b x ∈ NO_HAT ` Γ ∪ HAT ` Γ" by auto
  show "add_inp b a x ∈ SYM ` Γ ∪ {∙}" using a b
    unfolding add_inp_def by (cases "b x", auto simp: gamma_set_def)
qed


lemma automation[simp]: "⋀ a b A B. (S a b ∈ (λx. case x of (x1, x2) ⇒ S x1 x2) ` (A × B)) ⟷ (a ∈ A ∧ b ∈ B)"
  "⋀ a b A B. (S1 a b ∈ (λx. case x of (x1, x2) ⇒ S1 x1 x2) ` (A × B)) ⟷ (a ∈ A ∧ b ∈ B)"
  "⋀ a b c A B C. (E0 a b c ∈ (λx. case x of (x1, x2, x3) ⇒ E0 x1 x2 x3) ` (A × B × C)) ⟷ (a ∈ A ∧ b ∈ B ∧ c ∈ C)"
  "⋀ a b c A B C. (E a b c ∈ (λx. case x of (x1, x2, x3) ⇒ E x1 x2 x3) ` (A × B × C)) ⟷ (a ∈ A ∧ b ∈ B ∧ c ∈ C)"
  "⋀ a b c d A B C. (Er a b c d ∈ (λx. case x of (x1, x2, x3, x4) ⇒ Er x1 x2 x3 x4) ` (A × B × C)) ⟷ (a ∈ A ∧ b ∈ B ∧ (c,d) ∈ C)"
  "⋀ a b c d A B C. (Em a b c d ∈ (λx. case x of (x1, x2, x3, x4) ⇒ Em x1 x2 x3 x4) ` (A × B × C)) ⟷ (a ∈ A ∧ b ∈ B ∧ (c,d) ∈ C)"
  "⋀ a b c d A B C. (El a b c d ∈ (λx. case x of (x1, x2, x3, x4) ⇒ El x1 x2 x3 x4) ` (A × B × C)) ⟷ (a ∈ A ∧ b ∈ B ∧ (c,d) ∈ C)"
  "blank' ≠ ⊢" 
  "⊢ ≠ blank'" 
  "blank' ≠ INP x" 
  "INP x ≠ blank'" 
  by (force simp: blank'_def)+

interpretation st: singletape_tm Q' "(INP ` Σ)" Γ' blank' ⊢ δ' "R1 ∙" "S0 t" "S0 r"
proof 
  show "finite Q'" 
    unfolding Q'_def using fin_Q fin_Γ
    by (intro finite_UnI finite_imageI finite_cartesian_product, auto)
  show "finite Γ'" by (rule fin_Γ')
  show "S0 t ∈ Q'" unfolding Q'_def using tQ by auto
  show "S0 r ∈ Q'" unfolding Q'_def using rQ by auto
  show "S0 t ≠ S0 r" using tr by auto
  show "blank' ∉ INP ` Σ" unfolding blank'_def by auto
  show "R1 ∙ ∈ Q'" unfolding Q'_def by auto
  show "δ' ⊆ (Q' - {S0 t, S0 r}) × Γ' × Q' × Γ' × UNIV" 
    unfolding δ'_def Q'_def using tm
    by (auto dest: δ)
  show "(q, ⊢, q', a', d) ∈ δ' ⟹ a' = ⊢ ∧ d ∈ {dir.N, dir.R}" for q q' a' d
    unfolding δ'_def by (auto simp: hatLE'_def blank'_def)
qed auto

lemma valid_st: "singletape_tm Q' (INP ` Σ) Γ' blank' ⊢ δ' (R1 ∙) (S0 t) (S0 r)" ..

text ‹Determinism is preserved.›

lemma det_preservation: "deterministic ⟹ st.deterministic" 
  unfolding deterministic_def st.deterministic_def unfolding δ'_def
  by auto


subsection ‹Soundness of the Translation›

lemma range_mt_pos: 
  "∃ i. Max (range (mt_pos cm)) = mt_pos cm i" 
  "finite (range (mt_pos (cm :: ('a, 'q, 'k) mt_config)))" 
  "range (mt_pos cm) ≠ {}"
proof -
  show "finite (range (mt_pos cm))" by auto
  moreover show "range (mt_pos cm) ≠ {}" by auto
  ultimately show "∃ i. Max (range (mt_pos cm)) = mt_pos cm i"
    by (meson Max_in imageE)
qed

lemma max_mt_pos_step: assumes "(cm,cm') ∈ step" 
  shows "Max (range (mt_pos cm')) ≤ Suc (Max (range (mt_pos cm)))" 
proof -
  from range_mt_pos(1)[of cm'] obtain i'
    where max1: "Max (range (mt_pos cm')) = mt_pos cm' i'" by auto
  hence "Max (range (mt_pos cm')) ≤ mt_pos cm' i'" by auto
  also have "… ≤ Suc (mt_pos cm i')" using assms
  proof (cases)
    case (step q ts n q' a dir)
    then show ?thesis by (cases "dir i'", auto)
  qed
  also have "… ≤ Suc (Max (range (mt_pos cm)))" using range_mt_pos[of cm] by simp
  finally show ?thesis .
qed

lemma max_mt_pos_init: "Max (range (mt_pos (init_config w))) = 0" 
  unfolding init_config_def by auto

lemma INP_D: assumes "set x ⊆ INP ` Σ" 
  shows "∃ w. x = map INP w ∧ set w ⊆ Σ" 
  using assms 
proof (induct x)
  case (Cons x xs)
  then obtain w where "xs = map INP w ∧ set w ⊆ Σ" by auto
  moreover from Cons(2) obtain a where "x = INP a" and "a ∈ Σ" by auto
  ultimately show ?case by (intro exI[of _ "a # w"], auto)
qed auto


subsubsection ‹R-Phase›

fun enc :: "('a, 'q, 'k) mt_config ⇒ nat ⇒ ('a, 'k) st_tape_symbol"
  where "enc (ConfigM q tc p) n = TUPLE (λ k. if p k = n then HAT (tc k n) else NO_HAT (tc k n))"

inductive rel_R1 :: "(('a, 'k) st_tape_symbol,('a, 'q, 'k) st_states)st_config ⇒ 'a list ⇒ nat ⇒ bool" where 
  "n = length w ⟹ 
  tc' 0 = ⊢ ⟹ 
  p' ≤ n ⟹ 
  (⋀ i. i < p' ⟹ enc (init_config w) i = tc' (Suc i)) ⟹
  (⋀ i. i ≥ p' ⟹ tc' (Suc i) = (if i < n then INP (w ! i) else blank')) ⟹
  (p' = 0 ⟹ q' = ∙) ⟹
  (⋀ p. p' = Suc p ⟹ q' = SYM (w ! p)) ⟹
  rel_R1 (ConfigS (R1 q') tc' (Suc p')) w p'" 


lemma rel_R1_init: shows "∃ cs1. (st.init_config (map INP w), cs1) ∈ st.dstep ∧ rel_R1 cs1 w 0" 
proof -
  let ?INP = "INP :: 'a ⇒ ('a, 'k) st_tape_symbol" 
  have mem: "(R1 ∙, ⊢, R1 ∙, ⊢, dir.R) ∈ δ'" unfolding δ'_def by auto
  let ?cs1 = "ConfigS (R1 ∙) (λn. if n = 0 then ⊢ else if n ≤ length (map ?INP w) then map ?INP w ! (n - 1) else blank') (Suc 0)" 
  have "(st.init_config (map INP w), ?cs1) ∈ st.dstep" 
    unfolding st.init_config_def by (rule st.dstepI[OF mem], auto simp: δ'_def blank'_def)
  moreover have "rel_R1 ?cs1 w 0" 
    by (intro rel_R1.intros[OF refl], auto)
  ultimately show ?thesis by blast
qed

lemma rel_R1_R1: assumes "rel_R1 cs0 w j"
  and "j < length w" 
  and "set w ⊆ Σ" 
shows "∃ cs1. (cs0, cs1) ∈ st.dstep ∧ rel_R1 cs1 w (Suc j)" 
  using assms(1)
proof (cases rule: rel_R1.cases)
  case (1 n tc' q')
  note cs0 = 1(1)
  from assms have wj: "w ! j ∈ Σ" by auto
  show ?thesis
  proof (cases j)
    case 0
    with 1 have q': "q' = ∙" by auto
    from 1(6)[of 0] 0 assms 1 have tc'1: "tc' (Suc 0) = INP (w ! 0)" by auto
    have mem: "(R1 ∙, INP (w ! 0), R1 (SYM (w ! 0)), hatLE', dir.R) ∈ δ'" unfolding δ'_def
      using wj 0 by auto
    let ?cs1 = "ConfigS (R1 (SYM (w ! 0))) (tc'(Suc 0 := hatLE')) (Suc (Suc 0))" 
    have enc: "enc (init_config w) 0 = hatLE'" unfolding init_config_def hatLE'_def by auto
    have "(cs0, ?cs1) ∈ st.dstep" unfolding cs0 0
      by (intro st.dstepI[OF mem], auto simp: q' tc'1 δ'_def blank'_def)
    moreover have "rel_R1 ?cs1 w (Suc 0)" 
      by (intro rel_R1.intros, rule 1(2), insert 1 0 assms(2), auto simp: enc) (cases w, auto)
    ultimately show ?thesis unfolding 0 by blast
  next
    case (Suc p)
    from 1(8)[OF Suc] have q': "q' = SYM (w ! p)" by auto
    from Suc assms(2) have "p < length w" by auto
    with assms(3) have "w ! p ∈ Σ" by auto
    with wj have "(w ! p, w ! j) ∈ Σ × Σ" by auto
    hence mem: "(R1 (SYM (w ! p)), INP (w ! j), R1 (SYM (w ! j)), encSym (w ! p), dir.R) ∈ δ'" unfolding δ'_def by auto
    have enc: "enc (init_config w) j = encSym (w ! p)" unfolding Suc using ‹p < length w›
      by (auto simp: init_config_def encSym_def)
    from 1(6)[of j] assms 1 have tc': "tc' (Suc j) = INP (w ! j)" by auto
    let ?cs1 = "ConfigS (R1 (SYM (w ! j))) (tc'(Suc j := encSym (w ! p))) (Suc (Suc j))" 
    have "(cs0, ?cs1) ∈ st.dstep" unfolding cs0
      by (rule st.dstepI[OF mem], insert q' tc', auto simp: δ'_def blank'_def)
    moreover have "rel_R1 ?cs1 w (Suc j)" 
      by (intro rel_R1.intros, insert 1 assms enc, auto)
    ultimately show ?thesis by blast
  qed
qed

inductive rel_R2 :: "(('a, 'k) st_tape_symbol,('a, 'q, 'k) st_states)st_config ⇒ 'a list ⇒ nat ⇒ bool" where 
  "tc' 0 = ⊢ ⟹ 
  (⋀ i. enc (init_config w) i = tc' (Suc i)) ⟹
  p ≤ length w ⟹
  rel_R2 (ConfigS R2 tc' p) w p" 


lemma rel_R1_R2: assumes "rel_R1 cs0 w (length w)"
  and "set w ⊆ Σ" 
shows "∃ cs1. (cs0, cs1) ∈ st.dstep ∧ rel_R2 cs1 w (length w)" 
  using assms
proof (cases rule: rel_R1.cases)
  case (1 n tc' q')
  note cs0 = 1(1)
  have enc: "enc (init_config w) i = tc' (Suc i)" if "i ≠ length w" for i
  proof (cases "i < length w")
    case True
    thus ?thesis using 1(5)[of i] by auto
  next
    case False
    with that have i: "i > length w" by auto
    with 1(6)[of i] 1 have "tc' (Suc i) = blank'" by auto
    also have "… = enc (init_config w) i" using i unfolding init_config_def by (auto simp: blank'_def)
    finally show ?thesis by simp
  qed
  show ?thesis
  proof (cases "length w")
    case 0
    with 1 have q': "q' = ∙" by auto
    from 1(6)[of 0] 0 1 have tc'1: "tc' (Suc 0) = blank'" by auto
    have mem: "(R1 ∙, blank', R2, hatLE', dir.L) ∈ δ'" unfolding δ'_def
      by auto
    let ?tc = "tc'(Suc 0 := hatLE')" 
    let ?cs1 = "ConfigS R2 ?tc 0" 
    have enc0: "enc (init_config w) 0 = hatLE'" unfolding init_config_def hatLE'_def by auto
    have enc: "enc (init_config w) i = ?tc (Suc i)" for i using enc[of i] enc0 using 0
      by (cases i, auto)
    have "(cs0, ?cs1) ∈ st.dstep" unfolding cs0 0
      by (intro st.dstepI[OF mem], auto simp: q' tc'1 δ'_def blank'_def)
    moreover have "rel_R2 ?cs1 w (length w)" unfolding 0
      by (intro rel_R2.intros enc, insert 1 0, auto)
    ultimately show ?thesis unfolding 0 by blast
  next
    case (Suc p)
    from 1(8)[OF Suc] have q': "q' = SYM (w ! p)" by auto
    from Suc have "p < length w" by auto
    with assms(2) have "w ! p ∈ Σ" by auto
    hence mem: "(R1 (SYM (w ! p)), blank', R2, encSym (w ! p), dir.L) ∈ δ'" unfolding δ'_def by auto
    let ?tc = "tc'(Suc (length w) := encSym (w ! p))" 
    have encW: "enc (init_config w) (length w) = encSym (w ! p)" unfolding Suc using ‹p < length w›
      by (auto simp: init_config_def encSym_def)
    from 1(6)[of "length w"] assms 1 have tc': "tc' (Suc (length w)) = blank'" by auto
    let ?cs1 = "ConfigS R2 ?tc (length w)" 
    have enc: "enc (init_config w) i = ?tc (Suc i)" for i using enc[of i] encW by auto
    have "(cs0, ?cs1) ∈ st.dstep" unfolding cs0 q'
      by (intro st.dstepI[OF mem] tc', auto simp: δ'_def blank'_def)
    moreover have "rel_R2 ?cs1 w (length w)" 
      by (intro rel_R2.intros, insert 1 assms enc, auto)
    ultimately show ?thesis by blast
  qed
qed


lemma rel_R2_R2: assumes "rel_R2 cs0 w (Suc j)"
  and "set w ⊆ Σ" 
shows "∃ cs1. (cs0, cs1) ∈ st.dstep ∧ rel_R2 cs1 w j" 
  using assms
proof (cases rule: rel_R2.cases)
  case (1 tc')
  note cs0 = 1(1)
  from 1 have j: "j < length w" by auto
  have tc: "tc' (Suc j) ∈ Γ' - { ⊢ }" unfolding 1(3)[symmetric] using j assms(2)[unfolded set_conv_nth] unfolding init_config_def
    by (force simp: Γ'_def gamma_set_def intro!: imageI LE blank set_mp[OF Σ_sub_Γ, of "w ! (j - Suc 0)"])
  hence mem: "(R2, tc' (Suc j), R2, tc' (Suc j), dir.L) ∈ δ'" unfolding δ'_def by auto
  let ?cs1 = "ConfigS R2 tc' j" 
  have "(cs0, ?cs1) ∈ st.dstep" unfolding cs0 using tc
    by (intro st.dstepI[OF mem], auto simp: δ'_def blank'_def)
  moreover have "rel_R2 ?cs1 w j"
    by (intro rel_R2.intros, insert 1, auto)
  ultimately show ?thesis by blast
qed

inductive rel_S0 :: "(('a, 'k) st_tape_symbol,('a, 'q, 'k) st_states)st_config ⇒ ('a, 'q, 'k) mt_config ⇒ bool" where 
  "tc' 0 = ⊢ ⟹ 
  (⋀ i. tc' (Suc i) = enc (ConfigM q tc p) i) ⟹
  valid_config (ConfigM q tc p) ⟹
  rel_S0 (ConfigS (S0 q) tc' 0) (ConfigM q tc p)" 

lemma rel_R2_S0: assumes "rel_R2 cs0 w 0"
  and "set w ⊆ Σ" 
shows "∃ cs1. (cs0, cs1) ∈ st.dstep ∧ rel_S0 cs1 (init_config w)" 
  using assms
proof (cases rule: rel_R2.cases)
  case (1 tc')
  note cs0 = 1(1)
  hence mem: "(R2, ⊢, S0 s, ⊢, dir.N) ∈ δ'" unfolding δ'_def by auto
  let ?cs1 = "ConfigS (S0 s) tc' 0" 
  have "(cs0, ?cs1) ∈ st.dstep" unfolding cs0
    by (intro st.dstepI[OF mem], insert 1, auto simp: δ'_def blank'_def)
  moreover have "rel_S0 ?cs1 (init_config w)" using valid_init_config[OF assms(2)] unfolding init_config_def
    by (intro rel_S0.intros, insert 1(1,2,4-), auto simp: 1(3)[symmetric] init_config_def)
  ultimately show ?thesis by blast
qed

text ‹If we start with a proper word ‹w› as input on the singletape TM, 
  then via the R-phase one can switch to the beginning of 
  the S-phase (@{const rel_S0}) for the initial configuration.›

lemma R_phase: assumes "set w ⊆ Σ"
  shows "∃ cs. (st.init_config (map INP w), cs) ∈ st.dstep^^(3 + 2 * length w) ∧ rel_S0 cs (init_config w)" 
proof -
  from rel_R1_init[of w] obtain cs1 n where
    step1: "(st.init_config (map INP w), cs1) ∈ st.dstep" and 
    relR1: "rel_R1 cs1 w n" and 
    n0: "n = 0" 
    by auto
  from relR1
  have "n + k ≤ length w ⟹ ∃ cs2. (cs1, cs2) ∈ st.dstep^^k ∧ rel_R1 cs2 w (n + k)" for k
  proof (induction k arbitrary: cs1 n)
    case (Suc k cs1 n)  
    hence "n < length w" by auto
    from rel_R1_R1[OF Suc(3) this assms] obtain cs3 where
      step: "(cs1, cs3) ∈ st.dstep" and rel: "rel_R1 cs3 w (Suc n)" by auto
    from Suc.IH[OF _ rel] Suc(2) obtain cs2 where
      steps: "(cs3, cs2) ∈ st.dstep ^^ k"  and rel: "rel_R1 cs2 w (Suc n + k)" 
      by auto
    from relpow_Suc_I2[OF step steps] rel
    show ?case by auto
  qed auto
  from this[of "length w", unfolded n0]
  obtain cs2 where steps2: "(cs1, cs2) ∈ st.dstep ^^ length w" and rel: "rel_R1 cs2 w (length w)" by auto
  from rel_R1_R2[OF rel assms] obtain cs3 n where step3: "(cs2, cs3) ∈ st.dstep" 
    and rel: "rel_R2 cs3 w n" and n: "n = length w" 
    by auto
  from rel have "∃ cs. (cs3, cs) ∈ st.dstep^^n ∧ rel_R2 cs w 0" 
  proof (induction n arbitrary: cs3 rule: nat_induct)
    case (Suc n cs3)
    from rel_R2_R2[OF Suc(2) assms] obtain cs1 where
      step: "(cs3, cs1) ∈ st.dstep" and rel: "rel_R2 cs1 w n" by auto
    from Suc.IH[OF rel] obtain cs where steps: "(cs1, cs) ∈ st.dstep ^^ n" and rel: "rel_R2 cs w 0" by auto
    from relpow_Suc_I2[OF step steps] rel show ?case by auto
  qed auto
  then obtain cs4 where steps4: "(cs3, cs4) ∈ st.dstep^^(length w)"  and rel: "rel_R2 cs4 w 0" by (auto simp: n)
  from rel_R2_S0[OF rel assms] obtain cs where step5: "(cs4, cs) ∈ st.dstep" and 
    rel: "rel_S0 cs (init_config w)" by auto
  from relpow_Suc_I2[OF step1 relpow_transI[OF steps2 relpow_Suc_I2[OF step3 relpow_Suc_I[OF steps4 step5]]]]
  have "(st.init_config (map INP w), cs) ∈ st.dstep ^^ Suc (length w + Suc (Suc (length w)))" .
  also have "Suc (length w + Suc (Suc (length w))) = 3 + 2 * length w" by simp
  finally show ?thesis using rel by auto
qed  

subsubsection ‹S-Phase›

inductive rel_S :: "(('a, 'k) st_tape_symbol,('a, 'q, 'k) st_states)st_config ⇒ ('a, 'q, 'k) mt_config ⇒ nat ⇒ bool" where 
  "tc' 0 = ⊢ ⟹ 
  (⋀ i. tc' (Suc i) = enc (ConfigM q tc p) i) ⟹
  valid_config (ConfigM q tc p) ⟹
  (⋀ i. inp i = (if p i < p' then SYM (tc i (p i)) else ∙)) ⟹
  rel_S (ConfigS (S q inp) tc' (Suc p')) (ConfigM q tc p) p'" 

lemma rel_S0_S: assumes "rel_S0 cs0 cm"
  and "mt_state cm ∉ {t,r}" 
shows "∃ cs1. (cs0, cs1) ∈ st.dstep ∧ rel_S cs1 cm 0" 
  using assms(1)
proof (cases rule: rel_S0.cases)
  case (1 tc' q tc p)
  note cs0 = 1(1)
  note cm = 1(2)
  from assms(2) cm 1(5) have qtr: "q ∈ Q - {t,r}" by auto
  hence mem: "(S0 q, ⊢, S q (λ_. ∙), ⊢, dir.R) ∈ δ'" unfolding δ'_def by auto
  let ?cs1 = "ConfigS (S q (λ_. ∙)) tc' (Suc 0)" 
  have "(cs0, ?cs1) ∈ st.dstep" unfolding cs0
    by (rule st.dstepI[OF mem], insert 1, auto simp: δ'_def blank'_def)
  moreover have "rel_S ?cs1 cm 0" unfolding cm
    by (intro rel_S.intros 1, auto)
  ultimately show ?thesis by blast
qed

lemma rel_S_mem: assumes "rel_S (ConfigS (S q inp) tc' p') cm j" 
  shows "inp ∈ func_set ∧ q ∈ Q ∧ (∃ t. tc' (Suc i) = TUPLE t ∧ t ∈ gamma_set)" 
  using assms(1)
proof (cases rule: rel_S.cases)
  case (1 tc p)
  from 1 have q: "q ∈ Q" by auto
  have inp: "inp ∈ func_set" unfolding func_set_def 1(6) using 1(5)
    by force
  have "∃ t. tc' (Suc i) = TUPLE t ∧ t ∈ gamma_set" using 1(5)
    unfolding 1(4) by (force simp: gamma_set_def) 
  with q inp show ?thesis by auto
qed

lemma rel_S_S: assumes "rel_S cs0 cm p'" 
  "p' ≤ Max (range (mt_pos cm))" 
shows "∃ cs1. (cs0, cs1) ∈ st.dstep ∧ rel_S cs1 cm (Suc p')"
  using assms(1)
proof (cases rule: rel_S.cases)
  case (1 tc' q tc p inp)
  note cs0 = 1(1)
  note cm = 1(2)
  let ?Set = "Q × (func_set - (UNIV → SYM ` Γ)) × gamma_set" 
  let ?f = "λ(q, inp, t). (S q inp, TUPLE t, S q (add_inp t inp), TUPLE t, dir.R)" 
  obtain i where "mt_pos cm i = Max (range (mt_pos cm))" using range_mt_pos(1)[of cm] by auto
  with assms 1 have "p' ≤ p i" by auto
  with 1(6)[of i] have "inp i = ∙" by auto
  hence inp: "inp ∉ (UNIV → SYM ` Γ)"
    by (metis PiE UNIV_I image_iff sym_or_bullet.distinct(1))
  with rel_S_mem[OF assms(1)[unfolded cs0], of p'] obtain t where
    "(q,inp,t) ∈ ?Set" and tc': "tc' (Suc p') = TUPLE t" by auto
  hence "?f (q,inp,t) ∈ δ'" unfolding δ'_def by blast
  hence mem: "(S q inp, TUPLE t, S q (add_inp t inp), TUPLE t, dir.R) ∈ δ'" by simp 
  let ?cs1 = "ConfigS (S q (add_inp t inp)) tc' (Suc (Suc p'))" 
  have "(cs0,?cs1) ∈ st.dstep" unfolding cs0 using inp
    by (intro st.dstepI[OF mem], auto simp: tc' δ'_def blank'_def)
  moreover have "rel_S ?cs1 cm (Suc p')" unfolding cm
  proof (intro rel_S.intros 1)
    from 1(4)[of p', unfolded tc']
    have t: "t = (λk. if p k = p' then HAT (tc k p') else NO_HAT (tc k p'))" by auto
    show "⋀ k. add_inp t inp k = (if p k < Suc p' then SYM (tc k (p k)) else ∙)" 
      unfolding add_inp_def 1 t by auto
  qed
  ultimately show ?thesis by blast
qed

inductive rel_S1 :: "(('a, 'k) st_tape_symbol,('a, 'q, 'k) st_states)st_config ⇒ ('a, 'q, 'k) mt_config ⇒ bool" where 
  "tc' 0 = ⊢ ⟹ 
  (⋀ i. tc' (Suc i) = enc (ConfigM q tc p) i) ⟹
  valid_config (ConfigM q tc p) ⟹
  (⋀ i. inp i = tc i (p i)) ⟹
  (⋀ i. p i < p') ⟹
  p' = Suc (Max (range p)) ⟹
  rel_S1 (ConfigS (S1 q inp) tc' p') (ConfigM q tc p)" 

lemma rel_S_S1: assumes "rel_S cs0 cm p'" 
  "p' = Suc (Max (range (mt_pos cm)))" 
shows "∃ cs1. (cs0, cs1) ∈ st.dstep ∧ rel_S1 cs1 cm"
  using assms(1)
proof (cases rule: rel_S.cases)
  case (1 tc' q tc p inp)
  from assms have p'Max: "p' > Max (range (mt_pos cm))" by auto
  note cs0 = 1(1)
  note cm = 1(2)
  from p'Max range_mt_pos(2-)[of cm] have pip: "p i < p'" for i unfolding cm by auto
  let ?SET = "Q × func_set × gamma_set" 
  let ?Set = "Q × (UNIV → SYM ` Γ) × (Γ' - { ⊢ })" 
  from rel_S_mem[OF assms(1)[unfolded cs0], of p'] obtain t where
    mem: "(q,inp,t) ∈ ?SET" and tc': "tc' (Suc p') = TUPLE t" by auto
  hence "inp ∈ func_set" by auto
  with pip have inp: "inp ∈ UNIV → SYM ` Γ" unfolding func_set_def using 1(6) by auto
  with mem have "(q,inp,TUPLE t) ∈ ?Set" by auto
  hence "(λ (q,inp,a). (S q inp, a, S1 q (project_inp inp), a, dir.L)) (q,inp,TUPLE t) ∈ δ'" unfolding δ'_def by blast
  hence mem: "(S q inp, TUPLE t, S1 q (project_inp inp), TUPLE t, dir.L) ∈ δ'" by simp 
  let ?cs1 = "ConfigS (S1 q (project_inp inp)) tc' p'" 
  have "(cs0,?cs1) ∈ st.dstep" unfolding cs0 using inp
    by (intro st.dstepI[OF mem], auto simp: tc' δ'_def blank'_def)
  moreover have "rel_S1 ?cs1 cm" unfolding cm
  proof (intro rel_S1.intros 1 pip)
    fix i
    from inp have "inp i ∈ SYM ` Γ" by auto
    then obtain g where "inp i = SYM g" and "g ∈ Γ" by auto
    thus "project_inp inp i = tc i (p i)" using 1(6)[of i] by (auto simp: project_inp_def split: if_splits)
    show "p' = Suc (Max (range p))" unfolding assms(2) unfolding cm by simp
  qed
  ultimately show ?thesis by auto
qed

text ‹If we start the S-phase (in @{const rel_S0}), and the multitape-TM is not in a final state, 
  then we can move to the end of the S-phase (in @{const rel_S1}).›

lemma S_phase: assumes "rel_S0 cs cm"
  and "mt_state cm ∉ {t, r}" 
shows "∃ cs'. (cs, cs') ∈ st.dstep^^(3 + Max (range (mt_pos cm))) ∧ rel_S1 cs' cm" 
proof -
  let ?N = "Max (range (mt_pos cm))" 
  from rel_S0_S[OF assms] obtain cs1 n where
    step1: "(cs, cs1) ∈ st.dstep" and rel: "rel_S cs1 cm n" and n: "n = 0"   
    by auto
  from rel have "n + k ≤ Suc ?N ⟹ ∃ cs2. (cs1, cs2) ∈ st.dstep ^^ k ∧ rel_S cs2 cm (n + k)" for k
  proof (induction k arbitrary: cs1 n)
    case (Suc k cs n)
    hence "n ≤ ?N" by auto
    from rel_S_S[OF Suc(3) this] obtain cs1 where step: "(cs, cs1) ∈ st.dstep" and rel: "rel_S cs1 cm (Suc n)" by auto
    from Suc have "Suc n + k ≤ Suc ?N" by auto
    from Suc.IH[OF this rel] obtain cs2 where steps: "(cs1, cs2) ∈ st.dstep ^^ k" and rel: "rel_S cs2 cm (n + Suc k)" by auto
    from relpow_Suc_I2[OF step steps] rel
    show ?case by auto
  qed auto
  from this[of "Suc ?N", unfolded n] obtain cs2 where 
    steps2: "(cs1, cs2) ∈ st.dstep ^^ (Suc ?N)" and rel: "rel_S cs2 cm (Suc ?N)" by auto
  from rel_S_S1[OF rel] obtain cs3 where step3: "(cs2,cs3) ∈ st.dstep" and rel: "rel_S1 cs3 cm" by auto
  from relpow_Suc_I2[OF step1 relpow_Suc_I[OF steps2 step3]]
  have "(cs, cs3) ∈ st.dstep ^^ Suc (Suc (Suc ?N))" by simp
  also have "Suc (Suc (Suc ?N)) = 3 + ?N" by simp
  finally show ?thesis using rel by blast
qed

subsubsection ‹E-Phase›

context
  fixes rule :: "('a,'q,'k)mt_rule"
begin
inductive_set δstep :: "('a, 'q, 'k) mt_config rel" where
  δstep: "rule = (q, a, q1, b, dir) ⟹
   rule ∈ δ ⟹
   (⋀ k. ts k (n k) = a k) ⟹
   (⋀ k. ts' k = (ts k)(n k := b k)) ⟹
   (⋀ k. n' k = go_dir (dir k) (n k)) ⟹ 
   (ConfigM q ts n, ConfigM q1 ts' n') ∈ δstep"
end

lemma step_to_δstep: "(c1,c2) ∈ step ⟹ ∃ rule. (c1,c2) ∈ δstep rule" 
proof (induct rule: step.induct)
  case (step q ts n q' a dir)
  show ?case
    by (rule exI, rule δstep.intros[OF refl step], auto)
qed

lemma δstep_to_step: "(c1,c2) ∈ δstep rule ⟹ (c1,c2) ∈ step" 
proof (induct rule: δstep.induct)
  case *: (δstep q a q' b dir ts n ts' n')
  from * have a: "a = (λ k. ts k (n k))" by auto
  from * have ts': "ts' = (λ k. (ts k)(n k := b k))" by auto
  from * have n': "n' = (λ k. go_dir (dir k) (n k))" by auto
  from * show ?case using step.intros[of q ts n q' b dir] unfolding a ts' n' by auto
qed

inductive rel_E0 :: "(('a, 'k) st_tape_symbol,('a, 'q, 'k) st_states)st_config 
  ⇒ ('a, 'q, 'k) mt_config ⇒ ('a, 'q, 'k) mt_config ⇒ ('a,'q,'k)mt_rule ⇒ bool" where 
  "tc' 0 = ⊢ ⟹ 
  (⋀ i. tc' (Suc i) = enc (ConfigM q tc p) i) ⟹
  valid_config (ConfigM q tc p) ⟹
  rule = (q,a,q1,b,d) ⟹
  (ConfigM q tc p, ConfigM q1 tc1 p1) ∈ δstep rule ⟹
  (⋀ i. p i < p') ⟹
  p' = Suc (Max (range p)) ⟹
  rel_E0 (ConfigS (E0 q1 b d) tc' p') (ConfigM q tc p) (ConfigM q1 tc1 p1) rule" 

text ‹For the transition between S and E phase we do not have deterministic steps.
  Therefore we add two lemmas: the former one is for showing that multitape can be simulated
  by singletape, and the latter one is for the inverse direction.›
lemma rel_S1_E0_step: assumes "rel_S1 cs cm" 
  and "(cm,cm1) ∈ step" 
shows "∃ rule cs1. (cs, cs1) ∈ st.step ∧ rel_E0 cs1 cm cm1 rule"
proof -
  from step_to_δstep[OF assms(2)] obtain rule where rstep: "(cm, cm1) ∈ δstep rule" by auto 
  show ?thesis using assms(1)
  proof (cases rule: rel_S1.cases)
    case (1 tc' q tc p inp p')
    note cs = 1(1)
    note cm = 1(2)
    have tc': "tc' p' ∈ Γ'" unfolding 1(8,4) enc.simps Γ'_def gamma_set_def using 1(5)
      by (force intro!: imageI)
    show ?thesis using rstep[unfolded cm]
    proof (cases rule: δstep.cases)
      case 2: (δstep a q1 b dir ts' n')
      note rule = 2(2)
      note cm1 = 2(1)
      have "(λ((q, a, q', b, d), t). (S1 q a, t, E0 q' b d, t, dir.N)) (rule,tc' p') ∈ δ'"
        unfolding δ'_def using tc' 2(3) by blast
      hence mem: "(S1 q a, tc' p', E0 q1 b dir, tc' p', dir.N) ∈ δ'" by (auto simp: rule)
      have inp_a: "inp = a" using 2(4)[folded 1(6)] by auto
      let ?cs1 = "ConfigS (E0 q1 b dir) tc' p'" 
      have step: "(cs, ?cs1) ∈ st.step" unfolding cs
        by (intro st.stepI[OF mem], insert inp_a, auto