--- a/Paper/Paper.thy	Thu Apr 01 17:00:52 2010 +0200
+++ b/Paper/Paper.thy	Thu Apr 01 17:55:46 2010 +0200
@@ -1487,11 +1487,36 @@
   creating new types in Isabelle/HOL (recall the picture shown in the 
   Introduction).
 
-  The first usefull property about term-constructors @{text
-  "C"}$^\alpha_{1..m}$ is to know that they are distinct, that is
-  @{text "C"}$^\alpha_i$@{text "x\<^isub>1 \<dots> x\<^isub>n"} @{text "\<noteq>"} 
-  @{text "C"}$^\alpha_j$@{text "y\<^isub>1 \<dots> y\<^isub>m"} holds for @{text "i \<noteq> j"}.
+  The first useful property about term-constructors 
+  is to know that they are distinct, that is
+  %
+  \begin{equation}\label{distinctalpha}
+  \mbox{@{text "C"}$^\alpha_i$@{text "x\<^isub>1 \<dots> x\<^isub>n"} @{text "\<noteq>"} 
+  @{text "C"}$^\alpha_j$@{text "y\<^isub>1 \<dots> y\<^isub>m"} holds for @{text "i \<noteq> j"}.} 
+  \end{equation}
+  
+  \noindent
+  By definition of alpha-equivalence on raw terms we can show that
+  for the raw term-constructors
 
+  \begin{center}
+  @{text "C\<^isub>i x\<^isub>1 \<dots> x\<^isub>n"}$\;\not\approx@{text ty}\;$@{text "C\<^isub>j y\<^isub>1 \<dots> y\<^isub>m"} holds for @{text "i \<noteq> j"}.
+  \end{center}
+
+  \noindent
+  In order to generate \eqref{distinctalpha} from this fact, the quotient
+  package needs to know that the term-constructors @{text "C\<^isub>i"} and @{text "C\<^isub>j"} 
+  are \emph{respectful} w.r.t.~the alpha-equivalence relations \cite{Homeier05}.
+  
+  Given a term-constructor @{text C} of type @{text ty} and argument
+  types @{text "C ty\<^isub>1 \<dots> ty\<^isub>n"}, respectfullness means that
+  %
+  \begin{center}
+  aa
+  \end{center}
+   
+
+  \mbox{}\bigskip\bigskip
   then define the quotient types @{text "ty\<^isub>1\<^isup>\<alpha> \<dots> ty\<^isub>n\<^isup>\<alpha>"}.  To lift
   the raw definitions to the quotient type, we need to prove that they
   \emph{respect} the relation. We follow the definition of respectfullness given
@@ -1772,15 +1797,15 @@
 
 text {*
   To our knowledge the earliest usage of general binders in a theorem prover
-  setting is in \cite{NaraschewskiNipkow99}, which describes a formalisation
-  of the algorithm W. This formalisation implements binding in type schemes
-  using a de-Bruijn indices representation. Since type schemes contain only a
-  single binder, different indices do not refer to different binders (as in
-  the usual de-Bruijn representation), but to different bound variables. Also
-  recently an extension for general binders has been proposed for the locally
-  nameless approach to binding \cite{chargueraud09}.  In this proposal, de-Bruijn 
-  indices consist of two numbers, one referring to the place where a variable is bound
-  and the other to which variable is bound. The reasoning infrastructure for both
+  is described in \cite{NaraschewskiNipkow99} about a formalisation of the
+  algorithm W. This formalisation implements binding in type schemes using a
+  de-Bruijn indices representation. Since type schemes contain only a single
+  binder, different indices do not refer to different binders (as in the usual
+  de-Bruijn representation), but to different bound variables. A similar idea
+  has been recently explored for general binders in the locally nameless
+  approach to binding \cite{chargueraud09}.  There de-Bruijn indices consist
+  of two numbers, one referring to the place where a variable is bound and the
+  other to which variable is bound. The reasoning infrastructure for both
   kinds of de-Bruijn indices comes for free in any modern theorem prover as
   the corresponding term-calculi can be implemented as ``normal'' datatypes.
   However, in both approaches, it seems difficult to achieve our fine-grained
@@ -1788,23 +1813,28 @@
   binders should matter, or vacuous binders should be taken into account). To
   do so, requires additional predicates that filter out some unwanted
   terms. Our guess is that they results in rather intricate formal reasoning.
+  Also one motivation of our work is that the user does not need to know
+  anything at all about de-Bruijn indices, which are of course visible in the
+  usual de-Bruijn indices representations, but also in locally nameless
+  representations.
 
   Another representation technique for binding is higher-order abstract syntax
   (HOAS), for example implemented in the Twelf system. This representation
