equal
deleted
inserted
replaced
1 theory ExLeroy |
1 theory ExLeroy |
2 imports "../Parser" |
2 imports "../NewParser" |
3 begin |
3 begin |
4 |
4 |
5 (* example form Leroy 96 about modules; OTT *) |
5 (* example form Leroy 96 about modules; OTT *) |
6 |
6 |
7 atom_decl name |
7 atom_decl name |
8 |
8 |
9 ML {* val _ = recursive := false *} |
|
10 nominal_datatype mexp = |
9 nominal_datatype mexp = |
11 Acc "path" |
10 Acc "path" |
12 | Stru "body" |
11 | Stru "body" |
13 | Funct x::"name" "sexp" m::"mexp" bind x in m |
12 | Funct x::"name" "sexp" m::"mexp" bind_set x in m |
14 | FApp "mexp" "path" |
13 | FApp "mexp" "path" |
15 | Ascr "mexp" "sexp" |
14 | Ascr "mexp" "sexp" |
16 and body = |
15 and body = |
17 Empty |
16 Empty |
18 | Seq c::defn d::"body" bind "cbinders c" in d |
17 | Seq c::defn d::"body" bind_set "cbinders c" in d |
19 and defn = |
18 and defn = |
20 Type "name" "tyty" |
19 Type "name" "tyty" |
21 | Dty "name" |
20 | Dty "name" |
22 | DStru "name" "mexp" |
21 | DStru "name" "mexp" |
23 | Val "name" "trmtrm" |
22 | Val "name" "trmtrm" |
24 and sexp = |
23 and sexp = |
25 Sig sbody |
24 Sig sbody |
26 | SFunc "name" "sexp" "sexp" |
25 | SFunc "name" "sexp" "sexp" |
27 and sbody = |
26 and sbody = |
28 SEmpty |
27 SEmpty |
29 | SSeq C::spec D::sbody bind "Cbinders C" in D |
28 | SSeq C::spec D::sbody bind_set "Cbinders C" in D |
30 and spec = |
29 and spec = |
31 Type1 "name" |
30 Type1 "name" |
32 | Type2 "name" "tyty" |
31 | Type2 "name" "tyty" |
33 | SStru "name" "sexp" |
32 | SStru "name" "sexp" |
34 | SVal "name" "tyty" |
33 | SVal "name" "tyty" |
40 Sref1 "name" |
39 Sref1 "name" |
41 | Sref2 "path" "name" |
40 | Sref2 "path" "name" |
42 and trmtrm = |
41 and trmtrm = |
43 Tref1 "name" |
42 Tref1 "name" |
44 | Tref2 "path" "name" |
43 | Tref2 "path" "name" |
45 | Lam' v::"name" "tyty" M::"trmtrm" bind v in M |
44 | Lam' v::"name" "tyty" M::"trmtrm" bind_set v in M |
46 | App' "trmtrm" "trmtrm" |
45 | App' "trmtrm" "trmtrm" |
47 | Let' "body" "trmtrm" |
46 | Let' "body" "trmtrm" |
48 binder |
47 binder |
49 cbinders :: "defn \<Rightarrow> atom set" |
48 cbinders :: "defn \<Rightarrow> atom set" |
50 and Cbinders :: "spec \<Rightarrow> atom set" |
49 and Cbinders :: "spec \<Rightarrow> atom set" |
63 thm mexp_body_defn_sexp_sbody_spec_tyty_path_trmtrm.bn |
62 thm mexp_body_defn_sexp_sbody_spec_tyty_path_trmtrm.bn |
64 thm mexp_body_defn_sexp_sbody_spec_tyty_path_trmtrm.perm |
63 thm mexp_body_defn_sexp_sbody_spec_tyty_path_trmtrm.perm |
65 thm mexp_body_defn_sexp_sbody_spec_tyty_path_trmtrm.induct |
64 thm mexp_body_defn_sexp_sbody_spec_tyty_path_trmtrm.induct |
66 thm mexp_body_defn_sexp_sbody_spec_tyty_path_trmtrm.inducts |
65 thm mexp_body_defn_sexp_sbody_spec_tyty_path_trmtrm.inducts |
67 thm mexp_body_defn_sexp_sbody_spec_tyty_path_trmtrm.distinct |
66 thm mexp_body_defn_sexp_sbody_spec_tyty_path_trmtrm.distinct |
68 thm mexp_body_defn_sexp_sbody_spec_tyty_path_trmtrm.supp |
67 thm mexp_body_defn_sexp_sbody_spec_tyty_path_trmtrm.supp(1-3,5-7,9-10) |
69 thm mexp_body_defn_sexp_sbody_spec_tyty_path_trmtrm.fv[simplified mexp_body_defn_sexp_sbody_spec_tyty_path_trmtrm.supp] |
68 thm mexp_body_defn_sexp_sbody_spec_tyty_path_trmtrm.fv[simplified mexp_body_defn_sexp_sbody_spec_tyty_path_trmtrm.supp(1-3,5-7,9-10)] |
70 |
69 |
71 end |
70 end |
72 |
71 |
73 |
72 |
74 |
73 |