
diff -r 41c1e98c686f -r e842807d8268 LMCS-Paper/Paper.thy
--- a/LMCS-Paper/Paper.thy	Sun Sep 11 18:04:29 2011 +0100
+++ b/LMCS-Paper/Paper.thy	Mon Sep 12 21:48:26 2011 +0200
@@ -664,7 +664,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 \<pi>} makes the sets of abstracted atoms @{text as} and @{text bs} equal. The
-  requirements {\it (i)} to {\it (iv)} can be stated formally as the conjunction of:
+  requirements {\it (i)} to {\it (iv)} can be stated formally as:
 
   \begin{defi}[Alpha-Equivalence for Set-Bindings]\label{alphaset}\mbox{}\\
   \begin{tabular}{@ {\hspace{10mm}}l@ {\hspace{5mm}}rl}  
@@ -899,6 +899,19 @@
   Finally, taking \eqref{halfone} and \eqref{halftwo} together establishes 
   the first equation of Theorem~\ref{suppabs}. 
 
+  Recall the definition of support \eqref{suppdef}, and note the difference between 
+  the support of a ``raw'' pair and an abstraction
+
+  \[
+  @{term "supp (as, x) = supp as \<union> supp x"}\hspace{15mm}
+  @{term "supp (Abs_set as x) = supp x - as"}
+  \]\smallskip
+
+  \noindent
+  While the permutation operations behave in both cases the same (the permutation
+  is just moved to the arguments), the notion of equality is different for pairs and
+  abstractions. Therefore we have different supports.
+
   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
@@ -1022,25 +1035,27 @@
   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
+  \isacommand{binds} the labels must refer to atom types or to 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:
 
   \[\mbox{
-  \begin{tabular}{@ {}c@ {\hspace{5mm}}c@ {}}
+  \begin{tabular}{@ {}c@ {\hspace{8mm}}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"}\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"}\hspace{3mm}%
+  \hspace{2mm}\phantom{$\mid$}~@{text "TVar name"}\\
+  \hspace{2mm}$\mid$~@{text "TFun ty ty"}\\
+  \isacommand{and}~@{text "tsc ="}\\
+  \hspace{2mm}\phantom{$\mid$}~@{text "TAll xs::(name fset) T::ty"}\hspace{3mm}%
   \isacommand{binds (set+)} @{text xs} \isacommand{in} @{text T}\\
   \end{tabular}
   \end{tabular}}
@@ -1176,16 +1191,16 @@
   \end{equation}\smallskip
 
   \noindent
-  In this example the term constructor @{text "ACons'"} contains a binding 
-  clause, and also is used in the definition of the binding function. The
-  restriction we have to impose is that the binding function can only return
-  free atoms, that is the ones that are not mentioned in a binding clause.
-  Therefore @{text "y"} cannot be used in the binding function @{text "bn"}
-  (since it is bound in @{text "ACons'"} by the binding clause), but @{text x}
-  can (since it is a free atom). This restriction is sufficient for lifting 
-  the binding function to alpha-equated terms. If we would permit that @{text "bn"}
-  can also return @{text "y"}, then it would not be respectful and therefore
-  cannot be lifted.
+  In this example the term constructor @{text "ACons'"} has four arguments and
+  contains a binding clause. This constructor is also used in the definition
+  of the binding function. The restriction we have to impose is that the
+  binding function can only return free atoms, that is the ones that are not
+  mentioned in a binding clause.  Therefore @{text "y"} cannot be used in the
+  binding function @{text "bn"} (since it is bound in @{text "ACons'"} by the
+  binding clause), but @{text x} can (since it is a free atom). This
+  restriction is sufficient for lifting the binding function to alpha-equated
+  terms. If we would permit that @{text "bn"} can also return @{text "y"},
+  then it would not be respectful and therefore cannot be lifted.
 
   In the version of Nominal Isabelle described here, we also adopted the
   restriction from the Ott-tool that binding functions can only return: the
@@ -1499,7 +1514,7 @@
 
   \noindent
   The task below is to specify what the premises corresponding to a binding
-  clause are. To understand better whet the general pattern is, let us first 
+  clause are. To understand better what the general pattern is, let us first 
   treat the special instance where @{text "bc\<^isub>i"} is the empty binding clause 
   of the form
 
@@ -1508,27 +1523,33 @@
   \]\smallskip
 
   \noindent
-  In this binding clause no atom is bound and we only have to `alpha-relate' the bodies. For this
-  we build first the tuples @{text "D \<equiv> (d\<^isub>1,\<dots>, d\<^isub>q)"} and @{text "D' \<equiv> (d\<PRIME>\<^isub>1,\<dots>, d\<PRIME>\<^isub>q)"}  
-  whereby the labels @{text "d"}$_{1..q}$ refer to arguments @{text "z"}$_{1..n}$ and
-  respectively @{text "d\<PRIME>"}$_{1..q}$ to @{text "z\<PRIME>"}$_{1..n}$. In order to relate
-  two such tuples we define the compound alpha-equivalence relation @{text "R"} as follows
-  
+  In this binding clause no atom is bound and we only have to `alpha-relate'
+  the bodies. For this we build first the tuples @{text "D \<equiv> (d\<^isub>1,\<dots>,
+  d\<^isub>q)"} and @{text "D' \<equiv> (d\<PRIME>\<^isub>1,\<dots>, d\<PRIME>\<^isub>q)"}
+  whereby the labels @{text "d"}$_{1..q}$ refer to the arguments @{text
+  "z"}$_{1..n}$ and respectively @{text "d\<PRIME>"}$_{1..q}$ to @{text
+  "z\<PRIME>"}$_{1..n}$ of the term-constructor. In order to relate two such
+  tuples we define the compound alpha-equivalence relation @{text "R"} as
+  follows
+
   \begin{equation}\label{rempty}
   \mbox{@{text "R \<equiv> (R\<^isub>1,\<dots>, R\<^isub>q)"}}
