Theory Multitape_Finite_Control

theory Multitape_Finite_Control
  imports Multitape_Substrate
begin

section ‹Finite-control small-input recogniser›

text ‹A reusable substrate construction for the ubiquitous low-level
  move: finitely many bounded-length inputs are decided directly by
  the finite control, reading the input in a fixed number of moves;
  only longer inputs need run a real machine.

  This theory provides the atom ∗‹finite recogniser›: given a finite
  input alphabet ‹Sg›, a concrete tape alphabet ‹Gamma› with a blank
  and a left endmarker, a finite set ‹F› of words over ‹Sg›, and a
  tape count ‹k›, it builds a deterministic machine that decides ‹F›
  --- accepting each member reading only its input.  The combinator
  ∗‹finite patch›, which reuses the recogniser on short inputs and
  hands off to an arbitrary machine on long inputs, is built on top.

  The construction is read-only: it never modifies the tape (the
  write component of every transition equals its read component), so
  the left-endmarker write discipline is vacuous and only the head
  movement carries the left-endmarker read discipline.›


subsection ‹Recogniser state space›

text ‹Three phases: @{text "FR_Scan u"} has read the prefix ‹u› of the
  input so far, @{text FR_Acc} has accepted, @{text FR_Rej} has
  rejected.  The scan payload ranges over words of length at most the
  recogniser's cutoff, so the state set is finite.›

datatype 'a fr_state = FR_Scan "'a list" | FR_Acc | FR_Rej


subsection ‹Recogniser transition components›

text ‹The read/write tuple for a step reading symbol ‹x› on the input
  tape ‹0›: tape ‹0› carries ‹x›, every other active tape (index
  ‹1 ≤ j < k›) reads the left endmarker ‹le› (its head never leaves
  position ‹0›), and every inactive tape (index ‹j ≥ k›) reads the
  blank ‹bl› (the support invariant).›

definition fr_read :: "'a ⇒ 'a ⇒ nat ⇒ 'a ⇒ (nat ⇒ 'a)" where
  "fr_read bl le k x = (λj. if j = 0 then x else if j < k then le else bl)"

text ‹The head-move tuple: tape ‹0› moves by ‹d›, every other tape
  stays put.  This meets the support invariant (‹N› beyond ‹k›) and,
  paired with @{const fr_read}, the left-endmarker read discipline.›

definition fr_move :: "dir ⇒ (nat ⇒ dir)" where
  "fr_move d = (λj. if j = 0 then d else dir.N)"


subsection ‹Recogniser cutoff and transition relation›

text ‹The scan cutoff: an upper bound on the length of every word in
  ‹F› (the maximum length, or ‹0› when ‹F› is empty).  Inputs longer
  than the cutoff cannot be in ‹F›, so the scan rejects them on the
  overflow read.›

definition fr_N :: "'a list set ⇒ nat" where
  "fr_N F = (if F = {} then 0 else Max (length ` F))"

text ‹The recogniser transition relation.  Five families, all with
  write component equal to read component:
  ▪ advance past the left endmarker (start step);
  ▪ extend the scanned prefix by one symbol while below the cutoff;
  ▪ overflow: reading a symbol at the cutoff rejects (input too long);
  ▪ end-of-input on a member prefix accepts;
  ▪ end-of-input on a non-member prefix rejects.›

