# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1316033068 -7200
# Node ID 4fafa8d219dc28381bfd3240bd8a2fd5c49a1568
# Parent  e57c175d9214c8b42c2bc5f19576ffa590318088
more on paper

diff -r e57c175d9214 -r 4fafa8d219dc LMCS-Paper/Paper.thy
--- a/LMCS-Paper/Paper.thy	Wed Sep 14 13:40:24 2011 +0900
+++ b/LMCS-Paper/Paper.thy	Wed Sep 14 22:44:28 2011 +0200
@@ -1280,7 +1280,7 @@
   in Isabelle/HOL). 
   We subsequently define each of the user-specified binding 
   functions @{term "bn"}$_{1..m}$ by recursion over the corresponding 
-  raw datatype. We also define permutation operations by 
+  ``raw'' datatype. We also define permutation operations by 
   recursion so that for each term constructor @{text "C"} we have that
   
   \begin{equation}\label{ceqvt}
@@ -1717,7 +1717,7 @@
   Note also that in case of more than one body (e.g.~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 cluase specifies a binder with two bodies.
+  corresponding binding clause specifies a binder with two bodies.
 *}
 
 section {* Establishing the Reasoning Infrastructure *}
@@ -1741,12 +1741,12 @@
   \end{lem}
 
   \begin{proof}
-  The function package of Isabelle/HOL \cite{Krauss09} allows us to prove the
-  first part is by mutual induction over the definitions of the functions.\footnote{We
-  know that they are terminating functions. From this an induction principle
-  is derived by the function package.} The second is by a straightforward 
-  induction over the rules of @{text "\<approx>ty"}$_{1..n}$ and @{text "\<approx>bn"}$_{1..m}$ using 
-  the first part.
+  The function package of Isabelle/HOL allows us to prove the first part by
+  mutual induction over the definitions of the functions.\footnote{We have
+  that they are terminating functions. From this an induction principle is
+  derived by the function package \cite{Krauss09}.} The second is by a
+  straightforward induction over the rules of @{text "\<approx>ty"}$_{1..n}$ and
+  @{text "\<approx>bn"}$_{1..m}$ using the first part.
   \end{proof}
 
   \noindent
@@ -1856,7 +1856,8 @@
   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 $\approx_{\textit{set}}^{\textit{R}, \textit{fa}}$
-  are replaced by $\approx_{\textit{set}}^{=, \textit{fa}}$.
+  are replaced by $\approx_{\textit{set}}^{=, \textit{fa}}$ (similarly for the
+  other binding modes).
 
   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
@@ -1873,27 +1874,26 @@
   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 the size functions @{text "size_ty\<AL>"}$_{1..n}$.
-  The latter are defined automatically for the raw types @{text "ty"}$_{1..n}$
+  "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)
   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 all cases how an element in a type @{text "ty\<AL>"}$_i$ can
-  be constructed (that means one case for each of term-constructors
-  of type @{text "ty\<AL>"}$_i\,$). The lifted cases
-  lemma for the type @{text "ty\<AL>"}$_i\,$ looks as
-  follows
+  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
+  constructed (that means one case for each of the term-constructors in @{text
+  "ty\<AL>"}$_i\,$). The lifted cases lemma for the type @{text
+  "ty\<AL>"}$_i\,$ looks as follows
 
-  \[
+  \begin{equation}\label{cases}
   \infer{P}
   {\begin{array}{l}
   @{text "\<forall>x\<^isub>1\<dots>x\<^isub>k. y = C\<AL>\<^isub>1 x\<^isub>1 \<dots> x\<^isub>k \<Rightarrow> P"}\\
   \hspace{5mm}\ldots\\
   @{text "\<forall>x\<^isub>1\<dots>x\<^isub>l. y = C\<AL>\<^isub>m x\<^isub>1 \<dots> x\<^isub>l \<Rightarrow> P"}\\
   \end{array}}
-  \]\smallskip
+  \end{equation}\smallskip
 
   \noindent
   where @{text "y"} is a variable of type @{text "ty"}$_i$ and @{text "P"} is the 
@@ -1901,60 +1901,86 @@
   induction principle for the types @{text "ty\<AL>"}$_{1..n}$, which is of the 
   form
 
