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

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: