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 |
|
6 |
3 |
7 nominal_primrec |
4 nominal_primrec |
8 CPS1 :: "lt \<Rightarrow> (lt \<Rightarrow> lt) \<Rightarrow> lt" ("_*_" [100,100] 100) |
5 CPS1 :: "lt \<Rightarrow> (lt \<Rightarrow> lt) \<Rightarrow> lt" ("_*_" [100,100] 100) |
9 and |
6 and |
10 CPS2 :: "lt \<Rightarrow> lt \<Rightarrow> lt" ("_^_" [100,100] 100) |
7 CPS2 :: "lt \<Rightarrow> lt \<Rightarrow> lt" ("_^_" [100,100] 100) |
102 apply simp_all[3] |
99 apply simp_all[3] |
103 apply rule |
100 apply rule |
104 apply (case_tac "c = xa") |
101 apply (case_tac "c = xa") |
105 apply simp_all[2] |
102 apply simp_all[2] |
106 apply (rotate_tac 1) |
103 apply (rotate_tac 1) |
107 apply (drule TODO) |
104 apply (drule_tac q="(atom ca \<rightleftharpoons> atom x)" in eqvt_at_perm) |
108 apply (drule_tac x="(atom ca \<rightleftharpoons> atom x)" in spec) |
|
109 apply (simp add: swap_fresh_fresh) |
105 apply (simp add: swap_fresh_fresh) |
110 apply (simp add: eqvt_at_def swap_fresh_fresh) |
106 apply (simp add: eqvt_at_def swap_fresh_fresh) |
111 apply (thin_tac "eqvt_at CPS1_CPS2_sumC (Inr (M, c~))") |
107 apply (thin_tac "eqvt_at CPS1_CPS2_sumC (Inr (M, c~))") |
112 apply (simp add: eqvt_at_def) |
108 apply (simp add: eqvt_at_def) |
113 apply (drule_tac x="(atom ca \<rightleftharpoons> atom c)" in spec) |
109 apply (drule_tac x="(atom ca \<rightleftharpoons> atom c)" in spec) |
187 apply simp_all[3] |
183 apply simp_all[3] |
188 apply rule |
184 apply rule |
189 apply (case_tac "c = xa") |
185 apply (case_tac "c = xa") |
190 apply simp_all[2] |
186 apply simp_all[2] |
191 apply (rotate_tac 1) |
187 apply (rotate_tac 1) |
192 apply (drule TODO) |
188 apply (drule_tac q="(atom ca \<rightleftharpoons> atom x)" in eqvt_at_perm) |
193 apply (drule_tac x="(atom ca \<rightleftharpoons> atom x)" in spec) |
|
194 apply (simp add: swap_fresh_fresh) |
189 apply (simp add: swap_fresh_fresh) |
195 apply (simp add: eqvt_at_def swap_fresh_fresh) |
190 apply (simp add: eqvt_at_def swap_fresh_fresh) |
196 apply (thin_tac "eqvt_at CPS1_CPS2_sumC (Inr (M, c~))") |
191 apply (thin_tac "eqvt_at CPS1_CPS2_sumC (Inr (M, c~))") |
197 apply (simp add: eqvt_at_def) |
192 apply (simp add: eqvt_at_def) |
198 apply (drule_tac x="(atom ca \<rightleftharpoons> atom c)" in spec) |
193 apply (drule_tac x="(atom ca \<rightleftharpoons> atom c)" in spec) |