
diff -r f296ef291ca9 -r 36aeb97fabb0 Paper/Paper.thy
--- a/Paper/Paper.thy	Thu Jul 01 01:53:00 2010 +0100
+++ b/Paper/Paper.thy	Thu Jul 01 14:18:36 2010 +0100
@@ -46,7 +46,7 @@
 %%%  @{text "(1, (2, 3))"}
 
   So far, Nominal Isabelle provides a mechanism for constructing
-  $\alpha$-equated terms, for example
+  $\alpha$-equated terms, for example lambda-terms
 
   \begin{center}
   @{text "t ::= x | t t | \<lambda>x. t"}
@@ -365,9 +365,9 @@
   terms, including properties about support, freshness and equality
   conditions for $\alpha$-equated terms. We are also able to derive strong 
   induction principles that have the variable convention already built in.
-  The concepts behind our specifications of general binders are taken 
+  The method behind our specification of general binders is taken 
   from the Ott-tool, but we introduce restrictions, and also one extension, so 
-  that the specifications make sense for reasoning about $\alpha$-equated terms. 
+  that our specifications make sense for reasoning about $\alpha$-equated terms. 
 
 
   \begin{figure}
@@ -567,9 +567,9 @@
   @{text "x R y"} \;\;\textit{implies}\;\; @{text "(p \<bullet> x) R (p \<bullet> y)"}
   \end{center}
 
-  Finally, the nominal logic work provides us with general means to rename 
+  Finally, the nominal logic work provides us with general means for renaming 
   binders. While in the older version of Nominal Isabelle, we used extensively 
-  Property~\ref{swapfreshfresh} for renaming single binders, this property 
+  Property~\ref{swapfreshfresh} to rename single binders, this property 
   proved too unwieldy for dealing with multiple binders. For such binders the 
   following generalisations turned out to be easier to use.
 
@@ -628,7 +628,7 @@
   {\it (iii)} ``moves'' their bound names so that we obtain modulo a relation,
   say \mbox{@{text "_ R _"}}, two equivalent terms. We also require that {\it (iv)}
   @{text p} makes the sets of abstracted atoms @{text as} and @{text bs} equal. The
-  requirements {\it i)} to {\it iv)} can be stated formally as follows:
+  requirements {\it (i)} to {\it (iv)} can be stated formally as follows:
   %
   \begin{equation}\label{alphaset}
   \begin{array}{@ {\hspace{10mm}}r@ {\hspace{2mm}}l@ {\hspace{4mm}}r}
@@ -739,7 +739,7 @@
   \end{proof}
 
   \noindent
-  This lemma allows us to use our quotient package and introduce 
+  This lemma allows us to use our quotient package for introducing 
   new types @{text "\<beta> abs_set"}, @{text "\<beta> abs_res"} and @{text "\<beta> abs_list"}
   representing $\alpha$-equivalence classes of pairs of type 
   @{text "(atom set) \<times> \<beta>"} (in the first two cases) and of type @{text "(atom list) \<times> \<beta>"}
@@ -913,9 +913,9 @@
 
   \begin{center}
   \begin{tabular}{l}
-  \isacommand{bind}\; {\it binders}\; \isacommand{in}\; {\it labels}\\
-  \isacommand{bind\_set}\; {\it binders}\; \isacommand{in}\; {\it labels}\\
-  \isacommand{bind\_res}\; {\it binders}\; \isacommand{in}\; {\it labels}\\
+  \isacommand{bind}\; {\it binders}\; \isacommand{in}\; {\it bodies}\\
+  \isacommand{bind\_set}\; {\it binders}\; \isacommand{in}\; {\it bodies}\\
+  \isacommand{bind\_res}\; {\it binders}\; \isacommand{in}\; {\it bodies}\\
   \end{tabular}
   \end{center}
 
@@ -923,8 +923,8 @@
   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 the
   cardinality does) and the last is for sets of binders (with vacuous binders
-  preserving $\alpha$-equivalence). The ``\isacommand{in}-part'' of a binding
-  clause will be called \emph{bodies} (there can be more than one); the
+  preserving $\alpha$-equivalence). As indicated, the ``\isacommand{in}-part'' of a binding
+  clause will be called \emph{bodies}; the
   ``\isacommand{bind}-part'' will be called \emph{binders}. In contrast to
   Ott, we allow multiple labels in binders and bodies. For example we allow
   binding clauses of the form:
@@ -940,25 +940,28 @@
   \end{center}
 
   \noindent
