theory Ex1
imports "Parser"
begin

text {* example 1, equivalent to example 2 from Terms *}

atom_decl name

ML {* val _ = recursive := false *}
nominal_datatype lam =
  VAR "name"
| APP "lam" "lam"
| LAM x::"name" t::"lam" bind x in t
| LET bp::"bp" t::"lam"   bind "bi bp" in t
and bp =
  BP "name" "lam"
binder
  bi::"bp \<Rightarrow> atom set"
where
  "bi (BP x t) = {atom x}"

thm lam_bp.fv
thm lam_bp.supp
thm lam_bp.eq_iff
thm lam_bp.bn
thm lam_bp.perm
thm lam_bp.induct
thm lam_bp.inducts
thm lam_bp.distinct
ML {* Sign.of_sort @{theory} (@{typ lam}, @{sort fs}) *}
thm lam_bp.fv[simplified lam_bp.supp]

end