--- 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