doc-src/TutorialI/Misc/document/Itrev.tex
 changeset 10971 6852682eaf16 parent 10950 aa788fcb75a5 child 11458 09a6c44a48ea
     1.1 --- a/doc-src/TutorialI/Misc/document/Itrev.tex	Wed Jan 24 11:59:15 2001 +0100
1.2 +++ b/doc-src/TutorialI/Misc/document/Itrev.tex	Wed Jan 24 12:29:10 2001 +0100
1.3 @@ -28,7 +28,7 @@
1.4  The key heuristic, and the main point of this section, is to
1.5  generalize the goal before induction. The reason is simple: if the goal is
1.6  too specific, the induction hypothesis is too weak to allow the induction
1.7 -step to go through. Let us now illustrate the idea with an example.
1.8 +step to go through. Let us illustrate the idea with an example.
1.9
1.10  Function \isa{rev} has quadratic worst-case running time
1.11  because it calls function \isa{{\isacharat}} for each element of the list and
1.12 @@ -62,8 +62,7 @@
1.13  Unfortunately, this is not a complete success:
1.14  \begin{isabelle}%
1.16 -\isaindent{\ {\isadigit{1}}{\isachardot}\ \ \ \ }itrev\ list\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharequal}\ rev\ list\ {\isasymLongrightarrow}\isanewline
1.17 -\isaindent{\ {\isadigit{1}}{\isachardot}\ \ \ \ }itrev\ list\ {\isacharbrackleft}a{\isacharbrackright}\ {\isacharequal}\ rev\ list\ {\isacharat}\ {\isacharbrackleft}a{\isacharbrackright}%
1.18 +\isaindent{\ {\isadigit{1}}{\isachardot}\ \ \ \ }itrev\ list\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharequal}\ rev\ list\ {\isasymLongrightarrow}\ itrev\ list\ {\isacharbrackleft}a{\isacharbrackright}\ {\isacharequal}\ rev\ list\ {\isacharat}\ {\isacharbrackleft}a{\isacharbrackright}%
1.19  \end{isabelle}
1.20  Just as predicted above, the overall goal, and hence the induction
1.21  hypothesis, is too weak to solve the induction step because of the fixed
1.22 @@ -72,7 +71,7 @@
1.23  \emph{Generalize goals for induction by replacing constants by variables.}
1.24  \end{quote}
1.25  Of course one cannot do this na\"{\i}vely: \isa{itrev\ xs\ ys\ {\isacharequal}\ rev\ xs} is
1.26 -just not true---the correct generalization is%
1.27 +just not true --- the correct generalization is%
1.28  \end{isamarkuptxt}%
1.29  \isacommand{lemma}\ {\isachardoublequote}itrev\ xs\ ys\ {\isacharequal}\ rev\ xs\ {\isacharat}\ ys{\isachardoublequote}%
1.30  \begin{isamarkuptxt}%
1.31 @@ -114,13 +113,6 @@
1.32  The variables that require generalization are typically those that
1.33  change in recursive calls.
1.34
1.35 -In general, if you have tried the above heuristics and still find your
1.36 -induction does not go through, and no obvious lemma suggests itself, you may
1.37 -need to generalize your proposition even further. This requires insight into
1.38 -the problem at hand and is beyond simple rules of thumb.  You
1.41 -
1.42  A final point worth mentioning is the orientation of the equation we just
1.43  proved: the more complex notion (\isa{itrev}) is on the left-hand
1.44  side, the simpler one (\isa{rev}) on the right-hand side. This constitutes
1.45 @@ -131,7 +123,14 @@
1.46  \end{quote}
1.47  This heuristic is tricky to apply because it is not obvious that
1.48  \isa{rev\ xs\ {\isacharat}\ ys} is simpler than \isa{itrev\ xs\ ys}. But see what
1.49 -happens if you try to prove \isa{rev\ xs\ {\isacharat}\ ys\ {\isacharequal}\ itrev\ xs\ ys}!%
1.50 +happens if you try to prove \isa{rev\ xs\ {\isacharat}\ ys\ {\isacharequal}\ itrev\ xs\ ys}!
1.51 +
1.52 +In general, if you have tried the above heuristics and still find your
1.53 +induction does not go through, and no obvious lemma suggests itself, you may
1.54 +need to generalize your proposition even further. This requires insight into
1.55 +the problem at hand and is beyond simple rules of thumb.  You