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