Theory Multitape_Alphabet_Reduction.AlphabetReduction_Delta
theory AlphabetReduction_Delta
imports AlphabetReduction_Stage
begin
subsection ‹Substep transition relations›
text ‹The output machine's ‹δ'› is defined as a
union of five per-substep transition relations, mirroring
AE's ‹alphabet_enlarge_delta› shape. Each substep
relation is a set of substrate-shape 5-tuples
‹((q, stg), a, (q', stg'), a', d)› where
‹q› ranges over ‹Q_tm M›, ‹stg›
over ‹'a ar_stage›, ‹a› /
‹a'› over ‹nat ⇒ sym4›, and
‹d› over ‹nat ⇒ dir›. The five substep
relations are defined below, one per simulation phase.
No validation cluster: AR's language theorem is quantified
over encoder-image inputs only, so non-canonical sym4 inputs
are outside the theorem's scope and M''s behaviour on them is
unconstrained.
The union is intersected with two global restrictions:
LE-preservation (no transition forges ‹LE4› out of
a non-‹LE4› cell, matching the substrate's
‹δLE› invariant) and
‹ar_valid_stage›-membership on both source and
target stages (matching the non-product ‹Q'› shape).
Throughout, ‹b› abbreviates ‹block_width Γ› (the per-symbol cell width).›
definition ar_delta_read ::
"('q, 'a) mttm
⇒ (('q × 'a ar_stage)
× (nat ⇒ sym4)
× ('q × 'a ar_stage)
× (nat ⇒ sym4)
× (nat ⇒ dir)) set" where
"ar_delta_read M =
{((q, AR_SimRead, tk, 0, buf, dvec, posk), a,
(q, AR_SimRead, k_succ tk, 0,
buf(tk := le_tm M), dvec, posk), a, d) |
q tk buf dvec posk a d.
q ∈ Q_tm M
∧ ¬ is_last_k M tk
∧ posk tk = AR_AtLE
∧ a tk = LE4
∧ d = (λkk. if kk = tk then dir.R else dir.N)}
∪
{((q, AR_SimRead, tk, 0, buf, dvec, posk), a,
(q, AR_SimCompute, k_unidx 0, 0,
buf(tk := le_tm M), dvec, posk), a, d) |
q tk buf dvec posk a d.
q ∈ Q_tm M
∧ is_last_k M tk
∧ posk tk = AR_AtLE
∧ a tk = LE4
∧ d = (λkk. if kk = tk then dir.R else dir.N)}
∪
{((q, AR_SimRead, tk, 0, buf, dvec, posk), a,
(q, AR_SimRead, tk, Suc 0, buf, dvec, posk), a, d) |
q tk buf dvec posk a d.
q ∈ Q_tm M
∧ posk tk ∈ {AR_AtFirstProper, AR_AtFurtherProper}
∧ a tk ≠ LE4
∧ d = (λkk. if kk = tk then dir.L else dir.N)}
∪
{((q, AR_SimRead, tk, Suc 0, buf, dvec, posk), a,
(q, AR_SimRead, tk, Suc (Suc 0),
buf(tk := gamma_unenum (Γ_tm M) (bl_tm M) 0),
dvec,
posk(tk := if a tk = LE4 then AR_AtFirstProper
else AR_AtFurtherProper)), a, d) |
q tk buf dvec posk a d.
q ∈ Q_tm M
∧ posk tk ∈ {AR_AtFirstProper, AR_AtFurtherProper}
∧ d = (λkk. if kk = tk then dir.R else dir.N)}
∪
{((q, AR_SimRead, tk, i, buf, dvec, posk), a,
(q, AR_SimRead, tk, Suc i,
buf(tk := gamma_unenum (Γ_tm M) (bl_tm M)
(2 * gamma_enum (Γ_tm M) (bl_tm M) (buf tk)
+ bit_value (a tk))),
dvec, posk), a, d) |
q tk i buf dvec posk a d.
q ∈ Q_tm M
∧ posk tk ∈ {AR_AtFirstProper, AR_AtFurtherProper}
∧ 2 ≤ i
∧ Suc i ≤ Suc (block_width (Γ_tm M))
∧ d = (λkk. if kk = tk then dir.R else dir.N)}
∪
{((q, AR_SimRead, tk, i, buf, dvec, posk), a,
(q, AR_SimRead, k_succ tk, 0,
buf(tk := gamma_unenum (Γ_tm M) (bl_tm M)
(2 * gamma_enum (Γ_tm M) (bl_tm M) (buf tk)
+ bit_value (a tk))),
dvec, posk), a, d) |
q tk i buf dvec posk a d.
q ∈ Q_tm M
∧ ¬ is_last_k M tk
∧ posk tk ∈ {AR_AtFirstProper, AR_AtFurtherProper}
∧ i = Suc (block_width (Γ_tm M))
∧ d = (λkk. if kk = tk then dir.R else dir.N)}
∪
{((q, AR_SimRead, tk, i, buf, dvec, posk), a,
(q, AR_SimCompute, k_unidx 0, 0,
buf(tk := gamma_unenum (Γ_tm M) (bl_tm M)
(2 * gamma_enum (Γ_tm M) (bl_tm M) (buf tk)
+ bit_value (a tk))),
dvec, posk), a, d) |
q tk i buf dvec posk a d.
q ∈ Q_tm M
∧ is_last_k M tk
∧ posk tk ∈ {AR_AtFirstProper, AR_AtFurtherProper}
∧ i = Suc (block_width (Γ_tm M))
∧ d = (λkk. if kk = tk then dir.R else dir.N)}"
definition ar_delta_compute ::
"('q, 'a) mttm
⇒ (('q × 'a ar_stage)
× (nat ⇒ sym4)
× ('q × 'a ar_stage)
× (nat ⇒ sym4)
× (nat ⇒ dir)) set" where
"ar_delta_compute M =
{((q, AR_SimCompute, tk, i, buf, dvec, posk), a,
(q', AR_SimWrite, 0, 0, m_a', m_d, posk), a, d) |
q buf q' m_a' m_d tk i dvec posk a d.
(q, buf, q', m_a', m_d) ∈ delta_tm M
∧ d = (λ_. dir.N)}"
definition ar_delta_write ::
"('q, 'a) mttm
⇒ (('q × 'a ar_stage)
× (nat ⇒ sym4)
× ('q × 'a ar_stage)
× (nat ⇒ sym4)
× (nat ⇒ dir)) set" where
"ar_delta_write M =
{((q, AR_SimWrite, tk, 0, buf, dvec, posk), a,
(q, AR_SimWrite, k_succ tk, 0, buf, dvec, posk), a, d) |
q tk buf dvec posk a d.
q ∈ Q_tm M
∧ posk tk = AR_AtLE
∧ ¬ is_last_k M tk
∧ d = (λ_. dir.N)}
∪
{((q, AR_SimWrite, tk, 0, buf, dvec, posk), a,
(q, AR_SimAdvance, k_unidx 0, 0, buf, dvec, posk), a, d) |
q tk buf dvec posk a d.
q ∈ Q_tm M
∧ posk tk = AR_AtLE
∧ is_last_k M tk
∧ d = (λ_. dir.N)}
∪
{((q, AR_SimWrite, tk, i, buf, dvec, posk), a,
(q, AR_SimWrite, tk, Suc i, buf, dvec, posk), a, d) |
q tk i buf dvec posk a d.
q ∈ Q_tm M
∧ posk tk ≠ AR_AtLE
∧ a tk ≠ LE4
∧ Suc i ≤ block_width (Γ_tm M)
∧ d = (λkk. if kk = tk then dir.L else dir.N)}
∪
{((q, AR_SimWrite, tk, i, buf, dvec, posk), a,
(q, AR_SimWrite, tk, Suc i, buf, dvec, posk), a', d) |
q tk i buf dvec posk a a' d.
q ∈ Q_tm M
∧ posk tk ≠ AR_AtLE
∧ block_width (Γ_tm M) ≤ i
∧ Suc i < 2 * block_width (Γ_tm M)
∧ a' = (λkk. if kk = tk
then write_bit (Γ_tm M) (bl_tm M)
(buf tk)
(i - block_width (Γ_tm M))
else a kk)
∧ d = (λkk. if kk = tk then dir.R else dir.N)}
∪
{((q, AR_SimWrite, tk, i, buf, dvec, posk), a,
(q, AR_SimWrite, k_succ tk, 0, buf, dvec, posk), a', d) |
q tk i buf dvec posk a a' d.
q ∈ Q_tm M
∧ posk tk ≠ AR_AtLE
∧ ¬ is_last_k M tk
∧ Suc i = 2 * block_width (Γ_tm M)
∧ a' = (λkk. if kk = tk
then write_bit (Γ_tm M) (bl_tm M)
(buf tk)
(i - block_width (Γ_tm M))
else a kk)
∧ d = (λkk. if kk = tk then dir.R else dir.N)}
∪
{((q, AR_SimWrite, tk, i, buf, dvec, posk), a,
(q, AR_SimAdvance, k_unidx 0, 0, buf, dvec, posk), a', d) |
q tk i buf dvec posk a a' d.
q ∈ Q_tm M
∧ posk tk ≠ AR_AtLE
∧ is_last_k M tk
∧ Suc i = 2 * block_width (Γ_tm M)
∧ a' = (λkk. if kk = tk
then write_bit (Γ_tm M) (bl_tm M)
(buf tk)
(i - block_width (Γ_tm M))
else a kk)
∧ d = (λkk. if kk = tk then dir.R else dir.N)}"
definition ar_delta_advance ::
"('q, 'a) mttm
⇒ (('q × 'a ar_stage)
× (nat ⇒ sym4)
× ('q × 'a ar_stage)
× (nat ⇒ sym4)
× (nat ⇒ dir)) set" where
"ar_delta_advance M =
{((q, AR_SimAdvance, tk, i, buf, dvec, posk), a,
(q, AR_SimAdvance, tk, Suc i, buf, dvec, posk), a, d) |
q tk i buf dvec posk a d.
q ∈ Q_tm M
∧ a tk ≠ LE4
∧ Suc i < ar_disp (block_width (Γ_tm M)) (dvec tk) (posk tk)
∧ d = (λkk. if kk = tk then dir.L else dir.N)}
∪
{((q, AR_SimAdvance, tk, i, buf, dvec, posk), a,
(q, AR_SimAdvance, k_succ tk, 0, buf, dvec,
posk(tk := ar_newpos (dvec tk) (posk tk))), a, d) |
q tk i buf dvec posk a d.
q ∈ Q_tm M
∧ ¬ is_last_k M tk
∧ ((dvec tk = dir.R ∧ i = 0)
∨ (dvec tk ≠ dir.R
∧ a tk ≠ LE4
∧ Suc i = ar_disp (block_width (Γ_tm M))
(dvec tk) (posk tk)))
∧ d = (λkk. if kk = tk ∧ dvec tk ≠ dir.R
then dir.L else dir.N)}
∪
{((q, AR_SimAdvance, tk, i, buf, dvec, posk), a,
(q, AR_SimNext, k_unidx 0, 0, buf, dvec,
posk(tk := ar_newpos (dvec tk) (posk tk))), a, d) |
q tk i buf dvec posk a d.
q ∈ Q_tm M
∧ is_last_k M tk
∧ ((dvec tk = dir.R ∧ i = 0)
∨ (dvec tk ≠ dir.R
∧ a tk ≠ LE4
∧ Suc i = ar_disp (block_width (Γ_tm M))
(dvec tk) (posk tk)))
∧ d = (λkk. if kk = tk ∧ dvec tk ≠ dir.R
then dir.L else dir.N)}"
definition ar_delta_next ::
"('q, 'a) mttm
⇒ (('q × 'a ar_stage)
× (nat ⇒ sym4)
× ('q × 'a ar_stage)
× (nat ⇒ sym4)
× (nat ⇒ dir)) set" where
"ar_delta_next M =
{((q, AR_SimNext, tk, i, buf, dvec, posk), a,
(q, AR_SimRead, 0, 0, buf, dvec, posk), a, d) |
q tk i buf dvec posk a d.
q ∈ Q_tm M ∧ q ≠ t_tm M ∧ q ≠ r_tm M
∧ d = (λ_. dir.N)}
∪
{((q, AR_SimNext, tk, i, buf, dvec, posk), a,
(q, AR_HaltAccept, 0, 0,
(λ_. bl_tm M), (λ_. dir.N), (λ_. AR_AtLE)), a, d) |
q tk i buf dvec posk a d.
q = t_tm M
∧ d = (λ_. dir.N)}
∪
{((q, AR_SimNext, tk, i, buf, dvec, posk), a,
(q, AR_HaltReject, 0, 0,
(λ_. bl_tm M), (λ_. dir.N), (λ_. AR_AtLE)), a, d) |
q tk i buf dvec posk a d.
q = r_tm M
∧ d = (λ_. dir.N)}"
text ‹The output machine's full transition relation: union of
the five per-substep relations, intersected with three global
restrictions — ‹δLE›-backward (no transition forges
‹LE4› out of a non-‹LE4› cell),
‹δLE›-forward (every transition reading ‹LE4›
on tape ‹k› rewrites ‹LE4› back on the same tape
and moves ‹N› or ‹R›), and
‹ar_valid_stage›-membership on both source and target
stages. The two ‹δLE› filters together discharge
the substrate's bidirectional ‹δLE› invariant
uniformly — without per-arm ‹a tk ≠ LE4›
preconditions on every arm that performs a write distinct from
the read cell (proper-arm forward-write in particular). The
per-arm ‹a tk ≠ LE4› constraints that do appear (in
look-back step 1, back-walk, and advance L-step) reflect the
simulation invariant rather than the bare ‹δLE›
requirement: those arms move ‹L› on the current tape,
which the substrate forbids from an ‹LE4› cell
regardless of write content.›
definition alphabet_reduce_delta ::
"('q, 'a) mttm
⇒ (('q × 'a ar_stage)
× (nat ⇒ sym4)
× ('q × 'a ar_stage)
× (nat ⇒ sym4)
× (nat ⇒ dir)) set" where
"alphabet_reduce_delta M =
(ar_delta_read M ∪ ar_delta_compute M
∪ ar_delta_write M ∪ ar_delta_advance M
∪ ar_delta_next M)
∩ {(s, a, s', a', d).
∀k. a' k = LE4 ⟶ a k = LE4}
∩ {(s, a, s', a', d).
∀k. a k = LE4 ⟶ a' k = LE4 ∧ d k ∈ {dir.N, dir.R}}
∩ {(s, a, s', a', d).
ar_valid_stage (Γ_tm M) (bl_tm M) (snd s)
∧ ar_valid_stage (Γ_tm M) (bl_tm M) (snd s')}
∩ {(s, a, s', a', d).
∀j ≥ k_tm M. a j = BLANK4 ∧ a' j = BLANK4 ∧ d j = dir.N}
∩ {(s, a, s', a', d).
ar_stage_bounded (bl_tm M) (k_tm M) (snd s)
∧ ar_stage_bounded (bl_tm M) (k_tm M) (snd s')}"
text ‹Initial / halt stages used to populate the output
machine's ‹s'› / ‹t'› / ‹r'›
components. All three share the same shape: substep-counter
‹i = 0›, current-tape ‹0›
placeholder (per-tape phase fields are inactive in
‹AR_SimRead›'s initial entry and inactive in halt
states), per-tape ‹buf› initialised to
‹bl› (any value in ‹Γ ∪ ⦃bl⦄› would
satisfy ‹ar_valid_stage›; ‹bl› is the
canonical placeholder), per-tape direction-vector
‹dir.N› (irrelevant outside ‹AR_SimAdvance›),
per-tape position-kind ‹AR_AtLE› (the initial
head position is ‹0›; for halt states the field is
vestigial). The three stages differ only in their
‹ar_substep_idx› tag.›
definition ar_init_stage ::
"'a ⇒ 'a ar_stage" where
"ar_init_stage bl =
(AR_SimRead, 0, 0, (λ_. bl), (λ_. dir.N), (λ_. AR_AtLE))"
definition ar_accept_stage ::
"'a ⇒ 'a ar_stage" where
"ar_accept_stage bl =
(AR_HaltAccept, 0, 0, (λ_. bl), (λ_. dir.N), (λ_. AR_AtLE))"
definition ar_reject_stage ::
"'a ⇒ 'a ar_stage" where
"ar_reject_stage bl =
(AR_HaltReject, 0, 0, (λ_. bl), (λ_. dir.N), (λ_. AR_AtLE))"
text ‹Positivity of the block width: ‹b› is bounded below
by ‹1› via the ‹max› on the right-hand side. Used
below to discharge the ‹i < 2 ⋅ b› conjunct of
‹ar_valid_stage› at ‹i = 0›, and downstream by
the per-substep step-count lemmas.›
lemma block_width_pos: "1 ≤ block_width Γ"
unfolding block_width_def by simp
text ‹The three stage constants used to populate ‹s'›,
‹t'›, and ‹r'› all satisfy
‹ar_valid_stage Γ bl› for any ‹Γ›
and ‹bl›: the bit-counter is ‹0 < 2 ⋅ b›
(since ‹b ≥ 1›) and the buf field is constantly
‹bl ∈ Γ ∪ ⦃bl⦄›.›
lemma ar_valid_stage_init: "ar_valid_stage Γ bl (ar_init_stage bl)"
proof -
have "(0 :: nat) < 2 * block_width Γ" using block_width_pos[of Γ] by linarith
thus ?thesis
unfolding ar_valid_stage_def ar_init_stage_def by simp
qed
lemma ar_valid_stage_accept: "ar_valid_stage Γ bl (ar_accept_stage bl)"
proof -
have "(0 :: nat) < 2 * block_width Γ" using block_width_pos[of Γ] by linarith
thus ?thesis
unfolding ar_valid_stage_def ar_accept_stage_def by simp
qed
lemma ar_valid_stage_reject: "ar_valid_stage Γ bl (ar_reject_stage bl)"
proof -
have "(0 :: nat) < 2 * block_width Γ" using block_width_pos[of Γ] by linarith
thus ?thesis
unfolding ar_valid_stage_def ar_reject_stage_def by simp
qed
text ‹The alphabet-reduction combinator. Input: ‹mttm› over
‹'a›, with tape alphabet ‹Γ_tm M› a finite subset of
‹'a› (via ‹valid_mttm›) of cardinality ‹≥ 4›.
Output: ‹mttm› over ‹sym4›, with state set
‹'q × 'a ar_stage›. Tape count ‹k_tm M› is preserved.
Output components:
▪ ‹Q'› = ‹Q_M × ⦃stg. ar_valid_stage Γ_M bl_M stg⦄›
(the non-product Q-shape);
▪ ‹Σ'› = ‹⦃BIT0, BIT1⦄›
(the encoded input alphabet);
▪ ‹Γ'› = ‹UNIV :: sym4 set›
(all four cell shapes — BIT0, BIT1, BLANK4, LE4);
▪ ‹bl'› = ‹BLANK4›, ‹le'› = ‹LE4›;
▪ ‹δ'› = ‹alphabet_reduce_delta M›
(the five-substep union under the global LE-preservation
and ‹ar_valid_stage› filters);
▪ ‹s'› = ‹(s_M, ar_init_stage bl_M)›,
‹t'› = ‹(t_M, ar_accept_stage bl_M)›,
‹r'› = ‹(r_M, ar_reject_stage bl_M)›
(M's start / accept / reject states paired with the
matching ‹ar_substep_idx› tag).›
definition alphabet_reduce ::
"('q, 'a) mttm
⇒ ('q × 'a ar_stage, sym4) mttm"
where
"alphabet_reduce M =
(case M of MTTM Q_M _ Γ_M bl_M _ _ s_M t_M r_M k_M ⇒
MTTM (Q_M × {stg. ar_valid_stage Γ_M bl_M stg
∧ ar_stage_bounded bl_M k_M stg})
{BIT0, BIT1}
(UNIV :: sym4 set)
BLANK4
LE4
(alphabet_reduce_delta M)
(s_M, ar_init_stage bl_M)
(t_M, ar_accept_stage bl_M)
(r_M, ar_reject_stage bl_M)
k_M)"
text ‹Projection-simp lemmas for the reduced machine: each
structural accessor reads straight off the ‹MTTM› the
combinator builds. Marked ‹[simp]› so the language and
time proofs never re-derive them via ‹cases M›; the
accept-state projection in particular is the bridge that makes
the simulation engine's terminal state syntactically equal to
‹t_tm (alphabet_reduce M)›.›
lemma alphabet_reduce_Sigma [simp]:
"Sigma_tm (alphabet_reduce M) = {BIT0, BIT1}"
by (cases M) (simp add: alphabet_reduce_def)
lemma alphabet_reduce_Gamma [simp]:
"Γ_tm (alphabet_reduce M) = (UNIV :: sym4 set)"
by (cases M) (simp add: alphabet_reduce_def)
lemma alphabet_reduce_bl [simp]:
"bl_tm (alphabet_reduce M) = BLANK4"
by (cases M) (simp add: alphabet_reduce_def)
lemma alphabet_reduce_le [simp]:
"le_tm (alphabet_reduce M) = LE4"
by (cases M) (simp add: alphabet_reduce_def)
lemma alphabet_reduce_start [simp]:
"s_tm (alphabet_reduce M) = (s_tm M, ar_init_stage (bl_tm M))"
by (cases M) (simp add: alphabet_reduce_def)
lemma alphabet_reduce_accept [simp]:
"t_tm (alphabet_reduce M) = (t_tm M, ar_accept_stage (bl_tm M))"
by (cases M) (simp add: alphabet_reduce_def)
lemma alphabet_reduce_reject [simp]:
"r_tm (alphabet_reduce M) = (r_tm M, ar_reject_stage (bl_tm M))"
by (cases M) (simp add: alphabet_reduce_def)
lemma alphabet_reduce_delta [simp]:
"delta_tm (alphabet_reduce M) = alphabet_reduce_delta M"
by (cases M) (simp add: alphabet_reduce_def)
end