-  technique supports very elegantly some aspects of \emph{single} binding, and
+  technique supports very elegantly many aspects of \emph{single} binding, and
   impressive work is in progress that uses HOAS for mechanising the metatheory
-  of SML \cite{LeeCraryHarper07}. We are not aware how multiple binders of SML
-  are represented in this work, but the submitted Twelf-solution for the
-  POPLmark challenge reveals that HOAS cannot easily deal with binding
+  of SML \cite{LeeCraryHarper07}. We are, however, not aware how multiple binders of SML
+  are represented in this work. Judging from the submitted Twelf-solution for the
+  POPLmark challenge, HOAS cannot easily deal with binding
   constructs where the number of bound variables is not fixed. For example in
-  the second part of this challenge, @{text "Let"}s involve patterns and bind
-  multiple variables at once. In such situations, HOAS needs to use, essentially,
-  iterated single binders for representing multiple binders.
+  the second part of this challenge, @{text "Let"}s involve patterns that bind
+  multiple variables at once. In such situations, HOAS representations have to 
+  resort, essentially, to the iterated-single-binders-approach with all the unwanted
+  consequences for reasoning about terms. 
 
   Two formalisations involving general binders have been performed in older
   versions of Nominal Isabelle \cite{BengtsonParow09, UrbanNipkow09}.  Both
-  use the approach based on iterated single binders. Our experience with the
-  latter formalisation has been far from satisfying. The major pain arises
+  use also the approach based on iterated single binders. Our experience with the
+  latter formalisation has been disappointing. The major pain arises
   from the need to ``unbind'' variables. This can be done in one step with our
   general binders, for example @{term "Abs as x"}, but needs a cumbersome
   iteration with single binders. The resulting formal reasoning is rather
@@ -1812,30 +1842,36 @@
   substantial improvement.  
  
   The most closely related work is the description of the Ott-tool
-  \cite{ott-jfp}. This tool is a nifty front end for creating \LaTeX{}
+  \cite{ott-jfp}. This tool is a nifty front-end for creating \LaTeX{}
   documents from term-calculi specifications. For a subset of the
   specifications, Ott can also generate theorem prover code using a raw
-  representation and a locally nameless representation for terms. The
-  developers of this tool have also put forward a definition for the notion of
-  alpha-equivalence of the term-calculi that can be specified in Ott.  This
-  definition is rather different from ours, not using any of the nominal
-  techniques; it also aims for maximum expressivity, covering as many binding
-  structures from programming language research as possible.  Although we were
-  heavily inspired by their syntax, their definition of alpha-equivalence was
-  no use at all 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 sense for our alpha-equated terms, and it
-  also allows empty types that have no meaning in a HOL-based theorem
-  prover. Because of how we set up our definitions, we had to impose some
+  representation and in Coq also a locally nameless representation for
+  terms. The developers of this tool have also put forward (on paper) a
+  definition for the notion of alpha-equivalence of the term-calculi that can
+  be specified in Ott.  This definition is rather different from ours, not
+  using any nominal techniques; it also aims for maximum expressivity,
+  covering as many binding structures from programming language research as
+  possible.  Although we were heavily inspired by their syntax, their
+  definition of alpha-equivalence was no use at all 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
+  sense for our alpha-equated terms. It also allows empty types that have
+  no meaning in a HOL-based theorem prover. 
+
+  Because of how we set up our definitions, we had to impose some
   restrictions, like excluding overlapping deep binders, which are not present
-  in Ott. Our motivation is that we can still cover interesting term-calculi
+  in Ott. Our expectation is that we can still cover many interesting term-calculi
   from programming language research, like Core-Haskell. For features of Ott,
   like subgrammars, the datatype infrastructure in Isabelle/HOL is
-  unfortunately not yet powerful enough. On the other hand we are not aware
-  that Ott can make any distinction between our three different binding
-  modes. Also, definitions for notions like free-variables are work in
-  progress in Ott.
+  unfortunately not yet powerful enough to implement them. On the other hand 
+  we are not aware that Ott can make any distinction between our three 
+  different binding modes. Also, definitions for notions like free-variables 
+  are work in progress in Ott. Since Ott produces either raw representations
+  or locally nameless representations it can largely rely on the reasoning
+  infrastructure derived automatically by the theorem provers. In contrast,
+  have to make considerable effort to establish a reasoning infrastructure 
+  for alpha-equated terms. 
 *}
 
 section {* Conclusion *}