-  \end{equation}
+  \end{equation}\smallskip
 
   \noindent
-  with @{text "R\<^isub>i"} being @{text "\<approx>ty\<^isub>i"} if the corresponding labels @{text "d\<^isub>i"} and 
-  @{text "d\<PRIME>\<^isub>i"} refer
-  to a recursive argument of @{text C} with type @{text "ty\<^isub>i"}; otherwise
-  we take @{text "R\<^isub>i"} to be the equality @{text "="}. This lets us define
-  the premise for an empty binding clause succinctly as @{text "prems(bc\<^isub>i) \<equiv> D R D'"},
-  which can be unfolded to the series of premises
+  with @{text "R\<^isub>i"} being @{text "\<approx>ty\<^isub>i"} if the corresponding
+  labels @{text "d\<^isub>i"} and @{text "d\<PRIME>\<^isub>i"} refer to a
+  recursive argument of @{text C} with type @{text "ty\<^isub>i"}; otherwise
+  we take @{text "R\<^isub>i"} to be the equality @{text "="}. Again the
+  latter is because @{text "ty\<^isub>i"} is not part of the specified types
+  and alpha-equivalence of any previously defined type is supposed to coincide
+  with equality.  This lets us now define the premise for an empty binding
+  clause succinctly as @{text "prems(bc\<^isub>i) \<equiv> D R D'"}, which can be
+  unfolded to the series of premises
   
-  \begin{center}
+  \[
   @{text "d\<^isub>1 R\<^isub>1 d\<PRIME>\<^isub>1  \<dots> d\<^isub>q R\<^isub>q d\<PRIME>\<^isub>q"}.
-  \end{center}
+  \]\smallskip
   
   \noindent
   We will use the unfolded version in the examples below.
@@ -1537,7 +1558,7 @@
   
   \begin{equation}\label{nonempty}
   \mbox{\isacommand{binds (set)} @{text "b\<^isub>1\<dots>b\<^isub>p"} \isacommand{in} @{text "d\<^isub>1\<dots>d\<^isub>q"}.}
-  \end{equation}
+  \end{equation}\smallskip
 
   \noindent
   In this case we define a premise @{text P} using the relation
@@ -1550,83 +1571,82 @@
   For $\approx_{\,\textit{set}}$  we also need
   a compound free-atom function for the bodies defined as
   
-  \begin{center}
+  \[
   \mbox{@{text "fa \<equiv> (fa_ty\<^isub>1,\<dots>, fa_ty\<^isub>q)"}}
-  \end{center}
+  \]\smallskip
 
   \noindent
   with the assumption that the @{text "d"}$_{1..q}$ refer to arguments of types @{text "ty"}$_{1..q}$.
   The last ingredient we need are the sets of atoms bound in the bodies.
   For this we take
 
-  \begin{center}
+  \[
   @{text "B \<equiv> bn_ty\<^isub>1 b\<^isub>1 \<union> \<dots> \<union> bn_ty\<^isub>p b\<^isub>p"}\;.\\
-  \end{center}
+  \]\smallskip
 
   \noindent
   Similarly for @{text "B'"} using the labels @{text "b\<PRIME>"}$_{1..p}$. This 
   lets us formally define the premise @{text P} for a non-empty binding clause as:
   
-  \begin{center}
+  \[
   \mbox{@{term "P \<equiv> alpha_set_ex (B, D) R fa (B', D')"}}\;.
-  \end{center}
+  \]\smallskip
 
   \noindent
   This premise accounts for alpha-equivalence of the bodies of the binding
-  clause. 
-  However, in case the binders have non-recursive deep binders, this premise
-  is not enough:
-  we also have to ``propagate'' alpha-equivalence inside the structure of
-  these binders. An example is @{text "Let"} where we have to make sure the
-  right-hand sides of assignments are alpha-equivalent. For this we use 
-  relations @{text "\<approx>bn"}$_{1..m}$ (which we will formally define shortly).
-  Let us assume the non-recursive deep binders in @{text "bc\<^isub>i"} are
+  clause. However, in case the binders have non-recursive deep binders, this
+  premise is not enough: we also have to ``propagate'' alpha-equivalence
+  inside the structure of these binders. An example is @{text "Let"} where we
+  have to make sure the right-hand sides of assignments are
+  alpha-equivalent. For this we use relations @{text "\<approx>bn"}$_{1..m}$ (which we
+  will formally define shortly).  Let us assume the non-recursive deep binders
+  in @{text "bc\<^isub>i"} are
   
-  \begin{center}
+  \[
   @{text "bn\<^isub>1 l\<^isub>1, \<dots>, bn\<^isub>r l\<^isub>r"}.
-  \end{center}
+  \]\smallskip
   
   \noindent
-  The tuple @{text L} is then @{text "(l\<^isub>1,\<dots>,l\<^isub>r)"} (similarly @{text "L'"})
-  and the compound equivalence relation @{text "R'"} is @{text "(\<approx>bn\<^isub>1,\<dots>,\<approx>bn\<^isub>r)"}. 
-  All premises for @{text "bc\<^isub>i"} are then given by
+  The tuple @{text L} consists then of all these binders @{text "(l\<^isub>1,\<dots>,l\<^isub>r)"} 
+  (similarly @{text "L'"}) and the compound equivalence relation @{text "R'"} 
+  is @{text "(\<approx>bn\<^isub>1,\<dots>,\<approx>bn\<^isub>r)"}.  All premises for @{text "bc\<^isub>i"} are then given by
   
