theory LetPat
imports "../Nominal2"
begin

declare [[STEPS = 100]]

atom_decl name

nominal_datatype trm =
  Var "name"
| App "trm" "trm"
| Lam x::"name" t::"trm"       bind (set) x in t
| Let p::"pat" "trm" t::"trm"  bind (set) "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.distinct
thm trm_pat.induct
thm trm_pat.exhaust
thm trm_pat.fv_defs
thm trm_pat.bn_defs
thm trm_pat.perm_simps
thm trm_pat.eq_iff
thm trm_pat.fv_bn_eqvt
thm trm_pat.size_eqvt


end