8 equations) are simplification rules, we might like to prove something about |
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 |
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 |
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 |
11 with datatypes is unlikely to work well---otherwise we could have defined the |
12 function by \isacommand{primrec}. Therefore \isacommand{recdef} automatically |
12 function by \isacommand{primrec}. Therefore \isacommand{recdef} automatically |
13 proves a suitable induction rule $f$\isa{.induct} that follows the |
13 proves a suitable induction rule $f$@{text".induct"} that follows the |
14 recursion pattern of the particular function $f$. We call this |
14 recursion pattern of the particular function $f$. We call this |
15 \textbf{recursion induction}. Roughly speaking, it |
15 \textbf{recursion induction}. Roughly speaking, it |
16 requires you to prove for each \isacommand{recdef} equation that the property |
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 |
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 |
18 for all recursive calls on the right-hand side. Here is a simple example |
19 *} |
19 *} |
20 |
20 |
21 lemma "map f (sep(x,xs)) = sep(f x, map f xs)"; |
21 lemma "map f (sep(x,xs)) = sep(f x, map f xs)"; |
22 |
22 |
23 txt{*\noindent |
23 txt{*\noindent |
24 involving the predefined \isa{map} functional on lists: \isa{map f xs} |
24 involving the predefined @{term"map"} functional on lists: @{term"map f xs"} |
25 is the result of applying \isa{f} to all elements of \isa{xs}. We prove |
25 is the result of applying @{term"f"} to all elements of @{term"xs"}. We prove |
26 this lemma by recursion induction w.r.t. \isa{sep}: |
26 this lemma by recursion induction w.r.t. @{term"sep"}: |
27 *} |
27 *} |
28 |
28 |
29 apply(induct_tac x xs rule: sep.induct); |
29 apply(induct_tac x xs rule: sep.induct); |
30 |
30 |
31 txt{*\noindent |
31 txt{*\noindent |
32 The resulting proof state has three subgoals corresponding to the three |
32 The resulting proof state has three subgoals corresponding to the three |
33 clauses for \isa{sep}: |
33 clauses for @{term"sep"}: |
34 \begin{isabelle} |
34 \begin{isabelle} |
35 ~1.~{\isasymAnd}a.~map~f~(sep~(a,~[]))~=~sep~(f~a,~map~f~[])\isanewline |
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 |
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 |
37 ~3.~{\isasymAnd}a~x~y~zs.\isanewline |
38 ~~~~~~~map~f~(sep~(a,~y~\#~zs))~=~sep~(f~a,~map~f~(y~\#~zs))~{\isasymLongrightarrow}\isanewline |
38 ~~~~~~~map~f~(sep~(a,~y~\#~zs))~=~sep~(f~a,~map~f~(y~\#~zs))~{\isasymLongrightarrow}\isanewline |
45 |
45 |
46 text{* |
46 text{* |
47 Try proving the above lemma by structural induction, and you find that you |
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 |
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 |
49 are invented by Isabelle and have nothing to do with the names in the |
50 definition of \isa{sep}. |
50 definition of @{term"sep"}. |
51 |
51 |
52 In general, the format of invoking recursion induction is |
52 In general, the format of invoking recursion induction is |
53 \begin{ttbox} |
53 \begin{quote} |
54 apply(induct_tac \(x@1 \dots x@n\) rule: \(f\).induct) |
54 \isacommand{apply}@{text"(induct_tac ("}$x@1 \dots x@n$ @{text"rule:"} $f$@{text".induct)"} |
55 \end{ttbox}\index{*induct_tac}% |
55 \end{quote}\index{*induct_tac}% |
56 where $x@1~\dots~x@n$ is a list of free variables in the subgoal and $f$ the |
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 |
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 |
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} |
59 induction rules do not mention $f$ at all. For example @{thm[source]sep.induct} |
60 \begin{isabelle} |
60 \begin{isabelle} |
61 {\isasymlbrakk}~{\isasymAnd}a.~P~a~[];\isanewline |
61 {\isasymlbrakk}~{\isasymAnd}a.~P~a~[];\isanewline |
62 ~~{\isasymAnd}a~x.~P~a~[x];\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 |
63 ~~{\isasymAnd}a~x~y~zs.~P~a~(y~\#~zs)~{\isasymLongrightarrow}~P~a~(x~\#~y~\#~zs){\isasymrbrakk}\isanewline |
64 {\isasymLongrightarrow}~P~u~v% |
64 {\isasymLongrightarrow}~P~u~v% |
65 \end{isabelle} |
65 \end{isabelle} |
66 merely says that in order to prove a property \isa{P} of \isa{u} and |
66 merely says that in order to prove a property @{term"P"} of @{term"u"} and |
67 \isa{v} you need to prove it for the three cases where \isa{v} is the |
67 @{term"v"} you need to prove it for the three cases where @{term"v"} is the |
68 empty list, the singleton list, and the list with at least two elements |
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). |
69 (in which case you may assume it holds for the tail of that list). |
70 *} |
70 *} |
71 |
71 |
72 (*<*) |
72 (*<*) |