--- a/Paper/Paper.thy	Thu Mar 18 19:39:01 2010 +0100
+++ b/Paper/Paper.thy	Thu Mar 18 22:06:28 2010 +0100
@@ -15,16 +15,16 @@
 section {* Introduction *}
 
 text {*
-  So far, Nominal Isabelle provided a mechanism to construct
-  automatically alpha-equated lambda terms sich as
+  So far, Nominal Isabelle provides a mechanism for constructing
+  automatically alpha-equated terms such as
 
   \begin{center}
   $t ::= x \mid t\;t \mid \lambda x. t$
   \end{center}
 
   \noindent
-  For such calculi, it derived automatically a convenient reasoning
-  infrastructure. With this it has been used to formalise an equivalence
+  For such terms it derives automatically a reasoning
+  infrastructure, which has been used in formalisations of an equivalence
   checking algorithm for LF \cite{UrbanCheneyBerghofer08}, Typed
   Scheme~\cite{TobinHochstadtFelleisen08}, several calculi for concurrency
   \cite{BengtsonParrow07,BengtsonParow09} and a strong normalisation result
@@ -32,9 +32,9 @@
   used by Pollack for formalisations in the locally-nameless approach to
   binding \cite{SatoPollack10}.
 
-  However, Nominal Isabelle has fared less well in a formalisation of
-  the algorithm W \cite{UrbanNipkow09} where types and type-schemes
-  are represented by
+  However, Nominal Isabelle fared less well in a formalisation of
+  the algorithm W \cite{UrbanNipkow09}, where types and type-schemes
+  are of the form
 
   \begin{center}
   \begin{tabular}{l}
@@ -43,108 +43,115 @@
   \end{center}
 
   \noindent
-  While it is possible to formalise the finite set of variables that are
-  abstracted in a type-scheme by iterating single abstractions, it leads to a very
-  clumsy formalisation. This need of iterating single binders for representing
-  multiple binders is also the reason why Nominal Isabelle and other theorem
-  provers have so far not fared very well with the more advanced tasks in the POPLmark
-  challenge, because also there one would like to abstract several variables 
+  and the quantification abstracts over a finite (possibly empty) set of type variables.
+  While it is possible to formalise such abstractions by iterating single bindings, 
+  it leads to a very clumsy formalisation of W. This need of iterating single binders 
+  for representing multiple binders is also the reason why Nominal Isabelle and other 
+  theorem provers have not fared extremely well with the more advanced tasks 
+  in the POPLmark challenge \cite{challenge05}, because also there one would be able 
+  to aviod clumsy reasoning if there were a mechanisms for abstracting several variables 
   at once.
 
-  There are interesting points to note with binders that abstract multiple 
-  variables. First in the case of type-schemes we do not like to make a distinction
-  about the order of the binders. So we would like to regard the following two
-  type-schemes as alpha-equivalent:
+  To see this, let us point out some interesting properties of binders abstracting multiple 
+  variables. First, in the case of type-schemes, we do not like to make a distinction
+  about the order of the bound variables. Therefore we would like to regard the following two
+  type-schemes as alpha-equivalent
 
   \begin{center}
   $\forall \{x, y\}. x \rightarrow y  \;\approx_\alpha\; \forall \{y, x\}. y \rightarrow x$ 
   \end{center}
 
   \noindent
-  but assuming $x$, $y$ and $z$ are distinct, the following two should be \emph{not} 
-  alpha-equivalent:
+  but  the following two should \emph{not} be alpha-equivalent
 
   \begin{center}
   $\forall \{x, y\}. x \rightarrow y  \;\not\approx_\alpha\; \forall \{z\}. z \rightarrow z$ 
   \end{center}
 
   \noindent
-  However we do like to regard type-schemes as alpha-equivalent, if they
-  differ only on \emph{vacuous} binders, such as
+  assuming that $x$, $y$ and $z$ are distinct. Moreover, we like to regard type-schemes as 
+  alpha-equivalent, if they differ only on \emph{vacuous} binders, such as
 
   \begin{center}
   $\forall \{x\}. x \rightarrow y  \;\approx_\alpha\; \forall \{x, z\}. x \rightarrow y$ 
   \end{center}
 
   \noindent
-  In this paper we will give a general abstraction mechanism and assciated notion of alpha-equivalence 
-  which can be used to represent type-schemes.  The difficulty in finding the notion of alpha-equivalence 
-  can be appreciated by considering that the definition given by Leroy in \cite{Leroy92} is incorrect 
-  (it omits a side-condition).
+  In this paper we will give a general abstraction mechanism and associated
+  notion of alpha-equivalence that can be used to faithfully represent
+  type-schemes in Nominal Isabelle.  The difficulty of finding the right notion 
+  for alpha-equivalence in this case can be appreciated by considering that the 
+  definition given by Leroy in \cite{Leroy92} is incorrect (it omits a side-condition).
+
+
 
   However, the notion of alpha-equivalence that is preserved by vacuous binders is not
-  alway wanted. For example in constructs like
+  alway wanted. For example in terms like
 
   \begin{center}
-  $\LET x = 3 \AND y = 2 \IN x \backslash y \END$
+  $\LET x = 3 \AND y = 2 \IN x\,\backslash\,y \END$
   \end{center}
 
   \noindent
-  we might not care in which order the associations $x = 3$ and $y = 2$ are
-  given, but it would be unusual to regard this term as alpha-equivalent with
+  we might not care in which order the assignments $x = 3$ and $y = 2$ are
+  given, but it would be unusual to regard the above term as alpha-equivalent 
+  with
 
   \begin{center}
-  $\LET x = 3 \AND y = 2 \AND z = loop \IN x \backslash y \END$
+  $\LET x = 3 \AND y = 2 \AND z = loop \IN x\,\backslash\,y \END$
   \end{center}
 
   \noindent
-  We will provide a separate abstraction mechanism for this case where the
-  order of binders does not matter, but the ``cardinality'' of the binders
-  has to be the same.
+  Therefore we will also provide a separate abstraction mechanism for cases 
+  in which the order of binders does not matter, but the ``cardinality'' of the 
+  binders has to be the same.
 
-  However, this is still not sufficient for covering language constructs frequently 
-  occuring in programming language research. For example in patters like
+  However, we found that this is still not sufficient for covering language 
+  constructs frequently occuring in programming language research. For example 
+  in $\mathtt{let}$s involving patterns 
 
   \begin{center}
-  $\LET (x, y) = (3, 2) \IN x \backslash y \END$
+  $\LET (x, y) = (3, 2) \IN x\,\backslash\,y \END$
   \end{center}
 
   \noindent
   we want to bind all variables from the pattern (there might be an arbitrary
-  number of them) inside the body of the let, but we also care about the order
-  of these variables, since we do not want to identify this term with
+  number of them) inside the body of the $\mathtt{let}$, but we also care about 
+  the order of these variables, since we do not want to identify the above term 
+  with
 
   \begin{center}
