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.15  \ {\isadigit{1}}{\isachardot}\ {\isasymAnd}a\ list{\isachardot}\isanewline
    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.39 -will need to be creative. Additionally, you can read \S\ref{sec:advanced-ind}
    1.40 -to learn about some advanced techniques for inductive proofs.
    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
    1.56 +will need to be creative. Additionally, you can read \S\ref{sec:advanced-ind}
    1.57 +to learn about some advanced techniques for inductive proofs.%
    1.58  \end{isamarkuptext}%
    1.59  \end{isabellebody}%
    1.60  %%% Local Variables: