--- a/doc-src/TutorialI/Misc/Itrev.thy Tue Sep 05 13:12:00 2000 +0200
+++ b/doc-src/TutorialI/Misc/Itrev.thy Tue Sep 05 13:53:39 2000 +0200
@@ -2,7 +2,32 @@
theory Itrev = Main:;
(*>*)
-text{*
+section{*Induction heuristics*}
+
+text{*\label{sec:InductionHeuristics}
+The purpose of this section is to illustrate some simple heuristics for
+inductive proofs. The first one we have already mentioned in our initial
+example:
+\begin{quote}
+\emph{Theorems about recursive functions are proved by induction.}
+\end{quote}
+In case the function has more than one argument
+\begin{quote}
+\emph{Do induction on argument number $i$ if the function is defined by
+recursion in argument number $i$.}
+\end{quote}
+When we look at the proof of @{term[source]"(xs @ ys) @ zs = xs @ (ys @ zs)"}
+in \S\ref{sec:intro-proof} we find (a) @{text"@"} is recursive in
+the first argument, (b) @{term xs} occurs only as the first argument of
+@{text"@"}, and (c) both @{term ys} and @{term zs} occur at least once as
+the second argument of @{text"@"}. Hence it is natural to perform induction
+on @{term xs}.
+
+The key heuristic, and the main point of this section, is to
+generalize the goal before induction. The reason is simple: if the goal is
+too specific, the induction hypothesis is too weak to allow the induction
+step to go through. Let us now illustrate the idea with an example.
+
Function @{term"rev"} has quadratic worst-case running time
because it calls function @{text"@"} for each element of the list and
@{text"@"} is linear in its first argument. A linear time version of
@@ -36,7 +61,7 @@
txt{*\noindent
Unfortunately, this is not a complete success:
-\begin{isabelle}
+\begin{isabelle}\makeatother
~1.~\dots~itrev~list~[]~=~rev~list~{\isasymLongrightarrow}~itrev~list~[a]~=~rev~list~@~[a]%
\end{isabelle}
Just as predicted above, the overall goal, and hence the induction
@@ -62,7 +87,7 @@
Although we now have two variables, only @{term"xs"} is suitable for
induction, and we repeat our above proof attempt. Unfortunately, we are still
not there:
-\begin{isabelle}
+\begin{isabelle}\makeatother
~1.~{\isasymAnd}a~list.\isanewline
~~~~~~~itrev~list~ys~=~rev~list~@~ys~{\isasymLongrightarrow}\isanewline
~~~~~~~itrev~list~(a~\#~ys)~=~rev~list~@~a~\#~ys
@@ -75,8 +100,11 @@
*};
(*<*)oops;(*>*)
lemma "\\<forall>ys. itrev xs ys = rev xs @ ys";
+(*<*)
+by(induct_tac xs, simp_all);
+(*>*)
-txt{*\noindent
+text{*\noindent
This time induction on @{term"xs"} followed by simplification succeeds. This
leads to another heuristic for generalization:
\begin{quote}
@@ -94,9 +122,19 @@
the problem at hand and is beyond simple rules of thumb. In a nutshell: you
will need to be creative. Additionally, you can read \S\ref{sec:advanced-ind}
to learn about some advanced techniques for inductive proofs.
-*};
+A final point worth mentioning is the orientation of the equation we just
+proved: the more complex notion (@{term itrev}) is on the left-hand
+side, the simpler one (@{term rev}) on the right-hand side. This constitutes
+another, albeit weak heuristic that is not restricted to induction:
+\begin{quote}
+ \emph{The right-hand side of an equation should (in some sense) be simpler
+ than the left-hand side.}
+\end{quote}
+This heuristic is tricky to apply because it is not obvious that
+@{term"rev xs @ ys"} is simpler than @{term"itrev xs ys"}. But see what
+happens if you try to prove @{prop"rev xs @ ys = itrev xs ys"}!
+*}
(*<*)
-by(induct_tac xs, simp_all);
end
(*>*)