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"