Theory Multitape_Finite_Patch

theory Multitape_Finite_Patch
  imports Multitape_Finite_Control
begin

section ‹Finite-control patch combinator›

text ‹The combinator @{text finite_patch} wraps an arbitrary machine
  ‹M› with a finite-control front end deciding the short inputs (length
  at most a cutoff ‹N›) by a caller-supplied table, while long inputs
  (length above ‹N›) are handed to ‹M› unchanged.  Unlike the alphabet
  combinators it performs ∗‹no encoding›: it keeps ‹M›'s input alphabet,
  tape alphabet, blank, left endmarker, and tape count, so running ‹M›
  is a pure state relabelling (@{text "FP_Run q"} mirrors ‹M›'s state
  ‹q›) on the very same tapes.

  The front end scans the input read-only as the recogniser does; once
  it has read past the cutoff it walks the head back to the origin
  (phase @{text FP_Rewind}) and enters ‹M›'s start state, so the handoff
  configuration is exactly ‹M›'s initial configuration.  Short inputs
  are decided in place: the scan ends on the end-of-input blank and
  jumps straight to ‹M›'s accept state (identify-with-run, so no extra
  halting funnel) when the table holds, or to a dedicated reject sink
  otherwise.›


subsection ‹Patch state space›

text ‹Four phases: @{text "FP_Scan u"} has read the prefix ‹u›;
  @{text FP_Rewind} is walking the head back to the origin after a
  long-input overflow; @{text "FP_Run q"} is running the wrapped
  machine in (relabelled) state ‹q›; @{text FP_Rej} is the short-input
  rejection sink.  Acceptance is identified with ∗‹reaching ‹M›'s accept
  state under the run relabelling›, @{text "FP_Run (t_tm M)"}.›

datatype ('q, 'a) fp_state =
    FP_Scan "'a list" | FP_Rewind | FP_Run 'q | FP_Rej


subsection ‹Patch transition relation›

text ‹Eight families, reusing the recogniser's read/move tuples
  @{const fr_read} / @{const fr_move} (so the front end is read-only,
  slots 2 and 4 equal).  Parameters: input alphabet ‹Sg›, blank ‹bl›,
  left endmarker ‹le›, tape count ‹k›, the wrapped machine's start
  state ‹st› and accept state ‹tt›, the short-input decision table
  ‹table›, the cutoff ‹N›, and the wrapped machine's transition relation
  ‹deltaM›.

  ▪ advance-le --- read past the left endmarker (start step);
  ▪ scan-extend --- extend the scanned prefix while below the cutoff;
  ▪ overflow --- at the cutoff with input remaining, enter the rewind;
  ▪ short-accept --- end-of-input on a table member jumps to ‹M›'s accept;
  ▪ short-reject --- end-of-input on a non-member rejects;
  ▪ rewind-walk --- walk the head left over the input (the only left move);
  ▪ rewind-done --- reading the left endmarker enters ‹M›'s start state;
  ▪ run-lift --- ‹M›'s own transitions, relabelled by @{const FP_Run}.›

