|
1 header {* CPS transformation of Danvy and Filinski *} |
|
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 |
|
103 nominal_primrec |
|
104 CPS1 :: "lt \<Rightarrow> (lt \<Rightarrow> lt) \<Rightarrow> lt" ("_*_" [100,100] 100) |
|
105 and |
|
106 CPS2 :: "lt \<Rightarrow> lt \<Rightarrow> lt" ("_^_" [100,100] 100) |
|
107 where |
|
108 "eqvt k \<Longrightarrow> (x~)*k = k (x~)" |
|
109 | "eqvt k \<Longrightarrow> (M$N)*k = M*(%m. (N*(%n.((m $ n) $ (Abs c (k (c~)))))))" |
|
110 | "eqvt k \<Longrightarrow> atom c \<sharp> (x, M) \<Longrightarrow> (Abs x M)*k = k (Abs x (Abs c (M^(c~))))" |
|
111 | "\<not>eqvt k \<Longrightarrow> (CPS1 t k) = t" |
|
112 | "(x~)^l = l $ (x~)" |
|
113 | "(M$N)^l = M*(%m. (N*(%n.((m $ n) $ l))))" |
|
114 | "atom c \<sharp> (x, M) \<Longrightarrow> (Abs x M)^l = l $ (Abs x (Abs c (M^(c~))))" |
|
115 apply (simp only: eqvt_def CPS1_CPS2_graph_def) |
|
116 apply (rule, perm_simp, rule) |
|
117 apply auto |
|
118 apply (case_tac x) |
|
119 apply (case_tac a) |
|
120 apply (case_tac "eqvt b") |
|
121 apply (rule_tac y="aa" in lt.strong_exhaust) |
|
122 apply auto[4] |
|
123 apply (rule_tac x="(name, lt)" and ?'a="name" in obtain_fresh) |
|
124 apply (simp add: fresh_at_base Abs1_eq_iff) |
|
125 apply (case_tac b) |
|
126 apply (rule_tac y="a" in lt.strong_exhaust) |
|
127 apply auto[3] |
|
128 apply blast |
|
129 apply (rule_tac x="(name, lt)" and ?'a="name" in obtain_fresh) |
|
130 apply (simp add: fresh_at_base Abs1_eq_iff) |
|
131 apply blast |
|
132 --"-" |
|
133 apply (subgoal_tac "Abs c (ka (c~)) = Abs ca (ka (ca~))") |
|
134 apply (simp only:) |
|
135 apply (simp add: Abs1_eq_iff) |
|
136 apply (case_tac "c=ca") |
|
137 apply simp_all[2] |
|
138 apply rule |
|
139 apply (perm_simp) |
|
140 apply (simp add: eqvt_def) |
|
141 apply (simp add: fresh_def) |
|
142 apply (rule contra_subsetD[OF supp_fun_app]) |
|
143 back |
|
144 apply (simp add: supp_fun_eqvt lt.supp supp_at_base) |
|
145 --"-" |
|
146 apply (rule arg_cong) |
|
147 back |
|
148 apply simp |
|
149 apply (erule Abs_lst1_fcb2) |
|
150 apply simp |
|
151 apply (thin_tac "eqvt ka") |
|
152 apply (rule_tac x="(c, ca, x, xa, M, Ma)" and ?'a="name" in obtain_fresh) |
|
153 apply (subgoal_tac "Abs c (CPS1_CPS2_sumC (Inr (M, c~))) = Abs a (CPS1_CPS2_sumC (Inr (M, a~)))") |
|
154 prefer 2 |
|
155 apply (simp add: Abs1_eq_iff') |
|
156 apply (case_tac "c = a") |
|
157 apply simp_all[2] |
|
158 apply rule |
|
159 apply (simp add: eqvt_at_def) |
|
160 apply (simp add: swap_fresh_fresh fresh_Pair_elim) |
|
161 apply (erule fresh_eqvt_at) |
|
162 apply (simp add: supp_Inr finite_supp) |
|
163 apply (simp add: fresh_Inr fresh_Pair lt.fresh fresh_at_base) |
|
164 apply (subgoal_tac "Abs ca (CPS1_CPS2_sumC (Inr (Ma, ca~))) = Abs a (CPS1_CPS2_sumC (Inr (Ma, a~)))") |
|
165 prefer 2 |
|
166 apply (simp add: Abs1_eq_iff') |
|
167 apply (case_tac "ca = a") |
|
168 apply simp_all[2] |
|
169 apply rule |
|
170 apply (simp add: eqvt_at_def) |
|
171 apply (simp add: swap_fresh_fresh fresh_Pair_elim) |
|
172 apply (erule fresh_eqvt_at) |
|
173 apply (simp add: supp_Inr finite_supp) |
|
174 apply (simp add: fresh_Inr fresh_Pair lt.fresh fresh_at_base) |
|
175 apply (simp only: ) |
|
176 apply (erule Abs_lst1_fcb2) |
|
177 apply (simp add: Abs_fresh_iff) |
|
178 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~)))") |
|
180 apply (simp add: perm_supp_eq fresh_star_def lt.fresh) |
|
181 apply (drule sym) |
|
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 |
|
353 end |
|
354 |
|
355 |
|
356 |