
diff -r 186d8486dfd5 -r 23480003f9c5 Paper/Paper.thy
--- a/Paper/Paper.thy	Mon Apr 26 13:08:14 2010 +0200
+++ b/Paper/Paper.thy	Mon Apr 26 20:17:41 2010 +0200
@@ -363,7 +363,7 @@
   inspired by earlier work of Pitts \cite{Pitts04}. By means of automatic
   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, at the moment 
+  conditions for alpha-equated terms. We are also able to derive, for the moment 
   only manually, strong induction principles that 
   have the variable convention already built in.
 
@@ -490,7 +490,7 @@
   \end{center}
 
   \noindent
-  We also use for sets of atoms the abbreviation 
+  We use for sets of atoms the abbreviation 
   @{thm (lhs) fresh_star_def[no_vars]}, defined as 
   @{thm (rhs) fresh_star_def[no_vars]}.
   A striking consequence of these definitions is that we can prove
@@ -682,7 +682,7 @@
   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 equality and for @{text "fv(T)"} we define
+  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)"}
@@ -764,13 +764,14 @@
   \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. The elements in these types 
-  will be, respectively, written as:
+  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>"}. 
+  The elements in these types will be, respectively, written as:
 
   \begin{center}
   @{term "Abs as x"} \hspace{5mm} 
-  @{term "Abs_lst as x"} \hspace{5mm}
-  @{term "Abs_res as x"}
+  @{term "Abs_res as x"} \hspace{5mm}
+  @{term "Abs_lst as x"} 
   \end{center}
 
   \noindent
@@ -784,8 +785,8 @@
   \begin{center}
   \begin{tabular}{l@ {\hspace{2mm}}c@ {\hspace{2mm}}l}
   @{thm (lhs) supp_abs(1)[no_vars]} & $=$ & @{thm (rhs) supp_abs(1)[no_vars]}\\
-  @{thm (lhs) supp_abs(3)[where bs="as", no_vars]} & $=$ & @{thm (rhs) supp_abs(3)[where bs="as", no_vars]}\\
-  @{thm (lhs) supp_abs(2)[no_vars]} & $=$ & @{thm (rhs) supp_abs(2)[no_vars]}
+  @{thm (lhs) supp_abs(2)[no_vars]} & $=$ & @{thm (rhs) supp_abs(2)[no_vars]}\\
+  @{thm (lhs) supp_abs(3)[where bs="as", no_vars]} & $=$ & @{thm (rhs) supp_abs(3)[where bs="as", no_vars]}
   \end{tabular}
   \end{center}
   \end{thm}
@@ -851,7 +852,7 @@
   \end{center}
 
   \noindent
-  using \eqref{suppfun}. Assuming @{term "supp x - as"} is a finite set
+  using \eqref{suppfun}. Assuming @{term "supp x - as"} is a finite set,
   we further obtain
   %
   \begin{equation}\label{halftwo}
@@ -897,7 +898,7 @@
   binding \mbox{function part} &
   $\begin{cases}
   \mbox{\begin{tabular}{l}
-  \isacommand{with} @{text "bn\<AL>\<^isub>1"} \isacommand{and} \ldots \isacommand{and} @{text "bn\<AL>\<^isub>m"}\\
+  \isacommand{binder} @{text "bn\<AL>\<^isub>1"} \isacommand{and} \ldots \isacommand{and} @{text "bn\<AL>\<^isub>m"}\\
   \isacommand{where}\\
   $\ldots$\\
   \end{tabular}}
@@ -943,8 +944,10 @@
   the second is for sets of binders (the order does not matter, but the
   cardinality does) and the last is for sets of binders (with vacuous binders
   preserving alpha-equivalence). The ``\isacommand{in}-part'' of a binding
-  clause will be called \emph{body}; the ``\isacommand{bind}-part'' will
-  be called \emph{binder}.
+  clause will be called \emph{bodies} (there can be more than one); the 
+  ``\isacommand{bind}-part'' will be called \emph{binders}. A body can only occur 
+  in \emph{one} binding clause. A binder, in contrast, may occur in several binding 
+  clauses, but cannot occur as a body.
 
   In addition we distinguish between \emph{shallow} and \emph{deep}
   binders.  Shallow binders are of the form \isacommand{bind}\; {\it labels}\;
@@ -976,22 +979,16 @@
 
   \noindent
   Note that in this specification \emph{name} refers to an atom type.
-  If we have shallow binders that ``share'' a body, for instance $t$ in
-  the following term-constructor
+  Shallow binders may also ``share'' several bodies, for instance @{text t} 
+  and @{text s} in the following term-constructor
 
   \begin{center}
   \begin{tabular}{ll}
