
diff -r 4de1d6ab04f7 -r a5a6aebec1fb LMCS-Paper/Paper.thy
--- a/LMCS-Paper/Paper.thy	Sun Sep 18 22:52:56 2011 +0200
+++ b/LMCS-Paper/Paper.thy	Mon Sep 19 21:52:59 2011 +0200
@@ -166,7 +166,7 @@
 
   \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
+  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
@@ -253,7 +253,7 @@
   the Isabelle/HOL theorem prover.
 
   However, we will not be able to cope with all specifications that are
-  allowed by Ott. One reason is that Ott lets the user specify ``empty'' types
+  allowed by Ott. One reason is that Ott lets the user specify `empty' types
   like \mbox{@{text "t ::= t t | \<lambda>x. t"}} where no clause for variables is
   given. Arguably, such specifications make some sense in the context of Coq's
   type theory (which Ott supports), but not at all in a HOL-based environment
@@ -261,7 +261,7 @@
   \cite{Berghofer99}.  Another reason is that we establish the reasoning
   infrastructure for alpha-\emph{equated} terms. In contrast, Ott produces a
   reasoning infrastructure in Isabelle/HOL for \emph{non}-alpha-equated, or
-  ``raw'', terms. While our alpha-equated terms and the raw terms produced by
+  `raw', terms. While our alpha-equated terms and the raw terms produced by
   Ott use names for bound variables, there is a key difference: working with
   alpha-equated terms means, for example, that the two type-schemes
 
@@ -281,8 +281,8 @@
   for non-trivial properties, reasoning with alpha-equated terms is much
   easier than reasoning with raw terms. The fundamental reason for this 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
+  `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
@@ -330,11 +330,11 @@
   non-empty subset shows that the new type is a faithful representation of
   alpha-equated terms. That is not the case for example for terms using the
   locally nameless representation of binders \cite{McKinnaPollack99}: in this
-  representation there are ``junk'' terms that need to be excluded by
+  representation there are `junk' terms that need to be excluded by
   reasoning about a well-formedness predicate.
 
   The problem with introducing a new type in Isabelle/HOL is that in order to
-  be useful, a reasoning infrastructure needs to be ``lifted'' from the
+  be useful, a reasoning infrastructure needs to be `lifted' from the
   underlying subset to the new type. This is usually a tricky and arduous
   task. To ease it, we re-implemented in Isabelle/HOL \cite{KaliszykUrban11}
   the quotient package described by Homeier \cite{Homeier05} for the HOL4
@@ -368,7 +368,7 @@
   (Note that this means also the term-constructors for variables, applications
   and lambda are lifted to the quotient level.)  This construction, of course,
   only works if alpha-equivalence is indeed an equivalence relation, and the
-  ``raw'' definitions and theorems are respectful w.r.t.~alpha-equivalence.
+  `raw' definitions and theorems are respectful w.r.t.~alpha-equivalence.
   For example, we will not be able to lift a bound-variable function. Although
   this function can be defined for raw terms, it does not respect
   alpha-equivalence and therefore cannot be lifted. 
@@ -402,7 +402,7 @@
   improvement over Ott is that we introduce three binding modes (only one is
   present in Ott), provide formalised definitions for alpha-equivalence and
   for free variables of our terms, and also derive a reasoning infrastructure
-  for our specifications from ``first principles'' inside a theorem prover.
+  for our specifications from `first principles' inside a theorem prover.
 
 
   \begin{figure}[t]
@@ -504,8 +504,8 @@
   \]\smallskip
 
   The most original aspect of the nominal logic work of Pitts is a general
-  definition for the notion of the ``set of free variables of an object @{text
-  "x"}''.  This notion, written @{term "supp x"}, is general in the sense that
+  definition for the notion of the `set of free variables of an object @{text
+  "x"}'.  This notion, written @{term "supp x"}, is general in the sense that
   it applies not only to lambda-terms (alpha-equated or not), but also to lists,
   products, sets and even functions. Its definition depends only on the
   permutation operation and on the notion of equality defined for the type of
@@ -635,7 +635,7 @@
   the renamed binders @{term "\<pi> \<bullet> as"} avoid @{text c} (which can be arbitrarily chosen
   as long as it is finitely supported) and also @{text "\<pi>"} does not affect anything
   in the support of @{text x} (that is @{term "supp x \<sharp>* \<pi>"}). The last 
-  fact and Property~\ref{supppermeq} allow us to ``rename'' just the binders 
+  fact and Property~\ref{supppermeq} allow us to `rename' just the binders 
   @{text as} in @{text x}, because @{term "\<pi> \<bullet> x = x"}. 
 
   Note that @{term "supp x \<sharp>* \<pi>"}
@@ -661,7 +661,7 @@
 
   In order to keep our work with deriving the reasoning infrastructure
   manageable, we will wherever possible state definitions and perform proofs
-  on the ``user-level'' of Isabelle/HOL, as opposed to writing custom ML-code that
+  on the `user-level' of Isabelle/HOL, as opposed to writing custom ML-code that
   generates them anew for each specification. 
   To that end, we will consider
   first pairs @{text "(as, x)"} of type @{text "(atom set) \<times> \<beta>"}.  These pairs
@@ -676,7 +676,7 @@
   set"}}, then @{text x} and @{text y} need to have the same set of free
   atoms; moreover there must be a permutation @{text \<pi>} such that {\it
   (ii)} @{text \<pi>} leaves the free atoms of @{text x} and @{text y} unchanged, but
-  {\it (iii)} ``moves'' their bound names so that we obtain modulo a relation,
+  {\it (iii)} `moves' their bound names so that we obtain modulo a relation,
   say \mbox{@{text "_ R _"}}, two equivalent terms. We also require that {\it (iv)}
   @{text \<pi>} makes the sets of abstracted atoms @{text as} and @{text bs} equal. The
   requirements {\it (i)} to {\it (iv)} can be stated formally as:
@@ -696,7 +696,7 @@
   Note that the relation is
   dependent on a free-atom function @{text "fa"} and a relation @{text
   "R"}. The reason for this extra generality is that we will use
-  $\approx_{\,\textit{set}}^{\textit{R}, \textit{fa}}$ for both ``raw'' terms and 
+  $\approx_{\,\textit{set}}^{\textit{R}, \textit{fa}}$ for both `raw' terms and 
   alpha-equated terms. In
   the latter case, @{text R} will be replaced by equality @{text "="} and we
   will prove that @{text "fa"} is equal to @{text "supp"}.
@@ -891,8 +891,8 @@
   \end{equation}\smallskip
   
   \noindent
-  which by Property~\ref{supportsprop} gives us ``one half'' of
-  Theorem~\ref{suppabs}. The ``other half'' is a bit more involved. To establish 
+  which by Property~\ref{supportsprop} gives us `one half' of
+  Theorem~\ref{suppabs}. The `other half' is a bit more involved. To establish 
   it, we use a trick from \cite{Pitts04} and first define an auxiliary 
   function @{text aux}, taking an abstraction as argument
 
@@ -925,7 +925,7 @@
   the first equation of Theorem~\ref{suppabs}. 
 
   Recall the definition of support given in \eqref{suppdef}, and note the difference between 
-  the support of a ``raw'' pair and an abstraction
+  the support of a `raw' pair and an abstraction
 
   \[
   @{term "supp (as, x) = supp as \<union> supp x"}\hspace{15mm}
@@ -936,8 +936,8 @@
   While the permutation operations behave in both cases the same (a permutation
   is just moved to the arguments), the notion of equality is different for pairs and
   abstractions. Therefore we have different supports. In case of abstractions,
-  we have established that bound atoms are removed from the support of the
-  abstractions' bodies.
+  we have established in Theorem~\ref{suppabs} that bound atoms are removed from 
+  the support of the abstractions' bodies.
 
   The method of first considering abstractions of the form @{term "Abs_set as
   x"} etc is motivated by the fact that we can conveniently establish at the
@@ -997,7 +997,7 @@
   contained in the collection of @{text ty}$^\alpha_{1..n}$ declared in
   \eqref{scheme}. In this case we will call the corresponding argument a
   \emph{recursive argument} of @{text "C\<^sup>\<alpha>"}. The types of such
-  recursive arguments need to satisfy a ``positivity'' restriction, which
+  recursive arguments need to satisfy a `positivity' restriction, which
   ensures that the type has a set-theoretic semantics (see
   \cite{Berghofer99}).  The labels annotated on the types are optional. Their
   purpose is to be used in the (possibly empty) list of \emph{binding
@@ -1018,8 +1018,8 @@
   matters); the second is for sets of binders (the order does not matter, but
   the cardinality does) and the last is for sets of binders (with vacuous
   binders preserving alpha-equivalence). As indicated, the labels in the
-  ``\isacommand{in}-part'' of a binding clause will be called \emph{bodies};
-  the ``\isacommand{binds}-part'' will be called \emph{binders}. In contrast to
+  `\isacommand{in}-part' of a binding clause will be called \emph{bodies};
+  the `\isacommand{binds}-part' will be called \emph{binders}. In contrast to
   Ott, we allow multiple labels in binders and bodies.  For example we allow
   binding clauses of the form:
  
@@ -1098,7 +1098,7 @@
   in the second case makes a difference to the semantics of the specification
   (which we will define in the next section).
 
-  A \emph{deep} binder uses an auxiliary binding function that ``picks'' out
+  A \emph{deep} binder uses an auxiliary binding function that `picks' out
   the atoms in one argument of the term-constructor, which can be bound in
   other arguments and also in the same argument (we will call such binders
   \emph{recursive}, see below). The binding functions are
@@ -1150,7 +1150,7 @@
   \noindent
   where the argument of the deep binder also occurs in the body. We call such
   binders \emph{recursive}.  To see the purpose of such recursive binders,
-  compare ``plain'' @{text "Let"}s and @{text "Let_rec"}s in the following
+  compare `plain' @{text "Let"}s and @{text "Let_rec"}s in the following
   specification:
  
   \begin{equation}\label{letrecs}
