src/HOL/Nominal/Examples/Fsub.thy
author urbanc
Sun Jul 02 17:27:10 2006 +0200 (2006-07-02)
changeset 19972 89c5afe4139a
parent 19501 9afa7183dfc2
child 20395 9a60e3151244
permissions -rw-r--r--
added more infrastructure for the recursion combinator
     1 (* $Id$ *)
     2 
     3 (*<*)
     4 theory Fsub
     5 imports "../Nominal" 
     6 begin
     7 (*>*)
     8 
     9 text{* Authors: Christian Urban,
    10                 Benjamin Pierce,
    11                 Dimitrios Vytiniotis
    12                 Stephanie Weirich and
    13                 Steve Zdancewic
    14 
    15        with great help from Stefan Berghofer and  Markus Wenzel. *}
    16 
    17 section {* Types for Names, Nominal Datatype Declaration for Types and Terms *}
    18 
    19 text {* The main point of this solution is to use names everywhere (be they bound, 
    20   binding or free). In System \FSUB{} there are two kinds of names corresponding to 
    21   type-variables and to term-variables. These two kinds of names are represented in 
    22   the nominal datatype package as atom-types @{text "tyvrs"} and @{text "vrs"}: *}
    23 
    24 atom_decl tyvrs vrs
    25 
    26 text{* There are numerous facts that come with this declaration: for example that 
    27   there are infinitely many elements in @{text "tyvrs"} and @{text "vrs"}. *}
    28 
    29 text{* The constructors for types and terms in System \FSUB{} contain abstractions 
    30   over type-variables and term-variables. The nominal datatype-package uses 
    31   @{text "\<guillemotleft>\<dots>\<guillemotright>\<dots>"} to indicate where abstractions occur. *}
    32 
    33 nominal_datatype ty = 
    34     Tvar   "tyvrs"
    35   | Top
    36   | Arrow  "ty" "ty"          ("_ \<rightarrow> _" [100,100] 100)
    37   | Forall "\<guillemotleft>tyvrs\<guillemotright>ty" "ty" 
    38 
    39 nominal_datatype trm = 
    40     Var   "vrs"
    41   | Lam   "\<guillemotleft>vrs\<guillemotright>trm" "ty" 
    42   | Tabs  "\<guillemotleft>tyvrs\<guillemotright>trm" "ty"
    43   | App   "trm" "trm"
    44   | Tapp  "trm" "ty"
    45 
    46 text {* To be polite to the eye, some more familiar notation is introduced. 
    47   Because of the change in the order of arguments, one needs to use 
    48   translation rules, instead of syntax annotations at the term-constructors
    49   as given above for @{term "Arrow"}. *}
    50 
    51 syntax
    52   Forall_syn :: "tyvrs \<Rightarrow> ty \<Rightarrow> ty \<Rightarrow> ty" ("\<forall>[_<:_]._" [100,100,100] 100)
    53   Lam_syn    :: "vrs \<Rightarrow> ty \<Rightarrow> trm \<Rightarrow> trm"   ("Lam [_:_]._" [100,100,100] 100)
    54   Tabs_syn   :: "tyvrs \<Rightarrow> ty \<Rightarrow> trm \<Rightarrow> trm" ("Tabs [_<:_]._" [100,100,100] 100)
    55 
    56 translations 
    57   "\<forall>[X<:T\<^isub>1].T\<^isub>2" \<rightleftharpoons> "ty.Forall X T\<^isub>2 T\<^isub>1"
    58   "Lam [x:T].t" \<rightleftharpoons> "trm.Lam x t T"
    59   "Tabs [X<:T].t" \<rightleftharpoons> "trm.Tabs X t T"
    60 
    61 text {* Again there are numerous facts that are proved automatically for @{typ "ty"} 
    62   and @{typ "trm"}: for example that the set of free variables, i.e.~the @{text "support"}, 
    63   is finite. However note that nominal-datatype declarations do \emph{not} define 
    64   ``classical" constructor-based datatypes, but rather define $\alpha$-equivalence 
    65   classes---we can for example show that $\alpha$-equivalent @{typ "ty"}s 
    66   and @{typ "trm"}s are equal: *}
    67 
    68 lemma alpha_illustration:
    69   shows "\<forall>[X<:T].(Tvar X) = \<forall>[Y<:T].(Tvar Y)" 
    70   and "Lam [x:T].(Var x) = Lam [y:T].(Var y)"
    71   by (simp_all add: ty.inject trm.inject alpha calc_atm fresh_atm)
    72 
    73 section {* SubTyping Contexts *}
    74 
    75 types ty_context = "(tyvrs\<times>ty) list"
    76 
    77 text {* Typing contexts are represented as lists that ``grow" on the left; we
    78   thereby deviating from the convention in the POPLmark-paper. The lists contain
    79   pairs of type-variables and types (this is sufficient for Part 1A). *}
    80 
    81 text {* In order to state validity-conditions for typing-contexts, the notion of
    82   a @{text "domain"} of a typing-context is handy. *}
    83 
    84 consts
    85   "domain" :: "ty_context \<Rightarrow> tyvrs set"
    86 primrec
    87   "domain [] = {}"
    88   "domain (X#\<Gamma>) = {fst X}\<union>(domain \<Gamma>)" 
    89 
    90 lemma domain_eqvt:
    91   fixes pi::"tyvrs prm"
    92   shows "pi\<bullet>(domain \<Gamma>) = domain (pi\<bullet>\<Gamma>)" 
    93   by (induct \<Gamma>, simp_all add: perm_empty perm_insert perm_fst)
    94 
    95 lemma finite_domain:
    96   shows "finite (domain \<Gamma>)"
    97   by (induct \<Gamma>, auto)
    98 
    99 lemma domain_supp:
   100   shows "(supp (domain \<Gamma>)) = (domain \<Gamma>)"
   101   by (simp only: at_fin_set_supp at_tyvrs_inst finite_domain)
   102 
   103 lemma domain_inclusion:
   104   assumes a: "(X,T)\<in>set \<Gamma>" 
   105   shows "X\<in>(domain \<Gamma>)"
   106   using a by (induct \<Gamma>, auto)
   107 
   108 lemma domain_existence:
   109   assumes a: "X\<in>(domain \<Gamma>)" 
   110   shows "\<exists>T.(X,T)\<in>set \<Gamma>"
   111   using a by (induct \<Gamma>, auto)
   112 
   113 lemma domain_append:
   114   shows "domain (\<Gamma>@\<Delta>) = ((domain \<Gamma>) \<union> (domain \<Delta>))"
   115   by (induct \<Gamma>, auto)
   116 
   117 lemma fresh_domain_cons:
   118   fixes X::"tyvrs"
   119   shows "X\<sharp>(domain (Y#\<Gamma>)) = (X\<sharp>(fst Y) \<and> X\<sharp>(domain \<Gamma>))"
   120   by (simp add: fresh_fin_insert pt_tyvrs_inst at_tyvrs_inst fs_tyvrs_inst finite_domain)
   121 
   122 lemma fresh_domain:
   123   fixes X::"tyvrs"
   124   assumes a: "X\<sharp>\<Gamma>" 
   125   shows "X\<sharp>(domain \<Gamma>)"
   126 using a
   127 apply(induct \<Gamma>)
   128 apply(simp add: fresh_set_empty) 
   129 apply(simp only: fresh_domain_cons)
   130 apply(auto simp add: fresh_prod fresh_list_cons) 
   131 done
   132 
   133 text {* Not all lists of type @{typ "ty_context"} are well-formed. One condition
   134   requires that in @{term "(X,S)#\<Gamma>"} all free variables of @{term "S"} must be 
   135   in the @{term "domain"} of @{term "\<Gamma>"}, that is @{term "S"} must be @{text "closed"} 
   136   in @{term "\<Gamma>"}. The set of free variables of @{term "S"} is the 
   137   @{text "support"} of @{term "S"}. *}
   138 
   139 constdefs
   140   "closed_in" :: "ty \<Rightarrow> ty_context \<Rightarrow> bool" ("_ closed'_in _" [100,100] 100)
   141   "S closed_in \<Gamma> \<equiv> (supp S)\<subseteq>(domain \<Gamma>)"
   142 
   143 lemma closed_in_eqvt:
   144   fixes pi::"tyvrs prm"
   145   assumes a: "S closed_in \<Gamma>" 
   146   shows "(pi\<bullet>S) closed_in (pi\<bullet>\<Gamma>)"
   147   using a
   148 proof (unfold "closed_in_def")
   149   assume "supp S \<subseteq> (domain \<Gamma>)" 
   150   hence "pi\<bullet>(supp S) \<subseteq> pi\<bullet>(domain \<Gamma>)"
   151     by (simp add: pt_subseteq_eqvt[OF pt_tyvrs_inst, OF at_tyvrs_inst])
   152   thus "(supp (pi\<bullet>S)) \<subseteq> (domain (pi\<bullet>\<Gamma>))"
   153     by (simp add: domain_eqvt pt_perm_supp[OF pt_tyvrs_inst, OF at_tyvrs_inst])
   154 qed
   155 
   156 text {* Now validity of a context is a straightforward inductive definition. *}
   157   
   158 consts
   159   valid_rel :: "ty_context set" 
   160   valid_sym :: "ty_context \<Rightarrow> bool" ("\<turnstile> _ ok" [100] 100)
   161 translations
   162   "\<turnstile> \<Gamma> ok" \<rightleftharpoons> "\<Gamma> \<in> valid_rel"  
   163 inductive valid_rel
   164 intros
   165 valid_nil[simp]:  "\<turnstile> [] ok"
   166 valid_cons[simp]: "\<lbrakk>\<turnstile> \<Gamma> ok; X\<sharp>(domain \<Gamma>); T closed_in \<Gamma>\<rbrakk>  \<Longrightarrow>  \<turnstile> ((X,T)#\<Gamma>) ok"
   167 
   168 lemma valid_eqvt:
   169   fixes pi::"tyvrs prm"
   170   assumes a: "\<turnstile> \<Gamma> ok" 
   171   shows "\<turnstile> (pi\<bullet>\<Gamma>) ok"
   172   using a
   173 proof (induct)
   174   case valid_nil
   175   show "\<turnstile> (pi\<bullet>[]) ok" by simp
   176 next
   177   case (valid_cons T X \<Gamma>)
   178   have "\<turnstile> (pi\<bullet>\<Gamma>) ok" by fact
   179   moreover
   180   have "X\<sharp>(domain \<Gamma>)" by fact
   181   hence "(pi\<bullet>X)\<sharp>(domain (pi\<bullet>\<Gamma>))" by (simp add: fresh_bij domain_eqvt[symmetric])
   182   moreover
   183   have "T closed_in \<Gamma>" by fact
   184   hence "(pi\<bullet>T) closed_in (pi\<bullet>\<Gamma>)" by (simp add: closed_in_eqvt)
   185   ultimately show "\<turnstile> (pi\<bullet>((X,T)#\<Gamma>)) ok" by simp
   186 qed
   187 
   188 lemma validE:
   189   assumes a: "\<turnstile> ((X,T)#\<Gamma>) ok"
   190   shows "\<turnstile> \<Gamma> ok \<and> X\<sharp>(domain \<Gamma>) \<and> T closed_in \<Gamma>"
   191 using a by (cases, auto)
   192 
   193 lemma validE_append:
   194   assumes a: "\<turnstile> (\<Delta>@\<Gamma>) ok" 
   195   shows "\<turnstile> \<Gamma> ok"
   196   using a by (induct \<Delta>, auto dest: validE)
   197 
   198 lemma replace_type:
   199   assumes a: "\<turnstile> (\<Delta>@(X,T)#\<Gamma>) ok"
   200   and     b: "S closed_in \<Gamma>"
   201   shows "\<turnstile> (\<Delta>@(X,S)#\<Gamma>) ok"
   202 using a b
   203 apply(induct \<Delta>)
   204 apply(auto dest!: validE intro!: valid_cons simp add: domain_append closed_in_def)
   205 done
   206 
   207 text {* Well-formed contexts have a unique type-binding for a type-variable. *} 
   208 
   209 lemma uniqueness_of_ctxt:
   210   fixes \<Gamma>::"ty_context"
   211   assumes a: "\<turnstile> \<Gamma> ok"
   212   and     b: "(X,T)\<in>set \<Gamma>"
   213   and     c: "(X,S)\<in>set \<Gamma>"
   214   shows "T=S"
   215 using a b c
   216 proof (induct)
   217   case valid_nil thus "T=S" by simp
   218 next
   219   case (valid_cons U Y \<Gamma>)
   220   moreover
   221   { fix \<Gamma>::"ty_context"
   222     assume a: "X\<sharp>(domain \<Gamma>)" 
   223     have "\<not>(\<exists>T.(X,T)\<in>(set \<Gamma>))" using a 
   224     proof (induct \<Gamma>)
   225       case (Cons Y \<Gamma>)
   226       thus "\<not> (\<exists>T.(X,T)\<in>set(Y#\<Gamma>))" 
   227 	by (simp only: fresh_domain_cons, auto simp add: fresh_atm)
   228     qed (simp)
   229   }
   230   ultimately show "T=S" by auto
   231 qed 
   232 
   233 section {* Size and Capture-Avoiding Substitution for Types *}
   234 
   235 text {* In the current version of the nominal datatype package even simple 
   236   functions (such as size of types and capture-avoiding substitution) can 
   237   only be defined manually via some laborious proof constructions. Therefore 
   238   we just assume them here. Cheat! *}
   239 
   240 consts size_ty :: "ty \<Rightarrow> nat"
   241 
   242 lemma size_ty[simp]:
   243   shows "size_ty (Tvar X) = 1"
   244   and   "size_ty (Top) = 1"
   245   and   "\<lbrakk>size_ty T\<^isub>1 = m; size_ty T\<^isub>2 = n\<rbrakk> \<Longrightarrow> size_ty (T\<^isub>1 \<rightarrow> T\<^isub>2) = m + n + 1"
   246   and   "\<lbrakk>size_ty T\<^isub>1 = m; size_ty T\<^isub>2 = n\<rbrakk> \<Longrightarrow> size_ty (\<forall>[X<:T\<^isub>1].T\<^isub>2) = m + n + 1"
   247 sorry
   248 
   249 consts subst_ty :: "ty \<Rightarrow> tyvrs \<Rightarrow> ty \<Rightarrow> ty" ("_[_:=_]\<^isub>t\<^isub>y" [100,100,100] 100)
   250 
   251 lemma subst_ty[simp]:
   252   shows "(Tvar X)[Y:=T]\<^isub>t\<^isub>y = (if X=Y then T else (Tvar X))"
   253   and   "(Top)[Y:=T]\<^isub>t\<^isub>y = Top"
   254   and   "(T\<^isub>1 \<rightarrow> T\<^isub>2)[Y:=T]\<^isub>t\<^isub>y = (T\<^isub>1[Y:=T]\<^isub>t\<^isub>y) \<rightarrow> (T\<^isub>2[Y:=T]\<^isub>t\<^isub>y)"
   255   and   "X\<sharp>(Y,T) \<Longrightarrow> (\<forall>[X<:T\<^isub>1].T\<^isub>2)[Y:=T]\<^isub>t\<^isub>y = (\<forall>[X<:(T\<^isub>1[Y:=T]\<^isub>t\<^isub>y)].(T\<^isub>2[Y:=T]\<^isub>t\<^isub>y))"
   256   and   "\<lbrakk>X\<sharp>Y; X\<sharp>T\<rbrakk> \<Longrightarrow> (\<forall>[X<:T\<^isub>1].T\<^isub>2)[Y:=T]\<^isub>t\<^isub>y = (\<forall>[X<:(T\<^isub>1[Y:=T]\<^isub>t\<^isub>y)].(T\<^isub>2[Y:=T]\<^isub>t\<^isub>y))"
   257 sorry
   258 
   259 consts subst_tyc :: "ty_context \<Rightarrow> tyvrs \<Rightarrow> ty \<Rightarrow> ty_context" ("_[_:=_]\<^isub>t\<^isub>y\<^isub>c" [100,100,100] 100)
   260 primrec
   261 "([])[Y:=T]\<^isub>t\<^isub>y\<^isub>c= []"
   262 "(XT#\<Gamma>)[Y:=T]\<^isub>t\<^isub>y\<^isub>c = (fst XT,(snd XT)[Y:=T]\<^isub>t\<^isub>y)#(\<Gamma>[Y:=T]\<^isub>t\<^isub>y\<^isub>c)"
   263  
   264 section {* Subtyping-Relation *}
   265 
   266 text {* The definition for the subtyping-relation follows quite closely what is written 
   267   in the POPLmark-paper, except for the premises dealing with well-formed contexts and 
   268   the freshness constraint @{term "X\<sharp>\<Gamma>"} in the @{text "S_Forall"}-rule. (The freshness
   269   constraint is specific to the \emph{nominal approach}. Note, however, that the constraint
   270   does \emph{not} make the subtyping-relation ``partial"\ldots because we work over
   271   $\alpha$-equivalence classes.) *}
   272 
   273 consts
   274   subtype_of :: "(ty_context \<times> ty \<times> ty) set"   
   275 syntax 
   276   subtype_of_syn :: "ty_context \<Rightarrow> ty \<Rightarrow> ty \<Rightarrow> bool"   ("_\<turnstile>_<:_" [100,100,100] 100)
   277 
   278 translations
   279   "\<Gamma> \<turnstile> S <: T" \<rightleftharpoons> "(\<Gamma>,S,T) \<in> subtype_of"
   280 inductive subtype_of
   281 intros
   282 S_Top[intro]:    "\<lbrakk>\<turnstile> \<Gamma> ok; S closed_in \<Gamma>\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> S <: Top"
   283 S_Var[intro]:    "\<lbrakk>(X,S) \<in> set \<Gamma>; \<Gamma> \<turnstile> S <: T\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> (Tvar X) <: T"
   284 S_Refl[intro]:   "\<lbrakk>\<turnstile> \<Gamma> ok; X \<in> domain \<Gamma>\<rbrakk>\<Longrightarrow> \<Gamma> \<turnstile> Tvar X <: Tvar X"
   285 S_Arrow[intro]:  "\<lbrakk>\<Gamma> \<turnstile> T\<^isub>1 <: S\<^isub>1; \<Gamma> \<turnstile> S\<^isub>2 <: T\<^isub>2\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> (S\<^isub>1 \<rightarrow> S\<^isub>2) <: (T\<^isub>1 \<rightarrow> T\<^isub>2)" 
   286 S_Forall[intro]: "\<lbrakk>\<Gamma> \<turnstile> T\<^isub>1 <: S\<^isub>1; X\<sharp>\<Gamma>; ((X,T\<^isub>1)#\<Gamma>) \<turnstile> S\<^isub>2 <: T\<^isub>2\<rbrakk> 
   287                  \<Longrightarrow> \<Gamma> \<turnstile> \<forall>[X<:S\<^isub>1].S\<^isub>2 <: \<forall>[X<:T\<^isub>1].T\<^isub>2"  
   288 
   289 lemma subtype_implies_closed:
   290   assumes a: "\<Gamma> \<turnstile> S <: T"
   291   shows "S closed_in \<Gamma> \<and> T closed_in \<Gamma>"
   292 using a
   293 proof (induct)
   294   case (S_Top S \<Gamma>)
   295   have "Top closed_in \<Gamma>" by (simp add: closed_in_def ty.supp)
   296   moreover
   297   have "S closed_in \<Gamma>" by fact
   298   ultimately show "S closed_in \<Gamma> \<and> Top closed_in \<Gamma>" by simp
   299 next
   300   case (S_Var S T X \<Gamma>)
   301   have "(X,S)\<in>set \<Gamma>" by fact
   302   hence "X \<in> domain \<Gamma>" by (rule domain_inclusion)
   303   hence "(Tvar X) closed_in \<Gamma>" by (simp add: closed_in_def ty.supp supp_atm)
   304   moreover
   305   have "S closed_in \<Gamma> \<and> T closed_in \<Gamma>" by fact
   306   hence "T closed_in \<Gamma>" by force
   307   ultimately show "(Tvar X) closed_in \<Gamma> \<and> T closed_in \<Gamma>" by simp
   308 qed (auto simp add: closed_in_def ty.supp supp_atm abs_supp)
   309 
   310 lemma subtype_implies_ok:
   311   fixes X::"tyvrs"
   312   assumes a1: "\<Gamma> \<turnstile> S <: T"
   313   shows "\<turnstile> \<Gamma> ok"  
   314 using a1 by (induct, auto)
   315 
   316 lemma subtype_implies_fresh:
   317   fixes X::"tyvrs"
   318   assumes a1: "\<Gamma> \<turnstile> S <: T"
   319   and     a2: "X\<sharp>\<Gamma>"
   320   shows "X\<sharp>S \<and> X\<sharp>T"  
   321 proof -
   322   from a1 have "\<turnstile> \<Gamma> ok" by (rule subtype_implies_ok)
   323   with a2 have "X\<sharp>domain(\<Gamma>)" by (simp add: fresh_domain)
   324   moreover
   325   from a1 have "S closed_in \<Gamma> \<and> T closed_in \<Gamma>" by (rule subtype_implies_closed)
   326   hence "supp S \<subseteq> ((supp (domain \<Gamma>))::tyvrs set)" 
   327     and "supp T \<subseteq> ((supp (domain \<Gamma>))::tyvrs set)" by (simp_all add: domain_supp closed_in_def)
   328   ultimately show "X\<sharp>S \<and> X\<sharp>T" by (force simp add: supp_prod fresh_def)
   329 qed
   330 
   331 lemma subtype_eqvt:
   332   fixes pi::"tyvrs prm"
   333   shows "\<Gamma> \<turnstile> S <: T \<Longrightarrow> (pi\<bullet>\<Gamma>) \<turnstile> (pi\<bullet>S) <: (pi\<bullet>T)"
   334 apply(erule subtype_of.induct)
   335 apply(force intro: valid_eqvt closed_in_eqvt)
   336 apply(force intro!: S_Var
   337             intro: closed_in_eqvt valid_eqvt 
   338             dest: pt_set_bij2[OF pt_tyvrs_inst, OF at_tyvrs_inst]
   339             simp add: pt_list_set_pi[OF pt_tyvrs_inst, symmetric])
   340 apply(force intro: valid_eqvt
   341             dest: pt_set_bij2[OF pt_tyvrs_inst, OF at_tyvrs_inst]
   342             simp add: domain_eqvt)
   343 apply(force)
   344 apply(force intro!: S_Forall simp add: fresh_prod fresh_bij)
   345 done
   346 
   347 text {* The most painful part of the subtyping definition is the strengthening of the
   348   induction principle. The induction principle that comes for free with the definition of 
   349   @{term "subtype_of"} requires to prove the @{text "S_Forall"}-case for \emph{all} binders
   350   @{text "X"}. This will often cause some renaming-manoeuvres in the reasoning. To avoid this,
   351   we strengthening the induction-principle so that we only have to establish
   352   the @{text "S_Forall"}-case for \emph{fresh} binders @{text "X"}. The property that allows
   353   us to strengthen the induction-principle is that the equivariance of @{text "subtype_of"}. *}
   354 
   355 lemma subtype_of_induct[consumes 1, case_names S_Top S_Var S_Refl S_Arrow S_Forall]:
   356   fixes  P :: "'a::fs_tyvrs\<Rightarrow>ty_context \<Rightarrow> ty \<Rightarrow> ty \<Rightarrow>bool"
   357   assumes a: "\<Gamma> \<turnstile> S <: T"
   358   and a1: "\<And>\<Gamma> S x. \<lbrakk>\<turnstile> \<Gamma> ok; S closed_in \<Gamma>\<rbrakk> \<Longrightarrow> P x \<Gamma> S Top"
   359   and a2: "\<And>\<Gamma> X S T x. \<lbrakk>(X,S)\<in>set \<Gamma>; \<Gamma> \<turnstile> S <: T; \<And>z. P z \<Gamma> S T\<rbrakk> \<Longrightarrow> P x \<Gamma> (Tvar X) T"
   360   and a3: "\<And>\<Gamma> X x. \<lbrakk>\<turnstile> \<Gamma> ok; X\<in>domain \<Gamma>\<rbrakk> \<Longrightarrow> P x \<Gamma> (Tvar X) (Tvar X)"  
   361   and a4: "\<And>\<Gamma> S\<^isub>1 S\<^isub>2 T\<^isub>1 T\<^isub>2 x. 
   362   \<lbrakk>\<Gamma> \<turnstile> T\<^isub>1 <: S\<^isub>1; \<And>z. P z \<Gamma> T\<^isub>1 S\<^isub>1; \<Gamma> \<turnstile> S\<^isub>2 <: T\<^isub>2; \<And>z. P z \<Gamma> S\<^isub>2 T\<^isub>2\<rbrakk> 
   363   \<Longrightarrow> P x \<Gamma> (S\<^isub>1 \<rightarrow> S\<^isub>2) (T\<^isub>1 \<rightarrow> T\<^isub>2)"
   364   and a5: "\<And>\<Gamma> X S\<^isub>1 S\<^isub>2 T\<^isub>1 T\<^isub>2 x. 
   365   \<lbrakk>X\<sharp>x; X\<sharp>(\<Gamma>,S\<^isub>1,T\<^isub>1); \<Gamma> \<turnstile> T\<^isub>1 <: S\<^isub>1; \<And>z. P z \<Gamma> T\<^isub>1 S\<^isub>1; 
   366   ((X,T\<^isub>1)#\<Gamma>) \<turnstile> S\<^isub>2 <: T\<^isub>2; \<And>z. P z ((X,T\<^isub>1)#\<Gamma>) S\<^isub>2 T\<^isub>2\<rbrakk>
   367   \<Longrightarrow> P x \<Gamma> (\<forall>[X<:S\<^isub>1].S\<^isub>2) (\<forall>[X<:T\<^isub>1].T\<^isub>2)"
   368   shows "P x \<Gamma> S T"
   369 proof -
   370   from a have "\<And>(pi::tyvrs prm) (x::'a::fs_tyvrs). P x (pi\<bullet>\<Gamma>) (pi\<bullet>S) (pi\<bullet>T)"
   371   proof (induct)
   372     case (S_Top S \<Gamma>) 
   373     thus "P x (pi\<bullet>\<Gamma>) (pi\<bullet>S) (pi\<bullet>Top)" by (force intro: valid_eqvt closed_in_eqvt a1)
   374   next
   375     case (S_Var S T X \<Gamma>)
   376     have "(X,S) \<in> set \<Gamma>" by fact
   377     hence "pi\<bullet>(X,S)\<in>pi\<bullet>(set \<Gamma>)" by (rule pt_set_bij2[OF pt_tyvrs_inst, OF at_tyvrs_inst])
   378     hence "(pi\<bullet>X,pi\<bullet>S)\<in>set (pi\<bullet>\<Gamma>)" by (simp add: pt_list_set_pi[OF pt_tyvrs_inst])
   379     moreover
   380     have "\<Gamma> \<turnstile> S <: T" by fact
   381     hence "(pi\<bullet>\<Gamma>) \<turnstile> (pi\<bullet>S) <: (pi\<bullet>T)" by (rule subtype_eqvt)
   382     moreover
   383     have  "\<And>(pi::tyvrs prm) x. P x (pi\<bullet>\<Gamma>) (pi\<bullet>S) (pi\<bullet>T)" by fact
   384     hence "\<And>x. P x (pi\<bullet>\<Gamma>) (pi\<bullet>S) (pi\<bullet>T)" by simp
   385     ultimately 
   386     show "P x (pi\<bullet>\<Gamma>) (pi\<bullet>(Tvar X)) (pi\<bullet>T)" by (simp add: a2)
   387   next
   388     case (S_Refl X \<Gamma>)
   389     have "\<turnstile> \<Gamma> ok" by fact
   390     hence "\<turnstile> (pi\<bullet>\<Gamma>) ok" by (rule valid_eqvt)
   391     moreover
   392     have "X \<in> domain \<Gamma>" by fact
   393     hence "(pi\<bullet>X)\<in>pi\<bullet>domain \<Gamma>" by (rule pt_set_bij2[OF pt_tyvrs_inst, OF at_tyvrs_inst])
   394     hence "(pi\<bullet>X)\<in>domain (pi\<bullet>\<Gamma>)" by (simp add: domain_eqvt pt_list_set_pi[OF pt_tyvrs_inst])
   395     ultimately show "P x (pi\<bullet>\<Gamma>) (pi\<bullet>(Tvar X)) (pi\<bullet>(Tvar X))" by (simp add: a3)
   396   next
   397     case S_Arrow thus ?case by (auto intro: a4 subtype_eqvt)
   398   next
   399     case (S_Forall S1 S2 T1 T2 X \<Gamma>)
   400     have b1: "\<Gamma> \<turnstile> T1 <: S1" by fact 
   401     have b2: "\<And>(pi::tyvrs prm) x. P x (pi\<bullet>\<Gamma>) (pi\<bullet>T1) (pi\<bullet>S1)" by fact
   402     have b4: "((X,T1)#\<Gamma>) \<turnstile> S2 <: T2" by fact
   403     have b5: "\<And>(pi::tyvrs prm) x. P x (pi\<bullet>((X,T1)#\<Gamma>)) (pi\<bullet>S2) (pi\<bullet>T2)" by fact
   404     have b3: "X\<sharp>\<Gamma>" by fact
   405     have b3': "X\<sharp>T1" "X\<sharp>S1" using b1 b3 by (simp_all add: subtype_implies_fresh)
   406     have "\<exists>C::tyvrs. C\<sharp>(pi\<bullet>X,pi\<bullet>S2,pi\<bullet>T2,pi\<bullet>S1,pi\<bullet>T1,pi\<bullet>\<Gamma>,x)"
   407       by (rule at_exists_fresh[OF at_tyvrs_inst], simp add: fs_tyvrs1)
   408     then obtain C::"tyvrs" where  f1: "C\<noteq>(pi\<bullet>X)" and f2: "C\<sharp>(pi\<bullet>S1)" and f3: "C\<sharp>(pi\<bullet>T1)"
   409       and f4: "C\<sharp>(pi\<bullet>S2)" and f5: "C\<sharp>(pi\<bullet>T2)" and f6: "C\<sharp>(pi\<bullet>\<Gamma>)" and f7: "C\<sharp>x"
   410       by (auto simp add: fresh_prod fresh_atm)
   411     let ?pi' = "[(C,pi\<bullet>X)]@pi"
   412     from b2 have c1: "\<And>x. P x (?pi'\<bullet>\<Gamma>) (?pi'\<bullet>T1) (?pi'\<bullet>S1)" by simp
   413     from b5 have "\<And>x. P x (?pi'\<bullet>((X,T1)#\<Gamma>)) (?pi'\<bullet>S2) (?pi'\<bullet>T2)" by simp
   414     hence "\<And>x. P x ((?pi'\<bullet>X,?pi'\<bullet>T1)#(?pi'\<bullet>\<Gamma>)) (?pi'\<bullet>S2) (?pi'\<bullet>T2)" by simp
   415     hence c2: "\<And>x. P x ((C,?pi'\<bullet>T1)#(?pi'\<bullet>\<Gamma>)) (?pi'\<bullet>S2) (?pi'\<bullet>T2)" using f1
   416       by (simp only: pt_tyvrs2 calc_atm, simp)
   417     from b3 have "(pi\<bullet>X)\<sharp>(pi\<bullet>\<Gamma>)" 
   418       by (simp add: fresh_prod pt_fresh_bij[OF pt_tyvrs_inst, OF at_tyvrs_inst])
   419     with f6 have f6a: "?pi'\<bullet>\<Gamma>=pi\<bullet>\<Gamma>" 
   420       by (simp only: pt_tyvrs2 pt_fresh_fresh[OF pt_tyvrs_inst, OF at_tyvrs_inst])
   421     hence f6': "C\<sharp>(?pi'\<bullet>\<Gamma>)" using f6 by simp
   422     from b3' have "(pi\<bullet>X)\<sharp>(pi\<bullet>S1)" 
   423       by (simp add: fresh_prod pt_fresh_bij[OF pt_tyvrs_inst, OF at_tyvrs_inst])
   424     with f2 have f2a: "?pi'\<bullet>S1=pi\<bullet>S1" 
   425       by (simp only: pt_tyvrs2 pt_fresh_fresh[OF pt_tyvrs_inst, OF at_tyvrs_inst])
   426     hence f2': "C\<sharp>(?pi'\<bullet>S1)" using f2 by simp
   427     from b3' have "(pi\<bullet>X)\<sharp>(pi\<bullet>T1)" 
   428       by (simp add: fresh_prod pt_fresh_bij[OF pt_tyvrs_inst, OF at_tyvrs_inst])
   429     with f3 have f3a: "?pi'\<bullet>T1=pi\<bullet>T1" 
   430       by (simp only: pt_tyvrs2 pt_fresh_fresh[OF pt_tyvrs_inst, OF at_tyvrs_inst])
   431     hence f3': "C\<sharp>(?pi'\<bullet>T1)" using f3 by simp
   432     from b1 have e1: "(?pi'\<bullet>\<Gamma>) \<turnstile> (?pi'\<bullet>T1) <: (?pi'\<bullet>S1)" by (rule subtype_eqvt)
   433     from b4 have "(?pi'\<bullet>((X,T1)#\<Gamma>)) \<turnstile> (?pi'\<bullet>S2) <: (?pi'\<bullet>T2)" by (rule subtype_eqvt)
   434     hence "((?pi'\<bullet>X,?pi'\<bullet>T1)#(?pi'\<bullet>\<Gamma>)) \<turnstile> (?pi'\<bullet>S2) <: (?pi'\<bullet>T2)" by simp
   435     hence e2: "((C,?pi'\<bullet>T1)#(?pi'\<bullet>\<Gamma>)) \<turnstile> (?pi'\<bullet>S2) <: (?pi'\<bullet>T2)" using f1
   436       by (simp only: pt_tyvrs2 calc_atm, simp)
   437     have fnew: "C\<sharp>(?pi'\<bullet>\<Gamma>,?pi'\<bullet>S1,?pi'\<bullet>T1)" using f6' f2' f3' by (simp add: fresh_prod)
   438     have main: "P x (?pi'\<bullet>\<Gamma>) (\<forall>[C<:(?pi'\<bullet>S1)].(?pi'\<bullet>S2)) (\<forall>[C<:(?pi'\<bullet>T1)].(?pi'\<bullet>T2))"
   439       using f7 fnew e1 c1 e2 c2 by (rule a5)
   440     have alpha1: "(\<forall>[C<:(?pi'\<bullet>S1)].(?pi'\<bullet>S2)) = (pi\<bullet>(\<forall>[X<:S1].S2))"
   441       using f1 f4 f2a[symmetric] by (simp add: ty.inject alpha pt_tyvrs2[symmetric])
   442     have alpha2: "(\<forall>[C<:(?pi'\<bullet>T1)].(?pi'\<bullet>T2)) = (pi\<bullet>(\<forall>[X<:T1].T2))"
   443       using f1 f5 f3a[symmetric] by (simp add: ty.inject alpha pt_tyvrs2[symmetric])
   444     show "P x (pi\<bullet>\<Gamma>) (pi\<bullet>(\<forall>[X<:S1].S2)) (pi\<bullet>(\<forall>[X<:T1].T2))"
   445       using alpha1 alpha2 f6a main by simp  
   446   qed
   447   hence "P x (([]::tyvrs prm)\<bullet>\<Gamma>) (([]::tyvrs prm)\<bullet>S) (([]::tyvrs prm)\<bullet>T)" by blast
   448   thus ?thesis by simp
   449 qed
   450 
   451 section {* Reflexivity of Subtyping *}
   452 
   453 lemma subtype_reflexivity:
   454   assumes a: "\<turnstile> \<Gamma> ok"
   455   and b: "T closed_in \<Gamma>"
   456   shows "\<Gamma> \<turnstile> T <: T"
   457 using a b
   458 proof(nominal_induct T avoiding: \<Gamma> rule: ty.induct)
   459   case (Forall X T\<^isub>1 T\<^isub>2)
   460   have ih_T\<^isub>1: "\<And>\<Gamma>. \<lbrakk>\<turnstile> \<Gamma> ok; T\<^isub>1 closed_in \<Gamma>\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> T\<^isub>1 <: T\<^isub>1" by fact 
   461   have ih_T\<^isub>2: "\<And>\<Gamma>. \<lbrakk>\<turnstile> \<Gamma> ok; T\<^isub>2 closed_in \<Gamma>\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> T\<^isub>2 <: T\<^isub>2" by fact
   462   have fresh_cond: "X\<sharp>\<Gamma>" by fact
   463   hence fresh_domain: "X\<sharp>(domain \<Gamma>)" by (simp add: fresh_domain)
   464   have "(\<forall>[X<:T\<^isub>2].T\<^isub>1) closed_in \<Gamma>" by fact
   465   hence closed\<^isub>T\<^isub>2: "T\<^isub>2 closed_in \<Gamma>" and closed\<^isub>T\<^isub>1: "T\<^isub>1 closed_in ((X,T\<^isub>2)#\<Gamma>)" 
   466     by (auto simp add: closed_in_def ty.supp abs_supp)
   467   have ok: "\<turnstile> \<Gamma> ok" by fact  
   468   hence ok': "\<turnstile> ((X,T\<^isub>2)#\<Gamma>) ok" using closed\<^isub>T\<^isub>2 fresh_domain by simp
   469   have "\<Gamma> \<turnstile> T\<^isub>2 <: T\<^isub>2" using ih_T\<^isub>2 closed\<^isub>T\<^isub>2 ok by simp
   470   moreover
   471   have "((X,T\<^isub>2)#\<Gamma>) \<turnstile> T\<^isub>1 <: T\<^isub>1" using ih_T\<^isub>1 closed\<^isub>T\<^isub>1 ok' by simp
   472   ultimately show "\<Gamma> \<turnstile> \<forall>[X<:T\<^isub>2].T\<^isub>1 <: \<forall>[X<:T\<^isub>2].T\<^isub>1" using fresh_cond 
   473     by (simp add: subtype_of.S_Forall)
   474 qed (auto simp add: closed_in_def ty.supp supp_atm)
   475 
   476 lemma subtype_reflexivity_semiautomated:
   477   assumes a: "\<turnstile> \<Gamma> ok"
   478   and     b: "T closed_in \<Gamma>"
   479   shows "\<Gamma> \<turnstile> T <: T"
   480 using a b
   481 apply(nominal_induct T avoiding: \<Gamma> rule: ty.induct)
   482 apply(auto simp add: ty.supp abs_supp supp_atm closed_in_def)
   483   --{* Too bad that this instantiation cannot be found automatically by
   484   \isakeyword{auto}; \isakeyword{blast} would find it if we had not used 
   485   an explicit definition for @{text "closed_in_def"}. *}
   486 apply(drule_tac x="(tyvrs, ty2)#\<Gamma>" in meta_spec)
   487 apply(force dest: fresh_domain simp add: closed_in_def)
   488 done
   489 
   490 
   491 section {* Weakening *}
   492 
   493 text {* In order to prove weakening we introduce the notion of a type-context extending 
   494   another. This generalization seems to make the proof for weakening to be
   495   smoother than if we had strictly adhered to the version in the POPLmark-paper. *}
   496 
   497 constdefs 
   498   extends :: "ty_context \<Rightarrow> ty_context \<Rightarrow> bool" ("_ extends _" [100,100] 100)
   499   "\<Delta> extends \<Gamma> \<equiv> \<forall>X Q. (X,Q)\<in>set \<Gamma> \<longrightarrow> (X,Q)\<in>set \<Delta>"
   500 
   501 lemma extends_domain:
   502   assumes a: "\<Delta> extends \<Gamma>"
   503   shows "domain \<Gamma> \<subseteq> domain \<Delta>"
   504   using a 
   505   apply (auto simp add: extends_def)
   506   apply (drule domain_existence)
   507   apply (force simp add: domain_inclusion)
   508   done
   509 
   510 lemma extends_closed:
   511   assumes a1: "T closed_in \<Gamma>"
   512   and     a2: "\<Delta> extends \<Gamma>"
   513   shows "T closed_in \<Delta>"
   514   using a1 a2
   515   by (auto dest: extends_domain simp add: closed_in_def)
   516 
   517 lemma extends_memb:
   518   assumes a: "\<Delta> extends \<Gamma>"
   519   and b: "(X,T) \<in> set \<Gamma>"
   520   shows "(X,T) \<in> set \<Delta>"
   521   using a b by (simp add: extends_def)
   522 
   523 lemma weakening:
   524   assumes a: "\<Gamma> \<turnstile> S <: T"
   525   and b: "\<turnstile> \<Delta> ok"
   526   and c: "\<Delta> extends \<Gamma>"
   527   shows "\<Delta> \<turnstile> S <: T"
   528   using a b c 
   529 proof (nominal_induct \<Gamma> S T avoiding: \<Delta> rule: subtype_of_induct)
   530   case (S_Top \<Gamma> S) 
   531   have lh_drv_prem: "S closed_in \<Gamma>" by fact
   532   have "\<turnstile> \<Delta> ok" by fact
   533   moreover
   534   have "\<Delta> extends \<Gamma>" by fact
   535   hence "S closed_in \<Delta>" using lh_drv_prem by (simp only: extends_closed)
   536   ultimately show "\<Delta> \<turnstile> S <: Top" by force
   537 next 
   538   case (S_Var \<Gamma> X S T)
   539   have lh_drv_prem: "(X,S) \<in> set \<Gamma>" by fact
   540   have ih: "\<And>\<Delta>. \<turnstile> \<Delta> ok \<Longrightarrow> \<Delta> extends \<Gamma> \<Longrightarrow> \<Delta> \<turnstile> S <: T" by fact
   541   have ok: "\<turnstile> \<Delta> ok" by fact
   542   have extends: "\<Delta> extends \<Gamma>" by fact
   543   have "(X,S) \<in> set \<Delta>" using lh_drv_prem extends by (simp only: extends_memb)
   544   moreover
   545   have "\<Delta> \<turnstile> S <: T" using ok extends ih by simp
   546   ultimately show "\<Delta> \<turnstile> Tvar X <: T" using ok by force
   547 next
   548   case (S_Refl \<Gamma> X)
   549   have lh_drv_prem: "X \<in> domain \<Gamma>" by fact
   550   have "\<turnstile> \<Delta> ok" by fact
   551   moreover
   552   have "\<Delta> extends \<Gamma>" by fact
   553   hence "X \<in> domain \<Delta>" using lh_drv_prem by (force dest: extends_domain)
   554   ultimately show "\<Delta> \<turnstile> Tvar X <: Tvar X" by force
   555 next 
   556   case (S_Arrow \<Gamma> S\<^isub>1 S\<^isub>2 T\<^isub>1 T\<^isub>2) thus "\<Delta> \<turnstile> S\<^isub>1 \<rightarrow> S\<^isub>2 <: T\<^isub>1 \<rightarrow> T\<^isub>2" by blast
   557 next
   558   case (S_Forall \<Gamma> X S\<^isub>1 S\<^isub>2 T\<^isub>1 T\<^isub>2)
   559   have fresh_cond: "X\<sharp>\<Delta>" by fact
   560   hence fresh_domain: "X\<sharp>(domain \<Delta>)" by (simp add: fresh_domain)
   561   have ih\<^isub>1: "\<And>\<Delta>. \<turnstile> \<Delta> ok \<Longrightarrow> \<Delta> extends \<Gamma> \<Longrightarrow> \<Delta> \<turnstile> T\<^isub>1 <: S\<^isub>1" by fact
   562   have ih\<^isub>2: "\<And>\<Delta>. \<turnstile> \<Delta> ok \<Longrightarrow> \<Delta> extends ((X,T\<^isub>1)#\<Gamma>) \<Longrightarrow> \<Delta> \<turnstile> S\<^isub>2 <: T\<^isub>2" by fact
   563   have lh_drv_prem: "\<Gamma> \<turnstile> T\<^isub>1 <: S\<^isub>1" by fact
   564   hence closed\<^isub>T\<^isub>1: "T\<^isub>1 closed_in \<Gamma>" by (simp add: subtype_implies_closed) 
   565   have ok: "\<turnstile> \<Delta> ok" by fact
   566   have ext: "\<Delta> extends \<Gamma>" by fact
   567   have "T\<^isub>1 closed_in \<Delta>" using ext closed\<^isub>T\<^isub>1 by (simp only: extends_closed)
   568   hence "\<turnstile> ((X,T\<^isub>1)#\<Delta>) ok" using fresh_domain ok by force   
   569   moreover 
   570   have "((X,T\<^isub>1)#\<Delta>) extends ((X,T\<^isub>1)#\<Gamma>)" using ext by (force simp add: extends_def)
   571   ultimately have "((X,T\<^isub>1)#\<Delta>) \<turnstile> S\<^isub>2 <: T\<^isub>2" using ih\<^isub>2 by simp
   572   moreover
   573   have "\<Delta> \<turnstile> T\<^isub>1 <: S\<^isub>1" using ok ext ih\<^isub>1 by simp 
   574   ultimately show "\<Delta> \<turnstile> \<forall>[X<:S\<^isub>1].S\<^isub>2 <: \<forall>[X<:T\<^isub>1].T\<^isub>2" using ok by (force intro: S_Forall)
   575 qed
   576 
   577 text {* In fact all ``non-binding" cases can be solved automatically: *}
   578 
   579 lemma weakening_more_automated:
   580   assumes a: "\<Gamma> \<turnstile> S <: T"
   581   and b: "\<turnstile> \<Delta> ok"
   582   and c: "\<Delta> extends \<Gamma>"
   583   shows "\<Delta> \<turnstile> S <: T"
   584   using a b c 
   585 proof (nominal_induct \<Gamma> S T avoiding: \<Delta> rule: subtype_of_induct)
   586   case (S_Forall \<Gamma> X S\<^isub>1 S\<^isub>2 T\<^isub>1 T\<^isub>2)
   587   have fresh_cond: "X\<sharp>\<Delta>" by fact
   588   hence fresh_domain: "X\<sharp>(domain \<Delta>)" by (simp add: fresh_domain)
   589   have ih\<^isub>1: "\<And>\<Delta>. \<turnstile> \<Delta> ok \<Longrightarrow> \<Delta> extends \<Gamma> \<Longrightarrow> \<Delta> \<turnstile> T\<^isub>1 <: S\<^isub>1" by fact
   590   have ih\<^isub>2: "\<And>\<Delta>. \<turnstile> \<Delta> ok \<Longrightarrow> \<Delta> extends ((X,T\<^isub>1)#\<Gamma>) \<Longrightarrow> \<Delta> \<turnstile> S\<^isub>2 <: T\<^isub>2" by fact
   591   have lh_drv_prem: "\<Gamma> \<turnstile> T\<^isub>1 <: S\<^isub>1" by fact
   592   hence closed\<^isub>T\<^isub>1: "T\<^isub>1 closed_in \<Gamma>" by (simp add: subtype_implies_closed) 
   593   have ok: "\<turnstile> \<Delta> ok" by fact
   594   have ext: "\<Delta> extends \<Gamma>" by fact
   595   have "T\<^isub>1 closed_in \<Delta>" using ext closed\<^isub>T\<^isub>1 by (simp only: extends_closed)
   596   hence "\<turnstile> ((X,T\<^isub>1)#\<Delta>) ok" using fresh_domain ok by force   
   597   moreover
   598   have "((X,T\<^isub>1)#\<Delta>) extends ((X,T\<^isub>1)#\<Gamma>)" using ext by (force simp add: extends_def)
   599   ultimately have "((X,T\<^isub>1)#\<Delta>) \<turnstile> S\<^isub>2 <: T\<^isub>2" using ih\<^isub>2 by simp
   600   moreover
   601   have "\<Delta> \<turnstile> T\<^isub>1 <: S\<^isub>1" using ok ext ih\<^isub>1 by simp 
   602   ultimately show "\<Delta> \<turnstile> \<forall>[X<:S\<^isub>1].S\<^isub>2 <: \<forall>[X<:T\<^isub>1].T\<^isub>2" using ok by (force intro: S_Forall)
   603 qed (blast intro: extends_closed extends_memb dest: extends_domain)+
   604 
   605 section {* Transitivity and Narrowing *}
   606 
   607 text {* Some inversion lemmas that are needed in the transitivity and narrowing proof.*}
   608 
   609 lemma S_TopE:
   610   assumes a: "\<Gamma> \<turnstile> Top <: T"
   611   shows "T = Top"
   612 using a by (cases, auto) 
   613 
   614 lemma S_ArrowE_left:
   615   assumes a: "\<Gamma> \<turnstile> S\<^isub>1 \<rightarrow> S\<^isub>2 <: T" 
   616   shows "T = Top \<or> (\<exists>T\<^isub>1 T\<^isub>2. T = T\<^isub>1 \<rightarrow> T\<^isub>2 \<and> \<Gamma> \<turnstile> T\<^isub>1 <: S\<^isub>1 \<and> \<Gamma> \<turnstile> S\<^isub>2 <: T\<^isub>2)"
   617 using a by (cases, auto simp add: ty.inject)
   618 
   619 lemma S_ForallE_left:
   620   shows "\<lbrakk>\<Gamma> \<turnstile> \<forall>[X<:S\<^isub>1].S\<^isub>2 <: T; X\<sharp>\<Gamma>; X\<sharp>S\<^isub>1\<rbrakk>
   621          \<Longrightarrow> T = Top \<or> (\<exists>T\<^isub>1 T\<^isub>2. T = \<forall>[X<:T\<^isub>1].T\<^isub>2 \<and> \<Gamma> \<turnstile> T\<^isub>1 <: S\<^isub>1 \<and> ((X,T\<^isub>1)#\<Gamma>) \<turnstile> S\<^isub>2 <: T\<^isub>2)"
   622   apply(frule subtype_implies_ok)
   623   apply(ind_cases "\<Gamma> \<turnstile> \<forall>[X<:S\<^isub>1].S\<^isub>2 <: T")
   624   apply(auto simp add: ty.inject alpha)
   625   apply(rule_tac x="[(X,Xa)]\<bullet>T\<^isub>2" in exI)
   626   apply(rule conjI)
   627   apply(rule sym)
   628   apply(rule pt_bij2[OF pt_tyvrs_inst, OF at_tyvrs_inst])
   629   apply(rule pt_tyvrs3)
   630   apply(simp)
   631   apply(rule at_ds5[OF at_tyvrs_inst])
   632   apply(rule conjI)
   633   apply(simp add: pt_fresh_left[OF pt_tyvrs_inst, OF at_tyvrs_inst] calc_atm)
   634   apply(drule_tac \<Gamma>="((Xa,T\<^isub>1)#\<Gamma>)" in  subtype_implies_closed)+
   635   apply(simp add: closed_in_def)
   636   apply(drule fresh_domain)+
   637   apply(simp add: fresh_def)
   638   apply(subgoal_tac "X \<notin> (insert Xa (domain \<Gamma>))")(*A*)
   639   apply(force)
   640   (*A*)apply(simp add: at_fin_set_supp[OF at_tyvrs_inst, OF finite_domain])
   641   (* 2nd conjunct *)apply(frule_tac X="X" in subtype_implies_fresh)
   642   apply(assumption)
   643   apply(drule_tac X="Xa" in subtype_implies_fresh)
   644   apply(assumption)
   645   apply(simp add: fresh_prod)
   646   apply(drule_tac pi="[(X,Xa)]" in subtype_eqvt)
   647   apply(simp add: calc_atm)
   648   apply(simp add: pt_fresh_fresh[OF pt_tyvrs_inst, OF at_tyvrs_inst])
   649   done
   650 
   651 text {* Next we prove the transitivity and narrowing for the subtyping-relation. 
   652 The POPLmark-paper says the following:
   653 
   654 \begin{quote}
   655 \begin{lemma}[Transitivity and Narrowing] \
   656 \begin{enumerate}
   657 \item If @{term "\<Gamma> \<turnstile> S<:Q"} and @{term "\<Gamma> \<turnstile> Q<:T"}, then @{term "\<Gamma> \<turnstile> S<:T"}.
   658 \item If @{text "\<Gamma>,X<:Q,\<Delta> \<turnstile> M<:N"} and @{term "\<Gamma> \<turnstile> P<:Q"} then @{text "\<Gamma>,X<:P,\<Delta> \<turnstile> M<:N"}.
   659 \end{enumerate}
   660 \end{lemma}
   661 
   662 The two parts are proved simultaneously, by induction on the size
   663 of @{term "Q"}.  The argument for part (2) assumes that part (1) has 
   664 been established already for the @{term "Q"} in question; part (1) uses 
   665 part (2) only for strictly smaller @{term "Q"}.
   666 \end{quote}
   667 
   668 For the induction on the size of @{term "Q"}, we use the induction-rule 
   669 @{text "measure_induct_rule"}:
   670 
   671 \begin{center}
   672 @{thm measure_induct_rule[of "size_ty",no_vars]}
   673 \end{center}
   674 
   675 That means in order to show a property @{term "P a"} for all @{term "a"}, 
   676 the induct-rule requires to prove that for all @{term x} @{term "P x"} holds using the 
   677 assumption that for all @{term y} whose size is strictly smaller than 
   678 that of @{term x} the property @{term "P y"} holds. *}
   679 
   680 lemma 
   681   shows trans: "\<Gamma>\<turnstile>S<:Q \<Longrightarrow> \<Gamma>\<turnstile>Q<:T \<Longrightarrow> \<Gamma>\<turnstile>S<:T" 
   682   and narrow: "(\<Delta>@[(X,Q)]@\<Gamma>)\<turnstile>M<:N \<Longrightarrow> \<Gamma>\<turnstile>P<:Q \<Longrightarrow> (\<Delta>@[(X,P)]@\<Gamma>)\<turnstile>M<:N"
   683 proof (induct Q fixing: \<Gamma> S T \<Delta> X P M N taking: "size_ty" rule: measure_induct_rule)
   684   case (less Q)
   685     --{* \begin{minipage}[t]{0.9\textwidth}
   686     First we mention the induction hypotheses of the outer induction for later
   687     reference:\end{minipage}*}
   688   have IH_trans:  
   689     "\<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
   690   have IH_narrow:
   691     "\<And>Q' \<Delta> \<Gamma> X M N P. \<lbrakk>size_ty Q' < size_ty Q; (\<Delta>@[(X,Q')]@\<Gamma>)\<turnstile>M<:N; \<Gamma>\<turnstile>P<:Q'\<rbrakk> 
   692     \<Longrightarrow> (\<Delta>@[(X,P)]@\<Gamma>)\<turnstile>M<:N" by fact
   693     --{* \begin{minipage}[t]{0.9\textwidth}
   694     We proceed with the transitivity proof as an auxiliary lemma, because it needs 
   695     to be referenced in the narrowing proof.\end{minipage}*}
   696   have transitivity_aux:
   697     "\<And>\<Gamma> S T. \<lbrakk>\<Gamma> \<turnstile> S <: Q; \<Gamma> \<turnstile> Q <: T\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> S <: T"
   698   proof - 
   699     fix \<Gamma>' S' T
   700     assume "\<Gamma>' \<turnstile> S' <: Q" --{* left-hand derivation *}
   701       and  "\<Gamma>' \<turnstile> Q <: T"  --{* right-hand derivation *}
   702     thus "\<Gamma>' \<turnstile> S' <: T"
   703     proof (nominal_induct \<Gamma>' S' Q\<equiv>Q rule: subtype_of_induct) 
   704       case (S_Top \<Gamma> S) 
   705 	--{* \begin{minipage}[t]{0.9\textwidth}
   706 	In this case the left-hand derivation is @{term "\<Gamma> \<turnstile> S <: Top"}, giving
   707 	us @{term "\<turnstile> \<Gamma> ok"} and @{term "S closed_in \<Gamma>"}. This case is straightforward, 
   708 	because the right-hand derivation must be of the form @{term "\<Gamma> \<turnstile> Top <: Top"} 
   709 	giving us the equation @{term "T = Top"}.\end{minipage}*}
   710       hence rh_drv: "\<Gamma> \<turnstile> Top <: T" by simp
   711       hence T_inst: "T = Top" by (simp add: S_TopE)
   712       have "\<turnstile> \<Gamma> ok" 
   713 	and "S closed_in \<Gamma>" by fact
   714       hence "\<Gamma> \<turnstile> S <: Top" by (simp add: subtype_of.S_Top)
   715       thus "\<Gamma> \<turnstile> S <: T" using T_inst by simp
   716     next
   717       case (S_Var \<Gamma> Y U) 
   718 	-- {* \begin{minipage}[t]{0.9\textwidth}
   719 	In this case the left-hand derivation is @{term "\<Gamma> \<turnstile> Tvar Y <: Q"} 
   720 	with @{term "S = Tvar Y"}. We have therefore @{term "(Y,U)"} 
   721 	is in @{term "\<Gamma>"} and by inner induction hypothesis that @{term "\<Gamma> \<turnstile> U <: T"}. 
   722 	By @{text "S_Var"} follows @{term "\<Gamma> \<turnstile> Tvar Y <: T"}.\end{minipage}*}
   723       hence IH_inner: "\<Gamma> \<turnstile> U <: T" by simp
   724       have "(Y,U) \<in> set \<Gamma>" by fact
   725       with IH_inner show "\<Gamma> \<turnstile> Tvar Y <: T" by (simp add: subtype_of.S_Var)
   726     next
   727       case (S_Refl \<Gamma> X) 
   728 	--{* \begin{minipage}[t]{0.9\textwidth}
   729         In this case the left-hand derivation is @{term "\<Gamma>\<turnstile>(Tvar X) <: (Tvar X)"} with
   730         @{term "Q=Tvar X"}. The goal then follows immediately from the right-hand 
   731 	derivation.\end{minipage}*}
   732       thus "\<Gamma> \<turnstile> Tvar X <: T" by simp
   733     next
   734       case (S_Arrow \<Gamma> S\<^isub>1 S\<^isub>2 Q\<^isub>1 Q\<^isub>2) 
   735 	--{* \begin{minipage}[t]{0.9\textwidth}
   736 	In this case the left-hand derivation is @{term "\<Gamma> \<turnstile> S\<^isub>1 \<rightarrow> S\<^isub>2 <: Q\<^isub>1 \<rightarrow> Q\<^isub>2"} with
   737         @{term "S\<^isub>1\<rightarrow>S\<^isub>2=S"} and @{term "Q\<^isub>1\<rightarrow>Q\<^isub>2=Q"}. We know that the @{text "size_ty"} of 
   738 	@{term Q\<^isub>1} and @{term Q\<^isub>2} is smaller than that of @{term Q};
   739 	so we can apply the outer induction hypotheses for @{term Q\<^isub>1} and @{term Q\<^isub>2}. 
   740 	We also have the sub-derivations  @{term "\<Gamma>\<turnstile>Q\<^isub>1<:S\<^isub>1"} and @{term "\<Gamma>\<turnstile>S\<^isub>2<:Q\<^isub>2"}.
   741 	The right-hand derivation is @{term "\<Gamma> \<turnstile> Q\<^isub>1 \<rightarrow> Q\<^isub>2 <: T"}. There exist types 
   742 	@{text "T\<^isub>1,T\<^isub>2"} such that @{term "T=Top \<or> T=T\<^isub>1\<rightarrow>T\<^isub>2"}. The @{term "Top"}-case is 
   743 	straightforward once we know @{term "(S\<^isub>1 \<rightarrow> S\<^isub>2) closed_in \<Gamma>"} and @{term "\<turnstile> \<Gamma> ok"}. 
   744 	In the other case we have the sub-derivations @{term "\<Gamma>\<turnstile>T\<^isub>1<:Q\<^isub>1"} and @{term "\<Gamma>\<turnstile>Q\<^isub>2<:T\<^isub>2"}. 
   745 	Using the outer induction hypothesis for transitivity we can derive @{term "\<Gamma>\<turnstile>T\<^isub>1<:S\<^isub>1"} 
   746 	and @{term "\<Gamma>\<turnstile>S\<^isub>2<:T\<^isub>2"}. By rule @{text "S_Arrow"} follows @{term "\<Gamma> \<turnstile> S\<^isub>1 \<rightarrow> S\<^isub>2 <: T\<^isub>1 \<rightarrow> T\<^isub>2"},
   747 	which is @{term "\<Gamma> \<turnstile> S\<^isub>1 \<rightarrow> S\<^isub>2 <: T\<^isub>"}.\end{minipage}*}
   748       hence rh_drv: "\<Gamma> \<turnstile> Q\<^isub>1 \<rightarrow> Q\<^isub>2 <: T" by simp
   749       from `Q\<^isub>1 \<rightarrow> Q\<^isub>2 = Q` 
   750       have Q\<^isub>1\<^isub>2_less: "size_ty Q\<^isub>1 < size_ty Q" "size_ty Q\<^isub>2 < size_ty Q" by auto
   751       have lh_drv_prm\<^isub>1: "\<Gamma> \<turnstile> Q\<^isub>1 <: S\<^isub>1" by fact
   752       have lh_drv_prm\<^isub>2: "\<Gamma> \<turnstile> S\<^isub>2 <: Q\<^isub>2" by fact      
   753       from rh_drv have "T=Top \<or> (\<exists>T\<^isub>1 T\<^isub>2. T=T\<^isub>1\<rightarrow>T\<^isub>2 \<and> \<Gamma>\<turnstile>T\<^isub>1<:Q\<^isub>1 \<and> \<Gamma>\<turnstile>Q\<^isub>2<:T\<^isub>2)" 
   754 	by (simp add: S_ArrowE_left)  
   755       moreover
   756       have "S\<^isub>1 closed_in \<Gamma>" and "S\<^isub>2 closed_in \<Gamma>" 
   757 	using lh_drv_prm\<^isub>1 lh_drv_prm\<^isub>2 by (simp_all add: subtype_implies_closed)
   758       hence "(S\<^isub>1 \<rightarrow> S\<^isub>2) closed_in \<Gamma>" by (simp add: closed_in_def ty.supp)
   759       moreover
   760       have "\<turnstile> \<Gamma> ok" using rh_drv by (rule subtype_implies_ok)
   761       moreover
   762       { assume "\<exists>T\<^isub>1 T\<^isub>2. T=T\<^isub>1\<rightarrow>T\<^isub>2 \<and> \<Gamma>\<turnstile>T\<^isub>1<:Q\<^isub>1 \<and> \<Gamma>\<turnstile>Q\<^isub>2<:T\<^isub>2"
   763 	then obtain T\<^isub>1 T\<^isub>2 
   764 	  where T_inst: "T = T\<^isub>1 \<rightarrow> T\<^isub>2" 
   765 	  and   rh_drv_prm\<^isub>1: "\<Gamma> \<turnstile> T\<^isub>1 <: Q\<^isub>1"
   766 	  and   rh_drv_prm\<^isub>2: "\<Gamma> \<turnstile> Q\<^isub>2 <: T\<^isub>2" by force
   767 	from IH_trans[of "Q\<^isub>1"] 
   768 	have "\<Gamma> \<turnstile> T\<^isub>1 <: S\<^isub>1" using Q\<^isub>1\<^isub>2_less rh_drv_prm\<^isub>1 lh_drv_prm\<^isub>1 by simp 
   769 	moreover
   770 	from IH_trans[of "Q\<^isub>2"] 
   771 	have "\<Gamma> \<turnstile> S\<^isub>2 <: T\<^isub>2" using Q\<^isub>1\<^isub>2_less rh_drv_prm\<^isub>2 lh_drv_prm\<^isub>2 by simp
   772 	ultimately have "\<Gamma> \<turnstile> S\<^isub>1 \<rightarrow> S\<^isub>2 <: T\<^isub>1 \<rightarrow> T\<^isub>2" by (simp add: subtype_of.S_Arrow)
   773 	hence "\<Gamma> \<turnstile> S\<^isub>1 \<rightarrow> S\<^isub>2 <: T" using T_inst by simp
   774       }
   775       ultimately show "\<Gamma> \<turnstile> S\<^isub>1 \<rightarrow> S\<^isub>2 <: T" by blast
   776     next
   777       case (S_Forall \<Gamma> X S\<^isub>1 S\<^isub>2 Q\<^isub>1 Q\<^isub>2) 
   778 	--{* \begin{minipage}[t]{0.9\textwidth}
   779 	In this case the left-hand derivation is @{text "\<Gamma>\<turnstile>\<forall>[X<:S\<^isub>1].S\<^isub>2 <: \<forall>[X<:Q\<^isub>1].Q\<^isub>2"} with 
   780 	@{text "\<forall>[X<:S\<^isub>1].S\<^isub>2=S"} and @{text "\<forall>[X<:Q\<^isub>1].Q\<^isub>2=Q"}. We therefore have the sub-derivations  
   781 	@{term "\<Gamma>\<turnstile>Q\<^isub>1<:S\<^isub>1"} and @{term "((X,Q\<^isub>1)#\<Gamma>)\<turnstile>S\<^isub>2<:Q\<^isub>2"}. Since @{term "X"} is a binder, we
   782 	assume that it is sufficiently fresh; in particular we have the freshness conditions
   783 	@{term "X\<sharp>\<Gamma>"} and @{term "X\<sharp>Q\<^isub>1"} (these assumptions are provided by the strong 
   784 	induction-rule @{text "subtype_of_induct"}). We know that the @{text "size_ty"} of 
   785 	@{term Q\<^isub>1} and @{term Q\<^isub>2} is smaller than that of @{term Q};
   786 	so we can apply the outer induction hypotheses for @{term Q\<^isub>1} and @{term Q\<^isub>2}. 
   787 	The right-hand derivation is @{text "\<Gamma> \<turnstile> \<forall>[X<:Q\<^isub>1].Q\<^isub>2 <: T"}. Since @{term "X\<sharp>\<Gamma>"} 
   788 	and @{term "X\<sharp>Q\<^isub>1"} there exists types @{text "T\<^isub>1,T\<^isub>2"} such that 
   789 	@{text "T=Top \<or> T=\<forall>[X<:T\<^isub>1].T\<^isub>2"}. The @{term "Top"}-case is straightforward once we know 
   790 	@{text "(\<forall>[X<:S\<^isub>1].S\<^isub>2) closed_in \<Gamma>"} and @{term "\<turnstile> \<Gamma> ok"}. In the other case we have 
   791 	the sub-derivations @{term "\<Gamma>\<turnstile>T\<^isub>1<:Q\<^isub>1"} and @{term "((X,T\<^isub>1)#\<Gamma>)\<turnstile>Q\<^isub>2<:T\<^isub>2"}. Using the outer 
   792 	induction hypothesis for transitivity we can derive @{term "\<Gamma>\<turnstile>T\<^isub>1<:S\<^isub>1"}. From the outer 
   793 	induction for narrowing we get @{term "((X,T\<^isub>1)#\<Gamma>) \<turnstile> S\<^isub>2 <: Q\<^isub>2"} and then using again 
   794 	induction for transitivity we obtain @{term "((X,T\<^isub>1)#\<Gamma>) \<turnstile> S\<^isub>2 <: T\<^isub>2"}. By rule 
   795 	@{text "S_Forall"} and the freshness condition @{term "X\<sharp>\<Gamma>"} follows 
   796 	@{text "\<Gamma> \<turnstile> \<forall>[X<:S\<^isub>1].S\<^isub>2 <: \<forall>[X<:T\<^isub>1].T\<^isub>2"}, which is @{text "\<Gamma> \<turnstile>  \<forall>[X<:S\<^isub>1].S\<^isub>2 <: T\<^isub>"}.
   797 	\end{minipage}*}
   798       hence rh_drv: "\<Gamma> \<turnstile> \<forall>[X<:Q\<^isub>1].Q\<^isub>2 <: T" by simp
   799       have lh_drv_prm\<^isub>1: "\<Gamma> \<turnstile> Q\<^isub>1 <: S\<^isub>1" by fact
   800       have lh_drv_prm\<^isub>2: "((X,Q\<^isub>1)#\<Gamma>) \<turnstile> S\<^isub>2 <: Q\<^isub>2" by fact
   801       have fresh_cond: "X\<sharp>\<Gamma>" "X\<sharp>Q\<^isub>1" by fact
   802       from `\<forall>[X<:Q\<^isub>1].Q\<^isub>2 = Q` 
   803       have Q\<^isub>1\<^isub>2_less: "size_ty Q\<^isub>1 < size_ty Q" "size_ty Q\<^isub>2 < size_ty Q " by auto
   804       from rh_drv 
   805       have "T=Top \<or> (\<exists>T\<^isub>1 T\<^isub>2. T=\<forall>[X<:T\<^isub>1].T\<^isub>2 \<and> \<Gamma>\<turnstile>T\<^isub>1<:Q\<^isub>1 \<and> ((X,T\<^isub>1)#\<Gamma>)\<turnstile>Q\<^isub>2<:T\<^isub>2)" 
   806 	using fresh_cond by (simp add: S_ForallE_left)
   807       moreover
   808       have "S\<^isub>1 closed_in \<Gamma>" and "S\<^isub>2 closed_in ((X,Q\<^isub>1)#\<Gamma>)" 
   809 	using lh_drv_prm\<^isub>1 lh_drv_prm\<^isub>2 by (simp_all add: subtype_implies_closed)
   810       hence "(\<forall>[X<:S\<^isub>1].S\<^isub>2) closed_in \<Gamma>" by (force simp add: closed_in_def ty.supp abs_supp)
   811       moreover
   812       have "\<turnstile> \<Gamma> ok" using rh_drv by (rule subtype_implies_ok)
   813       moreover
   814       { assume "\<exists>T\<^isub>1 T\<^isub>2. T=\<forall>[X<:T\<^isub>1].T\<^isub>2 \<and> \<Gamma>\<turnstile>T\<^isub>1<:Q\<^isub>1 \<and> ((X,T\<^isub>1)#\<Gamma>)\<turnstile>Q\<^isub>2<:T\<^isub>2"
   815 	then obtain T\<^isub>1 T\<^isub>2 
   816 	  where T_inst: "T = \<forall>[X<:T\<^isub>1].T\<^isub>2" 
   817 	  and   rh_drv_prm\<^isub>1: "\<Gamma> \<turnstile> T\<^isub>1 <: Q\<^isub>1" 
   818 	  and   rh_drv_prm\<^isub>2:"((X,T\<^isub>1)#\<Gamma>) \<turnstile> Q\<^isub>2 <: T\<^isub>2" by force
   819 	from IH_trans[of "Q\<^isub>1"] 
   820 	have "\<Gamma> \<turnstile> T\<^isub>1 <: S\<^isub>1" using lh_drv_prm\<^isub>1 rh_drv_prm\<^isub>1 Q\<^isub>1\<^isub>2_less by blast
   821 	moreover
   822 	from IH_narrow[of "Q\<^isub>1" "[]"] 
   823 	have "((X,T\<^isub>1)#\<Gamma>) \<turnstile> S\<^isub>2 <: Q\<^isub>2" using Q\<^isub>1\<^isub>2_less lh_drv_prm\<^isub>2 rh_drv_prm\<^isub>1 by simp
   824 	with IH_trans[of "Q\<^isub>2"] 
   825 	have "((X,T\<^isub>1)#\<Gamma>) \<turnstile> S\<^isub>2 <: T\<^isub>2" using Q\<^isub>1\<^isub>2_less rh_drv_prm\<^isub>2 by simp
   826 	ultimately have "\<Gamma> \<turnstile> \<forall>[X<:S\<^isub>1].S\<^isub>2 <: \<forall>[X<:T\<^isub>1].T\<^isub>2"
   827 	  using fresh_cond by (simp add: subtype_of.S_Forall)
   828 	hence "\<Gamma> \<turnstile> \<forall>[X<:S\<^isub>1].S\<^isub>2 <: T" using T_inst by simp
   829       }
   830       ultimately show "\<Gamma> \<turnstile> \<forall>[X<:S\<^isub>1].S\<^isub>2 <: T" by blast
   831     qed
   832   qed
   833 
   834   { --{* The transitivity proof is now by the auxiliary lemma. *}
   835     case 1 
   836     have  "\<Gamma> \<turnstile> S <: Q" 
   837       and "\<Gamma> \<turnstile> Q <: T" by fact
   838     thus "\<Gamma> \<turnstile> S <: T" by (rule transitivity_aux) 
   839   next 
   840     --{* The narrowing proof proceeds by an induction over @{term "(\<Delta>@[(X,Q)]@\<Gamma>) \<turnstile> M <: N"}. *}
   841     case 2
   842     have  "(\<Delta>@[(X,Q)]@\<Gamma>) \<turnstile> M <: N" --{* left-hand derivation *}
   843       and "\<Gamma> \<turnstile> P<:Q" by fact --{* right-hand derivation *}
   844     thus "(\<Delta>@[(X,P)]@\<Gamma>) \<turnstile> M <: N" 
   845     proof (nominal_induct \<Gamma>\<equiv>"\<Delta>@[(X,Q)]@\<Gamma>" M N avoiding: \<Delta> \<Gamma> X rule: subtype_of_induct) 
   846       case (S_Top _ S \<Delta> \<Gamma> X)
   847 	--{* \begin{minipage}[t]{0.9\textwidth}
   848 	In this case the left-hand derivation is @{term "(\<Delta>@[(X,Q)]@\<Gamma>) \<turnstile> S <: Top"}. We show
   849 	that the context @{term "\<Delta>@[(X,P)]@\<Gamma>"} is ok and that @{term S} is closed in 
   850 	@{term "\<Delta>@[(X,P)]@\<Gamma>"}. Then we can apply the @{text "S_Top"}-rule.\end{minipage}*}
   851       hence lh_drv_prm\<^isub>1: "\<turnstile> (\<Delta>@[(X,Q)]@\<Gamma>) ok" 
   852 	and lh_drv_prm\<^isub>2: "S closed_in (\<Delta>@[(X,Q)]@\<Gamma>)" by simp_all
   853       have rh_drv: "\<Gamma> \<turnstile> P <: Q" by fact
   854       hence "P closed_in \<Gamma>" by (simp add: subtype_implies_closed)
   855       with lh_drv_prm\<^isub>1 have "\<turnstile> (\<Delta>@[(X,P)]@\<Gamma>) ok" by (simp add: replace_type)
   856       moreover
   857       from lh_drv_prm\<^isub>2 have "S closed_in (\<Delta>@[(X,P)]@\<Gamma>)" 
   858 	by (simp add: closed_in_def domain_append)
   859       ultimately show "(\<Delta>@[(X,P)]@\<Gamma>) \<turnstile> S <: Top" by (simp add: subtype_of.S_Top)
   860     next
   861       case (S_Var _ Y S N \<Delta> \<Gamma> X) 
   862 	--{* \begin{minipage}[t]{0.9\textwidth}
   863 	In this case the left-hand derivation is @{term "(\<Delta>@[(X,Q)]@\<Gamma>) \<turnstile> Tvar Y <: N"} and
   864 	by inner induction hypothesis we have @{term "(\<Delta>@[(X,P)]@\<Gamma>) \<turnstile> S <: N"}. We therefore 
   865 	know that the contexts @{term "\<Delta>@[(X,Q)]@\<Gamma>"} and @{term "\<Delta>@[(X,P)]@\<Gamma>"} are ok, and that 
   866 	@{term "(Y,S)"} is in @{term "\<Delta>@[(X,Q)]@\<Gamma>"}. We need to show that 
   867 	@{term "(\<Delta>@[(X,P)]@\<Gamma>) \<turnstile> Tvar Y <: N"}  holds. In case @{term "X\<noteq>Y"} we know that 
   868 	@{term "(Y,S)"} is in @{term "\<Delta>@[(X,P)]@\<Gamma>"} and can use the inner induction hypothesis 
   869 	and rule @{text "S_Var"} to conclude. In case @{term "X=Y"} we can infer that 
   870 	@{term "S=Q"}; moreover we have that  @{term "(\<Delta>@[(X,P)]@\<Gamma>) extends \<Gamma>"} and therefore 
   871 	by @{text "weakening"} that @{term "(\<Delta>@[(X,P)]@\<Gamma>) \<turnstile> P <: Q"} holds. By transitivity we 
   872 	obtain then @{term "(\<Delta>@[(X,P)]@\<Gamma>) \<turnstile> P <: N"} and can conclude by applying rule 
   873 	@{text "S_Var"}.\end{minipage}*}
   874       hence IH_inner: "(\<Delta>@[(X,P)]@\<Gamma>) \<turnstile> S <: N"
   875 	and lh_drv_prm: "(Y,S) \<in> set (\<Delta>@[(X,Q)]@\<Gamma>)"
   876 	and rh_drv: "\<Gamma> \<turnstile> P<:Q"
   877 	and ok\<^isub>Q: "\<turnstile> (\<Delta>@[(X,Q)]@\<Gamma>) ok" by (simp_all add: subtype_implies_ok)
   878       hence ok\<^isub>P: "\<turnstile> (\<Delta>@[(X,P)]@\<Gamma>) ok" by (simp add: subtype_implies_ok) 
   879       show "(\<Delta>@[(X,P)]@\<Gamma>) \<turnstile> Tvar Y <: N"
   880       proof (cases "X=Y")
   881 	case False
   882 	have "X\<noteq>Y" by fact
   883 	hence "(Y,S)\<in>set (\<Delta>@[(X,P)]@\<Gamma>)" using lh_drv_prm by simp
   884 	with IH_inner show "(\<Delta>@[(X,P)]@\<Gamma>) \<turnstile> Tvar Y <: N" by (simp add: subtype_of.S_Var)
   885       next
   886 	case True
   887 	have memb\<^isub>X\<^isub>Q: "(X,Q)\<in>set (\<Delta>@[(X,Q)]@\<Gamma>)" by simp
   888 	have memb\<^isub>X\<^isub>P: "(X,P)\<in>set (\<Delta>@[(X,P)]@\<Gamma>)" by simp
   889 	have eq: "X=Y" by fact 
   890 	hence "S=Q" using ok\<^isub>Q lh_drv_prm memb\<^isub>X\<^isub>Q by (simp only: uniqueness_of_ctxt)
   891 	hence "(\<Delta>@[(X,P)]@\<Gamma>) \<turnstile> Q <: N" using IH_inner by simp
   892 	moreover
   893 	have "(\<Delta>@[(X,P)]@\<Gamma>) extends \<Gamma>" by (simp add: extends_def)
   894 	hence "(\<Delta>@[(X,P)]@\<Gamma>) \<turnstile> P <: Q" using rh_drv ok\<^isub>P by (simp only: weakening)
   895 	ultimately have "(\<Delta>@[(X,P)]@\<Gamma>) \<turnstile> P <: N" by (simp add: transitivity_aux) 
   896 	thus "(\<Delta>@[(X,P)]@\<Gamma>) \<turnstile> Tvar Y <: N" using memb\<^isub>X\<^isub>P eq by (simp only: subtype_of.S_Var)
   897       qed
   898     next
   899       case (S_Refl _ Y \<Delta> \<Gamma> X)
   900 	--{* \begin{minipage}[t]{0.9\textwidth}
   901 	In this case the left-hand derivation is @{term "(\<Delta>@[(X,Q)]@\<Gamma>) \<turnstile> Tvar Y <: Tvar Y"} and we
   902 	therefore know that @{term "\<Delta>@[(X,Q)]@\<Gamma>"} is ok and that @{term "Y"} is in 
   903 	the domain of @{term "\<Delta>@[(X,Q)]@\<Gamma>"}. We therefore know that @{term "\<Delta>@[(X,P)]@\<Gamma>"} is ok
   904 	and that @{term Y} is in the domain of @{term "\<Delta>@[(X,P)]@\<Gamma>"}. We can conclude by applying 
   905 	rule @{text "S_Refl"}.\end{minipage}*}
   906       hence lh_drv_prm\<^isub>1: "\<turnstile> (\<Delta>@[(X,Q)]@\<Gamma>) ok" 
   907 	and lh_drv_prm\<^isub>2: "Y \<in> domain (\<Delta>@[(X,Q)]@\<Gamma>)" by simp_all
   908       have "\<Gamma> \<turnstile> P <: Q" by fact
   909       hence "P closed_in \<Gamma>" by (simp add: subtype_implies_closed)
   910       with lh_drv_prm\<^isub>1 have "\<turnstile> (\<Delta>@[(X,P)]@\<Gamma>) ok" by (simp add: replace_type)
   911       moreover
   912       from lh_drv_prm\<^isub>2 have "Y \<in> domain (\<Delta>@[(X,P)]@\<Gamma>)" by (simp add: domain_append)
   913       ultimately show "(\<Delta>@[(X,P)]@\<Gamma>) \<turnstile> Tvar Y <: Tvar Y" by (simp add: subtype_of.S_Refl)
   914     next
   915       case (S_Arrow _ Q\<^isub>1 Q\<^isub>2 S\<^isub>1 S\<^isub>2 \<Delta> \<Gamma> X) 
   916 	--{* \begin{minipage}[t]{0.9\textwidth}
   917 	In this case the left-hand derivation is @{term "(\<Delta>@[(X,Q)]@\<Gamma>) \<turnstile> Q\<^isub>1 \<rightarrow> Q\<^isub>2 <: S\<^isub>1 \<rightarrow> S\<^isub>2"} 
   918 	and the proof is trivial.\end{minipage}*}
   919       thus "(\<Delta>@[(X,P)]@\<Gamma>) \<turnstile> Q\<^isub>1 \<rightarrow> Q\<^isub>2 <: S\<^isub>1 \<rightarrow> S\<^isub>2" by blast 
   920     next
   921       case (S_Forall _ Y S\<^isub>1 S\<^isub>2 T\<^isub>1 T\<^isub>2 \<Delta> \<Gamma> X)
   922 	--{* \begin{minipage}[t]{0.9\textwidth}
   923 	In this case the left-hand derivation is @{text "(\<Delta>@[(X,Q)]@\<Gamma>) \<turnstile> \<forall>[Y<:S\<^isub>1].S\<^isub>2 <: \<forall>[Y<:T\<^isub>1].T\<^isub>2"}
   924 	and therfore we know that the binder @{term Y} is fresh for @{term "\<Delta>@[(X,Q)]@\<Gamma>"}. By
   925 	the inner induction hypothesis we have that @{term "(\<Delta>@[(X,P)]@\<Gamma>) \<turnstile> T\<^isub>1 <: S\<^isub>1"} and 
   926 	@{term "((Y,T\<^isub>1)#\<Delta>@[(X,P)]@\<Gamma>) \<turnstile> S\<^isub>2 <: T\<^isub>2"}. Since @{term P} is a subtype of @{term Q}
   927 	we can infer that @{term Y} is fresh for @{term P} and thus also fresh for 
   928 	@{term "\<Delta>@[(X,P)]@\<Gamma>"}. We can then conclude by applying rule @{text "S_Forall"}.
   929 	\end{minipage}*}
   930       hence IH_inner\<^isub>1: "(\<Delta>@[(X,P)]@\<Gamma>) \<turnstile> T\<^isub>1 <: S\<^isub>1" 
   931 	and IH_inner\<^isub>2: "((Y,T\<^isub>1)#\<Delta>@[(X,P)]@\<Gamma>) \<turnstile> S\<^isub>2 <: T\<^isub>2" 
   932 	and lh_drv_prm: "Y\<sharp>(\<Delta>@[(X,Q)]@\<Gamma>)" by force+
   933       have rh_drv: "\<Gamma> \<turnstile> P <: Q" by fact
   934       hence "Y\<sharp>P" using lh_drv_prm by (simp only: fresh_list_append subtype_implies_fresh)
   935       hence "Y\<sharp>(\<Delta>@[(X,P)]@\<Gamma>)" using lh_drv_prm 
   936 	by (simp add: fresh_list_append fresh_list_cons fresh_prod)
   937       with IH_inner\<^isub>1 IH_inner\<^isub>2 
   938       show "(\<Delta>@[(X,P)]@\<Gamma>) \<turnstile> \<forall>[Y<:S\<^isub>1].S\<^isub>2 <: \<forall>[Y<:T\<^isub>1].T\<^isub>2" by (simp add: subtype_of.S_Forall)
   939     qed
   940   } 
   941 qed
   942 
   943 end