-  @{text "Foo x::name y::name t::lam"} &  
-      \isacommand{bind} @{text x} \isacommand{in} @{text t},\;
-      \isacommand{bind} @{text y} \isacommand{in} @{text t}  
+  @{text "Foo x::name y::name t::lam s::lam"} &  
+      \isacommand{bind} @{text "x y"} \isacommand{in} @{text "t s"}  
   \end{tabular}
   \end{center}
 
-  \noindent
-  then we have to make sure the modes of the binders agree. We cannot
-  have, for instance, in the first binding clause the mode \isacommand{bind} 
-  and in the second \isacommand{bind\_set}.
-
   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
@@ -1017,7 +1014,7 @@
   \hspace{5mm}\phantom{$\mid$}~@{text PNil}\\
   \hspace{5mm}$\mid$~@{text "PVar name"}\\
   \hspace{5mm}$\mid$~@{text "PTup pat pat"}\\ 
-  \isacommand{with}~@{text "bn::pat \<Rightarrow> atom list"}\\
+  \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)"}\\ 
@@ -1046,18 +1043,16 @@
 
   \begin{center}
   \begin{tabular}{ll}
-  @{text "Foo p::pat q::pat t::trm"} & 
-     \isacommand{bind} @{text "bn(p)"} \isacommand{in} @{text t},\;
-     \isacommand{bind} @{text "bn(q)"} \isacommand{in} @{text t}\\
-  @{text "Foo' x::name p::pat t::trm"} & 
-     \isacommand{bind} @{text x} \isacommand{in} @{text t},\;
-     \isacommand{bind} @{text "bn(p)"} \isacommand{in} @{text t} 
+  @{text "Foo\<^isub>1 p::pat q::pat t::trm"} & 
+     \isacommand{bind} @{text "bn(p) bn(q)"} \isacommand{in} @{text t}\\
+  @{text "Foo\<^isub>2 x::name p::pat t::trm"} & 
+     \isacommand{bind} @{text "x bn(p)"} \isacommand{in} @{text t}\\ 
   \end{tabular}
   \end{center}
 
   \noindent
-  In the first case we might bind all atoms from the pattern @{text p} in @{text t}
-  and also all atoms from @{text q} in @{text t}. As a result we have no way
+  In the first case the intention is to bind all atoms from the pattern @{text p} in @{text t}
+  and also all atoms from @{text q} in @{text t}. Unfortunately, we have no way
   to determine whether the binder came from the binding function @{text
   "bn(p)"} or @{text "bn(q)"}. Similarly in the second case. The reason why
   we must exclude such specifications is that they cannot be represent by
@@ -1066,19 +1061,17 @@
 
   \begin{center}
   \begin{tabular}{ll}
-  @{text "Bar p::pat t::trm s::trm"} & 
-     \isacommand{bind} @{text "bn(p)"} \isacommand{in} @{text t},\;
-     \isacommand{bind} @{text "bn(p)"} \isacommand{in} @{text s}\\
-  @{text "Bar' p::pat t::trm"} &  
-     \isacommand{bind} @{text "bn(p)"} \isacommand{in} @{text p},\;
-     \isacommand{bind} @{text "bn(p)"} \isacommand{in} @{text t}\\
+  @{text "Bar\<^isub>1 p::pat t::trm s::trm"} & 
+     \isacommand{bind} @{text "bn(p)"} \isacommand{in} @{text "t s"}\\
+  @{text "Bar\<^isub>2 p::pat t::trm"} &  
+     \isacommand{bind} @{text "bn(p)"} \isacommand{in} @{text "p t"}\\
   \end{tabular}
   \end{center}
 
   \noindent
   since there is no overlap of binders.
   
-  Note that in the last example we wrote {\it\isacommand{bind}\;bn(p)\;\isacommand{in}\;p}.
+  Note that in the last example we wrote \isacommand{bind}~@{text "bn(p)"}~\isacommand{in}~@{text "p.."}.
   Whenever such a binding clause is present, we will call the corresponding binder \emph{recursive}.
   To see the purpose of such recursive binders, compare ``plain'' @{text "Let"}s and @{text "Let_rec"}s
   in the following specification:
@@ -1090,13 +1083,12 @@
   \hspace{5mm}\phantom{$\mid$}\ldots\\
   \hspace{5mm}$\mid$~@{text "Let as::assn t::trm"} 
      \;\;\isacommand{bind} @{text "bn(as)"} \isacommand{in} @{text t}\\
