So far, Nominal Isabelle provided a mechanism to construct

  automatically alpha-equated lambda terms sich as

  \begin{center}

  $t ::= x \mid t\;t \mid \lambda x. t$

  \end{center}

  \noindent

  For such calculi, it derived automatically a convenient reasoning

  infrastructure. With this it has been used to formalise an equivalence

  checking algorithm for LF \cite{UrbanCheneyBerghofer08}, Typed

  Scheme~\cite{TobinHochstadtFelleisen08}, several calculi for concurrency

  \cite{BengtsonParrow07,BengtsonParow09} and a strong normalisation result

  for cut-elimination in classical logic \cite{UrbanZhu08}. It has also been

  used by Pollack for formalisations in the locally-nameless approach to

  binding \cite{SatoPollack10}.

  However, Nominal Isabelle has fared less well in a formalisation of

  the algorithm W \cite{UrbanNipkow09} where types and type-schemes

  are represented by

  \begin{center}

  \begin{tabular}{l}

  $T ::= x \mid T \rightarrow T$ \hspace{5mm} $S ::= \forall \{x_1,\ldots, x_n\}. T$

  \end{tabular}

  \end{center}

  \noindent

  While it is possible to formalise the finite set of variables that are

  abstracted in a type-scheme by iterating single abstractions, it leads to a very

  clumsy formalisation. This need of iterating single binders for representing

  multiple binders is also the reason why Nominal Isabelle and other theorem

  provers have so far not fared very well with the more advanced tasks in the POPLmark

  challenge, because also there one would like to abstract several variables 

  at once.

  There are interesting points to note with binders that abstract multiple 

  variables. First in the case of type-schemes we do not like to make a distinction

  about the order of the binders. So we would like to regard the following two

  type-schemes as alpha-equivalent:

  \begin{center}

  $\forall \{x, y\}. x \rightarrow y  \;\approx_\alpha\; \forall \{y, x\}. y \rightarrow x$ 

  \end{center}

  \noindent

  but assuming $x$, $y$ and $z$ are distinct, the following two should be \emph{not} 

  alpha-equivalent:

  \begin{center}

  $\forall \{x, y\}. x \rightarrow y  \;\not\approx_\alpha\; \forall \{z\}. z \rightarrow z$ 

  \end{center}

  \noindent

  However we do like to regard type-schemes as alpha-equivalent, if they

  differ only on \emph{vacuous} binders, such as

  \begin{center}

  $\forall \{x\}. x \rightarrow y  \;\approx_\alpha\; \forall \{x, z\}. x \rightarrow y$ 

  \end{center}

  \noindent

  In this paper we will give a general abstraction mechanism and assciated notion of alpha-equivalence 

  which can be used to represent type-schemes.  The difficulty in finding the notion of alpha-equivalence 

  can be appreciated by considering that the definition given by Leroy in \cite{Leroy92} is incorrect 

  (it omits a side-condition).

  However, the notion of alpha-equivalence that is preserved by vacuous binders is not

  alway wanted. For example in constructs like

  \begin{center}

  $\LET x = 3 \AND y = 2 \IN x \backslash y \END$

  \end{center}

  \noindent

  we might not care in which order the associations $x = 3$ and $y = 2$ are

  given, but it would be unusual to regard this term as alpha-equivalent with

  \begin{center}

  $\LET x = 3 \AND y = 2 \AND z = loop \IN x \backslash y \END$

  \end{center}

  \noindent

  We will provide a separate abstraction mechanism for this case where the

  order of binders does not matter, but the ``cardinality'' of the binders

  has to be the same.

  However, this is still not sufficient for covering language constructs frequently 

  occuring in programming language research. For example in patters like

  \begin{center}

  $\LET (x, y) = (3, 2) \IN x \backslash y \END$

  \end{center}

  \noindent

  we want to bind all variables from the pattern (there might be an arbitrary

  number of them) inside the body of the let, but we also care about the order

  of these variables, since we do not want to identify this term with

  \begin{center}

  $\LET (y, x) = (3, 2) \IN x \backslash y \END$

  \end{center}

  \noindent

  Therefore we have identified three abstraction mechanisms for multiple binders

  and allow the user to chose which one is intended. 

  By providing general abstraction mechanisms that allow the binding of multiple

  variables, we have to work around aproblem that has been first pointed out

  by Pottier in \cite{Pottier}: in let-constructs such as

  \begin{center}

  $\LET x_1 = t_1 \AND \ldots \AND x_n = t_n \IN s \END$

  \end{center}

  \noindent

  where the $x_i$ are bound in $s$. In this term we might not care about the order in 

  which the $x_i = t_i$ are given, but we do care about the information that there are 

  as many $x_i$ as there are $t_i$. We lose this information if we represent the $\mathtt{let}$

  as something 

text {*

  Restrictions

  \begin{itemize}

  \item non-emptyness

  \item positive datatype definitions

  \item finitely supported abstractions

  \item respectfulness of the bn-functions\bigskip

  \item binders can only have a ``single scope''

  \end{itemize}

*}

  Complication when the single scopedness restriction is lifted (two 

  overlapping permutations)

*}

text {*