Theory Multitape_Alphabet_Enlargement.AlphabetEnlargement_ValidationStep
theory AlphabetEnlargement_ValidationStep
imports AlphabetEnlargement_Codec
begin
subsection ‹Validation step machinery and initial config›
subsubsection ‹Validation canonicity equivalence with encoder image›
text ‹If a block is in ‹gamma_block (Sigma_M ∪ {bl_M})›,
then the decoder's per-block output stays in ‹Sigma_M›: the
takeWhile-prefix strips off any ‹bl_M›-symbols, leaving only
‹Sigma_M› elements. Per-block contribution to the
set-containment side of the iff lemma's forward direction.›
lemma ae_decode_block_subset:
fixes c :: "'c :: enum ⇒ 'a"
and Sigma :: "'a set"
and bl :: 'a
assumes "c ∈ gamma_block (Sigma ∪ {bl})"
shows "set (ae_decode_block bl c) ⊆ Sigma"
proof
fix a assume a_in: "a ∈ set (ae_decode_block bl c)"
let ?xs = "map c (enum_class.enum :: 'c list)"
have a_in_tW: "a ∈ set (takeWhile (λa. a ≠ bl) ?xs)"
using a_in by (simp add: ae_decode_block_def)
have neq_bl: "⋀ys :: 'a list. ∀x ∈ set (takeWhile (λa. a ≠ bl) ys).
x ≠ bl"
proof -
fix ys :: "'a list"
show "∀x ∈ set (takeWhile (λa. a ≠ bl) ys). x ≠ bl"
by (induct ys) (auto split: if_split_asm)
qed
have a_neq_bl: "a ≠ bl" using a_in_tW neq_bl by blast
have a_in_xs: "a ∈ set ?xs" using a_in_tW set_takeWhileD by metis
obtain x where a_eq: "a = c x" using a_in_xs by auto
have c_x_in: "c x ∈ Sigma ∪ {bl}"
using assms unfolding gamma_block_def by auto
show "a ∈ Sigma" using a_eq a_neq_bl c_x_in by blast
qed
text ‹The "in encoder image ‹⟶› well-formed" direction of
‹ae_validation_canonical_iff_encoder_image›. Stated as a
standalone lemma since it doesn't need the alphabet hypothesis
(the existential's ‹set u ⊆ Sigma_tm M› suffices) and is
cited by ‹ae_validation_post_state_canonical› for going
from "given ‹u ∈ Sigma_tm M⇧*›" to "validation passes
on ‹encode_input (bl_tm M) u›".›
lemma ae_well_formed_of_encoder_image:
fixes M :: "('q, 'a) mttm"
and u :: "'a list"
assumes vM: "valid_mttm M"
and u_sub: "set u ⊆ Sigma_tm M"
shows "ae_input_well_formed (bl_tm M)
(encode_input (bl_tm M) u :: ('c :: enum ⇒ 'a) list)"
proof -
have bl_notin: "bl_tm M ∉ Sigma_tm M"
using bl_tm_notin_Sigma_tm[OF vM] .
show ?thesis
unfolding ae_input_well_formed_def
proof (intro allI impI)
fix s
assume s_lt: "s < length (encode_input (bl_tm M) u :: ('c ⇒ 'a) list)"
show "is_pure_block (bl_tm M) ((encode_input (bl_tm M) u :: ('c ⇒ 'a) list) ! s)
∨ (s = length (encode_input (bl_tm M) u :: ('c ⇒ 'a) list) - 1
∧ is_padded_block (bl_tm M)
((encode_input (bl_tm M) u :: ('c ⇒ 'a) list) ! s))"
proof (cases "(s + 1) * card (UNIV :: 'c set) ≤ length u")
case True
have pure: "is_pure_block (bl_tm M)
((encode_input (bl_tm M) u :: ('c ⇒ 'a) list) ! s)"
unfolding is_pure_block_def
proof (rule allI)
fix x :: 'c
have c_idx_lt: "c_idx x < card (UNIV :: 'c set)"
by (rule c_idx_lt_card)
have j_lt: "s * card (UNIV :: 'c set) + c_idx x < length u"
using True c_idx_lt by (auto simp: algebra_simps)
have w_s_x: "((encode_input (bl_tm M) u :: ('c ⇒ 'a) list) ! s) x
= u ! (s * card (UNIV :: 'c set) + c_idx x)"
using encode_input_nth[OF s_lt, of x] j_lt by (simp add: Let_def)
have "u ! (s * card (UNIV :: 'c set) + c_idx x) ∈ set u"
using j_lt by (rule nth_mem)
hence "u ! (s * card (UNIV :: 'c set) + c_idx x) ∈ Sigma_tm M"
using u_sub by blast
thus "((encode_input (bl_tm M) u :: ('c ⇒ 'a) list) ! s) x
≠ bl_tm M"
using bl_notin w_s_x by auto
qed
show ?thesis using pure by (rule disjI1)
next
case False
let ?c = "card (UNIV :: 'c set)"
let ?N = "length (encode_input (bl_tm M) u :: ('c ⇒ 'a) list)"
have N_eq: "?N = (length u + ?c - 1) div ?c"
by (rule length_encode_input)
have c_eq_len_enum: "?c = 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)
have c_pos: "0 < ?c"
proof -
have "(c_first :: 'c) ∈ UNIV" by simp
thus ?thesis by (simp add: card_gt_0_iff)
qed
have len_u_pos: "0 < length u"
proof (rule ccontr)
assume "¬ 0 < length u"
hence u_eq: "length u = 0" by simp
have "?N = (?c - 1) div ?c" using N_eq u_eq by simp
also have "… = 0" using c_pos by simp
finally have "?N = 0" .
thus False using s_lt by simp
qed
from False have sp1c_gt: "length u < (s + 1) * ?c" by simp
have N_form: "?N = (length u - 1) div ?c + 1"
proof -
have eq1: "length u + ?c - 1 = (length u - 1) + ?c"
using len_u_pos c_pos by arith
have eq2: "((length u - 1) + ?c) div ?c
= (length u - 1) div ?c + 1"
using c_pos by (simp add: div_add_self2)
show ?thesis using N_eq eq1 eq2 by simp
qed
have N_minus_1: "?N - 1 = (length u - 1) div ?c"
using N_form by simp
have s_eq: "s = ?N - 1"
proof (rule ccontr)
assume "s ≠ ?N - 1"
with s_lt have s_lt_Nm1: "s < ?N - 1" by simp
hence sp1_le: "s + 1 ≤ ?N - 1" by simp
have "(s + 1) * ?c ≤ (?N - 1) * ?c"
using sp1_le by (rule mult_le_mono1)
also have "(?N - 1) * ?c = ((length u - 1) div ?c) * ?c"
using N_minus_1 by simp
also have "… ≤ length u - 1"
by (rule div_times_less_eq_dividend)
also have "… < length u" using len_u_pos by simp
finally have "(s + 1) * ?c < length u" .
thus False using sp1c_gt by simp
qed
have sc_lt: "s * ?c < length u"
proof -
have "s = (length u - 1) div ?c" using s_eq N_minus_1 by simp
hence "s * ?c = ((length u - 1) div ?c) * ?c" by simp
also have "… ≤ length u - 1"
by (rule div_times_less_eq_dividend)
also have "… < length u" using len_u_pos by simp
finally show ?thesis .
qed
let ?k = "length u - s * ?c"
have k_ge_1: "1 ≤ ?k" using sc_lt by simp
have k_lt_c: "?k < ?c"
proof -
have "length u < s * ?c + ?c"
using sp1c_gt by (simp add: algebra_simps)
thus ?thesis using sc_lt by simp
qed
have k_lt_enum: "?k < length (enum_class.enum :: 'c list)"
using k_lt_c c_eq_len_enum by simp
have padded: "is_padded_block (bl_tm M)
((encode_input (bl_tm M) u :: ('c ⇒ 'a) list) ! s)"
unfolding is_padded_block_def
proof (rule exI[of _ ?k], intro conjI)
show "1 ≤ ?k" by (rule k_ge_1)
show "?k < length (enum_class.enum :: 'c list)" by (rule k_lt_enum)
show "∀x. c_idx x < ?k
⟶ ((encode_input (bl_tm M) u :: ('c ⇒ 'a) list) ! s) x
≠ bl_tm M"
proof (intro allI impI)
fix x :: 'c
assume cx_lt: "c_idx x < ?k"
hence j_lt: "s * ?c + c_idx x < length u" by simp
have w_s_x: "((encode_input (bl_tm M) u :: ('c ⇒ 'a) list) ! s) x
= u ! (s * ?c + c_idx x)"
using encode_input_nth[OF s_lt, of x] j_lt by (simp add: Let_def)
have "u ! (s * ?c + c_idx x) ∈ set u"
using j_lt by (rule nth_mem)
hence "u ! (s * ?c + c_idx x) ∈ Sigma_tm M"
using u_sub by blast
thus "((encode_input (bl_tm M) u :: ('c ⇒ 'a) list) ! s) x
≠ bl_tm M"
using bl_notin w_s_x by auto
qed
show "∀x. ?k ≤ c_idx x
⟶ ((encode_input (bl_tm M) u :: ('c ⇒ 'a) list) ! s) x
= bl_tm M"
proof (intro allI impI)
fix x :: 'c
assume cx_ge: "?k ≤ c_idx x"
hence j_ge: "length u ≤ s * ?c + c_idx x" by simp
hence j_not_lt: "¬ s * ?c + c_idx x < length u" by simp
show "((encode_input (bl_tm M) u :: ('c ⇒ 'a) list) ! s) x
= bl_tm M"
using encode_input_nth[OF s_lt, of x] j_not_lt
by (simp add: Let_def)
qed
qed
from s_eq padded show ?thesis by blast
qed
qed
qed
text ‹Validation lemmas — structural induction over the input.
These do not require simulation infrastructure.›
text ‹The following biconditional characterises the AE machine's
set of well-formed inputs: a string is
‹ae_input_well_formed› if and only if it is the encoder
image of some base-alphabet input. The headline language
theorems ‹alphabet_enlarge_language› and
‹alphabet_enlarge_language_forward› are quantified only
over explicit encoder-image inputs (‹set w ⊆ Sigma_tm M›,
with the AE-side string given as
‹encode_input (bl_tm M) w›), so they need only the
forward direction provided above by
‹encode_input_well_formed›; they never appeal to this
biconditional's reverse direction (every well-formed AE-input
has a preimage under the encoder). The biconditional is
retained as a structural completeness result identifying
exactly what the AE machine accepts as a legitimate input, and
is potentially useful for the nondeterministic-reverse
research thread, where extracting an encoder preimage from an
AE-validation hypothesis is one of the load-bearing steps.›
lemma ae_validation_canonical_iff_encoder_image:
fixes M :: "('q, 'a) mttm"
and w :: "('c :: enum ⇒ 'a) list"
assumes vM: "valid_mttm M"
and w_sub: "set w ⊆ gamma_block (Sigma_tm M ∪ {bl_tm M})"
shows "ae_input_well_formed (bl_tm M) w
⟷ (∃u. set u ⊆ Sigma_tm M
∧ w = encode_input (bl_tm M) u)"
proof
assume wf: "ae_input_well_formed (bl_tm M) w"
let ?u = "ae_decode_input (bl_tm M) w"
have round_trip: "encode_input (bl_tm M) ?u = w"
using encode_decode_round_trip[OF wf] .
have u_sub: "set ?u ⊆ Sigma_tm M"
proof
fix a assume "a ∈ set ?u"
hence "a ∈ set (concat (map (ae_decode_block (bl_tm M)) w))"
by (simp add: ae_decode_input_def)
then obtain c where c_in: "c ∈ set w"
and a_in_blk: "a ∈ set (ae_decode_block (bl_tm M) c)"
by auto
have c_in_gamma: "c ∈ gamma_block (Sigma_tm M ∪ {bl_tm M})"
using c_in w_sub by blast
have "set (ae_decode_block (bl_tm M) c) ⊆ Sigma_tm M"
by (rule ae_decode_block_subset[OF c_in_gamma])
thus "a ∈ Sigma_tm M" using a_in_blk by blast
qed
show "∃u. set u ⊆ Sigma_tm M
∧ w = encode_input (bl_tm M) u"
using u_sub round_trip[symmetric] by blast
next
assume "∃u. set u ⊆ Sigma_tm M
∧ w = encode_input (bl_tm M) u"
then obtain u where
u_sub: "set u ⊆ Sigma_tm M" and
w_eq: "w = encode_input (bl_tm M) u" by blast
have "ae_input_well_formed (bl_tm M)
(encode_input (bl_tm M) u :: ('c ⇒ 'a) list)"
using ae_well_formed_of_encoder_image[OF vM u_sub] .
thus "ae_input_well_formed (bl_tm M) w" using w_eq by simp
qed
subsubsection ‹Validation step helpers›
text ‹Step-helper library for the validation phase. Each
helper packages one validation substep relation as an
‹mttm_step›-constructor: given source-state and
read-tape constraints satisfying the relation's source pattern,
produce a single ‹mttm_step (alphabet_enlarge_delta M)›.
Used by the three remaining commit-B lemmas
(‹ae_validation_steps_bound›,
‹ae_validation_post_state_canonical›,
‹ae_validation_post_state_noncanonical›) to assemble
validation-phase chains by composition rather than re-deriving
each step.›
lemma ae_step_make:
fixes M :: "('q, 'a) mttm"
and ts :: "nat ⇒ nat ⇒ ('c :: enum ⇒ 'a)"
and n :: "nat ⇒ nat"
and s s' :: "'q × ('a, 'c) ae_stage"
and a' :: "nat ⇒ ('c ⇒ 'a)"
and d :: "nat ⇒ dir"
assumes rel: "(s, (λk. ts k (n k)), s', a', d)
∈ alphabet_enlarge_delta M"
shows "(Config⇩M s ts n,
Config⇩M s' (λk. (ts k)(n k := a' k))
(λk. go_dir (d k) (n k)))
∈ mttm_step (alphabet_enlarge_delta M)"
proof (rule mttm_step.intros)
show "(s, (λk. ts k (n k)), s', a', d)
∈ alphabet_enlarge_delta M" by (rule rel)
qed
text ‹Reflexive frozen-tail for the initial stage. The stage
fields ‹init_offset› / ‹init_buffer le› / ‹init_dest› agree with
themselves beyond any tape count ‹K›, so this discharges the
‹stage_tail› premise of every validation step-helper at the call
sites, where the stage is literally ‹init_stage (le_tm M)› (the
validation phases never touch the buffer).›
lemma init_stage_tail:
"(∀j≥K. init_offset j = init_offset j)
∧ (∀j≥K. init_buffer le j = init_buffer le j)
∧ (∀j≥K. init_dest j = init_dest j)"
by simp
text ‹VFwd advance: read ‹LE_block› or a pure block on
tape 0; head moves R on tape 0, N elsewhere; phase stays VFwd;
no write change.›
lemma ae_step_val_fwd_advance:
fixes M :: "('q, 'a) mttm"
and ts :: "nat ⇒ nat ⇒ ('c :: enum ⇒ 'a)"
and n :: "nat ⇒ nat"
and q :: 'q
and ofs :: "nat ⇒ 'c"
and buf :: "nat ⇒ ('c ⇒ 'a) × ('c ⇒ 'a) × ('c ⇒ 'a)"
and dest :: "nat ⇒ ae_dest"
assumes q_in: "q ∈ Q_tm M"
and q_neq_t: "q ≠ t_tm M"
and q_neq_r: "q ≠ r_tm M"
and read: "ts (0 :: nat) (n 0) = LE_block (le_tm M)
∨ is_pure_block (bl_tm M) (ts 0 (n 0))"
and bt: "∀j≥k_tm M. ∀i. ts j i = bl_block (bl_tm M)"
and stage_tail: "(∀j≥k_tm M. ofs j = init_offset j)
∧ (∀j≥k_tm M. buf j = init_buffer (le_tm M) j)
∧ (∀j≥k_tm M. dest j = init_dest j)"
and gamma: "∀k. ts k (n k) ∈ gamma_block (Γ_tm M)"
and buf_gamma: "∀k. fst (buf k) ∈ gamma_block (Γ_tm M)
∧ fst (snd (buf k)) ∈ gamma_block (Γ_tm M)
∧ snd (snd (buf k)) ∈ gamma_block (Γ_tm M)"
shows "(Config⇩M (q, ofs, buf, dest, VFwd) ts n,
Config⇩M (q, ofs, buf, dest, VFwd) ts
(λk. go_dir (if k = 0 then dir.R else dir.N) (n k)))
∈ mttm_step (alphabet_enlarge_delta M)"
proof -
let ?d = "λk :: nat. if k = 0 then dir.R else dir.N"
let ?a = "λk. ts k (n k)"
have rel_in: "((q, ofs, buf, dest, VFwd), ?a,
(q, ofs, buf, dest, VFwd), ?a, ?d)
∈ ae_delta_val_fwd_advance M"
unfolding ae_delta_val_fwd_advance_def
using q_in q_neq_t q_neq_r read bt by auto
have src_valid: "ae_valid_stage (Γ_tm M) (le_tm M) (k_tm M)
(snd ((q, ofs, buf, dest, VFwd)
:: 'q × ('a, 'c) ae_stage))"
using buf_gamma stage_tail unfolding ae_valid_stage_def by simp
have aed_in: "((q, ofs, buf, dest, VFwd), ?a,
(q, ofs, buf, dest, VFwd), ?a, ?d)
∈ alphabet_enlarge_delta M"
unfolding alphabet_enlarge_delta_def
using rel_in gamma src_valid by auto
have ts_unchanged: "(λk. (ts k)(n k := ?a k)) = ts"
by (rule ext) auto
have step: "(Config⇩M (q, ofs, buf, dest, VFwd) ts n,
Config⇩M (q, ofs, buf, dest, VFwd)
(λk. (ts k)(n k := ?a k))
(λk. go_dir (?d k) (n k)))
∈ mttm_step (alphabet_enlarge_delta M)"
proof (rule ae_step_make)
show "((q, ofs, buf, dest, VFwd), ?a,
(q, ofs, buf, dest, VFwd), ?a, ?d)
∈ alphabet_enlarge_delta M" by (rule aed_in)
qed
show ?thesis using step ts_unchanged by simp
qed
text ‹VFwd ‹→› VFwdPad: read a padded block on
tape 0; head moves R on tape 0, N elsewhere; phase becomes
VFwdPad; no write change.›
lemma ae_step_val_fwd_to_padded:
fixes M :: "('q, 'a) mttm"
and ts :: "nat ⇒ nat ⇒ ('c :: enum ⇒ 'a)"
and n :: "nat ⇒ nat"
and q :: 'q
and ofs :: "nat ⇒ 'c"
and buf :: "nat ⇒ ('c ⇒ 'a) × ('c ⇒ 'a) × ('c ⇒ 'a)"
and dest :: "nat ⇒ ae_dest"
assumes q_in: "q ∈ Q_tm M"
and q_neq_t: "q ≠ t_tm M"
and q_neq_r: "q ≠ r_tm M"
and read: "is_padded_block (bl_tm M) (ts (0 :: nat) (n 0))"
and bt: "∀j≥k_tm M. ∀i. ts j i = bl_block (bl_tm M)"
and stage_tail: "(∀j≥k_tm M. ofs j = init_offset j)
∧ (∀j≥k_tm M. buf j = init_buffer (le_tm M) j)
∧ (∀j≥k_tm M. dest j = init_dest j)"
and gamma: "∀k. ts k (n k) ∈ gamma_block (Γ_tm M)"
and buf_gamma: "∀k. fst (buf k) ∈ gamma_block (Γ_tm M)
∧ fst (snd (buf k)) ∈ gamma_block (Γ_tm M)
∧ snd (snd (buf k)) ∈ gamma_block (Γ_tm M)"
shows "(Config⇩M (q, ofs, buf, dest, VFwd) ts n,
Config⇩M (q, ofs, buf, dest, VFwdPad) ts
(λk. go_dir (if k = 0 then dir.R else dir.N) (n k)))
∈ mttm_step (alphabet_enlarge_delta M)"
proof -
let ?d = "λk :: nat. if k = 0 then dir.R else dir.N"
let ?a = "λk. ts k (n k)"
have rel_in: "((q, ofs, buf, dest, VFwd), ?a,
(q, ofs, buf, dest, VFwdPad), ?a, ?d)
∈ ae_delta_val_fwd_to_padded M"
unfolding ae_delta_val_fwd_to_padded_def
using q_in q_neq_t q_neq_r read bt by auto
have src_valid: "ae_valid_stage (Γ_tm M) (le_tm M) (k_tm M)
(snd ((q, ofs, buf, dest, VFwd)
:: 'q × ('a, 'c) ae_stage))"
using buf_gamma stage_tail unfolding ae_valid_stage_def by simp
have dst_valid: "ae_valid_stage (Γ_tm M) (le_tm M) (k_tm M)
(snd ((q, ofs, buf, dest, VFwdPad)
:: 'q × ('a, 'c) ae_stage))"
using buf_gamma stage_tail unfolding ae_valid_stage_def by simp
have aed_in: "((q, ofs, buf, dest, VFwd), ?a,
(q, ofs, buf, dest, VFwdPad), ?a, ?d)
∈ alphabet_enlarge_delta M"
unfolding alphabet_enlarge_delta_def
using rel_in gamma src_valid dst_valid by auto
have ts_unchanged: "(λk. (ts k)(n k := ?a k)) = ts"
by (rule ext) auto
have step: "(Config⇩M (q, ofs, buf, dest, VFwd) ts n,
Config⇩M (q, ofs, buf, dest, VFwdPad)
(λk. (ts k)(n k := ?a k))
(λk. go_dir (?d k) (n k)))
∈ mttm_step (alphabet_enlarge_delta M)"
proof (rule ae_step_make)
show "((q, ofs, buf, dest, VFwd), ?a,
(q, ofs, buf, dest, VFwdPad), ?a, ?d)
∈ alphabet_enlarge_delta M" by (rule aed_in)
qed
show ?thesis using step ts_unchanged by simp
qed
text ‹VFwd ‹→› VRet: read ‹bl_block bl_M› on tape 0
(past the encoded input); N moves uniformly (head stays); phase
becomes VRet.›
lemma ae_step_val_fwd_to_ret:
fixes M :: "('q, 'a) mttm"
and ts :: "nat ⇒ nat ⇒ ('c :: enum ⇒ 'a)"
and n :: "nat ⇒ nat"
and q :: 'q
and ofs :: "nat ⇒ 'c"
and buf :: "nat ⇒ ('c ⇒ 'a) × ('c ⇒ 'a) × ('c ⇒ 'a)"
and dest :: "nat ⇒ ae_dest"
assumes q_in: "q ∈ Q_tm M"
and q_neq_t: "q ≠ t_tm M"
and q_neq_r: "q ≠ r_tm M"
and read: "ts (0 :: nat) (n 0) = bl_block (bl_tm M)"
and bt: "∀j≥k_tm M. ∀i. ts j i = bl_block (bl_tm M)"
and stage_tail: "(∀j≥k_tm M. ofs j = init_offset j)
∧ (∀j≥k_tm M. buf j = init_buffer (le_tm M) j)
∧ (∀j≥k_tm M. dest j = init_dest j)"
and gamma: "∀k. ts k (n k) ∈ gamma_block (Γ_tm M)"
and buf_gamma: "∀k. fst (buf k) ∈ gamma_block (Γ_tm M)
∧ fst (snd (buf k)) ∈ gamma_block (Γ_tm M)
∧ snd (snd (buf k)) ∈ gamma_block (Γ_tm M)"
shows "(Config⇩M (q, ofs, buf, dest, VFwd) ts n,
Config⇩M (q, ofs, buf, dest, VRet) ts n)
∈ mttm_step (alphabet_enlarge_delta M)"
proof -
let ?d = "λ_ :: nat. dir.N"
let ?a = "λk. ts k (n k)"
have rel_in: "((q, ofs, buf, dest, VFwd), ?a,
(q, ofs, buf, dest, VRet), ?a, ?d)
∈ ae_delta_val_fwd_to_ret M"
unfolding ae_delta_val_fwd_to_ret_def
using q_in q_neq_t q_neq_r read bt by auto
have src_valid: "ae_valid_stage (Γ_tm M) (le_tm M) (k_tm M)
(snd ((q, ofs, buf, dest, VFwd)
:: 'q × ('a, 'c) ae_stage))"
using buf_gamma stage_tail unfolding ae_valid_stage_def by simp
have dst_valid: "ae_valid_stage (Γ_tm M) (le_tm M) (k_tm M)
(snd ((q, ofs, buf, dest, VRet)
:: 'q × ('a, 'c) ae_stage))"
using buf_gamma stage_tail unfolding ae_valid_stage_def by simp
have aed_in: "((q, ofs, buf, dest, VFwd), ?a,
(q, ofs, buf, dest, VRet), ?a, ?d)
∈ alphabet_enlarge_delta M"
unfolding alphabet_enlarge_delta_def
using rel_in gamma src_valid dst_valid by auto
have ts_unchanged: "(λk. (ts k)(n k := ?a k)) = ts"
by (rule ext) auto
have n_unchanged: "(λk :: nat. go_dir (?d k) (n k)) = n"
by (rule ext) simp
have step: "(Config⇩M (q, ofs, buf, dest, VFwd) ts n,
Config⇩M (q, ofs, buf, dest, VRet)
(λk. (ts k)(n k := ?a k))
(λk. go_dir (?d k) (n k)))
∈ mttm_step (alphabet_enlarge_delta M)"
proof (rule ae_step_make)
show "((q, ofs, buf, dest, VFwd), ?a,
(q, ofs, buf, dest, VRet), ?a, ?d)
∈ alphabet_enlarge_delta M" by (rule aed_in)
qed
show ?thesis using step ts_unchanged n_unchanged by simp
qed
text ‹VFwdPad ‹→› VRet: read ‹bl_block bl_M› on tape 0
(past the trailing-padded block into the blanks); N moves;
phase becomes VRet.›
lemma ae_step_val_pad_to_ret:
fixes M :: "('q, 'a) mttm"
and ts :: "nat ⇒ nat ⇒ ('c :: enum ⇒ 'a)"
and n :: "nat ⇒ nat"
and q :: 'q
and ofs :: "nat ⇒ 'c"
and buf :: "nat ⇒ ('c ⇒ 'a) × ('c ⇒ 'a) × ('c ⇒ 'a)"
and dest :: "nat ⇒ ae_dest"
assumes q_in: "q ∈ Q_tm M"
and read: "ts (0 :: nat) (n 0) = bl_block (bl_tm M)"
and bt: "∀j≥k_tm M. ∀i. ts j i = bl_block (bl_tm M)"
and stage_tail: "(∀j≥k_tm M. ofs j = init_offset j)
∧ (∀j≥k_tm M. buf j = init_buffer (le_tm M) j)
∧ (∀j≥k_tm M. dest j = init_dest j)"
and gamma: "∀k. ts k (n k) ∈ gamma_block (Γ_tm M)"
and buf_gamma: "∀k. fst (buf k) ∈ gamma_block (Γ_tm M)
∧ fst (snd (buf k)) ∈ gamma_block (Γ_tm M)
∧ snd (snd (buf k)) ∈ gamma_block (Γ_tm M)"
shows "(Config⇩M (q, ofs, buf, dest, VFwdPad) ts n,
Config⇩M (q, ofs, buf, dest, VRet) ts n)
∈ mttm_step (alphabet_enlarge_delta M)"
proof -
let ?d = "λ_ :: nat. dir.N"
let ?a = "λk. ts k (n k)"
have rel_in: "((q, ofs, buf, dest, VFwdPad), ?a,
(q, ofs, buf, dest, VRet), ?a, ?d)
∈ ae_delta_val_pad_to_ret M"
unfolding ae_delta_val_pad_to_ret_def
using q_in read bt by auto
have src_valid: "ae_valid_stage (Γ_tm M) (le_tm M) (k_tm M)
(snd ((q, ofs, buf, dest, VFwdPad)
:: 'q × ('a, 'c) ae_stage))"
using buf_gamma stage_tail unfolding ae_valid_stage_def by simp
have dst_valid: "ae_valid_stage (Γ_tm M) (le_tm M) (k_tm M)
(snd ((q, ofs, buf, dest, VRet)
:: 'q × ('a, 'c) ae_stage))"
using buf_gamma stage_tail unfolding ae_valid_stage_def by simp
have aed_in: "((q, ofs, buf, dest, VFwdPad), ?a,
(q, ofs, buf, dest, VRet), ?a, ?d)
∈ alphabet_enlarge_delta M"
unfolding alphabet_enlarge_delta_def
using rel_in gamma src_valid dst_valid by auto
have ts_unchanged: "(λk. (ts k)(n k := ?a k)) = ts"
by (rule ext) auto
have n_unchanged: "(λk :: nat. go_dir (?d k) (n k)) = n"
by (rule ext) simp
have step: "(Config⇩M (q, ofs, buf, dest, VFwdPad) ts n,
Config⇩M (q, ofs, buf, dest, VRet)
(λk. (ts k)(n k := ?a k))
(λk. go_dir (?d k) (n k)))
∈ mttm_step (alphabet_enlarge_delta M)"
proof (rule ae_step_make)
show "((q, ofs, buf, dest, VFwdPad), ?a,
(q, ofs, buf, dest, VRet), ?a, ?d)
∈ alphabet_enlarge_delta M" by (rule aed_in)
qed
show ?thesis using step ts_unchanged n_unchanged by simp
qed
text ‹VRet step: read a non-LE block on tape 0 (during the
return scan); head moves L on tape 0, N elsewhere; phase stays
VRet.›
lemma ae_step_val_ret_step:
fixes M :: "('q, 'a) mttm"
and ts :: "nat ⇒ nat ⇒ ('c :: enum ⇒ 'a)"
and n :: "nat ⇒ nat"
and q :: 'q
and ofs :: "nat ⇒ 'c"
and buf :: "nat ⇒ ('c ⇒ 'a) × ('c ⇒ 'a) × ('c ⇒ 'a)"
and dest :: "nat ⇒ ae_dest"
assumes q_in: "q ∈ Q_tm M"
and read: "ts (0 :: nat) (n 0) ≠ LE_block (le_tm M)"
and bt: "∀j≥k_tm M. ∀i. ts j i = bl_block (bl_tm M)"
and stage_tail: "(∀j≥k_tm M. ofs j = init_offset j)
∧ (∀j≥k_tm M. buf j = init_buffer (le_tm M) j)
∧ (∀j≥k_tm M. dest j = init_dest j)"
and gamma: "∀k. ts k (n k) ∈ gamma_block (Γ_tm M)"
and buf_gamma: "∀k. fst (buf k) ∈ gamma_block (Γ_tm M)
∧ fst (snd (buf k)) ∈ gamma_block (Γ_tm M)
∧ snd (snd (buf k)) ∈ gamma_block (Γ_tm M)"
shows "(Config⇩M (q, ofs, buf, dest, VRet) ts n,
Config⇩M (q, ofs, buf, dest, VRet) ts
(λk. go_dir (if k = 0 then dir.L else dir.N) (n k)))
∈ mttm_step (alphabet_enlarge_delta M)"
proof -
let ?d = "λk :: nat. if k = 0 then dir.L else dir.N"
let ?a = "λk. ts k (n k)"
have rel_in: "((q, ofs, buf, dest, VRet), ?a,
(q, ofs, buf, dest, VRet), ?a, ?d)
∈ ae_delta_val_ret_step M"
unfolding ae_delta_val_ret_step_def
using q_in read bt by auto
have src_valid: "ae_valid_stage (Γ_tm M) (le_tm M) (k_tm M)
(snd ((q, ofs, buf, dest, VRet)
:: 'q × ('a, 'c) ae_stage))"
using buf_gamma stage_tail unfolding ae_valid_stage_def by simp
have aed_in: "((q, ofs, buf, dest, VRet), ?a,
(q, ofs, buf, dest, VRet), ?a, ?d)
∈ alphabet_enlarge_delta M"
unfolding alphabet_enlarge_delta_def
using rel_in gamma src_valid by auto
have ts_unchanged: "(λk. (ts k)(n k := ?a k)) = ts"
by (rule ext) auto
have step: "(Config⇩M (q, ofs, buf, dest, VRet) ts n,
Config⇩M (q, ofs, buf, dest, VRet)
(λk. (ts k)(n k := ?a k))
(λk. go_dir (?d k) (n k)))
∈ mttm_step (alphabet_enlarge_delta M)"
proof (rule ae_step_make)
show "((q, ofs, buf, dest, VRet), ?a,
(q, ofs, buf, dest, VRet), ?a, ?d)
∈ alphabet_enlarge_delta M" by (rule aed_in)
qed
show ?thesis using step ts_unchanged by simp
qed
text ‹VRet ‹→› Sim: read ‹LE_block le_M› on tape 0
(return scan reached position 0); N moves uniformly (head
stays); phase becomes Sim with ‹substep_idx› = SS1.›
lemma ae_step_val_ret_to_sim:
fixes M :: "('q, 'a) mttm"
and ts :: "nat ⇒ nat ⇒ ('c :: enum ⇒ 'a)"
and n :: "nat ⇒ nat"
and q :: 'q
and ofs :: "nat ⇒ 'c"
and buf :: "nat ⇒ ('c ⇒ 'a) × ('c ⇒ 'a) × ('c ⇒ 'a)"
and dest :: "nat ⇒ ae_dest"
assumes q_in: "q ∈ Q_tm M"
and read: "ts (0 :: nat) (n 0) = LE_block (le_tm M)"
and bt: "∀j≥k_tm M. ∀i. ts j i = bl_block (bl_tm M)"
and stage_tail: "(∀j≥k_tm M. ofs j = init_offset j)
∧ (∀j≥k_tm M. buf j = init_buffer (le_tm M) j)
∧ (∀j≥k_tm M. dest j = init_dest j)"
and gamma: "∀k. ts k (n k) ∈ gamma_block (Γ_tm M)"
and buf_gamma: "∀k. fst (buf k) ∈ gamma_block (Γ_tm M)
∧ fst (snd (buf k)) ∈ gamma_block (Γ_tm M)
∧ snd (snd (buf k)) ∈ gamma_block (Γ_tm M)"
shows "(Config⇩M (q, ofs, buf, dest, VRet) ts n,
Config⇩M (q, ofs, buf, dest, SS1) ts n)
∈ mttm_step (alphabet_enlarge_delta M)"
proof -
let ?d = "λ_ :: nat. dir.N"
let ?a = "λk. ts k (n k)"
have rel_in: "((q, ofs, buf, dest, VRet), ?a,
(q, ofs, buf, dest, SS1), ?a, ?d)
∈ ae_delta_val_ret_to_sim M"
unfolding ae_delta_val_ret_to_sim_def
using q_in read bt by auto
have src_valid: "ae_valid_stage (Γ_tm M) (le_tm M) (k_tm M)
(snd ((q, ofs, buf, dest, VRet)
:: 'q × ('a, 'c) ae_stage))"
using buf_gamma stage_tail unfolding ae_valid_stage_def by simp
have dst_valid: "ae_valid_stage (Γ_tm M) (le_tm M) (k_tm M)
(snd ((q, ofs, buf, dest, SS1)
:: 'q × ('a, 'c) ae_stage))"
using buf_gamma stage_tail unfolding ae_valid_stage_def by simp
have aed_in: "((q, ofs, buf, dest, VRet), ?a,
(q, ofs, buf, dest, SS1), ?a, ?d)
∈ alphabet_enlarge_delta M"
unfolding alphabet_enlarge_delta_def
using rel_in gamma src_valid dst_valid by auto
have ts_unchanged: "(λk. (ts k)(n k := ?a k)) = ts"
by (rule ext) auto
have n_unchanged: "(λk :: nat. go_dir (?d k) (n k)) = n"
by (rule ext) simp
have step: "(Config⇩M (q, ofs, buf, dest, VRet) ts n,
Config⇩M (q, ofs, buf, dest, SS1)
(λk. (ts k)(n k := ?a k))
(λk. go_dir (?d k) (n k)))
∈ mttm_step (alphabet_enlarge_delta M)"
proof (rule ae_step_make)
show "((q, ofs, buf, dest, VRet), ?a,
(q, ofs, buf, dest, SS1), ?a, ?d)
∈ alphabet_enlarge_delta M" by (rule aed_in)
qed
show ?thesis using step ts_unchanged n_unchanged by simp
qed
text ‹VFwd reject: read a non-canonical block on tape 0
(in ‹Σ'› but neither pure nor padded — blanks in
non-trailing positions); N moves uniformly; transition to
‹(r_M, init_stage le_M)›.›
lemma ae_step_val_fwd_reject:
fixes M :: "('q, 'a) mttm"
and ts :: "nat ⇒ nat ⇒ ('c :: enum ⇒ 'a)"
and n :: "nat ⇒ nat"
and q :: '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 q_in: "q ∈ Q_tm M"
and q_neq_t: "q ≠ t_tm M"
and q_neq_r: "q ≠ r_tm M"
and read_nle: "ts (0 :: nat) (n 0) ≠ LE_block (le_tm M)"
and read_nbl: "ts (0 :: nat) (n 0) ≠ bl_block (bl_tm M)"
and read_ncan: "¬ is_canonical_block (bl_tm M) (ts (0 :: nat) (n 0))"
and bt: "∀j≥k_tm M. ∀i. ts j i = bl_block (bl_tm M)"
and stage_tail: "(∀j≥k_tm M. ofs j = init_offset j)
∧ (∀j≥k_tm M. buf j = init_buffer (le_tm M) j)
∧ (∀j≥k_tm M. dest j = init_dest j)"
and gamma: "∀k. ts k (n k) ∈ gamma_block (Γ_tm M)"
and buf_gamma: "∀k. fst (buf k) ∈ gamma_block (Γ_tm M)
∧ fst (snd (buf k)) ∈ gamma_block (Γ_tm M)
∧ snd (snd (buf k)) ∈ gamma_block (Γ_tm M)"
shows "(Config⇩M (q, ofs, buf, dest, VFwd) ts n,
Config⇩M (r_tm M, init_stage (le_tm M)) ts n)
∈ mttm_step (alphabet_enlarge_delta M)"
proof -
let ?d = "λ_ :: nat. dir.N"
let ?a = "λk. ts k (n k)"
have rel_in: "((q, ofs, buf, dest, VFwd), ?a,
(r_tm M, init_stage (le_tm M)), ?a, ?d)
∈ ae_delta_val_fwd_reject M"
unfolding ae_delta_val_fwd_reject_def
using q_in q_neq_t q_neq_r read_nle read_nbl read_ncan bt by auto
have src_valid: "ae_valid_stage (Γ_tm M) (le_tm M) (k_tm M)
(snd ((q, ofs, buf, dest, VFwd)
:: 'q × ('a, 'c) ae_stage))"
using buf_gamma stage_tail unfolding ae_valid_stage_def by simp
have dst_valid: "ae_valid_stage (Γ_tm M) (le_tm M) (k_tm M)
(snd ((r_tm M, init_stage (le_tm M))
:: 'q × ('a, 'c) ae_stage))"
using ae_valid_stage_init[OF valid_mttm_LE_in_Gamma[OF vM]] by simp
have aed_in: "((q, ofs, buf, dest, VFwd), ?a,
(r_tm M, init_stage (le_tm M)), ?a, ?d)
∈ alphabet_enlarge_delta M"
unfolding alphabet_enlarge_delta_def
using rel_in gamma src_valid dst_valid by auto
have ts_unchanged: "(λk. (ts k)(n k := ?a k)) = ts"
by (rule ext) auto
have n_unchanged: "(λk :: nat. go_dir (?d k) (n k)) = n"
by (rule ext) simp
have step: "(Config⇩M (q, ofs, buf, dest, VFwd) ts n,
Config⇩M (r_tm M, init_stage (le_tm M))
(λk. (ts k)(n k := ?a k))
(λk. go_dir (?d k) (n k)))
∈ mttm_step (alphabet_enlarge_delta M)"
proof (rule ae_step_make)
show "((q, ofs, buf, dest, VFwd), ?a,
(r_tm M, init_stage (le_tm M)), ?a, ?d)
∈ alphabet_enlarge_delta M" by (rule aed_in)
qed
show ?thesis using step ts_unchanged n_unchanged by simp
qed
text ‹VFwdPad reject: read anything on tape 0 other than
‹bl_block bl_M› (a non-blank block after the
trailing-padded one); N moves; transition to
‹(r_M, init_stage le_M)›.›
lemma ae_step_val_pad_reject:
fixes M :: "('q, 'a) mttm"
and ts :: "nat ⇒ nat ⇒ ('c :: enum ⇒ 'a)"
and n :: "nat ⇒ nat"
and q :: '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 q_in: "q ∈ Q_tm M"
and read: "ts (0 :: nat) (n 0) ≠ bl_block (bl_tm M)"
and bt: "∀j≥k_tm M. ∀i. ts j i = bl_block (bl_tm M)"
and stage_tail: "(∀j≥k_tm M. ofs j = init_offset j)
∧ (∀j≥k_tm M. buf j = init_buffer (le_tm M) j)
∧ (∀j≥k_tm M. dest j = init_dest j)"
and gamma: "∀k. ts k (n k) ∈ gamma_block (Γ_tm M)"
and buf_gamma: "∀k. fst (buf k) ∈ gamma_block (Γ_tm M)
∧ fst (snd (buf k)) ∈ gamma_block (Γ_tm M)
∧ snd (snd (buf k)) ∈ gamma_block (Γ_tm M)"
shows "(Config⇩M (q, ofs, buf, dest, VFwdPad) ts n,
Config⇩M (r_tm M, init_stage (le_tm M)) ts n)
∈ mttm_step (alphabet_enlarge_delta M)"
proof -
let ?d = "λ_ :: nat. dir.N"
let ?a = "λk. ts k (n k)"
have rel_in: "((q, ofs, buf, dest, VFwdPad), ?a,
(r_tm M, init_stage (le_tm M)), ?a, ?d)
∈ ae_delta_val_pad_reject M"
unfolding ae_delta_val_pad_reject_def
using q_in read bt by auto
have src_valid: "ae_valid_stage (Γ_tm M) (le_tm M) (k_tm M)
(snd ((q, ofs, buf, dest, VFwdPad)
:: 'q × ('a, 'c) ae_stage))"
using buf_gamma stage_tail unfolding ae_valid_stage_def by simp
have dst_valid: "ae_valid_stage (Γ_tm M) (le_tm M) (k_tm M)
(snd ((r_tm M, init_stage (le_tm M))
:: 'q × ('a, 'c) ae_stage))"
using ae_valid_stage_init[OF valid_mttm_LE_in_Gamma[OF vM]] by simp
have aed_in: "((q, ofs, buf, dest, VFwdPad), ?a,
(r_tm M, init_stage (le_tm M)), ?a, ?d)
∈ alphabet_enlarge_delta M"
unfolding alphabet_enlarge_delta_def
using rel_in gamma src_valid dst_valid by auto
have ts_unchanged: "(λk. (ts k)(n k := ?a k)) = ts"
by (rule ext) auto
have n_unchanged: "(λk :: nat. go_dir (?d k) (n k)) = n"
by (rule ext) simp
have step: "(Config⇩M (q, ofs, buf, dest, VFwdPad) ts n,
Config⇩M (r_tm M, init_stage (le_tm M))
(λk. (ts k)(n k := ?a k))
(λk. go_dir (?d k) (n k)))
∈ mttm_step (alphabet_enlarge_delta M)"
proof (rule ae_step_make)
show "((q, ofs, buf, dest, VFwdPad), ?a,
(r_tm M, init_stage (le_tm M)), ?a, ?d)
∈ alphabet_enlarge_delta M" by (rule aed_in)
qed
show ?thesis using step ts_unchanged n_unchanged by simp
qed
subsubsection ‹Initial-config shape and gamma-block›
text ‹Shape lookups for ‹ae_init_config›. These give the tape
contents at named positions — LE at position 0, input blocks
at positions ‹1…length w›, blank-block elsewhere — and the
uniform state / head shape. Used pervasively by the validation
chain proofs; trivial unfoldings of ‹ae_init_config_def›.›
lemma ae_init_config_state:
"mt_state (ae_init_config M w) = (s_tm M, init_stage (le_tm M))"
unfolding ae_init_config_def by simp
lemma ae_init_config_pos:
"mt_pos (ae_init_config M w) k = 0"
unfolding ae_init_config_def by simp
lemma ae_init_config_tape_le:
assumes "k < k_tm M"
shows "mt_tape (ae_init_config M w) k 0 = LE_block (le_tm M)"
using assms unfolding ae_init_config_def by simp
lemma ae_init_config_tape_input:
assumes "1 ≤ p" and "p ≤ length w" and "0 < k_tm M"
shows "mt_tape (ae_init_config M w) 0 p = w ! (p - 1)"
using assms unfolding ae_init_config_def by simp
lemma ae_init_config_tape_blank_after_input:
assumes "p > length w"
shows "mt_tape (ae_init_config M w) 0 p = bl_block (bl_tm M)"
using assms unfolding ae_init_config_def by simp
lemma ae_init_config_tape_other:
assumes "k ≠ 0" and "p > 0"
shows "mt_tape (ae_init_config M w) k p = bl_block (bl_tm M)"
using assms unfolding ae_init_config_def by simp
text ‹Blank-tail of the initial configuration: every cell of every
inactive tape (index ‹≥ k_tm M›) holds the blank block.
This is the value-level support condition the substrate's
‹init_config_mttm› imposes on ‹alphabet_enlarge M›; it discharges
the ‹∀j≥k_tm M. ts j (n j) = bl_block (bl_tm M)› premise of every
validation step-helper (the tape is never written during
validation, so ‹ts = mt_tape (ae_init_config M w)› throughout).›
lemma ae_init_config_tape_blank_tail:
assumes "k_tm M ≤ k"
shows "mt_tape (ae_init_config M w) k p = bl_block (bl_tm M)"
using assms unfolding ae_init_config_def by simp
text ‹Gamma-block membership of every tape cell of the initial
configuration. Uniformly discharges the
‹∀k. ts k (n k) ∈ gamma_block (Γ_tm M)› premise of every
validation step-helper, regardless of the head position ‹n›
reached during the chain.›
lemma ae_init_config_in_gamma_block:
fixes M :: "('q, 'a) mttm"
and w :: "(('c :: enum) ⇒ 'a) list"
assumes vM: "valid_mttm M"
and w_sub: "set w ⊆ gamma_block (Sigma_tm M ∪ {bl_tm M})"
shows "mt_tape (ae_init_config M w) k p ∈ gamma_block (Γ_tm M)"
proof -
have bl_in: "bl_tm M ∈ Γ_tm M"
by (rule valid_mttm_blank_in_Gamma[OF vM])
have le_in: "le_tm M ∈ Γ_tm M"
by (rule valid_mttm_LE_in_Gamma[OF vM])
have Sigma_sub: "Sigma_tm M ⊆ Γ_tm M"
by (rule valid_mttm_Sigma_sub_Gamma[OF vM])
have sub: "Sigma_tm M ∪ {bl_tm M} ⊆ Γ_tm M"
using Sigma_sub bl_in by auto
have w_sub_G: "set w ⊆ gamma_block (Γ_tm M)"
using w_sub gamma_block_mono[OF sub] by blast
have kpos: "0 < k_tm M" by (rule valid_mttm_k_pos[OF vM])
consider
(zero_act) "p = 0" and "k < k_tm M"
| (zero_inact) "p = 0" and "¬ k < k_tm M"
| (input) "p ≠ 0" and "k = 0" and "p ≤ length w"
| (blank) "p ≠ 0" and "¬ (k = 0 ∧ p ≤ length w)"
by blast
thus ?thesis
proof cases
case zero_act
have "mt_tape (ae_init_config M w) k p = LE_block (le_tm M)"
using zero_act ae_init_config_tape_le by simp
thus ?thesis using LE_block_in_gamma_block[OF le_in] by simp
next
case zero_inact
have "mt_tape (ae_init_config M w) k p = bl_block (bl_tm M)"
using zero_inact unfolding ae_init_config_def by simp
thus ?thesis using bl_block_in_gamma_block[OF bl_in] by simp
next
case input
have "mt_tape (ae_init_config M w) k p = w ! (p - 1)"
using input kpos ae_init_config_tape_input[of p w M] by simp
moreover have "w ! (p - 1) ∈ set w"
using input by auto
ultimately show ?thesis using w_sub_G by auto
next
case blank
have "mt_tape (ae_init_config M w) k p = bl_block (bl_tm M)"
using blank unfolding ae_init_config_def by auto
thus ?thesis using bl_block_in_gamma_block[OF bl_in] by simp
qed
qed
end