-  \hspace{5mm}$\mid$~@{text "Let_rec as::assn t::trm"}\\ 
-  \hspace{20mm}\isacommand{bind} @{text "bn(as)"} \isacommand{in} @{text t},
-         \isacommand{bind} @{text "bn(as)"} \isacommand{in} @{text as}\\
-  \isacommand{and} {\it assn} =\\
+  \hspace{5mm}$\mid$~@{text "Let_rec as::assn t::trm"}
+     \;\;\isacommand{bind} @{text "bn(as)"} \isacommand{in} @{text "as t"}\\
+  \isacommand{and} @{text "ass"} =\\
   \hspace{5mm}\phantom{$\mid$}~@{text "ANil"}\\
   \hspace{5mm}$\mid$~@{text "ACons name trm assn"}\\
-  \isacommand{with} @{text "bn::assn \<Rightarrow> atom list"}\\
+  \isacommand{binder} @{text "bn::assn \<Rightarrow> atom list"}\\
   \isacommand{where}~@{text "bn(ANil) = []"}\\
   \hspace{5mm}$\mid$~@{text "bn(ACons a t as) = [atom a] @ bn(as)"}\\
   \end{tabular}}
@@ -1109,14 +1101,39 @@
   function and alpha-equivalence relation, which we are going to describe in the 
   rest of this section.
  
+  In order to simplify matters below, we shall assume specifications 
+  of term-calculi are \emph{completed}. By this we mean that  
+  for every argument of a term-constructor that is \emph{not} 
+  already part of a binding clause, we add implicitly a special \emph{empty} binding
+  clause, written \isacommand{bind}~@{term "{}"}~\isacommand{in}~@{text "\<dots>"}. In case
+  of the lambda-calculus, the comletion is as follows:
+
+  \begin{center}
+  \begin{tabular}{@ {}l@ {\hspace{-1mm}}}
+  \isacommand{nominal\_datatype} @{text lam} =\\
+  \hspace{5mm}\phantom{$\mid$}~@{text "Var x::name"}
+    \;\;\isacommand{bind}~@{term "{}"}~\isacommand{in}~@{text "x"}\\
+  \hspace{5mm}$\mid$~@{text "App t\<^isub>1::lam t\<^isub>2::lam"}
+    \;\;\isacommand{bind}~@{term "{}"}~\isacommand{in}~@{text "t\<^isub>1"},
+        \isacommand{bind}~@{term "{}"}~\isacommand{in}~@{text "t\<^isub>2"}\\
+  \hspace{5mm}$\mid$~@{text "Lam x::name t::lam"}
+    \;\;\isacommand{bind}~@{text x} \isacommand{in} @{text t}\\
+  \end{tabular}
+  \end{center}
+
+  \noindent 
+  The point of completion is that we can make definitions over the binding
+  clauses, which defined purely over arguments, turned out to be unwieldy.
+
   Having dealt with all syntax matters, the problem now is how we can turn
   specifications into actual type definitions in Isabelle/HOL and then
   establish a reasoning infrastructure for them. As
-  Pottier and Cheney pointed out \cite{Pottier06,Cheney5}, we cannot in general 
-  re-arrange arguments of
+  Pottier and Cheney pointed out \cite{Pottier06,Cheney05}, by just 
+  re-arranging the arguments of
   term-constructors so that binders and their bodies are next to each other, and
-  then use the type constructors @{text "abs_set"}, @{text "abs_res"} and
-  @{text "abs_list"} from Section \ref{sec:binders}. Therefore we will first
+  then use directly the type constructors @{text "abs_set"}, @{text "abs_res"} and
+  @{text "abs_list"} from Section \ref{sec:binders}, will result in an inadequate
+  representatation. Therefore we will first
   extract datatype definitions from the specification and then define 
   expicitly an alpha-equivalence relation over them.
 
@@ -1152,8 +1169,24 @@
   \end{equation}
   
   The first non-trivial step we have to perform is the generation free-variable 
-  functions from the specifications. Given the raw types @{text "ty\<^isub>1 \<dots> ty\<^isub>n"}
-  we need to define free-variable functions
+  functions from the specifications. For atomic types we define the auxilary
+  free variable functions:
+
+  \begin{center}
+  \begin{tabular}{r@ {\hspace{2mm}}c@ {\hspace{2mm}}l}
+  @{text "fv_atom a"} & @{text "="} & @{text "atom a"}\\
+  @{text "fv_atom_set as"} & @{text "="} & @{text "atoms as"}\\
+  @{text "fv_atom_list as"} & @{text "="} & @{text "atoms (set as)"}\\
+  \end{tabular}
+  \end{center}
+
+  \noindent 
+  Like the coercion function @{text atom} used earlier, @{text "atoms"} coerces 
+  the set of atoms to a set of the generic atom type.
+  It is defined as @{text "atoms as \<equiv> {atom a | a \<in> as}"}.
+
+  Given the raw types @{text "ty\<^isub>1 \<dots> ty\<^isub>n"}
+  we define now free-variable functions
 
   \begin{center}
   @{text "fv_ty\<^isub>1, \<dots>, fv_ty\<^isub>n"}
