531   Our specifications for term-calculi are heavily

   531   Our specifications for term-calculi are heavily inspired by the existing

   532   inspired by the syntax of the Ott-tool \cite{ott-jfp}. A specification is

   532   datatype package of Isabelle/HOL and by the syntax of the Ott-tool

   533   a collection of (possibly mutual recursive) type declarations, say

   533   \cite{ott-jfp}. A specification is a collection of (possibly mutual

   534   $ty^\alpha_1$, $ty^\alpha_2$, \ldots $ty^\alpha_n$, and an

   534   recursive) type declarations, say @{text "ty"}$^\alpha_1$, \ldots, 

   535   associated collection of binding functions, say

   535   @{text ty}$^\alpha_n$, and an associated collection

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

   536   of binding functions, say @{text bn}$^\alpha_1$, \ldots, @{text

   537   for such specifications is rougly as follows:

   537   bn}$^\alpha_m$. The syntax in Nominal Isabelle for such specifications is

   538   rougly as follows:

   544   \isacommand{nominal\_datatype} $ty^\alpha_1 = \ldots$\\

   545   \isacommand{nominal\_datatype} @{text ty}$^\alpha_1 = \ldots$\\

   545   \isacommand{and} $ty^\alpha_2 = \ldots$\\

   546   \isacommand{and} @{text ty}$^\alpha_2 = \ldots$\\

   547   \isacommand{and} $ty^\alpha_n = \ldots$\\ 

   548   \isacommand{and} @{text ty}$^\alpha_n = \ldots$\\ 

   553   \isacommand{with} $bn^\alpha_1$ \isacommand{and} \ldots \isacommand{and} $bn^\alpha_m$

   554   \isacommand{with} @{text bn}$^\alpha_1$ \isacommand{and} \ldots \isacommand{and} @{text bn}$^\alpha_m$\\

   554   $\ldots$\\

   563   Every type declaration $ty^\alpha_i$ consists of a collection of 

   563   Every type declaration @{text ty}$^\alpha_{1..n}$ consists of a collection of 

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

   566   For example a term-constructor @{text "C\<^sup>\<alpha>"} might have

   567 

   567 

   568   \begin{center}

   568   \begin{center}

   569   $C^\alpha\;label_1\!::\!ty'_1\;\ldots label_l\!::\!ty'_l\;\;\textit{binding\_clauses}$ 

   569   @{text "C\<^sup>\<alpha> label\<^isub>1::ty"}$'_1$ @{text "\<dots> label\<^isub>l::ty"}$'_l\;\;$  @{text "binding_clauses"} 

   570   \end{center}

   570   \end{center}

   571   

   571   

   572   \noindent

   572   \noindent

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

   573   whereby some of the @{text ty}$'_{1..l}$ (or their components) are contained in the collection

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

   574   of @{text ty}$^\alpha_{1..n}$ declared in \eqref{scheme}. In this case we will call the

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

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

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

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

   591   of binders (the order does not matter, but cardinality does) and the last is for  

   591   of binders (the order does not matter, but the cardinality does) and the last is for  

   596   \isacommand{in}\; {\it another\_label} (similar for the other two modes). The

   596   \isacommand{in}\; {\it label'} (similar for the other two modes). The

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

   599   list of an atom type. Two examples for the use of shallow binders are the

   600   a single name is bound, and type-schemes, where a finite set of names is

   600   specification of lambda-terms, where a single name is bound, and of

   601   bound, use shallow binders (the type \emph{name} is an atom type):

   601   type-schemes, where a finite set of names is bound:

   624   the term-constructor Foo$_0$

   625   the following term-constructor

   628   \it {\rm Foo}$_0$ x::name y::name t::lam & \it 

   629   \it {\rm Foo} x::name y::name t::lam & \it 

   636   have in the first binding clause the mode \isacommand{bind} and in the second 

   637   have, for instance, in the first binding clause the mode \isacommand{bind} 

   637   \isacommand{bind\_set}.

   638   and in the second \isacommand{bind\_set}.

   642   call such binders \emph{recursive}). 

   643   call such binders \emph{recursive}, see below). 

   648   with tuple patterns, you might declare

   649   with tuple patterns, you might specify

   660   \hspace{5mm}\phantom{$\mid$} PNo\\

   661   \hspace{5mm}\phantom{$\mid$} PNil\\

   661   \hspace{5mm}$\mid$ PVr\;{\it name}\\

   662   \hspace{5mm}$\mid$ PVar\;{\it name}\\

   662   \hspace{5mm}$\mid$ PPr\;{\it pat}\;{\it pat}\\ 

   663   \hspace{5mm}$\mid$ PTup\;{\it pat}\;{\it pat}\\ 

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

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

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

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

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

   667   \hspace{5mm}$\mid$ $\textit{bn}(\textrm{PTup}\;p_1\;p_2) = \textit{bn}(p_1)\; @\;\textit{bn}(p_2)$\\ 

   667   \end{tabular}

   668   \end{tabular}

   668   \end{center}

   669   \end{center}

   669   

   670   

   670   \noindent

   671   \noindent

   671   In this specification the function $atom$ coerces a name into the generic

   672   In this specification the function @{text "bn"} determines which atoms of @{text  p} are

   672   atom type of Nominal Isabelle. This allows us to treat binders of different

   673   bound in the argument @{text "t"}. Note that the second last clause the function @{text "atom"}

   673   atom type uniformly. As will shortly become clear, we cannot return an atom in a

   674   coerces a name into the generic atom type of Nominal Isabelle. This allows

   674   binding function that also is bound in the term-constructor. In the present

   675   us to treat binders of different atom type uniformly. 

   675   version of Nominal Isabelle, we adopted the restriction the Ott-tool imposes

   676 

   676   on the binding functions, namely a binding function can only return the

   677   As will shortly become clear, we cannot return an atom in a binding function

   677   empty set (case PNil), a singleton set containing an atom (case PVar) or

   678   that is also bound in the corresponding term-constructor. That means in the

   678   unions of atom sets (case PPrd). Moreover, as with shallow binders, deep

   679   example above that the term-constructors PVar and PTup must not have a

   679   binders with shared body need to have the same binding mode. Finally, the

   680   binding clause.  In the present version of Nominal Isabelle, we also adopted

   680   most drastic restriction we have to impose on deep binders is that we cannot

   681   the restriction from the Ott-tool that binding functions can only return:

   681   have ``overlapping'' deep binders. Consider for example the term-constructors:

   682   the empty set or empty list (as in case PNil), a singleton set or singleton

   683   list containing an atom (case PVar), or unions of atom sets or appended atom

   684   lists (case PTup). This restriction will simplify proofs later on.

   685   The the most drastic restriction we have to impose on deep binders is that 

   686   we cannot have ``overlapping'' deep binders. Consider for example the 

   687   term-constructors:

   685   \it {\rm Foo}$_1$ p::pat q::pat t::trm & \it \isacommand{bind}\;bn(p)\;\isacommand{in}\;t,\;

   691   \it {\rm Foo} p::pat q::pat t::trm & \it \isacommand{bind}\;bn(p)\;\isacommand{in}\;t,\;

   687   \it {\rm Foo}$_2$ x::name p::pat t::trm & \it \it \isacommand{bind}\;x\;\isacommand{in}\;t,\;

   693   \it {\rm Foo}$'$x::name p::pat t::trm & \it \it \isacommand{bind}\;x\;\isacommand{in}\;t,\;

   694   In the first case we bind all atoms from the pattern $p$ in $t$ and also all atoms 

   700   In the first case we bind all atoms from the pattern @{text p} in @{text t}

   695   from $q$ in $t$. As a result we have no way to determine whether the binder came from the

   701   and also all atoms from @{text q} in @{text t}. As a result we have no way

   696   binding function in $p$ or $q$. Similarly in the second case:

   702   to determine whether the binder came from the binding function @{text

   697   the binder $bn(p)$ overlaps with the shallow binder $x$. We must exclude such specifiactions, 

   703   "bn(p)"} or @{text "bn(q)"}. Similarly in the second case. There the binder

   698   as we will not be able to represent them using the general binders described in 

   704   @{text "bn(p)"} overlaps with the shallow binder @{text x}. The reason why

   699   Section \ref{sec:binders}. However the following two term-constructors are allowed:

   705   we must exclude such specifiactions is that they cannot be represent by

   706   the general binders described in Section \ref{sec:binders}. However

   707   the following two term-constructors are allowed

   703   \it {\rm Bar}$_1$ p::pat t::trm s::trm & \it \isacommand{bind}\;bn(p)\;\isacommand{in}\;t,\;

   711   \it {\rm Bar} p::pat t::trm s::trm & \it \isacommand{bind}\;bn(p)\;\isacommand{in}\;t,\;

   705   \it {\rm Bar}$_2$ p::pat t::trm &  \it \isacommand{bind}\;bn(p)\;\isacommand{in}\;p,\;

   713   \it {\rm Bar}$'$p::pat t::trm &  \it \isacommand{bind}\;bn(p)\;\isacommand{in}\;p,\;

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

   721   Note that in the last example we wrote {\it\isacommand{bind}\;bn(p)\;\isacommand{in}\;p}.

   714   A specification for them looks as follows:

   722   Whenver such a binding clause is present, we will call the binder \emph{recursive}.

   715 

   723   To see the purpose for this, consider ``plain'' Lets and Let\_recs:

   716   \begin{center}

   724 

   717   \begin{tabular}{l}

   725   \begin{center}

   726   \begin{tabular}{@ {}l@ {}}

   732   The intention with this specification is to bind all variables 

   744   The difference is that with Let we only want to bind the atoms @{text

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

   745   "bn(a)"} in the term @{text t}, but with Let\_rec we also want to bind the atoms

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

   746   inside the assignment. This requires recursive binders and also has

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

   747   consequences for the free variable function and alpha-equivalence relation,

   736   this case we need to specify

   748   which we are going to explain in the rest of this section.

   737 

   749  

   738   \begin{center}

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

   739   \begin{tabular}{l}

   751   specifications into actual type definitions in Isabelle/HOL and then

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

   752   establish a reasoning infrastructure for them. Because of the problem

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

   753   Pottier and Cheney pointed out, we cannot in general re-arrange arguments of

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

   754   term-constructors so that binders and their bodies are next to each other, and

   743   \end{tabular}

   755   then use the type constructors @{text "abs_set"}, @{text "abs_res"} and

   744   \end{center}

   756   @{text "abs_list"} from Section \ref{sec:binders}. Therefore we will first

   745   

   757   extract datatype definitions from the specification and then define an

   746   \noindent

   758   alpha-equiavlence relation over them.

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

   759 

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

   760 

   749 

   761   The datatype definition can be obtained by just stripping off the 

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

   751   specifications into actual type

   752   definitions in Isabelle/HOL and then establish a reasoning infrastructure 

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

   754   in general re-arrange arguments of term-constructors so that binders and 

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

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

   757   \ref{sec:binders}. Therefore

   758   we will first extract datatype definitions from the specification and

   759   then define an alpha-equiavlence relation over them.

   760 

   761   The datatype definition can be obtained by just stripping of the 

   763   new names for the types, $ty^\alpha$ and term-constructors $C^\alpha$

   763   new names for the types @{text "ty\<^sup>\<alpha>"} and term-constructors @{text "C\<^sup>\<alpha>"}

   764   given by user. We just use an affix like

   764   given by user. In our implementation we just use an affix like

   765 

   765 

   766   \begin{center}

   766   \begin{center}

   767   $ty^\alpha \mapsto ty\_raw  \qquad C^\alpha \mapsto C\_raw$

   767   @{text "ty\<^sup>\<alpha> \<mapsto> ty_raw"} \hspace{7mm} @{text "C\<^sup>\<alpha> \<mapsto> C_raw"}

   768   \end{center}

   768   \end{center}

   769   

   769   

   770   \noindent

   770   \noindent

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

   771   The resulting datatype definition is legal in Isabelle/HOL provided the datatypes are 

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

   772   non-empty and the types in the constructors only occur in positive 

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

   773   position (see \cite{} for an indepth explanataion of the datatype package

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

   774   in Isabelle/HOL). We then define the user-specified binding 

   775 

   775   functions by primitive recursion over the raw datatypes. We can also

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

   776   easily define a permutation operation by primitive recursion so that for each

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

   777   term constructor @{text "C_raw ty\<^isub>1 \<dots> ty\<^isub>n"} we have that

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

   778 

   779   binding mechanisms the details are somewhat involved.

   779   \begin{center}

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

   780   @{text "p \<bullet> (C_raw x\<^isub>1 \<dots> x\<^isub>n) \<equiv> C_raw (p \<bullet> x\<^isub>1) \<dots> (p \<bullet> x\<^isub>n)"}

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

   781   \end{center}

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

   782   

   783   be dependencies between them. 

   783   \noindent

   784 

   784   From this definition we can easily show that the raw datatypes are 

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

   785   all permutation types (Def ??) by a simple structural induction over

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

   786   the @{text "ty_raw"}s.

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

   787 

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

   788   The first non-trivial step we have to perform is the generatation free-variable 

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

   789   functions from the specifications. Given types @{text "ty\<^isub>1, \<dots>, ty\<^isub>n"}

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

   790   we need to define the free-variable functions

   791 

   792   \begin{center}

   793   @{text "fv_ty\<^isub>1 :: ty\<^isub>1 \<Rightarrow> atom set \<dots> fv_ty\<^isub>n :: ty\<^isub>n \<Rightarrow> atom set"}

   794   \end{center}

   795 

   796   \noindent

   797   and given binding functions @{text "bn_ty\<^isub>1, \<dots>, bn_ty\<^isub>m"} we also need to define 

   798   the free-variable functions

   799 

   800   \begin{center}

   801   @{text "fv_bn_ty\<^isub>1 :: ty\<^isub>1 \<Rightarrow> atom set \<dots> fv_bn_ty\<^isub>m :: ty\<^isub>m \<Rightarrow> atom set"}

   802   \end{center}

   803 

   804   \noindent

   805   The basic idea behind these free-variable functions is to collect all atoms

   806   that are not bound in a term constructor, but because of the rather

   807   complicated binding mechanisms the details are somewhat involved. 

   808 

   809   Given a term-constructor @{text "C_raw ty\<^isub>1 \<dots> ty\<^isub>n"}, of type @{text ty} together with 

   810   some  binding clauses, the function @{text "fv_ty (C_raw x\<^isub>1 \<dots> x\<^isub>n)"} will be 

   811   the union of the values defined below for each argument, say @{text "x\<^isub>i"} with type @{text "ty\<^isub>i"}. 

   812   From the binding clause of this term constructor, we can determine whether the 

   813   argument @{text "x\<^isub>i"} is a shallow or deep binder, and in the latter case also 

   814   whether it is a recursive or non-recursive of a binder. In these cases the value is: 

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

   825   In case the argument @{text "x\<^isub>i"} is not a binder, it might be a body of

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

   826   one or more abstractions. There are two cases: either the 

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

   830   function returns. Let @{text "bnds"} be an abbreviation of the bound

   831   atoms. Then the value is given by:  

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

   844   If the argument is neither a binder, nor a body of an abstraction, then the 

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

   845   value is defined as above, except that @{text "bnds"} is empty. i.e.~no atoms

   825 

   874 section {* The Lifting of Definitions and Properties *}