-  \begin{center}
+  \[
   @{text "prems(bc\<^isub>i) \<equiv> P  \<and>   L R' L'"}
-  \end{center} 
+  \]\smallskip
 
   \noindent 
   The auxiliary alpha-equivalence relations @{text "\<approx>bn"}$_{1..m}$ 
   in @{text "R'"} are defined as follows: assuming a @{text bn}-clause is of the form
   
-  \begin{center}
+  \[
   @{text "bn (C z\<^isub>1 \<dots> z\<^isub>s) = rhs"}
-  \end{center}
+  \]\smallskip
   
   \noindent
   where the @{text "z"}$_{1..s}$ are of types @{text "ty"}$_{1..s}$,
   then the corresponding alpha-equivalence clause for @{text "\<approx>bn"} has the form
   
-  \begin{center}
+  \[
   \mbox{\infer{@{text "C z\<^isub>1 \<dots> z\<^isub>s \<approx>bn C z\<PRIME>\<^isub>1 \<dots> z\<PRIME>\<^isub>s"}}
   {@{text "z\<^isub>1 R\<^isub>1 z\<PRIME>\<^isub>1 \<dots> z\<^isub>s R\<^isub>s z\<PRIME>\<^isub>s"}}}
-  \end{center}
+  \]\smallskip
   
   \noindent
   In this clause the relations @{text "R"}$_{1..s}$ are given by 
 
-  \begin{center}
+  \[\mbox{
   \begin{tabular}{c@ {\hspace{2mm}}p{0.9\textwidth}}
   $\bullet$ & @{text "z\<^isub>i \<approx>ty z\<PRIME>\<^isub>i"} provided @{text "z\<^isub>i"} does not occur in @{text rhs} and 
-  is a recursive argument of @{text C},\\
+  is a recursive argument of @{text C},\smallskip\\
   $\bullet$ & @{text "z\<^isub>i = z\<PRIME>\<^isub>i"} provided @{text "z\<^isub>i"} does not occur in @{text rhs}
-  and is a non-recursive argument of @{text C},\\
+  and is a non-recursive argument of @{text C},\smallskip\\
   $\bullet$ & @{text "z\<^isub>i \<approx>bn\<^isub>i z\<PRIME>\<^isub>i"} provided @{text "z\<^isub>i"} occurs in @{text rhs}
-  with the recursive call @{text "bn\<^isub>i x\<^isub>i"} and\\
+  with the recursive call @{text "bn\<^isub>i x\<^isub>i"} and\smallskip\\
   $\bullet$ & @{text True} provided @{text "z\<^isub>i"} occurs in @{text rhs} but without a
   recursive call.
-  \end{tabular}
-  \end{center}
+  \end{tabular}}
+  \]\smallskip
 
   \noindent
   This completes the definition of alpha-equivalence. As a sanity check, we can show
@@ -1638,30 +1658,30 @@
   we have three relations $\approx_{\textit{trm}}$, $\approx_{\textit{assn}}$ and
   $\approx_{\textit{bn}}$ with the following clauses:
 
-  \begin{center}
+  \[\mbox{
   \begin{tabular}{@ {}c @ {}}
   \infer{@{text "Let as t \<approx>\<^bsub>trm\<^esub> Let as' t'"}}
-  {@{term "alpha_lst_ex (bn as, t) alpha_trm fa_trm (bn as', t')"} & @{text "as \<approx>\<^bsub>bn\<^esub> as'"}}\smallskip\\
+  {@{term "alpha_lst_ex (bn as, t) alpha_trm fa_trm (bn as', t')"} & 
+  \hspace{5mm}@{text "as \<approx>\<^bsub>bn\<^esub> as'"}}\\
+  \\
   \makebox[0mm]{\infer{@{text "Let_rec as t \<approx>\<^bsub>trm\<^esub> Let_rec as' t'"}}
-  {@{term "alpha_lst_ex (bn as, ast) alpha_trm2 fa_trm2 (bn as', ast')"}}}
-  \end{tabular}
-  \end{center}
+  {@{term "alpha_lst_ex (bn as, ast) alpha_trm2 fa_trm2 (bn as', ast')"}}}\\
+  \\
 
-  \begin{center}
   \begin{tabular}{@ {}c @ {}}
   \infer{@{text "ANil \<approx>\<^bsub>assn\<^esub> ANil"}}{}\hspace{9mm}
   \infer{@{text "ACons a t as \<approx>\<^bsub>assn\<^esub> ACons a' t' as"}}
-  {@{text "a = a'"} & @{text "t \<approx>\<^bsub>trm\<^esub> t'"} & @{text "as \<approx>\<^bsub>assn\<^esub> as'"}}
-  \end{tabular}
-  \end{center}
+  {@{text "a = a'"} & \hspace{5mm}@{text "t \<approx>\<^bsub>trm\<^esub> t'"} & \hspace{5mm}@{text "as \<approx>\<^bsub>assn\<^esub> as'"}}
+  \end{tabular}\\
+  \\
 
-  \begin{center}
   \begin{tabular}{@ {}c @ {}}
   \infer{@{text "ANil \<approx>\<^bsub>bn\<^esub> ANil"}}{}\hspace{9mm}
   \infer{@{text "ACons a t as \<approx>\<^bsub>bn\<^esub> ACons a' t' as"}}
-  {@{text "t \<approx>\<^bsub>trm\<^esub> t'"} & @{text "as \<approx>\<^bsub>bn\<^esub> as'"}}
+  {@{text "t \<approx>\<^bsub>trm\<^esub> t'"} & \hspace{5mm}@{text "as \<approx>\<^bsub>bn\<^esub> as'"}}
   \end{tabular}
-  \end{center}
+  \end{tabular}}
+  \]\smallskip
 
   \noindent
   Note the difference between  $\approx_{\textit{assn}}$ and
