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.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