Theory Encoding

section ‹Encoding›

theory Encoding imports "HOL-Library.Nat_Bijection" Syntax begin

abbreviation infix_sum_encode (infixr ‹$› 100) where
  ‹c $ x ≡ sum_encode (c x)›

lemma lt_sum_encode_Inr: ‹n < Inr $ n›
  unfolding sum_encode_def by simp

lemma sum_prod_decode_lt [simp]: ‹sum_decode n = Inr b ⟹ (x, y) = prod_decode b ⟹ y < Suc n›
  by (metis le_prod_encode_2 less_Suc_eq lt_sum_encode_Inr order_le_less_trans
      prod_decode_inverse sum_decode_inverse)

lemma sum_prod_decode_lt_Suc [simp]:
  ‹sum_decode n = Inr b ⟹ (Suc x, y) = prod_decode b ⟹ x < Suc n›
  by (metis dual_order.strict_trans le_prod_encode_1 lessI linorder_not_less lt_sum_encode_Inr
      not_less_eq prod_decode_inverse sum_decode_inverse)

lemma lt_list_encode: ‹n [∈] ns ⟹ n < list_encode ns›
proof (induct ns)
  case (Cons m ns)
  then show ?case
    using le_prod_encode_1 le_prod_encode_2
    by (metis dual_order.strict_trans1 le_imp_less_Suc less_SucI list_encode.simps(2) set_ConsD)
qed simp

lemma prod_Suc_list_decode_lt [simp]:
  ‹(x, Suc y) = prod_decode n ⟹ y' [∈] (list_decode y) ⟹ y' < n›
  by (metis Suc_le_lessD lt_list_encode le_prod_encode_2 list_decode_inverse order_less_trans
      prod_decode_inverse)

subsection ‹Terms›

primrec nat_of_tm :: ‹tm ⇒ nat› where
  ‹nat_of_tm (❙#n) = prod_encode (n, 0)›
| ‹nat_of_tm (❙†f ts) = prod_encode (f, Suc (list_encode (map nat_of_tm ts)))›

function tm_of_nat :: ‹nat ⇒ tm› where
  ‹tm_of_nat n = (case prod_decode n of
    (n, 0) ⇒ ❙#n
  | (f, Suc ts) ⇒ ❙†f (map tm_of_nat (list_decode ts)))›
  by pat_completeness auto
termination by (relation ‹measure id›) simp_all

lemma tm_nat: ‹tm_of_nat (nat_of_tm t) = t›
  by (induct t) (simp_all add: map_idI)

lemma surj_tm_of_nat: ‹surj tm_of_nat›
  unfolding surj_def using tm_nat by metis

subsection ‹Formulas›

primrec nat_of_fm :: ‹fm ⇒ nat› where
  ‹nat_of_fm ❙⊥ = 0›
| ‹nat_of_fm (❙‡P ts) = Suc (Inl $ prod_encode (P, list_encode (map nat_of_tm ts)))›
| ‹nat_of_fm (p ❙⟶ q) = Suc (Inr $ prod_encode (Suc (nat_of_fm p), nat_of_fm q))›
| ‹nat_of_fm (❙∀p) = Suc (Inr $ prod_encode (0, nat_of_fm p))›

function fm_of_nat :: ‹nat ⇒ fm› where
  ‹fm_of_nat 0 = ❙⊥›
| ‹fm_of_nat (Suc n) = (case sum_decode n of
    Inl n ⇒ let (P, ts) = prod_decode n in ❙‡P (map tm_of_nat (list_decode ts))
  | Inr n ⇒ (case prod_decode n of
      (Suc p, q) ⇒ fm_of_nat p ❙⟶ fm_of_nat q
    | (0, p) ⇒ ❙∀(fm_of_nat p)))›
  by pat_completeness auto
termination by (relation ‹measure id›) simp_all

lemma fm_nat: ‹fm_of_nat (nat_of_fm p) = p›
  using tm_nat by (induct p) (simp_all add: map_idI)

lemma surj_fm_of_nat: ‹surj fm_of_nat›
  unfolding surj_def using fm_nat by metis

subsection ‹Rules›

text ‹Pick a large number to help encode the Idle rule, so that we never hit it in practice.›

definition idle_nat :: nat where
  ‹idle_nat ≡ 4294967295›

primrec nat_of_rule :: ‹rule ⇒ nat› where
  ‹nat_of_rule Idle = Inl $ prod_encode (0, idle_nat)›
| ‹nat_of_rule (Axiom n ts) = Inl $ prod_encode (Suc n, Suc (list_encode (map nat_of_tm ts)))›
| ‹nat_of_rule FlsL = Inl $ prod_encode (0, 0)›
| ‹nat_of_rule FlsR = Inl $ prod_encode (0, Suc 0)›
| ‹nat_of_rule (ImpL p q) = Inr $ prod_encode (Inl $ nat_of_fm p, Inl $ nat_of_fm q)›
| ‹nat_of_rule (ImpR p q) = Inr $ prod_encode (Inr $ nat_of_fm p, nat_of_fm q)›
| ‹nat_of_rule (UniL t p) = Inr $ prod_encode (Inl $ nat_of_tm t, Inr $ nat_of_fm p)›
| ‹nat_of_rule (UniR p) = Inl $ prod_encode (Suc (nat_of_fm p), 0)›

fun rule_of_nat :: ‹nat ⇒ rule› where
  ‹rule_of_nat n = (case sum_decode n of
    Inl n ⇒ (case prod_decode n of
      (0, 0) ⇒ FlsL
    | (0, Suc 0) ⇒ FlsR
    | (0, n2) ⇒ if n2 = idle_nat then Idle else
      let (p, q) = prod_decode n2 in ImpR (fm_of_nat p) (fm_of_nat q)
    | (Suc n, Suc ts) ⇒ Axiom n (map tm_of_nat (list_decode ts))
    | (Suc p, 0) ⇒ UniR (fm_of_nat p))
  | Inr n ⇒ (let (n1, n2) = prod_decode n in
    case sum_decode n1 of
      Inl n1 ⇒ (case sum_decode n2 of
        Inl q ⇒ ImpL (fm_of_nat n1) (fm_of_nat q)
      | Inr p ⇒ UniL (tm_of_nat n1) (fm_of_nat p))
    | Inr p ⇒ ImpR (fm_of_nat p) (fm_of_nat n2)))›

lemma rule_nat: ‹rule_of_nat (nat_of_rule r) = r›
  using tm_nat fm_nat by (cases r) (simp_all add: map_idI idle_nat_def)

lemma surj_rule_of_nat: ‹surj rule_of_nat›
  unfolding surj_def using rule_nat by metis

end