src/HOL/Nominal/Examples/Fsub.thy
changeset 63167 0909deb8059b
parent 61069 aefe89038dd2
child 66453 cc19f7ca2ed6
     1.1 --- a/src/HOL/Nominal/Examples/Fsub.thy	Thu May 26 16:57:14 2016 +0200
     1.2 +++ b/src/HOL/Nominal/Examples/Fsub.thy	Thu May 26 17:51:22 2016 +0200
     1.3 @@ -4,7 +4,7 @@
     1.4  begin
     1.5  (*>*)
     1.6  
     1.7 -text{* Authors: Christian Urban,
     1.8 +text\<open>Authors: Christian Urban,
     1.9                  Benjamin Pierce,
    1.10                  Dimitrios Vytiniotis
    1.11                  Stephanie Weirich
    1.12 @@ -12,26 +12,26 @@
    1.13                  Julien Narboux
    1.14                  Stefan Berghofer
    1.15  
    1.16 -       with great help from Markus Wenzel. *}
    1.17 +       with great help from Markus Wenzel.\<close>
    1.18  
    1.19 -section {* Types for Names, Nominal Datatype Declaration for Types and Terms *}
    1.20 +section \<open>Types for Names, Nominal Datatype Declaration for Types and Terms\<close>
    1.21  
    1.22  no_syntax
    1.23    "_Map" :: "maplets => 'a \<rightharpoonup> 'b"  ("(1[_])")
    1.24  
    1.25 -text {* The main point of this solution is to use names everywhere (be they bound, 
    1.26 +text \<open>The main point of this solution is to use names everywhere (be they bound, 
    1.27    binding or free). In System \FSUB{} there are two kinds of names corresponding to 
    1.28    type-variables and to term-variables. These two kinds of names are represented in 
    1.29 -  the nominal datatype package as atom-types @{text "tyvrs"} and @{text "vrs"}: *}
    1.30 +  the nominal datatype package as atom-types \<open>tyvrs\<close> and \<open>vrs\<close>:\<close>
    1.31  
    1.32  atom_decl tyvrs vrs
    1.33  
    1.34 -text{* There are numerous facts that come with this declaration: for example that 
    1.35 -  there are infinitely many elements in @{text "tyvrs"} and @{text "vrs"}. *}
    1.36 +text\<open>There are numerous facts that come with this declaration: for example that 
    1.37 +  there are infinitely many elements in \<open>tyvrs\<close> and \<open>vrs\<close>.\<close>
    1.38  
    1.39 -text{* The constructors for types and terms in System \FSUB{} contain abstractions 
    1.40 +text\<open>The constructors for types and terms in System \FSUB{} contain abstractions 
    1.41    over type-variables and term-variables. The nominal datatype package uses 
    1.42 -  @{text "\<guillemotleft>\<dots>\<guillemotright>\<dots>"} to indicate where abstractions occur. *}
    1.43 +  \<open>\<guillemotleft>\<dots>\<guillemotright>\<dots>\<close> to indicate where abstractions occur.\<close>
    1.44  
    1.45  nominal_datatype ty = 
    1.46      Tvar   "tyvrs"
    1.47 @@ -46,10 +46,10 @@
    1.48    | App   "trm" "trm" (infixl "\<cdot>" 200)
    1.49    | TApp  "trm" "ty"  (infixl "\<cdot>\<^sub>\<tau>" 200)
    1.50  
    1.51 -text {* To be polite to the eye, some more familiar notation is introduced. 
    1.52 +text \<open>To be polite to the eye, some more familiar notation is introduced. 
    1.53    Because of the change in the order of arguments, one needs to use 
    1.54    translation rules, instead of syntax annotations at the term-constructors
    1.55 -  as given above for @{term "Arrow"}. *}
    1.56 +  as given above for @{term "Arrow"}.\<close>
    1.57  
    1.58  abbreviation
    1.59    Forall_syn :: "tyvrs \<Rightarrow> ty \<Rightarrow> ty \<Rightarrow> ty"  ("(3\<forall>_<:_./ _)" [0, 0, 10] 10) 
    1.60 @@ -66,19 +66,19 @@
    1.61  where
    1.62    "\<lambda>X<:T. t \<equiv> trm.TAbs X t T"
    1.63  
    1.64 -text {* Again there are numerous facts that are proved automatically for @{typ "ty"} 
    1.65 -  and @{typ "trm"}: for example that the set of free variables, i.e.~the @{text "support"}, 
    1.66 +text \<open>Again there are numerous facts that are proved automatically for @{typ "ty"} 
    1.67 +  and @{typ "trm"}: for example that the set of free variables, i.e.~the \<open>support\<close>, 
    1.68    is finite. However note that nominal-datatype declarations do \emph{not} define 
    1.69    ``classical" constructor-based datatypes, but rather define $\alpha$-equivalence 
    1.70    classes---we can for example show that $\alpha$-equivalent @{typ "ty"}s 
    1.71 -  and @{typ "trm"}s are equal: *}
    1.72 +  and @{typ "trm"}s are equal:\<close>
    1.73  
    1.74  lemma alpha_illustration:
    1.75    shows "(\<forall>X<:T. Tvar X) = (\<forall>Y<:T. Tvar Y)"
    1.76    and   "(\<lambda>x:T. Var x) = (\<lambda>y:T. Var y)"
    1.77    by (simp_all add: ty.inject trm.inject alpha calc_atm fresh_atm)
    1.78  
    1.79 -section {* SubTyping Contexts *}
    1.80 +section \<open>SubTyping Contexts\<close>
    1.81  
    1.82  nominal_datatype binding = 
    1.83      VarB vrs ty 
    1.84 @@ -86,12 +86,12 @@
    1.85  
    1.86  type_synonym env = "binding list"
    1.87  
    1.88 -text {* Typing contexts are represented as lists that ``grow" on the left; we
    1.89 +text \<open>Typing contexts are represented as lists that ``grow" on the left; we
    1.90    thereby deviating from the convention in the POPLmark-paper. The lists contain
    1.91 -  pairs of type-variables and types (this is sufficient for Part 1A). *}
    1.92 +  pairs of type-variables and types (this is sufficient for Part 1A).\<close>
    1.93  
    1.94 -text {* In order to state validity-conditions for typing-contexts, the notion of
    1.95 -  a @{text "dom"} of a typing-context is handy. *}
    1.96 +text \<open>In order to state validity-conditions for typing-contexts, the notion of
    1.97 +  a \<open>dom\<close> of a typing-context is handy.\<close>
    1.98  
    1.99  nominal_primrec
   1.100    "tyvrs_of" :: "binding \<Rightarrow> tyvrs set"
   1.101 @@ -218,11 +218,11 @@
   1.102  apply(auto simp add: fresh_prod fresh_list_cons tyvrs_fresh) 
   1.103  done
   1.104  
   1.105 -text {* Not all lists of type @{typ "env"} are well-formed. One condition
   1.106 +text \<open>Not all lists of type @{typ "env"} are well-formed. One condition
   1.107    requires that in @{term "TVarB X S#\<Gamma>"} all free variables of @{term "S"} must be 
   1.108 -  in the @{term "ty_dom"} of @{term "\<Gamma>"}, that is @{term "S"} must be @{text "closed"} 
   1.109 +  in the @{term "ty_dom"} of @{term "\<Gamma>"}, that is @{term "S"} must be \<open>closed\<close> 
   1.110    in @{term "\<Gamma>"}. The set of free variables of @{term "S"} is the 
   1.111 -  @{text "support"} of @{term "S"}. *}
   1.112 +  \<open>support\<close> of @{term "S"}.\<close>
   1.113  
   1.114  definition "closed_in" :: "ty \<Rightarrow> env \<Rightarrow> bool" ("_ closed'_in _" [100,100] 100) where
   1.115    "S closed_in \<Gamma> \<equiv> (supp S)\<subseteq>(ty_dom \<Gamma>)"
   1.116 @@ -284,7 +284,7 @@
   1.117  lemma closed_in_fresh: "(X::tyvrs) \<sharp> ty_dom \<Gamma> \<Longrightarrow> T closed_in \<Gamma> \<Longrightarrow> X \<sharp> T"
   1.118    by (auto simp add: closed_in_def fresh_def ty_dom_supp)
   1.119  
   1.120 -text {* Now validity of a context is a straightforward inductive definition. *}
   1.121 +text \<open>Now validity of a context is a straightforward inductive definition.\<close>
   1.122    
   1.123  inductive
   1.124    valid_rel :: "env \<Rightarrow> bool" ("\<turnstile> _ ok" [100] 100)
   1.125 @@ -332,7 +332,7 @@
   1.126         (auto elim: validE intro!: valid_cons simp add: doms_append closed_in_def)
   1.127  qed
   1.128  
   1.129 -text {* Well-formed contexts have a unique type-binding for a type-variable. *} 
   1.130 +text \<open>Well-formed contexts have a unique type-binding for a type-variable.\<close> 
   1.131  
   1.132  lemma uniqueness_of_ctxt:
   1.133    fixes \<Gamma>::"env"
   1.134 @@ -383,7 +383,7 @@
   1.135    ultimately show "T=S" by (auto simp add: binding.inject)
   1.136  qed (auto)
   1.137  
   1.138 -section {* Size and Capture-Avoiding Substitution for Types *}
   1.139 +section \<open>Size and Capture-Avoiding Substitution for Types\<close>
   1.140  
   1.141  nominal_primrec
   1.142    size_ty :: "ty \<Rightarrow> nat"
   1.143 @@ -590,14 +590,14 @@
   1.144    by (nominal_induct t avoiding: X Y U rule: trm.strong_induct)
   1.145      (simp_all add: fresh_atm calc_atm abs_fresh fresh_aux type_subst_rename)
   1.146  
   1.147 -section {* Subtyping-Relation *}
   1.148 +section \<open>Subtyping-Relation\<close>
   1.149  
   1.150 -text {* The definition for the subtyping-relation follows quite closely what is written 
   1.151 +text \<open>The definition for the subtyping-relation follows quite closely what is written 
   1.152    in the POPLmark-paper, except for the premises dealing with well-formed contexts and 
   1.153 -  the freshness constraint @{term "X\<sharp>\<Gamma>"} in the @{text "S_Forall"}-rule. (The freshness
   1.154 +  the freshness constraint @{term "X\<sharp>\<Gamma>"} in the \<open>S_Forall\<close>-rule. (The freshness
   1.155    constraint is specific to the \emph{nominal approach}. Note, however, that the constraint
   1.156    does \emph{not} make the subtyping-relation ``partial"\ldots because we work over
   1.157 -  $\alpha$-equivalence classes.) *}
   1.158 +  $\alpha$-equivalence classes.)\<close>
   1.159  
   1.160  inductive 
   1.161    subtype_of :: "env \<Rightarrow> ty \<Rightarrow> ty \<Rightarrow> bool"   ("_\<turnstile>_<:_" [100,100,100] 100)
   1.162 @@ -670,7 +670,7 @@
   1.163    apply (force simp add: closed_in_fresh dest: subtype_implies_closed subtype_implies_ok)+
   1.164    done
   1.165  
   1.166 -section {* Reflexivity of Subtyping *}
   1.167 +section \<open>Reflexivity of Subtyping\<close>
   1.168  
   1.169  lemma subtype_reflexivity:
   1.170    assumes a: "\<turnstile> \<Gamma> ok"
   1.171 @@ -702,18 +702,18 @@
   1.172  using a b
   1.173  apply(nominal_induct T avoiding: \<Gamma> rule: ty.strong_induct)
   1.174  apply(auto simp add: ty.supp abs_supp supp_atm closed_in_def)
   1.175 -  --{* Too bad that this instantiation cannot be found automatically by
   1.176 +  \<comment>\<open>Too bad that this instantiation cannot be found automatically by
   1.177    \isakeyword{auto}; \isakeyword{blast} would find it if we had not used 
   1.178 -  an explicit definition for @{text "closed_in_def"}. *}
   1.179 +  an explicit definition for \<open>closed_in_def\<close>.\<close>
   1.180  apply(drule_tac x="(TVarB tyvrs ty2)#\<Gamma>" in meta_spec)
   1.181  apply(force dest: fresh_dom simp add: closed_in_def)
   1.182  done
   1.183  
   1.184 -section {* Weakening *}
   1.185 +section \<open>Weakening\<close>
   1.186  
   1.187 -text {* In order to prove weakening we introduce the notion of a type-context extending 
   1.188 +text \<open>In order to prove weakening we introduce the notion of a type-context extending 
   1.189    another. This generalization seems to make the proof for weakening to be
   1.190 -  smoother than if we had strictly adhered to the version in the POPLmark-paper. *}
   1.191 +  smoother than if we had strictly adhered to the version in the POPLmark-paper.\<close>
   1.192  
   1.193  definition extends :: "env \<Rightarrow> env \<Rightarrow> bool" ("_ extends _" [100,100] 100) where
   1.194    "\<Delta> extends \<Gamma> \<equiv> \<forall>X Q. (TVarB X Q)\<in>set \<Gamma> \<longrightarrow> (TVarB X Q)\<in>set \<Delta>"
   1.195 @@ -794,7 +794,7 @@
   1.196    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)
   1.197  qed
   1.198  
   1.199 -text {* In fact all ``non-binding" cases can be solved automatically: *}
   1.200 +text \<open>In fact all ``non-binding" cases can be solved automatically:\<close>
   1.201  
   1.202  lemma weakening_more_automated:
   1.203    assumes a: "\<Gamma> \<turnstile> S <: T"
   1.204 @@ -822,9 +822,9 @@
   1.205    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)
   1.206  qed (blast intro: extends_closed extends_memb dest: extends_ty_dom)+
   1.207  
   1.208 -section {* Transitivity and Narrowing *}
   1.209 +section \<open>Transitivity and Narrowing\<close>
   1.210  
   1.211 -text {* Some inversion lemmas that are needed in the transitivity and narrowing proof.*}
   1.212 +text \<open>Some inversion lemmas that are needed in the transitivity and narrowing proof.\<close>
   1.213  
   1.214  declare ty.inject [simp add]
   1.215  
   1.216 @@ -840,14 +840,14 @@
   1.217  apply(auto simp add: abs_fresh ty.inject alpha)
   1.218  done
   1.219  
   1.220 -text {* Next we prove the transitivity and narrowing for the subtyping-relation. 
   1.221 +text \<open>Next we prove the transitivity and narrowing for the subtyping-relation. 
   1.222  The POPLmark-paper says the following:
   1.223  
   1.224  \begin{quote}
   1.225  \begin{lemma}[Transitivity and Narrowing] \
   1.226  \begin{enumerate}
   1.227  \item If @{term "\<Gamma> \<turnstile> S<:Q"} and @{term "\<Gamma> \<turnstile> Q<:T"}, then @{term "\<Gamma> \<turnstile> S<:T"}.
   1.228 -\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"}.
   1.229 +\item If \<open>\<Gamma>,X<:Q,\<Delta> \<turnstile> M<:N\<close> and @{term "\<Gamma> \<turnstile> P<:Q"} then \<open>\<Gamma>,X<:P,\<Delta> \<turnstile> M<:N\<close>.
   1.230  \end{enumerate}
   1.231  \end{lemma}
   1.232  
   1.233 @@ -858,7 +858,7 @@
   1.234  \end{quote}
   1.235  
   1.236  For the induction on the size of @{term "Q"}, we use the induction-rule 
   1.237 -@{text "measure_induct_rule"}:
   1.238 +\<open>measure_induct_rule\<close>:
   1.239  
   1.240  \begin{center}
   1.241  @{thm measure_induct_rule[of "size_ty",no_vars]}
   1.242 @@ -867,7 +867,7 @@
   1.243  That means in order to show a property @{term "P a"} for all @{term "a"}, 
   1.244  the induct-rule requires to prove that for all @{term x} @{term "P x"} holds using the 
   1.245  assumption that for all @{term y} whose size is strictly smaller than 
   1.246 -that of @{term x} the property @{term "P y"} holds. *}
   1.247 +that of @{term x} the property @{term "P y"} holds.\<close>
   1.248  
   1.249  lemma 
   1.250    shows subtype_transitivity: "\<Gamma>\<turnstile>S<:Q \<Longrightarrow> \<Gamma>\<turnstile>Q<:T \<Longrightarrow> \<Gamma>\<turnstile>S<:T" 
   1.251 @@ -886,7 +886,7 @@
   1.252        case (SA_Top \<Gamma> S) 
   1.253        then have rh_drv: "\<Gamma> \<turnstile> Top <: T" by simp
   1.254        then have T_inst: "T = Top" by (auto elim: S_TopE)
   1.255 -      from `\<turnstile> \<Gamma> ok` and `S closed_in \<Gamma>`
   1.256 +      from \<open>\<turnstile> \<Gamma> ok\<close> and \<open>S closed_in \<Gamma>\<close>
   1.257        have "\<Gamma> \<turnstile> S <: Top" by auto
   1.258        then show "\<Gamma> \<turnstile> S <: T" using T_inst by simp 
   1.259      next
   1.260 @@ -900,7 +900,7 @@
   1.261      next
   1.262        case (SA_arrow \<Gamma> Q\<^sub>1 S\<^sub>1 S\<^sub>2 Q\<^sub>2) 
   1.263        then have rh_drv: "\<Gamma> \<turnstile> Q\<^sub>1 \<rightarrow> Q\<^sub>2 <: T" by simp
   1.264 -      from `Q\<^sub>1 \<rightarrow> Q\<^sub>2 = Q` 
   1.265 +      from \<open>Q\<^sub>1 \<rightarrow> Q\<^sub>2 = Q\<close> 
   1.266        have Q\<^sub>12_less: "size_ty Q\<^sub>1 < size_ty Q" "size_ty Q\<^sub>2 < size_ty Q" by auto
   1.267        have lh_drv_prm\<^sub>1: "\<Gamma> \<turnstile> Q\<^sub>1 <: S\<^sub>1" by fact
   1.268        have lh_drv_prm\<^sub>2: "\<Gamma> \<turnstile> S\<^sub>2 <: Q\<^sub>2" by fact      
   1.269 @@ -969,23 +969,23 @@
   1.270      qed
   1.271    } note transitivity_lemma = this  
   1.272  
   1.273 -  { --{* The transitivity proof is now by the auxiliary lemma. *}
   1.274 +  { \<comment>\<open>The transitivity proof is now by the auxiliary lemma.\<close>
   1.275      case 1 
   1.276 -    from `\<Gamma> \<turnstile> S <: Q` and `\<Gamma> \<turnstile> Q <: T`
   1.277 +    from \<open>\<Gamma> \<turnstile> S <: Q\<close> and \<open>\<Gamma> \<turnstile> Q <: T\<close>
   1.278      show "\<Gamma> \<turnstile> S <: T" by (rule transitivity_lemma) 
   1.279    next 
   1.280      case 2
   1.281 -    from `(\<Delta>@[(TVarB X Q)]@\<Gamma>) \<turnstile> M <: N` 
   1.282 -      and `\<Gamma> \<turnstile> P<:Q` 
   1.283 +    from \<open>(\<Delta>@[(TVarB X Q)]@\<Gamma>) \<turnstile> M <: N\<close> 
   1.284 +      and \<open>\<Gamma> \<turnstile> P<:Q\<close> 
   1.285      show "(\<Delta>@[(TVarB X P)]@\<Gamma>) \<turnstile> M <: N" 
   1.286      proof (induct "\<Delta>@[(TVarB X Q)]@\<Gamma>" M N arbitrary: \<Gamma> X \<Delta> rule: subtype_of.induct) 
   1.287        case (SA_Top S \<Gamma> X \<Delta>)
   1.288 -      from `\<Gamma> \<turnstile> P <: Q`
   1.289 +      from \<open>\<Gamma> \<turnstile> P <: Q\<close>
   1.290        have "P closed_in \<Gamma>" by (simp add: subtype_implies_closed)
   1.291 -      with `\<turnstile> (\<Delta>@[(TVarB X Q)]@\<Gamma>) ok` have "\<turnstile> (\<Delta>@[(TVarB X P)]@\<Gamma>) ok"
   1.292 +      with \<open>\<turnstile> (\<Delta>@[(TVarB X Q)]@\<Gamma>) ok\<close> have "\<turnstile> (\<Delta>@[(TVarB X P)]@\<Gamma>) ok"
   1.293          by (simp add: replace_type)
   1.294        moreover
   1.295 -      from `S closed_in (\<Delta>@[(TVarB X Q)]@\<Gamma>)` have "S closed_in (\<Delta>@[(TVarB X P)]@\<Gamma>)" 
   1.296 +      from \<open>S closed_in (\<Delta>@[(TVarB X Q)]@\<Gamma>)\<close> have "S closed_in (\<Delta>@[(TVarB X P)]@\<Gamma>)" 
   1.297          by (simp add: closed_in_def doms_append)
   1.298        ultimately show "(\<Delta>@[(TVarB X P)]@\<Gamma>) \<turnstile> S <: Top" by (simp add: subtype_of.SA_Top)
   1.299      next
   1.300 @@ -1016,12 +1016,12 @@
   1.301        qed
   1.302      next
   1.303        case (SA_refl_TVar Y \<Gamma> X \<Delta>)
   1.304 -      from `\<Gamma> \<turnstile> P <: Q`
   1.305 +      from \<open>\<Gamma> \<turnstile> P <: Q\<close>
   1.306        have "P closed_in \<Gamma>" by (simp add: subtype_implies_closed)
   1.307 -      with `\<turnstile> (\<Delta>@[(TVarB X Q)]@\<Gamma>) ok` have "\<turnstile> (\<Delta>@[(TVarB X P)]@\<Gamma>) ok"
   1.308 +      with \<open>\<turnstile> (\<Delta>@[(TVarB X Q)]@\<Gamma>) ok\<close> have "\<turnstile> (\<Delta>@[(TVarB X P)]@\<Gamma>) ok"
   1.309          by (simp add: replace_type)
   1.310        moreover
   1.311 -      from `Y \<in> ty_dom (\<Delta>@[(TVarB X Q)]@\<Gamma>)` have "Y \<in> ty_dom (\<Delta>@[(TVarB X P)]@\<Gamma>)"
   1.312 +      from \<open>Y \<in> ty_dom (\<Delta>@[(TVarB X Q)]@\<Gamma>)\<close> have "Y \<in> ty_dom (\<Delta>@[(TVarB X P)]@\<Gamma>)"
   1.313          by (simp add: doms_append)
   1.314        ultimately show "(\<Delta>@[(TVarB X P)]@\<Gamma>) \<turnstile> Tvar Y <: Tvar Y" by (simp add: subtype_of.SA_refl_TVar)
   1.315      next
   1.316 @@ -1037,7 +1037,7 @@
   1.317    } 
   1.318  qed
   1.319  
   1.320 -section {* Typing *}
   1.321 +section \<open>Typing\<close>
   1.322  
   1.323  inductive
   1.324    typing :: "env \<Rightarrow> trm \<Rightarrow> ty \<Rightarrow> bool" ("_ \<turnstile> _ : _" [60,60,60] 60) 
   1.325 @@ -1116,22 +1116,22 @@
   1.326  using assms
   1.327  proof induct
   1.328    case (T_Var x T \<Gamma>)
   1.329 -  from `\<turnstile> \<Gamma> ok` and `VarB x T \<in> set \<Gamma>`
   1.330 +  from \<open>\<turnstile> \<Gamma> ok\<close> and \<open>VarB x T \<in> set \<Gamma>\<close>
   1.331    show ?case by (rule ok_imp_VarB_closed_in)
   1.332  next
   1.333    case (T_App \<Gamma> t\<^sub>1 T\<^sub>1 T\<^sub>2 t\<^sub>2)
   1.334    then show ?case by (auto simp add: ty.supp closed_in_def)
   1.335  next
   1.336    case (T_Abs x T\<^sub>1 \<Gamma> t\<^sub>2 T\<^sub>2)
   1.337 -  from `VarB x T\<^sub>1 # \<Gamma> \<turnstile> t\<^sub>2 : T\<^sub>2`
   1.338 +  from \<open>VarB x T\<^sub>1 # \<Gamma> \<turnstile> t\<^sub>2 : T\<^sub>2\<close>
   1.339    have "T\<^sub>1 closed_in \<Gamma>" by (auto dest: typing_ok)
   1.340    with T_Abs show ?case by (auto simp add: ty.supp closed_in_def)
   1.341  next
   1.342    case (T_Sub \<Gamma> t S T)
   1.343 -  from `\<Gamma> \<turnstile> S <: T` show ?case by (simp add: subtype_implies_closed)
   1.344 +  from \<open>\<Gamma> \<turnstile> S <: T\<close> show ?case by (simp add: subtype_implies_closed)
   1.345  next
   1.346    case (T_TAbs X T\<^sub>1 \<Gamma> t\<^sub>2 T\<^sub>2)
   1.347 -  from `TVarB X T\<^sub>1 # \<Gamma> \<turnstile> t\<^sub>2 : T\<^sub>2`
   1.348 +  from \<open>TVarB X T\<^sub>1 # \<Gamma> \<turnstile> t\<^sub>2 : T\<^sub>2\<close>
   1.349    have "T\<^sub>1 closed_in \<Gamma>" by (auto dest: typing_ok)
   1.350    with T_TAbs show ?case by (auto simp add: ty.supp closed_in_def abs_supp)
   1.351  next
   1.352 @@ -1144,7 +1144,7 @@
   1.353  qed
   1.354  
   1.355  
   1.356 -subsection {* Evaluation *}
   1.357 +subsection \<open>Evaluation\<close>
   1.358  
   1.359  inductive
   1.360    val :: "trm \<Rightarrow> bool"
   1.361 @@ -1302,7 +1302,7 @@
   1.362    qed
   1.363  qed
   1.364    
   1.365 -text {* A.5(6) *}
   1.366 +text \<open>A.5(6)\<close>
   1.367  
   1.368  lemma type_weaken:
   1.369    assumes "(\<Delta>@\<Gamma>) \<turnstile> t : T"
   1.370 @@ -1337,15 +1337,15 @@
   1.371    then show ?case by (rule typing.T_Abs)
   1.372  next
   1.373    case (T_Sub t S T \<Delta> \<Gamma>)
   1.374 -  from refl and `\<turnstile> (\<Delta> @ B # \<Gamma>) ok`
   1.375 +  from refl and \<open>\<turnstile> (\<Delta> @ B # \<Gamma>) ok\<close>
   1.376    have "\<Delta> @ B # \<Gamma> \<turnstile> t : S" by (rule T_Sub)
   1.377 -  moreover from  `(\<Delta> @ \<Gamma>)\<turnstile>S<:T` and `\<turnstile> (\<Delta> @ B # \<Gamma>) ok`
   1.378 +  moreover from  \<open>(\<Delta> @ \<Gamma>)\<turnstile>S<:T\<close> and \<open>\<turnstile> (\<Delta> @ B # \<Gamma>) ok\<close>
   1.379    have "(\<Delta> @ B # \<Gamma>)\<turnstile>S<:T"
   1.380      by (rule weakening) (simp add: extends_def T_Sub)
   1.381    ultimately show ?case by (rule typing.T_Sub)
   1.382  next
   1.383    case (T_TAbs X T\<^sub>1 t\<^sub>2 T\<^sub>2 \<Delta> \<Gamma>)
   1.384 -  from `TVarB X T\<^sub>1 # \<Delta> @ \<Gamma> \<turnstile> t\<^sub>2 : T\<^sub>2`
   1.385 +  from \<open>TVarB X T\<^sub>1 # \<Delta> @ \<Gamma> \<turnstile> t\<^sub>2 : T\<^sub>2\<close>
   1.386    have closed: "T\<^sub>1 closed_in (\<Delta> @ \<Gamma>)"
   1.387      by (auto dest: typing_ok)
   1.388    have "\<turnstile> (TVarB X T\<^sub>1 # \<Delta> @ B # \<Gamma>) ok"
   1.389 @@ -1367,7 +1367,7 @@
   1.390    case (T_TApp X t\<^sub>1 T2 T11 T12 \<Delta> \<Gamma>)
   1.391    have "\<Delta> @ B # \<Gamma> \<turnstile> t\<^sub>1 : (\<forall>X<:T11. T12)"
   1.392      by (rule T_TApp refl)+
   1.393 -  moreover from `(\<Delta> @ \<Gamma>)\<turnstile>T2<:T11` and `\<turnstile> (\<Delta> @ B # \<Gamma>) ok`
   1.394 +  moreover from \<open>(\<Delta> @ \<Gamma>)\<turnstile>T2<:T11\<close> and \<open>\<turnstile> (\<Delta> @ B # \<Gamma>) ok\<close>
   1.395    have "(\<Delta> @ B # \<Gamma>)\<turnstile>T2<:T11"
   1.396      by (rule weakening) (simp add: extends_def T_TApp)
   1.397    ultimately show ?case by (rule better_T_TApp)
   1.398 @@ -1382,7 +1382,7 @@
   1.399    apply simp_all
   1.400    done
   1.401  
   1.402 -text {* A.6 *}
   1.403 +text \<open>A.6\<close>
   1.404  
   1.405  lemma strengthening:
   1.406    assumes "(\<Gamma> @ VarB x Q # \<Delta>) \<turnstile> S <: T"
   1.407 @@ -1395,7 +1395,7 @@
   1.408    ultimately show ?case using subtype_of.SA_Top by auto
   1.409  next
   1.410    case (SA_refl_TVar X)
   1.411 -  from `\<turnstile> (\<Gamma> @ VarB x Q # \<Delta>) ok`
   1.412 +  from \<open>\<turnstile> (\<Gamma> @ VarB x Q # \<Delta>) ok\<close>
   1.413    have h1:"\<turnstile> (\<Gamma> @ \<Delta>) ok" by (auto dest: valid_cons')
   1.414    have "X \<in> ty_dom (\<Gamma> @ VarB x Q # \<Delta>)" using SA_refl_TVar by auto
   1.415    then have h2:"X \<in> ty_dom (\<Gamma> @ \<Delta>)" using ty_dom_vrs by auto
   1.416 @@ -1407,7 +1407,7 @@
   1.417    then show ?case using h1 h2 by auto
   1.418  qed (auto)
   1.419  
   1.420 -lemma narrow_type: -- {* A.7 *}
   1.421 +lemma narrow_type: \<comment> \<open>A.7\<close>
   1.422    assumes H: "\<Delta> @ (TVarB X Q) # \<Gamma> \<turnstile> t : T"
   1.423    shows "\<Gamma> \<turnstile> P <: Q \<Longrightarrow> \<Delta> @ (TVarB X P) # \<Gamma> \<turnstile> t : T"
   1.424    using H
   1.425 @@ -1433,18 +1433,18 @@
   1.426      case (T_TApp X' t1 T2 T11 T12 P D)
   1.427      then have "D @ TVarB X P # \<Gamma> \<turnstile> t1 : Forall X' T12 T11" by fastforce
   1.428      moreover have "(D @ [TVarB X Q] @ \<Gamma>) \<turnstile> T2<:T11" using T_TApp by auto
   1.429 -    then have "(D @ [TVarB X P] @ \<Gamma>) \<turnstile> T2<:T11" using `\<Gamma>\<turnstile>P<:Q`
   1.430 +    then have "(D @ [TVarB X P] @ \<Gamma>) \<turnstile> T2<:T11" using \<open>\<Gamma>\<turnstile>P<:Q\<close>
   1.431        by (rule subtype_narrow)
   1.432      moreover from T_TApp have "X' \<sharp> (D @ TVarB X P # \<Gamma>, t1, T2)"
   1.433        by (simp add: fresh_list_append fresh_list_cons fresh_prod)
   1.434      ultimately show ?case by auto
   1.435  qed
   1.436  
   1.437 -subsection {* Substitution lemmas *}
   1.438 +subsection \<open>Substitution lemmas\<close>
   1.439  
   1.440 -subsubsection {* Substition Preserves Typing *}
   1.441 +subsubsection \<open>Substition Preserves Typing\<close>
   1.442  
   1.443 -theorem subst_type: -- {* A.8 *}
   1.444 +theorem subst_type: \<comment> \<open>A.8\<close>
   1.445    assumes H: "(\<Delta> @ (VarB x U) # \<Gamma>) \<turnstile> t : T"
   1.446    shows "\<Gamma> \<turnstile> u : U \<Longrightarrow> \<Delta> @ \<Gamma> \<turnstile> t[x \<mapsto> u] : T" using H
   1.447   proof (nominal_induct "\<Delta> @ (VarB x U) # \<Gamma>" t T avoiding: x u arbitrary: \<Delta> rule: typing.strong_induct)
   1.448 @@ -1473,9 +1473,9 @@
   1.449     ultimately show ?case by auto 
   1.450   next
   1.451     case (T_TAbs X T1 t2 T2 x u D)
   1.452 -   from `TVarB X T1 # D @ VarB x U # \<Gamma> \<turnstile> t2 : T2` have "X \<sharp> T1"
   1.453 +   from \<open>TVarB X T1 # D @ VarB x U # \<Gamma> \<turnstile> t2 : T2\<close> have "X \<sharp> T1"
   1.454       by (auto simp add: valid_ty_dom_fresh dest: typing_ok intro!: closed_in_fresh)
   1.455 -   with `X \<sharp> u` and T_TAbs show ?case by fastforce
   1.456 +   with \<open>X \<sharp> u\<close> and T_TAbs show ?case by fastforce
   1.457   next
   1.458     case (T_TApp X t1 T2 T11 T12 x u D)
   1.459     then have "(D@\<Gamma>) \<turnstile>T2<:T11" using T_TApp by (auto dest: strengthening)
   1.460 @@ -1483,9 +1483,9 @@
   1.461       by (force simp add: fresh_prod fresh_list_append fresh_list_cons subst_trm_fresh_tyvar)
   1.462  qed
   1.463  
   1.464 -subsubsection {* Type Substitution Preserves Subtyping *}
   1.465 +subsubsection \<open>Type Substitution Preserves Subtyping\<close>
   1.466  
   1.467 -lemma substT_subtype: -- {* A.10 *}
   1.468 +lemma substT_subtype: \<comment> \<open>A.10\<close>
   1.469    assumes H: "(\<Delta> @ ((TVarB X Q) # \<Gamma>)) \<turnstile> S <: T"
   1.470    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>" 
   1.471    using H
   1.472 @@ -1508,11 +1508,11 @@
   1.473    proof (cases "X = Y")
   1.474      assume eq: "X = Y"
   1.475      from eq and SA_trans_TVar have "TVarB Y Q \<in> set (D @ TVarB X Q # \<Gamma>)" by simp
   1.476 -    with G_ok have QS: "Q = S" using `TVarB Y S \<in> set (D @ TVarB X Q # \<Gamma>)`
   1.477 +    with G_ok have QS: "Q = S" using \<open>TVarB Y S \<in> set (D @ TVarB X Q # \<Gamma>)\<close>
   1.478        by (rule uniqueness_of_ctxt)
   1.479      from X_\<Gamma>_ok have "X \<sharp> ty_dom \<Gamma>" and "Q closed_in \<Gamma>" by auto
   1.480      then have XQ: "X \<sharp> Q" by (rule closed_in_fresh)
   1.481 -    note `\<Gamma>\<turnstile>P<:Q`
   1.482 +    note \<open>\<Gamma>\<turnstile>P<:Q\<close>
   1.483      moreover from ST have "\<turnstile> (D[X \<mapsto> P]\<^sub>e @ \<Gamma>) ok" by (rule subtype_implies_ok)
   1.484      moreover have "(D[X \<mapsto> P]\<^sub>e @ \<Gamma>) extends \<Gamma>" by (simp add: extends_def)
   1.485      ultimately have "(D[X \<mapsto> P]\<^sub>e @ \<Gamma>) \<turnstile> P<:Q" by (rule weakening)
   1.486 @@ -1547,7 +1547,7 @@
   1.487    qed
   1.488  next
   1.489    case (SA_refl_TVar Y X P D)
   1.490 -  note `\<turnstile> (D @ TVarB X Q # \<Gamma>) ok`
   1.491 +  note \<open>\<turnstile> (D @ TVarB X Q # \<Gamma>) ok\<close>
   1.492    moreover from SA_refl_TVar have closed: "P closed_in \<Gamma>"
   1.493      by (auto dest: subtype_implies_closed)
   1.494    ultimately have ok: "\<turnstile> (D[X \<mapsto> P]\<^sub>e @ \<Gamma>) ok" using valid_subst by auto
   1.495 @@ -1582,9 +1582,9 @@
   1.496    with SA_all and S1 show ?case by force
   1.497  qed
   1.498  
   1.499 -subsubsection {* Type Substitution Preserves Typing *}
   1.500 +subsubsection \<open>Type Substitution Preserves Typing\<close>
   1.501  
   1.502 -theorem substT_type: -- {* A.11 *}
   1.503 +theorem substT_type: \<comment> \<open>A.11\<close>
   1.504    assumes H: "(D @ TVarB X Q # G) \<turnstile> t : T"
   1.505    shows "G \<turnstile> P <: Q \<Longrightarrow>
   1.506      (D[X \<mapsto> P]\<^sub>e @ G) \<turnstile> t[X \<mapsto>\<^sub>\<tau> P] : T[X \<mapsto> P]\<^sub>\<tau>" using H
   1.507 @@ -1592,9 +1592,9 @@
   1.508    case (T_Var x T X P D')
   1.509    have "G\<turnstile>P<:Q" by fact
   1.510    then have "P closed_in G" using subtype_implies_closed by auto
   1.511 -  moreover note `\<turnstile> (D' @ TVarB X Q # G) ok`
   1.512 +  moreover note \<open>\<turnstile> (D' @ TVarB X Q # G) ok\<close>
   1.513    ultimately have "\<turnstile> (D'[X \<mapsto> P]\<^sub>e @ G) ok" using valid_subst by auto
   1.514 -  moreover note `VarB x T \<in> set (D' @ TVarB X Q # G)`
   1.515 +  moreover note \<open>VarB x T \<in> set (D' @ TVarB X Q # G)\<close>
   1.516    then have "VarB x T \<in> set D' \<or> VarB x T \<in> set G" by simp
   1.517    then have "(VarB x (T[X \<mapsto> P]\<^sub>\<tau>)) \<in> set (D'[X \<mapsto> P]\<^sub>e @ G)"
   1.518    proof
   1.519 @@ -1648,7 +1648,7 @@
   1.520        intro: substT_subtype)
   1.521  qed
   1.522  
   1.523 -lemma Abs_type: -- {* A.13(1) *}
   1.524 +lemma Abs_type: \<comment> \<open>A.13(1)\<close>
   1.525    assumes H: "\<Gamma> \<turnstile> (\<lambda>x:S. s) : T"
   1.526    and H': "\<Gamma> \<turnstile> T <: U \<rightarrow> U'"
   1.527    and H'': "x \<sharp> \<Gamma>"
   1.528 @@ -1658,7 +1658,7 @@
   1.529    using H H' H''
   1.530  proof (nominal_induct \<Gamma> t \<equiv> "\<lambda>x:S. s" T avoiding: x arbitrary: U U' S s rule: typing.strong_induct)
   1.531    case (T_Abs y T\<^sub>1 \<Gamma> t\<^sub>2 T\<^sub>2)
   1.532 -  from `\<Gamma> \<turnstile> T\<^sub>1 \<rightarrow> T\<^sub>2 <: U \<rightarrow> U'`
   1.533 +  from \<open>\<Gamma> \<turnstile> T\<^sub>1 \<rightarrow> T\<^sub>2 <: U \<rightarrow> U'\<close>
   1.534    obtain ty1: "\<Gamma> \<turnstile> U <: S" and ty2: "\<Gamma> \<turnstile> T\<^sub>2 <: U'" using T_Abs
   1.535      by cases (simp_all add: ty.inject trm.inject alpha fresh_atm)
   1.536    from T_Abs have "VarB y S # \<Gamma> \<turnstile> [(y, x)] \<bullet> s : T\<^sub>2"
   1.537 @@ -1690,7 +1690,7 @@
   1.538    using H subtype_reflexivity_from_typing [OF H] H'
   1.539    by (rule Abs_type)
   1.540  
   1.541 -lemma TAbs_type: -- {* A.13(2) *}
   1.542 +lemma TAbs_type: \<comment> \<open>A.13(2)\<close>
   1.543    assumes H: "\<Gamma> \<turnstile> (\<lambda>X<:S. s) : T"
   1.544    and H': "\<Gamma> \<turnstile> T <: (\<forall>X<:U. U')"
   1.545    and fresh: "X \<sharp> \<Gamma>" "X \<sharp> S" "X \<sharp> U"
   1.546 @@ -1701,9 +1701,9 @@
   1.547    using H H' fresh
   1.548  proof (nominal_induct \<Gamma> t \<equiv> "\<lambda>X<:S. s" T avoiding: X U U' S arbitrary: s rule: typing.strong_induct)
   1.549    case (T_TAbs Y T\<^sub>1 \<Gamma> t\<^sub>2 T\<^sub>2)
   1.550 -  from `TVarB Y T\<^sub>1 # \<Gamma> \<turnstile> t\<^sub>2 : T\<^sub>2` have Y: "Y \<sharp> \<Gamma>"
   1.551 +  from \<open>TVarB Y T\<^sub>1 # \<Gamma> \<turnstile> t\<^sub>2 : T\<^sub>2\<close> have Y: "Y \<sharp> \<Gamma>"
   1.552      by (auto dest!: typing_ok simp add: valid_ty_dom_fresh)
   1.553 -  from `Y \<sharp> U'` and `Y \<sharp> X`
   1.554 +  from \<open>Y \<sharp> U'\<close> and \<open>Y \<sharp> X\<close>
   1.555    have "(\<forall>X<:U. U') = (\<forall>Y<:U. [(Y, X)] \<bullet> U')"
   1.556      by (simp add: ty.inject alpha' fresh_atm)
   1.557    with T_TAbs have "\<Gamma> \<turnstile> (\<forall>Y<:S. T\<^sub>2) <: (\<forall>Y<:U. [(Y, X)] \<bullet> U')" by (simp add: trm.inject)
   1.558 @@ -1714,13 +1714,13 @@
   1.559      by (simp add: trm.inject alpha fresh_atm)
   1.560    then have "[(Y, X)] \<bullet> (TVarB Y S # \<Gamma>) \<turnstile> [(Y, X)] \<bullet> [(Y, X)] \<bullet> s : [(Y, X)] \<bullet> T\<^sub>2"
   1.561      by (rule typing.eqvt)
   1.562 -  with `X \<sharp> \<Gamma>` `X \<sharp> S` Y `Y \<sharp> S` have "TVarB X S # \<Gamma> \<turnstile> s : [(Y, X)] \<bullet> T\<^sub>2"
   1.563 +  with \<open>X \<sharp> \<Gamma>\<close> \<open>X \<sharp> S\<close> Y \<open>Y \<sharp> S\<close> have "TVarB X S # \<Gamma> \<turnstile> s : [(Y, X)] \<bullet> T\<^sub>2"
   1.564      by perm_simp
   1.565    then have "TVarB X U # \<Gamma> \<turnstile> s : [(Y, X)] \<bullet> T\<^sub>2" using ty1
   1.566      by (rule narrow_type [of "[]", simplified])
   1.567    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')"
   1.568      by (rule subtype_of.eqvt)
   1.569 -  with `X \<sharp> \<Gamma>` `X \<sharp> U` Y `Y \<sharp> U` have "(TVarB X U # \<Gamma>) \<turnstile> ([(Y, X)] \<bullet> T\<^sub>2) <: U'"
   1.570 +  with \<open>X \<sharp> \<Gamma>\<close> \<open>X \<sharp> U\<close> Y \<open>Y \<sharp> U\<close> have "(TVarB X U # \<Gamma>) \<turnstile> ([(Y, X)] \<bullet> T\<^sub>2) <: U'"
   1.571      by perm_simp
   1.572    ultimately show ?case by (rule T_TAbs)
   1.573  next
   1.574 @@ -1738,7 +1738,7 @@
   1.575    using H subtype_reflexivity_from_typing [OF H] fresh
   1.576    by (rule TAbs_type)
   1.577  
   1.578 -theorem preservation: -- {* A.20 *}
   1.579 +theorem preservation: \<comment> \<open>A.20\<close>
   1.580    assumes H: "\<Gamma> \<turnstile> t : T"
   1.581    shows "t \<longmapsto> t' \<Longrightarrow> \<Gamma> \<turnstile> t' : T" using H
   1.582  proof (nominal_induct avoiding: t' rule: typing.strong_induct)
   1.583 @@ -1747,7 +1747,7 @@
   1.584      by (rule exists_fresh) (rule fin_supp)
   1.585    obtain X::tyvrs where "X \<sharp> (t\<^sub>1 \<cdot> t\<^sub>2, t')"
   1.586      by (rule exists_fresh) (rule fin_supp)
   1.587 -  with `t\<^sub>1 \<cdot> t\<^sub>2 \<longmapsto> t'` show ?case
   1.588 +  with \<open>t\<^sub>1 \<cdot> t\<^sub>2 \<longmapsto> t'\<close> show ?case
   1.589    proof (cases rule: eval.strong_cases [where x=x and X=X])
   1.590      case (E_Abs v\<^sub>2 T\<^sub>11' t\<^sub>12)
   1.591      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"
   1.592 @@ -1758,7 +1758,7 @@
   1.593        and t\<^sub>12: "(VarB x T\<^sub>11') # \<Gamma> \<turnstile> t\<^sub>12 : S'"
   1.594        and S': "\<Gamma> \<turnstile> S' <: T\<^sub>12"
   1.595        by (rule Abs_type') blast
   1.596 -    from `\<Gamma> \<turnstile> t\<^sub>2 : T\<^sub>11`
   1.597 +    from \<open>\<Gamma> \<turnstile> t\<^sub>2 : T\<^sub>11\<close>
   1.598      have "\<Gamma> \<turnstile> t\<^sub>2 : T\<^sub>11'" using T\<^sub>11 by (rule T_Sub)
   1.599      with t\<^sub>12 have "\<Gamma> \<turnstile> t\<^sub>12[x \<mapsto> t\<^sub>2] : S'" 
   1.600        by (rule subst_type [where \<Delta>="[]", simplified])
   1.601 @@ -1768,7 +1768,7 @@
   1.602      case (E_App1 t''' t'' u)
   1.603      hence "t\<^sub>1 \<longmapsto> t''" by (simp add:trm.inject) 
   1.604      hence "\<Gamma> \<turnstile> t'' : T\<^sub>11 \<rightarrow> T\<^sub>12" by (rule T_App)
   1.605 -    hence "\<Gamma> \<turnstile> t'' \<cdot> t\<^sub>2 : T\<^sub>12" using `\<Gamma> \<turnstile> t\<^sub>2 : T\<^sub>11`
   1.606 +    hence "\<Gamma> \<turnstile> t'' \<cdot> t\<^sub>2 : T\<^sub>12" using \<open>\<Gamma> \<turnstile> t\<^sub>2 : T\<^sub>11\<close>
   1.607        by (rule typing.T_App)
   1.608      with E_App1 show ?thesis by (simp add:trm.inject)
   1.609    next
   1.610 @@ -1783,27 +1783,27 @@
   1.611    case (T_TApp X \<Gamma> t\<^sub>1 T\<^sub>2  T\<^sub>11  T\<^sub>12 t')
   1.612    obtain x::vrs where "x \<sharp> (t\<^sub>1 \<cdot>\<^sub>\<tau> T\<^sub>2, t')"
   1.613      by (rule exists_fresh) (rule fin_supp)
   1.614 -  with `t\<^sub>1 \<cdot>\<^sub>\<tau> T\<^sub>2 \<longmapsto> t'`
   1.615 +  with \<open>t\<^sub>1 \<cdot>\<^sub>\<tau> T\<^sub>2 \<longmapsto> t'\<close>
   1.616    show ?case
   1.617    proof (cases rule: eval.strong_cases [where X=X and x=x])
   1.618      case (E_TAbs T\<^sub>11' T\<^sub>2' t\<^sub>12)
   1.619      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'"
   1.620        by (simp_all add: trm.inject)
   1.621 -    moreover from `\<Gamma>\<turnstile>T\<^sub>2<:T\<^sub>11` and `X \<sharp> \<Gamma>` have "X \<sharp> T\<^sub>11"
   1.622 +    moreover from \<open>\<Gamma>\<turnstile>T\<^sub>2<:T\<^sub>11\<close> and \<open>X \<sharp> \<Gamma>\<close> have "X \<sharp> T\<^sub>11"
   1.623        by (blast intro: closed_in_fresh fresh_dom dest: subtype_implies_closed)
   1.624      ultimately obtain S'
   1.625        where "TVarB X T\<^sub>11 # \<Gamma> \<turnstile> t\<^sub>12 : S'"
   1.626        and "(TVarB X T\<^sub>11 # \<Gamma>) \<turnstile> S' <: T\<^sub>12"
   1.627        by (rule TAbs_type') blast
   1.628      hence "TVarB X T\<^sub>11 # \<Gamma> \<turnstile> t\<^sub>12 : T\<^sub>12" by (rule T_Sub)
   1.629 -    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`
   1.630 +    hence "\<Gamma> \<turnstile> t\<^sub>12[X \<mapsto>\<^sub>\<tau> T\<^sub>2] : T\<^sub>12[X \<mapsto> T\<^sub>2]\<^sub>\<tau>" using \<open>\<Gamma> \<turnstile> T\<^sub>2 <: T\<^sub>11\<close>
   1.631        by (rule substT_type [where D="[]", simplified])
   1.632      with T_TApp and E_TAbs show ?thesis by (simp add: trm.inject)
   1.633    next
   1.634      case (E_TApp t''' t'' T)
   1.635      from E_TApp have "t\<^sub>1 \<longmapsto> t''" by (simp add: trm.inject)
   1.636      then have "\<Gamma> \<turnstile> t'' : (\<forall>X<:T\<^sub>11. T\<^sub>12)" by (rule T_TApp)
   1.637 -    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`
   1.638 +    then have "\<Gamma> \<turnstile> t'' \<cdot>\<^sub>\<tau> T\<^sub>2 : T\<^sub>12[X \<mapsto> T\<^sub>2]\<^sub>\<tau>" using \<open>\<Gamma> \<turnstile> T\<^sub>2 <: T\<^sub>11\<close>
   1.639        by (rule better_T_TApp)
   1.640      with E_TApp show ?thesis by (simp add: trm.inject)
   1.641    qed (simp_all add: fresh_prod)
   1.642 @@ -1815,24 +1815,24 @@
   1.643    ultimately show ?case by (rule typing.T_Sub)
   1.644  qed (auto)
   1.645  
   1.646 -lemma Fun_canonical: -- {* A.14(1) *}
   1.647 +lemma Fun_canonical: \<comment> \<open>A.14(1)\<close>
   1.648    assumes ty: "[] \<turnstile> v : T\<^sub>1 \<rightarrow> T\<^sub>2"
   1.649    shows "val v \<Longrightarrow> \<exists>x t S. v = (\<lambda>x:S. t)" using ty
   1.650  proof (induct "[]::env" v "T\<^sub>1 \<rightarrow> T\<^sub>2" arbitrary: T\<^sub>1 T\<^sub>2)
   1.651    case (T_Sub t S)
   1.652 -  from `[] \<turnstile> S <: T\<^sub>1 \<rightarrow> T\<^sub>2`
   1.653 +  from \<open>[] \<turnstile> S <: T\<^sub>1 \<rightarrow> T\<^sub>2\<close>
   1.654    obtain S\<^sub>1 S\<^sub>2 where S: "S = S\<^sub>1 \<rightarrow> S\<^sub>2" 
   1.655      by cases (auto simp add: T_Sub)
   1.656 -  then show ?case using `val t` by (rule T_Sub)
   1.657 +  then show ?case using \<open>val t\<close> by (rule T_Sub)
   1.658  qed (auto)
   1.659  
   1.660 -lemma TyAll_canonical: -- {* A.14(3) *}
   1.661 +lemma TyAll_canonical: \<comment> \<open>A.14(3)\<close>
   1.662    fixes X::tyvrs
   1.663    assumes ty: "[] \<turnstile> v : (\<forall>X<:T\<^sub>1. T\<^sub>2)"
   1.664    shows "val v \<Longrightarrow> \<exists>X t S. v = (\<lambda>X<:S. t)" using ty
   1.665  proof (induct "[]::env" v "\<forall>X<:T\<^sub>1. T\<^sub>2" arbitrary: X T\<^sub>1 T\<^sub>2)
   1.666    case (T_Sub t S)
   1.667 -  from `[] \<turnstile> S <: (\<forall>X<:T\<^sub>1. T\<^sub>2)`
   1.668 +  from \<open>[] \<turnstile> S <: (\<forall>X<:T\<^sub>1. T\<^sub>2)\<close>
   1.669    obtain X S\<^sub>1 S\<^sub>2 where S: "S = (\<forall>X<:S\<^sub>1. S\<^sub>2)"
   1.670      by cases (auto simp add: T_Sub)
   1.671    then show ?case using T_Sub by auto