definition fr_delta ::
  "'a set ⇒ 'a ⇒ 'a ⇒ 'a list set ⇒ nat ⇒ nat
     ⇒ ('a fr_state × (nat ⇒ 'a) × 'a fr_state
          × (nat ⇒ 'a) × (nat ⇒ dir)) set"
where
  "fr_delta Sg bl le F k N =
     { (FR_Scan [], fr_read bl le k le, FR_Scan [],
        fr_read bl le k le, fr_move dir.R) }
     ∪ { (FR_Scan u, fr_read bl le k x, FR_Scan (u @ [x]),
          fr_read bl le k x, fr_move dir.R)
         | u x. set u ⊆ Sg ∧ length u < N ∧ x ∈ Sg }
     ∪ { (FR_Scan u, fr_read bl le k x, FR_Rej,
          fr_read bl le k x, fr_move dir.N)
         | u x. set u ⊆ Sg ∧ length u = N ∧ x ∈ Sg }
     ∪ { (FR_Scan u, fr_read bl le k bl, FR_Acc,
          fr_read bl le k bl, fr_move dir.N)
         | u. set u ⊆ Sg ∧ length u ≤ N ∧ u ∈ F }
     ∪ { (FR_Scan u, fr_read bl le k bl, FR_Rej,
          fr_read bl le k bl, fr_move dir.N)
         | u. set u ⊆ Sg ∧ length u ≤ N ∧ u ∉ F }"


subsection ‹The recogniser machine›

text ‹The finite recogniser over input alphabet ‹Sg›, tape alphabet
  ‹Gamma›, blank ‹bl›, left endmarker ‹le›, word set ‹F›, and tape
  count ‹k›.  Its state set is the scannable prefixes (words over ‹Sg›
  up to the cutoff) plus the two halting states; the start state is
  the empty scan.›

definition finite_recogniser ::
  "'a set ⇒ 'a set ⇒ 'a ⇒ 'a ⇒ 'a list set ⇒ nat
     ⇒ ('a fr_state, 'a) mttm"
where
  "finite_recogniser Sg Gamma bl le F k =
     MTTM
       (FR_Scan ` {u. set u ⊆ Sg ∧ length u ≤ fr_N F} ∪ {FR_Acc, FR_Rej})
       Sg
       Gamma
       bl
       le
       (fr_delta Sg bl le F k (fr_N F))
       (FR_Scan [])
       FR_Acc
       FR_Rej
       k"


subsection ‹Component accessors›

lemma finite_recogniser_k_tm:
  "k_tm (finite_recogniser Sg Gamma bl le F k) = k"
  by (simp add: finite_recogniser_def)

lemma finite_recogniser_Sigma_tm:
  "Sigma_tm (finite_recogniser Sg Gamma bl le F k) = Sg"
  by (simp add: finite_recogniser_def)

lemma finite_recogniser_Gamma_tm:
  "Γ_tm (finite_recogniser Sg Gamma bl le F k) = Gamma"
  by (simp add: finite_recogniser_def)

lemma finite_recogniser_bl_tm:
  "bl_tm (finite_recogniser Sg Gamma bl le F k) = bl"
  by (simp add: finite_recogniser_def)

lemma finite_recogniser_le_tm:
  "le_tm (finite_recogniser Sg Gamma bl le F k) = le"
  by (simp add: finite_recogniser_def)

lemma finite_recogniser_s_tm:
  "s_tm (finite_recogniser Sg Gamma bl le F k) = FR_Scan []"
  by (simp add: finite_recogniser_def)

lemma finite_recogniser_t_tm:
  "t_tm (finite_recogniser Sg Gamma bl le F k) = FR_Acc"
  by (simp add: finite_recogniser_def)

lemma finite_recogniser_r_tm:
  "r_tm (finite_recogniser Sg Gamma bl le F k) = FR_Rej"
  by (simp add: finite_recogniser_def)

lemma finite_recogniser_Q_tm:
  "Q_tm (finite_recogniser Sg Gamma bl le F k)
     = FR_Scan ` {u. set u ⊆ Sg ∧ length u ≤ fr_N F} ∪ {FR_Acc, FR_Rej}"
  by (simp add: finite_recogniser_def)

lemma finite_recogniser_delta_tm:
  "delta_tm (finite_recogniser Sg Gamma bl le F k)
     = fr_delta Sg bl le F k (fr_N F)"
  by (simp add: finite_recogniser_def)


subsection ‹Transition-relation discipline›

text ‹Every recogniser transition writes back exactly what it reads:
  the recogniser never modifies the tape.  This makes the
  left-endmarker ∗‹write› discipline (@{const le_unique}) vacuous.›

lemma fr_delta_no_write:
  "(q, a, q', a', d) ∈ fr_delta Sg bl le F k N ⟹ a' = a"
  by (auto simp: fr_delta_def)

text ‹The read tuple is injective in the tape-‹0› symbol (its value
  there), so a transition's read component determines the symbol
  scanned.  This is the discriminator behind determinism.›

lemma fr_read_inj:
  "fr_read bl le k x = fr_read bl le k y ⟹ x = y"
proof -
  assume "fr_read bl le k x = fr_read bl le k y"
  hence "fr_read bl le k x 0 = fr_read bl le k y 0" by simp
  thus "x = y" by (simp add: fr_read_def)
qed

text ‹The support invariant: at every inactive tape index ‹j ≥ k›,
  each transition reads and writes the blank and stays put.›

lemma fr_delta_support:
  assumes "0 < k"
    and "(q, a, q', a', d) ∈ fr_delta Sg bl le F k N"
    and "k ≤ j"
  shows "a j = bl ∧ a' j = bl ∧ d j = dir.N"
  using assms by (auto simp: fr_delta_def fr_read_def fr_move_def)

text ‹No recogniser transition ever moves left: the input tape moves
  ‹R› or stays, and every other tape stays put.›

lemma fr_delta_move_no_L:
  "(q, a, q', a', d) ∈ fr_delta Sg bl le F k N ⟹ d j ∈ {dir.N, dir.R}"
  by (auto simp: fr_delta_def fr_move_def split: if_splits)

text ‹The left-endmarker read discipline: a transition reading ‹le› on
  tape ‹j› writes ‹le› back there (read-only) and moves only ‹N› or
  ‹R› (never-left).  Both halves fall out of the two facts above,
  needing no alphabet side-conditions.›

lemma fr_delta_LE:
  assumes "(q, a, q', a', d) ∈ fr_delta Sg bl le F k N"
    and "a j = le"
  shows "a' j = le ∧ d j ∈ {dir.N, dir.R}"
  using fr_delta_no_write[OF assms(1)] fr_delta_move_no_L[OF assms(1)] assms(2)
  by simp


subsection ‹Well-formedness›

text ‹The recogniser is a valid substrate machine.  The alphabet must
  be finite with the blank and left endmarker inside ‹Gamma› but
  outside ‹Sg›, and the tape count positive --- the standard machine
  hypotheses, exactly the data a concrete machine (or the combinator
  @{term finite_patch} built on this one) already carries.›

lemma finite_recogniser_valid:
  assumes finG: "finite Gamma"
    and SgG:  "Sg ⊆ Gamma"
    and blG:  "bl ∈ Gamma"
    and blS:  "bl ∉ Sg"
    and leG:  "le ∈ Gamma"
    and leS:  "le ∉ Sg"
    and kpos: "0 < k"
  shows "valid_mttm (finite_recogniser Sg Gamma bl le F k)"
proof -
  have finSg: "finite Sg" using finite_subset[OF SgG finG] .
  have finP: "finite {u. set u ⊆ Sg ∧ length u ≤ fr_N F}"
    using finite_lists_length_le[OF finSg] by blast
  have finQ: "finite (FR_Scan ` {u. set u ⊆ Sg ∧ length u ≤ fr_N F}
                       ∪ {FR_Acc, FR_Rej})"
    using finP by simp
  have shape: "fr_delta Sg bl le F k (fr_N F)
      ⊆ (FR_Scan ` {u. set u ⊆ Sg ∧ length u ≤ fr_N F} ∪ {FR_Acc, FR_Rej}
           - {FR_Acc, FR_Rej})
         × (UNIV → Gamma)
         × (FR_Scan ` {u. set u ⊆ Sg ∧ length u ≤ fr_N F} ∪ {FR_Acc, FR_Rej})
         × (UNIV → Gamma)
         × (UNIV → UNIV)"
    unfolding fr_delta_def fr_read_def
    using SgG blG leG by (auto simp: Pi_iff)
  have LEc: "∀q a q' a' d j.
      (q, a, q', a', d) ∈ fr_delta Sg bl le F k (fr_N F)
        ⟶ a j = le ⟶ a' j = le ∧ d j ∈ {dir.N, dir.R}"
    by (auto dest: fr_delta_LE)
  have suppc: "∀q a q' a' d.
      (q, a, q', a', d) ∈ fr_delta Sg bl le F k (fr_N F)
        ⟶ (∀j ≥ k. a j = bl ∧ a' j = bl ∧ d j = dir.N)"
    by (auto dest: fr_delta_support[OF kpos])
  show ?thesis
    unfolding finite_recogniser_def valid_mttm.simps
    using finQ finG SgG blG blS leG leS kpos shape LEc suppc
    by (intro conjI) auto
qed

text ‹The recogniser is well-formed in the strengthened sense
  (@{const well_formed_mttm}): distinct start / accept / reject and
  distinct endmarker / blank, plus the left-endmarker write discipline
  --- the last free from read-only-ness.›

lemma finite_recogniser_well_formed:
  assumes finG: "finite Gamma"
    and SgG:  "Sg ⊆ Gamma"
    and blG:  "bl ∈ Gamma"
    and blS:  "bl ∉ Sg"
    and leG:  "le ∈ Gamma"
    and leS:  "le ∉ Sg"
    and blle: "bl ≠ le"
    and kpos: "0 < k"
  shows "well_formed_mttm (finite_recogniser Sg Gamma bl le F k)"
proof -
  have lu: "le_unique (finite_recogniser Sg Gamma bl le F k)"
    unfolding le_unique_def finite_recogniser_delta_tm
    by (auto dest: fr_delta_no_write)
  have vd: "valid_mttm (finite_recogniser Sg Gamma bl le F k)"
    by (rule finite_recogniser_valid[OF finG SgG blG blS leG leS kpos])
  show ?thesis
    using vd lu blle
    by (auto simp: finite_recogniser_s_tm finite_recogniser_t_tm
                   finite_recogniser_r_tm finite_recogniser_le_tm
                   finite_recogniser_bl_tm)
qed


subsection ‹Determinism›

text ‹The recogniser is deterministic.  The source state fixes the
  scanned prefix (constructor injectivity) and the read component
  fixes the scanned symbol (@{thm fr_read_inj}); the five transition
  families are then pairwise disjoint because the left endmarker, the
  blank, and the input alphabet are pairwise distinct.›

lemma finite_recogniser_det:
  assumes leS: "le ∉ Sg" and blS: "bl ∉ Sg" and blle: "bl ≠ le"
  shows "det_mttm (finite_recogniser Sg Gamma bl le F k)"
  unfolding det_mttm_def finite_recogniser_delta_tm fr_delta_def
  using leS blS blle by (auto dest: fr_read_inj)


subsection ‹The accepting run›

text ‹The configuration after the recogniser has read the left
  endmarker and the first ‹m› input symbols: state @{text "FR_Scan
  (take m w)"}, the (read-only, hence unchanging) input tape, and the
  input head at position ‹m + 1›.›

definition fr_run_config ::
  "'a ⇒ 'a ⇒ nat ⇒ 'a list ⇒ nat ⇒ ('a, 'a fr_state) mt_config"
where
  "fr_run_config bl le k w m =
     Config⇩M (FR_Scan (take m w))
       (λ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)
       (λi. if i = 0 then m + 1 else 0)"

text ‹One scan step: from the length-‹m› scan configuration, reading
  the ‹(m+1)›-th input symbol advances to the length-‹(Suc m)› one,
  provided the input still has a symbol there (‹m < length w›) and the
  cutoff is not yet reached (‹m < fr_N F›).›

lemma fr_scan_step:
  assumes kpos: "0 < k" and mlt: "m < length w" and mN: "m < fr_N F"
    and wSg: "set w ⊆ Sg"
  shows "(fr_run_config bl le k w m, fr_run_config bl le k w (Suc m))
           ∈ mttm_step (fr_delta Sg bl le F k (fr_N F))"
proof -
  let ?x = "w ! m"
  let ?ts = "λ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"
  let ?nn = "λi::nat. if i = 0 then m + 1 else 0"
  have xSg: "?x ∈ Sg" using nth_mem[OF mlt] wSg by blast
  have lenu: "length (take m w) = m" using mlt by simp
  have takeq: "take (Suc m) w = take m w @ [?x]"
    using mlt by (simp add: take_Suc_conv_app_nth)
  have setu: "set (take m w) ⊆ Sg"
    using wSg by (meson set_take_subset subset_trans)
  have read_eq: "(λi. ?ts i (?nn i)) = fr_read bl le k ?x"
  proof (rule ext)
    fix i show "?ts i (?nn i) = fr_read bl le k ?x i"
      using kpos mlt by (cases "i = 0") (auto simp: fr_read_def)
  qed
  have tr: "(FR_Scan (take m w), fr_read bl le k ?x, FR_Scan (take (Suc m) w),
             fr_read bl le k ?x, fr_move dir.R) ∈ fr_delta Sg bl le F k (fr_N F)"
    unfolding fr_delta_def takeq using setu lenu mN xSg by auto
  have src: "fr_run_config bl le k w m = Config⇩M (FR_Scan (take m w)) ?ts ?nn"
    by (simp add: fr_run_config_def)
  have step: "(Config⇩M (FR_Scan (take m w)) ?ts ?nn,
               Config⇩M (FR_Scan (take (Suc m) w))
                 (λi. (?ts i)(?nn i := fr_read bl le k ?x i))
                 (λi. go_dir (fr_move dir.R i) (?nn i)))
              ∈ mttm_step (fr_delta Sg bl le F k (fr_N F))"
  proof (rule mttm_step.step)
    show "(FR_Scan (take m w), λi. ?ts i (?nn i), FR_Scan (take (Suc m) w),
           fr_read bl le k ?x, fr_move dir.R) ∈ fr_delta Sg bl le F k (fr_N F)"
      using tr by (simp add: read_eq)
  qed
  have tgt: "fr_run_config bl le k w (Suc m)
              = Config⇩M (FR_Scan (take (Suc m) w))
                  (λi. (?ts i)(?nn i := fr_read bl le k ?x i))
                  (λi. go_dir (fr_move dir.R i) (?nn i))"
  proof -
    have tape: "(λi. (?ts i)(?nn i := fr_read bl le k ?x i)) = ?ts"
    proof (rule ext)
      fix i
      have eq: "fr_read bl le k ?x i = ?ts i (?nn i)"
        using kpos mlt by (cases "i = 0") (auto simp: fr_read_def)
      show "(?ts i)(?nn i := fr_read bl le k ?x i) = ?ts i"
        unfolding eq by (rule fun_upd_triv)
    qed
    have head: "(λi. go_dir (fr_move dir.R i) (?nn i))
                  = (λi::nat. if i = 0 then Suc m + 1 else 0)"
    proof (rule ext)
      fix i show "go_dir (fr_move dir.R i) (?nn i) = (if i = 0 then Suc m + 1 else 0)"
        by (cases "i = 0") (simp_all add: fr_move_def)
    qed
    show ?thesis
      by (simp add: fr_run_config_def tape head)
  qed
  show ?thesis unfolding src tgt by (rule step)
