
diff -r 02d98590454d -r c6af56de923d LMCS-Paper/Paper.thy
--- a/LMCS-Paper/Paper.thy	Thu Sep 08 11:21:03 2011 +0100
+++ b/LMCS-Paper/Paper.thy	Thu Sep 08 13:03:19 2011 +0100
@@ -202,7 +202,7 @@
   \mbox{\begin{tabular}{r@ {\hspace{2mm}}r@ {\hspace{2mm}}ll}
   @{text trm} & @{text "::="}  & @{text "\<dots>"} \\
               & @{text "|"}    & @{text "\<LET>  as::assn  s::trm"}\hspace{2mm} 
-                                 \isacommand{bind} @{text "bn(as)"} \isacommand{in} @{text "s"}\\[1mm]
+                                 \isacommand{binds} @{text "bn(as)"} \isacommand{in} @{text "s"}\\[1mm]
   @{text assn} & @{text "::="} & @{text "\<ANIL>"}\\
                &  @{text "|"}  & @{text "\<ACONS>  name  trm  assn"}
   \end{tabular}}
@@ -222,7 +222,7 @@
   \noindent
   The scope of the binding is indicated by labels given to the types, for
   example @{text "s::trm"}, and a binding clause, in this case
-  \isacommand{bind} @{text "bn(as)"} \isacommand{in} @{text "s"}. This binding
+  \isacommand{binds} @{text "bn(as)"} \isacommand{in} @{text "s"}. This binding
   clause states that all the names the function @{text "bn(as)"} returns
   should be bound in @{text s}.  This style of specifying terms and bindings
   is heavily inspired by the syntax of the Ott-tool \cite{ott-jfp}. Our work
@@ -517,7 +517,7 @@
   described, for example for atoms, products, lists, function applications, 
   booleans and permutations as follows
   
