
diff -r 4df720c9b660 -r 4baa2fccfb61 LMCS-Paper/Paper.thy
--- a/LMCS-Paper/Paper.thy	Fri Sep 09 11:52:24 2011 +0100
+++ b/LMCS-Paper/Paper.thy	Fri Sep 09 17:11:38 2011 +0100
@@ -15,6 +15,17 @@
 definition
  "equal \<equiv> (op =)" 
 
+fun alpha_set_ex where
+  "alpha_set_ex (bs, x) R f (cs, y) = (\<exists>pi. alpha_set (bs, x) R f pi (cs, y))"
+ 
+fun alpha_res_ex where
+  "alpha_res_ex (bs, x) R f pi (cs, y) = (\<exists>pi. alpha_res (bs, x) R f pi (cs, y))"
+
+fun alpha_lst_ex where
+  "alpha_lst_ex (bs, x) R f pi (cs, y) = (\<exists>pi. alpha_lst (bs, x) R f pi (cs, y))"
+
+
+
 notation (latex output)
   swap ("'(_ _')" [1000, 1000] 1000) and
   fresh ("_ # _" [51, 51] 50) and
@@ -22,9 +33,9 @@
   supp ("supp _" [78] 73) and
   uminus ("-_" [78] 73) and
   If  ("if _ then _ else _" 10) and
-  alpha_set ("_ \<approx>\<^raw:\,\raisebox{-1pt}{\makebox[0mm][l]{$_{\textit{set}}$}}>\<^bsup>_, _, _\<^esup> _") and
-  alpha_lst ("_ \<approx>\<^raw:\,\raisebox{-1pt}{\makebox[0mm][l]{$_{\textit{list}}$}}>\<^bsup>_, _, _\<^esup> _") and
-  alpha_res ("_ \<approx>\<^raw:\,\raisebox{-1pt}{\makebox[0mm][l]{$_{\textit{set+}}$}}>\<^bsup>_, _, _\<^esup> _") and
+  alpha_set_ex ("_ \<approx>\<^raw:\,\raisebox{-1pt}{\makebox[0mm][l]{$_{\textit{set}}$}}>\<^bsup>_, _\<^esup> _") and
+  alpha_lst_ex ("_ \<approx>\<^raw:\,\raisebox{-1pt}{\makebox[0mm][l]{$_{\textit{list}}$}}>\<^bsup>_, _\<^esup> _") and
+  alpha_res_ex ("_ \<approx>\<^raw:\,\raisebox{-1pt}{\makebox[0mm][l]{$_{\textit{set+}}$}}>\<^bsup>_, _\<^esup> _") and
   abs_set ("_ \<approx>\<^raw:{$\,_{\textit{abs\_set}}$}> _") and
   abs_set2 ("_ \<approx>\<^raw:\raisebox{-1pt}{\makebox[0mm][l]{$\,_{\textit{list}}$}}>\<^bsup>_\<^esup>  _") and
   fv ("fa'(_')" [100] 100) and
@@ -657,7 +668,8 @@
 
   \begin{defi}[Alpha-Equivalence for Set-Bindings]\label{alphaset}\mbox{}\\
   \begin{tabular}{@ {\hspace{10mm}}l@ {\hspace{5mm}}rl}  
-  @{term "(as, x) \<approx>set R fa \<pi> (bs, y)"}\hspace{2mm}@{text "\<equiv>"} 
+  @{term "alpha_set_ex (as, x) R fa (bs, y)"}\hspace{2mm}@{text "\<equiv>"} & 
+    \multicolumn{2}{@ {}l}{if there exists a @{text "\<pi>"} such that:}\\ 
        & \mbox{\it (i)}   & @{term "fa(x) - as = fa(y) - bs"}\\
        & \mbox{\it (ii)}  & @{term "(fa(x) - as) \<sharp>* \<pi>"}\\
        & \mbox{\it (iii)} &  @{text "(\<pi> \<bullet> x) R y"} \\
@@ -666,9 +678,7 @@
   \end{defi}
  
   \noindent
-  Note that this relation depends on the permutation @{text
-  "\<pi>"}; alpha-equivalence between two pairs is then the relation where we
-  existentially quantify over this @{text "\<pi>"}. Also note that the relation is
+  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}}$ for both ``raw'' terms and alpha-equated terms. In
@@ -682,7 +692,8 @@
   
   \begin{defi}[Alpha-Equivalence for List-Bindings]\label{alphalist}\mbox{}\\
   \begin{tabular}{@ {\hspace{10mm}}l@ {\hspace{5mm}}rl}  
