1 (*<*) |
|
2 theory Induction imports examples simplification begin; |
|
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$@{text".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 involving the predefined @{term"map"} functional on lists: |
|
20 *} |
|
21 |
|
22 lemma "map f (sep(x,xs)) = sep(f x, map f xs)"; |
|
23 |
|
24 txt{*\noindent |
|
25 Note that @{term"map f xs"} |
|
26 is the result of applying @{term"f"} to all elements of @{term"xs"}. We prove |
|
27 this lemma by recursion induction over @{term"sep"}: |
|
28 *} |
|
29 |
|
30 apply(induct_tac x xs rule: sep.induct); |
|
31 |
|
32 txt{*\noindent |
|
33 The resulting proof state has three subgoals corresponding to the three |
|
34 clauses for @{term"sep"}: |
|
35 @{subgoals[display,indent=0]} |
|
36 The rest is pure simplification: |
|
37 *} |
|
38 |
|
39 apply simp_all; |
|
40 done |
|
41 |
|
42 text{* |
|
43 Try proving the above lemma by structural induction, and you find that you |
|
44 need an additional case distinction. What is worse, the names of variables |
|
45 are invented by Isabelle and have nothing to do with the names in the |
|
46 definition of @{term"sep"}. |
|
47 |
|
48 In general, the format of invoking recursion induction is |
|
49 \begin{quote} |
|
50 \isacommand{apply}@{text"(induct_tac"} $x@1 \dots x@n$ @{text"rule:"} $f$@{text".induct)"} |
|
51 \end{quote}\index{*induct_tac (method)}% |
|
52 where $x@1~\dots~x@n$ is a list of free variables in the subgoal and $f$ the |
|
53 name of a function that takes an $n$-tuple. Usually the subgoal will |
|
54 contain the term $f(x@1,\dots,x@n)$ but this need not be the case. The |
|
55 induction rules do not mention $f$ at all. Here is @{thm[source]sep.induct}: |
|
56 \begin{isabelle} |
|
57 {\isasymlbrakk}~{\isasymAnd}a.~P~a~[];\isanewline |
|
58 ~~{\isasymAnd}a~x.~P~a~[x];\isanewline |
|
59 ~~{\isasymAnd}a~x~y~zs.~P~a~(y~\#~zs)~{\isasymLongrightarrow}~P~a~(x~\#~y~\#~zs){\isasymrbrakk}\isanewline |
|
60 {\isasymLongrightarrow}~P~u~v% |
|
61 \end{isabelle} |
|
62 It merely says that in order to prove a property @{term"P"} of @{term"u"} and |
|
63 @{term"v"} you need to prove it for the three cases where @{term"v"} is the |
|
64 empty list, the singleton list, and the list with at least two elements. |
|
65 The final case has an induction hypothesis: you may assume that @{term"P"} |
|
66 holds for the tail of that list. |
|
67 *} |
|
68 |
|
69 (*<*) |
|
70 end |
|
71 (*>*) |
|