Theory AlphabetReduction_Codec

theory AlphabetReduction_Codec
  imports "Multitape_TM_Substrate.Multitape_Substrate"
begin

section ‹Alphabet reduction›

text ‹This theory opens the alphabet-reduction development.  The
  ‹alphabet_reduce› combinator takes a well-formed substrate
  machine over an arbitrary finite alphabet ‹'a› (with
  tape-alphabet cardinality ‹≥› 4) and produces a
  well-formed substrate machine over the fixed four-element alphabet
  ‹sym4›, preserving the accepted language, determinism, and
  tape count.

  This is the elementary determinism-preserving per-symbol multi-cell
  encoding.

  The development is layered: this first theory fixes the output
  alphabet ‹sym4› and the per-symbol binary codec; the
  simulator, its delta, and the headline theorems
  (‹alphabet_reduce_wf›, ‹alphabet_reduce_language›,
  ‹alphabet_reduce_time›, ‹alphabet_reduce_det›) are
  built across the theories that follow.
  Throughout, ‹b› abbreviates ‹block_width Γ› (the per-symbol cell width).›

text ‹The fixed four-element output alphabet:
  ‹BLANK4› (blank), ‹LE4› (left endmarker),
  ‹BIT0› (binary 0), ‹BIT1› (binary 1).›

datatype sym4 = BLANK4 | LE4 | BIT0 | BIT1

lemma sym4_UNIV: "(UNIV :: sym4 set) = {BLANK4, LE4, BIT0, BIT1}"
  using sym4.exhaust by blast

lemma sym4_card: "card (UNIV :: sym4 set) = 4"
proof -
  have "(UNIV :: sym4 set) = {BLANK4, LE4, BIT0, BIT1}"
    by (rule sym4_UNIV)
  moreover have "card {BLANK4, LE4, BIT0, BIT1} = 4"
    by simp
  ultimately show ?thesis by simp
qed

subsection ‹Per-symbol encoder helpers›

text ‹The per-source-symbol block length: the number of ‹sym4›
  cells that encode one ‹Γ›-symbol, and the slowdown factor of
  the reduction.  At least ‹1› (to avoid degenerate empty
  encodings even for trivial ‹Γ›), and otherwise
  ‹⌈log⇩2 (card Γ)⌉›, the fewest binary digits that
  index all of ‹Γ›.  Defined combinatorially via ‹LEAST›
  on the predicate ‹card Γ ≤ 2 ^ n›; existence of such an
  ‹n› follows from ‹card Γ ≤ 2 ^ card Γ›
  (HOL.Power.‹less_exp›).

  ❙‹What is counted.›  The index space ‹{..< card Γ}›
  covers ∗‹every› symbol of ‹Γ›: the blank at index
  ‹0› (the anchor ‹gamma_enum› relies on --- see below), and
  the left endmarker ‹le› as an ordinary coded symbol, since
  ‹valid_mttm› permits a machine to write ‹le› at any tape
  position (its only special handling is the single ‹LE4› cell at
  position ‹0›).  So ‹block_width› is genuinely the width of
  this uniform code, not a loose bound on a smaller one --- but it is not
  the ∗‹coding› minimum.  Reserving index ‹0› for the
  blank (so an all-‹BLANK4› block reads back through the same
  accumulator) puts it one digit above
  ‹⌈log⇩2 (card Γ - 1)⌉›, the width for the
  ‹card Γ - 1› non-blank symbols; the two agree except just
  past a power of two.  Detecting the all-‹BLANK4› block directly
  would recover that digit, and additionally giving ‹le› its own
  marker block would reach ‹⌈log⇩2 (card Γ - 2)⌉›
  --- but each costs a marker-detection branch in the read and write
  phases, so that constant-factor gain is deliberately not taken.›

definition block_width :: "'a set ⇒ nat" where
  "block_width Γ = max 1 (LEAST n. card Γ ≤ 2 ^ n)"

text ‹A ∗‹blank-anchored› enumeration of ‹Γ› as a
  bijection to ‹{..< card Γ}› that additionally sends the
  blank ‹bl› to ‹0›.  The anchor is load-bearing for the
  read phase: a blank source cell is encoded as a ‹b›-cell
  all-‹BLANK4› block (‹bit_value = 0›), so the read fold
  is a fixpoint at ‹gamma_unenum Γ bl 0›, which must equal
  ‹bl› — and the decode round-trips force that to
  ‹gamma_enum Γ bl bl = 0›.  Existence of such a bijection
  is unconditional on ‹finite Γ› for ∗‹any›
  ‹bl› (‹ex_bij_betw_anchor› below: swap ‹0› with
  ‹g bl› when ‹bl ∈ Γ›, otherwise free off-domain),
  so the carried ‹bl› needs no ‹bl ∈ Γ› side
  condition.  Downstream proofs reason about ‹bij_betw›- and
  anchor-derived facts only; the Hilbert choice picks one specific
  anchored bijection.›