-  Similarly for the other binding modes. Interestingly, in case of \isacommand{bind\_set}
-  and \isacommand{bind\_res} the binding clauses above will make a difference to the semantics
-  of the specifications (the corresponding $\alpha$-equivalence will differ). We will 
-  show this later with an example.
+  Similarly for the other binding modes. 
+  %Interestingly, in case of \isacommand{bind\_set}
+  %and \isacommand{bind\_res} the binding clauses above will make a difference to the semantics
+  %of the specifications (the corresponding $\alpha$-equivalence will differ). We will 
+  %show this later with an example.
   
-  There are some restrictions we need to impose on binding clauses: the main idea behind 
-  these restrictions is that we obtain a sensible notion of $\alpha$-equivalence where
-  it is ensured that a bound variable cannot be free at the same time.  First, a
-  body can only occur in \emph{one} binding clause of a term constructor (this ensures
-  that the bound variables of a body cannot be free at the same time by specifying 
-  an alternative binder for the body). For
-  binders we distinguish between \emph{shallow} and \emph{deep} binders.
-  Shallow binders are just labels. The restriction we need to impose on them
-  is that in case of \isacommand{bind\_set} and \isacommand{bind\_res} the
-  labels must either refer to atom types or to sets of atom types; in case of
-  \isacommand{bind} the labels must refer to atom types or lists of atom
-  types. Two examples for the use of shallow binders are the specification of
-  lambda-terms, where a single name is bound, and type-schemes, where a finite
-  set of names is bound:
+  There are also some restrictions we need to impose on binding clauses: the
+  main idea behind these restrictions is that we obtain a sensible notion of
+  $\alpha$-equivalence where it is ensured that within a given scope a 
+  variable occurence cannot be bound and free at the same time.  First, a body can only occur in
+  \emph{one} binding clause of a term constructor (this ensures that the bound
+  variables of a body cannot be free at the same time by specifying an
+  alternative binder for the body). For binders we distinguish between
+  \emph{shallow} and \emph{deep} binders.  Shallow binders are just
+  labels. The restriction we need to impose on them is that in case of
+  \isacommand{bind\_set} and \isacommand{bind\_res} the labels must either
+  refer to atom types or to sets of atom types; in case of \isacommand{bind}
+  the labels must refer to atom types or lists of atom types. Two examples for
+  the use of shallow binders are the specification of lambda-terms, where a
+  single name is bound, and type-schemes, where a finite set of names is
+  bound:
+
 
   \begin{center}
   \begin{tabular}{@ {}cc@ {}}
@@ -994,11 +997,10 @@
   \emph{recursive}, see below). The binding functions are
   expected to return either a set of atoms (for \isacommand{bind\_set} and
   \isacommand{bind\_res}) or a list of atoms (for \isacommand{bind}). They can
-  be defined by primitive recursion over the corresponding type; the equations
+  be defined by recursion over the corresponding type; the equations
   must be given in the binding function part of the scheme shown in
   \eqref{scheme}. For example a term-calculus containing @{text "Let"}s with
   tuple patterns might be specified as:
