theory Ex1rec
imports "../NewParser"
begin

declare [[STEPS = 9]]

atom_decl name

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 alpha_lam_raw_alpha_bp_raw_alpha_bi_raw.intros

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)]



end