# Theory Singletape_TM

```section ‹Singletape Turing Machines›

theory Singletape_TM
imports
TM_Common
begin

text ‹Turing machines can be either defined via a datatype or via a locale.
We use TMs with left endmarker and dedicated accepting and rejecting state from
which no further transitions are allowed. Deterministic TMs can be partial.›

datatype ('q,'a)tm = TM
(Q_tm: "'q set")   (* Q - states *)
"'a set"   (* Sigma - input alphabet *)
(Γ_tm: "'a set")   (* Gamma - tape alphabet *)
'a         (* blank *)
'a         (* left endmarker *)
"('q × 'a × 'q × 'a × dir) set" (* transitions δ *)
'q         (* start state *)
'q         (* accept state *)
'q         (* reject state *)

datatype ('a, 'q) st_config = Config⇩S
"'q"         (* state *)
"nat ⇒ 'a"  (* tape content *)
"nat"        (* tape position *)

locale singletape_tm =
fixes
Q :: "'q set" and
Σ :: "'a set" and
Γ :: "'a set" and
blank :: 'a and
LE :: 'a and
δ :: "('q × 'a × 'q × 'a × dir) set" and
s :: 'q and
t :: 'q and
r :: 'q
assumes
fin_Q: "finite Q" and
fin_Γ: "finite Γ" and
Σ_sub_Γ: "Σ ⊆ Γ" and
sQ: "s ∈ Q" and
tQ: "t ∈ Q" and
rQ: "r ∈ Q" and
blank: "blank ∈ Γ" "blank ∉ Σ" and
LE: "LE ∈ Γ" "LE ∉ Σ" and
tr: "t ≠ r" and
δ_set: "δ ⊆ (Q - {t,r}) × Γ × Q × Γ × UNIV" and
δLE: "(q, LE, q', a', d) ∈ δ ⟹ a' = LE ∧ d ∈ {dir.N,dir.R}"
begin

lemma δ: assumes "(q,a,q',b,d) ∈ δ"
shows "q ∈ Q" "a ∈ Γ" "q' ∈ Q" "b ∈ Γ"
using assms δ_set by auto

lemma finΣ: "finite Σ"
using fin_Γ Σ_sub_Γ by (metis finite_subset)

lemmas tm = sQ Σ_sub_Γ blank(1) LE(1)

fun valid_config :: "('a, 'q) st_config ⇒ bool" where
"valid_config (Config⇩S q w n) = (q ∈ Q ∧ range w ⊆ Γ)"

definition init_config :: "'a list  ⇒ ('a,'q)st_config" where
"init_config w = (Config⇩S s (λ n. if n = 0 then LE else if n ≤ length w then w ! (n-1) else blank) 0)"

lemma valid_init_config: "set w ⊆ Σ ⟹ valid_config (init_config w)"
unfolding init_config_def valid_config.simps using tm by (force simp: set_conv_nth)

inductive_set step :: "('a, 'q) st_config rel" where
step: "(q, ts n, q', a, dir) ∈ δ ⟹
(Config⇩S q ts n, Config⇩S q' (ts(n := a)) (go_dir dir n)) ∈ step"

lemma stepI: "(q, a, q', b, dir) ∈ δ ⟹ ts n = a ⟹ ts' = ts(n := b) ⟹ n' = go_dir dir n ⟹ q1 = q ⟹ q2 = q'
⟹ (Config⇩S q1 ts n, Config⇩S q2 ts' n') ∈ step"
using step[of q ts n q' b dir] by auto

lemma valid_step: assumes step: "(α,β) ∈ step"
and val: "valid_config α"
shows "valid_config β"
using step
proof (cases rule: step.cases)
case (step q ts n q' a dir)
from δ[OF step(3)] val
show ?thesis unfolding step(1-2) by auto
qed

definition Lang :: "'a list set" where
"Lang = {w . set w ⊆ Σ ∧ (∃ w' n. (init_config w, Config⇩S t w' n) ∈ step^*)}"

definition deterministic where
"deterministic = (∀ q a p1 b1 d1 p2 b2 d2. (q,a,p1,b1,d1) ∈ δ ⟶ (q,a,p2,b2,d2) ∈ δ ⟶ (p1,b1,d1) = (p2,b2,d2))"

definition upper_time_bound :: "(nat ⇒ nat) ⇒ bool" where
"upper_time_bound f = (∀ w c n. set w ⊆ Σ ⟶ (init_config w, c) ∈ step^^n ⟶ n ≤ f (length w))"
end

fun valid_tm :: "('q,'a)tm ⇒ bool" where
"valid_tm (TM Q Σ Γ bl le δ s t r) = singletape_tm Q Σ Γ bl le δ s t r"

fun Lang_tm :: "('q,'a)tm ⇒ 'a list set" where
"Lang_tm (TM Q Σ Γ bl le δ s t r) = singletape_tm.Lang Σ bl le δ s t"

fun det_tm :: "('q,'a)tm ⇒ bool" where
"det_tm (TM Q Σ Γ bl le δ s t r) = singletape_tm.deterministic δ"

fun upperb_time_tm :: "('q,'a)tm ⇒ (nat ⇒ nat) ⇒ bool" where
"upperb_time_tm (TM Q Σ Γ bl le δ s t r) f = singletape_tm.upper_time_bound Σ bl le δ s f"

context singletape_tm
begin

text ‹A deterministic step (in a potentially non-determistic TM) is a step without alternatives.
This will be useful in the translation of multitape TMs. The simulation is mostly deterministic, and
only at very specific points it is non-determistic, namely at the points where the multitape-TM transition
is chosen.›

inductive_set dstep :: "('a, 'q) st_config rel" where
dstep: "(q, ts n, q', a, dir) ∈ δ ⟹
(⋀ q1' a1 dir1. (q, ts n, q1', a1, dir1) ∈ δ ⟹ (q1',a1,dir1) = (q',a,dir)) ⟹
(Config⇩S q ts n, Config⇩S q' (ts(n := a)) (go_dir dir n)) ∈ dstep"

lemma dstepI: "(q, a, q', b, dir) ∈ δ ⟹ ts n = a ⟹ ts' = ts(n := b) ⟹ n' = go_dir dir n ⟹ q1 = q ⟹ q2 = q'
⟹ (⋀ q'' b' dir'. (q, a, q'', b', dir') ∈ δ ⟹ (q'', b', dir') = (q',b,dir))
⟹ (Config⇩S q1 ts n, Config⇩S q2 ts' n') ∈ dstep"
using dstep[of q ts n q' b dir] by blast

lemma dstep_step: "dstep ⊆ step"
proof
fix st
assume dstep: "st ∈ dstep"
obtain s t where st: "st = (s,t)" by force
have "(s,t) ∈ step" using dstep[unfolded st]
proof (cases rule: dstep.cases)
case 1: (dstep q ts n q' a dir)
show ?thesis unfolding 1(1-2) by (rule stepI[OF 1(3)], auto)
qed
thus "st ∈ step" using st by auto
qed

lemma dstep_inj: assumes "(x,y) ∈ dstep"
and "(x,z) ∈ step"
shows "z = y"
using assms(2)
proof (cases)
case 1: (step q ts n p a d)
show ?thesis using assms(1) unfolding 1(1)
proof cases
case 2: (dstep p' a' d')
from 2(3)[OF 1(3)] have id: "p' = p" "a' = a" "d' = d" by auto
show ?thesis unfolding 1 2 id ..
qed
qed

lemma dsteps_inj: assumes "(x,y) ∈ dstep^^n"
and "(x,z) ∈ step^^m"
and "¬ (∃ u. (z,u) ∈ step)"
shows "∃ k. m = n + k ∧ (y,z) ∈ step^^k"
using assms(1-2)
proof (induct n arbitrary: m x)
case (Suc n m x)
from Suc(2) obtain x' where step: "(x,x') ∈ dstep" and steps: "(x',y) ∈ dstep^^n" by (metis relpow_Suc_E2)
from step dstep_step have "(x,x') ∈ step" by auto
with assms(3) have "x ≠ z" by auto
with Suc(3) obtain mm where m: "m = Suc mm" by (cases m, auto)
from Suc(3)[unfolded this] obtain x'' where step': "(x,x'') ∈ step" and steps': "(x'',z) ∈ step^^mm" by (metis relpow_Suc_E2)
from dstep_inj[OF step step'] have x'': "x'' = x'" by auto
from Suc(1)[OF steps steps'[unfolded x'']] obtain k where mm: "mm = n + k" and steps: "(y, z) ∈ step ^^ k" by auto
thus ?case unfolding m mm by auto
qed auto

lemma dsteps_inj': assumes "(x,y) ∈ dstep^^n"
and "(x,z) ∈ step^^m"
and "m ≥ n"
shows "∃ k. m = n + k ∧ (y,z) ∈ step^^k"
using assms(1-3)
proof (induct n arbitrary: m x)
case (Suc n m x)
from Suc(2) obtain x' where step: "(x,x') ∈ dstep" and steps: "(x',y) ∈ dstep^^n" by (metis relpow_Suc_E2)
from step dstep_step have "(x,x') ∈ step" by auto
with Suc obtain mm where m: "m = Suc mm" by (cases m, auto)
from Suc(3)[unfolded this] obtain x'' where step': "(x,x'') ∈ step" and steps': "(x'',z) ∈ step^^mm" by (metis relpow_Suc_E2)
from dstep_inj[OF step step'] have x'': "x'' = x'" by auto
from Suc(1)[OF steps steps'[unfolded x'']] m Suc obtain k where mm: "mm = n + k" and steps: "(y, z) ∈ step ^^ k" by auto
thus ?case unfolding m mm by auto
qed auto
end
end
```