definition gamma_enum :: "'a set ⇒ 'a ⇒ 'a ⇒ nat" where
  "gamma_enum Γ bl =
     (SOME f. bij_betw f Γ {..< card Γ} ∧ f bl = 0)"

text ‹Render a natural number as a fixed-length ‹sym4›
  bit list (‹BIT0› / ‹BIT1› only).  The list has
  shape ‹[bit⇩b⇩-⇩1, …, bit⇩1, bit⇩0]›:
  most-significant bit at the head, least-significant bit at
  the tail.  For ‹n ≥ 2 ^ b› the high bits are dropped
  (only the low ‹b› bits are rendered).›

fun nat_to_bits :: "nat ⇒ nat ⇒ sym4 list" where
  "nat_to_bits 0 _ = []"
| "nat_to_bits (Suc k) n =
     nat_to_bits k (n div 2)
       @ [if n mod 2 = 0 then BIT0 else BIT1]"

subsection ‹Per-symbol encoder›

text ‹Encoding a single ‹'a›-symbol as a fixed-length list of
  ‹sym4›-symbols, parameterised over the source alphabet
  ‹Γ› (a finite set, passed explicitly as a value rather
  than through a type-class constraint, so the construction is uniform
  over all source alphabets).  The
  length ‹b› is the slowdown factor; the encoding is
  injective on ‹Γ›.  The two bit symbols ‹BIT0›,
  ‹BIT1› carry the payload; ‹LE4› and ‹BLANK4›
  do not appear in any encoder image.  For ‹x ∉ Γ› the
  encoder produces a value that's structurally well-shaped (a
  ‹b›-cell bit list) but semantically arbitrary —
  downstream proofs always operate on ‹x ∈ Γ›.›

definition encode_symbol ::
  "'a set ⇒ 'a ⇒ 'a ⇒ sym4 list" where
  "encode_symbol Γ bl x = nat_to_bits (block_width Γ) (gamma_enum Γ bl x)"

text ‹Encoding an input word as a flat list of ‹sym4›-symbols
  (concatenation of per-symbol encodings under the given ‹Γ›).›

definition encode_input_ar ::
  "'a set ⇒ 'a ⇒ 'a list ⇒ sym4 list" where
  "encode_input_ar Γ bl w = concat (map (encode_symbol Γ bl) w)"

subsection ‹Per-symbol encoder lemmas›

text ‹The encoded list has length ‹b›, by induction
  on the block width.  Total — no ‹x ∈ Γ› precondition is
  needed.›

lemma length_nat_to_bits [simp]:
  "length (nat_to_bits k n) = k"
  by (induct k arbitrary: n) auto

lemma length_encode_symbol [simp]:
  "length (encode_symbol Γ bl x) = block_width Γ"
  unfolding encode_symbol_def by simp

text ‹Every cell of an encoded symbol is in the bit alphabet
  ‹{BIT0, BIT1}›.  In particular, the substrate-reserved
  markers ‹LE4› and ‹BLANK4› never appear in an
  encoder image.›

lemma set_nat_to_bits:
  "set (nat_to_bits k n) ⊆ {BIT0, BIT1}"
  by (induct k arbitrary: n) auto

lemma encode_symbol_cell_domain:
  "set (encode_symbol Γ bl x) ⊆ {BIT0, BIT1}"
  unfolding encode_symbol_def
  by (rule set_nat_to_bits)

text ‹The enumeration ‹gamma_enum Γ bl› is a genuine bijection
  from ‹Γ› to ‹{..< card Γ}› whenever ‹Γ› is
  finite.  Existence is library
  (‹ex_bij_betw_finite_nat›); the Hilbert-choice operator
  picks one such bijection.›

text ‹Existence of a blank-anchored bijection
  ‹Γ → {..< card Γ}› sending ‹bl› to ‹0›,
  unconditional on ‹finite Γ› for any ‹bl›.  Take any
  bijection ‹g› (library ‹ex_bij_betw_finite_nat›); if
  ‹bl ∈ Γ›, post-compose with the nat-level transposition of
  ‹0› and ‹g bl› (both ‹< card Γ›), which is a
  ‹bij_betw› of ‹{..< card Γ}› onto itself by
  ‹endo_inj_surj›; if ‹bl ∉ Γ›, just override
  ‹g› at ‹bl› (off-domain, so ‹bij_betw› is
  unchanged by ‹bij_betw_cong›).›

lemma ex_bij_betw_anchor:
  fixes Γ :: "'a set" and bl :: 'a
  assumes finG: "finite Γ"
  shows "∃f. bij_betw f Γ {..< card Γ} ∧ f bl = 0"
