Theory Multitape_Alphabet_Enlargement.AlphabetEnlargement_OutputWF
theory AlphabetEnlargement_OutputWF
imports AlphabetEnlargement_SS4
begin
subsection ‹Home classification and output well-formedness›
subsubsection ‹Home classification, stage unpack, load chain›
text ‹Per-tape home-cell LE-classification at SS1. Given the
M‹↔›M' tape correspondence (extracted from
‹ae_simulates›), the LE anchor on tape 0, and the
no-LE-window invariant on ‹cM›'s tape, the home block
of ‹c'›'s tape ‹k› equals ‹LE_block (le_tm M)›
iff ‹mt_pos c' k = 0›. Direction-agnostic; consumed by
both arms of the SS4-stage setup (the forward arm uses it to
drive ‹ae_ss1_to_ss4_buffer_chars_general›'s
‹home_class› hypothesis; the reverse arm uses it for the
symmetric extraction).›
lemma ae_home_classification:
fixes M :: "('q, 'a) mttm"
and cM :: "('a, 'q) mt_config"
and c' :: "('c :: enum ⇒ 'a,
'q × ('a, 'c) ae_stage) mt_config"
assumes le_anchor: "∀k<k_tm M. mt_tape c' k 0 = LE_block (le_tm M)"
and no_le_per_tape:
"∀k. (mt_pos c' k ≥ 2
⟶ (∀i. i < 3 * card (UNIV :: 'c set)
⟶ mt_tape cM k
((mt_pos c' k - 2)
* card (UNIV :: 'c set) + 1 + i)
≠ le_tm M))
∧ (mt_pos c' k = 1
⟶ (∀i. i < 2 * card (UNIV :: 'c set)
⟶ mt_tape cM k (Suc i) ≠ le_tm M))
∧ (mt_pos c' k = 0
⟶ (∀i. i < card (UNIV :: 'c set)
⟶ mt_tape cM k (Suc i) ≠ le_tm M))"
and tape_corr:
"∀k<k_tm M. ae_tape_correspondence (le_tm M)
(mt_tape cM k) (mt_tape c' k)"
shows "∀k<k_tm M. (mt_pos c' k = 0
⟶ mt_tape c' k (mt_pos c' k) = LE_block (le_tm M))
∧ (mt_pos c' k ≥ 1
⟶ mt_tape c' k (mt_pos c' k) ≠ LE_block (le_tm M))"
proof (intro allI impI conjI)
fix k :: nat
assume klt: "k < k_tm M" and pos0: "mt_pos c' k = 0"
have "mt_tape c' k 0 = LE_block (le_tm M)" using le_anchor klt by blast
thus "mt_tape c' k (mt_pos c' k) = LE_block (le_tm M)"
using pos0 by simp
next
fix k :: nat
assume klt: "k < k_tm M" and pos_ge1: "1 ≤ mt_pos c' k"
have c_ge_1: "1 ≤ card (UNIV :: 'c set)"
using c_idx_lt_card[of "SOME x :: 'c. True"] by simp
have c_eq_len:
"card (UNIV :: 'c set) = length (enum_class.enum :: 'c list)"
using enum_class.UNIV_enum enum_class.enum_distinct
by (metis distinct_card length_remdups_card_conv set_remdups)
let ?x = "(enum_class.enum :: 'c list) ! 0"
have zero_lt_len: "0 < length (enum_class.enum :: 'c list)"
using c_ge_1 c_eq_len by linarith
have x_idx0: "c_idx ?x = 0"
using c_idx_enum_nth[OF zero_lt_len] .
have tc_k: "ae_tape_correspondence (le_tm M)
(mt_tape cM k) (mt_tape c' k)"
using tape_corr klt by blast
have addr_lit:
"mt_tape cM k
((mt_pos c' k - 1) * card (UNIV :: 'c set) + c_idx ?x + 1)
= mt_tape c' k (mt_pos c' k) ?x"
using tc_k[unfolded ae_tape_correspondence_def, THEN conjunct2,
rule_format, OF pos_ge1, of ?x] .
have addr_via_tc:
"mt_tape cM k ((mt_pos c' k - 1) * card (UNIV :: 'c set) + 1)
= mt_tape c' k (mt_pos c' k) ?x"
using addr_lit x_idx0 by simp
consider (eq1) "mt_pos c' k = 1" | (ge2) "mt_pos c' k ≥ 2"
using pos_ge1 by linarith
hence "mt_tape c' k (mt_pos c' k) ?x ≠ le_tm M"
proof cases
case eq1
have idx_lt: "(0 :: nat) < 2 * card (UNIV :: 'c set)"
using c_ge_1 by simp
have addr_at_1:
"mt_tape cM k (Suc 0) = mt_tape c' k (mt_pos c' k) ?x"
using addr_via_tc eq1 by simp
have nle_at_1: "mt_tape cM k (Suc 0) ≠ le_tm M"
using no_le_per_tape eq1 idx_lt by blast
thus ?thesis using addr_at_1 by simp
next
case ge2
let ?j = "card (UNIV :: 'c set)"
have j_lt_3c: "?j < 3 * card (UNIV :: 'c set)"
using c_ge_1 by simp
have addr_eq:
"(mt_pos c' k - 1) * card (UNIV :: 'c set) + 1
= (mt_pos c' k - 2) * card (UNIV :: 'c set) + 1 + ?j"
using ge2 by (simp add: algebra_simps diff_mult_distrib)
have nle_at_addr:
"mt_tape cM k ((mt_pos c' k - 2) * card (UNIV :: 'c set) + 1 + ?j)
≠ le_tm M"
using no_le_per_tape ge2 j_lt_3c by blast
hence "mt_tape cM k ((mt_pos c' k - 1) * card (UNIV :: 'c set) + 1)
≠ le_tm M"
using addr_eq by simp
thus ?thesis using addr_via_tc by simp
qed
thus "mt_tape c' k (mt_pos c' k) ≠ LE_block (le_tm M)"
unfolding LE_block_def by auto
qed
text ‹Auxiliary: unpack the ‹ae_simulates› invariant at SS1
entry into the structural data forward-stage proofs need.
Extracts ‹M'›'s state-tuple shape (with ‹idx = SS1› pinned
by the M-state not-halted hypothesis), the ‹M›-state equality,
the M‹↔›M' tape and position correspondences, the gamma-block
side-band, the SS1 substrate invariant, and the (vacuous-at-SS1)
position-link. All three forward-stage variants —
steady-state and the two head-LE arms ‹le0›, ‹le1›
— open with this same unpacking; factoring it out keeps
the variants from cloning ~47 lines of preamble apiece.›
lemma ae_forward_stage_unpack_sim:
fixes M :: "('q, 'a) mttm"
and cM :: "('a, 'q) mt_config"
and c' :: "('c :: enum ⇒ 'a,
'q × ('a, 'c) ae_stage) mt_config"
assumes sim: "ae_simulates M cM c'"
and qM_in_Q: "mt_state cM ∈ Q_tm M"
and q_neq_t: "mt_state cM ≠ t_tm M"
and q_neq_r: "mt_state cM ≠ r_tm M"
obtains qM' ofs buf dest where
"mt_state c' = (qM', ofs, buf, dest, SS1)"
and "mt_state cM = qM'"
and "qM' ∈ Q_tm M"
and "qM' ≠ t_tm M"
and "qM' ≠ r_tm M"
and "∀k<k_tm M. ae_tape_correspondence (le_tm M)
(mt_tape cM k) (mt_tape c' k)"
and "∀k<k_tm M. mt_pos cM k = ae_decode_pos (mt_pos c' k) (ofs k)"
and "ae_tape_in_gamma_block M c'"
and "ae_inv_ss1 M c'"
and "ae_position_link M c'"
proof -
obtain qM' ofs buf dest idx_init where
state_comp: "mt_state c' = (qM', ofs, buf, dest, idx_init)"
by (cases "mt_state c'")
have sim_body:
"((idx_init = SS1 ∧ qM' ∉ {t_tm M, r_tm M})
∨ (qM' ∈ {t_tm M, r_tm M}
∧ (ofs, buf, dest, idx_init) = init_stage (le_tm M)))
∧ mt_state cM = qM'
∧ (∀k<k_tm M. ae_tape_correspondence (le_tm M)
(mt_tape cM k) (mt_tape c' k))
∧ (idx_init = SS1
⟶ (∀k<k_tm M. mt_pos cM k = ae_decode_pos (mt_pos c' k) (ofs k)))
∧ ae_tape_in_gamma_block M c'"
using sim state_comp unfolding ae_simulates_def by simp
have qM_eq: "mt_state cM = qM'" using sim_body by simp
have qM'_neq_t: "qM' ≠ t_tm M" using qM_eq q_neq_t by simp
have qM'_neq_r: "qM' ≠ r_tm M" using qM_eq q_neq_r by simp
have idx_is_ss1: "idx_init = SS1"
using sim_body qM'_neq_t qM'_neq_r by auto
have c'_state: "mt_state c' = (qM', ofs, buf, dest, SS1)"
using state_comp idx_is_ss1 by simp
have tape_corr:
"∀k<k_tm M. ae_tape_correspondence (le_tm M)
(mt_tape cM k) (mt_tape c' k)"
using sim_body by simp
have pos_corr:
"∀k<k_tm M. mt_pos cM k = ae_decode_pos (mt_pos c' k) (ofs k)"
using sim_body idx_is_ss1 by simp
have gamma_c': "ae_tape_in_gamma_block M c'"
using sim_body by simp
have qM'_in_Q: "qM' ∈ Q_tm M"
using qM_in_Q qM_eq by simp
have inv_ss1: "ae_inv_ss1 M c'"
unfolding ae_inv_ss1_def using c'_state qM'_in_Q by simp
have pos_link_c': "ae_position_link M c'"
using c'_state unfolding ae_position_link_def by simp
show ?thesis
by (rule that[OF c'_state qM_eq qM'_in_Q qM'_neq_t qM'_neq_r
tape_corr pos_corr gamma_c' inv_ss1 pos_link_c'])
qed
text ‹Auxiliary: the three buffer-load substeps SS1
‹→› SS2 ‹→› SS3 ‹→› SS4 as a
single chained existence lemma. Threads invariant preservation,
gamma preservation (tape + buffer), M-state propagation, and
position-link propagation across the three substeps; produces
the SS4-entry configuration ‹c3› with all the structural
facts forward-stage proofs need before reaching the c-fold
compute substep.
The block is arm-uniform: it depends only on the SS1 invariant
and the gamma side-band, not on the head's block position
or the no-LE window structure. All three forward-stage variants
— steady-state and the head-LE arms ‹le0›,
‹le1› — share this load chain verbatim;
factoring it out keeps the variants from cloning ~122 lines of
preservation plumbing apiece.
Position-link propagation through the load chain rests on the
pre-state's idx being SS1, SS2, SS3 respectively at each
substep, which keeps all three aux-void lemmas
(‹ae_pos_link_aux_void_ss<N>_ss<M>›) vacuously
satisfied.›
lemma ae_forward_stage_load_chain:
fixes M :: "('q, 'a) mttm"
and c' :: "('c :: enum ⇒ 'a,
'q × ('a, 'c) ae_stage) mt_config"
and qM' :: 'q
and ofs :: "nat ⇒ 'c"
and buf :: "nat ⇒ ('c ⇒ 'a) × ('c ⇒ 'a) × ('c ⇒ 'a)"
and dest :: "nat ⇒ ae_dest"
assumes vM: "valid_mttm M"
and c'_state: "mt_state c' = (qM', ofs, buf, dest, SS1)"
and inv_ss1: "ae_inv_ss1 M c'"
and gamma_c': "ae_tape_in_gamma_block M c'"
and buf_gamma: "ae_buffer_in_gamma_block M c'"
and pos_link_c': "ae_position_link M c'"
and qM'_neq_t: "qM' ≠ t_tm M"
and qM'_neq_r: "qM' ≠ r_tm M"
obtains c1 c2 c3 where
"(c', c1) ∈ mttm_step (ae_delta_ss1_ss2 M)"
and "(c', c1) ∈ mttm_step (alphabet_enlarge_delta M)"
and "(c1, c2) ∈ mttm_step (ae_delta_ss2_ss3 M)"
and "(c1, c2) ∈ mttm_step (alphabet_enlarge_delta M)"
and "(c2, c3) ∈ mttm_step (ae_delta_ss3_ss4 M)"
and "(c2, c3) ∈ mttm_step (alphabet_enlarge_delta M)"
and "ae_inv_ss4 M c3"
and "ae_tape_in_gamma_block M c3"
and "ae_buffer_in_gamma_block M c3"
and "fst (mt_state c3) = qM'"
and "ae_position_link M c3"
proof -
have c'_fst_neq_t: "fst (mt_state c') ≠ t_tm M"
using c'_state qM'_neq_t by simp
have c'_fst_neq_r: "fst (mt_state c') ≠ r_tm M"
using c'_state qM'_neq_r by simp
obtain c1 where
step1_sub: "(c', c1) ∈ mttm_step (ae_delta_ss1_ss2 M)"
and step1: "(c', c1) ∈ mttm_step (alphabet_enlarge_delta M)"
using ae_step_ss1_ss2_exists[OF inv_ss1 gamma_c' buf_gamma
c'_fst_neq_t c'_fst_neq_r] by blast
have inv_ss2: "ae_inv_ss2 M c1"
using ae_step_ss1_ss2_invariant[OF vM inv_ss1 step1_sub] .
have gamma_c1: "ae_tape_in_gamma_block M c1"
using ae_step_alphabet_enlarge_gamma_preserve[OF gamma_c' step1] .
have buf_gamma_c1: "ae_buffer_in_gamma_block M c1"
using ae_step_alphabet_enlarge_buffer_gamma_preserve[OF vM buf_gamma
gamma_c' step1] .
have c1_fst_eq: "fst (mt_state c1) = qM'"
using step1_sub c'_state
by (auto simp: ae_delta_ss1_ss2_def elim: mttm_step.cases)
have c1_fst_neq_t: "fst (mt_state c1) ≠ t_tm M"
using c1_fst_eq qM'_neq_t by simp
have c1_fst_neq_r: "fst (mt_state c1) ≠ r_tm M"
using c1_fst_eq qM'_neq_r by simp
have c'_idx_ss1: "snd (snd (snd (snd (mt_state c')))) = SS1"
using c'_state by simp
have aux_45_at_c': "(c', c1) ∈ mttm_step (ae_delta_ss4_ss5 M)
⟹ ae_position_link M c1"
using ae_pos_link_aux_void_ss4_ss5[where M = M and c_pre = c' and c_post = c1]
c'_idx_ss1 by simp
have aux_56_at_c': "(c', c1) ∈ mttm_step (ae_delta_ss5_ss6 M)
⟹ ae_position_link M c1"
using ae_pos_link_aux_void_ss5_ss6[where M = M and c_pre = c' and c_post = c1]
c'_idx_ss1 by simp
have aux_78_at_c': "(c', c1) ∈ mttm_step (ae_delta_ss7_ss8 M)
⟹ ae_position_link M c1"
using ae_pos_link_aux_void_ss7_ss8[where M = M and c_pre = c' and c_post = c1]
c'_idx_ss1 by simp
have pos_link_c1: "ae_position_link M c1"
using ae_step_alphabet_enlarge_position_link_preserve[OF pos_link_c'
step1 aux_45_at_c' aux_56_at_c' aux_78_at_c'] .
obtain c2 where
step2_sub: "(c1, c2) ∈ mttm_step (ae_delta_ss2_ss3 M)"
and step2: "(c1, c2) ∈ mttm_step (alphabet_enlarge_delta M)"
using ae_step_ss2_ss3_exists[OF vM inv_ss2 gamma_c1 buf_gamma_c1
c1_fst_neq_t c1_fst_neq_r] by blast
have inv_ss3: "ae_inv_ss3 M c2"
using ae_step_ss2_ss3_invariant[OF vM inv_ss2 step2_sub] .
have gamma_c2: "ae_tape_in_gamma_block M c2"
using ae_step_alphabet_enlarge_gamma_preserve[OF gamma_c1 step2] .
have buf_gamma_c2: "ae_buffer_in_gamma_block M c2"
using ae_step_alphabet_enlarge_buffer_gamma_preserve[OF vM buf_gamma_c1
gamma_c1 step2] .
have c2_fst_eq: "fst (mt_state c2) = qM'"
using step2_sub c1_fst_eq
by (cases "mt_state c1")
(auto simp: ae_delta_ss2_ss3_def elim: mttm_step.cases)
have c2_fst_neq_t: "fst (mt_state c2) ≠ t_tm M"
using c2_fst_eq qM'_neq_t by simp
have c2_fst_neq_r: "fst (mt_state c2) ≠ r_tm M"
using c2_fst_eq qM'_neq_r by simp
have c1_idx_ss2: "snd (snd (snd (snd (mt_state c1)))) = SS2"
using inv_ss2 unfolding ae_inv_ss2_def by (cases "mt_state c1") auto
have aux_45_at_c1: "(c1, c2) ∈ mttm_step (ae_delta_ss4_ss5 M)
⟹ ae_position_link M c2"
using ae_pos_link_aux_void_ss4_ss5[where M = M and c_pre = c1 and c_post = c2]
c1_idx_ss2 by simp
have aux_56_at_c1: "(c1, c2) ∈ mttm_step (ae_delta_ss5_ss6 M)
⟹ ae_position_link M c2"
using ae_pos_link_aux_void_ss5_ss6[where M = M and c_pre = c1 and c_post = c2]
c1_idx_ss2 by simp
have aux_78_at_c1: "(c1, c2) ∈ mttm_step (ae_delta_ss7_ss8 M)
⟹ ae_position_link M c2"
using ae_pos_link_aux_void_ss7_ss8[where M = M and c_pre = c1 and c_post = c2]
c1_idx_ss2 by simp
have pos_link_c2: "ae_position_link M c2"
using ae_step_alphabet_enlarge_position_link_preserve[OF pos_link_c1
step2 aux_45_at_c1 aux_56_at_c1 aux_78_at_c1] .
obtain c3 where
step3_sub: "(c2, c3) ∈ mttm_step (ae_delta_ss3_ss4 M)"
and step3: "(c2, c3) ∈ mttm_step (alphabet_enlarge_delta M)"
using ae_step_ss3_ss4_exists[OF inv_ss3 gamma_c2 buf_gamma_c2
c2_fst_neq_t c2_fst_neq_r] by blast
have inv_ss4: "ae_inv_ss4 M c3"
using ae_step_ss3_ss4_invariant[OF vM inv_ss3 step3_sub] .
have gamma_c3: "ae_tape_in_gamma_block M c3"
using ae_step_alphabet_enlarge_gamma_preserve[OF gamma_c2 step3] .
have buf_gamma_c3: "ae_buffer_in_gamma_block M c3"
using ae_step_alphabet_enlarge_buffer_gamma_preserve[OF vM buf_gamma_c2
gamma_c2 step3] .
have c3_fst_eq: "fst (mt_state c3) = qM'"
using step3_sub c2_fst_eq
by (cases "mt_state c2")
(auto simp: ae_delta_ss3_ss4_def elim: mttm_step.cases)
have c2_idx_ss3: "snd (snd (snd (snd (mt_state c2)))) = SS3"
using inv_ss3 unfolding ae_inv_ss3_def by (cases "mt_state c2") auto
have aux_45_at_c2: "(c2, c3) ∈ mttm_step (ae_delta_ss4_ss5 M)
⟹ ae_position_link M c3"
using ae_pos_link_aux_void_ss4_ss5[where M = M and c_pre = c2 and c_post = c3]
c2_idx_ss3 by simp
have aux_56_at_c2: "(c2, c3) ∈ mttm_step (ae_delta_ss5_ss6 M)
⟹ ae_position_link M c3"
using ae_pos_link_aux_void_ss5_ss6[where M = M and c_pre = c2 and c_post = c3]
c2_idx_ss3 by simp
have aux_78_at_c2: "(c2, c3) ∈ mttm_step (ae_delta_ss7_ss8 M)
⟹ ae_position_link M c3"
using ae_pos_link_aux_void_ss7_ss8[where M = M and c_pre = c2 and c_post = c3]
c2_idx_ss3 by simp
have pos_link_c3: "ae_position_link M c3"
using ae_step_alphabet_enlarge_position_link_preserve[OF pos_link_c2
step3 aux_45_at_c2 aux_56_at_c2 aux_78_at_c2] .
show ?thesis
by (rule that[OF step1_sub step1 step2_sub step2 step3_sub step3
inv_ss4 gamma_c3 buf_gamma_c3 c3_fst_eq pos_link_c3])
qed
subsubsection ‹Output well-formedness theorem›
text ‹Output well-formedness: ‹alphabet_enlarge› maps a valid
substrate machine to a valid one, i.e.
‹valid_mttm M ⟹ valid_mttm (alphabet_enlarge M)›.
Every component of ‹alphabet_enlarge M› is derived from
‹M›'s: the state set is ‹Q_tm M› paired with the finite
set of valid simulation stages, the tape alphabet is the block
alphabet ‹gamma_block (Γ_tm M)›, and the input
alphabet, endmarkers, and start/accept/reject states are the
corresponding block-encoded images. The proof discharges each
‹valid_mttm› conjunct (finiteness of the state and
alphabet sets, ‹Σ ⊆ Γ›, blank- and
endmarker-membership, and the LE-discipline on
‹alphabet_enlarge_delta›) from ‹M›'s.
This is the structural precondition the headline results build
on: ‹alphabet_enlarge_time› and the language theorems
(‹alphabet_enlarge_language_forward› here, the
biconditional ‹alphabet_enlarge_language› in
‹AlphabetEnlargement_Reverse.thy›) all reason about runs
of ‹alphabet_enlarge M›, which first requires it to be a
well-formed substrate object.›
text ‹State-shape projection of ‹alphabet_enlarge_delta›: every
transition's source and destination carry an ‹M›-state in
‹Q_tm M›, and the source is neither the lifted accept nor the
lifted reject state ‹(t_tm M, init_stage le)› /
‹(r_tm M, init_stage le)›. Read off the 16 substep builders by
their explicit ‹q ∈ Q_tm M› / substep-index discipline
(‹m_steps_buffered_state_preservation› supplies the
SS4‹→›SS5 destination ‹q'›). Crucially the proof touches only
the discrete state components, never the guarded per-tape lambdas, so
no ‹split: if_splits› is needed — that split, applied to the
‹if k < k_tm M› tape count guards across all 16 unfolded builders, is
what made the monolithic ‹δ›-shape ‹auto› in
‹alphabet_enlarge_wf› loop. The gamma-codomain and
‹ae_valid_stage› halves of that ‹δ›-shape conjunct come
straight off ‹alphabet_enlarge_delta›'s intersection guards
instead.›
lemma alphabet_enlarge_delta_state_shape:
fixes M :: "('q, 'a) mttm"
assumes valM: "valid_mttm M"
and mem: "(s, a, s', a', d) ∈ alphabet_enlarge_delta M"
shows "fst s ∈ Q_tm M ∧ fst s' ∈ Q_tm M
∧ s ≠ (t_tm M, init_stage (le_tm M))
∧ s ≠ (r_tm M, init_stage (le_tm M))"
proof -
from mem have mem_u:
"(s, a, s', a', d) ∈
ae_delta_val_fwd_advance M ∪ ae_delta_val_fwd_to_padded M
∪ ae_delta_val_fwd_reject M ∪ ae_delta_val_fwd_to_ret M
∪ ae_delta_val_pad_to_ret M ∪ ae_delta_val_pad_reject M
∪ ae_delta_val_ret_step M ∪ ae_delta_val_ret_to_sim M
∪ ae_delta_ss1_ss2 M ∪ ae_delta_ss2_ss3 M
∪ ae_delta_ss3_ss4 M ∪ ae_delta_ss4_ss5 M
∪ ae_delta_ss5_ss6 M ∪ ae_delta_ss6_ss7 M
∪ ae_delta_ss7_ss8 M ∪ ae_delta_ss8_ss1 M"
unfolding alphabet_enlarge_delta_def by blast
show ?thesis
using mem_u
unfolding ae_delta_val_fwd_advance_def ae_delta_val_fwd_to_padded_def
ae_delta_val_fwd_reject_def ae_delta_val_fwd_to_ret_def
ae_delta_val_pad_to_ret_def ae_delta_val_pad_reject_def
ae_delta_val_ret_step_def ae_delta_val_ret_to_sim_def
ae_delta_ss1_ss2_def ae_delta_ss2_ss3_def
ae_delta_ss3_ss4_def ae_delta_ss4_ss5_def
ae_delta_ss5_ss6_def ae_delta_ss6_ss7_def
ae_delta_ss7_ss8_def ae_delta_ss8_ss1_def
init_stage_def
using m_steps_buffered_state_preservation[OF valM]
valid_mttm_r_in_Q[OF valM] valid_mttm_t_in_Q[OF valM]
by auto
qed
theorem alphabet_enlarge_wf:
fixes M :: "('q, 'a) mttm"
assumes valM: "valid_mttm M"
shows "valid_mttm
(alphabet_enlarge M
:: ('q × ('a, ('c :: enum)) ae_stage, 'c ⇒ 'a) 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 le_in_Gamma: "le⇩M ∈ Γ⇩M"
using valid_mttm_LE_in_Gamma[OF valM] M_eq by simp
have ae_eq: "(alphabet_enlarge M
:: ('q × ('a, 'c) ae_stage, 'c ⇒ 'a) mttm) =
MTTM (Q⇩M × {stg. ae_valid_stage Γ⇩M le⇩M k⇩M stg})
(gamma_block (Σ⇩M ∪ {bl⇩M})
- {bl_block bl⇩M, LE_block le⇩M})
(gamma_block Γ⇩M)
(bl_block bl⇩M)
(LE_block le⇩M)
(alphabet_enlarge_delta M)
(s⇩M, init_stage le⇩M)
(t⇩M, init_stage le⇩M)
(r⇩M, init_stage le⇩M)
k⇩M"
unfolding M_eq alphabet_enlarge_def by simp
have init_valid: "ae_valid_stage Γ⇩M le⇩M k⇩M (init_stage le⇩M)"
by (rule ae_valid_stage_init[OF le_in_Gamma])
show "valid_mttm
(alphabet_enlarge M
:: ('q × ('a, ('c :: enum)) ae_stage, 'c ⇒ 'a) mttm)"
unfolding ae_eq valid_mttm.simps
proof (intro conjI)
show "0 < k⇩M"
using valid_mttm_k_pos[OF valM] M_eq by simp
show "finite (Q⇩M ×
({stg. ae_valid_stage Γ⇩M le⇩M k⇩M stg}
:: ('a, 'c) ae_stage set))"
using valid_mttm_finite_Q[OF valM] M_eq
finite_ae_valid_stages[OF fin_Gamma]
by (auto intro: finite_cartesian_product)
show "finite (gamma_block Γ⇩M :: ('c ⇒ 'a) set)"
using valid_mttm_finite_Gamma[OF valM] M_eq
by (auto intro: finite_gamma_block)
show "gamma_block (Σ⇩M ∪ {bl⇩M}) - {bl_block bl⇩M, LE_block le⇩M}
⊆ gamma_block Γ⇩M"
proof -
have "Σ⇩M ∪ {bl⇩M} ⊆ Γ⇩M"
using valid_mttm_Sigma_sub_Gamma[OF valM] valid_mttm_blank_in_Gamma[OF valM] M_eq
by auto
hence "gamma_block (Σ⇩M ∪ {bl⇩M}) ⊆ gamma_block Γ⇩M"
by (rule gamma_block_mono)
thus ?thesis by blast
qed
show "(s⇩M, init_stage le⇩M)
∈ Q⇩M × {stg. ae_valid_stage Γ⇩M le⇩M k⇩M stg}"
using valid_mttm_s_in_Q[OF valM] M_eq init_valid by simp
show "(t⇩M, init_stage le⇩M)
∈ Q⇩M × {stg. ae_valid_stage Γ⇩M le⇩M k⇩M stg}"
using valid_mttm_t_in_Q[OF valM] M_eq init_valid by simp
show "(r⇩M, init_stage le⇩M)
∈ Q⇩M × {stg. ae_valid_stage Γ⇩M le⇩M k⇩M stg}"
using valid_mttm_r_in_Q[OF valM] M_eq init_valid by simp
show "bl_block bl⇩M ∈ gamma_block Γ⇩M"
using bl_block_in_gamma_block[OF valid_mttm_blank_in_Gamma[OF valM]] M_eq
by simp
show "bl_block bl⇩M
∉ gamma_block (Σ⇩M ∪ {bl⇩M}) - {bl_block bl⇩M, LE_block le⇩M}"
by simp
show "LE_block le⇩M ∈ gamma_block Γ⇩M"
using LE_block_in_gamma_block[OF valid_mttm_LE_in_Gamma[OF valM]] M_eq
by simp
show "LE_block le⇩M
∉ gamma_block (Σ⇩M ∪ {bl⇩M}) - {bl_block bl⇩M, LE_block le⇩M}"
by simp
show "(t⇩M, init_stage le⇩M) ≠ (r⇩M, init_stage le⇩M)"
using valid_mttm_t_neq_r[OF valM] M_eq by simp
show "alphabet_enlarge_delta M
⊆ ((Q⇩M × {stg. ae_valid_stage Γ⇩M le⇩M k⇩M stg})
- {(t⇩M, init_stage le⇩M), (r⇩M, init_stage le⇩M)})
× (UNIV → gamma_block Γ⇩M)
× (Q⇩M × {stg. ae_valid_stage Γ⇩M le⇩M k⇩M stg})
× (UNIV → gamma_block Γ⇩M)
× (UNIV → UNIV)"
proof (rule subsetI)
fix x assume xin: "x ∈ alphabet_enlarge_delta M"
obtain s rest where x1: "x = (s, rest)" by (cases x)
obtain a rest2 where x2: "rest = (a, rest2)" by (cases rest)
obtain s' rest3 where x3: "rest2 = (s', rest3)" by (cases rest2)
obtain a' d where x4: "rest3 = (a', d)" by (cases rest3)
from x1 x2 x3 x4 have x_eq: "x = (s, a, s', a', d)" by simp
from xin have mem_t: "(s, a, s', a', d) ∈ alphabet_enlarge_delta M"
unfolding x_eq by simp
from mem_t have inter:
"(∀k. a k ∈ gamma_block (Γ_tm M))
∧ (∀k. a' k ∈ gamma_block (Γ_tm M))
∧ ae_valid_stage (Γ_tm M) (le_tm M) (k_tm M) (snd s)
∧ ae_valid_stage (Γ_tm M) (le_tm M) (k_tm M) (snd s')"
unfolding alphabet_enlarge_delta_def by simp
have shape: "fst s ∈ Q_tm M ∧ fst s' ∈ Q_tm M
∧ s ≠ (t_tm M, init_stage (le_tm M))
∧ s ≠ (r_tm M, init_stage (le_tm M))"
by (rule alphabet_enlarge_delta_state_shape[OF valM mem_t])
have s_in: "s ∈ (Q⇩M × {stg. ae_valid_stage Γ⇩M le⇩M k⇩M stg})
- {(t⇩M, init_stage le⇩M), (r⇩M, init_stage le⇩M)}"
using shape inter M_eq by (cases s) auto
have s'_in: "s' ∈ Q⇩M × {stg. ae_valid_stage Γ⇩M le⇩M k⇩M stg}"
using shape inter M_eq by (cases s') auto
have a_in: "a ∈ UNIV → gamma_block Γ⇩M"
using inter M_eq by (auto simp: Pi_iff)
have a'_in: "a' ∈ UNIV → gamma_block Γ⇩M"
using inter M_eq by (auto simp: Pi_iff)
show "x ∈ ((Q⇩M × {stg. ae_valid_stage Γ⇩M le⇩M k⇩M stg})
- {(t⇩M, init_stage le⇩M), (r⇩M, init_stage le⇩M)})
× (UNIV → gamma_block Γ⇩M)
× (Q⇩M × {stg. ae_valid_stage Γ⇩M le⇩M k⇩M stg})
× (UNIV → gamma_block Γ⇩M)
× (UNIV → UNIV)"
unfolding x_eq using s_in s'_in a_in a'_in
by (auto simp: mem_Times_iff Pi_iff)
qed
show "∀q a q' a' d k.
(q, a, q', a', d) ∈ alphabet_enlarge_delta M ⟶
a k = LE_block le⇩M ⟶
a' k = LE_block le⇩M ∧ d k ∈ {dir.N, dir.R}"
unfolding alphabet_enlarge_delta_def
ae_delta_val_fwd_advance_def ae_delta_val_fwd_to_padded_def
ae_delta_val_fwd_reject_def ae_delta_val_fwd_to_ret_def
ae_delta_val_pad_to_ret_def ae_delta_val_pad_reject_def
ae_delta_val_ret_step_def ae_delta_val_ret_to_sim_def
ae_delta_ss1_ss2_def ae_delta_ss2_ss3_def
ae_delta_ss3_ss4_def ae_delta_ss4_ss5_def
ae_delta_ss5_ss6_def ae_delta_ss6_ss7_def
ae_delta_ss7_ss8_def ae_delta_ss8_ss1_def
init_stage_def
using M_eq
by (auto split: if_splits prod.splits)
show "∀q a q' a' d.
(q, a, q', a', d) ∈ alphabet_enlarge_delta M ⟶
(∀j≥k⇩M. a j = bl_block bl⇩M
∧ a' j = bl_block bl⇩M
∧ d j = dir.N)"
unfolding alphabet_enlarge_delta_def
ae_delta_val_fwd_advance_def ae_delta_val_fwd_to_padded_def
ae_delta_val_fwd_reject_def ae_delta_val_fwd_to_ret_def
ae_delta_val_pad_to_ret_def ae_delta_val_pad_reject_def
ae_delta_val_ret_step_def ae_delta_val_ret_to_sim_def
ae_delta_ss1_ss2_def ae_delta_ss2_ss3_def
ae_delta_ss3_ss4_def ae_delta_ss4_ss5_def
ae_delta_ss5_ss6_def ae_delta_ss6_ss7_def
ae_delta_ss7_ss8_def ae_delta_ss8_ss1_def
using M_eq valid_mttm_k_pos[OF valM]
by (auto split: if_splits prod.splits)
qed
qed
end