-  @{term "(as, x) \<approx>lst R fa \<pi> (bs, y)"}\hspace{2mm}@{text "\<equiv>"}
+  @{term "alpha_lst_ex (as, x) R fa (bs, y)"}\hspace{2mm}@{text "\<equiv>"} &
+  \multicolumn{2}{@ {}l}{if there exists a @{text "\<pi>"} such that:}\\ 
          & \mbox{\it (i)}   & @{term "fa(x) - (set as) = fa(y) - (set bs)"}\\ 
          & \mbox{\it (ii)}  & @{term "(fa(x) - set as) \<sharp>* \<pi>"}\\
          & \mbox{\it (iii)} & @{text "(\<pi> \<bullet> x) R y"}\\
@@ -701,7 +712,8 @@
 
   \begin{defi}[Alpha-Equivalence for Set+-Bindings]\label{alphares}\mbox{}\\
   \begin{tabular}{@ {\hspace{10mm}}l@ {\hspace{5mm}}rl}  
-  @{term "(as, x) \<approx>res R fa \<pi> (bs, y)"}\hspace{2mm}@{text "\<equiv>"}
+  @{term "alpha_res_ex (as, x) R fa (bs, y)"}\hspace{2mm}@{text "\<equiv>"} &
+  \multicolumn{2}{@ {}l}{if there exists a @{text "\<pi>"} such that:}\\ 
              & \mbox{\it (i)}   & @{term "fa(x) - as = fa(y) - bs"}\\
              & \mbox{\it (ii)}  & @{term "(fa(x) - as) \<sharp>* \<pi>"}\\
              & \mbox{\it (iii)} & @{text "(\<pi> \<bullet> x) R y"}\\
@@ -737,24 +749,25 @@
   shown that all three notions of alpha-equivalence coincide, if we only
   abstract a single atom.
 
-  In the rest of this section we are going to introduce three abstraction 
-  types. For this we define the relations
+  In the rest of this section we are going to show that the alpha-equivalences really 
+  lead to abstractions where some atoms are bound.  For this we are going to introduce 
+  three abstraction types that are quotients with respect to the relations
 
   \begin{equation}
   \begin{array}{r}
-  @{term "alpha_abs_set (as, x) (bs, y) \<equiv> \<exists>\<pi>. alpha_set (as, x) equal supp \<pi> (bs, y)"}\\
-  @{term "alpha_abs_res (as, x) (bs, y) \<equiv> \<exists>\<pi>. alpha_res (as, x) equal supp \<pi> (bs, y)"}\\
-  @{term "alpha_abs_lst (as, x) (bs, y) \<equiv> \<exists>\<pi>. alpha_lst (as, x) equal supp \<pi> (bs, y)"}\\
+  @{term "alpha_abs_set (as, x) (bs, y)"}~~@{text "\<equiv>"}~~@{term "alpha_set_ex (as, x) equal supp (bs, y)"}\\
+  @{term "alpha_abs_res (as, x) (bs, y)"}~~@{text "\<equiv>"}~~@{term "alpha_res_ex (as, x) equal supp (bs, y)"}\\
+  @{term "alpha_abs_lst (as, x) (bs, y)"}~~@{text "\<equiv>"}~~@{term "alpha_lst_ex (as, x) equal supp (bs, y)"}\\
   \end{array}
   \end{equation}\smallskip
   
   \noindent
-  We can show that these relations are equivalence 
-  relations and equivariant.
+  In these relation we replaced the free-atom function @{text "fa"} with @{term "supp"} and the 
+  relation @{text R} with equality. We can show the following properties:
 
   \begin{lem}\label{alphaeq} 
-  The relations $\approx_{\,\textit{abs\_set}}$, $\approx_{\,\textit{abs\_list}}$
-  and $\approx_{\,\textit{abs\_set+}}$ are equivalence relations and equivariant. 
+  The relations $\approx_{\,\textit{abs\_set}}$, $\approx_{\,\textit{abs\_set+}}$
+  and $\approx_{\,\textit{abs\_list}}$ are equivalence relations and equivariant. 
   \end{lem}
 
   \begin{proof}
@@ -763,10 +776,10 @@
   of transitivity, we have two permutations @{text "\<pi>\<^isub>1"} and @{text "\<pi>\<^isub>2"}, and for the
   proof obligation use @{text "\<pi>\<^isub>1 + \<pi>\<^isub>2"}. Equivariance means
   @{term "abs_set (\<pi> \<bullet> as, \<pi> \<bullet> x) (\<pi> \<bullet> bs, \<pi> \<bullet> y)"} holds provided 
