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