definition fp_delta ::
  "'a set ⇒ 'a ⇒ 'a ⇒ nat ⇒ 'q ⇒ 'q ⇒ ('a list ⇒ bool) ⇒ nat
     ⇒ ('q × (nat ⇒ 'a) × 'q × (nat ⇒ 'a) × (nat ⇒ dir)) set
     ⇒ (('q, 'a) fp_state × (nat ⇒ 'a) × ('q, 'a) fp_state
          × (nat ⇒ 'a) × (nat ⇒ dir)) set"
where
  "fp_delta Sg bl le k st tt table N deltaM =
     { (FP_Scan [], fr_read bl le k le, FP_Scan [],
        fr_read bl le k le, fr_move dir.R) }
     ∪ { (FP_Scan u, fr_read bl le k x, FP_Scan (u @ [x]),
          fr_read bl le k x, fr_move dir.R)
         | u x. set u ⊆ Sg ∧ length u < N ∧ x ∈ Sg }
     ∪ { (FP_Scan u, fr_read bl le k x, FP_Rewind,
          fr_read bl le k x, fr_move dir.N)
         | u x. set u ⊆ Sg ∧ length u = N ∧ x ∈ Sg }
     ∪ { (FP_Scan u, fr_read bl le k bl, FP_Run tt,
          fr_read bl le k bl, fr_move dir.N)
         | u. set u ⊆ Sg ∧ length u ≤ N ∧ table u }
     ∪ { (FP_Scan u, fr_read bl le k bl, FP_Rej,
          fr_read bl le k bl, fr_move dir.N)
         | u. set u ⊆ Sg ∧ length u ≤ N ∧ ¬ table u }
     ∪ { (FP_Rewind, fr_read bl le k x, FP_Rewind,
          fr_read bl le k x, fr_move dir.L)
         | x. x ∈ Sg }
     ∪ { (FP_Rewind, fr_read bl le k le, FP_Run st,
          fr_read bl le k le, fr_move dir.N) }
     ∪ { (FP_Run q, a, FP_Run q', a', d)
         | q a q' a' d. (q, a, q', a', d) ∈ deltaM }"


subsection ‹The patch machine›

text ‹The finite patch of ‹M› at cutoff ‹N› with short-input table
  ‹table›.  Its state set is the scannable prefixes (words over ‹M›'s
  input alphabet up to the cutoff), the relabelled states of ‹M›, the
  rewind state, and the reject sink; alphabet, blank, endmarker, and
  tape count are inherited from ‹M›.›

definition finite_patch ::
  "('q, 'a) mttm ⇒ ('a list ⇒ bool) ⇒ nat ⇒ (('q, 'a) fp_state, 'a) mttm"
where
  "finite_patch M table N =
     MTTM
       (FP_Scan ` {u. set u ⊆ Sigma_tm M ∧ length u ≤ N}
          ∪ FP_Run ` Q_tm M ∪ {FP_Rewind, FP_Rej})
       (Sigma_tm M)
       (Γ_tm M)
       (bl_tm M)
       (le_tm M)
       (fp_delta (Sigma_tm M) (bl_tm M) (le_tm M) (k_tm M)
          (s_tm M) (t_tm M) table N (delta_tm M))
       (FP_Scan [])
       (FP_Run (t_tm M))
       FP_Rej
       (k_tm M)"


subsection ‹Component accessors›

lemma finite_patch_k_tm:
  "k_tm (finite_patch M table N) = k_tm M"
  by (simp add: finite_patch_def)

lemma finite_patch_Sigma_tm:
  "Sigma_tm (finite_patch M table N) = Sigma_tm M"
  by (simp add: finite_patch_def)

lemma finite_patch_Gamma_tm:
  "Γ_tm (finite_patch M table N) = Γ_tm M"
  by (simp add: finite_patch_def)

lemma finite_patch_bl_tm:
  "bl_tm (finite_patch M table N) = bl_tm M"
  by (simp add: finite_patch_def)

lemma finite_patch_le_tm:
  "le_tm (finite_patch M table N) = le_tm M"
  by (simp add: finite_patch_def)

lemma finite_patch_s_tm:
  "s_tm (finite_patch M table N) = FP_Scan []"
  by (simp add: finite_patch_def)

lemma finite_patch_t_tm:
  "t_tm (finite_patch M table N) = FP_Run (t_tm M)"
  by (simp add: finite_patch_def)

lemma finite_patch_r_tm:
  "r_tm (finite_patch M table N) = FP_Rej"
  by (simp add: finite_patch_def)

lemma finite_patch_Q_tm:
  "Q_tm (finite_patch M table N)
     = FP_Scan ` {u. set u ⊆ Sigma_tm M ∧ length u ≤ N}
         ∪ FP_Run ` Q_tm M ∪ {FP_Rewind, FP_Rej}"
  by (simp add: finite_patch_def)

lemma finite_patch_delta_tm:
  "delta_tm (finite_patch M table N)
     = fp_delta (Sigma_tm M) (bl_tm M) (le_tm M) (k_tm M)
         (s_tm M) (t_tm M) table N (delta_tm M)"
  by (simp add: finite_patch_def)


subsection ‹Transition-relation discipline›

text ‹The support invariant: at every inactive tape index ‹j ≥ k›,
  each transition reads and writes the blank and stays put.  The front
  families are read-only with @{const fr_read} / @{const fr_move}, so
  ‹j ≥ k› reads and writes ‹bl› and moves ‹N›; the run-lift family
  inherits it from the wrapped machine's own support hypothesis.›

lemma fp_delta_support:
  assumes kpos: "0 < k"
    and dM: "∀q a q' a' d. (q, a, q', a', d) ∈ deltaM
                ⟶ (∀j≥k. a j = bl ∧ a' j = bl ∧ d j = dir.N)"
    and tr: "(q, a, q', a', d) ∈ fp_delta Sg bl le k st tt table N deltaM"
    and j: "k ≤ j"
  shows "a j = bl ∧ a' j = bl ∧ d j = dir.N"
proof -
  have jn0: "j ≠ 0" using j kpos by simp
  have jk: "¬ j < k" using j by simp
  from tr consider
      (front) rsym mdir where "a = fr_read bl le k rsym"
                              "a' = fr_read bl le k rsym" "d = fr_move mdir"
    | (run) q0 q0' where "(q0, a, q0', a', d) ∈ deltaM"
    unfolding fp_delta_def by blast
  then show ?thesis
  proof cases
    case front ― ‹read-only front families: ‹bl› on the support region›
    show ?thesis using front jn0 jk by (simp add: fr_read_def fr_move_def)
  next
    case run ― ‹the run-lift family inherits ‹M›'s support invariant›
    show ?thesis using dM run j by blast
  qed
qed

text ‹A tape reading @{const fr_read}'s input symbol ‹x ∈ Sg› as ‹le›
  must be tape ‹0›'s neighbour, not tape ‹0› itself: tape ‹0› carries
  ‹x›, and ‹x ≠ le› since ‹le ∉ Sg›.  This is what keeps the rewind
  walk's left move off any endmarker-reading tape.›

lemma fr_read_le_pos:
  "le ∉ Sg ⟹ x ∈ Sg ⟹ fr_read bl le k x j = le ⟹ j ≠ 0"
  by (auto simp: fr_read_def split: if_splits)

text ‹The left-endmarker read discipline: a transition reading ‹le› on
  tape ‹j› writes ‹le› back there and moves only ‹N› or ‹R›.  The front
  families are read-only, so the write half is immediate; for the move
  half the only left move is the rewind walk (@{const fr_move} ‹L›),
  and there tape ‹0› reads an input symbol (never ‹le›, as ‹le ∉ Sg›)
  while every other tape stays put.  The run-lift family inherits it
  from the wrapped machine's own endmarker hypothesis.›

lemma fp_delta_LE:
  assumes leS: "le ∉ Sg"
    and dM: "∀q a q' a' d j. (q, a, q', a', d) ∈ deltaM ⟶ a j = le
                ⟶ a' j = le ∧ d j ∈ {dir.N, dir.R}"
    and tr: "(q, a, q', a', d) ∈ fp_delta Sg bl le k st tt table N deltaM"
    and LE: "a j = le"
  shows "a' j = le ∧ d j ∈ {dir.N, dir.R}"
proof -
  ― ‹name the family up front, so each case reasons over clean
     (non-recursive) equations rather than letting the simplifier
     back-substitute ‹le› into an ‹fr_read› body›
  from tr consider
      (front) "a' = a" "d = fr_move dir.R ∨ d = fr_move dir.N"
    | (rwalk) x where "x ∈ Sg" "a = fr_read bl le k x" "a' = a"
                      "d = fr_move dir.L"
    | (run) q0 q0' where "(q0, a, q0', a', d) ∈ deltaM"
    unfolding fp_delta_def by blast
  then show ?thesis
  proof cases
    case front ― ‹read-only front families with no left move›
    from front(1) LE have aj: "a' j = le" by simp
    have "d j ≠ dir.L" using front(2) by (auto simp: fr_move_def split: if_splits)
    hence "d j ∈ {dir.N, dir.R}" by (cases "d j") auto
    with aj show ?thesis by blast
  next
    case rwalk ― ‹the rewind walk: reading ‹le› forces the head off tape ‹0››
    have aj: "fr_read bl le k x j = le" using LE rwalk(2) by simp
    have "j ≠ 0" using fr_read_le_pos[OF leS rwalk(1) aj] .
    moreover have "a' j = le" using LE rwalk(3) by simp
    ultimately show ?thesis using rwalk(4) by (simp add: fr_move_def)
  next
    case run ― ‹the run-lift family inherits ‹M›'s endmarker discipline›
    show ?thesis using dM run LE by blast
  qed
qed


subsection ‹Well-formedness›

text ‹The patch of a valid machine is a valid substrate machine.  The
  front families supply the finite-control side of every structural
  axiom (finiteness of the scannable prefixes, the read/write alphabet,
  the endmarker and support disciplines) and the run-lift family
  forwards ‹M›'s own structure through the substrate's projection
  lemmas.›

lemma finite_patch_valid:
  assumes vM: "valid_mttm M"
  shows "valid_mttm (finite_patch M table N)"
proof -
  let ?Sg = "Sigma_tm M"
  let ?Ga = "Γ_tm M"
  let ?bl = "bl_tm M"
  let ?le = "le_tm M"
  let ?k = "k_tm M"
  let ?st = "s_tm M"
  let ?tt = "t_tm M"
  let ?QM = "Q_tm M"
  let ?Q = "FP_Scan ` {u. set u ⊆ ?Sg ∧ length u ≤ N}
              ∪ FP_Run ` ?QM ∪ {FP_Rewind, FP_Rej}"
  let ?dl = "fp_delta ?Sg ?bl ?le ?k ?st ?tt table N (delta_tm M)"
  ― ‹the machine's own structural facts, projected out of @{term vM}›
  have SgG: "?Sg ⊆ ?Ga" by (rule valid_mttm_Sigma_sub_Gamma[OF vM])
  have blG: "?bl ∈ ?Ga" by (rule valid_mttm_blank_in_Gamma[OF vM])
  have blS: "?bl ∉ ?Sg" by (rule valid_mttm_blank_not_Sigma[OF vM])
  have leG: "?le ∈ ?Ga" by (rule valid_mttm_LE_in_Gamma[OF vM])
  have leS: "?le ∉ ?Sg" by (rule valid_mttm_LE_not_Sigma[OF vM])
  have sQ: "?st ∈ ?QM" by (rule valid_mttm_s_in_Q[OF vM])
  have tQ: "?tt ∈ ?QM" by (rule valid_mttm_t_in_Q[OF vM])
  have kpos: "0 < ?k" by (rule valid_mttm_k_pos[OF vM])
  have finGa: "finite ?Ga" by (rule valid_mttm_finite_Gamma[OF vM])
  have finQM: "finite ?QM" by (rule valid_mttm_finite_Q[OF vM])
  have dM_set: "delta_tm M
      ⊆ (?QM - {?tt, r_tm M}) × (UNIV → ?Ga) × ?QM
           × (UNIV → ?Ga) × (UNIV → UNIV)"
    by (rule valid_mttm_delta_set[OF vM])
  have dM_LE: "∀q a q' a' d j. (q, a, q', a', d) ∈ delta_tm M ⟶ a j = ?le
                 ⟶ a' j = ?le ∧ d j ∈ {dir.N, dir.R}"
    using valid_mttm_deltaLE[OF vM] by blast
  have dM_supp: "∀q a q' a' d. (q, a, q', a', d) ∈ delta_tm M
                   ⟶ (∀j≥?k. a j = ?bl ∧ a' j = ?bl ∧ d j = dir.N)"
    using valid_mttm_delta_support[OF vM] by blast
  ― ‹finiteness of the scannable-prefix component, hence of ‹Q››
  have finSg: "finite ?Sg" using finite_subset[OF SgG finGa] .
  have finP: "finite {u. set u ⊆ ?Sg ∧ length u ≤ N}"
    using finite_lists_length_le[OF finSg] by blast
  have finQ: "finite ?Q" using finP finQM by simp
  ― ‹the transition-shape, endmarker, and support obligations›
  have shape: "?dl ⊆ (?Q - {FP_Run ?tt, FP_Rej}) × (UNIV → ?Ga) × ?Q
                        × (UNIV → ?Ga) × (UNIV → UNIV)"
    unfolding fp_delta_def fr_read_def
    using SgG blG leG sQ tQ dM_set by (auto simp: Pi_iff)
  have LEc: "∀q a q' a' d j.
      (q, a, q', a', d) ∈ ?dl ⟶ a j = ?le ⟶ a' j = ?le ∧ d j ∈ {dir.N, dir.R}"
    using fp_delta_LE[OF leS dM_LE] by blast
  have suppc: "∀q a q' a' d.
      (q, a, q', a', d) ∈ ?dl ⟶ (∀j≥?k. a j = ?bl ∧ a' j = ?bl ∧ d j = dir.N)"
    using fp_delta_support[OF kpos dM_supp] by blast
  show ?thesis
    unfolding finite_patch_def valid_mttm.simps
    using finQ finGa SgG blG blS leG leS kpos tQ shape LEc suppc
    by (intro conjI) auto
qed


subsection ‹Determinism›

text ‹The patch is deterministic when the wrapped machine is.  The
  three phases are disjoint by source constructor (@{const FP_Scan} /
  @{const FP_Rewind} / @{const FP_Run}); within the scan and rewind
  phases the tape-‹0› read (@{thm[source] fr_read_inj}) selects a unique
  family, the left endmarker, the blank, and the input alphabet being
  pairwise distinct; and the run phase is single-valued because ‹M›
  is.›

lemma finite_patch_det:
  assumes vM: "valid_mttm M" and blle: "bl_tm M ≠ le_tm M" and dM: "det_mttm M"
  shows "det_mttm (finite_patch M table N)"
proof -
  have leS: "le_tm M ∉ Sigma_tm M" by (rule valid_mttm_LE_not_Sigma[OF vM])
  have blS: "bl_tm M ∉ Sigma_tm M" by (rule valid_mttm_blank_not_Sigma[OF vM])
  show ?thesis
    unfolding det_mttm_def finite_patch_delta_tm fp_delta_def
    using leS blS blle dM[unfolded det_mttm_def]
    by (auto dest: fr_read_inj)
qed


subsection ‹Long-input simulation of the wrapped machine›

text ‹The run-lift family embeds ‹M›'s transitions verbatim, so the
  ∗‹run relabelling› --- tagging ‹M›'s state ‹q› as @{term "FP_Run q"} on
  the very same tapes --- carries every ‹M› step to a patch step.  This
  is the long-input arm's correctness, and it holds for a
  nondeterministic ‹M› (the run phase is where the patch's own
  nondeterminism lives).›

fun fp_lift :: "('a, 'q) mt_config ⇒ ('a, ('q, 'a) fp_state) mt_config" where
  "fp_lift (Config⇩M q ts n) = Config⇩M (FP_Run q) ts n"

lemma fp_run_step:
  assumes "(c, c') ∈ mttm_step deltaM"
  shows "(fp_lift c, fp_lift c')
           ∈ mttm_step (fp_delta Sg bl le k st tt table N deltaM)"
proof -
  from assms obtain q ts n q' a d where
      c: "c = Config⇩M q ts n"
    and c': "c' = Config⇩M q' (λi. (ts i)(n i := a i)) (λi. go_dir (d i) (n i))"
    and tr: "(q, λi. ts i (n i), q', a, d) ∈ deltaM"
    by (auto elim: mttm_step.cases)
  have tr': "(FP_Run q, λi. ts i (n i), FP_Run q', a, d)
               ∈ fp_delta Sg bl le k st tt table N deltaM"
    unfolding fp_delta_def using tr by blast
  have "(Config⇩M (FP_Run q) ts n,
         Config⇩M (FP_Run q') (λi. (ts i)(n i := a i)) (λi. go_dir (d i) (n i)))
          ∈ mttm_step (fp_delta Sg bl le k st tt table N deltaM)"
  proof (rule mttm_step.step)
    show "(FP_Run q, λi. ts i (n i), FP_Run q', a, d)
            ∈ fp_delta Sg bl le k st tt table N deltaM"
      by (rule tr')
  qed
  thus ?thesis using c c' by simp
qed

lemma fp_run_rtrancl:
  assumes "(c, c') ∈ (mttm_step deltaM)⇧*"
  shows "(fp_lift c, fp_lift c')
           ∈ (mttm_step (fp_delta Sg bl le k st tt table N deltaM))⇧*"
  using assms
proof (induction rule: rtrancl_induct)
  case base
  show ?case by simp
next
  case (step y z)
  from fp_run_step[OF step.hyps(2)] step.IH
  show ?case by (auto intro: rtrancl.rtrancl_into_rtrancl)
qed


subsection ‹The scanning front run›

text ‹The configuration after the patch has read the left endmarker
  and the first ‹m› input symbols: state @{term "FP_Scan (take m w)"},
  the (read-only, hence unchanging) input tape, and the input head at
  position ‹m + 1›.  Identical in tape shape to the recogniser's
  @{const fr_run_config}, differing only in the scan constructor.›

definition fp_scan_config ::
  "'a ⇒ 'a ⇒ nat ⇒ 'a list ⇒ nat ⇒ ('a, ('q, 'a) fp_state) mt_config"
where
  "fp_scan_config bl le k w m =
     Config⇩M (FP_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 ‹The start step: reading the left endmarker advances the patch's
  initial configuration into the length-‹0› scan configuration.›

lemma fp_le_step:
  assumes kpos: "0 < k_tm M"
  shows "(init_config_mttm (finite_patch M table N) w,
          fp_scan_config (bl_tm M) (le_tm M) (k_tm M) w 0)
           ∈ mttm_step (fp_delta (Sigma_tm M) (bl_tm M) (le_tm M) (k_tm M)
                          (s_tm M) (t_tm M) table N (delta_tm M))"
proof -
  let ?bl = "bl_tm M" and ?le = "le_tm M" and ?k = "k_tm 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 ?dl = "fp_delta (Sigma_tm M) ?bl ?le ?k (s_tm M) (t_tm M) table N (delta_tm M)"
  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: "(FP_Scan [], fr_read ?bl ?le ?k ?le, FP_Scan [],
             fr_read ?bl ?le ?k ?le, fr_move dir.R) ∈ ?dl"
    unfolding fp_delta_def by auto
  have init_eq: "init_config_mttm (finite_patch M table N) w
                   = Config⇩M (FP_Scan []) ?ts (λ_. 0)"
    by (simp add: finite_patch_def)
  have step: "(Config⇩M (FP_Scan []) ?ts (λ_. 0),
               Config⇩M (FP_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 ?dl"
  proof (rule mttm_step.step)
    show "(FP_Scan [], λi. ?ts i ((λ_. 0) i), FP_Scan [],
           fr_read ?bl ?le ?k ?le, fr_move dir.R) ∈ ?dl"
      using tr by (simp add: read_eq)
  qed
  have tgt: "fp_scan_config ?bl ?le ?k w 0
              = Config⇩M (FP_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)"
      by (rule ext) (simp add: fr_move_def)
    show ?thesis by (simp add: fp_scan_config_def tape head)
  qed
  show ?thesis unfolding init_eq tgt by (rule step)
qed

text ‹One scan step: reading the next input symbol extends the scanned
  prefix, provided the input still has a symbol there and the cutoff
  is not yet reached.›

lemma fp_scan_step:
  assumes kpos: "0 < k" and mlt: "m < length w" and mN: "m < N"
    and wSg: "set w ⊆ Sg"
  shows "(fp_scan_config bl le k w m, fp_scan_config bl le k w (Suc m))
           ∈ mttm_step (fp_delta Sg bl le k st tt table N deltaM)"
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 ?dl = "fp_delta Sg bl le k st tt table N deltaM"
  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: "(FP_Scan (take m w), fr_read bl le k ?x, FP_Scan (take (Suc m) w),
             fr_read bl le k ?x, fr_move dir.R) ∈ ?dl"
    unfolding fp_delta_def takeq using setu lenu mN xSg by auto
  have src: "fp_scan_config bl le k w m = Config⇩M (FP_Scan (take m w)) ?ts ?nn"
    by (simp add: fp_scan_config_def)
  have step: "(Config⇩M (FP_Scan (take m w)) ?ts ?nn,
               Config⇩M (FP_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 ?dl"
  proof (rule mttm_step.step)
    show "(FP_Scan (take m w), λi. ?ts i (?nn i), FP_Scan (take (Suc m) w),
           fr_read bl le k ?x, fr_move dir.R) ∈ ?dl"
      using tr by (simp add: read_eq)
  qed
  have tgt: "fp_scan_config bl le k w (Suc m)
              = Config⇩M (FP_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)"
      by (rule ext) (simp add: fr_move_def)
    show ?thesis by (simp add: fp_scan_config_def tape head)
  qed
  show ?thesis unfolding src tgt by (rule step)
qed

text ‹The scan phase: from the length-‹0› scan configuration, iterating
  the scan step reaches the length-‹m› one in ‹m› steps, for any ‹m› up
  to both the input length and the cutoff.  Assembled by the
  substrate's @{thm[source] relpow_invariant_chain}.›

lemma fp_scan_chain:
  assumes kpos: "0 < k" and mle: "m ≤ length w" and mN: "m ≤ N"
    and wSg: "set w ⊆ Sg"
  shows "(fp_scan_config bl le k w 0, fp_scan_config bl le k w m)
           ∈ (mttm_step (fp_delta Sg bl le k st tt table N deltaM)) ^^ m"
  using mle mN
proof (induction m)
  case 0
  show ?case by simp
next
  case (Suc m)
  have mw: "m < length w" using Suc.prems(1) by simp
  have mN': "m < N" using Suc.prems(2) by simp
  have chain: "(fp_scan_config bl le k w 0, fp_scan_config bl le k w m)
                 ∈ (mttm_step (fp_delta Sg bl le k st tt table N deltaM)) ^^ m"
    using Suc.IH Suc.prems by simp
  have step: "(fp_scan_config bl le k w m, fp_scan_config bl le k w (Suc m))
                ∈ mttm_step (fp_delta Sg bl le k st tt table N deltaM)"
    by (rule fp_scan_step[OF kpos mw mN' wSg])
  from chain step show ?case by (rule relpow_Suc_I)
qed


subsection ‹Short-input dispatch›

text ‹At the end of a short input (length at most the cutoff), reading
  the end-of-input blank on a fully-scanned prefix jumps to ‹M›'s accept
  state when the table holds --- the short arm never runs ‹M›.›

lemma fp_accept_step:
  assumes wtab: "table w" and wSg: "set w ⊆ Sg" and lenN: "length w ≤ N"
  shows "(fp_scan_config bl le k w (length w),
          Config⇩M (FP_Run tt)
            (λ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 (fp_delta Sg bl le k st tt table N deltaM)"
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 ?dl = "fp_delta Sg bl le k st tt table N deltaM"
  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: "(FP_Scan w, fr_read bl le k bl, FP_Run tt,
             fr_read bl le k bl, fr_move dir.N) ∈ ?dl"
    unfolding fp_delta_def using wSg lenN wtab by auto
  have src: "fp_scan_config bl le k w (length w) = Config⇩M (FP_Scan w) ?ts ?nn"
    by (simp add: fp_scan_config_def)
  have step: "(Config⇩M (FP_Scan w) ?ts ?nn,
               Config⇩M (FP_Run tt)
                 (λi. (?ts i)(?nn i := fr_read bl le k bl i))
                 (λi. go_dir (fr_move dir.N i) (?nn i))) ∈ mttm_step ?dl"
  proof (rule mttm_step.step)
    show "(FP_Scan w, λi. ?ts i (?nn i), FP_Run tt,
           fr_read bl le k bl, fr_move dir.N) ∈ ?dl"
      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 dual short-input step: on a non-member prefix the scan
  rejects into the dedicated sink @{const FP_Rej}.›

lemma fp_reject_step:
  assumes wtab: "¬ table w" and wSg: "set w ⊆ Sg" and lenN: "length w ≤ N"
  shows "∃c'. (fp_scan_config bl le k w (length w), c')
               ∈ mttm_step (fp_delta Sg bl le k st tt table N deltaM)
             ∧ mt_state c' = FP_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 ?dl = "fp_delta Sg bl le k st tt table N deltaM"
  let ?tgt = "Config⇩M FP_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: "(FP_Scan w, fr_read bl le k bl, FP_Rej,
             fr_read bl le k bl, fr_move dir.N) ∈ ?dl"
    unfolding fp_delta_def using wSg lenN wtab by auto
  have src: "fp_scan_config bl le k w (length w) = Config⇩M (FP_Scan w) ?ts ?nn"
    by (simp add: fp_scan_config_def)
  have step: "(fp_scan_config bl le k w (length w), ?tgt) ∈ mttm_step ?dl"
    unfolding src
  proof (rule mttm_step.step)
    show "(FP_Scan w, λi. ?ts i (?nn i), FP_Rej,
           fr_read bl le k bl, fr_move dir.N) ∈ ?dl"
      using tr by (simp add: read_eq)
  qed
  have "(fp_scan_config bl le k w (length w), ?tgt) ∈ mttm_step ?dl
          ∧ mt_state ?tgt = FP_Rej"
    using step by simp
  thus ?thesis by blast
qed


subsection ‹Long-input rewind and handoff›

text ‹The rewind configuration: state @{const FP_Rewind}, the unchanging
  input tape, and the input head at position ‹p› as it walks back to
  the origin.›

definition fp_rewind_config ::
  "'a ⇒ 'a ⇒ nat ⇒ 'a list ⇒ nat ⇒ ('a, ('q, 'a) fp_state) mt_config"
where
  "fp_rewind_config bl le k w p =
     Config⇩M FP_Rewind
       (λ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 p else 0)"

text ‹Overflow: at the cutoff with input still remaining, reading the
  next symbol enters the rewind (the head does not move --- the symbol
  under it is re-read on the first rewind step).›

lemma fp_overflow_step:
  assumes kpos: "0 < k" and Nlt: "N < length w" and wSg: "set w ⊆ Sg"
  shows "(fp_scan_config bl le k w N, fp_rewind_config bl le k w (N + 1))
           ∈ mttm_step (fp_delta Sg bl le k st tt table N deltaM)"
proof -
  let ?x = "w ! N"
  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 N + 1 else 0"
  let ?dl = "fp_delta Sg bl le k st tt table N deltaM"
  have xSg: "?x ∈ Sg" using nth_mem[OF Nlt] wSg by blast
  have lenu: "length (take N w) = N" using Nlt by simp
  have setu: "set (take N 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 Nlt by (cases "i = 0") (auto simp: fr_read_def)
  qed
  have tr: "(FP_Scan (take N w), fr_read bl le k ?x, FP_Rewind,
             fr_read bl le k ?x, fr_move dir.N) ∈ ?dl"
    unfolding fp_delta_def using setu lenu xSg by auto
  have src: "fp_scan_config bl le k w N = Config⇩M (FP_Scan (take N w)) ?ts ?nn"
    by (simp add: fp_scan_config_def)
  have step: "(Config⇩M (FP_Scan (take N w)) ?ts ?nn,
               Config⇩M FP_Rewind
                 (λi. (?ts i)(?nn i := fr_read bl le k ?x i))
                 (λi. go_dir (fr_move dir.N i) (?nn i))) ∈ mttm_step ?dl"
  proof (rule mttm_step.step)
    show "(FP_Scan (take N w), λi. ?ts i (?nn i), FP_Rewind,
           fr_read bl le k ?x, fr_move dir.N) ∈ ?dl"
      using tr by (simp add: read_eq)
  qed
  have tgt: "fp_rewind_config bl le k w (N + 1)
              = Config⇩M FP_Rewind
                  (λi. (?ts i)(?nn i := fr_read bl le k ?x i))
                  (λi. go_dir (fr_move dir.N 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 Nlt 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.N i) (?nn i)) = ?nn"
      by (rule ext) (simp add: fr_move_def)
    show ?thesis by (simp add: fp_rewind_config_def tape head fun_eq_iff)
  qed
  show ?thesis unfolding src tgt by (rule step)
qed

text ‹One rewind step: reading an input symbol walks the head one cell
  left, leaving the tape unchanged.›

lemma fp_rewind_walk_step:
  assumes kpos: "0 < k" and qw: "Suc q ≤ length w" and wSg: "set w ⊆ Sg"
  shows "(fp_rewind_config bl le k w (Suc q), fp_rewind_config bl le k w q)
           ∈ mttm_step (fp_delta Sg bl le k st tt table N deltaM)"
proof -
  let ?x = "w ! q"
  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 Suc q else 0"
  let ?dl = "fp_delta Sg bl le k st tt table N deltaM"
  have xin: "q < length w" using qw by simp
  have xSg: "?x ∈ Sg" using nth_mem[OF xin] wSg by blast
  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 qw by (cases "i = 0") (auto simp: fr_read_def)
  qed
  have tr: "(FP_Rewind, fr_read bl le k ?x, FP_Rewind,
             fr_read bl le k ?x, fr_move dir.L) ∈ ?dl"
    unfolding fp_delta_def using xSg by auto
  have src: "fp_rewind_config bl le k w (Suc q) = Config⇩M FP_Rewind ?ts ?nn"
    by (simp add: fp_rewind_config_def)
  have step: "(Config⇩M FP_Rewind ?ts ?nn,
               Config⇩M FP_Rewind
                 (λi. (?ts i)(?nn i := fr_read bl le k ?x i))
                 (λi. go_dir (fr_move dir.L i) (?nn i))) ∈ mttm_step ?dl"
  proof (rule mttm_step.step)
    show "(FP_Rewind, λi. ?ts i (?nn i), FP_Rewind,
           fr_read bl le k ?x, fr_move dir.L) ∈ ?dl"
      using tr by (simp add: read_eq)
  qed
  have tgt: "fp_rewind_config bl le k w q
              = Config⇩M FP_Rewind
                  (λi. (?ts i)(?nn i := fr_read bl le k ?x i))
                  (λi. go_dir (fr_move dir.L 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 qw 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.L i) (?nn i))
                  = (λi::nat. if i = 0 then q else 0)"
      by (rule ext) (simp add: fr_move_def)
    show ?thesis by (simp add: fp_rewind_config_def tape head)
  qed
  show ?thesis unfolding src tgt by (rule step)
qed

text ‹The rewind phase: from head position ‹p› (within the input) the
  walk reaches the origin in ‹p› steps.›

lemma fp_rewind_chain:
  assumes kpos: "0 < k" and pw: "p ≤ length w" and wSg: "set w ⊆ Sg"
  shows "(fp_rewind_config bl le k w p, fp_rewind_config bl le k w 0)
           ∈ (mttm_step (fp_delta Sg bl le k st tt table N deltaM)) ^^ p"
  using pw
proof (induction p)
  case 0
  show ?case by simp
next
  case (Suc p)
  have step: "(fp_rewind_config bl le k w (Suc p), fp_rewind_config bl le k w p)
                ∈ mttm_step (fp_delta Sg bl le k st tt table N deltaM)"
    by (rule fp_rewind_walk_step[OF kpos Suc.prems wSg])
  have chain: "(fp_rewind_config bl le k w p, fp_rewind_config bl le k w 0)
                 ∈ (mttm_step (fp_delta Sg bl le k st tt table N deltaM)) ^^ p"
    using Suc.IH Suc.prems by simp
  from step chain show ?case by (rule relpow_Suc_I2)
qed

text ‹Rewind completion: reading the left endmarker at the origin
  enters ‹M›'s start state, and the configuration is exactly the run
  relabelling of ‹M›'s initial configuration.›

lemma fp_rewind_done_step:
  assumes kpos: "0 < k_tm M"
  shows "(fp_rewind_config (bl_tm M) (le_tm M) (k_tm M) w 0,
          fp_lift (init_config_mttm M w))
           ∈ mttm_step (fp_delta (Sigma_tm M) (bl_tm M) (le_tm M) (k_tm M)
                          (s_tm M) (t_tm M) table N (delta_tm M))"
proof (cases M)
  case (MTTM Q Sg Ga bl le d s t r k)
  ― ‹reduce every ‹_tm M› selector to a concrete component up front, so
     the tape reasoning is over ground terms›
  have kpos': "0 < k" using kpos by (simp add: MTTM)
  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 ?dl = "fp_delta Sg bl le k s t table N d"
  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: "(FP_Rewind, fr_read bl le k le, FP_Run s,
             fr_read bl le k le, fr_move dir.N) ∈ ?dl"
    unfolding fp_delta_def by auto
  have src: "fp_rewind_config (bl_tm M) (le_tm M) (k_tm M) w 0
               = Config⇩M FP_Rewind ?ts (λ_. 0)"
    by (simp add: fp_rewind_config_def MTTM)
  have dl_eq: "fp_delta (Sigma_tm M) (bl_tm M) (le_tm M) (k_tm M)
                 (s_tm M) (t_tm M) table N (delta_tm M) = ?dl"
    by (simp add: MTTM)
  have step: "(Config⇩M FP_Rewind ?ts (λ_. 0),
               Config⇩M (FP_Run s)
                 (λi. (?ts i)((λ_. 0) i := fr_read bl le k le i))
                 (λi. go_dir (fr_move dir.N i) ((λ_. 0) i)))
              ∈ mttm_step ?dl"
  proof (rule mttm_step.step)
    show "(FP_Rewind, λi. ?ts i ((λ_. 0) i), FP_Run s,
           fr_read bl le k le, fr_move dir.N) ∈ ?dl"
      using tr by (simp add: read_eq)
  qed
  have tgt: "fp_lift (init_config_mttm M w)
              = Config⇩M (FP_Run s)
                  (λi. (?ts i)((λ_. 0) i := fr_read bl le k le i))
                  (λi. go_dir (fr_move dir.N 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.N i) ((λ_. 0) i)) = (λ_::nat. 0)"
      by (rule ext) (simp add: fr_move_def)
    have init: "init_config_mttm M w = Config⇩M s ?ts (λ_. 0)"
      by (simp add: MTTM)
    show ?thesis by (simp add: init tape head)
  qed
  show ?thesis unfolding dl_eq src tgt using step by simp
qed


subsection ‹Forward language direction›

text ‹A short accepted input reaches ‹M›'s accept state without running
  ‹M›: read the endmarker, scan the whole input, and dispatch on the
  table.›

lemma fp_short_run:
  assumes kpos: "0 < k_tm M" and wSg: "set w ⊆ Sigma_tm M"
    and lenN: "length w ≤ N" and tab: "table w"
  shows "∃c. (init_config_mttm (finite_patch M table N) w, c)
               ∈ (mttm_step (delta_tm (finite_patch M table N)))⇧*
             ∧ mt_state c = FP_Run (t_tm M)"
proof -
  let ?dl = "fp_delta (Sigma_tm M) (bl_tm M) (le_tm M) (k_tm M)
               (s_tm M) (t_tm M) table N (delta_tm M)"
  let ?sc = "fp_scan_config (bl_tm M) (le_tm M) (k_tm M) w"
  let ?acc = "Config⇩M (FP_Run (t_tm M))
                (λi n. if i < k_tm M
                       then (if n = 0 then le_tm M
                             else if i = 0 ∧ n ≤ length w then w ! (n - 1) else bl_tm M)
                       else bl_tm M)
                (λi::nat. if i = 0 then length w + 1 else 0)"
  have dl: "delta_tm (finite_patch M table N) = ?dl" by (rule finite_patch_delta_tm)
  have le: "(init_config_mttm (finite_patch M table N) w, ?sc 0) ∈ (mttm_step ?dl)⇧*"
    using fp_le_step[OF kpos] by (rule r_into_rtrancl)
  have sc: "(?sc 0, ?sc (length w)) ∈ (mttm_step ?dl)⇧*"
    using fp_scan_chain[OF kpos order_refl lenN wSg] by (rule relpow_imp_rtrancl)
  have ac0: "(?sc (length w), ?acc) ∈ mttm_step ?dl"
    using tab wSg lenN by (rule fp_accept_step)
  have ac: "(?sc (length w), ?acc) ∈ (mttm_step ?dl)⇧*"
    using ac0 by (rule r_into_rtrancl)
  have reach: "(init_config_mttm (finite_patch M table N) w, ?acc) ∈ (mttm_step ?dl)⇧*"
    using le sc ac by (meson rtrancl_trans)
  have "mt_state ?acc = FP_Run (t_tm M)" by simp
  thus ?thesis using reach dl by auto
qed

text ‹A long accepted input (in ‹M›'s language) reaches ‹M›'s accept
  state by overflowing into the rewind, walking back to ‹M›'s initial
  configuration, and then running ‹M›'s accepting computation under the
  run relabelling.›

lemma fp_long_run:
  assumes kpos: "0 < k_tm M" and wSg: "set w ⊆ Sigma_tm M"
    and Nlt: "N < length w" and wL: "w ∈ Lang_mttm M"
  shows "∃c. (init_config_mttm (finite_patch M table N) w, c)
               ∈ (mttm_step (delta_tm (finite_patch M table N)))⇧*
             ∧ mt_state c = FP_Run (t_tm M)"
proof -
  let ?dl = "fp_delta (Sigma_tm M) (bl_tm M) (le_tm M) (k_tm M)
               (s_tm M) (t_tm M) table N (delta_tm M)"
  let ?init = "init_config_mttm (finite_patch M table N) w"
  let ?sc = "fp_scan_config (bl_tm M) (le_tm M) (k_tm M) w"
  let ?rw = "fp_rewind_config (bl_tm M) (le_tm M) (k_tm M) w"
  have dl: "delta_tm (finite_patch M table N) = ?dl" by (rule finite_patch_delta_tm)
  have Nle: "N ≤ length w" using Nlt by simp
  have N1le: "N + 1 ≤ length w" using Nlt by simp
  have le: "(?init, ?sc 0) ∈ (mttm_step ?dl)⇧*"
    using fp_le_step[OF kpos] by (rule r_into_rtrancl)
  have sc: "(?sc 0, ?sc N) ∈ (mttm_step ?dl)⇧*"
    using fp_scan_chain[OF kpos Nle order_refl wSg] by (rule relpow_imp_rtrancl)
  have ov: "(?sc N, ?rw (N + 1)) ∈ (mttm_step ?dl)⇧*"
    using fp_overflow_step[OF kpos Nlt wSg] by (rule r_into_rtrancl)
  have rc: "(?rw (N + 1), ?rw 0) ∈ (mttm_step ?dl)⇧*"
    using fp_rewind_chain[OF kpos N1le wSg] by (rule relpow_imp_rtrancl)
  have dn: "(?rw 0, fp_lift (init_config_mttm M w)) ∈ (mttm_step ?dl)⇧*"
    using fp_rewind_done_step[OF kpos] by (rule r_into_rtrancl)
  from wL obtain w' n where mreach:
      "(init_config_mttm M w, Config⇩M (t_tm M) w' n) ∈ (mttm_step (delta_tm M))⇧*"
    unfolding Lang_mttm_def by auto
  have sim: "(fp_lift (init_config_mttm M w), Config⇩M (FP_Run (t_tm M)) w' n)
               ∈ (mttm_step ?dl)⇧*"
    using fp_run_rtrancl[OF mreach] by simp
  have r1: "(?init, ?sc N) ∈ (mttm_step ?dl)⇧*" using le sc by (rule rtrancl_trans)
  have r2: "(?init, ?rw (N + 1)) ∈ (mttm_step ?dl)⇧*" using r1 ov by (rule rtrancl_trans)
  have r3: "(?init, ?rw 0) ∈ (mttm_step ?dl)⇧*" using r2 rc by (rule rtrancl_trans)
  have r4: "(?init, fp_lift (init_config_mttm M w)) ∈ (mttm_step ?dl)⇧*"
    using r3 dn by (rule rtrancl_trans)
  have reach: "(?init, Config⇩M (FP_Run (t_tm M)) w' n) ∈ (mttm_step ?dl)⇧*"
    using r4 sim by (rule rtrancl_trans)
  have "mt_state (Config⇩M (FP_Run (t_tm M)) w' n) = FP_Run (t_tm M)" by simp
  thus ?thesis using reach dl by auto
qed

text ‹Forward language inclusion: every input satisfying the dispatch
  specification (short inputs decided by the table, long inputs by
  ‹M›'s language) is accepted by the patch.›

theorem finite_patch_language_forward:
  assumes vM: "valid_mttm M"
  shows "{w. set w ⊆ Sigma_tm M
              ∧ (if length w ≤ N then table w else w ∈ Lang_mttm M)}
           ⊆ Lang_mttm (finite_patch M table N)"
proof
  fix w assume "w ∈ {w. set w ⊆ Sigma_tm M
                        ∧ (if length w ≤ N then table w else w ∈ Lang_mttm M)}"
  hence wSg: "set w ⊆ Sigma_tm M"
    and disp: "if length w ≤ N then table w else w ∈ Lang_mttm M" by auto
  have kpos: "0 < k_tm M" by (rule valid_mttm_k_pos[OF vM])
  have ex: "∃c. (init_config_mttm (finite_patch M table N) w, c)
                  ∈ (mttm_step (delta_tm (finite_patch M table N)))⇧*
                ∧ mt_state c = FP_Run (t_tm M)"
  proof (cases "length w ≤ N")
    case True
    hence tab: "table w" using disp by simp
    show ?thesis using kpos wSg True tab by (rule fp_short_run)
  next
    case False
    hence Nlt: "N < length w" by simp
    have wL: "w ∈ Lang_mttm M" using disp False by simp
    show ?thesis using kpos wSg Nlt wL by (rule fp_long_run)
  qed
  then obtain c where reach: "(init_config_mttm (finite_patch M table N) w, c)
                                ∈ (mttm_step (delta_tm (finite_patch M table N)))⇧*"
    and cst: "mt_state c = FP_Run (t_tm M)" by blast
  obtain w' n where c_eq: "c = Config⇩M (FP_Run (t_tm M)) w' n"
    using cst by (cases c) auto
  show "w ∈ Lang_mttm (finite_patch M table N)"
    unfolding Lang_mttm_def finite_patch_Sigma_tm finite_patch_t_tm
    using wSg reach c_eq by auto
qed


subsection ‹Reverse language direction›

text ‹The front (scan and rewind) is deterministic irrespective of ‹M›:
  its families are the only ones with a @{const FP_Scan} or
  @{const FP_Rewind} source, and they are pairwise disjoint on the read
  (the endmarker, the blank, and the input alphabet being distinct).
  The wrapped machine's nondeterminism is confined to the @{const FP_Run}
  phase, so soundness needs no ‹det_mttm M›.›

lemma fp_delta_front_functional:
  assumes leS: "le ∉ Sg" and blS: "bl ∉ Sg" and blle: "bl ≠ le"
    and src: "(∃u. q = FP_Scan u) ∨ q = FP_Rewind"
    and tr1: "(q, a, p1, b1, d1) ∈ fp_delta Sg bl le k st tt table N deltaM"
    and tr2: "(q, a, p2, b2, d2) ∈ fp_delta Sg bl le k st tt table N deltaM"
  shows "(p1, b1, d1) = (p2, b2, d2)"
  using src tr1 tr2 leS blS blle
  unfolding fp_delta_def
  by (auto dest: fr_read_inj)

lemma fp_step_front_functional:
  assumes leS: "le ∉ Sg" and blS: "bl ∉ Sg" and blle: "bl ≠ le"
    and src: "(∃u. mt_state c = FP_Scan u) ∨ mt_state c = FP_Rewind"
    and step1: "(c, c1) ∈ mttm_step (fp_delta Sg bl le k st tt table N deltaM)"
    and step2: "(c, c2) ∈ mttm_step (fp_delta Sg bl le k st tt table N deltaM)"
  shows "c1 = c2"
proof -
  from step1 obtain q ts n q1' a1 d1 where
      c_eq: "c = Config⇩M q ts n"
    and c1_eq: "c1 = Config⇩M q1' (λi. (ts i)(n i := a1 i)) (λi. go_dir (d1 i) (n i))"
    and tr1: "(q, λi. ts i (n i), q1', a1, d1)
                ∈ fp_delta Sg bl le k st tt table N deltaM"
    by (auto elim: mttm_step.cases)
  from step2 obtain q2' a2 d2 where
      c2_eq: "c2 = Config⇩M q2' (λi. (ts i)(n i := a2 i)) (λi. go_dir (d2 i) (n i))"
    and tr2: "(q, λi. ts i (n i), q2', a2, d2)
                ∈ fp_delta Sg bl le k st tt table N deltaM"
    using c_eq by (auto elim: mttm_step.cases)
  have srcq: "(∃u. q = FP_Scan u) ∨ q = FP_Rewind" using src c_eq by simp
  have "(q1', a1, d1) = (q2', a2, d2)"
    by (rule fp_delta_front_functional[OF leS blS blle srcq tr1 tr2])
  thus ?thesis using c1_eq c2_eq by simp
qed

text ‹Reverse simulation: a step out of a run-relabelled configuration
  is a run relabelling of an ‹M› step (only the run-lift family has an
  @{const FP_Run} source).›

lemma fp_run_step_rev:
  assumes step: "(fp_lift cM, c')
                   ∈ mttm_step (fp_delta Sg bl le k st tt table N deltaM)"
  shows "∃cM'. c' = fp_lift cM' ∧ (cM, cM') ∈ mttm_step deltaM"
proof -
  obtain q0 ts n where cM_eq: "cM = Config⇩M q0 ts n" by (cases cM)
  have lift_eq: "fp_lift cM = Config⇩M (FP_Run q0) ts n" using cM_eq by simp
  from step[unfolded lift_eq] obtain q' a d where
      c'_eq: "c' = Config⇩M q' (λi. (ts i)(n i := a i)) (λi. go_dir (d i) (n i))"
    and tr: "(FP_Run q0, λi. ts i (n i), q', a, d)
               ∈ fp_delta Sg bl le k st tt table N deltaM"
    by (auto elim: mttm_step.cases)
  from tr obtain q0' where q'_eq: "q' = FP_Run q0'"
    and trM: "(q0, λi. ts i (n i), q0', a, d) ∈ deltaM"
    unfolding fp_delta_def by auto
  let ?cM' = "Config⇩M q0' (λi. (ts i)(n i := a i)) (λi. go_dir (d i) (n i))"
  have "c' = fp_lift ?cM'" using c'_eq q'_eq by simp
  moreover have "(cM, ?cM') ∈ mttm_step deltaM"
    unfolding cM_eq
  proof (rule mttm_step.step)
    show "(q0, λi. ts i (n i), q0', a, d) ∈ deltaM" by (rule trM)
  qed
  ultimately show ?thesis by blast
qed

text ‹The two halting states are sinks: ‹M›'s accept (relabelled) has
  no successor because ‹M›'s transitions never leave it, and the reject
  sink is the source of no family.›

lemma fp_run_t_sink:
  assumes vM: "valid_mttm M"
    and step: "(c, c') ∈ mttm_step (fp_delta Sg bl le k st tt table N (delta_tm M))"
    and st: "mt_state c = FP_Run (t_tm M)"
  shows False
proof -
  from step obtain q ts n q' a d where c_eq: "c = Config⇩M q ts n"
    and tr: "(q, λi. ts i (n i), q', a, d)
               ∈ fp_delta Sg bl le k st tt table N (delta_tm M)"
    by (auto elim: mttm_step.cases)
  have q_eq: "q = FP_Run (t_tm M)" using st c_eq by simp
  from tr q_eq obtain q0' where
      trM: "(t_tm M, λi. ts i (n i), q0', a, d) ∈ delta_tm M"
    unfolding fp_delta_def by auto
  have "t_tm M ∈ Q_tm M - {t_tm M, r_tm M}"
    using valid_mttm_delta_set[OF vM] trM by blast
  thus False by simp
qed

lemma fp_rej_sink:
  assumes step: "(c, c') ∈ mttm_step (fp_delta Sg bl le k st tt table N deltaM)"
    and st: "mt_state c = FP_Rej"
  shows False
proof -
  from step obtain q ts n q' a d where c_eq: "c = Config⇩M q ts n"
    and tr: "(q, λi. ts i (n i), q', a, d)
               ∈ fp_delta Sg bl le k st tt table N deltaM"
    by (auto elim: mttm_step.cases)
  have "q = FP_Rej" using st c_eq by simp
  thus False using tr unfolding fp_delta_def by auto
qed

text ‹State of each canonical configuration.›

lemma mt_state_fp_scan_config:
  "mt_state (fp_scan_config bl le k w m) = FP_Scan (take m w)"
  by (simp add: fp_scan_config_def)

lemma mt_state_fp_rewind_config:
  "mt_state (fp_rewind_config bl le k w p) = FP_Rewind"
  by (simp add: fp_rewind_config_def)

lemma mt_state_init_finite_patch:
  "mt_state (init_config_mttm (finite_patch M table N) w) = FP_Scan []"
  by (simp add: finite_patch_def)

lemma mt_state_fp_lift:
  "mt_state (fp_lift cM) = FP_Run (mt_state cM)"
  by (cases cM) simp

text ‹The reachability invariant.  From the initial configuration on an
  input over ‹M›'s alphabet, every reachable configuration is: the
  initial one; a scan configuration below the cutoff; (long inputs
  only) a rewind configuration or a run relabelling of an
  ‹M›-reachable configuration; a short accept certifying the table; or a
  reject.›

definition fp_inv ::
  "('q, 'a) mttm ⇒ ('a list ⇒ bool) ⇒ nat ⇒ 'a list
     ⇒ ('a, ('q, 'a) fp_state) mt_config ⇒ bool"
where
  "fp_inv M table N w c ⟷
     c = init_config_mttm (finite_patch M table N) w
     ∨ (∃m. m ≤ length w ∧ m ≤ N
            ∧ c = fp_scan_config (bl_tm M) (le_tm M) (k_tm M) w m)
     ∨ (N < length w ∧ (∃p. p ≤ N + 1
            ∧ c = fp_rewind_config (bl_tm M) (le_tm M) (k_tm M) w p))
     ∨ (N < length w ∧ (∃cM. (init_config_mttm M w, cM)
                              ∈ (mttm_step (delta_tm M))⇧* ∧ c = fp_lift cM))
     ∨ (length w ≤ N ∧ table w ∧ mt_state c = FP_Run (t_tm M))
     ∨ mt_state c = FP_Rej"

text ‹Closure of the invariant under a step.  Front configurations
  (init, scan, rewind) have a unique successor given by the matching
  step lemma (@{thm[source] fp_step_front_functional}); a run
  configuration steps to another run configuration
  (@{thm[source] fp_run_step_rev}); the two halting states are sinks.›

lemma fp_inv_closed:
  assumes vM: "valid_mttm M" and blle: "bl_tm M ≠ le_tm M"
    and wSg: "set w ⊆ Sigma_tm M"
    and inv: "fp_inv M table N w c"
    and step: "(c, c') ∈ mttm_step (fp_delta (Sigma_tm M) (bl_tm M) (le_tm M)
                  (k_tm M) (s_tm M) (t_tm M) table N (delta_tm M))"
  shows "fp_inv M table N w c'"
proof -
  let ?bl = "bl_tm M"
  let ?le = "le_tm M"
  let ?k = "k_tm M"
  let ?dl = "fp_delta (Sigma_tm M) ?bl ?le ?k (s_tm M) (t_tm M) table N (delta_tm M)"
  have kpos: "0 < ?k" by (rule valid_mttm_k_pos[OF vM])
  have leS: "?le ∉ Sigma_tm M" by (rule valid_mttm_LE_not_Sigma[OF vM])
  have blS: "?bl ∉ Sigma_tm M" by (rule valid_mttm_blank_not_Sigma[OF vM])
  note funct = fp_step_front_functional[OF leS blS blle]
  from inv[unfolded fp_inv_def] show ?thesis
  proof (elim disjE)
    assume "c = init_config_mttm (finite_patch M table N) w"
    note cinit = this
    have src: "(∃u. mt_state c = FP_Scan u) ∨ mt_state c = FP_Rewind"
      using cinit by (auto simp: mt_state_init_finite_patch)
    have cs: "(c, fp_scan_config ?bl ?le ?k w 0) ∈ mttm_step ?dl"
      using fp_le_step[OF kpos] cinit by simp
    have "c' = fp_scan_config ?bl ?le ?k w 0" by (rule funct[OF src step cs])
    thus ?thesis unfolding fp_inv_def by auto
  next
    assume "∃m. m ≤ length w ∧ m ≤ N
                 ∧ c = fp_scan_config ?bl ?le ?k w m"
    then obtain m where mlw: "m ≤ length w" and mN: "m ≤ N"
      and c_eq: "c = fp_scan_config ?bl ?le ?k w m" by blast
    have src: "(∃u. mt_state c = FP_Scan u) ∨ mt_state c = FP_Rewind"
      using c_eq by (auto simp: mt_state_fp_scan_config)
    show ?thesis
    proof (cases "m < length w")
      case True
      show ?thesis
      proof (cases "m < N")
        case True
        have cs: "(c, fp_scan_config ?bl ?le ?k w (Suc m)) ∈ mttm_step ?dl"
          using fp_scan_step[OF kpos ‹m < length w› True wSg] c_eq by simp
        have "c' = fp_scan_config ?bl ?le ?k w (Suc m)"
          by (rule funct[OF src step cs])
        moreover have "Suc m ≤ length w" using ‹m < length w› by simp
        moreover have "Suc m ≤ N" using True by simp
        ultimately show ?thesis unfolding fp_inv_def by blast
      next
        case False
        hence mEqN: "m = N" using mN by simp
        have Nlt: "N < length w" using ‹m < length w› mEqN by simp
        have cs: "(c, fp_rewind_config ?bl ?le ?k w (N + 1)) ∈ mttm_step ?dl"
          using fp_overflow_step[OF kpos Nlt wSg] c_eq mEqN by simp
        have "c' = fp_rewind_config ?bl ?le ?k w (N + 1)"
          by (rule funct[OF src step cs])
        moreover have "N + 1 ≤ N + 1" by simp
        ultimately show ?thesis unfolding fp_inv_def using Nlt by blast
      qed
    next
      case False
      hence mEq: "m = length w" using mlw by simp
      hence lenN: "length w ≤ N" using mN by simp
      show ?thesis
      proof (cases "table w")
        case True
        let ?acc = "Config⇩M (FP_Run (t_tm M))
                      (λ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 cs: "(c, ?acc) ∈ mttm_step ?dl"
          using True wSg lenN unfolding c_eq mEq by (rule fp_accept_step)
        have "c' = ?acc" by (rule funct[OF src step cs])
        hence "mt_state c' = FP_Run (t_tm M)" by simp
        thus ?thesis unfolding fp_inv_def using lenN True by blast
      next
        case False
        have rex: "∃d. (fp_scan_config ?bl ?le ?k w (length w), d) ∈ mttm_step ?dl
                        ∧ mt_state d = FP_Rej"
          using False wSg lenN by (rule fp_reject_step)
        then obtain d where rstep: "(fp_scan_config ?bl ?le ?k w (length w), d)
                                       ∈ mttm_step ?dl" and dst: "mt_state d = FP_Rej"
          by blast
        have cs: "(c, d) ∈ mttm_step ?dl" using rstep c_eq mEq by simp
        have "c' = d" by (rule funct[OF src step cs])
        thus ?thesis unfolding fp_inv_def using dst by blast
      qed
    qed
  next
    assume "N < length w ∧ (∃p. p ≤ N + 1
                                  ∧ c = fp_rewind_config ?bl ?le ?k w p)"
    then obtain p where Nlt: "N < length w" and pN1: "p ≤ N + 1"
      and c_eq: "c = fp_rewind_config ?bl ?le ?k w p" by blast
    have src: "(∃u. mt_state c = FP_Scan u) ∨ mt_state c = FP_Rewind"
      using c_eq by (auto simp: mt_state_fp_rewind_config)
    have N1lw: "N + 1 ≤ length w" using Nlt by simp
    show ?thesis
    proof (cases p)
      case 0
      have cs: "(c, fp_lift (init_config_mttm M w)) ∈ mttm_step ?dl"
        using fp_rewind_done_step[OF kpos] c_eq 0 by simp
      have "c' = fp_lift (init_config_mttm M w)" by (rule funct[OF src step cs])
      moreover have "(init_config_mttm M w, init_config_mttm M w)
                       ∈ (mttm_step (delta_tm M))⇧*" by simp
      ultimately show ?thesis unfolding fp_inv_def using Nlt by blast
    next
      case (Suc q)
      have Sqlw: "Suc q ≤ length w" using pN1 Suc N1lw by simp
      have cs: "(c, fp_rewind_config ?bl ?le ?k w q) ∈ mttm_step ?dl"
        using fp_rewind_walk_step[OF kpos Sqlw wSg] c_eq Suc by simp
      have "c' = fp_rewind_config ?bl ?le ?k w q" by (rule funct[OF src step cs])
      moreover have "q ≤ N + 1" using pN1 Suc by simp
      ultimately show ?thesis unfolding fp_inv_def using Nlt by blast
    qed
  next
    assume "N < length w ∧ (∃cM. (init_config_mttm M w, cM)
                                  ∈ (mttm_step (delta_tm M))⇧* ∧ c = fp_lift cM)"
    then obtain cM where Nlt: "N < length w"
      and reachM: "(init_config_mttm M w, cM) ∈ (mttm_step (delta_tm M))⇧*"
      and c_eq: "c = fp_lift cM" by blast
    have "∃cM'. c' = fp_lift cM' ∧ (cM, cM') ∈ mttm_step (delta_tm M)"
      using fp_run_step_rev[OF step[unfolded c_eq]] .
    then obtain cM' where c'_eq: "c' = fp_lift cM'"
      and mstep: "(cM, cM') ∈ mttm_step (delta_tm M)" by blast
    have "(init_config_mttm M w, cM') ∈ (mttm_step (delta_tm M))⇧*"
      using reachM mstep by (rule rtrancl_into_rtrancl)
    thus ?thesis unfolding fp_inv_def using Nlt c'_eq by blast
  next
    assume "length w ≤ N ∧ table w ∧ mt_state c = FP_Run (t_tm M)"
    hence "mt_state c = FP_Run (t_tm M)" by simp
    hence False using fp_run_t_sink[OF vM step] by simp
    thus ?thesis by simp
  next
    assume "mt_state c = FP_Rej"
    hence False using fp_rej_sink[OF step] by simp
    thus ?thesis by simp
  qed
qed

text ‹The invariant holds at every reachable configuration.›

lemma fp_inv_reach:
  assumes vM: "valid_mttm M" and blle: "bl_tm M ≠ le_tm M"
    and wSg: "set w ⊆ Sigma_tm M"
    and reach: "(init_config_mttm (finite_patch M table N) w, c)
                  ∈ (mttm_step (delta_tm (finite_patch M table N)))⇧*"
  shows "fp_inv M table N w c"
  using reach
proof (induction rule: rtrancl_induct)
  case base
  show ?case unfolding fp_inv_def by simp
next
  case (step y z)
  have yz: "(y, z) ∈ mttm_step (fp_delta (Sigma_tm M) (bl_tm M) (le_tm M)
              (k_tm M) (s_tm M) (t_tm M) table N (delta_tm M))"
    using step.hyps(2) by (simp add: finite_patch_delta_tm)
  show ?case by (rule fp_inv_closed[OF vM blle wSg step.IH yz])
qed

text ‹An accepting reachable configuration certifies the dispatch
  condition: a short input satisfies the table, a long input is in
  ‹M›'s language.›

lemma fp_inv_accept:
  assumes inv: "fp_inv M table N w c" and st: "mt_state c = FP_Run (t_tm M)"
    and wSg: "set w ⊆ Sigma_tm M"
  shows "if length w ≤ N then table w else w ∈ Lang_mttm M"
  using inv[unfolded fp_inv_def]
proof (elim disjE)
  assume "c = init_config_mttm (finite_patch M table N) w"
  hence "mt_state c = FP_Scan []" by (simp add: mt_state_init_finite_patch)
  thus ?thesis using st by simp
next
  assume "∃m. m ≤ length w ∧ m ≤ N
               ∧ c = fp_scan_config (bl_tm M) (le_tm M) (k_tm M) w m"
  then obtain m where "c = fp_scan_config (bl_tm M) (le_tm M) (k_tm M) w m" by blast
  hence "mt_state c = FP_Scan (take m w)" by (simp add: mt_state_fp_scan_config)
  thus ?thesis using st by simp
next
  assume "N < length w ∧ (∃p. p ≤ N + 1
                                ∧ c = fp_rewind_config (bl_tm M) (le_tm M) (k_tm M) w p)"
  then obtain p where "c = fp_rewind_config (bl_tm M) (le_tm M) (k_tm M) w p" by blast
  hence "mt_state c = FP_Rewind" by (simp add: mt_state_fp_rewind_config)
  thus ?thesis using st by simp
next
  assume "N < length w ∧ (∃cM. (init_config_mttm M w, cM)
                                ∈ (mttm_step (delta_tm M))⇧* ∧ c = fp_lift cM)"
  then obtain cM where Nlt: "N < length w"
    and reachM: "(init_config_mttm M w, cM) ∈ (mttm_step (delta_tm M))⇧*"
    and c_eq: "c = fp_lift cM" by blast
  have "mt_state cM = t_tm M" using st c_eq by (simp add: mt_state_fp_lift)
  then obtain w' n where cM_eq: "cM = Config⇩M (t_tm M) w' n" by (cases cM) auto
  have "w ∈ Lang_mttm M"
    unfolding Lang_mttm_def using wSg reachM cM_eq by auto
  thus ?thesis using Nlt by simp
next
  assume "length w ≤ N ∧ table w ∧ mt_state c = FP_Run (t_tm M)"
  thus ?thesis by simp
next
  assume "mt_state c = FP_Rej"
  thus ?thesis using st by simp
qed

text ‹Reverse language inclusion, hence the language characterisation:
  the patch decides exactly the dispatch specification --- and this holds
  for a possibly-nondeterministic ‹M›.›

theorem finite_patch_language_sound:
  assumes vM: "valid_mttm M" and blle: "bl_tm M ≠ le_tm M"
  shows "Lang_mttm (finite_patch M table N)
           ⊆ {w. set w ⊆ Sigma_tm M
                   ∧ (if length w ≤ N then table w else w ∈ Lang_mttm M)}"
proof
  fix w assume "w ∈ Lang_mttm (finite_patch M table N)"
  from this[unfolded Lang_mttm_def finite_patch_Sigma_tm finite_patch_t_tm]
  obtain w' n where wSg: "set w ⊆ Sigma_tm M"
    and r: "(init_config_mttm (finite_patch M table N) w,
             Config⇩M (FP_Run (t_tm M)) w' n)
              ∈ (mttm_step (delta_tm (finite_patch M table N)))⇧*"
    by auto
  have inv: "fp_inv M table N w (Config⇩M (FP_Run (t_tm M)) w' n)"
    by (rule fp_inv_reach[OF vM blle wSg r])
  have "if length w ≤ N then table w else w ∈ Lang_mttm M"
    by (rule fp_inv_accept[OF inv _ wSg]) simp
  thus "w ∈ {w. set w ⊆ Sigma_tm M
                 ∧ (if length w ≤ N then table w else w ∈ Lang_mttm M)}"
    using wSg by simp
qed

theorem finite_patch_language:
  assumes vM: "valid_mttm M" and blle: "bl_tm M ≠ le_tm M"
  shows "Lang_mttm (finite_patch M table N)
           = {w. set w ⊆ Sigma_tm M
                   ∧ (if length w ≤ N then table w else w ∈ Lang_mttm M)}"
  using finite_patch_language_forward[OF vM] finite_patch_language_sound[OF vM blle]
  by blast


subsection ‹Strengthened well-formedness›

text ‹The left-endmarker write discipline for the patch: the front
  families are read-only, and the run-lift family inherits it from
  ‹M›'s own @{const le_unique}.›

lemma fp_delta_write_le:
  assumes dM: "∀q a q' a' d j. (q, a, q', a', d) ∈ deltaM
                 ⟶ a' j = le ⟶ a j = le"
    and tr: "(q, a, q', a', d) ∈ fp_delta Sg bl le k st tt table N deltaM"
    and w: "a' j = le"
  shows "a j = le"
proof -
  from tr consider
      (front) "a' = a"
    | (run) q0 q0' where "(q0, a, q0', a', d) ∈ deltaM"
    unfolding fp_delta_def by blast
  then show ?thesis
  proof cases
    case front thus ?thesis using w by simp
  next
    case run thus ?thesis using dM w by blast
  qed
qed

text ‹The patch of a well-formed machine is well-formed (distinct start /
  accept / reject and endmarker / blank, plus the endmarker write
  discipline).›

lemma finite_patch_well_formed:
  assumes wfM: "well_formed_mttm M"
  shows "well_formed_mttm (finite_patch M table N)"
proof -
  have vM: "valid_mttm M" using wfM by simp
  have luM: "le_unique M" using wfM by simp
  have dM: "∀q a q' a' d j. (q, a, q', a', d) ∈ delta_tm M
              ⟶ a' j = le_tm M ⟶ a j = le_tm M"
    using luM unfolding le_unique_def by simp
  have "valid_mttm (finite_patch M table N)" by (rule finite_patch_valid[OF vM])
  moreover have "s_tm (finite_patch M table N) ≠ t_tm (finite_patch M table N)"
    by (simp add: finite_patch_s_tm finite_patch_t_tm)
  moreover have "s_tm (finite_patch M table N) ≠ r_tm (finite_patch M table N)"
    by (simp add: finite_patch_s_tm finite_patch_r_tm)
  moreover have "le_tm (finite_patch M table N) ≠ bl_tm (finite_patch M table N)"
    using wfM by (simp add: finite_patch_le_tm finite_patch_bl_tm)
  moreover have "le_unique (finite_patch M table N)"
    unfolding le_unique_def finite_patch_delta_tm finite_patch_le_tm
    using fp_delta_write_le[OF dM] by blast
  ultimately show ?thesis by simp
qed


subsection ‹Time bounds›

text ‹The step-counting analogue of @{thm[source] fp_run_rtrancl}: an
  ‹n›-step ‹M› computation lifts to an ‹n›-step patch computation.›

lemma fp_run_relpow:
  assumes "(c, c') ∈ (mttm_step deltaM) ^^ n"
  shows "(fp_lift c, fp_lift c')
           ∈ (mttm_step (fp_delta Sg bl le k st tt table N deltaM)) ^^ n"
  using assms
proof (induction n arbitrary: c')
  case 0
  show ?case using 0 by simp
next
  case (Suc n)
  from Suc.prems obtain c'' where sn: "(c, c'') ∈ (mttm_step deltaM) ^^ n"
    and s1: "(c'', c') ∈ mttm_step deltaM"
    by (blast elim: relpow_Suc_E)
  have "(fp_lift c, fp_lift c'')
          ∈ (mttm_step (fp_delta Sg bl le k st tt table N deltaM)) ^^ n"
    by (rule Suc.IH[OF sn])
  moreover have "(fp_lift c'', fp_lift c')
                   ∈ mttm_step (fp_delta Sg bl le k st tt table N deltaM)"
    by (rule fp_run_step[OF s1])
  ultimately show ?case by (rule relpow_Suc_I)
qed

text ‹A short accepted input is decided in ‹length w + 2› steps --- the
  endmarker read, the ‹length w› scan steps, and the dispatch --- without
  running ‹M› (the same ‹+2› as the recogniser).›

lemma fp_short_time:
  assumes vM: "valid_mttm M" and wSg: "set w ⊆ Sigma_tm M"
    and lenN: "length w ≤ N" and tab: "table w"
  shows "accepts_in_time_mttm (finite_patch M table N) w (length w + 2)"
proof -
  let ?dl = "fp_delta (Sigma_tm M) (bl_tm M) (le_tm M) (k_tm M)
               (s_tm M) (t_tm M) table N (delta_tm M)"
  let ?R = "mttm_step ?dl"
  let ?sc = "fp_scan_config (bl_tm M) (le_tm M) (k_tm M) w"
  let ?init = "init_config_mttm (finite_patch M table N) w"
  let ?acc = "Config⇩M (FP_Run (t_tm M))
                (λi n. if i < k_tm M
                       then (if n = 0 then le_tm M
                             else if i = 0 ∧ n ≤ length w then w ! (n - 1) else bl_tm M)
                       else bl_tm M)
                (λi::nat. if i = 0 then length w + 1 else 0)"
  have kpos: "0 < k_tm M" by (rule valid_mttm_k_pos[OF vM])
  have le: "(?init, ?sc 0) ∈ ?R ^^ 1" using fp_le_step[OF kpos] by simp
  have sc: "(?sc 0, ?sc (length w)) ∈ ?R ^^ (length w)"
    by (rule fp_scan_chain[OF kpos order_refl lenN wSg])
  have ac1: "(?sc (length w), ?acc) ∈ ?R" using tab wSg lenN by (rule fp_accept_step)
  have ac: "(?sc (length w), ?acc) ∈ ?R ^^ 1" using ac1 by simp
  have t1: "(?init, ?sc (length w)) ∈ ?R ^^ (1 + length w)"
    by (rule relpow_transI[OF le sc])
  have t2: "(?init, ?acc) ∈ ?R ^^ (1 + length w + 1)"
    by (rule relpow_transI[OF t1 ac])
  have run: "(?init, ?acc) ∈ ?R ^^ (length w + 2)" using t2 by (simp add: add.commute)
  have "mt_state ?acc = FP_Run (t_tm M)" by simp
  thus ?thesis
    unfolding accepts_in_time_mttm_def finite_patch_delta_tm finite_patch_t_tm
    using run by blast
qed

text ‹A long accepted input is decided in ‹t + c0› steps, where ‹t›
  bounds ‹M›'s own acceptance time and the additive constant
  ‹c0 = 2 * N + 4› is the finite-control overhead --- the endmarker read,
  the ‹N› scan steps to the cutoff, the overflow, the ‹N + 1› rewind
  steps, and the handoff.›

lemma fp_long_time:
  assumes vM: "valid_mttm M" and wSg: "set w ⊆ Sigma_tm M"
    and Nlt: "N < length w" and acc: "accepts_in_time_mttm M w t"
  shows "accepts_in_time_mttm (finite_patch M table N) w (t + (2 * N + 4))"
proof -
  let ?dl = "fp_delta (Sigma_tm M) (bl_tm M) (le_tm M) (k_tm M)
               (s_tm M) (t_tm M) table N (delta_tm M)"
  let ?R = "mttm_step ?dl"
  let ?sc = "fp_scan_config (bl_tm M) (le_tm M) (k_tm M) w"
  let ?rw = "fp_rewind_config (bl_tm M) (le_tm M) (k_tm M) w"
  let ?init = "init_config_mttm (finite_patch M table N) w"
  have kpos: "0 < k_tm M" by (rule valid_mttm_k_pos[OF vM])
  have Nle: "N ≤ length w" using Nlt by simp
  have N1le: "N + 1 ≤ length w" using Nlt by simp
  have le: "(?init, ?sc 0) ∈ ?R ^^ 1" using fp_le_step[OF kpos] by simp
  have sc: "(?sc 0, ?sc N) ∈ ?R ^^ N"
    by (rule fp_scan_chain[OF kpos Nle order_refl wSg])
  have ov: "(?sc N, ?rw (N + 1)) ∈ ?R ^^ 1"
    using fp_overflow_step[OF kpos Nlt wSg] by simp
  have rc: "(?rw (N + 1), ?rw 0) ∈ ?R ^^ (N + 1)"
    by (rule fp_rewind_chain[OF kpos N1le wSg])
  have dn: "(?rw 0, fp_lift (init_config_mttm M w)) ∈ ?R ^^ 1"
    using fp_rewind_done_step[OF kpos] by simp
  from acc obtain n cMn where nt: "n ≤ t"
    and mreach: "(init_config_mttm M w, cMn) ∈ (mttm_step (delta_tm M)) ^^ n"
    and mst: "mt_state cMn = t_tm M"
    unfolding accepts_in_time_mttm_def by blast
  have sim: "(fp_lift (init_config_mttm M w), fp_lift cMn) ∈ ?R ^^ n"
    by (rule fp_run_relpow[OF mreach])
  have c1: "(?init, ?sc N) ∈ ?R ^^ (1 + N)"
    by (rule relpow_transI[OF le sc])
  have c2: "(?init, ?rw (N + 1)) ∈ ?R ^^ (1 + N + 1)"
    by (rule relpow_transI[OF c1 ov])
  have c3: "(?init, ?rw 0) ∈ ?R ^^ (1 + N + 1 + (N + 1))"
    by (rule relpow_transI[OF c2 rc])
  have c4: "(?init, fp_lift (init_config_mttm M w)) ∈ ?R ^^ (1 + N + 1 + (N + 1) + 1)"
    by (rule relpow_transI[OF c3 dn])
  have c5: "(?init, fp_lift cMn) ∈ ?R ^^ (1 + N + 1 + (N + 1) + 1 + n)"
    by (rule relpow_transI[OF c4 sim])
  ― ‹keep the raw step count (‹2 * N + 4 + n›) as the witness rather than
     rewrite the relpow exponent, which the simplifier would peel into a
     relcomp chain›
  have bound: "1 + N + 1 + (N + 1) + 1 + n ≤ t + (2 * N + 4)" using nt by simp
  have "mt_state (fp_lift cMn) = FP_Run (t_tm M)" using mst by (simp add: mt_state_fp_lift)
  thus ?thesis
    unfolding accepts_in_time_mttm_def finite_patch_delta_tm finite_patch_t_tm
    using c5 bound by blast
qed

end