--- a/Paper/Paper.thy	Fri Jul 16 02:38:19 2010 +0100
+++ b/Paper/Paper.thy	Fri Jul 16 03:22:24 2010 +0100
@@ -2066,7 +2066,7 @@
   representations have to resort to the iterated-single-binders-approach with
   all the unwanted consequences when reasoning about the resulting terms.
 
-  In a similar fashion, two formalisations involving general binders have been 
+  Two formalisations involving general binders have been 
   performed in older
   versions of Nominal Isabelle (one about Psi-calculi and one about algorithm W 
   \cite{BengtsonParow09, UrbanNipkow09}).  Both
@@ -2089,10 +2089,10 @@
   rather different from ours, not using any nominal techniques.  To our
   knowledge there is also no concrete mathematical result concerning this
   notion of $\alpha$-equivalence.  A definition for the notion of free variables
-  in a term are work in progress in Ott.
+  is work in progress in Ott.
 
-  Although we were heavily inspired by their syntax,
-  their definition of $\alpha$-equivalence is unsuitable for our extension of
+  Although we were heavily inspired by the syntax in Ott,
+  its definition of $\alpha$-equivalence is unsuitable for our extension of
   Nominal Isabelle. First, it is far too complicated to be a basis for
   automated proofs implemented on the ML-level of Isabelle/HOL. Second, it
   covers cases of binders depending on other binders, which just do not make
@@ -2101,7 +2101,7 @@
   binding clauses. In Ott you specify binding clauses with a single body; we 
   allow more than one. We have to do this, because this makes a difference 
   for our notion of $\alpha$-equivalence in case of \isacommand{bind\_set} and 
-  \isacommand{bind\_res}. This makes 
+  \isacommand{bind\_res}. For example
 
   \begin{center}
   \begin{tabular}{@ {}l@ {\hspace{2mm}}l@ {}}
@@ -2114,9 +2114,9 @@
   \end{center}
 
   \noindent
-  behave differently. In the first term-constructor, we essentially have a single
-  body, which happens to be ``spread'' over two arguments; in the second we have
-  two independent bodies, in which the same variables are bound. As a result we 
+  in the first term-constructor we have a single
+  body that happens to be ``spread'' over two arguments; in the second term-constructor we have
+  two independent bodies in which the same variables are bound. As a result we 
   have
 
   \begin{center}
@@ -2128,58 +2128,53 @@
   \end{tabular}
   \end{center}
 
-  Because of how we set up our definitions, we had to impose restrictions,
-  like a single binding function for a deep binder, that are not present in Ott. Our
+  \noindent
+  and therefore need the extra generality to be able to distinguish between 
+  both specifications.
+  Because of how we set up our definitions, we also had to impose some restrictions
+  (like a single binding function for a deep binder) that are not present in Ott. Our
   expectation is that we can still cover many interesting term-calculi from
-  programming language research, for example Core-Haskell. For providing support
-  of neat features in Ott, such as subgrammars, the existing datatype
-  infrastructure in Isabelle/HOL is unfortunately not powerful enough. On the
-  other hand, we are not aware that Ott can make the distinction between our
-  three different binding modes.
+  programming language research, for example Core-Haskell. 
 
   Pottier presents in \cite{Pottier06} a language, called C$\alpha$ml, for 
   representing terms with general binders inside OCaml. This language is
-  implemented as a front-end that can be translated to OCaml with a help of
+  implemented as a front-end that can be translated to OCaml with the help of
   a library. He presents a type-system in which the scope of general binders
-  can be indicated with some special markers, written @{text "inner"} and 
-  @{text "outer"}. With this, it seems, our and his specifications can be
-  inter-translated, but we have not proved this. However, we believe the
-  binding specifications in the style of Ott are a more natural way for 
-  representing terms involving bindings. Pottier gives a definition for 
-  $\alpha$-equivalence, which is similar to our binding mode \isacommand{bind}. 
-  Although he uses also a permutation in case of abstractions, his
-  definition is rather different from ours. He proves that his notion
-  of $\alpha$-equivalence is indeed a equivalence relation, but a complete
+  can be specified using special markers, written @{text "inner"} and 
+  @{text "outer"}. It seems our and his specifications can be
+  inter-translated as long as ours use the binding mode 
+  \isacommand{bind} only.
+  However, we have not proved this. Pottier gives a definition for 
+  $\alpha$-equivalence, which also uses a permutation operation (like ours).
+  Still, this definition is rather different from ours and he only proves that
+  it defines an equivalence relation. A complete
   reasoning infrastructure is well beyond the purposes of his language. 
