|
1 |
|
2 |
1 theory Tutorial5 |
3 theory Tutorial5 |
2 imports Tutorial4 |
4 imports Tutorial4 |
3 begin |
5 begin |
4 |
6 |
5 |
7 section {* Type-Preservation and Progress Lemma*} |
6 section {* Type Preservation (fixme separate file) *} |
8 |
|
9 text {* |
|
10 The point of this tutorial is to prove the |
|
11 type-preservation and progress lemma. Since |
|
12 we now know that \<Down>, \<longrightarrow>cbv* and the machine |
|
13 correspond to each other, we only need to |
|
14 prove this property for one of them. We chose |
|
15 \<longrightarrow>cbv. |
|
16 |
|
17 First we need to establish two elimination |
|
18 properties and two auxiliary lemmas about contexts. |
|
19 *} |
7 |
20 |
8 |
21 |
9 lemma valid_elim: |
22 lemma valid_elim: |
10 assumes a: "valid ((x, T) # \<Gamma>)" |
23 assumes a: "valid ((x, T) # \<Gamma>)" |
11 shows "atom x \<sharp> \<Gamma> \<and> valid \<Gamma>" |
24 shows "atom x \<sharp> \<Gamma> \<and> valid \<Gamma>" |
27 and a2: "(x, T) \<in> set \<Gamma>" |
40 and a2: "(x, T) \<in> set \<Gamma>" |
28 and a3: "(x, U) \<in> set \<Gamma>" |
41 and a3: "(x, U) \<in> set \<Gamma>" |
29 shows "T = U" |
42 shows "T = U" |
30 using a1 a2 a3 |
43 using a1 a2 a3 |
31 by (induct) (auto simp add: fresh_list fresh_Pair fresh_at_base) |
44 by (induct) (auto simp add: fresh_list fresh_Pair fresh_at_base) |
|
45 |
|
46 |
|
47 section {* EXERCISE 16 *} |
|
48 |
|
49 text {* |
|
50 Next we want to show the type substitution lemma. Unfortunately, |
|
51 we have to prove a slightly more general version of it, where |
|
52 the variable being substituted occurs somewhere inside the |
|
53 context. |
|
54 *} |
32 |
55 |
33 lemma type_substitution_aux: |
56 lemma type_substitution_aux: |
34 assumes a: "\<Delta> @ [(x, T')] @ \<Gamma> \<turnstile> e : T" |
57 assumes a: "\<Delta> @ [(x, T')] @ \<Gamma> \<turnstile> e : T" |
35 and b: "\<Gamma> \<turnstile> e' : T'" |
58 and b: "\<Gamma> \<turnstile> e' : T'" |
36 shows "\<Delta> @ \<Gamma> \<turnstile> e[x ::= e'] : T" |
59 shows "\<Delta> @ \<Gamma> \<turnstile> e[x ::= e'] : T" |
38 proof (nominal_induct \<Gamma>'\<equiv>"\<Delta> @ [(x, T')] @ \<Gamma>" e T avoiding: x e' \<Delta> rule: typing.strong_induct) |
61 proof (nominal_induct \<Gamma>'\<equiv>"\<Delta> @ [(x, T')] @ \<Gamma>" e T avoiding: x e' \<Delta> rule: typing.strong_induct) |
39 case (t_Var y T x e' \<Delta>) |
62 case (t_Var y T x e' \<Delta>) |
40 have a1: "valid (\<Delta> @ [(x, T')] @ \<Gamma>)" by fact |
63 have a1: "valid (\<Delta> @ [(x, T')] @ \<Gamma>)" by fact |
41 have a2: "(y,T) \<in> set (\<Delta> @ [(x, T')] @ \<Gamma>)" by fact |
64 have a2: "(y,T) \<in> set (\<Delta> @ [(x, T')] @ \<Gamma>)" by fact |
42 have a3: "\<Gamma> \<turnstile> e' : T'" by fact |
65 have a3: "\<Gamma> \<turnstile> e' : T'" by fact |
|
66 |
43 from a1 have a4: "valid (\<Delta> @ \<Gamma>)" by (rule valid_insert) |
67 from a1 have a4: "valid (\<Delta> @ \<Gamma>)" by (rule valid_insert) |
44 { assume eq: "x = y" |
68 { assume eq: "x = y" |
45 from a1 a2 have "T = T'" using eq by (auto intro: context_unique) |
69 |
46 with a3 have "\<Delta> @ \<Gamma> \<turnstile> Var y[x ::= e'] : T" using eq a4 by (auto intro: weakening) |
70 have "\<Delta> @ \<Gamma> \<turnstile> Var y[x ::= e'] : T" sorry |
47 } |
71 } |
48 moreover |
72 moreover |
49 { assume ineq: "x \<noteq> y" |
73 { assume ineq: "x \<noteq> y" |
50 from a2 have "(y, T) \<in> set (\<Delta> @ \<Gamma>)" using ineq by simp |
74 from a2 have "(y, T) \<in> set (\<Delta> @ \<Gamma>)" using ineq by simp |
51 then have "\<Delta> @ \<Gamma> \<turnstile> Var y[x ::= e'] : T" using ineq a4 by auto |
75 then have "\<Delta> @ \<Gamma> \<turnstile> Var y[x ::= e'] : T" using ineq a4 by auto |
52 } |
76 } |
53 ultimately show "\<Delta> @ \<Gamma> \<turnstile> Var y[x::=e'] : T" by blast |
77 ultimately show "\<Delta> @ \<Gamma> \<turnstile> Var y[x::=e'] : T" by blast |
54 qed (force simp add: fresh_append fresh_Cons)+ |
78 next |
|
79 case (t_Lam y T1 t T2 x e' \<Delta>) |
|
80 have a1: "atom y \<sharp> e'" by fact |
|
81 have a2: "atom y \<sharp> \<Delta> @ [(x, T')] @ \<Gamma>" by fact |
|
82 have a3: "\<Gamma> \<turnstile> e' : T'" by fact |
|
83 have ih: "\<Gamma> \<turnstile> e' : T' \<Longrightarrow> ((y, T1) # \<Delta>) @ \<Gamma> \<turnstile> t [x ::= e'] : T2" |
|
84 using t_Lam(6)[of "(y, T1) # \<Delta>"] by auto |
|
85 |
|
86 |
|
87 show "\<Delta> @ \<Gamma> \<turnstile> (Lam [y]. t)[x ::= e'] : T1 \<rightarrow> T2" sorry |
|
88 next |
|
89 case (t_App t1 T1 T2 t2 x e' \<Delta>) |
|
90 have ih1: "\<Gamma> \<turnstile> e' : T' \<Longrightarrow> \<Delta> @ \<Gamma> \<turnstile> t1 [x ::= e'] : T1 \<rightarrow> T2" using t_App(2) by auto |
|
91 have ih2: "\<Gamma> \<turnstile> e' : T' \<Longrightarrow> \<Delta> @ \<Gamma> \<turnstile> t2 [x ::= e'] : T1" using t_App(4) by auto |
|
92 have a: "\<Gamma> \<turnstile> e' : T'" by fact |
|
93 |
|
94 show "\<Delta> @ \<Gamma> \<turnstile> App t1 t2 [x ::= e'] : T2" sorry |
|
95 qed |
|
96 |
|
97 text {* |
|
98 From this we can derive the usual version of the substitution |
|
99 lemma. |
|
100 *} |
55 |
101 |
56 corollary type_substitution: |
102 corollary type_substitution: |
57 assumes a: "(x, T') # \<Gamma> \<turnstile> e : T" |
103 assumes a: "(x, T') # \<Gamma> \<turnstile> e : T" |
58 and b: "\<Gamma> \<turnstile> e' : T'" |
104 and b: "\<Gamma> \<turnstile> e' : T'" |
59 shows "\<Gamma> \<turnstile> e[x ::= e'] : T" |
105 shows "\<Gamma> \<turnstile> e[x ::= e'] : T" |
60 using a b type_substitution_aux[where \<Delta>="[]"] |
106 using a b type_substitution_aux[of "[]"] |
61 by auto |
107 by auto |
|
108 |
|
109 |
|
110 section {* Type Preservation *} |
|
111 |
|
112 text {* |
|
113 Finally we are in a position to establish the type preservation |
|
114 property. We just need the following two inversion rules for |
|
115 particualr typing instances. |
|
116 *} |
62 |
117 |
63 lemma t_App_elim: |
118 lemma t_App_elim: |
64 assumes a: "\<Gamma> \<turnstile> App t1 t2 : T" |
119 assumes a: "\<Gamma> \<turnstile> App t1 t2 : T" |
65 obtains T' where "\<Gamma> \<turnstile> t1 : T' \<rightarrow> T" "\<Gamma> \<turnstile> t2 : T'" |
120 obtains T' where "\<Gamma> \<turnstile> t1 : T' \<rightarrow> T" "\<Gamma> \<turnstile> t2 : T'" |
66 using a |
121 using a |
79 apply(drule_tac p="(x \<leftrightarrow> xa)" in permute_boolI) |
134 apply(drule_tac p="(x \<leftrightarrow> xa)" in permute_boolI) |
80 apply(perm_simp) |
135 apply(perm_simp) |
81 apply(auto simp add: flip_def swap_fresh_fresh ty_fresh) |
136 apply(auto simp add: flip_def swap_fresh_fresh ty_fresh) |
82 done |
137 done |
83 |
138 |
|
139 |
|
140 section {* EXERCISE 17 *} |
|
141 |
|
142 text {* |
|
143 Fill in the gaps in the t_Lam case. You will need |
|
144 the type substitution lemma proved above. |
|
145 *} |
|
146 |
84 theorem cbv_type_preservation: |
147 theorem cbv_type_preservation: |
85 assumes a: "t \<longrightarrow>cbv t'" |
148 assumes a: "t \<longrightarrow>cbv t'" |
86 and b: "\<Gamma> \<turnstile> t : T" |
149 and b: "\<Gamma> \<turnstile> t : T" |
87 shows "\<Gamma> \<turnstile> t' : T" |
150 shows "\<Gamma> \<turnstile> t' : T" |
88 using a b |
151 using a b |
89 by (nominal_induct avoiding: \<Gamma> T rule: cbv.strong_induct) |
152 proof (nominal_induct avoiding: \<Gamma> T rule: cbv.strong_induct) |
90 (auto elim!: t_Lam_elim t_App_elim simp add: type_substitution ty.eq_iff) |
153 case (cbv1 v x t \<Gamma> T) |
|
154 have fc: "atom x \<sharp> \<Gamma>" by fact |
|
155 have "\<Gamma> \<turnstile> App (Lam [x]. t) v : T" by fact |
|
156 then obtain T' where |
|
157 *: "\<Gamma> \<turnstile> Lam [x]. t : T' \<rightarrow> T" and |
|
158 **: "\<Gamma> \<turnstile> v : T'" by (rule t_App_elim) |
|
159 have "(x, T') # \<Gamma> \<turnstile> t : T" using * fc by (rule t_Lam_elim) (simp add: ty.eq_iff) |
|
160 |
|
161 show "\<Gamma> \<turnstile> t [x ::= v] : T " sorry |
|
162 qed (auto elim!: t_App_elim) |
|
163 |
|
164 text {* |
|
165 We can easily extend this to sequences of cbv* reductions. |
|
166 *} |
91 |
167 |
92 corollary cbvs_type_preservation: |
168 corollary cbvs_type_preservation: |
93 assumes a: "t \<longrightarrow>cbv* t'" |
169 assumes a: "t \<longrightarrow>cbv* t'" |
94 and b: "\<Gamma> \<turnstile> t : T" |
170 and b: "\<Gamma> \<turnstile> t : T" |
95 shows "\<Gamma> \<turnstile> t' : T" |
171 shows "\<Gamma> \<turnstile> t' : T" |