
diff -r 0d845717f181 -r 2789dd26171a Paper/Paper.thy
--- a/Paper/Paper.thy	Fri Mar 19 10:24:16 2010 +0100
+++ b/Paper/Paper.thy	Fri Mar 19 10:24:49 2010 +0100
@@ -16,15 +16,15 @@
 
 text {*
   So far, Nominal Isabelle provides a mechanism for constructing
-  automatically alpha-equated terms such as
+  alpha-equated terms such as
 
   \begin{center}
   $t ::= x \mid t\;t \mid \lambda x. t$
   \end{center}
 
   \noindent
-  where bound variables have a name.
-  For such terms it derives automatically a reasoning
+  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
   checking algorithm for LF \cite{UrbanCheneyBerghofer08}, Typed
   Scheme~\cite{TobinHochstadtFelleisen08}, several calculi for concurrency
@@ -33,7 +33,7 @@
   used by Pollack for formalisations in the locally-nameless approach to
   binding \cite{SatoPollack10}.
 
-  However, Nominal Isabelle fared less well in a formalisation of
+  However, Nominal Isabelle has fared less well in a formalisation of
   the algorithm W \cite{UrbanNipkow09}, where types and type-schemes
   are of the form
 
@@ -44,17 +44,17 @@
   \end{center}
 
   \noindent
-  and the quantification abstracts over a finite (possibly empty) set of type variables.
+  and the quantification binds 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 
+  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 
   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.
+  in the POPLmark challenge \cite{challenge05}, because also there one would like 
+  to bind multiple variables at once.
 
-  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
+  Binding multiple variables in a single abstraction 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
   type-schemes as alpha-equivalent
 
@@ -78,6 +78,7 @@
   \end{center}
 
   \noindent
+  where $z$ does not occur freely in the type.
   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 
@@ -89,13 +90,13 @@
   However, the notion of alpha-equivalence that is preserved by vacuous binders is not
   alway wanted. For example in terms like
 
-  \begin{center}
-  $\LET x = 3 \AND y = 2 \IN x\,\backslash\,y \END$
-  \end{center}
+  \begin{equation}\label{one}
+  \LET x = 3 \AND y = 2 \IN x\,\backslash\,y \END
+  \end{equation}
 
   \noindent
   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 
+  given, but it would be unusual to regard \eqref{one} as alpha-equivalent 
   with
 
   \begin{center}
@@ -105,29 +106,28 @@
   \noindent
   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.
+  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 
   in $\mathtt{let}$s involving patterns 
 
-  \begin{center}
-  $\LET (x, y) = (3, 2) \IN x\,\backslash\,y \END$
-  \end{center}
+  \begin{equation}\label{two}
+  \LET (x, y) = (3, 2) \IN x\,\backslash\,y \END
+  \end{equation}
 
   \noindent
-  we want to bind all variables from the pattern (there might be an arbitrary
-  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
+  we want to bind all variables from the pattern inside the body of the
+  $\mathtt{let}$, but we also care about the order of these variables, since
+  we do not want to identify \eqref{two} with
 
   \begin{center}
   $\LET (y, x) = (3, 2) \IN x\,\backslash y\,\END$
   \end{center}
 
   \noindent
-  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
+  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
   programming language calculus.
 
   By providing these general abstraction mechanisms, however, we have to work around 
@@ -149,9 +149,9 @@
   \end{center}
 
   \noindent
-  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 
+  where the notation $[\_\!\_].\_\!\_$ indicates that a set of variables becomes 
+  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 
   as follows
@@ -168,21 +168,22 @@
   \noindent
   where $assn$ is an auxiliary type representing a list of assignments
   and $bn$ an auxilary function identifying the variables to be bound by 
-  the $\mathtt{let}$, given by 
+  the $\mathtt{let}$. This function can be defined as 
 
   \begin{center}
   $bn\,(\mathtt{anil}) = \varnothing \qquad bn\,(\mathtt{acons}\;x\;t\;as) = \{x\} \cup bn\,(as)$ 
   \end{center}
   
   \noindent
-  This style of specifications for term-calculi with multiple binders is heavily 
-  inspired by the Ott-tool \cite{ott-jfp}.
+  This style of specifying terms and bindings is heavily 
+  inspired by the syntax of the Ott-tool \cite{ott-jfp}.
 
-  We will not be able to deal with all specifications that are allowed by
+  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 involving concrete,
-  \emph{non}-alpha-equated terms. To see the difference, note that working
+  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
 
@@ -191,25 +192,23 @@
   \end{center}
   
   \noindent
-  are not just alpha-equal, but actually equal---we are working with 
-  alpha-equivalence classes, but still have that bound variables 
-  carry a name.
-  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 is that the HOL-logic 
-  underlying Nominal Isabelle allows us to replace ``equals-by-equals''. 
-  Replacing ``alpha-equals-by-alpha-equals'' requires a lot of work.
+  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
+  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.
+
   
-  Although a reasoning infrastructure for alpha-equated terms with names 
-  is in informal reasoning nearly always taken for granted, establishing 
+  Although in informal settings a reasoning infrastructure for alpha-equated 
+  terms that have names is nearly always taken for granted, establishing 
   it automatically in a theorem prover is a rather non-trivial task. 
-  For every specification we will construct a type that contains 
-  exactly the corresponding alpha-equated terms. For this we use the 
-  standard HOL-technique of defining a new type that has been 
-  identified as a non-empty subset of an existing type. In our 
-  context we take as the starting point the type of sets of concrete
+  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 
+  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 
@@ -271,8 +270,8 @@
   logic work are sorted atoms and permutations of atoms. The sorted atoms
   represent different kinds of variables, such as term- and type-variables in
   Core-Haskell, and it is assumed that there is an infinite supply of atoms
-  for each sort. However, in order to simplify the description of our work, we
-  shall assume in this paper that there is only a single sort of atoms.
+  for each sort. However, in order to simplify the description, we
+  shall assume in what follows that there is only a single sort of atoms.
 
   Permutations are bijective functions from atoms to atoms that are 
   the identity everywhere except on a finite number of atoms. There is a 




