1theory W 2imports "HOL-Nominal.Nominal" 3begin 4 5text \<open>Example for strong induction rules avoiding sets of atoms.\<close> 6 7atom_decl tvar var 8 9abbreviation 10 "difference_list" :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list" ("_ - _" [60,60] 60) 11where 12 "xs - ys \<equiv> [x \<leftarrow> xs. x\<notin>set ys]" 13 14lemma difference_eqvt_tvar[eqvt]: 15 fixes pi::"tvar prm" 16 and Xs Ys::"tvar list" 17 shows "pi\<bullet>(Xs - Ys) = (pi\<bullet>Xs) - (pi\<bullet>Ys)" 18by (induct Xs) (simp_all add: eqvts) 19 20lemma difference_fresh: 21 fixes X::"tvar" 22 and Xs Ys::"tvar list" 23 assumes a: "X\<in>set Ys" 24 shows "X\<sharp>(Xs - Ys)" 25using a 26by (induct Xs) (auto simp add: fresh_list_nil fresh_list_cons fresh_atm) 27 28lemma difference_supset: 29 fixes xs::"'a list" 30 and ys::"'a list" 31 and zs::"'a list" 32 assumes asm: "set xs \<subseteq> set ys" 33 shows "xs - ys = []" 34using asm 35by (induct xs) (auto) 36 37nominal_datatype ty = 38 TVar "tvar" 39 | Fun "ty" "ty" ("_\<rightarrow>_" [100,100] 100) 40 41nominal_datatype tyS = 42 Ty "ty" 43 | ALL "\<guillemotleft>tvar\<guillemotright>tyS" ("\<forall>[_]._" [100,100] 100) 44 45nominal_datatype trm = 46 Var "var" 47 | App "trm" "trm" 48 | Lam "\<guillemotleft>var\<guillemotright>trm" ("Lam [_]._" [100,100] 100) 49 | Let "\<guillemotleft>var\<guillemotright>trm" "trm" 50 51abbreviation 52 LetBe :: "var \<Rightarrow> trm \<Rightarrow> trm \<Rightarrow> trm" ("Let _ be _ in _" [100,100,100] 100) 53where 54 "Let x be t1 in t2 \<equiv> trm.Let x t2 t1" 55 56type_synonym 57 Ctxt = "(var\<times>tyS) list" 58 59text \<open>free type variables\<close> 60 61consts ftv :: "'a \<Rightarrow> tvar list" 62 63overloading 64 ftv_prod \<equiv> "ftv :: ('a \<times> 'b) \<Rightarrow> tvar list" 65 ftv_tvar \<equiv> "ftv :: tvar \<Rightarrow> tvar list" 66 ftv_var \<equiv> "ftv :: var \<Rightarrow> tvar list" 67 ftv_list \<equiv> "ftv :: 'a list \<Rightarrow> tvar list" 68 ftv_ty \<equiv> "ftv :: ty \<Rightarrow> tvar list" 69begin 70 71primrec 72 ftv_prod 73where 74 "ftv_prod (x, y) = (ftv x) @ (ftv y)" 75 76definition 77 ftv_tvar :: "tvar \<Rightarrow> tvar list" 78where 79[simp]: "ftv_tvar X \<equiv> [(X::tvar)]" 80 81definition 82 ftv_var :: "var \<Rightarrow> tvar list" 83where 84[simp]: "ftv_var x \<equiv> []" 85 86primrec 87 ftv_list 88where 89 "ftv_list [] = []" 90| "ftv_list (x#xs) = (ftv x)@(ftv_list xs)" 91 92nominal_primrec 93 ftv_ty :: "ty \<Rightarrow> tvar list" 94where 95 "ftv_ty (TVar X) = [X]" 96| "ftv_ty (T1 \<rightarrow>T2) = (ftv_ty T1) @ (ftv_ty T2)" 97by (rule TrueI)+ 98 99end 100 101lemma ftv_ty_eqvt[eqvt]: 102 fixes pi::"tvar prm" 103 and T::"ty" 104 shows "pi\<bullet>(ftv T) = ftv (pi\<bullet>T)" 105by (nominal_induct T rule: ty.strong_induct) 106 (perm_simp add: append_eqvt)+ 107 108overloading 109 ftv_tyS \<equiv> "ftv :: tyS \<Rightarrow> tvar list" 110begin 111 112nominal_primrec 113 ftv_tyS :: "tyS \<Rightarrow> tvar list" 114where 115 "ftv_tyS (Ty T) = ((ftv (T::ty))::tvar list)" 116| "ftv_tyS (\<forall>[X].S) = (ftv_tyS S) - [X]" 117apply(finite_guess add: ftv_ty_eqvt fs_tvar1)+ 118apply(rule TrueI)+ 119apply(rule difference_fresh) 120apply(simp) 121apply(fresh_guess add: ftv_ty_eqvt fs_tvar1)+ 122done 123 124end 125 126lemma ftv_tyS_eqvt[eqvt]: 127 fixes pi::"tvar prm" 128 and S::"tyS" 129 shows "pi\<bullet>(ftv S) = ftv (pi\<bullet>S)" 130apply(nominal_induct S rule: tyS.strong_induct) 131apply(simp add: eqvts) 132apply(simp only: ftv_tyS.simps) 133apply(simp only: eqvts) 134apply(simp add: eqvts) 135done 136 137lemma ftv_Ctxt_eqvt[eqvt]: 138 fixes pi::"tvar prm" 139 and \<Gamma>::"Ctxt" 140 shows "pi\<bullet>(ftv \<Gamma>) = ftv (pi\<bullet>\<Gamma>)" 141by (induct \<Gamma>) (auto simp add: eqvts) 142 143text \<open>Valid\<close> 144inductive 145 valid :: "Ctxt \<Rightarrow> bool" 146where 147 V_Nil[intro]: "valid []" 148| V_Cons[intro]: "\<lbrakk>valid \<Gamma>;x\<sharp>\<Gamma>\<rbrakk>\<Longrightarrow> valid ((x,S)#\<Gamma>)" 149 150equivariance valid 151 152text \<open>General\<close> 153primrec gen :: "ty \<Rightarrow> tvar list \<Rightarrow> tyS" where 154 "gen T [] = Ty T" 155| "gen T (X#Xs) = \<forall>[X].(gen T Xs)" 156 157lemma gen_eqvt[eqvt]: 158 fixes pi::"tvar prm" 159 shows "pi\<bullet>(gen T Xs) = gen (pi\<bullet>T) (pi\<bullet>Xs)" 160by (induct Xs) (simp_all add: eqvts) 161 162 163 164abbreviation 165 close :: "Ctxt \<Rightarrow> ty \<Rightarrow> tyS" 166where 167 "close \<Gamma> T \<equiv> gen T ((ftv T) - (ftv \<Gamma>))" 168 169lemma close_eqvt[eqvt]: 170 fixes pi::"tvar prm" 171 shows "pi\<bullet>(close \<Gamma> T) = close (pi\<bullet>\<Gamma>) (pi\<bullet>T)" 172by (simp_all only: eqvts) 173 174text \<open>Substitution\<close> 175 176type_synonym Subst = "(tvar\<times>ty) list" 177 178consts 179 psubst :: "Subst \<Rightarrow> 'a \<Rightarrow> 'a" ("_<_>" [100,60] 120) 180 181abbreviation 182 subst :: "'a \<Rightarrow> tvar \<Rightarrow> ty \<Rightarrow> 'a" ("_[_::=_]" [100,100,100] 100) 183where 184 "smth[X::=T] \<equiv> ([(X,T)])<smth>" 185 186fun 187 lookup :: "Subst \<Rightarrow> tvar \<Rightarrow> ty" 188where 189 "lookup [] X = TVar X" 190| "lookup ((Y,T)#\<theta>) X = (if X=Y then T else lookup \<theta> X)" 191 192lemma lookup_eqvt[eqvt]: 193 fixes pi::"tvar prm" 194 shows "pi\<bullet>(lookup \<theta> X) = lookup (pi\<bullet>\<theta>) (pi\<bullet>X)" 195by (induct \<theta>) (auto simp add: eqvts) 196 197lemma lookup_fresh: 198 fixes X::"tvar" 199 assumes a: "X\<sharp>\<theta>" 200 shows "lookup \<theta> X = TVar X" 201using a 202by (induct \<theta>) 203 (auto simp add: fresh_list_cons fresh_prod fresh_atm) 204 205overloading 206 psubst_ty \<equiv> "psubst :: Subst \<Rightarrow> ty \<Rightarrow> ty" 207begin 208 209nominal_primrec 210 psubst_ty 211where 212 "\<theta><TVar X> = lookup \<theta> X" 213| "\<theta><T\<^sub>1 \<rightarrow> T\<^sub>2> = (\<theta><T\<^sub>1>) \<rightarrow> (\<theta><T\<^sub>2>)" 214by (rule TrueI)+ 215 216end 217 218lemma psubst_ty_eqvt[eqvt]: 219 fixes pi::"tvar prm" 220 and \<theta>::"Subst" 221 and T::"ty" 222 shows "pi\<bullet>(\<theta><T>) = (pi\<bullet>\<theta>)<(pi\<bullet>T)>" 223by (induct T rule: ty.induct) (simp_all add: eqvts) 224 225overloading 226 psubst_tyS \<equiv> "psubst :: Subst \<Rightarrow> tyS \<Rightarrow> tyS" 227begin 228 229nominal_primrec 230 psubst_tyS :: "Subst \<Rightarrow> tyS \<Rightarrow> tyS" 231where 232 "\<theta><(Ty T)> = Ty (\<theta><T>)" 233| "X\<sharp>\<theta> \<Longrightarrow> \<theta><(\<forall>[X].S)> = \<forall>[X].(\<theta><S>)" 234apply(finite_guess add: psubst_ty_eqvt fs_tvar1)+ 235apply(rule TrueI)+ 236apply(simp add: abs_fresh) 237apply(fresh_guess add: psubst_ty_eqvt fs_tvar1)+ 238done 239 240end 241 242overloading 243 psubst_Ctxt \<equiv> "psubst :: Subst \<Rightarrow> Ctxt \<Rightarrow> Ctxt" 244begin 245 246fun 247 psubst_Ctxt :: "Subst \<Rightarrow> Ctxt \<Rightarrow> Ctxt" 248where 249 "psubst_Ctxt \<theta> [] = []" 250| "psubst_Ctxt \<theta> ((x,S)#\<Gamma>) = (x,\<theta><S>)#(psubst_Ctxt \<theta> \<Gamma>)" 251 252end 253 254lemma fresh_lookup: 255 fixes X::"tvar" 256 and \<theta>::"Subst" 257 and Y::"tvar" 258 assumes asms: "X\<sharp>Y" "X\<sharp>\<theta>" 259 shows "X\<sharp>(lookup \<theta> Y)" 260 using asms 261 by (induct \<theta>) 262 (auto simp add: fresh_list_cons fresh_prod fresh_atm) 263 264lemma fresh_psubst_ty: 265 fixes X::"tvar" 266 and \<theta>::"Subst" 267 and T::"ty" 268 assumes asms: "X\<sharp>\<theta>" "X\<sharp>T" 269 shows "X\<sharp>\<theta><T>" 270 using asms 271 by (nominal_induct T rule: ty.strong_induct) 272 (auto simp add: fresh_list_append fresh_list_cons fresh_prod fresh_lookup) 273 274lemma fresh_psubst_tyS: 275 fixes X::"tvar" 276 and \<theta>::"Subst" 277 and S::"tyS" 278 assumes asms: "X\<sharp>\<theta>" "X\<sharp>S" 279 shows "X\<sharp>\<theta><S>" 280 using asms 281 by (nominal_induct S avoiding: \<theta> X rule: tyS.strong_induct) 282 (auto simp add: fresh_psubst_ty abs_fresh) 283 284lemma fresh_psubst_Ctxt: 285 fixes X::"tvar" 286 and \<theta>::"Subst" 287 and \<Gamma>::"Ctxt" 288 assumes asms: "X\<sharp>\<theta>" "X\<sharp>\<Gamma>" 289 shows "X\<sharp>\<theta><\<Gamma>>" 290using asms 291by (induct \<Gamma>) 292 (auto simp add: fresh_psubst_tyS fresh_list_cons) 293 294lemma subst_freshfact2_ty: 295 fixes X::"tvar" 296 and Y::"tvar" 297 and T::"ty" 298 assumes asms: "X\<sharp>S" 299 shows "X\<sharp>T[X::=S]" 300 using asms 301by (nominal_induct T rule: ty.strong_induct) 302 (auto simp add: fresh_atm) 303 304text \<open>instance of a type scheme\<close> 305inductive 306 inst :: "ty \<Rightarrow> tyS \<Rightarrow> bool"("_ \<prec> _" [50,51] 50) 307where 308 I_Ty[intro]: "T \<prec> (Ty T)" 309| I_All[intro]: "\<lbrakk>X\<sharp>T'; T \<prec> S\<rbrakk> \<Longrightarrow> T[X::=T'] \<prec> \<forall>[X].S" 310 311equivariance inst[tvar] 312 313nominal_inductive inst 314 by (simp_all add: abs_fresh subst_freshfact2_ty) 315 316lemma subst_forget_ty: 317 fixes T::"ty" 318 and X::"tvar" 319 assumes a: "X\<sharp>T" 320 shows "T[X::=S] = T" 321 using a 322 by (nominal_induct T rule: ty.strong_induct) 323 (auto simp add: fresh_atm) 324 325lemma psubst_ty_lemma: 326 fixes \<theta>::"Subst" 327 and X::"tvar" 328 and T'::"ty" 329 and T::"ty" 330 assumes a: "X\<sharp>\<theta>" 331 shows "\<theta><T[X::=T']> = (\<theta><T>)[X::=\<theta><T'>]" 332using a 333apply(nominal_induct T avoiding: \<theta> X T' rule: ty.strong_induct) 334apply(auto simp add: ty.inject lookup_fresh) 335apply(rule sym) 336apply(rule subst_forget_ty) 337apply(rule fresh_lookup) 338apply(simp_all add: fresh_atm) 339done 340 341lemma general_preserved: 342 fixes \<theta>::"Subst" 343 assumes a: "T \<prec> S" 344 shows "\<theta><T> \<prec> \<theta><S>" 345using a 346apply(nominal_induct T S avoiding: \<theta> rule: inst.strong_induct) 347apply(auto)[1] 348apply(simp add: psubst_ty_lemma) 349apply(rule_tac I_All) 350apply(simp add: fresh_psubst_ty) 351apply(simp) 352done 353 354 355text\<open>typing judgements\<close> 356inductive 357 typing :: "Ctxt \<Rightarrow> trm \<Rightarrow> ty \<Rightarrow> bool" (" _ \<turnstile> _ : _ " [60,60,60] 60) 358where 359 T_VAR[intro]: "\<lbrakk>valid \<Gamma>; (x,S)\<in>set \<Gamma>; T \<prec> S\<rbrakk>\<Longrightarrow> \<Gamma> \<turnstile> Var x : T" 360| T_APP[intro]: "\<lbrakk>\<Gamma> \<turnstile> t\<^sub>1 : T\<^sub>1\<rightarrow>T\<^sub>2; \<Gamma> \<turnstile> t\<^sub>2 : T\<^sub>1\<rbrakk>\<Longrightarrow> \<Gamma> \<turnstile> App t\<^sub>1 t\<^sub>2 : T\<^sub>2" 361| T_LAM[intro]: "\<lbrakk>x\<sharp>\<Gamma>;((x,Ty T\<^sub>1)#\<Gamma>) \<turnstile> t : T\<^sub>2\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> Lam [x].t : T\<^sub>1\<rightarrow>T\<^sub>2" 362| T_LET[intro]: "\<lbrakk>x\<sharp>\<Gamma>; \<Gamma> \<turnstile> t\<^sub>1 : T\<^sub>1; ((x,close \<Gamma> T\<^sub>1)#\<Gamma>) \<turnstile> t\<^sub>2 : T\<^sub>2; set (ftv T\<^sub>1 - ftv \<Gamma>) \<sharp>* T\<^sub>2\<rbrakk> 363 \<Longrightarrow> \<Gamma> \<turnstile> Let x be t\<^sub>1 in t\<^sub>2 : T\<^sub>2" 364 365equivariance typing[tvar] 366 367lemma fresh_tvar_trm: 368 fixes X::"tvar" 369 and t::"trm" 370 shows "X\<sharp>t" 371by (nominal_induct t rule: trm.strong_induct) 372 (simp_all add: fresh_atm abs_fresh) 373 374lemma ftv_ty: 375 fixes T::"ty" 376 shows "supp T = set (ftv T)" 377by (nominal_induct T rule: ty.strong_induct) 378 (simp_all add: ty.supp supp_atm) 379 380lemma ftv_tyS: 381 fixes S::"tyS" 382 shows "supp S = set (ftv S)" 383by (nominal_induct S rule: tyS.strong_induct) 384 (auto simp add: tyS.supp abs_supp ftv_ty) 385 386lemma ftv_Ctxt: 387 fixes \<Gamma>::"Ctxt" 388 shows "supp \<Gamma> = set (ftv \<Gamma>)" 389apply (induct \<Gamma>) 390apply (simp_all add: supp_list_nil supp_list_cons) 391apply (rename_tac a \<Gamma>') 392apply (case_tac a) 393apply (simp add: supp_prod supp_atm ftv_tyS) 394done 395 396lemma ftv_tvars: 397 fixes Tvs::"tvar list" 398 shows "supp Tvs = set Tvs" 399by (induct Tvs) 400 (simp_all add: supp_list_nil supp_list_cons supp_atm) 401 402lemma difference_supp: 403 fixes xs ys::"tvar list" 404 shows "((supp (xs - ys))::tvar set) = supp xs - supp ys" 405by (induct xs) 406 (auto simp add: supp_list_nil supp_list_cons ftv_tvars) 407 408lemma set_supp_eq: 409 fixes xs::"tvar list" 410 shows "set xs = supp xs" 411by (induct xs) 412 (simp_all add: supp_list_nil supp_list_cons supp_atm) 413 414nominal_inductive2 typing 415 avoids T_LET: "set (ftv T\<^sub>1 - ftv \<Gamma>)" 416apply (simp add: fresh_star_def fresh_def ftv_Ctxt) 417apply (simp add: fresh_star_def fresh_tvar_trm) 418apply assumption 419apply simp 420done 421 422lemma perm_fresh_fresh_aux: 423 "\<forall>(x,y)\<in>set (pi::tvar prm). x \<sharp> z \<and> y \<sharp> z \<Longrightarrow> pi \<bullet> (z::'a::pt_tvar) = z" 424 apply (induct pi rule: rev_induct) 425 apply simp 426 apply (simp add: split_paired_all pt_tvar2) 427 apply (frule_tac x="(a, b)" in bspec) 428 apply simp 429 apply (simp add: perm_fresh_fresh) 430 done 431 432lemma freshs_mem: 433 fixes S::"tvar set" 434 assumes "x \<in> S" 435 and "S \<sharp>* z" 436 shows "x \<sharp> z" 437using assms by (simp add: fresh_star_def) 438 439lemma fresh_gen_set: 440 fixes X::"tvar" 441 and Xs::"tvar list" 442 assumes asm: "X\<in>set Xs" 443 shows "X\<sharp>gen T Xs" 444using asm 445apply(induct Xs) 446apply(simp) 447apply(rename_tac a Xs') 448apply(case_tac "X=a") 449apply(simp add: abs_fresh) 450apply(simp add: abs_fresh) 451done 452 453lemma close_fresh: 454 fixes \<Gamma>::"Ctxt" 455 shows "\<forall>(X::tvar)\<in>set ((ftv T) - (ftv \<Gamma>)). X\<sharp>(close \<Gamma> T)" 456by (simp add: fresh_gen_set) 457 458lemma gen_supp: 459 shows "(supp (gen T Xs)::tvar set) = supp T - supp Xs" 460by (induct Xs) 461 (auto simp add: supp_list_nil supp_list_cons tyS.supp abs_supp supp_atm) 462 463lemma minus_Int_eq: 464 shows "T - (T - U) = T \<inter> U" 465 by blast 466 467lemma close_supp: 468 shows "supp (close \<Gamma> T) = set (ftv T) \<inter> set (ftv \<Gamma>)" 469 apply (simp add: gen_supp difference_supp ftv_ty ftv_Ctxt) 470 apply (simp only: set_supp_eq minus_Int_eq) 471 done 472 473lemma better_T_LET: 474 assumes x: "x\<sharp>\<Gamma>" 475 and t1: "\<Gamma> \<turnstile> t\<^sub>1 : T\<^sub>1" 476 and t2: "((x,close \<Gamma> T\<^sub>1)#\<Gamma>) \<turnstile> t\<^sub>2 : T\<^sub>2" 477 shows "\<Gamma> \<turnstile> Let x be t\<^sub>1 in t\<^sub>2 : T\<^sub>2" 478proof - 479 have fin: "finite (set (ftv T\<^sub>1 - ftv \<Gamma>))" by simp 480 obtain pi where pi1: "(pi \<bullet> set (ftv T\<^sub>1 - ftv \<Gamma>)) \<sharp>* (T\<^sub>2, \<Gamma>)" 481 and pi2: "set pi \<subseteq> set (ftv T\<^sub>1 - ftv \<Gamma>) \<times> (pi \<bullet> set (ftv T\<^sub>1 - ftv \<Gamma>))" 482 by (rule at_set_avoiding [OF at_tvar_inst fin fs_tvar1, of "(T\<^sub>2, \<Gamma>)"]) 483 from pi1 have pi1': "(pi \<bullet> set (ftv T\<^sub>1 - ftv \<Gamma>)) \<sharp>* \<Gamma>" 484 by (simp add: fresh_star_prod) 485 have Gamma_fresh: "\<forall>(x,y)\<in>set pi. x \<sharp> \<Gamma> \<and> y \<sharp> \<Gamma>" 486 apply (rule ballI) 487 apply (simp add: split_paired_all) 488 apply (drule subsetD [OF pi2]) 489 apply (erule SigmaE) 490 apply (drule freshs_mem [OF _ pi1']) 491 apply (simp add: ftv_Ctxt [symmetric] fresh_def) 492 done 493 have close_fresh': "\<forall>(x, y)\<in>set pi. x \<sharp> close \<Gamma> T\<^sub>1 \<and> y \<sharp> close \<Gamma> T\<^sub>1" 494 apply (rule ballI) 495 apply (simp add: split_paired_all) 496 apply (drule subsetD [OF pi2]) 497 apply (erule SigmaE) 498 apply (drule bspec [OF close_fresh]) 499 apply (drule freshs_mem [OF _ pi1']) 500 apply (simp add: fresh_def close_supp ftv_Ctxt) 501 done 502 note x 503 moreover from Gamma_fresh perm_boolI [OF t1, of pi] 504 have "\<Gamma> \<turnstile> t\<^sub>1 : pi \<bullet> T\<^sub>1" 505 by (simp add: perm_fresh_fresh_aux eqvts fresh_tvar_trm) 506 moreover from t2 close_fresh' 507 have "(x,(pi \<bullet> close \<Gamma> T\<^sub>1))#\<Gamma> \<turnstile> t\<^sub>2 : T\<^sub>2" 508 by (simp add: perm_fresh_fresh_aux) 509 with Gamma_fresh have "(x,close \<Gamma> (pi \<bullet> T\<^sub>1))#\<Gamma> \<turnstile> t\<^sub>2 : T\<^sub>2" 510 by (simp add: close_eqvt perm_fresh_fresh_aux) 511 moreover from pi1 Gamma_fresh 512 have "set (ftv (pi \<bullet> T\<^sub>1) - ftv \<Gamma>) \<sharp>* T\<^sub>2" 513 by (simp only: eqvts fresh_star_prod perm_fresh_fresh_aux) 514 ultimately show ?thesis by (rule T_LET) 515qed 516 517lemma ftv_ty_subst: 518 fixes T::"ty" 519 and \<theta>::"Subst" 520 and X Y ::"tvar" 521 assumes a1: "X \<in> set (ftv T)" 522 and a2: "Y \<in> set (ftv (lookup \<theta> X))" 523 shows "Y \<in> set (ftv (\<theta><T>))" 524using a1 a2 525by (nominal_induct T rule: ty.strong_induct) (auto) 526 527lemma ftv_tyS_subst: 528 fixes S::"tyS" 529 and \<theta>::"Subst" 530 and X Y::"tvar" 531 assumes a1: "X \<in> set (ftv S)" 532 and a2: "Y \<in> set (ftv (lookup \<theta> X))" 533 shows "Y \<in> set (ftv (\<theta><S>))" 534using a1 a2 535by (nominal_induct S avoiding: \<theta> Y rule: tyS.strong_induct) 536 (auto simp add: ftv_ty_subst fresh_atm) 537 538lemma ftv_Ctxt_subst: 539 fixes \<Gamma>::"Ctxt" 540 and \<theta>::"Subst" 541 assumes a1: "X \<in> set (ftv \<Gamma>)" 542 and a2: "Y \<in> set (ftv (lookup \<theta> X))" 543 shows "Y \<in> set (ftv (\<theta><\<Gamma>>))" 544using a1 a2 545by (induct \<Gamma>) 546 (auto simp add: ftv_tyS_subst) 547 548lemma gen_preserved1: 549 assumes asm: "Xs \<sharp>* \<theta>" 550 shows "\<theta><gen T Xs> = gen (\<theta><T>) Xs" 551using asm 552by (induct Xs) 553 (auto simp add: fresh_star_def) 554 555lemma gen_preserved2: 556 fixes T::"ty" 557 and \<Gamma>::"Ctxt" 558 assumes asm: "((ftv T) - (ftv \<Gamma>)) \<sharp>* \<theta>" 559 shows "((ftv (\<theta><T>)) - (ftv (\<theta><\<Gamma>>))) = ((ftv T) - (ftv \<Gamma>))" 560using asm 561apply(nominal_induct T rule: ty.strong_induct) 562apply(auto simp add: fresh_star_def) 563apply(simp add: lookup_fresh) 564apply(simp add: ftv_Ctxt[symmetric]) 565apply(fold fresh_def) 566apply(rule fresh_psubst_Ctxt) 567apply(assumption) 568apply(assumption) 569apply(rule difference_supset) 570apply(auto) 571apply(simp add: ftv_Ctxt_subst) 572done 573 574lemma close_preserved: 575 fixes \<Gamma>::"Ctxt" 576 assumes asm: "((ftv T) - (ftv \<Gamma>)) \<sharp>* \<theta>" 577 shows "\<theta><close \<Gamma> T> = close (\<theta><\<Gamma>>) (\<theta><T>)" 578using asm 579by (simp add: gen_preserved1 gen_preserved2) 580 581lemma var_fresh_for_ty: 582 fixes x::"var" 583 and T::"ty" 584 shows "x\<sharp>T" 585by (nominal_induct T rule: ty.strong_induct) 586 (simp_all add: fresh_atm) 587 588lemma var_fresh_for_tyS: 589 fixes x::"var" 590 and S::"tyS" 591 shows "x\<sharp>S" 592by (nominal_induct S rule: tyS.strong_induct) 593 (simp_all add: abs_fresh var_fresh_for_ty) 594 595lemma psubst_fresh_Ctxt: 596 fixes x::"var" 597 and \<Gamma>::"Ctxt" 598 and \<theta>::"Subst" 599 shows "x\<sharp>\<theta><\<Gamma>> = x\<sharp>\<Gamma>" 600by (induct \<Gamma>) 601 (auto simp add: fresh_list_cons fresh_list_nil fresh_prod var_fresh_for_tyS) 602 603lemma psubst_valid: 604 fixes \<theta>::Subst 605 and \<Gamma>::Ctxt 606 assumes a: "valid \<Gamma>" 607 shows "valid (\<theta><\<Gamma>>)" 608using a 609by (induct) 610 (auto simp add: psubst_fresh_Ctxt) 611 612lemma psubst_in: 613 fixes \<Gamma>::"Ctxt" 614 and \<theta>::"Subst" 615 and pi::"tvar prm" 616 and S::"tyS" 617 assumes a: "(x,S)\<in>set \<Gamma>" 618 shows "(x,\<theta><S>)\<in>set (\<theta><\<Gamma>>)" 619using a 620by (induct \<Gamma>) 621 (auto simp add: calc_atm) 622 623 624lemma typing_preserved: 625 fixes \<theta>::"Subst" 626 and pi::"tvar prm" 627 assumes a: "\<Gamma> \<turnstile> t : T" 628 shows "(\<theta><\<Gamma>>) \<turnstile> t : (\<theta><T>)" 629using a 630proof (nominal_induct \<Gamma> t T avoiding: \<theta> rule: typing.strong_induct) 631 case (T_VAR \<Gamma> x S T) 632 have a1: "valid \<Gamma>" by fact 633 have a2: "(x, S) \<in> set \<Gamma>" by fact 634 have a3: "T \<prec> S" by fact 635 have "valid (\<theta><\<Gamma>>)" using a1 by (simp add: psubst_valid) 636 moreover 637 have "(x,\<theta><S>)\<in>set (\<theta><\<Gamma>>)" using a2 by (simp add: psubst_in) 638 moreover 639 have "\<theta><T> \<prec> \<theta><S>" using a3 by (simp add: general_preserved) 640 ultimately show "(\<theta><\<Gamma>>) \<turnstile> Var x : (\<theta><T>)" by (simp add: typing.T_VAR) 641next 642 case (T_APP \<Gamma> t1 T1 T2 t2) 643 have "\<theta><\<Gamma>> \<turnstile> t1 : \<theta><T1 \<rightarrow> T2>" by fact 644 then have "\<theta><\<Gamma>> \<turnstile> t1 : (\<theta><T1>) \<rightarrow> (\<theta><T2>)" by simp 645 moreover 646 have "\<theta><\<Gamma>> \<turnstile> t2 : \<theta><T1>" by fact 647 ultimately show "\<theta><\<Gamma>> \<turnstile> App t1 t2 : \<theta><T2>" by (simp add: typing.T_APP) 648next 649 case (T_LAM x \<Gamma> T1 t T2) 650 fix pi::"tvar prm" and \<theta>::"Subst" 651 have "x\<sharp>\<Gamma>" by fact 652 then have "x\<sharp>\<theta><\<Gamma>>" by (simp add: psubst_fresh_Ctxt) 653 moreover 654 have "\<theta><((x, Ty T1)#\<Gamma>)> \<turnstile> t : \<theta><T2>" by fact 655 then have "((x, Ty (\<theta><T1>))#(\<theta><\<Gamma>>)) \<turnstile> t : \<theta><T2>" by (simp add: calc_atm) 656 ultimately show "\<theta><\<Gamma>> \<turnstile> Lam [x].t : \<theta><T1 \<rightarrow> T2>" by (simp add: typing.T_LAM) 657next 658 case (T_LET x \<Gamma> t1 T1 t2 T2) 659 have vc: "((ftv T1) - (ftv \<Gamma>)) \<sharp>* \<theta>" by fact 660 have "x\<sharp>\<Gamma>" by fact 661 then have a1: "x\<sharp>\<theta><\<Gamma>>" by (simp add: calc_atm psubst_fresh_Ctxt) 662 have a2: "\<theta><\<Gamma>> \<turnstile> t1 : \<theta><T1>" by fact 663 have a3: "\<theta><((x, close \<Gamma> T1)#\<Gamma>)> \<turnstile> t2 : \<theta><T2>" by fact 664 from a2 a3 show "\<theta><\<Gamma>> \<turnstile> Let x be t1 in t2 : \<theta><T2>" 665 apply - 666 apply(rule better_T_LET) 667 apply(rule a1) 668 apply(rule a2) 669 apply(simp add: close_preserved vc) 670 done 671qed 672 673 674 675end 676