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   collection of (possibly mutual recursive) type declarations, say

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

   529   collection of associated binding function declarations, say

   530   $bn_{\alpha{}1}$, \ldots $bn_{\alpha{}m}$. They are schematically 

   530   \begin{tabular}{l}

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

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

   535   types \mbox{declaration part} &

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

   536   $\begin{cases}

   537   \mbox{\begin{tabular}{l}

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

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

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

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

   542   \end{tabular}}

   543   \end{cases}$\\

   544   binding \mbox{functions part} &

   545   $\begin{cases}

   546   \mbox{\begin{tabular}{l}

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

   536   \isacommand{with}\\

   549   \isacommand{where}\\

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

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

   543   will be explained below.

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

   544   

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

   545 

   560   like 

   546 

   561 

   562   \begin{center}

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

   564   \end{center}

   565   

   566   \noindent

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

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

   569   are of the form

   570 

   571   \begin{center}

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

   573   \end{center}

   574 

   575   \noindent

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

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

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

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

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

   581   lambda-terms and type-schemes use them:

   582 

   583   \begin{center}

   584   \begin{tabular}{@ {}cc@ {}}

   585   \begin{tabular}{@ {}l@ {\hspace{-1mm}}}

   586   \isacommand{nominal\_datatype} {\it lam} =\\

   587   \hspace{5mm}\phantom{$\mid$} Var\;{\it name}\\

   588   \hspace{5mm}$\mid$ App\;{\it lam}\;{\it lam}\\

   589   \hspace{5mm}$\mid$ Lam\;{\it x::name}\;{\it t::lam}\\

   590   \hspace{22mm}\isacommand{bind} {\it x} \isacommand{in} {\it t}\\

   591   \end{tabular} &

   592   \begin{tabular}{@ {}l@ {}}

   593   \isacommand{nominal\_datatype} {\it ty} =\\

   594   \hspace{5mm}\phantom{$\mid$} TVar\;{\it name}\\

   595   \hspace{5mm}$\mid$ TFun\;{\it ty}\;{\it ty}\\

   596   \isacommand{and} {\it S} = All\;{\it xs::(name fset)}\;{\it T::ty}\\

   597   \hspace{27mm}\isacommand{bind} {\it xs} \isacommand{in} {\it T}\\

   598   \end{tabular}

   599   \end{tabular}

   600   \end{center}

   601 

   602   \noindent