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
```