qed

text ‹Every word in ‹F› is no longer than the cutoff.›

lemma fr_length_le_N:
  assumes "w ∈ F" and "finite F"
  shows "length w ≤ fr_N F"
proof -
  have "F ≠ {}" using assms(1) by auto
  hence "fr_N F = Max (length ` F)" by (simp add: fr_N_def)
  moreover have "length w ∈ length ` F" using assms(1) by simp
  ultimately show ?thesis using assms(2) by simp
qed

text ‹The start step: from the initial configuration, reading the left
  endmarker advances into the length-‹0› scan configuration.›

lemma fr_le_step:
  assumes kpos: "0 < k"
  shows "(init_config_mttm (finite_recogniser Sg Gamma bl le F k) w,
          fr_run_config bl le k w 0)
           ∈ mttm_step (fr_delta Sg bl le F k (fr_N F))"
proof -
  let ?ts = "λ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"
  have read_eq: "(λi. ?ts i ((λ_. 0) i)) = fr_read bl le k le"
  proof (rule ext)
    fix i show "?ts i ((λ_. 0) i) = fr_read bl le k le i"
      using kpos by (cases "i = 0") (auto simp: fr_read_def)
  qed
  have tr: "(FR_Scan [], fr_read bl le k le, FR_Scan [],
             fr_read bl le k le, fr_move dir.R) ∈ fr_delta Sg bl le F k (fr_N F)"
    unfolding fr_delta_def by auto
  have init_eq: "init_config_mttm (finite_recogniser Sg Gamma bl le F k) w
                   = Config⇩M (FR_Scan []) ?ts (λ_. 0)"
    by (simp add: finite_recogniser_def)
  have step: "(Config⇩M (FR_Scan []) ?ts (λ_. 0),
               Config⇩M (FR_Scan [])
                 (λi. (?ts i)((λ_. 0) i := fr_read bl le k le i))
                 (λi. go_dir (fr_move dir.R i) ((λ_. 0) i)))
              ∈ mttm_step (fr_delta Sg bl le F k (fr_N F))"
  proof (rule mttm_step.step)
    show "(FR_Scan [], λi. ?ts i ((λ_. 0) i), FR_Scan [],
           fr_read bl le k le, fr_move dir.R) ∈ fr_delta Sg bl le F k (fr_N F)"
      using tr by (simp add: read_eq)
  qed
  have tgt: "fr_run_config bl le k w 0
              = Config⇩M (FR_Scan [])
                  (λi. (?ts i)((λ_. 0) i := fr_read bl le k le i))
                  (λi. go_dir (fr_move dir.R i) ((λ_. 0) i))"
  proof -
    have tape: "(λi. (?ts i)((λ_. 0) i := fr_read bl le k le i)) = ?ts"
    proof (rule ext)
      fix i
      have eq: "fr_read bl le k le i = ?ts i ((λ_. 0) i)"
        using kpos by (cases "i = 0") (auto simp: fr_read_def)
      show "(?ts i)((λ_. 0) i := fr_read bl le k le i) = ?ts i"
        unfolding eq by (rule fun_upd_triv)
    qed
    have head: "(λi. go_dir (fr_move dir.R i) ((λ_. 0) i))
                  = (λi::nat. if i = 0 then 0 + 1 else 0)"
    proof (rule ext)
      fix i show "go_dir (fr_move dir.R i) ((λ_. 0) i) = (if i = 0 then 0 + 1 else 0)"
        by (cases "i = 0") (simp_all add: fr_move_def)
    qed
    show ?thesis by (simp add: fr_run_config_def tape head)
  qed
  show ?thesis unfolding init_eq tgt by (rule step)
