equal
deleted
inserted
replaced
22 |
22 |
23 print_theorems |
23 print_theorems |
24 |
24 |
25 text {* example 2 *} |
25 text {* example 2 *} |
26 |
26 |
27 nominal_datatype trm = |
27 nominal_datatype trm' = |
28 Var "name" |
28 Var "name" |
29 | App "trm" "trm" |
29 | App "trm'" "trm'" |
30 | Lam x::"name" t::"trm" bind x in t |
30 | Lam x::"name" t::"trm'" bind x in t |
31 | Let p::"pat" "trm" t::"trm" bind "f p" in t |
31 | Let p::"pat'" "trm'" t::"trm'" bind "f p" in t |
32 and pat = |
32 and pat' = |
33 PN |
33 PN |
34 | PS "name" |
34 | PS "name" |
35 | PD "name" "name" |
35 | PD "name" "name" |
36 binder |
36 binder |
37 f::"pat \<Rightarrow> name set" |
37 f::"pat' \<Rightarrow> name set" |
38 where |
38 where |
39 "f PN = {}" |
39 "f PN = {}" |
40 | "f (PS x) = {x}" |
40 | "f (PS x) = {x}" |
41 | "f (PD x y) = {x,y}" |
41 | "f (PD x y) = {x,y}" |
42 |
42 |
59 | "f0 (PD0 p1 p2) = (f0 p1) \<union> (f0 p2)" |
59 | "f0 (PD0 p1 p2) = (f0 p1) \<union> (f0 p2)" |
60 |
60 |
61 thm f0_raw.simps |
61 thm f0_raw.simps |
62 |
62 |
63 text {* example type schemes *} |
63 text {* example type schemes *} |
64 datatype ty = |
64 datatype t = |
65 Var "name" |
65 Var "name" |
66 | Fun "ty" "ty" |
66 | Fun "t" "t" |
67 |
67 |
68 nominal_datatype tyS = |
68 nominal_datatype tyS = |
69 All xs::"name list" ty::"ty" bind xs in ty |
69 All xs::"name list" ty::"t" bind xs in ty |
70 |
70 |
71 |
71 |
72 |
72 |
73 (* example 1 from Terms.thy *) |
73 (* example 1 from Terms.thy *) |
74 |
74 |
193 bv9 |
193 bv9 |
194 where |
194 where |
195 "bv9 (Var9 x) = {}" |
195 "bv9 (Var9 x) = {}" |
196 | "bv9 (Lam9 x b) = {atom x}" |
196 | "bv9 (Lam9 x b) = {atom x}" |
197 |
197 |
|
198 |
|
199 (* core haskell *) |
|
200 |
|
201 atom_decl var |
|
202 atom_decl tvar |
|
203 atom_decl co |
|
204 |
|
205 datatype sort = |
|
206 TY tvar |
|
207 | CO co |
|
208 |
|
209 datatype kind = |
|
210 KStar |
|
211 | KFun kind kind |
|
212 | KEq kind kind |
|
213 |
|
214 (* there are types, coercion types and regular types *) |
|
215 nominal_datatype ty = |
|
216 TVar tvar |
|
217 | TFun string "ty list" |
|
218 | TAll tvar kind ty --"some binding" |
|
219 | TSym ty |
|
220 | TCir ty ty |
|
221 | TApp ty ty |
|
222 | TLeft ty |
|
223 | TRight ty |
|
224 | TEq ty |
|
225 | TRightc ty |
|
226 | TLeftc ty |
|
227 | TCoe ty ty |
|
228 |
|
229 typedecl ty --"hack since ty is not yet defined" |
|
230 |
|
231 abbreviation |
|
232 "atoms A \<equiv> atom ` A" |
|
233 |
|
234 nominal_datatype trm = |
|
235 Var var |
|
236 | LAM tv::tvar kind t::trm bind v in t |
|
237 | APP trm ty |
|
238 | Lam v::var ty t::trm bind v in t |
|
239 | App trm trm |
|
240 | Let x::var ty trm t::trm bind x in t |
|
241 | Case trm "assoc list" |
|
242 | Cast trm ty --"ty is supposed to be a coercion type only" |
|
243 and assoc = |
|
244 A p::pat t::trm bind "bv p" in t |
|
245 and pat = |
|
246 K string "(tvar \<times> kind) list" "(var \<times> ty) list" |
|
247 binder |
|
248 bv :: "pat \<Rightarrow> atom set" |
|
249 where |
|
250 "bv (K s ts vs) = (atoms (set (map fst ts))) \<union> (atoms (set (map fst vs)))" |
|
251 |
|
252 |
|
253 thm bv_raw.simps |
|
254 |
198 end |
255 end |
199 |
256 |
200 |
257 |
201 |
258 |