@@ -1173,92 +1206,65 @@
   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 binding mechanisms their definitions are
-  somewhat involved.
-  Given a term-constructor @{text "C"} of type @{text ty} with argument types
-  \mbox{@{text "ty\<^isub>1 \<dots> ty\<^isub>n"}}, the function
-  @{text "fv_ty (C x\<^isub>1 \<dots> x\<^isub>n)"} will be the union of the values, @{text v},
-  calculated below for each argument. 
-  First we deal with the case that @{text "x\<^isub>i"} is a binder. From the binding clauses, 
-  we can determine whether the argument is a shallow or deep
-  binder, and in the latter case also whether it is a recursive or
-  non-recursive binder. 
-  %
+  While the idea behind these free-variable functions is clear (they just
+  collect all atoms that are not bound), because of our rather complicated
+  binding mechanisms their definitions are somewhat involved.  Given a
+  term-constructor @{text "C"} of type @{text ty} and some associated binding
+  clauses, the function @{text "fv_ty (C x\<^isub>1 \<dots> x\<^isub>n)"} will be
+  the union of the values, @{text v}, calculated below for each binding
+  clause. 
+
   \begin{equation}\label{deepbinder}
   \mbox{%
   \begin{tabular}{c@ {\hspace{2mm}}p{7cm}}
-  $\bullet$ & @{term "v = {}"} provided @{text "x\<^isub>i"} is a shallow binder\\
-  $\bullet$ & @{text "v = fv_bn x\<^isub>i"} provided @{text "x\<^isub>i"} is a deep
-      non-recursive binder with the auxiliary binding function @{text "bn"}\\
-  $\bullet$ & @{text "v = fv_ty\<^isub>i x\<^isub>i - bn x\<^isub>i"} provided @{text "x\<^isub>i"} is
-      a deep recursive binder with the auxiliary binding function @{text "bn"}
+  \multicolumn{2}{@ {}l}{Empty binding clauses of the form 
+  \isacommand{bind\_set}~@{term "{}"}~\isacommand{in}~@{text "y"}:}\\ 
+  $\bullet$ & @{term "v = fv_ty y"} provided @{text "y"} is of type @{text "ty"}\smallskip\\
+  \multicolumn{2}{@ {}l}{Shallow binders of the form 
+  \isacommand{bind\_set}~@{text "x\<^isub>1\<dots>x\<^isub>n"}~\isacommand{in}~@{text "y\<^isub>1\<dots>y\<^isub>m"}:}\\ 
+  $\bullet$ & @{text "v = (fv_ty\<^isub>1 y\<^isub>1 \<union> fv_ty\<^isub>m y\<^isub>m) - (x\<^isub>1 \<union> \<dots> \<union> x\<^isub>n)"} 
+     provided the @{text "y\<^isub>i"} are of type @{text "ty\<^isub>i"}\smallskip\\
+  \multicolumn{2}{@ {}l}{Deep binders of the form 
+  \isacommand{bind\_set}~@{text "bn x"}~\isacommand{in}~@{text "y\<^isub>1\<dots>y\<^isub>m"}:}\\ 
+  $\bullet$ & @{text "v = (fv_ty\<^isub>1 y\<^isub>1 \<union> fv_ty\<^isub>m y\<^isub>m) - (bn x) \<union> (fv_bn x)"}\\
+  $\bullet$ & @{text "v = (fv_ty\<^isub>1 y\<^isub>1 \<union> fv_ty\<^isub>m y\<^isub>m) - (bn x)"}\\
+     & provided the @{text "y\<^isub>i"} are of type @{text "ty\<^isub>i"}; the first 
+    clause applies for @{text x} being a non-recursive deep binder, the 
+    second for a recursive deep binder
   \end{tabular}}
   \end{equation}
 
   \noindent
