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