theory Modules

imports "../Nominal2"

begin

(* example from Leroy'96 about modules; 

   see OTT example by Owens *)

atom_decl name

nominal_datatype modules: 

 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 modules.distinct

thm modules.induct

thm modules.exhaust

thm modules.fv_defs

thm modules.bn_defs

thm modules.perm_simps

thm modules.eq_iff

thm modules.fv_bn_eqvt

thm modules.size_eqvt

end