
diff -r 2eafd8ed4bbf -r fd2913415a73 Paper/Paper.thy
--- a/Paper/Paper.thy	Wed Mar 31 02:59:18 2010 +0200
+++ b/Paper/Paper.thy	Wed Mar 31 05:44:24 2010 +0200
@@ -65,7 +65,7 @@
   \end{equation}
 
   \noindent
-  and the quantification $\forall$ binds a finite (possibly empty) set of
+  and the @{text "\<forall>"}-quantification binds a finite (possibly empty) set of
   type-variables.  While it is possible to implement this kind of more general
   binders by iterating single binders, this leads to a rather clumsy
   formalisation of W. The need of iterating single binders is also one reason
@@ -183,8 +183,8 @@
   \begin{center}
   \begin{tabular}{r@ {\hspace{2mm}}r@ {\hspace{2mm}}l}
   @{text trm} & @{text "::="}  & @{text "\<dots>"}\\ 
-              & @{text "|"}    & @{text "\<LET> a::assn s::trm"}\hspace{4mm} 
-                                 \isacommand{bind} @{text "bn(a)"} \isacommand{in} @{text "s"}\\[1mm]
+              & @{text "|"}    & @{text "\<LET> as::assn s::trm"}\hspace{4mm} 
+                                 \isacommand{bind} @{text "bn(as)"} \isacommand{in} @{text "s"}\\[1mm]
   @{text assn} & @{text "::="} & @{text "\<ANIL>"}\\
                & @{text "|"}   & @{text "\<ACONS> name trm assn"}
   \end{tabular}
@@ -204,13 +204,12 @@
   \noindent
   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(a)"} \isacommand{in} @{text "s"}, that states
-  to bind in @{text s} all the names the function call @{text "bn(a)"} returns.
-  This style of specifying terms and bindings is heavily inspired by the
-  syntax of the Ott-tool \cite{ott-jfp}.
+  \isacommand{bind} @{text "bn(as)"} \isacommand{in} @{text "s"}. This binding
+  clause states to bind in @{text s} all the names the function call @{text
+  "bn(as)"} returns.  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 deal with all specifications that are
+  However, we will not be able to cope with all specifications that are
   allowed by Ott. One reason is that Ott lets the user to specify ``empty'' 
   types like
 
@@ -316,7 +315,7 @@
   \end{center}
   
   \noindent
-  then with the help of the quotient package we obtain a function @{text "fv\<^sup>\<alpha>"}
+  then with the help of the quotient package we can obtain a function @{text "fv\<^sup>\<alpha>"}
   operating on quotients, or alpha-equivalence classes of lambda-terms. This
   lifted function is characterised by the equations
 
@@ -344,7 +343,8 @@
   known as Core-Haskell (see Figure~\ref{corehas}). This term language
   involves patterns that have lists of type-, coercion- and term-variables,
   all of which are bound in @{text "\<CASE>"}-expressions. One
-  difficulty is that each of these variables come with a kind or type
+  difficulty is that we do not know in advance how many variables need to
+  be bound. Another is that each bound variable comes with a kind or type
   annotation. Representing such binders with single binders and reasoning
   about them in a theorem prover would be a major pain.  \medskip
 
@@ -410,13 +410,13 @@
   to aid the description of what follows. 
 
   Two central notions in the nominal logic work are sorted atoms and
