theory ExLeroy
imports "Parser"
begin

(* example form Leroy 96 about modules; OTT *)

atom_decl name

ML {* val _ = recursive := false  *}
nominal_datatype mexp =
  Acc "path"
| Stru "body"
| Funct x::"name" "sexp" m::"mexp"    bind x in m
| FApp "mexp" "path"
| Ascr "mexp" "sexp"
and body =
  Empty
| Seq c::defn d::"body"     bind "cbinders c" in d
and defn =
  Type "name" "tyty"
| Dty "name"
| DStru "name" "mexp"
| Val "name" "trmtrm"
and sexp =
  Sig sbody
| SFunc "name" "sexp" "sexp"
and sbody =
  SEmpty
| SSeq C::spec D::sbody    bind "Cbinders C" in D
and spec =
  Type1 "name"
| Type2 "name" "tyty"
| SStru "name" "sexp"
| SVal "name" "tyty"
and tyty =
  Tyref1 "name"
| Tyref2 "path" "tyty"
| Fun "tyty" "tyty"
and path =
  Sref1 "name"
| Sref2 "path" "name"
and trmtrm =
  Tref1 "name"
| Tref2 "path" "name"
| Lam' v::"name" "tyty" M::"trmtrm"  bind v in M
| App' "trmtrm" "trmtrm"
| Let' "body" "trmtrm"
binder
    cbinders :: "defn \<Rightarrow> atom set"
and Cbinders :: "spec \<Rightarrow> atom set"
where
  "cbinders (Type t T) = {atom t}"
| "cbinders (Dty t) = {atom t}"
| "cbinders (DStru x s) = {atom x}"
| "cbinders (Val v M) = {atom v}"
| "Cbinders (Type1 t) = {atom t}"
| "Cbinders (Type2 t T) = {atom t}"
| "Cbinders (SStru x S) = {atom x}"
| "Cbinders (SVal v T) = {atom v}"

thm mexp_body_defn_sexp_sbody_spec_tyty_path_trmtrm.fv
thm mexp_body_defn_sexp_sbody_spec_tyty_path_trmtrm.eq_iff
thm mexp_body_defn_sexp_sbody_spec_tyty_path_trmtrm.bn
thm mexp_body_defn_sexp_sbody_spec_tyty_path_trmtrm.perm
thm mexp_body_defn_sexp_sbody_spec_tyty_path_trmtrm.induct
thm mexp_body_defn_sexp_sbody_spec_tyty_path_trmtrm.inducts
thm mexp_body_defn_sexp_sbody_spec_tyty_path_trmtrm.distinct
thm mexp_body_defn_sexp_sbody_spec_tyty_path_trmtrm.supp
thm mexp_body_defn_sexp_sbody_spec_tyty_path_trmtrm.fv[simplified mexp_body_defn_sexp_sbody_spec_tyty_path_trmtrm.supp]

end