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.48 +gradually, using only~@{text"#"}:
    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.  
   1.142 +Additionally, you can read \S\ref{sec:advanced-ind}
   1.143 +to learn about some advanced techniques for inductive proofs.%
   1.144 +\index{induction heuristics|)}
   1.145 +*}
   1.146 +(*<*)
   1.147 +declare [[names_unique = true]]
   1.148 +end
   1.149 +(*>*)