equal
deleted
inserted
replaced
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 add: eqvt_def CPS1_CPS2_graph_aux_def) |
17 apply (rule, perm_simp, rule) |
|
18 using [[simproc del: alpha_lst]] |
17 using [[simproc del: alpha_lst]] |
19 apply auto |
18 apply auto |
20 apply (case_tac x) |
19 apply (case_tac x) |
21 apply (case_tac a) |
20 apply (case_tac a) |
22 apply (case_tac "eqvt b") |
21 apply (case_tac "eqvt b") |