-  sort-respecting permutations of atoms. We will use the variables @{text "a,
+  sort-respecting permutations of atoms. We will use the letters @{text "a,
   b, c, \<dots>"} to stand for atoms and @{text "p, q, \<dots>"} to stand for
   permutations.  The sorts of atoms can be used to represent different kinds of
-  variables, such as the term-, coercion- and type-variables in Core-Haskell,
-  and it is assumed that there is an infinite supply of atoms for each
-  sort. However, in order to simplify the description, we shall assume in what
-  follows that there is only one sort of atoms.
+  variables, such as the term-, coercion- and type-variables in Core-Haskell.
+  It is assumed that there is an infinite supply of atoms for each
+  sort. However, in order to simplify the description, we shall restrict ourselves 
+  in what follows to only one sort of atoms.
 
   Permutations are bijective functions from atoms to atoms that are 
   the identity everywhere except on a finite number of atoms. There is a 
@@ -433,7 +433,8 @@
   the composition of two permutations @{term p} and @{term q} as \mbox{@{term "p + q"}}, 
   and the inverse permutation of @{term p} as @{text "- p"}. The permutation
   operation is defined by induction over the type-hierarchy (see \cite{HuffmanUrban10});
-  for example as follows for products, lists, sets, functions and booleans:
+  for example permutations acting on products, lists, sets, functions and booleans is
+  given by:
   %
   \begin{equation}\label{permute}
   \mbox{\begin{tabular}{@ {}cc@ {}}
@@ -506,9 +507,9 @@
   
   \noindent 
   in some cases it can be difficult to establish the support precisely, and
-  only give an approximation (see the case for function applications
-  above). Such approximations can be calculated with the notion
-  \emph{supports}, defined as follows
+  only give an approximation (see \eqref{suppfun} above). Reasoning about
+  such approximations can be made precise with the notion \emph{supports}, defined 
+  as follows:
 
   \begin{defn}
   A set @{text S} \emph{supports} @{text x} if for all atoms @{text a} and @{text b}
@@ -516,7 +517,8 @@
   \end{defn}
 
   \noindent
-  The main point of this definition is that we can show the following two properties.
+  The main point of @{text supports} is that we can establish the following 
+  two properties.
 
   \begin{property}\label{supportsprop}
   {\it i)} @{thm[mode=IfThen] supp_is_subset[no_vars]}\\ 
@@ -525,7 +527,7 @@
 
   Another important notion in the nominal logic work is \emph{equivariance}.
   For a function @{text f}, say of type @{text "\<alpha> \<Rightarrow> \<beta>"}, to be equivariant 
-  requires that every permutation leaves @{text f} unchanged, that is
+  it is required that every permutation leaves @{text f} unchanged, that is
   %
   \begin{equation}\label{equivariancedef}
   @{term "\<forall>p. p \<bullet> f = f"}
@@ -541,15 +543,14 @@
   \end{equation}
  
   \noindent
-  From equation \eqref{equivariancedef} and the definition of support shown in
-  \eqref{suppdef}, we can be easily deduce that an equivariant function has
-  empty support.
+  From property \eqref{equivariancedef} and the definition of @{text supp}, we 
+  can be easily deduce that an equivariant function has empty support.
 
-  Finally, the nominal logic work provides us with elegant means to rename 
+  Finally, the nominal logic work provides us with convenient means to rename 
   binders. While in the older version of Nominal Isabelle, we used extensively 
   Property~\ref{swapfreshfresh} for renaming single binders, this property 
-  proved unwieldy for dealing with multiple binders. For this the following
-  generalisations turned out to be easier to use.
+  proved unwieldy for dealing with multiple binders. For such pinders the 
+  following generalisations turned out to be easier to use.
 
   \begin{property}\label{supppermeq}
   @{thm[mode=IfThen] supp_perm_eq[no_vars]}
@@ -564,18 +565,19 @@
 
   \noindent
   The idea behind the second property is that given a finite set @{text as}
-  of binders (being bound in @{text x} which is ensured by the
+  of binders (being bound, or fresh, in @{text x} is ensured by the
   assumption @{term "as \<sharp>* x"}), then there exists a permutation @{text p} such that
-  the renamed binders @{term "p \<bullet> as"} avoid the @{text c} (which can be arbitrarily chosen
-  as long as it is finitely supported) and also does not affect anything
+  the renamed binders @{term "p \<bullet> as"} avoid @{text c} (which can be arbitrarily chosen
+  as long as it is finitely supported) and also it does not affect anything
   in the support of @{text x} (that is @{term "supp x \<sharp>* p"}). The last 
   fact and Property~\ref{supppermeq} allow us to ``rename'' just the binders 
-  in @{text x}, because @{term "p \<bullet> x = x"}.
+  @{text as} in @{text x}, because @{term "p \<bullet> x = x"}.
 
   All properties given in this section are formalised in Isabelle/HOL and also
-  most of them are described with proofs in \cite{HuffmanUrban10}. In the next
-  sections we will make extensively use of these properties for characterising
-  alpha-equivalence in the presence of multiple binders.
+  most of proofs are described in \cite{HuffmanUrban10} to which we refer the
+  reader. In the next sections we will make extensively use of these
+  properties in order to define alpha-equivalence in the presence of multiple
+  binders.
 *}
 
 
@@ -595,7 +597,7 @@
   are intended to represent the abstraction, or binding, of the set @{text
   "as"} in the body @{text "x"}.
 
-  The first question we have to answer is when the pairs @{text "(as, x)"} and
+  The first question we have to answer is when two pairs @{text "(as, x)"} and
   @{text "(bs, y)"} are alpha-equivalent? (At the moment we are interested in
   the notion of alpha-equivalence that is \emph{not} preserved by adding
   vacuous binders.) To answer this, we identify four conditions: {\it i)}
@@ -626,8 +628,7 @@
   "R"}. The reason for this extra generality is that we will use
   $\approx_{\textit{set}}$ for both ``raw'' terms and alpha-equated terms. In
   the latter case, $R$ will be replaced by equality @{text "="} and we
-  will prove that @{text "fv"} is equal to the support of @{text
-  x} and @{text y}.
+  will prove that @{text "fv"} is equal to @{text "supp"}.
 
   The definition in \eqref{alphaset} does not make any distinction between the
   order of abstracted variables. If we want this, then we can define alpha-equivalence 
@@ -673,7 +674,7 @@
   \noindent
   Now recall the examples shown in \eqref{ex1}, \eqref{ex2} and
   \eqref{ex3}. It can be easily checked that @{text "({x, y}, x \<rightarrow> y)"} and
