535 $ty_{\alpha{}1}$, $ty_{\alpha{}2}$, \ldots $ty_{\alpha{}n}$, and an |
535 $ty_{\alpha{}1}$, $ty_{\alpha{}2}$, \ldots $ty_{\alpha{}n}$, and an |
536 associated collection of binding function declarations, say |
536 associated collection of binding function declarations, say |
537 $bn_{\alpha{}1}$, \ldots $bn_{\alpha{}m}$. They are schematically written as |
537 $bn_{\alpha{}1}$, \ldots $bn_{\alpha{}m}$. They are schematically written as |
538 follows: |
538 follows: |
539 |
539 |
540 \begin{center} |
540 \begin{equation}\label{scheme} |
541 \begin{tabular}{@ {\hspace{-9mm}}p{1.8cm}l} |
541 \mbox{\begin{tabular}{@ {\hspace{-9mm}}p{1.8cm}l} |
542 type \mbox{declaration part} & |
542 type \mbox{declaration part} & |
543 $\begin{cases} |
543 $\begin{cases} |
544 \mbox{\begin{tabular}{l} |
544 \mbox{\begin{tabular}{l} |
545 \isacommand{nominal\_datatype} $ty_{\alpha{}1} = \ldots$\\ |
545 \isacommand{nominal\_datatype} $ty_{\alpha{}1} = \ldots$\\ |
546 \isacommand{and} $ty_{\alpha{}2} = \ldots$\\ |
546 \isacommand{and} $ty_{\alpha{}2} = \ldots$\\ |
604 \begin{tabular}{@ {}l@ {}} |
604 \begin{tabular}{@ {}l@ {}} |
605 \isacommand{nominal\_datatype} {\it ty} =\\ |
605 \isacommand{nominal\_datatype} {\it ty} =\\ |
606 \hspace{5mm}\phantom{$\mid$} TVar\;{\it name}\\ |
606 \hspace{5mm}\phantom{$\mid$} TVar\;{\it name}\\ |
607 \hspace{5mm}$\mid$ TFun\;{\it ty}\;{\it ty}\\ |
607 \hspace{5mm}$\mid$ TFun\;{\it ty}\;{\it ty}\\ |
608 \isacommand{and} {\it tsc} = All\;{\it xs::(name fset)}\;{\it T::ty}\\ |
608 \isacommand{and} {\it tsc} = All\;{\it xs::(name fset)}\;{\it T::ty}\\ |
609 \hspace{22mm}\isacommand{bind\_res} {\it xs} \isacommand{in} {\it T}\\ |
609 \hspace{24mm}\isacommand{bind\_res} {\it xs} \isacommand{in} {\it T}\\ |
610 \end{tabular} |
610 \end{tabular} |
611 \end{tabular} |
611 \end{tabular} |
612 \end{center} |
612 \end{center} |
613 |
613 |
614 \noindent |
614 \noindent |
615 A \emph{deep} binder uses an auxiliary binding function that picks out the atoms |
615 A \emph{deep} binder uses an auxiliary binding function that ``picks'' out the atoms |
616 that are bound in one or more arguments. This binding function returns either |
616 in one argument that can be bound in one or more arguments. Such a binding function returns either |
617 a set of atoms (for \isacommand{bind\_set} and \isacommand{bind\_res}) or a |
617 a set of atoms (for \isacommand{bind\_set} and \isacommand{bind\_res}) or a |
618 list of atoms (for \isacommand{bind}). Such binding functions can be defined |
618 list of atoms (for \isacommand{bind}). It can be defined |
619 by primitive recursion over the corresponding type. They are defined by equations |
619 by primitive recursion over the corresponding type; the equations |
620 included in the binding function part of the scheme given above. |
620 are stated in the binding function part of the scheme shown in \eqref{scheme}. |
621 |
621 |
622 For the moment we |
622 In the present version of Nominal Isabelle, we |
623 adopt the restriction of the Ott-tool that binding functions can only return |
623 adopted the restrictions the Ott-tool imposes on the binding functions, namely a |
624 the empty set, a singleton set of atoms or unions of atom sets. For example |
624 binding functions can only return the empty set, a singleton set of atoms or |
625 |
625 unions of atom sets. For example for lets with patterns you might define |
626 over the type for which they specify the bound atoms. |
626 |
627 |
627 \begin{center} |
628 |
628 \begin{tabular}{l} |
629 |
629 \isacommand{nominal\_datatype} {\it trm} =\\ |
630 \noindent |
630 \hspace{5mm}\phantom{$\mid$} Var\;{\it name}\\ |
631 A specification of a term-calculus in Nominal Isabelle is very similar to |
631 \hspace{5mm}$\mid$ App\;{\it trm}\;{\it trm}\\ |
632 the usual datatype definition of Isabelle/HOL: |
632 \hspace{5mm}$\mid$ Lam\;{\it x::name}\;{\it t::trm} |
633 |
633 \;\;\isacommand{bind} {\it x} \isacommand{in} {\it t}\\ |
|
634 \hspace{5mm}$\mid$ Let\;{\it p::pat}\;{\it trm}\; {\it t::trm} |
|
635 \;\;\isacommand{bind} {\it bn(p)} \isacommand{in} {\it t}\\ |
|
636 \isacommand{and} {\it pat} =\\ |
|
637 \hspace{5mm}\phantom{$\mid$} PNo\\ |
|
638 \hspace{5mm}$\mid$ PVr\;{\it name}\\ |
|
639 \hspace{5mm}$\mid$ PPr\;{\it pat}\;{\it pat}\\ |
|
640 \isacommand{with} {\it bn::pat $\Rightarrow$ atom set}\\ |
|
641 \isacommand{where} $bn(\textrm{PNo}) = \varnothing$\\ |
|
642 \hspace{5mm}$\mid$ $bn(\textrm{PVr}\;x) = \{atom\; x\}$\\ |
|
643 \hspace{5mm}$\mid$ $bn(\textrm{PPr}\;p_1\;p_2) = bn(p_1) \cup bn(p_2)$\\ |
|
644 \end{tabular} |
|
645 \end{center} |
|
646 |
|
647 \noindent |
|
648 In this definition the function $atom$ coerces a name into the generic |
|
649 atom type of Nominal Isabelle. In this way we can treat binders of different |
|
650 type uniformely. |
|
651 |
|
652 |
634 |
653 |
635 Because of the problem Pottier pointed out in \cite{Pottier06}, the general |
654 Because of the problem Pottier pointed out in \cite{Pottier06}, the general |
636 binders from the previous section cannot be used directly to represent w |
655 binders from the previous section cannot be used directly to represent w |
637 be used directly |
656 be used directly |
638 *} |
657 *} |