Theory AlphabetReduction_Reverse
theory AlphabetReduction_Reverse
imports AlphabetReduction_Theorems
begin
section ‹Alphabet reduction: reverse language inclusion›
text ‹The reverse leg of ‹alphabet_reduce_language›:
‹encode_input_ar (Γ_tm M) (bl_tm M) w ∈ Lang_mttm (alphabet_reduce M)
⟹ w ∈ Lang_mttm M›, the converse of the proven
‹alphabet_reduce_language_forward›.
Unlike AE's reverse arm, which restricts to ‹det_mttm M› and
closes via chain uniqueness (Path C), AR proves this
unconditionally — deterministic and nondeterministic ‹M›
alike. The counterexample probe is negative: AR's
nondeterminism gateway ‹ar_delta_compute› is a direct
single-step embedding of ‹delta_tm M› (one substrate tuple per
‹M›-tuple, no AE-style ‹m_steps_buffered› slack), so every
accepting ‹M'›-path decodes branch-by-branch to a genuine
accepting ‹M›-path.
Strategy (Strategy B, direct backward inversion): a per-cycle
backward step lemma reads the ‹M›-transition straight off the
compute tuple on the given ‹M'›-path and reuses the forward
arm's invariants ‹ar_simulates›, ‹ar_posk_consistent›,
‹ar_at_read_boundary› read backward; a backward chunked engine
aggregates the per-cycle steps into an ‹M›-run.
Throughout, ‹b› abbreviates ‹block_width Γ› (the per-symbol cell width).›
subsection ‹Terminal accept configuration›
text ‹Base case of the backward engine: the accept state
‹t_tm (alphabet_reduce M)› is terminal. A valid machine never
steps from its accept state (substrate ‹mttm_step_src_neq_t›),
and ‹alphabet_reduce M› is valid by ‹alphabet_reduce_wf›;
its accept state is ‹(t_tm M, ar_accept_stage (bl_tm M))› by
‹alphabet_reduce_accept›.
Itself currently uncalled: the backward engine kills reject boundaries
mid-trace via ‹ar_reject_terminal›, not accept ones; retained as the
documented half of the accept/reject terminal pair.›
lemma ar_accept_terminal:
fixes M :: "('q, 'a) mttm"
and c c' :: "(sym4, 'q × 'a ar_stage) mt_config"
assumes vM: "valid_mttm M"
and card_ge: "card (Γ_tm M) ≥ 4"
and step: "(c, c') ∈ mttm_step (alphabet_reduce_delta M)"
shows "mt_state c ≠ (t_tm M, ar_accept_stage (bl_tm M))"
proof -
let ?M' = "alphabet_reduce M :: ('q × 'a ar_stage, sym4) mttm"
have valM': "valid_mttm ?M'" by (rule alphabet_reduce_wf[OF vM card_ge])
have step': "(c, c') ∈ mttm_step (delta_tm ?M')" using step by simp
have "mt_state c ≠ t_tm ?M'" by (rule mttm_step_src_neq_t[OF valM' step'])
thus ?thesis by simp
qed
text ‹Reject companion of ‹ar_accept_terminal›: the reject state
‹r_tm (alphabet_reduce M) = (r_tm M, ar_reject_stage (bl_tm M))›
(by ‹alphabet_reduce_reject›) is terminal too (substrate
‹mttm_step_src_neq_r›). The backward engine uses it to kill a
reject boundary reached mid-trace: the trace runs to the accept
config, so a reject config can carry no outgoing step.›
lemma ar_reject_terminal:
fixes M :: "('q, 'a) mttm"
and c c' :: "(sym4, 'q × 'a ar_stage) mt_config"
assumes vM: "valid_mttm M"
and card_ge: "card (Γ_tm M) ≥ 4"
and step: "(c, c') ∈ mttm_step (alphabet_reduce_delta M)"
shows "mt_state c ≠ (r_tm M, ar_reject_stage (bl_tm M))"
proof -
let ?M' = "alphabet_reduce M :: ('q × 'a ar_stage, sym4) mttm"
have valM': "valid_mttm ?M'" by (rule alphabet_reduce_wf[OF vM card_ge])
have step': "(c, c') ∈ mttm_step (delta_tm ?M')" using step by simp
have "mt_state c ≠ r_tm ?M'" by (rule mttm_step_src_neq_r[OF valM' step'])
thus ?thesis by simp
qed
subsection ‹Source substep-tags partition the substep relations›
text ‹Each of the five substep relations carries a uniform source
substep-tag (‹fst (snd s)› for a source state ‹s = (q, stg)›),
and the five tags are pairwise distinct datatype constructors. This
is the structural fact every step-inversion lemma rests on: a step
whose source is at substep ‹X› can only come from the relation
whose sources carry tag ‹X›.›
lemma ar_delta_read_src:
"(s, a, s', a', d) ∈ ar_delta_read M ⟹ fst (snd s) = AR_SimRead"
by (auto simp: ar_delta_read_def)
lemma ar_delta_compute_src:
"(s, a, s', a', d) ∈ ar_delta_compute M ⟹ fst (snd s) = AR_SimCompute"
by (auto simp: ar_delta_compute_def)
lemma ar_delta_write_src:
"(s, a, s', a', d) ∈ ar_delta_write M ⟹ fst (snd s) = AR_SimWrite"
by (auto simp: ar_delta_write_def)
lemma ar_delta_advance_src:
"(s, a, s', a', d) ∈ ar_delta_advance M ⟹ fst (snd s) = AR_SimAdvance"
by (auto simp: ar_delta_advance_def)
lemma ar_delta_next_src:
"(s, a, s', a', d) ∈ ar_delta_next M ⟹ fst (snd s) = AR_SimNext"
by (auto simp: ar_delta_next_def)
subsection ‹Destination substep-tags carve the cycle's substep order›
text ‹Each substep relation's destination tag is confined to a
small set: read loops to itself or transitions to compute; compute
is the unique non-deterministic step and lands at write; write
loops or advances; advance loops or hands off to next; next closes
the cycle (back to read) or dispatches to a halt-coerced
configuration. These five facts encode the substep transition
graph and underpin the chain-shape arguments used in the reverse
arm's pinning lemmas.›
lemma ar_delta_read_dest:
"(s, a, s', a', d) ∈ ar_delta_read M ⟹
fst (snd s') = AR_SimRead ∨ fst (snd s') = AR_SimCompute"
by (auto simp: ar_delta_read_def)
lemma ar_delta_compute_dest:
"(s, a, s', a', d) ∈ ar_delta_compute M ⟹ fst (snd s') = AR_SimWrite"
by (auto simp: ar_delta_compute_def)
lemma ar_delta_write_dest:
"(s, a, s', a', d) ∈ ar_delta_write M ⟹
fst (snd s') = AR_SimWrite ∨ fst (snd s') = AR_SimAdvance"
by (auto simp: ar_delta_write_def)
lemma ar_delta_advance_dest:
"(s, a, s', a', d) ∈ ar_delta_advance M ⟹
fst (snd s') = AR_SimAdvance ∨ fst (snd s') = AR_SimNext"
by (auto simp: ar_delta_advance_def)
lemma ar_delta_next_dest:
"(s, a, s', a', d) ∈ ar_delta_next M ⟹
fst (snd s') = AR_SimRead ∨ fst (snd s') = AR_HaltAccept
∨ fst (snd s') = AR_HaltReject"
by (auto simp: ar_delta_next_def ar_accept_stage_def ar_reject_stage_def)
text ‹Union-disambiguation: a tuple in ‹alphabet_reduce_delta M›
whose source is at ‹AR_SimCompute› must lie in the compute
relation ‹ar_delta_compute M›. The intersection filters of
‹alphabet_reduce_delta› (‹δLE› and the valid-stage
guards) only shrink the union, so membership of the union is all we
need; the other four source-tag lemmas rule out the other disjuncts
by constructor-distinctness.›
lemma ar_delta_compute_from_src:
assumes mem: "(s, a, s', a', d) ∈ alphabet_reduce_delta M"
and src: "fst (snd s) = AR_SimCompute"
shows "(s, a, s', a', d) ∈ ar_delta_compute M"
proof -
from mem
have u: "(s, a, s', a', d) ∈ ar_delta_read M ∪ ar_delta_compute M
∪ ar_delta_write M ∪ ar_delta_advance M ∪ ar_delta_next M"
unfolding alphabet_reduce_delta_def by blast
have nr: "(s, a, s', a', d) ∉ ar_delta_read M"
proof
assume "(s, a, s', a', d) ∈ ar_delta_read M"
from ar_delta_read_src[OF this] src show False by simp
qed
have nw: "(s, a, s', a', d) ∉ ar_delta_write M"
proof
assume "(s, a, s', a', d) ∈ ar_delta_write M"
from ar_delta_write_src[OF this] src show False by simp
qed
have nad: "(s, a, s', a', d) ∉ ar_delta_advance M"
proof
assume "(s, a, s', a', d) ∈ ar_delta_advance M"
from ar_delta_advance_src[OF this] src show False by simp
qed
have nx: "(s, a, s', a', d) ∉ ar_delta_next M"
proof
assume "(s, a, s', a', d) ∈ ar_delta_next M"
from ar_delta_next_src[OF this] src show False by simp
qed
from u nr nw nad nx show ?thesis by blast
qed
subsection ‹Compute-step inversion›
text ‹The keystone of the reverse arm: a single ‹M'›-step out of
an ‹AR_SimCompute› configuration reads the simulated
‹M›-transition straight off the compute tuple. Because
‹ar_delta_compute› is a direct single-step embedding of
‹delta_tm M›, the inversion yields a genuine
‹(q, buf, q', m_a', m_d) ∈ delta_tm M› with no chain-uniqueness
or determinism assumption — this is where AR's ND-generality is
earned. Compute neither writes nor moves: the tape and head
positions are unchanged (read symbol equals write symbol, direction
‹N›).›
lemma ar_compute_step_inv_sub:
fixes M :: "('q, 'a) mttm"
and c' c'' :: "(sym4, 'q × 'a ar_stage) mt_config"
assumes step: "(c', c'') ∈ mttm_step (ar_delta_compute M)"
and stg: "mt_state c' = (q, AR_SimCompute, tk, i, buf, dvec, posk)"
obtains q' m_a' m_d where
"(q, buf, q', m_a', m_d) ∈ delta_tm M"
and "mt_state c'' = (q', AR_SimWrite, 0, 0, m_a', m_d, posk)"
and "mt_tape c'' = mt_tape c'"
and "mt_pos c'' = mt_pos c'"
proof -
from step obtain S ts n S'' aw dir where
c'_eq: "c' = Config⇩M S ts n"
and c''_eq: "c'' = Config⇩M S'' (λk. (ts k)(n k := aw k))
(λk. go_dir (dir k) (n k))"
and rel: "(S, (λk. ts k (n k)), S'', aw, dir)
∈ ar_delta_compute M"
by (auto elim: mttm_step.cases)
have S_eq: "S = (q, AR_SimCompute, tk, i, buf, dvec, posk)"
using stg c'_eq by simp
have crel: "((q, AR_SimCompute, tk, i, buf, dvec, posk),
(λk. ts k (n k)), S'', aw, dir) ∈ ar_delta_compute M"
using rel S_eq by simp
from crel obtain q' m_a' m_d where
mdelta: "(q, buf, q', m_a', m_d) ∈ delta_tm M"
and S''_eq: "S'' = (q', AR_SimWrite, 0, 0, m_a', m_d, posk)"
and aw_eq: "aw = (λk. ts k (n k))"
and dir_eq: "dir = (λ_. dir.N)"
unfolding ar_delta_compute_def by auto
have state: "mt_state c'' = (q', AR_SimWrite, 0, 0, m_a', m_d, posk)"
using c''_eq S''_eq by simp
have tape: "mt_tape c'' = mt_tape c'"
proof -
have "mt_tape c'' = (λk. (ts k)(n k := aw k))" using c''_eq by simp
also have "… = ts" by (simp add: aw_eq fun_upd_triv)
finally show ?thesis using c'_eq by simp
qed
have pos: "mt_pos c'' = mt_pos c'"
proof -
have "mt_pos c'' = (λk. go_dir (dir k) (n k))" using c''_eq by simp
also have "… = n" by (simp add: dir_eq)
finally show ?thesis using c'_eq by simp
qed
show ?thesis by (rule that[OF mdelta state tape pos])
qed
text ‹The union-step face of the inversion: lift the union step into
the compute sub-relation (‹ar_step_compute_lift›) and invert there.
Used by the forward walker preservation ‹ar_walker_step_from_at_compute›;
the reverse cycle-close inverts the walker's own sub-relation compute
step directly via ‹ar_compute_step_inv_sub›.›
lemma ar_compute_step_inv:
fixes M :: "('q, 'a) mttm"
and c' c'' :: "(sym4, 'q × 'a ar_stage) mt_config"
assumes step: "(c', c'') ∈ mttm_step (alphabet_reduce_delta M)"
and stg: "mt_state c' = (q, AR_SimCompute, tk, i, buf, dvec, posk)"
obtains q' m_a' m_d where
"(q, buf, q', m_a', m_d) ∈ delta_tm M"
and "mt_state c'' = (q', AR_SimWrite, 0, 0, m_a', m_d, posk)"
and "mt_tape c'' = mt_tape c'"
and "mt_pos c'' = mt_pos c'"
proof -
from step obtain S ts n S'' aw dir where
c'_eq: "c' = Config⇩M S ts n"
and c''_eq: "c'' = Config⇩M S'' (λk. (ts k)(n k := aw k))
(λk. go_dir (dir k) (n k))"
and rel: "(S, (λk. ts k (n k)), S'', aw, dir)
∈ alphabet_reduce_delta M"
by (auto elim: mttm_step.cases)
have src: "fst (snd S) = AR_SimCompute" using stg c'_eq by simp
have crel: "(S, (λk. ts k (n k)), S'', aw, dir) ∈ ar_delta_compute M"
by (rule ar_delta_compute_from_src[OF rel src])
have step_explicit:
"(Config⇩M S ts n, Config⇩M S'' (λk. (ts k)(n k := aw k))
(λk. go_dir (dir k) (n k))) ∈ mttm_step (ar_delta_compute M)"
using crel by (rule mttm_step.step)
have sub: "(c', c'') ∈ mttm_step (ar_delta_compute M)"
using step_explicit c'_eq c''_eq by simp
show thesis
proof (rule ar_compute_step_inv_sub[OF sub stg])
fix q' m_a' m_d
assume "(q, buf, q', m_a', m_d) ∈ delta_tm M"
and "mt_state c'' = (q', AR_SimWrite, 0, 0, m_a', m_d, posk)"
and "mt_tape c'' = mt_tape c'"
and "mt_pos c'' = mt_pos c'"
thus thesis by (rule that)
qed
qed
subsection ‹Next-step inversion (cycle closure / halt dispatch)›
text ‹Source disambiguation for ‹AR_SimNext›, mirroring
‹ar_delta_compute_from_src›.›
lemma ar_delta_next_from_src:
assumes mem: "(s, a, s', a', d) ∈ alphabet_reduce_delta M"
and src: "fst (snd s) = AR_SimNext"
shows "(s, a, s', a', d) ∈ ar_delta_next M"
proof -
from mem
have u: "(s, a, s', a', d) ∈ ar_delta_read M ∪ ar_delta_compute M
∪ ar_delta_write M ∪ ar_delta_advance M ∪ ar_delta_next M"
unfolding alphabet_reduce_delta_def by blast
have nr: "(s, a, s', a', d) ∉ ar_delta_read M"
proof
assume "(s, a, s', a', d) ∈ ar_delta_read M"
from ar_delta_read_src[OF this] src show False by simp
qed
have nc: "(s, a, s', a', d) ∉ ar_delta_compute M"
proof
assume "(s, a, s', a', d) ∈ ar_delta_compute M"
from ar_delta_compute_src[OF this] src show False by simp
qed
have nw: "(s, a, s', a', d) ∉ ar_delta_write M"
proof
assume "(s, a, s', a', d) ∈ ar_delta_write M"
from ar_delta_write_src[OF this] src show False by simp
qed
have nad: "(s, a, s', a', d) ∉ ar_delta_advance M"
proof
assume "(s, a, s', a', d) ∈ ar_delta_advance M"
from ar_delta_advance_src[OF this] src show False by simp
qed
from u nr nc nw nad show ?thesis by blast
qed
text ‹A single ‹M'›-step out of an ‹AR_SimNext›
configuration neither writes nor moves, and dispatches on the
simulated ‹M›-state ‹q›: continue to the next
‹AR_SimRead› boundary when ‹q› is non-halting, or land
in the accept/reject halt stage when ‹q› is ‹M›'s
accept/reject state. The accept landing is exactly
‹t_tm (alphabet_reduce M)›.›
lemma ar_next_step_inv:
fixes M :: "('q, 'a) mttm"
and c' c'' :: "(sym4, 'q × 'a ar_stage) mt_config"
assumes step: "(c', c'') ∈ mttm_step (alphabet_reduce_delta M)"
and stg: "mt_state c' = (q, AR_SimNext, tk, i, buf, dvec, posk)"
shows "mt_tape c'' = mt_tape c' ∧ mt_pos c'' = mt_pos c'
∧ ((q ∉ {t_tm M, r_tm M}
∧ mt_state c'' = (q, AR_SimRead, 0, 0, buf, dvec, posk))
∨ (q = t_tm M
∧ mt_state c'' = (t_tm M, ar_accept_stage (bl_tm M)))
∨ (q = r_tm M
∧ mt_state c'' = (r_tm M, ar_reject_stage (bl_tm M))))"
proof -
from step obtain S ts n S'' aw dir where
c'_eq: "c' = Config⇩M S ts n"
and c''_eq: "c'' = Config⇩M S'' (λk. (ts k)(n k := aw k))
(λk. go_dir (dir k) (n k))"
and rel: "(S, (λk. ts k (n k)), S'', aw, dir)
∈ alphabet_reduce_delta M"
by (auto elim: mttm_step.cases)
have S_eq: "S = (q, AR_SimNext, tk, i, buf, dvec, posk)"
using stg c'_eq by simp
have src: "fst (snd S) = AR_SimNext" using S_eq by simp
have nrel: "((q, AR_SimNext, tk, i, buf, dvec, posk),
(λk. ts k (n k)), S'', aw, dir) ∈ ar_delta_next M"
using ar_delta_next_from_src[OF rel src] S_eq by simp
have core: "aw = (λk. ts k (n k)) ∧ dir = (λ_. dir.N)
∧ ((q ∉ {t_tm M, r_tm M}
∧ S'' = (q, AR_SimRead, 0, 0, buf, dvec, posk))
∨ (q = t_tm M ∧ S'' = (t_tm M, ar_accept_stage (bl_tm M)))
∨ (q = r_tm M ∧ S'' = (r_tm M, ar_reject_stage (bl_tm M))))"
using nrel
unfolding ar_delta_next_def ar_accept_stage_def ar_reject_stage_def
by auto
have tape: "mt_tape c'' = mt_tape c'"
proof -
have "mt_tape c'' = (λk. (ts k)(n k := aw k))" using c''_eq by simp
also have "… = ts" using core by (simp add: fun_upd_triv)
finally show ?thesis using c'_eq by simp
qed
have pos: "mt_pos c'' = mt_pos c'"
proof -
have "mt_pos c'' = (λk. go_dir (dir k) (n k))" using c''_eq by simp
also have "… = n" using core by simp
finally show ?thesis using c'_eq by simp
qed
have st: "mt_state c'' = S''" using c''_eq by simp
show ?thesis using tape pos core st by simp
qed
subsection ‹Determinism of the read substep›
text ‹The read relation is a *function* of (source state, read
symbol): for a fixed source ‹s› and read vector ‹a› the
target state, written vector, and direction are uniquely determined.
The seven arms partition by the bit-counter ‹i›, then within an
‹i›-class by ‹posk tk› / ‹a tk› / ‹is_last_k M tk›.
The one non-obvious exclusion is arm 4 (‹i = Suc 0›) versus arms
6/7 (‹i = Suc (b)›): these collide only if
‹b = 0›, ruled out by ‹block_width_pos› (which is
therefore load-bearing here, not decorative).›
lemma ar_delta_read_func:
fixes M :: "('q, 'a) mttm"
assumes "(s, a, s⇩1, a⇩1, d⇩1) ∈ ar_delta_read M"
and "(s, a, s⇩2, a⇩2, d⇩2) ∈ ar_delta_read M"
shows "(s⇩1, a⇩1, d⇩1) = (s⇩2, a⇩2, d⇩2)"
using assms block_width_pos[of "Γ_tm M"]
by (auto simp: ar_delta_read_def)
text ‹Write is a function of (source, read vector): the LE arms
(‹buf tk = le›) split from the proper arms by the buf cell,
and the proper back-walk / forward-write / boundary arms partition by
the bit-counter ranges ‹[0, b-1]›, ‹[b, 2b-2]›,
‹{2b-1}›, separated arithmetically; ‹is_last_k› splits
the last-tape arms.›
lemma ar_delta_write_func:
fixes M :: "('q, 'a) mttm"
assumes "(s, a, s⇩1, a⇩1, d⇩1) ∈ ar_delta_write M"
and "(s, a, s⇩2, a⇩2, d⇩2) ∈ ar_delta_write M"
shows "(s⇩1, a⇩1, d⇩1) = (s⇩2, a⇩2, d⇩2)"
using assms
by (auto simp: ar_delta_write_def)
text ‹Advance is a function of (source, read vector). The stepping
arm (‹Suc i < ar_disp b (dvec tk) (posk tk)›) is excluded from
the ‹R›-direction boundary sub-case by
‹ar_disp _ dir.R _ = 0› (the first ‹ar_disp›
equation), and from the non-‹R› boundary by ‹<›
versus ‹=› on the displacement; ‹is_last_k› splits the
two boundary arms.›
lemma ar_delta_advance_func:
fixes M :: "('q, 'a) mttm"
assumes "(s, a, s⇩1, a⇩1, d⇩1) ∈ ar_delta_advance M"
and "(s, a, s⇩2, a⇩2, d⇩2) ∈ ar_delta_advance M"
shows "(s⇩1, a⇩1, d⇩1) = (s⇩2, a⇩2, d⇩2)"
using assms
by (auto simp: ar_delta_advance_def)
text ‹Next is a function of the source: the continue / accept /
reject arms partition on the simulated ‹M›-state ‹q› by
‹q ∉ {t, r}› / ‹q = t› / ‹q = r›, mutually
exclusive precisely because ‹valid_mttm M› supplies
‹t_tm M ≠ r_tm M›.
Currently uncalled: the ‹next› substep is the cycle closer, handled
by bespoke inversion (‹ar_next_step_inv›) rather than functional
pinning, so this member of the per-substep determinism family goes
unused; kept to keep that family complete.›
lemma ar_delta_next_func:
fixes M :: "('q, 'a) mttm"
assumes vM: "valid_mttm M"
and "(s, a, s⇩1, a⇩1, d⇩1) ∈ ar_delta_next M"
and "(s, a, s⇩2, a⇩2, d⇩2) ∈ ar_delta_next M"
shows "(s⇩1, a⇩1, d⇩1) = (s⇩2, a⇩2, d⇩2)"
proof -
have tr: "t_tm M ≠ r_tm M" using vM by (cases M) auto
show ?thesis using assms(2,3) tr by (auto simp: ar_delta_next_def)
qed
subsection ‹Source disambiguation for the remaining substeps›
text ‹Source disambiguation for the remaining three substeps,
completing the ‹from_src› family alongside
‹ar_delta_compute_from_src› / ‹ar_delta_next_from_src›.›
lemma ar_delta_read_from_src:
assumes "(s, a, s', a', d) ∈ alphabet_reduce_delta M"
and "fst (snd s) = AR_SimRead"
shows "(s, a, s', a', d) ∈ ar_delta_read M"
using assms unfolding alphabet_reduce_delta_def
by (auto dest: ar_delta_compute_src ar_delta_write_src
ar_delta_advance_src ar_delta_next_src)
lemma ar_delta_write_from_src:
assumes "(s, a, s', a', d) ∈ alphabet_reduce_delta M"
and "fst (snd s) = AR_SimWrite"
shows "(s, a, s', a', d) ∈ ar_delta_write M"
using assms unfolding alphabet_reduce_delta_def
by (auto dest: ar_delta_read_src ar_delta_compute_src
ar_delta_advance_src ar_delta_next_src)
lemma ar_delta_advance_from_src:
assumes "(s, a, s', a', d) ∈ alphabet_reduce_delta M"
and "fst (snd s) = AR_SimAdvance"
shows "(s, a, s', a', d) ∈ ar_delta_advance M"
using assms unfolding alphabet_reduce_delta_def
by (auto dest: ar_delta_read_src ar_delta_compute_src
ar_delta_write_src ar_delta_next_src)
text ‹Every ‹alphabet_reduce_delta› tuple has its source at one
of the five substep tags (the halt tags never appear as sources).›
lemma alphabet_reduce_delta_src_tag:
assumes "(s, a, s', a', d) ∈ alphabet_reduce_delta M"
shows "fst (snd s) ∈ {AR_SimRead, AR_SimCompute, AR_SimWrite,
AR_SimAdvance, AR_SimNext}"
using assms unfolding alphabet_reduce_delta_def
by (auto dest: ar_delta_read_src ar_delta_compute_src ar_delta_write_src
ar_delta_advance_src ar_delta_next_src)
subsection ‹Substep step semantics — ‹mttm_step›-level lands-at›
text ‹Lift the per-relation destination-tag lemmas
(‹ar_delta_X_dest›) up through ‹mttm_step›: an
‹M'›-step out of a configuration whose source idx is
‹AR_SimX› lands at a configuration whose idx is in
‹X›'s dest set. The five lemmas compose
‹mttm_step.cases› (extract the firing tuple), the
‹from_src› union-disambiguation helpers, and
‹ar_delta_X_dest›. Together they encode the cycle's
substep transition graph at the level the substep-walker engine
consumes: SimRead-loop-or-compute, compute-to-write,
write-loop-or-advance, advance-loop-or-next,
next-to-read-or-halt.›
lemma ar_step_from_SimRead_lands:
assumes step: "(c, c') ∈ mttm_step (alphabet_reduce_delta M)"
and src: "fst (snd (mt_state c)) = AR_SimRead"
shows "fst (snd (mt_state c')) = AR_SimRead
∨ fst (snd (mt_state c')) = AR_SimCompute"
proof -
from step obtain S ts n S' aw dir where
c_eq: "c = Config⇩M S ts n"
and c'_eq: "c' = Config⇩M S' (λk. (ts k)(n k := aw k))
(λk. go_dir (dir k) (n k))"
and rel: "(S, (λk. ts k (n k)), S', aw, dir)
∈ alphabet_reduce_delta M"
by (auto elim: mttm_step.cases)
have src_S: "fst (snd S) = AR_SimRead" using src c_eq by simp
have "(S, (λk. ts k (n k)), S', aw, dir) ∈ ar_delta_read M"
using ar_delta_read_from_src[OF rel src_S] .
hence "fst (snd S') = AR_SimRead ∨ fst (snd S') = AR_SimCompute"
by (rule ar_delta_read_dest)
thus ?thesis using c'_eq by simp
qed
text ‹The ‹compute› member of the five-lemma lands-at family above is
currently uncalled: the compute substep is the nondeterministic branch
point, handled by bespoke reconstruct-and-reuse reasoning rather than the
generic lands-at lift. Retained to keep the substep transition graph
complete.›
lemma ar_step_from_SimCompute_lands:
assumes step: "(c, c') ∈ mttm_step (alphabet_reduce_delta M)"
and src: "fst (snd (mt_state c)) = AR_SimCompute"
shows "fst (snd (mt_state c')) = AR_SimWrite"
proof -
from step obtain S ts n S' aw dir where
c_eq: "c = Config⇩M S ts n"
and c'_eq: "c' = Config⇩M S' (λk. (ts k)(n k := aw k))
(λk. go_dir (dir k) (n k))"
and rel: "(S, (λk. ts k (n k)), S', aw, dir)
∈ alphabet_reduce_delta M"
by (auto elim: mttm_step.cases)
have src_S: "fst (snd S) = AR_SimCompute" using src c_eq by simp
have "(S, (λk. ts k (n k)), S', aw, dir) ∈ ar_delta_compute M"
using ar_delta_compute_from_src[OF rel src_S] .
hence "fst (snd S') = AR_SimWrite" by (rule ar_delta_compute_dest)
thus ?thesis using c'_eq by simp
qed
lemma ar_step_from_SimWrite_lands:
assumes step: "(c, c') ∈ mttm_step (alphabet_reduce_delta M)"
and src: "fst (snd (mt_state c)) = AR_SimWrite"
shows "fst (snd (mt_state c')) = AR_SimWrite
∨ fst (snd (mt_state c')) = AR_SimAdvance"
proof -
from step obtain S ts n S' aw dir where
c_eq: "c = Config⇩M S ts n"
and c'_eq: "c' = Config⇩M S' (λk. (ts k)(n k := aw k))
(λk. go_dir (dir k) (n k))"
and rel: "(S, (λk. ts k (n k)), S', aw, dir)
∈ alphabet_reduce_delta M"
by (auto elim: mttm_step.cases)
have src_S: "fst (snd S) = AR_SimWrite" using src c_eq by simp
have "(S, (λk. ts k (n k)), S', aw, dir) ∈ ar_delta_write M"
using ar_delta_write_from_src[OF rel src_S] .
hence "fst (snd S') = AR_SimWrite ∨ fst (snd S') = AR_SimAdvance"
by (rule ar_delta_write_dest)
thus ?thesis using c'_eq by simp
qed
lemma ar_step_from_SimAdvance_lands:
assumes step: "(c, c') ∈ mttm_step (alphabet_reduce_delta M)"
and src: "fst (snd (mt_state c)) = AR_SimAdvance"
shows "fst (snd (mt_state c')) = AR_SimAdvance
∨ fst (snd (mt_state c')) = AR_SimNext"
proof -
from step obtain S ts n S' aw dir where
c_eq: "c = Config⇩M S ts n"
and c'_eq: "c' = Config⇩M S' (λk. (ts k)(n k := aw k))
(λk. go_dir (dir k) (n k))"
and rel: "(S, (λk. ts k (n k)), S', aw, dir)
∈ alphabet_reduce_delta M"
by (auto elim: mttm_step.cases)
have src_S: "fst (snd S) = AR_SimAdvance" using src c_eq by simp
have "(S, (λk. ts k (n k)), S', aw, dir) ∈ ar_delta_advance M"
using ar_delta_advance_from_src[OF rel src_S] .
hence "fst (snd S') = AR_SimAdvance ∨ fst (snd S') = AR_SimNext"
by (rule ar_delta_advance_dest)
thus ?thesis using c'_eq by simp
qed
lemma ar_step_from_SimNext_lands:
assumes step: "(c, c') ∈ mttm_step (alphabet_reduce_delta M)"
and src: "fst (snd (mt_state c)) = AR_SimNext"
shows "fst (snd (mt_state c')) = AR_SimRead
∨ fst (snd (mt_state c')) = AR_HaltAccept
∨ fst (snd (mt_state c')) = AR_HaltReject"
proof -
from step obtain S ts n S' aw dir where
c_eq: "c = Config⇩M S ts n"
and c'_eq: "c' = Config⇩M S' (λk. (ts k)(n k := aw k))
(λk. go_dir (dir k) (n k))"
and rel: "(S, (λk. ts k (n k)), S', aw, dir)
∈ alphabet_reduce_delta M"
by (auto elim: mttm_step.cases)
have src_S: "fst (snd S) = AR_SimNext" using src c_eq by simp
have "(S, (λk. ts k (n k)), S', aw, dir) ∈ ar_delta_next M"
using ar_delta_next_from_src[OF rel src_S] .
hence "fst (snd S') = AR_SimRead ∨ fst (snd S') = AR_HaltAccept
∨ fst (snd S') = AR_HaltReject"
by (rule ar_delta_next_dest)
thus ?thesis using c'_eq by simp
qed
subsection ‹Walker invariants — per-substep stage predicates›
text ‹The substep-walker is a per-step induction over the
‹M'›-path that tracks where in the cycle we are by reading
the substep idx off each visited configuration's state. Six stage
predicates carry the per-substep relationship between the cycle's
source ‹M›-config ‹cM› and the current
‹M'›-configuration ‹c'›:
▪ ‹ar_walker_at_boundary M cM c'›: fresh cycle start —
‹c'› at ‹AR_SimRead› boundary, the three
forward invariants hold for ‹cM›.
▪ ‹ar_walker_in_read M cM c'›: mid-read-phase —
reachable from a boundary by ‹ar_delta_read›-only
steps, still at ‹AR_SimRead›.
▪ ‹ar_walker_at_compute M cM c'›: read complete —
reachable from a boundary by ‹ar_delta_read›-only
steps, now at ‹AR_SimCompute›. The next M'-step on
the path extracts the M-tuple via
‹ar_compute_step_inv›.
▪ ‹ar_walker_in_write M cM c'›: M-tuple
extracted, mid-write-phase — at ‹AR_SimWrite›.
▪ ‹ar_walker_in_advance M cM c'›: write done,
mid-advance-phase — at ‹AR_SimAdvance›.
▪ ‹ar_walker_at_next M cM c'›: at
‹AR_SimNext›, about to dispatch to next boundary or
halt via ‹ar_next_step_inv›.
The witness-chain formulation (rather than concrete per-state
conditions) makes preservation lemmas mechanical: at a config with
substep tag T, an M'-step fires the unique substep relation with
src tag T (by ‹ar_delta_T_src› + ‹from_src›);
extending the witness chain by one step preserves the invariant.
Chain shape (no cycle-wrap before completing this cycle) follows
from the witness chain living in the *specific* substep relation
‹mttm_step (ar_delta_T M)›, which by
‹ar_delta_T_src› can only fire from sources at T —
ruling out the wrap.›
definition ar_walker_at_boundary ::
"('q, 'a) mttm
⇒ ('a, 'q) mt_config
⇒ (sym4, 'q × 'a ar_stage) mt_config ⇒ bool" where
"ar_walker_at_boundary M cM c' ⟷
ar_simulates M cM c'
∧ ar_posk_consistent M cM c'
∧ ar_at_read_boundary M c'"
definition ar_walker_in_read ::
"('q, 'a) mttm
⇒ ('a, 'q) mt_config
⇒ (sym4, 'q × 'a ar_stage) mt_config ⇒ bool" where
"ar_walker_in_read M cM c' ⟷
fst (snd (mt_state c')) = AR_SimRead
∧ (∃c_b m. ar_walker_at_boundary M cM c_b
∧ (c_b, c') ∈ (mttm_step (ar_delta_read M)) ^^ m)"
definition ar_walker_at_compute ::
"('q, 'a) mttm
⇒ ('a, 'q) mt_config
⇒ (sym4, 'q × 'a ar_stage) mt_config ⇒ bool" where
"ar_walker_at_compute M cM c' ⟷
fst (snd (mt_state c')) = AR_SimCompute
∧ (∃c_b m. ar_walker_at_boundary M cM c_b
∧ (c_b, c') ∈ (mttm_step (ar_delta_read M)) ^^ m)"
definition ar_walker_in_write ::
"('q, 'a) mttm
⇒ ('a, 'q) mt_config
⇒ (sym4, 'q × 'a ar_stage) mt_config ⇒ bool" where
"ar_walker_in_write M cM c' ⟷
fst (snd (mt_state c')) = AR_SimWrite
∧ (∃c_b c_w m_r m_w.
ar_walker_at_boundary M cM c_b
∧ (c_b, c_w) ∈ (mttm_step (ar_delta_read M)) ^^ m_r
∧ fst (snd (mt_state c_w)) = AR_SimCompute
∧ (∃c_w_post. (c_w, c_w_post) ∈ mttm_step (ar_delta_compute M)
∧ (c_w_post, c') ∈ (mttm_step (ar_delta_write M)) ^^ m_w))"
definition ar_walker_in_advance ::
"('q, 'a) mttm
⇒ ('a, 'q) mt_config
⇒ (sym4, 'q × 'a ar_stage) mt_config ⇒ bool" where
"ar_walker_in_advance M cM c' ⟷
fst (snd (mt_state c')) = AR_SimAdvance
∧ (∃c_b c_w c_a m_r m_w m_a.
ar_walker_at_boundary M cM c_b
∧ (c_b, c_w) ∈ (mttm_step (ar_delta_read M)) ^^ m_r
∧ fst (snd (mt_state c_w)) = AR_SimCompute
∧ fst (snd (mt_state c_a)) = AR_SimAdvance
∧ (∃c_w_post. (c_w, c_w_post) ∈ mttm_step (ar_delta_compute M)
∧ (c_w_post, c_a) ∈ (mttm_step (ar_delta_write M)) ^^ m_w
∧ (c_a, c') ∈ (mttm_step (ar_delta_advance M)) ^^ m_a))"
definition ar_walker_at_next ::
"('q, 'a) mttm
⇒ ('a, 'q) mt_config
⇒ (sym4, 'q × 'a ar_stage) mt_config ⇒ bool" where
"ar_walker_at_next M cM c' ⟷
fst (snd (mt_state c')) = AR_SimNext
∧ (∃c_b c_w c_a c_n m_r m_w m_a.
ar_walker_at_boundary M cM c_b
∧ (c_b, c_w) ∈ (mttm_step (ar_delta_read M)) ^^ m_r
∧ fst (snd (mt_state c_w)) = AR_SimCompute
∧ fst (snd (mt_state c_a)) = AR_SimAdvance
∧ (∃c_w_post. (c_w, c_w_post) ∈ mttm_step (ar_delta_compute M)
∧ (c_w_post, c_a) ∈ (mttm_step (ar_delta_write M)) ^^ m_w
∧ (c_a, c_n) ∈ (mttm_step (ar_delta_advance M)) ^^ m_a
∧ c_n = c'))"
subsection ‹Step lifts — ‹mttm_step› to specific substep›
text ‹Five ‹mttm_step›-to-specific-substep lifts: an
‹M'›-step in ‹mttm_step (alphabet_reduce_delta M)›
whose source carries substep tag T is in fact in the smaller
‹mttm_step (ar_delta_T M)›. Each composes
‹mttm_step.cases› (destructure the step), the matching
‹ar_delta_T_from_src› helper (narrow the firing tuple by
src-tag uniqueness), and ‹mttm_step.step› with
‹where ts = ts and n = n› instantiation (break the
higher-order unification ambiguity inherent in
‹mttm_step.step›'s pattern when matched against concrete
tuples). The walker preservation lemmas chain these lifts with
the dest-tag dispatch (lands-at lemmas) to advance the witness
chain by one step.›
lemma ar_step_read_lift:
fixes M :: "('q, 'a) mttm"
and c' c'' :: "(sym4, 'q × 'a ar_stage) mt_config"
assumes src: "fst (snd (mt_state c')) = AR_SimRead"
and step: "(c', c'') ∈ mttm_step (alphabet_reduce_delta M)"
shows "(c', c'') ∈ mttm_step (ar_delta_read M)"
proof -
from step obtain S ts n S' aw dir where
c'_eq: "c' = Config⇩M S ts n"
and c''_eq: "c'' = Config⇩M S' (λk. (ts k)(n k := aw k))
(λk. go_dir (dir k) (n k))"
and rel: "(S, (λk. ts k (n k)), S', aw, dir)
∈ alphabet_reduce_delta M"
by (auto elim: mttm_step.cases)
have src_S: "fst (snd S) = AR_SimRead" using src c'_eq by simp
have rel_T: "(S, (λk. ts k (n k)), S', aw, dir) ∈ ar_delta_read M"
using ar_delta_read_from_src[OF rel src_S] .
have step_aux: "(Config⇩M S ts n,
Config⇩M S' (λk. (ts k)(n k := aw k))
(λk. go_dir (dir k) (n k)))
∈ mttm_step (ar_delta_read M)"
by (rule mttm_step.step[where ts = ts and n = n, OF rel_T])
show ?thesis using step_aux c'_eq c''_eq by simp
qed
lemma ar_step_compute_lift:
fixes M :: "('q, 'a) mttm"
and c' c'' :: "(sym4, 'q × 'a ar_stage) mt_config"
assumes src: "fst (snd (mt_state c')) = AR_SimCompute"
and step: "(c', c'') ∈ mttm_step (alphabet_reduce_delta M)"
shows "(c', c'') ∈ mttm_step (ar_delta_compute M)"
proof -
from step obtain S ts n S' aw dir where
c'_eq: "c' = Config⇩M S ts n"
and c''_eq: "c'' = Config⇩M S' (λk. (ts k)(n k := aw k))
(λk. go_dir (dir k) (n k))"
and rel: "(S, (λk. ts k (n k)), S', aw, dir)
∈ alphabet_reduce_delta M"
by (auto elim: mttm_step.cases)
have src_S: "fst (snd S) = AR_SimCompute" using src c'_eq by simp
have rel_T: "(S, (λk. ts k (n k)), S', aw, dir) ∈ ar_delta_compute M"
using ar_delta_compute_from_src[OF rel src_S] .
have step_aux: "(Config⇩M S ts n,
Config⇩M S' (λk. (ts k)(n k := aw k))
(λk. go_dir (dir k) (n k)))
∈ mttm_step (ar_delta_compute M)"
by (rule mttm_step.step[where ts = ts and n = n, OF rel_T])
show ?thesis using step_aux c'_eq c''_eq by simp
qed
lemma ar_step_write_lift:
fixes M :: "('q, 'a) mttm"
and c' c'' :: "(sym4, 'q × 'a ar_stage) mt_config"
assumes src: "fst (snd (mt_state c')) = AR_SimWrite"
and step: "(c', c'') ∈ mttm_step (alphabet_reduce_delta M)"
shows "(c', c'') ∈ mttm_step (ar_delta_write M)"
proof -
from step obtain S ts n S' aw dir where
c'_eq: "c' = Config⇩M S ts n"
and c''_eq: "c'' = Config⇩M S' (λk. (ts k)(n k := aw k))
(λk. go_dir (dir k) (n k))"
and rel: "(S, (λk. ts k (n k)), S', aw, dir)
∈ alphabet_reduce_delta M"
by (auto elim: mttm_step.cases)
have src_S: "fst (snd S) = AR_SimWrite" using src c'_eq by simp
have rel_T: "(S, (λk. ts k (n k)), S', aw, dir) ∈ ar_delta_write M"
using ar_delta_write_from_src[OF rel src_S] .
have step_aux: "(Config⇩M S ts n,
Config⇩M S' (λk. (ts k)(n k := aw k))
(λk. go_dir (dir k) (n k)))
∈ mttm_step (ar_delta_write M)"
by (rule mttm_step.step[where ts = ts and n = n, OF rel_T])
show ?thesis using step_aux c'_eq c''_eq by simp
qed
lemma ar_step_advance_lift:
fixes M :: "('q, 'a) mttm"
and c' c'' :: "(sym4, 'q × 'a ar_stage) mt_config"
assumes src: "fst (snd (mt_state c')) = AR_SimAdvance"
and step: "(c', c'') ∈ mttm_step (alphabet_reduce_delta M)"
shows "(c', c'') ∈ mttm_step (ar_delta_advance M)"
proof -
from step obtain S ts n S' aw dir where
c'_eq: "c' = Config⇩M S ts n"
and c''_eq: "c'' = Config⇩M S' (λk. (ts k)(n k := aw k))
(λk. go_dir (dir k) (n k))"
and rel: "(S, (λk. ts k (n k)), S', aw, dir)
∈ alphabet_reduce_delta M"
by (auto elim: mttm_step.cases)
have src_S: "fst (snd S) = AR_SimAdvance" using src c'_eq by simp
have rel_T: "(S, (λk. ts k (n k)), S', aw, dir) ∈ ar_delta_advance M"
using ar_delta_advance_from_src[OF rel src_S] .
have step_aux: "(Config⇩M S ts n,
Config⇩M S' (λk. (ts k)(n k := aw k))
(λk. go_dir (dir k) (n k)))
∈ mttm_step (ar_delta_advance M)"
by (rule mttm_step.step[where ts = ts and n = n, OF rel_T])
show ?thesis using step_aux c'_eq c''_eq by simp
qed
text ‹Existence-lift wrappers around the ‹ar_step_X_lift›
lemmas for the three generic substeps (read, write, advance):
convert an existential conclusion
‹∃c''. (c', c'') ∈ mttm_step (alphabet_reduce_delta M)
∧ P c''› into the same existential with the step in
‹mttm_step (ar_delta_X M)›, given the source tag of ‹c'›.
These collapse the leaf-in-sub boilerplate (the
‹obtain … using ar_step_X_lift[OF src …] …
show ?thesis using … by blast›
scaffold) into a single application. The other two substeps carry
no wrapper: compute is the nondeterministic branch and next closes
the cycle, so both are handled by the cycle-close's
reconstruct-and-reuse machinery rather than a generic lift.›
lemma ar_exists_step_in_sub_read:
fixes M :: "('q, 'a) mttm"
and c' :: "(sym4, 'q × 'a ar_stage) mt_config"
and P :: "(sym4, 'q × 'a ar_stage) mt_config ⇒ bool"
assumes orig: "∃c''. (c', c'') ∈ mttm_step (alphabet_reduce_delta M)
∧ P c''"
and src: "fst (snd (mt_state c')) = AR_SimRead"
shows "∃c''. (c', c'') ∈ mttm_step (ar_delta_read M) ∧ P c''"
proof -
obtain c'' where step: "(c', c'') ∈ mttm_step (alphabet_reduce_delta M)"
and pc: "P c''"
using orig by blast
have step_sub: "(c', c'') ∈ mttm_step (ar_delta_read M)"
using ar_step_read_lift[OF src step] .
show ?thesis using step_sub pc by blast
qed
lemma ar_exists_step_in_sub_write:
fixes M :: "('q, 'a) mttm"
and c' :: "(sym4, 'q × 'a ar_stage) mt_config"
and P :: "(sym4, 'q × 'a ar_stage) mt_config ⇒ bool"
assumes orig: "∃c''. (c', c'') ∈ mttm_step (alphabet_reduce_delta M)
∧ P c''"
and src: "fst (snd (mt_state c')) = AR_SimWrite"
shows "∃c''. (c', c'') ∈ mttm_step (ar_delta_write M) ∧ P c''"
proof -
obtain c'' where step: "(c', c'') ∈ mttm_step (alphabet_reduce_delta M)"
and pc: "P c''"
using orig by blast
have step_sub: "(c', c'') ∈ mttm_step (ar_delta_write M)"
using ar_step_write_lift[OF src step] .
show ?thesis using step_sub pc by blast
qed
lemma ar_exists_step_in_sub_advance:
fixes M :: "('q, 'a) mttm"
and c' :: "(sym4, 'q × 'a ar_stage) mt_config"
and P :: "(sym4, 'q × 'a ar_stage) mt_config ⇒ bool"
assumes orig: "∃c''. (c', c'') ∈ mttm_step (alphabet_reduce_delta M)
∧ P c''"
and src: "fst (snd (mt_state c')) = AR_SimAdvance"
shows "∃c''. (c', c'') ∈ mttm_step (ar_delta_advance M) ∧ P c''"
proof -
obtain c'' where step: "(c', c'') ∈ mttm_step (alphabet_reduce_delta M)"
and pc: "P c''"
using orig by blast
have step_sub: "(c', c'') ∈ mttm_step (ar_delta_advance M)"
using ar_step_advance_lift[OF src step] .
show ?thesis using step_sub pc by blast
qed
subsection ‹Chain pinning in ‹mttm_step (ar_delta_read M)››
text ‹Two structural facts about chains in the read sub-relation:
the sub-relation is *functional* (lifted from
‹ar_delta_read_func› via ‹mttm_step›'s shape), so its
‹m›-step extension of any seed is unique; and it cannot fire
from a source whose substep tag is ‹AR_SimCompute› (by
‹ar_delta_read_src›). Together these pin a chain ending at
‹AR_SimCompute› uniquely on both its length and its endpoint:
if two chains in the sub-relation start at the same seed and both
end at an ‹AR_SimCompute›-tagged config, they coincide. This
is what bridges the walker's by-construction ‹R_read› witness
chain to the existence chain produced by the (re-mirrored)
‹ar_read_phase_in_sub›: the witness chain inherits the latter's
stated endpoint state shape, including the load-bearing
‹buf = λk. mt_tape cM k (mt_pos cM k)›.›
lemma mttm_step_ar_delta_read_func:
fixes M :: "('q, 'a) mttm"
and c c⇩1 c⇩2 :: "(sym4, 'q × 'a ar_stage) mt_config"
assumes h⇩1: "(c, c⇩1) ∈ mttm_step (ar_delta_read M)"
and h⇩2: "(c, c⇩2) ∈ mttm_step (ar_delta_read M)"
shows "c⇩1 = c⇩2"
proof -
from h⇩1 obtain S ts n S⇩1 aw⇩1 dir⇩1 where
ceq⇩1: "c = Config⇩M S ts n"
and c⇩1eq: "c⇩1 = Config⇩M S⇩1 (λk. (ts k)(n k := aw⇩1 k))
(λk. go_dir (dir⇩1 k) (n k))"
and rel⇩1: "(S, (λk. ts k (n k)), S⇩1, aw⇩1, dir⇩1) ∈ ar_delta_read M"
by (auto elim: mttm_step.cases)
from h⇩2 obtain S' ts' n' S⇩2 aw⇩2 dir⇩2 where
ceq⇩2: "c = Config⇩M S' ts' n'"
and c⇩2eq: "c⇩2 = Config⇩M S⇩2 (λk. (ts' k)(n' k := aw⇩2 k))
(λk. go_dir (dir⇩2 k) (n' k))"
and rel⇩2: "(S', (λk. ts' k (n' k)), S⇩2, aw⇩2, dir⇩2) ∈ ar_delta_read M"
by (auto elim: mttm_step.cases)
have eq: "S = S' ∧ ts = ts' ∧ n = n'" using ceq⇩1 ceq⇩2 by simp
have rel⇩2': "(S, (λk. ts k (n k)), S⇩2, aw⇩2, dir⇩2) ∈ ar_delta_read M"
using rel⇩2 eq by simp
have "(S⇩1, aw⇩1, dir⇩1) = (S⇩2, aw⇩2, dir⇩2)"
using ar_delta_read_func[OF rel⇩1 rel⇩2'] .
hence "S⇩1 = S⇩2 ∧ aw⇩1 = aw⇩2 ∧ dir⇩1 = dir⇩2" by simp
thus ?thesis using c⇩1eq c⇩2eq eq by simp
qed
lemma chain_ar_delta_read_func:
fixes M :: "('q, 'a) mttm"
shows "(c, c⇩1) ∈ (mttm_step (ar_delta_read M)) ^^ m
⟹ (c, c⇩2) ∈ (mttm_step (ar_delta_read M)) ^^ m
⟹ c⇩1 = c⇩2"
proof (induction m arbitrary: c⇩1 c⇩2)
case 0
thus ?case by auto
next
case (Suc m)
obtain c⇩1' where
a: "(c, c⇩1') ∈ (mttm_step (ar_delta_read M)) ^^ m"
and b: "(c⇩1', c⇩1) ∈ mttm_step (ar_delta_read M)"
using Suc(2) by (auto elim: relpow_Suc_E)
obtain c⇩2' where
c: "(c, c⇩2') ∈ (mttm_step (ar_delta_read M)) ^^ m"
and d: "(c⇩2', c⇩2) ∈ mttm_step (ar_delta_read M)"
using Suc(3) by (auto elim: relpow_Suc_E)
have "c⇩1' = c⇩2'" using Suc(1)[OF a c] .
thus ?case using b d mttm_step_ar_delta_read_func by simp
qed
lemma ar_delta_read_no_step_from_SimCompute:
fixes M :: "('q, 'a) mttm"
and c c' :: "(sym4, 'q × 'a ar_stage) mt_config"
assumes "fst (snd (mt_state c)) = AR_SimCompute"
shows "(c, c') ∉ mttm_step (ar_delta_read M)"
proof
assume h: "(c, c') ∈ mttm_step (ar_delta_read M)"
from h obtain S ts n S' aw dir where
ceq: "c = Config⇩M S ts n"
and rel: "(S, (λk. ts k (n k)), S', aw, dir) ∈ ar_delta_read M"
by (auto elim: mttm_step.cases)
have "fst (snd S) = AR_SimRead" using ar_delta_read_src[OF rel] .
hence "fst (snd (mt_state c)) = AR_SimRead" using ceq by simp
with assms show False by simp
qed
lemma chain_ar_delta_read_to_SimCompute_uniq:
fixes M :: "('q, 'a) mttm"
and c c⇩1 c⇩2 :: "(sym4, 'q × 'a ar_stage) mt_config"
assumes h⇩1: "(c, c⇩1) ∈ (mttm_step (ar_delta_read M)) ^^ m"
and h⇩2: "(c, c⇩2) ∈ (mttm_step (ar_delta_read M)) ^^ n"
and c⇩1cpu: "fst (snd (mt_state c⇩1)) = AR_SimCompute"
and c⇩2cpu: "fst (snd (mt_state c⇩2)) = AR_SimCompute"
shows "m = n ∧ c⇩1 = c⇩2"
proof -
have aux:
"⋀m n c⇩1 c⇩2. (c, c⇩1) ∈ (mttm_step (ar_delta_read M)) ^^ m
⟹ (c, c⇩2) ∈ (mttm_step (ar_delta_read M)) ^^ n
⟹ fst (snd (mt_state c⇩1)) = AR_SimCompute
⟹ m ≤ n
⟹ m = n"
proof -
fix m n c⇩1 c⇩2
assume a⇩1: "(c, c⇩1) ∈ (mttm_step (ar_delta_read M)) ^^ m"
and a⇩2: "(c, c⇩2) ∈ (mttm_step (ar_delta_read M)) ^^ n"
and acpu: "fst (snd (mt_state c⇩1)) = AR_SimCompute"
and ale: "m ≤ n"
obtain dm where ndecomp: "n = m + dm" using ale le_Suc_ex by blast
have "(c, c⇩2) ∈ ((mttm_step (ar_delta_read M)) ^^ m)
O ((mttm_step (ar_delta_read M)) ^^ dm)"
using a⇩2 ndecomp by (simp add: relpow_add)
then obtain c⇩m where
am: "(c, c⇩m) ∈ (mttm_step (ar_delta_read M)) ^^ m"
and adm: "(c⇩m, c⇩2) ∈ (mttm_step (ar_delta_read M)) ^^ dm"
by auto
have cm_eq: "c⇩m = c⇩1" using chain_ar_delta_read_func[OF am a⇩1] .
show "m = n"
proof (rule ccontr)
assume "m ≠ n"
hence dm_pos: "0 < dm" using ndecomp by simp
then obtain dm' where dm_eq: "dm = Suc dm'" using gr0_implies_Suc by blast
have hsuc: "(c⇩1, c⇩2) ∈ (mttm_step (ar_delta_read M)) ^^ (Suc dm')"
using adm cm_eq dm_eq by simp
obtain c_next where
first: "(c⇩1, c_next) ∈ mttm_step (ar_delta_read M)"
using relpow_Suc_D2[OF hsuc] by blast
have "(c⇩1, c_next) ∉ mttm_step (ar_delta_read M)"
using acpu by (rule ar_delta_read_no_step_from_SimCompute)
thus False using first by simp
qed
qed
have mn_eq: "m = n"
proof (cases "m ≤ n")
case True
show ?thesis using aux[OF h⇩1 h⇩2 c⇩1cpu True] .
next
case False
hence nle: "n ≤ m" by simp
show ?thesis using aux[OF h⇩2 h⇩1 c⇩2cpu nle] by simp
qed
have "c⇩1 = c⇩2"
using chain_ar_delta_read_func[OF h⇩1 h⇩2[unfolded mn_eq[symmetric]]] .
thus ?thesis using mn_eq by simp
qed
text ‹Two parallel chain-pinning suites for the write and advance
sub-relations, mirroring the read suite verbatim with
‹ar_delta_write› / ‹ar_delta_advance› in place of
‹ar_delta_read› and ‹AR_SimAdvance› / ‹AR_SimNext›
in place of ‹AR_SimCompute›. Functional projections
(‹ar_delta_write_func›, ‹ar_delta_advance_func›) and src
uniqueness (‹ar_delta_write_src›, ‹ar_delta_advance_src›)
feed the same scaffold. These suites are used by the cycle-close
bridging lemma to pin walker write/advance chains against the
forward ‹ar_write_phase› / ‹ar_advance_phase›
constructions.›
lemma mttm_step_ar_delta_write_func:
fixes M :: "('q, 'a) mttm"
and c c⇩1 c⇩2 :: "(sym4, 'q × 'a ar_stage) mt_config"
assumes h⇩1: "(c, c⇩1) ∈ mttm_step (ar_delta_write M)"
and h⇩2: "(c, c⇩2) ∈ mttm_step (ar_delta_write M)"
shows "c⇩1 = c⇩2"
proof -
from h⇩1 obtain S ts n S⇩1 aw⇩1 dir⇩1 where
ceq⇩1: "c = Config⇩M S ts n"
and c⇩1eq: "c⇩1 = Config⇩M S⇩1 (λk. (ts k)(n k := aw⇩1 k))
(λk. go_dir (dir⇩1 k) (n k))"
and rel⇩1: "(S, (λk. ts k (n k)), S⇩1, aw⇩1, dir⇩1) ∈ ar_delta_write M"
by (auto elim: mttm_step.cases)
from h⇩2 obtain S' ts' n' S⇩2 aw⇩2 dir⇩2 where
ceq⇩2: "c = Config⇩M S' ts' n'"
and c⇩2eq: "c⇩2 = Config⇩M S⇩2 (λk. (ts' k)(n' k := aw⇩2 k))
(λk. go_dir (dir⇩2 k) (n' k))"
and rel⇩2: "(S', (λk. ts' k (n' k)), S⇩2, aw⇩2, dir⇩2) ∈ ar_delta_write M"
by (auto elim: mttm_step.cases)
have eq: "S = S' ∧ ts = ts' ∧ n = n'" using ceq⇩1 ceq⇩2 by simp
have rel⇩2': "(S, (λk. ts k (n k)), S⇩2, aw⇩2, dir⇩2) ∈ ar_delta_write M"
using rel⇩2 eq by simp
have "(S⇩1, aw⇩1, dir⇩1) = (S⇩2, aw⇩2, dir⇩2)"
using ar_delta_write_func[OF rel⇩1 rel⇩2'] .
hence "S⇩1 = S⇩2 ∧ aw⇩1 = aw⇩2 ∧ dir⇩1 = dir⇩2" by simp
thus ?thesis using c⇩1eq c⇩2eq eq by simp
qed
lemma chain_ar_delta_write_func:
fixes M :: "('q, 'a) mttm"
shows "(c, c⇩1) ∈ (mttm_step (ar_delta_write M)) ^^ m
⟹ (c, c⇩2) ∈ (mttm_step (ar_delta_write M)) ^^ m
⟹ c⇩1 = c⇩2"
proof (induction m arbitrary: c⇩1 c⇩2)
case 0
thus ?case by auto
next
case (Suc m)
obtain c⇩1' where
a: "(c, c⇩1') ∈ (mttm_step (ar_delta_write M)) ^^ m"
and b: "(c⇩1', c⇩1) ∈ mttm_step (ar_delta_write M)"
using Suc(2) by (auto elim: relpow_Suc_E)
obtain c⇩2' where
c: "(c, c⇩2') ∈ (mttm_step (ar_delta_write M)) ^^ m"
and d: "(c⇩2', c⇩2) ∈ mttm_step (ar_delta_write M)"
using Suc(3) by (auto elim: relpow_Suc_E)
have "c⇩1' = c⇩2'" using Suc(1)[OF a c] .
thus ?case using b d mttm_step_ar_delta_write_func by simp
qed
lemma ar_delta_write_no_step_from_SimAdvance:
fixes M :: "('q, 'a) mttm"
and c c' :: "(sym4, 'q × 'a ar_stage) mt_config"
assumes "fst (snd (mt_state c)) = AR_SimAdvance"
shows "(c, c') ∉ mttm_step (ar_delta_write M)"
proof
assume h: "(c, c') ∈ mttm_step (ar_delta_write M)"
from h obtain S ts n S' aw dir where
ceq: "c = Config⇩M S ts n"
and rel: "(S, (λk. ts k (n k)), S', aw, dir) ∈ ar_delta_write M"
by (auto elim: mttm_step.cases)
have "fst (snd S) = AR_SimWrite" using ar_delta_write_src[OF rel] .
hence "fst (snd (mt_state c)) = AR_SimWrite" using ceq by simp
with assms show False by simp
qed
lemma chain_ar_delta_write_to_SimAdvance_uniq:
fixes M :: "('q, 'a) mttm"
and c c⇩1 c⇩2 :: "(sym4, 'q × 'a ar_stage) mt_config"
assumes h⇩1: "(c, c⇩1) ∈ (mttm_step (ar_delta_write M)) ^^ m"
and h⇩2: "(c, c⇩2) ∈ (mttm_step (ar_delta_write M)) ^^ n"
and c⇩1adv: "fst (snd (mt_state c⇩1)) = AR_SimAdvance"
and c⇩2adv: "fst (snd (mt_state c⇩2)) = AR_SimAdvance"
shows "m = n ∧ c⇩1 = c⇩2"
proof -
have aux:
"⋀m n c⇩1 c⇩2. (c, c⇩1) ∈ (mttm_step (ar_delta_write M)) ^^ m
⟹ (c, c⇩2) ∈ (mttm_step (ar_delta_write M)) ^^ n
⟹ fst (snd (mt_state c⇩1)) = AR_SimAdvance
⟹ m ≤ n
⟹ m = n"
proof -
fix m n c⇩1 c⇩2
assume a⇩1: "(c, c⇩1) ∈ (mttm_step (ar_delta_write M)) ^^ m"
and a⇩2: "(c, c⇩2) ∈ (mttm_step (ar_delta_write M)) ^^ n"
and aadv: "fst (snd (mt_state c⇩1)) = AR_SimAdvance"
and ale: "m ≤ n"
obtain dm where ndecomp: "n = m + dm" using ale le_Suc_ex by blast
have "(c, c⇩2) ∈ ((mttm_step (ar_delta_write M)) ^^ m)
O ((mttm_step (ar_delta_write M)) ^^ dm)"
using a⇩2 ndecomp by (simp add: relpow_add)
then obtain c⇩m where
am: "(c, c⇩m) ∈ (mttm_step (ar_delta_write M)) ^^ m"
and adm: "(c⇩m, c⇩2) ∈ (mttm_step (ar_delta_write M)) ^^ dm"
by auto
have cm_eq: "c⇩m = c⇩1" using chain_ar_delta_write_func[OF am a⇩1] .
show "m = n"
proof (rule ccontr)
assume "m ≠ n"
hence dm_pos: "0 < dm" using ndecomp by simp
then obtain dm' where dm_eq: "dm = Suc dm'" using gr0_implies_Suc by blast
have hsuc: "(c⇩1, c⇩2) ∈ (mttm_step (ar_delta_write M)) ^^ (Suc dm')"
using adm cm_eq dm_eq by simp
obtain c_next where
first: "(c⇩1, c_next) ∈ mttm_step (ar_delta_write M)"
using relpow_Suc_D2[OF hsuc] by blast
have "(c⇩1, c_next) ∉ mttm_step (ar_delta_write M)"
using aadv by (rule ar_delta_write_no_step_from_SimAdvance)
thus False using first by simp
qed
qed
have mn_eq: "m = n"
proof (cases "m ≤ n")
case True
show ?thesis using aux[OF h⇩1 h⇩2 c⇩1adv True] .
next
case False
hence nle: "n ≤ m" by simp
show ?thesis using aux[OF h⇩2 h⇩1 c⇩2adv nle] by simp
qed
have "c⇩1 = c⇩2"
using chain_ar_delta_write_func[OF h⇩1 h⇩2[unfolded mn_eq[symmetric]]] .
thus ?thesis using mn_eq by simp
qed
lemma mttm_step_ar_delta_advance_func:
fixes M :: "('q, 'a) mttm"
and c c⇩1 c⇩2 :: "(sym4, 'q × 'a ar_stage) mt_config"
assumes h⇩1: "(c, c⇩1) ∈ mttm_step (ar_delta_advance M)"
and h⇩2: "(c, c⇩2) ∈ mttm_step (ar_delta_advance M)"
shows "c⇩1 = c⇩2"
proof -
from h⇩1 obtain S ts n S⇩1 aw⇩1 dir⇩1 where
ceq⇩1: "c = Config⇩M S ts n"
and c⇩1eq: "c⇩1 = Config⇩M S⇩1 (λk. (ts k)(n k := aw⇩1 k))
(λk. go_dir (dir⇩1 k) (n k))"
and rel⇩1: "(S, (λk. ts k (n k)), S⇩1, aw⇩1, dir⇩1) ∈ ar_delta_advance M"
by (auto elim: mttm_step.cases)
from h⇩2 obtain S' ts' n' S⇩2 aw⇩2 dir⇩2 where
ceq⇩2: "c = Config⇩M S' ts' n'"
and c⇩2eq: "c⇩2 = Config⇩M S⇩2 (λk. (ts' k)(n' k := aw⇩2 k))
(λk. go_dir (dir⇩2 k) (n' k))"
and rel⇩2: "(S', (λk. ts' k (n' k)), S⇩2, aw⇩2, dir⇩2) ∈ ar_delta_advance M"
by (auto elim: mttm_step.cases)
have eq: "S = S' ∧ ts = ts' ∧ n = n'" using ceq⇩1 ceq⇩2 by simp
have rel⇩2': "(S, (λk. ts k (n k)), S⇩2, aw⇩2, dir⇩2) ∈ ar_delta_advance M"
using rel⇩2 eq by simp
have "(S⇩1, aw⇩1, dir⇩1) = (S⇩2, aw⇩2, dir⇩2)"
using ar_delta_advance_func[OF rel⇩1 rel⇩2'] .
hence "S⇩1 = S⇩2 ∧ aw⇩1 = aw⇩2 ∧ dir⇩1 = dir⇩2" by simp
thus ?thesis using c⇩1eq c⇩2eq eq by simp
qed
lemma chain_ar_delta_advance_func:
fixes M :: "('q, 'a) mttm"
shows "(c, c⇩1) ∈ (mttm_step (ar_delta_advance M)) ^^ m
⟹ (c, c⇩2) ∈ (mttm_step (ar_delta_advance M)) ^^ m
⟹ c⇩1 = c⇩2"
proof (induction m arbitrary: c⇩1 c⇩2)
case 0
thus ?case by auto
next
case (Suc m)
obtain c⇩1' where
a: "(c, c⇩1') ∈ (mttm_step (ar_delta_advance M)) ^^ m"
and b: "(c⇩1', c⇩1) ∈ mttm_step (ar_delta_advance M)"
using Suc(2) by (auto elim: relpow_Suc_E)
obtain c⇩2' where
c: "(c, c⇩2') ∈ (mttm_step (ar_delta_advance M)) ^^ m"
and d: "(c⇩2', c⇩2) ∈ mttm_step (ar_delta_advance M)"
using Suc(3) by (auto elim: relpow_Suc_E)
have "c⇩1' = c⇩2'" using Suc(1)[OF a c] .
thus ?case using b d mttm_step_ar_delta_advance_func by simp
qed
lemma ar_delta_advance_no_step_from_SimNext:
fixes M :: "('q, 'a) mttm"
and c c' :: "(sym4, 'q × 'a ar_stage) mt_config"
assumes "fst (snd (mt_state c)) = AR_SimNext"
shows "(c, c') ∉ mttm_step (ar_delta_advance M)"
proof
assume h: "(c, c') ∈ mttm_step (ar_delta_advance M)"
from h obtain S ts n S' aw dir where
ceq: "c = Config⇩M S ts n"
and rel: "(S, (λk. ts k (n k)), S', aw, dir) ∈ ar_delta_advance M"
by (auto elim: mttm_step.cases)
have "fst (snd S) = AR_SimAdvance" using ar_delta_advance_src[OF rel] .
hence "fst (snd (mt_state c)) = AR_SimAdvance" using ceq by simp
with assms show False by simp
qed
lemma chain_ar_delta_advance_to_SimNext_uniq:
fixes M :: "('q, 'a) mttm"
and c c⇩1 c⇩2 :: "(sym4, 'q × 'a ar_stage) mt_config"
assumes h⇩1: "(c, c⇩1) ∈ (mttm_step (ar_delta_advance M)) ^^ m"
and h⇩2: "(c, c⇩2) ∈ (mttm_step (ar_delta_advance M)) ^^ n"
and c⇩1nxt: "fst (snd (mt_state c⇩1)) = AR_SimNext"
and c⇩2nxt: "fst (snd (mt_state c⇩2)) = AR_SimNext"
shows "m = n ∧ c⇩1 = c⇩2"
proof -
have aux:
"⋀m n c⇩1 c⇩2. (c, c⇩1) ∈ (mttm_step (ar_delta_advance M)) ^^ m
⟹ (c, c⇩2) ∈ (mttm_step (ar_delta_advance M)) ^^ n
⟹ fst (snd (mt_state c⇩1)) = AR_SimNext
⟹ m ≤ n
⟹ m = n"
proof -
fix m n c⇩1 c⇩2
assume a⇩1: "(c, c⇩1) ∈ (mttm_step (ar_delta_advance M)) ^^ m"
and a⇩2: "(c, c⇩2) ∈ (mttm_step (ar_delta_advance M)) ^^ n"
and anxt: "fst (snd (mt_state c⇩1)) = AR_SimNext"
and ale: "m ≤ n"
obtain dm where ndecomp: "n = m + dm" using ale le_Suc_ex by blast
have "(c, c⇩2) ∈ ((mttm_step (ar_delta_advance M)) ^^ m)
O ((mttm_step (ar_delta_advance M)) ^^ dm)"
using a⇩2 ndecomp by (simp add: relpow_add)
then obtain c⇩m where
am: "(c, c⇩m) ∈ (mttm_step (ar_delta_advance M)) ^^ m"
and adm: "(c⇩m, c⇩2) ∈ (mttm_step (ar_delta_advance M)) ^^ dm"
by auto
have cm_eq: "c⇩m = c⇩1" using chain_ar_delta_advance_func[OF am a⇩1] .
show "m = n"
proof (rule ccontr)
assume "m ≠ n"
hence dm_pos: "0 < dm" using ndecomp by simp
then obtain dm' where dm_eq: "dm = Suc dm'" using gr0_implies_Suc by blast
have hsuc: "(c⇩1, c⇩2) ∈ (mttm_step (ar_delta_advance M)) ^^ (Suc dm')"
using adm cm_eq dm_eq by simp
obtain c_next where
first: "(c⇩1, c_next) ∈ mttm_step (ar_delta_advance M)"
using relpow_Suc_D2[OF hsuc] by blast
have "(c⇩1, c_next) ∉ mttm_step (ar_delta_advance M)"
using anxt by (rule ar_delta_advance_no_step_from_SimNext)
thus False using first by simp
qed
qed
have mn_eq: "m = n"
proof (cases "m ≤ n")
case True
show ?thesis using aux[OF h⇩1 h⇩2 c⇩1nxt True] .
next
case False
hence nle: "n ≤ m" by simp
show ?thesis using aux[OF h⇩2 h⇩1 c⇩2nxt nle] by simp
qed
have "c⇩1 = c⇩2"
using chain_ar_delta_advance_func[OF h⇩1 h⇩2[unfolded mn_eq[symmetric]]] .
thus ?thesis using mn_eq by simp
qed
subsection ‹Read-phase leaves, sub-relation chain variants›
text ‹For each single-step read-phase leaf
(‹ar_read_le_step›, ‹ar_read_le_finish_step›,
‹ar_read_lookback1_step›, ‹ar_read_lookback2_step›,
‹ar_read_bit_step›, ‹ar_read_bit_boundary_step›,
‹ar_read_bit_finish_step›), a companion lemma producing the
step in ‹mttm_step (ar_delta_read M)› instead of
‹mttm_step (alphabet_reduce_delta M)›. Each variant uses the
existing lemma to obtain the step, then lifts via
‹ar_step_read_lift› (the source tag is ‹AR_SimRead› by
the leaf's ‹stg› hypothesis). No re-derivation of the step's
effect — the existing leaf's stated post-state, post-tape, post-pos
conclusions flow through verbatim.›
lemma ar_read_le_step_in_sub:
fixes M :: "('q, 'a) mttm"
and c' :: "(sym4, 'q × 'a ar_stage) mt_config"
assumes vM: "valid_mttm M"
and stg: "mt_state c' = (q, AR_SimRead, tk, 0, buf, dvec, posk)"
and qQ: "q ∈ Q_tm M"
and notlast: "¬ is_last_k M tk"
and posk_le: "posk tk = AR_AtLE"
and aLE: "mt_tape c' tk (mt_pos c' tk) = LE4"
and vsrc: "ar_valid_stage (Γ_tm M) (bl_tm M)
(AR_SimRead, tk, 0, buf, dvec, posk)"
and pad_blank: "∀j ≥ k_tm M. mt_tape c' j (mt_pos c' j) = BLANK4"
and src_bounded: "ar_stage_bounded (bl_tm M) (k_tm M)
(AR_SimRead, tk, 0, buf, dvec, posk)"
shows "∃c''. (c', c'') ∈ mttm_step (ar_delta_read M)
∧ mt_state c'' = (q, AR_SimRead, k_succ tk, 0,
buf(tk := le_tm M), dvec, posk)
∧ mt_tape c'' = mt_tape c'
∧ mt_pos c'' = (mt_pos c')(tk := Suc (mt_pos c' tk))"
proof -
have src: "fst (snd (mt_state c')) = AR_SimRead" using stg by simp
show ?thesis
using ar_exists_step_in_sub_read
[OF ar_read_le_step[OF vM stg qQ notlast posk_le aLE vsrc pad_blank src_bounded] src] .
qed
lemma ar_read_le_finish_step_in_sub:
fixes M :: "('q, 'a) mttm"
and c' :: "(sym4, 'q × 'a ar_stage) mt_config"
assumes vM: "valid_mttm M"
and stg: "mt_state c' = (q, AR_SimRead, tk, 0, buf, dvec, posk)"
and qQ: "q ∈ Q_tm M"
and last: "is_last_k M tk"
and posk_le: "posk tk = AR_AtLE"
and aLE: "mt_tape c' tk (mt_pos c' tk) = LE4"
and vsrc: "ar_valid_stage (Γ_tm M) (bl_tm M)
(AR_SimRead, tk, 0, buf, dvec, posk)"
and pad_blank: "∀j ≥ k_tm M. mt_tape c' j (mt_pos c' j) = BLANK4"
and src_bounded: "ar_stage_bounded (bl_tm M) (k_tm M)
(AR_SimRead, tk, 0, buf, dvec, posk)"
shows "∃c''. (c', c'') ∈ mttm_step (ar_delta_read M)
∧ mt_state c'' = (q, AR_SimCompute, k_unidx 0, 0,
buf(tk := le_tm M), dvec, posk)
∧ mt_tape c'' = mt_tape c'
∧ mt_pos c'' = (mt_pos c')(tk := Suc (mt_pos c' tk))"
proof -
have src: "fst (snd (mt_state c')) = AR_SimRead" using stg by simp
show ?thesis
using ar_exists_step_in_sub_read
[OF ar_read_le_finish_step[OF vM stg qQ last posk_le aLE vsrc pad_blank src_bounded] src] .
qed
lemma ar_read_lookback1_step_in_sub:
fixes M :: "('q, 'a) mttm"
and c' :: "(sym4, 'q × 'a ar_stage) mt_config"
assumes vM: "valid_mttm M"
and stg: "mt_state c' = (q, AR_SimRead, tk, 0, buf, dvec, posk)"
and qQ: "q ∈ Q_tm M"
and posk_proper: "posk tk ∈ {AR_AtFirstProper, AR_AtFurtherProper}"
and notLE: "mt_tape c' tk (mt_pos c' tk) ≠ LE4"
and vsrc: "ar_valid_stage (Γ_tm M) (bl_tm M)
(AR_SimRead, tk, 0, buf, dvec, posk)"
and pad_blank: "∀j ≥ k_tm M. mt_tape c' j (mt_pos c' j) = BLANK4"
and src_bounded: "ar_stage_bounded (bl_tm M) (k_tm M)
(AR_SimRead, tk, 0, buf, dvec, posk)"
shows "∃c''. (c', c'') ∈ mttm_step (ar_delta_read M)
∧ mt_state c'' = (q, AR_SimRead, tk, Suc 0, buf, dvec, posk)
∧ mt_tape c'' = mt_tape c'
∧ mt_pos c'' = (mt_pos c')(tk := mt_pos c' tk - 1)"
proof -
have src: "fst (snd (mt_state c')) = AR_SimRead" using stg by simp
show ?thesis
using ar_exists_step_in_sub_read
[OF ar_read_lookback1_step[OF vM stg qQ posk_proper notLE vsrc pad_blank src_bounded] src] .
qed
lemma ar_read_lookback2_step_in_sub:
fixes M :: "('q, 'a) mttm"
and c' :: "(sym4, 'q × 'a ar_stage) mt_config"
assumes vM: "valid_mttm M"
and stg: "mt_state c' = (q, AR_SimRead, tk, Suc 0, buf, dvec, posk)"
and qQ: "q ∈ Q_tm M"
and posk_proper: "posk tk ∈ {AR_AtFirstProper, AR_AtFurtherProper}"
and kge2: "2 ≤ block_width (Γ_tm M)"
and vsrc: "ar_valid_stage (Γ_tm M) (bl_tm M)
(AR_SimRead, tk, Suc 0, buf, dvec, posk)"
and pad_blank: "∀j ≥ k_tm M. mt_tape c' j (mt_pos c' j) = BLANK4"
and src_bounded: "ar_stage_bounded (bl_tm M) (k_tm M)
(AR_SimRead, tk, Suc 0, buf, dvec, posk)"
shows "∃c''. (c', c'') ∈ mttm_step (ar_delta_read M)
∧ mt_state c'' = (q, AR_SimRead, tk, Suc (Suc 0),
buf(tk := gamma_unenum (Γ_tm M) (bl_tm M) 0), dvec,
posk(tk := if mt_tape c' tk (mt_pos c' tk) = LE4
then AR_AtFirstProper else AR_AtFurtherProper))
∧ mt_tape c'' = mt_tape c'
∧ mt_pos c'' = (mt_pos c')(tk := Suc (mt_pos c' tk))"
proof -
have src: "fst (snd (mt_state c')) = AR_SimRead" using stg by simp
show ?thesis
using ar_exists_step_in_sub_read
[OF ar_read_lookback2_step[OF vM stg qQ posk_proper kge2 vsrc pad_blank src_bounded] src] .
qed
lemma ar_read_bit_step_in_sub:
fixes M :: "('q, 'a) mttm"
and c' :: "(sym4, 'q × 'a ar_stage) mt_config"
assumes vM: "valid_mttm M"
and stg: "mt_state c' = (q, AR_SimRead, tk, i, buf, dvec, posk)"
and qQ: "q ∈ Q_tm M"
and posk_proper: "posk tk ∈ {AR_AtFirstProper, AR_AtFurtherProper}"
and ilo: "2 ≤ i"
and ihi: "Suc i ≤ Suc (block_width (Γ_tm M))"
and kge2: "2 ≤ block_width (Γ_tm M)"
and vsrc: "ar_valid_stage (Γ_tm M) (bl_tm M)
(AR_SimRead, tk, i, buf, dvec, posk)"
and pad_blank: "∀j ≥ k_tm M. mt_tape c' j (mt_pos c' j) = BLANK4"
and src_bounded: "ar_stage_bounded (bl_tm M) (k_tm M)
(AR_SimRead, tk, i, buf, dvec, posk)"
shows "∃c''. (c', c'') ∈ mttm_step (ar_delta_read M)
∧ mt_state c'' = (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 (mt_tape c' tk (mt_pos c' tk)))),
dvec, posk)
∧ mt_tape c'' = mt_tape c'
∧ mt_pos c'' = (mt_pos c')(tk := Suc (mt_pos c' tk))"
proof -
have src: "fst (snd (mt_state c')) = AR_SimRead" using stg by simp
show ?thesis
using ar_exists_step_in_sub_read
[OF ar_read_bit_step[OF vM stg qQ posk_proper ilo ihi kge2 vsrc pad_blank src_bounded] src] .
qed
lemma ar_read_bit_boundary_step_in_sub:
fixes M :: "('q, 'a) mttm"
and c' :: "(sym4, 'q × 'a ar_stage) mt_config"
assumes vM: "valid_mttm M"
and stg: "mt_state c' = (q, AR_SimRead, tk, i, buf, dvec, posk)"
and qQ: "q ∈ Q_tm M"
and notlast: "¬ is_last_k M tk"
and posk_proper: "posk tk ∈ {AR_AtFirstProper, AR_AtFurtherProper}"
and ieq: "i = Suc (block_width (Γ_tm M))"
and vsrc: "ar_valid_stage (Γ_tm M) (bl_tm M)
(AR_SimRead, tk, i, buf, dvec, posk)"
and pad_blank: "∀j ≥ k_tm M. mt_tape c' j (mt_pos c' j) = BLANK4"
and src_bounded: "ar_stage_bounded (bl_tm M) (k_tm M)
(AR_SimRead, tk, i, buf, dvec, posk)"
shows "∃c''. (c', c'') ∈ mttm_step (ar_delta_read M)
∧ mt_state c'' = (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 (mt_tape c' tk (mt_pos c' tk)))),
dvec, posk)
∧ mt_tape c'' = mt_tape c'
∧ mt_pos c'' = (mt_pos c')(tk := Suc (mt_pos c' tk))"
proof -
have src: "fst (snd (mt_state c')) = AR_SimRead" using stg by simp
show ?thesis
using ar_exists_step_in_sub_read
[OF ar_read_bit_boundary_step[OF vM stg qQ notlast posk_proper ieq vsrc pad_blank src_bounded]
src] .
qed
lemma ar_read_bit_finish_step_in_sub:
fixes M :: "('q, 'a) mttm"
and c' :: "(sym4, 'q × 'a ar_stage) mt_config"
assumes vM: "valid_mttm M"
and stg: "mt_state c' = (q, AR_SimRead, tk, i, buf, dvec, posk)"
and qQ: "q ∈ Q_tm M"
and last: "is_last_k M tk"
and posk_proper: "posk tk ∈ {AR_AtFirstProper, AR_AtFurtherProper}"
and ieq: "i = Suc (block_width (Γ_tm M))"
and vsrc: "ar_valid_stage (Γ_tm M) (bl_tm M)
(AR_SimRead, tk, i, buf, dvec, posk)"
and pad_blank: "∀j ≥ k_tm M. mt_tape c' j (mt_pos c' j) = BLANK4"
and src_bounded: "ar_stage_bounded (bl_tm M) (k_tm M)
(AR_SimRead, tk, i, buf, dvec, posk)"
shows "∃c''. (c', c'') ∈ mttm_step (ar_delta_read M)
∧ mt_state c'' = (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 (mt_tape c' tk (mt_pos c' tk)))),
dvec, posk)
∧ mt_tape c'' = mt_tape c'
∧ mt_pos c'' = (mt_pos c')(tk := Suc (mt_pos c' tk))"
proof -
have src: "fst (snd (mt_state c')) = AR_SimRead" using stg by simp
show ?thesis
using ar_exists_step_in_sub_read
[OF ar_read_bit_finish_step[OF vM stg qQ last posk_proper ieq vsrc pad_blank src_bounded]
src] .
qed
subsection ‹Read-phase combiners, sub-relation chain variants›
text ‹Multi-step combiner ‹_in_sub› variants follow the same
proof structure as the originals, but obtain their sub-chains from
the leaf ‹_in_sub› companions and compose via the generic
‹relpow_Suc_I2›/‹relpow_add› combinators (which work over
any relation, in particular ‹mttm_step (ar_delta_read M)›).
All bookkeeping for tape, position, state shape transfers verbatim
from the originals.›
lemma ar_read_bit_loop_in_sub:
fixes M :: "('q, 'a) mttm"
and c' :: "(sym4, 'q × 'a ar_stage) mt_config"
assumes vM: "valid_mttm M"
and qQ: "q ∈ Q_tm M"
and kge2: "2 ≤ block_width (Γ_tm M)"
and posk_proper: "posk tk ∈ {AR_AtFirstProper, AR_AtFurtherProper}"
and stg: "mt_state c' = (q, AR_SimRead, tk, 2, buf0, dvec, posk)"
and buf0_valid: "∀k. buf0 k ∈ Γ_tm M ∪ {bl_tm M}"
and pos_base: "mt_pos c' tk = base"
and pad0: "∀j ≥ k_tm M. mt_tape c' j (mt_pos c' j) = BLANK4"
and src0: "ar_stage_bounded (bl_tm M) (k_tm M)
(AR_SimRead, tk, 2, buf0, dvec, posk)"
shows "∃c''. (c', c'') ∈ (mttm_step (ar_delta_read M))
^^ (block_width (Γ_tm M) - 1)
∧ mt_state c'' = (q, AR_SimRead, tk, Suc (block_width (Γ_tm M)),
buf0(tk := foldl (ar_acc (Γ_tm M) (bl_tm M)) (buf0 tk)
(map (λm. mt_tape c' tk (base + m))
[0..<block_width (Γ_tm M) - 1])),
dvec, posk)
∧ mt_pos c'' tk = base + (block_width (Γ_tm M) - 1)
∧ mt_tape c'' = mt_tape c'
∧ (∀k'. k' ≠ tk ⟶ mt_pos c'' k' = mt_pos c' k')"
by (rule ar_read_bit_loop_gen
[OF ar_read_bit_step_in_sub vM qQ kge2 posk_proper stg buf0_valid pos_base pad0 src0])
lemma ar_read_proper_prefix_in_sub:
fixes M :: "('q, 'a) mttm"
and c' :: "(sym4, 'q × 'a ar_stage) mt_config"
assumes vM: "valid_mttm M"
and qQ: "q ∈ Q_tm M"
and kge2: "2 ≤ block_width (Γ_tm M)"
and posk_proper: "posk tk ∈ {AR_AtFirstProper, AR_AtFurtherProper}"
and stg: "mt_state c' = (q, AR_SimRead, tk, 0, buf, dvec, posk)"
and notLE: "mt_tape c' tk (mt_pos c' tk) ≠ LE4"
and base_pos: "0 < base"
and pos_base: "mt_pos c' tk = base"
and vsrc: "ar_valid_stage (Γ_tm M) (bl_tm M)
(AR_SimRead, tk, 0, buf, dvec, posk)"
and pad0: "∀j ≥ k_tm M. mt_tape c' j (mt_pos c' j) = BLANK4"
and src0: "ar_stage_bounded (bl_tm M) (k_tm M)
(AR_SimRead, tk, 0, buf, dvec, posk)"
shows "∃c''. (c', c'') ∈ (mttm_step (ar_delta_read M))
^^ Suc (block_width (Γ_tm M))
∧ mt_state c'' = (q, AR_SimRead, tk, Suc (block_width (Γ_tm M)),
buf(tk := foldl (ar_acc (Γ_tm M) (bl_tm M))
(gamma_unenum (Γ_tm M) (bl_tm M) 0)
(map (λm. mt_tape c' tk (base + m))
[0..<block_width (Γ_tm M) - 1])),
dvec,
posk(tk := if mt_tape c' tk (base - 1) = LE4
then AR_AtFirstProper else AR_AtFurtherProper))
∧ mt_tape c'' = mt_tape c'
∧ mt_pos c'' = (mt_pos c')(tk := base + (block_width (Γ_tm M) - 1))"
by (rule ar_read_proper_prefix_gen
[OF ar_read_lookback1_step_in_sub ar_read_lookback2_step_in_sub
ar_read_bit_loop_in_sub
vM qQ kge2 posk_proper stg notLE base_pos pos_base vsrc pad0 src0])
lemma ar_read_proper_step_in_sub:
fixes M :: "('q, 'a) mttm"
and c' :: "(sym4, 'q × 'a ar_stage) mt_config"
assumes vM: "valid_mttm M"
and qQ: "q ∈ Q_tm M"
and kge2: "2 ≤ block_width (Γ_tm M)"
and notlast: "¬ is_last_k M tk"
and posk_proper: "posk tk ∈ {AR_AtFirstProper, AR_AtFurtherProper}"
and stg: "mt_state c' = (q, AR_SimRead, tk, 0, buf, dvec, posk)"
and notLE: "mt_tape c' tk (mt_pos c' tk) ≠ LE4"
and base_pos: "0 < base"
and pos_base: "mt_pos c' tk = base"
and vsrc: "ar_valid_stage (Γ_tm M) (bl_tm M)
(AR_SimRead, tk, 0, buf, dvec, posk)"
and pad0: "∀j ≥ k_tm M. mt_tape c' j (mt_pos c' j) = BLANK4"
and src0: "ar_stage_bounded (bl_tm M) (k_tm M)
(AR_SimRead, tk, 0, buf, dvec, posk)"
shows "∃c''. (c', c'') ∈ (mttm_step (ar_delta_read M))
^^ (block_width (Γ_tm M) + 2)
∧ mt_state c'' = (q, AR_SimRead, k_succ tk, 0,
buf(tk := foldl (ar_acc (Γ_tm M) (bl_tm M))
(gamma_unenum (Γ_tm M) (bl_tm M) 0)
(map (λm. mt_tape c' tk (base + m))
[0..<block_width (Γ_tm M)])),
dvec,
posk(tk := if mt_tape c' tk (base - 1) = LE4
then AR_AtFirstProper else AR_AtFurtherProper))
∧ mt_tape c'' = mt_tape c'
∧ mt_pos c'' = (mt_pos c')(tk := base + block_width (Γ_tm M))"
by (rule ar_read_proper_step_gen
[OF ar_read_proper_prefix_in_sub ar_read_bit_boundary_step_in_sub
vM qQ kge2 notlast posk_proper stg notLE base_pos pos_base vsrc pad0 src0])
lemma ar_read_proper_finish_step_in_sub:
fixes M :: "('q, 'a) mttm"
and c' :: "(sym4, 'q × 'a ar_stage) mt_config"
assumes vM: "valid_mttm M"
and qQ: "q ∈ Q_tm M"
and kge2: "2 ≤ block_width (Γ_tm M)"
and last: "is_last_k M tk"
and posk_proper: "posk tk ∈ {AR_AtFirstProper, AR_AtFurtherProper}"
and stg: "mt_state c' = (q, AR_SimRead, tk, 0, buf, dvec, posk)"
and notLE: "mt_tape c' tk (mt_pos c' tk) ≠ LE4"
and base_pos: "0 < base"
and pos_base: "mt_pos c' tk = base"
and vsrc: "ar_valid_stage (Γ_tm M) (bl_tm M)
(AR_SimRead, tk, 0, buf, dvec, posk)"
and pad0: "∀j ≥ k_tm M. mt_tape c' j (mt_pos c' j) = BLANK4"
and src0: "ar_stage_bounded (bl_tm M) (k_tm M)
(AR_SimRead, tk, 0, buf, dvec, posk)"
shows "∃c''. (c', c'') ∈ (mttm_step (ar_delta_read M))
^^ (block_width (Γ_tm M) + 2)
∧ mt_state c'' = (q, AR_SimCompute, k_unidx 0, 0,
buf(tk := foldl (ar_acc (Γ_tm M) (bl_tm M))
(gamma_unenum (Γ_tm M) (bl_tm M) 0)
(map (λm. mt_tape c' tk (base + m))
[0..<block_width (Γ_tm M)])),
dvec,
posk(tk := if mt_tape c' tk (base - 1) = LE4
then AR_AtFirstProper else AR_AtFurtherProper))
∧ mt_tape c'' = mt_tape c'
∧ mt_pos c'' = (mt_pos c')(tk := base + block_width (Γ_tm M))"
by (rule ar_read_proper_finish_step_gen
[OF ar_read_proper_prefix_in_sub ar_read_bit_finish_step_in_sub
vM qQ kge2 last posk_proper stg notLE base_pos pos_base vsrc pad0 src0])
lemma ar_read_tape_step_in_sub:
fixes M :: "('q, 'a) mttm"
and c' :: "(sym4, 'q × 'a ar_stage) mt_config"
and tM :: "nat ⇒ 'a"
assumes vM: "valid_mttm M"
and qQ: "q ∈ Q_tm M"
and kge2: "2 ≤ block_width (Γ_tm M)"
and notlast: "¬ is_last_k M tk"
and stg: "mt_state c' = (q, AR_SimRead, tk, 0, buf, dvec, posk)"
and tcorr: "ar_tape_correspondence (Γ_tm M) (le_tm M) (bl_tm M)
tM (mt_tape c' tk)"
and ppos: "mt_pos c' tk = sim_pos (block_width (Γ_tm M)) p"
and pkok: "posk tk = AR_AtLE ⟷ p = 0"
and proper_mem: "1 ≤ p ⟹ tM p ∈ Γ_tm M"
and vsrc: "ar_valid_stage (Γ_tm M) (bl_tm M)
(AR_SimRead, tk, 0, buf, dvec, posk)"
and pad0: "∀j ≥ k_tm M. mt_tape c' j (mt_pos c' j) = BLANK4"
and src0: "ar_stage_bounded (bl_tm M) (k_tm M)
(AR_SimRead, tk, 0, buf, dvec, posk)"
shows "∃c''. (c', c'') ∈ (mttm_step (ar_delta_read M))
^^ (if p = 0 then 1 else block_width (Γ_tm M) + 2)
∧ mt_state c'' = (q, AR_SimRead, k_succ tk, 0,
buf(tk := tM p), dvec,
posk(tk := if p = 0 then AR_AtLE
else if p = 1 then AR_AtFirstProper
else AR_AtFurtherProper))
∧ mt_tape c'' = mt_tape c'
∧ mt_pos c'' = (mt_pos c')(tk :=
if p = 0 then Suc 0
else sim_pos (block_width (Γ_tm M)) p + block_width (Γ_tm M))"
by (rule ar_read_tape_step_gen
[OF ar_read_le_step_in_sub ar_read_proper_step_in_sub
vM qQ kge2 notlast stg tcorr ppos pkok proper_mem vsrc pad0 src0])
lemma ar_read_tape_finish_step_in_sub:
fixes M :: "('q, 'a) mttm"
and c' :: "(sym4, 'q × 'a ar_stage) mt_config"
and tM :: "nat ⇒ 'a"
assumes vM: "valid_mttm M"
and qQ: "q ∈ Q_tm M"
and kge2: "2 ≤ block_width (Γ_tm M)"
and last: "is_last_k M tk"
and stg: "mt_state c' = (q, AR_SimRead, tk, 0, buf, dvec, posk)"
and tcorr: "ar_tape_correspondence (Γ_tm M) (le_tm M) (bl_tm M)
tM (mt_tape c' tk)"
and ppos: "mt_pos c' tk = sim_pos (block_width (Γ_tm M)) p"
and pkok: "posk tk = AR_AtLE ⟷ p = 0"
and proper_mem: "1 ≤ p ⟹ tM p ∈ Γ_tm M"
and vsrc: "ar_valid_stage (Γ_tm M) (bl_tm M)
(AR_SimRead, tk, 0, buf, dvec, posk)"
and pad0: "∀j ≥ k_tm M. mt_tape c' j (mt_pos c' j) = BLANK4"
and src0: "ar_stage_bounded (bl_tm M) (k_tm M)
(AR_SimRead, tk, 0, buf, dvec, posk)"
shows "∃c''. (c', c'') ∈ (mttm_step (ar_delta_read M))
^^ (if p = 0 then 1 else block_width (Γ_tm M) + 2)
∧ mt_state c'' = (q, AR_SimCompute, k_unidx 0, 0,
buf(tk := tM p), dvec,
posk(tk := if p = 0 then AR_AtLE
else if p = 1 then AR_AtFirstProper
else AR_AtFurtherProper))
∧ mt_tape c'' = mt_tape c'
∧ mt_pos c'' = (mt_pos c')(tk :=
if p = 0 then Suc 0
else sim_pos (block_width (Γ_tm M)) p + block_width (Γ_tm M))"
by (rule ar_read_tape_finish_step_gen
[OF ar_read_le_finish_step_in_sub ar_read_proper_finish_step_in_sub
vM qQ kge2 last stg tcorr ppos pkok proper_mem vsrc pad0 src0])
lemma ar_read_prefix_in_sub:
fixes M :: "('q, 'a) mttm"
and cM :: "('a, 'q) mt_config"
and c0 :: "(sym4, 'q × 'a ar_stage) mt_config"
assumes vM: "valid_mttm M"
and qQ: "q ∈ Q_tm M"
and kge2: "2 ≤ block_width (Γ_tm M)"
and stg0: "mt_state c0 = (q, AR_SimRead, 0, 0, buf0, dvec, posk0)"
and tcorr: "∀k < k_tm M. ar_tape_correspondence (Γ_tm M) (le_tm M) (bl_tm M)
(mt_tape cM k) (mt_tape c0 k)"
and ppos: "⋀k. mt_pos c0 k = sim_pos (block_width (Γ_tm M)) (mt_pos cM k)"
and pkok: "⋀k. posk0 k = AR_AtLE ⟷ mt_pos cM k = 0"
and tapeG: "⋀k. mt_tape cM k (mt_pos cM k) ∈ Γ_tm M"
and bufG: "⋀k. buf0 k ∈ Γ_tm M ∪ {bl_tm M}"
and pad0: "∀j ≥ k_tm M. mt_tape c0 j (mt_pos c0 j) = BLANK4"
and src0: "ar_stage_bounded (bl_tm M) (k_tm M)
(AR_SimRead, 0, 0, buf0, dvec, posk0)"
shows "j ≤ k_tm M - 1 ⟹
(∃c m. (c0, c) ∈ (mttm_step (ar_delta_read M)) ^^ m
∧ m ≤ j * (block_width (Γ_tm M) + 2)
∧ mt_state c = (q, AR_SimRead, k_unidx j, 0,
(λk. if k_idx k < j then mt_tape cM k (mt_pos cM k) else buf0 k),
dvec,
(λk. if k_idx k < j
then (if mt_pos cM k = 0 then AR_AtLE
else if mt_pos cM k = 1 then AR_AtFirstProper
else AR_AtFurtherProper)
else posk0 k))
∧ mt_tape c = mt_tape c0
∧ mt_pos c = (λk. if k_idx k < j
then (if mt_pos cM k = 0 then Suc 0
else sim_pos (block_width (Γ_tm M)) (mt_pos cM k)
+ block_width (Γ_tm M))
else mt_pos c0 k))"
by (rule ar_read_prefix_gen
[OF _ vM qQ kge2 stg0 tcorr ppos pkok tapeG bufG pad0 src0])
(rule ar_read_tape_step_in_sub; assumption)
lemma ar_read_phase_in_sub:
fixes M :: "('q, 'a) mttm"
and cM :: "('a, 'q) mt_config"
and c0 :: "(sym4, 'q × 'a ar_stage) mt_config"
assumes vM: "valid_mttm M"
and qQ: "q ∈ Q_tm M"
and kge2: "2 ≤ block_width (Γ_tm M)"
and stg0: "mt_state c0 = (q, AR_SimRead, 0, 0, buf0, dvec, posk0)"
and tcorr: "∀k < k_tm M. ar_tape_correspondence (Γ_tm M) (le_tm M) (bl_tm M)
(mt_tape cM k) (mt_tape c0 k)"
and ppos: "⋀k. mt_pos c0 k = sim_pos (block_width (Γ_tm M)) (mt_pos cM k)"
and pkok: "⋀k. posk0 k = AR_AtLE ⟷ mt_pos cM k = 0"
and tapeG: "⋀k. mt_tape cM k (mt_pos cM k) ∈ Γ_tm M"
and bufG: "⋀k. buf0 k ∈ Γ_tm M ∪ {bl_tm M}"
and pad0: "∀j ≥ k_tm M. mt_tape c0 j (mt_pos c0 j) = BLANK4"
and src0: "ar_stage_bounded (bl_tm M) (k_tm M)
(AR_SimRead, 0, 0, buf0, dvec, posk0)"
shows "∃c m. (c0, c) ∈ (mttm_step (ar_delta_read M)) ^^ m
∧ m ≤ k_tm M * (block_width (Γ_tm M) + 2)
∧ mt_state c = (q, AR_SimCompute, k_unidx 0, 0,
(λk. if k < k_tm M then mt_tape cM k (mt_pos cM k) else buf0 k),
dvec,
(λk. if k < k_tm M
then (if mt_pos cM k = 0 then AR_AtLE
else if mt_pos cM k = 1 then AR_AtFirstProper
else AR_AtFurtherProper)
else posk0 k))
∧ mt_tape c = mt_tape c0
∧ mt_pos c = (λk. if k < k_tm M
then (if mt_pos cM k = 0 then Suc 0
else sim_pos (block_width (Γ_tm M)) (mt_pos cM k) + block_width (Γ_tm M))
else mt_pos c0 k)"
by (rule ar_read_phase_gen
[OF _ _ vM qQ kge2 stg0 tcorr ppos pkok tapeG bufG pad0 src0];
(rule ar_read_prefix_in_sub ar_read_tape_finish_step_in_sub; assumption))
subsection ‹Write-phase leaves, sub-relation chain variants›
text ‹Six write-phase leaves mirror to the sub-relation
‹mttm_step (ar_delta_write M)› via ‹ar_step_write_lift›,
parallel to the seven read leaves at the earlier subsection.
Each variant obtains the step from the original leaf, derives the
‹AR_SimWrite› source tag from the ‹stg› hypothesis,
and lifts via ‹ar_step_write_lift›.›
lemma ar_write_le_step_in_sub:
fixes M :: "('q, 'a) mttm"
and c' :: "(sym4, 'q × 'a ar_stage) mt_config"
assumes vM: "valid_mttm M"
and stg: "mt_state c' = (q, AR_SimWrite, tk, 0, buf, dvec, posk)"
and qQ: "q ∈ Q_tm M"
and poskLE: "posk tk = AR_AtLE"
and notlast: "¬ is_last_k M tk"
and vsrc: "ar_valid_stage (Γ_tm M) (bl_tm M)
(AR_SimWrite, tk, 0, buf, dvec, posk)"
and pad_blank: "∀j ≥ k_tm M. mt_tape c' j (mt_pos c' j) = BLANK4"
and src_bounded: "ar_stage_bounded (bl_tm M) (k_tm M)
(AR_SimWrite, tk, 0, buf, dvec, posk)"
shows "∃c''. (c', c'') ∈ mttm_step (ar_delta_write M)
∧ mt_state c'' = (q, AR_SimWrite, k_succ tk, 0, buf, dvec, posk)
∧ mt_tape c'' = mt_tape c'
∧ mt_pos c'' = mt_pos c'"
proof -
have src: "fst (snd (mt_state c')) = AR_SimWrite" using stg by simp
show ?thesis
using ar_exists_step_in_sub_write
[OF ar_write_le_step[OF vM stg qQ poskLE notlast vsrc pad_blank src_bounded] src] .
qed
lemma ar_write_le_finish_step_in_sub:
fixes M :: "('q, 'a) mttm"
and c' :: "(sym4, 'q × 'a ar_stage) mt_config"
assumes vM: "valid_mttm M"
and stg: "mt_state c' = (q, AR_SimWrite, tk, 0, buf, dvec, posk)"
and qQ: "q ∈ Q_tm M"
and poskLE: "posk tk = AR_AtLE"
and last: "is_last_k M tk"
and vsrc: "ar_valid_stage (Γ_tm M) (bl_tm M)
(AR_SimWrite, tk, 0, buf, dvec, posk)"
and pad_blank: "∀j ≥ k_tm M. mt_tape c' j (mt_pos c' j) = BLANK4"
and src_bounded: "ar_stage_bounded (bl_tm M) (k_tm M)
(AR_SimWrite, tk, 0, buf, dvec, posk)"
shows "∃c''. (c', c'') ∈ mttm_step (ar_delta_write M)
∧ mt_state c'' = (q, AR_SimAdvance, k_unidx 0, 0, buf, dvec, posk)
∧ mt_tape c'' = mt_tape c'
∧ mt_pos c'' = mt_pos c'"
proof -
have src: "fst (snd (mt_state c')) = AR_SimWrite" using stg by simp
show ?thesis
using ar_exists_step_in_sub_write
[OF ar_write_le_finish_step[OF vM stg qQ poskLE last vsrc pad_blank src_bounded] src] .
qed
lemma ar_write_walk_step_in_sub:
fixes M :: "('q, 'a) mttm"
and c' :: "(sym4, 'q × 'a ar_stage) mt_config"
assumes vM: "valid_mttm M"
and stg: "mt_state c' = (q, AR_SimWrite, tk, i, buf, dvec, posk)"
and qQ: "q ∈ Q_tm M"
and poskproper: "posk tk ≠ AR_AtLE"
and notLE: "mt_tape c' tk (mt_pos c' tk) ≠ LE4"
and step_le: "Suc i ≤ block_width (Γ_tm M)"
and vsrc: "ar_valid_stage (Γ_tm M) (bl_tm M)
(AR_SimWrite, tk, i, buf, dvec, posk)"
and pad_blank: "∀j ≥ k_tm M. mt_tape c' j (mt_pos c' j) = BLANK4"
and src_bounded: "ar_stage_bounded (bl_tm M) (k_tm M)
(AR_SimWrite, tk, i, buf, dvec, posk)"
shows "∃c''. (c', c'') ∈ mttm_step (ar_delta_write M)
∧ mt_state c'' = (q, AR_SimWrite, tk, Suc i, buf, dvec, posk)
∧ mt_tape c'' = mt_tape c'
∧ mt_pos c'' = (mt_pos c')(tk := mt_pos c' tk - 1)"
proof -
have src: "fst (snd (mt_state c')) = AR_SimWrite" using stg by simp
show ?thesis
using ar_exists_step_in_sub_write
[OF ar_write_walk_step[OF vM stg qQ poskproper notLE step_le vsrc pad_blank src_bounded] src] .
qed
lemma ar_write_bit_step_in_sub:
fixes M :: "('q, 'a) mttm"
and c' :: "(sym4, 'q × 'a ar_stage) mt_config"
assumes vM: "valid_mttm M"
and stg: "mt_state c' = (q, AR_SimWrite, tk, i, buf, dvec, posk)"
and qQ: "q ∈ Q_tm M"
and poskproper: "posk tk ≠ AR_AtLE"
and notLE: "mt_tape c' tk (mt_pos c' tk) ≠ LE4"
and ilo: "block_width (Γ_tm M) ≤ i"
and ihi: "Suc i < 2 * block_width (Γ_tm M)"
and vsrc: "ar_valid_stage (Γ_tm M) (bl_tm M)
(AR_SimWrite, tk, i, buf, dvec, posk)"
and pad_blank: "∀j ≥ k_tm M. mt_tape c' j (mt_pos c' j) = BLANK4"
and src_bounded: "ar_stage_bounded (bl_tm M) (k_tm M)
(AR_SimWrite, tk, i, buf, dvec, posk)"
shows "∃c''. (c', c'') ∈ mttm_step (ar_delta_write M)
∧ mt_state c'' = (q, AR_SimWrite, tk, Suc i, buf, dvec, posk)
∧ mt_tape c'' = (mt_tape c')(tk :=
(mt_tape c' tk)(mt_pos c' tk :=
write_bit (Γ_tm M) (bl_tm M) (buf tk)
(i - block_width (Γ_tm M))))
∧ mt_pos c'' = (mt_pos c')(tk := Suc (mt_pos c' tk))"
proof -
have src: "fst (snd (mt_state c')) = AR_SimWrite" using stg by simp
show ?thesis
using ar_exists_step_in_sub_write
[OF ar_write_bit_step[OF vM stg qQ poskproper notLE ilo ihi vsrc pad_blank src_bounded] src] .
qed
lemma ar_write_bit_boundary_step_in_sub:
fixes M :: "('q, 'a) mttm"
and c' :: "(sym4, 'q × 'a ar_stage) mt_config"
assumes vM: "valid_mttm M"
and stg: "mt_state c' = (q, AR_SimWrite, tk, i, buf, dvec, posk)"
and qQ: "q ∈ Q_tm M"
and poskproper: "posk tk ≠ AR_AtLE"
and notLE: "mt_tape c' tk (mt_pos c' tk) ≠ LE4"
and notlast: "¬ is_last_k M tk"
and ihi: "Suc i = 2 * block_width (Γ_tm M)"
and vsrc: "ar_valid_stage (Γ_tm M) (bl_tm M)
(AR_SimWrite, tk, i, buf, dvec, posk)"
and pad_blank: "∀j ≥ k_tm M. mt_tape c' j (mt_pos c' j) = BLANK4"
and src_bounded: "ar_stage_bounded (bl_tm M) (k_tm M)
(AR_SimWrite, tk, i, buf, dvec, posk)"
shows "∃c''. (c', c'') ∈ mttm_step (ar_delta_write M)
∧ mt_state c'' = (q, AR_SimWrite, k_succ tk, 0, buf, dvec, posk)
∧ mt_tape c'' = (mt_tape c')(tk :=
(mt_tape c' tk)(mt_pos c' tk :=
write_bit (Γ_tm M) (bl_tm M) (buf tk)
(i - block_width (Γ_tm M))))
∧ mt_pos c'' = (mt_pos c')(tk := Suc (mt_pos c' tk))"
proof -
have src: "fst (snd (mt_state c')) = AR_SimWrite" using stg by simp
show ?thesis
using ar_exists_step_in_sub_write
[OF ar_write_bit_boundary_step
[OF vM stg qQ poskproper notLE notlast ihi vsrc pad_blank src_bounded] src] .
qed
lemma ar_write_bit_finish_step_in_sub:
fixes M :: "('q, 'a) mttm"
and c' :: "(sym4, 'q × 'a ar_stage) mt_config"
assumes vM: "valid_mttm M"
and stg: "mt_state c' = (q, AR_SimWrite, tk, i, buf, dvec, posk)"
and qQ: "q ∈ Q_tm M"
and poskproper: "posk tk ≠ AR_AtLE"
and notLE: "mt_tape c' tk (mt_pos c' tk) ≠ LE4"
and last: "is_last_k M tk"
and ihi: "Suc i = 2 * block_width (Γ_tm M)"
and vsrc: "ar_valid_stage (Γ_tm M) (bl_tm M)
(AR_SimWrite, tk, i, buf, dvec, posk)"
and pad_blank: "∀j ≥ k_tm M. mt_tape c' j (mt_pos c' j) = BLANK4"
and src_bounded: "ar_stage_bounded (bl_tm M) (k_tm M)
(AR_SimWrite, tk, i, buf, dvec, posk)"
shows "∃c''. (c', c'') ∈ mttm_step (ar_delta_write M)
∧ mt_state c'' = (q, AR_SimAdvance, k_unidx 0, 0, buf, dvec, posk)
∧ mt_tape c'' = (mt_tape c')(tk :=
(mt_tape c' tk)(mt_pos c' tk :=
write_bit (Γ_tm M) (bl_tm M) (buf tk)
(i - block_width (Γ_tm M))))
∧ mt_pos c'' = (mt_pos c')(tk := Suc (mt_pos c' tk))"
proof -
have src: "fst (snd (mt_state c')) = AR_SimWrite" using stg by simp
show ?thesis
using ar_exists_step_in_sub_write
[OF ar_write_bit_finish_step
[OF vM stg qQ poskproper notLE last ihi vsrc pad_blank src_bounded] src] .
qed
subsection ‹Advance-phase leaves, sub-relation chain variants›
text ‹Three advance-phase leaves
(‹ar_advance_walk_step›, ‹ar_advance_boundary_step›,
‹ar_advance_finish_step›) mirror to the sub-relation
‹mttm_step (ar_delta_advance M)› via
‹ar_exists_step_in_sub_advance›, parallel to the write and
read leaves above. Each variant derives the
‹AR_SimAdvance› source tag from ‹stg›, then composes
the original leaf with the existence lifter.›
lemma ar_advance_walk_step_in_sub:
fixes M :: "('q, 'a) mttm"
and c' :: "(sym4, 'q × 'a ar_stage) mt_config"
assumes vM: "valid_mttm M"
and stg: "mt_state c' = (q, AR_SimAdvance, tk, i, buf, dvec, posk)"
and qQ: "q ∈ Q_tm M"
and notLE: "mt_tape c' tk (mt_pos c' tk) ≠ LE4"
and step_lt: "Suc i < ar_disp (block_width (Γ_tm M)) (dvec tk) (posk tk)"
and vsrc: "ar_valid_stage (Γ_tm M) (bl_tm M)
(AR_SimAdvance, tk, i, buf, dvec, posk)"
and pad_blank: "∀j ≥ k_tm M. mt_tape c' j (mt_pos c' j) = BLANK4"
and src_bounded: "ar_stage_bounded (bl_tm M) (k_tm M)
(AR_SimAdvance, tk, i, buf, dvec, posk)"
shows "∃c''. (c', c'') ∈ mttm_step (ar_delta_advance M)
∧ mt_state c'' = (q, AR_SimAdvance, tk, Suc i, buf, dvec, posk)
∧ mt_tape c'' = mt_tape c'
∧ mt_pos c'' = (mt_pos c')(tk := mt_pos c' tk - 1)"
proof -
have src: "fst (snd (mt_state c')) = AR_SimAdvance" using stg by simp
show ?thesis
using ar_exists_step_in_sub_advance
[OF ar_advance_walk_step[OF vM stg qQ notLE step_lt vsrc pad_blank src_bounded] src] .
qed
lemma ar_advance_boundary_step_in_sub:
fixes M :: "('q, 'a) mttm"
and c' :: "(sym4, 'q × 'a ar_stage) mt_config"
assumes vM: "valid_mttm M"
and stg: "mt_state c' = (q, AR_SimAdvance, tk, i, buf, dvec, posk)"
and qQ: "q ∈ Q_tm M"
and notlast: "¬ is_last_k M tk"
and fire: "(dvec tk = dir.R ∧ i = 0)
∨ (dvec tk ≠ dir.R
∧ mt_tape c' tk (mt_pos c' tk) ≠ LE4
∧ Suc i = ar_disp (block_width (Γ_tm M)) (dvec tk) (posk tk))"
and vsrc: "ar_valid_stage (Γ_tm M) (bl_tm M)
(AR_SimAdvance, tk, i, buf, dvec, posk)"
and pad_blank: "∀j ≥ k_tm M. mt_tape c' j (mt_pos c' j) = BLANK4"
and src_bounded: "ar_stage_bounded (bl_tm M) (k_tm M)
(AR_SimAdvance, tk, i, buf, dvec, posk)"
shows "∃c''. (c', c'') ∈ mttm_step (ar_delta_advance M)
∧ mt_state c'' = (q, AR_SimAdvance, k_succ tk, 0, buf, dvec,
posk(tk := ar_newpos (dvec tk) (posk tk)))
∧ mt_tape c'' = mt_tape c'
∧ mt_pos c'' = (if dvec tk = dir.R then mt_pos c'
else (mt_pos c')(tk := mt_pos c' tk - 1))"
proof -
have src: "fst (snd (mt_state c')) = AR_SimAdvance" using stg by simp
show ?thesis
using ar_exists_step_in_sub_advance
[OF ar_advance_boundary_step[OF vM stg qQ notlast fire vsrc pad_blank src_bounded] src] .
qed
lemma ar_advance_finish_step_in_sub:
fixes M :: "('q, 'a) mttm"
and c' :: "(sym4, 'q × 'a ar_stage) mt_config"
assumes vM: "valid_mttm M"
and stg: "mt_state c' = (q, AR_SimAdvance, tk, i, buf, dvec, posk)"
and qQ: "q ∈ Q_tm M"
and last: "is_last_k M tk"
and fire: "(dvec tk = dir.R ∧ i = 0)
∨ (dvec tk ≠ dir.R
∧ mt_tape c' tk (mt_pos c' tk) ≠ LE4
∧ Suc i = ar_disp (block_width (Γ_tm M)) (dvec tk) (posk tk))"
and vsrc: "ar_valid_stage (Γ_tm M) (bl_tm M)
(AR_SimAdvance, tk, i, buf, dvec, posk)"
and pad_blank: "∀j ≥ k_tm M. mt_tape c' j (mt_pos c' j) = BLANK4"
and src_bounded: "ar_stage_bounded (bl_tm M) (k_tm M)
(AR_SimAdvance, tk, i, buf, dvec, posk)"
shows "∃c''. (c', c'') ∈ mttm_step (ar_delta_advance M)
∧ mt_state c'' = (q, AR_SimNext, k_unidx 0, 0, buf, dvec,
posk(tk := ar_newpos (dvec tk) (posk tk)))
∧ mt_tape c'' = mt_tape c'
∧ mt_pos c'' = (if dvec tk = dir.R then mt_pos c'
else (mt_pos c')(tk := mt_pos c' tk - 1))"
proof -
have src: "fst (snd (mt_state c')) = AR_SimAdvance" using stg by simp
show ?thesis
using ar_exists_step_in_sub_advance
[OF ar_advance_finish_step[OF vM stg qQ last fire vsrc pad_blank src_bounded] src] .
qed
subsection ‹Write-phase combiners, sub-relation chain variants›
text ‹Write-phase multi-step combiner ‹_in_sub› variants
follow the same proof structure as the originals, obtaining
sub-chains from the write-leaf ‹_in_sub› companions and
composing via the generic ‹relpow_Suc_I2› /
‹relpow_invariant_chain› combinators (which work over any
relation, in particular ‹mttm_step (ar_delta_write M)›).›
lemma ar_write_back_loop_in_sub:
fixes M :: "('q, 'a) mttm"
and c0 :: "(sym4, 'q × 'a ar_stage) mt_config"
assumes vM: "valid_mttm M"
and qQ: "q ∈ Q_tm M"
and kge2: "2 ≤ block_width (Γ_tm M)"
and poskproper: "posk tk ≠ AR_AtLE"
and stg: "mt_state c0 = (q, AR_SimWrite, tk, 0, buf, dvec, posk)"
and buf_valid: "∀k. buf k ∈ Γ_tm M ∪ {bl_tm M}"
and pos_base: "mt_pos c0 tk = base + block_width (Γ_tm M)"
and notLE: "⋀m. ⟦ 1 ≤ m; m ≤ block_width (Γ_tm M) ⟧
⟹ mt_tape c0 tk (base + m) ≠ LE4"
and pad0: "∀j ≥ k_tm M. mt_tape c0 j (mt_pos c0 j) = BLANK4"
and src0: "ar_stage_bounded (bl_tm M) (k_tm M)
(AR_SimWrite, tk, 0, buf, dvec, posk)"
shows "∃c'. (c0, c') ∈ (mttm_step (ar_delta_write M))
^^ block_width (Γ_tm M)
∧ mt_state c' = (q, AR_SimWrite, tk, block_width (Γ_tm M),
buf, dvec, posk)
∧ mt_pos c' tk = base
∧ mt_tape c' = mt_tape c0
∧ (∀k'. k' ≠ tk ⟶ mt_pos c' k' = mt_pos c0 k')"
by (rule ar_write_back_loop_gen
[OF ar_write_walk_step_in_sub vM qQ kge2 poskproper stg buf_valid pos_base notLE pad0 src0])
lemma ar_write_fwd_loop_in_sub:
fixes M :: "('q, 'a) mttm"
and c0 :: "(sym4, 'q × 'a ar_stage) mt_config"
assumes vM: "valid_mttm M"
and qQ: "q ∈ Q_tm M"
and kge2: "2 ≤ block_width (Γ_tm M)"
and poskproper: "posk tk ≠ AR_AtLE"
and stg: "mt_state c0 = (q, AR_SimWrite, tk, block_width (Γ_tm M),
buf, dvec, posk)"
and buf_valid: "∀k. buf k ∈ Γ_tm M ∪ {bl_tm M}"
and pos_base: "mt_pos c0 tk = base"
and notLE: "⋀m. m < block_width (Γ_tm M)
⟹ mt_tape c0 tk (base + m) ≠ LE4"
and pad0: "∀j ≥ k_tm M. mt_tape c0 j (mt_pos c0 j) = BLANK4"
and src0: "ar_stage_bounded (bl_tm M) (k_tm M)
(AR_SimWrite, tk, block_width (Γ_tm M), buf, dvec, posk)"
shows "∃c'. (c0, c') ∈ (mttm_step (ar_delta_write M))
^^ (block_width (Γ_tm M) - 1)
∧ mt_state c' = (q, AR_SimWrite, tk,
block_width (Γ_tm M) + (block_width (Γ_tm M) - 1),
buf, dvec, posk)
∧ mt_pos c' tk = base + (block_width (Γ_tm M) - 1)
∧ mt_tape c' tk = (λpos.
if base ≤ pos ∧ pos < base + (block_width (Γ_tm M) - 1)
then write_bit (Γ_tm M) (bl_tm M) (buf tk) (pos - base)
else mt_tape c0 tk pos)
∧ (∀k'. k' ≠ tk ⟶ mt_tape c' k' = mt_tape c0 k')
∧ (∀k'. k' ≠ tk ⟶ mt_pos c' k' = mt_pos c0 k')"
by (rule ar_write_fwd_loop_gen
[OF ar_write_bit_step_in_sub vM qQ kge2 poskproper stg buf_valid pos_base notLE pad0 src0])
text ‹The proper-cell single-tape write prefix, re-mirrored into
‹mttm_step (ar_delta_write M)›. Composes the back-walk loop
(‹ar_write_back_loop_in_sub›) and the forward bit-write loop
(‹ar_write_fwd_loop_in_sub›) by ‹relcompI› +
‹relpow_add›; since both ‹_in_sub› sub-combiners carry
field-for-field the same output contract as the originals, the
composition and the two ‹ext› reassemblies (tape, pos)
transfer verbatim with only the relation and the two helper calls
changed.›
lemma ar_write_proper_prefix_in_sub:
fixes M :: "('q, 'a) mttm"
and c' :: "(sym4, 'q × 'a ar_stage) mt_config"
assumes vM: "valid_mttm M"
and qQ: "q ∈ Q_tm M"
and kge2: "2 ≤ block_width (Γ_tm M)"
and poskproper: "posk tk ≠ AR_AtLE"
and stg: "mt_state c' = (q, AR_SimWrite, tk, 0, buf, dvec, posk)"
and buf_valid: "∀k. buf k ∈ Γ_tm M ∪ {bl_tm M}"
and pos_base: "mt_pos c' tk = base + block_width (Γ_tm M)"
and notLE: "⋀m. m ≤ block_width (Γ_tm M)
⟹ mt_tape c' tk (base + m) ≠ LE4"
and pad0: "∀j ≥ k_tm M. mt_tape c' j (mt_pos c' j) = BLANK4"
and src0: "ar_stage_bounded (bl_tm M) (k_tm M)
(AR_SimWrite, tk, 0, buf, dvec, posk)"
shows "∃c2. (c', c2) ∈ (mttm_step (ar_delta_write M))
^^ (block_width (Γ_tm M) + (block_width (Γ_tm M) - 1))
∧ mt_state c2 = (q, AR_SimWrite, tk,
block_width (Γ_tm M) + (block_width (Γ_tm M) - 1),
buf, dvec, posk)
∧ mt_tape c2 = (mt_tape c')(tk := (λpos.
if base ≤ pos ∧ pos < base + (block_width (Γ_tm M) - 1)
then write_bit (Γ_tm M) (bl_tm M) (buf tk) (pos - base)
else mt_tape c' tk pos))
∧ mt_pos c2 = (mt_pos c')(tk := base + (block_width (Γ_tm M) - 1))"
by (rule ar_write_proper_prefix_gen
[OF ar_write_back_loop_in_sub ar_write_fwd_loop_in_sub
vM qQ kge2 poskproper stg buf_valid pos_base notLE pad0 src0])
text ‹The proper-cell single-tape write, non-last tape, re-mirrored
into ‹mttm_step (ar_delta_write M)›. As
‹ar_write_proper_prefix_in_sub› followed by one bit-boundary
step (‹ar_write_bit_boundary_step_in_sub›), composing by
‹relpow_Suc_I›. The shared ‹write_block_extend› helper is
relation-agnostic (pure ‹fun_upd› arithmetic) and reused
verbatim; the body transfers from the original with only the
relation and the two helper references changed.›
lemma ar_write_proper_step_in_sub:
fixes M :: "('q, 'a) mttm"
and c' :: "(sym4, 'q × 'a ar_stage) mt_config"
assumes vM: "valid_mttm M"
and qQ: "q ∈ Q_tm M"
and kge2: "2 ≤ block_width (Γ_tm M)"
and notlast: "¬ is_last_k M tk"
and poskproper: "posk tk ≠ AR_AtLE"
and stg: "mt_state c' = (q, AR_SimWrite, tk, 0, buf, dvec, posk)"
and buf_valid: "∀k. buf k ∈ Γ_tm M ∪ {bl_tm M}"
and pos_base: "mt_pos c' tk = base + block_width (Γ_tm M)"
and notLE: "⋀m. m ≤ block_width (Γ_tm M)
⟹ mt_tape c' tk (base + m) ≠ LE4"
and pad0: "∀j ≥ k_tm M. mt_tape c' j (mt_pos c' j) = BLANK4"
and src0: "ar_stage_bounded (bl_tm M) (k_tm M)
(AR_SimWrite, tk, 0, buf, dvec, posk)"
shows "∃c''. (c', c'') ∈ (mttm_step (ar_delta_write M))
^^ (2 * block_width (Γ_tm M))
∧ mt_state c'' = (q, AR_SimWrite, k_succ tk, 0, buf, dvec, posk)
∧ mt_tape c'' = (mt_tape c')(tk := (λpos.
if base ≤ pos ∧ pos < base + block_width (Γ_tm M)
then write_bit (Γ_tm M) (bl_tm M) (buf tk) (pos - base)
else mt_tape c' tk pos))
∧ mt_pos c'' = (mt_pos c')(tk := base + block_width (Γ_tm M))"
by (rule ar_write_proper_step_gen
[OF ar_write_proper_prefix_in_sub ar_write_bit_boundary_step_in_sub
vM qQ kge2 notlast poskproper stg buf_valid pos_base notLE pad0 src0])
text ‹The proper-cell single-tape write, last tape, re-mirrored
into ‹mttm_step (ar_delta_write M)›. As
‹ar_write_proper_step_in_sub› but ‹tk› is the last tape,
so the closing step is ‹ar_write_bit_finish_step_in_sub›:
after the last-cell write the phase transitions to
‹AR_SimAdvance› with the current-tape field reset to
‹k_unidx 0›. Same ‹2b›-step block write and head return
to ‹base + b›; body transfers verbatim with only the relation
and the two helper references changed.›
lemma ar_write_proper_finish_step_in_sub:
fixes M :: "('q, 'a) mttm"
and c' :: "(sym4, 'q × 'a ar_stage) mt_config"
assumes vM: "valid_mttm M"
and qQ: "q ∈ Q_tm M"
and kge2: "2 ≤ block_width (Γ_tm M)"
and last: "is_last_k M tk"
and poskproper: "posk tk ≠ AR_AtLE"
and stg: "mt_state c' = (q, AR_SimWrite, tk, 0, buf, dvec, posk)"
and buf_valid: "∀k. buf k ∈ Γ_tm M ∪ {bl_tm M}"
and pos_base: "mt_pos c' tk = base + block_width (Γ_tm M)"
and notLE: "⋀m. m ≤ block_width (Γ_tm M)
⟹ mt_tape c' tk (base + m) ≠ LE4"
and pad0: "∀j ≥ k_tm M. mt_tape c' j (mt_pos c' j) = BLANK4"
and src0: "ar_stage_bounded (bl_tm M) (k_tm M)
(AR_SimWrite, tk, 0, buf, dvec, posk)"
shows "∃c''. (c', c'') ∈ (mttm_step (ar_delta_write M))
^^ (2 * block_width (Γ_tm M))
∧ mt_state c'' = (q, AR_SimAdvance, k_unidx 0, 0, buf, dvec, posk)
∧ mt_tape c'' = (mt_tape c')(tk := (λpos.
if base ≤ pos ∧ pos < base + block_width (Γ_tm M)
then write_bit (Γ_tm M) (bl_tm M) (buf tk) (pos - base)
else mt_tape c' tk pos))
∧ mt_pos c'' = (mt_pos c')(tk := base + block_width (Γ_tm M))"
by (rule ar_write_proper_finish_step_gen
[OF ar_write_proper_prefix_in_sub ar_write_bit_finish_step_in_sub
vM qQ kge2 last poskproper stg buf_valid pos_base notLE pad0 src0])
text ‹The unified single-tape write, non-last tape, re-mirrored
into ‹mttm_step (ar_delta_write M)›: the LE/proper dispatch
on ‹posk tk = AR_AtLE› (pinned by ‹poskle› to ‹p =
0›). The LE arm (‹ar_write_le_step_in_sub›, ‹1›
step) hands off untouched; the proper arm
(‹ar_write_proper_step_in_sub›, ‹2b› steps) overwrites
the ‹b›-cell block. Head invariant in both arms. The
‹≠ LE4› facts come from the input correspondence
‹tcorr›; that derivation is relation-agnostic and transfers
verbatim along with the relation and two helper references
changing.›
lemma ar_write_tape_step_in_sub:
fixes M :: "('q, 'a) mttm"
and c' :: "(sym4, 'q × 'a ar_stage) mt_config"
and tM :: "nat ⇒ 'a"
assumes vM: "valid_mttm M"
and qQ: "q ∈ Q_tm M"
and kge2: "2 ≤ block_width (Γ_tm M)"
and notlast: "¬ is_last_k M tk"
and stg: "mt_state c' = (q, AR_SimWrite, tk, 0, buf, dvec, posk)"
and tcorr: "ar_tape_correspondence (Γ_tm M) (le_tm M) (bl_tm M)
tM (mt_tape c' tk)"
and ppos: "mt_pos c' tk = (if p = 0 then Suc 0
else sim_pos (block_width (Γ_tm M)) p + block_width (Γ_tm M))"
and poskle: "posk tk = AR_AtLE ⟷ p = 0"
and buf_valid: "∀k. buf k ∈ Γ_tm M ∪ {bl_tm M}"
and vsrc: "ar_valid_stage (Γ_tm M) (bl_tm M)
(AR_SimWrite, tk, 0, buf, dvec, posk)"
and pad0: "∀j ≥ k_tm M. mt_tape c' j (mt_pos c' j) = BLANK4"
and src0: "ar_stage_bounded (bl_tm M) (k_tm M)
(AR_SimWrite, tk, 0, buf, dvec, posk)"
shows "∃c''. (c', c'') ∈ (mttm_step (ar_delta_write M))
^^ (if p = 0 then 1 else 2 * block_width (Γ_tm M))
∧ mt_state c'' = (q, AR_SimWrite, k_succ tk, 0, buf, dvec, posk)
∧ mt_tape c'' = (if p = 0 then mt_tape c'
else (mt_tape c')(tk := (λpos.
if sim_pos (block_width (Γ_tm M)) p ≤ pos
∧ pos < sim_pos (block_width (Γ_tm M)) p + block_width (Γ_tm M)
then write_bit (Γ_tm M) (bl_tm M) (buf tk)
(pos - sim_pos (block_width (Γ_tm M)) p)
else mt_tape c' tk pos)))
∧ mt_pos c'' = mt_pos c'"
by (rule ar_write_tape_step_gen
[OF ar_write_le_step_in_sub ar_write_proper_step_in_sub
vM qQ kge2 notlast stg tcorr ppos poskle buf_valid vsrc pad0 src0])
text ‹The unified single-tape write, last tape, re-mirrored into
‹mttm_step (ar_delta_write M)›: as
‹ar_write_tape_step_in_sub› but ‹tk› is the last tape,
so both arms transition to ‹AR_SimAdvance› (current-tape
field reset to ‹k_unidx 0›): the LE arm via
‹ar_write_le_finish_step_in_sub›, the proper arm via
‹ar_write_proper_finish_step_in_sub›. Same tape edit and
head invariance; body transfers verbatim with only the relation
and the two helper references changed.›
lemma ar_write_tape_finish_step_in_sub:
fixes M :: "('q, 'a) mttm"
and c' :: "(sym4, 'q × 'a ar_stage) mt_config"
and tM :: "nat ⇒ 'a"
assumes vM: "valid_mttm M"
and qQ: "q ∈ Q_tm M"
and kge2: "2 ≤ block_width (Γ_tm M)"
and last: "is_last_k M tk"
and stg: "mt_state c' = (q, AR_SimWrite, tk, 0, buf, dvec, posk)"
and tcorr: "ar_tape_correspondence (Γ_tm M) (le_tm M) (bl_tm M)
tM (mt_tape c' tk)"
and ppos: "mt_pos c' tk = (if p = 0 then Suc 0
else sim_pos (block_width (Γ_tm M)) p + block_width (Γ_tm M))"
and poskle: "posk tk = AR_AtLE ⟷ p = 0"
and buf_valid: "∀k. buf k ∈ Γ_tm M ∪ {bl_tm M}"
and vsrc: "ar_valid_stage (Γ_tm M) (bl_tm M)
(AR_SimWrite, tk, 0, buf, dvec, posk)"
and pad0: "∀j ≥ k_tm M. mt_tape c' j (mt_pos c' j) = BLANK4"
and src0: "ar_stage_bounded (bl_tm M) (k_tm M)
(AR_SimWrite, tk, 0, buf, dvec, posk)"
shows "∃c''. (c', c'') ∈ (mttm_step (ar_delta_write M))
^^ (if p = 0 then 1 else 2 * block_width (Γ_tm M))
∧ mt_state c'' = (q, AR_SimAdvance, k_unidx 0, 0, buf, dvec, posk)
∧ mt_tape c'' = (if p = 0 then mt_tape c'
else (mt_tape c')(tk := (λpos.
if sim_pos (block_width (Γ_tm M)) p ≤ pos
∧ pos < sim_pos (block_width (Γ_tm M)) p + block_width (Γ_tm M)
then write_bit (Γ_tm M) (bl_tm M) (buf tk)
(pos - sim_pos (block_width (Γ_tm M)) p)
else mt_tape c' tk pos)))
∧ mt_pos c'' = mt_pos c'"
by (rule ar_write_tape_finish_step_gen
[OF ar_write_le_finish_step_in_sub ar_write_proper_finish_step_in_sub
vM qQ kge2 last stg tcorr ppos poskle buf_valid vsrc pad0 src0])
text ‹The write-phase prefix walk, re-mirrored into
‹mttm_step (ar_delta_write M)›: from the write boundary,
iterate the unified non-last per-tape write
‹ar_write_tape_step_in_sub› over the first ‹j› tapes
(all non-last), landing back at ‹AR_SimWrite› on tape
‹k_unidx j›. The induction on ‹j›, the split tape
descriptor, and the per-tape ‹tcorr›/position bookkeeping
transfer verbatim from the original; only the relation and the
one helper reference change. The internal IH is already over
‹ar_delta_write M›.›
lemma ar_write_prefix_in_sub:
fixes M :: "('q, 'a) mttm"
and cM :: "('a, 'q) mt_config"
and c0 :: "(sym4, 'q × 'a ar_stage) mt_config"
assumes vM: "valid_mttm M"
and qQ: "q ∈ Q_tm M"
and kge2: "2 ≤ block_width (Γ_tm M)"
and stg0: "mt_state c0 = (q, AR_SimWrite, 0, 0, buf, dvec, posk)"
and tcorr: "∀k < k_tm M. ar_tape_correspondence (Γ_tm M) (le_tm M) (bl_tm M)
(mt_tape cM k) (mt_tape c0 k)"
and ppos: "∀k < k_tm M. mt_pos c0 k = (if mt_pos cM k = 0 then Suc 0
else sim_pos (block_width (Γ_tm M)) (mt_pos cM k)
+ block_width (Γ_tm M))"
and poskle: "∀k < k_tm M. posk k = AR_AtLE ⟷ mt_pos cM k = 0"
and buf_valid: "∀k. buf k ∈ Γ_tm M ∪ {bl_tm M}"
and pad0: "∀j ≥ k_tm M. mt_tape c0 j (mt_pos c0 j) = BLANK4"
and src0: "ar_stage_bounded (bl_tm M) (k_tm M)
(AR_SimWrite, 0, 0, buf, dvec, posk)"
shows "j ≤ k_tm M - 1 ⟹
(∃c m. (c0, c) ∈ (mttm_step (ar_delta_write M)) ^^ m
∧ m ≤ j * (2 * block_width (Γ_tm M))
∧ mt_state c = (q, AR_SimWrite, k_unidx j, 0, buf, dvec, posk)
∧ mt_tape c = (λk. if k_idx k < j
then (if mt_pos cM k = 0 then mt_tape c0 k
else (λpos. if sim_pos (block_width (Γ_tm M)) (mt_pos cM k) ≤ pos
∧ pos < sim_pos (block_width (Γ_tm M)) (mt_pos cM k)
+ block_width (Γ_tm M)
then write_bit (Γ_tm M) (bl_tm M) (buf k)
(pos - sim_pos (block_width (Γ_tm M)) (mt_pos cM k))
else mt_tape c0 k pos))
else mt_tape c0 k)
∧ mt_pos c = mt_pos c0)"
by (rule ar_write_prefix_gen
[OF ar_write_tape_step_in_sub vM qQ kge2 stg0 tcorr ppos poskle buf_valid pad0 src0])
text ‹The full write phase, re-mirrored into
‹mttm_step (ar_delta_write M)›: the prefix walk
(‹ar_write_prefix_in_sub›) over the first ‹k_tm M -
1› tapes followed by the unified last-tape write
(‹ar_write_tape_finish_step_in_sub›), landing at
‹AR_SimAdvance› with every proper tape's block overwritten by
‹write_bit (buf k)› and every ‹LE› tape / head
unchanged. Aggregate cost ‹≤ k_tm M ⋅ 2b›. The
split-to-full descriptor collapse, the cardinality bookkeeping, and
the cost bound are relation-agnostic and transfer verbatim; only the
relation and the two helper references change.›
lemma ar_write_phase_in_sub:
fixes M :: "('q, 'a) mttm"
and cM :: "('a, 'q) mt_config"
and c0 :: "(sym4, 'q × 'a ar_stage) mt_config"
assumes vM: "valid_mttm M"
and qQ: "q ∈ Q_tm M"
and kge2: "2 ≤ block_width (Γ_tm M)"
and stg0: "mt_state c0 = (q, AR_SimWrite, 0, 0, buf, dvec, posk)"
and tcorr: "∀k < k_tm M. ar_tape_correspondence (Γ_tm M) (le_tm M) (bl_tm M)
(mt_tape cM k) (mt_tape c0 k)"
and ppos: "∀k < k_tm M. mt_pos c0 k = (if mt_pos cM k = 0 then Suc 0
else sim_pos (block_width (Γ_tm M)) (mt_pos cM k)
+ block_width (Γ_tm M))"
and poskle: "∀k < k_tm M. posk k = AR_AtLE ⟷ mt_pos cM k = 0"
and buf_valid: "∀k. buf k ∈ Γ_tm M ∪ {bl_tm M}"
and pad0: "∀j ≥ k_tm M. mt_tape c0 j (mt_pos c0 j) = BLANK4"
and src0: "ar_stage_bounded (bl_tm M) (k_tm M)
(AR_SimWrite, 0, 0, buf, dvec, posk)"
shows "∃c m. (c0, c) ∈ (mttm_step (ar_delta_write M)) ^^ m
∧ m ≤ k_tm M * (2 * block_width (Γ_tm M))
∧ mt_state c = (q, AR_SimAdvance, k_unidx 0, 0, buf, dvec, posk)
∧ mt_tape c = (λk. if k < k_tm M
then (if mt_pos cM k = 0 then mt_tape c0 k
else (λpos. if sim_pos (block_width (Γ_tm M)) (mt_pos cM k) ≤ pos
∧ pos < sim_pos (block_width (Γ_tm M)) (mt_pos cM k)
+ block_width (Γ_tm M)
then write_bit (Γ_tm M) (bl_tm M) (buf k)
(pos - sim_pos (block_width (Γ_tm M)) (mt_pos cM k))
else mt_tape c0 k pos))
else mt_tape c0 k)
∧ mt_pos c = mt_pos c0"
by (rule ar_write_phase_gen
[OF ar_write_prefix_in_sub ar_write_tape_finish_step_in_sub
vM qQ kge2 stg0 tcorr ppos poskle buf_valid pad0 src0])
text ‹The advance left-walk loop, re-mirrored into
‹mttm_step (ar_delta_advance M)›. From an
‹AR_SimAdvance› stage at bit-counter ‹0›, ‹n›
‹M'›-steps walk the head ‹n› cells ‹L›
(counter ‹0 → n›), tape and other heads unchanged.
The ‹relpow_invariant_chain› loop, the per-step
‹≠ LE4› guard, and the displacement bound
(‹ar_disp_le_2k›) are relation-agnostic and transfer
verbatim; only the relation and the one helper reference change.›
lemma ar_advance_walk_loop_in_sub:
fixes M :: "('q, 'a) mttm"
and c0 :: "(sym4, 'q × 'a ar_stage) mt_config"
assumes vM: "valid_mttm M"
and qQ: "q ∈ Q_tm M"
and stg: "mt_state c0 = (q, AR_SimAdvance, tk, 0, buf, dvec, posk)"
and buf_valid: "∀k. buf k ∈ Γ_tm M ∪ {bl_tm M}"
and ndisp: "n < ar_disp (block_width (Γ_tm M)) (dvec tk) (posk tk)"
and notLE: "⋀j. j < n ⟹ mt_tape c0 tk (mt_pos c0 tk - j) ≠ LE4"
and pad0: "∀j ≥ k_tm M. mt_tape c0 j (mt_pos c0 j) = BLANK4"
and src0: "ar_stage_bounded (bl_tm M) (k_tm M)
(AR_SimAdvance, tk, 0, buf, dvec, posk)"
shows "∃c'. (c0, c') ∈ (mttm_step (ar_delta_advance M)) ^^ n
∧ mt_state c' = (q, AR_SimAdvance, tk, n, buf, dvec, posk)
∧ mt_pos c' tk = mt_pos c0 tk - n
∧ mt_tape c' = mt_tape c0
∧ (∀k'. k' ≠ tk ⟶ mt_pos c' k' = mt_pos c0 k')"
by (rule ar_advance_walk_loop_gen
[OF ar_advance_walk_step_in_sub vM qQ stg buf_valid ndisp notLE pad0 src0])
text ‹The unified single-tape advance, non-last tape, re-mirrored
into ‹mttm_step (ar_delta_advance M)›: the
‹R›/non-‹R› dispatch. An ‹R›-move needs no
head motion (single boundary step, cost ‹1›); a
non-‹R›-move walks the head ‹D = ar_disp› cells
‹L› (the ‹D - 1›-step
‹ar_advance_walk_loop_in_sub› then the final boundary
‹L›-move), landing at ‹start - D›. The
walk-then-boundary decomposition and the conditional head
conclusion transfer verbatim; only the relation and the two helper
references change.›
lemma ar_advance_tape_step_in_sub:
fixes M :: "('q, 'a) mttm"
and c0 :: "(sym4, 'q × 'a ar_stage) mt_config"
assumes vM: "valid_mttm M"
and qQ: "q ∈ Q_tm M"
and kge2: "2 ≤ block_width (Γ_tm M)"
and notlast: "¬ is_last_k M tk"
and stg: "mt_state c0 = (q, AR_SimAdvance, tk, 0, buf, dvec, posk)"
and buf_valid: "∀k. buf k ∈ Γ_tm M ∪ {bl_tm M}"
and dge1: "dvec tk ≠ dir.R
⟹ 0 < ar_disp (block_width (Γ_tm M)) (dvec tk) (posk tk)"
and notLE: "⋀m. m < ar_disp (block_width (Γ_tm M)) (dvec tk) (posk tk)
⟹ mt_tape c0 tk (mt_pos c0 tk - m) ≠ LE4"
and pad0: "∀j ≥ k_tm M. mt_tape c0 j (mt_pos c0 j) = BLANK4"
and src0: "ar_stage_bounded (bl_tm M) (k_tm M)
(AR_SimAdvance, tk, 0, buf, dvec, posk)"
shows "∃c'. (c0, c') ∈ (mttm_step (ar_delta_advance M))
^^ (if dvec tk = dir.R then 1
else ar_disp (block_width (Γ_tm M)) (dvec tk) (posk tk))
∧ mt_state c' = (q, AR_SimAdvance, k_succ tk, 0, buf, dvec,
posk(tk := ar_newpos (dvec tk) (posk tk)))
∧ mt_tape c' = mt_tape c0
∧ mt_pos c' = (if dvec tk = dir.R then mt_pos c0
else (mt_pos c0)(tk := mt_pos c0 tk
- ar_disp (block_width (Γ_tm M)) (dvec tk) (posk tk)))"
by (rule ar_advance_tape_step_gen
[OF ar_advance_walk_loop_in_sub ar_advance_boundary_step_in_sub
vM qQ kge2 notlast stg buf_valid dge1 notLE pad0 src0])
text ‹The unified single-tape advance, last tape, re-mirrored
into ‹mttm_step (ar_delta_advance M)›: as
‹ar_advance_tape_step_in_sub› but ‹tk› is the last
tape, so the boundary step (‹ar_advance_finish_step_in_sub›)
transitions to ‹AR_SimNext› (current-tape field reset to
‹k_unidx 0›) rather than advancing to ‹k_succ tk›.
Same R/non-R dispatch and walk-then-boundary decomposition; only
the relation and the two helper references change.›
lemma ar_advance_tape_finish_step_in_sub:
fixes M :: "('q, 'a) mttm"
and c0 :: "(sym4, 'q × 'a ar_stage) mt_config"
assumes vM: "valid_mttm M"
and qQ: "q ∈ Q_tm M"
and kge2: "2 ≤ block_width (Γ_tm M)"
and last: "is_last_k M tk"
and stg: "mt_state c0 = (q, AR_SimAdvance, tk, 0, buf, dvec, posk)"
and buf_valid: "∀k. buf k ∈ Γ_tm M ∪ {bl_tm M}"
and dge1: "dvec tk ≠ dir.R
⟹ 0 < ar_disp (block_width (Γ_tm M)) (dvec tk) (posk tk)"
and notLE: "⋀m. m < ar_disp (block_width (Γ_tm M)) (dvec tk) (posk tk)
⟹ mt_tape c0 tk (mt_pos c0 tk - m) ≠ LE4"
and pad0: "∀j ≥ k_tm M. mt_tape c0 j (mt_pos c0 j) = BLANK4"
and src0: "ar_stage_bounded (bl_tm M) (k_tm M)
(AR_SimAdvance, tk, 0, buf, dvec, posk)"
shows "∃c'. (c0, c') ∈ (mttm_step (ar_delta_advance M))
^^ (if dvec tk = dir.R then 1
else ar_disp (block_width (Γ_tm M)) (dvec tk) (posk tk))
∧ mt_state c' = (q, AR_SimNext, k_unidx 0, 0, buf, dvec,
posk(tk := ar_newpos (dvec tk) (posk tk)))
∧ mt_tape c' = mt_tape c0
∧ mt_pos c' = (if dvec tk = dir.R then mt_pos c0
else (mt_pos c0)(tk := mt_pos c0 tk
- ar_disp (block_width (Γ_tm M)) (dvec tk) (posk tk)))"
by (rule ar_advance_tape_finish_step_gen
[OF ar_advance_walk_loop_in_sub ar_advance_finish_step_in_sub
vM qQ kge2 last stg buf_valid dge1 notLE pad0 src0])
text ‹The advance prefix walk, re-mirrored into
‹mttm_step (ar_delta_advance M)›: a custom induction on the
tape index ‹j› (‹j ≤ k_tm M - 1›, every tape it
touches non-last), iterating ‹ar_advance_tape_step_in_sub›
from the boundary tape ‹k_unidx 0›. The tape is
constant; the carried state is a ‹k_idx k < j› split over
the ‹posk› and position vectors. The induction, the
descriptor collapse, and the per-tape ‹notLE›/‹dge1›
entry facts are relation-agnostic and transfer verbatim; only the
relation and the one helper reference change.›
lemma ar_advance_prefix_in_sub:
fixes M :: "('q, 'a) mttm"
and c0 :: "(sym4, 'q × 'a ar_stage) mt_config"
assumes vM: "valid_mttm M"
and qQ: "q ∈ Q_tm M"
and kge2: "2 ≤ block_width (Γ_tm M)"
and stg0: "mt_state c0 = (q, AR_SimAdvance, 0, 0, buf0, dvec, posk0)"
and buf_valid: "∀k. buf0 k ∈ Γ_tm M ∪ {bl_tm M}"
and dge1: "∀k < k_tm M. dvec k ≠ dir.R
⟶ 0 < ar_disp (block_width (Γ_tm M)) (dvec k) (posk0 k)"
and notLE: "∀k < k_tm M. ∀m. m < ar_disp (block_width (Γ_tm M)) (dvec k) (posk0 k)
⟶ mt_tape c0 k (mt_pos c0 k - m) ≠ LE4"
and pad0: "∀j ≥ k_tm M. mt_tape c0 j (mt_pos c0 j) = BLANK4"
and src0: "ar_stage_bounded (bl_tm M) (k_tm M)
(AR_SimAdvance, 0, 0, buf0, dvec, posk0)"
shows "j ≤ k_tm M - 1 ⟹
(∃c m. (c0, c) ∈ (mttm_step (ar_delta_advance M)) ^^ m
∧ m ≤ j * (2 * block_width (Γ_tm M))
∧ mt_state c = (q, AR_SimAdvance, k_unidx j, 0, buf0, dvec,
(λk. if k_idx k < j then ar_newpos (dvec k) (posk0 k)
else posk0 k))
∧ mt_tape c = mt_tape c0
∧ mt_pos c = (λk. if k_idx k < j
then (if dvec k = dir.R then mt_pos c0 k
else mt_pos c0 k
- ar_disp (block_width (Γ_tm M)) (dvec k) (posk0 k))
else mt_pos c0 k))"
by (rule ar_advance_prefix_gen
[OF ar_advance_tape_step_in_sub vM qQ kge2 stg0 buf_valid dge1 notLE pad0 src0])
text ‹The full advance phase, re-mirrored into
‹mttm_step (ar_delta_advance M)›: the prefix walk
(‹ar_advance_prefix_in_sub›) over the first
‹k_tm M - 1› tapes followed by the unified last-tape
advance (‹ar_advance_tape_finish_step_in_sub›), landing at
‹AR_SimNext› (current-tape field ‹k_unidx 0›) with
every head moved to ‹M›'s new position and every ‹posk›
updated by ‹ar_newpos›. The tape is unchanged. Aggregate
cost ‹≤ k_tm M ⋅ 2b›. The split-to-full descriptor
collapse and cost bound are relation-agnostic and transfer
verbatim; only the relation and the two helper references
change.›
lemma ar_advance_phase_in_sub:
fixes M :: "('q, 'a) mttm"
and c0 :: "(sym4, 'q × 'a ar_stage) mt_config"
assumes vM: "valid_mttm M"
and qQ: "q ∈ Q_tm M"
and kge2: "2 ≤ block_width (Γ_tm M)"
and stg0: "mt_state c0 = (q, AR_SimAdvance, 0, 0, buf0, dvec, posk0)"
and buf_valid: "∀k. buf0 k ∈ Γ_tm M ∪ {bl_tm M}"
and dge1: "∀k < k_tm M. dvec k ≠ dir.R
⟶ 0 < ar_disp (block_width (Γ_tm M)) (dvec k) (posk0 k)"
and notLE: "∀k < k_tm M. ∀m. m < ar_disp (block_width (Γ_tm M)) (dvec k) (posk0 k)
⟶ mt_tape c0 k (mt_pos c0 k - m) ≠ LE4"
and pad0: "∀j ≥ k_tm M. mt_tape c0 j (mt_pos c0 j) = BLANK4"
and src0: "ar_stage_bounded (bl_tm M) (k_tm M)
(AR_SimAdvance, 0, 0, buf0, dvec, posk0)"
shows "∃c m. (c0, c) ∈ (mttm_step (ar_delta_advance M)) ^^ m
∧ m ≤ k_tm M * (2 * block_width (Γ_tm M))
∧ mt_state c = (q, AR_SimNext, k_unidx 0, 0, buf0, dvec,
(λk. if k < k_tm M then ar_newpos (dvec k) (posk0 k)
else posk0 k))
∧ mt_tape c = mt_tape c0
∧ mt_pos c = (λk. if k < k_tm M
then (if dvec k = dir.R then mt_pos c0 k
else mt_pos c0 k - ar_disp (block_width (Γ_tm M)) (dvec k) (posk0 k))
else mt_pos c0 k)"
by (rule ar_advance_phase_gen
[OF ar_advance_prefix_in_sub ar_advance_tape_finish_step_in_sub
vM qQ kge2 stg0 buf_valid dge1 notLE pad0 src0])
subsection ‹Walker preservation — per-substep M'-step lemmas›
text ‹One preservation lemma per substep predicate: an
‹M'›-step out of a config satisfying the current invariant
lands at a config satisfying the next invariant in the cycle (or
splits the disjunction when the substep's relation has multiple
destination arms). Together with the chunked engine, these
characterise the walker's per-step evolution: the substep idx
carried in the M'-config is the dispatch discriminator at each
step, no chain pinning needed.›
lemma ar_walker_step_from_boundary:
fixes M :: "('q, 'a) mttm"
and cM :: "('a, 'q) mt_config"
and c' c'' :: "(sym4, 'q × 'a ar_stage) mt_config"
assumes inv: "ar_walker_at_boundary M cM c'"
and step: "(c', c'') ∈ mttm_step (alphabet_reduce_delta M)"
shows "ar_walker_in_read M cM c'' ∨ ar_walker_at_compute M cM c''"
proof -
have rbnd: "ar_at_read_boundary M c'"
using inv unfolding ar_walker_at_boundary_def by simp
obtain qM' stg where st: "mt_state c' = (qM', stg)"
by (cases "mt_state c'") auto
obtain idx tk i buf dvec posk where
sg: "stg = (idx, tk, i, buf, dvec, posk)" by (cases stg) auto
have src: "fst (snd (mt_state c')) = AR_SimRead"
proof -
have sim: "ar_simulates M cM c'"
using inv unfolding ar_walker_at_boundary_def by simp
have sim_body:
"((idx = AR_SimRead ∧ qM' ∉ {t_tm M, r_tm M})
∨ (qM' = t_tm M
∧ (idx, tk, i, buf, dvec, posk) = ar_accept_stage (bl_tm M))
∨ (qM' = r_tm M
∧ (idx, tk, i, buf, dvec, posk) = ar_reject_stage (bl_tm M)))
∧ mt_state cM = qM'"
using sim unfolding ar_simulates_def by (simp add: st sg Let_def)
consider (R) "idx = AR_SimRead"
| (A) "qM' = t_tm M ∧ (idx, tk, i, buf, dvec, posk) = ar_accept_stage (bl_tm M)"
| (J) "qM' = r_tm M ∧ (idx, tk, i, buf, dvec, posk) = ar_reject_stage (bl_tm M)"
using sim_body by blast
thus ?thesis
proof cases
case R thus ?thesis using st sg by simp
next
case A
have idx_acc: "idx = AR_HaltAccept"
using A by (simp add: ar_accept_stage_def)
from step obtain S ts n S' aw dir where
c'_eq: "c' = Config⇩M S ts n"
and rel: "(S, (λk. ts k (n k)), S', aw, dir)
∈ alphabet_reduce_delta M"
by (auto elim: mttm_step.cases)
have src_S: "fst (snd S) = AR_HaltAccept"
using c'_eq st sg idx_acc by simp
from alphabet_reduce_delta_src_tag[OF rel]
have "fst (snd S) ∈ {AR_SimRead, AR_SimCompute, AR_SimWrite,
AR_SimAdvance, AR_SimNext}" .
hence False using src_S by auto
thus ?thesis ..
next
case J
have idx_rej: "idx = AR_HaltReject"
using J by (simp add: ar_reject_stage_def)
from step obtain S ts n S' aw dir where
c'_eq: "c' = Config⇩M S ts n"
and rel: "(S, (λk. ts k (n k)), S', aw, dir)
∈ alphabet_reduce_delta M"
by (auto elim: mttm_step.cases)
have src_S: "fst (snd S) = AR_HaltReject"
using c'_eq st sg idx_rej by simp
from alphabet_reduce_delta_src_tag[OF rel]
have "fst (snd S) ∈ {AR_SimRead, AR_SimCompute, AR_SimWrite,
AR_SimAdvance, AR_SimNext}" .
hence False using src_S by auto
thus ?thesis ..
qed
qed
have step_read: "(c', c'') ∈ mttm_step (ar_delta_read M)"
using ar_step_read_lift[OF src step] .
hence step_read1: "(c', c'') ∈ (mttm_step (ar_delta_read M)) ^^ Suc 0"
by simp
from ar_step_from_SimRead_lands[OF step src]
have dest: "fst (snd (mt_state c'')) = AR_SimRead
∨ fst (snd (mt_state c'')) = AR_SimCompute" .
thus ?thesis
proof
assume dr: "fst (snd (mt_state c'')) = AR_SimRead"
have "ar_walker_in_read M cM c''"
unfolding ar_walker_in_read_def
using dr inv step_read1 by blast
thus ?thesis ..
next
assume dc: "fst (snd (mt_state c'')) = AR_SimCompute"
have "ar_walker_at_compute M cM c''"
unfolding ar_walker_at_compute_def
using dc inv step_read1 by blast
thus ?thesis ..
qed
qed
lemma ar_walker_step_from_in_read:
fixes M :: "('q, 'a) mttm"
and cM :: "('a, 'q) mt_config"
and c' c'' :: "(sym4, 'q × 'a ar_stage) mt_config"
assumes inv: "ar_walker_in_read M cM c'"
and step: "(c', c'') ∈ mttm_step (alphabet_reduce_delta M)"
shows "ar_walker_in_read M cM c'' ∨ ar_walker_at_compute M cM c''"
proof -
have src: "fst (snd (mt_state c')) = AR_SimRead"
using inv unfolding ar_walker_in_read_def by simp
obtain c_b m where
wb: "ar_walker_at_boundary M cM c_b"
and chain: "(c_b, c') ∈ (mttm_step (ar_delta_read M)) ^^ m"
using inv unfolding ar_walker_in_read_def by blast
have step_read: "(c', c'') ∈ mttm_step (ar_delta_read M)"
using ar_step_read_lift[OF src step] .
have chain_ext: "(c_b, c'') ∈ (mttm_step (ar_delta_read M)) ^^ Suc m"
using chain step_read by (rule relpow_Suc_I)
from ar_step_from_SimRead_lands[OF step src]
have dest: "fst (snd (mt_state c'')) = AR_SimRead
∨ fst (snd (mt_state c'')) = AR_SimCompute" .
thus ?thesis
proof
assume dr: "fst (snd (mt_state c'')) = AR_SimRead"
have "ar_walker_in_read M cM c''"
unfolding ar_walker_in_read_def
using dr wb chain_ext by blast
thus ?thesis ..
next
assume dc: "fst (snd (mt_state c'')) = AR_SimCompute"
have "ar_walker_at_compute M cM c''"
unfolding ar_walker_at_compute_def
using dc wb chain_ext by blast
thus ?thesis ..
qed
qed
lemma ar_walker_step_from_at_compute:
fixes M :: "('q, 'a) mttm"
and cM :: "('a, 'q) mt_config"
and c' c'' :: "(sym4, 'q × 'a ar_stage) mt_config"
assumes inv: "ar_walker_at_compute M cM c'"
and step: "(c', c'') ∈ mttm_step (alphabet_reduce_delta M)"
and vM: "valid_mttm M"
and qQ: "mt_state cM ∈ Q_tm M"
and kge2: "2 ≤ block_width (Γ_tm M)"
and tapeG: "⋀k. mt_tape cM k (mt_pos cM k) ∈ Γ_tm M"
shows "ar_walker_in_write M cM c''"
proof -
let ?k = "block_width (Γ_tm M)"
let ?aM = "λk. mt_tape cM k (mt_pos cM k)"
have c'_compute: "fst (snd (mt_state c')) = AR_SimCompute"
using inv unfolding ar_walker_at_compute_def by simp
obtain c_b m_w where
wb: "ar_walker_at_boundary M cM c_b"
and chain_w: "(c_b, c') ∈ (mttm_step (ar_delta_read M)) ^^ m_w"
using inv unfolding ar_walker_at_compute_def by blast
have sim: "ar_simulates M cM c_b"
using wb unfolding ar_walker_at_boundary_def by simp
have pcons: "ar_posk_consistent M cM c_b"
using wb unfolding ar_walker_at_boundary_def by simp
have rbnd: "ar_at_read_boundary M c_b"
using wb unfolding ar_walker_at_boundary_def by simp
have cb_idx: "fst (snd (mt_state c_b)) = AR_SimRead"
proof (cases m_w)
case 0
have cb_eq: "c_b = c'" using chain_w 0 by simp
have cb_compute: "fst (snd (mt_state c_b)) = AR_SimCompute"
using c'_compute cb_eq by simp
obtain qM' stg where st_b: "mt_state c_b = (qM', stg)"
by (cases "mt_state c_b") auto
obtain idx tk i buf dvec posk where
sg_b: "stg = (idx, tk, i, buf, dvec, posk)" by (cases stg) auto
have idx_cpu: "idx = AR_SimCompute" using cb_compute st_b sg_b by simp
have "(idx = AR_SimRead ∧ qM' ∉ {t_tm M, r_tm M})
∨ (qM' = t_tm M ∧ stg = ar_accept_stage (bl_tm M))
∨ (qM' = r_tm M ∧ stg = ar_reject_stage (bl_tm M))"
using sim st_b sg_b unfolding ar_simulates_def by (auto split: prod.splits)
hence False
using idx_cpu sg_b
by (auto simp: ar_accept_stage_def ar_reject_stage_def)
thus ?thesis ..
next
case (Suc m')
have hsuc: "(c_b, c') ∈ (mttm_step (ar_delta_read M)) ^^ Suc m'"
using chain_w Suc by simp
obtain c_1 where
first: "(c_b, c_1) ∈ mttm_step (ar_delta_read M)"
using relpow_Suc_D2[OF hsuc] by blast
from first obtain S ts n S' aw dir where
ceq: "c_b = Config⇩M S ts n"
and rel: "(S, (λk. ts k (n k)), S', aw, dir) ∈ ar_delta_read M"
by (auto elim: mttm_step.cases)
have "fst (snd S) = AR_SimRead" using ar_delta_read_src[OF rel] .
thus ?thesis using ceq by simp
qed
obtain qM' stg where st_b: "mt_state c_b = (qM', stg)"
by (cases "mt_state c_b") auto
obtain idx tk i buf dvec posk where
sg_b: "stg = (idx, tk, i, buf, dvec, posk)" by (cases stg) auto
have idx_read: "idx = AR_SimRead" using cb_idx st_b sg_b by simp
have sim_unfold: "(idx = AR_SimRead ∧ qM' ∉ {t_tm M, r_tm M})
∨ (qM' = t_tm M ∧ stg = ar_accept_stage (bl_tm M))
∨ (qM' = r_tm M ∧ stg = ar_reject_stage (bl_tm M))"
using sim st_b sg_b unfolding ar_simulates_def by (auto split: prod.splits)
have qM'_eq: "qM' = mt_state cM"
using sim st_b sg_b unfolding ar_simulates_def by (auto split: prod.splits)
have tcorr: "∀k < k_tm M. ar_tape_correspondence (Γ_tm M) (le_tm M) (bl_tm M)
(mt_tape cM k) (mt_tape c_b k)"
using sim st_b sg_b unfolding ar_simulates_def by (auto split: prod.splits)
have ppos: "⋀k. mt_pos c_b k = sim_pos ?k (mt_pos cM k)"
using sim st_b sg_b idx_read
unfolding ar_simulates_def by (auto split: prod.splits)
have pkok: "⋀k. posk k = AR_AtLE ⟷ mt_pos cM k = 0"
using pcons st_b sg_b idx_read
unfolding ar_posk_consistent_def by (auto split: prod.splits)
have bnd_unfold: "idx = AR_SimRead
⟶ (tk = 0 ∧ i = 0
∧ (∀k. buf k ∈ Γ_tm M ∪ {bl_tm M})
∧ ar_stage_bounded (bl_tm M) (k_tm M)
(idx, tk, i, buf, dvec, posk))"
using rbnd st_b sg_b
unfolding ar_at_read_boundary_def by (auto split: prod.splits)
have tk0: "tk = 0" and i0: "i = 0"
and bufG: "⋀k. buf k ∈ Γ_tm M ∪ {bl_tm M}"
using bnd_unfold idx_read by simp_all
have stg0: "mt_state c_b = (mt_state cM, AR_SimRead, 0, 0, buf, dvec, posk)"
using st_b sg_b qM'_eq idx_read tk0 i0 by simp
have pad0_b: "∀j ≥ k_tm M. mt_tape c_b j (mt_pos c_b j) = BLANK4"
using rbnd unfolding ar_at_read_boundary_def by (auto split: prod.splits)
have src0_b: "ar_stage_bounded (bl_tm M) (k_tm M)
(AR_SimRead, 0, 0, buf, dvec, posk)"
using bnd_unfold idx_read tk0 i0 by simp
obtain c_r m_phase where
r_chain: "(c_b, c_r) ∈ (mttm_step (ar_delta_read M)) ^^ m_phase"
and r_state: "mt_state c_r = (mt_state cM, AR_SimCompute, k_unidx 0, 0,
(λk. if k < k_tm M then ?aM k else buf k), dvec,
(λk. if k < k_tm M
then (if mt_pos cM k = 0 then AR_AtLE
else if mt_pos cM k = 1 then AR_AtFirstProper
else AR_AtFurtherProper)
else posk k))"
using ar_read_phase_in_sub[OF vM qQ kge2 stg0 tcorr ppos pkok tapeG bufG
pad0_b src0_b]
by blast
have r_cpu: "fst (snd (mt_state c_r)) = AR_SimCompute"
using r_state by simp
have c'_eq_c_r: "c' = c_r"
using chain_ar_delta_read_to_SimCompute_uniq[OF chain_w r_chain c'_compute r_cpu]
by simp
have c'_state: "mt_state c' = (mt_state cM, AR_SimCompute, k_unidx 0, 0,
(λk. if k < k_tm M then ?aM k else buf k), dvec,
(λk. if k < k_tm M
then (if mt_pos cM k = 0 then AR_AtLE
else if mt_pos cM k = 1 then AR_AtFirstProper
else AR_AtFurtherProper)
else posk k))"
using c'_eq_c_r r_state by simp
have step_compute: "(c', c'') ∈ mttm_step (ar_delta_compute M)"
using ar_step_compute_lift[OF c'_compute step] .
obtain q' m_a' m_d where
mdelta: "(mt_state cM, (λk. if k < k_tm M then ?aM k else buf k),
q', m_a', m_d) ∈ delta_tm M"
and c''_state: "mt_state c'' = (q', AR_SimWrite, 0, 0, m_a', m_d,
(λk. if k < k_tm M
then (if mt_pos cM k = 0 then AR_AtLE
else if mt_pos cM k = 1 then AR_AtFirstProper
else AR_AtFurtherProper)
else posk k))"
and c''_tape: "mt_tape c'' = mt_tape c'"
and c''_pos: "mt_pos c'' = mt_pos c'"
using ar_compute_step_inv[OF step c'_state] by blast
have c''_write: "fst (snd (mt_state c'')) = AR_SimWrite"
using c''_state by simp
have empty_w: "(c'', c'') ∈ (mttm_step (ar_delta_write M)) ^^ 0" by simp
show "ar_walker_in_write M cM c''"
unfolding ar_walker_in_write_def
proof (intro conjI)
show "fst (snd (mt_state c'')) = AR_SimWrite" by (rule c''_write)
show "∃c_b c_w m_r m_w.
ar_walker_at_boundary M cM c_b
∧ (c_b, c_w) ∈ (mttm_step (ar_delta_read M)) ^^ m_r
∧ fst (snd (mt_state c_w)) = AR_SimCompute
∧ (∃c_w_post. (c_w, c_w_post) ∈ mttm_step (ar_delta_compute M)
∧ (c_w_post, c'') ∈ (mttm_step (ar_delta_write M)) ^^ m_w)"
by (intro exI[where x = c_b] exI[where x = c'] exI[where x = m_w]
exI[where x = 0] conjI wb chain_w c'_compute
exI[where x = c''] step_compute empty_w)
qed
qed
lemma ar_walker_step_from_in_write:
fixes M :: "('q, 'a) mttm"
and cM :: "('a, 'q) mt_config"
and c' c'' :: "(sym4, 'q × 'a ar_stage) mt_config"
assumes inv: "ar_walker_in_write M cM c'"
and step: "(c', c'') ∈ mttm_step (alphabet_reduce_delta M)"
shows "ar_walker_in_write M cM c'' ∨ ar_walker_in_advance M cM c''"
proof -
have src: "fst (snd (mt_state c')) = AR_SimWrite"
using inv unfolding ar_walker_in_write_def by simp
obtain c_b c_w m_r m_w where
wb: "ar_walker_at_boundary M cM c_b"
and chr: "(c_b, c_w) ∈ (mttm_step (ar_delta_read M)) ^^ m_r"
and cwC: "fst (snd (mt_state c_w)) = AR_SimCompute"
and rest: "∃c_w_post. (c_w, c_w_post) ∈ mttm_step (ar_delta_compute M)
∧ (c_w_post, c') ∈ (mttm_step (ar_delta_write M)) ^^ m_w"
using inv unfolding ar_walker_in_write_def by blast
obtain c_w_post where
ccs: "(c_w, c_w_post) ∈ mttm_step (ar_delta_compute M)"
and chw: "(c_w_post, c') ∈ (mttm_step (ar_delta_write M)) ^^ m_w"
using rest by blast
have step_write: "(c', c'') ∈ mttm_step (ar_delta_write M)"
using ar_step_write_lift[OF src step] .
have chw_ext: "(c_w_post, c'') ∈ (mttm_step (ar_delta_write M)) ^^ Suc m_w"
using chw step_write by (rule relpow_Suc_I)
from ar_step_from_SimWrite_lands[OF step src]
have dest: "fst (snd (mt_state c'')) = AR_SimWrite
∨ fst (snd (mt_state c'')) = AR_SimAdvance" .
thus ?thesis
proof
assume dw: "fst (snd (mt_state c'')) = AR_SimWrite"
have "ar_walker_in_write M cM c''"
unfolding ar_walker_in_write_def
proof (intro conjI)
show "fst (snd (mt_state c'')) = AR_SimWrite" by (rule dw)
show "∃c_b c_w m_r m_w.
ar_walker_at_boundary M cM c_b
∧ (c_b, c_w) ∈ (mttm_step (ar_delta_read M)) ^^ m_r
∧ fst (snd (mt_state c_w)) = AR_SimCompute
∧ (∃c_w_post.
(c_w, c_w_post) ∈ mttm_step (ar_delta_compute M)
∧ (c_w_post, c'') ∈ (mttm_step (ar_delta_write M)) ^^ m_w)"
by (intro exI[where x = c_b] exI[where x = c_w] exI[where x = m_r]
exI[where x = "Suc m_w"] conjI wb chr cwC
exI[where x = c_w_post] ccs chw_ext)
qed
thus ?thesis ..
next
assume da: "fst (snd (mt_state c'')) = AR_SimAdvance"
have empty_a: "(c'', c'') ∈ (mttm_step (ar_delta_advance M)) ^^ 0"
by simp
have "ar_walker_in_advance M cM c''"
unfolding ar_walker_in_advance_def
proof (intro conjI)
show "fst (snd (mt_state c'')) = AR_SimAdvance" by (rule da)
show "∃c_b c_w c_a m_r m_w m_a.
ar_walker_at_boundary M cM c_b
∧ (c_b, c_w) ∈ (mttm_step (ar_delta_read M)) ^^ m_r
∧ fst (snd (mt_state c_w)) = AR_SimCompute
∧ fst (snd (mt_state c_a)) = AR_SimAdvance
∧ (∃c_w_post.
(c_w, c_w_post) ∈ mttm_step (ar_delta_compute M)
∧ (c_w_post, c_a) ∈ (mttm_step (ar_delta_write M)) ^^ m_w
∧ (c_a, c'') ∈ (mttm_step (ar_delta_advance M)) ^^ m_a)"
by (intro exI[where x = c_b] exI[where x = c_w] exI[where x = c'']
exI[where x = m_r] exI[where x = "Suc m_w"] exI[where x = 0]
conjI wb chr cwC da
exI[where x = c_w_post] ccs chw_ext empty_a)
qed
thus ?thesis ..
qed
qed
lemma ar_walker_step_from_in_advance:
fixes M :: "('q, 'a) mttm"
and cM :: "('a, 'q) mt_config"
and c' c'' :: "(sym4, 'q × 'a ar_stage) mt_config"
assumes inv: "ar_walker_in_advance M cM c'"
and step: "(c', c'') ∈ mttm_step (alphabet_reduce_delta M)"
shows "ar_walker_in_advance M cM c'' ∨ ar_walker_at_next M cM c''"
proof -
have src: "fst (snd (mt_state c')) = AR_SimAdvance"
using inv unfolding ar_walker_in_advance_def by simp
obtain c_b c_w c_a m_r m_w m_a where
wb: "ar_walker_at_boundary M cM c_b"
and chr: "(c_b, c_w) ∈ (mttm_step (ar_delta_read M)) ^^ m_r"
and cwC: "fst (snd (mt_state c_w)) = AR_SimCompute"
and caC: "fst (snd (mt_state c_a)) = AR_SimAdvance"
and rest: "∃c_w_post.
(c_w, c_w_post) ∈ mttm_step (ar_delta_compute M)
∧ (c_w_post, c_a) ∈ (mttm_step (ar_delta_write M)) ^^ m_w
∧ (c_a, c') ∈ (mttm_step (ar_delta_advance M)) ^^ m_a"
using inv unfolding ar_walker_in_advance_def by blast
obtain c_w_post where
ccs: "(c_w, c_w_post) ∈ mttm_step (ar_delta_compute M)"
and chw: "(c_w_post, c_a) ∈ (mttm_step (ar_delta_write M)) ^^ m_w"
and cha: "(c_a, c') ∈ (mttm_step (ar_delta_advance M)) ^^ m_a"
using rest by blast
have step_advance: "(c', c'') ∈ mttm_step (ar_delta_advance M)"
using ar_step_advance_lift[OF src step] .
have cha_ext: "(c_a, c'') ∈ (mttm_step (ar_delta_advance M)) ^^ Suc m_a"
using cha step_advance by (rule relpow_Suc_I)
from ar_step_from_SimAdvance_lands[OF step src]
have dest: "fst (snd (mt_state c'')) = AR_SimAdvance
∨ fst (snd (mt_state c'')) = AR_SimNext" .
thus ?thesis
proof
assume da: "fst (snd (mt_state c'')) = AR_SimAdvance"
have "ar_walker_in_advance M cM c''"
unfolding ar_walker_in_advance_def
proof (intro conjI)
show "fst (snd (mt_state c'')) = AR_SimAdvance" by (rule da)
show "∃c_b c_w c_a m_r m_w m_a.
ar_walker_at_boundary M cM c_b
∧ (c_b, c_w) ∈ (mttm_step (ar_delta_read M)) ^^ m_r
∧ fst (snd (mt_state c_w)) = AR_SimCompute
∧ fst (snd (mt_state c_a)) = AR_SimAdvance
∧ (∃c_w_post.
(c_w, c_w_post) ∈ mttm_step (ar_delta_compute M)
∧ (c_w_post, c_a) ∈ (mttm_step (ar_delta_write M)) ^^ m_w
∧ (c_a, c'') ∈ (mttm_step (ar_delta_advance M)) ^^ m_a)"
by (intro exI[where x = c_b] exI[where x = c_w] exI[where x = c_a]
exI[where x = m_r] exI[where x = m_w] exI[where x = "Suc m_a"]
conjI wb chr cwC caC
exI[where x = c_w_post] ccs chw cha_ext)
qed
thus ?thesis ..
next
assume dn: "fst (snd (mt_state c'')) = AR_SimNext"
have "ar_walker_at_next M cM c''"
unfolding ar_walker_at_next_def
proof (intro conjI)
show "fst (snd (mt_state c'')) = AR_SimNext" by (rule dn)
show "∃c_b c_w c_a c_n m_r m_w m_a.
ar_walker_at_boundary M cM c_b
∧ (c_b, c_w) ∈ (mttm_step (ar_delta_read M)) ^^ m_r
∧ fst (snd (mt_state c_w)) = AR_SimCompute
∧ fst (snd (mt_state c_a)) = AR_SimAdvance
∧ (∃c_w_post.
(c_w, c_w_post) ∈ mttm_step (ar_delta_compute M)
∧ (c_w_post, c_a) ∈ (mttm_step (ar_delta_write M)) ^^ m_w
∧ (c_a, c_n) ∈ (mttm_step (ar_delta_advance M)) ^^ m_a
∧ c_n = c'')"
by (intro exI[where x = c_b] exI[where x = c_w] exI[where x = c_a]
exI[where x = c''] exI[where x = m_r] exI[where x = m_w]
exI[where x = "Suc m_a"] conjI wb chr cwC caC
exI[where x = c_w_post] ccs chw cha_ext refl)
qed
thus ?thesis ..
qed
qed
text ‹The sixth and final substep preservation closes the
walker suite mechanically: an ‹M'›-step out of
‹AR_SimNext› lands at ‹AR_SimRead› (cycle close),
‹AR_HaltAccept›, or ‹AR_HaltReject› by
‹ar_step_from_SimNext_lands›. This is a pure dispatch
lemma — establishing the boundary for the reconstructed
‹M›-successor at a cycle close is a separate cycle-level
concern handled by ‹ar_walker_cycle_close› and the chunked
reverse engine. Keeping the ‹at_next› walker preservation
thin keeps the suite uniform — all six are one-substep
mechanical lemmas. Itself currently uncalled — the cycle close runs
through ‹ar_walker_cycle_close› directly — kept to complete the
six-member walker-preservation suite.›
lemma ar_walker_step_from_at_next:
fixes M :: "('q, 'a) mttm"
and cM :: "('a, 'q) mt_config"
and c' c'' :: "(sym4, 'q × 'a ar_stage) mt_config"
assumes inv: "ar_walker_at_next M cM c'"
and step: "(c', c'') ∈ mttm_step (alphabet_reduce_delta M)"
shows "fst (snd (mt_state c'')) = AR_SimRead
∨ fst (snd (mt_state c'')) = AR_HaltAccept
∨ fst (snd (mt_state c'')) = AR_HaltReject"
proof -
have src: "fst (snd (mt_state c')) = AR_SimNext"
using inv unfolding ar_walker_at_next_def by simp
show ?thesis using ar_step_from_SimNext_lands[OF step src] .
qed
subsection ‹Cycle-close bridging lemma›
text ‹An ‹AR_SimNext› step closes a simulation cycle: the walker is
re-established at a boundary for the next ‹M›-configuration. The
successor is ∗‹reconstructed› from the pinned compute branch
(the ‹∃cM'› in the conclusion): under nondeterministic
‹delta_tm M› the source ‹cM› may have several successors, so the
fired branch is recovered from the walker's own witness chain rather
than assumed. The forward
arm is rebuilt entirely over the substep sub-relations and each walker
witness chain is pinned by a ‹chain_ar_delta_X_to_Y_uniq› suite.
The closing next step is inverted by ‹ar_next_step_inv›, which
dispatches on the reconstructed ‹M›-state ‹q'› into three
outcomes: continue (‹q' ∉ {t, r}›, landing at ‹AR_SimRead›),
accept (‹q' = t_tm M›) or reject (‹q' = r_tm M›). All three
re-establish ‹ar_walker_at_boundary M cMn c''›: the boundary
invariant carries the halt cases too — ‹ar_simulates›'s state
disjunction has dedicated accept/reject arms, and both
‹ar_posk_consistent› and ‹ar_at_read_boundary› are
‹AR_SimRead›-guarded, hence vacuous off the read boundary. The
three predicates are discharged from the explicit endpoint by the shared
semantic lemmas (‹ar_write_tape_correspondence›,
‹ar_advance_newsimpos›, ‹ar_newpos_atLE_iff›). No union chain
is pinned and ‹ar_simulates_forward_step› is not invoked.›
lemma ar_walker_cycle_close:
fixes M :: "('q, 'a) mttm"
and w :: "'a list"
and cM :: "('a, 'q) mt_config"
and c' c'' :: "(sym4, 'q × 'a ar_stage) mt_config"
assumes inv: "ar_walker_at_next M cM c'"
and step: "(c', c'') ∈ mttm_step (alphabet_reduce_delta M)"
and vM: "valid_mttm M"
and qQ: "mt_state cM ∈ Q_tm M"
and kge2: "2 ≤ block_width (Γ_tm M)"
and tapeG: "⋀k. mt_tape cM k (mt_pos cM k) ∈ Γ_tm M"
and w_sub: "set w ⊆ Sigma_tm M"
and reach_M: "(init_config_mttm M w, cM) ∈ (mttm_step (delta_tm M))⇧*"
and lebl: "le_tm M ≠ bl_tm M"
shows "∃cM'. (cM, cM') ∈ mttm_step (delta_tm M)
∧ ar_walker_at_boundary M cM' c''"
proof -
let ?k = "block_width (Γ_tm M)"
let ?aM = "λk. mt_tape cM k (mt_pos cM k)"
have kpos_tm: "0 < k_tm M" using vM by (cases M) auto
obtain c_b c_w c_a c_n m_r m_w m_a c_w_post where
wb: "ar_walker_at_boundary M cM c_b"
and chain_r: "(c_b, c_w) ∈ (mttm_step (ar_delta_read M)) ^^ m_r"
and cw_cpu: "fst (snd (mt_state c_w)) = AR_SimCompute"
and ca_adv: "fst (snd (mt_state c_a)) = AR_SimAdvance"
and cstep: "(c_w, c_w_post) ∈ mttm_step (ar_delta_compute M)"
and wchain: "(c_w_post, c_a) ∈ (mttm_step (ar_delta_write M)) ^^ m_w"
and achain0: "(c_a, c_n) ∈ (mttm_step (ar_delta_advance M)) ^^ m_a"
and cn_eq: "c_n = c'"
using inv unfolding ar_walker_at_next_def by blast
have achain: "(c_a, c') ∈ (mttm_step (ar_delta_advance M)) ^^ m_a"
using achain0 cn_eq by simp
have c'_next: "fst (snd (mt_state c')) = AR_SimNext"
using inv unfolding ar_walker_at_next_def by simp
have sim: "ar_simulates M cM c_b"
using wb unfolding ar_walker_at_boundary_def by simp
have pcons: "ar_posk_consistent M cM c_b"
using wb unfolding ar_walker_at_boundary_def by simp
have rbnd: "ar_at_read_boundary M c_b"
using wb unfolding ar_walker_at_boundary_def by simp
have cb_idx: "fst (snd (mt_state c_b)) = AR_SimRead"
proof (cases m_r)
case 0
have cb_eq: "c_b = c_w" using chain_r 0 by simp
have cb_compute: "fst (snd (mt_state c_b)) = AR_SimCompute"
using cw_cpu cb_eq by simp
obtain qM' stg where st_b: "mt_state c_b = (qM', stg)"
by (cases "mt_state c_b") auto
obtain idx tk i buf dvec posk where
sg_b: "stg = (idx, tk, i, buf, dvec, posk)" by (cases stg) auto
have idx_cpu: "idx = AR_SimCompute" using cb_compute st_b sg_b by simp
have "(idx = AR_SimRead ∧ qM' ∉ {t_tm M, r_tm M})
∨ (qM' = t_tm M ∧ stg = ar_accept_stage (bl_tm M))
∨ (qM' = r_tm M ∧ stg = ar_reject_stage (bl_tm M))"
using sim st_b sg_b unfolding ar_simulates_def by (auto split: prod.splits)
hence False using idx_cpu sg_b
by (auto simp: ar_accept_stage_def ar_reject_stage_def)
thus ?thesis ..
next
case (Suc m')
have hsuc: "(c_b, c_w) ∈ (mttm_step (ar_delta_read M)) ^^ Suc m'"
using chain_r Suc by simp
obtain c_1 where first: "(c_b, c_1) ∈ mttm_step (ar_delta_read M)"
using relpow_Suc_D2[OF hsuc] by blast
from first obtain S ts n S' aw dir where
ceq: "c_b = Config⇩M S ts n"
and rel: "(S, (λk. ts k (n k)), S', aw, dir) ∈ ar_delta_read M"
by (auto elim: mttm_step.cases)
have "fst (snd S) = AR_SimRead" using ar_delta_read_src[OF rel] .
thus ?thesis using ceq by simp
qed
obtain qM' stg where st_b: "mt_state c_b = (qM', stg)"
by (cases "mt_state c_b") auto
obtain idx tk i buf dvec posk where
sg_b: "stg = (idx, tk, i, buf, dvec, posk)" by (cases stg) auto
have idx_read: "idx = AR_SimRead" using cb_idx st_b sg_b by simp
have qM'_eq: "qM' = mt_state cM"
using sim st_b sg_b unfolding ar_simulates_def by (auto split: prod.splits)
have tcorr: "∀k < k_tm M. ar_tape_correspondence (Γ_tm M) (le_tm M) (bl_tm M)
(mt_tape cM k) (mt_tape c_b k)"
using sim st_b sg_b unfolding ar_simulates_def by (auto split: prod.splits)
have ppos: "⋀k. mt_pos c_b k = sim_pos ?k (mt_pos cM k)"
using sim st_b sg_b idx_read
unfolding ar_simulates_def by (auto split: prod.splits)
have pkok: "⋀k. posk k = AR_AtLE ⟷ mt_pos cM k = 0"
using pcons st_b sg_b idx_read
unfolding ar_posk_consistent_def by (auto split: prod.splits)
have bnd_unfold: "idx = AR_SimRead
⟶ (tk = 0 ∧ i = 0
∧ (∀k. buf k ∈ Γ_tm M ∪ {bl_tm M})
∧ ar_stage_bounded (bl_tm M) (k_tm M)
(idx, tk, i, buf, dvec, posk))"
using rbnd st_b sg_b
unfolding ar_at_read_boundary_def by (auto split: prod.splits)
have tk0: "tk = 0" and i0: "i = 0"
and bufG: "⋀k. buf k ∈ Γ_tm M ∪ {bl_tm M}"
using bnd_unfold idx_read by simp_all
have src_b: "ar_stage_bounded (bl_tm M) (k_tm M)
(AR_SimRead, 0, 0, buf, dvec, posk)"
using bnd_unfold idx_read tk0 i0 by simp
have pad_b: "∀j ≥ k_tm M. mt_tape c_b j (mt_pos c_b j) = BLANK4"
using rbnd unfolding ar_at_read_boundary_def by (auto split: prod.splits)
have stg0: "mt_state c_b = (mt_state cM, AR_SimRead, 0, 0, buf, dvec, posk)"
using st_b sg_b qM'_eq idx_read tk0 i0 by simp
have buf_tail: "∀j ≥ k_tm M. buf j = bl_tm M"
using src_b by (simp add: ar_stage_bounded_def)
have dvec_tail: "∀j ≥ k_tm M. dvec j = dir.N"
using src_b by (simp add: ar_stage_bounded_def)
have posk_tail: "∀j ≥ k_tm M. posk j = AR_AtLE"
using src_b by (simp add: ar_stage_bounded_def)
have valcM: "valid_config_mttm M cM"
using valid_reach_mttm[OF vM w_sub reach_M] .
have aM_tail: "∀j ≥ k_tm M. mt_tape cM j (mt_pos cM j) = bl_tm M"
using valid_config_mttm_blank_tail[OF valcM] by blast
let ?rbuf = "λk. if k < k_tm M then ?aM k else buf k"
let ?rposk = "λk. if k < k_tm M
then (if mt_pos cM k = 0 then AR_AtLE
else if mt_pos cM k = 1 then AR_AtFirstProper
else AR_AtFurtherProper)
else posk k"
let ?rpos = "λk. if k < k_tm M
then (if mt_pos cM k = 0 then Suc 0
else sim_pos ?k (mt_pos cM k) + ?k)
else mt_pos c_b k"
obtain c_r m_phase where
r_chain: "(c_b, c_r) ∈ (mttm_step (ar_delta_read M)) ^^ m_phase"
and r_state: "mt_state c_r = (mt_state cM, AR_SimCompute, k_unidx 0, 0,
?rbuf, dvec, ?rposk)"
and r_tape: "mt_tape c_r = mt_tape c_b"
and r_pos: "mt_pos c_r = ?rpos"
using ar_read_phase_in_sub[OF vM qQ kge2 stg0 tcorr ppos pkok tapeG bufG
pad_b src_b]
by blast
have r_cpu: "fst (snd (mt_state c_r)) = AR_SimCompute" using r_state by simp
have cw_eq_cr: "c_w = c_r"
using chain_ar_delta_read_to_SimCompute_uniq[OF chain_r r_chain cw_cpu r_cpu]
by simp
have cw_state: "mt_state c_w = (mt_state cM, AR_SimCompute, k_unidx 0, 0,
?rbuf, dvec, ?rposk)"
using cw_eq_cr r_state by simp
obtain q' m_a' m_d where
mdelta: "(mt_state cM, ?rbuf, q', m_a', m_d) ∈ delta_tm M"
and cwpost_state: "mt_state c_w_post = (q', AR_SimWrite, 0, 0, m_a', m_d, ?rposk)"
and cwpost_tape: "mt_tape c_w_post = mt_tape c_w"
and cwpost_pos: "mt_pos c_w_post = mt_pos c_w"
using ar_compute_step_inv_sub[OF cstep cw_state] by blast
obtain qM tsM nM where cM_eq: "cM = Config⇩M qM tsM nM" by (cases cM) auto
have qM_eq: "qM = mt_state cM" using cM_eq by simp
have aM_eq: "(λk. tsM k (nM k)) = ?aM" using cM_eq by simp
have rbuf_eq: "?rbuf = ?aM"
proof (rule ext)
fix k show "?rbuf k = ?aM k"
proof (cases "k < k_tm M")
case True thus ?thesis by simp
next
case False
have "?rbuf k = bl_tm M" using buf_tail False by simp
moreover have "?aM k = bl_tm M" using aM_tail False by simp
ultimately show ?thesis by simp
qed
qed
have mdelta_aM: "(mt_state cM, ?aM, q', m_a', m_d) ∈ delta_tm M"
using mdelta rbuf_eq by simp
define cMn where cMn_def: "cMn = Config⇩M q' (λk. (tsM k)(nM k := m_a' k))
(λk. go_dir (m_d k) (nM k))"
have mdelta': "(qM, (λk. tsM k (nM k)), q', m_a', m_d) ∈ delta_tm M"
using mdelta_aM qM_eq aM_eq by simp
have m_step: "(cM, cMn) ∈ mttm_step (delta_tm M)"
using mttm_step.step[where ts = tsM and n = nM, OF mdelta'] cM_eq cMn_def by simp
have q'Q: "q' ∈ Q_tm M" using valid_mttm_delta(3)[OF vM mdelta_aM] .
have a'G: "m_a' k ∈ Γ_tm M" for k using valid_mttm_delta(4)[OF vM mdelta_aM] .
have a'val: "∀k. m_a' k ∈ Γ_tm M ∪ {bl_tm M}" using a'G by blast
have dsupp: "∀j ≥ k_tm M. m_a' j = bl_tm M ∧ m_d j = dir.N"
using valid_mttm_delta_support[OF vM mdelta_aM] by blast
have pad_cwpost: "∀j ≥ k_tm M. mt_tape c_w_post j (mt_pos c_w_post j) = BLANK4"
proof (intro allI impI)
fix j assume jk: "k_tm M ≤ j"
have "mt_pos c_w_post j = mt_pos c_b j"
using cwpost_pos cw_eq_cr r_pos jk by simp
moreover have "mt_tape c_w_post j = mt_tape c_b j"
using cwpost_tape cw_eq_cr r_tape by simp
ultimately show "mt_tape c_w_post j (mt_pos c_w_post j) = BLANK4"
using pad_b jk by simp
qed
have src_cwpost: "ar_stage_bounded (bl_tm M) (k_tm M)
(AR_SimWrite, 0, 0, m_a', m_d, ?rposk)"
using kpos_tm dsupp posk_tail by (simp add: ar_stage_bounded_def)
have tcorr_w: "∀k < k_tm M. ar_tape_correspondence (Γ_tm M) (le_tm M) (bl_tm M)
(mt_tape cM k) (mt_tape c_w_post k)"
proof (intro allI impI)
fix k assume kN: "k < k_tm M"
have "mt_tape c_w_post k = mt_tape c_b k"
using cwpost_tape cw_eq_cr r_tape by simp
thus "ar_tape_correspondence (Γ_tm M) (le_tm M) (bl_tm M)
(mt_tape cM k) (mt_tape c_w_post k)"
using tcorr kN by simp
qed
have ppos_w: "∀k < k_tm M. mt_pos c_w_post k = (if mt_pos cM k = 0 then Suc 0
else sim_pos ?k (mt_pos cM k) + ?k)"
using cwpost_pos cw_eq_cr r_pos by simp
have a'le0_w: "∀k < k_tm M. mt_pos cM k = 0 ⟶ m_a' k = le_tm M"
proof (intro allI impI)
fix k assume kN: "k < k_tm M" and p0: "mt_pos cM k = 0"
have tsk0: "tsM k 0 = le_tm M" using valcM cM_eq kN by (cases M) auto
have "(λj. tsM j (nM j)) k = le_tm M" using tsk0 p0 cM_eq by simp
thus "m_a' k = le_tm M" using valid_mttm_deltaLE[OF vM mdelta'] by simp
qed
have poskle_w: "∀k < k_tm M. ?rposk k = AR_AtLE ⟷ mt_pos cM k = 0"
by auto
obtain c_write mw where
w_chain: "(c_w_post, c_write) ∈ (mttm_step (ar_delta_write M)) ^^ mw"
and w_state: "mt_state c_write = (q', AR_SimAdvance, k_unidx 0, 0, m_a', m_d,
?rposk)"
and w_tape: "mt_tape c_write = (λk. if k < k_tm M
then (if mt_pos cM k = 0 then mt_tape c_w_post k
else (λpos. if sim_pos ?k (mt_pos cM k) ≤ pos
∧ pos < sim_pos ?k (mt_pos cM k) + ?k
then write_bit (Γ_tm M) (bl_tm M) (m_a' k)
(pos - sim_pos ?k (mt_pos cM k))
else mt_tape c_w_post k pos))
else mt_tape c_w_post k)"
and w_pos: "mt_pos c_write = mt_pos c_w_post"
using ar_write_phase_in_sub[OF vM q'Q kge2 cwpost_state tcorr_w ppos_w
poskle_w a'val pad_cwpost src_cwpost]
by blast
have c_write_adv: "fst (snd (mt_state c_write)) = AR_SimAdvance"
using w_state by simp
have ca_eq: "c_a = c_write"
using chain_ar_delta_write_to_SimAdvance_uniq[OF wchain w_chain ca_adv
c_write_adv]
by simp
have w_state': "mt_state c_write = (q', AR_SimAdvance, 0, 0, m_a', m_d, ?rposk)"
using w_state by (simp add: k_unidx_zero)
have pad_cwrite: "∀j ≥ k_tm M. mt_tape c_write j (mt_pos c_write j) = BLANK4"
proof (intro allI impI)
fix j assume jk: "k_tm M ≤ j"
have "mt_tape c_write j = mt_tape c_w_post j" using w_tape jk by simp
moreover have "mt_pos c_write j = mt_pos c_w_post j" using w_pos by simp
ultimately show "mt_tape c_write j (mt_pos c_write j) = BLANK4"
using pad_cwpost jk by simp
qed
have src_cwrite: "ar_stage_bounded (bl_tm M) (k_tm M)
(AR_SimAdvance, 0, 0, m_a', m_d, ?rposk)"
using kpos_tm dsupp posk_tail by (simp add: ar_stage_bounded_def)
have dge1: "∀k < k_tm M. m_d k ≠ dir.R ⟶ 0 < ar_disp ?k (m_d k) (?rposk k)"
proof (intro allI impI)
fix k assume kN: "k < k_tm M" and dkR: "m_d k ≠ dir.R"
show "0 < ar_disp ?k (m_d k) (?rposk k)"
proof (cases "mt_pos cM k = 0")
case True
have nM0: "nM k = 0" using True cM_eq by simp
have "tsM k 0 = le_tm M" using valcM cM_eq kN by (cases M) auto
hence "(λj. tsM j (nM j)) k = le_tm M" using nM0 by simp
hence "m_d k ∈ {dir.N, dir.R}" using valid_mttm_deltaLE[OF vM mdelta'] by simp
hence "m_d k = dir.N" using dkR by auto
moreover have "?rposk k = AR_AtLE" using True kN by simp
ultimately show "0 < ar_disp ?k (m_d k) (?rposk k)" by simp
next
case False
have dN_or_L: "m_d k = dir.N ∨ m_d k = dir.L"
using dkR by (cases "m_d k") auto
have rk: "?rposk k = AR_AtFirstProper ∨ ?rposk k = AR_AtFurtherProper"
using False kN by auto
from dN_or_L rk kge2 show "0 < ar_disp ?k (m_d k) (?rposk k)" by auto
qed
qed
have notLE: "∀k < k_tm M. ∀m. m < ar_disp ?k (m_d k) (?rposk k)
⟶ mt_tape c_write k (mt_pos c_write k - m) ≠ LE4"
proof (intro allI impI)
fix k m assume kN: "k < k_tm M"
and mlt: "m < ar_disp ?k (m_d k) (?rposk k)"
have tcorr_wk: "ar_tape_correspondence (Γ_tm M) (le_tm M) (bl_tm M)
(mt_tape cM k) (mt_tape c_w_post k)"
using tcorr_w kN by blast
have wcpos: "mt_pos c_write k = (if mt_pos cM k = 0 then Suc 0
else sim_pos ?k (mt_pos cM k) + ?k)"
using w_pos ppos_w kN by simp
have wtape_notLE: "mt_tape c_write k pos ≠ LE4" if pos1: "1 ≤ pos" for pos
proof (cases "mt_pos cM k = 0")
case True
have "mt_tape c_write k pos = mt_tape c_w_post k pos"
using w_tape True kN by simp
thus ?thesis
using ar_tape_correspondence_not_LE4[OF tcorr_wk pos1] by simp
next
case False
have wexp: "mt_tape c_write k pos
= (if sim_pos ?k (mt_pos cM k) ≤ pos
∧ pos < sim_pos ?k (mt_pos cM k) + ?k
then write_bit (Γ_tm M) (bl_tm M) (m_a' k)
(pos - sim_pos ?k (mt_pos cM k))
else mt_tape c_w_post k pos)"
using w_tape False kN by simp
show ?thesis
proof (cases "sim_pos ?k (mt_pos cM k) ≤ pos
∧ pos < sim_pos ?k (mt_pos cM k) + ?k")
case True
have b: "pos - sim_pos ?k (mt_pos cM k) < ?k" using True by linarith
have "mt_tape c_write k pos
= write_bit (Γ_tm M) (bl_tm M) (m_a' k)
(pos - sim_pos ?k (mt_pos cM k))"
using wexp True by simp
thus ?thesis using write_bit_not_LE4[OF b] by simp
next
case False
have nreg: "¬ (sim_pos ?k (mt_pos cM k) ≤ pos
∧ pos < sim_pos ?k (mt_pos cM k) + ?k)"
using False by simp
have "mt_tape c_write k pos = mt_tape c_w_post k pos"
using wexp by (simp add: if_not_P[OF nreg])
thus ?thesis
using ar_tape_correspondence_not_LE4[OF tcorr_wk pos1] by simp
qed
qed
have rge: "ar_disp ?k (m_d k) (?rposk k) ≤ mt_pos c_write k"
proof (cases "mt_pos cM k = 0")
case True
have "ar_disp ?k (m_d k) (?rposk k) ≤ Suc 0"
using True kN by (cases "m_d k") auto
thus ?thesis using wcpos True by simp
next
case nz: False
show ?thesis
proof (cases "mt_pos cM k = 1")
case True
have "ar_disp ?k (m_d k) (?rposk k) ≤ Suc ?k"
using True kN by (cases "m_d k") auto
thus ?thesis using wcpos True by (simp add: sim_pos_def)
next
case False
have p2: "2 ≤ mt_pos cM k" using nz False by simp
have d2: "ar_disp ?k (m_d k) (?rposk k) ≤ 2 * ?k"
using nz False kN by (cases "m_d k") auto
have cw_eq2: "mt_pos c_write k = (mt_pos cM k - 1) * ?k + 1 + ?k"
using wcpos nz by (simp add: sim_pos_def)
have "(1::nat) ≤ mt_pos cM k - 1" using p2 by simp
hence "1 * ?k ≤ (mt_pos cM k - 1) * ?k" by (rule mult_le_mono1)
hence kk: "?k ≤ (mt_pos cM k - 1) * ?k" by (simp only: mult_1_left)
have "2 * ?k ≤ mt_pos c_write k" using kk cw_eq2 by linarith
thus ?thesis using d2 by linarith
qed
qed
have "m < mt_pos c_write k" using mlt rge by simp
hence "1 ≤ mt_pos c_write k - m" by simp
thus "mt_tape c_write k (mt_pos c_write k - m) ≠ LE4" by (rule wtape_notLE)
qed
let ?aposk = "λk. if k < k_tm M then ar_newpos (m_d k) (?rposk k) else ?rposk k"
let ?apos = "λk. if k < k_tm M
then (if m_d k = dir.R then mt_pos c_write k
else mt_pos c_write k - ar_disp ?k (m_d k) (?rposk k))
else mt_pos c_write k"
obtain c_adv ma where
a_chain: "(c_write, c_adv) ∈ (mttm_step (ar_delta_advance M)) ^^ ma"
and a_state: "mt_state c_adv = (q', AR_SimNext, k_unidx 0, 0, m_a', m_d, ?aposk)"
and a_tape: "mt_tape c_adv = mt_tape c_write"
and a_pos: "mt_pos c_adv = ?apos"
using ar_advance_phase_in_sub[OF vM q'Q kge2 w_state' a'val dge1 notLE
pad_cwrite src_cwrite]
by blast
have c_adv_nxt: "fst (snd (mt_state c_adv)) = AR_SimNext" using a_state by simp
have achain': "(c_write, c') ∈ (mttm_step (ar_delta_advance M)) ^^ m_a"
using achain ca_eq by simp
have c'_eq: "c' = c_adv"
using chain_ar_delta_advance_to_SimNext_uniq[OF achain' a_chain c'_next
c_adv_nxt]
by simp
have c'_state: "mt_state c' = (q', AR_SimNext, k_unidx 0, 0, m_a', m_d, ?aposk)"
using c'_eq a_state by simp
have nxt: "mt_tape c'' = mt_tape c' ∧ mt_pos c'' = mt_pos c'
∧ ((q' ∉ {t_tm M, r_tm M}
∧ mt_state c'' = (q', AR_SimRead, 0, 0, m_a', m_d, ?aposk))
∨ (q' = t_tm M
∧ mt_state c'' = (t_tm M, ar_accept_stage (bl_tm M)))
∨ (q' = r_tm M
∧ mt_state c'' = (r_tm M, ar_reject_stage (bl_tm M))))"
using ar_next_step_inv[OF step c'_state] .
have nxt_tape: "mt_tape c'' = mt_tape c'" using nxt by simp
have nxt_pos: "mt_pos c'' = mt_pos c'" using nxt by simp
have nxt_disj:
"(q' ∉ {t_tm M, r_tm M}
∧ mt_state c'' = (q', AR_SimRead, 0, 0, m_a', m_d, ?aposk))
∨ (q' = t_tm M
∧ mt_state c'' = (t_tm M, ar_accept_stage (bl_tm M)))
∨ (q' = r_tm M
∧ mt_state c'' = (r_tm M, ar_reject_stage (bl_tm M)))"
using nxt by simp
have st_cMn: "mt_state cMn = q'" using cMn_def by simp
have padpos0: "∀j ≥ k_tm M. mt_pos cM j = 0" using pkok posk_tail by blast
have dposL: "m_d k ≠ dir.L" if p0: "mt_pos cM k = 0" and kN: "k < k_tm M" for k
proof -
have nM0: "nM k = 0" using p0 cM_eq by simp
have "tsM k 0 = le_tm M" using valcM cM_eq kN by (cases M) auto
hence "(λj. tsM j (nM j)) k = le_tm M" using nM0 by simp
hence "m_d k ∈ {dir.N, dir.R}" using valid_mttm_deltaLE[OF vM mdelta'] by simp
thus "m_d k ≠ dir.L" by auto
qed
have cwpost_b: "mt_tape c_w_post = mt_tape c_b"
using cwpost_tape cw_eq_cr r_tape by simp
have cM1tape: "mt_tape cMn k = (mt_tape cM k)(mt_pos cM k := m_a' k)" for k
using cMn_def cM_eq by simp
have wt_def: "mt_tape c'' k pos
= (if mt_pos cM k = 0 then mt_tape c_b k pos
else if sim_pos ?k (mt_pos cM k) ≤ pos
∧ pos < sim_pos ?k (mt_pos cM k) + ?k
then write_bit (Γ_tm M) (bl_tm M) (m_a' k)
(pos - sim_pos ?k (mt_pos cM k))
else mt_tape c_b k pos)" for k pos
proof (cases "k < k_tm M")
case True
thus ?thesis using nxt_tape c'_eq a_tape w_tape cwpost_b by simp
next
case False
hence kge: "k_tm M ≤ k" by simp
have p0: "mt_pos cM k = 0" using padpos0 kge by blast
have "mt_tape c'' k = mt_tape c_b k"
using nxt_tape c'_eq a_tape w_tape cwpost_b kge by simp
thus ?thesis using p0 by simp
qed
have tcorr_1: "∀k < k_tm M. ar_tape_correspondence (Γ_tm M) (le_tm M) (bl_tm M)
(mt_tape cMn k) (mt_tape c'' k)"
proof (intro allI impI)
fix k assume kN: "k < k_tm M"
show "ar_tape_correspondence (Γ_tm M) (le_tm M) (bl_tm M)
(mt_tape cMn k) (mt_tape c'' k)"
by (rule ar_write_tape_correspondence
[OF kge2 kN tcorr cM1tape a'le0_w wt_def])
qed
have apos_1: "mt_pos c'' k = sim_pos ?k (mt_pos cMn k)" for k
proof (cases "k < k_tm M")
case kN: True
have posM1: "mt_pos cMn k = go_dir (m_d k) (mt_pos cM k)"
using cMn_def cM_eq by simp
have key: "(if m_d k = dir.R
then (if mt_pos cM k = 0 then Suc 0
else sim_pos ?k (mt_pos cM k) + ?k)
else (if mt_pos cM k = 0 then Suc 0
else sim_pos ?k (mt_pos cM k) + ?k)
- ar_disp ?k (m_d k)
(if mt_pos cM k = 0 then AR_AtLE
else if mt_pos cM k = 1 then AR_AtFirstProper
else AR_AtFurtherProper))
= sim_pos ?k (go_dir (m_d k) (mt_pos cM k))"
proof (rule ar_advance_newsimpos)
show "2 ≤ ?k" by (rule kge2)
show "mt_pos cM k = 0 ⟹ m_d k ≠ dir.L" using dposL kN by blast
qed
have cadv_pos: "mt_pos c'' k = (if m_d k = dir.R
then (if mt_pos cM k = 0 then Suc 0
else sim_pos ?k (mt_pos cM k) + ?k)
else (if mt_pos cM k = 0 then Suc 0
else sim_pos ?k (mt_pos cM k) + ?k)
- ar_disp ?k (m_d k)
(if mt_pos cM k = 0 then AR_AtLE
else if mt_pos cM k = 1 then AR_AtFirstProper
else AR_AtFurtherProper))"
using nxt_pos c'_eq a_pos w_pos ppos_w kN by simp
show ?thesis by (simp add: cadv_pos key posM1)
next
case False
hence kge: "k_tm M ≤ k" by simp
have dN: "m_d k = dir.N" using dsupp kge by blast
have posM1: "mt_pos cMn k = go_dir (m_d k) (mt_pos cM k)"
using cMn_def cM_eq by simp
have "mt_pos c'' k = mt_pos c_b k"
using nxt_pos c'_eq a_pos w_pos cwpost_pos cw_eq_cr r_pos kge by simp
also have "… = sim_pos ?k (mt_pos cM k)" using ppos by simp
also have "… = sim_pos ?k (mt_pos cMn k)" using posM1 dN by simp
finally show ?thesis .
qed
have aposk_1: "?aposk k = AR_AtLE ⟷ mt_pos cMn k = 0" for k
proof (cases "k < k_tm M")
case kN: True
have posM1: "mt_pos cMn k = go_dir (m_d k) (mt_pos cM k)"
using cMn_def cM_eq by simp
have key: "(ar_newpos (m_d k)
(if mt_pos cM k = 0 then AR_AtLE
else if mt_pos cM k = 1 then AR_AtFirstProper
else AR_AtFurtherProper) = AR_AtLE)
⟷ go_dir (m_d k) (mt_pos cM k) = 0"
proof (rule ar_newpos_atLE_iff)
show "mt_pos cM k = 0 ⟹ m_d k ≠ dir.L" using dposL kN by blast
qed
have aposk_k: "?aposk k = ar_newpos (m_d k)
(if mt_pos cM k = 0 then AR_AtLE
else if mt_pos cM k = 1 then AR_AtFirstProper
else AR_AtFurtherProper)"
using kN by simp
show ?thesis by (simp add: aposk_k key posM1)
next
case False
hence kge: "k_tm M ≤ k" by simp
have dN: "m_d k = dir.N" using dsupp kge by blast
have p0: "mt_pos cM k = 0" using padpos0 kge by blast
have posM1: "mt_pos cMn k = go_dir (m_d k) (mt_pos cM k)"
using cMn_def cM_eq by simp
have "mt_pos cMn k = 0" using posM1 dN p0 by simp
moreover have "posk k = AR_AtLE" using posk_tail kge by blast
moreover have "?aposk k = posk k" using kge by simp
ultimately show ?thesis by simp
qed
have pad_c'': "∀j ≥ k_tm M. mt_tape c'' j (mt_pos c'' j) = BLANK4"
proof (intro allI impI)
fix j assume jk: "k_tm M ≤ j"
have "mt_pos c'' j = mt_pos c_write j"
using nxt_pos c'_eq a_pos jk by simp
moreover have "mt_tape c'' j = mt_tape c_write j"
using nxt_tape c'_eq a_tape by simp
ultimately show "mt_tape c'' j (mt_pos c'' j) = BLANK4"
using pad_cwrite jk by simp
qed
have src_read'': "ar_stage_bounded (bl_tm M) (k_tm M)
(AR_SimRead, 0, 0, m_a', m_d, ?aposk)"
using kpos_tm dsupp posk_tail by (simp add: ar_stage_bounded_def)
show ?thesis
proof (intro exI[where x = cMn] conjI)
show "(cM, cMn) ∈ mttm_step (delta_tm M)" by (rule m_step)
show "ar_walker_at_boundary M cMn c''"
proof -
consider
(cont) "q' ∉ {t_tm M, r_tm M}"
"mt_state c'' = (q', AR_SimRead, 0, 0, m_a', m_d, ?aposk)"
| (acc) "q' = t_tm M"
"mt_state c'' = (t_tm M, ar_accept_stage (bl_tm M))"
| (rej) "q' = r_tm M"
"mt_state c'' = (r_tm M, ar_reject_stage (bl_tm M))"
using nxt_disj by blast
thus ?thesis
proof cases
case cont
have notT: "q' ≠ t_tm M" using cont(1) by simp
have notR: "q' ≠ r_tm M" using cont(1) by simp
show ?thesis
unfolding ar_walker_at_boundary_def
proof (intro conjI)
show "ar_simulates M cMn c''"
by (simp add: ar_simulates_def Let_def cont(2) st_cMn notT notR
tcorr_1 apos_1)
show "ar_posk_consistent M cMn c''"
by (simp add: ar_posk_consistent_def cont(2) aposk_1)
show "ar_at_read_boundary M c''"
by (simp add: ar_at_read_boundary_def cont(2) a'G pad_c'' src_read'')
qed
next
case acc
show ?thesis
unfolding ar_walker_at_boundary_def
proof (intro conjI)
show "ar_simulates M cMn c''"
by (simp add: ar_simulates_def Let_def acc(2) st_cMn acc(1)
tcorr_1 ar_accept_stage_def)
show "ar_posk_consistent M cMn c''"
by (simp add: ar_posk_consistent_def acc(2) ar_accept_stage_def)
show "ar_at_read_boundary M c''"
by (simp add: ar_at_read_boundary_def acc(2) ar_accept_stage_def
pad_c'')
qed
next
case rej
show ?thesis
unfolding ar_walker_at_boundary_def
proof (intro conjI)
show "ar_simulates M cMn c''"
by (simp add: ar_simulates_def Let_def rej(2) st_cMn rej(1)
tcorr_1 ar_reject_stage_def)
show "ar_posk_consistent M cMn c''"
by (simp add: ar_posk_consistent_def rej(2) ar_reject_stage_def)
show "ar_at_read_boundary M c''"
by (simp add: ar_at_read_boundary_def rej(2) ar_reject_stage_def
pad_c'')
qed
qed
qed
qed
qed
subsection ‹Chunked reverse engine›
text ‹The reverse-arm loop invariant: the substep-walker is in
∗‹some› stage of the cycle. Six disjuncts, one per walker
predicate. This is the AR analogue of
carrying ‹ae_simulates› across AE's reverse induction, but
stage-granular: where AE peels a whole fixed-length cycle per
‹ae_backward_stage›, AR peels one ‹M'›-substep and dispatches on
the current substep tag (the cycle length is data-dependent here, which
is why the pivot to the substep walker was needed in the first place).›
definition ar_walker ::
"('q, 'a) mttm
⇒ ('a, 'q) mt_config
⇒ (sym4, 'q × 'a ar_stage) mt_config ⇒ bool" where
"ar_walker M cM c' ⟷
ar_walker_at_boundary M cM c'
∨ ar_walker_in_read M cM c'
∨ ar_walker_at_compute M cM c'
∨ ar_walker_in_write M cM c'
∨ ar_walker_in_advance M cM c'
∨ ar_walker_at_next M cM c'"
text ‹Chunked-induction engine for the reverse arm, the AR analogue of
AE's ‹ae_simulation_phase_chunked_reverse›. Given a finite
‹M'›-trace ‹(c', c_acc)› of length ‹m› ending in the canonical
accept config ‹(t_tm M, ar_accept_stage (bl_tm M))› and the walker
invariant at ‹c'› relative to a reachable ‹cM›, deliver an
accepting ‹M›-path from ‹cM›. Strong induction on ‹m›; at
each level dispatch on the walker stage and peel one ‹M'›-step:
▪ the five active stages (‹in_read›, ‹at_compute›,
‹in_write›, ‹in_advance›, ‹at_next›, and an active read
boundary) all have ‹c' ≠ c_acc›, so ‹m = Suc m'›; peel
the step via the matching preservation lemma (‹at_compute› emits
one ‹M›-step into the ‹in_write› witness; ‹at_next› emits
one via ‹ar_walker_cycle_close› and advances ‹cM›), then
recurse on ‹m'›;
▪ a boundary at the accept config closes the induction:
‹ar_simulates_accept_iff› forces ‹mt_state cM = t_tm M›;
▪ a boundary at the reject config is impossible — the trace runs to
the accept config, but reject is terminal (‹ar_reject_terminal›)
and the reject config is not the accept config.
The conclusion is in ‹rtrancl› form for the downstream
‹Lang_mttm›-repacking in ‹alphabet_reduce_language›.›
lemma ar_simulation_phase_chunked_reverse:
fixes M :: "('q, 'a) mttm"
and w :: "'a list"
and cM :: "('a, 'q) mt_config"
and c' c_acc :: "(sym4, 'q × 'a ar_stage) mt_config"
and m :: nat
assumes vM: "valid_mttm M"
and w_sub: "set w ⊆ Sigma_tm M"
and card_ge: "card (Γ_tm M) ≥ 4"
and lebl: "le_tm M ≠ bl_tm M"
and reach_M: "(init_config_mttm M w, cM) ∈ (mttm_step (delta_tm M))⇧*"
and trace: "(c', c_acc) ∈ (mttm_step (alphabet_reduce_delta M)) ^^ m"
and accept: "mt_state c_acc = (t_tm M, ar_accept_stage (bl_tm M))"
and walk: "ar_walker M cM c'"
shows "∃cM_final. (cM, cM_final) ∈ (mttm_step (delta_tm M))⇧*
∧ mt_state cM_final = t_tm M"
using reach_M trace walk
proof (induction m arbitrary: cM c' rule: less_induct)
case (less m)
let ?R = "mttm_step (alphabet_reduce_delta M)"
have kge2: "2 ≤ block_width (Γ_tm M)"
proof -
have "(2::nat) ^ 2 ≤ 2 ^ block_width (Γ_tm M)"
using card_ge card_le_two_pow_block_width[of "Γ_tm M"] by simp
thus "2 ≤ block_width (Γ_tm M)"
using power_le_imp_le_exp[of "2::nat" 2 "block_width (Γ_tm M)"] by simp
qed
have valcM: "valid_config_mttm M cM"
by (rule valid_reach_mttm[OF vM w_sub less.prems(1)])
have qQ: "mt_state cM ∈ Q_tm M" using valcM by (cases M; cases cM) auto
have tapeG: "mt_tape cM k (mt_pos cM k) ∈ Γ_tm M" for k
proof -
have "range (mt_tape cM k) ⊆ Γ_tm M"
using valcM by (cases M; cases cM) auto
thus ?thesis by blast
qed
have acc_idx: "fst (snd (mt_state c_acc)) = AR_HaltAccept"
using accept by (simp add: ar_accept_stage_def)
have peel: "∃m' c'_1. m = Suc m'
∧ (c', c'_1) ∈ ?R ∧ (c'_1, c_acc) ∈ ?R ^^ m'"
if notHA: "fst (snd (mt_state c')) ≠ AR_HaltAccept"
proof -
have "m ≠ 0"
proof
assume "m = 0"
hence "c' = c_acc" using less.prems(2) by simp
thus False using notHA acc_idx by simp
qed
then obtain m' where mSuc: "m = Suc m'" using not0_implies_Suc by blast
have "(c', c_acc) ∈ ?R ^^ Suc m'" using less.prems(2) mSuc by simp
from relpow_Suc_D2[OF this] obtain c'_1 where
"(c', c'_1) ∈ ?R" and "(c'_1, c_acc) ∈ ?R ^^ m'" by blast
thus ?thesis using mSuc by blast
qed
from less.prems(3)
consider (bnd) "ar_walker_at_boundary M cM c'"
| (rd) "ar_walker_in_read M cM c'"
| (cmp) "ar_walker_at_compute M cM c'"
| (wr) "ar_walker_in_write M cM c'"
| (adv) "ar_walker_in_advance M cM c'"
| (nx) "ar_walker_at_next M cM c'"
unfolding ar_walker_def by blast
then show ?case
proof cases
case bnd
have sim: "ar_simulates M cM c'"
using bnd unfolding ar_walker_at_boundary_def by simp
obtain qM0 stg where st: "mt_state c' = (qM0, stg)"
by (cases "mt_state c'") auto
obtain idx tk i buf dvec posk where
sg: "stg = (idx, tk, i, buf, dvec, posk)" by (cases stg) auto
have state_disj:
"(idx = AR_SimRead ∧ qM0 ∉ {t_tm M, r_tm M})
∨ (qM0 = t_tm M ∧ stg = ar_accept_stage (bl_tm M))
∨ (qM0 = r_tm M ∧ stg = ar_reject_stage (bl_tm M))"
using sim st sg unfolding ar_simulates_def by (auto split: prod.splits)
consider (active) "idx = AR_SimRead"
| (acc) "stg = ar_accept_stage (bl_tm M)" "qM0 = t_tm M"
| (rej) "stg = ar_reject_stage (bl_tm M)" "qM0 = r_tm M"
using state_disj by blast
thus ?thesis
proof cases
case active
have neq: "fst (snd (mt_state c')) ≠ AR_HaltAccept"
using st sg active by simp
obtain m' c'_1 where mSuc: "m = Suc m'"
and fst_step: "(c', c'_1) ∈ ?R"
and rest: "(c'_1, c_acc) ∈ ?R ^^ m'"
using peel[OF neq] by blast
have m'_lt: "m' < m" using mSuc by simp
have "ar_walker_in_read M cM c'_1 ∨ ar_walker_at_compute M cM c'_1"
using ar_walker_step_from_boundary[OF bnd fst_step] .
hence walk_1: "ar_walker M cM c'_1" unfolding ar_walker_def by blast
show ?thesis using less.IH[OF m'_lt less.prems(1) rest walk_1] .
next
case acc
have c'_acc: "mt_state c' = (t_tm M, ar_accept_stage (bl_tm M))"
using st sg acc by simp
have cM_t: "mt_state cM = t_tm M"
using ar_simulates_accept_iff[OF vM sim] c'_acc by simp
have "(cM, cM) ∈ (mttm_step (delta_tm M))⇧*" by simp
thus ?thesis using cM_t by blast
next
case rej
have c'_rej: "mt_state c' = (r_tm M, ar_reject_stage (bl_tm M))"
using st sg rej by simp
show ?thesis
proof (cases m)
case 0
have ceq: "c' = c_acc" using less.prems(2) 0 by simp
have "fst (snd (mt_state c')) = AR_HaltReject"
using c'_rej by (simp add: ar_reject_stage_def)
moreover have "fst (snd (mt_state c')) = AR_HaltAccept"
using ceq accept by (simp add: ar_accept_stage_def)
ultimately show ?thesis by simp
next
case (Suc m')
have "(c', c_acc) ∈ ?R ^^ Suc m'" using less.prems(2) Suc by simp
from relpow_Suc_D2[OF this] obtain c'_1 where
fst_step: "(c', c'_1) ∈ ?R" by blast
have "mt_state c' ≠ (r_tm M, ar_reject_stage (bl_tm M))"
by (rule ar_reject_terminal[OF vM card_ge fst_step])
thus ?thesis using c'_rej by simp
qed
qed
next
case rd
have neq: "fst (snd (mt_state c')) ≠ AR_HaltAccept"
using rd unfolding ar_walker_in_read_def by simp
obtain m' c'_1 where mSuc: "m = Suc m'"
and fst_step: "(c', c'_1) ∈ ?R"
and rest: "(c'_1, c_acc) ∈ ?R ^^ m'"
using peel[OF neq] by blast
have m'_lt: "m' < m" using mSuc by simp
have "ar_walker_in_read M cM c'_1 ∨ ar_walker_at_compute M cM c'_1"
using ar_walker_step_from_in_read[OF rd fst_step] .
hence walk_1: "ar_walker M cM c'_1" unfolding ar_walker_def by blast
show ?thesis using less.IH[OF m'_lt less.prems(1) rest walk_1] .
next
case cmp
have neq: "fst (snd (mt_state c')) ≠ AR_HaltAccept"
using cmp unfolding ar_walker_at_compute_def by simp
obtain m' c'_1 where mSuc: "m = Suc m'"
and fst_step: "(c', c'_1) ∈ ?R"
and rest: "(c'_1, c_acc) ∈ ?R ^^ m'"
using peel[OF neq] by blast
have m'_lt: "m' < m" using mSuc by simp
have w_1: "ar_walker_in_write M cM c'_1"
using ar_walker_step_from_at_compute[OF cmp fst_step vM qQ kge2 tapeG] .
have walk_1: "ar_walker M cM c'_1" using w_1 unfolding ar_walker_def by blast
show ?thesis using less.IH[OF m'_lt less.prems(1) rest walk_1] .
next
case wr
have neq: "fst (snd (mt_state c')) ≠ AR_HaltAccept"
using wr unfolding ar_walker_in_write_def by simp
obtain m' c'_1 where mSuc: "m = Suc m'"
and fst_step: "(c', c'_1) ∈ ?R"
and rest: "(c'_1, c_acc) ∈ ?R ^^ m'"
using peel[OF neq] by blast
have m'_lt: "m' < m" using mSuc by simp
have "ar_walker_in_write M cM c'_1 ∨ ar_walker_in_advance M cM c'_1"
using ar_walker_step_from_in_write[OF wr fst_step] .
hence walk_1: "ar_walker M cM c'_1" unfolding ar_walker_def by blast
show ?thesis using less.IH[OF m'_lt less.prems(1) rest walk_1] .
next
case adv
have neq: "fst (snd (mt_state c')) ≠ AR_HaltAccept"
using adv unfolding ar_walker_in_advance_def by simp
obtain m' c'_1 where mSuc: "m = Suc m'"
and fst_step: "(c', c'_1) ∈ ?R"
and rest: "(c'_1, c_acc) ∈ ?R ^^ m'"
using peel[OF neq] by blast
have m'_lt: "m' < m" using mSuc by simp
have "ar_walker_in_advance M cM c'_1 ∨ ar_walker_at_next M cM c'_1"
using ar_walker_step_from_in_advance[OF adv fst_step] .
hence walk_1: "ar_walker M cM c'_1" unfolding ar_walker_def by blast
show ?thesis using less.IH[OF m'_lt less.prems(1) rest walk_1] .
next
case nx
have neq: "fst (snd (mt_state c')) ≠ AR_HaltAccept"
using nx unfolding ar_walker_at_next_def by simp
obtain m' c'_1 where mSuc: "m = Suc m'"
and fst_step: "(c', c'_1) ∈ ?R"
and rest: "(c'_1, c_acc) ∈ ?R ^^ m'"
using peel[OF neq] by blast
have m'_lt: "m' < m" using mSuc by simp
obtain cMn where step_cMn: "(cM, cMn) ∈ mttm_step (delta_tm M)"
and bnd_1: "ar_walker_at_boundary M cMn c'_1"
using ar_walker_cycle_close[OF nx fst_step vM qQ kge2 tapeG
w_sub less.prems(1) lebl]
by blast
have reach_Mn: "(init_config_mttm M w, cMn) ∈ (mttm_step (delta_tm M))⇧*"
using less.prems(1) step_cMn by (rule rtrancl.rtrancl_into_rtrancl)
have walk_1: "ar_walker M cMn c'_1"
using bnd_1 unfolding ar_walker_def by blast
obtain cM_final where
run_final: "(cMn, cM_final) ∈ (mttm_step (delta_tm M))⇧*"
and acc_final: "mt_state cM_final = t_tm M"
using less.IH[OF m'_lt reach_Mn rest walk_1] by blast
have "(cM, cM_final) ∈ (mttm_step (delta_tm M))⇧*"
using step_cMn run_final by (meson r_into_rtrancl rtrancl_trans)
thus ?thesis using acc_final by blast
qed
qed
text ‹Classical language-equivalence (biconditional) for alphabet
reduction: an ‹'a›-word ‹w› over the input alphabet is in
‹M›'s language iff its ‹sym4›-encoding is in the language
of the reduced machine ‹M'›. Pairs the forward inclusion
‹alphabet_reduce_language_forward› (in
‹AlphabetReduction_Theorems.thy›) with the reverse leg supplied by
‹ar_simulation_phase_chunked_reverse›.
Unlike AE, the alphabet-reduction construction has no input
validation prefix (the no-validation design point), so the reverse
direction needs neither a validation-peel nor a determinism /
chain-uniqueness argument: the encoded input's accepting ‹M'›-run
is handed to the engine directly off the initial read-boundary
correspondence (‹ar_walker_at_boundary›, the conjunction of the
three ‹_init› invariants). No ‹det_mttm› hypothesis is
required.
The ‹set w ⊆ Sigma_tm M› guard is required (and matches
AE's statement): ‹Lang_mttm› bakes in the input-alphabet
restriction, so ‹w ∈ Lang_mttm M› supplies the guard for
free in the forward direction, but membership of the encoded word
in ‹Lang_mttm M'› says nothing about ‹w›'s alphabet. For
‹w› outside the input alphabet the encoded word can still be
accepted by ‹M'› while ‹w ∉ Lang_mttm M›.›
theorem alphabet_reduce_language:
fixes M :: "('q, 'a) mttm"
assumes vM: "valid_mttm M"
and s_neq_t: "s_tm M ≠ t_tm M"
and s_neq_r: "s_tm M ≠ r_tm M"
and le_neq_bl: "le_tm M ≠ bl_tm M"
and card_ge: "card (Γ_tm M) ≥ 4"
shows "∀w. set w ⊆ Sigma_tm M
⟶ (encode_input_ar (Γ_tm M) (bl_tm M) w ∈ Lang_mttm
(alphabet_reduce M
:: ('q × 'a ar_stage, sym4) mttm))
= (w ∈ Lang_mttm M)"
proof -
let ?M' = "alphabet_reduce M :: ('q × 'a ar_stage, sym4) mttm"
have fwd: "∀w. set w ⊆ Sigma_tm M
⟶ w ∈ Lang_mttm M
⟶ encode_input_ar (Γ_tm M) (bl_tm M) w ∈ Lang_mttm ?M'"
by (rule alphabet_reduce_language_forward[OF vM s_neq_t s_neq_r le_neq_bl card_ge])
show ?thesis
proof (intro allI impI)
fix w :: "'a list"
assume w_sub: "set w ⊆ Sigma_tm M"
let ?enc = "encode_input_ar (Γ_tm M) (bl_tm M) w"
let ?c' = "init_config_mttm ?M' ?enc"
show "(?enc ∈ Lang_mttm ?M') = (w ∈ Lang_mttm M)"
proof
assume w_in_M: "w ∈ Lang_mttm M"
from fwd w_sub w_in_M show "?enc ∈ Lang_mttm ?M'" by blast
next
assume enc_in_M': "?enc ∈ Lang_mttm ?M'"
from enc_in_M' obtain wM' nM' where
acc_path_M':
"(?c', Config⇩M (t_tm ?M') wM' nM')
∈ (mttm_step (delta_tm ?M'))⇧*"
unfolding Lang_mttm_def by blast
have acc_path:
"(?c', Config⇩M (t_tm ?M') wM' nM')
∈ (mttm_step (alphabet_reduce_delta M))⇧*"
using acc_path_M' by simp
obtain m where trace:
"(?c', Config⇩M (t_tm ?M') wM' nM')
∈ (mttm_step (alphabet_reduce_delta M)) ^^ m"
using acc_path rtrancl_imp_relpow by metis
have accept:
"mt_state (Config⇩M (t_tm ?M') wM' nM')
= (t_tm M, ar_accept_stage (bl_tm M))"
by simp
have sim: "ar_simulates M (init_config_mttm M w) ?c'"
by (rule ar_simulates_init[OF vM w_sub s_neq_t s_neq_r])
have posk: "ar_posk_consistent M (init_config_mttm M w) ?c'"
by (rule ar_posk_consistent_init)
have rbnd: "ar_at_read_boundary M ?c'"
by (rule ar_at_read_boundary_init[OF vM])
have walk: "ar_walker M (init_config_mttm M w) ?c'"
unfolding ar_walker_def ar_walker_at_boundary_def
using sim posk rbnd by blast
have reach_refl: "(init_config_mttm M w, init_config_mttm M w)
∈ (mttm_step (delta_tm M))⇧*" by simp
obtain cM_final where
M_path: "(init_config_mttm M w, cM_final)
∈ (mttm_step (delta_tm M))⇧*"
and M_acc: "mt_state cM_final = t_tm M"
using ar_simulation_phase_chunked_reverse
[OF vM w_sub card_ge le_neq_bl reach_refl trace accept walk]
by blast
obtain wM_acc nM_acc where
cM_final_eq: "cM_final = Config⇩M (t_tm M) wM_acc nM_acc"
using M_acc by (cases cM_final) simp
show "w ∈ Lang_mttm M"
unfolding Lang_mttm_def
using w_sub M_path cM_final_eq by blast
qed
qed
qed
end