9722
|
1 |
%
|
|
2 |
\begin{isabellebody}%
|
9924
|
3 |
\def\isabellecontext{termination}%
|
17056
|
4 |
%
|
|
5 |
\isadelimtheory
|
|
6 |
%
|
|
7 |
\endisadelimtheory
|
|
8 |
%
|
|
9 |
\isatagtheory
|
17175
|
10 |
\isamarkupfalse%
|
17056
|
11 |
%
|
|
12 |
\endisatagtheory
|
|
13 |
{\isafoldtheory}%
|
|
14 |
%
|
|
15 |
\isadelimtheory
|
|
16 |
%
|
|
17 |
\endisadelimtheory
|
8749
|
18 |
%
|
|
19 |
\begin{isamarkuptext}%
|
11309
|
20 |
When a function~$f$ is defined via \isacommand{recdef}, Isabelle tries to prove
|
|
21 |
its termination with the help of the user-supplied measure. Each of the examples
|
|
22 |
above is simple enough that Isabelle can automatically prove that the
|
|
23 |
argument's measure decreases in each recursive call. As a result,
|
9792
|
24 |
$f$\isa{{\isachardot}simps} will contain the defining equations (or variants derived
|
|
25 |
from them) as theorems. For example, look (via \isacommand{thm}) at
|
10187
|
26 |
\isa{sep{\isachardot}simps} and \isa{sep{\isadigit{1}}{\isachardot}simps} to see that they define
|
9792
|
27 |
the same function. What is more, those equations are automatically declared as
|
8749
|
28 |
simplification rules.
|
|
29 |
|
11458
|
30 |
Isabelle may fail to prove the termination condition for some
|
12489
|
31 |
recursive call. Let us try to define Quicksort:%
|
11636
|
32 |
\end{isamarkuptext}%
|
17175
|
33 |
\isamarkuptrue%
|
|
34 |
\isacommand{consts}\isamarkupfalse%
|
|
35 |
\ qs\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}nat\ list\ {\isasymRightarrow}\ nat\ list{\isachardoublequoteclose}\isanewline
|
|
36 |
\isacommand{recdef}\isamarkupfalse%
|
|
37 |
\ qs\ {\isachardoublequoteopen}measure\ length{\isachardoublequoteclose}\isanewline
|
|
38 |
\ {\isachardoublequoteopen}qs\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}{\isachardoublequoteclose}\isanewline
|
|
39 |
\ {\isachardoublequoteopen}qs{\isacharparenleft}x{\isacharhash}xs{\isacharparenright}\ {\isacharequal}\ qs{\isacharparenleft}filter\ {\isacharparenleft}{\isasymlambda}y{\isachardot}\ y{\isasymle}x{\isacharparenright}\ xs{\isacharparenright}\ {\isacharat}\ {\isacharbrackleft}x{\isacharbrackright}\ {\isacharat}\ qs{\isacharparenleft}filter\ {\isacharparenleft}{\isasymlambda}y{\isachardot}\ x{\isacharless}y{\isacharparenright}\ xs{\isacharparenright}{\isachardoublequoteclose}%
|
11636
|
40 |
\begin{isamarkuptext}%
|
12489
|
41 |
\noindent where \isa{filter} is predefined and \isa{filter\ P\ xs}
|
|
42 |
is the list of elements of \isa{xs} satisfying \isa{P}.
|
|
43 |
This definition of \isa{qs} fails, and Isabelle prints an error message
|
|
44 |
showing you what it was unable to prove:
|
|
45 |
\begin{isabelle}%
|
|
46 |
\ \ \ \ \ length\ {\isacharparenleft}filter\ {\isachardot}{\isachardot}{\isachardot}\ xs{\isacharparenright}\ {\isacharless}\ Suc\ {\isacharparenleft}length\ xs{\isacharparenright}%
|
|
47 |
\end{isabelle}
|
|
48 |
We can either prove this as a separate lemma, or try to figure out which
|
|
49 |
existing lemmas may help. We opt for the second alternative. The theory of
|
|
50 |
lists contains the simplification rule \isa{length\ {\isacharparenleft}filter\ P\ xs{\isacharparenright}\ {\isasymle}\ length\ xs},
|
15270
|
51 |
which is what we need, provided we turn \mbox{\isa{{\isacharless}\ Suc}}
|
12489
|
52 |
into
|
15270
|
53 |
\isa{{\isasymle}} so that the rule applies. Lemma
|
12489
|
54 |
\isa{less{\isacharunderscore}Suc{\isacharunderscore}eq{\isacharunderscore}le} does just that: \isa{{\isacharparenleft}m\ {\isacharless}\ Suc\ n{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}m\ {\isasymle}\ n{\isacharparenright}}.
|
|
55 |
|
|
56 |
Now we retry the above definition but supply the lemma(s) just found (or
|
|
57 |
proved). Because \isacommand{recdef}'s termination prover involves
|
|
58 |
simplification, we include in our second attempt a hint: the
|
|
59 |
\attrdx{recdef_simp} attribute says to use \isa{less{\isacharunderscore}Suc{\isacharunderscore}eq{\isacharunderscore}le} as a
|
13111
|
60 |
simplification rule.\cmmdx{hints}%
|
11636
|
61 |
\end{isamarkuptext}%
|
17175
|
62 |
\isamarkuptrue%
|
11866
|
63 |
\isamarkupfalse%
|
17175
|
64 |
\isamarkupfalse%
|
|
65 |
\isacommand{recdef}\isamarkupfalse%
|
|
66 |
\ qs\ {\isachardoublequoteopen}measure\ length{\isachardoublequoteclose}\isanewline
|
|
67 |
\ {\isachardoublequoteopen}qs\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}{\isachardoublequoteclose}\isanewline
|
|
68 |
\ {\isachardoublequoteopen}qs{\isacharparenleft}x{\isacharhash}xs{\isacharparenright}\ {\isacharequal}\ qs{\isacharparenleft}filter\ {\isacharparenleft}{\isasymlambda}y{\isachardot}\ y{\isasymle}x{\isacharparenright}\ xs{\isacharparenright}\ {\isacharat}\ {\isacharbrackleft}x{\isacharbrackright}\ {\isacharat}\ qs{\isacharparenleft}filter\ {\isacharparenleft}{\isasymlambda}y{\isachardot}\ x{\isacharless}y{\isacharparenright}\ xs{\isacharparenright}{\isachardoublequoteclose}\isanewline
|
|
69 |
{\isacharparenleft}\isakeyword{hints}\ recdef{\isacharunderscore}simp{\isacharcolon}\ less{\isacharunderscore}Suc{\isacharunderscore}eq{\isacharunderscore}le{\isacharparenright}\isamarkupfalse%
|
11866
|
70 |
%
|
11636
|
71 |
\begin{isamarkuptext}%
|
|
72 |
\noindent
|
12489
|
73 |
This time everything works fine. Now \isa{qs{\isachardot}simps} contains precisely
|
|
74 |
the stated recursion equations for \isa{qs} and they have become
|
|
75 |
simplification rules.
|
|
76 |
Thus we can automatically prove results such as this one:%
|
11636
|
77 |
\end{isamarkuptext}%
|
17175
|
78 |
\isamarkuptrue%
|
|
79 |
\isacommand{theorem}\isamarkupfalse%
|
|
80 |
\ {\isachardoublequoteopen}qs{\isacharbrackleft}{\isadigit{2}}{\isacharcomma}{\isadigit{3}}{\isacharcomma}{\isadigit{0}}{\isacharbrackright}\ {\isacharequal}\ qs{\isacharbrackleft}{\isadigit{3}}{\isacharcomma}{\isadigit{0}}{\isacharcomma}{\isadigit{2}}{\isacharbrackright}{\isachardoublequoteclose}\isanewline
|
17056
|
81 |
%
|
|
82 |
\isadelimproof
|
|
83 |
%
|
|
84 |
\endisadelimproof
|
|
85 |
%
|
|
86 |
\isatagproof
|
17175
|
87 |
\isacommand{apply}\isamarkupfalse%
|
|
88 |
{\isacharparenleft}simp{\isacharparenright}\isanewline
|
|
89 |
\isacommand{done}\isamarkupfalse%
|
|
90 |
%
|
17056
|
91 |
\endisatagproof
|
|
92 |
{\isafoldproof}%
|
|
93 |
%
|
|
94 |
\isadelimproof
|
|
95 |
%
|
|
96 |
\endisadelimproof
|
11866
|
97 |
%
|
11636
|
98 |
\begin{isamarkuptext}%
|
|
99 |
\noindent
|
|
100 |
More exciting theorems require induction, which is discussed below.
|
|
101 |
|
12489
|
102 |
If the termination proof requires a lemma that is of general use, you can
|
11636
|
103 |
turn it permanently into a simplification rule, in which case the above
|
12489
|
104 |
\isacommand{hint} is not necessary. But in the case of
|
|
105 |
\isa{less{\isacharunderscore}Suc{\isacharunderscore}eq{\isacharunderscore}le} this would be of dubious value.%
|
11636
|
106 |
\end{isamarkuptext}%
|
17175
|
107 |
\isamarkuptrue%
|
17056
|
108 |
%
|
|
109 |
\isadelimtheory
|
|
110 |
%
|
|
111 |
\endisadelimtheory
|
|
112 |
%
|
|
113 |
\isatagtheory
|
17175
|
114 |
\isamarkupfalse%
|
17056
|
115 |
%
|
|
116 |
\endisatagtheory
|
|
117 |
{\isafoldtheory}%
|
|
118 |
%
|
|
119 |
\isadelimtheory
|
|
120 |
%
|
|
121 |
\endisadelimtheory
|
11636
|
122 |
\end{isabellebody}%
|
9145
|
123 |
%%% Local Variables:
|
|
124 |
%%% mode: latex
|
|
125 |
%%% TeX-master: "root"
|
|
126 |
%%% End:
|