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