diff -r 799769b40f0e -r 014f0ea2381c LMCS-Paper/Paper.thy
--- a/LMCS-Paper/Paper.thy	Thu Sep 15 01:01:43 2011 +0200
+++ b/LMCS-Paper/Paper.thy	Fri Sep 16 08:00:15 2011 +0200
@@ -874,7 +874,7 @@
   
   \begin{proof}
   If @{term "a = b"} the lemma is immediate, since @{term "(a \<rightleftharpoons> b) = 0"}.
-  Also in the other case, it is straightforward using \eqref{abseqiff} and
+  Also in the other case it is straightforward using \eqref{abseqiff} and
   observing that the assumptions give us @{term "(a \<rightleftharpoons> b) \<bullet> (supp x - as) =
   (supp x - as)"}.  We therefore can use as permutation the swapping @{term
   "(a \<rightleftharpoons> b)"}.
@@ -1039,7 +1039,7 @@
   
   There are also some restrictions we need to impose on our binding clauses in
   comparison to the ones of Ott. The main idea behind these restrictions is
-  that we obtain a sensible notion of alpha-equivalence where it is ensured
+  that we obtain a notion of alpha-equivalence where it is ensured
   that within a given scope an atom occurrence cannot be both bound and free
   at the same time.  The first restriction is that a body can only occur in
   \emph{one} binding clause of a term constructor. So for example
@@ -1215,15 +1215,16 @@
 
   \noindent
   In this example the term constructor @{text "ACons'"} has four arguments with
-  a binding clause for two of them. This constructor is also used in the definition
+  a binding clause involving two of them. 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
+  binding function can only return free atoms, that is the ones that are \emph{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.
+  terms. If we would permit @{text "bn"} to return @{text "y"},
+  then it would not be respectful and therefore cannot be lifted to
+  alpha-equated lambda-terms.
 
   In the version of Nominal Isabelle described here, we also adopted the
   restriction from the Ott-tool that binding functions can only return: the
@@ -1281,7 +1282,8 @@
   for the corresponding notion given on the ``raw'' level. So for example 
   we have @{text "ty\<^sup>\<alpha> \<mapsto> ty"} and @{text "C\<^sup>\<alpha> \<mapsto> C"}
   where @{term ty} is the type used in the quotient construction for 
-  @{text "ty\<^sup>\<alpha>"} and @{text "C"} is the term-constructor on the ``raw'' type @{text "ty"}. 
+  @{text "ty\<^sup>\<alpha>"} and @{text "C"} is the term-constructor in the ``raw'' type @{text "ty"},
+  respectively @{text "C\<^sup>\<alpha>"} is the corresponding term-constructor in @{text "ty\<^sup>\<alpha>"}. 
 
   The resulting datatype definition is legal in Isabelle/HOL provided the datatypes are 
   non-empty and the types in the constructors only occur in positive 
@@ -1323,7 +1325,7 @@
   
   \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
+  bound, as we saw in \eqref{letrecs} with the example of ``plain'' @{text Let}s. We need
   therefore functions that calculate those free atoms in deep binders.
 
   While the idea behind these free-atom functions is simple (they just
@@ -1687,7 +1689,7 @@
   Again let us take a look at a concrete example for these definitions. For 
   the specification given in \eqref{letrecs}
   we have three relations $\approx_{\textit{trm}}$, $\approx_{\textit{assn}}$ and
-  $\approx_{\textit{bn}}$ with the following clauses:
+  $\approx_{\textit{bn}}$ with the following rules:
 
   \begin{equation}\label{rawalpha}\mbox{
   \begin{tabular}{@ {}c @ {}}
@@ -1723,10 +1725,11 @@
   The underlying reason is that the terms inside an assignment are not meant 
   to be ``under'' the binder. Such a premise is \emph{not} needed in @{text "Let_rec"}, 
   because there all components of an assignment are ``under'' the binder. 
-  Note also that in case of more than one body (e.g.~in the @{text "Let_rec"}-case)
+  Note also that in case of more than one body (that is in the @{text "Let_rec"}-case)
   we need to parametrise the relation $\approx_{\textit{list}}$ with a compound
   equivalence relation and a compound free-atom function. This is because the
-  corresponding binding clause specifies a binder with two bodies.
+  corresponding binding clause specifies a binder with two bodies, namely
+  @{text "as"} and @{text "t"}.
 *}
 
 section {* Establishing the Reasoning Infrastructure *}
@@ -1768,7 +1771,7 @@
   \end{lem}
 
   \begin{proof} 
-  The proof is by induction over the definitions. The non-trivial
+  The proofs are by induction. 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}. However, the transitivity
@@ -1843,11 +1846,30 @@
   "bn"}$_{1..m}$ so that they return bound atoms and in this case the third
   implication is \emph{not} true. A result is that in general the lifting of the
   corresponding binding functions in Ott to alpha-equated terms is impossible.
-
   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 
