
diff -r 9bbf2a1f9b3f -r cfd3a7368543 Paper/Paper.thy
--- a/Paper/Paper.thy	Wed Mar 31 12:30:17 2010 +0200
+++ b/Paper/Paper.thy	Wed Mar 31 16:26:51 2010 +0200
@@ -455,8 +455,9 @@
   \end{equation}
 
   \noindent
-  Concrete permutations are built up from swappings, written as \mbox{@{text "(a
-  b)"}}, which are permutations that behave as follows:
+  Concrete permutations in Nominal Isabelle are built up from swappings, 
+  written as \mbox{@{text "(a b)"}}, which are permutations that behave 
+  as follows:
   %
   \begin{center}
   @{text "(a b) = \<lambda>c. if a = c then b else if b = c then a else c"}
@@ -496,22 +497,23 @@
   \end{property}
 
   While often the support of an object can be relatively easily 
-  described, for example\\[-6mm]
+  described, for example for atoms, products, lists, function applications, 
+  booleans and permutations\\[-6mm]
   %
   \begin{eqnarray}
   @{term "supp a"} & = & @{term "{a}"}\\
   @{term "supp (x, y)"} & = & @{term "supp x \<union> supp y"}\\
   @{term "supp []"} & = & @{term "{}"}\\
   @{term "supp (x#xs)"} & = & @{term "supp x \<union> supp xs"}\\
-  @{text "supp (f x)"} & @{text "\<subseteq>"} & @{term "supp (f, x)"}\label{suppfun}\\
+  @{text "supp (f x)"} & @{text "\<subseteq>"} & @{term "supp f \<union> supp x"}\label{suppfun}\\
   @{term "supp b"} & = & @{term "{}"}\\
   @{term "supp p"} & = & @{term "{a. p \<bullet> a \<noteq> a}"}
   \end{eqnarray}
   
   \noindent 
-  in some cases it can be difficult to establish the support precisely, and
-  only give an approximation (see \eqref{suppfun} above). Reasoning about
-  such approximations can be made precise with the notion \emph{supports}, defined 
+  in some cases it can be difficult to characterise the support precisely, and
+  only an approximation can be established (see \eqref{suppfun} above). Reasoning about
+  such approximations can be simplified with the notion \emph{supports}, defined 
   as follows:
 
   \begin{defn}
@@ -537,8 +539,8 @@
   \end{equation}
 
   \noindent or equivalently that a permutation applied to the application
-  @{text "f x"} can be moved to the argument @{text x}. That means we have for
-  all permutations @{text p}
+  @{text "f x"} can be moved to the argument @{text x}. That means for equivariant
+  functions @{text f} we have for all permutations @{text p}
   %
   \begin{equation}\label{equivariance}
   @{text "p \<bullet> f = f"} \;\;\;\textit{if and only if}\;\;\;
@@ -571,12 +573,12 @@
   of binders (being bound, or fresh, in @{text x} is ensured by the
   assumption @{term "as \<sharp>* x"}), then there exists a permutation @{text p} such that
   the renamed binders @{term "p \<bullet> as"} avoid @{text c} (which can be arbitrarily chosen
-  as long as it is finitely supported) and also it does not affect anything
+  as long as it is finitely supported) and also @{text "p"} does not affect anything
   in the support of @{text x} (that is @{term "supp x \<sharp>* p"}). The last 
   fact and Property~\ref{supppermeq} allow us to ``rename'' just the binders 
   @{text as} in @{text x}, because @{term "p \<bullet> x = x"}.
 
-  All properties given in this section are formalised in Isabelle/HOL and also
+  All properties given in this section are formalised in Isabelle/HOL and 
   most of proofs are described in \cite{HuffmanUrban10} to which we refer the
   reader. In the next sections we will make extensively use of these
   properties in order to define alpha-equivalence in the presence of multiple
@@ -720,8 +722,8 @@
   %\end{proof}
 
 
-  In the rest of this section we are going to introduce a type- and term-constructors 
-  for abstraction. For this we define 
+  In the rest of this section we are going to introduce three abstraction 
+  types. For this we define 
   %
   \begin{equation}
   @{term "abs_set (as, x) (bs, x) \<equiv> \<exists>p. alpha_gen (as, x) equal supp p (bs, x)"}
@@ -763,9 +765,9 @@
   \end{center}
 
   \noindent
-  indicating that a set or list @{text as} is abstracted in @{text x}. We will
+  indicating that a set (or list) @{text as} is abstracted in @{text x}. We will
   call the types \emph{abstraction types} and their elements
