
diff -r b1549d391ea7 -r f659ce282610 Paper/Paper.thy
--- a/Paper/Paper.thy	Tue Jun 29 18:00:59 2010 +0100
+++ b/Paper/Paper.thy	Wed Jun 30 16:56:37 2010 +0100
@@ -21,9 +21,9 @@
   supp ("supp _" [78] 73) and
   uminus ("-_" [78] 73) and
   If  ("if _ then _ else _" 10) and
-  alpha_gen ("_ \<approx>\<^raw:\raisebox{-1pt}{\makebox[0mm][l]{$\,_{\textit{set}}$}}>\<^bsup>_, _, _\<^esup> _") and
-  alpha_lst ("_ \<approx>\<^raw:\raisebox{-1pt}{\makebox[0mm][l]{$\,_{\textit{list}}$}}>\<^bsup>_, _, _\<^esup> _") and
-  alpha_res ("_ \<approx>\<^raw:\raisebox{-1pt}{\makebox[0mm][l]{$\,_{\textit{res}}$}}>\<^bsup>_, _, _\<^esup> _") and
+  alpha_gen ("_ \<approx>\<^raw:\,\raisebox{-1pt}{\makebox[0mm][l]{$_{\textit{set}}$}}>\<^bsup>_, _, _\<^esup> _") and
+  alpha_lst ("_ \<approx>\<^raw:\,\raisebox{-1pt}{\makebox[0mm][l]{$_{\textit{list}}$}}>\<^bsup>_, _, _\<^esup> _") and
+  alpha_res ("_ \<approx>\<^raw:\,\raisebox{-1pt}{\makebox[0mm][l]{$_{\textit{res}}$}}>\<^bsup>_, _, _\<^esup> _") and
   abs_set ("_ \<approx>\<^raw:{$\,_{\textit{abs\_set}}$}> _") and
   abs_set2 ("_ \<approx>\<^raw:\raisebox{-1pt}{\makebox[0mm][l]{$\,_{\textit{list}}$}}>\<^bsup>_\<^esup>  _") and
   fv ("fv'(_')" [100] 100) and
@@ -46,14 +46,14 @@
 %%%  @{text "(1, (2, 3))"}
 
   So far, Nominal Isabelle provides a mechanism for constructing
-  alpha-equated terms, for example
+  $\alpha$-equated terms, for example
 
   \begin{center}
   @{text "t ::= x | t t | \<lambda>x. t"}
   \end{center}
 
   \noindent
-  where free and bound variables have names.  For such alpha-equated terms,
+  where free and bound variables have names.  For such $\alpha$-equated terms,
   Nominal Isabelle derives automatically a reasoning infrastructure that has
   been used successfully in formalisations of an equivalence checking
   algorithm for LF \cite{UrbanCheneyBerghofer08}, Typed
@@ -87,7 +87,7 @@
   Binding multiple variables has interesting properties that cannot be captured
   easily by iterating single binders. For example in the case of type-schemes we do not
   want to make a distinction about the order of the bound variables. Therefore
-  we would like to regard the following two type-schemes as alpha-equivalent
+  we would like to regard the following two type-schemes as $\alpha$-equivalent
   %
   \begin{equation}\label{ex1}
   @{text "\<forall>{x, y}. x \<rightarrow> y  \<approx>\<^isub>\<alpha>  \<forall>{y, x}. y \<rightarrow> x"} 
@@ -95,14 +95,14 @@
 
   \noindent
   but assuming that @{text x}, @{text y} and @{text z} are distinct variables,
-  the following two should \emph{not} be alpha-equivalent
+  the following two should \emph{not} be $\alpha$-equivalent
   %
   \begin{equation}\label{ex2}
   @{text "\<forall>{x, y}. x \<rightarrow> y  \<notapprox>\<^isub>\<alpha>  \<forall>{z}. z \<rightarrow> z"} 
   \end{equation}
 
   \noindent
-  Moreover, we like to regard type-schemes as alpha-equivalent, if they differ
+  Moreover, we like to regard type-schemes as $\alpha$-equivalent, if they differ
   only on \emph{vacuous} binders, such as
   %
   \begin{equation}\label{ex3}
@@ -111,13 +111,13 @@
 
   \noindent
   where @{text z} does not occur freely in the type.  In this paper we will
-  give a general binding mechanism and associated notion of alpha-equivalence
+  give a general binding mechanism and associated notion of $\alpha$-equivalence
   that can be used to faithfully represent this kind of binding in Nominal
-  Isabelle.  The difficulty of finding the right notion for alpha-equivalence
+  Isabelle.  The difficulty of finding the right notion for $\alpha$-equivalence
   can be appreciated in this case by considering that the definition given by
   Leroy in \cite{Leroy92} is incorrect (it omits a side-condition). 
 
-  However, the notion of alpha-equivalence that is preserved by vacuous
+  However, the notion of $\alpha$-equivalence that is preserved by vacuous
   binders is not always wanted. For example in terms like
   %
   \begin{equation}\label{one}
@@ -125,9 +125,9 @@
   \end{equation}
 
   \noindent
-  we might not care in which order the assignments $x = 3$ and $y = 2$ are
-  given, but it would be unusual to regard \eqref{one} as alpha-equivalent 
-  with
+  we might not care in which order the assignments @{text "x = 3"} and
+  \mbox{@{text "y = 2"}} are given, but it would be unusual to regard
+  \eqref{one} as $\alpha$-equivalent with
   %
   \begin{center}
   @{text "\<LET> x = 3 \<AND> y = 2 \<AND> z = loop \<IN> x - y \<END>"}
@@ -149,7 +149,7 @@
   \noindent
   we want to bind all variables from the pattern inside the body of the
   $\mathtt{let}$, but we also care about the order of these variables, since
-  we do not want to regard \eqref{two} as alpha-equivalent with
+  we do not want to regard \eqref{two} as $\alpha$-equivalent with
   %
   \begin{center}
   @{text "\<LET> (y, x) = (3, 2) \<IN> x - y \<END>"}
@@ -176,27 +176,26 @@
   we represent the @{text "\<LET>"}-constructor by something like
   %
   \begin{center}
-  @{text "\<LET> [x\<^isub>1,\<dots>,x\<^isub>n].s [t\<^isub>1,\<dots>,t\<^isub>n]"}
+  @{text "\<LET> (\<lambda>x\<^isub>1\<dots>x\<^isub>n . s)  [t\<^isub>1,\<dots>,t\<^isub>n]"}
   \end{center}
 
   \noindent
