# 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 =
R⇩1 "'a sym_or_bullet" |
R⇩2 |
S⇩0 'q |
S  "'q" "'k ⇒ 'a sym_or_bullet" |
S⇩1  "'q" "'k ⇒ 'a" |
E⇩0  "'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
"δ' = ({(R⇩1 ∙, ⊢, R⇩1 ∙, ⊢, dir.R)})
∪ (λ x. (R⇩1 ∙, INP x, R⇩1 (SYM x), hatLE', dir.R)) ` Σ
∪ (λ (a,x). (R⇩1 (SYM a), INP x, R⇩1 (SYM x), encSym a, dir.R)) ` (Σ × Σ)
∪ {(R⇩1 ∙, blank', R⇩2, hatLE', dir.L)}
∪ (λ a. (R⇩1 (SYM a), blank', R⇩2, encSym a, dir.L)) ` Σ
∪ (λ x. (R⇩2, x, R⇩2, x, dir.L)) ` (Γ' - { ⊢ })
∪ {(R⇩2, ⊢, S⇩0 s, ⊢, dir.N)}
∪ (λ q. (S⇩0 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, S⇩1 q (project_inp inp), a, dir.L)) ` (Q × (UNIV → SYM ` Γ) × (Γ' - { ⊢ }))
∪ (λ ((q,a,q',b,d),t). (S⇩1 q a, t, E⇩0 q' b d, t, dir.N)) ` (δ × Γ')
∪ (λ ((q,a,d),t). (E⇩0 q a d, t, E q (SYM o a) d, t, dir.N)) ` ((Q × (UNIV → Γ) × UNIV) × Γ')
∪ (λ (q,d). (E q (λ _. ∙) d, ⊢, S⇩0 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' =
R⇩1 ` R1_Set ∪ {R⇩2} ∪
S⇩0 ` Q ∪ (λ (q,inp). S q inp) ` (Q × func_set) ∪ (λ (q,a). S⇩1 q a) ` (Q × (UNIV → Γ)) ∪
(λ (q,a,d). E⇩0 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. (S⇩1 a b ∈ (λx. case x of (x1, x2) ⇒ S⇩1 x1 x2) ` (A × B)) ⟷ (a ∈ A ∧ b ∈ B)"
"⋀ a b c A B C. (E⇩0 a b c ∈ (λx. case x of (x1, x2, x3) ⇒ E⇩0 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' ⊢ δ' "R⇩1 ∙" "S⇩0 t" "S⇩0 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 "S⇩0 t ∈ Q'" unfolding Q'_def using tQ by auto
show "S⇩0 r ∈ Q'" unfolding Q'_def using rQ by auto
show "S⇩0 t ≠ S⇩0 r" using tr by auto
show "blank' ∉ INP ` Σ" unfolding blank'_def by auto
show "R⇩1 ∙ ∈ Q'" unfolding Q'_def by auto
show "δ' ⊆ (Q' - {S⇩0 t, S⇩0 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' ⊢ δ' (R⇩1 ∙) (S⇩0 t) (S⇩0 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 (Config⇩M q tc p) n = TUPLE (λ k. if p k = n then HAT (tc k n) else NO_HAT (tc k n))"

inductive rel_R⇩1 :: "(('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_R⇩1 (Config⇩S (R⇩1 q') tc' (Suc p')) w p'"

lemma rel_R⇩1_init: shows "∃ cs1. (st.init_config (map INP w), cs1) ∈ st.dstep ∧ rel_R⇩1 cs1 w 0"
proof -
let ?INP = "INP :: 'a ⇒ ('a, 'k) st_tape_symbol"
have mem: "(R⇩1 ∙, ⊢, R⇩1 ∙, ⊢, dir.R) ∈ δ'" unfolding δ'_def by auto
let ?cs1 = "Config⇩S (R⇩1 ∙) (λ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_R⇩1 ?cs1 w 0"
by (intro rel_R⇩1.intros[OF refl], auto)
ultimately show ?thesis by blast
qed

lemma rel_R⇩1_R⇩1: assumes "rel_R⇩1 cs0 w j"
and "j < length w"
and "set w ⊆ Σ"
shows "∃ cs1. (cs0, cs1) ∈ st.dstep ∧ rel_R⇩1 cs1 w (Suc j)"
using assms(1)
proof (cases rule: rel_R⇩1.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: "(R⇩1 ∙, INP (w ! 0), R⇩1 (SYM (w ! 0)), hatLE', dir.R) ∈ δ'" unfolding δ'_def
using wj 0 by auto
let ?cs1 = "Config⇩S (R⇩1 (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_R⇩1 ?cs1 w (Suc 0)"
by (intro rel_R⇩1.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: "(R⇩1 (SYM (w ! p)), INP (w ! j), R⇩1 (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 = "Config⇩S (R⇩1 (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_R⇩1 ?cs1 w (Suc j)"
by (intro rel_R⇩1.intros, insert 1 assms enc, auto)
ultimately show ?thesis by blast
qed
qed

inductive rel_R⇩2 :: "(('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_R⇩2 (Config⇩S R⇩2 tc' p) w p"

lemma rel_R⇩1_R⇩2: assumes "rel_R⇩1 cs0 w (length w)"
and "set w ⊆ Σ"
shows "∃ cs1. (cs0, cs1) ∈ st.dstep ∧ rel_R⇩2 cs1 w (length w)"
using assms
proof (cases rule: rel_R⇩1.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: "(R⇩1 ∙, blank', R⇩2, hatLE', dir.L) ∈ δ'" unfolding δ'_def
by auto
let ?tc = "tc'(Suc 0 := hatLE')"
let ?cs1 = "Config⇩S R⇩2 ?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_R⇩2 ?cs1 w (length w)" unfolding 0
by (intro rel_R⇩2.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: "(R⇩1 (SYM (w ! p)), blank', R⇩2, 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 = "Config⇩S R⇩2 ?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_R⇩2 ?cs1 w (length w)"
by (intro rel_R⇩2.intros, insert 1 assms enc, auto)
ultimately show ?thesis by blast
qed
qed

lemma rel_R⇩2_R⇩2: assumes "rel_R⇩2 cs0 w (Suc j)"
and "set w ⊆ Σ"
shows "∃ cs1. (cs0, cs1) ∈ st.dstep ∧ rel_R⇩2 cs1 w j"
using assms
proof (cases rule: rel_R⇩2.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: "(R⇩2, tc' (Suc j), R⇩2, tc' (Suc j), dir.L) ∈ δ'" unfolding δ'_def by auto
let ?cs1 = "Config⇩S R⇩2 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_R⇩2 ?cs1 w j"
by (intro rel_R⇩2.intros, insert 1, auto)
ultimately show ?thesis by blast
qed

inductive rel_S⇩0 :: "(('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 (Config⇩M q tc p) i) ⟹
valid_config (Config⇩M q tc p) ⟹
rel_S⇩0 (Config⇩S (S⇩0 q) tc' 0) (Config⇩M q tc p)"

lemma rel_R⇩2_S⇩0: assumes "rel_R⇩2 cs0 w 0"
and "set w ⊆ Σ"
shows "∃ cs1. (cs0, cs1) ∈ st.dstep ∧ rel_S⇩0 cs1 (init_config w)"
using assms
proof (cases rule: rel_R⇩2.cases)
case (1 tc')
note cs0 = 1(1)
hence mem: "(R⇩2, ⊢, S⇩0 s, ⊢, dir.N) ∈ δ'" unfolding δ'_def by auto
let ?cs1 = "Config⇩S (S⇩0 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_S⇩0 ?cs1 (init_config w)" using valid_init_config[OF assms(2)] unfolding init_config_def
by (intro rel_S⇩0.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_S⇩0}) 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_S⇩0 cs (init_config w)"
proof -
from rel_R⇩1_init[of w] obtain cs1 n where
step1: "(st.init_config (map INP w), cs1) ∈ st.dstep" and
relR1: "rel_R⇩1 cs1 w n" and
n0: "n = 0"
by auto
from relR1
have "n + k ≤ length w ⟹ ∃ cs2. (cs1, cs2) ∈ st.dstep^^k ∧ rel_R⇩1 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_R⇩1_R⇩1[OF Suc(3) this assms] obtain cs3 where
step: "(cs1, cs3) ∈ st.dstep" and rel: "rel_R⇩1 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_R⇩1 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_R⇩1 cs2 w (length w)" by auto
from rel_R⇩1_R⇩2[OF rel assms] obtain cs3 n where step3: "(cs2, cs3) ∈ st.dstep"
and rel: "rel_R⇩2 cs3 w n" and n: "n = length w"
by auto
from rel have "∃ cs. (cs3, cs) ∈ st.dstep^^n ∧ rel_R⇩2 cs w 0"
proof (induction n arbitrary: cs3 rule: nat_induct)
case (Suc n cs3)
from rel_R⇩2_R⇩2[OF Suc(2) assms] obtain cs1 where
step: "(cs3, cs1) ∈ st.dstep" and rel: "rel_R⇩2 cs1 w n" by auto
from Suc.IH[OF rel] obtain cs where steps: "(cs1, cs) ∈ st.dstep ^^ n" and rel: "rel_R⇩2 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_R⇩2 cs4 w 0" by (auto simp: n)
from rel_R⇩2_S⇩0[OF rel assms] obtain cs where step5: "(cs4, cs) ∈ st.dstep" and
rel: "rel_S⇩0 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 (Config⇩M q tc p) i) ⟹
valid_config (Config⇩M q tc p) ⟹
(⋀ i. inp i = (if p i < p' then SYM (tc i (p i)) else ∙)) ⟹
rel_S (Config⇩S (S q inp) tc' (Suc p')) (Config⇩M q tc p) p'"

lemma rel_S⇩0_S: assumes "rel_S⇩0 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_S⇩0.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: "(S⇩0 q, ⊢, S q (λ_. ∙), ⊢, dir.R) ∈ δ'" unfolding δ'_def by auto
let ?cs1 = "Config⇩S (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 (Config⇩S (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 = "Config⇩S (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_S⇩1 :: "(('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 (Config⇩M q tc p) i) ⟹
valid_config (Config⇩M q tc p) ⟹
(⋀ i. inp i = tc i (p i)) ⟹
(⋀ i. p i < p') ⟹
p' = Suc (Max (range p)) ⟹
rel_S⇩1 (Config⇩S (S⇩1 q inp) tc' p') (Config⇩M q tc p)"

lemma rel_S_S⇩1: assumes "rel_S cs0 cm p'"
"p' = Suc (Max (range (mt_pos cm)))"
shows "∃ cs1. (cs0, cs1) ∈ st.dstep ∧ rel_S⇩1 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, S⇩1 q (project_inp inp), a, dir.L)) (q,inp,TUPLE t) ∈ δ'" unfolding δ'_def by blast
hence mem: "(S q inp, TUPLE t, S⇩1 q (project_inp inp), TUPLE t, dir.L) ∈ δ'" by simp
let ?cs1 = "Config⇩S (S⇩1 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_S⇩1 ?cs1 cm" unfolding cm
proof (intro rel_S⇩1.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_S⇩0}), and the multitape-TM is not in a final state,
then we can move to the end of the S-phase (in @{const rel_S⇩1}).›

lemma S_phase: assumes "rel_S⇩0 cs cm"
and "mt_state cm ∉ {t, r}"
shows "∃ cs'. (cs, cs') ∈ st.dstep^^(3 + Max (range (mt_pos cm))) ∧ rel_S⇩1 cs' cm"
proof -
let ?N = "Max (range (mt_pos cm))"
from rel_S⇩0_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_S⇩1[OF rel] obtain cs3 where step3: "(cs2,cs3) ∈ st.dstep" and rel: "rel_S⇩1 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)) ⟹
(Config⇩M q ts n, Config⇩M 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_E⇩0 :: "(('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 (Config⇩M q tc p) i) ⟹
valid_config (Config⇩M q tc p) ⟹
rule = (q,a,q1,b,d) ⟹
(Config⇩M q tc p, Config⇩M q1 tc1 p1) ∈ δstep rule ⟹
(⋀ i. p i < p') ⟹
p' = Suc (Max (range p)) ⟹
rel_E⇩0 (Config⇩S (E⇩0 q1 b d) tc' p') (Config⇩M q tc p) (Config⇩M 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_S⇩1_E⇩0_step: assumes "rel_S⇩1 cs cm"
and "(cm,cm1) ∈ step"
shows "∃ rule cs1. (cs, cs1) ∈ st.step ∧ rel_E⇩0 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_S⇩1.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). (S⇩1 q a, t, E⇩0 q' b d, t, dir.N)) (rule,tc' p') ∈ δ'"
unfolding δ'_def using tc' 2(3) by blast
hence mem: "(S⇩1 q a, tc' p', E⇩0 q1 b dir, tc' p', dir.N) ∈ δ'" by (auto simp: rule)
have inp_a: "inp = a" ```