@@ -1272,21 +1272,21 @@
   term-constructors so that binders and their bodies are next to each other
   will result in inadequate representations in cases like \mbox{@{text "Let
   x\<^isub>1 = t\<^isub>1\<dots>x\<^isub>n = t\<^isub>n in s"}}. Therefore we will
-  first extract ``raw'' datatype definitions from the specification and then
+  first extract `raw' datatype definitions from the specification and then
   define explicitly an alpha-equivalence relation over them. We subsequently
   construct the quotient of the datatypes according to our alpha-equivalence.
 
 
-  The ``raw'' 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"}''.
+  given by the user. In our implementation we just use the affix `@{text "_raw"}'.
   But for the purpose of this paper, we use the superscript @{text "_\<^sup>\<alpha>"} to indicate 
   that a notion is given for alpha-equivalence classes and leave it out 
-  for the corresponding notion given on the ``raw'' level. So for example 
+  for the corresponding notion given on the `raw' level. So for example 
   we have @{text "ty\<^sup>\<alpha> / ty"} and @{text "C\<^sup>\<alpha> / C"}
   where @{term ty} is the type used in the quotient construction for 
-  @{text "ty\<^sup>\<alpha>"} and @{text "C"} is the term-constructor of the ``raw'' type @{text "ty"},
+  @{text "ty\<^sup>\<alpha>"} and @{text "C"} is the term-constructor of the `raw' type @{text "ty"},
   respectively @{text "C\<^sup>\<alpha>"} is the corresponding term-constructor of @{text "ty\<^sup>\<alpha>"}. 
 
   The resulting datatype definition is legal in Isabelle/HOL provided the datatypes are 
@@ -1295,7 +1295,7 @@
   in Isabelle/HOL). 
   We subsequently define each of the user-specified binding 
   functions @{term "bn"}$_{1..m}$ by recursion over the corresponding 
-  ``raw'' datatype. We also define permutation operations by 
+  `raw' datatype. We also define permutation operations by 
   recursion so that for each term constructor @{text "C"} we have that
   
   \begin{equation}\label{ceqvt}
@@ -1308,7 +1308,7 @@
   The first non-trivial step we have to perform is the generation of
   \emph{free-atom functions} from the specifications.\footnote{Admittedly, the
   details of our definitions will be somewhat involved. However they are still
-  conceptually simple in comparison with the ``positional'' approach taken in
+  conceptually simple in comparison with the `positional' approach taken in
   Ott \cite[Pages 88--95]{ott-jfp}, which uses the notions of \emph{occurrences} and
   \emph{partial equivalence relations} over sets of occurrences.} For the
   \emph{raw} types @{text "ty"}$_{1..n}$ we define the free-atom functions
@@ -1329,13 +1329,13 @@
   
   \noindent
   The reason for this setup is that in a deep binder not all atoms have to be
-  bound, as we saw in \eqref{letrecs} with the example of ``plain'' @{text Let}s. We need
+  bound, as we saw in \eqref{letrecs} with the example of `plain' @{text Let}s. We need
   therefore functions that calculate those free atoms in deep binders.
 
   While the idea behind these free-atom functions is simple (they just
   collect all atoms that are not bound), because of our rather complicated
   binding mechanisms their definitions are somewhat involved.  Given
-  a ``raw'' term-constructor @{text "C"} of type @{text ty} and some associated
+  a `raw' 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
   "fa_ty (C z\<^isub>1 \<dots> z\<^isub>n)"} will be the union @{text
   "fa(bc\<^isub>1) \<union> \<dots> \<union> fa(bc\<^isub>k)"} where we will define below what @{text "fa"} for a binding
@@ -1444,7 +1444,7 @@
   & (that means nothing is bound in @{text "z\<^isub>i"} by the binding function),\smallskip\\
   $\bullet$ & @{term "fa_bn\<^isub>i z\<^isub>i"} provided @{text "z\<^isub>i"} occurs in  @{text "rhs"}
   with the recursive call @{text "bn\<^isub>i z\<^isub>i"}\\
-  & (that means whatever is ``left over'' from the @{text "bn"}-function is free)\smallskip\\
+  & (that means whatever is `left over' from the @{text "bn"}-function is free)\smallskip\\
   $\bullet$ & @{term "{}"} provided @{text "z\<^isub>i"} occurs in  @{text "rhs"},
   but without a recursive call\\
   & (that means @{text "z\<^isub>i"} is supposed to become bound by the binding function)\\
@@ -1496,7 +1496,7 @@
   this example the free atoms in the argument @{text "t"}.
 
 
-  An interesting point in this example is that a ``naked'' assignment (@{text
+  An interesting point in this example is that a `naked' assignment (@{text
   "ANil"} or @{text "ACons"}) does not bind any atoms, even if the binding
   function is specified over assignments. Only in the context of a @{text Let}
   or @{text "Let_rec"}, where the binding clauses are given, will some atoms
@@ -1506,7 +1506,7 @@
   act on atoms that are bound. In that case, these functions would \emph{not}
   respect alpha-equivalence.
 
-  Having the free atom functions at our disposal, we can next define the 
+  Having the free-atom functions at our disposal, we can next define the 
   alpha-equivalence relations for the raw types @{text
   "ty"}$_{1..n}$. We write them as
   
@@ -1629,7 +1629,7 @@
   \noindent
   This premise accounts for alpha-equivalence of the bodies of the binding
   clause. However, in case the binders have non-recursive deep binders, this
