133   a problem that has been pointed out by Pottier in \cite{Pottier06} and Cheney in

   133   a problem that has been pointed out by Pottier \cite{Pottier06} and Cheney 

   134   \cite{Cheney05}: in 

   134   \cite{Cheney05}: in $\mathtt{let}$-constructs of the form

   135   $\mathtt{let}$-constructs of the form

   536   associated collection of binding function declarations, say

   535   associated collection of binding functions, say

   537   $bn^\alpha_1$, \ldots $bn^\alpha_m$. The syntax in Nominal Isabelle 

   536   $bn^\alpha_1$, \ldots, $bn^\alpha_m$. The syntax in Nominal Isabelle 

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

   540   \mbox{\begin{tabular}{@ {\hspace{-5mm}}p{1.8cm}l}

   567   For example for a term-constructor $C^\alpha$ we might have

   566   For example a term-constructor $C^\alpha$ might have

   574   whereby some of the $ty'_k$ (or their type components) are contained in the 

   573   whereby some of the $ty'_k$ (or their components) are contained in the collection

   575   set of $ty^\alpha_i$

   574   of $ty^\alpha_i$ declared in \eqref{scheme}. In this case we will call the

   576   declared in \eqref{scheme}. In this case we will call

   575   corresponding argument a \emph{recursive argument}.  The labels annotated on

   577   the corresponding argument a \emph{recursive argument}.  The labels

   576   the types are optional and can be used in the (possibly empty) list of

   578   annotated on the types are optional and can be used in the (possibly empty)

   577   \emph{binding clauses}.  These clauses indicate the binders and the scope of

   579   list of \emph{binding clauses}.  These clauses indicate the binders and the

   578   the binders in a term-constructor.  They come in three \emph{modes}

   580   scope of the binders in a term-constructor.  They come in three \emph{modes}

   579 

   591   The first mode is for binding lists of atoms (the order matters); the second is for sets

   590   The first mode is for binding lists of atoms (the order of binders matters); the second is for sets

   600   list of an atom type. For example the specifications of lambda-terms, where

   599   list of an atom type. For example the specifications for lambda-terms, where

   641   the atoms in one argument of the term-constructor that can be bound in  

   640   the atoms in one argument of the term-constructor, which can be bound in  

   659      \;\;\isacommand{bind\_set} {\it bn(p)} \isacommand{in} {\it t}\\

   658      \;\;\isacommand{bind} {\it bn(p)} \isacommand{in} {\it t}\\

   664   \isacommand{with} {\it bn::pat $\Rightarrow$ atom set}\\

   663   \isacommand{with} {\it bn::pat $\Rightarrow$ atom list}\\

   665   \isacommand{where} $bn(\textrm{PNil}) = \varnothing$\\

   664   \isacommand{where} $bn(\textrm{PNil}) = []$\\

   666   \hspace{5mm}$\mid$ $bn(\textrm{PVar}\;x) = \{atom\; x\}$\\

   665   \hspace{5mm}$\mid$ $bn(\textrm{PVar}\;x) = [atom\; x]$\\

   667   \hspace{5mm}$\mid$ $bn(\textrm{PPrd}\;p_1\;p_2) = bn(p_1) \cup bn(p_2)$\\ 

   666   \hspace{5mm}$\mid$ $bn(\textrm{PPrd}\;p_1\;p_2) = bn(p_1)\; @\;bn(p_2)$\\ 

   714   Now the question is how we can turn specifications into actual type

   713   Let us come back one more time to the specification of simultaneous lets. 

   714   A specification for them looks as follows:

   715 

   716   \begin{center}

   717   \begin{tabular}{l}

   718   \isacommand{nominal\_datatype} {\it trm} =\\

   719   \hspace{5mm}\phantom{$\mid$}\ldots\\

   720   \hspace{5mm}$\mid$ Let\;{\it a::assn}\; {\it t::trm} 

   721      \;\;\isacommand{bind} {\it bn(a)} \isacommand{in} {\it t}\\

   722   \isacommand{and} {\it assn} =\\

   723   \hspace{5mm}\phantom{$\mid$} ANil\\

   724   \hspace{5mm}$\mid$ ACons\;{\it name}\;{\it trm}\;{\it assn}\\

   725   \isacommand{with} {\it bn::assn $\Rightarrow$ atom list}\\

   726   \isacommand{where} $bn(\textrm{ANil}) = []$\\

   727   \hspace{5mm}$\mid$ $bn(\textrm{ACons}\;x\;t\;a) = [atom\; x]\; @\; bn(a)$\\

   728   \end{tabular}

   729   \end{center}

   730 

   731   \noindent

   732   The intention with this specification is to bind all variables 

   733   from the assignments inside the body @{text t}. However one might

   734   like to consider the variant where the variables are not just

   735   bound in @{term t}, but also in the assignments themselves. In

   736   this case we need to specify

   737 

   738   \begin{center}

   739   \begin{tabular}{l}

   740   Let\_rec\;{\it a::assn}\; {\it t::trm} 

   741      \;\;\isacommand{bind} {\it bn(a)} \isacommand{in} {\it t},

   742          \isacommand{bind} {\it bn(a)} \isacommand{in} {\it a}\\

   743   \end{tabular}

   744   \end{center}

   745   

   746   \noindent

   747   where we bind also in @{text a} all the atoms @{text bn} returns. In this

   748   case we will say the binder is a \emph{recursive binder}.

   749 

   750   Having dealt with all syntax matters, the problem now is how we can turn 

   751   specifications into actual type

   716   for them? Because of the problem Pottier and Cheney pointed out, we cannot 

   753   for them. Because of the problem Pottier and Cheney pointed out, we cannot 

   718   their scopes next to each other, an then use the type constructors 

   755   their bodies next to each other, an then use the type constructors 

   719   @{text "abs_set"}, @{text "abs_res"} and @{text "abs_list"}. Therefore

   756   @{text "abs_set"}, @{text "abs_res"} and @{text "abs_list"} from Section 

   757   \ref{sec:binders}. Therefore

   726   given by user. We just use an affix:

   764   given by user. We just use an affix like

   733   This definition can be made, provided the usual conditions hold: the 

   771   The datatype definition can be made, provided the usual conditions hold: 

   734   types must be non-empty and the types in the term-constructors need to 

   772   the datatypes must be non-empty and they must only occur in positive 

   735   be, what is called, positive position (see \cite{}). We then take the binding

   773   position (see \cite{}). We then consider the user-specified binding 

   736   functions and define them by primitive recursion over the raw datatypes.  

   774   functions and define them by primitive recursion over the raw datatypes.

   737   binding function. 

   775 

   738 

   776   The first non-trivial step we have to generate free-variable 

   739   The first non-trivial step is to read off from the specification free-variable 

   777   functions from the specifications. The basic idea is to collect

   740   functions. There are two kinds: free-variable functions corresponding to types,

   778   all atoms that are not bound, but because of the rather complicated

   741   written $\fv\_ty$, and  free-variable functions corresponding to binding functions,

   779   binding mechanisms the details are somewhat involved.

   742   written $\fv\_bn$. They have to be defined at the same time since there can

   780   There are two kinds of free-variable functions: one corresponds to types,

   743   be interdependencies. Given a term-constructor $C\_raw\;ty_1 \ldots ty_n$ and some 

   781   written $\fv\_ty$, and the other corresponds to binding functions,

   744   binding clauses, the function $\fv (C\_raw\;x_1 \ldots x_n)$ will be the union 

   782   written $\fv\_bn$. They have to be defined at the same time, since there can

   745   of the values generated for each argument, say $x_i$, as follows:

   783   be dependencies between them. 

   746 

   784 

   747   \begin{center}

   785   Given a term-constructor $C\_raw\;ty_1 \ldots ty_n$, of type $ty$ together with 

   748   \begin{tabular}{cp{8cm}}

   786   some  binding clauses, the function $\fv\_ty (C\_raw\;x_1 \ldots x_n)$ will be 

   749   $\bullet$ & if it is a shallow binder, then $\varnothing$\\

   787   the union of the values generated for each argument, say $x_i$ with type $ty_i$. 

   750   $\bullet$ & if it is a deep binder, then $\fv_bn x_i$\\

   788   By the binding clause we know whether the argument $x_i$ is a shallow or deep

   751   $\bullet$ & if 

   789   binder and in the latter case also whether it is a recursive or non-recursive  

   752   \end{tabular}

   790   of a binder. In these cases we return as value: 

   753   \end{center}

   791 

   754 

   792   \begin{center}

   755 

   793   \begin{tabular}{cp{7cm}}

   794   $\bullet$ & @{term "{}"} provided @{text "x\<^isub>i"} is a shallow binder\\

   795   $\bullet$ & @{text "fv_bn_ty\<^isub>i x\<^isub>i"} provided @{text "x\<^isub>i"} is a deep non-recursive binder\\

   796   $\bullet$ & @{text "fv_ty\<^isub>i x\<^isub>i - bn_ty\<^isub>i x\<^isub>i"} provided @{text "x\<^isub>i"} is a deep recursive binder\\

   797   \end{tabular}

   798   \end{center}

   799 

   800   \noindent

   801   The binding clause will also give us whether the argument @{term "x\<^isub>i"} is

   802   a body of one or more abstractions. There are two cases: either the 

   803   corresponding binders are all shallow or there is a single deep binder. 

   804   In the former case we build the union of all shallow binders; in the 

   805   later case we just take set or list of atoms the specified binding

   806   function returns. Below use @{text "bnds"} to stand for them. 

   807  

   808   \begin{center}

   809   \begin{tabular}{cp{7cm}}

   810   $\bullet$ & @{text "{atom x\<^isub>i} - bnds"} provided @{term "x\<^isub>i"} is an atom\\

   811   $\bullet$ & @{text "(atoms x\<^isub>i) - bnds"} provided @{term "x\<^isub>i"} is a set of atoms\\

   812   $\bullet$ & @{text "(atoml x\<^isub>i) - bnds"} provided @{term "x\<^isub>i"} is a list of atoms\\

   813   $\bullet$ & @{text "(fv_ty\<^isub>i x\<^isub>i) - bnds"} provided @{term "ty\<^isub>i"} is a nominal datatype\\

   814   $\bullet$ & @{term "{}"} otherwise 

   815   \end{tabular}

   816   \end{center}

   817 

   818   \noindent

   819   If the argument is neither a binder, nor a body, then it is defined as

   820   the four clauses above, except that @{text "bnds"} is empty. i.e.~no atoms

   821   are abstracted.