@@ -1677,37 +1697,81 @@
 section {* Establishing the Reasoning Infrastructure *}
 
 text {*
-  Having made all necessary definitions for raw terms, we can start
-  with establishing the reasoning infrastructure for the alpha-equated types
-  @{text "ty\<AL>"}$_{1..n}$, that is the types the user originally specified. We sketch
-  in this section the proofs we need for establishing this infrastructure. One
-  main point of our work is that we have completely automated these proofs in Isabelle/HOL.
+  Having made all necessary definitions for raw terms, we can start with
+  establishing the reasoning infrastructure for the alpha-equated types @{text
+  "ty\<AL>"}$_{1..n}$, that is the types the user originally specified. We
+  give in this section and the next the proofs we need for establishing this
+  infrastructure. One main point of our work is that we have completely
+  automated these proofs in Isabelle/HOL.
+
+  First we establish that the free-variable functions, the binding functions and the
+  alpha-equivalences are equivariant.
 
-  First we establish that the
-  alpha-equivalence relations defined in the previous section are 
-  equivalence relations.
+  \begin{lem}\mbox{}\\
+  @{text "(i)"} The functions @{text "fa_ty"}$_{1..n}$, @{text "fa_bn"}$_{1..m}$ and
+  @{text "bn"}$_{1..m}$ are equivariant.\\
+  @{text "(ii)"} The relations @{text "\<approx>ty"}$_{1..n}$ and
+  @{text "\<approx>bn"}$_{1..m}$ are equivariant.
+  \end{lem}
+
+  \begin{proof}
+  The function package of Isabelle/HOL allows us to prove the first part is by mutual 
+  induction over the definitions of the functions. The second is by a straightforward
+  induction over the rules of @{text "\<approx>ty"}$_{1..n}$ and @{text "\<approx>bn"}$_{1..m}$ using 
+  the first part.
+  \end{proof}
+
+  \noindent
+  Next we establish that the alpha-equivalence relations defined in the
+  previous section are equivalence relations.
 
   \begin{lem}\label{equiv} 
-  Given the raw types @{text "ty"}$_{1..n}$ and binding functions
-  @{text "bn"}$_{1..m}$, the relations @{text "\<approx>ty"}$_{1..n}$ and 
-  @{text "\<approx>bn"}$_{1..m}$ are equivalence relations. and equivariant.
+  The relations @{text "\<approx>ty"}$_{1..n}$ and @{text "\<approx>bn"}$_{1..m}$ are
+  equivalence relations.
   \end{lem}
 
   \begin{proof} 
   The proof is by mutual induction over the definitions. The non-trivial
   cases involve premises built up by $\approx_{\textit{set}}$, 
   $\approx_{\textit{set+}}$ and $\approx_{\textit{list}}$. They 
-  can be dealt with as in Lemma~\ref{alphaeq}.
+  can be dealt with as in Lemma~\ref{alphaeq}. However, the transitivity
+  case needs in addition the fact that the relations are equivariant. 
   \end{proof}
 
   \noindent 
   We can feed this lemma into our quotient package and obtain new types @{text
   "ty"}$^\alpha_{1..n}$ representing alpha-equated terms of types @{text "ty"}$_{1..n}$. 
+  
   We also obtain definitions for the term-constructors @{text
-  "C"}$^\alpha_{1..k}$ from the raw term-constructors @{text
-  "C"}$_{1..k}$, and similar definitions for the free-atom functions @{text
-  "fa_ty"}$^\alpha_{1..n}$ and @{text "fa_bn"}$^\alpha_{1..m}$ as well as the binding functions @{text
-  "bn"}$^\alpha_{1..m}$. However, these definitions are not really useful to the 
+  "C"}$^\alpha_{1..k}$ from the raw term-constructors @{text "C"}$_{1..k}$,
+  and similar definitions for the free-atom functions @{text
+  "fa_ty"}$^\alpha_{1..n}$ and @{text "fa_bn"}$^\alpha_{1..m}$ as well as the
+  binding functions @{text "bn"}$^\alpha_{1..m}$. For this we have to show
+  by induction over the definitions of alpha-equivalences that the ``raw'' 
+  functions are respectful. This means we need to establish that
+
+  \[\mbox{
+  \begin{tabular}{lll}
+  @{text "x \<approx>ty\<^isub>i x'"} & implies & @{text "fa_ty\<^isub>i x = fa_ty\<^isub>i x'"}\\
+  @{text "x \<approx>ty\<^isub>l x'"} & implies & @{text "fa_bn\<^isub>j x = fa_bn\<^isub>j x'"}\\
+  @{text "x \<approx>ty\<^isub>l x'"} & implies & @{text "bn\<^isub>j x = bn\<^isub>j x'"}\\
+  \end{tabular}
+  }\]\smallskip
+  
+  \noindent
+  holds whereby @{text "ty\<^isub>l"} is the type over which @{text "bn\<^isub>j"} is defined. A 
+  similar property is needed for the constructors @{text "C"}$_{1..k}$. In order 
+  to establish it we need to prove that
+
+  \[\mbox{
+  \begin{tabular}{lll}
+  @{text "x \<approx>ty\<^isub>l x'"} & implies & @{text "x \<approx>bn\<^isub>j x'"}\\
+  \end{tabular}
+  }\]\smallskip
+
+  \noindent
+  The respectfulness properties are crucial, ... ???
+  However, these definitions are not really useful to the 
   user, since they are given in terms of the isomorphisms we obtained by 
   creating new types in Isabelle/HOL (recall the picture shown in the 
   Introduction).