-  \emph{abstractions}. The important property we need to know is what the 
+  \emph{abstractions}. The important property we need to derive is what the 
   support of abstractions is, namely:
 
   \begin{thm}[Support of Abstractions]\label{suppabs} 
@@ -781,7 +783,7 @@
 
   \noindent
   Below we will show the first equation. The others 
-  follow similar arguments. By definition of the abstraction type @{text "abs_set"} 
+  follow by similar arguments. By definition of the abstraction type @{text "abs_set"} 
   we have 
   %
   \begin{equation}\label{abseqiff}
@@ -807,9 +809,9 @@
   \end{lemma}
 
   \begin{proof}
-  This lemma is straightforward by using \eqref{abseqiff} and observing that
+  This lemma is straightforward using \eqref{abseqiff} and observing that
   the assumptions give us @{term "(a \<rightleftharpoons> b) \<bullet> (supp x - as) = (supp x - as)"}.
-  Moreover @{text supp} and set difference are equivariant \cite{HuffmanUrban10}.
+  Moreover @{text supp} and set difference are equivariant (see \cite{HuffmanUrban10}).
   \end{proof}
 
   \noindent
@@ -851,11 +853,12 @@
   since for finite sets, @{text "S"}, we have @{thm (concl) supp_finite_atom_set[no_vars]}.
 
   Finally, taking \eqref{halfone} and \eqref{halftwo} together establishes of
-  Theorem~\ref{suppabs}. This theorem gives us confidence that our
-  abstractions behave as one expects. To consider first abstractions of the
-  form @{term "Abs as x"} is motivated by the fact that properties about them
-  can be conveninetly established at the Isabelle/HOL level.  But we can also
-  use when we deal with binding in our term-calculi specifications.
+  Theorem~\ref{suppabs}. The method of first considering abstractions of the
+  form @{term "Abs as x"} etc is motivated by the fact that properties about them
+  can be conveninetly established at the Isabelle/HOL level.  It would be
+  difficult to write custom ML-code that derives automatically such properties 
+  for every term-constructor that binds some atoms. Also the generality of
+  the definitions for alpha-equivalence will also help us in the next section.
 *}
 
 section {* Alpha-Equivalence and Free Variables\label{sec:alpha} *}
@@ -903,13 +906,15 @@
   \end{center}
   
   \noindent
-  whereby some of the @{text ty}$'_{1..l}$ (or their components) are contained in the collection
-  of @{text ty}$^\alpha_{1..n}$ declared in \eqref{scheme}. In this case we will call the
-  corresponding argument a \emph{recursive argument} of @{text "C\<^sup>\<alpha>"}.  The labels annotated on
-  the types are optional. Their purpose is to be used in the (possibly empty) list of
-  \emph{binding clauses}, which indicate the binders and their scope
-  in a term-constructor.  They come in three \emph{modes}:
-
+  whereby some of the @{text ty}$'_{1..l}$ (or their components) are contained
+  in the collection of @{text ty}$^\alpha_{1..n}$ declared in
+  \eqref{scheme}. In this case we will call the corresponding argument a
+  \emph{recursive argument} of @{text "C\<^sup>\<alpha>"}. There are ``positivity''
+  restrictions imposed in the type of such recursive arguments, which ensure
+  that the type has a set-theoretic semantics \cite{Berghofer99}.  The labels
+  annotated on the types are optional. Their purpose is to be used in the
+  (possibly empty) list of \emph{binding clauses}, which indicate the binders
+  and their scope in a term-constructor.  They come in three \emph{modes}:
 
   \begin{center}
   \begin{tabular}{l}
@@ -920,9 +925,12 @@
   \end{center}
 
   \noindent
-  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 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 the \emph{body} of the abstraction; the
+  ``\isacommand{bind}-part'' will be the \emph{binder} of the binding clause.
 
   In addition we distinguish between \emph{shallow} and \emph{deep}
   binders.  Shallow binders are of the form \isacommand{bind}\; {\it label}\;
@@ -1034,7 +1042,7 @@
   \end{center}
 
   \noindent
-  In the first case we bind all atoms from the pattern @{text p} in @{text t}
+  In the first case we might bind all atoms from the pattern @{text p} in @{text t}
   and also all atoms from @{text q} in @{text t}. As a result we have no way
   to determine whether the binder came from the binding function @{text
   "bn(p)"} or @{text "bn(q)"}. Similarly in the second case. The reason why
@@ -1081,7 +1089,7 @@
 
   \noindent
   The difference is that with @{text Let} we only want to bind the atoms @{text
-  "bn(a)"} in the term @{text t}, but with @{text "Let_rec"} we also want to bind the atoms
+  "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 describe in the 
   rest of this section.
