author  haftmann 
Sat, 05 Jul 2014 11:01:53 +0200  
changeset 57514  bdc2c6b40bf2 
parent 50336  1d9a31b58053 
child 58622  aa99568f56de 
permissions  rwrr 
39157
b98909faaea8
more explicit HOLProofs 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 simplytyped 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{MatthesJoachimskiAML}. 

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 {* Welltyped 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 tabwidth;
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 {* Welltyped 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 