theory LetRec
imports "../Nominal2"
begin

atom_decl name

nominal_datatype let_rec:
 trm =
  Var "name"
| App "trm" "trm"
| Lam x::"name" t::"trm"     bind (set) x in t
| Let_Rec bp::"bp" t::"trm"  bind (set) "bn bp" in bp t
and bp =
  Bp "name" "trm"
binder
  bn::"bp \<Rightarrow> atom set"
where
  "bn (Bp x t) = {atom x}"

thm let_rec.distinct
thm let_rec.induct
thm let_rec.exhaust
thm let_rec.fv_defs
thm let_rec.bn_defs
thm let_rec.perm_simps
thm let_rec.eq_iff
thm let_rec.fv_bn_eqvt
thm let_rec.size_eqvt


end