-  premise is not enough: we also have to ``propagate'' alpha-equivalence
+  premise is not enough: we also have to `propagate' alpha-equivalence
   inside the structure of these binders. An example is @{text "Let"} where we
   have to make sure the right-hand sides of assignments are
   alpha-equivalent. For this we use relations @{text "\<approx>bn"}$_{1..m}$ (which we
@@ -1721,13 +1721,13 @@
 
   \noindent
   Notice the difference between  $\approx_{\textit{assn}}$ and
-  $\approx_{\textit{bn}}$: the latter only ``tracks'' alpha-equivalence of 
+  $\approx_{\textit{bn}}$: the latter only `tracks' alpha-equivalence of 
   the components in an assignment that are \emph{not} bound. This is needed in the 
   clause for @{text "Let"} (which has
   a non-recursive binder). 
   The underlying reason is that the terms inside an assignment are not meant 
-  to be ``under'' the binder. Such a premise is \emph{not} needed in @{text "Let_rec"}, 
-  because there all components of an assignment are ``under'' the binder. 
+  to be `under' the binder. Such a premise is \emph{not} needed in @{text "Let_rec"}, 
+  because there all components of an assignment are `under' the binder. 
   Note also that in case of more than one body (that is in the @{text "Let_rec"}-case above)
   we need to parametrise the relation $\approx_{\textit{list}}$ with a compound
   equivalence relation and a compound free-atom function. This is because the
@@ -1758,8 +1758,8 @@
   \begin{proof}
   The function package of Isabelle/HOL allows us to prove the first part by
   mutual induction over the definitions of the functions.\footnote{We have
-  that they are terminating functions. From this an induction principle is
-  derived by the function package \cite{Krauss09}.} The second is by a
+  that the free-atom functions are terminating. From this the function
+  package derives an induction principle \cite{Krauss09}.} The second is by a
   straightforward induction over the rules of @{text "\<approx>ty"}$_{1..n}$ and
   @{text "\<approx>bn"}$_{1..m}$ using the first part.
   \end{proof}
@@ -1785,7 +1785,7 @@
   We can feed the last lemma into our quotient package and obtain new types
   @{text "ty"}$^\alpha_{1..n}$ representing alpha-equated terms of types
   @{text "ty"}$_{1..n}$. We also obtain definitions for the term-constructors
