Theory Wrap_Language
theory Wrap_Language
imports Wrap_Canonical
begin
section ‹Faithful (k-tape) plant-‹le› wrap: language preservation›
text ‹The user-facing language of the faithful plant-‹le› wrap equals the
encoded-input language of M: @{term "Lang_user_wrap (encoding_wrap M pack c
Σu) = {w. set w ⊆ Σu ∧ wrap_enc pack c w ∈ Lang_mttm M}"}. As with the
transpose wrap this is mutual inclusion of accepting languages (two one-way
trace arguments; not a bisimulation, since @{term M} is nondeterministic).
The ∗‹reverse› inclusion (M-acceptance of the encoded input gives
wrap-acceptance) differs from the transpose at the reset‹→›run seam. Where
the transpose rewinds all the way to the true origin and hands the run the
genuine @{const lift_M_config}, the plant wrap stops at the ∗‹floated›
configuration @{const post_plant_dispatch_config} --- no input rewind, a fresh
@{text le} planted at the reused input head. The origin-float bridge
reconciles the two: the M-run lifts (via @{thm[source] run_steps_forward_relpow})
to a run from the @{text τ}-lift, and @{thm[source] shift_reach_state_forward}
--- instantiated at the wrap machine itself --- re-bases that run onto the
floated config the plant reset actually reaches, preserving the accept state.›
subsection ‹Reverse inclusion: chaining the phases through the floated origin›
lemma wrap_language_reverse:
assumes vM: "valid_mttm M"
and fin_Sigmau: "finite Σu"
and c_pos: "0 < c"
and bl_ne_le: "bl_tm M ≠ le_tm M"
and k2: "2 ≤ k_tm M"
shows "{w. set w ⊆ Σu ∧ wrap_enc pack c w ∈ Lang_mttm M}
⊆ Lang_user_wrap (encoding_wrap M pack c Σu)"
proof
fix w
assume "w ∈ {w. set w ⊆ Σu ∧ wrap_enc pack c w ∈ Lang_mttm M}"
hence w_alpha: "set w ⊆ Σu"
and enc_lang: "wrap_enc pack c w ∈ Lang_mttm M"
by auto
from enc_lang have enc_in_Sigma: "set (wrap_enc pack c w) ⊆ Sigma_tm M"
by (simp add: Lang_mttm_def)
from enc_lang obtain w_ts cf_pos where M_trace:
"(init_config_mttm M (wrap_enc pack c w),
Config⇩M (t_tm M) w_ts cf_pos)
∈ (mttm_step (delta_tm M))⇧*"
by (auto simp: Lang_mttm_def)
let ?W = "encoding_wrap M pack c Σu"
let ?init_M = "init_config_mttm M (wrap_enc pack c w)"
let ?cf_M = "Config⇩M (t_tm M) w_ts cf_pos"
let ?R_W = "mttm_step (wrap_delta M pack c Σu)"
let ?d = "λp::nat. if p = 0 then length w + 1 else 0"
obtain Q Σi Γset bl le δM sM tM rM kM where M_eq:
"M = MTTM Q Σi Γset bl le δM sM tM rM kM"
by (cases M)
have Sigma_sub_Γ: "Sigma_tm M ⊆ Γ_tm M" using vM M_eq by auto
have le_not_in_Sigma: "le_tm M ∉ Sigma_tm M" using vM M_eq by auto
have pack_in_Sigma:
"⋀i. i * c < length w ⟹ pack (take c (drop (i * c) w)) ∈ Sigma_tm M"
proof -
fix i :: nat
assume i_c_lt: "i * c < length w"
have "pack (take c (drop (i * c) w)) ∈ set (wrap_enc pack c w)"
by (rule pack_take_in_set_wrap_enc[OF c_pos i_c_lt])
thus "pack (take c (drop (i * c) w)) ∈ Sigma_tm M"
using enc_in_Sigma by auto
qed
have pack_in:
"⋀i. i * c < length w ⟹ pack (take c (drop (i * c) w)) ∈ Γ_tm M"
proof -
fix i :: nat
assume i_c_lt: "i * c < length w"
from pack_in_Sigma[OF i_c_lt] Sigma_sub_Γ
show "pack (take c (drop (i * c) w)) ∈ Γ_tm M" by auto
qed
have pack_ne_le:
"⋀i. i * c < length w ⟹ pack (take c (drop (i * c) w)) ≠ le_tm M"
proof -
fix i :: nat
assume i_c_lt: "i * c < length w"
from pack_in_Sigma[OF i_c_lt] le_not_in_Sigma
show "pack (take c (drop (i * c) w)) ≠ le_tm M" by auto
qed
have enc_step:
"(init_config_mttm ?W (map Raw w),
post_encoder_config_gen (k_tm M) M pack c w) ∈ ?R_W⇧*"
by (rule encoder_phase_terminates
[where pack = pack, OF vM c_pos w_alpha bl_ne_le k2 pack_in_Sigma])
have pr_step:
"(post_encoder_config_gen (k_tm M) M pack c w,
post_plant_dispatch_config M pack c w) ∈ ?R_W⇧*"
by (rule plant_reset_dispatch_rtrancl
[where pack = pack, OF vM c_pos w_alpha bl_ne_le k2 pack_in pack_ne_le])
have val_init_M: "valid_config_mttm M ?init_M"
by (rule valid_init_config_mttm[OF vM enc_in_Sigma])
from M_trace obtain n where M_trace_n:
"(?init_M, ?cf_M) ∈ (mttm_step (delta_tm M)) ^^ n"
by (auto simp: rtrancl_power)
have run_relpow:
"(lift_M_config M ?init_M, lift_M_config M ?cf_M) ∈ ?R_W ^^ n"
by (rule run_steps_forward_relpow[OF vM k2 val_init_M M_trace_n])
have wf_wrap: "valid_mttm ?W"
by (rule wrap_wf[OF vM bl_ne_le[THEN not_sym] fin_Sigmau c_pos k2])
have shift:
"shift_rel ?d (lift_M_config M ?init_M)
(post_plant_dispatch_config M pack c w)"
by (rule post_plant_dispatch_shift_lift[OF k2])
have wrap_delta_eq: "delta_tm ?W = wrap_delta M pack c Σu"
by simp
have suc0_lt: "Suc 0 < k_tm M" using k2 by simp
have le0:
"∀k. ?d k ≠ 0 ⟶ mt_tape (lift_M_config M ?init_M) k 0 = le_tm ?W"
proof (intro allI impI)
fix k :: nat
assume "?d k ≠ 0"
hence k0: "k = 0" by (auto split: if_splits)
have "mt_tape (lift_M_config M ?init_M) 0 0
= Enc (mt_tape ?init_M (wrap_tau 0) 0)"
using k2 by (simp add: lift_M_config_def)
also have "… = Enc (mt_tape ?init_M (Suc 0) 0)"
by (simp add: wrap_tau_def)
also have "mt_tape ?init_M (Suc 0) 0 = le_tm M"
using suc0_lt by (simp add: M_eq)
finally show "mt_tape (lift_M_config M ?init_M) k 0 = le_tm ?W"
using k0 by simp
qed
have acc_lift: "mt_state (lift_M_config M ?cf_M) = W_Run (t_tm M)"
by (simp add: lift_M_config_def)
have run_relpow':
"(lift_M_config M ?init_M, lift_M_config M ?cf_M)
∈ (mttm_step (delta_tm ?W)) ^^ n"
using run_relpow wrap_delta_eq by simp
from shift_reach_state_forward[OF wf_wrap le0 shift run_relpow' acc_lift]
obtain cb where cb_run:
"(post_plant_dispatch_config M pack c w, cb)
∈ (mttm_step (delta_tm ?W)) ^^ n"
and cb_state: "mt_state cb = W_Run (t_tm M)"
by blast
have cb_run_R: "(post_plant_dispatch_config M pack c w, cb) ∈ ?R_W ^^ n"
using cb_run wrap_delta_eq by simp
have cb_run_rtrancl: "(post_plant_dispatch_config M pack c w, cb) ∈ ?R_W⇧*"
by (rule relpow_imp_rtrancl[OF cb_run_R])
from enc_step pr_step have er_step:
"(init_config_mttm ?W (map Raw w),
post_plant_dispatch_config M pack c w) ∈ ?R_W⇧*"
by (rule rtrancl_trans)
from er_step cb_run_rtrancl have full_trace:
"(init_config_mttm ?W (map Raw w), cb) ∈ ?R_W⇧*"
by (rule rtrancl_trans)
obtain cb_ts cb_n where cb_eq:
"cb = Config⇩M (t_tm ?W) cb_ts cb_n"
proof -
have "t_tm ?W = W_Run (t_tm M)" by simp
hence "cb = Config⇩M (t_tm ?W) (mt_tape cb) (mt_pos cb)"
using cb_state by (cases cb) simp
thus thesis by (rule that)
qed
from full_trace cb_eq have accept_trace:
"(init_config_mttm ?W (map Raw w),
Config⇩M (t_tm ?W) cb_ts cb_n) ∈ ?R_W⇧*"
by simp
have set_Raw_w: "set (map Raw w) ⊆ Sigma_tm ?W"
using w_alpha by auto
show "w ∈ Lang_user_wrap ?W"
unfolding Lang_user_wrap_def Lang_mttm_def
using set_Raw_w accept_trace wrap_delta_eq by auto
qed
subsection ‹Forward inclusion: factoring through the floated origin›
text ‹The forward inclusion: wrap-B acceptance of @{term "map Raw w"} gives
M-acceptance of @{term "wrap_enc pack c w"}. The accepting wrap-trace factors
via @{thm[source] wrap_accept_canonical_factor} (reaching the ∗‹floated›
@{const post_plant_dispatch_config}), then the origin float runs in reverse:
@{thm[source] shift_reach_state_reverse} re-bases the run-phase tail from the
floated config to the @{text τ}-lift, and @{thm[source] run_steps_reverse}
projects it to an accepting M-trace on @{term "wrap_enc pack c w"}.›
lemma wrap_language_forward:
fixes M :: "('q, 'b) mttm"
assumes vM: "valid_mttm M"
and fin_Sigmau: "finite Σu"
and c_pos: "0 < c"
and bl_ne_le: "bl_tm M ≠ le_tm M"
and k2: "2 ≤ k_tm M"
shows "Lang_user_wrap (encoding_wrap M pack c Σu)
⊆ {w. set w ⊆ Σu ∧ wrap_enc pack c w ∈ Lang_mttm M}"
proof
fix w
assume mem: "w ∈ Lang_user_wrap (encoding_wrap M pack c Σu)"
hence raw_w_lang:
"map Raw w ∈ Lang_mttm (encoding_wrap M pack c Σu)"
unfolding Lang_user_wrap_def by simp
have w_alpha: "set w ⊆ Σu"
proof
fix x assume x_in: "x ∈ set w"
hence raw_x_in: "Raw x ∈ set (map Raw w)" by simp
from raw_w_lang have map_raw_in:
"set (map Raw w) ⊆ Raw ` Σu"
unfolding Lang_mttm_def by auto
from raw_x_in map_raw_in have "Raw x ∈ Raw ` Σu" by blast
thus "x ∈ Σu" by auto
qed
let ?W = "encoding_wrap M pack c Σu"
let ?R_W = "mttm_step (wrap_delta M pack c Σu)"
let ?init_M = "init_config_mttm M (wrap_enc pack c w)"
let ?d = "λp::nat. if p = 0 then length w + 1 else 0"
from raw_w_lang obtain w_ts cf_pos where wrap_trace_raw:
"(init_config_mttm ?W (map Raw w),
Config⇩M (t_tm ?W) w_ts cf_pos)
∈ (mttm_step (delta_tm ?W))⇧*"
unfolding Lang_mttm_def by auto
let ?C_acc = "Config⇩M (W_Run (t_tm M)) w_ts cf_pos"
have wrap_trace:
"(init_config_mttm ?W (map Raw w), ?C_acc) ∈ ?R_W⇧*"
using wrap_trace_raw by simp
have accept_state: "∃q. mt_state ?C_acc = W_Run q" by simp
from wrap_accept_canonical_factor
[OF vM c_pos bl_ne_le w_alpha k2 wrap_trace accept_state]
have suffix:
"(post_plant_dispatch_config M pack c w, ?C_acc) ∈ ?R_W⇧*"
and pack_in_Sigma:
"⋀i. i * c < length w ⟹ pack (take c (drop (i * c) w)) ∈ Sigma_tm M"
by auto
have enc_in_Sigma: "set (wrap_enc pack c w) ⊆ Sigma_tm M"
proof
fix x
assume "x ∈ set (wrap_enc pack c w)"
then obtain j where j_lt: "j < length (wrap_enc pack c w)"
and x_eq: "x = wrap_enc pack c w ! j"
by (auto simp: in_set_conv_nth)
from wrap_enc_in_Sigma[OF c_pos pack_in_Sigma j_lt]
show "x ∈ Sigma_tm M" using x_eq by simp
qed
have val_init_M: "valid_config_mttm M ?init_M"
by (rule valid_init_config_mttm[OF vM enc_in_Sigma])
have wf_wrap: "valid_mttm ?W"
by (rule wrap_wf[OF vM bl_ne_le[THEN not_sym] fin_Sigmau c_pos k2])
have shift:
"shift_rel ?d (lift_M_config M ?init_M)
(post_plant_dispatch_config M pack c w)"
by (rule post_plant_dispatch_shift_lift[OF k2])
have wrap_delta_eq: "delta_tm ?W = wrap_delta M pack c Σu"
by simp
obtain Q Σi Γset bl le δM sM tM rM kM where M_eq:
"M = MTTM Q Σi Γset bl le δM sM tM rM kM"
by (cases M)
have suc0_lt: "Suc 0 < k_tm M" using k2 by simp
have le0:
"∀k. ?d k ≠ 0 ⟶ mt_tape (lift_M_config M ?init_M) k 0 = le_tm ?W"
proof (intro allI impI)
fix k :: nat
assume "?d k ≠ 0"
hence k0: "k = 0" by (auto split: if_splits)
have "mt_tape (lift_M_config M ?init_M) 0 0
= Enc (mt_tape ?init_M (wrap_tau 0) 0)"
using k2 by (simp add: lift_M_config_def)
also have "… = Enc (mt_tape ?init_M (Suc 0) 0)"
by (simp add: wrap_tau_def)
also have "mt_tape ?init_M (Suc 0) 0 = le_tm M"
using suc0_lt by (simp add: M_eq)
finally show "mt_tape (lift_M_config M ?init_M) k 0 = le_tm ?W"
using k0 by simp
qed
from suffix obtain n where suffix_n:
"(post_plant_dispatch_config M pack c w, ?C_acc) ∈ ?R_W ^^ n"
by (auto simp: rtrancl_power)
have suffix_n':
"(post_plant_dispatch_config M pack c w, ?C_acc)
∈ (mttm_step (delta_tm ?W)) ^^ n"
using suffix_n wrap_delta_eq by simp
have acc_state: "mt_state ?C_acc = W_Run (t_tm M)" by simp
from shift_reach_state_reverse[OF wf_wrap le0 shift suffix_n' acc_state]
obtain ca where ca_run:
"(lift_M_config M ?init_M, ca) ∈ (mttm_step (delta_tm ?W)) ^^ n"
and ca_state: "mt_state ca = W_Run (t_tm M)"
by blast
have ca_run_rt: "(lift_M_config M ?init_M, ca) ∈ ?R_W⇧*"
proof -
have "(lift_M_config M ?init_M, ca) ∈ ?R_W ^^ n"
using ca_run wrap_delta_eq by simp
thus ?thesis by (rule relpow_imp_rtrancl)
qed
from run_steps_reverse[OF vM k2 val_init_M ca_run_rt]
obtain cM_acc where
ca_lift: "ca = lift_M_config M cM_acc"
and M_trace_acc: "(?init_M, cM_acc) ∈ (mttm_step (delta_tm M))⇧*"
by blast
obtain cM_q cM_ts cM_n where cM_decomp:
"cM_acc = Config⇩M cM_q cM_ts cM_n"
by (cases cM_acc)
with ca_lift have lift_state_eq:
"mt_state ca = W_Run cM_q"
by (simp add: lift_M_config_def)
with ca_state have cM_q_eq: "cM_q = t_tm M" by simp
have enc_lang: "wrap_enc pack c w ∈ Lang_mttm M"
unfolding Lang_mttm_def
using enc_in_Sigma M_trace_acc cM_decomp cM_q_eq
by auto
show "w ∈ {w. set w ⊆ Σu ∧ wrap_enc pack c w ∈ Lang_mttm M}"
using w_alpha enc_lang by simp
qed
subsection ‹Language equality headline›
text ‹The user-facing language of the faithful @{text k}-tape plant-‹le› wrap
equals the encoded-input language of M --- both inclusions, spliced through the
origin float in opposite directions.›
lemma wrap_language:
assumes "valid_mttm M"
and "finite Σu"
and "0 < c"
and "bl_tm M ≠ le_tm M"
and "2 ≤ k_tm M"
shows "Lang_user_wrap (encoding_wrap M pack c Σu)
= {w. set w ⊆ Σu ∧ wrap_enc pack c w ∈ Lang_mttm M}"
using wrap_language_forward[OF assms] wrap_language_reverse[OF assms]
by blast
end