# 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"}.›