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