
diff -r e90f6a26d74b -r a908ea36054f Paper/Paper.thy
--- a/Paper/Paper.thy	Fri Jul 02 01:54:19 2010 +0100
+++ b/Paper/Paper.thy	Fri Jul 02 15:34:46 2010 +0100
@@ -45,7 +45,7 @@
 text {*
 %%%  @{text "(1, (2, 3))"}
 
-  So far, Nominal Isabelle provides a mechanism for constructing
+  So far, Nominal Isabelle provided a mechanism for constructing
   $\alpha$-equated terms, for example lambda-terms
 
   \begin{center}
@@ -366,7 +366,7 @@
   conditions for $\alpha$-equated terms. We are also able to derive strong 
   induction principles that have the variable convention already built in.
   The method behind our specification of general binders is taken 
-  from the Ott-tool, but we introduce restrictions, and also one extension, so 
+  from the Ott-tool, but we introduce crucial restrictions, and also one extension, so 
   that our specifications make sense for reasoning about $\alpha$-equated terms. 
 
 
@@ -404,9 +404,9 @@
   \end{tabular}
   \end{center}
   \end{boxedminipage}
-  \caption{The term-language of System @{text "F\<^isub>C"}
+  \caption{The System @{text "F\<^isub>C"}
   \cite{CoreHaskell}, also often referred to as \emph{Core-Haskell}. In this
-  version of the term-language we made a modification by separating the
+  version of @{text "F\<^isub>C"} we made a modification by separating the
   grammars for type kinds and coercion kinds, as well as for types and coercion
   types. For this paper the interesting term-constructor is @{text "\<CASE>"},
   which binds multiple type-, coercion- and term-variables.\label{corehas}}
@@ -601,7 +601,7 @@
 *}
 
 
-section {* General Binders\label{sec:binders} *}
+section {* General Bindings\label{sec:binders} *}
 
 text {*
   In Nominal Isabelle, the user is expected to write down a specification of a
@@ -683,7 +683,7 @@
   \end{array}
   \end{equation}
 
-  It might be useful to consider first some examples for how these definitions
+  It might be useful to consider first some examples about how these definitions
   of $\alpha$-equivalence pan out in practice.  For this consider the case of
   abstracting a set of variables over types (as in type-schemes). We set
   @{text R} to be the usual equality @{text "="} and for @{text "fv(T)"} we
@@ -853,7 +853,7 @@
   the definitions for $\alpha$-equivalence will help us in the next section.
 *}
 
-section {* Specifying General Binders\label{sec:spec} *}
+section {* Specifying General Bindings\label{sec:spec} *}
 
 text {*
   Our choice of syntax for specifications is influenced by the existing
@@ -989,7 +989,7 @@
   Note that for @{text lam} it does not matter which binding mode we use. The
   reason is that we bind only a single @{text name}. However, having
   \isacommand{bind\_set} or \isacommand{bind} in the second case makes a
-  difference to the semantics of the specification (which we will define below).
+  difference to the semantics of the specification (which we will define in the next section).
 
 
   A \emph{deep} binder uses an auxiliary binding function that ``picks'' out
@@ -1068,10 +1068,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 later.
+  function and $\alpha$-equivalence relation.
   
   To make sure that variables bound by deep binders cannot be free at the
-  same time, we cannot have more than one binding function for one binder. 
+  same time, we cannot have more than one binding function for one deep binder. 
   Consequently we exclude specifications such as
 
   \begin{center}
@@ -1089,7 +1089,7 @@
   out different atoms to become bound, respectively be free, in @{text "p"}.
   
   We also need to restrict the form of the binding functions in order 
-  to ensure the @{text "bn"}-functions can be lifted defined for $\alpha$-equated 
+  to ensure the @{text "bn"}-functions can be defined for $\alpha$-equated 
   terms. As a result we cannot return an atom in a binding function that is also
   bound in the corresponding term-constructor. That means in the example
   \eqref{letpat} that the term-constructors @{text PVar} and @{text PTup} may
@@ -1097,7 +1097,7 @@
   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). This restriction
-  means that we can lift the binding function to $\alpha$-equated terms.
+  is sufficient for defining the binding function over $\alpha$-equated terms.
 
   In the version of
   Nominal Isabelle described here, we also adopted the restriction from the
@@ -1171,8 +1171,7 @@
   in Isabelle/HOL). We then define the user-specified binding 
   functions @{term "bn"} by recursion over the corresponding 
   raw datatype. We can also easily define permutation operations by 
