theory Ex2
imports "Parser"
begin

text {* example 2 *}

atom_decl name

ML {* val _ = recursive := false  *}
nominal_datatype trm' =
  Var "name"
| App "trm'" "trm'"
| Lam x::"name" t::"trm'"          bind x in t
| Let p::"pat'" "trm'" t::"trm'"   bind "f p" in t
and pat' =
  PN
| PS "name"
| PD "name" "name"
binder
  f::"pat' \<Rightarrow> atom set"
where
  "f PN = {}"
| "f (PD x y) = {atom x, atom y}"
| "f (PS x) = {atom x}"

thm trm'_pat'.fv
thm trm'_pat'.eq_iff
thm trm'_pat'.bn
thm trm'_pat'.perm
thm trm'_pat'.induct
thm trm'_pat'.distinct
thm trm'_pat'.fv[simplified trm'_pat'.supp]

end