diff -r f51d4a302962 -r 5386df44a037 doc-src/TutorialI/Misc/Itrev.thy --- a/doc-src/TutorialI/Misc/Itrev.thy Tue Aug 28 18:46:15 2012 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,146 +0,0 @@ -(*<*) -theory Itrev -imports Main -begin -declare [[names_unique = false]] -(*>*) - -section{*Induction Heuristics*} - -text{*\label{sec:InductionHeuristics} -\index{induction heuristics|(}% -The purpose of this section is to illustrate some simple heuristics for -inductive proofs. The first one we have already mentioned in our initial -example: -\begin{quote} -\emph{Theorems about recursive functions are proved by induction.} -\end{quote} -In case the function has more than one argument -\begin{quote} -\emph{Do induction on argument number $i$ if the function is defined by -recursion in argument number $i$.} -\end{quote} -When we look at the proof of @{text"(xs@ys) @ zs = xs @ (ys@zs)"} -in \S\ref{sec:intro-proof} we find -\begin{itemize} -\item @{text"@"} is recursive in -the first argument -\item @{term xs} occurs only as the first argument of -@{text"@"} -\item both @{term ys} and @{term zs} occur at least once as -the second argument of @{text"@"} -\end{itemize} -Hence it is natural to perform induction on~@{term xs}. - -The key heuristic, and the main point of this section, is to -\emph{generalize the goal before induction}. -The reason is simple: if the goal is -too specific, the induction hypothesis is too weak to allow the induction -step to go through. Let us illustrate the idea with an example. - -Function \cdx{rev} has quadratic worst-case running time -because it calls function @{text"@"} for each element of the list and -@{text"@"} is linear in its first argument. A linear time version of -@{term"rev"} reqires an extra argument where the result is accumulated -gradually, using only~@{text"#"}: -*} - -primrec itrev :: "'a list \ 'a list \ 'a list" where -"itrev [] ys = ys" | -"itrev (x#xs) ys = itrev xs (x#ys)" - -text{*\noindent -The behaviour of \cdx{itrev} is simple: it reverses -its first argument by stacking its elements onto the second argument, -and returning that second argument when the first one becomes -empty. Note that @{term"itrev"} is tail-recursive: it can be -compiled into a loop. - -Naturally, we would like to show that @{term"itrev"} does indeed reverse -its first argument provided the second one is empty: -*}; - -lemma "itrev xs [] = rev xs"; - -txt{*\noindent -There is no choice as to the induction variable, and we immediately simplify: -*}; - -apply(induct_tac xs, simp_all); - -txt{*\noindent -Unfortunately, this attempt does not prove -the induction step: -@{subgoals[display,indent=0,margin=70]} -The induction hypothesis is too weak. The fixed -argument,~@{term"[]"}, prevents it from rewriting the conclusion. -This example suggests a heuristic: -\begin{quote}\index{generalizing induction formulae}% -\emph{Generalize goals for induction by replacing constants by variables.} -\end{quote} -Of course one cannot do this na\"{\i}vely: @{term"itrev xs ys = rev xs"} is -just not true. The correct generalization is -*}; -(*<*)oops;(*>*) -lemma "itrev xs ys = rev xs @ ys"; -(*<*)apply(induct_tac xs, simp_all)(*>*) -txt{*\noindent -If @{term"ys"} is replaced by @{term"[]"}, the right-hand side simplifies to -@{term"rev xs"}, as required. - -In this instance it was easy to guess the right generalization. -Other situations can require a good deal of creativity. - -Although we now have two variables, only @{term"xs"} is suitable for -induction, and we repeat our proof attempt. Unfortunately, we are still -not there: -@{subgoals[display,indent=0,goals_limit=1]} -The induction hypothesis is still too weak, but this time it takes no -intuition to generalize: the problem is that @{term"ys"} is fixed throughout -the subgoal, but the induction hypothesis needs to be applied with -@{term"a # ys"} instead of @{term"ys"}. Hence we prove the theorem -for all @{term"ys"} instead of a fixed one: -*}; -(*<*)oops;(*>*) -lemma "\ys. itrev xs ys = rev xs @ ys"; -(*<*) -by(induct_tac xs, simp_all); -(*>*) - -text{*\noindent -This time induction on @{term"xs"} followed by simplification succeeds. This -leads to another heuristic for generalization: -\begin{quote} -\emph{Generalize goals for induction by universally quantifying all free -variables {\em(except the induction variable itself!)}.} -\end{quote} -This prevents trivial failures like the one above and does not affect the -validity of the goal. However, this heuristic should not be applied blindly. -It is not always required, and the additional quantifiers can complicate -matters in some cases. The variables that should be quantified are typically -those that change in recursive calls. - -A final point worth mentioning is the orientation of the equation we just -proved: the more complex notion (@{const itrev}) is on the left-hand -side, the simpler one (@{term rev}) on the right-hand side. This constitutes -another, albeit weak heuristic that is not restricted to induction: -\begin{quote} - \emph{The right-hand side of an equation should (in some sense) be simpler - than the left-hand side.} -\end{quote} -This heuristic is tricky to apply because it is not obvious that -@{term"rev xs @ ys"} is simpler than @{term"itrev xs ys"}. But see what -happens if you try to prove @{prop"rev xs @ ys = itrev xs ys"}! - -If you have tried these heuristics and still find your -induction does not go through, and no obvious lemma suggests itself, you may -need to generalize your proposition even further. This requires insight into -the problem at hand and is beyond simple rules of thumb. -Additionally, you can read \S\ref{sec:advanced-ind} -to learn about some advanced techniques for inductive proofs.% -\index{induction heuristics|)} -*} -(*<*) -declare [[names_unique = true]] -end -(*>*)