Theory Lambda_Term

(*  Title:      HOL/Datatype_Examples/Lambda_Term.thy
    Author:     Dmitriy Traytel, TU Muenchen
    Author:     Andrei Popescu, TU Muenchen
    Copyright   2012

Lambda-terms.
*)

section ‹Lambda-Terms›

theory Lambda_Term
imports "HOL-Library.FSet"
begin

section ‹Datatype definition›

datatype 'a trm =
  Var 'a |
  App "'a trm" "'a trm" |
  Lam 'a "'a trm" |
  Lt "('a × 'a trm) fset" "'a trm"


subsection ‹Example: The set of all variables varsOf and free variables fvarsOf of a term›

primrec varsOf :: "'a trm ⇒ 'a set" where
  "varsOf (Var a) = {a}"
| "varsOf (App f x) = varsOf f ∪ varsOf x"
| "varsOf (Lam x b) = {x} ∪ varsOf b"
| "varsOf (Lt F t) = varsOf t ∪ (⋃{{x} ∪ X | x X. (x,X) |∈| fimage (map_prod id varsOf) F})"

primrec fvarsOf :: "'a trm ⇒ 'a set" where
  "fvarsOf (Var x) = {x}"
| "fvarsOf (App t1 t2) = fvarsOf t1 ∪ fvarsOf t2"
| "fvarsOf (Lam x t) = fvarsOf t - {x}"
| "fvarsOf (Lt xts t) = fvarsOf t - {x | x X. (x,X) |∈| fimage (map_prod id varsOf) xts} ∪
    (⋃{X | x X. (x,X) |∈| fimage (map_prod id varsOf) xts})"

lemma diff_Un_incl_triv: "⟦A ⊆ D; C ⊆ E⟧ ⟹ A - B ∪ C ⊆ D ∪ E" by blast

lemma in_fimage_map_prod_fset_iff[simp]:
  "(x, y) |∈| fimage (map_prod f g) xts ⟷ (∃ t1 t2. (t1, t2) |∈| xts ∧ x = f t1 ∧ y = g t2)"
  by force

lemma fvarsOf_varsOf: "fvarsOf t ⊆ varsOf t"
proof induct
  case (Lt xts t) thus ?case unfolding fvarsOf.simps varsOf.simps by (elim diff_Un_incl_triv) auto
qed auto

end