equal
deleted
inserted
replaced
8 where |
8 where |
9 "atom k \<sharp> x \<Longrightarrow> (x~)* = (Lam k ((k~) $$ (x~)))" |
9 "atom k \<sharp> x \<Longrightarrow> (x~)* = (Lam k ((k~) $$ (x~)))" |
10 | "atom k \<sharp> (x, M) \<Longrightarrow> (Lam x M)* = Lam k (k~ $$ Lam x (M*))" |
10 | "atom k \<sharp> (x, M) \<Longrightarrow> (Lam x M)* = Lam k (k~ $$ Lam x (M*))" |
11 | "atom k \<sharp> (M, N) \<Longrightarrow> atom m \<sharp> (N, k) \<Longrightarrow> atom n \<sharp> (k, m) \<Longrightarrow> |
11 | "atom k \<sharp> (M, N) \<Longrightarrow> atom m \<sharp> (N, k) \<Longrightarrow> atom n \<sharp> (k, m) \<Longrightarrow> |
12 (M $$ N)* = Lam k (M* $$ Lam m (N* $$ Lam n (m~ $$ n~ $$ k~)))" |
12 (M $$ N)* = Lam k (M* $$ Lam m (N* $$ Lam n (m~ $$ n~ $$ k~)))" |
13 unfolding eqvt_def CPS_graph_def |
13 unfolding eqvt_def CPS_graph_aux_def |
14 apply (rule, perm_simp, rule, rule) |
14 apply (simp) |
15 using [[simproc del: alpha_lst]] |
15 using [[simproc del: alpha_lst]] |
16 apply (simp_all add: fresh_Pair_elim) |
16 apply (simp_all add: fresh_Pair_elim) |
17 apply (rule_tac y="x" in lt.exhaust) |
17 apply (rule_tac y="x" in lt.exhaust) |
18 apply (auto)[3] |
18 apply (auto)[3] |
19 apply (rule_tac x="name" and ?'a="name" in obtain_fresh) |
19 apply (rule_tac x="name" and ?'a="name" in obtain_fresh) |
78 convert:: "lt => lt" ("_+" [250] 250) |
78 convert:: "lt => lt" ("_+" [250] 250) |
79 where |
79 where |
80 "(Var x)+ = Var x" |
80 "(Var x)+ = Var x" |
81 | "(Lam x M)+ = Lam x (M*)" |
81 | "(Lam x M)+ = Lam x (M*)" |
82 | "(M $$ N)+ = M $$ N" |
82 | "(M $$ N)+ = M $$ N" |
83 unfolding convert_graph_def eqvt_def |
83 unfolding convert_graph_aux_def eqvt_def |
84 apply (rule, perm_simp, rule, rule) |
84 apply (simp) |
|
85 apply(rule TrueI) |
85 apply (erule lt.exhaust) |
86 apply (erule lt.exhaust) |
86 using [[simproc del: alpha_lst]] |
87 using [[simproc del: alpha_lst]] |
87 apply (simp_all) |
88 apply (simp_all) |
88 apply blast |
89 apply blast |
89 apply (simp add: Abs1_eq_iff CPS.eqvt) |
90 apply (simp add: Abs1_eq_iff CPS.eqvt) |
112 | "isValue M \<Longrightarrow> isValue N \<Longrightarrow> Kapply (M $$ N) K = M+ $$ N+ $$ K" |
113 | "isValue M \<Longrightarrow> isValue N \<Longrightarrow> Kapply (M $$ N) K = M+ $$ N+ $$ K" |
113 | "isValue M \<Longrightarrow> \<not>isValue N \<Longrightarrow> atom n \<sharp> M \<Longrightarrow> atom n \<sharp> K \<Longrightarrow> |
114 | "isValue M \<Longrightarrow> \<not>isValue N \<Longrightarrow> atom n \<sharp> M \<Longrightarrow> atom n \<sharp> K \<Longrightarrow> |
114 Kapply (M $$ N) K = N; (Lam n (M+ $$ Var n $$ K))" |
115 Kapply (M $$ N) K = N; (Lam n (M+ $$ Var n $$ K))" |
115 | "\<not>isValue M \<Longrightarrow> atom m \<sharp> N \<Longrightarrow> atom m \<sharp> K \<Longrightarrow> atom n \<sharp> m \<Longrightarrow> atom n \<sharp> K \<Longrightarrow> |
116 | "\<not>isValue M \<Longrightarrow> atom m \<sharp> N \<Longrightarrow> atom m \<sharp> K \<Longrightarrow> atom n \<sharp> m \<Longrightarrow> atom n \<sharp> K \<Longrightarrow> |
116 Kapply (M $$ N) K = M; (Lam m (N* $$ (Lam n (Var m $$ Var n $$ K))))" |
117 Kapply (M $$ N) K = M; (Lam m (N* $$ (Lam n (Var m $$ Var n $$ K))))" |
117 unfolding Kapply_graph_def eqvt_def |
118 unfolding Kapply_graph_aux_def eqvt_def |
118 apply (rule, perm_simp, rule, rule) |
119 apply (simp) |
119 using [[simproc del: alpha_lst]] |
120 using [[simproc del: alpha_lst]] |
120 apply (simp_all) |
121 apply (simp_all) |
121 apply (case_tac x) |
122 apply (case_tac x) |
122 apply (rule_tac y="a" in lt.exhaust) |
123 apply (rule_tac y="a" in lt.exhaust) |
123 apply (auto) |
124 apply (auto) |