Theory AlphabetRoundtrip
theory AlphabetRoundtrip
imports
"Multitape_Alphabet_Enlargement.AlphabetEnlargement_Reverse"
"Multitape_Alphabet_Reduction.AlphabetReduction_Reverse"
begin
section ‹Round-trip composition of the alphabet transformations›
text ‹The two alphabet transformations compose ∗‹as machines› in both
orders on the shared substrate. This theory states, for each order,
language preservation and a composed linear-time slowdown bound. Nothing
is re-proved: each headline chains the language / time theorems of
\<^const>‹alphabet_enlarge› and \<^const>‹alphabet_reduce› already established
in the two sibling sessions.
Two directions:
▪ ❙‹reduce after enlarge›: \<^term>‹alphabet_reduce (alphabet_enlarge M)›.
The enlarged machine feeds \<^const>‹alphabet_reduce›; the four-symbol lower
bound its hypotheses require follows from the constant-cell embedding of
the source alphabet into the block alphabet (‹card_gamma_block_ge_card›).
▪ ❙‹enlarge after reduce›: \<^term>‹alphabet_enlarge (alphabet_reduce M)›.
The reduced machine is well-formed for ∗‹any› valid source with a
four-symbol alphabet (‹alphabet_reduce_well_formed›), which discharges the
\<^const>‹well_formed_mttm› hypothesis \<^const>‹alphabet_enlarge› requires of its
input -- the cut-tolerance payoff.›
subsection ‹The enlarged alphabet has at least as many symbols as the source›
text ‹The block alphabet \<^term>‹gamma_block Γ› contains the constant
blocks \<^term>‹λ_. a› for every \<^term>‹a ∈ Γ›, and the embedding sending
‹a› to that constant cell is injective (the index type is inhabited). Hence
the enlarged alphabet is at least as large as the source, so a source with
\<^term>‹4 ≤ card Γ› enlarges to a machine whose alphabet still meets the
reduction combinator's minimal-alphabet bound.›
lemma card_gamma_block_ge_card:
fixes Γ :: "'a set"
assumes finG: "finite Γ"
shows "card Γ ≤ card (gamma_block Γ :: (('c :: enum) ⇒ 'a) set)"
proof -
have inj: "inj_on (λa. (λ_::'c. a)) Γ"
by (rule inj_onI) (metis fun_cong)
have img: "(λa. (λ_::'c. a)) ` Γ ⊆ gamma_block Γ"
by (auto simp: gamma_block_def)
have "card Γ = card ((λa. (λ_::'c. a)) ` Γ)"
by (simp add: card_image[OF inj])
also have "… ≤ card (gamma_block Γ :: ('c ⇒ 'a) set)"
by (rule card_mono[OF finite_gamma_block[OF finG] img])
finally show ?thesis .
qed
subsection ‹Time-composition preliminaries›
text ‹A small fact used when composing the running-time bounds: the block
count ‹(n + c - 1) div c› (rounding ‹n / c› up) that the enlargement
bound divides by never exceeds ‹n› for a nonempty index (‹0 < c›). (Weak
acceptance monotonicity, formerly local here, is now the substrate's
‹accepts_in_time_mttm_mono›.)›
lemma ceil_div_le:
fixes n c :: nat
assumes cpos: "0 < c"
shows "(n + c - 1) div c ≤ n"
proof (cases "n = 0")
case True
from cpos obtain m where cm: "c = Suc m" using gr0_implies_Suc by blast
have "c - 1 < c" using cm by simp
hence "(c - 1) div c = 0" by (rule div_less)
thus ?thesis using True by simp
next
case False
then have n1: "1 ≤ n" by simp
have cnz: "c ≠ 0" using cpos by simp
have eq: "n + c - 1 = (n - 1) + c" using n1 by simp
have "(n + c - 1) div c = (n - 1) div c + 1"
unfolding eq by (rule div_add_self2[OF cnz])
also have "… ≤ (n - 1) + 1"
using div_le_dividend[of "n - 1" c] by simp
also have "… = n" using n1 by simp
finally show ?thesis .
qed
subsection ‹Enlarge after reduce›
text ‹Reduce ‹M› to the four-symbol machine \<^term>‹alphabet_reduce M›, then
enlarge that. Language preservation chains the two headline biconditionals:
‹alphabet_reduce_language› (from ‹M› to the reduced machine, under the
per-symbol encoding \<^const>‹encode_input_ar›) and ‹alphabet_enlarge_language›
(from the reduced machine to its enlargement, under the block encoding
\<^const>‹encode_input›). Two seams are discharged locally: the reduced machine
is well-formed for any valid four-symbol source
(‹alphabet_reduce_well_formed›, the input hypothesis
\<^const>‹alphabet_enlarge› requires), and the encoded intermediate word lies in
the reduced machine's input alphabet \<^term>‹{BIT0, BIT1}›
(‹set_encode_input_ar›).›
theorem alphabet_reduce_enlarge_language:
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 ⟶
(encode_input (bl_tm (alphabet_reduce M))
(encode_input_ar (Γ_tm M) (bl_tm M) w)
∈ Lang_mttm (alphabet_enlarge (alphabet_reduce M)
:: ((('q × 'a ar_stage) × (sym4, 'c :: enum) ae_stage),
'c ⇒ sym4) mttm))
= (w ∈ Lang_mttm M)"
proof (intro allI impI)
fix w assume w: "set w ⊆ Sigma_tm M"
let ?Mr = "alphabet_reduce M :: ('q × 'a ar_stage, sym4) mttm"
let ?enc = "encode_input_ar (Γ_tm M) (bl_tm M) w"
have wfr: "well_formed_mttm ?Mr"
by (rule alphabet_reduce_well_formed[OF vM card_ge])
have red: "(?enc ∈ Lang_mttm ?Mr) = (w ∈ Lang_mttm M)"
using alphabet_reduce_language[OF vM s_neq_t s_neq_r le_neq_bl card_ge] w
by blast
have guard: "set ?enc ⊆ Sigma_tm ?Mr"
using set_encode_input_ar[of "Γ_tm M" "bl_tm M" w]
by (simp add: alphabet_reduce_Sigma)
have enl: "(encode_input (bl_tm ?Mr) ?enc
∈ Lang_mttm (alphabet_enlarge ?Mr
:: ((('q × 'a ar_stage) × (sym4, 'c) ae_stage),
'c ⇒ sym4) mttm))
= (?enc ∈ Lang_mttm ?Mr)"
using alphabet_enlarge_language[OF wfr] guard by blast
show "(encode_input (bl_tm ?Mr) ?enc
∈ Lang_mttm (alphabet_enlarge ?Mr
:: ((('q × 'a ar_stage) × (sym4, 'c) ae_stage),
'c ⇒ sym4) mttm))
= (w ∈ Lang_mttm M)"
using enl red by simp
qed
text ‹The composed slowdown, with explicit constants. Reducing then
enlarging is linear-time, with the affine bound
‹8 ⋅ (6 ⋅ k_tm M + 1) ⋅ b ⋅ T(|w|) + 2 ⋅ b ⋅ |w| + 4›, where
‹b = block_width (Γ_tm M)› is the per-symbol binary width and ‹k_tm M› the tape
count. It routes the explicit reduction bound
(‹(6 ⋅ k_tm M + 1) ⋅ b ⋅ T›, ‹alphabet_reduce_time_explicit›) in as the
enlargement's per-input running-time function ‹Tr›; on the encoded
intermediate word (length ‹b ⋅ |w|›) the enlargement hypothesis holds
∗‹exactly› (‹Tr (b ⋅ |w|) = (6 ⋅ k_tm M + 1) ⋅ b ⋅ T(|w|)›), and the
enlargement's ceiling divisions are relaxed by ‹ceil_div_le› and
‹accepts_in_time_mttm_mono›. The enlargement's block-speedup divisor
‹c = card (UNIV :: 'c set)› ∗‹cancels›: it divides the intermediate length
and running time, but ‹ceil_div_le› discards it in the relaxation, so it
does not appear in the bound --- the block speedup buys nothing once the
reduction has fixed the alphabet. The classical existential form is
‹alphabet_reduce_enlarge_time› below.›
theorem alphabet_reduce_enlarge_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_enlarge (alphabet_reduce M)
:: ((('q × 'a ar_stage) × (sym4, 'c :: enum) ae_stage),
'c ⇒ sym4) mttm)
(encode_input (bl_tm (alphabet_reduce M))
(encode_input_ar (Γ_tm M) (bl_tm M) w))
(8 * (6 * k_tm M + 1) * block_width (Γ_tm M) * T (length w)
+ 2 * block_width (Γ_tm M) * length w + 4)"
proof -
let ?Mr = "alphabet_reduce M :: ('q × 'a ar_stage, sym4) mttm"
let ?Me = "alphabet_enlarge ?Mr
:: ((('q × 'a ar_stage) × (sym4, 'c :: enum) ae_stage),
'c ⇒ sym4) mttm"
let ?kf = "block_width (Γ_tm M)"
let ?c = "card (UNIV :: 'c set)"
let ?d = "6 * k_tm M + 1"
have wfr: "well_formed_mttm ?Mr" by (rule alphabet_reduce_well_formed[OF vM card_ge])
have kfpos: "0 < ?kf" using block_width_pos[of "Γ_tm M"] by simp
have cpos: "0 < ?c" by (simp add: card_gt_0_iff)
have ar: "∀w. set w ⊆ Sigma_tm M ⟶
accepts_in_time_mttm M w (T (length w)) ⟶
accepts_in_time_mttm ?Mr (encode_input_ar (Γ_tm M) (bl_tm M) w)
(?d * ?kf * T (length w))"
by (rule alphabet_reduce_time_explicit[OF vM s_neq_t s_neq_r le_neq_bl card_ge])
define Tr :: "nat ⇒ nat" where "Tr = (λn. ?d * ?kf * T (n div ?kf))"
have ae: "∀v. set v ⊆ Sigma_tm ?Mr ⟶
accepts_in_time_mttm ?Mr v (Tr (length v)) ⟶
accepts_in_time_mttm ?Me (encode_input (bl_tm ?Mr) v)
(2 * ((length v + ?c - 1) div ?c)
+ 8 * ((Tr (length v) + ?c - 1) div ?c) + 4)"
by (rule alphabet_enlarge_time_explicit[OF wfr, where T = Tr])
show "∀w. set w ⊆ Sigma_tm M ⟶
accepts_in_time_mttm M w (T (length w)) ⟶
accepts_in_time_mttm ?Me
(encode_input (bl_tm ?Mr) (encode_input_ar (Γ_tm M) (bl_tm M) w))
(8 * (6 * k_tm M + 1) * block_width (Γ_tm M) * T (length w)
+ 2 * block_width (Γ_tm M) * length w + 4)"
proof (intro allI impI)
fix w assume w: "set w ⊆ Sigma_tm M"
and accM: "accepts_in_time_mttm M w (T (length w))"
let ?v = "encode_input_ar (Γ_tm M) (bl_tm M) w"
have lenv: "length ?v = ?kf * length w"
by (simp add: length_encode_input_ar)
have div_w: "length ?v div ?kf = length w"
using lenv kfpos by simp
have Tr_v: "Tr (length ?v) = ?d * ?kf * T (length w)"
using div_w by (simp add: Tr_def)
have accr: "accepts_in_time_mttm ?Mr ?v (Tr (length ?v))"
using ar w accM Tr_v by simp
have guard: "set ?v ⊆ Sigma_tm ?Mr"
using set_encode_input_ar[of "Γ_tm M" "bl_tm M" w]
by (simp add: alphabet_reduce_Sigma)
have ae_acc: "accepts_in_time_mttm ?Me (encode_input (bl_tm ?Mr) ?v)
(2 * ((length ?v + ?c - 1) div ?c)
+ 8 * ((Tr (length ?v) + ?c - 1) div ?c) + 4)"
using ae guard accr by blast
have bound_le:
"2 * ((length ?v + ?c - 1) div ?c)
+ 8 * ((Tr (length ?v) + ?c - 1) div ?c) + 4
≤ 8 * ?d * ?kf * T (length w) + 2 * ?kf * length w + 4"
proof -
have h1: "(length ?v + ?c - 1) div ?c ≤ length ?v" by (rule ceil_div_le[OF cpos])
have h2: "(Tr (length ?v) + ?c - 1) div ?c ≤ Tr (length ?v)" by (rule ceil_div_le[OF cpos])
have "2 * ((length ?v + ?c - 1) div ?c)
+ 8 * ((Tr (length ?v) + ?c - 1) div ?c) + 4
≤ 2 * length ?v + 8 * Tr (length ?v) + 4"
using h1 h2 by (simp add: add_mono mult_le_mono2)
also have "… = 2 * (?kf * length w) + 8 * (?d * ?kf * T (length w)) + 4"
using lenv Tr_v by simp
also have "… = 8 * ?d * ?kf * T (length w) + 2 * ?kf * length w + 4"
by (simp add: algebra_simps)
finally show ?thesis .
qed
show "accepts_in_time_mttm ?Me
(encode_input (bl_tm ?Mr) ?v)
(8 * (6 * k_tm M + 1) * block_width (Γ_tm M) * T (length w)
+ 2 * block_width (Γ_tm M) * length w + 4)"
by (rule accepts_in_time_mttm_mono[OF ae_acc bound_le])
qed
qed
text ‹The classical existential form ‹A ⋅ T(|w|) + B ⋅ |w| + C›, with
‹A = 8 ⋅ (6 ⋅ k_tm M + 1) ⋅ b›,
‹B = 2 ⋅ b›, and ‹C = 4› from
‹alphabet_reduce_enlarge_time_explicit›.›
theorem alphabet_reduce_enlarge_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 A B C :: nat
where "∀w. set w ⊆ Sigma_tm M ⟶
accepts_in_time_mttm M w (T (length w)) ⟶
accepts_in_time_mttm
(alphabet_enlarge (alphabet_reduce M)
:: ((('q × 'a ar_stage) × (sym4, 'c :: enum) ae_stage),
'c ⇒ sym4) mttm)
(encode_input (bl_tm (alphabet_reduce M))
(encode_input_ar (Γ_tm M) (bl_tm M) w))
(A * T (length w) + B * length w + C)"
proof (rule that[of "8 * (6 * k_tm M + 1) * block_width (Γ_tm M)"
"2 * block_width (Γ_tm M)" 4])
show "∀w. set w ⊆ Sigma_tm M ⟶
accepts_in_time_mttm M w (T (length w)) ⟶
accepts_in_time_mttm
(alphabet_enlarge (alphabet_reduce M)
:: ((('q × 'a ar_stage) × (sym4, 'c :: enum) ae_stage),
'c ⇒ sym4) mttm)
(encode_input (bl_tm (alphabet_reduce M))
(encode_input_ar (Γ_tm M) (bl_tm M) w))
(8 * (6 * k_tm M + 1) * block_width (Γ_tm M) * T (length w)
+ 2 * block_width (Γ_tm M) * length w + 4)"
by (rule alphabet_reduce_enlarge_time_explicit[OF vM s_neq_t s_neq_r le_neq_bl card_ge])
qed
subsection ‹Reduce after enlarge›
text ‹Enlarge ‹M› to the block machine \<^term>‹alphabet_enlarge M›, then reduce
that back to four symbols. This is the direction whose seams need the
enlarged machine's own well-formedness data: its start / accept / reject
states, blank and endmarker are the source ones tagged / block-encoded (the
field accessors ‹s_tm_alphabet_enlarge› etc.), and its tape alphabet is the
block alphabet \<^term>‹gamma_block (Γ_tm M)›, whose cardinality is at least
the source's (‹card_gamma_block_ge_card›) --- so a four-symbol source stays
above the reduction's minimal-alphabet bound.›
lemma Gamma_tm_alphabet_enlarge:
fixes M :: "('q, 'a) mttm"
shows "Γ_tm (alphabet_enlarge M
:: ('q × ('a, ('c :: enum)) ae_stage, 'c ⇒ 'a) mttm)
= gamma_block (Γ_tm M)"
by (cases M) (simp add: alphabet_enlarge_def)
text ‹Enlargement preserves the tape count (the last ‹mttm› field is
copied unchanged): the block transformation is purely alphabet-level, so the
reduction's tape-count factor ‹6 ⋅ k_tm M + 1› is the ∗‹source› tape count
even when the reduction is applied to the enlarged machine. Mirrors
‹alphabet_reduce_preserves_tape_count›.›
lemma k_tm_alphabet_enlarge:
fixes M :: "('q, 'a) mttm"
shows "k_tm (alphabet_enlarge M
:: ('q × ('a, ('c :: enum)) ae_stage, 'c ⇒ 'a) mttm)
= k_tm M"
by (cases M) (simp add: alphabet_enlarge_def)
text ‹Discharge of the reduction's input hypotheses on the enlarged machine
(validity, the three non-degeneracy conditions, and the four-symbol lower
bound), packaged for reuse by both the language and the time theorem.›
lemma alphabet_enlarge_reduce_hyps:
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 "valid_mttm (alphabet_enlarge M
:: ('q × ('a, 'c :: enum) ae_stage, 'c ⇒ 'a) mttm)"
and "s_tm (alphabet_enlarge M
:: ('q × ('a, 'c) ae_stage, 'c ⇒ 'a) mttm)
≠ t_tm (alphabet_enlarge M)"
and "s_tm (alphabet_enlarge M
:: ('q × ('a, 'c) ae_stage, 'c ⇒ 'a) mttm)
≠ r_tm (alphabet_enlarge M)"
and "le_tm (alphabet_enlarge M
:: ('q × ('a, 'c) ae_stage, 'c ⇒ 'a) mttm)
≠ bl_tm (alphabet_enlarge M)"
and "card (Γ_tm (alphabet_enlarge M
:: ('q × ('a, 'c) ae_stage, 'c ⇒ 'a) mttm)) ≥ 4"
proof -
let ?M' = "alphabet_enlarge M :: ('q × ('a, 'c) ae_stage, 'c ⇒ 'a) mttm"
have finG: "finite (Γ_tm M)" by (rule valid_mttm_finite_Gamma[OF vM])
show "valid_mttm ?M'" by (rule alphabet_enlarge_wf[OF vM])
show "s_tm ?M' ≠ t_tm ?M'"
using s_neq_t by (simp add: s_tm_alphabet_enlarge t_tm_alphabet_enlarge)
show "s_tm ?M' ≠ r_tm ?M'"
using s_neq_r by (simp add: s_tm_alphabet_enlarge r_tm_alphabet_enlarge)
show "le_tm ?M' ≠ bl_tm ?M'"
proof
assume "le_tm ?M' = bl_tm ?M'"
hence "(LE_block (le_tm M) :: 'c ⇒ 'a) = bl_block (bl_tm M)"
by (simp add: le_tm_alphabet_enlarge bl_tm_alphabet_enlarge)
hence "le_tm M = bl_tm M" by (rule LE_block_eq_bl_block_imp_eq)
with le_neq_bl show False by simp
qed
have "card (Γ_tm M) ≤ card (gamma_block (Γ_tm M) :: ('c ⇒ 'a) set)"
by (rule card_gamma_block_ge_card[OF finG])
hence "4 ≤ card (gamma_block (Γ_tm M) :: ('c ⇒ 'a) set)"
using card_ge by linarith
thus "card (Γ_tm ?M') ≥ 4" by (simp add: Gamma_tm_alphabet_enlarge)
qed
text ‹The intermediate-word guard: the block encoding of a genuine input
word lands in the enlarged machine's input alphabet (it is a block
over the source, and avoids the two reserved blocks). Shared by the
language and time theorems of this direction.›
lemma encode_input_in_Sigma_alphabet_enlarge:
fixes M :: "('q, 'a) mttm"
assumes vM: "valid_mttm M" and w: "set w ⊆ Sigma_tm M"
shows "set (encode_input (bl_tm M) w :: ('c :: enum ⇒ 'a) list)
⊆ Sigma_tm (alphabet_enlarge M
:: ('q × ('a, 'c) ae_stage, 'c ⇒ 'a) mttm)"
proof -
have "set (encode_input (bl_tm M) w :: ('c ⇒ 'a) list)
⊆ gamma_block (Sigma_tm M ∪ {bl_tm M})"
by (rule encode_input_in_gamma_block[OF w])
moreover have "bl_block (bl_tm M)
∉ set (encode_input (bl_tm M) w :: ('c ⇒ 'a) list)"
by (rule encode_input_no_bl_block[OF vM w])
moreover have "LE_block (le_tm M)
∉ set (encode_input (bl_tm M) w :: ('c ⇒ 'a) list)"
by (rule encode_input_no_LE_block[OF vM w])
ultimately show ?thesis by (auto simp: Sigma_tm_alphabet_enlarge)
qed
theorem alphabet_enlarge_reduce_language:
fixes M :: "('q, 'a) mttm"
assumes wfM: "well_formed_mttm M"
and card_ge: "card (Γ_tm M) ≥ 4"
shows "∀w. set w ⊆ Sigma_tm M ⟶
(encode_input_ar
(Γ_tm (alphabet_enlarge M
:: ('q × ('a, 'c :: enum) ae_stage, 'c ⇒ 'a) mttm))
(bl_tm (alphabet_enlarge M))
(encode_input (bl_tm M) w)
∈ Lang_mttm (alphabet_reduce (alphabet_enlarge M)
:: ((('q × ('a, 'c) ae_stage) × ('c ⇒ 'a) ar_stage), sym4) mttm))
= (w ∈ Lang_mttm M)"
proof (intro allI impI)
fix w assume w: "set w ⊆ Sigma_tm M"
let ?M' = "alphabet_enlarge M :: ('q × ('a, 'c) ae_stage, 'c ⇒ 'a) mttm"
have 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"
using wfM by auto
note hyps = alphabet_enlarge_reduce_hyps[OF vM s_neq_t s_neq_r le_neq_bl card_ge]
have enl: "(encode_input (bl_tm M) w ∈ Lang_mttm ?M') = (w ∈ Lang_mttm M)"
using alphabet_enlarge_language[OF wfM] w by blast
have guard: "set (encode_input (bl_tm M) w :: ('c ⇒ 'a) list) ⊆ Sigma_tm ?M'"
by (rule encode_input_in_Sigma_alphabet_enlarge[OF vM w])
have red: "(encode_input_ar (Γ_tm ?M') (bl_tm ?M') (encode_input (bl_tm M) w)
∈ Lang_mttm (alphabet_reduce ?M'
:: ((('q × ('a, 'c) ae_stage) × ('c ⇒ 'a) ar_stage), sym4) mttm))
= (encode_input (bl_tm M) w ∈ Lang_mttm ?M')"
using alphabet_reduce_language[OF hyps(1) hyps(2) hyps(3) hyps(4) hyps(5)] guard
by blast
show "(encode_input_ar (Γ_tm ?M') (bl_tm ?M') (encode_input (bl_tm M) w)
∈ Lang_mttm (alphabet_reduce ?M'
:: ((('q × ('a, 'c) ae_stage) × ('c ⇒ 'a) ar_stage), sym4) mttm))
= (w ∈ Lang_mttm M)"
using red enl by simp
qed
text ‹The composed slowdown for reduce-after-enlarge, with explicit
constants. Unlike the other order, the inner transformation (enlargement)
∗‹speeds up› by the block factor ‹c = card (UNIV :: 'c set)›, so the
intermediate word has length ‹⌈|w| / c⌉› --- a lossy function of ‹|w|›,
not an exact multiple --- and the enlarged machine's running time cannot be
routed into the reduction's time function exactly. Two mild ingredients
close the gap: ‹T› is assumed non-decreasing (‹mono T›), and the outer
bound is stated at ‹T(|w| + c - 1)› --- ‹T› at the input length rounded up
to the next block boundary. The bound is
‹8 ⋅ D ⋅ b' ⋅ T(|w| + c - 1) + 2 ⋅ D ⋅ b' ⋅ |w| + 4 ⋅ D ⋅ b'›, where
‹D = 6 ⋅ k_tm M + 1› (the tape count is preserved by enlargement,
‹k_tm_alphabet_enlarge›) and
‹b' = block_width (Γ_tm (alphabet_enlarge M)) = block_width (gamma_block (Γ_tm M))› is
the per-symbol width of the ∗‹block› alphabet, i.e.
‹⌈c ⋅ log⇩2 (card Γ⇩M)⌉›. Because ‹b'› grows with ‹c›, the block-speedup
factor ∗‹does not› cancel here: ‹c› survives both in the time argument
‹T(|w| + c - 1)› and, through ‹b'›, in every coefficient. The classical
existential form is ‹alphabet_enlarge_reduce_time› below.›
theorem alphabet_enlarge_reduce_time_explicit:
fixes M :: "('q, 'a) mttm" and T :: "nat ⇒ nat"
assumes wfM: "well_formed_mttm M"
and card_ge: "card (Γ_tm M) ≥ 4"
and Tmono: "mono T"
shows "∀w. set w ⊆ Sigma_tm M ⟶
accepts_in_time_mttm M w (T (length w)) ⟶
accepts_in_time_mttm
(alphabet_reduce (alphabet_enlarge M)
:: ((('q × ('a, 'c :: enum) ae_stage) × ('c ⇒ 'a) ar_stage), sym4) mttm)
(encode_input_ar
(Γ_tm (alphabet_enlarge M :: ('q × ('a, 'c) ae_stage, 'c ⇒ 'a) mttm))
(bl_tm (alphabet_enlarge M))
(encode_input (bl_tm M) w))
(8 * (6 * k_tm M + 1)
* block_width (Γ_tm (alphabet_enlarge M
:: ('q × ('a, 'c) ae_stage, 'c ⇒ 'a) mttm))
* T (length w + card (UNIV :: 'c set) - 1)
+ 2 * (6 * k_tm M + 1)
* block_width (Γ_tm (alphabet_enlarge M
:: ('q × ('a, 'c) ae_stage, 'c ⇒ 'a) mttm))
* length w
+ 4 * (6 * k_tm M + 1)
* block_width (Γ_tm (alphabet_enlarge M
:: ('q × ('a, 'c) ae_stage, 'c ⇒ 'a) mttm)))"
proof -
let ?M' = "alphabet_enlarge M :: ('q × ('a, 'c) ae_stage, 'c ⇒ 'a) mttm"
let ?c = "card (UNIV :: 'c set)"
let ?ke = "block_width (Γ_tm ?M')"
let ?d = "6 * k_tm M + 1"
have 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"
using wfM by auto
have cpos: "0 < ?c" by (simp add: card_gt_0_iff)
have ktm: "k_tm ?M' = k_tm M" by (rule k_tm_alphabet_enlarge)
note hyps = alphabet_enlarge_reduce_hyps[OF vM s_neq_t s_neq_r le_neq_bl card_ge]
have ae: "∀w. set w ⊆ Sigma_tm M ⟶
accepts_in_time_mttm M w (T (length w)) ⟶
accepts_in_time_mttm ?M' (encode_input (bl_tm M) w)
(2 * ((length w + ?c - 1) div ?c)
+ 8 * ((T (length w) + ?c - 1) div ?c) + 4)"
by (rule alphabet_enlarge_time_explicit[OF wfM])
define Te :: "nat ⇒ nat" where "Te = (λn. 8 * T (?c * n) + 2 * n + 4)"
have ar0: "∀v. set v ⊆ Sigma_tm ?M' ⟶
accepts_in_time_mttm ?M' v (Te (length v)) ⟶
accepts_in_time_mttm (alphabet_reduce ?M'
:: ((('q × ('a, 'c) ae_stage) × ('c ⇒ 'a) ar_stage), sym4) mttm)
(encode_input_ar (Γ_tm ?M') (bl_tm ?M') v)
((6 * k_tm ?M' + 1) * ?ke * Te (length v))"
by (rule alphabet_reduce_time_explicit[OF hyps(1) hyps(2) hyps(3) hyps(4) hyps(5)])
have ar: "∀v. set v ⊆ Sigma_tm ?M' ⟶
accepts_in_time_mttm ?M' v (Te (length v)) ⟶
accepts_in_time_mttm (alphabet_reduce ?M'
:: ((('q × ('a, 'c) ae_stage) × ('c ⇒ 'a) ar_stage), sym4) mttm)
(encode_input_ar (Γ_tm ?M') (bl_tm ?M') v)
(?d * ?ke * Te (length v))"
using ar0 by (simp add: ktm)
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, 'c) ae_stage) × ('c ⇒ 'a) ar_stage), sym4) mttm)
(encode_input_ar (Γ_tm ?M') (bl_tm ?M') (encode_input (bl_tm M) w))
(8 * ?d * ?ke * T (length w + ?c - 1)
+ 2 * ?d * ?ke * length w + 4 * ?d * ?ke)"
proof (intro allI impI)
fix w assume w: "set w ⊆ Sigma_tm M"
and accM: "accepts_in_time_mttm M w (T (length w))"
let ?v = "encode_input (bl_tm M) w :: ('c ⇒ 'a) list"
have lenv: "length ?v = (length w + ?c - 1) div ?c"
by (rule length_encode_input)
have lv_le: "length ?v ≤ length w"
using lenv ceil_div_le[OF cpos] by simp
have cge: "length w ≤ ?c * length ?v"
proof -
have eq: "?c * ((length w + ?c - 1) div ?c) + (length w + ?c - 1) mod ?c
= length w + ?c - 1"
by (rule mult_div_mod_eq)
have ml: "(length w + ?c - 1) mod ?c < ?c"
using cpos by (rule mod_less_divisor)
have "length w ≤ ?c * ((length w + ?c - 1) div ?c)"
using eq ml cpos by linarith
thus ?thesis by (simp add: lenv)
qed
have mcle: "?c * length ?v ≤ length w + ?c - 1"
proof -
have "?c * ((length w + ?c - 1) div ?c) ≤ length w + ?c - 1"
by (metis mult_div_mod_eq le_add1)
thus ?thesis using lenv by simp
qed
have accAE: "accepts_in_time_mttm ?M' ?v
(2 * ((length w + ?c - 1) div ?c)
+ 8 * ((T (length w) + ?c - 1) div ?c) + 4)"
using ae w accM by blast
have le1: "2 * ((length w + ?c - 1) div ?c)
+ 8 * ((T (length w) + ?c - 1) div ?c) + 4
≤ Te (length ?v)"
proof -
have alv: "2 * ((length w + ?c - 1) div ?c) = 2 * length ?v"
by (simp add: lenv)
have tb: "8 * ((T (length w) + ?c - 1) div ?c) ≤ 8 * T (?c * length ?v)"
proof -
have "(T (length w) + ?c - 1) div ?c ≤ T (length w)"
by (rule ceil_div_le[OF cpos])
also have "… ≤ T (?c * length ?v)" using Tmono cge by (rule monoD)
finally show ?thesis by (rule mult_le_mono2)
qed
have "2 * ((length w + ?c - 1) div ?c)
+ 8 * ((T (length w) + ?c - 1) div ?c) + 4
= 2 * length ?v + 8 * ((T (length w) + ?c - 1) div ?c) + 4"
by (simp only: alv)
also have "… ≤ 2 * length ?v + 8 * T (?c * length ?v) + 4"
using tb by simp
also have "… = Te (length ?v)" by (simp add: Te_def)
finally show ?thesis .
qed
have accr_hyp: "accepts_in_time_mttm ?M' ?v (Te (length ?v))"
by (rule accepts_in_time_mttm_mono[OF accAE le1])
have guard: "set ?v ⊆ Sigma_tm ?M'"
by (rule encode_input_in_Sigma_alphabet_enlarge[OF vM w])
have accAR: "accepts_in_time_mttm (alphabet_reduce ?M'
:: ((('q × ('a, 'c) ae_stage) × ('c ⇒ 'a) ar_stage), sym4) mttm)
(encode_input_ar (Γ_tm ?M') (bl_tm ?M') ?v)
(?d * ?ke * Te (length ?v))"
using ar guard accr_hyp by blast
have le2: "?d * ?ke * Te (length ?v)
≤ 8 * ?d * ?ke * T (length w + ?c - 1)
+ 2 * ?d * ?ke * length w + 4 * ?d * ?ke"
proof -
have T_le: "T (?c * length ?v) ≤ T (length w + ?c - 1)"
using Tmono mcle by (simp add: monoD)
have TeB: "Te (length ?v) ≤ 8 * T (length w + ?c - 1) + 2 * length w + 4"
unfolding Te_def using T_le lv_le
by (auto intro: add_mono mult_le_mono2)
have "?d * ?ke * Te (length ?v)
≤ ?d * ?ke * (8 * T (length w + ?c - 1) + 2 * length w + 4)"
using TeB by (rule mult_le_mono2)
also have "… = 8 * ?d * ?ke * T (length w + ?c - 1)
+ 2 * ?d * ?ke * length w + 4 * ?d * ?ke"
by (simp add: algebra_simps)
finally show ?thesis .
qed
show "accepts_in_time_mttm (alphabet_reduce ?M'
:: ((('q × ('a, 'c) ae_stage) × ('c ⇒ 'a) ar_stage), sym4) mttm)
(encode_input_ar (Γ_tm ?M') (bl_tm ?M') ?v)
(8 * ?d * ?ke * T (length w + ?c - 1)
+ 2 * ?d * ?ke * length w + 4 * ?d * ?ke)"
by (rule accepts_in_time_mttm_mono[OF accAR le2])
qed
qed
text ‹The classical existential form ‹A ⋅ T(|w| + c - 1) + B ⋅ |w| + C›,
with ‹A = 8 ⋅ D ⋅ b'›, ‹B = 2 ⋅ D ⋅ b'›, ‹C = 4 ⋅ D ⋅ b'› for
‹D = 6 ⋅ k_tm M + 1› and ‹b' = block_width (Γ_tm (alphabet_enlarge M))›, from
‹alphabet_enlarge_reduce_time_explicit›.›
theorem alphabet_enlarge_reduce_time:
fixes M :: "('q, 'a) mttm" and T :: "nat ⇒ nat"
assumes wfM: "well_formed_mttm M"
and card_ge: "card (Γ_tm M) ≥ 4"
and Tmono: "mono T"
obtains A B C :: nat
where "∀w. set w ⊆ Sigma_tm M ⟶
accepts_in_time_mttm M w (T (length w)) ⟶
accepts_in_time_mttm
(alphabet_reduce (alphabet_enlarge M)
:: ((('q × ('a, 'c :: enum) ae_stage) × ('c ⇒ 'a) ar_stage), sym4) mttm)
(encode_input_ar
(Γ_tm (alphabet_enlarge M :: ('q × ('a, 'c) ae_stage, 'c ⇒ 'a) mttm))
(bl_tm (alphabet_enlarge M))
(encode_input (bl_tm M) w))
(A * T (length w + card (UNIV :: 'c set) - 1) + B * length w + C)"
proof (rule that[of "8 * (6 * k_tm M + 1)
* block_width (Γ_tm (alphabet_enlarge M
:: ('q × ('a, 'c) ae_stage, 'c ⇒ 'a) mttm))"
"2 * (6 * k_tm M + 1)
* block_width (Γ_tm (alphabet_enlarge M
:: ('q × ('a, 'c) ae_stage, 'c ⇒ 'a) mttm))"
"4 * (6 * k_tm M + 1)
* block_width (Γ_tm (alphabet_enlarge M
:: ('q × ('a, 'c) ae_stage, 'c ⇒ 'a) mttm))"])
show "∀w. set w ⊆ Sigma_tm M ⟶
accepts_in_time_mttm M w (T (length w)) ⟶
accepts_in_time_mttm
(alphabet_reduce (alphabet_enlarge M)
:: ((('q × ('a, 'c) ae_stage) × ('c ⇒ 'a) ar_stage), sym4) mttm)
(encode_input_ar
(Γ_tm (alphabet_enlarge M :: ('q × ('a, 'c) ae_stage, 'c ⇒ 'a) mttm))
(bl_tm (alphabet_enlarge M))
(encode_input (bl_tm M) w))
(8 * (6 * k_tm M + 1)
* block_width (Γ_tm (alphabet_enlarge M
:: ('q × ('a, 'c) ae_stage, 'c ⇒ 'a) mttm))
* T (length w + card (UNIV :: 'c set) - 1)
+ 2 * (6 * k_tm M + 1)
* block_width (Γ_tm (alphabet_enlarge M
:: ('q × ('a, 'c) ae_stage, 'c ⇒ 'a) mttm))
* length w
+ 4 * (6 * k_tm M + 1)
* block_width (Γ_tm (alphabet_enlarge M
:: ('q × ('a, 'c) ae_stage, 'c ⇒ 'a) mttm)))"
by (rule alphabet_enlarge_reduce_time_explicit[OF wfM card_ge Tmono])
qed
end