1219820Sjeff(* Title: HOL/Proofs/Lambda/StrongNorm.thy 2219820Sjeff Author: Stefan Berghofer 3219820Sjeff Copyright 2000 TU Muenchen 4219820Sjeff*) 5219820Sjeff 6219820Sjeffsection \<open>Strong normalization for simply-typed lambda calculus\<close> 7219820Sjeff 8219820Sjefftheory StrongNorm imports LambdaType InductTermi begin 9219820Sjeff 10219820Sjefftext \<open> 11219820SjeffFormalization by Stefan Berghofer. Partly based on a paper proof by 12219820SjeffFelix Joachimski and Ralph Matthes @{cite "Matthes-Joachimski-AML"}. 13219820Sjeff\<close> 14219820Sjeff 15219820Sjeff 16219820Sjeffsubsection \<open>Properties of \<open>IT\<close>\<close> 17219820Sjeff 18219820Sjefflemma lift_IT [intro!]: "IT t \<Longrightarrow> IT (lift t i)" 19219820Sjeff apply (induct arbitrary: i set: IT) 20219820Sjeff apply (simp (no_asm)) 21219820Sjeff apply (rule conjI) 22219820Sjeff apply 23219820Sjeff (rule impI, 24219820Sjeff rule IT.Var, 25219820Sjeff erule listsp.induct, 26219820Sjeff simp (no_asm), 27219820Sjeff simp (no_asm), 28219820Sjeff rule listsp.Cons, 29219820Sjeff blast, 30219820Sjeff assumption)+ 31219820Sjeff apply auto 32219820Sjeff done 33219820Sjeff 34219820Sjefflemma lifts_IT: "listsp IT ts \<Longrightarrow> listsp IT (map (\<lambda>t. lift t 0) ts)" 35219820Sjeff by (induct ts) auto 36219820Sjeff 37219820Sjefflemma subst_Var_IT: "IT r \<Longrightarrow> IT (r[Var i/j])" 38219820Sjeff apply (induct arbitrary: i j set: IT) 39219820Sjeff txt \<open>Case \<^term>\<open>Var\<close>:\<close> 40219820Sjeff apply (simp (no_asm) add: subst_Var) 41219820Sjeff apply 42219820Sjeff ((rule conjI impI)+, 43219820Sjeff rule IT.Var, 44219820Sjeff erule listsp.induct, 45219820Sjeff simp (no_asm), 46219820Sjeff simp (no_asm), 47219820Sjeff rule listsp.Cons, 48219820Sjeff fast, 49219820Sjeff assumption)+ 50219820Sjeff txt \<open>Case \<^term>\<open>Lambda\<close>:\<close> 51219820Sjeff apply atomize 52219820Sjeff apply simp 53219820Sjeff apply (rule IT.Lambda) 54219820Sjeff apply fast 55219820Sjeff txt \<open>Case \<^term>\<open>Beta\<close>:\<close> 56219820Sjeff apply atomize 57219820Sjeff apply (simp (no_asm_use) add: subst_subst [symmetric]) 58219820Sjeff apply (rule IT.Beta) 59219820Sjeff apply auto 60219820Sjeff done 61219820Sjeff 62219820Sjefflemma Var_IT: "IT (Var n)" 63219820Sjeff apply (subgoal_tac "IT (Var n \<degree>\<degree> [])") 64219820Sjeff apply simp 65219820Sjeff apply (rule IT.Var) 66219820Sjeff apply (rule listsp.Nil) 67219820Sjeff done 68219820Sjeff 69219820Sjefflemma app_Var_IT: "IT t \<Longrightarrow> IT (t \<degree> Var i)" 70219820Sjeff apply (induct set: IT) 71219820Sjeff apply (subst app_last) 72219820Sjeff apply (rule IT.Var) 73219820Sjeff apply simp 74219820Sjeff apply (rule listsp.Cons) 75219820Sjeff apply (rule Var_IT) 76219820Sjeff apply (rule listsp.Nil) 77219820Sjeff apply (rule IT.Beta [where ?ss = "[]", unfolded foldl_Nil [THEN eq_reflection]]) 78219820Sjeff apply (erule subst_Var_IT) 79219820Sjeff apply (rule Var_IT) 80219820Sjeff apply (subst app_last) 81219820Sjeff apply (rule IT.Beta) 82219820Sjeff apply (subst app_last [symmetric]) 83219820Sjeff apply assumption 84219820Sjeff apply assumption 85219820Sjeff done 86219820Sjeff 87219820Sjeff 88219820Sjeffsubsection \<open>Well-typed substitution preserves termination\<close> 89219820Sjeff 90219820Sjefflemma subst_type_IT: 91219820Sjeff "\<And>t e T u i. IT t \<Longrightarrow> e\<langle>i:U\<rangle> \<turnstile> t : T \<Longrightarrow> 92219820Sjeff IT u \<Longrightarrow> e \<turnstile> u : U \<Longrightarrow> IT (t[u/i])" 93219820Sjeff (is "PROP ?P U" is "\<And>t e T u i. _ \<Longrightarrow> PROP ?Q t e T u i U") 94219820Sjeffproof (induct U) 95219820Sjeff fix T t 96219820Sjeff assume MI1: "\<And>T1 T2. T = T1 \<Rightarrow> T2 \<Longrightarrow> PROP ?P T1" 97219820Sjeff assume MI2: "\<And>T1 T2. T = T1 \<Rightarrow> T2 \<Longrightarrow> PROP ?P T2" 98219820Sjeff assume "IT t" 99219820Sjeff thus "\<And>e T' u i. PROP ?Q t e T' u i T" 100219820Sjeff proof induct 101219820Sjeff fix e T' u i 102219820Sjeff assume uIT: "IT u" 103219820Sjeff assume uT: "e \<turnstile> u : T" 104219820Sjeff { 105219820Sjeff case (Var rs n e1 T'1 u1 i1) 106219820Sjeff assume nT: "e\<langle>i:T\<rangle> \<turnstile> Var n \<degree>\<degree> rs : T'" 107219820Sjeff let ?ty = "\<lambda>t. \<exists>T'. e\<langle>i:T\<rangle> \<turnstile> t : T'" 108219820Sjeff let ?R = "\<lambda>t. \<forall>e T' u i. 109219820Sjeff e\<langle>i:T\<rangle> \<turnstile> t : T' \<longrightarrow> IT u \<longrightarrow> e \<turnstile> u : T \<longrightarrow> IT (t[u/i])" 110219820Sjeff show "IT ((Var n \<degree>\<degree> rs)[u/i])" 111219820Sjeff proof (cases "n = i") 112219820Sjeff case True 113219820Sjeff show ?thesis 114219820Sjeff proof (cases rs) 115219820Sjeff case Nil 116219820Sjeff with uIT True show ?thesis by simp 117219820Sjeff next 118219820Sjeff case (Cons a as) 119219820Sjeff with nT have "e\<langle>i:T\<rangle> \<turnstile> Var n \<degree> a \<degree>\<degree> as : T'" by simp 120219820Sjeff then obtain Ts 121219820Sjeff where headT: "e\<langle>i:T\<rangle> \<turnstile> Var n \<degree> a : Ts \<Rrightarrow> T'" 122219820Sjeff and argsT: "e\<langle>i:T\<rangle> \<tturnstile> as : Ts" 123219820Sjeff by (rule list_app_typeE) 124219820Sjeff from headT obtain T'' 125219820Sjeff where varT: "e\<langle>i:T\<rangle> \<turnstile> Var n : T'' \<Rightarrow> Ts \<Rrightarrow> T'" 126219820Sjeff and argT: "e\<langle>i:T\<rangle> \<turnstile> a : T''" 127219820Sjeff by cases simp_all 128219820Sjeff from varT True have T: "T = T'' \<Rightarrow> Ts \<Rrightarrow> T'" 129219820Sjeff by cases auto 130219820Sjeff with uT have uT': "e \<turnstile> u : T'' \<Rightarrow> Ts \<Rrightarrow> T'" by simp 131219820Sjeff from T have "IT ((Var 0 \<degree>\<degree> map (\<lambda>t. lift t 0) 132219820Sjeff (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