--- a/Paper/Paper.thy	Fri Jul 02 15:34:46 2010 +0100
+++ b/Paper/Paper.thy	Wed Jul 07 09:34:00 2010 +0100
@@ -90,7 +90,7 @@
   we would like to regard the following two type-schemes as $\alpha$-equivalent
   %
   \begin{equation}\label{ex1}
-  @{text "\<forall>{x, y}. x \<rightarrow> y  \<approx>\<^isub>\<alpha>  \<forall>{y, x}. y \<rightarrow> x"} 
+  @{text "\<forall>{x, y}. x \<rightarrow> y  \<approx>\<^isub>\<alpha>  \<forall>{y, x}. x \<rightarrow> y"} 
   \end{equation}
 
   \noindent
@@ -214,8 +214,8 @@
   The scope of the binding is indicated by labels given to the types, for
   example @{text "s::trm"}, and a binding clause, in this case
   \isacommand{bind} @{text "bn(as)"} \isacommand{in} @{text "s"}. This binding
-  clause states to bind in @{text s} all the names the function @{text
-  "bn(as)"} returns.  This style of specifying terms and bindings is heavily
+  clause states that all the names the function @{text
+  "bn(as)"} returns should be bound in @{text 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 cope with all specifications that are
@@ -358,7 +358,7 @@
   about them in a theorem prover would be a major pain.  \medskip
 
   \noindent
-  {\bf Contributions:}  We provide novel definitions for when terms
+  {\bf Contributions:}  We provide novel three definitions for when terms
   involving general binders are $\alpha$-equivalent. These definitions are
   inspired by earlier work of Pitts \cite{Pitts04}. By means of automatic
   proofs, we establish a reasoning infrastructure for $\alpha$-equated
@@ -366,7 +366,7 @@
   conditions for $\alpha$-equated terms. We are also able to derive strong 
   induction principles that have the variable convention already built in.
   The method behind our specification of general binders is taken 
-  from the Ott-tool, but we introduce crucial restrictions, and also one extension, so 
+  from the Ott-tool, but we introduce crucial restrictions, and also extensions, so 
   that our specifications make sense for reasoning about $\alpha$-equated terms. 
 
 
@@ -1026,7 +1026,7 @@
   
   \noindent
   In this specification the function @{text "bn"} determines which atoms of
-  @{text p} are bound in the argument @{text "t"}. Note that in the
+  the pattern @{text p} are bound in the argument @{text "t"}. Note that in the
   second-last @{text bn}-clause the function @{text "atom"} coerces a name
   into the generic atom type of Nominal Isabelle \cite{HuffmanUrban10}. This
   allows us to treat binders of different atom type uniformly.
@@ -1067,11 +1067,11 @@
   \noindent
   The difference is that with @{text Let} we only want to bind the atoms @{text
   "bn(as)"} in the term @{text t}, but with @{text "Let_rec"} we also want to bind the atoms
-  inside the assignment. This difference has consequences for the free-variable 
-  function and $\alpha$-equivalence relation.
+  inside the assignment. This difference has consequences for the associated
+  notions of free-variables and $\alpha$-equivalence.
   
   To make sure that variables bound by deep binders cannot be free at the
-  same time, we cannot have more than one binding function for one deep binder. 
+  same time, we cannot have more than one binding function for a deep binder. 
   Consequently we exclude specifications such as
 
   \begin{center}
@@ -1090,9 +1090,9 @@
   
   We also need to restrict the form of the binding functions in order 
   to ensure the @{text "bn"}-functions can be defined for $\alpha$-equated 
-  terms. As a result we cannot return an atom in a binding function that is also
-  bound in the corresponding term-constructor. That means in the example
-  \eqref{letpat} that the term-constructors @{text PVar} and @{text PTup} may
+  terms. The main restriction is that we cannot return an atom in a binding function that is also
+  bound in the corresponding term-constructor. That means in \eqref{letpat} 
+  that the term-constructors @{text PVar} and @{text PTup} may
   not have a binding clause (all arguments are used to define @{text "bn"}).
   In contrast, in case of \eqref{letrecs} the term-constructor @{text ACons}
   may have a binding clause involving the argument @{text t} (the only one that
@@ -1143,12 +1143,12 @@
   term-constructors so that binders and their bodies are next to each other will 
   result in inadequate representations in cases like @{text "Let x\<^isub>1=t\<^isub>1\<dots>x\<^isub>n=t\<^isub>n in s"}. 
   Therefore we will first
-  extract datatype definitions from the specification and then define 
+  extract ``raw'' datatype definitions from the specification and then define 
   explicitly an $\alpha$-equivalence relation over them. We subsequently
   quotient the datatypes according to our $\alpha$-equivalence.
 
 
-  The datatype definition can be obtained by stripping off the 
+  The ``raw'' datatype definition can be obtained by stripping off the 
   binding clauses and the labels from the types. We also have to invent
   new names for the types @{text "ty\<^sup>\<alpha>"} and term-constructors @{text "C\<^sup>\<alpha>"}
   given by the user. In our implementation we just use the affix ``@{text "_raw"}''.
@@ -1179,15 +1179,14 @@
 
   The first non-trivial step we have to perform is the generation of
   free-variable functions from the specifications. For the 
-  \emph{raw} types @{text "ty"}$_{1..n}$ extracted from  a specification,
-  we define the free-variable functions
+  \emph{raw} types @{text "ty"}$_{1..n}$ we define the free-variable functions
   %
   \begin{equation}\label{fvars}
   @{text "fv_ty\<^isub>1, \<dots>, fv_ty\<^isub>n"}
   \end{equation}
 
   \noindent
-  by recursion over the types @{text "ty"}$_{1..n}$.
+  by mutual recursion.
   We define these functions together with auxiliary free-variable functions for
   the binding functions. Given raw binding functions @{text "bn"}$_{1..m}$ 
   we define
@@ -1204,11 +1203,11 @@
   While the idea behind these free-variable functions is clear (they just
   collect all atoms that are not bound), because of our rather complicated
   binding mechanisms their definitions are somewhat involved.  Given
-  the term-constructor @{text "C"} of type @{text ty} and some associated
+  a term-constructor @{text "C"} of type @{text ty} and some associated
   binding clauses @{text "bc\<^isub>1\<dots>bc\<^isub>k"}, the result of @{text
   "fv_ty (C z\<^isub>1 \<dots> z\<^isub>n)"} will be the union @{text
   "fv(bc\<^isub>1) \<union> \<dots> \<union> fv(bc\<^isub>k)"} where we define below what @{text "fv"} of a binding
-  clause with mode \isacommand{bin\_set} means (similarly for the other modes). 
+  clause means. We only show the mode \isacommand{bind\_set} (the other modes are similar). 
   Suppose the binding clause @{text bc\<^isub>i} is of the form 
   %
   \begin{equation}
@@ -1239,7 +1238,7 @@
   \noindent
   whereby the functions @{text "fv_ty\<^isub>i"} are the ones we are defining by recursion 
   (see \eqref{fvars}) provided the @{text "d\<^isub>i"} refers to one of the raw types 
-  @{text "ty"}$_{1..n}$ from a specification; otherwise we set @{text "fv_ty\<^isub>i d\<^isub>i = supp d\<^isub>i"}.
+  @{text "ty"}$_{1..n}$ from the specification; otherwise we set @{text "fv_ty\<^isub>i d\<^isub>i = supp d\<^isub>i"}.
   In order to define the set @{text B} we use the following auxiliary @{text "bn"}-functions
   for atom types to which shallow binders have to refer
   %