1 header {* CPS transformation of Danvy and Filinski *} |
|
2 theory CPS3_DanvyFilinski imports Lt begin |
|
3 |
|
4 nominal_primrec |
|
5 CPS1 :: "lt \<Rightarrow> (lt \<Rightarrow> lt) \<Rightarrow> lt" ("_*_" [100,100] 100) |
|
6 and |
|
7 CPS2 :: "lt \<Rightarrow> lt \<Rightarrow> lt" ("_^_" [100,100] 100) |
|
8 where |
|
9 "eqvt k \<Longrightarrow> (x~)*k = k (x~)" |
|
10 | "eqvt k \<Longrightarrow> (M$N)*k = M*(%m. (N*(%n.((m $ n) $ (Lam c (k (c~)))))))" |
|
11 | "eqvt k \<Longrightarrow> atom c \<sharp> (x, M) \<Longrightarrow> (Lam x M)*k = k (Lam x (Lam c (M^(c~))))" |
|
12 | "\<not>eqvt k \<Longrightarrow> (CPS1 t k) = t" |
|
13 | "(x~)^l = l $ (x~)" |
|
14 | "(M$N)^l = M*(%m. (N*(%n.((m $ n) $ l))))" |
|
15 | "atom c \<sharp> (x, M) \<Longrightarrow> (Lam x M)^l = l $ (Lam x (Lam c (M^(c~))))" |
|
16 apply (simp only: eqvt_def CPS1_CPS2_graph_def) |
|
17 apply (rule, perm_simp, rule) |
|
18 apply auto |
|
19 apply (case_tac x) |
|
20 apply (case_tac a) |
|
21 apply (case_tac "eqvt b") |
|
22 apply (rule_tac y="aa" in lt.strong_exhaust) |
|
23 apply auto[4] |
|
24 apply (rule_tac x="(name, lt)" and ?'a="name" in obtain_fresh) |
|
25 apply (simp add: fresh_at_base Abs1_eq_iff) |
|
26 apply (case_tac b) |
|
27 apply (rule_tac y="a" in lt.strong_exhaust) |
|
28 apply auto[3] |
|
29 apply blast+ |
|
30 apply (rule_tac x="(name, lt)" and ?'a="name" in obtain_fresh) |
|
31 apply (simp add: fresh_at_base Abs1_eq_iff) |
|
32 --"-" |
|
33 apply (subgoal_tac "Lam c (ka (c~)) = Lam ca (ka (ca~))") |
|
34 apply (simp only:) |
|
35 apply (simp add: Abs1_eq_iff) |
|
36 apply (case_tac "c=ca") |
|
37 apply simp_all[2] |
|
38 apply rule |
|
39 apply (perm_simp) |
|
40 apply (simp add: eqvt_def) |
|
41 apply (simp add: fresh_def) |
|
42 apply (rule contra_subsetD[OF supp_fun_app]) |
|
43 back |
|
44 apply (simp add: supp_fun_eqvt lt.supp supp_at_base) |
|
45 --"-" |
|
46 apply (rule arg_cong) |
|
47 back |
|
48 apply simp |
|
49 apply (thin_tac "eqvt ka") |
|
50 apply (rule_tac x="(c, ca, x, xa, M, Ma)" and ?'a="name" in obtain_fresh) |
|
51 apply (subgoal_tac "Lam c (CPS1_CPS2_sumC (Inr (M, c~))) = Lam a (CPS1_CPS2_sumC (Inr (M, a~)))") |
|
52 prefer 2 |
|
53 apply (simp add: Abs1_eq_iff') |
|
54 apply (case_tac "c = a") |
|
55 apply simp_all[2] |
|
56 apply rule |
|
57 apply (simp add: eqvt_at_def) |
|
58 apply (simp add: swap_fresh_fresh fresh_Pair_elim) |
|
59 apply (erule fresh_eqvt_at) |
|
60 apply (simp add: supp_Inr finite_supp) |
|
61 apply (simp add: fresh_Inr fresh_Pair lt.fresh fresh_at_base) |
|
62 apply (subgoal_tac "Lam ca (CPS1_CPS2_sumC (Inr (Ma, ca~))) = Lam a (CPS1_CPS2_sumC (Inr (Ma, a~)))") |
|
63 prefer 2 |
|
64 apply (simp add: Abs1_eq_iff') |
|
65 apply (case_tac "ca = a") |
|
66 apply simp_all[2] |
|
67 apply rule |
|
68 apply (simp add: eqvt_at_def) |
|
69 apply (simp add: swap_fresh_fresh fresh_Pair_elim) |
|
70 apply (erule fresh_eqvt_at) |
|
71 apply (simp add: supp_Inr finite_supp) |
|
72 apply (simp add: fresh_Inr fresh_Pair lt.fresh fresh_at_base) |
|
73 apply (simp only: ) |
|
74 apply (erule Abs_lst1_fcb) |
|
75 apply (simp add: Abs_fresh_iff) |
|
76 apply (drule sym) |
|
77 apply (simp only:) |
|
78 apply (simp add: Abs_fresh_iff lt.fresh) |
|
79 apply clarify |
|
80 apply (erule fresh_eqvt_at) |
|
81 apply (simp add: supp_Inr finite_supp) |
|
82 apply (simp add: fresh_Inr fresh_Pair lt.fresh fresh_at_base) |
|
83 apply (drule sym) |
|
84 apply (drule sym) |
|
85 apply (drule sym) |
|
86 apply (simp only:) |
|
87 apply (thin_tac "Lam a (CPS1_CPS2_sumC (Inr (M, a~))) = Lam c (CPS1_CPS2_sumC (Inr (M, c~)))") |
|
88 apply (thin_tac "Lam a (CPS1_CPS2_sumC (Inr (Ma, a~))) = Lam ca (CPS1_CPS2_sumC (Inr (Ma, ca~)))") |
|
89 apply (thin_tac "atom a \<sharp> (c, ca, x, xa, M, Ma)") |
|
90 apply (simp add: fresh_Pair_elim) |
|
91 apply (subst iffD1[OF meta_eq_to_obj_eq[OF eqvt_at_def]]) |
|
92 back |
|
93 back |
|
94 back |
|
95 apply assumption |
|
96 apply (simp add: Abs1_eq_iff' fresh_Pair_elim fresh_at_base swap_fresh_fresh lt.fresh) |
|
97 apply (case_tac "(atom x \<rightleftharpoons> atom xa) \<bullet> c = ca") |
|
98 apply simp_all[3] |
|
99 apply rule |
|
100 apply (case_tac "c = xa") |
|
101 apply simp_all[2] |
|
102 apply (rotate_tac 1) |
|
103 apply (drule_tac q="(atom ca \<rightleftharpoons> atom x)" in eqvt_at_perm) |
|
104 apply (simp add: swap_fresh_fresh) |
|
105 apply (simp add: eqvt_at_def swap_fresh_fresh) |
|
106 apply (thin_tac "eqvt_at CPS1_CPS2_sumC (Inr (M, c~))") |
|
107 apply (simp add: eqvt_at_def) |
|
108 apply (drule_tac x="(atom ca \<rightleftharpoons> atom c)" in spec) |
|
109 apply simp |
|
110 apply (metis (no_types) atom_eq_iff fresh_permute_iff permute_swap_cancel swap_atom_simps(3) swap_fresh_fresh) |
|
111 apply (case_tac "c = xa") |
|
112 apply simp |
|
113 apply (subgoal_tac "((ca \<leftrightarrow> x) \<bullet> (atom x)) \<sharp> (ca \<leftrightarrow> x) \<bullet> CPS1_CPS2_sumC (Inr (Ma, ca~))") |
|
114 apply (simp add: atom_eqvt eqvt_at_def) |
|
115 apply (simp add: flip_fresh_fresh) |
|
116 apply (subst fresh_permute_iff) |
|
117 apply (erule fresh_eqvt_at) |
|
118 apply (simp add: supp_Inr finite_supp) |
|
119 apply (simp add: fresh_Inr lt.fresh fresh_at_base fresh_Pair) |
|
120 apply simp |
|
121 apply clarify |
|
122 apply (subgoal_tac "atom ca \<sharp> (atom x \<rightleftharpoons> atom xa) \<bullet> CPS1_CPS2_sumC (Inr (M, c~))") |
|
123 apply (simp add: eqvt_at_def) |
|
124 apply (subgoal_tac "(atom x \<rightleftharpoons> atom xa) \<bullet> atom ca \<sharp> CPS1_CPS2_sumC (Inr (M, c~))") |
|
125 apply (metis Nominal2_Base.swap_commute fresh_permute_iff permute_swap_cancel2) |
|
126 apply (erule fresh_eqvt_at) |
|
127 apply (simp add: finite_supp supp_Inr) |
|
128 apply (simp add: fresh_Inr fresh_Pair lt.fresh) |
|
129 apply rule |
|
130 apply (metis Nominal2_Base.swap_commute fresh_permute_iff permute_swap_cancel2) |
|
131 apply (simp add: fresh_def supp_at_base) |
|
132 apply (metis atom_eq_iff permute_swap_cancel2 swap_atom_simps(3)) |
|
133 --"-" |
|
134 apply (rule_tac x="(c, ca, x, xa, M, Ma)" and ?'a="name" in obtain_fresh) |
|
135 apply (subgoal_tac "Lam c (CPS1_CPS2_sumC (Inr (M, c~))) = Lam a (CPS1_CPS2_sumC (Inr (M, a~)))") |
|
136 prefer 2 |
|
137 apply (simp add: Abs1_eq_iff') |
|
138 apply (case_tac "c = a") |
|
139 apply simp_all[2] |
|
140 apply rule |
|
141 apply (simp add: eqvt_at_def) |
|
142 apply (simp add: swap_fresh_fresh fresh_Pair_elim) |
|
143 apply (erule fresh_eqvt_at) |
|
144 apply (simp add: supp_Inr finite_supp) |
|
145 apply (simp add: fresh_Inr fresh_Pair lt.fresh fresh_at_base) |
|
146 apply (subgoal_tac "Lam ca (CPS1_CPS2_sumC (Inr (Ma, ca~))) = Lam a (CPS1_CPS2_sumC (Inr (Ma, a~)))") |
|
147 prefer 2 |
|
148 apply (simp add: Abs1_eq_iff') |
|
149 apply (case_tac "ca = a") |
|
150 apply simp_all[2] |
|
151 apply rule |
|
152 apply (simp add: eqvt_at_def) |
|
153 apply (simp add: swap_fresh_fresh fresh_Pair_elim) |
|
154 apply (erule fresh_eqvt_at) |
|
155 apply (simp add: supp_Inr finite_supp) |
|
156 apply (simp add: fresh_Inr fresh_Pair lt.fresh fresh_at_base) |
|
157 apply (simp only: ) |
|
158 apply (erule Abs_lst1_fcb) |
|
159 apply (simp add: Abs_fresh_iff) |
|
160 apply (drule sym) |
|
161 apply (simp only:) |
|
162 apply (simp add: Abs_fresh_iff lt.fresh) |
|
163 apply clarify |
|
164 apply (erule fresh_eqvt_at) |
|
165 apply (simp add: supp_Inr finite_supp) (* TODO put sum of fs into fs typeclass *) |
|
166 apply (simp add: fresh_Inr fresh_Pair lt.fresh fresh_at_base) |
|
167 apply (drule sym) |
|
168 apply (drule sym) |
|
169 apply (drule sym) |
|
170 apply (simp only:) |
|
171 apply (thin_tac "Lam a (CPS1_CPS2_sumC (Inr (M, a~))) = Lam c (CPS1_CPS2_sumC (Inr (M, c~)))") |
|
172 apply (thin_tac "Lam a (CPS1_CPS2_sumC (Inr (Ma, a~))) = Lam ca (CPS1_CPS2_sumC (Inr (Ma, ca~)))") |
|
173 apply (thin_tac "atom a \<sharp> (c, ca, x, xa, M, Ma)") |
|
174 apply (simp add: fresh_Pair_elim) |
|
175 apply (subst iffD1[OF meta_eq_to_obj_eq[OF eqvt_at_def]]) |
|
176 back |
|
177 back |
|
178 back |
|
179 apply assumption |
|
180 apply (simp add: Abs1_eq_iff' fresh_Pair_elim fresh_at_base swap_fresh_fresh lt.fresh) |
|
181 apply (case_tac "(atom x \<rightleftharpoons> atom xa) \<bullet> c = ca") |
|
182 apply simp_all[3] |
|
183 apply rule |
|
184 apply (case_tac "c = xa") |
|
185 apply simp_all[2] |
|
186 apply (rotate_tac 1) |
|
187 apply (drule_tac q="(atom ca \<rightleftharpoons> atom x)" in eqvt_at_perm) |
|
188 apply (simp add: swap_fresh_fresh) |
|
189 apply (simp add: eqvt_at_def swap_fresh_fresh) |
|
190 apply (thin_tac "eqvt_at CPS1_CPS2_sumC (Inr (M, c~))") |
|
191 apply (simp add: eqvt_at_def) |
|
192 apply (drule_tac x="(atom ca \<rightleftharpoons> atom c)" in spec) |
|
193 apply simp |
|
194 apply (metis (no_types) atom_eq_iff fresh_permute_iff permute_swap_cancel swap_atom_simps(3) swap_fresh_fresh) |
|
195 apply (case_tac "c = xa") |
|
196 apply simp |
|
197 apply (subgoal_tac "((ca \<leftrightarrow> x) \<bullet> (atom x)) \<sharp> (ca \<leftrightarrow> x) \<bullet> CPS1_CPS2_sumC (Inr (Ma, ca~))") |
|
198 apply (simp add: atom_eqvt eqvt_at_def) |
|
199 apply (simp add: flip_fresh_fresh) |
|
200 apply (subst fresh_permute_iff) |
|
201 apply (erule fresh_eqvt_at) |
|
202 apply (simp add: supp_Inr finite_supp) |
|
203 apply (simp add: fresh_Inr lt.fresh fresh_at_base fresh_Pair) |
|
204 apply simp |
|
205 apply clarify |
|
206 apply (subgoal_tac "atom ca \<sharp> (atom x \<rightleftharpoons> atom xa) \<bullet> CPS1_CPS2_sumC (Inr (M, c~))") |
|
207 apply (simp add: eqvt_at_def) |
|
208 apply (subgoal_tac "(atom x \<rightleftharpoons> atom xa) \<bullet> atom ca \<sharp> CPS1_CPS2_sumC (Inr (M, c~))") |
|
209 apply (metis Nominal2_Base.swap_commute fresh_permute_iff permute_swap_cancel2) |
|
210 apply (erule fresh_eqvt_at) |
|
211 apply (simp add: finite_supp supp_Inr) |
|
212 apply (simp add: fresh_Inr fresh_Pair lt.fresh) |
|
213 apply rule |
|
214 apply (metis Nominal2_Base.swap_commute fresh_permute_iff permute_swap_cancel2) |
|
215 apply (simp add: fresh_def supp_at_base) |
|
216 apply (metis atom_eq_iff permute_swap_cancel2 swap_atom_simps(3)) |
|
217 done |
|
218 |
|
219 termination (eqvt) |
|
220 by lexicographic_order |
|
221 |
|
222 definition psi:: "lt => lt" |
|
223 where [simp]: "psi V == V*(\<lambda>x. x)" |
|
224 |
|
225 section {* Simple consequence of CPS *} |
|
226 |
|
227 lemma [simp]: "eqvt (\<lambda>x\<Colon>lt. x)" |
|
228 by (simp add: eqvt_def eqvt_bound eqvt_lambda) |
|
229 |
|
230 lemma value_eq1 : "isValue V \<Longrightarrow> eqvt k \<Longrightarrow> V*k = k (psi V)" |
|
231 apply (cases V rule: lt.exhaust) |
|
232 apply simp_all |
|
233 apply (rule_tac x="(name, lt)" and ?'a="name" in obtain_fresh) |
|
234 apply simp |
|
235 done |
|
236 |
|
237 lemma value_eq2 : "isValue V \<Longrightarrow> V^K = K $ (psi V)" |
|
238 apply (cases V rule: lt.exhaust) |
|
239 apply simp_all |
|
240 apply (rule_tac x="(name, lt)" and ?'a="name" in obtain_fresh) |
|
241 apply simp |
|
242 done |
|
243 |
|
244 lemma value_eq3' : "~isValue M \<Longrightarrow> eqvt k \<Longrightarrow> M*k = (M^(Lam n (k (Var n))))" |
|
245 by (cases M rule: lt.exhaust) auto |
|
246 |
|
247 |
|
248 |
|
249 end |
|
250 |
|
251 |
|
252 |
|