9722
|
1 |
%
|
|
2 |
\begin{isabellebody}%
|
9924
|
3 |
\def\isabellecontext{Induction}%
|
17056
|
4 |
%
|
|
5 |
\isadelimtheory
|
|
6 |
%
|
|
7 |
\endisadelimtheory
|
|
8 |
%
|
|
9 |
\isatagtheory
|
|
10 |
%
|
|
11 |
\endisatagtheory
|
|
12 |
{\isafoldtheory}%
|
|
13 |
%
|
|
14 |
\isadelimtheory
|
|
15 |
%
|
|
16 |
\endisadelimtheory
|
8749
|
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
|
10971
|
24 |
with datatypes is unlikely to work well --- otherwise we could have defined the
|
8749
|
25 |
function by \isacommand{primrec}. Therefore \isacommand{recdef} automatically
|
9792
|
26 |
proves a suitable induction rule $f$\isa{{\isachardot}induct} that follows the
|
8749
|
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
|
10795
|
31 |
for all recursive calls on the right-hand side. Here is a simple example
|
|
32 |
involving the predefined \isa{map} functional on lists:%
|
8749
|
33 |
\end{isamarkuptext}%
|
17175
|
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}%
|
17056
|
37 |
\isadelimproof
|
|
38 |
%
|
|
39 |
\endisadelimproof
|
|
40 |
%
|
|
41 |
\isatagproof
|
16069
|
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}%
|
17175
|
49 |
\isamarkuptrue%
|
|
50 |
\isacommand{apply}\isamarkupfalse%
|
|
51 |
{\isacharparenleft}induct{\isacharunderscore}tac\ x\ xs\ rule{\isacharcolon}\ sep{\isachardot}induct{\isacharparenright}%
|
16069
|
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}%
|
17175
|
65 |
\isamarkuptrue%
|
|
66 |
\isacommand{apply}\isamarkupfalse%
|
|
67 |
\ simp{\isacharunderscore}all\isanewline
|
|
68 |
\isacommand{done}\isamarkupfalse%
|
|
69 |
%
|
17056
|
70 |
\endisatagproof
|
|
71 |
{\isafoldproof}%
|
|
72 |
%
|
|
73 |
\isadelimproof
|
|
74 |
%
|
|
75 |
\endisadelimproof
|
11866
|
76 |
%
|
8749
|
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
|
9792
|
84 |
\begin{quote}
|
11159
|
85 |
\isacommand{apply}\isa{{\isacharparenleft}induct{\isacharunderscore}tac} $x@1 \dots x@n$ \isa{rule{\isacharcolon}} $f$\isa{{\isachardot}induct{\isacharparenright}}
|
11428
|
86 |
\end{quote}\index{*induct_tac (method)}%
|
8749
|
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
|
10971
|
89 |
contain the term $f(x@1,\dots,x@n)$ but this need not be the case. The
|
11458
|
90 |
induction rules do not mention $f$ at all. Here is \isa{sep{\isachardot}induct}:
|
9723
|
91 |
\begin{isabelle}
|
9689
|
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%
|
9723
|
96 |
\end{isabelle}
|
11458
|
97 |
It merely says that in order to prove a property \isa{P} of \isa{u} and
|
9689
|
98 |
\isa{v} you need to prove it for the three cases where \isa{v} is the
|
11458
|
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.%
|
8749
|
102 |
\end{isamarkuptext}%
|
17175
|
103 |
\isamarkuptrue%
|
17056
|
104 |
%
|
|
105 |
\isadelimtheory
|
|
106 |
%
|
|
107 |
\endisadelimtheory
|
|
108 |
%
|
|
109 |
\isatagtheory
|
|
110 |
%
|
|
111 |
\endisatagtheory
|
|
112 |
{\isafoldtheory}%
|
|
113 |
%
|
|
114 |
\isadelimtheory
|
|
115 |
%
|
|
116 |
\endisadelimtheory
|
9722
|
117 |
\end{isabellebody}%
|
9145
|
118 |
%%% Local Variables:
|
|
119 |
%%% mode: latex
|
|
120 |
%%% TeX-master: "root"
|
|
121 |
%%% End:
|