1(*<*) 2theory Fsub 3imports "HOL-Nominal.Nominal" 4begin 5(*>*) 6 7text\<open>Authors: Christian Urban, 8 Benjamin Pierce, 9 Dimitrios Vytiniotis 10 Stephanie Weirich 11 Steve Zdancewic 12 Julien Narboux 13 Stefan Berghofer 14 15 with great help from Markus Wenzel.\<close> 16 17section \<open>Types for Names, Nominal Datatype Declaration for Types and Terms\<close> 18 19no_syntax 20 "_Map" :: "maplets => 'a \<rightharpoonup> 'b" ("(1[_])") 21 22text \<open>The main point of this solution is to use names everywhere (be they bound, 23 binding or free). In System \FSUB{} there are two kinds of names corresponding to 24 type-variables and to term-variables. These two kinds of names are represented in 25 the nominal datatype package as atom-types \<open>tyvrs\<close> and \<open>vrs\<close>:\<close> 26 27atom_decl tyvrs vrs 28 29text\<open>There are numerous facts that come with this declaration: for example that 30 there are infinitely many elements in \<open>tyvrs\<close> and \<open>vrs\<close>.\<close> 31 32text\<open>The constructors for types and terms in System \FSUB{} contain abstractions 33 over type-variables and term-variables. The nominal datatype package uses 34 \<open>\<guillemotleft>\<dots>\<guillemotright>\<dots>\<close> to indicate where abstractions occur.\<close> 35 36nominal_datatype ty = 37 Tvar "tyvrs" 38 | Top 39 | Arrow "ty" "ty" (infixr "\<rightarrow>" 200) 40 | Forall "\<guillemotleft>tyvrs\<guillemotright>ty" "ty" 41 42nominal_datatype trm = 43 Var "vrs" 44 | Abs "\<guillemotleft>vrs\<guillemotright>trm" "ty" 45 | TAbs "\<guillemotleft>tyvrs\<guillemotright>trm" "ty" 46 | App "trm" "trm" (infixl "\<cdot>" 200) 47 | TApp "trm" "ty" (infixl "\<cdot>\<^sub>\<tau>" 200) 48 49text \<open>To be polite to the eye, some more familiar notation is introduced. 50 Because of the change in the order of arguments, one needs to use 51 translation rules, instead of syntax annotations at the term-constructors 52 as given above for \<^term>\<open>Arrow\<close>.\<close> 53 54abbreviation 55 Forall_syn :: "tyvrs \<Rightarrow> ty \<Rightarrow> ty \<Rightarrow> ty" ("(3\<forall>_<:_./ _)" [0, 0, 10] 10) 56where 57 "\<forall>X<:T\<^sub>1. T\<^sub>2 \<equiv> ty.Forall X T\<^sub>2 T\<^sub>1" 58 59abbreviation 60 Abs_syn :: "vrs \<Rightarrow> ty \<Rightarrow> trm \<Rightarrow> trm" ("(3\<lambda>_:_./ _)" [0, 0, 10] 10) 61where 62 "\<lambda>x:T. t \<equiv> trm.Abs x t T" 63 64abbreviation 65 TAbs_syn :: "tyvrs \<Rightarrow> ty \<Rightarrow> trm \<Rightarrow> trm" ("(3\<lambda>_<:_./ _)" [0, 0, 10] 10) 66where 67 "\<lambda>X<:T. t \<equiv> trm.TAbs X t T" 68 69text \<open>Again there are numerous facts that are proved automatically for \<^typ>\<open>ty\<close> 70 and \<^typ>\<open>trm\<close>: for example that the set of free variables, i.e.~the \<open>support\<close>, 71 is finite. However note that nominal-datatype declarations do \emph{not} define 72 ``classical" constructor-based datatypes, but rather define $\alpha$-equivalence 73 classes---we can for example show that $\alpha$-equivalent \<^typ>\<open>ty\<close>s 74 and \<^typ>\<open>trm\<close>s are equal:\<close> 75 76lemma alpha_illustration: 77 shows "(\<forall>X<:T. Tvar X) = (\<forall>Y<:T. Tvar Y)" 78 and "(\<lambda>x:T. Var x) = (\<lambda>y:T. Var y)" 79 by (simp_all add: ty.inject trm.inject alpha calc_atm fresh_atm) 80 81section \<open>SubTyping Contexts\<close> 82 83nominal_datatype binding = 84 VarB vrs ty 85 | TVarB tyvrs ty 86 87type_synonym env = "binding list" 88 89text \<open>Typing contexts are represented as lists that ``grow" on the left; we 90 thereby deviating from the convention in the POPLmark-paper. The lists contain 91 pairs of type-variables and types (this is sufficient for Part 1A).\<close> 92 93text \<open>In order to state validity-conditions for typing-contexts, the notion of 94 a \<open>dom\<close> of a typing-context is handy.\<close> 95 96nominal_primrec 97 "tyvrs_of" :: "binding \<Rightarrow> tyvrs set" 98where 99 "tyvrs_of (VarB x y) = {}" 100| "tyvrs_of (TVarB x y) = {x}" 101by auto 102 103nominal_primrec 104 "vrs_of" :: "binding \<Rightarrow> vrs set" 105where 106 "vrs_of (VarB x y) = {x}" 107| "vrs_of (TVarB x y) = {}" 108by auto 109 110primrec 111 "ty_dom" :: "env \<Rightarrow> tyvrs set" 112where 113 "ty_dom [] = {}" 114| "ty_dom (X#\<Gamma>) = (tyvrs_of X)\<union>(ty_dom \<Gamma>)" 115 116primrec 117 "trm_dom" :: "env \<Rightarrow> vrs set" 118where 119 "trm_dom [] = {}" 120| "trm_dom (X#\<Gamma>) = (vrs_of X)\<union>(trm_dom \<Gamma>)" 121 122lemma vrs_of_eqvt[eqvt]: 123 fixes pi ::"tyvrs prm" 124 and pi'::"vrs prm" 125 shows "pi \<bullet>(tyvrs_of x) = tyvrs_of (pi\<bullet>x)" 126 and "pi'\<bullet>(tyvrs_of x) = tyvrs_of (pi'\<bullet>x)" 127 and "pi \<bullet>(vrs_of x) = vrs_of (pi\<bullet>x)" 128 and "pi'\<bullet>(vrs_of x) = vrs_of (pi'\<bullet>x)" 129by (nominal_induct x rule: binding.strong_induct) (simp_all add: tyvrs_of.simps eqvts) 130 131lemma doms_eqvt[eqvt]: 132 fixes pi::"tyvrs prm" 133 and pi'::"vrs prm" 134 shows "pi \<bullet>(ty_dom \<Gamma>) = ty_dom (pi\<bullet>\<Gamma>)" 135 and "pi'\<bullet>(ty_dom \<Gamma>) = ty_dom (pi'\<bullet>\<Gamma>)" 136 and "pi \<bullet>(trm_dom \<Gamma>) = trm_dom (pi\<bullet>\<Gamma>)" 137 and "pi'\<bullet>(trm_dom \<Gamma>) = trm_dom (pi'\<bullet>\<Gamma>)" 138by (induct \<Gamma>) (simp_all add: eqvts) 139 140lemma finite_vrs: 141 shows "finite (tyvrs_of x)" 142 and "finite (vrs_of x)" 143by (nominal_induct rule:binding.strong_induct) auto 144 145lemma finite_doms: 146 shows "finite (ty_dom \<Gamma>)" 147 and "finite (trm_dom \<Gamma>)" 148by (induct \<Gamma>) (auto simp add: finite_vrs) 149 150lemma ty_dom_supp: 151 shows "(supp (ty_dom \<Gamma>)) = (ty_dom \<Gamma>)" 152 and "(supp (trm_dom \<Gamma>)) = (trm_dom \<Gamma>)" 153by (simp only: at_fin_set_supp at_tyvrs_inst at_vrs_inst finite_doms)+ 154 155lemma ty_dom_inclusion: 156 assumes a: "(TVarB X T)\<in>set \<Gamma>" 157 shows "X\<in>(ty_dom \<Gamma>)" 158using a by (induct \<Gamma>) (auto) 159 160lemma ty_binding_existence: 161 assumes "X \<in> (tyvrs_of a)" 162 shows "\<exists>T.(TVarB X T=a)" 163 using assms 164by (nominal_induct a rule: binding.strong_induct) (auto) 165 166lemma ty_dom_existence: 167 assumes a: "X\<in>(ty_dom \<Gamma>)" 168 shows "\<exists>T.(TVarB X T)\<in>set \<Gamma>" 169 using a 170 apply (induct \<Gamma>, auto) 171 apply (rename_tac a \<Gamma>') 172 apply (subgoal_tac "\<exists>T.(TVarB X T=a)") 173 apply (auto) 174 apply (auto simp add: ty_binding_existence) 175done 176 177lemma doms_append: 178 shows "ty_dom (\<Gamma>@\<Delta>) = ((ty_dom \<Gamma>) \<union> (ty_dom \<Delta>))" 179 and "trm_dom (\<Gamma>@\<Delta>) = ((trm_dom \<Gamma>) \<union> (trm_dom \<Delta>))" 180 by (induct \<Gamma>) (auto) 181 182lemma ty_vrs_prm_simp: 183 fixes pi::"vrs prm" 184 and S::"ty" 185 shows "pi\<bullet>S = S" 186by (induct S rule: ty.induct) (auto simp add: calc_atm) 187 188lemma fresh_ty_dom_cons: 189 fixes X::"tyvrs" 190 shows "X\<sharp>(ty_dom (Y#\<Gamma>)) = (X\<sharp>(tyvrs_of Y) \<and> X\<sharp>(ty_dom \<Gamma>))" 191 apply (nominal_induct rule:binding.strong_induct) 192 apply (auto) 193 apply (simp add: fresh_def supp_def eqvts) 194 apply (simp add: fresh_fin_insert [OF pt_tyvrs_inst at_tyvrs_inst fs_tyvrs_inst] finite_doms) 195 apply (simp add: fresh_def supp_def eqvts) 196 apply (simp add: fresh_fin_insert [OF pt_tyvrs_inst at_tyvrs_inst fs_tyvrs_inst] finite_doms)+ 197 done 198 199lemma tyvrs_fresh: 200 fixes X::"tyvrs" 201 assumes "X \<sharp> a" 202 shows "X \<sharp> tyvrs_of a" 203 and "X \<sharp> vrs_of a" 204 using assms 205 apply (nominal_induct a rule:binding.strong_induct) 206 apply (auto) 207 apply (fresh_guess)+ 208done 209 210lemma fresh_dom: 211 fixes X::"tyvrs" 212 assumes a: "X\<sharp>\<Gamma>" 213 shows "X\<sharp>(ty_dom \<Gamma>)" 214using a 215apply(induct \<Gamma>) 216apply(simp add: fresh_set_empty) 217apply(simp only: fresh_ty_dom_cons) 218apply(auto simp add: fresh_prod fresh_list_cons tyvrs_fresh) 219done 220 221text \<open>Not all lists of type \<^typ>\<open>env\<close> are well-formed. One condition 222 requires that in \<^term>\<open>TVarB X S#\<Gamma>\<close> all free variables of \<^term>\<open>S\<close> must be 223 in the \<^term>\<open>ty_dom\<close> of \<^term>\<open>\<Gamma>\<close>, that is \<^term>\<open>S\<close> must be \<open>closed\<close> 224 in \<^term>\<open>\<Gamma>\<close>. The set of free variables of \<^term>\<open>S\<close> is the 225 \<open>support\<close> of \<^term>\<open>S\<close>.\<close> 226 227definition "closed_in" :: "ty \<Rightarrow> env \<Rightarrow> bool" ("_ closed'_in _" [100,100] 100) where 228 "S closed_in \<Gamma> \<equiv> (supp S)\<subseteq>(ty_dom \<Gamma>)" 229 230lemma closed_in_eqvt[eqvt]: 231 fixes pi::"tyvrs prm" 232 assumes a: "S closed_in \<Gamma>" 233 shows "(pi\<bullet>S) closed_in (pi\<bullet>\<Gamma>)" 234 using a 235proof - 236 from a have "pi\<bullet>(S closed_in \<Gamma>)" by (simp add: perm_bool) 237 then show "(pi\<bullet>S) closed_in (pi\<bullet>\<Gamma>)" by (simp add: closed_in_def eqvts) 238qed 239 240lemma tyvrs_vrs_prm_simp: 241 fixes pi::"vrs prm" 242 shows "tyvrs_of (pi\<bullet>a) = tyvrs_of a" 243 apply (nominal_induct rule:binding.strong_induct) 244 apply (simp_all add: eqvts) 245 apply (simp add: dj_perm_forget[OF dj_tyvrs_vrs]) 246 done 247 248lemma ty_vrs_fresh: 249 fixes x::"vrs" 250 and T::"ty" 251 shows "x \<sharp> T" 252by (simp add: fresh_def supp_def ty_vrs_prm_simp) 253 254lemma ty_dom_vrs_prm_simp: 255 fixes pi::"vrs prm" 256 and \<Gamma>::"env" 257 shows "(ty_dom (pi\<bullet>\<Gamma>)) = (ty_dom \<Gamma>)" 258 apply(induct \<Gamma>) 259 apply (simp add: eqvts) 260 apply(simp add: tyvrs_vrs_prm_simp) 261done 262 263lemma closed_in_eqvt'[eqvt]: 264 fixes pi::"vrs prm" 265 assumes a: "S closed_in \<Gamma>" 266 shows "(pi\<bullet>S) closed_in (pi\<bullet>\<Gamma>)" 267using a 268by (simp add: closed_in_def ty_dom_vrs_prm_simp ty_vrs_prm_simp) 269 270lemma fresh_vrs_of: 271 fixes x::"vrs" 272 shows "x\<sharp>vrs_of b = x\<sharp>b" 273 by (nominal_induct b rule: binding.strong_induct) 274 (simp_all add: fresh_singleton fresh_set_empty ty_vrs_fresh fresh_atm) 275 276lemma fresh_trm_dom: 277 fixes x::"vrs" 278 shows "x\<sharp> trm_dom \<Gamma> = x\<sharp>\<Gamma>" 279 by (induct \<Gamma>) 280 (simp_all add: fresh_set_empty fresh_list_cons 281 fresh_fin_union [OF pt_vrs_inst at_vrs_inst fs_vrs_inst] 282 finite_doms finite_vrs fresh_vrs_of fresh_list_nil) 283 284lemma closed_in_fresh: "(X::tyvrs) \<sharp> ty_dom \<Gamma> \<Longrightarrow> T closed_in \<Gamma> \<Longrightarrow> X \<sharp> T" 285 by (auto simp add: closed_in_def fresh_def ty_dom_supp) 286 287text \<open>Now validity of a context is a straightforward inductive definition.\<close> 288 289inductive 290 valid_rel :: "env \<Rightarrow> bool" ("\<turnstile> _ ok" [100] 100) 291where 292 valid_nil[simp]: "\<turnstile> [] ok" 293| valid_consT[simp]: "\<lbrakk>\<turnstile> \<Gamma> ok; X\<sharp>(ty_dom \<Gamma>); T closed_in \<Gamma>\<rbrakk> \<Longrightarrow> \<turnstile> (TVarB X T#\<Gamma>) ok" 294| valid_cons [simp]: "\<lbrakk>\<turnstile> \<Gamma> ok; x\<sharp>(trm_dom \<Gamma>); T closed_in \<Gamma>\<rbrakk> \<Longrightarrow> \<turnstile> (VarB x T#\<Gamma>) ok" 295 296equivariance valid_rel 297 298declare binding.inject [simp add] 299declare trm.inject [simp add] 300 301inductive_cases validE[elim]: 302 "\<turnstile> (TVarB X T#\<Gamma>) ok" 303 "\<turnstile> (VarB x T#\<Gamma>) ok" 304 "\<turnstile> (b#\<Gamma>) ok" 305 306declare binding.inject [simp del] 307declare trm.inject [simp del] 308 309lemma validE_append: 310 assumes a: "\<turnstile> (\<Delta>@\<Gamma>) ok" 311 shows "\<turnstile> \<Gamma> ok" 312 using a 313proof (induct \<Delta>) 314 case (Cons a \<Gamma>') 315 then show ?case 316 by (nominal_induct a rule:binding.strong_induct) 317 (auto elim: validE) 318qed (auto) 319 320lemma replace_type: 321 assumes a: "\<turnstile> (\<Delta>@(TVarB X T)#\<Gamma>) ok" 322 and b: "S closed_in \<Gamma>" 323 shows "\<turnstile> (\<Delta>@(TVarB X S)#\<Gamma>) ok" 324using a b 325proof(induct \<Delta>) 326 case Nil 327 then show ?case by (auto elim: validE intro: valid_cons simp add: doms_append closed_in_def) 328next 329 case (Cons a \<Gamma>') 330 then show ?case 331 by (nominal_induct a rule:binding.strong_induct) 332 (auto elim: validE intro!: valid_cons simp add: doms_append closed_in_def) 333qed 334 335text \<open>Well-formed contexts have a unique type-binding for a type-variable.\<close> 336 337lemma uniqueness_of_ctxt: 338 fixes \<Gamma>::"env" 339 assumes a: "\<turnstile> \<Gamma> ok" 340 and b: "(TVarB X T)\<in>set \<Gamma>" 341 and c: "(TVarB X S)\<in>set \<Gamma>" 342 shows "T=S" 343using a b c 344proof (induct) 345 case (valid_consT \<Gamma> X' T') 346 moreover 347 { fix \<Gamma>'::"env" 348 assume a: "X'\<sharp>(ty_dom \<Gamma>')" 349 have "\<not>(\<exists>T.(TVarB X' T)\<in>(set \<Gamma>'))" using a 350 proof (induct \<Gamma>') 351 case (Cons Y \<Gamma>') 352 thus "\<not> (\<exists>T.(TVarB X' T)\<in>set(Y#\<Gamma>'))" 353 by (simp add: fresh_ty_dom_cons 354 fresh_fin_union[OF pt_tyvrs_inst at_tyvrs_inst fs_tyvrs_inst] 355 finite_vrs finite_doms, 356 auto simp add: fresh_atm fresh_singleton) 357 qed (simp) 358 } 359 ultimately show "T=S" by (auto simp add: binding.inject) 360qed (auto) 361 362lemma uniqueness_of_ctxt': 363 fixes \<Gamma>::"env" 364 assumes a: "\<turnstile> \<Gamma> ok" 365 and b: "(VarB x T)\<in>set \<Gamma>" 366 and c: "(VarB x S)\<in>set \<Gamma>" 367 shows "T=S" 368using a b c 369proof (induct) 370 case (valid_cons \<Gamma> x' T') 371 moreover 372 { fix \<Gamma>'::"env" 373 assume a: "x'\<sharp>(trm_dom \<Gamma>')" 374 have "\<not>(\<exists>T.(VarB x' T)\<in>(set \<Gamma>'))" using a 375 proof (induct \<Gamma>') 376 case (Cons y \<Gamma>') 377 thus "\<not> (\<exists>T.(VarB x' T)\<in>set(y#\<Gamma>'))" 378 by (simp add: fresh_fin_union[OF pt_vrs_inst at_vrs_inst fs_vrs_inst] 379 finite_vrs finite_doms, 380 auto simp add: fresh_atm fresh_singleton) 381 qed (simp) 382 } 383 ultimately show "T=S" by (auto simp add: binding.inject) 384qed (auto) 385 386section \<open>Size and Capture-Avoiding Substitution for Types\<close> 387 388nominal_primrec 389 size_ty :: "ty \<Rightarrow> nat" 390where 391 "size_ty (Tvar X) = 1" 392| "size_ty (Top) = 1" 393| "size_ty (T1 \<rightarrow> T2) = (size_ty T1) + (size_ty T2) + 1" 394| "X \<sharp> T1 \<Longrightarrow> size_ty (\<forall>X<:T1. T2) = (size_ty T1) + (size_ty T2) + 1" 395 apply (finite_guess)+ 396 apply (rule TrueI)+ 397 apply (simp add: fresh_nat) 398 apply (fresh_guess)+ 399 done 400 401nominal_primrec 402 subst_ty :: "ty \<Rightarrow> tyvrs \<Rightarrow> ty \<Rightarrow> ty" ("_[_ \<mapsto> _]\<^sub>\<tau>" [300, 0, 0] 300) 403where 404 "(Tvar X)[Y \<mapsto> T]\<^sub>\<tau> = (if X=Y then T else Tvar X)" 405| "(Top)[Y \<mapsto> T]\<^sub>\<tau> = Top" 406| "(T\<^sub>1 \<rightarrow> T\<^sub>2)[Y \<mapsto> T]\<^sub>\<tau> = T\<^sub>1[Y \<mapsto> T]\<^sub>\<tau> \<rightarrow> T\<^sub>2[Y \<mapsto> T]\<^sub>\<tau>" 407| "X\<sharp>(Y,T,T\<^sub>1) \<Longrightarrow> (\<forall>X<:T\<^sub>1. T\<^sub>2)[Y \<mapsto> T]\<^sub>\<tau> = (\<forall>X<:T\<^sub>1[Y \<mapsto> T]\<^sub>\<tau>. T\<^sub>2[Y \<mapsto> T]\<^sub>\<tau>)" 408 apply (finite_guess)+ 409 apply (rule TrueI)+ 410 apply (simp add: abs_fresh) 411 apply (fresh_guess)+ 412 done 413 414lemma subst_eqvt[eqvt]: 415 fixes pi::"tyvrs prm" 416 and T::"ty" 417 shows "pi\<bullet>(T[X \<mapsto> T']\<^sub>\<tau>) = (pi\<bullet>T)[(pi\<bullet>X) \<mapsto> (pi\<bullet>T')]\<^sub>\<tau>" 418 by (nominal_induct T avoiding: X T' rule: ty.strong_induct) 419 (perm_simp add: fresh_bij)+ 420 421lemma subst_eqvt'[eqvt]: 422 fixes pi::"vrs prm" 423 and T::"ty" 424 shows "pi\<bullet>(T[X \<mapsto> T']\<^sub>\<tau>) = (pi\<bullet>T)[(pi\<bullet>X) \<mapsto> (pi\<bullet>T')]\<^sub>\<tau>" 425 by (nominal_induct T avoiding: X T' rule: ty.strong_induct) 426 (perm_simp add: fresh_left)+ 427 428lemma type_subst_fresh: 429 fixes X::"tyvrs" 430 assumes "X\<sharp>T" and "X\<sharp>P" 431 shows "X\<sharp>T[Y \<mapsto> P]\<^sub>\<tau>" 432using assms 433by (nominal_induct T avoiding: X Y P rule:ty.strong_induct) 434 (auto simp add: abs_fresh) 435 436lemma fresh_type_subst_fresh: 437 assumes "X\<sharp>T'" 438 shows "X\<sharp>T[X \<mapsto> T']\<^sub>\<tau>" 439using assms 440by (nominal_induct T avoiding: X T' rule: ty.strong_induct) 441 (auto simp add: fresh_atm abs_fresh fresh_nat) 442 443lemma type_subst_identity: 444 "X\<sharp>T \<Longrightarrow> T[X \<mapsto> U]\<^sub>\<tau> = T" 445 by (nominal_induct T avoiding: X U rule: ty.strong_induct) 446 (simp_all add: fresh_atm abs_fresh) 447 448lemma type_substitution_lemma: 449 "X \<noteq> Y \<Longrightarrow> X\<sharp>L \<Longrightarrow> M[X \<mapsto> N]\<^sub>\<tau>[Y \<mapsto> L]\<^sub>\<tau> = M[Y \<mapsto> L]\<^sub>\<tau>[X \<mapsto> N[Y \<mapsto> L]\<^sub>\<tau>]\<^sub>\<tau>" 450 by (nominal_induct M avoiding: X Y N L rule: ty.strong_induct) 451 (auto simp add: type_subst_fresh type_subst_identity) 452 453lemma type_subst_rename: 454 "Y\<sharp>T \<Longrightarrow> ([(Y,X)]\<bullet>T)[Y \<mapsto> U]\<^sub>\<tau> = T[X \<mapsto> U]\<^sub>\<tau>" 455 by (nominal_induct T avoiding: X Y U rule: ty.strong_induct) 456 (simp_all add: fresh_atm calc_atm abs_fresh fresh_aux) 457 458nominal_primrec 459 subst_tyb :: "binding \<Rightarrow> tyvrs \<Rightarrow> ty \<Rightarrow> binding" ("_[_ \<mapsto> _]\<^sub>b" [100,100,100] 100) 460where 461 "(TVarB X U)[Y \<mapsto> T]\<^sub>b = TVarB X (U[Y \<mapsto> T]\<^sub>\<tau>)" 462| "(VarB X U)[Y \<mapsto> T]\<^sub>b = VarB X (U[Y \<mapsto> T]\<^sub>\<tau>)" 463by auto 464 465lemma binding_subst_fresh: 466 fixes X::"tyvrs" 467 assumes "X\<sharp>a" 468 and "X\<sharp>P" 469 shows "X\<sharp>a[Y \<mapsto> P]\<^sub>b" 470using assms 471by (nominal_induct a rule: binding.strong_induct) 472 (auto simp add: type_subst_fresh) 473 474lemma binding_subst_identity: 475 shows "X\<sharp>B \<Longrightarrow> B[X \<mapsto> U]\<^sub>b = B" 476by (induct B rule: binding.induct) 477 (simp_all add: fresh_atm type_subst_identity) 478 479primrec subst_tyc :: "env \<Rightarrow> tyvrs \<Rightarrow> ty \<Rightarrow> env" ("_[_ \<mapsto> _]\<^sub>e" [100,100,100] 100) where 480 "([])[Y \<mapsto> T]\<^sub>e= []" 481| "(B#\<Gamma>)[Y \<mapsto> T]\<^sub>e = (B[Y \<mapsto> T]\<^sub>b)#(\<Gamma>[Y \<mapsto> T]\<^sub>e)" 482 483lemma ctxt_subst_fresh': 484 fixes X::"tyvrs" 485 assumes "X\<sharp>\<Gamma>" 486 and "X\<sharp>P" 487 shows "X\<sharp>\<Gamma>[Y \<mapsto> P]\<^sub>e" 488using assms 489by (induct \<Gamma>) 490 (auto simp add: fresh_list_cons binding_subst_fresh) 491 492lemma ctxt_subst_mem_TVarB: "TVarB X T \<in> set \<Gamma> \<Longrightarrow> TVarB X (T[Y \<mapsto> U]\<^sub>\<tau>) \<in> set (\<Gamma>[Y \<mapsto> U]\<^sub>e)" 493 by (induct \<Gamma>) auto 494 495lemma ctxt_subst_mem_VarB: "VarB x T \<in> set \<Gamma> \<Longrightarrow> VarB x (T[Y \<mapsto> U]\<^sub>\<tau>) \<in> set (\<Gamma>[Y \<mapsto> U]\<^sub>e)" 496 by (induct \<Gamma>) auto 497 498lemma ctxt_subst_identity: "X\<sharp>\<Gamma> \<Longrightarrow> \<Gamma>[X \<mapsto> U]\<^sub>e = \<Gamma>" 499 by (induct \<Gamma>) (simp_all add: fresh_list_cons binding_subst_identity) 500 501lemma ctxt_subst_append: "(\<Delta> @ \<Gamma>)[X \<mapsto> T]\<^sub>e = \<Delta>[X \<mapsto> T]\<^sub>e @ \<Gamma>[X \<mapsto> T]\<^sub>e" 502 by (induct \<Delta>) simp_all 503 504nominal_primrec 505 subst_trm :: "trm \<Rightarrow> vrs \<Rightarrow> trm \<Rightarrow> trm" ("_[_ \<mapsto> _]" [300, 0, 0] 300) 506where 507 "(Var x)[y \<mapsto> t'] = (if x=y then t' else (Var x))" 508| "(t1 \<cdot> t2)[y \<mapsto> t'] = t1[y \<mapsto> t'] \<cdot> t2[y \<mapsto> t']" 509| "(t \<cdot>\<^sub>\<tau> T)[y \<mapsto> t'] = t[y \<mapsto> t'] \<cdot>\<^sub>\<tau> T" 510| "X\<sharp>(T,t') \<Longrightarrow> (\<lambda>X<:T. t)[y \<mapsto> t'] = (\<lambda>X<:T. t[y \<mapsto> t'])" 511| "x\<sharp>(y,t') \<Longrightarrow> (\<lambda>x:T. t)[y \<mapsto> t'] = (\<lambda>x:T. t[y \<mapsto> t'])" 512apply(finite_guess)+ 513apply(rule TrueI)+ 514apply(simp add: abs_fresh)+ 515apply(fresh_guess add: ty_vrs_fresh abs_fresh)+ 516done 517 518lemma subst_trm_fresh_tyvar: 519 fixes X::"tyvrs" 520 shows "X\<sharp>t \<Longrightarrow> X\<sharp>u \<Longrightarrow> X\<sharp>t[x \<mapsto> u]" 521 by (nominal_induct t avoiding: x u rule: trm.strong_induct) 522 (auto simp add: trm.fresh abs_fresh) 523 524lemma subst_trm_fresh_var: 525 "x\<sharp>u \<Longrightarrow> x\<sharp>t[x \<mapsto> u]" 526 by (nominal_induct t avoiding: x u rule: trm.strong_induct) 527 (simp_all add: abs_fresh fresh_atm ty_vrs_fresh) 528 529lemma subst_trm_eqvt[eqvt]: 530 fixes pi::"tyvrs prm" 531 and t::"trm" 532 shows "pi\<bullet>(t[x \<mapsto> u]) = (pi\<bullet>t)[(pi\<bullet>x) \<mapsto> (pi\<bullet>u)]" 533 by (nominal_induct t avoiding: x u rule: trm.strong_induct) 534 (perm_simp add: fresh_left)+ 535 536lemma subst_trm_eqvt'[eqvt]: 537 fixes pi::"vrs prm" 538 and t::"trm" 539 shows "pi\<bullet>(t[x \<mapsto> u]) = (pi\<bullet>t)[(pi\<bullet>x) \<mapsto> (pi\<bullet>u)]" 540 by (nominal_induct t avoiding: x u rule: trm.strong_induct) 541 (perm_simp add: fresh_left)+ 542 543lemma subst_trm_rename: 544 "y\<sharp>t \<Longrightarrow> ([(y, x)] \<bullet> t)[y \<mapsto> u] = t[x \<mapsto> u]" 545 by (nominal_induct t avoiding: x y u rule: trm.strong_induct) 546 (simp_all add: fresh_atm calc_atm abs_fresh fresh_aux ty_vrs_fresh perm_fresh_fresh) 547 548nominal_primrec (freshness_context: "T2::ty") 549 subst_trm_ty :: "trm \<Rightarrow> tyvrs \<Rightarrow> ty \<Rightarrow> trm" ("_[_ \<mapsto>\<^sub>\<tau> _]" [300, 0, 0] 300) 550where 551 "(Var x)[Y \<mapsto>\<^sub>\<tau> T2] = Var x" 552| "(t1 \<cdot> t2)[Y \<mapsto>\<^sub>\<tau> T2] = t1[Y \<mapsto>\<^sub>\<tau> T2] \<cdot> t2[Y \<mapsto>\<^sub>\<tau> T2]" 553| "(t1 \<cdot>\<^sub>\<tau> T)[Y \<mapsto>\<^sub>\<tau> T2] = t1[Y \<mapsto>\<^sub>\<tau> T2] \<cdot>\<^sub>\<tau> T[Y \<mapsto> T2]\<^sub>\<tau>" 554| "X\<sharp>(Y,T,T2) \<Longrightarrow> (\<lambda>X<:T. t)[Y \<mapsto>\<^sub>\<tau> T2] = (\<lambda>X<:T[Y \<mapsto> T2]\<^sub>\<tau>. t[Y \<mapsto>\<^sub>\<tau> T2])" 555| "(\<lambda>x:T. t)[Y \<mapsto>\<^sub>\<tau> T2] = (\<lambda>x:T[Y \<mapsto> T2]\<^sub>\<tau>. t[Y \<mapsto>\<^sub>\<tau> T2])" 556apply(finite_guess)+ 557apply(rule TrueI)+ 558apply(simp add: abs_fresh ty_vrs_fresh)+ 559apply(simp add: type_subst_fresh) 560apply(fresh_guess add: ty_vrs_fresh abs_fresh)+ 561done 562 563lemma subst_trm_ty_fresh: 564 fixes X::"tyvrs" 565 shows "X\<sharp>t \<Longrightarrow> X\<sharp>T \<Longrightarrow> X\<sharp>t[Y \<mapsto>\<^sub>\<tau> T]" 566 by (nominal_induct t avoiding: Y T rule: trm.strong_induct) 567 (auto simp add: abs_fresh type_subst_fresh) 568 569lemma subst_trm_ty_fresh': 570 "X\<sharp>T \<Longrightarrow> X\<sharp>t[X \<mapsto>\<^sub>\<tau> T]" 571 by (nominal_induct t avoiding: X T rule: trm.strong_induct) 572 (simp_all add: abs_fresh fresh_type_subst_fresh fresh_atm) 573 574lemma subst_trm_ty_eqvt[eqvt]: 575 fixes pi::"tyvrs prm" 576 and t::"trm" 577 shows "pi\<bullet>(t[X \<mapsto>\<^sub>\<tau> T]) = (pi\<bullet>t)[(pi\<bullet>X) \<mapsto>\<^sub>\<tau> (pi\<bullet>T)]" 578 by (nominal_induct t avoiding: X T rule: trm.strong_induct) 579 (perm_simp add: fresh_bij subst_eqvt)+ 580 581lemma subst_trm_ty_eqvt'[eqvt]: 582 fixes pi::"vrs prm" 583 and t::"trm" 584 shows "pi\<bullet>(t[X \<mapsto>\<^sub>\<tau> T]) = (pi\<bullet>t)[(pi\<bullet>X) \<mapsto>\<^sub>\<tau> (pi\<bullet>T)]" 585 by (nominal_induct t avoiding: X T rule: trm.strong_induct) 586 (perm_simp add: fresh_left subst_eqvt')+ 587 588lemma subst_trm_ty_rename: 589 "Y\<sharp>t \<Longrightarrow> ([(Y, X)] \<bullet> t)[Y \<mapsto>\<^sub>\<tau> U] = t[X \<mapsto>\<^sub>\<tau> U]" 590 by (nominal_induct t avoiding: X Y U rule: trm.strong_induct) 591 (simp_all add: fresh_atm calc_atm abs_fresh fresh_aux type_subst_rename) 592 593section \<open>Subtyping-Relation\<close> 594 595text \<open>The definition for the subtyping-relation follows quite closely what is written 596 in the POPLmark-paper, except for the premises dealing with well-formed contexts and 597 the freshness constraint \<^term>\<open>X\<sharp>\<Gamma>\<close> in the \<open>S_Forall\<close>-rule. (The freshness 598 constraint is specific to the \emph{nominal approach}. Note, however, that the constraint 599 does \emph{not} make the subtyping-relation ``partial"\ldots because we work over 600 $\alpha$-equivalence classes.)\<close> 601 602inductive 603 subtype_of :: "env \<Rightarrow> ty \<Rightarrow> ty \<Rightarrow> bool" ("_\<turnstile>_<:_" [100,100,100] 100) 604where 605 SA_Top[intro]: "\<lbrakk>\<turnstile> \<Gamma> ok; S closed_in \<Gamma>\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> S <: Top" 606| SA_refl_TVar[intro]: "\<lbrakk>\<turnstile> \<Gamma> ok; X \<in> ty_dom \<Gamma>\<rbrakk>\<Longrightarrow> \<Gamma> \<turnstile> Tvar X <: Tvar X" 607| SA_trans_TVar[intro]: "\<lbrakk>(TVarB X S) \<in> set \<Gamma>; \<Gamma> \<turnstile> S <: T\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> (Tvar X) <: T" 608| SA_arrow[intro]: "\<lbrakk>\<Gamma> \<turnstile> T\<^sub>1 <: S\<^sub>1; \<Gamma> \<turnstile> S\<^sub>2 <: T\<^sub>2\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> (S\<^sub>1 \<rightarrow> S\<^sub>2) <: (T\<^sub>1 \<rightarrow> T\<^sub>2)" 609| SA_all[intro]: "\<lbrakk>\<Gamma> \<turnstile> T\<^sub>1 <: S\<^sub>1; ((TVarB X T\<^sub>1)#\<Gamma>) \<turnstile> S\<^sub>2 <: T\<^sub>2\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> (\<forall>X<:S\<^sub>1. S\<^sub>2) <: (\<forall>X<:T\<^sub>1. T\<^sub>2)" 610 611lemma subtype_implies_ok: 612 fixes X::"tyvrs" 613 assumes a: "\<Gamma> \<turnstile> S <: T" 614 shows "\<turnstile> \<Gamma> ok" 615using a by (induct) (auto) 616 617lemma subtype_implies_closed: 618 assumes a: "\<Gamma> \<turnstile> S <: T" 619 shows "S closed_in \<Gamma> \<and> T closed_in \<Gamma>" 620using a 621proof (induct) 622 case (SA_Top \<Gamma> S) 623 have "Top closed_in \<Gamma>" by (simp add: closed_in_def ty.supp) 624 moreover 625 have "S closed_in \<Gamma>" by fact 626 ultimately show "S closed_in \<Gamma> \<and> Top closed_in \<Gamma>" by simp 627next 628 case (SA_trans_TVar X S \<Gamma> T) 629 have "(TVarB X S)\<in>set \<Gamma>" by fact 630 hence "X \<in> ty_dom \<Gamma>" by (rule ty_dom_inclusion) 631 hence "(Tvar X) closed_in \<Gamma>" by (simp add: closed_in_def ty.supp supp_atm) 632 moreover 633 have "S closed_in \<Gamma> \<and> T closed_in \<Gamma>" by fact 634 hence "T closed_in \<Gamma>" by force 635 ultimately show "(Tvar X) closed_in \<Gamma> \<and> T closed_in \<Gamma>" by simp 636qed (auto simp add: closed_in_def ty.supp supp_atm abs_supp) 637 638lemma subtype_implies_fresh: 639 fixes X::"tyvrs" 640 assumes a1: "\<Gamma> \<turnstile> S <: T" 641 and a2: "X\<sharp>\<Gamma>" 642 shows "X\<sharp>S \<and> X\<sharp>T" 643proof - 644 from a1 have "\<turnstile> \<Gamma> ok" by (rule subtype_implies_ok) 645 with a2 have "X\<sharp>ty_dom(\<Gamma>)" by (simp add: fresh_dom) 646 moreover 647 from a1 have "S closed_in \<Gamma> \<and> T closed_in \<Gamma>" by (rule subtype_implies_closed) 648 hence "supp S \<subseteq> ((supp (ty_dom \<Gamma>))::tyvrs set)" 649 and "supp T \<subseteq> ((supp (ty_dom \<Gamma>))::tyvrs set)" by (simp_all add: ty_dom_supp closed_in_def) 650 ultimately show "X\<sharp>S \<and> X\<sharp>T" by (force simp add: supp_prod fresh_def) 651qed 652 653lemma valid_ty_dom_fresh: 654 fixes X::"tyvrs" 655 assumes valid: "\<turnstile> \<Gamma> ok" 656 shows "X\<sharp>(ty_dom \<Gamma>) = X\<sharp>\<Gamma>" 657 using valid 658 apply induct 659 apply (simp add: fresh_list_nil fresh_set_empty) 660 apply (simp_all add: binding.fresh fresh_list_cons 661 fresh_fin_insert [OF pt_tyvrs_inst at_tyvrs_inst fs_tyvrs_inst] finite_doms fresh_atm) 662 apply (auto simp add: closed_in_fresh) 663 done 664 665equivariance subtype_of 666 667nominal_inductive subtype_of 668 apply (simp_all add: abs_fresh) 669 apply (fastforce simp add: valid_ty_dom_fresh dest: subtype_implies_ok) 670 apply (force simp add: closed_in_fresh dest: subtype_implies_closed subtype_implies_ok)+ 671 done 672 673section \<open>Reflexivity of Subtyping\<close> 674 675lemma subtype_reflexivity: 676 assumes a: "\<turnstile> \<Gamma> ok" 677 and b: "T closed_in \<Gamma>" 678 shows "\<Gamma> \<turnstile> T <: T" 679using a b 680proof(nominal_induct T avoiding: \<Gamma> rule: ty.strong_induct) 681 case (Forall X T\<^sub>1 T\<^sub>2) 682 have ih_T\<^sub>1: "\<And>\<Gamma>. \<lbrakk>\<turnstile> \<Gamma> ok; T\<^sub>1 closed_in \<Gamma>\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> T\<^sub>1 <: T\<^sub>1" by fact 683 have ih_T\<^sub>2: "\<And>\<Gamma>. \<lbrakk>\<turnstile> \<Gamma> ok; T\<^sub>2 closed_in \<Gamma>\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> T\<^sub>2 <: T\<^sub>2" by fact 684 have fresh_cond: "X\<sharp>\<Gamma>" by fact 685 hence fresh_ty_dom: "X\<sharp>(ty_dom \<Gamma>)" by (simp add: fresh_dom) 686 have "(\<forall>X<:T\<^sub>2. T\<^sub>1) closed_in \<Gamma>" by fact 687 hence closed\<^sub>T2: "T\<^sub>2 closed_in \<Gamma>" and closed\<^sub>T1: "T\<^sub>1 closed_in ((TVarB X T\<^sub>2)#\<Gamma>)" 688 by (auto simp add: closed_in_def ty.supp abs_supp) 689 have ok: "\<turnstile> \<Gamma> ok" by fact 690 hence ok': "\<turnstile> ((TVarB X T\<^sub>2)#\<Gamma>) ok" using closed\<^sub>T2 fresh_ty_dom by simp 691 have "\<Gamma> \<turnstile> T\<^sub>2 <: T\<^sub>2" using ih_T\<^sub>2 closed\<^sub>T2 ok by simp 692 moreover 693 have "((TVarB X T\<^sub>2)#\<Gamma>) \<turnstile> T\<^sub>1 <: T\<^sub>1" using ih_T\<^sub>1 closed\<^sub>T1 ok' by simp 694 ultimately show "\<Gamma> \<turnstile> (\<forall>X<:T\<^sub>2. T\<^sub>1) <: (\<forall>X<:T\<^sub>2. T\<^sub>1)" using fresh_cond 695 by (simp add: subtype_of.SA_all) 696qed (auto simp add: closed_in_def ty.supp supp_atm) 697 698lemma subtype_reflexivity_semiautomated: 699 assumes a: "\<turnstile> \<Gamma> ok" 700 and b: "T closed_in \<Gamma>" 701 shows "\<Gamma> \<turnstile> T <: T" 702using a b 703apply(nominal_induct T avoiding: \<Gamma> rule: ty.strong_induct) 704apply(auto simp add: ty.supp abs_supp supp_atm closed_in_def) 705 \<comment> \<open>Too bad that this instantiation cannot be found automatically by 706 \isakeyword{auto}; \isakeyword{blast} would find it if we had not used 707 an explicit definition for \<open>closed_in_def\<close>.\<close> 708apply(drule_tac x="(TVarB tyvrs ty2)#\<Gamma>" in meta_spec) 709apply(force dest: fresh_dom simp add: closed_in_def) 710done 711 712section \<open>Weakening\<close> 713 714text \<open>In order to prove weakening we introduce the notion of a type-context extending 715 another. This generalization seems to make the proof for weakening to be 716 smoother than if we had strictly adhered to the version in the POPLmark-paper.\<close> 717 718definition extends :: "env \<Rightarrow> env \<Rightarrow> bool" ("_ extends _" [100,100] 100) where 719 "\<Delta> extends \<Gamma> \<equiv> \<forall>X Q. (TVarB X Q)\<in>set \<Gamma> \<longrightarrow> (TVarB X Q)\<in>set \<Delta>" 720 721lemma extends_ty_dom: 722 assumes a: "\<Delta> extends \<Gamma>" 723 shows "ty_dom \<Gamma> \<subseteq> ty_dom \<Delta>" 724 using a 725 apply (auto simp add: extends_def) 726 apply (drule ty_dom_existence) 727 apply (force simp add: ty_dom_inclusion) 728 done 729 730lemma extends_closed: 731 assumes a1: "T closed_in \<Gamma>" 732 and a2: "\<Delta> extends \<Gamma>" 733 shows "T closed_in \<Delta>" 734 using a1 a2 735 by (auto dest: extends_ty_dom simp add: closed_in_def) 736 737lemma extends_memb: 738 assumes a: "\<Delta> extends \<Gamma>" 739 and b: "(TVarB X T) \<in> set \<Gamma>" 740 shows "(TVarB X T) \<in> set \<Delta>" 741 using a b by (simp add: extends_def) 742 743lemma weakening: 744 assumes a: "\<Gamma> \<turnstile> S <: T" 745 and b: "\<turnstile> \<Delta> ok" 746 and c: "\<Delta> extends \<Gamma>" 747 shows "\<Delta> \<turnstile> S <: T" 748 using a b c 749proof (nominal_induct \<Gamma> S T avoiding: \<Delta> rule: subtype_of.strong_induct) 750 case (SA_Top \<Gamma> S) 751 have lh_drv_prem: "S closed_in \<Gamma>" by fact 752 have "\<turnstile> \<Delta> ok" by fact 753 moreover 754 have "\<Delta> extends \<Gamma>" by fact 755 hence "S closed_in \<Delta>" using lh_drv_prem by (simp only: extends_closed) 756 ultimately show "\<Delta> \<turnstile> S <: Top" by force 757next 758 case (SA_trans_TVar X S \<Gamma> T) 759 have lh_drv_prem: "(TVarB X S) \<in> set \<Gamma>" by fact 760 have ih: "\<And>\<Delta>. \<turnstile> \<Delta> ok \<Longrightarrow> \<Delta> extends \<Gamma> \<Longrightarrow> \<Delta> \<turnstile> S <: T" by fact 761 have ok: "\<turnstile> \<Delta> ok" by fact 762 have extends: "\<Delta> extends \<Gamma>" by fact 763 have "(TVarB X S) \<in> set \<Delta>" using lh_drv_prem extends by (simp only: extends_memb) 764 moreover 765 have "\<Delta> \<turnstile> S <: T" using ok extends ih by simp 766 ultimately show "\<Delta> \<turnstile> Tvar X <: T" using ok by force 767next 768 case (SA_refl_TVar \<Gamma> X) 769 have lh_drv_prem: "X \<in> ty_dom \<Gamma>" by fact 770 have "\<turnstile> \<Delta> ok" by fact 771 moreover 772 have "\<Delta> extends \<Gamma>" by fact 773 hence "X \<in> ty_dom \<Delta>" using lh_drv_prem by (force dest: extends_ty_dom) 774 ultimately show "\<Delta> \<turnstile> Tvar X <: Tvar X" by force 775next 776 case (SA_arrow \<Gamma> T\<^sub>1 S\<^sub>1 S\<^sub>2 T\<^sub>2) thus "\<Delta> \<turnstile> S\<^sub>1 \<rightarrow> S\<^sub>2 <: T\<^sub>1 \<rightarrow> T\<^sub>2" by blast 777next 778 case (SA_all \<Gamma> T\<^sub>1 S\<^sub>1 X S\<^sub>2 T\<^sub>2) 779 have fresh_cond: "X\<sharp>\<Delta>" by fact 780 hence fresh_dom: "X\<sharp>(ty_dom \<Delta>)" by (simp add: fresh_dom) 781 have ih\<^sub>1: "\<And>\<Delta>. \<turnstile> \<Delta> ok \<Longrightarrow> \<Delta> extends \<Gamma> \<Longrightarrow> \<Delta> \<turnstile> T\<^sub>1 <: S\<^sub>1" by fact 782 have ih\<^sub>2: "\<And>\<Delta>. \<turnstile> \<Delta> ok \<Longrightarrow> \<Delta> extends ((TVarB X T\<^sub>1)#\<Gamma>) \<Longrightarrow> \<Delta> \<turnstile> S\<^sub>2 <: T\<^sub>2" by fact 783 have lh_drv_prem: "\<Gamma> \<turnstile> T\<^sub>1 <: S\<^sub>1" by fact 784 hence closed\<^sub>T1: "T\<^sub>1 closed_in \<Gamma>" by (simp add: subtype_implies_closed) 785 have ok: "\<turnstile> \<Delta> ok" by fact 786 have ext: "\<Delta> extends \<Gamma>" by fact 787 have "T\<^sub>1 closed_in \<Delta>" using ext closed\<^sub>T1 by (simp only: extends_closed) 788 hence "\<turnstile> ((TVarB X T\<^sub>1)#\<Delta>) ok" using fresh_dom ok by force 789 moreover 790 have "((TVarB X T\<^sub>1)#\<Delta>) extends ((TVarB X T\<^sub>1)#\<Gamma>)" using ext by (force simp add: extends_def) 791 ultimately have "((TVarB X T\<^sub>1)#\<Delta>) \<turnstile> S\<^sub>2 <: T\<^sub>2" using ih\<^sub>2 by simp 792 moreover 793 have "\<Delta> \<turnstile> T\<^sub>1 <: S\<^sub>1" using ok ext ih\<^sub>1 by simp 794 ultimately show "\<Delta> \<turnstile> (\<forall>X<:S\<^sub>1. S\<^sub>2) <: (\<forall>X<:T\<^sub>1. T\<^sub>2)" using ok by (force intro: SA_all) 795qed 796 797text \<open>In fact all ``non-binding" cases can be solved automatically:\<close> 798 799lemma weakening_more_automated: 800 assumes a: "\<Gamma> \<turnstile> S <: T" 801 and b: "\<turnstile> \<Delta> ok" 802 and c: "\<Delta> extends \<Gamma>" 803 shows "\<Delta> \<turnstile> S <: T" 804 using a b c 805proof (nominal_induct \<Gamma> S T avoiding: \<Delta> rule: subtype_of.strong_induct) 806 case (SA_all \<Gamma> T\<^sub>1 S\<^sub>1 X S\<^sub>2 T\<^sub>2) 807 have fresh_cond: "X\<sharp>\<Delta>" by fact 808 hence fresh_dom: "X\<sharp>(ty_dom \<Delta>)" by (simp add: fresh_dom) 809 have ih\<^sub>1: "\<And>\<Delta>. \<turnstile> \<Delta> ok \<Longrightarrow> \<Delta> extends \<Gamma> \<Longrightarrow> \<Delta> \<turnstile> T\<^sub>1 <: S\<^sub>1" by fact 810 have ih\<^sub>2: "\<And>\<Delta>. \<turnstile> \<Delta> ok \<Longrightarrow> \<Delta> extends ((TVarB X T\<^sub>1)#\<Gamma>) \<Longrightarrow> \<Delta> \<turnstile> S\<^sub>2 <: T\<^sub>2" by fact 811 have lh_drv_prem: "\<Gamma> \<turnstile> T\<^sub>1 <: S\<^sub>1" by fact 812 hence closed\<^sub>T1: "T\<^sub>1 closed_in \<Gamma>" by (simp add: subtype_implies_closed) 813 have ok: "\<turnstile> \<Delta> ok" by fact 814 have ext: "\<Delta> extends \<Gamma>" by fact 815 have "T\<^sub>1 closed_in \<Delta>" using ext closed\<^sub>T1 by (simp only: extends_closed) 816 hence "\<turnstile> ((TVarB X T\<^sub>1)#\<Delta>) ok" using fresh_dom ok by force 817 moreover 818 have "((TVarB X T\<^sub>1)#\<Delta>) extends ((TVarB X T\<^sub>1)#\<Gamma>)" using ext by (force simp add: extends_def) 819 ultimately have "((TVarB X T\<^sub>1)#\<Delta>) \<turnstile> S\<^sub>2 <: T\<^sub>2" using ih\<^sub>2 by simp 820 moreover 821 have "\<Delta> \<turnstile> T\<^sub>1 <: S\<^sub>1" using ok ext ih\<^sub>1 by simp 822 ultimately show "\<Delta> \<turnstile> (\<forall>X<:S\<^sub>1. S\<^sub>2) <: (\<forall>X<:T\<^sub>1. T\<^sub>2)" using ok by (force intro: SA_all) 823qed (blast intro: extends_closed extends_memb dest: extends_ty_dom)+ 824 825section \<open>Transitivity and Narrowing\<close> 826 827text \<open>Some inversion lemmas that are needed in the transitivity and narrowing proof.\<close> 828 829declare ty.inject [simp add] 830 831inductive_cases S_TopE: "\<Gamma> \<turnstile> Top <: T" 832inductive_cases S_ArrowE_left: "\<Gamma> \<turnstile> S\<^sub>1 \<rightarrow> S\<^sub>2 <: T" 833 834declare ty.inject [simp del] 835 836lemma S_ForallE_left: 837 shows "\<lbrakk>\<Gamma> \<turnstile> (\<forall>X<:S\<^sub>1. S\<^sub>2) <: T; X\<sharp>\<Gamma>; X\<sharp>S\<^sub>1; X\<sharp>T\<rbrakk> 838 \<Longrightarrow> T = Top \<or> (\<exists>T\<^sub>1 T\<^sub>2. T = (\<forall>X<:T\<^sub>1. T\<^sub>2) \<and> \<Gamma> \<turnstile> T\<^sub>1 <: S\<^sub>1 \<and> ((TVarB X T\<^sub>1)#\<Gamma>) \<turnstile> S\<^sub>2 <: T\<^sub>2)" 839apply(erule subtype_of.strong_cases[where X="X"]) 840apply(auto simp add: abs_fresh ty.inject alpha) 841done 842 843text \<open>Next we prove the transitivity and narrowing for the subtyping-relation. 844The POPLmark-paper says the following: 845 846\begin{quote} 847\begin{lemma}[Transitivity and Narrowing] \ 848\begin{enumerate} 849\item If \<^term>\<open>\<Gamma> \<turnstile> S<:Q\<close> and \<^term>\<open>\<Gamma> \<turnstile> Q<:T\<close>, then \<^term>\<open>\<Gamma> \<turnstile> S<:T\<close>. 850\item If \<open>\<Gamma>,X<:Q,\<Delta> \<turnstile> M<:N\<close> and \<^term>\<open>\<Gamma> \<turnstile> P<:Q\<close> then \<open>\<Gamma>,X<:P,\<Delta> \<turnstile> M<:N\<close>. 851\end{enumerate} 852\end{lemma} 853 854The two parts are proved simultaneously, by induction on the size 855of \<^term>\<open>Q\<close>. The argument for part (2) assumes that part (1) has 856been established already for the \<^term>\<open>Q\<close> in question; part (1) uses 857part (2) only for strictly smaller \<^term>\<open>Q\<close>. 858\end{quote} 859 860For the induction on the size of \<^term>\<open>Q\<close>, we use the induction-rule 861\<open>measure_induct_rule\<close>: 862 863\begin{center} 864@{thm measure_induct_rule[of "size_ty",no_vars]} 865\end{center} 866 867That means in order to show a property \<^term>\<open>P a\<close> for all \<^term>\<open>a\<close>, 868the induct-rule requires to prove that for all \<^term>\<open>x\<close> \<^term>\<open>P x\<close> holds using the 869assumption that for all \<^term>\<open>y\<close> whose size is strictly smaller than 870that of \<^term>\<open>x\<close> the property \<^term>\<open>P y\<close> holds.\<close> 871 872lemma 873 shows subtype_transitivity: "\<Gamma>\<turnstile>S<:Q \<Longrightarrow> \<Gamma>\<turnstile>Q<:T \<Longrightarrow> \<Gamma>\<turnstile>S<:T" 874 and subtype_narrow: "(\<Delta>@[(TVarB X Q)]@\<Gamma>)\<turnstile>M<:N \<Longrightarrow> \<Gamma>\<turnstile>P<:Q \<Longrightarrow> (\<Delta>@[(TVarB X P)]@\<Gamma>)\<turnstile>M<:N" 875proof (induct Q arbitrary: \<Gamma> S T \<Delta> X P M N taking: "size_ty" rule: measure_induct_rule) 876 case (less Q) 877 have IH_trans: 878 "\<And>Q' \<Gamma> S T. \<lbrakk>size_ty Q' < size_ty Q; \<Gamma>\<turnstile>S<:Q'; \<Gamma>\<turnstile>Q'<:T\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>S<:T" by fact 879 have IH_narrow: 880 "\<And>Q' \<Delta> \<Gamma> X M N P. \<lbrakk>size_ty Q' < size_ty Q; (\<Delta>@[(TVarB X Q')]@\<Gamma>)\<turnstile>M<:N; \<Gamma>\<turnstile>P<:Q'\<rbrakk> 881 \<Longrightarrow> (\<Delta>@[(TVarB X P)]@\<Gamma>)\<turnstile>M<:N" by fact 882 883 { fix \<Gamma> S T 884 have "\<lbrakk>\<Gamma> \<turnstile> S <: Q; \<Gamma> \<turnstile> Q <: T\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> S <: T" 885 proof (induct \<Gamma> S Q\<equiv>Q rule: subtype_of.induct) 886 case (SA_Top \<Gamma> S) 887 then have rh_drv: "\<Gamma> \<turnstile> Top <: T" by simp 888 then have T_inst: "T = Top" by (auto elim: S_TopE) 889 from \<open>\<turnstile> \<Gamma> ok\<close> and \<open>S closed_in \<Gamma>\<close> 890 have "\<Gamma> \<turnstile> S <: Top" by auto 891 then show "\<Gamma> \<turnstile> S <: T" using T_inst by simp 892 next 893 case (SA_trans_TVar Y U \<Gamma>) 894 then have IH_inner: "\<Gamma> \<turnstile> U <: T" by simp 895 have "(TVarB Y U) \<in> set \<Gamma>" by fact 896 with IH_inner show "\<Gamma> \<turnstile> Tvar Y <: T" by auto 897 next 898 case (SA_refl_TVar \<Gamma> X) 899 then show "\<Gamma> \<turnstile> Tvar X <: T" by simp 900 next 901 case (SA_arrow \<Gamma> Q\<^sub>1 S\<^sub>1 S\<^sub>2 Q\<^sub>2) 902 then have rh_drv: "\<Gamma> \<turnstile> Q\<^sub>1 \<rightarrow> Q\<^sub>2 <: T" by simp 903 from \<open>Q\<^sub>1 \<rightarrow> Q\<^sub>2 = Q\<close> 904 have Q\<^sub>12_less: "size_ty Q\<^sub>1 < size_ty Q" "size_ty Q\<^sub>2 < size_ty Q" by auto 905 have lh_drv_prm\<^sub>1: "\<Gamma> \<turnstile> Q\<^sub>1 <: S\<^sub>1" by fact 906 have lh_drv_prm\<^sub>2: "\<Gamma> \<turnstile> S\<^sub>2 <: Q\<^sub>2" by fact 907 from rh_drv have "T=Top \<or> (\<exists>T\<^sub>1 T\<^sub>2. T=T\<^sub>1\<rightarrow>T\<^sub>2 \<and> \<Gamma>\<turnstile>T\<^sub>1<:Q\<^sub>1 \<and> \<Gamma>\<turnstile>Q\<^sub>2<:T\<^sub>2)" 908 by (auto elim: S_ArrowE_left) 909 moreover 910 have "S\<^sub>1 closed_in \<Gamma>" and "S\<^sub>2 closed_in \<Gamma>" 911 using lh_drv_prm\<^sub>1 lh_drv_prm\<^sub>2 by (simp_all add: subtype_implies_closed) 912 hence "(S\<^sub>1 \<rightarrow> S\<^sub>2) closed_in \<Gamma>" by (simp add: closed_in_def ty.supp) 913 moreover 914 have "\<turnstile> \<Gamma> ok" using rh_drv by (rule subtype_implies_ok) 915 moreover 916 { assume "\<exists>T\<^sub>1 T\<^sub>2. T = T\<^sub>1\<rightarrow>T\<^sub>2 \<and> \<Gamma> \<turnstile> T\<^sub>1 <: Q\<^sub>1 \<and> \<Gamma> \<turnstile> Q\<^sub>2 <: T\<^sub>2" 917 then obtain T\<^sub>1 T\<^sub>2 918 where T_inst: "T = T\<^sub>1 \<rightarrow> T\<^sub>2" 919 and rh_drv_prm\<^sub>1: "\<Gamma> \<turnstile> T\<^sub>1 <: Q\<^sub>1" 920 and rh_drv_prm\<^sub>2: "\<Gamma> \<turnstile> Q\<^sub>2 <: T\<^sub>2" by force 921 from IH_trans[of "Q\<^sub>1"] 922 have "\<Gamma> \<turnstile> T\<^sub>1 <: S\<^sub>1" using Q\<^sub>12_less rh_drv_prm\<^sub>1 lh_drv_prm\<^sub>1 by simp 923 moreover 924 from IH_trans[of "Q\<^sub>2"] 925 have "\<Gamma> \<turnstile> S\<^sub>2 <: T\<^sub>2" using Q\<^sub>12_less rh_drv_prm\<^sub>2 lh_drv_prm\<^sub>2 by simp 926 ultimately have "\<Gamma> \<turnstile> S\<^sub>1 \<rightarrow> S\<^sub>2 <: T\<^sub>1 \<rightarrow> T\<^sub>2" by auto 927 then have "\<Gamma> \<turnstile> S\<^sub>1 \<rightarrow> S\<^sub>2 <: T" using T_inst by simp 928 } 929 ultimately show "\<Gamma> \<turnstile> S\<^sub>1 \<rightarrow> S\<^sub>2 <: T" by blast 930 next 931 case (SA_all \<Gamma> Q\<^sub>1 S\<^sub>1 X S\<^sub>2 Q\<^sub>2) 932 then have rh_drv: "\<Gamma> \<turnstile> (\<forall>X<:Q\<^sub>1. Q\<^sub>2) <: T" by simp 933 have lh_drv_prm\<^sub>1: "\<Gamma> \<turnstile> Q\<^sub>1 <: S\<^sub>1" by fact 934 have lh_drv_prm\<^sub>2: "((TVarB X Q\<^sub>1)#\<Gamma>) \<turnstile> S\<^sub>2 <: Q\<^sub>2" by fact 935 then have "X\<sharp>\<Gamma>" by (force dest: subtype_implies_ok simp add: valid_ty_dom_fresh) 936 then have fresh_cond: "X\<sharp>\<Gamma>" "X\<sharp>Q\<^sub>1" "X\<sharp>T" using rh_drv lh_drv_prm\<^sub>1 937 by (simp_all add: subtype_implies_fresh) 938 from rh_drv 939 have "T = Top \<or> 940 (\<exists>T\<^sub>1 T\<^sub>2. T = (\<forall>X<:T\<^sub>1. T\<^sub>2) \<and> \<Gamma> \<turnstile> T\<^sub>1 <: Q\<^sub>1 \<and> ((TVarB X T\<^sub>1)#\<Gamma>) \<turnstile> Q\<^sub>2 <: T\<^sub>2)" 941 using fresh_cond by (simp add: S_ForallE_left) 942 moreover 943 have "S\<^sub>1 closed_in \<Gamma>" and "S\<^sub>2 closed_in ((TVarB X Q\<^sub>1)#\<Gamma>)" 944 using lh_drv_prm\<^sub>1 lh_drv_prm\<^sub>2 by (simp_all add: subtype_implies_closed) 945 then have "(\<forall>X<:S\<^sub>1. S\<^sub>2) closed_in \<Gamma>" by (force simp add: closed_in_def ty.supp abs_supp) 946 moreover 947 have "\<turnstile> \<Gamma> ok" using rh_drv by (rule subtype_implies_ok) 948 moreover 949 { assume "\<exists>T\<^sub>1 T\<^sub>2. T=(\<forall>X<:T\<^sub>1. T\<^sub>2) \<and> \<Gamma>\<turnstile>T\<^sub>1<:Q\<^sub>1 \<and> ((TVarB X T\<^sub>1)#\<Gamma>)\<turnstile>Q\<^sub>2<:T\<^sub>2" 950 then obtain T\<^sub>1 T\<^sub>2 951 where T_inst: "T = (\<forall>X<:T\<^sub>1. T\<^sub>2)" 952 and rh_drv_prm\<^sub>1: "\<Gamma> \<turnstile> T\<^sub>1 <: Q\<^sub>1" 953 and rh_drv_prm\<^sub>2:"((TVarB X T\<^sub>1)#\<Gamma>) \<turnstile> Q\<^sub>2 <: T\<^sub>2" by force 954 have "(\<forall>X<:Q\<^sub>1. Q\<^sub>2) = Q" by fact 955 then have Q\<^sub>12_less: "size_ty Q\<^sub>1 < size_ty Q" "size_ty Q\<^sub>2 < size_ty Q" 956 using fresh_cond by auto 957 from IH_trans[of "Q\<^sub>1"] 958 have "\<Gamma> \<turnstile> T\<^sub>1 <: S\<^sub>1" using lh_drv_prm\<^sub>1 rh_drv_prm\<^sub>1 Q\<^sub>12_less by blast 959 moreover 960 from IH_narrow[of "Q\<^sub>1" "[]"] 961 have "((TVarB X T\<^sub>1)#\<Gamma>) \<turnstile> S\<^sub>2 <: Q\<^sub>2" using Q\<^sub>12_less lh_drv_prm\<^sub>2 rh_drv_prm\<^sub>1 by simp 962 with IH_trans[of "Q\<^sub>2"] 963 have "((TVarB X T\<^sub>1)#\<Gamma>) \<turnstile> S\<^sub>2 <: T\<^sub>2" using Q\<^sub>12_less rh_drv_prm\<^sub>2 by simp 964 ultimately have "\<Gamma> \<turnstile> (\<forall>X<:S\<^sub>1. S\<^sub>2) <: (\<forall>X<:T\<^sub>1. T\<^sub>2)" 965 using fresh_cond by (simp add: subtype_of.SA_all) 966 hence "\<Gamma> \<turnstile> (\<forall>X<:S\<^sub>1. S\<^sub>2) <: T" using T_inst by simp 967 } 968 ultimately show "\<Gamma> \<turnstile> (\<forall>X<:S\<^sub>1. S\<^sub>2) <: T" by blast 969 qed 970 } note transitivity_lemma = this 971 972 { \<comment> \<open>The transitivity proof is now by the auxiliary lemma.\<close> 973 case 1 974 from \<open>\<Gamma> \<turnstile> S <: Q\<close> and \<open>\<Gamma> \<turnstile> Q <: T\<close> 975 show "\<Gamma> \<turnstile> S <: T" by (rule transitivity_lemma) 976 next 977 case 2 978 from \<open>(\<Delta>@[(TVarB X Q)]@\<Gamma>) \<turnstile> M <: N\<close> 979 and \<open>\<Gamma> \<turnstile> P<:Q\<close> 980 show "(\<Delta>@[(TVarB X P)]@\<Gamma>) \<turnstile> M <: N" 981 proof (induct "\<Delta>@[(TVarB X Q)]@\<Gamma>" M N arbitrary: \<Gamma> X \<Delta> rule: subtype_of.induct) 982 case (SA_Top S \<Gamma> X \<Delta>) 983 from \<open>\<Gamma> \<turnstile> P <: Q\<close> 984 have "P closed_in \<Gamma>" by (simp add: subtype_implies_closed) 985 with \<open>\<turnstile> (\<Delta>@[(TVarB X Q)]@\<Gamma>) ok\<close> have "\<turnstile> (\<Delta>@[(TVarB X P)]@\<Gamma>) ok" 986 by (simp add: replace_type) 987 moreover 988 from \<open>S closed_in (\<Delta>@[(TVarB X Q)]@\<Gamma>)\<close> have "S closed_in (\<Delta>@[(TVarB X P)]@\<Gamma>)" 989 by (simp add: closed_in_def doms_append) 990 ultimately show "(\<Delta>@[(TVarB X P)]@\<Gamma>) \<turnstile> S <: Top" by (simp add: subtype_of.SA_Top) 991 next 992 case (SA_trans_TVar Y S N \<Gamma> X \<Delta>) 993 then have IH_inner: "(\<Delta>@[(TVarB X P)]@\<Gamma>) \<turnstile> S <: N" 994 and lh_drv_prm: "(TVarB Y S) \<in> set (\<Delta>@[(TVarB X Q)]@\<Gamma>)" 995 and rh_drv: "\<Gamma> \<turnstile> P<:Q" 996 and ok\<^sub>Q: "\<turnstile> (\<Delta>@[(TVarB X Q)]@\<Gamma>) ok" by (simp_all add: subtype_implies_ok) 997 then have ok\<^sub>P: "\<turnstile> (\<Delta>@[(TVarB X P)]@\<Gamma>) ok" by (simp add: subtype_implies_ok) 998 show "(\<Delta>@[(TVarB X P)]@\<Gamma>) \<turnstile> Tvar Y <: N" 999 proof (cases "X=Y") 1000 case False 1001 have "X\<noteq>Y" by fact 1002 hence "(TVarB Y S)\<in>set (\<Delta>@[(TVarB X P)]@\<Gamma>)" using lh_drv_prm by (simp add:binding.inject) 1003 with IH_inner show "(\<Delta>@[(TVarB X P)]@\<Gamma>) \<turnstile> Tvar Y <: N" by (simp add: subtype_of.SA_trans_TVar) 1004 next 1005 case True 1006 have memb\<^sub>XQ: "(TVarB X Q)\<in>set (\<Delta>@[(TVarB X Q)]@\<Gamma>)" by simp 1007 have memb\<^sub>XP: "(TVarB X P)\<in>set (\<Delta>@[(TVarB X P)]@\<Gamma>)" by simp 1008 have eq: "X=Y" by fact 1009 hence "S=Q" using ok\<^sub>Q lh_drv_prm memb\<^sub>XQ by (simp only: uniqueness_of_ctxt) 1010 hence "(\<Delta>@[(TVarB X P)]@\<Gamma>) \<turnstile> Q <: N" using IH_inner by simp 1011 moreover 1012 have "(\<Delta>@[(TVarB X P)]@\<Gamma>) extends \<Gamma>" by (simp add: extends_def) 1013 hence "(\<Delta>@[(TVarB X P)]@\<Gamma>) \<turnstile> P <: Q" using rh_drv ok\<^sub>P by (simp only: weakening) 1014 ultimately have "(\<Delta>@[(TVarB X P)]@\<Gamma>) \<turnstile> P <: N" by (simp add: transitivity_lemma) 1015 then show "(\<Delta>@[(TVarB X P)]@\<Gamma>) \<turnstile> Tvar Y <: N" using memb\<^sub>XP eq by auto 1016 qed 1017 next 1018 case (SA_refl_TVar Y \<Gamma> X \<Delta>) 1019 from \<open>\<Gamma> \<turnstile> P <: Q\<close> 1020 have "P closed_in \<Gamma>" by (simp add: subtype_implies_closed) 1021 with \<open>\<turnstile> (\<Delta>@[(TVarB X Q)]@\<Gamma>) ok\<close> have "\<turnstile> (\<Delta>@[(TVarB X P)]@\<Gamma>) ok" 1022 by (simp add: replace_type) 1023 moreover 1024 from \<open>Y \<in> ty_dom (\<Delta>@[(TVarB X Q)]@\<Gamma>)\<close> have "Y \<in> ty_dom (\<Delta>@[(TVarB X P)]@\<Gamma>)" 1025 by (simp add: doms_append) 1026 ultimately show "(\<Delta>@[(TVarB X P)]@\<Gamma>) \<turnstile> Tvar Y <: Tvar Y" by (simp add: subtype_of.SA_refl_TVar) 1027 next 1028 case (SA_arrow S\<^sub>1 Q\<^sub>1 Q\<^sub>2 S\<^sub>2 \<Gamma> X \<Delta>) 1029 then show "(\<Delta>@[(TVarB X P)]@\<Gamma>) \<turnstile> Q\<^sub>1 \<rightarrow> Q\<^sub>2 <: S\<^sub>1 \<rightarrow> S\<^sub>2" by blast 1030 next 1031 case (SA_all T\<^sub>1 S\<^sub>1 Y S\<^sub>2 T\<^sub>2 \<Gamma> X \<Delta>) 1032 have IH_inner\<^sub>1: "(\<Delta>@[(TVarB X P)]@\<Gamma>) \<turnstile> T\<^sub>1 <: S\<^sub>1" 1033 and IH_inner\<^sub>2: "(((TVarB Y T\<^sub>1)#\<Delta>)@[(TVarB X P)]@\<Gamma>) \<turnstile> S\<^sub>2 <: T\<^sub>2" 1034 by (fastforce intro: SA_all)+ 1035 then show "(\<Delta>@[(TVarB X P)]@\<Gamma>) \<turnstile> (\<forall>Y<:S\<^sub>1. S\<^sub>2) <: (\<forall>Y<:T\<^sub>1. T\<^sub>2)" by auto 1036 qed 1037 } 1038qed 1039 1040section \<open>Typing\<close> 1041 1042inductive 1043 typing :: "env \<Rightarrow> trm \<Rightarrow> ty \<Rightarrow> bool" ("_ \<turnstile> _ : _" [60,60,60] 60) 1044where 1045 T_Var[intro]: "\<lbrakk> VarB x T \<in> set \<Gamma>; \<turnstile> \<Gamma> ok \<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> Var x : T" 1046| 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> t\<^sub>1 \<cdot> t\<^sub>2 : T\<^sub>2" 1047| T_Abs[intro]: "\<lbrakk> VarB x T\<^sub>1 # \<Gamma> \<turnstile> t\<^sub>2 : T\<^sub>2 \<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> (\<lambda>x:T\<^sub>1. t\<^sub>2) : T\<^sub>1 \<rightarrow> T\<^sub>2" 1048| T_Sub[intro]: "\<lbrakk> \<Gamma> \<turnstile> t : S; \<Gamma> \<turnstile> S <: T \<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> t : T" 1049| T_TAbs[intro]:"\<lbrakk> TVarB X T\<^sub>1 # \<Gamma> \<turnstile> t\<^sub>2 : T\<^sub>2 \<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> (\<lambda>X<:T\<^sub>1. t\<^sub>2) : (\<forall>X<:T\<^sub>1. T\<^sub>2)" 1050| T_TApp[intro]:"\<lbrakk>X\<sharp>(\<Gamma>,t\<^sub>1,T\<^sub>2); \<Gamma> \<turnstile> t\<^sub>1 : (\<forall>X<:T\<^sub>11. T\<^sub>12); \<Gamma> \<turnstile> T\<^sub>2 <: T\<^sub>11\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> t\<^sub>1 \<cdot>\<^sub>\<tau> T\<^sub>2 : (T\<^sub>12[X \<mapsto> T\<^sub>2]\<^sub>\<tau>)" 1051 1052equivariance typing 1053 1054lemma better_T_TApp: 1055 assumes H1: "\<Gamma> \<turnstile> t\<^sub>1 : (\<forall>X<:T11. T12)" 1056 and H2: "\<Gamma> \<turnstile> T2 <: T11" 1057 shows "\<Gamma> \<turnstile> t\<^sub>1 \<cdot>\<^sub>\<tau> T2 : (T12[X \<mapsto> T2]\<^sub>\<tau>)" 1058proof - 1059 obtain Y::tyvrs where Y: "Y \<sharp> (X, T12, \<Gamma>, t\<^sub>1, T2)" 1060 by (rule exists_fresh) (rule fin_supp) 1061 then have "Y \<sharp> (\<Gamma>, t\<^sub>1, T2)" by simp 1062 moreover from Y have "(\<forall>X<:T11. T12) = (\<forall>Y<:T11. [(Y, X)] \<bullet> T12)" 1063 by (auto simp add: ty.inject alpha' fresh_prod fresh_atm) 1064 with H1 have "\<Gamma> \<turnstile> t\<^sub>1 : (\<forall>Y<:T11. [(Y, X)] \<bullet> T12)" by simp 1065 ultimately have "\<Gamma> \<turnstile> t\<^sub>1 \<cdot>\<^sub>\<tau> T2 : (([(Y, X)] \<bullet> T12)[Y \<mapsto> T2]\<^sub>\<tau>)" using H2 1066 by (rule T_TApp) 1067 with Y show ?thesis by (simp add: type_subst_rename) 1068qed 1069 1070lemma typing_ok: 1071 assumes "\<Gamma> \<turnstile> t : T" 1072 shows "\<turnstile> \<Gamma> ok" 1073using assms by (induct) (auto) 1074 1075nominal_inductive typing 1076by (auto dest!: typing_ok intro: closed_in_fresh fresh_dom type_subst_fresh 1077 simp: abs_fresh fresh_type_subst_fresh ty_vrs_fresh valid_ty_dom_fresh fresh_trm_dom) 1078 1079lemma ok_imp_VarB_closed_in: 1080 assumes ok: "\<turnstile> \<Gamma> ok" 1081 shows "VarB x T \<in> set \<Gamma> \<Longrightarrow> T closed_in \<Gamma>" using ok 1082 by induct (auto simp add: binding.inject closed_in_def) 1083 1084lemma tyvrs_of_subst: "tyvrs_of (B[X \<mapsto> T]\<^sub>b) = tyvrs_of B" 1085 by (nominal_induct B rule: binding.strong_induct) simp_all 1086 1087lemma ty_dom_subst: "ty_dom (\<Gamma>[X \<mapsto> T]\<^sub>e) = ty_dom \<Gamma>" 1088 by (induct \<Gamma>) (simp_all add: tyvrs_of_subst) 1089 1090lemma vrs_of_subst: "vrs_of (B[X \<mapsto> T]\<^sub>b) = vrs_of B" 1091 by (nominal_induct B rule: binding.strong_induct) simp_all 1092 1093lemma trm_dom_subst: "trm_dom (\<Gamma>[X \<mapsto> T]\<^sub>e) = trm_dom \<Gamma>" 1094 by (induct \<Gamma>) (simp_all add: vrs_of_subst) 1095 1096lemma subst_closed_in: 1097 "T closed_in (\<Delta> @ TVarB X S # \<Gamma>) \<Longrightarrow> U closed_in \<Gamma> \<Longrightarrow> T[X \<mapsto> U]\<^sub>\<tau> closed_in (\<Delta>[X \<mapsto> U]\<^sub>e @ \<Gamma>)" 1098 apply (nominal_induct T avoiding: X U \<Gamma> rule: ty.strong_induct) 1099 apply (simp add: closed_in_def ty.supp supp_atm doms_append ty_dom_subst) 1100 apply blast 1101 apply (simp add: closed_in_def ty.supp) 1102 apply (simp add: closed_in_def ty.supp) 1103 apply (simp add: closed_in_def ty.supp abs_supp) 1104 apply (drule_tac x = X in meta_spec) 1105 apply (drule_tac x = U in meta_spec) 1106 apply (drule_tac x = "(TVarB tyvrs ty2) # \<Gamma>" in meta_spec) 1107 apply (simp add: doms_append ty_dom_subst) 1108 apply blast 1109 done 1110 1111lemmas subst_closed_in' = subst_closed_in [where \<Delta>="[]", simplified] 1112 1113lemma typing_closed_in: 1114 assumes "\<Gamma> \<turnstile> t : T" 1115 shows "T closed_in \<Gamma>" 1116using assms 1117proof induct 1118 case (T_Var x T \<Gamma>) 1119 from \<open>\<turnstile> \<Gamma> ok\<close> and \<open>VarB x T \<in> set \<Gamma>\<close> 1120 show ?case by (rule ok_imp_VarB_closed_in) 1121next 1122 case (T_App \<Gamma> t\<^sub>1 T\<^sub>1 T\<^sub>2 t\<^sub>2) 1123 then show ?case by (auto simp add: ty.supp closed_in_def) 1124next 1125 case (T_Abs x T\<^sub>1 \<Gamma> t\<^sub>2 T\<^sub>2) 1126 from \<open>VarB x T\<^sub>1 # \<Gamma> \<turnstile> t\<^sub>2 : T\<^sub>2\<close> 1127 have "T\<^sub>1 closed_in \<Gamma>" by (auto dest: typing_ok) 1128 with T_Abs show ?case by (auto simp add: ty.supp closed_in_def) 1129next 1130 case (T_Sub \<Gamma> t S T) 1131 from \<open>\<Gamma> \<turnstile> S <: T\<close> show ?case by (simp add: subtype_implies_closed) 1132next 1133 case (T_TAbs X T\<^sub>1 \<Gamma> t\<^sub>2 T\<^sub>2) 1134 from \<open>TVarB X T\<^sub>1 # \<Gamma> \<turnstile> t\<^sub>2 : T\<^sub>2\<close> 1135 have "T\<^sub>1 closed_in \<Gamma>" by (auto dest: typing_ok) 1136 with T_TAbs show ?case by (auto simp add: ty.supp closed_in_def abs_supp) 1137next 1138 case (T_TApp X \<Gamma> t\<^sub>1 T2 T11 T12) 1139 then have "T12 closed_in (TVarB X T11 # \<Gamma>)" 1140 by (auto simp add: closed_in_def ty.supp abs_supp) 1141 moreover from T_TApp have "T2 closed_in \<Gamma>" 1142 by (simp add: subtype_implies_closed) 1143 ultimately show ?case by (rule subst_closed_in') 1144qed 1145 1146 1147subsection \<open>Evaluation\<close> 1148 1149inductive 1150 val :: "trm \<Rightarrow> bool" 1151where 1152 Abs[intro]: "val (\<lambda>x:T. t)" 1153| TAbs[intro]: "val (\<lambda>X<:T. t)" 1154 1155equivariance val 1156 1157inductive_cases val_inv_auto[elim]: 1158 "val (Var x)" 1159 "val (t1 \<cdot> t2)" 1160 "val (t1 \<cdot>\<^sub>\<tau> t2)" 1161 1162inductive 1163 eval :: "trm \<Rightarrow> trm \<Rightarrow> bool" ("_ \<longmapsto> _" [60,60] 60) 1164where 1165 E_Abs : "\<lbrakk> x \<sharp> v\<^sub>2; val v\<^sub>2 \<rbrakk> \<Longrightarrow> (\<lambda>x:T\<^sub>11. t\<^sub>12) \<cdot> v\<^sub>2 \<longmapsto> t\<^sub>12[x \<mapsto> v\<^sub>2]" 1166| E_App1 [intro]: "t \<longmapsto> t' \<Longrightarrow> t \<cdot> u \<longmapsto> t' \<cdot> u" 1167| E_App2 [intro]: "\<lbrakk> val v; t \<longmapsto> t' \<rbrakk> \<Longrightarrow> v \<cdot> t \<longmapsto> v \<cdot> t'" 1168| E_TAbs : "X \<sharp> (T\<^sub>11, T\<^sub>2) \<Longrightarrow> (\<lambda>X<:T\<^sub>11. t\<^sub>12) \<cdot>\<^sub>\<tau> T\<^sub>2 \<longmapsto> t\<^sub>12[X \<mapsto>\<^sub>\<tau> T\<^sub>2]" 1169| E_TApp [intro]: "t \<longmapsto> t' \<Longrightarrow> t \<cdot>\<^sub>\<tau> T \<longmapsto> t' \<cdot>\<^sub>\<tau> T" 1170 1171lemma better_E_Abs[intro]: 1172 assumes H: "val v2" 1173 shows "(\<lambda>x:T11. t12) \<cdot> v2 \<longmapsto> t12[x \<mapsto> v2]" 1174proof - 1175 obtain y::vrs where y: "y \<sharp> (x, t12, v2)" by (rule exists_fresh) (rule fin_supp) 1176 then have "y \<sharp> v2" by simp 1177 then have "(\<lambda>y:T11. [(y, x)] \<bullet> t12) \<cdot> v2 \<longmapsto> ([(y, x)] \<bullet> t12)[y \<mapsto> v2]" using H 1178 by (rule E_Abs) 1179 moreover from y have "(\<lambda>x:T11. t12) \<cdot> v2 = (\<lambda>y:T11. [(y, x)] \<bullet> t12) \<cdot> v2" 1180 by (auto simp add: trm.inject alpha' fresh_prod fresh_atm) 1181 ultimately have "(\<lambda>x:T11. t12) \<cdot> v2 \<longmapsto> ([(y, x)] \<bullet> t12)[y \<mapsto> v2]" 1182 by simp 1183 with y show ?thesis by (simp add: subst_trm_rename) 1184qed 1185 1186lemma better_E_TAbs[intro]: "(\<lambda>X<:T11. t12) \<cdot>\<^sub>\<tau> T2 \<longmapsto> t12[X \<mapsto>\<^sub>\<tau> T2]" 1187proof - 1188 obtain Y::tyvrs where Y: "Y \<sharp> (X, t12, T11, T2)" by (rule exists_fresh) (rule fin_supp) 1189 then have "Y \<sharp> (T11, T2)" by simp 1190 then have "(\<lambda>Y<:T11. [(Y, X)] \<bullet> t12) \<cdot>\<^sub>\<tau> T2 \<longmapsto> ([(Y, X)] \<bullet> t12)[Y \<mapsto>\<^sub>\<tau> T2]" 1191 by (rule E_TAbs) 1192 moreover from Y have "(\<lambda>X<:T11. t12) \<cdot>\<^sub>\<tau> T2 = (\<lambda>Y<:T11. [(Y, X)] \<bullet> t12) \<cdot>\<^sub>\<tau> T2" 1193 by (auto simp add: trm.inject alpha' fresh_prod fresh_atm) 1194 ultimately have "(\<lambda>X<:T11. t12) \<cdot>\<^sub>\<tau> T2 \<longmapsto> ([(Y, X)] \<bullet> t12)[Y \<mapsto>\<^sub>\<tau> T2]" 1195 by simp 1196 with Y show ?thesis by (simp add: subst_trm_ty_rename) 1197qed 1198 1199equivariance eval 1200 1201nominal_inductive eval 1202 by (simp_all add: abs_fresh ty_vrs_fresh subst_trm_fresh_tyvar 1203 subst_trm_fresh_var subst_trm_ty_fresh') 1204 1205inductive_cases eval_inv_auto[elim]: 1206 "Var x \<longmapsto> t'" 1207 "(\<lambda>x:T. t) \<longmapsto> t'" 1208 "(\<lambda>X<:T. t) \<longmapsto> t'" 1209 1210lemma ty_dom_cons: 1211 shows "ty_dom (\<Gamma>@[VarB X Q]@\<Delta>) = ty_dom (\<Gamma>@\<Delta>)" 1212by (induct \<Gamma>) (auto) 1213 1214lemma closed_in_cons: 1215 assumes "S closed_in (\<Gamma> @ VarB X Q # \<Delta>)" 1216 shows "S closed_in (\<Gamma>@\<Delta>)" 1217using assms ty_dom_cons closed_in_def by auto 1218 1219lemma closed_in_weaken: "T closed_in (\<Delta> @ \<Gamma>) \<Longrightarrow> T closed_in (\<Delta> @ B # \<Gamma>)" 1220 by (auto simp add: closed_in_def doms_append) 1221 1222lemma closed_in_weaken': "T closed_in \<Gamma> \<Longrightarrow> T closed_in (\<Delta> @ \<Gamma>)" 1223 by (auto simp add: closed_in_def doms_append) 1224 1225lemma valid_subst: 1226 assumes ok: "\<turnstile> (\<Delta> @ TVarB X Q # \<Gamma>) ok" 1227 and closed: "P closed_in \<Gamma>" 1228 shows "\<turnstile> (\<Delta>[X \<mapsto> P]\<^sub>e @ \<Gamma>) ok" using ok closed 1229 apply (induct \<Delta>) 1230 apply simp_all 1231 apply (erule validE) 1232 apply assumption 1233 apply (erule validE) 1234 apply simp 1235 apply (rule valid_consT) 1236 apply assumption 1237 apply (simp add: doms_append ty_dom_subst) 1238 apply (simp add: fresh_fin_insert [OF pt_tyvrs_inst at_tyvrs_inst fs_tyvrs_inst] finite_doms) 1239 apply (rule_tac S=Q in subst_closed_in') 1240 apply (simp add: closed_in_def doms_append ty_dom_subst) 1241 apply (simp add: closed_in_def doms_append) 1242 apply blast 1243 apply simp 1244 apply (rule valid_cons) 1245 apply assumption 1246 apply (simp add: doms_append trm_dom_subst) 1247 apply (rule_tac S=Q in subst_closed_in') 1248 apply (simp add: closed_in_def doms_append ty_dom_subst) 1249 apply (simp add: closed_in_def doms_append) 1250 apply blast 1251 done 1252 1253lemma ty_dom_vrs: 1254 shows "ty_dom (G @ [VarB x Q] @ D) = ty_dom (G @ D)" 1255by (induct G) (auto) 1256 1257lemma valid_cons': 1258 assumes "\<turnstile> (\<Gamma> @ VarB x Q # \<Delta>) ok" 1259 shows "\<turnstile> (\<Gamma> @ \<Delta>) ok" 1260 using assms 1261proof (induct "\<Gamma> @ VarB x Q # \<Delta>" arbitrary: \<Gamma> \<Delta>) 1262 case valid_nil 1263 have "[] = \<Gamma> @ VarB x Q # \<Delta>" by fact 1264 then have "False" by auto 1265 then show ?case by auto 1266next 1267 case (valid_consT G X T) 1268 then show ?case 1269 proof (cases \<Gamma>) 1270 case Nil 1271 with valid_consT show ?thesis by simp 1272 next 1273 case (Cons b bs) 1274 with valid_consT 1275 have "\<turnstile> (bs @ \<Delta>) ok" by simp 1276 moreover from Cons and valid_consT have "X \<sharp> ty_dom (bs @ \<Delta>)" 1277 by (simp add: doms_append) 1278 moreover from Cons and valid_consT have "T closed_in (bs @ \<Delta>)" 1279 by (simp add: closed_in_def doms_append) 1280 ultimately have "\<turnstile> (TVarB X T # bs @ \<Delta>) ok" 1281 by (rule valid_rel.valid_consT) 1282 with Cons and valid_consT show ?thesis by simp 1283 qed 1284next 1285 case (valid_cons G x T) 1286 then show ?case 1287 proof (cases \<Gamma>) 1288 case Nil 1289 with valid_cons show ?thesis by simp 1290 next 1291 case (Cons b bs) 1292 with valid_cons 1293 have "\<turnstile> (bs @ \<Delta>) ok" by simp 1294 moreover from Cons and valid_cons have "x \<sharp> trm_dom (bs @ \<Delta>)" 1295 by (simp add: doms_append finite_doms 1296 fresh_fin_insert [OF pt_vrs_inst at_vrs_inst fs_vrs_inst]) 1297 moreover from Cons and valid_cons have "T closed_in (bs @ \<Delta>)" 1298 by (simp add: closed_in_def doms_append) 1299 ultimately have "\<turnstile> (VarB x T # bs @ \<Delta>) ok" 1300 by (rule valid_rel.valid_cons) 1301 with Cons and valid_cons show ?thesis by simp 1302 qed 1303qed 1304 1305text \<open>A.5(6)\<close> 1306 1307lemma type_weaken: 1308 assumes "(\<Delta>@\<Gamma>) \<turnstile> t : T" 1309 and "\<turnstile> (\<Delta> @ B # \<Gamma>) ok" 1310 shows "(\<Delta> @ B # \<Gamma>) \<turnstile> t : T" 1311using assms 1312proof(nominal_induct "\<Delta> @ \<Gamma>" t T avoiding: \<Delta> \<Gamma> B rule: typing.strong_induct) 1313 case (T_Var x T) 1314 then show ?case by auto 1315next 1316 case (T_App X t\<^sub>1 T\<^sub>2 T\<^sub>11 T\<^sub>12) 1317 then show ?case by force 1318next 1319 case (T_Abs y T\<^sub>1 t\<^sub>2 T\<^sub>2 \<Delta> \<Gamma>) 1320 then have "VarB y T\<^sub>1 # \<Delta> @ \<Gamma> \<turnstile> t\<^sub>2 : T\<^sub>2" by simp 1321 then have closed: "T\<^sub>1 closed_in (\<Delta> @ \<Gamma>)" 1322 by (auto dest: typing_ok) 1323 have "\<turnstile> (VarB y T\<^sub>1 # \<Delta> @ B # \<Gamma>) ok" 1324 apply (rule valid_cons) 1325 apply (rule T_Abs) 1326 apply (simp add: doms_append 1327 fresh_fin_insert [OF pt_vrs_inst at_vrs_inst fs_vrs_inst] 1328 fresh_fin_union [OF pt_vrs_inst at_vrs_inst fs_vrs_inst] 1329 finite_doms finite_vrs fresh_vrs_of T_Abs fresh_trm_dom) 1330 apply (rule closed_in_weaken) 1331 apply (rule closed) 1332 done 1333 then have "\<turnstile> ((VarB y T\<^sub>1 # \<Delta>) @ B # \<Gamma>) ok" by simp 1334 with _ have "(VarB y T\<^sub>1 # \<Delta>) @ B # \<Gamma> \<turnstile> t\<^sub>2 : T\<^sub>2" 1335 by (rule T_Abs) simp 1336 then have "VarB y T\<^sub>1 # \<Delta> @ B # \<Gamma> \<turnstile> t\<^sub>2 : T\<^sub>2" by simp 1337 then show ?case by (rule typing.T_Abs) 1338next 1339 case (T_Sub t S T \<Delta> \<Gamma>) 1340 from refl and \<open>\<turnstile> (\<Delta> @ B # \<Gamma>) ok\<close> 1341 have "\<Delta> @ B # \<Gamma> \<turnstile> t : S" by (rule T_Sub) 1342 moreover from \<open>(\<Delta> @ \<Gamma>)\<turnstile>S<:T\<close> and \<open>\<turnstile> (\<Delta> @ B # \<Gamma>) ok\<close> 1343 have "(\<Delta> @ B # \<Gamma>)\<turnstile>S<:T" 1344 by (rule weakening) (simp add: extends_def T_Sub) 1345 ultimately show ?case by (rule typing.T_Sub) 1346next 1347 case (T_TAbs X T\<^sub>1 t\<^sub>2 T\<^sub>2 \<Delta> \<Gamma>) 1348 from \<open>TVarB X T\<^sub>1 # \<Delta> @ \<Gamma> \<turnstile> t\<^sub>2 : T\<^sub>2\<close> 1349 have closed: "T\<^sub>1 closed_in (\<Delta> @ \<Gamma>)" 1350 by (auto dest: typing_ok) 1351 have "\<turnstile> (TVarB X T\<^sub>1 # \<Delta> @ B # \<Gamma>) ok" 1352 apply (rule valid_consT) 1353 apply (rule T_TAbs) 1354 apply (simp add: doms_append 1355 fresh_fin_insert [OF pt_tyvrs_inst at_tyvrs_inst fs_tyvrs_inst] 1356 fresh_fin_union [OF pt_tyvrs_inst at_tyvrs_inst fs_tyvrs_inst] 1357 finite_doms finite_vrs tyvrs_fresh T_TAbs fresh_dom) 1358 apply (rule closed_in_weaken) 1359 apply (rule closed) 1360 done 1361 then have "\<turnstile> ((TVarB X T\<^sub>1 # \<Delta>) @ B # \<Gamma>) ok" by simp 1362 with _ have "(TVarB X T\<^sub>1 # \<Delta>) @ B # \<Gamma> \<turnstile> t\<^sub>2 : T\<^sub>2" 1363 by (rule T_TAbs) simp 1364 then have "TVarB X T\<^sub>1 # \<Delta> @ B # \<Gamma> \<turnstile> t\<^sub>2 : T\<^sub>2" by simp 1365 then show ?case by (rule typing.T_TAbs) 1366next 1367 case (T_TApp X t\<^sub>1 T2 T11 T12 \<Delta> \<Gamma>) 1368 have "\<Delta> @ B # \<Gamma> \<turnstile> t\<^sub>1 : (\<forall>X<:T11. T12)" 1369 by (rule T_TApp refl)+ 1370 moreover from \<open>(\<Delta> @ \<Gamma>)\<turnstile>T2<:T11\<close> and \<open>\<turnstile> (\<Delta> @ B # \<Gamma>) ok\<close> 1371 have "(\<Delta> @ B # \<Gamma>)\<turnstile>T2<:T11" 1372 by (rule weakening) (simp add: extends_def T_TApp) 1373 ultimately show ?case by (rule better_T_TApp) 1374qed 1375 1376lemma type_weaken': 1377 "\<Gamma> \<turnstile> t : T \<Longrightarrow> \<turnstile> (\<Delta>@\<Gamma>) ok \<Longrightarrow> (\<Delta>@\<Gamma>) \<turnstile> t : T" 1378 apply (induct \<Delta>) 1379 apply simp_all 1380 apply (erule validE) 1381 apply (insert type_weaken [of "[]", simplified]) 1382 apply simp_all 1383 done 1384 1385text \<open>A.6\<close> 1386 1387lemma strengthening: 1388 assumes "(\<Gamma> @ VarB x Q # \<Delta>) \<turnstile> S <: T" 1389 shows "(\<Gamma>@\<Delta>) \<turnstile> S <: T" 1390 using assms 1391proof (induct "\<Gamma> @ VarB x Q # \<Delta>" S T arbitrary: \<Gamma>) 1392 case (SA_Top S) 1393 then have "\<turnstile> (\<Gamma> @ \<Delta>) ok" by (auto dest: valid_cons') 1394 moreover have "S closed_in (\<Gamma> @ \<Delta>)" using SA_Top by (auto dest: closed_in_cons) 1395 ultimately show ?case using subtype_of.SA_Top by auto 1396next 1397 case (SA_refl_TVar X) 1398 from \<open>\<turnstile> (\<Gamma> @ VarB x Q # \<Delta>) ok\<close> 1399 have h1:"\<turnstile> (\<Gamma> @ \<Delta>) ok" by (auto dest: valid_cons') 1400 have "X \<in> ty_dom (\<Gamma> @ VarB x Q # \<Delta>)" using SA_refl_TVar by auto 1401 then have h2:"X \<in> ty_dom (\<Gamma> @ \<Delta>)" using ty_dom_vrs by auto 1402 show ?case using h1 h2 by auto 1403next 1404 case (SA_all T1 S1 X S2 T2) 1405 have h1:"((TVarB X T1 # \<Gamma>) @ \<Delta>)\<turnstile>S2<:T2" by (fastforce intro: SA_all) 1406 have h2:"(\<Gamma> @ \<Delta>)\<turnstile>T1<:S1" using SA_all by auto 1407 then show ?case using h1 h2 by auto 1408qed (auto) 1409 1410lemma narrow_type: \<comment> \<open>A.7\<close> 1411 assumes H: "\<Delta> @ (TVarB X Q) # \<Gamma> \<turnstile> t : T" 1412 shows "\<Gamma> \<turnstile> P <: Q \<Longrightarrow> \<Delta> @ (TVarB X P) # \<Gamma> \<turnstile> t : T" 1413 using H 1414 proof (nominal_induct "\<Delta> @ (TVarB X Q) # \<Gamma>" t T avoiding: P arbitrary: \<Delta> rule: typing.strong_induct) 1415 case (T_Var x T P D) 1416 then have "VarB x T \<in> set (D @ TVarB X P # \<Gamma>)" 1417 and "\<turnstile> (D @ TVarB X P # \<Gamma>) ok" 1418 by (auto intro: replace_type dest!: subtype_implies_closed) 1419 then show ?case by auto 1420 next 1421 case (T_App t1 T1 T2 t2 P D) 1422 then show ?case by force 1423 next 1424 case (T_Abs x T1 t2 T2 P D) 1425 then show ?case by (fastforce dest: typing_ok) 1426 next 1427 case (T_Sub t S T P D) 1428 then show ?case using subtype_narrow by fastforce 1429 next 1430 case (T_TAbs X' T1 t2 T2 P D) 1431 then show ?case by (fastforce dest: typing_ok) 1432 next 1433 case (T_TApp X' t1 T2 T11 T12 P D) 1434 then have "D @ TVarB X P # \<Gamma> \<turnstile> t1 : Forall X' T12 T11" by fastforce 1435 moreover have "(D @ [TVarB X Q] @ \<Gamma>) \<turnstile> T2<:T11" using T_TApp by auto 1436 then have "(D @ [TVarB X P] @ \<Gamma>) \<turnstile> T2<:T11" using \<open>\<Gamma>\<turnstile>P<:Q\<close> 1437 by (rule subtype_narrow) 1438 moreover from T_TApp have "X' \<sharp> (D @ TVarB X P # \<Gamma>, t1, T2)" 1439 by (simp add: fresh_list_append fresh_list_cons fresh_prod) 1440 ultimately show ?case by auto 1441qed 1442 1443subsection \<open>Substitution lemmas\<close> 1444 1445subsubsection \<open>Substition Preserves Typing\<close> 1446 1447theorem subst_type: \<comment> \<open>A.8\<close> 1448 assumes H: "(\<Delta> @ (VarB x U) # \<Gamma>) \<turnstile> t : T" 1449 shows "\<Gamma> \<turnstile> u : U \<Longrightarrow> \<Delta> @ \<Gamma> \<turnstile> t[x \<mapsto> u] : T" using H 1450 proof (nominal_induct "\<Delta> @ (VarB x U) # \<Gamma>" t T avoiding: x u arbitrary: \<Delta> rule: typing.strong_induct) 1451 case (T_Var y T x u D) 1452 show ?case 1453 proof (cases "x = y") 1454 assume eq:"x=y" 1455 then have "T=U" using T_Var uniqueness_of_ctxt' by auto 1456 then show ?case using eq T_Var 1457 by (auto intro: type_weaken' dest: valid_cons') 1458 next 1459 assume "x\<noteq>y" 1460 then show ?case using T_Var 1461 by (auto simp add:binding.inject dest: valid_cons') 1462 qed 1463 next 1464 case (T_App t1 T1 T2 t2 x u D) 1465 then show ?case by force 1466 next 1467 case (T_Abs y T1 t2 T2 x u D) 1468 then show ?case by force 1469 next 1470 case (T_Sub t S T x u D) 1471 then have "D @ \<Gamma> \<turnstile> t[x \<mapsto> u] : S" by auto 1472 moreover have "(D @ \<Gamma>) \<turnstile> S<:T" using T_Sub by (auto dest: strengthening) 1473 ultimately show ?case by auto 1474 next 1475 case (T_TAbs X T1 t2 T2 x u D) 1476 from \<open>TVarB X T1 # D @ VarB x U # \<Gamma> \<turnstile> t2 : T2\<close> have "X \<sharp> T1" 1477 by (auto simp add: valid_ty_dom_fresh dest: typing_ok intro!: closed_in_fresh) 1478 with \<open>X \<sharp> u\<close> and T_TAbs show ?case by fastforce 1479 next 1480 case (T_TApp X t1 T2 T11 T12 x u D) 1481 then have "(D@\<Gamma>) \<turnstile>T2<:T11" using T_TApp by (auto dest: strengthening) 1482 then show "((D @ \<Gamma>) \<turnstile> ((t1 \<cdot>\<^sub>\<tau> T2)[x \<mapsto> u]) : (T12[X \<mapsto> T2]\<^sub>\<tau>))" using T_TApp 1483 by (force simp add: fresh_prod fresh_list_append fresh_list_cons subst_trm_fresh_tyvar) 1484qed 1485 1486subsubsection \<open>Type Substitution Preserves Subtyping\<close> 1487 1488lemma substT_subtype: \<comment> \<open>A.10\<close> 1489 assumes H: "(\<Delta> @ ((TVarB X Q) # \<Gamma>)) \<turnstile> S <: T" 1490 shows "\<Gamma> \<turnstile> P <: Q \<Longrightarrow> (\<Delta>[X \<mapsto> P]\<^sub>e @ \<Gamma>) \<turnstile> S[X \<mapsto> P]\<^sub>\<tau> <: T[X \<mapsto> P]\<^sub>\<tau>" 1491 using H 1492proof (nominal_induct "\<Delta> @ TVarB X Q # \<Gamma>" S T avoiding: X P arbitrary: \<Delta> rule: subtype_of.strong_induct) 1493 case (SA_Top S X P D) 1494 then have "\<turnstile> (D @ TVarB X Q # \<Gamma>) ok" by simp 1495 moreover have closed: "P closed_in \<Gamma>" using SA_Top subtype_implies_closed by auto 1496 ultimately have "\<turnstile> (D[X \<mapsto> P]\<^sub>e @ \<Gamma>) ok" by (rule valid_subst) 1497 moreover from SA_Top have "S closed_in (D @ TVarB X Q # \<Gamma>)" by simp 1498 then have "S[X \<mapsto> P]\<^sub>\<tau> closed_in (D[X \<mapsto> P]\<^sub>e @ \<Gamma>)" using closed by (rule subst_closed_in) 1499 ultimately show ?case by auto 1500next 1501 case (SA_trans_TVar Y S T X P D) 1502 have h:"(D @ TVarB X Q # \<Gamma>)\<turnstile>S<:T" by fact 1503 then have ST: "(D[X \<mapsto> P]\<^sub>e @ \<Gamma>) \<turnstile> S[X \<mapsto> P]\<^sub>\<tau> <: T[X \<mapsto> P]\<^sub>\<tau>" using SA_trans_TVar by auto 1504 from h have G_ok: "\<turnstile> (D @ TVarB X Q # \<Gamma>) ok" by (rule subtype_implies_ok) 1505 from G_ok and SA_trans_TVar have X_\<Gamma>_ok: "\<turnstile> (TVarB X Q # \<Gamma>) ok" 1506 by (auto intro: validE_append) 1507 show "(D[X \<mapsto> P]\<^sub>e @ \<Gamma>) \<turnstile> Tvar Y[X \<mapsto> P]\<^sub>\<tau><:T[X \<mapsto> P]\<^sub>\<tau>" 1508 proof (cases "X = Y") 1509 assume eq: "X = Y" 1510 from eq and SA_trans_TVar have "TVarB Y Q \<in> set (D @ TVarB X Q # \<Gamma>)" by simp 1511 with G_ok have QS: "Q = S" using \<open>TVarB Y S \<in> set (D @ TVarB X Q # \<Gamma>)\<close> 1512 by (rule uniqueness_of_ctxt) 1513 from X_\<Gamma>_ok have "X \<sharp> ty_dom \<Gamma>" and "Q closed_in \<Gamma>" by auto 1514 then have XQ: "X \<sharp> Q" by (rule closed_in_fresh) 1515 note \<open>\<Gamma>\<turnstile>P<:Q\<close> 1516 moreover from ST have "\<turnstile> (D[X \<mapsto> P]\<^sub>e @ \<Gamma>) ok" by (rule subtype_implies_ok) 1517 moreover have "(D[X \<mapsto> P]\<^sub>e @ \<Gamma>) extends \<Gamma>" by (simp add: extends_def) 1518 ultimately have "(D[X \<mapsto> P]\<^sub>e @ \<Gamma>) \<turnstile> P<:Q" by (rule weakening) 1519 with QS have "(D[X \<mapsto> P]\<^sub>e @ \<Gamma>) \<turnstile> P<:S" by simp 1520 moreover from XQ and ST and QS have "(D[X \<mapsto> P]\<^sub>e @ \<Gamma>) \<turnstile> S<:T[X \<mapsto> P]\<^sub>\<tau>" 1521 by (simp add: type_subst_identity) 1522 ultimately have "(D[X \<mapsto> P]\<^sub>e @ \<Gamma>) \<turnstile> P<:T[X \<mapsto> P]\<^sub>\<tau>" 1523 by (rule subtype_transitivity) 1524 with eq show ?case by simp 1525 next 1526 assume neq: "X \<noteq> Y" 1527 with SA_trans_TVar have "TVarB Y S \<in> set D \<or> TVarB Y S \<in> set \<Gamma>" 1528 by (simp add: binding.inject) 1529 then show ?case 1530 proof 1531 assume "TVarB Y S \<in> set D" 1532 then have "TVarB Y (S[X \<mapsto> P]\<^sub>\<tau>) \<in> set (D[X \<mapsto> P]\<^sub>e)" 1533 by (rule ctxt_subst_mem_TVarB) 1534 then have "TVarB Y (S[X \<mapsto> P]\<^sub>\<tau>) \<in> set (D[X \<mapsto> P]\<^sub>e @ \<Gamma>)" by simp 1535 with neq and ST show ?thesis by auto 1536 next 1537 assume Y: "TVarB Y S \<in> set \<Gamma>" 1538 from X_\<Gamma>_ok have "X \<sharp> ty_dom \<Gamma>" and "\<turnstile> \<Gamma> ok" by auto 1539 then have "X \<sharp> \<Gamma>" by (simp add: valid_ty_dom_fresh) 1540 with Y have "X \<sharp> S" 1541 by (induct \<Gamma>) (auto simp add: fresh_list_nil fresh_list_cons) 1542 with ST have "(D[X \<mapsto> P]\<^sub>e @ \<Gamma>)\<turnstile>S<:T[X \<mapsto> P]\<^sub>\<tau>" 1543 by (simp add: type_subst_identity) 1544 moreover from Y have "TVarB Y S \<in> set (D[X \<mapsto> P]\<^sub>e @ \<Gamma>)" by simp 1545 ultimately show ?thesis using neq by auto 1546 qed 1547 qed 1548next 1549 case (SA_refl_TVar Y X P D) 1550 note \<open>\<turnstile> (D @ TVarB X Q # \<Gamma>) ok\<close> 1551 moreover from SA_refl_TVar have closed: "P closed_in \<Gamma>" 1552 by (auto dest: subtype_implies_closed) 1553 ultimately have ok: "\<turnstile> (D[X \<mapsto> P]\<^sub>e @ \<Gamma>) ok" using valid_subst by auto 1554 from closed have closed': "P closed_in (D[X \<mapsto> P]\<^sub>e @ \<Gamma>)" 1555 by (simp add: closed_in_weaken') 1556 show ?case 1557 proof (cases "X = Y") 1558 assume "X = Y" 1559 with closed' and ok show ?thesis 1560 by (auto intro: subtype_reflexivity) 1561 next 1562 assume neq: "X \<noteq> Y" 1563 with SA_refl_TVar have "Y \<in> ty_dom (D[X \<mapsto> P]\<^sub>e @ \<Gamma>)" 1564 by (simp add: ty_dom_subst doms_append) 1565 with neq and ok show ?thesis by auto 1566 qed 1567next 1568 case (SA_arrow T1 S1 S2 T2 X P D) 1569 then have h1:"(D[X \<mapsto> P]\<^sub>e @ \<Gamma>)\<turnstile>T1[X \<mapsto> P]\<^sub>\<tau><:S1[X \<mapsto> P]\<^sub>\<tau>" using SA_arrow by auto 1570 from SA_arrow have h2:"(D[X \<mapsto> P]\<^sub>e @ \<Gamma>)\<turnstile>S2[X \<mapsto> P]\<^sub>\<tau><:T2[X \<mapsto> P]\<^sub>\<tau>" using SA_arrow by auto 1571 show ?case using subtype_of.SA_arrow h1 h2 by auto 1572next 1573 case (SA_all T1 S1 Y S2 T2 X P D) 1574 then have Y: "Y \<sharp> ty_dom (D @ TVarB X Q # \<Gamma>)" 1575 by (auto dest: subtype_implies_ok intro: fresh_dom) 1576 moreover from SA_all have "S1 closed_in (D @ TVarB X Q # \<Gamma>)" 1577 by (auto dest: subtype_implies_closed) 1578 ultimately have S1: "Y \<sharp> S1" by (rule closed_in_fresh) 1579 from SA_all have "T1 closed_in (D @ TVarB X Q # \<Gamma>)" 1580 by (auto dest: subtype_implies_closed) 1581 with Y have T1: "Y \<sharp> T1" by (rule closed_in_fresh) 1582 with SA_all and S1 show ?case by force 1583qed 1584 1585subsubsection \<open>Type Substitution Preserves Typing\<close> 1586 1587theorem substT_type: \<comment> \<open>A.11\<close> 1588 assumes H: "(D @ TVarB X Q # G) \<turnstile> t : T" 1589 shows "G \<turnstile> P <: Q \<Longrightarrow> 1590 (D[X \<mapsto> P]\<^sub>e @ G) \<turnstile> t[X \<mapsto>\<^sub>\<tau> P] : T[X \<mapsto> P]\<^sub>\<tau>" using H 1591proof (nominal_induct "D @ TVarB X Q # G" t T avoiding: X P arbitrary: D rule: typing.strong_induct) 1592 case (T_Var x T X P D') 1593 have "G\<turnstile>P<:Q" by fact 1594 then have "P closed_in G" using subtype_implies_closed by auto 1595 moreover note \<open>\<turnstile> (D' @ TVarB X Q # G) ok\<close> 1596 ultimately have "\<turnstile> (D'[X \<mapsto> P]\<^sub>e @ G) ok" using valid_subst by auto 1597 moreover note \<open>VarB x T \<in> set (D' @ TVarB X Q # G)\<close> 1598 then have "VarB x T \<in> set D' \<or> VarB x T \<in> set G" by simp 1599 then have "(VarB x (T[X \<mapsto> P]\<^sub>\<tau>)) \<in> set (D'[X \<mapsto> P]\<^sub>e @ G)" 1600 proof 1601 assume "VarB x T \<in> set D'" 1602 then have "VarB x (T[X \<mapsto> P]\<^sub>\<tau>) \<in> set (D'[X \<mapsto> P]\<^sub>e)" 1603 by (rule ctxt_subst_mem_VarB) 1604 then show ?thesis by simp 1605 next 1606 assume x: "VarB x T \<in> set G" 1607 from T_Var have ok: "\<turnstile> G ok" by (auto dest: subtype_implies_ok) 1608 then have "X \<sharp> ty_dom G" using T_Var by (auto dest: validE_append) 1609 with ok have "X \<sharp> G" by (simp add: valid_ty_dom_fresh) 1610 moreover from x have "VarB x T \<in> set (D' @ G)" by simp 1611 then have "VarB x (T[X \<mapsto> P]\<^sub>\<tau>) \<in> set ((D' @ G)[X \<mapsto> P]\<^sub>e)" 1612 by (rule ctxt_subst_mem_VarB) 1613 ultimately show ?thesis 1614 by (simp add: ctxt_subst_append ctxt_subst_identity) 1615 qed 1616 ultimately show ?case by auto 1617next 1618 case (T_App t1 T1 T2 t2 X P D') 1619 then have "D'[X \<mapsto> P]\<^sub>e @ G \<turnstile> t1[X \<mapsto>\<^sub>\<tau> P] : (T1 \<rightarrow> T2)[X \<mapsto> P]\<^sub>\<tau>" by auto 1620 moreover from T_App have "D'[X \<mapsto> P]\<^sub>e @ G \<turnstile> t2[X \<mapsto>\<^sub>\<tau> P] : T1[X \<mapsto> P]\<^sub>\<tau>" by auto 1621 ultimately show ?case by auto 1622next 1623 case (T_Abs x T1 t2 T2 X P D') 1624 then show ?case by force 1625next 1626 case (T_Sub t S T X P D') 1627 then show ?case using substT_subtype by force 1628next 1629 case (T_TAbs X' T1 t2 T2 X P D') 1630 then have "X' \<sharp> ty_dom (D' @ TVarB X Q # G)" 1631 and "T1 closed_in (D' @ TVarB X Q # G)" 1632 by (auto dest: typing_ok) 1633 then have "X' \<sharp> T1" by (rule closed_in_fresh) 1634 with T_TAbs show ?case by force 1635next 1636 case (T_TApp X' t1 T2 T11 T12 X P D') 1637 then have "X' \<sharp> ty_dom (D' @ TVarB X Q # G)" 1638 by (simp add: fresh_dom) 1639 moreover from T_TApp have "T11 closed_in (D' @ TVarB X Q # G)" 1640 by (auto dest: subtype_implies_closed) 1641 ultimately have X': "X' \<sharp> T11" by (rule closed_in_fresh) 1642 from T_TApp have "D'[X \<mapsto> P]\<^sub>e @ G \<turnstile> t1[X \<mapsto>\<^sub>\<tau> P] : (\<forall>X'<:T11. T12)[X \<mapsto> P]\<^sub>\<tau>" 1643 by simp 1644 with X' and T_TApp show ?case 1645 by (auto simp add: fresh_atm type_substitution_lemma 1646 fresh_list_append fresh_list_cons 1647 ctxt_subst_fresh' type_subst_fresh subst_trm_ty_fresh 1648 intro: substT_subtype) 1649qed 1650 1651lemma Abs_type: \<comment> \<open>A.13(1)\<close> 1652 assumes H: "\<Gamma> \<turnstile> (\<lambda>x:S. s) : T" 1653 and H': "\<Gamma> \<turnstile> T <: U \<rightarrow> U'" 1654 and H'': "x \<sharp> \<Gamma>" 1655 obtains S' where "\<Gamma> \<turnstile> U <: S" 1656 and "(VarB x S) # \<Gamma> \<turnstile> s : S'" 1657 and "\<Gamma> \<turnstile> S' <: U'" 1658 using H H' H'' 1659proof (nominal_induct \<Gamma> t \<equiv> "\<lambda>x:S. s" T avoiding: x arbitrary: U U' S s rule: typing.strong_induct) 1660 case (T_Abs y T\<^sub>1 \<Gamma> t\<^sub>2 T\<^sub>2) 1661 from \<open>\<Gamma> \<turnstile> T\<^sub>1 \<rightarrow> T\<^sub>2 <: U \<rightarrow> U'\<close> 1662 obtain ty1: "\<Gamma> \<turnstile> U <: S" and ty2: "\<Gamma> \<turnstile> T\<^sub>2 <: U'" using T_Abs 1663 by cases (simp_all add: ty.inject trm.inject alpha fresh_atm) 1664 from T_Abs have "VarB y S # \<Gamma> \<turnstile> [(y, x)] \<bullet> s : T\<^sub>2" 1665 by (simp add: trm.inject alpha fresh_atm) 1666 then have "[(y, x)] \<bullet> (VarB y S # \<Gamma>) \<turnstile> [(y, x)] \<bullet> [(y, x)] \<bullet> s : [(y, x)] \<bullet> T\<^sub>2" 1667 by (rule typing.eqvt) 1668 moreover from T_Abs have "y \<sharp> \<Gamma>" 1669 by (auto dest!: typing_ok simp add: fresh_trm_dom) 1670 ultimately have "VarB x S # \<Gamma> \<turnstile> s : T\<^sub>2" using T_Abs 1671 by (perm_simp add: ty_vrs_prm_simp) 1672 with ty1 show ?case using ty2 by (rule T_Abs) 1673next 1674 case (T_Sub \<Gamma> t S T) 1675 then show ?case using subtype_transitivity by blast 1676qed simp_all 1677 1678lemma subtype_reflexivity_from_typing: 1679 assumes "\<Gamma> \<turnstile> t : T" 1680 shows "\<Gamma> \<turnstile> T <: T" 1681using assms subtype_reflexivity typing_ok typing_closed_in by simp 1682 1683lemma Abs_type': 1684 assumes H: "\<Gamma> \<turnstile> (\<lambda>x:S. s) : U \<rightarrow> U'" 1685 and H': "x \<sharp> \<Gamma>" 1686 obtains S' 1687 where "\<Gamma> \<turnstile> U <: S" 1688 and "(VarB x S) # \<Gamma> \<turnstile> s : S'" 1689 and "\<Gamma> \<turnstile> S' <: U'" 1690 using H subtype_reflexivity_from_typing [OF H] H' 1691 by (rule Abs_type) 1692 1693lemma TAbs_type: \<comment> \<open>A.13(2)\<close> 1694 assumes H: "\<Gamma> \<turnstile> (\<lambda>X<:S. s) : T" 1695 and H': "\<Gamma> \<turnstile> T <: (\<forall>X<:U. U')" 1696 and fresh: "X \<sharp> \<Gamma>" "X \<sharp> S" "X \<sharp> U" 1697 obtains S' 1698 where "\<Gamma> \<turnstile> U <: S" 1699 and "(TVarB X U # \<Gamma>) \<turnstile> s : S'" 1700 and "(TVarB X U # \<Gamma>) \<turnstile> S' <: U'" 1701 using H H' fresh 1702proof (nominal_induct \<Gamma> t \<equiv> "\<lambda>X<:S. s" T avoiding: X U U' S arbitrary: s rule: typing.strong_induct) 1703 case (T_TAbs Y T\<^sub>1 \<Gamma> t\<^sub>2 T\<^sub>2) 1704 from \<open>TVarB Y T\<^sub>1 # \<Gamma> \<turnstile> t\<^sub>2 : T\<^sub>2\<close> have Y: "Y \<sharp> \<Gamma>" 1705 by (auto dest!: typing_ok simp add: valid_ty_dom_fresh) 1706 from \<open>Y \<sharp> U'\<close> and \<open>Y \<sharp> X\<close> 1707 have "(\<forall>X<:U. U') = (\<forall>Y<:U. [(Y, X)] \<bullet> U')" 1708 by (simp add: ty.inject alpha' fresh_atm) 1709 with T_TAbs have "\<Gamma> \<turnstile> (\<forall>Y<:S. T\<^sub>2) <: (\<forall>Y<:U. [(Y, X)] \<bullet> U')" by (simp add: trm.inject) 1710 then obtain ty1: "\<Gamma> \<turnstile> U <: S" and ty2: "(TVarB Y U # \<Gamma>) \<turnstile> T\<^sub>2 <: ([(Y, X)] \<bullet> U')" using T_TAbs Y 1711 by (cases rule: subtype_of.strong_cases [where X=Y]) (simp_all add: ty.inject alpha abs_fresh) 1712 note ty1 1713 moreover from T_TAbs have "TVarB Y S # \<Gamma> \<turnstile> ([(Y, X)] \<bullet> s) : T\<^sub>2" 1714 by (simp add: trm.inject alpha fresh_atm) 1715 then have "[(Y, X)] \<bullet> (TVarB Y S # \<Gamma>) \<turnstile> [(Y, X)] \<bullet> [(Y, X)] \<bullet> s : [(Y, X)] \<bullet> T\<^sub>2" 1716 by (rule typing.eqvt) 1717 with \<open>X \<sharp> \<Gamma>\<close> \<open>X \<sharp> S\<close> Y \<open>Y \<sharp> S\<close> have "TVarB X S # \<Gamma> \<turnstile> s : [(Y, X)] \<bullet> T\<^sub>2" 1718 by perm_simp 1719 then have "TVarB X U # \<Gamma> \<turnstile> s : [(Y, X)] \<bullet> T\<^sub>2" using ty1 1720 by (rule narrow_type [of "[]", simplified]) 1721 moreover from ty2 have "([(Y, X)] \<bullet> (TVarB Y U # \<Gamma>)) \<turnstile> ([(Y, X)] \<bullet> T\<^sub>2) <: ([(Y, X)] \<bullet> [(Y, X)] \<bullet> U')" 1722 by (rule subtype_of.eqvt) 1723 with \<open>X \<sharp> \<Gamma>\<close> \<open>X \<sharp> U\<close> Y \<open>Y \<sharp> U\<close> have "(TVarB X U # \<Gamma>) \<turnstile> ([(Y, X)] \<bullet> T\<^sub>2) <: U'" 1724 by perm_simp 1725 ultimately show ?case by (rule T_TAbs) 1726next 1727 case (T_Sub \<Gamma> t S T) 1728 then show ?case using subtype_transitivity by blast 1729qed simp_all 1730 1731lemma TAbs_type': 1732 assumes H: "\<Gamma> \<turnstile> (\<lambda>X<:S. s) : (\<forall>X<:U. U')" 1733 and fresh: "X \<sharp> \<Gamma>" "X \<sharp> S" "X \<sharp> U" 1734 obtains S' 1735 where "\<Gamma> \<turnstile> U <: S" 1736 and "(TVarB X U # \<Gamma>) \<turnstile> s : S'" 1737 and "(TVarB X U # \<Gamma>) \<turnstile> S' <: U'" 1738 using H subtype_reflexivity_from_typing [OF H] fresh 1739 by (rule TAbs_type) 1740 1741theorem preservation: \<comment> \<open>A.20\<close> 1742 assumes H: "\<Gamma> \<turnstile> t : T" 1743 shows "t \<longmapsto> t' \<Longrightarrow> \<Gamma> \<turnstile> t' : T" using H 1744proof (nominal_induct avoiding: t' rule: typing.strong_induct) 1745 case (T_App \<Gamma> t\<^sub>1 T\<^sub>11 T\<^sub>12 t\<^sub>2 t') 1746 obtain x::vrs where x_fresh: "x \<sharp> (\<Gamma>, t\<^sub>1 \<cdot> t\<^sub>2, t')" 1747 by (rule exists_fresh) (rule fin_supp) 1748 obtain X::tyvrs where "X \<sharp> (t\<^sub>1 \<cdot> t\<^sub>2, t')" 1749 by (rule exists_fresh) (rule fin_supp) 1750 with \<open>t\<^sub>1 \<cdot> t\<^sub>2 \<longmapsto> t'\<close> show ?case 1751 proof (cases rule: eval.strong_cases [where x=x and X=X]) 1752 case (E_Abs v\<^sub>2 T\<^sub>11' t\<^sub>12) 1753 with T_App and x_fresh have h: "\<Gamma> \<turnstile> (\<lambda>x:T\<^sub>11'. t\<^sub>12) : T\<^sub>11 \<rightarrow> T\<^sub>12" 1754 by (simp add: trm.inject fresh_prod) 1755 moreover from x_fresh have "x \<sharp> \<Gamma>" by simp 1756 ultimately obtain S' 1757 where T\<^sub>11: "\<Gamma> \<turnstile> T\<^sub>11 <: T\<^sub>11'" 1758 and t\<^sub>12: "(VarB x T\<^sub>11') # \<Gamma> \<turnstile> t\<^sub>12 : S'" 1759 and S': "\<Gamma> \<turnstile> S' <: T\<^sub>12" 1760 by (rule Abs_type') blast 1761 from \<open>\<Gamma> \<turnstile> t\<^sub>2 : T\<^sub>11\<close> 1762 have "\<Gamma> \<turnstile> t\<^sub>2 : T\<^sub>11'" using T\<^sub>11 by (rule T_Sub) 1763 with t\<^sub>12 have "\<Gamma> \<turnstile> t\<^sub>12[x \<mapsto> t\<^sub>2] : S'" 1764 by (rule subst_type [where \<Delta>="[]", simplified]) 1765 hence "\<Gamma> \<turnstile> t\<^sub>12[x \<mapsto> t\<^sub>2] : T\<^sub>12" using S' by (rule T_Sub) 1766 with E_Abs and x_fresh show ?thesis by (simp add: trm.inject fresh_prod) 1767 next 1768 case (E_App1 t''' t'' u) 1769 hence "t\<^sub>1 \<longmapsto> t''" by (simp add:trm.inject) 1770 hence "\<Gamma> \<turnstile> t'' : T\<^sub>11 \<rightarrow> T\<^sub>12" by (rule T_App) 1771 hence "\<Gamma> \<turnstile> t'' \<cdot> t\<^sub>2 : T\<^sub>12" using \<open>\<Gamma> \<turnstile> t\<^sub>2 : T\<^sub>11\<close> 1772 by (rule typing.T_App) 1773 with E_App1 show ?thesis by (simp add:trm.inject) 1774 next 1775 case (E_App2 v t''' t'') 1776 hence "t\<^sub>2 \<longmapsto> t''" by (simp add:trm.inject) 1777 hence "\<Gamma> \<turnstile> t'' : T\<^sub>11" by (rule T_App) 1778 with T_App(1) have "\<Gamma> \<turnstile> t\<^sub>1 \<cdot> t'' : T\<^sub>12" 1779 by (rule typing.T_App) 1780 with E_App2 show ?thesis by (simp add:trm.inject) 1781 qed (simp_all add: fresh_prod) 1782next 1783 case (T_TApp X \<Gamma> t\<^sub>1 T\<^sub>2 T\<^sub>11 T\<^sub>12 t') 1784 obtain x::vrs where "x \<sharp> (t\<^sub>1 \<cdot>\<^sub>\<tau> T\<^sub>2, t')" 1785 by (rule exists_fresh) (rule fin_supp) 1786 with \<open>t\<^sub>1 \<cdot>\<^sub>\<tau> T\<^sub>2 \<longmapsto> t'\<close> 1787 show ?case 1788 proof (cases rule: eval.strong_cases [where X=X and x=x]) 1789 case (E_TAbs T\<^sub>11' T\<^sub>2' t\<^sub>12) 1790 with T_TApp have "\<Gamma> \<turnstile> (\<lambda>X<:T\<^sub>11'. t\<^sub>12) : (\<forall>X<:T\<^sub>11. T\<^sub>12)" and "X \<sharp> \<Gamma>" and "X \<sharp> T\<^sub>11'" 1791 by (simp_all add: trm.inject) 1792 moreover from \<open>\<Gamma>\<turnstile>T\<^sub>2<:T\<^sub>11\<close> and \<open>X \<sharp> \<Gamma>\<close> have "X \<sharp> T\<^sub>11" 1793 by (blast intro: closed_in_fresh fresh_dom dest: subtype_implies_closed) 1794 ultimately obtain S' 1795 where "TVarB X T\<^sub>11 # \<Gamma> \<turnstile> t\<^sub>12 : S'" 1796 and "(TVarB X T\<^sub>11 # \<Gamma>) \<turnstile> S' <: T\<^sub>12" 1797 by (rule TAbs_type') blast 1798 hence "TVarB X T\<^sub>11 # \<Gamma> \<turnstile> t\<^sub>12 : T\<^sub>12" by (rule T_Sub) 1799 hence "\<Gamma> \<turnstile> t\<^sub>12[X \<mapsto>\<^sub>\<tau> T\<^sub>2] : T\<^sub>12[X \<mapsto> T\<^sub>2]\<^sub>\<tau>" using \<open>\<Gamma> \<turnstile> T\<^sub>2 <: T\<^sub>11\<close> 1800 by (rule substT_type [where D="[]", simplified]) 1801 with T_TApp and E_TAbs show ?thesis by (simp add: trm.inject) 1802 next 1803 case (E_TApp t''' t'' T) 1804 from E_TApp have "t\<^sub>1 \<longmapsto> t''" by (simp add: trm.inject) 1805 then have "\<Gamma> \<turnstile> t'' : (\<forall>X<:T\<^sub>11. T\<^sub>12)" by (rule T_TApp) 1806 then have "\<Gamma> \<turnstile> t'' \<cdot>\<^sub>\<tau> T\<^sub>2 : T\<^sub>12[X \<mapsto> T\<^sub>2]\<^sub>\<tau>" using \<open>\<Gamma> \<turnstile> T\<^sub>2 <: T\<^sub>11\<close> 1807 by (rule better_T_TApp) 1808 with E_TApp show ?thesis by (simp add: trm.inject) 1809 qed (simp_all add: fresh_prod) 1810next 1811 case (T_Sub \<Gamma> t S T t') 1812 have "t \<longmapsto> t'" by fact 1813 hence "\<Gamma> \<turnstile> t' : S" by (rule T_Sub) 1814 moreover have "\<Gamma> \<turnstile> S <: T" by fact 1815 ultimately show ?case by (rule typing.T_Sub) 1816qed (auto) 1817 1818lemma Fun_canonical: \<comment> \<open>A.14(1)\<close> 1819 assumes ty: "[] \<turnstile> v : T\<^sub>1 \<rightarrow> T\<^sub>2" 1820 shows "val v \<Longrightarrow> \<exists>x t S. v = (\<lambda>x:S. t)" using ty 1821proof (induct "[]::env" v "T\<^sub>1 \<rightarrow> T\<^sub>2" arbitrary: T\<^sub>1 T\<^sub>2) 1822 case (T_Sub t S) 1823 from \<open>[] \<turnstile> S <: T\<^sub>1 \<rightarrow> T\<^sub>2\<close> 1824 obtain S\<^sub>1 S\<^sub>2 where S: "S = S\<^sub>1 \<rightarrow> S\<^sub>2" 1825 by cases (auto simp add: T_Sub) 1826 then show ?case using \<open>val t\<close> by (rule T_Sub) 1827qed (auto) 1828 1829lemma TyAll_canonical: \<comment> \<open>A.14(3)\<close> 1830 fixes X::tyvrs 1831 assumes ty: "[] \<turnstile> v : (\<forall>X<:T\<^sub>1. T\<^sub>2)" 1832 shows "val v \<Longrightarrow> \<exists>X t S. v = (\<lambda>X<:S. t)" using ty 1833proof (induct "[]::env" v "\<forall>X<:T\<^sub>1. T\<^sub>2" arbitrary: X T\<^sub>1 T\<^sub>2) 1834 case (T_Sub t S) 1835 from \<open>[] \<turnstile> S <: (\<forall>X<:T\<^sub>1. T\<^sub>2)\<close> 1836 obtain X S\<^sub>1 S\<^sub>2 where S: "S = (\<forall>X<:S\<^sub>1. S\<^sub>2)" 1837 by cases (auto simp add: T_Sub) 1838 then show ?case using T_Sub by auto 1839qed (auto) 1840 1841theorem progress: 1842 assumes "[] \<turnstile> t : T" 1843 shows "val t \<or> (\<exists>t'. t \<longmapsto> t')" 1844using assms 1845proof (induct "[]::env" t T) 1846 case (T_App t\<^sub>1 T\<^sub>11 T\<^sub>12 t\<^sub>2) 1847 hence "val t\<^sub>1 \<or> (\<exists>t'. t\<^sub>1 \<longmapsto> t')" by simp 1848 thus ?case 1849 proof 1850 assume t\<^sub>1_val: "val t\<^sub>1" 1851 with T_App obtain x t3 S where t\<^sub>1: "t\<^sub>1 = (\<lambda>x:S. t3)" 1852 by (auto dest!: Fun_canonical) 1853 from T_App have "val t\<^sub>2 \<or> (\<exists>t'. t\<^sub>2 \<longmapsto> t')" by simp 1854 thus ?case 1855 proof 1856 assume "val t\<^sub>2" 1857 with t\<^sub>1 have "t\<^sub>1 \<cdot> t\<^sub>2 \<longmapsto> t3[x \<mapsto> t\<^sub>2]" by auto 1858 thus ?case by auto 1859 next 1860 assume "\<exists>t'. t\<^sub>2 \<longmapsto> t'" 1861 then obtain t' where "t\<^sub>2 \<longmapsto> t'" by auto 1862 with t\<^sub>1_val have "t\<^sub>1 \<cdot> t\<^sub>2 \<longmapsto> t\<^sub>1 \<cdot> t'" by auto 1863 thus ?case by auto 1864 qed 1865 next 1866 assume "\<exists>t'. t\<^sub>1 \<longmapsto> t'" 1867 then obtain t' where "t\<^sub>1 \<longmapsto> t'" by auto 1868 hence "t\<^sub>1 \<cdot> t\<^sub>2 \<longmapsto> t' \<cdot> t\<^sub>2" by auto 1869 thus ?case by auto 1870 qed 1871next 1872 case (T_TApp X t\<^sub>1 T\<^sub>2 T\<^sub>11 T\<^sub>12) 1873 hence "val t\<^sub>1 \<or> (\<exists>t'. t\<^sub>1 \<longmapsto> t')" by simp 1874 thus ?case 1875 proof 1876 assume "val t\<^sub>1" 1877 with T_TApp obtain x t S where "t\<^sub>1 = (\<lambda>x<:S. t)" 1878 by (auto dest!: TyAll_canonical) 1879 hence "t\<^sub>1 \<cdot>\<^sub>\<tau> T\<^sub>2 \<longmapsto> t[x \<mapsto>\<^sub>\<tau> T\<^sub>2]" by auto 1880 thus ?case by auto 1881 next 1882 assume "\<exists>t'. t\<^sub>1 \<longmapsto> t'" thus ?case by auto 1883 qed 1884qed (auto) 1885 1886end 1887