equal
deleted
inserted
replaced
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 lemma TODO: "eqvt_at f a \<Longrightarrow> eqvt_at f (p \<bullet> a)" |
|
5 sorry |
3 |
6 |
4 nominal_primrec |
7 nominal_primrec |
5 CPS1 :: "lt \<Rightarrow> (lt \<Rightarrow> lt) \<Rightarrow> lt" ("_*_" [100,100] 100) |
8 CPS1 :: "lt \<Rightarrow> (lt \<Rightarrow> lt) \<Rightarrow> lt" ("_*_" [100,100] 100) |
6 and |
9 and |
7 CPS2 :: "lt \<Rightarrow> lt \<Rightarrow> lt" ("_^_" [100,100] 100) |
10 CPS2 :: "lt \<Rightarrow> lt \<Rightarrow> lt" ("_^_" [100,100] 100) |
98 apply (case_tac "(atom x \<rightleftharpoons> atom xa) \<bullet> c = ca") |
101 apply (case_tac "(atom x \<rightleftharpoons> atom xa) \<bullet> c = ca") |
99 apply simp_all[3] |
102 apply simp_all[3] |
100 apply rule |
103 apply rule |
101 apply (case_tac "c = xa") |
104 apply (case_tac "c = xa") |
102 apply simp_all[2] |
105 apply simp_all[2] |
103 apply (simp add: eqvt_at_def) |
106 apply (rotate_tac 1) |
104 apply clarify |
107 apply (drule TODO) |
105 apply (smt flip_def permute_flip_at permute_swap_cancel swap_fresh_fresh) |
108 apply (drule_tac x="(atom ca \<rightleftharpoons> atom x)" in spec) |
106 apply (simp add: eqvt_at_def) |
109 apply (simp add: swap_fresh_fresh) |
107 apply clarify |
110 apply (simp add: eqvt_at_def swap_fresh_fresh) |
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) |
111 apply (thin_tac "eqvt_at CPS1_CPS2_sumC (Inr (M, c~))") |
|
112 apply (simp add: eqvt_at_def) |
|
113 apply (drule_tac x="(atom ca \<rightleftharpoons> atom c)" in spec) |
|
114 apply simp |
|
115 apply (metis (no_types) atom_eq_iff fresh_permute_iff permute_swap_cancel swap_atom_simps(3) swap_fresh_fresh) |
109 apply (case_tac "c = xa") |
116 apply (case_tac "c = xa") |
110 apply simp |
117 apply simp |
111 apply (subgoal_tac "((ca \<leftrightarrow> x) \<bullet> (atom x)) \<sharp> (ca \<leftrightarrow> x) \<bullet> CPS1_CPS2_sumC (Inr (Ma, ca~))") |
118 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) |
119 apply (simp add: atom_eqvt eqvt_at_def) |
113 apply (simp add: flip_fresh_fresh) |
120 apply (simp add: flip_fresh_fresh) |
158 apply (drule sym) |
165 apply (drule sym) |
159 apply (simp only:) |
166 apply (simp only:) |
160 apply (simp add: Abs_fresh_iff lt.fresh) |
167 apply (simp add: Abs_fresh_iff lt.fresh) |
161 apply clarify |
168 apply clarify |
162 apply (erule fresh_eqvt_at) |
169 apply (erule fresh_eqvt_at) |
163 apply (simp add: supp_Inr finite_supp) |
170 apply (simp add: supp_Inr finite_supp) (* TODO put sum of fs into fs typeclass *) |
164 apply (simp add: fresh_Inr fresh_Pair lt.fresh fresh_at_base) |
171 apply (simp add: fresh_Inr fresh_Pair lt.fresh fresh_at_base) |
165 apply (drule sym) |
172 apply (drule sym) |
166 apply (drule sym) |
173 apply (drule sym) |
167 apply (drule sym) |
174 apply (drule sym) |
168 apply (simp only:) |
175 apply (simp only:) |
179 apply (case_tac "(atom x \<rightleftharpoons> atom xa) \<bullet> c = ca") |
186 apply (case_tac "(atom x \<rightleftharpoons> atom xa) \<bullet> c = ca") |
180 apply simp_all[3] |
187 apply simp_all[3] |
181 apply rule |
188 apply rule |
182 apply (case_tac "c = xa") |
189 apply (case_tac "c = xa") |
183 apply simp_all[2] |
190 apply simp_all[2] |
184 apply (simp add: eqvt_at_def) |
191 apply (rotate_tac 1) |
185 apply clarify |
192 apply (drule TODO) |
186 apply (smt flip_def permute_flip_at permute_swap_cancel swap_fresh_fresh) |
193 apply (drule_tac x="(atom ca \<rightleftharpoons> atom x)" in spec) |
187 apply (simp add: eqvt_at_def) |
194 apply (simp add: swap_fresh_fresh) |
188 apply clarify |
195 apply (simp add: eqvt_at_def swap_fresh_fresh) |
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) |
196 apply (thin_tac "eqvt_at CPS1_CPS2_sumC (Inr (M, c~))") |
|
197 apply (simp add: eqvt_at_def) |
|
198 apply (drule_tac x="(atom ca \<rightleftharpoons> atom c)" in spec) |
|
199 apply simp |
|
200 apply (metis (no_types) atom_eq_iff fresh_permute_iff permute_swap_cancel swap_atom_simps(3) swap_fresh_fresh) |
190 apply (case_tac "c = xa") |
201 apply (case_tac "c = xa") |
191 apply simp |
202 apply simp |
192 apply (subgoal_tac "((ca \<leftrightarrow> x) \<bullet> (atom x)) \<sharp> (ca \<leftrightarrow> x) \<bullet> CPS1_CPS2_sumC (Inr (Ma, ca~))") |
203 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) |
204 apply (simp add: atom_eqvt eqvt_at_def) |
194 apply (simp add: flip_fresh_fresh) |
205 apply (simp add: flip_fresh_fresh) |