theory LetRec
imports "../NewParser"
begin

declare [[STEPS = 14]]

atom_decl name

nominal_datatype let_rec:
 lam =
  Var "name"
| App "lam" "lam"
| Lam x::"name" t::"lam"     bind (set) x in t
| Let_Rec bp::"bp" t::"lam"  bind (set) "bi bp" in bp t
and bp =
  Bp "name" "lam"
binder
  bi::"bp \<Rightarrow> atom set"
where
  "bi (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