Theory Multitape_Substrate_Core

theory Multitape_Substrate_Core
  imports "HOL-Library.FuncSet"
begin

section ‹Substrate core (Dalvit--Thiemann definition surface)›

text ‹The ∗‹definition surface› of the substrate, deliberately isolated
  in this theory: the datatypes, selectors, step relation, and the validity /
  configuration / language definitions --- and no proofs.  This is the part
  of the development that corresponds to the Dalvit--Thiemann AFP entry
  ‹Multitape_To_Singletape_TM› (its files ‹Multitape_TM› and
  ‹TM_Common›, about 180 lines), kept small so a reader can diff it
  directly against that source.  Every lemma --- the ‹valid_mttm›
  axiom-extraction toolkit, the validity-preservation and reachability
  results, and the displacement / left-endmarker tape tools, all
  ∗‹our› additions --- lives in the parent theory ‹Multitape_Substrate›,
  which imports this one.

  The datatypes (‹mttm›, ‹mt_config›, ‹dir›) and the step
  relation are adapted from that entry cite‹"Dalvit2022:verified"›;
  ‹valid_mttm› is a direct conjunction of the substrate's structural
  axioms (no locale wrapping), tightened beyond the AFP entry's
  ‹δLE› axiom by an additional LE-write conjunct (see the
  validity predicate below).

  The number of tapes is a ∗‹value›: a machine carries its tape count
  as a ‹nat› field ‹k›, and head contents are a total function
  ‹nat ⇒ 'a› with a ∗‹blank tail› beyond ‹k› (the
  support invariant).  This departs from the AFP source, where the
  tape count is trapped in a finite type parameter ‹'k›; the value
  form is what makes ‹∃ M› / ‹∀ M› over machines of all
  arities a single HOL proposition.›


subsection ‹TM-direction primitive (forked from AFP ‹TM_Common›)›

text ‹Three-valued TM head movement: right (R), left (L), or
  neutral / stay (N).  Used positionally as the fifth component
  of every transition tuple; functions ‹nat ⇒ dir› encode the
  per-tape head movement.›

datatype dir = R | L | N

fun go_dir :: "dir ⇒ nat ⇒ nat" where
  "go_dir R n = Suc n"
| "go_dir L n = n - 1"
| "go_dir N n = n"


subsection ‹Multitape-TM datatypes (forked from AFP ‹Multitape_TM›)›

text ‹Multi-tape Turing-machine descriptor.  Ten components: state
  set ‹Q›, input alphabet ‹Σ›, tape alphabet ‹Γ›, blank symbol,
  left endmarker, transition relation ‹δ›, start state, accept
  state, reject state, and tape count ‹k›.  The shape mirrors the
  AFP source (the ‹mttm› type abbreviations are a conscious
  near-copy), except the tape count, trapped in the AFP source's
  finite type parameter ‹'k›, is here the value-level ‹nat› field
  ‹k›; transition tuples index the tapes by ‹nat›, blank beyond ‹k›.
  Only the ‹Q_tm› and ‹Γ_tm› accessors are record-style — the
  others are positional with custom selectors below.›

datatype ('q, 'a) mttm = MTTM
  (Q_tm: "'q set")        ― ‹Q — states›
  "'a set"                ― ‹‹Σ› — input alphabet›
  (Γ_tm: "'a set")        ― ‹‹Γ› — tape alphabet›
  'a                      ― ‹blank›
  'a                      ― ‹left endmarker›
  "('q × (nat ⇒ 'a) × 'q × (nat ⇒ 'a) × (nat ⇒ dir)) set"
                          ― ‹transitions ‹δ››
  'q                      ― ‹start state›
  'q                      ― ‹accept state›
  'q                      ― ‹reject state›
  nat                     ― ‹‹k› — tape count›

