1(* Title: HOL/Proofs/Lambda/Standardization.thy 2 Author: Stefan Berghofer 3 Copyright 2005 TU Muenchen 4*) 5 6section \<open>Standardization\<close> 7 8theory Standardization 9imports NormalForm 10begin 11 12text \<open> 13Based on lecture notes by Ralph Matthes @{cite "Matthes-ESSLLI2000"}, 14original proof idea due to Ralph Loader @{cite Loader1998}. 15\<close> 16 17 18subsection \<open>Standard reduction relation\<close> 19 20declare listrel_mono [mono_set] 21 22inductive 23 sred :: "dB \<Rightarrow> dB \<Rightarrow> bool" (infixl "\<rightarrow>\<^sub>s" 50) 24 and sredlist :: "dB list \<Rightarrow> dB list \<Rightarrow> bool" (infixl "[\<rightarrow>\<^sub>s]" 50) 25where 26 "s [\<rightarrow>\<^sub>s] t \<equiv> listrelp (\<rightarrow>\<^sub>s) s t" 27| Var: "rs [\<rightarrow>\<^sub>s] rs' \<Longrightarrow> Var x \<degree>\<degree> rs \<rightarrow>\<^sub>s Var x \<degree>\<degree> rs'" 28| Abs: "r \<rightarrow>\<^sub>s r' \<Longrightarrow> ss [\<rightarrow>\<^sub>s] ss' \<Longrightarrow> Abs r \<degree>\<degree> ss \<rightarrow>\<^sub>s Abs r' \<degree>\<degree> ss'" 29| Beta: "r[s/0] \<degree>\<degree> ss \<rightarrow>\<^sub>s t \<Longrightarrow> Abs r \<degree> s \<degree>\<degree> ss \<rightarrow>\<^sub>s t" 30 31lemma refl_listrelp: "\<forall>x\<in>set xs. R x x \<Longrightarrow> listrelp R xs xs" 32 by (induct xs) (auto intro: listrelp.intros) 33 34lemma refl_sred: "t \<rightarrow>\<^sub>s t" 35 by (induct t rule: Apps_dB_induct) (auto intro: refl_listrelp sred.intros) 36 37lemma refl_sreds: "ts [\<rightarrow>\<^sub>s] ts" 38 by (simp add: refl_sred refl_listrelp) 39 40lemma listrelp_conj1: "listrelp (\<lambda>x y. R x y \<and> S x y) x y \<Longrightarrow> listrelp R x y" 41 by (erule listrelp.induct) (auto intro: listrelp.intros) 42 43lemma listrelp_conj2: "listrelp (\<lambda>x y. R x y \<and> S x y) x y \<Longrightarrow> listrelp S x y" 44 by (erule listrelp.induct) (auto intro: listrelp.intros) 45 46lemma listrelp_app: 47 assumes xsys: "listrelp R xs ys" 48 shows "listrelp R xs' ys' \<Longrightarrow> listrelp R (xs @ xs') (ys @ ys')" using xsys 49 by (induct arbitrary: xs' ys') (auto intro: listrelp.intros) 50 51lemma lemma1: 52 assumes r: "r \<rightarrow>\<^sub>s r'" and s: "s \<rightarrow>\<^sub>s s'" 53 shows "r \<degree> s \<rightarrow>\<^sub>s r' \<degree> s'" using r 54proof induct 55 case (Var rs rs' x) 56 then have "rs [\<rightarrow>\<^sub>s] rs'" by (rule listrelp_conj1) 57 moreover have "[s] [\<rightarrow>\<^sub>s] [s']" by (iprover intro: s listrelp.intros) 58 ultimately have "rs @ [s] [\<rightarrow>\<^sub>s] rs' @ [s']" by (rule listrelp_app) 59 hence "Var x \<degree>\<degree> (rs @ [s]) \<rightarrow>\<^sub>s Var x \<degree>\<degree> (rs' @ [s'])" by (rule sred.Var) 60 thus ?case by (simp only: app_last) 61next 62 case (Abs r r' ss ss') 63 from Abs(3) have "ss [\<rightarrow>\<^sub>s] ss'" by (rule listrelp_conj1) 64 moreover have "[s] [\<rightarrow>\<^sub>s] [s']" by (iprover intro: s listrelp.intros) 65 ultimately have "ss @ [s] [\<rightarrow>\<^sub>s] ss' @ [s']" by (rule listrelp_app) 66 with \<open>r \<rightarrow>\<^sub>s r'\<close> have "Abs r \<degree>\<degree> (ss @ [s]) \<rightarrow>\<^sub>s Abs r' \<degree>\<degree> (ss' @ [s'])" 67 by (rule sred.Abs) 68 thus ?case by (simp only: app_last) 69next 70 case (Beta r u ss t) 71 hence "r[u/0] \<degree>\<degree> (ss @ [s]) \<rightarrow>\<^sub>s t \<degree> s'" by (simp only: app_last) 72 hence "Abs r \<degree> u \<degree>\<degree> (ss @ [s]) \<rightarrow>\<^sub>s t \<degree> s'" by (rule sred.Beta) 73 thus ?case by (simp only: app_last) 74qed 75 76lemma lemma1': 77 assumes ts: "ts [\<rightarrow>\<^sub>s] ts'" 78 shows "r \<rightarrow>\<^sub>s r' \<Longrightarrow> r \<degree>\<degree> ts \<rightarrow>\<^sub>s r' \<degree>\<degree> ts'" using ts 79 by (induct arbitrary: r r') (auto intro: lemma1) 80 81lemma lemma2_1: 82 assumes beta: "t \<rightarrow>\<^sub>\<beta> u" 83 shows "t \<rightarrow>\<^sub>s u" using beta 84proof induct 85 case (beta s t) 86 have "Abs s \<degree> t \<degree>\<degree> [] \<rightarrow>\<^sub>s s[t/0] \<degree>\<degree> []" by (iprover intro: sred.Beta refl_sred) 87 thus ?case by simp 88next 89 case (appL s t u) 90 thus ?case by (iprover intro: lemma1 refl_sred) 91next 92 case (appR s t u) 93 thus ?case by (iprover intro: lemma1 refl_sred) 94next 95 case (abs s t) 96 hence "Abs s \<degree>\<degree> [] \<rightarrow>\<^sub>s Abs t \<degree>\<degree> []" by (iprover intro: sred.Abs listrelp.Nil) 97 thus ?case by simp 98qed 99 100lemma listrelp_betas: 101 assumes ts: "listrelp (\<rightarrow>\<^sub>\<beta>\<^sup>*) ts ts'" 102 shows "\<And>t t'. t \<rightarrow>\<^sub>\<beta>\<^sup>* t' \<Longrightarrow> t \<degree>\<degree> ts \<rightarrow>\<^sub>\<beta>\<^sup>* t' \<degree>\<degree> ts'" using ts 103 by induct auto 104 105lemma lemma2_2: 106 assumes t: "t \<rightarrow>\<^sub>s u" 107 shows "t \<rightarrow>\<^sub>\<beta>\<^sup>* u" using t 108 by induct (auto dest: listrelp_conj2 109 intro: listrelp_betas apps_preserves_beta converse_rtranclp_into_rtranclp) 110 111lemma sred_lift: 112 assumes s: "s \<rightarrow>\<^sub>s t" 113 shows "lift s i \<rightarrow>\<^sub>s lift t i" using s 114proof (induct arbitrary: i) 115 case (Var rs rs' x) 116 hence "map (\<lambda>t. lift t i) rs [\<rightarrow>\<^sub>s] map (\<lambda>t. lift t i) rs'" 117 by induct (auto intro: listrelp.intros) 118 thus ?case by (cases "x < i") (auto intro: sred.Var) 119next 120 case (Abs r r' ss ss') 121 from Abs(3) have "map (\<lambda>t. lift t i) ss [\<rightarrow>\<^sub>s] map (\<lambda>t. lift t i) ss'" 122 by induct (auto intro: listrelp.intros) 123 thus ?case by (auto intro: sred.Abs Abs) 124next 125 case (Beta r s ss t) 126 thus ?case by (auto intro: sred.Beta) 127qed 128 129lemma lemma3: 130 assumes r: "r \<rightarrow>\<^sub>s r'" 131 shows "s \<rightarrow>\<^sub>s s' \<Longrightarrow> r[s/x] \<rightarrow>\<^sub>s r'[s'/x]" using r 132proof (induct arbitrary: s s' x) 133 case (Var rs rs' y) 134 hence "map (\<lambda>t. t[s/x]) rs [\<rightarrow>\<^sub>s] map (\<lambda>t. t[s'/x]) rs'" 135 by induct (auto intro: listrelp.intros Var) 136 moreover have "Var y[s/x] \<rightarrow>\<^sub>s Var y[s'/x]" 137 proof (cases "y < x") 138 case True thus ?thesis by simp (rule refl_sred) 139 next 140 case False 141 thus ?thesis 142 by (cases "y = x") (auto simp add: Var intro: refl_sred) 143 qed 144 ultimately show ?case by simp (rule lemma1') 145next 146 case (Abs r r' ss ss') 147 from Abs(4) have "lift s 0 \<rightarrow>\<^sub>s lift s' 0" by (rule sred_lift) 148 hence "r[lift s 0/Suc x] \<rightarrow>\<^sub>s r'[lift s' 0/Suc x]" by (fast intro: Abs.hyps) 149 moreover from Abs(3) have "map (\<lambda>t. t[s/x]) ss [\<rightarrow>\<^sub>s] map (\<lambda>t. t[s'/x]) ss'" 150 by induct (auto intro: listrelp.intros Abs) 151 ultimately show ?case by simp (rule sred.Abs) 152next 153 case (Beta r u ss t) 154 thus ?case by (auto simp add: subst_subst intro: sred.Beta) 155qed 156 157lemma lemma4_aux: 158 assumes rs: "listrelp (\<lambda>t u. t \<rightarrow>\<^sub>s u \<and> (\<forall>r. u \<rightarrow>\<^sub>\<beta> r \<longrightarrow> t \<rightarrow>\<^sub>s r)) rs rs'" 159 shows "rs' => ss \<Longrightarrow> rs [\<rightarrow>\<^sub>s] ss" using rs 160proof (induct arbitrary: ss) 161 case Nil 162 thus ?case by cases (auto intro: listrelp.Nil) 163next 164 case (Cons x y xs ys) 165 note Cons' = Cons 166 show ?case 167 proof (cases ss) 168 case Nil with Cons show ?thesis by simp 169 next 170 case (Cons y' ys') 171 hence ss: "ss = y' # ys'" by simp 172 from Cons Cons' have "y \<rightarrow>\<^sub>\<beta> y' \<and> ys' = ys \<or> y' = y \<and> ys => ys'" by simp 173 hence "x # xs [\<rightarrow>\<^sub>s] y' # ys'" 174 proof 175 assume H: "y \<rightarrow>\<^sub>\<beta> y' \<and> ys' = ys" 176 with Cons' have "x \<rightarrow>\<^sub>s y'" by blast 177 moreover from Cons' have "xs [\<rightarrow>\<^sub>s] ys" by (iprover dest: listrelp_conj1) 178 ultimately have "x # xs [\<rightarrow>\<^sub>s] y' # ys" by (rule listrelp.Cons) 179 with H show ?thesis by simp 180 next 181 assume H: "y' = y \<and> ys => ys'" 182 with Cons' have "x \<rightarrow>\<^sub>s y'" by blast 183 moreover from H have "xs [\<rightarrow>\<^sub>s] ys'" by (blast intro: Cons') 184 ultimately show ?thesis by (rule listrelp.Cons) 185 qed 186 with ss show ?thesis by simp 187 qed 188qed 189 190lemma lemma4: 191 assumes r: "r \<rightarrow>\<^sub>s r'" 192 shows "r' \<rightarrow>\<^sub>\<beta> r'' \<Longrightarrow> r \<rightarrow>\<^sub>s r''" using r 193proof (induct arbitrary: r'') 194 case (Var rs rs' x) 195 then obtain ss where rs: "rs' => ss" and r'': "r'' = Var x \<degree>\<degree> ss" 196 by (blast dest: head_Var_reduction) 197 from Var(1) rs have "rs [\<rightarrow>\<^sub>s] ss" by (rule lemma4_aux) 198 hence "Var x \<degree>\<degree> rs \<rightarrow>\<^sub>s Var x \<degree>\<degree> ss" by (rule sred.Var) 199 with r'' show ?case by simp 200next 201 case (Abs r r' ss ss') 202 from \<open>Abs r' \<degree>\<degree> ss' \<rightarrow>\<^sub>\<beta> r''\<close> show ?case 203 proof 204 fix s 205 assume r'': "r'' = s \<degree>\<degree> ss'" 206 assume "Abs r' \<rightarrow>\<^sub>\<beta> s" 207 then obtain r''' where s: "s = Abs r'''" and r''': "r' \<rightarrow>\<^sub>\<beta> r'''" by cases auto 208 from r''' have "r \<rightarrow>\<^sub>s r'''" by (blast intro: Abs) 209 moreover from Abs have "ss [\<rightarrow>\<^sub>s] ss'" by (iprover dest: listrelp_conj1) 210 ultimately have "Abs r \<degree>\<degree> ss \<rightarrow>\<^sub>s Abs r''' \<degree>\<degree> ss'" by (rule sred.Abs) 211 with r'' s show "Abs r \<degree>\<degree> ss \<rightarrow>\<^sub>s r''" by simp 212 next 213 fix rs' 214 assume "ss' => rs'" 215 with Abs(3) have "ss [\<rightarrow>\<^sub>s] rs'" by (rule lemma4_aux) 216 with \<open>r \<rightarrow>\<^sub>s r'\<close> have "Abs r \<degree>\<degree> ss \<rightarrow>\<^sub>s Abs r' \<degree>\<degree> rs'" by (rule sred.Abs) 217 moreover assume "r'' = Abs r' \<degree>\<degree> rs'" 218 ultimately show "Abs r \<degree>\<degree> ss \<rightarrow>\<^sub>s r''" by simp 219 next 220 fix t u' us' 221 assume "ss' = u' # us'" 222 with Abs(3) obtain u us where 223 ss: "ss = u # us" and u: "u \<rightarrow>\<^sub>s u'" and us: "us [\<rightarrow>\<^sub>s] us'" 224 by cases (auto dest!: listrelp_conj1) 225 have "r[u/0] \<rightarrow>\<^sub>s r'[u'/0]" using Abs(1) and u by (rule lemma3) 226 with us have "r[u/0] \<degree>\<degree> us \<rightarrow>\<^sub>s r'[u'/0] \<degree>\<degree> us'" by (rule lemma1') 227 hence "Abs r \<degree> u \<degree>\<degree> us \<rightarrow>\<^sub>s r'[u'/0] \<degree>\<degree> us'" by (rule sred.Beta) 228 moreover assume "Abs r' = Abs t" and "r'' = t[u'/0] \<degree>\<degree> us'" 229 ultimately show "Abs r \<degree>\<degree> ss \<rightarrow>\<^sub>s r''" using ss by simp 230 qed 231next 232 case (Beta r s ss t) 233 show ?case 234 by (rule sred.Beta) (rule Beta)+ 235qed 236 237lemma rtrancl_beta_sred: 238 assumes r: "r \<rightarrow>\<^sub>\<beta>\<^sup>* r'" 239 shows "r \<rightarrow>\<^sub>s r'" using r 240 by induct (iprover intro: refl_sred lemma4)+ 241 242 243subsection \<open>Leftmost reduction and weakly normalizing terms\<close> 244 245inductive 246 lred :: "dB \<Rightarrow> dB \<Rightarrow> bool" (infixl "\<rightarrow>\<^sub>l" 50) 247 and lredlist :: "dB list \<Rightarrow> dB list \<Rightarrow> bool" (infixl "[\<rightarrow>\<^sub>l]" 50) 248where 249 "s [\<rightarrow>\<^sub>l] t \<equiv> listrelp (\<rightarrow>\<^sub>l) s t" 250| Var: "rs [\<rightarrow>\<^sub>l] rs' \<Longrightarrow> Var x \<degree>\<degree> rs \<rightarrow>\<^sub>l Var x \<degree>\<degree> rs'" 251| Abs: "r \<rightarrow>\<^sub>l r' \<Longrightarrow> Abs r \<rightarrow>\<^sub>l Abs r'" 252| Beta: "r[s/0] \<degree>\<degree> ss \<rightarrow>\<^sub>l t \<Longrightarrow> Abs r \<degree> s \<degree>\<degree> ss \<rightarrow>\<^sub>l t" 253 254lemma lred_imp_sred: 255 assumes lred: "s \<rightarrow>\<^sub>l t" 256 shows "s \<rightarrow>\<^sub>s t" using lred 257proof induct 258 case (Var rs rs' x) 259 then have "rs [\<rightarrow>\<^sub>s] rs'" 260 by induct (iprover intro: listrelp.intros)+ 261 then show ?case by (rule sred.Var) 262next 263 case (Abs r r') 264 from \<open>r \<rightarrow>\<^sub>s r'\<close> 265 have "Abs r \<degree>\<degree> [] \<rightarrow>\<^sub>s Abs r' \<degree>\<degree> []" using listrelp.Nil 266 by (rule sred.Abs) 267 then show ?case by simp 268next 269 case (Beta r s ss t) 270 from \<open>r[s/0] \<degree>\<degree> ss \<rightarrow>\<^sub>s t\<close> 271 show ?case by (rule sred.Beta) 272qed 273 274inductive WN :: "dB => bool" 275 where 276 Var: "listsp WN rs \<Longrightarrow> WN (Var n \<degree>\<degree> rs)" 277 | Lambda: "WN r \<Longrightarrow> WN (Abs r)" 278 | Beta: "WN ((r[s/0]) \<degree>\<degree> ss) \<Longrightarrow> WN ((Abs r \<degree> s) \<degree>\<degree> ss)" 279 280lemma listrelp_imp_listsp1: 281 assumes H: "listrelp (\<lambda>x y. P x) xs ys" 282 shows "listsp P xs" using H 283 by induct auto 284 285lemma listrelp_imp_listsp2: 286 assumes H: "listrelp (\<lambda>x y. P y) xs ys" 287 shows "listsp P ys" using H 288 by induct auto 289 290lemma lemma5: 291 assumes lred: "r \<rightarrow>\<^sub>l r'" 292 shows "WN r" and "NF r'" using lred 293 by induct 294 (iprover dest: listrelp_conj1 listrelp_conj2 295 listrelp_imp_listsp1 listrelp_imp_listsp2 intro: WN.intros 296 NF.intros [simplified listall_listsp_eq])+ 297 298lemma lemma6: 299 assumes wn: "WN r" 300 shows "\<exists>r'. r \<rightarrow>\<^sub>l r'" using wn 301proof induct 302 case (Var rs n) 303 then have "\<exists>rs'. rs [\<rightarrow>\<^sub>l] rs'" 304 by induct (iprover intro: listrelp.intros)+ 305 then show ?case by (iprover intro: lred.Var) 306qed (iprover intro: lred.intros)+ 307 308lemma lemma7: 309 assumes r: "r \<rightarrow>\<^sub>s r'" 310 shows "NF r' \<Longrightarrow> r \<rightarrow>\<^sub>l r'" using r 311proof induct 312 case (Var rs rs' x) 313 from \<open>NF (Var x \<degree>\<degree> rs')\<close> have "listall NF rs'" 314 by cases simp_all 315 with Var(1) have "rs [\<rightarrow>\<^sub>l] rs'" 316 proof induct 317 case Nil 318 show ?case by (rule listrelp.Nil) 319 next 320 case (Cons x y xs ys) 321 hence "x \<rightarrow>\<^sub>l y" and "xs [\<rightarrow>\<^sub>l] ys" by simp_all 322 thus ?case by (rule listrelp.Cons) 323 qed 324 thus ?case by (rule lred.Var) 325next 326 case (Abs r r' ss ss') 327 from \<open>NF (Abs r' \<degree>\<degree> ss')\<close> 328 have ss': "ss' = []" by (rule Abs_NF) 329 from Abs(3) have ss: "ss = []" using ss' 330 by cases simp_all 331 from ss' Abs have "NF (Abs r')" by simp 332 hence "NF r'" by cases simp_all 333 with Abs have "r \<rightarrow>\<^sub>l r'" by simp 334 hence "Abs r \<rightarrow>\<^sub>l Abs r'" by (rule lred.Abs) 335 with ss ss' show ?case by simp 336next 337 case (Beta r s ss t) 338 hence "r[s/0] \<degree>\<degree> ss \<rightarrow>\<^sub>l t" by simp 339 thus ?case by (rule lred.Beta) 340qed 341 342lemma WN_eq: "WN t = (\<exists>t'. t \<rightarrow>\<^sub>\<beta>\<^sup>* t' \<and> NF t')" 343proof 344 assume "WN t" 345 then have "\<exists>t'. t \<rightarrow>\<^sub>l t'" by (rule lemma6) 346 then obtain t' where t': "t \<rightarrow>\<^sub>l t'" .. 347 then have NF: "NF t'" by (rule lemma5) 348 from t' have "t \<rightarrow>\<^sub>s t'" by (rule lred_imp_sred) 349 then have "t \<rightarrow>\<^sub>\<beta>\<^sup>* t'" by (rule lemma2_2) 350 with NF show "\<exists>t'. t \<rightarrow>\<^sub>\<beta>\<^sup>* t' \<and> NF t'" by iprover 351next 352 assume "\<exists>t'. t \<rightarrow>\<^sub>\<beta>\<^sup>* t' \<and> NF t'" 353 then obtain t' where t': "t \<rightarrow>\<^sub>\<beta>\<^sup>* t'" and NF: "NF t'" 354 by iprover 355 from t' have "t \<rightarrow>\<^sub>s t'" by (rule rtrancl_beta_sred) 356 then have "t \<rightarrow>\<^sub>l t'" using NF by (rule lemma7) 357 then show "WN t" by (rule lemma5) 358qed 359 360end 361