proof -
  obtain g where g: "bij_betw g Γ {..< card Γ}"
    using ex_bij_betw_finite_nat[OF finG] by (auto simp: atLeast0LessThan)
  show ?thesis
  proof (cases "bl ∈ Γ")
    case False
    have agree: "⋀x. x ∈ Γ ⟹ (g(bl := 0)) x = g x"
      using False by auto
    have "bij_betw (g(bl := 0)) Γ {..< card Γ}"
      using g agree by (metis bij_betw_cong)
    moreover have "(g(bl := 0)) bl = 0" by simp
    ultimately show ?thesis by blast
  next
    case True
    have npos: "0 < card Γ" using True finG by (auto simp: card_gt_0_iff)
    have gbl: "g bl < card Γ" using g True by (auto simp: bij_betw_def)
    let ?s = "λi. if i = 0 then g bl else if i = g bl then 0 else i"
    have into: "?s ` {..< card Γ} ⊆ {..< card Γ}"
      using gbl npos by auto
    have inj: "inj_on ?s {..< card Γ}"
      by (auto simp: inj_on_def split: if_splits)
    have "bij_betw ?s {..< card Γ} {..< card Γ}"
      unfolding bij_betw_def
      using inj endo_inj_surj[OF finite_lessThan into inj] by blast
    from bij_betw_trans[OF g this]
    have "bij_betw (?s ∘ g) Γ {..< card Γ}" .
    moreover have "(?s ∘ g) bl = 0" using gbl by (auto simp: comp_def)
    ultimately show ?thesis by blast
  qed
qed

lemma gamma_enum_anchor:
  assumes "finite Γ"
  shows "bij_betw (gamma_enum Γ bl) Γ {..< card Γ}
           ∧ gamma_enum Γ bl bl = 0"
  unfolding gamma_enum_def
  using ex_bij_betw_anchor[OF assms] by (rule someI_ex)

lemma gamma_enum_bij:
  assumes "finite Γ"
  shows "bij_betw (gamma_enum Γ bl) Γ {..< card Γ}"
  using gamma_enum_anchor[OF assms] by simp

text ‹The anchor: the blank-anchored enumeration sends the blank to
  ‹0›.  This is what makes an all-‹BLANK4› block decode to
  ‹bl› (‹decode_blank›).›

lemma gamma_enum_blank:
  assumes "finite Γ"
  shows "gamma_enum Γ bl bl = 0"
  using gamma_enum_anchor[OF assms] by simp

lemma gamma_enum_lt_card:
  assumes "finite Γ" and "x ∈ Γ"
  shows "gamma_enum Γ bl x < card Γ"
proof -
  from gamma_enum_bij[OF ‹finite Γ›] ‹x ∈ Γ›
  have "gamma_enum Γ bl x ∈ {..< card Γ}"
    by (auto simp: bij_betw_def)
  thus ?thesis by simp
qed

text ‹The cardinality of ‹Γ› fits in ‹b› bits:
  ‹card Γ ≤ 2 ^ b›.  This is the structural
  bound that underwrites injectivity: every enumeration value
  ‹gamma_enum Γ bl x < card Γ› for ‹x ∈ Γ› is in the
  range where ‹nat_to_bits› is injective.›

lemma card_le_two_pow_block_width: "card Γ ≤ 2 ^ block_width Γ"
proof -
  have ex: "∃n. card Γ ≤ 2 ^ n"
    using less_exp[of "card Γ"] by (intro exI[of _ "card Γ"]) simp
  let ?m = "LEAST n. card Γ ≤ 2 ^ n"
  have m_bound: "card Γ ≤ 2 ^ ?m"
    using LeastI_ex[OF ex] .
  have "?m ≤ block_width Γ"
    unfolding block_width_def by simp
  hence "(2::nat) ^ ?m ≤ 2 ^ block_width Γ"
    by (rule power_increasing) simp
  with m_bound show ?thesis by linarith
qed

text ‹Minimality (the lower edge): ‹b› is the ∗‹smallest› width
  that indexes all of ‹Γ›, so once ‹card Γ ≥ 2› one
  bit fewer does not suffice --- ‹2 ^ (b - 1) < card Γ›.  With
  ‹card_le_two_pow_block_width› this pins ‹b› to
  ‹⌈log⇩2 (card Γ)⌉› exactly: ‹b› is a ∗‹step
  function› of ‹card Γ›, constant on each band
  ‹2 ^ (b - 1) < card Γ ≤ 2 ^ b› and jumping by one as
  ‹card Γ› crosses a power of two (‹4 → 5›,
  ‹8 → 9›, ‹16 → 17›).  The slowdown factor therefore
  rises in unit steps at the powers of two, not smoothly with alphabet
  size.  This is minimality for the ∗‹uniform› code that indexes
  every symbol of ‹Γ› with the blank at index ‹0›; the
  ∗‹coding› minimum (the non-blank symbols alone) sits one digit
  lower just past each power of two --- see ‹block_width›.›

lemma two_pow_block_width_pred_less_card:
  assumes card2: "2 ≤ card Γ"
  shows "2 ^ (block_width Γ - 1) < card Γ"
