src/HOL/Nominal/Examples/Fsub.thy
changeset 18424 a37f06555c07
parent 18417 149cc4126997
child 18577 a636846a02c7
     1.1 --- a/src/HOL/Nominal/Examples/Fsub.thy	Fri Dec 16 16:59:32 2005 +0100
     1.2 +++ b/src/HOL/Nominal/Examples/Fsub.thy	Fri Dec 16 18:20:03 2005 +0100
     1.3 @@ -4,35 +4,47 @@
     1.4  imports "../nominal" 
     1.5  begin
     1.6  
     1.7 -text {* Authors: Christian Urban
     1.8 -                 Benjamin Pierce
     1.9 -                 Steve Zdancewic
    1.10 -                 Stephanie Weihrich
    1.11 -                 Dimitrios Vytiniotis
    1.12 +text {* Authors: Christian Urban,
    1.13 +                 Benjamin Pierce,
    1.14 +                 Steve Zdancewic.
    1.15 +                 Stephanie Weihrich and
    1.16 +                 Dimitrios Vytiniotis;
    1.17  
    1.18 -                 with help from Stefan Berghofer, Markus Wenzel
    1.19 +                 with help from Stefan Berghofer and  Markus Wenzel.
    1.20        *}
    1.21  
    1.22  
    1.23 +section {* Atom Types, Types and Terms *}
    1.24 +
    1.25  atom_decl tyvrs vrs
    1.26  
    1.27 -section {* Types *}
    1.28 +nominal_datatype ty = 
    1.29 +    TVar  "tyvrs"
    1.30 +  | Top
    1.31 +  | Arrow  "ty" "ty"          ("_ \<rightarrow> _" [900,900] 900)
    1.32 +  | TAll  "\<guillemotleft>tyvrs\<guillemotright>ty" "ty" 
    1.33  
    1.34 -nominal_datatype ty = TyVar "tyvrs"
    1.35 -                    | Top
    1.36 -                    | Arrow  "ty" "ty"          ("_ \<rightarrow> _" [900,900] 900)
    1.37 -                    | TAll  "\<guillemotleft>tyvrs\<guillemotright>ty" "ty" 
    1.38 +nominal_datatype trm = 
    1.39 +    Var   "vrs"
    1.40 +  | Lam   "\<guillemotleft>vrs\<guillemotright>trm" "ty"
    1.41 +  | TAbs  "\<guillemotleft>tyvrs\<guillemotright>trm" "ty"
    1.42 +  | App   "trm" "trm"
    1.43 +  | TApp  "trm" "ty"
    1.44  
    1.45  syntax
    1.46    TAll_syn  :: "tyvrs \<Rightarrow> ty \<Rightarrow> ty \<Rightarrow> ty" ("\<forall> [_<:_]._" [900,900,900] 900)
    1.47 +  Lam_syn   :: "vrs \<Rightarrow> ty \<Rightarrow> trm \<Rightarrow> trm"   ("Lam [_:_]._" [100,100,100] 100)
    1.48 +  TAbs_syn  :: "tyvrs \<Rightarrow> ty \<Rightarrow> trm \<Rightarrow> trm" ("TAbs [_<:_]._" [100,100,100] 100)
    1.49 +
    1.50  translations 
    1.51 -  "(\<forall>[a<:ty1].ty2)" \<rightleftharpoons> "TAll a ty2 ty1"
    1.52 +  "\<forall>[a<:ty1].ty2" \<rightleftharpoons> "TAll a ty2 ty1"
    1.53 +  "Lam  [a:tys].t" \<rightleftharpoons> "trm.Lam a t tys"
    1.54 +  "TAbs [a<:tys].t" \<rightleftharpoons> "trm.TAbs a t tys"
    1.55  
    1.56 -section {* typing contexts and their domains *}
    1.57 +subsection {* Typing contexts and Their Domains *}
    1.58  
    1.59  types ty_context = "(tyvrs\<times>ty) list"
    1.60  
    1.61 -text {* domain of a context --- (the name "dom" is already used elsewhere) *}
    1.62  consts
    1.63    "domain" :: "ty_context \<Rightarrow> tyvrs set"
    1.64  primrec
    1.65 @@ -49,26 +61,28 @@
    1.66    shows "finite (domain \<Gamma>)"
    1.67    by (induct \<Gamma>, auto)
    1.68  
    1.69 -lemma domain_inclusion[rule_format]:
    1.70 -  shows "(X,T)\<in>set \<Gamma> \<longrightarrow> X\<in>(domain \<Gamma>)"
    1.71 -  by (induct \<Gamma>, auto)
    1.72 +lemma domain_inclusion:
    1.73 +  assumes a: "(X,T)\<in>set \<Gamma>" 
    1.74 +  shows "X\<in>(domain \<Gamma>)"
    1.75 +  using a by (induct \<Gamma>, auto)
    1.76  
    1.77 -lemma domain_existence[rule_format]:
    1.78 -  shows "X\<in>(domain \<Gamma>) \<longrightarrow> (\<exists>T.(X,T)\<in>set \<Gamma>)"
    1.79 -  by (induct \<Gamma>, auto)
    1.80 +lemma domain_existence:
    1.81 +  assumes a: "X\<in>(domain \<Gamma>)" 
    1.82 +  shows "\<exists>T.(X,T)\<in>set \<Gamma>"
    1.83 +  using a by (induct \<Gamma>, auto)
    1.84  
    1.85  lemma domain_append:
    1.86    shows "domain (\<Gamma>@\<Delta>) = ((domain \<Gamma>) \<union> (domain \<Delta>))"
    1.87    by (induct \<Gamma>, auto)
    1.88  
    1.89 -section {* Two functions over types *}
    1.90 +section {* Size Functions and Capture Avoiding Substitutiuon for Types *}
    1.91  
    1.92  text {* they cannot yet be defined conveniently unless we have a recursion combinator *}
    1.93  
    1.94  consts size_ty :: "ty \<Rightarrow> nat"
    1.95  
    1.96  lemma size_ty[simp]:
    1.97 -  shows "size_ty (TyVar X) = 1"
    1.98 +  shows "size_ty (TVar X) = 1"
    1.99    and   "size_ty (Top) = 1"
   1.100    and   "\<lbrakk>size_ty t1 = m ; size_ty t2 = n\<rbrakk> \<Longrightarrow> size_ty (t1 \<rightarrow> t2) = m + n + 1"
   1.101    and   "\<lbrakk>size_ty t1 = m ; size_ty t2 = n\<rbrakk> \<Longrightarrow> size_ty (\<forall> [a<:t1].t2) = m + n + 1"
   1.102 @@ -77,7 +91,7 @@
   1.103  consts subst_ty :: "ty \<Rightarrow> tyvrs \<Rightarrow> ty \<Rightarrow> ty"
   1.104  
   1.105  lemma subst_ty[simp]:
   1.106 -  shows "subst_ty (TyVar X) Y T = (if X=Y then T else (TyVar X))"
   1.107 +  shows "subst_ty (TVar X) Y T = (if X=Y then T else (TVar X))"
   1.108    and   "subst_ty Top Y T = Top"
   1.109    and   "subst_ty (T1 \<rightarrow> T2) Y T = (subst_ty T1 Y T) \<rightarrow> (subst_ty T2 Y T)"
   1.110    and   "X\<sharp>(Y,T) \<Longrightarrow> subst_ty (\<forall>[X<:T1].T2) Y T = (\<forall>[X<:(subst_ty T1 Y T)].(subst_ty T2 Y T))"
   1.111 @@ -90,7 +104,7 @@
   1.112  "subst_ctxt [] Y T = []"
   1.113  "subst_ctxt (XT#Xs) Y T = (fst XT, subst_ty (snd XT) Y T)#(subst_ctxt Xs Y T)"
   1.114  
   1.115 -text {* valid contexts *}
   1.116 +subsection {* valid contexts *}
   1.117  
   1.118  constdefs
   1.119    "closed_in" :: "ty \<Rightarrow> ty_context \<Rightarrow> bool" ("_ closed'_in _" [100,100] 100)
   1.120 @@ -108,7 +122,7 @@
   1.121    shows "(pi\<bullet>S) closed_in (pi\<bullet>\<Gamma>)"
   1.122    using a
   1.123  proof (unfold "closed_in_def")
   1.124 -  assume "supp S \<subseteq> (domain \<Gamma>)"
   1.125 +  assume "supp S \<subseteq> (domain \<Gamma>)" 
   1.126    hence "pi\<bullet>(supp S) \<subseteq> pi\<bullet>(domain \<Gamma>)"
   1.127      by (simp add: pt_subseteq_eqvt[OF pt_tyvrs_inst, OF at_tyvrs_inst])
   1.128    thus "(supp (pi\<bullet>S)) \<subseteq> (domain (pi\<bullet>\<Gamma>))"
   1.129 @@ -142,7 +156,7 @@
   1.130    proof (simp, rule valid_rel.v2)
   1.131      show "\<turnstile> (pi \<bullet> \<Gamma>) ok" using a1 by simp
   1.132    next 
   1.133 -    show "(pi\<bullet>X)\<sharp>(pi\<bullet>\<Gamma>)" using a2 by (simp add: pt_fresh_bij[OF pt_tyvrs_inst, OF at_tyvrs_inst])
   1.134 +    show "(pi\<bullet>X)\<sharp>(pi\<bullet>\<Gamma>)" using a2 by (simp add: fresh_eqvt)
   1.135    next
   1.136      show "(pi\<bullet>T) closed_in (pi\<bullet>\<Gamma>)" using a3 by (rule closed_in_eqvt)
   1.137    qed
   1.138 @@ -153,24 +167,20 @@
   1.139    shows "\<turnstile> \<Gamma> ok \<and> X\<sharp>\<Gamma> \<and> T closed_in \<Gamma>"
   1.140  using a by (cases, auto)
   1.141  
   1.142 -lemma validE_append[rule_format]:
   1.143 -  shows "\<turnstile> (\<Delta>@\<Gamma>) ok \<longrightarrow> \<turnstile> \<Gamma> ok"
   1.144 -  by (induct \<Delta>, auto dest: validE)
   1.145 +lemma validE_append:
   1.146 +  assumes a: "\<turnstile> (\<Delta>@\<Gamma>) ok" 
   1.147 +  shows "\<turnstile> \<Gamma> ok"
   1.148 +  using a by (induct \<Delta>, auto dest: validE)
   1.149  
   1.150 -lemma domain_fresh[rule_format]:
   1.151 +lemma domain_fresh:
   1.152    fixes X::"tyvrs"
   1.153 -  shows "\<turnstile> \<Gamma> ok \<longrightarrow> (X\<sharp>(domain \<Gamma>) = X\<sharp>\<Gamma>)"
   1.154 +  assumes a: "\<turnstile> \<Gamma> ok" 
   1.155 +  shows "X\<sharp>(domain \<Gamma>) = X\<sharp>\<Gamma>"
   1.156 +using a
   1.157  apply(induct \<Gamma>)
   1.158 -apply(simp add: fresh_list_nil fresh_set_empty)
   1.159 -apply(simp add: fresh_list_cons fresh_prod 
   1.160 -   fresh_fin_insert[OF pt_tyvrs_inst, OF at_tyvrs_inst, OF fs_tyvrs_inst, OF finite_domain])
   1.161 -apply(rule impI)
   1.162 -apply(clarify)
   1.163 -apply(simp add: fresh_prod)
   1.164 -apply(drule validE)
   1.165 -apply(simp)
   1.166 -apply(simp add: closed_in_def2 fresh_def)
   1.167 -apply(force)
   1.168 +apply(auto simp add: fresh_list_nil fresh_list_cons fresh_set_empty fresh_prod fresh_atm
   1.169 +  fresh_fin_insert[OF pt_tyvrs_inst, OF at_tyvrs_inst, OF fs_tyvrs_inst, OF finite_domain])
   1.170 +apply(force simp add: closed_in_def2 fresh_def)
   1.171  done
   1.172  
   1.173  lemma closed_in_fresh:
   1.174 @@ -186,8 +196,11 @@
   1.175  apply(force)
   1.176  done
   1.177  
   1.178 -lemma replace_type[rule_format]:
   1.179 -  shows "\<turnstile> (\<Delta>@(X,T)#\<Gamma>) ok \<longrightarrow> S closed_in \<Gamma> \<longrightarrow> \<turnstile> (\<Delta>@(X,S)#\<Gamma>) ok"
   1.180 +lemma replace_type:
   1.181 +  assumes a: "\<turnstile> (\<Delta>@(X,T)#\<Gamma>) ok"
   1.182 +  and     b: "S closed_in \<Gamma>"
   1.183 +  shows "\<turnstile> (\<Delta>@(X,S)#\<Gamma>) ok"
   1.184 +using a b 
   1.185  apply(induct \<Delta>)
   1.186  apply(auto dest!: validE intro!: v2 simp add: fresh_list_append fresh_list_cons fresh_prod)
   1.187  apply(drule validE_append)
   1.188 @@ -199,9 +212,11 @@
   1.189  apply(simp add: domain_append)
   1.190  done
   1.191  
   1.192 -lemma fresh_implies_not_member[rule_format]:
   1.193 +lemma fresh_implies_not_member:
   1.194    fixes \<Gamma>::"ty_context"
   1.195 -  shows "X\<sharp>\<Gamma> \<longrightarrow> \<not>(\<exists>T.(X,T)\<in>(set \<Gamma>))"
   1.196 +  assumes a: "X\<sharp>\<Gamma>" 
   1.197 +  shows "\<not>(\<exists>T.(X,T)\<in>(set \<Gamma>))"
   1.198 +  using a
   1.199    apply (induct \<Gamma>)
   1.200    apply (auto dest: validE simp add: fresh_list_cons fresh_prod fresh_atm)
   1.201    done
   1.202 @@ -227,8 +242,8 @@
   1.203  inductive subtype_of_rel
   1.204  intros
   1.205  S_Top[intro]:   "\<lbrakk>\<turnstile> \<Gamma> ok; S closed_in \<Gamma>\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> S <: Top"
   1.206 -S_Var[intro]:   "\<lbrakk>\<turnstile> \<Gamma> ok; (X,S) \<in> (set \<Gamma>); \<Gamma> \<turnstile> S <: T\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> (TyVar X) <: T"
   1.207 -S_Refl[intro]:  "\<lbrakk>\<turnstile> \<Gamma> ok; X \<in> (domain \<Gamma>)\<rbrakk>\<Longrightarrow> \<Gamma> \<turnstile> TyVar X <: TyVar X"
   1.208 +S_Var[intro]:   "\<lbrakk>\<turnstile> \<Gamma> ok; (X,S) \<in> set \<Gamma>; \<Gamma> \<turnstile> S <: T\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> (TVar X) <: T"
   1.209 +S_Refl[intro]:  "\<lbrakk>\<turnstile> \<Gamma> ok; X \<in> domain \<Gamma>\<rbrakk>\<Longrightarrow> \<Gamma> \<turnstile> TVar X <: TVar X"
   1.210  S_Arrow[intro]: "\<lbrakk>\<Gamma> \<turnstile> T1 <: S1; \<Gamma> \<turnstile> S2 <: T2\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> (S1 \<rightarrow> S2) <: (T1 \<rightarrow> T2)" 
   1.211  S_All[intro]:   "\<lbrakk>\<Gamma> \<turnstile> T1 <: S1; X\<sharp>\<Gamma>; ((X,T1)#\<Gamma>) \<turnstile> S2 <: T2\<rbrakk> 
   1.212                    \<Longrightarrow> \<Gamma> \<turnstile> \<forall> [X<:S1].S2 <: \<forall> [X<:T1].T2"  
   1.213 @@ -239,37 +254,21 @@
   1.214  using a
   1.215  proof (induct)
   1.216    case (S_Top S \<Gamma>)
   1.217 -  have "Top closed_in \<Gamma>" 
   1.218 -    by (simp add: closed_in_def ty.supp)
   1.219 +  have "Top closed_in \<Gamma>" by (simp add: closed_in_def ty.supp)
   1.220    moreover
   1.221    have "S closed_in \<Gamma>" by fact
   1.222    ultimately show "S closed_in \<Gamma> \<and> Top closed_in \<Gamma>" by simp
   1.223  next
   1.224    case (S_Var S T X \<Gamma>)
   1.225    have "(X,S)\<in>set \<Gamma>" by fact
   1.226 -  hence "X\<in>(domain \<Gamma>)" by (rule domain_inclusion)
   1.227 -  hence "(TyVar X) closed_in \<Gamma>" by (simp add: closed_in_def ty.supp supp_atm)
   1.228 +  hence "X \<in> domain \<Gamma>" by (rule domain_inclusion)
   1.229 +  hence "(TVar X) closed_in \<Gamma>" by (simp add: closed_in_def ty.supp supp_atm)
   1.230    moreover
   1.231    have "S closed_in \<Gamma> \<and> T closed_in \<Gamma>" by fact
   1.232    hence "T closed_in \<Gamma>" by force
   1.233 -  ultimately show "(TyVar X) closed_in \<Gamma> \<and> T closed_in \<Gamma>" by simp
   1.234 -next
   1.235 -  case S_Refl thus ?case 
   1.236 -    by (simp add: closed_in_def ty.supp supp_atm) 
   1.237 -next
   1.238 -  case S_Arrow thus ?case by (force simp add: closed_in_def ty.supp)
   1.239 -next 
   1.240 -  case S_All thus ?case by (auto simp add: closed_in_def ty.supp abs_supp)
   1.241 -qed
   1.242 +  ultimately show "(TVar X) closed_in \<Gamma> \<and> T closed_in \<Gamma>" by simp
   1.243 +qed (auto simp add: closed_in_def ty.supp supp_atm abs_supp)
   1.244  
   1.245 -text {* a completely automated proof *}
   1.246 -lemma subtype_implies_closed:
   1.247 -  assumes a: "\<Gamma> \<turnstile> S <: T"
   1.248 -  shows "S closed_in \<Gamma> \<and> T closed_in \<Gamma>"
   1.249 -using a
   1.250 -apply (induct) 
   1.251 -apply (auto simp add: closed_in_def ty.supp abs_supp domain_inclusion supp_atm)
   1.252 -done
   1.253  
   1.254  lemma subtype_implies_ok:
   1.255    fixes X::"tyvrs"
   1.256 @@ -281,14 +280,15 @@
   1.257    fixes X::"tyvrs"
   1.258    assumes a1: "\<Gamma> \<turnstile> S <: T"
   1.259    and     a2: "X\<sharp>\<Gamma>"
   1.260 -  shows "X\<sharp>(S,T)"  
   1.261 +  shows "X\<sharp>S \<and> X\<sharp>T"  
   1.262  proof -
   1.263    from a1 have "\<turnstile> \<Gamma> ok" by (rule subtype_implies_ok)
   1.264 -  with a2 have b0: "X\<sharp>domain(\<Gamma>)" by (simp add: domain_fresh)
   1.265 +  with a2 have "X\<sharp>domain(\<Gamma>)" by (simp add: domain_fresh)
   1.266 +  moreover
   1.267    from a1 have "S closed_in \<Gamma> \<and> T closed_in \<Gamma>" by (rule subtype_implies_closed)
   1.268 -  hence b1: "supp S \<subseteq> ((supp (domain \<Gamma>))::tyvrs set)" 
   1.269 -    and b2: "supp T \<subseteq> ((supp (domain \<Gamma>))::tyvrs set)" by (simp_all add: closed_in_def2)
   1.270 -  thus "X\<sharp>(S,T)" using b0 b1 b2 by (force simp add: supp_prod fresh_def)
   1.271 +  hence "supp S \<subseteq> ((supp (domain \<Gamma>))::tyvrs set)" 
   1.272 +    and "supp T \<subseteq> ((supp (domain \<Gamma>))::tyvrs set)" by (simp_all add: closed_in_def2)
   1.273 +  ultimately show "X\<sharp>S \<and> X\<sharp>T" by (force simp add: supp_prod fresh_def)
   1.274  qed
   1.275  
   1.276  lemma silly_eqvt1:
   1.277 @@ -322,10 +322,10 @@
   1.278  lemma subtype_of_rel_induct[consumes 1, case_names S_Top S_Var S_Refl S_Arrow S_All]:
   1.279    fixes  P :: "'a::fs_tyvrs\<Rightarrow>ty_context \<Rightarrow> ty \<Rightarrow> ty \<Rightarrow>bool"
   1.280    assumes a: "\<Gamma> \<turnstile> S <: T"
   1.281 -  and a1:    "\<And>\<Gamma> S x. (\<turnstile> \<Gamma> ok) \<Longrightarrow> (S closed_in \<Gamma>) \<Longrightarrow> P x \<Gamma> S Top"
   1.282 -  and a2:    "\<And>\<Gamma> X S T x. (\<turnstile> \<Gamma> ok) \<Longrightarrow> ((X,S)\<in>set \<Gamma>) \<Longrightarrow> (\<Gamma> \<turnstile> S <: T) \<Longrightarrow> (\<And>z. P z \<Gamma> S T)
   1.283 -              \<Longrightarrow> P x \<Gamma> (TyVar X) T"
   1.284 -  and a3:    "\<And>\<Gamma> X x. (\<turnstile> \<Gamma> ok) \<Longrightarrow> X\<in>domain \<Gamma> \<Longrightarrow> P x \<Gamma> (TyVar X) (TyVar X)"  
   1.285 +  and a1:    "\<And>\<Gamma> S x. \<turnstile> \<Gamma> ok \<Longrightarrow> S closed_in \<Gamma> \<Longrightarrow> P x \<Gamma> S Top"
   1.286 +  and a2:    "\<And>\<Gamma> X S T x. \<turnstile> \<Gamma> ok \<Longrightarrow> (X,S)\<in>set \<Gamma> \<Longrightarrow> \<Gamma> \<turnstile> S <: T \<Longrightarrow> (\<And>z. P z \<Gamma> S T)
   1.287 +              \<Longrightarrow> P x \<Gamma> (TVar X) T"
   1.288 +  and a3:    "\<And>\<Gamma> X x. \<turnstile> \<Gamma> ok \<Longrightarrow> X\<in>domain \<Gamma> \<Longrightarrow> P x \<Gamma> (TVar X) (TVar X)"  
   1.289    and a4:    "\<And>\<Gamma> S1 S2 T1 T2 x. \<Gamma> \<turnstile> T1 <: S1 \<Longrightarrow> (\<And>z. P z \<Gamma> T1 S1) \<Longrightarrow> \<Gamma> \<turnstile> S2 <: T2 \<Longrightarrow> 
   1.290                (\<And>z. P z \<Gamma> S2 T2) \<Longrightarrow> P x \<Gamma> (S1 \<rightarrow> S2) (T1 \<rightarrow> T2)"
   1.291    and a5:    "\<And>\<Gamma> X S1 S2 T1 T2 x. 
   1.292 @@ -335,13 +335,8 @@
   1.293  proof -
   1.294    from a have "\<And>(pi::tyvrs prm) (x::'a::fs_tyvrs). P x (pi\<bullet>\<Gamma>) (pi\<bullet>S) (pi\<bullet>T)"
   1.295    proof (induct)
   1.296 -    case (S_Top S \<Gamma>)
   1.297 -    have b1: "\<turnstile> \<Gamma> ok" by fact 
   1.298 -    have b2: "S closed_in \<Gamma>" by fact
   1.299 -    from b1 have "\<turnstile> (pi\<bullet>\<Gamma>) ok" by (rule valid_eqvt)
   1.300 -    moreover
   1.301 -    from b2 have "(pi\<bullet>S) closed_in (pi\<bullet>\<Gamma>)" by (rule closed_in_eqvt)
   1.302 -    ultimately show "P x (pi \<bullet> \<Gamma>) (pi \<bullet> S) (pi\<bullet>Top)" by (simp add: a1)
   1.303 +    case (S_Top S \<Gamma>) 
   1.304 +    thus "P x (pi\<bullet>\<Gamma>) (pi\<bullet>S) (pi\<bullet>Top)" by (force intro: valid_eqvt closed_in_eqvt a1)
   1.305    next
   1.306      case (S_Var S T X \<Gamma>)
   1.307      have b1: "\<turnstile> \<Gamma> ok" by fact 
   1.308 @@ -357,7 +352,7 @@
   1.309      moreover 
   1.310      from b4 have "\<And>x. P x (pi\<bullet>\<Gamma>) (pi\<bullet>S) (pi\<bullet>T)" by simp
   1.311      ultimately 
   1.312 -    show "P x (pi\<bullet>\<Gamma>) (pi\<bullet>(TyVar X)) (pi\<bullet>T)" by (simp add: a2)
   1.313 +    show "P x (pi\<bullet>\<Gamma>) (pi\<bullet>(TVar X)) (pi\<bullet>T)" by (simp add: a2)
   1.314    next
   1.315      case (S_Refl X \<Gamma>)
   1.316      have b1: "\<turnstile> \<Gamma> ok" by fact
   1.317 @@ -366,9 +361,9 @@
   1.318      moreover
   1.319      from b2 have "(pi\<bullet>X)\<in>pi\<bullet>domain \<Gamma>" by (rule pt_set_bij2[OF pt_tyvrs_inst, OF at_tyvrs_inst])
   1.320      hence "(pi\<bullet>X)\<in>domain (pi\<bullet>\<Gamma>)" by (simp add: domain_eqvt pt_list_set_pi[OF pt_tyvrs_inst])
   1.321 -    ultimately show "P x (pi\<bullet>\<Gamma>) (pi\<bullet>(TyVar X)) (pi\<bullet>(TyVar X))" by (simp add: a3)
   1.322 +    ultimately show "P x (pi\<bullet>\<Gamma>) (pi\<bullet>(TVar X)) (pi\<bullet>(TVar X))" by (simp add: a3)
   1.323    next
   1.324 -    case S_Arrow thus ?case by (simp, auto intro!: a4 subtype_eqvt)
   1.325 +    case S_Arrow thus ?case by (auto intro: a4 subtype_eqvt)
   1.326    next
   1.327      case (S_All S1 S2 T1 T2 X \<Gamma>)
   1.328      have b1: "\<Gamma> \<turnstile> T1 <: S1" by fact 
   1.329 @@ -376,7 +371,7 @@
   1.330      have b4: "((X,T1)#\<Gamma>) \<turnstile> S2 <: T2" by fact
   1.331      have b5: "\<And>(pi::tyvrs prm) x. P x (pi\<bullet>((X,T1)#\<Gamma>)) (pi\<bullet>S2) (pi\<bullet>T2)" by fact
   1.332      have b3': "X\<sharp>\<Gamma>" by fact
   1.333 -    have b3'': "X\<sharp>(T1,S1)" using b1 b3' by (rule subtype_implies_fresh)
   1.334 +    have b3'': "X\<sharp>T1" "X\<sharp>S1" using b1 b3' by (simp_all add: subtype_implies_fresh)
   1.335      have b3: "X\<sharp>(\<Gamma>,S1,T1)" using b3' b3'' by (simp add: fresh_prod)
   1.336      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)"
   1.337        by (rule at_exists_fresh[OF at_tyvrs_inst], simp add: fs_tyvrs1)
   1.338 @@ -423,27 +418,28 @@
   1.339    thus ?thesis by simp
   1.340  qed
   1.341  
   1.342 -section {* Two proofs for reflexivity of subtyping *}
   1.343 +subsection {* Reflexivity of Subtyping *}
   1.344  
   1.345  lemma subtype_reflexivity:
   1.346    assumes a: "\<turnstile> \<Gamma> ok"
   1.347 -  and     b: "T closed_in \<Gamma>"
   1.348 +  and b: "T closed_in \<Gamma>"
   1.349    shows "\<Gamma> \<turnstile> T <: T"
   1.350  using a b
   1.351  proof(nominal_induct T avoiding: \<Gamma> rule: ty.induct_unsafe)
   1.352 -  case (TAll X T1 T2)
   1.353 -  have i1: "\<And>\<Gamma>. \<turnstile> \<Gamma> ok \<Longrightarrow> T1 closed_in \<Gamma> \<Longrightarrow> \<Gamma> \<turnstile> T1 <: T1" by fact 
   1.354 -  have i2: "\<And>\<Gamma>. \<turnstile> \<Gamma> ok \<Longrightarrow> T2 closed_in \<Gamma> \<Longrightarrow> \<Gamma> \<turnstile> T2 <: T2" by fact
   1.355 -  have f: "X\<sharp>\<Gamma>" by fact
   1.356 -  have "(\<forall>[X<:T2].T1) closed_in \<Gamma>" by fact
   1.357 -  hence b1: "T2 closed_in \<Gamma>" and b2: "T1 closed_in ((X,T2)#\<Gamma>)" 
   1.358 -      by (auto simp add: closed_in_def ty.supp abs_supp)
   1.359 -  have c1: "\<turnstile> \<Gamma> ok" by fact  
   1.360 -  hence c2: "\<turnstile> ((X,T2)#\<Gamma>) ok" using b1 f by force
   1.361 -  have "\<Gamma> \<turnstile> T2 <: T2" using i2 b1 c1 by simp
   1.362 +  case (TAll X T\<^isub>1 T\<^isub>2)
   1.363 +  have ih_T\<^isub>1: "\<And>\<Gamma>. \<turnstile> \<Gamma> ok \<Longrightarrow> T\<^isub>1 closed_in \<Gamma> \<Longrightarrow> \<Gamma> \<turnstile> T\<^isub>1 <: T\<^isub>1" by fact 
   1.364 +  have ih_T\<^isub>2: "\<And>\<Gamma>. \<turnstile> \<Gamma> ok \<Longrightarrow> T\<^isub>2 closed_in \<Gamma> \<Longrightarrow> \<Gamma> \<turnstile> T\<^isub>2 <: T\<^isub>2" by fact
   1.365 +  have fresh_cond: "X\<sharp>\<Gamma>" by fact
   1.366 +  have "(\<forall>[X<:T\<^isub>2].T\<^isub>1) closed_in \<Gamma>" by fact
   1.367 +  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>)" 
   1.368 +    by (auto simp add: closed_in_def ty.supp abs_supp)
   1.369 +  have ok: "\<turnstile> \<Gamma> ok" by fact  
   1.370 +  hence ok': "\<turnstile> ((X,T\<^isub>2)#\<Gamma>) ok" using closed\<^isub>T\<^isub>2 fresh_cond by force
   1.371 +  have "\<Gamma> \<turnstile> T\<^isub>2 <: T\<^isub>2" using ih_T\<^isub>2 closed\<^isub>T\<^isub>2 ok by simp
   1.372    moreover
   1.373 -  have "((X,T2)#\<Gamma>) \<turnstile> T1 <: T1" using i1 b2 c2 by simp
   1.374 -  ultimately show "\<Gamma> \<turnstile> \<forall>[X<:T2].T1 <: \<forall>[X<:T2].T1" using f by force
   1.375 +  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
   1.376 +  ultimately show "\<Gamma> \<turnstile> \<forall>[X<:T\<^isub>2].T\<^isub>1 <: \<forall>[X<:T\<^isub>2].T\<^isub>1" using fresh_cond 
   1.377 +    by (simp add: subtype_of_rel.S_All)
   1.378  qed (auto simp add: closed_in_def ty.supp supp_atm)
   1.379  
   1.380  lemma subtype_reflexivity:
   1.381 @@ -453,24 +449,24 @@
   1.382  using a b
   1.383  apply(nominal_induct T avoiding: \<Gamma> rule: ty.induct_unsafe)
   1.384  apply(auto simp add: ty.supp abs_supp closed_in_def supp_atm)
   1.385 -(* too bad that this cannot be found automatically *)
   1.386 +--{* Too bad that this instantiation cannot be found automatically. *}
   1.387  apply(drule_tac x="(tyvrs, ty2)#\<Gamma>" in meta_spec)
   1.388  apply(force simp add: closed_in_def)
   1.389  done
   1.390  
   1.391 -text {* Inversion lemmas. . .  *}
   1.392 +text {* Inversion lemmas *}
   1.393  lemma S_TopE:
   1.394 - shows "\<Gamma> \<turnstile> Top <: T \<Longrightarrow> T = Top" 
   1.395 -apply(ind_cases "\<Gamma> \<turnstile> Top <: T", auto)
   1.396 -done
   1.397 +  assumes a: "\<Gamma> \<turnstile> Top <: T"
   1.398 +  shows "T = Top"
   1.399 +using a by (cases, auto) 
   1.400  
   1.401  lemma S_ArrowE_left:
   1.402    assumes a: "\<Gamma> \<turnstile> S1 \<rightarrow> S2 <: T" 
   1.403    shows "T = Top \<or> (\<exists>T1 T2. T = T1 \<rightarrow> T2 \<and> \<Gamma> \<turnstile> T1 <: S1 \<and> \<Gamma> \<turnstile> S2 <: T2)"
   1.404 -using  a by (cases, auto simp add: ty.inject)
   1.405 +using a by (cases, auto simp add: ty.inject)
   1.406  
   1.407  lemma S_AllE_left:
   1.408 -  shows "\<lbrakk>\<Gamma> \<turnstile> \<forall>[X<:S1].S2 <: T; X\<sharp>(\<Gamma>,S1)\<rbrakk>
   1.409 +  shows "\<lbrakk>\<Gamma> \<turnstile> \<forall>[X<:S1].S2 <: T; X\<sharp>\<Gamma>; X\<sharp>S1\<rbrakk>
   1.410           \<Longrightarrow> T = Top \<or> (\<exists>T1 T2. T = \<forall>[X<:T1].T2 \<and> \<Gamma> \<turnstile> T1 <: S1 \<and> ((X,T1)#\<Gamma>) \<turnstile> S2 <: T2)"
   1.411    apply(frule subtype_implies_ok)
   1.412    apply(ind_cases "\<Gamma> \<turnstile> \<forall>[X<:S1].S2 <: T")
   1.413 @@ -486,10 +482,9 @@
   1.414    (* 1st conjunct *)
   1.415    apply(rule conjI)
   1.416    apply(simp add: pt_fresh_left[OF pt_tyvrs_inst, OF at_tyvrs_inst] calc_atm)
   1.417 -  apply(simp add: fresh_prod)
   1.418    apply(drule_tac \<Gamma>="((Xa,T1)#\<Gamma>)" in  subtype_implies_closed)+
   1.419    apply(simp add: closed_in_def)
   1.420 -  apply(auto simp add: domain_fresh[of "\<Gamma>" "X", symmetric])
   1.421 +  apply(simp add: domain_fresh[of "\<Gamma>" "X", symmetric])
   1.422    apply(simp add: fresh_def)
   1.423    apply(subgoal_tac "X \<notin> (insert Xa (domain \<Gamma>))")(*A*)
   1.424    apply(force)
   1.425 @@ -497,7 +492,7 @@
   1.426    apply(simp add: at_fin_set_supp[OF at_tyvrs_inst, OF finite_domain])
   1.427    (* 2nd conjunct *)
   1.428    apply(frule_tac X="X" in subtype_implies_fresh)
   1.429 -  apply(simp add: fresh_prod)
   1.430 +  apply(assumption)
   1.431    apply(drule_tac X="Xa" in subtype_implies_fresh)
   1.432    apply(assumption)
   1.433    apply(simp add: fresh_prod)
   1.434 @@ -506,19 +501,22 @@
   1.435    apply(simp add: pt_fresh_fresh[OF pt_tyvrs_inst, OF at_tyvrs_inst])
   1.436    done
   1.437  
   1.438 -section {* Type substitution *}
   1.439 +section {* Type Substitution *}
   1.440  
   1.441 -lemma subst_ty_fresh[rule_format]:
   1.442 -  fixes P :: "ty"
   1.443 -  and   X :: "tyvrs"
   1.444 -  shows "X\<sharp>(T,P) \<longrightarrow> X\<sharp>(subst_ty T Y P)"
   1.445 +lemma subst_ty_fresh:
   1.446 +  fixes X :: "tyvrs"
   1.447 +  assumes a: "X\<sharp>(T,P)"
   1.448 +  shows "X\<sharp>(subst_ty T Y P)"
   1.449 +  using a
   1.450    apply (nominal_induct T avoiding : T Y P rule: ty.induct_unsafe)
   1.451    apply (auto simp add: fresh_prod abs_fresh)
   1.452    done
   1.453  
   1.454 -lemma subst_ctxt_fresh[rule_format]:
   1.455 +lemma subst_ctxt_fresh:
   1.456    fixes X::"tyvrs"
   1.457 -  shows "X\<sharp>(\<Gamma>,P) \<longrightarrow> X\<sharp>(subst_ctxt \<Gamma> Y P)"
   1.458 +  assumes a: "X\<sharp>(\<Gamma>,P)"
   1.459 +  shows "X\<sharp>(subst_ctxt \<Gamma> Y P)"
   1.460 +  using a
   1.461    apply (induct \<Gamma>)
   1.462    apply (auto intro: subst_ty_fresh simp add: fresh_prod fresh_list_cons)
   1.463    done
   1.464 @@ -596,10 +594,16 @@
   1.465    using a1 a2
   1.466    by (auto dest: extends_domain simp add: closed_in_def)
   1.467  
   1.468 +lemma extends_memb:
   1.469 +  assumes a: "\<Delta> extends \<Gamma>"
   1.470 +  and b: "(X,T) \<in> set \<Gamma>"
   1.471 +  shows "(X,T) \<in> set \<Delta>"
   1.472 +  using a b by (simp add: extends_def)
   1.473 +
   1.474  lemma weakening:
   1.475    assumes a: "\<Gamma> \<turnstile> S <: T"
   1.476 -  and     b: "\<turnstile> \<Delta> ok"
   1.477 -  and     c: "\<Delta> extends \<Gamma>"
   1.478 +  and b: "\<turnstile> \<Delta> ok"
   1.479 +  and c: "\<Delta> extends \<Gamma>"
   1.480    shows "\<Delta> \<turnstile> S <: T"
   1.481    using a b c 
   1.482  proof (nominal_induct \<Gamma> S T avoiding: \<Delta> rule: subtype_of_rel_induct)
   1.483 @@ -608,7 +612,7 @@
   1.484    have "\<turnstile> \<Delta> ok" by fact
   1.485    moreover
   1.486    have "\<Delta> extends \<Gamma>" by fact
   1.487 -  hence "S closed_in \<Delta>" using lh_drv_prem by (rule_tac extends_closed)
   1.488 +  hence "S closed_in \<Delta>" using lh_drv_prem by (simp only: extends_closed)
   1.489    ultimately show "\<Delta> \<turnstile> S <: Top" by force
   1.490  next 
   1.491    case (S_Var \<Gamma> X S T)
   1.492 @@ -616,10 +620,10 @@
   1.493    have ih: "\<And>\<Delta>. \<turnstile> \<Delta> ok \<Longrightarrow> \<Delta> extends \<Gamma> \<Longrightarrow> \<Delta> \<turnstile> S <: T" by fact
   1.494    have ok: "\<turnstile> \<Delta> ok" by fact
   1.495    have extends: "\<Delta> extends \<Gamma>" by fact
   1.496 -  have "(X,S) \<in> set \<Delta>" using lh_drv_prem extends by (simp add: extends_def)
   1.497 +  have "(X,S) \<in> set \<Delta>" using lh_drv_prem extends by (simp only: extends_memb)
   1.498    moreover
   1.499    have "\<Delta> \<turnstile> S <: T" using ok extends ih by simp
   1.500 -  ultimately show "\<Delta> \<turnstile> TyVar X <: T" using ok by force
   1.501 +  ultimately show "\<Delta> \<turnstile> TVar X <: T" using ok by force
   1.502  next
   1.503    case (S_Refl \<Gamma> X)
   1.504    have lh_drv_prem: "X \<in> domain \<Gamma>" by fact
   1.505 @@ -627,90 +631,84 @@
   1.506    moreover
   1.507    have "\<Delta> extends \<Gamma>" by fact
   1.508    hence "X \<in> domain \<Delta>" using lh_drv_prem by (force dest: extends_domain)
   1.509 -  ultimately show "\<Delta> \<turnstile> TyVar X <: TyVar X" by force
   1.510 +  ultimately show "\<Delta> \<turnstile> TVar X <: TVar X" by force
   1.511  next 
   1.512 -  case S_Arrow thus ?case by force
   1.513 +  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
   1.514  next
   1.515 -  case (S_All \<Gamma> X S1 S2 T1 T2)
   1.516 -  have fresh: "X\<sharp>\<Delta>" by fact
   1.517 -  have ih1: "\<And>\<Delta>. \<turnstile> \<Delta> ok \<Longrightarrow> \<Delta> extends \<Gamma> \<Longrightarrow> \<Delta> \<turnstile> T1 <: S1" by fact
   1.518 -  have ih2: "\<And>\<Delta>. \<turnstile> \<Delta> ok \<Longrightarrow> \<Delta> extends ((X,T1)#\<Gamma>) \<Longrightarrow> \<Delta> \<turnstile> S2 <: T2" by fact
   1.519 -  have lh_drv_prem: "\<Gamma> \<turnstile> T1 <: S1" by fact
   1.520 -  hence b5: "T1 closed_in \<Gamma>" by (simp add: subtype_implies_closed) 
   1.521 +  case (S_All \<Gamma> X S\<^isub>1 S\<^isub>2 T\<^isub>1 T\<^isub>2)
   1.522 +  have fresh_cond: "X\<sharp>\<Delta>" by fact
   1.523 +  have ih\<^isub>1: "\<And>\<Delta>. \<turnstile> \<Delta> ok \<Longrightarrow> \<Delta> extends \<Gamma> \<Longrightarrow> \<Delta> \<turnstile> T\<^isub>1 <: S\<^isub>1" by fact
   1.524 +  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
   1.525 +  have lh_drv_prem: "\<Gamma> \<turnstile> T\<^isub>1 <: S\<^isub>1" by fact
   1.526 +  hence closed\<^isub>T\<^isub>1: "T\<^isub>1 closed_in \<Gamma>" by (simp add: subtype_implies_closed) 
   1.527    have ok: "\<turnstile> \<Delta> ok" by fact
   1.528 -  have extends: "\<Delta> extends \<Gamma>" by fact
   1.529 -  have "T1 closed_in \<Delta>" using extends b5 by (simp only: extends_closed)
   1.530 -  hence "\<turnstile> ((X,T1)#\<Delta>) ok" using fresh ok by force   
   1.531 +  have ext: "\<Delta> extends \<Gamma>" by fact
   1.532 +  have "T\<^isub>1 closed_in \<Delta>" using ext closed\<^isub>T\<^isub>1 by (simp only: extends_closed)
   1.533 +  hence "\<turnstile> ((X,T\<^isub>1)#\<Delta>) ok" using fresh_cond ok by force   
   1.534    moreover 
   1.535 -  have "((X,T1)#\<Delta>) extends ((X,T1)#\<Gamma>)" using extends by (force simp add: extends_def)
   1.536 -  ultimately have "((X,T1)#\<Delta>) \<turnstile> S2 <: T2" using ih2 by simp
   1.537 +  have "((X,T\<^isub>1)#\<Delta>) extends ((X,T\<^isub>1)#\<Gamma>)" using ext by (force simp add: extends_def)
   1.538 +  ultimately have "((X,T\<^isub>1)#\<Delta>) \<turnstile> S\<^isub>2 <: T\<^isub>2" using ih\<^isub>2 by simp
   1.539    moreover
   1.540 -  have "\<Delta> \<turnstile> T1 <: S1" using ok extends ih1 by simp 
   1.541 -  ultimately show "\<Delta> \<turnstile> \<forall> [X<:S1].S2 <: \<forall> [X<:T1].T2" using ok by (force intro: S_All) 
   1.542 +  have "\<Delta> \<turnstile> T\<^isub>1 <: S\<^isub>1" using ok ext ih\<^isub>1 by simp 
   1.543 +  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_All)
   1.544  qed
   1.545  
   1.546 -text {* more automated proof *}
   1.547 +text {* In fact all "non-binding" cases can be solved automatically: *}
   1.548  
   1.549  lemma weakening:
   1.550    assumes a: "\<Gamma> \<turnstile> S <: T"
   1.551 -  and     b: "\<turnstile> \<Delta> ok"
   1.552 -  and     c: "\<Delta> extends \<Gamma>"
   1.553 +  and b: "\<turnstile> \<Delta> ok"
   1.554 +  and c: "\<Delta> extends \<Gamma>"
   1.555    shows "\<Delta> \<turnstile> S <: T"
   1.556    using a b c 
   1.557  proof (nominal_induct \<Gamma> S T avoiding: \<Delta> rule: subtype_of_rel_induct)
   1.558 -  case (S_Top \<Gamma> S) thus ?case by (force intro: extends_closed)
   1.559 -next 
   1.560 -  case (S_Var \<Gamma> X S T) thus ?case by (force simp add: extends_def)
   1.561 -next
   1.562 -  case (S_Refl \<Gamma> X) thus ?case by (force dest: extends_domain)
   1.563 -next 
   1.564 -  case S_Arrow thus ?case by force
   1.565 -next
   1.566 -  case (S_All \<Gamma> X S1 S2 T1 T2)
   1.567 -  have fresh: "X\<sharp>\<Delta>" by fact
   1.568 -  have ih1: "\<And>\<Delta>. \<turnstile> \<Delta> ok \<Longrightarrow> \<Delta> extends \<Gamma> \<Longrightarrow> \<Delta> \<turnstile> T1 <: S1" by fact
   1.569 -  have ih2: "\<And>\<Delta>. \<turnstile> \<Delta> ok \<Longrightarrow> \<Delta> extends ((X,T1)#\<Gamma>) \<Longrightarrow> \<Delta> \<turnstile> S2 <: T2" by fact
   1.570 -  have lh_drv_prem: "\<Gamma> \<turnstile> T1 <: S1" by fact
   1.571 -  hence b5: "T1 closed_in \<Gamma>" by (simp add: subtype_implies_closed) 
   1.572 +  case (S_All \<Gamma> X S\<^isub>1 S\<^isub>2 T\<^isub>1 T\<^isub>2)
   1.573 +  have fresh_cond: "X\<sharp>\<Delta>" by fact
   1.574 +  have ih\<^isub>1: "\<And>\<Delta>. \<turnstile> \<Delta> ok \<Longrightarrow> \<Delta> extends \<Gamma> \<Longrightarrow> \<Delta> \<turnstile> T\<^isub>1 <: S\<^isub>1" by fact
   1.575 +  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
   1.576 +  have lh_drv_prem: "\<Gamma> \<turnstile> T\<^isub>1 <: S\<^isub>1" by fact
   1.577 +  hence closed\<^isub>T\<^isub>1: "T\<^isub>1 closed_in \<Gamma>" by (simp add: subtype_implies_closed) 
   1.578    have ok: "\<turnstile> \<Delta> ok" by fact
   1.579 -  have extends: "\<Delta> extends \<Gamma>" by fact
   1.580 -  have "T1 closed_in \<Delta>" using extends b5 by (simp only: extends_closed)
   1.581 -  hence "\<turnstile> ((X,T1)#\<Delta>) ok" using fresh ok by force   
   1.582 +  have ext: "\<Delta> extends \<Gamma>" by fact
   1.583 +  have "T\<^isub>1 closed_in \<Delta>" using ext closed\<^isub>T\<^isub>1 by (simp only: extends_closed)
   1.584 +  hence "\<turnstile> ((X,T\<^isub>1)#\<Delta>) ok" using fresh_cond ok by force   
   1.585    moreover 
   1.586 -  have "((X,T1)#\<Delta>) extends ((X,T1)#\<Gamma>)" using extends by (force simp add: extends_def)
   1.587 -  ultimately have "((X,T1)#\<Delta>) \<turnstile> S2 <: T2" using ih2 by simp
   1.588 +  have "((X,T\<^isub>1)#\<Delta>) extends ((X,T\<^isub>1)#\<Gamma>)" using ext by (force simp add: extends_def)
   1.589 +  ultimately have "((X,T\<^isub>1)#\<Delta>) \<turnstile> S\<^isub>2 <: T\<^isub>2" using ih\<^isub>2 by simp
   1.590    moreover
   1.591 -  have "\<Delta> \<turnstile> T1 <: S1" using ok extends ih1 by simp 
   1.592 -  ultimately show "\<Delta> \<turnstile> \<forall> [X<:S1].S2 <: \<forall> [X<:T1].T2" using ok by (force intro: S_All) 
   1.593 -qed
   1.594 +  have "\<Delta> \<turnstile> T\<^isub>1 <: S\<^isub>1" using ok ext ih\<^isub>1 by simp 
   1.595 +  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_All)
   1.596 +qed (blast intro: extends_closed extends_memb dest: extends_domain)+
   1.597  
   1.598 +text {* our contexts grow from right to left *}
   1.599  
   1.600  lemma transitivity_and_narrowing:
   1.601    shows "\<Gamma> \<turnstile> S <: Q \<Longrightarrow> \<Gamma> \<turnstile> Q <: T \<Longrightarrow> \<Gamma> \<turnstile> S <: T"
   1.602 -  and   "(\<Delta>@(X,Q)#\<Gamma>) \<turnstile> M <: N \<Longrightarrow> \<Gamma> \<turnstile> P <: Q \<Longrightarrow> (\<Delta>@(X,P)#\<Gamma>) \<turnstile> M <: N"
   1.603 +  and "(\<Delta>@[(X,Q)]@\<Gamma>) \<turnstile> M <: N \<Longrightarrow> \<Gamma> \<turnstile> P <: Q \<Longrightarrow> (\<Delta>@[(X,P)]@\<Gamma>) \<turnstile> M <: N"
   1.604  proof (induct Q fixing: \<Gamma> S T and \<Delta> \<Gamma> X P M N taking: "size_ty" rule: measure_induct_rule)
   1.605 -  case (less Q)
   1.606 -  note  IH1_outer = less[THEN conjunct1, rule_format]
   1.607 -    and IH2_outer = less[THEN conjunct2, THEN spec, of _ "[]", simplified, rule_format]
   1.608 +  case (less Q) 
   1.609 +  note IH_trans = prems[THEN conjunct1, rule_format]
   1.610 +  note IH_narrow = prems[THEN conjunct2, THEN spec, of _ "[]", simplified, rule_format]
   1.611  
   1.612 +    --{* The inner induction for transitivity over @{term "\<Gamma> \<turnstile> S <: Q"} *}
   1.613    have transitivity: 
   1.614      "\<And>\<Gamma> S T. \<Gamma> \<turnstile> S <: Q \<Longrightarrow> \<Gamma> \<turnstile> Q <: T \<Longrightarrow> \<Gamma> \<turnstile> S <: T"
   1.615    proof - 
   1.616      
   1.617 -  -- {* We first handle the case where T = Top once and for all; this saves some 
   1.618 -        repeated argument below (just like on paper :-).  We establish a little lemma
   1.619 -        that is invoked where needed in each case of the induction. *} 
   1.620 +      -- {* We first handle the case where T = Top once and for all; this saves some 
   1.621 +      repeated argument below (just like on paper :-).  To do so we establish a little 
   1.622 +      lemma that is invoked where needed in the induction for transitivity. *} 
   1.623      have top_case: 
   1.624        "\<And>\<Gamma> S T' P. \<lbrakk>\<turnstile> \<Gamma> ok; S closed_in \<Gamma>; P \<Longrightarrow> \<Gamma> \<turnstile> S <: T'; T'=Top \<or> P\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> S <: T'"
   1.625      proof - 
   1.626        fix \<Gamma> S T' P
   1.627 -      assume S_Top_prem1: "S closed_in \<Gamma>"
   1.628 -	and  S_Top_prem2: "\<turnstile> \<Gamma> ok"
   1.629 +      assume S_Top_prm1: "S closed_in \<Gamma>"
   1.630 +	and  S_Top_prm2: "\<turnstile> \<Gamma> ok"
   1.631  	and  alternative: "P \<Longrightarrow> \<Gamma> \<turnstile> S <: T'" 
   1.632  	and  "T'=Top \<or> P" 
   1.633        moreover
   1.634        { assume "T'=Top"
   1.635 -	hence "\<Gamma> \<turnstile> S <: T'" using S_Top_prem1 S_Top_prem2 by (simp add: S_Top)
   1.636 +	hence "\<Gamma> \<turnstile> S <: T'" using S_Top_prm1 S_Top_prm2 by (simp add: S_Top)
   1.637        } 
   1.638        moreover 
   1.639        { assume P 
   1.640 @@ -719,199 +717,184 @@
   1.641        ultimately show "\<Gamma> \<turnstile> S <: T'" by blast
   1.642      qed
   1.643  
   1.644 -    (* Now proceed by induction on the left-hand derivation *)
   1.645 -    fix \<Gamma> S T
   1.646 -    assume a: "\<Gamma> \<turnstile> S <: Q" 
   1.647 -    assume b: "\<Gamma> \<turnstile> Q <: T"
   1.648 -    from a b show "\<Gamma> \<turnstile> S <: T"
   1.649 -    proof(nominal_induct \<Gamma> S Q\<equiv>Q avoiding: \<Gamma> S T rule: subtype_of_rel_induct)
   1.650 -      case (S_Top \<Gamma>1 S1) --{* lh drv.: @{term "\<Gamma> \<turnstile> S <: Q \<equiv> \<Gamma>1 \<turnstile> S1 <: Top"} *}
   1.651 -      have lh_drv_prem1: "\<turnstile> \<Gamma>1 ok" by fact
   1.652 -      have lh_drv_prem2: "S1 closed_in \<Gamma>1" by fact
   1.653 -      have Q_inst: "Top=Q" by fact
   1.654 -      have rh_drv: "\<Gamma>1 \<turnstile> Q <: T" --"rh drv." by fact
   1.655 -      hence "T = Top" using Q_inst by (simp add: S_TopE)
   1.656 -      thus "\<Gamma>1 \<turnstile> S1 <: T" using top_case[of "\<Gamma>1" "S1" "False" "T"] lh_drv_prem1 lh_drv_prem2 by blast
   1.657 +	--{* Now proceed by the inner induction on the left-hand derivation *}
   1.658 +    fix \<Gamma>' S' T
   1.659 +    assume a: "\<Gamma>' \<turnstile> S' <: Q" --{* lh derivation *}
   1.660 +    assume b: "\<Gamma>' \<turnstile> Q <: T" --{* rh derivation *}
   1.661 +    from a b show "\<Gamma>' \<turnstile> S' <: T"
   1.662 +    proof(nominal_induct \<Gamma>' S' Q\<equiv>Q avoiding: \<Gamma>' S' T rule: subtype_of_rel_induct)
   1.663 +      case (S_Top \<Gamma> S) 
   1.664 +	--{* in this case lh drv is @{term "\<Gamma> \<turnstile> S <: Top"} *}
   1.665 +      hence rh_drv: "\<Gamma> \<turnstile> Top <: T" by simp
   1.666 +      hence T_inst: "T = Top" by (simp add: S_TopE)
   1.667 +      have lh_drv_prm1: "\<turnstile> \<Gamma> ok" by fact
   1.668 +      have lh_drv_prm2: "S closed_in \<Gamma>" by fact
   1.669 +      from lh_drv_prm1 lh_drv_prm2 have "\<Gamma> \<turnstile> S <: Top" by (simp add: subtype_of_rel.S_Top)
   1.670 +      thus "\<Gamma> \<turnstile> S <: T" using T_inst by simp
   1.671      next
   1.672 -      case (S_Var \<Gamma>1 X1 S1 T1) --{* lh drv.: @{term "\<Gamma> \<turnstile> S <: Q \<equiv> \<Gamma>1 \<turnstile> TVar(X1) <: S1"} *}
   1.673 -      have lh_drv_prem1: "\<turnstile> \<Gamma>1 ok" by fact
   1.674 -      have lh_drv_prem2: "(X1,S1)\<in>set \<Gamma>1" by fact
   1.675 -      have IH_inner: "\<And>T. \<Gamma>1 \<turnstile> Q <: T \<Longrightarrow> T1=Q \<Longrightarrow> \<Gamma>1 \<turnstile> S1 <: T" by fact
   1.676 -      have Q_inst: "T1=Q" by fact
   1.677 -      have rh_drv: "\<Gamma>1 \<turnstile> Q <: T" by fact 
   1.678 -      with IH_inner have "\<Gamma>1 \<turnstile> S1 <: T" using Q_inst by simp
   1.679 -      thus "\<Gamma>1 \<turnstile> TyVar X1 <: T" using lh_drv_prem1 lh_drv_prem2 by (simp add: subtype_of_rel.S_Var)
   1.680 +      case (S_Var \<Gamma> Y U Q) 
   1.681 +	--{* in this case lh drv is @{term "\<Gamma> \<turnstile> TVar(Y) <: Q"} *}
   1.682 +      hence IH_inner: "\<Gamma> \<turnstile> U <: T" by simp
   1.683 +      have lh_drv_prm1: "\<turnstile> \<Gamma> ok" by fact
   1.684 +      have lh_drv_prm2: "(Y,U)\<in>set \<Gamma>" by fact
   1.685 +      from IH_inner show "\<Gamma> \<turnstile> TVar Y <: T" using lh_drv_prm1 lh_drv_prm2 
   1.686 +	by (simp add: subtype_of_rel.S_Var)
   1.687      next
   1.688 -      case S_Refl --{* @{text S_Refl} case *} 
   1.689 -	thus ?case by simp
   1.690 +      case (S_Refl \<Gamma> X) 
   1.691 +	--{* in this case lh drv is @{term "\<Gamma> \<turnstile> TVar X <: TVar X"} *}
   1.692 +      thus "\<Gamma> \<turnstile> TVar X <: T" by simp
   1.693      next
   1.694 -      case (S_Arrow \<Gamma>1 S1 S2 T1 T2) --{* lh drv.: @{term "\<Gamma> \<turnstile> S <: Q \<equiv> \<Gamma>1 \<turnstile> S1 \<rightarrow> S2 <: T1 \<rightarrow> T2"} *}
   1.695 -      have lh_drv_prem1: "\<Gamma>1 \<turnstile> T1 <: S1" by fact
   1.696 -      have lh_drv_prem2: "\<Gamma>1 \<turnstile> S2 <: T2" by fact
   1.697 -      have rh_deriv: "\<Gamma>1 \<turnstile> Q <: T" by fact
   1.698 -      have Q_inst: "T1 \<rightarrow> T2 = Q" by fact
   1.699 -      have measure: "size_ty T1 < size_ty Q" "size_ty T2 < size_ty Q " using Q_inst by force+
   1.700 -      have "S1 closed_in \<Gamma>1" and "S2 closed_in \<Gamma>1" 
   1.701 -	using lh_drv_prem1 lh_drv_prem2 by (simp_all add: subtype_implies_closed)
   1.702 -      hence "(S1 \<rightarrow> S2) closed_in \<Gamma>1" by (simp add: closed_in_def ty.supp)
   1.703 +      case (S_Arrow \<Gamma> S1 S2 Q1 Q2) 
   1.704 +	--{* in this case lh drv is @{term "\<Gamma> \<turnstile> S1 \<rightarrow> S2 <: Q1 \<rightarrow> Q2"} *}
   1.705 +      hence rh_drv: "\<Gamma> \<turnstile> Q1 \<rightarrow> Q2 <: T" by simp
   1.706 +      have Q_inst: "Q1 \<rightarrow> Q2 = Q" by fact
   1.707 +      hence Q1_less: "size_ty Q1 < size_ty Q" 
   1.708 +	and Q2_less: "size_ty Q2 < size_ty Q" by auto
   1.709 +      have lh_drv_prm1: "\<Gamma> \<turnstile> Q1 <: S1" by fact
   1.710 +      have lh_drv_prm2: "\<Gamma> \<turnstile> S2 <: Q2" by fact      
   1.711 +      have "S1 closed_in \<Gamma>" and "S2 closed_in \<Gamma>" 
   1.712 +	using lh_drv_prm1 lh_drv_prm2 by (simp_all add: subtype_implies_closed)
   1.713 +      hence "(S1 \<rightarrow> S2) closed_in \<Gamma>" by (simp add: closed_in_def ty.supp)
   1.714        moreover
   1.715 -      have "\<turnstile> \<Gamma>1 ok" using rh_deriv by (rule subtype_implies_ok)
   1.716 +      have "\<turnstile> \<Gamma> ok" using rh_drv by (rule subtype_implies_ok)
   1.717        moreover
   1.718 -      have "T = Top \<or> (\<exists>T3 T4.  T= T3 \<rightarrow> T4 \<and> \<Gamma>1 \<turnstile> T3 <: T1 \<and> \<Gamma>1 \<turnstile> T2 <: T4)" 
   1.719 -	using rh_deriv Q_inst by (simp add:S_ArrowE_left)  
   1.720 +      from rh_drv have "T = Top \<or> (\<exists>T1 T2.  T = T1 \<rightarrow> T2 \<and> \<Gamma> \<turnstile> T1 <: Q1 \<and> \<Gamma> \<turnstile> Q2 <: T2)" 
   1.721 +	by (simp add: S_ArrowE_left)  
   1.722        moreover
   1.723 -      { assume "\<exists>T3 T4. T= T3 \<rightarrow> T4 \<and> \<Gamma>1 \<turnstile> T3 <: T1 \<and> \<Gamma>1 \<turnstile> T2 <: T4"
   1.724 -	then obtain T3 T4 
   1.725 -	  where T_inst: "T= T3 \<rightarrow> T4" 
   1.726 -	  and   rh_drv_prem1: "\<Gamma>1 \<turnstile> T3 <: T1"
   1.727 -	  and   rh_drv_prem2: "\<Gamma>1 \<turnstile> T2 <: T4" by force
   1.728 -        from IH1_outer[of "T1"] have "\<Gamma>1 \<turnstile> T3 <: S1" using measure rh_drv_prem1 lh_drv_prem1 by blast
   1.729 +      { assume "\<exists>T1 T2. T = T1 \<rightarrow> T2 \<and> \<Gamma> \<turnstile> T1 <: Q1 \<and> \<Gamma> \<turnstile> Q2 <: T2"
   1.730 +	then obtain T1 T2 
   1.731 +	  where T_inst: "T = T1 \<rightarrow> T2" 
   1.732 +	  and   rh_drv_prm1: "\<Gamma> \<turnstile> T1 <: Q1"
   1.733 +	  and   rh_drv_prm2: "\<Gamma> \<turnstile> Q2 <: T2" by force
   1.734 +        from IH_trans[of "Q1"] have "\<Gamma> \<turnstile> T1 <: S1" using Q1_less rh_drv_prm1 lh_drv_prm1 by simp 
   1.735  	moreover
   1.736 -	from IH1_outer[of "T2"] have "\<Gamma>1 \<turnstile> S2 <: T4" using measure rh_drv_prem2 lh_drv_prem2 by blast
   1.737 -	ultimately have "\<Gamma>1 \<turnstile> S1 \<rightarrow> S2 <: T" using T_inst by force
   1.738 +	from IH_trans[of "Q2"] have "\<Gamma> \<turnstile> S2 <: T2" using Q2_less rh_drv_prm2 lh_drv_prm2 by simp
   1.739 +	ultimately have "\<Gamma> \<turnstile> S1 \<rightarrow> S2 <: T1 \<rightarrow> T2" by (simp add: subtype_of_rel.S_Arrow)
   1.740 +	hence "\<Gamma> \<turnstile> S1 \<rightarrow> S2 <: T" using T_inst by simp
   1.741        }
   1.742 -      ultimately show "\<Gamma>1 \<turnstile> S1 \<rightarrow> S2 <: T" using top_case[of "\<Gamma>1" "S1\<rightarrow>S2" _ "T'"] by blast
   1.743 +      ultimately show "\<Gamma> \<turnstile> S1 \<rightarrow> S2 <: T" using top_case by blast
   1.744      next
   1.745 -      case (S_All \<Gamma>1 X S1 S2 T1 T2) --{* lh drv.: @{term "\<Gamma>\<turnstile>S<:Q \<equiv> \<Gamma>1\<turnstile>\<forall>[X<:S1].S2 <: \<forall>[X<:T1].T2"} *} 
   1.746 -      have lh_drv_prem1: "\<Gamma>1 \<turnstile> T1 <: S1" by fact
   1.747 -      have lh_drv_prem2: "((X,T1)#\<Gamma>1) \<turnstile> S2 <: T2" by fact
   1.748 -      have rh_deriv: "\<Gamma>1 \<turnstile> Q <: T" by fact
   1.749 -      have fresh_cond: "X\<sharp>\<Gamma>1" "X\<sharp>S1" "X\<sharp>T1" by fact
   1.750 -      have Q_inst: "\<forall>[X<:T1].T2 = Q" by fact
   1.751 -      have measure: "size_ty T1 < size_ty Q" "size_ty T2 < size_ty Q " using Q_inst by force+
   1.752 -      have "S1 closed_in \<Gamma>1" and "S2 closed_in ((X,T1)#\<Gamma>1)" 
   1.753 -	using lh_drv_prem1 lh_drv_prem2 by (simp_all add: subtype_implies_closed)
   1.754 -      hence "(\<forall>[X<:S1].S2) closed_in \<Gamma>1" by (force simp add: closed_in_def ty.supp abs_supp)
   1.755 +      case (S_All \<Gamma> X S1 S2 Q1 Q2) 
   1.756 +	--{* in this case lh drv is @{term "\<Gamma>\<turnstile>\<forall>[X<:S1].S2 <: \<forall>[X<:Q1].Q2"} *}
   1.757 +      hence rh_drv: "\<Gamma> \<turnstile> \<forall>[X<:Q1].Q2 <: T" by simp
   1.758 +      have lh_drv_prm1: "\<Gamma> \<turnstile> Q1 <: S1" by fact
   1.759 +      have lh_drv_prm2: "((X,Q1)#\<Gamma>) \<turnstile> S2 <: Q2" by fact
   1.760 +      have fresh_cond: "X\<sharp>\<Gamma>" "X\<sharp>Q1" by fact
   1.761 +      have Q_inst: "\<forall>[X<:Q1].Q2 = Q" by fact
   1.762 +      hence Q1_less: "size_ty Q1 < size_ty Q" 
   1.763 +	and Q2_less: "size_ty Q2 < size_ty Q " by auto
   1.764 +      have "S1 closed_in \<Gamma>" and "S2 closed_in ((X,Q1)#\<Gamma>)" 
   1.765 +	using lh_drv_prm1 lh_drv_prm2 by (simp_all add: subtype_implies_closed)
   1.766 +      hence "(\<forall>[X<:S1].S2) closed_in \<Gamma>" by (force simp add: closed_in_def ty.supp abs_supp)
   1.767        moreover
   1.768 -      have "\<turnstile> \<Gamma>1 ok" using rh_deriv by (rule subtype_implies_ok)
   1.769 +      have "\<turnstile> \<Gamma> ok" using rh_drv by (rule subtype_implies_ok)
   1.770        moreover
   1.771 -        (* FIX: Maybe T3,T4 could be T1',T2' *)
   1.772 -      have "T = Top \<or> (\<exists>T3 T4. T=\<forall>[X<:T3].T4 \<and> \<Gamma>1 \<turnstile> T3 <: T1 \<and> ((X,T3)#\<Gamma>1) \<turnstile> T2 <: T4)" 
   1.773 -	using rh_deriv fresh_cond Q_inst by (auto dest: S_AllE_left simp add: fresh_prod)
   1.774 +      from rh_drv have "T = Top \<or> (\<exists>T1 T2. T = \<forall>[X<:T1].T2 \<and> \<Gamma> \<turnstile> T1 <: Q1 \<and> ((X,T1)#\<Gamma>) \<turnstile> Q2 <: T2)" 
   1.775 +	using fresh_cond by (simp add: S_AllE_left)
   1.776        moreover
   1.777 -      { assume "\<exists>T3 T4. T=\<forall>[X<:T3].T4 \<and> \<Gamma>1 \<turnstile> T3 <: T1 \<and> ((X,T3)#\<Gamma>1) \<turnstile> T2 <: T4"
   1.778 -	then obtain T3 T4 
   1.779 -	  where T_inst: "T= \<forall>[X<:T3].T4" 
   1.780 -	  and   rh_drv_prem1: "\<Gamma>1 \<turnstile> T3 <: T1" 
   1.781 -	  and   rh_drv_prem2:"((X,T3)#\<Gamma>1) \<turnstile> T2 <: T4" by force
   1.782 -        from IH1_outer[of "T1"] have "\<Gamma>1 \<turnstile> T3 <: S1" 
   1.783 -	  using lh_drv_prem1 rh_drv_prem1 measure by blast
   1.784 +      { assume "\<exists>T1 T2. T = \<forall>[X<:T1].T2 \<and> \<Gamma> \<turnstile> T1 <: Q1 \<and> ((X,T1)#\<Gamma>) \<turnstile> Q2 <: T2"
   1.785 +	then obtain T1 T2 
   1.786 +	  where T_inst: "T = \<forall>[X<:T1].T2" 
   1.787 +	  and   rh_drv_prm1: "\<Gamma> \<turnstile> T1 <: Q1" 
   1.788 +	  and   rh_drv_prm2:"((X,T1)#\<Gamma>) \<turnstile> Q2 <: T2" by force
   1.789 +        from IH_trans[of "Q1"] have "\<Gamma> \<turnstile> T1 <: S1" 
   1.790 +	  using lh_drv_prm1 rh_drv_prm1 Q1_less by blast
   1.791          moreover
   1.792 -	from IH2_outer[of "T1"] have "((X,T3)#\<Gamma>1) \<turnstile> S2 <: T2" 
   1.793 -	  using measure lh_drv_prem2 rh_drv_prem1 by force
   1.794 -	with IH1_outer[of "T2"] have "((X,T3)#\<Gamma>1) \<turnstile> S2 <: T4" 
   1.795 -	  using measure rh_drv_prem2 by force
   1.796 +	from IH_narrow[of "Q1"] have "((X,T1)#\<Gamma>) \<turnstile> S2 <: Q2" 
   1.797 +	  using Q1_less lh_drv_prm2 rh_drv_prm1 by blast
   1.798 +	with IH_trans[of "Q2"] have "((X,T1)#\<Gamma>) \<turnstile> S2 <: T2" 
   1.799 +	  using Q2_less rh_drv_prm2 by blast
   1.800          moreover
   1.801 -	ultimately have "\<Gamma>1 \<turnstile> \<forall>[X<:S1].S2 <: T"
   1.802 -	  using fresh_cond T_inst by (simp add: fresh_prod subtype_of_rel.S_All)
   1.803 +	ultimately have "\<Gamma> \<turnstile> \<forall>[X<:S1].S2 <: \<forall>[X<:T1].T2"
   1.804 +	  using fresh_cond by (simp add: subtype_of_rel.S_All)
   1.805 +	hence "\<Gamma> \<turnstile> \<forall>[X<:S1].S2 <: T" using T_inst by simp
   1.806        }
   1.807 -      ultimately show "\<Gamma>1 \<turnstile> \<forall>[X<:S1].S2 <: T" using Q_inst top_case[of "\<Gamma>1" "\<forall>[X<:S1].S2" _ "T'"] 
   1.808 -	by auto
   1.809 +      ultimately show "\<Gamma> \<turnstile> \<forall>[X<:S1].S2 <: T" using top_case by blast
   1.810      qed
   1.811    qed
   1.812  
   1.813 +  --{* The inner induction for narrowing over @{term "(\<Delta>@[(X,Q)]@\<Gamma>) \<turnstile> M <: N"} *}
   1.814    have narrowing:
   1.815 -    "\<And>\<Delta> \<Gamma> X M N P. (\<Delta>@(X,Q)#\<Gamma>) \<turnstile> M <: N \<Longrightarrow> \<Gamma> \<turnstile> P<:Q \<Longrightarrow> (\<Delta>@(X,P)#\<Gamma>) \<turnstile> M <: N"
   1.816 +    "\<And>\<Delta> \<Gamma> X M N P. (\<Delta>@[(X,Q)]@\<Gamma>) \<turnstile> M <: N \<Longrightarrow> \<Gamma> \<turnstile> P<:Q \<Longrightarrow> (\<Delta>@[(X,P)]@\<Gamma>) \<turnstile> M <: N"
   1.817    proof -
   1.818 -    fix \<Delta> \<Gamma> X M N P
   1.819 -    assume a: "(\<Delta>@(X,Q)#\<Gamma>) \<turnstile> M <: N"
   1.820 -    assume b: "\<Gamma> \<turnstile> P<:Q"
   1.821 -    show "(\<Delta>@(X,P)#\<Gamma>) \<turnstile> M <: N"
   1.822 -      using a b 
   1.823 -    proof (nominal_induct \<Gamma>\<equiv>"\<Delta>@(X,Q)#\<Gamma>" M N avoiding: \<Delta> \<Gamma> X rule: subtype_of_rel_induct) 
   1.824 -      case (S_Top \<Gamma>1 S1 \<Delta> \<Gamma>2 X)
   1.825 -      then have lh_drv_prem1: "\<turnstile> (\<Delta>@(X,Q)#\<Gamma>2) ok" 
   1.826 -           and  lh_drv_prem2: "S1 closed_in (\<Delta>@(X,Q)#\<Gamma>2)" by (simp_all only:)
   1.827 -      have rh_drv: "\<Gamma>2 \<turnstile> P <: Q" by fact
   1.828 -      hence "P closed_in \<Gamma>2" by (simp add: subtype_implies_closed)
   1.829 -      with lh_drv_prem1 have "\<turnstile> (\<Delta>@(X,P)#\<Gamma>2) ok" by (simp only: replace_type)
   1.830 +    fix \<Delta>' \<Gamma>' X M N P
   1.831 +    assume a: "(\<Delta>'@[(X,Q)]@\<Gamma>') \<turnstile> M <: N"
   1.832 +    assume b: "\<Gamma>' \<turnstile> P<:Q"
   1.833 +    from a b show "(\<Delta>'@[(X,P)]@\<Gamma>') \<turnstile> M <: N" 
   1.834 +    proof (nominal_induct \<Gamma>\<equiv>"\<Delta>'@[(X,Q)]@\<Gamma>'" M N avoiding: \<Delta>' \<Gamma>' X rule: subtype_of_rel_induct) 
   1.835 +      case (S_Top _ S \<Delta> \<Gamma> X)
   1.836 +	--{* in this case lh drv is @{term "(\<Delta>@[(X,Q)]@\<Gamma>) \<turnstile> S <: Top"} *}
   1.837 +      hence lh_drv_prm1: "\<turnstile> (\<Delta>@[(X,Q)]@\<Gamma>) ok" 
   1.838 +        and lh_drv_prm2: "S closed_in (\<Delta>@[(X,Q)]@\<Gamma>)" by simp_all
   1.839 +      have rh_drv: "\<Gamma> \<turnstile> P <: Q" by fact
   1.840 +      hence "P closed_in \<Gamma>" by (simp add: subtype_implies_closed)
   1.841 +      with lh_drv_prm1 have "\<turnstile> (\<Delta>@[(X,P)]@\<Gamma>) ok" by (simp add: replace_type)
   1.842        moreover
   1.843 -      from lh_drv_prem2 have "S1 closed_in (\<Delta>@(X,P)#\<Gamma>2)" by (simp add: closed_in_def domain_append)
   1.844 -      ultimately show "(\<Delta>@(X,P)#\<Gamma>2) \<turnstile> S1 <: Top" by (rule subtype_of_rel.S_Top)
   1.845 +      from lh_drv_prm2 have "S closed_in (\<Delta>@[(X,P)]@\<Gamma>)" by (simp add: closed_in_def domain_append)
   1.846 +      ultimately show "(\<Delta>@[(X,P)]@\<Gamma>) \<turnstile> S <: Top" by (simp add: subtype_of_rel.S_Top)
   1.847      next
   1.848 -      case (S_Var \<Gamma>1 X1 S1 T1 \<Delta> \<Gamma>2 X)
   1.849 -      then have lh_drv_prem1: "\<turnstile> (\<Delta>@(X,Q)#\<Gamma>2) ok" 
   1.850 -           and  lh_drv_prem2: "(X1,S1)\<in>set (\<Delta>@(X,Q)#\<Gamma>2)" 
   1.851 -           and  lh_drv_prem3: "(\<Delta>@(X,Q)#\<Gamma>2) \<turnstile> S1 <: T1" 
   1.852 -           and  IH_inner: "\<Gamma>2 \<turnstile> P <: Q \<Longrightarrow> (\<Delta>@(X,P)#\<Gamma>2) \<turnstile> S1 <: T1" by (simp_all only:)
   1.853 -      have rh_drv: "\<Gamma>2 \<turnstile> P <: Q" by fact
   1.854 -      hence "P closed_in \<Gamma>2" by (simp add: subtype_implies_closed)
   1.855 -      hence a3: "\<turnstile> (\<Delta>@(X,P)#\<Gamma>2) ok" using lh_drv_prem1 by (simp only: replace_type)
   1.856 -      show "(\<Delta>@(X,P)#\<Gamma>2) \<turnstile> TyVar X1 <: T1"
   1.857 -      proof (cases "X=X1")
   1.858 -	case False
   1.859 -	have b0: "X\<noteq>X1" by fact
   1.860 -	from lh_drv_prem3 rh_drv IH_inner 
   1.861 -	have b1: "(\<Delta>@(X,P)#\<Gamma>2) \<turnstile> S1 <: T1" by simp
   1.862 -	from lh_drv_prem2 b0 have b2: "(X1,S1)\<in>set (\<Delta>@(X,P)#\<Gamma>2)" by simp
   1.863 -	show "(\<Delta>@(X,P)#\<Gamma>2) \<turnstile> TyVar X1 <: T1" using a3 b2 b1 by (rule subtype_of_rel.S_Var)
   1.864 -      next 
   1.865 -	case True
   1.866 -	have b0: "X=X1" by fact
   1.867 -	have a4: "S1=Q"
   1.868 -	proof -
   1.869 -	  have "(X1,Q)\<in>set (\<Delta>@(X,Q)#\<Gamma>2)" using b0 by simp
   1.870 -	  with lh_drv_prem1 lh_drv_prem2 show "S1=Q" by (blast intro: uniqueness_of_ctxt)
   1.871 -	qed
   1.872 -	have a5: "(\<Delta>@(X,P)#\<Gamma>2) extends \<Gamma>2" by (force simp add: extends_def)
   1.873 -	have a6: "(\<Delta>@(X1,P)#\<Gamma>2) \<turnstile> P <: Q" using b0 a5 rh_drv a3 by (simp add: weakening)	
   1.874 -	have a7: "(\<Delta>@(X1,P)#\<Gamma>2) \<turnstile> Q <: T1" using b0 IH_inner lh_drv_prem3 rh_drv a4 by simp
   1.875 -	have a8: "(\<Delta>@(X1,P)#\<Gamma>2) \<turnstile> P <: T1" using a6 a7 transitivity by blast
   1.876 -	have a9: "(X1,P)\<in>set (\<Delta>@(X,P)#\<Gamma>2)" using b0 by simp
   1.877 -	show "(\<Delta>@(X,P)#\<Gamma>2) \<turnstile> TyVar X1 <: T1" using a3 b0 a8 a9 by force
   1.878 -      qed
   1.879 +      case (S_Var _ Y S N \<Delta> \<Gamma> X) 
   1.880 +	--{* in this case lh drv is @{term "(\<Delta>@[(X,Q)]@\<Gamma>) \<turnstile> TVar Y <: N"} *}
   1.881 +      hence IH_inner: "(\<Delta>@[(X,P)]@\<Gamma>) \<turnstile> S <: N" 
   1.882 +	and lh_drv_prm1: "\<turnstile> (\<Delta>@[(X,Q)]@\<Gamma>) ok" 
   1.883 +        and lh_drv_prm2: "(Y,S)\<in>set (\<Delta>@[(X,Q)]@\<Gamma>)" by simp_all
   1.884 +      have rh_drv: "\<Gamma> \<turnstile> P <: Q" by fact
   1.885 +      hence "P closed_in \<Gamma>" by (simp add: subtype_implies_closed)
   1.886 +      hence cntxt_ok: "\<turnstile> (\<Delta>@[(X,P)]@\<Gamma>) ok" using lh_drv_prm1 by (simp add: replace_type)
   1.887 +	-- {* we distinguishing the cases @{term "X\<noteq>Y"} and @{term "X=Y"} (the latter 
   1.888 +	being the interesting one) *}
   1.889 +      { assume "X\<noteq>Y"
   1.890 +	hence "(Y,S)\<in>set (\<Delta>@[(X,P)]@\<Gamma>)" using lh_drv_prm2 by simp
   1.891 +	with IH_inner have "(\<Delta>@[(X,P)]@\<Gamma>) \<turnstile> TVar Y <: N" 
   1.892 +	  using cntxt_ok by (simp add: subtype_of_rel.S_Var)
   1.893 +      }
   1.894 +      moreover
   1.895 +      { have memb_XQ: "(X,Q)\<in>set (\<Delta>@[(X,Q)]@\<Gamma>)" by simp
   1.896 +	have memb_XP: "(X,P)\<in>set (\<Delta>@[(X,P)]@\<Gamma>)" by simp
   1.897 +	assume "X=Y" 
   1.898 +	hence "S=Q" using lh_drv_prm1 lh_drv_prm2 memb_XQ by (simp only: uniqueness_of_ctxt)
   1.899 +	hence "(\<Delta>@[(X,P)]@\<Gamma>) \<turnstile> Q <: N" using IH_inner by simp
   1.900 +	moreover
   1.901 +	have "(\<Delta>@[(X,P)]@\<Gamma>) extends \<Gamma>" by (simp add: extends_def)
   1.902 +	hence "(\<Delta>@[(X,P)]@\<Gamma>) \<turnstile> P <: Q" using rh_drv cntxt_ok by (simp only: weakening)
   1.903 +	ultimately have "(\<Delta>@[(X,P)]@\<Gamma>) \<turnstile> P <: N" using transitivity by simp
   1.904 +	hence "(\<Delta>@[(X,P)]@\<Gamma>) \<turnstile> TVar X <: N" using memb_XP cntxt_ok 
   1.905 +	  by (simp only: subtype_of_rel.S_Var)
   1.906 +      }
   1.907 +      ultimately show "(\<Delta>@[(X,P)]@\<Gamma>) \<turnstile> TVar Y <: N" by blast
   1.908      next
   1.909 -      case (S_Refl \<Gamma>1 X1 \<Delta> \<Gamma>2 X)
   1.910 -      have lh_drv_prem1: "\<turnstile> \<Gamma>1 ok" by fact
   1.911 -      have lh_drv_prem2: "X1 \<in> domain \<Gamma>1" by fact
   1.912 -      have \<Gamma>1_inst: "\<Gamma>1 = \<Delta>@(X,Q)#\<Gamma>2" by fact
   1.913 -      have "\<Gamma>2 \<turnstile> P <: Q" by fact
   1.914 -      hence "P closed_in \<Gamma>2" by (simp add: subtype_implies_closed)
   1.915 -      hence a3: "\<turnstile> (\<Delta>@(X,P)#\<Gamma>2) ok" using lh_drv_prem1 \<Gamma>1_inst by (simp add: replace_type)
   1.916 -      have b0: "X1 \<in> domain (\<Delta>@(X,P)#\<Gamma>2)" using lh_drv_prem2 \<Gamma>1_inst by (simp add: domain_append)
   1.917 -      show "(\<Delta>@(X,P)#\<Gamma>2) \<turnstile> TyVar X1 <: TyVar X1" using a3 b0 by (rule subtype_of_rel.S_Refl)
   1.918 -    next
   1.919 -      case S_Arrow thus ?case by blast
   1.920 +      case (S_Refl _ Y \<Delta> \<Gamma> X)
   1.921 +	--{* in this case lh drv is @{term "(\<Delta>@[(X,Q)]@\<Gamma>) \<turnstile> TVar Y <: TVar Y"} *}
   1.922 +      hence lh_drv_prm1: "\<turnstile> (\<Delta>@[(X,Q)]@\<Gamma>) ok" 
   1.923 +	and lh_drv_prm2: "Y \<in> domain (\<Delta>@[(X,Q)]@\<Gamma>)" by simp_all
   1.924 +      have "\<Gamma> \<turnstile> P <: Q" by fact
   1.925 +      hence "P closed_in \<Gamma>" by (simp add: subtype_implies_closed)
   1.926 +      with lh_drv_prm1 have "\<turnstile> (\<Delta>@[(X,P)]@\<Gamma>) ok" by (simp add: replace_type)
   1.927 +      moreover
   1.928 +      from lh_drv_prm2 have "Y \<in> domain (\<Delta>@[(X,P)]@\<Gamma>)" by (simp add: domain_append)
   1.929 +      ultimately show "(\<Delta>@[(X,P)]@\<Gamma>) \<turnstile> TVar Y <: TVar Y" by (simp add: subtype_of_rel.S_Refl)
   1.930      next
   1.931 -      case (S_All \<Gamma>1 X1 S1 S2 T1 T2 \<Delta> \<Gamma>2 X)
   1.932 -      have IH_inner1: "\<And>\<Delta> \<Gamma> X. \<Gamma> \<turnstile> P <: Q \<Longrightarrow> \<Gamma>1 = \<Delta>@(X,Q)#\<Gamma> \<Longrightarrow> (\<Delta>@(X,P)#\<Gamma>) \<turnstile> T1 <: S1" by fact
   1.933 -      have IH_inner2: "\<And>\<Delta> \<Gamma> X. \<Gamma> \<turnstile> P <: Q \<Longrightarrow> (X1,T1)#\<Gamma>1 = \<Delta>@(X,Q)#\<Gamma> \<Longrightarrow> (\<Delta>@(X,P)#\<Gamma>) \<turnstile> S2 <: T2" 
   1.934 -	by fact
   1.935 -      have lh_drv_prem1: "\<Gamma>1 \<turnstile> T1 <: S1" by fact
   1.936 -      have lh_drv_prem2: "X1\<sharp>\<Gamma>1" "X1\<sharp>S1" "X1\<sharp>T1" by fact (* check this whether this is the lh_drv_p2 *)
   1.937 -      have lh_drv_prem3: "((X1,T1)#\<Gamma>1) \<turnstile> S2 <: T2" by fact
   1.938 -      have \<Gamma>1_inst: "\<Gamma>1 = \<Delta>@(X,Q)#\<Gamma>2" by fact
   1.939 -      have a2: "\<Gamma>2 \<turnstile> P <: Q" by fact
   1.940 -      have b0: "(\<Delta>@(X,P)#\<Gamma>2) \<turnstile> T1 <: S1" using \<Gamma>1_inst a2 lh_drv_prem1 IH_inner1 by simp
   1.941 -      have b1: "(((X1,T1)#\<Delta>)@(X,P)#\<Gamma>2) \<turnstile> S2 <: T2" using \<Gamma>1_inst a2 lh_drv_prem3 IH_inner2
   1.942 -	apply(auto)
   1.943 -	apply(drule_tac x="\<Gamma>2" in meta_spec)
   1.944 -	apply(drule_tac x="(X1,T1)#\<Delta>" in meta_spec)
   1.945 -	apply(auto)
   1.946 -	done
   1.947 -      have b3: "X1\<sharp>(\<Delta>@(X,P)#\<Gamma>2)" using lh_drv_prem2 \<Gamma>1_inst a2
   1.948 -	by (auto simp add: fresh_prod fresh_list_append fresh_list_cons dest: subtype_implies_fresh)
   1.949 -      show "(\<Delta>@(X,P)#\<Gamma>2) \<turnstile> \<forall> [X1<:S1].S2 <: \<forall> [X1<:T1].T2" using b0 b3 b1 by force 
   1.950 +      case (S_Arrow _ Q1 Q2 S1 S2 \<Delta> \<Gamma> X) 
   1.951 +	--{* in this case lh drv is @{term "(\<Delta>@[(X,Q)]@\<Gamma>) \<turnstile> Q1 \<rightarrow> Q2 <: S1 \<rightarrow> S2"} *}
   1.952 +      thus "(\<Delta>@[(X,P)]@\<Gamma>) \<turnstile> Q1 \<rightarrow> Q2 <: S1 \<rightarrow> S2" by blast 
   1.953 +    next
   1.954 +      case (S_All _ Y S1 S2 T1 T2 \<Delta> \<Gamma> X)
   1.955 +	--{* in this case lh drv is @{term "(\<Delta>@[(X,Q)]@\<Gamma>) \<turnstile> \<forall>[Y<:S1].S2 <: \<forall>[Y<:T1].T2"} *}
   1.956 +      hence IH_inner1: "(\<Delta>@[(X,P)]@\<Gamma>) \<turnstile> T1 <: S1" 
   1.957 +	and IH_inner2: "((Y,T1)#\<Delta>@[(X,P)]@\<Gamma>) \<turnstile> S2 <: T2" 
   1.958 +	and lh_drv_prm2: "Y\<sharp>(\<Delta>@[(X,Q)]@\<Gamma>)" by force+
   1.959 +      have rh_drv: "\<Gamma> \<turnstile> P <: Q" by fact
   1.960 +      hence "Y\<sharp>P" using lh_drv_prm2 by (simp only: fresh_list_append subtype_implies_fresh)
   1.961 +      hence "Y\<sharp>(\<Delta>@[(X,P)]@\<Gamma>)" using lh_drv_prm2 
   1.962 +	by (simp add: fresh_list_append fresh_list_cons fresh_prod)
   1.963 +      with IH_inner1 IH_inner2 
   1.964 +      show "(\<Delta>@[(X,P)]@\<Gamma>) \<turnstile> \<forall>[Y<:S1].S2 <: \<forall>[Y<:T1].T2" by (simp add: subtype_of_rel.S_All)
   1.965      qed
   1.966    qed
   1.967    from transitivity narrowing show ?case by blast 
   1.968  qed
   1.969  
   1.970  
   1.971 - 
   1.972 -section {* Terms *}
   1.973  
   1.974 -nominal_datatype trm = Var   "vrs"
   1.975 -                     | Lam   "\<guillemotleft>vrs\<guillemotright>trm" "ty"
   1.976 -                     | TAbs  "\<guillemotleft>tyvrs\<guillemotright>trm" "ty"
   1.977 -                     | App   "trm" "trm"
   1.978 -                     | TApp  "trm" "ty"
   1.979 -
   1.980 -consts
   1.981 -  Lam_syn   :: "vrs \<Rightarrow> ty \<Rightarrow> trm \<Rightarrow> trm"   ("Lam [_:_]._" [100,100,100] 100)
   1.982 -  TAbs_syn  :: "tyvrs \<Rightarrow> ty \<Rightarrow> trm \<Rightarrow> trm" ("TAbs [_<:_]._" [100,100,100] 100)
   1.983 -translations 
   1.984 -  "Lam  [a:tys].t" \<rightleftharpoons> "trm.Lam a t tys"
   1.985 -  "TAbs [a<:tys].t" \<rightleftharpoons> "trm.TAbs a t tys"
   1.986  
   1.987  end
   1.988 \ No newline at end of file