-  The first clause states that shallow binders do not contribute to the
-  free variables; in the second clause, we have to collect all
-  variables that are left unbound by the binding function @{text "bn"}---this
-  is done with function @{text "fv_bn"}; in the third clause, since the 
-  binder is recursive, we need to bind all variables specified by 
-  @{text "bn"}---therefore we subtract @{text "bn x\<^isub>i"} from the free
-  variables of @{text "x\<^isub>i"}.
+  Similarly for the other binding modes. Note that in a non-recursive deep
+  binder, we have to add all atoms that are left unbound by the binding
+  function @{text "bn"}. For this we use the function @{text "fv_bn"}. Assume
+  for the constructor @{text "C"} the binding function equation is of the form @{text
+  "bn\<^isub>j (C x\<^isub>1 \<dots> x\<^isub>n) = rhs"}. We again define a value
+  @{text v} which is exactly as in \eqref{deepbinder} for shallow and deep
+  binders. We only modify the clause for empty binding clauses as follows:
 
-  In case the argument is \emph{not} a binder, we need to consider 
-  whether the @{text "x\<^isub>i"} is the body of one or more binding clauses. 
-  In this case we first calculate the set @{text "bnds"} as follows: 
-  either the corresponding binders are all shallow or there is a single deep binder.
-  In the former case we take @{text bnds} to be the union of all shallow 
-  binders; in the latter case, we just take the set of atoms specified by the 
-  corresponding binding function. The value for @{text "x\<^isub>i"} is then given by:
-  %
-  \begin{equation}\label{deepbody}
+
+  \begin{equation}\label{bnemptybinder}
   \mbox{%
   \begin{tabular}{c@ {\hspace{2mm}}p{7cm}}
-  $\bullet$ & @{text "v = {atom x\<^isub>i} - bnds"} provided @{term "x\<^isub>i"} is an atom\\
-  $\bullet$ & @{text "v = (atoms x\<^isub>i) - bnds"} provided @{term "x\<^isub>i"} is a set of atoms\\
-  $\bullet$ & @{text "v = (atoms (set x\<^isub>i)) - bnds"} provided @{term "x\<^isub>i"} is a list of atoms\\
-  $\bullet$ & @{text "v = (fv_ty\<^isub>i x\<^isub>i) - bnds"} provided @{term "ty\<^isub>i"} is one of the raw datatypes
-     corresponding to the types specified by the user\\
-%  $\bullet$ & @{text "(fv\<^isup>\<alpha> x\<^isub>i) - bnds"} provided @{term "x\<^isub>i"} is a defined nominal datatype
-%     with a free-variable function @{text "fv\<^isup>\<alpha>"}\\
-  $\bullet$ & @{term "v = {}"} otherwise
+  \multicolumn{2}{@ {}l}{Empty binding clauses of the form 
+  \isacommand{bind\_set}~@{term "{}"}~\isacommand{in}~@{text "y"}:}\\ 
+  $\bullet$ & @{term "v = fv_ty\<^isub>i y"} provided @{text "y"} does not occur in @{text "rhs"}
+  and the free-variable function for the type of @{text "y"} is @{text "fv_ty\<^isub>i"}\\
+  $\bullet$ & @{term "v = fv_bn\<^isub>i y"} provided @{text "y"} occurs in  @{text "rhs"}
+  with a recursive call @{text "bn\<^isub>i y"}\\
+  $\bullet$ & @{term "v = {}"} provided @{text "y"} occurs in  @{text "rhs"},
+  but without a recursive call\\
   \end{tabular}}
   \end{equation}
 
-  \noindent 
-  Like the coercion function @{text atom} used earlier, @{text "atoms"} coerces 
-  the set of atoms to a set of the generic atom type.
-  It is defined as @{text "atoms as \<equiv> {atom a | a \<in> as}"}.
-
-  The last case we need to consider is when @{text "x\<^isub>i"} is neither
-  a binder nor a body of an abstraction. In this case it is defined 
-  as in \eqref{deepbody}, except that we do not need to subtract the 
-  set @{text bnds}.
+  \noindent
+  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.
 
-  The definitions of the free-variable functions for binding
-  functions are similar. For each binding function
-  @{text "bn\<^isub>j"} we need to define a free-variable function
-  @{text "fv_bn\<^isub>j"}. Given a term-constructor @{term "C"}, the
-  function @{text "fv_bn\<^isub>j(C x\<^isub>1 \<dots> x\<^isub>n)"} is the union of the
-  values calculated for the arguments. For each argument @{term "x\<^isub>i"}
-  we know whether it appears in the @{term "rhs"} of the binding
-  function equation @{text "bn\<^isub>j (C x\<^isub>1 \<dots> x\<^isub>n) = rhs"}. If it does not
-  appear in @{text "rhs"} we generate the premise according to the
-  rules for @{text "fv_ty"} described above in (\ref{deepbinder}--\ref{deepbody}). Otherwise:
 
