Theory Multitape_TM

section ‹Multitape Turing Machines›

theory Multitape_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.

  Having multiple tapes, tape positions, directions, etc. is modelled via functions 
  of type @{typ "'k ⇒ 'whatever"} for some finite index type @{typ "'k :: finite"}.

  The input will always be provided on the first tape, indexed by @{term "0 :: 'k :: zero"}.›

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

datatype ('a,'q,'k) mt_config = Config⇩M
  (mt_state: 'q)                  (* state *)
  "'k ⇒ nat ⇒ 'a"        (* k tape contents *)
  (mt_pos: "'k ⇒ nat")    (* k tape positions *)

locale multitape_tm =
  fixes 
    Q :: "'q set" and
    Σ :: "'a set" and
    Γ :: "'a set" and
    blank :: 'a and
    LE :: 'a and
    δ :: "('q × ('k ⇒ 'a) × 'q × ('k ⇒ 'a) × ('k :: {finite,zero} ⇒ 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}) × (UNIV → Γ) × Q × (UNIV → Γ) × (UNIV → UNIV)" and
    δLE: "(q, a, q', a', d) ∈ δ ⟹ a k = LE ⟹ a' k = LE ∧ d k ∈ {dir.N,dir.R}"
begin

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

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

lemma fin_δ: "finite δ" 
  by (intro finite_subset[OF δ_set] finite_cartesian_product fin_funcsetI, insert fin_Q fin_Γ, auto)

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

fun valid_config :: "('a, 'q, 'k) mt_config ⇒ bool" where
  "valid_config (Config⇩M q w n) = (q ∈ Q ∧ (∀ k. range (w k) ⊆ Γ) ∧ (∀ k. w k 0 = LE))"

definition init_config :: "'a list  ⇒ ('a,'q,'k)mt_config" where
  "init_config w = (Config⇩M s (λ k n. if n = 0 then LE else if k = 0 ∧ 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, 'k) mt_config rel" where
  step: "(q, (λ k. ts k (n k)), q', a, dir) ∈ δ ⟹
  (Config⇩M q ts n, Config⇩M q' (λ k. (ts k)(n k := a k)) (λ k. go_dir (dir k) (n k))) ∈ step"

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 δLE step(3)
  show ?thesis unfolding step(1-2) by fastforce
qed

definition Lang :: "'a list set" where
  "Lang = {w . set w ⊆ Σ ∧ (∃ w' n. (init_config w, Config⇩M 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_mttm :: "('q,'a,'k :: {finite,zero})mttm ⇒ bool" where 
  "valid_mttm (MTTM Q Σ Γ bl le δ s t r) = multitape_tm Q Σ Γ bl le δ s t r" 

fun Lang_mttm :: "('q,'a,'k :: {finite,zero})mttm ⇒ 'a list set" where
  "Lang_mttm (MTTM Q Σ Γ bl le δ s t r) = multitape_tm.Lang Σ bl le δ s t" 

fun det_mttm :: "('q,'a,'k :: {finite,zero})mttm ⇒ bool" where
  "det_mttm (MTTM Q Σ Γ bl le δ s t r) = multitape_tm.deterministic δ" 

fun upperb_time_mttm :: "('q,'a,'k :: {finite, zero})mttm ⇒ (nat ⇒ nat) ⇒ bool" where
  "upperb_time_mttm (MTTM Q Σ Γ bl le δ s t r) f = multitape_tm.upper_time_bound Σ bl le δ s f" 


end