--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Nominal/Ex/Modules.thy	Sun May 09 12:38:59 2010 +0100
@@ -0,0 +1,80 @@
+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)]
+
+declare permute_mexp_raw_permute_body_raw_permute_defn_raw_permute_sexp_raw_permute_sbody_raw_permute_spec_raw_permute_ty_raw_permute_path_raw_permute_trm_raw.simps[eqvt]
+declare alpha_gen_eqvt[eqvt]
+
+equivariance alpha_trm_raw
+
+
+end
+
+
+