+  
   In a slightly different domain (programming with dependent types), the 
   paper \cite{Altenkirch10} presents a calculus with a notion of 
   $\alpha$-equivalence related to our binding mode \isacommand{bind\_res}.
-  This definition is similar to the one by Pottier, except that it
+  The corresponding definition is similar to the one by Pottier, except that it
   has a more operational flavour and calculates a partial (renaming) map. 
-  In this way they can handle vacuous binders. However, their notion of
-  equality between terms also includes rules for $\beta$ and to our
-  knowledge no concrete mathematical result concerning their notion
+  In this way Altenkirch et al can deal with vacuous binders. However, to our
+  best knowledge, no concrete mathematical result concerning their notion
   of equality has been proved.    
 *}
 
 section {* Conclusion *}
 
 text {*
-  We have presented an extension of Nominal Isabelle for deriving
-  automatically a convenient reasoning infrastructure that can deal with
-  general binders, that is term-constructors binding multiple variables at
-  once. This extension has been tried out with the Core-Haskell
-  term-calculus. For such general binders, we can also extend
-  earlier work that derives strong induction principles which have the usual
-  variable convention already built in. For the moment we can do so only with manual help,
-  but future work will automate them completely.  The code underlying the presented
-  extension will become part of the Isabelle distribution.\footnote{For the moment
+  We have presented an extension of Nominal Isabelle for dealing with
+  general binders, that is term-constructors having multiple bound 
+  variables. For this extension we introduced novel definitions of 
+  $\alpha$-equivalence and automated all necessary proofs in Isabelle/HOL.
+  We have tried out the extension with terms from Core-Haskell and our code
+  will become part of the Isabelle distribution.\footnote{For the moment
   it can be downloaded from the Mercurial repository linked at
   \href{http://isabelle.in.tum.de/nominal/download}
   {http://isabelle.in.tum.de/nominal/download}.}
 
   We have left out a discussion about how functions can be defined over
-  $\alpha$-equated terms that involve general binders. In earlier versions of Nominal
+  $\alpha$-equated terms involving general binders. In earlier versions of Nominal
   Isabelle \cite{UrbanBerghofer06} this turned out to be a thorny issue.  We
   hope to do better this time by using the function package that has recently
   been implemented in Isabelle/HOL and also by restricting function
@@ -2190,10 +2185,10 @@
   future work. One is the exclusion of nested datatype definitions. Nested
   datatype definitions allow one to specify, for instance, the function kinds
   in Core-Haskell as @{text "TFun string (ty list)"} instead of the unfolded
-  version @{text "TFun string ty_list"} in Figure~\ref{nominalcorehas}. For
-  them we need a more clever implementation than we have at the moment. 
+  version @{text "TFun string ty_list"} (see Figure~\ref{nominalcorehas}). To
+  achieve this, we need a slightly more clever implementation than we have at the moment. 
 
-  More interesting line of investigation is whether we can go beyond the 
+  A more interesting line of investigation is whether we can go beyond the 
   simple-minded form for binding functions that we adopted from Ott. At the moment, binding
   functions can only return the empty set, a singleton atom set or unions
   of atom sets (similarly for lists). It remains to be seen whether 
@@ -2204,9 +2199,7 @@
   \end{center}
   
   \noindent
-  provide us with means to support more interesting
-  binding functions. 
-
+  allow us to support more interesting binding functions. 
 
   We have also not yet played with other binding modes. For example we can
   imagine that there is need for a binding mode 
@@ -2214,14 +2207,14 @@
   Once we feel confident about such binding modes, our implementation 
   can be easily extended to accommodate them.
 
-  %\medskip
-  %\noindent
-  %{\bf Acknowledgements:} We are very grateful to Andrew Pitts for  
-  %many discussions about Nominal Isabelle. We also thank Peter Sewell for 
-  %making the informal notes \cite{SewellBestiary} available to us and 
-  %also for patiently explaining some of the finer points of the work on the Ott-tool.
-  %Stephanie Weirich suggested to separate the subgrammars
-  %of kinds and types in our Core-Haskell example.  
+  \medskip
+  \noindent
+  {\bf Acknowledgements:} We are very grateful to Andrew Pitts for  
+  many discussions about Nominal Isabelle. We also thank Peter Sewell for 
+  making the informal notes \cite{SewellBestiary} available to us and 
+  also for patiently explaining some of the finer points of the work on the Ott-tool.
+  Stephanie Weirich suggested to separate the subgrammars
+  of kinds and types in our Core-Haskell example.  
 
 *}