Theory Multitape_Origin_Float
theory Multitape_Origin_Float
imports Multitape_Substrate
begin
section ‹Origin floating: an unreachable left prefix is invisible›
text ‹A machine that has planted a fresh left endmarker at some cell
‹d› can never read the cells to its left: the left-endmarker discipline
(clause 1, @{thm[source] valid_mttm_deltaLE}) forbids a leftward move
off ‹le›, so the head is penned in the semi-tape ‹[d, ∞)›. The
content below ‹d› is therefore dead weight. This theory makes that
precise as a per-tape left ∗‹shift› relation and shows the substrate
step relation translates across it in both directions.
The intended use is origin floating on a singly-infinite tape: to
reuse a spent input tape as a blank work tape without the linear
rewind, a machine plants ‹le› at the current head cell ‹d› and treats
‹d› as the new origin. The tape from ‹d› onward (‹le› then blanks)
is then indistinguishable from a fresh blank tape whose origin sits
at cell 0 --- which is exactly a shift by ‹d›.
❙‹Not a bisimulation.› The machines here may be nondeterministic, so
the two step relations are ∗‹not› bisimilar (their successor sets do
not correspond). Each single-step lemma below translates ∗‹one›
transition; chained along a path it carries a single witnessing run
from one origin to the other, which is all that language inclusion
needs. The forward and reverse lemmas together give inclusion in
both directions --- never a claim that the run trees match.›
subsection ‹The per-tape left-shift relation›
text ‹‹shift_rel d c1 c2›: configuration ‹c2› is ‹c1› with each tape
‹k› shifted right by ‹d k› cells. The state agrees, every head sits
‹d k› cells further right, and every cell of ‹c1› reappears ‹d k›
cells further right in ‹c2›. The cells of ‹c2› below ‹d k› are
unconstrained --- that is the discarded prefix. Setting ‹d k = 0›
leaves tape ‹k› untouched, so a single-tape float is the instance
‹d = (λj. if j = k0 then off else 0)›.›
definition shift_rel ::
"(nat ⇒ nat) ⇒ ('a, 'q) mt_config ⇒ ('a, 'q) mt_config ⇒ bool" where
"shift_rel d c1 c2 ⟷
mt_state c2 = mt_state c1
∧ (∀k. mt_pos c2 k = mt_pos c1 k + d k)
∧ (∀k p. mt_tape c2 k (p + d k) = mt_tape c1 k p)"
lemma shift_rel_state:
"shift_rel d c1 c2 ⟹ mt_state c2 = mt_state c1"
by (simp add: shift_rel_def)
subsection ‹Single-step translation, both directions›
text ‹Forward: a step of ‹M› from the base config ‹c1› lifts to a step
from the shifted config ‹c2›, landing in the shift of the base
successor. The one delicate point is the head position at a floated
origin: were the head at cell 0 of a floated tape (‹d k > 0›) to move
left, the base clamps at 0 while the shift lands at ‹d k - 1›,
breaking sync. But cell 0 of the base carries ‹le› (hypothesis
‹le0›), so clause 1 forbids that leftward move. ‹le0› is required only
on the ∗‹floated› tapes (‹d k ≠ 0›): where ‹d k = 0› the shift is the
identity and a leftward move at cell 0 stays in sync, so no ‹le› is
needed there. This matters when the base is a lift with all-blank
out-of-range tapes (no ‹le› at their cell 0): those tapes are never
floated, so ‹le0› does not constrain them. On the floated tapes ‹le0›
holds of every configuration reachable from an initial one
(@{thm[source] valid_reach_LE_pos0_mttm}).›
lemma mttm_step_shift_forward:
fixes M :: "('q, 'a) mttm"
assumes vM: "valid_mttm M"
and le0: "∀k. d k ≠ 0 ⟶ mt_tape c1 k 0 = le_tm M"
and rel: "shift_rel d c1 c2"
and step: "(c1, c1') ∈ mttm_step (delta_tm M)"
shows "∃c2'. (c2, c2') ∈ mttm_step (delta_tm M) ∧ shift_rel d c1' c2'"
proof -
from step obtain q ts1 n1 q' a dr where
c1_eq: "c1 = Config⇩M q ts1 n1"
and c1'_eq: "c1' = Config⇩M q' (λk. (ts1 k)(n1 k := a k))
(λk. go_dir (dr k) (n1 k))"
and tr: "(q, λk. ts1 k (n1 k), q', a, dr) ∈ delta_tm M"
by (auto elim: mttm_step.cases)
obtain sc ts2 n2 where c2_eq: "c2 = Config⇩M sc ts2 n2"
by (cases c2) auto
have unpacked:
"sc = q ∧ (∀k. n2 k = n1 k + d k) ∧ (∀k p. ts2 k (p + d k) = ts1 k p)"
using rel by (simp add: shift_rel_def c1_eq c2_eq)
from unpacked have st2: "sc = q" by simp
from unpacked have pos2: "⋀k. n2 k = n1 k + d k" by simp
from unpacked have tape2: "⋀k p. ts2 k (p + d k) = ts1 k p" by simp
have read_eq: "(λk. ts2 k (n2 k)) = (λk. ts1 k (n1 k))"
proof
fix k
have "ts2 k (n2 k) = ts2 k (n1 k + d k)" using pos2 by simp
also have "… = ts1 k (n1 k)" using tape2 by simp
finally show "ts2 k (n2 k) = ts1 k (n1 k)" .
qed
have tr2: "(q, λk. ts2 k (n2 k), q', a, dr) ∈ delta_tm M"
using tr read_eq by simp
let ?c2' = "Config⇩M q' (λk. (ts2 k)(n2 k := a k))
(λk. go_dir (dr k) (n2 k))"
have step2: "(c2, ?c2') ∈ mttm_step (delta_tm M)"
unfolding c2_eq st2 by (rule mttm_step.step, rule tr2)
have no_L_at0: "⋀k. d k ≠ 0 ⟹ n1 k = 0 ⟹ dr k ≠ dir.L"
proof -
fix k assume dk: "d k ≠ 0" and nk0: "n1 k = 0"
have "(λk. ts1 k (n1 k)) k = le_tm M" using le0 dk nk0 c1_eq by simp
from valid_mttm_deltaLE[OF vM tr this] show "dr k ≠ dir.L" by auto
qed
have pos_sync: "⋀k. go_dir (dr k) (n2 k) = go_dir (dr k) (n1 k) + d k"
proof -
fix k
show "go_dir (dr k) (n2 k) = go_dir (dr k) (n1 k) + d k"
proof (cases "dr k")
case N thus ?thesis using pos2 by simp
next
case R thus ?thesis using pos2 by simp
next
case L
show ?thesis
proof (cases "d k = 0")
case True thus ?thesis using L pos2 by simp
next
case False
hence "n1 k ≠ 0" using no_L_at0 L by blast
then obtain m where "n1 k = Suc m" by (cases "n1 k") auto
thus ?thesis using L pos2 by simp
qed
qed
qed
have tape_sync:
"⋀k p. ((ts2 k)(n2 k := a k)) (p + d k) = ((ts1 k)(n1 k := a k)) p"
proof -
fix k p
show "((ts2 k)(n2 k := a k)) (p + d k) = ((ts1 k)(n1 k := a k)) p"
proof (cases "p = n1 k")
case True
hence "p + d k = n2 k" using pos2 by simp
thus ?thesis using True by simp
next
case False
hence "p + d k ≠ n2 k" using pos2 by simp
thus ?thesis using False tape2 by simp
qed
qed
have rel': "shift_rel d c1' ?c2'"
unfolding shift_rel_def c1'_eq using pos_sync tape_sync by simp
from step2 rel' show ?thesis by blast
qed
text ‹Reverse: a step of ‹M› from the shifted config ‹c2› descends to a
step from the base config ‹c1›. The transition witnessing the ‹c2›
step reads exactly what ‹c1›'s head reads (the shift relation), so the
same transition fires from ‹c1›; the boundary argument is identical
(‹le› at the base origin forbids the desyncing leftward move).›
lemma mttm_step_shift_reverse:
fixes M :: "('q, 'a) mttm"
assumes vM: "valid_mttm M"
and le0: "∀k. d k ≠ 0 ⟶ mt_tape c1 k 0 = le_tm M"
and rel: "shift_rel d c1 c2"
and step: "(c2, c2') ∈ mttm_step (delta_tm M)"
shows "∃c1'. (c1, c1') ∈ mttm_step (delta_tm M) ∧ shift_rel d c1' c2'"
proof -
obtain q ts1 n1 where c1_eq: "c1 = Config⇩M q ts1 n1"
by (cases c1) auto
from step obtain sc ts2 n2 q' a dr where
c2_eq: "c2 = Config⇩M sc ts2 n2"
and c2'_eq: "c2' = Config⇩M q' (λk. (ts2 k)(n2 k := a k))
(λk. go_dir (dr k) (n2 k))"
and tr: "(sc, λk. ts2 k (n2 k), q', a, dr) ∈ delta_tm M"
by (auto elim: mttm_step.cases)
have unpacked:
"sc = q ∧ (∀k. n2 k = n1 k + d k) ∧ (∀k p. ts2 k (p + d k) = ts1 k p)"
using rel by (simp add: shift_rel_def c1_eq c2_eq)
from unpacked have st2: "sc = q" by simp
from unpacked have pos2: "⋀k. n2 k = n1 k + d k" by simp
from unpacked have tape2: "⋀k p. ts2 k (p + d k) = ts1 k p" by simp
have read_eq: "(λk. ts2 k (n2 k)) = (λk. ts1 k (n1 k))"
proof
fix k
have "ts2 k (n2 k) = ts2 k (n1 k + d k)" using pos2 by simp
also have "… = ts1 k (n1 k)" using tape2 by simp
finally show "ts2 k (n2 k) = ts1 k (n1 k)" .
qed
have tr1: "(q, λk. ts1 k (n1 k), q', a, dr) ∈ delta_tm M"
using tr read_eq st2 by simp
let ?c1' = "Config⇩M q' (λk. (ts1 k)(n1 k := a k))
(λk. go_dir (dr k) (n1 k))"
have step1: "(c1, ?c1') ∈ mttm_step (delta_tm M)"
unfolding c1_eq by (rule mttm_step.step, rule tr1)
have no_L_at0: "⋀k. d k ≠ 0 ⟹ n1 k = 0 ⟹ dr k ≠ dir.L"
proof -
fix k assume dk: "d k ≠ 0" and nk0: "n1 k = 0"
have "(λk. ts1 k (n1 k)) k = le_tm M" using le0 dk nk0 c1_eq by simp
from valid_mttm_deltaLE[OF vM tr1 this] show "dr k ≠ dir.L" by auto
qed
have pos_sync: "⋀k. go_dir (dr k) (n2 k) = go_dir (dr k) (n1 k) + d k"
proof -
fix k
show "go_dir (dr k) (n2 k) = go_dir (dr k) (n1 k) + d k"
proof (cases "dr k")
case N thus ?thesis using pos2 by simp
next
case R thus ?thesis using pos2 by simp
next
case L
show ?thesis
proof (cases "d k = 0")
case True thus ?thesis using L pos2 by simp
next
case False
hence "n1 k ≠ 0" using no_L_at0 L by blast
then obtain m where "n1 k = Suc m" by (cases "n1 k") auto
thus ?thesis using L pos2 by simp
qed
qed
qed
have tape_sync:
"⋀k p. ((ts2 k)(n2 k := a k)) (p + d k) = ((ts1 k)(n1 k := a k)) p"
proof -
fix k p
show "((ts2 k)(n2 k := a k)) (p + d k) = ((ts1 k)(n1 k := a k)) p"
proof (cases "p = n1 k")
case True
hence "p + d k = n2 k" using pos2 by simp
thus ?thesis using True by simp
next
case False
hence "p + d k ≠ n2 k" using pos2 by simp
thus ?thesis using False tape2 by simp
qed
qed
have rel': "shift_rel d ?c1' c2'"
unfolding shift_rel_def c2'_eq using pos_sync tape_sync by simp
from step1 rel' show ?thesis by blast
qed
subsection ‹Path translation, both directions›
text ‹Chaining the single-step lemmas along a path. The ‹le›-at-0
invariant is re-established at each intermediate configuration by
@{thm[source] mttm_step_LE_pos0_preserve}, so the same base config
hypothesis ‹le0› drives the whole chain. These translate ∗‹one›
path of length ‹n›; there is no claim that the base and shifted
machines have matching successor sets.›
lemma mttm_relpow_shift_forward:
fixes M :: "('q, 'a) mttm"
assumes vM: "valid_mttm M"
shows "⟦ ∀k. d k ≠ 0 ⟶ mt_tape c1 k 0 = le_tm M; shift_rel d c1 c2;
(c1, c1') ∈ (mttm_step (delta_tm M)) ^^ n ⟧
⟹ ∃c2'. (c2, c2') ∈ (mttm_step (delta_tm M)) ^^ n
∧ shift_rel d c1' c2'"
proof (induction n arbitrary: c1 c2 c1')
case 0
then show ?case by auto
next
case (Suc n)
from Suc.prems(3) obtain cmid where
first: "(c1, cmid) ∈ mttm_step (delta_tm M)"
and rest: "(cmid, c1') ∈ (mttm_step (delta_tm M)) ^^ n"
by (blast dest: relpow_Suc_D2)
obtain cmid2 where
first2: "(c2, cmid2) ∈ mttm_step (delta_tm M)"
and rel_mid: "shift_rel d cmid cmid2"
using mttm_step_shift_forward[OF vM Suc.prems(1) Suc.prems(2) first] by blast
have le0_mid: "∀k. d k ≠ 0 ⟶ mt_tape cmid k 0 = le_tm M"
proof (intro allI impI)
fix k assume "d k ≠ 0"
have "mt_tape c1 k 0 = le_tm M" using Suc.prems(1) ‹d k ≠ 0› by blast
from mttm_step_LE_pos0_preserve[OF vM first this]
show "mt_tape cmid k 0 = le_tm M" .
qed
from Suc.IH[OF le0_mid rel_mid rest] obtain c2' where
tail2: "(cmid2, c2') ∈ (mttm_step (delta_tm M)) ^^ n"
and rel_end: "shift_rel d c1' c2'"
by blast
have "(c2, c2') ∈ (mttm_step (delta_tm M)) ^^ (Suc n)"
using first2 tail2 by (rule relpow_Suc_I2)
then show ?case using rel_end by blast
qed
lemma mttm_relpow_shift_reverse:
fixes M :: "('q, 'a) mttm"
assumes vM: "valid_mttm M"
shows "⟦ ∀k. d k ≠ 0 ⟶ mt_tape c1 k 0 = le_tm M; shift_rel d c1 c2;
(c2, c2') ∈ (mttm_step (delta_tm M)) ^^ n ⟧
⟹ ∃c1'. (c1, c1') ∈ (mttm_step (delta_tm M)) ^^ n
∧ shift_rel d c1' c2'"
proof (induction n arbitrary: c1 c2 c2')
case 0
then show ?case by auto
next
case (Suc n)
from Suc.prems(3) obtain cmid2 where
first2: "(c2, cmid2) ∈ mttm_step (delta_tm M)"
and rest2: "(cmid2, c2') ∈ (mttm_step (delta_tm M)) ^^ n"
by (blast dest: relpow_Suc_D2)
obtain cmid where
first: "(c1, cmid) ∈ mttm_step (delta_tm M)"
and rel_mid: "shift_rel d cmid cmid2"
using mttm_step_shift_reverse[OF vM Suc.prems(1) Suc.prems(2) first2] by blast
have le0_mid: "∀k. d k ≠ 0 ⟶ mt_tape cmid k 0 = le_tm M"
proof (intro allI impI)
fix k assume "d k ≠ 0"
have "mt_tape c1 k 0 = le_tm M" using Suc.prems(1) ‹d k ≠ 0› by blast
from mttm_step_LE_pos0_preserve[OF vM first this]
show "mt_tape cmid k 0 = le_tm M" .
qed
from Suc.IH[OF le0_mid rel_mid rest2] obtain c1' where
tail: "(cmid, c1') ∈ (mttm_step (delta_tm M)) ^^ n"
and rel_end: "shift_rel d c1' c2'"
by blast
have "(c1, c1') ∈ (mttm_step (delta_tm M)) ^^ (Suc n)"
using first tail by (rule relpow_Suc_I2)
then show ?case using rel_end by blast
qed
subsection ‹Acceptance transfers across the shift, both directions›
text ‹The consumer-facing interface. A run reaching a nominated state
‹qa› (the accept state, in use) in ‹n› steps from the base config
yields one of the ∗‹same length› reaching the same state from the
shifted config, and conversely. Length preservation carries the time
bound; state preservation (@{thm[source] shift_rel_state}) carries
acceptance. The two directions give language inclusion each way ---
exactly what a nondeterministic machine admits, with no bisimulation
claim. These ‹relpow› (fixed-length) forms feed
@{const accepts_in_time_mttm} directly; a caller working with
@{const Lang_mttm} unfolds @{thm[source] rtrancl_power} to a fixed
length first, then applies them.›
lemma shift_reach_state_forward:
fixes M :: "('q, 'a) mttm"
assumes vM: "valid_mttm M"
and le0: "∀k. d k ≠ 0 ⟶ mt_tape c1 k 0 = le_tm M"
and rel: "shift_rel d c1 c2"
and run: "(c1, ca) ∈ (mttm_step (delta_tm M)) ^^ n"
and acc: "mt_state ca = qa"
shows "∃cb. (c2, cb) ∈ (mttm_step (delta_tm M)) ^^ n ∧ mt_state cb = qa"
proof -
from mttm_relpow_shift_forward[OF vM le0 rel run] obtain cb where
run2: "(c2, cb) ∈ (mttm_step (delta_tm M)) ^^ n"
and rel2: "shift_rel d ca cb" by blast
have "mt_state cb = mt_state ca" using rel2 by (rule shift_rel_state)
thus ?thesis using run2 acc by auto
qed
lemma shift_reach_state_reverse:
fixes M :: "('q, 'a) mttm"
assumes vM: "valid_mttm M"
and le0: "∀k. d k ≠ 0 ⟶ mt_tape c1 k 0 = le_tm M"
and rel: "shift_rel d c1 c2"
and run: "(c2, cb) ∈ (mttm_step (delta_tm M)) ^^ n"
and acc: "mt_state cb = qa"
shows "∃ca. (c1, ca) ∈ (mttm_step (delta_tm M)) ^^ n ∧ mt_state ca = qa"
proof -
from mttm_relpow_shift_reverse[OF vM le0 rel run] obtain ca where
run1: "(c1, ca) ∈ (mttm_step (delta_tm M)) ^^ n"
and rel2: "shift_rel d ca cb" by blast
have "mt_state cb = mt_state ca" using rel2 by (rule shift_rel_state)
thus ?thesis using run1 acc by auto
qed
end