equal
deleted
inserted
replaced
1 header {* CPS transformation of Danvy and Filinski *} |
1 header {* CPS transformation of Danvy and Filinski *} |
2 theory CPS3_DanvyFilinski_FCB2 |
2 theory CPS3_DanvyFilinski_FCB2 |
3 imports Lt |
3 imports Lt |
4 begin |
4 begin |
5 |
5 |
6 nominal_primrec |
6 nominal_function |
7 CPS1 :: "lt \<Rightarrow> (lt \<Rightarrow> lt) \<Rightarrow> lt" ("_*_" [100,100] 100) |
7 CPS1 :: "lt \<Rightarrow> (lt \<Rightarrow> lt) \<Rightarrow> lt" ("_*_" [100,100] 100) |
8 and |
8 and |
9 CPS2 :: "lt \<Rightarrow> lt \<Rightarrow> lt" ("_^_" [100,100] 100) |
9 CPS2 :: "lt \<Rightarrow> lt \<Rightarrow> lt" ("_^_" [100,100] 100) |
10 where |
10 where |
11 "eqvt k \<Longrightarrow> (x~)*k = k (x~)" |
11 "eqvt k \<Longrightarrow> (x~)*k = k (x~)" |