-
   %
   \begin{equation}\label{letpat}
   \mbox{%
@@ -1042,7 +1044,7 @@
   binders \emph{recursive}.  To see the purpose of such recursive binders,
   compare ``plain'' @{text "Let"}s and @{text "Let_rec"}s in the following
   specification:
-
+  %
   \begin{equation}\label{letrecs}
   \mbox{%
   \begin{tabular}{@ {}l@ {}}
@@ -1065,10 +1067,10 @@
   The difference is that with @{text Let} we only want to bind the atoms @{text
   "bn(as)"} in the term @{text t}, but with @{text "Let_rec"} we also want to bind the atoms
   inside the assignment. This difference has consequences for the free-variable 
-  function and $\alpha$-equivalence relation, which we are going to define below.
+  function and $\alpha$-equivalence relation, which we are going to define later.
   
   To make sure that variables bound by deep binders cannot be free at the
-  same time, we have to impose some restrictions. First,
+  same time, we have to impose some further restrictions. First,
   we cannot have more than one binding function for one binder. So we exclude:
 
   \begin{center}
@@ -1082,6 +1084,10 @@
   \end{center}
 
   \noindent
+  Otherwise it is be possible that @{text "bn\<^isub>1"} and @{text "bn\<^isub>2"}  pick 
+  out different atoms to become bound in @{text "p"}.
+  
+
   We also need to restrict the form of the binding functions. As will shortly
   become clear, we cannot return an atom in a binding function that is also
   bound in the corresponding term-constructor. That means in the example
@@ -1089,7 +1095,8 @@
   not have a binding clause (all arguments are used to define @{text "bn"}).
   In contrast, in case of \eqref{letrecs} the term-constructor @{text ACons}
   may have a binding clause involving the argument @{text t} (the only one that
-  is \emph{not} used in the definition of the binding function).  
+  is \emph{not} used in the definition of the binding function). This restriction
+  means that we can lift the binding function to $\alpha$-equated terms.
 
   In the version of
   Nominal Isabelle described here, we also adopted the restriction from the
@@ -1099,7 +1106,8 @@
   (case @{text PTup}). This restriction will simplify some automatic definitions and proofs
   later on.
   
-  In order to simplify our definitions, we shall assume specifications 
+  In order to simplify our definitions of free variables and $\alpha$-equivalence, 
+  we shall assume specifications 
   of term-calculi are implicitly \emph{completed}. By this we mean that  
   for every argument of a term-constructor that is \emph{not} 
   already part of a binding clause given by the user, we add implicitly a special \emph{empty} binding
@@ -1132,9 +1140,11 @@
   Pottier and Cheney pointed out \cite{Pottier06,Cheney05}, just 
   re-arranging the arguments of
   term-constructors so that binders and their bodies are next to each other will 
-  result in inadequate representations. Therefore we will first
+  result in inadequate representations in cases like @{text "Let x\<^isub>1=t\<^isub>1\<dots>x\<^isub>n=t\<^isub>n in s"}. 
+  Therefore we will first
   extract datatype definitions from the specification and then define 
-  explicitly an $\alpha$-equivalence relation over them.
+  explicitly an $\alpha$-equivalence relation over them. We subsequently
+  quotient the datatypes according to our $\alpha$-equivalence.
 
 
   The datatype definition can be obtained by stripping off the 
@@ -1158,28 +1168,33 @@
   non-empty and the types in the constructors only occur in positive 
   position (see \cite{Berghofer99} for an indepth description of the datatype package
   in Isabelle/HOL). We then define the user-specified binding 
-  functions, called @{term "bn"}, by primitive recursion over the corresponding 
+  functions, called @{term "bn"}, by recursion over the corresponding 
   raw datatype. We can also easily define permutation operations by 
-  primitive recursion so that for each term constructor @{text "C ty\<^isub>1 \<dots> ty\<^isub>n"} 
-  we have that
+  recursion so that for each term constructor @{text "C"} with the 
+  argument types @{text "ty"}$_{1..n}$ we have that
   %
   \begin{equation}\label{ceqvt}
   @{text "p \<bullet> (C z\<^isub>1 \<dots> z\<^isub>n) = C (p \<bullet> z\<^isub>1) \<dots> (p \<bullet> z\<^isub>n)"}
   \end{equation}
+
+  \noindent
+  where the variables @{text "z"}$_{1..n}$ are of types @{text "ty"}$_{1..n}$.
   
   The first non-trivial step we have to perform is the generation of
-  free-variable functions from the specifications. Given the raw types @{text
-  "ty\<^isub>1 \<dots> ty\<^isub>n"} derived from a specification, we define the
-  free-variable functions
-
-  \begin{center}
+  free-variable functions from the specifications. Given a raw term, these 
+  functions return sets of atoms. Assuming a nominal datatype
+  specification as in \eqref{scheme} and its \emph{raw} types @{text "ty"}$_{1..n}$, 
+  we define the free-variable functions
+  %
+  \begin{equation}\label{fvars}
   @{text "fv_ty\<^isub>1, \<dots>, fv_ty\<^isub>n"}
-  \end{center}
+  \end{equation}
 
   \noindent
   We define them together with auxiliary free-variable functions for
-  the binding functions. Given raw binding functions @{text "bn\<^isub>1 \<dots> bn\<^isub>m"} we define
-  
+  the binding functions. Given raw binding functions @{text "bn"}$_{1..m}$ 
+  we define
+  %
   \begin{center}
   @{text "fv_bn\<^isub>1, \<dots>, fv_bn\<^isub>m"}
   \end{center}
@@ -1187,32 +1202,65 @@
   \noindent
   The reason for this setup is that in a deep binder not all atoms have to be
   bound, as we saw in the example with ``plain'' @{text Let}s. We need therefore a function
-  that calculates those unbound atoms. 
+  that calculates those unbound atoms in a deep binder.
+
+  While the idea behind these free-variable functions is clear (they just
+  collect all atoms that are not bound), because of our rather complicated
+  binding mechanisms their definitions are somewhat involved.  Given a
+  term-constructor @{text "C"} of type @{text ty} and some associated binding
+  clauses @{text "bc\<^isub>1\<dots>bc\<^isub>k"}, the result of the @{text "fv_ty (C z\<^isub>1 \<dots> z\<^isub>n)"} will be
+  the union @{text "fv(bc\<^isub>1) \<union> \<dots> \<union> fv(bc\<^isub>k)"} of free variables calculated for 
+  each binding clause. Given a binding clause @{text bc} is of the form
+  %
+  \begin{equation}
+  \mbox{\isacommand{bind} @{text "b\<^isub>1\<dots>b\<^isub>p"} \isacommand{in} @{text "d\<^isub>1\<dots>d\<^isub>q"}}
+  \end{equation}
 
-  For atomic types we define the auxiliary
-  free variable functions:
+  \noindent
+  where the body labels @{text "d"}$_{1..q}$ refer to types @{text ty}$_{1..q}$; the binders 
+  @{text b}$_{1..p}$
+  either refer to labels of atom types (in case of shallow binders) or to binding 
+  functions taking a single label as argument (in case of deep binders). Assuming the
+  free variables of the bodies is the set @{text "D"}, the bound variables of the binders 
+  is the set @{text B} and the free variables of the non-recursive deep binders is @{text "B'"}
+  then the free variables of the binding clause @{text bc} is
+  %
+  \begin{center}
+  @{text "fv(bc) = (D - B) \<union> B'"}
+  \end{center}
+
+  \noindent
+  Formally the set @{text D} is the union of the free variables for the bodies
+  %
+  \begin{center}
+  @{text "D = fv_ty\<^isub>1 d\<^isub>1 \<union> ... \<union> fv_ty\<^isub>q d\<^isub>q"}
+  \end{center} 
+
+  \noindent
+  whereby the free variable functions @{text "fv_ty\<^isub>i"} are the ones in \eqref{fvars}
+  provided the @{text "d\<^isub>i"} refers to one of the types @{text "ty"}$_{1..n}$; 
+  otherwise we set @{text "fv_ty\<^isub>i d\<^isub>i = supp d\<^isub>i"}.
+
+
+if @{text "d\<^isub>i"} is a label
+  for an atomic type we use the following auxiliary free variable functions
 
   \begin{center}
   \begin{tabular}{r@ {\hspace{2mm}}c@ {\hspace{2mm}}l}
-  @{text "fv_atom a"} & @{text "="} & @{text "atom a"}\\
+  @{text "fv_atom a"} & @{text "="} & @{text "{atom a}"}\\
   @{text "fv_atom_set as"} & @{text "="} & @{text "atoms as"}\\
   @{text "fv_atom_list as"} & @{text "="} & @{text "atoms (set as)"}\\
   \end{tabular}
   \end{center}
 
   \noindent 
-  Like the coercion function @{text atom}, @{text "atoms"} coerces 
+  In these functions, @{text "atoms"}, like @{text "atom"}, coerces 
   the set of atoms to a set of the generic atom type.
-  It is defined as @{text "atoms as \<equiv> {atom a | a \<in> as}"}.
+  It is defined as @{text "atoms as \<equiv> {atom a | a \<in> as}"}. Otherwise
+  
 
 
-  While the idea behind these free-variable functions is clear (they just
-  collect all atoms that are not bound), because of our rather complicated
-  binding mechanisms their definitions are somewhat involved.  Given a
-  term-constructor @{text "C"} of type @{text ty} and some associated binding
-  clauses @{text bcs}, the result of the @{text "fv_ty (C z\<^isub>1 \<dots> z\<^isub>n)"} will be
-  the union of the values, @{text v}, calculated by the rules for empty, shallow and
-  deep binding clauses: 
+the values, @{text v}, calculated by the rules for each bining clause:
   %
   \begin{equation}\label{deepbinderA}
   \mbox{%
@@ -1965,7 +2013,7 @@
   The most closely related work to the one presented here is the Ott-tool
   \cite{ott-jfp} and the C$\alpha$ml language \cite{Pottier06}. Ott is a nifty
   front-end for creating \LaTeX{} documents from specifications of
-  term-calculi involving general binders. For a subset of the specifications,
+  term-calculi involving general binders. For a subset of the specifications
   Ott can also generate theorem prover code using a raw representation of
   terms, and in Coq also a locally nameless representation. The developers of
   this tool have also put forward (on paper) a definition for
@@ -2043,7 +2091,7 @@
   representing terms with general binders inside OCaml. This language is
   implemented as a front-end that can be translated to OCaml with a help of
   a library. He presents a type-system in which the scope of general binders
-  can be indicated with some special constructs, written @{text "inner"} and 
+  can be indicated with some special markers, written @{text "inner"} and 
   @{text "outer"}. With this, it seems, our and his specifications can be
   inter-translated, but we have not proved this. However, we believe the
   binding specifications in the style of Ott are a more natural way for 




