|
1 theory Tutorial2 |
|
2 imports Tutorial1 |
|
3 begin |
|
4 |
|
5 (* fixme: put height example here *) |
|
6 |
|
7 |
|
8 section {* Types *} |
|
9 |
|
10 nominal_datatype ty = |
|
11 tVar "string" |
|
12 | tArr "ty" "ty" ("_ \<rightarrow> _" [100, 100] 100) |
|
13 |
|
14 |
|
15 text {* |
|
16 Having defined them as nominal datatypes gives us additional |
|
17 definitions and theorems that come with types (see below). |
|
18 |
|
19 We next define the type of typing contexts, a predicate that |
|
20 defines valid contexts (i.e. lists that contain only unique |
|
21 variables) and the typing judgement. |
|
22 |
|
23 *} |
|
24 |
|
25 type_synonym ty_ctx = "(name \<times> ty) list" |
|
26 |
|
27 |
|
28 inductive |
|
29 valid :: "ty_ctx \<Rightarrow> bool" |
|
30 where |
|
31 v1[intro]: "valid []" |
|
32 | v2[intro]: "\<lbrakk>valid \<Gamma>; atom x \<sharp> \<Gamma>\<rbrakk>\<Longrightarrow> valid ((x, T) # \<Gamma>)" |
|
33 |
|
34 |
|
35 inductive |
|
36 typing :: "ty_ctx \<Rightarrow> lam \<Rightarrow> ty \<Rightarrow> bool" ("_ \<turnstile> _ : _" [60, 60, 60] 60) |
|
37 where |
|
38 t_Var[intro]: "\<lbrakk>valid \<Gamma>; (x, T) \<in> set \<Gamma>\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> Var x : T" |
|
39 | t_App[intro]: "\<lbrakk>\<Gamma> \<turnstile> t1 : T1 \<rightarrow> T2; \<Gamma> \<turnstile> t2 : T1\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> App t1 t2 : T2" |
|
40 | t_Lam[intro]: "\<lbrakk>atom x \<sharp> \<Gamma>; (x, T1) # \<Gamma> \<turnstile> t : T2\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> Lam [x].t : T1 \<rightarrow> T2" |
|
41 |
|
42 |
|
43 text {* |
|
44 The predicate atom x \<sharp> \<Gamma>, read as x fresh for \<Gamma>, is defined by |
|
45 Nominal Isabelle. It is defined for lambda-terms, products, lists etc. |
|
46 For example we have: |
|
47 *} |
|
48 |
|
49 lemma |
|
50 fixes x::"name" |
|
51 shows "atom x \<sharp> Lam [x].t" |
|
52 and "atom x \<sharp> (t1, t2) \<Longrightarrow> atom x \<sharp> App t1 t2" |
|
53 and "atom x \<sharp> Var y \<Longrightarrow> atom x \<sharp> y" |
|
54 and "\<lbrakk>atom x \<sharp> t1; atom x \<sharp> t2\<rbrakk> \<Longrightarrow> atom x \<sharp> (t1, t2)" |
|
55 and "\<lbrakk>atom x \<sharp> l1; atom x \<sharp> l2\<rbrakk> \<Longrightarrow> atom x \<sharp> (l1 @ l2)" |
|
56 and "atom x \<sharp> y \<Longrightarrow> x \<noteq> y" |
|
57 by (simp_all add: lam.fresh fresh_append fresh_at_base) |
|
58 |
|
59 text {* |
|
60 We can also prove that every variable is fresh for a type. |
|
61 *} |
|
62 |
|
63 lemma ty_fresh: |
|
64 fixes x::"name" |
|
65 and T::"ty" |
|
66 shows "atom x \<sharp> T" |
|
67 by (induct T rule: ty.induct) |
|
68 (simp_all add: ty.fresh pure_fresh) |
|
69 |
|
70 text {* |
|
71 In order to state the weakening lemma in a convenient form, we |
|
72 using the following abbreviation. Abbreviations behave like |
|
73 definitions, except that they are always automatically folded |
|
74 and unfolded. |
|
75 *} |
|
76 |
|
77 abbreviation |
|
78 "sub_ty_ctx" :: "ty_ctx \<Rightarrow> ty_ctx \<Rightarrow> bool" ("_ \<sqsubseteq> _" [60, 60] 60) |
|
79 where |
|
80 "\<Gamma>1 \<sqsubseteq> \<Gamma>2 \<equiv> \<forall>x. x \<in> set \<Gamma>1 \<longrightarrow> x \<in> set \<Gamma>2" |
|
81 |
|
82 |
|
83 subsection {* EXERCISE 4 *} |
|
84 |
|
85 text {* |
|
86 Fill in the details and give a proof of the weakening lemma. |
|
87 *} |
|
88 |
|
89 lemma |
|
90 assumes a: "\<Gamma>1 \<turnstile> t : T" |
|
91 and b: "valid \<Gamma>2" |
|
92 and c: "\<Gamma>1 \<sqsubseteq> \<Gamma>2" |
|
93 shows "\<Gamma>2 \<turnstile> t : T" |
|
94 using a b c |
|
95 proof (induct arbitrary: \<Gamma>2) |
|
96 case (t_Var \<Gamma>1 x T) |
|
97 have a1: "valid \<Gamma>1" by fact |
|
98 have a2: "(x, T) \<in> set \<Gamma>1" by fact |
|
99 have a3: "valid \<Gamma>2" by fact |
|
100 have a4: "\<Gamma>1 \<sqsubseteq> \<Gamma>2" by fact |
|
101 |
|
102 show "\<Gamma>2 \<turnstile> Var x : T" sorry |
|
103 next |
|
104 case (t_Lam x \<Gamma>1 T1 t T2) |
|
105 have ih: "\<And>\<Gamma>3. \<lbrakk>valid \<Gamma>3; (x, T1) # \<Gamma>1 \<sqsubseteq> \<Gamma>3\<rbrakk> \<Longrightarrow> \<Gamma>3 \<turnstile> t : T2" by fact |
|
106 have a0: "atom x \<sharp> \<Gamma>1" by fact |
|
107 have a1: "valid \<Gamma>2" by fact |
|
108 have a2: "\<Gamma>1 \<sqsubseteq> \<Gamma>2" by fact |
|
109 |
|
110 show "\<Gamma>2 \<turnstile> Lam [x].t : T1 \<rightarrow> T2" sorry |
|
111 qed (auto) -- {* the application case *} |
|
112 |
|
113 |
|
114 text {* |
|
115 Despite the frequent claim that the weakening lemma is trivial, |
|
116 routine or obvious, the proof in the lambda-case does not go |
|
117 through smoothly. Painful variable renamings seem to be necessary. |
|
118 But the proof using renamings is horribly complicated (see below). |
|
119 *} |
|
120 |
|
121 equivariance valid |
|
122 equivariance typing |
|
123 |
|
124 lemma weakening_NOT_TO_BE_TRIED_AT_HOME: |
|
125 assumes a: "\<Gamma>1 \<turnstile> t : T" |
|
126 and b: "valid \<Gamma>2" |
|
127 and c: "\<Gamma>1 \<sqsubseteq> \<Gamma>2" |
|
128 shows "\<Gamma>2 \<turnstile> t : T" |
|
129 using a b c |
|
130 proof (induct arbitrary: \<Gamma>2) |
|
131 -- {* lambda case *} |
|
132 case (t_Lam x \<Gamma>1 T1 t T2) |
|
133 have fc0: "atom x \<sharp> \<Gamma>1" by fact |
|
134 have ih: "\<And>\<Gamma>3. \<lbrakk>valid \<Gamma>3; (x, T1) # \<Gamma>1 \<sqsubseteq> \<Gamma>3\<rbrakk> \<Longrightarrow> \<Gamma>3 \<turnstile> t : T2" by fact |
|
135 -- {* we choose a fresh variable *} |
|
136 obtain c::"name" where fc1: "atom c \<sharp> (x, t, \<Gamma>1, \<Gamma>2)" by (rule obtain_fresh) |
|
137 -- {* we alpha-rename the abstraction *} |
|
138 have "Lam [c].((c \<leftrightarrow> x) \<bullet> t) = Lam [x].t" using fc1 |
|
139 by (auto simp add: lam.eq_iff Abs1_eq_iff flip_def) |
|
140 moreover |
|
141 -- {* we can then alpha rename the goal *} |
|
142 have "\<Gamma>2 \<turnstile> Lam [c].((c \<leftrightarrow> x) \<bullet> t) : T1 \<rightarrow> T2" |
|
143 proof - |
|
144 -- {* we need to establish *} |
|
145 -- {* (1) (x, T1) # \<Gamma>1 \<sqsubseteq> (x, T1) # ((c \<leftrightarrow> x) \<bullet> \<Gamma>2) *} |
|
146 -- {* (2) valid ((x, T1) # ((c \<leftrightarrow> x) \<bullet> \<Gamma>2)) *} |
|
147 have "(1)": "(x, T1) # \<Gamma>1 \<sqsubseteq> (x, T1) # ((c \<leftrightarrow> x) \<bullet> \<Gamma>2)" |
|
148 proof - |
|
149 have "\<Gamma>1 \<sqsubseteq> \<Gamma>2" by fact |
|
150 then have "(c \<leftrightarrow> x) \<bullet> ((x, T1) # \<Gamma>1 \<sqsubseteq> (x, T1) # ((c \<leftrightarrow> x) \<bullet> \<Gamma>2))" using fc0 fc1 |
|
151 by (perm_simp) (simp add: flip_fresh_fresh) |
|
152 then show "(x, T1) # \<Gamma>1 \<sqsubseteq> (x, T1) # ((c \<leftrightarrow> x) \<bullet> \<Gamma>2)" by (rule permute_boolE) |
|
153 qed |
|
154 moreover |
|
155 have "(2)": "valid ((x, T1) # ((c \<leftrightarrow> x) \<bullet> \<Gamma>2))" |
|
156 proof - |
|
157 have "valid \<Gamma>2" by fact |
|
158 then show "valid ((x, T1) # ((c \<leftrightarrow> x) \<bullet> \<Gamma>2))" using fc1 |
|
159 by (auto simp add: fresh_permute_left atom_eqvt valid.eqvt) |
|
160 qed |
|
161 -- {* these two facts give us by induction hypothesis the following *} |
|
162 ultimately have "(x, T1) # ((c \<leftrightarrow> x) \<bullet> \<Gamma>2) \<turnstile> t : T2" using ih by simp |
|
163 -- {* we now apply renamings to get to our goal *} |
|
164 then have "(c \<leftrightarrow> x) \<bullet> ((x, T1) # ((c \<leftrightarrow> x) \<bullet> \<Gamma>2) \<turnstile> t : T2)" by (rule permute_boolI) |
|
165 then have "(c, T1) # \<Gamma>2 \<turnstile> ((c \<leftrightarrow> x) \<bullet> t) : T2" using fc1 |
|
166 by (perm_simp) (simp add: flip_fresh_fresh ty_fresh) |
|
167 then show "\<Gamma>2 \<turnstile> Lam [c].((c \<leftrightarrow> x) \<bullet> t) : T1 \<rightarrow> T2" using fc1 by auto |
|
168 qed |
|
169 ultimately show "\<Gamma>2 \<turnstile> Lam [x].t : T1 \<rightarrow> T2" by simp |
|
170 qed (auto) -- {* var and app cases, luckily, are automatic *} |
|
171 |
|
172 |
|
173 text {* |
|
174 The remedy is to use a stronger induction principle that |
|
175 has the usual "variable convention" already build in. The |
|
176 following command derives this induction principle for us. |
|
177 (We shall explain what happens here later.) |
|
178 *} |
|
179 |
|
180 nominal_inductive typing |
|
181 avoids t_Lam: "x" |
|
182 unfolding fresh_star_def |
|
183 by (simp_all add: fresh_Pair lam.fresh ty_fresh) |
|
184 |
|
185 text {* Compare the two induction principles *} |
|
186 |
|
187 thm typing.induct |
|
188 thm typing.strong_induct -- {* has the additional assumption {atom x} \<sharp> c *} |
|
189 |
|
190 text {* |
|
191 We can use the stronger induction principle by replacing |
|
192 the line |
|
193 |
|
194 proof (induct arbitrary: \<Gamma>2) |
|
195 |
|
196 with |
|
197 |
|
198 proof (nominal_induct avoiding: \<Gamma>2 rule: typing.strong_induct) |
|
199 |
|
200 Try now the proof. |
|
201 *} |
|
202 |
|
203 |
|
204 lemma weakening: |
|
205 assumes a: "\<Gamma>1 \<turnstile> t : T" |
|
206 and b: "valid \<Gamma>2" |
|
207 and c: "\<Gamma>1 \<sqsubseteq> \<Gamma>2" |
|
208 shows "\<Gamma>2 \<turnstile> t : T" |
|
209 using a b c |
|
210 proof (nominal_induct avoiding: \<Gamma>2 rule: typing.strong_induct) |
|
211 case (t_Var \<Gamma>1 x T) -- {* variable case is as before *} |
|
212 have "\<Gamma>1 \<sqsubseteq> \<Gamma>2" by fact |
|
213 moreover |
|
214 have "valid \<Gamma>2" by fact |
|
215 moreover |
|
216 have "(x, T)\<in> set \<Gamma>1" by fact |
|
217 ultimately show "\<Gamma>2 \<turnstile> Var x : T" by auto |
|
218 next |
|
219 case (t_Lam x \<Gamma>1 T1 t T2) |
|
220 have vc: "atom x \<sharp> \<Gamma>2" by fact -- {* additional fact afforded by the strong induction *} |
|
221 have ih: "\<And>\<Gamma>3. \<lbrakk>valid \<Gamma>3; (x, T1) # \<Gamma>1 \<sqsubseteq> \<Gamma>3\<rbrakk> \<Longrightarrow> \<Gamma>3 \<turnstile> t : T2" by fact |
|
222 have a0: "atom x \<sharp> \<Gamma>1" by fact |
|
223 have a1: "valid \<Gamma>2" by fact |
|
224 have a2: "\<Gamma>1 \<sqsubseteq> \<Gamma>2" by fact |
|
225 have "valid ((x, T1) # \<Gamma>2)" using a1 vc by auto |
|
226 moreover |
|
227 have "(x, T1) # \<Gamma>1 \<sqsubseteq> (x, T1) # \<Gamma>2" using a2 by auto |
|
228 ultimately |
|
229 have "(x, T1) # \<Gamma>2 \<turnstile> t : T2" using ih by simp |
|
230 then show "\<Gamma>2 \<turnstile> Lam [x].t : T1 \<rightarrow> T2" using vc by auto |
|
231 qed (auto) -- {* app case *} |
|
232 |
|
233 |
|
234 text {* unbind / inconsistency example *} |
|
235 |
|
236 inductive |
|
237 unbind :: "lam \<Rightarrow> lam \<Rightarrow> bool" ("_ \<mapsto> _" [60, 60] 60) |
|
238 where |
|
239 u_Var[intro]: "Var x \<mapsto> Var x" |
|
240 | u_App[intro]: "App t1 t2 \<mapsto> App t1 t2" |
|
241 | u_Lam[intro]: "t \<mapsto> t' \<Longrightarrow> Lam [x].t \<mapsto> t'" |
|
242 |
|
243 lemma unbind_simple: |
|
244 shows "Lam [x].Var x \<mapsto> Var x" |
|
245 by auto |
|
246 |
|
247 equivariance unbind |
|
248 |
|
249 nominal_inductive unbind |
|
250 avoids u_Lam: "x" |
|
251 sorry |
|
252 |
|
253 lemma unbind_fake: |
|
254 fixes y::"name" |
|
255 assumes a: "t \<mapsto> t'" |
|
256 and b: "atom y \<sharp> t" |
|
257 shows "atom y \<sharp> t'" |
|
258 using a b |
|
259 proof (nominal_induct avoiding: y rule: unbind.strong_induct) |
|
260 case (u_Lam t t' x y) |
|
261 have ih: "atom y \<sharp> t \<Longrightarrow> atom y \<sharp> t'" by fact |
|
262 have asm: "atom y \<sharp> Lam [x]. t" by fact |
|
263 have fc: "atom x \<sharp> y" by fact |
|
264 then have in_eq: "x \<noteq> y" by (simp add: fresh_at_base) |
|
265 then have "atom y \<sharp> t" using asm by (simp add: lam.fresh) |
|
266 then show "atom y \<sharp> t'" using ih by simp |
|
267 qed |
|
268 |
|
269 lemma |
|
270 shows "False" |
|
271 proof - |
|
272 have "atom x \<sharp> Lam [x]. Var x" by (simp add: lam.fresh) |
|
273 then have "atom x \<sharp> Var x" using unbind_fake unbind_simple by auto |
|
274 then show "False" by (simp add: lam.fresh fresh_at_base) |
|
275 qed |
|
276 |
|
277 end |