-  also lift properties that characterise when two ``raw'' terms of the form
+  \eqref{distinctraw}.
+
+  Next we can lift the permutation operations defined in \eqref{ceqvt}. In
+  order to make this lifting to go through, we have to show that the
+  permutation operations are respectful. This amounts to showing that the
+  alpha-equivalence relations are equivariant, which
+  we already established in Lemma~\ref{equiv}. As a result we can add the
+  equations
+  
+  \begin{equation}\label{calphaeqvt}
+  @{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
+  of the free-atom functions @{text "fa_ty\<AL>"}$_{1..n}$ and
+  @{text "fa_bn\<AL>"}$_{1..m}$ as well as of the binding functions @{text
+  "bn\<AL>"}$_{1..m}$ and size functions @{text "size_ty\<AL>"}$_{1..n}$.
+  The latter are defined automatically for the ``raw'' types @{text "ty"}$_{1..n}$
+  by the datatype package of Isabelle/HOL.
+
+  We also need to lift the properties that characterise when two ``raw'' terms of the form
   
   \[
   \mbox{@{text "C x\<^isub>1 \<dots> x\<^isub>r \<approx>ty C x\<PRIME>\<^isub>1 \<dots> x\<PRIME>\<^isub>r"}}
@@ -1862,11 +1884,13 @@
   \]\smallskip
   
   \noindent
-  We call these conditions as \emph{quasi-injectivity}. They correspond to
-  the premises in our alpha-equiva\-lence relations, with the exception that 
-  in case of binders the relations @{text "\<approx>ty"}$_{1..n}$ are all replaced
-  by equality. Recall the alpha-equivalence rules for @{text "Let"} and @{text "Let_rec"} 
-  shown in \eqref{rawalpha}. For @{text "Let\<^sup>\<alpha>"} and @{text "Let_rec\<^sup>\<alpha>"} we have
+  We call these conditions as \emph{quasi-injectivity}. They correspond to the
+  premises in our alpha-equiva\-lence relations, with the exception that the
+  relations @{text "\<approx>ty"}$_{1..n}$ are all replaced by equality (and similarly
+  the free-atom and binding functions are replaced by their lifted
+  counterparts). Recall the alpha-equivalence rules for @{text "Let"} and
+  @{text "Let_rec"} shown in \eqref{rawalpha}. For @{text "Let\<^sup>\<alpha>"} and
+  @{text "Let_rec\<^sup>\<alpha>"} we have
 
   \begin{equation}\label{alphalift}\mbox{
   \begin{tabular}{@ {}c @ {}}
@@ -1879,30 +1903,7 @@
   \end{tabular}}
   \end{equation}\smallskip
 
-  \noindent
-  where @{text "\<approx>\<^bsub>trm\<^esub>"} and @{text "\<approx>\<^bsub>assn\<^esub>"} are replaced by @{text "="} (and similarly 
-  the free-atom and binding functions are replaced by their lifted counterparts). 
-
-  Next we can lift the permutation operations defined in \eqref{ceqvt}. In
-  order to make this lifting to go through, we have to show that the
-  permutation operations are respectful. This amounts to showing that the
-  alpha-equivalence relations are equivariant, which
-  we already established in Lemma~\ref{equiv}. As a result we can add the
-  equations
-  
-  \begin{equation}\label{calphaeqvt}
-  @{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
-  of the free-atom functions @{text "fn_ty\<AL>"}$_{1..n}$ and
-  @{text "fa_bn\<AL>"}$_{1..m}$ as well as of the binding functions @{text
-  "bn\<AL>"}$_{1..m}$ and size functions @{text "size_ty\<AL>"}$_{1..n}$.
-  The latter are defined automatically for the ``raw'' types @{text "ty"}$_{1..n}$
-  by the datatype package of Isabelle/HOL.
-
-  Finally we can add to our infrastructure cases lemmas and a (mutual)
+  We can also add to our infrastructure cases lemmas and a (mutual)
   induction principle for the types @{text "ty\<AL>"}$_{1..n}$. The cases
   lemmas allow the user to deduce a property @{text "P"} by exhaustively
   analysing how an element in a type, say @{text "ty\<AL>"}$_i$, can be
@@ -1938,7 +1939,7 @@
   whereby the @{text P}$_{1..n}$ are the properties established by the induction
   and the @{text y}$_{1..n}$ are of type @{text "ty\<AL>"}$_{1..n}$. Note that 
   the induction principle has for the term constructors @{text "C"}$^\alpha_1$ a
-  premise of the form
+  hypothesis of the form
 
   \[
   \mbox{@{text "\<forall>x\<^isub>1\<dots>x\<^isub>k. P\<^isub>i x\<^isub>i \<and> \<dots> \<and> P\<^isub>j x\<^isub>j \<Rightarrow> P (C\<AL>\<^sub>1 x\<^isub>1 \<dots> x\<^isub>k)"}} 
@@ -1956,18 +1957,18 @@
   on the right):
 
   \begin{equation}\label{inductex}\mbox{
-  \begin{tabular}{c@ {\hspace{10mm}}c}
+  \begin{tabular}{@ {}c@ {\hspace{3mm}}c@ {}}
   \begin{tabular}{@ {}c@ {}}
   \infer{@{text "P\<^bsub>trm\<^esub>"}}
-  {\begin{array}{l}
+  {\begin{array}{@ {}l@ {}}
    @{text "\<forall>x. y = Var\<^sup>\<alpha> x \<Rightarrow> P\<^bsub>trm\<^esub>"}\\
    @{text "\<forall>x\<^isub>1 x\<^isub>2. y = App\<^sup>\<alpha> x\<^isub>1 x\<^isub>2 \<Rightarrow> P\<^bsub>trm\<^esub>"}\\
    @{text "\<forall>x\<^isub>1 x\<^isub>2. y = Lam\<^sup>\<alpha> x\<^isub>1 x\<^isub>2 \<Rightarrow> P\<^bsub>trm\<^esub>"}\\
-   @{text "\<forall>x\<^isub>1 x\<^isub>2. y = Let\<^sup>\<alpha> x\<^isub>1 x\<^isub>2 \<Rightarrow> P\<^bsub>trm\<^esub>"}
+   @{text "\<forall>x\<^isub>1 x\<^isub>2 x\<^isub>3. y = Let\<^sup>\<alpha> x\<^isub>1 x\<^isub>2 x\<^isub>3 \<Rightarrow> P\<^bsub>trm\<^esub>"}
    \end{array}}\medskip\\
 
   \infer{@{text "P\<^bsub>pat\<^esub>"}}
-  {\begin{array}{l}
+  {\begin{array}{@ {}l@ {}}
    @{text "y = PNil\<^sup>\<alpha>  \<Rightarrow> P\<^bsub>pat\<^esub>"}\\
    @{text "\<forall>x. y = PVar\<^sup>\<alpha> x \<Rightarrow> P\<^bsub>pat\<^esub>"}\\
    @{text "\<forall>x\<^isub>1 x\<^isub>2. y = PTup\<^sup>\<alpha> x\<^isub>1 x\<^isub>2 \<Rightarrow> P\<^bsub>pat\<^esub>"}
@@ -1977,11 +1978,11 @@
   
   \begin{tabular}{@ {}c@ {}}
   \infer{@{text "P\<^bsub>trm\<^esub> y\<^isub>1 \<and> P\<^bsub>pat\<^esub> y\<^isub>2"}}
-  {\begin{array}{l}
+  {\begin{array}{@ {}l@ {}}
    @{text "\<forall>x. P\<^bsub>trm\<^esub> (Var\<^sup>\<alpha> x)"}\\
    @{text "\<forall>x\<^isub>1 x\<^isub>2. P\<^bsub>trm\<^esub> x\<^isub>1 \<and> P\<^bsub>trm\<^esub> x\<^isub>2 \<Rightarrow> P\<^bsub>trm\<^esub> (App\<^sup>\<alpha> x\<^isub>1 x\<^isub>2)"}\\
    @{text "\<forall>x\<^isub>1 x\<^isub>2. P\<^bsub>trm\<^esub> x\<^isub>2 \<Rightarrow> P\<^bsub>trm\<^esub> (Lam\<^sup>\<alpha> x\<^isub>1 x\<^isub>2)"}\\
-   @{text "\<forall>x\<^isub>1 x\<^isub>2. P\<^bsub>pat\<^esub> x\<^isub>1 \<and> P\<^bsub>trm\<^esub> x\<^isub>2 \<Rightarrow> P\<^bsub>trm\<^esub> (Let\<^sup>\<alpha> x\<^isub>1 x\<^isub>2)"}\\
+   @{text "\<forall>x\<^isub>1 x\<^isub>2 x\<^isub>3. P\<^bsub>pat\<^esub> x\<^isub>1 \<and> P\<^bsub>trm\<^esub> x\<^isub>2 \<and> P\<^bsub>trm\<^esub> x\<^isub>3 \<Rightarrow> P\<^bsub>trm\<^esub> (Let\<^sup>\<alpha> x\<^isub>1 x\<^isub>2 x\<^isub>3)"}\\
    @{text "P\<^bsub>pat\<^esub> (PNil\<^sup>\<alpha>)"}\\
    @{text "\<forall>x. P\<^bsub>pat\<^esub> (PVar\<^sup>\<alpha> x)"}\\
    @{text "\<forall>x\<^isub>1 x\<^isub>2. P\<^bsub>pat\<^esub> x\<^isub>1 \<and> P\<^bsub>pat\<^esub> x\<^isub>2 \<Rightarrow> P\<^bsub>pat\<^esub> (PTup\<^sup>\<alpha> x\<^isub>1 x\<^isub>2)"}
@@ -2022,13 +2023,13 @@
   in terms of support and freshness, but also provides evidence that our
   notions of free-atoms and alpha-equivalence ``match up''.
 
-  \begin{thm} 
+  \begin{thm}\label{suppfa} 
   For @{text "x"}$_{1..n}$ with type @{text "ty\<AL>"}$_{1..n}$, we have
   @{text "supp x\<^isub>i = fa_ty\<AL>\<^isub>i x\<^isub>i"}.
   \end{thm}
 
   \begin{proof}
-  The proof is by induction. In each case
+  The proof is by induction on @{text "x"}$_{1..n}$. In each case
   we unfold the definition of @{text "supp"}, move the swapping inside the 
   term-constructors and then use the quasi-injectivity lemmas in order to complete the
   proof. For the abstraction cases we use then the facts derived in Theorem~\ref{suppabs},
@@ -2052,9 +2053,11 @@
   \]\smallskip
 
   \noindent
-  Taking the fact into account that @{term "equ2"} and @{term "supp2"} are
-  by definition equal to @{term "equal"} and @{term "supp"}, respectively, 
-  the above rules simplify even further to
+  Taking the fact into account that the compound equivalence relation @{term
+  "equ2"} and the compound free-atom function @{term "supp2"} are by
+  definition equal to @{term "equal"} and @{term "supp"}, respectively, the
+  above rules simplify even further to
+
 
   \[\mbox{
   \begin{tabular}{@ {}c @ {}}
@@ -2068,10 +2071,11 @@
   \]\smallskip
 
   \noindent
-  which means we can characterise equality between term-constructors in terms
-  of equality between the abstractions defined in Section~\ref{sec:binders}. From this
-  we can derive the support for @{text "Let\<^sup>\<alpha>"} and 
-  @{text "Let_rec\<^sup>\<alpha>"}, namely
+  which means we can characterise equality between term-constructors (on the
+  alpha-equated level) in terms of equality between the abstractions defined
+  in Section~\ref{sec:binders}. From this we can deduce the support for @{text
+  "Let\<^sup>\<alpha>"} and @{text "Let_rec\<^sup>\<alpha>"}, namely
+
 
   \[\mbox{
   \begin{tabular}{l@ {\hspace{2mm}}l@ {\hspace{2mm}}l}
@@ -2096,32 +2100,31 @@
 
 text {*
   In the previous section we derived induction principles for alpha-equated
-  terms (see \eqref{induct} and \eqref{inductex}). This was done by lifting
-  the corresponding inductions principles for ``raw'' terms.  We already
-  employed these induction principles in order to derive several facts for
-  alpha-equated terms, including the property that the free-variable functions
-  and the notion of support coincide. Still, we call these induction
-  principles \emph{weak}, because for a term-constructor, say \mbox{@{text
-  "C\<^sup>\<alpha> x\<^isub>1\<dots>x\<^isub>r"}}, the induction hypothesis requires us to
-  establish (under some assumptions) a property @{text "P (C\<^sup>\<alpha>
-  x\<^isub>1\<dots>x\<^isub>r)"} for \emph{all} @{text "x"}$_{1..r}$. The problem is that in the
-  presence of binders we cannot make any assumptions about the atoms that are
-  bound, and we have to potentially rename them. This renaming has to be
-  done manually and is often very cumbersome (especially in the case for 
+  terms (see \eqref{induct} for the general form and \eqref{inductex} for an
+  instance). This was done by lifting the corresponding inductions principles
+  for ``raw'' terms.  We already employed these induction principles for
+  deriving several facts for alpha-equated terms, including the property that
+  the free-variable functions and the notion of support coincide. Still, we
+  call these induction principles \emph{weak}, because for a term-constructor,
+  say \mbox{@{text "C\<^sup>\<alpha> x\<^isub>1\<dots>x\<^isub>r"}}, the induction
+  hypothesis requires us to establish (under some assumptions) a property
+  @{text "P (C\<^sup>\<alpha> x\<^isub>1\<dots>x\<^isub>r)"} for \emph{all} @{text
+  "x"}$_{1..r}$. The problem is that in the presence of binders we cannot make
+  any assumptions about the atoms that are bound. One obvious way around this
+  problem is to rename them. Unfortunately, this leads to very clunky proofs
+  and makes formalisations grievous experiences (especially in the case for
   multiple bound atoms).
 
+
   For the older versions of Nominal Isabelle we introduced in
   \cite{UrbanTasson05} a method for automatically strengthening weak induction
-  principles in case of single binders. These stronger induction principles
-  allow the user to make additional assumptions about bound atoms. The main
-  point is that these additional assumptions amount to a formal version of the
-  informal variable convention for binders and nearly always make manual
-  renaming of binders unnecessary.
-
-  To explain how the strengthening works in the presence of multiple binders,
-  we use as running example the lambda-calculus with @{text "Let"}-patterns
-  shown in \eqref{letpat}. Its weak induction principle is given in \eqref{inductex}.
-  The stronger induction principle is as follows
+  principles. These stronger induction principles allow the user to make
+  additional assumptions about bound atoms. The advantage of these assumptions
+  is that they make in most cases any renaming of bound atoms unnecessary.  To
+  explain how the strengthening works in the presence of multiple binders, we
+  use as running example the lambda-calculus with @{text "Let"}-patterns shown
+  in \eqref{letpat}. Its weak induction principle is given in
+  \eqref{inductex}.  The stronger induction principle is as follows:
 
   \begin{equation}\label{stronginduct}
   \mbox{
@@ -2130,8 +2133,9 @@
   {\begin{array}{l}
    @{text "\<forall>x c. P\<^bsub>trm\<^esub> c (Var\<^sup>\<alpha> x)"}\\
    @{text "\<forall>x\<^isub>1 x\<^isub>2 c. (\<forall>d. P\<^bsub>trm\<^esub> d x\<^isub>1) \<and> (\<forall>d. P\<^bsub>trm\<^esub> d x\<^isub>2) \<Rightarrow> P\<^bsub>trm\<^esub> c (App\<^sup>\<alpha> x\<^isub>1 x\<^isub>2)"}\\
-   @{text "\<forall>x\<^isub>1 x\<^isub>2 c. {atom x\<^isub>1} #\<^sup>* c \<and> (\<forall>d. P\<^bsub>trm\<^esub> d x\<^isub>2) \<Rightarrow> P\<^bsub>trm\<^esub> c (Lam\<^sup>\<alpha> x\<^isub>1 x\<^isub>2)"}\\
-   @{text "\<forall>x\<^isub>1 x\<^isub>2 c. (set (bn\<^sup>\<alpha> x\<^isub>1)) #\<^sup>* c \<and> (\<forall>d. P\<^bsub>pat\<^esub> d x\<^isub>1) \<and> (\<forall>d. P\<^bsub>trm\<^esub> d x\<^isub>2) \<Rightarrow> P\<^bsub>trm\<^esub> c (Let\<^sup>\<alpha> x\<^isub>1 x\<^isub>2)"}\\
+   @{text "\<forall>x\<^isub>1 x\<^isub>2 c. atom x\<^isub>1 # c \<and> (\<forall>d. P\<^bsub>trm\<^esub> d x\<^isub>2) \<Rightarrow> P\<^bsub>trm\<^esub> c (Lam\<^sup>\<alpha> x\<^isub>1 x\<^isub>2)"}\\
+   @{text "\<forall>x\<^isub>1 x\<^isub>2 x\<^isub>3 c. (set (bn\<^sup>\<alpha> x\<^isub>1)) #\<^sup>* c \<and>"}\\ 
+   \hspace{10mm}@{text "(\<forall>d. P\<^bsub>pat\<^esub> d x\<^isub>1) \<and> (\<forall>d. P\<^bsub>trm\<^esub> d x\<^isub>2) \<and> (\<forall>d. P\<^bsub>trm\<^esub> d x\<^isub>3) \<Rightarrow> P\<^bsub>trm\<^esub> c (Let\<^sup>\<alpha> x\<^isub>1 x\<^isub>2 x\<^isub>3)"}\\
    @{text "\<forall>c. P\<^bsub>pat\<^esub> c (PNil\<^sup>\<alpha>)"}\\
    @{text "\<forall>x c. P\<^bsub>pat\<^esub> c (PVar\<^sup>\<alpha> x)"}\\
    @{text "\<forall>x\<^isub>1 x\<^isub>2 c. (\<forall>d. P\<^bsub>pat\<^esub> d x\<^isub>1) \<and> (\<forall>d. P\<^bsub>pat\<^esub> d x\<^isub>2) \<Rightarrow> P\<^bsub>pat\<^esub> c (PTup\<^sup>\<alpha> x\<^isub>1 x\<^isub>2)"}
@@ -2141,45 +2145,122 @@
 
 
   \noindent
-  Instead of establishing the two properties @{text " P\<^bsub>trm\<^esub> y\<^isub>1 \<and>
-  P\<^bsub>pat\<^esub> y\<^isub>2"}, as the weak one does, the stronger
-  induction principle establishes the properties @{text " P\<^bsub>trm\<^esub> c
-  y\<^isub>1 \<and> P\<^bsub>pat\<^esub> c y\<^isub>2"} in which the additional
-  parameter @{text c} is assumed to be of finite support. The purpose of
-  @{text "c"} is to ``control'' which freshness assumptions the binders should
-  satisfy in the @{text "Lam\<^sup>\<alpha>"} and @{text "Let\<^sup>\<alpha>"} cases (these are the cases 
-  where the user specified some binding clauses).
+  Instead of establishing the two properties @{text " P\<^bsub>trm\<^esub>
+  y\<^isub>1 \<and> P\<^bsub>pat\<^esub> y\<^isub>2"}, as the weak one does, the
+  stronger induction principle establishes the properties @{text "
+  P\<^bsub>trm\<^esub> c y\<^isub>1 \<and> P\<^bsub>pat\<^esub> c y\<^isub>2"} in
+  which the additional parameter @{text c} is assumed to be of finite
+  support. The purpose of @{text "c"} is to ``control'' which freshness
+  assumptions the binders should satisfy in the @{text "Lam\<^sup>\<alpha>"} and
+  @{text "Let\<^sup>\<alpha>"} cases: for @{text "Lam\<^sup>\<alpha>"} we can assume the
+  bound atom @{text "x\<^isub>1"} is fresh for @{text "c"}; for @{text
+  "Let\<^sup>\<alpha>"} we can assume all bound atoms from an assignment are fresh
+  for @{text "c"}. If @{text "c"} is instantiated appropriately, the user can
+  mimic the ``pencil-and-paper'' reasoning employing the usual variable
+  convention.
 
   In what follows we will show that the induction principle in
-  \eqref{inductex} implies \eqref{stronginduct}. This fact was established in
-  \cite{UrbanTasson05} by some quite involved, nevertheless automated,
-  induction proof. In this paper we simplify the proof by leveraging the
-  automated proof methods from the function package of Isabelle/HOL
-  \cite{Krauss09}. The reasoning principle behind these methods is
-  well-founded induction. To use them in our setting, we have to discharge two
-  proof obligations: one is that we have well-founded measures (one for each type
-  @{text "ty"}$^\alpha_{1..n}$) that decrease in every induction step and the
-  other is that we have covered all cases. 
+  \eqref{inductex} implies \eqref{stronginduct}. This fact was established for
+  single binders in \cite{UrbanTasson05} by some quite involved, nevertheless
+  automated, induction proof. In this paper we simplify the proof by
+  leveraging the automated proof methods from the function package of
+  Isabelle/HOL \cite{Krauss09}. The reasoning principle behind these methods
+  is well-founded induction. To use them in our setting, we have to discharge
+  two proof obligations: one is that we have well-founded measures (one for
+  each type @{text "ty"}$^\alpha_{1..n}$) that decrease in every induction
+  step and the other is that we have covered all cases. Once these two
+  proof obligations are discharged, the reasoning infrastructure in 
+  the function package will automatically derive the stronger induction
+  principle. This considerably simplifies the work we have to do.
 
   As measures we can use the size functions @{text "size_ty"}$^\alpha_{1..n}$,
   which we lifted in the previous section and which are all well-founded. It
-  is straightforward to establish that these measures decrease in every
+  is straightforward to establish that the sizes decrease in every
   induction step. What is left to show is that we covered all cases. 
-  To do so, we use a \emph{cases lemma} derived for each type. For the terms in \eqref{letpat} 
-  this lemma is of the form
-  
-  \begin{equation}\label{weakcases}
+  To do so, we have to derive stronger cases lemmas, which look in our
+  running example as follows:
+
+  \[\mbox{
+  \begin{tabular}{@ {}c@ {\hspace{6mm}}c@ {}}
   \infer{@{text "P\<^bsub>trm\<^esub>"}}
-  {\begin{array}{l@ {\hspace{9mm}}l}
-  @{text "\<forall>x. t = Var x \<Rightarrow> P\<^bsub>trm\<^esub>"} & @{text "\<forall>a t'. t = Lam a t' \<Rightarrow> P\<^bsub>trm\<^esub>"}\\
-  @{text "\<forall>t\<^isub>1 t\<^isub>2. t = App t\<^isub>1 t\<^isub>2 \<Rightarrow> P\<^bsub>trm\<^esub>"} & @{text "\<forall>p t'. t = Let p t' \<Rightarrow> P\<^bsub>trm\<^esub>"}\\
-  \end{array}}\\[-1mm]
-  \end{equation}
-  
-  where we have a premise for each term-constructor.
-  The idea behind such cases lemmas is that we can conclude with a property @{text "P\<^bsub>trm\<^esub>"},
-  provided we can show that this property holds if we substitute for @{text "t"} all 
-  possible term-constructors. 
+  {\begin{array}{@ {}l@ {}}
+   @{text "\<forall>x. y = Var\<^sup>\<alpha> x \<Rightarrow> P\<^bsub>trm\<^esub>"}\\
+   @{text "\<forall>x\<^isub>1 x\<^isub>2. y = App\<^sup>\<alpha> x\<^isub>1 x\<^isub>2 \<Rightarrow> P\<^bsub>trm\<^esub>"}\\
+   @{text "\<forall>x\<^isub>1 x\<^isub>2. atom x\<^isub>1 # c \<and> y = Lam\<^sup>\<alpha> x\<^isub>1 x\<^isub>2 \<Rightarrow> P\<^bsub>trm\<^esub>"}\\
+   @{text "\<forall>x\<^isub>1 x\<^isub>2 x\<^isub>3. set (bn\<^sup>\<alpha> x\<^isub>1) #\<^sup>* c \<and> y = Let\<^sup>\<alpha> x\<^isub>1 x\<^isub>2 x\<^isub>3 \<Rightarrow> P\<^bsub>trm\<^esub>"}
+   \end{array}} &
+
+  \infer{@{text "P\<^bsub>pat\<^esub>"}}
+  {\begin{array}{@ {}l@ {}}
+   @{text "y = PNil\<^sup>\<alpha>  \<Rightarrow> P\<^bsub>pat\<^esub>"}\\
+   @{text "\<forall>x. y = PVar\<^sup>\<alpha> x \<Rightarrow> P\<^bsub>pat\<^esub>"}\\
+   @{text "\<forall>x\<^isub>1 x\<^isub>2. y = PTup\<^sup>\<alpha> x\<^isub>1 x\<^isub>2 \<Rightarrow> P\<^bsub>pat\<^esub>"}
+  \end{array}}
+  \end{tabular}}
+  \]\smallskip 
+
+  \noindent
+  These stronger cases lemmas need to be derived from the `weak' cases lemmas given
+  in \eqref{inductex}. This is trivial in case of patterns (the one on the right-hand side)
+  since weak and strong cases lemma coincide (there is no binding in patterns).
+  Interesting are only the cases for @{text "Lam\<^sup>\<alpha>"} and @{text "Let\<^sup>\<alpha>"}. There the
+  stronger cases lemma allow us to assume that the bound atoms avoid the context @{text "c"}
+  (which is assumed to be finitely supported).
+ 
+  Let us show first establish the simpler case for @{text "Lam\<^sup>\<alpha>"}. By the weak cases lemma 
+  \eqref{inductex} we can assume that
+
+  \begin{equation}\label{assm}
+  @{text "y = Lam\<^sup>\<alpha> x\<^isub>1 x\<^isub>2"}
+  \end{equation}\smallskip
+
+  \noindent
+  holds and need to establish @{text "P\<^bsub>trm\<^esub>"}. The stronger cases lemma has the implication 
+
+  \begin{equation}\label{imp}
+  @{text "\<forall>x\<^isub>1 x\<^isub>2. atom x\<^isub>1 # c \<and> y = Lam\<^sup>\<alpha> x\<^isub>1 x\<^isub>2 \<Rightarrow> P\<^bsub>trm\<^esub>"}
+  \end{equation}\smallskip
+
+  \noindent
+  which we can use to infer @{text "P\<^bsub>trm\<^esub>"}. Clearly, we cannot
+  use this implication directly, because we have no information whether @{text
+  "x\<^isub>1"} is fresh for @{text "c"}.  However, we can use Properties
+  \ref{supppermeq} and \ref{avoiding} to rename @{text "x\<^isub>1"}. We know
+  by Theorem~\ref{suppfa} that @{text "{atom x\<^isub>1} #\<^sup>* Lam\<^sup>\<alpha>
+  x\<^isub>1 x\<^isub>2"} (since its support is @{text "supp x\<^isub>2 -
+  {atom x\<^isub>1}"}). Property \ref{avoiding} provides us therefore with a
+  permutation @{text "\<pi>"}, such that @{text "{atom (\<pi> \<bullet> x\<^isub>1)} #\<^sup>*
+  c"} and \mbox{@{text "supp (Lam\<^sup>\<alpha> x\<^isub>1 x\<^isub>2) #\<^sup>* \<pi>"}} hold.
+  By using Property \ref{supppermeq}, we can infer from the latter that @{text
+  "Lam\<^sup>\<alpha> (\<pi> \<bullet> x\<^isub>1) (\<pi> \<bullet> x\<^isub>2) = Lam\<^sup>\<alpha> x\<^isub>1 x\<^isub>2"}. We can use this in the assumption
+  \eqref{assm} and then use \eqref{imp} to conclude this case.
+
+  The @{text "Let\<^sup>\<alpha>"}-case involving a (non-recursive) deep binder is more complicated.
+  We have the assumption
+
+  \begin{equation}\label{assm}
+  @{text "y = Let\<^sup>\<alpha> x\<^isub>1 x\<^isub>2 x\<^isub>3"}
+  \end{equation}\smallskip
+
+  \noindent
+  and as implication
+
+  \[
+
+  \]\smallskip
+
+
+  The reason is that the we cannot apply Property \ref{avoiding} to the whole term @{text "Let p t"},
+  because @{text p} might contain names bound by @{text bn}, but also some that are 
+  free. To solve this problem we have to introduce a permutation function that only
+  permutes names bound by @{text bn} and leaves the other names unchanged. We do this again
+  by lifting. For a
+  clause @{text "bn (C x\<^isub>1 \<dots> x\<^isub>r) = rhs"}, we define 
+
+
+  {\bf NOT DONE YET}
+
+  {\it 
   
   The only remaining difficulty is that in order to derive the stronger induction
   principles conveniently, the cases lemma in \eqref{weakcases} is too weak. For this note that
@@ -2187,31 +2268,8 @@
   \emph{all} @{text Let}-terms. 
   What we need instead is a cases lemma where we only have to consider terms that have 
   binders that are fresh w.r.t.~a context @{text "c"}. This gives the implications
-  
-  \begin{center}
-  \begin{tabular}{l}
-  @{text "\<forall>a t'. t = Lam a t' \<and> {atom a} \<FRESH>\<^sup>* c \<Rightarrow> P\<^bsub>trm\<^esub>"}\\
-  @{text "\<forall>p t'. t = Let p t' \<and> (set (bn p)) \<FRESH>\<^sup>* c \<Rightarrow> P\<^bsub>trm\<^esub>"}\\[-2mm]
-  \end{tabular}
-  \end{center}
+
   
-  \noindent
-  which however can be relatively easily be derived from the implications in \eqref{weakcases} 
-  by a renaming using Properties \ref{supppermeq} and \ref{avoiding}. In the first case we know
-  that @{text "{atom a} \<FRESH>\<^sup>* Lam a t"}. Property \eqref{avoiding} provides us therefore with 
-  a permutation @{text q}, such that @{text "{atom (q \<bullet> a)} \<FRESH>\<^sup>* c"} and 
-  @{text "supp (Lam a t) \<FRESH>\<^sup>* q"} hold.
-  By using Property \ref{supppermeq}, we can infer from the latter 
-  that @{text "Lam (q \<bullet> a) (q \<bullet> t) = Lam a t"}
-  and we are done with this case.
-
-  The @{text Let}-case involving a (non-recursive) deep binder is a bit more complicated.
-  The reason is that the we cannot apply Property \ref{avoiding} to the whole term @{text "Let p t"},
-  because @{text p} might contain names bound by @{text bn}, but also some that are 
-  free. To solve this problem we have to introduce a permutation function that only
-  permutes names bound by @{text bn} and leaves the other names unchanged. We do this again
-  by lifting. For a
-  clause @{text "bn (C x\<^isub>1 \<dots> x\<^isub>r) = rhs"}, we define 
   
   \begin{center}
   @{text "p \<bullet>\<^bsub>bn\<^esub> (C x\<^isub>1 \<dots> x\<^isub>r) \<equiv> C y\<^isub>1 \<dots> y\<^isub>r"}  with
@@ -2242,12 +2300,6 @@
   principle.
   
 
-
-  A natural question is
-  whether we can also strengthen the weak induction principles involving
-  the general binders presented here. We will indeed be able to so, but for this we need an 
-  additional notion for permuting deep binders. 
-
   Given a binding function @{text "bn"} we define an auxiliary permutation 
   operation @{text "_ \<bullet>\<^bsub>bn\<^esub> _"} which permutes only bound arguments in a deep binder.
   Assuming a clause of @{text bn} is given as 
@@ -2311,88 +2363,10 @@
   This fact will be crucial when establishing the strong induction principles below.
 
  
-  In our running example about @{text "Let"}, the strong induction
-  principle means that instead 
-  of establishing the implication 
-  
-  \begin{center}
-  @{text "\<forall>p t\<^isub>1 t\<^isub>2. P\<^bsub>pat\<^esub> p \<and> P\<^bsub>trm\<^esub> t\<^isub>1 \<and> P\<^bsub>trm\<^esub> t\<^isub>2 \<Rightarrow> P\<^bsub>trm\<^esub> (Let p t\<^isub>1 t\<^isub>2)"}
-  \end{center}
-  
-  \noindent
-  it is sufficient to establish the following implication
-  
-  \begin{equation}\label{strong}
-  \mbox{\begin{tabular}{l}
-  @{text "\<forall>p t\<^isub>1 t\<^isub>2 c."}\\
-  \hspace{5mm}@{text "set (bn p) #\<^sup>* c \<and>"}\\
-  \hspace{5mm}@{text "(\<forall>d. P\<^bsub>pat\<^esub> d p) \<and> (\<forall>d. P\<^bsub>trm\<^esub> d t\<^isub>1) \<and> (\<forall>d. P\<^bsub>trm\<^esub> d t\<^isub>2)"}\\
-  \hspace{15mm}@{text "\<Rightarrow> P\<^bsub>trm\<^esub> c (Let p t\<^isub>1 t\<^isub>2)"}
-  \end{tabular}}
-  \end{equation}
-  
-  \noindent 
-  While this implication contains an additional argument, namely @{text c}, and 
-  also additional universal quantifications, it is usually easier to establish.
-  The reason is that we have the freshness 
-  assumption @{text "set (bn\<^sup>\<alpha> p) #\<^sup>* c"}, whereby @{text c} can be arbitrarily 
-  chosen by the user as long as it has finite support.
-  
-  Let us now show how we derive the strong induction principles from the
-  weak ones. In case of the @{text "Let"}-example we derive by the weak 
-  induction the following two properties
-  
-  \begin{equation}\label{hyps}
-  @{text "\<forall>q c. P\<^bsub>trm\<^esub> c (q \<bullet> t)"} \hspace{4mm} 
-  @{text "\<forall>q\<^isub>1 q\<^isub>2 c. P\<^bsub>pat\<^esub> (q\<^isub>1 \<bullet>\<AL>\<^bsub>bn\<^esub> (q\<^isub>2 \<bullet> p))"}
-  \end{equation} 
-  
-  \noindent
-  For the @{text Let} term-constructor  we therefore have to establish @{text "P\<^bsub>trm\<^esub> c (q \<bullet> Let p t\<^isub>1 t\<^isub>2)"} 
-  assuming \eqref{hyps} as induction hypotheses (the first for @{text t\<^isub>1} and @{text t\<^isub>2}). 
-  By Property~\ref{avoiding} we
-  obtain a permutation @{text "r"} such that 
-  
-  \begin{equation}\label{rprops}
-  @{term "(r \<bullet> set (bn (q \<bullet> p))) \<sharp>* c "}\hspace{4mm}
-  @{term "supp (Abs_lst (bn (q \<bullet> p)) (q \<bullet> t\<^isub>2)) \<sharp>* r"}
-  \end{equation}
-  
-  \noindent
-  hold. The latter fact and \eqref{renaming} give us
-  
-  \begin{center}
-  \begin{tabular}{l}
-  @{text "Let (q \<bullet> p) (q \<bullet> t\<^isub>1) (q \<bullet> t\<^isub>2) ="} \\
-  \hspace{15mm}@{text "Let (r \<bullet>\<AL>\<^bsub>bn\<^esub> (q \<bullet> p)) (q \<bullet> t\<^isub>1) (r \<bullet> (q \<bullet> t\<^isub>2))"}
-  \end{tabular}
-  \end{center}
-  
-  \noindent
-  So instead of proving @{text "P\<^bsub>trm\<^esub> c (q \<bullet> Let p t\<^isub>1 t\<^isub>2)"}, we can equally
-  establish @{text "P\<^bsub>trm\<^esub> c (Let (r \<bullet>\<AL>\<^bsub>bn\<^esub> (q \<bullet> p)) (q \<bullet> t\<^isub>1) (r \<bullet> (q \<bullet> t\<^isub>2)))"}.
-  To do so, we will use the implication \eqref{strong} of the strong induction
-  principle, which requires us to discharge
-  the following four proof obligations:
-  
-  \begin{center}
-  \begin{tabular}{rl}
-  {\it (i)} &   @{text "set (bn (r \<bullet>\<AL>\<^bsub>bn\<^esub> (q \<bullet> p))) #\<^sup>* c"}\\
-  {\it (ii)} &  @{text "\<forall>d. P\<^bsub>pat\<^esub> d (r \<bullet>\<AL>\<^bsub>bn\<^esub> (q \<bullet> p))"}\\
-  {\it (iii)} & @{text "\<forall>d. P\<^bsub>trm\<^esub> d (q \<bullet> t\<^isub>1)"}\\
-  {\it (iv)} & @{text "\<forall>d. P\<^bsub>trm\<^esub> d (r \<bullet> (q \<bullet> t\<^isub>2))"}\\
-  \end{tabular}
-  \end{center}
-  
-  \noindent
-  The first follows from \eqref{rprops} and Lemma~\ref{permutebn}.{\it (i)}; the 
-  others from the induction hypotheses in \eqref{hyps} (in the fourth case
-  we have to use the fact that @{term "(r \<bullet> (q \<bullet> t\<^isub>2)) = (r + q) \<bullet> t\<^isub>2"}).
-  
-  Taking now the identity permutation @{text 0} for the permutations in \eqref{hyps},
-  we can establish our original goals, namely @{text "P\<^bsub>trm\<^esub> c t"} and \mbox{@{text "P\<^bsub>pat\<^esub> c p"}}.
+
   This completes the proof showing that the weak induction principles imply 
   the strong induction principles. 
+  }
 *}