Theory Multitape_Alphabet_Enlargement.AlphabetEnlargement_Delta
theory AlphabetEnlargement_Delta
imports AlphabetEnlargement_Substeps
begin
subsection ‹Transition relation (union of per-substep parts)›
text ‹The output machine's tape alphabet ‹Γ'›: the set of
‹'c›-blocks whose every cell is in ‹M›'s
tape alphabet ‹Γ›.›
definition gamma_block ::
"'a set ⇒ (('c :: enum) ⇒ 'a) set" where
"gamma_block Γ = {f. range f ⊆ Γ}"
lemma gamma_block_mono: "A ⊆ B ⟹ gamma_block A ⊆ gamma_block B"
unfolding gamma_block_def by auto
lemma finite_gamma_block:
fixes A :: "'a set"
assumes finA: "finite A"
shows "finite (gamma_block A :: ('c :: enum ⇒ 'a) set)"
proof -
have eq: "gamma_block A = Pi⇩E (UNIV :: 'c set) (λ_. A)"
by (auto simp: gamma_block_def PiE_def Pi_def extensional_def)
show ?thesis
unfolding eq by (intro finite_PiE) (auto simp: finA)
qed
lemma LE_block_in_gamma_block:
"le ∈ Γ ⟹ LE_block le ∈ gamma_block Γ"
unfolding gamma_block_def LE_block_def by auto
lemma bl_block_in_gamma_block:
"bl ∈ Γ ⟹ bl_block bl ∈ gamma_block Γ"
unfolding gamma_block_def bl_block_def by auto
text ‹State-level buffer validity: every per-tape block triple
stored in the stage's buffer component has all three blocks in
‹gamma_block Γ›. Spec-side counterpart to the config-level
invariant ‹ae_buffer_in_gamma_block›; used as the
buffer-component restriction in ‹alphabet_enlarge›'s output
state set ‹Q'›. This makes ‹Q'› finite from the
set-level premise ‹finite Γ› alone — without requiring
‹UNIV('c ⇒ 'a)› to be a finite type, which would not be
derivable from ‹finite Γ› generically.›
definition ae_valid_stage ::
"'a set ⇒ 'a ⇒ nat ⇒ ('a, 'c :: enum) ae_stage ⇒ bool" where
"ae_valid_stage Γ le K stg ⟷
(case stg of (off, buf, dst, _) ⇒
(∀k. fst (buf k) ∈ gamma_block Γ
∧ fst (snd (buf k)) ∈ gamma_block Γ
∧ snd (snd (buf k)) ∈ gamma_block Γ)
∧ (∀j≥K. off j = init_offset j)
∧ (∀j≥K. buf j = init_buffer le j)
∧ (∀j≥K. dst j = init_dest j))"
lemma ae_valid_stage_init:
assumes "le ∈ Γ"
shows "ae_valid_stage Γ le K (init_stage le)"
unfolding ae_valid_stage_def init_stage_def init_buffer_def
using LE_block_in_gamma_block[OF assms] by simp
lemma init_buffer_in_gamma_block:
fixes le :: 'a and Γ :: "'a set"
and ib :: "nat ⇒ ('c :: enum ⇒ 'a)
× ('c ⇒ 'a) × ('c ⇒ 'a)"
assumes le_in: "le ∈ Γ"
and ib_def: "ib = init_buffer le"
shows "∀k. fst (ib k) ∈ gamma_block Γ
∧ fst (snd (ib k)) ∈ gamma_block Γ
∧ snd (snd (ib k)) ∈ gamma_block Γ"
using LE_block_in_gamma_block[OF le_in]
by (auto simp: ib_def init_buffer_def)
text ‹Specialized variant for direct invocation at validation-phase
call sites where the buffer is ‹init_buffer (le_tm M)›. The
buf-gamma claim is in the explicit shape that
‹ae_step_val_*›'s new ‹buf_gamma› hypothesis expects.
Anchors the polymorphic ‹'c› via type annotations on every
occurrence (cf. discussion in commit a812ed0).›
lemma init_buffer_in_gamma_block_at_M:
fixes M :: "('q, 'a) mttm"
assumes vM: "valid_mttm M"
shows "∀kk :: nat.
fst (init_buffer (le_tm M) kk
:: ('c :: enum ⇒ 'a) × ('c ⇒ 'a) × ('c ⇒ 'a))
∈ gamma_block (Γ_tm M)
∧ fst (snd (init_buffer (le_tm M) kk
:: ('c ⇒ 'a) × ('c ⇒ 'a) × ('c ⇒ 'a)))
∈ gamma_block (Γ_tm M)
∧ snd (snd (init_buffer (le_tm M) kk
:: ('c ⇒ 'a) × ('c ⇒ 'a) × ('c ⇒ 'a)))
∈ gamma_block (Γ_tm M)"
proof (intro allI)
fix kk :: nat
have lg: "(LE_block (le_tm M) :: 'c ⇒ 'a) ∈ gamma_block (Γ_tm M)"
by (rule LE_block_in_gamma_block[OF valid_mttm_LE_in_Gamma[OF vM]])
show "fst (init_buffer (le_tm M) kk
:: ('c ⇒ 'a) × ('c ⇒ 'a) × ('c ⇒ 'a))
∈ gamma_block (Γ_tm M)
∧ fst (snd (init_buffer (le_tm M) kk
:: ('c ⇒ 'a) × ('c ⇒ 'a) × ('c ⇒ 'a)))
∈ gamma_block (Γ_tm M)
∧ snd (snd (init_buffer (le_tm M) kk
:: ('c ⇒ 'a) × ('c ⇒ 'a) × ('c ⇒ 'a)))
∈ gamma_block (Γ_tm M)"
using lg by (simp add: init_buffer_def)
qed
lemma finite_ae_valid_stages:
fixes Γ :: "'a set" and le :: 'a and K :: nat
assumes finG: "finite Γ"
shows "finite {stg :: ('a, 'c :: enum) ae_stage.
ae_valid_stage Γ le K stg}"
proof -
let ?G = "gamma_block Γ :: ('c ⇒ 'a) set"
let ?GGG = "?G × ?G × ?G"
have fG: "finite ?G" by (rule finite_gamma_block[OF finG])
have fGGG: "finite ?GGG"
using fG by (intro finite_cartesian_product)
let ?offs = "{off :: nat ⇒ 'c.
(∀j. off j ∈ (UNIV :: 'c set))
∧ (∀j≥K. off j = init_offset j)}"
let ?bufs = "{buf :: nat ⇒ ('c ⇒ 'a) × ('c ⇒ 'a) × ('c ⇒ 'a).
(∀j. buf j ∈ ?GGG)
∧ (∀j≥K. buf j = init_buffer le j)}"
let ?dsts = "{dst :: nat ⇒ ae_dest.
(∀j. dst j ∈ (UNIV :: ae_dest set))
∧ (∀j≥K. dst j = init_dest j)}"
have foffs: "finite ?offs"
using finite_tail_const_funcs[OF finite_UNIV, of K "SOME x :: 'c. True"]
by (simp add: init_offset_def)
have fbufs: "finite ?bufs"
using finite_tail_const_funcs[OF fGGG, of K "init_buffer le 0"]
by (simp add: init_buffer_def)
have fdsts: "finite ?dsts"
using finite_tail_const_funcs[OF finite_UNIV, of K AE_Home]
by (simp add: init_dest_def)
let ?ENV = "?offs × ?bufs × ?dsts × (UNIV :: substep_idx set)"
have "{stg :: ('a, 'c) ae_stage. ae_valid_stage Γ le K stg} ⊆ ?ENV"
unfolding ae_valid_stage_def
by (auto simp: mem_Times_iff split: prod.splits)
moreover have "finite ?ENV"
using foffs fbufs fdsts by (intro finite_cartesian_product) simp_all
ultimately show ?thesis by (rule finite_subset)
qed
text ‹LE-input simp rules for the per-tape action helpers. When
the read block on tape ‹k› is the all-LE block, each
helper's LE-guard prefix returns ‹(LE_block le, N)› (or
‹(LE_block le, R)› for SS6) regardless of the buffer triple's
components. These rules unblock the ‹δLE›-preservation case
analysis: ‹fun›-generated simp rules match only literal
triples ‹(l, h, r)›; named LE-input lemmas simplify the
general application form via tuple destructuring.›
lemma ae_ss5_action_LE [simp]:
"ae_ss5_action le (LE_block le) buf ds = (LE_block le, dir.N)"
proof -
obtain l h r where "buf = (l, h, r)" using prod.exhaust by metis
thus ?thesis by simp
qed
lemma ae_ss6_action_LE [simp]:
"ae_ss6_action le (LE_block le) buf ds = (LE_block le, dir.R)"
proof -
obtain l h r where "buf = (l, h, r)" using prod.exhaust by metis
thus ?thesis by simp
qed
lemma ae_ss7_action_LE [simp]:
"ae_ss7_action le (LE_block le) buf ds = (LE_block le, dir.N)"
proof -
obtain l h r where "buf = (l, h, r)" using prod.exhaust by metis
thus ?thesis by simp
qed
lemma ae_ss8_action_LE [simp]:
"ae_ss8_action le (LE_block le) buf ds = (LE_block le, dir.N)"
proof -
obtain l h r where "buf = (l, h, r)" using prod.exhaust by metis
thus ?thesis by simp
qed
text ‹State preservation for a single buffered ‹M›-step: if the
source state is in ‹Q›, so is the destination. Direct
consequence of the substrate's ‹δ_set› range obligation.›
lemma m_step_buffered_state_preservation:
fixes M :: "('q, 'a) mttm"
assumes valM: "valid_mttm M"
and step: "((q, blocks, pos), (q', blocks', pos')) ∈ m_step_buffered M"
and qQ: "q ∈ Q_tm M"
shows "q' ∈ Q_tm M"
proof -
from step obtain a a' d where
"(q, a, q', a', d) ∈ delta_tm M"
unfolding m_step_buffered_def by blast
thus "q' ∈ Q_tm M"
using valid_mttm_delta_set[OF valM] by auto
qed
text ‹State preservation for the up-to-‹c›-step composition: if the
source state is in ‹Q›, so is the destination. Induction on
the relation power.›
lemma m_steps_buffered_state_preservation:
fixes M :: "('q, 'a) mttm"
assumes valM: "valid_mttm M"
and steps: "((q, blocks, pos), (q', blocks', pos')) ∈ m_steps_buffered M"
and qQ: "q ∈ Q_tm M"
shows "q' ∈ Q_tm M"
proof -
from steps obtain n where
n_step: "((q, blocks, pos), (q', blocks', pos')) ∈ (m_step_buffered M) ^^ n"
unfolding m_steps_buffered_def by blast
from n_step qQ show ?thesis
proof (induction n arbitrary: q' blocks' pos')
case 0
then show ?case by auto
next
case (Suc n)
from Suc.prems(1) obtain q'' blocks'' pos'' where
step_n: "((q, blocks, pos), (q'', blocks'', pos''))
∈ (m_step_buffered M) ^^ n"
and step_one: "((q'', blocks'', pos''), (q', blocks', pos'))
∈ m_step_buffered M"
by (auto elim: relpow_Suc_E)
from Suc.IH[OF step_n Suc.prems(2)] have qQ'': "q'' ∈ Q_tm M" .
from m_step_buffered_state_preservation[OF valM step_one qQ''] show ?case .
qed
qed
text ‹Buffer-gamma preservation under a single ‹m_step_buffered›:
if every slot of every tape's buffer is in ‹gamma_block (Γ_tm M)›
pre-step, the post-step buffer's slots are too. The substantive
fact: ‹m_step_buffered›'s write updates exactly one cell of one
slot per tape, the written value lies in ‹Γ_tm M› (by
‹valid_mttm_delta›), and ‹gamma_block› is closed under such
point-updates.›
lemma m_step_buffered_gamma_preserve:
fixes M :: "('q, 'a) mttm"
assumes vM: "valid_mttm M"
and step: "((q, blocks, pos), (q', blocks', pos')) ∈ m_step_buffered M"
and pre: "∀k. fst (blocks k) ∈ gamma_block (Γ_tm M)
∧ fst (snd (blocks k)) ∈ gamma_block (Γ_tm M)
∧ snd (snd (blocks k)) ∈ gamma_block (Γ_tm M)"
shows "∀k. fst (blocks' k) ∈ gamma_block (Γ_tm M)
∧ fst (snd (blocks' k)) ∈ gamma_block (Γ_tm M)
∧ snd (snd (blocks' k)) ∈ gamma_block (Γ_tm M)"
proof -
from step obtain a a' d where
tr: "(q, a, q', a', d) ∈ delta_tm M"
and bk_update: "∀k. blocks' k = write_bp (blocks k) (pos k) (a' k)"
unfolding m_step_buffered_def by auto
show ?thesis
proof (intro allI)
fix k
obtain l h r where bk_eq: "blocks k = (l, h, r)"
by (cases "blocks k") auto
obtain b off where pk_eq: "pos k = (b, off)"
by (cases "pos k") auto
from pre[rule_format, of k] bk_eq have
l_in: "l ∈ gamma_block (Γ_tm M)" and
h_in: "h ∈ gamma_block (Γ_tm M)" and
r_in: "r ∈ gamma_block (Γ_tm M)"
by auto
from valid_mttm_delta(4)[OF vM tr, of k] have a'_in: "a' k ∈ Γ_tm M" .
have l_upd: "l(off := a' k) ∈ gamma_block (Γ_tm M)"
using l_in a'_in unfolding gamma_block_def by auto
have h_upd: "h(off := a' k) ∈ gamma_block (Γ_tm M)"
using h_in a'_in unfolding gamma_block_def by auto
have r_upd: "r(off := a' k) ∈ gamma_block (Γ_tm M)"
using r_in a'_in unfolding gamma_block_def by auto
have bk'_eq: "blocks' k = write_bp (l, h, r) (b, off) (a' k)"
using bk_update[rule_format, of k] bk_eq pk_eq by simp
show "fst (blocks' k) ∈ gamma_block (Γ_tm M)
∧ fst (snd (blocks' k)) ∈ gamma_block (Γ_tm M)
∧ snd (snd (blocks' k)) ∈ gamma_block (Γ_tm M)"
using bk'_eq l_in h_in r_in l_upd h_upd r_upd
by (cases b) (auto simp: write_bp_def)
qed
qed
text ‹Buffer-gamma preservation under ‹m_steps_buffered› (the
iterated up-to-c-step relation). Induction on the relation
power; the step case applies ‹m_step_buffered_gamma_preserve›.›
lemma m_steps_buffered_gamma_preserve:
fixes M :: "('q, 'a) mttm"
assumes vM: "valid_mttm M"
and steps: "((q, blocks, pos), (q', blocks', pos')) ∈ m_steps_buffered M"
and pre: "∀k. fst (blocks k) ∈ gamma_block (Γ_tm M)
∧ fst (snd (blocks k)) ∈ gamma_block (Γ_tm M)
∧ snd (snd (blocks k)) ∈ gamma_block (Γ_tm M)"
shows "∀k. fst (blocks' k) ∈ gamma_block (Γ_tm M)
∧ fst (snd (blocks' k)) ∈ gamma_block (Γ_tm M)
∧ snd (snd (blocks' k)) ∈ gamma_block (Γ_tm M)"
proof -
from steps obtain n where
n_step: "((q, blocks, pos), (q', blocks', pos'))
∈ (m_step_buffered M) ^^ n"
unfolding m_steps_buffered_def by blast
from n_step pre show ?thesis
proof (induction n arbitrary: q' blocks' pos')
case 0
then show ?case by auto
next
case (Suc n)
from Suc.prems(1) obtain q'' blocks'' pos'' where
step_n: "((q, blocks, pos), (q'', blocks'', pos''))
∈ (m_step_buffered M) ^^ n"
and step_one: "((q'', blocks'', pos''), (q', blocks', pos'))
∈ m_step_buffered M"
by (auto elim: relpow_Suc_E)
from Suc.IH[OF step_n Suc.prems(2)] have IH:
"∀k. fst (blocks'' k) ∈ gamma_block (Γ_tm M)
∧ fst (snd (blocks'' k)) ∈ gamma_block (Γ_tm M)
∧ snd (snd (blocks'' k)) ∈ gamma_block (Γ_tm M)" .
from m_step_buffered_gamma_preserve[OF vM step_one IH] show ?case .
qed
qed
text ‹Per-substep destination-stage-validity helpers. Given that a
tuple is in a particular substep delta, source-stage validity, and
any auxiliary gamma-block facts (‹a›'s gamma, ‹bl_M›/‹le_M›
in ‹Γ_M› as needed for SS2‹→›SS3 and SS8‹→›SS1
halt branch, ‹m_steps_buffered_gamma_preserve› for SS4‹→›SS5),
the destination stage is valid. Companion to
‹ae_step_alphabet_enlarge_buffer_gamma_preserve› at the
tuple level instead of the configuration level. These are used by
the ‹_exists› construction lemmas to discharge the
‹Q'›-filter conjunct that ‹alphabet_enlarge_delta›
carries to enforce ‹Q' = Q × {stg. ae_valid_stage Γ_M stg}›
finiteness on a set-finite-‹Γ› premise (instead of
type-class-finite-‹'a›).›
lemma ae_delta_ss1_ss2_dest_valid:
assumes rel: "(s, a, s', a', d) ∈ ae_delta_ss1_ss2 M"
and a_gamma: "∀k. a k ∈ gamma_block (Γ_tm M)"
and src_valid: "ae_valid_stage (Γ_tm M) (le_tm M) (k_tm M) (snd s)"
shows "ae_valid_stage (Γ_tm M) (le_tm M) (k_tm M) (snd s')"
proof -
from rel obtain q ofs buf dest buf' where
s_eq: "s = (q, ofs, buf, dest, SS1)"
and s'_eq: "s' = (q, ofs, buf', dest, SS2)"
and buf'_def: "buf' = (λk. if k < k_tm M
then (fst (buf k), a k, snd (snd (buf k)))
else init_buffer (le_tm M) k)"
unfolding ae_delta_ss1_ss2_def by auto
from src_valid s_eq have
src_g: "∀k. fst (buf k) ∈ gamma_block (Γ_tm M)
∧ fst (snd (buf k)) ∈ gamma_block (Γ_tm M)
∧ snd (snd (buf k)) ∈ gamma_block (Γ_tm M)"
and src_off: "∀j≥k_tm M. ofs j = init_offset j"
and src_buf: "∀j≥k_tm M. buf j = init_buffer (le_tm M) j"
and src_dst: "∀j≥k_tm M. dest j = init_dest j"
by (simp_all add: ae_valid_stage_def)
have buf'_g: "∀k. fst (buf' k) ∈ gamma_block (Γ_tm M)
∧ fst (snd (buf' k)) ∈ gamma_block (Γ_tm M)
∧ snd (snd (buf' k)) ∈ gamma_block (Γ_tm M)"
proof (intro allI)
fix k
show "fst (buf' k) ∈ gamma_block (Γ_tm M)
∧ fst (snd (buf' k)) ∈ gamma_block (Γ_tm M)
∧ snd (snd (buf' k)) ∈ gamma_block (Γ_tm M)"
proof (cases "k < k_tm M")
case True
thus ?thesis using buf'_def src_g a_gamma by simp
next
case False
hence le_k: "k_tm M ≤ k" by simp
have "buf' k = init_buffer (le_tm M) k" using buf'_def False by simp
moreover have "buf k = init_buffer (le_tm M) k"
using src_buf[rule_format, OF le_k] .
ultimately have "buf' k = buf k" by simp
thus ?thesis using src_g by simp
qed
qed
have buf'_tail: "∀j≥k_tm M. buf' j = init_buffer (le_tm M) j"
using buf'_def by simp
show ?thesis
unfolding s'_eq ae_valid_stage_def
using buf'_g src_off src_dst buf'_tail by simp
qed
lemma ae_delta_ss2_ss3_dest_valid:
assumes vM: "valid_mttm M"
and rel: "(s, a, s', a', d) ∈ ae_delta_ss2_ss3 M"
and a_gamma: "∀k. a k ∈ gamma_block (Γ_tm M)"
and src_valid: "ae_valid_stage (Γ_tm M) (le_tm M) (k_tm M) (snd s)"
shows "ae_valid_stage (Γ_tm M) (le_tm M) (k_tm M) (snd s')"
proof -
from rel obtain q ofs buf dest buf' where
s_eq: "s = (q, ofs, buf, dest, SS2)"
and s'_eq: "s' = (q, ofs, buf', dest, SS3)"
and buf'_def: "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)"
unfolding ae_delta_ss2_ss3_def by auto
from src_valid s_eq have
src: "∀k. fst (buf k) ∈ gamma_block (Γ_tm M)
∧ fst (snd (buf k)) ∈ gamma_block (Γ_tm M)
∧ snd (snd (buf k)) ∈ gamma_block (Γ_tm M)"
and src_off: "∀j≥k_tm M. ofs j = init_offset j"
and src_buf: "∀j≥k_tm M. buf j = init_buffer (le_tm M) j"
and src_dst: "∀j≥k_tm M. dest j = init_dest j"
by (simp_all add: ae_valid_stage_def)
have bl_gam: "bl_block (bl_tm M) ∈ gamma_block (Γ_tm M)"
using bl_block_in_gamma_block[OF valid_mttm_blank_in_Gamma[OF vM]] .
have per_k: "∀k. fst (buf' k) ∈ gamma_block (Γ_tm M)
∧ fst (snd (buf' k)) ∈ gamma_block (Γ_tm M)
∧ snd (snd (buf' k)) ∈ gamma_block (Γ_tm M)"
proof
fix k
show "fst (buf' k) ∈ gamma_block (Γ_tm M)
∧ fst (snd (buf' k)) ∈ gamma_block (Γ_tm M)
∧ snd (snd (buf' k)) ∈ gamma_block (Γ_tm M)"
proof (cases "k < k_tm M")
case True
obtain l h r where buf_eq: "buf k = (l, h, r)" using prod.exhaust by metis
have lhr: "l ∈ gamma_block (Γ_tm M)
∧ h ∈ gamma_block (Γ_tm M)
∧ r ∈ gamma_block (Γ_tm M)"
using src buf_eq by (metis fst_conv snd_conv)
have buf'_k: "buf' k = (if h = LE_block (le_tm M)
then bl_block (bl_tm M)
else a k, h, r)"
using buf'_def buf_eq True by simp
show ?thesis using lhr a_gamma bl_gam buf'_k by auto
next
case False
hence le_k: "k_tm M ≤ k" by simp
have "buf' k = init_buffer (le_tm M) k" using buf'_def False by simp
moreover have "buf k = init_buffer (le_tm M) k"
using src_buf[rule_format, OF le_k] .
ultimately have "buf' k = buf k" by simp
thus ?thesis using src by simp
qed
qed
have buf'_tail: "∀j≥k_tm M. buf' j = init_buffer (le_tm M) j"
using buf'_def by simp
show ?thesis
unfolding s'_eq ae_valid_stage_def
using per_k src_off src_dst buf'_tail by simp
qed
lemma ae_delta_ss3_ss4_dest_valid:
assumes rel: "(s, a, s', a', d) ∈ ae_delta_ss3_ss4 M"
and src_valid: "ae_valid_stage (Γ_tm M) (le_tm M) (k_tm M) (snd s)"
shows "ae_valid_stage (Γ_tm M) (le_tm M) (k_tm M) (snd s')"
proof -
from rel obtain q ofs buf dest where
s_eq: "s = (q, ofs, buf, dest, SS3)"
and s'_eq: "s' = (q, ofs, buf, dest, SS4)"
unfolding ae_delta_ss3_ss4_def by auto
show ?thesis
using src_valid unfolding s_eq s'_eq ae_valid_stage_def by simp
qed
lemma ae_delta_ss4_ss5_dest_valid:
assumes vM: "valid_mttm M"
and rel: "(s, a, s', a', d) ∈ ae_delta_ss4_ss5 M"
and a_gamma: "∀k. a k ∈ gamma_block (Γ_tm M)"
and src_valid: "ae_valid_stage (Γ_tm M) (le_tm M) (k_tm M) (snd s)"
shows "ae_valid_stage (Γ_tm M) (le_tm M) (k_tm M) (snd s')"
proof -
from rel obtain q ofs buf dest_old q' ofs' buf' dest' buf_full end_pos bufC where
s_eq: "s = (q, ofs, buf, dest_old, SS4)"
and s'_eq: "s' = (q', ofs', buf', dest', SS5)"
and buf_full_def: "buf_full = (λk. (fst (buf k),
if k < k_tm M then fst (snd (buf k)) else a k,
a k))"
and mst: "((q, buf_full, λk. (AE_Home, ofs k)),
(q', bufC, end_pos)) ∈ m_steps_buffered M"
and ofs'_def: "ofs' = (λk. if k < k_tm M then snd (end_pos k) else init_offset k)"
and buf'_def: "buf' = (λk. if k < k_tm M then bufC k else init_buffer (le_tm M) k)"
and dest'_def: "dest' = (λk. if k < k_tm M then fst (end_pos k) else init_dest k)"
unfolding ae_delta_ss4_ss5_def by auto
from src_valid s_eq have
src: "∀k. fst (buf k) ∈ gamma_block (Γ_tm M)
∧ fst (snd (buf k)) ∈ gamma_block (Γ_tm M)
∧ snd (snd (buf k)) ∈ gamma_block (Γ_tm M)"
and src_buf: "∀j≥k_tm M. buf j = init_buffer (le_tm M) j"
by (simp_all add: ae_valid_stage_def)
have full: "∀k. fst (buf_full k) ∈ gamma_block (Γ_tm M)
∧ fst (snd (buf_full k)) ∈ gamma_block (Γ_tm M)
∧ snd (snd (buf_full k)) ∈ gamma_block (Γ_tm M)"
unfolding buf_full_def using src a_gamma by (auto split: if_splits)
have bufC_gam: "∀k. fst (bufC k) ∈ gamma_block (Γ_tm M)
∧ fst (snd (bufC k)) ∈ gamma_block (Γ_tm M)
∧ snd (snd (bufC k)) ∈ gamma_block (Γ_tm M)"
by (rule m_steps_buffered_gamma_preserve[OF vM mst full])
have buf'_gam: "∀k. fst (buf' k) ∈ gamma_block (Γ_tm M)
∧ fst (snd (buf' k)) ∈ gamma_block (Γ_tm M)
∧ snd (snd (buf' k)) ∈ gamma_block (Γ_tm M)"
proof (intro allI)
fix k
show "fst (buf' k) ∈ gamma_block (Γ_tm M)
∧ fst (snd (buf' k)) ∈ gamma_block (Γ_tm M)
∧ snd (snd (buf' k)) ∈ gamma_block (Γ_tm M)"
proof (cases "k < k_tm M")
case True
thus ?thesis using bufC_gam by (simp add: buf'_def)
next
case False
hence le_k: "k_tm M ≤ k" by simp
have "buf' k = init_buffer (le_tm M) k" by (simp add: buf'_def False)
also have "… = buf k" using src_buf[rule_format, OF le_k] by simp
finally have "buf' k = buf k" .
thus ?thesis using src by simp
qed
qed
have ofs'_tail: "∀j≥k_tm M. ofs' j = init_offset j" by (simp add: ofs'_def)
have buf'_tail: "∀j≥k_tm M. buf' j = init_buffer (le_tm M) j" by (simp add: buf'_def)
have dest'_tail: "∀j≥k_tm M. dest' j = init_dest j" by (simp add: dest'_def)
show ?thesis unfolding s'_eq ae_valid_stage_def
using buf'_gam ofs'_tail buf'_tail dest'_tail by simp
qed
lemma ae_delta_ss5_ss6_dest_valid:
assumes rel: "(s, a, s', a', d) ∈ ae_delta_ss5_ss6 M"
and src_valid: "ae_valid_stage (Γ_tm M) (le_tm M) (k_tm M) (snd s)"
shows "ae_valid_stage (Γ_tm M) (le_tm M) (k_tm M) (snd s')"
proof -
from rel obtain q ofs buf dest where
s_eq: "s = (q, ofs, buf, dest, SS5)"
and s'_eq: "s' = (q, ofs, buf, dest, SS6)"
unfolding ae_delta_ss5_ss6_def by auto
show ?thesis
using src_valid unfolding s_eq s'_eq ae_valid_stage_def by simp
qed
lemma ae_delta_ss6_ss7_dest_valid:
assumes rel: "(s, a, s', a', d) ∈ ae_delta_ss6_ss7 M"
and src_valid: "ae_valid_stage (Γ_tm M) (le_tm M) (k_tm M) (snd s)"
shows "ae_valid_stage (Γ_tm M) (le_tm M) (k_tm M) (snd s')"
proof -
from rel obtain q ofs buf dest where
s_eq: "s = (q, ofs, buf, dest, SS6)"
and s'_eq: "s' = (q, ofs, buf, dest, SS7)"
unfolding ae_delta_ss6_ss7_def by auto
show ?thesis
using src_valid unfolding s_eq s'_eq ae_valid_stage_def by simp
qed
lemma ae_delta_ss7_ss8_dest_valid:
assumes rel: "(s, a, s', a', d) ∈ ae_delta_ss7_ss8 M"
and src_valid: "ae_valid_stage (Γ_tm M) (le_tm M) (k_tm M) (snd s)"
shows "ae_valid_stage (Γ_tm M) (le_tm M) (k_tm M) (snd s')"
proof -
from rel obtain q ofs buf dest where
s_eq: "s = (q, ofs, buf, dest, SS7)"
and s'_eq: "s' = (q, ofs, buf, dest, SS8)"
unfolding ae_delta_ss7_ss8_def by auto
show ?thesis
using src_valid unfolding s_eq s'_eq ae_valid_stage_def by simp
qed
lemma ae_delta_ss8_ss1_dest_valid:
assumes vM: "valid_mttm M"
and rel: "(s, a, s', a', d) ∈ ae_delta_ss8_ss1 M"
and src_valid: "ae_valid_stage (Γ_tm M) (le_tm M) (k_tm M) (snd s)"
shows "ae_valid_stage (Γ_tm M) (le_tm M) (k_tm M) (snd s')"
proof -
from rel obtain q ofs buf dest stage' where
s_eq: "s = (q, ofs, buf, dest, SS8)"
and s'_eq: "s' = (q, stage')"
and stage'_def: "stage' = (if q ∈ {t_tm M, r_tm M}
then init_stage (le_tm M)
else (ofs, buf, init_dest, SS1))"
unfolding ae_delta_ss8_ss1_def by auto
from src_valid s_eq have
buf_src: "∀k. fst (buf k) ∈ gamma_block (Γ_tm M)
∧ fst (snd (buf k)) ∈ gamma_block (Γ_tm M)
∧ snd (snd (buf k)) ∈ gamma_block (Γ_tm M)"
and src_off: "∀j≥k_tm M. ofs j = init_offset j"
and src_buf: "∀j≥k_tm M. buf j = init_buffer (le_tm M) j"
by (simp_all add: ae_valid_stage_def)
show ?thesis
proof (cases "q ∈ {t_tm M, r_tm M}")
case True
hence "stage' = init_stage (le_tm M)" using stage'_def by simp
moreover have "ae_valid_stage (Γ_tm M) (le_tm M) (k_tm M) (init_stage (le_tm M))"
using ae_valid_stage_init[OF valid_mttm_LE_in_Gamma[OF vM]] .
ultimately show ?thesis unfolding s'_eq by simp
next
case False
hence "stage' = (ofs, buf, init_dest, SS1)" using stage'_def by simp
thus ?thesis unfolding s'_eq ae_valid_stage_def
using buf_src src_off src_buf by simp
qed
qed
text ‹Validation-phase destination-stage-validity helpers. All 8
validation substeps preserve the buffer component, so the proofs
are mechanical: extract the stage destructuring from the relation
and propagate ‹src_valid›.›
lemma ae_delta_val_fwd_advance_dest_valid:
assumes rel: "(s, a, s', a', d) ∈ ae_delta_val_fwd_advance M"
and src_valid: "ae_valid_stage (Γ_tm M) (le_tm M) (k_tm M) (snd s)"
shows "ae_valid_stage (Γ_tm M) (le_tm M) (k_tm M) (snd s')"
proof -
from rel obtain q ofs buf dest where
s_eq: "s = (q, ofs, buf, dest, VFwd)"
and s'_eq: "s' = (q, ofs, buf, dest, VFwd)"
unfolding ae_delta_val_fwd_advance_def by auto
show ?thesis using src_valid unfolding s_eq s'_eq by simp
qed
lemma ae_delta_val_fwd_to_padded_dest_valid:
assumes rel: "(s, a, s', a', d) ∈ ae_delta_val_fwd_to_padded M"
and src_valid: "ae_valid_stage (Γ_tm M) (le_tm M) (k_tm M) (snd s)"
shows "ae_valid_stage (Γ_tm M) (le_tm M) (k_tm M) (snd s')"
proof -
from rel obtain q ofs buf dest where
s_eq: "s = (q, ofs, buf, dest, VFwd)"
and s'_eq: "s' = (q, ofs, buf, dest, VFwdPad)"
unfolding ae_delta_val_fwd_to_padded_def by auto
show ?thesis
using src_valid unfolding s_eq s'_eq ae_valid_stage_def by simp
qed
lemma ae_delta_val_fwd_reject_dest_valid:
assumes vM: "valid_mttm M"
and rel: "(s, a, s', a', d) ∈ ae_delta_val_fwd_reject M"
and src_valid: "ae_valid_stage (Γ_tm M) (le_tm M) (k_tm M) (snd s)"
shows "ae_valid_stage (Γ_tm M) (le_tm M) (k_tm M) (snd s')"
proof -
from rel have s'_eq: "s' = (r_tm M, init_stage (le_tm M))"
unfolding ae_delta_val_fwd_reject_def by auto
have "ae_valid_stage (Γ_tm M) (le_tm M) (k_tm M) (init_stage (le_tm M))"
using ae_valid_stage_init[OF valid_mttm_LE_in_Gamma[OF vM]] .
thus ?thesis unfolding s'_eq by simp
qed
lemma ae_delta_val_fwd_to_ret_dest_valid:
assumes rel: "(s, a, s', a', d) ∈ ae_delta_val_fwd_to_ret M"
and src_valid: "ae_valid_stage (Γ_tm M) (le_tm M) (k_tm M) (snd s)"
shows "ae_valid_stage (Γ_tm M) (le_tm M) (k_tm M) (snd s')"
proof -
from rel obtain q ofs buf dest where
s_eq: "s = (q, ofs, buf, dest, VFwd)"
and s'_eq: "s' = (q, ofs, buf, dest, VRet)"
unfolding ae_delta_val_fwd_to_ret_def by auto
show ?thesis
using src_valid unfolding s_eq s'_eq ae_valid_stage_def by simp
qed
lemma ae_delta_val_pad_to_ret_dest_valid:
assumes rel: "(s, a, s', a', d) ∈ ae_delta_val_pad_to_ret M"
and src_valid: "ae_valid_stage (Γ_tm M) (le_tm M) (k_tm M) (snd s)"
shows "ae_valid_stage (Γ_tm M) (le_tm M) (k_tm M) (snd s')"
proof -
from rel obtain q ofs buf dest where
s_eq: "s = (q, ofs, buf, dest, VFwdPad)"
and s'_eq: "s' = (q, ofs, buf, dest, VRet)"
unfolding ae_delta_val_pad_to_ret_def by auto
show ?thesis
using src_valid unfolding s_eq s'_eq ae_valid_stage_def by simp
qed
lemma ae_delta_val_pad_reject_dest_valid:
assumes vM: "valid_mttm M"
and rel: "(s, a, s', a', d) ∈ ae_delta_val_pad_reject M"
and src_valid: "ae_valid_stage (Γ_tm M) (le_tm M) (k_tm M) (snd s)"
shows "ae_valid_stage (Γ_tm M) (le_tm M) (k_tm M) (snd s')"
proof -
from rel have s'_eq: "s' = (r_tm M, init_stage (le_tm M))"
unfolding ae_delta_val_pad_reject_def by auto
have "ae_valid_stage (Γ_tm M) (le_tm M) (k_tm M) (init_stage (le_tm M))"
using ae_valid_stage_init[OF valid_mttm_LE_in_Gamma[OF vM]] .
thus ?thesis unfolding s'_eq by simp
qed
lemma ae_delta_val_ret_step_dest_valid:
assumes rel: "(s, a, s', a', d) ∈ ae_delta_val_ret_step M"
and src_valid: "ae_valid_stage (Γ_tm M) (le_tm M) (k_tm M) (snd s)"
shows "ae_valid_stage (Γ_tm M) (le_tm M) (k_tm M) (snd s')"
proof -
from rel obtain q ofs buf dest where
s_eq: "s = (q, ofs, buf, dest, VRet)"
and s'_eq: "s' = (q, ofs, buf, dest, VRet)"
unfolding ae_delta_val_ret_step_def by auto
show ?thesis using src_valid unfolding s_eq s'_eq by simp
qed
lemma ae_delta_val_ret_to_sim_dest_valid:
assumes rel: "(s, a, s', a', d) ∈ ae_delta_val_ret_to_sim M"
and src_valid: "ae_valid_stage (Γ_tm M) (le_tm M) (k_tm M) (snd s)"
shows "ae_valid_stage (Γ_tm M) (le_tm M) (k_tm M) (snd s')"
proof -
from rel obtain q ofs buf dest where
s_eq: "s = (q, ofs, buf, dest, VRet)"
and s'_eq: "s' = (q, ofs, buf, dest, SS1)"
unfolding ae_delta_val_ret_to_sim_def by auto
show ?thesis
using src_valid unfolding s_eq s'_eq ae_valid_stage_def by simp
qed
text ‹‹δ'› for the alphabet-enlargement combinator: the union of
the 16 per-substep relations, intersected with two restrictions.
First restriction: read / write blocks lie in
‹Γ' = gamma_block (Γ_tm M)›. This makes ‹δ'› satisfy
the substrate's ‹δ_set›-shape obligation.
Second restriction (added 2026-05-09 alongside the substrate's
‹δLE›-no-write strengthening): a transition writes
‹LE_block (le_tm M)› on tape ‹k› only when reading the same.
The substep relations for SS5‹→›SS8 produce write-back tuples
whose ‹a' k› can in unreachable buffer states (left or right
block holding ‹LE_block (le_tm M)›) equal ‹LE_block (le_tm M)›
without the read ‹a k› matching; the intersection drops those
tuples. Since reachable buffer states do not put ‹LE_block›
in left or right blocks (the LE block stays at M-position
0, below the simulation phase's ‹p_start ≥ 1› window), this is
semantically inert in reachable executions and exists only to
syntactically satisfy the substrate's universal
‹δLE›-no-write obligation.›
definition alphabet_enlarge_delta ::
"('q, 'a) mttm
⇒ (('q × ('a, 'c :: enum) ae_stage)
× (nat ⇒ ('c ⇒ 'a))
× ('q × ('a, 'c) ae_stage)
× (nat ⇒ ('c ⇒ 'a))
× (nat ⇒ dir)) set" where
"alphabet_enlarge_delta M =
(ae_delta_val_fwd_advance M
∪ ae_delta_val_fwd_to_padded M
∪ ae_delta_val_fwd_reject M
∪ ae_delta_val_fwd_to_ret M
∪ ae_delta_val_pad_to_ret M
∪ ae_delta_val_pad_reject M
∪ ae_delta_val_ret_step M
∪ ae_delta_val_ret_to_sim M
∪ ae_delta_ss1_ss2 M
∪ ae_delta_ss2_ss3 M
∪ ae_delta_ss3_ss4 M
∪ ae_delta_ss4_ss5 M
∪ ae_delta_ss5_ss6 M
∪ ae_delta_ss6_ss7 M
∪ ae_delta_ss7_ss8 M
∪ ae_delta_ss8_ss1 M)
∩ {(s, a, s', a', d).
(∀k. a k ∈ gamma_block (Γ_tm M))
∧ (∀k. a' k ∈ gamma_block (Γ_tm M))}
∩ {(s, a, s', a', d).
∀k. a' k = LE_block (le_tm M) ⟶ a k = LE_block (le_tm M)}
∩ {(s, a, s', a', d).
ae_valid_stage (Γ_tm M) (le_tm M) (k_tm M) (snd s)
∧ ae_valid_stage (Γ_tm M) (le_tm M) (k_tm M) (snd s')}"
subsection ‹Per-substep functionality (source determines target,
except SS4‹→›SS5)›
text ‹For each of the 15 non-compute substep relations, the source
configuration uniquely determines the target. These functionality
lemmas underpin the reverse-arm trace decoder: given an
‹M'›-step from a config with a known substep index, the
target components are mechanically read off.›
lemma ae_delta_val_fwd_advance_functional:
assumes "(s, a, s1, a1, d1) ∈ ae_delta_val_fwd_advance M"
and "(s, a, s2, a2, d2) ∈ ae_delta_val_fwd_advance M"
shows "s1 = s2 ∧ a1 = a2 ∧ d1 = d2"
using assms unfolding ae_delta_val_fwd_advance_def by auto
lemma ae_delta_val_fwd_to_padded_functional:
assumes "(s, a, s1, a1, d1) ∈ ae_delta_val_fwd_to_padded M"
and "(s, a, s2, a2, d2) ∈ ae_delta_val_fwd_to_padded M"
shows "s1 = s2 ∧ a1 = a2 ∧ d1 = d2"
using assms unfolding ae_delta_val_fwd_to_padded_def by auto
lemma ae_delta_val_fwd_reject_functional:
assumes "(s, a, s1, a1, d1) ∈ ae_delta_val_fwd_reject M"
and "(s, a, s2, a2, d2) ∈ ae_delta_val_fwd_reject M"
shows "s1 = s2 ∧ a1 = a2 ∧ d1 = d2"
using assms unfolding ae_delta_val_fwd_reject_def by auto
lemma ae_delta_val_fwd_to_ret_functional:
assumes "(s, a, s1, a1, d1) ∈ ae_delta_val_fwd_to_ret M"
and "(s, a, s2, a2, d2) ∈ ae_delta_val_fwd_to_ret M"
shows "s1 = s2 ∧ a1 = a2 ∧ d1 = d2"
using assms unfolding ae_delta_val_fwd_to_ret_def by auto
lemma ae_delta_val_pad_to_ret_functional:
assumes "(s, a, s1, a1, d1) ∈ ae_delta_val_pad_to_ret M"
and "(s, a, s2, a2, d2) ∈ ae_delta_val_pad_to_ret M"
shows "s1 = s2 ∧ a1 = a2 ∧ d1 = d2"
using assms unfolding ae_delta_val_pad_to_ret_def by auto
lemma ae_delta_val_pad_reject_functional:
assumes "(s, a, s1, a1, d1) ∈ ae_delta_val_pad_reject M"
and "(s, a, s2, a2, d2) ∈ ae_delta_val_pad_reject M"
shows "s1 = s2 ∧ a1 = a2 ∧ d1 = d2"
using assms unfolding ae_delta_val_pad_reject_def by auto
lemma ae_delta_val_ret_step_functional:
assumes "(s, a, s1, a1, d1) ∈ ae_delta_val_ret_step M"
and "(s, a, s2, a2, d2) ∈ ae_delta_val_ret_step M"
shows "s1 = s2 ∧ a1 = a2 ∧ d1 = d2"
using assms unfolding ae_delta_val_ret_step_def by auto
lemma ae_delta_val_ret_to_sim_functional:
assumes "(s, a, s1, a1, d1) ∈ ae_delta_val_ret_to_sim M"
and "(s, a, s2, a2, d2) ∈ ae_delta_val_ret_to_sim M"
shows "s1 = s2 ∧ a1 = a2 ∧ d1 = d2"
using assms unfolding ae_delta_val_ret_to_sim_def by auto
lemma ae_delta_ss1_ss2_functional:
assumes "(s, a, s1, a1, d1) ∈ ae_delta_ss1_ss2 M"
and "(s, a, s2, a2, d2) ∈ ae_delta_ss1_ss2 M"
shows "s1 = s2 ∧ a1 = a2 ∧ d1 = d2"
using assms unfolding ae_delta_ss1_ss2_def by auto
lemma ae_delta_ss2_ss3_functional:
assumes "(s, a, s1, a1, d1) ∈ ae_delta_ss2_ss3 M"
and "(s, a, s2, a2, d2) ∈ ae_delta_ss2_ss3 M"
shows "s1 = s2 ∧ a1 = a2 ∧ d1 = d2"
using assms unfolding ae_delta_ss2_ss3_def by auto
lemma ae_delta_ss3_ss4_functional:
assumes "(s, a, s1, a1, d1) ∈ ae_delta_ss3_ss4 M"
and "(s, a, s2, a2, d2) ∈ ae_delta_ss3_ss4 M"
shows "s1 = s2 ∧ a1 = a2 ∧ d1 = d2"
using assms unfolding ae_delta_ss3_ss4_def by auto
text ‹SS4‹→›SS5 (compute substep) functionality under
‹det_mttm M›: the source determines the target uniquely.
Unlike the other 15 substep functionality lemmas which follow
from pure definitional unfolding, this one consumes M's
determinism via ‹m_steps_buffered_functional› because
SS4‹→›SS5 is precisely where M's ‹δ› enters AE's
‹δ'›. Completes the 16th functionality entry; together
with the 15 simpler entries, this discharges the per-substep
functionality obligations of the reverse-arm chain-uniqueness
argument.›
lemma ae_delta_ss4_ss5_functional:
fixes M :: "('q, 'a) mttm"
assumes vM: "valid_mttm M"
and det: "det_mttm M"
and h1: "(s, a, s1, a1, d1) ∈ ae_delta_ss4_ss5 M"
and h2: "(s, a, s2, a2, d2) ∈ ae_delta_ss4_ss5 M"
shows "s1 = s2 ∧ a1 = a2 ∧ d1 = d2"
proof -
from h1 obtain q ofs buf dest_old q1' ofs1' buf1' dest1' buf_full1 end_pos1 bufC1
where sd1: "s = (q, ofs, buf, dest_old, SS4)"
and rs1: "s1 = (q1', ofs1', buf1', dest1', SS5)"
and ad1: "a1 = a"
and dd1: "d1 = (λk. if k < k_tm M
then (if a k = LE_block (le_tm M) then dir.N else dir.L)
else dir.N)"
and bf1: "buf_full1 = (λk. (fst (buf k),
if k < k_tm M then fst (snd (buf k)) else a k,
a k))"
and ms1: "((q, buf_full1, λk. (AE_Home, ofs k)),
(q1', bufC1, end_pos1)) ∈ m_steps_buffered M"
and of1: "ofs1' = (λk. if k < k_tm M then snd (end_pos1 k) else init_offset k)"
and bd1: "buf1' = (λk. if k < k_tm M then bufC1 k else init_buffer (le_tm M) k)"
and de1: "dest1' = (λk. if k < k_tm M then fst (end_pos1 k) else init_dest k)"
unfolding ae_delta_ss4_ss5_def by auto
from h2 obtain q2 ofs2v buf2v dest_old2 q2' ofs2' buf2' dest2' buf_full2 end_pos2 bufC2
where sd2: "s = (q2, ofs2v, buf2v, dest_old2, SS4)"
and rs2: "s2 = (q2', ofs2', buf2', dest2', SS5)"
and ad2: "a2 = a"
and dd2: "d2 = (λk. if k < k_tm M
then (if a k = LE_block (le_tm M) then dir.N else dir.L)
else dir.N)"
and bf2: "buf_full2 = (λk. (fst (buf2v k),
if k < k_tm M then fst (snd (buf2v k)) else a k,
a k))"
and ms2: "((q2, buf_full2, λk. (AE_Home, ofs2v k)),
(q2', bufC2, end_pos2)) ∈ m_steps_buffered M"
and of2: "ofs2' = (λk. if k < k_tm M then snd (end_pos2 k) else init_offset k)"
and bd2: "buf2' = (λk. if k < k_tm M then bufC2 k else init_buffer (le_tm M) k)"
and de2: "dest2' = (λk. if k < k_tm M then fst (end_pos2 k) else init_dest k)"
unfolding ae_delta_ss4_ss5_def by auto
from sd1 sd2 have q2_eq: "q2 = q" and ofs2_eq: "ofs2v = ofs"
and buf2_eq: "buf2v = buf" by simp_all
have bf_eq: "buf_full2 = buf_full1"
unfolding bf1 bf2 buf2_eq by (rule refl)
have ms2': "((q, buf_full1, λk. (AE_Home, ofs k)),
(q2', bufC2, end_pos2)) ∈ m_steps_buffered M"
using ms2 q2_eq ofs2_eq bf_eq by simp
from m_steps_buffered_functional[OF vM det ms1 ms2']
have target_eq: "(q1', bufC1, end_pos1) = (q2', bufC2, end_pos2)" .
hence q'_eq: "q1' = q2'" and bufC_eq: "bufC1 = bufC2"
and ep_eq: "end_pos1 = end_pos2" by auto
show ?thesis
proof (intro conjI)
show "s1 = s2"
using rs1 rs2 of1 of2 bd1 bd2 de1 de2 q'_eq bufC_eq ep_eq
by (simp add: fun_eq_iff)
show "a1 = a2" using ad1 ad2 by simp
show "d1 = d2" using dd1 dd2 by simp
qed
qed
lemma ae_delta_ss5_ss6_functional:
assumes "(s, a, s1, a1, d1) ∈ ae_delta_ss5_ss6 M"
and "(s, a, s2, a2, d2) ∈ ae_delta_ss5_ss6 M"
shows "s1 = s2 ∧ a1 = a2 ∧ d1 = d2"
using assms unfolding ae_delta_ss5_ss6_def by auto
lemma ae_delta_ss6_ss7_functional:
assumes "(s, a, s1, a1, d1) ∈ ae_delta_ss6_ss7 M"
and "(s, a, s2, a2, d2) ∈ ae_delta_ss6_ss7 M"
shows "s1 = s2 ∧ a1 = a2 ∧ d1 = d2"
using assms unfolding ae_delta_ss6_ss7_def by auto
lemma ae_delta_ss7_ss8_functional:
assumes "(s, a, s1, a1, d1) ∈ ae_delta_ss7_ss8 M"
and "(s, a, s2, a2, d2) ∈ ae_delta_ss7_ss8 M"
shows "s1 = s2 ∧ a1 = a2 ∧ d1 = d2"
using assms unfolding ae_delta_ss7_ss8_def by auto
lemma ae_delta_ss8_ss1_functional:
assumes "(s, a, s1, a1, d1) ∈ ae_delta_ss8_ss1 M"
and "(s, a, s2, a2, d2) ∈ ae_delta_ss8_ss1 M"
shows "s1 = s2 ∧ a1 = a2 ∧ d1 = d2"
using assms unfolding ae_delta_ss8_ss1_def by (auto split: if_split_asm)
text ‹Within-phase exclusion: for each source substep index with
multiple relations (VFwd: 4, VFwdPad: 2, VRet: 2), the relations
do not overlap. These lemmas commit the reverse-arm trace
decoder to a specific branch.›
lemma ae_delta_val_pad_to_ret_pad_reject_disjoint:
assumes "(s, a, s1, a1, d1) ∈ ae_delta_val_pad_to_ret M"
and "(s, a, s2, a2, d2) ∈ ae_delta_val_pad_reject M"
shows "False"
using assms unfolding ae_delta_val_pad_to_ret_def ae_delta_val_pad_reject_def
by auto
lemma ae_delta_val_ret_step_ret_to_sim_disjoint:
assumes "(s, a, s1, a1, d1) ∈ ae_delta_val_ret_step M"
and "(s, a, s2, a2, d2) ∈ ae_delta_val_ret_to_sim M"
shows "False"
using assms unfolding ae_delta_val_ret_step_def ae_delta_val_ret_to_sim_def
by auto
text ‹Cross-phase exclusion: a tuple in ‹alphabet_enlarge_delta M›
whose source state has substep index ‹SSn› lies in the
matching ‹ae_delta_ssn_ssm M› (and not in any other relation
of the union). Each of the 16 union components pins its source
substep index to a specific value; the 15 other relations have
source substep indices in
‹{VFwd, VFwdPad, VRet, SS1, …, SS8} ∖ {SSn}›, hence
cannot match. The alphabet intersection clauses are preserved
through the conclusion (membership in
‹ae_delta_ssn_ssm M› does not require them, so we discard
them). Used by the reverse-arm trace decoder to commit each
peeled ‹δ'›-step to its canonical substep.›
lemma ae_delta_ss1_only:
fixes M :: "('q, 'a) mttm"
assumes "(s, a, s', a', d) ∈ alphabet_enlarge_delta M"
and "snd (snd (snd (snd s))) = SS1"
shows "(s, a, s', a', d) ∈ ae_delta_ss1_ss2 M"
using assms
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_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
lemma ae_delta_ss2_only:
fixes M :: "('q, 'a) mttm"
assumes "(s, a, s', a', d) ∈ alphabet_enlarge_delta M"
and "snd (snd (snd (snd s))) = SS2"
shows "(s, a, s', a', d) ∈ ae_delta_ss2_ss3 M"
using assms
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_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
lemma ae_delta_ss3_only:
fixes M :: "('q, 'a) mttm"
assumes "(s, a, s', a', d) ∈ alphabet_enlarge_delta M"
and "snd (snd (snd (snd s))) = SS3"
shows "(s, a, s', a', d) ∈ ae_delta_ss3_ss4 M"
using assms
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_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
lemma ae_delta_ss4_only:
fixes M :: "('q, 'a) mttm"
assumes "(s, a, s', a', d) ∈ alphabet_enlarge_delta M"
and "snd (snd (snd (snd s))) = SS4"
shows "(s, a, s', a', d) ∈ ae_delta_ss4_ss5 M"
using assms
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_ss5_ss6_def
ae_delta_ss6_ss7_def
ae_delta_ss7_ss8_def
ae_delta_ss8_ss1_def
by auto
lemma ae_delta_ss5_only:
fixes M :: "('q, 'a) mttm"
assumes "(s, a, s', a', d) ∈ alphabet_enlarge_delta M"
and "snd (snd (snd (snd s))) = SS5"
shows "(s, a, s', a', d) ∈ ae_delta_ss5_ss6 M"
using assms
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_ss6_ss7_def
ae_delta_ss7_ss8_def
ae_delta_ss8_ss1_def
by auto
lemma ae_delta_ss6_only:
fixes M :: "('q, 'a) mttm"
assumes "(s, a, s', a', d) ∈ alphabet_enlarge_delta M"
and "snd (snd (snd (snd s))) = SS6"
shows "(s, a, s', a', d) ∈ ae_delta_ss6_ss7 M"
using assms
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_ss7_ss8_def
ae_delta_ss8_ss1_def
by auto
lemma ae_delta_ss7_only:
fixes M :: "('q, 'a) mttm"
assumes "(s, a, s', a', d) ∈ alphabet_enlarge_delta M"
and "snd (snd (snd (snd s))) = SS7"
shows "(s, a, s', a', d) ∈ ae_delta_ss7_ss8 M"
using assms
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_ss8_ss1_def
by auto
lemma ae_delta_ss8_only:
fixes M :: "('q, 'a) mttm"
assumes "(s, a, s', a', d) ∈ alphabet_enlarge_delta M"
and "snd (snd (snd (snd s))) = SS8"
shows "(s, a, s', a', d) ∈ ae_delta_ss8_ss1 M"
using assms
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
by auto
end