1 % |
|
2 \begin{isabellebody}% |
|
3 \def\isabellecontext{Induction}% |
|
4 % |
|
5 \isadelimtheory |
|
6 % |
|
7 \endisadelimtheory |
|
8 % |
|
9 \isatagtheory |
|
10 % |
|
11 \endisatagtheory |
|
12 {\isafoldtheory}% |
|
13 % |
|
14 \isadelimtheory |
|
15 % |
|
16 \endisadelimtheory |
|
17 % |
|
18 \begin{isamarkuptext}% |
|
19 Assuming we have defined our function such that Isabelle could prove |
|
20 termination and that the recursion equations (or some suitable derived |
|
21 equations) are simplification rules, we might like to prove something about |
|
22 our function. Since the function is recursive, the natural proof principle is |
|
23 again induction. But this time the structural form of induction that comes |
|
24 with datatypes is unlikely to work well --- otherwise we could have defined the |
|
25 function by \isacommand{primrec}. Therefore \isacommand{recdef} automatically |
|
26 proves a suitable induction rule $f$\isa{{\isachardot}induct} that follows the |
|
27 recursion pattern of the particular function $f$. We call this |
|
28 \textbf{recursion induction}. Roughly speaking, it |
|
29 requires you to prove for each \isacommand{recdef} equation that the property |
|
30 you are trying to establish holds for the left-hand side provided it holds |
|
31 for all recursive calls on the right-hand side. Here is a simple example |
|
32 involving the predefined \isa{map} functional on lists:% |
|
33 \end{isamarkuptext}% |
|
34 \isamarkuptrue% |
|
35 \isacommand{lemma}\isamarkupfalse% |
|
36 \ {\isachardoublequoteopen}map\ f\ {\isacharparenleft}sep{\isacharparenleft}x{\isacharcomma}xs{\isacharparenright}{\isacharparenright}\ {\isacharequal}\ sep{\isacharparenleft}f\ x{\isacharcomma}\ map\ f\ xs{\isacharparenright}{\isachardoublequoteclose}% |
|
37 \isadelimproof |
|
38 % |
|
39 \endisadelimproof |
|
40 % |
|
41 \isatagproof |
|
42 % |
|
43 \begin{isamarkuptxt}% |
|
44 \noindent |
|
45 Note that \isa{map\ f\ xs} |
|
46 is the result of applying \isa{f} to all elements of \isa{xs}. We prove |
|
47 this lemma by recursion induction over \isa{sep}:% |
|
48 \end{isamarkuptxt}% |
|
49 \isamarkuptrue% |
|
50 \isacommand{apply}\isamarkupfalse% |
|
51 {\isacharparenleft}induct{\isacharunderscore}tac\ x\ xs\ rule{\isacharcolon}\ sep{\isachardot}induct{\isacharparenright}% |
|
52 \begin{isamarkuptxt}% |
|
53 \noindent |
|
54 The resulting proof state has three subgoals corresponding to the three |
|
55 clauses for \isa{sep}: |
|
56 \begin{isabelle}% |
|
57 \ {\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 |
|
58 \ {\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 |
|
59 \ {\isadigit{3}}{\isachardot}\ {\isasymAnd}a\ x\ y\ zs{\isachardot}\isanewline |
|
60 \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 |
|
61 \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}% |
|
62 \end{isabelle} |
|
63 The rest is pure simplification:% |
|
64 \end{isamarkuptxt}% |
|
65 \isamarkuptrue% |
|
66 \isacommand{apply}\isamarkupfalse% |
|
67 \ simp{\isacharunderscore}all\isanewline |
|
68 \isacommand{done}\isamarkupfalse% |
|
69 % |
|
70 \endisatagproof |
|
71 {\isafoldproof}% |
|
72 % |
|
73 \isadelimproof |
|
74 % |
|
75 \endisadelimproof |
|
76 % |
|
77 \begin{isamarkuptext}% |
|
78 Try proving the above lemma by structural induction, and you find that you |
|
79 need an additional case distinction. What is worse, the names of variables |
|
80 are invented by Isabelle and have nothing to do with the names in the |
|
81 definition of \isa{sep}. |
|
82 |
|
83 In general, the format of invoking recursion induction is |
|
84 \begin{quote} |
|
85 \isacommand{apply}\isa{{\isacharparenleft}induct{\isacharunderscore}tac} $x@1 \dots x@n$ \isa{rule{\isacharcolon}} $f$\isa{{\isachardot}induct{\isacharparenright}} |
|
86 \end{quote}\index{*induct_tac (method)}% |
|
87 where $x@1~\dots~x@n$ is a list of free variables in the subgoal and $f$ the |
|
88 name of a function that takes an $n$-tuple. Usually the subgoal will |
|
89 contain the term $f(x@1,\dots,x@n)$ but this need not be the case. The |
|
90 induction rules do not mention $f$ at all. Here is \isa{sep{\isachardot}induct}: |
|
91 \begin{isabelle} |
|
92 {\isasymlbrakk}~{\isasymAnd}a.~P~a~[];\isanewline |
|
93 ~~{\isasymAnd}a~x.~P~a~[x];\isanewline |
|
94 ~~{\isasymAnd}a~x~y~zs.~P~a~(y~\#~zs)~{\isasymLongrightarrow}~P~a~(x~\#~y~\#~zs){\isasymrbrakk}\isanewline |
|
95 {\isasymLongrightarrow}~P~u~v% |
|
96 \end{isabelle} |
|
97 It merely says that in order to prove a property \isa{P} of \isa{u} and |
|
98 \isa{v} you need to prove it for the three cases where \isa{v} is the |
|
99 empty list, the singleton list, and the list with at least two elements. |
|
100 The final case has an induction hypothesis: you may assume that \isa{P} |
|
101 holds for the tail of that list.% |
|
102 \end{isamarkuptext}% |
|
103 \isamarkuptrue% |
|
104 % |
|
105 \isadelimtheory |
|
106 % |
|
107 \endisadelimtheory |
|
108 % |
|
109 \isatagtheory |
|
110 % |
|
111 \endisatagtheory |
|
112 {\isafoldtheory}% |
|
113 % |
|
114 \isadelimtheory |
|
115 % |
|
116 \endisadelimtheory |
|
117 \end{isabellebody}% |
|
118 %%% Local Variables: |
|
119 %%% mode: latex |
|
120 %%% TeX-master: "root" |
|
121 %%% End: |
|