qed

text ‹The accept step: from the fully-scanned configuration (prefix
  ‹w›), reading the end-of-input blank accepts, provided ‹w ∈ F›.›

lemma fr_accept_step:
  assumes wF: "w ∈ F" and wSg: "set w ⊆ Sg" and finF: "finite F"
  shows "(fr_run_config bl le k w (length w),
          Config⇩M FR_Acc
            (λ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)
            (λi::nat. if i = 0 then length w + 1 else 0))
           ∈ mttm_step (fr_delta Sg bl le F k (fr_N F))"
proof -
  let ?ts = "λ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"
  let ?nn = "λi::nat. if i = 0 then length w + 1 else 0"
  have lenN: "length w ≤ fr_N F" using fr_length_le_N[OF wF finF] .
  have read_eq: "(λi. ?ts i (?nn i)) = fr_read bl le k bl"
  proof (rule ext)
    fix i show "?ts i (?nn i) = fr_read bl le k bl i"
      by (cases "i = 0") (auto simp: fr_read_def)
  qed
  have tr: "(FR_Scan w, fr_read bl le k bl, FR_Acc,
             fr_read bl le k bl, fr_move dir.N) ∈ fr_delta Sg bl le F k (fr_N F)"
    unfolding fr_delta_def using wSg lenN wF by auto
  have src: "fr_run_config bl le k w (length w) = Config⇩M (FR_Scan w) ?ts ?nn"
    by (simp add: fr_run_config_def)
  have step: "(Config⇩M (FR_Scan w) ?ts ?nn,
               Config⇩M FR_Acc
                 (λi. (?ts i)(?nn i := fr_read bl le k bl i))
                 (λi. go_dir (fr_move dir.N i) (?nn i)))
              ∈ mttm_step (fr_delta Sg bl le F k (fr_N F))"
  proof (rule mttm_step.step)
    show "(FR_Scan w, λi. ?ts i (?nn i), FR_Acc,
           fr_read bl le k bl, fr_move dir.N) ∈ fr_delta Sg bl le F k (fr_N F)"
      using tr by (simp add: read_eq)
  qed
  have tape: "(λi. (?ts i)(?nn i := fr_read bl le k bl i)) = ?ts"
  proof (rule ext)
    fix i
    have eq: "fr_read bl le k bl i = ?ts i (?nn i)"
      by (cases "i = 0") (auto simp: fr_read_def)
    show "(?ts i)(?nn i := fr_read bl le k bl i) = ?ts i"
      unfolding eq by (rule fun_upd_triv)
  qed
  have head: "(λi. go_dir (fr_move dir.N i) (?nn i)) = ?nn"
    by (rule ext) (simp add: fr_move_def)
  show ?thesis
    unfolding src using step by (simp add: tape head)