-   \[
+   \begin{equation}\label{induct}
   \infer{@{text "P\<^isub>1 y\<^isub>1 \<and> \<dots> \<and> P\<^isub>n y\<^isub>n "}}
   {\begin{array}{l}
   @{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>\<^isub>1 x\<^isub>1 \<dots> x\<^isub>k)"}\\
   \hspace{5mm}\ldots\\
   @{text "\<forall>x\<^isub>1\<dots>x\<^isub>l. P\<^isub>r x\<^isub>r \<and> \<dots> \<and> P\<^isub>s x\<^isub>s \<Rightarrow> P (C\<AL>\<^isub>m x\<^isub>1 \<dots> x\<^isub>l)"}\\
   \end{array}}
+  \end{equation}\smallskip
+
+  \noindent
+  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
+
+  \[
+  \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)"}} 
+  \]\smallskip
+
+  \noindent 
+  in which the @{text "x"}$_{i..j}$ @{text "\<subseteq>"} @{text "x"}$_{1..k}$ are the
+  recursive arguments of this term constructor (similarly for the other
+  term-constructors). 
+
+  Recall the lambda-calculus with @{text "Let"}-patterns shown in
+  \eqref{letpat}. The cases lemmas and the induction principle shown in
+  \eqref{cases} and \eqref{induct} boil down to the following three inference
+  rules (the cases lemmas are on the left-hand side; the induction principle
+  on the right):
+
+  \begin{equation}\label{inductex}\mbox{
+  \begin{tabular}{c@ {\hspace{10mm}}c}
+  \begin{tabular}{@ {}c@ {}}
+  \infer{@{text "P\<^bsub>trm\<^esub>"}}
+  {\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>"}
+   \end{array}}\medskip\\
+
+  \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} 
+  &
+  
+  \begin{tabular}{@ {}c@ {}}
+  \infer{@{text "P\<^bsub>trm\<^esub> y\<^isub>1 \<and> P\<^bsub>pat\<^esub> y\<^isub>2"}}
+  {\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 "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)"}
+  \end{array}}
+  \end{tabular}
+  \end{tabular}}
+  \end{equation}\smallskip
+
+  By working now completely on the alpha-equated level, we
+  can first show using \eqref{calphaeqvt} that the support of each term
+  constructor is included in the support of its arguments, 
+  namely
+
+  \[
+  @{text "(supp x\<^isub>1 \<union> \<dots> \<union> supp x\<^isub>r) supports (C\<^sup>\<alpha> x\<^isub>1 \<dots> x\<^isub>r)"}
   \]\smallskip
 
   \noindent
