|
1 theory Modules |
|
2 imports "../NewParser" |
|
3 begin |
|
4 |
|
5 (* example from Leroy'96 about modules; |
|
6 see OTT example by Owens *) |
|
7 |
|
8 atom_decl name |
|
9 |
|
10 nominal_datatype mexp = |
|
11 Acc "path" |
|
12 | Stru "body" |
|
13 | Funct x::"name" "sexp" m::"mexp" bind_set x in m |
|
14 | FApp "mexp" "path" |
|
15 | Ascr "mexp" "sexp" |
|
16 and body = |
|
17 Empty |
|
18 | Seq c::defn d::"body" bind_set "cbinders c" in d |
|
19 and defn = |
|
20 Type "name" "ty" |
|
21 | Dty "name" |
|
22 | DStru "name" "mexp" |
|
23 | Val "name" "trm" |
|
24 and sexp = |
|
25 Sig sbody |
|
26 | SFunc "name" "sexp" "sexp" |
|
27 and sbody = |
|
28 SEmpty |
|
29 | SSeq C::spec D::sbody bind_set "Cbinders C" in D |
|
30 and spec = |
|
31 Type1 "name" |
|
32 | Type2 "name" "ty" |
|
33 | SStru "name" "sexp" |
|
34 | SVal "name" "ty" |
|
35 and ty = |
|
36 Tyref1 "name" |
|
37 | Tyref2 "path" "ty" |
|
38 | Fun "ty" "ty" |
|
39 and path = |
|
40 Sref1 "name" |
|
41 | Sref2 "path" "name" |
|
42 and trm = |
|
43 Tref1 "name" |
|
44 | Tref2 "path" "name" |
|
45 | Lam' v::"name" "ty" M::"trm" bind_set v in M |
|
46 | App' "trm" "trm" |
|
47 | Let' "body" "trm" |
|
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_ty_path_trm.fv |
|
62 thm mexp_body_defn_sexp_sbody_spec_ty_path_trm.eq_iff |
|
63 thm mexp_body_defn_sexp_sbody_spec_ty_path_trm.bn |
|
64 thm mexp_body_defn_sexp_sbody_spec_ty_path_trm.perm |
|
65 thm mexp_body_defn_sexp_sbody_spec_ty_path_trm.induct |
|
66 thm mexp_body_defn_sexp_sbody_spec_ty_path_trm.inducts |
|
67 thm mexp_body_defn_sexp_sbody_spec_ty_path_trm.distinct |
|
68 thm mexp_body_defn_sexp_sbody_spec_ty_path_trm.supp(1-3,5-7,9-10) |
|
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 |
|
71 declare permute_mexp_raw_permute_body_raw_permute_defn_raw_permute_sexp_raw_permute_sbody_raw_permute_spec_raw_permute_ty_raw_permute_path_raw_permute_trm_raw.simps[eqvt] |
|
72 declare alpha_gen_eqvt[eqvt] |
|
73 |
|
74 equivariance alpha_trm_raw |
|
75 |
|
76 |
|
77 end |
|
78 |
|
79 |
|
80 |