proof -
  have ex: "∃n. card Γ ≤ 2 ^ n"
    using less_exp[of "card Γ"] by (intro exI[of _ "card Γ"]) simp
  let ?m = "LEAST n. card Γ ≤ 2 ^ n"
  have notP0: "¬ card Γ ≤ 2 ^ (0::nat)" using card2 by simp
  have m_pos: "0 < ?m"
  proof (rule ccontr)
    assume "¬ 0 < ?m"
    then have "?m = 0" by simp
    then have "card Γ ≤ 2 ^ (0::nat)" using LeastI_ex[OF ex] by simp
    with notP0 show False by simp
  qed
  hence bw: "block_width Γ = ?m" unfolding block_width_def by simp
  have "block_width Γ - 1 < ?m" using bw m_pos by simp
  hence "¬ card Γ ≤ 2 ^ (block_width Γ - 1)" by (rule not_less_Least)
  thus ?thesis by simp
qed

text ‹The bit-renderer is injective on inputs bounded by
  ‹2 ^ b›: two values with the same ‹b›-bit
  representation are equal.  Proven by induction on ‹b›:
  the head of the bit list determines the high bit ‹n div 2›
  (recursive case), and the tail single element determines the
  low bit ‹n mod 2›; combining via
  ‹n = 2 ⋅ (n div 2) + n mod 2› gives equality.›

lemma nat_to_bits_inj_bounded:
  assumes "n1 < 2 ^ k"
      and "n2 < 2 ^ k"
      and "nat_to_bits k n1 = nat_to_bits k n2"
  shows "n1 = n2"
  using assms
proof (induct k arbitrary: n1 n2)
  case 0
  thus ?case by simp
next
  case (Suc k)
  from ‹nat_to_bits (Suc k) n1 = nat_to_bits (Suc k) n2›
  have eq:
    "nat_to_bits k (n1 div 2)
       @ [if n1 mod 2 = 0 then BIT0 else BIT1]
     = nat_to_bits k (n2 div 2)
       @ [if n2 mod 2 = 0 then BIT0 else BIT1]"
    by simp
  hence pref_eq:
    "nat_to_bits k (n1 div 2) = nat_to_bits k (n2 div 2)"
    and suf_eq:
    "(if n1 mod 2 = 0 then BIT0 else BIT1)
       = (if n2 mod 2 = 0 then BIT0 else BIT1)"
    by simp_all
  from suf_eq have mod_zero_iff:
    "n1 mod 2 = 0 ⟷ n2 mod 2 = 0"
    by (auto split: if_split_asm)
  have "n1 mod 2 < 2" and "n2 mod 2 < 2" by simp_all
  with mod_zero_iff have mod_eq: "n1 mod 2 = n2 mod 2"
    by (cases "n1 mod 2 = 0"; cases "n2 mod 2 = 0") auto
  from ‹n1 < 2 ^ Suc k› have lt1: "n1 div 2 < 2 ^ k" by simp
  from ‹n2 < 2 ^ Suc k› have lt2: "n2 div 2 < 2 ^ k" by simp
  from Suc.hyps[OF lt1 lt2 pref_eq]
  have div_eq: "n1 div 2 = n2 div 2" .
  have "n1 = 2 * (n1 div 2) + n1 mod 2" by simp
  also from div_eq mod_eq have "… = 2 * (n2 div 2) + n2 mod 2"
    by simp
  also have "… = n2" by simp
  finally show ?case .
qed

text ‹Injectivity-on-‹Γ›: distinct source symbols in ‹Γ›
  produce distinct encoder images.  This is the load-bearing
  property for language preservation: no two source symbols
  collide under the encoder.›

lemma encode_symbol_inj_on_Gamma:
  assumes "finite Γ"
      and "x ∈ Γ" and "y ∈ Γ"
      and "encode_symbol Γ bl x = encode_symbol Γ bl y"
  shows "x = y"
proof -
  from ‹encode_symbol Γ bl x = encode_symbol Γ bl y›
  have bits_eq:
    "nat_to_bits (block_width Γ) (gamma_enum Γ bl x)
       = nat_to_bits (block_width Γ) (gamma_enum Γ bl y)"
    by (simp add: encode_symbol_def)
  have lt_x: "gamma_enum Γ bl x < 2 ^ block_width Γ"
    using gamma_enum_lt_card[OF ‹finite Γ› ‹x ∈ Γ›, of bl]
          card_le_two_pow_block_width[of Γ]
    by linarith
  have lt_y: "gamma_enum Γ bl y < 2 ^ block_width Γ"
    using gamma_enum_lt_card[OF ‹finite Γ› ‹y ∈ Γ›, of bl]
          card_le_two_pow_block_width[of Γ]
    by linarith
  from nat_to_bits_inj_bounded[OF lt_x lt_y bits_eq]
  have enum_eq: "gamma_enum Γ bl x = gamma_enum Γ bl y" .
  have "inj_on (gamma_enum Γ bl) Γ"
    using gamma_enum_bij[OF ‹finite Γ›]
    by (simp add: bij_betw_def)
  from this enum_eq ‹x ∈ Γ› ‹y ∈ Γ› show ?thesis
    by (rule inj_onD)