-  whereby the @{text P}$_{1..n}$ are the properties established by induction 
-  and the @{text y}$_{1..n}$ are of type @{text "ty\<AL>"}$_{1..n}$. 
-  This induction principle has for the term constructors @{text "C"}$^\alpha_1$ 
-  a premise of the form
-  
-  \begin{equation}\label{weakprem}
-  \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)"}} 
-  \end{equation}\smallskip
-
-  \noindent 
-  in which the @{text "x"}$_{i..j}$ @{text "\<subseteq>"} @{text "x"}$_{1..k}$ are 
-  the recursive arguments of this term constructor (similarly for the other
-  term-constructors). In case of the lambda-calculus (with constructors
-   @{text "Var\<^sup>\<alpha>"},  @{text "App\<^sup>\<alpha>"} and  @{text "Lam\<^sup>\<alpha>"}),
-  the cases lemmas and the induction principle boil down to the following
-  two inference rules:
-
-  \[\mbox{
-  \begin{tabular}{c@ {\hspace{10mm}}c}
-  \infer{@{text "P"}}
-  {\begin{array}{l}
-   @{text "\<forall>x. y = Var\<^sup>\<alpha> x \<Rightarrow> P"}\\
-   @{text "\<forall>x\<^isub>1 x\<^isub>2. y = App\<^sup>\<alpha> x\<^isub>1 x\<^isub>2 \<Rightarrow> P"}\\
-   @{text "\<forall>x\<^isub>1 x\<^isub>2. y = Lam\<^sup>\<alpha> x\<^isub>1 x\<^isub>2 \<Rightarrow> P"}
-   \end{array}} &
-
-  \infer{@{text "P y"}}
-  {\begin{array}{l}
-   @{text "\<forall>x. P (Var\<^sup>\<alpha> x)"}\\
-   @{text "\<forall>x\<^isub>1 x\<^isub>2. P x\<^isub>1 \<and> P x\<^isub>2 \<Rightarrow> P (App\<^sup>\<alpha> x\<^isub>1 x\<^isub>2)"}\\
-   @{text "\<forall>x\<^isub>1 x\<^isub>2. P x\<^isub>2 \<Rightarrow> P (Lam\<^sup>\<alpha> x\<^isub>1 x\<^isub>2)"}
-   \end{array}}
-  \end{tabular}}
-  \]\smallskip
-
-  \noindent
-  We will show in the next section that these inference rules are not very 
-  convenient for the user to establish properties about lambda-terms, but
-  they are crucial for completing our reasoning infrastructure for the 
-  types @{text "ty\<AL>"}$_{1..n}$.
-
-  By working now completely on the alpha-equated level, we
-  can first show that the free-atom functions and binding functions are
-  equivariant, namely
+  This allows us to prove using the induction principle for  @{text "ty\<AL>"}$_{1..n}$ 
+  that every element of type @{text "ty\<AL>"}$_{1..n}$ is finitely supported 
+  (using Prop.~\ref{supportsprop}{\it (i)}). 
+  Similarly, we can establish by induction that the free-atom functions and binding 
+  functions are equivariant, namely
   
   \[\mbox{
   \begin{tabular}{rcl}
@@ -1966,25 +1992,11 @@
 
   
   \noindent
-  These properties can be established using the induction principle for the
-  types @{text "ty\<AL>"}$_{1..n}$.  Having these
-  equivariant properties at our disposal, we can show that the support of
-  term-constructors @{text "C\<^sup>\<alpha>"} is included in the support of its
-  arguments, that means
-
-  \[
-  @{text "supp (C\<^sup>\<alpha> x\<^isub>1 \<dots> x\<^isub>r) \<subseteq> (supp x\<^isub>1 \<union> \<dots> \<union> supp x\<^isub>r)"}
-  \]\smallskip
- 
-  \noindent
-  holds. This allows us to prove by induction that every @{text x} of type
-  @{text "ty\<AL>"}$_{1..n}$ is finitely supported. This can be again shown by
-  the induction principle for  @{text "ty\<AL>"}$_{1..n}$. Lastly, we can show that the
-  support of elements in @{text "ty\<AL>"}$_{1..n}$ is the same as @{text
-  "fa_ty\<AL>"}$_{1..n}$.  This fact is important in the nominal setting
-  where the general theory is formulated in terms of @{text "supp"} and @{text "#"}, but
-  also provides evidence that our notions of free-atoms and alpha-equivalence
-  are sensible.
+  Lastly, we can show that the support of elements in @{text
+  "ty\<AL>"}$_{1..n}$ is the same as @{text "fa_ty\<AL>"}$_{1..n}$.  This fact
+  is important in the nominal setting where the general theory is formulated
+  in terms of support and freshness, but also provides evidence that our
+  notions of free-atoms and alpha-equivalence ``match up''.
 
   \begin{thm} 
   For @{text "x"}$_{1..n}$ with type @{text "ty\<AL>"}$_{1..n}$, we have
@@ -1995,67 +2007,94 @@
   The proof is by induction. 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 the facts derived in Theorem~\ref{suppabs}.
+  proof. For the abstraction cases we use then the facts derived in Theorem~\ref{suppabs},
+  for which we have to know that every body of an abstraction is finitely supported.
+  This we have proved earlier.
   \end{proof}
 
   \noindent
-  To sum up this section, we can establish automatically a reasoning infrastructure
-  for the types @{text "ty\<AL>"}$_{1..n}$ 
-  by first lifting definitions from the ``raw'' level to the quotient level and
-  then by establishing facts about these lifted definitions. All necessary proofs
-  are generated automatically by custom ML-code. 
-
+  To sum up this section, we can establish a reasoning infrastructure for the
+  types @{text "ty\<AL>"}$_{1..n}$ by first lifting definitions from the
+  ``raw'' level to the quotient level and then by proving facts about
+  these lifted definitions. All necessary proofs are generated automatically
+  by custom ML-code.
 *}
 
 
 section {* Strong Induction Principles *}
 
 text {*
-  In the previous section we derived induction principles for alpha-equated terms. 
-  We call such induction principles \emph{weak}, because for a 
-  term-constructor \mbox{@{text "C\<^sup>\<alpha> x\<^isub>1\<dots>x\<^isub>r"}}
-  the induction hypothesis requires us to establish the implications \eqref{weakprem}.
-  The problem with these implications is that in general they are difficult to establish.
-  The reason is that we cannot make any assumption about the bound atoms that might be in @{text "C\<^sup>\<alpha>"}. 
-  (for example we cannot assume the variable convention for them).
+  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 
+  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
 
-  In \cite{UrbanTasson05} we introduced a method for automatically
-  strengthening weak induction principles for terms containing single
-  binders. These stronger induction principles allow the user to make additional
-  assumptions about bound atoms. 
-  These additional assumptions amount to a formal
-  version of the informal variable convention for binders. 
-  To sketch how this strengthening extends to the case of multiple binders, we use as
-  running example the term-constructors @{text "Lam"} and @{text "Let"}
-  from example \eqref{letpat}. Instead of establishing @{text " P\<^bsub>trm\<^esub> t \<and> P\<^bsub>pat\<^esub> p"},
-  the stronger induction principle for \eqref{letpat} establishes properties @{text " P\<^bsub>trm\<^esub> c t \<and> P\<^bsub>pat\<^esub> c p"}
-  where the additional parameter @{text c} controls
-  which freshness assumptions the binders should satisfy. For the two term constructors 
-  this means that the user has to establish in inductions the implications
-  
-  \begin{center}
-  \begin{tabular}{l}
-  @{text "\<forall>a t c. {atom a} \<FRESH>\<^sup>* c \<and> (\<forall>d. P\<^bsub>trm\<^esub> d t) \<Rightarrow> P\<^bsub>trm\<^esub> c (Lam a t)"}\\
-  @{text "\<forall>p t c. (set (bn p)) \<FRESH>\<^sup>* c \<and> (\<forall>d. P\<^bsub>pat\<^esub> d p) \<and> (\<forall>d. P\<^bsub>trm\<^esub> d t) \<and> \<Rightarrow> P\<^bsub>trm\<^esub> c (Let p t)"}\\%[-0mm]
-  \end{tabular}
-  \end{center}
+  \begin{equation}\label{stronginduct}
+  \mbox{
+  \begin{tabular}{@ {}c@ {}}
+  \infer{@{text "P\<^bsub>trm\<^esub> c y\<^isub>1 \<and> P\<^bsub>pat\<^esub> c y\<^isub>2"}}
+  {\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 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>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)"}
+  \end{array}}
+  \end{tabular}}
+  \end{equation}\smallskip
+
 
-  In \cite{UrbanTasson05} we showed how the weaker induction principles imply
-  the stronger ones. This was done by some quite complicated, nevertheless automated,
-  induction proof. In this paper we simplify this work by leveraging the automated proof
-  methods from the function package of Isabelle/HOL. 
-  The reasoning principle these methods employ 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 (for each type @{text "ty"}$^\alpha_{1..n}$) that decrease in 
-  every induction step and the other is that we have covered all cases. 
-  As measures we 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 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} 
+  \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).
+
+  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. 
+
+  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
+  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}
@@ -2352,7 +2391,7 @@
   is as expected (that means bound names are removed from the support). We
   also showed that our specifications lift from ``raw'' types to types of
   alpha-equivalence classes. For this we had to establish (automatically) that every
-  term-constructor and function is repectful w.r.t.~alpha-equivalence.
+  term-constructor and function is respectful w.r.t.~alpha-equivalence.
 
   Although we were heavily inspired by the syntax of Ott, its definition of
   alpha-equi\-valence is unsuitable for our extension of Nominal