qed

text ‹The scan phase: iterating the scan step reads all of ‹w›,
  reaching the fully-scanned configuration in ‹length w› steps.
  Assembled by the substrate's bounded-iteration combinator
  @{thm[source] relpow_invariant_chain}.›

lemma fr_scan_chain:
  assumes kpos: "0 < k" and wF: "w ∈ F" and wSg: "set w ⊆ Sg" and finF: "finite F"
  shows "(fr_run_config bl le k w 0, fr_run_config bl le k w (length w))
           ∈ (mttm_step (fr_delta Sg bl le F k (fr_N F))) ^^ (length w)"
proof -
  have lenN: "length w ≤ fr_N F" using fr_length_le_N[OF wF finF] .
  have "∃c'. (fr_run_config bl le k w 0, c')
               ∈ (mttm_step (fr_delta Sg bl le F k (fr_N F))) ^^ (length w)
             ∧ c' = fr_run_config bl le k w (length w)"
  proof (rule relpow_invariant_chain[where P = "λi c. c = fr_run_config bl le k w i"])
    fix i c assume ilt: "i < length w" and Pi: "c = fr_run_config bl le k w i"
    have iN: "i < fr_N F" using ilt lenN by linarith
    have "(fr_run_config bl le k w i, fr_run_config bl le k w (Suc i))
            ∈ mttm_step (fr_delta Sg bl le F k (fr_N F))"
      by (rule fr_scan_step[OF kpos ilt iN wSg])
    thus "∃c'. (c, c') ∈ mttm_step (fr_delta Sg bl le F k (fr_N F))
                ∧ c' = fr_run_config bl le k w (Suc i)"
      using Pi by blast
  next
    show "fr_run_config bl le k w 0 = fr_run_config bl le k w 0" by (rule refl)
  qed
  thus ?thesis by blast
qed

text ‹The full accepting run: for a member ‹w›, the recogniser reaches
  its accept state from the initial configuration in ‹length w + 2›
  steps --- the start step, the ‹length w› scan steps, and the accept
  step.›

lemma fr_accepting_run:
  assumes kpos: "0 < k" and wF: "w ∈ F" and wSg: "set w ⊆ Sg" and finF: "finite F"
  shows "∃c. (init_config_mttm (finite_recogniser Sg Gamma bl le F k) w, c)
               ∈ (mttm_step (fr_delta Sg bl le F k (fr_N F))) ^^ (length w + 2)
             ∧ mt_state c = FR_Acc"
proof -
  let ?R = "mttm_step (fr_delta Sg bl le F k (fr_N F))"
  let ?init = "init_config_mttm (finite_recogniser Sg Gamma bl le F k) w"
  let ?acc = "Config⇩M FR_Acc
                (λ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)
                (λi::nat. if i = 0 then length w + 1 else 0)"
  have le1: "(?init, fr_run_config bl le k w 0) ∈ ?R ^^ 1"
    using fr_le_step[OF kpos] by simp
  have sc: "(fr_run_config bl le k w 0, fr_run_config bl le k w (length w)) ∈ ?R ^^ (length w)"
    using fr_scan_chain[OF kpos wF wSg finF] .
  have ac: "(fr_run_config bl le k w (length w), ?acc) ∈ ?R ^^ 1"
    using fr_accept_step[OF wF wSg finF] by simp
  have t1: "(?init, fr_run_config bl le k w (length w)) ∈ ?R ^^ (1 + length w)"
    by (rule relpow_transI[OF le1 sc])
  have t2: "(?init, ?acc) ∈ ?R ^^ (1 + length w + 1)"
    by (rule relpow_transI[OF t1 ac])
  have "(?init, ?acc) ∈ ?R ^^ (length w + 2)" using t2 by (simp add: add.commute)
  moreover have "mt_state ?acc = FR_Acc" by simp
  ultimately show ?thesis by blast
qed

text ‹Consequently a member is accepted within ‹length w + 2› steps.
  (The extra ‹+2› over the classical ‹n+1› is the substrate's left
  endmarker read, which the textbook model has no counterpart for.)›

