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.perm_bn_alpha+
−
thm modules.perm_bn_simps+
−
thm modules.bn_finite+
−
+
−
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+
−
thm modules.supp+
−
+
−
+
−
end+
−
+
−
+
−
+
−