578 is that the {\it label} must refer to either a type which is single atom or |
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 |
579 to a type which is a finite set of atoms. For example the specification of |
580 lambda-terms and type-schemes use them: |
580 lambda-terms and type-schemes use them: |
581 |
581 |
582 \begin{center} |
582 \begin{center} |
583 \begin{tabular}{cc} |
583 \begin{tabular}{@ {}cc@ {}} |
584 \begin{tabular}{l} |
584 \begin{tabular}{@ {}l@ {\hspace{-1mm}}} |
585 \isacommand{nominal\_datatype} lam =\\ |
585 \isacommand{nominal\_datatype} {\it lam} =\\ |
586 \hspace{5mm}Var\;{\it name}\\ |
586 \hspace{5mm}\phantom{$\mid$} Var\;{\it name}\\ |
587 \hspace{5mm}App\;{\it lam}\;{\it lam}\\ |
587 \hspace{5mm}$\mid$ App\;{\it lam}\;{\it lam}\\ |
588 \hspace{5mm}Lam\;{\it x::name}\;{\it t::lam}\; |
588 \hspace{5mm}$\mid$ Lam\;{\it x::name}\;{\it t::lam}\\ |
589 \isacommand{bind} {\it x} \isacommand{in} {\it t}\\ |
589 \hspace{22mm}\isacommand{bind} {\it x} \isacommand{in} {\it t}\\ |
590 \end{tabular} & |
590 \end{tabular} & |
591 \begin{tabular}{l} |
591 \begin{tabular}{@ {}l@ {}} |
592 foo |
592 \isacommand{nominal\_datatype} {\it ty} =\\ |
|
593 \hspace{5mm}\phantom{$\mid$} TVar\;{\it name}\\ |
|
594 \hspace{5mm}$\mid$ TFun\;{\it ty}\;{\it ty}\\ |
|
595 \isacommand{and} {\it S} = All\;{\it xs::(name fset)}\;{\it T::ty}\\ |
|
596 \hspace{27mm}\isacommand{bind} {\it xs} \isacommand{in} {\it T}\\ |
593 \end{tabular} |
597 \end{tabular} |
594 \end{tabular} |
598 \end{tabular} |
595 \end{center} |
599 \end{center} |
596 |
600 |
|
601 \noindent |
597 A specification of a term-calculus in Nominal Isabell is very similar to |
602 A specification of a term-calculus in Nominal Isabell is very similar to |
598 the usual datatype definition of Isabelle/HOL: |
603 the usual datatype definition of Isabelle/HOL: |
599 |
604 |
600 |
605 |
601 Because of the problem Pottier pointed out in \cite{Pottier06}, the general |
606 Because of the problem Pottier pointed out in \cite{Pottier06}, the general |