
diff -r dbdce626c925 -r 66d388a84e3c Paper/Paper.thy
--- a/Paper/Paper.thy	Fri Mar 19 12:31:55 2010 +0100
+++ b/Paper/Paper.thy	Fri Mar 19 15:43:43 2010 +0100
@@ -23,10 +23,10 @@
   \end{center}
 
   \noindent
-  where free and bound variables have names.
-  For such terms Nominal Isabelle derives automatically a reasoning
-  infrastructure, which has been used successfully in formalisations of an equivalence
-  checking algorithm for LF \cite{UrbanCheneyBerghofer08}, Typed
+  where free and bound variables have names.  For such terms Nominal Isabelle
+  derives automatically a reasoning 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
   for cut-elimination in classical logic \cite{UrbanZhu08}. It has also been
@@ -44,19 +44,19 @@
   \end{center}
 
   \noindent
-  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.
+  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 that only provide
+  mechanisms for binding single variables 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 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
+  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 type-schemes as alpha-equivalent
 
   \begin{center}
   $\forall \{x, y\}. x \rightarrow y  \;\approx_\alpha\; \forall \{y, x\}. y \rightarrow x$ 
@@ -89,7 +89,7 @@
   alway wanted. For example in terms like
 
   \begin{equation}\label{one}
-  \LET x = 3 \AND y = 2 \IN x\,\backslash\,y \END
+  \LET x = 3 \AND y = 2 \IN x\,-\,y \END
   \end{equation}
 
   \noindent
@@ -98,20 +98,20 @@
   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\,-\,y \END$
   \end{center}
 
   \noindent
-  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 
+  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 dealing with language 
-  constructs frequently occurring in programming language research. For example 
-  in $\mathtt{let}$s involving patterns 
+  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 containing patterns
 
   \begin{equation}\label{two}
-  \LET (x, y) = (3, 2) \IN x\,\backslash\,y \END
+  \LET (x, y) = (3, 2) \IN x\,-\,y \END
   \end{equation}
 
   \noindent
@@ -120,7 +120,7 @@
   we do not want to identify \eqref{two} with
 
   \begin{center}
-  $\LET (y, x) = (3, 2) \IN x\,\backslash y\,\END$
+  $\LET (y, x) = (3, 2) \IN x\,- y\,\END$
   \end{center}
 
   \noindent
@@ -140,7 +140,7 @@
   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 represent the 
-  $\mathtt{let}$-constructor as something like 
+  $\mathtt{let}$-constructor by something like 
 
   \begin{center}
   $\LET [x_1,\ldots,x_n].s\;\; [t_1,\ldots,t_n]$
@@ -148,10 +148,11 @@
 
   \noindent
   where the notation $[\_\!\_].\_\!\_$ indicates that the $x_i$ become 
-  bound in $s$. In this representation we need additional predicates about terms 
+  bound in $s$. In this representation the term \mbox{$\LET [x].s\;\;[t_1,t_2]$}
+  would be perfectly legal instance, and so one needs 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 to specify $\mathtt{let}$s 
+  messy reasoning (see for example~\cite{BengtsonParow09}). 
+  To avoid this, we will allow for example to specify $\mathtt{let}$s 
   as follows
 
   \begin{center}
@@ -173,17 +174,18 @@
   \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 
+  The scope of the binding is indicated by labels given to the types, for
+  example \mbox{$s\!::\!trm$}, and a binding clause, in this case
+  $\mathtt{bind}\;bn\,(a) \IN s$, that states bind all the names the function
+  $bn$ returns 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 specifications a reasoning infrastructure in Isabelle for
+  its specifications a reasoning infrastructure in Isabelle/HOL 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,
+  and the raw 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
 
@@ -192,26 +194,29 @@
   \end{center}
   
   \noindent
-  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 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.
+  are not just alpha-equal, but actually equal. As a
+  result, we can only support specifications that make sense on the level of
+  alpha-equated terms (offending specifications, which for example bind a variable
+  according to a variable bound somewhere else, are not excluded by Ott).  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 raw 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 representation based on raw terms requires a lot of extra reasoning work.
 
-  
   Although in informal settings a reasoning infrastructure for alpha-equated 
   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. 
+  it automatically in the Isabelle/HOL theorem prover is a rather non-trivial task. 
   For every specification we will need to construct a type containing as 
   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 
-  case  we take as the starting point the type of sets of concrete
-  terms (the latter being defined as a datatype). Then identify the 
+  case  we take as the starting point the type of sets of raw
+  terms (the latter being defined as a datatype); 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 
+  then define the new type as these alpha-equivalence classes.  The construction we 
   can perform in HOL is illustrated by the following picture:
  
   \begin{center}
@@ -240,7 +245,7 @@
   \noindent
   To ``lift'' the reasoning from the underlying type to the new type
   is usually a tricky task. To ease this task we reimplemented in Isabelle/HOL
-  the quotient package described by Homeier in \cite{Homeier05}. This
+  the quotient package described by Homeier \cite{Homeier05}. This
   re-implementation will automate the proofs we require for our
   reasoning infrastructure over alpha-equated terms.\medskip
 




