src/Doc/Tutorial/Misc/Itrev.thy
 author wenzelm Tue Aug 28 18:57:32 2012 +0200 (2012-08-28) changeset 48985 5386df44a037 parent 42669 doc-src/TutorialI/Misc/Itrev.thy@04dfffda5671 child 58860 fee7cfa69c50 permissions -rw-r--r--
renamed doc-src to src/Doc;
renamed TutorialI to Tutorial;
 nipkow@8745  1 (*<*)  nipkow@17326  2 theory Itrev  nipkow@17326  3 imports Main  nipkow@17326  4 begin  wenzelm@42669  5 declare [[names_unique = false]]  nipkow@8745  6 (*>*)  nipkow@8745  7 paulson@10885  8 section{*Induction Heuristics*}  nipkow@9844  9 nipkow@9844  10 text{*\label{sec:InductionHeuristics}  paulson@11458  11 \index{induction heuristics|(}%  nipkow@9844  12 The purpose of this section is to illustrate some simple heuristics for  nipkow@9844  13 inductive proofs. The first one we have already mentioned in our initial  nipkow@9844  14 example:  nipkow@9844  15 \begin{quote}  nipkow@9844  16 \emph{Theorems about recursive functions are proved by induction.}  nipkow@9844  17 \end{quote}  nipkow@9844  18 In case the function has more than one argument  nipkow@9844  19 \begin{quote}  nipkow@9844  20 \emph{Do induction on argument number $i$ if the function is defined by  nipkow@9844  21 recursion in argument number $i$.}  nipkow@9844  22 \end{quote}  paulson@11458  23 When we look at the proof of @{text"(xs@ys) @ zs = xs @ (ys@zs)"}  paulson@11458  24 in \S\ref{sec:intro-proof} we find  paulson@11458  25 \begin{itemize}  paulson@11458  26 \item @{text"@"} is recursive in  paulson@11458  27 the first argument  paulson@11458  28 \item @{term xs} occurs only as the first argument of  paulson@11458  29 @{text"@"}  paulson@11458  30 \item both @{term ys} and @{term zs} occur at least once as  paulson@11458  31 the second argument of @{text"@"}  paulson@11458  32 \end{itemize}  paulson@11458  33 Hence it is natural to perform induction on~@{term xs}.  nipkow@9844  34 nipkow@9844  35 The key heuristic, and the main point of this section, is to  paulson@11458  36 \emph{generalize the goal before induction}.  paulson@11458  37 The reason is simple: if the goal is  nipkow@9844  38 too specific, the induction hypothesis is too weak to allow the induction  nipkow@10971  39 step to go through. Let us illustrate the idea with an example.  nipkow@9844  40 paulson@11458  41 Function \cdx{rev} has quadratic worst-case running time  nipkow@9792  42 because it calls function @{text"@"} for each element of the list and  nipkow@9792  43 @{text"@"} is linear in its first argument. A linear time version of  nipkow@9754  44 @{term"rev"} reqires an extra argument where the result is accumulated  paulson@11458  45 gradually, using only~@{text"#"}:  nipkow@9754  46 *}  nipkow@8745  47 nipkow@27015  48 primrec itrev :: "'a list \ 'a list \ 'a list" where  nipkow@27015  49 "itrev [] ys = ys" |  nipkow@27015  50 "itrev (x#xs) ys = itrev xs (x#ys)"  nipkow@8745  51 nipkow@9754  52 text{*\noindent  paulson@11458  53 The behaviour of \cdx{itrev} is simple: it reverses  nipkow@9493  54 its first argument by stacking its elements onto the second argument,  nipkow@9493  55 and returning that second argument when the first one becomes  paulson@11458  56 empty. Note that @{term"itrev"} is tail-recursive: it can be  nipkow@9493  57 compiled into a loop.  nipkow@9493  58 nipkow@9754  59 Naturally, we would like to show that @{term"itrev"} does indeed reverse  nipkow@9754  60 its first argument provided the second one is empty:  nipkow@9754  61 *};  nipkow@8745  62 nipkow@8745  63 lemma "itrev xs [] = rev xs";  nipkow@8745  64 nipkow@8745  65 txt{*\noindent  nipkow@8745  66 There is no choice as to the induction variable, and we immediately simplify:  nipkow@9458  67 *};  nipkow@8745  68 nipkow@9689  69 apply(induct_tac xs, simp_all);  nipkow@8745  70 nipkow@8745  71 txt{*\noindent  paulson@11458  72 Unfortunately, this attempt does not prove  paulson@11458  73 the induction step:  nipkow@10971  74 @{subgoals[display,indent=0,margin=70]}  paulson@11458  75 The induction hypothesis is too weak. The fixed  paulson@11458  76 argument,~@{term"[]"}, prevents it from rewriting the conclusion.  paulson@11458  77 This example suggests a heuristic:  paulson@11458  78 \begin{quote}\index{generalizing induction formulae}%  nipkow@9754  79 \emph{Generalize goals for induction by replacing constants by variables.}  nipkow@8745  80 \end{quote}  nipkow@9754  81 Of course one cannot do this na\"{\i}vely: @{term"itrev xs ys = rev xs"} is  paulson@11458  82 just not true. The correct generalization is  nipkow@9458  83 *};  nipkow@8745  84 (*<*)oops;(*>*)  nipkow@8745  85 lemma "itrev xs ys = rev xs @ ys";  nipkow@10362  86 (*<*)apply(induct_tac xs, simp_all)(*>*)  nipkow@8745  87 txt{*\noindent  nipkow@9754  88 If @{term"ys"} is replaced by @{term"[]"}, the right-hand side simplifies to  paulson@11458  89 @{term"rev xs"}, as required.  nipkow@8745  90 paulson@11458  91 In this instance it was easy to guess the right generalization.  paulson@11458  92 Other situations can require a good deal of creativity.  nipkow@8745  93 nipkow@9754  94 Although we now have two variables, only @{term"xs"} is suitable for  paulson@11458  95 induction, and we repeat our proof attempt. Unfortunately, we are still  nipkow@8745  96 not there:  nipkow@10362  97 @{subgoals[display,indent=0,goals_limit=1]}  nipkow@8745  98 The induction hypothesis is still too weak, but this time it takes no  nipkow@9754  99 intuition to generalize: the problem is that @{term"ys"} is fixed throughout  nipkow@8745  100 the subgoal, but the induction hypothesis needs to be applied with  nipkow@9754  101 @{term"a # ys"} instead of @{term"ys"}. Hence we prove the theorem  nipkow@9754  102 for all @{term"ys"} instead of a fixed one:  nipkow@9458  103 *};  nipkow@8745  104 (*<*)oops;(*>*)  nipkow@10362  105 lemma "\ys. itrev xs ys = rev xs @ ys";  nipkow@9844  106 (*<*)  nipkow@9844  107 by(induct_tac xs, simp_all);  nipkow@9844  108 (*>*)  nipkow@8745  109 nipkow@9844  110 text{*\noindent  nipkow@9754  111 This time induction on @{term"xs"} followed by simplification succeeds. This  nipkow@8745  112 leads to another heuristic for generalization:  nipkow@8745  113 \begin{quote}  nipkow@9754  114 \emph{Generalize goals for induction by universally quantifying all free  nipkow@8745  115 variables {\em(except the induction variable itself!)}.}  nipkow@8745  116 \end{quote}  paulson@11458  117 This prevents trivial failures like the one above and does not affect the  paulson@11458  118 validity of the goal. However, this heuristic should not be applied blindly.  paulson@11458  119 It is not always required, and the additional quantifiers can complicate  nipkow@13081  120 matters in some cases. The variables that should be quantified are typically  paulson@11458  121 those that change in recursive calls.  nipkow@9644  122 nipkow@9844  123 A final point worth mentioning is the orientation of the equation we just  haftmann@15905  124 proved: the more complex notion (@{const itrev}) is on the left-hand  nipkow@9844  125 side, the simpler one (@{term rev}) on the right-hand side. This constitutes  nipkow@9844  126 another, albeit weak heuristic that is not restricted to induction:  nipkow@9844  127 \begin{quote}  nipkow@9844  128  \emph{The right-hand side of an equation should (in some sense) be simpler  nipkow@9844  129  than the left-hand side.}  nipkow@9844  130 \end{quote}  nipkow@9844  131 This heuristic is tricky to apply because it is not obvious that  nipkow@9844  132 @{term"rev xs @ ys"} is simpler than @{term"itrev xs ys"}. But see what  nipkow@9844  133 happens if you try to prove @{prop"rev xs @ ys = itrev xs ys"}!  nipkow@10971  134 paulson@11458  135 If you have tried these heuristics and still find your  nipkow@10971  136 induction does not go through, and no obvious lemma suggests itself, you may  nipkow@10971  137 need to generalize your proposition even further. This requires insight into  paulson@11458  138 the problem at hand and is beyond simple rules of thumb.  paulson@11458  139 Additionally, you can read \S\ref{sec:advanced-ind}  paulson@11458  140 to learn about some advanced techniques for inductive proofs.%  paulson@11458  141 \index{induction heuristics|)}  nipkow@9844  142 *}  nipkow@8745  143 (*<*)  wenzelm@42669  144 declare [[names_unique = true]]  nipkow@8745  145 end  nipkow@8745  146 (*>*)