-  where the notation @{text "[_]._"} indicates that the list of @{text "x\<^isub>i"}
-  becomes bound in @{text s}. In this representation the term 
-  \mbox{@{text "\<LET> [x].s [t\<^isub>1, t\<^isub>2]"}} is a perfectly legal
-  instance, but the lengths of the two lists do not agree. To exclude such terms, 
-  additional predicates about well-formed
-  terms are needed in order to ensure that the two lists are of equal
-  length. This can result in very messy reasoning (see for
-  example~\cite{BengtsonParow09}). To avoid this, we will allow type
-  specifications for $\mathtt{let}$s as follows
+  where the notation @{text "\<lambda>_ . _"} indicates that the list of @{text
+  "x\<^isub>i"} becomes bound in @{text s}. In this representation the term
+  \mbox{@{text "\<LET> (\<lambda>x . s)  [t\<^isub>1, t\<^isub>2]"}} is a perfectly legal
+  instance, but the lengths of the two lists do not agree. To exclude such
+  terms, additional predicates about well-formed terms are needed in order to
+  ensure that the two lists are of equal length. This can result in very messy
+  reasoning (see for example~\cite{BengtsonParow09}). To avoid this, we will
+  allow type specifications for @{text "\<LET>"}s as follows
   %
   \begin{center}
   \begin{tabular}{r@ {\hspace{2mm}}r@ {\hspace{2mm}}l}
   @{text trm} & @{text "::="}  & @{text "\<dots>"}\\ 
-              & @{text "|"}    & @{text "\<LET> as::assn s::trm"}\hspace{4mm} 
+              & @{text "|"}    & @{text "\<LET>  as::assn  s::trm"}\hspace{4mm} 
                                  \isacommand{bind} @{text "bn(as)"} \isacommand{in} @{text "s"}\\[1mm]
   @{text assn} & @{text "::="} & @{text "\<ANIL>"}\\
-               & @{text "|"}   & @{text "\<ACONS> name trm assn"}
+               & @{text "|"}   & @{text "\<ACONS>  name  trm  assn"}
   \end{tabular}
   \end{center}
 
@@ -234,11 +233,11 @@
   set-theoretic model \cite{Berghofer99}.
 
   Another reason is that we establish the reasoning infrastructure
-  for alpha-\emph{equated} terms. In contrast, Ott produces  a reasoning 
+  for $\alpha$-\emph{equated} terms. In contrast, Ott produces  a reasoning 
   infrastructure in Isabelle/HOL for
-  \emph{non}-alpha-equated, or ``raw'', terms. While our alpha-equated terms
+  \emph{non}-$\alpha$-equated, or ``raw'', terms. While our $\alpha$-equated terms
   and the raw terms produced by Ott use names for bound variables,
-  there is a key difference: working with alpha-equated terms means, for example,  
+  there is a key difference: working with $\alpha$-equated terms means, for example,  
   that the two type-schemes
 
   \begin{center}
@@ -246,26 +245,26 @@
   \end{center}
   
   \noindent
-  are not just alpha-equal, but actually \emph{equal}! As a result, we can
-  only support specifications that make sense on the level of alpha-equated
+  are not just $\alpha$-equal, but actually \emph{equal}! As a result, we can
+  only support specifications that make sense on the level of $\alpha$-equated
   terms (offending specifications, which for example bind a variable according
   to a variable bound somewhere else, are not excluded by Ott, but we have
   to).  
 
-  Our insistence on reasoning with alpha-equated terms comes from the
+  Our insistence on reasoning with $\alpha$-equated terms comes from the
   wealth of experience we gained with the older version of Nominal Isabelle:
-  for non-trivial properties, reasoning with alpha-equated terms is much
+  for non-trivial properties, reasoning with $\alpha$-equated terms is much
   easier than reasoning with raw terms. The fundamental reason for this is
   that the HOL-logic underlying Nominal Isabelle allows us to replace
   ``equals-by-equals''. In contrast, replacing
-  ``alpha-equals-by-alpha-equals'' in a representation based on raw terms
+  ``$\alpha$-equals-by-$\alpha$-equals'' in a representation based on raw terms
   requires a lot of extra reasoning work.
 
-  Although in informal settings a reasoning infrastructure for alpha-equated
+  Although in informal settings a reasoning infrastructure for $\alpha$-equated
   terms is nearly always taken for granted, establishing it automatically in
   the Isabelle/HOL theorem prover is a rather non-trivial task. For every
   specification we will need to construct a type containing as elements the
-  alpha-equated terms. To do so, we use the standard HOL-technique of defining
+  $\alpha$-equated terms. To do so, we use the standard HOL-technique of defining
   a new type by identifying a non-empty subset of an existing type.  The
   construction we perform in Isabelle/HOL can be illustrated by the following picture:
 
@@ -295,16 +294,16 @@
 
   \noindent
   We take as the starting point a definition of raw terms (defined as a
-  datatype in Isabelle/HOL); identify then the alpha-equivalence classes in
-  the type of sets of raw terms according to our alpha-equivalence relation,
-  and finally define the new type as these alpha-equivalence classes
+  datatype in Isabelle/HOL); identify then the $\alpha$-equivalence classes in
+  the type of sets of raw terms according to our $\alpha$-equivalence relation,
+  and finally define the new type as these $\alpha$-equivalence classes
   (non-emptiness is satisfied whenever the raw terms are definable as datatype
-  in Isabelle/HOL and the property that our relation for alpha-equivalence is
+  in Isabelle/HOL and the property that our relation for $\alpha$-equivalence is
   indeed an equivalence relation).
 
   The fact that we obtain an isomorphism between the new type and the
   non-empty subset shows that the new type is a faithful representation of
-  alpha-equated terms. That is not the case for example for terms using the
+  $\alpha$-equated terms. That is not the case for example for terms using the
   locally nameless representation of binders \cite{McKinnaPollack99}: in this
   representation there are ``junk'' terms that need to be excluded by
   reasoning about a well-formedness predicate.
@@ -315,7 +314,7 @@
   task. To ease it, we re-implemented in Isabelle/HOL the quotient package
   described by Homeier \cite{Homeier05} for the HOL4 system. This package
   allows us to lift definitions and theorems involving raw terms to
-  definitions and theorems involving alpha-equated terms. For example if we
+  definitions and theorems involving $\alpha$-equated terms. For example if we
   define the free-variable function over raw lambda-terms
 
   \begin{center}
@@ -326,7 +325,7 @@
   
   \noindent
   then with the help of the quotient package we can obtain a function @{text "fv\<^sup>\<alpha>"}
-  operating on quotients, or alpha-equivalence classes of lambda-terms. This
+  operating on quotients, or $\alpha$-equivalence classes of lambda-terms. This
   lifted function is characterised by the equations
 
   \begin{center}