-  recursion so that for each term constructor @{text "C"} with  
-  arguments @{text "z"}$_{1..n}$ we have that
+  recursion so that for each term constructor @{text "C"} 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)"}
@@ -1180,7 +1179,7 @@
 
   The first non-trivial step we have to perform is the generation of
   free-variable functions from the specifications. For the 
-  \emph{raw} types @{text "ty"}$_{1..n}$ of a specification,
+  \emph{raw} types @{text "ty"}$_{1..n}$ extracted from  a specification,
   we define the free-variable functions
   %
   \begin{equation}\label{fvars}
@@ -1188,7 +1187,8 @@
   \end{equation}
 
   \noindent
-  We define them together with auxiliary free-variable functions for
+  by recursion over the types @{text "ty"}$_{1..n}$.
+  We define these functions together with auxiliary free-variable functions for
   the binding functions. Given raw binding functions @{text "bn"}$_{1..m}$ 
   we define
   %
@@ -1203,13 +1203,13 @@
 
   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. The functions
-  are defined by recursion defining a clause for each term-constructor.  Given
+  binding mechanisms their definitions are somewhat involved.  Given
   the term-constructor @{text "C"} of type @{text ty} and some associated
   binding clauses @{text "bc\<^isub>1\<dots>bc\<^isub>k"}, the result of @{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)"}. Given the binding clause @{text
-  bc\<^isub>i} is of the form
+  "fv(bc\<^isub>1) \<union> \<dots> \<union> fv(bc\<^isub>k)"} where we define below what @{text "fv"} of a binding
+  clause with mode \isacommand{bin\_set} means (similarly for the other modes). 
+  Suppose the binding clause @{text bc\<^isub>i} is of the form 
   %
   \begin{equation}
   \mbox{\isacommand{bind\_set} @{text "b\<^isub>1\<dots>b\<^isub>p"} \isacommand{in} @{text "d\<^isub>1\<dots>d\<^isub>q"}}
@@ -1220,7 +1220,7 @@
   and 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
-  set @{text "D"} stands for the free atoms in the bodies, @{text B} for the 
+  set @{text "D"} stands for the free atoms in the bodies, the set @{text B} for the 
   binding atoms in the binders and @{text "B'"} for the free atoms in 
   non-recursive deep binders,
   then the free atoms of the binding clause @{text bc\<^isub>i} are given by
@@ -1230,7 +1230,7 @@
   \end{center}
 
   \noindent
-  The set @{text D} is defined as
+  The set @{text D} is formally defined as
   %
   \begin{center}
   @{text "D \<equiv> fv_ty\<^isub>1 d\<^isub>1 \<union> ... \<union> fv_ty\<^isub>q d\<^isub>q"}
@@ -1238,24 +1238,24 @@
 
   \noindent
   whereby the functions @{text "fv_ty\<^isub>i"} are the ones we are defining by recursion 
-  (see \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"}.
-  In order to define the set @{text B} we use the following auxiliary bn-functions
+  (see \eqref{fvars}) provided the @{text "d\<^isub>i"} refers to one of the raw types 
+  @{text "ty"}$_{1..n}$ from a specification; otherwise we set @{text "fv_ty\<^isub>i d\<^isub>i = supp d\<^isub>i"}.
+  In order to define the set @{text B} we use the following auxiliary @{text "bn"}-functions
   for atom types to which shallow binders have to refer
   %
   \begin{center}
   \begin{tabular}{r@ {\hspace{2mm}}c@ {\hspace{2mm}}l}
-  @{text "bn_atom a"} & @{text "="} & @{text "{atom a}"}\\
-  @{text "bn_atom_set as"} & @{text "="} & @{text "atoms as"}\\
-  @{text "bn_atom_list as"} & @{text "="} & @{text "atoms (set as)"}
+  @{text "bn_atom a"} & @{text "\<equiv>"} & @{text "{atom a}"}\\
+  @{text "bn_atom_set as"} & @{text "\<equiv>"} & @{text "atoms as"}\\
+  @{text "bn_atom_list as"} & @{text "\<equiv>"} & @{text "atoms (set as)"}
   \end{tabular}
   \end{center}
 
   \noindent 
-  In these functions, @{text "atoms"}, like @{text "atom"}, coerces 
+  The function @{text "atoms"} 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}"}. 
-  The set @{text B} is then defined as
+  The set @{text B} is then formally defined as
   %
   \begin{center}
   @{text "B \<equiv> bn_ty\<^isub>1 b\<^isub>1 \<union> ... \<union> bn_ty\<^isub>p b\<^isub>p"}