@@ -1100,7 +1108,7 @@
   The datatype definition can be obtained by stripping off the 
   binding clauses and the labels on the types. We also have to invent
   new names for the types @{text "ty\<^sup>\<alpha>"} and term-constructors @{text "C\<^sup>\<alpha>"}
-  given by user. In our implementation we just use the affix @{text "_raw"}.
+  given by user. In our implementation we just use the affix ``@{text "_raw"}''.
   But for the purpose of this paper, we just use the superscript @{text "_\<^sup>\<alpha>"} to indicate 
   that a notion is defined over alpha-equivalence classes and leave it out 
   for the corresponding notion defined on the ``raw'' level. So for example 
@@ -1111,15 +1119,15 @@
   \end{center}
   
   \noindent
-  where the type @{term ty} is the type used in the quotient construction for 
+  where @{term ty} is the type used in the quotient construction for 
   @{text "ty\<^sup>\<alpha>"} and @{text "C"} is the term-constructor on the ``raw'' type @{text "ty"}. 
 
   The resulting datatype definition is legal in Isabelle/HOL provided the datatypes are 
   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_ty"}, by primitive recursion over the corresponding 
-  raw datatype @{text ty}. We can also easily define permutation operations by 
+  functions, called @{term "bn"}, by primitive 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
 
@@ -1144,19 +1152,21 @@
   \noindent
   We define them together with auxiliary free-variable functions for
   the binding functions. Given binding functions 
-  @{text "bn_ty\<^isub>1 \<dots> bn_ty\<^isub>m"} we need to define
+  @{text "bn\<^isub>1 \<dots> bn\<^isub>m"} we need to define
   %
   \begin{center}
-  @{text "fv_bn_ty\<^isub>1 :: ty\<^isub>1 \<Rightarrow> atom set  \<dots>  fv_bn_ty\<^isub>m :: ty\<^isub>m \<Rightarrow> atom set"}
+  @{text "fv_bn\<^isub>1 :: ty\<^isub>1 \<Rightarrow> atom set  \<dots>  fv_bn\<^isub>m :: ty\<^isub>m \<Rightarrow> atom set"}
   \end{center}
 
   \noindent
   The reason for this setup is that in a deep binder not all atoms have to be
-  bound, as we shall see in an example below. While the idea behind these
+  bound, as we shall see in an example below. We need therefore the function
+  that returns us those unbound atoms. 
+
+  While the idea behind these
   free-variable functions is clear (they just collect all atoms that are not bound),
   because of the rather complicated binding mechanisms their definitions are
   somewhat involved.
-
   Given a term-constructor @{text "C"} of type @{text ty} with argument types
   \mbox{@{text "ty\<^isub>1 \<dots> ty\<^isub>n"}}, the function
   @{text "fv_ty (C x\<^isub>1 \<dots> x\<^isub>n)"} will be the union of the values
