14 | Ascr "mexp" "sexp" |
14 | Ascr "mexp" "sexp" |
15 and body = |
15 and body = |
16 Empty |
16 Empty |
17 | Seq c::defn d::"body" bind_set "cbinders c" in d |
17 | Seq c::defn d::"body" bind_set "cbinders c" in d |
18 and defn = |
18 and defn = |
19 Type "name" "tyty" |
19 Type "name" "ty" |
20 | Dty "name" |
20 | Dty "name" |
21 | DStru "name" "mexp" |
21 | DStru "name" "mexp" |
22 | Val "name" "trmtrm" |
22 | Val "name" "trm" |
23 and sexp = |
23 and sexp = |
24 Sig sbody |
24 Sig sbody |
25 | SFunc "name" "sexp" "sexp" |
25 | SFunc "name" "sexp" "sexp" |
26 and sbody = |
26 and sbody = |
27 SEmpty |
27 SEmpty |
28 | SSeq C::spec D::sbody bind_set "Cbinders C" in D |
28 | SSeq C::spec D::sbody bind_set "Cbinders C" in D |
29 and spec = |
29 and spec = |
30 Type1 "name" |
30 Type1 "name" |
31 | Type2 "name" "tyty" |
31 | Type2 "name" "ty" |
32 | SStru "name" "sexp" |
32 | SStru "name" "sexp" |
33 | SVal "name" "tyty" |
33 | SVal "name" "ty" |
34 and tyty = |
34 and ty = |
35 Tyref1 "name" |
35 Tyref1 "name" |
36 | Tyref2 "path" "tyty" |
36 | Tyref2 "path" "ty" |
37 | Fun "tyty" "tyty" |
37 | Fun "ty" "ty" |
38 and path = |
38 and path = |
39 Sref1 "name" |
39 Sref1 "name" |
40 | Sref2 "path" "name" |
40 | Sref2 "path" "name" |
41 and trmtrm = |
41 and trm = |
42 Tref1 "name" |
42 Tref1 "name" |
43 | Tref2 "path" "name" |
43 | Tref2 "path" "name" |
44 | Lam' v::"name" "tyty" M::"trmtrm" bind_set v in M |
44 | Lam' v::"name" "ty" M::"trm" bind_set v in M |
45 | App' "trmtrm" "trmtrm" |
45 | App' "trm" "trm" |
46 | Let' "body" "trmtrm" |
46 | Let' "body" "trm" |
47 binder |
47 binder |
48 cbinders :: "defn \<Rightarrow> atom set" |
48 cbinders :: "defn \<Rightarrow> atom set" |
49 and Cbinders :: "spec \<Rightarrow> atom set" |
49 and Cbinders :: "spec \<Rightarrow> atom set" |
50 where |
50 where |
51 "cbinders (Type t T) = {atom t}" |
51 "cbinders (Type t T) = {atom t}" |
55 | "Cbinders (Type1 t) = {atom t}" |
55 | "Cbinders (Type1 t) = {atom t}" |
56 | "Cbinders (Type2 t T) = {atom t}" |
56 | "Cbinders (Type2 t T) = {atom t}" |
57 | "Cbinders (SStru x S) = {atom x}" |
57 | "Cbinders (SStru x S) = {atom x}" |
58 | "Cbinders (SVal v T) = {atom v}" |
58 | "Cbinders (SVal v T) = {atom v}" |
59 |
59 |
60 thm mexp_body_defn_sexp_sbody_spec_tyty_path_trmtrm.fv |
60 thm mexp_body_defn_sexp_sbody_spec_ty_path_trm.fv |
61 thm mexp_body_defn_sexp_sbody_spec_tyty_path_trmtrm.eq_iff |
61 thm mexp_body_defn_sexp_sbody_spec_ty_path_trm.eq_iff |
62 thm mexp_body_defn_sexp_sbody_spec_tyty_path_trmtrm.bn |
62 thm mexp_body_defn_sexp_sbody_spec_ty_path_trm.bn |
63 thm mexp_body_defn_sexp_sbody_spec_tyty_path_trmtrm.perm |
63 thm mexp_body_defn_sexp_sbody_spec_ty_path_trm.perm |
64 thm mexp_body_defn_sexp_sbody_spec_tyty_path_trmtrm.induct |
64 thm mexp_body_defn_sexp_sbody_spec_ty_path_trm.induct |
65 thm mexp_body_defn_sexp_sbody_spec_tyty_path_trmtrm.inducts |
65 thm mexp_body_defn_sexp_sbody_spec_ty_path_trm.inducts |
66 thm mexp_body_defn_sexp_sbody_spec_tyty_path_trmtrm.distinct |
66 thm mexp_body_defn_sexp_sbody_spec_ty_path_trm.distinct |
67 thm mexp_body_defn_sexp_sbody_spec_tyty_path_trmtrm.supp(1-3,5-7,9-10) |
67 thm mexp_body_defn_sexp_sbody_spec_ty_path_trm.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)] |
68 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)] |
|
69 |
|
70 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] |
|
71 declare alpha_gen_eqvt[eqvt] |
|
72 |
|
73 equivariance alpha_trm_raw |
|
74 |
69 |
75 |
70 end |
76 end |
71 |
77 |
72 |
78 |
73 |
79 |