50 thm trm5_lts.bn |
50 thm trm5_lts.bn |
51 thm trm5_lts.perm |
51 thm trm5_lts.perm |
52 thm trm5_lts.induct |
52 thm trm5_lts.induct |
53 thm trm5_lts.distinct |
53 thm trm5_lts.distinct |
54 thm trm5_lts.fv[simplified trm5_lts.supp] |
54 thm trm5_lts.fv[simplified trm5_lts.supp] |
55 |
|
56 (* example form Leroy 96 about modules; OTT *) |
|
57 |
|
58 nominal_datatype mexp = |
|
59 Acc "path" |
|
60 | Stru "body" |
|
61 | Funct x::"name" "sexp" m::"mexp" bind x in m |
|
62 | FApp "mexp" "path" |
|
63 | Ascr "mexp" "sexp" |
|
64 and body = |
|
65 Empty |
|
66 | Seq c::defn d::"body" bind "cbinders c" in d |
|
67 and defn = |
|
68 Type "name" "tyty" |
|
69 | Dty "name" |
|
70 | DStru "name" "mexp" |
|
71 | Val "name" "trmtrm" |
|
72 and sexp = |
|
73 Sig sbody |
|
74 | SFunc "name" "sexp" "sexp" |
|
75 and sbody = |
|
76 SEmpty |
|
77 | SSeq C::spec D::sbody bind "Cbinders C" in D |
|
78 and spec = |
|
79 Type1 "name" |
|
80 | Type2 "name" "tyty" |
|
81 | SStru "name" "sexp" |
|
82 | SVal "name" "tyty" |
|
83 and tyty = |
|
84 Tyref1 "name" |
|
85 | Tyref2 "path" "tyty" |
|
86 | Fun "tyty" "tyty" |
|
87 and path = |
|
88 Sref1 "name" |
|
89 | Sref2 "path" "name" |
|
90 and trmtrm = |
|
91 Tref1 "name" |
|
92 | Tref2 "path" "name" |
|
93 | Lam' v::"name" "tyty" M::"trmtrm" bind v in M |
|
94 | App' "trmtrm" "trmtrm" |
|
95 | Let' "body" "trmtrm" |
|
96 binder |
|
97 cbinders :: "defn \<Rightarrow> atom set" |
|
98 and Cbinders :: "spec \<Rightarrow> atom set" |
|
99 where |
|
100 "cbinders (Type t T) = {atom t}" |
|
101 | "cbinders (Dty t) = {atom t}" |
|
102 | "cbinders (DStru x s) = {atom x}" |
|
103 | "cbinders (Val v M) = {atom v}" |
|
104 | "Cbinders (Type1 t) = {atom t}" |
|
105 | "Cbinders (Type2 t T) = {atom t}" |
|
106 | "Cbinders (SStru x S) = {atom x}" |
|
107 | "Cbinders (SVal v T) = {atom v}" |
|
108 |
|
109 thm mexp_body_defn_sexp_sbody_spec_tyty_path_trmtrm.fv |
|
110 thm mexp_body_defn_sexp_sbody_spec_tyty_path_trmtrm.eq_iff |
|
111 thm mexp_body_defn_sexp_sbody_spec_tyty_path_trmtrm.bn |
|
112 thm mexp_body_defn_sexp_sbody_spec_tyty_path_trmtrm.perm |
|
113 thm mexp_body_defn_sexp_sbody_spec_tyty_path_trmtrm.induct |
|
114 thm mexp_body_defn_sexp_sbody_spec_tyty_path_trmtrm.inducts |
|
115 thm mexp_body_defn_sexp_sbody_spec_tyty_path_trmtrm.distinct |
|
116 thm mexp_body_defn_sexp_sbody_spec_tyty_path_trmtrm.supp |
|
117 thm mexp_body_defn_sexp_sbody_spec_tyty_path_trmtrm.fv[simplified mexp_body_defn_sexp_sbody_spec_tyty_path_trmtrm.supp] |
|
118 |
55 |
119 (* example 3 from Peter Sewell's bestiary *) |
56 (* example 3 from Peter Sewell's bestiary *) |
120 |
57 |
121 nominal_datatype exp = |
58 nominal_datatype exp = |
122 VarP "name" |
59 VarP "name" |