# 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
```