--- a/Paper/Paper.thy	Wed Mar 24 12:03:48 2010 +0100
+++ b/Paper/Paper.thy	Wed Mar 24 12:04:03 2010 +0100
@@ -287,14 +287,14 @@
   \end{center}
   
   \noindent
-  then with not too great effort we obtain a function $\fv_\alpha$
+  then with not too great effort we obtain a function $\fv^\alpha$
   operating on quotients, or alpha-equivalence classes of lambda-terms. This
   function is characterised by the equations
 
   \begin{center}
-  $\fv_\alpha(x) = \{x\}$\hspace{10mm}
-  $\fv_\alpha(t_1\;t_2) = \fv_\alpha(t_1) \cup \fv_\alpha(t_2)$\\[1mm]
-  $\fv_\alpha(\lambda x.t) = \fv_\alpha(t) - \{x\}$
+  $\fv^\alpha(x) = \{x\}$\hspace{10mm}
+  $\fv^\alpha(t_1\;t_2) = \fv^\alpha(t_1) \cup \fv^\alpha(t_2)$\\[1mm]
+  $\fv^\alpha(\lambda x.t) = \fv^\alpha(t) - \{x\}$
   \end{center}
 
   \noindent
@@ -393,7 +393,7 @@
 *}
 
 
-section {* General Binders *}
+section {* General Binders\label{sec:binders} *}
 
 text {*
   In Nominal Isabelle, the user is expected to write down a specification of a
@@ -532,26 +532,26 @@
   Our specifications for term-calculi are heavily
   inspired by the syntax of the Ott-tool \cite{ott-jfp}. A specification is
   a collection of (possibly mutual recursive) type declarations, say
-  $ty_{\alpha{}1}$, $ty_{\alpha{}2}$, \ldots $ty_{\alpha{}n}$, and an
+  $ty^\alpha_1$, $ty^\alpha_2$, \ldots $ty^\alpha_n$, and an
   associated collection of binding function declarations, say
-  $bn_{\alpha{}1}$, \ldots $bn_{\alpha{}m}$. They are schematically written as
-  follows:
+  $bn^\alpha_1$, \ldots $bn^\alpha_m$. The syntax for a specification is
+  rougly as follows:
 
   \begin{equation}\label{scheme}
   \mbox{\begin{tabular}{@ {\hspace{-9mm}}p{1.8cm}l}
   type \mbox{declaration part} &
   $\begin{cases}
   \mbox{\begin{tabular}{l}
-  \isacommand{nominal\_datatype} $ty_{\alpha{}1} = \ldots$\\
-  \isacommand{and} $ty_{\alpha{}2} = \ldots$\\
+  \isacommand{nominal\_datatype} $ty^\alpha_1 = \ldots$\\
+  \isacommand{and} $ty^\alpha_2 = \ldots$\\
   $\ldots$\\ 
-  \isacommand{and} $ty_{\alpha{}n} = \ldots$\\ 
+  \isacommand{and} $ty^\alpha_n = \ldots$\\ 
   \end{tabular}}
   \end{cases}$\\
   binding \mbox{function part} &
   $\begin{cases}
   \mbox{\begin{tabular}{l}
-  \isacommand{with} $bn_{\alpha{}1}$ \isacommand{and} \ldots \isacommand{and} $bn_{\alpha{}m}$
+  \isacommand{with} $bn^\alpha_1$ \isacommand{and} \ldots \isacommand{and} $bn^\alpha_m$
   $\ldots$\\
   \isacommand{where}\\
   $\ldots$\\
@@ -561,19 +561,22 @@
   \end{equation}
 
   \noindent
-  Every type declaration $ty_{\alpha{}i}$ consists of a collection of 
+  Every type declaration $ty^\alpha_i$ consists of a collection of 
   term-constructors, each of which comes with a list of labelled 
-  types that indicate the types of the arguments of the term-constructor.
-  For example for a term-constructor $C_{\alpha}$ we might have
+  types that stand for the types of the arguments of the term-constructor.
+  For example for a term-constructor $C^\alpha$ we might have
 
   \begin{center}
-  $C_\alpha\;label_1\!::\!ty'_1\;\ldots label_j\!::\!ty'_j\;\;\textit{binding\_clauses}$ 
+  $C^\alpha\;label_1\!::\!ty'_1\;\ldots label_l\!::\!ty'_l\;\;\textit{binding\_clauses}$ 
   \end{center}
   
   \noindent
-  The labels are optional and can be used in the (possibly empty) list of \emph{binding clauses}.
-  These clauses indicate  the binders and the scope of the binders in a term-constructor.
-  They come in three forms
+  whereby some of the $ty'_k$ are contained in the set of $ty^\alpha_i$
+  declared in \eqref{scheme}. In this case we will call
+  the corresponding argument a \emph{recursive argument}.  The labels
+  annotated on the types are optional and can be used in the (possibly empty)
+  list of \emph{binding clauses}.  These clauses indicate the binders and the
+  scope of the binders in a term-constructor.  They come in three \emph{modes}
 
   \begin{center}
   \begin{tabular}{l}
@@ -584,13 +587,18 @@
   \end{center}
 
   \noindent
-  whereby we also distinguish between \emph{shallow} binders and \emph{deep} binders.
-  Shallow binders are of the form \isacommand{bind}\; {\it label}\; 
-  \isacommand{in}\; {\it another\_label} (similar the other forms). The 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. For example the specifications of 
-  lambda-terms and type-schemes use shallow binders (where \emph{name} is an atom type):
+  The first mode is for binding lists of atoms (order matters); in the second sets
+  of binders (order does not matter, but cardinality does) and in the last 
+  sets of binders (with vacuous binders preserving alpha-equivalence).
+
+  In addition we distinguish between \emph{shallow} binders and \emph{deep}
+  binders.  Shallow binders are of the form \isacommand{bind}\; {\it label}\;
+  \isacommand{in}\; {\it another\_label} (similar the other two modes). The
+  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. For example the specifications of lambda-terms, where
+  a single name is bound, and type-schemes, where a finite set of names is
+  bound, use shallow binders (the type \emph{name} is an atom type):
 
   \begin{center}
   \begin{tabular}{@ {}cc@ {}}
@@ -612,17 +620,37 @@
   \end{center}
 
   \noindent
-  A \emph{deep} binder uses an auxiliary binding function that ``picks'' out the atoms
-  in one argument that can be bound in one or more arguments. Such a binding function returns either 
-  a set of atoms (for \isacommand{bind\_set} and \isacommand{bind\_res}) or a 
-  list of atoms (for \isacommand{bind}). It can be defined 
-  by primitive recursion over the corresponding type; the equations
-  are stated in the binding function part of the scheme shown in \eqref{scheme}. 
+  If we have shallow binders that ``share'' a body, for example
+
+  \begin{center}
+  \begin{tabular}{ll}
+  \it {\rm Foo}$_0$ x::name y::name t::lam & \it 
+                              \isacommand{bind}\;x\;\isacommand{in}\;t,\;
+                              \isacommand{bind}\;y\;\isacommand{in}\;t  
+  \end{tabular}
+  \end{center}
+
+  \noindent
+  then we have to make sure the modes of the binders agree. For example we cannot
+  have in the first binding clause the mode \isacommand{bind} and in the second 
+  \isacommand{bind\_set}.
+
+  A \emph{deep} binder uses an auxiliary binding function that ``picks'' out
+  the atoms in one argument of the term-constructor that can be bound in one
+  or more of the other arguments and also can be bound in the same argument (we will
+  call such binders \emph{recursive}). 
+  The 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}.
+
 
   In the present version of Nominal Isabelle, we 
   adopted the restrictions the Ott-tool imposes on the binding functions, namely a 
-  binding functions can only return the empty set, a singleton set of atoms or 
-  unions of atom sets. For example for lets with patterns you might define
+  binding function can only return the empty set, a singleton set containing an 
+  atom or unions of atom sets. For example for lets with tuple patterns you might 
+  define
 
   \begin{center}
   \begin{tabular}{l}
@@ -645,10 +673,44 @@
   \end{center}
   
   \noindent
-  In this definition the function $atom$ coerces a name into the generic 
-  atom type of Nominal Isabelle. In this way we can treat binders of different
-  type uniformely.
+  In this specification the function $atom$ coerces a name into the generic 
+  atom type of Nominal Isabelle. This allows us to treat binders of different
+  type uniformly. As will shortly become clear, we cannot return an atom 
+  in a binding function that also is bound in the term-constructor. 
+
+  Like with shallow binders, deep binders with shared body need to have the
+  same binding mode. A more serious restriction we have to impose on deep binders 
+  is that we cannot have ``overlapping'' binders. Consider for example the 
+  term-constructors:
 
+  \begin{center}
+  \begin{tabular}{ll}
+  \it {\rm Foo}$_1$ p::pat q::pat t::trm & \it \isacommand{bind}\;bn(p)\;\isacommand{in}\;t,\;
+                              \isacommand{bind}\;bn(q)\;\isacommand{in}\;t\\
+  \it {\rm Foo}$_2$ x::name p::pat t::trm & \it \it \isacommand{bind}\;x\;\isacommand{in}\;t,\;
+                              \isacommand{bind}\;bn(p)\;\isacommand{in}\;t 
+  
+  \end{tabular}
+  \end{center}
+
+  \noindent
+  In the first case we bind all atoms from the pattern $p$ in $t$ and also all atoms 
+  from $q$ in $t$. Therefore the binders overlap in $t$. Similarly in the second case:
+  the binder $bn(p)$ overlap with the shallow binder $x$. We must exclude such specifiactions, 
+  as we will not be able to represent them using the general binders described in 
+  Section \ref{sec:binders}. However the following two term-constructors are allowed:
+
+  \begin{center}
+  \begin{tabular}{ll}
+  \it {\rm Bar}$_1$ p::pat t::trm s::trm & \it \isacommand{bind}\;bn(p)\;\isacommand{in}\;t,\;
+                                            \isacommand{bind}\;bn(p)\;\isacommand{in}\;s\\
+  \it {\rm Bar}$_2$ p::pat t::trm &  \it \isacommand{bind}\;bn(p)\;\isacommand{in}\;p,\;
+                                      \isacommand{bind}\;bn(p)\;\isacommand{in}\;t\\
+  \end{tabular}
+  \end{center}
+
+  \noindent
+  as no overlapping of binders occurs.
   
 
   Because of the problem Pottier pointed out in \cite{Pottier06}, the general