|
1 |
1 theory Tutorial2 |
2 theory Tutorial2 |
2 imports Tutorial1 |
3 imports Lambda |
3 begin |
4 begin |
4 |
5 |
5 (* fixme: put height example here *) |
6 section {* Height of a Lambda-Term *} |
6 |
7 |
7 |
8 text {* |
8 section {* Types *} |
9 The theory Lambda defines the notions of capture-avoiding |
|
10 substitution and the height of lambda terms. |
|
11 *} |
|
12 |
|
13 thm height.simps |
|
14 thm subst.simps |
|
15 |
|
16 subsection {* EXERCISE 7 *} |
|
17 |
|
18 text {* |
|
19 Lets prove a property about the height of substitutions. |
|
20 |
|
21 Assume that the height of a lambda-term is always greater |
|
22 or equal to 1. |
|
23 *} |
|
24 |
|
25 lemma height_ge_one: |
|
26 shows "1 \<le> height t" |
|
27 by (induct t rule: lam.induct) (auto) |
|
28 |
|
29 text {* Remove the sorries *} |
|
30 |
|
31 theorem height_subst: |
|
32 shows "height (t[x ::= t']) \<le> height t - 1 + height t'" |
|
33 proof (induct t rule: lam.induct) |
|
34 case (Var y) |
|
35 show "height (Var y[x ::= t']) \<le> height (Var y) - 1 + height t'" sorry |
|
36 next |
|
37 case (App t1 t2) |
|
38 have ih1: "height (t1[x::=t']) \<le> (height t1) - 1 + height t'" by fact |
|
39 have ih2: "height (t2[x::=t']) \<le> (height t2) - 1 + height t'" by fact |
|
40 |
|
41 show "height ((App t1 t2)[x ::= t']) \<le> height (App t1 t2) - 1 + height t'" sorry |
|
42 next |
|
43 case (Lam y t1) |
|
44 have ih: "height (t1[x::=t']) \<le> height t1 - 1 + height t'" by fact |
|
45 -- {* the definition of capture-avoiding substitution *} |
|
46 thm subst.simps |
|
47 |
|
48 show "height ((Lam [y].t1)[x ::= t']) \<le> height (Lam [y].t1) - 1 + height t'" sorry |
|
49 qed |
|
50 |
|
51 |
|
52 text {* |
|
53 The point is that substitutions can only be moved under a binder |
|
54 provided certain freshness conditions are satisfied. The structural |
|
55 induction above does not say anything about such freshness conditions. |
|
56 |
|
57 Fortunately, Nominal derives automatically some stronger induction |
|
58 principle for lambda terms which has the usual variable convention |
|
59 build in. |
|
60 |
|
61 In the proof below, we use this stronger induction principle. The |
|
62 variable and application case are as before. |
|
63 *} |
|
64 |
|
65 |
|
66 theorem |
|
67 shows "height (t[x ::= t']) \<le> height t - 1 + height t'" |
|
68 proof (nominal_induct t avoiding: x t' rule: lam.strong_induct) |
|
69 case (Var y) |
|
70 have "1 \<le> height t'" using height_ge_one by simp |
|
71 then show "height (Var y[x ::= t']) \<le> height (Var y) - 1 + height t'" by simp |
|
72 next |
|
73 case (App t1 t2) |
|
74 have ih1: "height (t1[x::=t']) \<le> (height t1) - 1 + height t'" |
|
75 and ih2: "height (t2[x::=t']) \<le> (height t2) - 1 + height t'" by fact+ |
|
76 then show "height ((App t1 t2)[x ::= t']) \<le> height (App t1 t2) - 1 + height t'" by simp |
|
77 next |
|
78 case (Lam y t1) |
|
79 have ih: "height (t1[x::=t']) \<le> height t1 - 1 + height t'" by fact |
|
80 have vc: "atom y \<sharp> x" "atom y \<sharp> t'" by fact+ -- {* usual variable convention *} |
|
81 |
|
82 show "height ((Lam [y].t1)[x ::= t']) \<le> height (Lam [y].t1) - 1 + height t'" sorry |
|
83 qed |
|
84 |
|
85 |
|
86 section {* Types and the Weakening Lemma *} |
9 |
87 |
10 nominal_datatype ty = |
88 nominal_datatype ty = |
11 tVar "string" |
89 tVar "string" |
12 | tArr "ty" "ty" ("_ \<rightarrow> _" [100, 100] 100) |
90 | tArr "ty" "ty" (infixr "\<rightarrow>" 100) |
13 |
91 |
14 |
92 |
15 text {* |
93 text {* |
16 Having defined them as nominal datatypes gives us additional |
94 Having defined them as nominal datatypes gives us additional |
17 definitions and theorems that come with types (see below). |
95 definitions and theorems that come with types (see below). |
18 |
96 |
19 We next define the type of typing contexts, a predicate that |
97 We next define the type of typing contexts, a predicate that |
20 defines valid contexts (i.e. lists that contain only unique |
98 defines valid contexts (i.e. lists that contain only unique |
21 variables) and the typing judgement. |
99 variables) and the typing judgement. |
22 |
|
23 *} |
100 *} |
24 |
101 |
25 type_synonym ty_ctx = "(name \<times> ty) list" |
102 type_synonym ty_ctx = "(name \<times> ty) list" |
26 |
103 |
27 inductive |
104 inductive |
105 have a0: "atom x \<sharp> \<Gamma>1" by fact |
182 have a0: "atom x \<sharp> \<Gamma>1" by fact |
106 have a1: "valid \<Gamma>2" by fact |
183 have a1: "valid \<Gamma>2" by fact |
107 have a2: "\<Gamma>1 \<sqsubseteq> \<Gamma>2" by fact |
184 have a2: "\<Gamma>1 \<sqsubseteq> \<Gamma>2" by fact |
108 |
185 |
109 show "\<Gamma>2 \<turnstile> Lam [x].t : T1 \<rightarrow> T2" sorry |
186 show "\<Gamma>2 \<turnstile> Lam [x].t : T1 \<rightarrow> T2" sorry |
110 qed (auto) -- {* the application case *} |
187 qed (auto) -- {* the application case is automatic*} |
111 |
188 |
112 |
189 |
113 text {* |
190 text {* |
114 Despite the frequent claim that the weakening lemma is trivial, |
191 Despite the frequent claim that the weakening lemma is trivial, |
115 routine or obvious, the proof in the lambda-case does not go |
192 routine or obvious, the proof in the lambda-case does not go |
168 ultimately show "\<Gamma>2 \<turnstile> Lam [x].t : T1 \<rightarrow> T2" by simp |
245 ultimately show "\<Gamma>2 \<turnstile> Lam [x].t : T1 \<rightarrow> T2" by simp |
169 qed (auto) -- {* var and app cases, luckily, are automatic *} |
246 qed (auto) -- {* var and app cases, luckily, are automatic *} |
170 |
247 |
171 |
248 |
172 text {* |
249 text {* |
173 The remedy is to use a stronger induction principle that |
250 The remedy is to use again a stronger induction principle that |
174 has the usual "variable convention" already build in. The |
251 has the usual "variable convention" already build in. The |
175 following command derives this induction principle for us. |
252 following command derives this induction principle for the typing |
176 (We shall explain what happens here later.) |
253 relation. (We shall explain what happens here later.) |
177 *} |
254 *} |
178 |
255 |
179 nominal_inductive typing |
256 nominal_inductive typing |
180 avoids t_Lam: "x" |
257 avoids t_Lam: "x" |
181 unfolding fresh_star_def |
258 unfolding fresh_star_def |
182 by (simp_all add: fresh_Pair lam.fresh ty_fresh) |
259 by (simp_all add: fresh_Pair lam.fresh ty_fresh) |
183 |
260 |
184 text {* Compare the two induction principles *} |
261 text {* Compare the two induction principles *} |
185 |
262 |
186 thm typing.induct |
263 thm typing.induct |
187 thm typing.strong_induct -- {* has the additional assumption {atom x} \<sharp> c *} |
264 thm typing.strong_induct -- {* note the additional assumption {atom x} \<sharp> c *} |
188 |
265 |
189 text {* |
266 text {* |
190 We can use the stronger induction principle by replacing |
267 We can use the stronger induction principle by replacing |
191 the line |
268 the line |
192 |
269 |
196 |
273 |
197 proof (nominal_induct avoiding: \<Gamma>2 rule: typing.strong_induct) |
274 proof (nominal_induct avoiding: \<Gamma>2 rule: typing.strong_induct) |
198 |
275 |
199 Try now the proof. |
276 Try now the proof. |
200 *} |
277 *} |
201 |
278 |
|
279 subsection {* EXERCISE 9 *} |
202 |
280 |
203 lemma weakening: |
281 lemma weakening: |
204 assumes a: "\<Gamma>1 \<turnstile> t : T" |
282 assumes a: "\<Gamma>1 \<turnstile> t : T" |
205 and b: "valid \<Gamma>2" |
283 and b: "valid \<Gamma>2" |
206 and c: "\<Gamma>1 \<sqsubseteq> \<Gamma>2" |
284 and c: "\<Gamma>1 \<sqsubseteq> \<Gamma>2" |
207 shows "\<Gamma>2 \<turnstile> t : T" |
285 shows "\<Gamma>2 \<turnstile> t : T" |
208 using a b c |
286 using a b c |
209 proof (nominal_induct avoiding: \<Gamma>2 rule: typing.strong_induct) |
287 proof (nominal_induct avoiding: \<Gamma>2 rule: typing.strong_induct) |
210 case (t_Var \<Gamma>1 x T) -- {* variable case is as before *} |
288 case (t_Var \<Gamma>1 x T) -- {* again the variable case is as before *} |
211 have "\<Gamma>1 \<sqsubseteq> \<Gamma>2" by fact |
289 have "\<Gamma>1 \<sqsubseteq> \<Gamma>2" by fact |
212 moreover |
290 moreover |
213 have "valid \<Gamma>2" by fact |
291 have "valid \<Gamma>2" by fact |
214 moreover |
292 moreover |
215 have "(x, T)\<in> set \<Gamma>1" by fact |
293 have "(x, T)\<in> set \<Gamma>1" by fact |
219 have vc: "atom x \<sharp> \<Gamma>2" by fact -- {* additional fact afforded by the strong induction *} |
297 have vc: "atom x \<sharp> \<Gamma>2" by fact -- {* additional fact afforded by the strong induction *} |
220 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 |
298 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 |
221 have a0: "atom x \<sharp> \<Gamma>1" by fact |
299 have a0: "atom x \<sharp> \<Gamma>1" by fact |
222 have a1: "valid \<Gamma>2" by fact |
300 have a1: "valid \<Gamma>2" by fact |
223 have a2: "\<Gamma>1 \<sqsubseteq> \<Gamma>2" by fact |
301 have a2: "\<Gamma>1 \<sqsubseteq> \<Gamma>2" by fact |
224 have "valid ((x, T1) # \<Gamma>2)" using a1 vc by auto |
302 |
225 moreover |
303 show "\<Gamma>2 \<turnstile> Lam [x].t : T1 \<rightarrow> T2" sorry |
226 have "(x, T1) # \<Gamma>1 \<sqsubseteq> (x, T1) # \<Gamma>2" using a2 by auto |
|
227 ultimately |
|
228 have "(x, T1) # \<Gamma>2 \<turnstile> t : T2" using ih by simp |
|
229 then show "\<Gamma>2 \<turnstile> Lam [x].t : T1 \<rightarrow> T2" using vc by auto |
|
230 qed (auto) -- {* app case *} |
304 qed (auto) -- {* app case *} |
231 |
305 |
232 |
306 |
233 text {* unbind / inconsistency example *} |
307 |
|
308 section {* Unbind and an Inconsistency Example *} |
|
309 |
|
310 text {* |
|
311 You might wonder why we had to discharge some proof |
|
312 obligations in order to obtain the stronger induction |
|
313 principle for the typing relation. (Remember for |
|
314 lambda terms this stronger induction principle is |
|
315 derived automatically.) |
|
316 |
|
317 This proof obligation is really needed, because if we |
|
318 assume universally a stronger induction principle, then |
|
319 in some cases we can derive false. This is "shown" below. |
|
320 *} |
|
321 |
234 |
322 |
235 inductive |
323 inductive |
236 unbind :: "lam \<Rightarrow> lam \<Rightarrow> bool" ("_ \<mapsto> _" [60, 60] 60) |
324 unbind :: "lam \<Rightarrow> lam \<Rightarrow> bool" (infixr "\<mapsto>" 60) |
237 where |
325 where |
238 u_Var[intro]: "Var x \<mapsto> Var x" |
326 u_Var[intro]: "Var x \<mapsto> Var x" |
239 | u_App[intro]: "App t1 t2 \<mapsto> App t1 t2" |
327 | u_App[intro]: "App t1 t2 \<mapsto> App t1 t2" |
240 | u_Lam[intro]: "t \<mapsto> t' \<Longrightarrow> Lam [x].t \<mapsto> t'" |
328 | u_Lam[intro]: "t \<mapsto> t' \<Longrightarrow> Lam [x].t \<mapsto> t'" |
241 |
329 |
|
330 text {* It is clear that the following judgement holds. *} |
|
331 |
242 lemma unbind_simple: |
332 lemma unbind_simple: |
243 shows "Lam [x].Var x \<mapsto> Var x" |
333 shows "Lam [x].Var x \<mapsto> Var x" |
244 by auto |
334 by auto |
245 |
335 |
|
336 text {* |
|
337 Now lets derive the strong induction principle for unbind. |
|
338 The point is that we cannot establish the proof obligations, |
|
339 therefore we force Isabelle to accept them by using "sorry". |
|
340 *} |
|
341 |
246 equivariance unbind |
342 equivariance unbind |
247 |
|
248 nominal_inductive unbind |
343 nominal_inductive unbind |
249 avoids u_Lam: "x" |
344 avoids u_Lam: "x" |
250 sorry |
345 sorry |
|
346 |
|
347 text {* |
|
348 Using the stronger induction principle, we can establish |
|
349 th follwoing bogus property. |
|
350 *} |
251 |
351 |
252 lemma unbind_fake: |
352 lemma unbind_fake: |
253 fixes y::"name" |
353 fixes y::"name" |
254 assumes a: "t \<mapsto> t'" |
354 assumes a: "t \<mapsto> t'" |
255 and b: "atom y \<sharp> t" |
355 and b: "atom y \<sharp> t" |
263 then have in_eq: "x \<noteq> y" by (simp add: fresh_at_base) |
363 then have in_eq: "x \<noteq> y" by (simp add: fresh_at_base) |
264 then have "atom y \<sharp> t" using asm by (simp add: lam.fresh) |
364 then have "atom y \<sharp> t" using asm by (simp add: lam.fresh) |
265 then show "atom y \<sharp> t'" using ih by simp |
365 then show "atom y \<sharp> t'" using ih by simp |
266 qed |
366 qed |
267 |
367 |
|
368 text {* |
|
369 And from this follows the inconsitency: |
|
370 *} |
|
371 |
268 lemma |
372 lemma |
269 shows "False" |
373 shows "False" |
270 proof - |
374 proof - |
271 have "atom x \<sharp> Lam [x]. Var x" by (simp add: lam.fresh) |
375 have "atom x \<sharp> Lam [x]. Var x" by (simp add: lam.fresh) |
272 then have "atom x \<sharp> Var x" using unbind_fake unbind_simple by auto |
376 moreover |
273 then show "False" by (simp add: lam.fresh fresh_at_base) |
377 have "Lam [x]. Var x \<mapsto> Var x" using unbind_simple by auto |
|
378 ultimately |
|
379 have "atom x \<sharp> Var x" using unbind_fake by auto |
|
380 then have "x \<noteq> x" by (simp add: lam.fresh fresh_at_base) |
|
381 then show "False" by simp |
274 qed |
382 qed |
275 |
383 |
276 end |
384 end |