Theory AlphabetEnlargement_ComputeCorrect
theory AlphabetEnlargement_ComputeCorrect
imports AlphabetEnlargement_ValidationBound
begin
text ‹Entry point of the ‹alphabet_enlarge›
forward-simulation chain (the combinator is defined in
‹AlphabetEnlargement_Simulation›). The chain establishes
that ‹M' = alphabet_enlarge M› simulates ‹M›, and
culminates in the three top-level theorems characterising the
combinator — well-formedness preservation
(‹alphabet_enlarge_wf›), forward language preservation
modulo input encoding
(‹alphabet_enlarge_language_forward›), and the linear
time bound (‹alphabet_enlarge_time›) — which are proved
in theory ‹AlphabetEnlargement› at the end of the chain.
The construction follows the linear-speedup theorem of
Hartmanis and Stearns
\<^cite>‹‹Theorem 2› in "Hartmanis1965:computational"›,
modernised in Hopcroft and Ullman
\<^cite>‹‹Theorem 12.3› in "Hopcroft1979:introduction"›.
The forward chain is split across theories in dependency
order, each importing the previous:
▪ ‹AlphabetEnlargement_ComputeCorrect› (this theory):
per-substep state shape and invariant preservation, the
‹mttm_step› lift, and buffered c-fold compute
correctness.
▪ ‹AlphabetEnlargement_SS4›: SS4 trace-existence and
the buffer characterisations at SS4 entry.
▪ ‹AlphabetEnlargement_OutputWF›: home classification
and output well-formedness.
▪ ‹AlphabetEnlargement_ForwardStage›: the per-tape
unified forward stage
‹ae_simulates_forward_stage_general›.
▪ ‹AlphabetEnlargement_Acceptance›: acceptance
correspondence and the step-count / chunked simulation
engine.
▪ ‹AlphabetEnlargement›: the three top-level
theorems.›
subsection ‹Forward simulation chain›
subsubsection ‹Per-substep state shape and invariant preservation›
text ‹Per-substep mid-stage invariant preservation lemmas.
Eight in total, one per simulation substep transition
SS‹n›‹→›SS‹n+1› (with SS9 ‹≡› SS1 by
wrap-around).›
text ‹Common skeleton: each per-substep delta is a set of
tuples whose post-state component fixes ‹idx› at the target
substep and constrains ‹q› via ‹q ∈ Q_tm M›.
This helper packages the ‹mttm_step›-elimination plus the
set-comprehension destructuring once, reducing each per-substep
proof to a one-line shape obligation discharged by ‹auto› on
the relevant ‹ae_delta_ss<N>_ss<N+1>_def›.
The helper does not apply to ‹ae_step_ss8_ss1_invariant›:
that substep's halting branch lands at ‹idx = VFwd›, not
‹idx = SS1›, so the post-state's ‹idx› is not uniformly
fixed.›
lemma ae_substep_state_shape:
fixes M :: "('q, 'a) mttm"
and δ :: "(('q × ('a, 'c :: enum) ae_stage)
× (nat ⇒ ('c ⇒ 'a))
× ('q × ('a, 'c) ae_stage)
× (nat ⇒ ('c ⇒ 'a))
× (nat ⇒ dir)) set"
and c' c'' :: "('c :: enum ⇒ 'a,
'q × ('a, 'c) ae_stage) mt_config"
and tgt :: substep_idx
assumes step: "(c', c'') ∈ mttm_step δ"
and shape: "⋀s a s' a' d.
(s, a, s', a', d) ∈ δ
⟹ ∃q ofs buf dest.
s' = (q, ofs, buf, dest, tgt)
∧ q ∈ Q_tm M"
shows "case mt_state c'' of (qM', _, _, _, idx) ⇒
idx = tgt ∧ qM' ∈ Q_tm M"
proof -
from step obtain s ts n s' a' d where
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) ∈ δ"
by (auto elim: mttm_step.cases)
from shape[OF rel] obtain q ofs buf dest where
s'_eq: "s' = (q, ofs, buf, dest, tgt)"
and q_in: "q ∈ Q_tm M"
by blast
show ?thesis using c''_eq s'_eq q_in by simp
qed
lemma ae_step_ss1_ss2_invariant:
fixes M :: "('q, 'a) mttm"
and c' c'' :: "('c :: enum ⇒ 'a,
'q × ('a, 'c) ae_stage) mt_config"
assumes "valid_mttm M"
and "ae_inv_ss1 M c'"
and "(c', c'') ∈ mttm_step (ae_delta_ss1_ss2 M)"
shows "ae_inv_ss2 M c''"
proof -
have shape: "⋀s a s' a' d.
(s, a, s', a', d) ∈ ae_delta_ss1_ss2 M
⟹ ∃q ofs buf dest.
s' = (q, ofs, buf, dest, SS2)
∧ q ∈ Q_tm M"
by (force simp: ae_delta_ss1_ss2_def)
show "ae_inv_ss2 M c''"
unfolding ae_inv_ss2_def
using ae_substep_state_shape[OF assms(3) shape] .
qed
lemma ae_step_ss2_ss3_invariant:
fixes M :: "('q, 'a) mttm"
and c' c'' :: "('c :: enum ⇒ 'a,
'q × ('a, 'c) ae_stage) mt_config"
assumes "valid_mttm M"
and "ae_inv_ss2 M c'"
and "(c', c'') ∈ mttm_step (ae_delta_ss2_ss3 M)"
shows "ae_inv_ss3 M c''"
proof -
have shape: "⋀s a s' a' d.
(s, a, s', a', d) ∈ ae_delta_ss2_ss3 M
⟹ ∃q ofs buf dest.
s' = (q, ofs, buf, dest, SS3)
∧ q ∈ Q_tm M"
by (force simp: ae_delta_ss2_ss3_def)
show "ae_inv_ss3 M c''"
unfolding ae_inv_ss3_def
using ae_substep_state_shape[OF assms(3) shape] .
qed
lemma ae_step_ss3_ss4_invariant:
fixes M :: "('q, 'a) mttm"
and c' c'' :: "('c :: enum ⇒ 'a,
'q × ('a, 'c) ae_stage) mt_config"
assumes "valid_mttm M"
and "ae_inv_ss3 M c'"
and "(c', c'') ∈ mttm_step (ae_delta_ss3_ss4 M)"
shows "ae_inv_ss4 M c''"
proof -
have shape: "⋀s a s' a' d.
(s, a, s', a', d) ∈ ae_delta_ss3_ss4 M
⟹ ∃q ofs buf dest.
s' = (q, ofs, buf, dest, SS4)
∧ q ∈ Q_tm M"
by (force simp: ae_delta_ss3_ss4_def)
show "ae_inv_ss4 M c''"
unfolding ae_inv_ss4_def
using ae_substep_state_shape[OF assms(3) shape] .
qed
lemma ae_step_ss4_ss5_invariant:
fixes M :: "('q, 'a) mttm"
and c' c'' :: "('c :: enum ⇒ 'a,
'q × ('a, 'c) ae_stage) mt_config"
assumes valM: "valid_mttm M"
and "ae_inv_ss4 M c'"
and step: "(c', c'') ∈ mttm_step (ae_delta_ss4_ss5 M)"
shows "ae_inv_ss5 M c''"
proof -
from step obtain s ts n s' a' d where
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) ∈ ae_delta_ss4_ss5 M"
by (auto elim: mttm_step.cases)
from rel[unfolded ae_delta_ss4_ss5_def mem_Collect_eq]
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 q_Q: "q ∈ Q_tm M"
and m_steps: "((q, buf_full, λk. (AE_Home, ofs k)),
(q', bufC, end_pos))
∈ m_steps_buffered M"
by auto
from m_steps_buffered_state_preservation[OF valM m_steps q_Q]
have q'_in_Q: "q' ∈ Q_tm M" .
show "ae_inv_ss5 M c''"
unfolding ae_inv_ss5_def using c''_eq s'_eq q'_in_Q by simp
qed
lemma ae_step_ss5_ss6_invariant:
fixes M :: "('q, 'a) mttm"
and c' c'' :: "('c :: enum ⇒ 'a,
'q × ('a, 'c) ae_stage) mt_config"
assumes "valid_mttm M"
and "ae_inv_ss5 M c'"
and "(c', c'') ∈ mttm_step (ae_delta_ss5_ss6 M)"
shows "ae_inv_ss6 M c''"
proof -
have shape: "⋀s a s' a' d.
(s, a, s', a', d) ∈ ae_delta_ss5_ss6 M
⟹ ∃q ofs buf dest.
s' = (q, ofs, buf, dest, SS6)
∧ q ∈ Q_tm M"
by (force simp: ae_delta_ss5_ss6_def)
show "ae_inv_ss6 M c''"
unfolding ae_inv_ss6_def
using ae_substep_state_shape[OF assms(3) shape] .
qed
lemma ae_step_ss6_ss7_invariant:
fixes M :: "('q, 'a) mttm"
and c' c'' :: "('c :: enum ⇒ 'a,
'q × ('a, 'c) ae_stage) mt_config"
assumes "valid_mttm M"
and "ae_inv_ss6 M c'"
and "(c', c'') ∈ mttm_step (ae_delta_ss6_ss7 M)"
shows "ae_inv_ss7 M c''"
proof -
have shape: "⋀s a s' a' d.
(s, a, s', a', d) ∈ ae_delta_ss6_ss7 M
⟹ ∃q ofs buf dest.
s' = (q, ofs, buf, dest, SS7)
∧ q ∈ Q_tm M"
by (force simp: ae_delta_ss6_ss7_def)
show "ae_inv_ss7 M c''"
unfolding ae_inv_ss7_def
using ae_substep_state_shape[OF assms(3) shape] .
qed
lemma ae_step_ss7_ss8_invariant:
fixes M :: "('q, 'a) mttm"
and c' c'' :: "('c :: enum ⇒ 'a,
'q × ('a, 'c) ae_stage) mt_config"
assumes "valid_mttm M"
and "ae_inv_ss7 M c'"
and "(c', c'') ∈ mttm_step (ae_delta_ss7_ss8 M)"
shows "ae_inv_ss8 M c''"
proof -
have shape: "⋀s a s' a' d.
(s, a, s', a', d) ∈ ae_delta_ss7_ss8 M
⟹ ∃q ofs buf dest.
s' = (q, ofs, buf, dest, SS8)
∧ q ∈ Q_tm M"
by (force simp: ae_delta_ss7_ss8_def)
show "ae_inv_ss8 M c''"
unfolding ae_inv_ss8_def
using ae_substep_state_shape[OF assms(3) shape] .
qed
lemma ae_step_ss8_ss1_invariant:
fixes M :: "('q, 'a) mttm"
and c' c'' :: "('c :: enum ⇒ 'a,
'q × ('a, 'c) ae_stage) mt_config"
assumes "valid_mttm M"
and "ae_inv_ss8 M c'"
and non_halt: "case mt_state c' of (qM', _, _, _, _) ⇒
qM' ≠ t_tm M ∧ qM' ≠ r_tm M"
and step: "(c', c'') ∈ mttm_step (ae_delta_ss8_ss1 M)"
shows "ae_inv_ss1 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) ∈ ae_delta_ss8_ss1 M"
by (auto elim: mttm_step.cases)
from rel obtain q ofs buf dest stage' where
s_eq: "s = (q, ofs, buf, dest, SS8)"
and s'_eq: "s' = (q, stage')"
and q_in: "q ∈ Q_tm M"
and stage'_eq: "stage' = (if q ∈ {t_tm M, r_tm M}
then init_stage (le_tm M)
else (ofs, buf, init_dest, SS1))"
by (auto simp: ae_delta_ss8_ss1_def)
from non_halt c'_eq s_eq have q_non_halt: "q ≠ t_tm M ∧ q ≠ r_tm M"
by simp
with stage'_eq have stage'_resolved:
"stage' = (ofs, buf, init_dest, SS1)" by simp
show "ae_inv_ss1 M c''"
unfolding ae_inv_ss1_def
using c''_eq s'_eq stage'_resolved q_in by simp
qed
text ‹Halt-branch invariant for SS8‹→›SS1: when
‹M›'s simulated state at SS8 is halting
(‹qM' ∈ {t_tm M, r_tm M}›), the SS8‹→›SS1
step routes to ‹init_stage le› (post-idx is ‹VFwd›, not
‹SS1›) and preserves the halt-state ‹q›. Companion to
‹ae_step_ss8_ss1_invariant› (non-halt branch). The chain
proof in ‹ae_simulates_forward_stage› case-splits on whether
‹M›'s state is halting at SS8 and applies one of these two
lemmas accordingly; the halt branch lands in the simulation's
halt disjunct (‹qM' ∈ {t_tm M, r_tm M}›), the non-halt
branch in the SS1 disjunct.›
lemma ae_step_ss8_ss1_invariant_halt:
fixes M :: "('q, 'a) mttm"
and c' c'' :: "('c :: enum ⇒ 'a,
'q × ('a, 'c) ae_stage) mt_config"
assumes inv: "ae_inv_ss8 M c'"
and halt: "case mt_state c' of (qM', _, _, _, _) ⇒
qM' ∈ {t_tm M, r_tm M}"
and step: "(c', c'') ∈ mttm_step (ae_delta_ss8_ss1 M)"
shows "(case mt_state c'' of (qM', _, _, _, idx) ⇒
qM' ∈ {t_tm M, r_tm M} ∧ idx = VFwd)"
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) ∈ ae_delta_ss8_ss1 M"
by (auto elim: mttm_step.cases)
from rel obtain q ofs buf dest stage' where
s_eq: "s = (q, ofs, buf, dest, SS8)"
and s'_eq: "s' = (q, stage')"
and q_in: "q ∈ Q_tm M"
and stage'_eq: "stage' = (if q ∈ {t_tm M, r_tm M}
then init_stage (le_tm M)
else (ofs, buf, init_dest, SS1))"
by (auto simp: ae_delta_ss8_ss1_def)
from halt c'_eq s_eq have q_halt: "q ∈ {t_tm M, r_tm M}"
by simp
with stage'_eq have stage'_resolved:
"stage' = init_stage (le_tm M)" by simp
show ?thesis
using c''_eq s'_eq stage'_resolved q_halt
unfolding init_stage_def by simp
qed
subsubsection ‹‹mttm_step› lifts of cross-phase exclusions›
text ‹‹mttm_step›-level lifts of the cross-phase exclusion
lemmas ‹ae_delta_ssN_only›: when a substrate-level step
in the alphabet-enlarged combinator's union has source
‹substep_idx› ‹SSN›, the step is in the canonical
‹ae_delta_ssN_ssM› substep relation. Used by the reverse
arm to commit each peeled ‹δ'›-step to its canonical
substep before invoking the per-substep invariant
propagation.›
lemma mttm_step_ae_delta_ss1_only:
fixes M :: "('q, 'a) mttm"
and c c' :: "('c :: enum ⇒ 'a,
'q × ('a, 'c) ae_stage) mt_config"
assumes step: "(c, c') ∈ mttm_step (alphabet_enlarge_delta M)"
and ss1: "snd (snd (snd (snd (mt_state c)))) = SS1"
shows "(c, c') ∈ mttm_step (ae_delta_ss1_ss2 M)"
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 ss1 c_eq have s_ss1: "snd (snd (snd (snd s))) = SS1"
by simp
have rel_sub: "(s, (λk. ts k (n k)), s', a', d)
∈ ae_delta_ss1_ss2 M"
by (rule ae_delta_ss1_only[OF rel s_ss1])
show ?thesis
unfolding c_eq c'_eq
by (rule mttm_step.step[where ts = ts and n = n and a = a' and dir = d,
OF rel_sub])
qed
lemma mttm_step_ae_delta_ss2_only:
fixes M :: "('q, 'a) mttm"
and c c' :: "('c :: enum ⇒ 'a,
'q × ('a, 'c) ae_stage) mt_config"
assumes step: "(c, c') ∈ mttm_step (alphabet_enlarge_delta M)"
and ss2: "snd (snd (snd (snd (mt_state c)))) = SS2"
shows "(c, c') ∈ mttm_step (ae_delta_ss2_ss3 M)"
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 ss2 c_eq have s_ss2: "snd (snd (snd (snd s))) = SS2"
by simp
have rel_sub: "(s, (λk. ts k (n k)), s', a', d)
∈ ae_delta_ss2_ss3 M"
by (rule ae_delta_ss2_only[OF rel s_ss2])
show ?thesis
unfolding c_eq c'_eq
by (rule mttm_step.step[where ts = ts and n = n and a = a' and dir = d,
OF rel_sub])
qed
lemma mttm_step_ae_delta_ss3_only:
fixes M :: "('q, 'a) mttm"
and c c' :: "('c :: enum ⇒ 'a,
'q × ('a, 'c) ae_stage) mt_config"
assumes step: "(c, c') ∈ mttm_step (alphabet_enlarge_delta M)"
and ss3: "snd (snd (snd (snd (mt_state c)))) = SS3"
shows "(c, c') ∈ mttm_step (ae_delta_ss3_ss4 M)"
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 ss3 c_eq have s_ss3: "snd (snd (snd (snd s))) = SS3"
by simp
have rel_sub: "(s, (λk. ts k (n k)), s', a', d)
∈ ae_delta_ss3_ss4 M"
by (rule ae_delta_ss3_only[OF rel s_ss3])
show ?thesis
unfolding c_eq c'_eq
by (rule mttm_step.step[where ts = ts and n = n and a = a' and dir = d,
OF rel_sub])
qed
lemma mttm_step_ae_delta_ss4_only:
fixes M :: "('q, 'a) mttm"
and c c' :: "('c :: enum ⇒ 'a,
'q × ('a, 'c) ae_stage) mt_config"
assumes step: "(c, c') ∈ mttm_step (alphabet_enlarge_delta M)"
and ss4: "snd (snd (snd (snd (mt_state c)))) = SS4"
shows "(c, c') ∈ mttm_step (ae_delta_ss4_ss5 M)"
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 ss4 c_eq have s_ss4: "snd (snd (snd (snd s))) = SS4"
by simp
have rel_sub: "(s, (λk. ts k (n k)), s', a', d)
∈ ae_delta_ss4_ss5 M"
by (rule ae_delta_ss4_only[OF rel s_ss4])
show ?thesis
unfolding c_eq c'_eq
by (rule mttm_step.step[where ts = ts and n = n and a = a' and dir = d,
OF rel_sub])
qed
lemma mttm_step_ae_delta_ss5_only:
fixes M :: "('q, 'a) mttm"
and c c' :: "('c :: enum ⇒ 'a,
'q × ('a, 'c) ae_stage) mt_config"
assumes step: "(c, c') ∈ mttm_step (alphabet_enlarge_delta M)"
and ss5: "snd (snd (snd (snd (mt_state c)))) = SS5"
shows "(c, c') ∈ mttm_step (ae_delta_ss5_ss6 M)"
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 ss5 c_eq have s_ss5: "snd (snd (snd (snd s))) = SS5"
by simp
have rel_sub: "(s, (λk. ts k (n k)), s', a', d)
∈ ae_delta_ss5_ss6 M"
by (rule ae_delta_ss5_only[OF rel s_ss5])
show ?thesis
unfolding c_eq c'_eq
by (rule mttm_step.step[where ts = ts and n = n and a = a' and dir = d,
OF rel_sub])
qed
lemma mttm_step_ae_delta_ss6_only:
fixes M :: "('q, 'a) mttm"
and c c' :: "('c :: enum ⇒ 'a,
'q × ('a, 'c) ae_stage) mt_config"
assumes step: "(c, c') ∈ mttm_step (alphabet_enlarge_delta M)"
and ss6: "snd (snd (snd (snd (mt_state c)))) = SS6"
shows "(c, c') ∈ mttm_step (ae_delta_ss6_ss7 M)"
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 ss6 c_eq have s_ss6: "snd (snd (snd (snd s))) = SS6"
by simp
have rel_sub: "(s, (λk. ts k (n k)), s', a', d)
∈ ae_delta_ss6_ss7 M"
by (rule ae_delta_ss6_only[OF rel s_ss6])
show ?thesis
unfolding c_eq c'_eq
by (rule mttm_step.step[where ts = ts and n = n and a = a' and dir = d,
OF rel_sub])
qed
lemma mttm_step_ae_delta_ss7_only:
fixes M :: "('q, 'a) mttm"
and c c' :: "('c :: enum ⇒ 'a,
'q × ('a, 'c) ae_stage) mt_config"
assumes step: "(c, c') ∈ mttm_step (alphabet_enlarge_delta M)"
and ss7: "snd (snd (snd (snd (mt_state c)))) = SS7"
shows "(c, c') ∈ mttm_step (ae_delta_ss7_ss8 M)"
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 ss7 c_eq have s_ss7: "snd (snd (snd (snd s))) = SS7"
by simp
have rel_sub: "(s, (λk. ts k (n k)), s', a', d)
∈ ae_delta_ss7_ss8 M"
by (rule ae_delta_ss7_only[OF rel s_ss7])
show ?thesis
unfolding c_eq c'_eq
by (rule mttm_step.step[where ts = ts and n = n and a = a' and dir = d,
OF rel_sub])
qed
lemma mttm_step_ae_delta_ss8_only:
fixes M :: "('q, 'a) mttm"
and c c' :: "('c :: enum ⇒ 'a,
'q × ('a, 'c) ae_stage) mt_config"
assumes step: "(c, c') ∈ mttm_step (alphabet_enlarge_delta M)"
and ss8: "snd (snd (snd (snd (mt_state c)))) = SS8"
shows "(c, c') ∈ mttm_step (ae_delta_ss8_ss1 M)"
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 ss8 c_eq have s_ss8: "snd (snd (snd (snd s))) = SS8"
by simp
have rel_sub: "(s, (λk. ts k (n k)), s', a', d)
∈ ae_delta_ss8_ss1 M"
by (rule ae_delta_ss8_only[OF rel s_ss8])
show ?thesis
unfolding c_eq c'_eq
by (rule mttm_step.step[where ts = ts and n = n and a = a' and dir = d,
OF rel_sub])
qed
subsubsection ‹Buffered c-fold compute correctness›
text ‹Algebraic correctness of the buffered c-fold compute:
starting from a 3-block buffer matching a 3c-cell window of
the M-tape, with M's head at the home block and within the
non-LE region, the buffered compute simulates M's actual
c-step trace. The conclusion exhibits a buffered-compute
trajectory and a matching M-trace, with the post-state buffer
/ head still satisfying the window invariant.
Proof skeleton:
Induction on a step counter ‹i ∈ [0, c]›.
Base case (‹i = 0›): pre-state matches itself by the
‹window› hypothesis.
Step case (‹i ≤ c›): assume the IH holds at step ‹i›.
Either M halts at ‹i› (early-stop branch fires;
‹q_i ∈ {t, r}›; done), or M takes an ‹(i + 1)›-st step.
In the second sub-case:
1. Read symbol from the buffer at IH's ‹bp_i› via
‹read_bp›; the window invariant gives this equals
‹tsM_i (nM_i)›.
2. Apply M's ‹δ› (total on non-halting states by
‹valid_mttm›) to get ‹(q_{i+1}, a', d)›.
3. Write ‹a' k› back to the buffer via ‹write_bp›.
4. Advance ‹bp_i› via ‹bp_advance_le›. The load-bearing
claim is that this returns ‹Some bp_{i+1}› (i.e., the
head doesn't walk off the buffer). This holds because
displacement after ‹i + 1› steps is at most ‹i + 1
≤ c›, and the buffer covers 3c positions with the
head starting at home (linearised positions
‹[c, 2c-1]›), so the head stays within
‹[1, 3c-2] ⊂ [0, 3c-1]›.
5. Verify the post-state still satisfies the window
invariant: same ‹p_start›; new ‹bp_{i+1}›;
buffer's linearised reading at position
‹bp_linear bp_{i+1}› agrees with ‹tsM_{i+1}› at
‹nM_{i+1}›.
The step case's load-bearing arithmetic (item 4) is a
‹bp_advance_le›-vs-tape-position commutation lemma:
‹bp_linear› of the advanced ‹bp› equals the
linearised tape position relative to ‹p_start›. This
sub-lemma is non-trivial but standalone — it doesn't depend
on M's ‹δ›, only on the encoding's arithmetic.
The ‹delta_total› precondition rules out the
stuck-non-halt case: the substrate's ‹δ_set› axiom
permits non-halting states with no ‹δ›-successor
(‹δ ⊆ (Q - {t,r}) × ...› is a subset, not an
equality). Without this hypothesis the conclusion is
unprovable: a stuck ‹qM› has no buffered run and is
non-halt, so neither disjunct of the final claim can hold.
Hartmanis and Stearns's Theorem 2 implicitly assumes ‹δ› is
total on ‹Q - {t,r}›; a caller whose machines are total by
construction discharges this precondition trivially.›
text ‹Per-tape unified companion of ‹ae_coupled_run_aux›,
‹_le0›, and ‹_le1›. Takes a per-tape regime
selector ‹pos :: nat ⇒ nat› (= ‹mt_pos c' k›
at the SS4 entry) and the per-tape hybrid window-invariant
predicate ‹ae_window_invariant_general›, which
dispatches internally on each tape's regime. The buffered
run is the same simultaneous ‹m_step_buffered M›
relation as the three siblings — the regime selector is
frozen per tape during the run (‹m_step_buffered›
has no ‹c'› in scope), so per-tape regime case-splits
commute with the induction on ‹n›.
The no-LE hypothesis is per-tape regime-aware: width
‹c› for ‹pos = 0›, ‹2c› for
‹pos = 1›, ‹3c› for ‹pos ≥ 2›.
Uniform ‹p_start = (pos - 2) * c + 1› simplifies to
‹1› on ‹pos ∈ {0, 1}› by nat arithmetic,
matching the three siblings' ‹Suc i› shape.
The post-compute left-slot guard
(‹fst (buf' k) ≠ LE_block›) is preserved on
‹pos = 0› tapes (the generalisation of the le0 chain
strengthening); le1 tapes have ‹fst (buf k) = LE_block›
on entry, and steady tapes do not need this property at the
SS4‹→›SS5 boundary.
It sits alongside
‹ae_coupled_run_aux_le0› and ‹_le1› as
load-bearing inductive helpers. Consumer:
‹ae_m_steps_buffered_correct_trace_general›, feeding
‹ae_step_ss4_ss5_exists_general_trace›, which closes
the SS4‹→›SS5 trace in
‹ae_simulates_forward_stage_general›'s body.›
lemma ae_coupled_run_aux_general:
fixes M :: "('q, 'a) mttm"
and qM :: 'q
and tsM :: "nat ⇒ nat ⇒ 'a"
and nM :: "nat ⇒ nat"
and ofs :: "nat ⇒ ('c :: enum)"
and buf_full :: "nat ⇒ (('c ⇒ 'a) × ('c ⇒ 'a) × ('c ⇒ 'a))"
and pos :: "nat ⇒ nat"
and n :: nat
and cM_n :: "('a, 'q) mt_config"
assumes vM: "valid_mttm M"
and lu: "le_unique M"
and qM_in: "qM ∈ Q_tm M"
and window: "∀k<k_tm M. ae_window_invariant_general (tsM k) (nM k)
(AE_Home, ofs k) (buf_full k) (pos k) (le_tm M)"
and pad_home: "∀k≥k_tm M. fst (snd (buf_full k)) = bl_block (bl_tm M)"
and trace: "(Config⇩M qM tsM nM, cM_n)
∈ mttm_step (delta_tm M) ^^ n"
and n_bound: "n ≤ card (UNIV :: 'c set)"
and no_le:
"∀k. (pos k = 0
⟶ (∀i. i < card (UNIV :: 'c set)
⟶ tsM k (Suc i) ≠ le_tm M))
∧ (pos k = 1
⟶ (∀i. i < 2 * card (UNIV :: 'c set)
⟶ tsM k (Suc i) ≠ le_tm M))
∧ (pos k ≥ 2
⟶ (∀i. i < 3 * card (UNIV :: 'c set)
⟶ tsM k
((pos k - 2) * card (UNIV :: 'c set)
+ 1 + i)
≠ le_tm M))"
and left_not_le_pos0:
"∀k<k_tm M. pos k = 0 ⟶ fst (buf_full k) ≠ LE_block (le_tm M)"
shows "∃buf' end_pos.
((qM, buf_full, λk. (AE_Home, ofs k)),
(mt_state cM_n, buf', end_pos))
∈ (m_step_buffered M) ^^ n
∧ (∀k<k_tm M. ae_window_invariant_general
(mt_tape cM_n k) (mt_pos cM_n k)
(end_pos k) (buf' k) (pos k) (le_tm M))
∧ (∀k. (pos k = 0
⟶ (∀i. i < card (UNIV :: 'c set)
⟶ mt_tape cM_n k (Suc i) ≠ le_tm M))
∧ (pos k = 1
⟶ (∀i. i < 2 * card (UNIV :: 'c set)
⟶ mt_tape cM_n k (Suc i) ≠ le_tm M))
∧ (pos k ≥ 2
⟶ (∀i. i < 3 * card (UNIV :: 'c set)
⟶ mt_tape cM_n k
((pos k - 2) * card (UNIV :: 'c set)
+ 1 + i)
≠ le_tm M)))
∧ (∀k<k_tm M. pos k = 0
⟶ fst (buf' k) ≠ LE_block (le_tm M))
∧ (∀k. card (UNIV :: 'c set) ≤ bp_linear (end_pos k) + n
∧ bp_linear (end_pos k)
< 2 * card (UNIV :: 'c set) + n)
∧ (∀k≥k_tm M. fst (snd (buf' k)) = bl_block (bl_tm M)
∧ end_pos k = (AE_Home, ofs k))"
using trace n_bound
proof (induction n arbitrary: cM_n)
case 0
from ‹(Config⇩M qM tsM nM, cM_n)
∈ mttm_step (delta_tm M) ^^ 0›
have cM_eq: "cM_n = Config⇩M qM tsM nM" by simp
hence st: "mt_state cM_n = qM"
and tp: "mt_tape cM_n = tsM"
and ps: "mt_pos cM_n = nM" by auto
show ?case
proof (intro exI [where x = buf_full]
exI [where x = "λk. (AE_Home, ofs k)"]
conjI)
show "((qM, buf_full, λk. (AE_Home, ofs k)),
(mt_state cM_n, buf_full, λk. (AE_Home, ofs k)))
∈ (m_step_buffered M) ^^ 0"
using st by simp
show "∀k<k_tm M. ae_window_invariant_general
(mt_tape cM_n k) (mt_pos cM_n k)
((λk. (AE_Home, ofs k)) k)
(buf_full k) (pos k) (le_tm M)"
using window tp ps by simp
show "∀k. (pos k = 0
⟶ (∀i. i < card (UNIV :: 'c set)
⟶ mt_tape cM_n k (Suc i) ≠ le_tm M))
∧ (pos k = 1
⟶ (∀i. i < 2 * card (UNIV :: 'c set)
⟶ mt_tape cM_n k (Suc i) ≠ le_tm M))
∧ (pos k ≥ 2
⟶ (∀i. i < 3 * card (UNIV :: 'c set)
⟶ mt_tape cM_n k
((pos k - 2) * card (UNIV :: 'c set)
+ 1 + i)
≠ le_tm M))"
using no_le tp by simp
show "∀k<k_tm M. pos k = 0
⟶ fst (buf_full k) ≠ LE_block (le_tm M)"
using left_not_le_pos0 .
show "∀k. card (UNIV :: 'c set)
≤ bp_linear ((λk. (AE_Home, ofs k)) k) + 0
∧ bp_linear ((λk. (AE_Home, ofs k)) k)
< 2 * card (UNIV :: 'c set) + 0"
proof (intro allI conjI)
fix k
have lin: "bp_linear ((λk. (AE_Home, ofs k)) k)
= card (UNIV :: 'c set) + c_idx (ofs k)"
unfolding bp_linear_def by simp
show "card (UNIV :: 'c set)
≤ bp_linear ((λk. (AE_Home, ofs k)) k) + 0"
using lin by simp
show "bp_linear ((λk. (AE_Home, ofs k)) k)
< 2 * card (UNIV :: 'c set) + 0"
using lin c_idx_lt_card[where x = "ofs k"] by simp
qed
show "∀k≥k_tm M. fst (snd (buf_full k)) = bl_block (bl_tm M)
∧ (λk. (AE_Home, ofs k)) k = (AE_Home, ofs k)"
using pad_home by simp
qed
next
case (Suc n')
have n'_bound: "n' ≤ card (UNIV :: 'c set)"
using Suc.prems(2) by simp
from Suc.prems(1) obtain cM_n' where
trace_n': "(Config⇩M qM tsM nM, cM_n')
∈ mttm_step (delta_tm M) ^^ n'"
and last_step: "(cM_n', cM_n) ∈ mttm_step (delta_tm M)"
by (rule relpow_Suc_E)
from Suc.IH[OF trace_n' n'_bound]
obtain buf_n' end_pos_n' where
coupled_n':
"((qM, buf_full, λk. (AE_Home, ofs k)),
(mt_state cM_n', buf_n', end_pos_n'))
∈ (m_step_buffered M) ^^ n'"
and window_n':
"∀k<k_tm M. ae_window_invariant_general
(mt_tape cM_n' k) (mt_pos cM_n' k)
(end_pos_n' k) (buf_n' k) (pos k) (le_tm M)"
and no_le_n':
"∀k. (pos k = 0
⟶ (∀i. i < card (UNIV :: 'c set)
⟶ mt_tape cM_n' k (Suc i)
≠ le_tm M))
∧ (pos k = 1
⟶ (∀i. i < 2 * card (UNIV :: 'c set)
⟶ mt_tape cM_n' k (Suc i)
≠ le_tm M))
∧ (pos k ≥ 2
⟶ (∀i. i < 3 * card (UNIV :: 'c set)
⟶ mt_tape cM_n' k
((pos k - 2)
* card (UNIV :: 'c set)
+ 1 + i)
≠ le_tm M))"
and left_n':
"∀k<k_tm M. pos k = 0
⟶ fst (buf_n' k) ≠ LE_block (le_tm M)"
and bp_bound_n':
"∀k. card (UNIV :: 'c set) ≤ bp_linear (end_pos_n' k) + n'
∧ bp_linear (end_pos_n' k)
< 2 * card (UNIV :: 'c set) + n'"
and pad_n':
"∀k≥k_tm M. fst (snd (buf_n' k)) = bl_block (bl_tm M)
∧ end_pos_n' k = (AE_Home, ofs k)"
by blast
from last_step obtain q_pre ts_pre n_pre q_post a_step dir_step where
cM_n'_eq: "cM_n' = Config⇩M q_pre ts_pre n_pre"
and cM_n_eq:
"cM_n = Config⇩M q_post
(λk. (ts_pre k)(n_pre k := a_step k))
(λk. go_dir (dir_step k) (n_pre k))"
and delta_mem:
"(q_pre, λk. ts_pre k (n_pre k),
q_post, a_step, dir_step) ∈ delta_tm M"
by (rule mttm_step.cases)
have st_n': "mt_state cM_n' = q_pre"
and tp_n': "mt_tape cM_n' = ts_pre"
and ps_n': "mt_pos cM_n' = n_pre"
using cM_n'_eq by auto
have st_n: "mt_state cM_n = q_post"
and tp_n: "∀k. mt_tape cM_n k
= (ts_pre k)(n_pre k := a_step k)"
and ps_n: "∀k. mt_pos cM_n k
= go_dir (dir_step k) (n_pre k)"
using cM_n_eq by auto
have read_match:
"∀k. read_bp (buf_n' k) (end_pos_n' k) = ts_pre k (n_pre k)"
proof (intro allI)
fix k
show "read_bp (buf_n' k) (end_pos_n' k) = ts_pre k (n_pre k)"
proof (cases "k < k_tm M")
case True
from window_n'[rule_format, OF True] have wi_k:
"ae_window_invariant_general
(mt_tape cM_n' k) (mt_pos cM_n' k)
(end_pos_n' k) (buf_n' k) (pos k) (le_tm M)" .
hence wi_k':
"ae_window_invariant_general
(ts_pre k) (n_pre k)
(end_pos_n' k) (buf_n' k) (pos k) (le_tm M)"
using tp_n' ps_n' by simp
show ?thesis
by (rule read_bp_via_window_general[OF wi_k'])
next
case False
hence kge: "k_tm M ≤ k" by simp
from pad_n'[rule_format, OF kge]
have ph: "fst (snd (buf_n' k)) = bl_block (bl_tm M)"
and ep: "end_pos_n' k = (AE_Home, ofs k)" by simp_all
have rd: "ts_pre k (n_pre k) = bl_tm M"
using valid_mttm_delta_support[OF vM delta_mem kge] by simp
obtain l h r where blk: "buf_n' k = (l, h, r)"
by (cases "buf_n' k") auto
from ph blk have h_eq: "h = bl_block (bl_tm M)" by simp
have "read_bp (buf_n' k) (end_pos_n' k) = bl_tm M"
using blk ep h_eq by (simp add: read_bp_def bl_block_def)
thus ?thesis using rd by simp
qed
qed
have c_pos: "1 ≤ card (UNIV :: 'c set)"
using Suc.prems(2) by linarith
have bp_lt_max:
"∀k. bp_linear (end_pos_n' k)
< 3 * card (UNIV :: 'c set) - 1"
proof (intro allI)
fix k
have lin_lt: "bp_linear (end_pos_n' k) < 2 * card (UNIV :: 'c set) + n'"
using bp_bound_n' by blast
show "bp_linear (end_pos_n' k) < 3 * card (UNIV :: 'c set) - 1"
using lin_lt Suc.prems(2) c_pos by linarith
qed
have bp_gt_zero:
"∀k. 0 < bp_linear (end_pos_n' k)"
proof (intro allI)
fix k
have low: "card (UNIV :: 'c set) ≤ bp_linear (end_pos_n' k) + n'"
using bp_bound_n' by blast
show "0 < bp_linear (end_pos_n' k)"
using low Suc.prems(2) c_pos by linarith
qed
have per_tape_total:
"∀k. ∃p'. bp_advance_le (le_tm M)
(ts_pre k (n_pre k))
(end_pos_n' k) (dir_step k)
= Some p'"
proof (intro allI)
fix k
show "∃p'. bp_advance_le (le_tm M)
(ts_pre k (n_pre k))
(end_pos_n' k) (dir_step k)
= Some p'"
by (rule bp_advance_le_total[OF bp_lt_max[rule_format]
bp_gt_zero[rule_format]])
qed
from per_tape_total
have "∃end_pos_n.
∀k. bp_advance_le (le_tm M)
(ts_pre k (n_pre k))
(end_pos_n' k) (dir_step k)
= Some (end_pos_n k)"
by (rule choice)
then obtain end_pos_n where
end_pos_n_eq:
"∀k. bp_advance_le (le_tm M)
(ts_pre k (n_pre k))
(end_pos_n' k) (dir_step k)
= Some (end_pos_n k)"
by blast
define buf_n where
"buf_n = (λk. write_bp (buf_n' k) (end_pos_n' k) (a_step k))"
have read_match_sym:
"∀k. ts_pre k (n_pre k) = read_bp (buf_n' k) (end_pos_n' k)"
using read_match by auto
have buf_n_def_forall:
"∀k. buf_n k = write_bp (buf_n' k) (end_pos_n' k) (a_step k)"
using buf_n_def by simp
have m_step_last:
"((q_pre, buf_n', end_pos_n'),
(q_post, buf_n, end_pos_n))
∈ m_step_buffered M"
by (rule m_step_bufferedI[OF delta_mem read_match_sym
buf_n_def_forall end_pos_n_eq])
have coupled_n_pre:
"((qM, buf_full, λk. (AE_Home, ofs k)),
(q_pre, buf_n', end_pos_n'))
∈ (m_step_buffered M) ^^ n'"
using coupled_n' st_n' by simp
have coupled_n:
"((qM, buf_full, λk. (AE_Home, ofs k)),
(q_post, buf_n, end_pos_n))
∈ (m_step_buffered M) ^^ Suc n'"
using coupled_n_pre m_step_last by (rule relpow_Suc_I)
have bp_bound_n:
"∀k. card (UNIV :: 'c set) ≤ bp_linear (end_pos_n k) + Suc n'
∧ bp_linear (end_pos_n k)
< 2 * card (UNIV :: 'c set) + Suc n'"
proof (intro allI)
fix k
show "card (UNIV :: 'c set) ≤ bp_linear (end_pos_n k) + Suc n'
∧ bp_linear (end_pos_n k)
< 2 * card (UNIV :: 'c set) + Suc n'"
by (rule bp_advance_le_lin_bounded
[OF end_pos_n_eq[rule_format, of k]
bp_gt_zero[rule_format, of k]
conjunct2[OF bp_bound_n'[rule_format, of k]]
conjunct1[OF bp_bound_n'[rule_format, of k]]])
qed
have left_n:
"∀k<k_tm M. pos k = 0
⟶ fst (buf_n k) ≠ LE_block (le_tm M)"
proof (intro allI impI)
fix k
assume klt: "k < k_tm M"
assume pos_0: "pos k = 0"
from window_n'[rule_format, OF klt] have wi_k:
"ae_window_invariant_general (mt_tape cM_n' k) (mt_pos cM_n' k)
(end_pos_n' k) (buf_n' k) (pos k) (le_tm M)" .
with pos_0 have wi_le0:
"ae_window_invariant_le0 (mt_tape cM_n' k) (mt_pos cM_n' k)
(end_pos_n' k) (buf_n' k) (le_tm M)"
unfolding ae_window_invariant_general_def by simp
have fst_bp_not_left: "fst (end_pos_n' k) ≠ AE_Left"
proof (rule ccontr)
assume "¬ fst (end_pos_n' k) ≠ AE_Left"
hence "fst (end_pos_n' k) = AE_Left" by simp
with wi_le0 show False
unfolding ae_window_invariant_le0_def by simp
qed
have fst_buf_n: "fst (buf_n k) = fst (buf_n' k)"
proof -
obtain l h r where blocks_eq: "buf_n' k = (l, h, r)"
by (cases "buf_n' k") auto
obtain b off where bp_eq: "end_pos_n' k = (b, off)"
by (cases "end_pos_n' k") auto
from fst_bp_not_left bp_eq have "b ≠ AE_Left" by simp
thus ?thesis
unfolding buf_n_def
using blocks_eq bp_eq
by (cases b) (auto simp: write_bp_def)
qed
have "fst (buf_n' k) ≠ LE_block (le_tm M)"
using left_n' pos_0 klt by blast
thus "fst (buf_n k) ≠ LE_block (le_tm M)"
using fst_buf_n by simp
qed
have coupled_chain:
"((qM, buf_full, λk. (AE_Home, ofs k)),
(mt_state cM_n, buf_n, end_pos_n))
∈ (m_step_buffered M) ^^ Suc n'"
using coupled_n st_n by simp
have no_le_contra:
"∀k. ts_pre k (n_pre k) ≠ le_tm M
⟶ a_step k ≠ le_tm M"
proof (intro allI impI)
fix k
assume rd_not_le: "ts_pre k (n_pre k) ≠ le_tm M"
show "a_step k ≠ le_tm M"
proof
assume a_le: "a_step k = le_tm M"
have "(λk. ts_pre k (n_pre k)) k = le_tm M"
by (rule valid_mttm_deltaLE_no_write[OF lu delta_mem a_le])
hence "ts_pre k (n_pre k) = le_tm M" by simp
with rd_not_le show False ..
qed
qed
have no_le0_n:
"∀k. pos k = 0
⟶ (∀i. i < card (UNIV :: 'c set)
⟶ mt_tape cM_n k (Suc i) ≠ le_tm M)"
proof (intro allI impI allI impI)
fix k i
assume pos_0: "pos k = 0"
and i_bd: "i < card (UNIV :: 'c set)"
have ih_at: "ts_pre k (Suc i) ≠ le_tm M"
proof -
from no_le_n' pos_0 i_bd
have "mt_tape cM_n' k (Suc i) ≠ le_tm M" by blast
thus ?thesis using tp_n' by simp
qed
show "mt_tape cM_n k (Suc i) ≠ le_tm M"
proof (cases "Suc i = n_pre k")
case False
hence "mt_tape cM_n k (Suc i) = ts_pre k (Suc i)"
using tp_n by simp
thus ?thesis using ih_at by simp
next
case True
hence tape_eq: "mt_tape cM_n k (Suc i) = a_step k"
using tp_n by simp
from True have "ts_pre k (n_pre k) = ts_pre k (Suc i)"
by simp
with ih_at have "ts_pre k (n_pre k) ≠ le_tm M" by simp
hence "a_step k ≠ le_tm M" using no_le_contra by blast
thus ?thesis using tape_eq by simp
qed
qed
have no_le1_n:
"∀k. pos k = 1
⟶ (∀i. i < 2 * card (UNIV :: 'c set)
⟶ mt_tape cM_n k (Suc i) ≠ le_tm M)"
proof (intro allI impI allI impI)
fix k i
assume pos_1: "pos k = 1"
and i_bd: "i < 2 * card (UNIV :: 'c set)"
have ih_at: "ts_pre k (Suc i) ≠ le_tm M"
proof -
from no_le_n' pos_1 i_bd
have "mt_tape cM_n' k (Suc i) ≠ le_tm M" by blast
thus ?thesis using tp_n' by simp
qed
show "mt_tape cM_n k (Suc i) ≠ le_tm M"
proof (cases "Suc i = n_pre k")
case False
hence "mt_tape cM_n k (Suc i) = ts_pre k (Suc i)"
using tp_n by simp
thus ?thesis using ih_at by simp
next
case True
hence tape_eq: "mt_tape cM_n k (Suc i) = a_step k"
using tp_n by simp
from True have "ts_pre k (n_pre k) = ts_pre k (Suc i)"
by simp
with ih_at have "ts_pre k (n_pre k) ≠ le_tm M" by simp
hence "a_step k ≠ le_tm M" using no_le_contra by blast
thus ?thesis using tape_eq by simp
qed
qed
have no_le2_n:
"∀k. pos k ≥ 2
⟶ (∀i. i < 3 * card (UNIV :: 'c set)
⟶ mt_tape cM_n k
((pos k - 2) * card (UNIV :: 'c set) + 1 + i)
≠ le_tm M)"
proof (intro allI impI allI impI)
fix k i
assume pos_ge: "pos k ≥ 2"
and i_bd: "i < 3 * card (UNIV :: 'c set)"
let ?j = "(pos k - 2) * card (UNIV :: 'c set) + 1 + i"
have ih_at: "ts_pre k ?j ≠ le_tm M"
proof -
from no_le_n' pos_ge i_bd
have "mt_tape cM_n' k ?j ≠ le_tm M" by blast
thus ?thesis using tp_n' by simp
qed
show "mt_tape cM_n k ?j ≠ le_tm M"
proof (cases "?j = n_pre k")
case False
hence "mt_tape cM_n k ?j = ts_pre k ?j"
using tp_n by simp
thus ?thesis using ih_at by simp
next
case True
hence tape_eq: "mt_tape cM_n k ?j = a_step k"
using tp_n by simp
from True have "ts_pre k (n_pre k) = ts_pre k ?j"
by simp
with ih_at have "ts_pre k (n_pre k) ≠ le_tm M" by simp
hence "a_step k ≠ le_tm M" using no_le_contra by blast
thus ?thesis using tape_eq by simp
qed
qed
have no_le_n:
"∀k. (pos k = 0
⟶ (∀i. i < card (UNIV :: 'c set)
⟶ mt_tape cM_n k (Suc i) ≠ le_tm M))
∧ (pos k = 1
⟶ (∀i. i < 2 * card (UNIV :: 'c set)
⟶ mt_tape cM_n k (Suc i) ≠ le_tm M))
∧ (pos k ≥ 2
⟶ (∀i. i < 3 * card (UNIV :: 'c set)
⟶ mt_tape cM_n k
((pos k - 2) * card (UNIV :: 'c set)
+ 1 + i)
≠ le_tm M))"
using no_le0_n no_le1_n no_le2_n by blast
have win2_n:
"∀k<k_tm M. pos k ≥ 2
⟶ ae_window_invariant
(mt_tape cM_n k) (mt_pos cM_n k)
(end_pos_n k) (buf_n k)
((pos k - 2) * card (UNIV :: 'c set) + 1)"
proof (intro allI impI)
fix k
assume klt: "k < k_tm M"
assume pos_ge: "pos k ≥ 2"
from window_n'[rule_format, OF klt] pos_ge have wi_k:
"ae_window_invariant (mt_tape cM_n' k) (mt_pos cM_n' k)
(end_pos_n' k) (buf_n' k)
((pos k - 2) * card (UNIV :: 'c set) + 1)"
unfolding ae_window_invariant_general_def by simp
hence wi_k': "ae_window_invariant (ts_pre k) (n_pre k)
(end_pos_n' k) (buf_n' k)
((pos k - 2) * card (UNIV :: 'c set) + 1)"
using tp_n' ps_n' by simp
have adv_k: "bp_advance_le (le_tm M) (ts_pre k (n_pre k))
(end_pos_n' k) (dir_step k) = Some (end_pos_n k)"
using end_pos_n_eq by blast
have bp_lt_k: "bp_linear (end_pos_n' k)
< 3 * card (UNIV :: 'c set) - 1"
using bp_lt_max by blast
have bp_pos_k: "0 < bp_linear (end_pos_n' k)"
using bp_gt_zero by blast
have no_le_k: "ts_pre k (n_pre k) ≠ le_tm M"
proof -
let ?j = "bp_linear (end_pos_n' k)"
from wi_k' have head_corr:
"n_pre k = (pos k - 2) * card (UNIV :: 'c set) + 1 + ?j"
unfolding ae_window_invariant_def by simp
have j_lt: "?j < 3 * card (UNIV :: 'c set)"
by (rule bp_linear_lt_3c)
from no_le_n' pos_ge j_lt have
"mt_tape cM_n' k
((pos k - 2) * card (UNIV :: 'c set) + 1 + ?j)
≠ le_tm M" by blast
hence "ts_pre k
((pos k - 2) * card (UNIV :: 'c set) + 1 + ?j)
≠ le_tm M" using tp_n' by simp
thus ?thesis using head_corr by simp
qed
have wi_step:
"ae_window_invariant
((ts_pre k)(n_pre k := a_step k))
(go_dir (dir_step k) (n_pre k))
(end_pos_n k)
(write_bp (buf_n' k) (end_pos_n' k) (a_step k))
((pos k - 2) * card (UNIV :: 'c set) + 1)"
by (rule ae_window_invariant_step
[OF wi_k' adv_k bp_lt_k bp_pos_k no_le_k])
show "ae_window_invariant
(mt_tape cM_n k) (mt_pos cM_n k)
(end_pos_n k) (buf_n k)
((pos k - 2) * card (UNIV :: 'c set) + 1)"
using wi_step tp_n ps_n buf_n_def by simp
qed
have win1_n:
"∀k<k_tm M. pos k = 1
⟶ ae_window_invariant_le1
(mt_tape cM_n k) (mt_pos cM_n k)
(end_pos_n k) (buf_n k) (le_tm M)"
proof (intro allI impI)
fix k
assume klt: "k < k_tm M"
assume pos_1: "pos k = 1"
from window_n'[rule_format, OF klt] pos_1 have wi_k:
"ae_window_invariant_le1 (mt_tape cM_n' k) (mt_pos cM_n' k)
(end_pos_n' k) (buf_n' k) (le_tm M)"
unfolding ae_window_invariant_general_def by simp
hence wi_k': "ae_window_invariant_le1 (ts_pre k) (n_pre k)
(end_pos_n' k) (buf_n' k) (le_tm M)"
using tp_n' ps_n' by simp
have adv_k: "bp_advance_le (le_tm M) (ts_pre k (n_pre k))
(end_pos_n' k) (dir_step k) = Some (end_pos_n k)"
using end_pos_n_eq by blast
have bp_lt_k: "bp_linear (end_pos_n' k)
< 3 * card (UNIV :: 'c set) - 1"
using bp_lt_max by blast
have bp_pos_k: "0 < bp_linear (end_pos_n' k)"
using bp_gt_zero by blast
have a_le_k:
"ts_pre k (n_pre k) = le_tm M
⟹ a_step k = le_tm M ∧ dir_step k ∈ {dir.N, dir.R}"
proof -
assume rd_le: "ts_pre k (n_pre k) = le_tm M"
have "a_step k = le_tm M ∧ dir_step k ∈ {dir.N, dir.R}"
by (rule valid_mttm_deltaLE[OF vM delta_mem, of k, OF rd_le])
thus "a_step k = le_tm M ∧ dir_step k ∈ {dir.N, dir.R}" .
qed
have a_not_le_k:
"ts_pre k (n_pre k) ≠ le_tm M ⟹ a_step k ≠ le_tm M"
using no_le_contra by blast
have no_le_win_k:
"∀i. 0 < i ∧ i ≤ 2 * card (UNIV :: 'c set)
⟶ ts_pre k i ≠ le_tm M"
proof (intro allI impI)
fix i
assume i_bd: "0 < i ∧ i ≤ 2 * card (UNIV :: 'c set)"
obtain j where j_eq: "i = Suc j" using i_bd by (cases i) auto
have j_lt: "j < 2 * card (UNIV :: 'c set)"
using i_bd j_eq by simp
from no_le_n' pos_1 j_lt
have "mt_tape cM_n' k (Suc j) ≠ le_tm M" by blast
thus "ts_pre k i ≠ le_tm M" using tp_n' j_eq by simp
qed
have wi_step:
"ae_window_invariant_le1
((ts_pre k)(n_pre k := a_step k))
(go_dir (dir_step k) (n_pre k))
(end_pos_n k)
(write_bp (buf_n' k) (end_pos_n' k) (a_step k))
(le_tm M)"
by (rule ae_window_invariant_le1_step
[OF wi_k' adv_k bp_lt_k bp_pos_k
a_le_k a_not_le_k no_le_win_k])
show "ae_window_invariant_le1
(mt_tape cM_n k) (mt_pos cM_n k)
(end_pos_n k) (buf_n k) (le_tm M)"
using wi_step tp_n ps_n buf_n_def by simp
qed
have win0_n:
"∀k<k_tm M. pos k = 0
⟶ ae_window_invariant_le0
(mt_tape cM_n k) (mt_pos cM_n k)
(end_pos_n k) (buf_n k) (le_tm M)"
proof (intro allI impI)
fix k
assume klt: "k < k_tm M"
assume pos_0: "pos k = 0"
from window_n'[rule_format, OF klt] pos_0 have wi_k:
"ae_window_invariant_le0 (mt_tape cM_n' k) (mt_pos cM_n' k)
(end_pos_n' k) (buf_n' k) (le_tm M)"
unfolding ae_window_invariant_general_def by simp
hence wi_k': "ae_window_invariant_le0 (ts_pre k) (n_pre k)
(end_pos_n' k) (buf_n' k) (le_tm M)"
using tp_n' ps_n' by simp
have adv_k: "bp_advance_le (le_tm M) (ts_pre k (n_pre k))
(end_pos_n' k) (dir_step k) = Some (end_pos_n k)"
using end_pos_n_eq by blast
have bp_lt_k: "bp_linear (end_pos_n' k)
< 3 * card (UNIV :: 'c set) - 1"
using bp_lt_max by blast
have bp_pos_k: "0 < bp_linear (end_pos_n' k)"
using bp_gt_zero by blast
have a_le_k:
"ts_pre k (n_pre k) = le_tm M
⟹ a_step k = le_tm M ∧ dir_step k ∈ {dir.N, dir.R}"
proof -
assume rd_le: "ts_pre k (n_pre k) = le_tm M"
show "a_step k = le_tm M ∧ dir_step k ∈ {dir.N, dir.R}"
by (rule valid_mttm_deltaLE[OF vM delta_mem, of k, OF rd_le])
qed
have a_not_le_k:
"ts_pre k (n_pre k) ≠ le_tm M ⟹ a_step k ≠ le_tm M"
using no_le_contra by blast
have no_le_win_k:
"∀i. 0 < i ∧ i ≤ card (UNIV :: 'c set)
⟶ ts_pre k i ≠ le_tm M"
proof (intro allI impI)
fix i
assume i_bd: "0 < i ∧ i ≤ card (UNIV :: 'c set)"
obtain j where j_eq: "i = Suc j" using i_bd by (cases i) auto
have j_lt: "j < card (UNIV :: 'c set)"
using i_bd j_eq by simp
from no_le_n' pos_0 j_lt
have "mt_tape cM_n' k (Suc j) ≠ le_tm M" by blast
thus "ts_pre k i ≠ le_tm M" using tp_n' j_eq by simp
qed
have wi_step:
"ae_window_invariant_le0
((ts_pre k)(n_pre k := a_step k))
(go_dir (dir_step k) (n_pre k))
(end_pos_n k)
(write_bp (buf_n' k) (end_pos_n' k) (a_step k))
(le_tm M)"
by (rule ae_window_invariant_le0_step
[OF wi_k' adv_k bp_lt_k bp_pos_k
a_le_k a_not_le_k no_le_win_k])
show "ae_window_invariant_le0
(mt_tape cM_n k) (mt_pos cM_n k)
(end_pos_n k) (buf_n k) (le_tm M)"
using wi_step tp_n ps_n buf_n_def by simp
qed
have window_n:
"∀k<k_tm M. ae_window_invariant_general
(mt_tape cM_n k) (mt_pos cM_n k)
(end_pos_n k) (buf_n k) (pos k) (le_tm M)"
proof (intro allI impI)
fix k
assume klt: "k < k_tm M"
show "ae_window_invariant_general
(mt_tape cM_n k) (mt_pos cM_n k)
(end_pos_n k) (buf_n k) (pos k) (le_tm M)"
unfolding ae_window_invariant_general_def
using win0_n win1_n win2_n klt by blast
qed
have pad_n:
"∀k≥k_tm M. fst (snd (buf_n k)) = bl_block (bl_tm M)
∧ end_pos_n k = (AE_Home, ofs k)"
proof (intro allI impI)
fix k
assume kge: "k_tm M ≤ k"
from pad_n'[rule_format, OF kge]
have ph: "fst (snd (buf_n' k)) = bl_block (bl_tm M)"
and ep: "end_pos_n' k = (AE_Home, ofs k)" by simp_all
from valid_mttm_delta_support[OF vM delta_mem kge]
have rd: "ts_pre k (n_pre k) = bl_tm M"
and wr: "a_step k = bl_tm M"
and dr: "dir_step k = dir.N" by simp_all
have ep_n: "end_pos_n k = (AE_Home, ofs k)"
proof -
have adv: "bp_advance_le (le_tm M) (ts_pre k (n_pre k))
(end_pos_n' k) (dir_step k) = Some (end_pos_n k)"
using end_pos_n_eq by blast
have "bp_advance_le (le_tm M) (bl_tm M) (AE_Home, ofs k) dir.N
= Some (AE_Home, ofs k)"
by (simp add: bp_advance_le_def bp_advance_def)
thus ?thesis using adv rd ep dr by simp
qed
have buf_n_k: "fst (snd (buf_n k)) = bl_block (bl_tm M)"
proof -
obtain l h r where blk: "buf_n' k = (l, h, r)"
by (cases "buf_n' k") auto
from ph blk have h_eq: "h = bl_block (bl_tm M)" by simp
have "buf_n k = (l, h(ofs k := bl_tm M), r)"
using blk ep wr by (simp add: buf_n_def write_bp_def)
hence "fst (snd (buf_n k)) = h(ofs k := bl_tm M)" by simp
also have "… = bl_block (bl_tm M)"
using h_eq by (simp add: bl_block_def fun_eq_iff)
finally show ?thesis .
qed
show "fst (snd (buf_n k)) = bl_block (bl_tm M)
∧ end_pos_n k = (AE_Home, ofs k)"
using buf_n_k ep_n by simp
qed
show ?case
proof (intro exI [where x = buf_n] exI [where x = end_pos_n] conjI)
show "((qM, buf_full, λk. (AE_Home, ofs k)),
(mt_state cM_n, buf_n, end_pos_n))
∈ (m_step_buffered M) ^^ Suc n'"
by (rule coupled_chain)
show "∀k<k_tm M. ae_window_invariant_general
(mt_tape cM_n k) (mt_pos cM_n k)
(end_pos_n k) (buf_n k) (pos k) (le_tm M)"
by (rule window_n)
show "∀k. (pos k = 0
⟶ (∀i. i < card (UNIV :: 'c set)
⟶ mt_tape cM_n k (Suc i) ≠ le_tm M))
∧ (pos k = 1
⟶ (∀i. i < 2 * card (UNIV :: 'c set)
⟶ mt_tape cM_n k (Suc i) ≠ le_tm M))
∧ (pos k ≥ 2
⟶ (∀i. i < 3 * card (UNIV :: 'c set)
⟶ mt_tape cM_n k
((pos k - 2) * card (UNIV :: 'c set)
+ 1 + i)
≠ le_tm M))"
by (rule no_le_n)
show "∀k<k_tm M. pos k = 0
⟶ fst (buf_n k) ≠ LE_block (le_tm M)"
by (rule left_n)
show "∀k. card (UNIV :: 'c set) ≤ bp_linear (end_pos_n k) + Suc n'
∧ bp_linear (end_pos_n k)
< 2 * card (UNIV :: 'c set) + Suc n'"
by (rule bp_bound_n)
show "∀k≥k_tm M. fst (snd (buf_n k)) = bl_block (bl_tm M)
∧ end_pos_n k = (AE_Home, ofs k)"
by (rule pad_n)
qed
qed
text ‹Per-tape unified companion of
‹ae_m_steps_buffered_correct_trace›, ‹_le0›, and
‹_le1›. A wrapper over
‹ae_coupled_run_aux_general›: builds the
‹m_steps_buffered› step (= relpow plus
‹kM ≤ c› and end-or-halt) and re-packages the aux's
existential into an ‹obtains›-style witness.
The hypothesis shape matches the three siblings' wrapper
pattern: a per-tape regime selector ‹pos›, the per-tape
hybrid window invariant, the per-tape regime-guarded
‹no_le›, and the ‹pos = 0›-conditional left-slot
guard. Output conjuncts mirror the input, with the buffered
config existentially bound.›
lemma ae_m_steps_buffered_correct_trace_general:
fixes M :: "('q, 'a) mttm"
and qM :: 'q
and tsM :: "nat ⇒ nat ⇒ 'a"
and nM :: "nat ⇒ nat"
and ofs :: "nat ⇒ ('c :: enum)"
and buf_full :: "nat ⇒ (('c ⇒ 'a) × ('c ⇒ 'a) × ('c ⇒ 'a))"
and pos :: "nat ⇒ nat"
and kM :: nat
and cM_k :: "('a, 'q) mt_config"
assumes vM: "valid_mttm M"
and lu: "le_unique M"
and qM_in: "qM ∈ Q_tm M"
and window: "∀k<k_tm M. ae_window_invariant_general (tsM k) (nM k)
(AE_Home, ofs k) (buf_full k) (pos k) (le_tm M)"
and pad_home: "∀k≥k_tm M. fst (snd (buf_full k)) = bl_block (bl_tm M)"
and no_le:
"∀k. (pos k = 0
⟶ (∀i. i < card (UNIV :: 'c set)
⟶ tsM k (Suc i) ≠ le_tm M))
∧ (pos k = 1
⟶ (∀i. i < 2 * card (UNIV :: 'c set)
⟶ tsM k (Suc i) ≠ le_tm M))
∧ (pos k ≥ 2
⟶ (∀i. i < 3 * card (UNIV :: 'c set)
⟶ tsM k
((pos k - 2) * card (UNIV :: 'c set)
+ 1 + i)
≠ le_tm M))"
and trace: "(Config⇩M qM tsM nM, cM_k)
∈ mttm_step (delta_tm M) ^^ kM"
and kM_le: "kM ≤ card (UNIV :: 'c set)"
and end_or_halt:
"kM = card (UNIV :: 'c set)
∨ mt_state cM_k ∈ {t_tm M, r_tm M}"
and left_not_le_pos0:
"∀k<k_tm M. pos k = 0 ⟶ fst (buf_full k) ≠ LE_block (le_tm M)"
obtains q_out buf' end_pos where
"((qM, buf_full, λk. (AE_Home, ofs k)),
(q_out, buf', end_pos)) ∈ m_steps_buffered M"
and "q_out = mt_state cM_k"
and "∀k<k_tm M. ae_window_invariant_general
(mt_tape cM_k k) (mt_pos cM_k k)
(end_pos k) (buf' k) (pos k) (le_tm M)"
and "∀k. (pos k = 0
⟶ (∀i. i < card (UNIV :: 'c set)
⟶ mt_tape cM_k k (Suc i) ≠ le_tm M))
∧ (pos k = 1
⟶ (∀i. i < 2 * card (UNIV :: 'c set)
⟶ mt_tape cM_k k (Suc i) ≠ le_tm M))
∧ (pos k ≥ 2
⟶ (∀i. i < 3 * card (UNIV :: 'c set)
⟶ mt_tape cM_k k
((pos k - 2) * card (UNIV :: 'c set)
+ 1 + i)
≠ le_tm M))"
and "∀k<k_tm M. pos k = 0
⟶ fst (buf' k) ≠ LE_block (le_tm M)"
proof -
have ae_result_general:
"∃buf' end_pos.
((qM, buf_full, λk. (AE_Home, ofs k)),
(mt_state cM_k, buf', end_pos))
∈ (m_step_buffered M) ^^ kM
∧ (∀k<k_tm M. ae_window_invariant_general
(mt_tape cM_k k) (mt_pos cM_k k)
(end_pos k) (buf' k) (pos k) (le_tm M))
∧ (∀k. (pos k = 0
⟶ (∀i. i < card (UNIV :: 'c set)
⟶ mt_tape cM_k k (Suc i) ≠ le_tm M))
∧ (pos k = 1
⟶ (∀i. i < 2 * card (UNIV :: 'c set)
⟶ mt_tape cM_k k (Suc i) ≠ le_tm M))
∧ (pos k ≥ 2
⟶ (∀i. i < 3 * card (UNIV :: 'c set)
⟶ mt_tape cM_k k
((pos k - 2) * card (UNIV :: 'c set)
+ 1 + i)
≠ le_tm M)))
∧ (∀k<k_tm M. pos k = 0
⟶ fst (buf' k) ≠ LE_block (le_tm M))
∧ (∀k. card (UNIV :: 'c set) ≤ bp_linear (end_pos k) + kM
∧ bp_linear (end_pos k)
< 2 * card (UNIV :: 'c set) + kM)
∧ (∀k≥k_tm M. fst (snd (buf' k)) = bl_block (bl_tm M)
∧ end_pos k = (AE_Home, ofs k))"
by (rule ae_coupled_run_aux_general[OF vM lu qM_in window pad_home trace kM_le
no_le left_not_le_pos0])
obtain buf' end_pos where
coupled: "((qM, buf_full, λk. (AE_Home, ofs k)),
(mt_state cM_k, buf', end_pos))
∈ (m_step_buffered M) ^^ kM"
and new_window:
"∀k<k_tm M. ae_window_invariant_general
(mt_tape cM_k k) (mt_pos cM_k k)
(end_pos k) (buf' k) (pos k) (le_tm M)"
and post_no_le:
"∀k. (pos k = 0
⟶ (∀i. i < card (UNIV :: 'c set)
⟶ mt_tape cM_k k (Suc i) ≠ le_tm M))
∧ (pos k = 1
⟶ (∀i. i < 2 * card (UNIV :: 'c set)
⟶ mt_tape cM_k k (Suc i) ≠ le_tm M))
∧ (pos k ≥ 2
⟶ (∀i. i < 3 * card (UNIV :: 'c set)
⟶ mt_tape cM_k k
((pos k - 2) * card (UNIV :: 'c set)
+ 1 + i)
≠ le_tm M))"
and post_left_not_le_pos0:
"∀k<k_tm M. pos k = 0
⟶ fst (buf' k) ≠ LE_block (le_tm M)"
and bp_bound:
"∀k. card (UNIV :: 'c set) ≤ bp_linear (end_pos k) + kM
∧ bp_linear (end_pos k)
< 2 * card (UNIV :: 'c set) + kM"
using ae_result_general by blast
have buffered_full:
"((qM, buf_full, λk. (AE_Home, ofs k)),
(mt_state cM_k, buf', end_pos)) ∈ m_steps_buffered M"
unfolding m_steps_buffered_def
using coupled kM_le end_or_halt by auto
show thesis
proof (rule that[where q_out = "mt_state cM_k"
and buf' = buf' and end_pos = end_pos])
show "((qM, buf_full, λk. (AE_Home, ofs k)),
(mt_state cM_k, buf', end_pos)) ∈ m_steps_buffered M"
using buffered_full .
show "mt_state cM_k = mt_state cM_k" by (rule refl)
show "∀k<k_tm M. ae_window_invariant_general
(mt_tape cM_k k) (mt_pos cM_k k)
(end_pos k) (buf' k) (pos k) (le_tm M)"
using new_window .
show "∀k. (pos k = 0
⟶ (∀i. i < card (UNIV :: 'c set)
⟶ mt_tape cM_k k (Suc i) ≠ le_tm M))
∧ (pos k = 1
⟶ (∀i. i < 2 * card (UNIV :: 'c set)
⟶ mt_tape cM_k k (Suc i) ≠ le_tm M))
∧ (pos k ≥ 2
⟶ (∀i. i < 3 * card (UNIV :: 'c set)
⟶ mt_tape cM_k k
((pos k - 2) * card (UNIV :: 'c set)
+ 1 + i)
≠ le_tm M))"
using post_no_le .
show "∀k<k_tm M. pos k = 0
⟶ fst (buf' k) ≠ LE_block (le_tm M)"
using post_left_not_le_pos0 .
qed
qed
end