@@ -1716,19 +1780,19 @@
   term-constructors are not 
   equal, that is
   
-  \begin{equation}\label{distinctalpha}
+  \[\label{distinctalpha}
   \mbox{@{text "C"}$^\alpha$~@{text "x\<^isub>1 \<dots> x\<^isub>r"}~@{text "\<noteq>"}~% 
   @{text "D"}$^\alpha$~@{text "y\<^isub>1 \<dots> y\<^isub>s"}} 
-  \end{equation}
+  \]\smallskip
   
   \noindent
   whenever @{text "C"}$^\alpha$~@{text "\<noteq>"}~@{text "D"}$^\alpha$.
   In order to derive this fact, we use the definition of alpha-equivalence
   and establish that
   
-  \begin{equation}\label{distinctraw}
+  \[\label{distinctraw}
   \mbox{@{text "C x\<^isub>1 \<dots> x\<^isub>r"}\;$\not\approx$@{text ty}\;@{text "D y\<^isub>1 \<dots> y\<^isub>s"}}
-  \end{equation}
+  \]\smallskip
 
   \noindent
   holds for the corresponding raw term-constructors.
@@ -1774,20 +1838,20 @@
 
   Having established respectfulness for the raw term-constructors, the 
   quotient package is able to automatically deduce \eqref{distinctalpha} from 
-  \eqref{distinctraw}. Having the facts \eqref{fnresp} at our disposal, we can 
+  \eqref{distinctraw}. ??? Having the facts \eqref{fnresp} at our disposal, we can 
   also lift properties that characterise when two raw terms of the form
-  %
-  \begin{center}
-  @{text "C x\<^isub>1 \<dots> x\<^isub>r \<approx>ty C x\<PRIME>\<^isub>1 \<dots> x\<PRIME>\<^isub>r"}
-  \end{center}
+  
+  \[
+  \mbox{@{text "C x\<^isub>1 \<dots> x\<^isub>r \<approx>ty C x\<PRIME>\<^isub>1 \<dots> x\<PRIME>\<^isub>r"}}
+  \]\smallskip
 
   \noindent
   are alpha-equivalent. This gives us conditions when the corresponding
   alpha-equated terms are \emph{equal}, namely
   
-  \begin{center}
+  \[
   @{text "C\<^sup>\<alpha> x\<^isub>1 \<dots> x\<^isub>r = C\<^sup>\<alpha> x\<PRIME>\<^isub>1 \<dots> x\<PRIME>\<^isub>r"}.
-  \end{center}
+  \]\smallskip
   
   \noindent
   We call these conditions as \emph{quasi-injectivity}. They correspond to
@@ -1803,8 +1867,8 @@
   As a result we can add the equations
   
   \begin{equation}\label{calphaeqvt}
-  @{text "p \<bullet> (C\<^sup>\<alpha> x\<^isub>1 \<dots> x\<^isub>r) = C\<^sup>\<alpha> (p \<bullet> x\<^isub>1) \<dots> (p \<bullet> x\<^isub>r)"}
-  \end{equation}
+  @{text "\<pi> \<bullet> (C\<^sup>\<alpha> x\<^isub>1 \<dots> x\<^isub>r) = C\<^sup>\<alpha> (\<pi> \<bullet> x\<^isub>1) \<dots> (\<pi> \<bullet> x\<^isub>r)"}
+  \end{equation}\smallskip
 
   \noindent
   to our infrastructure. In a similar fashion we can lift the defining equations
@@ -1821,7 +1885,7 @@
   
   \begin{equation}\label{weakinduct}
   \mbox{@{text "P\<^isub>1 x\<^isub>1 \<and> \<dots> \<and> P\<^isub>n x\<^isub>n "}}
-  \end{equation} 
+  \end{equation} \smallskip
   
   \noindent
   whereby the @{text P}$_{1..n}$ are predicates and the @{text x}$_{1..n}$ 
@@ -1830,7 +1894,7 @@
   
   \begin{equation}\label{weakprem}
   \mbox{@{text "\<forall>x\<^isub>1\<dots>x\<^isub>r. P\<^isub>i x\<^isub>i \<and> \<dots> \<and> P\<^isub>j x\<^isub>j \<Rightarrow> P (C\<^sup>\<alpha> x\<^isub>1 \<dots> x\<^isub>r)"}} 
-  \end{equation}
+  \end{equation}\smallskip
 
   \noindent 
   in which the @{text "x"}$_{i..j}$ @{text "\<subseteq>"} @{text "x"}$_{1..r}$ are 
@@ -1840,24 +1904,25 @@
   can first show that the free-atom functions and binding functions are
   equivariant, namely
   
-  \begin{center}
-  \begin{tabular}{rcl@ {\hspace{10mm}}rcl}
-  @{text "p \<bullet> (fa_ty\<AL>\<^isub>i  x)"} & $=$ & @{text "fa_ty\<AL>\<^isub>i (p \<bullet> x)"} &
-  @{text "p \<bullet> (bn\<AL>\<^isub>j  x)"}    & $=$ & @{text "bn\<AL>\<^isub>j (p \<bullet> x)"}\\
-  @{text "p \<bullet> (fa_bn\<AL>\<^isub>j  x)"} & $=$ & @{text "fa_bn\<AL>\<^isub>j (p \<bullet> x)"}\\
-  \end{tabular}
-  \end{center}
+  \[\mbox{
+  \begin{tabular}{rcl}
+  @{text "\<pi> \<bullet> (fa_ty\<AL>\<^isub>i  x)"} & $=$ & @{text "fa_ty\<AL>\<^isub>i (\<pi> \<bullet> x)"}\\
+  @{text "\<pi> \<bullet> (fa_bn\<AL>\<^isub>j  x)"} & $=$ & @{text "fa_bn\<AL>\<^isub>j (\<pi> \<bullet> x)"}\\
+  @{text "\<pi> \<bullet> (bn\<AL>\<^isub>j  x)"}    & $=$ & @{text "bn\<AL>\<^isub>j (\<pi> \<bullet> x)"}\\
+  \end{tabular}}
+  \]
+
   
   \noindent
