Theory Wrap_Base
theory Wrap_Base
imports "Multitape_TM_Substrate.Multitape_Substrate"
begin
section ‹Encoding-wrap combinator›
text ‹The encoding-wrap combinator. Given a substrate machine
‹M› over an encoded alphabet ‹'b› and a per-block packer
‹pack :: 'a list ⇒ 'b› together with a block size ‹c›, the
combinator produces a substrate machine over the union
alphabet ‹('a, 'b) wrap_alphabet = Raw 'a | Enc 'b› at the
textbook tape count ‹k_tm M› (no extra tape): the user's raw
input starts on tape ‹0›, which the wrap reuses as a work tape
rather than adding one (faithful ‹k›-tape section below).
The wrap operates in five reachable phases:
▸ @{text W_Init} — advance both ‹W_User› and ‹W_M 0› past their
LE markers in a single super-step.
▸ @{text "W_Buf ws"} — accumulate up to ‹c› raw symbols from
‹W_User›; on filling the buffer, pack and write one block
to ‹W_M 0›; on seeing an ‹Enc _› symbol (blank past the input
region), flush any partial buffer and proceed to reset.
▸ @{text W_Reset} — move ‹W_M 0›'s head left until LE, restoring
the canonical "head at position 0 reading LE" position M
expects at the start of its own computation.
▸ @{text W_Disp} — single transition handing over to M.
▸ @{text "W_Run q"} — simulate M directly: every M-‹δ› entry
lifts to a wrap-‹δ› entry that reads M's tapes through the
‹Enc› embedding and leaves ‹W_User› untouched.
Halt propagation rides directly on the @{text W_Run}
constructor: the wrap's accept state is @{text "W_Run (t_tm M)"},
inheriting M's acceptance. The wrap's reject state
@{text W_Rej} is declared for substrate compliance (the
@{text "t ≠ r"} requirement) but is unreachable from the start
state.›
text ‹Architecture note: the wrap is monolithic at the substrate
level. The substrate has no generic machine-composition
combinator, so the wrap's per-cell read, head-positioning, and
per-cell write actions are written directly into the wrap's
‹δ›-table rather than as composed sub-machines.›
subsection ‹Wrap alphabet›
text ‹Disjoint union of user-facing and encoded alphabets.
Constructors are injective and disjoint;
the wrap's substrate-level blank and LE symbols are chosen
from the ‹Enc›-image to keep lifted M-transitions transparent.›