(*<*) theory Fsub imports "HOL-Nominal.Nominal" begin (*>*) text‹Authors: Christian Urban, Benjamin Pierce, Dimitrios Vytiniotis Stephanie Weirich Steve Zdancewic Julien Narboux Stefan Berghofer with great help from Markus Wenzel.› section ‹Types for Names, Nominal Datatype Declaration for Types and Terms› no_syntax "_Map" :: "maplets => 'a ⇀ 'b" ("(1[_])") text ‹The main point of this solution is to use names everywhere (be they bound, binding or free). In System \FSUB{} there are two kinds of names corresponding to type-variables and to term-variables. These two kinds of names are represented in the nominal datatype package as atom-types ‹tyvrs› and ‹vrs›:› atom_decl tyvrs vrs text‹There are numerous facts that come with this declaration: for example that there are infinitely many elements in ‹tyvrs› and ‹vrs›.› text‹The constructors for types and terms in System \FSUB{} contain abstractions over type-variables and term-variables. The nominal datatype package uses ‹«…»…› to indicate where abstractions occur.› nominal_datatype ty = Tvar "tyvrs" | Top | Arrow "ty" "ty" (infixr "→" 200) | Forall "«tyvrs»ty" "ty" nominal_datatype trm = Var "vrs" | Abs "«vrs»trm" "ty" | TAbs "«tyvrs»trm" "ty" | App "trm" "trm" (infixl "⋅" 200) | TApp "trm" "ty" (infixl "⋅⇩_{τ}" 200) text ‹To be polite to the eye, some more familiar notation is introduced. Because of the change in the order of arguments, one needs to use translation rules, instead of syntax annotations at the term-constructors as given above for @{term "Arrow"}.› abbreviation Forall_syn :: "tyvrs ⇒ ty ⇒ ty ⇒ ty" ("(3∀_<:_./ _)" [0, 0, 10] 10) where "∀X<:T⇩_{1}. T⇩_{2}≡ ty.Forall X T⇩_{2}T⇩_{1}" abbreviation Abs_syn :: "vrs ⇒ ty ⇒ trm ⇒ trm" ("(3λ_:_./ _)" [0, 0, 10] 10) where "λx:T. t ≡ trm.Abs x t T" abbreviation TAbs_syn :: "tyvrs ⇒ ty ⇒ trm ⇒ trm" ("(3λ_<:_./ _)" [0, 0, 10] 10) where "λX<:T. t ≡ trm.TAbs X t T" text ‹Again there are numerous facts that are proved automatically for @{typ "ty"} and @{typ "trm"}: for example that the set of free variables, i.e.~the ‹support›, is finite. However note that nominal-datatype declarations do \emph{not} define ``classical" constructor-based datatypes, but rather define $\alpha$-equivalence classes---we can for example show that $\alpha$-equivalent @{typ "ty"}s and @{typ "trm"}s are equal:› lemma alpha_illustration: shows "(∀X<:T. Tvar X) = (∀Y<:T. Tvar Y)" and "(λx:T. Var x) = (λy:T. Var y)" by (simp_all add: ty.inject trm.inject alpha calc_atm fresh_atm) section ‹SubTyping Contexts› nominal_datatype binding = VarB vrs ty | TVarB tyvrs ty type_synonym env = "binding list" text ‹Typing contexts are represented as lists that ``grow" on the left; we thereby deviating from the convention in the POPLmark-paper. The lists contain pairs of type-variables and types (this is sufficient for Part 1A).› text ‹In order to state validity-conditions for typing-contexts, the notion of a ‹dom› of a typing-context is handy.› nominal_primrec "tyvrs_of" :: "binding ⇒ tyvrs set" where "tyvrs_of (VarB x y) = {}" | "tyvrs_of (TVarB x y) = {x}" by auto nominal_primrec "vrs_of" :: "binding ⇒ vrs set" where "vrs_of (VarB x y) = {x}" | "vrs_of (TVarB x y) = {}" by auto primrec "ty_dom" :: "env ⇒ tyvrs set" where "ty_dom [] = {}" | "ty_dom (X#Γ) = (tyvrs_of X)∪(ty_dom Γ)" primrec "trm_dom" :: "env ⇒ vrs set" where "trm_dom [] = {}" | "trm_dom (X#Γ) = (vrs_of X)∪(trm_dom Γ)" lemma vrs_of_eqvt[eqvt]: fixes pi ::"tyvrs prm" and pi'::"vrs prm" shows "pi ∙(tyvrs_of x) = tyvrs_of (pi∙x)" and "pi'∙(tyvrs_of x) = tyvrs_of (pi'∙x)" and "pi ∙(vrs_of x) = vrs_of (pi∙x)" and "pi'∙(vrs_of x) = vrs_of (pi'∙x)" by (nominal_induct x rule: binding.strong_induct) (simp_all add: tyvrs_of.simps eqvts) lemma doms_eqvt[eqvt]: fixes pi::"tyvrs prm" and pi'::"vrs prm" shows "pi ∙(ty_dom Γ) = ty_dom (pi∙Γ)" and "pi'∙(ty_dom Γ) = ty_dom (pi'∙Γ)" and "pi ∙(trm_dom Γ) = trm_dom (pi∙Γ)" and "pi'∙(trm_dom Γ) = trm_dom (pi'∙Γ)" by (induct Γ) (simp_all add: eqvts) lemma finite_vrs: shows "finite (tyvrs_of x)" and "finite (vrs_of x)" by (nominal_induct rule:binding.strong_induct) auto lemma finite_doms: shows "finite (ty_dom Γ)" and "finite (trm_dom Γ)" by (induct Γ) (auto simp add: finite_vrs) lemma ty_dom_supp: shows "(supp (ty_dom Γ)) = (ty_dom Γ)" and "(supp (trm_dom Γ)) = (trm_dom Γ)" by (simp only: at_fin_set_supp at_tyvrs_inst at_vrs_inst finite_doms)+ lemma ty_dom_inclusion: assumes a: "(TVarB X T)∈set Γ" shows "X∈(ty_dom Γ)" using a by (induct Γ) (auto) lemma ty_binding_existence: assumes "X ∈ (tyvrs_of a)" shows "∃T.(TVarB X T=a)" using assms by (nominal_induct a rule: binding.strong_induct) (auto) lemma ty_dom_existence: assumes a: "X∈(ty_dom Γ)" shows "∃T.(TVarB X T)∈set Γ" using a apply (induct Γ, auto) apply (rename_tac a Γ') apply (subgoal_tac "∃T.(TVarB X T=a)") apply (auto) apply (auto simp add: ty_binding_existence) done lemma doms_append: shows "ty_dom (Γ@Δ) = ((ty_dom Γ) ∪ (ty_dom Δ))" and "trm_dom (Γ@Δ) = ((trm_dom Γ) ∪ (trm_dom Δ))" by (induct Γ) (auto) lemma ty_vrs_prm_simp: fixes pi::"vrs prm" and S::"ty" shows "pi∙S = S" by (induct S rule: ty.induct) (auto simp add: calc_atm) lemma fresh_ty_dom_cons: fixes X::"tyvrs" shows "X♯(ty_dom (Y#Γ)) = (X♯(tyvrs_of Y) ∧ X♯(ty_dom Γ))" apply (nominal_induct rule:binding.strong_induct) apply (auto) apply (simp add: fresh_def supp_def eqvts) apply (simp add: fresh_fin_insert [OF pt_tyvrs_inst at_tyvrs_inst fs_tyvrs_inst] finite_doms) apply (simp add: fresh_def supp_def eqvts) apply (simp add: fresh_fin_insert [OF pt_tyvrs_inst at_tyvrs_inst fs_tyvrs_inst] finite_doms)+ done lemma tyvrs_fresh: fixes X::"tyvrs" assumes "X ♯ a" shows "X ♯ tyvrs_of a" and "X ♯ vrs_of a" using assms apply (nominal_induct a rule:binding.strong_induct) apply (auto) apply (fresh_guess)+ done lemma fresh_dom: fixes X::"tyvrs" assumes a: "X♯Γ" shows "X♯(ty_dom Γ)" using a apply(induct Γ) apply(simp add: fresh_set_empty) apply(simp only: fresh_ty_dom_cons) apply(auto simp add: fresh_prod fresh_list_cons tyvrs_fresh) done text ‹Not all lists of type @{typ "env"} are well-formed. One condition requires that in @{term "TVarB X S#Γ"} all free variables of @{term "S"} must be in the @{term "ty_dom"} of @{term "Γ"}, that is @{term "S"} must be ‹closed› in @{term "Γ"}. The set of free variables of @{term "S"} is the ‹support› of @{term "S"}.› definition "closed_in" :: "ty ⇒ env ⇒ bool" ("_ closed'_in _" [100,100] 100) where "S closed_in Γ ≡ (supp S)⊆(ty_dom Γ)" lemma closed_in_eqvt[eqvt]: fixes pi::"tyvrs prm" assumes a: "S closed_in Γ" shows "(pi∙S) closed_in (pi∙Γ)" using a proof - from a have "pi∙(S closed_in Γ)" by (simp add: perm_bool) then show "(pi∙S) closed_in (pi∙Γ)" by (simp add: closed_in_def eqvts) qed lemma tyvrs_vrs_prm_simp: fixes pi::"vrs prm" shows "tyvrs_of (pi∙a) = tyvrs_of a" apply (nominal_induct rule:binding.strong_induct) apply (simp_all add: eqvts) apply (simp add: dj_perm_forget[OF dj_tyvrs_vrs]) done lemma ty_vrs_fresh: fixes x::"vrs" and T::"ty" shows "x ♯ T" by (simp add: fresh_def supp_def ty_vrs_prm_simp) lemma ty_dom_vrs_prm_simp: fixes pi::"vrs prm" and Γ::"env" shows "(ty_dom (pi∙Γ)) = (ty_dom Γ)" apply(induct Γ) apply (simp add: eqvts) apply(simp add: tyvrs_vrs_prm_simp) done lemma closed_in_eqvt'[eqvt]: fixes pi::"vrs prm" assumes a: "S closed_in Γ" shows "(pi∙S) closed_in (pi∙Γ)" using a by (simp add: closed_in_def ty_dom_vrs_prm_simp ty_vrs_prm_simp) lemma fresh_vrs_of: fixes x::"vrs" shows "x♯vrs_of b = x♯b" by (nominal_induct b rule: binding.strong_induct) (simp_all add: fresh_singleton fresh_set_empty ty_vrs_fresh fresh_atm) lemma fresh_trm_dom: fixes x::"vrs" shows "x♯ trm_dom Γ = x♯Γ" by (induct Γ) (simp_all add: fresh_set_empty fresh_list_cons fresh_fin_union [OF pt_vrs_inst at_vrs_inst fs_vrs_inst] finite_doms finite_vrs fresh_vrs_of fresh_list_nil) lemma closed_in_fresh: "(X::tyvrs) ♯ ty_dom Γ ⟹ T closed_in Γ ⟹ X ♯ T" by (auto simp add: closed_in_def fresh_def ty_dom_supp) text ‹Now validity of a context is a straightforward inductive definition.› inductive valid_rel :: "env ⇒ bool" ("⊢ _ ok" [100] 100) where valid_nil[simp]: "⊢ [] ok" | valid_consT[simp]: "⟦⊢ Γ ok; X♯(ty_dom Γ); T closed_in Γ⟧ ⟹ ⊢ (TVarB X T#Γ) ok" | valid_cons [simp]: "⟦⊢ Γ ok; x♯(trm_dom Γ); T closed_in Γ⟧ ⟹ ⊢ (VarB x T#Γ) ok" equivariance valid_rel declare binding.inject [simp add] declare trm.inject [simp add] inductive_cases validE[elim]: "⊢ (TVarB X T#Γ) ok" "⊢ (VarB x T#Γ) ok" "⊢ (b#Γ) ok" declare binding.inject [simp del] declare trm.inject [simp del] lemma validE_append: assumes a: "⊢ (Δ@Γ) ok" shows "⊢ Γ ok" using a proof (induct Δ) case (Cons a Γ') then show ?case by (nominal_induct a rule:binding.strong_induct) (auto elim: validE) qed (auto) lemma replace_type: assumes a: "⊢ (Δ@(TVarB X T)#Γ) ok" and b: "S closed_in Γ" shows "⊢ (Δ@(TVarB X S)#Γ) ok" using a b proof(induct Δ) case Nil then show ?case by (auto elim: validE intro: valid_cons simp add: doms_append closed_in_def) next case (Cons a Γ') then show ?case by (nominal_induct a rule:binding.strong_induct) (auto elim: validE intro!: valid_cons simp add: doms_append closed_in_def) qed text ‹Well-formed contexts have a unique type-binding for a type-variable.› lemma uniqueness_of_ctxt: fixes Γ::"env" assumes a: "⊢ Γ ok" and b: "(TVarB X T)∈set Γ" and c: "(TVarB X S)∈set Γ" shows "T=S" using a b c proof (induct) case (valid_consT Γ X' T') moreover { fix Γ'::"env" assume a: "X'♯(ty_dom Γ')" have "¬(∃T.(TVarB X' T)∈(set Γ'))" using a proof (induct Γ') case (Cons Y Γ') thus "¬ (∃T.(TVarB X' T)∈set(Y#Γ'))" by (simp add: fresh_ty_dom_cons fresh_fin_union[OF pt_tyvrs_inst at_tyvrs_inst fs_tyvrs_inst] finite_vrs finite_doms, auto simp add: fresh_atm fresh_singleton) qed (simp) } ultimately show "T=S" by (auto simp add: binding.inject) qed (auto) lemma uniqueness_of_ctxt': fixes Γ::"env" assumes a: "⊢ Γ ok" and b: "(VarB x T)∈set Γ" and c: "(VarB x S)∈set Γ" shows "T=S" using a b c proof (induct) case (valid_cons Γ x' T') moreover { fix Γ'::"env" assume a: "x'♯(trm_dom Γ')" have "¬(∃T.(VarB x' T)∈(set Γ'))" using a proof (induct Γ') case (Cons y Γ') thus "¬ (∃T.(VarB x' T)∈set(y#Γ'))" by (simp add: fresh_fin_union[OF pt_vrs_inst at_vrs_inst fs_vrs_inst] finite_vrs finite_doms, auto simp add: fresh_atm fresh_singleton) qed (simp) } ultimately show "T=S" by (auto simp add: binding.inject) qed (auto) section ‹Size and Capture-Avoiding Substitution for Types› nominal_primrec size_ty :: "ty ⇒ nat" where "size_ty (Tvar X) = 1" | "size_ty (Top) = 1" | "size_ty (T1 → T2) = (size_ty T1) + (size_ty T2) + 1" | "X ♯ T1 ⟹ size_ty (∀X<:T1. T2) = (size_ty T1) + (size_ty T2) + 1" apply (finite_guess)+ apply (rule TrueI)+ apply (simp add: fresh_nat) apply (fresh_guess)+ done nominal_primrec subst_ty :: "ty ⇒ tyvrs ⇒ ty ⇒ ty" ("_[_ ↦ _]⇩_{τ}" [300, 0, 0] 300) where "(Tvar X)[Y ↦ T]⇩_{τ}= (if X=Y then T else Tvar X)" | "(Top)[Y ↦ T]⇩_{τ}= Top" | "(T⇩_{1}→ T⇩_{2})[Y ↦ T]⇩_{τ}= T⇩_{1}[Y ↦ T]⇩_{τ}→ T⇩_{2}[Y ↦ T]⇩_{τ}" | "X♯(Y,T,T⇩_{1}) ⟹ (∀X<:T⇩_{1}. T⇩_{2})[Y ↦ T]⇩_{τ}= (∀X<:T⇩_{1}[Y ↦ T]⇩_{τ}. T⇩_{2}[Y ↦ T]⇩_{τ})" apply (finite_guess)+ apply (rule TrueI)+ apply (simp add: abs_fresh) apply (fresh_guess)+ done lemma subst_eqvt[eqvt]: fixes pi::"tyvrs prm" and T::"ty" shows "pi∙(T[X ↦ T']⇩_{τ}) = (pi∙T)[(pi∙X) ↦ (pi∙T')]⇩_{τ}" by (nominal_induct T avoiding: X T' rule: ty.strong_induct) (perm_simp add: fresh_bij)+ lemma subst_eqvt'[eqvt]: fixes pi::"vrs prm" and T::"ty" shows "pi∙(T[X ↦ T']⇩_{τ}) = (pi∙T)[(pi∙X) ↦ (pi∙T')]⇩_{τ}" by (nominal_induct T avoiding: X T' rule: ty.strong_induct) (perm_simp add: fresh_left)+ lemma type_subst_fresh: fixes X::"tyvrs" assumes "X♯T" and "X♯P" shows "X♯T[Y ↦ P]⇩_{τ}" using assms by (nominal_induct T avoiding: X Y P rule:ty.strong_induct) (auto simp add: abs_fresh) lemma fresh_type_subst_fresh: assumes "X♯T'" shows "X♯T[X ↦ T']⇩_{τ}" using assms by (nominal_induct T avoiding: X T' rule: ty.strong_induct) (auto simp add: fresh_atm abs_fresh fresh_nat) lemma type_subst_identity: "X♯T ⟹ T[X ↦ U]⇩_{τ}= T" by (nominal_induct T avoiding: X U rule: ty.strong_induct) (simp_all add: fresh_atm abs_fresh) lemma type_substitution_lemma: "X ≠ Y ⟹ X♯L ⟹ M[X ↦ N]⇩_{τ}[Y ↦ L]⇩_{τ}= M[Y ↦ L]⇩_{τ}[X ↦ N[Y ↦ L]⇩_{τ}]⇩_{τ}" by (nominal_induct M avoiding: X Y N L rule: ty.strong_induct) (auto simp add: type_subst_fresh type_subst_identity) lemma type_subst_rename: "Y♯T ⟹ ([(Y,X)]∙T)[Y ↦ U]⇩_{τ}= T[X ↦ U]⇩_{τ}" by (nominal_induct T avoiding: X Y U rule: ty.strong_induct) (simp_all add: fresh_atm calc_atm abs_fresh fresh_aux) nominal_primrec subst_tyb :: "binding ⇒ tyvrs ⇒ ty ⇒ binding" ("_[_ ↦ _]⇩_{b}" [100,100,100] 100) where "(TVarB X U)[Y ↦ T]⇩_{b}= TVarB X (U[Y ↦ T]⇩_{τ})" | "(VarB X U)[Y ↦ T]⇩_{b}= VarB X (U[Y ↦ T]⇩_{τ})" by auto lemma binding_subst_fresh: fixes X::"tyvrs" assumes "X♯a" and "X♯P" shows "X♯a[Y ↦ P]⇩_{b}" using assms by (nominal_induct a rule: binding.strong_induct) (auto simp add: type_subst_fresh) lemma binding_subst_identity: shows "X♯B ⟹ B[X ↦ U]⇩_{b}= B" by (induct B rule: binding.induct) (simp_all add: fresh_atm type_subst_identity) primrec subst_tyc :: "env ⇒ tyvrs ⇒ ty ⇒ env" ("_[_ ↦ _]⇩_{e}" [100,100,100] 100) where "([])[Y ↦ T]⇩_{e}= []" | "(B#Γ)[Y ↦ T]⇩_{e}= (B[Y ↦ T]⇩_{b})#(Γ[Y ↦ T]⇩_{e})" lemma ctxt_subst_fresh': fixes X::"tyvrs" assumes "X♯Γ" and "X♯P" shows "X♯Γ[Y ↦ P]⇩_{e}" using assms by (induct Γ) (auto simp add: fresh_list_cons binding_subst_fresh) lemma ctxt_subst_mem_TVarB: "TVarB X T ∈ set Γ ⟹ TVarB X (T[Y ↦ U]⇩_{τ}) ∈ set (Γ[Y ↦ U]⇩_{e})" by (induct Γ) auto lemma ctxt_subst_mem_VarB: "VarB x T ∈ set Γ ⟹ VarB x (T[Y ↦ U]⇩_{τ}) ∈ set (Γ[Y ↦ U]⇩_{e})" by (induct Γ) auto lemma ctxt_subst_identity: "X♯Γ ⟹ Γ[X ↦ U]⇩_{e}= Γ" by (induct Γ) (simp_all add: fresh_list_cons binding_subst_identity) lemma ctxt_subst_append: "(Δ @ Γ)[X ↦ T]⇩_{e}= Δ[X ↦ T]⇩_{e}@ Γ[X ↦ T]⇩_{e}" by (induct Δ) simp_all nominal_primrec subst_trm :: "trm ⇒ vrs ⇒ trm ⇒ trm" ("_[_ ↦ _]" [300, 0, 0] 300) where "(Var x)[y ↦ t'] = (if x=y then t' else (Var x))" | "(t1 ⋅ t2)[y ↦ t'] = t1[y ↦ t'] ⋅ t2[y ↦ t']" | "(t ⋅⇩_{τ}T)[y ↦ t'] = t[y ↦ t'] ⋅⇩_{τ}T" | "X♯(T,t') ⟹ (λX<:T. t)[y ↦ t'] = (λX<:T. t[y ↦ t'])" | "x♯(y,t') ⟹ (λx:T. t)[y ↦ t'] = (λx:T. t[y ↦ t'])" apply(finite_guess)+ apply(rule TrueI)+ apply(simp add: abs_fresh)+ apply(fresh_guess add: ty_vrs_fresh abs_fresh)+ done lemma subst_trm_fresh_tyvar: fixes X::"tyvrs" shows "X♯t ⟹ X♯u ⟹ X♯t[x ↦ u]" by (nominal_induct t avoiding: x u rule: trm.strong_induct) (auto simp add: trm.fresh abs_fresh) lemma subst_trm_fresh_var: "x♯u ⟹ x♯t[x ↦ u]" by (nominal_induct t avoiding: x u rule: trm.strong_induct) (simp_all add: abs_fresh fresh_atm ty_vrs_fresh) lemma subst_trm_eqvt[eqvt]: fixes pi::"tyvrs prm" and t::"trm" shows "pi∙(t[x ↦ u]) = (pi∙t)[(pi∙x) ↦ (pi∙u)]" by (nominal_induct t avoiding: x u rule: trm.strong_induct) (perm_simp add: fresh_left)+ lemma subst_trm_eqvt'[eqvt]: fixes pi::"vrs prm" and t::"trm" shows "pi∙(t[x ↦ u]) = (pi∙t)[(pi∙x) ↦ (pi∙u)]" by (nominal_induct t avoiding: x u rule: trm.strong_induct) (perm_simp add: fresh_left)+ lemma subst_trm_rename: "y♯t ⟹ ([(y, x)] ∙ t)[y ↦ u] = t[x ↦ u]" by (nominal_induct t avoiding: x y u rule: trm.strong_induct) (simp_all add: fresh_atm calc_atm abs_fresh fresh_aux ty_vrs_fresh perm_fresh_fresh) nominal_primrec (freshness_context: "T2::ty") subst_trm_ty :: "trm ⇒ tyvrs ⇒ ty ⇒ trm" ("_[_ ↦⇩_{τ}_]" [300, 0, 0] 300) where "(Var x)[Y ↦⇩_{τ}T2] = Var x" | "(t1 ⋅ t2)[Y ↦⇩_{τ}T2] = t1[Y ↦⇩_{τ}T2] ⋅ t2[Y ↦⇩_{τ}T2]" | "(t1 ⋅⇩_{τ}T)[Y ↦⇩_{τ}T2] = t1[Y ↦⇩_{τ}T2] ⋅⇩_{τ}T[Y ↦ T2]⇩_{τ}" | "X♯(Y,T,T2) ⟹ (λX<:T. t)[Y ↦⇩_{τ}T2] = (λX<:T[Y ↦ T2]⇩_{τ}. t[Y ↦⇩_{τ}T2])" | "(λx:T. t)[Y ↦⇩_{τ}T2] = (λx:T[Y ↦ T2]⇩_{τ}. t[Y ↦⇩_{τ}T2])" apply(finite_guess)+ apply(rule TrueI)+ apply(simp add: abs_fresh ty_vrs_fresh)+ apply(simp add: type_subst_fresh) apply(fresh_guess add: ty_vrs_fresh abs_fresh)+ done lemma subst_trm_ty_fresh: fixes X::"tyvrs" shows "X♯t ⟹ X♯T ⟹ X♯t[Y ↦⇩_{τ}T]" by (nominal_induct t avoiding: Y T rule: trm.strong_induct) (auto simp add: abs_fresh type_subst_fresh) lemma subst_trm_ty_fresh': "X♯T ⟹ X♯t[X ↦⇩_{τ}T]" by (nominal_induct t avoiding: X T rule: trm.strong_induct) (simp_all add: abs_fresh fresh_type_subst_fresh fresh_atm) lemma subst_trm_ty_eqvt[eqvt]: fixes pi::"tyvrs prm" and t::"trm" shows "pi∙(t[X ↦⇩_{τ}T]) = (pi∙t)[(pi∙X) ↦⇩_{τ}(pi∙T)]" by (nominal_induct t avoiding: X T rule: trm.strong_induct) (perm_simp add: fresh_bij subst_eqvt)+ lemma subst_trm_ty_eqvt'[eqvt]: fixes pi::"vrs prm" and t::"trm" shows "pi∙(t[X ↦⇩_{τ}T]) = (pi∙t)[(pi∙X) ↦⇩_{τ}(pi∙T)]" by (nominal_induct t avoiding: X T rule: trm.strong_induct) (perm_simp add: fresh_left subst_eqvt')+ lemma subst_trm_ty_rename: "Y♯t ⟹ ([(Y, X)] ∙ t)[Y ↦⇩_{τ}U] = t[X ↦⇩_{τ}U]" by (nominal_induct t avoiding: X Y U rule: trm.strong_induct) (simp_all add: fresh_atm calc_atm abs_fresh fresh_aux type_subst_rename) section ‹Subtyping-Relation› text ‹The definition for the subtyping-relation follows quite closely what is written in the POPLmark-paper, except for the premises dealing with well-formed contexts and the freshness constraint @{term "X♯Γ"} in the ‹S_Forall›-rule. (The freshness constraint is specific to the \emph{nominal approach}. Note, however, that the constraint does \emph{not} make the subtyping-relation ``partial"\ldots because we work over $\alpha$-equivalence classes.)› inductive subtype_of :: "env ⇒ ty ⇒ ty ⇒ bool" ("_⊢_<:_" [100,100,100] 100) where SA_Top[intro]: "⟦⊢ Γ ok; S closed_in Γ⟧ ⟹ Γ ⊢ S <: Top" | SA_refl_TVar[intro]: "⟦⊢ Γ ok; X ∈ ty_dom Γ⟧⟹ Γ ⊢ Tvar X <: Tvar X" | SA_trans_TVar[intro]: "⟦(TVarB X S) ∈ set Γ; Γ ⊢ S <: T⟧ ⟹ Γ ⊢ (Tvar X) <: T" | SA_arrow[intro]: "⟦Γ ⊢ T⇩_{1}<: S⇩_{1}; Γ ⊢ S⇩_{2}<: T⇩_{2}⟧ ⟹ Γ ⊢ (S⇩_{1}→ S⇩_{2}) <: (T⇩_{1}→ T⇩_{2})" | SA_all[intro]: "⟦Γ ⊢ T⇩_{1}<: S⇩_{1}; ((TVarB X T⇩_{1})#Γ) ⊢ S⇩_{2}<: T⇩_{2}⟧ ⟹ Γ ⊢ (∀X<:S⇩_{1}. S⇩_{2}) <: (∀X<:T⇩_{1}. T⇩_{2})" lemma subtype_implies_ok: fixes X::"tyvrs" assumes a: "Γ ⊢ S <: T" shows "⊢ Γ ok" using a by (induct) (auto) lemma subtype_implies_closed: assumes a: "Γ ⊢ S <: T" shows "S closed_in Γ ∧ T closed_in Γ" using a proof (induct) case (SA_Top Γ S) have "Top closed_in Γ" by (simp add: closed_in_def ty.supp) moreover have "S closed_in Γ" by fact ultimately show "S closed_in Γ ∧ Top closed_in Γ" by simp next case (SA_trans_TVar X S Γ T) have "(TVarB X S)∈set Γ" by fact hence "X ∈ ty_dom Γ" by (rule ty_dom_inclusion) hence "(Tvar X) closed_in Γ" by (simp add: closed_in_def ty.supp supp_atm) moreover have "S closed_in Γ ∧ T closed_in Γ" by fact hence "T closed_in Γ" by force ultimately show "(Tvar X) closed_in Γ ∧ T closed_in Γ" by simp qed (auto simp add: closed_in_def ty.supp supp_atm abs_supp) lemma subtype_implies_fresh: fixes X::"tyvrs" assumes a1: "Γ ⊢ S <: T" and a2: "X♯Γ" shows "X♯S ∧ X♯T" proof - from a1 have "⊢ Γ ok" by (rule subtype_implies_ok) with a2 have "X♯ty_dom(Γ)" by (simp add: fresh_dom) moreover from a1 have "S closed_in Γ ∧ T closed_in Γ" by (rule subtype_implies_closed) hence "supp S ⊆ ((supp (ty_dom Γ))::tyvrs set)" and "supp T ⊆ ((supp (ty_dom Γ))::tyvrs set)" by (simp_all add: ty_dom_supp closed_in_def) ultimately show "X♯S ∧ X♯T" by (force simp add: supp_prod fresh_def) qed lemma valid_ty_dom_fresh: fixes X::"tyvrs" assumes valid: "⊢ Γ ok" shows "X♯(ty_dom Γ) = X♯Γ" using valid apply induct apply (simp add: fresh_list_nil fresh_set_empty) apply (simp_all add: binding.fresh fresh_list_cons fresh_fin_insert [OF pt_tyvrs_inst at_tyvrs_inst fs_tyvrs_inst] finite_doms fresh_atm) apply (auto simp add: closed_in_fresh) done equivariance subtype_of nominal_inductive subtype_of apply (simp_all add: abs_fresh) apply (fastforce simp add: valid_ty_dom_fresh dest: subtype_implies_ok) apply (force simp add: closed_in_fresh dest: subtype_implies_closed subtype_implies_ok)+ done section ‹Reflexivity of Subtyping› lemma subtype_reflexivity: assumes a: "⊢ Γ ok" and b: "T closed_in Γ" shows "Γ ⊢ T <: T" using a b proof(nominal_induct T avoiding: Γ rule: ty.strong_induct) case (Forall X T⇩_{1}T⇩_{2}) have ih_T⇩_{1}: "⋀Γ. ⟦⊢ Γ ok; T⇩_{1}closed_in Γ⟧ ⟹ Γ ⊢ T⇩_{1}<: T⇩_{1}" by fact have ih_T⇩_{2}: "⋀Γ. ⟦⊢ Γ ok; T⇩_{2}closed_in Γ⟧ ⟹ Γ ⊢ T⇩_{2}<: T⇩_{2}" by fact have fresh_cond: "X♯Γ" by fact hence fresh_ty_dom: "X♯(ty_dom Γ)" by (simp add: fresh_dom) have "(∀X<:T⇩_{2}. T⇩_{1}) closed_in Γ" by fact hence closed⇩_{T}2: "T⇩_{2}closed_in Γ" and closed⇩_{T}1: "T⇩_{1}closed_in ((TVarB X T⇩_{2})#Γ)" by (auto simp add: closed_in_def ty.supp abs_supp) have ok: "⊢ Γ ok" by fact hence ok': "⊢ ((TVarB X T⇩_{2})#Γ) ok" using closed⇩_{T}2 fresh_ty_dom by simp have "Γ ⊢ T⇩_{2}<: T⇩_{2}" using ih_T⇩_{2}closed⇩_{T}2 ok by simp moreover have "((TVarB X T⇩_{2})#Γ) ⊢ T⇩_{1}<: T⇩_{1}" using ih_T⇩_{1}closed⇩_{T}1 ok' by simp ultimately show "Γ ⊢ (∀X<:T⇩_{2}. T⇩_{1}) <: (∀X<:T⇩_{2}. T⇩_{1})" using fresh_cond by (simp add: subtype_of.SA_all) qed (auto simp add: closed_in_def ty.supp supp_atm) lemma subtype_reflexivity_semiautomated: assumes a: "⊢ Γ ok" and b: "T closed_in Γ" shows "Γ ⊢ T <: T" using a b apply(nominal_induct T avoiding: Γ rule: ty.strong_induct) apply(auto simp add: ty.supp abs_supp supp_atm closed_in_def) ― ‹Too bad that this instantiation cannot be found automatically by \isakeyword{auto}; \isakeyword{blast} would find it if we had not used an explicit definition for ‹closed_in_def›.› apply(drule_tac x="(TVarB tyvrs ty2)#Γ" in meta_spec) apply(force dest: fresh_dom simp add: closed_in_def) done section ‹Weakening› text ‹In order to prove weakening we introduce the notion of a type-context extending another. This generalization seems to make the proof for weakening to be smoother than if we had strictly adhered to the version in the POPLmark-paper.› definition extends :: "env ⇒ env ⇒ bool" ("_ extends _" [100,100] 100) where "Δ extends Γ ≡ ∀X Q. (TVarB X Q)∈set Γ ⟶ (TVarB X Q)∈set Δ" lemma extends_ty_dom: assumes a: "Δ extends Γ" shows "ty_dom Γ ⊆ ty_dom Δ" using a apply (auto simp add: extends_def) apply (drule ty_dom_existence) apply (force simp add: ty_dom_inclusion) done lemma extends_closed: assumes a1: "T closed_in Γ" and a2: "Δ extends Γ" shows "T closed_in Δ" using a1 a2 by (auto dest: extends_ty_dom simp add: closed_in_def) lemma extends_memb: assumes a: "Δ extends Γ" and b: "(TVarB X T) ∈ set Γ" shows "(TVarB X T) ∈ set Δ" using a b by (simp add: extends_def) lemma weakening: assumes a: "Γ ⊢ S <: T" and b: "⊢ Δ ok" and c: "Δ extends Γ" shows "Δ ⊢ S <: T" using a b c proof (nominal_induct Γ S T avoiding: Δ rule: subtype_of.strong_induct) case (SA_Top Γ S) have lh_drv_prem: "S closed_in Γ" by fact have "⊢ Δ ok" by fact moreover have "Δ extends Γ" by fact hence "S closed_in Δ" using lh_drv_prem by (simp only: extends_closed) ultimately show "Δ ⊢ S <: Top" by force next case (SA_trans_TVar X S Γ T) have lh_drv_prem: "(TVarB X S) ∈ set Γ" by fact have ih: "⋀Δ. ⊢ Δ ok ⟹ Δ extends Γ ⟹ Δ ⊢ S <: T" by fact have ok: "⊢ Δ ok" by fact have extends: "Δ extends Γ" by fact have "(TVarB X S) ∈ set Δ" using lh_drv_prem extends by (simp only: extends_memb) moreover have "Δ ⊢ S <: T" using ok extends ih by simp ultimately show "Δ ⊢ Tvar X <: T" using ok by force next case (SA_refl_TVar Γ X) have lh_drv_prem: "X ∈ ty_dom Γ" by fact have "⊢ Δ ok" by fact moreover have "Δ extends Γ" by fact hence "X ∈ ty_dom Δ" using lh_drv_prem by (force dest: extends_ty_dom) ultimately show "Δ ⊢ Tvar X <: Tvar X" by force next case (SA_arrow Γ T⇩_{1}S⇩_{1}S⇩_{2}T⇩_{2}) thus "Δ ⊢ S⇩_{1}→ S⇩_{2}<: T⇩_{1}→ T⇩_{2}" by blast next case (SA_all Γ T⇩_{1}S⇩_{1}X S⇩_{2}T⇩_{2}) have fresh_cond: "X♯Δ" by fact hence fresh_dom: "X♯(ty_dom Δ)" by (simp add: fresh_dom) have ih⇩_{1}: "⋀Δ. ⊢ Δ ok ⟹ Δ extends Γ ⟹ Δ ⊢ T⇩_{1}<: S⇩_{1}" by fact have ih⇩_{2}: "⋀Δ. ⊢ Δ ok ⟹ Δ extends ((TVarB X T⇩_{1})#Γ) ⟹ Δ ⊢ S⇩_{2}<: T⇩_{2}" by fact have lh_drv_prem: "Γ ⊢ T⇩_{1}<: S⇩_{1}" by fact hence closed⇩_{T}1: "T⇩_{1}closed_in Γ" by (simp add: subtype_implies_closed) have ok: "⊢ Δ ok" by fact have ext: "Δ extends Γ" by fact have "T⇩_{1}closed_in Δ" using ext closed⇩_{T}1 by (simp only: extends_closed) hence "⊢ ((TVarB X T⇩_{1})#Δ) ok" using fresh_dom ok by force moreover have "((TVarB X T⇩_{1})#Δ) extends ((TVarB X T⇩_{1})#Γ)" using ext by (force simp add: extends_def) ultimately have "((TVarB X T⇩_{1})#Δ) ⊢ S⇩_{2}<: T⇩_{2}" using ih⇩_{2}by simp moreover have "Δ ⊢ T⇩_{1}<: S⇩_{1}" using ok ext ih⇩_{1}by simp ultimately show "Δ ⊢ (∀X<:S⇩_{1}. S⇩_{2}) <: (∀X<:T⇩_{1}. T⇩_{2})" using ok by (force intro: SA_all) qed text ‹In fact all ``non-binding" cases can be solved automatically:› lemma weakening_more_automated: assumes a: "Γ ⊢ S <: T" and b: "⊢ Δ ok" and c: "Δ extends Γ" shows "Δ ⊢ S <: T" using a b c proof (nominal_induct Γ S T avoiding: Δ rule: subtype_of.strong_induct) case (SA_all Γ T⇩_{1}S⇩_{1}X S⇩_{2}T⇩_{2}) have fresh_cond: "X♯Δ" by fact hence fresh_dom: "X♯(ty_dom Δ)" by (simp add: fresh_dom) have ih⇩_{1}: "⋀Δ. ⊢ Δ ok ⟹ Δ extends Γ ⟹ Δ ⊢ T⇩_{1}<: S⇩_{1}" by fact have ih⇩_{2}: "⋀Δ. ⊢ Δ ok ⟹ Δ extends ((TVarB X T⇩_{1})#Γ) ⟹ Δ ⊢ S⇩_{2}<: T⇩_{2}" by fact have lh_drv_prem: "Γ ⊢ T⇩_{1}<: S⇩_{1}" by fact hence closed⇩_{T}1: "T⇩_{1}closed_in Γ" by (simp add: subtype_implies_closed) have ok: "⊢ Δ ok" by fact have ext: "Δ extends Γ" by fact have "T⇩_{1}closed_in Δ" using ext closed⇩_{T}1 by (simp only: extends_closed) hence "⊢ ((TVarB X T⇩_{1})#Δ) ok" using fresh_dom ok by force moreover have "((TVarB X T⇩_{1})#Δ) extends ((TVarB X T⇩_{1})#Γ)" using ext by (force simp add: extends_def) ultimately have "((TVarB X T⇩_{1})#Δ) ⊢ S⇩_{2}<: T⇩_{2}" using ih⇩_{2}by simp moreover have "Δ ⊢ T⇩_{1}<: S⇩_{1}" using ok ext ih⇩_{1}by simp ultimately show "Δ ⊢ (∀X<:S⇩_{1}. S⇩_{2}) <: (∀X<:T⇩_{1}. T⇩_{2})" using ok by (force intro: SA_all) qed (blast intro: extends_closed extends_memb dest: extends_ty_dom)+ section ‹Transitivity and Narrowing› text ‹Some inversion lemmas that are needed in the transitivity and narrowing proof.› declare ty.inject [simp add] inductive_cases S_TopE: "Γ ⊢ Top <: T" inductive_cases S_ArrowE_left: "Γ ⊢ S⇩_{1}→ S⇩_{2}<: T" declare ty.inject [simp del] lemma S_ForallE_left: shows "⟦Γ ⊢ (∀X<:S⇩_{1}. S⇩_{2}) <: T; X♯Γ; X♯S⇩_{1}; X♯T⟧ ⟹ T = Top ∨ (∃T⇩_{1}T⇩_{2}. T = (∀X<:T⇩_{1}. T⇩_{2}) ∧ Γ ⊢ T⇩_{1}<: S⇩_{1}∧ ((TVarB X T⇩_{1})#Γ) ⊢ S⇩_{2}<: T⇩_{2})" apply(erule subtype_of.strong_cases[where X="X"]) apply(auto simp add: abs_fresh ty.inject alpha) done text ‹Next we prove the transitivity and narrowing for the subtyping-relation. The POPLmark-paper says the following: \begin{quote} \begin{lemma}[Transitivity and Narrowing] \ \begin{enumerate} \item If @{term "Γ ⊢ S<:Q"} and @{term "Γ ⊢ Q<:T"}, then @{term "Γ ⊢ S<:T"}. \item If ‹Γ,X<:Q,Δ ⊢ M<:N› and @{term "Γ ⊢ P<:Q"} then ‹Γ,X<:P,Δ ⊢ M<:N›. \end{enumerate} \end{lemma} The two parts are proved simultaneously, by induction on the size of @{term "Q"}. The argument for part (2) assumes that part (1) has been established already for the @{term "Q"} in question; part (1) uses part (2) only for strictly smaller @{term "Q"}. \end{quote} For the induction on the size of @{term "Q"}, we use the induction-rule ‹measure_induct_rule›: \begin{center} @{thm measure_induct_rule[of "size_ty",no_vars]} \end{center} That means in order to show a property @{term "P a"} for all @{term "a"}, the induct-rule requires to prove that for all @{term x} @{term "P x"} holds using the assumption that for all @{term y} whose size is strictly smaller than that of @{term x} the property @{term "P y"} holds.› lemma shows subtype_transitivity: "Γ⊢S<:Q ⟹ Γ⊢Q<:T ⟹ Γ⊢S<:T" and subtype_narrow: "(Δ@[(TVarB X Q)]@Γ)⊢M<:N ⟹ Γ⊢P<:Q ⟹ (Δ@[(TVarB X P)]@Γ)⊢M<:N" proof (induct Q arbitrary: Γ S T Δ X P M N taking: "size_ty" rule: measure_induct_rule) case (less Q) have IH_trans: "⋀Q' Γ S T. ⟦size_ty Q' < size_ty Q; Γ⊢S<:Q'; Γ⊢Q'<:T⟧ ⟹ Γ⊢S<:T" by fact have IH_narrow: "⋀Q' Δ Γ X M N P. ⟦size_ty Q' < size_ty Q; (Δ@[(TVarB X Q')]@Γ)⊢M<:N; Γ⊢P<:Q'⟧ ⟹ (Δ@[(TVarB X P)]@Γ)⊢M<:N" by fact { fix Γ S T have "⟦Γ ⊢ S <: Q; Γ ⊢ Q <: T⟧ ⟹ Γ ⊢ S <: T" proof (induct Γ S Q≡Q rule: subtype_of.induct) case (SA_Top Γ S) then have rh_drv: "Γ ⊢ Top <: T" by simp then have T_inst: "T = Top" by (auto elim: S_TopE) from ‹⊢ Γ ok› and ‹S closed_in Γ› have "Γ ⊢ S <: Top" by auto then show "Γ ⊢ S <: T" using T_inst by simp next case (SA_trans_TVar Y U Γ) then have IH_inner: "Γ ⊢ U <: T" by simp have "(TVarB Y U) ∈ set Γ" by fact with IH_inner show "Γ ⊢ Tvar Y <: T" by auto next case (SA_refl_TVar Γ X) then show "Γ ⊢ Tvar X <: T" by simp next case (SA_arrow Γ Q⇩_{1}S⇩_{1}S⇩_{2}Q⇩_{2}) then have rh_drv: "Γ ⊢ Q⇩_{1}→ Q⇩_{2}<: T" by simp from ‹Q⇩_{1}→ Q⇩_{2}= Q› have Q⇩_{1}2_less: "size_ty Q⇩_{1}< size_ty Q" "size_ty Q⇩_{2}< size_ty Q" by auto have lh_drv_prm⇩_{1}: "Γ ⊢ Q⇩_{1}<: S⇩_{1}" by fact have lh_drv_prm⇩_{2}: "Γ ⊢ S⇩_{2}<: Q⇩_{2}" by fact from rh_drv have "T=Top ∨ (∃T⇩_{1}T⇩_{2}. T=T⇩_{1}→T⇩_{2}∧ Γ⊢T⇩_{1}<:Q⇩_{1}∧ Γ⊢Q⇩_{2}<:T⇩_{2})" by (auto elim: S_ArrowE_left) moreover have "S⇩_{1}closed_in Γ" and "S⇩_{2}closed_in Γ" using lh_drv_prm⇩_{1}lh_drv_prm⇩_{2}by (simp_all add: subtype_implies_closed) hence "(S⇩_{1}→ S⇩_{2}) closed_in Γ" by (simp add: closed_in_def ty.supp) moreover have "⊢ Γ ok" using rh_drv by (rule subtype_implies_ok) moreover { assume "∃T⇩_{1}T⇩_{2}. T = T⇩_{1}→T⇩_{2}∧ Γ ⊢ T⇩_{1}<: Q⇩_{1}∧ Γ ⊢ Q⇩_{2}<: T⇩_{2}" then obtain T⇩_{1}T⇩_{2}where T_inst: "T = T⇩_{1}→ T⇩_{2}" and rh_drv_prm⇩_{1}: "Γ ⊢ T⇩_{1}<: Q⇩_{1}" and rh_drv_prm⇩_{2}: "Γ ⊢ Q⇩_{2}<: T⇩_{2}" by force from IH_trans[of "Q⇩_{1}"] have "Γ ⊢ T⇩_{1}<: S⇩_{1}" using Q⇩_{1}2_less rh_drv_prm⇩_{1}lh_drv_prm⇩_{1}by simp moreover from IH_trans[of "Q⇩_{2}"] have "Γ ⊢ S⇩_{2}<: T⇩_{2}" using Q⇩_{1}2_less rh_drv_prm⇩_{2}lh_drv_prm⇩_{2}by simp ultimately have "Γ ⊢ S⇩_{1}→ S⇩_{2}<: T⇩_{1}→ T⇩_{2}" by auto then have "Γ ⊢ S⇩_{1}→ S⇩_{2}<: T" using T_inst by simp } ultimately show "Γ ⊢ S⇩_{1}→ S⇩_{2}<: T" by blast next case (SA_all Γ Q⇩_{1}S⇩_{1}X S⇩_{2}Q⇩_{2}) then have rh_drv: "Γ ⊢ (∀X<:Q⇩_{1}. Q⇩_{2}) <: T" by simp have lh_drv_prm⇩_{1}: "Γ ⊢ Q⇩_{1}<: S⇩_{1}" by fact have lh_drv_prm⇩_{2}: "((TVarB X Q⇩_{1})#Γ) ⊢ S⇩_{2}<: Q⇩_{2}" by fact then have "X♯Γ" by (force dest: subtype_implies_ok simp add: valid_ty_dom_fresh) then have fresh_cond: "X♯Γ" "X♯Q⇩_{1}" "X♯T" using rh_drv lh_drv_prm⇩_{1}by (simp_all add: subtype_implies_fresh) from rh_drv have "T = Top ∨ (∃T⇩_{1}T⇩_{2}. T = (∀X<:T⇩_{1}. T⇩_{2}) ∧ Γ ⊢ T⇩_{1}<: Q⇩_{1}∧ ((TVarB X T⇩_{1})#Γ) ⊢ Q⇩_{2}<: T⇩_{2})" using fresh_cond by (simp add: S_ForallE_left) moreover have "S⇩_{1}closed_in Γ" and "S⇩_{2}closed_in ((TVarB X Q⇩_{1})#Γ)" using lh_drv_prm⇩_{1}lh_drv_prm⇩_{2}by (simp_all add: subtype_implies_closed) then have "(∀X<:S⇩_{1}. S⇩_{2}) closed_in Γ" by (force simp add: closed_in_def ty.supp abs_supp) moreover have "⊢ Γ ok" using rh_drv by (rule subtype_implies_ok) moreover { assume "∃T⇩_{1}T⇩_{2}. T=(∀X<:T⇩_{1}. T⇩_{2}) ∧ Γ⊢T⇩_{1}<:Q⇩_{1}∧ ((TVarB X T⇩_{1})#Γ)⊢Q⇩_{2}<:T⇩_{2}" then obtain T⇩_{1}T⇩_{2}where T_inst: "T = (∀X<:T⇩_{1}. T⇩_{2})" and rh_drv_prm⇩_{1}: "Γ ⊢ T⇩_{1}<: Q⇩_{1}" and rh_drv_prm⇩_{2}:"((TVarB X T⇩_{1})#Γ) ⊢ Q⇩_{2}<: T⇩_{2}" by force have "(∀X<:Q⇩_{1}. Q⇩_{2}) = Q" by fact then have Q⇩_{1}2_less: "size_ty Q⇩_{1}< size_ty Q" "size_ty Q⇩_{2}< size_ty Q" using fresh_cond by auto from IH_trans[of "Q⇩_{1}"] have "Γ ⊢ T⇩_{1}<: S⇩_{1}" using lh_drv_prm⇩_{1}rh_drv_prm⇩_{1}Q⇩_{1}2_less by blast moreover from IH_narrow[of "Q⇩_{1}" "[]"] have "((TVarB X T⇩_{1})#Γ) ⊢ S⇩_{2}<: Q⇩_{2}" using Q⇩_{1}2_less lh_drv_prm⇩_{2}rh_drv_prm⇩_{1}by simp with IH_trans[of "Q⇩_{2}"] have "((TVarB X T⇩_{1})#Γ) ⊢ S⇩_{2}<: T⇩_{2}" using Q⇩_{1}2_less rh_drv_prm⇩_{2}by simp ultimately have "Γ ⊢ (∀X<:S⇩_{1}. S⇩_{2}) <: (∀X<:T⇩_{1}. T⇩_{2})" using fresh_cond by (simp add: subtype_of.SA_all) hence "Γ ⊢ (∀X<:S⇩_{1}. S⇩_{2}) <: T" using T_inst by simp } ultimately show "Γ ⊢ (∀X<:S⇩_{1}. S⇩_{2}) <: T" by blast qed } note transitivity_lemma = this { ― ‹The transitivity proof is now by the auxiliary lemma.› case 1 from ‹Γ ⊢ S <: Q› and ‹Γ ⊢ Q <: T› show "Γ ⊢ S <: T" by (rule transitivity_lemma) next case 2 from ‹(Δ@[(TVarB X Q)]@Γ) ⊢ M <: N› and ‹Γ ⊢ P<:Q› show "(Δ@[(TVarB X P)]@Γ) ⊢ M <: N" proof (induct "Δ@[(TVarB X Q)]@Γ" M N arbitrary: Γ X Δ rule: subtype_of.induct) case (SA_Top S Γ X Δ) from ‹Γ ⊢ P <: Q› have "P closed_in Γ" by (simp add: subtype_implies_closed) with ‹⊢ (Δ@[(TVarB X Q)]@Γ) ok› have "⊢ (Δ@[(TVarB X P)]@Γ) ok" by (simp add: replace_type) moreover from ‹S closed_in (Δ@[(TVarB X Q)]@Γ)› have "S closed_in (Δ@[(TVarB X P)]@Γ)" by (simp add: closed_in_def doms_append) ultimately show "(Δ@[(TVarB X P)]@Γ) ⊢ S <: Top" by (simp add: subtype_of.SA_Top) next case (SA_trans_TVar Y S N Γ X Δ) then have IH_inner: "(Δ@[(TVarB X P)]@Γ) ⊢ S <: N" and lh_drv_prm: "(TVarB Y S) ∈ set (Δ@[(TVarB X Q)]@Γ)" and rh_drv: "Γ ⊢ P<:Q" and ok⇩_{Q}: "⊢ (Δ@[(TVarB X Q)]@Γ) ok" by (simp_all add: subtype_implies_ok) then have ok⇩_{P}: "⊢ (Δ@[(TVarB X P)]@Γ) ok" by (simp add: subtype_implies_ok) show "(Δ@[(TVarB X P)]@Γ) ⊢ Tvar Y <: N" proof (cases "X=Y") case False have "X≠Y" by fact hence "(TVarB Y S)∈set (Δ@[(TVarB X P)]@Γ)" using lh_drv_prm by (simp add:binding.inject) with IH_inner show "(Δ@[(TVarB X P)]@Γ) ⊢ Tvar Y <: N" by (simp add: subtype_of.SA_trans_TVar) next case True have memb⇩_{X}Q: "(TVarB X Q)∈set (Δ@[(TVarB X Q)]@Γ)" by simp have memb⇩_{X}P: "(TVarB X P)∈set (Δ@[(TVarB X P)]@Γ)" by simp have eq: "X=Y" by fact hence "S=Q" using ok⇩_{Q}lh_drv_prm memb⇩_{X}Q by (simp only: uniqueness_of_ctxt) hence "(Δ@[(TVarB X P)]@Γ) ⊢ Q <: N" using IH_inner by simp moreover have "(Δ@[(TVarB X P)]@Γ) extends Γ" by (simp add: extends_def) hence "(Δ@[(TVarB X P)]@Γ) ⊢ P <: Q" using rh_drv ok⇩_{P}by (simp only: weakening) ultimately have "(Δ@[(TVarB X P)]@Γ) ⊢ P <: N" by (simp add: transitivity_lemma) then show "(Δ@[(TVarB X P)]@Γ) ⊢ Tvar Y <: N" using memb⇩_{X}P eq by auto qed next case (SA_refl_TVar Y Γ X Δ) from ‹Γ ⊢ P <: Q› have "P closed_in Γ" by (simp add: subtype_implies_closed) with ‹⊢ (Δ@[(TVarB X Q)]@Γ) ok› have "⊢ (Δ@[(TVarB X P)]@Γ) ok" by (simp add: replace_type) moreover from ‹Y ∈ ty_dom (Δ@[(TVarB X Q)]@Γ)› have "Y ∈ ty_dom (Δ@[(TVarB X P)]@Γ)" by (simp add: doms_append) ultimately show "(Δ@[(TVarB X P)]@Γ) ⊢ Tvar Y <: Tvar Y" by (simp add: subtype_of.SA_refl_TVar) next case (SA_arrow S⇩_{1}Q⇩_{1}Q⇩_{2}S⇩_{2}Γ X Δ) then show "(Δ@[(TVarB X P)]@Γ) ⊢ Q⇩_{1}→ Q⇩_{2}<: S⇩_{1}→ S⇩_{2}" by blast next case (SA_all T⇩_{1}S⇩_{1}Y S⇩_{2}T⇩_{2}Γ X Δ) have IH_inner⇩_{1}: "(Δ@[(TVarB X P)]@Γ) ⊢ T⇩_{1}<: S⇩_{1}" and IH_inner⇩_{2}: "(((TVarB Y T⇩_{1})#Δ)@[(TVarB X P)]@Γ) ⊢ S⇩_{2}<: T⇩_{2}" by (fastforce intro: SA_all)+ then show "(Δ@[(TVarB X P)]@Γ) ⊢ (∀Y<:S⇩_{1}. S⇩_{2}) <: (∀Y<:T⇩_{1}. T⇩_{2})" by auto qed } qed section ‹Typing› inductive typing :: "env ⇒ trm ⇒ ty ⇒ bool" ("_ ⊢ _ : _" [60,60,60] 60) where T_Var[intro]: "⟦ VarB x T ∈ set Γ; ⊢ Γ ok ⟧ ⟹ Γ ⊢ Var x : T" | T_App[intro]: "⟦ Γ ⊢ t⇩_{1}: T⇩_{1}→ T⇩_{2}; Γ ⊢ t⇩_{2}: T⇩_{1}⟧ ⟹ Γ ⊢ t⇩_{1}⋅ t⇩_{2}: T⇩_{2}" | T_Abs[intro]: "⟦ VarB x T⇩_{1}# Γ ⊢ t⇩_{2}: T⇩_{2}⟧ ⟹ Γ ⊢ (λx:T⇩_{1}. t⇩_{2}) : T⇩_{1}→ T⇩_{2}" | T_Sub[intro]: "⟦ Γ ⊢ t : S; Γ ⊢ S <: T ⟧ ⟹ Γ ⊢ t : T" | T_TAbs[intro]:"⟦ TVarB X T⇩_{1}# Γ ⊢ t⇩_{2}: T⇩_{2}⟧ ⟹ Γ ⊢ (λX<:T⇩_{1}. t⇩_{2}) : (∀X<:T⇩_{1}. T⇩_{2})" | T_TApp[intro]:"⟦X♯(Γ,t⇩_{1},T⇩_{2}); Γ ⊢ t⇩_{1}: (∀X<:T⇩_{1}1. T⇩_{1}2); Γ ⊢ T⇩_{2}<: T⇩_{1}1⟧ ⟹ Γ ⊢ t⇩_{1}⋅⇩_{τ}T⇩_{2}: (T⇩_{1}2[X ↦ T⇩_{2}]⇩_{τ})" equivariance typing lemma better_T_TApp: assumes H1: "Γ ⊢ t⇩_{1}: (∀X<:T11. T12)" and H2: "Γ ⊢ T2 <: T11" shows "Γ ⊢ t⇩_{1}⋅⇩_{τ}T2 : (T12[X ↦ T2]⇩_{τ})" proof - obtain Y::tyvrs where Y: "Y ♯ (X, T12, Γ, t⇩_{1}, T2)" by (rule exists_fresh) (rule fin_supp) then have "Y ♯ (Γ, t⇩_{1}, T2)" by simp moreover from Y have "(∀X<:T11. T12) = (∀Y<:T11. [(Y, X)] ∙ T12)" by (auto simp add: ty.inject alpha' fresh_prod fresh_atm) with H1 have "Γ ⊢ t⇩_{1}: (∀Y<:T11. [(Y, X)] ∙ T12)" by simp ultimately have "Γ ⊢ t⇩_{1}⋅⇩_{τ}T2 : (([(Y, X)] ∙ T12)[Y ↦ T2]⇩_{τ})" using H2 by (rule T_TApp) with Y show ?thesis by (simp add: type_subst_rename) qed lemma typing_ok: assumes "Γ ⊢ t : T" shows "⊢ Γ ok" using assms by (induct) (auto) nominal_inductive typing by (auto dest!: typing_ok intro: closed_in_fresh fresh_dom type_subst_fresh simp: abs_fresh fresh_type_subst_fresh ty_vrs_fresh valid_ty_dom_fresh fresh_trm_dom) lemma ok_imp_VarB_closed_in: assumes ok: "⊢ Γ ok" shows "VarB x T ∈ set Γ ⟹ T closed_in Γ" using ok by induct (auto simp add: binding.inject closed_in_def) lemma tyvrs_of_subst: "tyvrs_of (B[X ↦ T]⇩_{b}) = tyvrs_of B" by (nominal_induct B rule: binding.strong_induct) simp_all lemma ty_dom_subst: "ty_dom (Γ[X ↦ T]⇩_{e}) = ty_dom Γ" by (induct Γ) (simp_all add: tyvrs_of_subst) lemma vrs_of_subst: "vrs_of (B[X ↦ T]⇩_{b}) = vrs_of B" by (nominal_induct B rule: binding.strong_induct) simp_all lemma trm_dom_subst: "trm_dom (Γ[X ↦ T]⇩_{e}) = trm_dom Γ" by (induct Γ) (simp_all add: vrs_of_subst) lemma subst_closed_in: "T closed_in (Δ @ TVarB X S # Γ) ⟹ U closed_in Γ ⟹ T[X ↦ U]⇩_{τ}closed_in (Δ[X ↦ U]⇩_{e}@ Γ)" apply (nominal_induct T avoiding: X U Γ rule: ty.strong_induct) apply (simp add: closed_in_def ty.supp supp_atm doms_append ty_dom_subst) apply blast apply (simp add: closed_in_def ty.supp) apply (simp add: closed_in_def ty.supp) apply (simp add: closed_in_def ty.supp abs_supp) apply (drule_tac x = X in meta_spec) apply (drule_tac x = U in meta_spec) apply (drule_tac x = "(TVarB tyvrs ty2) # Γ" in meta_spec) apply (simp add: doms_append ty_dom_subst) apply blast done lemmas subst_closed_in' = subst_closed_in [where Δ="[]", simplified] lemma typing_closed_in: assumes "Γ ⊢ t : T" shows "T closed_in Γ" using assms proof induct case (T_Var x T Γ) from ‹⊢ Γ ok› and ‹VarB x T ∈ set Γ› show ?case by (rule ok_imp_VarB_closed_in) next case (T_App Γ t⇩_{1}T⇩_{1}T⇩_{2}t⇩_{2}) then show ?case by (auto simp add: ty.supp closed_in_def) next case (T_Abs x T⇩_{1}Γ t⇩_{2}T⇩_{2}) from ‹VarB x T⇩_{1}# Γ ⊢ t⇩_{2}: T⇩_{2}› have "T⇩_{1}closed_in Γ" by (auto dest: typing_ok) with T_Abs show ?case by (auto simp add: ty.supp closed_in_def) next case (T_Sub Γ t S T) from ‹Γ ⊢ S <: T› show ?case by (simp add: subtype_implies_closed) next case (T_TAbs X T⇩_{1}Γ t⇩_{2}T⇩_{2}) from ‹TVarB X T⇩_{1}# Γ ⊢ t⇩_{2}: T⇩_{2}› have "T⇩_{1}closed_in Γ" by (auto dest: typing_ok) with T_TAbs show ?case by (auto simp add: ty.supp closed_in_def abs_supp) next case (T_TApp X Γ t⇩_{1}T2 T11 T12) then have "T12 closed_in (TVarB X T11 # Γ)" by (auto simp add: closed_in_def ty.supp abs_supp) moreover from T_TApp have "T2 closed_in Γ" by (simp add: subtype_implies_closed) ultimately show ?case by (rule subst_closed_in') qed subsection ‹Evaluation› inductive val :: "trm ⇒ bool" where Abs[intro]: "val (λx:T. t)" | TAbs[intro]: "val (λX<:T. t)" equivariance val inductive_cases val_inv_auto[elim]: "val (Var x)" "val (t1 ⋅ t2)" "val (t1 ⋅⇩_{τ}t2)" inductive eval :: "trm ⇒ trm ⇒ bool" ("_ ⟼ _" [60,60] 60) where E_Abs : "⟦ x ♯ v⇩_{2}; val v⇩_{2}⟧ ⟹ (λx:T⇩_{1}1. t⇩_{1}2) ⋅ v⇩_{2}⟼ t⇩_{1}2[x ↦ v⇩_{2}]" | E_App1 [intro]: "t ⟼ t' ⟹ t ⋅ u ⟼ t' ⋅ u" | E_App2 [intro]: "⟦ val v; t ⟼ t' ⟧ ⟹ v ⋅ t ⟼ v ⋅ t'" | E_TAbs : "X ♯ (T⇩_{1}1, T⇩_{2}) ⟹ (λX<:T⇩_{1}1. t⇩_{1}2) ⋅⇩_{τ}T⇩_{2}⟼ t⇩_{1}2[X ↦⇩_{τ}T⇩_{2}]" | E_TApp [intro]: "t ⟼ t' ⟹ t ⋅⇩_{τ}T ⟼ t' ⋅⇩_{τ}T" lemma better_E_Abs[intro]: assumes H: "val v2" shows "(λx:T11. t12) ⋅ v2 ⟼ t12[x ↦ v2]" proof - obtain y::vrs where y: "y ♯ (x, t12, v2)" by (rule exists_fresh) (rule fin_supp) then have "y ♯ v2" by simp then have "(λy:T11. [(y, x)] ∙ t12) ⋅ v2 ⟼ ([(y, x)] ∙ t12)[y ↦ v2]" using H by (rule E_Abs) moreover from y have "(λx:T11. t12) ⋅ v2 = (λy:T11. [(y, x)] ∙ t12) ⋅ v2" by (auto simp add: trm.inject alpha' fresh_prod fresh_atm) ultimately have "(λx:T11. t12) ⋅ v2 ⟼ ([(y, x)] ∙ t12)[y ↦ v2]" by simp with y show ?thesis by (simp add: subst_trm_rename) qed lemma better_E_TAbs[intro]: "(λX<:T11. t12) ⋅⇩_{τ}T2 ⟼ t12[X ↦⇩_{τ}T2]" proof - obtain Y::tyvrs where Y: "Y ♯ (X, t12, T11, T2)" by (rule exists_fresh) (rule fin_supp) then have "Y ♯ (T11, T2)" by simp then have "(λY<:T11. [(Y, X)] ∙ t12) ⋅⇩_{τ}T2 ⟼ ([(Y, X)] ∙ t12)[Y ↦⇩_{τ}T2]" by (rule E_TAbs) moreover from Y have "(λX<:T11. t12) ⋅⇩_{τ}T2 = (λY<:T11. [(Y, X)] ∙ t12) ⋅⇩_{τ}T2" by (auto simp add: trm.inject alpha' fresh_prod fresh_atm) ultimately have "(λX<:T11. t12) ⋅⇩_{τ}T2 ⟼ ([(Y, X)] ∙ t12)[Y ↦⇩_{τ}T2]" by simp with Y show ?thesis by (simp add: subst_trm_ty_rename) qed equivariance eval nominal_inductive eval by (simp_all add: abs_fresh ty_vrs_fresh subst_trm_fresh_tyvar subst_trm_fresh_var subst_trm_ty_fresh') inductive_cases eval_inv_auto[elim]: "Var x ⟼ t'" "(λx:T. t) ⟼ t'" "(λX<:T. t) ⟼ t'" lemma ty_dom_cons: shows "ty_dom (Γ@[VarB X Q]@Δ) = ty_dom (Γ@Δ)" by (induct Γ) (auto) lemma closed_in_cons: assumes "S closed_in (Γ @ VarB X Q # Δ)" shows "S closed_in (Γ@Δ)" using assms ty_dom_cons closed_in_def by auto lemma closed_in_weaken: "T closed_in (Δ @ Γ) ⟹ T closed_in (Δ @ B # Γ)" by (auto simp add: closed_in_def doms_append) lemma closed_in_weaken': "T closed_in Γ ⟹ T closed_in (Δ @ Γ)" by (auto simp add: closed_in_def doms_append) lemma valid_subst: assumes ok: "⊢ (Δ @ TVarB X Q # Γ) ok" and closed: "P closed_in Γ" shows "⊢ (Δ[X ↦ P]⇩_{e}@ Γ) ok" using ok closed apply (induct Δ) apply simp_all apply (erule validE) apply assumption apply (erule validE) apply simp apply (rule valid_consT) apply assumption apply (simp add: doms_append ty_dom_subst) apply (simp add: fresh_fin_insert [OF pt_tyvrs_inst at_tyvrs_inst fs_tyvrs_inst] finite_doms) apply (rule_tac S=Q in subst_closed_in') apply (simp add: closed_in_def doms_append ty_dom_subst) apply (simp add: closed_in_def doms_append) apply blast apply simp apply (rule valid_cons) apply assumption apply (simp add: doms_append trm_dom_subst) apply (rule_tac S=Q in subst_closed_in') apply (simp add: closed_in_def doms_append ty_dom_subst) apply (simp add: closed_in_def doms_append) apply blast done lemma ty_dom_vrs: shows "ty_dom (G @ [VarB x Q] @ D) = ty_dom (G @ D)" by (induct G) (auto) lemma valid_cons': assumes "⊢ (Γ @ VarB x Q # Δ) ok" shows "⊢ (Γ @ Δ) ok" using assms proof (induct "Γ @ VarB x Q # Δ" arbitrary: Γ Δ) case valid_nil have "[] = Γ @ VarB x Q # Δ" by fact then have "False" by auto then show ?case by auto next case (valid_consT G X T) then show ?case proof (cases Γ) case Nil with valid_consT show ?thesis by simp next case (Cons b bs) with valid_consT have "⊢ (bs @ Δ) ok" by simp moreover from Cons and valid_consT have "X ♯ ty_dom (bs @ Δ)" by (simp add: doms_append) moreover from Cons and valid_consT have "T closed_in (bs @ Δ)" by (simp add: closed_in_def doms_append) ultimately have "⊢ (TVarB X T # bs @ Δ) ok" by (rule valid_rel.valid_consT) with Cons and valid_consT show ?thesis by simp qed next case (valid_cons G x T) then show ?case proof (cases Γ) case Nil with valid_cons show ?thesis by simp next case (Cons b bs) with valid_cons have "⊢ (bs @ Δ) ok" by simp moreover from Cons and valid_cons have "x ♯ trm_dom (bs @ Δ)" by (simp add: doms_append finite_doms fresh_fin_insert [OF pt_vrs_inst at_vrs_inst fs_vrs_inst]) moreover from Cons and valid_cons have "T closed_in (bs @ Δ)" by (simp add: closed_in_def doms_append) ultimately have "⊢ (VarB x T # bs @ Δ) ok" by (rule valid_rel.valid_cons) with Cons and valid_cons show ?thesis by simp qed qed text ‹A.5(6)› lemma type_weaken: assumes "(Δ@Γ) ⊢ t : T" and "⊢ (Δ @ B # Γ) ok" shows "(Δ @ B # Γ) ⊢ t : T" using assms proof(nominal_induct "Δ @ Γ" t T avoiding: Δ Γ B rule: typing.strong_induct) case (T_Var x T) then show ?case by auto next case (T_App X t⇩_{1}T⇩_{2}T⇩_{1}1 T⇩_{1}2) then show ?case by force next case (T_Abs y T⇩_{1}t⇩_{2}T⇩_{2}Δ Γ) then have "VarB y T⇩_{1}# Δ @ Γ ⊢ t⇩_{2}: T⇩_{2}" by simp then have closed: "T⇩_{1}closed_in (Δ @ Γ)" by (auto dest: typing_ok) have "⊢ (VarB y T⇩_{1}# Δ @ B # Γ) ok" apply (rule valid_cons) apply (rule T_Abs) apply (simp add: doms_append fresh_fin_insert [OF pt_vrs_inst at_vrs_inst fs_vrs_inst] fresh_fin_union [OF pt_vrs_inst at_vrs_inst fs_vrs_inst] finite_doms finite_vrs fresh_vrs_of T_Abs fresh_trm_dom) apply (rule closed_in_weaken) apply (rule closed) done then have "⊢ ((VarB y T⇩_{1}# Δ) @ B # Γ) ok" by simp with _ have "(VarB y T⇩_{1}# Δ) @ B # Γ ⊢ t⇩_{2}: T⇩_{2}" by (rule T_Abs) simp then have "VarB y T⇩_{1}# Δ @ B # Γ ⊢ t⇩_{2}: T⇩_{2}" by simp then show ?case by (rule typing.T_Abs) next case (T_Sub t S T Δ Γ) from refl and ‹⊢ (Δ @ B # Γ) ok› have "Δ @ B # Γ ⊢ t : S" by (rule T_Sub) moreover from ‹(Δ @ Γ)⊢S<:T› and ‹⊢ (Δ @ B # Γ) ok› have "(Δ @ B # Γ)⊢S<:T" by (rule weakening) (simp add: extends_def T_Sub) ultimately show ?case by (rule typing.T_Sub) next case (T_TAbs X T⇩_{1}t⇩_{2}T⇩_{2}Δ Γ) from ‹TVarB X T⇩_{1}# Δ @ Γ ⊢ t⇩_{2}: T⇩_{2}› have closed: "T⇩_{1}closed_in (Δ @ Γ)" by (auto dest: typing_ok) have "⊢ (TVarB X T⇩_{1}# Δ @ B # Γ) ok" apply (rule valid_consT) apply (rule T_TAbs) apply (simp add: doms_append fresh_fin_insert [OF pt_tyvrs_inst at_tyvrs_inst fs_tyvrs_inst] fresh_fin_union [OF pt_tyvrs_inst at_tyvrs_inst fs_tyvrs_inst] finite_doms finite_vrs tyvrs_fresh T_TAbs fresh_dom) apply (rule closed_in_weaken) apply (rule closed) done then have "⊢ ((TVarB X T⇩_{1}# Δ) @ B # Γ) ok" by simp with _ have "(TVarB X T⇩_{1}# Δ) @ B # Γ ⊢ t⇩_{2}: T⇩_{2}" by (rule T_TAbs) simp then have "TVarB X T⇩_{1}# Δ @ B # Γ ⊢ t⇩_{2}: T⇩_{2}" by simp then show ?case by (rule typing.T_TAbs) next case (T_TApp X t⇩_{1}T2 T11 T12 Δ Γ) have "Δ @ B # Γ ⊢ t⇩_{1}: (∀X<:T11. T12)" by (rule T_TApp refl)+ moreover from ‹(Δ @ Γ)⊢T2<:T11› and ‹⊢ (Δ @ B # Γ) ok› have "(Δ @ B # Γ)⊢T2<:T11" by (rule weakening) (simp add: extends_def T_TApp) ultimately show ?case by (rule better_T_TApp) qed lemma type_weaken': "Γ ⊢ t : T ⟹ ⊢ (Δ@Γ) ok ⟹ (Δ@Γ) ⊢ t : T" apply (induct Δ) apply simp_all apply (erule validE) apply (insert type_weaken [of "[]", simplified]) apply simp_all done text ‹A.6› lemma strengthening: assumes "(Γ @ VarB x Q # Δ) ⊢ S <: T" shows "(Γ@Δ) ⊢ S <: T" using assms proof (induct "Γ @ VarB x Q # Δ" S T arbitrary: Γ) case (SA_Top S) then have "⊢ (Γ @ Δ) ok" by (auto dest: valid_cons') moreover have "S closed_in (Γ @ Δ)" using SA_Top by (auto dest: closed_in_cons) ultimately show ?case using subtype_of.SA_Top by auto next case (SA_refl_TVar X) from ‹⊢ (Γ @ VarB x Q # Δ) ok› have h1:"⊢ (Γ @ Δ) ok" by (auto dest: valid_cons') have "X ∈ ty_dom (Γ @ VarB x Q # Δ)" using SA_refl_TVar by auto then have h2:"X ∈ ty_dom (Γ @ Δ)" using ty_dom_vrs by auto show ?case using h1 h2 by auto next case (SA_all T1 S1 X S2 T2) have h1:"((TVarB X T1 # Γ) @ Δ)⊢S2<:T2" by (fastforce intro: SA_all) have h2:"(Γ @ Δ)⊢T1<:S1" using SA_all by auto then show ?case using h1 h2 by auto qed (auto) lemma narrow_type: ― ‹A.7› assumes H: "Δ @ (TVarB X Q) # Γ ⊢ t : T" shows "Γ ⊢ P <: Q ⟹ Δ @ (TVarB X P) # Γ ⊢ t : T" using H proof (nominal_induct "Δ @ (TVarB X Q) # Γ" t T avoiding: P arbitrary: Δ rule: typing.strong_induct) case (T_Var x T P D) then have "VarB x T ∈ set (D @ TVarB X P # Γ)" and "⊢ (D @ TVarB X P # Γ) ok" by (auto intro: replace_type dest!: subtype_implies_closed) then show ?case by auto next case (T_App t1 T1 T2 t2 P D) then show ?case by force next case (T_Abs x T1 t2 T2 P D) then show ?case by (fastforce dest: typing_ok) next case (T_Sub t S T P D) then show ?case using subtype_narrow by fastforce next case (T_TAbs X' T1 t2 T2 P D) then show ?case by (fastforce dest: typing_ok) next case (T_TApp X' t1 T2 T11 T12 P D) then have "D @ TVarB X P # Γ ⊢ t1 : Forall X' T12 T11" by fastforce moreover have "(D @ [TVarB X Q] @ Γ) ⊢ T2<:T11" using T_TApp by auto then have "(D @ [TVarB X P] @ Γ) ⊢ T2<:T11" using ‹Γ⊢P<:Q› by (rule subtype_narrow) moreover from T_TApp have "X' ♯ (D @ TVarB X P # Γ, t1, T2)" by (simp add: fresh_list_append fresh_list_cons fresh_prod) ultimately show ?case by auto qed subsection ‹Substitution lemmas› subsubsection ‹Substition Preserves Typing› theorem subst_type: ― ‹A.8› assumes H: "(Δ @ (VarB x U) # Γ) ⊢ t : T" shows "Γ ⊢ u : U ⟹ Δ @ Γ ⊢ t[x ↦ u] : T" using H proof (nominal_induct "Δ @ (VarB x U) # Γ" t T avoiding: x u arbitrary: Δ rule: typing.strong_induct) case (T_Var y T x u D) show ?case proof (cases "x = y") assume eq:"x=y" then have "T=U" using T_Var uniqueness_of_ctxt' by auto then show ?case using eq T_Var by (auto intro: type_weaken' dest: valid_cons') next assume "x≠y" then show ?case using T_Var by (auto simp add:binding.inject dest: valid_cons') qed next case (T_App t1 T1 T2 t2 x u D) then show ?case by force next case (T_Abs y T1 t2 T2 x u D) then show ?case by force next case (T_Sub t S T x u D) then have "D @ Γ ⊢ t[x ↦ u] : S" by auto moreover have "(D @ Γ) ⊢ S<:T" using T_Sub by (auto dest: strengthening) ultimately show ?case by auto next case (T_TAbs X T1 t2 T2 x u D) from ‹TVarB X T1 # D @ VarB x U # Γ ⊢ t2 : T2› have "X ♯ T1" by (auto simp add: valid_ty_dom_fresh dest: typing_ok intro!: closed_in_fresh) with ‹X ♯ u› and T_TAbs show ?case by fastforce next case (T_TApp X t1 T2 T11 T12 x u D) then have "(D@Γ) ⊢T2<:T11" using T_TApp by (auto dest: strengthening) then show "((D @ Γ) ⊢ ((t1 ⋅⇩_{τ}T2)[x ↦ u]) : (T12[X ↦ T2]⇩_{τ}))" using T_TApp by (force simp add: fresh_prod fresh_list_append fresh_list_cons subst_trm_fresh_tyvar) qed subsubsection ‹Type Substitution Preserves Subtyping› lemma substT_subtype: ― ‹A.10› assumes H: "(Δ @ ((TVarB X Q) # Γ)) ⊢ S <: T" shows "Γ ⊢ P <: Q ⟹ (Δ[X ↦ P]⇩_{e}@ Γ) ⊢ S[X ↦ P]⇩_{τ}<: T[X ↦ P]⇩_{τ}" using H proof (nominal_induct "Δ @ TVarB X Q # Γ" S T avoiding: X P arbitrary: Δ rule: subtype_of.strong_induct) case (SA_Top S X P D) then have "⊢ (D @ TVarB X Q # Γ) ok" by simp moreover have closed: "P closed_in Γ" using SA_Top subtype_implies_closed by auto ultimately have "⊢ (D[X ↦ P]⇩_{e}@ Γ) ok" by (rule valid_subst) moreover from SA_Top have "S closed_in (D @ TVarB X Q # Γ)" by simp then have "S[X ↦ P]⇩_{τ}closed_in (D[X ↦ P]⇩_{e}@ Γ)" using closed by (rule subst_closed_in) ultimately show ?case by auto next case (SA_trans_TVar Y S T X P D) have h:"(D @ TVarB X Q # Γ)⊢S<:T" by fact then have ST: "(D[X ↦ P]⇩_{e}@ Γ) ⊢ S[X ↦ P]⇩_{τ}<: T[X ↦ P]⇩_{τ}" using SA_trans_TVar by auto from h have G_ok: "⊢ (D @ TVarB X Q # Γ) ok" by (rule subtype_implies_ok) from G_ok and SA_trans_TVar have X_Γ_ok: "⊢ (TVarB X Q # Γ) ok" by (auto intro: validE_append) show "(D[X ↦ P]⇩_{e}@ Γ) ⊢ Tvar Y[X ↦ P]⇩_{τ}<:T[X ↦ P]⇩_{τ}" proof (cases "X = Y") assume eq: "X = Y" from eq and SA_trans_TVar have "TVarB Y Q ∈ set (D @ TVarB X Q # Γ)" by simp with G_ok have QS: "Q = S" using ‹TVarB Y S ∈ set (D @ TVarB X Q # Γ)› by (rule uniqueness_of_ctxt) from X_Γ_ok have "X ♯ ty_dom Γ" and "Q closed_in Γ" by auto then have XQ: "X ♯ Q" by (rule closed_in_fresh) note ‹Γ⊢P<:Q› moreover from ST have "⊢ (D[X ↦ P]⇩_{e}@ Γ) ok" by (rule subtype_implies_ok) moreover have "(D[X ↦ P]⇩_{e}@ Γ) extends Γ" by (simp add: extends_def) ultimately have "(D[X ↦ P]⇩_{e}@ Γ) ⊢ P<:Q" by (rule weakening) with QS have "(D[X ↦ P]⇩_{e}@ Γ) ⊢ P<:S" by simp moreover from XQ and ST and QS have "(D[X ↦ P]⇩_{e}@ Γ) ⊢ S<:T[X ↦ P]⇩_{τ}" by (simp add: type_subst_identity) ultimately have "(D[X ↦ P]⇩_{e}@ Γ) ⊢ P<:T[X ↦ P]⇩_{τ}" by (rule subtype_transitivity) with eq show ?case by simp next assume neq: "X ≠ Y" with SA_trans_TVar have "TVarB Y S ∈ set D ∨ TVarB Y S ∈ set Γ" by (simp add: binding.inject) then show ?case proof assume "TVarB Y S ∈ set D" then have "TVarB Y (S[X ↦ P]⇩_{τ}) ∈ set (D[X ↦ P]⇩_{e})" by (rule ctxt_subst_mem_TVarB) then have "TVarB Y (S[X ↦ P]⇩_{τ}) ∈ set (D[X ↦ P]⇩_{e}@ Γ)" by simp with neq and ST show ?thesis by auto next assume Y: "TVarB Y S ∈ set Γ" from X_Γ_ok have "X ♯ ty_dom Γ" and "⊢ Γ ok" by auto then have "X ♯ Γ" by (simp add: valid_ty_dom_fresh) with Y have "X ♯ S" by (induct Γ) (auto simp add: fresh_list_nil fresh_list_cons) with ST have "(D[X ↦ P]⇩_{e}@ Γ)⊢S<:T[X ↦ P]⇩_{τ}" by (simp add: type_subst_identity) moreover from Y have "TVarB Y S ∈ set (D[X ↦ P]⇩_{e}@ Γ)" by simp ultimately show ?thesis using neq by auto qed qed next case (SA_refl_TVar Y X P D) note ‹⊢ (D @ TVarB X Q # Γ) ok› moreover from SA_refl_TVar have closed: "P closed_in Γ" by (auto dest: subtype_implies_closed) ultimately have ok: "⊢ (D[X ↦ P]⇩_{e}@ Γ) ok" using valid_subst by auto from closed have closed': "P closed_in (D[X ↦ P]⇩_{e}@ Γ)" by (simp add: closed_in_weaken') show ?case proof (cases "X = Y") assume "X = Y" with closed' and ok show ?thesis by (auto intro: subtype_reflexivity) next assume neq: "X ≠ Y" with SA_refl_TVar have "Y ∈ ty_dom (D[X ↦ P]⇩_{e}@ Γ)" by (simp add: ty_dom_subst doms_append) with neq and ok show ?thesis by auto qed next case (SA_arrow T1 S1 S2 T2 X P D) then have h1:"(D[X ↦ P]⇩_{e}@ Γ)⊢T1[X ↦ P]⇩_{τ}<:S1[X ↦ P]⇩_{τ}" using SA_arrow by auto from SA_arrow have h2:"(D[X ↦ P]⇩_{e}@ Γ)⊢S2[X ↦ P]⇩_{τ}<:T2[X ↦ P]⇩_{τ}" using SA_arrow by auto show ?case using subtype_of.SA_arrow h1 h2 by auto next case (SA_all T1 S1 Y S2 T2 X P D) then have Y: "Y ♯ ty_dom (D @ TVarB X Q # Γ)" by (auto dest: subtype_implies_ok intro: fresh_dom) moreover from SA_all have "S1 closed_in (D @ TVarB X Q # Γ)" by (auto dest: subtype_implies_closed) ultimately have S1: "Y ♯ S1" by (rule closed_in_fresh) from SA_all have "T1 closed_in (D @ TVarB X Q # Γ)" by (auto dest: subtype_implies_closed) with Y have T1: "Y ♯ T1" by (rule closed_in_fresh) with SA_all and S1 show ?case by force qed subsubsection ‹Type Substitution Preserves Typing› theorem substT_type: ― ‹A.11› assumes H: "(D @ TVarB X Q # G) ⊢ t : T" shows "G ⊢ P <: Q ⟹ (D[X ↦ P]⇩_{e}@ G) ⊢ t[X ↦⇩_{τ}P] : T[X ↦ P]⇩_{τ}" using H proof (nominal_induct "D @ TVarB X Q # G" t T avoiding: X P arbitrary: D rule: typing.strong_induct) case (T_Var x T X P D') have "G⊢P<:Q" by fact then have "P closed_in G" using subtype_implies_closed by auto moreover note ‹⊢ (D' @ TVarB X Q # G) ok› ultimately have "⊢ (D'[X ↦ P]⇩_{e}@ G) ok" using valid_subst by auto moreover note ‹VarB x T ∈ set (D' @ TVarB X Q # G)› then have "VarB x T ∈ set D' ∨ VarB x T ∈ set G" by simp then have "(VarB x (T[X ↦ P]⇩_{τ})) ∈ set (D'[X ↦ P]⇩_{e}@ G)" proof assume "VarB x T ∈ set D'" then have "VarB x (T[X ↦ P]⇩_{τ}) ∈ set (D'[X ↦ P]⇩_{e})" by (rule ctxt_subst_mem_VarB) then show ?thesis by simp next assume x: "VarB x T ∈ set G" from T_Var have ok: "⊢ G ok" by (auto dest: subtype_implies_ok) then have "X ♯ ty_dom G" using T_Var by (auto dest: validE_append) with ok have "X ♯ G" by (simp add: valid_ty_dom_fresh) moreover from x have "VarB x T ∈ set (D' @ G)" by simp then have "VarB x (T[X ↦ P]⇩_{τ}) ∈ set ((D' @ G)[X ↦ P]⇩_{e})" by (rule ctxt_subst_mem_VarB) ultimately show ?thesis by (simp add: ctxt_subst_append ctxt_subst_identity) qed ultimately show ?case by auto next case (T_App t1 T1 T2 t2 X P D') then have "D'[X ↦ P]⇩_{e}@ G ⊢ t1[X ↦⇩_{τ}P] : (T1 → T2)[X ↦ P]⇩_{τ}" by auto moreover from T_App have "D'[X ↦ P]⇩_{e}@ G ⊢ t2[X ↦⇩_{τ}P] : T1[X ↦ P]⇩_{τ}" by auto ultimately show ?case by auto next case (T_Abs x T1 t2 T2 X P D') then show ?case by force next case (T_Sub t S T X P D') then show ?case using substT_subtype by force next case (T_TAbs X' T1 t2 T2 X P D') then have "X' ♯ ty_dom (D' @ TVarB X Q # G)" and "T1 closed_in (D' @ TVarB X Q # G)" by (auto dest: typing_ok) then have "X' ♯ T1" by (rule closed_in_fresh) with T_TAbs show ?case by force next case (T_TApp X' t1 T2 T11 T12 X P D') then have "X' ♯ ty_dom (D' @ TVarB X Q # G)" by (simp add: fresh_dom) moreover from T_TApp have "T11 closed_in (D' @ TVarB X Q # G)" by (auto dest: subtype_implies_closed) ultimately have X': "X' ♯ T11" by (rule closed_in_fresh) from T_TApp have "D'[X ↦ P]⇩_{e}@ G ⊢ t1[X ↦⇩_{τ}P] : (∀X'<:T11. T12)[X ↦ P]⇩_{τ}" by simp with X' and T_TApp show ?case by (auto simp add: fresh_atm type_substitution_lemma fresh_list_append fresh_list_cons ctxt_subst_fresh' type_subst_fresh subst_trm_ty_fresh intro: substT_subtype) qed lemma Abs_type: ― ‹A.13(1)› assumes H: "Γ ⊢ (λx:S. s) : T" and H': "Γ ⊢ T <: U → U'" and H'': "x ♯ Γ" obtains S' where "Γ ⊢ U <: S" and "(VarB x S) # Γ ⊢ s : S'" and "Γ ⊢ S' <: U'" using H H' H'' proof (nominal_induct Γ t ≡ "λx:S. s" T avoiding: x arbitrary: U U' S s rule: typing.strong_induct) case (T_Abs y T⇩_{1}Γ t⇩_{2}T⇩_{2}) from ‹Γ ⊢ T⇩_{1}→ T⇩_{2}<: U → U'› obtain ty1: "Γ ⊢ U <: S" and ty2: "Γ ⊢ T⇩_{2}<: U'" using T_Abs by cases (simp_all add: ty.inject trm.inject alpha fresh_atm) from T_Abs have "VarB y S # Γ ⊢ [(y, x)] ∙ s : T⇩_{2}" by (simp add: trm.inject alpha fresh_atm) then have "[(y, x)] ∙ (VarB y S # Γ) ⊢ [(y, x)] ∙ [(y, x)] ∙ s : [(y, x)] ∙ T⇩_{2}" by (rule typing.eqvt) moreover from T_Abs have "y ♯ Γ" by (auto dest!: typing_ok simp add: fresh_trm_dom) ultimately have "VarB x S # Γ ⊢ s : T⇩_{2}" using T_Abs by (perm_simp add: ty_vrs_prm_simp) with ty1 show ?case using ty2 by (rule T_Abs) next case (T_Sub Γ t S T) then show ?case using subtype_transitivity by blast qed simp_all lemma subtype_reflexivity_from_typing: assumes "Γ ⊢ t : T" shows "Γ ⊢ T <: T" using assms subtype_reflexivity typing_ok typing_closed_in by simp lemma Abs_type': assumes H: "Γ ⊢ (λx:S. s) : U → U'" and H': "x ♯ Γ" obtains S' where "Γ ⊢ U <: S" and "(VarB x S) # Γ ⊢ s : S'" and "Γ ⊢ S' <: U'" using H subtype_reflexivity_from_typing [OF H] H' by (rule Abs_type) lemma TAbs_type: ― ‹A.13(2)› assumes H: "Γ ⊢ (λX<:S. s) : T" and H': "Γ ⊢ T <: (∀X<:U. U')" and fresh: "X ♯ Γ" "X ♯ S" "X ♯ U" obtains S' where "Γ ⊢ U <: S" and "(TVarB X U # Γ) ⊢ s : S'" and "(TVarB X U # Γ) ⊢ S' <: U'" using H H' fresh proof (nominal_induct Γ t ≡ "λX<:S. s" T avoiding: X U U' S arbitrary: s rule: typing.strong_induct) case (T_TAbs Y T⇩_{1}Γ t⇩_{2}T⇩_{2}) from ‹TVarB Y T⇩_{1}# Γ ⊢ t⇩_{2}: T⇩_{2}› have Y: "Y ♯ Γ" by (auto dest!: typing_ok simp add: valid_ty_dom_fresh) from ‹Y ♯ U'› and ‹Y ♯ X› have "(∀X<:U. U') = (∀Y<:U. [(Y, X)] ∙ U')" by (simp add: ty.inject alpha' fresh_atm) with T_TAbs have "Γ ⊢ (∀Y<:S. T⇩_{2}) <: (∀Y<:U. [(Y, X)] ∙ U')" by (simp add: trm.inject) then obtain ty1: "Γ ⊢ U <: S" and ty2: "(TVarB Y U # Γ) ⊢ T⇩_{2}<: ([(Y, X)] ∙ U')" using T_TAbs Y by (cases rule: subtype_of.strong_cases [where X=Y]) (simp_all add: ty.inject alpha abs_fresh) note ty1 moreover from T_TAbs have "TVarB Y S # Γ ⊢ ([(Y, X)] ∙ s) : T⇩_{2}" by (simp add: trm.inject alpha fresh_atm) then have "[(Y, X)] ∙ (TVarB Y S # Γ) ⊢ [(Y, X)] ∙ [(Y, X)] ∙ s : [(Y, X)] ∙ T⇩_{2}" by (rule typing.eqvt) with ‹X ♯ Γ› ‹X ♯ S› Y ‹Y ♯ S› have "TVarB X S # Γ ⊢ s : [(Y, X)] ∙ T⇩_{2}" by perm_simp then have "TVarB X U # Γ ⊢ s : [(Y, X)] ∙ T⇩_{2}" using ty1 by (rule narrow_type [of "[]", simplified]) moreover from ty2 have "([(Y, X)] ∙ (TVarB Y U # Γ)) ⊢ ([(Y, X)] ∙ T⇩_{2}) <: ([(Y, X)] ∙ [(Y, X)] ∙ U')" by (rule subtype_of.eqvt) with ‹X ♯ Γ› ‹X ♯ U› Y ‹Y ♯ U› have "(TVarB X U # Γ) ⊢ ([(Y, X)] ∙ T⇩_{2}) <: U'" by perm_simp ultimately show ?case by (rule T_TAbs) next case (T_Sub Γ t S T) then show ?case using subtype_transitivity by blast qed simp_all lemma TAbs_type': assumes H: "Γ ⊢ (λX<:S. s) : (∀X<:U. U')" and fresh: "X ♯ Γ" "X ♯ S" "X ♯ U" obtains S' where "Γ ⊢ U <: S" and "(TVarB X U # Γ) ⊢ s : S'" and "(TVarB X U # Γ) ⊢ S' <: U'" using H subtype_reflexivity_from_typing [OF H] fresh by (rule TAbs_type) theorem preservation: ― ‹A.20› assumes H: "Γ ⊢ t : T" shows "t ⟼ t' ⟹ Γ ⊢ t' : T" using H proof (nominal_induct avoiding: t' rule: typing.strong_induct) case (T_App Γ t⇩_{1}T⇩_{1}1 T⇩_{1}2 t⇩_{2}t') obtain x::vrs where x_fresh: "x ♯ (Γ, t⇩_{1}⋅ t⇩_{2}, t')" by (rule exists_fresh) (rule fin_supp) obtain X::tyvrs where "X ♯ (t⇩_{1}⋅ t⇩_{2}, t')" by (rule exists_fresh) (rule fin_supp) with ‹t⇩_{1}⋅ t⇩_{2}⟼ t'› show ?case proof (cases rule: eval.strong_cases [where x=x and X=X]) case (E_Abs v⇩_{2}T⇩_{1}1' t⇩_{1}2) with T_App and x_fresh have h: "Γ ⊢ (λx:T⇩_{1}1'. t⇩_{1}2) : T⇩_{1}1 → T⇩_{1}2" by (simp add: trm.inject fresh_prod) moreover from x_fresh have "x ♯ Γ" by simp ultimately obtain S' where T⇩_{1}1: "Γ ⊢ T⇩_{1}1 <: T⇩_{1}1'" and t⇩_{1}2: "(VarB x T⇩_{1}1') # Γ ⊢ t⇩_{1}2 : S'" and S': "Γ ⊢ S' <: T⇩_{1}2" by (rule Abs_type') blast from ‹Γ ⊢ t⇩_{2}: T⇩_{1}1› have "Γ ⊢ t⇩_{2}: T⇩_{1}1'" using T⇩_{1}1 by (rule T_Sub) with t⇩_{1}2 have "Γ ⊢ t⇩_{1}2[x ↦ t⇩_{2}] : S'" by (rule subst_type [where Δ="[]", simplified]) hence "Γ ⊢ t⇩_{1}2[x ↦ t⇩_{2}] : T⇩_{1}2" using S' by (rule T_Sub) with E_Abs and x_fresh show ?thesis by (simp add: trm.inject fresh_prod) next case (E_App1 t''' t'' u) hence "t⇩_{1}⟼ t''" by (simp add:trm.inject) hence "Γ ⊢ t'' : T⇩_{1}1 → T⇩_{1}2" by (rule T_App) hence "Γ ⊢ t'' ⋅ t⇩_{2}: T⇩_{1}2" using ‹Γ ⊢ t⇩_{2}: T⇩_{1}1› by (rule typing.T_App) with E_App1 show ?thesis by (simp add:trm.inject) next case (E_App2 v t''' t'') hence "t⇩_{2}⟼ t''" by (simp add:trm.inject) hence "Γ ⊢ t'' : T⇩_{1}1" by (rule T_App) with T_App(1) have "Γ ⊢ t⇩_{1}⋅ t'' : T⇩_{1}2" by (rule typing.T_App) with E_App2 show ?thesis by (simp add:trm.inject) qed (simp_all add: fresh_prod) next case (T_TApp X Γ t⇩_{1}T⇩_{2}T⇩_{1}1 T⇩_{1}2 t') obtain x::vrs where "x ♯ (t⇩_{1}⋅⇩_{τ}T⇩_{2}, t')" by (rule exists_fresh) (rule fin_supp) with ‹t⇩_{1}⋅⇩_{τ}T⇩_{2}⟼ t'› show ?case proof (cases rule: eval.strong_cases [where X=X and x=x]) case (E_TAbs T⇩_{1}1' T⇩_{2}' t⇩_{1}2) with T_TApp have "Γ ⊢ (λX<:T⇩_{1}1'. t⇩_{1}2) : (∀X<:T⇩_{1}1. T⇩_{1}2)" and "X ♯ Γ" and "X ♯ T⇩_{1}1'" by (simp_all add: trm.inject) moreover from ‹Γ⊢T⇩_{2}<:T⇩_{1}1› and ‹X ♯ Γ› have "X ♯ T⇩_{1}1" by (blast intro: closed_in_fresh fresh_dom dest: subtype_implies_closed) ultimately obtain S' where "TVarB X T⇩_{1}1 # Γ ⊢ t⇩_{1}2 : S'" and "(TVarB X T⇩_{1}1 # Γ) ⊢ S' <: T⇩_{1}2" by (rule TAbs_type') blast hence "TVarB X T⇩_{1}1 # Γ ⊢ t⇩_{1}2 : T⇩_{1}2" by (rule T_Sub) hence "Γ ⊢ t⇩_{1}2[X ↦⇩_{τ}T⇩_{2}] : T⇩_{1}2[X ↦ T⇩_{2}]⇩_{τ}" using ‹Γ ⊢ T⇩_{2}<: T⇩_{1}1› by (rule substT_type [where D="[]", simplified]) with T_TApp and E_TAbs show ?thesis by (simp add: trm.inject) next case (E_TApp t''' t'' T) from E_TApp have "t⇩_{1}⟼ t''" by (simp add: trm.inject) then have "Γ ⊢ t'' : (∀X<:T⇩_{1}1. T⇩_{1}2)" by (rule T_TApp) then have "Γ ⊢ t'' ⋅⇩_{τ}T⇩_{2}: T⇩_{1}2[X ↦ T⇩_{2}]⇩_{τ}" using ‹Γ ⊢ T⇩_{2}<: T⇩_{1}1› by (rule better_T_TApp) with E_TApp show ?thesis by (simp add: trm.inject) qed (simp_all add: fresh_prod) next case (T_Sub Γ t S T t') have "t ⟼ t'" by fact hence "Γ ⊢ t' : S" by (rule T_Sub) moreover have "Γ ⊢ S <: T" by fact ultimately show ?case by (rule typing.T_Sub) qed (auto) lemma Fun_canonical: ― ‹A.14(1)› assumes ty: "[] ⊢ v : T⇩_{1}→ T⇩_{2}" shows "val v ⟹ ∃x t S. v = (λx:S. t)" using ty proof (induct "[]::env" v "T⇩_{1}→ T⇩_{2}" arbitrary: T⇩_{1}T⇩_{2}) case (T_Sub t S) from ‹[] ⊢ S <: T⇩_{1}→ T⇩_{2}› obtain S⇩_{1}S⇩_{2}where S: "S = S⇩_{1}→ S⇩_{2}" by cases (auto simp add: T_Sub) then show ?case using ‹val t› by (rule T_Sub) qed (auto) lemma TyAll_canonical: ― ‹A.14(3)› fixes X::tyvrs assumes ty: "[] ⊢ v : (∀X<:T⇩_{1}. T⇩_{2})" shows "val v ⟹ ∃X t S. v = (λX<:S. t)" using ty proof (induct "[]::env" v "∀X<:T⇩_{1}. T⇩_{2}" arbitrary: X T⇩_{1}T⇩_{2}) case (T_Sub t S) from ‹[] ⊢ S <: (∀X<:T⇩_{1}. T⇩_{2})› obtain X S⇩_{1}S⇩_{2}where S: "S = (∀X<:S⇩_{1}. S⇩_{2})" by cases (auto simp add: T_Sub) then show ?case using T_Sub by auto qed (auto) theorem progress: assumes "[] ⊢ t : T" shows "val t ∨ (∃t'. t ⟼ t')" using assms proof (induct "[]::env" t T) case (T_App t⇩_{1}T⇩_{1}1 T⇩_{1}2 t⇩_{2}) hence "val t⇩_{1}∨ (∃t'. t⇩_{1}⟼ t')" by simp thus ?case proof assume t⇩_{1}_val: "val t⇩_{1}" with T_App obtain x t3 S where t⇩_{1}: "t⇩_{1}= (λx:S. t3)" by (auto dest!: Fun_canonical) from T_App have "val t⇩_{2}∨ (∃t'. t⇩_{2}⟼ t')" by simp thus ?case proof assume "val t⇩_{2}" with t⇩_{1}have "t⇩_{1}⋅ t⇩_{2}⟼ t3[x ↦ t⇩_{2}]" by auto thus ?case by auto next assume "∃t'. t⇩_{2}⟼ t'" then obtain t' where "t⇩_{2}⟼ t'" by auto with t⇩_{1}_val have "t⇩_{1}⋅ t⇩_{2}⟼ t⇩_{1}⋅ t'" by auto thus ?case by auto qed next assume "∃t'. t⇩_{1}⟼ t'" then obtain t' where "t⇩_{1}⟼ t'" by auto hence "t⇩_{1}⋅ t⇩_{2}⟼ t' ⋅ t⇩_{2}" by auto thus ?case by auto qed next case (T_TApp X t⇩_{1}T⇩_{2}T⇩_{1}1 T⇩_{1}2) hence "val t⇩_{1}∨ (∃t'. t⇩_{1}⟼ t')" by simp thus ?case proof assume "val t⇩_{1}" with T_TApp obtain x t S where "t⇩_{1}= (λx<:S. t)" by (auto dest!: TyAll_canonical) hence "t⇩_{1}⋅⇩_{τ}T⇩_{2}⟼ t[x ↦⇩_{τ}T⇩_{2}]" by auto thus ?case by auto next assume "∃t'. t⇩_{1}⟼ t'" thus ?case by auto qed qed (auto) end