-  These properties can be established using the induction principle for the types @{text "ty\<AL>"}$_{1..n}$.
-  in \eqref{weakinduct}.
-  Having these equivariant properties established, we can
-  show that the support of term-constructors @{text "C\<^sup>\<alpha>"} is included in
-  the support of its arguments, that means 
+  These properties can be established using the induction principle for the
+  types @{text "ty\<AL>"}$_{1..n}$.  in \eqref{weakinduct}.  Having these
+  equivariant properties established, we can show that the support of
+  term-constructors @{text "C\<^sup>\<alpha>"} is included in the support of its
+  arguments, that means
 
-  \begin{center}
+  \[
   @{text "supp (C\<^sup>\<alpha> x\<^isub>1 \<dots> x\<^isub>r) \<subseteq> (supp x\<^isub>1 \<union> \<dots> \<union> supp x\<^isub>r)"}
-  \end{center}
+  \]\smallskip
  
   \noindent
   holds. This allows us to prove by induction that
@@ -2244,37 +2309,42 @@
 
 text {*
   To our knowledge the earliest usage of general binders in a theorem prover
-  is described in \cite{NaraschewskiNipkow99} about a formalisation of the
-  algorithm W. This formalisation implements binding in type-schemes using a
-  de-Bruijn indices representation. Since type-schemes in W contain only a single
-  place where variables are bound, different indices do not refer to different binders (as in the usual
-  de-Bruijn representation), but to different bound variables. A similar idea
-  has been recently explored for general binders in the locally nameless
-  approach to binding \cite{chargueraud09}.  There, de-Bruijn indices consist
-  of two numbers, one referring to the place where a variable is bound, and the
-  other to which variable is bound. The reasoning infrastructure for both
-  representations of bindings comes for free in theorem provers like Isabelle/HOL or
-  Coq, since the corresponding term-calculi can be implemented as ``normal''
-  datatypes.  However, in both approaches it seems difficult to achieve our
-  fine-grained control over the ``semantics'' of bindings (i.e.~whether the
-  order of binders should matter, or vacuous binders should be taken into
-  account). To do so, one would require additional predicates that filter out
-  unwanted terms. Our guess is that such predicates result in rather
-  intricate formal reasoning.
+  is described by Nara\-schew\-ski and Nipkow \cite{NaraschewskiNipkow99} with a
+  formalisation of the algorithm W. This formalisation implements binding in
+  type-schemes using a de-Bruijn indices representation. Since type-schemes in
+  W contain only a single place where variables are bound, different indices
+  do not refer to different binders (as in the usual de-Bruijn
+  representation), but to different bound variables. A similar idea has been
+  recently explored for general binders by Chargu\'eraud in the locally nameless 
+  approach to
+  binding \cite{chargueraud09}.  There, de-Bruijn indices consist of two
+  numbers, one referring to the place where a variable is bound, and the other
+  to which variable is bound. The reasoning infrastructure for both
+  representations of bindings comes for free in theorem provers like
+  Isabelle/HOL or Coq, since the corresponding term-calculi can be implemented
+  as ``normal'' datatypes.  However, in both approaches it seems difficult to
+  achieve our fine-grained control over the ``semantics'' of bindings
+  (i.e.~whether the order of binders should matter, or vacuous binders should
+  be taken into account). To do so, one would require additional predicates
+  that filter out unwanted terms. Our guess is that such predicates result in
+  rather intricate formal reasoning. We are not aware of any non-trivial 
+  formalisation that uses Chargu\'eraud's idea.
+
 
   Another technique for representing binding is higher-order abstract syntax
-  (HOAS). , which for example is implemented in the Twelf system. 
-  This representation
-  technique supports very elegantly many aspects of \emph{single} binding, and
-  impressive work has been done that uses HOAS for mechanising the metatheory
-  of SML~\cite{LeeCraryHarper07}. We are, however, not aware how multiple
-  binders of SML are represented in this work. Judging from the submitted
-  Twelf-solution for the POPLmark challenge, HOAS cannot easily deal with
-  binding constructs where the number of bound variables is not fixed. For example 
-  In the second part of this challenge, @{text "Let"}s involve
-  patterns that bind multiple variables at once. In such situations, HOAS
-  seems to have to resort to the iterated-single-binders-approach with
-  all the unwanted consequences when reasoning about the resulting terms.
+  (HOAS), which for example is implemented in the Twelf system. This
+  representation technique supports very elegantly many aspects of
+  \emph{single} binding, and impressive work by Lee et al has been done that
+  uses HOAS for mechanising the metatheory of SML~\cite{LeeCraryHarper07}. We
+  are, however, not aware how multiple binders of SML are represented in this
+  work. Judging from the submitted Twelf-solution for the POPLmark challenge,
+  HOAS cannot easily deal with binding constructs where the number of bound
+  variables is not fixed. For example In the second part of this challenge,
+  @{text "Let"}s involve patterns that bind multiple variables at once. In
+  such situations, HOAS seems to have to resort to the
+  iterated-single-binders-approach with all the unwanted consequences when
+  reasoning about the resulting terms.
+
 
   Two formalisations involving general binders have been 
   performed in older
@@ -2285,117 +2355,126 @@
   the need to ``unbind'' variables. This can be done in one step with our
   general binders described in this paper, but needs a cumbersome
   iteration with single binders. The resulting formal reasoning turned out to
-  be rather unpleasant. The hope is that the extension presented in this paper
-  is a substantial improvement.
+  be rather unpleasant. 
  
-  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
-  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
-  alpha-equivalence of terms that can be specified in Ott.  This definition is
-  rather different from ours, not using any nominal techniques.  To our
-  knowledge there is no concrete mathematical result concerning this
-  notion of alpha-equivalence.  Also the definition for the 
-  notion of free variables
-  is work in progress.
+  The most closely related work to the one presented here is the Ott-tool by
+  Sewell et al \cite{ott-jfp} and the C$\alpha$ml language by Pottier
+  \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 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 alpha-equivalence and free variables for terms that can be
+  specified in Ott.  This definition is rather different from ours, not using
+  any nominal techniques.  To our knowledge there is no concrete mathematical
+  result concerning this notion of alpha-equivalence and free variables. We
+  have proved that our definitions lead to alpha-equated terms, whose support
+  is as expected (that means bound names are removed from the support). We
+  also showed that our specifications lift from a raw type to a type of
+  alpha-equivalence classes. For this we were able to establish then every
+  term-constructor and function is repectful w.r.t.~alpha-equivalence.
 
-  Although we were heavily inspired by the syntax of Ott,
-  its definition of alpha-equi\-valence is unsuitable for our extension of
-  Nominal Isabelle. First, it is far too complicated to be a basis for
-  automated proofs implemented on the ML-level of Isabelle/HOL. Second, it
-  covers cases of binders depending on other binders, which just do not make
-  sense for our alpha-equated terms. Third, it allows empty types that have no
-  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{binds (set)} and 
-  \isacommand{binds (set+)}. 
+  Although we were heavily inspired by the syntax of Ott, its definition of
+  alpha-equi\-valence is unsuitable for our extension of Nominal
+  Isabelle. First, it is far too complicated to be a basis for automated
+  proofs implemented on the ML-level of Isabelle/HOL. Second, it covers cases
+  of binders depending on other binders, which just do not make sense for our
+  alpha-equated terms. Third, it allows empty types that have no meaning in a
+  HOL-based theorem prover. We also had to generalise slightly Ott's binding
+  clauses. In Ott one specifies 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{binds (set)} and
+  \isacommand{binds (set+)}. Consider the examples
   
-  Consider the examples
-  
-  \begin{center}
+  \[\mbox{
   \begin{tabular}{@ {}l@ {\hspace{2mm}}l@ {}}
   @{text "Foo\<^isub>1 xs::name fset t::trm s::trm"} &  
       \isacommand{binds (set)} @{text "xs"} \isacommand{in} @{text "t s"}\\
   @{text "Foo\<^isub>2 xs::name fset t::trm s::trm"} &  
       \isacommand{binds (set)} @{text "xs"} \isacommand{in} @{text "t"}, 
       \isacommand{binds (set)} @{text "xs"} \isacommand{in} @{text "s"}\\
-  \end{tabular}
-  \end{center}
-  
-  \noindent
-  In the first term-constructor we have a single
-  body that happens to be ``spread'' over two arguments; in the second term-constructor we have
-  two independent bodies in which the same variables are bound. As a result we 
-  have
-   
-  \begin{center}
-  \begin{tabular}{r@ {\hspace{1.5mm}}c@ {\hspace{1.5mm}}l}
-  @{text "Foo\<^isub>1 {a, b} (a, b) (a, b)"} & $\not=$ & 
-  @{text "Foo\<^isub>1 {a, b} (a, b) (b, a)"}\\
-  @{text "Foo\<^isub>2 {a, b} (a, b) (a, b)"} & $=$ & 
-  @{text "Foo\<^isub>2 {a, b} (a, b) (b, a)"}\\
-  \end{tabular}
-  \end{center}
+  \end{tabular}}
+  \]\smallskip
   
   \noindent
-  and therefore need the extra generality to be able to distinguish between 
-  both specifications.
-  Because of how we set up our definitions, we also had to impose some restrictions
-  (like a single binding function for a deep binder) that are not present in Ott. 
-  Our
-  expectation is that we can still cover many interesting term-calculi from
-  programming language research, for example Core-Haskell. 
+  In the first term-constructor we have a single body that happens to be
+  ``spread'' over two arguments; in the second term-constructor we have two
+  independent bodies in which the same variables are bound. As a result we
+  have\footnote{Assuming @{term "a \<noteq> b"}, there is no permutation that can
+  make @{text "(a, b)"} equal with @{text "(a, b)"} and @{text "(b, a)"}, but
+  there are two permutations so that we can make @{text "(a, b)"} and @{text
+  "(a, b)"} equal with one permutation, and @{text "(a, b)"} and @{text "(b,
+  a)"} with the other.}
+
+   
+  \[\mbox{
+  \begin{tabular}{r@ {\hspace{1.5mm}}c@ {\hspace{1.5mm}}l}
+  @{text "Foo\<^isub>1 {a, b} (a, b) (a, b)"} & $\not=$ & 
+  @{text "Foo\<^isub>1 {a, b} (a, b) (b, a)"}
+  \end{tabular}}
+  \]\smallskip
+ 
+  \noindent
+  but 
 
-  Pottier presents in \cite{Pottier06} a language, called C$\alpha$ml, for 
-  representing terms with general binders inside OCaml. This language is
-  implemented as a front-end that can be translated to OCaml with the help of
-  a library. He presents a type-system in which the scope of general binders
-  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{binds} only.
-  However, we have not proved this. Pottier gives a definition for 
+  \[\mbox{
+  \begin{tabular}{r@ {\hspace{1.5mm}}c@ {\hspace{1.5mm}}l}
+  @{text "Foo\<^isub>2 {a, b} (a, b) (a, b)"} & $=$ & 
+  @{text "Foo\<^isub>2 {a, b} (a, b) (b, a)"}\\
+  \end{tabular}}
+  \]\smallskip
+  
+  \noindent
+  and therefore need the extra generality to be able to distinguish between
+  both specifications.  Because of how we set up our definitions, we also had
+  to impose some restrictions (like a single binding function for a deep
+  binder) that are not present in Ott. Our expectation is that we can still
+  cover many interesting term-calculi from programming language research, for
+  example Core-Haskell. ???
+
+  Pottier presents a programming language, called C$\alpha$ml, for
+  representing terms with general binders inside OCaml \cite{Pottier06}. This
+  language is implemented as a front-end that can be translated to OCaml with
+  the help of a library. He presents a type-system in which the scope of
+  general binders 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{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
-  it defines an equivalence relation. A complete
-  reasoning infrastructure is well beyond the purposes of his language. 
-  Similar work for Haskell with similar results was reported by Cheney \cite{Cheney05a}.
-  
-  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{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
-  best knowledge, no concrete mathematical result concerning this
-  definition of alpha-equivalence has been proved.  
+  it defines an equivalence relation. A complete reasoning infrastructure is
+  well beyond the purposes of his language. Similar work for Haskell with
+  similar results was reported by Cheney \cite{Cheney05a} and more recently 
+  by ???
+
+  In a slightly different domain (programming with dependent types),
+  Altenkirch et al present a calculus with a notion of alpha-equivalence
+  related to our binding mode \isacommand{binds (set+)} \cite{Altenkirch10}.
+  Their definition 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 best
+  knowledge, no concrete mathematical result concerning this definition of
+  alpha-equivalence has been proved.
 *}
 
 section {* Conclusion *}
 
 text {*
-  Telsescopes by de Bruijn (AUTOMATH project does not provide an automatic infrastructure).
+  %%Telsescopes by de Bruijn (AUTOMATH project does not provide an automatic infrastructure).
 
 
-  We have presented an extension of Nominal Isabelle for dealing with
-  general binders, that is term-constructors having multiple bound 
-  variables. For this extension we introduced new definitions of 
-  alpha-equivalence and automated all necessary proofs in Isabelle/HOL.
-  To specify general binders we used the specifications from Ott, but extended them 
-  in some places and restricted
-  them in others so that they make sense in the context of alpha-equated terms. 
-  We also introduced two binding modes (set and set+) that do not 
-  exist in Ott. 
-  We have tried out the extension with calculi such as Core-Haskell, type-schemes 
-  and approximately a  dozen of other typical examples from programming 
-  language research~\cite{SewellBestiary}. 
-  The code
-  will eventually become part of the next Isabelle distribution.\footnote{For the moment
-  it can be downloaded from the Mercurial repository linked at
+  We have presented an extension of Nominal Isabelle for dealing with general
+  binders, that is term-constructors having multiple bound variables. For this
+  extension we introduced new definitions of alpha-equivalence and automated
+  all necessary proofs in Isabelle/HOL.  To specify general binders we used
+  the syntax from Ott, but extended it in some places and restricted
+  it in others so that they make sense in the context of alpha-equated
+  terms. We also introduced two binding modes (set and set+) that do not exist
+  in Ott. We have tried out the extension with calculi such as Core-Haskell,
+  type-schemes and approximately a dozen of other typical examples from
+  programming language research~\cite{SewellBestiary}. The code will
+  eventually become part of the next Isabelle distribution.\footnote{It 
+  can be downloaded already from the Mercurial repository linked at
   \href{http://isabelle.in.tum.de/nominal/download}
   {http://isabelle.in.tum.de/nominal/download}.}
 
@@ -2412,7 +2491,9 @@
   datatype definitions allow one to specify, for instance, the function kinds
   in Core-Haskell as @{text "TFun string (ty list)"} instead of the unfolded
   version @{text "TFun string ty_list"} (see Figure~\ref{nominalcorehas}). To
-  achieve this, we need a slightly more clever implementation than we have at the moment. 
+  achieve this, we need more clever implementation than we have 
+  at the moment. However, really lifting this restriction will involve major
+  work on the datatype package of Isabelle/HOL.
 
   A more interesting line of investigation is whether we can go beyond the 
   simple-minded form of binding functions that we adopted from Ott. At the moment, binding
@@ -2420,18 +2501,18 @@
   of atom sets (similarly for lists). It remains to be seen whether 
   properties like
   
-  \begin{center}
-  @{text "fa_ty x  =  bn x \<union> fa_bn x"}.
-  \end{center}
+  \[
+  \mbox{@{text "fa_ty x  =  bn x \<union> fa_bn x"}}
+  \]\smallskip
   
   \noindent
   allow us to support more interesting binding functions. 
   
   We have also not yet played with other binding modes. For example we can
-  imagine that there is need for a binding mode where instead of lists, we
-  abstract lists of distinct elements.  Once we feel confident about such
-  binding modes, our implementation can be easily extended to accommodate
-  them.\medskip
+  imagine that there is need for a binding mode where instead of usual lists,
+  we abstract lists of distinct elements (the corresponding type @{text
+  "dlist"} already exists in the library of Isabelle/HOL). We expect the
+  presented work can be easily extended to accommodate them.\medskip
   
   \noindent
   {\bf Acknowledgements:} We are very grateful to Andrew Pitts for many




