doc-src/TutorialI/Misc/document/Itrev.tex

tuned msg;

\begin{isabelle}%
%
\begin{isamarkuptext}%
We define a tail-recursive version of list-reversal,
i.e.\ one that can be compiled into a loop:%
\end{isamarkuptext}%
\isacommand{consts}~itrev~::~{"}'a~list~{\isasymRightarrow}~'a~list~{\isasymRightarrow}~'a~list{"}\isanewline
\isacommand{primrec}\isanewline
{"}itrev~[]~~~~~ys~=~ys{"}\isanewline
{"}itrev~(x\#xs)~ys~=~itrev~xs~(x\#ys){"}%
\begin{isamarkuptext}%
\noindent
The behaviour of \isa{itrev} is simple: it reverses its first argument by
stacking its elements onto the second argument, and returning that second
argument when the first one becomes empty.
We need to show that \isa{itrev} does indeed reverse its first argument
provided the second one is empty:%
\end{isamarkuptext}%
\isacommand{lemma}~{"}itrev~xs~[]~=~rev~xs{"}%
\begin{isamarkuptxt}%
\noindent
There is no choice as to the induction variable, and we immediately simplify:%
\end{isamarkuptxt}%
\isacommand{apply}(induct\_tac~xs,~auto)%
\begin{isamarkuptxt}%
\noindent
Unfortunately, this is not a complete success:
\begin{isabellepar}%
~1.~\dots~itrev~list~[]~=~rev~list~{\isasymLongrightarrow}~itrev~list~[a]~=~rev~list~@~[a]%
\end{isabellepar}%
Just as predicted above, the overall goal, and hence the induction
hypothesis, is too weak to solve the induction step because of the fixed
\isa{[]}. The corresponding heuristic:
\begin{quote}
{\em 3. Generalize goals for induction by replacing constants by variables.}
\end{quote}

Of course one cannot do this na\"{\i}vely: \isa{itrev xs ys = rev xs} is
just not true---the correct generalization is%
\end{isamarkuptxt}%
\isacommand{lemma}~{"}itrev~xs~ys~=~rev~xs~@~ys{"}%
\begin{isamarkuptxt}%
\noindent
If \isa{ys} is replaced by \isa{[]}, the right-hand side simplifies to
\isa{rev xs}, just as required.

In this particular instance it was easy to guess the right generalization,
but in more complex situations a good deal of creativity is needed. This is
the main source of complications in inductive proofs.

Although we now have two variables, only \isa{xs} is suitable for
induction, and we repeat our above proof attempt. Unfortunately, we are still
not there:
\begin{isabellepar}%
~1.~{\isasymAnd}a~list.\isanewline
~~~~~~~itrev~list~ys~=~rev~list~@~ys~{\isasymLongrightarrow}\isanewline
~~~~~~~itrev~list~(a~\#~ys)~=~rev~list~@~a~\#~ys%
\end{isabellepar}%
The induction hypothesis is still too weak, but this time it takes no
intuition to generalize: the problem is that \isa{ys} is fixed throughout
the subgoal, but the induction hypothesis needs to be applied with
\isa{a \# ys} instead of \isa{ys}. Hence we prove the theorem
for all \isa{ys} instead of a fixed one:%
\end{isamarkuptxt}%
\isacommand{lemma}~{"}{\isasymforall}ys.~itrev~xs~ys~=~rev~xs~@~ys{"}%
\begin{isamarkuptxt}%
\noindent
This time induction on \isa{xs} followed by simplification succeeds. This
leads to another heuristic for generalization:
\begin{quote}
{\em 4. Generalize goals for induction by universally quantifying all free
variables {\em(except the induction variable itself!)}.}
\end{quote}
This prevents trivial failures like the above and does not change the
provability of the goal. Because it is not always required, and may even
complicate matters in some cases, this heuristic is often not
applied blindly.%
\end{isamarkuptxt}%
\end{isabelle}%
%%% Local Variables:
%%% mode: latex
%%% TeX-master: "root"
%%% End: