Encoding.thy

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