290   then with not too great effort we obtain a function $\fv_\alpha$

   290   then with not too great effort we obtain a function $\fv^\alpha$

   295   $\fv_\alpha(x) = \{x\}$\hspace{10mm}

   295   $\fv^\alpha(x) = \{x\}$\hspace{10mm}

   296   $\fv_\alpha(t_1\;t_2) = \fv_\alpha(t_1) \cup \fv_\alpha(t_2)$\\[1mm]

   296   $\fv^\alpha(t_1\;t_2) = \fv^\alpha(t_1) \cup \fv^\alpha(t_2)$\\[1mm]

   297   $\fv_\alpha(\lambda x.t) = \fv_\alpha(t) - \{x\}$

   297   $\fv^\alpha(\lambda x.t) = \fv^\alpha(t) - \{x\}$

   396 section {* General Binders *}

   396 section {* General Binders\label{sec:binders} *}

   535   $ty_{\alpha{}1}$, $ty_{\alpha{}2}$, \ldots $ty_{\alpha{}n}$, and an

   535   $ty^\alpha_1$, $ty^\alpha_2$, \ldots $ty^\alpha_n$, and an

   537   $bn_{\alpha{}1}$, \ldots $bn_{\alpha{}m}$. They are schematically written as

   537   $bn^\alpha_1$, \ldots $bn^\alpha_m$. The syntax for a specification is

   538   follows:

   538   rougly as follows:

   545   \isacommand{nominal\_datatype} $ty_{\alpha{}1} = \ldots$\\

   545   \isacommand{nominal\_datatype} $ty^\alpha_1 = \ldots$\\

   546   \isacommand{and} $ty_{\alpha{}2} = \ldots$\\

   546   \isacommand{and} $ty^\alpha_2 = \ldots$\\

   548   \isacommand{and} $ty_{\alpha{}n} = \ldots$\\ 

   548   \isacommand{and} $ty^\alpha_n = \ldots$\\ 

   554   \isacommand{with} $bn_{\alpha{}1}$ \isacommand{and} \ldots \isacommand{and} $bn_{\alpha{}m}$

   554   \isacommand{with} $bn^\alpha_1$ \isacommand{and} \ldots \isacommand{and} $bn^\alpha_m$

   564   Every type declaration $ty_{\alpha{}i}$ consists of a collection of 

   564   Every type declaration $ty^\alpha_i$ consists of a collection of 

   566   types that indicate the types of the arguments of the term-constructor.

   566   types that stand for the types of the arguments of the term-constructor.

   567   For example for a term-constructor $C_{\alpha}$ we might have

   567   For example for a term-constructor $C^\alpha$ we might have

   568 

   568 

   569   \begin{center}

   569   \begin{center}

   570   $C_\alpha\;label_1\!::\!ty'_1\;\ldots label_j\!::\!ty'_j\;\;\textit{binding\_clauses}$ 

   570   $C^\alpha\;label_1\!::\!ty'_1\;\ldots label_l\!::\!ty'_l\;\;\textit{binding\_clauses}$ 

   571   \end{center}

   571   \end{center}

   572   

   572   

   573   \noindent

   573   \noindent

   574   The labels are optional and can be used in the (possibly empty) list of \emph{binding clauses}.

   574   whereby some of the $ty'_k$ are contained in the set of $ty^\alpha_i$

   575   These clauses indicate  the binders and the scope of the binders in a term-constructor.

   575   declared in \eqref{scheme}. In this case we will call

   576   They come in three forms

   576   the corresponding argument a \emph{recursive argument}.  The labels

   577   annotated on the types are optional and can be used in the (possibly empty)

   578   list of \emph{binding clauses}.  These clauses indicate the binders and the

   579   scope of the binders in a term-constructor.  They come in three \emph{modes}

   587   whereby we also distinguish between \emph{shallow} binders and \emph{deep} binders.

   590   The first mode is for binding lists of atoms (order matters); in the second sets

   588   Shallow binders are of the form \isacommand{bind}\; {\it label}\; 

   591   of binders (order does not matter, but cardinality does) and in the last 

   589   \isacommand{in}\; {\it another\_label} (similar the other forms). The restriction 

   592   sets of binders (with vacuous binders preserving alpha-equivalence).

   590   we impose on shallow binders

   593 

   591   is that the {\it label} must either refer to a type that is an atom type or

   594   In addition we distinguish between \emph{shallow} binders and \emph{deep}

   592   to a type that is a finite set or list of an atom type. For example the specifications of 

   595   binders.  Shallow binders are of the form \isacommand{bind}\; {\it label}\;

   593   lambda-terms and type-schemes use shallow binders (where \emph{name} is an atom type):

   596   \isacommand{in}\; {\it another\_label} (similar the other two modes). The

   597   restriction we impose on shallow binders is that the {\it label} must either

   598   refer to a type that is an atom type or to a type that is a finite set or

   599   list of an atom type. For example the specifications of lambda-terms, where

   600   a single name is bound, and type-schemes, where a finite set of names is

   601   bound, use shallow binders (the type \emph{name} is an atom type):

   615   A \emph{deep} binder uses an auxiliary binding function that ``picks'' out the atoms

   623   If we have shallow binders that ``share'' a body, for example

   616   in one argument that can be bound in one or more arguments. Such a binding function returns either 

   624 

   617   a set of atoms (for \isacommand{bind\_set} and \isacommand{bind\_res}) or a 

   625   \begin{center}

   618   list of atoms (for \isacommand{bind}). It can be defined 

   626   \begin{tabular}{ll}

   619   by primitive recursion over the corresponding type; the equations

   627   \it {\rm Foo}$_0$ x::name y::name t::lam & \it 

   620   are stated in the binding function part of the scheme shown in \eqref{scheme}. 

   628                               \isacommand{bind}\;x\;\isacommand{in}\;t,\;

   629                               \isacommand{bind}\;y\;\isacommand{in}\;t  

   630   \end{tabular}

   631   \end{center}

   632 

   633   \noindent

   634   then we have to make sure the modes of the binders agree. For example we cannot

   635   have in the first binding clause the mode \isacommand{bind} and in the second 

   636   \isacommand{bind\_set}.

   637 

   638   A \emph{deep} binder uses an auxiliary binding function that ``picks'' out

   639   the atoms in one argument of the term-constructor that can be bound in one

   640   or more of the other arguments and also can be bound in the same argument (we will

   641   call such binders \emph{recursive}). 

   642   The binding functions are expected to return either a set of atoms

   643   (for \isacommand{bind\_set} and \isacommand{bind\_res}) or a list of atoms

   644   (for \isacommand{bind}). They can be defined by primitive recursion over the

   645   corresponding type; the equations must be given in the binding function part of

   646   the scheme shown in \eqref{scheme}.

   647 

   624   binding functions can only return the empty set, a singleton set of atoms or 

   651   binding function can only return the empty set, a singleton set containing an 

   625   unions of atom sets. For example for lets with patterns you might define

   652   atom or unions of atom sets. For example for lets with tuple patterns you might 

   653   define

   648   In this definition the function $atom$ coerces a name into the generic 

   676   In this specification the function $atom$ coerces a name into the generic 

   649   atom type of Nominal Isabelle. In this way we can treat binders of different

   677   atom type of Nominal Isabelle. This allows us to treat binders of different

   650   type uniformely.

   678   type uniformly. As will shortly become clear, we cannot return an atom 

   651 

   679   in a binding function that also is bound in the term-constructor. 

   680 

   681   Like with shallow binders, deep binders with shared body need to have the

   682   same binding mode. A more serious restriction we have to impose on deep binders 

   683   is that we cannot have ``overlapping'' binders. Consider for example the 

   684   term-constructors:

   685 

   686   \begin{center}

   687   \begin{tabular}{ll}

   688   \it {\rm Foo}$_1$ p::pat q::pat t::trm & \it \isacommand{bind}\;bn(p)\;\isacommand{in}\;t,\;

   689                               \isacommand{bind}\;bn(q)\;\isacommand{in}\;t\\

   690   \it {\rm Foo}$_2$ x::name p::pat t::trm & \it \it \isacommand{bind}\;x\;\isacommand{in}\;t,\;

   691                               \isacommand{bind}\;bn(p)\;\isacommand{in}\;t 

   692   

   693   \end{tabular}

   694   \end{center}

   695 

   696   \noindent

   697   In the first case we bind all atoms from the pattern $p$ in $t$ and also all atoms 

   698   from $q$ in $t$. Therefore the binders overlap in $t$. Similarly in the second case:

   699   the binder $bn(p)$ overlap with the shallow binder $x$. We must exclude such specifiactions, 

   700   as we will not be able to represent them using the general binders described in 

   701   Section \ref{sec:binders}. However the following two term-constructors are allowed:

   702 

   703   \begin{center}

   704   \begin{tabular}{ll}

   705   \it {\rm Bar}$_1$ p::pat t::trm s::trm & \it \isacommand{bind}\;bn(p)\;\isacommand{in}\;t,\;

   706                                             \isacommand{bind}\;bn(p)\;\isacommand{in}\;s\\

   707   \it {\rm Bar}$_2$ p::pat t::trm &  \it \isacommand{bind}\;bn(p)\;\isacommand{in}\;p,\;

   708                                       \isacommand{bind}\;bn(p)\;\isacommand{in}\;t\\

   709   \end{tabular}

   710   \end{center}

   711 

   712   \noindent

   713   as no overlapping of binders occurs.