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 |
|
8 theory StrongNorm imports Type InductTermi begin |
|
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 |
|
18 lemma lift_IT [intro!]: "IT t \<Longrightarrow> IT (lift t i)" |
|
19 apply (induct arbitrary: i set: IT) |
|
20 apply (simp (no_asm)) |
|
21 apply (rule conjI) |
|
22 apply |
|
23 (rule impI, |
|
24 rule IT.Var, |
|
25 erule listsp.induct, |
|
26 simp (no_asm), |
|
27 rule listsp.Nil, |
|
28 simp (no_asm), |
|
29 rule listsp.Cons, |
|
30 blast, |
|
31 assumption)+ |
|
32 apply auto |
|
33 done |
|
34 |
|
35 lemma lifts_IT: "listsp IT ts \<Longrightarrow> listsp IT (map (\<lambda>t. lift t 0) ts)" |
|
36 by (induct ts) auto |
|
37 |
|
38 lemma subst_Var_IT: "IT r \<Longrightarrow> IT (r[Var i/j])" |
|
39 apply (induct arbitrary: i j set: IT) |
|
40 txt {* Case @{term Var}: *} |
|
41 apply (simp (no_asm) add: subst_Var) |
|
42 apply |
|
43 ((rule conjI impI)+, |
|
44 rule IT.Var, |
|
45 erule listsp.induct, |
|
46 simp (no_asm), |
|
47 rule listsp.Nil, |
|
48 simp (no_asm), |
|
49 rule listsp.Cons, |
|
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 |
|
64 lemma Var_IT: "IT (Var n)" |
|
65 apply (subgoal_tac "IT (Var n \<degree>\<degree> [])") |
|
66 apply simp |
|
67 apply (rule IT.Var) |
|
68 apply (rule listsp.Nil) |
|
69 done |
|
70 |
|
71 lemma app_Var_IT: "IT t \<Longrightarrow> IT (t \<degree> Var i)" |
|
72 apply (induct set: IT) |
|
73 apply (subst app_last) |
|
74 apply (rule IT.Var) |
|
75 apply simp |
|
76 apply (rule listsp.Cons) |
|
77 apply (rule Var_IT) |
|
78 apply (rule listsp.Nil) |
|
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: |
|
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])" |
|
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" |
|
100 assume "IT t" |
|
101 thus "\<And>e T' u i. PROP ?Q t e T' u i T" |
|
102 proof induct |
|
103 fix e T' u i |
|
104 assume uIT: "IT u" |
|
105 assume uT: "e \<turnstile> u : T" |
|
106 { |
|
107 case (Var rs n e_ T'_ u_ i_) |
|
108 assume nT: "e\<langle>i:T\<rangle> \<turnstile> Var n \<degree>\<degree> rs : T'" |
|
109 let ?ty = "\<lambda>t. \<exists>T'. e\<langle>i:T\<rangle> \<turnstile> t : T'" |
|
110 let ?R = "\<lambda>t. \<forall>e T' u i. |
|
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])" |
|
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 |
|
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])" |
|
135 proof (rule MI2) |
|
136 from T have "IT ((lift u 0 \<degree> Var 0)[a[u/i]/0])" |
|
137 proof (rule MI1) |
|
138 have "IT (lift u 0)" by (rule lift_IT [OF uIT]) |
|
139 thus "IT (lift u 0 \<degree> Var 0)" by (rule app_Var_IT) |
|
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) |
|
148 with argT uIT uT show "IT (a[u/i])" by simp |
|
149 from argT uT show "e \<turnstile> a[u/i] : T''" |
|
150 by (rule subst_lemma) simp |
|
151 qed |
|
152 thus "IT (u \<degree> a[u/i])" by simp |
|
153 from Var have "listsp ?R as" |
|
154 by cases (simp_all add: Cons) |
|
155 moreover from argsT have "listsp ?ty as" |
|
156 by (rule lists_typings) |
|
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)") |
|
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 |
|
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) |
|
172 thus ?case by simp |
|
173 qed |
|
174 thus "IT (Var 0 \<degree>\<degree> ?ls as)" by (rule IT.Var) |
|
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 |
|
189 by (simp add: comp_def) |
|
190 qed |
|
191 next |
|
192 case False |
|
193 from Var have "listsp ?R rs" by simp |
|
194 moreover from nT obtain Ts where "e\<langle>i:T\<rangle> \<tturnstile> rs : Ts" |
|
195 by (rule list_app_typeE) |
|
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)" |
|
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 |
|
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) |
|
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" |
|
218 with uIT uT show "IT (Abs r[u/i])" |
|
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" |
|
225 have "IT (Abs (r[lift u 0/Suc i]) \<degree> a[u/i] \<degree>\<degree> map (\<lambda>t. t[u/i]) as)" |
|
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) |
|
231 hence "IT ((r[a/0] \<degree>\<degree> as)[u/i])" |
|
232 using uIT uT by (rule SI1) |
|
233 thus "IT (r[lift u 0/Suc i][a[u/i]/0] \<degree>\<degree> map (\<lambda>t. t[u/i]) as)" |
|
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 |
|
238 thus "IT (a[u/i])" using uIT uT by (rule SI2) |
|
239 qed |
|
240 thus "IT ((Abs r \<degree> a \<degree>\<degree> as)[u/i])" by simp |
|
241 } |
|
242 qed |
|
243 qed |
|
244 |
|
245 |
|
246 subsection {* Well-typed terms are strongly normalizing *} |
|
247 |
|
248 lemma type_implies_IT: |
|
249 assumes "e \<turnstile> t : T" |
|
250 shows "IT t" |
|
251 using assms |
|
252 proof induct |
|
253 case Var |
|
254 show ?case by (rule Var_IT) |
|
255 next |
|
256 case Abs |
|
257 show ?case by (rule IT.Lambda) (rule Abs) |
|
258 next |
|
259 case (App e s T U t) |
|
260 have "IT ((Var 0 \<degree> lift t 0)[s/0])" |
|
261 proof (rule subst_type_IT) |
|
262 have "IT (lift t 0)" using `IT t` by (rule lift_IT) |
|
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) |
|
265 also have "Var 0 \<degree>\<degree> [lift t 0] = Var 0 \<degree> lift t 0" by simp |
|
266 finally show "IT \<dots>" . |
|
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" |
|
270 by (rule lift_type) (rule App.hyps) |
|
271 ultimately show "e\<langle>0:T \<Rightarrow> U\<rangle> \<turnstile> Var 0 \<degree> lift t 0 : U" |
|
272 by (rule typing.App) |
|
273 show "IT s" by fact |
|
274 show "e \<turnstile> s : T \<Rightarrow> U" by fact |
|
275 qed |
|
276 thus ?case by simp |
|
277 qed |
|
278 |
|
279 theorem type_implies_termi: "e \<turnstile> t : T \<Longrightarrow> termip beta t" |
|
280 proof - |
|
281 assume "e \<turnstile> t : T" |
|
282 hence "IT t" by (rule type_implies_IT) |
|
283 thus ?thesis by (rule IT_implies_termi) |
|
284 qed |
|
285 |
|
286 end |
|