Theory Multitape_Alphabet_Enlargement.AlphabetEnlargement_Defs

theory AlphabetEnlargement_Defs
  imports "Multitape_TM_Substrate.Multitape_Substrate"
begin

section ‹Alphabet enlargement›

text ‹Setup for the ‹alphabet_enlarge› combinator:
  substrate selectors, stage-bookkeeping types, offset and
  block helpers, encoder / decoder, encoder-canonicity
  predicates, per-substep transition relations, the
  ‹alphabet_enlarge› combinator itself, the
  ‹ae_simulates› relation, and the eight mid-stage
  invariants ‹ae_inv_ss1› through ‹ae_inv_ss8›,
  plus the upstream structural lemmas, the encoder-roundtrip
  chain, and the validation-phase chain culminating in
  ‹ae_validation_steps_bound›.

  The forward-simulation chain that consumes the validation
  result, and the top-level theorems
  ‹alphabet_enlarge_wf›,
  ‹alphabet_enlarge_language›, and
  ‹alphabet_enlarge_time›, follow further on in this
  chapter.›

text ‹Substrate selectors (‹bl_tm›, ‹le_tm›, ‹delta_tm›,
  ‹s_tm›, ‹t_tm›, ‹r_tm›, ‹Sigma_tm›, ‹mt_tape›) live in
  the ‹Multitape_Substrate› theory alongside the functional substrate
  layer; they're imported transitively.›

subsection ‹Stage bookkeeping types›

text ‹Substep counter / phase indicator for ‹M'›'s state machine.

  Constructors ‹VFwd› / ‹VFwdPad› / ‹VRet› mark the
  validation phase: forward scan (no padded block seen yet),
  forward scan after a trailing-padded block has been
  observed, and return scan back to the first input block.

  Constructors ‹SS1› … ‹SS8› mark the 8-substep simulation
  stage of Hopcroft--Ullman
  \<^cite>‹‹Theorem 12.3› in "Hopcroft1979:introduction"›; ‹SSn›
  corresponds to the spec's "substep ‹n›".›

datatype substep_idx =
    VFwd | VFwdPad | VRet
  | SS1 | SS2 | SS3 | SS4 | SS5 | SS6 | SS7 | SS8

instance substep_idx :: finite
proof (intro_classes)
  have "(UNIV :: substep_idx set) ⊆
          {VFwd, VFwdPad, VRet,
           SS1, SS2, SS3, SS4, SS5, SS6, SS7, SS8}"
    using substep_idx.exhaust by blast
  thus "finite (UNIV :: substep_idx set)"
    using finite_subset by auto
qed

text ‹Per-tape destination indicator: which buffer slot now holds
  the home block of ‹M›'s simulated head, after the compute
  substep (the 4th component of ‹stage›).
  The compute substep sets this; the write-back phase consumes it
  to choose between move-sequence variants
  (`L,R,R,N` / `L,R,R,L` / `R,L,L,N` for steady-state stages).›

datatype ae_dest = AE_Left | AE_Home | AE_Right

instance ae_dest :: finite
proof (intro_classes)
  have "(UNIV :: ae_dest set) ⊆ {AE_Left, AE_Home, AE_Right}"
    using ae_dest.exhaust by blast
  thus "finite (UNIV :: ae_dest set)"
    using finite_subset by auto
qed

