8749
|
1 |
\begin{isabelle}%
|
|
2 |
%
|
|
3 |
\begin{isamarkuptext}%
|
|
4 |
Assuming we have defined our function such that Isabelle could prove
|
|
5 |
termination and that the recursion equations (or some suitable derived
|
|
6 |
equations) are simplification rules, we might like to prove something about
|
|
7 |
our function. Since the function is recursive, the natural proof principle is
|
|
8 |
again induction. But this time the structural form of induction that comes
|
|
9 |
with datatypes is unlikely to work well---otherwise we could have defined the
|
|
10 |
function by \isacommand{primrec}. Therefore \isacommand{recdef} automatically
|
|
11 |
proves a suitable induction rule $f$\isa{.induct} that follows the
|
|
12 |
recursion pattern of the particular function $f$. We call this
|
|
13 |
\textbf{recursion induction}. Roughly speaking, it
|
|
14 |
requires you to prove for each \isacommand{recdef} equation that the property
|
|
15 |
you are trying to establish holds for the left-hand side provided it holds
|
8771
|
16 |
for all recursive calls on the right-hand side. Here is a simple example%
|
8749
|
17 |
\end{isamarkuptext}%
|
9674
|
18 |
\isacommand{lemma}\ {\isachardoublequote}map\ f\ {\isacharparenleft}sep{\isacharparenleft}x{\isacharcomma}xs{\isacharparenright}{\isacharparenright}\ {\isacharequal}\ sep{\isacharparenleft}f\ x{\isacharcomma}\ map\ f\ xs{\isacharparenright}{\isachardoublequote}%
|
8749
|
19 |
\begin{isamarkuptxt}%
|
|
20 |
\noindent
|
|
21 |
involving the predefined \isa{map} functional on lists: \isa{map f xs}
|
|
22 |
is the result of applying \isa{f} to all elements of \isa{xs}. We prove
|
|
23 |
this lemma by recursion induction w.r.t. \isa{sep}:%
|
|
24 |
\end{isamarkuptxt}%
|
9674
|
25 |
\isacommand{apply}{\isacharparenleft}induct{\isacharunderscore}tac\ x\ xs\ rule{\isacharcolon}\ sep{\isachardot}induct{\isacharparenright}%
|
8749
|
26 |
\begin{isamarkuptxt}%
|
|
27 |
\noindent
|
|
28 |
The resulting proof state has three subgoals corresponding to the three
|
|
29 |
clauses for \isa{sep}:
|
|
30 |
\begin{isabellepar}%
|
|
31 |
~1.~{\isasymAnd}a.~map~f~(sep~(a,~[]))~=~sep~(f~a,~map~f~[])\isanewline
|
|
32 |
~2.~{\isasymAnd}a~x.~map~f~(sep~(a,~[x]))~=~sep~(f~a,~map~f~[x])\isanewline
|
|
33 |
~3.~{\isasymAnd}a~x~y~zs.\isanewline
|
|
34 |
~~~~~~~map~f~(sep~(a,~y~\#~zs))~=~sep~(f~a,~map~f~(y~\#~zs))~{\isasymLongrightarrow}\isanewline
|
|
35 |
~~~~~~~map~f~(sep~(a,~x~\#~y~\#~zs))~=~sep~(f~a,~map~f~(x~\#~y~\#~zs))%
|
|
36 |
\end{isabellepar}%
|
|
37 |
The rest is pure simplification:%
|
|
38 |
\end{isamarkuptxt}%
|
9541
|
39 |
\isacommand{by}\ auto%
|
8749
|
40 |
\begin{isamarkuptext}%
|
|
41 |
Try proving the above lemma by structural induction, and you find that you
|
|
42 |
need an additional case distinction. What is worse, the names of variables
|
|
43 |
are invented by Isabelle and have nothing to do with the names in the
|
|
44 |
definition of \isa{sep}.
|
|
45 |
|
|
46 |
In general, the format of invoking recursion induction is
|
|
47 |
\begin{ttbox}
|
|
48 |
apply(induct_tac \(x@1 \dots x@n\) rule: \(f\).induct)
|
|
49 |
\end{ttbox}\index{*induct_tac}%
|
|
50 |
where $x@1~\dots~x@n$ is a list of free variables in the subgoal and $f$ the
|
|
51 |
name of a function that takes an $n$-tuple. Usually the subgoal will
|
|
52 |
contain the term $f~x@1~\dots~x@n$ but this need not be the case. The
|
|
53 |
induction rules do not mention $f$ at all. For example \isa{sep.induct}
|
|
54 |
\begin{isabellepar}%
|
|
55 |
{\isasymlbrakk}~{\isasymAnd}a.~?P~a~[];\isanewline
|
|
56 |
~~{\isasymAnd}a~x.~?P~a~[x];\isanewline
|
|
57 |
~~{\isasymAnd}a~x~y~zs.~?P~a~(y~\#~zs)~{\isasymLongrightarrow}~?P~a~(x~\#~y~\#~zs){\isasymrbrakk}\isanewline
|
|
58 |
{\isasymLongrightarrow}~?P~?u~?v%
|
|
59 |
\end{isabellepar}%
|
|
60 |
merely says that in order to prove a property \isa{?P} of \isa{?u} and
|
|
61 |
\isa{?v} you need to prove it for the three cases where \isa{?v} is the
|
|
62 |
empty list, the singleton list, and the list with at least two elements
|
|
63 |
(in which case you may assume it holds for the tail of that list).%
|
|
64 |
\end{isamarkuptext}%
|
|
65 |
\end{isabelle}%
|
9145
|
66 |
%%% Local Variables:
|
|
67 |
%%% mode: latex
|
|
68 |
%%% TeX-master: "root"
|
|
69 |
%%% End:
|