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 \<Rightarrow> 'a list \<Rightarrow> '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 "\<forall>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
(*>*)