@@ -1271,18 +1271,18 @@
 
   \noindent
   with none of the @{text "a"}$_{1..r}$ being among the bodies @{text
-  "d"}$_{1..q}$. The set @{text "B'"} is then defined as
+  "d"}$_{1..q}$. The set @{text "B'"} is defined as
   %
   \begin{center}
   @{text "B' \<equiv> fv_bn\<^isub>1 a\<^isub>1 \<union> ... \<union> fv_bn\<^isub>r a\<^isub>r"}
   \end{center} 
 
   \noindent
-  Similarly for the other binding modes. 
+  This completes the definition of the free-variable functions.
 
   Note that for non-recursive deep binders, we have to add all atoms that are left 
   unbound by the binding function @{text "bn"}. This is the purpose of the functions 
-  @{text "fv_bn"}, also defined by recursion. Assume the user has specified 
+  @{text "fv_bn"}, also defined by recursion. Assume the user specified 
   a @{text bn}-clause of the form
   %
   \begin{center}
@@ -1291,25 +1291,27 @@
 
   \noindent
   where the @{text "z"}$_{1..n}$ are of types @{text "ty"}$_{1..n}$. For each of
-  the arguments we calculate the free atoms as follows
+  the arguments we calculate the free atoms as follows:
   %
   \begin{center}
   \begin{tabular}{c@ {\hspace{2mm}}p{7cm}}
-  $\bullet$ & @{term "fv_ty\<^isub>i z\<^isub>i"} provided @{text "z\<^isub>i"} does not occur in @{text "rhs"}\\
+  $\bullet$ & @{term "fv_ty\<^isub>i z\<^isub>i"} provided @{text "z\<^isub>i"} does not occur in @{text "rhs"} 
+  (nothing gets bound in @{text "z\<^isub>i"}),\\
   $\bullet$ & @{term "fv_bn\<^isub>i z\<^isub>i"} provided @{text "z\<^isub>i"} occurs in  @{text "rhs"}
-  with the recursive call @{text "bn\<^isub>i z\<^isub>i"}\\
+  with the recursive call @{text "bn\<^isub>i z\<^isub>i"}, and\\
   $\bullet$ & @{term "{}"} provided @{text "z\<^isub>i"} occurs in  @{text "rhs"},
   but without a recursive call
   \end{tabular}
   \end{center}
 
   \noindent
-  For defining @{text "fv_bn (C z\<^isub>1 \<dots> z\<^isub>n)"}, we just union up all these values.
+  For defining @{text "fv_bn (C z\<^isub>1 \<dots> z\<^isub>n)"} we just union up all these values.
  
   To see how these definitions work in practice, let us reconsider the term-constructors 
-  @{text "Let"} and @{text "Let_rec"} from the example shown in \eqref{letrecs}. 
-  For them we consider three free-variable functions, namely
-  @{text "fv\<^bsub>trm\<^esub>"}, @{text "fv\<^bsub>assn\<^esub>"} and @{text "fv\<^bsub>bn\<^esub>"}:
+  @{text "Let"} and @{text "Let_rec"}, as well as @{text "ANil"} and @{text "ACons"} 
+  from the example shown in \eqref{letrecs}. 
+  For them we define three free-variable functions, namely
+  @{text "fv\<^bsub>trm\<^esub>"}, @{text "fv\<^bsub>assn\<^esub>"} and @{text "fv\<^bsub>bn\<^esub>"} as follows:
   %
   \begin{center}
   \begin{tabular}{@ {}l@ {\hspace{1mm}}c@ {\hspace{1mm}}l@ {}}
