author | haftmann |
Tue, 20 Jul 2010 06:35:29 +0200 | |
changeset 37891 | c26f9d06e82c |
parent 33640 | 0d82107dc07a |
permissions | -rw-r--r-- |
14064 | 1 |
(* Title: HOL/Lambda/StrongNorm.thy |
2 |
Author: Stefan Berghofer |
|
3 |
Copyright 2000 TU Muenchen |
|
4 |
*) |
|
5 |
||
6 |
header {* Strong normalization for simply-typed lambda calculus *} |
|
7 |
||
16417 | 8 |
theory StrongNorm imports Type InductTermi begin |
14064 | 9 |
|
10 |
text {* |
|
11 |
Formalization by Stefan Berghofer. Partly based on a paper proof by |
|
12 |
Felix Joachimski and Ralph Matthes \cite{Matthes-Joachimski-AML}. |
|
13 |
*} |
|
14 |
||
15 |
||
16 |
subsection {* Properties of @{text IT} *} |
|
17 |
||
22271 | 18 |
lemma lift_IT [intro!]: "IT t \<Longrightarrow> IT (lift t i)" |
20503 | 19 |
apply (induct arbitrary: i set: IT) |
14064 | 20 |
apply (simp (no_asm)) |
21 |
apply (rule conjI) |
|
22 |
apply |
|
23 |
(rule impI, |
|
24 |
rule IT.Var, |
|
22271 | 25 |
erule listsp.induct, |
14064 | 26 |
simp (no_asm), |
22271 | 27 |
rule listsp.Nil, |
14064 | 28 |
simp (no_asm), |
22271 | 29 |
rule listsp.Cons, |
14064 | 30 |
blast, |
31 |
assumption)+ |
|
32 |
apply auto |
|
33 |
done |
|
34 |
||
22271 | 35 |
lemma lifts_IT: "listsp IT ts \<Longrightarrow> listsp IT (map (\<lambda>t. lift t 0) ts)" |
14064 | 36 |
by (induct ts) auto |
37 |
||
22271 | 38 |
lemma subst_Var_IT: "IT r \<Longrightarrow> IT (r[Var i/j])" |
20503 | 39 |
apply (induct arbitrary: i j set: IT) |
14064 | 40 |
txt {* Case @{term Var}: *} |
41 |
apply (simp (no_asm) add: subst_Var) |
|
42 |
apply |
|
43 |
((rule conjI impI)+, |
|
44 |
rule IT.Var, |
|
22271 | 45 |
erule listsp.induct, |
14064 | 46 |
simp (no_asm), |
22271 | 47 |
rule listsp.Nil, |
48 |
simp (no_asm), |
|
49 |
rule listsp.Cons, |
|
14064 | 50 |
fast, |
51 |
assumption)+ |
|
52 |
txt {* Case @{term Lambda}: *} |
|
53 |
apply atomize |
|
54 |
apply simp |
|
55 |
apply (rule IT.Lambda) |
|
56 |
apply fast |
|
57 |
txt {* Case @{term Beta}: *} |
|
58 |
apply atomize |
|
59 |
apply (simp (no_asm_use) add: subst_subst [symmetric]) |
|
60 |
apply (rule IT.Beta) |
|
61 |
apply auto |
|
62 |
done |
|
63 |
||
22271 | 64 |
lemma Var_IT: "IT (Var n)" |
65 |
apply (subgoal_tac "IT (Var n \<degree>\<degree> [])") |
|
14064 | 66 |
apply simp |
67 |
apply (rule IT.Var) |
|
22271 | 68 |
apply (rule listsp.Nil) |
14064 | 69 |
done |
70 |
||
22271 | 71 |
lemma app_Var_IT: "IT t \<Longrightarrow> IT (t \<degree> Var i)" |
14064 | 72 |
apply (induct set: IT) |
73 |
apply (subst app_last) |
|
74 |
apply (rule IT.Var) |
|
75 |
apply simp |
|
22271 | 76 |
apply (rule listsp.Cons) |
14064 | 77 |
apply (rule Var_IT) |
22271 | 78 |
apply (rule listsp.Nil) |
14064 | 79 |
apply (rule IT.Beta [where ?ss = "[]", unfolded foldl_Nil [THEN eq_reflection]]) |
80 |
apply (erule subst_Var_IT) |
|
81 |
apply (rule Var_IT) |
|
82 |
apply (subst app_last) |
|
83 |
apply (rule IT.Beta) |
|
84 |
apply (subst app_last [symmetric]) |
|
85 |
apply assumption |
|
86 |
apply assumption |
|
87 |
done |
|
88 |
||
89 |
||
90 |
subsection {* Well-typed substitution preserves termination *} |
|
91 |
||
92 |
lemma subst_type_IT: |
|
22271 | 93 |
"\<And>t e T u i. IT t \<Longrightarrow> e\<langle>i:U\<rangle> \<turnstile> t : T \<Longrightarrow> |
94 |
IT u \<Longrightarrow> e \<turnstile> u : U \<Longrightarrow> IT (t[u/i])" |
|
14064 | 95 |
(is "PROP ?P U" is "\<And>t e T u i. _ \<Longrightarrow> PROP ?Q t e T u i U") |
96 |
proof (induct U) |
|
97 |
fix T t |
|
98 |
assume MI1: "\<And>T1 T2. T = T1 \<Rightarrow> T2 \<Longrightarrow> PROP ?P T1" |
|
99 |
assume MI2: "\<And>T1 T2. T = T1 \<Rightarrow> T2 \<Longrightarrow> PROP ?P T2" |
|
22271 | 100 |
assume "IT t" |
14064 | 101 |
thus "\<And>e T' u i. PROP ?Q t e T' u i T" |
102 |
proof induct |
|
103 |
fix e T' u i |
|
22271 | 104 |
assume uIT: "IT u" |
14064 | 105 |
assume uT: "e \<turnstile> u : T" |
106 |
{ |
|
22271 | 107 |
case (Var rs n e_ T'_ u_ i_) |
14064 | 108 |
assume nT: "e\<langle>i:T\<rangle> \<turnstile> Var n \<degree>\<degree> rs : T'" |
22271 | 109 |
let ?ty = "\<lambda>t. \<exists>T'. e\<langle>i:T\<rangle> \<turnstile> t : T'" |
14064 | 110 |
let ?R = "\<lambda>t. \<forall>e T' u i. |
22271 | 111 |
e\<langle>i:T\<rangle> \<turnstile> t : T' \<longrightarrow> IT u \<longrightarrow> e \<turnstile> u : T \<longrightarrow> IT (t[u/i])" |
112 |
show "IT ((Var n \<degree>\<degree> rs)[u/i])" |
|
14064 | 113 |
proof (cases "n = i") |
114 |
case True |
|
115 |
show ?thesis |
|
116 |
proof (cases rs) |
|
117 |
case Nil |
|
118 |
with uIT True show ?thesis by simp |
|
119 |
next |
|
120 |
case (Cons a as) |
|
121 |
with nT have "e\<langle>i:T\<rangle> \<turnstile> Var n \<degree> a \<degree>\<degree> as : T'" by simp |
|
122 |
then obtain Ts |
|
123 |
where headT: "e\<langle>i:T\<rangle> \<turnstile> Var n \<degree> a : Ts \<Rrightarrow> T'" |
|
124 |
and argsT: "e\<langle>i:T\<rangle> \<tturnstile> as : Ts" |
|
125 |
by (rule list_app_typeE) |
|
126 |
from headT obtain T'' |
|
127 |
where varT: "e\<langle>i:T\<rangle> \<turnstile> Var n : T'' \<Rightarrow> Ts \<Rrightarrow> T'" |
|
128 |
and argT: "e\<langle>i:T\<rangle> \<turnstile> a : T''" |
|
129 |
by cases simp_all |
|
130 |
from varT True have T: "T = T'' \<Rightarrow> Ts \<Rrightarrow> T'" |
|
131 |
by cases auto |
|
132 |
with uT have uT': "e \<turnstile> u : T'' \<Rightarrow> Ts \<Rrightarrow> T'" by simp |
|
22271 | 133 |
from T have "IT ((Var 0 \<degree>\<degree> map (\<lambda>t. lift t 0) |
134 |
(map (\<lambda>t. t[u/i]) as))[(u \<degree> a[u/i])/0])" |
|
14064 | 135 |
proof (rule MI2) |
22271 | 136 |
from T have "IT ((lift u 0 \<degree> Var 0)[a[u/i]/0])" |
14064 | 137 |
proof (rule MI1) |
23464 | 138 |
have "IT (lift u 0)" by (rule lift_IT [OF uIT]) |
22271 | 139 |
thus "IT (lift u 0 \<degree> Var 0)" by (rule app_Var_IT) |
14064 | 140 |
show "e\<langle>0:T''\<rangle> \<turnstile> lift u 0 \<degree> Var 0 : Ts \<Rrightarrow> T'" |
141 |
proof (rule typing.App) |
|
142 |
show "e\<langle>0:T''\<rangle> \<turnstile> lift u 0 : T'' \<Rightarrow> Ts \<Rrightarrow> T'" |
|
143 |
by (rule lift_type) (rule uT') |
|
144 |
show "e\<langle>0:T''\<rangle> \<turnstile> Var 0 : T''" |
|
145 |
by (rule typing.Var) simp |
|
146 |
qed |
|
147 |
from Var have "?R a" by cases (simp_all add: Cons) |
|
22271 | 148 |
with argT uIT uT show "IT (a[u/i])" by simp |
14064 | 149 |
from argT uT show "e \<turnstile> a[u/i] : T''" |
150 |
by (rule subst_lemma) simp |
|
151 |
qed |
|
22271 | 152 |
thus "IT (u \<degree> a[u/i])" by simp |
153 |
from Var have "listsp ?R as" |
|
14064 | 154 |
by cases (simp_all add: Cons) |
22271 | 155 |
moreover from argsT have "listsp ?ty as" |
14064 | 156 |
by (rule lists_typings) |
22271 | 157 |
ultimately have "listsp (\<lambda>t. ?R t \<and> ?ty t) as" |
158 |
by simp |
|
159 |
hence "listsp IT (map (\<lambda>t. lift t 0) (map (\<lambda>t. t[u/i]) as))" |
|
160 |
(is "listsp IT (?ls as)") |
|
14064 | 161 |
proof induct |
162 |
case Nil |
|
163 |
show ?case by fastsimp |
|
164 |
next |
|
165 |
case (Cons b bs) |
|
166 |
hence I: "?R b" by simp |
|
167 |
from Cons obtain U where "e\<langle>i:T\<rangle> \<turnstile> b : U" by fast |
|
22271 | 168 |
with uT uIT I have "IT (b[u/i])" by simp |
169 |
hence "IT (lift (b[u/i]) 0)" by (rule lift_IT) |
|
170 |
hence "listsp IT (lift (b[u/i]) 0 # ?ls bs)" |
|
171 |
by (rule listsp.Cons) (rule Cons) |
|
14064 | 172 |
thus ?case by simp |
173 |
qed |
|
22271 | 174 |
thus "IT (Var 0 \<degree>\<degree> ?ls as)" by (rule IT.Var) |
14064 | 175 |
have "e\<langle>0:Ts \<Rrightarrow> T'\<rangle> \<turnstile> Var 0 : Ts \<Rrightarrow> T'" |
176 |
by (rule typing.Var) simp |
|
177 |
moreover from uT argsT have "e \<tturnstile> map (\<lambda>t. t[u/i]) as : Ts" |
|
178 |
by (rule substs_lemma) |
|
179 |
hence "e\<langle>0:Ts \<Rrightarrow> T'\<rangle> \<tturnstile> ?ls as : Ts" |
|
180 |
by (rule lift_types) |
|
181 |
ultimately show "e\<langle>0:Ts \<Rrightarrow> T'\<rangle> \<turnstile> Var 0 \<degree>\<degree> ?ls as : T'" |
|
182 |
by (rule list_app_typeI) |
|
183 |
from argT uT have "e \<turnstile> a[u/i] : T''" |
|
184 |
by (rule subst_lemma) (rule refl) |
|
185 |
with uT' show "e \<turnstile> u \<degree> a[u/i] : Ts \<Rrightarrow> T'" |
|
186 |
by (rule typing.App) |
|
187 |
qed |
|
188 |
with Cons True show ?thesis |
|
33640 | 189 |
by (simp add: comp_def) |
14064 | 190 |
qed |
191 |
next |
|
192 |
case False |
|
22271 | 193 |
from Var have "listsp ?R rs" by simp |
14064 | 194 |
moreover from nT obtain Ts where "e\<langle>i:T\<rangle> \<tturnstile> rs : Ts" |
195 |
by (rule list_app_typeE) |
|
22271 | 196 |
hence "listsp ?ty rs" by (rule lists_typings) |
197 |
ultimately have "listsp (\<lambda>t. ?R t \<and> ?ty t) rs" |
|
198 |
by simp |
|
199 |
hence "listsp IT (map (\<lambda>x. x[u/i]) rs)" |
|
14064 | 200 |
proof induct |
201 |
case Nil |
|
202 |
show ?case by fastsimp |
|
203 |
next |
|
204 |
case (Cons a as) |
|
205 |
hence I: "?R a" by simp |
|
206 |
from Cons obtain U where "e\<langle>i:T\<rangle> \<turnstile> a : U" by fast |
|
22271 | 207 |
with uT uIT I have "IT (a[u/i])" by simp |
208 |
hence "listsp IT (a[u/i] # map (\<lambda>t. t[u/i]) as)" |
|
209 |
by (rule listsp.Cons) (rule Cons) |
|
14064 | 210 |
thus ?case by simp |
211 |
qed |
|
212 |
with False show ?thesis by (auto simp add: subst_Var) |
|
213 |
qed |
|
214 |
next |
|
215 |
case (Lambda r e_ T'_ u_ i_) |
|
216 |
assume "e\<langle>i:T\<rangle> \<turnstile> Abs r : T'" |
|
217 |
and "\<And>e T' u i. PROP ?Q r e T' u i T" |
|
22271 | 218 |
with uIT uT show "IT (Abs r[u/i])" |
14064 | 219 |
by fastsimp |
220 |
next |
|
221 |
case (Beta r a as e_ T'_ u_ i_) |
|
222 |
assume T: "e\<langle>i:T\<rangle> \<turnstile> Abs r \<degree> a \<degree>\<degree> as : T'" |
|
223 |
assume SI1: "\<And>e T' u i. PROP ?Q (r[a/0] \<degree>\<degree> as) e T' u i T" |
|
224 |
assume SI2: "\<And>e T' u i. PROP ?Q a e T' u i T" |
|
22271 | 225 |
have "IT (Abs (r[lift u 0/Suc i]) \<degree> a[u/i] \<degree>\<degree> map (\<lambda>t. t[u/i]) as)" |
14064 | 226 |
proof (rule IT.Beta) |
227 |
have "Abs r \<degree> a \<degree>\<degree> as \<rightarrow>\<^sub>\<beta> r[a/0] \<degree>\<degree> as" |
|
228 |
by (rule apps_preserves_beta) (rule beta.beta) |
|
229 |
with T have "e\<langle>i:T\<rangle> \<turnstile> r[a/0] \<degree>\<degree> as : T'" |
|
230 |
by (rule subject_reduction) |
|
22271 | 231 |
hence "IT ((r[a/0] \<degree>\<degree> as)[u/i])" |
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
23750
diff
changeset
|
232 |
using uIT uT by (rule SI1) |
22271 | 233 |
thus "IT (r[lift u 0/Suc i][a[u/i]/0] \<degree>\<degree> map (\<lambda>t. t[u/i]) as)" |
14064 | 234 |
by (simp del: subst_map add: subst_subst subst_map [symmetric]) |
235 |
from T obtain U where "e\<langle>i:T\<rangle> \<turnstile> Abs r \<degree> a : U" |
|
236 |
by (rule list_app_typeE) fast |
|
237 |
then obtain T'' where "e\<langle>i:T\<rangle> \<turnstile> a : T''" by cases simp_all |
|
23464 | 238 |
thus "IT (a[u/i])" using uIT uT by (rule SI2) |
14064 | 239 |
qed |
22271 | 240 |
thus "IT ((Abs r \<degree> a \<degree>\<degree> as)[u/i])" by simp |
14064 | 241 |
} |
242 |
qed |
|
243 |
qed |
|
244 |
||
245 |
||
246 |
subsection {* Well-typed terms are strongly normalizing *} |
|
247 |
||
18257 | 248 |
lemma type_implies_IT: |
249 |
assumes "e \<turnstile> t : T" |
|
22271 | 250 |
shows "IT t" |
23464 | 251 |
using assms |
18257 | 252 |
proof induct |
253 |
case Var |
|
254 |
show ?case by (rule Var_IT) |
|
255 |
next |
|
256 |
case Abs |
|
23464 | 257 |
show ?case by (rule IT.Lambda) (rule Abs) |
18257 | 258 |
next |
22271 | 259 |
case (App e s T U t) |
260 |
have "IT ((Var 0 \<degree> lift t 0)[s/0])" |
|
18257 | 261 |
proof (rule subst_type_IT) |
23464 | 262 |
have "IT (lift t 0)" using `IT t` by (rule lift_IT) |
22271 | 263 |
hence "listsp IT [lift t 0]" by (rule listsp.Cons) (rule listsp.Nil) |
264 |
hence "IT (Var 0 \<degree>\<degree> [lift t 0])" by (rule IT.Var) |
|
18257 | 265 |
also have "Var 0 \<degree>\<degree> [lift t 0] = Var 0 \<degree> lift t 0" by simp |
22271 | 266 |
finally show "IT \<dots>" . |
18257 | 267 |
have "e\<langle>0:T \<Rightarrow> U\<rangle> \<turnstile> Var 0 : T \<Rightarrow> U" |
268 |
by (rule typing.Var) simp |
|
269 |
moreover have "e\<langle>0:T \<Rightarrow> U\<rangle> \<turnstile> lift t 0 : T" |
|
23464 | 270 |
by (rule lift_type) (rule App.hyps) |
18257 | 271 |
ultimately show "e\<langle>0:T \<Rightarrow> U\<rangle> \<turnstile> Var 0 \<degree> lift t 0 : U" |
272 |
by (rule typing.App) |
|
23464 | 273 |
show "IT s" by fact |
274 |
show "e \<turnstile> s : T \<Rightarrow> U" by fact |
|
14064 | 275 |
qed |
18257 | 276 |
thus ?case by simp |
14064 | 277 |
qed |
278 |
||
23750 | 279 |
theorem type_implies_termi: "e \<turnstile> t : T \<Longrightarrow> termip beta t" |
14064 | 280 |
proof - |
281 |
assume "e \<turnstile> t : T" |
|
22271 | 282 |
hence "IT t" by (rule type_implies_IT) |
14064 | 283 |
thus ?thesis by (rule IT_implies_termi) |
284 |
qed |
|
285 |
||
286 |
end |