3 \def\isabellecontext{Induction}%
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{{\isachardot}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 \isa{map} functional on lists:%
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}%
24 Note that \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 over \isa{sep}:%
28 \isacommand{apply}{\isacharparenleft}induct{\isacharunderscore}tac\ x\ xs\ rule{\isacharcolon}\ sep{\isachardot}induct{\isacharparenright}%
31 The resulting proof state has three subgoals corresponding to the three
32 clauses for \isa{sep}:
34 \ {\isadigit{1}}{\isachardot}\ {\isasymAnd}a{\isachardot}\ map\ f\ {\isacharparenleft}sep\ {\isacharparenleft}a{\isacharcomma}\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}{\isacharparenright}\ {\isacharequal}\ sep\ {\isacharparenleft}f\ a{\isacharcomma}\ map\ f\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}\isanewline
35 \ {\isadigit{2}}{\isachardot}\ {\isasymAnd}a\ x{\isachardot}\ map\ f\ {\isacharparenleft}sep\ {\isacharparenleft}a{\isacharcomma}\ {\isacharbrackleft}x{\isacharbrackright}{\isacharparenright}{\isacharparenright}\ {\isacharequal}\ sep\ {\isacharparenleft}f\ a{\isacharcomma}\ map\ f\ {\isacharbrackleft}x{\isacharbrackright}{\isacharparenright}\isanewline
36 \ {\isadigit{3}}{\isachardot}\ {\isasymAnd}a\ x\ y\ zs{\isachardot}\isanewline
37 \isaindent{\ {\isadigit{3}}{\isachardot}\ \ \ \ }map\ f\ {\isacharparenleft}sep\ {\isacharparenleft}a{\isacharcomma}\ y\ {\isacharhash}\ zs{\isacharparenright}{\isacharparenright}\ {\isacharequal}\ sep\ {\isacharparenleft}f\ a{\isacharcomma}\ map\ f\ {\isacharparenleft}y\ {\isacharhash}\ zs{\isacharparenright}{\isacharparenright}\ {\isasymLongrightarrow}\isanewline
38 \isaindent{\ {\isadigit{3}}{\isachardot}\ \ \ \ }map\ f\ {\isacharparenleft}sep\ {\isacharparenleft}a{\isacharcomma}\ x\ {\isacharhash}\ y\ {\isacharhash}\ zs{\isacharparenright}{\isacharparenright}\ {\isacharequal}\ sep\ {\isacharparenleft}f\ a{\isacharcomma}\ map\ f\ {\isacharparenleft}x\ {\isacharhash}\ y\ {\isacharhash}\ zs{\isacharparenright}{\isacharparenright}%
40 The rest is pure simplification:%
42 \isacommand{apply}\ simp{\isacharunderscore}all\isanewline
44 \begin{isamarkuptext}%
45 Try proving the above lemma by structural induction, and you find that you
46 need an additional case distinction. What is worse, the names of variables
47 are invented by Isabelle and have nothing to do with the names in the
48 definition of \isa{sep}.
50 In general, the format of invoking recursion induction is
52 \isacommand{apply}\isa{{\isacharparenleft}induct{\isacharunderscore}tac\ }$x@1 \dots x@n$ \isa{rule{\isacharcolon}} $f$\isa{{\isachardot}induct{\isacharparenright}}
53 \end{quote}\index{*induct_tac}%
54 where $x@1~\dots~x@n$ is a list of free variables in the subgoal and $f$ the
55 name of a function that takes an $n$-tuple. Usually the subgoal will
56 contain the term $f(x@1,\dots,x@n)$ but this need not be the case. The
57 induction rules do not mention $f$ at all. For example \isa{sep{\isachardot}induct}
59 {\isasymlbrakk}~{\isasymAnd}a.~P~a~[];\isanewline
60 ~~{\isasymAnd}a~x.~P~a~[x];\isanewline
61 ~~{\isasymAnd}a~x~y~zs.~P~a~(y~\#~zs)~{\isasymLongrightarrow}~P~a~(x~\#~y~\#~zs){\isasymrbrakk}\isanewline
62 {\isasymLongrightarrow}~P~u~v%
64 merely says that in order to prove a property \isa{P} of \isa{u} and
65 \isa{v} you need to prove it for the three cases where \isa{v} is the
66 empty list, the singleton list, and the list with at least two elements
67 (in which case you may assume it holds for the tail of that list).%
72 %%% TeX-master: "root"