13 proves a suitable induction rule $f$\isa{{\isachardot}induct} that follows the |
13 proves a suitable induction rule $f$\isa{{\isachardot}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 involving the predefined \isa{map} functional on lists:% |
19 \end{isamarkuptext}% |
20 \end{isamarkuptext}% |
20 \isacommand{lemma}\ {\isachardoublequote}map\ f\ {\isacharparenleft}sep{\isacharparenleft}x{\isacharcomma}xs{\isacharparenright}{\isacharparenright}\ {\isacharequal}\ sep{\isacharparenleft}f\ x{\isacharcomma}\ map\ f\ xs{\isacharparenright}{\isachardoublequote}% |
21 \isacommand{lemma}\ {\isachardoublequote}map\ f\ {\isacharparenleft}sep{\isacharparenleft}x{\isacharcomma}xs{\isacharparenright}{\isacharparenright}\ {\isacharequal}\ sep{\isacharparenleft}f\ x{\isacharcomma}\ map\ f\ xs{\isacharparenright}{\isachardoublequote}% |
21 \begin{isamarkuptxt}% |
22 \begin{isamarkuptxt}% |
22 \noindent |
23 \noindent |
23 involving the predefined \isa{map} functional on lists: \isa{map\ f\ xs} |
24 Note that \isa{map\ f\ xs} |
24 is the result of applying \isa{f} to all elements of \isa{xs}. We prove |
25 is the result of applying \isa{f} to all elements of \isa{xs}. We prove |
25 this lemma by recursion induction w.r.t. \isa{sep}:% |
26 this lemma by recursion induction over \isa{sep}:% |
26 \end{isamarkuptxt}% |
27 \end{isamarkuptxt}% |
27 \isacommand{apply}{\isacharparenleft}induct{\isacharunderscore}tac\ x\ xs\ rule{\isacharcolon}\ sep{\isachardot}induct{\isacharparenright}% |
28 \isacommand{apply}{\isacharparenleft}induct{\isacharunderscore}tac\ x\ xs\ rule{\isacharcolon}\ sep{\isachardot}induct{\isacharparenright}% |
28 \begin{isamarkuptxt}% |
29 \begin{isamarkuptxt}% |
29 \noindent |
30 \noindent |
30 The resulting proof state has three subgoals corresponding to the three |
31 The resulting proof state has three subgoals corresponding to the three |
46 are invented by Isabelle and have nothing to do with the names in the |
47 are invented by Isabelle and have nothing to do with the names in the |
47 definition of \isa{sep}. |
48 definition of \isa{sep}. |
48 |
49 |
49 In general, the format of invoking recursion induction is |
50 In general, the format of invoking recursion induction is |
50 \begin{quote} |
51 \begin{quote} |
51 \isacommand{apply}\isa{{\isacharparenleft}induct{\isacharunderscore}tac\ {\isacharparenleft}}$x@1 \dots x@n$ \isa{rule{\isacharcolon}} $f$\isa{{\isachardot}induct{\isacharparenright}} |
52 \isacommand{apply}\isa{{\isacharparenleft}induct{\isacharunderscore}tac\ }$x@1 \dots x@n$ \isa{rule{\isacharcolon}} $f$\isa{{\isachardot}induct{\isacharparenright}} |
52 \end{quote}\index{*induct_tac}% |
53 \end{quote}\index{*induct_tac}% |
53 where $x@1~\dots~x@n$ is a list of free variables in the subgoal and $f$ the |
54 where $x@1~\dots~x@n$ is a list of free variables in the subgoal and $f$ the |
54 name of a function that takes an $n$-tuple. Usually the subgoal will |
55 name of a function that takes an $n$-tuple. Usually the subgoal will |
55 contain the term $f~x@1~\dots~x@n$ but this need not be the case. The |
56 contain the term $f~x@1~\dots~x@n$ but this need not be the case. The |
56 induction rules do not mention $f$ at all. For example \isa{sep{\isachardot}induct} |
57 induction rules do not mention $f$ at all. For example \isa{sep{\isachardot}induct} |