1 (* "$Id$" *) |
1 (* "$Id$" *) |
2 (* *) |
2 (* *) |
3 (* Formalisation of some typical SOS-proofs *) |
3 (* Formalisation of some typical SOS-proofs. *) |
4 (* *) |
4 (* *) |
5 (* This work arose from challenge suggested by Adam *) |
5 (* This work arose from a challenge suggested by Adam *) |
6 (* Chlipala suggested on the POPLmark mailing list. *) |
6 (* Chlipala on the POPLmark mailing list. *) |
7 (* *) |
7 (* *) |
8 (* We thank Nick Benton for helping us with the *) |
8 (* We thank Nick Benton for helping us with the *) |
9 (* termination-proof for evaluation. *) |
9 (* termination-proof for evaluation. *) |
10 (* *) |
10 (* *) |
11 (* The formalisation was done by Julien Narboux and *) |
11 (* The formalisation was done by Julien Narboux and *) |
12 (* Christian Urban. *) |
12 (* Christian Urban. *) |
13 |
13 |
14 theory SOS |
14 theory SOS |
15 imports "../Nominal" |
15 imports "../Nominal" |
16 begin |
16 begin |
17 |
17 |
18 atom_decl name |
18 atom_decl name |
19 |
19 |
20 nominal_datatype data = |
20 text {* types and terms *} |
21 DNat |
|
22 | DProd "data" "data" |
|
23 | DSum "data" "data" |
|
24 |
|
25 nominal_datatype ty = |
21 nominal_datatype ty = |
26 Data "data" |
22 TVar "nat" |
27 | Arrow "ty" "ty" ("_\<rightarrow>_" [100,100] 100) |
23 | Arrow "ty" "ty" ("_\<rightarrow>_" [100,100] 100) |
28 |
24 |
29 nominal_datatype trm = |
25 nominal_datatype trm = |
30 Var "name" |
26 Var "name" |
31 | Lam "\<guillemotleft>name\<guillemotright>trm" ("Lam [_]._" [100,100] 100) |
27 | Lam "\<guillemotleft>name\<guillemotright>trm" ("Lam [_]._" [100,100] 100) |
32 | App "trm" "trm" |
28 | App "trm" "trm" |
33 | Const "nat" |
29 |
34 | Pr "trm" "trm" |
30 lemma fresh_ty: |
35 | Fst "trm" |
|
36 | Snd "trm" |
|
37 | InL "trm" |
|
38 | InR "trm" |
|
39 | Case "trm" "\<guillemotleft>name\<guillemotright>trm" "\<guillemotleft>name\<guillemotright>trm" ("Case _ of inl _ \<rightarrow> _ | inr _ \<rightarrow> _" [100,100,100,100,100] 100) |
|
40 |
|
41 lemma in_eqvt[eqvt]: |
|
42 fixes pi::"name prm" |
|
43 and x::"'a::pt_name" |
|
44 assumes "x\<in>X" |
|
45 shows "pi\<bullet>x \<in> pi\<bullet>X" |
|
46 using assms by (perm_simp add: pt_set_bij1a[OF pt_name_inst, OF at_name_inst]) |
|
47 |
|
48 lemma perm_data[simp]: |
|
49 fixes D::"data" |
|
50 and pi::"name prm" |
|
51 shows "pi\<bullet>D = D" |
|
52 by (induct D rule: data.weak_induct) (simp_all) |
|
53 |
|
54 lemma perm_ty[simp]: |
|
55 fixes T::"ty" |
|
56 and pi::"name prm" |
|
57 shows "pi\<bullet>T = T" |
|
58 by (induct T rule: ty.weak_induct) (simp_all) |
|
59 |
|
60 lemma fresh_ty[simp]: |
|
61 fixes x::"name" |
31 fixes x::"name" |
62 and T::"ty" |
32 and T::"ty" |
63 shows "x\<sharp>T" |
33 shows "x\<sharp>T" |
64 by (simp add: fresh_def supp_def) |
34 by (induct T rule: ty.weak_induct) |
65 |
35 (auto simp add: fresh_nat) |
66 text {* substitution *} |
36 |
67 |
37 text {* Parallel and single substitution. *} |
68 fun |
38 fun |
69 lookup :: "(name\<times>trm) list \<Rightarrow> name \<Rightarrow> trm" |
39 lookup :: "(name\<times>trm) list \<Rightarrow> name \<Rightarrow> trm" |
70 where |
40 where |
71 "lookup [] x = Var x" |
41 "lookup [] x = Var x" |
72 | "lookup ((y,e)#\<theta>) x = (if x=y then e else lookup \<theta> x)" |
42 | "lookup ((y,e)#\<theta>) x = (if x=y then e else lookup \<theta> x)" |
73 |
43 |
74 lemma lookup_eqvt: |
44 lemma lookup_eqvt[eqvt]: |
75 fixes pi::"name prm" |
45 fixes pi::"name prm" |
76 and \<theta>::"(name\<times>trm) list" |
46 and \<theta>::"(name\<times>trm) list" |
77 and X::"name" |
47 and X::"name" |
78 shows "pi\<bullet>(lookup \<theta> X) = lookup (pi\<bullet>\<theta>) (pi\<bullet>X)" |
48 shows "pi\<bullet>(lookup \<theta> X) = lookup (pi\<bullet>\<theta>) (pi\<bullet>X)" |
79 by (induct \<theta>, auto simp add: perm_bij) |
49 by (induct \<theta>) (auto simp add: eqvts) |
80 |
50 |
81 lemma lookup_fresh: |
51 lemma lookup_fresh: |
82 fixes z::"name" |
52 fixes z::"name" |
83 assumes "z\<sharp>\<theta>" and "z\<sharp>x" |
53 assumes a: "z\<sharp>\<theta>" and b: "z\<sharp>x" |
84 shows "z \<sharp>lookup \<theta> x" |
54 shows "z \<sharp>lookup \<theta> x" |
85 using assms |
55 using a b |
86 by (induct rule: lookup.induct) (auto simp add: fresh_list_cons) |
56 by (induct rule: lookup.induct) (auto simp add: fresh_list_cons) |
87 |
57 |
88 lemma lookup_fresh': |
58 lemma lookup_fresh': |
89 assumes "z\<sharp>\<theta>" |
59 assumes "z\<sharp>\<theta>" |
90 shows "lookup \<theta> z = Var z" |
60 shows "lookup \<theta> z = Var z" |
91 using assms |
61 using assms |
92 by (induct rule: lookup.induct) |
62 by (induct rule: lookup.induct) |
93 (auto simp add: fresh_list_cons fresh_prod fresh_atm) |
63 (auto simp add: fresh_list_cons fresh_prod fresh_atm) |
94 |
64 |
95 text {* Parallel Substitution *} |
65 (* parallel substitution *) |
96 |
|
97 consts |
66 consts |
98 psubst :: "(name\<times>trm) list \<Rightarrow> trm \<Rightarrow> trm" ("_<_>" [95,95] 105) |
67 psubst :: "(name\<times>trm) list \<Rightarrow> trm \<Rightarrow> trm" ("_<_>" [95,95] 105) |
99 |
68 |
100 nominal_primrec |
69 nominal_primrec |
101 "\<theta><(Var x)> = (lookup \<theta> x)" |
70 "\<theta><(Var x)> = (lookup \<theta> x)" |
102 "\<theta><(App e\<^isub>1 e\<^isub>2)> = App (\<theta><e\<^isub>1>) (\<theta><e\<^isub>2>)" |
71 "\<theta><(App e\<^isub>1 e\<^isub>2)> = App (\<theta><e\<^isub>1>) (\<theta><e\<^isub>2>)" |
103 "x\<sharp>\<theta> \<Longrightarrow> \<theta><(Lam [x].e)> = Lam [x].(\<theta><e>)" |
72 "x\<sharp>\<theta> \<Longrightarrow> \<theta><(Lam [x].e)> = Lam [x].(\<theta><e>)" |
104 "\<theta><(Const n)> = Const n" |
73 apply(finite_guess)+ |
105 "\<theta><(Pr e\<^isub>1 e\<^isub>2)> = Pr (\<theta><e\<^isub>1>) (\<theta><e\<^isub>2>)" |
|
106 "\<theta><(Fst e)> = Fst (\<theta><e>)" |
|
107 "\<theta><(Snd e)> = Snd (\<theta><e>)" |
|
108 "\<theta><(InL e)> = InL (\<theta><e>)" |
|
109 "\<theta><(InR e)> = InR (\<theta><e>)" |
|
110 "\<lbrakk>y\<noteq>x; x\<sharp>(e,e\<^isub>2,\<theta>); y\<sharp>(e,e\<^isub>1,\<theta>)\<rbrakk> |
|
111 \<Longrightarrow> \<theta><Case e of inl x \<rightarrow> e\<^isub>1 | inr y \<rightarrow> e\<^isub>2> = (Case (\<theta><e>) of inl x \<rightarrow> (\<theta><e\<^isub>1>) | inr y \<rightarrow> (\<theta><e\<^isub>2>))" |
|
112 apply(finite_guess add: lookup_eqvt)+ |
|
113 apply(rule TrueI)+ |
74 apply(rule TrueI)+ |
114 apply(simp add: abs_fresh)+ |
75 apply(simp add: abs_fresh)+ |
115 apply(fresh_guess add: fs_name1 lookup_eqvt)+ |
76 apply(fresh_guess)+ |
116 done |
77 done |
117 |
78 |
118 lemma psubst_eqvt[eqvt]: |
79 lemma psubst_eqvt[eqvt]: |
119 fixes pi::"name prm" |
80 fixes pi::"name prm" |
120 and t::"trm" |
81 and t::"trm" |
234 then have "(x,t\<^isub>2) = (x,t\<^isub>1)" using asm1 by auto |
167 then have "(x,t\<^isub>2) = (x,t\<^isub>1)" using asm1 by auto |
235 then show "t\<^isub>1 = t\<^isub>2" by auto |
168 then show "t\<^isub>1 = t\<^isub>2" by auto |
236 qed |
169 qed |
237 |
170 |
238 lemma case_distinction_on_context: |
171 lemma case_distinction_on_context: |
239 fixes \<Gamma>::"(name \<times> ty) list" |
172 fixes \<Gamma>::"(name\<times>ty) list" |
240 assumes asm1: "valid ((m,t)#\<Gamma>)" |
173 assumes asm1: "valid ((m,t)#\<Gamma>)" |
241 and asm2: "(n,U) \<in> set ((m,T)#\<Gamma>)" |
174 and asm2: "(n,U) \<in> set ((m,T)#\<Gamma>)" |
242 shows "(n,U) = (m,T) \<or> ((n,U) \<in> set \<Gamma> \<and> n \<noteq> m)" |
175 shows "(n,U) = (m,T) \<or> ((n,U) \<in> set \<Gamma> \<and> n \<noteq> m)" |
243 proof - |
176 proof - |
244 from asm2 have "(n,U) \<in> set [(m,T)] \<or> (n,U) \<in> set \<Gamma>" by auto |
177 from asm2 have "(n,U) \<in> set [(m,T)] \<or> (n,U) \<in> set \<Gamma>" by auto |
245 moreover |
178 moreover |
246 { assume eq: "m=n" |
179 { assume eq: "m=n" |
247 assume "(n,U) \<in> set \<Gamma>" |
180 assume "(n,U) \<in> set \<Gamma>" |
248 then have "\<not> n\<sharp>\<Gamma>" |
181 then have "\<not> n\<sharp>\<Gamma>" |
249 by (induct \<Gamma>) (auto simp add: fresh_list_cons fresh_prod fresh_atm) |
182 by (induct \<Gamma>) (auto simp add: fresh_list_cons fresh_prod fresh_atm) |
250 moreover have "m\<sharp>\<Gamma>" using asm1 by auto |
183 moreover have "m\<sharp>\<Gamma>" using asm1 by auto |
251 ultimately have False using eq by auto |
184 ultimately have False using eq by auto |
252 } |
185 } |
253 ultimately show ?thesis by auto |
186 ultimately show ?thesis by auto |
254 qed |
187 qed |
255 |
188 |
256 inductive |
189 inductive |
257 typing :: "(name\<times>ty) list\<Rightarrow>trm\<Rightarrow>ty\<Rightarrow>bool" ("_ \<turnstile> _ : _" [60,60,60] 60) |
190 typing :: "(name\<times>ty) list\<Rightarrow>trm\<Rightarrow>ty\<Rightarrow>bool" ("_ \<turnstile> _ : _" [60,60,60] 60) |
258 where |
191 where |
259 t_Var[intro]: "\<lbrakk>valid \<Gamma>; (x,T)\<in>set \<Gamma>\<rbrakk>\<Longrightarrow> \<Gamma> \<turnstile> Var x : T" |
192 t_Var[intro]: "\<lbrakk>valid \<Gamma>; (x,T)\<in>set \<Gamma>\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> Var x : T" |
260 | t_App[intro]: "\<lbrakk>\<Gamma> \<turnstile> e\<^isub>1 : T\<^isub>1\<rightarrow>T\<^isub>2; \<Gamma> \<turnstile> e\<^isub>2 : T\<^isub>1\<rbrakk>\<Longrightarrow> \<Gamma> \<turnstile> App e\<^isub>1 e\<^isub>2 : T\<^isub>2" |
193 | t_App[intro]: "\<lbrakk>\<Gamma> \<turnstile> e\<^isub>1 : T\<^isub>1\<rightarrow>T\<^isub>2; \<Gamma> \<turnstile> e\<^isub>2 : T\<^isub>1\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> App e\<^isub>1 e\<^isub>2 : T\<^isub>2" |
261 | t_Lam[intro]: "\<lbrakk>x\<sharp>\<Gamma>; (x,T\<^isub>1)#\<Gamma> \<turnstile> e : T\<^isub>2\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> Lam [x].e : T\<^isub>1\<rightarrow>T\<^isub>2" |
194 | t_Lam[intro]: "\<lbrakk>x\<sharp>\<Gamma>; (x,T\<^isub>1)#\<Gamma> \<turnstile> e : T\<^isub>2\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> Lam [x].e : T\<^isub>1\<rightarrow>T\<^isub>2" |
262 | t_Const[intro]: "valid \<Gamma> \<Longrightarrow> \<Gamma> \<turnstile> Const n : Data(DNat)" |
|
263 | t_Pr[intro]: "\<lbrakk>\<Gamma> \<turnstile> e\<^isub>1 : Data(S\<^isub>1); \<Gamma> \<turnstile> e\<^isub>2 : Data(S\<^isub>2)\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> Pr e\<^isub>1 e\<^isub>2 : Data (DProd S\<^isub>1 S\<^isub>2)" |
|
264 | t_Fst[intro]: "\<lbrakk>\<Gamma> \<turnstile> e : Data(DProd S\<^isub>1 S\<^isub>2)\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> Fst e : Data(S\<^isub>1)" |
|
265 | t_Snd[intro]: "\<lbrakk>\<Gamma> \<turnstile> e : Data(DProd S\<^isub>1 S\<^isub>2)\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> Snd e : Data(S\<^isub>2)" |
|
266 | t_InL[intro]: "\<lbrakk>\<Gamma> \<turnstile> e : Data(S\<^isub>1)\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> InL e : Data(DSum S\<^isub>1 S\<^isub>2)" |
|
267 | t_InR[intro]: "\<lbrakk>\<Gamma> \<turnstile> e : Data(S\<^isub>2)\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> InR e : Data(DSum S\<^isub>1 S\<^isub>2)" |
|
268 | t_Case[intro]: "\<lbrakk>x\<^isub>1\<sharp>(\<Gamma>,e,e\<^isub>2,x\<^isub>2); x\<^isub>2\<sharp>(\<Gamma>,e,e\<^isub>1,x\<^isub>1); \<Gamma> \<turnstile> e: Data(DSum S\<^isub>1 S\<^isub>2); |
|
269 (x\<^isub>1,Data(S\<^isub>1))#\<Gamma> \<turnstile> e\<^isub>1 : T; (x\<^isub>2,Data(S\<^isub>2))#\<Gamma> \<turnstile> e\<^isub>2 : T\<rbrakk> |
|
270 \<Longrightarrow> \<Gamma> \<turnstile> (Case e of inl x\<^isub>1 \<rightarrow> e\<^isub>1 | inr x\<^isub>2 \<rightarrow> e\<^isub>2) : T" |
|
271 |
195 |
272 equivariance typing |
196 equivariance typing |
273 |
197 |
274 nominal_inductive typing |
198 nominal_inductive typing |
275 by (simp_all add: abs_fresh fresh_prod fresh_atm) |
199 by (simp_all add: abs_fresh fresh_ty) |
276 |
|
277 lemmas typing_eqvt' = typing.eqvt[simplified] |
|
278 |
200 |
279 lemma typing_implies_valid: |
201 lemma typing_implies_valid: |
280 assumes "\<Gamma> \<turnstile> t : T" |
202 assumes a: "\<Gamma> \<turnstile> t : T" |
281 shows "valid \<Gamma>" |
203 shows "valid \<Gamma>" |
282 using assms |
204 using a |
283 by (induct) (auto) |
205 by (induct) (auto) |
284 |
206 |
285 declare trm.inject [simp add] |
207 lemma t_Lam_elim: |
286 declare ty.inject [simp add] |
|
287 declare data.inject [simp add] |
|
288 |
|
289 |
|
290 inductive_cases typing_inv_auto[elim]: |
|
291 "\<Gamma> \<turnstile> Lam [x].t : T" |
|
292 "\<Gamma> \<turnstile> Var x : T" |
|
293 "\<Gamma> \<turnstile> App x y : T" |
|
294 "\<Gamma> \<turnstile> Const n : T" |
|
295 "\<Gamma> \<turnstile> Fst x : T" |
|
296 "\<Gamma> \<turnstile> Snd x : T" |
|
297 "\<Gamma> \<turnstile> InL x : T" |
|
298 "\<Gamma> \<turnstile> InL x : Data (DSum T\<^isub>1 T2)" |
|
299 "\<Gamma> \<turnstile> InR x : T" |
|
300 "\<Gamma> \<turnstile> InR x : Data (DSum T\<^isub>1 T2)" |
|
301 "\<Gamma> \<turnstile> Pr x y : T" |
|
302 "\<Gamma> \<turnstile> Pr e\<^isub>1 e\<^isub>2 : Data (DProd \<sigma>1 \<sigma>\<^isub>2)" |
|
303 "\<Gamma> \<turnstile> Case e of inl x\<^isub>1 \<rightarrow> e\<^isub>1 | inr x\<^isub>2 \<rightarrow> e\<^isub>2 : T" |
|
304 |
|
305 declare trm.inject [simp del] |
|
306 declare ty.inject [simp del] |
|
307 declare data.inject [simp del] |
|
308 |
|
309 lemma t_Lam_elim[elim]: |
|
310 assumes a1:"\<Gamma> \<turnstile> Lam [x].t : T" |
208 assumes a1:"\<Gamma> \<turnstile> Lam [x].t : T" |
311 and a2: "x\<sharp>\<Gamma>" |
209 and a2: "x\<sharp>\<Gamma>" |
312 obtains T\<^isub>1 and T\<^isub>2 where "(x,T\<^isub>1)#\<Gamma> \<turnstile> t : T\<^isub>2" and "T=T\<^isub>1\<rightarrow>T\<^isub>2" |
210 obtains T\<^isub>1 and T\<^isub>2 where "(x,T\<^isub>1)#\<Gamma> \<turnstile> t : T\<^isub>2" and "T=T\<^isub>1\<rightarrow>T\<^isub>2" |
313 proof - |
211 using a1 a2 |
314 from a1 obtain x' t' T\<^isub>1 T\<^isub>2 |
212 by (cases rule: typing.strong_cases [where x="x"]) |
315 where b1: "x'\<sharp>\<Gamma>" and b2: "(x',T\<^isub>1)#\<Gamma> \<turnstile> t' : T\<^isub>2" and b3: "[x'].t' = [x].t" and b4: "T=T\<^isub>1\<rightarrow>T\<^isub>2" |
213 (auto simp add: abs_fresh fresh_ty alpha trm.inject) |
316 by auto |
214 |
317 obtain c::"name" where "c\<sharp>(\<Gamma>,x,x',t,t')" by (erule exists_fresh[OF fs_name1]) |
215 abbreviation |
318 then have fs: "c\<sharp>\<Gamma>" "c\<noteq>x" "c\<noteq>x'" "c\<sharp>t" "c\<sharp>t'" by (simp_all add: fresh_atm[symmetric]) |
216 "sub_context" :: "(name\<times>ty) list \<Rightarrow> (name\<times>ty) list \<Rightarrow> bool" ("_ \<subseteq> _" [55,55] 55) |
319 then have b5: "[(x',c)]\<bullet>t'=[(x,c)]\<bullet>t" using b3 fs by (simp add: alpha_fresh) |
217 where |
320 have "([(x,c)]\<bullet>[(x',c)]\<bullet>((x',T\<^isub>1)#\<Gamma>)) \<turnstile> ([(x,c)]\<bullet>[(x',c)]\<bullet>t') : T\<^isub>2" using b2 |
218 "\<Gamma>\<^isub>1 \<subseteq> \<Gamma>\<^isub>2 \<equiv> \<forall>x T. (x,T)\<in>set \<Gamma>\<^isub>1 \<longrightarrow> (x,T)\<in>set \<Gamma>\<^isub>2" |
321 by (simp only: typing_eqvt') |
|
322 then have "(x,T\<^isub>1)#\<Gamma> \<turnstile> t : T\<^isub>2" using fs b1 a2 b5 by (perm_simp add: calc_atm) |
|
323 then show ?thesis using prems b4 by simp |
|
324 qed |
|
325 |
|
326 lemma t_Case_elim[elim]: |
|
327 assumes "\<Gamma> \<turnstile> Case e of inl x\<^isub>1 \<rightarrow> e\<^isub>1 | inr x\<^isub>2 \<rightarrow> e\<^isub>2 : T" and "x\<^isub>1\<sharp>\<Gamma>" and "x\<^isub>2\<sharp>\<Gamma>" |
|
328 obtains \<sigma>\<^isub>1 \<sigma>\<^isub>2 where "\<Gamma> \<turnstile> e : Data (DSum \<sigma>\<^isub>1 \<sigma>\<^isub>2)" |
|
329 and "(x\<^isub>1, Data \<sigma>\<^isub>1)#\<Gamma> \<turnstile> e\<^isub>1 : T" |
|
330 and "(x\<^isub>2, Data \<sigma>\<^isub>2)#\<Gamma> \<turnstile> e\<^isub>2 : T" |
|
331 proof - |
|
332 have f:"x\<^isub>1\<sharp>\<Gamma>" "x\<^isub>2\<sharp>\<Gamma>" by fact+ |
|
333 have "\<Gamma> \<turnstile> Case e of inl x\<^isub>1 \<rightarrow> e\<^isub>1 | inr x\<^isub>2 \<rightarrow> e\<^isub>2 : T" by fact |
|
334 then obtain \<sigma>\<^isub>1 \<sigma>\<^isub>2 x\<^isub>1' x\<^isub>2' e\<^isub>1' e\<^isub>2' where |
|
335 h:"\<Gamma> \<turnstile> e : Data (DSum \<sigma>\<^isub>1 \<sigma>\<^isub>2)" and |
|
336 h1:"(x\<^isub>1',Data \<sigma>\<^isub>1)#\<Gamma> \<turnstile> e\<^isub>1' : T" and |
|
337 h2:"(x\<^isub>2',Data \<sigma>\<^isub>2)#\<Gamma> \<turnstile> e\<^isub>2' : T" and |
|
338 e1:"[x\<^isub>1].e\<^isub>1=[x\<^isub>1'].e\<^isub>1'" and e2:"[x\<^isub>2].e\<^isub>2=[x\<^isub>2'].e\<^isub>2'" |
|
339 by auto |
|
340 obtain c::name where f':"c \<sharp> (x\<^isub>1,x\<^isub>1',e\<^isub>1,e\<^isub>1',\<Gamma>)" by (erule exists_fresh[OF fs_name1]) |
|
341 have e1':"[(x\<^isub>1,c)]\<bullet>e\<^isub>1 = [(x\<^isub>1',c)]\<bullet>e\<^isub>1'" using e1 f' by (auto simp add: alpha_fresh fresh_prod fresh_atm) |
|
342 have "[(x\<^isub>1',c)]\<bullet>((x\<^isub>1',Data \<sigma>\<^isub>1)# \<Gamma>) \<turnstile> [(x\<^isub>1',c)]\<bullet>e\<^isub>1' : T" using h1 typing_eqvt' by blast |
|
343 then have x:"(c,Data \<sigma>\<^isub>1)#( [(x\<^isub>1',c)]\<bullet>\<Gamma>) \<turnstile> [(x\<^isub>1',c)]\<bullet>e\<^isub>1': T" using f' |
|
344 by (auto simp add: fresh_atm calc_atm) |
|
345 have "x\<^isub>1' \<sharp> \<Gamma>" using h1 typing_implies_valid by auto |
|
346 then have "(c,Data \<sigma>\<^isub>1)#\<Gamma> \<turnstile> [(x\<^isub>1 ,c)]\<bullet>e\<^isub>1 : T" using f' x e1' by (auto simp add: perm_fresh_fresh) |
|
347 then have "[(x\<^isub>1,c)]\<bullet>((c,Data \<sigma>\<^isub>1)#\<Gamma>) \<turnstile> [(x\<^isub>1,c)]\<bullet>[(x\<^isub>1 ,c)]\<bullet>e\<^isub>1 : T" using typing_eqvt' by blast |
|
348 then have "([(x\<^isub>1,c)]\<bullet>(c,Data \<sigma>\<^isub>1)) #\<Gamma> \<turnstile> [(x\<^isub>1,c)]\<bullet>[(x\<^isub>1 ,c)]\<bullet>e\<^isub>1 : T" using f f' |
|
349 by (auto simp add: perm_fresh_fresh) |
|
350 then have "([(x\<^isub>1,c)]\<bullet>(c,Data \<sigma>\<^isub>1)) #\<Gamma> \<turnstile> e\<^isub>1 : T" by perm_simp |
|
351 then have g1:"(x\<^isub>1, Data \<sigma>\<^isub>1)#\<Gamma> \<turnstile> e\<^isub>1 : T" using f' by (auto simp add: fresh_atm calc_atm fresh_prod) |
|
352 (* The second part of the proof is the same *) |
|
353 obtain c::name where f':"c \<sharp> (x\<^isub>2,x\<^isub>2',e\<^isub>2,e\<^isub>2',\<Gamma>)" by (erule exists_fresh[OF fs_name1]) |
|
354 have e2':"[(x\<^isub>2,c)]\<bullet>e\<^isub>2 = [(x\<^isub>2',c)]\<bullet>e\<^isub>2'" using e2 f' by (auto simp add: alpha_fresh fresh_prod fresh_atm) |
|
355 have "[(x\<^isub>2',c)]\<bullet>((x\<^isub>2',Data \<sigma>\<^isub>2)# \<Gamma>) \<turnstile> [(x\<^isub>2',c)]\<bullet>e\<^isub>2' : T" using h2 typing_eqvt' by blast |
|
356 then have x:"(c,Data \<sigma>\<^isub>2)#([(x\<^isub>2',c)]\<bullet>\<Gamma>) \<turnstile> [(x\<^isub>2',c)]\<bullet>e\<^isub>2': T" using f' |
|
357 by (auto simp add: fresh_atm calc_atm) |
|
358 have "x\<^isub>2' \<sharp> \<Gamma>" using h2 typing_implies_valid by auto |
|
359 then have "(c,Data \<sigma>\<^isub>2)#\<Gamma> \<turnstile> [(x\<^isub>2 ,c)]\<bullet>e\<^isub>2 : T" using f' x e2' by (auto simp add: perm_fresh_fresh) |
|
360 then have "[(x\<^isub>2,c)]\<bullet>((c,Data \<sigma>\<^isub>2)#\<Gamma>) \<turnstile> [(x\<^isub>2,c)]\<bullet>[(x\<^isub>2 ,c)]\<bullet>e\<^isub>2 : T" using typing_eqvt' by blast |
|
361 then have "([(x\<^isub>2,c)]\<bullet>(c,Data \<sigma>\<^isub>2))#\<Gamma> \<turnstile> [(x\<^isub>2,c)]\<bullet>[(x\<^isub>2 ,c)]\<bullet>e\<^isub>2 : T" using f f' |
|
362 by (auto simp add: perm_fresh_fresh) |
|
363 then have "([(x\<^isub>2,c)]\<bullet>(c,Data \<sigma>\<^isub>2)) #\<Gamma> \<turnstile> e\<^isub>2 : T" by perm_simp |
|
364 then have g2:"(x\<^isub>2,Data \<sigma>\<^isub>2)#\<Gamma> \<turnstile> e\<^isub>2 : T" using f' by (auto simp add: fresh_atm calc_atm fresh_prod) |
|
365 show ?thesis using g1 g2 prems by auto |
|
366 qed |
|
367 |
219 |
368 lemma weakening: |
220 lemma weakening: |
369 fixes \<Gamma>\<^isub>1 \<Gamma>\<^isub>2 :: "(name\<times>ty) list" |
221 fixes \<Gamma>\<^isub>1 \<Gamma>\<^isub>2::"(name\<times>ty) list" |
370 assumes "\<Gamma>\<^isub>1 \<turnstile> e: T" and "valid \<Gamma>\<^isub>2" and "\<Gamma>\<^isub>1 \<subseteq> \<Gamma>\<^isub>2" |
222 assumes "\<Gamma>\<^isub>1 \<turnstile> e: T" and "valid \<Gamma>\<^isub>2" and "\<Gamma>\<^isub>1 \<subseteq> \<Gamma>\<^isub>2" |
371 shows "\<Gamma>\<^isub>2 \<turnstile> e: T" |
223 shows "\<Gamma>\<^isub>2 \<turnstile> e: T" |
372 using assms |
224 using assms |
373 proof(nominal_induct \<Gamma>\<^isub>1 e T avoiding: \<Gamma>\<^isub>2 rule: typing.strong_induct) |
225 proof(nominal_induct \<Gamma>\<^isub>1 e T avoiding: \<Gamma>\<^isub>2 rule: typing.strong_induct) |
374 case (t_Lam x \<Gamma>\<^isub>1 T\<^isub>1 t T\<^isub>2 \<Gamma>\<^isub>2) |
226 case (t_Lam x \<Gamma>\<^isub>1 T\<^isub>1 t T\<^isub>2 \<Gamma>\<^isub>2) |
|
227 have vc: "x\<sharp>\<Gamma>\<^isub>2" by fact |
375 have ih: "\<lbrakk>valid ((x,T\<^isub>1)#\<Gamma>\<^isub>2); (x,T\<^isub>1)#\<Gamma>\<^isub>1 \<subseteq> (x,T\<^isub>1)#\<Gamma>\<^isub>2\<rbrakk> \<Longrightarrow> (x,T\<^isub>1)#\<Gamma>\<^isub>2 \<turnstile> t : T\<^isub>2" by fact |
228 have ih: "\<lbrakk>valid ((x,T\<^isub>1)#\<Gamma>\<^isub>2); (x,T\<^isub>1)#\<Gamma>\<^isub>1 \<subseteq> (x,T\<^isub>1)#\<Gamma>\<^isub>2\<rbrakk> \<Longrightarrow> (x,T\<^isub>1)#\<Gamma>\<^isub>2 \<turnstile> t : T\<^isub>2" by fact |
376 have H1: "valid \<Gamma>\<^isub>2" by fact |
229 have "valid \<Gamma>\<^isub>2" by fact |
377 have H2: "\<Gamma>\<^isub>1 \<subseteq> \<Gamma>\<^isub>2" by fact |
230 then have "valid ((x,T\<^isub>1)#\<Gamma>\<^isub>2)" using vc by auto |
378 have fs: "x\<sharp>\<Gamma>\<^isub>2" by fact |
231 moreover |
379 then have "valid ((x,T\<^isub>1)#\<Gamma>\<^isub>2)" using H1 by auto |
232 have "\<Gamma>\<^isub>1 \<subseteq> \<Gamma>\<^isub>2" by fact |
380 moreover have "(x,T\<^isub>1)#\<Gamma>\<^isub>1 \<subseteq> (x,T\<^isub>1)#\<Gamma>\<^isub>2" using H2 by auto |
233 then have "(x,T\<^isub>1)#\<Gamma>\<^isub>1 \<subseteq> (x,T\<^isub>1)#\<Gamma>\<^isub>2" by simp |
381 ultimately have "(x,T\<^isub>1)#\<Gamma>\<^isub>2 \<turnstile> t : T\<^isub>2" using ih by simp |
234 ultimately have "(x,T\<^isub>1)#\<Gamma>\<^isub>2 \<turnstile> t : T\<^isub>2" using ih by simp |
382 thus "\<Gamma>\<^isub>2 \<turnstile> Lam [x].t : T\<^isub>1\<rightarrow>T\<^isub>2" using fs by auto |
235 with vc show "\<Gamma>\<^isub>2 \<turnstile> Lam [x].t : T\<^isub>1\<rightarrow>T\<^isub>2" by auto |
383 next |
|
384 case (t_Case x\<^isub>1 \<Gamma>\<^isub>1 e e\<^isub>2 x\<^isub>2 e\<^isub>1 S\<^isub>1 S\<^isub>2 T \<Gamma>\<^isub>2) |
|
385 then have ih\<^isub>1: "valid ((x\<^isub>1,Data S\<^isub>1)#\<Gamma>\<^isub>2) \<Longrightarrow> (x\<^isub>1,Data S\<^isub>1)#\<Gamma>\<^isub>2 \<turnstile> e\<^isub>1 : T" |
|
386 and ih\<^isub>2: "valid ((x\<^isub>2,Data S\<^isub>2)#\<Gamma>\<^isub>2) \<Longrightarrow> (x\<^isub>2,Data S\<^isub>2)#\<Gamma>\<^isub>2 \<turnstile> e\<^isub>2 : T" |
|
387 and ih\<^isub>3: "\<Gamma>\<^isub>2 \<turnstile> e : Data (DSum S\<^isub>1 S\<^isub>2)" by auto |
|
388 have fs\<^isub>1: "x\<^isub>1\<sharp>\<Gamma>\<^isub>2" "x\<^isub>1\<sharp>e" "x\<^isub>1\<sharp>e\<^isub>2" "x\<^isub>1\<sharp>x\<^isub>2" by fact+ |
|
389 have fs\<^isub>2: "x\<^isub>2\<sharp>\<Gamma>\<^isub>2" "x\<^isub>2\<sharp>e" "x\<^isub>2\<sharp>e\<^isub>1" "x\<^isub>2\<sharp>x\<^isub>1" by fact+ |
|
390 have "valid \<Gamma>\<^isub>2" by fact |
|
391 then have "valid ((x\<^isub>1,Data S\<^isub>1)#\<Gamma>\<^isub>2)" and "valid ((x\<^isub>2,Data S\<^isub>2)#\<Gamma>\<^isub>2)" using fs\<^isub>1 fs\<^isub>2 by auto |
|
392 then have "(x\<^isub>1, Data S\<^isub>1)#\<Gamma>\<^isub>2 \<turnstile> e\<^isub>1 : T" and "(x\<^isub>2, Data S\<^isub>2)#\<Gamma>\<^isub>2 \<turnstile> e\<^isub>2 : T" using ih\<^isub>1 ih\<^isub>2 by simp_all |
|
393 with ih\<^isub>3 show "\<Gamma>\<^isub>2 \<turnstile> Case e of inl x\<^isub>1 \<rightarrow> e\<^isub>1 | inr x\<^isub>2 \<rightarrow> e\<^isub>2 : T" using fs\<^isub>1 fs\<^isub>2 by auto |
|
394 qed (auto) |
236 qed (auto) |
395 |
237 |
396 lemma context_exchange: |
238 lemma context_exchange: |
397 assumes a: "(x\<^isub>1,T\<^isub>1)#(x\<^isub>2,T\<^isub>2)#\<Gamma> \<turnstile> e : T" |
239 assumes a: "(x\<^isub>1,T\<^isub>1)#(x\<^isub>2,T\<^isub>2)#\<Gamma> \<turnstile> e : T" |
398 shows "(x\<^isub>2,T\<^isub>2)#(x\<^isub>1,T\<^isub>1)#\<Gamma> \<turnstile> e : T" |
240 shows "(x\<^isub>2,T\<^isub>2)#(x\<^isub>1,T\<^isub>1)#\<Gamma> \<turnstile> e : T" |
399 proof - |
241 proof - |
400 from a have "valid ((x\<^isub>1,T\<^isub>1)#(x\<^isub>2,T\<^isub>2)#\<Gamma>)" by (simp add: typing_implies_valid) |
242 from a have "valid ((x\<^isub>1,T\<^isub>1)#(x\<^isub>2,T\<^isub>2)#\<Gamma>)" by (simp add: typing_implies_valid) |
401 then have "x\<^isub>1\<noteq>x\<^isub>2" "x\<^isub>1\<sharp>\<Gamma>" "x\<^isub>2\<sharp>\<Gamma>" "valid \<Gamma>" |
243 then have "x\<^isub>1\<noteq>x\<^isub>2" "x\<^isub>1\<sharp>\<Gamma>" "x\<^isub>2\<sharp>\<Gamma>" "valid \<Gamma>" |
402 by (auto simp: fresh_list_cons fresh_atm[symmetric]) |
244 by (auto simp: fresh_list_cons fresh_atm[symmetric]) |
403 then have "valid ((x\<^isub>2,T\<^isub>2)#(x\<^isub>1,T\<^isub>1)#\<Gamma>)" |
245 then have "valid ((x\<^isub>2,T\<^isub>2)#(x\<^isub>1,T\<^isub>1)#\<Gamma>)" |
404 by (auto simp: fresh_list_cons fresh_atm) |
246 by (auto simp: fresh_list_cons fresh_atm fresh_ty) |
405 moreover |
247 moreover |
406 have "(x\<^isub>1,T\<^isub>1)#(x\<^isub>2,T\<^isub>2)#\<Gamma> \<subseteq> (x\<^isub>2,T\<^isub>2)#(x\<^isub>1,T\<^isub>1)#\<Gamma>" by auto |
248 have "(x\<^isub>1,T\<^isub>1)#(x\<^isub>2,T\<^isub>2)#\<Gamma> \<subseteq> (x\<^isub>2,T\<^isub>2)#(x\<^isub>1,T\<^isub>1)#\<Gamma>" by auto |
407 ultimately show "(x\<^isub>2,T\<^isub>2)#(x\<^isub>1,T\<^isub>1)#\<Gamma> \<turnstile> e : T" using a by (auto intro: weakening) |
249 ultimately show "(x\<^isub>2,T\<^isub>2)#(x\<^isub>1,T\<^isub>1)#\<Gamma> \<turnstile> e : T" using a by (auto intro: weakening) |
408 qed |
250 qed |
409 |
251 |
410 lemma typing_var_unicity: |
252 lemma typing_var_unicity: |
411 assumes "(x,t\<^isub>1)#\<Gamma> \<turnstile> Var x : t\<^isub>2" |
253 assumes a: "(x,T\<^isub>1)#\<Gamma> \<turnstile> Var x : T\<^isub>2" |
412 shows "t\<^isub>1=t\<^isub>2" |
254 shows "T\<^isub>1=T\<^isub>2" |
413 proof - |
255 proof - |
414 have "(x,t\<^isub>2) \<in> set ((x,t\<^isub>1)#\<Gamma>)" and "valid ((x,t\<^isub>1)#\<Gamma>)" using assms by auto |
256 have "(x,T\<^isub>2) \<in> set ((x,T\<^isub>1)#\<Gamma>)" using a |
415 thus "t\<^isub>1=t\<^isub>2" by (simp only: type_unicity_in_context) |
257 by (cases) (auto simp add: trm.inject) |
|
258 moreover |
|
259 have "valid ((x,T\<^isub>1)#\<Gamma>)" using a by (simp add: typing_implies_valid) |
|
260 ultimately show "T\<^isub>1=T\<^isub>2" by (simp only: type_unicity_in_context) |
416 qed |
261 qed |
417 |
262 |
418 lemma typing_substitution: |
263 lemma typing_substitution: |
419 fixes \<Gamma>::"(name \<times> ty) list" |
264 fixes \<Gamma>::"(name \<times> ty) list" |
420 assumes "(x,T')#\<Gamma> \<turnstile> e : T" |
265 assumes "(x,T')#\<Gamma> \<turnstile> e : T" |
432 then have "T=T'" using h1 typing_var_unicity by auto |
277 then have "T=T'" using h1 typing_var_unicity by auto |
433 then show "\<Gamma> \<turnstile> (Var y)[x::=e'] : T" using as h2 by simp |
278 then show "\<Gamma> \<turnstile> (Var y)[x::=e'] : T" using as h2 by simp |
434 next |
279 next |
435 case False |
280 case False |
436 assume as: "x\<noteq>y" |
281 assume as: "x\<noteq>y" |
437 have "(y,T) \<in> set ((x,T')#\<Gamma>)" using h1 by auto |
282 have "(y,T) \<in> set ((x,T')#\<Gamma>)" using h1 by (cases) (auto simp add: trm.inject) |
438 then have "(y,T) \<in> set \<Gamma>" using as by auto |
283 then have "(y,T) \<in> set \<Gamma>" using as by auto |
439 moreover |
284 moreover |
440 have "valid \<Gamma>" using h2 by (simp only: typing_implies_valid) |
285 have "valid \<Gamma>" using h2 by (simp only: typing_implies_valid) |
441 ultimately show "\<Gamma> \<turnstile> (Var y)[x::=e'] : T" using as by (simp add: t_Var) |
286 ultimately show "\<Gamma> \<turnstile> (Var y)[x::=e'] : T" using as by (simp add: t_Var) |
442 qed |
287 qed |
443 next |
288 next |
444 case (Lam y t \<Gamma> e' x T) |
289 case (Lam y t \<Gamma> e' x T) |
445 have vc: "y\<sharp>\<Gamma>" "y\<sharp>x" "y\<sharp>e'" by fact+ |
290 have vc: "y\<sharp>\<Gamma>" "y\<sharp>x" "y\<sharp>e'" by fact |
446 have pr1: "\<Gamma> \<turnstile> e' : T'" by fact |
291 have pr1: "\<Gamma> \<turnstile> e' : T'" by fact |
447 have pr2: "(x,T')#\<Gamma> \<turnstile> Lam [y].t : T" by fact |
292 have pr2: "(x,T')#\<Gamma> \<turnstile> Lam [y].t : T" by fact |
448 then obtain T\<^isub>1 T\<^isub>2 where pr2': "(y,T\<^isub>1)#(x,T')#\<Gamma> \<turnstile> t : T\<^isub>2" and eq: "T = T\<^isub>1\<rightarrow>T\<^isub>2" |
293 then obtain T\<^isub>1 T\<^isub>2 where pr2': "(y,T\<^isub>1)#(x,T')#\<Gamma> \<turnstile> t : T\<^isub>2" and eq: "T = T\<^isub>1\<rightarrow>T\<^isub>2" |
449 using vc by (auto simp add: fresh_list_cons) |
294 using vc by (auto elim: t_Lam_elim simp add: fresh_list_cons fresh_ty) |
450 then have pr2'':"(x,T')#(y,T\<^isub>1)#\<Gamma> \<turnstile> t : T\<^isub>2" by (simp add: context_exchange) |
295 then have pr2'':"(x,T')#(y,T\<^isub>1)#\<Gamma> \<turnstile> t : T\<^isub>2" by (simp add: context_exchange) |
451 have ih: "\<lbrakk>(x,T')#(y,T\<^isub>1)#\<Gamma> \<turnstile> t : T\<^isub>2; (y,T\<^isub>1)#\<Gamma> \<turnstile> e' : T'\<rbrakk> \<Longrightarrow> (y,T\<^isub>1)#\<Gamma> \<turnstile> t[x::=e'] : T\<^isub>2" by fact |
296 have ih: "\<lbrakk>(x,T')#(y,T\<^isub>1)#\<Gamma> \<turnstile> t : T\<^isub>2; (y,T\<^isub>1)#\<Gamma> \<turnstile> e' : T'\<rbrakk> \<Longrightarrow> (y,T\<^isub>1)#\<Gamma> \<turnstile> t[x::=e'] : T\<^isub>2" by fact |
452 have "valid \<Gamma>" using pr1 by (simp add: typing_implies_valid) |
297 have "valid \<Gamma>" using pr1 by (simp add: typing_implies_valid) |
453 then have "valid ((y,T\<^isub>1)#\<Gamma>)" using vc by auto |
298 then have "valid ((y,T\<^isub>1)#\<Gamma>)" using vc by auto |
454 then have "(y,T\<^isub>1)#\<Gamma> \<turnstile> e' : T'" using pr1 by (auto intro: weakening) |
299 then have "(y,T\<^isub>1)#\<Gamma> \<turnstile> e' : T'" using pr1 by (simp add: weakening) |
455 then have "(y,T\<^isub>1)#\<Gamma> \<turnstile> t[x::=e'] : T\<^isub>2" using ih pr2'' by simp |
300 then have "(y,T\<^isub>1)#\<Gamma> \<turnstile> t[x::=e'] : T\<^isub>2" using ih pr2'' by simp |
456 then have "\<Gamma> \<turnstile> Lam [y].(t[x::=e']) : T\<^isub>1\<rightarrow>T\<^isub>2" using vc by (auto intro: t_Lam) |
301 then have "\<Gamma> \<turnstile> Lam [y].(t[x::=e']) : T\<^isub>1\<rightarrow>T\<^isub>2" using vc by auto |
457 thus "\<Gamma> \<turnstile> (Lam [y].t)[x::=e'] : T" using vc eq by simp |
302 then show "\<Gamma> \<turnstile> (Lam [y].t)[x::=e'] : T" using vc eq by simp |
458 next |
303 next |
459 case (Case t\<^isub>1 x\<^isub>1 t\<^isub>2 x\<^isub>2 t3 \<Gamma> e' x T) |
304 case (App e1 e2 \<Gamma> e' x T) |
460 have vc: "x\<^isub>1\<sharp>\<Gamma>" "x\<^isub>1\<sharp>e'" "x\<^isub>1\<sharp>x""x\<^isub>1\<sharp>t\<^isub>1" "x\<^isub>1\<sharp>t3" "x\<^isub>2\<sharp>\<Gamma>" |
305 have "(x,T')#\<Gamma> \<turnstile> App e1 e2 : T" by fact |
461 "x\<^isub>2\<sharp>e'" "x\<^isub>2\<sharp>x" "x\<^isub>2\<sharp>t\<^isub>1" "x\<^isub>2\<sharp>t\<^isub>2" "x\<^isub>2\<noteq>x\<^isub>1" by fact+ |
306 then obtain Tn where a1: "(x,T')#\<Gamma> \<turnstile> e1 : Tn \<rightarrow> T" |
462 have as1: "\<Gamma> \<turnstile> e' : T'" by fact |
307 and a2: "(x,T')#\<Gamma> \<turnstile> e2 : Tn" |
463 have as2: "(x,T')#\<Gamma> \<turnstile> Case t\<^isub>1 of inl x\<^isub>1 \<rightarrow> t\<^isub>2 | inr x\<^isub>2 \<rightarrow> t3 : T" by fact |
308 by (cases) (auto simp add: trm.inject) |
464 then obtain S\<^isub>1 S\<^isub>2 where |
309 have a3: "\<Gamma> \<turnstile> e' : T'" by fact |
465 h1:"(x,T')#\<Gamma> \<turnstile> t\<^isub>1 : Data (DSum S\<^isub>1 S\<^isub>2)" and |
310 have ih1: "\<lbrakk>(x,T')#\<Gamma> \<turnstile> e1 : Tn\<rightarrow>T; \<Gamma> \<turnstile> e' : T'\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> e1[x::=e'] : Tn\<rightarrow>T" by fact |
466 h2:"(x\<^isub>1,Data S\<^isub>1)#(x,T')#\<Gamma> \<turnstile> t\<^isub>2 : T" and |
311 have ih2: "\<lbrakk>(x,T')#\<Gamma> \<turnstile> e2 : Tn; \<Gamma> \<turnstile> e' : T'\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> e2[x::=e'] : Tn" by fact |
467 h3:"(x\<^isub>2,Data S\<^isub>2)#(x,T')#\<Gamma> \<turnstile> t3 : T" |
312 then show ?case using a1 a2 a3 ih1 ih2 by auto |
468 using vc by (auto simp add: fresh_list_cons) |
313 qed |
469 have ih1: "\<lbrakk>(x,T')#\<Gamma> \<turnstile> t\<^isub>1 : Data (DSum S\<^isub>1 S\<^isub>2); \<Gamma> \<turnstile> e' : T'\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> t\<^isub>1[x::=e'] : Data (DSum S\<^isub>1 S\<^isub>2)" |
314 |
470 and ih2: "\<lbrakk>(x,T')#(x\<^isub>1,Data S\<^isub>1)#\<Gamma> \<turnstile> t\<^isub>2:T; (x\<^isub>1,Data S\<^isub>1)#\<Gamma> \<turnstile> e':T'\<rbrakk> \<Longrightarrow> (x\<^isub>1,Data S\<^isub>1)#\<Gamma> \<turnstile> t\<^isub>2[x::=e']:T" |
315 text {* Values *} |
471 and ih3: "\<lbrakk>(x,T')#(x\<^isub>2,Data S\<^isub>2)#\<Gamma> \<turnstile> t3:T; (x\<^isub>2,Data S\<^isub>2)#\<Gamma> \<turnstile> e':T'\<rbrakk> \<Longrightarrow> (x\<^isub>2,Data S\<^isub>2)#\<Gamma> \<turnstile> t3[x::=e']:T" |
316 inductive |
472 by fact+ |
317 val :: "trm\<Rightarrow>bool" |
473 from h2 have h2': "(x,T')#(x\<^isub>1,Data S\<^isub>1)#\<Gamma> \<turnstile> t\<^isub>2 : T" by (rule context_exchange) |
318 where |
474 from h3 have h3': "(x,T')#(x\<^isub>2,Data S\<^isub>2)#\<Gamma> \<turnstile> t3 : T" by (rule context_exchange) |
319 v_Lam[intro]: "val (Lam [x].e)" |
475 have "\<Gamma> \<turnstile> t\<^isub>1[x::=e'] : Data (DSum S\<^isub>1 S\<^isub>2)" using h1 ih1 as1 by simp |
320 |
476 moreover |
321 equivariance val |
477 have "valid ((x\<^isub>1,Data S\<^isub>1)#\<Gamma>)" using h2' by (auto dest: typing_implies_valid) |
322 |
478 then have "(x\<^isub>1,Data S\<^isub>1)#\<Gamma> \<turnstile> e' : T'" using as1 by (auto simp add: weakening) |
323 lemma not_val_App[simp]: |
479 then have "(x\<^isub>1,Data S\<^isub>1)#\<Gamma> \<turnstile> t\<^isub>2[x::=e'] : T" using ih2 h2' by simp |
324 shows |
480 moreover |
325 "\<not> val (App e\<^isub>1 e\<^isub>2)" |
481 have "valid ((x\<^isub>2,Data S\<^isub>2)#\<Gamma>)" using h3' by (auto dest: typing_implies_valid) |
326 "\<not> val (Var x)" |
482 then have "(x\<^isub>2,Data S\<^isub>2)#\<Gamma> \<turnstile> e' : T'" using as1 by (auto simp add: weakening) |
327 by (auto elim: val.cases) |
483 then have "(x\<^isub>2,Data S\<^isub>2)#\<Gamma> \<turnstile> t3[x::=e'] : T" using ih3 h3' by simp |
|
484 ultimately have "\<Gamma> \<turnstile> Case (t\<^isub>1[x::=e']) of inl x\<^isub>1 \<rightarrow> (t\<^isub>2[x::=e']) | inr x\<^isub>2 \<rightarrow> (t3[x::=e']) : T" |
|
485 using vc by (auto simp add: fresh_atm fresh_subst) |
|
486 thus "\<Gamma> \<turnstile> (Case t\<^isub>1 of inl x\<^isub>1 \<rightarrow> t\<^isub>2 | inr x\<^isub>2 \<rightarrow> t3)[x::=e'] : T" using vc by simp |
|
487 qed (simp, fast)+ |
|
488 |
328 |
489 text {* Big-Step Evaluation *} |
329 text {* Big-Step Evaluation *} |
490 |
330 |
491 inductive |
331 inductive |
492 big :: "trm\<Rightarrow>trm\<Rightarrow>bool" ("_ \<Down> _" [80,80] 80) |
332 big :: "trm\<Rightarrow>trm\<Rightarrow>bool" ("_ \<Down> _" [80,80] 80) |
493 where |
333 where |
494 b_Lam[intro]: "Lam [x].e \<Down> Lam [x].e" |
334 b_Lam[intro]: "Lam [x].e \<Down> Lam [x].e" |
495 | b_App[intro]: "\<lbrakk>x\<sharp>(e\<^isub>1,e\<^isub>2,e'); e\<^isub>1\<Down>Lam [x].e; e\<^isub>2\<Down>e\<^isub>2'; e[x::=e\<^isub>2']\<Down>e'\<rbrakk> \<Longrightarrow> App e\<^isub>1 e\<^isub>2 \<Down> e'" |
335 | b_App[intro]: "\<lbrakk>x\<sharp>(e\<^isub>1,e\<^isub>2,e'); e\<^isub>1\<Down>Lam [x].e; e\<^isub>2\<Down>e\<^isub>2'; e[x::=e\<^isub>2']\<Down>e'\<rbrakk> \<Longrightarrow> App e\<^isub>1 e\<^isub>2 \<Down> e'" |
496 | b_Const[intro]: "Const n \<Down> Const n" |
|
497 | b_Pr[intro]: "\<lbrakk>e\<^isub>1\<Down>e\<^isub>1'; e\<^isub>2\<Down>e\<^isub>2'\<rbrakk> \<Longrightarrow> Pr e\<^isub>1 e\<^isub>2 \<Down> Pr e\<^isub>1' e\<^isub>2'" |
|
498 | b_Fst[intro]: "e\<Down>Pr e\<^isub>1 e\<^isub>2 \<Longrightarrow> Fst e\<Down>e\<^isub>1" |
|
499 | b_Snd[intro]: "e\<Down>Pr e\<^isub>1 e\<^isub>2 \<Longrightarrow> Snd e\<Down>e\<^isub>2" |
|
500 | b_InL[intro]: "e\<Down>e' \<Longrightarrow> InL e \<Down> InL e'" |
|
501 | b_InR[intro]: "e\<Down>e' \<Longrightarrow> InR e \<Down> InR e'" |
|
502 | b_CaseL[intro]: "\<lbrakk>x\<^isub>1\<sharp>(e,e\<^isub>2,e'',x\<^isub>2); x\<^isub>2\<sharp>(e,e\<^isub>1,e'',x\<^isub>1) ; e\<Down>InL e'; e\<^isub>1[x\<^isub>1::=e']\<Down>e''\<rbrakk> |
|
503 \<Longrightarrow> Case e of inl x\<^isub>1 \<rightarrow> e\<^isub>1 | inr x\<^isub>2 \<rightarrow> e\<^isub>2 \<Down> e''" |
|
504 | b_CaseR[intro]: "\<lbrakk>x\<^isub>1\<sharp>(e,e\<^isub>2,e'',x\<^isub>2); x\<^isub>2\<sharp>(e,e\<^isub>1,e'',x\<^isub>1) ; e\<Down>InR e'; e\<^isub>2[x\<^isub>2::=e']\<Down>e''\<rbrakk> |
|
505 \<Longrightarrow> Case e of inl x\<^isub>1 \<rightarrow> e\<^isub>1 | inr x\<^isub>2 \<rightarrow> e\<^isub>2 \<Down> e''" |
|
506 |
336 |
507 equivariance big |
337 equivariance big |
508 |
338 |
509 nominal_inductive big |
339 nominal_inductive big |
510 by (simp_all add: abs_fresh fresh_prod fresh_atm) |
340 by (simp_all add: abs_fresh) |
511 |
341 |
512 lemma big_eqvt': |
342 lemma big_preserves_fresh: |
513 fixes pi::"name prm" |
343 fixes x::"name" |
514 assumes a: "(pi\<bullet>t) \<Down> (pi\<bullet>t')" |
344 assumes a: "e \<Down> e'" "x\<sharp>e" |
515 shows "t \<Down> t'" |
|
516 using a |
|
517 apply - |
|
518 apply(drule_tac pi="rev pi" in big.eqvt) |
|
519 apply(perm_simp) |
|
520 done |
|
521 |
|
522 lemma fresh_preserved: |
|
523 fixes x::name |
|
524 fixes t::trm |
|
525 fixes t'::trm |
|
526 assumes "e \<Down> e'" and "x\<sharp>e" |
|
527 shows "x\<sharp>e'" |
345 shows "x\<sharp>e'" |
528 using assms by (induct) (auto simp add:fresh_subst') |
346 using a by (induct) (auto simp add: abs_fresh fresh_subst) |
529 |
347 |
530 declare trm.inject [simp add] |
348 lemma b_App_elim: |
531 declare ty.inject [simp add] |
349 assumes a: "App e\<^isub>1 e\<^isub>2 \<Down> e'" "x\<sharp>(e\<^isub>1,e\<^isub>2,e')" |
532 declare data.inject [simp add] |
|
533 |
|
534 inductive_cases b_inv_auto[elim]: |
|
535 "App e\<^isub>1 e\<^isub>2 \<Down> t" |
|
536 "Case e of inl x\<^isub>1 \<rightarrow> e\<^isub>1 | inr x\<^isub>2 \<rightarrow> e\<^isub>2 \<Down> t" |
|
537 "Lam[x].t \<Down> t" |
|
538 "Const n \<Down> t" |
|
539 "Fst e \<Down> t" |
|
540 "Snd e \<Down> t" |
|
541 "InL e \<Down> t" |
|
542 "InR e \<Down> t" |
|
543 "Pr e\<^isub>1 e\<^isub>2 \<Down> t" |
|
544 |
|
545 declare trm.inject [simp del] |
|
546 declare ty.inject [simp del] |
|
547 declare data.inject [simp del] |
|
548 |
|
549 lemma b_App_elim[elim]: |
|
550 assumes "App e\<^isub>1 e\<^isub>2 \<Down> e'" and "x\<sharp>(e\<^isub>1,e\<^isub>2,e')" |
|
551 obtains f\<^isub>1 and f\<^isub>2 where "e\<^isub>1 \<Down> Lam [x]. f\<^isub>1" "e\<^isub>2 \<Down> f\<^isub>2" "f\<^isub>1[x::=f\<^isub>2] \<Down> e'" |
350 obtains f\<^isub>1 and f\<^isub>2 where "e\<^isub>1 \<Down> Lam [x]. f\<^isub>1" "e\<^isub>2 \<Down> f\<^isub>2" "f\<^isub>1[x::=f\<^isub>2] \<Down> e'" |
552 using assms |
351 using a |
553 apply - |
352 by (cases rule: big.strong_cases[where x="x" and xa="x"]) |
554 apply(erule b_inv_auto) |
353 (auto simp add: trm.inject) |
555 apply(drule_tac pi="[(xa,x)]" in big.eqvt) |
|
556 apply(drule_tac pi="[(xa,x)]" in big.eqvt) |
|
557 apply(drule_tac pi="[(xa,x)]" in big.eqvt) |
|
558 apply(perm_simp add: calc_atm eqvts) |
|
559 done |
|
560 |
|
561 lemma b_CaseL_elim[elim]: |
|
562 assumes "Case e of inl x\<^isub>1 \<rightarrow> e\<^isub>1 | inr x\<^isub>2 \<rightarrow> e\<^isub>2 \<Down> e''" |
|
563 and "\<And> t. \<not> e \<Down> InR t" |
|
564 and "x\<^isub>1\<sharp>e''" "x\<^isub>1\<sharp>e" "x\<^isub>2\<sharp>e''" "x\<^isub>1\<sharp>e" |
|
565 obtains e' where "e \<Down> InL e'" and "e\<^isub>1[x\<^isub>1::=e'] \<Down> e''" |
|
566 using assms |
|
567 apply - |
|
568 apply(rule b_inv_auto(2)) |
|
569 apply(auto) |
|
570 apply(simp add: alpha) |
|
571 apply(auto) |
|
572 apply(drule_tac x="[(x\<^isub>1,x\<^isub>1')]\<bullet>e'" in meta_spec) |
|
573 apply(drule meta_mp) |
|
574 apply(rule_tac pi="[(x\<^isub>1,x\<^isub>1')]" in big_eqvt') |
|
575 apply(perm_simp add: fresh_prod) |
|
576 apply(drule meta_mp) |
|
577 apply(rule_tac pi="[(x\<^isub>1,x\<^isub>1')]" in big_eqvt') |
|
578 apply(perm_simp add: eqvts calc_atm) |
|
579 apply(assumption) |
|
580 apply(drule_tac x="[(x\<^isub>1,x\<^isub>1')]\<bullet>e'" in meta_spec) |
|
581 apply(drule meta_mp) |
|
582 apply(rule_tac pi="[(x\<^isub>1,x\<^isub>1')]" in big_eqvt') |
|
583 apply(perm_simp add: fresh_prod) |
|
584 apply(drule meta_mp) |
|
585 apply(rule_tac pi="[(x\<^isub>1,x\<^isub>1')]" in big_eqvt') |
|
586 apply(perm_simp add: eqvts calc_atm) |
|
587 apply(assumption) |
|
588 done |
|
589 |
|
590 lemma b_CaseR_elim[elim]: |
|
591 assumes "Case e of inl x\<^isub>1 \<rightarrow> e\<^isub>1 | inr x\<^isub>2 \<rightarrow> e\<^isub>2 \<Down> e''" |
|
592 and "\<And> t. \<not> e \<Down> InL t" |
|
593 and "x\<^isub>1\<sharp>e''" "x\<^isub>1\<sharp>e" "x\<^isub>2\<sharp>e''" "x\<^isub>2\<sharp>e" |
|
594 obtains e' where "e \<Down> InR e'" and "e\<^isub>2[x\<^isub>2::=e'] \<Down> e''" |
|
595 using assms |
|
596 apply - |
|
597 apply(rule b_inv_auto(2)) |
|
598 apply(auto) |
|
599 apply(simp add: alpha) |
|
600 apply(auto) |
|
601 apply(drule_tac x="[(x\<^isub>2,x\<^isub>2')]\<bullet>e'" in meta_spec) |
|
602 apply(drule meta_mp) |
|
603 apply(rule_tac pi="[(x\<^isub>2,x\<^isub>2')]" in big_eqvt') |
|
604 apply(perm_simp add: fresh_prod) |
|
605 apply(drule meta_mp) |
|
606 apply(rule_tac pi="[(x\<^isub>2,x\<^isub>2')]" in big_eqvt') |
|
607 apply(perm_simp add: eqvts calc_atm) |
|
608 apply(assumption) |
|
609 apply(drule_tac x="[(x\<^isub>2,x\<^isub>2')]\<bullet>e'" in meta_spec) |
|
610 apply(drule meta_mp) |
|
611 apply(rule_tac pi="[(x\<^isub>2,x\<^isub>2')]" in big_eqvt') |
|
612 apply(perm_simp add: fresh_prod) |
|
613 apply(drule meta_mp) |
|
614 apply(rule_tac pi="[(x\<^isub>2,x\<^isub>2')]" in big_eqvt') |
|
615 apply(perm_simp add: eqvts calc_atm) |
|
616 apply(assumption) |
|
617 done |
|
618 |
|
619 inductive |
|
620 val :: "trm\<Rightarrow>bool" |
|
621 where |
|
622 v_Lam[intro]: "val (Lam [x].e)" |
|
623 | v_Const[intro]: "val (Const n)" |
|
624 | v_Pr[intro]: "\<lbrakk>val e\<^isub>1; val e\<^isub>2\<rbrakk> \<Longrightarrow> val (Pr e\<^isub>1 e\<^isub>2)" |
|
625 | v_InL[intro]: "val e \<Longrightarrow> val (InL e)" |
|
626 | v_InR[intro]: "val e \<Longrightarrow> val (InR e)" |
|
627 |
|
628 declare trm.inject [simp add] |
|
629 declare ty.inject [simp add] |
|
630 declare data.inject [simp add] |
|
631 |
|
632 inductive_cases v_inv_auto[elim]: |
|
633 "val (Const n)" |
|
634 "val (Pr e\<^isub>1 e\<^isub>2)" |
|
635 "val (InL e)" |
|
636 "val (InR e)" |
|
637 "val (Fst e)" |
|
638 "val (Snd e)" |
|
639 "val (Case e of inl x\<^isub>1 \<rightarrow> e\<^isub>1 | inr x\<^isub>2 \<rightarrow> e\<^isub>2)" |
|
640 "val (Var x)" |
|
641 "val (Lam [x].e)" |
|
642 "val (App e\<^isub>1 e\<^isub>2)" |
|
643 |
|
644 declare trm.inject [simp del] |
|
645 declare ty.inject [simp del] |
|
646 declare data.inject [simp del] |
|
647 |
354 |
648 lemma subject_reduction: |
355 lemma subject_reduction: |
649 assumes a: "e \<Down> e'" |
356 assumes a: "e \<Down> e'" and b: "\<Gamma> \<turnstile> e : T" |
650 and b: "\<Gamma> \<turnstile> e : T" |
|
651 shows "\<Gamma> \<turnstile> e' : T" |
357 shows "\<Gamma> \<turnstile> e' : T" |
652 using a b |
358 using a b |
653 proof (nominal_induct avoiding: \<Gamma> arbitrary: T rule: big.strong_induct) |
359 proof (nominal_induct avoiding: \<Gamma> arbitrary: T rule: big.strong_induct) |
654 case (b_App x e\<^isub>1 e\<^isub>2 e' e e\<^isub>2' \<Gamma> T) |
360 case (b_App x e\<^isub>1 e\<^isub>2 e' e e\<^isub>2' \<Gamma> T) |
655 have vc: "x\<sharp>\<Gamma>" by fact |
361 have vc: "x\<sharp>\<Gamma>" by fact |
656 have "\<Gamma> \<turnstile> App e\<^isub>1 e\<^isub>2 : T" by fact |
362 have "\<Gamma> \<turnstile> App e\<^isub>1 e\<^isub>2 : T" by fact |
657 then obtain T' where |
363 then obtain T' where a1: "\<Gamma> \<turnstile> e\<^isub>1 : T'\<rightarrow>T" and a2: "\<Gamma> \<turnstile> e\<^isub>2 : T'" |
658 a1: "\<Gamma> \<turnstile> e\<^isub>1 : T'\<rightarrow>T" and |
364 by (cases) (auto simp add: trm.inject) |
659 a2: "\<Gamma> \<turnstile> e\<^isub>2 : T'" by auto |
|
660 have ih1: "\<Gamma> \<turnstile> e\<^isub>1 : T' \<rightarrow> T \<Longrightarrow> \<Gamma> \<turnstile> Lam [x].e : T' \<rightarrow> T" by fact |
365 have ih1: "\<Gamma> \<turnstile> e\<^isub>1 : T' \<rightarrow> T \<Longrightarrow> \<Gamma> \<turnstile> Lam [x].e : T' \<rightarrow> T" by fact |
661 have ih2: "\<Gamma> \<turnstile> e\<^isub>2 : T' \<Longrightarrow> \<Gamma> \<turnstile> e\<^isub>2' : T'" by fact |
366 have ih2: "\<Gamma> \<turnstile> e\<^isub>2 : T' \<Longrightarrow> \<Gamma> \<turnstile> e\<^isub>2' : T'" by fact |
662 have ih3: "\<Gamma> \<turnstile> e[x::=e\<^isub>2'] : T \<Longrightarrow> \<Gamma> \<turnstile> e' : T" by fact |
367 have ih3: "\<Gamma> \<turnstile> e[x::=e\<^isub>2'] : T \<Longrightarrow> \<Gamma> \<turnstile> e' : T" by fact |
663 have "\<Gamma> \<turnstile> Lam [x].e : T'\<rightarrow>T" using ih1 a1 by simp |
368 have "\<Gamma> \<turnstile> Lam [x].e : T'\<rightarrow>T" using ih1 a1 by simp |
664 then have "((x,T')#\<Gamma>) \<turnstile> e : T" using vc by (auto simp add: ty.inject) |
369 then have "((x,T')#\<Gamma>) \<turnstile> e : T" using vc |
|
370 by (auto elim: t_Lam_elim simp add: ty.inject) |
665 moreover |
371 moreover |
666 have "\<Gamma> \<turnstile> e\<^isub>2': T'" using ih2 a2 by simp |
372 have "\<Gamma> \<turnstile> e\<^isub>2': T'" using ih2 a2 by simp |
667 ultimately have "\<Gamma> \<turnstile> e[x::=e\<^isub>2'] : T" by (simp add: typing_substitution) |
373 ultimately have "\<Gamma> \<turnstile> e[x::=e\<^isub>2'] : T" by (simp add: typing_substitution) |
668 thus "\<Gamma> \<turnstile> e' : T" using ih3 by simp |
374 thus "\<Gamma> \<turnstile> e' : T" using ih3 by simp |
669 next |
|
670 case (b_CaseL x\<^isub>1 e e\<^isub>2 e'' x\<^isub>2 e\<^isub>1 e' \<Gamma>) |
|
671 have vc: "x\<^isub>1\<sharp>\<Gamma>" "x\<^isub>2\<sharp>\<Gamma>" by fact+ |
|
672 have "\<Gamma> \<turnstile> Case e of inl x\<^isub>1 \<rightarrow> e\<^isub>1 | inr x\<^isub>2 \<rightarrow> e\<^isub>2 : T" by fact |
|
673 then obtain S\<^isub>1 S\<^isub>2 e\<^isub>1' e\<^isub>2' where |
|
674 a1: "\<Gamma> \<turnstile> e : Data (DSum S\<^isub>1 S\<^isub>2)" and |
|
675 a2: "((x\<^isub>1,Data S\<^isub>1)#\<Gamma>) \<turnstile> e\<^isub>1 : T" using vc by auto |
|
676 have ih1:"\<Gamma> \<turnstile> e : Data (DSum S\<^isub>1 S\<^isub>2) \<Longrightarrow> \<Gamma> \<turnstile> InL e' : Data (DSum S\<^isub>1 S\<^isub>2)" by fact |
|
677 have ih2:"\<Gamma> \<turnstile> e\<^isub>1[x\<^isub>1::=e'] : T \<Longrightarrow> \<Gamma> \<turnstile> e'' : T " by fact |
|
678 have "\<Gamma> \<turnstile> InL e' : Data (DSum S\<^isub>1 S\<^isub>2)" using ih1 a1 by simp |
|
679 then have "\<Gamma> \<turnstile> e' : Data S\<^isub>1" by auto |
|
680 then have "\<Gamma> \<turnstile> e\<^isub>1[x\<^isub>1::=e'] : T" using a2 by (simp add: typing_substitution) |
|
681 then show "\<Gamma> \<turnstile> e'' : T" using ih2 by simp |
|
682 next |
|
683 case (b_CaseR x\<^isub>1 e e\<^isub>2 e'' x\<^isub>2 e\<^isub>1 e' \<Gamma> T) |
|
684 then show "\<Gamma> \<turnstile> e'' : T" by (blast intro: typing_substitution) |
|
685 qed (blast)+ |
375 qed (blast)+ |
686 |
376 |
687 lemma unicity_of_evaluation: |
377 lemma unicity_of_evaluation: |
688 assumes a: "e \<Down> e\<^isub>1" |
378 assumes a: "e \<Down> e\<^isub>1" |
689 and b: "e \<Down> e\<^isub>2" |
379 and b: "e \<Down> e\<^isub>2" |
697 case (b_App x e\<^isub>1 e\<^isub>2 e' e\<^isub>1' e\<^isub>2' t\<^isub>2) |
387 case (b_App x e\<^isub>1 e\<^isub>2 e' e\<^isub>1' e\<^isub>2' t\<^isub>2) |
698 have ih1: "\<And>t. e\<^isub>1 \<Down> t \<Longrightarrow> Lam [x].e\<^isub>1' = t" by fact |
388 have ih1: "\<And>t. e\<^isub>1 \<Down> t \<Longrightarrow> Lam [x].e\<^isub>1' = t" by fact |
699 have ih2:"\<And>t. e\<^isub>2 \<Down> t \<Longrightarrow> e\<^isub>2' = t" by fact |
389 have ih2:"\<And>t. e\<^isub>2 \<Down> t \<Longrightarrow> e\<^isub>2' = t" by fact |
700 have ih3: "\<And>t. e\<^isub>1'[x::=e\<^isub>2'] \<Down> t \<Longrightarrow> e' = t" by fact |
390 have ih3: "\<And>t. e\<^isub>1'[x::=e\<^isub>2'] \<Down> t \<Longrightarrow> e' = t" by fact |
701 have app: "App e\<^isub>1 e\<^isub>2 \<Down> t\<^isub>2" by fact |
391 have app: "App e\<^isub>1 e\<^isub>2 \<Down> t\<^isub>2" by fact |
702 have vc: "x\<sharp>e\<^isub>1" "x\<sharp>e\<^isub>2" by fact+ |
392 have vc: "x\<sharp>e\<^isub>1" "x\<sharp>e\<^isub>2" "x\<sharp>t\<^isub>2" by fact |
703 then have "x \<sharp> App e\<^isub>1 e\<^isub>2" by auto |
393 then have "x\<sharp>App e\<^isub>1 e\<^isub>2" by auto |
704 then have vc': "x\<sharp>t\<^isub>2" using fresh_preserved app by blast |
394 from app vc obtain f\<^isub>1 f\<^isub>2 where x1: "e\<^isub>1 \<Down> Lam [x]. f\<^isub>1" and x2: "e\<^isub>2 \<Down> f\<^isub>2" and x3: "f\<^isub>1[x::=f\<^isub>2] \<Down> t\<^isub>2" |
705 from vc vc' obtain f\<^isub>1 f\<^isub>2 where x1: "e\<^isub>1 \<Down> Lam [x]. f\<^isub>1" and x2: "e\<^isub>2 \<Down> f\<^isub>2" and x3: "f\<^isub>1[x::=f\<^isub>2] \<Down> t\<^isub>2" |
395 by (cases rule: big.strong_cases[where x="x" and xa="x"]) |
706 using app by (auto simp add: fresh_prod) |
396 (auto simp add: trm.inject) |
707 then have "Lam [x]. f\<^isub>1 = Lam [x]. e\<^isub>1'" using ih1 by simp |
397 then have "Lam [x]. f\<^isub>1 = Lam [x]. e\<^isub>1'" using ih1 by simp |
708 then |
398 then |
709 have "f\<^isub>1 = e\<^isub>1'" by (auto simp add: trm.inject alpha) |
399 have "f\<^isub>1 = e\<^isub>1'" by (auto simp add: trm.inject alpha) |
710 moreover |
400 moreover |
711 have "f\<^isub>2 = e\<^isub>2'" using x2 ih2 by simp |
401 have "f\<^isub>2 = e\<^isub>2'" using x2 ih2 by simp |
712 ultimately have "e\<^isub>1'[x::=e\<^isub>2'] \<Down> t\<^isub>2" using x3 by simp |
402 ultimately have "e\<^isub>1'[x::=e\<^isub>2'] \<Down> t\<^isub>2" using x3 by simp |
713 thus ?case using ih3 by simp |
403 thus "e' = t\<^isub>2" using ih3 by simp |
714 next |
404 qed |
715 case (b_CaseL x\<^isub>1 e e\<^isub>2 e'' x\<^isub>2 e\<^isub>1 e' t\<^isub>2) |
|
716 have fs: "x\<^isub>1\<sharp>e" "x\<^isub>1\<sharp>t\<^isub>2" "x\<^isub>2\<sharp>e" "x\<^isub>2\<sharp>t\<^isub>2" by fact+ |
|
717 have ih1:"\<And>t. e \<Down> t \<Longrightarrow> InL e' = t" by fact |
|
718 have ih2:"\<And>t. e\<^isub>1[x\<^isub>1::=e'] \<Down> t \<Longrightarrow> e'' = t" by fact |
|
719 have ha: "\<not>(\<exists>t. e \<Down> InR t)" using ih1 by force |
|
720 have "Case e of inl x\<^isub>1 \<rightarrow> e\<^isub>1 | inr x\<^isub>2 \<rightarrow> e\<^isub>2 \<Down> t\<^isub>2" by fact |
|
721 then obtain f' where "e \<Down> InL f'" and h: "e\<^isub>1[x\<^isub>1::=f']\<Down>t\<^isub>2" using ha fs by auto |
|
722 then have "InL f' = InL e'" using ih1 by simp |
|
723 then have "f' = e'" by (simp add: trm.inject) |
|
724 then have "e\<^isub>1[x\<^isub>1::=e'] \<Down> t\<^isub>2" using h by simp |
|
725 then show "e'' = t\<^isub>2" using ih2 by simp |
|
726 next |
|
727 case (b_CaseR x\<^isub>1 e e\<^isub>2 e'' x\<^isub>2 e\<^isub>1 e' t\<^isub>2 ) |
|
728 have fs: "x\<^isub>1\<sharp>e" "x\<^isub>1\<sharp>t\<^isub>2" "x\<^isub>2\<sharp>e" "x\<^isub>2\<sharp>t\<^isub>2" by fact+ |
|
729 have ih1: "\<And>t. e \<Down> t \<Longrightarrow> InR e' = t" by fact |
|
730 have ih2: "\<And>t. e\<^isub>2[x\<^isub>2::=e'] \<Down> t \<Longrightarrow> e'' = t" by fact |
|
731 have ha: "\<not>(\<exists>t. e \<Down> InL t)" using ih1 by force |
|
732 have "Case e of inl x\<^isub>1 \<rightarrow> e\<^isub>1 | inr x\<^isub>2 \<rightarrow> e\<^isub>2 \<Down> t\<^isub>2" by fact |
|
733 then obtain f' where "e \<Down> InR f'" and h: "e\<^isub>2[x\<^isub>2::=f']\<Down>t\<^isub>2" using ha fs by auto |
|
734 then have "InR f' = InR e'" using ih1 by simp |
|
735 then have "e\<^isub>2[x\<^isub>2::=e'] \<Down> t\<^isub>2" using h by (simp add: trm.inject) |
|
736 thus "e'' = t\<^isub>2" using ih2 by simp |
|
737 next |
|
738 case (b_Fst e e\<^isub>1 e\<^isub>2 e\<^isub>2') |
|
739 have "e \<Down> Pr e\<^isub>1 e\<^isub>2" by fact |
|
740 have "\<And> b. e \<Down> b \<Longrightarrow> Pr e\<^isub>1 e\<^isub>2 = b" by fact |
|
741 have "Fst e \<Down> e\<^isub>2'" by fact |
|
742 show "e\<^isub>1 = e\<^isub>2'" using prems by (force simp add: trm.inject) |
|
743 next |
|
744 case (b_Snd e e\<^isub>1 e\<^isub>2 e\<^isub>2') |
|
745 have "e \<Down> Pr e\<^isub>1 e\<^isub>2" by fact |
|
746 have "\<And> b. e \<Down> b \<Longrightarrow> Pr e\<^isub>1 e\<^isub>2 = b" by fact |
|
747 have "Snd e \<Down> e\<^isub>2'" by fact |
|
748 show "e\<^isub>2 = e\<^isub>2'" using prems by (force simp add: trm.inject) |
|
749 qed (blast)+ |
|
750 |
|
751 lemma not_val_App[simp]: |
|
752 shows |
|
753 "\<not> val (App e\<^isub>1 e\<^isub>2)" |
|
754 "\<not> val (Fst e)" |
|
755 "\<not> val (Snd e)" |
|
756 "\<not> val (Var x)" |
|
757 "\<not> val (Case e of inl x\<^isub>1 \<rightarrow> e\<^isub>1 | inr x\<^isub>2 \<rightarrow> e\<^isub>2)" |
|
758 by auto |
|
759 |
405 |
760 lemma reduces_evaluates_to_values: |
406 lemma reduces_evaluates_to_values: |
761 assumes h:"t \<Down> t'" |
407 assumes h:"t \<Down> t'" |
762 shows "val t'" |
408 shows "val t'" |
763 using h by (induct) (auto) |
409 using h by (induct) (auto) |
764 |
|
765 lemma type_prod_evaluates_to_pairs: |
|
766 assumes a: "\<Gamma> \<turnstile> t : Data (DProd S\<^isub>1 S\<^isub>2)" |
|
767 and b: "t \<Down> t'" |
|
768 obtains t\<^isub>1 t\<^isub>2 where "t' = Pr t\<^isub>1 t\<^isub>2" |
|
769 proof - |
|
770 have "\<Gamma> \<turnstile> t' : Data (DProd S\<^isub>1 S\<^isub>2)" using assms subject_reduction by simp |
|
771 moreover |
|
772 have "val t'" using reduces_evaluates_to_values assms by simp |
|
773 ultimately obtain t\<^isub>1 t\<^isub>2 where "t' = Pr t\<^isub>1 t\<^isub>2" by (cases, auto simp add:ty.inject data.inject) |
|
774 thus ?thesis using prems by auto |
|
775 qed |
|
776 |
|
777 lemma type_sum_evaluates_to_ins: |
|
778 assumes "\<Gamma> \<turnstile> t : Data (DSum \<sigma>\<^isub>1 \<sigma>\<^isub>2)" and "t \<Down> t'" |
|
779 shows "(\<exists>t''. t' = InL t'') \<or> (\<exists>t''. t' = InR t'')" |
|
780 proof - |
|
781 have "\<Gamma> \<turnstile> t' : Data (DSum \<sigma>\<^isub>1 \<sigma>\<^isub>2)" using assms subject_reduction by simp |
|
782 moreover |
|
783 have "val t'" using reduces_evaluates_to_values assms by simp |
|
784 ultimately obtain t'' where "t' = InL t'' \<or> t' = InR t''" |
|
785 by (cases, auto simp add:ty.inject data.inject) |
|
786 thus ?thesis by auto |
|
787 qed |
|
788 |
410 |
789 lemma type_arrow_evaluates_to_lams: |
411 lemma type_arrow_evaluates_to_lams: |
790 assumes "\<Gamma> \<turnstile> t : \<sigma> \<rightarrow> \<tau>" and "t \<Down> t'" |
412 assumes "\<Gamma> \<turnstile> t : \<sigma> \<rightarrow> \<tau>" and "t \<Down> t'" |
791 obtains x t'' where "t' = Lam [x]. t''" |
413 obtains x t'' where "t' = Lam [x]. t''" |
792 proof - |
414 proof - |
793 have "\<Gamma> \<turnstile> t' : \<sigma> \<rightarrow> \<tau>" using assms subject_reduction by simp |
415 have "\<Gamma> \<turnstile> t' : \<sigma> \<rightarrow> \<tau>" using assms subject_reduction by simp |
794 moreover |
416 moreover |
795 have "val t'" using reduces_evaluates_to_values assms by simp |
417 have "val t'" using reduces_evaluates_to_values assms by simp |
796 ultimately obtain x t'' where "t' = Lam [x]. t''" by (cases, auto simp add:ty.inject data.inject) |
418 ultimately obtain x t'' where "t' = Lam [x]. t''" by (cases, auto simp add:ty.inject) |
797 thus ?thesis using prems by auto |
419 thus ?thesis using prems by auto |
798 qed |
420 qed |
799 |
421 |
800 lemma type_nat_evaluates_to_consts: |
422 (* Valuation *) |
801 assumes "\<Gamma> \<turnstile> t : Data DNat" and "t \<Down> t'" |
|
802 obtains n where "t' = Const n" |
|
803 proof - |
|
804 have "\<Gamma> \<turnstile> t' : Data DNat " using assms subject_reduction by simp |
|
805 moreover have "val t'" using reduces_evaluates_to_values assms by simp |
|
806 ultimately obtain n where "t' = Const n" by (cases, auto simp add:ty.inject data.inject) |
|
807 thus ?thesis using prems by auto |
|
808 qed |
|
809 |
|
810 consts |
|
811 V' :: "data \<Rightarrow> trm set" |
|
812 |
|
813 nominal_primrec |
|
814 "V' (DNat) = {Const n | n. n \<in> (UNIV::nat set)}" |
|
815 "V' (DProd S\<^isub>1 S\<^isub>2) = {Pr x y | x y. x \<in> V' S\<^isub>1 \<and> y \<in> V' S\<^isub>2}" |
|
816 "V' (DSum S\<^isub>1 S\<^isub>2) = {InL x | x. x \<in> V' S\<^isub>1} \<union> {InR y | y. y \<in> V' S\<^isub>2}" |
|
817 apply(rule TrueI)+ |
|
818 done |
|
819 |
|
820 lemma Vprimes_are_values : |
|
821 fixes S::"data" |
|
822 assumes h: "e \<in> V' S" |
|
823 shows "val e" |
|
824 using h |
|
825 by (nominal_induct S arbitrary: e rule:data.induct) |
|
826 (auto) |
|
827 |
|
828 lemma V'_eqvt: |
|
829 fixes pi::"name prm" |
|
830 assumes a: "v \<in> V' S" |
|
831 shows "(pi\<bullet>v) \<in> V' S" |
|
832 using a |
|
833 by (nominal_induct S arbitrary: v rule: data.induct) |
|
834 (auto simp add: trm.inject) |
|
835 |
|
836 consts |
423 consts |
837 V :: "ty \<Rightarrow> trm set" |
424 V :: "ty \<Rightarrow> trm set" |
838 |
425 |
839 nominal_primrec |
426 nominal_primrec |
840 "V (Data S) = V' S" |
427 "V (TVar x) = {e. val e}" |
841 "V (T\<^isub>1 \<rightarrow> T\<^isub>2) = {Lam [x].e | x e. \<forall> v \<in> (V T\<^isub>1). \<exists> v'. e[x::=v] \<Down> v' \<and> v' \<in> V T\<^isub>2}" |
428 "V (T\<^isub>1 \<rightarrow> T\<^isub>2) = {Lam [x].e | x e. \<forall> v \<in> (V T\<^isub>1). \<exists> v'. e[x::=v] \<Down> v' \<and> v' \<in> V T\<^isub>2}" |
842 apply(rule TrueI)+ |
429 by (rule TrueI)+ |
843 done |
430 |
844 |
431 (* can go with strong inversion rules *) |
845 lemma V_eqvt: |
432 lemma V_eqvt: |
846 fixes pi::"name prm" |
433 fixes pi::"name prm" |
847 assumes a: "x\<in>V T" |
434 assumes a: "x\<in>V T" |
848 shows "(pi\<bullet>x)\<in>V T" |
435 shows "(pi\<bullet>x)\<in>V T" |
849 using a |
436 using a |
850 apply(nominal_induct T arbitrary: pi x rule: ty.induct) |
437 apply(nominal_induct T arbitrary: pi x rule: ty.induct) |
851 apply(auto simp add: trm.inject perm_set_def) |
438 apply(auto simp add: trm.inject perm_set_def) |
852 apply(perm_simp add: V'_eqvt) |
439 apply(simp add: eqvts) |
853 apply(rule_tac x="pi\<bullet>xa" in exI) |
440 apply(rule_tac x="pi\<bullet>xa" in exI) |
854 apply(rule_tac x="pi\<bullet>e" in exI) |
441 apply(rule_tac x="pi\<bullet>e" in exI) |
855 apply(simp) |
442 apply(simp) |
856 apply(auto) |
443 apply(auto) |
857 apply(drule_tac x="(rev pi)\<bullet>v" in bspec) |
444 apply(drule_tac x="(rev pi)\<bullet>v" in bspec) |
956 } |
538 } |
957 ultimately show "\<exists>e'. ((x,e)#\<theta>) maps x' to e' \<and> e' \<in> V T'" by blast |
539 ultimately show "\<exists>e'. ((x,e)#\<theta>) maps x' to e' \<and> e' \<in> V T'" by blast |
958 qed |
540 qed |
959 |
541 |
960 lemma termination_aux: |
542 lemma termination_aux: |
961 fixes T :: "ty" |
|
962 fixes \<Gamma> :: "(name \<times> ty) list" |
|
963 fixes \<theta> :: "(name \<times> trm) list" |
|
964 fixes e :: "trm" |
|
965 assumes h1: "\<Gamma> \<turnstile> e : T" |
543 assumes h1: "\<Gamma> \<turnstile> e : T" |
966 and h2: "\<theta> Vcloses \<Gamma>" |
544 and h2: "\<theta> Vcloses \<Gamma>" |
967 shows "\<exists>v. \<theta><e> \<Down> v \<and> v \<in> V T" |
545 shows "\<exists>v. \<theta><e> \<Down> v \<and> v \<in> V T" |
968 using h2 h1 |
546 using h2 h1 |
969 proof(nominal_induct e avoiding: \<Gamma> \<theta> arbitrary: T rule: trm.induct) |
547 proof(nominal_induct e avoiding: \<Gamma> \<theta> arbitrary: T rule: trm.induct) |
970 case (App e\<^isub>1 e\<^isub>2 \<Gamma> \<theta> T) |
548 case (App e\<^isub>1 e\<^isub>2 \<Gamma> \<theta> T) |
971 have ih\<^isub>1:"\<And>\<theta> \<Gamma> T. \<lbrakk>\<theta> Vcloses \<Gamma>; \<Gamma> \<turnstile> e\<^isub>1 : T\<rbrakk> \<Longrightarrow> \<exists>v. \<theta><e\<^isub>1> \<Down> v \<and> v \<in> V T" by fact |
549 have ih\<^isub>1:"\<And>\<theta> \<Gamma> T. \<lbrakk>\<theta> Vcloses \<Gamma>; \<Gamma> \<turnstile> e\<^isub>1 : T\<rbrakk> \<Longrightarrow> \<exists>v. \<theta><e\<^isub>1> \<Down> v \<and> v \<in> V T" by fact |
972 have ih\<^isub>2:"\<And>\<theta> \<Gamma> T. \<lbrakk>\<theta> Vcloses \<Gamma>; \<Gamma> \<turnstile> e\<^isub>2 : T\<rbrakk> \<Longrightarrow> \<exists>v. \<theta><e\<^isub>2> \<Down> v \<and> v \<in> V T" by fact |
550 have ih\<^isub>2:"\<And>\<theta> \<Gamma> T. \<lbrakk>\<theta> Vcloses \<Gamma>; \<Gamma> \<turnstile> e\<^isub>2 : T\<rbrakk> \<Longrightarrow> \<exists>v. \<theta><e\<^isub>2> \<Down> v \<and> v \<in> V T" by fact |
973 have as\<^isub>1:"\<theta> Vcloses \<Gamma>" by fact |
551 have as\<^isub>1:"\<theta> Vcloses \<Gamma>" by fact |
974 have as\<^isub>2: "\<Gamma> \<turnstile> App e\<^isub>1 e\<^isub>2 : T" by fact |
552 have as\<^isub>2: "\<Gamma> \<turnstile> App e\<^isub>1 e\<^isub>2 : T" by fact |
975 from as\<^isub>2 obtain T' where "\<Gamma> \<turnstile> e\<^isub>1 : T' \<rightarrow> T" and "\<Gamma> \<turnstile> e\<^isub>2 : T'" by auto |
553 then obtain T' where "\<Gamma> \<turnstile> e\<^isub>1 : T' \<rightarrow> T" and "\<Gamma> \<turnstile> e\<^isub>2 : T'" |
|
554 by (cases) (auto simp add: trm.inject) |
976 then obtain v\<^isub>1 v\<^isub>2 where "(i)": "\<theta><e\<^isub>1> \<Down> v\<^isub>1" "v\<^isub>1 \<in> V (T' \<rightarrow> T)" |
555 then obtain v\<^isub>1 v\<^isub>2 where "(i)": "\<theta><e\<^isub>1> \<Down> v\<^isub>1" "v\<^isub>1 \<in> V (T' \<rightarrow> T)" |
977 and "(ii)":"\<theta><e\<^isub>2> \<Down> v\<^isub>2" "v\<^isub>2 \<in> V T'" using ih\<^isub>1 ih\<^isub>2 as\<^isub>1 by blast |
556 and "(ii)":"\<theta><e\<^isub>2> \<Down> v\<^isub>2" "v\<^isub>2 \<in> V T'" using ih\<^isub>1 ih\<^isub>2 as\<^isub>1 by blast |
978 from "(i)" obtain x e' |
557 from "(i)" obtain x e' |
979 where "v\<^isub>1 = Lam[x].e'" |
558 where "v\<^isub>1 = Lam[x].e'" |
980 and "(iii)": "(\<forall>v \<in> (V T').\<exists> v'. e'[x::=v] \<Down> v' \<and> v' \<in> V T)" |
559 and "(iii)": "(\<forall>v \<in> (V T').\<exists> v'. e'[x::=v] \<Down> v' \<and> v' \<in> V T)" |
981 and "(iv)": "\<theta><e\<^isub>1> \<Down> Lam [x].e'" |
560 and "(iv)": "\<theta><e\<^isub>1> \<Down> Lam [x].e'" |
982 and fr: "x\<sharp>(\<theta>,e\<^isub>1,e\<^isub>2)" by blast |
561 and fr: "x\<sharp>(\<theta>,e\<^isub>1,e\<^isub>2)" by (blast elim: V_arrow_elim_strong) |
983 from fr have fr\<^isub>1: "x\<sharp>\<theta><e\<^isub>1>" and fr\<^isub>2: "x\<sharp>\<theta><e\<^isub>2>" by (simp_all add: fresh_psubst) |
562 from fr have fr\<^isub>1: "x\<sharp>\<theta><e\<^isub>1>" and fr\<^isub>2: "x\<sharp>\<theta><e\<^isub>2>" by (simp_all add: fresh_psubst) |
984 from "(ii)" "(iii)" obtain v\<^isub>3 where "(v)": "e'[x::=v\<^isub>2] \<Down> v\<^isub>3" "v\<^isub>3 \<in> V T" by auto |
563 from "(ii)" "(iii)" obtain v\<^isub>3 where "(v)": "e'[x::=v\<^isub>2] \<Down> v\<^isub>3" "v\<^isub>3 \<in> V T" by auto |
985 from fr\<^isub>2 "(ii)" have "x\<sharp>v\<^isub>2" by (simp add: fresh_preserved) |
564 from fr\<^isub>2 "(ii)" have "x\<sharp>v\<^isub>2" by (simp add: big_preserves_fresh) |
986 then have "x\<sharp>e'[x::=v\<^isub>2]" by (simp add: fresh_subst_fresh) |
565 then have "x\<sharp>e'[x::=v\<^isub>2]" by (simp add: fresh_subst') |
987 then have fr\<^isub>3: "x\<sharp>v\<^isub>3" using "(v)" by (simp add: fresh_preserved) |
566 then have fr\<^isub>3: "x\<sharp>v\<^isub>3" using "(v)" by (simp add: big_preserves_fresh) |
988 from fr\<^isub>1 fr\<^isub>2 fr\<^isub>3 have "x\<sharp>(\<theta><e\<^isub>1>,\<theta><e\<^isub>2>,v\<^isub>3)" by simp |
567 from fr\<^isub>1 fr\<^isub>2 fr\<^isub>3 have "x\<sharp>(\<theta><e\<^isub>1>,\<theta><e\<^isub>2>,v\<^isub>3)" by simp |
989 with "(iv)" "(ii)" "(v)" have "App (\<theta><e\<^isub>1>) (\<theta><e\<^isub>2>) \<Down> v\<^isub>3" by auto |
568 with "(iv)" "(ii)" "(v)" have "App (\<theta><e\<^isub>1>) (\<theta><e\<^isub>2>) \<Down> v\<^isub>3" by auto |
990 then show "\<exists>v. \<theta><App e\<^isub>1 e\<^isub>2> \<Down> v \<and> v \<in> V T" using "(v)" by auto |
569 then show "\<exists>v. \<theta><App e\<^isub>1 e\<^isub>2> \<Down> v \<and> v \<in> V T" using "(v)" by auto |
991 next |
570 next |
992 case (Pr t\<^isub>1 t\<^isub>2 \<Gamma> \<theta> T) |
|
993 have "\<Gamma> \<turnstile> Pr t\<^isub>1 t\<^isub>2 : T" by fact |
|
994 then obtain T\<^isub>a T\<^isub>b where ta:"\<Gamma> \<turnstile> t\<^isub>1 : Data T\<^isub>a" and "\<Gamma> \<turnstile> t\<^isub>2 : Data T\<^isub>b" |
|
995 and eq:"T=Data (DProd T\<^isub>a T\<^isub>b)" by auto |
|
996 have h:"\<theta> Vcloses \<Gamma>" by fact |
|
997 then obtain v\<^isub>1 v\<^isub>2 where "\<theta><t\<^isub>1> \<Down> v\<^isub>1 \<and> v\<^isub>1 \<in> V (Data T\<^isub>a)" "\<theta><t\<^isub>2> \<Down> v\<^isub>2 \<and> v\<^isub>2 \<in> V (Data T\<^isub>b)" |
|
998 using prems by blast |
|
999 thus "\<exists>v. \<theta><Pr t\<^isub>1 t\<^isub>2> \<Down> v \<and> v \<in> V T" using eq by auto |
|
1000 next |
|
1001 case (Lam x e \<Gamma> \<theta> T) |
571 case (Lam x e \<Gamma> \<theta> T) |
1002 have ih:"\<And>\<theta> \<Gamma> T. \<lbrakk>\<theta> Vcloses \<Gamma>; \<Gamma> \<turnstile> e : T\<rbrakk> \<Longrightarrow> \<exists>v. \<theta><e> \<Down> v \<and> v \<in> V T" by fact |
572 have ih:"\<And>\<theta> \<Gamma> T. \<lbrakk>\<theta> Vcloses \<Gamma>; \<Gamma> \<turnstile> e : T\<rbrakk> \<Longrightarrow> \<exists>v. \<theta><e> \<Down> v \<and> v \<in> V T" by fact |
1003 have as\<^isub>1: "\<theta> Vcloses \<Gamma>" by fact |
573 have as\<^isub>1: "\<theta> Vcloses \<Gamma>" by fact |
1004 have as\<^isub>2: "\<Gamma> \<turnstile> Lam [x].e : T" by fact |
574 have as\<^isub>2: "\<Gamma> \<turnstile> Lam [x].e : T" by fact |
1005 have fs: "x\<sharp>\<Gamma>" "x\<sharp>\<theta>" by fact+ |
575 have fs: "x\<sharp>\<Gamma>" "x\<sharp>\<theta>" by fact |
1006 from as\<^isub>2 fs obtain T\<^isub>1 T\<^isub>2 |
576 from as\<^isub>2 fs obtain T\<^isub>1 T\<^isub>2 |
1007 where "(i)": "(x,T\<^isub>1)#\<Gamma> \<turnstile> e:T\<^isub>2" and "(ii)": "T = T\<^isub>1 \<rightarrow> T\<^isub>2" by auto |
577 where "(i)": "(x,T\<^isub>1)#\<Gamma> \<turnstile> e:T\<^isub>2" and "(ii)": "T = T\<^isub>1 \<rightarrow> T\<^isub>2" using fs |
|
578 by (cases rule: typing.strong_cases[where x="x"]) |
|
579 (auto simp add: trm.inject alpha abs_fresh fresh_ty) |
1008 from "(i)" have "(iii)": "valid ((x,T\<^isub>1)#\<Gamma>)" by (simp add: typing_implies_valid) |
580 from "(i)" have "(iii)": "valid ((x,T\<^isub>1)#\<Gamma>)" by (simp add: typing_implies_valid) |
1009 have "\<forall>v \<in> (V T\<^isub>1). \<exists>v'. (\<theta><e>)[x::=v] \<Down> v' \<and> v' \<in> V T\<^isub>2" |
581 have "\<forall>v \<in> (V T\<^isub>1). \<exists>v'. (\<theta><e>)[x::=v] \<Down> v' \<and> v' \<in> V T\<^isub>2" |
1010 proof |
582 proof |
1011 fix v |
583 fix v |
1012 assume "v \<in> (V T\<^isub>1)" |
584 assume "v \<in> (V T\<^isub>1)" |
1017 qed |
589 qed |
1018 then have "Lam[x].\<theta><e> \<in> V (T\<^isub>1 \<rightarrow> T\<^isub>2)" by auto |
590 then have "Lam[x].\<theta><e> \<in> V (T\<^isub>1 \<rightarrow> T\<^isub>2)" by auto |
1019 then have "\<theta><Lam [x].e> \<Down> Lam[x].\<theta><e> \<and> Lam[x].\<theta><e> \<in> V (T\<^isub>1\<rightarrow>T\<^isub>2)" using fs by auto |
591 then have "\<theta><Lam [x].e> \<Down> Lam[x].\<theta><e> \<and> Lam[x].\<theta><e> \<in> V (T\<^isub>1\<rightarrow>T\<^isub>2)" using fs by auto |
1020 thus "\<exists>v. \<theta><Lam [x].e> \<Down> v \<and> v \<in> V T" using "(ii)" by auto |
592 thus "\<exists>v. \<theta><Lam [x].e> \<Down> v \<and> v \<in> V T" using "(ii)" by auto |
1021 next |
593 next |
1022 case (Case t' n\<^isub>1 t\<^isub>1 n\<^isub>2 t\<^isub>2 \<Gamma> \<theta> T) |
594 case (Var x \<Gamma> \<theta> T) |
1023 have f: "n\<^isub>1\<sharp>\<Gamma>" "n\<^isub>1\<sharp>\<theta>" "n\<^isub>2\<sharp>\<Gamma>" "n\<^isub>2\<sharp>\<theta>" "n\<^isub>2\<noteq>n\<^isub>1" "n\<^isub>1\<sharp>t'" |
595 have "\<Gamma> \<turnstile> (Var x) : T" by fact |
1024 "n\<^isub>1\<sharp>t\<^isub>2" "n\<^isub>2\<sharp>t'" "n\<^isub>2\<sharp>t\<^isub>1" by fact+ |
596 then have "(x,T)\<in>set \<Gamma>" by (cases) (auto simp add: trm.inject) |
1025 have h:"\<theta> Vcloses \<Gamma>" by fact |
597 with prems have "\<theta><Var x> \<Down> \<theta><Var x> \<and> \<theta><Var x>\<in> V T" |
1026 have th:"\<Gamma> \<turnstile> Case t' of inl n\<^isub>1 \<rightarrow> t\<^isub>1 | inr n\<^isub>2 \<rightarrow> t\<^isub>2 : T" by fact |
598 by (auto intro!: Vs_reduce_to_themselves) |
1027 then obtain S\<^isub>1 S\<^isub>2 where |
599 then show "\<exists>v. \<theta><Var x> \<Down> v \<and> v \<in> V T" by auto |
1028 hm:"\<Gamma> \<turnstile> t' : Data (DSum S\<^isub>1 S\<^isub>2)" and |
600 qed |
1029 hl:"(n\<^isub>1,Data S\<^isub>1)#\<Gamma> \<turnstile> t\<^isub>1 : T" and |
|
1030 hr:"(n\<^isub>2,Data S\<^isub>2)#\<Gamma> \<turnstile> t\<^isub>2 : T" using f by auto |
|
1031 then obtain v\<^isub>0 where ht':"\<theta><t'> \<Down> v\<^isub>0" and hS:"v\<^isub>0 \<in> V (Data (DSum S\<^isub>1 S\<^isub>2))" using prems h by blast |
|
1032 (* We distinguish between the cases InL and InR *) |
|
1033 { fix v\<^isub>0' |
|
1034 assume eqc:"v\<^isub>0 = InL v\<^isub>0'" and "v\<^isub>0' \<in> V' S\<^isub>1" |
|
1035 then have inc: "v\<^isub>0' \<in> V (Data S\<^isub>1)" by auto |
|
1036 have "valid \<Gamma>" using th typing_implies_valid by auto |
|
1037 then moreover have "valid ((n\<^isub>1,Data S\<^isub>1)#\<Gamma>)" using f by auto |
|
1038 then moreover have "(n\<^isub>1,v\<^isub>0')#\<theta> Vcloses (n\<^isub>1,Data S\<^isub>1)#\<Gamma>" |
|
1039 using inc h monotonicity by blast |
|
1040 moreover |
|
1041 have ih:"\<And>\<Gamma> \<theta> T. \<lbrakk>\<theta> Vcloses \<Gamma>; \<Gamma> \<turnstile> t\<^isub>1 : T\<rbrakk> \<Longrightarrow> \<exists>v. \<theta><t\<^isub>1> \<Down> v \<and> v \<in> V T" by fact |
|
1042 ultimately obtain v\<^isub>1 where ho: "((n\<^isub>1,v\<^isub>0')#\<theta>)<t\<^isub>1> \<Down> v\<^isub>1 \<and> v\<^isub>1 \<in> V T" using hl by blast |
|
1043 then have r:"\<theta><t\<^isub>1>[n\<^isub>1::=v\<^isub>0'] \<Down> v\<^isub>1 \<and> v\<^isub>1 \<in> V T" using psubst_subst_psubst f by simp |
|
1044 then moreover have "n\<^isub>1\<sharp>(\<theta><t'>,\<theta><t\<^isub>2>,v\<^isub>1,n\<^isub>2)" |
|
1045 proof - |
|
1046 have "n\<^isub>1\<sharp>v\<^isub>0" using ht' fresh_preserved fresh_psubst f by auto |
|
1047 then have "n\<^isub>1\<sharp>v\<^isub>0'" using eqc by auto |
|
1048 then have "n\<^isub>1\<sharp>v\<^isub>1" using f r fresh_preserved fresh_subst_fresh by blast |
|
1049 thus "n\<^isub>1\<sharp>(\<theta><t'>,\<theta><t\<^isub>2>,v\<^isub>1,n\<^isub>2)" using f by (simp add: fresh_atm fresh_psubst) |
|
1050 qed |
|
1051 moreover have "n\<^isub>2\<sharp>(\<theta><t'>,\<theta><t\<^isub>1>,v\<^isub>1,n\<^isub>1)" |
|
1052 proof - |
|
1053 have "n\<^isub>2\<sharp>v\<^isub>0" using ht' fresh_preserved fresh_psubst f by auto |
|
1054 then have "n\<^isub>2\<sharp>v\<^isub>0'" using eqc by auto |
|
1055 then have "n\<^isub>2\<sharp>((n\<^isub>1,v\<^isub>0')#\<theta>)" using f by (simp add: fresh_list_cons fresh_prod fresh_atm) |
|
1056 then have "n\<^isub>2\<sharp>((n\<^isub>1,v\<^isub>0')#\<theta>)<t\<^isub>1>" using f fresh_psubst by auto |
|
1057 moreover then have "n\<^isub>2 \<sharp> v\<^isub>1" using fresh_preserved ho by auto |
|
1058 ultimately show "n\<^isub>2\<sharp>(\<theta><t'>,\<theta><t\<^isub>1>,v\<^isub>1,n\<^isub>1)" using f by (simp add: fresh_psubst fresh_atm) |
|
1059 qed |
|
1060 ultimately have "Case \<theta><t'> of inl n\<^isub>1 \<rightarrow> \<theta><t\<^isub>1> | inr n\<^isub>2 \<rightarrow> \<theta><t\<^isub>2> \<Down> v\<^isub>1 \<and> v\<^isub>1 \<in> V T" using ht' eqc by auto |
|
1061 moreover |
|
1062 have "Case \<theta><t'> of inl n\<^isub>1 \<rightarrow> \<theta><t\<^isub>1> | inr n\<^isub>2 \<rightarrow> \<theta><t\<^isub>2> = \<theta><Case t' of inl n\<^isub>1 \<rightarrow> t\<^isub>1 | inr n\<^isub>2 \<rightarrow> t\<^isub>2>" |
|
1063 using f by auto |
|
1064 ultimately have "\<exists>v. \<theta><Case t' of inl n\<^isub>1 \<rightarrow> t\<^isub>1 | inr n\<^isub>2 \<rightarrow> t\<^isub>2> \<Down> v \<and> v \<in> V T" by auto |
|
1065 } |
|
1066 moreover |
|
1067 { fix v\<^isub>0' |
|
1068 assume eqc:"v\<^isub>0 = InR v\<^isub>0'" and "v\<^isub>0' \<in> V' S\<^isub>2" |
|
1069 then have inc:"v\<^isub>0' \<in> V (Data S\<^isub>2)" by auto |
|
1070 have "valid \<Gamma>" using th typing_implies_valid by auto |
|
1071 then moreover have "valid ((n\<^isub>2,Data S\<^isub>2)#\<Gamma>)" using f by auto |
|
1072 then moreover have "(n\<^isub>2,v\<^isub>0')#\<theta> Vcloses (n\<^isub>2,Data S\<^isub>2)#\<Gamma>" |
|
1073 using inc h monotonicity by blast |
|
1074 moreover have ih:"\<And>\<Gamma> \<theta> T. \<lbrakk>\<theta> Vcloses \<Gamma>; \<Gamma> \<turnstile> t\<^isub>2 : T\<rbrakk> \<Longrightarrow> \<exists>v. \<theta><t\<^isub>2> \<Down> v \<and> v \<in> V T" by fact |
|
1075 ultimately obtain v\<^isub>2 where ho:"((n\<^isub>2,v\<^isub>0')#\<theta>)<t\<^isub>2> \<Down> v\<^isub>2 \<and> v\<^isub>2 \<in> V T" using hr by blast |
|
1076 then have r:"\<theta><t\<^isub>2>[n\<^isub>2::=v\<^isub>0'] \<Down> v\<^isub>2 \<and> v\<^isub>2 \<in> V T" using psubst_subst_psubst f by simp |
|
1077 moreover have "n\<^isub>1\<sharp>(\<theta><t'>,\<theta><t\<^isub>2>,v\<^isub>2,n\<^isub>2)" |
|
1078 proof - |
|
1079 have "n\<^isub>1\<sharp>\<theta><t'>" using fresh_psubst f by simp |
|
1080 then have "n\<^isub>1\<sharp>v\<^isub>0" using ht' fresh_preserved by auto |
|
1081 then have "n\<^isub>1\<sharp>v\<^isub>0'" using eqc by auto |
|
1082 then have "n\<^isub>1\<sharp>((n\<^isub>2,v\<^isub>0')#\<theta>)" using f by (simp add: fresh_list_cons fresh_atm fresh_prod) |
|
1083 then have "n\<^isub>1\<sharp>((n\<^isub>2,v\<^isub>0')#\<theta>)<t\<^isub>2>" using f fresh_psubst by auto |
|
1084 moreover then have "n\<^isub>1\<sharp>v\<^isub>2" using fresh_preserved ho by auto |
|
1085 ultimately show "n\<^isub>1 \<sharp> (\<theta><t'>,\<theta><t\<^isub>2>,v\<^isub>2,n\<^isub>2)" using f by (simp add: fresh_psubst fresh_atm) |
|
1086 qed |
|
1087 moreover have "n\<^isub>2 \<sharp> (\<theta><t'>,\<theta><t\<^isub>1>,v\<^isub>2,n\<^isub>1)" |
|
1088 proof - |
|
1089 have "n\<^isub>2\<sharp>\<theta><t'>" using fresh_psubst f by simp |
|
1090 then have "n\<^isub>2\<sharp>v\<^isub>0" using ht' fresh_preserved by auto |
|
1091 then have "n\<^isub>2\<sharp>v\<^isub>0'" using eqc by auto |
|
1092 then have "n\<^isub>2\<sharp>\<theta><t\<^isub>2>[n\<^isub>2::=v\<^isub>0']" using f fresh_subst_fresh by auto |
|
1093 then have "n\<^isub>2\<sharp>v\<^isub>2" using f fresh_preserved r by blast |
|
1094 then show "n\<^isub>2\<sharp>(\<theta><t'>,\<theta><t\<^isub>1>,v\<^isub>2,n\<^isub>1)" using f by (simp add: fresh_atm fresh_psubst) |
|
1095 qed |
|
1096 ultimately have "Case \<theta><t'> of inl n\<^isub>1 \<rightarrow> \<theta><t\<^isub>1> | inr n\<^isub>2 \<rightarrow> \<theta><t\<^isub>2> \<Down> v\<^isub>2 \<and> v\<^isub>2 \<in> V T" using ht' eqc by auto |
|
1097 then have "\<exists>v. \<theta><Case t' of inl n\<^isub>1 \<rightarrow> t\<^isub>1 | inr n\<^isub>2 \<rightarrow> t\<^isub>2> \<Down> v \<and> v \<in> V T" using f by auto |
|
1098 } |
|
1099 ultimately show "\<exists>v. \<theta><Case t' of inl n\<^isub>1 \<rightarrow> t\<^isub>1 | inr n\<^isub>2 \<rightarrow> t\<^isub>2> \<Down> v \<and> v \<in> V T" using hS V_sum by blast |
|
1100 qed (force)+ |
|
1101 |
601 |
1102 theorem termination_of_evaluation: |
602 theorem termination_of_evaluation: |
1103 assumes a: "[] \<turnstile> e : T" |
603 assumes a: "[] \<turnstile> e : T" |
1104 shows "\<exists>v. e \<Down> v \<and> val v" |
604 shows "\<exists>v. e \<Down> v \<and> val v" |
1105 proof - |
605 proof - |
1106 from a have "\<exists>v. (([]::(name \<times> trm) list)<e>) \<Down> v \<and> v \<in> V T" |
606 from a have "\<exists>v. []<e> \<Down> v \<and> v \<in> V T" by (rule termination_aux) (auto) |
1107 by (rule termination_aux) (auto) |
607 thus "\<exists>v. e \<Down> v \<and> val v" using Vs_are_values by auto |
1108 thus "\<exists>v. e \<Down> v \<and> val v" using V_are_values by auto |
|
1109 qed |
608 qed |
1110 |
609 |
1111 end |
610 end |