525   A specification of a term-calculus in Nominal Isabelle is a collection

   525   The syntax of a specification for a term-calculus in Nominal Isabelle is

   526   of (possibly mutual recursive) type declarations, say $ty_1$, $ty_2$, \ldots $ty_n$ 

   526   heavily inspired by the syntax of the Ott-tool \cite{ott-jfp}. It is a

   527   written as follows:

   527   collection of (possibly mutual recursive) type declarations, say

   528 

   528   $ty_{\alpha{}1}$, $ty_{\alpha{}2}$, \ldots $ty_{\alpha{}n}$, and a

   529   \begin{center}

   529   collection of associated binding function declarations, say

   530   $bn_{\alpha{}1}$, \ldots $bn_{\alpha{}m}$. They are written as follows:

   531 

   532   \begin{center}

   533   \begin{tabular}{@ {\hspace{-9mm}}p{1.8cm}l}

   534   types \mbox{declaration part} &

   535   $\begin{cases}

   536   \mbox{\begin{tabular}{l}

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

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

   539   $\ldots$\\ 

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

   541   \end{tabular}}

   542   \end{cases}$\\

   543   binding \mbox{functions part} &

   544   $\begin{cases}

   545   \mbox{\begin{tabular}{l}

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

   547   $\ldots$\\

   548   \isacommand{where}\\

   549   $\ldots$\\

   550   \end{tabular}}

   551   \end{cases}$\\

   552   \end{tabular}

   553   \end{center}

   554 

   555   \noindent

   556   Each type declaration $ty_{\alpha{}i}$ consists of a collection of 

   557   term-constructors, each of which comes with a list of labelled 

   558   types that indicate the types of the arguments of the term-constructor,

   559   like 

   560 

   561   \begin{center}

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

   563   \end{center}

   564   

   565   \noindent

   566   The labels are optional and can be used in the (possibly empty) list of binding clauses.

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

   568   are of the form

   569 

   570   \begin{center}

   571   \isacommand{bind}\; {\it binders}\; \isacommand{in}\; {\it label} 

   572   \end{center}

   573 

   574   \noindent

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

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

   577   \isacommand{in}\; {\it another\_label}. The only restriction on shallow binders

   578   is that the {\it label} must refer to either a type which is single atom or

   579   to a type which is a finite set of atoms. For example the specification of 

   580   lambda-terms and type-schemes use them:

   581 

   582   \begin{center}

   583   \begin{tabular}{cc}

   531   \isacommand{nominal\_datatype} $ty_{\alpha{}1} =$\\

   585   \isacommand{nominal\_datatype} lam =\\

   532   \isacommand{and} $ty_{\alpha{}2} =$\\

   586   \hspace{5mm}Var\;{\it name}\\

   533   $\ldots$\\ 

   587   \hspace{5mm}App\;{\it lam}\;{\it lam}\\

   534   \isacommand{and} $ty_{\alpha{}}n =$\\ 

   588   \hspace{5mm}Lam\;{\it x::name}\;{\it t::lam}\;

   535   $\ldots$\\

   589   \isacommand{bind} {\it x} \isacommand{in} {\it t}\\

   536   \isacommand{with}\\

   590   \end{tabular} &

   537   $\ldots$\\

   591   \begin{tabular}{l}

   592   foo

   539   \end{center}

   594   \end{tabular}

   540 

   595   \end{center}

   541   \noindent

   542   The section below the \isacommand{with} are binding functions, which

   543   will be explained below.

   544   

   545