1 header {* CPS transformation of Danvy and Filinski *} |
1 header {* CPS transformation of Danvy and Filinski *} |
2 theory CPS3_DanvyFilinski imports Lt begin |
2 theory CPS3_DanvyFilinski imports Lt begin |
3 |
|
4 |
|
5 lemma Abs_lst_fcb2: |
|
6 fixes as bs :: "atom list" |
|
7 and x y :: "'b :: fs" |
|
8 and c::"'c::fs" |
|
9 assumes eq: "[as]lst. x = [bs]lst. y" |
|
10 and fcb1: "(set as) \<sharp>* c \<Longrightarrow> (set as) \<sharp>* f as x c" |
|
11 and fresh1: "set as \<sharp>* c" |
|
12 and fresh2: "set bs \<sharp>* c" |
|
13 and perm1: "\<And>p. supp p \<sharp>* c \<Longrightarrow> p \<bullet> (f as x c) = f (p \<bullet> as) (p \<bullet> x) c" |
|
14 and perm2: "\<And>p. supp p \<sharp>* c \<Longrightarrow> p \<bullet> (f bs y c) = f (p \<bullet> bs) (p \<bullet> y) c" |
|
15 shows "f as x c = f bs y c" |
|
16 proof - |
|
17 have "supp (as, x, c) supports (f as x c)" |
|
18 unfolding supports_def fresh_def[symmetric] |
|
19 by (simp add: fresh_Pair perm1 fresh_star_def supp_swap swap_fresh_fresh) |
|
20 then have fin1: "finite (supp (f as x c))" |
|
21 by (auto intro: supports_finite simp add: finite_supp) |
|
22 have "supp (bs, y, c) supports (f bs y c)" |
|
23 unfolding supports_def fresh_def[symmetric] |
|
24 by (simp add: fresh_Pair perm2 fresh_star_def supp_swap swap_fresh_fresh) |
|
25 then have fin2: "finite (supp (f bs y c))" |
|
26 by (auto intro: supports_finite simp add: finite_supp) |
|
27 obtain q::"perm" where |
|
28 fr1: "(q \<bullet> (set as)) \<sharp>* (x, c, f as x c, f bs y c)" and |
|
29 fr2: "supp q \<sharp>* Abs_lst as x" and |
|
30 inc: "supp q \<subseteq> (set as) \<union> q \<bullet> (set as)" |
|
31 using at_set_avoiding3[where xs="set as" and c="(x, c, f as x c, f bs y c)" and x="[as]lst. x"] |
|
32 fin1 fin2 |
|
33 by (auto simp add: supp_Pair finite_supp Abs_fresh_star dest: fresh_star_supp_conv) |
|
34 have "Abs_lst (q \<bullet> as) (q \<bullet> x) = q \<bullet> Abs_lst as x" by simp |
|
35 also have "\<dots> = Abs_lst as x" |
|
36 by (simp only: fr2 perm_supp_eq) |
|
37 finally have "Abs_lst (q \<bullet> as) (q \<bullet> x) = Abs_lst bs y" using eq by simp |
|
38 then obtain r::perm where |
|
39 qq1: "q \<bullet> x = r \<bullet> y" and |
|
40 qq2: "q \<bullet> as = r \<bullet> bs" and |
|
41 qq3: "supp r \<subseteq> (q \<bullet> (set as)) \<union> set bs" |
|
42 apply(drule_tac sym) |
|
43 apply(simp only: Abs_eq_iff2 alphas) |
|
44 apply(erule exE) |
|
45 apply(erule conjE)+ |
|
46 apply(drule_tac x="p" in meta_spec) |
|
47 apply(simp add: set_eqvt) |
|
48 apply(blast) |
|
49 done |
|
50 have "(set as) \<sharp>* f as x c" |
|
51 apply(rule fcb1) |
|
52 apply(rule fresh1) |
|
53 done |
|
54 then have "q \<bullet> ((set as) \<sharp>* f as x c)" |
|
55 by (simp add: permute_bool_def) |
|
56 then have "set (q \<bullet> as) \<sharp>* f (q \<bullet> as) (q \<bullet> x) c" |
|
57 apply(simp add: fresh_star_eqvt set_eqvt) |
|
58 apply(subst (asm) perm1) |
|
59 using inc fresh1 fr1 |
|
60 apply(auto simp add: fresh_star_def fresh_Pair) |
|
61 done |
|
62 then have "set (r \<bullet> bs) \<sharp>* f (r \<bullet> bs) (r \<bullet> y) c" using qq1 qq2 by simp |
|
63 then have "r \<bullet> ((set bs) \<sharp>* f bs y c)" |
|
64 apply(simp add: fresh_star_eqvt set_eqvt) |
|
65 apply(subst (asm) perm2[symmetric]) |
|
66 using qq3 fresh2 fr1 |
|
67 apply(auto simp add: set_eqvt fresh_star_def fresh_Pair) |
|
68 done |
|
69 then have fcb2: "(set bs) \<sharp>* f bs y c" by (simp add: permute_bool_def) |
|
70 have "f as x c = q \<bullet> (f as x c)" |
|
71 apply(rule perm_supp_eq[symmetric]) |
|
72 using inc fcb1[OF fresh1] fr1 by (auto simp add: fresh_star_def) |
|
73 also have "\<dots> = f (q \<bullet> as) (q \<bullet> x) c" |
|
74 apply(rule perm1) |
|
75 using inc fresh1 fr1 by (auto simp add: fresh_star_def) |
|
76 also have "\<dots> = f (r \<bullet> bs) (r \<bullet> y) c" using qq1 qq2 by simp |
|
77 also have "\<dots> = r \<bullet> (f bs y c)" |
|
78 apply(rule perm2[symmetric]) |
|
79 using qq3 fresh2 fr1 by (auto simp add: fresh_star_def) |
|
80 also have "... = f bs y c" |
|
81 apply(rule perm_supp_eq) |
|
82 using qq3 fr1 fcb2 by (auto simp add: fresh_star_def) |
|
83 finally show ?thesis by simp |
|
84 qed |
|
85 |
|
86 lemma Abs_lst1_fcb2: |
|
87 fixes a b :: "atom" |
|
88 and x y :: "'b :: fs" |
|
89 and c::"'c :: fs" |
|
90 assumes e: "(Abs_lst [a] x) = (Abs_lst [b] y)" |
|
91 and fcb1: "a \<sharp> c \<Longrightarrow> a \<sharp> f a x c" |
|
92 and fresh: "{a, b} \<sharp>* c" |
|
93 and perm1: "\<And>p. supp p \<sharp>* c \<Longrightarrow> p \<bullet> (f a x c) = f (p \<bullet> a) (p \<bullet> x) c" |
|
94 and perm2: "\<And>p. supp p \<sharp>* c \<Longrightarrow> p \<bullet> (f b y c) = f (p \<bullet> b) (p \<bullet> y) c" |
|
95 shows "f a x c = f b y c" |
|
96 using e |
|
97 apply(drule_tac Abs_lst_fcb2[where c="c" and f="\<lambda>(as::atom list) . f (hd as)"]) |
|
98 apply(simp_all) |
|
99 using fcb1 fresh perm1 perm2 |
|
100 apply(simp_all add: fresh_star_def) |
|
101 done |
|
102 |
3 |
103 nominal_primrec |
4 nominal_primrec |
104 CPS1 :: "lt \<Rightarrow> (lt \<Rightarrow> lt) \<Rightarrow> lt" ("_*_" [100,100] 100) |
5 CPS1 :: "lt \<Rightarrow> (lt \<Rightarrow> lt) \<Rightarrow> lt" ("_*_" [100,100] 100) |
105 and |
6 and |
106 CPS2 :: "lt \<Rightarrow> lt \<Rightarrow> lt" ("_^_" [100,100] 100) |
7 CPS2 :: "lt \<Rightarrow> lt \<Rightarrow> lt" ("_^_" [100,100] 100) |
171 apply (simp add: swap_fresh_fresh fresh_Pair_elim) |
69 apply (simp add: swap_fresh_fresh fresh_Pair_elim) |
172 apply (erule fresh_eqvt_at) |
70 apply (erule fresh_eqvt_at) |
173 apply (simp add: supp_Inr finite_supp) |
71 apply (simp add: supp_Inr finite_supp) |
174 apply (simp add: fresh_Inr fresh_Pair lt.fresh fresh_at_base) |
72 apply (simp add: fresh_Inr fresh_Pair lt.fresh fresh_at_base) |
175 apply (simp only: ) |
73 apply (simp only: ) |
176 apply (erule Abs_lst1_fcb2) |
74 apply (erule_tac c="a" in Abs_lst1_fcb2') |
177 apply (simp add: Abs_fresh_iff) |
75 apply (simp add: Abs_fresh_iff lt.fresh) |
178 apply (simp add: fresh_star_def fresh_Pair_elim lt.fresh fresh_at_base) |
76 apply (simp add: fresh_star_def fresh_Pair_elim lt.fresh fresh_at_base) |
179 apply (subgoal_tac "p \<bullet> CPS1_CPS2_sumC (Inr (M, a~)) = CPS1_CPS2_sumC (p \<bullet> (Inr (M, a~)))") |
77 apply (subgoal_tac "p \<bullet> CPS1_CPS2_sumC (Inr (M, a~)) = CPS1_CPS2_sumC (p \<bullet> (Inr (M, a~)))") |
180 apply (simp add: perm_supp_eq fresh_star_def lt.fresh) |
78 apply (simp add: perm_supp_eq fresh_star_def lt.fresh) |
181 apply (drule sym) |
79 oops |
182 apply (simp only: ) |
|
183 apply (simp only: permute_Abs_lst) |
|
184 apply simp |
|
185 apply (simp add: eqvt_at_def) |
|
186 apply (drule sym) |
|
187 apply (simp only:) |
|
188 apply (simp add: Abs_fresh_iff lt.fresh) |
|
189 apply clarify |
|
190 apply (erule fresh_eqvt_at) |
|
191 apply (simp add: supp_Inr finite_supp) |
|
192 apply (simp add: fresh_Inr fresh_Pair lt.fresh fresh_at_base) |
|
193 apply (drule sym) |
|
194 apply (drule sym) |
|
195 apply (drule sym) |
|
196 apply (simp only:) |
|
197 apply (thin_tac "Abs a (CPS1_CPS2_sumC (Inr (M, a~))) = Abs c (CPS1_CPS2_sumC (Inr (M, c~)))") |
|
198 apply (thin_tac "Abs a (CPS1_CPS2_sumC (Inr (Ma, a~))) = Abs ca (CPS1_CPS2_sumC (Inr (Ma, ca~)))") |
|
199 apply (thin_tac "atom a \<sharp> (c, ca, x, xa, M, Ma)") |
|
200 apply (simp add: fresh_Pair_elim) |
|
201 apply (subst iffD1[OF meta_eq_to_obj_eq[OF eqvt_at_def]]) |
|
202 back |
|
203 back |
|
204 back |
|
205 apply assumption |
|
206 apply (simp add: Abs1_eq_iff' fresh_Pair_elim fresh_at_base swap_fresh_fresh lt.fresh) |
|
207 apply (case_tac "(atom x \<rightleftharpoons> atom xa) \<bullet> c = ca") |
|
208 apply simp_all[3] |
|
209 apply rule |
|
210 apply (case_tac "c = xa") |
|
211 apply simp_all[2] |
|
212 apply (simp add: eqvt_at_def) |
|
213 apply clarify |
|
214 apply (smt flip_def permute_flip_at permute_swap_cancel swap_fresh_fresh) |
|
215 apply (simp add: eqvt_at_def) |
|
216 apply clarify |
|
217 apply (smt atom_eq_iff atom_eqvt flip_def fresh_eqvt permute_flip_at permute_swap_cancel swap_at_base_simps(3) swap_fresh_fresh) |
|
218 apply (case_tac "c = xa") |
|
219 apply simp |
|
220 apply (subgoal_tac "((ca \<leftrightarrow> x) \<bullet> (atom x)) \<sharp> (ca \<leftrightarrow> x) \<bullet> CPS1_CPS2_sumC (Inr (Ma, ca~))") |
|
221 apply (simp add: atom_eqvt eqvt_at_def) |
|
222 apply (simp add: flip_fresh_fresh) |
|
223 apply (subst fresh_permute_iff) |
|
224 apply (erule fresh_eqvt_at) |
|
225 apply (simp add: supp_Inr finite_supp) |
|
226 apply (simp add: fresh_Inr lt.fresh fresh_at_base fresh_Pair) |
|
227 apply simp |
|
228 apply clarify |
|
229 apply (subgoal_tac "atom ca \<sharp> (atom x \<rightleftharpoons> atom xa) \<bullet> CPS1_CPS2_sumC (Inr (M, c~))") |
|
230 apply (simp add: eqvt_at_def) |
|
231 apply (subgoal_tac "(atom x \<rightleftharpoons> atom xa) \<bullet> atom ca \<sharp> CPS1_CPS2_sumC (Inr (M, c~))") |
|
232 apply (metis Nominal2_Base.swap_commute fresh_permute_iff permute_swap_cancel2) |
|
233 apply (erule fresh_eqvt_at) |
|
234 apply (simp add: finite_supp supp_Inr) |
|
235 apply (simp add: fresh_Inr fresh_Pair lt.fresh) |
|
236 apply rule |
|
237 apply (metis Nominal2_Base.swap_commute fresh_permute_iff permute_swap_cancel2) |
|
238 apply (simp add: fresh_def supp_at_base) |
|
239 apply (metis atom_eq_iff permute_swap_cancel2 swap_atom_simps(3)) |
|
240 --"-" |
|
241 apply (rule_tac x="(c, ca, x, xa, M, Ma)" and ?'a="name" in obtain_fresh) |
|
242 apply (subgoal_tac "Abs c (CPS1_CPS2_sumC (Inr (M, c~))) = Abs a (CPS1_CPS2_sumC (Inr (M, a~)))") |
|
243 prefer 2 |
|
244 apply (simp add: Abs1_eq_iff') |
|
245 apply (case_tac "c = a") |
|
246 apply simp_all[2] |
|
247 apply rule |
|
248 apply (simp add: eqvt_at_def) |
|
249 apply (simp add: swap_fresh_fresh fresh_Pair_elim) |
|
250 apply (erule fresh_eqvt_at) |
|
251 apply (simp add: supp_Inr finite_supp) |
|
252 apply (simp add: fresh_Inr fresh_Pair lt.fresh fresh_at_base) |
|
253 apply (subgoal_tac "Abs ca (CPS1_CPS2_sumC (Inr (Ma, ca~))) = Abs a (CPS1_CPS2_sumC (Inr (Ma, a~)))") |
|
254 prefer 2 |
|
255 apply (simp add: Abs1_eq_iff') |
|
256 apply (case_tac "ca = a") |
|
257 apply simp_all[2] |
|
258 apply rule |
|
259 apply (simp add: eqvt_at_def) |
|
260 apply (simp add: swap_fresh_fresh fresh_Pair_elim) |
|
261 apply (erule fresh_eqvt_at) |
|
262 apply (simp add: supp_Inr finite_supp) |
|
263 apply (simp add: fresh_Inr fresh_Pair lt.fresh fresh_at_base) |
|
264 apply (simp only: ) |
|
265 apply (erule Abs_lst1_fcb) |
|
266 apply (simp add: Abs_fresh_iff) |
|
267 apply (drule sym) |
|
268 apply (simp only:) |
|
269 apply (simp add: Abs_fresh_iff lt.fresh) |
|
270 apply clarify |
|
271 apply (erule fresh_eqvt_at) |
|
272 apply (simp add: supp_Inr finite_supp) |
|
273 apply (simp add: fresh_Inr fresh_Pair lt.fresh fresh_at_base) |
|
274 apply (drule sym) |
|
275 apply (drule sym) |
|
276 apply (drule sym) |
|
277 apply (simp only:) |
|
278 apply (thin_tac "Abs a (CPS1_CPS2_sumC (Inr (M, a~))) = Abs c (CPS1_CPS2_sumC (Inr (M, c~)))") |
|
279 apply (thin_tac "Abs a (CPS1_CPS2_sumC (Inr (Ma, a~))) = Abs ca (CPS1_CPS2_sumC (Inr (Ma, ca~)))") |
|
280 apply (thin_tac "atom a \<sharp> (c, ca, x, xa, M, Ma)") |
|
281 apply (simp add: fresh_Pair_elim) |
|
282 apply (subst iffD1[OF meta_eq_to_obj_eq[OF eqvt_at_def]]) |
|
283 back |
|
284 back |
|
285 back |
|
286 apply assumption |
|
287 apply (simp add: Abs1_eq_iff' fresh_Pair_elim fresh_at_base swap_fresh_fresh lt.fresh) |
|
288 apply (case_tac "(atom x \<rightleftharpoons> atom xa) \<bullet> c = ca") |
|
289 apply simp_all[3] |
|
290 apply rule |
|
291 apply (case_tac "c = xa") |
|
292 apply simp_all[2] |
|
293 apply (simp add: eqvt_at_def) |
|
294 apply clarify |
|
295 apply (smt flip_def permute_flip_at permute_swap_cancel swap_fresh_fresh) |
|
296 apply (simp add: eqvt_at_def) |
|
297 apply clarify |
|
298 apply (smt atom_eq_iff atom_eqvt flip_def fresh_eqvt permute_flip_at permute_swap_cancel swap_at_base_simps(3) swap_fresh_fresh) |
|
299 apply (case_tac "c = xa") |
|
300 apply simp |
|
301 apply (subgoal_tac "((ca \<leftrightarrow> x) \<bullet> (atom x)) \<sharp> (ca \<leftrightarrow> x) \<bullet> CPS1_CPS2_sumC (Inr (Ma, ca~))") |
|
302 apply (simp add: atom_eqvt eqvt_at_def) |
|
303 apply (simp add: flip_fresh_fresh) |
|
304 apply (subst fresh_permute_iff) |
|
305 apply (erule fresh_eqvt_at) |
|
306 apply (simp add: supp_Inr finite_supp) |
|
307 apply (simp add: fresh_Inr lt.fresh fresh_at_base fresh_Pair) |
|
308 apply simp |
|
309 apply clarify |
|
310 apply (subgoal_tac "atom ca \<sharp> (atom x \<rightleftharpoons> atom xa) \<bullet> CPS1_CPS2_sumC (Inr (M, c~))") |
|
311 apply (simp add: eqvt_at_def) |
|
312 apply (subgoal_tac "(atom x \<rightleftharpoons> atom xa) \<bullet> atom ca \<sharp> CPS1_CPS2_sumC (Inr (M, c~))") |
|
313 apply (metis Nominal2_Base.swap_commute fresh_permute_iff permute_swap_cancel2) |
|
314 apply (erule fresh_eqvt_at) |
|
315 apply (simp add: finite_supp supp_Inr) |
|
316 apply (simp add: fresh_Inr fresh_Pair lt.fresh) |
|
317 apply rule |
|
318 apply (metis Nominal2_Base.swap_commute fresh_permute_iff permute_swap_cancel2) |
|
319 apply (simp add: fresh_def supp_at_base) |
|
320 apply (metis atom_eq_iff permute_swap_cancel2 swap_atom_simps(3)) |
|
321 done |
|
322 |
|
323 termination |
|
324 by lexicographic_order |
|
325 |
|
326 definition psi:: "lt => lt" |
|
327 where [simp]: "psi V == V*(\<lambda>x. x)" |
|
328 |
|
329 section {* Simple consequence of CPS *} |
|
330 |
|
331 lemma [simp]: "eqvt (\<lambda>x\<Colon>lt. x)" |
|
332 by (simp add: eqvt_def eqvt_bound eqvt_lambda) |
|
333 |
|
334 lemma value_eq1 : "isValue V \<Longrightarrow> eqvt k \<Longrightarrow> V*k = k (psi V)" |
|
335 apply (cases V rule: lt.exhaust) |
|
336 apply simp_all |
|
337 apply (rule_tac x="(name, lt)" and ?'a="name" in obtain_fresh) |
|
338 apply simp |
|
339 done |
|
340 |
|
341 lemma value_eq2 : "isValue V \<Longrightarrow> V^K = K $ (psi V)" |
|
342 apply (cases V rule: lt.exhaust) |
|
343 apply simp_all |
|
344 apply (rule_tac x="(name, lt)" and ?'a="name" in obtain_fresh) |
|
345 apply simp |
|
346 done |
|
347 |
|
348 lemma value_eq3' : "~isValue M \<Longrightarrow> eqvt k \<Longrightarrow> M*k = (M^(Abs n (k (Var n))))" |
|
349 by (cases M rule: lt.exhaust) auto |
|
350 |
|
351 |
|
352 |
80 |
353 end |
81 end |
354 |
82 |
355 |
83 |
356 |
84 |