text ‹Stage bookkeeping carried in the output machine's state set:
  per-tape within-block offset (‹nat ⇒ 'c›), per-tape three-block
  buffer (left, home, right), per-tape destination indicator
  (‹AE_Left› / ‹AE_Home› / ‹AE_Right›), and the substep counter
  within the current 8-substep stage.›

type_synonym ('a, 'c) ae_stage =
  "(nat ⇒ 'c)
   × (nat ⇒ ('c ⇒ 'a) × ('c ⇒ 'a) × ('c ⇒ 'a))
   × (nat ⇒ ae_dest)
   × substep_idx"

subsection ‹Offset arithmetic on ‹'c››

text ‹The compute substep tracks a simulated head position by an
  offset within a 3-block buffer; advancing by ‹L› / ‹R›
  requires partial successor / predecessor on ‹'c›.  We use the
  canonical enumeration provided by the ‹enum› class.›

definition c_idx :: "'c :: enum ⇒ nat" where
  "c_idx x = (THE i. i < length (enum_class.enum :: 'c list)
                     ∧ (enum_class.enum :: 'c list) ! i = x)"

definition c_first :: "'c :: enum" where
  "c_first = (enum_class.enum :: 'c list) ! 0"

definition c_last :: "'c :: enum" where
  "c_last = (enum_class.enum :: 'c list)
              ! (length (enum_class.enum :: 'c list) - 1)"

definition c_succ :: "'c :: enum ⇒ 'c option" where
  "c_succ x =
     (let xs = enum_class.enum :: 'c list; i = c_idx x in
        if Suc i < length xs then Some (xs ! Suc i) else None)"

definition c_pred :: "'c :: enum ⇒ 'c option" where
  "c_pred x =
     (let xs = enum_class.enum :: 'c list; i = c_idx x in
        if i = 0 then None else Some (xs ! (i - 1)))"

subsection ‹Block-encoding helpers›

text ‹The constant LE-block: a block whose every cell holds
  ‹M›'s left-endmarker symbol.  Used as ‹M'›'s left endmarker.
  Compatible with the substrate's ‹δLE› invariant: any read of
  this block tests ‹le› at every cell, so the
  ‹a k = LE ⟹ a' k = LE ∧ d k ∈ {N, R}› obligation lifts
  pointwise from ‹M›'s.›

definition LE_block :: "'a ⇒ ('c :: enum ⇒ 'a)" where
  "LE_block le = (λ_. le)"

text ‹The constant blank-block: a block whose every cell holds
  ‹M›'s blank symbol.  Used as ‹M'›'s blank, and also as the
  semantic placeholder for ‹buf.left› in LE-stages.›

definition bl_block :: "'a ⇒ ('c :: enum ⇒ 'a)" where
  "bl_block bl = (λ_. bl)"

subsection ‹Encoder›

text ‹Encoding an input word as a list of ‹c›-blocks,
  padding the final block with the substrate's blank symbol if the
  input length is not a multiple of ‹c›.

  The grouping factor ‹c = card (UNIV :: 'c set)› is determined at
  the type level.  Block ‹i› (for ‹i < ⌈length w / c⌉›) is
  the function ‹λx. if i ⋅ c + c_idx x < length w then w ! (i ⋅ c
  + c_idx x) else bl›; the output list has length
  ‹⌈length w / c⌉›, computed in nat arithmetic as
  ‹(length w + c - 1) div c›.›

definition encode_input ::
  "'a ⇒ 'a list ⇒ (('c :: enum) ⇒ 'a) list" where
  "encode_input bl w =
     (let c = card (UNIV :: 'c set) in
        map (λi. (λx. let j = i * c + c_idx x in
                          if j < length w then w ! j else bl))
            [0 ..< (length w + c - 1) div c])"

subsection ‹Decoder›

text ‹Decoder: extract ‹M›-symbols from a list of blocks by
  taking each block's ‹bl›-free prefix under the canonical
  ‹'c›-enumeration.  For pure blocks this yields all ‹c›
  cells; for trailing-padded blocks it yields the non-blank
  prefix; for non-canonical blocks (blank-then-non-blank
  pattern) it yields the leading non-blank prefix only — but
  the validation phase rejects these before decoding is invoked.
  Inverse to ‹encode_input› on the encoder image; cited by the
  forward direction of
  ‹ae_validation_canonical_iff_encoder_image›.›

definition ae_decode_block :: "'a ⇒ ('c :: enum ⇒ 'a) ⇒ 'a list" where
  "ae_decode_block bl f =
     takeWhile (λa. a ≠ bl) (map f (enum_class.enum :: 'c list))"

definition ae_decode_input :: "'a ⇒ (('c :: enum) ⇒ 'a) list ⇒ 'a list" where
  "ae_decode_input bl w = concat (map (ae_decode_block bl) w)"

subsection ‹Initial stage›

text ‹Initial within-block offset.  Every tape's offset starts at a
  canonical element of ‹'c› (treated as the within-block position
  of ‹M›'s left endmarker on each tape).  The specific element is
  underspecified at this level; the simulation argument (§30.4)
  fixes a canonical ‹0›-offset matching ‹M›'s initial head
  position.›

definition init_offset :: "nat ⇒ ('c :: enum)" where
  "init_offset = (λ_. SOME x. True)"

text ‹Initial buffer.  Every tape starts with three constant
  ‹LE›-blocks: at ‹M'›'s position 0 the home block is the
  left-endmarker block, and the buffer phase has not yet executed
  on the surrounding cells; the SS1‹→›SS4 buffer phase
  refills the slots from actual tape contents at the start of
  every stage.›

definition init_buffer ::
  "'a ⇒ (nat ⇒ (('c :: enum ⇒ 'a)
                  × ('c ⇒ 'a)
                  × ('c ⇒ 'a)))" where
  "init_buffer le = (λ_. (LE_block le, LE_block le, LE_block le))"

text ‹Initial destination indicator: every tape starts with
  ‹AE_Home› (the indicator is meaningful only after the compute
  substep sets it; the initial value is canonical).›

definition init_dest :: "nat ⇒ ae_dest" where
  "init_dest = (λ_. AE_Home)"

text ‹Initial stage: zero offset, all-‹LE› buffers, dest = home,
  substep counter ‹SS1›.›

definition init_stage ::
  "'a ⇒ ('a, 'c :: enum) ae_stage" where
  "init_stage le = (init_offset, init_buffer le, init_dest, VFwd)"

subsection ‹Encoder-canonicity predicates›

text ‹A block is ‹pure› if every cell is non-blank.  In the
  encoder image, every block except possibly the last has
  this form (every cell is from the original input).›

definition is_pure_block ::
  "'a ⇒ ('c :: enum ⇒ 'a) ⇒ bool" where
  "is_pure_block bl f = (∀x. f x ≠ bl)"

text ‹A block is ‹trailing-padded› if there is a non-empty,
  proper prefix (under the canonical ‹'c›-enumeration) of
  non-blank cells, and the remaining cells are all blank.  In the
  encoder image, the last block has this form when the
  input length is not a multiple of ‹c›.›

definition is_padded_block ::
  "'a ⇒ ('c :: enum ⇒ 'a) ⇒ bool" where
  "is_padded_block bl f =
     (∃k. k ≥ 1 ∧ k < length (enum_class.enum :: 'c list)
       ∧ (∀x. c_idx x < k ⟶ f x ≠ bl)
       ∧ (∀x. c_idx x ≥ k ⟶ f x = bl))"

text ‹Encoder-canonical block: pure or trailing-padded.  The
  validation phase accepts only blocks satisfying this
  predicate; non-canonical blocks (blanks scattered in
  non-trailing positions) route the input to ‹r_M'›.›

definition is_canonical_block ::
  "'a ⇒ ('c :: enum ⇒ 'a) ⇒ bool" where
  "is_canonical_block bl f = (is_pure_block bl f ∨ is_padded_block bl f)"

text ‹Sequence-level encoder-canonicity: the input ‹w› is
  well-formed (= in the encoder image) iff every block is
  pure, *except possibly the last* which may also be padded.
  Per block encoder-canonicity (‹is_canonical_block›) is
  necessary but not sufficient — a sequence with a padded
  block followed by anything else is per-cell canonical but
  not in the encoder image.

  The validation phase enforces exactly this distinction: VFwd
  reject fires on non-canonical cells; VFwdPad reject fires on
  any non-‹bl_block› cell after a padded block.›

definition ae_input_well_formed ::
  "'a ⇒ ('c :: enum ⇒ 'a) list ⇒ bool" where
  "ae_input_well_formed bl w ⟷
     (∀s. s < length w ⟶
        (is_pure_block bl (w ! s)
         ∨ (s = length w - 1 ∧ is_padded_block bl (w ! s))))"

end