(*<*) theoryInductionimports examples simplification begin (*>*)
text‹
we have defined our function such that Isabelle could prove
and that the recursion equations (or some suitable derived
) are simplification rules, we might like to prove something about
function. Since the function is recursive, the natural proof principle is
induction. But this time the structural form of induction that comes
datatypes is unlikely to work well --- otherwise we could have defined the
by \isacommand{primrec}. Therefore \isacommand{recdef} automatically
a suitable induction rule $f$‹.induct› that follows the
pattern of the particular function $f$. We call this
textbf{recursion induction}. Roughly speaking, it
you to prove for each \isacommand{recdef} equation that the property
are trying to establish holds for the left-hand side provided it holds
all recursive calls on the right-hand side. Here is a simple example
the predefined @{term"map"} functional on lists: ›
lemma"map f (sep(x,xs)) = sep(f x, map f xs)"
txt‹\noindent
that @{term"map f xs"}
the result of applying @{term"f"} to all elements of @{term"xs"}. We prove
lemma by recursion induction over @{term"sep"}: ›
apply(induct_tac x xs rule: sep.induct)
txt‹\noindent
resulting proof state has three subgoals corresponding to the three
for @{term"sep"}:
{subgoals[display,indent=0]}
rest is pure simplification: ›
apply simp_all done
text‹
proving the above lemma by structural induction, and you find that you
an additional case distinction. What is worse, the names of variables
invented by Isabelle and have nothing to do with the names in the
of @{term"sep"}.
general, the format of invoking recursion induction is
begin{quote}
isacommand{apply}‹(induct_tac› $x@1 \dots x@n$ ‹rule:› $f$‹.induct)›
end{quote}\index{*induct_tac (method)}%
$x@1~\dots~x@n$ is a list of free variables in the subgoal and $f$ the
of a function that takes an $n$-tuple. Usually the subgoal will
the term $f(x@1,\dots,x@n)$ but this need not be the case. The
rules do not mention $f$ at all. Here is @{thm[source]sep.induct}:
begin{isabelle} \isasymlbrakk}~{\isasymAnd}a.~P~a~[];\isanewline
~{\isasymAnd}a~x.~P~a~[x];\isanewline
~{\isasymAnd}a~x~y~zs.~P~a~(y~\#~zs)~{\isasymLongrightarrow}~P~a~(x~\#~y~\#~zs){\isasymrbrakk}\isanewline \isasymLongrightarrow}~P~u~v%
end{isabelle}
merely says that in order to prove a property @{term"P"} of @{term"u"} and
{term"v"} you need to prove it for the three cases where @{term"v"} is the
list, the singleton list, and the list with at least two elements.
final case has an induction hypothesis: you may assume that @{term"P"}
for the tail of that list. ›
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.
