src/Doc/Tutorial/Misc/Itrev.thy
 changeset 48985 5386df44a037 parent 42669 04dfffda5671 child 58860 fee7cfa69c50
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
1.2 +++ b/src/Doc/Tutorial/Misc/Itrev.thy	Tue Aug 28 18:57:32 2012 +0200
1.3 @@ -0,0 +1,146 @@
1.4 +(*<*)
1.5 +theory Itrev
1.6 +imports Main
1.7 +begin
1.8 +declare [[names_unique = false]]
1.9 +(*>*)
1.10 +
1.11 +section{*Induction Heuristics*}
1.12 +
1.13 +text{*\label{sec:InductionHeuristics}
1.14 +\index{induction heuristics|(}%
1.15 +The purpose of this section is to illustrate some simple heuristics for
1.16 +inductive proofs. The first one we have already mentioned in our initial
1.17 +example:
1.18 +\begin{quote}
1.19 +\emph{Theorems about recursive functions are proved by induction.}
1.20 +\end{quote}
1.21 +In case the function has more than one argument
1.22 +\begin{quote}
1.23 +\emph{Do induction on argument number $i$ if the function is defined by
1.24 +recursion in argument number $i$.}
1.25 +\end{quote}
1.26 +When we look at the proof of @{text"(xs@ys) @ zs = xs @ (ys@zs)"}
1.27 +in \S\ref{sec:intro-proof} we find
1.28 +\begin{itemize}
1.29 +\item @{text"@"} is recursive in
1.30 +the first argument
1.31 +\item @{term xs}  occurs only as the first argument of
1.32 +@{text"@"}
1.33 +\item both @{term ys} and @{term zs} occur at least once as
1.34 +the second argument of @{text"@"}
1.35 +\end{itemize}
1.36 +Hence it is natural to perform induction on~@{term xs}.
1.37 +
1.38 +The key heuristic, and the main point of this section, is to
1.39 +\emph{generalize the goal before induction}.
1.40 +The reason is simple: if the goal is
1.41 +too specific, the induction hypothesis is too weak to allow the induction
1.42 +step to go through. Let us illustrate the idea with an example.
1.43 +
1.44 +Function \cdx{rev} has quadratic worst-case running time
1.45 +because it calls function @{text"@"} for each element of the list and
1.46 +@{text"@"} is linear in its first argument.  A linear time version of
1.47 +@{term"rev"} reqires an extra argument where the result is accumulated
1.49 +*}
1.50 +
1.51 +primrec itrev :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list" where
1.52 +"itrev []     ys = ys" |
1.53 +"itrev (x#xs) ys = itrev xs (x#ys)"
1.54 +
1.55 +text{*\noindent
1.56 +The behaviour of \cdx{itrev} is simple: it reverses
1.57 +its first argument by stacking its elements onto the second argument,
1.58 +and returning that second argument when the first one becomes
1.59 +empty. Note that @{term"itrev"} is tail-recursive: it can be
1.60 +compiled into a loop.
1.61 +
1.62 +Naturally, we would like to show that @{term"itrev"} does indeed reverse
1.63 +its first argument provided the second one is empty:
1.64 +*};
1.65 +
1.66 +lemma "itrev xs [] = rev xs";
1.67 +
1.68 +txt{*\noindent
1.69 +There is no choice as to the induction variable, and we immediately simplify:
1.70 +*};
1.71 +
1.72 +apply(induct_tac xs, simp_all);
1.73 +
1.74 +txt{*\noindent
1.75 +Unfortunately, this attempt does not prove
1.76 +the induction step:
1.77 +@{subgoals[display,indent=0,margin=70]}
1.78 +The induction hypothesis is too weak.  The fixed
1.79 +argument,~@{term"[]"}, prevents it from rewriting the conclusion.
1.80 +This example suggests a heuristic:
1.81 +\begin{quote}\index{generalizing induction formulae}%
1.82 +\emph{Generalize goals for induction by replacing constants by variables.}
1.83 +\end{quote}
1.84 +Of course one cannot do this na\"{\i}vely: @{term"itrev xs ys = rev xs"} is
1.85 +just not true.  The correct generalization is
1.86 +*};
1.87 +(*<*)oops;(*>*)
1.88 +lemma "itrev xs ys = rev xs @ ys";
1.89 +(*<*)apply(induct_tac xs, simp_all)(*>*)
1.90 +txt{*\noindent
1.91 +If @{term"ys"} is replaced by @{term"[]"}, the right-hand side simplifies to
1.92 +@{term"rev xs"}, as required.
1.93 +
1.94 +In this instance it was easy to guess the right generalization.
1.95 +Other situations can require a good deal of creativity.
1.96 +
1.97 +Although we now have two variables, only @{term"xs"} is suitable for
1.98 +induction, and we repeat our proof attempt. Unfortunately, we are still
1.99 +not there:
1.100 +@{subgoals[display,indent=0,goals_limit=1]}
1.101 +The induction hypothesis is still too weak, but this time it takes no
1.102 +intuition to generalize: the problem is that @{term"ys"} is fixed throughout
1.103 +the subgoal, but the induction hypothesis needs to be applied with
1.104 +@{term"a # ys"} instead of @{term"ys"}. Hence we prove the theorem
1.105 +for all @{term"ys"} instead of a fixed one:
1.106 +*};
1.107 +(*<*)oops;(*>*)
1.108 +lemma "\<forall>ys. itrev xs ys = rev xs @ ys";
1.109 +(*<*)
1.110 +by(induct_tac xs, simp_all);
1.111 +(*>*)
1.112 +
1.113 +text{*\noindent
1.114 +This time induction on @{term"xs"} followed by simplification succeeds. This
1.115 +leads to another heuristic for generalization:
1.116 +\begin{quote}
1.117 +\emph{Generalize goals for induction by universally quantifying all free
1.118 +variables {\em(except the induction variable itself!)}.}
1.119 +\end{quote}
1.120 +This prevents trivial failures like the one above and does not affect the
1.121 +validity of the goal.  However, this heuristic should not be applied blindly.
1.122 +It is not always required, and the additional quantifiers can complicate
1.123 +matters in some cases. The variables that should be quantified are typically
1.124 +those that change in recursive calls.
1.125 +
1.126 +A final point worth mentioning is the orientation of the equation we just
1.127 +proved: the more complex notion (@{const itrev}) is on the left-hand
1.128 +side, the simpler one (@{term rev}) on the right-hand side. This constitutes
1.129 +another, albeit weak heuristic that is not restricted to induction:
1.130 +\begin{quote}
1.131 +  \emph{The right-hand side of an equation should (in some sense) be simpler
1.132 +    than the left-hand side.}
1.133 +\end{quote}
1.134 +This heuristic is tricky to apply because it is not obvious that
1.135 +@{term"rev xs @ ys"} is simpler than @{term"itrev xs ys"}. But see what
1.136 +happens if you try to prove @{prop"rev xs @ ys = itrev xs ys"}!
1.137 +
1.138 +If you have tried these heuristics and still find your
1.139 +induction does not go through, and no obvious lemma suggests itself, you may
1.140 +need to generalize your proposition even further. This requires insight into
1.141 +the problem at hand and is beyond simple rules of thumb.