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~)" |
12 | "eqvt k \<Longrightarrow> (M$N)*k = M*(%m. (N*(%n.((m $ n) $ (Lam c (k (c~)))))))" |
12 | "eqvt k \<Longrightarrow> (M $$ N)*k = M*(%m. (N*(%n.((m $$ n) $$ (Lam c (k (c~)))))))" |
13 | "eqvt k \<Longrightarrow> atom c \<sharp> (x, M) \<Longrightarrow> (Lam x M)*k = k (Lam x (Lam c (M^(c~))))" |
13 | "eqvt k \<Longrightarrow> atom c \<sharp> (x, M) \<Longrightarrow> (Lam x M)*k = k (Lam x (Lam c (M^(c~))))" |
14 | "\<not>eqvt k \<Longrightarrow> (CPS1 t k) = t" |
14 | "\<not>eqvt k \<Longrightarrow> (CPS1 t k) = t" |
15 | "(x~)^l = l $ (x~)" |
15 | "(x~)^l = l $$ (x~)" |
16 | "(M$N)^l = M*(%m. (N*(%n.((m $ n) $ l))))" |
16 | "(M $$ N)^l = M*(%m. (N*(%n.((m $$ n) $$ l))))" |
17 | "atom c \<sharp> (x, M) \<Longrightarrow> (Lam x M)^l = l $ (Lam x (Lam c (M^(c~))))" |
17 | "atom c \<sharp> (x, M) \<Longrightarrow> (Lam x M)^l = l $$ (Lam x (Lam c (M^(c~))))" |
18 apply (simp only: eqvt_def CPS1_CPS2_graph_def) |
18 apply (simp only: eqvt_def CPS1_CPS2_graph_def) |
19 apply (rule, perm_simp, rule) |
19 apply (rule, perm_simp, rule) |
20 apply (auto simp only:) |
20 apply (auto simp only:) |
21 apply (case_tac x) |
21 apply (case_tac x) |
22 apply (case_tac a) |
22 apply (case_tac a) |