Theory Wrap_Reset
theory Wrap_Reset
imports Wrap_Defs
begin
section ‹Faithful (k-tape) plant-‹le› wrap: reset threading and the origin float›
text ‹The plant wrap's reset differs from a combined blank-and-rewind reset
in that it
∗‹does not› walk the input tape (physical @{text 0}) back to its @{text le}.
It rewinds only the storage tape (physical @{text 1}, carrying M's tape
@{text 0} = the encoded input) --- the @{text "⌈n/c⌉"} cells that make
up the @{text "ε⋅n"} term --- freezing the input head at
@{term "length w + 1"} throughout. When the storage head reaches its
@{text le} at cell @{text 0}, the plant-done step writes a fresh @{text le}
on the input tape at the frozen head and hands to @{text W_Disp}.
The resulting engine configuration is the input tape ∗‹floated›: physical
tape @{text 0} carries a planted @{text le} at cell @{term "length w + 1"}
with the spent raw input as an unreachable prefix below it, and blanks
above --- indistinguishable, from the engine's position-agnostic view,
from a fresh blank work tape whose origin sits at @{term "length w + 1"}.
This is exactly a @{const shift_rel} by @{term "length w + 1"} of the
@{text τ}-lift of M's initial configuration, so the origin-float lemmas
of @{theory Multitape_TM_Substrate.Multitape_Origin_Float} bridge the floated run back
to the proper @{const init_config_mttm} the transpose run machinery
consumes.›
subsection ‹The storage-tape rewind, input head frozen›
text ‹One generic-rewind step retracts the storage head (physical
@{text "Suc 0"}) from @{term "Suc m1"} to @{term m1}, the input head frozen
at @{term "length w + 1"} and every tape's content preserved. This reuses
@{const mid_reset_combined_config_gen} with the input head @{term m0} pinned
at @{term "length w + 1"}: since that config only blanks cells @{text "> m0"}
and @{term "length w + 1 > length w"}, the raw input stays intact and the
configuration depends on the storage head @{term m1} only through its
position.›
lemma mid_plant_rewind_step:
assumes vM: "valid_mttm M"
and c_pos: "0 < c"
and w_alpha: "set w ⊆ Σu"
and bl_ne_le: "bl_tm M ≠ le_tm M"
and k2: "2 ≤ k_tm M"
and pack_in:
"⋀i. i * c < length w ⟹ pack (take c (drop (i * c) w)) ∈ Γ_tm M"
and pack_ne_le:
"⋀i. i * c < length w ⟹ pack (take c (drop (i * c) w)) ≠ le_tm M"
shows "(mid_reset_combined_config_gen (k_tm M) M pack c w (length w + 1) (Suc m1),
mid_reset_combined_config_gen (k_tm M) M pack c w (length w + 1) m1)
∈ mttm_step (wrap_delta M pack c Σu)"
proof -
let ?src = "mid_reset_combined_config_gen (k_tm M) M pack c w (length w + 1) (Suc m1)"
let ?L = "length (wrap_enc pack c w)"
let ?sym = "λk. mt_tape ?src k (mt_pos ?src k)"
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 kpos: "0 < k_tm M" using k2 by simp
have src_state: "mt_state ?src = W_Reset"
by (simp add: mid_reset_combined_config_gen_def)
have src_eq: "?src = Config⇩M W_Reset (mt_tape ?src) (mt_pos ?src)"
using src_state by (cases ?src) simp
have sym1_ne_le: "?sym (Suc 0) ≠ Enc (le_tm M)"
proof (cases "Suc m1 ≤ ?L")
case True
hence m1_lt_L: "m1 < ?L" by simp
have ne: "wrap_enc pack c w ! m1 ≠ le_tm M"
by (rule wrap_enc_ne_le[OF c_pos pack_ne_le m1_lt_L])
have read: "?sym (Suc 0) = Enc (wrap_enc pack c w ! m1)"
using True k2 by (simp add: mid_reset_combined_config_gen_def split: nat.split)
show ?thesis using read ne by simp
next
case False
have read: "?sym (Suc 0) = Enc (bl_tm M)"
using False k2 by (simp add: mid_reset_combined_config_gen_def split: nat.split)
show ?thesis using read bl_ne_le by simp
qed
have enc_in_Gamma:
"⋀i. i < length (wrap_enc pack c w) ⟹ wrap_enc pack c w ! i ∈ Γ_tm M"
by (rule wrap_enc_in_Gamma[where pack = pack, OF c_pos pack_in])
have wi0: "⋀i. Suc i ≤ length w ⟹ w ! i ∈ Σu"
using w_alpha by (meson Suc_le_eq nth_mem subsetD)
have rd_range: "?sym ∈ UNIV → Raw ` Σu ∪ Enc ` Γ_tm M"
using bl_in le_in enc_in_Gamma wi0
by (auto simp: mid_reset_combined_config_gen_def split: nat.split)
have tail_bl: "∀j≥k_tm M. ?sym j = Enc (bl_tm M)"
by (auto simp: mid_reset_combined_config_gen_def)
let ?dir = "λt. if t = Suc 0 then dir.L else dir.N"
have tuple_in: "(W_Reset, ?sym, W_Reset, ?sym, ?dir) ∈ wrap_delta M pack c Σu"
proof -
have "(W_Reset, ?sym, W_Reset, ?sym, ?dir)
∈ wrap_rewind_loop_delta_gen W_Reset (Suc 0) (k_tm M) M Σu"
unfolding wrap_rewind_loop_delta_gen_def
using sym1_ne_le tail_bl rd_range by blast
thus ?thesis by (simp add: wrap_delta_def)
qed
have step_holds:
"(Config⇩M W_Reset (mt_tape ?src) (mt_pos ?src),
Config⇩M W_Reset
(λk. (mt_tape ?src k)((mt_pos ?src k) := ?sym k))
(λk. go_dir (?dir k) (mt_pos ?src k)))
∈ mttm_step (wrap_delta M pack c Σu)"
by (rule mttm_step.step
[where ts = "mt_tape ?src" and n = "mt_pos ?src" and a = ?sym and dir = ?dir,
OF tuple_in])
have target_eq:
"Config⇩M W_Reset
(λk. (mt_tape ?src k)((mt_pos ?src k) := ?sym k))
(λk. go_dir (?dir k) (mt_pos ?src k))
= mid_reset_combined_config_gen (k_tm M) M pack c w (length w + 1) m1"
by (auto simp: mid_reset_combined_config_gen_def fun_upd_triv fun_eq_iff
split: nat.split)
from step_holds target_eq src_eq show ?thesis by simp
qed
text ‹Iterated: @{term s} storage-rewind steps retract the storage head from
@{term "m1 + s"} to @{term m1}, the input head frozen throughout.›
lemma mid_plant_rewind_iter:
assumes vM: "valid_mttm M"
and c_pos: "0 < c"
and w_alpha: "set w ⊆ Σu"
and bl_ne_le: "bl_tm M ≠ le_tm M"
and k2: "2 ≤ k_tm M"
and pack_in:
"⋀i. i * c < length w ⟹ pack (take c (drop (i * c) w)) ∈ Γ_tm M"
and pack_ne_le:
"⋀i. i * c < length w ⟹ pack (take c (drop (i * c) w)) ≠ le_tm M"
shows "(mid_reset_combined_config_gen (k_tm M) M pack c w (length w + 1) (m1 + s),
mid_reset_combined_config_gen (k_tm M) M pack c w (length w + 1) m1)
∈ (mttm_step (wrap_delta M pack c Σu)) ^^ s"
proof (induction s)
case 0
show ?case by simp
next
case (Suc s)
have step:
"(mid_reset_combined_config_gen (k_tm M) M pack c w (length w + 1) (Suc (m1 + s)),
mid_reset_combined_config_gen (k_tm M) M pack c w (length w + 1) (m1 + s))
∈ mttm_step (wrap_delta M pack c Σu)"
apply (rule mid_plant_rewind_step[OF vM c_pos w_alpha bl_ne_le k2])
apply (fact pack_in)
apply (fact pack_ne_le)
done
from relpow_Suc_I2[OF step Suc.IH]
show ?case by simp
qed
text ‹The storage rewind reaches the bottom @{term "mid_reset_combined_config_gen
(k_tm M) M pack c w (length w + 1) 0"} (storage head at @{text le}, input head
still frozen at @{term "length w + 1"}) from @{const post_encoder_config_gen}
in exactly @{term "Suc (length (wrap_enc pack c w))"} rewind steps --- the
@{text "⌈n/c⌉"} storage cells, the @{text "ε⋅n"} term. The input tape
is ∗‹never› walked.›
lemma plant_rewind_loop_relpow:
assumes vM: "valid_mttm M"
and c_pos: "0 < c"
and w_alpha: "set w ⊆ Σu"
and bl_ne_le: "bl_tm M ≠ le_tm M"
and k2: "2 ≤ k_tm M"
and pack_in:
"⋀i. i * c < length w ⟹ pack (take c (drop (i * c) w)) ∈ Γ_tm M"
and pack_ne_le:
"⋀i. i * c < length w ⟹ pack (take c (drop (i * c) w)) ≠ le_tm M"
shows "(post_encoder_config_gen (k_tm M) M pack c w,
mid_reset_combined_config_gen (k_tm M) M pack c w (length w + 1) 0)
∈ (mttm_step (wrap_delta M pack c Σu))
^^ (Suc (length (wrap_enc pack c w)))"
proof -
let ?L = "length (wrap_enc pack c w)"
have iter:
"(mid_reset_combined_config_gen (k_tm M) M pack c w (length w + 1) (0 + Suc ?L),
mid_reset_combined_config_gen (k_tm M) M pack c w (length w + 1) 0)
∈ (mttm_step (wrap_delta M pack c Σu)) ^^ (Suc ?L)"
apply (rule mid_plant_rewind_iter[OF vM c_pos w_alpha bl_ne_le k2])
apply (fact pack_in)
apply (fact pack_ne_le)
done
show ?thesis
using iter by (simp add: post_encoder_eq_mid_reset_combined_top)
qed
subsection ‹The floated engine configuration and the plant-done / dispatch steps›
text ‹After the rewind bottoms out, the plant-done step writes a fresh
@{text le} on the input tape (physical @{text 0}) at its frozen head
@{term "length w + 1"} and hands to @{text W_Disp}; the dispatch then
lifts @{text "W_Disp → W_Run (s_tm M)"}. Both leave heads fixed. The
common tape function ‹plant_reset_tape› is the rewind bottom with
the planted @{text le}: physical tape @{text 0} carries @{text le} at cell
@{text 0}, the spent raw input at cells @{text "1 … length w"}, the
∗‹planted› @{text le} at cell @{term "length w + 1"}, and blanks above.›
definition plant_reset_tape ::
"('q, 'b) mttm ⇒ ('a list ⇒ 'b) ⇒ nat ⇒ 'a list ⇒ nat ⇒ nat
⇒ ('a, 'b) wrap_alphabet"
where
"plant_reset_tape M pack c w t n =
(if t < k_tm M
then (case t of
0 ⇒ (if n = 0 then Enc (le_tm M)
else if n ≤ length w then Raw (w ! (n - 1))
else if n = length w + 1 then Enc (le_tm M)
else Enc (bl_tm M))
| Suc k ⇒ (if n = 0 then Enc (le_tm M)
else if k = 0 ∧ n ≤ length (wrap_enc pack c w)
then Enc (wrap_enc pack c w ! (n - 1))
else Enc (bl_tm M)))
else Enc (bl_tm M))"
definition plant_reset_pos :: "'a list ⇒ nat ⇒ nat" where
"plant_reset_pos w t = (case t of 0 ⇒ length w + 1 | Suc _ ⇒ 0)"
definition mid_plant_disp_config ::
"('q, 'b) mttm ⇒ ('a list ⇒ 'b) ⇒ nat ⇒ 'a list
⇒ (('a, 'b) wrap_alphabet, ('q, 'a, 'b) wrap_state) mt_config"
where
"mid_plant_disp_config M pack c w =
Config⇩M W_Disp (plant_reset_tape M pack c w) (plant_reset_pos w)"
definition post_plant_dispatch_config ::
"('q, 'b) mttm ⇒ ('a list ⇒ 'b) ⇒ nat ⇒ 'a list
⇒ (('a, 'b) wrap_alphabet, ('q, 'a, 'b) wrap_state) mt_config"
where
"post_plant_dispatch_config M pack c w =
Config⇩M (W_Run (s_tm M)) (plant_reset_tape M pack c w) (plant_reset_pos w)"
text ‹The plant-done step: from the rewind bottom (storage head at @{text le})
one @{const wrap_plant_done_delta} transition plants @{text le} on the
input tape at its frozen head and lifts @{text "W_Reset → W_Disp"}.›
lemma plant_done_step:
assumes vM: "valid_mttm M"
and k2: "2 ≤ k_tm M"
shows "(mid_reset_combined_config_gen (k_tm M) M pack c w (length w + 1) 0,
mid_plant_disp_config M pack c w)
∈ mttm_step (wrap_delta M pack c Σu)"
proof -
let ?src = "mid_reset_combined_config_gen (k_tm M) M pack c w (length w + 1) 0"
let ?sym = "λk. mt_tape ?src k (mt_pos ?src k)"
let ?a = "λt. if t = 0 then Enc (le_tm M) else ?sym t"
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 src_state: "mt_state ?src = W_Reset"
by (simp add: mid_reset_combined_config_gen_def)
have src_eq: "?src = Config⇩M W_Reset (mt_tape ?src) (mt_pos ?src)"
using src_state by (cases ?src) simp
have sym1_le: "?sym (Suc 0) = Enc (le_tm M)"
using k2 by (simp add: mid_reset_combined_config_gen_def split: nat.split)
have tail_bl: "∀j≥k_tm M. ?sym j = Enc (bl_tm M)"
by (auto simp: mid_reset_combined_config_gen_def)
have rd_range: "?sym ∈ UNIV → Raw ` Σu ∪ Enc ` Γ_tm M"
using bl_in le_in
by (auto simp: mid_reset_combined_config_gen_def split: nat.split)
have tuple_in: "(W_Reset, ?sym, W_Disp, ?a, λ_. dir.N)
∈ wrap_delta M pack c Σu"
proof -
have "(W_Reset, ?sym, W_Disp, ?a, λ_. dir.N)
∈ wrap_plant_done_delta M Σu"
unfolding wrap_plant_done_delta_def
using sym1_le tail_bl rd_range by blast
thus ?thesis by (simp add: wrap_delta_def)
qed
have step_holds:
"(Config⇩M W_Reset (mt_tape ?src) (mt_pos ?src),
Config⇩M W_Disp
(λk. (mt_tape ?src k)((mt_pos ?src k) := ?a k))
(λk. go_dir dir.N (mt_pos ?src k)))
∈ mttm_step (wrap_delta M pack c Σu)"
by (rule mttm_step.step
[where ts = "mt_tape ?src" and n = "mt_pos ?src" and a = ?a
and dir = "λ_. dir.N", OF tuple_in])
have target_eq:
"Config⇩M W_Disp
(λk. (mt_tape ?src k)((mt_pos ?src k) := ?a k))
(λk. go_dir dir.N (mt_pos ?src k))
= mid_plant_disp_config M pack c w"
using k2
by (auto simp: mid_plant_disp_config_def plant_reset_tape_def plant_reset_pos_def
mid_reset_combined_config_gen_def fun_eq_iff
split: nat.split)
from step_holds target_eq src_eq show ?thesis by simp
qed
text ‹The dispatch step: one @{const wrap_disp_delta_gen} transition lifts
@{text "W_Disp → W_Run (s_tm M)"}, tapes and heads untouched --- reaching
the floated engine configuration @{const post_plant_dispatch_config}.›
lemma plant_disp_step:
assumes vM: "valid_mttm M"
and k2: "2 ≤ k_tm M"
shows "(mid_plant_disp_config M pack c w, post_plant_dispatch_config M pack c w)
∈ mttm_step (wrap_delta M pack c Σu)"
proof -
let ?src = "mid_plant_disp_config M pack c w"
let ?sym = "λk. mt_tape ?src k (mt_pos ?src k)"
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 src_state: "mt_state ?src = W_Disp"
by (simp add: mid_plant_disp_config_def)
have src_eq: "?src = Config⇩M W_Disp (mt_tape ?src) (mt_pos ?src)"
using src_state by (cases ?src) simp
have tail_bl: "∀j≥k_tm M. ?sym j = Enc (bl_tm M)"
by (auto simp: mid_plant_disp_config_def plant_reset_tape_def)
have rd_range: "?sym ∈ UNIV → Raw ` Σu ∪ Enc ` Γ_tm M"
using bl_in le_in
by (auto simp: mid_plant_disp_config_def plant_reset_tape_def plant_reset_pos_def
split: nat.split)
have tuple_in:
"(W_Disp, ?sym, W_Run (s_tm M), ?sym, λ_. dir.N) ∈ wrap_delta M pack c Σu"
proof -
have "(W_Disp, ?sym, W_Run (s_tm M), ?sym, λ_. dir.N)
∈ wrap_disp_delta_gen (k_tm M) M Σu"
unfolding wrap_disp_delta_gen_def
using tail_bl rd_range by blast
thus ?thesis by (simp add: wrap_delta_def)
qed
have step_holds:
"(Config⇩M W_Disp (mt_tape ?src) (mt_pos ?src),
Config⇩M (W_Run (s_tm M))
(λk. (mt_tape ?src k)((mt_pos ?src k) := ?sym k))
(λk. go_dir dir.N (mt_pos ?src k)))
∈ mttm_step (wrap_delta M pack c Σu)"
by (rule mttm_step.step
[where ts = "mt_tape ?src" and n = "mt_pos ?src"
and a = ?sym and dir = "λ_. dir.N", OF tuple_in])
have target_eq:
"Config⇩M (W_Run (s_tm M))
(λk. (mt_tape ?src k)((mt_pos ?src k) := ?sym k))
(λk. go_dir dir.N (mt_pos ?src k))
= post_plant_dispatch_config M pack c w"
by (simp add: post_plant_dispatch_config_def mid_plant_disp_config_def fun_eq_iff)
from step_holds target_eq src_eq show ?thesis by simp
qed
subsection ‹The reset reaches the floated engine configuration›
text ‹From @{const post_encoder_config_gen} the storage rewind, plant-done, and
dispatch together reach the floated engine configuration
@{const post_plant_dispatch_config} in @{term "Suc (length (wrap_enc pack c
w)) + 2"} wrap-steps: @{term "Suc (length (wrap_enc pack c w))"} storage-rewind
steps, the plant-done step, and the dispatch step. Only the storage tape is
walked; the input tape is left in place with a planted @{text le}.›
lemma plant_reset_dispatch_relpow:
assumes vM: "valid_mttm M"
and c_pos: "0 < c"
and w_alpha: "set w ⊆ Σu"
and bl_ne_le: "bl_tm M ≠ le_tm M"
and k2: "2 ≤ k_tm M"
and pack_in:
"⋀i. i * c < length w ⟹ pack (take c (drop (i * c) w)) ∈ Γ_tm M"
and pack_ne_le:
"⋀i. i * c < length w ⟹ pack (take c (drop (i * c) w)) ≠ le_tm M"
shows "(post_encoder_config_gen (k_tm M) M pack c w,
post_plant_dispatch_config M pack c w)
∈ (mttm_step (wrap_delta M pack c Σu))
^^ (Suc (length (wrap_enc pack c w)) + 2)"
proof -
let ?R = "mttm_step (wrap_delta M pack c Σu)"
let ?L = "length (wrap_enc pack c w)"
have loop: "(post_encoder_config_gen (k_tm M) M pack c w,
mid_reset_combined_config_gen (k_tm M) M pack c w (length w + 1) 0)
∈ ?R ^^ (Suc ?L)"
apply (rule plant_rewind_loop_relpow[OF vM c_pos w_alpha bl_ne_le k2])
apply (fact pack_in)
apply (fact pack_ne_le)
done
have done_step: "(mid_reset_combined_config_gen (k_tm M) M pack c w (length w + 1) 0,
mid_plant_disp_config M pack c w) ∈ ?R"
by (rule plant_done_step[OF vM k2])
have disp: "(mid_plant_disp_config M pack c w, post_plant_dispatch_config M pack c w)
∈ ?R"
by (rule plant_disp_step[OF vM k2])
from relpow_Suc_I[OF loop done_step]
have "(post_encoder_config_gen (k_tm M) M pack c w, mid_plant_disp_config M pack c w)
∈ ?R ^^ Suc (Suc ?L)" .
from relpow_Suc_I[OF this disp]
have "(post_encoder_config_gen (k_tm M) M pack c w,
post_plant_dispatch_config M pack c w) ∈ ?R ^^ Suc (Suc (Suc ?L))" .
thus ?thesis by (simp add: numeral_2_eq_2)
qed
lemma plant_reset_dispatch_rtrancl:
assumes vM: "valid_mttm M"
and c_pos: "0 < c"
and w_alpha: "set w ⊆ Σu"
and bl_ne_le: "bl_tm M ≠ le_tm M"
and k2: "2 ≤ k_tm M"
and pack_in:
"⋀i. i * c < length w ⟹ pack (take c (drop (i * c) w)) ∈ Γ_tm M"
and pack_ne_le:
"⋀i. i * c < length w ⟹ pack (take c (drop (i * c) w)) ≠ le_tm M"
shows "(post_encoder_config_gen (k_tm M) M pack c w,
post_plant_dispatch_config M pack c w)
∈ (mttm_step (wrap_delta M pack c Σu))⇧*"
proof -
have "(post_encoder_config_gen (k_tm M) M pack c w,
post_plant_dispatch_config M pack c w)
∈ (mttm_step (wrap_delta M pack c Σu))
^^ (Suc (length (wrap_enc pack c w)) + 2)"
apply (rule plant_reset_dispatch_relpow[OF vM c_pos w_alpha bl_ne_le k2])
apply (fact pack_in)
apply (fact pack_ne_le)
done
thus ?thesis by (rule relpow_imp_rtrancl)
qed
subsection ‹The floated config is a shift of the proper ‹τ›-lift›
text ‹The floated engine configuration @{const post_plant_dispatch_config} is
exactly a @{const shift_rel} of the @{text τ}-lift of M's initial
configuration on the encoded input, shifting ∗‹only› physical tape @{text 0}
(M's tape @{text 1}) right by @{term "length w + 1"}: the planted @{text le}
sits at the shifted origin, the spent raw input is the discarded prefix
below it, and blanks lie above. Every other physical tape (the storage tape
@{text 1} = M's tape @{text 0}, carrying the encoded input, and the fresh
work tapes @{text "2 … k-1"}) is unshifted (@{term "d p = 0"}), so it
matches the lift verbatim. This is the hinge: the origin-float lemmas of
@{theory Multitape_TM_Substrate.Multitape_Origin_Float} translate runs between the two
configs, and only physical tape @{text 0} needs @{text le} at its base
origin --- which the lift supplies (M's blank tape @{text 1} has @{text le}
at cell @{text 0}).›
lemma post_plant_dispatch_shift_lift:
assumes k2: "2 ≤ k_tm M"
shows "shift_rel (λp. if p = 0 then length w + 1 else 0)
(lift_M_config M (init_config_mttm M (wrap_enc pack c w)))
(post_plant_dispatch_config M pack c w)"
proof (cases M)
case (MTTM Q Σi Γ bl le δ s t r kM)
show ?thesis
using k2
unfolding shift_rel_def MTTM
post_plant_dispatch_config_def plant_reset_tape_def plant_reset_pos_def
lift_M_config_def
by (auto simp: wrap_tau_def fun_eq_iff split: nat.split if_splits)
qed
end