@@ -338,15 +337,15 @@
   \noindent
   (Note that this means also the term-constructors for variables, applications
   and lambda are lifted to the quotient level.)  This construction, of course,
-  only works if alpha-equivalence is indeed an equivalence relation, and the
-  ``raw'' definitions and theorems are respectful w.r.t.~alpha-equivalence.
+  only works if $\alpha$-equivalence is indeed an equivalence relation, and the
+  ``raw'' definitions and theorems are respectful w.r.t.~$\alpha$-equivalence.
   For example, we will not be able to lift a bound-variable function. Although
   this function can be defined for raw terms, it does not respect
-  alpha-equivalence and therefore cannot be lifted. To sum up, every lifting
+  $\alpha$-equivalence and therefore cannot be lifted. To sum up, every lifting
   of theorems to the quotient level needs proofs of some respectfulness
   properties (see \cite{Homeier05}). In the paper we show that we are able to
   automate these proofs and as a result can automatically establish a reasoning 
-  infrastructure for alpha-equated terms.
+  infrastructure for $\alpha$-equated terms.
 
   The examples we have in mind where our reasoning infrastructure will be
   helpful includes the term language of System @{text "F\<^isub>C"}, also
@@ -359,13 +358,17 @@
   about them in a theorem prover would be a major pain.  \medskip
 
   \noindent
-  {\bf Contributions:}  We provide new definitions for when terms
-  involving multiple binders are alpha-equivalent. These definitions are
+  {\bf Contributions:}  We provide novel definitions for when terms
+  involving general binders are $\alpha$-equivalent. These definitions are
   inspired by earlier work of Pitts \cite{Pitts04}. By means of automatic
-  proofs, we establish a reasoning infrastructure for alpha-equated
+  proofs, we establish a reasoning infrastructure for $\alpha$-equated
   terms, including properties about support, freshness and equality
-  conditions for alpha-equated terms. We are also able to derive strong 
+  conditions for $\alpha$-equated terms. We are also able to derive strong 
   induction principles that have the variable convention already built in.
+  The concepts behind our specifications of general binders are taken 
+  from the Ott-tool, but we introduce restrictions, and also one extension, so 
+  that the specifications make sense for reasoning about $\alpha$-equated terms. 
+
 
   \begin{figure}
   \begin{boxedminipage}{\linewidth}
@@ -472,7 +475,7 @@
   The most original aspect of the nominal logic work of Pitts is a general
   definition for the notion of the ``set of free variables of an object @{text
   "x"}''.  This notion, written @{term "supp x"}, is general in the sense that
-  it applies not only to lambda-terms (alpha-equated or not), but also to lists,
+  it applies not only to lambda-terms ($\alpha$-equated or not), but also to lists,
   products, sets and even functions. The definition depends only on the
   permutation operation and on the notion of equality defined for the type of
   @{text x}, namely:
@@ -504,7 +507,7 @@
 
   While often the support of an object can be relatively easily 
   described, for example for atoms, products, lists, function applications, 
-  booleans and permutations as follows\\[-6mm]
+  booleans and permutations as follows
   %
   \begin{eqnarray}
   @{term "supp a"} & = & @{term "{a}"}\\
@@ -517,7 +520,7 @@
   \end{eqnarray}
   
   \noindent 
-  in some cases it can be difficult to characterise the support precisely, and
+  In some cases it can be difficult to characterise the support precisely, and
   only an approximation can be established (see \eqref{suppfun} above). Reasoning about
   such approximations can be simplified with the notion \emph{supports}, defined 
   as follows:
@@ -532,7 +535,8 @@
   two properties.
 
   \begin{property}\label{supportsprop}
-  {\it i)} @{thm[mode=IfThen] supp_is_subset[no_vars]}\\ 
+  Given a set @{text "as"} of atoms.
+  {\it i)} @{thm[mode=IfThen] supp_is_subset[where S="as", no_vars]}
   {\it ii)} @{thm supp_supports[no_vars]}.
   \end{property}
 
@@ -546,7 +550,7 @@
 
   \noindent or equivalently that a permutation applied to the application
   @{text "f x"} can be moved to the argument @{text x}. That means for equivariant
-  functions @{text f}, we have for all permutations @{text p}
+  functions @{text f}, we have for all permutations @{text p}:
   %
   \begin{equation}\label{equivariance}
   @{text "p \<bullet> f = f"} \;\;\;\textit{if and only if}\;\;\;
@@ -560,13 +564,13 @@
   that
   %
   \begin{center}
-  @{text "x R y"} \;\;implies\;\; @{text "(p \<bullet> x) R (p \<bullet> y)"}
+  @{text "x R y"} \;\;\textit{implies}\;\; @{text "(p \<bullet> x) R (p \<bullet> y)"}
   \end{center}
 
   Finally, the nominal logic work provides us with general means to rename 
   binders. While in the older version of Nominal Isabelle, we used extensively 
   Property~\ref{swapfreshfresh} for renaming single binders, this property 
-  proved unwieldy for dealing with multiple binders. For such binders the 
+  proved too unwieldy for dealing with multiple binders. For such binders the 
   following generalisations turned out to be easier to use.
 
   \begin{property}\label{supppermeq}
@@ -592,7 +596,7 @@
 
   Most properties given in this section are described in detail in \cite{HuffmanUrban10}
   and of course all are formalised in Isabelle/HOL. In the next sections we will make 
-  extensive use of these properties in order to define alpha-equivalence in 
+  extensive use of these properties in order to define $\alpha$-equivalence in 
   the presence of multiple binders.
 *}
 
@@ -607,62 +611,62 @@
 
   In order to keep our work with deriving the reasoning infrastructure
   manageable, we will wherever possible state definitions and perform proofs
-  on the user-level of Isabelle/HOL, as opposed to write custom ML-code that
+  on the ``user-level'' of Isabelle/HOL, as opposed to write custom ML-code that
   generates them anew for each specification. To that end, we will consider
   first pairs @{text "(as, x)"} of type @{text "(atom set) \<times> \<beta>"}.  These pairs
   are intended to represent the abstraction, or binding, of the set of atoms @{text
   "as"} in the body @{text "x"}.
 
   The first question we have to answer is when two pairs @{text "(as, x)"} and
