equal
deleted
inserted
replaced
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 add: eqvt_def CPS1_CPS2_graph_aux_def) |
19 apply (rule, perm_simp, rule) |
|
20 apply (auto simp only:) |
19 apply (auto simp only:) |
21 apply (case_tac x) |
20 apply (case_tac x) |
22 apply (case_tac a) |
21 apply (case_tac a) |
23 apply (case_tac "eqvt b") |
22 apply (case_tac "eqvt b") |
24 apply (rule_tac y="aa" in lt.strong_exhaust) |
23 apply (rule_tac y="aa" in lt.strong_exhaust) |