-  @{text "({y, x}, y \<rightarrow> x)"} are equal according to $\approx_{\textit{set}}$ and
+  @{text "({y, x}, y \<rightarrow> x)"} are alpha-equivalent according to $\approx_{\textit{set}}$ and
   $\approx_{\textit{res}}$ by taking @{text p} to be the swapping @{term "(x \<rightleftharpoons>
   y)"}. In case of @{text "x \<noteq> y"}, then @{text "([x, y], x \<rightarrow> y)"}
   $\not\approx_{\textit{list}}$ @{text "([y, x], x \<rightarrow> y)"} since there is no permutation
@@ -750,7 +751,7 @@
   This lemma allows us to use our quotient package and introduce 
   new types @{text "\<beta> abs_set"}, @{text "\<beta> abs_res"} and @{text "\<beta> abs_list"}
   representing alpha-equivalence classes of pairs. The elements in these types 
-  we will, respectively, write as:
+  will be, respectively, written as:
 
   \begin{center}
   @{term "Abs as x"} \hspace{5mm} 
@@ -761,8 +762,8 @@
   \noindent
   indicating that a set or list @{text as} is abstracted in @{text x}. We will
   call the types \emph{abstraction types} and their elements
-  \emph{abstractions}. The important property we need is a characterisation
-  for the support of abstractions, namely:
+  \emph{abstractions}. The important property we need to know is what the 
+  support of abstractions is, namely:
 
   \begin{thm}[Support of Abstractions]\label{suppabs} 
   Assuming @{text x} has finite support, then\\[-6mm] 
@@ -776,7 +777,7 @@
   \end{thm}
 
   \noindent
-  We will show below the first equation as the others 
+  Below we will show the first equation. The others 
   follow similar arguments. By definition of the abstraction type @{text "abs_set"} 
   we have 
   %
@@ -803,9 +804,9 @@
   \end{lemma}
 
   \begin{proof}
-  By using \eqref{abseqiff}, this lemma is straightforward when observing that
-  the assumptions give us @{term "(a \<rightleftharpoons> b) \<bullet> (supp x - as) = (supp x - as)"}
-  and that @{text supp} and set difference are equivariant.
+  This lemma is straightforward by using \eqref{abseqiff} and observing that
+  the assumptions give us @{term "(a \<rightleftharpoons> b) \<bullet> (supp x - as) = (supp x - as)"}.
+  Moreover @{text supp} and set difference are equivariant \cite{HuffmanUrban10}.
   \end{proof}
 
   \noindent
@@ -819,7 +820,7 @@
   which by Property~\ref{supportsprop} gives us ``one half'' of
   Thm~\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 taking an abstraction as argument
+  function taking an abstraction as argument:
   %
   \begin{center}
   @{thm supp_gen.simps[THEN eq_reflection, no_vars]}
@@ -846,19 +847,20 @@
   \noindent
   since for finite sets, @{text "S"}, we have @{thm (concl) supp_finite_atom_set[no_vars]}.
 