@@ -1317,7 +1319,7 @@
   @{text "fv\<^bsub>trm\<^esub> (Let_rec as t)"} & @{text "="} & @{text "(fv\<^bsub>assn\<^esub> as \<union> fv\<^bsub>trm\<^esub> t) - set (bn as)"}\\[1mm]
 
   @{text "fv\<^bsub>assn\<^esub> (ANil)"} & @{text "="} & @{term "{}"}\\
-  @{text "fv\<^bsub>assn\<^esub> (ACons a t as)"} & @{text "="} & @{text "{atom a} \<union> (fv\<^bsub>trm\<^esub> t) \<union> (fv\<^bsub>assn\<^esub> as)"}\\[1mm]
+  @{text "fv\<^bsub>assn\<^esub> (ACons a t as)"} & @{text "="} & @{text "(supp a) \<union> (fv\<^bsub>trm\<^esub> t) \<union> (fv\<^bsub>assn\<^esub> as)"}\\[1mm]
 
   @{text "fv\<^bsub>bn\<^esub> (ANil)"} & @{text "="} & @{term "{}"}\\
   @{text "fv\<^bsub>bn\<^esub> (ACons a t as)"} & @{text "="} & @{text "(fv\<^bsub>trm\<^esub> t) \<union> (fv\<^bsub>bn\<^esub> as)"}
@@ -1325,42 +1327,48 @@
   \end{center}
 
   \noindent
