1 header {* CPS conversion *} |
|
2 theory CPS1_Plotkin |
|
3 imports Lt |
|
4 begin |
|
5 |
|
6 nominal_primrec |
|
7 CPS :: "lt \<Rightarrow> lt" ("_*" [250] 250) |
|
8 where |
|
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*))" |
|
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~)))" |
|
13 unfolding eqvt_def CPS_graph_def |
|
14 apply (rule, perm_simp, rule, rule) |
|
15 apply (simp_all add: fresh_Pair_elim) |
|
16 apply (rule_tac y="x" in lt.exhaust) |
|
17 apply (auto) |
|
18 apply (rule_tac x="name" and ?'a="name" in obtain_fresh) |
|
19 apply (simp_all add: fresh_at_base)[3] |
|
20 apply (rule_tac x="(name, lt)" and ?'a="name" in obtain_fresh) |
|
21 apply (simp add: fresh_Pair_elim fresh_at_base)[2] |
|
22 apply (rule_tac x="(lt1, lt2)" and ?'a="name" in obtain_fresh) |
|
23 apply (rule_tac x="(lt2, a)" and ?'a="name" in obtain_fresh) |
|
24 apply (rule_tac x="(a, aa)" and ?'a="name" in obtain_fresh) |
|
25 apply (simp add: fresh_Pair_elim fresh_at_base) |
|
26 apply (simp add: Abs1_eq_iff lt.fresh fresh_at_base) |
|
27 --"-" |
|
28 apply(rule_tac s="[[atom ka]]lst. ka~ $ Lam x (CPS_sumC M)" in trans) |
|
29 apply (case_tac "k = ka") |
|
30 apply simp |
|
31 apply(simp (no_asm) add: Abs1_eq_iff del:eqvts) |
|
32 apply (simp del: eqvts add: lt.fresh fresh_at_base) |
|
33 apply (simp only: lt.perm_simps(1) lt.perm_simps(3) flip_def[symmetric] lt.eq_iff(3)) |
|
34 apply (subst flip_at_base_simps(2)) |
|
35 apply simp |
|
36 apply (intro conjI refl) |
|
37 apply (rule flip_fresh_fresh[symmetric]) |
|
38 apply (simp_all add: lt.fresh) |
|
39 apply (metis fresh_eqvt_at lt.fsupp) |
|
40 apply (case_tac "ka = x") |
|
41 apply simp_all[2] |
|
42 apply (metis Abs_fresh_iff(3) atom_eq_iff finite_set fresh_Cons fresh_Nil fresh_atom fresh_eqvt_at fresh_finite_atom_set fresh_set lt.fsupp) |
|
43 apply (metis Abs_fresh_iff(3) atom_eq_iff finite_set fresh_Cons fresh_Nil fresh_atom fresh_eqvt_at fresh_finite_atom_set fresh_set lt.fsupp) |
|
44 --"-" |
|
45 apply (simp add: Abs1_eq(3)) |
|
46 apply (erule Abs_lst1_fcb2) |
|
47 apply (simp_all add: Abs_fresh_iff fresh_Nil fresh_star_def eqvt_at_def)[4] |
|
48 --"-" |
|
49 apply (rename_tac k' M N m' n') |
|
50 apply (subgoal_tac "atom k \<sharp> CPS_sumC M \<and> atom k' \<sharp> CPS_sumC M \<and> atom k \<sharp> CPS_sumC N \<and> atom k' \<sharp> CPS_sumC N \<and> |
|
51 atom m \<sharp> CPS_sumC N \<and> atom m' \<sharp> CPS_sumC N") |
|
52 prefer 2 |
|
53 apply (intro conjI) |
|
54 apply (erule fresh_eqvt_at, simp add: finite_supp, assumption)+ |
|
55 apply clarify |
|
56 apply (case_tac "k = k'", case_tac [!] "m' = k",case_tac [!]"m = k'",case_tac[!] "m = m'") |
|
57 apply (simp_all add: Abs1_eq_iff lt.fresh flip_def[symmetric] fresh_at_base flip_fresh_fresh permute_eq_iff) |
|
58 by (metis flip_at_base_simps(3) flip_at_simps(2) flip_commute permute_flip_at)+ |
|
59 |
|
60 termination (eqvt) by lexicographic_order |
|
61 |
|
62 lemmas [simp] = fresh_Pair_elim CPS.simps(2,3)[simplified fresh_Pair_elim] |
|
63 |
|
64 lemma [simp]: "supp (M*) = supp M" |
|
65 by (induct rule: CPS.induct, simp_all add: lt.supp supp_at_base fresh_at_base fresh_def supp_Pair) |
|
66 (simp_all only: atom_eq_iff[symmetric], blast+) |
|
67 |
|
68 lemma [simp]: "x \<sharp> M* = x \<sharp> M" |
|
69 unfolding fresh_def by simp |
|
70 |
|
71 nominal_primrec |
|
72 convert:: "lt => lt" ("_+" [250] 250) |
|
73 where |
|
74 "(Var x)+ = Var x" |
|
75 | "(Lam x M)+ = Lam x (M*)" |
|
76 | "(M $ N)+ = M $ N" |
|
77 unfolding convert_graph_def eqvt_def |
|
78 apply (rule, perm_simp, rule, rule) |
|
79 apply (erule lt.exhaust) |
|
80 apply (simp_all) |
|
81 apply blast |
|
82 apply (simp add: Abs1_eq_iff CPS.eqvt) |
|
83 by blast |
|
84 |
|
85 termination (eqvt) |
|
86 by (relation "measure size") (simp_all) |
|
87 |
|
88 lemma convert_supp[simp]: |
|
89 shows "supp (M+) = supp M" |
|
90 by (induct M rule: lt.induct, simp_all add: lt.supp) |
|
91 |
|
92 lemma convert_fresh[simp]: |
|
93 shows "x \<sharp> (M+) = x \<sharp> M" |
|
94 unfolding fresh_def by simp |
|
95 |
|
96 lemma [simp]: |
|
97 shows "isValue (p \<bullet> (M::lt)) = isValue M" |
|
98 by (nominal_induct M rule: lt.strong_induct) auto |
|
99 |
|
100 nominal_primrec |
|
101 Kapply :: "lt \<Rightarrow> lt \<Rightarrow> lt" (infixl ";" 100) |
|
102 where |
|
103 "Kapply (Lam x M) K = K $ (Lam x M)+" |
|
104 | "Kapply (Var x) K = K $ Var x" |
|
105 | "isValue M \<Longrightarrow> isValue N \<Longrightarrow> Kapply (M $ N) K = M+ $ N+ $ K" |
|
106 | "isValue M \<Longrightarrow> \<not>isValue N \<Longrightarrow> atom n \<sharp> M \<Longrightarrow> atom n \<sharp> K \<Longrightarrow> |
|
107 Kapply (M $ N) K = N; (Lam n (M+ $ Var n $ K))" |
|
108 | "\<not>isValue M \<Longrightarrow> atom m \<sharp> N \<Longrightarrow> atom m \<sharp> K \<Longrightarrow> atom n \<sharp> m \<Longrightarrow> atom n \<sharp> K \<Longrightarrow> |
|
109 Kapply (M $ N) K = M; (Lam m (N* $ (Lam n (Var m $ Var n $ K))))" |
|
110 unfolding Kapply_graph_def eqvt_def |
|
111 apply (rule, perm_simp, rule, rule) |
|
112 apply (simp_all) |
|
113 apply (case_tac x) |
|
114 apply (rule_tac y="a" in lt.exhaust) |
|
115 apply (auto) |
|
116 apply (case_tac "isValue lt1") |
|
117 apply (case_tac "isValue lt2") |
|
118 apply (auto)[1] |
|
119 apply (rule_tac x="(lt1, ba)" and ?'a="name" in obtain_fresh) |
|
120 apply (simp add: fresh_Pair_elim fresh_at_base) |
|
121 apply (rule_tac x="(lt2, ba)" and ?'a="name" in obtain_fresh) |
|
122 apply (rule_tac x="(a, ba)" and ?'a="name" in obtain_fresh) |
|
123 apply (simp add: fresh_Pair_elim fresh_at_base) |
|
124 apply (auto simp add: Abs1_eq_iff eqvts)[1] |
|
125 apply (rename_tac M N u K) |
|
126 apply (subgoal_tac "Lam n (M+ $ n~ $ K) = Lam u (M+ $ u~ $ K)") |
|
127 apply (simp only:) |
|
128 apply (auto simp add: Abs1_eq_iff flip_def[symmetric] lt.fresh fresh_at_base flip_fresh_fresh[symmetric])[1] |
|
129 apply (subgoal_tac "Lam m (Na* $ Lam n (m~ $ n~ $ Ka)) = Lam ma (Na* $ Lam na (ma~ $ na~ $ Ka))") |
|
130 apply (simp only:) |
|
131 apply (simp add: Abs1_eq_iff flip_def[symmetric] lt.fresh fresh_at_base) |
|
132 apply (subgoal_tac "Ka = (n \<leftrightarrow> na) \<bullet> Ka") |
|
133 apply (subgoal_tac "Ka = (m \<leftrightarrow> ma) \<bullet> Ka") |
|
134 apply (subgoal_tac "Ka = (n \<leftrightarrow> (m \<leftrightarrow> ma) \<bullet> na) \<bullet> Ka") |
|
135 apply (case_tac "m = ma") |
|
136 apply simp_all |
|
137 apply rule |
|
138 apply (auto simp add: flip_fresh_fresh[symmetric]) |
|
139 apply (metis flip_at_base_simps(3) flip_fresh_fresh permute_flip_at)+ |
|
140 done |
|
141 |
|
142 termination (eqvt) |
|
143 by (relation "measure (\<lambda>(t, _). size t)") (simp_all) |
|
144 |
|
145 section{* lemma related to Kapply *} |
|
146 |
|
147 lemma [simp]: "isValue V \<Longrightarrow> V; K = K $ (V+)" |
|
148 by (nominal_induct V rule: lt.strong_induct) auto |
|
149 |
|
150 section{* lemma related to CPS conversion *} |
|
151 |
|
152 lemma value_CPS: |
|
153 assumes "isValue V" |
|
154 and "atom a \<sharp> V" |
|
155 shows "V* = Lam a (a~ $ V+)" |
|
156 using assms |
|
157 proof (nominal_induct V avoiding: a rule: lt.strong_induct, simp_all add: lt.fresh) |
|
158 fix name :: name and lt aa |
|
159 assume a: "atom name \<sharp> aa" "\<And>b. \<lbrakk>isValue lt; atom b \<sharp> lt\<rbrakk> \<Longrightarrow> lt* = Lam b (b~ $ lt+)" |
|
160 "atom aa \<sharp> lt \<or> aa = name" |
|
161 obtain ab :: name where b: "atom ab \<sharp> (name, lt, a)" using obtain_fresh by blast |
|
162 show "Lam name lt* = Lam aa (aa~ $ Lam name (lt*))" using a b |
|
163 by (simp add: Abs1_eq_iff fresh_at_base lt.fresh) |
|
164 qed |
|
165 |
|
166 section{* first lemma CPS subst *} |
|
167 |
|
168 lemma CPS_subst_fv: |
|
169 assumes *:"isValue V" |
|
170 shows "((M[x ::= V])* = (M*)[x ::= V+])" |
|
171 using * proof (nominal_induct M avoiding: V x rule: lt.strong_induct) |
|
172 case (Var name) |
|
173 assume *: "isValue V" |
|
174 obtain a :: name where a: "atom a \<sharp> (x, name, V)" using obtain_fresh by blast |
|
175 show "((name~)[x ::= V])* = (name~)*[x ::= V+]" using a |
|
176 by (simp add: fresh_at_base * value_CPS) |
|
177 next |
|
178 case (Lam name lt V x) |
|
179 assume *: "atom name \<sharp> V" "atom name \<sharp> x" "\<And>b ba. isValue b \<Longrightarrow> (lt[ba ::= b])* = lt*[ba ::= b+]" |
|
180 "isValue V" |
|
181 obtain a :: name where a: "atom a \<sharp> (name, lt, lt[x ::= V], x, V)" using obtain_fresh by blast |
|
182 show "(Lam name lt[x ::= V])* = Lam name lt*[x ::= V+]" using * a |
|
183 by (simp add: fresh_at_base) |
|
184 next |
|
185 case (App lt1 lt2 V x) |
|
186 assume *: "\<And>b ba. isValue b \<Longrightarrow> (lt1[ba ::= b])* = lt1*[ba ::= b+]" "\<And>b ba. isValue b \<Longrightarrow> (lt2[ba ::= b])* = lt2*[ba ::= b+]" |
|
187 "isValue V" |
|
188 obtain a :: name where a: "atom a \<sharp> (lt1[x ::= V], lt1, lt2[x ::= V], lt2, V, x)" using obtain_fresh by blast |
|
189 obtain b :: name where b: "atom b \<sharp> (lt2[x ::= V], lt2, a, V, x)" using obtain_fresh by blast |
|
190 obtain c :: name where c: "atom c \<sharp> (a, b, V, x)" using obtain_fresh by blast |
|
191 show "((lt1 $ lt2)[x ::= V])* = (lt1 $ lt2)*[x ::= V+]" using * a b c |
|
192 by (simp add: fresh_at_base) |
|
193 qed |
|
194 |
|
195 lemma [simp]: "isValue V \<Longrightarrow> isValue (V+)" |
|
196 by (nominal_induct V rule: lt.strong_induct, auto) |
|
197 |
|
198 lemma CPS_eval_Kapply: |
|
199 assumes a: "isValue K" |
|
200 shows "(M* $ K) \<longrightarrow>\<^isub>\<beta>\<^sup>* (M ; K)" |
|
201 using a |
|
202 proof (nominal_induct M avoiding: K rule: lt.strong_induct, simp_all) |
|
203 case (Var name K) |
|
204 assume *: "isValue K" |
|
205 obtain a :: name where a: "atom a \<sharp> (name, K)" using obtain_fresh by blast |
|
206 show "(name~)* $ K \<longrightarrow>\<^isub>\<beta>\<^sup>* K $ name~" using * a |
|
207 by simp (rule evbeta', simp_all add: fresh_at_base) |
|
208 next |
|
209 fix name :: name and lt K |
|
210 assume *: "atom name \<sharp> K" "\<And>b. isValue b \<Longrightarrow> lt* $ b \<longrightarrow>\<^isub>\<beta>\<^sup>* lt ; b" "isValue K" |
|
211 obtain a :: name where a: "atom a \<sharp> (name, K, lt)" using obtain_fresh by blast |
|
212 then have b: "atom name \<sharp> a" using fresh_PairD(1) fresh_at_base atom_eq_iff by metis |
|
213 show "Lam name lt* $ K \<longrightarrow>\<^isub>\<beta>\<^sup>* K $ Lam name (lt*)" using * a b |
|
214 by simp (rule evbeta', simp_all) |
|
215 next |
|
216 fix lt1 lt2 K |
|
217 assume *: "\<And>b. isValue b \<Longrightarrow> lt1* $ b \<longrightarrow>\<^isub>\<beta>\<^sup>* lt1 ; b" "\<And>b. isValue b \<Longrightarrow> lt2* $ b \<longrightarrow>\<^isub>\<beta>\<^sup>* lt2 ; b" "isValue K" |
|
218 obtain a :: name where a: "atom a \<sharp> (lt1, lt2, K)" using obtain_fresh by blast |
|
219 obtain b :: name where b: "atom b \<sharp> (lt1, lt2, K, a)" using obtain_fresh by blast |
|
220 obtain c :: name where c: "atom c \<sharp> (lt1, lt2, K, a, b)" using obtain_fresh by blast |
|
221 have d: "atom a \<sharp> lt1" "atom a \<sharp> lt2" "atom a \<sharp> K" "atom b \<sharp> lt1" "atom b \<sharp> lt2" "atom b \<sharp> K" "atom b \<sharp> a" |
|
222 "atom c \<sharp> lt1" "atom c \<sharp> lt2" "atom c \<sharp> K" "atom c \<sharp> a" "atom c \<sharp> b" using fresh_Pair a b c by simp_all |
|
223 have "(lt1 $ lt2)* $ K \<longrightarrow>\<^isub>\<beta>\<^sup>* lt1* $ Lam b (lt2* $ Lam c (b~ $ c~ $ K))" using * d |
|
224 by (simp add: fresh_at_base) (rule evbeta', simp_all add: fresh_at_base) |
|
225 also have "... \<longrightarrow>\<^isub>\<beta>\<^sup>* lt1 $ lt2 ; K" proof (cases "isValue lt1") |
|
226 assume e: "isValue lt1" |
|
227 have "lt1* $ Lam b (lt2* $ Lam c (b~ $ c~ $ K)) \<longrightarrow>\<^isub>\<beta>\<^sup>* Lam b (lt2* $ Lam c (b~ $ c~ $ K)) $ lt1+" |
|
228 using * d e by simp |
|
229 also have "... \<longrightarrow>\<^isub>\<beta>\<^sup>* lt2* $ Lam c (lt1+ $ c~ $ K)" |
|
230 by (rule evbeta', simp_all add: * d e, metis d(12) fresh_at_base) |
|
231 also have "... \<longrightarrow>\<^isub>\<beta>\<^sup>* lt1 $ lt2 ; K" proof (cases "isValue lt2") |
|
232 assume f: "isValue lt2" |
|
233 have "lt2* $ Lam c (lt1+ $ c~ $ K) \<longrightarrow>\<^isub>\<beta>\<^sup>* Lam c (lt1+ $ c~ $ K) $ lt2+" using * d e f by simp |
|
234 also have "... \<longrightarrow>\<^isub>\<beta>\<^sup>* lt1+ $ lt2+ $ K" |
|
235 by (rule evbeta', simp_all add: d e f) |
|
236 finally show ?thesis using * d e f by simp |
|
237 next |
|
238 assume f: "\<not> isValue lt2" |
|
239 have "lt2* $ Lam c (lt1+ $ c~ $ K) \<longrightarrow>\<^isub>\<beta>\<^sup>* lt2 ; Lam c (lt1+ $ c~ $ K)" using * d e f by simp |
|
240 also have "... \<longrightarrow>\<^isub>\<beta>\<^sup>* lt2 ; Lam a (lt1+ $ a~ $ K)" using Kapply.simps(4) d e evs1 f by metis |
|
241 finally show ?thesis using * d e f by simp |
|
242 qed |
|
243 finally show ?thesis . |
|
244 qed (metis Kapply.simps(5) isValue.simps(2) * d) |
|
245 finally show "(lt1 $ lt2)* $ K \<longrightarrow>\<^isub>\<beta>\<^sup>* lt1 $ lt2 ; K" . |
|
246 qed |
|
247 |
|
248 lemma Kapply_eval: |
|
249 assumes a: "M \<longrightarrow>\<^isub>\<beta> N" "isValue K" |
|
250 shows "(M; K) \<longrightarrow>\<^isub>\<beta>\<^sup>* (N; K)" |
|
251 using assms |
|
252 proof (induct arbitrary: K rule: eval.induct) |
|
253 case (evbeta x V M) |
|
254 fix K |
|
255 assume a: "isValue K" "isValue V" "atom x \<sharp> V" |
|
256 have "Lam x (M*) $ V+ $ K \<longrightarrow>\<^isub>\<beta>\<^sup>* (((M*)[x ::= V+]) $ K)" |
|
257 by (rule evs2,rule ev2,rule Lt.evbeta) (simp_all add: fresh_def a[simplified fresh_def] evs1) |
|
258 also have "... = ((M[x ::= V])* $ K)" by (simp add: CPS_subst_fv a) |
|
259 also have "... \<longrightarrow>\<^isub>\<beta>\<^sup>* ((M[x ::= V]) ; K)" by (rule CPS_eval_Kapply, simp_all add: a) |
|
260 finally show "(Lam x M $ V ; K) \<longrightarrow>\<^isub>\<beta>\<^sup>* ((M[x ::= V]) ; K)" using a by simp |
|
261 next |
|
262 case (ev1 V M N) |
|
263 fix V M N K |
|
264 assume a: "isValue V" "M \<longrightarrow>\<^isub>\<beta> N" "\<And>K. isValue K \<Longrightarrow> M ; K \<longrightarrow>\<^isub>\<beta>\<^sup>* N ; K" "isValue K" |
|
265 obtain a :: name where b: "atom a \<sharp> (V, K, M, N)" using obtain_fresh by blast |
|
266 show "V $ M ; K \<longrightarrow>\<^isub>\<beta>\<^sup>* V $ N ; K" proof (cases "isValue N") |
|
267 assume "\<not> isValue N" |
|
268 then show "V $ M ; K \<longrightarrow>\<^isub>\<beta>\<^sup>* V $ N ; K" using a b by simp |
|
269 next |
|
270 assume n: "isValue N" |
|
271 have c: "M; Lam a (V+ $ a~ $ K) \<longrightarrow>\<^isub>\<beta>\<^sup>* Lam a (V+ $ a~ $ K) $ N+" using a b by (simp add: n) |
|
272 also have d: "... \<longrightarrow>\<^isub>\<beta>\<^sup>* V+ $ N+ $ K" by (rule evbeta') (simp_all add: a b n) |
|
273 finally show "V $ M ; K \<longrightarrow>\<^isub>\<beta>\<^sup>* V $ N ; K" using a b by (simp add: n) |
|
274 qed |
|
275 next |
|
276 case (ev2 M M' N) |
|
277 assume *: "M \<longrightarrow>\<^isub>\<beta> M'" "\<And>K. isValue K \<Longrightarrow> M ; K \<longrightarrow>\<^isub>\<beta>\<^sup>* M' ; K" "isValue K" |
|
278 obtain a :: name where a: "atom a \<sharp> (K, M, N, M')" using obtain_fresh by blast |
|
279 obtain b :: name where b: "atom b \<sharp> (a, K, M, N, M', N+)" using obtain_fresh by blast |
|
280 have d: "atom a \<sharp> K" "atom a \<sharp> M" "atom a \<sharp> N" "atom a \<sharp> M'" "atom b \<sharp> a" "atom b \<sharp> K" |
|
281 "atom b \<sharp> M" "atom b \<sharp> N" "atom b \<sharp> M'" using a b fresh_Pair by simp_all |
|
282 have "M $ N ; K \<longrightarrow>\<^isub>\<beta>\<^sup>* M' ; Lam a (N* $ Lam b (a~ $ b~ $ K))" using * d by simp |
|
283 also have "... \<longrightarrow>\<^isub>\<beta>\<^sup>* M' $ N ; K" proof (cases "isValue M'") |
|
284 assume "\<not> isValue M'" |
|
285 then show ?thesis using * d by (simp_all add: evs1) |
|
286 next |
|
287 assume e: "isValue M'" |
|
288 then have "M' ; Lam a (N* $ Lam b (a~ $ b~ $ K)) = Lam a (N* $ Lam b (a~ $ b~ $ K)) $ M'+" by simp |
|
289 also have "... \<longrightarrow>\<^isub>\<beta>\<^sup>* (N* $ Lam b (a~ $ b~ $ K))[a ::= M'+]" |
|
290 by (rule evbeta') (simp_all add: fresh_at_base e d) |
|
291 also have "... = N* $ Lam b (M'+ $ b~ $ K)" using * d by (simp add: fresh_at_base) |
|
292 also have "... \<longrightarrow>\<^isub>\<beta>\<^sup>* M' $ N ; K" proof (cases "isValue N") |
|
293 assume f: "isValue N" |
|
294 have "N* $ Lam b (M'+ $ b~ $ K) \<longrightarrow>\<^isub>\<beta>\<^sup>* Lam b (M'+ $ b~ $ K) $ N+" |
|
295 by (rule eval_trans, rule CPS_eval_Kapply) (simp_all add: d e f * evs1) |
|
296 also have "... \<longrightarrow>\<^isub>\<beta>\<^sup>* M' $ N ; K" by (rule evbeta') (simp_all add: d e f evs1) |
|
297 finally show ?thesis . |
|
298 next |
|
299 assume "\<not> isValue N" |
|
300 then show ?thesis using d e |
|
301 by (metis CPS_eval_Kapply Kapply.simps(4) isValue.simps(2)) |
|
302 qed |
|
303 finally show ?thesis . |
|
304 qed |
|
305 finally show ?case . |
|
306 qed |
|
307 |
|
308 lemma Kapply_eval_rtrancl: |
|
309 assumes H: "M \<longrightarrow>\<^isub>\<beta>\<^sup>* N" and "isValue K" |
|
310 shows "(M;K) \<longrightarrow>\<^isub>\<beta>\<^sup>* (N;K)" |
|
311 using H |
|
312 by (induct) (metis Kapply_eval assms(2) eval_trans evs1)+ |
|
313 |
|
314 lemma |
|
315 assumes "isValue V" "M \<longrightarrow>\<^isub>\<beta>\<^sup>* V" |
|
316 shows "M* $ (Lam x (x~)) \<longrightarrow>\<^isub>\<beta>\<^sup>* V+" |
|
317 proof- |
|
318 obtain y::name where *: "atom y \<sharp> V" using obtain_fresh by blast |
|
319 have e: "Lam x (x~) = Lam y (y~)" |
|
320 by (simp add: Abs1_eq_iff lt.fresh fresh_at_base) |
|
321 have "M* $ Lam x (x~) \<longrightarrow>\<^isub>\<beta>\<^sup>* M ; Lam x (x~)" |
|
322 by(rule CPS_eval_Kapply,simp_all add: assms) |
|
323 also have "... \<longrightarrow>\<^isub>\<beta>\<^sup>* (V ; Lam x (x~))" by (rule Kapply_eval_rtrancl, simp_all add: assms) |
|
324 also have "... = V ; Lam y (y~)" using e by (simp only:) |
|
325 also have "... \<longrightarrow>\<^isub>\<beta>\<^sup>* (V+)" by (simp add: assms, rule evbeta') (simp_all add: assms *) |
|
326 finally show "M* $ (Lam x (x~)) \<longrightarrow>\<^isub>\<beta>\<^sup>* (V+)" . |
|
327 qed |
|
328 |
|
329 end |
|
330 |
|
331 |
|
332 |
|