lemma finite_recogniser_accepts:
  assumes kpos: "0 < k" and wF: "w ∈ F" and wSg: "set w ⊆ Sg" and finF: "finite F"
  shows "accepts_in_time_mttm (finite_recogniser Sg Gamma bl le F k) w (length w + 2)"
proof -
  obtain c where c: "(init_config_mttm (finite_recogniser Sg Gamma bl le F k) w, c)
                        ∈ (mttm_step (fr_delta Sg bl le F k (fr_N F))) ^^ (length w + 2)"
             and cst: "mt_state c = FR_Acc"
    using fr_accepting_run[OF kpos wF wSg finF] by blast
  show ?thesis
    unfolding accepts_in_time_mttm_def finite_recogniser_delta_tm finite_recogniser_t_tm
    using c cst by blast
qed

text ‹Completeness half of the language characterisation: every member
  is accepted, hence in the language.›

lemma finite_recogniser_lang_complete:
  assumes kpos: "0 < k" and Fsub: "∀w∈F. set w ⊆ Sg" and finF: "finite F"
  shows "F ⊆ Lang_mttm (finite_recogniser Sg Gamma bl le F k)"
proof
  fix w assume wF: "w ∈ F"
  have wSg: "set w ⊆ Sg" using Fsub wF by blast
  obtain c where c: "(init_config_mttm (finite_recogniser Sg Gamma bl le F k) w, c)
                        ∈ (mttm_step (fr_delta Sg bl le F k (fr_N F))) ^^ (length w + 2)"
             and cst: "mt_state c = FR_Acc"
    using fr_accepting_run[OF kpos wF wSg finF] by blast
  obtain w' n where c_eq: "c = Config⇩M FR_Acc w' n"
    using cst by (cases c) auto
  have reach: "(init_config_mttm (finite_recogniser Sg Gamma bl le F k) w,
                Config⇩M FR_Acc w' n)
                 ∈ (mttm_step (fr_delta Sg bl le F k (fr_N F)))⇧*"
    using c c_eq by (metis relpow_imp_rtrancl)
  show "w ∈ Lang_mttm (finite_recogniser Sg Gamma bl le F k)"
    unfolding Lang_mttm_def finite_recogniser_Sigma_tm finite_recogniser_t_tm
              finite_recogniser_delta_tm
    using wSg reach by blast
qed


subsection ‹Soundness of the run›

text ‹Every recogniser transition, and hence every recogniser step,
  starts from a scan state --- so the two halting states are sinks.›

lemma fr_delta_src_scan:
  "(q, a, q', a', d) ∈ fr_delta Sg bl le F k N ⟹ ∃u. q = FR_Scan u"
  by (auto simp: fr_delta_def)

lemma fr_step_src_scan:
  assumes "(c, c') ∈ mttm_step (fr_delta Sg bl le F k N)"
  shows "∃u. mt_state c = FR_Scan u"
proof -
  from assms obtain q ts n q' a d where
      c_eq: "c = Config⇩M q ts n"
    and tr: "(q, λk. ts k (n k), q', a, d) ∈ fr_delta Sg bl le F k N"
    by (auto elim: mttm_step.cases)
  from fr_delta_src_scan[OF tr] obtain u where "q = FR_Scan u" by blast
  thus ?thesis using c_eq by auto
qed

text ‹The overflow step: at the cutoff (‹m = fr_N F›) with input still
  remaining (‹m < length w›), reading the next symbol rejects.›

lemma fr_overflow_step:
  assumes kpos: "0 < k" and mlt: "m < length w" and mN: "m = fr_N F"
    and wSg: "set w ⊆ Sg"
  shows "∃c'. (fr_run_config bl le k w m, c')
               ∈ mttm_step (fr_delta Sg bl le F k (fr_N F)) ∧ mt_state c' = FR_Rej"
proof -
  let ?x = "w ! m"
  let ?ts = "λ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"
  let ?nn = "λi::nat. if i = 0 then m + 1 else 0"
  let ?tgt = "Config⇩M FR_Rej
                (λi. (?ts i)(?nn i := fr_read bl le k ?x i))
                (λi. go_dir (fr_move dir.N i) (?nn i))"
  have xSg: "?x ∈ Sg" using nth_mem[OF mlt] wSg by blast
  have lenu: "length (take m w) = m" using mlt by simp
  have setu: "set (take m w) ⊆ Sg"
    using wSg by (meson set_take_subset subset_trans)
  have read_eq: "(λi. ?ts i (?nn i)) = fr_read bl le k ?x"
  proof (rule ext)
    fix i show "?ts i (?nn i) = fr_read bl le k ?x i"
      using kpos mlt by (cases "i = 0") (auto simp: fr_read_def)
  qed
  have tr: "(FR_Scan (take m w), fr_read bl le k ?x, FR_Rej,
             fr_read bl le k ?x, fr_move dir.N) ∈ fr_delta Sg bl le F k (fr_N F)"
    unfolding fr_delta_def using setu lenu mN xSg by auto
  have src: "fr_run_config bl le k w m = Config⇩M (FR_Scan (take m w)) ?ts ?nn"
    by (simp add: fr_run_config_def)
  have step: "(fr_run_config bl le k w m, ?tgt)
                ∈ mttm_step (fr_delta Sg bl le F k (fr_N F))"
    unfolding src
  proof (rule mttm_step.step)
    show "(FR_Scan (take m w), λi. ?ts i (?nn i), FR_Rej,
           fr_read bl le k ?x, fr_move dir.N) ∈ fr_delta Sg bl le F k (fr_N F)"
      using tr by (simp add: read_eq)
  qed
  have "(fr_run_config bl le k w m, ?tgt)
          ∈ mttm_step (fr_delta Sg bl le F k (fr_N F)) ∧ mt_state ?tgt = FR_Rej"
    using step by simp
  thus ?thesis by blast
qed

text ‹The end-reject step: reading the end-of-input blank on a
  non-member prefix rejects.›

