|
1 theory Test_compat |
|
2 imports "Parser" "../Attic/Prove" |
|
3 begin |
|
4 |
|
5 text {* |
|
6 example 1 |
|
7 |
|
8 single let binding |
|
9 *} |
|
10 |
|
11 nominal_datatype lam = |
|
12 VAR "name" |
|
13 | APP "lam" "lam" |
|
14 | LET bp::"bp" t::"lam" bind "bi bp" in t |
|
15 and bp = |
|
16 BP "name" "lam" |
|
17 binder |
|
18 bi::"bp \<Rightarrow> atom set" |
|
19 where |
|
20 "bi (BP x t) = {atom x}" |
|
21 |
|
22 thm alpha_lam_raw_alpha_bp_raw.intros[no_vars] |
|
23 |
|
24 abbreviation "VAR \<equiv> VAR_raw" |
|
25 abbreviation "APP \<equiv> APP_raw" |
|
26 abbreviation "LET \<equiv> LET_raw" |
|
27 abbreviation "BP \<equiv> BP_raw" |
|
28 abbreviation "bi \<equiv> bi_raw" |
|
29 |
|
30 (* non-recursive case *) |
|
31 |
|
32 inductive |
|
33 alpha_lam :: "lam_raw \<Rightarrow> lam_raw \<Rightarrow> bool" and |
|
34 alpha_bp :: "bp_raw \<Rightarrow> bp_raw \<Rightarrow> bool" and |
|
35 compat_bp :: "bp_raw \<Rightarrow> perm \<Rightarrow> bp_raw \<Rightarrow> bool" |
|
36 where |
|
37 "x = y \<Longrightarrow> alpha_lam (VAR x) (VAR y)" |
|
38 | "alpha_lam l1 s1 \<and> alpha_lam l2 s2 \<Longrightarrow> alpha_lam (APP l1 l2) (APP s1 s2)" |
|
39 | "\<exists>pi. (bi bp, lam) \<approx>gen alpha_lam fv_lam_raw pi (bi bp', lam') \<and> (pi \<bullet> (bi bp)) = bi bp' |
|
40 \<and> compat_bp bp pi bp' |
|
41 \<Longrightarrow> alpha_lam (LET bp lam) (LET bp' lam')" |
|
42 | "alpha_lam lam lam' \<and> name = name' \<Longrightarrow> alpha_bp (BP name lam) (BP name' lam')" |
|
43 | "alpha_lam t t' \<Longrightarrow> compat_bp (BP x t) pi (BP x' t')" |
|
44 |
|
45 lemma test1: |
|
46 assumes "distinct [x, y]" |
|
47 shows "alpha_lam (LET (BP x (VAR x)) (VAR x)) |
|
48 (LET (BP y (VAR x)) (VAR y))" |
|
49 apply(rule alpha_lam_alpha_bp_compat_bp.intros) |
|
50 apply(rule_tac x="(x \<leftrightarrow> y)" in exI) |
|
51 apply(simp add: alpha_gen fresh_star_def) |
|
52 apply(simp add: alpha_lam_alpha_bp_compat_bp.intros(1)) |
|
53 apply(rule conjI) |
|
54 defer |
|
55 apply(rule alpha_lam_alpha_bp_compat_bp.intros) |
|
56 apply(simp add: alpha_lam_alpha_bp_compat_bp.intros(1)) |
|
57 apply(simp add: permute_set_eq atom_eqvt) |
|
58 done |
|
59 |
|
60 lemma test2: |
|
61 assumes asm: "distinct [x, y]" |
|
62 shows "\<not> alpha_lam (LET (BP x (VAR x)) (VAR x)) |
|
63 (LET (BP y (VAR y)) (VAR y))" |
|
64 using asm |
|
65 apply(clarify) |
|
66 apply(erule alpha_lam.cases) |
|
67 apply(simp_all) |
|
68 apply(erule exE) |
|
69 apply(clarify) |
|
70 apply(simp add: alpha_gen fresh_star_def) |
|
71 apply(erule alpha_lam.cases) |
|
72 apply(simp_all) |
|
73 apply(clarify) |
|
74 apply(erule compat_bp.cases) |
|
75 apply(simp_all) |
|
76 apply(clarify) |
|
77 apply(erule alpha_lam.cases) |
|
78 apply(simp_all) |
|
79 done |
|
80 |
|
81 (* recursive case where we have also bind "bi bp" in bp *) |
|
82 |
|
83 inductive |
|
84 Alpha_lam :: "lam_raw \<Rightarrow> lam_raw \<Rightarrow> bool" and |
|
85 Alpha_bp :: "bp_raw \<Rightarrow> bp_raw \<Rightarrow> bool" and |
|
86 Compat_bp :: "bp_raw \<Rightarrow> perm \<Rightarrow> bp_raw \<Rightarrow> bool" |
|
87 where |
|
88 "x = y \<Longrightarrow> Alpha_lam (VAR x) (VAR y)" |
|
89 | "Alpha_lam l1 s1 \<and> Alpha_lam l2 s2 \<Longrightarrow> Alpha_lam (APP l1 l2) (APP s1 s2)" |
|
90 | "\<exists>pi. (bi bp, lam) \<approx>gen Alpha_lam fv_lam_raw pi (bi bp', lam') \<and> Compat_bp bp pi bp' |
|
91 \<and> (pi \<bullet> (bi bp)) = bi bp' |
|
92 \<Longrightarrow> Alpha_lam (LET bp lam) (LET bp' lam')" |
|
93 | "Alpha_lam lam lam' \<and> name = name' \<Longrightarrow> Alpha_bp (BP name lam) (BP name' lam')" |
|
94 | "Alpha_lam (pi \<bullet> t) t' \<Longrightarrow> Compat_bp (BP x t) pi (BP x' t')" |
|
95 |
|
96 lemma Test1: |
|
97 assumes "distinct [x, y]" |
|
98 shows "Alpha_lam (LET (BP x (VAR x)) (VAR x)) |
|
99 (LET (BP y (VAR y)) (VAR y))" |
|
100 apply(rule Alpha_lam_Alpha_bp_Compat_bp.intros) |
|
101 apply(rule_tac x="(x \<leftrightarrow> y)" in exI) |
|
102 apply(simp add: alpha_gen fresh_star_def) |
|
103 apply(simp add: Alpha_lam_Alpha_bp_Compat_bp.intros(1)) |
|
104 apply(rule conjI) |
|
105 apply(rule Alpha_lam_Alpha_bp_Compat_bp.intros) |
|
106 apply(simp add: Alpha_lam_Alpha_bp_Compat_bp.intros(1)) |
|
107 apply(simp add: permute_set_eq atom_eqvt) |
|
108 done |
|
109 |
|
110 lemma Test2: |
|
111 assumes asm: "distinct [x, y]" |
|
112 shows "\<not> Alpha_lam (LET (BP x (VAR x)) (VAR x)) |
|
113 (LET (BP y (VAR x)) (VAR y))" |
|
114 using asm |
|
115 apply(clarify) |
|
116 apply(erule Alpha_lam.cases) |
|
117 apply(simp_all) |
|
118 apply(erule exE) |
|
119 apply(clarify) |
|
120 apply(simp add: alpha_gen fresh_star_def) |
|
121 apply(erule Alpha_lam.cases) |
|
122 apply(simp_all) |
|
123 apply(clarify) |
|
124 apply(erule Compat_bp.cases) |
|
125 apply(simp_all) |
|
126 apply(clarify) |
|
127 apply(erule Alpha_lam.cases) |
|
128 apply(simp_all) |
|
129 done |
|
130 |
|
131 |
|
132 text {* example 2 *} |
|
133 |
|
134 nominal_datatype trm' = |
|
135 Var "name" |
|
136 | App "trm'" "trm'" |
|
137 | Lam x::"name" t::"trm'" bind x in t |
|
138 | Let p::"pat'" "trm'" t::"trm'" bind "f p" in t |
|
139 and pat' = |
|
140 PN |
|
141 | PS "name" |
|
142 | PD "name" "name" |
|
143 binder |
|
144 f::"pat' \<Rightarrow> atom set" |
|
145 where |
|
146 "f PN = {}" |
|
147 | "f (PS x) = {atom x}" |
|
148 | "f (PD x y) = {atom x} \<union> {atom y}" |
|
149 |
|
150 thm alpha_trm'_raw_alpha_pat'_raw.intros[no_vars] |
|
151 |
|
152 abbreviation "Var \<equiv> Var_raw" |
|
153 abbreviation "App \<equiv> App_raw" |
|
154 abbreviation "Lam \<equiv> Lam_raw" |
|
155 abbreviation "Lett \<equiv> Let_raw" |
|
156 abbreviation "PN \<equiv> PN_raw" |
|
157 abbreviation "PS \<equiv> PS_raw" |
|
158 abbreviation "PD \<equiv> PD_raw" |
|
159 abbreviation "f \<equiv> f_raw" |
|
160 |
|
161 (* not_yet_done *) |
|
162 inductive |
|
163 alpha_trm' :: "trm'_raw \<Rightarrow> trm'_raw \<Rightarrow> bool" and |
|
164 alpha_pat' :: "pat'_raw \<Rightarrow> pat'_raw \<Rightarrow> bool" and |
|
165 compat_pat' :: "pat'_raw \<Rightarrow> perm \<Rightarrow> pat'_raw \<Rightarrow> bool" |
|
166 where |
|
167 "name = name' \<Longrightarrow> alpha_trm' (Var name) (Var name')" |
|
168 | "alpha_trm' t2 t2' \<and> alpha_trm' t1 t1' \<Longrightarrow> alpha_trm' (App t1 t2) (App t1' t2')" |
|
169 | "\<exists>pi. ({atom x}, t) \<approx>gen alpha_trm' fv_trm'_raw pi ({atom x'}, t') \<Longrightarrow> alpha_trm' (Lam x t) (Lam x' t')" |
|
170 | "\<exists>pi. (f p, t) \<approx>gen alpha_trm' fv_trm'_raw pi (f p', t') \<and> alpha_trm' s s' \<and> (pi \<bullet> f p) = f p' \<and> |
|
171 compat_pat' p pi p' \<Longrightarrow> alpha_trm' (Lett p s t) (Lett p' s' t')" |
|
172 | "alpha_pat' PN PN" |
|
173 | "name = name' \<Longrightarrow> alpha_pat' (PS name) (PS name')" |
|
174 | "name2 = name2' \<and> name1 = name1' \<Longrightarrow> alpha_pat' (PD name1 name2) (PD name1' name2')" |
|
175 | "compat_pat' PN pi PN" |
|
176 | "compat_pat' (PS x) pi (PS x')" |
|
177 | "compat_pat' (PD p1 p2) pi (PD p1' p2')" |
|
178 |
|
179 lemma |
|
180 assumes a: "distinct [x, y, z, u]" |
|
181 shows "alpha_trm' (Lett (PD x u) t (App (Var x) (Var y))) |
|
182 (Lett (PD z u) t (App (Var z) (Var y)))" |
|
183 using a |
|
184 apply - |
|
185 apply(rule alpha_trm'_alpha_pat'_compat_pat'.intros) |
|
186 apply(auto simp add: alpha_gen) |
|
187 apply(rule_tac x="(x \<leftrightarrow> z)" in exI) |
|
188 apply(auto simp add: fresh_star_def permute_set_eq atom_eqvt) |
|
189 defer |
|
190 apply(rule alpha_trm'_alpha_pat'_compat_pat'.intros) |
|
191 apply(simp add: alpha_trm'_alpha_pat'_compat_pat'.intros) |
|
192 prefer 4 |
|
193 apply(rule alpha_trm'_alpha_pat'_compat_pat'.intros) |
|
194 (* they can be proved *) |
|
195 oops |
|
196 |
|
197 lemma |
|
198 assumes a: "distinct [x, y, z, u]" |
|
199 shows "alpha_trm' (Lett (PD x u) t (App (Var x) (Var y))) |
|
200 (Lett (PD z z) t (App (Var z) (Var y)))" |
|
201 using a |
|
202 apply - |
|
203 apply(rule alpha_trm'_alpha_pat'_compat_pat'.intros) |
|
204 apply(auto simp add: alpha_gen) |
|
205 apply(rule_tac x="(x \<leftrightarrow> z)" in exI) |
|
206 apply(auto simp add: fresh_star_def permute_set_eq atom_eqvt) |
|
207 defer |
|
208 apply(rule alpha_trm'_alpha_pat'_compat_pat'.intros) |
|
209 apply(simp add: alpha_trm'_alpha_pat'_compat_pat'.intros) |
|
210 prefer 4 |
|
211 apply(rule alpha_trm'_alpha_pat'_compat_pat'.intros) |
|
212 (* they can be proved *) |
|
213 oops |
|
214 |
|
215 using a |
|
216 apply(clarify) |
|
217 apply(erule alpha_trm'.cases) |
|
218 apply(simp_all) |
|
219 apply(auto simp add: alpha_gen) |
|
220 apply(erule alpha_trm'.cases) |
|
221 apply(simp_all) |
|
222 apply(clarify) |
|
223 apply(erule compat_pat'.cases) |
|
224 apply(simp_all) |
|
225 apply(clarify) |
|
226 apply(erule alpha_trm'.cases) |
|
227 apply(simp_all) |
|
228 done |
|
229 |
|
230 nominal_datatype trm0 = |
|
231 Var0 "name" |
|
232 | App0 "trm0" "trm0" |
|
233 | Lam0 x::"name" t::"trm0" bind x in t |
|
234 | Let0 p::"pat0" "trm0" t::"trm0" bind "f0 p" in t |
|
235 and pat0 = |
|
236 PN0 |
|
237 | PS0 "name" |
|
238 | PD0 "pat0" "pat0" |
|
239 binder |
|
240 f0::"pat0 \<Rightarrow> atom set" |
|
241 where |
|
242 "f0 PN0 = {}" |
|
243 | "f0 (PS0 x) = {atom x}" |
|
244 | "f0 (PD0 p1 p2) = (f0 p1) \<union> (f0 p2)" |
|
245 |
|
246 thm f0_raw.simps |
|
247 (*thm trm0_pat0_induct |
|
248 thm trm0_pat0_perm |
|
249 thm trm0_pat0_fv |
|
250 thm trm0_pat0_bn*) |
|
251 |
|
252 text {* example type schemes *} |
|
253 |
|
254 (* does not work yet |
|
255 nominal_datatype t = |
|
256 Var "name" |
|
257 | Fun "t" "t" |
|
258 |
|
259 nominal_datatype tyS = |
|
260 All xs::"name list" ty::"t_raw" bind xs in ty |
|
261 *) |
|
262 |
|
263 |
|
264 nominal_datatype t = |
|
265 Var "name" |
|
266 | Fun "t" "t" |
|
267 and tyS = |
|
268 All xs::"name set" ty::"t" bind xs in ty |
|
269 |
|
270 (* example 1 from Terms.thy *) |
|
271 |
|
272 nominal_datatype trm1 = |
|
273 Vr1 "name" |
|
274 | Ap1 "trm1" "trm1" |
|
275 | Lm1 x::"name" t::"trm1" bind x in t |
|
276 | Lt1 p::"bp1" "trm1" t::"trm1" bind "bv1 p" in t |
|
277 and bp1 = |
|
278 BUnit1 |
|
279 | BV1 "name" |
|
280 | BP1 "bp1" "bp1" |
|
281 binder |
|
282 bv1 |
|
283 where |
|
284 "bv1 (BUnit1) = {}" |
|
285 | "bv1 (BV1 x) = {atom x}" |
|
286 | "bv1 (BP1 bp1 bp2) = (bv1 bp1) \<union> (bv1 bp2)" |
|
287 |
|
288 thm bv1_raw.simps |
|
289 |
|
290 (* example 2 from Terms.thy *) |
|
291 |
|
292 nominal_datatype trm2 = |
|
293 Vr2 "name" |
|
294 | Ap2 "trm2" "trm2" |
|
295 | Lm2 x::"name" t::"trm2" bind x in t |
|
296 | Lt2 r::"assign" t::"trm2" bind "bv2 r" in t |
|
297 and assign = |
|
298 As "name" "trm2" |
|
299 binder |
|
300 bv2 |
|
301 where |
|
302 "bv2 (As x t) = {atom x}" |
|
303 |
|
304 (* compat should be |
|
305 compat (As x t) pi (As x' t') == pi o x = x' & alpha t t' |
|
306 *) |
|
307 |
|
308 |
|
309 thm fv_trm2_raw_fv_assign_raw.simps[no_vars] |
|
310 thm alpha_trm2_raw_alpha_assign_raw.intros[no_vars] |
|
311 |
|
312 |
|
313 |
|
314 text {* example 3 from Terms.thy *} |
|
315 |
|
316 nominal_datatype trm3 = |
|
317 Vr3 "name" |
|
318 | Ap3 "trm3" "trm3" |
|
319 | Lm3 x::"name" t::"trm3" bind x in t |
|
320 | Lt3 r::"rassigns3" t::"trm3" bind "bv3 r" in t |
|
321 and rassigns3 = |
|
322 ANil |
|
323 | ACons "name" "trm3" "rassigns3" |
|
324 binder |
|
325 bv3 |
|
326 where |
|
327 "bv3 ANil = {}" |
|
328 | "bv3 (ACons x t as) = {atom x} \<union> (bv3 as)" |
|
329 |
|
330 |
|
331 (* compat should be |
|
332 compat (ANil) pi (PNil) \<equiv> TRue |
|
333 compat (ACons x t ts) pi (ACons x' t' ts') \<equiv> pi o x = x' \<and> alpha t t' \<and> compat ts pi ts' |
|
334 *) |
|
335 |
|
336 (* example 4 from Terms.thy *) |
|
337 |
|
338 (* fv_eqvt does not work, we need to repaire defined permute functions |
|
339 defined fv and defined alpha... *) |
|
340 nominal_datatype trm4 = |
|
341 Vr4 "name" |
|
342 | Ap4 "trm4" "trm4 list" |
|
343 | Lm4 x::"name" t::"trm4" bind x in t |
|
344 |
|
345 thm alpha_trm4_raw_alpha_trm4_raw_list.intros[no_vars] |
|
346 thm fv_trm4_raw_fv_trm4_raw_list.simps[no_vars] |
|
347 |
|
348 (* example 5 from Terms.thy *) |
|
349 |
|
350 nominal_datatype trm5 = |
|
351 Vr5 "name" |
|
352 | Ap5 "trm5" "trm5" |
|
353 | Lt5 l::"lts" t::"trm5" bind "bv5 l" in t |
|
354 and lts = |
|
355 Lnil |
|
356 | Lcons "name" "trm5" "lts" |
|
357 binder |
|
358 bv5 |
|
359 where |
|
360 "bv5 Lnil = {}" |
|
361 | "bv5 (Lcons n t ltl) = {atom n} \<union> (bv5 ltl)" |
|
362 |
|
363 (* example 6 from Terms.thy *) |
|
364 |
|
365 (* BV is not respectful, needs to fail*) |
|
366 nominal_datatype trm6 = |
|
367 Vr6 "name" |
|
368 | Lm6 x::"name" t::"trm6" bind x in t |
|
369 | Lt6 left::"trm6" right::"trm6" bind "bv6 left" in right |
|
370 binder |
|
371 bv6 |
|
372 where |
|
373 "bv6 (Vr6 n) = {}" |
|
374 | "bv6 (Lm6 n t) = {atom n} \<union> bv6 t" |
|
375 | "bv6 (Lt6 l r) = bv6 l \<union> bv6 r" |
|
376 (* example 7 from Terms.thy *) |
|
377 |
|
378 (* BV is not respectful, needs to fail*) |
|
379 nominal_datatype trm7 = |
|
380 Vr7 "name" |
|
381 | Lm7 l::"name" r::"trm7" bind l in r |
|
382 | Lt7 l::"trm7" r::"trm7" bind "bv7 l" in r |
|
383 binder |
|
384 bv7 |
|
385 where |
|
386 "bv7 (Vr7 n) = {atom n}" |
|
387 | "bv7 (Lm7 n t) = bv7 t - {atom n}" |
|
388 | "bv7 (Lt7 l r) = bv7 l \<union> bv7 r" |
|
389 |
|
390 (* example 8 from Terms.thy *) |
|
391 |
|
392 nominal_datatype foo8 = |
|
393 Foo0 "name" |
|
394 | Foo1 b::"bar8" f::"foo8" bind "bv8 b" in f --"check fo error if this is called foo" |
|
395 and bar8 = |
|
396 Bar0 "name" |
|
397 | Bar1 "name" s::"name" b::"bar8" bind s in b |
|
398 binder |
|
399 bv8 |
|
400 where |
|
401 "bv8 (Bar0 x) = {}" |
|
402 | "bv8 (Bar1 v x b) = {atom v}" |
|
403 |
|
404 (* example 9 from Terms.thy *) |
|
405 |
|
406 (* BV is not respectful, needs to fail*) |
|
407 nominal_datatype lam9 = |
|
408 Var9 "name" |
|
409 | Lam9 n::"name" l::"lam9" bind n in l |
|
410 and bla9 = |
|
411 Bla9 f::"lam9" s::"lam9" bind "bv9 f" in s |
|
412 binder |
|
413 bv9 |
|
414 where |
|
415 "bv9 (Var9 x) = {}" |
|
416 | "bv9 (Lam9 x b) = {atom x}" |
|
417 |
|
418 (* example from my PHD *) |
|
419 |
|
420 atom_decl coname |
|
421 |
|
422 nominal_datatype phd = |
|
423 Ax "name" "coname" |
|
424 | Cut n::"coname" t1::"phd" c::"coname" t2::"phd" bind n in t1, bind c in t2 |
|
425 | AndR c1::"coname" t1::"phd" c2::"coname" t2::"phd" "coname" bind c1 in t1, bind c2 in t2 |
|
426 | AndL1 n::"name" t::"phd" "name" bind n in t |
|
427 | AndL2 n::"name" t::"phd" "name" bind n in t |
|
428 | ImpL c::"coname" t1::"phd" n::"name" t2::"phd" "name" bind c in t1, bind n in t2 |
|
429 | ImpR c::"coname" n::"name" t::"phd" "coname" bind n in t, bind c in t |
|
430 |
|
431 thm alpha_phd_raw.intros[no_vars] |
|
432 thm fv_phd_raw.simps[no_vars] |
|
433 |
|
434 |
|
435 (* example form Leroy 96 about modules; OTT *) |
|
436 |
|
437 nominal_datatype mexp = |
|
438 Acc "path" |
|
439 | Stru "body" |
|
440 | Funct x::"name" "sexp" m::"mexp" bind x in m |
|
441 | FApp "mexp" "path" |
|
442 | Ascr "mexp" "sexp" |
|
443 and body = |
|
444 Empty |
|
445 | Seq c::defn d::"body" bind "cbinders c" in d |
|
446 and defn = |
|
447 Type "name" "tyty" |
|
448 | Dty "name" |
|
449 | DStru "name" "mexp" |
|
450 | Val "name" "trmtrm" |
|
451 and sexp = |
|
452 Sig sbody |
|
453 | SFunc "name" "sexp" "sexp" |
|
454 and sbody = |
|
455 SEmpty |
|
456 | SSeq C::spec D::sbody bind "Cbinders C" in D |
|
457 and spec = |
|
458 Type1 "name" |
|
459 | Type2 "name" "tyty" |
|
460 | SStru "name" "sexp" |
|
461 | SVal "name" "tyty" |
|
462 and tyty = |
|
463 Tyref1 "name" |
|
464 | Tyref2 "path" "tyty" |
|
465 | Fun "tyty" "tyty" |
|
466 and path = |
|
467 Sref1 "name" |
|
468 | Sref2 "path" "name" |
|
469 and trmtrm = |
|
470 Tref1 "name" |
|
471 | Tref2 "path" "name" |
|
472 | Lam' v::"name" "tyty" M::"trmtrm" bind v in M |
|
473 | App' "trmtrm" "trmtrm" |
|
474 | Let' "body" "trmtrm" |
|
475 binder |
|
476 cbinders :: "defn \<Rightarrow> atom set" |
|
477 and Cbinders :: "spec \<Rightarrow> atom set" |
|
478 where |
|
479 "cbinders (Type t T) = {atom t}" |
|
480 | "cbinders (Dty t) = {atom t}" |
|
481 | "cbinders (DStru x s) = {atom x}" |
|
482 | "cbinders (Val v M) = {atom v}" |
|
483 | "Cbinders (Type1 t) = {atom t}" |
|
484 | "Cbinders (Type2 t T) = {atom t}" |
|
485 | "Cbinders (SStru x S) = {atom x}" |
|
486 | "Cbinders (SVal v T) = {atom v}" |
|
487 |
|
488 (* core haskell *) |
|
489 print_theorems |
|
490 |
|
491 atom_decl var |
|
492 atom_decl tvar |
|
493 |
|
494 |
|
495 (* there are types, coercion types and regular types *) |
|
496 nominal_datatype tkind = |
|
497 KStar |
|
498 | KFun "tkind" "tkind" |
|
499 and ckind = |
|
500 CKEq "ty" "ty" |
|
501 and ty = |
|
502 TVar "tvar" |
|
503 | TC "string" |
|
504 | TApp "ty" "ty" |
|
505 | TFun "string" "ty list" |
|
506 | TAll tv::"tvar" "tkind" T::"ty" bind tv in T |
|
507 | TEq "ty" "ty" "ty" |
|
508 and co = |
|
509 CC "string" |
|
510 | CApp "co" "co" |
|
511 | CFun "string" "co list" |
|
512 | CAll tv::"tvar" "ckind" C::"co" bind tv in C |
|
513 | CEq "co" "co" "co" |
|
514 | CSym "co" |
|
515 | CCir "co" "co" |
|
516 | CLeft "co" |
|
517 | CRight "co" |
|
518 | CSim "co" |
|
519 | CRightc "co" |
|
520 | CLeftc "co" |
|
521 | CCoe "co" "co" |
|
522 |
|
523 |
|
524 typedecl ty --"hack since ty is not yet defined" |
|
525 |
|
526 abbreviation |
|
527 "atoms A \<equiv> atom ` A" |
|
528 |
|
529 nominal_datatype trm = |
|
530 Var "var" |
|
531 | C "string" |
|
532 | LAM tv::"tvar" "kind" t::"trm" bind tv in t |
|
533 | APP "trm" "ty" |
|
534 | Lam v::"var" "ty" t::"trm" bind v in t |
|
535 | App "trm" "trm" |
|
536 | Let x::"var" "ty" "trm" t::"trm" bind x in t |
|
537 | Case "trm" "assoc list" |
|
538 | Cast "trm" "ty" --"ty is supposed to be a coercion type only" |
|
539 and assoc = |
|
540 A p::"pat" t::"trm" bind "bv p" in t |
|
541 and pat = |
|
542 K "string" "(tvar \<times> kind) list" "(var \<times> ty) list" |
|
543 binder |
|
544 bv :: "pat \<Rightarrow> atom set" |
|
545 where |
|
546 "bv (K s ts vs) = (atoms (set (map fst ts))) \<union> (atoms (set (map fst vs)))" |
|
547 |
|
548 (* |
|
549 compat (K s ts vs) pi (K s' ts' vs') == |
|
550 s = s' & |
|
551 |
|
552 *) |
|
553 |
|
554 |
|
555 (*thm bv_raw.simps*) |
|
556 |
|
557 (* example 3 from Peter Sewell's bestiary *) |
|
558 nominal_datatype exp = |
|
559 VarP "name" |
|
560 | AppP "exp" "exp" |
|
561 | LamP x::"name" e::"exp" bind x in e |
|
562 | LetP x::"name" p::"pat" e1::"exp" e2::"exp" bind x in e2, bind "bp p" in e1 |
|
563 and pat = |
|
564 PVar "name" |
|
565 | PUnit |
|
566 | PPair "pat" "pat" |
|
567 binder |
|
568 bp :: "pat \<Rightarrow> atom set" |
|
569 where |
|
570 "bp (PVar x) = {atom x}" |
|
571 | "bp (PUnit) = {}" |
|
572 | "bp (PPair p1 p2) = bp p1 \<union> bp p2" |
|
573 thm alpha_exp_raw_alpha_pat_raw.intros |
|
574 |
|
575 (* example 6 from Peter Sewell's bestiary *) |
|
576 nominal_datatype exp6 = |
|
577 EVar name |
|
578 | EPair exp6 exp6 |
|
579 | ELetRec x::name p::pat6 e1::exp6 e2::exp6 bind x in e1, bind x in e2, bind "bp6 p" in e1 |
|
580 and pat6 = |
|
581 PVar' name |
|
582 | PUnit' |
|
583 | PPair' pat6 pat6 |
|
584 binder |
|
585 bp6 :: "pat6 \<Rightarrow> atom set" |
|
586 where |
|
587 "bp6 (PVar' x) = {atom x}" |
|
588 | "bp6 (PUnit') = {}" |
|
589 | "bp6 (PPair' p1 p2) = bp6 p1 \<union> bp6 p2" |
|
590 thm alpha_exp6_raw_alpha_pat6_raw.intros |
|
591 |
|
592 (* example 7 from Peter Sewell's bestiary *) |
|
593 nominal_datatype exp7 = |
|
594 EVar name |
|
595 | EUnit |
|
596 | EPair exp7 exp7 |
|
597 | ELetRec l::lrbs e::exp7 bind "b7s l" in e, bind "b7s l" in l |
|
598 and lrb = |
|
599 Assign name exp7 |
|
600 and lrbs = |
|
601 Single lrb |
|
602 | More lrb lrbs |
|
603 binder |
|
604 b7 :: "lrb \<Rightarrow> atom set" and |
|
605 b7s :: "lrbs \<Rightarrow> atom set" |
|
606 where |
|
607 "b7 (Assign x e) = {atom x}" |
|
608 | "b7s (Single a) = b7 a" |
|
609 | "b7s (More a as) = (b7 a) \<union> (b7s as)" |
|
610 thm alpha_exp7_raw_alpha_lrb_raw_alpha_lrbs_raw.intros |
|
611 |
|
612 (* example 8 from Peter Sewell's bestiary *) |
|
613 nominal_datatype exp8 = |
|
614 EVar name |
|
615 | EUnit |
|
616 | EPair exp8 exp8 |
|
617 | ELetRec l::lrbs8 e::exp8 bind "b_lrbs8 l" in e, bind "b_lrbs8 l" in l |
|
618 and fnclause = |
|
619 K x::name p::pat8 e::exp8 bind "b_pat p" in e |
|
620 and fnclauses = |
|
621 S fnclause |
|
622 | ORs fnclause fnclauses |
|
623 and lrb8 = |
|
624 Clause fnclauses |
|
625 and lrbs8 = |
|
626 Single lrb8 |
|
627 | More lrb8 lrbs8 |
|
628 and pat8 = |
|
629 PVar name |
|
630 | PUnit |
|
631 | PPair pat8 pat8 |
|
632 binder |
|
633 b_lrbs8 :: "lrbs8 \<Rightarrow> atom set" and |
|
634 b_pat :: "pat8 \<Rightarrow> atom set" and |
|
635 b_fnclauses :: "fnclauses \<Rightarrow> atom set" and |
|
636 b_fnclause :: "fnclause \<Rightarrow> atom set" and |
|
637 b_lrb8 :: "lrb8 \<Rightarrow> atom set" |
|
638 where |
|
639 "b_lrbs8 (Single l) = b_lrb8 l" |
|
640 | "b_lrbs8 (More l ls) = b_lrb8 l \<union> b_lrbs8 ls" |
|
641 | "b_pat (PVar x) = {atom x}" |
|
642 | "b_pat (PUnit) = {}" |
|
643 | "b_pat (PPair p1 p2) = b_pat p1 \<union> b_pat p2" |
|
644 | "b_fnclauses (S fc) = (b_fnclause fc)" |
|
645 | "b_fnclauses (ORs fc fcs) = (b_fnclause fc) \<union> (b_fnclauses fcs)" |
|
646 | "b_lrb8 (Clause fcs) = (b_fnclauses fcs)" |
|
647 | "b_fnclause (K x pat exp8) = {atom x}" |
|
648 thm alpha_exp8_raw_alpha_fnclause_raw_alpha_fnclauses_raw_alpha_lrb8_raw_alpha_lrbs8_raw_alpha_pat8_raw.intros |
|
649 |
|
650 |
|
651 |
|
652 |
|
653 (* example 9 from Peter Sewell's bestiary *) |
|
654 (* run out of steam at the moment *) |
|
655 |
|
656 end |
|
657 |
|
658 |
|
659 |