55 and pat0 = |
56 and pat0 = |
56 PN0 |
57 PN0 |
57 | PS0 "name" |
58 | PS0 "name" |
58 | PD0 "pat0" "pat0" |
59 | PD0 "pat0" "pat0" |
59 binder |
60 binder |
60 f0::"pat0 \<Rightarrow> name set" |
61 f0::"pat0 \<Rightarrow> atom set" |
61 where |
62 where |
62 "f0 PN0 = {}" |
63 "f0 PN0 = {}" |
63 | "f0 (PS0 x) = {x}" |
64 | "f0 (PS0 x) = {atom x}" |
64 | "f0 (PD0 p1 p2) = (f0 p1) \<union> (f0 p2)" |
65 | "f0 (PD0 p1 p2) = (f0 p1) \<union> (f0 p2)" |
65 |
66 |
66 thm f0_raw.simps |
67 thm f0_raw.simps |
67 |
68 |
68 text {* example type schemes *} |
69 text {* example type schemes *} |
69 |
70 |
70 datatype t = |
71 (* does not work yet |
|
72 nominal_datatype t = |
71 Var "name" |
73 Var "name" |
72 | Fun "t" "t" |
74 | Fun "t" "t" |
73 |
75 |
74 nominal_datatype tyS = |
76 nominal_datatype tyS = |
|
77 All xs::"name list" ty::"t_raw" bind xs in ty |
|
78 *) |
|
79 |
|
80 (* also does not work |
|
81 nominal_datatype t = |
|
82 Var "name" |
|
83 | Fun "t" "t" |
|
84 and tyS = |
75 All xs::"name list" ty::"t" bind xs in ty |
85 All xs::"name list" ty::"t" bind xs in ty |
76 |
86 *) |
77 |
|
78 |
87 |
79 (* example 1 from Terms.thy *) |
88 (* example 1 from Terms.thy *) |
80 |
89 |
81 nominal_datatype trm1 = |
90 nominal_datatype trm1 = |
82 Vr1 "name" |
91 Vr1 "name" |
126 "bv3 ANil = {}" |
135 "bv3 ANil = {}" |
127 | "bv3 (ACons x t as) = {atom x} \<union> (bv3 as)" |
136 | "bv3 (ACons x t as) = {atom x} \<union> (bv3 as)" |
128 |
137 |
129 (* example 4 from Terms.thy *) |
138 (* example 4 from Terms.thy *) |
130 |
139 |
|
140 (* does not work yet |
131 nominal_datatype trm4 = |
141 nominal_datatype trm4 = |
132 Vr4 "name" |
142 Vr4 "name" |
133 | Ap4 "trm4" "trm4 list" |
143 | Ap4 "trm4" "trm4 list" |
134 | Lm4 x::"name" t::"trm4" bind x in t |
144 | Lm4 x::"name" t::"trm4" bind x in t |
|
145 *) |
135 |
146 |
136 (* example 5 from Terms.thy *) |
147 (* example 5 from Terms.thy *) |
137 |
148 |
138 nominal_datatype trm5 = |
149 nominal_datatype trm5 = |
139 Vr5 "name" |
150 Vr5 "name" |
275 |
286 |
276 datatype sort = |
287 datatype sort = |
277 TY tvar |
288 TY tvar |
278 | CO co |
289 | CO co |
279 |
290 |
280 datatype kind = |
291 nominal_datatype kind = |
281 KStar |
292 KStar |
282 | KFun kind kind |
293 | KFun kind kind |
283 | KEq kind kind |
294 | KEq kind kind |
284 |
295 |
285 (* there are types, coercion types and regular types *) |
296 (* there are types, coercion types and regular types *) |
|
297 (* |
286 nominal_datatype ty = |
298 nominal_datatype ty = |
287 TVar tvar |
299 TVar tvar |
288 | TFun string "ty list" |
300 | TFun string "ty list" |
289 | TAll tvar kind ty --"some binding" |
301 | TAll tvar kind_raw ty --"some binding" |
290 | TSym ty |
302 | TSym ty |
291 | TCir ty ty |
303 | TCir ty ty |
292 | TApp ty ty |
304 | TApp ty ty |
293 | TLeft ty |
305 | TLeft ty |
294 | TRight ty |
306 | TRight ty |
295 | TEq ty |
307 | TEq ty |
296 | TRightc ty |
308 | TRightc ty |
297 | TLeftc ty |
309 | TLeftc ty |
298 | TCoe ty ty |
310 | TCoe ty ty |
299 |
311 *) |
300 typedecl ty --"hack since ty is not yet defined" |
312 typedecl ty --"hack since ty is not yet defined" |
301 |
313 |
302 abbreviation |
314 abbreviation |
303 "atoms A \<equiv> atom ` A" |
315 "atoms A \<equiv> atom ` A" |
304 |
316 |
|
317 (* does not work yet |
305 nominal_datatype trm = |
318 nominal_datatype trm = |
306 Var var |
319 Var var |
307 | LAM tv::tvar kind t::trm bind tv in t |
320 | LAM tv::tvar kind_raw t::trm bind tv in t |
308 | APP trm ty |
321 | APP trm ty |
309 | Lam v::var ty t::trm bind v in t |
322 | Lam v::var ty t::trm bind v in t |
310 | App trm trm |
323 | App trm trm |
311 | Let x::var ty trm t::trm bind x in t |
324 | Let x::var ty trm t::trm bind x in t |
312 | Case trm "assoc list" |
325 | Case trm "assoc list" |
313 | Cast trm ty --"ty is supposed to be a coercion type only" |
326 | Cast trm ty --"ty is supposed to be a coercion type only" |
314 and assoc = |
327 and assoc = |
315 A p::pat t::trm bind "bv p" in t |
328 A p::pat t::trm bind "bv p" in t |
316 and pat = |
329 and pat = |
317 K string "(tvar \<times> kind) list" "(var \<times> ty) list" |
330 K string "(tvar \<times> kind_raw) list" "(var \<times> ty) list" |
318 binder |
331 binder |
319 bv :: "pat \<Rightarrow> atom set" |
332 bv :: "pat \<Rightarrow> atom set" |
320 where |
333 where |
321 "bv (K s ts vs) = (atoms (set (map fst ts))) \<union> (atoms (set (map fst vs)))" |
334 "bv (K s ts vs) = (atoms (set (map fst ts))) \<union> (atoms (set (map fst vs)))" |
322 |
335 *) |
323 |
336 |
324 thm bv_raw.simps |
337 thm bv_raw.simps |
325 |
338 |
326 end |
339 end |
327 |
340 |