summary |
shortlog |
changelog |
graph |
tags |
branches |
files |
changeset |
file |
revisions |
annotate |
diff |
raw

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