-  @{text "(bs, y)"} are alpha-equivalent? (For the moment we are interested in
-  the notion of alpha-equivalence that is \emph{not} preserved by adding
-  vacuous binders.) To answer this, we identify four conditions: {\it i)}
+  @{text "(bs, y)"} are $\alpha$-equivalent? (For the moment we are interested in
+  the notion of $\alpha$-equivalence that is \emph{not} preserved by adding
+  vacuous binders.) To answer this question, we identify four conditions: {\it (i)}
   given a free-variable function @{text "fv"} of type \mbox{@{text "\<beta> \<Rightarrow> atom
   set"}}, then @{text x} and @{text y} need to have the same set of free
   variables; moreover there must be a permutation @{text p} such that {\it
-  ii)} @{text p} leaves the free variables of @{text x} and @{text y} unchanged, but
-  {\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)}
+  (ii)} @{text p} leaves the free variables of @{text x} and @{text y} unchanged, but
+  {\it (iii)} ``moves'' their bound names so that we obtain modulo a relation,
+  say \mbox{@{text "_ R _"}}, two equivalent terms. We also require that {\it (iv)}
   @{text p} makes the sets of abstracted atoms @{text as} and @{text bs} equal. The
   requirements {\it i)} to {\it iv)} can be stated formally as follows:
   %
   \begin{equation}\label{alphaset}
-  \begin{array}{@ {\hspace{10mm}}r@ {\hspace{2mm}}l}
-  \multicolumn{2}{l}{@{term "(as, x) \<approx>gen R fv p (bs, y)"}\hspace{2mm}@{text "\<equiv>"}\hspace{30mm}}\\[1mm]
-               & @{term "fv(x) - as = fv(y) - bs"}\\
-  @{text "\<and>"} & @{term "(fv(x) - as) \<sharp>* p"}\\
-  @{text "\<and>"} & @{text "(p \<bullet> x) R y"}\\
-  @{text "\<and>"} & @{term "(p \<bullet> as) = bs"}\\ 
+  \begin{array}{@ {\hspace{10mm}}r@ {\hspace{2mm}}l@ {\hspace{4mm}}r}
+  \multicolumn{3}{l}{@{term "(as, x) \<approx>gen R fv p (bs, y)"}\hspace{2mm}@{text "\<equiv>"}}\\[1mm]
+              & @{term "fv(x) - as = fv(y) - bs"} & \mbox{\it (i)}\\
+  @{text "\<and>"} & @{term "(fv(x) - as) \<sharp>* p"} & \mbox{\it (ii)}\\
+  @{text "\<and>"} & @{text "(p \<bullet> x) R y"} & \mbox{\it (iii)}\\
+  @{text "\<and>"} & @{term "(p \<bullet> as) = bs"} & \mbox{\it (iv)}\\ 
   \end{array}
   \end{equation}
 
   \noindent
   Note that this relation depends on the permutation @{text
-  "p"}. Alpha-equivalence between two pairs is then the relation where we
+  "p"}; $\alpha$-equivalence between two pairs is then the relation where we
   existentially quantify over this @{text "p"}. Also note that the relation is
   dependent on a free-variable function @{text "fv"} and a relation @{text
   "R"}. The reason for this extra generality is that we will use
-  $\approx_{\textit{set}}$ for both ``raw'' terms and alpha-equated terms. In
-  the latter case, $R$ will be replaced by equality @{text "="} and we
+  $\approx_{\,\textit{set}}$ for both ``raw'' terms and $\alpha$-equated terms. In
+  the latter case, @{text R} will be replaced by equality @{text "="} and we
   will prove that @{text "fv"} is equal to @{text "supp"}.
 
   The definition in \eqref{alphaset} does not make any distinction between the
-  order of abstracted variables. If we want this, then we can define alpha-equivalence 
+  order of abstracted variables. If we want this, then we can define $\alpha$-equivalence 
   for pairs of the form \mbox{@{text "(as, x)"}} with type @{text "(atom list) \<times> \<beta>"} 
   as follows
   %
   \begin{equation}\label{alphalist}
-  \begin{array}{@ {\hspace{10mm}}r@ {\hspace{2mm}}l}
-  \multicolumn{2}{l}{@{term "(as, x) \<approx>lst R fv p (bs, y)"}\hspace{2mm}@{text "\<equiv>"}\hspace{30mm}}\\[1mm]
-             & @{term "fv(x) - (set as) = fv(y) - (set bs)"}\\
-  \wedge     & @{term "(fv(x) - set as) \<sharp>* p"}\\
-  \wedge     & @{text "(p \<bullet> x) R y"}\\
-  \wedge     & @{term "(p \<bullet> as) = bs"}\\ 
+  \begin{array}{@ {\hspace{10mm}}r@ {\hspace{2mm}}l@ {\hspace{4mm}}r}
+  \multicolumn{2}{l}{@{term "(as, x) \<approx>lst R fv p (bs, y)"}\hspace{2mm}@{text "\<equiv>"}}\\[1mm]
+             & @{term "fv(x) - (set as) = fv(y) - (set bs)"} & \mbox{\it (i)}\\
+  \wedge     & @{term "(fv(x) - set as) \<sharp>* p"} & \mbox{\it (ii)}\\
+  \wedge     & @{text "(p \<bullet> x) R y"} & \mbox{\it (iii)}\\
+  \wedge     & @{term "(p \<bullet> as) = bs"} & \mbox{\it (iv)}\\ 
   \end{array}
   \end{equation}
   
   \noindent
-  where @{term set} is a function that coerces a list of atoms into a set of atoms.
+  where @{term set} is the function that coerces a list of atoms into a set of atoms.
   Now the last clause ensures that the order of the binders matters (since @{text as}
   and @{text bs} are lists of atoms).
 
@@ -671,18 +675,19 @@
   condition in \eqref{alphaset}:
   %
   \begin{equation}\label{alphares}
-  \begin{array}{@ {\hspace{10mm}}r@ {\hspace{2mm}}l}
-  \multicolumn{2}{l}{@{term "(as, x) \<approx>res R fv p (bs, y)"}\hspace{2mm}@{text "\<equiv>"}\hspace{30mm}}\\[1mm]
-             & @{term "fv(x) - as = fv(y) - bs"}\\
-  \wedge     & @{term "(fv(x) - as) \<sharp>* p"}\\
-  \wedge     & @{text "(p \<bullet> x) R y"}\\
+  \begin{array}{@ {\hspace{10mm}}r@ {\hspace{2mm}}l@ {\hspace{4mm}}r}
+  \multicolumn{2}{l}{@{term "(as, x) \<approx>res R fv p (bs, y)"}\hspace{2mm}@{text "\<equiv>"}}\\[1mm]
+             & @{term "fv(x) - as = fv(y) - bs"} & \mbox{\it (i)}\\
+  \wedge     & @{term "(fv(x) - as) \<sharp>* p"} & \mbox{\it (ii)}\\
+  \wedge     & @{text "(p \<bullet> x) R y"} & \mbox{\it (iii)}\\
   \end{array}
   \end{equation}
 