-  \begin{center}
-  \begin{tabular}{c@ {\hspace{2mm}}p{7cm}}
-   $\bullet$ & @{text "v = fv_bn x\<^isub>i"} provided @{text "rhs"} contains the
-    recursive call @{text "bn x\<^isub>i"}\medskip\\
-  $\bullet$ & @{term "v = {}"} provided @{text "rhs"} contains
-    @{term "x\<^isub>i"} and @{term "x\<^isub>i"} is of atom type.
-  \end{tabular}
-  \end{center}
-
-  \noindent
   To see how these definitions work in practice, let us reconsider the term-constructors 
   @{text "Let"} and @{text "Let_rec"} from the example shown in \eqref{letrecs}. 
   For this specification we need to define three free-variable functions, namely
@@ -1266,20 +1272,19 @@
   %
   \begin{center}
   \begin{tabular}{@ {}l@ {\hspace{1mm}}c@ {\hspace{1mm}}l@ {}}
-  @{text "fv\<^bsub>trm\<^esub> (Let as t)"} & @{text "="} & @{text "fv\<^bsub>bn\<^esub> as \<union> (fv\<^bsub>trm\<^esub> t - set (bn as))"}\\
-  @{text "fv\<^bsub>trm\<^esub> (Let_rec as t)"} & @{text "="} &\\
-  \multicolumn{3}{r}{@{text "(fv\<^bsub>assn\<^esub> as - set (bn as)) \<union> (fv\<^bsub>trm\<^esub> t - set (bn as))"}}\\[1mm]
+  @{text "fv\<^bsub>trm\<^esub> (Let as t)"} & @{text "="} & @{text "(fv\<^bsub>trm\<^esub> t - set (bn as)) \<union> fv\<^bsub>bn\<^esub> as"}\\
+  @{text "fv\<^bsub>trm\<^esub> (Let_rec as t)"} & @{text "="} & @{text "(fv\<^bsub>assn\<^esub> as \<union> fv\<^bsub>trm\<^esub> t) - set (bn as)"}\\[1mm]
 
-  @{text "fv\<^bsub>assn\<^esub> (ANil)"} & @{text "="} & @{text "[]"}\\
+  @{text "fv\<^bsub>assn\<^esub> (ANil)"} & @{text "="} & @{term "{}"}\\
   @{text "fv\<^bsub>assn\<^esub> (ACons a t as)"} & @{text "="} & @{text "{atom a} \<union> (fv\<^bsub>trm\<^esub> t) \<union> (fv\<^bsub>assn\<^esub> as)"}\\[1mm]
 
-  @{text "fv\<^bsub>bn\<^esub> (ANil)"} & @{text "="} & @{text "[]"}\\
+  @{text "fv\<^bsub>bn\<^esub> (ANil)"} & @{text "="} & @{term "{}"}\\
   @{text "fv\<^bsub>bn\<^esub> (ACons a t as)"} & @{text "="} & @{text "(fv\<^bsub>trm\<^esub> t) \<union> (fv\<^bsub>bn\<^esub> as)"}
   \end{tabular}
   \end{center}
 
   \noindent
-  Since there are no binding clauses for the term-constructors @{text ANil}
+  Since there are only (implicit) empty binding clauses for the term-constructors @{text ANil}
   and @{text "ACons"}, the corresponding free-variable function @{text
   "fv\<^bsub>assn\<^esub>"} returns all atoms occuring in an assignment. The
   binding only takes place in @{text Let} and @{text "Let_rec"}. In the @{text
@@ -1290,12 +1295,15 @@
   "fv\<^bsub>bn\<^esub>"} is.  In contrast, in @{text "Let_rec"} we have a
   recursive binder where we want to also bind all occurrences of the atoms
   in @{text "set (bn as)"} inside @{text "as"}. Therefore we have to subtract @{text
-  "set (bn as)"} from @{text "fv\<^bsub>assn\<^esub> as"}, as well as from
-  @{text "fv\<^bsub>trm\<^esub> t"}. An interesting point in this example is
+  "set (bn as)"} from @{text "fv\<^bsub>trm\<^esub> t"}, as well as from
+  @{text "fv\<^bsub>assn\<^esub> as"}. An interesting point in this example is
   that an assignment ``alone'' does not have any bound variables. Only in the
   context of a @{text Let} or @{text "Let_rec"} will some atoms become bound.  
   This is a phenomenon 
-  that has also been pointed out in \cite{ott-jfp}. We can also see that
+  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
   %
   \begin{equation}\label{bnprop}
   @{text "fv_ty x  =  bn x \<union> fv_bn x"}.
