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