1(* Title: HOL/Proofs/Lambda/StrongNorm.thy 2 Author: Stefan Berghofer 3 Copyright 2000 TU Muenchen 4*) 5 6section \<open>Strong normalization for simply-typed lambda calculus\<close> 7 8theory StrongNorm imports LambdaType InductTermi begin 9 10text \<open> 11Formalization by Stefan Berghofer. Partly based on a paper proof by 12Felix Joachimski and Ralph Matthes @{cite "Matthes-Joachimski-AML"}. 13\<close> 14 15 16subsection \<open>Properties of \<open>IT\<close>\<close> 17 18lemma 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 simp (no_asm), 28 rule listsp.Cons, 29 blast, 30 assumption)+ 31 apply auto 32 done 33 34lemma lifts_IT: "listsp IT ts \<Longrightarrow> listsp IT (map (\<lambda>t. lift t 0) ts)" 35 by (induct ts) auto 36 37lemma subst_Var_IT: "IT r \<Longrightarrow> IT (r[Var i/j])" 38 apply (induct arbitrary: i j set: IT) 39 txt \<open>Case @{term Var}:\<close> 40 apply (simp (no_asm) add: subst_Var) 41 apply 42 ((rule conjI impI)+, 43 rule IT.Var, 44 erule listsp.induct, 45 simp (no_asm), 46 simp (no_asm), 47 rule listsp.Cons, 48 fast, 49 assumption)+ 50 txt \<open>Case @{term Lambda}:\<close> 51 apply atomize 52 apply simp 53 apply (rule IT.Lambda) 54 apply fast 55 txt \<open>Case @{term Beta}:\<close> 56 apply atomize 57 apply (simp (no_asm_use) add: subst_subst [symmetric]) 58 apply (rule IT.Beta) 59 apply auto 60 done 61 62lemma Var_IT: "IT (Var n)" 63 apply (subgoal_tac "IT (Var n \<degree>\<degree> [])") 64 apply simp 65 apply (rule IT.Var) 66 apply (rule listsp.Nil) 67 done 68 69lemma app_Var_IT: "IT t \<Longrightarrow> IT (t \<degree> Var i)" 70 apply (induct set: IT) 71 apply (subst app_last) 72 apply (rule IT.Var) 73 apply simp 74 apply (rule listsp.Cons) 75 apply (rule Var_IT) 76 apply (rule listsp.Nil) 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 88subsection \<open>Well-typed substitution preserves termination\<close> 89 90lemma subst_type_IT: 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])" 93 (is "PROP ?P U" is "\<And>t e T u i. _ \<Longrightarrow> PROP ?Q t e T u i U") 94proof (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" 98 assume "IT t" 99 thus "\<And>e T' u i. PROP ?Q t e T' u i T" 100 proof induct 101 fix e T' u i 102 assume uIT: "IT u" 103 assume uT: "e \<turnstile> u : T" 104 { 105 case (Var rs n e1 T'1 u1 i1) 106 assume nT: "e\<langle>i:T\<rangle> \<turnstile> Var n \<degree>\<degree> rs : T'" 107 let ?ty = "\<lambda>t. \<exists>T'. e\<langle>i:T\<rangle> \<turnstile> t : T'" 108 let ?R = "\<lambda>t. \<forall>e T' u i. 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])" 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 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])" 133 proof (rule MI2) 134 from T have "IT ((lift u 0 \<degree> Var 0)[a[u/i]/0])" 135 proof (rule MI1) 136 have "IT (lift u 0)" by (rule lift_IT [OF uIT]) 137 thus "IT (lift u 0 \<degree> Var 0)" by (rule app_Var_IT) 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) 146 with argT uIT uT show "IT (a[u/i])" by simp 147 from argT uT show "e \<turnstile> a[u/i] : T''" 148 by (rule subst_lemma) simp 149 qed 150 thus "IT (u \<degree> a[u/i])" by simp 151 from Var have "listsp ?R as" 152 by cases (simp_all add: Cons) 153 moreover from argsT have "listsp ?ty as" 154 by (rule lists_typings) 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)") 159 proof induct 160 case Nil 161 show ?case by fastforce 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 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) 170 thus ?case by simp 171 qed 172 thus "IT (Var 0 \<degree>\<degree> ?ls as)" by (rule IT.Var) 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 187 by (simp add: comp_def) 188 qed 189 next 190 case False 191 from Var have "listsp ?R rs" by simp 192 moreover from nT obtain Ts where "e\<langle>i:T\<rangle> \<tturnstile> rs : Ts" 193 by (rule list_app_typeE) 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)" 198 proof induct 199 case Nil 200 show ?case by fastforce 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 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) 208 thus ?case by simp 209 qed 210 with False show ?thesis by (auto simp add: subst_Var) 211 qed 212 next 213 case (Lambda r e1 T'1 u1 i1) 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" 216 with uIT uT show "IT (Abs r[u/i])" 217 by fastforce 218 next 219 case (Beta r a as e1 T'1 u1 i1) 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" 223 have "IT (Abs (r[lift u 0/Suc i]) \<degree> a[u/i] \<degree>\<degree> map (\<lambda>t. t[u/i]) as)" 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) 229 hence "IT ((r[a/0] \<degree>\<degree> as)[u/i])" 230 using uIT uT by (rule SI1) 231 thus "IT (r[lift u 0/Suc i][a[u/i]/0] \<degree>\<degree> map (\<lambda>t. t[u/i]) as)" 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 236 thus "IT (a[u/i])" using uIT uT by (rule SI2) 237 qed 238 thus "IT ((Abs r \<degree> a \<degree>\<degree> as)[u/i])" by simp 239 } 240 qed 241qed 242 243 244subsection \<open>Well-typed terms are strongly normalizing\<close> 245 246lemma type_implies_IT: 247 assumes "e \<turnstile> t : T" 248 shows "IT t" 249 using assms 250proof induct 251 case Var 252 show ?case by (rule Var_IT) 253next 254 case Abs 255 show ?case by (rule IT.Lambda) (rule Abs) 256next 257 case (App e s T U t) 258 have "IT ((Var 0 \<degree> lift t 0)[s/0])" 259 proof (rule subst_type_IT) 260 have "IT (lift t 0)" using \<open>IT t\<close> by (rule lift_IT) 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) 263 also have "Var 0 \<degree>\<degree> [lift t 0] = Var 0 \<degree> lift t 0" by simp 264 finally show "IT \<dots>" . 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" 268 by (rule lift_type) (rule App.hyps) 269 ultimately show "e\<langle>0:T \<Rightarrow> U\<rangle> \<turnstile> Var 0 \<degree> lift t 0 : U" 270 by (rule typing.App) 271 show "IT s" by fact 272 show "e \<turnstile> s : T \<Rightarrow> U" by fact 273 qed 274 thus ?case by simp 275qed 276 277theorem type_implies_termi: "e \<turnstile> t : T \<Longrightarrow> termip beta t" 278proof - 279 assume "e \<turnstile> t : T" 280 hence "IT t" by (rule type_implies_IT) 281 thus ?thesis by (rule IT_implies_termi) 282qed 283 284end 285