Theory AlphabetReduction_Simulation
theory AlphabetReduction_Simulation
imports AlphabetReduction_Determinism
begin
subsection ‹Simulation correspondence›
text ‹Position correspondence ‹sim_pos b›, the AR analogue of
AE's ‹ae_decode_pos› read forwards (M-position to
M'-position). ‹M›-position ‹0› (the mandatory
‹LE› cell) maps to ‹M'›-position ‹0›;
‹M›-position ‹p ≥ 1› maps to the start of its
‹b›-cell block at ‹(p - 1) ⋅ b + 1›. The
‹1›-cell ‹LE› / ‹b›-cell proper layout
is intrinsic to the substrate's mandatory single ‹LE›
cell at position ‹0›.
Throughout, ‹b› abbreviates ‹block_width Γ› (the per-symbol cell width).›
definition sim_pos :: "nat ⇒ nat ⇒ nat" where
"sim_pos k p = (if p = 0 then 0 else (p - 1) * k + 1)"
text ‹The proper-region tiling fact: the encoded cells are
‹b›-wide, aligned, and disjoint, so a position
‹sim_pos b p + j› (‹j < b›) lands in another cell's
block ‹[sim_pos b q, sim_pos b q + b)› exactly when
‹p = q›. This is the bridge the forward-step tape
re-establishment (‹tcorr⇩1›) and the advance back-walk
(‹notLE›) both turn on: a write at ‹M›-position
‹q› touches the ‹p›-block iff ‹p = q›.
Proved by the alignment argument — a block index off by one shifts
the position by a full ‹b›, past the ‹j < b›
offset.›
lemma sim_pos_in_block_iff:
fixes K p q j :: nat
assumes K1: "1 ≤ K" and p1: "1 ≤ p" and q1: "1 ≤ q" and jK: "j < K"
shows "(sim_pos K q ≤ sim_pos K p + j ∧ sim_pos K p + j < sim_pos K q + K)
⟷ p = q"
proof
assume "p = q"
thus "sim_pos K q ≤ sim_pos K p + j ∧ sim_pos K p + j < sim_pos K q + K"
using jK by (simp add: sim_pos_def)
next
assume L: "sim_pos K q ≤ sim_pos K p + j
∧ sim_pos K p + j < sim_pos K q + K"
have lo: "(q - 1) * K ≤ (p - 1) * K + j"
and hi: "(p - 1) * K + j < (q - 1) * K + K"
using L p1 q1 by (auto simp: sim_pos_def)
have "p - 1 = q - 1"
proof (rule ccontr)
assume "p - 1 ≠ q - 1"
then consider "p - 1 < q - 1" | "q - 1 < p - 1" by linarith
thus False
proof cases
case 1
hence "(p - 1) + 1 ≤ q - 1" by simp
hence "((p - 1) + 1) * K ≤ (q - 1) * K" by (rule mult_le_mono1)
hence "(p - 1) * K + K ≤ (q - 1) * K" by (simp add: algebra_simps)
thus False using lo jK by linarith
next
case 2
hence "(q - 1) + 1 ≤ p - 1" by simp
hence "((q - 1) + 1) * K ≤ (p - 1) * K" by (rule mult_le_mono1)
hence "(q - 1) * K + K ≤ (p - 1) * K" by (simp add: algebra_simps)
thus False using hi by linarith
qed
qed
thus "p = q" using p1 q1 by linarith
qed
text ‹Per-cell encoding image ‹cell_repr Γ bl x›: the
‹b›-cell ‹sym4› block that a single
source cell of value ‹x› occupies on ‹M'›'s tape
(at proper positions ‹p ≥ 1›). The blank
‹bl› maps to ‹b› consecutive ‹BLANK4›
cells; every other source symbol maps to its
‹encode_symbol› bit-block. Both branches have length
‹b›, so the block is uniformly ‹b›-wide.
The endmarker ‹le› is not a case here: ‹le›
occurs only at position ‹0› (a ‹1›-cell
‹LE4›), handled directly in
‹ar_tape_correspondence›.›
definition cell_repr :: "'a set ⇒ 'a ⇒ 'a ⇒ sym4 list" where
"cell_repr Γ bl x =
(if x = bl then replicate (block_width Γ) BLANK4
else encode_symbol Γ bl x)"
text ‹Read-phase decode correctness for a whole cell block: folding
the accumulator from ‹gamma_unenum 0› over ‹cell_repr
Γ bl x› recovers ‹x›, uniformly across the blank and
proper branches. The blank branch is ‹foldl_ar_acc_blank›
(seed rewritten to ‹bl› via ‹gamma_unenum_zero›); the
proper branch is ‹foldl_ar_acc_encode_symbol›. This is the
fact the single-tape read composition discharges its ‹buf
tk›-correctness against.›
lemma foldl_ar_acc_cell_repr:
assumes "finite Γ" and "bl ∈ Γ" and "x ∈ Γ"
shows "foldl (ar_acc Γ bl) (gamma_unenum Γ bl 0)
(cell_repr Γ bl x) = x"
proof (cases "x = bl")
case True
have "foldl (ar_acc Γ bl) (gamma_unenum Γ bl 0) (cell_repr Γ bl x)
= foldl (ar_acc Γ bl) bl (replicate (block_width Γ) BLANK4)"
using True gamma_unenum_zero[OF assms(1,2)] by (simp add: cell_repr_def)
also have "… = bl" by (rule foldl_ar_acc_blank[OF assms(1,2)])
finally show ?thesis using True by simp
next
case False
have "foldl (ar_acc Γ bl) (gamma_unenum Γ bl 0) (cell_repr Γ bl x)
= foldl (ar_acc Γ bl) (gamma_unenum Γ bl 0)
(encode_symbol Γ bl x)"
using False by (simp add: cell_repr_def)
also have "… = x" by (rule foldl_ar_acc_encode_symbol[OF assms(1,3)])
finally show ?thesis .
qed
text ‹Tape-content correspondence under the encoding, the AR
analogue of AE's ‹ae_tape_correspondence›. ‹M›'s
tape cell ‹0› holds ‹le› and ‹M'›'s
cell ‹0› holds ‹LE4›; for every proper position
‹p ≥ 1›, the ‹b›-cell block on
‹M'› starting at ‹sim_pos b p›
spells out ‹cell_repr Γ bl (tM p)›. Since
‹M'›'s alphabet is the whole of ‹sym4›, no
separate gamma-block invariant is carried (AE's
‹ae_tape_in_gamma_block› would be vacuous here): the
correspondence pins every ‹M'›-cell.›
definition ar_tape_correspondence ::
"'a set ⇒ 'a ⇒ 'a ⇒ (nat ⇒ 'a) ⇒ (nat ⇒ sym4) ⇒ bool" where
"ar_tape_correspondence Γ le bl tM tM' ⟷
tM 0 = le ∧ tM' 0 = LE4 ∧
(∀p. 1 ≤ p ⟶
(∀j. j < block_width Γ ⟶
tM' (sim_pos (block_width Γ) p + j) = cell_repr Γ bl (tM p) ! j))"
text ‹The simulation relation, stage-granular, the AR analogue
of AE's ‹ae_simulates›. Holds at ‹AR_SimRead›
boundaries (M-step start, M-state not halted) or at the two
halt configurations between an ‹M›-configuration
‹cM› and an ‹M'›-configuration ‹cM'›:
▪ the ‹ar_substep_idx› tag is ‹AR_SimRead›
with the embedded M-state not yet in ‹⦃t, r⦄›,
or the M-state is ‹t› / ‹r› and the stage is the
matching ‹ar_accept_stage› / ‹ar_reject_stage›
(AR's dedicated halt stages, unlike AE's parked
‹init_stage›);
▪ the embedded M-state matches ‹M›'s state;
▪ every tape corresponds cell-for-cell via
‹ar_tape_correspondence›;
▪ at an ‹AR_SimRead› boundary, every head sits at
‹sim_pos b› of ‹M›'s head.›
definition ar_simulates ::
"('q, 'a) mttm
⇒ ('a, 'q) mt_config
⇒ (sym4, 'q × 'a ar_stage) mt_config
⇒ bool" where
"ar_simulates M cM cM' ⟷
(let qM = mt_state cM; tsM = mt_tape cM; nM = mt_pos cM;
full = mt_state cM';
tsM' = mt_tape cM'; nM' = mt_pos cM' in
(case full of (qM', stg) ⇒
(case stg of (idx, _, _, _, _, _) ⇒
((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)))
∧ qM = qM'
∧ (∀k < k_tm M. ar_tape_correspondence (Γ_tm M) (le_tm M) (bl_tm M)
(tsM k) (tsM' k))
∧ (idx = AR_SimRead
⟶ (∀k. nM' k = sim_pos (block_width (Γ_tm M)) (nM k))))))"
text ‹Companion invariant carried alongside ‹ar_simulates› (the AR
analogue of AE's ‹ae_buffer_in_gamma_block›): at an
‹AR_SimRead› boundary the per-tape position-kind flag
‹posk› agrees with ‹M›'s head being on the left-end
marker, ‹posk k = AR_AtLE ⟷ nM k = 0›. This is
the bit the read's LE-vs-proper dispatch consumes; the
‹AR_AtFirstProper›/‹AR_AtFurtherProper› split is
deliberately not pinned (the read re-derives it via look-back). Kept
out of ‹ar_simulates› proper so the reverse-direction language
proof, which shares ‹ar_simulates›, carries no ‹posk›
reasoning. Vacuous off the ‹AR_SimRead› boundary (terminal
accept/reject configs), where the flag is never read again. Sound by
the look-back re-sync argument: established
at the initial config (all heads at ‹0›, all flags
‹AR_AtLE›) and preserved each ‹M›-step by
‹ar_simulates_forward_step›.›
definition ar_posk_consistent ::
"('q, 'a) mttm
⇒ ('a, 'q) mt_config
⇒ (sym4, 'q × 'a ar_stage) mt_config ⇒ bool" where
"ar_posk_consistent M cM cM' ⟷
(case mt_state cM' of (qM', stg) ⇒
(case stg of (idx, _, _, _, _, posk) ⇒
idx = AR_SimRead
⟶ (∀k. posk k = AR_AtLE ⟷ mt_pos cM k = 0)))"
text ‹Second companion invariant, the boundary-shape companion (the
buffer-in-‹Γ› companion, plus
the canonical-position pin). ‹ar_simulates›'s
‹AR_SimRead› arm pins only ‹idx = AR_SimRead› — not
the current-tape / bit-counter fields, nor that ‹buf› is a
valid alphabet vector — but the read phase
(‹ar_read_phase›) starts a fresh per-‹M›-step scan
at tape ‹0›, counter ‹0›, and
‹ar_valid_stage› requires ‹buf› in
‹Γ ∪ {bl}›. So this companion asserts, at an
‹AR_SimRead› boundary, the canonical entry shape ‹tk =
0›, ‹i = 0›, ‹∀k. buf k ∈ Γ ∪
{bl}›. Vacuous off the boundary (the halt configs), where the
read phase never runs. Under value-level tape count it carries two
further invariants the reverse walker's read-phase lift needs: the
boundary stage is ‹ar_stage_bounded› (its ‹buf› /
‹dvec› / ‹posk› tails freeze beyond ‹k_tm M›),
and the whole config is blank-tailed (‹∀j ≥ k_tm M.
mt_tape cM' j (mt_pos cM' j) = BLANK4›) — the ‹src0_b› /
‹pad0_b› facts the substrate's ‹alphabet_reduce_delta›
support filter forces on every produced step. Established at the
initial config
(‹ar_init_stage›: tape ‹0›, counter ‹0›,
‹buf = λ_. bl›) and preserved each ‹M›-step by
the next handshake's non-terminal arm (resets tape / counter to
‹0›; ‹buf› carries the just-written symbols, all in
‹Γ›). Kept separate from ‹ar_simulates› for
the same reason as ‹ar_posk_consistent› — the
reverse-direction language proof shares ‹ar_simulates› and
should carry no forward-only boundary bookkeeping.›
definition ar_at_read_boundary ::
"('q, 'a) mttm
⇒ (sym4, 'q × 'a ar_stage) mt_config ⇒ bool" where
"ar_at_read_boundary M cM' ⟷
(case mt_state cM' of (qM', stg) ⇒
(case stg of (idx, tk, i, buf, dvec, posk) ⇒
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))))
∧ (∀j ≥ k_tm M. mt_tape cM' j (mt_pos cM' j) = BLANK4)"
end