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