1(* Title: HOL/Nominal/Examples/Standardization.thy 2 Author: Stefan Berghofer and Tobias Nipkow 3 Copyright 2005, 2008 TU Muenchen 4*) 5 6section \<open>Standardization\<close> 7 8theory Standardization 9imports "HOL-Nominal.Nominal" 10begin 11 12text \<open> 13The proof of the standardization theorem, as well as most of the theorems about 14lambda calculus in the following sections, are taken from \<open>HOL/Lambda\<close>. 15\<close> 16 17subsection \<open>Lambda terms\<close> 18 19atom_decl name 20 21nominal_datatype lam = 22 Var "name" 23| App "lam" "lam" (infixl "\<degree>" 200) 24| Lam "\<guillemotleft>name\<guillemotright>lam" ("Lam [_]._" [0, 10] 10) 25 26instantiation lam :: size 27begin 28 29nominal_primrec size_lam 30where 31 "size (Var n) = 0" 32| "size (t \<degree> u) = size t + size u + 1" 33| "size (Lam [x].t) = size t + 1" 34 apply finite_guess+ 35 apply (rule TrueI)+ 36 apply (simp add: fresh_nat) 37 apply fresh_guess+ 38 done 39 40instance .. 41 42end 43 44nominal_primrec 45 subst :: "lam \<Rightarrow> name \<Rightarrow> lam \<Rightarrow> lam" ("_[_::=_]" [300, 0, 0] 300) 46where 47 subst_Var: "(Var x)[y::=s] = (if x=y then s else (Var x))" 48| subst_App: "(t\<^sub>1 \<degree> t\<^sub>2)[y::=s] = t\<^sub>1[y::=s] \<degree> t\<^sub>2[y::=s]" 49| subst_Lam: "x \<sharp> (y, s) \<Longrightarrow> (Lam [x].t)[y::=s] = (Lam [x].(t[y::=s]))" 50 apply(finite_guess)+ 51 apply(rule TrueI)+ 52 apply(simp add: abs_fresh) 53 apply(fresh_guess)+ 54 done 55 56lemma subst_eqvt [eqvt]: 57 "(pi::name prm) \<bullet> (t[x::=u]) = (pi \<bullet> t)[(pi \<bullet> x)::=(pi \<bullet> u)]" 58 by (nominal_induct t avoiding: x u rule: lam.strong_induct) 59 (perm_simp add: fresh_bij)+ 60 61lemma subst_rename: 62 "y \<sharp> t \<Longrightarrow> ([(y, x)] \<bullet> t)[y::=u] = t[x::=u]" 63 by (nominal_induct t avoiding: x y u rule: lam.strong_induct) 64 (simp_all add: fresh_atm calc_atm abs_fresh) 65 66lemma fresh_subst: 67 "(x::name) \<sharp> t \<Longrightarrow> x \<sharp> u \<Longrightarrow> x \<sharp> t[y::=u]" 68 by (nominal_induct t avoiding: x y u rule: lam.strong_induct) 69 (auto simp add: abs_fresh fresh_atm) 70 71lemma fresh_subst': 72 "(x::name) \<sharp> u \<Longrightarrow> x \<sharp> t[x::=u]" 73 by (nominal_induct t avoiding: x u rule: lam.strong_induct) 74 (auto simp add: abs_fresh fresh_atm) 75 76lemma subst_forget: "(x::name) \<sharp> t \<Longrightarrow> t[x::=u] = t" 77 by (nominal_induct t avoiding: x u rule: lam.strong_induct) 78 (auto simp add: abs_fresh fresh_atm) 79 80lemma subst_subst: 81 "x \<noteq> y \<Longrightarrow> x \<sharp> v \<Longrightarrow> t[y::=v][x::=u[y::=v]] = t[x::=u][y::=v]" 82 by (nominal_induct t avoiding: x y u v rule: lam.strong_induct) 83 (auto simp add: fresh_subst subst_forget) 84 85declare subst_Var [simp del] 86 87lemma subst_eq [simp]: "(Var x)[x::=u] = u" 88 by (simp add: subst_Var) 89 90lemma subst_neq [simp]: "x \<noteq> y \<Longrightarrow> (Var x)[y::=u] = Var x" 91 by (simp add: subst_Var) 92 93inductive beta :: "lam \<Rightarrow> lam \<Rightarrow> bool" (infixl "\<rightarrow>\<^sub>\<beta>" 50) 94 where 95 beta: "x \<sharp> t \<Longrightarrow> (Lam [x].s) \<degree> t \<rightarrow>\<^sub>\<beta> s[x::=t]" 96 | appL [simp, intro!]: "s \<rightarrow>\<^sub>\<beta> t \<Longrightarrow> s \<degree> u \<rightarrow>\<^sub>\<beta> t \<degree> u" 97 | appR [simp, intro!]: "s \<rightarrow>\<^sub>\<beta> t \<Longrightarrow> u \<degree> s \<rightarrow>\<^sub>\<beta> u \<degree> t" 98 | abs [simp, intro!]: "s \<rightarrow>\<^sub>\<beta> t \<Longrightarrow> (Lam [x].s) \<rightarrow>\<^sub>\<beta> (Lam [x].t)" 99 100equivariance beta 101nominal_inductive beta 102 by (simp_all add: abs_fresh fresh_subst') 103 104lemma better_beta [simp, intro!]: "(Lam [x].s) \<degree> t \<rightarrow>\<^sub>\<beta> s[x::=t]" 105proof - 106 obtain y::name where y: "y \<sharp> (x, s, t)" 107 by (rule exists_fresh) (rule fin_supp) 108 then have "y \<sharp> t" by simp 109 then have "(Lam [y]. [(y, x)] \<bullet> s) \<degree> t \<rightarrow>\<^sub>\<beta> ([(y, x)] \<bullet> s)[y::=t]" 110 by (rule beta) 111 moreover from y have "(Lam [x].s) = (Lam [y]. [(y, x)] \<bullet> s)" 112 by (auto simp add: lam.inject alpha' fresh_prod fresh_atm) 113 ultimately show ?thesis using y by (simp add: subst_rename) 114qed 115 116abbreviation 117 beta_reds :: "lam \<Rightarrow> lam \<Rightarrow> bool" (infixl "\<rightarrow>\<^sub>\<beta>\<^sup>*" 50) where 118 "s \<rightarrow>\<^sub>\<beta>\<^sup>* t \<equiv> beta\<^sup>*\<^sup>* s t" 119 120 121subsection \<open>Application of a term to a list of terms\<close> 122 123abbreviation 124 list_application :: "lam \<Rightarrow> lam list \<Rightarrow> lam" (infixl "\<degree>\<degree>" 150) where 125 "t \<degree>\<degree> ts \<equiv> foldl (\<degree>) t ts" 126 127lemma apps_eq_tail_conv [iff]: "(r \<degree>\<degree> ts = s \<degree>\<degree> ts) = (r = s)" 128 by (induct ts rule: rev_induct) (auto simp add: lam.inject) 129 130lemma Var_eq_apps_conv [iff]: "(Var m = s \<degree>\<degree> ss) = (Var m = s \<and> ss = [])" 131 by (induct ss arbitrary: s) auto 132 133lemma Var_apps_eq_Var_apps_conv [iff]: 134 "(Var m \<degree>\<degree> rs = Var n \<degree>\<degree> ss) = (m = n \<and> rs = ss)" 135 apply (induct rs arbitrary: ss rule: rev_induct) 136 apply (simp add: lam.inject) 137 apply blast 138 apply (induct_tac ss rule: rev_induct) 139 apply (auto simp add: lam.inject) 140 done 141 142lemma App_eq_foldl_conv: 143 "(r \<degree> s = t \<degree>\<degree> ts) = 144 (if ts = [] then r \<degree> s = t 145 else (\<exists>ss. ts = ss @ [s] \<and> r = t \<degree>\<degree> ss))" 146 apply (rule_tac xs = ts in rev_exhaust) 147 apply (auto simp add: lam.inject) 148 done 149 150lemma Abs_eq_apps_conv [iff]: 151 "((Lam [x].r) = s \<degree>\<degree> ss) = ((Lam [x].r) = s \<and> ss = [])" 152 by (induct ss rule: rev_induct) auto 153 154lemma apps_eq_Abs_conv [iff]: "(s \<degree>\<degree> ss = (Lam [x].r)) = (s = (Lam [x].r) \<and> ss = [])" 155 by (induct ss rule: rev_induct) auto 156 157lemma Abs_App_neq_Var_apps [iff]: 158 "(Lam [x].s) \<degree> t \<noteq> Var n \<degree>\<degree> ss" 159 by (induct ss arbitrary: s t rule: rev_induct) (auto simp add: lam.inject) 160 161lemma Var_apps_neq_Abs_apps [iff]: 162 "Var n \<degree>\<degree> ts \<noteq> (Lam [x].r) \<degree>\<degree> ss" 163 apply (induct ss arbitrary: ts rule: rev_induct) 164 apply simp 165 apply (induct_tac ts rule: rev_induct) 166 apply (auto simp add: lam.inject) 167 done 168 169lemma ex_head_tail: 170 "\<exists>ts h. t = h \<degree>\<degree> ts \<and> ((\<exists>n. h = Var n) \<or> (\<exists>x u. h = (Lam [x].u)))" 171 apply (induct t rule: lam.induct) 172 apply (metis foldl_Nil) 173 apply (metis foldl_Cons foldl_Nil foldl_append) 174 apply (metis foldl_Nil) 175 done 176 177lemma size_apps [simp]: 178 "size (r \<degree>\<degree> rs) = size r + foldl (+) 0 (map size rs) + length rs" 179 by (induct rs rule: rev_induct) auto 180 181lemma lem0: "(0::nat) < k \<Longrightarrow> m \<le> n \<Longrightarrow> m < n + k" 182 by simp 183 184lemma subst_map [simp]: 185 "(t \<degree>\<degree> ts)[x::=u] = t[x::=u] \<degree>\<degree> map (\<lambda>t. t[x::=u]) ts" 186 by (induct ts arbitrary: t) simp_all 187 188lemma app_last: "(t \<degree>\<degree> ts) \<degree> u = t \<degree>\<degree> (ts @ [u])" 189 by simp 190 191lemma perm_apps [eqvt]: 192 "(pi::name prm) \<bullet> (t \<degree>\<degree> ts) = ((pi \<bullet> t) \<degree>\<degree> (pi \<bullet> ts))" 193 by (induct ts rule: rev_induct) (auto simp add: append_eqvt) 194 195lemma fresh_apps [simp]: "(x::name) \<sharp> (t \<degree>\<degree> ts) = (x \<sharp> t \<and> x \<sharp> ts)" 196 by (induct ts rule: rev_induct) 197 (auto simp add: fresh_list_append fresh_list_nil fresh_list_cons) 198 199text \<open>A customized induction schema for \<open>\<degree>\<degree>\<close>.\<close> 200 201lemma lem: 202 assumes "\<And>n ts (z::'a::fs_name). (\<And>z. \<forall>t \<in> set ts. P z t) \<Longrightarrow> P z (Var n \<degree>\<degree> ts)" 203 and "\<And>x u ts z. x \<sharp> z \<Longrightarrow> (\<And>z. P z u) \<Longrightarrow> (\<And>z. \<forall>t \<in> set ts. P z t) \<Longrightarrow> P z ((Lam [x].u) \<degree>\<degree> ts)" 204 shows "size t = n \<Longrightarrow> P z t" 205 apply (induct n arbitrary: t z rule: nat_less_induct) 206 apply (cut_tac t = t in ex_head_tail) 207 apply clarify 208 apply (erule disjE) 209 apply clarify 210 apply (rule assms) 211 apply clarify 212 apply (erule allE, erule impE) 213 prefer 2 214 apply (erule allE, erule impE, rule refl, erule spec) 215 apply simp 216 apply (simp only: foldl_conv_fold add.commute fold_plus_sum_list_rev) 217 apply (fastforce simp add: sum_list_map_remove1) 218 apply clarify 219 apply (subgoal_tac "\<exists>y::name. y \<sharp> (x, u, z)") 220 prefer 2 221 apply (blast intro: exists_fresh' fin_supp) 222 apply (erule exE) 223 apply (subgoal_tac "(Lam [x].u) = (Lam [y].([(y, x)] \<bullet> u))") 224 prefer 2 225 apply (auto simp add: lam.inject alpha' fresh_prod fresh_atm)[] 226 apply (simp (no_asm_simp)) 227 apply (rule assms) 228 apply (simp add: fresh_prod) 229 apply (erule allE, erule impE) 230 prefer 2 231 apply (erule allE, erule impE, rule refl, erule spec) 232 apply simp 233 apply clarify 234 apply (erule allE, erule impE) 235 prefer 2 236 apply blast 237 apply simp 238 apply (simp only: foldl_conv_fold add.commute fold_plus_sum_list_rev) 239 apply (fastforce simp add: sum_list_map_remove1) 240 done 241 242theorem Apps_lam_induct: 243 assumes "\<And>n ts (z::'a::fs_name). (\<And>z. \<forall>t \<in> set ts. P z t) \<Longrightarrow> P z (Var n \<degree>\<degree> ts)" 244 and "\<And>x u ts z. x \<sharp> z \<Longrightarrow> (\<And>z. P z u) \<Longrightarrow> (\<And>z. \<forall>t \<in> set ts. P z t) \<Longrightarrow> P z ((Lam [x].u) \<degree>\<degree> ts)" 245 shows "P z t" 246 apply (rule_tac t = t and z = z in lem) 247 prefer 3 248 apply (rule refl) 249 using assms apply blast+ 250 done 251 252 253subsection \<open>Congruence rules\<close> 254 255lemma apps_preserves_beta [simp]: 256 "r \<rightarrow>\<^sub>\<beta> s \<Longrightarrow> r \<degree>\<degree> ss \<rightarrow>\<^sub>\<beta> s \<degree>\<degree> ss" 257 by (induct ss rule: rev_induct) auto 258 259lemma rtrancl_beta_Abs [intro!]: 260 "s \<rightarrow>\<^sub>\<beta>\<^sup>* s' \<Longrightarrow> (Lam [x].s) \<rightarrow>\<^sub>\<beta>\<^sup>* (Lam [x].s')" 261 by (induct set: rtranclp) (blast intro: rtranclp.rtrancl_into_rtrancl)+ 262 263lemma rtrancl_beta_AppL: 264 "s \<rightarrow>\<^sub>\<beta>\<^sup>* s' \<Longrightarrow> s \<degree> t \<rightarrow>\<^sub>\<beta>\<^sup>* s' \<degree> t" 265 by (induct set: rtranclp) (blast intro: rtranclp.rtrancl_into_rtrancl)+ 266 267lemma rtrancl_beta_AppR: 268 "t \<rightarrow>\<^sub>\<beta>\<^sup>* t' \<Longrightarrow> s \<degree> t \<rightarrow>\<^sub>\<beta>\<^sup>* s \<degree> t'" 269 by (induct set: rtranclp) (blast intro: rtranclp.rtrancl_into_rtrancl)+ 270 271lemma rtrancl_beta_App [intro]: 272 "s \<rightarrow>\<^sub>\<beta>\<^sup>* s' \<Longrightarrow> t \<rightarrow>\<^sub>\<beta>\<^sup>* t' \<Longrightarrow> s \<degree> t \<rightarrow>\<^sub>\<beta>\<^sup>* s' \<degree> t'" 273 by (blast intro!: rtrancl_beta_AppL rtrancl_beta_AppR intro: rtranclp_trans) 274 275 276subsection \<open>Lifting an order to lists of elements\<close> 277 278definition 279 step1 :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> 'a list \<Rightarrow> bool" where 280 "step1 r = 281 (\<lambda>ys xs. \<exists>us z z' vs. xs = us @ z # vs \<and> r z' z \<and> ys = 282 us @ z' # vs)" 283 284lemma not_Nil_step1 [iff]: "\<not> step1 r [] xs" 285 apply (unfold step1_def) 286 apply blast 287 done 288 289lemma not_step1_Nil [iff]: "\<not> step1 r xs []" 290 apply (unfold step1_def) 291 apply blast 292 done 293 294lemma Cons_step1_Cons [iff]: 295 "(step1 r (y # ys) (x # xs)) = 296 (r y x \<and> xs = ys \<or> x = y \<and> step1 r ys xs)" 297 apply (unfold step1_def) 298 apply (rule iffI) 299 apply (erule exE) 300 apply (rename_tac ts) 301 apply (case_tac ts) 302 apply fastforce 303 apply force 304 apply (erule disjE) 305 apply blast 306 apply (blast intro: Cons_eq_appendI) 307 done 308 309lemma append_step1I: 310 "step1 r ys xs \<and> vs = us \<or> ys = xs \<and> step1 r vs us 311 \<Longrightarrow> step1 r (ys @ vs) (xs @ us)" 312 apply (unfold step1_def) 313 apply auto 314 apply blast 315 apply (blast intro: append_eq_appendI) 316 done 317 318lemma Cons_step1E [elim!]: 319 assumes "step1 r ys (x # xs)" 320 and "\<And>y. ys = y # xs \<Longrightarrow> r y x \<Longrightarrow> R" 321 and "\<And>zs. ys = x # zs \<Longrightarrow> step1 r zs xs \<Longrightarrow> R" 322 shows R 323 using assms 324 apply (cases ys) 325 apply (simp add: step1_def) 326 apply blast 327 done 328 329lemma Snoc_step1_SnocD: 330 "step1 r (ys @ [y]) (xs @ [x]) 331 \<Longrightarrow> (step1 r ys xs \<and> y = x \<or> ys = xs \<and> r y x)" 332 apply (unfold step1_def) 333 apply (clarify del: disjCI) 334 apply (rename_tac vs) 335 apply (rule_tac xs = vs in rev_exhaust) 336 apply force 337 apply simp 338 apply blast 339 done 340 341 342subsection \<open>Lifting beta-reduction to lists\<close> 343 344abbreviation 345 list_beta :: "lam list \<Rightarrow> lam list \<Rightarrow> bool" (infixl "[\<rightarrow>\<^sub>\<beta>]\<^sub>1" 50) where 346 "rs [\<rightarrow>\<^sub>\<beta>]\<^sub>1 ss \<equiv> step1 beta rs ss" 347 348lemma head_Var_reduction: 349 "Var n \<degree>\<degree> rs \<rightarrow>\<^sub>\<beta> v \<Longrightarrow> \<exists>ss. rs [\<rightarrow>\<^sub>\<beta>]\<^sub>1 ss \<and> v = Var n \<degree>\<degree> ss" 350 apply (induct u \<equiv> "Var n \<degree>\<degree> rs" v arbitrary: rs set: beta) 351 apply simp 352 apply (rule_tac xs = rs in rev_exhaust) 353 apply simp 354 apply (atomize, force intro: append_step1I iff: lam.inject) 355 apply (rule_tac xs = rs in rev_exhaust) 356 apply simp 357 apply (auto 0 3 intro: disjI2 [THEN append_step1I] simp add: lam.inject) 358 done 359 360lemma apps_betasE [case_names appL appR beta, consumes 1]: 361 assumes major: "r \<degree>\<degree> rs \<rightarrow>\<^sub>\<beta> s" 362 and cases: "\<And>r'. r \<rightarrow>\<^sub>\<beta> r' \<Longrightarrow> s = r' \<degree>\<degree> rs \<Longrightarrow> R" 363 "\<And>rs'. rs [\<rightarrow>\<^sub>\<beta>]\<^sub>1 rs' \<Longrightarrow> s = r \<degree>\<degree> rs' \<Longrightarrow> R" 364 "\<And>t u us. (x \<sharp> r \<Longrightarrow> r = (Lam [x].t) \<and> rs = u # us \<and> s = t[x::=u] \<degree>\<degree> us) \<Longrightarrow> R" 365 shows R 366proof - 367 from major have 368 "(\<exists>r'. r \<rightarrow>\<^sub>\<beta> r' \<and> s = r' \<degree>\<degree> rs) \<or> 369 (\<exists>rs'. rs [\<rightarrow>\<^sub>\<beta>]\<^sub>1 rs' \<and> s = r \<degree>\<degree> rs') \<or> 370 (\<exists>t u us. x \<sharp> r \<longrightarrow> r = (Lam [x].t) \<and> rs = u # us \<and> s = t[x::=u] \<degree>\<degree> us)" 371 apply (nominal_induct u \<equiv> "r \<degree>\<degree> rs" s avoiding: x r rs rule: beta.strong_induct) 372 apply (simp add: App_eq_foldl_conv) 373 apply (split if_split_asm) 374 apply simp 375 apply blast 376 apply simp 377 apply (rule impI)+ 378 apply (rule disjI2) 379 apply (rule disjI2) 380 apply (subgoal_tac "r = [(xa, x)] \<bullet> (Lam [x].s)") 381 prefer 2 382 apply (simp add: perm_fresh_fresh) 383 apply (drule conjunct1) 384 apply (subgoal_tac "r = (Lam [xa]. [(xa, x)] \<bullet> s)") 385 prefer 2 386 apply (simp add: calc_atm) 387 apply (thin_tac "r = _") 388 apply simp 389 apply (rule exI) 390 apply (rule conjI) 391 apply (rule refl) 392 apply (simp add: abs_fresh fresh_atm fresh_left calc_atm subst_rename) 393 apply (drule App_eq_foldl_conv [THEN iffD1]) 394 apply (split if_split_asm) 395 apply simp 396 apply blast 397 apply (force intro!: disjI1 [THEN append_step1I] simp add: fresh_list_append) 398 apply (drule App_eq_foldl_conv [THEN iffD1]) 399 apply (split if_split_asm) 400 apply simp 401 apply blast 402 apply (clarify, auto 0 3 intro!: exI intro: append_step1I) 403 done 404 with cases show ?thesis by blast 405qed 406 407lemma apps_preserves_betas [simp]: 408 "rs [\<rightarrow>\<^sub>\<beta>]\<^sub>1 ss \<Longrightarrow> r \<degree>\<degree> rs \<rightarrow>\<^sub>\<beta> r \<degree>\<degree> ss" 409 apply (induct rs arbitrary: ss rule: rev_induct) 410 apply simp 411 apply simp 412 apply (rule_tac xs = ss in rev_exhaust) 413 apply simp 414 apply simp 415 apply (drule Snoc_step1_SnocD) 416 apply blast 417 done 418 419 420subsection \<open>Standard reduction relation\<close> 421 422text \<open> 423Based on lecture notes by Ralph Matthes, 424original proof idea due to Ralph Loader. 425\<close> 426 427declare listrel_mono [mono_set] 428 429lemma listrelp_eqvt [eqvt]: 430 fixes f :: "'a::pt_name \<Rightarrow> 'b::pt_name \<Rightarrow> bool" 431 assumes xy: "listrelp f (x::'a::pt_name list) y" 432 shows "listrelp ((pi::name prm) \<bullet> f) (pi \<bullet> x) (pi \<bullet> y)" using xy 433 by induct (simp_all add: listrelp.intros perm_app [symmetric]) 434 435inductive 436 sred :: "lam \<Rightarrow> lam \<Rightarrow> bool" (infixl "\<rightarrow>\<^sub>s" 50) 437 and sredlist :: "lam list \<Rightarrow> lam list \<Rightarrow> bool" (infixl "[\<rightarrow>\<^sub>s]" 50) 438where 439 "s [\<rightarrow>\<^sub>s] t \<equiv> listrelp (\<rightarrow>\<^sub>s) s t" 440| Var: "rs [\<rightarrow>\<^sub>s] rs' \<Longrightarrow> Var x \<degree>\<degree> rs \<rightarrow>\<^sub>s Var x \<degree>\<degree> rs'" 441| Abs: "x \<sharp> (ss, ss') \<Longrightarrow> r \<rightarrow>\<^sub>s r' \<Longrightarrow> ss [\<rightarrow>\<^sub>s] ss' \<Longrightarrow> (Lam [x].r) \<degree>\<degree> ss \<rightarrow>\<^sub>s (Lam [x].r') \<degree>\<degree> ss'" 442| Beta: "x \<sharp> (s, ss, t) \<Longrightarrow> r[x::=s] \<degree>\<degree> ss \<rightarrow>\<^sub>s t \<Longrightarrow> (Lam [x].r) \<degree> s \<degree>\<degree> ss \<rightarrow>\<^sub>s t" 443 444equivariance sred 445nominal_inductive sred 446 by (simp add: abs_fresh)+ 447 448lemma better_sred_Abs: 449 assumes H1: "r \<rightarrow>\<^sub>s r'" 450 and H2: "ss [\<rightarrow>\<^sub>s] ss'" 451 shows "(Lam [x].r) \<degree>\<degree> ss \<rightarrow>\<^sub>s (Lam [x].r') \<degree>\<degree> ss'" 452proof - 453 obtain y::name where y: "y \<sharp> (x, r, r', ss, ss')" 454 by (rule exists_fresh) (rule fin_supp) 455 then have "y \<sharp> (ss, ss')" by simp 456 moreover from H1 have "[(y, x)] \<bullet> (r \<rightarrow>\<^sub>s r')" by (rule perm_boolI) 457 then have "([(y, x)] \<bullet> r) \<rightarrow>\<^sub>s ([(y, x)] \<bullet> r')" by (simp add: eqvts) 458 ultimately have "(Lam [y]. [(y, x)] \<bullet> r) \<degree>\<degree> ss \<rightarrow>\<^sub>s (Lam [y]. [(y, x)] \<bullet> r') \<degree>\<degree> ss'" using H2 459 by (rule sred.Abs) 460 moreover from y have "(Lam [x].r) = (Lam [y]. [(y, x)] \<bullet> r)" 461 by (auto simp add: lam.inject alpha' fresh_prod fresh_atm) 462 moreover from y have "(Lam [x].r') = (Lam [y]. [(y, x)] \<bullet> r')" 463 by (auto simp add: lam.inject alpha' fresh_prod fresh_atm) 464 ultimately show ?thesis by simp 465qed 466 467lemma better_sred_Beta: 468 assumes H: "r[x::=s] \<degree>\<degree> ss \<rightarrow>\<^sub>s t" 469 shows "(Lam [x].r) \<degree> s \<degree>\<degree> ss \<rightarrow>\<^sub>s t" 470proof - 471 obtain y::name where y: "y \<sharp> (x, r, s, ss, t)" 472 by (rule exists_fresh) (rule fin_supp) 473 then have "y \<sharp> (s, ss, t)" by simp 474 moreover from y H have "([(y, x)] \<bullet> r)[y::=s] \<degree>\<degree> ss \<rightarrow>\<^sub>s t" 475 by (simp add: subst_rename) 476 ultimately have "(Lam [y].[(y, x)] \<bullet> r) \<degree> s \<degree>\<degree> ss \<rightarrow>\<^sub>s t" 477 by (rule sred.Beta) 478 moreover from y have "(Lam [x].r) = (Lam [y]. [(y, x)] \<bullet> r)" 479 by (auto simp add: lam.inject alpha' fresh_prod fresh_atm) 480 ultimately show ?thesis by simp 481qed 482 483lemmas better_sred_intros = sred.Var better_sred_Abs better_sred_Beta 484 485lemma refl_listrelp: "\<forall>x\<in>set xs. R x x \<Longrightarrow> listrelp R xs xs" 486 by (induct xs) (auto intro: listrelp.intros) 487 488lemma refl_sred: "t \<rightarrow>\<^sub>s t" 489 by (nominal_induct t rule: Apps_lam_induct) (auto intro: refl_listrelp better_sred_intros) 490 491lemma listrelp_conj1: "listrelp (\<lambda>x y. R x y \<and> S x y) x y \<Longrightarrow> listrelp R x y" 492 by (erule listrelp.induct) (auto intro: listrelp.intros) 493 494lemma listrelp_conj2: "listrelp (\<lambda>x y. R x y \<and> S x y) x y \<Longrightarrow> listrelp S x y" 495 by (erule listrelp.induct) (auto intro: listrelp.intros) 496 497lemma listrelp_app: 498 assumes xsys: "listrelp R xs ys" 499 shows "listrelp R xs' ys' \<Longrightarrow> listrelp R (xs @ xs') (ys @ ys')" using xsys 500 by (induct arbitrary: xs' ys') (auto intro: listrelp.intros) 501 502lemma lemma1: 503 assumes r: "r \<rightarrow>\<^sub>s r'" and s: "s \<rightarrow>\<^sub>s s'" 504 shows "r \<degree> s \<rightarrow>\<^sub>s r' \<degree> s'" using r 505proof induct 506 case (Var rs rs' x) 507 then have "rs [\<rightarrow>\<^sub>s] rs'" by (rule listrelp_conj1) 508 moreover have "[s] [\<rightarrow>\<^sub>s] [s']" by (iprover intro: s listrelp.intros) 509 ultimately have "rs @ [s] [\<rightarrow>\<^sub>s] rs' @ [s']" by (rule listrelp_app) 510 hence "Var x \<degree>\<degree> (rs @ [s]) \<rightarrow>\<^sub>s Var x \<degree>\<degree> (rs' @ [s'])" by (rule sred.Var) 511 thus ?case by (simp only: app_last) 512next 513 case (Abs x ss ss' r r') 514 from Abs(4) have "ss [\<rightarrow>\<^sub>s] ss'" by (rule listrelp_conj1) 515 moreover have "[s] [\<rightarrow>\<^sub>s] [s']" by (iprover intro: s listrelp.intros) 516 ultimately have "ss @ [s] [\<rightarrow>\<^sub>s] ss' @ [s']" by (rule listrelp_app) 517 with \<open>r \<rightarrow>\<^sub>s r'\<close> have "(Lam [x].r) \<degree>\<degree> (ss @ [s]) \<rightarrow>\<^sub>s (Lam [x].r') \<degree>\<degree> (ss' @ [s'])" 518 by (rule better_sred_Abs) 519 thus ?case by (simp only: app_last) 520next 521 case (Beta x u ss t r) 522 hence "r[x::=u] \<degree>\<degree> (ss @ [s]) \<rightarrow>\<^sub>s t \<degree> s'" by (simp only: app_last) 523 hence "(Lam [x].r) \<degree> u \<degree>\<degree> (ss @ [s]) \<rightarrow>\<^sub>s t \<degree> s'" by (rule better_sred_Beta) 524 thus ?case by (simp only: app_last) 525qed 526 527lemma lemma1': 528 assumes ts: "ts [\<rightarrow>\<^sub>s] ts'" 529 shows "r \<rightarrow>\<^sub>s r' \<Longrightarrow> r \<degree>\<degree> ts \<rightarrow>\<^sub>s r' \<degree>\<degree> ts'" using ts 530 by (induct arbitrary: r r') (auto intro: lemma1) 531 532lemma listrelp_betas: 533 assumes ts: "listrelp (\<rightarrow>\<^sub>\<beta>\<^sup>*) ts ts'" 534 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 535 by induct auto 536 537lemma lemma2: 538 assumes t: "t \<rightarrow>\<^sub>s u" 539 shows "t \<rightarrow>\<^sub>\<beta>\<^sup>* u" using t 540 by induct (auto dest: listrelp_conj2 541 intro: listrelp_betas apps_preserves_beta converse_rtranclp_into_rtranclp) 542 543lemma lemma3: 544 assumes r: "r \<rightarrow>\<^sub>s r'" 545 shows "s \<rightarrow>\<^sub>s s' \<Longrightarrow> r[x::=s] \<rightarrow>\<^sub>s r'[x::=s']" using r 546proof (nominal_induct avoiding: x s s' rule: sred.strong_induct) 547 case (Var rs rs' y) 548 hence "map (\<lambda>t. t[x::=s]) rs [\<rightarrow>\<^sub>s] map (\<lambda>t. t[x::=s']) rs'" 549 by induct (auto intro: listrelp.intros Var) 550 moreover have "Var y[x::=s] \<rightarrow>\<^sub>s Var y[x::=s']" 551 by (cases "y = x") (auto simp add: Var intro: refl_sred) 552 ultimately show ?case by simp (rule lemma1') 553next 554 case (Abs y ss ss' r r') 555 then have "r[x::=s] \<rightarrow>\<^sub>s r'[x::=s']" by fast 556 moreover from Abs(8) \<open>s \<rightarrow>\<^sub>s s'\<close> have "map (\<lambda>t. t[x::=s]) ss [\<rightarrow>\<^sub>s] map (\<lambda>t. t[x::=s']) ss'" 557 by induct (auto intro: listrelp.intros Abs) 558 ultimately show ?case using Abs(6) \<open>y \<sharp> x\<close> \<open>y \<sharp> s\<close> \<open>y \<sharp> s'\<close> 559 by simp (rule better_sred_Abs) 560next 561 case (Beta y u ss t r) 562 thus ?case by (auto simp add: subst_subst fresh_atm intro: better_sred_Beta) 563qed 564 565lemma lemma4_aux: 566 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'" 567 shows "rs' [\<rightarrow>\<^sub>\<beta>]\<^sub>1 ss \<Longrightarrow> rs [\<rightarrow>\<^sub>s] ss" using rs 568proof (induct arbitrary: ss) 569 case Nil 570 thus ?case by cases (auto intro: listrelp.Nil) 571next 572 case (Cons x y xs ys) 573 note Cons' = Cons 574 show ?case 575 proof (cases ss) 576 case Nil with Cons show ?thesis by simp 577 next 578 case (Cons y' ys') 579 hence ss: "ss = y' # ys'" by simp 580 from Cons Cons' have "y \<rightarrow>\<^sub>\<beta> y' \<and> ys' = ys \<or> y' = y \<and> ys [\<rightarrow>\<^sub>\<beta>]\<^sub>1 ys'" by simp 581 hence "x # xs [\<rightarrow>\<^sub>s] y' # ys'" 582 proof 583 assume H: "y \<rightarrow>\<^sub>\<beta> y' \<and> ys' = ys" 584 with Cons' have "x \<rightarrow>\<^sub>s y'" by blast 585 moreover from Cons' have "xs [\<rightarrow>\<^sub>s] ys" by (iprover dest: listrelp_conj1) 586 ultimately have "x # xs [\<rightarrow>\<^sub>s] y' # ys" by (rule listrelp.Cons) 587 with H show ?thesis by simp 588 next 589 assume H: "y' = y \<and> ys [\<rightarrow>\<^sub>\<beta>]\<^sub>1 ys'" 590 with Cons' have "x \<rightarrow>\<^sub>s y'" by blast 591 moreover from H have "xs [\<rightarrow>\<^sub>s] ys'" by (blast intro: Cons') 592 ultimately show ?thesis by (rule listrelp.Cons) 593 qed 594 with ss show ?thesis by simp 595 qed 596qed 597 598lemma lemma4: 599 assumes r: "r \<rightarrow>\<^sub>s r'" 600 shows "r' \<rightarrow>\<^sub>\<beta> r'' \<Longrightarrow> r \<rightarrow>\<^sub>s r''" using r 601proof (nominal_induct avoiding: r'' rule: sred.strong_induct) 602 case (Var rs rs' x) 603 then obtain ss where rs: "rs' [\<rightarrow>\<^sub>\<beta>]\<^sub>1 ss" and r'': "r'' = Var x \<degree>\<degree> ss" 604 by (blast dest: head_Var_reduction) 605 from Var(1) [simplified] rs have "rs [\<rightarrow>\<^sub>s] ss" by (rule lemma4_aux) 606 hence "Var x \<degree>\<degree> rs \<rightarrow>\<^sub>s Var x \<degree>\<degree> ss" by (rule sred.Var) 607 with r'' show ?case by simp 608next 609 case (Abs x ss ss' r r') 610 from \<open>(Lam [x].r') \<degree>\<degree> ss' \<rightarrow>\<^sub>\<beta> r''\<close> show ?case 611 proof (cases rule: apps_betasE [where x=x]) 612 case (appL s) 613 then obtain r''' where s: "s = (Lam [x].r''')" and r''': "r' \<rightarrow>\<^sub>\<beta> r'''" using \<open>x \<sharp> r''\<close> 614 by (cases rule: beta.strong_cases) (auto simp add: abs_fresh lam.inject alpha) 615 from r''' have "r \<rightarrow>\<^sub>s r'''" by (blast intro: Abs) 616 moreover from Abs have "ss [\<rightarrow>\<^sub>s] ss'" by (iprover dest: listrelp_conj1) 617 ultimately have "(Lam [x].r) \<degree>\<degree> ss \<rightarrow>\<^sub>s (Lam [x].r''') \<degree>\<degree> ss'" by (rule better_sred_Abs) 618 with appL s show "(Lam [x].r) \<degree>\<degree> ss \<rightarrow>\<^sub>s r''" by simp 619 next 620 case (appR rs') 621 from Abs(6) [simplified] \<open>ss' [\<rightarrow>\<^sub>\<beta>]\<^sub>1 rs'\<close> 622 have "ss [\<rightarrow>\<^sub>s] rs'" by (rule lemma4_aux) 623 with \<open>r \<rightarrow>\<^sub>s r'\<close> have "(Lam [x].r) \<degree>\<degree> ss \<rightarrow>\<^sub>s (Lam [x].r') \<degree>\<degree> rs'" by (rule better_sred_Abs) 624 with appR show "(Lam [x].r) \<degree>\<degree> ss \<rightarrow>\<^sub>s r''" by simp 625 next 626 case (beta t u' us') 627 then have Lam_eq: "(Lam [x].r') = (Lam [x].t)" and ss': "ss' = u' # us'" 628 and r'': "r'' = t[x::=u'] \<degree>\<degree> us'" 629 by (simp_all add: abs_fresh) 630 from Abs(6) ss' obtain u us where 631 ss: "ss = u # us" and u: "u \<rightarrow>\<^sub>s u'" and us: "us [\<rightarrow>\<^sub>s] us'" 632 by cases (auto dest!: listrelp_conj1) 633 have "r[x::=u] \<rightarrow>\<^sub>s r'[x::=u']" using \<open>r \<rightarrow>\<^sub>s r'\<close> and u by (rule lemma3) 634 with us have "r[x::=u] \<degree>\<degree> us \<rightarrow>\<^sub>s r'[x::=u'] \<degree>\<degree> us'" by (rule lemma1') 635 hence "(Lam [x].r) \<degree> u \<degree>\<degree> us \<rightarrow>\<^sub>s r'[x::=u'] \<degree>\<degree> us'" by (rule better_sred_Beta) 636 with ss r'' Lam_eq show "(Lam [x].r) \<degree>\<degree> ss \<rightarrow>\<^sub>s r''" by (simp add: lam.inject alpha) 637 qed 638next 639 case (Beta x s ss t r) 640 show ?case 641 by (rule better_sred_Beta) (rule Beta)+ 642qed 643 644lemma rtrancl_beta_sred: 645 assumes r: "r \<rightarrow>\<^sub>\<beta>\<^sup>* r'" 646 shows "r \<rightarrow>\<^sub>s r'" using r 647 by induct (iprover intro: refl_sred lemma4)+ 648 649 650subsection \<open>Terms in normal form\<close> 651 652lemma listsp_eqvt [eqvt]: 653 assumes xs: "listsp p (xs::'a::pt_name list)" 654 shows "listsp ((pi::name prm) \<bullet> p) (pi \<bullet> xs)" using xs 655 apply induct 656 apply simp 657 apply simp 658 apply (rule listsp.intros) 659 apply (drule_tac pi=pi in perm_boolI) 660 apply perm_simp 661 apply assumption 662 done 663 664inductive NF :: "lam \<Rightarrow> bool" 665where 666 App: "listsp NF ts \<Longrightarrow> NF (Var x \<degree>\<degree> ts)" 667| Abs: "NF t \<Longrightarrow> NF (Lam [x].t)" 668 669equivariance NF 670nominal_inductive NF 671 by (simp add: abs_fresh) 672 673lemma Abs_NF: 674 assumes NF: "NF ((Lam [x].t) \<degree>\<degree> ts)" 675 shows "ts = []" using NF 676proof cases 677 case (App us i) 678 thus ?thesis by (simp add: Var_apps_neq_Abs_apps [THEN not_sym]) 679next 680 case (Abs u) 681 thus ?thesis by simp 682qed 683 684text \<open> 685\<^term>\<open>NF\<close> characterizes exactly the terms that are in normal form. 686\<close> 687 688lemma NF_eq: "NF t = (\<forall>t'. \<not> t \<rightarrow>\<^sub>\<beta> t')" 689proof 690 assume H: "NF t" 691 show "\<forall>t'. \<not> t \<rightarrow>\<^sub>\<beta> t'" 692 proof 693 fix t' 694 from H show "\<not> t \<rightarrow>\<^sub>\<beta> t'" 695 proof (nominal_induct avoiding: t' rule: NF.strong_induct) 696 case (App ts t) 697 show ?case 698 proof 699 assume "Var t \<degree>\<degree> ts \<rightarrow>\<^sub>\<beta> t'" 700 then obtain rs where "ts [\<rightarrow>\<^sub>\<beta>]\<^sub>1 rs" 701 by (iprover dest: head_Var_reduction) 702 with App show False 703 by (induct rs arbitrary: ts) (auto del: in_listspD) 704 qed 705 next 706 case (Abs t x) 707 show ?case 708 proof 709 assume "(Lam [x].t) \<rightarrow>\<^sub>\<beta> t'" 710 then show False using Abs 711 by (cases rule: beta.strong_cases) (auto simp add: abs_fresh lam.inject alpha) 712 qed 713 qed 714 qed 715next 716 assume H: "\<forall>t'. \<not> t \<rightarrow>\<^sub>\<beta> t'" 717 then show "NF t" 718 proof (nominal_induct t rule: Apps_lam_induct) 719 case (1 n ts) 720 then have "\<forall>ts'. \<not> ts [\<rightarrow>\<^sub>\<beta>]\<^sub>1 ts'" 721 by (iprover intro: apps_preserves_betas) 722 with 1(1) have "listsp NF ts" 723 by (induct ts) (auto simp add: in_listsp_conv_set) 724 then show ?case by (rule NF.App) 725 next 726 case (2 x u ts) 727 show ?case 728 proof (cases ts) 729 case Nil thus ?thesis by (metis 2 NF.Abs abs foldl_Nil) 730 next 731 case (Cons r rs) 732 have "(Lam [x].u) \<degree> r \<rightarrow>\<^sub>\<beta> u[x::=r]" .. 733 then have "(Lam [x].u) \<degree> r \<degree>\<degree> rs \<rightarrow>\<^sub>\<beta> u[x::=r] \<degree>\<degree> rs" 734 by (rule apps_preserves_beta) 735 with Cons have "(Lam [x].u) \<degree>\<degree> ts \<rightarrow>\<^sub>\<beta> u[x::=r] \<degree>\<degree> rs" 736 by simp 737 with 2 show ?thesis by iprover 738 qed 739 qed 740qed 741 742 743subsection \<open>Leftmost reduction and weakly normalizing terms\<close> 744 745inductive 746 lred :: "lam \<Rightarrow> lam \<Rightarrow> bool" (infixl "\<rightarrow>\<^sub>l" 50) 747 and lredlist :: "lam list \<Rightarrow> lam list \<Rightarrow> bool" (infixl "[\<rightarrow>\<^sub>l]" 50) 748where 749 "s [\<rightarrow>\<^sub>l] t \<equiv> listrelp (\<rightarrow>\<^sub>l) s t" 750| Var: "rs [\<rightarrow>\<^sub>l] rs' \<Longrightarrow> Var x \<degree>\<degree> rs \<rightarrow>\<^sub>l Var x \<degree>\<degree> rs'" 751| Abs: "r \<rightarrow>\<^sub>l r' \<Longrightarrow> (Lam [x].r) \<rightarrow>\<^sub>l (Lam [x].r')" 752| Beta: "r[x::=s] \<degree>\<degree> ss \<rightarrow>\<^sub>l t \<Longrightarrow> (Lam [x].r) \<degree> s \<degree>\<degree> ss \<rightarrow>\<^sub>l t" 753 754lemma lred_imp_sred: 755 assumes lred: "s \<rightarrow>\<^sub>l t" 756 shows "s \<rightarrow>\<^sub>s t" using lred 757proof induct 758 case (Var rs rs' x) 759 then have "rs [\<rightarrow>\<^sub>s] rs'" 760 by induct (iprover intro: listrelp.intros)+ 761 then show ?case by (rule sred.Var) 762next 763 case (Abs r r' x) 764 from \<open>r \<rightarrow>\<^sub>s r'\<close> 765 have "(Lam [x].r) \<degree>\<degree> [] \<rightarrow>\<^sub>s (Lam [x].r') \<degree>\<degree> []" using listrelp.Nil 766 by (rule better_sred_Abs) 767 then show ?case by simp 768next 769 case (Beta r x s ss t) 770 from \<open>r[x::=s] \<degree>\<degree> ss \<rightarrow>\<^sub>s t\<close> 771 show ?case by (rule better_sred_Beta) 772qed 773 774inductive WN :: "lam \<Rightarrow> bool" 775 where 776 Var: "listsp WN rs \<Longrightarrow> WN (Var n \<degree>\<degree> rs)" 777 | Lambda: "WN r \<Longrightarrow> WN (Lam [x].r)" 778 | Beta: "WN ((r[x::=s]) \<degree>\<degree> ss) \<Longrightarrow> WN (((Lam [x].r) \<degree> s) \<degree>\<degree> ss)" 779 780lemma listrelp_imp_listsp1: 781 assumes H: "listrelp (\<lambda>x y. P x) xs ys" 782 shows "listsp P xs" using H 783 by induct auto 784 785lemma listrelp_imp_listsp2: 786 assumes H: "listrelp (\<lambda>x y. P y) xs ys" 787 shows "listsp P ys" using H 788 by induct auto 789 790lemma lemma5: 791 assumes lred: "r \<rightarrow>\<^sub>l r'" 792 shows "WN r" and "NF r'" using lred 793 by induct 794 (iprover dest: listrelp_conj1 listrelp_conj2 795 listrelp_imp_listsp1 listrelp_imp_listsp2 intro: WN.intros 796 NF.intros)+ 797 798lemma lemma6: 799 assumes wn: "WN r" 800 shows "\<exists>r'. r \<rightarrow>\<^sub>l r'" using wn 801proof induct 802 case (Var rs n) 803 then have "\<exists>rs'. rs [\<rightarrow>\<^sub>l] rs'" 804 by induct (iprover intro: listrelp.intros)+ 805 then show ?case by (iprover intro: lred.Var) 806qed (iprover intro: lred.intros)+ 807 808lemma lemma7: 809 assumes r: "r \<rightarrow>\<^sub>s r'" 810 shows "NF r' \<Longrightarrow> r \<rightarrow>\<^sub>l r'" using r 811proof induct 812 case (Var rs rs' x) 813 from \<open>NF (Var x \<degree>\<degree> rs')\<close> have "listsp NF rs'" 814 by cases simp_all 815 with Var(1) have "rs [\<rightarrow>\<^sub>l] rs'" 816 proof induct 817 case Nil 818 show ?case by (rule listrelp.Nil) 819 next 820 case (Cons x y xs ys) 821 hence "x \<rightarrow>\<^sub>l y" and "xs [\<rightarrow>\<^sub>l] ys" by (auto del: in_listspD) 822 thus ?case by (rule listrelp.Cons) 823 qed 824 thus ?case by (rule lred.Var) 825next 826 case (Abs x ss ss' r r') 827 from \<open>NF ((Lam [x].r') \<degree>\<degree> ss')\<close> 828 have ss': "ss' = []" by (rule Abs_NF) 829 from Abs(4) have ss: "ss = []" using ss' 830 by cases simp_all 831 from ss' Abs have "NF (Lam [x].r')" by simp 832 hence "NF r'" by (cases rule: NF.strong_cases) (auto simp add: abs_fresh lam.inject alpha) 833 with Abs have "r \<rightarrow>\<^sub>l r'" by simp 834 hence "(Lam [x].r) \<rightarrow>\<^sub>l (Lam [x].r')" by (rule lred.Abs) 835 with ss ss' show ?case by simp 836next 837 case (Beta x s ss t r) 838 hence "r[x::=s] \<degree>\<degree> ss \<rightarrow>\<^sub>l t" by simp 839 thus ?case by (rule lred.Beta) 840qed 841 842lemma WN_eq: "WN t = (\<exists>t'. t \<rightarrow>\<^sub>\<beta>\<^sup>* t' \<and> NF t')" 843proof 844 assume "WN t" 845 then have "\<exists>t'. t \<rightarrow>\<^sub>l t'" by (rule lemma6) 846 then obtain t' where t': "t \<rightarrow>\<^sub>l t'" .. 847 then have NF: "NF t'" by (rule lemma5) 848 from t' have "t \<rightarrow>\<^sub>s t'" by (rule lred_imp_sred) 849 then have "t \<rightarrow>\<^sub>\<beta>\<^sup>* t'" by (rule lemma2) 850 with NF show "\<exists>t'. t \<rightarrow>\<^sub>\<beta>\<^sup>* t' \<and> NF t'" by iprover 851next 852 assume "\<exists>t'. t \<rightarrow>\<^sub>\<beta>\<^sup>* t' \<and> NF t'" 853 then obtain t' where t': "t \<rightarrow>\<^sub>\<beta>\<^sup>* t'" and NF: "NF t'" 854 by iprover 855 from t' have "t \<rightarrow>\<^sub>s t'" by (rule rtrancl_beta_sred) 856 then have "t \<rightarrow>\<^sub>l t'" using NF by (rule lemma7) 857 then show "WN t" by (rule lemma5) 858qed 859 860end 861 862