-  It might be useful to consider some examples for 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 define
+  It might be useful to consider first some examples for 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
+  define
 
   \begin{center}
   @{text "fv(x) = {x}"}  \hspace{5mm} @{text "fv(T\<^isub>1 \<rightarrow> T\<^isub>2) = fv(T\<^isub>1) \<union> fv(T\<^isub>2)"}
@@ -691,19 +696,19 @@
   \noindent
   Now recall the examples shown in \eqref{ex1}, \eqref{ex2} and
   \eqref{ex3}. It can be easily checked that @{text "({x, y}, x \<rightarrow> y)"} and
-  @{text "({y, x}, y \<rightarrow> x)"} are alpha-equivalent according to
-  $\approx_{\textit{set}}$ and $\approx_{\textit{res}}$ by taking @{text p} to
+  @{text "({y, x}, y \<rightarrow> x)"} are $\alpha$-equivalent according to
+  $\approx_{\,\textit{set}}$ and $\approx_{\,\textit{res}}$ by taking @{text p} to
   be the swapping @{term "(x \<rightleftharpoons> y)"}. In case of @{text "x \<noteq> y"}, then @{text
-  "([x, y], x \<rightarrow> y)"} $\not\approx_{\textit{list}}$ @{text "([y, x], x \<rightarrow> y)"}
+  "([x, y], x \<rightarrow> y)"} $\not\approx_{\,\textit{list}}$ @{text "([y, x], x \<rightarrow> y)"}
   since there is no permutation that makes the lists @{text "[x, y]"} and
   @{text "[y, x]"} equal, and also leaves the type \mbox{@{text "x \<rightarrow> y"}}
-  unchanged. Another example is @{text "({x}, x)"} $\approx_{\textit{res}}$
+  unchanged. Another example is @{text "({x}, x)"} $\approx_{\,\textit{res}}$
   @{text "({x, y}, x)"} which holds by taking @{text p} to be the identity
   permutation.  However, if @{text "x \<noteq> y"}, then @{text "({x}, x)"}
-  $\not\approx_{\textit{set}}$ @{text "({x, y}, x)"} since there is no
+  $\not\approx_{\,\textit{set}}$ @{text "({x, y}, x)"} since there is no
   permutation that makes the sets @{text "{x}"} and @{text "{x, y}"} equal
-  (similarly for $\approx_{\textit{list}}$).  It can also relatively easily be
-  shown that all three notions of alpha-equivalence coincide, if we only
+  (similarly for $\approx_{\,\textit{list}}$).  It can also relatively easily be
+  shown that all three notions of $\alpha$-equivalence coincide, if we only
   abstract a single atom.
 
   In the rest of this section we are going to introduce three abstraction 
@@ -714,13 +719,13 @@
   \end{equation}
   
   \noindent
-  (similarly for $\approx_{\textit{abs\_res}}$ 
-  and $\approx_{\textit{abs\_list}}$). We can show that these relations are equivalence 
+  (similarly for $\approx_{\,\textit{abs\_res}}$ 
+  and $\approx_{\,\textit{abs\_list}}$). We can show that these relations are equivalence 
   relations and equivariant.
 
   \begin{lemma}\label{alphaeq} 
-  The relations $\approx_{\textit{abs\_set}}$, $\approx_{\textit{abs\_list}}$
-  and $\approx_{\textit{abs\_res}}$ are equivalence relations, and if @{term
+  The relations $\approx_{\,\textit{abs\_set}}$, $\approx_{\,\textit{abs\_list}}$
+  and $\approx_{\,\textit{abs\_res}}$ are equivalence relations, 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{lemma}
@@ -736,7 +741,7 @@
   \noindent
   This lemma allows us to use our quotient package and introduce 
   new types @{text "\<beta> abs_set"}, @{text "\<beta> abs_res"} and @{text "\<beta> abs_list"}
-  representing alpha-equivalence classes of pairs of type 
+  representing $\alpha$-equivalence classes of pairs of type 
   @{text "(atom set) \<times> \<beta>"} (in the first two cases) and of type @{text "(atom list) \<times> \<beta>"}
   (in the third case). 
   The elements in these types will be, respectively, written as:
@@ -783,9 +788,9 @@
 
   \noindent
   The second fact derives from the definition of permutations acting on pairs 
-  \eqref{permute} and alpha-equivalence being equivariant 
+  \eqref{permute} and $\alpha$-equivalence being equivariant 
   (see Lemma~\ref{alphaeq}). With these two facts at our disposal, we can show 
-  the following lemma about swapping two atoms.
+  the following lemma about swapping two atoms in an abstraction.
   
   \begin{lemma}
   @{thm[mode=IfThen] abs_swap1(1)[where bs="as", no_vars]}
@@ -845,7 +850,7 @@
   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 section.
+  the definitions for $\alpha$-equivalence will help us in the next section.
 *}
 
 section {* Alpha-Equivalence and Free Variables\label{sec:alpha} *}
@@ -883,7 +888,7 @@
 
   \noindent
   Every type declaration @{text ty}$^\alpha_{1..n}$ consists of a collection of 
-  term-constructors, each of which come with a list of labelled 
+  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
 
@@ -918,7 +923,7 @@
   The first mode is for binding lists of atoms (the order of binders matters);
   the second is for sets of binders (the order does not matter, but the
   cardinality does) and the last is for sets of binders (with vacuous binders
-  preserving alpha-equivalence). The ``\isacommand{in}-part'' of a binding
+  preserving $\alpha$-equivalence). The ``\isacommand{in}-part'' of a binding
   clause will be called \emph{bodies} (there can be more than one); 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
@@ -926,9 +931,9 @@
 
   \begin{center}
   \begin{tabular}{@ {}ll@ {}}
-  @{text "Foo\<^isub>1 x::name y::name t::lam s::lam"} &  
+  @{text "Foo\<^isub>1 x::name y::name t::trm s::trm"} &  
       \isacommand{bind} @{text "x y"} \isacommand{in} @{text "t s"}\\
-  @{text "Foo\<^isub>2 x::name y::name t::lam s::lam"} &  
+  @{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}
@@ -937,11 +942,15 @@
   \noindent
   Similarly for the other binding modes. Interestingly, in case of \isacommand{bind\_set}
   and \isacommand{bind\_res} the binding clauses above will make a difference to the semantics
