Theory Multitape_Substrate
theory Multitape_Substrate
imports Multitape_Substrate_Core
begin
section ‹Substrate metatheory›
text ‹The substrate metatheory --- ∗‹our› additions over the
Dalvit--Thiemann definition surface isolated in ‹Multitape_Substrate_Core›:
relation-power and finiteness utilities, the ‹valid_mttm›
axiom-extraction toolkit, per-step and reachability validity
preservation, and the displacement / left-endmarker / no-write tape
tools. The core (‹Multitape_Substrate_Core›) carries the datatypes, accessors,
step relation, and the validity / language definitions.›
subsection ‹Relation-power and finiteness utilities›
lemma finite_UNIV_dir [simp, intro]: "finite (UNIV :: dir set)"
proof -
have id: "UNIV = {L, R, N}"
using dir.exhaust by auto
show ?thesis unfolding id by auto
qed
hide_const (open) L R N
text ‹Blank-tail finiteness: the set of total functions ‹nat ⇒ 'b›
ranging in a finite codomain ‹B› and ∗‹constant ‹c› beyond an
index ‹k›› is finite. This replaces the function-space finiteness
lemmas (‹fin_funcsetI› / ‹finite_UNIV_fun_dir›) that the AFP source
relied on: those are false at the value-level ‹nat› index, where
the domain is infinite. Finiteness is recovered from the support
bound — a blank-tail function is determined by its restriction to
‹{..<k}›, of which there are finitely many. Used to re-derive
‹finite δ› for constructed machines (‹valid_mttm_finite_delta›),
with codomain ‹Γ› (blank tail) for read/write tuples and ‹dir›
(N tail) for the move tuples.›
lemma finite_tail_const_funcs:
fixes B :: "'b set" and k :: nat and c :: 'b
assumes finB: "finite B"
shows "finite {f :: nat ⇒ 'b. (∀j. f j ∈ B) ∧ (∀j ≥ k. f j = c)}"
proof -
let ?S = "{f :: nat ⇒ 'b. (∀j. f j ∈ B) ∧ (∀j ≥ k. f j = c)}"
have inj: "inj_on (λf. restrict f {..<k}) ?S"
proof (rule inj_onI)
fix f g
assume f: "f ∈ ?S" and g: "g ∈ ?S"
and eq: "restrict f {..<k} = restrict g {..<k}"
show "f = g"
proof
fix j
show "f j = g j"
proof (cases "j < k")
case True
have "restrict f {..<k} j = restrict g {..<k} j" using eq by simp
thus ?thesis using True by (simp add: restrict_def)
next
case False
hence "k ≤ j" by simp
with f g show ?thesis by simp
qed
qed
qed
have rng: "(λf. restrict f {..<k}) ` ?S ⊆ ({..<k} →⇩E B)"
proof
fix h assume "h ∈ (λf. restrict f {..<k}) ` ?S"
then obtain f where f: "f ∈ ?S" and h: "h = restrict f {..<k}" by blast
show "h ∈ {..<k} →⇩E B"
using f unfolding h by (simp add: restrict_PiE Pi_iff)
qed
have finPiE: "finite ({..<k} →⇩E B)" using finB by (simp add: finite_PiE)
have "finite ((λf. restrict f {..<k}) ` ?S)"
by (rule finite_subset[OF rng finPiE])
thus "finite ?S" using inj by (rule finite_imageD)
qed
lemma relpow_transI:
"(x, y) ∈ R^^n ⟹ (y, z) ∈ R^^m ⟹ (x, z) ∈ R^^(n + m)"
by (simp add: relcomp.intros relpow_add)
lemma relpow_mono: fixes R :: "'a rel"
shows "R ⊆ S ⟹ R^^n ⊆ S^^n"
by (induct n, auto)
text ‹Bounded-iteration combinator: given a single-step law that,
from any config satisfying an index-parameterised invariant
‹P i› with ‹i < n›, takes one ‹R›-step to a config satisfying
‹P (Suc i)›, iterate it: from ‹P 0 c⇩0› reach a ‹c'› with
‹(c⇩0, c') ∈ R⇗n⇖› and ‹P n c'›. A loop whose counter
starts at some ‹off > 0› instantiates ‹P› to re-index by that
offset. Proved by induction generalising ∗‹both› the start
config and the invariant, so the hypothesis applies to the shifted
predicate ‹λj. P (Suc j)› after peeling the first step
(prepended via ‹relpow_Suc_I2›).›
lemma relpow_invariant_chain:
fixes R :: "('s × 's) set"
and P :: "nat ⇒ 's ⇒ bool"
assumes step: "⋀i c. ⟦ i < n; P i c ⟧
⟹ ∃c'. (c, c') ∈ R ∧ P (Suc i) c'"
and base: "P 0 c0"
shows "∃c'. (c0, c') ∈ R ^^ n ∧ P n c'"
using assms
proof (induction n arbitrary: c0)
case 0
show ?case using "0.prems"(2) by auto
next
case (Suc m)
have step_m:
"⋀i c. ⟦ i < m; P i c ⟧
⟹ ∃c'. (c, c') ∈ R ∧ P (Suc i) c'"
proof -
fix i :: nat and c :: 's
assume "i < m" and "P i c"
thus "∃c'. (c, c') ∈ R ∧ P (Suc i) c'"
using Suc.prems(1)[of i c] by simp
qed
obtain c_m where chain_m: "(c0, c_m) ∈ R ^^ m" and Pcm: "P m c_m"
using Suc.IH[OF step_m Suc.prems(2)] by blast
obtain c' where last_step: "(c_m, c') ∈ R" and Pc': "P (Suc m) c'"
using Suc.prems(1)[of m c_m] Pcm by auto
have "(c0, c') ∈ R ^^ Suc m"
using chain_m last_step by (rule relpow_Suc_I)
thus ?case using Pc' by blast
qed
subsection ‹Functional axiom-extraction toolkit›
text ‹Convenience lemmas projecting the substrate's structural
axioms out of @{const valid_mttm} at the functional layer.
Each one is a one-shot ‹by (cases M) auto›: the case-decomposition
rewrites @{term M} into MTTM-form, exposes the @{thm[source] valid_mttm.simps}
conjunction, and ‹auto› extracts the relevant conjunct.
These replace what used to be locale-routed retrievals of the
form ‹multitape_tm.X[OF loc]›.›
lemma valid_mttm_finite_Q:
assumes "valid_mttm M"
shows "finite (Q_tm M)"
using assms by (cases M) auto
lemma valid_mttm_finite_Gamma:
assumes "valid_mttm M"
shows "finite (Γ_tm M)"
using assms by (cases M) auto
lemma valid_mttm_Sigma_sub_Gamma:
assumes "valid_mttm M"
shows "Sigma_tm M ⊆ Γ_tm M"
using assms by (cases M) auto
lemma valid_mttm_s_in_Q:
assumes "valid_mttm M"
shows "s_tm M ∈ Q_tm M"
using assms by (cases M) auto
lemma valid_mttm_t_in_Q:
assumes "valid_mttm M"
shows "t_tm M ∈ Q_tm M"
using assms by (cases M) auto
lemma valid_mttm_r_in_Q:
assumes "valid_mttm M"
shows "r_tm M ∈ Q_tm M"
using assms by (cases M) auto
lemma valid_mttm_blank_in_Gamma:
assumes "valid_mttm M"
shows "bl_tm M ∈ Γ_tm M"
using assms by (cases M) auto
lemma valid_mttm_blank_not_Sigma:
assumes "valid_mttm M"
shows "bl_tm M ∉ Sigma_tm M"
using assms by (cases M) auto
lemma valid_mttm_LE_in_Gamma:
assumes "valid_mttm M"
shows "le_tm M ∈ Γ_tm M"
using assms by (cases M) auto
lemma valid_mttm_LE_not_Sigma:
assumes "valid_mttm M"
shows "le_tm M ∉ Sigma_tm M"
using assms by (cases M) auto
lemma valid_mttm_t_neq_r:
assumes "valid_mttm M"
shows "t_tm M ≠ r_tm M"
using assms by (cases M) auto
lemma valid_mttm_k_pos:
assumes "valid_mttm M"
shows "0 < k_tm M"
using assms by (cases M) auto
lemma valid_mttm_delta_set:
assumes "valid_mttm M"
shows "delta_tm M ⊆
(Q_tm M - {t_tm M, r_tm M})
× (UNIV → Γ_tm M)
× Q_tm M
× (UNIV → Γ_tm M)
× (UNIV → UNIV)"
using assms by (cases M) auto
text ‹Range typing for transition tuples: pulls the four
per-component facts from a single transition membership.›
lemma valid_mttm_delta:
assumes vM: "valid_mttm M"
and tr: "(q, a, q', b, d) ∈ delta_tm M"
shows "q ∈ Q_tm M" "a k ∈ Γ_tm M" "q' ∈ Q_tm M" "b k ∈ Γ_tm M"
using valid_mttm_delta_set[OF vM] tr by auto
text ‹Left-endmarker discipline: transitions reading ‹le› must
rewrite ‹le› with itself and move only ‹N› or ‹R›.›
lemma valid_mttm_deltaLE:
assumes vM: "valid_mttm M"
and tr: "(q, a, q', a', d) ∈ delta_tm M"
and LE: "a k = le_tm M"
shows "a' k = le_tm M ∧ d k ∈ {dir.N, dir.R}"
using vM tr LE by (cases M) auto
text ‹Left-endmarker write discipline: a transition writes ‹le› on
tape ‹k› only when it was reading ‹le› on the same tape. This is
exactly the content of @{const le_unique} specialised to one tape /
transition; it is the sole place that fact is extracted. Needed by
‹ae_coupled_run_aux› to preserve the "no LE in window" invariant
across an M-step. Takes @{const le_unique} (not @{const valid_mttm}):
it is the property a machine may forgo, so consumers thread it
explicitly rather than reading it off ‹valid_mttm›.›
lemma valid_mttm_deltaLE_no_write:
assumes lu: "le_unique M"
and tr: "(q, a, q', a', d) ∈ delta_tm M"
and LE': "a' k = le_tm M"
shows "a k = le_tm M"
using lu[unfolded le_unique_def] tr LE' by blast
text ‹Support invariant: every transition of a valid machine is
blank on reads and writes, and stationary, at every tape index
‹j ≥ k_tm M›. The value-level confinement of a ‹k›-tape machine's
action to tapes ‹0 … k - 1›.›
lemma valid_mttm_delta_support:
assumes vM: "valid_mttm M"
and tr: "(q, a, q', a', d) ∈ delta_tm M"
and j: "j ≥ k_tm M"
shows "a j = bl_tm M ∧ a' j = bl_tm M ∧ d j = dir.N"
proof -
obtain Q Σ Γ bl le δ s t r K where M_eq:
"M = MTTM Q Σ Γ bl le δ s t r K"
by (cases M)
have supp:
"∀q a q' a' d. (q, a, q', a', d) ∈ δ ⟶
(∀j ≥ K. a j = bl ∧ a' j = bl ∧ d j = dir.N)"
using vM[unfolded M_eq valid_mttm.simps] by blast
from tr M_eq have tr_delta: "(q, a, q', a', d) ∈ δ" by simp
from j M_eq have jK: "j ≥ K" by simp
have bleq: "bl_tm M = bl" using M_eq by simp
from supp tr_delta jK have "a j = bl ∧ a' j = bl ∧ d j = dir.N" by blast
thus ?thesis using bleq by simp
qed
text ‹Finiteness of ‹δ› from bounded support: a valid machine's
transition relation is finite. The value-level replacement for
the AFP source's function-space finiteness over a finite tape
type. Each transition's read / write tuples range in the finite
@{term Γ} and are blank beyond ‹k›, each move tuple is ‹N›
beyond ‹k›; by @{thm[source] finite_tail_const_funcs} there are
finitely many of each, so ‹δ› embeds in a finite product.›
lemma valid_mttm_finite_delta:
assumes vM: "valid_mttm M"
shows "finite (delta_tm M)"
proof -
obtain Q Σ Γ bl le δ s t r K where M_eq:
"M = MTTM Q Σ Γ bl le δ s t r K"
by (cases M)
have finQ: "finite Q" using valid_mttm_finite_Q[OF vM] M_eq by simp
have finG: "finite Γ" using valid_mttm_finite_Gamma[OF vM] M_eq by simp
let ?A = "{a. (∀j. a j ∈ Γ) ∧ (∀j ≥ K. a j = bl)}"
let ?D = "{d. (∀j. d j ∈ (UNIV :: dir set)) ∧ (∀j ≥ K. d j = dir.N)}"
have finA: "finite ?A" by (rule finite_tail_const_funcs[OF finG, of K bl])
have finD: "finite ?D" by (rule finite_tail_const_funcs[OF finite_UNIV_dir, of K dir.N])
have finprod: "finite ((Q - {t, r}) × ?A × Q × ?A × ?D)"
using finQ finA finD by (intro finite_cartesian_product) auto
have sub: "delta_tm M ⊆ (Q - {t, r}) × ?A × Q × ?A × ?D"
proof
fix x assume xd: "x ∈ delta_tm M"
obtain q a q' a' d where x: "x = (q, a, q', a', d)"
by (cases x)
from valid_mttm_delta_set[OF vM] xd x M_eq
have q_mem: "q ∈ Q - {t, r}" and a_pi: "a ∈ UNIV → Γ"
and q'_mem: "q' ∈ Q" and a'_pi: "a' ∈ UNIV → Γ"
by auto
from a_pi have aG: "∀j. a j ∈ Γ" by (auto simp: Pi_iff)
from a'_pi have a'G: "∀j. a' j ∈ Γ" by (auto simp: Pi_iff)
have trM: "(q, a, q', a', d) ∈ delta_tm M" using xd x by simp
have supp: "∀j ≥ K. a j = bl ∧ a' j = bl ∧ d j = dir.N"
proof (intro allI impI)
fix j assume "K ≤ j"
hence "j ≥ k_tm M" using M_eq by simp
thus "a j = bl ∧ a' j = bl ∧ d j = dir.N"
using valid_mttm_delta_support[OF vM trM] M_eq by simp
qed
have "a ∈ ?A" using aG supp by auto
moreover have "a' ∈ ?A" using a'G supp by auto
moreover have "d ∈ ?D" using supp by auto
ultimately show "x ∈ (Q - {t, r}) × ?A × Q × ?A × ?D"
using x q_mem q'_mem by auto
qed
show ?thesis using sub finprod by (rule finite_subset)
qed
text ‹State membership at the source of an ‹mttm_step›: the
source state is in ‹Q_tm M› and is neither the accept nor
the reject state. Direct consequence of the ‹mttm_step›
introduction rule plus ‹valid_mttm_delta_set›'s range typing
(which excludes halting states from the source projection of
‹delta_tm M›).
Used by the chunked-induction engine
‹ae_simulation_phase_chunked›: when the M-trace
‹(cM, cM_final) ∈ mttm_step (delta_tm M) ^^ (Suc n)›
is non-empty, the first step exists and forces ‹cM›'s state
to be non-halt and in ‹Q›, which feeds
‹ae_simulates_forward_stage_general›'s ‹qM_in_Q› /
‹q_neq_t› / ‹q_neq_r› hypotheses.›
lemma mttm_step_src:
fixes M :: "('q, 'a) mttm"
assumes vM: "valid_mttm M"
and step: "(c, c') ∈ mttm_step (delta_tm M)"
shows mttm_step_src_in_Q: "mt_state c ∈ Q_tm M"
and mttm_step_src_neq_t: "mt_state c ≠ t_tm M"
and mttm_step_src_neq_r: "mt_state c ≠ r_tm M"
proof -
from step obtain q ts n q' a dir where
c_eq: "c = Config⇩M q ts n"
and tr: "(q, λk. ts k (n k), q', a, dir) ∈ delta_tm M"
by (auto elim: mttm_step.cases)
have q_eq: "mt_state c = q" using c_eq by simp
have q_in_strict: "q ∈ Q_tm M - {t_tm M, r_tm M}"
using valid_mttm_delta_set[OF vM] tr by auto
show "mt_state c ∈ Q_tm M" using q_eq q_in_strict by simp
show "mt_state c ≠ t_tm M" using q_eq q_in_strict by simp
show "mt_state c ≠ r_tm M" using q_eq q_in_strict by simp
qed
subsection ‹Functional validity preservation›
text ‹Per-step preservation of @{const valid_config_mttm}: a valid
configuration steps only to valid configurations. Re-derived
directly from @{thm[source] valid_mttm_delta} (range typing),
@{thm[source] valid_mttm_deltaLE} (left-endmarker discipline),
and @{thm[source] valid_mttm_delta_support} (the new inactive-tape
blank-tail case).›
lemma valid_step_mttm:
fixes M :: "('q, 'a) mttm"
assumes vM: "valid_mttm M"
and step: "(c, c') ∈ mttm_step (delta_tm M)"
and val_c: "valid_config_mttm M c"
shows "valid_config_mttm M c'"
proof -
obtain Q Σ Γ bl le δ s t r K where M_eq:
"M = MTTM Q Σ Γ bl le δ s t r K"
by (cases M)
obtain q ts n where c_eq: "c = Config⇩M q ts n"
by (cases c)
from step M_eq c_eq have step_delta:
"(Config⇩M q ts n, c') ∈ mttm_step δ"
by simp
obtain q' a dir where c'_eq:
"c' = Config⇩M q' (λk. (ts k)(n k := a k))
(λk. go_dir (dir k) (n k))"
and tr: "(q, (λk. ts k (n k)), q', a, dir) ∈ δ"
using step_delta by (auto elim: mttm_step.cases)
from val_c c_eq M_eq have q_in: "q ∈ Q"
and ts_Gamma: "⋀k. range (ts k) ⊆ Γ"
and ts_LE: "⋀k. k < K ⟹ ts k 0 = le"
and ts_blank: "⋀k p. k ≥ K ⟹ ts k p = bl"
by auto
from tr M_eq have tr_M: "(q, (λk. ts k (n k)), q', a, dir) ∈ delta_tm M"
by simp
have q'_in: "q' ∈ Q_tm M" and a_Gamma: "⋀k. a k ∈ Γ_tm M"
using valid_mttm_delta[OF vM tr_M] by auto
hence q'_in_Q: "q' ∈ Q" and a_Gamma_set: "⋀k. a k ∈ Γ"
using M_eq by auto
have new_ts_Gamma: "⋀k. range ((ts k)(n k := a k)) ⊆ Γ"
using ts_Gamma a_Gamma_set by auto
have new_LE: "⋀k. k < K ⟹ ((ts k)(n k := a k)) 0 = le"
proof -
fix k assume kK: "k < K"
show "((ts k)(n k := a k)) 0 = le"
proof (cases "n k = 0")
case True
have read_LE: "(λj. ts j (n j)) k = le"
using ts_LE[OF kK] True by simp
have read_LE_le: "(λj. ts j (n j)) k = le_tm M"
using read_LE M_eq by simp
have "a k = le_tm M"
using valid_mttm_deltaLE[OF vM tr_M read_LE_le] by simp
hence "a k = le" using M_eq by simp
with True show ?thesis by simp
next
case False
thus ?thesis using ts_LE[OF kK] by simp
qed
qed
have new_blank: "⋀k p. k ≥ K ⟹ ((ts k)(n k := a k)) p = bl"
proof -
fix k p assume kK: "k ≥ K"
have ak_bl: "a k = bl"
proof -
have "k ≥ k_tm M" using kK M_eq by simp
hence "a k = bl_tm M"
using valid_mttm_delta_support[OF vM tr_M] by simp
thus ?thesis using M_eq by simp
qed
show "((ts k)(n k := a k)) p = bl"
using ts_blank[OF kK] ak_bl by (cases "p = n k") auto
qed
show ?thesis
unfolding M_eq c'_eq valid_config_mttm.simps
proof (intro conjI allI impI)
show "q' ∈ Q" using q'_in_Q .
next
fix i
show "range ((λk. (ts k)(n k := a k)) i) ⊆ Γ"
using new_ts_Gamma by simp
next
fix i assume "i < K"
show "(λk. (ts k)(n k := a k)) i 0 = le"
using new_LE[OF ‹i < K›] by simp
next
fix i p assume "K ≤ i"
show "(λk. (ts k)(n k := a k)) i p = bl"
using new_blank[OF ‹K ≤ i›] by simp
qed
qed
text ‹Initial-configuration validity: a valid ‹M›'s initial
configuration on a valid input is itself valid.›
lemma valid_init_config_mttm:
fixes M :: "('q, 'a) mttm"
assumes vM: "valid_mttm M"
and w: "set w ⊆ Sigma_tm M"
shows "valid_config_mttm M (init_config_mttm M w)"
proof -
obtain Q Σ Γ bl le δ s t r K where M_eq:
"M = MTTM Q Σ Γ bl le δ s t r K"
by (cases M)
have w_Sigma: "set w ⊆ Σ"
using w M_eq by simp
have s_in: "s ∈ Q" using valid_mttm_s_in_Q[OF vM] M_eq by simp
have Sigma_sub: "Σ ⊆ Γ" using valid_mttm_Sigma_sub_Gamma[OF vM] M_eq by simp
have bl_in: "bl ∈ Γ" using valid_mttm_blank_in_Gamma[OF vM] M_eq by simp
have le_in: "le ∈ Γ" using valid_mttm_LE_in_Gamma[OF vM] M_eq by simp
show ?thesis
unfolding M_eq init_config_mttm.simps valid_config_mttm.simps
proof (intro conjI allI impI)
show "s ∈ Q" using s_in .
next
fix i
show "range (λ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) ⊆ Γ"
proof (cases "i < K")
case True
show ?thesis
using bl_in le_in Sigma_sub w_Sigma True
by (force simp: set_conv_nth)
next
case False
show ?thesis using bl_in False by simp
qed
next
fix i assume "i < K"
show "(if i < K
then (if (0::nat) = 0 then le
else if i = 0 ∧ 0 ≤ length w then w ! (0 - 1)
else bl)
else bl) = le"
using ‹i < K› by simp
next
fix i p assume "K ≤ i"
show "(if i < K
then (if p = 0 then le
else if i = 0 ∧ p ≤ length w then w ! (p - 1)
else bl)
else bl) = bl"
using ‹K ≤ i› by simp
qed
qed
text ‹Reachability lift: every configuration reachable from a
valid initial configuration is itself valid.›
lemma valid_reach_mttm:
fixes M :: "('q, 'a) mttm"
assumes vM: "valid_mttm M"
and w: "set w ⊆ Sigma_tm M"
and reach: "(init_config_mttm M w, c) ∈ (mttm_step (delta_tm M))⇧*"
shows "valid_config_mttm M c"
using reach
proof induction
case base
show ?case using valid_init_config_mttm[OF vM w] .
next
case (step y z)
show ?case using valid_step_mttm[OF vM step.hyps(2) step.IH] .
qed
text ‹Blank-tail accessor for a valid configuration: beyond the
machine's tape count ‹k_tm M› every cell holds the blank
‹bl_tm M›. Used on the reverse lift's padding tapes, where the
per-tape window invariant is unavailable (it constrains the LE
home cell, which is blank on padding) and the read-match must
instead come from the substrate blank-tail.›
lemma valid_config_mttm_blank_tail:
assumes valc: "valid_config_mttm M c"
and kge: "i ≥ k_tm M"
shows "mt_tape c i p = bl_tm M"
proof -
obtain Q Σ Γ bl le δ s t r K where
M_eq: "M = MTTM Q Σ Γ bl le δ s t r K"
by (cases M)
obtain q ts n where c_eq: "c = Config⇩M q ts n" by (cases c)
from valc kge show ?thesis
unfolding M_eq c_eq by auto
qed
text ‹Validity preservation along an ‹n›-step substrate trace
from an arbitrary valid configuration (generic relpow closure of
@{thm[source] valid_step_mttm}; @{thm[source] valid_reach_mttm}
anchors only at ‹init_config_mttm›). Threads the blank-tail
validity of the reverse lift's intermediate configs ‹cM_n'›
through the chain induction.›
lemma valid_reach_relpow_mttm:
assumes vM: "valid_mttm M"
and valc: "valid_config_mttm M c"
and reach: "(c, c') ∈ mttm_step (delta_tm M) ^^ n"
shows "valid_config_mttm M c'"
using reach
proof (induction n arbitrary: c')
case 0
thus ?case using valc by simp
next
case (Suc n)
from Suc.prems obtain c'' where
mid: "(c, c'') ∈ mttm_step (delta_tm M) ^^ n"
and lst: "(c'', c') ∈ mttm_step (delta_tm M)"
by (rule relpow_Suc_E)
have "valid_config_mttm M c''" using Suc.IH[OF mid] .
thus ?case by (rule valid_step_mttm[OF vM lst])
qed
text ‹Per-tape LE-pinning corollary: along any reachable trace
from a valid initial configuration, every ∗‹active› tape
(index ‹k < k_tm M›) carries ‹le_tm M› at position 0.
Note: ‹valid_config_mttm› only encodes the position-0 = LE
constraint on active tapes, not the converse (positions ‹p ≠ 0›
may legally hold LE in an arbitrary valid config). The "LE only
at position 0" property is reach-specific and proved separately
in the companion lemma below.›
lemma valid_reach_LE_pos0_mttm:
fixes M :: "('q, 'a) mttm"
assumes vM: "valid_mttm M"
and w: "set w ⊆ Sigma_tm M"
and reach: "(init_config_mttm M w, Config⇩M q ts n)
∈ (mttm_step (delta_tm M))⇧*"
and kK: "k < k_tm M"
shows "ts k 0 = le_tm M"
proof -
have val: "valid_config_mttm M (Config⇩M q ts n)"
using valid_reach_mttm[OF vM w reach] .
obtain Q Σ Γ bl le δ sM t r K where M_eq:
"M = MTTM Q Σ Γ bl le δ sM t r K"
by (cases M)
have "k < K" using kK M_eq by simp
thus ?thesis using val M_eq by simp
qed
text ‹Dual to @{thm[source] valid_reach_LE_pos0_mttm}: along any reachable
trace from a valid initial configuration whose blank symbol differs
from the left endmarker, every cell at a position ‹p ≠ 0› on any
tape is not the left endmarker. Proof: induction on the
reachability relation. Base: ‹init_config_mttm› places ‹le›
only at position 0 of active tapes (input cells are in ‹Σ› hence
‹≠ le›; other active cells and all inactive cells are ‹bl› which
by hypothesis ‹≠ le›). Step: cells away from the head are
preserved (substrate update is ‹(ts k)(n k := a k)›); at the head,
the substrate's ‹δLE›-no-write rule says the write equals ‹le›
only if the read did, which by IH is impossible since the read
sits at the head position ‹n k› (and if ‹n k = p ≠ 0› the IH
gives the read is not ‹le›; if ‹n k = 0› then ‹p ≠ n k› and the
off-head case fires).›
lemma valid_reach_LE_only_pos0_mttm:
fixes M :: "('q, 'a) mttm"
and c :: "('a, 'q) mt_config"
and k :: nat
and p :: nat
assumes vM: "valid_mttm M"
and lu: "le_unique M"
and w: "set w ⊆ Sigma_tm M"
and reach: "(init_config_mttm M w, c) ∈ (mttm_step (delta_tm M))⇧*"
and p_ne_0: "p ≠ 0"
and bl_neq_le: "bl_tm M ≠ le_tm M"
shows "mt_tape c k p ≠ le_tm M"
proof -
obtain Q Σ Γ bl le δ sM tt rr K where M_eq:
"M = MTTM Q Σ Γ bl le δ sM tt rr K"
by (cases M)
have le_eq: "le_tm M = le" using M_eq by simp
have bl_eq: "bl_tm M = bl" using M_eq by simp
have bl_ne_le: "bl ≠ le" using bl_neq_le le_eq bl_eq by simp
have le_not_Sigma: "le ∉ Σ"
using valid_mttm_LE_not_Sigma[OF vM] M_eq by simp
have w_Sigma: "set w ⊆ Σ" using w M_eq by simp
have main:
"∀c'. (init_config_mttm M w, c') ∈ (mttm_step (delta_tm M))⇧*
⟶ mt_tape c' k p ≠ le_tm M"
proof (intro allI impI)
fix c'
assume r: "(init_config_mttm M w, c') ∈ (mttm_step (delta_tm M))⇧*"
show "mt_tape c' k p ≠ le_tm M"
using r
proof induction
case base
have tape_p_init:
"mt_tape (init_config_mttm M w) k p
= (if k < K
then (if p = 0 then le
else if k = 0 ∧ p ≤ length w then w ! (p - 1)
else bl)
else bl)"
unfolding M_eq init_config_mttm.simps by simp
show ?case
proof (cases "k = 0 ∧ p ≤ length w")
case True
have K_pos: "0 < K" using valid_mttm_k_pos[OF vM] M_eq by simp
have kK: "k < K" using True K_pos by simp
have p_ge_1: "p ≥ 1" using p_ne_0 by simp
have idx_lt: "p - 1 < length w" using True p_ge_1 by linarith
have in_w: "w ! (p - 1) ∈ set w"
using idx_lt by (auto simp: set_conv_nth)
with w_Sigma have "w ! (p - 1) ∈ Σ" by blast
with le_not_Sigma have "w ! (p - 1) ≠ le" by blast
thus ?thesis using tape_p_init True kK p_ne_0 le_eq by simp
next
case False
have "mt_tape (init_config_mttm M w) k p = bl"
using tape_p_init False p_ne_0 by (cases "k < K") auto
thus ?thesis using bl_ne_le le_eq by simp
qed
next
case (step y z)
have ne_y: "mt_tape y k p ≠ le_tm M" using step.IH .
obtain qy ts n where y_eq: "y = Config⇩M qy ts n"
by (cases y)
from step.hyps(2) y_eq obtain q' a dr where
z_eq: "z = Config⇩M q'
(λkk. (ts kk)(n kk := a kk))
(λkk. go_dir (dr kk) (n kk))"
and tr: "(qy, (λkk. ts kk (n kk)), q', a, dr) ∈ delta_tm M"
by (auto elim: mttm_step.cases)
show ?case
proof (cases "n k = p")
case False
have "mt_tape z k p = ((ts k)(n k := a k)) p" using z_eq by simp
also have "… = ts k p" using False by simp
also have "… = mt_tape y k p" using y_eq by simp
finally have "mt_tape z k p = mt_tape y k p" .
thus ?thesis using ne_y by simp
next
case True
have read_at_p: "ts k (n k) = mt_tape y k p"
using y_eq True by simp
have read_ne: "ts k (n k) ≠ le_tm M"
using ne_y read_at_p by simp
have a_ne: "a k ≠ le_tm M"
proof
assume a_le: "a k = le_tm M"
have "(λkk. ts kk (n kk)) k = le_tm M"
using valid_mttm_deltaLE_no_write[OF lu tr a_le] by simp
hence "ts k (n k) = le_tm M" by simp
thus False using read_ne by simp
qed
have "mt_tape z k p = ((ts k)(n k := a k)) p" using z_eq by simp
also have "… = a k" using True by simp
finally have "mt_tape z k p = a k" .
thus ?thesis using a_ne by simp
qed
qed
qed
show ?thesis using main reach by blast
qed
subsection ‹Step locality: non-head cells preserved, head moves by ‹≤› 1›
text ‹Two structural facts about ‹mttm_step› that fall directly out
of the single rule's body ‹(ts k)(n k := a k)› and
‹go_dir (dir k) (n k)›: a single step modifies only the head
cell on each tape, and the head displaces by at most one position
per tape per step. These are generic over ‹δ› and used by
alphabet-enlargement / -reduction to argue that cells outside a
bounded window are unchanged after ‹n› steps.›
lemma mttm_step_tape_off_head:
assumes step: "(c, c') ∈ mttm_step δ"
and ne: "p ≠ mt_pos c k"
shows "mt_tape c' k p = mt_tape c k p"
proof -
from step obtain q ts n q' a dr where
c_eq: "c = Config⇩M q ts n"
and c'_eq: "c' = Config⇩M q'
(λk. (ts k)(n k := a k))
(λk. go_dir (dr k) (n k))"
by (auto elim: mttm_step.cases)
from ne c_eq have "p ≠ n k" by simp
thus ?thesis by (simp add: c_eq c'_eq)
qed
lemma mttm_step_pos_displacement:
assumes step: "(c, c') ∈ mttm_step δ"
shows "mt_pos c' k ≤ mt_pos c k + 1
∧ mt_pos c k ≤ mt_pos c' k + 1"
proof -
from step obtain q ts n q' a dr where
c_eq: "c = Config⇩M q ts n"
and c'_eq: "c' = Config⇩M q'
(λk. (ts k)(n k := a k))
(λk. go_dir (dr k) (n k))"
by (auto elim: mttm_step.cases)
have pos: "mt_pos c k = n k" by (simp add: c_eq)
have pos': "mt_pos c' k = go_dir (dr k) (n k)" by (simp add: c'_eq)
show ?thesis
unfolding pos pos' by (cases "dr k") auto
qed
text ‹‹n›-step lift: after ‹n› steps, head displacement on each
tape is at most ‹n›.›
lemma mttm_relpow_pos_displacement:
assumes "(c, c') ∈ mttm_step δ ^^ n"
shows "mt_pos c' k ≤ mt_pos c k + n
∧ mt_pos c k ≤ mt_pos c' k + n"
using assms
proof (induction n arbitrary: c')
case 0
thus ?case by simp
next
case (Suc n)
from Suc.prems obtain c'' where
ih: "(c, c'') ∈ mttm_step δ ^^ n"
and step: "(c'', c') ∈ mttm_step δ"
by (auto elim: relpow_Suc_E)
have h1: "mt_pos c'' k ≤ mt_pos c k + n
∧ mt_pos c k ≤ mt_pos c'' k + n"
using Suc.IH[OF ih] .
have h2: "mt_pos c' k ≤ mt_pos c'' k + 1
∧ mt_pos c'' k ≤ mt_pos c' k + 1"
using mttm_step_pos_displacement[OF step] .
from h1 h2 show ?case by linarith
qed
text ‹‹n›-step lift: cells more than ‹n› away from the start head
position are unchanged after ‹n› steps.›
lemma mttm_relpow_tape_off_window:
assumes "(c, c') ∈ mttm_step δ ^^ n"
and "p > mt_pos c k + n ∨ p + n < mt_pos c k"
shows "mt_tape c' k p = mt_tape c k p"
using assms
proof (induction n arbitrary: c')
case 0
thus ?case by simp
next
case (Suc n)
from Suc.prems(1) obtain c'' where
ih: "(c, c'') ∈ mttm_step δ ^^ n"
and step: "(c'', c') ∈ mttm_step δ"
by (auto elim: relpow_Suc_E)
have far: "p > mt_pos c k + n ∨ p + n < mt_pos c k"
using Suc.prems(2) by linarith
have eq_ih: "mt_tape c'' k p = mt_tape c k p"
using Suc.IH[OF ih far] .
have disp: "mt_pos c'' k ≤ mt_pos c k + n
∧ mt_pos c k ≤ mt_pos c'' k + n"
using mttm_relpow_pos_displacement[OF ih] .
have ne: "p ≠ mt_pos c'' k"
using Suc.prems(2) disp by linarith
have eq_step: "mt_tape c' k p = mt_tape c'' k p"
using mttm_step_tape_off_head[OF step ne] .
show ?case using eq_step eq_ih by simp
qed
subsection ‹Left-endmarker pinning at position 0 along execution›
text ‹Local LE-pinning: any step of a valid M from a config whose
tape ‹k› already has ‹le_tm M› at position 0 ends with a config
whose tape ‹k› still has ‹le_tm M› at position 0. Standalone
variant of ‹valid_step_mttm›'s position-0-= LE conjunct,
stripped of the ‹valid_config_mttm› precondition: only the
per-tape LE-at-0 fact is needed (not Q-membership or ‹Γ›-typing).
Case-split on whether the head is at position 0: at-head fires
‹δLE› (read LE forces write LE); off-head uses
‹mttm_step_tape_off_head› directly.›
lemma mttm_step_LE_pos0_preserve:
fixes M :: "('q, 'a) mttm"
assumes vM: "valid_mttm M"
and step: "(c, c') ∈ mttm_step (delta_tm M)"
and LE_at0: "mt_tape c k 0 = le_tm M"
shows "mt_tape c' k 0 = le_tm M"
proof (cases "mt_pos c k = 0")
case True
from step obtain q ts n q' a dr where
c_eq: "c = Config⇩M q ts n"
and c'_eq: "c' = Config⇩M q'
(λkk. (ts kk)(n kk := a kk))
(λkk. go_dir (dr kk) (n kk))"
and tr: "(q, λkk. ts kk (n kk), q', a, dr) ∈ delta_tm M"
by (auto elim: mttm_step.cases)
have nk_0: "n k = 0" using True c_eq by simp
have ts_k_0_le: "ts k 0 = le_tm M" using LE_at0 c_eq by simp
have read_LE: "(λkk. ts kk (n kk)) k = le_tm M"
using ts_k_0_le nk_0 by simp
have write_LE: "a k = le_tm M"
using valid_mttm_deltaLE[OF vM tr read_LE] by simp
have "mt_tape c' k 0 = ((ts k)(n k := a k)) 0"
using c'_eq by simp
also have "… = a k" using nk_0 by simp
also have "… = le_tm M" using write_LE .
finally show ?thesis .
next
case False
have ne_0: "(0 :: nat) ≠ mt_pos c k" using False by simp
have unchanged: "mt_tape c' k 0 = mt_tape c k 0"
using mttm_step_tape_off_head[OF step ne_0] .
show ?thesis using unchanged LE_at0 by simp
qed
text ‹‹n›-step lift of @{thm[source] mttm_step_LE_pos0_preserve}: along
any chain of M-steps, ‹le_tm M› at position 0 is preserved
on every tape. Used in AE's LE-edge forward stage to derive
‹cM_k›'s position-0 = LE without recourse to reachability
from init.›
lemma mttm_relpow_LE_pos0_preserve:
fixes M :: "('q, 'a) mttm"
assumes vM: "valid_mttm M"
and chain: "(c, c') ∈ mttm_step (delta_tm M) ^^ n"
and LE_at0: "mt_tape c k 0 = le_tm M"
shows "mt_tape c' k 0 = le_tm M"
using chain
proof (induction n arbitrary: c')
case 0
thus ?case using LE_at0 by simp
next
case (Suc n)
from Suc.prems obtain c'' where
ih: "(c, c'') ∈ mttm_step (delta_tm M) ^^ n"
and step: "(c'', c') ∈ mttm_step (delta_tm M)"
by (auto elim: relpow_Suc_E)
have at_c'': "mt_tape c'' k 0 = le_tm M" using Suc.IH[OF ih] .
show ?case
using mttm_step_LE_pos0_preserve[OF vM step at_c''] .
qed
subsection ‹Step structural decomposition›
text ‹Packages ‹mttm_step.cases› with the post-state position +
tape equations on each tape: a single ‹obtains› rule that
yields all four useful facts (pre-state's state, post-state's
state, the per-tape position equation ‹go_dir (dr k) (n k)›,
and the per-tape head-cell update). Chain proofs in
AE / AR / TR avoid re-doing the case-analysis at every
per-substep position-trajectory step.›
lemma mttm_step_obtain_action:
assumes step: "(c, c') ∈ mttm_step δ"
obtains q q' a dr where
"mt_state c = q"
and "mt_state c' = q'"
and "(q, λk. mt_tape c k (mt_pos c k), q', a, dr) ∈ δ"
and "⋀kk. mt_pos c' kk = go_dir (dr kk) (mt_pos c kk)"
and "⋀kk p. p ≠ mt_pos c kk
⟹ mt_tape c' kk p = mt_tape c kk p"
and "⋀kk. mt_tape c' kk (mt_pos c kk) = a kk"
proof -
from step obtain q ts n q' a dr where
c_eq: "c = Config⇩M q ts n"
and c'_eq: "c' = Config⇩M q'
(λk. (ts k)(n k := a k))
(λk. go_dir (dr k) (n k))"
and tr: "(q, λk. ts k (n k), q', a, dr) ∈ δ"
by (auto elim: mttm_step.cases)
have st_c: "mt_state c = q" using c_eq by simp
have st_c': "mt_state c' = q'" using c'_eq by simp
have pos_c: "⋀kk. mt_pos c kk = n kk" using c_eq by simp
have pos_c': "⋀kk. mt_pos c' kk = go_dir (dr kk) (n kk)"
using c'_eq by simp
have tape_c: "⋀kk. mt_tape c kk = ts kk" using c_eq by simp
have tape_c': "⋀kk. mt_tape c' kk = (ts kk)(n kk := a kk)"
using c'_eq by simp
have tr': "(q, λk. mt_tape c k (mt_pos c k), q', a, dr) ∈ δ"
using tr c_eq by simp
show thesis
proof (rule that[OF st_c st_c' tr'])
fix kk show "mt_pos c' kk = go_dir (dr kk) (mt_pos c kk)"
using pos_c' pos_c by simp
next
fix kk p assume "p ≠ mt_pos c kk"
thus "mt_tape c' kk p = mt_tape c kk p"
using tape_c' tape_c pos_c by simp
next
fix kk show "mt_tape c' kk (mt_pos c kk) = a kk"
using tape_c' pos_c by simp
qed
qed
subsection ‹No-write deltas: tape preserved across a step›
text ‹For a transition relation in which every tuple's
read-component equals its write-component, a single step
preserves the entire tape function (the substrate update
‹f(x := f x)› is the identity). Used by the alphabet-
enlargement chain proof for the read-only buffer-loading
substeps SS1‹→›SS2, SS2‹→›SS3, SS3‹→›SS4, SS4‹→›SS5.›
lemma mttm_step_no_write_tape:
assumes step: "(c, c') ∈ mttm_step δ"
and no_write: "⋀q a q' a' d. (q, a, q', a', d) ∈ δ ⟹ a' = a"
shows "mt_tape c' = mt_tape c"
proof -
from step obtain q ts n q' a dr where
c_eq: "c = Config⇩M q ts n"
and c'_eq: "c' = Config⇩M q'
(λk. (ts k)(n k := a k))
(λk. go_dir (dr k) (n k))"
and tr: "(q, λk. ts k (n k), q', a, dr) ∈ δ"
by (auto elim: mttm_step.cases)
from no_write[OF tr] have "a = (λk. ts k (n k))" by simp
hence "(λk. (ts k)(n k := a k)) = ts" by auto
thus ?thesis by (simp add: c_eq c'_eq)
qed
subsection ‹Step determinism and acceptance monotonicity›
text ‹Two general facts promoted from the finite-control layer: a step of
a functional transition relation is deterministic (a configuration has at
most one successor), and weak time-bounded acceptance is monotone in the
time budget.›
lemma mttm_step_functional:
assumes fdet: "∀q a p⇩1 b⇩1 d⇩1 p⇩2 b⇩2 d⇩2.
(q, a, p⇩1, b⇩1, d⇩1) ∈ δ ⟶ (q, a, p⇩2, b⇩2, d⇩2) ∈ δ
⟶ (p⇩1, b⇩1, d⇩1) = (p⇩2, b⇩2, d⇩2)"
and step1: "(c, c1) ∈ mttm_step δ"
and step2: "(c, c2) ∈ mttm_step δ"
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' (λk. (ts k)(n k := a1 k)) (λk. go_dir (d1 k) (n k))"
and tr1: "(q, λk. ts k (n k), q1', a1, d1) ∈ δ"
by (auto elim: mttm_step.cases)
from step2 obtain q2' a2 d2 where
c2_eq: "c2 = Config⇩M q2' (λk. (ts k)(n k := a2 k)) (λk. go_dir (d2 k) (n k))"
and tr2: "(q, λk. ts k (n k), q2', a2, d2) ∈ δ"
using c_eq by (auto elim: mttm_step.cases)
have "(q1', a1, d1) = (q2', a2, d2)" using fdet tr1 tr2 by blast
thus ?thesis using c1_eq c2_eq by simp
qed
text ‹Weak time-bounded acceptance is monotone in the time budget.›
lemma accepts_in_time_mttm_mono:
"accepts_in_time_mttm M w t ⟹ t ≤ t' ⟹ accepts_in_time_mttm M w t'"
unfolding accepts_in_time_mttm_def by (meson order_trans)
end