@@ -1169,20 +1179,20 @@
   \begin{center}
   \begin{tabular}{c@ {\hspace{2mm}}p{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 with the auxiliary function @{text "bn_ty\<^isub>i"}\\
-  $\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 with the auxiliary function @{text "bn_ty\<^isub>i"}
+  $\bullet$ & @{text "fv_bn x\<^isub>i"} provided @{text "x\<^isub>i"} is a deep
+      non-recursive binder with the auxiliary binding function @{text "bn"}\\
+  $\bullet$ & @{text "fv_ty\<^isub>i x\<^isub>i - bn x\<^isub>i"} provided @{text "x\<^isub>i"} is
+      a deep recursive binder with the auxiliary binding function @{text "bn"}
   \end{tabular}
   \end{center}
 
   \noindent
   The first clause states that shallow binders do not contribute to the
   free variables; in the second clause, we have to collect all
-  variables that are left unbound by the binding function @{text "bn_ty\<^isub>i"}---this
-  is done with function @{text "fv_bn_ty\<^isub>i"}; in the third clause, since the 
+  variables that are left unbound by the binding function @{text "bn"}---this
+  is done with function @{text "fv_bn"}; in the third clause, since the 
   binder is recursive, we need to bind all variables specified by 
-  @{text "bn_ty\<^isub>i"}---therefore we subtract @{text "bn_ty\<^isub>i x\<^isub>i"} from the free
+  @{text "bn"}---therefore we subtract @{text "bn x\<^isub>i"} from the free
   variables of @{text "x\<^isub>i"}.
 
   In case the argument is \emph{not} a binder, we need to consider 
@@ -1217,31 +1227,31 @@
   as in \eqref{deepbody}, except that we do not need to subtract the 
   set @{text bnds}.
   
-  Next, we need to define a free-variable function @{text "fv_bn_ty\<^isub>i"} for 
-  each binding function @{text "bn_ty\<^isub>i"}. The idea behind this
+  Next, we need to define a free-variable function @{text "fv_bn\<^isub>j"} for 
+  each binding function @{text "bn\<^isub>j"}. The idea behind this
   function is to compute the set of free atoms that are not bound by 
-  @{text "bn_ty\<^isub>i"}. Because of the restrictions we imposed on the 
+  @{text "bn\<^isub>j"}. Because of the restrictions we imposed on the 
   form of binding functions, this can be done automatically by recursively 
   building up the the set of free variables from the arguments that are 
   not bound. Let us assume one clause of the binding function is 
-  @{text "bn_ty\<^isub>i (C x\<^isub>1 \<dots> x\<^isub>n) = rhs"}, then @{text "fv_bn_ty\<^isub>i"} is the 
-  union of the values calculated for @{text "x\<^isub>j"} of type @{text "ty\<^isub>j"}
+  @{text "bn\<^isub>j (C x\<^isub>1 \<dots> x\<^isub>n) = rhs"}, then @{text "fv_bn\<^isub>j"} is the 
+  union of the values calculated for @{text "x\<^isub>i"} of type @{text "ty\<^isub>i"}
   as follows:
 
   \begin{center}
   \begin{tabular}{c@ {\hspace{2mm}}p{7cm}}
-  \multicolumn{2}{l}{@{text "x\<^isub>j"} occurs in @{text "rhs"}:}\\ 
-  $\bullet$ & @{term "{}"} provided @{term "x\<^isub>j"} is a single atom,
+  \multicolumn{2}{l}{@{text "x\<^isub>i"} occurs in @{text "rhs"}:}\\ 
+  $\bullet$ & @{term "{}"} provided @{term "x\<^isub>i"} is a single atom,
      atom list or atom set\\
-  $\bullet$ & @{text "fv_bn_ty\<^isub>j x\<^isub>j"} in case @{text "rhs"} contains the 
-  recursive call @{text "bn_ty\<^isub>j x\<^isub>j"}\\[1mm]
+  $\bullet$ & @{text "fv_bn x\<^isub>i"} in case @{text "rhs"} contains the 
+  recursive call @{text "bn x\<^isub>i"}\\[1mm]
   %
-  \multicolumn{2}{l}{@{text "x\<^isub>j"} does not occur in @{text "rhs"}:}\\ 
-  $\bullet$ & @{text "atoms x\<^isub>j"} provided @{term "x\<^isub>j"} is a set of atoms\\
-  $\bullet$ & @{term "atoms (set x\<^isub>j)"} provided @{term "x\<^isub>j"} is a list of atoms\\
-  $\bullet$ & @{text "fv_ty\<^isub>j x\<^isub>j"} provided @{term "ty\<^isub>j"} is one of the raw
+  \multicolumn{2}{l}{@{text "x\<^isub>i"} does not occur in @{text "rhs"}:}\\ 
+  $\bullet$ & @{text "atoms x\<^isub>i"} provided @{term "x\<^isub>i"} is a set of atoms\\
+  $\bullet$ & @{term "atoms (set x\<^isub>i)"} provided @{term "x\<^isub>i"} is a list of atoms\\
+  $\bullet$ & @{text "fv_ty\<^isub>i x\<^isub>i"} provided @{term "ty\<^isub>i"} is one of the raw
      types corresponding to the types specified by the user\\
-%  $\bullet$ & @{text "fv_ty\<^isup>\<alpha> x\<^isub>j - bnds"} provided @{term "x\<^isub>j"}  is not in @{text "rhs"}
+%  $\bullet$ & @{text "fv_ty\<^isup>\<alpha> x\<^isub>i - bnds"} provided @{term "x\<^isub>i"}  is not in @{text "rhs"}
 %     and is an existing nominal datatype with the free-variable function @{text "fv\<^isup>\<alpha>"}\\
   $\bullet$ & @{term "{}"} otherwise
   \end{tabular}
@@ -1577,7 +1587,7 @@
 section {* Related Work *}
 
 text {*
-  The earliest usage we know of general binders in a theorem prover setting is 
+  To our knowledge the earliest usage of general binders in a theorem prover setting is 
   in the paper \cite{NaraschewskiNipkow99}, which describes a formalisation of 
   the algorithm W. This formalisation implements binding in type schemes using a 
   a de-Bruijn indices representation. Also recently an extension for general binders 