-  $\LET (y, x) = (3, 2) \IN x \backslash y \END$
+  $\LET (y, x) = (3, 2) \IN x\,\backslash y\,\END$
   \end{center}
 
   \noindent
-  Therefore we have identified three abstraction mechanisms for multiple binders
-  and allow the user to chose which one is intended. 
+  As a result, we provide three general abstraction mechanisms for multiple binders
+  and allow the user to chose which one is intended when formalising a
+  programming language calculus.
 
-  By providing general abstraction mechanisms that allow the binding of multiple
-  variables, we have to work around aproblem that has been first pointed out
-  by Pottier in \cite{Pottier}: in let-constructs such as
+  By providing these general abstraction mechanisms, however, we have to work around 
+  a problem that has been pointed out by Pottier in \cite{Pottier06}: in 
+  $\mathtt{let}$-constructs of the form
 
   \begin{center}
   $\LET x_1 = t_1 \AND \ldots \AND x_n = t_n \IN s \END$
   \end{center}
 
   \noindent
-  where the $x_i$ are bound in $s$. In this term we might not care about the order in 
+  which bind all the $x_i$ in $s$, we might not care about the order in 
   which the $x_i = t_i$ are given, but we do care about the information that there are 
-  as many $x_i$ as there are $t_i$. We lose this information if we specify the 
+  as many $x_i$ as there are $t_i$. We lose this information if we represent the 
   $\mathtt{let}$-constructor as something like 
 
   \begin{center}
-  $\LET [x_1,\ldots,x_n].s\; [t_1,\ldots,t_n]$
+  $\LET [x_1,\ldots,x_n].s\;\; [t_1,\ldots,t_n]$
   \end{center}
 
   \noindent
-  where the $[\_].\_$ indicates that a list of variables become bound
+  where the $[\_\!\_].\_\!\_$ indicates that a list of variables becomes bound
   in $s$. In this representation we need additional predicates to ensure 
   that the two lists are of equal length. This can result into very 
-  elaborate reasoning (see \cite{BengtsonParow09}). 
+  unintelligible reasoning (see for example~\cite{BengtsonParow09}).