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