5 CPS1 :: "lt \<Rightarrow> (lt \<Rightarrow> lt) \<Rightarrow> lt" ("_*_" [100,100] 100) |
5 CPS1 :: "lt \<Rightarrow> (lt \<Rightarrow> lt) \<Rightarrow> lt" ("_*_" [100,100] 100) |
6 and |
6 and |
7 CPS2 :: "lt \<Rightarrow> lt \<Rightarrow> lt" ("_^_" [100,100] 100) |
7 CPS2 :: "lt \<Rightarrow> lt \<Rightarrow> lt" ("_^_" [100,100] 100) |
8 where |
8 where |
9 "eqvt k \<Longrightarrow> (x~)*k = k (x~)" |
9 "eqvt k \<Longrightarrow> (x~)*k = k (x~)" |
10 | "eqvt k \<Longrightarrow> (M$N)*k = M*(%m. (N*(%n.((m $ n) $ (Lam c (k (c~)))))))" |
10 | "eqvt k \<Longrightarrow> (M$$N)*k = M*(%m. (N*(%n.((m $$ n) $$ (Lam c (k (c~)))))))" |
11 | "eqvt k \<Longrightarrow> atom c \<sharp> (x, M) \<Longrightarrow> (Lam x M)*k = k (Lam x (Lam c (M^(c~))))" |
11 | "eqvt k \<Longrightarrow> atom c \<sharp> (x, M) \<Longrightarrow> (Lam x M)*k = k (Lam x (Lam c (M^(c~))))" |
12 | "\<not>eqvt k \<Longrightarrow> (CPS1 t k) = t" |
12 | "\<not>eqvt k \<Longrightarrow> (CPS1 t k) = t" |
13 | "(x~)^l = l $ (x~)" |
13 | "(x~)^l = l $$ (x~)" |
14 | "(M$N)^l = M*(%m. (N*(%n.((m $ n) $ l))))" |
14 | "(M$$N)^l = M*(%m. (N*(%n.((m $$ n) $$ l))))" |
15 | "atom c \<sharp> (x, M) \<Longrightarrow> (Lam x M)^l = l $ (Lam x (Lam c (M^(c~))))" |
15 | "atom c \<sharp> (x, M) \<Longrightarrow> (Lam x M)^l = l $$ (Lam x (Lam c (M^(c~))))" |
16 apply (simp only: eqvt_def CPS1_CPS2_graph_def) |
16 apply (simp only: eqvt_def CPS1_CPS2_graph_def) |
17 apply (rule, perm_simp, rule) |
17 apply (rule, perm_simp, rule) |
18 apply auto |
18 apply auto |
19 apply (case_tac x) |
19 apply (case_tac x) |
20 apply (case_tac a) |
20 apply (case_tac a) |