theory Ex1rec
imports "../NewParser"
begin

atom_decl name

ML {* val _ = cheat_supp_eq := true *}

nominal_datatype lam =
  Var "name"
| App "lam" "lam"
| Lam x::"name" t::"lam"  bind_set x in t
| Let 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 lam_bp.fv
thm lam_bp.eq_iff[no_vars]
thm lam_bp.bn
thm lam_bp.perm
thm lam_bp.induct
thm lam_bp.inducts
thm lam_bp.distinct
thm lam_bp.supp
ML {* Sign.of_sort @{theory} (@{typ lam}, @{sort fs}) *}
thm lam_bp.fv[simplified lam_bp.supp(1-2)]

(*declare permute_lam_raw_permute_bp_raw.simps[eqvt]
declare alpha_gen_eqvt[eqvt]
equivariance alpha_lam_raw
*)

end