--- a/Paper/Paper.thy	Fri Mar 19 10:24:49 2010 +0100
+++ b/Paper/Paper.thy	Fri Mar 19 12:31:17 2010 +0100
@@ -25,7 +25,7 @@
   \noindent
   where free and bound variables have names.
   For such terms Nominal Isabelle derives automatically a reasoning
-  infrastructure, which has been used in formalisations of an equivalence
+  infrastructure, which has been used successfully 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
@@ -44,15 +44,15 @@
   \end{center}
 
   \noindent
-  and the quantification binds a finite (possibly empty) set of type-variables.
-  While it is possible to formalise such abstractions by iterating single bindings, 
-  this leads to a rather clumsy formalisation of W. This need of iterating single binders 
-  in order to representing multiple binders is also one reason why Nominal Isabelle and other 
+  and the quantification binds at once a finite (possibly empty) set of type-variables.
+  While it is possible to implement this kind of more general binders by iterating single binders, 
+  this leads to a rather clumsy formalisation of W. The need of iterating single binders 
+  is also one reason why Nominal Isabelle and similar 
   theorem provers have not fared extremely well with the more advanced tasks 
   in the POPLmark challenge \cite{challenge05}, because also there one would like 
   to bind multiple variables at once.
 
-  Binding multiple variables in a single abstraction has interesting properties that are not
+  Binding multiple variables has interesting properties that are not
   captured by iterating single binders. 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
@@ -79,14 +79,12 @@
 
   \noindent
   where $z$ does not occur freely in the type.
-  In this paper we will give a general abstraction mechanism and associated
+  In this paper we will give a general binding 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 
+  this kind of binding 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 terms like
 
@@ -104,12 +102,12 @@
   \end{center}
 
   \noindent
-  Therefore we will also provide a separate abstraction mechanism for cases 
+  Therefore we will also provide a separate binding mechanism for cases 
   in which the order of binders does not matter, but the ``cardinality'' of the 
   binders has to agree.
 
-  However, we found that this is still not sufficient for covering language 
-  constructs frequently occuring in programming language research. For example 
+  However, we found that this is still not sufficient for dealing with language 
+  constructs frequently occurring in programming language research. For example 
   in $\mathtt{let}$s involving patterns 
 
   \begin{equation}\label{two}
@@ -126,11 +124,11 @@
   \end{center}
 
   \noindent
-  As a result, we provide three general abstraction mechanisms for binding multiple
-  variables and allow the user to chose which one is intended when formalising a
+  As a result, we provide three general binding mechanisms each of which binds multiple
+  variables at once, and we let the user chose which one is intended when formalising a
   programming language calculus.
 
-  By providing these general abstraction mechanisms, however, we have to work around 
+  By providing these general binding 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
 
@@ -149,17 +147,17 @@
   \end{center}
 
   \noindent
-  where the notation $[\_\!\_].\_\!\_$ indicates that a set of variables becomes 
+  where the notation $[\_\!\_].\_\!\_$ indicates that the $x_i$ become 
   bound in $s$. In this representation we need additional predicates about terms 
   to ensure that the two lists are of equal length. This can result into very 
   unintelligible reasoning (see for example~\cite{BengtsonParow09}). 
-  To avoid this, we will allow for example specifications of $\mathtt{let}$s 
+  To avoid this, we will allow to specify $\mathtt{let}$s 
   as follows
 
   \begin{center}
   \begin{tabular}{r@ {\hspace{2mm}}r@ {\hspace{2mm}}l}
   $trm$ & $::=$  & \ldots\\ 
-        & $\mid$ & $\mathtt{let}\;a\!::\!assn\;\;t\!::\!trm\quad\mathtt{bind}\;bn\,(a) \IN t$\\[1mm]
+        & $\mid$ & $\mathtt{let}\;a\!::\!assn\;\;s\!::\!trm\quad\mathtt{bind}\;bn\,(a) \IN s$\\[1mm]
   $assn$ & $::=$  & $\mathtt{anil}$\\
          & $\mid$ & $\mathtt{acons}\;\;name\;\;trm\;\;assn$
   \end{tabular}
@@ -167,7 +165,7 @@
 
   \noindent
   where $assn$ is an auxiliary type representing a list of assignments
-  and $bn$ an auxilary function identifying the variables to be bound by 
+  and $bn$ an auxiliary function identifying the variables to be bound by 
   the $\mathtt{let}$. This function can be defined as 
 
   \begin{center}
@@ -175,50 +173,47 @@
   \end{center}
   
   \noindent
+  The scope of the binding is indicated by labels given to the types, for example
+  $s\!::\!trm$, and a binding clause $\mathtt{bind}\;bn\,(a) \IN s$.
   This style of specifying terms and bindings is heavily 
   inspired by the syntax of the Ott-tool \cite{ott-jfp}.
 
