|
1 header {* CPS transformation of Danvy and Filinski *} |
|
2 theory 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) $ (Abs c (k (c~)))))))" |
|
11 | "eqvt k \<Longrightarrow> atom c \<sharp> (x, M) \<Longrightarrow> (Abs x M)*k = k (Abs x (Abs 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> (Abs x M)^l = l $ (Abs x (Abs 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 apply blast |
|
33 --"-" |
|
34 apply (subgoal_tac "Abs c (ka (c~)) = Abs ca (ka (ca~))") |
|
35 apply (simp only:) |
|
36 apply (simp add: Abs1_eq_iff) |
|
37 apply (case_tac "c=ca") |
|
38 apply simp_all[2] |
|
39 apply rule |
|
40 apply (perm_simp) |
|
41 apply (simp add: eqvt_def) |
|
42 apply (simp add: fresh_def) |
|
43 apply (rule contra_subsetD[OF supp_fun_app]) |
|
44 back |
|
45 apply (simp add: supp_fun_eqvt lt.supp supp_at_base) |
|
46 --"-" |
|
47 apply (rule arg_cong) |
|
48 back |
|
49 apply simp |
|
50 apply (thin_tac "eqvt ka") |
|
51 apply (rule_tac x="(c, ca, x, xa, M, Ma)" and ?'a="name" in obtain_fresh) |
|
52 apply (subgoal_tac "Abs c (CPS1_CPS2_sumC (Inr (M, c~))) = Abs a (CPS1_CPS2_sumC (Inr (M, a~)))") |
|
53 prefer 2 |
|
54 apply (simp add: Abs1_eq_iff') |
|
55 apply (case_tac "c = a") |
|
56 apply simp_all[2] |
|
57 apply rule |
|
58 apply (simp add: eqvt_at_def) |
|
59 apply (simp add: swap_fresh_fresh fresh_Pair_elim) |
|
60 apply (erule fresh_eqvt_at) |
|
61 apply (simp add: supp_Inr finite_supp) |
|
62 apply (simp add: fresh_Inr fresh_Pair lt.fresh fresh_at_base) |
|
63 apply (subgoal_tac "Abs ca (CPS1_CPS2_sumC (Inr (Ma, ca~))) = Abs a (CPS1_CPS2_sumC (Inr (Ma, a~)))") |
|
64 prefer 2 |
|
65 apply (simp add: Abs1_eq_iff') |
|
66 apply (case_tac "ca = a") |
|
67 apply simp_all[2] |
|
68 apply rule |
|
69 apply (simp add: eqvt_at_def) |
|
70 apply (simp add: swap_fresh_fresh fresh_Pair_elim) |
|
71 apply (erule fresh_eqvt_at) |
|
72 apply (simp add: supp_Inr finite_supp) |
|
73 apply (simp add: fresh_Inr fresh_Pair lt.fresh fresh_at_base) |
|
74 apply (simp only: ) |
|
75 apply (erule Abs_lst1_fcb) |
|
76 apply (simp add: Abs_fresh_iff) |
|
77 apply (drule sym) |
|
78 apply (simp only:) |
|
79 apply (simp add: Abs_fresh_iff lt.fresh) |
|
80 apply clarify |
|
81 apply (erule fresh_eqvt_at) |
|
82 apply (simp add: supp_Inr finite_supp) |
|
83 apply (simp add: fresh_Inr fresh_Pair lt.fresh fresh_at_base) |
|
84 apply (drule sym) |
|
85 apply (drule sym) |
|
86 apply (drule sym) |
|
87 apply (simp only:) |
|
88 apply (thin_tac "Abs a (CPS1_CPS2_sumC (Inr (M, a~))) = Abs c (CPS1_CPS2_sumC (Inr (M, c~)))") |
|
89 apply (thin_tac "Abs a (CPS1_CPS2_sumC (Inr (Ma, a~))) = Abs ca (CPS1_CPS2_sumC (Inr (Ma, ca~)))") |
|
90 apply (thin_tac "atom a \<sharp> (c, ca, x, xa, M, Ma)") |
|
91 apply (simp add: fresh_Pair_elim) |
|
92 apply (subst iffD1[OF meta_eq_to_obj_eq[OF eqvt_at_def]]) |
|
93 back |
|
94 back |
|
95 back |
|
96 apply assumption |
|
97 apply (simp add: Abs1_eq_iff' fresh_Pair_elim fresh_at_base swap_fresh_fresh lt.fresh) |
|
98 apply (case_tac "(atom x \<rightleftharpoons> atom xa) \<bullet> c = ca") |
|
99 apply simp_all[3] |
|
100 apply rule |
|
101 apply (case_tac "c = xa") |
|
102 apply simp_all[2] |
|
103 apply (simp add: eqvt_at_def) |
|
104 apply clarify |
|
105 apply (smt flip_def permute_flip_at permute_swap_cancel swap_fresh_fresh) |
|
106 apply (simp add: eqvt_at_def) |
|
107 apply clarify |
|
108 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) |
|
109 apply (case_tac "c = xa") |
|
110 apply simp |
|
111 apply (subgoal_tac "((ca \<leftrightarrow> x) \<bullet> (atom x)) \<sharp> (ca \<leftrightarrow> x) \<bullet> CPS1_CPS2_sumC (Inr (Ma, ca~))") |
|
112 apply (simp add: atom_eqvt eqvt_at_def) |
|
113 apply (simp add: flip_fresh_fresh) |
|
114 apply (subst fresh_permute_iff) |
|
115 apply (erule fresh_eqvt_at) |
|
116 apply (simp add: supp_Inr finite_supp) |
|
117 apply (simp add: fresh_Inr lt.fresh fresh_at_base fresh_Pair) |
|
118 apply simp |
|
119 apply clarify |
|
120 apply (subgoal_tac "atom ca \<sharp> (atom x \<rightleftharpoons> atom xa) \<bullet> CPS1_CPS2_sumC (Inr (M, c~))") |
|
121 apply (simp add: eqvt_at_def) |
|
122 apply (subgoal_tac "(atom x \<rightleftharpoons> atom xa) \<bullet> atom ca \<sharp> CPS1_CPS2_sumC (Inr (M, c~))") |
|
123 apply (metis Nominal2_Base.swap_commute fresh_permute_iff permute_swap_cancel2) |
|
124 apply (erule fresh_eqvt_at) |
|
125 apply (simp add: finite_supp supp_Inr) |
|
126 apply (simp add: fresh_Inr fresh_Pair lt.fresh) |
|
127 apply rule |
|
128 apply (metis Nominal2_Base.swap_commute fresh_permute_iff permute_swap_cancel2) |
|
129 apply (simp add: fresh_def supp_at_base) |
|
130 apply (metis atom_eq_iff permute_swap_cancel2 swap_atom_simps(3)) |
|
131 --"-" |
|
132 apply (rule_tac x="(c, ca, x, xa, M, Ma)" and ?'a="name" in obtain_fresh) |
|
133 apply (subgoal_tac "Abs c (CPS1_CPS2_sumC (Inr (M, c~))) = Abs a (CPS1_CPS2_sumC (Inr (M, a~)))") |
|
134 prefer 2 |
|
135 apply (simp add: Abs1_eq_iff') |
|
136 apply (case_tac "c = a") |
|
137 apply simp_all[2] |
|
138 apply rule |
|
139 apply (simp add: eqvt_at_def) |
|
140 apply (simp add: swap_fresh_fresh fresh_Pair_elim) |
|
141 apply (erule fresh_eqvt_at) |
|
142 apply (simp add: supp_Inr finite_supp) |
|
143 apply (simp add: fresh_Inr fresh_Pair lt.fresh fresh_at_base) |
|
144 apply (subgoal_tac "Abs ca (CPS1_CPS2_sumC (Inr (Ma, ca~))) = Abs a (CPS1_CPS2_sumC (Inr (Ma, a~)))") |
|
145 prefer 2 |
|
146 apply (simp add: Abs1_eq_iff') |
|
147 apply (case_tac "ca = a") |
|
148 apply simp_all[2] |
|
149 apply rule |
|
150 apply (simp add: eqvt_at_def) |
|
151 apply (simp add: swap_fresh_fresh fresh_Pair_elim) |
|
152 apply (erule fresh_eqvt_at) |
|
153 apply (simp add: supp_Inr finite_supp) |
|
154 apply (simp add: fresh_Inr fresh_Pair lt.fresh fresh_at_base) |
|
155 apply (simp only: ) |
|
156 apply (erule Abs_lst1_fcb) |
|
157 apply (simp add: Abs_fresh_iff) |
|
158 apply (drule sym) |
|
159 apply (simp only:) |
|
160 apply (simp add: Abs_fresh_iff lt.fresh) |
|
161 apply clarify |
|
162 apply (erule fresh_eqvt_at) |
|
163 apply (simp add: supp_Inr finite_supp) |
|
164 apply (simp add: fresh_Inr fresh_Pair lt.fresh fresh_at_base) |
|
165 apply (drule sym) |
|
166 apply (drule sym) |
|
167 apply (drule sym) |
|
168 apply (simp only:) |
|
169 apply (thin_tac "Abs a (CPS1_CPS2_sumC (Inr (M, a~))) = Abs c (CPS1_CPS2_sumC (Inr (M, c~)))") |
|
170 apply (thin_tac "Abs a (CPS1_CPS2_sumC (Inr (Ma, a~))) = Abs ca (CPS1_CPS2_sumC (Inr (Ma, ca~)))") |
|
171 apply (thin_tac "atom a \<sharp> (c, ca, x, xa, M, Ma)") |
|
172 apply (simp add: fresh_Pair_elim) |
|
173 apply (subst iffD1[OF meta_eq_to_obj_eq[OF eqvt_at_def]]) |
|
174 back |
|
175 back |
|
176 back |
|
177 apply assumption |
|
178 apply (simp add: Abs1_eq_iff' fresh_Pair_elim fresh_at_base swap_fresh_fresh lt.fresh) |
|
179 apply (case_tac "(atom x \<rightleftharpoons> atom xa) \<bullet> c = ca") |
|
180 apply simp_all[3] |
|
181 apply rule |
|
182 apply (case_tac "c = xa") |
|
183 apply simp_all[2] |
|
184 apply (simp add: eqvt_at_def) |
|
185 apply clarify |
|
186 apply (smt flip_def permute_flip_at permute_swap_cancel swap_fresh_fresh) |
|
187 apply (simp add: eqvt_at_def) |
|
188 apply clarify |
|
189 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) |
|
190 apply (case_tac "c = xa") |
|
191 apply simp |
|
192 apply (subgoal_tac "((ca \<leftrightarrow> x) \<bullet> (atom x)) \<sharp> (ca \<leftrightarrow> x) \<bullet> CPS1_CPS2_sumC (Inr (Ma, ca~))") |
|
193 apply (simp add: atom_eqvt eqvt_at_def) |
|
194 apply (simp add: flip_fresh_fresh) |
|
195 apply (subst fresh_permute_iff) |
|
196 apply (erule fresh_eqvt_at) |
|
197 apply (simp add: supp_Inr finite_supp) |
|
198 apply (simp add: fresh_Inr lt.fresh fresh_at_base fresh_Pair) |
|
199 apply simp |
|
200 apply clarify |
|
201 apply (subgoal_tac "atom ca \<sharp> (atom x \<rightleftharpoons> atom xa) \<bullet> CPS1_CPS2_sumC (Inr (M, c~))") |
|
202 apply (simp add: eqvt_at_def) |
|
203 apply (subgoal_tac "(atom x \<rightleftharpoons> atom xa) \<bullet> atom ca \<sharp> CPS1_CPS2_sumC (Inr (M, c~))") |
|
204 apply (metis Nominal2_Base.swap_commute fresh_permute_iff permute_swap_cancel2) |
|
205 apply (erule fresh_eqvt_at) |
|
206 apply (simp add: finite_supp supp_Inr) |
|
207 apply (simp add: fresh_Inr fresh_Pair lt.fresh) |
|
208 apply rule |
|
209 apply (metis Nominal2_Base.swap_commute fresh_permute_iff permute_swap_cancel2) |
|
210 apply (simp add: fresh_def supp_at_base) |
|
211 apply (metis atom_eq_iff permute_swap_cancel2 swap_atom_simps(3)) |
|
212 done |
|
213 |
|
214 termination |
|
215 by lexicographic_order |
|
216 |
|
217 definition psi:: "lt => lt" |
|
218 where "psi V == V*(\<lambda>x. x)" |
|
219 |
|
220 section {* Simple consequence of CPS *} |
|
221 |
|
222 lemma value_eq1 : "isValue V \<Longrightarrow> eqvt k \<Longrightarrow> V*k = k (psi V)" |
|
223 apply (cases V rule: lt.exhaust) |
|
224 apply (auto simp add: psi_def) |
|
225 apply (subst CPS1.simps) |
|
226 apply (simp add: eqvt_def eqvt_bound eqvt_lambda) |
|
227 apply rule |
|
228 apply (rule_tac x="(name, lt)" and ?'a="name" in obtain_fresh) |
|
229 apply (subst CPS1.simps(3)) |
|
230 apply assumption+ |
|
231 apply (subst CPS1.simps(3)) |
|
232 apply (simp add: eqvt_def eqvt_bound eqvt_lambda) |
|
233 apply assumption |
|
234 apply rule |
|
235 done |
|
236 |
|
237 end |
|
238 |
|
239 |
|
240 |