qed

text ‹Structural properties of the input-word encoder.  These
  follow directly from the ‹concat (map (encode_symbol Γ bl)
  …)› definition and are useful for the validation-phase
  reach lemmas in later slices.›

lemma encode_input_ar_Nil [simp]:
  "encode_input_ar Γ bl [] = []"
  unfolding encode_input_ar_def by simp

lemma encode_input_ar_append:
  "encode_input_ar Γ bl (w1 @ w2)
     = encode_input_ar Γ bl w1 @ encode_input_ar Γ bl w2"
  unfolding encode_input_ar_def by simp

lemma length_encode_input_ar:
  "length (encode_input_ar Γ bl w) = block_width Γ * length w"
  unfolding encode_input_ar_def
  by (induct w) auto

text ‹Uniform-width block indexing: when every block ‹f x›
  has the same length ‹K›, the ‹(i ⋅ K + j)›-th cell
  of ‹concat (map f xs)› is the ‹j›-th cell of the
  ‹i›-th block.  The list-level fact underlying the
  initial-tape correspondence: ‹encode_input_ar› is exactly
  such a uniform concatenation, every block ‹b›
  wide by ‹length_encode_symbol›.›
lemma nth_concat_map_uniform:
  assumes K: "⋀x. length (f x) = K"
      and i: "i < length xs"
      and j: "j < K"
  shows "concat (map f xs) ! (i * K + j) = f (xs ! i) ! j"
  using i
proof (induct xs arbitrary: i)
  case Nil
  then show ?case by simp