-  @{term "abs_set (as, x) (bs, y)"}. To show this, we need to unfold the
+  \mbox{@{term "abs_set (as, x) (bs, y)"}} holds. To show this, we need to unfold the
   definitions and `pull out' the permutations, which is possible since all
   operators, such as @{text "#\<^sup>*, -, set"} and @{text "supp"}, are equivariant
-  (see \cite{HuffmanUrban10}).
+  (see \cite{HuffmanUrban10}). Finally we apply the permutation operation on booleans.
   \end{proof}
 
   \noindent
@@ -803,15 +816,17 @@
   \end{thm}
 
   \noindent
-  In effect, this theorem states that the bound names do not appear in the support
-  of abstractions. This can be seen as test that our Definitions \ref{alphaset}, \ref{alphalist}
-  and \ref{alphares} capture the idea of alpha-equivalence relations. 
-  Below we will show the first equation of Theorem \ref{suppabs}. The others follow by similar
-  arguments. By definition of the abstraction type @{text "abs\<^bsub>set\<^esub>"} we have
+  In effect, this theorem states that the atoms @{text "as"} are bound in the
+  abstraction. As stated earlier, this can be seen as test that our
+  Definitions \ref{alphaset}, \ref{alphalist} and \ref{alphares} capture the
+  idea of alpha-equivalence relations. Below we will give the proof for the
+  first equation of Theorem \ref{suppabs}. The others follow by similar
+  arguments. By definition of the abstraction type @{text
+  "abs\<^bsub>set\<^esub>"} we have
 
   \begin{equation}\label{abseqiff}
   @{thm (lhs) Abs_eq_iff(1)[where bs="as" and cs="bs", no_vars]} \;\;\;\text{if and only if}\;\;\; 
-  @{term "\<exists>\<pi>. alpha_set (as, x) equal supp \<pi> (bs, y)"}
+  @{term "alpha_set_ex (as, x) equal supp (bs, y)"}
   \end{equation}\smallskip
   
   \noindent
@@ -836,6 +851,7 @@
   \begin{proof}
   This lemma is straightforward using \eqref{abseqiff} and observing that
   the assumptions give us @{term "(a \<rightleftharpoons> b) \<bullet> (supp x - as) = (supp x - as)"}.
+  We therefore can use as permutation the swapping @{term "(a \<rightleftharpoons> b)"}.
   \end{proof}
   
   \noindent
@@ -867,7 +883,7 @@
   \]\smallskip
   
   \noindent
-  using fact about function applications in \eqref{supps}. Assuming 
+  using the fact about the support of function applications in \eqref{supps}. Assuming 
   @{term "supp x - as"} is a finite set, we further obtain
   
   \begin{equation}\label{halftwo}
@@ -875,7 +891,7 @@
   \end{equation}\smallskip
   
   \noindent
-  since for every finite sets of atoms, say @{text "bs"}, we have 
+  This is because for every finite sets of atoms, say @{text "bs"}, we have 
   @{thm (concl) supp_finite_atom_set[where S="bs", no_vars]}.
   Finally, taking \eqref{halfone} and \eqref{halftwo} together establishes 
   Theorem~\ref{suppabs}. 
@@ -898,7 +914,7 @@
   collection of (possibly mutual recursive) type declarations, say @{text
   "ty\<AL>\<^isub>1, \<dots>, ty\<AL>\<^isub>n"}, and an associated collection of
   binding functions, say @{text "bn\<AL>\<^isub>1, \<dots>, bn\<AL>\<^isub>m"}. The
-  syntax in Nominal Isabelle for such specifications is roughly as follows:
+  syntax in Nominal Isabelle for such specifications is schematically as follows:
   
   \begin{equation}\label{scheme}
   \mbox{\begin{tabular}{@ {}p{2.5cm}l}
@@ -910,7 +926,7 @@
   \raisebox{2mm}{$\ldots$}\\[-2mm] 
   \isacommand{and} @{text "ty\<AL>\<^isub>n = \<dots>"}\\ 
   \end{tabular}}
-  \end{cases}$\\
+  \end{cases}$\\[2mm]
   binding \mbox{function part} &
   $\begin{cases}
   \mbox{\begin{tabular}{l}
@@ -986,9 +1002,17 @@
   that we obtain a sensible notion of alpha-equivalence where it is ensured
   that within a given scope an 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 alternative
-  binder for the same body).
+  \emph{one} binding clause of a term constructor. So for example
+
+  \[\mbox{
+  @{text "Foo x::name y::name t::trm"}\hspace{3mm}  
+  \isacommand{binds} @{text "x"} \isacommand{in} @{text "t"},
+  \isacommand{binds} @{text "y"} \isacommand{in} @{text "t"}}
+  \]\smallskip
+
+  \noindent
+  is not allowed. This ensures that the bound atoms of a body cannot be free
+  at the same time by specifying an alternative binder for the same body.
 
   For binders we distinguish between \emph{shallow} and \emph{deep} binders.
   Shallow binders are just labels. The restriction we need to impose on them
@@ -1021,9 +1045,9 @@
 
   \noindent
   In these specifications @{text "name"} refers to an atom type, and @{text
-  "fset"} to the type of finite sets.  Note that for @{text lam} it does not
+  "fset"} to the type of finite sets.  Note that for @{text Lam} it does not
   matter which binding mode we use. The reason is that we bind only a single
-  @{text name}. However, having \isacommand{binds (set)} or \isacommand{binds}
+  @{text name}. However, having \isacommand{binds (set)} or just \isacommand{binds}
   in the second case makes a difference to the semantics of the specification
   (which we will define in the next section).
 
@@ -1108,16 +1132,16 @@
   To make sure that atoms bound by deep binders cannot be free at the
   same time, we cannot have more than one binding function for a deep binder. 
   Consequently we exclude specifications such as
-  %
-  \begin{center}
+
+  \[\mbox{
   \begin{tabular}{@ {}l@ {\hspace{2mm}}l@ {}}
   @{text "Baz\<^isub>1 p::pat t::trm"} & 
      \isacommand{binds} @{text "bn\<^isub>1(p) bn\<^isub>2(p)"} \isacommand{in} @{text t}\\
   @{text "Baz\<^isub>2 p::pat t\<^isub>1::trm t\<^isub>2::trm"} & 
      \isacommand{binds} @{text "bn\<^isub>1(p)"} \isacommand{in} @{text "t\<^isub>1"},
      \isacommand{binds} @{text "bn\<^isub>2(p)"} \isacommand{in} @{text "t\<^isub>2"}\\
-  \end{tabular}
-  \end{center}
+  \end{tabular}}
+  \]\smallskip
 
   \noindent
   Otherwise it is possible that @{text "bn\<^isub>1"} and @{text "bn\<^isub>2"}  pick 
@@ -1125,24 +1149,45 @@
   (Since the Ott-tool does not derive a reasoning infrastructure for 
   alpha-equated terms with deep binders, 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 
-  terms. The main restriction is that we cannot return an atom in a binding function that is also
-  bound in the corresponding term-constructor. That means in \eqref{letpat} 
-  that the term-constructors @{text PVar} and @{text PTup} may
-  not have a binding clause (all arguments are used to define @{text "bn"}).
-  In contrast, in case of \eqref{letrecs} the term-constructor @{text ACons}
-  may have a binding clause involving the argument @{text trm} (the only one that
-  is \emph{not} used in the definition of the binding function). This restriction
-  is sufficient for lifting the binding function to alpha-equated terms.
+  We also need to restrict the form of the binding functions in order to
+  ensure the @{text "bn"}-functions can be defined for alpha-equated
+  terms. The main restriction is that we cannot return an atom in a binding
+  function that is also bound in the corresponding term-constructor.
+  Consider again the specification for @{text "trm"} and a contrived
+  version for assignments, @{text "assn"}:
 
-  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 some automatic definitions and proofs
-  later on.
+  \begin{equation}\label{bnexp}
+  \mbox{%
+  \begin{tabular}{@ {}l@ {}}
+  \isacommand{nominal\_datatype}~@{text "trm ="}~\ldots\\
+  \isacommand{and} @{text "assn"} $=$\\
+  \hspace{5mm}\phantom{$\mid$}~@{text "ANil"}\\
+  \hspace{5mm}$\mid$~@{text "ACons x::name y::name t::trm assn"}
+     \;\;\isacommand{binds} @{text "y"} \isacommand{in} @{text t}\\
+  \isacommand{binder} @{text "bn::assn \<Rightarrow> atom list"}\\
+  \isacommand{where}~@{text "bn(ANil) = []"}\\
+  \hspace{5mm}$\mid$~@{text "bn(ACons x y t as) = [atom x] @ bn(as)"}\\
+  \end{tabular}}
+  \end{equation}\smallskip
+
+  \noindent
+  In this example the term constructor @{text "ACons"} contains a binding 
+  clause, and also is used in the definition of the binding function. The
+  restriction we have to impose is that the binding function can only return
+  free atoms, that is the ones that are not mentioned in a binding clause.
+  Therefore @{text "y"} cannot be used in the binding function, @{text "bn"}
+  (since it is bound in @{text "ACons"} by the binding clause), but @{text x}
+  can (since it is a free atom). This restriction is sufficient for lifting 
+  the binding function to alpha-equated terms. If we would allow that @{text "bn"}
+  can return also @{text "y"}, then it would not be respectful and therefore
+  cannot be lifted.
+
+  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 ANil}), a singleton set or
+  singleton list containing an atom (case @{text PVar} in \eqref{letpat}), or
+  unions of atom sets or appended atom lists (case @{text ACons}). This
+  restriction will simplify some automatic definitions and proofs later on.
   
   In order to simplify our definitions of free atoms and alpha-equivalence, 
   we shall assume specifications 
@@ -1152,7 +1197,7 @@
   clause, written \isacommand{binds}~@{term "{}"}~\isacommand{in}~@{text "labels"}. In case
   of the lambda-terms, the completion produces
 
-  \begin{center}
+  \[\mbox{
   \begin{tabular}{@ {}l@ {\hspace{-1mm}}}
   \isacommand{nominal\_datatype} @{text lam} =\\
   \hspace{5mm}\phantom{$\mid$}~@{text "Var x::name"}
@@ -1161,8 +1206,8 @@
     \;\;\isacommand{binds}~@{term "{}"}~\isacommand{in}~@{text "t\<^isub>1 t\<^isub>2"}\\
   \hspace{5mm}$\mid$~@{text "Lam x::name t::lam"}
     \;\;\isacommand{binds}~@{text x} \isacommand{in} @{text t}\\
-  \end{tabular}
-  \end{center}
+  \end{tabular}}
+  \]\smallskip
 
   \noindent 
   The point of completion is that we can make definitions over the binding
@@ -1174,16 +1219,16 @@
 text {*
   Having dealt with all syntax matters, the problem now is how we can turn
   specifications into actual type definitions in Isabelle/HOL and then
-  establish a reasoning infrastructure for them. As
-  Pottier and Cheney pointed out \cite{Pottier06,Cheney05}, just 
-  re-arranging the arguments of
-  term-constructors so that binders and their bodies are next to each other will 
-  result in inadequate representations in cases like @{text "Let x\<^isub>1 = t\<^isub>1\<dots>x\<^isub>n = t\<^isub>n in s"}. 
-  Therefore we will first
-  extract ``raw'' datatype definitions from the specification and then define 
-  explicitly an alpha-equivalence relation over them. We subsequently
+  establish a reasoning infrastructure for them. As Pottier and Cheney pointed
+  out \cite{Cheney05,Pottier06}, just re-arranging the arguments of
+  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
+  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 
   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>"}
@@ -1203,18 +1248,22 @@
   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
-  %
+  
   \begin{equation}\label{ceqvt}
-  @{text "p \<bullet> (C z\<^isub>1 \<dots> z\<^isub>n) = C (p \<bullet> z\<^isub>1) \<dots> (p \<bullet> z\<^isub>n)"}
-  \end{equation}
+  @{text "\<pi> \<bullet> (C z\<^isub>1 \<dots> z\<^isub>n) = C (\<pi> \<bullet> z\<^isub>1) \<dots> (\<pi> \<bullet> z\<^isub>n)"}
+  \end{equation}\smallskip
 
   The first non-trivial step we have to perform is the generation of
-  free-atom functions from the specification. For the 
+  \emph{free-atom functions} from the specification.\footnote{Admittedly, the
+  details of our definitions are somewhat involved. However they are still
+  conceptually simple in comparison with the ``positional'' approach taken in
+  Ott \cite[Pages 88--95]{ott-jfp}, which uses \emph{occurences} and
+  \emph{partial equivalence relations} over sets of occurences.} For the
   \emph{raw} types @{text "ty"}$_{1..n}$ we define the free-atom functions
-  
+
   \begin{equation}\label{fvars}
   \mbox{@{text "fa_ty"}$_{1..n}$}
-  \end{equation}
+  \end{equation}\smallskip
   
   \noindent
   by recursion.
@@ -1222,9 +1271,9 @@
   the binding functions. Given raw binding functions @{text "bn"}$_{1..m}$ 
   we define
   
-  \begin{center}
-  @{text "fa_bn"}$_{1..m}$.
-  \end{center}
+  \[
+  @{text "fa_bn"}\mbox{$_{1..m}$}.
+  \]\smallskip
   
   \noindent
   The reason for this setup is that in a deep binder not all atoms have to be
@@ -1241,110 +1290,111 @@
   clause means. We only show the details for the mode \isacommand{binds (set)} (the other modes are similar). 
   Suppose the binding clause @{text bc\<^isub>i} is of the form 
   
-  \begin{center}
+  \[
   \mbox{\isacommand{binds (set)} @{text "b\<^isub>1\<dots>b\<^isub>p"} \isacommand{in} @{text "d\<^isub>1\<dots>d\<^isub>q"}}
-  \end{center}
+  \]\smallskip
   
   \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 
-  @{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\\[-2mm]
-  %
+  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 @{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
+
   \begin{equation}\label{fadef}
   \mbox{@{text "fa(bc\<^isub>i) \<equiv> (D - B) \<union> B'"}}.
-  \end{equation}
-  %
+  \end{equation}\smallskip
+  
   \noindent
   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} 
+  \]\smallskip
   
   \noindent
   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"}.
+  we are defining by recursion; otherwise we set \mbox{@{text "fa_ty\<^isub>i d\<^isub>i = supp d\<^isub>i"}}. The reason
+  for the latter choice is that @{text "ty"}$_i$ is not a type that is part of the specification, and
+  we assume @{text supp} is the generic notion that characterises the free variables of 
+  a type (in fact in the next section we will show that the free-variable functions we
+  define here, are equal to the support once lifted to alpha-equivalence classes).
   
   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\\[-4mm]
   
-  \begin{center}
+  \[\mbox{
   \begin{tabular}{r@ {\hspace{2mm}}c@ {\hspace{2mm}}l}
-  @{text "bn_atom a"} & @{text "\<equiv>"} & @{text "{atom a}"}\\
-  @{text "bn_atom_set as"} & @{text "\<equiv>"} & @{text "atoms as"}\\
-  @{text "bn_atom_list as"} & @{text "\<equiv>"} & @{text "atoms (set as)"}
-  \end{tabular}
-  \end{center}
+  @{text "bn\<^bsub>atom\<^esup> a"} & @{text "\<equiv>"} & @{text "{atom a}"}\\
+  @{text "bn\<^bsub>atom_set\<^esup> as"} & @{text "\<equiv>"} & @{text "atoms as"}\\
+  @{text "bn\<^bsub>atom_list\<^esub> as"} & @{text "\<equiv>"} & @{text "atoms (set as)"}
+  \end{tabular}}
+  \]\smallskip
   
-  \begin{center}
-  @{text "bn\<^bsub>atom\<^esub> a \<equiv> {atom a}"}\hfill
-  @{text "bn\<^bsub>atom_set\<^esub> as \<equiv> atoms as"}\hfill
-  @{text "bn\<^bsub>atom_list\<^esub> as \<equiv> atoms (set as)"}
-  \end{center}
-  %
   \noindent 
   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\\[-4mm]
-  %
-  \begin{center}
+  The set @{text B} is then formally defined as
+  
+  \begin{equation}\label{bdef}
   @{text "B \<equiv> bn_ty\<^isub>1 b\<^isub>1 \<union> ... \<union> bn_ty\<^isub>p b\<^isub>p"}
-  \end{center} 
-  %
+  \end{equation}\smallskip
+
   \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}
+  where we use the auxiliary binding functions for shallow binders (that means
+  when @{text "ty"}$_i$ is of type @{text "atom"}, @{text "atom set"} or
+  @{text "atom list"}). The set @{text "B'"} collects all free atoms in
+  non-recursive deep binders. Let us assume these binders in the binding 
+  clause @{text "bc\<^isub>i"} are
+
+  \[
   \mbox{@{text "bn\<^isub>1 l\<^isub>1, \<dots>, bn\<^isub>r l\<^isub>r"}}
-  \end{center}
+  \]\smallskip
   
   \noindent
-  with @{text "l"}$_{1..r}$ $\subseteq$ @{text "b"}$_{1..p}$ and none of the 
-  @{text "l"}$_{1..r}$ being among the bodies @{text
-  "d"}$_{1..q}$. The set @{text "B'"} is defined as\\[-5mm]
-  %
-  \begin{center}
-  @{text "B' \<equiv> fa_bn\<^isub>1 l\<^isub>1 \<union> ... \<union> fa_bn\<^isub>r l\<^isub>r"}\\[-9mm]
-  \end{center}
-  %
+  with @{text "l"}$_{1..r}$ $\subseteq$ @{text "b"}$_{1..p}$ (see
+  \eqref{bdef}) and none of the @{text "l"}$_{1..r}$ being among the bodies
+  @{text "d"}$_{1..q}$. The set @{text "B'"} is defined as
+  
+  \begin{equation}\label{bprimedef}
+  @{text "B' \<equiv> fa_bn\<^isub>1 l\<^isub>1 \<union> ... \<union> fa_bn\<^isub>r l\<^isub>r"}
+  \end{equation}\smallskip
+  
   \noindent
   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 in \eqref{fadef}
   the set of atoms that are left unbound by the binding functions @{text
-  "bn"}$_{1..m}$. We used 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
+  "bn"}$_{1..m}$, see also the definition in \eqref{bprimedef}. We used for
+  the definition of this set the functions @{text "fa_bn"}$_{1..m}$. The
+  definition for those functions needs to be extracted from the clauses the
+  user provided for @{text "bn"}$_{1..m}$ Assume the user specified a @{text
+  bn}-clause of the form
   
-  \begin{center}
+  \[
   @{text "bn (C z\<^isub>1 \<dots> z\<^isub>s) = rhs"}
-  \end{center}
+  \]\smallskip
   
   \noindent
-  where the @{text "z"}$_{1..s}$ are of types @{text "ty"}$_{1..s}$. For each of
-  the arguments we calculate the free atoms as follows:
+  where the @{text "z"}$_{1..s}$ are of types @{text "ty"}$_{1..s}$. For 
+  each of the arguments we calculate the free atoms as follows:
   
-  \begin{center}
+  \[\mbox{
   \begin{tabular}{c@ {\hspace{2mm}}p{0.9\textwidth}}
-  $\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"} by the binding function),\\
+  $\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"} 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"}, and\\
+  with the recursive call @{text "bn\<^isub>i z\<^isub>i"}, and\smallskip\\
   $\bullet$ & @{term "{}"} provided @{text "z\<^isub>i"} occurs in  @{text "rhs"},
-  but without a recursive call.
-  \end{tabular}
-  \end{center}
+  but without a recursive call\\
+  & (that means @{text "z\<^isub>i"} is supposed to become bound by the binding function)\\
+  \end{tabular}}
+  \]\smallskip
   
   \noindent
   For defining @{text "fa_bn (C z\<^isub>1 \<dots> z\<^isub>n)"} we just union up all these sets.
@@ -1356,77 +1406,79 @@
   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}
+  
+  \[\mbox{
   \begin{tabular}{@ {}l@ {\hspace{1mm}}c@ {\hspace{1mm}}l@ {}}
   @{text "fa\<^bsub>trm\<^esub> (Let as t)"} & @{text "="} & @{text "(fa\<^bsub>trm\<^esub> t - set (bn as)) \<union> fa\<^bsub>bn\<^esub> as"}\\
-  @{text "fa\<^bsub>trm\<^esub> (Let_rec as t)"} & @{text "="} & @{text "(fa\<^bsub>assn\<^esub> as \<union> fa\<^bsub>trm\<^esub> t) - set (bn as)"}\\[1mm]
+  @{text "fa\<^bsub>trm\<^esub> (Let_rec as t)"} & @{text "="} & @{text "(fa\<^bsub>assn\<^esub> as \<union> fa\<^bsub>trm\<^esub> t) - set (bn as)"}\smallskip\\
 
   @{text "fa\<^bsub>assn\<^esub> (ANil)"} & @{text "="} & @{term "{}"}\\
-  @{text "fa\<^bsub>assn\<^esub> (ACons a t as)"} & @{text "="} & @{text "(supp a) \<union> (fa\<^bsub>trm\<^esub> t) \<union> (fa\<^bsub>assn\<^esub> as)"}\\[1mm]
+  @{text "fa\<^bsub>assn\<^esub> (ACons a t as)"} & @{text "="} & @{text "(supp a) \<union> (fa\<^bsub>trm\<^esub> t) \<union> (fa\<^bsub>assn\<^esub> as)"}\smallskip\\
 
   @{text "fa\<^bsub>bn\<^esub> (ANil)"} & @{text "="} & @{term "{}"}\\
   @{text "fa\<^bsub>bn\<^esub> (ACons a t as)"} & @{text "="} & @{text "(fa\<^bsub>trm\<^esub> t) \<union> (fa\<^bsub>bn\<^esub> as)"}
-  \end{tabular}
-  \end{center}
+  \end{tabular}}
+  \]\smallskip
+
 
   \noindent
-  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 free atoms
-  of an assignment (in case of @{text "ACons"}, they are given in
-  terms of @{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"}. 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 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, which means in this 
-  example the free atoms in the argument @{text "t"}.  
+  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 free atoms of an assignment
+  (in case of @{text "ACons"}, they are given in terms of @{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"}. 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 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, which means in
+  this example the free atoms in the argument @{text "t"}.
 
-  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 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"}-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 the alpha-equivalence relations for the raw types @{text
-  "ty"}$_{1..n}$ from the specification. We write them as
+  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
+  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"}-functions to alpha-equated terms if they
+  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 
+  alpha-equivalence relations for the raw types @{text
+  "ty"}$_{1..n}$. We write them as
   
-  \begin{center}
-  @{text "\<approx>ty"}$_{1..n}$.
-  \end{center}
+  \[
+  \mbox{@{text "\<approx>ty"}$_{1..n}$}.
+  \]\smallskip
   
   \noindent
   Like with the free-atom functions, we also need to
   define auxiliary alpha-equivalence relations 
   
-  \begin{center}
-  @{text "\<approx>bn\<^isub>"}$_{1..m}$
-  \end{center}
+  \[
+  \mbox{@{text "\<approx>bn\<^isub>"}$_{1..m}$}
+  \]\smallskip
   
   \noindent
   for the binding functions @{text "bn"}$_{1..m}$, 
   To simplify our definitions we will use the following abbreviations for
   \emph{compound equivalence relations} and \emph{compound free-atom functions} acting on tuples.
   
-  \begin{center}
+  \[\mbox{
   \begin{tabular}{r@ {\hspace{2mm}}c@ {\hspace{2mm}}l}
-  @{text "(x\<^isub>1,\<dots>, x\<^isub>n) (R\<^isub>1,\<dots>, R\<^isub>n) (x\<PRIME>\<^isub>1,\<dots>, x\<PRIME>\<^isub>n)"} & @{text "\<equiv>"} &
-  @{text "x\<^isub>1 R\<^isub>1 x\<PRIME>\<^isub>1 \<and> \<dots> \<and> x\<^isub>n R\<^isub>n x\<PRIME>\<^isub>n"}\\
+  @{text "(x\<^isub>1,\<dots>, x\<^isub>n) (R\<^isub>1,\<dots>, R\<^isub>n) (y\<^isub>1,\<dots>, y\<^isub>n)"} & @{text "\<equiv>"} &
+  @{text "x\<^isub>1 R\<^isub>1 y\<^isub>1 \<and> \<dots> \<and> x\<^isub>n R\<^isub>n y\<^isub>n"}\\
   @{text "(fa\<^isub>1,\<dots>, fa\<^isub>n) (x\<^isub>1,\<dots>, x\<^isub>n)"} & @{text "\<equiv>"} & @{text "fa\<^isub>1 x\<^isub>1 \<union> \<dots> \<union> fa\<^isub>n x\<^isub>n"}\\
-  \end{tabular}
-  \end{center}
+  \end{tabular}}
+  \]\smallskip
 
 
   The alpha-equivalence relations are defined as inductive predicates
@@ -1434,22 +1486,23 @@
   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) \<dots> prems(bc\<^isub>k)"}}} 
-  \end{center}
+  \]\smallskip
 
   \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}
+  The task below is to specify what the premises corresponding to a binding
+  clause are. To understand better whet the general pattern is, let us first 
+  treat the special instance where @{text "bc\<^isub>i"} is the empty binding clause 
+  of the form
+
+  \[
   \mbox{\isacommand{binds (set)} @{term "{}"} \isacommand{in} @{text "d\<^isub>1\<dots>d\<^isub>q"}.}
-  \end{center}
+  \]\smallskip
 
   \noindent
-  In this binding clause no atom is bound and we only have to alpha-relate the bodies. For this
+  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
@@ -1509,7 +1562,7 @@
   lets us formally define the premise @{text P} for a non-empty binding clause as:
   
   \begin{center}
-  \mbox{@{term "P \<equiv> \<exists>p. (B, D) \<approx>set R fa p (B', D')"}}\;.
+  \mbox{@{term "P \<equiv> alpha_set_ex (B, D) R fa (B', D')"}}\;.
   \end{center}
 
   \noindent
@@ -1582,9 +1635,9 @@
   \begin{center}
   \begin{tabular}{@ {}c @ {}}
   \infer{@{text "Let as t \<approx>\<^bsub>trm\<^esub> Let as' t'"}}
-  {@{term "\<exists>p. (bn as, t) \<approx>lst alpha_trm fa_trm p (bn as', t')"} & @{text "as \<approx>\<^bsub>bn\<^esub> as'"}}\smallskip\\
+  {@{term "alpha_lst_ex (bn as, t) alpha_trm fa_trm (bn as', t')"} & @{text "as \<approx>\<^bsub>bn\<^esub> as'"}}\smallskip\\
   \makebox[0mm]{\infer{@{text "Let_rec as t \<approx>\<^bsub>trm\<^esub> Let_rec as' t'"}}
-  {@{term "\<exists>p. (bn as, ast) \<approx>lst alpha_trm2 fa_trm2 p (bn as', ast')"}}}
+  {@{term "alpha_lst_ex (bn as, ast) alpha_trm2 fa_trm2 (bn as', ast')"}}}
   \end{tabular}
   \end{center}
 