-  @{text "C"}$^\alpha_{1..k}$ from the ``raw'' term-constructors @{text
+  @{text "C"}$^\alpha_{1..k}$ from the `raw' term-constructors @{text
   "C"}$_{1..k}$, and similar definitions for the free-atom functions @{text
   "fa_ty"}$^\alpha_{1..n}$ and @{text "fa_bn"}$^\alpha_{1..m}$ as well as the
   binding functions @{text "bn"}$^\alpha_{1..m}$. However, these definitions
@@ -1811,9 +1811,9 @@
   \end{equation}\smallskip
 
   \noindent
-  holds for the corresponding ``raw'' term-constructors.
+  holds for the corresponding `raw' term-constructors.
   In order to deduce \eqref{distinctalpha} from \eqref{distinctraw}, our quotient
-  package needs to know that the ``raw'' term-constructors @{text "C"} and @{text "D"} 
+  package needs to know that the `raw' term-constructors @{text "C"} and @{text "D"} 
   are \emph{respectful} w.r.t.~the alpha-equivalence relations (see \cite{Homeier05}).
   Given, for example, @{text "C"} is of type @{text "ty"} with argument types
   @{text "ty"}$_{1..r}$, respectfulness amounts to showing that
@@ -1849,7 +1849,7 @@
   "bn"}$_{1..m}$ so that they return bound atoms and in this case the third
   implication is \emph{not} true. A result is that in general the lifting of the
   corresponding binding functions in Ott to alpha-equated terms is impossible.
-  Having established respectfulness for the ``raw'' term-constructors, the 
+  Having established respectfulness for the `raw' term-constructors, the 
   quotient package is able to automatically deduce \eqref{distinctalpha} from 
   \eqref{distinctraw}.
 
@@ -1869,10 +1869,10 @@
   of the free-atom functions @{text "fa_ty\<AL>"}$_{1..n}$ and
   @{text "fa_bn\<AL>"}$_{1..m}$ as well as of the binding functions @{text
   "bn\<AL>"}$_{1..m}$ and size functions @{text "size_ty\<AL>"}$_{1..n}$.
-  The latter are defined automatically for the ``raw'' types @{text "ty"}$_{1..n}$
+  The latter are defined automatically for the `raw' types @{text "ty"}$_{1..n}$
   by the datatype package of Isabelle/HOL.
 
-  We also need to lift the properties that characterise when two ``raw'' terms of the form
+  We also need to lift the properties that characterise when two `raw' terms of the form
   
   \[
   \mbox{@{text "C x\<^isub>1 \<dots> x\<^isub>r \<approx>ty C x\<PRIME>\<^isub>1 \<dots> x\<PRIME>\<^isub>r"}}
@@ -1955,7 +1955,7 @@
 
   Recall the lambda-calculus with @{text "Let"}-patterns shown in
   \eqref{letpat}. The cases lemmas and the induction principle shown in
-  \eqref{cases} and \eqref{induct} boil down in this example to the following three inference
+  \eqref{cases} and \eqref{induct} boil down in that example to the following three inference
   rules (the cases lemmas are on the left-hand side; the induction principle
   on the right):
 
@@ -2019,11 +2019,11 @@
   
   \noindent
   Lastly, we can show that the support of elements in @{text
-  "ty\<AL>"}$_{1..n}$ is the same as the free atom functions @{text
+  "ty\<AL>"}$_{1..n}$ is the same as the free-atom functions @{text
   "fa_ty\<AL>"}$_{1..n}$.  This fact is important in the nominal setting where
   the general theory is formulated in terms of support and freshness, but also
   provides evidence that our notions of free-atoms and alpha-equivalence
-  ``match up'' correctly.
+  `match up' correctly.
 
   \begin{thm}\label{suppfa} 
   For @{text "x"}$_{1..n}$ with type @{text "ty\<AL>"}$_{1..n}$, we have
@@ -2040,7 +2040,7 @@
   \end{proof}
 
   \noindent
-  Consequently, we can replace the free atom functions by @{text "supp"} in  
+  Consequently, we can replace the free-atom functions by @{text "supp"} in  
   our quasi-injection lemmas. In the examples shown in \eqref{alphalift}, for instance,
   we obtain for @{text "Let\<^sup>\<alpha>"} and @{text "Let_rec\<^sup>\<alpha>"} 
 
@@ -2091,7 +2091,7 @@
 
   To sum up this section, we have established a reasoning infrastructure for the
   types @{text "ty\<AL>"}$_{1..n}$ by first lifting definitions from the
-  ``raw'' level to the quotient level and then by proving facts about
+  `raw' level to the quotient level and then by proving facts about
   these lifted definitions. All necessary proofs are generated automatically
   by custom ML-code.
 *}
@@ -2103,9 +2103,9 @@
   In the previous section we derived induction principles for alpha-equated
   terms (see \eqref{induct} for the general form and \eqref{inductex} for an
   example). This was done by lifting the corresponding inductions principles
-  for ``raw'' terms.  We already employed these induction principles for
+  for `raw' terms.  We already employed these induction principles for
   deriving several facts about alpha-equated terms, including the property that
-  the free-variable functions and the notion of support coincide. Still, we
+  the free-atom functions and the notion of support coincide. Still, we
   call these induction principles \emph{weak}, because for a term-constructor,
   say \mbox{@{text "C\<^sup>\<alpha> x\<^isub>1\<dots>x\<^isub>r"}}, the induction
   hypothesis requires us to establish (under some assumptions) a property
@@ -2151,13 +2151,13 @@
   of the form @{text " P\<^bsub>trm\<^esub> c y\<^isub>1 \<and>
   P\<^bsub>pat\<^esub> c y\<^isub>2"} in which the additional parameter @{text
   c} is assumed to be of finite support. The purpose of @{text "c"} is to
-  ``control'' which freshness assumptions the binders should satisfy in the
+  `control' which freshness assumptions the binders should satisfy in the
   @{text "Lam\<^sup>\<alpha>"} and @{text "Let_pat\<^sup>\<alpha>"} cases: for @{text
   "Lam\<^sup>\<alpha>"} we can assume the bound atom @{text "x\<^isub>1"} is fresh
   for @{text "c"} (third line); for @{text "Let_pat\<^sup>\<alpha>"} we can assume
   all bound atoms from an assignment are fresh for @{text "c"} (fourth
   line). If @{text "c"} is instantiated appropriately in the strong induction
-  principle, the user can mimic the usual ``pencil-and-paper'' reasoning
+  principle, then the user can mimic the usual `pencil-and-paper' reasoning
   employing the variable convention about bound and free variables being
   distinct \cite{Urban08}.
 
@@ -2165,8 +2165,8 @@
   \eqref{inductex} implies the strong one \eqref{stronginduct}. This fact was established for
   single binders in \cite{Urban08} by some quite involved, nevertheless
   automated, induction proof. In this paper we simplify the proof by
-  leveraging the automated proving methods from the function package of
-  Isabelle/HOL \cite{Krauss09}. The reasoning principle behind these methods
+  leveraging the automated proving tools from the function package of
+  Isabelle/HOL \cite{Krauss09}. The reasoning principle behind these tools
   is well-founded induction. To use them in our setting, we have to discharge
   two proof obligations: one is that we have well-founded measures (one for
   each type @{text "ty"}$^\alpha_{1..n}$) that decrease in every induction
@@ -2174,7 +2174,7 @@
   principle. Once these two proof obligations are discharged, the reasoning
   infrastructure in the function package will automatically derive the
   stronger induction principle. This way of establishing the stronger induction
-  principle is considerably simpler than the work presented \cite{Urban08}.
+  principle is considerably simpler than the earlier work presented \cite{Urban08}.
 
   As measures we can use the size functions @{text "size_ty"}$^\alpha_{1..n}$,
   which we lifted in the previous section and which are all well-founded. It
@@ -2207,7 +2207,7 @@
   "Lam\<^sup>\<alpha>"} and @{text "Let_pat\<^sup>\<alpha>"} cases that the bound atoms
   avoid a context @{text "c"} (which is assumed to be finitely supported).
   
-  These stronger cases lemmas need to be derived from the `weak' cases lemmas
+  These stronger cases lemmas can be derived from the `weak' cases lemmas
   given in \eqref{inductex}. This is trivial in case of patterns (the one on
   the right-hand side) since the weak and strong cases lemma coincide (there
   is no binding in patterns).  Interesting are only the cases for @{text
@@ -2230,7 +2230,7 @@
 
   \noindent
   which we must use to infer @{text "P\<^bsub>trm\<^esub>"}. Clearly, we cannot
-  use this implication directly, because we have no information whether @{text
+  use this implication directly, because we have no information whether or not @{text
   "x\<^isub>1"} is fresh for @{text "c"}.  However, we can use Properties
   \ref{supppermeq} and \ref{avoiding} to rename @{text "x\<^isub>1"}: we know
   by Theorem~\ref{suppfa} that @{text "{atom x\<^isub>1} #\<^sup>* Lam\<^sup>\<alpha>
@@ -2264,10 +2264,10 @@
   \end{equation}\smallskip
 
   \noindent
-  The reason that this case is more complicated is that we cannot apply directly Property 
+  The reason that this case is more complicated is that we cannot directly apply Property 
   \ref{avoiding} for obtaining a renaming permutation. Property \ref{avoiding} requires
   that the binders are fresh for the term in which we want to perform the renaming. But
-  this is not true in cases like (using informal notation)
+  this is not true in terms such as (using an informal notation)
 
   \[
   @{text "Let (x, y) := (x, y) in (x, y)"}
@@ -2275,7 +2275,7 @@
 
   \noindent
   where @{text x} and @{text y} are bound in the term, but they are also free
-  in the assignment. We can, however, obtain such a renaming permutation, say
+  in the right-hand side of the assignment. We can, however, obtain such a renaming permutation, say
   @{text "\<pi>"}, for the abstraction @{term "Abs_lst (bn_al x\<^isub>1)
   x\<^isub>3"}. As a result we have \mbox{@{term "set (bn_al (\<pi> \<bullet> x\<^isub>1))
   \<sharp>* c"}} and @{term "Abs_lst (bn_al (\<pi> \<bullet> x\<^isub>1)) (\<pi> \<bullet> x\<^isub>3) =
@@ -2291,29 +2291,29 @@
 
   \noindent
   Since all atoms in a pattern are bound by @{text "Let_pat\<^sup>\<alpha>"}, we can infer
-  @{text "(\<pi> \<bullet> x\<^isub>1) \<approx>\<AL>\<^bsub>bn\<^esub> x\<^isub>1"} holds for every @{text "\<pi>"}. Therefore we have that
+  that @{text "(\<pi> \<bullet> x\<^isub>1) \<approx>\<AL>\<^bsub>bn\<^esub> x\<^isub>1"} holds for every @{text "\<pi>"}. Therefore we have that
 
   \[
   @{text "Let_pat\<^sup>\<alpha> (\<pi> \<bullet> x\<^isub>1) x\<^isub>2 (\<pi> \<bullet> x\<^isub>3) = Let_pat\<^sup>\<alpha> x\<^isub>1 x\<^isub>2 x\<^isub>3"}  
   \]\smallskip
   
   \noindent
-  Taking the left-hand side in the assumption from \eqref{assmtwo}, we can use
+  Taking the left-hand side in the assumption shown in \eqref{assmtwo}, we can use
   the implication \eqref{impletpat} from the stronger cases lemma to infer @{text "P\<^bsub>trm\<^esub>"}, as needed.
 
-  The remaining difficulty is when a deep binder contains atoms that are
-  bound, but also some that are free. An example is @{text "Let\<^sup>\<alpha>"} in
+  The remaining difficulty is when a deep binder contains some atoms that are
+  bound and some that are free. An example is @{text "Let\<^sup>\<alpha>"} in
   the example \eqref{letrecs}.  In such cases @{text "(\<pi> \<bullet> x\<^isub>1)
-  \<approx>\<AL>\<^bsub>bn\<^esub> x\<^isub>1"} does not hold in general. The idea is
-  that we only want to rename binders that will become bound. This does not
-  affect @{text "\<approx>\<AL>\<^bsub>bn\<^esub>"}. However, the problem is that the
-  permutation operation @{text "_ \<bullet> _"} applies to all of them. To avoid this
+  \<approx>\<AL>\<^bsub>bn\<^esub> x\<^isub>1"} does not hold in general. The idea however is
+  that @{text "\<pi>"} only renames atoms that become bound. In this way @{text "\<pi>"}
+  does not affect @{text "\<approx>\<AL>\<^bsub>bn\<^esub>"}. However, the problem is that the
+  permutation operation @{text "\<pi> \<bullet> x\<^isub>1"} applies to all attoms in @{text "x\<^isub>1"}. To avoid this
   we introduce an auxiliary permutation operations, written @{text "_
   \<bullet>\<^bsub>bn\<^esub> _"}, for deep binders that only permutes bound atoms (or
   more precisely the atoms specified by the @{text "bn"}-functions) and leaves
-  the other atoms unchanged. Like the @{text "fa_bn"}$_{1..m}$-functions, we
-  can define these operations over raw terms analysing how the @{text
-  "bn"}$_{1..m}$-functions are defined. Assuming the user specified a clause
+  the other atoms unchanged. Like the functions @{text "fa_bn"}$_{1..m}$, we
+  can define these operations over raw terms analysing how the functions @{text
+  "bn"}$_{1..m}$ are defined. Assuming the user specified a clause
 
   \[  
   @{text "bn (C x\<^isub>1 \<dots> x\<^isub>r) = rhs"}
@@ -2335,7 +2335,8 @@
   alpha-equated terms. Moreover we can prove the following two properties
 
   \begin{lem}\label{permutebn} 
-  Given a binding function @{text "bn\<^sup>\<alpha>"} then for all @{text "\<pi>"}\smallskip\\
+  Given a binding function @{text "bn\<^sup>\<alpha>"} and auxiliary equivalence @{text "\<approx>\<AL>\<^bsub>bn\<^esub>"} 
+  then for all @{text "\<pi>"}\smallskip\\
   {\it (i)} @{text "\<pi> \<bullet> (bn\<^sup>\<alpha> x) = bn\<^sup>\<alpha> (\<pi> \<bullet>\<AL>\<^bsub>bn\<^esub> x)"} and\\ 
   {\it (ii)} @{text "(\<pi>  \<bullet>\<AL>\<^bsub>bn\<^esub> x) \<approx>\<AL>\<^bsub>bn\<^esub> x"}.
   \end{lem}
@@ -2363,10 +2364,10 @@
   \]\smallskip
 
   \noindent
-  hold. Using Lemma \ref{permutebn}{\it (i)} we can simplify this
+  hold. Using the first part of Lemma \ref{permutebn}, we can simplify this
   to @{text "set (bn\<^sup>\<alpha> (\<pi> \<bullet>\<AL>\<^bsub>bn\<^esub> x\<^isub>1)) #\<^sup>* c"} and 
   @{text "[bn\<^sup>\<alpha> (\<pi> \<bullet>\<AL>\<^bsub>bn\<^esub> x\<^isub>1)]\<^bsub>list\<^esub>. (\<pi> \<bullet> x\<^isub>2) = [bn\<^sup>\<alpha> x\<^isub>1]\<^bsub>list\<^esub>. x\<^isub>2"}. Since
-  @{text "(\<pi>  \<bullet>\<AL>\<^bsub>bn\<^esub> x\<^isub>1) \<approx>\<AL>\<^bsub>bn\<^esub> x\<^isub>1"} holds by Lemma \ref{permutebn}{\it (ii)},
+  @{text "(\<pi>  \<bullet>\<AL>\<^bsub>bn\<^esub> x\<^isub>1) \<approx>\<AL>\<^bsub>bn\<^esub> x\<^isub>1"} holds by teh second part,
   we can infer that
 
   \[
@@ -2377,9 +2378,11 @@
   holds. This allows us to use the implication from the strong cases
   lemma.
 
-  Conseqently,  we can discharge all proof-obligations to do with having covered all
-  cases. This completes the proof showing that the weak induction principles imply 
-  the strong induction principles.
+  Conseqently,  we can discharge all proof-obligations about having covered all
+  cases. This completes the proof establishing that the weak induction principles imply 
+  the strong induction principles. These strong induction principles have proved 
+  already to be very useful in practice, particularly for proving properties about 
+  capture-avoiding substitution. 
 *}
 
 
@@ -2393,15 +2396,15 @@
   W contain only a single place where variables are bound, 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 by Chargu\'eraud in the locally nameless 
-  approach to
-  binding \cite{chargueraud09}.  There, de-Bruijn indices consist of two
+  recently explored for general binders by Chargu\'eraud \cite{chargueraud09}
+  in the locally nameless approach to
+  binding.  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
   representations of bindings comes for free in theorem provers like
   Isabelle/HOL and Coq, since the corresponding term-calculi can be implemented
-  as ``normal'' datatypes.  However, in both approaches it seems difficult to
-  achieve our fine-grained control over the ``semantics'' of bindings
+  as `normal' datatypes.  However, in both approaches it seems difficult to
+  achieve our fine-grained control over the `semantics' of bindings
   (i.e.~whether the order of binders should matter, or vacuous binders should
   be taken into account). To do so, one would require additional predicates
   that filter out unwanted terms. Our guess is that such predicates result in
@@ -2409,14 +2412,14 @@
   a non-trivial language that uses Chargu\'eraud's idea.
 
   Another technique for representing binding is higher-order abstract syntax
-  (HOAS), which for example is implemented in the Twelf system. This
-  representation technique supports very elegantly many aspects of
-  \emph{single} binding, and impressive work by Lee et al has been done that
-  uses HOAS for mechanising the metatheory of SML~\cite{LeeCraryHarper07}. We
+  (HOAS), which for example is implemented in the Twelf system \cite{pfenningsystem}. 
+  This representation technique supports very elegantly many aspects of
+  \emph{single} binding, and impressive work by Lee et al ~\cite{LeeCraryHarper07} 
+  has been done that uses HOAS for mechanising the metatheory of SML. 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,
+  variables is not fixed. For example, in the second part of this challenge,
   @{text "Let"}s involve patterns that bind multiple variables at once. In
   such situations, HOAS seems to have to resort to the
   iterated-single-binders-approach with all the unwanted consequences when
@@ -2429,7 +2432,7 @@
   \cite{BengtsonParow09,UrbanNipkow09}).  Both
   use the approach based on iterated single binders. Our experience with
   the latter formalisation has been disappointing. The major pain arose from
-  the need to ``unbind'' variables. This can be done in one step with our
+  the need to `unbind' variables. This can be done in one step with our
   general binders described in this paper, but needs a cumbersome
   iteration with single binders. The resulting formal reasoning turned out to
   be rather unpleasant. 
@@ -2438,7 +2441,7 @@
   Sewell et al \cite{ott-jfp} and the C$\alpha$ml language by Pottier
   \cite{Pottier06}. Ott is a nifty front-end for creating \LaTeX{} documents
   from specifications of term-calculi involving general binders. For a subset
-  of the specifications Ott can also generate theorem prover code using a ``raw''
+  of the specifications Ott can also generate theorem prover code using a `raw'
   representation of terms, and in Coq also a locally nameless
   representation. The developers of this tool have also put forward (on paper)
   a definition for alpha-equivalence and free variables for terms that can be
@@ -2447,9 +2450,10 @@
   result concerning this notion of alpha-equivalence and free variables. We
   have proved that our definitions lead to alpha-equated terms, whose support
   is as expected (that means bound names are removed from the support). We
-  also showed that our specifications lift from ``raw'' types to types of
+  also showed that our specifications lift from `raw' types to types of
   alpha-equivalence classes. For this we had to establish (automatically) that every
-  term-constructor and function is respectful w.r.t.~alpha-equivalence.
+  term-constructor and function defined for `raw' types 
+  is respectful w.r.t.~alpha-equivalence.
 
   Although we were heavily inspired by the syntax of Ott, its definition of
   alpha-equi\-valence is unsuitable for our extension of Nominal
@@ -2475,7 +2479,7 @@
   
   \noindent
   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
+  `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\footnote{Assuming @{term "a \<noteq> b"}, there is no permutation that can
   make @{text "(a, b)"} equal with both @{text "(a, b)"} and @{text "(b, a)"}, but
@@ -2507,9 +2511,12 @@
   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 (see Figure~\ref{nominalcorehas}).
+  example the Core-Haskell language from the Introduction. With the work
+  presented in this paper we can define formally this language as shown in 
+  Figure~\ref{nominalcorehas} and then Nominal Isabelle derives automatically
+  a corresponding reasoning infrastructure.
 
-  \begin{figure}[t]
+  \begin{figure}[p]
   \begin{boxedminipage}{\linewidth}
   \small
   \begin{tabular}{l}
@@ -2556,15 +2563,15 @@
   $|$~@{text "bv\<^isub>3 (TVCKCons c cty tl) = (atom c)::(bv\<^isub>3 tl)"}\\
   \end{tabular}
   \end{boxedminipage}
-  \caption{The nominal datatype declaration for Core-Haskell. For the moment we
+  \caption{A definition for Core-Haskell in Nominal Isabelle. For the moment we
   do not support nested types; therefore we explicitly have to unfold the 
   lists @{text "co_lst"}, @{text "assoc_lst"} and so on. Apart from that, the 
-  declaration follows closely the original in Figure~\ref{corehas}. The
-  point of our work is that having made such a declaration in Nominal Isabelle,
-  one obtains automatically a reasoning infrastructure for Core-Haskell.\bigskip\bigskip
+  definition follows closely the original shown in Figure~\ref{corehas}. The
+  point of our work is that having made such a definition in Nominal Isabelle,
+  one obtains automatically a reasoning infrastructure for Core-Haskell.
   \label{nominalcorehas}}
   \end{figure}
-
+  \afterpage{\clearpage}
 
   Pottier presents a programming language, called C$\alpha$ml, for
   representing terms with general binders inside OCaml \cite{Pottier06}. This
@@ -2596,17 +2603,17 @@
 text {*
 
   We have presented an extension of Nominal Isabelle for dealing with general
-  binders, that is term-constructors having multiple bound variables. For this
+  binders, that is where term-constructors have multiple bound atoms. For this
   extension we introduced new definitions of alpha-equivalence and automated
   all necessary proofs in Isabelle/HOL.  To specify general binders we used
   the syntax from Ott, but extended it in some places and restricted
-  it in others so that they make sense in the context of alpha-equated
+  it in others so that the definitions make sense in the context of alpha-equated
   terms. We also introduced two binding modes (set and set+) that do not exist
   in Ott. We have tried out the extension with calculi such as Core-Haskell,
   type-schemes and approximately a dozen of other typical examples from
   programming language research~\cite{SewellBestiary}. The code will
   eventually become part of the next Isabelle distribution.\footnote{It 
-  can be downloaded from \href{http://isabelle.in.tum.de/nominal/download}
+  can be downloaded already from \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
@@ -2624,7 +2631,7 @@
   version @{text "TFun string ty_list"} (see Figure~\ref{nominalcorehas}). To
   achieve this, we need more clever implementation than we have 
   at the moment. However, really lifting this restriction will involve major
-  work on the datatype package of Isabelle/HOL.
+  work on the underlying datatype package of Isabelle/HOL.
 
   A more interesting line of investigation is whether we can go beyond the 
   simple-minded form of binding functions that we adopted from Ott. At the moment, binding
@@ -2643,7 +2650,7 @@
   imagine that there is need for a binding mode where instead of usual lists,
   we abstract lists of distinct elements (the corresponding type @{text
   "dlist"} already exists in the library of Isabelle/HOL). We expect the
-  presented work can be easily extended to accommodate them.\medskip
+  presented work can be easily extended to accommodate such binding modes.\medskip
   
   \noindent
   {\bf Acknowledgements:} We are very grateful to Andrew Pitts for many




