doc-src/TutorialI/Misc/Itrev.thy
changeset 10971 6852682eaf16
parent 10885 90695f46440b
child 11458 09a6c44a48ea
     1.1 --- a/doc-src/TutorialI/Misc/Itrev.thy	Wed Jan 24 11:59:15 2001 +0100
     1.2 +++ b/doc-src/TutorialI/Misc/Itrev.thy	Wed Jan 24 12:29:10 2001 +0100
     1.3 @@ -26,7 +26,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 @{term"rev"} has quadratic worst-case running time
    1.11  because it calls function @{text"@"} for each element of the list and
    1.12 @@ -61,7 +61,7 @@
    1.13  
    1.14  txt{*\noindent
    1.15  Unfortunately, this is not a complete success:
    1.16 -@{subgoals[display,indent=0,margin=65]}
    1.17 +@{subgoals[display,indent=0,margin=70]}
    1.18  Just as predicted above, the overall goal, and hence the induction
    1.19  hypothesis, is too weak to solve the induction step because of the fixed
    1.20  argument, @{term"[]"}.  This suggests a heuristic:
    1.21 @@ -69,7 +69,7 @@
    1.22  \emph{Generalize goals for induction by replacing constants by variables.}
    1.23  \end{quote}
    1.24  Of course one cannot do this na\"{\i}vely: @{term"itrev xs ys = rev xs"} is
    1.25 -just not true---the correct generalization is
    1.26 +just not true --- the correct generalization is
    1.27  *};
    1.28  (*<*)oops;(*>*)
    1.29  lemma "itrev xs ys = rev xs @ ys";
    1.30 @@ -112,13 +112,6 @@
    1.31  The variables that require generalization are typically those that 
    1.32  change in recursive calls.
    1.33  
    1.34 -In general, if you have tried the above heuristics and still find your
    1.35 -induction does not go through, and no obvious lemma suggests itself, you may
    1.36 -need to generalize your proposition even further. This requires insight into
    1.37 -the problem at hand and is beyond simple rules of thumb.  You
    1.38 -will need to be creative. Additionally, you can read \S\ref{sec:advanced-ind}
    1.39 -to learn about some advanced techniques for inductive proofs.
    1.40 -
    1.41  A final point worth mentioning is the orientation of the equation we just
    1.42  proved: the more complex notion (@{term itrev}) is on the left-hand
    1.43  side, the simpler one (@{term rev}) on the right-hand side. This constitutes
    1.44 @@ -130,6 +123,13 @@
    1.45  This heuristic is tricky to apply because it is not obvious that
    1.46  @{term"rev xs @ ys"} is simpler than @{term"itrev xs ys"}. But see what
    1.47  happens if you try to prove @{prop"rev xs @ ys = itrev xs ys"}!
    1.48 +
    1.49 +In general, if you have tried the above heuristics and still find your
    1.50 +induction does not go through, and no obvious lemma suggests itself, you may
    1.51 +need to generalize your proposition even further. This requires insight into
    1.52 +the problem at hand and is beyond simple rules of thumb.  You
    1.53 +will need to be creative. Additionally, you can read \S\ref{sec:advanced-ind}
    1.54 +to learn about some advanced techniques for inductive proofs.
    1.55  *}
    1.56  (*<*)
    1.57  end