-  Since there are only (implicit) empty binding clauses for the term-constructors @{text ANil}
-  and @{text "ACons"}, the corresponding free-variable function @{text
-  "fv\<^bsub>assn\<^esub>"} returns all atoms occurring in an assignment. The
-  binding only takes place in @{text Let} and @{text "Let_rec"}. In the @{text
-  "Let"}-clause we want to bind all atoms given by @{text "set (bn as)"} in
-  @{text t}. Therefore we have to subtract @{text "set (bn as)"} from @{text
+  To see the ``pattern'', recall that @{text ANil} and @{text "ACons"} have no
+  binding clause in the specification. The corresponding free-variable
+  function @{text "fv\<^bsub>assn\<^esub>"} therefore returns all atoms
+  occurring in an assignment. The binding only takes place in @{text Let} and
+  @{text "Let_rec"}. In the @{text "Let"}-clause, the binding clause specifies
+  that all atoms given by @{text "set (bn as)"} have to be bound in @{text
+  t}. Therefore we have to subtract @{text "set (bn as)"} from @{text
   "fv\<^bsub>trm\<^esub> t"}. However, we also need to add all atoms that are
-  free in @{text "as"}. This is what the purpose of the function @{text
-  "fv\<^bsub>bn\<^esub>"} is.  In contrast, in @{text "Let_rec"} we have a
-  recursive binder where we want to also bind all occurrences of the atoms
-  in @{text "set (bn as)"} inside @{text "as"}. Therefore we have to subtract @{text
-  "set (bn as)"} from @{text "fv\<^bsub>trm\<^esub> t"}, as well as from
-  @{text "fv\<^bsub>assn\<^esub> as"}. An interesting point in this example is
-  that an assignment ``alone'' does not have any bound variables. Only in the
-  context of a @{text Let} or @{text "Let_rec"} will some atoms become bound.  
-  This is a phenomenon 
-  that has also been pointed out in \cite{ott-jfp}. For us it is crucial, because
-  we would not be able to lift a @{text "bn"}-function that is defined over 
-  arguments that are either binders or bodies. In that case @{text "bn"} would
-  not respect $\alpha$-equivalence. We can also see that
+  free in @{text "as"}.  In contrast, in @{text "Let_rec"} we have a recursive
+  binder where we want to also bind all occurrences of the atoms in @{text
+  "set (bn as)"} also inside @{text "as"}. Therefore we have to subtract
+  @{text "set (bn as)"} from the union @{text "fv\<^bsub>trm\<^esub> t"} and @{text "fv\<^bsub>assn\<^esub> as"}. 
+  
+  An interesting point in this
+  example is that a ``naked'' assignment does not bind any
+  atoms. Only in the context of a @{text Let} or @{text "Let_rec"} will
+  some atoms from an assignment become bound.  This is a phenomenon that has also been pointed
+  out in \cite{ott-jfp}. For us this observation is crucial, because we would 
+  not be able to lift the @{text "bn"}-function if it was defined over assignments 
+  where some atoms are bound. In that case @{text "bn"} would \emph{not} respect
+  $\alpha$-equivalence.
+
+  Next we define $\alpha$-equivalence relations for the raw types @{text
+  "ty"}$_{1..n}$. We call them 
   %
-  \begin{equation}\label{bnprop}
-  @{text "fv_ty x  =  bn x \<union> fv_bn x"}.
-  \end{equation}
+  \begin{center}
+  @{text "\<approx>ty\<^isub>1, \<dots>, \<approx>ty\<^isub>n"}. 
+  \end{center}
 
   \noindent
-  holds for any @{text "bn"}-function defined for the type @{text "ty"}.
-
-  TBD below.
+  Like with the free-variable functions, we also need to
+  define auxiliary $\alpha$-equivalence relations 
+  %
+  \begin{center}
+  @{text "\<approx>bn\<^isub>1, \<dots>, \<approx>bn\<^isub>m"}
+  \end{center}
 
-  Next we define $\alpha$-equivalence relations for the types @{text "ty\<^isub>1, \<dots>, ty\<^isub>n"}. We call them
-  @{text "\<approx>ty\<^isub>1, \<dots>, \<approx>ty\<^isub>n"}. Like with the free-variable functions, 
-  we also need to  define auxiliary $\alpha$-equivalence relations for the binding functions. 
-  Say we have binding functions @{text "bn\<^isub>1, \<dots>, bn\<^isub>m"}, then we also define @{text "\<approx>bn\<^isub>1, \<dots>, \<approx>bn\<^isub>m"}.
-  To simplify our definitions we will use the following abbreviations for 
-  relations and free-variable acting on products.
+  \noindent
+  for the binding functions @{text "bn"}$_{1..m}$, 
+  To simplify our definitions we will use the following abbreviations for
+  equivalence relations and free-variable functions acting on pairs
+
   %
   \begin{center}
   \begin{tabular}{r@ {\hspace{2mm}}c@ {\hspace{2mm}}l}
@@ -1370,16 +1378,17 @@
   \end{center}
 
 
-  The relations for $\alpha$-equivalence are inductively defined predicates, whose clauses have
-  conclusions of the form  
+  The relations for $\alpha$-equivalence are inductively defined 
+  predicates, whose clauses have the form  
   %
   \begin{center}
-  \mbox{\infer{@{text "C x\<^isub>1 \<dots> x\<^isub>n  \<approx>ty  C y\<^isub>1 \<dots> y\<^isub>n"}}
-  {@{text "prems(bc\<^isub>1)"} & @{text "\<dots>"} & @{text "prems(bc\<^isub>p)"}}} 
+  \mbox{\infer{@{text "C z\<^isub>1 \<dots> z\<^isub>n  \<approx>ty  C z\<PRIME>\<^isub>1 \<dots> z\<PRIME>\<^isub>n"}}
+  {@{text "prems(bc\<^isub>1) \<and> \<dots> \<and> prems(bc\<^isub>k)"}}} 
   \end{center}
 
   \noindent
-  For what follows, let us assume @{text C} is of type @{text ty}.  The task
+  assuming the term-constructor @{text C} is of type @{text ty} and has
+  the binding clauses @{term "bc"}$_{1..k}$.  The task
   is to specify what the premises of these clauses are. Again for this we
   analyse the binding clauses and produce a corresponding premise.
 *}
@@ -1397,6 +1406,8 @@
   fv_trm2 ("fv\<^bsub>assn\<^esub> \<oplus> fv\<^bsub>trm\<^esub>") 
 (*>*)
 text {*
+  *TBD below *
+
   \begin{equation}\label{alpha}
   \mbox{%
   \begin{tabular}{c@ {\hspace{2mm}}p{7cm}}
@@ -2090,6 +2101,19 @@
 section {* Conclusion *}
 
 text {*
+We can also see that
+  %
+  \begin{equation}\label{bnprop}
+  @{text "fv_ty x  =  bn x \<union> fv_bn x"}.
+  \end{equation}
+
+  \noindent
+  holds for any @{text "bn"}-function defined for the type @{text "ty"}.
+
+*}
+
+
+text {*
   We have presented an extension of Nominal Isabelle for deriving
   automatically a convenient reasoning infrastructure that can deal with
   general binders, that is term-constructors binding multiple variables at




