Theory Lambda_Encoding

(*  Title:       An Encoding of Lambdas in Lambda-Free Higher-Order Logic
    Author:      Jasmin Blanchette <j.c.blanchette at vu.nl>, 2019
    Maintainer:  Jasmin Blanchette <j.c.blanchette at vu.nl>
*)

section ‹An Encoding of Lambdas in Lambda-Free Higher-Order Logic›

theory Lambda_Encoding
imports Lambda_Free_Term
begin

text ‹
This theory defines an encoding of ‹λ›-expressions as ‹λ›-free higher-order terms.
›

locale lambda_encoding =
  fixes
    lam :: 's and
    db :: "nat ⇒ 's"
begin

definition is_db :: "'s ⇒ bool" where
  "is_db f ⟷ (∃i. f = db i)"

fun subst_db :: "nat ⇒ 'v ⇒ ('s, 'v) tm ⇒ ('s, 'v) tm" where
  "subst_db i x (Hd ζ) = Hd (if ζ = Var x then Sym (db i) else ζ)"
| "subst_db i x (App s t) =
   App (subst_db i x s) (subst_db (if head s = Sym lam then i + 1 else i) x t)"

definition raw_db_subst :: "nat ⇒ 'v ⇒ 'v ⇒ ('s, 'v) tm" where
  "raw_db_subst i x = (λy. Hd (if y = x then Sym (db i) else Var y))"

lemma vars_mset_subst_db: "vars_mset (subst_db i x s) = {#y ∈# vars_mset s. y ≠ x#}"
  by (induct s arbitrary: i) (auto elim: hd.set_cases)

lemma head_subst_db: "head (subst_db i x s) = head (subst (raw_db_subst i x) s)"
  by (induct s arbitrary: i) (auto simp: raw_db_subst_def split: hd.split)

lemma args_subst_db:
  "args (subst_db i x s) = map (subst_db (if head s = Sym lam then i + 1 else i) x) (args s)"
  by (induct s arbitrary: i) auto

lemma var_mset_subst_db_subseteq:
  "vars_mset s ⊆# vars_mset t ⟹ vars_mset (subst_db i x s) ⊆# vars_mset (subst_db i x t)"
  by (simp add: vars_mset_subst_db multiset_filter_mono)

end

end