Theory Multitape_Alphabet_Enlargement.AlphabetEnlargement_Simulation
theory AlphabetEnlargement_Simulation
imports AlphabetEnlargement_Delta
begin
subsection ‹The combinator›
text ‹The alphabet-enlargement combinator following Hopcroft--Ullman
\<^cite>‹‹Theorem 12.3› in "Hopcroft1979:introduction"›. Takes a
substrate machine over alphabet ‹'a›;
produces a substrate machine over alphabet
‹'c ⇒ 'a› (blocks) with state set
‹'q × ('a, 'c) ae_stage›. Tape count ‹k_tm M› is preserved.
The output machine simulates ‹M› on the externally encoded
input via a stage-based simulation: each stage consumes 8
super-steps of ‹M'› to simulate exactly ‹c› consecutive steps
of ‹M› (pre-fetch home + neighbour blocks in 4 substeps;
compute next ‹c› ‹M›-steps internally; write back up to 3
modified blocks and reposition heads in 4 substeps).
Pieces:
▪ ‹Q'›: ‹Q_M × UNIV› over ‹ae_stage›.
▪ ‹Σ'›: blocks composed of ‹Σ_M ∪ {bl_M}› cells (the
encoder's image), excluding the all-blank and all-LE blocks.
▪ ‹Γ'›: blocks composed of ‹Γ_M› cells.
▪ blank: ‹bl_block bl_M› (the constant blank-block).
▪ LE: ‹LE_block le_M› (the constant LE-block).
▪ ‹δ'›: ‹alphabet_enlarge_delta M› (union of 8 per-substep
relations; bodies partially filled in this pass).
▪ start: ‹(s_M, init_stage le_M)›.
▪ accept / reject: ‹(t_M, init_stage le_M)› /
‹(r_M, init_stage le_M)›; distinguished by the ‹M›-state
component, which inherits ‹t_M ≠ r_M› from ‹M›'s wf.›
definition alphabet_enlarge ::
"('q, 'a) mttm
⇒ ('q × ('a, ('c :: enum)) ae_stage, 'c ⇒ 'a) mttm"
where
"alphabet_enlarge M =
(case M of MTTM Q_M Sigma_M Gamma_M bl_M le_M _ s_M t_M r_M k_M ⇒
MTTM (Q_M × {stg. ae_valid_stage Gamma_M le_M k_M stg})
(gamma_block (Sigma_M ∪ {bl_M})
- {bl_block bl_M, LE_block le_M})
(gamma_block Gamma_M)
(bl_block bl_M)
(LE_block le_M)
(alphabet_enlarge_delta M)
(s_M, init_stage le_M)
(t_M, init_stage le_M)
(r_M, init_stage le_M)
k_M)"
subsection ‹Simulation infrastructure›
text ‹The two top-level theorems below — ‹alphabet_enlarge_language›
and ‹alphabet_enlarge_time› — both route through a shared
simulation argument relating ‹M›'s configurations to
‹M' = alphabet_enlarge M›'s configurations at SS1 stage
boundaries (or at halt configurations reached via
SS8‹→›SS1's halt-routing). The relation ‹ae_simulates›,
the per-substep mid-stage invariants ‹ae_inv_ss1›,
‹…›, ‹ae_inv_ss8›, and the lemma roster below
carry the structure of that argument.›
subsubsection ‹Position-decoding, tape correspondence, initial config›
text ‹The position-decoding map: given ‹M'›'s block
position ‹s› and a within-block offset ‹i :: 'c›, return
the corresponding ‹M›-tape position. For ‹s = 0› the result
is 0 (the LE position is shared between ‹M› and ‹M'›). For
‹s ≥ 1›, the block at ‹s› covers ‹M›'s positions
‹(s - 1) ⋅ c + 1› through ‹(s - 1) ⋅ c + c› in the order
determined by the canonical ‹'c›-enumeration via
‹c_idx›.›
definition ae_decode_pos :: "nat ⇒ ('c :: enum) ⇒ nat" where
"ae_decode_pos s i =
(if s = 0 then 0
else (s - 1) * card (UNIV :: 'c set) + c_idx i + 1)"
text ‹Tape-content correspondence under the encoding: for every
‹M›-tape position ‹p›, the value at ‹p› equals the value of
the corresponding ‹M'›-block at the corresponding offset.
Position 0 of ‹M›'s tape is fixed at ‹le› (the substrate's
LE invariant); positions ‹p ≥ 1› map bijectively to
block-and-offset pairs ‹(s, i)› with ‹s ≥ 1› via
‹p = (s - 1) ⋅ c + c_idx i + 1›.›
definition ae_tape_correspondence ::
"'a ⇒ (nat ⇒ 'a) ⇒ (nat ⇒ ('c :: enum ⇒ 'a)) ⇒ bool" where
"ae_tape_correspondence le tM tM' ⟷
tM 0 = le ∧
(∀s i. s ≥ 1
⟶ tM ((s - 1) * card (UNIV :: 'c set) + c_idx i + 1)
= tM' s i)"
text ‹Initial configuration of ‹M' = alphabet_enlarge M› on a
block input ‹w :: ('c ⇒ 'a) list›. Mirrors the
substrate's top-level ‹init_config_mttm› shape, re-stated here
with the explicit block tape layout the downstream
simulation lemmas need. Position 0 holds the LE-block; positions
‹1›‹…›‹length w› on tape 0 hold ‹w›'s blocks; all
other positions hold the blank-block; all heads at position
0.›
definition ae_init_config ::
"('q, 'a) mttm
⇒ (('c :: enum) ⇒ 'a) list
⇒ ('c ⇒ 'a, 'q × ('a, 'c) ae_stage) mt_config" where
"ae_init_config M w =
Config⇩M (s_tm M, init_stage (le_tm M))
(λi n. if i < k_tm M
then if n = 0 then LE_block (le_tm M)
else if i = 0 ∧ n ≤ length w
then w ! (n - 1)
else bl_block (bl_tm M)
else bl_block (bl_tm M))
(λ_. 0)"
text ‹Bridge: the substrate's ‹init_config_mttm› of
‹alphabet_enlarge M› on a block input ‹w› coincides
with the AE-specific ‹ae_init_config M w›. The substrate's
‹init_config_mttm› uses ‹alphabet_enlarge M›'s field
projections, which inherit from ‹M› via the construction
(start state becomes ‹(s_tm M, init_stage (le_tm M))›;
blank becomes ‹bl_block (bl_tm M)›; LE becomes
‹LE_block (le_tm M)›). Used by
‹alphabet_enlarge_language› and ‹alphabet_enlarge_time›
to translate the substrate-level ‹accepts_in_time_mttm›
conclusion into the AE-side ‹ae_init_config› form on which the
validation / simulation chains operate.›
lemma init_config_alphabet_enlarge:
fixes M :: "('q, 'a) mttm"
and w :: "('c :: enum ⇒ 'a) list"
shows "init_config_mttm
(alphabet_enlarge M
:: ('q × ('a, 'c) ae_stage, 'c ⇒ 'a) mttm) w
= ae_init_config M w"
proof -
obtain Q Σ Γ bl le δ s t r k where
M_eq: "M = MTTM Q Σ Γ bl le δ s t r k"
by (cases M)
have s_eq: "s_tm M = s" by (simp only: M_eq s_tm.simps)
have le_eq: "le_tm M = le" by (simp only: M_eq le_tm.simps)
have bl_eq: "bl_tm M = bl" by (simp only: M_eq bl_tm.simps)
show ?thesis
unfolding ae_init_config_def
unfolding s_eq le_eq bl_eq
unfolding M_eq alphabet_enlarge_def
by simp
qed
subsubsection ‹Substrate projection bridges›
text ‹Projection bridges for ‹alphabet_enlarge M›: the field
accessors ‹s_tm›, ‹t_tm›, ‹r_tm›, ‹bl_tm›, ‹le_tm›,
‹delta_tm› are positional pattern-matches on the
‹MTTM› constructor. Used by ‹alphabet_enlarge_language›
and ‹alphabet_enlarge_time› to translate substrate-level
field references on ‹alphabet_enlarge M› into the AE-side
expressions (the construction's start / accept / reject states
inherit from ‹M› with an attached ‹init_stage le›;
blank and LE become block-encoded; delta is
‹alphabet_enlarge_delta M›).›
lemma s_tm_alphabet_enlarge:
fixes M :: "('q, 'a) mttm"
shows "s_tm (alphabet_enlarge M
:: ('q × ('a, ('c :: enum)) ae_stage,
'c ⇒ 'a) mttm)
= (s_tm M, init_stage (le_tm M))"
by (cases M) (simp add: alphabet_enlarge_def)
lemma t_tm_alphabet_enlarge:
fixes M :: "('q, 'a) mttm"
shows "t_tm (alphabet_enlarge M
:: ('q × ('a, ('c :: enum)) ae_stage,
'c ⇒ 'a) mttm)
= (t_tm M, init_stage (le_tm M))"
by (cases M) (simp add: alphabet_enlarge_def)
lemma r_tm_alphabet_enlarge:
fixes M :: "('q, 'a) mttm"
shows "r_tm (alphabet_enlarge M
:: ('q × ('a, ('c :: enum)) ae_stage,
'c ⇒ 'a) mttm)
= (r_tm M, init_stage (le_tm M))"
by (cases M) (simp add: alphabet_enlarge_def)
lemma bl_tm_alphabet_enlarge:
fixes M :: "('q, 'a) mttm"
shows "bl_tm (alphabet_enlarge M
:: ('q × ('a, ('c :: enum)) ae_stage,
'c ⇒ 'a) mttm)
= bl_block (bl_tm M)"
by (cases M) (simp add: alphabet_enlarge_def)
lemma le_tm_alphabet_enlarge:
fixes M :: "('q, 'a) mttm"
shows "le_tm (alphabet_enlarge M
:: ('q × ('a, ('c :: enum)) ae_stage,
'c ⇒ 'a) mttm)
= LE_block (le_tm M)"
by (cases M) (simp add: alphabet_enlarge_def)
lemma delta_tm_alphabet_enlarge:
fixes M :: "('q, 'a) mttm"
shows "delta_tm (alphabet_enlarge M
:: ('q × ('a, ('c :: enum)) ae_stage,
'c ⇒ 'a) mttm)
= alphabet_enlarge_delta M"
by (cases M) (simp add: alphabet_enlarge_def)
lemma Sigma_tm_alphabet_enlarge:
fixes M :: "('q, 'a) mttm"
shows "Sigma_tm (alphabet_enlarge M
:: ('q × ('a, ('c :: enum)) ae_stage,
'c ⇒ 'a) mttm)
= gamma_block (Sigma_tm M ∪ {bl_tm M})
- {bl_block (bl_tm M), LE_block (le_tm M)}"
by (cases M) (simp add: alphabet_enlarge_def)
subsubsection ‹Gamma-block invariants and preservation›
text ‹Tape well-formedness invariant on an ‹M'›-configuration:
every cell of every tape lies in ‹gamma_block (Γ_tm M)›, and
every cell of every ∗‹inactive› tape (index ‹≥ k_tm M›)
holds the blank block ‹bl_block (bl_tm M)›. The blank-tail
conjunct is the value-level analogue of the substrate's config
support: with the tape count a runtime ‹nat›, the inactive tapes
must read blank so that a constructed ‹δ'›-transition meets the
substrate ‹δ›-support's read-side condition ‹∀j≥k. a j = bl›.
Carried by the simulation (and by each ‹ae_inv_ss<N>›) so that
downstream chain steps in ‹alphabet_enlarge_delta M› can
discharge both the intersection guard's read-side membership and
the support's blank-tail locally.›
definition ae_tape_in_gamma_block ::
"('q, 'a) mttm
⇒ ('c :: enum ⇒ 'a,
'q × ('a, 'c) ae_stage) mt_config
⇒ bool" where
"ae_tape_in_gamma_block M cM' ⟷
(∀k p. mt_tape cM' k p ∈ gamma_block (Γ_tm M))
∧ (∀j≥k_tm M. ∀p. mt_tape cM' j p = bl_block (bl_tm M))"
text ‹Write-side blank-tail of ‹alphabet_enlarge_delta›: every
member writes the blank block ‹bl_block (bl_tm M)› on every
inactive tape (index ‹≥ k_tm M›). Holds builder-by-builder —
the validation and buffer-load substeps leave the tape unchanged
(‹a' = a›, so the write-tail is the read-tail conjunct), and the
write-back substeps guard their write to ‹bl_block (bl_tm M)›
beyond ‹k_tm M›. Discharges the ‹δ›-support write-side
obligation when threading ‹ae_tape_in_gamma_block›'s blank-tail
across a step.›
lemma alphabet_enlarge_delta_write_tail:
fixes M :: "('q, 'a) mttm"
assumes mem: "(s, a, s', a', d) ∈ alphabet_enlarge_delta M"
shows "∀j≥k_tm M. a' j = bl_block (bl_tm M)"
using mem
unfolding alphabet_enlarge_delta_def
ae_delta_val_fwd_advance_def ae_delta_val_fwd_to_padded_def
ae_delta_val_fwd_reject_def ae_delta_val_fwd_to_ret_def
ae_delta_val_pad_to_ret_def ae_delta_val_pad_reject_def
ae_delta_val_ret_step_def ae_delta_val_ret_to_sim_def
ae_delta_ss1_ss2_def ae_delta_ss2_ss3_def ae_delta_ss3_ss4_def
ae_delta_ss4_ss5_def ae_delta_ss5_ss6_def ae_delta_ss6_ss7_def
ae_delta_ss7_ss8_def ae_delta_ss8_ss1_def
by auto
text ‹Single-step preservation of the gamma-block invariant
under ‹alphabet_enlarge_delta›. The intersection guard in
‹alphabet_enlarge_delta›'s definition forces the written
value ‹a' k› to lie in ‹gamma_block (Γ_tm M)›; untouched
cells inherit gamma-block-ness from the precondition on
‹c'›. Iteration to ‹^^ k›-step chains follows by induction
on ‹k› at use sites; not packaged separately here pending
a concrete use site.›
lemma ae_step_alphabet_enlarge_gamma_preserve:
fixes M :: "('q, 'a) mttm"
and c' c'' :: "('c :: enum ⇒ 'a,
'q × ('a, 'c) ae_stage) mt_config"
assumes pre: "ae_tape_in_gamma_block M c'"
and step: "(c', c'') ∈ mttm_step (alphabet_enlarge_delta M)"
shows "ae_tape_in_gamma_block M c''"
proof -
from step obtain s ts n s' a' d where
c'_eq: "c' = Config⇩M s ts n"
and c''_eq: "c'' = Config⇩M s' (λk. (ts k)(n k := a' k))
(λk. go_dir (d k) (n k))"
and rel: "(s, (λk. ts k (n k)), s', a', d) ∈ alphabet_enlarge_delta M"
by (auto elim: mttm_step.cases)
from rel have a'_gamma: "∀k. a' k ∈ gamma_block (Γ_tm M)"
unfolding alphabet_enlarge_delta_def by auto
from rel have a'_tail: "∀j≥k_tm M. a' j = bl_block (bl_tm M)"
by (rule alphabet_enlarge_delta_write_tail)
have pre_gamma: "∀k p. mt_tape c' k p ∈ gamma_block (Γ_tm M)"
using pre unfolding ae_tape_in_gamma_block_def by simp
have pre_tail: "∀j≥k_tm M. ∀p. mt_tape c' j p = bl_block (bl_tm M)"
using pre unfolding ae_tape_in_gamma_block_def by simp
have gamma_part: "∀k p. mt_tape c'' k p ∈ gamma_block (Γ_tm M)"
proof (intro allI)
fix k p
show "mt_tape c'' k p ∈ gamma_block (Γ_tm M)"
proof (cases "p = n k")
case True
with c''_eq have "mt_tape c'' k p = a' k" by simp
thus ?thesis using a'_gamma by simp
next
case False
with c''_eq have eq_c'': "mt_tape c'' k p = ts k p" by simp
from c'_eq have eq_c': "mt_tape c' k p = ts k p" by simp
from eq_c'' eq_c' have "mt_tape c'' k p = mt_tape c' k p" by simp
thus ?thesis using pre_gamma by simp
qed
qed
have tail_part: "∀j≥k_tm M. ∀p. mt_tape c'' j p = bl_block (bl_tm M)"
proof (intro allI impI)
fix j p assume jk: "k_tm M ≤ j"
show "mt_tape c'' j p = bl_block (bl_tm M)"
proof (cases "p = n j")
case True
with c''_eq have "mt_tape c'' j p = a' j" by simp
thus ?thesis using a'_tail jk by simp
next
case False
with c''_eq have eq_c'': "mt_tape c'' j p = ts j p" by simp
from c'_eq have "mt_tape c' j p = ts j p" by simp
with eq_c'' have "mt_tape c'' j p = mt_tape c' j p" by simp
thus ?thesis using pre_tail jk by simp
qed
qed
show ?thesis
unfolding ae_tape_in_gamma_block_def
using gamma_part tail_part by blast
qed
text ‹Side-band invariant: the ‹M'›-state's stage is ∗‹valid›
in the sense of ‹ae_valid_stage› at ‹Γ_tm M›, ‹le_tm M›,
‹k_tm M› — every block stored in the three-block buffer
lies in ‹gamma_block (Γ_tm M)›, and the per-tape offset,
buffer and destination fields are all frozen at their initial
values beyond the tape count ‹k_tm M›. Companion to
‹ae_tape_in_gamma_block›: the gamma conjunct discharges the
‹alphabet_enlarge_delta› intersection's write-side membership
at the write-back substeps (SS5‹→›SS6, SS6‹→›SS7,
SS7‹→›SS8), and the frozen-tail conjuncts supply the
‹ae_valid_stage› source obligation the step-existence lemmas
feed to the ‹*_dest_valid› preservation lemmas — neither is
provable from the minimal ‹ae_inv_ss<N>› bodies alone. Equal by
construction to ‹ae_valid_stage (Γ_tm M) (le_tm M) (k_tm M)
(snd (mt_state cM'))›.›
definition ae_buffer_in_gamma_block ::
"('q, 'a) mttm
⇒ ('c :: enum ⇒ 'a,
'q × ('a, 'c) ae_stage) mt_config
⇒ bool" where
"ae_buffer_in_gamma_block M cM' ⟷
(case mt_state cM' of (_, off, buf, dst, _) ⇒
(∀k. fst (buf k) ∈ gamma_block (Γ_tm M)
∧ fst (snd (buf k)) ∈ gamma_block (Γ_tm M)
∧ snd (snd (buf k)) ∈ gamma_block (Γ_tm M))
∧ (∀j≥k_tm M. off j = init_offset j)
∧ (∀j≥k_tm M. buf j = init_buffer (le_tm M) j)
∧ (∀j≥k_tm M. dst j = init_dest j))"
text ‹Preservation of ‹ae_buffer_in_gamma_block› (stage
validity) under a single ‹mttm_step› via
‹alphabet_enlarge_delta›. Companion to
‹ae_step_alphabet_enlarge_gamma_preserve› (tape-side). The
destination stage's ‹ae_valid_stage› is already an explicit
conjunct of ‹alphabet_enlarge_delta›'s intersection, so the
invariant is preserved by reading it straight off the post-state
— no case split on the 16 sub-deltas is required. (The
per-substep discharge of that conjunct lives in the
‹*_dest_valid› lemmas, which the step-existence lemmas invoke
when building each ‹δ'›-membership.)›
lemma ae_step_alphabet_enlarge_buffer_gamma_preserve:
fixes M :: "('q, 'a) mttm"
and c' c'' :: "('c :: enum ⇒ 'a,
'q × ('a, 'c) ae_stage) mt_config"
assumes vM: "valid_mttm M"
and pre_buf: "ae_buffer_in_gamma_block M c'"
and pre_tape: "ae_tape_in_gamma_block M c'"
and step: "(c', c'') ∈ mttm_step (alphabet_enlarge_delta M)"
shows "ae_buffer_in_gamma_block M c''"
proof -
obtain s ts n s' a' d where
rel: "(s, (λk. ts k (n k)), s', a', d) ∈ alphabet_enlarge_delta M"
and c'_eq: "c' = Config⇩M s ts n"
and c''_eq: "c'' = Config⇩M s' (λk. (ts k)(n k := a' k))
(λk. go_dir (d k) (n k))"
using step by (auto elim: mttm_step.cases)
obtain q' off' buf' dst' idx' where s'_eq: "s' = (q', off', buf', dst', idx')"
by (cases s')
have vs': "ae_valid_stage (Γ_tm M) (le_tm M) (k_tm M) (snd s')"
using rel unfolding alphabet_enlarge_delta_def by auto
have mt_c'': "mt_state c'' = s'" using c''_eq by simp
show ?thesis
using vs' mt_c'' s'_eq
unfolding ae_buffer_in_gamma_block_def ae_valid_stage_def by simp
qed
text ‹Joint preservation of ‹ae_tape_in_gamma_block› and
‹ae_buffer_in_gamma_block› across an ‹n›-step chain
of ‹mttm_step (alphabet_enlarge_delta M)›. The per-step
buffer-side preservation requires both invariants at the
source, so they must thread jointly across the chain.›
lemma ae_gamma_preserve_relpow:
fixes M :: "('q, 'a) mttm"
and c' c'' :: "('c :: enum ⇒ 'a,
'q × ('a, 'c) ae_stage) mt_config"
and n :: nat
assumes vM: "valid_mttm M"
and pre_buf: "ae_buffer_in_gamma_block M c'"
and pre_tape: "ae_tape_in_gamma_block M c'"
and chain: "(c', c'') ∈ mttm_step (alphabet_enlarge_delta M) ^^ n"
shows "ae_buffer_in_gamma_block M c'' ∧ ae_tape_in_gamma_block M c''"
proof -
have main:
"∀d. (c', d) ∈ mttm_step (alphabet_enlarge_delta M) ^^ n
⟶ ae_buffer_in_gamma_block M d ∧ ae_tape_in_gamma_block M d"
proof (induct n)
case 0
show ?case
proof (intro allI impI)
fix d
assume "(c', d) ∈ mttm_step (alphabet_enlarge_delta M) ^^ 0"
hence "d = c'" by simp
thus "ae_buffer_in_gamma_block M d ∧ ae_tape_in_gamma_block M d"
using pre_buf pre_tape by simp
qed
next
case (Suc n)
show ?case
proof (intro allI impI)
fix d
assume chain_Sn:
"(c', d) ∈ mttm_step (alphabet_enlarge_delta M) ^^ Suc n"
obtain c_mid where
chain_n: "(c', c_mid) ∈ mttm_step (alphabet_enlarge_delta M) ^^ n"
and step: "(c_mid, d) ∈ mttm_step (alphabet_enlarge_delta M)"
using chain_Sn by (auto elim: relpow_Suc_E)
from Suc.hyps chain_n have
mid_buf: "ae_buffer_in_gamma_block M c_mid"
and mid_tape: "ae_tape_in_gamma_block M c_mid"
by blast+
have d_tape: "ae_tape_in_gamma_block M d"
using ae_step_alphabet_enlarge_gamma_preserve[OF mid_tape step] .
have d_buf: "ae_buffer_in_gamma_block M d"
using ae_step_alphabet_enlarge_buffer_gamma_preserve
[OF vM mid_buf mid_tape step] .
show "ae_buffer_in_gamma_block M d ∧ ae_tape_in_gamma_block M d"
using d_buf d_tape by simp
qed
qed
show ?thesis using main chain by blast
qed
subsubsection ‹Simulation relation and mid-stage invariants›
text ‹The simulation relation, stage-granular. Holds at SS1
boundaries (or at halt configurations) between
‹M›-configurations and ‹M'›-configurations. Captures five
invariants: ‹substep_idx› is SS1 (or the halt branch fires);
‹M›-state matches the projected ‹'q›-component of ‹M'›'s
state; tape contents correspond cell-by-block-and-offset
per ‹ae_tape_correspondence›; head positions correspond per
‹ae_decode_pos›; and every ‹M'›-tape cell lies in
‹gamma_block (Γ_tm M)› per ‹ae_tape_in_gamma_block›.
Mid-stage configurations (‹substep_idx› ‹∈› ‹{SS2, …, SS7}›
or any validation phase) are not in this relation; they're
handled by the per-substep invariants ‹ae_inv_ss<N>› below
that thread through individual substep proofs.›
definition ae_simulates ::
"('q, 'a) mttm
⇒ ('a, 'q) mt_config
⇒ ('c :: enum ⇒ 'a,
'q × ('a, 'c) ae_stage) mt_config
⇒ bool" where
"ae_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', off, buf, dest, idx) ⇒
((idx = SS1 ∧ qM' ∉ {t_tm M, r_tm M})
∨ (qM' ∈ {t_tm M, r_tm M}
∧ (off, buf, dest, idx) = init_stage (le_tm M)))
∧ qM = qM'
∧ (∀k<k_tm M. ae_tape_correspondence (le_tm M) (tsM k) (tsM' k))
∧ (idx = SS1
⟶ (∀k<k_tm M. nM k = ae_decode_pos (nM' k) (off k)))
∧ ae_tape_in_gamma_block M cM'))"
text ‹Mid-stage invariants: one per simulation substep boundary.
Each ‹ae_inv_ss<N>› describes ‹M'›'s configuration shape
at the substep boundary entering substep ‹SS<N>›. The
bodies are deliberately minimal: they pin only the
‹substep_idx› component and the ‹M›-state's
membership in ‹Q_tm M›. The heavier tape- and
buffer-content properties are tracked separately by the
companion side-band invariants ‹ae_tape_in_gamma_block›
and ‹ae_buffer_in_gamma_block› below, rather than folded
into these per-substep bodies.›
definition ae_inv_ss1 ::
"('q, 'a) mttm
⇒ ('c :: enum ⇒ 'a,
'q × ('a, 'c) ae_stage) mt_config
⇒ bool" where
"ae_inv_ss1 M cM' ⟷
(case mt_state cM' of (qM', _, _, _, idx) ⇒
idx = SS1 ∧ qM' ∈ Q_tm M)"
definition ae_inv_ss2 ::
"('q, 'a) mttm
⇒ ('c :: enum ⇒ 'a,
'q × ('a, 'c) ae_stage) mt_config
⇒ bool" where
"ae_inv_ss2 M cM' ⟷
(case mt_state cM' of (qM', _, _, _, idx) ⇒
idx = SS2 ∧ qM' ∈ Q_tm M)"
definition ae_inv_ss3 ::
"('q, 'a) mttm
⇒ ('c :: enum ⇒ 'a,
'q × ('a, 'c) ae_stage) mt_config
⇒ bool" where
"ae_inv_ss3 M cM' ⟷
(case mt_state cM' of (qM', _, _, _, idx) ⇒
idx = SS3 ∧ qM' ∈ Q_tm M)"
definition ae_inv_ss4 ::
"('q, 'a) mttm
⇒ ('c :: enum ⇒ 'a,
'q × ('a, 'c) ae_stage) mt_config
⇒ bool" where
"ae_inv_ss4 M cM' ⟷
(case mt_state cM' of (qM', _, _, _, idx) ⇒
idx = SS4 ∧ qM' ∈ Q_tm M)"
definition ae_inv_ss5 ::
"('q, 'a) mttm
⇒ ('c :: enum ⇒ 'a,
'q × ('a, 'c) ae_stage) mt_config
⇒ bool" where
"ae_inv_ss5 M cM' ⟷
(case mt_state cM' of (qM', _, _, _, idx) ⇒
idx = SS5 ∧ qM' ∈ Q_tm M)"
definition ae_inv_ss6 ::
"('q, 'a) mttm
⇒ ('c :: enum ⇒ 'a,
'q × ('a, 'c) ae_stage) mt_config
⇒ bool" where
"ae_inv_ss6 M cM' ⟷
(case mt_state cM' of (qM', _, _, _, idx) ⇒
idx = SS6 ∧ qM' ∈ Q_tm M)"
definition ae_inv_ss7 ::
"('q, 'a) mttm
⇒ ('c :: enum ⇒ 'a,
'q × ('a, 'c) ae_stage) mt_config
⇒ bool" where
"ae_inv_ss7 M cM' ⟷
(case mt_state cM' of (qM', _, _, _, idx) ⇒
idx = SS7 ∧ qM' ∈ Q_tm M)"
definition ae_inv_ss8 ::
"('q, 'a) mttm
⇒ ('c :: enum ⇒ 'a,
'q × ('a, 'c) ae_stage) mt_config
⇒ bool" where
"ae_inv_ss8 M cM' ⟷
(case mt_state cM' of (qM', _, _, _, idx) ⇒
idx = SS8 ∧ qM' ∈ Q_tm M)"
subsubsection ‹LE-guard pre-emption invariant›
text ‹Per-substep LE-compatibility predicates (SS6, SS7, SS8).
At these substeps, the action returns one of the buffer's side
slots ‹l›, ‹r› (or in SS8's halt case, the home slot) in
branches the LE-no-write guard cannot discharge structurally
(gamma-block alone allows ‹l, r ∈ LE_block›). Each predicate
asserts the substrate-level guard exactly: at the current
configuration, if the substep's action returns ‹LE_block› on
tape ‹k›, then ‹ts k (n k)› already equals ‹LE_block›.
These are contracts the chain proof discharges from a richer
position-buffer correspondence; the per-substep step-existence
lemmas consume them as additional hypotheses.›
definition ae_le_compat_ss6 ::
"('q, 'a) mttm
⇒ ('c :: enum ⇒ 'a,
'q × ('a, 'c) ae_stage) mt_config
⇒ bool" where
"ae_le_compat_ss6 M cM' ⟷
(case cM' of Config⇩M (_, _, buf, dest, _) ts n ⇒
∀k<k_tm M. fst (ae_ss6_action (le_tm M) (ts k (n k)) (buf k) (dest k))
= LE_block (le_tm M)
⟶ ts k (n k) = LE_block (le_tm M))"
definition ae_le_compat_ss7 ::
"('q, 'a) mttm
⇒ ('c :: enum ⇒ 'a,
'q × ('a, 'c) ae_stage) mt_config
⇒ bool" where
"ae_le_compat_ss7 M cM' ⟷
(case cM' of Config⇩M (_, _, buf, dest, _) ts n ⇒
∀k<k_tm M. fst (ae_ss7_action (le_tm M) (ts k (n k)) (buf k) (dest k))
= LE_block (le_tm M)
⟶ ts k (n k) = LE_block (le_tm M))"
definition ae_le_compat_ss8 ::
"('q, 'a) mttm
⇒ ('c :: enum ⇒ 'a,
'q × ('a, 'c) ae_stage) mt_config
⇒ bool" where
"ae_le_compat_ss8 M cM' ⟷
(case cM' of Config⇩M (_, _, buf, dest, _) ts n ⇒
∀k<k_tm M. fst (ae_ss8_action (le_tm M) (ts k (n k)) (buf k) (dest k))
= LE_block (le_tm M)
⟶ ts k (n k) = LE_block (le_tm M))"
text ‹**The LE-guard pre-emption invariant.** This is the
load-bearing side-band that makes the writeback chain
correct across all three regimes (steady-state, le1, le0).
*Why we need it.* Each writeback substep's action
(‹ae_ss5_action› through ‹ae_ss8_action›) has
an LE-guard prefix branch (‹a = LE_block le›: write
‹LE_block› back, idempotent — see the action-helper
preamble) and a default branch that writes some buffer slot.
If the buffer slot the default branch *would* write is itself
‹LE_block› and the head is at a non-LE position, the
default branch would corrupt the tape encoding by writing
‹LE_block› where non-LE data should be. The construction
prevents this by **threading the head trajectory through
block 0 (the LE position) at exactly the moments when a
buffer-LE-write would otherwise occur** — so the LE-guard
branch fires first and pre-empts the default branch's
dangerous write.
*What the predicate captures.* The three conjuncts are
exactly the structural facts needed for this pre-emption to
hold:
▸ Post-buffer-load (‹idx ∈ {SS5, SS6, SS7, SS8}›): the
buffer's ‹r› slot is not ‹LE_block›. This rules out
the dangerous write whenever SS6 (‹dest = AE_Left›) or
SS7/SS8 (various ‹dest›) would write the r-slot — those
branches' antecedent (‹slot = LE_block›) is vacuously
false. Justification: ‹r› is loaded from ‹M'›-position
‹p_start + 1 ≥ 1›; the substrate's ‹δ›LE
forbids ‹LE_block› at any position ‹≥ 1›, and the
c-step compute (via ‹ae_m_steps_buffered_correct›)
preserves this.
▸ SS6 (‹dest ≠ AE_Left›): when SS6's default branch
would write the ‹l›-slot, and that ‹l›-slot is
‹LE_block›, then the head IS at a position holding
‹LE_block›. The LE-guard fires and pre-empts the
default branch. In steady-state (‹s ≥ 2›) the
antecedent ‹l = LE_block› is vacuously false (l is
loaded from block ‹s-1 ≥ 1›, non-LE). In le1
(‹s = 1›) the antecedent is true (l is loaded from
block 0, which IS ‹LE_block›), and the consequent
is established by le1's head trajectory: SS5's
‹move L› rule (for ‹dest ≠ AE_Left›) takes the
head from block 1 (SS5 entry) to block 0 (SS6
entry) where it reads ‹LE_block›.
▸ SS8 (‹dest = AE_Left›): symmetric to the SS6 clause.
When SS8's default branch would write the ‹l›-slot for
‹dest = AE_Left›, and that slot is ‹LE_block›,
the head is at ‹LE_block›. Steady-state vacuous;
in le1 with ‹dest = AE_Left›, SS5's ‹move R› +
SS6's ‹move L› + SS7's ‹move L› threads the
head from block 1 to block 0 by SS8 entry.
Other substep+dest combinations either write ‹r›
(covered by conjunct 1, vacuous antecedent), write ‹a›
back idempotently (SS7's default; no ‹LE_block› ever
introduced), or fire only on the LE-guard branch (writing
‹LE_block› only when ‹a = LE_block›, which is
trivially safe).
*Why this isn't separate predicates per regime.* The
predicate's antecedents (‹slot = LE_block›) are
inherently regime-discriminating: steady-state satisfies
them vacuously, le1 satisfies them via head-trajectory
tracing. A single uniform predicate works because the
substep actions' direction rules
(‹ae_ss5_action›'s "move L when ‹dest ≠
AE_Left›", etc.) deliver the head to block 0 at
exactly the right substeps in le1, and don't need to in
steady-state.›
definition ae_position_link ::
"('q, 'a) mttm
⇒ ('c :: enum ⇒ 'a,
'q × ('a, 'c) ae_stage) mt_config
⇒ bool" where
"ae_position_link M cM' ⟷
(case mt_state cM' of (_, _, buf, dest, idx) ⇒
(idx ∈ {SS5, SS6, SS7, SS8} ⟶
(∀k<k_tm M. snd (snd (buf k)) ≠ LE_block (le_tm M)))
∧ (idx = SS6 ⟶
(∀k<k_tm M. dest k ≠ AE_Left
⟶ fst (buf k) = LE_block (le_tm M)
⟶ mt_tape cM' k (mt_pos cM' k)
= LE_block (le_tm M)))
∧ (idx = SS8 ⟶
(∀k<k_tm M. dest k = AE_Left
⟶ fst (buf k) = LE_block (le_tm M)
⟶ mt_tape cM' k (mt_pos cM' k)
= LE_block (le_tm M))))"
subsubsection ‹Position-link discharges›
text ‹Discharge lemmas: at SS‹<N>› entry (per
‹ae_inv_ss<N>›), the side-band ‹ae_position_link› implies the
per-substep contract ‹ae_le_compat_ss<N>›. Each proof
case-splits on the ‹ae_ss<N>_action›'s branches: r-write
branches close via the first conjunct of ‹ae_position_link›
(‹r ≠ LE_block› makes the antecedent vacuous); a-write
branches close trivially via ‹a' = a›; the l-write branch
(SS6 with ‹dest ≠ AE_Left›; SS8 with ‹dest = AE_Left›)
closes via the second conjunct (the position-link's
‹l = LE_block ⟶ ts (n) = LE_block› guard for that
substep+dest). Used at the chain proof's call site to
discharge the ‹ae_le_compat_ss<N>› hypotheses on the
‹ae_step_ss<N>_ss<N+1>_exists› step-existence helpers.›
lemma ae_position_link_discharges_ss6:
fixes M :: "('q, 'a) mttm"
and c' :: "('c :: enum ⇒ 'a,
'q × ('a, 'c) ae_stage) mt_config"
assumes inv: "ae_inv_ss6 M c'"
and pos: "ae_position_link M c'"
shows "ae_le_compat_ss6 M c'"
proof -
obtain q ofs buf dest where
state_eq: "mt_state c' = (q, ofs, buf, dest, SS6)"
using inv unfolding ae_inv_ss6_def
by (cases "mt_state c'") auto
obtain ts n where
c'_eq: "c' = Config⇩M (q, ofs, buf, dest, SS6) ts n"
using state_eq by (cases c') auto
have r_not_le: "∀k<k_tm M. snd (snd (buf k)) ≠ LE_block (le_tm M)"
using pos state_eq unfolding ae_position_link_def by simp
have l_guard:
"∀k<k_tm M. dest k ≠ AE_Left
⟶ fst (buf k) = LE_block (le_tm M)
⟶ ts k (n k) = LE_block (le_tm M)"
using pos state_eq c'_eq unfolding ae_position_link_def by simp
have body:
"∀k<k_tm M. fst (ae_ss6_action (le_tm M) (ts k (n k)) (buf k) (dest k))
= LE_block (le_tm M)
⟶ ts k (n k) = LE_block (le_tm M)"
proof (intro allI impI)
fix k
assume klt: "k < k_tm M"
let ?a = "ts k (n k)"
obtain l h r where buf_k: "buf k = (l, h, r)"
by (cases "buf k") auto
assume act_le:
"fst (ae_ss6_action (le_tm M) ?a (buf k) (dest k))
= LE_block (le_tm M)"
show "?a = LE_block (le_tm M)"
proof (cases "?a = LE_block (le_tm M)")
case True thus ?thesis .
next
case a_neq: False
show ?thesis
proof (cases "h = LE_block (le_tm M)")
case h_le: True
from a_neq h_le buf_k have
"fst (ae_ss6_action (le_tm M) ?a (buf k) (dest k)) = ?a"
by simp
with act_le show ?thesis by simp
next
case h_neq: False
show ?thesis
proof (cases "dest k = AE_Left")
case ds_l: True
from a_neq h_neq ds_l buf_k have
"fst (ae_ss6_action (le_tm M) ?a (buf k) (dest k)) = r"
by simp
with act_le have "r = LE_block (le_tm M)" by simp
with r_not_le[rule_format, OF klt] buf_k have False by simp
thus ?thesis ..
next
case ds_nl: False
from a_neq h_neq ds_nl buf_k have
"fst (ae_ss6_action (le_tm M) ?a (buf k) (dest k)) = l"
by simp
with act_le have l_le: "l = LE_block (le_tm M)" by simp
have "fst (buf k) = l" using buf_k by simp
with l_le ds_nl l_guard[rule_format, OF klt] show ?thesis by simp
qed
qed
qed
qed
show ?thesis
using body unfolding ae_le_compat_ss6_def c'_eq by simp
qed
lemma ae_position_link_discharges_ss7:
fixes M :: "('q, 'a) mttm"
and c' :: "('c :: enum ⇒ 'a,
'q × ('a, 'c) ae_stage) mt_config"
assumes inv: "ae_inv_ss7 M c'"
and pos: "ae_position_link M c'"
shows "ae_le_compat_ss7 M c'"
proof -
obtain q ofs buf dest where
state_eq: "mt_state c' = (q, ofs, buf, dest, SS7)"
using inv unfolding ae_inv_ss7_def
by (cases "mt_state c'") auto
obtain ts n where
c'_eq: "c' = Config⇩M (q, ofs, buf, dest, SS7) ts n"
using state_eq by (cases c') auto
have r_not_le: "∀k<k_tm M. snd (snd (buf k)) ≠ LE_block (le_tm M)"
using pos state_eq unfolding ae_position_link_def by simp
have body:
"∀k<k_tm M. fst (ae_ss7_action (le_tm M) (ts k (n k)) (buf k) (dest k))
= LE_block (le_tm M)
⟶ ts k (n k) = LE_block (le_tm M)"
proof (intro allI impI)
fix k
assume klt: "k < k_tm M"
let ?a = "ts k (n k)"
obtain l h r where buf_k: "buf k = (l, h, r)"
by (cases "buf k") auto
assume act_le:
"fst (ae_ss7_action (le_tm M) ?a (buf k) (dest k))
= LE_block (le_tm M)"
show "?a = LE_block (le_tm M)"
proof (cases "?a = LE_block (le_tm M)")
case True thus ?thesis .
next
case a_neq: False
show ?thesis
proof (cases "h = LE_block (le_tm M)")
case h_le: True
from a_neq h_le buf_k have
"fst (ae_ss7_action (le_tm M) ?a (buf k) (dest k)) = r"
by simp
with act_le have "r = LE_block (le_tm M)" by simp
with r_not_le[rule_format, OF klt] buf_k have False by simp
thus ?thesis ..
next
case h_neq: False
from a_neq h_neq buf_k have
"fst (ae_ss7_action (le_tm M) ?a (buf k) (dest k)) = ?a"
by simp
with act_le show ?thesis by simp
qed
qed
qed
show ?thesis
using body unfolding ae_le_compat_ss7_def c'_eq by simp
qed
lemma ae_position_link_discharges_ss8:
fixes M :: "('q, 'a) mttm"
and c' :: "('c :: enum ⇒ 'a,
'q × ('a, 'c) ae_stage) mt_config"
assumes inv: "ae_inv_ss8 M c'"
and pos: "ae_position_link M c'"
shows "ae_le_compat_ss8 M c'"
proof -
obtain q ofs buf dest where
state_eq: "mt_state c' = (q, ofs, buf, dest, SS8)"
using inv unfolding ae_inv_ss8_def
by (cases "mt_state c'") auto
obtain ts n where
c'_eq: "c' = Config⇩M (q, ofs, buf, dest, SS8) ts n"
using state_eq by (cases c') auto
have r_not_le: "∀k<k_tm M. snd (snd (buf k)) ≠ LE_block (le_tm M)"
using pos state_eq unfolding ae_position_link_def by simp
have l_guard:
"∀k<k_tm M. dest k = AE_Left
⟶ fst (buf k) = LE_block (le_tm M)
⟶ ts k (n k) = LE_block (le_tm M)"
using pos state_eq c'_eq unfolding ae_position_link_def by simp
have body:
"∀k<k_tm M. fst (ae_ss8_action (le_tm M) (ts k (n k)) (buf k) (dest k))
= LE_block (le_tm M)
⟶ ts k (n k) = LE_block (le_tm M)"
proof (intro allI impI)
fix k
assume klt: "k < k_tm M"
let ?a = "ts k (n k)"
obtain l h r where buf_k: "buf k = (l, h, r)"
by (cases "buf k") auto
assume act_le:
"fst (ae_ss8_action (le_tm M) ?a (buf k) (dest k))
= LE_block (le_tm M)"
show "?a = LE_block (le_tm M)"
proof (cases "?a = LE_block (le_tm M)")
case True thus ?thesis .
next
case a_neq: False
show ?thesis
proof (cases "h = LE_block (le_tm M)")
case h_le: True
show ?thesis
proof (cases "dest k = AE_Right")
case ds_r: True
from a_neq h_le ds_r buf_k have
"fst (ae_ss8_action (le_tm M) ?a (buf k) (dest k)) = r"
by simp
with act_le have "r = LE_block (le_tm M)" by simp
with r_not_le[rule_format, OF klt] buf_k have False by simp
thus ?thesis ..
next
case ds_nr: False
from a_neq h_le ds_nr buf_k have
"fst (ae_ss8_action (le_tm M) ?a (buf k) (dest k)) = ?a"
by simp
with act_le show ?thesis by simp
qed
next
case h_neq: False
show ?thesis
proof (cases "dest k")
case AE_Left
from a_neq h_neq AE_Left buf_k have
"fst (ae_ss8_action (le_tm M) ?a (buf k) (dest k)) = l"
by simp
with act_le have l_le: "l = LE_block (le_tm M)" by simp
have "fst (buf k) = l" using buf_k by simp
with l_le AE_Left l_guard[rule_format, OF klt] show ?thesis by simp
next
case AE_Home
from a_neq h_neq AE_Home buf_k have
"fst (ae_ss8_action (le_tm M) ?a (buf k) (dest k)) = r"
by simp
with act_le have "r = LE_block (le_tm M)" by simp
with r_not_le[rule_format, OF klt] buf_k have False by simp
thus ?thesis ..
next
case AE_Right
from a_neq h_neq AE_Right buf_k have
"fst (ae_ss8_action (le_tm M) ?a (buf k) (dest k)) = r"
by simp
with act_le have "r = LE_block (le_tm M)" by simp
with r_not_le[rule_format, OF klt] buf_k have False by simp
thus ?thesis ..
qed
qed
qed
qed
show ?thesis
using body unfolding ae_le_compat_ss8_def c'_eq by simp
qed
subsubsection ‹Pre-state idx and void-aux helpers›
text ‹Pre-state idx determinations for the three substantive
sub-deltas of ‹ae_step_alphabet_enlarge_position_link_preserve›'s
aux hypotheses. Used by the chain proof to discharge vacuous-aux
cases of the preservation lemma: when the actual sub-step is e.g.
‹ss1→ss2›, the pre-state idx is SS1 ‹≠› SS4, so
the ‹aux_ss4_ss5› antecedent is unsatisfiable.›
lemma ae_delta_ss4_ss5_pre_idx:
assumes "(s, a, s', a', d) ∈ ae_delta_ss4_ss5 M"
shows "snd (snd (snd (snd s))) = SS4"
using assms unfolding ae_delta_ss4_ss5_def by force
lemma ae_delta_ss5_ss6_pre_idx:
assumes "(s, a, s', a', d) ∈ ae_delta_ss5_ss6 M"
shows "snd (snd (snd (snd s))) = SS5"
using assms unfolding ae_delta_ss5_ss6_def by force
lemma ae_delta_ss7_ss8_pre_idx:
assumes "(s, a, s', a', d) ∈ ae_delta_ss7_ss8 M"
shows "snd (snd (snd (snd s))) = SS7"
using assms unfolding ae_delta_ss7_ss8_def by force
text ‹Vacuous-aux helpers: when the actual sub-step is not
SS4‹→›SS5 / SS5‹→›SS6 / SS7‹→›SS8
(per the pre-state idx), the corresponding aux antecedent of
‹ae_step_alphabet_enlarge_position_link_preserve› is
unsatisfiable, so the aux holds vacuously. Used in the chain
proof to discharge the three aux hypotheses at substeps whose
pre-state idx doesn't match.›
lemma ae_pos_link_aux_void_ss4_ss5:
fixes M :: "('q, 'a) mttm"
and c_pre c_post :: "('c :: enum ⇒ 'a,
'q × ('a, 'c) ae_stage) mt_config"
assumes pre_neq: "snd (snd (snd (snd (mt_state c_pre)))) ≠ SS4"
and step: "(c_pre, c_post) ∈ mttm_step (ae_delta_ss4_ss5 M)"
shows "ae_position_link M c_post"
proof -
from step obtain s ts n s' a' d where
eq: "c_pre = Config⇩M s ts n"
and rel: "(s, (λk. ts k (n k)), s', a', d) ∈ ae_delta_ss4_ss5 M"
by (auto elim: mttm_step.cases)
have "snd (snd (snd (snd s))) = SS4"
using ae_delta_ss4_ss5_pre_idx[OF rel] .
with eq pre_neq have False by simp
thus ?thesis ..
qed
lemma ae_pos_link_aux_void_ss5_ss6:
fixes M :: "('q, 'a) mttm"
and c_pre c_post :: "('c :: enum ⇒ 'a,
'q × ('a, 'c) ae_stage) mt_config"
assumes pre_neq: "snd (snd (snd (snd (mt_state c_pre)))) ≠ SS5"
and step: "(c_pre, c_post) ∈ mttm_step (ae_delta_ss5_ss6 M)"
shows "ae_position_link M c_post"
proof -
from step obtain s ts n s' a' d where
eq: "c_pre = Config⇩M s ts n"
and rel: "(s, (λk. ts k (n k)), s', a', d) ∈ ae_delta_ss5_ss6 M"
by (auto elim: mttm_step.cases)
have "snd (snd (snd (snd s))) = SS5"
using ae_delta_ss5_ss6_pre_idx[OF rel] .
with eq pre_neq have False by simp
thus ?thesis ..
qed
lemma ae_pos_link_aux_void_ss7_ss8:
fixes M :: "('q, 'a) mttm"
and c_pre c_post :: "('c :: enum ⇒ 'a,
'q × ('a, 'c) ae_stage) mt_config"
assumes pre_neq: "snd (snd (snd (snd (mt_state c_pre)))) ≠ SS7"
and step: "(c_pre, c_post) ∈ mttm_step (ae_delta_ss7_ss8 M)"
shows "ae_position_link M c_post"
proof -
from step obtain s ts n s' a' d where
eq: "c_pre = Config⇩M s ts n"
and rel: "(s, (λk. ts k (n k)), s', a', d) ∈ ae_delta_ss7_ss8 M"
by (auto elim: mttm_step.cases)
have "snd (snd (snd (snd s))) = SS7"
using ae_delta_ss7_ss8_pre_idx[OF rel] .
with eq pre_neq have False by simp
thus ?thesis ..
qed
subsubsection ‹Position-link preservation›
text ‹Preservation of ‹ae_position_link› under a single
‹mttm_step› via ‹alphabet_enlarge_delta›. The proof
case-splits on which of the 16 sub-deltas fires. Validation
transitions (8) and simulation transitions whose post-idx is
outside the post-buffer-load regime
(‹ss1→ss2›, ‹ss2→ss3›,
‹ss3→ss4›, ‹ss8→ss1›) close
vacuously — the predicate's content is conditional on
‹idx ∈› ‹{SS5, SS6, SS7, SS8}›. The buffer-stable
transition ‹ss6→ss7› closes by transferring the
pre-state's ‹r ≠ LE_block› across the buffer-preserving
step. The three substantive transitions ‹ss4→ss5›,
‹ss5→ss6›, ‹ss7→ss8› require
auxiliary hypotheses that the chain proof discharges from the
broader simulation context (‹m_steps_buffered_correct›'s
‹δ›LE preservation, the buffer-load invariants, and
the cadence at SS5/SS7 entry).›
lemma ae_step_alphabet_enlarge_position_link_preserve:
fixes M :: "('q, 'a) mttm"
and c' c'' :: "('c :: enum ⇒ 'a,
'q × ('a, 'c) ae_stage) mt_config"
assumes pre: "ae_position_link M c'"
and step: "(c', c'') ∈ mttm_step (alphabet_enlarge_delta M)"
and aux_ss4_ss5:
"(c', c'') ∈ mttm_step (ae_delta_ss4_ss5 M)
⟹ ae_position_link M c''"
and aux_ss5_ss6:
"(c', c'') ∈ mttm_step (ae_delta_ss5_ss6 M)
⟹ ae_position_link M c''"
and aux_ss7_ss8:
"(c', c'') ∈ mttm_step (ae_delta_ss7_ss8 M)
⟹ ae_position_link M c''"
shows "ae_position_link M c''"
proof -
obtain s ts n s' a' d where
rel: "(s, (λk. ts k (n k)), s', a', d) ∈ alphabet_enlarge_delta M"
and c'_eq: "c' = Config⇩M s ts n"
and c''_eq: "c'' = Config⇩M s' (λk. (ts k)(n k := a' k))
(λk. go_dir (d k) (n k))"
using step by (auto elim: mttm_step.cases)
let ?rel_tup = "(s, (λk. ts k (n k)), s', a', d)"
consider
(vfa) "?rel_tup ∈ ae_delta_val_fwd_advance M"
| (vfp) "?rel_tup ∈ ae_delta_val_fwd_to_padded M"
| (vfr) "?rel_tup ∈ ae_delta_val_fwd_reject M"
| (vfr2) "?rel_tup ∈ ae_delta_val_fwd_to_ret M"
| (vpr) "?rel_tup ∈ ae_delta_val_pad_to_ret M"
| (vpr2) "?rel_tup ∈ ae_delta_val_pad_reject M"
| (vrs) "?rel_tup ∈ ae_delta_val_ret_step M"
| (vrts) "?rel_tup ∈ ae_delta_val_ret_to_sim M"
| (s12) "?rel_tup ∈ ae_delta_ss1_ss2 M"
| (s23) "?rel_tup ∈ ae_delta_ss2_ss3 M"
| (s34) "?rel_tup ∈ ae_delta_ss3_ss4 M"
| (s45) "?rel_tup ∈ ae_delta_ss4_ss5 M"
| (s56) "?rel_tup ∈ ae_delta_ss5_ss6 M"
| (s67) "?rel_tup ∈ ae_delta_ss6_ss7 M"
| (s78) "?rel_tup ∈ ae_delta_ss7_ss8 M"
| (s81) "?rel_tup ∈ ae_delta_ss8_ss1 M"
using rel unfolding alphabet_enlarge_delta_def by blast
thus ?thesis
proof cases
case vfa
thus ?thesis
using c''_eq unfolding ae_position_link_def ae_delta_val_fwd_advance_def
by auto
next
case vfp
thus ?thesis
using c''_eq unfolding ae_position_link_def ae_delta_val_fwd_to_padded_def
by auto
next
case vfr
thus ?thesis
using c''_eq
unfolding ae_position_link_def ae_delta_val_fwd_reject_def init_stage_def
by auto
next
case vfr2
thus ?thesis
using c''_eq unfolding ae_position_link_def ae_delta_val_fwd_to_ret_def
by auto
next
case vpr
thus ?thesis
using c''_eq unfolding ae_position_link_def ae_delta_val_pad_to_ret_def
by auto
next
case vpr2
thus ?thesis
using c''_eq
unfolding ae_position_link_def ae_delta_val_pad_reject_def init_stage_def
by auto
next
case vrs
thus ?thesis
using c''_eq unfolding ae_position_link_def ae_delta_val_ret_step_def
by auto
next
case vrts
thus ?thesis
using c''_eq unfolding ae_position_link_def ae_delta_val_ret_to_sim_def
by auto
next
case s12
thus ?thesis
using c''_eq unfolding ae_position_link_def ae_delta_ss1_ss2_def
by auto
next
case s23
thus ?thesis
using c''_eq unfolding ae_position_link_def ae_delta_ss2_ss3_def
by auto
next
case s34
thus ?thesis
using c''_eq unfolding ae_position_link_def ae_delta_ss3_ss4_def
by auto
next
case s45
have step_s45: "(c', c'') ∈ mttm_step (ae_delta_ss4_ss5 M)"
using s45 c'_eq c''_eq by (auto intro: mttm_step.intros)
thus ?thesis by (rule aux_ss4_ss5)
next
case s56
have step_s56: "(c', c'') ∈ mttm_step (ae_delta_ss5_ss6 M)"
using s56 c'_eq c''_eq by (auto intro: mttm_step.intros)
thus ?thesis by (rule aux_ss5_ss6)
next
case s67
obtain q ofs buf dest where
pre_state: "s = (q, ofs, buf, dest, SS6)"
and post_state: "s' = (q, ofs, buf, dest, SS7)"
using s67 unfolding ae_delta_ss6_ss7_def by auto
have pre_state': "mt_state c' = (q, ofs, buf, dest, SS6)"
using c'_eq pre_state by simp
have post_state': "mt_state c'' = (q, ofs, buf, dest, SS7)"
using c''_eq post_state by simp
have r_not_le:
"∀k<k_tm M. snd (snd (buf k)) ≠ LE_block (le_tm M)"
using pre pre_state' unfolding ae_position_link_def by simp
show ?thesis
unfolding ae_position_link_def post_state'
using r_not_le by simp
next
case s78
have step_s78: "(c', c'') ∈ mttm_step (ae_delta_ss7_ss8 M)"
using s78 c'_eq c''_eq by (auto intro: mttm_step.intros)
thus ?thesis by (rule aux_ss7_ss8)
next
case s81
obtain q ofs buf dest where
pre_state: "s = (q, ofs, buf, dest, SS8)"
and post_state:
"s' = (q, if q ∈ {t_tm M, r_tm M}
then init_stage (le_tm M)
else (ofs, buf, init_dest, SS1))"
using s81 unfolding ae_delta_ss8_ss1_def by auto
show ?thesis
proof (cases "q ∈ {t_tm M, r_tm M}")
case True
hence "s' = (q, init_stage (le_tm M))" using post_state by simp
thus ?thesis
using c''_eq
unfolding ae_position_link_def init_stage_def
by auto
next
case False
hence "s' = (q, ofs, buf, init_dest, SS1)" using post_state by simp
thus ?thesis
using c''_eq
unfolding ae_position_link_def
by auto
qed
qed
qed
subsubsection ‹Per-substep step-existence›
text ‹Per-substep step-existence lemmas (forward simulation,
buffer phase). Each lemma, given a configuration ‹c'›
satisfying the appropriate ‹ae_inv_ss<N>› precondition (plus
whichever side-band invariants the substep requires), produces
a witness ‹c''› for which both the per-substep step
‹mttm_step (ae_delta_ss<N>_ss<N+1> M)› and the full-delta
step ‹mttm_step (alphabet_enlarge_delta M)› hold. Per-substep
delta is forwarded to the existing
‹ae_step_ss<N>_ss<N+1>_invariant› lemma at the chain
orchestration site (‹ae_simulates_forward_stage›);
full-delta step accumulates into the chain's
‹mttm_step⇧*› closure.
Hypothesis pattern by substep:
▪ SS1‹→›SS2, SS2‹→›SS3,
SS3‹→›SS4 (buffer-load): ‹ae_inv_ss<N>› +
‹ae_tape_in_gamma_block› + non-halt; substrate write is a
no-op (‹a' = a›).
▪ SS4‹→›SS5 (c-fold compute): adds ‹valid_mttm›,
‹delta_total›, the per-tape ‹ae_window_invariant›, and a
no-LE-in-window hypothesis; the substrate witness is obtained
by invoking ‹ae_m_steps_buffered_correct›. Substrate write
is still a no-op. Located in
‹AlphabetEnlargement› rather than this theory because
‹ae_m_steps_buffered_correct› lives there.
▪ SS5‹→›SS6 (write-back, first cell):
‹ae_inv_ss5› + ‹ae_tape_in_gamma_block› +
‹ae_buffer_in_gamma_block›; no non-halt hypothesis (the
SS5 action is total in its inputs; halt routing kicks in only
at SS8‹→›SS1).
▪ SS6‹→›SS7 (write-back, side cell):
‹ae_inv_ss6› + ‹ae_tape_in_gamma_block› +
‹ae_buffer_in_gamma_block› + ‹ae_le_compat_ss6›.
The fourth hypothesis is the per-substep LE-no-write
contract (the action returns the buffer's ‹l› or ‹r› slot
in steady-state, and gamma-block alone does not preclude
‹l, r ∈ LE_block›).
▪ SS7‹→›SS8: same shape as SS6, with
‹ae_le_compat_ss7›.
▪ SS8‹→›SS1: same shape, with
‹ae_le_compat_ss8›; halt-aware destination routing is
internal to ‹ae_delta_ss8_ss1›'s ‹stage'› if-then-else,
so step-existence is uniform across halt and non-halt.›
lemma ae_step_ss1_ss2_exists:
fixes M :: "('q, 'a) mttm"
and c' :: "('c :: enum ⇒ 'a,
'q × ('a, 'c) ae_stage) mt_config"
assumes inv: "ae_inv_ss1 M c'"
and gamma: "ae_tape_in_gamma_block M c'"
and buf: "ae_buffer_in_gamma_block M c'"
and q_neq_t: "fst (mt_state c') ≠ t_tm M"
and q_neq_r: "fst (mt_state c') ≠ r_tm M"
shows "∃c''. (c', c'') ∈ mttm_step (ae_delta_ss1_ss2 M)
∧ (c', c'') ∈ mttm_step (alphabet_enlarge_delta M)"
proof -
obtain q ofs buf dest where
state_eq: "mt_state c' = (q, ofs, buf, dest, SS1)"
and q_in: "q ∈ Q_tm M"
using inv unfolding ae_inv_ss1_def
by (cases "mt_state c'") auto
obtain ts n where c'_eq: "c' = Config⇩M (q, ofs, buf, dest, SS1) ts n"
using state_eq by (cases c') auto
let ?a = "λk. ts k (n k)"
let ?buf' = "λk. if k < k_tm M
then (fst (buf k), ?a k, snd (snd (buf k)))
else init_buffer (le_tm M) k"
let ?d = "λk. if k < k_tm M
then (if ?a k = LE_block (le_tm M) then dir.N else dir.L)
else dir.N"
have q_neq_t': "q ≠ t_tm M" using q_neq_t state_eq by simp
have q_neq_r': "q ≠ r_tm M" using q_neq_r state_eq by simp
have a_tail: "∀j≥k_tm M. ?a j = bl_block (bl_tm M)"
using gamma c'_eq unfolding ae_tape_in_gamma_block_def by simp
have rel_in: "((q, ofs, buf, dest, SS1), ?a,
(q, ofs, ?buf', dest, SS2), ?a, ?d)
∈ ae_delta_ss1_ss2 M"
unfolding ae_delta_ss1_ss2_def
using q_in q_neq_t' q_neq_r' a_tail by auto
have gamma_a: "∀k. ?a k ∈ gamma_block (Γ_tm M)"
using gamma c'_eq unfolding ae_tape_in_gamma_block_def by simp
have src_valid: "ae_valid_stage (Γ_tm M) (le_tm M) (k_tm M)
(snd ((q, ofs, buf, dest, SS1)
:: 'q × ('a, 'c) ae_stage))"
using buf state_eq
unfolding ae_buffer_in_gamma_block_def ae_valid_stage_def by simp
have dst_valid: "ae_valid_stage (Γ_tm M) (le_tm M) (k_tm M)
(snd ((q, ofs, ?buf', dest, SS2)
:: 'q × ('a, 'c) ae_stage))"
by (rule ae_delta_ss1_ss2_dest_valid[OF rel_in gamma_a src_valid])
have aed_in: "((q, ofs, buf, dest, SS1), ?a,
(q, ofs, ?buf', dest, SS2), ?a, ?d)
∈ alphabet_enlarge_delta M"
unfolding alphabet_enlarge_delta_def
using rel_in gamma_a src_valid dst_valid by auto
have ts_unchanged: "(λk. (ts k)(n k := ?a k)) = ts"
by (rule ext) auto
let ?c'' = "Config⇩M (q, ofs, ?buf', dest, SS2) ts
(λk. go_dir (?d k) (n k))"
have step_sub_raw:
"(Config⇩M (q, ofs, buf, dest, SS1) ts n,
Config⇩M (q, ofs, ?buf', dest, SS2)
(λk. (ts k)(n k := ?a k))
(λk. go_dir (?d k) (n k)))
∈ mttm_step (ae_delta_ss1_ss2 M)"
proof (rule mttm_step.intros)
show "((q, ofs, buf, dest, SS1), ?a,
(q, ofs, ?buf', dest, SS2), ?a, ?d)
∈ ae_delta_ss1_ss2 M" by (rule rel_in)
qed
have step_sub: "(c', ?c'') ∈ mttm_step (ae_delta_ss1_ss2 M)"
using step_sub_raw c'_eq ts_unchanged by simp
have step_full_raw:
"(Config⇩M (q, ofs, buf, dest, SS1) ts n,
Config⇩M (q, ofs, ?buf', dest, SS2)
(λk. (ts k)(n k := ?a k))
(λk. go_dir (?d k) (n k)))
∈ mttm_step (alphabet_enlarge_delta M)"
proof (rule mttm_step.intros)
show "((q, ofs, buf, dest, SS1), ?a,
(q, ofs, ?buf', dest, SS2), ?a, ?d)
∈ alphabet_enlarge_delta M" by (rule aed_in)
qed
have step_full: "(c', ?c'') ∈ mttm_step (alphabet_enlarge_delta M)"
using step_full_raw c'_eq ts_unchanged by simp
show ?thesis using step_sub step_full by blast
qed
lemma ae_step_ss2_ss3_exists:
fixes M :: "('q, 'a) mttm"
and c' :: "('c :: enum ⇒ 'a,
'q × ('a, 'c) ae_stage) mt_config"
assumes vM: "valid_mttm M"
and inv: "ae_inv_ss2 M c'"
and gamma: "ae_tape_in_gamma_block M c'"
and buf: "ae_buffer_in_gamma_block M c'"
and q_neq_t: "fst (mt_state c') ≠ t_tm M"
and q_neq_r: "fst (mt_state c') ≠ r_tm M"
shows "∃c''. (c', c'') ∈ mttm_step (ae_delta_ss2_ss3 M)
∧ (c', c'') ∈ mttm_step (alphabet_enlarge_delta M)"
proof -
obtain q ofs buf dest where
state_eq: "mt_state c' = (q, ofs, buf, dest, SS2)"
and q_in: "q ∈ Q_tm M"
using inv unfolding ae_inv_ss2_def
by (cases "mt_state c'") auto
obtain ts n where c'_eq: "c' = Config⇩M (q, ofs, buf, dest, SS2) ts n"
using state_eq by (cases c') auto
let ?a = "λk. ts k (n k)"
let ?buf' = "λk. if k < k_tm M
then (let (l, h, r) = buf k in
(if h = LE_block (le_tm M)
then bl_block (bl_tm M)
else ?a k,
h, r))
else init_buffer (le_tm M) k"
let ?d = "λk. if k < k_tm M
then (if (fst (snd (buf k))) = LE_block (le_tm M)
then dir.N else dir.R)
else dir.N"
have q_neq_t': "q ≠ t_tm M" using q_neq_t state_eq by simp
have q_neq_r': "q ≠ r_tm M" using q_neq_r state_eq by simp
have a_tail: "∀j≥k_tm M. ?a j = bl_block (bl_tm M)"
using gamma c'_eq unfolding ae_tape_in_gamma_block_def by simp
have rel_in: "((q, ofs, buf, dest, SS2), ?a,
(q, ofs, ?buf', dest, SS3), ?a, ?d)
∈ ae_delta_ss2_ss3 M"
unfolding ae_delta_ss2_ss3_def
using q_in q_neq_t' q_neq_r' a_tail by auto
have gamma_a: "∀k. ?a k ∈ gamma_block (Γ_tm M)"
using gamma c'_eq unfolding ae_tape_in_gamma_block_def by simp
have src_valid: "ae_valid_stage (Γ_tm M) (le_tm M) (k_tm M)
(snd ((q, ofs, buf, dest, SS2)
:: 'q × ('a, 'c) ae_stage))"
using buf state_eq
unfolding ae_buffer_in_gamma_block_def ae_valid_stage_def by simp
have dst_valid: "ae_valid_stage (Γ_tm M) (le_tm M) (k_tm M)
(snd ((q, ofs, ?buf', dest, SS3)
:: 'q × ('a, 'c) ae_stage))"
by (rule ae_delta_ss2_ss3_dest_valid[OF vM rel_in gamma_a src_valid])
have aed_in: "((q, ofs, buf, dest, SS2), ?a,
(q, ofs, ?buf', dest, SS3), ?a, ?d)
∈ alphabet_enlarge_delta M"
unfolding alphabet_enlarge_delta_def
using rel_in gamma_a src_valid dst_valid by auto
have ts_unchanged: "(λk. (ts k)(n k := ?a k)) = ts"
by (rule ext) auto
let ?c'' = "Config⇩M (q, ofs, ?buf', dest, SS3) ts
(λk. go_dir (?d k) (n k))"
have step_sub_raw:
"(Config⇩M (q, ofs, buf, dest, SS2) ts n,
Config⇩M (q, ofs, ?buf', dest, SS3)
(λk. (ts k)(n k := ?a k))
(λk. go_dir (?d k) (n k)))
∈ mttm_step (ae_delta_ss2_ss3 M)"
proof (rule mttm_step.intros)
show "((q, ofs, buf, dest, SS2), ?a,
(q, ofs, ?buf', dest, SS3), ?a, ?d)
∈ ae_delta_ss2_ss3 M" by (rule rel_in)
qed
have step_sub: "(c', ?c'') ∈ mttm_step (ae_delta_ss2_ss3 M)"
using step_sub_raw c'_eq ts_unchanged by simp
have step_full_raw:
"(Config⇩M (q, ofs, buf, dest, SS2) ts n,
Config⇩M (q, ofs, ?buf', dest, SS3)
(λk. (ts k)(n k := ?a k))
(λk. go_dir (?d k) (n k)))
∈ mttm_step (alphabet_enlarge_delta M)"
proof (rule mttm_step.intros)
show "((q, ofs, buf, dest, SS2), ?a,
(q, ofs, ?buf', dest, SS3), ?a, ?d)
∈ alphabet_enlarge_delta M" by (rule aed_in)
qed
have step_full: "(c', ?c'') ∈ mttm_step (alphabet_enlarge_delta M)"
using step_full_raw c'_eq ts_unchanged by simp
show ?thesis using step_sub step_full by blast
qed
lemma ae_step_ss3_ss4_exists:
fixes M :: "('q, 'a) mttm"
and c' :: "('c :: enum ⇒ 'a,
'q × ('a, 'c) ae_stage) mt_config"
assumes inv: "ae_inv_ss3 M c'"
and gamma: "ae_tape_in_gamma_block M c'"
and buf: "ae_buffer_in_gamma_block M c'"
and q_neq_t: "fst (mt_state c') ≠ t_tm M"
and q_neq_r: "fst (mt_state c') ≠ r_tm M"
shows "∃c''. (c', c'') ∈ mttm_step (ae_delta_ss3_ss4 M)
∧ (c', c'') ∈ mttm_step (alphabet_enlarge_delta M)"
proof -
obtain q ofs buf dest where
state_eq: "mt_state c' = (q, ofs, buf, dest, SS3)"
and q_in: "q ∈ Q_tm M"
using inv unfolding ae_inv_ss3_def
by (cases "mt_state c'") auto
obtain ts n where c'_eq: "c' = Config⇩M (q, ofs, buf, dest, SS3) ts n"
using state_eq by (cases c') auto
let ?a = "λk. ts k (n k)"
let ?d = "λk. if k < k_tm M then dir.R else dir.N"
have q_neq_t': "q ≠ t_tm M" using q_neq_t state_eq by simp
have q_neq_r': "q ≠ r_tm M" using q_neq_r state_eq by simp
have a_tail: "∀j≥k_tm M. ?a j = bl_block (bl_tm M)"
using gamma c'_eq unfolding ae_tape_in_gamma_block_def by simp
have rel_in: "((q, ofs, buf, dest, SS3), ?a,
(q, ofs, buf, dest, SS4), ?a, ?d)
∈ ae_delta_ss3_ss4 M"
unfolding ae_delta_ss3_ss4_def
using q_in q_neq_t' q_neq_r' a_tail by auto
have gamma_a: "∀k. ?a k ∈ gamma_block (Γ_tm M)"
using gamma c'_eq unfolding ae_tape_in_gamma_block_def by simp
have src_valid: "ae_valid_stage (Γ_tm M) (le_tm M) (k_tm M)
(snd ((q, ofs, buf, dest, SS3)
:: 'q × ('a, 'c) ae_stage))"
using buf state_eq
unfolding ae_buffer_in_gamma_block_def ae_valid_stage_def by simp
have dst_valid: "ae_valid_stage (Γ_tm M) (le_tm M) (k_tm M)
(snd ((q, ofs, buf, dest, SS4)
:: 'q × ('a, 'c) ae_stage))"
by (rule ae_delta_ss3_ss4_dest_valid[OF rel_in src_valid])
have aed_in: "((q, ofs, buf, dest, SS3), ?a,
(q, ofs, buf, dest, SS4), ?a, ?d)
∈ alphabet_enlarge_delta M"
unfolding alphabet_enlarge_delta_def
using rel_in gamma_a src_valid dst_valid by auto
have ts_unchanged: "(λk. (ts k)(n k := ?a k)) = ts"
by (rule ext) auto
let ?c'' = "Config⇩M (q, ofs, buf, dest, SS4) ts
(λk. go_dir (?d k) (n k))"
have step_sub_raw:
"(Config⇩M (q, ofs, buf, dest, SS3) ts n,
Config⇩M (q, ofs, buf, dest, SS4)
(λk. (ts k)(n k := ?a k))
(λk. go_dir (?d k) (n k)))
∈ mttm_step (ae_delta_ss3_ss4 M)"
proof (rule mttm_step.intros)
show "((q, ofs, buf, dest, SS3), ?a,
(q, ofs, buf, dest, SS4), ?a, ?d)
∈ ae_delta_ss3_ss4 M" by (rule rel_in)
qed
have step_sub: "(c', ?c'') ∈ mttm_step (ae_delta_ss3_ss4 M)"
using step_sub_raw c'_eq ts_unchanged by simp
have step_full_raw:
"(Config⇩M (q, ofs, buf, dest, SS3) ts n,
Config⇩M (q, ofs, buf, dest, SS4)
(λk. (ts k)(n k := ?a k))
(λk. go_dir (?d k) (n k)))
∈ mttm_step (alphabet_enlarge_delta M)"
proof (rule mttm_step.intros)
show "((q, ofs, buf, dest, SS3), ?a,
(q, ofs, buf, dest, SS4), ?a, ?d)
∈ alphabet_enlarge_delta M" by (rule aed_in)
qed
have step_full: "(c', ?c'') ∈ mttm_step (alphabet_enlarge_delta M)"
using step_full_raw c'_eq ts_unchanged by simp
show ?thesis using step_sub step_full by blast
qed
text ‹SS5‹→›SS6 step-existence. The first of the write-back
substeps' step-existence cluster (SS5‹→›SS6, SS6‹→›SS7,
SS7‹→›SS8) — each writes a buffer cell back to the tape, so
each needs ‹ae_buffer_in_gamma_block› to discharge the
‹alphabet_enlarge_delta› intersection guard's
‹a' k ∈ gamma_block› obligation.
The SS5 action is total in its inputs (no halt-state
precondition), so unlike the buffer-load substeps (SS1‹→›SS4)
the lemma does not need ‹q_neq_t›/‹q_neq_r› hypotheses.
Halt routing kicks in only at SS8‹→›SS1.›
lemma ae_step_ss5_ss6_exists:
fixes M :: "('q, 'a) mttm"
and c' :: "('c :: enum ⇒ 'a,
'q × ('a, 'c) ae_stage) mt_config"
assumes inv: "ae_inv_ss5 M c'"
and gamma: "ae_tape_in_gamma_block M c'"
and buf: "ae_buffer_in_gamma_block M c'"
shows "∃c''. (c', c'') ∈ mttm_step (ae_delta_ss5_ss6 M)
∧ (c', c'') ∈ mttm_step (alphabet_enlarge_delta M)"
proof -
obtain q ofs buf dest where
state_eq: "mt_state c' = (q, ofs, buf, dest, SS5)"
and q_in: "q ∈ Q_tm M"
using inv unfolding ae_inv_ss5_def
by (cases "mt_state c'") auto
obtain ts n where c'_eq: "c' = Config⇩M (q, ofs, buf, dest, SS5) ts n"
using state_eq by (cases c') auto
let ?a = "λk. ts k (n k)"
let ?a' = "λk. if k < k_tm M
then fst (ae_ss5_action (le_tm M) (?a k) (buf k) (dest k))
else bl_block (bl_tm M)"
let ?d = "λk. if k < k_tm M
then snd (ae_ss5_action (le_tm M) (?a k) (buf k) (dest k))
else dir.N"
have a_tail: "∀j≥k_tm M. ?a j = bl_block (bl_tm M)"
using gamma c'_eq unfolding ae_tape_in_gamma_block_def by simp
have rel_in: "((q, ofs, buf, dest, SS5), ?a,
(q, ofs, buf, dest, SS6), ?a', ?d)
∈ ae_delta_ss5_ss6 M"
unfolding ae_delta_ss5_ss6_def using q_in a_tail by auto
have gamma_a: "∀k. ?a k ∈ gamma_block (Γ_tm M)"
using gamma c'_eq unfolding ae_tape_in_gamma_block_def by simp
have h_gamma: "∀k. fst (snd (buf k)) ∈ gamma_block (Γ_tm M)"
using buf state_eq unfolding ae_buffer_in_gamma_block_def by simp
have act_gamma: "∀k. fst (ae_ss5_action (le_tm M) (?a k) (buf k) (dest k))
∈ gamma_block (Γ_tm M)"
proof (intro allI)
fix k
obtain l h r where buf_k: "buf k = (l, h, r)"
by (cases "buf k") auto
have h_in_gamma: "h ∈ gamma_block (Γ_tm M)"
using spec[OF h_gamma, of k] buf_k by simp
have a_k_in_gamma: "?a k ∈ gamma_block (Γ_tm M)"
using spec[OF gamma_a, of k] by simp
show "fst (ae_ss5_action (le_tm M) (?a k) (buf k) (dest k))
∈ gamma_block (Γ_tm M)"
proof (cases "?a k = LE_block (le_tm M)")
case True
thus ?thesis using a_k_in_gamma buf_k by simp
next
case a_neq_le: False
show ?thesis
proof (cases "h = LE_block (le_tm M)")
case True
thus ?thesis using a_neq_le a_k_in_gamma buf_k by simp
next
case False
thus ?thesis using a_neq_le h_in_gamma buf_k by simp
qed
qed
qed
have gamma_a': "∀k. ?a' k ∈ gamma_block (Γ_tm M)"
proof (intro allI)
fix k
show "?a' k ∈ gamma_block (Γ_tm M)"
proof (cases "k < k_tm M")
case True thus ?thesis using spec[OF act_gamma, of k] by simp
next
case False
hence "?a' k = ?a k" using a_tail by simp
thus ?thesis using spec[OF gamma_a, of k] by simp
qed
qed
have act_le: "∀k. fst (ae_ss5_action (le_tm M) (?a k) (buf k) (dest k))
= LE_block (le_tm M)
⟶ ?a k = LE_block (le_tm M)"
proof (intro allI impI)
fix k
assume a'_le: "fst (ae_ss5_action (le_tm M) (?a k) (buf k) (dest k))
= LE_block (le_tm M)"
obtain l h r where buf_k: "buf k = (l, h, r)"
by (cases "buf k") auto
show "?a k = LE_block (le_tm M)"
proof (cases "?a k = LE_block (le_tm M)")
case True thus ?thesis .
next
case a_neq_le: False
show ?thesis
proof (cases "h = LE_block (le_tm M)")
case True
hence "fst (ae_ss5_action (le_tm M) (?a k) (buf k) (dest k)) = ?a k"
using a_neq_le buf_k by simp
with a'_le a_neq_le show ?thesis by simp
next
case h_neq_le: False
hence "fst (ae_ss5_action (le_tm M) (?a k) (buf k) (dest k)) = h"
using a_neq_le buf_k by simp
with a'_le h_neq_le show ?thesis by simp
qed
qed
qed
have le_no_write: "∀k. ?a' k = LE_block (le_tm M)
⟶ ?a k = LE_block (le_tm M)"
proof (intro allI impI)
fix k
assume a'_le: "?a' k = LE_block (le_tm M)"
show "?a k = LE_block (le_tm M)"
proof (cases "k < k_tm M")
case True
hence "fst (ae_ss5_action (le_tm M) (?a k) (buf k) (dest k))
= LE_block (le_tm M)"
using a'_le by simp
thus ?thesis using spec[OF act_le, of k] by simp
next
case False
hence "?a k = ?a' k" using a_tail by simp
thus ?thesis using a'_le by simp
qed
qed
have src_valid: "ae_valid_stage (Γ_tm M) (le_tm M) (k_tm M)
(snd ((q, ofs, buf, dest, SS5)
:: 'q × ('a, 'c) ae_stage))"
using buf state_eq
unfolding ae_buffer_in_gamma_block_def ae_valid_stage_def by simp
have dst_valid: "ae_valid_stage (Γ_tm M) (le_tm M) (k_tm M)
(snd ((q, ofs, buf, dest, SS6)
:: 'q × ('a, 'c) ae_stage))"
by (rule ae_delta_ss5_ss6_dest_valid[OF rel_in src_valid])
have aed_in: "((q, ofs, buf, dest, SS5), ?a,
(q, ofs, buf, dest, SS6), ?a', ?d)
∈ alphabet_enlarge_delta M"
unfolding alphabet_enlarge_delta_def
using rel_in gamma_a gamma_a' le_no_write src_valid dst_valid by auto
have ts_unchanged_when_N:
"(λk. (ts k)(n k := ?a k)) = ts"
by (rule ext) auto
let ?ts' = "λk. (ts k)(n k := ?a' k)"
let ?n' = "λk. go_dir (?d k) (n k)"
let ?c'' = "Config⇩M (q, ofs, buf, dest, SS6) ?ts' ?n'"
have step_sub_raw:
"(Config⇩M (q, ofs, buf, dest, SS5) ts n,
Config⇩M (q, ofs, buf, dest, SS6) ?ts' ?n')
∈ mttm_step (ae_delta_ss5_ss6 M)"
proof (rule mttm_step.intros)
show "((q, ofs, buf, dest, SS5), ?a,
(q, ofs, buf, dest, SS6), ?a', ?d)
∈ ae_delta_ss5_ss6 M" by (rule rel_in)
qed
have step_sub: "(c', ?c'') ∈ mttm_step (ae_delta_ss5_ss6 M)"
using step_sub_raw c'_eq by simp
have step_full_raw:
"(Config⇩M (q, ofs, buf, dest, SS5) ts n,
Config⇩M (q, ofs, buf, dest, SS6) ?ts' ?n')
∈ mttm_step (alphabet_enlarge_delta M)"
proof (rule mttm_step.intros)
show "((q, ofs, buf, dest, SS5), ?a,
(q, ofs, buf, dest, SS6), ?a', ?d)
∈ alphabet_enlarge_delta M" by (rule aed_in)
qed
have step_full: "(c', ?c'') ∈ mttm_step (alphabet_enlarge_delta M)"
using step_full_raw c'_eq by simp
show ?thesis using step_sub step_full by blast
qed
text ‹Step-existence at SS6: writes the home block's previous
contents in steady-state (‹ds = AE_Left› writes ‹r›;
otherwise writes ‹l›); LE-stage branches return ‹a› idempotently.
The ‹l›/‹r› branches force the per-substep
‹ae_le_compat_ss6› hypothesis: ‹l› may legitimately equal
‹LE_block› when ‹p_start = 1›, so structural discharge fails
and the chain proof must thread the position-buffer
correspondence in.›
lemma ae_step_ss6_ss7_exists:
fixes M :: "('q, 'a) mttm"
and c' :: "('c :: enum ⇒ 'a,
'q × ('a, 'c) ae_stage) mt_config"
assumes inv: "ae_inv_ss6 M c'"
and gamma: "ae_tape_in_gamma_block M c'"
and buf: "ae_buffer_in_gamma_block M c'"
and le_compat: "ae_le_compat_ss6 M c'"
shows "∃c''. (c', c'') ∈ mttm_step (ae_delta_ss6_ss7 M)
∧ (c', c'') ∈ mttm_step (alphabet_enlarge_delta M)"
proof -
obtain q ofs buf dest where
state_eq: "mt_state c' = (q, ofs, buf, dest, SS6)"
and q_in: "q ∈ Q_tm M"
using inv unfolding ae_inv_ss6_def
by (cases "mt_state c'") auto
obtain ts n where c'_eq: "c' = Config⇩M (q, ofs, buf, dest, SS6) ts n"
using state_eq by (cases c') auto
let ?a = "λk. ts k (n k)"
let ?a' = "λk. if k < k_tm M
then fst (ae_ss6_action (le_tm M) (?a k) (buf k) (dest k))
else bl_block (bl_tm M)"
let ?d = "λk. if k < k_tm M
then snd (ae_ss6_action (le_tm M) (?a k) (buf k) (dest k))
else dir.N"
have a_tail: "∀j≥k_tm M. ?a j = bl_block (bl_tm M)"
using gamma c'_eq unfolding ae_tape_in_gamma_block_def by simp
have rel_in: "((q, ofs, buf, dest, SS6), ?a,
(q, ofs, buf, dest, SS7), ?a', ?d)
∈ ae_delta_ss6_ss7 M"
unfolding ae_delta_ss6_ss7_def using q_in a_tail by auto
have gamma_a: "∀k. ?a k ∈ gamma_block (Γ_tm M)"
using gamma c'_eq unfolding ae_tape_in_gamma_block_def by simp
have buf_gamma:
"∀k. fst (buf k) ∈ gamma_block (Γ_tm M)
∧ fst (snd (buf k)) ∈ gamma_block (Γ_tm M)
∧ snd (snd (buf k)) ∈ gamma_block (Γ_tm M)"
using buf state_eq unfolding ae_buffer_in_gamma_block_def by simp
have act_gamma: "∀k. fst (ae_ss6_action (le_tm M) (?a k) (buf k) (dest k))
∈ gamma_block (Γ_tm M)"
proof (intro allI)
fix k
obtain l h r where buf_k: "buf k = (l, h, r)"
by (cases "buf k") auto
have l_in: "l ∈ gamma_block (Γ_tm M)"
using spec[OF buf_gamma, of k] buf_k by simp
have h_in: "h ∈ gamma_block (Γ_tm M)"
using spec[OF buf_gamma, of k] buf_k by simp
have r_in: "r ∈ gamma_block (Γ_tm M)"
using spec[OF buf_gamma, of k] buf_k by simp
have a_in: "?a k ∈ gamma_block (Γ_tm M)"
using spec[OF gamma_a, of k] by simp
show "fst (ae_ss6_action (le_tm M) (?a k) (buf k) (dest k))
∈ gamma_block (Γ_tm M)"
proof (cases "?a k = LE_block (le_tm M)")
case True thus ?thesis using a_in buf_k by simp
next
case a_neq_le: False
show ?thesis
proof (cases "h = LE_block (le_tm M)")
case True thus ?thesis using a_neq_le a_in buf_k by simp
next
case h_neq_le: False
show ?thesis
proof (cases "dest k = AE_Left")
case True
thus ?thesis using a_neq_le h_neq_le r_in buf_k by simp
next
case False
thus ?thesis using a_neq_le h_neq_le l_in buf_k by simp
qed
qed
qed
qed
have gamma_a': "∀k. ?a' k ∈ gamma_block (Γ_tm M)"
proof (intro allI)
fix k
show "?a' k ∈ gamma_block (Γ_tm M)"
proof (cases "k < k_tm M")
case True thus ?thesis using spec[OF act_gamma, of k] by simp
next
case False
hence "?a' k = ?a k" using a_tail by simp
thus ?thesis using spec[OF gamma_a, of k] by simp
qed
qed
have act_le: "∀k<k_tm M. fst (ae_ss6_action (le_tm M) (?a k) (buf k) (dest k))
= LE_block (le_tm M)
⟶ ?a k = LE_block (le_tm M)"
using le_compat c'_eq unfolding ae_le_compat_ss6_def by simp
have le_no_write: "∀k. ?a' k = LE_block (le_tm M)
⟶ ?a k = LE_block (le_tm M)"
proof (intro allI impI)
fix k
assume a'_le: "?a' k = LE_block (le_tm M)"
show "?a k = LE_block (le_tm M)"
proof (cases "k < k_tm M")
case True
hence "fst (ae_ss6_action (le_tm M) (?a k) (buf k) (dest k))
= LE_block (le_tm M)"
using a'_le by simp
thus ?thesis using act_le[rule_format, OF True] by simp
next
case False
hence "?a k = ?a' k" using a_tail by simp
thus ?thesis using a'_le by simp
qed
qed
have src_valid: "ae_valid_stage (Γ_tm M) (le_tm M) (k_tm M)
(snd ((q, ofs, buf, dest, SS6)
:: 'q × ('a, 'c) ae_stage))"
using buf state_eq
unfolding ae_buffer_in_gamma_block_def ae_valid_stage_def by simp
have dst_valid: "ae_valid_stage (Γ_tm M) (le_tm M) (k_tm M)
(snd ((q, ofs, buf, dest, SS7)
:: 'q × ('a, 'c) ae_stage))"
by (rule ae_delta_ss6_ss7_dest_valid[OF rel_in src_valid])
have aed_in: "((q, ofs, buf, dest, SS6), ?a,
(q, ofs, buf, dest, SS7), ?a', ?d)
∈ alphabet_enlarge_delta M"
unfolding alphabet_enlarge_delta_def
using rel_in gamma_a gamma_a' le_no_write src_valid dst_valid by auto
let ?ts' = "λk. (ts k)(n k := ?a' k)"
let ?n' = "λk. go_dir (?d k) (n k)"
let ?c'' = "Config⇩M (q, ofs, buf, dest, SS7) ?ts' ?n'"
have step_sub_raw:
"(Config⇩M (q, ofs, buf, dest, SS6) ts n,
Config⇩M (q, ofs, buf, dest, SS7) ?ts' ?n')
∈ mttm_step (ae_delta_ss6_ss7 M)"
proof (rule mttm_step.intros)
show "((q, ofs, buf, dest, SS6), ?a,
(q, ofs, buf, dest, SS7), ?a', ?d)
∈ ae_delta_ss6_ss7 M" by (rule rel_in)
qed
have step_sub: "(c', ?c'') ∈ mttm_step (ae_delta_ss6_ss7 M)"
using step_sub_raw c'_eq by simp
have step_full_raw:
"(Config⇩M (q, ofs, buf, dest, SS6) ts n,
Config⇩M (q, ofs, buf, dest, SS7) ?ts' ?n')
∈ mttm_step (alphabet_enlarge_delta M)"
proof (rule mttm_step.intros)
show "((q, ofs, buf, dest, SS6), ?a,
(q, ofs, buf, dest, SS7), ?a', ?d)
∈ alphabet_enlarge_delta M" by (rule aed_in)
qed
have step_full: "(c', ?c'') ∈ mttm_step (alphabet_enlarge_delta M)"
using step_full_raw c'_eq by simp
show ?thesis using step_sub step_full by blast
qed
text ‹Step-existence at SS7: idempotent home re-write in
steady-state (returns ‹a›) or right write in LE-stage
(returns ‹r›); the LE-stage branch needs
‹ae_le_compat_ss7›. Steady-state is structurally safe
(‹a' = a›); the LE-stage branch fires only when ‹h = LE_block›
and ‹a ≠ LE_block›, returning ‹r›, where the chain proof
must show ‹r = LE_block› contradicts the position invariant.›
lemma ae_step_ss7_ss8_exists:
fixes M :: "('q, 'a) mttm"
and c' :: "('c :: enum ⇒ 'a,
'q × ('a, 'c) ae_stage) mt_config"
assumes inv: "ae_inv_ss7 M c'"
and gamma: "ae_tape_in_gamma_block M c'"
and buf: "ae_buffer_in_gamma_block M c'"
and le_compat: "ae_le_compat_ss7 M c'"
shows "∃c''. (c', c'') ∈ mttm_step (ae_delta_ss7_ss8 M)
∧ (c', c'') ∈ mttm_step (alphabet_enlarge_delta M)"
proof -
obtain q ofs buf dest where
state_eq: "mt_state c' = (q, ofs, buf, dest, SS7)"
and q_in: "q ∈ Q_tm M"
using inv unfolding ae_inv_ss7_def
by (cases "mt_state c'") auto
obtain ts n where c'_eq: "c' = Config⇩M (q, ofs, buf, dest, SS7) ts n"
using state_eq by (cases c') auto
let ?a = "λk. ts k (n k)"
let ?a' = "λk. if k < k_tm M
then fst (ae_ss7_action (le_tm M) (?a k) (buf k) (dest k))
else bl_block (bl_tm M)"
let ?d = "λk. if k < k_tm M
then snd (ae_ss7_action (le_tm M) (?a k) (buf k) (dest k))
else dir.N"
have a_tail: "∀j≥k_tm M. ?a j = bl_block (bl_tm M)"
using gamma c'_eq unfolding ae_tape_in_gamma_block_def by simp
have rel_in: "((q, ofs, buf, dest, SS7), ?a,
(q, ofs, buf, dest, SS8), ?a', ?d)
∈ ae_delta_ss7_ss8 M"
unfolding ae_delta_ss7_ss8_def using q_in a_tail by auto
have gamma_a: "∀k. ?a k ∈ gamma_block (Γ_tm M)"
using gamma c'_eq unfolding ae_tape_in_gamma_block_def by simp
have buf_gamma:
"∀k. fst (buf k) ∈ gamma_block (Γ_tm M)
∧ fst (snd (buf k)) ∈ gamma_block (Γ_tm M)
∧ snd (snd (buf k)) ∈ gamma_block (Γ_tm M)"
using buf state_eq unfolding ae_buffer_in_gamma_block_def by simp
have act_gamma: "∀k. fst (ae_ss7_action (le_tm M) (?a k) (buf k) (dest k))
∈ gamma_block (Γ_tm M)"
proof (intro allI)
fix k
obtain l h r where buf_k: "buf k = (l, h, r)"
by (cases "buf k") auto
have r_in: "r ∈ gamma_block (Γ_tm M)"
using spec[OF buf_gamma, of k] buf_k by simp
have a_in: "?a k ∈ gamma_block (Γ_tm M)"
using spec[OF gamma_a, of k] by simp
show "fst (ae_ss7_action (le_tm M) (?a k) (buf k) (dest k))
∈ gamma_block (Γ_tm M)"
proof (cases "?a k = LE_block (le_tm M)")
case True thus ?thesis using a_in buf_k by simp
next
case a_neq_le: False
show ?thesis
proof (cases "h = LE_block (le_tm M)")
case True thus ?thesis using a_neq_le r_in buf_k by simp
next
case h_neq_le: False
thus ?thesis using a_neq_le a_in buf_k by simp
qed
qed
qed
have gamma_a': "∀k. ?a' k ∈ gamma_block (Γ_tm M)"
proof (intro allI)
fix k
show "?a' k ∈ gamma_block (Γ_tm M)"
proof (cases "k < k_tm M")
case True thus ?thesis using spec[OF act_gamma, of k] by simp
next
case False
hence "?a' k = ?a k" using a_tail by simp
thus ?thesis using spec[OF gamma_a, of k] by simp
qed
qed
have act_le: "∀k<k_tm M. fst (ae_ss7_action (le_tm M) (?a k) (buf k) (dest k))
= LE_block (le_tm M)
⟶ ?a k = LE_block (le_tm M)"
using le_compat c'_eq unfolding ae_le_compat_ss7_def by simp
have le_no_write: "∀k. ?a' k = LE_block (le_tm M)
⟶ ?a k = LE_block (le_tm M)"
proof (intro allI impI)
fix k
assume a'_le: "?a' k = LE_block (le_tm M)"
show "?a k = LE_block (le_tm M)"
proof (cases "k < k_tm M")
case True
hence "fst (ae_ss7_action (le_tm M) (?a k) (buf k) (dest k))
= LE_block (le_tm M)"
using a'_le by simp
thus ?thesis using act_le[rule_format, OF True] by simp
next
case False
hence "?a k = ?a' k" using a_tail by simp
thus ?thesis using a'_le by simp
qed
qed
have src_valid: "ae_valid_stage (Γ_tm M) (le_tm M) (k_tm M)
(snd ((q, ofs, buf, dest, SS7)
:: 'q × ('a, 'c) ae_stage))"
using buf state_eq
unfolding ae_buffer_in_gamma_block_def ae_valid_stage_def by simp
have dst_valid: "ae_valid_stage (Γ_tm M) (le_tm M) (k_tm M)
(snd ((q, ofs, buf, dest, SS8)
:: 'q × ('a, 'c) ae_stage))"
by (rule ae_delta_ss7_ss8_dest_valid[OF rel_in src_valid])
have aed_in: "((q, ofs, buf, dest, SS7), ?a,
(q, ofs, buf, dest, SS8), ?a', ?d)
∈ alphabet_enlarge_delta M"
unfolding alphabet_enlarge_delta_def
using rel_in gamma_a gamma_a' le_no_write src_valid dst_valid by auto
let ?ts' = "λk. (ts k)(n k := ?a' k)"
let ?n' = "λk. go_dir (?d k) (n k)"
let ?c'' = "Config⇩M (q, ofs, buf, dest, SS8) ?ts' ?n'"
have step_sub_raw:
"(Config⇩M (q, ofs, buf, dest, SS7) ts n,
Config⇩M (q, ofs, buf, dest, SS8) ?ts' ?n')
∈ mttm_step (ae_delta_ss7_ss8 M)"
proof (rule mttm_step.intros)
show "((q, ofs, buf, dest, SS7), ?a,
(q, ofs, buf, dest, SS8), ?a', ?d)
∈ ae_delta_ss7_ss8 M" by (rule rel_in)
qed
have step_sub: "(c', ?c'') ∈ mttm_step (ae_delta_ss7_ss8 M)"
using step_sub_raw c'_eq by simp
have step_full_raw:
"(Config⇩M (q, ofs, buf, dest, SS7) ts n,
Config⇩M (q, ofs, buf, dest, SS8) ?ts' ?n')
∈ mttm_step (alphabet_enlarge_delta M)"
proof (rule mttm_step.intros)
show "((q, ofs, buf, dest, SS7), ?a,
(q, ofs, buf, dest, SS8), ?a', ?d)
∈ alphabet_enlarge_delta M" by (rule aed_in)
qed
have step_full: "(c', ?c'') ∈ mttm_step (alphabet_enlarge_delta M)"
using step_full_raw c'_eq by simp
show ?thesis using step_sub step_full by blast
qed
text ‹Step-existence at SS8: end of the write-back phase. The
action selects ‹l›, ‹r›, or ‹a› per stage-kind ‹×› dest;
the next stage is determined by halt routing — ‹q ∈ {t, r}›
routes to ‹init_stage le›, otherwise re-enters SS1 with
buffer + offset preserved and dest reset to ‹init_dest›.
Step-existence is uniform across the halt branch: both
branches are total in the action's input. The chain-level
forward-simulation argument splits halt-emission from cycle
continuation downstream, but step-existence itself does not
require a non-halting hypothesis.›
lemma ae_step_ss8_ss1_exists:
fixes M :: "('q, 'a) mttm"
and c' :: "('c :: enum ⇒ 'a,
'q × ('a, 'c) ae_stage) mt_config"
assumes vM: "valid_mttm M"
and inv: "ae_inv_ss8 M c'"
and gamma: "ae_tape_in_gamma_block M c'"
and buf: "ae_buffer_in_gamma_block M c'"
and le_compat: "ae_le_compat_ss8 M c'"
shows "∃c''. (c', c'') ∈ mttm_step (ae_delta_ss8_ss1 M)
∧ (c', c'') ∈ mttm_step (alphabet_enlarge_delta M)"
proof -
obtain q ofs buf dest where
state_eq: "mt_state c' = (q, ofs, buf, dest, SS8)"
and q_in: "q ∈ Q_tm M"
using inv unfolding ae_inv_ss8_def
by (cases "mt_state c'") auto
obtain ts n where c'_eq: "c' = Config⇩M (q, ofs, buf, dest, SS8) ts n"
using state_eq by (cases c') auto
let ?a = "λk. ts k (n k)"
let ?a' = "λk. if k < k_tm M
then fst (ae_ss8_action (le_tm M) (?a k) (buf k) (dest k))
else bl_block (bl_tm M)"
let ?d = "λk. if k < k_tm M
then snd (ae_ss8_action (le_tm M) (?a k) (buf k) (dest k))
else dir.N"
let ?stage' = "if q ∈ {t_tm M, r_tm M}
then init_stage (le_tm M)
else (ofs, buf, init_dest, SS1)"
have a_tail: "∀j≥k_tm M. ?a j = bl_block (bl_tm M)"
using gamma c'_eq unfolding ae_tape_in_gamma_block_def by simp
have rel_in: "((q, ofs, buf, dest, SS8), ?a,
(q, ?stage'), ?a', ?d)
∈ ae_delta_ss8_ss1 M"
unfolding ae_delta_ss8_ss1_def init_stage_def
using q_in a_tail by auto
have gamma_a: "∀k. ?a k ∈ gamma_block (Γ_tm M)"
using gamma c'_eq unfolding ae_tape_in_gamma_block_def by simp
have buf_gamma:
"∀k. fst (buf k) ∈ gamma_block (Γ_tm M)
∧ fst (snd (buf k)) ∈ gamma_block (Γ_tm M)
∧ snd (snd (buf k)) ∈ gamma_block (Γ_tm M)"
using buf state_eq unfolding ae_buffer_in_gamma_block_def by simp
have act_gamma: "∀k. fst (ae_ss8_action (le_tm M) (?a k) (buf k) (dest k))
∈ gamma_block (Γ_tm M)"
proof (intro allI)
fix k
obtain l h r where buf_k: "buf k = (l, h, r)"
by (cases "buf k") auto
have l_in: "l ∈ gamma_block (Γ_tm M)"
using spec[OF buf_gamma, of k] buf_k by simp
have r_in: "r ∈ gamma_block (Γ_tm M)"
using spec[OF buf_gamma, of k] buf_k by simp
have a_in: "?a k ∈ gamma_block (Γ_tm M)"
using spec[OF gamma_a, of k] by simp
show "fst (ae_ss8_action (le_tm M) (?a k) (buf k) (dest k))
∈ gamma_block (Γ_tm M)"
proof (cases "?a k = LE_block (le_tm M)")
case True thus ?thesis using a_in buf_k by simp
next
case a_neq_le: False
show ?thesis
proof (cases "h = LE_block (le_tm M)")
case True
show ?thesis
proof (cases "dest k = AE_Right")
case True thus ?thesis
using a_neq_le ‹h = LE_block (le_tm M)› r_in buf_k by simp
next
case False thus ?thesis
using a_neq_le ‹h = LE_block (le_tm M)› a_in buf_k by simp
qed
next
case h_neq_le: False
show ?thesis
proof (cases "dest k")
case AE_Left thus ?thesis
using a_neq_le h_neq_le l_in buf_k by simp
next
case AE_Home thus ?thesis
using a_neq_le h_neq_le r_in buf_k by simp
next
case AE_Right thus ?thesis
using a_neq_le h_neq_le r_in buf_k by simp
qed
qed
qed
qed
have gamma_a': "∀k. ?a' k ∈ gamma_block (Γ_tm M)"
proof (intro allI)
fix k
show "?a' k ∈ gamma_block (Γ_tm M)"
proof (cases "k < k_tm M")
case True thus ?thesis using spec[OF act_gamma, of k] by simp
next
case False
hence "?a' k = ?a k" using a_tail by simp
thus ?thesis using spec[OF gamma_a, of k] by simp
qed
qed
have act_le: "∀k<k_tm M. fst (ae_ss8_action (le_tm M) (?a k) (buf k) (dest k))
= LE_block (le_tm M)
⟶ ?a k = LE_block (le_tm M)"
using le_compat c'_eq unfolding ae_le_compat_ss8_def by simp
have le_no_write: "∀k. ?a' k = LE_block (le_tm M)
⟶ ?a k = LE_block (le_tm M)"
proof (intro allI impI)
fix k
assume a'_le: "?a' k = LE_block (le_tm M)"
show "?a k = LE_block (le_tm M)"
proof (cases "k < k_tm M")
case True
hence "fst (ae_ss8_action (le_tm M) (?a k) (buf k) (dest k))
= LE_block (le_tm M)"
using a'_le by simp
thus ?thesis using act_le[rule_format, OF True] by simp
next
case False
hence "?a k = ?a' k" using a_tail by simp
thus ?thesis using a'_le by simp
qed
qed
have src_valid: "ae_valid_stage (Γ_tm M) (le_tm M) (k_tm M)
(snd ((q, ofs, buf, dest, SS8)
:: 'q × ('a, 'c) ae_stage))"
using buf state_eq
unfolding ae_buffer_in_gamma_block_def ae_valid_stage_def by simp
have dst_valid: "ae_valid_stage (Γ_tm M) (le_tm M) (k_tm M)
(snd ((q, ?stage')
:: 'q × ('a, 'c) ae_stage))"
by (rule ae_delta_ss8_ss1_dest_valid[OF vM rel_in src_valid])
have aed_in: "((q, ofs, buf, dest, SS8), ?a,
(q, ?stage'), ?a', ?d)
∈ alphabet_enlarge_delta M"
unfolding alphabet_enlarge_delta_def
using rel_in gamma_a gamma_a' le_no_write src_valid dst_valid by auto
let ?ts' = "λk. (ts k)(n k := ?a' k)"
let ?n' = "λk. go_dir (?d k) (n k)"
let ?c'' = "Config⇩M (q, ?stage') ?ts' ?n'"
have step_sub_raw:
"(Config⇩M (q, ofs, buf, dest, SS8) ts n,
Config⇩M (q, ?stage') ?ts' ?n')
∈ mttm_step (ae_delta_ss8_ss1 M)"
proof (rule mttm_step.intros)
show "((q, ofs, buf, dest, SS8), ?a,
(q, ?stage'), ?a', ?d)
∈ ae_delta_ss8_ss1 M" by (rule rel_in)
qed
have step_sub: "(c', ?c'') ∈ mttm_step (ae_delta_ss8_ss1 M)"
using step_sub_raw c'_eq by simp
have step_full_raw:
"(Config⇩M (q, ofs, buf, dest, SS8) ts n,
Config⇩M (q, ?stage') ?ts' ?n')
∈ mttm_step (alphabet_enlarge_delta M)"
proof (rule mttm_step.intros)
show "((q, ofs, buf, dest, SS8), ?a,
(q, ?stage'), ?a', ?d)
∈ alphabet_enlarge_delta M" by (rule aed_in)
qed
have step_full: "(c', ?c'') ∈ mttm_step (alphabet_enlarge_delta M)"
using step_full_raw c'_eq by simp
show ?thesis using step_sub step_full by blast
qed
subsubsection ‹Substrate and encoder helpers›
text ‹Substrate-derived helpers used by the validation lemmas.›
lemma bl_tm_notin_Sigma_tm:
assumes "valid_mttm M"
shows "bl_tm M ∉ Sigma_tm M"
by (rule valid_mttm_blank_not_Sigma[OF assms])
lemma s_tm_in_Q_tm:
assumes "valid_mttm M"
shows "s_tm M ∈ Q_tm M"
by (rule valid_mttm_s_in_Q[OF assms])
text ‹Encoder structural helpers. ‹length_encode_input› and
‹encode_input_nth› unfold the encoder's definition into the
shape that downstream proofs about block content cite.›
lemma length_encode_input:
"length (encode_input bl u :: ('c :: enum ⇒ 'a) list)
= (length u + card (UNIV :: 'c set) - 1) div card (UNIV :: 'c set)"
by (simp add: encode_input_def Let_def)
lemma encode_input_nth:
fixes u :: "'a list"
and x :: "'c :: enum"
assumes "i < length (encode_input bl u :: ('c ⇒ 'a) list)"
shows "((encode_input bl u :: ('c ⇒ 'a) list) ! i) x
= (let j = i * card (UNIV :: 'c set) + c_idx x
in if j < length u then u ! j else bl)"
proof -
let ?c = "card (UNIV :: 'c set)"
have len_eq: "length (encode_input bl u :: ('c ⇒ 'a) list)
= (length u + ?c - 1) div ?c"
by (simp add: encode_input_def Let_def)
hence i_lt: "i < (length u + ?c - 1) div ?c" using assms by simp
show ?thesis
unfolding encode_input_def Let_def
using i_lt by simp
qed
text ‹Index range for ‹c_idx›: every element of ‹'c :: enum›
has an index strictly less than the length of the canonical
enumeration, and the enumeration retrieves that element back.›
lemma c_idx_in_range:
fixes x :: "'c :: enum"
shows "c_idx x < length (enum_class.enum :: 'c list)"
and "(enum_class.enum :: 'c list) ! c_idx x = x"
proof -
have ex_unique: "∃!i. i < length (enum_class.enum :: 'c list)
∧ (enum_class.enum :: 'c list) ! i = x"
proof -
have x_in: "x ∈ set (enum_class.enum :: 'c list)"
using enum_class.UNIV_enum by blast
then obtain i where
i_lt: "i < length (enum_class.enum :: 'c list)" and
i_eq: "(enum_class.enum :: 'c list) ! i = x"
by (auto simp: in_set_conv_nth)
moreover have "⋀j. j < length (enum_class.enum :: 'c list)
⟹ (enum_class.enum :: 'c list) ! j = x
⟹ j = i"
using i_lt i_eq enum_class.enum_distinct
by (metis nth_eq_iff_index_eq)
ultimately show ?thesis by blast
qed
have idx_eq: "c_idx x < length (enum_class.enum :: 'c list)
∧ (enum_class.enum :: 'c list) ! c_idx x = x"
unfolding c_idx_def using theI'[OF ex_unique] .
show "c_idx x < length (enum_class.enum :: 'c list)" using idx_eq ..
show "(enum_class.enum :: 'c list) ! c_idx x = x" using idx_eq ..
qed
lemma c_idx_lt_card: "c_idx (x :: 'c :: enum) < card (UNIV :: 'c set)"
proof -
have "card (UNIV :: 'c set) = length (enum_class.enum :: 'c list)"
using enum_class.UNIV_enum enum_class.enum_distinct
by (metis distinct_card length_remdups_card_conv set_remdups)
thus ?thesis using c_idx_in_range(1) by simp
qed
lemma card_eq_length_enum:
"card (UNIV :: 'c :: enum set) = length (enum_class.enum :: 'c list)"
using enum_class.UNIV_enum enum_class.enum_distinct
by (metis distinct_card length_remdups_card_conv set_remdups)
lemma c_idx_enum_nth:
fixes i :: nat
assumes "i < length (enum_class.enum :: 'c :: enum list)"
shows "c_idx ((enum_class.enum :: 'c list) ! i) = i"
proof -
let ?xs = "enum_class.enum :: 'c list"
have nth_eq: "?xs ! c_idx (?xs ! i) = ?xs ! i"
using c_idx_in_range(2) .
have lt: "c_idx (?xs ! i) < length ?xs"
by (rule c_idx_in_range(1))
show ?thesis
using nth_eq lt assms enum_class.enum_distinct
by (metis nth_eq_iff_index_eq)
qed
end