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

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