Theory Multitape_Alphabet_Reduction.AlphabetReduction_Theorems
theory AlphabetReduction_Theorems
imports AlphabetReduction_Forward
begin
subsection ‹Top-level theorems›
text ‹Per-substep typing facts: for each substep relation in
the five-substep union, the source and target states' ‹'q›
components lie in ‹Q_tm M›, and the source's
‹ar_substep_idx› tag is the relation-specific value
(never ‹AR_HaltAccept› or ‹AR_HaltReject›).
Used by ‹alphabet_reduce_wf›'s ‹δ'›-typing
conjunct to show ‹δ'›-tuples land in
‹(Q' - ⦃t', r'⦄) × … × Q' × …›.›
lemma ar_delta_read_typing:
assumes "(s, a, s', a', d) ∈ ar_delta_read M"
shows "fst s ∈ Q_tm M ∧ fst (snd s) = AR_SimRead
∧ fst s' ∈ Q_tm M"
using assms
unfolding ar_delta_read_def
by (cases M) auto
lemma ar_delta_compute_typing:
assumes valM: "valid_mttm M"
and tr: "(s, a, s', a', d) ∈ ar_delta_compute M"
shows "fst s ∈ Q_tm M ∧ fst (snd s) = AR_SimCompute
∧ fst s' ∈ Q_tm M"
proof -
from tr obtain q buf q' m_a' m_d tk i dvec posk a'' d''
where decomp: "s = (q, AR_SimCompute, tk, i, buf, dvec, posk)"
and decomp': "s' = (q', AR_SimWrite, 0, 0, m_a', m_d, posk)"
and m_tr: "(q, buf, q', m_a', m_d) ∈ delta_tm M"
unfolding ar_delta_compute_def by auto
from valid_mttm_delta_set[OF valM] m_tr
have "q ∈ Q_tm M" and "q' ∈ Q_tm M" by auto
thus ?thesis using decomp decomp' by simp
qed
lemma ar_delta_write_typing:
assumes "(s, a, s', a', d) ∈ ar_delta_write M"
shows "fst s ∈ Q_tm M ∧ fst (snd s) = AR_SimWrite
∧ fst s' ∈ Q_tm M"
using assms
unfolding ar_delta_write_def
by (cases M) auto
lemma ar_delta_advance_typing:
assumes "(s, a, s', a', d) ∈ ar_delta_advance M"
shows "fst s ∈ Q_tm M ∧ fst (snd s) = AR_SimAdvance
∧ fst s' ∈ Q_tm M"
using assms
unfolding ar_delta_advance_def
by (cases M) auto
lemma ar_delta_next_typing:
assumes valM: "valid_mttm M"
and tr: "(s, a, s', a', d) ∈ ar_delta_next M"
shows "fst s ∈ Q_tm M ∧ fst (snd s) = AR_SimNext
∧ fst s' ∈ Q_tm M"
proof -
from valid_mttm_t_in_Q[OF valM] valid_mttm_r_in_Q[OF valM]
have "t_tm M ∈ Q_tm M" and "r_tm M ∈ Q_tm M" by auto
thus ?thesis
using tr
unfolding ar_delta_next_def
by (cases M) auto
qed
text ‹State-shape extraction for ‹alphabet_reduce_delta›: every
transition's source and target carry an ‹M›-state in ‹Q›,
and the source stage's index is a ∗‹simulation› index — never a
halt index — so the source state is distinct from both canonical halt
states. Case-split across the five substep relations (the delta is
their union intersected with global guards, so membership lands in the
union), each branch discharged by its typing lemma; the halt-index
distinctness is datatype-level.›
lemma alphabet_reduce_delta_state_shape:
assumes valM: "valid_mttm M"
and mem: "(s, a, s', a', d) ∈ alphabet_reduce_delta M"
shows "fst s ∈ Q_tm M ∧ fst s' ∈ Q_tm M
∧ fst (snd s) ≠ AR_HaltAccept
∧ fst (snd s) ≠ AR_HaltReject"
proof -
have memU: "(s, a, s', a', d)
∈ ar_delta_read M ∪ ar_delta_compute M
∪ ar_delta_write M ∪ ar_delta_advance M
∪ ar_delta_next M"
using mem unfolding alphabet_reduce_delta_def by blast
then show ?thesis
proof (elim UnE)
assume "(s, a, s', a', d) ∈ ar_delta_read M"
from ar_delta_read_typing[OF this] show ?thesis by auto
next
assume "(s, a, s', a', d) ∈ ar_delta_compute M"
from ar_delta_compute_typing[OF valM this] show ?thesis by auto
next
assume "(s, a, s', a', d) ∈ ar_delta_write M"
from ar_delta_write_typing[OF this] show ?thesis by auto
next
assume "(s, a, s', a', d) ∈ ar_delta_advance M"
from ar_delta_advance_typing[OF this] show ?thesis by auto
next
assume "(s, a, s', a', d) ∈ ar_delta_next M"
from ar_delta_next_typing[OF valM this] show ?thesis by auto
qed
qed
text ‹Output well-formedness: ‹alphabet_reduce› preserves the
substrate's wf predicate when the input tape alphabet has at
least 4 symbols. The reduced machine's tape alphabet is the whole
finite type ‹sym4›, so the read / write codomain conditions are
vacuous (‹UNIV›), and the ‹δLE›-preservation,
‹δLE›-no-write, and ‹δ›-support-past-tape-count
conjuncts are read straight off ‹alphabet_reduce_delta›'s three
intersection guards — no substep-builder unfold. The only structural
work is finite ‹Q'› (product of finite ‹Q› with the
bounded valid stages, ‹finite_ar_valid_stages›), the three
distinguished states landing in ‹Q'› (their stages are valid and
bounded), and the ‹δ›-shape's source / target state
membership (‹alphabet_reduce_delta_state_shape› plus the stage
guards).›
theorem alphabet_reduce_wf:
fixes M :: "('q, 'a) mttm"
assumes valM: "valid_mttm M"
and cardG: "card (Γ_tm M) ≥ 4"
shows "valid_mttm
(alphabet_reduce M
:: ('q × 'a ar_stage, sym4) mttm)"
proof -
obtain Q⇩M Σ⇩M Γ⇩M bl⇩M le⇩M δ⇩M s⇩M t⇩M r⇩M k⇩M where
M_eq: "M = MTTM Q⇩M Σ⇩M Γ⇩M bl⇩M le⇩M δ⇩M s⇩M t⇩M r⇩M k⇩M"
using mttm.exhaust by metis
have fin_Gamma: "finite Γ⇩M"
using valid_mttm_finite_Gamma[OF valM] M_eq by simp
have kpos: "0 < k⇩M"
using valid_mttm_k_pos[OF valM] M_eq by simp
have kfor1: "1 ≤ block_width Γ⇩M" by (rule block_width_pos)
have ar_eq: "(alphabet_reduce M :: ('q × 'a ar_stage, sym4) mttm) =
MTTM (Q⇩M × {stg. ar_valid_stage Γ⇩M bl⇩M stg
∧ ar_stage_bounded bl⇩M k⇩M stg})
{BIT0, BIT1}
(UNIV :: sym4 set)
BLANK4 LE4
(alphabet_reduce_delta M)
(s⇩M, ar_init_stage bl⇩M)
(t⇩M, ar_accept_stage bl⇩M)
(r⇩M, ar_reject_stage bl⇩M)
k⇩M"
unfolding M_eq alphabet_reduce_def by simp
have init_P: "ar_valid_stage Γ⇩M bl⇩M (ar_init_stage bl⇩M)
∧ ar_stage_bounded bl⇩M k⇩M (ar_init_stage bl⇩M)"
using kfor1 kpos
by (simp add: ar_valid_stage_def ar_stage_bounded_def ar_init_stage_def)
have acc_P: "ar_valid_stage Γ⇩M bl⇩M (ar_accept_stage bl⇩M)
∧ ar_stage_bounded bl⇩M k⇩M (ar_accept_stage bl⇩M)"
using kfor1 kpos
by (simp add: ar_valid_stage_def ar_stage_bounded_def ar_accept_stage_def)
have rej_P: "ar_valid_stage Γ⇩M bl⇩M (ar_reject_stage bl⇩M)
∧ ar_stage_bounded bl⇩M k⇩M (ar_reject_stage bl⇩M)"
using kfor1 kpos
by (simp add: ar_valid_stage_def ar_stage_bounded_def ar_reject_stage_def)
show "valid_mttm
(alphabet_reduce M :: ('q × 'a ar_stage, sym4) mttm)"
unfolding ar_eq valid_mttm.simps
proof (intro conjI)
show "finite (Q⇩M ×
({stg. ar_valid_stage Γ⇩M bl⇩M stg
∧ ar_stage_bounded bl⇩M k⇩M stg}
:: 'a ar_stage set))"
using valid_mttm_finite_Q[OF valM] M_eq
finite_ar_valid_stages[OF fin_Gamma]
by (auto intro: finite_cartesian_product)
show "finite (UNIV :: sym4 set)" by (simp add: sym4_UNIV)
show "{BIT0, BIT1} ⊆ (UNIV :: sym4 set)" by simp
show "(s⇩M, ar_init_stage bl⇩M)
∈ Q⇩M × {stg. ar_valid_stage Γ⇩M bl⇩M stg
∧ ar_stage_bounded bl⇩M k⇩M stg}"
using valid_mttm_s_in_Q[OF valM] M_eq init_P by simp
show "(t⇩M, ar_accept_stage bl⇩M)
∈ Q⇩M × {stg. ar_valid_stage Γ⇩M bl⇩M stg
∧ ar_stage_bounded bl⇩M k⇩M stg}"
using valid_mttm_t_in_Q[OF valM] M_eq acc_P by simp
show "(r⇩M, ar_reject_stage bl⇩M)
∈ Q⇩M × {stg. ar_valid_stage Γ⇩M bl⇩M stg
∧ ar_stage_bounded bl⇩M k⇩M stg}"
using valid_mttm_r_in_Q[OF valM] M_eq rej_P by simp
show "BLANK4 ∈ (UNIV :: sym4 set)" by simp
show "BLANK4 ∉ {BIT0, BIT1}" by simp
show "LE4 ∈ (UNIV :: sym4 set)" by simp
show "LE4 ∉ {BIT0, BIT1}" by simp
show "(t⇩M, ar_accept_stage bl⇩M) ≠ (r⇩M, ar_reject_stage bl⇩M)"
using valid_mttm_t_neq_r[OF valM] M_eq by simp
show "0 < k⇩M" using kpos .
show "alphabet_reduce_delta M
⊆ ((Q⇩M × {stg. ar_valid_stage Γ⇩M bl⇩M stg
∧ ar_stage_bounded bl⇩M k⇩M stg})
- {(t⇩M, ar_accept_stage bl⇩M),
(r⇩M, ar_reject_stage bl⇩M)})
× (UNIV → (UNIV :: sym4 set))
× (Q⇩M × {stg. ar_valid_stage Γ⇩M bl⇩M stg
∧ ar_stage_bounded bl⇩M k⇩M stg})
× (UNIV → (UNIV :: sym4 set))
× (UNIV → UNIV)"
proof (rule subsetI)
fix x assume xin: "x ∈ alphabet_reduce_delta M"
obtain s a s' a' d where x_eq: "x = (s, a, s', a', d)"
by (cases x) auto
from xin have mem_t: "(s, a, s', a', d) ∈ alphabet_reduce_delta M"
unfolding x_eq by simp
from mem_t have inter:
"ar_valid_stage (Γ_tm M) (bl_tm M) (snd s)
∧ ar_valid_stage (Γ_tm M) (bl_tm M) (snd s')
∧ ar_stage_bounded (bl_tm M) (k_tm M) (snd s)
∧ ar_stage_bounded (bl_tm M) (k_tm M) (snd s')"
unfolding alphabet_reduce_delta_def by simp
have shape: "fst s ∈ Q_tm M ∧ fst s' ∈ Q_tm M
∧ fst (snd s) ≠ AR_HaltAccept
∧ fst (snd s) ≠ AR_HaltReject"
by (rule alphabet_reduce_delta_state_shape[OF valM mem_t])
have s_in: "s ∈ (Q⇩M × {stg. ar_valid_stage Γ⇩M bl⇩M stg
∧ ar_stage_bounded bl⇩M k⇩M stg})
- {(t⇩M, ar_accept_stage bl⇩M),
(r⇩M, ar_reject_stage bl⇩M)}"
using shape inter M_eq
by (cases s) (auto simp: ar_accept_stage_def ar_reject_stage_def)
have s'_in: "s' ∈ Q⇩M × {stg. ar_valid_stage Γ⇩M bl⇩M stg
∧ ar_stage_bounded bl⇩M k⇩M stg}"
using shape inter M_eq by (cases s') auto
show "x ∈ ((Q⇩M × {stg. ar_valid_stage Γ⇩M bl⇩M stg
∧ ar_stage_bounded bl⇩M k⇩M stg})
- {(t⇩M, ar_accept_stage bl⇩M),
(r⇩M, ar_reject_stage bl⇩M)})
× (UNIV → (UNIV :: sym4 set))
× (Q⇩M × {stg. ar_valid_stage Γ⇩M bl⇩M stg
∧ ar_stage_bounded bl⇩M k⇩M stg})
× (UNIV → (UNIV :: sym4 set))
× (UNIV → UNIV)"
unfolding x_eq using s_in s'_in
by (auto simp: mem_Times_iff Pi_iff)
qed
show "∀q a q' a' d j.
(q, a, q', a', d) ∈ alphabet_reduce_delta M ⟶
a j = LE4 ⟶ a' j = LE4 ∧ d j ∈ {dir.N, dir.R}"
unfolding alphabet_reduce_delta_def by auto
show "∀q a q' a' d.
(q, a, q', a', d) ∈ alphabet_reduce_delta M ⟶
(∀j≥k⇩M. a j = BLANK4 ∧ a' j = BLANK4 ∧ d j = dir.N)"
unfolding alphabet_reduce_delta_def using M_eq by auto
qed
qed
text ‹The reduced machine is ∗‹le-unique› unconditionally: its
‹δ'› is intersected with the support filter
‹{(s, a, s', a', d). ∀k. a' k = LE4 ⟶ a k = LE4}›
(the ‹le_unique› clause, with ‹le_tm (alphabet_reduce M) =
LE4›), so every produced transition writes ‹LE4› only where it
read ‹LE4› — no hypothesis on ‹M› at all. This is the
output-side guarantee that makes ‹alphabet_reduce› a
∗‹cut-absorbing› normaliser: even a source machine that has
planted a fresh ‹le› (cut its tape) reduces to a machine whose
only ‹LE4› cell is the mandatory boundary.›
lemma alphabet_reduce_le_unique:
"le_unique (alphabet_reduce M)"
proof (unfold le_unique_def, intro allI impI)
fix q a q' a' d j
assume mem: "(q, a, q', a', d) ∈ delta_tm (alphabet_reduce M)"
and a'le: "a' j = le_tm (alphabet_reduce M)"
have "(q, a, q', a', d)
∈ {(s, a, s', a', d). ∀k. a' k = LE4 ⟶ a k = LE4}"
using mem unfolding alphabet_reduce_delta alphabet_reduce_delta_def by blast
hence allk: "∀k. a' k = LE4 ⟶ a k = LE4" by simp
from a'le have "a' j = LE4" by simp
with allk have "a j = LE4" by blast
thus "a j = le_tm (alphabet_reduce M)" by simp
qed
text ‹Output well-formedness, the strong form: ‹alphabet_reduce›
maps any valid ‹M› (with a ‹≥ 4›-symbol tape alphabet) to a
∗‹well-formed› machine — ‹valid_mttm› plus the three
non-degeneracy conditions plus ‹le_unique›. The
start-vs-halt-state distinctness is structural (the
‹AR_SimRead› init stage differs from the ‹AR_HaltAccept›
/ ‹AR_HaltReject› halt stages in its substep tag), so no
‹s ≠ t› hypothesis on ‹M› is needed. This is the
precondition the alphabet-enlargement combinator requires of its
input, so it is the bridge that lets ‹alphabet_reduce›'s output
feed ‹alphabet_enlarge› in a composition.›
theorem alphabet_reduce_well_formed:
fixes M :: "('q, 'a) mttm"
assumes valM: "valid_mttm M"
and cardG: "card (Γ_tm M) ≥ 4"
shows "well_formed_mttm
(alphabet_reduce M :: ('q × 'a ar_stage, sym4) mttm)"
proof -
have v: "valid_mttm (alphabet_reduce M)" by (rule alphabet_reduce_wf[OF valM cardG])
have lu: "le_unique (alphabet_reduce M)" by (rule alphabet_reduce_le_unique)
have st: "s_tm (alphabet_reduce M) ≠ t_tm (alphabet_reduce M)"
by (simp add: ar_init_stage_def ar_accept_stage_def)
have sr: "s_tm (alphabet_reduce M) ≠ r_tm (alphabet_reduce M)"
by (simp add: ar_init_stage_def ar_reject_stage_def)
have lebl: "le_tm (alphabet_reduce M) ≠ bl_tm (alphabet_reduce M)"
by simp
from v st sr lebl lu show ?thesis by blast
qed
text ‹Initial-configuration accessors, in terms of the machine's
structural projections. Generic (any ‹M›); they let the
init-correspondence proofs read the start tape / state / heads
without an inline ‹cases M›.›
lemma mt_tape_init_config:
"mt_tape (init_config_mttm M w)
= (λk n. if k < k_tm M
then (if n = 0 then le_tm M
else if k = 0 ∧ n ≤ length w then w ! (n - 1)
else bl_tm M)
else bl_tm M)"
proof (cases M)
case (MTTM Q Sg Gm bl le dl s tt rr kk)
then have lhs: "mt_tape (init_config_mttm M w)
= (λk n. if k < kk
then (if n = 0 then le
else if k = 0 ∧ n ≤ length w then w ! (n - 1)
else bl)
else bl)"
and le': "le_tm M = le" and bl': "bl_tm M = bl" and kk': "k_tm M = kk"
by simp_all
show ?thesis by (simp only: lhs le' bl' kk')
qed
lemma mt_state_init_config:
"mt_state (init_config_mttm M w) = s_tm M"
proof (cases M)
case (MTTM Q Sg Gm bl le dl s tt rr kk)
then have lhs: "mt_state (init_config_mttm M w) = s" and s': "s_tm M = s"
by simp_all
show ?thesis by (simp only: lhs s')
qed
lemma mt_pos_init_config:
"mt_pos (init_config_mttm M w) = (λ_. 0)"
by (cases M) simp
text ‹Specialised initial tape of the reduced machine: ‹LE4› at
position 0, the (already-encoded) input ‹w'› on tape 0, and
‹BLANK4› everywhere else. Stated with ‹w'› free and an
‹M›-free right-hand side, so it closes by the same
‹cases M›/‹alphabet_reduce_def› route as the structural
projections — sidestepping selector-reduction on ‹Γ_tm M›
etc.›
lemma mt_tape_init_config_ar:
"mt_tape (init_config_mttm (alphabet_reduce M) w')
= (λk n. if k < k_tm M
then (if n = 0 then LE4
else if k = 0 ∧ n ≤ length w' then w' ! (n - 1)
else BLANK4)
else BLANK4)"
by (cases M) (simp add: alphabet_reduce_def)
text ‹Initial-tape correspondence: at the start configuration the
encoded input ‹encode_input_ar Γ bl w› lays out, block by
block, exactly as ‹cell_repr› demands of M's initial tape.
The proper region (M-position ‹1 ≤ p ≤ |w|›) reads off
‹nth_encode_input_ar›; the blank tail (‹p > |w|›) and the
non-input tapes (‹k ≠ 0›) both reduce to the all-‹BLANK4›
block ‹cell_repr Γ bl bl›.›
lemma ar_tape_correspondence_init:
fixes M :: "('q, 'a) mttm"
assumes vM: "valid_mttm M"
and wS: "set w ⊆ Sigma_tm M"
and kK: "k < k_tm M"
shows "ar_tape_correspondence (Γ_tm M) (le_tm M) (bl_tm M)
(mt_tape (init_config_mttm M w) k)
(mt_tape (init_config_mttm (alphabet_reduce M)
(encode_input_ar (Γ_tm M) (bl_tm M) w)) k)"
(is "ar_tape_correspondence ?G ?le ?bl ?tM ?tM'")
proof -
let ?K = "block_width ?G"
let ?w' = "encode_input_ar ?G ?bl w"
have len_w': "length ?w' = ?K * length w" by (rule length_encode_input_ar)
have bl_notin: "?bl ∉ Sigma_tm M" using vM by (cases M) auto
have tM_eq: "?tM = (λn. if n = 0 then ?le
else if k = 0 ∧ n ≤ length w then w ! (n - 1)
else ?bl)"
by (simp add: mt_tape_init_config kK)
have tM'_eq: "?tM' = (λn. if n = 0 then LE4
else if k = 0 ∧ n ≤ length ?w' then ?w' ! (n - 1)
else BLANK4)"
by (simp add: mt_tape_init_config_ar kK)
have blank_repr: "cell_repr ?G ?bl ?bl ! j = BLANK4" if "j < ?K" for j
using that by (simp add: cell_repr_def)
show ?thesis
unfolding ar_tape_correspondence_def
proof (intro conjI)
show "?tM 0 = ?le" by (simp add: tM_eq)
next
show "?tM' 0 = LE4" by (simp add: tM'_eq)
next
show "∀p. 1 ≤ p ⟶ (∀j. j < ?K ⟶
?tM' (sim_pos ?K p + j) = cell_repr ?G ?bl (?tM p) ! j)"
proof (intro allI impI)
fix p j :: nat
assume p1: "1 ≤ p" and jK: "j < ?K"
obtain p0 where p_eq: "p = Suc p0" using p1 by (cases p) auto
have sp: "sim_pos ?K p = p0 * ?K + 1"
by (simp add: p_eq sim_pos_def)
have q_ge1: "1 ≤ sim_pos ?K p + j" using sp by simp
have sppos: "0 < sim_pos ?K p" using sp by simp
show "?tM' (sim_pos ?K p + j) = cell_repr ?G ?bl (?tM p) ! j"
proof (cases "k = 0")
case False
have "?tM p = ?bl" using False p1 by (simp add: tM_eq)
moreover have "?tM' (sim_pos ?K p + j) = BLANK4"
using False sppos by (simp add: tM'_eq)
ultimately show ?thesis using blank_repr[OF jK] by simp
next
case True
note k0 = True
show ?thesis
proof (cases "p ≤ length w")
case True
note pw = True
have p0w: "p0 < length w" using pw p_eq by simp
have neq: "w ! p0 ≠ ?bl"
proof -
have "w ! p0 ∈ set w" using p0w by simp
hence "w ! p0 ∈ Sigma_tm M" using wS by blast
thus ?thesis using bl_notin by auto
qed
have qle: "sim_pos ?K p + j ≤ length ?w'"
proof -
have "sim_pos ?K p + j = p0 * ?K + 1 + j" using sp by simp
also have "… ≤ p0 * ?K + ?K" using jK by linarith
also have "… = Suc p0 * ?K" by (simp add: mult_Suc)
also have "… ≤ length w * ?K"
using Suc_leI[OF p0w] by (rule mult_le_mono1)
also have "… = length ?w'" using len_w' by (simp add: mult.commute)
finally show ?thesis .
qed
have lhs: "?tM' (sim_pos ?K p + j) = encode_symbol ?G ?bl (w ! p0) ! j"
proof -
have idx: "sim_pos ?K p + j - 1 = p0 * ?K + j" using sp by simp
have "?tM' (sim_pos ?K p + j) = ?w' ! (sim_pos ?K p + j - 1)"
unfolding tM'_eq using k0 sppos qle by simp
also have "… = ?w' ! (p0 * ?K + j)" using idx by simp
also have "… = encode_symbol ?G ?bl (w ! p0) ! j"
using p0w jK by (simp add: nth_encode_input_ar)
finally show ?thesis .
qed
have rhs: "cell_repr ?G ?bl (?tM p) ! j = encode_symbol ?G ?bl (w ! p0) ! j"
proof -
have "?tM p = w ! p0" unfolding tM_eq using k0 pw p_eq by simp
thus ?thesis using neq by (simp add: cell_repr_def)
qed
show ?thesis using lhs rhs by simp
next
case False
note pw = False
have lwle: "length w ≤ p0" using pw p_eq by simp
have "?tM p = ?bl" unfolding tM_eq using k0 pw p_eq by simp
hence rhs: "cell_repr ?G ?bl (?tM p) ! j = BLANK4"
using blank_repr[OF jK] by simp
have qgt: "length ?w' < sim_pos ?K p + j"
proof -
have a: "length w * ?K ≤ p0 * ?K" using lwle by (rule mult_le_mono1)
have b: "sim_pos ?K p + j = p0 * ?K + 1 + j" using sp by simp
have c: "length ?w' = length w * ?K" using len_w' by (simp add: mult.commute)
show ?thesis using a b c by linarith
qed
have "?tM' (sim_pos ?K p + j) = BLANK4"
unfolding tM'_eq using k0 sppos qgt by simp
thus ?thesis using rhs by simp
qed
qed
qed
qed
qed
text ‹The three simulation invariants at the start configuration —
the entry premises the chunked engine ‹ar_simulation_phase_chunked›
consumes. ‹ar_simulates_init› carries the weight (its
‹AR_SimRead› arm needs ‹s ≠ t›, ‹s ≠ r›
from ‹valid_mttm›, and its tape clause is
‹ar_tape_correspondence_init›); the other two read straight
off ‹ar_init_stage›.›
lemma ar_simulates_init:
fixes M :: "('q, 'a) mttm"
assumes vM: "valid_mttm M"
and wS: "set w ⊆ Sigma_tm M"
and snt: "s_tm M ≠ t_tm M"
and snr: "s_tm M ≠ r_tm M"
shows "ar_simulates M (init_config_mttm M w)
(init_config_mttm (alphabet_reduce M)
(encode_input_ar (Γ_tm M) (bl_tm M) w))"
proof -
let ?cM = "init_config_mttm M w"
let ?c' = "init_config_mttm (alphabet_reduce M)
(encode_input_ar (Γ_tm M) (bl_tm M) w)"
have st: "mt_state ?c' = (s_tm M, ar_init_stage (bl_tm M))"
by (simp add: mt_state_init_config)
have stM: "mt_state ?cM = s_tm M" by (simp add: mt_state_init_config)
have tc: "∀k < k_tm M. ar_tape_correspondence (Γ_tm M) (le_tm M) (bl_tm M)
(mt_tape ?cM k) (mt_tape ?c' k)"
using ar_tape_correspondence_init[OF vM wS] by blast
have posM: "mt_pos ?cM = (λ_. 0)" and pos': "mt_pos ?c' = (λ_. 0)"
by (simp_all add: mt_pos_init_config)
show ?thesis
unfolding ar_simulates_def Let_def
by (simp add: st stM tc posM pos' ar_init_stage_def sim_pos_def snt snr)
qed
lemma ar_posk_consistent_init:
shows "ar_posk_consistent M (init_config_mttm M w)
(init_config_mttm (alphabet_reduce M)
(encode_input_ar (Γ_tm M) (bl_tm M) w))"
unfolding ar_posk_consistent_def
by (simp add: mt_state_init_config mt_pos_init_config ar_init_stage_def)
lemma ar_at_read_boundary_init:
assumes vM: "valid_mttm M"
shows "ar_at_read_boundary M
(init_config_mttm (alphabet_reduce M)
(encode_input_ar (Γ_tm M) (bl_tm M) w))"
proof -
let ?M' = "alphabet_reduce M"
let ?c' = "init_config_mttm ?M' (encode_input_ar (Γ_tm M) (bl_tm M) w)"
have kpos: "0 < k_tm M" using vM by (cases M) auto
have pad: "∀j ≥ k_tm M. mt_tape ?c' j (mt_pos ?c' j) = BLANK4"
by (cases M) (auto simp: alphabet_reduce_def)
show ?thesis
unfolding ar_at_read_boundary_def
using pad kpos
by (simp add: mt_state_init_config ar_init_stage_def ar_stage_bounded_def)
qed
text ‹The encoded input is a ‹BIT0›/‹BIT1› string,
unconditionally: every block is ‹encode_symbol›'s image,
whose cells lie in ‹⦃BIT0, BIT1⦄› by
‹encode_symbol_cell_domain› — so this needs no
‹set w ⊆ Σ› hypothesis. It discharges the
set-containment side of ‹Lang_mttm (alphabet_reduce M)›
membership.›
lemma set_encode_input_ar:
"set (encode_input_ar Γ bl w) ⊆ {BIT0, BIT1}"
proof (induct w)
case Nil thus ?case by simp
next
case (Cons x xs)
have "encode_input_ar Γ bl (x # xs)
= encode_symbol Γ bl x @ encode_input_ar Γ bl xs"
by (simp add: encode_input_ar_def)
thus ?case using Cons.hyps encode_symbol_cell_domain[of Γ bl x] by auto
qed
text ‹Forward language preservation: an accepting ‹M›-run on
‹w› lifts to an accepting ‹M'›-run on the encoded
input, via the chunked engine off the initial correspondence.
This is the forward half of ‹alphabet_reduce_language›;
it mirrors ‹alphabet_enlarge_language_forward›. The reverse
half, and the full biconditional ‹alphabet_reduce_language›,
live in ‹AlphabetReduction_Reverse.thy› (which imports this
theory), supplied by the chunked-reverse engine
‹ar_simulation_phase_chunked_reverse›.›
theorem alphabet_reduce_language_forward:
fixes M :: "('q, 'a) mttm"
assumes vM: "valid_mttm M"
and s_neq_t: "s_tm M ≠ t_tm M"
and s_neq_r: "s_tm M ≠ r_tm M"
and le_neq_bl: "le_tm M ≠ bl_tm M"
and card_ge: "card (Γ_tm M) ≥ 4"
shows "∀w. set w ⊆ Sigma_tm M ⟶ w ∈ Lang_mttm M
⟶ encode_input_ar (Γ_tm M) (bl_tm M) w
∈ Lang_mttm (alphabet_reduce M
:: ('q × 'a ar_stage, sym4) mttm)"
proof -
let ?M' = "alphabet_reduce M :: ('q × 'a ar_stage, sym4) mttm"
show ?thesis
proof (intro allI impI)
fix w :: "'a list"
assume w_sub: "set w ⊆ Sigma_tm M"
assume w_in: "w ∈ Lang_mttm M"
from w_in obtain w' nw where
run_star: "(init_config_mttm M w, Config⇩M (t_tm M) w' nw)
∈ (mttm_step (delta_tm M))⇧*"
unfolding Lang_mttm_def by blast
then obtain nn where
trace: "(init_config_mttm M w, Config⇩M (t_tm M) w' nw)
∈ (mttm_step (delta_tm M)) ^^ nn"
using rtrancl_imp_relpow by blast
let ?c' = "init_config_mttm ?M' (encode_input_ar (Γ_tm M) (bl_tm M) w)"
have reach0: "(init_config_mttm M w, init_config_mttm M w)
∈ (mttm_step (delta_tm M))⇧*" by blast
have accf: "mt_state (Config⇩M (t_tm M) w' nw) = t_tm M" by simp
have sim: "ar_simulates M (init_config_mttm M w) ?c'"
by (rule ar_simulates_init[OF vM w_sub s_neq_t s_neq_r])
have posk: "ar_posk_consistent M (init_config_mttm M w) ?c'"
by (rule ar_posk_consistent_init)
have rbnd: "ar_at_read_boundary M ?c'"
by (rule ar_at_read_boundary_init[OF vM])
obtain m c'' where
run: "(?c', c'') ∈ (mttm_step (alphabet_reduce_delta M)) ^^ m"
and st'': "mt_state c'' = (t_tm M, ar_accept_stage (bl_tm M))"
using ar_simulation_phase_chunked
[OF vM w_sub card_ge reach0 trace accf sim posk rbnd le_neq_bl]
by blast
have st2: "mt_state c'' = t_tm ?M'" using st'' by simp
obtain wM' nM' where c''_eq: "c'' = Config⇩M (t_tm ?M') wM' nM'"
using st2 by (cases c'') simp
have run': "(?c', c'') ∈ (mttm_step (delta_tm ?M')) ^^ m"
using run by simp
have run_star': "(?c', Config⇩M (t_tm ?M') wM' nM')
∈ (mttm_step (delta_tm ?M'))⇧*"
using run' c''_eq relpow_imp_rtrancl by metis
have enc_sub: "set (encode_input_ar (Γ_tm M) (bl_tm M) w)
⊆ Sigma_tm ?M'"
using set_encode_input_ar by simp
show "encode_input_ar (Γ_tm M) (bl_tm M) w ∈ Lang_mttm ?M'"
unfolding Lang_mttm_def using enc_sub run_star' by blast
qed
qed
text ‹The per-‹M›-step super-step count ‹C ⋅ (5 ⋅ k + 2) + 2›
(‹C = k_tm M›, ‹k = b = block_width›) folds into one ‹b›-factor
‹(6 ⋅ C + 1) ⋅ k›. The slack is ‹(C + 1) ⋅ (k - 2) ≥ 0›, tight at
‹k = 2› --- so ‹6 ⋅ C + 1› is the least factor that absorbs the count
for every ‹k ≥ 2›. The reduction always encodes into blocks of width
‹≥ 2› (from ‹card Γ_M ≥ 4›), so the ‹b ≥ 2› precondition is always
met; the looser ‹b ≥ 1› fold to ‹7 ⋅ C + 2› is unnecessary.›
lemma ar_time_bound_arith_sharp:
fixes C k :: nat
assumes "2 ≤ k"
shows "C * (5 * k + 2) + 2 ≤ (6 * C + 1) * k"
proof -
obtain k0 where k: "k = 2 + k0" using le_Suc_ex[OF assms] by blast
have "(6 * C + 1) * k = C * (5 * k + 2) + 2 + (C + 1) * k0"
by (simp add: k algebra_simps)
thus ?thesis by linarith
qed
text ‹Time bound under weak time-bounded acceptance, with explicit
constants. If ‹M› accepts ‹w› within ‹T(|w|)› steps, the output
machine accepts the encoded input within
‹(6 ⋅ k_tm M + 1) ⋅ b ⋅ T(|w|)› steps, where
‹b = block_width (Γ_tm M)› is the per-symbol block length (in
‹sym4› cells) and ‹k_tm M› is
the tape count. The exact per-‹M›-step super-step count is
‹k_tm M ⋅ (5 ⋅ b + 2) + 2›, folded up to ‹(6 ⋅ k_tm M + 1) ⋅ b› using
‹b ≥ 2› (‹ar_time_bound_arith_sharp›; ‹b ≥ 2› holds because
‹card (Γ_tm M) ≥ 4›, and the factor is tight at ‹b = 2›, i.e.\
‹card (Γ_tm M) = 4›); the linear-in-‹|w|› coefficient and the
additive constant are both ‹0›. ‹b› is logarithmic in the
source-alphabet cardinality ‹card (Γ_tm M)› (the binary-encoding design
point) --- a ∗‹ceiling› log, so the slowdown factor is a step
function of ‹card (Γ_tm M)› that jumps by one at each power of two
(the band ‹2 ^ (b - 1) < card (Γ_tm M) ≤ 2 ^ b› is pinned by
‹card_le_two_pow_block_width› and ‹two_pow_block_width_pred_less_card›).
The count is the whole alphabet, blank included at index ‹0› (the
endmarker ‹le› is a genuinely coded symbol, so it too is counted); so
‹b› is the uniform-code width, one cell above the coding minimum
‹⌈log⇩2 (card (Γ_tm M) - 1)⌉› just past a power of two
--- see ‹block_width›.
Weak acceptance, not the strong all-paths ‹upperb_time_mttm›, is
the target: the strong bound is unprovable for the no-validation
construction, and weak acceptance serves both the DTM and NDTM
applications. Mirrors ‹alphabet_enlarge_time_explicit›. The classical
existential form is the ‹obtains›-corollary ‹alphabet_reduce_time› below.›
theorem alphabet_reduce_time_explicit:
fixes M :: "('q, 'a) mttm"
and T :: "nat ⇒ nat"
assumes vM: "valid_mttm M"
and s_neq_t: "s_tm M ≠ t_tm M"
and s_neq_r: "s_tm M ≠ r_tm M"
and le_neq_bl: "le_tm M ≠ bl_tm M"
and card_ge: "card (Γ_tm M) ≥ 4"
shows "∀w. set w ⊆ Sigma_tm M
⟶ accepts_in_time_mttm M w (T (length w))
⟶ accepts_in_time_mttm
(alphabet_reduce M
:: ('q × 'a ar_stage, sym4) mttm)
(encode_input_ar (Γ_tm M) (bl_tm M) w)
((6 * k_tm M + 1) * block_width (Γ_tm M) * T (length w))"
proof -
let ?C = "k_tm M"
let ?k = "block_width (Γ_tm M)"
let ?M' = "alphabet_reduce M :: ('q × 'a ar_stage, sym4) mttm"
let ?d = "6 * ?C + 1"
have kge2: "2 ≤ ?k"
proof -
have "(2::nat) ^ 2 ≤ 2 ^ ?k"
using card_ge card_le_two_pow_block_width[of "Γ_tm M"] by simp
thus "2 ≤ ?k" using power_le_imp_le_exp[of "2::nat" 2 ?k] by simp
qed
have bnd: "?C * (5 * ?k + 2) + 2 ≤ ?d * ?k"
by (rule ar_time_bound_arith_sharp[OF kge2])
show "∀w. set w ⊆ Sigma_tm M
⟶ accepts_in_time_mttm M w (T (length w))
⟶ accepts_in_time_mttm ?M'
(encode_input_ar (Γ_tm M) (bl_tm M) w)
(?d * ?k * T (length w))"
proof (intro allI impI)
fix w :: "'a list"
assume w_sub: "set w ⊆ Sigma_tm M"
assume m_acc: "accepts_in_time_mttm M w (T (length w))"
from m_acc obtain n_T cMf where
nT_le: "n_T ≤ T (length w)"
and trace: "(init_config_mttm M w, cMf)
∈ (mttm_step (delta_tm M)) ^^ n_T"
and accf: "mt_state cMf = t_tm M"
unfolding accepts_in_time_mttm_def by blast
let ?c' = "init_config_mttm ?M' (encode_input_ar (Γ_tm M) (bl_tm M) w)"
have reach0: "(init_config_mttm M w, init_config_mttm M w)
∈ (mttm_step (delta_tm M))⇧*" by blast
have sim: "ar_simulates M (init_config_mttm M w) ?c'"
by (rule ar_simulates_init[OF vM w_sub s_neq_t s_neq_r])
have posk: "ar_posk_consistent M (init_config_mttm M w) ?c'"
by (rule ar_posk_consistent_init)
have rbnd: "ar_at_read_boundary M ?c'"
by (rule ar_at_read_boundary_init[OF vM])
obtain m c'' where
m_le: "m ≤ (?C * (5 * ?k + 2) + 2) * n_T"
and run: "(?c', c'') ∈ (mttm_step (alphabet_reduce_delta M)) ^^ m"
and st'': "mt_state c'' = (t_tm M, ar_accept_stage (bl_tm M))"
using ar_simulation_phase_chunked
[OF vM w_sub card_ge reach0 trace accf sim posk rbnd le_neq_bl]
by blast
have m_bound: "m ≤ ?d * ?k * T (length w)"
proof -
have "m ≤ (?C * (5 * ?k + 2) + 2) * n_T" by (rule m_le)
also have "… ≤ (?d * ?k) * n_T" using bnd by (rule mult_le_mono1)
also have "… ≤ (?d * ?k) * T (length w)"
using nT_le by (rule mult_le_mono2)
finally show ?thesis by (simp add: mult.assoc)
qed
have run': "(?c', c'') ∈ (mttm_step (delta_tm ?M')) ^^ m"
using run by simp
have st''': "mt_state c'' = t_tm ?M'" using st'' by simp
show "accepts_in_time_mttm ?M'
(encode_input_ar (Γ_tm M) (bl_tm M) w)
(?d * ?k * T (length w))"
unfolding accepts_in_time_mttm_def
using m_bound run' st''' by blast
qed
qed
text ‹Linear-time slowdown, classical existential form: reducing the tape
alphabet to the fixed type ‹sym4› multiplies the running time by only a
constant times the per-symbol block width. The ‹obtains›-corollary of
‹alphabet_reduce_time_explicit› above, hiding its four explicit constants
behind existentials instantiated at ‹d = 6 ⋅ k_tm M + 1›,
‹e = f = 0›, and ‹b = block_width (Γ_tm M)›.›
theorem alphabet_reduce_time:
fixes M :: "('q, 'a) mttm"
and T :: "nat ⇒ nat"
assumes vM: "valid_mttm M"
and s_neq_t: "s_tm M ≠ t_tm M"
and s_neq_r: "s_tm M ≠ r_tm M"
and le_neq_bl: "le_tm M ≠ bl_tm M"
and card_ge: "card (Γ_tm M) ≥ 4"
obtains d e f b :: nat
where "b ≥ 1"
and "∀w. set w ⊆ Sigma_tm M
⟶ accepts_in_time_mttm M w (T (length w))
⟶ accepts_in_time_mttm
(alphabet_reduce M
:: ('q × 'a ar_stage, sym4) mttm)
(encode_input_ar (Γ_tm M) (bl_tm M) w)
(d * b * T (length w) + e * b * length w + f)"
proof -
have P: "∀w. set w ⊆ Sigma_tm M
⟶ accepts_in_time_mttm M w (T (length w))
⟶ accepts_in_time_mttm
(alphabet_reduce M
:: ('q × 'a ar_stage, sym4) mttm)
(encode_input_ar (Γ_tm M) (bl_tm M) w)
((6 * k_tm M + 1) * block_width (Γ_tm M) * T (length w)
+ 0 * block_width (Γ_tm M) * length w + 0)"
using alphabet_reduce_time_explicit[OF vM s_neq_t s_neq_r le_neq_bl card_ge]
by simp
show ?thesis
proof (rule that)
show "(block_width (Γ_tm M) :: nat) ≥ 1" by (rule block_width_pos)
next
show "∀w. set w ⊆ Sigma_tm M
⟶ accepts_in_time_mttm M w (T (length w))
⟶ accepts_in_time_mttm
(alphabet_reduce M
:: ('q × 'a ar_stage, sym4) mttm)
(encode_input_ar (Γ_tm M) (bl_tm M) w)
((6 * k_tm M + 1) * block_width (Γ_tm M) * T (length w)
+ 0 * block_width (Γ_tm M) * length w + 0)"
by (rule P)
qed
qed
text ‹Output alphabet: the reduced machine's tape alphabet is the
whole finite type ‹sym4›, of cardinality exactly four.›
theorem alphabet_reduce_produces_alphabet_size_4:
shows "card (UNIV :: sym4 set) = 4"
by (rule sym4_card)
text ‹Tape-count preservation: the reduction re-encodes the tape
alphabet symbol by symbol without changing the number of tapes, so
the reduced machine has exactly ‹M›'s tape count. This is the
formal counterpart of the headline ``tape count preserved'', and the
point of contrast with a tape-∗‹count› reduction such as
Book--Greibach--Wegbreit.›
theorem alphabet_reduce_preserves_tape_count:
fixes M :: "('q, 'a) mttm"
shows "k_tm (alphabet_reduce M :: ('q × 'a ar_stage, sym4) mttm)
= k_tm M"
by (cases M) (simp add: alphabet_reduce_def)
end