1 header {* CPS conversion *} |
1 header {* CPS conversion *} |
2 theory CPS1_Plotkin |
2 theory CPS1_Plotkin |
3 imports Lt |
3 imports Lt |
4 begin |
4 begin |
5 |
5 |
6 lemma Abs_lst_fcb2: |
|
7 fixes as bs :: "atom list" |
|
8 and x y :: "'b :: fs" |
|
9 and c::"'c::fs" |
|
10 assumes eq: "[as]lst. x = [bs]lst. y" |
|
11 and fcb1: "(set as) \<sharp>* c \<Longrightarrow> (set as) \<sharp>* f as x c" |
|
12 and fresh1: "set as \<sharp>* c" |
|
13 and fresh2: "set bs \<sharp>* c" |
|
14 and perm1: "\<And>p. supp p \<sharp>* c \<Longrightarrow> p \<bullet> (f as x c) = f (p \<bullet> as) (p \<bullet> x) c" |
|
15 and perm2: "\<And>p. supp p \<sharp>* c \<Longrightarrow> p \<bullet> (f bs y c) = f (p \<bullet> bs) (p \<bullet> y) c" |
|
16 shows "f as x c = f bs y c" |
|
17 proof - |
|
18 have "supp (as, x, c) supports (f as x c)" |
|
19 unfolding supports_def fresh_def[symmetric] |
|
20 by (simp add: fresh_Pair perm1 fresh_star_def supp_swap swap_fresh_fresh) |
|
21 then have fin1: "finite (supp (f as x c))" |
|
22 by (auto intro: supports_finite simp add: finite_supp) |
|
23 have "supp (bs, y, c) supports (f bs y c)" |
|
24 unfolding supports_def fresh_def[symmetric] |
|
25 by (simp add: fresh_Pair perm2 fresh_star_def supp_swap swap_fresh_fresh) |
|
26 then have fin2: "finite (supp (f bs y c))" |
|
27 by (auto intro: supports_finite simp add: finite_supp) |
|
28 obtain q::"perm" where |
|
29 fr1: "(q \<bullet> (set as)) \<sharp>* (x, c, f as x c, f bs y c)" and |
|
30 fr2: "supp q \<sharp>* Abs_lst as x" and |
|
31 inc: "supp q \<subseteq> (set as) \<union> q \<bullet> (set as)" |
|
32 using at_set_avoiding3[where xs="set as" and c="(x, c, f as x c, f bs y c)" and x="[as]lst. x"] |
|
33 fin1 fin2 |
|
34 by (auto simp add: supp_Pair finite_supp Abs_fresh_star dest: fresh_star_supp_conv) |
|
35 have "Abs_lst (q \<bullet> as) (q \<bullet> x) = q \<bullet> Abs_lst as x" by simp |
|
36 also have "\<dots> = Abs_lst as x" |
|
37 by (simp only: fr2 perm_supp_eq) |
|
38 finally have "Abs_lst (q \<bullet> as) (q \<bullet> x) = Abs_lst bs y" using eq by simp |
|
39 then obtain r::perm where |
|
40 qq1: "q \<bullet> x = r \<bullet> y" and |
|
41 qq2: "q \<bullet> as = r \<bullet> bs" and |
|
42 qq3: "supp r \<subseteq> (q \<bullet> (set as)) \<union> set bs" |
|
43 apply(drule_tac sym) |
|
44 apply(simp only: Abs_eq_iff2 alphas) |
|
45 apply(erule exE) |
|
46 apply(erule conjE)+ |
|
47 apply(drule_tac x="p" in meta_spec) |
|
48 apply(simp add: set_eqvt) |
|
49 apply(blast) |
|
50 done |
|
51 have "(set as) \<sharp>* f as x c" |
|
52 apply(rule fcb1) |
|
53 apply(rule fresh1) |
|
54 done |
|
55 then have "q \<bullet> ((set as) \<sharp>* f as x c)" |
|
56 by (simp add: permute_bool_def) |
|
57 then have "set (q \<bullet> as) \<sharp>* f (q \<bullet> as) (q \<bullet> x) c" |
|
58 apply(simp add: fresh_star_eqvt set_eqvt) |
|
59 apply(subst (asm) perm1) |
|
60 using inc fresh1 fr1 |
|
61 apply(auto simp add: fresh_star_def fresh_Pair) |
|
62 done |
|
63 then have "set (r \<bullet> bs) \<sharp>* f (r \<bullet> bs) (r \<bullet> y) c" using qq1 qq2 by simp |
|
64 then have "r \<bullet> ((set bs) \<sharp>* f bs y c)" |
|
65 apply(simp add: fresh_star_eqvt set_eqvt) |
|
66 apply(subst (asm) perm2[symmetric]) |
|
67 using qq3 fresh2 fr1 |
|
68 apply(auto simp add: set_eqvt fresh_star_def fresh_Pair) |
|
69 done |
|
70 then have fcb2: "(set bs) \<sharp>* f bs y c" by (simp add: permute_bool_def) |
|
71 have "f as x c = q \<bullet> (f as x c)" |
|
72 apply(rule perm_supp_eq[symmetric]) |
|
73 using inc fcb1[OF fresh1] fr1 by (auto simp add: fresh_star_def) |
|
74 also have "\<dots> = f (q \<bullet> as) (q \<bullet> x) c" |
|
75 apply(rule perm1) |
|
76 using inc fresh1 fr1 by (auto simp add: fresh_star_def) |
|
77 also have "\<dots> = f (r \<bullet> bs) (r \<bullet> y) c" using qq1 qq2 by simp |
|
78 also have "\<dots> = r \<bullet> (f bs y c)" |
|
79 apply(rule perm2[symmetric]) |
|
80 using qq3 fresh2 fr1 by (auto simp add: fresh_star_def) |
|
81 also have "... = f bs y c" |
|
82 apply(rule perm_supp_eq) |
|
83 using qq3 fr1 fcb2 by (auto simp add: fresh_star_def) |
|
84 finally show ?thesis by simp |
|
85 qed |
|
86 |
|
87 lemma Abs_lst1_fcb2: |
|
88 fixes a b :: "atom" |
|
89 and x y :: "'b :: fs" |
|
90 and c::"'c :: fs" |
|
91 assumes e: "(Abs_lst [a] x) = (Abs_lst [b] y)" |
|
92 and fcb1: "a \<sharp> c \<Longrightarrow> a \<sharp> f a x c" |
|
93 and fresh: "{a, b} \<sharp>* c" |
|
94 and perm1: "\<And>p. supp p \<sharp>* c \<Longrightarrow> p \<bullet> (f a x c) = f (p \<bullet> a) (p \<bullet> x) c" |
|
95 and perm2: "\<And>p. supp p \<sharp>* c \<Longrightarrow> p \<bullet> (f b y c) = f (p \<bullet> b) (p \<bullet> y) c" |
|
96 shows "f a x c = f b y c" |
|
97 using e |
|
98 apply(drule_tac Abs_lst_fcb2[where c="c" and f="\<lambda>(as::atom list) . f (hd as)"]) |
|
99 apply(simp_all) |
|
100 using fcb1 fresh perm1 perm2 |
|
101 apply(simp_all add: fresh_star_def) |
|
102 done |
|
103 |
|
104 nominal_primrec |
6 nominal_primrec |
105 CPS :: "lt \<Rightarrow> lt" ("_*" [250] 250) |
7 CPS :: "lt \<Rightarrow> lt" ("_*" [250] 250) |
106 where |
8 where |
107 "atom k \<sharp> x \<Longrightarrow> (x~)* = (Abs k ((k~) $ (x~)))" |
9 "atom k \<sharp> x \<Longrightarrow> (x~)* = (Lam k ((k~) $ (x~)))" |
108 | "atom k \<sharp> (x, M) \<Longrightarrow> (Abs x M)* = Abs k (k~ $ Abs x (M*))" |
10 | "atom k \<sharp> (x, M) \<Longrightarrow> (Lam x M)* = Lam k (k~ $ Lam x (M*))" |
109 | "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> |
110 (M $ N)* = Abs k (M* $ Abs m (N* $ Abs n (m~ $ n~ $ k~)))" |
12 (M $ N)* = Lam k (M* $ Lam m (N* $ Lam n (m~ $ n~ $ k~)))" |
111 unfolding eqvt_def CPS_graph_def |
13 unfolding eqvt_def CPS_graph_def |
112 apply (rule, perm_simp, rule, rule) |
14 apply (rule, perm_simp, rule, rule) |
113 apply (simp_all add: fresh_Pair_elim) |
15 apply (simp_all add: fresh_Pair_elim) |
114 apply (rule_tac y="x" in lt.exhaust) |
16 apply (rule_tac y="x" in lt.exhaust) |
115 apply (auto) |
17 apply (auto) |
193 |
95 |
194 lemma [simp]: |
96 lemma [simp]: |
195 shows "isValue (p \<bullet> (M::lt)) = isValue M" |
97 shows "isValue (p \<bullet> (M::lt)) = isValue M" |
196 by (nominal_induct M rule: lt.strong_induct) auto |
98 by (nominal_induct M rule: lt.strong_induct) auto |
197 |
99 |
198 lemma [eqvt]: |
|
199 shows "p \<bullet> isValue M = isValue (p \<bullet> M)" |
|
200 by (induct M rule: lt.induct) (perm_simp, rule refl)+ |
|
201 |
|
202 nominal_primrec |
100 nominal_primrec |
203 Kapply :: "lt \<Rightarrow> lt \<Rightarrow> lt" (infixl ";" 100) |
101 Kapply :: "lt \<Rightarrow> lt \<Rightarrow> lt" (infixl ";" 100) |
204 where |
102 where |
205 "Kapply (Abs x M) K = K $ (Abs x M)+" |
103 "Kapply (Lam x M) K = K $ (Lam x M)+" |
206 | "Kapply (Var x) K = K $ Var x" |
104 | "Kapply (Var x) K = K $ Var x" |
207 | "isValue M \<Longrightarrow> isValue N \<Longrightarrow> Kapply (M $ N) K = M+ $ N+ $ K" |
105 | "isValue M \<Longrightarrow> isValue N \<Longrightarrow> Kapply (M $ N) K = M+ $ N+ $ K" |
208 | "isValue M \<Longrightarrow> \<not>isValue N \<Longrightarrow> atom n \<sharp> M \<Longrightarrow> atom n \<sharp> K \<Longrightarrow> |
106 | "isValue M \<Longrightarrow> \<not>isValue N \<Longrightarrow> atom n \<sharp> M \<Longrightarrow> atom n \<sharp> K \<Longrightarrow> |
209 Kapply (M $ N) K = N; (Abs n (M+ $ Var n $ K))" |
107 Kapply (M $ N) K = N; (Lam n (M+ $ Var n $ K))" |
210 | "\<not>isValue M \<Longrightarrow> atom m \<sharp> N \<Longrightarrow> atom m \<sharp> K \<Longrightarrow> atom n \<sharp> m \<Longrightarrow> atom n \<sharp> K \<Longrightarrow> |
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> |
211 Kapply (M $ N) K = M; (Abs m (N* $ (Abs n (Var m $ Var n $ K))))" |
109 Kapply (M $ N) K = M; (Lam m (N* $ (Lam n (Var m $ Var n $ K))))" |
212 unfolding Kapply_graph_def eqvt_def |
110 unfolding Kapply_graph_def eqvt_def |
213 apply (rule, perm_simp, rule, rule) |
111 apply (rule, perm_simp, rule, rule) |
214 apply (simp_all) |
112 apply (simp_all) |
215 apply (case_tac x) |
113 apply (case_tac x) |
216 apply (rule_tac y="a" in lt.exhaust) |
114 apply (rule_tac y="a" in lt.exhaust) |
223 apply (rule_tac x="(lt2, ba)" and ?'a="name" in obtain_fresh) |
121 apply (rule_tac x="(lt2, ba)" and ?'a="name" in obtain_fresh) |
224 apply (rule_tac x="(a, ba)" and ?'a="name" in obtain_fresh) |
122 apply (rule_tac x="(a, ba)" and ?'a="name" in obtain_fresh) |
225 apply (simp add: fresh_Pair_elim fresh_at_base) |
123 apply (simp add: fresh_Pair_elim fresh_at_base) |
226 apply (auto simp add: Abs1_eq_iff eqvts)[1] |
124 apply (auto simp add: Abs1_eq_iff eqvts)[1] |
227 apply (rename_tac M N u K) |
125 apply (rename_tac M N u K) |
228 apply (subgoal_tac "Abs n (M+ $ n~ $ K) = Abs u (M+ $ u~ $ K)") |
126 apply (subgoal_tac "Lam n (M+ $ n~ $ K) = Lam u (M+ $ u~ $ K)") |
229 apply (simp only:) |
127 apply (simp only:) |
230 apply (auto simp add: Abs1_eq_iff flip_def[symmetric] lt.fresh fresh_at_base flip_fresh_fresh[symmetric])[1] |
128 apply (auto simp add: Abs1_eq_iff flip_def[symmetric] lt.fresh fresh_at_base flip_fresh_fresh[symmetric])[1] |
231 apply (subgoal_tac "Abs m (Na* $ Abs n (m~ $ n~ $ Ka)) = Abs ma (Na* $ Abs na (ma~ $ na~ $ Ka))") |
129 apply (subgoal_tac "Lam m (Na* $ Lam n (m~ $ n~ $ Ka)) = Lam ma (Na* $ Lam na (ma~ $ na~ $ Ka))") |
232 apply (simp only:) |
130 apply (simp only:) |
233 apply (simp add: Abs1_eq_iff flip_def[symmetric] lt.fresh fresh_at_base) |
131 apply (simp add: Abs1_eq_iff flip_def[symmetric] lt.fresh fresh_at_base) |
234 apply (subgoal_tac "Ka = (n \<leftrightarrow> na) \<bullet> Ka") |
132 apply (subgoal_tac "Ka = (n \<leftrightarrow> na) \<bullet> Ka") |
235 apply (subgoal_tac "Ka = (m \<leftrightarrow> ma) \<bullet> Ka") |
133 apply (subgoal_tac "Ka = (m \<leftrightarrow> ma) \<bullet> Ka") |
236 apply (subgoal_tac "Ka = (n \<leftrightarrow> (m \<leftrightarrow> ma) \<bullet> na) \<bullet> Ka") |
134 apply (subgoal_tac "Ka = (n \<leftrightarrow> (m \<leftrightarrow> ma) \<bullet> na) \<bullet> Ka") |
252 section{* lemma related to CPS conversion *} |
150 section{* lemma related to CPS conversion *} |
253 |
151 |
254 lemma value_CPS: |
152 lemma value_CPS: |
255 assumes "isValue V" |
153 assumes "isValue V" |
256 and "atom a \<sharp> V" |
154 and "atom a \<sharp> V" |
257 shows "V* = Abs a (a~ $ V+)" |
155 shows "V* = Lam a (a~ $ V+)" |
258 using assms |
156 using assms |
259 proof (nominal_induct V avoiding: a rule: lt.strong_induct, simp_all add: lt.fresh) |
157 proof (nominal_induct V avoiding: a rule: lt.strong_induct, simp_all add: lt.fresh) |
260 fix name :: name and lt aa |
158 fix name :: name and lt aa |
261 assume a: "atom name \<sharp> aa" "\<And>b. \<lbrakk>isValue lt; atom b \<sharp> lt\<rbrakk> \<Longrightarrow> lt* = Abs b (b~ $ lt+)" |
159 assume a: "atom name \<sharp> aa" "\<And>b. \<lbrakk>isValue lt; atom b \<sharp> lt\<rbrakk> \<Longrightarrow> lt* = Lam b (b~ $ lt+)" |
262 "atom aa \<sharp> lt \<or> aa = name" |
160 "atom aa \<sharp> lt \<or> aa = name" |
263 obtain ab :: name where b: "atom ab \<sharp> (name, lt, a)" using obtain_fresh by blast |
161 obtain ab :: name where b: "atom ab \<sharp> (name, lt, a)" using obtain_fresh by blast |
264 show "Abs name lt* = Abs aa (aa~ $ Abs name (lt*))" using a b |
162 show "Lam name lt* = Lam aa (aa~ $ Lam name (lt*))" using a b |
265 by (simp add: Abs1_eq_iff fresh_at_base lt.fresh) |
163 by (simp add: Abs1_eq_iff fresh_at_base lt.fresh) |
266 qed |
164 qed |
267 |
165 |
268 section{* first lemma CPS subst *} |
166 section{* first lemma CPS subst *} |
269 |
167 |
270 lemma CPS_subst_fv: |
168 lemma CPS_subst_fv: |
271 assumes *:"isValue V" |
169 assumes *:"isValue V" |
272 shows "((M[V/x])* = (M*)[V+/x])" |
170 shows "((M[x ::= V])* = (M*)[x ::= V+])" |
273 using * proof (nominal_induct M avoiding: V x rule: lt.strong_induct) |
171 using * proof (nominal_induct M avoiding: V x rule: lt.strong_induct) |
274 case (Var name) |
172 case (Var name) |
275 assume *: "isValue V" |
173 assume *: "isValue V" |
276 obtain a :: name where a: "atom a \<sharp> (x, name, V)" using obtain_fresh by blast |
174 obtain a :: name where a: "atom a \<sharp> (x, name, V)" using obtain_fresh by blast |
277 show "((name~)[V/x])* = (name~)*[V+/x]" using a |
175 show "((name~)[x ::= V])* = (name~)*[x ::= V+]" using a |
278 by (simp add: fresh_at_base * value_CPS) |
176 by (simp add: fresh_at_base * value_CPS) |
279 next |
177 next |
280 case (Abs name lt V x) |
178 case (Lam name lt V x) |
281 assume *: "atom name \<sharp> V" "atom name \<sharp> x" "\<And>b ba. isValue b \<Longrightarrow> (lt[b/ba])* = lt*[b+/ba]" |
179 assume *: "atom name \<sharp> V" "atom name \<sharp> x" "\<And>b ba. isValue b \<Longrightarrow> (lt[ba ::= b])* = lt*[ba ::= b+]" |
282 "isValue V" |
180 "isValue V" |
283 obtain a :: name where a: "atom a \<sharp> (name, lt, lt[V/x], x, V)" using obtain_fresh by blast |
181 obtain a :: name where a: "atom a \<sharp> (name, lt, lt[x ::= V], x, V)" using obtain_fresh by blast |
284 show "(Abs name lt[V/x])* = Abs name lt*[V+/x]" using * a |
182 show "(Lam name lt[x ::= V])* = Lam name lt*[x ::= V+]" using * a |
285 by (simp add: fresh_at_base) |
183 by (simp add: fresh_at_base) |
286 next |
184 next |
287 case (App lt1 lt2 V x) |
185 case (App lt1 lt2 V x) |
288 assume *: "\<And>b ba. isValue b \<Longrightarrow> (lt1[b/ba])* = lt1*[b+/ba]" "\<And>b ba. isValue b \<Longrightarrow> (lt2[b/ba])* = lt2*[b+/ba]" |
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+]" |
289 "isValue V" |
187 "isValue V" |
290 obtain a :: name where a: "atom a \<sharp> (lt1[V/x], lt1, lt2[V/x], lt2, V, x)" using obtain_fresh by blast |
188 obtain a :: name where a: "atom a \<sharp> (lt1[x ::= V], lt1, lt2[x ::= V], lt2, V, x)" using obtain_fresh by blast |
291 obtain b :: name where b: "atom b \<sharp> (lt2[V/x], lt2, a, 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 |
292 obtain c :: name where c: "atom c \<sharp> (a, b, 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 |
293 show "((lt1 $ lt2)[V/x])* = (lt1 $ lt2)*[V+/x]" using * a b c |
191 show "((lt1 $ lt2)[x ::= V])* = (lt1 $ lt2)*[x ::= V+]" using * a b c |
294 by (simp add: fresh_at_base) |
192 by (simp add: fresh_at_base) |
295 qed |
193 qed |
296 |
194 |
297 lemma [simp]: "isValue V \<Longrightarrow> isValue (V+)" |
195 lemma [simp]: "isValue V \<Longrightarrow> isValue (V+)" |
298 by (nominal_induct V rule: lt.strong_induct, auto) |
196 by (nominal_induct V rule: lt.strong_induct, auto) |
310 next |
208 next |
311 fix name :: name and lt K |
209 fix name :: name and lt K |
312 assume *: "atom name \<sharp> K" "\<And>b. isValue b \<Longrightarrow> lt* $ b \<longrightarrow>\<^isub>\<beta>\<^sup>* lt ; b" "isValue K" |
210 assume *: "atom name \<sharp> K" "\<And>b. isValue b \<Longrightarrow> lt* $ b \<longrightarrow>\<^isub>\<beta>\<^sup>* lt ; b" "isValue K" |
313 obtain a :: name where a: "atom a \<sharp> (name, K, lt)" using obtain_fresh by blast |
211 obtain a :: name where a: "atom a \<sharp> (name, K, lt)" using obtain_fresh by blast |
314 then have b: "atom name \<sharp> a" using fresh_PairD(1) fresh_at_base atom_eq_iff by metis |
212 then have b: "atom name \<sharp> a" using fresh_PairD(1) fresh_at_base atom_eq_iff by metis |
315 show "Abs name lt* $ K \<longrightarrow>\<^isub>\<beta>\<^sup>* K $ Abs name (lt*)" using * a b |
213 show "Lam name lt* $ K \<longrightarrow>\<^isub>\<beta>\<^sup>* K $ Lam name (lt*)" using * a b |
316 by simp (rule evbeta', simp_all) |
214 by simp (rule evbeta', simp_all) |
317 next |
215 next |
318 fix lt1 lt2 K |
216 fix lt1 lt2 K |
319 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" |
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" |
320 obtain a :: name where a: "atom a \<sharp> (lt1, lt2, K)" using obtain_fresh by blast |
218 obtain a :: name where a: "atom a \<sharp> (lt1, lt2, K)" using obtain_fresh by blast |
321 obtain b :: name where b: "atom b \<sharp> (lt1, lt2, K, a)" using obtain_fresh by blast |
219 obtain b :: name where b: "atom b \<sharp> (lt1, lt2, K, a)" using obtain_fresh by blast |
322 obtain c :: name where c: "atom c \<sharp> (lt1, lt2, K, a, b)" using obtain_fresh by blast |
220 obtain c :: name where c: "atom c \<sharp> (lt1, lt2, K, a, b)" using obtain_fresh by blast |
323 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" |
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" |
324 "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 |
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 |
325 have "(lt1 $ lt2)* $ K \<longrightarrow>\<^isub>\<beta>\<^sup>* lt1* $ Abs b (lt2* $ Abs c (b~ $ c~ $ K))" using * d |
223 have "(lt1 $ lt2)* $ K \<longrightarrow>\<^isub>\<beta>\<^sup>* lt1* $ Lam b (lt2* $ Lam c (b~ $ c~ $ K))" using * d |
326 by (simp add: fresh_at_base) (rule evbeta', simp_all add: fresh_at_base) |
224 by (simp add: fresh_at_base) (rule evbeta', simp_all add: fresh_at_base) |
327 also have "... \<longrightarrow>\<^isub>\<beta>\<^sup>* lt1 $ lt2 ; K" proof (cases "isValue lt1") |
225 also have "... \<longrightarrow>\<^isub>\<beta>\<^sup>* lt1 $ lt2 ; K" proof (cases "isValue lt1") |
328 assume e: "isValue lt1" |
226 assume e: "isValue lt1" |
329 have "lt1* $ Abs b (lt2* $ Abs c (b~ $ c~ $ K)) \<longrightarrow>\<^isub>\<beta>\<^sup>* Abs b (lt2* $ Abs c (b~ $ c~ $ K)) $ 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+" |
330 using * d e by simp |
228 using * d e by simp |
331 also have "... \<longrightarrow>\<^isub>\<beta>\<^sup>* lt2* $ Abs c (lt1+ $ c~ $ K)" |
229 also have "... \<longrightarrow>\<^isub>\<beta>\<^sup>* lt2* $ Lam c (lt1+ $ c~ $ K)" |
332 by (rule evbeta', simp_all add: * d e, metis d(12) fresh_at_base) |
230 by (rule evbeta', simp_all add: * d e, metis d(12) fresh_at_base) |
333 also have "... \<longrightarrow>\<^isub>\<beta>\<^sup>* lt1 $ lt2 ; K" proof (cases "isValue lt2") |
231 also have "... \<longrightarrow>\<^isub>\<beta>\<^sup>* lt1 $ lt2 ; K" proof (cases "isValue lt2") |
334 assume f: "isValue lt2" |
232 assume f: "isValue lt2" |
335 have "lt2* $ Abs c (lt1+ $ c~ $ K) \<longrightarrow>\<^isub>\<beta>\<^sup>* Abs c (lt1+ $ c~ $ K) $ lt2+" using * d e f by simp |
233 have "lt2* $ Lam c (lt1+ $ c~ $ K) \<longrightarrow>\<^isub>\<beta>\<^sup>* Lam c (lt1+ $ c~ $ K) $ lt2+" using * d e f by simp |
336 also have "... \<longrightarrow>\<^isub>\<beta>\<^sup>* lt1+ $ lt2+ $ K" |
234 also have "... \<longrightarrow>\<^isub>\<beta>\<^sup>* lt1+ $ lt2+ $ K" |
337 by (rule evbeta', simp_all add: d e f) |
235 by (rule evbeta', simp_all add: d e f) |
338 finally show ?thesis using * d e f by simp |
236 finally show ?thesis using * d e f by simp |
339 next |
237 next |
340 assume f: "\<not> isValue lt2" |
238 assume f: "\<not> isValue lt2" |
341 have "lt2* $ Abs c (lt1+ $ c~ $ K) \<longrightarrow>\<^isub>\<beta>\<^sup>* lt2 ; Abs c (lt1+ $ c~ $ K)" using * d e f by simp |
239 have "lt2* $ Lam c (lt1+ $ c~ $ K) \<longrightarrow>\<^isub>\<beta>\<^sup>* lt2 ; Lam c (lt1+ $ c~ $ K)" using * d e f by simp |
342 also have "... \<longrightarrow>\<^isub>\<beta>\<^sup>* lt2 ; Abs a (lt1+ $ a~ $ K)" using Kapply.simps(4) d e evs1 f by metis |
240 also have "... \<longrightarrow>\<^isub>\<beta>\<^sup>* lt2 ; Lam a (lt1+ $ a~ $ K)" using Kapply.simps(4) d e evs1 f by metis |
343 finally show ?thesis using * d e f by simp |
241 finally show ?thesis using * d e f by simp |
344 qed |
242 qed |
345 finally show ?thesis . |
243 finally show ?thesis . |
346 qed (metis Kapply.simps(5) isValue.simps(2) * d) |
244 qed (metis Kapply.simps(5) isValue.simps(2) * d) |
347 finally show "(lt1 $ lt2)* $ K \<longrightarrow>\<^isub>\<beta>\<^sup>* lt1 $ lt2 ; K" . |
245 finally show "(lt1 $ lt2)* $ K \<longrightarrow>\<^isub>\<beta>\<^sup>* lt1 $ lt2 ; K" . |
353 using assms |
251 using assms |
354 proof (induct arbitrary: K rule: eval.induct) |
252 proof (induct arbitrary: K rule: eval.induct) |
355 case (evbeta x V M) |
253 case (evbeta x V M) |
356 fix K |
254 fix K |
357 assume a: "isValue K" "isValue V" "atom x \<sharp> V" |
255 assume a: "isValue K" "isValue V" "atom x \<sharp> V" |
358 have "Abs x (M*) $ V+ $ K \<longrightarrow>\<^isub>\<beta>\<^sup>* ((M*)[V+/x] $ K)" |
256 have "Lam x (M*) $ V+ $ K \<longrightarrow>\<^isub>\<beta>\<^sup>* (((M*)[x ::= V+]) $ K)" |
359 by (rule evs2,rule ev2,rule Lt.evbeta) (simp_all add: fresh_def a[simplified fresh_def] evs1) |
257 by (rule evs2,rule ev2,rule Lt.evbeta) (simp_all add: fresh_def a[simplified fresh_def] evs1) |
360 also have "... = ((M[V/x])* $ K)" by (simp add: CPS_subst_fv a) |
258 also have "... = ((M[x ::= V])* $ K)" by (simp add: CPS_subst_fv a) |
361 also have "... \<longrightarrow>\<^isub>\<beta>\<^sup>* (M[V/x] ; K)" by (rule CPS_eval_Kapply, simp_all add: a) |
259 also have "... \<longrightarrow>\<^isub>\<beta>\<^sup>* ((M[x ::= V]) ; K)" by (rule CPS_eval_Kapply, simp_all add: a) |
362 finally show "(Abs x M $ V ; K) \<longrightarrow>\<^isub>\<beta>\<^sup>* (M[V/x] ; K)" using a by simp |
260 finally show "(Lam x M $ V ; K) \<longrightarrow>\<^isub>\<beta>\<^sup>* ((M[x ::= V]) ; K)" using a by simp |
363 next |
261 next |
364 case (ev1 V M N) |
262 case (ev1 V M N) |
365 fix V M N K |
263 fix V M N K |
366 assume a: "isValue V" "M \<longrightarrow>\<^isub>\<beta> N" "\<And>K. isValue K \<Longrightarrow> M ; K \<longrightarrow>\<^isub>\<beta>\<^sup>* N ; K" "isValue 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" |
367 obtain a :: name where b: "atom a \<sharp> (V, K, M, N)" using obtain_fresh by blast |
265 obtain a :: name where b: "atom a \<sharp> (V, K, M, N)" using obtain_fresh by blast |
368 show "V $ M ; K \<longrightarrow>\<^isub>\<beta>\<^sup>* V $ N ; K" proof (cases "isValue N") |
266 show "V $ M ; K \<longrightarrow>\<^isub>\<beta>\<^sup>* V $ N ; K" proof (cases "isValue N") |
369 assume "\<not> isValue N" |
267 assume "\<not> isValue N" |
370 then show "V $ M ; K \<longrightarrow>\<^isub>\<beta>\<^sup>* V $ N ; K" using a b by simp |
268 then show "V $ M ; K \<longrightarrow>\<^isub>\<beta>\<^sup>* V $ N ; K" using a b by simp |
371 next |
269 next |
372 assume n: "isValue N" |
270 assume n: "isValue N" |
373 have c: "M; Abs a (V+ $ a~ $ K) \<longrightarrow>\<^isub>\<beta>\<^sup>* Abs a (V+ $ a~ $ K) $ N+" using a b by (simp add: 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) |
374 also have d: "... \<longrightarrow>\<^isub>\<beta>\<^sup>* V+ $ N+ $ K" by (rule evbeta') (simp_all add: a b n) |
272 also have d: "... \<longrightarrow>\<^isub>\<beta>\<^sup>* V+ $ N+ $ K" by (rule evbeta') (simp_all add: a b n) |
375 finally show "V $ M ; K \<longrightarrow>\<^isub>\<beta>\<^sup>* V $ N ; K" using a b by (simp add: n) |
273 finally show "V $ M ; K \<longrightarrow>\<^isub>\<beta>\<^sup>* V $ N ; K" using a b by (simp add: n) |
376 qed |
274 qed |
377 next |
275 next |
378 case (ev2 M M' N) |
276 case (ev2 M M' N) |
379 assume *: "M \<longrightarrow>\<^isub>\<beta> M'" "\<And>K. isValue K \<Longrightarrow> M ; K \<longrightarrow>\<^isub>\<beta>\<^sup>* M' ; K" "isValue K" |
277 assume *: "M \<longrightarrow>\<^isub>\<beta> M'" "\<And>K. isValue K \<Longrightarrow> M ; K \<longrightarrow>\<^isub>\<beta>\<^sup>* M' ; K" "isValue K" |
380 obtain a :: name where a: "atom a \<sharp> (K, M, N, M')" using obtain_fresh by blast |
278 obtain a :: name where a: "atom a \<sharp> (K, M, N, M')" using obtain_fresh by blast |
381 obtain b :: name where b: "atom b \<sharp> (a, K, M, N, M', N+)" 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 |
382 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" |
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" |
383 "atom b \<sharp> M" "atom b \<sharp> N" "atom b \<sharp> M'" using a b fresh_Pair by simp_all |
281 "atom b \<sharp> M" "atom b \<sharp> N" "atom b \<sharp> M'" using a b fresh_Pair by simp_all |
384 have "M $ N ; K \<longrightarrow>\<^isub>\<beta>\<^sup>* M' ; Abs a (N* $ Abs b (a~ $ b~ $ K))" using * d by simp |
282 have "M $ N ; K \<longrightarrow>\<^isub>\<beta>\<^sup>* M' ; Lam a (N* $ Lam b (a~ $ b~ $ K))" using * d by simp |
385 also have "... \<longrightarrow>\<^isub>\<beta>\<^sup>* M' $ N ; K" proof (cases "isValue M'") |
283 also have "... \<longrightarrow>\<^isub>\<beta>\<^sup>* M' $ N ; K" proof (cases "isValue M'") |
386 assume "\<not> isValue M'" |
284 assume "\<not> isValue M'" |
387 then show ?thesis using * d by (simp_all add: evs1) |
285 then show ?thesis using * d by (simp_all add: evs1) |
388 next |
286 next |
389 assume e: "isValue M'" |
287 assume e: "isValue M'" |
390 then have "M' ; Abs a (N* $ Abs b (a~ $ b~ $ K)) = Abs a (N* $ Abs b (a~ $ b~ $ K)) $ M'+" by simp |
288 then have "M' ; Lam a (N* $ Lam b (a~ $ b~ $ K)) = Lam a (N* $ Lam b (a~ $ b~ $ K)) $ M'+" by simp |
391 also have "... \<longrightarrow>\<^isub>\<beta>\<^sup>* (N* $ Abs b (a~ $ b~ $ K))[M'+/a]" |
289 also have "... \<longrightarrow>\<^isub>\<beta>\<^sup>* (N* $ Lam b (a~ $ b~ $ K))[a ::= M'+]" |
392 by (rule evbeta') (simp_all add: fresh_at_base e d) |
290 by (rule evbeta') (simp_all add: fresh_at_base e d) |
393 also have "... = N* $ Abs b (M'+ $ b~ $ K)" using * d by (simp add: fresh_at_base) |
291 also have "... = N* $ Lam b (M'+ $ b~ $ K)" using * d by (simp add: fresh_at_base) |
394 also have "... \<longrightarrow>\<^isub>\<beta>\<^sup>* M' $ N ; K" proof (cases "isValue N") |
292 also have "... \<longrightarrow>\<^isub>\<beta>\<^sup>* M' $ N ; K" proof (cases "isValue N") |
395 assume f: "isValue N" |
293 assume f: "isValue N" |
396 have "N* $ Abs b (M'+ $ b~ $ K) \<longrightarrow>\<^isub>\<beta>\<^sup>* Abs b (M'+ $ b~ $ K) $ N+" |
294 have "N* $ Lam b (M'+ $ b~ $ K) \<longrightarrow>\<^isub>\<beta>\<^sup>* Lam b (M'+ $ b~ $ K) $ N+" |
397 by (rule eval_trans, rule CPS_eval_Kapply) (simp_all add: d e f * evs1) |
295 by (rule eval_trans, rule CPS_eval_Kapply) (simp_all add: d e f * evs1) |
398 also have "... \<longrightarrow>\<^isub>\<beta>\<^sup>* M' $ N ; K" by (rule evbeta') (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) |
399 finally show ?thesis . |
297 finally show ?thesis . |
400 next |
298 next |
401 assume "\<not> isValue N" |
299 assume "\<not> isValue N" |
413 using H |
311 using H |
414 by (induct) (metis Kapply_eval assms(2) eval_trans evs1)+ |
312 by (induct) (metis Kapply_eval assms(2) eval_trans evs1)+ |
415 |
313 |
416 lemma |
314 lemma |
417 assumes "isValue V" "M \<longrightarrow>\<^isub>\<beta>\<^sup>* V" |
315 assumes "isValue V" "M \<longrightarrow>\<^isub>\<beta>\<^sup>* V" |
418 shows "M* $ (Abs x (x~)) \<longrightarrow>\<^isub>\<beta>\<^sup>* V+" |
316 shows "M* $ (Lam x (x~)) \<longrightarrow>\<^isub>\<beta>\<^sup>* V+" |
419 proof- |
317 proof- |
420 obtain y::name where *: "atom y \<sharp> V" using obtain_fresh by blast |
318 obtain y::name where *: "atom y \<sharp> V" using obtain_fresh by blast |
421 have e: "Abs x (x~) = Abs y (y~)" |
319 have e: "Lam x (x~) = Lam y (y~)" |
422 by (simp add: Abs1_eq_iff lt.fresh fresh_at_base) |
320 by (simp add: Abs1_eq_iff lt.fresh fresh_at_base) |
423 have "M* $ Abs x (x~) \<longrightarrow>\<^isub>\<beta>\<^sup>* M ; Abs x (x~)" |
321 have "M* $ Lam x (x~) \<longrightarrow>\<^isub>\<beta>\<^sup>* M ; Lam x (x~)" |
424 by(rule CPS_eval_Kapply,simp_all add: assms) |
322 by(rule CPS_eval_Kapply,simp_all add: assms) |
425 also have "... \<longrightarrow>\<^isub>\<beta>\<^sup>* (V ; Abs x (x~))" by (rule Kapply_eval_rtrancl, simp_all add: assms) |
323 also have "... \<longrightarrow>\<^isub>\<beta>\<^sup>* (V ; Lam x (x~))" by (rule Kapply_eval_rtrancl, simp_all add: assms) |
426 also have "... = V ; Abs y (y~)" using e by (simp only:) |
324 also have "... = V ; Lam y (y~)" using e by (simp only:) |
427 also have "... \<longrightarrow>\<^isub>\<beta>\<^sup>* (V+)" by (simp add: assms, rule evbeta') (simp_all add: assms *) |
325 also have "... \<longrightarrow>\<^isub>\<beta>\<^sup>* (V+)" by (simp add: assms, rule evbeta') (simp_all add: assms *) |
428 finally show "M* $ (Abs x (x~)) \<longrightarrow>\<^isub>\<beta>\<^sup>* (V+)" . |
326 finally show "M* $ (Lam x (x~)) \<longrightarrow>\<^isub>\<beta>\<^sup>* (V+)" . |
429 qed |
327 qed |
430 |
328 |
431 end |
329 end |
432 |
330 |
433 |
331 |