equal
deleted
inserted
replaced
5 (* example from Leroy'96 about modules; |
5 (* example from Leroy'96 about modules; |
6 see OTT example by Owens *) |
6 see OTT example by Owens *) |
7 |
7 |
8 atom_decl name |
8 atom_decl name |
9 |
9 |
10 nominal_datatype mexp = |
10 nominal_datatype modules: |
|
11 mexp = |
11 Acc "path" |
12 Acc "path" |
12 | Stru "body" |
13 | Stru "body" |
13 | Funct x::"name" "sexp" m::"mexp" bind_set x in m |
14 | Funct x::"name" "sexp" m::"mexp" bind (set) x in m |
14 | FApp "mexp" "path" |
15 | FApp "mexp" "path" |
15 | Ascr "mexp" "sexp" |
16 | Ascr "mexp" "sexp" |
16 and body = |
17 and body = |
17 Empty |
18 Empty |
18 | Seq c::defn d::"body" bind_set "cbinders c" in d |
19 | Seq c::"defn" d::"body" bind (set) "cbinders c" in d |
19 and defn = |
20 and defn = |
20 Type "name" "ty" |
21 Type "name" "ty" |
21 | Dty "name" |
22 | Dty "name" |
22 | DStru "name" "mexp" |
23 | DStru "name" "mexp" |
23 | Val "name" "trm" |
24 | Val "name" "trm" |
24 and sexp = |
25 and sexp = |
25 Sig sbody |
26 Sig sbody |
26 | SFunc "name" "sexp" "sexp" |
27 | SFunc "name" "sexp" "sexp" |
27 and sbody = |
28 and sbody = |
28 SEmpty |
29 SEmpty |
29 | SSeq C::spec D::sbody bind_set "Cbinders C" in D |
30 | SSeq C::"spec" D::"sbody" bind (set) "Cbinders C" in D |
30 and spec = |
31 and spec = |
31 Type1 "name" |
32 Type1 "name" |
32 | Type2 "name" "ty" |
33 | Type2 "name" "ty" |
33 | SStru "name" "sexp" |
34 | SStru "name" "sexp" |
34 | SVal "name" "ty" |
35 | SVal "name" "ty" |
40 Sref1 "name" |
41 Sref1 "name" |
41 | Sref2 "path" "name" |
42 | Sref2 "path" "name" |
42 and trm = |
43 and trm = |
43 Tref1 "name" |
44 Tref1 "name" |
44 | Tref2 "path" "name" |
45 | Tref2 "path" "name" |
45 | Lam' v::"name" "ty" M::"trm" bind_set v in M |
46 | Lam' v::"name" "ty" M::"trm" bind (set) v in M |
46 | App' "trm" "trm" |
47 | App' "trm" "trm" |
47 | Let' "body" "trm" |
48 | Let' "body" "trm" |
48 binder |
49 binder |
49 cbinders :: "defn \<Rightarrow> atom set" |
50 cbinders :: "defn \<Rightarrow> atom set" |
50 and Cbinders :: "spec \<Rightarrow> atom set" |
51 and Cbinders :: "spec \<Rightarrow> atom set" |
56 | "Cbinders (Type1 t) = {atom t}" |
57 | "Cbinders (Type1 t) = {atom t}" |
57 | "Cbinders (Type2 t T) = {atom t}" |
58 | "Cbinders (Type2 t T) = {atom t}" |
58 | "Cbinders (SStru x S) = {atom x}" |
59 | "Cbinders (SStru x S) = {atom x}" |
59 | "Cbinders (SVal v T) = {atom v}" |
60 | "Cbinders (SVal v T) = {atom v}" |
60 |
61 |
61 thm mexp_body_defn_sexp_sbody_spec_ty_path_trm.fv |
62 |
62 thm mexp_body_defn_sexp_sbody_spec_ty_path_trm.eq_iff |
63 thm modules.distinct |
63 thm mexp_body_defn_sexp_sbody_spec_ty_path_trm.bn |
64 thm modules.induct |
64 thm mexp_body_defn_sexp_sbody_spec_ty_path_trm.perm |
65 thm modules.exhaust |
65 thm mexp_body_defn_sexp_sbody_spec_ty_path_trm.induct |
66 thm modules.fv_defs |
66 thm mexp_body_defn_sexp_sbody_spec_ty_path_trm.inducts |
67 thm modules.bn_defs |
67 thm mexp_body_defn_sexp_sbody_spec_ty_path_trm.distinct |
68 thm modules.perm_simps |
68 thm mexp_body_defn_sexp_sbody_spec_ty_path_trm.supp(1-3,5-7,9-10) |
69 thm modules.eq_iff |
69 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)] |
70 thm modules.fv_bn_eqvt |
|
71 thm modules.size_eqvt |
70 |
72 |
71 |
73 |
72 |
74 |
73 end |
75 end |
74 |
76 |