-  of the specifications (the corresponding alpha-equivalence will differ). We will 
+  of the specifications (the corresponding $\alpha$-equivalence will differ). We will 
   show this later with an example.
   
-  There are some restrictions we need to impose on binding clasues: First, a
-  body can only occur in \emph{one} binding clause of a term constructor. For
+  There are some restrictions we need to impose on binding clasues: the main idea behind 
+  these restrictions is that we obtain a sensible notion of $\alpha$-equivalence where
+  it is ensured that a bound variable cannot be free at the same time.  First, a
+  body can only occur in \emph{one} binding clause of a term constructor (this ensures
+  that the bound variables of a body cannot be free at the same time by specifying 
+  an alternative binder for the body). For
   binders we distinguish between \emph{shallow} and \emph{deep} binders.
   Shallow binders are just labels. The restriction we need to impose on them
   is that in case of \isacommand{bind\_set} and \isacommand{bind\_res} the
@@ -954,14 +963,14 @@
   \begin{center}
   \begin{tabular}{@ {}cc@ {}}
   \begin{tabular}{@ {}l@ {\hspace{-1mm}}}
-  \isacommand{nominal\_datatype} @{text lam} =\\
+  \isacommand{nominal\_datatype} @{text lam} $=$\\
   \hspace{5mm}\phantom{$\mid$}~@{text "Var name"}\\
   \hspace{5mm}$\mid$~@{text "App lam lam"}\\
   \hspace{5mm}$\mid$~@{text "Lam x::name t::lam"}\\
   \hspace{21mm}\isacommand{bind} @{text x} \isacommand{in} @{text t}\\
   \end{tabular} &
   \begin{tabular}{@ {}l@ {}}
-  \isacommand{nominal\_datatype}~@{text ty} =\\
+  \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"}\\
@@ -971,18 +980,18 @@
   \end{center}
 
   \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. Note also that in
-  these specifications @{text "name"} refers to an atom type, and @{text
-  "fset"} to the type of finite sets.
+  difference to the semantics of the specification (which we will define below).
 
 
   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 corresponding binding functions are
+  \emph{recursive}, see below). The binding functions are
   expected to return either a set of atoms (for \isacommand{bind\_set} and
   \isacommand{bind\_res}) or a list of atoms (for \isacommand{bind}). They can
   be defined by primitive recursion over the corresponding type; the equations
@@ -1008,7 +1017,7 @@
   \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)"}\\ 
+  \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}
   
@@ -1056,38 +1065,42 @@
   The difference is that with @{text Let} we only want to bind the atoms @{text
   "bn(as)"} in the term @{text t}, but with @{text "Let_rec"} we also want to bind the atoms
   inside the assignment. This difference has consequences for the free-variable 
-  function and alpha-equivalence relation, which we are going to define below.
-  For this definition, we have to impose some restrictions on deep binders. First,
+  function and $\alpha$-equivalence relation, which we are going to define below.
+  
+  To make sure that variables bound by deep binders cannot be free at the
+  same time, we have to impose some restrictions. First,
   we cannot have more than one binding function for one binder. So we exclude:
 
   \begin{center}
-  \begin{tabular}{ll}
-  @{text "Baz p::pat t::trm"} & 
+  \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}\\
+  @{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"}\\
   \end{tabular}
   \end{center}
 
   \noindent
-  The reason why we must exclude such specifications is that they cannot be
-  represented by the general binders described in Section~\ref{sec:binders}. 
-
   We also need to restrict the form of the binding functions. As will shortly
   become clear, we cannot return an atom in a binding function that is also
   bound in the corresponding term-constructor. That means in the example
   \eqref{letpat} that the term-constructors @{text PVar} and @{text PTup} may
   not have a binding clause (all arguments are used to define @{text "bn"}).
   In contrast, in case of \eqref{letrecs} the term-constructor @{text ACons}
-  may have binding clause involving the argument @{text t} (the only one that
-  is \emph{not} used in the definition of the binding function).  In the version of
+  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).  
+
+  In the version of
   Nominal Isabelle described here, we also adopted the restriction from the
   Ott-tool that binding functions can only return: the empty set or empty list
   (as in case @{text PNil}), a singleton set or singleton list containing an
   atom (case @{text PVar}), or unions of atom sets or appended atom lists
-  (case @{text PTup}). This restriction will simplify some automatic proofs
+  (case @{text PTup}). This restriction will simplify some automatic definitions and proofs
   later on.
   
   In order to simplify our definitions, we shall assume specifications 
-  of term-calculi are \emph{completed}. By this we mean that  
+  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
@@ -1117,7 +1130,7 @@
   term-constructors so that binders and their bodies are next to each other will 
   result in inadequate representations. Therefore we will first
   extract datatype definitions from the specification and then define 
-  explicitly an alpha-equivalence relation over them.
+  explicitly an $\alpha$-equivalence relation over them.
 
 
   The datatype definition can be obtained by stripping off the 
@@ -1125,7 +1138,7 @@
   new names for the types @{text "ty\<^sup>\<alpha>"} and term-constructors @{text "C\<^sup>\<alpha>"}
   given by the user. In our implementation we just use the affix ``@{text "_raw"}''.
   But for the purpose of this paper, we use the superscript @{text "_\<^sup>\<alpha>"} to indicate 
-  that a notion is defined over alpha-equivalence classes and leave it out 
+  that a notion is defined over $\alpha$-equivalence classes and leave it out 
   for the corresponding notion defined on the ``raw'' level. So for example 
   we have
   
@@ -1150,8 +1163,29 @@
   @{text "p \<bullet> (C z\<^isub>1 \<dots> z\<^isub>n) = C (p \<bullet> z\<^isub>1) \<dots> (p \<bullet> z\<^isub>n)"}
   \end{equation}
   
-  The first non-trivial step we have to perform is the generation of free-variable 
-  functions from the specifications. For atomic types we define the auxilary
+  The first non-trivial step we have to perform is the generation of
+  free-variable functions from the specifications. Given the raw types @{text
+  "ty\<^isub>1 \<dots> ty\<^isub>n"} derived from a specification, we define the
+  free-variable functions
+
+  \begin{center}
+  @{text "fv_ty\<^isub>1, \<dots>, fv_ty\<^isub>n"}
+  \end{center}
+
+  \noindent
+  We define them together with auxiliary free-variable functions for
+  the binding functions. Given raw binding functions @{text "bn\<^isub>1 \<dots> bn\<^isub>m"} we define
+  
+  \begin{center}
+  @{text "fv_bn\<^isub>1, \<dots>, fv_bn\<^isub>m"}
+  \end{center}
+
+  \noindent
+  The reason for this setup is that in a deep binder not all atoms have to be
+  bound, as we saw in the example with ``plain'' @{text Let}s. We need therefore a function
+  that calculates those unbound atoms. 
+
+  For atomic types we define the auxilary
   free variable functions:
 
   \begin{center}