next
  case (Cons x xs)
  show ?case
  proof (cases i)
    case 0
    have "concat (map f (x # xs)) ! (i * K + j)
            = (f x @ concat (map f xs)) ! j"
      using 0 by simp
    also have "… = f x ! j"
      using j K[of x] by (simp add: nth_append)
    finally show ?thesis using 0 by simp
  next
    case (Suc i')
    have i'len: "i' < length xs" using Cons.prems Suc by simp
    have idx: "i * K + j = length (f x) + (i' * K + j)"
      using Suc K[of x] by simp
    have "concat (map f (x # xs)) ! (i * K + j)
            = concat (map f xs) ! (i' * K + j)"
      using idx by (simp add: nth_append)
    also have "… = f (xs ! i') ! j"
      using Cons.hyps[OF i'len] .
    finally show ?thesis using Suc by simp
  qed
qed

lemma nth_encode_input_ar:
  assumes "i < length w" and "j < block_width Γ"
  shows "encode_input_ar Γ bl w ! (i * block_width Γ + j)
           = encode_symbol Γ bl (w ! i) ! j"
  unfolding encode_input_ar_def
  by (rule nth_concat_map_uniform[OF length_encode_symbol assms])

subsection ‹Per-symbol decoder helpers›

text ‹Bit value of a ‹sym4› cell.  ‹BIT1› contributes
  1, every other symbol contributes 0; the non-bit symbols
  (‹BIT0›, ‹LE4›, ‹BLANK4›) are conflated to
  zero — junk-in, junk-out — so the decoder produces a
  well-defined nat even on malformed input.  Validity checking
  is performed separately by ‹decode_symbol›'s cell-domain
  test.›

fun bit_value :: "sym4 ⇒ nat" where
  "bit_value BIT0 = 0"
| "bit_value BIT1 = 1"
| "bit_value LE4 = 0"
| "bit_value BLANK4 = 0"

text ‹Read a ‹sym4› list as a binary number, MSB at the
  head (matches ‹nat_to_bits›'s output shape).  Each
  position contributes ‹bit_value› times the appropriate
  power of two.›

fun bits_to_nat :: "sym4 list ⇒ nat" where
  "bits_to_nat [] = 0"
| "bits_to_nat (b # bs) = bit_value b * 2 ^ length bs + bits_to_nat bs"

text ‹Snoc-form of ‹bits_to_nat›: appending a low bit
  shifts the existing value left and adds the new bit.  This
  is the inductive workhorse for the round-trip lemma — it
  matches ‹nat_to_bits›'s recursive shape (which appends
  the LSB at the tail).›

lemma bits_to_nat_snoc:
  "bits_to_nat (xs @ [b]) = 2 * bits_to_nat xs + bit_value b"
  by (induct xs) auto

text ‹Round-trip on bounded naturals: rendering ‹n› as
  a ‹b›-bit list and reading it back recovers ‹n›,
  provided ‹n < 2 ^ b›.  Proof by induction on ‹b›:
  the snoc-form of ‹bits_to_nat› peels off the
  trailing bit, the IH handles the prefix ‹n div 2›, and
  ‹n = 2 ⋅ (n div 2) + n mod 2› reassembles.›

lemma bit_value_low_bit:
  "bit_value (if n mod 2 = 0 then BIT0 else BIT1) = n mod 2"
  using mod_less_divisor[of 2 n] by (auto split: if_split)

lemma bits_to_nat_nat_to_bits:
  assumes "n < 2 ^ k"
  shows "bits_to_nat (nat_to_bits k n) = n"
  using assms
proof (induct k arbitrary: n)
  case 0
  thus ?case by simp
next
  case (Suc k)
  have lt: "n div 2 < 2 ^ k"
    using ‹n < 2 ^ Suc k› by simp
  have "bits_to_nat (nat_to_bits (Suc k) n)
          = bits_to_nat
              (nat_to_bits k (n div 2)
                 @ [if n mod 2 = 0 then BIT0 else BIT1])"
    by simp
  also have "…
          = 2 * bits_to_nat (nat_to_bits k (n div 2))
              + bit_value (if n mod 2 = 0 then BIT0 else BIT1)"
    by (rule bits_to_nat_snoc)
  also have "… = 2 * (n div 2) + (n mod 2)"
    using Suc.hyps[OF lt] bit_value_low_bit[of n] by simp
  also have "… = n" by presburger
  finally show ?case .
qed

subsection ‹Per-symbol decoder›

text ‹Partial inverse of ‹encode_symbol›.  Returns
  ‹Some x› when the input list:
  ▸ has length ‹b› (correct cell count);
  ▸ contains only ‹BIT0› / ‹BIT1› cells (no
    substrate-reserved markers); and
  ▸ has binary interpretation strictly below
    ‹card Γ› (in the enumeration range).

  Otherwise returns ‹None›.  The validation phase in
  later slices implements this check as a sequence of substep
  transitions; the abstract ‹decode_symbol› partial
  function is the specification target.›

definition decode_symbol ::
  "'a set ⇒ 'a ⇒ sym4 list ⇒ 'a option" where
  "decode_symbol Γ bl ys =
     (if length ys = block_width Γ
              ∧ set ys ⊆ {BIT0, BIT1}
              ∧ bits_to_nat ys < card Γ
      then Some (inv_into Γ (gamma_enum Γ bl) (bits_to_nat ys))
      else None)"

text ‹Round-trip: decoding an encoded symbol from
  ‹Γ› recovers the source value.  All three validity
  preconditions of ‹decode_symbol› are satisfied by the
  encoder image; ‹inv_into› resolves to ‹x› via
  ‹gamma_enum›'s injectivity-on-‹Γ›.›

lemma decode_symbol_encode_symbol:
  assumes "finite Γ" and "x ∈ Γ"
  shows "decode_symbol Γ bl (encode_symbol Γ bl x) = Some x"
proof -
  let ?ys = "encode_symbol Γ bl x"
  have len: "length ?ys = block_width Γ" by simp
  have cd: "set ?ys ⊆ {BIT0, BIT1}"
    by (rule encode_symbol_cell_domain)
  have lt_x: "gamma_enum Γ bl x < 2 ^ block_width Γ"
    using gamma_enum_lt_card[OF ‹finite Γ› ‹x ∈ Γ›, of bl]
          card_le_two_pow_block_width[of Γ]
    by linarith
  have bn: "bits_to_nat ?ys = gamma_enum Γ bl x"
    unfolding encode_symbol_def
    by (rule bits_to_nat_nat_to_bits[OF lt_x])
  have lt_card: "bits_to_nat ?ys < card Γ"
    using bn gamma_enum_lt_card[OF ‹finite Γ› ‹x ∈ Γ›] by simp
  have inj: "inj_on (gamma_enum Γ bl) Γ"
    using gamma_enum_bij[OF ‹finite Γ›]
    by (simp add: bij_betw_def)
  have inv_eq: "inv_into Γ (gamma_enum Γ bl) (bits_to_nat ?ys) = x"
    using bn inv_into_f_f[OF inj ‹x ∈ Γ›] by simp
  show ?thesis
    unfolding decode_symbol_def
    using len cd lt_card inv_eq by simp
qed

text ‹A total form of the symbol decoder, indexed by a
  natural number rather than a bit list.  For ‹n < card
  Γ›, returns the unique ‹x ∈ Γ› with
  ‹gamma_enum Γ bl x = n› (via ‹inv_into›);
  for ‹n ≥ card Γ›, returns the blank
  ‹bl› as a defensive fallback.  Used by
  ‹ar_delta_read›'s per-bit accumulator to maintain
  ‹buf› as a partial-decoded ‹'a› value: at
  every per-bit substep before the boundary, the partial nat is
  strictly less than ‹2 ^ (b - 1) < card Γ›
  (since ‹b› is the *least* ‹n›
  with ‹card Γ ≤ 2 ^ n›), so the fallback is
  never substantively reached for valid inputs; only the
  boundary substep can land out of range under
  non-encoder-image inputs, where the language theorem doesn't
  care.›

definition gamma_unenum :: "'a set ⇒ 'a ⇒ nat ⇒ 'a" where
  "gamma_unenum Γ bl n =
     (if n < card Γ
      then inv_into Γ (gamma_enum Γ bl) n
      else bl)"

text ‹Enumeration round-trips between ‹gamma_enum› and its
  total inverse ‹gamma_unenum›, the arithmetic core the read
  phase's incremental decode rests on.  ‹gamma_enum ∘
  gamma_unenum› is the identity on the in-range index set
  ‹⦃0..<card Γ⦄› (where ‹gamma_unenum› resolves
  to ‹inv_into› and ‹gamma_enum› is surjective onto that
  set), and ‹gamma_unenum ∘ gamma_enum› is the identity on
  ‹Γ› (where ‹gamma_enum› is injective and lands
  below ‹card Γ›).›

lemma gamma_enum_gamma_unenum:
  assumes "finite Γ" and "n < card Γ"
  shows "gamma_enum Γ bl (gamma_unenum Γ bl n) = n"
proof -
  have img: "gamma_enum Γ bl ` Γ = {..<card Γ}"
    using gamma_enum_bij[OF assms(1)] by (simp add: bij_betw_def)
  have "n ∈ gamma_enum Γ bl ` Γ" using assms(2) img by simp
  hence "gamma_enum Γ bl (inv_into Γ (gamma_enum Γ bl) n) = n"
    by (rule f_inv_into_f)
  thus ?thesis using assms(2) by (simp add: gamma_unenum_def)
qed

lemma gamma_unenum_gamma_enum:
  assumes "finite Γ" and "x ∈ Γ"
  shows "gamma_unenum Γ bl (gamma_enum Γ bl x) = x"
proof -
  have lt: "gamma_enum Γ bl x < card Γ"
    by (rule gamma_enum_lt_card[OF assms])
  have inj: "inj_on (gamma_enum Γ bl) Γ"
    using gamma_enum_bij[OF assms(1)] by (simp add: bij_betw_def)
  have "inv_into Γ (gamma_enum Γ bl) (gamma_enum Γ bl x) = x"
    by (rule inv_into_f_f[OF inj assms(2)])
  thus ?thesis using lt by (simp add: gamma_unenum_def)
qed

text ‹Reading an encoded symbol back via ‹bits_to_nat›
  recovers its enumeration index, the named form of the local
  ‹bn› fact inside ‹decode_symbol_encode_symbol›.  Needed
  by the read-phase accumulator below.›

lemma bits_to_nat_encode_symbol:
  assumes "finite Γ" and "x ∈ Γ"
  shows "bits_to_nat (encode_symbol Γ bl x) = gamma_enum Γ bl x"
proof -
  have lt_x: "gamma_enum Γ bl x < 2 ^ block_width Γ"
    using gamma_enum_lt_card[OF assms, of bl] card_le_two_pow_block_width[of Γ]
    by linarith
  show ?thesis
    unfolding encode_symbol_def by (rule bits_to_nat_nat_to_bits[OF lt_x])
qed

text ‹The read-phase accumulator: one bit-cell folded into the
  running symbol.  Mirrors the per-bit update the read substeps
  perform — ‹buf := gamma_unenum (2 ⋅ gamma_enum buf +
  bit_value c)› — reading the ‹b›-cell block most-significant
  bit first.›

definition ar_acc :: "'a set ⇒ 'a ⇒ 'a ⇒ sym4 ⇒ 'a" where
  "ar_acc Γ bl b c = gamma_unenum Γ bl (2 * gamma_enum Γ bl b + bit_value c)"

text ‹Folding the accumulator from the seed ‹gamma_unenum 0›
  over a bit list whose value is in enumeration range yields exactly
  ‹gamma_unenum (bits_to_nat ys)›.  Proof by ‹rev_induct›:
  appending a low bit shifts the running value left and adds it
  (‹bits_to_nat_snoc›), the prefix value stays in range
  (‹bits_to_nat zs ≤ bits_to_nat (zs @ [b])›, no separate
  ‹take›-bound lemma needed), and the ‹gamma_enum ∘
  gamma_unenum› round-trip cancels at each step.›

lemma foldl_ar_acc_eq:
  assumes "finite Γ"
  shows "set ys ⊆ {BIT0, BIT1} ⟹ bits_to_nat ys < card Γ
          ⟹ foldl (ar_acc Γ bl) (gamma_unenum Γ bl 0) ys
                = gamma_unenum Γ bl (bits_to_nat ys)"
proof (induct ys rule: rev_induct)
  case Nil
  show ?case by simp
next
  case (snoc b zs)
  have set_zs: "set zs ⊆ {BIT0, BIT1}" using snoc.prems(1) by simp
  have snoc_eq: "bits_to_nat (zs @ [b]) = 2 * bits_to_nat zs + bit_value b"
    by (rule bits_to_nat_snoc)
  have bound_zs: "bits_to_nat zs < card Γ"
    using snoc.prems(2) snoc_eq by linarith
  have IH: "foldl (ar_acc Γ bl) (gamma_unenum Γ bl 0) zs
              = gamma_unenum Γ bl (bits_to_nat zs)"
    using snoc.hyps set_zs bound_zs by blast
  have ge_zs: "gamma_enum Γ bl
                 (foldl (ar_acc Γ bl) (gamma_unenum Γ bl 0) zs)
               = bits_to_nat zs"
    using IH gamma_enum_gamma_unenum[OF assms bound_zs] by simp
  have "foldl (ar_acc Γ bl) (gamma_unenum Γ bl 0) (zs @ [b])
          = ar_acc Γ bl
              (foldl (ar_acc Γ bl) (gamma_unenum Γ bl 0) zs) b"
    by simp
  also have "… = gamma_unenum Γ bl (2 * bits_to_nat zs + bit_value b)"
    by (simp add: ar_acc_def ge_zs)
  also have "… = gamma_unenum Γ bl (bits_to_nat (zs @ [b]))"
    using snoc_eq by simp
  finally show ?case .
qed

text ‹Read-phase decode correctness: folding the accumulator over
  a symbol's encoding recovers the symbol.  This is the arithmetic
  content the read phase delivers — every tape's ‹buf› field,
  after walking its ‹b›-cell block, holds the source cell's
  value.›

lemma foldl_ar_acc_encode_symbol:
  assumes "finite Γ" and "x ∈ Γ"
  shows "foldl (ar_acc Γ bl) (gamma_unenum Γ bl 0) (encode_symbol Γ bl x) = x"
proof -
  have cd: "set (encode_symbol Γ bl x) ⊆ {BIT0, BIT1}"
    by (rule encode_symbol_cell_domain)
  have bn: "bits_to_nat (encode_symbol Γ bl x) = gamma_enum Γ bl x"
    by (rule bits_to_nat_encode_symbol[OF assms])
  have lt: "bits_to_nat (encode_symbol Γ bl x) < card Γ"
    using bn gamma_enum_lt_card[OF assms] by simp
  have "foldl (ar_acc Γ bl) (gamma_unenum Γ bl 0) (encode_symbol Γ bl x)
          = gamma_unenum Γ bl (bits_to_nat (encode_symbol Γ bl x))"
    by (rule foldl_ar_acc_eq[OF assms(1) cd lt])
  also have "… = gamma_unenum Γ bl (gamma_enum Γ bl x)" using bn by simp
  also have "… = x" by (rule gamma_unenum_gamma_enum[OF assms])
  finally show ?thesis .
qed

text ‹The decoder's neutral element is the blank: ‹gamma_unenum
  Γ bl 0 = bl›, since the anchor puts ‹bl› at index
  ‹0› and the enumeration is injective.›

lemma gamma_unenum_zero:
  assumes "finite Γ" and "bl ∈ Γ"
  shows "gamma_unenum Γ bl 0 = bl"
proof -
  have npos: "0 < card Γ" using assms by (auto simp: card_gt_0_iff)
  have inj: "inj_on (gamma_enum Γ bl) Γ"
    using gamma_enum_bij[OF assms(1)] by (simp add: bij_betw_def)
  have "gamma_unenum Γ bl 0 = inv_into Γ (gamma_enum Γ bl) 0"
    using npos by (simp add: gamma_unenum_def)
  also have "…
        = inv_into Γ (gamma_enum Γ bl) (gamma_enum Γ bl bl)"
    using gamma_enum_blank[OF assms(1)] by simp
  also have "… = bl" by (rule inv_into_f_f[OF inj assms(2)])
  finally show ?thesis .
qed

text ‹An all-‹BLANK4› block decodes to the blank: ‹bl› is a
  fixpoint of the accumulator on a ‹BLANK4› cell (‹2 ⋅
  gamma_enum bl + 0 = 0›, decoding back to ‹bl›), so folding
  any number of ‹BLANK4› cells from ‹bl› stays ‹bl›.
  This is the read-phase decode correctness for the blank cell, the
  ‹BLANK4› counterpart of ‹foldl_ar_acc_encode_symbol›.›

lemma foldl_ar_acc_blank:
  assumes "finite Γ" and "bl ∈ Γ"
  shows "foldl (ar_acc Γ bl) bl (replicate k BLANK4) = bl"
proof (induct k)
  case 0
  show ?case by simp
next
  case (Suc k)
  have step: "ar_acc Γ bl bl BLANK4 = bl"
    unfolding ar_acc_def
    using gamma_enum_blank[OF assms(1)] gamma_unenum_zero[OF assms] by simp
  have "foldl (ar_acc Γ bl) bl (replicate (Suc k) BLANK4)
          = foldl (ar_acc Γ bl) (ar_acc Γ bl bl BLANK4)
                  (replicate k BLANK4)"
    by (simp add: replicate_Suc)
  also have "… = foldl (ar_acc Γ bl) bl (replicate k BLANK4)"
    using step by simp
  also have "… = bl" by (rule Suc.hyps)
  finally show ?case .
qed

end