-  However, we will not be able to deal with all specifications that are allowed by
-  Ott. One reason is that we establish the reasoning infrastructure for
-  alpha-\emph{equated} terms. In contrast, Ott produces for a subset of its
-  specifiactions a reasoning infrastructure for terms that have names for
-  bound variables, but these terms are concrete, \emph{non}-alpha-equated terms. To see 
-  the difference, note that working
-  with alpha-equated terms means that the two type-schemes with $x$, $y$ and
-  $z$ being distinct
+  However, we will not be able to deal with all specifications that are
+  allowed by Ott. One reason is that we establish the reasoning infrastructure
+  for alpha-\emph{equated} terms. In contrast, Ott produces for a subset of
+  its specifications a reasoning infrastructure in Isabelle for
+  \emph{non}-alpha-equated, or ``raw'', terms. While our alpha-equated terms
+  and the concrete terms produced by Ott use names for the bound variables,
+  there is a key difference: working with alpha-equated terms means that the
+  two type-schemes with $x$, $y$ and $z$ being distinct
 
   \begin{center}
   $\forall \{x\}. x \rightarrow y  \;=\; \forall \{x, z\}. x \rightarrow y$ 
   \end{center}
   
   \noindent
-  are not just alpha-equal, but actually equal. Our insistence on reasoning
-  with alpha-equated terms comes from the wealth of experience we gained with
+  are not just alpha-equal, but actually equal (note the ``=''-sign). Our insistence 
+  on reasoning with alpha-equated terms comes from the wealth of experience we gained with
   the older version of Nominal Isabelle: for non-trivial properties, reasoning
   about alpha-equated terms is much easier than reasoning with concrete
-  terms. The fundamental reason for this is that the HOL-logic underlying
-  Nominal Isabelle allows us to replace ``equals-by-equals''. In contrast,
-  replacing ``alpha-equals-by-alpha-equals'' requires a lot of extra work.
+  terms. The fundamental reason is that the HOL-logic underlying
+  Nominal Isabelle allows us to replace ``equals-by-equals''. In contrast replacing 
+  ``alpha-equals-by-alpha-equals'' in a term calculus requires a lot of extra reasoning work.
 
   
   Although in informal settings a reasoning infrastructure for alpha-equated 
-  terms that have names is nearly always taken for granted, establishing 
+  terms (that have names for bound variables) is nearly always taken for granted, establishing 
   it automatically in a theorem prover is a rather non-trivial task. 
   For every specification we will need to construct a type containing as 
-  elements exactly those sets containing alpha-equal terms. To do so we use 
+  elements the alpha-equated terms. To do so we use 
   the standard HOL-technique of defining a new type by  
   identifying a non-empty subset of an existing type. In our 
-   we take as the starting point the type of sets of concrete
-  terms (the latter being defined as datatypes). Then quotient these
-  sets according to our alpha-equivalence relation and then identifying
-  the new type as these alpha-equivalence classes.  The construction we 
+  case  we take as the starting point the type of sets of concrete
+  terms (the latter being defined as a datatype). Then identify the 
+  alpha-equivalence classes according to our alpha-equivalence relation and 
+  then identify the new type as these alpha-equivalence classes.  The construction we 
   can perform in HOL is illustrated by the following picture:
-
-  
-
-  Contributions:  We provide definitions for when terms
-  involving general bindings are alpha-equivelent.
-
+ 
   \begin{center}
   figure
   %\begin{pspicture}(0.5,0.0)(8,2.5)
@@ -370,7 +365,7 @@
   many discussions about Nominal Isabelle. We thank Peter Sewell for 
   making the informal notes \cite{SewellBestiary} available to us and 
   also for explaining some of the finer points about the abstract 
-  definitions and about the implmentation of the Ott-tool.
+  definitions and about the implementation of the Ott-tool.
 
 
 *}

--- a/Paper/document/root.tex	Fri Mar 19 10:24:49 2010 +0100
+++ b/Paper/document/root.tex	Fri Mar 19 12:31:17 2010 +0100
@@ -39,7 +39,7 @@
 
 \begin{document}
 
-\title{\LARGE\bf General Binding Structures in Nominal Isabelle,\\ or How to
+\title{\LARGE\bf General Bindings in Nominal Isabelle,\\ or How to
   Formalise Core-Haskell}
 \maketitle
 
@@ -49,13 +49,14 @@
 prover. It provides a proving infrastructure for convenient reasoning about
 programming language calculi involving bound variables that have names (as
 opposed to de-Bruijn indices). In this paper we present an extension of
-Nominal Isabelle in order to deal with general binding structures. Such
+Nominal Isabelle for dealing with general binding structures, that means
+where multiple variables are bound at once. Such
 binding structures are ubiquitous in programming language research and only
 very poorly supported with single binders, such as the lambdas in the
-lambda-calculus. For our extension we introduce novel definitions of
-alpha-equivalence and establish automatically the reasoning infrastructure for
+lambda-calculus. Our extension includes novel definitions of
+alpha-equivalence and establishes automatically the reasoning infrastructure for
 alpha-equated terms. This includes strong induction principles that have the
-variable convention already built in.
+usual variable convention already built in.
 \end{abstract}