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