@@ -1167,26 +1201,6 @@
   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}"}.
 
-  Given the raw types @{text "ty\<^isub>1 \<dots> ty\<^isub>n"} we define now the
-  free-variable functions
-
-  \begin{center}
-  @{text "fv_ty\<^isub>1, \<dots>, fv_ty\<^isub>n"}
-  \end{center}
-
-  \noindent
-  We define them together with auxiliary free-variable functions for
-  the binding functions. Given binding functions 
-  @{text "bn\<^isub>1 \<dots> bn\<^isub>m"} we define
-  %
-  \begin{center}
-  @{text "fv_bn\<^isub>1, \<dots>, fv_bn\<^isub>m"}
-  \end{center}
-
-  \noindent
-  The reason for this setup is that in a deep binder not all atoms have to be
-  bound, as we saw in the example with ``plain'' @{text Let}s. We need therefore a function
-  that calculates those unbound atoms. 
 
   While the idea behind these free-variable functions is clear (they just
   collect all atoms that are not bound), because of our rather complicated
@@ -1247,7 +1261,7 @@
   The reason why we only have to treat the empty binding clauses specially in
   the definition of @{text "fv_bn"} is that binding functions can only use arguments
   that do not occur in binding clauses. Otherwise the @{text "bn"} function cannot
-  be lifted to alpha-equated terms.
+  be lifted to $\alpha$-equated terms.
 
 
   To see how these definitions work in practice, let us reconsider the term-constructors 
@@ -1288,7 +1302,7 @@
   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
+  not respect $\alpha$-equivalence. We can also see that
   %
   \begin{equation}\label{bnprop}
   @{text "fv_ty x  =  bn x \<union> fv_bn x"}.
@@ -1297,9 +1311,9 @@
   \noindent
   holds for any @{text "bn"}-function defined for the type @{text "ty"}.
 
-  Next we define alpha-equivalence relations for the types @{text "ty\<^isub>1, \<dots>, ty\<^isub>n"}. We call them
+  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. 
+  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.
@@ -1312,7 +1326,7 @@
   \end{center}
 
 
-  The relations for alpha-equivalence are inductively defined predicates, whose clauses have
+  The relations for $\alpha$-equivalence are inductively defined predicates, whose clauses have
   conclusions of the form  
   %
   \begin{center}
@@ -1375,7 +1389,7 @@
 
 
 
-  The alpha-equivalence relations @{text "\<approx>bn\<^isub>j"} for binding functions 
+  The $\alpha$-equivalence relations @{text "\<approx>bn\<^isub>j"} for binding functions 
   are similar. We again have conclusions of the form \mbox{@{text "C x\<^isub>1 \<dots> x\<^isub>n \<approx>bn C y\<^isub>1 \<dots> y\<^isub>n"}}
   and need to generate appropriate premises. We generate first premises according to the first three
   rules given above. Only the ``left-over'' pairs  @{text "(x\<^isub>i, y\<^isub>i)"} need to be treated 
@@ -1427,7 +1441,7 @@
 
   \noindent
   Note the difference between  $\approx_{\textit{assn}}$ and
-  $\approx_{\textit{bn}}$: the latter only ``tracks'' alpha-equivalence of 
+  $\approx_{\textit{bn}}$: the latter only ``tracks'' $\alpha$-equivalence of 
   the components in an assignment that are \emph{not} bound. Therefore we have
   a $\approx_{\textit{bn}}$-premise in the clause for @{text "Let"} (which is 
   a non-recursive binder). The underlying reason is that the terms inside an assignment are not meant 