text ‹Multitape-TM configuration: state, per-tape contents (each a
  function ‹nat ⇒ 'a› of cell positions), per-tape head positions.
  Tapes and heads are indexed by ‹nat›; tapes beyond the machine's
  count ‹k› are all-blank in a valid configuration.›

datatype ('a, 'q) mt_config = ConfigM
  (mt_state: 'q)
  "nat ⇒ nat ⇒ 'a"
  (mt_pos: "nat ⇒ nat")


subsection ‹Substrate selectors›

text ‹Positional selectors for the @{type mttm} datatype's
  components.  The datatype declares record-style accessors for
  @{const Q_tm} and @{const Γ_tm} only; the others
  (‹Σ›, ‹blank›, ‹LE›, ‹δ›, ‹s›, ‹t›, ‹r›, ‹k›) are positional.
  These selectors are simple positional pattern matches, named
  on the ‹*_tm› convention to match @{const Q_tm} / @{const Γ_tm}.›

fun bl_tm :: "('q, 'a) mttm ⇒ 'a" where
  "bl_tm (MTTM _ _ _ bl _ _ _ _ _ _) = bl"

fun le_tm :: "('q, 'a) mttm ⇒ 'a" where
  "le_tm (MTTM _ _ _ _ le _ _ _ _ _) = le"

fun delta_tm ::
  "('q, 'a) mttm
    ⇒ ('q × (nat ⇒ 'a) × 'q × (nat ⇒ 'a) × (nat ⇒ dir)) set" where
  "delta_tm (MTTM _ _ _ _ _ δ _ _ _ _) = δ"

fun s_tm :: "('q, 'a) mttm ⇒ 'q" where
  "s_tm (MTTM _ _ _ _ _ _ s _ _ _) = s"

fun t_tm :: "('q, 'a) mttm ⇒ 'q" where
  "t_tm (MTTM _ _ _ _ _ _ _ t _ _) = t"

fun r_tm :: "('q, 'a) mttm ⇒ 'q" where
  "r_tm (MTTM _ _ _ _ _ _ _ _ r _) = r"

fun Sigma_tm :: "('q, 'a) mttm ⇒ 'a set" where
  "Sigma_tm (MTTM _ Σ _ _ _ _ _ _ _ _) = Σ"

fun k_tm :: "('q, 'a) mttm ⇒ nat" where
  "k_tm (MTTM _ _ _ _ _ _ _ _ _ k) = k"

text ‹Tape-content selector for substrate configurations.  The
  substrate datatype names @{const mt_state} and @{const mt_pos}
  via record-style accessors but leaves the tape function
  unnamed; we add it positionally for symmetry.›

fun mt_tape :: "('a, 'q) mt_config ⇒ nat ⇒ nat ⇒ 'a" where
  "mt_tape (ConfigM _ ts _) = ts"


subsection ‹Step relation›

