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