theory LF
imports "../Nominal2"
begin
atom_decl name
atom_decl ident
nominal_datatype lf:
kind =
Type
| KPi "ty" n::"name" k::"kind" bind n in k
and ty =
TConst "ident"
| TApp "ty" "trm"
| TPi "ty" n::"name" ty::"ty" bind n in ty
and trm =
Const "ident"
| Var "name"
| App "trm" "trm"
| Lam "ty" n::"name" t::"trm" bind n in t
thm lf.distinct
thm lf.induct
thm lf.inducts
thm lf.exhaust
thm lf.strong_exhaust
thm lf.fv_defs
thm lf.bn_defs
thm lf.perm_simps
thm lf.eq_iff
thm lf.fv_bn_eqvt
thm lf.size_eqvt
thm lf.supports
thm lf.fsupp
thm lf.supp
thm lf.fresh
thm lf.fresh[simplified]
end