text ‹Inductive characterisation of the multitape-TM step
  relation, parametrised by the transition relation ‹δ› alone.
  Body verbatim equivalent to the AFP source (only the tape index
  moves from the type ‹'k› to ‹nat›); functional layer, so
  downstream Hoare-triple proofs invoke
  ‹mttm_step.intros› directly without any locale routing.›

inductive_set mttm_step ::
  "('q × (nat ⇒ 'a) × 'q × (nat ⇒ 'a) × (nat ⇒ dir)) set
    ⇒ ('a, 'q) mt_config rel"
  for δ
where
  step: "(q, (λk. ts k (n k)), q', a, dir) ∈ δ ⟹
   (ConfigM q ts n,
    ConfigM q' (λk. (ts k)(n k := a k)) (λk. go_dir (dir k) (n k)))
     ∈ mttm_step δ"


subsection ‹Substrate validity (functional axiom bundle)›

text ‹Functional bundle of the substrate's structural axioms.  This
  predicate enumerates the standard well-formedness conditions of
  Hopcroft and Ullman cite‹‹\S7.3› in "Hopcroft1979:introduction"›:
  finiteness of @{term Q} and @{term Γ}, alphabet inclusion, state
  membership for the start, accept, and reject states, blank /
  left-endmarker tape-alphabet membership (with @{term Σ}
  disjointness), accept @{text "≠"} reject, a positive tape count
  (the input tape ‹0› must exist), the range typing of the
  transition relation, the LE read-discipline, and the
  ∗‹support invariant›.

  The LE-discipline kept here is the read direction only: every
  ‹δ›-transition reading the left endmarker on tape ‹j› rewrites the
  LE position with itself and moves only ‹N› or ‹R› (boundary
  preservation).  The converse write direction — a transition writes
  the left endmarker on tape ‹j› only where it was already reading
  it — is ∗‹not› a validity requirement: it is factored out as the
  separate predicate ‹le_unique› (below), which well-formed machines
  carry but a machine that deliberately plants a fresh ‹le› — the
  origin-floating wrapper for the faithful Hopcroft--Ullman speed-up bound
  cite‹‹Theorem 12.4› in "Hopcroft1979:introduction"› — may forgo
  while staying valid.  Keeping the write direction out of validity is
  exactly what lets that wrapper's output be a legal machine.

  The support invariant — every transition is blank on reads and
  writes and stationary (‹N›) on moves at every tape index ‹j ≥ k›
  — is the value-level replacement for the AFP source's finite tape
  type: it confines a ‹k›-tape machine's transitions to tapes
  ‹0 … k - 1› and, with @{term Γ} finite, makes ‹δ› finite
  (@{text "valid_mttm_finite_delta"}).›

fun valid_mttm :: "('q, 'a) mttm ⇒ bool" where
  "valid_mttm (MTTM Q Σ Γ bl le δ s t r k) =
     (finite Q ∧
      finite Γ ∧
      Σ ⊆ Γ ∧
      s ∈ Q ∧
      t ∈ Q ∧
      r ∈ Q ∧
      bl ∈ Γ ∧
      bl ∉ Σ ∧
      le ∈ Γ ∧
      le ∉ Σ ∧
      t ≠ r ∧
      0 < k ∧
      δ ⊆ (Q - {t, r}) × (UNIV → Γ) × Q × (UNIV → Γ) × (UNIV → UNIV) ∧
      (∀q a q' a' d j. (q, a, q', a', d) ∈ δ ⟶ a j = le ⟶
                         a' j = le ∧ d j ∈ {dir.N, dir.R}) ∧
      (∀q a q' a' d. (q, a, q', a', d) ∈ δ ⟶
                       (∀j ≥ k. a j = bl ∧ a' j = bl ∧ d j = dir.N)))"

text ‹The left-endmarker write discipline, as a standalone predicate:
  a transition writes the left endmarker @{term "le_tm M"} on a tape
  only where it was already reading it — the endmarker is never freshly
  planted.  This was formerly a clause of @{const valid_mttm}; it is
  kept separate precisely so a machine that *does* plant a fresh ‹le› —
  the origin-floating wrapper for the faithful Theorem 12.4 bound — is still
  @{const valid_mttm}, while the alphabet-transformation chain, which
  needs the property of the machine it simulates, carries it explicitly
  (folded into ‹well_formed_mttm› and threaded to the simulation
  lemmas through ‹valid_mttm_deltaLE_no_write›).›

definition le_unique :: "('q, 'a) mttm ⇒ bool" where
  "le_unique M =
     (∀q a q' a' d j. (q, a, q', a', d) ∈ delta_tm M ⟶
                        a' j = le_tm M ⟶ a j = le_tm M)"

text ‹Strengthening of @{const valid_mttm} with the three
  non-degeneracy conditions used by every linear-speedup-style
  theorem — distinct start / accept / reject states and distinct
  left-endmarker / blank tape symbols — plus the left-endmarker
  write discipline @{const le_unique}.  Bundles
  @{term "valid_mttm M"}, @{term "s_tm M ≠ t_tm M"},
  @{term "s_tm M ≠ r_tm M"}, @{term "le_tm M ≠ bl_tm M"}, and
  @{term "le_unique M"} into a single predicate so downstream
  statements need only one assumption clause instead of five.  Since
  @{const le_unique} is no longer implied by @{const valid_mttm} — it is
  exactly the clause the faithful-12.4 wrapper forgoes — it is
  load-bearing here: ‹well_formed_mttm› is the
  alphabet-transformation chain's carrier of LE-uniqueness, threaded to
  the simulation lemmas that need it.›

abbreviation well_formed_mttm
  :: "('q, 'a) mttm ⇒ bool"
where
  "well_formed_mttm M ≡
     valid_mttm M
     ∧ s_tm M ≠ t_tm M
     ∧ s_tm M ≠ r_tm M
     ∧ le_tm M ≠ bl_tm M
     ∧ le_unique M"


subsection ‹Configuration validity›

text ‹Functional re-exposition of the substrate's per-configuration
  validity invariant: state in @{term Q}, every tape's contents
  drawn from @{term Γ}, every ∗‹active› tape (index ‹i < k›)
  carries the left endmarker at position 0, and every ∗‹inactive›
  tape (index ‹i ≥ k›) is all-blank (the configuration-level support
  invariant — inactive tapes carry the blank symbol everywhere, not
  the left endmarker, since ‹bl ≠ le›).›

fun valid_config_mttm ::
  "('q, 'a) mttm ⇒ ('a, 'q) mt_config ⇒ bool"
where
  "valid_config_mttm (MTTM Q _ Γ bl le _ _ _ _ k) (ConfigM q ts _) =
     (q ∈ Q
      ∧ (∀i. range (ts i) ⊆ Γ)
      ∧ (∀i<k. ts i 0 = le)
      ∧ (∀i≥k. ∀p. ts i p = bl))"

text ‹Functional initial configuration: take ‹M› as parameter,
  pull start state, blank, left endmarker, and tape count
  positionally.  Active tapes (index ‹i < k›) carry the left
  endmarker at position 0 and, on the input tape ‹0›, the input
  ‹w›; inactive tapes (index ‹i ≥ k›) are all-blank.›

fun init_config_mttm ::
  "('q, 'a) mttm ⇒ 'a list ⇒ ('a, 'q) mt_config"
where
  "init_config_mttm (MTTM _ _ _ bl le _ s _ _ k) w =
     ConfigM s
       (λi n. if i < k
              then (if n = 0 then le
                    else if i = 0 ∧ n ≤ length w then w ! (n - 1)
                    else bl)
              else bl)
       (λ_. 0)"


subsection ‹Language and time-bound predicates›

text ‹Functional analogues of the AFP's @{text "Lang_mttm"}
  and @{text "det_mttm"} top-level wrappers, plus the
  weak-acceptance predicate @{text "accepts_in_time_mttm"}.
  @{text "Lang_mttm"} is the set of inputs over @{term "Sigma_tm M"}
  that drive @{term M} from its initial configuration to the accept
  state @{term "t_tm M"}.  @{text "det_mttm"} says the transition
  relation is single-valued: each source state together with the
  symbols read admits at most one outcome — one next state, one
  written-symbol tuple, one head-move tuple — so a configuration has
  at most one successor.  This is the determinism hypothesis on
  which the alphabet-enlargement reverse direction turns.  Bodies
  routed through the functional @{const init_config_mttm} and
  @{const mttm_step} rather than through locale-internal
  definitions.  Used by the AE / AR language- and time-preservation
  theorems.›

definition Lang_mttm :: "('q, 'a) mttm ⇒ 'a list set" where
  "Lang_mttm M =
     {w. set w ⊆ Sigma_tm M ∧
         (∃w' n. (init_config_mttm M w, ConfigM (t_tm M) w' n)
                    ∈ (mttm_step (delta_tm M))*)}"

definition det_mttm :: "('q, 'a) mttm ⇒ bool" where
  "det_mttm M =
     (∀q a p1 b1 d1 p2 b2 d2.
        (q, a, p1, b1, d1) ∈ delta_tm M ⟶
        (q, a, p2, b2, d2) ∈ delta_tm M ⟶
        (p1, b1, d1) = (p2, b2, d2))"

text ‹Weak time-bounded acceptance: M accepts input @{term w} in
  time at most @{term t} iff some accepting path of length @{term
  "n ≤ t"} exists from @{const init_config_mttm} to a config in
  state @{term "t_tm M"}.  This matches the existential
  accepting-path shape that the alphabet-enlargement top-level
  theorems preserve.  Non-accepting paths are not constrained,
  in contrast to a universal worst-case bound that would
  constrain every path regardless of acceptance.

  Used by @{text "alphabet_enlarge_language"} and
  @{text "alphabet_enlarge_time"}.›

definition accepts_in_time_mttm ::
  "('q, 'a) mttm ⇒ 'a list ⇒ nat ⇒ bool" where
  "accepts_in_time_mttm M w t =
     (∃n cM_n. n ≤ t
                ∧ (init_config_mttm M w, cM_n) ∈ (mttm_step (delta_tm M))^^n
                ∧ mt_state cM_n = t_tm M)"

end