Quelle Itrev.thy

Sprache: Isabelle

(*<*)
theory Itrev
imports Main
begin
declare [[names_unique = false]]
(*>*)

section‹Induction Heuristics›

text‹\label{sec:InductionHeuristics}
index{induction heuristics|(}%
purpose of this section is to illustrate some simple heuristics for
proofs. The first one we have already mentioned in our initial
:
begin{quote}
emph{Theorems about recursive functions are proved by induction.}
end{quote}
case the function has more than one argument
begin{quote}
emph{Do induction on argument number $i$ if the function is defined by
in argument number $i$.}
end{quote}
we look at the proof of ‹(xs@ys) @ zs = xs @ (ys@zs)›
\S\ref{sec:intro-proof} we find
begin{itemize}
item ‹@› is recursive in
first argument
item term‹xs› occurs only as the first argument of
‹@›
item both term‹ys› and term‹zs› occur at least once as
second argument of ‹@›
end{itemize}
it is natural to perform induction on~term‹xs›.

key heuristic, and the main point of this section, is to
emph{generalize the goal before induction}.
reason is simple: if the goal is
specific, the induction hypothesis is too weak to allow the induction
to go through. Let us illustrate the idea with an example.

\cdx{rev} has quadratic worst-case running time
it calls function ‹@› for each element of the list and
‹@› is linear in its first argument. A linear time version of
term‹rev› reqires an extra argument where the result is accumulated
, using only~‹#›:
›

primrec itrev :: "'a list ==> 'a list ==> 'a list" where
"itrev [] ys = ys" |
"itrev (x#xs) ys = itrev xs (x#ys)"

text‹\noindent
behaviour of \cdx{itrev} is simple: it reverses
first argument by stacking its elements onto the second argument,
returning that second argument when the first one becomes
. Note that term‹itrev› is tail-recursive: it can be
into a loop.

, we would like to show that term‹itrev› does indeed reverse
first argument provided the second one is empty:
›

lemma "itrev xs [] = rev xs"

txt‹\noindent
is no choice as to the induction variable, and we immediately simplify:
›

apply(induct_tac xs, simp_all)

txt‹\noindent
, this attempt does not prove
induction step:
{subgoals[display,indent=0,margin=70]}
induction hypothesis is too weak. The fixed
,~term‹[]›, prevents it from rewriting the conclusion.
example suggests a heuristic:
begin{quote}\index{generalizing induction formulae}%
emph{Generalize goals for induction by replacing constants by variables.}
end{quote}
course one cannot do this na\"{\i}vely: term‹itrev xs ys = rev xs› is
not true. The correct generalization is
›
(*<*)oops(*>*)
lemma "itrev xs ys = rev xs @ ys"
(*<*)apply(induct_tac xs, simp_all)(*>*)
txt‹\noindent
term‹ys› is replaced by term‹[]›, the right-hand side simplifies to
term‹rev xs›, as required.

this instance it was easy to guess the right generalization.
situations can require a good deal of creativity.

we now have two variables, only term‹xs› is suitable for
, and we repeat our proof attempt. Unfortunately, we are still
there:
{subgoals[display,indent=0,goals_limit=1]}
induction hypothesis is still too weak, but this time it takes no
to generalize: the problem is that term‹ys› is fixed throughout
subgoal, but the induction hypothesis needs to be applied with
term‹a # ys› instead of term‹ys›. Hence we prove the theorem
all term‹ys› instead of a fixed one:
›
(*<*)oops(*>*)
lemma "∀ys. itrev xs ys = rev xs @ ys"
(*<*)
by(induct_tac xs, simp_all)
(*>*)

text‹\noindent
time induction on term‹xs› followed by simplification succeeds. This
to another heuristic for generalization:
begin{quote}
emph{Generalize goals for induction by universally quantifying all free
{\em(except the induction variable itself!)}.}
end{quote}
prevents trivial failures like the one above and does not affect the
of the goal. However, this heuristic should not be applied blindly.
is not always required, and the additional quantifiers can complicate
in some cases. The variables that should be quantified are typically
that change in recursive calls.

final point worth mentioning is the orientation of the equation we just
: the more complex notion (const‹itrev›) is on the left-hand
, the simpler one (term‹rev›) on the right-hand side. This constitutes
, albeit weak heuristic that is not restricted to induction:
begin{quote}
\emph{The right-hand side of an equation should (in some sense) be simpler
than the left-hand side.}
end{quote}
heuristic is tricky to apply because it is not obvious that
term‹rev xs @ ys› is simpler than term‹itrev xs ys›. But see what
if you try to prove prop‹rev xs @ ys = itrev xs ys›!

you have tried these heuristics and still find your
does not go through, and no obvious lemma suggests itself, you may
to generalize your proposition even further. This requires insight into
problem at hand and is beyond simple rules of thumb.
, you can read \S\ref{sec:advanced-ind}
learn about some advanced techniques for inductive proofs.%
index{induction heuristics|)}
›
(*<*)
declare [[names_unique = true]]
end
(*>*)

Messung V0.5 in Prozent

¤ Dauer der Verarbeitung: 0.15 Sekunden (vorverarbeitet am 2026-06-10) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung und die Messung sind noch experimentell.