1theory SN 2imports Lam_Funs 3begin 4 5text \<open>Strong Normalisation proof from the Proofs and Types book\<close> 6 7section \<open>Beta Reduction\<close> 8 9lemma subst_rename: 10 assumes a: "c\<sharp>t1" 11 shows "t1[a::=t2] = ([(c,a)]\<bullet>t1)[c::=t2]" 12using a 13by (nominal_induct t1 avoiding: a c t2 rule: lam.strong_induct) 14 (auto simp add: calc_atm fresh_atm abs_fresh) 15 16lemma forget: 17 assumes a: "a\<sharp>t1" 18 shows "t1[a::=t2] = t1" 19 using a 20by (nominal_induct t1 avoiding: a t2 rule: lam.strong_induct) 21 (auto simp add: abs_fresh fresh_atm) 22 23lemma fresh_fact: 24 fixes a::"name" 25 assumes a: "a\<sharp>t1" "a\<sharp>t2" 26 shows "a\<sharp>t1[b::=t2]" 27using a 28by (nominal_induct t1 avoiding: a b t2 rule: lam.strong_induct) 29 (auto simp add: abs_fresh fresh_atm) 30 31lemma fresh_fact': 32 fixes a::"name" 33 assumes a: "a\<sharp>t2" 34 shows "a\<sharp>t1[a::=t2]" 35using a 36by (nominal_induct t1 avoiding: a t2 rule: lam.strong_induct) 37 (auto simp add: abs_fresh fresh_atm) 38 39lemma subst_lemma: 40 assumes a: "x\<noteq>y" 41 and b: "x\<sharp>L" 42 shows "M[x::=N][y::=L] = M[y::=L][x::=N[y::=L]]" 43using a b 44by (nominal_induct M avoiding: x y N L rule: lam.strong_induct) 45 (auto simp add: fresh_fact forget) 46 47lemma id_subs: 48 shows "t[x::=Var x] = t" 49 by (nominal_induct t avoiding: x rule: lam.strong_induct) 50 (simp_all add: fresh_atm) 51 52lemma lookup_fresh: 53 fixes z::"name" 54 assumes "z\<sharp>\<theta>" "z\<sharp>x" 55 shows "z\<sharp> lookup \<theta> x" 56using assms 57by (induct rule: lookup.induct) (auto simp add: fresh_list_cons) 58 59lemma lookup_fresh': 60 assumes "z\<sharp>\<theta>" 61 shows "lookup \<theta> z = Var z" 62using assms 63by (induct rule: lookup.induct) 64 (auto simp add: fresh_list_cons fresh_prod fresh_atm) 65 66lemma psubst_subst: 67 assumes h:"c\<sharp>\<theta>" 68 shows "(\<theta><t>)[c::=s] = ((c,s)#\<theta>)<t>" 69 using h 70by (nominal_induct t avoiding: \<theta> c s rule: lam.strong_induct) 71 (auto simp add: fresh_list_cons fresh_atm forget lookup_fresh lookup_fresh') 72 73inductive 74 Beta :: "lam\<Rightarrow>lam\<Rightarrow>bool" (" _ \<longrightarrow>\<^sub>\<beta> _" [80,80] 80) 75where 76 b1[intro!]: "s1 \<longrightarrow>\<^sub>\<beta> s2 \<Longrightarrow> App s1 t \<longrightarrow>\<^sub>\<beta> App s2 t" 77| b2[intro!]: "s1\<longrightarrow>\<^sub>\<beta>s2 \<Longrightarrow> App t s1 \<longrightarrow>\<^sub>\<beta> App t s2" 78| b3[intro!]: "s1\<longrightarrow>\<^sub>\<beta>s2 \<Longrightarrow> Lam [a].s1 \<longrightarrow>\<^sub>\<beta> Lam [a].s2" 79| b4[intro!]: "a\<sharp>s2 \<Longrightarrow> App (Lam [a].s1) s2\<longrightarrow>\<^sub>\<beta> (s1[a::=s2])" 80 81equivariance Beta 82 83nominal_inductive Beta 84 by (simp_all add: abs_fresh fresh_fact') 85 86lemma beta_preserves_fresh: 87 fixes a::"name" 88 assumes a: "t\<longrightarrow>\<^sub>\<beta> s" 89 shows "a\<sharp>t \<Longrightarrow> a\<sharp>s" 90using a 91apply(nominal_induct t s avoiding: a rule: Beta.strong_induct) 92apply(auto simp add: abs_fresh fresh_fact fresh_atm) 93done 94 95lemma beta_abs: 96 assumes a: "Lam [a].t\<longrightarrow>\<^sub>\<beta> t'" 97 shows "\<exists>t''. t'=Lam [a].t'' \<and> t\<longrightarrow>\<^sub>\<beta> t''" 98proof - 99 have "a\<sharp>Lam [a].t" by (simp add: abs_fresh) 100 with a have "a\<sharp>t'" by (simp add: beta_preserves_fresh) 101 with a show ?thesis 102 by (cases rule: Beta.strong_cases[where a="a" and aa="a"]) 103 (auto simp add: lam.inject abs_fresh alpha) 104qed 105 106lemma beta_subst: 107 assumes a: "M \<longrightarrow>\<^sub>\<beta> M'" 108 shows "M[x::=N]\<longrightarrow>\<^sub>\<beta> M'[x::=N]" 109using a 110by (nominal_induct M M' avoiding: x N rule: Beta.strong_induct) 111 (auto simp add: fresh_atm subst_lemma fresh_fact) 112 113section \<open>types\<close> 114 115nominal_datatype ty = 116 TVar "nat" 117 | TArr "ty" "ty" (infix "\<rightarrow>" 200) 118 119lemma fresh_ty: 120 fixes a ::"name" 121 and \<tau> ::"ty" 122 shows "a\<sharp>\<tau>" 123by (nominal_induct \<tau> rule: ty.strong_induct) 124 (auto simp add: fresh_nat) 125 126(* valid contexts *) 127 128inductive 129 valid :: "(name\<times>ty) list \<Rightarrow> bool" 130where 131 v1[intro]: "valid []" 132| v2[intro]: "\<lbrakk>valid \<Gamma>;a\<sharp>\<Gamma>\<rbrakk>\<Longrightarrow> valid ((a,\<sigma>)#\<Gamma>)" 133 134equivariance valid 135 136(* typing judgements *) 137 138lemma fresh_context: 139 fixes \<Gamma> :: "(name\<times>ty)list" 140 and a :: "name" 141 assumes a: "a\<sharp>\<Gamma>" 142 shows "\<not>(\<exists>\<tau>::ty. (a,\<tau>)\<in>set \<Gamma>)" 143using a 144by (induct \<Gamma>) 145 (auto simp add: fresh_prod fresh_list_cons fresh_atm) 146 147inductive 148 typing :: "(name\<times>ty) list\<Rightarrow>lam\<Rightarrow>ty\<Rightarrow>bool" ("_ \<turnstile> _ : _" [60,60,60] 60) 149where 150 t1[intro]: "\<lbrakk>valid \<Gamma>; (a,\<tau>)\<in>set \<Gamma>\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> Var a : \<tau>" 151| t2[intro]: "\<lbrakk>\<Gamma> \<turnstile> t1 : \<tau>\<rightarrow>\<sigma>; \<Gamma> \<turnstile> t2 : \<tau>\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> App t1 t2 : \<sigma>" 152| t3[intro]: "\<lbrakk>a\<sharp>\<Gamma>;((a,\<tau>)#\<Gamma>) \<turnstile> t : \<sigma>\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> Lam [a].t : \<tau>\<rightarrow>\<sigma>" 153 154equivariance typing 155 156nominal_inductive typing 157 by (simp_all add: abs_fresh fresh_ty) 158 159subsection \<open>a fact about beta\<close> 160 161definition "NORMAL" :: "lam \<Rightarrow> bool" where 162 "NORMAL t \<equiv> \<not>(\<exists>t'. t\<longrightarrow>\<^sub>\<beta> t')" 163 164lemma NORMAL_Var: 165 shows "NORMAL (Var a)" 166proof - 167 { assume "\<exists>t'. (Var a) \<longrightarrow>\<^sub>\<beta> t'" 168 then obtain t' where "(Var a) \<longrightarrow>\<^sub>\<beta> t'" by blast 169 hence False by (cases) (auto) 170 } 171 thus "NORMAL (Var a)" by (auto simp add: NORMAL_def) 172qed 173 174text \<open>Inductive version of Strong Normalisation\<close> 175inductive 176 SN :: "lam \<Rightarrow> bool" 177where 178 SN_intro: "(\<And>t'. t \<longrightarrow>\<^sub>\<beta> t' \<Longrightarrow> SN t') \<Longrightarrow> SN t" 179 180lemma SN_preserved: 181 assumes a: "SN t1" "t1\<longrightarrow>\<^sub>\<beta> t2" 182 shows "SN t2" 183using a 184by (cases) (auto) 185 186lemma double_SN_aux: 187 assumes a: "SN a" 188 and b: "SN b" 189 and hyp: "\<And>x z. 190 \<lbrakk>\<And>y. x \<longrightarrow>\<^sub>\<beta> y \<Longrightarrow> SN y; \<And>y. x \<longrightarrow>\<^sub>\<beta> y \<Longrightarrow> P y z; 191 \<And>u. z \<longrightarrow>\<^sub>\<beta> u \<Longrightarrow> SN u; \<And>u. z \<longrightarrow>\<^sub>\<beta> u \<Longrightarrow> P x u\<rbrakk> \<Longrightarrow> P x z" 192 shows "P a b" 193proof - 194 from a 195 have r: "\<And>b. SN b \<Longrightarrow> P a b" 196 proof (induct a rule: SN.SN.induct) 197 case (SN_intro x) 198 note SNI' = SN_intro 199 have "SN b" by fact 200 thus ?case 201 proof (induct b rule: SN.SN.induct) 202 case (SN_intro y) 203 show ?case 204 apply (rule hyp) 205 apply (erule SNI') 206 apply (erule SNI') 207 apply (rule SN.SN_intro) 208 apply (erule SN_intro)+ 209 done 210 qed 211 qed 212 from b show ?thesis by (rule r) 213qed 214 215lemma double_SN[consumes 2]: 216 assumes a: "SN a" 217 and b: "SN b" 218 and c: "\<And>x z. \<lbrakk>\<And>y. x \<longrightarrow>\<^sub>\<beta> y \<Longrightarrow> P y z; \<And>u. z \<longrightarrow>\<^sub>\<beta> u \<Longrightarrow> P x u\<rbrakk> \<Longrightarrow> P x z" 219 shows "P a b" 220using a b c 221apply(rule_tac double_SN_aux) 222apply(assumption)+ 223apply(blast) 224done 225 226section \<open>Candidates\<close> 227 228nominal_primrec 229 RED :: "ty \<Rightarrow> lam set" 230where 231 "RED (TVar X) = {t. SN(t)}" 232| "RED (\<tau>\<rightarrow>\<sigma>) = {t. \<forall>u. (u\<in>RED \<tau> \<longrightarrow> (App t u)\<in>RED \<sigma>)}" 233by (rule TrueI)+ 234 235text \<open>neutral terms\<close> 236definition NEUT :: "lam \<Rightarrow> bool" where 237 "NEUT t \<equiv> (\<exists>a. t = Var a) \<or> (\<exists>t1 t2. t = App t1 t2)" 238 239(* a slight hack to get the first element of applications *) 240(* this is needed to get (SN t) from SN (App t s) *) 241inductive 242 FST :: "lam\<Rightarrow>lam\<Rightarrow>bool" (" _ \<guillemotright> _" [80,80] 80) 243where 244 fst[intro!]: "(App t s) \<guillemotright> t" 245 246nominal_primrec 247 fst_app_aux::"lam\<Rightarrow>lam option" 248where 249 "fst_app_aux (Var a) = None" 250| "fst_app_aux (App t1 t2) = Some t1" 251| "fst_app_aux (Lam [x].t) = None" 252apply(finite_guess)+ 253apply(rule TrueI)+ 254apply(simp add: fresh_none) 255apply(fresh_guess)+ 256done 257 258definition 259 fst_app_def[simp]: "fst_app t = the (fst_app_aux t)" 260 261lemma SN_of_FST_of_App: 262 assumes a: "SN (App t s)" 263 shows "SN (fst_app (App t s))" 264using a 265proof - 266 from a have "\<forall>z. (App t s \<guillemotright> z) \<longrightarrow> SN z" 267 by (induct rule: SN.SN.induct) 268 (blast elim: FST.cases intro: SN_intro) 269 then have "SN t" by blast 270 then show "SN (fst_app (App t s))" by simp 271qed 272 273section \<open>Candidates\<close> 274 275definition "CR1" :: "ty \<Rightarrow> bool" where 276 "CR1 \<tau> \<equiv> \<forall>t. (t\<in>RED \<tau> \<longrightarrow> SN t)" 277 278definition "CR2" :: "ty \<Rightarrow> bool" where 279 "CR2 \<tau> \<equiv> \<forall>t t'. (t\<in>RED \<tau> \<and> t \<longrightarrow>\<^sub>\<beta> t') \<longrightarrow> t'\<in>RED \<tau>" 280 281definition "CR3_RED" :: "lam \<Rightarrow> ty \<Rightarrow> bool" where 282 "CR3_RED t \<tau> \<equiv> \<forall>t'. t\<longrightarrow>\<^sub>\<beta> t' \<longrightarrow> t'\<in>RED \<tau>" 283 284definition "CR3" :: "ty \<Rightarrow> bool" where 285 "CR3 \<tau> \<equiv> \<forall>t. (NEUT t \<and> CR3_RED t \<tau>) \<longrightarrow> t\<in>RED \<tau>" 286 287definition "CR4" :: "ty \<Rightarrow> bool" where 288 "CR4 \<tau> \<equiv> \<forall>t. (NEUT t \<and> NORMAL t) \<longrightarrow>t\<in>RED \<tau>" 289 290lemma CR3_implies_CR4: 291 assumes a: "CR3 \<tau>" 292 shows "CR4 \<tau>" 293using a by (auto simp add: CR3_def CR3_RED_def CR4_def NORMAL_def) 294 295(* sub_induction in the arrow-type case for the next proof *) 296lemma sub_induction: 297 assumes a: "SN(u)" 298 and b: "u\<in>RED \<tau>" 299 and c1: "NEUT t" 300 and c2: "CR2 \<tau>" 301 and c3: "CR3 \<sigma>" 302 and c4: "CR3_RED t (\<tau>\<rightarrow>\<sigma>)" 303 shows "(App t u)\<in>RED \<sigma>" 304using a b 305proof (induct) 306 fix u 307 assume as: "u\<in>RED \<tau>" 308 assume ih: " \<And>u'. \<lbrakk>u \<longrightarrow>\<^sub>\<beta> u'; u' \<in> RED \<tau>\<rbrakk> \<Longrightarrow> App t u' \<in> RED \<sigma>" 309 have "NEUT (App t u)" using c1 by (auto simp add: NEUT_def) 310 moreover 311 have "CR3_RED (App t u) \<sigma>" unfolding CR3_RED_def 312 proof (intro strip) 313 fix r 314 assume red: "App t u \<longrightarrow>\<^sub>\<beta> r" 315 moreover 316 { assume "\<exists>t'. t \<longrightarrow>\<^sub>\<beta> t' \<and> r = App t' u" 317 then obtain t' where a1: "t \<longrightarrow>\<^sub>\<beta> t'" and a2: "r = App t' u" by blast 318 have "t'\<in>RED (\<tau>\<rightarrow>\<sigma>)" using c4 a1 by (simp add: CR3_RED_def) 319 then have "App t' u\<in>RED \<sigma>" using as by simp 320 then have "r\<in>RED \<sigma>" using a2 by simp 321 } 322 moreover 323 { assume "\<exists>u'. u \<longrightarrow>\<^sub>\<beta> u' \<and> r = App t u'" 324 then obtain u' where b1: "u \<longrightarrow>\<^sub>\<beta> u'" and b2: "r = App t u'" by blast 325 have "u'\<in>RED \<tau>" using as b1 c2 by (auto simp add: CR2_def) 326 with ih have "App t u' \<in> RED \<sigma>" using b1 by simp 327 then have "r\<in>RED \<sigma>" using b2 by simp 328 } 329 moreover 330 { assume "\<exists>x t'. t = Lam [x].t'" 331 then obtain x t' where "t = Lam [x].t'" by blast 332 then have "NEUT (Lam [x].t')" using c1 by simp 333 then have "False" by (simp add: NEUT_def) 334 then have "r\<in>RED \<sigma>" by simp 335 } 336 ultimately show "r \<in> RED \<sigma>" by (cases) (auto simp add: lam.inject) 337 qed 338 ultimately show "App t u \<in> RED \<sigma>" using c3 by (simp add: CR3_def) 339qed 340 341text \<open>properties of the candiadates\<close> 342lemma RED_props: 343 shows "CR1 \<tau>" and "CR2 \<tau>" and "CR3 \<tau>" 344proof (nominal_induct \<tau> rule: ty.strong_induct) 345 case (TVar a) 346 { case 1 show "CR1 (TVar a)" by (simp add: CR1_def) 347 next 348 case 2 show "CR2 (TVar a)" by (auto intro: SN_preserved simp add: CR2_def) 349 next 350 case 3 show "CR3 (TVar a)" by (auto intro: SN_intro simp add: CR3_def CR3_RED_def) 351 } 352next 353 case (TArr \<tau>1 \<tau>2) 354 { case 1 355 have ih_CR3_\<tau>1: "CR3 \<tau>1" by fact 356 have ih_CR1_\<tau>2: "CR1 \<tau>2" by fact 357 have "\<And>t. t \<in> RED (\<tau>1 \<rightarrow> \<tau>2) \<Longrightarrow> SN t" 358 proof - 359 fix t 360 assume "t \<in> RED (\<tau>1 \<rightarrow> \<tau>2)" 361 then have a: "\<forall>u. u \<in> RED \<tau>1 \<longrightarrow> App t u \<in> RED \<tau>2" by simp 362 from ih_CR3_\<tau>1 have "CR4 \<tau>1" by (simp add: CR3_implies_CR4) 363 moreover 364 fix a have "NEUT (Var a)" by (force simp add: NEUT_def) 365 moreover 366 have "NORMAL (Var a)" by (rule NORMAL_Var) 367 ultimately have "(Var a)\<in> RED \<tau>1" by (simp add: CR4_def) 368 with a have "App t (Var a) \<in> RED \<tau>2" by simp 369 hence "SN (App t (Var a))" using ih_CR1_\<tau>2 by (simp add: CR1_def) 370 thus "SN t" by (auto dest: SN_of_FST_of_App) 371 qed 372 then show "CR1 (\<tau>1 \<rightarrow> \<tau>2)" unfolding CR1_def by simp 373 next 374 case 2 375 have ih_CR2_\<tau>2: "CR2 \<tau>2" by fact 376 then show "CR2 (\<tau>1 \<rightarrow> \<tau>2)" unfolding CR2_def by auto 377 next 378 case 3 379 have ih_CR1_\<tau>1: "CR1 \<tau>1" by fact 380 have ih_CR2_\<tau>1: "CR2 \<tau>1" by fact 381 have ih_CR3_\<tau>2: "CR3 \<tau>2" by fact 382 show "CR3 (\<tau>1 \<rightarrow> \<tau>2)" unfolding CR3_def 383 proof (simp, intro strip) 384 fix t u 385 assume a1: "u \<in> RED \<tau>1" 386 assume a2: "NEUT t \<and> CR3_RED t (\<tau>1 \<rightarrow> \<tau>2)" 387 have "SN(u)" using a1 ih_CR1_\<tau>1 by (simp add: CR1_def) 388 then show "(App t u)\<in>RED \<tau>2" using ih_CR2_\<tau>1 ih_CR3_\<tau>2 a1 a2 by (blast intro: sub_induction) 389 qed 390 } 391qed 392 393text \<open> 394 the next lemma not as simple as on paper, probably because of 395 the stronger double_SN induction 396\<close> 397lemma abs_RED: 398 assumes asm: "\<forall>s\<in>RED \<tau>. t[x::=s]\<in>RED \<sigma>" 399 shows "Lam [x].t\<in>RED (\<tau>\<rightarrow>\<sigma>)" 400proof - 401 have b1: "SN t" 402 proof - 403 have "Var x\<in>RED \<tau>" 404 proof - 405 have "CR4 \<tau>" by (simp add: RED_props CR3_implies_CR4) 406 moreover 407 have "NEUT (Var x)" by (auto simp add: NEUT_def) 408 moreover 409 have "NORMAL (Var x)" by (auto elim: Beta.cases simp add: NORMAL_def) 410 ultimately show "Var x\<in>RED \<tau>" by (simp add: CR4_def) 411 qed 412 then have "t[x::=Var x]\<in>RED \<sigma>" using asm by simp 413 then have "t\<in>RED \<sigma>" by (simp add: id_subs) 414 moreover 415 have "CR1 \<sigma>" by (simp add: RED_props) 416 ultimately show "SN t" by (simp add: CR1_def) 417 qed 418 show "Lam [x].t\<in>RED (\<tau>\<rightarrow>\<sigma>)" 419 proof (simp, intro strip) 420 fix u 421 assume b2: "u\<in>RED \<tau>" 422 then have b3: "SN u" using RED_props by (auto simp add: CR1_def) 423 show "App (Lam [x].t) u \<in> RED \<sigma>" using b1 b3 b2 asm 424 proof(induct t u rule: double_SN) 425 fix t u 426 assume ih1: "\<And>t'. \<lbrakk>t \<longrightarrow>\<^sub>\<beta> t'; u\<in>RED \<tau>; \<forall>s\<in>RED \<tau>. t'[x::=s]\<in>RED \<sigma>\<rbrakk> \<Longrightarrow> App (Lam [x].t') u \<in> RED \<sigma>" 427 assume ih2: "\<And>u'. \<lbrakk>u \<longrightarrow>\<^sub>\<beta> u'; u'\<in>RED \<tau>; \<forall>s\<in>RED \<tau>. t[x::=s]\<in>RED \<sigma>\<rbrakk> \<Longrightarrow> App (Lam [x].t) u' \<in> RED \<sigma>" 428 assume as1: "u \<in> RED \<tau>" 429 assume as2: "\<forall>s\<in>RED \<tau>. t[x::=s]\<in>RED \<sigma>" 430 have "CR3_RED (App (Lam [x].t) u) \<sigma>" unfolding CR3_RED_def 431 proof(intro strip) 432 fix r 433 assume red: "App (Lam [x].t) u \<longrightarrow>\<^sub>\<beta> r" 434 moreover 435 { assume "\<exists>t'. t \<longrightarrow>\<^sub>\<beta> t' \<and> r = App (Lam [x].t') u" 436 then obtain t' where a1: "t \<longrightarrow>\<^sub>\<beta> t'" and a2: "r = App (Lam [x].t') u" by blast 437 have "App (Lam [x].t') u\<in>RED \<sigma>" using ih1 a1 as1 as2 438 apply(auto) 439 apply(drule_tac x="t'" in meta_spec) 440 apply(simp) 441 apply(drule meta_mp) 442 prefer 2 443 apply(auto)[1] 444 apply(rule ballI) 445 apply(drule_tac x="s" in bspec) 446 apply(simp) 447 apply(subgoal_tac "CR2 \<sigma>")(*A*) 448 apply(unfold CR2_def)[1] 449 apply(drule_tac x="t[x::=s]" in spec) 450 apply(drule_tac x="t'[x::=s]" in spec) 451 apply(simp add: beta_subst) 452 (*A*) 453 apply(simp add: RED_props) 454 done 455 then have "r\<in>RED \<sigma>" using a2 by simp 456 } 457 moreover 458 { assume "\<exists>u'. u \<longrightarrow>\<^sub>\<beta> u' \<and> r = App (Lam [x].t) u'" 459 then obtain u' where b1: "u \<longrightarrow>\<^sub>\<beta> u'" and b2: "r = App (Lam [x].t) u'" by blast 460 have "App (Lam [x].t) u'\<in>RED \<sigma>" using ih2 b1 as1 as2 461 apply(auto) 462 apply(drule_tac x="u'" in meta_spec) 463 apply(simp) 464 apply(drule meta_mp) 465 apply(subgoal_tac "CR2 \<tau>") 466 apply(unfold CR2_def)[1] 467 apply(drule_tac x="u" in spec) 468 apply(drule_tac x="u'" in spec) 469 apply(simp) 470 apply(simp add: RED_props) 471 apply(simp) 472 done 473 then have "r\<in>RED \<sigma>" using b2 by simp 474 } 475 moreover 476 { assume "r = t[x::=u]" 477 then have "r\<in>RED \<sigma>" using as1 as2 by auto 478 } 479 ultimately show "r \<in> RED \<sigma>" 480 (* one wants to use the strong elimination principle; for this one 481 has to know that x\<sharp>u *) 482 apply(cases) 483 apply(auto simp add: lam.inject) 484 apply(drule beta_abs) 485 apply(auto)[1] 486 apply(auto simp add: alpha subst_rename) 487 done 488 qed 489 moreover 490 have "NEUT (App (Lam [x].t) u)" unfolding NEUT_def by (auto) 491 ultimately show "App (Lam [x].t) u \<in> RED \<sigma>" using RED_props by (simp add: CR3_def) 492 qed 493qed 494qed 495 496abbreviation 497 mapsto :: "(name\<times>lam) list \<Rightarrow> name \<Rightarrow> lam \<Rightarrow> bool" ("_ maps _ to _" [55,55,55] 55) 498where 499 "\<theta> maps x to e \<equiv> (lookup \<theta> x) = e" 500 501abbreviation 502 closes :: "(name\<times>lam) list \<Rightarrow> (name\<times>ty) list \<Rightarrow> bool" ("_ closes _" [55,55] 55) 503where 504 "\<theta> closes \<Gamma> \<equiv> \<forall>x T. ((x,T) \<in> set \<Gamma> \<longrightarrow> (\<exists>t. \<theta> maps x to t \<and> t \<in> RED T))" 505 506lemma all_RED: 507 assumes a: "\<Gamma> \<turnstile> t : \<tau>" 508 and b: "\<theta> closes \<Gamma>" 509 shows "\<theta><t> \<in> RED \<tau>" 510using a b 511proof(nominal_induct avoiding: \<theta> rule: typing.strong_induct) 512 case (t3 a \<Gamma> \<sigma> t \<tau> \<theta>) \<comment> \<open>lambda case\<close> 513 have ih: "\<And>\<theta>. \<theta> closes ((a,\<sigma>)#\<Gamma>) \<Longrightarrow> \<theta><t> \<in> RED \<tau>" by fact 514 have \<theta>_cond: "\<theta> closes \<Gamma>" by fact 515 have fresh: "a\<sharp>\<Gamma>" "a\<sharp>\<theta>" by fact+ 516 from ih have "\<forall>s\<in>RED \<sigma>. ((a,s)#\<theta>)<t> \<in> RED \<tau>" using fresh \<theta>_cond fresh_context by simp 517 then have "\<forall>s\<in>RED \<sigma>. \<theta><t>[a::=s] \<in> RED \<tau>" using fresh by (simp add: psubst_subst) 518 then have "Lam [a].(\<theta><t>) \<in> RED (\<sigma> \<rightarrow> \<tau>)" by (simp only: abs_RED) 519 then show "\<theta><(Lam [a].t)> \<in> RED (\<sigma> \<rightarrow> \<tau>)" using fresh by simp 520qed auto 521 522section \<open>identity substitution generated from a context \<Gamma>\<close> 523fun 524 "id" :: "(name\<times>ty) list \<Rightarrow> (name\<times>lam) list" 525where 526 "id [] = []" 527| "id ((x,\<tau>)#\<Gamma>) = (x,Var x)#(id \<Gamma>)" 528 529lemma id_maps: 530 shows "(id \<Gamma>) maps a to (Var a)" 531by (induct \<Gamma>) (auto) 532 533lemma id_fresh: 534 fixes a::"name" 535 assumes a: "a\<sharp>\<Gamma>" 536 shows "a\<sharp>(id \<Gamma>)" 537using a 538by (induct \<Gamma>) 539 (auto simp add: fresh_list_nil fresh_list_cons) 540 541lemma id_apply: 542 shows "(id \<Gamma>)<t> = t" 543by (nominal_induct t avoiding: \<Gamma> rule: lam.strong_induct) 544 (auto simp add: id_maps id_fresh) 545 546lemma id_closes: 547 shows "(id \<Gamma>) closes \<Gamma>" 548apply(auto) 549apply(simp add: id_maps) 550apply(subgoal_tac "CR3 T") \<comment> \<open>A\<close> 551apply(drule CR3_implies_CR4) 552apply(simp add: CR4_def) 553apply(drule_tac x="Var x" in spec) 554apply(force simp add: NEUT_def NORMAL_Var) 555\<comment> \<open>A\<close> 556apply(rule RED_props) 557done 558 559lemma typing_implies_RED: 560 assumes a: "\<Gamma> \<turnstile> t : \<tau>" 561 shows "t \<in> RED \<tau>" 562proof - 563 have "(id \<Gamma>)<t>\<in>RED \<tau>" 564 proof - 565 have "(id \<Gamma>) closes \<Gamma>" by (rule id_closes) 566 with a show ?thesis by (rule all_RED) 567 qed 568 thus"t \<in> RED \<tau>" by (simp add: id_apply) 569qed 570 571lemma typing_implies_SN: 572 assumes a: "\<Gamma> \<turnstile> t : \<tau>" 573 shows "SN(t)" 574proof - 575 from a have "t \<in> RED \<tau>" by (rule typing_implies_RED) 576 moreover 577 have "CR1 \<tau>" by (rule RED_props) 578 ultimately show "SN(t)" by (simp add: CR1_def) 579qed 580 581end 582