-  Finally taking \eqref{halfone} and \eqref{halftwo} together provides us with a proof
-  of Theorem~\ref{suppabs}. The point of these properties of abstractions is that we 
-  can define and prove them aconveniently on the Isabelle/HOL level,
-  but also use them in what follows next when we deal with binding in 
-  specifications of term-calculi. 
+  Finally, taking \eqref{halfone} and \eqref{halftwo} together establishes of
+  Theorem~\ref{suppabs}. This theorem gives us confidence that our
+  abstractions behave as one expects. To consider first abstractions of the
+  form @{term "Abs as x"} is motivated by the fact that properties about them
+  can be conveninetly established at the Isabelle/HOL level.  But we can also
+  use when we deal with binding in our term-calculi specifications.
 *}
 
 section {* Alpha-Equivalence and Free Variables\label{sec:alpha} *}
 
 text {*
-  Our choice of syntax for specifications of term-calculi is influenced by the existing
+  Our choice of syntax for specifications is influenced by the existing
   datatype package of Isabelle/HOL \cite{Berghofer99} and by the syntax of the Ott-tool
-  \cite{ott-jfp}. A specification is a collection of (possibly mutual
+  \cite{ott-jfp}. For us a specification of a term-calculus is a collection of (possibly mutual
   recursive) type declarations, say @{text "ty"}$^\alpha_1$, \ldots, 
   @{text ty}$^\alpha_n$, and an associated collection
   of binding functions, say @{text bn}$^\alpha_1$, \ldots, @{text
@@ -900,7 +902,7 @@
   \noindent
   whereby some of the @{text ty}$'_{1..l}$ (or their components) are 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}.  The labels annotated on
+  corresponding argument a \emph{recursive argument} of @{text "C\<^sup>\<alpha>"}.  The labels 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}:
@@ -925,7 +927,7 @@
   restriction we impose on shallow binders is that the {\it label} must either
   refer to a type that is an atom type or to a type that is a finite set or
   list of an atom type. Two examples for the use of shallow binders are the
-  specification of lambda-terms, where a single name is bound, and of
+  specification of lambda-terms, where a single name is bound, and 
   type-schemes, where a finite set of names is bound:
 
   \begin{center}
@@ -969,12 +971,12 @@
   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 expected to return either a set of atoms
+  The corresponding binding functions are expected to return either a set of atoms
   (for \isacommand{bind\_set} and \isacommand{bind\_res}) or a list of atoms
   (for \isacommand{bind}). They can be defined by primitive recursion over the
   corresponding type; the equations must be given in the binding function part of
-  the scheme shown in \eqref{scheme}. For example for a calculus containing lets 
-  with tuple patterns, you might specify
+  the scheme shown in \eqref{scheme}. For example a term-calculus containing lets 
+  with tuple patterns might be specified as:
 
   \begin{center}
   \begin{tabular}{l}
@@ -999,17 +1001,18 @@
   \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 second last clause the function @{text "atom"}
-  coerces a name into the generic atom type of Nominal Isabelle. This allows
+  coerces a name into the generic atom type of Nominal Isabelle \cite{HuffmanUrban10}. This allows
   us to treat binders of different atom type uniformly. 
 
   As will shortly become clear, we cannot return an atom in a binding function
   that is also bound in the corresponding term-constructor. That means in the
   example above that the term-constructors @{text PVar} and @{text PTup} must not have a
-  binding clause.  In the present version of Nominal Isabelle, we also adopted
+  binding clause.  In the version of Nominal Isabelle described here, we also adopted
   the restriction from the Ott-tool that binding functions can only return:
   the empty set or empty list (as in case @{text PNil}), a singleton set or singleton
   list containing an atom (case @{text PVar}), or unions of atom sets or appended atom
-  lists (case @{text PTup}). This restriction will simplify proofs later on.
+  lists (case @{text PTup}). This restriction will simplify definitions and 
+  proofs later on.
   
   The most drastic restriction we have to impose on deep binders is that 
   we cannot have ``overlapping'' deep binders. Consider for example the 
@@ -1031,8 +1034,7 @@
   In the first case we bind all atoms from the pattern @{text p} in @{text t}
   and also all atoms from @{text q} in @{text t}. As a result we have no way
   to determine whether the binder came from the binding function @{text
-  "bn(p)"} or @{text "bn(q)"}. Similarly in the second case. There the binder
-  @{text "bn(p)"} overlaps with the shallow binder @{text x}. The reason why
+  "bn(p)"} or @{text "bn(q)"}. Similarly in the second case. The reason why
   we must exclude such specifications is that they cannot be represent by
   the general binders described in Section \ref{sec:binders}. However
   the following two term-constructors are allowed
@@ -1053,7 +1055,7 @@
   
   Note that in the last example we wrote {\it\isacommand{bind}\;bn(p)\;\isacommand{in}\;p}.
   Whenever such a binding clause is present, we will call the binder \emph{recursive}.
-  To see the purpose for this, compare ``plain'' Lets and Let\_recs:
+  To see the purpose for such recursive binders, compare ``plain'' @{text "Let"}s and @{text "Let_rec"}s:
   %
   \begin{equation}\label{letrecs}
   \mbox{%
@@ -1075,11 +1077,11 @@
   \end{equation}
 
   \noindent
-  The difference is that with Let we only want to bind the atoms @{text
-  "bn(a)"} in the term @{text t}, but with Let\_rec we also want to bind the atoms
-  inside the assignment. This requires recursive binders and also has
-  consequences for the free variable function and alpha-equivalence relation,
-  which we are going to explain in the rest of this section.
+  The difference is that with @{text Let} we only want to bind the atoms @{text
+  "bn(a)"} 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, which we are going to describe in the 
+  rest of this section.
  
   Having dealt with all syntax matters, the problem now is how we can turn
   specifications into actual type definitions in Isabelle/HOL and then
@@ -1095,8 +1097,8 @@
   The datatype definition can be obtained by stripping off the 
   binding clauses and the labels on 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 user. In our implementation we just use an affix @{text "_raw"}.
-  For the purpose of the paper we just use the superscript @{text "_\<^sup>\<alpha>"} to indicate 
+  given by user. In our implementation we just use the affix @{text "_raw"}.
+  But for the purpose of this paper, we just use the superscript @{text "_\<^sup>\<alpha>"} to indicate 
   that a notion is defined over alpha-equivalence classes and leave it out 
   for the corresponding notion defined on the ``raw'' level. So for example 
   we have
@@ -1106,7 +1108,9 @@
   \end{center}
   
   \noindent
-  
+  where the type @{term ty} is the type used in the quotient construction for 
+  @{text "ty\<^sup>\<alpha>"} and @{text "C"} is the term-constructor on the ``raw'' type @{text "ty"}. 
+
   The resulting datatype definition is legal in Isabelle/HOL provided the datatypes are 
   non-empty and the types in the constructors only occur in positive 
   position (see \cite{Berghofer99} for an indepth description of the datatype package
@@ -1135,7 +1139,7 @@
   \end{center}
 
   \noindent
-  We define them together with auxiliary free variable functions for
+  We define them together with auxiliary free-variable functions for
   the binding functions. Given binding functions 
   @{text "bn_ty\<^isub>1 \<dots> bn_ty\<^isub>m"} we need to define
   %
@@ -1145,17 +1149,16 @@
 
   \noindent
   The reason for this setup is that in a deep binder not all atoms have to be
-  bound. While the idea behind these free variable functions is just to
-  collect all atoms that are not bound, because of the rather complicated
-  binding mechanisms their definitions are somewhat involved.
+  bound, as we shall see in an example below. While the idea behind these
+  free-variable functions is clear (they just collect all atoms that are not bound),
+  because of the rather complicated binding mechanisms their definitions are
+  somewhat involved.
 
   Given a term-constructor @{text "C"} of type @{text ty} with argument types
-  \mbox{@{text "ty\<^isub>1 \<dots> ty\<^isub>n"}} and given some binding clauses associated with 
-  this constructor, the function
+  \mbox{@{text "ty\<^isub>1 \<dots> ty\<^isub>n"}}, the function
   @{text "fv_ty (C x\<^isub>1 \<dots> x\<^isub>n)"} will be the union of the values
-  calculated below for each argument. 
-
-  First we deal with the case @{text "x\<^isub>i"} is a binder. From the binding clauses, 
+  calculated next for each argument. 
+  First we deal with the case that @{text "x\<^isub>i"} is a binder. From the binding clauses, 
   we can determine whether the argument is a shallow or deep
   binder, and in the latter case also whether it is a recursive or
   non-recursive binder. 
@@ -1172,8 +1175,8 @@
 
   \noindent
   The first clause states that shallow binders do not contribute to the
-  free variables; in the second clause, we have to look up all
-  the free variables that are left unbound by the binding function @{text "bn_ty\<^isub>i"}---this
+  free variables; in the second clause, we have to collect all
+  variables that are left unbound by the binding function @{text "bn_ty\<^isub>i"}---this
   is done with function @{text "fv_bn_ty\<^isub>i"}; in the third clause, since the 
   binder is recursive, we need to bind all variables specified by 
   @{text "bn_ty\<^isub>i"}---therefore we subtract @{text "bn_ty\<^isub>i x\<^isub>i"} from the free
@@ -1182,12 +1185,13 @@
   In case the argument is \emph{not} a binder, we need to consider 
   whether the @{text "x\<^isub>i"} is the body of one or more binding clauses. 
   In this case we first calculate the set @{text "bnds"} as follows: 
-  either the binders are all shallow or there is a single deep binder.
+  either the corresponding binders are all shallow or there is a single deep binder.
   In the former case we take @{text bnds} to be the union of all shallow 
   binders; in the latter case, we just take the set of atoms specified by the 
   binding function. The value for @{text "x\<^isub>i"} is then given by:
 
-  \begin{center}
+  \begin{equation}\label{deepbody}
+  \mbox{%
   \begin{tabular}{c@ {\hspace{2mm}}p{7cm}}
   $\bullet$ & @{text "{atom x\<^isub>i} - bnds"} provided @{term "x\<^isub>i"} is an atom\\
   $\bullet$ & @{text "(atoms x\<^isub>i) - bnds"} provided @{term "x\<^isub>i"} is a set of atoms\\
@@ -1195,23 +1199,25 @@
   $\bullet$ & @{text "(fv_ty\<^isub>i x\<^isub>i) - bnds"} provided @{term "ty\<^isub>i"} is one of the raw datatypes
      corresponding to the types specified by the user\\
 %  $\bullet$ & @{text "(fv\<^isup>\<alpha> x\<^isub>i) - bnds"} provided @{term "x\<^isub>i"} is a defined nominal datatype
-%     with a free variable function @{text "fv\<^isup>\<alpha>"}\\
+%     with a free-variable function @{text "fv\<^isup>\<alpha>"}\\
   $\bullet$ & @{term "{}"} otherwise
-  \end{tabular}
-  \end{center}
+  \end{tabular}}
+  \end{equation}
 
   \noindent 
-  Like the function @{text atom}, @{text "atoms"} coerces a set of atoms to the generic atom type.
+  Like the coercion function @{text atom} used above, @{text "atoms as"} coerces 
+  the set @{text as} to the generic atom type.
   It is defined as @{text "atom as \<equiv> {atom a | a \<in> as}"}.
 
   The last case we need to consider is when @{text "x\<^isub>i"} is neither
   a binder nor a body of an abstraction. In this case it is defined 
-  as above, except that we do not subtract the set @{text bnds}.
+  as in \eqref{deepbody}, except that we do not need to subtract the 
+  set @{text bnds}.
   
-  Next, we need to define a free variable function @{text "fv_bn_ty\<^isub>i"} for 
+  Next, we need to define a free-variable function @{text "fv_bn_ty\<^isub>i"} for 
   each binding function @{text "bn_ty\<^isub>i"}. The idea behind this
   function is to compute the set of free atoms that are not bound by 
-  the binding function. Because of the restrictions we imposed on the 
+  @{text "bn_ty\<^isub>i"}. Because of the restrictions we imposed on the 
   form of binding functions, this can be done automatically by recursively 
   building up the the set of free variables from the arguments that are 
   not bound. Let us assume one clause of the binding function is 
@@ -1222,7 +1228,7 @@
   \begin{center}
   \begin{tabular}{c@ {\hspace{2mm}}p{7cm}}
   \multicolumn{2}{l}{@{text "x\<^isub>j"} occurs in @{text "rhs"}:}\\ 
-  $\bullet$ & @{term "{}"} provided @{term "x\<^isub>j"} is an atom,
+  $\bullet$ & @{term "{}"} provided @{term "x\<^isub>j"} is a single atom,
      atom list or atom set\\
   $\bullet$ & @{text "fv_bn_ty\<^isub>j x\<^isub>j"} in case @{text "rhs"} contains the 
   recursive call @{text "bn_ty\<^isub>j x\<^isub>j"}\\[1mm]
@@ -1233,16 +1239,16 @@
   $\bullet$ & @{text "fv_ty\<^isub>j x\<^isub>j"} provided @{term "ty\<^isub>j"} is one of the raw
      types corresponding to the types specified by the user\\
 %  $\bullet$ & @{text "fv_ty\<^isup>\<alpha> x\<^isub>j - bnds"} provided @{term "x\<^isub>j"}  is not in @{text "rhs"}
-%     and is an existing nominal datatype with the free variable function @{text "fv\<^isup>\<alpha>"}\\
+%     and is an existing nominal datatype with the free-variable function @{text "fv\<^isup>\<alpha>"}\\
   $\bullet$ & @{term "{}"} otherwise
   \end{tabular}
   \end{center}
 
   \noindent
-  To see how these definitions work, let us consider the term-constructors 
-  for @{text "Let"} and @{text "Let_rec"} from example shown in \eqref{letrecs}. 
+  To see how these definitions work, let us consider again the term-constructors 
+  @{text "Let"} and @{text "Let_rec"} from example shown in \eqref{letrecs}. 
   For this specification we need to define three functions, namely
-  @{text "fv\<^bsub>trm\<^esub>"}, @{text "fv\<^bsub>assn\<^esub>"} and @{text "fv\<^bsub>bn\<^esub>"}. 
+  @{text "fv\<^bsub>trm\<^esub>"}, @{text "fv\<^bsub>assn\<^esub>"} and @{text "fv\<^bsub>bn\<^esub>"}. They are as follows:
   %
   \begin{center}
   \begin{tabular}{@ {}l@ {\hspace{1mm}}c@ {\hspace{1mm}}l@ {}}
@@ -1262,65 +1268,82 @@
   Since there are no binding clauses for the term-constructors @{text ANil}
   and @{text "ACons"}, the corresponding free-variable function @{text
   "fv\<^bsub>assn\<^esub>"} returns all atoms occuring in an assignment. The
-  binding happens in @{text Let} and @{text "Let_rec"}. In the first clause we
-  want to bind all atoms given by @{text "set (bn as)"} in @{text
-  t}. Therefore we have to subtract @{text "set (bn as)"} from @{text
+  binding only takes place in @{text Let} and @{text "Let_rec"}. In the @{text
+  "Let"}-clause we want to bind all atoms given by @{text "set (bn as)"} in
+  @{text t}. Therefore we have to subtract @{text "set (bn as)"} from @{text
   "fv\<^bsub>trm\<^esub> t"}. However, we also need to add all atoms that are
   free in @{text "as"}. This is what the purpose of the function @{text
   "fv\<^bsub>bn\<^esub>"} is.  In contrast, in @{text "Let_rec"} we have a
-  recursive binder where we want to also bind all occurences of atoms inside
-  @{text "as"}. Therefore we have to subtract @{text "set (bn as)"} from
-  @{text "fv\<^bsub>assn\<^esub> as"}. Similarly for @{text
-  "fv\<^bsub>trm\<^esub> t - bn as"}. An interesting point in this example is
+  recursive binder where we want to also bind all occurences of the atoms
+  @{text "bn as"} inside @{text "as"}. Therefore we have to subtract @{text
+  "set (bn as)"} from @{text "fv\<^bsub>assn\<^esub> as"}, as well as from
+  @{text "fv\<^bsub>trm\<^esub> t"}. An interesting point in this example is
   that an assignment ``alone'' does not have any bound variables. Only in the
-  context of a @{text Let} pr @{text "Let_rec"} will some atoms occuring in an
-  assignment become bound. This is a phenomenon that has also been pointed out
-  in \cite{ott-jfp}.
+  context of a @{text Let} or @{text "Let_rec"} will some atoms become bound
+  (teh term-constructors that have binding clauses).  This is a phenomenon 
+  that has also been pointed out in \cite{ott-jfp}.
 
-  We then define the alpha equivalence relations. For the types @{text "ty\<^isub>1, \<dots>, ty\<^isub>n"}
-  we need to define
+  Next we define alpha-equivalence realtions for the types @{text "ty\<^isub>1, \<dots>, ty\<^isub>n"}. We call them
+  @{text "\<approx>ty\<^isub>1 \<dots> \<approx>ty\<^isub>n"}. Like with the free-variable functions, 
+  we also need to  define auxiliary alpha-equivalence relations for the binding functions. 
+  Say we have @{text "bn_ty\<^isub>1 \<dots> bn_ty\<^isub>m"}, we also define @{text "\<approx>bn_ty\<^isub>1 \<dots> \<approx>bn_ty\<^isub>n"}.
+
+  The relations are inductively defined predicates, whose clauses have
+  conclusions of the form  @{text "C x\<^isub>1 \<dots> x\<^isub>n \<approx>ty C y\<^isub>1 \<dots> y\<^isub>n"} (let us assume 
+  @{text C} is of type @{text ty} and its arguments are specified as @{text "C ty\<^isub>1 \<dots> ty\<^isub>n"}).
+  The task is to specify what the premises of these clauses are. For this we
+  consider the pairs @{text "(x\<^isub>i, y\<^isub>i)"} which necesarily must have the same type, say
+  @{text "ty\<^isub>i"}. For each of these pairs we calculate a premise as follows. 
 
   \begin{center}
-  @{text "\<approx>\<^isub>1 :: ty\<^isub>1 \<Rightarrow> ty\<^isub>1 \<Rightarrow> bool \<dots> \<approx>\<^isub>n :: ty\<^isub>n \<Rightarrow> ty\<^isub>n \<Rightarrow> bool"}
+  \begin{tabular}{c@ {\hspace{2mm}}p{7cm}}
+  \multicolumn{2}{l}{@{text "x\<^isub>i"} is a binder:}\\
+  $\bullet$ & @{text "True"} provided @{text "x\<^isub>i"} is a shallow binder\\
+  $\bullet$ & @{text "x\<^isub>i \<approx>bn_ty\<^isub>i y\<^isub>i"} provided @{text "x\<^isub>i"} is a deep 
+     non-recursive binder\\
+  $\bullet$ & @{text "True"} provided @{text "x\<^isub>i"} is a deep 
+     recursive binder\\
+  \end{tabular}
   \end{center}
 
-  \noindent
-  together with the auxiliary equivalences for binding functions. Given binding
-  functions for types @{text "bn\<^isub>1 :: ty\<^isub>i\<^isub>1 \<Rightarrow> \<dots> \<dots> bn\<^isub>m :: ty\<^isub>i\<^isub>m \<Rightarrow> \<dots>"} we need to define
+  TODO BELOW
+
   \begin{center}
-  @{text "\<approx>bn\<^isub>1 :: ty\<^isub>i\<^isub>1 \<Rightarrow> ty\<^isub>i\<^isub>1 \<Rightarrow> bool \<dots> \<approx>bn\<^isub>n :: ty\<^isub>i\<^isub>m \<Rightarrow> ty\<^isub>i\<^isub>m \<Rightarrow> bool"}
+  \begin{tabular}{c@ {\hspace{2mm}}p{7cm}}
+  \multicolumn{2}{l}{@{text "x\<^isub>i"} is a body where the binding clause has mode \isacommand{bind}:}\\
+  $\bullet$ & @{text "\<exists>p. (bnds_x\<^isub>i, x\<^isub>i) \<approx>lst (\<approx>ty\<^isub>i) fv_ty\<^isub>i p (bnds_y\<^isub>i, y\<^isub>j)"} 
+     provided @{text "x\<^isub>i"} has only shallow binders; in this case @{text "bnds_x\<^isub>i"} is the
+     union of all these shallow binders (similarly for @{text "bnds_y\<^isub>i"}\\
+  $\bullet$ & @{text "\<exists>p. (bn_ty\<^isub>j x\<^isub>j, x\<^isub>i) \<approx>lst (\<approx>ty\<^isub>i) fv_ty\<^isub>i p (bn_ty y\<^isub>j, y\<^isub>i)"} 
+     provided @{text "x\<^isub>i"} is a body with a deep non-recursive binder @{text x\<^isub>j}
+     (similarly @{text "y\<^isub>j"} is the deep non-recursive binder for @{text "y\<^isub>i"})\\ 
+  $\bullet$ & @{text "\<exists>p (bn_ty\<^isub>i x\<^isub>i, (x\<^isub>j, x\<^isub>n)) \<approx>lst R fvs \<pi> (bn\<^isub>m y\<^isub>j, (y\<^isub>j, y\<^isub>n))"}
+     provided @{text "x\<^isub>j"} is a deep recursive binder with the auxiliary binding
+     function @{text "bn\<^isub>m"} and permutation @{text "\<pi>"}, @{term "fvs"} is a compound
+     free variable function returning the union of appropriate @{term "fv_ty\<^isub>x"} and
+     @{term "R"} is the composition of equivalence relations @{text "\<approx>"} and @{text "\<approx>\<^isub>n"}\\
+  $\bullet$ & @{text "x\<^isub>j"} has a deep recursive binding\\
+  $\bullet$ & @{text "({x\<^isub>n}, x\<^isub>j) \<approx>gen R fv_ty \<pi> ({y\<^isub>n}, y\<^isub>j)"} provided @{text "x\<^isub>j"} has
+     a shallow binder @{text "x\<^isub>n"} with permutation @{text "\<pi>"}, @{term "R"} is the
+     alpha-equivalence for @{term "x\<^isub>j"}
+     and @{term "fv_ty"} is the free-variable function for @{term "x\<^isub>j"}\\
+  $\bullet$ & @{text "(bn\<^isub>m x\<^isub>n, x\<^isub>j) \<approx>gen R fv_ty \<pi> (bn\<^isub>m y\<^isub>n, y\<^isub>j)"} provided @{text "x\<^isub>j"}
+     has a deep non-recursive binder @{text "bn\<^isub>m x\<^isub>n"} with permutation @{text "\<pi>"}, @{term "R"} is the
+     alpha-equivalence for @{term "x\<^isub>j"}
+     and @{term "fv_ty"} is the free-variable function for @{term "x\<^isub>j"}\\
+  $\bullet$ & @{text "x\<^isub>j \<approx>\<^isub>j y\<^isub>j"} provided @{term "x\<^isub>j"} is one of the types being
+     defined\\
+  $\bullet$ & @{text "x\<^isub>j = y\<^isub>j"} otherwise\\
+  \end{tabular}
   \end{center}
 
-  Given a term-constructor @{text "C ty\<^isub>1 \<dots> ty\<^isub>n"}, of a type @{text ty}, two instances
+  , of a type @{text ty}, two instances
   of this constructor are alpha-equivalent @{text "C x\<^isub>1 \<dots> x\<^isub>n \<approx> C y\<^isub>1 \<dots> y\<^isub>n"} if there
   exist permutations @{text "\<pi>\<^isub>1 \<dots> \<pi>\<^isub>p"} (one for each bound argument) such that
   the conjunction of equivalences defined below for each argument pair @{text "x\<^isub>j"}, @{text "y\<^isub>j"} holds.
   For an argument pair @{text "x\<^isub>j"}, @{text "y\<^isub>j"} this holds if:
 
-  \begin{center}
-  \begin{tabular}{cp{7cm}}
-  $\bullet$ & @{text "x\<^isub>j"} is a shallow binder\\
-  $\bullet$ & @{text "x\<^isub>j \<approx>bn\<^isub>m y\<^isub>j"} provided @{text "x\<^isub>j"} is a deep non-recursive binder
-     with the auxiliary binding function @{text "bn\<^isub>m"}\\
-  $\bullet$ & @{term "(bn\<^isub>m x\<^isub>j, (x\<^isub>j, x\<^isub>n)) \<approx>gen R fvs \<pi> (bn\<^isub>m y\<^isub>j, (y\<^isub>j, y\<^isub>n))"}
-     provided @{term "x\<^isub>j"} is a deep recursive binder with the auxiliary binding
-     function @{text "bn\<^isub>m"} and permutation @{text "\<pi>"}, @{term "fvs"} is a compound
-     free variable function returning the union of appropriate @{term "fv_ty\<^isub>x"} and
-     @{term "R"} is the composition of equivalence relations @{text "\<approx>"} and @{text "\<approx>\<^isub>n"}\\
-  $\bullet$ & @{text "x\<^isub>j"} has a deep recursive binding\\
-  $\bullet$ & @{term "({x\<^isub>n}, x\<^isub>j) \<approx>gen R fv_ty \<pi> ({y\<^isub>n}, y\<^isub>j)"} provided @{text "x\<^isub>j"} has
-     a shallow binder @{text "x\<^isub>n"} with permutation @{text "\<pi>"}, @{term "R"} is the
-     alpha-equivalence for @{term "x\<^isub>j"}
-     and @{term "fv_ty"} is the free variable function for @{term "x\<^isub>j"}\\
-  $\bullet$ & @{term "(bn\<^isub>m x\<^isub>n, x\<^isub>j) \<approx>gen R fv_ty \<pi> (bn\<^isub>m y\<^isub>n, y\<^isub>j)"} provided @{text "x\<^isub>j"}
-     has a deep non-recursive binder @{text "bn\<^isub>m x\<^isub>n"} with permutation @{text "\<pi>"}, @{term "R"} is the
-     alpha-equivalence for @{term "x\<^isub>j"}
-     and @{term "fv_ty"} is the free variable function for @{term "x\<^isub>j"}\\
-  $\bullet$ & @{text "x\<^isub>j \<approx>\<^isub>j y\<^isub>j"} provided @{term "x\<^isub>j"} is one of the types being
-     defined\\
-  $\bullet$ & @{text "x\<^isub>j = y\<^isub>j"} otherwise\\
-  \end{tabular}
-  \end{center}
+  
 
   The alpha-equivalence relations for binding functions are similar to the alpha-equivalences
   for their respective types, the difference is that they ommit checking the arguments that




