1.1 --- a/doc-src/TutorialI/Misc/Itrev.thy	Tue Sep 05 13:12:00 2000 +0200
     1.2 +++ b/doc-src/TutorialI/Misc/Itrev.thy	Tue Sep 05 13:53:39 2000 +0200
     1.3 @@ -2,7 +2,32 @@
     1.4  theory Itrev = Main:;
     1.5  (*>*)
     1.6  
     1.7 -text{*
     1.8 +section{*Induction heuristics*}
     1.9 +
    1.10 +text{*\label{sec:InductionHeuristics}
    1.11 +The purpose of this section is to illustrate some simple heuristics for
    1.12 +inductive proofs. The first one we have already mentioned in our initial
    1.13 +example:
    1.14 +\begin{quote}
    1.15 +\emph{Theorems about recursive functions are proved by induction.}
    1.16 +\end{quote}
    1.17 +In case the function has more than one argument
    1.18 +\begin{quote}
    1.19 +\emph{Do induction on argument number $i$ if the function is defined by
    1.20 +recursion in argument number $i$.}
    1.21 +\end{quote}
    1.22 +When we look at the proof of @{term[source]"(xs @ ys) @ zs = xs @ (ys @ zs)"}
    1.23 +in \S\ref{sec:intro-proof} we find (a) @{text"@"} is recursive in
    1.24 +the first argument, (b) @{term xs} occurs only as the first argument of
    1.25 +@{text"@"}, and (c) both @{term ys} and @{term zs} occur at least once as
    1.26 +the second argument of @{text"@"}. Hence it is natural to perform induction
    1.27 +on @{term xs}.
    1.28 +
    1.29 +The key heuristic, and the main point of this section, is to
    1.30 +generalize the goal before induction. The reason is simple: if the goal is
    1.31 +too specific, the induction hypothesis is too weak to allow the induction
    1.32 +step to go through. Let us now illustrate the idea with an example.
    1.33 +
    1.34  Function @{term"rev"} has quadratic worst-case running time
    1.35  because it calls function @{text"@"} for each element of the list and
    1.36  @{text"@"} is linear in its first argument.  A linear time version of
    1.37 @@ -36,7 +61,7 @@
    1.38  
    1.39  txt{*\noindent
    1.40  Unfortunately, this is not a complete success:
    1.41 -\begin{isabelle}
    1.42 +\begin{isabelle}\makeatother
    1.43  ~1.~\dots~itrev~list~[]~=~rev~list~{\isasymLongrightarrow}~itrev~list~[a]~=~rev~list~@~[a]%
    1.44  \end{isabelle}
    1.45  Just as predicted above, the overall goal, and hence the induction
    1.46 @@ -62,7 +87,7 @@
    1.47  Although we now have two variables, only @{term"xs"} is suitable for
    1.48  induction, and we repeat our above proof attempt. Unfortunately, we are still
    1.49  not there:
    1.50 -\begin{isabelle}
    1.51 +\begin{isabelle}\makeatother
    1.52  ~1.~{\isasymAnd}a~list.\isanewline
    1.53  ~~~~~~~itrev~list~ys~=~rev~list~@~ys~{\isasymLongrightarrow}\isanewline
    1.54  ~~~~~~~itrev~list~(a~\#~ys)~=~rev~list~@~a~\#~ys
    1.55 @@ -75,8 +100,11 @@
    1.56  *};
    1.57  (*<*)oops;(*>*)
    1.58  lemma "\\<forall>ys. itrev xs ys = rev xs @ ys";
    1.59 +(*<*)
    1.60 +by(induct_tac xs, simp_all);
    1.61 +(*>*)
    1.62  
    1.63 -txt{*\noindent
    1.64 +text{*\noindent
    1.65  This time induction on @{term"xs"} followed by simplification succeeds. This
    1.66  leads to another heuristic for generalization:
    1.67  \begin{quote}
    1.68 @@ -94,9 +122,19 @@
    1.69  the problem at hand and is beyond simple rules of thumb. In a nutshell: you
    1.70  will need to be creative. Additionally, you can read \S\ref{sec:advanced-ind}
    1.71  to learn about some advanced techniques for inductive proofs.
    1.72 -*};
    1.73  
    1.74 +A final point worth mentioning is the orientation of the equation we just
    1.75 +proved: the more complex notion (@{term itrev}) is on the left-hand
    1.76 +side, the simpler one (@{term rev}) on the right-hand side. This constitutes
    1.77 +another, albeit weak heuristic that is not restricted to induction:
    1.78 +\begin{quote}
    1.79 +  \emph{The right-hand side of an equation should (in some sense) be simpler
    1.80 +    than the left-hand side.}
    1.81 +\end{quote}
    1.82 +This heuristic is tricky to apply because it is not obvious that
    1.83 +@{term"rev xs @ ys"} is simpler than @{term"itrev xs ys"}. But see what
    1.84 +happens if you try to prove @{prop"rev xs @ ys = itrev xs ys"}!
    1.85 +*}
    1.86  (*<*)
    1.87 -by(induct_tac xs, simp_all);
    1.88  end
    1.89  (*>*)