lemma fr_reject_step:
  assumes wnF: "w ∉ F" and wSg: "set w ⊆ Sg" and lenN: "length w ≤ fr_N F"
  shows "∃c'. (fr_run_config bl le k w (length w), c')
               ∈ mttm_step (fr_delta Sg bl le F k (fr_N F)) ∧ mt_state c' = FR_Rej"
proof -
  let ?ts = "λ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"
  let ?nn = "λi::nat. if i = 0 then length w + 1 else 0"
  let ?tgt = "Config⇩M FR_Rej
                (λi. (?ts i)(?nn i := fr_read bl le k bl i))
                (λi. go_dir (fr_move dir.N i) (?nn i))"
  have read_eq: "(λi. ?ts i (?nn i)) = fr_read bl le k bl"
  proof (rule ext)
    fix i show "?ts i (?nn i) = fr_read bl le k bl i"
      by (cases "i = 0") (auto simp: fr_read_def)
  qed
  have tr: "(FR_Scan w, fr_read bl le k bl, FR_Rej,
             fr_read bl le k bl, fr_move dir.N) ∈ fr_delta Sg bl le F k (fr_N F)"
    unfolding fr_delta_def using wSg lenN wnF by auto
  have src: "fr_run_config bl le k w (length w) = Config⇩M (FR_Scan w) ?ts ?nn"
    by (simp add: fr_run_config_def)
  have step: "(fr_run_config bl le k w (length w), ?tgt)
                ∈ mttm_step (fr_delta Sg bl le F k (fr_N F))"
    unfolding src
  proof (rule mttm_step.step)
    show "(FR_Scan w, λi. ?ts i (?nn i), FR_Rej,
           fr_read bl le k bl, fr_move dir.N) ∈ fr_delta Sg bl le F k (fr_N F)"
      using tr by (simp add: read_eq)
  qed
  have "(fr_run_config bl le k w (length w), ?tgt)
          ∈ mttm_step (fr_delta Sg bl le F k (fr_N F)) ∧ mt_state ?tgt = FR_Rej"
    using step by simp
  thus ?thesis by blast
qed

text ‹The reachability invariant: from the initial configuration on an
  input over ‹Sg›, every reachable configuration is the initial one, a
  scan configuration below the cutoff, a reject, or an accept that
  certifies ‹w ∈ F›.›

definition fr_inv ::
  "'a set ⇒ 'a set ⇒ 'a ⇒ 'a ⇒ 'a list set ⇒ nat ⇒ 'a list
     ⇒ ('a, 'a fr_state) mt_config ⇒ bool"
where
  "fr_inv Sg Gamma bl le F k w c ⟷
     (∃m. m ≤ length w ∧ m ≤ fr_N F ∧ c = fr_run_config bl le k w m)
     ∨ c = init_config_mttm (finite_recogniser Sg Gamma bl le F k) w
     ∨ mt_state c = FR_Rej
     ∨ (mt_state c = FR_Acc ∧ w ∈ F)"

text ‹Closure of the invariant under a step.  Each canonical
  configuration has a single successor (determinism, via
  @{thm[source] mttm_step_functional}), given by the matching step
  lemma; the two halting states are sinks
  (@{thm[source] fr_step_src_scan}).›

lemma fr_inv_closed:
  assumes leS: "le ∉ Sg" and blS: "bl ∉ Sg" and blle: "bl ≠ le"
    and kpos: "0 < k" and finF: "finite F" and wSg: "set w ⊆ Sg"
    and inv: "fr_inv Sg Gamma bl le F k w c"
    and step: "(c, c') ∈ mttm_step (fr_delta Sg bl le F k (fr_N F))"
  shows "fr_inv Sg Gamma bl le F k w c'"
proof -
  have fdet: "∀q a p⇩1 b⇩1 d⇩1 p⇩2 b⇩2 d⇩2.
      (q, a, p⇩1, b⇩1, d⇩1) ∈ fr_delta Sg bl le F k (fr_N F)
        ⟶ (q, a, p⇩2, b⇩2, d⇩2) ∈ fr_delta Sg bl le F k (fr_N F)
        ⟶ (p⇩1, b⇩1, d⇩1) = (p⇩2, b⇩2, d⇩2)"
    using finite_recogniser_det[OF leS blS blle]
    unfolding det_mttm_def finite_recogniser_delta_tm by blast
  from inv[unfolded fr_inv_def] show ?thesis
  proof (elim disjE)
    assume "∃m. m ≤ length w ∧ m ≤ fr_N F ∧ c = fr_run_config bl le k w m"
    then obtain m where mlw: "m ≤ length w" and mN: "m ≤ fr_N F"
      and c_eq: "c = fr_run_config bl le k w m" by blast
    show ?thesis
    proof (cases "m < length w")
      case True
      show ?thesis
      proof (cases "m < fr_N F")
        case True
        have s: "(c, fr_run_config bl le k w (Suc m))
                   ∈ mttm_step (fr_delta Sg bl le F k (fr_N F))"
          using fr_scan_step[OF kpos ‹m < length w› True wSg] c_eq by simp
        have "c' = fr_run_config bl le k w (Suc m)"
          using mttm_step_functional[OF fdet step s] .
        moreover have "Suc m ≤ length w" using ‹m < length w› by simp
        moreover have "Suc m ≤ fr_N F" using True by simp
        ultimately show ?thesis unfolding fr_inv_def by blast
      next
        case False
        hence mEq: "m = fr_N F" using mN by simp
        obtain d where d: "(fr_run_config bl le k w m, d)
                             ∈ mttm_step (fr_delta Sg bl le F k (fr_N F))"
          and dst: "mt_state d = FR_Rej"
          using fr_overflow_step[OF kpos ‹m < length w› mEq wSg] by blast
        have "c' = d" using mttm_step_functional[OF fdet step] d c_eq by simp
        thus ?thesis unfolding fr_inv_def using dst by simp
      qed
    next
      case False
      hence mEq: "m = length w" using mlw by simp
      have lenN: "length w ≤ fr_N F" using mEq mN by simp
      show ?thesis
      proof (cases "w ∈ F")
        case True
        have acc: "(c, Config⇩M FR_Acc
                       (λ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)
                       (λi::nat. if i = 0 then length w + 1 else 0))
                     ∈ mttm_step (fr_delta Sg bl le F k (fr_N F))"
          using fr_accept_step[OF True wSg finF] c_eq mEq by simp
        have "c' = Config⇩M FR_Acc
                     (λ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)
                     (λi::nat. if i = 0 then length w + 1 else 0)"
          using mttm_step_functional[OF fdet step acc] .
        thus ?thesis unfolding fr_inv_def using True by simp
      next
        case False
        obtain d where d: "(fr_run_config bl le k w (length w), d)
                             ∈ mttm_step (fr_delta Sg bl le F k (fr_N F))"
          and dst: "mt_state d = FR_Rej"
          using fr_reject_step[OF False wSg lenN] by blast
        have "(c, d) ∈ mttm_step (fr_delta Sg bl le F k (fr_N F))"
          using d c_eq mEq by simp
        hence "c' = d" using mttm_step_functional[OF fdet step] by blast
        thus ?thesis unfolding fr_inv_def using dst by simp
      qed
    qed
  next
    assume ini: "c = init_config_mttm (finite_recogniser Sg Gamma bl le F k) w"
    have s: "(c, fr_run_config bl le k w 0)
               ∈ mttm_step (fr_delta Sg bl le F k (fr_N F))"
      using fr_le_step[OF kpos] ini by simp
    have "c' = fr_run_config bl le k w 0"
      using mttm_step_functional[OF fdet step s] .
    thus ?thesis unfolding fr_inv_def by auto
  next
    assume "mt_state c = FR_Rej"
    thus ?thesis using fr_step_src_scan[OF step] by auto
  next
    assume "mt_state c = FR_Acc ∧ w ∈ F"
    thus ?thesis using fr_step_src_scan[OF step] by auto
  qed