-  \[\mbox{
+  \begin{equation}\label{supps}\mbox{
   \begin{tabular}{c@ {\hspace{10mm}}c}
   \begin{tabular}{rcl}
   @{term "supp a"} & $=$ & @{term "{a}"}\\
@@ -532,7 +532,7 @@
   @{term "supp \<pi>"} & $=$ & @{term "{a. \<pi> \<bullet> a \<noteq> a}"}
   \end{tabular}
   \end{tabular}}
-  \]\smallskip
+  \end{equation}\smallskip
   
   \noindent 
   in some cases it can be difficult to characterise the support precisely, and
@@ -613,8 +613,10 @@
   in the support of @{text x} (that is @{term "supp x \<sharp>* \<pi>"}). The last 
   fact and Property~\ref{supppermeq} allow us to ``rename'' just the binders 
   @{text as} in @{text x}, because @{term "\<pi> \<bullet> x = x"}. Note that @{term "supp x \<sharp>* \<pi>"}
-  is equivalent with @{term "supp \<pi> \<sharp>* x"}, which means we could also use the other
-  `direction' in Propositions \ref{supppermeq} and \ref{avoiding}.
+  is equivalent with @{term "supp \<pi> \<sharp>* x"}, which means we could also formulate 
+  Propositions \ref{supppermeq} and \ref{avoiding} in the other `direction', however the 
+  reasoning infrastructure of Nominal Isabelle is set up so that it provides more
+  automation for the original formulation.
 
   Most properties given in this section are described in detail in \cite{HuffmanUrban10}
   and all are formalised in Isabelle/HOL. In the next sections we will make 
@@ -753,9 +755,6 @@
   \begin{lem}\label{alphaeq} 
   The relations $\approx_{\,\textit{abs\_set}}$, $\approx_{\,\textit{abs\_list}}$
   and $\approx_{\,\textit{abs\_set+}}$ are equivalence relations and equivariant. 
-  %, and if 
-  %@{term "abs_set (as, x) (bs, y)"} then also 
-  %@{term "abs_set (p \<bullet> as, p \<bullet> x) (p \<bullet> bs, p \<bullet> y)"} (similarly for the other two relations).
   \end{lem}
 
   \begin{proof}
@@ -763,9 +762,11 @@
   a permutation @{text "\<pi>"} and for the proof obligation take @{term "- \<pi>"}. In case 
   of transitivity, we have two permutations @{text "\<pi>\<^isub>1"} and @{text "\<pi>\<^isub>2"}, and for the
   proof obligation use @{text "\<pi>\<^isub>1 + \<pi>\<^isub>2"}. Equivariance means
-  @{term "abs_set (p \<bullet> as, p \<bullet> x) (p \<bullet> bs, p \<bullet> y)"} holds provided 
-  @{term "abs_set (as, x) (bs, y)"}.
-
+  @{term "abs_set (\<pi> \<bullet> as, \<pi> \<bullet> x) (\<pi> \<bullet> bs, \<pi> \<bullet> y)"} holds provided 
+  @{term "abs_set (as, x) (bs, y)"}. To show this, we need to unfold the
+  definitions and `pull out' the permutations, which is possible since all
+  operators, such as @{text "#\<^sup>*, -, set"} and @{text "supp"}, are equivariant
+  (see \cite{HuffmanUrban10}).
   \end{proof}
 
   \noindent
@@ -802,13 +803,14 @@
   \end{thm}
 
   \noindent
-  This theorem states that the bound names do not appear in the support.
-  Below we will show the first equation. The others follow by similar
+  In effect, this theorem states that the bound names do not appear in the support
+  of abstractions. This can be seen as test that our Definitions \ref{alphaset}, \ref{alphalist}
+  and \ref{alphares} capture the idea of alpha-equivalence relations. 
+  Below we will show the first equation of Theorem \ref{suppabs}. The others follow by similar
   arguments. By definition of the abstraction type @{text "abs\<^bsub>set\<^esub>"} we have
 
-  
   \begin{equation}\label{abseqiff}
-  @{thm (lhs) Abs_eq_iff(1)[where bs="as" and cs="bs", no_vars]} \;\;\text{if and only if}\;\; 
+  @{thm (lhs) Abs_eq_iff(1)[where bs="as" and cs="bs", no_vars]} \;\;\;\text{if and only if}\;\;\; 
   @{term "\<exists>\<pi>. alpha_set (as, x) equal supp \<pi> (bs, y)"}
   \end{equation}\smallskip
   
@@ -826,13 +828,14 @@
   the following lemma about swapping two atoms in an abstraction.
   
   \begin{lem}
-  @{thm[mode=IfThen] Abs_swap1(1)[where bs="as", no_vars]}
+  If @{thm (prem 1) Abs_swap1(1)[where bs="as", no_vars]} and
+  @{thm (prem 2) Abs_swap1(1)[where bs="as", no_vars]} then 
+  @{thm (concl) Abs_swap1(1)[where bs="as", no_vars]}
   \end{lem}
   
   \begin{proof}
   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 (see \cite{HuffmanUrban10}).
   \end{proof}
   
   \noindent
@@ -841,45 +844,48 @@
   
   \begin{equation}\label{halfone}
   @{thm Abs_supports(1)[no_vars]}
-  \end{equation}
+  \end{equation}\smallskip
   
   \noindent
   which by Property~\ref{supportsprop} gives us ``one half'' of
   Theorem~\ref{suppabs}. The ``other half'' is a bit more involved. To establish 
   it, we use a trick from \cite{Pitts04} and first define an auxiliary 
-  function @{text aux}, taking an abstraction as argument:
-  @{thm supp_set.simps[THEN eq_reflection, no_vars]}.
-  
+  function @{text aux}, taking an abstraction as argument
+
+  \[
+  @{thm supp_set.simps[THEN eq_reflection, no_vars]}
+  \]\smallskip 
+
+  \noindent
   Using the second equation in \eqref{equivariance}, we can show that 
-  @{text "aux"} is equivariant (since @{term "p \<bullet> (supp x - as) = (supp (p \<bullet> x)) - (p \<bullet> as)"}) 
+  @{text "aux"} is equivariant (since @{term "\<pi> \<bullet> (supp x - as) = (supp (\<pi> \<bullet> x)) - (\<pi> \<bullet> as)"}) 
   and therefore has empty support. 
   This in turn means
   
-  \begin{center}
-  @{term "supp (supp_gen (Abs_set as x)) \<subseteq> supp (Abs_set as x)"}
-  \end{center}
+  \[
+  @{term "supp (supp_set (Abs_set as x)) \<subseteq> supp (Abs_set as x)"}
+  \]\smallskip
   
   \noindent
-  using \eqref{suppfun}. Assuming @{term "supp x - as"} is a finite set,
-  we further obtain
+  using fact about function applications in \eqref{supps}. Assuming 
+  @{term "supp x - as"} is a finite set, we further obtain
   
   \begin{equation}\label{halftwo}
   @{thm (concl) Abs_supp_subset1(1)[no_vars]}
-  \end{equation}
+  \end{equation}\smallskip
   
   \noindent
-  since for finite sets of atoms, @{text "bs"}, we have 
+  since for every finite sets of atoms, say @{text "bs"}, we have 
   @{thm (concl) supp_finite_atom_set[where S="bs", no_vars]}.
   Finally, taking \eqref{halfone} and \eqref{halftwo} together establishes 
   Theorem~\ref{suppabs}. 
 
-  The method of first considering abstractions of the
-  form @{term "Abs_set as x"} etc is motivated by the fact that 
-  we can conveniently establish  at the Isabelle/HOL level
-  properties about them.  It would be
-  laborious 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 help us in the next sections.
+  The method of first considering abstractions of the form @{term "Abs_set as
+  x"} etc is motivated by the fact that we can conveniently establish at the
+  Isabelle/HOL level properties about them.  It would be extremely laborious
+  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 help us in the next sections.
 *}
 
 section {* Specifying General Bindings\label{sec:spec} *}
@@ -914,129 +920,124 @@
   \end{tabular}}
   \end{cases}$\\
   \end{tabular}}
-  \end{equation}
+  \end{equation}\smallskip
 
   \noindent
-  Every type declaration @{text ty}$^\alpha_{1..n}$ 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 a term-constructor @{text "C\<^sup>\<alpha>"} might be specified with
+  Every type declaration @{text ty}$^\alpha_{1..n}$ 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 a
+  term-constructor @{text "C\<^sup>\<alpha>"} might be specified with
 
-  \begin{center}
-  @{text "C\<^sup>\<alpha> label\<^isub>1::ty"}$'_1$ @{text "\<dots> label\<^isub>l::ty"}$'_l\;\;$  @{text "binding_clauses"} 
-  \end{center}
+  \[
+  @{text "C\<^sup>\<alpha> label\<^isub>1::ty"}\mbox{$'_1$} @{text "\<dots> label\<^isub>l::ty"}\mbox{$'_l\;\;$}  @{text "binding_clauses"} 
+  \]\smallskip
+  
+  \noindent
+  whereby some of the @{text ty}$'_{1..l}$ (or their components) can be
+  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 types of such
+  recursive arguments need to satisfy a ``positivity'' restriction, which
+  ensures that the type has a set-theoretic semantics (see
+  \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}:
+
+
+  \[\mbox{
+  \begin{tabular}{@ {}l@ {}}
+  \isacommand{binds} {\it binders} \isacommand{in} {\it bodies}\\
+  \isacommand{binds (set)} {\it binders} \isacommand{in} {\it bodies}\\
+  \isacommand{binds (set+)} {\it binders} \isacommand{in} {\it bodies}
+  \end{tabular}}
+  \]\smallskip
   
   \noindent
-  whereby some of the @{text ty}$'_{1..l}$ (or their components) 
-  can be 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 types of such recursive 
-  arguments need to satisfy a  ``positivity''
-  restriction, which ensures 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@ {}}
-  \isacommand{bind} {\it binders} \isacommand{in} {\it bodies}\;\;\;\,
-  \isacommand{bind (set)} {\it binders} \isacommand{in} {\it bodies}\;\;\;\,
-  \isacommand{bind (set+)} {\it binders} \isacommand{in} {\it bodies}
-  \end{tabular}
-  \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). As indicated, the labels in 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
+  The first mode is for binding lists of atoms (the order of bound atoms
+  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). As indicated, the labels in the
+  ``\isacommand{in}-part'' of a binding clause will be called \emph{bodies};
+  the ``\isacommand{binds}-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:
-  
-  \begin{center}
+ 
+  \[\mbox{
   \begin{tabular}{@ {}ll@ {}}
   @{text "Foo\<^isub>1 x::name y::name t::trm s::trm"} &  
-      \isacommand{bind} @{text "x y"} \isacommand{in} @{text "t s"}\\
+      \isacommand{binds} @{text "x y"} \isacommand{in} @{text "t s"}\\
   @{text "Foo\<^isub>2 x::name y::name t::trm s::trm"} &  
-      \isacommand{bind} @{text "x y"} \isacommand{in} @{text "t"}, 
-      \isacommand{bind} @{text "x y"} \isacommand{in} @{text "s"}\\
-  \end{tabular}
-  \end{center}
+      \isacommand{binds} @{text "x y"} \isacommand{in} @{text "t"}, 
+      \isacommand{binds} @{text "x y"} \isacommand{in} @{text "s"}\\
+  \end{tabular}}
+  \]\smallskip
 
   \noindent
-  Similarly for the other binding modes. 
-  Interestingly, in case of \isacommand{bind (set)}
-  and \isacommand{bind (set+)} 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{binds (set)} and \isacommand{binds (set+)} 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 also some restrictions we need to impose on our binding clauses in comparison to
-  the ones of Ott. 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 an 
-  atom occurrence cannot be both bound and free at the same time.  The first
-  restriction is that a body can only occur in
+  There are also some restrictions we need to impose on our binding clauses in
+  comparison to the ones of Ott. 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 an atom occurrence cannot be both bound and free
+  at the same time.  The first restriction is that a body can only occur in
   \emph{one} binding clause of a term constructor (this ensures that the bound
-  atoms of a body cannot be free at the same time by specifying an
-  alternative binder for the same body). 
+  atoms of a body cannot be free at the same time by specifying an alternative
+  binder for the same 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 (set+)} 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:
+  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{binds (set)} and \isacommand{binds (set+)} the
+  labels must either refer to atom types or to sets of atom types; in case of
+  \isacommand{binds} 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}{@ {}c@ {\hspace{7mm}}c@ {}}
+  \[\mbox{
+  \begin{tabular}{@ {}c@ {\hspace{5mm}}c@ {}}
   \begin{tabular}{@ {}l}
   \isacommand{nominal\_datatype} @{text lam} $=$\\
   \hspace{2mm}\phantom{$\mid$}~@{text "Var name"}\\
   \hspace{2mm}$\mid$~@{text "App lam lam"}\\
-  \hspace{2mm}$\mid$~@{text "Lam x::name t::lam"}~~\isacommand{bind} @{text x} \isacommand{in} @{text t}\\
+  \hspace{2mm}$\mid$~@{text "Lam x::name t::lam"}\hspace{3mm}%
+  \isacommand{binds} @{text x} \isacommand{in} @{text t}\\
   \end{tabular} &
   \begin{tabular}{@ {}l@ {}}
   \isacommand{nominal\_datatype}~@{text ty} $=$\\
   \hspace{5mm}\phantom{$\mid$}~@{text "TVar name"}\\
   \hspace{5mm}$\mid$~@{text "TFun ty ty"}\\
-  \isacommand{and}~@{text "tsc = All xs::(name fset) T::ty"}~~%
-  \isacommand{bind (set+)} @{text xs} \isacommand{in} @{text T}\\
+  \isacommand{and}~@{text "tsc = All xs::(name fset) T::ty"}\hspace{3mm}%
+  \isacommand{binds (set+)} @{text xs} \isacommand{in} @{text T}\\
   \end{tabular}
-  \end{tabular}
-  \end{center}
+  \end{tabular}}
+  \]\smallskip
+
 
   \noindent
   In these specifications @{text "name"} refers to an atom type, and @{text
-  "fset"} to the type of finite sets.
-  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 in the next section).
-
+  "fset"} to the type of finite sets.  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{binds (set)} or \isacommand{binds}
+  in the second case makes a 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
   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}, see below). The binding functions are
-  expected to return either a set of atoms (for \isacommand{bind (set)} and
-  \isacommand{bind (set+)}) or a list of atoms (for \isacommand{bind}). They can
-  be defined by recursion over the corresponding type; the equations
+  expected to return either a set of atoms (for \isacommand{binds (set)} and
+  \isacommand{binds (set+)}) or a list of atoms (for \isacommand{binds}). They need
+  to 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{%
   \begin{tabular}{l}
@@ -1044,20 +1045,20 @@
   \hspace{5mm}\phantom{$\mid$}~@{term "Var name"}\\
   \hspace{5mm}$\mid$~@{term "App trm trm"}\\
   \hspace{5mm}$\mid$~@{text "Lam x::name t::trm"} 
-     \;\;\isacommand{bind} @{text x} \isacommand{in} @{text t}\\
+     \;\;\isacommand{binds} @{text x} \isacommand{in} @{text t}\\
   \hspace{5mm}$\mid$~@{text "Let p::pat trm t::trm"} 
-     \;\;\isacommand{bind} @{text "bn(p)"} \isacommand{in} @{text t}\\
-  \isacommand{and} @{text pat} $=$
-  @{text PNil}
-  $\mid$~@{text "PVar name"}
-  $\mid$~@{text "PTup pat pat"}\\ 
+     \;\;\isacommand{binds} @{text "bn(p)"} \isacommand{in} @{text t}\\
+  \isacommand{and} @{text pat} $=$\\
+  \hspace{5mm}\phantom{$\mid$}~@{text PNil}\\
+  \hspace{5mm}$\mid$~@{text "PVar name"}\\
+  \hspace{5mm}$\mid$~@{text "PTup pat pat"}\\ 
   \isacommand{binder}~@{text "bn::pat \<Rightarrow> atom list"}\\
   \isacommand{where}~@{text "bn(PNil) = []"}\\
   \hspace{5mm}$\mid$~@{text "bn(PVar x) = [atom x]"}\\
   \hspace{5mm}$\mid$~@{text "bn(PTup p\<^isub>1 p\<^isub>2) = bn(p\<^isub>1) @ bn(p\<^isub>2)"}\smallskip\\ 
   \end{tabular}}
-  \end{equation}
-  %
+  \end{equation}\smallskip
+
   \noindent
   In this specification the function @{text "bn"} determines which atoms of
   the pattern @{text p} are bound in the argument @{text "t"}. Note that in the
@@ -1067,36 +1068,37 @@
 
   As said above, for deep binders we allow binding clauses such as
   
-  \begin{center}
+  \[\mbox{
   \begin{tabular}{ll}
   @{text "Bar p::pat t::trm"} &  
-     \isacommand{bind} @{text "bn(p)"} \isacommand{in} @{text "p t"} \\
-  \end{tabular}
-  \end{center}
+     \isacommand{binds} @{text "bn(p)"} \isacommand{in} @{text "p t"} \\
+  \end{tabular}}
+  \]\smallskip
+
   
   \noindent
   where the argument of the deep binder also occurs in the body. We call such
   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@ {}}
   \isacommand{nominal\_datatype}~@{text "trm ="}~\ldots\\
   \hspace{5mm}$\mid$~@{text "Let as::assn t::trm"} 
-     \;\;\isacommand{bind} @{text "bn(as)"} \isacommand{in} @{text t}\\
+     \;\;\isacommand{binds} @{text "bn(as)"} \isacommand{in} @{text t}\\
   \hspace{5mm}$\mid$~@{text "Let_rec as::assn t::trm"}
-     \;\;\isacommand{bind} @{text "bn(as)"} \isacommand{in} @{text "as t"}\\
-  \isacommand{and} @{text "assn"} $=$
-  @{text "ANil"}
-  $\mid$~@{text "ACons name trm assn"}\\
+     \;\;\isacommand{binds} @{text "bn(as)"} \isacommand{in} @{text "as t"}\\
+  \isacommand{and} @{text "assn"} $=$\\
+  \hspace{5mm}\phantom{$\mid$}~@{text "ANil"}\\
+  \hspace{5mm}$\mid$~@{text "ACons name trm assn"}\\
   \isacommand{binder} @{text "bn::assn \<Rightarrow> atom list"}\\
   \isacommand{where}~@{text "bn(ANil) = []"}\\
   \hspace{5mm}$\mid$~@{text "bn(ACons a t as) = [atom a] @ bn(as)"}\\
   \end{tabular}}
-  \end{equation}
-  %
+  \end{equation}\smallskip
+  
   \noindent
   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
@@ -1110,10 +1112,10 @@
   \begin{center}
   \begin{tabular}{@ {}l@ {\hspace{2mm}}l@ {}}
   @{text "Baz\<^isub>1 p::pat t::trm"} & 
-     \isacommand{bind} @{text "bn\<^isub>1(p) bn\<^isub>2(p)"} \isacommand{in} @{text t}\\
+     \isacommand{binds} @{text "bn\<^isub>1(p) bn\<^isub>2(p)"} \isacommand{in} @{text t}\\
   @{text "Baz\<^isub>2 p::pat t\<^isub>1::trm t\<^isub>2::trm"} & 
-     \isacommand{bind} @{text "bn\<^isub>1(p)"} \isacommand{in} @{text "t\<^isub>1"},
-     \isacommand{bind} @{text "bn\<^isub>2(p)"} \isacommand{in} @{text "t\<^isub>2"}\\
+     \isacommand{binds} @{text "bn\<^isub>1(p)"} \isacommand{in} @{text "t\<^isub>1"},
+     \isacommand{binds} @{text "bn\<^isub>2(p)"} \isacommand{in} @{text "t\<^isub>2"}\\
   \end{tabular}
   \end{center}
 
@@ -1147,18 +1149,18 @@
   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
-  clause, written \isacommand{bind}~@{term "{}"}~\isacommand{in}~@{text "labels"}. In case
+  clause, written \isacommand{binds}~@{term "{}"}~\isacommand{in}~@{text "labels"}. In case
   of the lambda-terms, the completion produces
 
   \begin{center}
   \begin{tabular}{@ {}l@ {\hspace{-1mm}}}
   \isacommand{nominal\_datatype} @{text lam} =\\
   \hspace{5mm}\phantom{$\mid$}~@{text "Var x::name"}
-    \;\;\isacommand{bind}~@{term "{}"}~\isacommand{in}~@{text "x"}\\
+    \;\;\isacommand{binds}~@{term "{}"}~\isacommand{in}~@{text "x"}\\
   \hspace{5mm}$\mid$~@{text "App t\<^isub>1::lam t\<^isub>2::lam"}
-    \;\;\isacommand{bind}~@{term "{}"}~\isacommand{in}~@{text "t\<^isub>1 t\<^isub>2"}\\
+    \;\;\isacommand{binds}~@{term "{}"}~\isacommand{in}~@{text "t\<^isub>1 t\<^isub>2"}\\
   \hspace{5mm}$\mid$~@{text "Lam x::name t::lam"}
-    \;\;\isacommand{bind}~@{text x} \isacommand{in} @{text t}\\
+    \;\;\isacommand{binds}~@{text x} \isacommand{in} @{text t}\\
   \end{tabular}
   \end{center}
 
@@ -1236,11 +1238,11 @@
   binding clauses @{text "bc\<^isub>1\<dots>bc\<^isub>k"}, the result of @{text
   "fa_ty (C z\<^isub>1 \<dots> z\<^isub>n)"} will be the union @{text
   "fa(bc\<^isub>1) \<union> \<dots> \<union> fa(bc\<^isub>k)"} where we will define below what @{text "fa"} for a binding
-  clause means. We only show the details for the mode \isacommand{bind (set)} (the other modes are similar). 
+  clause means. We only show the details for the mode \isacommand{binds (set)} (the other modes are similar). 
   Suppose the binding clause @{text bc\<^isub>i} is of the form 
   
   \begin{center}
-  \mbox{\isacommand{bind (set)} @{text "b\<^isub>1\<dots>b\<^isub>p"} \isacommand{in} @{text "d\<^isub>1\<dots>d\<^isub>q"}}
+  \mbox{\isacommand{binds (set)} @{text "b\<^isub>1\<dots>b\<^isub>p"} \isacommand{in} @{text "d\<^isub>1\<dots>d\<^isub>q"}}
   \end{center}
   
   \noindent
@@ -1443,7 +1445,7 @@
   empty binding clause of the form
   
   \begin{center}
-  \mbox{\isacommand{bind (set)} @{term "{}"} \isacommand{in} @{text "d\<^isub>1\<dots>d\<^isub>q"}.}
+  \mbox{\isacommand{binds (set)} @{term "{}"} \isacommand{in} @{text "d\<^isub>1\<dots>d\<^isub>q"}.}
   \end{center}
 
   \noindent
@@ -1475,7 +1477,7 @@
   Now suppose the binding clause @{text "bc\<^isub>i"} is of the general form 
   
   \begin{equation}\label{nonempty}
-  \mbox{\isacommand{bind (set)} @{text "b\<^isub>1\<dots>b\<^isub>p"} \isacommand{in} @{text "d\<^isub>1\<dots>d\<^isub>q"}.}
+  \mbox{\isacommand{binds (set)} @{text "b\<^isub>1\<dots>b\<^isub>p"} \isacommand{in} @{text "d\<^isub>1\<dots>d\<^isub>q"}.}
   \end{equation}
 
   \noindent
@@ -1842,14 +1844,14 @@
   %\isacommand{and}~@{text "ty ="}\\
   %\phantom{$|$}~@{text "TVar tvar"}~$|$~@{text "T string"}~$|$~@{text "TApp ty ty"}\\
   %$|$~@{text "TFun string ty_list"}~%
-  %$|$~@{text "TAll tv::tvar tkind ty::ty"}  \isacommand{bind}~@{text "tv"}~\isacommand{in}~@{text ty}\\
+  %$|$~@{text "TAll tv::tvar tkind ty::ty"}  \isacommand{binds}~@{text "tv"}~\isacommand{in}~@{text ty}\\
   %$|$~@{text "TArr ckind ty"}\\
   %\isacommand{and}~@{text "ty_lst ="}\\
   %\phantom{$|$}~@{text "TNil"}~$|$~@{text "TCons ty ty_lst"}\\
   %\isacommand{and}~@{text "cty ="}\\
   %\phantom{$|$}~@{text "CVar cvar"}~%
   %$|$~@{text "C string"}~$|$~@{text "CApp cty cty"}~$|$~@{text "CFun string co_lst"}\\
-  %$|$~@{text "CAll cv::cvar ckind cty::cty"}  \isacommand{bind}~@{text "cv"}~\isacommand{in}~@{text cty}\\
+  %$|$~@{text "CAll cv::cvar ckind cty::cty"}  \isacommand{binds}~@{text "cv"}~\isacommand{in}~@{text cty}\\
   %$|$~@{text "CArr ckind cty"}~$|$~@{text "CRefl ty"}~$|$~@{text "CSym cty"}~$|$~@{text "CCirc cty cty"}\\
   %$|$~@{text "CAt cty ty"}~$|$~@{text "CLeft cty"}~$|$~@{text "CRight cty"}~$|$~@{text "CSim cty cty"}\\
   %$|$~@{text "CRightc cty"}~$|$~@{text "CLeftc cty"}~$|$~@{text "Coerce cty cty"}\\
@@ -1857,15 +1859,15 @@
   %\phantom{$|$}@{text "CNil"}~$|$~@{text "CCons cty co_lst"}\\
   %\isacommand{and}~@{text "trm ="}\\
   %\phantom{$|$}~@{text "Var var"}~$|$~@{text "K string"}\\
-  %$|$~@{text "LAM_ty tv::tvar tkind t::trm"}  \isacommand{bind}~@{text "tv"}~\isacommand{in}~@{text t}\\
-  %$|$~@{text "LAM_cty cv::cvar ckind t::trm"}   \isacommand{bind}~@{text "cv"}~\isacommand{in}~@{text t}\\
+  %$|$~@{text "LAM_ty tv::tvar tkind t::trm"}  \isacommand{binds}~@{text "tv"}~\isacommand{in}~@{text t}\\
+  %$|$~@{text "LAM_cty cv::cvar ckind t::trm"}   \isacommand{binds}~@{text "cv"}~\isacommand{in}~@{text t}\\
   %$|$~@{text "App_ty trm ty"}~$|$~@{text "App_cty trm cty"}~$|$~@{text "App trm trm"}\\
-  %$|$~@{text "Lam v::var ty t::trm"}  \isacommand{bind}~@{text "v"}~\isacommand{in}~@{text t}\\
-  %$|$~@{text "Let x::var ty trm t::trm"}  \isacommand{bind}~@{text x}~\isacommand{in}~@{text t}\\
+  %$|$~@{text "Lam v::var ty t::trm"}  \isacommand{binds}~@{text "v"}~\isacommand{in}~@{text t}\\
+  %$|$~@{text "Let x::var ty trm t::trm"}  \isacommand{binds}~@{text x}~\isacommand{in}~@{text t}\\
   %$|$~@{text "Case trm assoc_lst"}~$|$~@{text "Cast trm co"}\\
   %\isacommand{and}~@{text "assoc_lst ="}\\
   %\phantom{$|$}~@{text ANil}~%
-  %$|$~@{text "ACons p::pat t::trm assoc_lst"}  \isacommand{bind}~@{text "bv p"}~\isacommand{in}~@{text t}\\
+  %$|$~@{text "ACons p::pat t::trm assoc_lst"}  \isacommand{binds}~@{text "bv p"}~\isacommand{in}~@{text t}\\
   %\isacommand{and}~@{text "pat ="}\\
   %\phantom{$|$}~@{text "Kpat string tvtk_lst tvck_lst vt_lst"}\\
   %\isacommand{and}~@{text "vt_lst ="}\\
@@ -2250,18 +2252,18 @@
   meaning in a HOL-based theorem prover. We also had to generalise slightly Ott's 
   binding clauses. In Ott you specify binding clauses with a single body; we 
   allow more than one. We have to do this, because this makes a difference 
-  for our notion of alpha-equivalence in case of \isacommand{bind (set)} and 
-  \isacommand{bind (set+)}. 
+  for our notion of alpha-equivalence in case of \isacommand{binds (set)} and 
+  \isacommand{binds (set+)}. 
   
   Consider the examples
   
   \begin{center}
   \begin{tabular}{@ {}l@ {\hspace{2mm}}l@ {}}
   @{text "Foo\<^isub>1 xs::name fset t::trm s::trm"} &  
-      \isacommand{bind (set)} @{text "xs"} \isacommand{in} @{text "t s"}\\
+      \isacommand{binds (set)} @{text "xs"} \isacommand{in} @{text "t s"}\\
   @{text "Foo\<^isub>2 xs::name fset t::trm s::trm"} &  
-      \isacommand{bind (set)} @{text "xs"} \isacommand{in} @{text "t"}, 
-      \isacommand{bind (set)} @{text "xs"} \isacommand{in} @{text "s"}\\
+      \isacommand{binds (set)} @{text "xs"} \isacommand{in} @{text "t"}, 
+      \isacommand{binds (set)} @{text "xs"} \isacommand{in} @{text "s"}\\
   \end{tabular}
   \end{center}
   
@@ -2296,7 +2298,7 @@
   can be specified using special markers, written @{text "inner"} and 
   @{text "outer"}. It seems our and his specifications can be
   inter-translated as long as ours use the binding mode 
-  \isacommand{bind} only.
+  \isacommand{binds} only.
   However, we have not proved this. Pottier gives a definition for 
   alpha-equivalence, which also uses a permutation operation (like ours).
   Still, this definition is rather different from ours and he only proves that
@@ -2306,7 +2308,7 @@
   
   In a slightly different domain (programming with dependent types), the 
   paper \cite{Altenkirch10} presents a calculus with a notion of 
-  alpha-equivalence related to our binding mode \isacommand{bind (set+)}.
+  alpha-equivalence related to our binding mode \isacommand{binds (set+)}.
   The definition in \cite{Altenkirch10} is similar to the one by Pottier, except that it
   has a more operational flavour and calculates a partial (renaming) map. 
   In this way, the definition can deal with vacuous binders. However, to our




