diff -r 9807d30c0e54 -r 09b476c20fe1 Paper/Paper.thy
--- a/Paper/Paper.thy	Wed Jul 07 13:13:18 2010 +0100
+++ b/Paper/Paper.thy	Fri Jul 09 10:00:37 2010 +0100
@@ -623,7 +623,7 @@
   vacuous binders.) To answer this question, we identify four conditions: {\it (i)}
   given a free-atom function @{text "fa"} of type \mbox{@{text "\<beta> \<Rightarrow> atom
   set"}}, then @{text x} and @{text y} need to have the same set of free
-  atomss; moreover there must be a permutation @{text p} such that {\it
+  atoms; moreover there must be a permutation @{text p} such that {\it
   (ii)} @{text p} 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,
   say \mbox{@{text "_ R _"}}, two equivalent terms. We also require that {\it (iv)}
@@ -950,7 +950,7 @@
   the ones of Ott. The
   main idea behind these restrictions is that we obtain a sensible notion of
   $\alpha$-equivalence where it is ensured that within a given scope an 
-  atom occurence cannot be both bound and free at the same time.  The first
+  atom occurrence cannot be both bound and free at the same time.  The first
   restriction is that a body can only occur in
   \emph{one} binding clause of a term constructor (this ensures that the bound
   atoms of a body cannot be free at the same time by specifying an
@@ -1087,9 +1087,9 @@
 
   \noindent
   Otherwise it is possible that @{text "bn\<^isub>1"} and @{text "bn\<^isub>2"}  pick 
-  out different atoms to become bound, respectively be free, in @{text "p"}
-  (since the Ott-tool does not derive a reasoning for $\alpha$-equated terms, it can permit 
-  such specifications).
+  out different atoms to become bound, respectively be free, in @{text "p"}.
+  (Since the Ott-tool does not derive a reasoning for $\alpha$-equated terms, it can permit 
+  such specifications.)
   
   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 
@@ -1170,9 +1170,9 @@
 
   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
-  in Isabelle/HOL). We then define each of the user-specified binding 
-  function @{term "bn\<^isub>i"} by recursion over the corresponding 
+  position (see \cite{Berghofer99} for an in-depth description of the datatype package
+  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 can also easily define permutation operations by 
   recursion so that for each term constructor @{text "C"} we have that
   %
@@ -1181,7 +1181,7 @@
   \end{equation}
 
   The first non-trivial step we have to perform is the generation of
-  free-atom functions from the specifications. For the 
+  free-atom functions from the specification. For the 
   \emph{raw} types @{text "ty"}$_{1..n}$ we define the free-atom functions
   %
   \begin{equation}\label{fvars}
@@ -1201,7 +1201,7 @@
   \noindent
   The reason for this setup is that in a deep binder not all atoms have to be
   bound, as we saw in the example with ``plain'' @{text Let}s. We need therefore a function
-  that calculates those unbound atoms in a deep binder.
+  that calculates those free atoms in a deep binder.
 
   While the idea behind these free-atom functions is clear (they just
   collect all atoms that are not bound), because of our rather complicated
@@ -1209,41 +1209,43 @@
   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
   "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 define below what @{text "fa"} for a binding
+  "fa(bc\<^isub>1) \<union> \<dots> \<union> fa(bc\<^isub>k)"} where we will define below what @{text "fa"} for a binding
   clause means. We only show the details for the mode \isacommand{bind\_set} (the other modes are similar). 
   Suppose the binding clause @{text bc\<^isub>i} is of the form 
   %
-  \begin{equation}
+  \begin{center}
   \mbox{\isacommand{bind\_set} @{text "b\<^isub>1\<dots>b\<^isub>p"} \isacommand{in} @{text "d\<^isub>1\<dots>d\<^isub>q"}}
-  \end{equation}
+  \end{center}
 
   \noindent
   in which the body-labels @{text "d"}$_{1..q}$ refer to types @{text ty}$_{1..q}$,
   and the binders @{text b}$_{1..p}$
   either refer to labels of atom types (in case of shallow binders) or to binding 
-  functions taking a single label as argument (in case of deep binders). Assuming the
-  set @{text "D"} stands for the free atoms in the bodies, the set @{text B} for the 
-  binding atoms in the binders and @{text "B'"} for the free atoms in 
+  functions taking a single label as argument (in case of deep binders). Assuming 
+  @{text "D"} stands for the set of free atoms of the bodies, @{text B} for the 
+  set of binding atoms in the binders and @{text "B'"} for the set of free atoms in 
   non-recursive deep binders,
-  then the free atoms of the binding clause @{text bc\<^isub>i} are given by
+  then the free atoms of the binding clause @{text bc\<^isub>i} are
   %
-  \begin{center}
-  @{text "fa(bc\<^isub>i) \<equiv> (D - B) \<union> B'"}
-  \end{center}
+  \begin{equation}\label{fadef}
+  \mbox{@{text "fa(bc\<^isub>i) \<equiv> (D - B) \<union> B'"}}.
+  \end{equation}
 
   \noindent
-  whereby the set @{text D} is formally defined as
+  The set @{text D} is formally defined as
   %
   \begin{center}
   @{text "D \<equiv> fa_ty\<^isub>1 d\<^isub>1 \<union> ... \<union> fa_ty\<^isub>q d\<^isub>q"}
   \end{center} 
 
   \noindent
-  The functions @{text "fa_ty\<^isub>i"} are the ones we are defining by recursion 
-  (see \eqref{fvars}) in case the @{text "d\<^isub>i"} refers to one of the raw types 
-  @{text "ty"}$_{1..n}$ from the specification; otherwise we set @{text "fa_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
+  where in case @{text "d\<^isub>i"} refers to one of the raw types @{text "ty"}$_{1..n}$ from the 
+  specification, the function @{text "fa_ty\<^isub>i"} is the corresponding free-atom function 
+  we are defining by recursion 
+  (see \eqref{fvars}); otherwise we set @{text "fa_ty\<^isub>i d\<^isub>i = supp d\<^isub>i"}.
+  
+  In order to formally define the set @{text B} we use the following auxiliary @{text "bn"}-functions
+  for atom types to which shallow binders may refer
   %
   \begin{center}
   \begin{tabular}{r@ {\hspace{2mm}}c@ {\hspace{2mm}}l}
@@ -1254,8 +1256,8 @@
   \end{center}
 
   \noindent 
-  The function @{text "atoms"} coerces 
-  the set of atoms to a set of the generic atom type. It is defined as 
+  Like the function @{text atom}, the function @{text "atoms"} coerces 
+  a set of atoms to a set of the generic atom type. It is defined as 
   @{text "atoms as \<equiv> {atom a | a \<in> as}"}. 
   The set @{text B} is then formally defined as
   %
@@ -1264,28 +1266,30 @@
   \end{center} 
 
   \noindent 
+  where we use the auxiliary binding functions for shallow binders. 
   The set @{text "B'"} collects all free atoms in non-recursive deep
   binders. Let us assume these binders in @{text "bc\<^isub>i"} are
   %
   \begin{center}
-  @{text "bn\<^isub>1 a\<^isub>1, \<dots>, bn\<^isub>r a\<^isub>r"}
+  @{text "bn\<^isub>1 l\<^isub>1, \<dots>, bn\<^isub>r l\<^isub>r"}
   \end{center}
 
   \noindent
-  with none of the @{text "a"}$_{1..r}$ being among the bodies @{text
+  with none of the @{text "l"}$_{1..r}$ being among the bodies @{text
   "d"}$_{1..q}$. The set @{text "B'"} is defined as
   %
   \begin{center}
-  @{text "B' \<equiv> fa_bn\<^isub>1 a\<^isub>1 \<union> ... \<union> fa_bn\<^isub>r a\<^isub>r"}
+  @{text "B' \<equiv> fa_bn\<^isub>1 l\<^isub>1 \<union> ... \<union> fa_bn\<^isub>r l\<^isub>r"}
   \end{center} 
 
   \noindent
-  This completes the definition of the free-atom functions.
+  This completes the definition of the free-atom functions @{text "fa_ty"}$_{1..n}$.
 
-  Note that for non-recursive deep binders, we have to add all atoms that are left 
-  unbound by the binding function @{text "bn"} (the set @{text "B'"}). We use for this 
-  the functions @{text "fa_bn"}, also defined by recursion. Assume the user specified 
-  a @{text bn}-clause of the form
+  Note that for non-recursive deep binders, we have to add in \eqref{fadef}
+  the set of atoms that are left unbound by the binding functions @{text
+  "bn"}$_{1..m}$. We use for the definition of
+  this set the functions @{text "fa_bn"}$_{1..m}$, which are also defined by mutual
+  recursion. Assume the user specified a @{text bn}-clause of the form
   %
   \begin{center}
   @{text "bn (C z\<^isub>1 \<dots> z\<^isub>s) = rhs"}
@@ -1298,7 +1302,7 @@
   \begin{center}
   \begin{tabular}{c@ {\hspace{2mm}}p{7cm}}
   $\bullet$ & @{term "fa_ty\<^isub>i z\<^isub>i"} provided @{text "z\<^isub>i"} does not occur in @{text "rhs"} 
-  (that means nothing is bound in @{text "z\<^isub>i"}),\\
+  (that means nothing is bound in @{text "z\<^isub>i"} by the binding function),\\
   $\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"}, and\\
   $\bullet$ & @{term "{}"} provided @{text "z\<^isub>i"} occurs in  @{text "rhs"},
@@ -1307,13 +1311,15 @@
   \end{center}
 
   \noindent
-  For defining @{text "fa_bn (C z\<^isub>1 \<dots> z\<^isub>n)"} we just union up all these values.
+  For defining @{text "fa_bn (C z\<^isub>1 \<dots> z\<^isub>n)"} we just union up all these sets.
  
-  To see how these definitions work in practice, let us reconsider the term-constructors 
-  @{text "Let"} and @{text "Let_rec"}, as well as @{text "ANil"} and @{text "ACons"} 
-  from the example shown in \eqref{letrecs}. 
-  For them we define three free-atom functions, namely
-  @{text "fa\<^bsub>trm\<^esub>"}, @{text "fa\<^bsub>assn\<^esub>"} and @{text "fa\<^bsub>bn\<^esub>"} as follows:
+  To see how these definitions work in practice, let us reconsider the
+  term-constructors @{text "Let"} and @{text "Let_rec"} shown in
+  \eqref{letrecs} together with the term-constructors for assignments @{text
+  "ANil"} and @{text "ACons"}. Since there is a binding function defined for
+  assignments, we have three free-atom functions, namely @{text
+  "fa\<^bsub>trm\<^esub>"}, @{text "fa\<^bsub>assn\<^esub>"} and @{text
+  "fa\<^bsub>bn\<^esub>"} as follows:
   %
   \begin{center}
   \begin{tabular}{@ {}l@ {\hspace{1mm}}c@ {\hspace{1mm}}l@ {}}
@@ -1329,30 +1335,37 @@
   \end{center}
 
   \noindent
-  To see the pattern, recall that @{text ANil} and @{text "ACons"} have no
+  For these definitions, recall that @{text ANil} and @{text "ACons"} have no
   binding clause in the specification. The corresponding free-atom
-  function @{text "fa\<^bsub>assn\<^esub>"} therefore returns all atoms
-  occurring in an assignment. The binding only takes place in @{text Let} and
-  @{text "Let_rec"}. In the @{text "Let"}-clause, the binding clause specifies
+  function @{text "fa\<^bsub>assn\<^esub>"} therefore returns all free atoms
+  occurring in an assignment (in case of @{text "ACons"}, they are given by 
+  calls to @{text supp}, @{text "fa\<^bsub>trm\<^esub>"} and @{text "fa\<^bsub>assn\<^esub>"}). 
+  The binding only takes place in @{text Let} and
+  @{text "Let_rec"}. In case of @{text "Let"}, the binding clause specifies
   that all atoms given by @{text "set (bn as)"} have to be bound in @{text
   t}. Therefore we have to subtract @{text "set (bn as)"} from @{text
   "fa\<^bsub>trm\<^esub> t"}. However, we also need to add all atoms that are
-  free in @{text "as"}.  In contrast, in @{text "Let_rec"} we have a recursive
-  binder where we want to also bind all occurrences of the atoms in @{text
+  free in @{text "as"}. This is
+  in contrast with @{text "Let_rec"} where we have a recursive
+  binder to bind all occurrences of the atoms in @{text
   "set (bn as)"} also inside @{text "as"}. Therefore we have to subtract
-  @{text "set (bn as)"} from the union @{text "fa\<^bsub>trm\<^esub> t"} and @{text "fa\<^bsub>assn\<^esub> as"}. 
-  
+  @{text "set (bn as)"} from both @{text "fa\<^bsub>trm\<^esub> t"} and @{text "fa\<^bsub>assn\<^esub> as"}. 
+  Like the function @{text "bn"}, the function @{text "fa\<^bsub>bn\<^esub>"} traverses the 
+  list of assignments, but instead returns the free atoms, that means in this 
+  example the free atoms in the argument @{text "t"}.  
+
   An interesting point in this
-  example is that a ``naked'' assignment does not bind any
-  atoms. Only in the context of a @{text Let} or @{text "Let_rec"} will
-  some atoms from an assignment become bound.  This is a phenomenon that has also been pointed
+  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 actually become bound.  This is a phenomenon that has also been pointed
   out in \cite{ott-jfp}. For us this observation is crucial, because we would 
-  not be able to lift the @{text "bn"}-function if it was defined over assignments 
-  where some atoms are bound. In that case @{text "bn"} would \emph{not} respect
+  not be able to lift the @{text "bn"}-functions to $\alpha$-equated terms if they act on 
+  atoms that are bound. In that case, these functions would \emph{not} respect
   $\alpha$-equivalence.
 
-  Next we define $\alpha$-equivalence relations for the raw types @{text
-  "ty"}$_{1..n}$. We write them 
+  Next we define the $\alpha$-equivalence relations for the raw types @{text
+  "ty"}$_{1..n}$ from the specification. We write them as
   %
   \begin{center}
   @{text "\<approx>ty\<^isub>1, \<dots>, \<approx>ty\<^isub>n"}. 
@@ -1369,33 +1382,162 @@
   \noindent
   for the binding functions @{text "bn"}$_{1..m}$, 
   To simplify our definitions we will use the following abbreviations for
-  equivalence relations and free-atom functions acting on pairs
-
+  \emph{compound equivalence relations} and \emph{compound free-atom functions} acting on tuples
   %
   \begin{center}
   \begin{tabular}{r@ {\hspace{2mm}}c@ {\hspace{2mm}}l}
-  @{text "(x\<^isub>1, y\<^isub>1) (R\<^isub>1 \<otimes> R\<^isub>2) (x\<^isub>2, y\<^isub>2)"} & @{text "\<equiv>"} & @{text "x\<^isub>1 R\<^isub>1 y\<^isub>1 \<and> x\<^isub>2 R\<^isub>2 y\<^isub>2"}\\
-  @{text "(fa\<^isub>1 \<oplus> fa\<^isub>2) (x, y)"} & @{text "\<equiv>"} & @{text "fa\<^isub>1 x \<union> fa\<^isub>2 y"}\\
+  @{text "(x\<^isub>1,.., x\<^isub>n) (R\<^isub>1,.., R\<^isub>n) (x\<PRIME>\<^isub>1,.., x\<PRIME>\<^isub>n)"} & @{text "\<equiv>"} & \\
+  \multicolumn{3}{r}{@{text "x\<^isub>1 R\<^isub>1 x\<PRIME>\<^isub>1 \<and> .. \<and> x\<^isub>n R\<^isub>n x\<PRIME>\<^isub>n"}}\\
+  @{text "(fa\<^isub>1,.., fa\<^isub>n) (x\<^isub>1,.., x\<^isub>n)"} & @{text "\<equiv>"} & @{text "fa\<^isub>1 x\<^isub>1 \<union> .. \<union> fa\<^isub>n x\<^isub>n"}\\
   \end{tabular}
   \end{center}
 
 
-  The relations for $\alpha$-equivalence are inductively defined 
-  predicates, whose clauses have the form  
+  The $\alpha$-equivalence relations are defined as inductive predicates
+  having a single clause for each term-constructor. Assuming a
+  term-constructor @{text C} is of type @{text ty} and has the binding clauses
+  @{term "bc"}$_{1..k}$, then the $\alpha$-equivalence clause has the form
   %
   \begin{center}
   \mbox{\infer{@{text "C z\<^isub>1 \<dots> z\<^isub>n  \<approx>ty  C z\<PRIME>\<^isub>1 \<dots> z\<PRIME>\<^isub>n"}}
-  {@{text "prems(bc\<^isub>1) \<and> \<dots> \<and> prems(bc\<^isub>k)"}}} 
+  {@{text "prems(bc\<^isub>1) \<dots> prems(bc\<^isub>k)"}}} 
+  \end{center}
+
+  \noindent
+  The task below is to specify what the premises of a binding clause are. As a
+  special instance, we first treat the case where @{text "bc\<^isub>i"} is the
+  empty binding clause of the form
+  %
+  \begin{center}
+  \mbox{\isacommand{bind\_set} @{term "{}"} \isacommand{in} @{text "d\<^isub>1\<dots>d\<^isub>q"}.}
+  \end{center}
+
+  \noindent
+  In this binding clause no atom is bound and we only have to $\alpha$-relate the bodies. For this
+  we build first the tuples @{text "D \<equiv> (d\<^isub>1,\<dots>, d\<^isub>q)"} and @{text "D' \<equiv> (d\<PRIME>\<^isub>1,\<dots>, d\<PRIME>\<^isub>q)"}  
+  whereby the labels @{text "d"}$_{1..q}$ refer to arguments @{text "z"}$_{1..n}$ and
+  respectively @{text "d\<PRIME>"}$_{1..q}$ to @{text "z\<PRIME>"}$_{1..n}$. In order to relate
+  two such tuples we define the compound $\alpha$-equivalence relation @{text "R"} as follows
+  %
+  \begin{equation}\label{rempty}
+  \mbox{@{text "R \<equiv> (R\<^isub>1,\<dots>, R\<^isub>q)"}}
+  \end{equation}
+
+  \noindent
+  with @{text "R\<^isub>i"} being @{text "\<approx>ty\<^isub>i"} if the corresponding labels @{text "d\<^isub>i"} and 
+  @{text "d\<PRIME>\<^isub>i"} refer
+  to a recursive argument of @{text C} with type @{text "ty\<^isub>i"}; otherwise
+  we take @{text "R\<^isub>i"} to be the equality @{text "="}. This lets us define
+  the premise for an empty binding clause succinctly as @{text "prems(bc\<^isub>i) \<equiv> D R D'"},
+  which can be unfolded to the series of premises
+  %
+  \begin{center}
+  @{text "d\<^isub>1 R\<^isub>1 d\<PRIME>\<^isub>1  \<dots> d\<^isub>q R\<^isub>q d\<PRIME>\<^isub>q"}
+  \end{center}
+
+  \noindent
+  We will use the unfolded version in the examples below.
+
+  Now suppose the binding clause @{text "bc\<^isub>i"} is of the general form 
+  %
+  \begin{equation}\label{nonempty}
+  \mbox{\isacommand{bind\_set} @{text "b\<^isub>1\<dots>b\<^isub>p"} \isacommand{in} @{text "d\<^isub>1\<dots>d\<^isub>q"}.}
+  \end{equation}
+
+  \noindent
+  In this case we define a premise @{text P} using the relation
+  $\approx_{\,\textit{set}}$ given in Section~\ref{sec:binders} (similarly
+  $\approx_{\,\textit{res}}$ and $\approx_{\,\textit{list}}$ for the other
+  binding modes). This premise defines $\alpha$-equivalence of two abstractions
+  involving multiple binders. We first define as above the tuples @{text "D"} and
+  @{text "D'"} for the bodies @{text "d"}$_{1..q}$, and the corresponding
+  compound $\alpha$-relation @{text "R"} (shown in \eqref{rempty}). 
+  For $\approx_{\,\textit{set}}$ we also need
+  a compound free-atom function for the bodies defined as
+  %
+  \begin{center}
+  \mbox{@{text "fa \<equiv> (fa_ty\<^isub>1,\<dots>, fa_ty\<^isub>q)"}}
+  \end{center}
+
+  \noindent
+  with assumption that the @{text "d"}$_{1..q}$ refer to arguments of types @{text "ty"}$_{1..q}$.
+  The last ingredient we need are the sets of atoms bound in the bodies.
+  For this we take
+
+  \begin{center}
+  @{text "B \<equiv> bn_ty\<^isub>1 b\<^isub>1 \<union> \<dots> \<union> bn_ty\<^isub>p b\<^isub>p"}\;.\\
   \end{center}
 
   \noindent
-  assuming the term-constructor @{text C} is of type @{text ty} and has
-  the binding clauses @{term "bc"}$_{1..k}$.  The task
-  is to specify what the premises of these clauses are. Again for this we
-  analyse the binding clauses and produce a corresponding premise.
+  Similarly for @{text "B'"} using the labels @{text "b\<PRIME>"}$_{1..p}$. This 
+  lets us formally define the premise @{text P} for a non-empty binding clause as:
+  %
+  \begin{equation}\label{pprem}
+  \mbox{@{term "P \<equiv> \<exists>p. (B, D) \<approx>gen R fa p (B', D')"}}\;.
+  \end{equation}
+
+  \noindent
+  This premise accounts for $\alpha$-equivalence of the bodies of the binding
+  clause. However, in case the binders have non-recursive deep binders, then
+  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 the
+  relations @{text "\<approx>bn"}$_{1..m}$ (which we will formally define shortly).
+  Let us assume the non-recursive deep binders in @{text "bc\<^isub>i"} are
+  %
+  \begin{center}
+  @{text "bn\<^isub>1 l\<^isub>1, \<dots>, bn\<^isub>r l\<^isub>r"}.
+  \end{center}
+
+  \noindent
+  The premises for @{text "bc\<^isub>i"} are then defined as
+  %
+  \begin{center}
+  @{text "prems(bc\<^isub>i) \<equiv> P  \<and>  l\<^isub>1 \<approx>bn\<^isub>1 l\<PRIME>\<^isub>1  \<and> ... \<and>  l\<^isub>r \<approx>bn\<^isub>r l\<PRIME>\<^isub>r"}
+  \end{center} 
+
+  \noindent
+  where @{text "P"} is defined in \eqref{pprem}. 
+ 
+  The $\alpha$-equivalence relations @{text "\<approx>bn"}$_{1..m}$ are defined as follows:
+  given a @{text bn}-clause of the form
+  %
+  \begin{center}
+  @{text "bn (C z\<^isub>1 \<dots> z\<^isub>s) = rhs"}
+  \end{center}
+
+  \noindent
+  where the @{text "z"}$_{1..s}$ are of types @{text "ty"}$_{1..s}$,
+  then the $\alpha$-equivalence clause for @{text "\<approx>bn"} has the form
+  %
+  \begin{center}
+  \mbox{\infer{@{text "C z\<^isub>1 \<dots> z\<^isub>s \<approx>bn C z\<PRIME>\<^isub>1 \<dots> z\<PRIME>\<^isub>s"}}
+  {@{text "z\<^isub>1 R\<^isub>1 z\<PRIME>\<^isub>1 \<dots> z\<^isub>s R\<^isub>s z\<PRIME>\<^isub>s"}}}
+  \end{center}
+  
+  \noindent
+  whereby the relations @{text "R"}$_{1..s}$ are given by 
+
+  \begin{center}
+  \begin{tabular}{c@ {\hspace{2mm}}p{7cm}}
+  $\bullet$ & @{text "z\<^isub>i \<approx>ty z\<PRIME>\<^isub>i"} provided @{text "z\<^isub>i"} does not occur in @{text rhs} and 
+  is a recursive argument of @{text C},\\
+  $\bullet$ & @{text "z\<^isub>i = z\<PRIME>\<^isub>i"} provided @{text "z\<^isub>i"} does not occur in @{text rhs}
+  and is a non-recursive argument of @{text C},\\
+  $\bullet$ & @{text "z\<^isub>i \<approx>bn\<^isub>i z\<PRIME>\<^isub>i"} provided @{text "z\<^isub>i"} occurs in @{text rhs}
+  with the recursive call @{text "bn\<^isub>i x\<^isub>i"} and\\
+  $\bullet$ & @{text True} provided @{text "z\<^isub>i"} occurs in @{text rhs} but without a
+  recursive call.
+  \end{tabular}
+  \end{center}
+
+  \noindent
+  This completes the definition of $\alpha$-equivalence. As a sanity check, we can show
+  that the premises of empty binding clauses are a special case of the clauses for 
+  non-empty ones (we just have to unfold the definition of $\approx_{\,\textit{set}}$ and take @{text "0"}
+  as the permutation).
 *}
-(*<*)
-consts alpha_ty ::'a
+(*<*)consts alpha_ty ::'a
 consts alpha_trm ::'a
 consts fa_trm :: 'a
 consts alpha_trm2 ::'a
@@ -1405,77 +1547,16 @@
   alpha_trm ("\<approx>\<^bsub>trm\<^esub>") and
   fa_trm ("fa\<^bsub>trm\<^esub>") and
   alpha_trm2 ("\<approx>\<^bsub>assn\<^esub> \<otimes> \<approx>\<^bsub>trm\<^esub>") and
-  fa_trm2 ("fa\<^bsub>assn\<^esub> \<oplus> fa\<^bsub>trm\<^esub>") 
-(*>*)
+  fa_trm2 ("fa\<^bsub>assn\<^esub> \<oplus> fa\<^bsub>trm\<^esub>")(*>*)
 text {*
-  *TBD below *
-
-  \begin{equation}\label{alpha}
-  \mbox{%
-  \begin{tabular}{c@ {\hspace{2mm}}p{7cm}}
-  \multicolumn{2}{@ {}l}{Empty binding clauses of the form 
-  \isacommand{bind\_set}~@{term "{}"}~\isacommand{in}~@{text "x\<^isub>i"}:}\\ 
-  $\bullet$ & @{text "x\<^isub>i \<approx>ty y\<^isub>i"} provided @{text "x\<^isub>i"} and @{text "y\<^isub>i"} 
-  are recursive arguments of @{text "C"}\\
-  $\bullet$ & @{term "x\<^isub>i = y\<^isub>i"} provided @{text "x\<^isub>i"} and @{text "y\<^isub>i"} are 
-  non-recursive arguments\smallskip\\
-  \multicolumn{2}{@ {}l}{Shallow binders of the form 
-  \isacommand{bind\_set}~@{text "x\<^isub>1\<dots>x\<^isub>n"}~\isacommand{in}~@{text "x'\<^isub>1\<dots>x'\<^isub>m"}:}\\ 
-  $\bullet$ & Assume the bodies @{text "x'\<^isub>1\<dots>x'\<^isub>m"} are of type @{text "ty\<^isub>1\<dots>ty\<^isub>m"},
-  @{text "R"} is @{text "\<approx>ty\<^isub>1 \<otimes> ... \<otimes> \<approx>ty\<^isub>m"} and @{text fa} is
-  @{text "fa_ty\<^isub>1 \<oplus> ... \<oplus> fa_ty\<^isub>m"}, then
-  \begin{center}
-  @{term "\<exists>p. (x\<^isub>1 \<union> \<xi> \<union> x\<^isub>n, (x'\<^isub>1,\<xi>,x'\<^isub>m)) \<approx>gen R fa p (y\<^isub>1 \<union> \<xi> \<union> y\<^isub>n, (y'\<^isub>1,\<xi>,y'\<^isub>m))"}
-  \end{center}\\
-  \multicolumn{2}{@ {}l}{Deep binders of the form 
-  \isacommand{bind\_set}~@{text "bn x"}~\isacommand{in}~@{text "x'\<^isub>1\<dots>x'\<^isub>m"}:}\\ 
-  $\bullet$ & Assume the bodies @{text "x'\<^isub>1\<dots>x'\<^isub>m"} are of type @{text "ty\<^isub>1\<dots>ty\<^isub>m"},
-  @{text "R"} is @{text "\<approx>ty\<^isub>1 \<otimes> ... \<otimes> \<approx>ty\<^isub>m"} and @{text fa} is
-  @{text "fa_ty\<^isub>1 \<oplus> ... \<oplus> fa_ty\<^isub>m"}, then for recursive deep binders
-  \begin{center}
-  @{term "\<exists>p. (bn x, (x'\<^isub>1,\<xi>,x'\<^isub>m)) \<approx>gen R fa p (bn y, (y'\<^isub>1,\<xi>,y'\<^isub>m))"}
-  \end{center}\\
-  $\bullet$ & for non-recursive binders we generate in addition @{text "x \<approx>bn y"}\\
-  \end{tabular}}
-  \end{equation}
-
-  \noindent
-  Similarly for the other binding modes.
-  From this definition it is clear why we have to impose the restriction
-  of excluding overlapping deep binders, as these would need to be translated into separate
-  abstractions.
-
-
-
-  The $\alpha$-equivalence relations @{text "\<approx>bn\<^isub>j"} for binding functions 
-  are similar. We again have conclusions of the form \mbox{@{text "C x\<^isub>1 \<dots> x\<^isub>n \<approx>bn C y\<^isub>1 \<dots> y\<^isub>n"}}
-  and need to generate appropriate premises. We generate first premises according to the first three
-  rules given above. Only the ``left-over'' pairs  @{text "(x\<^isub>i, y\<^isub>i)"} need to be treated 
-  differently. They depend on whether @{text "x\<^isub>i"}  occurs in @{text "rhs"} of  the 
-  clause @{text "bn (C x\<^isub>1 \<dots> x\<^isub>n) = rhs"}:
-
-  \begin{center}
-  \begin{tabular}{c@ {\hspace{2mm}}p{7cm}}
-  $\bullet$ & @{text "x\<^isub>i \<approx>ty y\<^isub>i"} provided @{text "x\<^isub>i"} does not occur in @{text rhs}
-  and the type of @{text "x\<^isub>i"} is @{text ty} and @{text "x\<^isub>i"} is a recursive argument 
-  in the term-constructor\\
-  $\bullet$ & @{text "x\<^isub>i = y\<^isub>i"} provided @{text "x\<^isub>i"} does not occur in @{text rhs}
-  and @{text "x\<^isub>i"} is not a recursive argument in the term-constructor\\
-  $\bullet$ & @{text "x\<^isub>i \<approx>bn y\<^isub>i"} provided @{text "x\<^isub>i"} occurs in @{text rhs}
-  with the recursive call @{text "bn x\<^isub>i"}\\
-  $\bullet$ & none provided @{text "x\<^isub>i"} occurs in @{text rhs} but it is not
-  in a recursive call involving a @{text "bn"}
-  \end{tabular}
-  \end{center}
-
   Again lets take a look at a concrete example for these definitions. For \eqref{letrecs}
-  we have three relations, namely $\approx_{\textit{trm}}$, $\approx_{\textit{assn}}$ and
-  $\approx_{\textit{bn}}$, with the clauses as follows:
+  we have three relations $\approx_{\textit{trm}}$, $\approx_{\textit{assn}}$ and
+  $\approx_{\textit{bn}}$ with the following clauses:
 
   \begin{center}
   \begin{tabular}{@ {}c @ {}}
   \infer{@{text "Let as t \<approx>\<^bsub>trm\<^esub> Let as' t'"}}
-  {@{text "as \<approx>\<^bsub>bn\<^esub> as'"} & @{term "\<exists>p. (bn as, t) \<approx>lst alpha_trm fa_trm p (bn as', t')"}}\smallskip\\
+  {@{term "\<exists>p. (bn as, t) \<approx>lst alpha_trm fa_trm p (bn as', t')"} & @{text "as \<approx>\<^bsub>bn\<^esub> as'"}}\smallskip\\
   \infer{@{text "Let_rec as t \<approx>\<^bsub>trm\<^esub> Let_rec as' t'"}}
   {@{term "\<exists>p. (bn as, (as, t)) \<approx>lst alpha_trm2 fa_trm2 p (bn as', (as', t'))"}}
   \end{tabular}