qed

text ‹State of the two canonical non-halting configurations.›

lemma mt_state_fr_run_config:
  "mt_state (fr_run_config bl le k w m) = FR_Scan (take m w)"
  by (simp add: fr_run_config_def)

lemma mt_state_init_finite_recogniser:
  "mt_state (init_config_mttm (finite_recogniser Sg Gamma bl le F k) w) = FR_Scan []"
  by (simp add: finite_recogniser_def)

text ‹The invariant holds at every reachable configuration
  (@{thm[source] rtrancl_induct} from the initial configuration, using
  closure).›

lemma fr_inv_reach:
  assumes leS: "le ∉ Sg" and blS: "bl ∉ Sg" and blle: "bl ≠ le"
    and kpos: "0 < k" and finF: "finite F" and wSg: "set w ⊆ Sg"
    and reach: "(init_config_mttm (finite_recogniser Sg Gamma bl le F k) w, c)
                  ∈ (mttm_step (fr_delta Sg bl le F k (fr_N F)))⇧*"
  shows "fr_inv Sg Gamma bl le F k w c"
  using reach
proof (induction rule: rtrancl_induct)
  case base
  show ?case unfolding fr_inv_def by simp
next
  case (step y z)
  show ?case
    by (rule fr_inv_closed[OF leS blS blle kpos finF wSg step.IH step.hyps(2)])
qed

text ‹An accepting reachable configuration certifies membership: the
  other invariant disjuncts have a non-accept state.›

lemma fr_inv_acc_imp_mem:
  assumes "fr_inv Sg Gamma bl le F k w c" and "mt_state c = FR_Acc"
  shows "w ∈ F"
  using assms unfolding fr_inv_def
  by (auto simp: mt_state_fr_run_config mt_state_init_finite_recogniser)

text ‹Soundness half of the language characterisation: only members
  are accepted.›

lemma finite_recogniser_lang_sound:
  assumes leS: "le ∉ Sg" and blS: "bl ∉ Sg" and blle: "bl ≠ le"
    and kpos: "0 < k" and finF: "finite F"
  shows "Lang_mttm (finite_recogniser Sg Gamma bl le F k) ⊆ F"
proof
  fix w assume wL: "w ∈ Lang_mttm (finite_recogniser Sg Gamma bl le F k)"
  from wL[unfolded Lang_mttm_def finite_recogniser_Sigma_tm finite_recogniser_t_tm]
  obtain w' n where wSg: "set w ⊆ Sg"
    and r: "(init_config_mttm (finite_recogniser Sg Gamma bl le F k) w,
             Config⇩M FR_Acc w' n)
              ∈ (mttm_step (delta_tm (finite_recogniser Sg Gamma bl le F k)))⇧*"
    by auto
  have r': "(init_config_mttm (finite_recogniser Sg Gamma bl le F k) w,
             Config⇩M FR_Acc w' n)
              ∈ (mttm_step (fr_delta Sg bl le F k (fr_N F)))⇧*"
    using r by (simp add: finite_recogniser_delta_tm)
  have inv: "fr_inv Sg Gamma bl le F k w (Config⇩M FR_Acc w' n)"
    by (rule fr_inv_reach[OF leS blS blle kpos finF wSg r'])
  show "w ∈ F" using fr_inv_acc_imp_mem[OF inv] by simp
qed

text ‹The language characterisation: the recogniser decides exactly
  ‹F›.›

theorem finite_recogniser_language:
  assumes leS: "le ∉ Sg" and blS: "bl ∉ Sg" and blle: "bl ≠ le"
    and kpos: "0 < k" and finF: "finite F" and Fsub: "∀w∈F. set w ⊆ Sg"
  shows "Lang_mttm (finite_recogniser Sg Gamma bl le F k) = F"
  using finite_recogniser_lang_complete[OF kpos Fsub finF]
        finite_recogniser_lang_sound[OF leS blS blle kpos finF]
  by blast


end