
diff -r 8b4595cb5524 -r d5b223b9c2bb Paper/Paper.thy
--- a/Paper/Paper.thy	Wed Mar 24 18:02:33 2010 +0100
+++ b/Paper/Paper.thy	Wed Mar 24 19:50:42 2010 +0100
@@ -130,9 +130,8 @@
   programming language calculus.
 
   By providing these general binding mechanisms, however, we have to work around 
-  a problem that has been pointed out by Pottier in \cite{Pottier06} and Cheney in
-  \cite{Cheney05}: in 
-  $\mathtt{let}$-constructs of the form
+  a problem that has been pointed out by Pottier \cite{Pottier06} and Cheney 
+  \cite{Cheney05}: in $\mathtt{let}$-constructs of the form
   %
   \begin{center}
   $\LET x_1 = t_1 \AND \ldots \AND x_n = t_n \IN s \END$
@@ -533,12 +532,12 @@
   inspired by the syntax of the Ott-tool \cite{ott-jfp}. A specification is
   a collection of (possibly mutual recursive) type declarations, say
   $ty^\alpha_1$, $ty^\alpha_2$, \ldots $ty^\alpha_n$, and an
-  associated collection of binding function declarations, say
-  $bn^\alpha_1$, \ldots $bn^\alpha_m$. The syntax in Nominal Isabelle 
+  associated collection of binding functions, say
+  $bn^\alpha_1$, \ldots, $bn^\alpha_m$. The syntax in Nominal Isabelle 
   for such specifications is rougly as follows:
   %
   \begin{equation}\label{scheme}