@@ -1307,7 +1315,7 @@
   Next we define alpha-equivalence relations for the types @{text "ty\<^isub>1, \<dots>, ty\<^isub>n"}. We call them
   @{text "\<approx>ty\<^isub>1, \<dots>, \<approx>ty\<^isub>n"}. Like with the free-variable functions, 
   we also need to  define auxiliary alpha-equivalence relations for the binding functions. 
-  Say we have @{text "bn\<^isub>1, \<dots>, bn\<^isub>m"}, then we also define @{text "\<approx>bn\<^isub>1, \<dots>, \<approx>bn\<^isub>m"}.
+  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.
   %
@@ -1327,12 +1335,9 @@
   \end{center}
 
   \noindent
-  For what follows, let us assume 
-  @{text C} is of type @{text ty} and its arguments are given by @{text "C ty\<^isub>1 \<dots> ty\<^isub>n"}.
-  The task is to specify what the premises of these clauses are. For this we
-  consider the pairs \mbox{@{text "(x\<^isub>i, y\<^isub>i)"}}, but instead of considering them in turn, it will 
-  be easier to analyse these pairs according to  ``clusters'' of the binding clauses. 
-  Therefore we distinguish the following cases:
+  For what follows, let us assume @{text C} is of type @{text ty}.  The task
+  is to specify what the premises of these clauses are. Again for this we
+  analyse the binding clauses and produce a corresponding premise.
 *}
 (*<*)
 consts alpha_ty ::'a
