doc-src/TutorialI/Misc/Itrev.thy

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/TutorialI/Misc/Itrev.thy	Wed Apr 19 11:56:31 2000 +0200
@@ -0,0 +1,90 @@
+(*<*)
+theory Itrev = Main:;
+(*>*)
+
+text{*
+We define a tail-recursive version of list-reversal,
+i.e.\ one that can be compiled into a loop:
+*}
+
+consts itrev :: "'a list \\<Rightarrow> 'a list \\<Rightarrow> 'a list";
+primrec
+"itrev []     ys = ys"
+"itrev (x#xs) ys = itrev xs (x#ys)";
+
+text{*\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:
+*}
+
+lemma "itrev xs [] = rev xs";
+
+txt{*\noindent
+There is no choice as to the induction variable, and we immediately simplify:
+*}
+
+apply(induct_tac xs, auto);
+
+txt{*\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
+*}
+(*<*)oops;(*>*)
+lemma "itrev xs ys = rev xs @ ys";
+
+txt{*\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:
+*}
+(*<*)oops;(*>*)
+lemma "\\<forall>ys. itrev xs ys = rev xs @ ys";
+
+txt{*\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.
+*}
+
+(*<*)
+oops;
+end
+(*>*)