-  \mbox{\begin{tabular}{@ {\hspace{-9mm}}p{1.8cm}l}
+  \mbox{\begin{tabular}{@ {\hspace{-5mm}}p{1.8cm}l}
   type \mbox{declaration part} &
   $\begin{cases}
   \mbox{\begin{tabular}{l}
@@ -564,20 +563,20 @@
   Every type declaration $ty^\alpha_i$ consists of a collection of 
   term-constructors, each of which comes with a list of labelled 
   types that stand for the types of the arguments of the term-constructor.
-  For example for a term-constructor $C^\alpha$ we might have
+  For example a term-constructor $C^\alpha$ might have
 
   \begin{center}
   $C^\alpha\;label_1\!::\!ty'_1\;\ldots label_l\!::\!ty'_l\;\;\textit{binding\_clauses}$ 
   \end{center}
   
   \noindent
-  whereby some of the $ty'_k$ (or their type components) are contained in the 
-  set of $ty^\alpha_i$
-  declared in \eqref{scheme}. In this case we will call
-  the corresponding argument a \emph{recursive argument}.  The labels
-  annotated on the types are optional and can be used in the (possibly empty)
-  list of \emph{binding clauses}.  These clauses indicate the binders and the
-  scope of the binders in a term-constructor.  They come in three \emph{modes}
+  whereby some of the $ty'_k$ (or their components) are contained in the collection
+  of $ty^\alpha_i$ declared in \eqref{scheme}. In this case we will call the
+  corresponding argument a \emph{recursive argument}.  The labels annotated on
+  the types are optional and can be used in the (possibly empty) list of
+  \emph{binding clauses}.  These clauses indicate the binders and the scope of
+  the binders in a term-constructor.  They come in three \emph{modes}
+
 
   \begin{center}
   \begin{tabular}{l}
@@ -588,7 +587,7 @@
   \end{center}
 
   \noindent
-  The first mode is for binding lists of atoms (the order matters); the second is for sets
+  The first mode is for binding lists of atoms (the order of binders matters); the second is for sets
   of binders (the order does not matter, but cardinality does) and the last is for  
   sets of binders (with vacuous binders preserving alpha-equivalence).
 
@@ -597,7 +596,7 @@
   \isacommand{in}\; {\it another\_label} (similar for the other two modes). The
   restriction we impose on shallow binders is that the {\it label} must either
   refer to a type that is an atom type or to a type that is a finite set or
-  list of an atom type. For example the specifications of lambda-terms, where
+  list of an atom type. For example the specifications for lambda-terms, where
   a single name is bound, and type-schemes, where a finite set of names is
   bound, use shallow binders (the type \emph{name} is an atom type):
 
@@ -638,7 +637,7 @@
   \isacommand{bind\_set}.
 
   A \emph{deep} binder uses an auxiliary binding function that ``picks'' out
-  the atoms in one argument of the term-constructor that can be bound in  
+  the atoms in one argument of the term-constructor, which can be bound in  
   other arguments and also in the same argument (we will
   call such binders \emph{recursive}). 
   The binding functions are expected to return either a set of atoms
@@ -656,15 +655,15 @@
   \hspace{5mm}$\mid$ Lam\;{\it x::name}\;{\it t::trm} 
      \;\;\isacommand{bind} {\it x} \isacommand{in} {\it t}\\
   \hspace{5mm}$\mid$ Let\;{\it p::pat}\;{\it trm}\; {\it t::trm} 
-     \;\;\isacommand{bind\_set} {\it bn(p)} \isacommand{in} {\it t}\\
+     \;\;\isacommand{bind} {\it bn(p)} \isacommand{in} {\it t}\\
   \isacommand{and} {\it pat} =\\
   \hspace{5mm}\phantom{$\mid$} PNo\\
   \hspace{5mm}$\mid$ PVr\;{\it name}\\
   \hspace{5mm}$\mid$ PPr\;{\it pat}\;{\it pat}\\ 
-  \isacommand{with} {\it bn::pat $\Rightarrow$ atom set}\\
-  \isacommand{where} $bn(\textrm{PNil}) = \varnothing$\\
-  \hspace{5mm}$\mid$ $bn(\textrm{PVar}\;x) = \{atom\; x\}$\\
-  \hspace{5mm}$\mid$ $bn(\textrm{PPrd}\;p_1\;p_2) = bn(p_1) \cup bn(p_2)$\\ 
+  \isacommand{with} {\it bn::pat $\Rightarrow$ atom list}\\
+  \isacommand{where} $bn(\textrm{PNil}) = []$\\
+  \hspace{5mm}$\mid$ $bn(\textrm{PVar}\;x) = [atom\; x]$\\
+  \hspace{5mm}$\mid$ $bn(\textrm{PPrd}\;p_1\;p_2) = bn(p_1)\; @\;bn(p_2)$\\ 
   \end{tabular}
   \end{center}
   
@@ -711,48 +710,115 @@
   \noindent
   since there is no overlap of binders.
   
-  Now the question is how we can turn specifications into actual type
+  Let us come back one more time to the specification of simultaneous lets. 
+  A specification for them looks as follows:
+
+  \begin{center}
+  \begin{tabular}{l}
+  \isacommand{nominal\_datatype} {\it trm} =\\
+  \hspace{5mm}\phantom{$\mid$}\ldots\\
+  \hspace{5mm}$\mid$ Let\;{\it a::assn}\; {\it t::trm} 
+     \;\;\isacommand{bind} {\it bn(a)} \isacommand{in} {\it t}\\
+  \isacommand{and} {\it assn} =\\
+  \hspace{5mm}\phantom{$\mid$} ANil\\
+  \hspace{5mm}$\mid$ ACons\;{\it name}\;{\it trm}\;{\it assn}\\
+  \isacommand{with} {\it bn::assn $\Rightarrow$ atom list}\\
+  \isacommand{where} $bn(\textrm{ANil}) = []$\\
+  \hspace{5mm}$\mid$ $bn(\textrm{ACons}\;x\;t\;a) = [atom\; x]\; @\; bn(a)$\\
+  \end{tabular}
+  \end{center}
+
+  \noindent
+  The intention with this specification is to bind all variables 
+  from the assignments inside the body @{text t}. However one might
+  like to consider the variant where the variables are not just
+  bound in @{term t}, but also in the assignments themselves. In
+  this case we need to specify
+
+  \begin{center}
+  \begin{tabular}{l}
+  Let\_rec\;{\it a::assn}\; {\it t::trm} 
+     \;\;\isacommand{bind} {\it bn(a)} \isacommand{in} {\it t},
+         \isacommand{bind} {\it bn(a)} \isacommand{in} {\it a}\\
+  \end{tabular}
+  \end{center}
+  
+  \noindent
+  where we bind also in @{text a} all the atoms @{text bn} returns. In this
+  case we will say the binder is a \emph{recursive binder}.
+
+  Having dealt with all syntax matters, the problem now is how we can turn 
+  specifications into actual type
   definitions in Isabelle/HOL and then establish a reasoning infrastructure 
-  for them? Because of the problem Pottier and Cheney pointed out, we cannot 
+  for them. Because of the problem Pottier and Cheney pointed out, we cannot 
   in general re-arrange arguments of term-constructors so that binders and 
-  their scopes next to each other, an then use the type constructors 
-  @{text "abs_set"}, @{text "abs_res"} and @{text "abs_list"}. Therefore
+  their bodies next to each other, an then use the type constructors 
+  @{text "abs_set"}, @{text "abs_res"} and @{text "abs_list"} from Section 
+  \ref{sec:binders}. Therefore
   we will first extract datatype definitions from the specification and
   then define an alpha-equiavlence relation over them.
 
   The datatype definition can be obtained by just stripping of the 
   binding clauses and the labels on the types. We also have to invent
   new names for the types, $ty^\alpha$ and term-constructors $C^\alpha$
-  given by user. We just use an affix:
+  given by user. We just use an affix like
 
   \begin{center}
   $ty^\alpha \mapsto ty\_raw  \qquad C^\alpha \mapsto C\_raw$
   \end{center}
   
   \noindent
-  This definition can be made, provided the usual conditions hold: the 
-  types must be non-empty and the types in the term-constructors need to 
-  be, what is called, positive position (see \cite{}). We then take the binding
-  functions and define them by primitive recursion over the raw datatypes.  
-  binding function. 
+  The datatype definition can be made, provided the usual conditions hold: 
+  the datatypes must be non-empty and they must only occur in positive 
+  position (see \cite{}). We then consider the user-specified binding 
+  functions and define them by primitive recursion over the raw datatypes.
 
-  The first non-trivial step is to read off from the specification free-variable 
-  functions. There are two kinds: free-variable functions corresponding to types,
-  written $\fv\_ty$, and  free-variable functions corresponding to binding functions,
-  written $\fv\_bn$. They have to be defined at the same time since there can
-  be interdependencies. Given a term-constructor $C\_raw\;ty_1 \ldots ty_n$ and some 
-  binding clauses, the function $\fv (C\_raw\;x_1 \ldots x_n)$ will be the union 
-  of the values generated for each argument, say $x_i$, as follows:
+  The first non-trivial step we have to generate free-variable 
+  functions from the specifications. The basic idea is to collect
+  all atoms that are not bound, but because of the rather complicated
+  binding mechanisms the details are somewhat involved.
+  There are two kinds of free-variable functions: one corresponds to types,
+  written $\fv\_ty$, and the other corresponds to binding functions,
+  written $\fv\_bn$. They have to be defined at the same time, since there can
+  be dependencies between them. 
+
+  Given a term-constructor $C\_raw\;ty_1 \ldots ty_n$, of type $ty$ together with 
+  some  binding clauses, the function $\fv\_ty (C\_raw\;x_1 \ldots x_n)$ will be 
+  the union of the values generated for each argument, say $x_i$ with type $ty_i$. 
+  By the binding clause we know whether the argument $x_i$ is a shallow or deep
+  binder and in the latter case also whether it is a recursive or non-recursive  
+  of a binder. In these cases we return as value: 
 
   \begin{center}
-  \begin{tabular}{cp{8cm}}
-  $\bullet$ & if it is a shallow binder, then $\varnothing$\\
-  $\bullet$ & if it is a deep binder, then $\fv_bn x_i$\\
-  $\bullet$ & if 
+  \begin{tabular}{cp{7cm}}
+  $\bullet$ & @{term "{}"} provided @{text "x\<^isub>i"} is a shallow binder\\
+  $\bullet$ & @{text "fv_bn_ty\<^isub>i x\<^isub>i"} provided @{text "x\<^isub>i"} is a deep non-recursive binder\\
+  $\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\\
   \end{tabular}
   \end{center}
 
+  \noindent
+  The binding clause will also give us whether the argument @{term "x\<^isub>i"} is
+  a body of one or more abstractions. There are two cases: either the 
+  corresponding binders are all shallow or there is a single deep binder. 
+  In the former case we build the union of all shallow binders; in the 
+  later case we just take set or list of atoms the specified binding
+  function returns. Below use @{text "bnds"} to stand for them. 
+ 
+  \begin{center}
+  \begin{tabular}{cp{7cm}}
+  $\bullet$ & @{text "{atom x\<^isub>i} - bnds"} provided @{term "x\<^isub>i"} is an atom\\
+  $\bullet$ & @{text "(atoms x\<^isub>i) - bnds"} provided @{term "x\<^isub>i"} is a set of atoms\\
+  $\bullet$ & @{text "(atoml x\<^isub>i) - bnds"} provided @{term "x\<^isub>i"} is a list of atoms\\
+  $\bullet$ & @{text "(fv_ty\<^isub>i x\<^isub>i) - bnds"} provided @{term "ty\<^isub>i"} is a nominal datatype\\
+  $\bullet$ & @{term "{}"} otherwise 
+  \end{tabular}
+  \end{center}
 
+  \noindent
+  If the argument is neither a binder, nor a body, then it is defined as
+  the four clauses above, except that @{text "bnds"} is empty. i.e.~no atoms
+  are abstracted.
 
 *}
 




