streamlined definition of alpha-equivalence for single binders (used flip instead of swap)
theory Datatypesimports "../Nominal2" begin(* plain nominal_datatype definition without an atom_decl - example by John Matthews*)nominal_datatype 'a::fs Maybe = Nothing | Just 'athm Maybe.distinctthm Maybe.inductthm Maybe.exhaustthm Maybe.strong_exhaustthm Maybe.fv_defsthm Maybe.bn_defsthm Maybe.perm_simpsthm Maybe.eq_iffthm Maybe.fv_bn_eqvtthm Maybe.size_eqvtthm Maybe.supp(* using a datatype inside a nominal_datatype the datatype needs to be shown to be an instance of the pure class (this is usually trivial)*)atom_decl namedatatype foo = Foo | Barinstantiation foo :: purebegindefinition "p \<bullet> (f::foo) = f"instanceapply(default)apply(simp_all add: permute_foo_def)doneendnominal_datatype baz = Baz x::name t::foo binds x in tthm baz.distinctthm baz.inductthm baz.exhaustthm baz.strong_exhaustthm baz.fv_defsthm baz.bn_defsthm baz.perm_simpsthm baz.eq_iffthm baz.fv_bn_eqvtthm baz.size_eqvtthm baz.supp(* a nominal datatype with a set argument of pure type*)nominal_datatype set_ty = Set_ty "nat set"| Fun "nat \<Rightarrow> nat"| Var "name"| Lam x::"name" t::"set_ty" binds x in tthm meta_eq_to_obj_eqthm set_ty.distinctthm set_ty.inductthm set_ty.exhaustthm set_ty.strong_exhaustthm set_ty.fv_defsthm set_ty.bn_defsthm set_ty.perm_simpsthm set_ty.eq_iffthm set_ty.fv_bn_eqvtthm set_ty.size_eqvtthm set_ty.suppend