925   we have binding clauses of the form:

   925   we allow binding clauses of the form:

   926 

   926 

   927   \begin{center}

   927   \begin{center}

   928   \begin{tabular}{ll}

   928   \begin{tabular}{@ {}ll@ {}}

   929   @{text "Foo x::name y::name t::lam s::lam"} &  

   929   @{text "Foo\<^isub>1 x::name y::name t::lam s::lam"} &  

   930       \isacommand{bind} @{text "x y"} \isacommand{in} @{text "t s"}  

   930       \isacommand{bind} @{text "x y"} \isacommand{in} @{text "t s"}\\

   931   \end{tabular}

   931   @{text "Foo\<^isub>2 x::name y::name t::lam s::lam"} &  

   932   \end{center}

   932       \isacommand{bind} @{text "x y"} \isacommand{in} @{text "t"}, 

   933 

   933       \isacommand{bind} @{text "x y"} \isacommand{in} @{text "s"}\\

   934   \noindent

   934   \end{tabular}

   935   Similarly for the other binding modes.

   935   \end{center}

   936   

   936 

   937 

   937   \noindent

   938   There are a few restrictions we need to impose: First, a body can only occur in

   938   Similarly for the other binding modes. Interestingly, in case of \isacommand{bind\_set}

   939   \emph{one} binding clause of a term constructor. 

   939   and \isacommand{bind\_res} the binding clauses will make a difference in

   940   For binders we distinguish between \emph{shallow} and \emph{deep} binders.

   940   terms of the corresponding alpha-equivalence. We will show this later with an example.

   941   Shallow binders are just labels. The

   941   

   942   restriction we need to impose on them is that in case of

   942   There are some restrictions we need to impose: First, a body can only occur

   943   \isacommand{bind\_set} and \isacommand{bind\_res} the labels must

   943   in \emph{one} binding clause of a term constructor. For binders we

   944   either refer to atom types or to sets of atom types; in case of

   944   distinguish between \emph{shallow} and \emph{deep} binders.  Shallow binders

   945   \isacommand{bind} the labels must refer to atom types or lists of atom types. 

   945   are just labels. The restriction we need to impose on them is that in case

   946   Two examples for the use of shallow binders are the specification of

   946   of \isacommand{bind\_set} and \isacommand{bind\_res} the labels must either

   947   lambda-terms, where a single name is bound, and type-schemes, where a finite

   947   refer to atom types or to sets of atom types; in case of \isacommand{bind}

   948   set of names is bound:

   948   the labels must refer to atom types or lists of atom types. Two examples for

   949   the use of shallow binders are the specification of lambda-terms, where a

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

   951   bound:

   970   Note that for @{text lam} it does not matter which binding mode we use. The reason is that 

   973   Note that for @{text lam} it does not matter which binding mode we use. The

   971   we bind only a single @{text name}. However, having \isacommand{bind\_set} or 

   974   reason is that we bind only a single @{text name}. However, having

   972   \isacommand{bind} in the second

   975   \isacommand{bind\_set} or \isacommand{bind} in the second case again makes a

   973   case changes the semantics of the specification. 

   976   difference to the underlying notion of alpha-equivalence. Note also that in

   974   Note also that in these specifications @{text "name"} refers to an atom type, and

   977   these specifications @{text "name"} refers to an atom type, and @{text

   975   @{text "fset"} to the type of finite sets. 

   978   "fset"} to the type of finite sets.

   979 

   978   the atoms in one argument of the term-constructor, which can be bound in  

   982   the atoms in one argument of the term-constructor, which can be bound in

   979   other arguments and also in the same argument (we will

   983   other arguments and also in the same argument (we will call such binders

   980   call such binders \emph{recursive}, see below). 

   984   \emph{recursive}, see below). The corresponding binding functions are

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

   985   expected to return either a set of atoms (for \isacommand{bind\_set} and

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

   986   \isacommand{bind\_res}) or a list of atoms (for \isacommand{bind}). They can

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

   987   be defined by primitive recursion over the corresponding type; the equations

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

   988   must be given in the binding function part of the scheme shown in

   985   the scheme shown in \eqref{scheme}. For example a term-calculus containing @{text "Let"}s 

   989   \eqref{scheme}. For example a term-calculus containing @{text "Let"}s with

   986   with tuple patterns might be specified as:

   990   tuple patterns might be specified as:

   991 

  1068   represented by the general binders described in Section

  1073   represented by the general binders described in Section~\ref{sec:binders}. 

  1069   \ref{sec:binders}. Unlike shallow binders, we restrict deep binders to occur

  1070   in only one binding clause.

  1087   In order to simplify later definitions, we shall assume specifications 

  1090   In order to simplify our definitions, we shall assume specifications