theory Modules
imports "../NewParser"
begin

(* example from Leroy'96 about modules; 
   see OTT example by Owens *)

atom_decl name

nominal_datatype mexp =
  Acc "path"
| Stru "body"
| Funct x::"name" "sexp" m::"mexp"    bind_set x in m
| FApp "mexp" "path"
| Ascr "mexp" "sexp"
and body =
  Empty
| Seq c::defn d::"body"     bind_set "cbinders c" in d
and defn =
  Type "name" "ty"
| Dty "name"
| DStru "name" "mexp"
| Val "name" "trm"
and sexp =
  Sig sbody
| SFunc "name" "sexp" "sexp"
and sbody =
  SEmpty
| SSeq C::spec D::sbody    bind_set "Cbinders C" in D
and spec =
  Type1 "name"
| Type2 "name" "ty"
| SStru "name" "sexp"
| SVal "name" "ty"
and ty =
  Tyref1 "name"
| Tyref2 "path" "ty"
| Fun "ty" "ty"
and path =
  Sref1 "name"
| Sref2 "path" "name"
and trm =
  Tref1 "name"
| Tref2 "path" "name"
| Lam' v::"name" "ty" M::"trm"  bind_set v in M
| App' "trm" "trm"
| Let' "body" "trm"
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_ty_path_trm.fv
thm mexp_body_defn_sexp_sbody_spec_ty_path_trm.eq_iff
thm mexp_body_defn_sexp_sbody_spec_ty_path_trm.bn
thm mexp_body_defn_sexp_sbody_spec_ty_path_trm.perm
thm mexp_body_defn_sexp_sbody_spec_ty_path_trm.induct
thm mexp_body_defn_sexp_sbody_spec_ty_path_trm.inducts
thm mexp_body_defn_sexp_sbody_spec_ty_path_trm.distinct
thm mexp_body_defn_sexp_sbody_spec_ty_path_trm.supp(1-3,5-7,9-10)
thm mexp_body_defn_sexp_sbody_spec_ty_path_trm.fv[simplified mexp_body_defn_sexp_sbody_spec_ty_path_trm.supp(1-3,5-7,9-10)]



end