@@ -1439,10 +1453,10 @@
 
 text {*
   Having made all necessary definitions for raw terms, we can start
-  introducing the reasoning infrastructure for the alpha-equated types the
+  introducing the reasoning infrastructure for the $\alpha$-equated types the
   user originally specified. We sketch in this section the facts we need for establishing
   this reasoning infrastructure. First we have to show that the
-  alpha-equivalence relations defined in the previous section are indeed
+  $\alpha$-equivalence relations defined in the previous section are indeed
   equivalence relations.
 
   \begin{lemma}\label{equiv} 
@@ -1460,7 +1474,7 @@
 
   \noindent 
   We can feed this lemma into our quotient package and obtain new types @{text
-  "ty\<AL>\<^bsub>1..n\<^esub>"} representing alpha-equated terms of types @{text "ty\<^bsub>1..n\<^esub>"}. We also obtain 
+  "ty\<AL>\<^bsub>1..n\<^esub>"} representing $\alpha$-equated terms of types @{text "ty\<^bsub>1..n\<^esub>"}. We also obtain 
   definitions for the term-constructors @{text
   "C"}$^\alpha_{1..m}$ from the raw term-constructors @{text
   "C"}$_{1..m}$, and similar definitions for the free-variable functions @{text
@@ -1479,7 +1493,7 @@
   \end{equation}
   
   \noindent
-  By definition of alpha-equivalence we can show that
+  By definition of $\alpha$-equivalence we can show that
   for the raw term-constructors
   %
   \begin{equation}\label{distinctraw}
@@ -1489,7 +1503,7 @@
   \noindent
   In order to generate \eqref{distinctalpha} from \eqref{distinctraw}, the quotient
   package needs to know that the term-constructors @{text "C\<^isub>i"} and @{text "C\<^isub>j"} 
-  are \emph{respectful} w.r.t.~the alpha-equivalence relations (see \cite{Homeier05}).
+  are \emph{respectful} w.r.t.~the $\alpha$-equivalence relations (see \cite{Homeier05}).
   Assuming @{text "C\<^isub>i"} is of type @{text "ty"} with argument types
   @{text "ty\<^isub>1, \<dots>, ty\<^isub>n"}, then respectfulness amounts to showing that
   
@@ -1498,7 +1512,7 @@
   \end{center}  
 
   \noindent
-  are alpha-equivalent under the assumption that @{text "x\<^isub>i \<approx>ty\<^isub>i y\<^isub>i"} holds for all recursive arguments
+  are $\alpha$-equivalent under the assumption that @{text "x\<^isub>i \<approx>ty\<^isub>i y\<^isub>i"} holds for all recursive arguments
   and  @{text "x\<^isub>i = y\<^isub>i"} holds for all non-recursive arguments of @{text "C\<^isub>i"}. We can prove this by 
   analysing the definition of @{text "\<approx>ty"}. For this proof to succeed we have to establish 
   the following auxiliary fact about binding functions. Given a binding function @{text bn\<^isub>i} defined 
@@ -1513,7 +1527,7 @@
    
   Having established respectfulness for every raw term-constructor, the 
   quotient package is able to automatically deduce \eqref{distinctalpha} from \eqref{distinctraw}.
-  In fact we can from now on lift facts from the raw level to the alpha-equated level
+  In fact we can from now on lift facts from the raw level to the $\alpha$-equated level
   as long as they contain raw term-constructors only. The 
   induction principles derived by the datatype package in Isabelle/HOL for the types @{text
   "ty\<^bsub>1..n\<^esub>"} fall into this category. So we can also add to our infrastructure
@@ -1540,8 +1554,8 @@
   to the term-constructors, also permutation operations. In order to make the 
   lifting go through, 
   we have to know that the permutation operations are respectful 
-  w.r.t.~alpha-equivalence. This amounts to showing that the 
-  alpha-equivalence relations are equivariant, which we already established 
+  w.r.t.~$\alpha$-equivalence. This amounts to showing that the 
+  $\alpha$-equivalence relations are equivariant, which we already established 
   in Lemma~\ref{equiv}. As a result we can establish the equations
   
   \begin{equation}\label{calphaeqvt}
@@ -1580,8 +1594,8 @@
   \end{center}
 
   \noindent
-  are alpha-equivalent. This gives us conditions when the corresponding
-  alpha-equated terms are \emph{equal}, namely
+  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>n = C\<^sup>\<alpha> y\<^isub>1 \<dots> y\<^isub>n"}
@@ -1592,7 +1606,7 @@
   we have to lift in the next section, we completed
   the lifting part of establishing the reasoning infrastructure. 
 
-  By working now completely on the alpha-equated level, we can first show that 
+  By working now completely on the $\alpha$-equated level, we can first show that 
   the free-variable functions and binding functions
   are equivariant, namely
 
@@ -1609,7 +1623,7 @@
   (using the induction principles we lifted above for the types @{text "ty\<AL>\<^bsub>1..n\<^esub>"}).
 
   Until now we have not yet derived anything about the support of the 
-  alpha-equated terms. This however will be necessary in order to derive
+  $\alpha$-equated terms. This however will be necessary in order to derive
   the strong induction principles in the next section.
   Using the equivariance properties in \eqref{ceqvt} we can
   show for every term-constructor @{text "C\<^sup>\<alpha>"} that 
@@ -1727,7 +1741,7 @@
 
 text {*
   In the previous section we were able to provide induction principles that 
-  allow us to perform structural inductions over alpha-equated terms. 
+  allow us to perform structural inductions over $\alpha$-equated terms. 
   We call such induction principles \emph{weak}, because in case of a term-constructor @{text "C\<^sup>\<alpha> x\<^isub>1 \<dots> x\<^isub>n"},
   the induction hypothesis requires us to establish the implication
   %
@@ -1772,7 +1786,7 @@
   
   \noindent
   Using again the quotient package  we can lift the @{text "_ \<bullet>\<^bsub>bn\<^esub> _"} function to 
-  alpha-equated terms. We can then prove the following two facts
+  $\alpha$-equated terms. We can then prove the following two facts
 
   \begin{lemma}\label{permutebn} 
   Given a binding function @{text "bn\<^sup>\<alpha>"} then for all @{text p}
@@ -1951,36 +1965,50 @@
   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
+  $\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 also no concrete mathematical result concerning this
-  notion of alpha-equivalence.  A definition for the notion of free variables
+  notion of $\alpha$-equivalence.  A definition for the notion of free variables
   in a term are work in progress in Ott.
 
   Although we were heavily inspired by their syntax,
-  their definition of alpha-equivalence is unsuitable for our extension of
+  their definition of $\alpha$-equivalence 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
+  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 their 
   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 
+  for our notion of $\alpha$-equivalence in case of \isacommand{bind\_set} and 
   \isacommand{bind\_res}. This makes 
 
   \begin{center}
-  \begin{tabular}{@ {}ll@ {}}
-  @{text "Foo\<^isub>1 xs::name fset x::name y::name"} &  
-      \isacommand{bind\_set} @{text "xs"} \isacommand{in} @{text "x y"}\\
-  @{text "Foo\<^isub>2 xs::name fset x::name y::name"} &  
-      \isacommand{bind\_set} @{text "xs"} \isacommand{in} @{text "x"}, 
-      \isacommand{bind\_set} @{text "xs"} \isacommand{in} @{text "y"}\\
+  \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"}\\
+  @{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"}\\
   \end{tabular}
   \end{center}
 
   \noindent
-  behave differently. To see this, consider the following equations 
+  behave differently. In the first term-constructor, we essentially have a single
+  body, which happens to be ``spread'' over two arguments; in the second 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}
+
+  To see this, consider the following equations 
 
   \begin{center}
   \begin{tabular}{c}
@@ -2016,14 +2044,14 @@
   inter-translated, but we have not proved this. However, we believe the
   binding specifications in the style of Ott are a more natural way for 
   representing terms involving bindings. Pottier gives a definition for 
-  alpha-equivalence, which is similar to our binding mode \isacommand{bind}. 
+  $\alpha$-equivalence, which is similar to our binding mode \isacommand{bind}. 
   Although he uses also a permutation in case of abstractions, his
   definition is rather different from ours. He proves that his notion
-  of alpha-equivalence is indeed a equivalence relation, but a complete
+  of $\alpha$-equivalence is indeed a equivalence relation, but a complete
   reasoning infrastructure is well beyond the purposes of his language. 
   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\_res}.
+  $\alpha$-equivalence related to our binding mode \isacommand{bind\_res}.
   This 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 they can handle vacous binders. However, their notion of
@@ -2049,7 +2077,7 @@
   {http://isabelle.in.tum.de/nominal/download}.
 
   We have left out a discussion about how functions can be defined over
-  alpha-equated terms that involve general binders. In earlier versions of Nominal
+  $\alpha$-equated terms that involve general binders. In earlier versions of Nominal
   Isabelle \cite{UrbanBerghofer06} this turned out to be a thorny issue.  We
   hope to do better this time by using the function package that has recently
   been implemented in Isabelle/HOL and also by restricting function
@@ -2092,6 +2120,9 @@
   also for patiently explaining some of the finer points of the work on the Ott-tool. We
   also thank Stephanie Weirich for suggesting to separate the subgrammars
   of kinds and types in our Core-Haskell example.  
+
+
+  * Conference of Altenkirch *
 *}
 
 (*<*)