@@ -1348,59 +1353,42 @@
   fv_trm2 ("fv\<^bsub>assn\<^esub> \<oplus> fv\<^bsub>trm\<^esub>") 
 (*>*)
 text {*
-  \begin{itemize}
-  \item The @{text "(x\<^isub>i, y\<^isub>i)"} is a body of shallow binder with type @{text "ty"}. We assume the 
-  \mbox{@{text "(u\<^isub>1, v\<^isub>1),\<dots>,(u\<^isub>m, v\<^isub>m)"}} are the corresponding binders. For the binding mode
-  \isacommand{bind\_set} we generate the premise
+  \begin{equation}\label{alpha}
+  \mbox{%
+  \begin{tabular}{c@ {\hspace{2mm}}p{7cm}}
+  \multicolumn{2}{@ {}l}{Empty binding clauses of the form 
+  \isacommand{bind\_set}~@{term "{}"}~\isacommand{in}~@{text "x\<^isub>i"}:}\\ 
+  $\bullet$ & @{text "x\<^isub>i \<approx>ty y\<^isub>i"} provided @{text "x\<^isub>i"} and @{text "y\<^isub>i"} 
+  are recursive arguments of @{text "C"}\\
+  $\bullet$ & @{term "x\<^isub>i = y\<^isub>i"} provided @{text "x\<^isub>i"} and @{text "y\<^isub>i"} are 
+  non-recursive arguments\smallskip\\
+  \multicolumn{2}{@ {}l}{Shallow binders of the form 
+  \isacommand{bind\_set}~@{text "x\<^isub>1\<dots>x\<^isub>n"}~\isacommand{in}~@{text "x'\<^isub>1\<dots>x'\<^isub>m"}:}\\ 
+  $\bullet$ & Assume the bodies @{text "x'\<^isub>1\<dots>x'\<^isub>m"} are of type @{text "ty\<^isub>1\<dots>ty\<^isub>m"},
+  @{text "R"} is @{text "\<approx>ty\<^isub>1 \<otimes> ... \<otimes> \<approx>ty\<^isub>m"} and @{text fv} is
+  @{text "fv_ty\<^isub>1 \<oplus> ... \<oplus> fv_ty\<^isub>m"}, then
   \begin{center}
-   @{term "\<exists>p. (u\<^isub>1 \<union> \<xi> \<union> u\<^isub>m, x\<^isub>i) \<approx>gen alpha_ty fv_ty p (v\<^isub>1 \<union> \<xi> \<union> v\<^isub>m, y\<^isub>i)"}
-  \end{center}
-
-  For the binding mode \isacommand{bind}, we use $\approx_{\textit{list}}$, and for
-  binding mode \isacommand{bind\_res} we use $\approx_{\textit{res}}$ instead. 
-
-  \item The @{text "(x\<^isub>i, y\<^isub>i)"} is a deep non-recursive binder with type @{text "ty"}
-  and @{text bn} is corresponding the binding function. We assume 
-  @{text "(u\<^isub>1, v\<^isub>1),\<dots>,(u\<^isub>m, v\<^isub>m)"} are the corresponding bodies with types @{text "ty\<^isub>1,\<dots>, ty\<^isub>m"}. 
-  For the binding mode \isacommand{bind\_set} we generate two premises
-  %
+  @{term "\<exists>p. (x\<^isub>1 \<union> \<xi> \<union> x\<^isub>n, (x'\<^isub>1,\<xi>,x'\<^isub>m)) \<approx>gen R fv p (y\<^isub>1 \<union> \<xi> \<union> y\<^isub>n, (y'\<^isub>1,\<xi>,y'\<^isub>m))"}
+  \end{center}\\
+  \multicolumn{2}{@ {}l}{Deep binders of the form 
+  \isacommand{bind\_set}~@{text "bn x"}~\isacommand{in}~@{text "x'\<^isub>1\<dots>x'\<^isub>m"}:}\\ 
+  $\bullet$ & Assume the bodies @{text "x'\<^isub>1\<dots>x'\<^isub>m"} are of type @{text "ty\<^isub>1\<dots>ty\<^isub>m"},
+  @{text "R"} is @{text "\<approx>ty\<^isub>1 \<otimes> ... \<otimes> \<approx>ty\<^isub>m"} and @{text fv} is
+  @{text "fv_ty\<^isub>1 \<oplus> ... \<oplus> fv_ty\<^isub>m"}, then for recursive deep binders
   \begin{center}
-   @{text "x\<^isub>i \<approx>bn y\<^isub>i"}\hfill
-   @{term "\<exists>p. (bn x\<^isub>i, (u\<^isub>1,\<xi>,u\<^isub>m)) \<approx>gen R fv p (bn y\<^isub>i, (v\<^isub>1,\<xi>,v\<^isub>m))"}
-  \end{center}
+  @{term "\<exists>p. (bn x, (x'\<^isub>1,\<xi>,x'\<^isub>m)) \<approx>gen R fv p (bn y, (y'\<^isub>1,\<xi>,y'\<^isub>m))"}
+  \end{center}\\
+  $\bullet$ & for non-recursive binders we generate in addition @{text "x \<approx>bn y"}\\
+  \end{tabular}}
+  \end{equation}
 
   \noindent
-  where @{text R} is @{text "\<approx>ty\<^isub>1 \<otimes> ... \<otimes> \<approx>ty\<^isub>m"} and @{text fv} is
-  @{text "fv_ty\<^isub>1 \<oplus> ... \<oplus> fv_ty\<^isub>m"}. Similarly for the other binding modes.
-
-  \item The @{text "(x\<^isub>i, y\<^isub>i)"} is a deep recursive binders with type @{text "ty"}
-  and  @{text bn} is the corresponding binding function. We assume 
-  @{text "(u\<^isub>1, v\<^isub>1),\<dots>,(u\<^isub>m, v\<^isub>m)"} are the corresponding bodies with types @{text "ty\<^isub>1,\<dots>, ty\<^isub>m"}. 
-  For the binding mode \isacommand{bind\_set} we generate the premise
-  %
-  \begin{center}
-  @{term "\<exists>p. (bn x\<^isub>i, (x\<^isub>i, u\<^isub>1,\<xi>,u\<^isub>m)) \<approx>gen R fv p (bn y\<^isub>i, (y\<^isub>i, v\<^isub>1,\<xi>,v\<^isub>m))"}
-  \end{center}
-
-  \noindent
-  where @{text R} is @{text "\<approx>ty \<otimes> \<approx>ty\<^isub>1 \<otimes> ... \<otimes> \<approx>ty\<^isub>m"} and @{text fv} is
-  @{text "fv_ty \<oplus> fv_ty\<^isub>1 \<oplus> ... \<oplus> fv_ty\<^isub>m"}. Similarly for the other modes.
-  \end{itemize}
-
-  \noindent
-  From this definition it is clear why we can only support one binding mode per binder
-  and body, as we cannot mix the relations $\approx_{\textit{set}}$, $\approx_{\textit{list}}$
-  and $\approx_{\textit{res}}$. It is also clear why we have to impose the restriction
-  of excluding overlapping binders, as these would need to be translated into separate
+  Similarly for the other binding modes.
+  From this definition it is clear why we have to impose the restriction
+  of excluding overlapping deep binders, as these would need to be translated into separate
   abstractions.
 
 
-  The only cases that are not covered by the rules above are the cases where @{text "(x\<^isub>i, y\<^isub>i)"} is
-  neither a binder nor a body in a binding clause. Then we just generate @{text "x\<^isub>i \<approx>ty y\<^isub>i"}  provided
-  the type of @{text "x\<^isub>i"} and @{text "y\<^isub>i"} is @{text ty} and the arguments are 
-  recursive arguments of the term-constructor. If they are non-recursive arguments,
-  then we generate the premise @{text "x\<^isub>i = y\<^isub>i"}.
-
 
   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"}}




