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