--- a/LMCS-Paper/Paper.thy	Wed Feb 29 03:13:45 2012 +0000
+++ b/LMCS-Paper/Paper.thy	Wed Feb 29 04:56:06 2012 +0000
@@ -128,7 +128,8 @@
   definition is to get access to the bound variables and the type-part of a type-scheme
   @{text S}, though in general 
   we will only get access to some variables and some type @{text T} that are  
-  ``alpha-equivalent'' to @{text S}---it is an unbinding \emph{relation}. Still, with this 
+  ``alpha-equivalent'' to @{text S}. This is because unbinding is a relation, not a function. 
+  Still, with this 
   definition in place we can formally define when a type is an instance of a type-scheme as
 
   \[
@@ -139,13 +140,13 @@
   meaning there exists a list of variables @{text xs} and a type @{text T'} to which
   the type-scheme @{text S} unbinds, and there exists a substitution whose domain is
   @{text xs} (seen as set) such that @{text "\<sigma>(T') = T"}.
-  The pain with this definition is that we cannot follow the usual proofs 
+  The problem with this definition is that we cannot follow the usual proofs 
   that are by induction on the type-part of the type-scheme (since it is under
-  an existential quantifier). The representation of type-schemes by iterating single binders 
+  an existential quantifier). The representation of type-schemes using iterations of single binders 
   prevents us from directly ``unbinding'' the bound variables and the type-part of 
   a type-scheme. The purpose of this paper is to introduce general binders, which 
-  allow us to represent type-schemes following closely informal practice and as 
-  a result solve this problem.
+  allow us to represent type-schemes so that they can bind multiple variables at once
+  and as a result solve this problem.
   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
@@ -160,7 +161,7 @@
   the second pair should \emph{not} be alpha-equivalent:
 
   \begin{equation}\label{ex1}
-  @{text "\<forall>{x, y}. x \<rightarrow> y  \<approx>\<^isub>\<alpha>  \<forall>{y, x}. y \<rightarrow> x"}\hspace{10mm}
+  @{text "\<forall>{x, y}. x \<rightarrow> y  \<approx>\<^isub>\<alpha>  \<forall>{x, y}. y \<rightarrow> x"}\hspace{10mm}
   @{text "\<forall>{x, y}. x \<rightarrow> y  \<notapprox>\<^isub>\<alpha>  \<forall>{z}. z \<rightarrow> z"}
   \end{equation}\smallskip
 
@@ -421,7 +422,7 @@
   \noindent
   {\bf Contributions:} We provide three new definitions for when terms
   involving general binders are alpha-equivalent. These definitions are
-  inspired by earlier work of Pitts \cite{Pitts04}. By means of automatically-generated
+  inspired by earlier work of Pitts \cite{Pitts04}. By means of automati\-cally-generated
   proofs, we establish a reasoning infrastructure for alpha-equated terms,
   including properties about support, freshness and equality conditions for
   alpha-equated terms. We are also able to automatically derive strong
@@ -519,7 +520,7 @@
   \end{tabular} &
   \begin{tabular}{@ {}l@ {}}
   @{thm permute_perm_def[where p="\<pi>" and q="\<pi>'", no_vars, THEN eq_reflection]}\\
-  @{thm permute_set_eq[where p="\<pi>", no_vars, THEN eq_reflection]}\\
+  @{thm permute_set_def[where p="\<pi>", no_vars, THEN eq_reflection]}\\
   @{text "\<pi> \<bullet> f \<equiv> \<lambda>x. \<pi> \<bullet> (f (- \<pi> \<bullet> x))"}\\
   @{thm permute_bool_def[where p="\<pi>", no_vars, THEN eq_reflection]}
   \end{tabular}
@@ -618,34 +619,33 @@
   it is required that every permutation leaves @{text f} unchanged, that is
   
   \begin{equation}\label{equivariancedef}
-  @{term "\<forall>\<pi>. \<pi> \<bullet> f = f"}
+  @{term "\<forall>\<pi>. \<pi> \<bullet> f = f"}\;.
   \end{equation}\smallskip
   
   \noindent
   If a function is of type @{text "\<alpha> \<Rightarrow> \<beta>"}, this definition is equivalent to 
   the fact that a permutation applied to the application
   @{text "f x"} can be moved to the argument @{text x}. That means for 
-  functions @{text f} of type @{text "\<alpha> \<Rightarrow> \<beta>"}, we have for all permutations @{text "\<pi>"}:
+  such functions, we have for all permutations @{text "\<pi>"}:
   
   \begin{equation}\label{equivariance}
   @{text "\<pi> \<bullet> f = f"} \;\;\;\;\textit{if and only if}\;\;\;\;
-  @{text "\<forall>x. \<pi> \<bullet> (f x) = f (\<pi> \<bullet> x)"}
+  @{text "\<forall>x. \<pi> \<bullet> (f x) = f (\<pi> \<bullet> x)"}\;.
   \end{equation}\smallskip
    
   \noindent
   There is
   also a similar property for relations, which are in HOL functions of type @{text "\<alpha> \<Rightarrow> \<beta> \<Rightarrow> bool"}.
-  Suppose a relation @{text R}, then
-  that for all permutations @{text \<pi>}:
+  Suppose a relation @{text R}, then for all permutations @{text \<pi>}:
   
   \[
   @{text "\<pi> \<bullet> R = R"} \;\;\;\;\textit{if and only if}\;\;\;\;
-  @{text "\<forall>x y."}~~@{text "x R y"} \;\textit{implies}\; @{text "(\<pi> \<bullet> x) R (\<pi> \<bullet> y)"}
+  @{text "\<forall>x y."}~~@{text "x R y"} \;\textit{implies}\; @{text "(\<pi> \<bullet> x) R (\<pi> \<bullet> y)"}\;.
   \]\smallskip
 
   \noindent
   Note that from property \eqref{equivariancedef} and the definition of @{text supp}, we 
-  can easily deduce that equivariant functions have empty support.
+  can easily deduce that for a function being equivariant is equivalent to having empty support.
 
   Using freshness, the nominal logic work provides us with general means for renaming 
   binders. 
@@ -1043,8 +1043,9 @@
   recursive arguments need to satisfy a `positivity' restriction, which
   ensures that the type has a set-theoretic semantics (see
   \cite{Berghofer99}). If the types are polymorphic, we require the
-  type variables are of finitely supported type.
-  The labels annotated on the types are optional. Their
+  type variables stand for types that are finitely supported and over which 
+  a permutation operation is defined.
+  The labels @{text "label"}$_{1..l}$ annotated on the types are optional. Their
   purpose is to be used in the (possibly empty) list of \emph{binding
   clauses}, which indicate the binders and their scope in a term-constructor.
   They come in three \emph{modes}:
@@ -1238,7 +1239,9 @@
   out different atoms to become bound, respectively be free, in @{text "p"}.
   (Since the Ott-tool does not derive a reasoning infrastructure for 
   alpha-equated terms with deep binders, it can permit such specifications.)
-  
+  For convenience we exlude such specifications even if @{text "bn\<^isub>1"} and 
+  @{text "bn\<^isub>2"} are the same binding functions, which would otherwise be harmless.
+
   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. The main restriction is that we cannot return an atom in a binding