1 (* Title: HOL/Lambda/Type.thy |
1 (* Title: HOL/Lambda/Type.thy |
2 ID: $Id$ |
2 ID: $Id$ |
3 Author: Stefan Berghofer |
3 Author: Stefan Berghofer |
4 Copyright 2000 TU Muenchen |
4 Copyright 2000 TU Muenchen |
5 |
5 |
6 Simply-typed lambda terms. |
6 Simply-typed lambda terms. Subject reduction and strong normalization |
|
7 of simply-typed lambda terms. Partly based on a paper proof by Ralph |
|
8 Matthes. |
7 *) |
9 *) |
8 |
10 |
9 Type = InductTermi + |
11 theory Type = InductTermi: |
10 |
12 |
11 datatype typ = Atom nat |
13 datatype "typ" = |
12 | Fun typ typ (infixr "=>" 200) |
14 Atom nat |
|
15 | Fun "typ" "typ" (infixr "=>" 200) |
13 |
16 |
14 consts |
17 consts |
15 typing :: "((nat => typ) * dB * typ) set" |
18 typing :: "((nat => typ) * dB * typ) set" |
16 |
19 |
17 syntax |
20 syntax |
18 "@type" :: "[nat => typ, dB, typ] => bool" ("_ |- _ : _" [50,50,50] 50) |
21 "_typing" :: "[nat => typ, dB, typ] => bool" ("_ |- _ : _" [50,50,50] 50) |
19 "=>>" :: "[typ list, typ] => typ" (infixl 150) |
22 "_funs" :: "[typ list, typ] => typ" (infixl "=>>" 150) |
20 |
23 |
21 translations |
24 translations |
22 "env |- t : T" == "(env, t, T) : typing" |
25 "env |- t : T" == "(env, t, T) : typing" |
23 "Ts =>> T" == "foldr Fun Ts T" |
26 "Ts =>> T" == "foldr Fun Ts T" |
24 |
27 |
|
28 lemmas [intro!] = IT.BetaI IT.LambdaI IT.VarI |
|
29 |
|
30 (* FIXME |
|
31 declare IT.intros [intro!] |
|
32 *) |
|
33 |
25 inductive typing |
34 inductive typing |
26 intrs |
35 intros (* FIXME [intro!] *) |
27 VAR "env x = T ==> env |- Var x : T" |
36 Var: "env x = T ==> env |- Var x : T" |
28 ABS "(nat_case T env) |- t : U ==> env |- (Abs t) : (T => U)" |
37 Abs: "(nat_case T env) |- t : U ==> env |- (Abs t) : (T => U)" |
29 APP "[| env |- s : T => U; env |- t : T |] ==> env |- (s $ t) : U" |
38 App: "env |- s : T => U ==> env |- t : T ==> env |- (s $ t) : U" |
|
39 |
|
40 lemmas [intro!] = App Abs Var |
30 |
41 |
31 consts |
42 consts |
32 "types" :: "[nat => typ, dB list, typ list] => bool" |
43 "types" :: "[nat => typ, dB list, typ list] => bool" |
33 |
|
34 primrec |
44 primrec |
35 "types e [] Ts = (Ts = [])" |
45 "types e [] Ts = (Ts = [])" |
36 "types e (t # ts) Ts = (case Ts of |
46 "types e (t # ts) Ts = |
|
47 (case Ts of |
37 [] => False |
48 [] => False |
38 | T # Ts => e |- t : T & types e ts Ts)" |
49 | T # Ts => e |- t : T & types e ts Ts)" |
39 |
50 |
|
51 (* FIXME order *) |
|
52 inductive_cases [elim!]: |
|
53 "e |- Abs t : T" |
|
54 "e |- t $ u : T" |
|
55 "e |- Var i : T" |
|
56 |
|
57 inductive_cases [elim!]: |
|
58 "x # xs : lists S" |
|
59 |
|
60 |
|
61 text {* Some tests. *} |
|
62 |
|
63 lemma "\<exists>T U. e |- Abs (Abs (Abs (Var 1 $ (Var 2 $ Var 1 $ Var 0)))) : T \<and> U = T" |
|
64 apply (intro exI conjI) |
|
65 apply force |
|
66 apply (rule refl) |
|
67 done |
|
68 |
|
69 lemma "\<exists>T U. e |- Abs (Abs (Abs (Var 2 $ Var 0 $ (Var 1 $ Var 0)))) : T \<and> U = T"; |
|
70 apply (intro exI conjI) |
|
71 apply force |
|
72 apply (rule refl) |
|
73 done |
|
74 |
|
75 |
|
76 text {* n-ary function types *} |
|
77 |
|
78 lemma list_app_typeD [rulify]: |
|
79 "\<forall>t T. e |- t $$ ts : T --> (\<exists>Ts. e |- t : Ts =>> T \<and> types e ts Ts)" |
|
80 apply (induct_tac ts) |
|
81 apply simp |
|
82 apply (intro strip) |
|
83 apply simp |
|
84 apply (erule_tac x = "t $ a" in allE) |
|
85 apply (erule_tac x = T in allE) |
|
86 apply (erule impE) |
|
87 apply assumption |
|
88 apply (elim exE conjE) |
|
89 apply (ind_cases "e |- t $ u : T") |
|
90 apply (rule_tac x = "Ta # Ts" in exI) |
|
91 apply simp |
|
92 done |
|
93 |
|
94 lemma list_app_typeI [rulify]: |
|
95 "\<forall>t T Ts. e |- t : Ts =>> T --> types e ts Ts --> e |- t $$ ts : T" |
|
96 apply (induct_tac ts) |
|
97 apply (intro strip) |
|
98 apply simp |
|
99 apply (intro strip) |
|
100 apply (case_tac Ts) |
|
101 apply simp |
|
102 apply simp |
|
103 apply (erule_tac x = "t $ a" in allE) |
|
104 apply (erule_tac x = T in allE) |
|
105 apply (erule_tac x = lista in allE) |
|
106 apply (erule impE) |
|
107 apply (erule conjE) |
|
108 apply (erule typing.App) |
|
109 apply assumption |
|
110 apply blast |
|
111 done |
|
112 |
|
113 lemma lists_types [rulify]: |
|
114 "\<forall>Ts. types e ts Ts --> ts : lists {t. \<exists>T. e |- t : T}" |
|
115 apply (induct_tac ts) |
|
116 apply (intro strip) |
|
117 apply (case_tac Ts) |
|
118 apply simp |
|
119 apply (rule lists.Nil) |
|
120 apply simp |
|
121 apply (intro strip) |
|
122 apply (case_tac Ts) |
|
123 apply simp |
|
124 apply simp |
|
125 apply (rule lists.Cons) |
|
126 apply blast |
|
127 apply blast |
|
128 done |
|
129 |
|
130 |
|
131 text {* lifting preserves termination and well-typedness *} |
|
132 |
|
133 lemma lift_map [rulify, simp]: |
|
134 "\<forall>t. lift (t $$ ts) i = lift t i $$ map (\<lambda>t. lift t i) ts" |
|
135 apply (induct_tac ts) |
|
136 apply simp_all |
|
137 done |
|
138 |
|
139 lemma subst_map [rulify, simp]: |
|
140 "\<forall>t. subst (t $$ ts) u i = subst t u i $$ map (\<lambda>t. subst t u i) ts" |
|
141 apply (induct_tac ts) |
|
142 apply simp_all |
|
143 done |
|
144 |
|
145 lemma lift_IT [rulify, intro!]: |
|
146 "t : IT ==> \<forall>i. lift t i : IT" |
|
147 apply (erule IT.induct) |
|
148 apply (rule allI) |
|
149 apply (simp (no_asm)) |
|
150 apply (rule conjI) |
|
151 apply |
|
152 (rule impI, |
|
153 rule IT.VarI, |
|
154 erule lists.induct, |
|
155 simp (no_asm), |
|
156 rule lists.Nil, |
|
157 simp (no_asm), |
|
158 erule IntE, |
|
159 rule lists.Cons, |
|
160 blast, |
|
161 assumption)+ |
|
162 apply auto |
|
163 done |
|
164 |
|
165 lemma lifts_IT [rulify]: |
|
166 "ts : lists IT --> map (\<lambda>t. lift t 0) ts : lists IT" |
|
167 apply (induct_tac ts) |
|
168 apply auto |
|
169 done |
|
170 |
|
171 |
|
172 lemma shift_env [simp]: |
|
173 "nat_case T |
|
174 (\<lambda>j. if j < i then e j else if j = i then Ua else e (j - 1)) = |
|
175 (\<lambda>j. if j < Suc i then nat_case T e j else if j = Suc i then Ua |
|
176 else nat_case T e (j - 1))" |
|
177 apply (rule ext) |
|
178 apply (case_tac j) |
|
179 apply simp |
|
180 apply (case_tac nat) |
|
181 apply simp_all |
|
182 done |
|
183 |
|
184 lemma lift_type' [rulify]: |
|
185 "e |- t : T ==> \<forall>i U. |
|
186 (\<lambda>j. if j < i then e j |
|
187 else if j = i then U |
|
188 else e (j - 1)) |- lift t i : T" |
|
189 apply (erule typing.induct) |
|
190 apply auto |
|
191 done |
|
192 |
|
193 |
|
194 lemma lift_type [intro!]: |
|
195 "e |- t : T ==> nat_case U e |- lift t 0 : T" |
|
196 apply (subgoal_tac |
|
197 "nat_case U e = |
|
198 (\<lambda>j. if j < 0 then e j |
|
199 else if j = 0 then U else e (j - 1))") |
|
200 apply (erule ssubst) |
|
201 apply (erule lift_type') |
|
202 apply (rule ext) |
|
203 apply (case_tac j) |
|
204 apply simp_all |
|
205 done |
|
206 |
|
207 lemma lift_types [rulify]: |
|
208 "\<forall>Ts. types e ts Ts --> |
|
209 types (\<lambda>j. if j < i then e j |
|
210 else if j = i then U |
|
211 else e (j - 1)) (map (\<lambda>t. lift t i) ts) Ts" |
|
212 apply (induct_tac ts) |
|
213 apply simp |
|
214 apply (intro strip) |
|
215 apply (case_tac Ts) |
|
216 apply simp_all |
|
217 apply (rule lift_type') |
|
218 apply (erule conjunct1) |
|
219 done |
|
220 |
|
221 |
|
222 text {* substitution lemma *} |
|
223 |
|
224 lemma subst_lemma [rulify]: |
|
225 "e |- t : T ==> \<forall>e' i U u. |
|
226 e = (\<lambda>j. if j < i then e' j |
|
227 else if j = i then U |
|
228 else e' (j-1)) --> |
|
229 e' |- u : U --> e' |- t[u/i] : T" |
|
230 apply (erule typing.induct) |
|
231 apply (intro strip) |
|
232 apply (case_tac "x = i") |
|
233 apply simp |
|
234 apply (frule linorder_neq_iff [THEN iffD1]) |
|
235 apply (erule disjE) |
|
236 apply simp |
|
237 apply (rule typing.Var) |
|
238 apply assumption |
|
239 apply (frule order_less_not_sym) |
|
240 apply (simp only: subst_gt split: split_if add: if_False) |
|
241 apply (rule typing.Var) |
|
242 apply assumption |
|
243 apply fastsimp |
|
244 apply fastsimp |
|
245 done |
|
246 |
|
247 lemma substs_lemma [rulify]: |
|
248 "e |- u : T ==> |
|
249 \<forall>Ts. types (\<lambda>j. if j < i then e j |
|
250 else if j = i then T else e (j - 1)) ts Ts --> |
|
251 types e (map (%t. t[u/i]) ts) Ts" |
|
252 apply (induct_tac ts) |
|
253 apply (intro strip) |
|
254 apply (case_tac Ts) |
|
255 apply simp |
|
256 apply simp |
|
257 apply (intro strip) |
|
258 apply (case_tac Ts) |
|
259 apply simp |
|
260 apply simp |
|
261 apply (erule conjE) |
|
262 apply (erule subst_lemma) |
|
263 apply (rule refl) |
|
264 apply assumption |
|
265 done |
|
266 |
|
267 |
|
268 text {* subject reduction *} |
|
269 |
|
270 lemma subject_reduction [rulify]: |
|
271 "e |- t : T ==> \<forall>t'. t -> t' --> e |- t' : T" |
|
272 apply (erule typing.induct) |
|
273 apply blast |
|
274 apply blast |
|
275 apply (intro strip) |
|
276 apply (ind_cases "s $ t -> t'") |
|
277 apply hypsubst |
|
278 apply (ind_cases "env |- Abs t : T => U") |
|
279 apply (rule subst_lemma) |
|
280 apply assumption |
|
281 prefer 2 |
|
282 apply assumption |
|
283 apply (rule ext) |
|
284 apply (case_tac j) |
|
285 |
|
286 apply simp |
|
287 apply simp |
|
288 apply fast |
|
289 apply fast |
|
290 (* FIXME apply auto *) |
|
291 done |
|
292 |
|
293 text {* additional lemmas *} |
|
294 |
|
295 lemma app_last: "(t $$ ts) $ u = t $$ (ts @ [u])" |
|
296 apply simp |
|
297 done |
|
298 |
|
299 |
|
300 lemma subst_Var_IT [rulify]: "r : IT ==> \<forall>i j. r[Var i/j] : IT" |
|
301 apply (erule IT.induct) |
|
302 txt {* Var *} |
|
303 apply (intro strip) |
|
304 apply (simp (no_asm) add: subst_Var) |
|
305 apply |
|
306 ((rule conjI impI)+, |
|
307 rule IT.VarI, |
|
308 erule lists.induct, |
|
309 simp (no_asm), |
|
310 rule lists.Nil, |
|
311 simp (no_asm), |
|
312 erule IntE, |
|
313 erule CollectE, |
|
314 rule lists.Cons, |
|
315 fast, |
|
316 assumption)+ |
|
317 txt {* Lambda *} |
|
318 apply (intro strip) |
|
319 apply simp |
|
320 apply (rule IT.LambdaI) |
|
321 apply fast |
|
322 txt {* Beta *} |
|
323 apply (intro strip) |
|
324 apply (simp (no_asm_use) add: subst_subst [symmetric]) |
|
325 apply (rule IT.BetaI) |
|
326 apply auto |
|
327 done |
|
328 |
|
329 lemma Var_IT: "Var n \<in> IT" |
|
330 apply (subgoal_tac "Var n $$ [] \<in> IT") |
|
331 apply simp |
|
332 apply (rule IT.VarI) |
|
333 apply (rule lists.Nil) |
|
334 done |
|
335 |
|
336 lemma app_Var_IT: "t : IT ==> t $ Var i : IT" |
|
337 apply (erule IT.induct) |
|
338 apply (subst app_last) |
|
339 apply (rule IT.VarI) |
|
340 apply simp |
|
341 apply (rule lists.Cons) |
|
342 apply (rule Var_IT) |
|
343 apply (rule lists.Nil) |
|
344 apply (rule IT.BetaI [where ?ss = "[]", unfold foldl_Nil [THEN eq_reflection]]) |
|
345 apply (erule subst_Var_IT) |
|
346 apply (rule Var_IT) |
|
347 apply (subst app_last) |
|
348 apply (rule IT.BetaI) |
|
349 apply (subst app_last [symmetric]) |
|
350 apply assumption |
|
351 apply assumption |
|
352 done |
|
353 |
|
354 |
|
355 text {* Well-typed substitution preserves termination. *} |
|
356 |
|
357 lemma subst_type_IT [rulify]: |
|
358 "\<forall>t. t : IT --> (\<forall>e T u i. |
|
359 (\<lambda>j. if j < i then e j |
|
360 else if j = i then U |
|
361 else e (j - 1)) |- t : T --> |
|
362 u : IT --> e |- u : U --> t[u/i] : IT)" |
|
363 apply (rule_tac f = size and a = U in measure_induct) |
|
364 apply (rule allI) |
|
365 apply (rule impI) |
|
366 apply (erule IT.induct) |
|
367 txt {* Var *} |
|
368 apply (intro strip) |
|
369 apply (case_tac "n = i") |
|
370 txt {* n=i *} |
|
371 apply (case_tac rs) |
|
372 apply simp |
|
373 apply simp |
|
374 apply (drule list_app_typeD) |
|
375 apply (elim exE conjE) |
|
376 apply (ind_cases "e |- t $ u : T") |
|
377 apply (ind_cases "e |- Var i : T") |
|
378 apply (drule_tac s = "(?T::typ) => ?U" in sym) |
|
379 apply simp |
|
380 apply (subgoal_tac "lift u 0 $ Var 0 : IT") |
|
381 prefer 2 |
|
382 apply (rule app_Var_IT) |
|
383 apply (erule lift_IT) |
|
384 apply (subgoal_tac "(lift u 0 $ Var 0)[a[u/i]/0] : IT") |
|
385 apply (simp (no_asm_use)) |
|
386 apply (subgoal_tac "(Var 0 $$ map (%t. lift t 0) |
|
387 (map (%t. t[u/i]) list))[(u $ a[u/i])/0] : IT") |
|
388 apply (simp (no_asm_use) del: map_compose add: map_compose [symmetric] o_def) |
|
389 apply (erule_tac x = "Ts =>> T" in allE) |
|
390 apply (erule impE) |
|
391 apply simp |
|
392 apply (erule_tac x = "Var 0 $$ |
|
393 map (%t. lift t 0) (map (%t. t[u/i]) list)" in allE) |
|
394 apply (erule impE) |
|
395 apply (rule IT.VarI) |
|
396 apply (rule lifts_IT) |
|
397 apply (drule lists_types) |
|
398 apply |
|
399 (ind_cases "x # xs : lists (Collect P)", |
|
400 erule lists_IntI [THEN lists.induct], |
|
401 assumption) |
|
402 apply fastsimp |
|
403 apply fastsimp |
|
404 apply (erule_tac x = e in allE) |
|
405 apply (erule_tac x = T in allE) |
|
406 apply (erule_tac x = "u $ a[u/i]" in allE) |
|
407 apply (erule_tac x = 0 in allE) |
|
408 apply (fastsimp intro!: list_app_typeI lift_types subst_lemma substs_lemma) |
|
409 |
|
410 (* FIXME |
|
411 apply (tactic { * fast_tac (claset() |
|
412 addSIs [thm "list_app_typeI", thm "lift_types", thm "subst_lemma", thm "substs_lemma"] |
|
413 addss simpset()) 1 * }) *) |
|
414 |
|
415 apply (erule_tac x = Ta in allE) |
|
416 apply (erule impE) |
|
417 apply simp |
|
418 apply (erule_tac x = "lift u 0 $ Var 0" in allE) |
|
419 apply (erule impE) |
|
420 apply assumption |
|
421 apply (erule_tac x = e in allE) |
|
422 apply (erule_tac x = "Ts =>> T" in allE) |
|
423 apply (erule_tac x = "a[u/i]" in allE) |
|
424 apply (erule_tac x = 0 in allE) |
|
425 apply (erule impE) |
|
426 apply (rule typing.App) |
|
427 apply (erule lift_type') |
|
428 apply (rule typing.Var) |
|
429 apply simp |
|
430 apply (fast intro!: subst_lemma) |
|
431 txt {* n~=i *} |
|
432 apply (drule list_app_typeD) |
|
433 apply (erule exE) |
|
434 apply (erule conjE) |
|
435 apply (drule lists_types) |
|
436 apply (subgoal_tac "map (%x. x[u/i]) rs : lists IT") |
|
437 apply (simp add: subst_Var) |
|
438 apply fast |
|
439 apply (erule lists_IntI [THEN lists.induct]) |
|
440 apply assumption |
|
441 apply fastsimp |
|
442 apply fastsimp |
|
443 txt {* Lambda *} |
|
444 apply fastsimp |
|
445 txt {* Beta *} |
|
446 apply (intro strip) |
|
447 apply (simp (no_asm)) |
|
448 apply (rule IT.BetaI) |
|
449 apply (simp (no_asm) del: subst_map add: subst_subst subst_map [symmetric]) |
|
450 apply (drule subject_reduction) |
|
451 apply (rule apps_preserves_beta) |
|
452 apply (rule beta.beta) |
|
453 apply fast |
|
454 apply (drule list_app_typeD) |
|
455 apply fast |
|
456 done |
|
457 |
|
458 |
|
459 text {* main theorem: well-typed terms are strongly normalizing *} |
|
460 |
|
461 lemma type_implies_IT: "e |- t : T ==> t : IT" |
|
462 apply (erule typing.induct) |
|
463 apply (rule Var_IT) |
|
464 apply (erule IT.LambdaI) |
|
465 apply (subgoal_tac "(Var 0 $ lift t 0)[s/0] : IT") |
|
466 apply simp |
|
467 apply (rule subst_type_IT) |
|
468 apply (rule lists.Nil [THEN 2 lists.Cons [THEN IT.VarI], unfold foldl_Nil [THEN eq_reflection] |
|
469 foldl_Cons [THEN eq_reflection]]) |
|
470 apply (erule lift_IT) |
|
471 apply (rule typing.App) |
|
472 apply (rule typing.Var) |
|
473 apply simp |
|
474 apply (erule lift_type') |
|
475 apply assumption |
|
476 apply assumption |
|
477 done |
|
478 |
|
479 theorem type_implies_termi: "e |- t : T ==> t : termi beta" |
|
480 apply (rule IT_implies_termi) |
|
481 apply (erule type_implies_IT) |
|
482 done |
|
483 |
40 end |
484 end |