10654
|
1 |
%
|
|
2 |
\begin{isabellebody}%
|
|
3 |
\def\isabellecontext{Partial}%
|
17181
|
4 |
\isamarkupfalse%
|
17056
|
5 |
%
|
|
6 |
\isadelimtheory
|
|
7 |
%
|
|
8 |
\endisadelimtheory
|
|
9 |
%
|
|
10 |
\isatagtheory
|
|
11 |
%
|
|
12 |
\endisatagtheory
|
|
13 |
{\isafoldtheory}%
|
|
14 |
%
|
|
15 |
\isadelimtheory
|
|
16 |
%
|
|
17 |
\endisadelimtheory
|
10654
|
18 |
%
|
|
19 |
\begin{isamarkuptext}%
|
11494
|
20 |
\noindent Throughout this tutorial, we have emphasized
|
|
21 |
that all functions in HOL are total. We cannot hope to define
|
11310
|
22 |
truly partial functions, but must make them total. A straightforward
|
|
23 |
method is to lift the result type of the function from $\tau$ to
|
11277
|
24 |
$\tau$~\isa{option} (see \ref{sec:option}), where \isa{None} is
|
|
25 |
returned if the function is applied to an argument not in its
|
|
26 |
domain. Function \isa{assoc} in \S\ref{sec:Trie} is a simple example.
|
|
27 |
We do not pursue this schema further because it should be clear
|
|
28 |
how it works. Its main drawback is that the result of such a lifted
|
|
29 |
function has to be unpacked first before it can be processed
|
|
30 |
further. Its main advantage is that you can distinguish if the
|
|
31 |
function was applied to an argument in its domain or not. If you do
|
|
32 |
not need to make this distinction, for example because the function is
|
|
33 |
never used outside its domain, it is easier to work with
|
11428
|
34 |
\emph{underdefined}\index{functions!underdefined} functions: for
|
11277
|
35 |
certain arguments we only know that a result exists, but we do not
|
|
36 |
know what it is. When defining functions that are normally considered
|
|
37 |
partial, underdefinedness turns out to be a very reasonable
|
|
38 |
alternative.
|
10654
|
39 |
|
|
40 |
We have already seen an instance of underdefinedness by means of
|
|
41 |
non-exhaustive pattern matching: the definition of \isa{last} in
|
|
42 |
\S\ref{sec:recdef-examples}. The same is allowed for \isacommand{primrec}%
|
|
43 |
\end{isamarkuptext}%
|
17175
|
44 |
\isamarkuptrue%
|
|
45 |
\isacommand{consts}\isamarkupfalse%
|
|
46 |
\ hd\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}a{\isachardoublequoteclose}\isanewline
|
|
47 |
\isacommand{primrec}\isamarkupfalse%
|
|
48 |
\ {\isachardoublequoteopen}hd\ {\isacharparenleft}x{\isacharhash}xs{\isacharparenright}\ {\isacharequal}\ x{\isachardoublequoteclose}%
|
10654
|
49 |
\begin{isamarkuptext}%
|
|
50 |
\noindent
|
|
51 |
although it generates a warning.
|
|
52 |
Even ordinary definitions allow underdefinedness, this time by means of
|
|
53 |
preconditions:%
|
|
54 |
\end{isamarkuptext}%
|
17175
|
55 |
\isamarkuptrue%
|
|
56 |
\isacommand{constdefs}\isamarkupfalse%
|
|
57 |
\ minus\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}nat\ {\isasymRightarrow}\ nat\ {\isasymRightarrow}\ nat{\isachardoublequoteclose}\isanewline
|
|
58 |
{\isachardoublequoteopen}n\ {\isasymle}\ m\ {\isasymLongrightarrow}\ minus\ m\ n\ {\isasymequiv}\ m\ {\isacharminus}\ n{\isachardoublequoteclose}%
|
10654
|
59 |
\begin{isamarkuptext}%
|
|
60 |
The rest of this section is devoted to the question of how to define
|
11256
|
61 |
partial recursive functions by other means than non-exhaustive pattern
|
10654
|
62 |
matching.%
|
|
63 |
\end{isamarkuptext}%
|
11866
|
64 |
\isamarkuptrue%
|
10654
|
65 |
%
|
10878
|
66 |
\isamarkupsubsubsection{Guarded Recursion%
|
10654
|
67 |
}
|
11866
|
68 |
\isamarkuptrue%
|
10654
|
69 |
%
|
|
70 |
\begin{isamarkuptext}%
|
11494
|
71 |
\index{recursion!guarded}%
|
10654
|
72 |
Neither \isacommand{primrec} nor \isacommand{recdef} allow to
|
|
73 |
prefix an equation with a condition in the way ordinary definitions do
|
|
74 |
(see \isa{minus} above). Instead we have to move the condition over
|
|
75 |
to the right-hand side of the equation. Given a partial function $f$
|
|
76 |
that should satisfy the recursion equation $f(x) = t$ over its domain
|
|
77 |
$dom(f)$, we turn this into the \isacommand{recdef}
|
|
78 |
\begin{isabelle}%
|
|
79 |
\ \ \ \ \ f\ x\ {\isacharequal}\ {\isacharparenleft}if\ x\ {\isasymin}\ dom\ f\ then\ t\ else\ arbitrary{\isacharparenright}%
|
|
80 |
\end{isabelle}
|
|
81 |
where \isa{arbitrary} is a predeclared constant of type \isa{{\isacharprime}a}
|
|
82 |
which has no definition. Thus we know nothing about its value,
|
|
83 |
which is ideal for specifying underdefined functions on top of it.
|
|
84 |
|
|
85 |
As a simple example we define division on \isa{nat}:%
|
|
86 |
\end{isamarkuptext}%
|
17175
|
87 |
\isamarkuptrue%
|
|
88 |
\isacommand{consts}\isamarkupfalse%
|
|
89 |
\ divi\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}nat\ {\isasymtimes}\ nat\ {\isasymRightarrow}\ nat{\isachardoublequoteclose}\isanewline
|
|
90 |
\isacommand{recdef}\isamarkupfalse%
|
|
91 |
\ divi\ {\isachardoublequoteopen}measure{\isacharparenleft}{\isasymlambda}{\isacharparenleft}m{\isacharcomma}n{\isacharparenright}{\isachardot}\ m{\isacharparenright}{\isachardoublequoteclose}\isanewline
|
|
92 |
\ \ {\isachardoublequoteopen}divi{\isacharparenleft}m{\isacharcomma}{\isadigit{0}}{\isacharparenright}\ {\isacharequal}\ arbitrary{\isachardoublequoteclose}\isanewline
|
|
93 |
\ \ {\isachardoublequoteopen}divi{\isacharparenleft}m{\isacharcomma}n{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}if\ m\ {\isacharless}\ n\ then\ {\isadigit{0}}\ else\ divi{\isacharparenleft}m{\isacharminus}n{\isacharcomma}n{\isacharparenright}{\isacharplus}{\isadigit{1}}{\isacharparenright}{\isachardoublequoteclose}%
|
10654
|
94 |
\begin{isamarkuptext}%
|
|
95 |
\noindent Of course we could also have defined
|
|
96 |
\isa{divi\ {\isacharparenleft}m{\isacharcomma}\ {\isadigit{0}}{\isacharparenright}} to be some specific number, for example 0. The
|
|
97 |
latter option is chosen for the predefined \isa{div} function, which
|
10878
|
98 |
simplifies proofs at the expense of deviating from the
|
|
99 |
standard mathematical division function.
|
10654
|
100 |
|
|
101 |
As a more substantial example we consider the problem of searching a graph.
|
11277
|
102 |
For simplicity our graph is given by a function \isa{f} of
|
10654
|
103 |
type \isa{{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a} which
|
12334
|
104 |
maps each node to its successor; the graph has out-degree 1.
|
11196
|
105 |
The task is to find the end of a chain, modelled by a node pointing to
|
|
106 |
itself. Here is a first attempt:
|
10654
|
107 |
\begin{isabelle}%
|
|
108 |
\ \ \ \ \ find\ {\isacharparenleft}f{\isacharcomma}\ x{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}if\ f\ x\ {\isacharequal}\ x\ then\ x\ else\ find\ {\isacharparenleft}f{\isacharcomma}\ f\ x{\isacharparenright}{\isacharparenright}%
|
|
109 |
\end{isabelle}
|
12334
|
110 |
This may be viewed as a fixed point finder or as the second half of the well
|
|
111 |
known \emph{Union-Find} algorithm.
|
11149
|
112 |
The snag is that it may not terminate if \isa{f} has non-trivial cycles.
|
10654
|
113 |
Phrased differently, the relation%
|
|
114 |
\end{isamarkuptext}%
|
17175
|
115 |
\isamarkuptrue%
|
|
116 |
\isacommand{constdefs}\isamarkupfalse%
|
|
117 |
\ step{\isadigit{1}}\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharparenleft}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a{\isacharparenright}\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}a{\isacharparenright}set{\isachardoublequoteclose}\isanewline
|
|
118 |
\ \ {\isachardoublequoteopen}step{\isadigit{1}}\ f\ {\isasymequiv}\ {\isacharbraceleft}{\isacharparenleft}y{\isacharcomma}x{\isacharparenright}{\isachardot}\ y\ {\isacharequal}\ f\ x\ {\isasymand}\ y\ {\isasymnoteq}\ x{\isacharbraceright}{\isachardoublequoteclose}%
|
10654
|
119 |
\begin{isamarkuptext}%
|
|
120 |
\noindent
|
|
121 |
must be well-founded. Thus we make the following definition:%
|
|
122 |
\end{isamarkuptext}%
|
17175
|
123 |
\isamarkuptrue%
|
|
124 |
\isacommand{consts}\isamarkupfalse%
|
|
125 |
\ find\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharparenleft}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a{\isacharparenright}\ {\isasymtimes}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a{\isachardoublequoteclose}\isanewline
|
|
126 |
\isacommand{recdef}\isamarkupfalse%
|
|
127 |
\ find\ {\isachardoublequoteopen}same{\isacharunderscore}fst\ {\isacharparenleft}{\isasymlambda}f{\isachardot}\ wf{\isacharparenleft}step{\isadigit{1}}\ f{\isacharparenright}{\isacharparenright}\ step{\isadigit{1}}{\isachardoublequoteclose}\isanewline
|
|
128 |
\ \ {\isachardoublequoteopen}find{\isacharparenleft}f{\isacharcomma}x{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}if\ wf{\isacharparenleft}step{\isadigit{1}}\ f{\isacharparenright}\isanewline
|
10654
|
129 |
\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ then\ if\ f\ x\ {\isacharequal}\ x\ then\ x\ else\ find{\isacharparenleft}f{\isacharcomma}\ f\ x{\isacharparenright}\isanewline
|
17175
|
130 |
\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ else\ arbitrary{\isacharparenright}{\isachardoublequoteclose}\isanewline
|
|
131 |
{\isacharparenleft}\isakeyword{hints}\ recdef{\isacharunderscore}simp{\isacharcolon}\ step{\isadigit{1}}{\isacharunderscore}def{\isacharparenright}%
|
10654
|
132 |
\begin{isamarkuptext}%
|
|
133 |
\noindent
|
|
134 |
The recursion equation itself should be clear enough: it is our aborted
|
|
135 |
first attempt augmented with a check that there are no non-trivial loops.
|
11277
|
136 |
To express the required well-founded relation we employ the
|
11196
|
137 |
predefined combinator \isa{same{\isacharunderscore}fst} of type
|
10654
|
138 |
\begin{isabelle}%
|
|
139 |
\ \ \ \ \ {\isacharparenleft}{\isacharprime}a\ {\isasymRightarrow}\ bool{\isacharparenright}\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}b{\isasymtimes}{\isacharprime}b{\isacharparenright}set{\isacharparenright}\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharparenleft}{\isacharprime}a{\isasymtimes}{\isacharprime}b{\isacharparenright}\ {\isasymtimes}\ {\isacharparenleft}{\isacharprime}a{\isasymtimes}{\isacharprime}b{\isacharparenright}{\isacharparenright}set%
|
|
140 |
\end{isabelle}
|
|
141 |
defined as
|
|
142 |
\begin{isabelle}%
|
|
143 |
\ \ \ \ \ same{\isacharunderscore}fst\ P\ R\ {\isasymequiv}\ {\isacharbraceleft}{\isacharparenleft}{\isacharparenleft}x{\isacharprime}{\isacharcomma}\ y{\isacharprime}{\isacharparenright}{\isacharcomma}\ x{\isacharcomma}\ y{\isacharparenright}{\isachardot}\ x{\isacharprime}\ {\isacharequal}\ x\ {\isasymand}\ P\ x\ {\isasymand}\ {\isacharparenleft}y{\isacharprime}{\isacharcomma}\ y{\isacharparenright}\ {\isasymin}\ R\ x{\isacharbraceright}%
|
|
144 |
\end{isabelle}
|
11196
|
145 |
This combinator is designed for
|
|
146 |
recursive functions on pairs where the first component of the argument is
|
|
147 |
passed unchanged to all recursive calls. Given a constraint on the first
|
|
148 |
component and a relation on the second component, \isa{same{\isacharunderscore}fst} builds the
|
|
149 |
required relation on pairs. The theorem
|
|
150 |
\begin{isabelle}%
|
10654
|
151 |
\ \ \ \ \ {\isacharparenleft}{\isasymAnd}x{\isachardot}\ P\ x\ {\isasymLongrightarrow}\ wf\ {\isacharparenleft}R\ x{\isacharparenright}{\isacharparenright}\ {\isasymLongrightarrow}\ wf\ {\isacharparenleft}same{\isacharunderscore}fst\ P\ R{\isacharparenright}%
|
|
152 |
\end{isabelle}
|
11196
|
153 |
is known to the well-foundedness prover of \isacommand{recdef}. Thus
|
|
154 |
well-foundedness of the relation given to \isacommand{recdef} is immediate.
|
|
155 |
Furthermore, each recursive call descends along that relation: the first
|
11285
|
156 |
argument stays unchanged and the second one descends along \isa{step{\isadigit{1}}\ f}. The proof requires unfolding the definition of \isa{step{\isadigit{1}}},
|
|
157 |
as specified in the \isacommand{hints} above.
|
10654
|
158 |
|
11494
|
159 |
Normally you will then derive the following conditional variant from
|
|
160 |
the recursion equation:%
|
10654
|
161 |
\end{isamarkuptext}%
|
17175
|
162 |
\isamarkuptrue%
|
|
163 |
\isacommand{lemma}\isamarkupfalse%
|
|
164 |
\ {\isacharbrackleft}simp{\isacharbrackright}{\isacharcolon}\isanewline
|
|
165 |
\ \ {\isachardoublequoteopen}wf{\isacharparenleft}step{\isadigit{1}}\ f{\isacharparenright}\ {\isasymLongrightarrow}\ find{\isacharparenleft}f{\isacharcomma}x{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}if\ f\ x\ {\isacharequal}\ x\ then\ x\ else\ find{\isacharparenleft}f{\isacharcomma}\ f\ x{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}\isanewline
|
17056
|
166 |
%
|
|
167 |
\isadelimproof
|
|
168 |
%
|
|
169 |
\endisadelimproof
|
|
170 |
%
|
|
171 |
\isatagproof
|
17175
|
172 |
\isacommand{by}\isamarkupfalse%
|
|
173 |
\ simp%
|
17056
|
174 |
\endisatagproof
|
|
175 |
{\isafoldproof}%
|
|
176 |
%
|
|
177 |
\isadelimproof
|
|
178 |
%
|
|
179 |
\endisadelimproof
|
11866
|
180 |
%
|
10654
|
181 |
\begin{isamarkuptext}%
|
11494
|
182 |
\noindent Then you should disable the original recursion equation:%
|
10654
|
183 |
\end{isamarkuptext}%
|
17175
|
184 |
\isamarkuptrue%
|
|
185 |
\isacommand{declare}\isamarkupfalse%
|
|
186 |
\ find{\isachardot}simps{\isacharbrackleft}simp\ del{\isacharbrackright}%
|
10654
|
187 |
\begin{isamarkuptext}%
|
11494
|
188 |
Reasoning about such underdefined functions is like that for other
|
|
189 |
recursive functions. Here is a simple example of recursion induction:%
|
10654
|
190 |
\end{isamarkuptext}%
|
17175
|
191 |
\isamarkuptrue%
|
|
192 |
\isacommand{lemma}\isamarkupfalse%
|
|
193 |
\ {\isachardoublequoteopen}wf{\isacharparenleft}step{\isadigit{1}}\ f{\isacharparenright}\ {\isasymlongrightarrow}\ f{\isacharparenleft}find{\isacharparenleft}f{\isacharcomma}x{\isacharparenright}{\isacharparenright}\ {\isacharequal}\ find{\isacharparenleft}f{\isacharcomma}x{\isacharparenright}{\isachardoublequoteclose}\isanewline
|
17056
|
194 |
%
|
|
195 |
\isadelimproof
|
|
196 |
%
|
|
197 |
\endisadelimproof
|
|
198 |
%
|
|
199 |
\isatagproof
|
17175
|
200 |
\isacommand{apply}\isamarkupfalse%
|
|
201 |
{\isacharparenleft}induct{\isacharunderscore}tac\ f\ x\ rule{\isacharcolon}\ find{\isachardot}induct{\isacharparenright}\isanewline
|
|
202 |
\isacommand{apply}\isamarkupfalse%
|
|
203 |
\ simp\isanewline
|
|
204 |
\isacommand{done}\isamarkupfalse%
|
|
205 |
%
|
17056
|
206 |
\endisatagproof
|
|
207 |
{\isafoldproof}%
|
|
208 |
%
|
|
209 |
\isadelimproof
|
|
210 |
%
|
|
211 |
\endisadelimproof
|
11866
|
212 |
%
|
10878
|
213 |
\isamarkupsubsubsection{The {\tt\slshape while} Combinator%
|
10654
|
214 |
}
|
11866
|
215 |
\isamarkuptrue%
|
10654
|
216 |
%
|
|
217 |
\begin{isamarkuptext}%
|
|
218 |
If the recursive function happens to be tail recursive, its
|
11428
|
219 |
definition becomes a triviality if based on the predefined \cdx{while}
|
12332
|
220 |
combinator. The latter lives in the Library theory \thydx{While_Combinator}.
|
|
221 |
% which is not part of {text Main} but needs to
|
|
222 |
% be included explicitly among the ancestor theories.
|
10654
|
223 |
|
|
224 |
Constant \isa{while} is of type \isa{{\isacharparenleft}{\isacharprime}a\ {\isasymRightarrow}\ bool{\isacharparenright}\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a}
|
|
225 |
and satisfies the recursion equation \begin{isabelle}%
|
|
226 |
\ \ \ \ \ while\ b\ c\ s\ {\isacharequal}\ {\isacharparenleft}if\ b\ s\ then\ while\ b\ c\ {\isacharparenleft}c\ s{\isacharparenright}\ else\ s{\isacharparenright}%
|
|
227 |
\end{isabelle}
|
|
228 |
That is, \isa{while\ b\ c\ s} is equivalent to the imperative program
|
|
229 |
\begin{verbatim}
|
|
230 |
x := s; while b(x) do x := c(x); return x
|
|
231 |
\end{verbatim}
|
11494
|
232 |
In general, \isa{s} will be a tuple or record. As an example
|
|
233 |
consider the following definition of function \isa{find}:%
|
10654
|
234 |
\end{isamarkuptext}%
|
17175
|
235 |
\isamarkuptrue%
|
|
236 |
\isacommand{constdefs}\isamarkupfalse%
|
|
237 |
\ find{\isadigit{2}}\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharparenleft}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a{\isachardoublequoteclose}\isanewline
|
|
238 |
\ \ {\isachardoublequoteopen}find{\isadigit{2}}\ f\ x\ {\isasymequiv}\isanewline
|
|
239 |
\ \ \ fst{\isacharparenleft}while\ {\isacharparenleft}{\isasymlambda}{\isacharparenleft}x{\isacharcomma}x{\isacharprime}{\isacharparenright}{\isachardot}\ x{\isacharprime}\ {\isasymnoteq}\ x{\isacharparenright}\ {\isacharparenleft}{\isasymlambda}{\isacharparenleft}x{\isacharcomma}x{\isacharprime}{\isacharparenright}{\isachardot}\ {\isacharparenleft}x{\isacharprime}{\isacharcomma}f\ x{\isacharprime}{\isacharparenright}{\isacharparenright}\ {\isacharparenleft}x{\isacharcomma}f\ x{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}%
|
10654
|
240 |
\begin{isamarkuptext}%
|
|
241 |
\noindent
|
|
242 |
The loop operates on two ``local variables'' \isa{x} and \isa{x{\isacharprime}}
|
|
243 |
containing the ``current'' and the ``next'' value of function \isa{f}.
|
11310
|
244 |
They are initialized with the global \isa{x} and \isa{f\ x}. At the
|
10654
|
245 |
end \isa{fst} selects the local \isa{x}.
|
|
246 |
|
11158
|
247 |
Although the definition of tail recursive functions via \isa{while} avoids
|
|
248 |
termination proofs, there is no free lunch. When proving properties of
|
|
249 |
functions defined by \isa{while}, termination rears its ugly head
|
11494
|
250 |
again. Here is \tdx{while_rule}, the well known proof rule for total
|
10654
|
251 |
correctness of loops expressed with \isa{while}:
|
|
252 |
\begin{isabelle}%
|
10696
|
253 |
\ \ \ \ \ {\isasymlbrakk}P\ s{\isacharsemicolon}\ {\isasymAnd}s{\isachardot}\ {\isasymlbrakk}P\ s{\isacharsemicolon}\ b\ s{\isasymrbrakk}\ {\isasymLongrightarrow}\ P\ {\isacharparenleft}c\ s{\isacharparenright}{\isacharsemicolon}\isanewline
|
14379
|
254 |
\isaindent{\ \ \ \ \ \ }{\isasymAnd}s{\isachardot}\ {\isasymlbrakk}P\ s{\isacharsemicolon}\ {\isasymnot}\ b\ s{\isasymrbrakk}\ {\isasymLongrightarrow}\ Q\ s{\isacharsemicolon}\ wf\ r{\isacharsemicolon}\isanewline
|
|
255 |
\isaindent{\ \ \ \ \ \ }{\isasymAnd}s{\isachardot}\ {\isasymlbrakk}P\ s{\isacharsemicolon}\ b\ s{\isasymrbrakk}\ {\isasymLongrightarrow}\ {\isacharparenleft}c\ s{\isacharcomma}\ s{\isacharparenright}\ {\isasymin}\ r{\isasymrbrakk}\isanewline
|
10950
|
256 |
\isaindent{\ \ \ \ \ }{\isasymLongrightarrow}\ Q\ {\isacharparenleft}while\ b\ c\ s{\isacharparenright}%
|
11158
|
257 |
\end{isabelle} \isa{P} needs to be true of
|
|
258 |
the initial state \isa{s} and invariant under \isa{c} (premises 1
|
|
259 |
and~2). The post-condition \isa{Q} must become true when leaving the loop
|
|
260 |
(premise~3). And each loop iteration must descend along a well-founded
|
|
261 |
relation \isa{r} (premises 4 and~5).
|
10654
|
262 |
|
|
263 |
Let us now prove that \isa{find{\isadigit{2}}} does indeed find a fixed point. Instead
|
|
264 |
of induction we apply the above while rule, suitably instantiated.
|
|
265 |
Only the final premise of \isa{while{\isacharunderscore}rule} is left unproved
|
|
266 |
by \isa{auto} but falls to \isa{simp}:%
|
|
267 |
\end{isamarkuptext}%
|
17175
|
268 |
\isamarkuptrue%
|
|
269 |
\isacommand{lemma}\isamarkupfalse%
|
|
270 |
\ lem{\isacharcolon}\ {\isachardoublequoteopen}wf{\isacharparenleft}step{\isadigit{1}}\ f{\isacharparenright}\ {\isasymLongrightarrow}\isanewline
|
11277
|
271 |
\ \ {\isasymexists}y{\isachardot}\ while\ {\isacharparenleft}{\isasymlambda}{\isacharparenleft}x{\isacharcomma}x{\isacharprime}{\isacharparenright}{\isachardot}\ x{\isacharprime}\ {\isasymnoteq}\ x{\isacharparenright}\ {\isacharparenleft}{\isasymlambda}{\isacharparenleft}x{\isacharcomma}x{\isacharprime}{\isacharparenright}{\isachardot}\ {\isacharparenleft}x{\isacharprime}{\isacharcomma}f\ x{\isacharprime}{\isacharparenright}{\isacharparenright}\ {\isacharparenleft}x{\isacharcomma}f\ x{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}y{\isacharcomma}y{\isacharparenright}\ {\isasymand}\isanewline
|
17175
|
272 |
\ \ \ \ \ \ \ f\ y\ {\isacharequal}\ y{\isachardoublequoteclose}\isanewline
|
17056
|
273 |
%
|
|
274 |
\isadelimproof
|
|
275 |
%
|
|
276 |
\endisadelimproof
|
|
277 |
%
|
|
278 |
\isatagproof
|
17175
|
279 |
\isacommand{apply}\isamarkupfalse%
|
|
280 |
{\isacharparenleft}rule{\isacharunderscore}tac\ P\ {\isacharequal}\ {\isachardoublequoteopen}{\isasymlambda}{\isacharparenleft}x{\isacharcomma}x{\isacharprime}{\isacharparenright}{\isachardot}\ x{\isacharprime}\ {\isacharequal}\ f\ x{\isachardoublequoteclose}\ \isakeyword{and}\isanewline
|
|
281 |
\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ r\ {\isacharequal}\ {\isachardoublequoteopen}inv{\isacharunderscore}image\ {\isacharparenleft}step{\isadigit{1}}\ f{\isacharparenright}\ fst{\isachardoublequoteclose}\ \isakeyword{in}\ while{\isacharunderscore}rule{\isacharparenright}\isanewline
|
|
282 |
\isacommand{apply}\isamarkupfalse%
|
|
283 |
\ auto\isanewline
|
|
284 |
\isacommand{apply}\isamarkupfalse%
|
|
285 |
{\isacharparenleft}simp\ add{\isacharcolon}\ inv{\isacharunderscore}image{\isacharunderscore}def\ step{\isadigit{1}}{\isacharunderscore}def{\isacharparenright}\isanewline
|
|
286 |
\isacommand{done}\isamarkupfalse%
|
|
287 |
%
|
17056
|
288 |
\endisatagproof
|
|
289 |
{\isafoldproof}%
|
|
290 |
%
|
|
291 |
\isadelimproof
|
|
292 |
%
|
|
293 |
\endisadelimproof
|
11866
|
294 |
%
|
10654
|
295 |
\begin{isamarkuptext}%
|
|
296 |
The theorem itself is a simple consequence of this lemma:%
|
|
297 |
\end{isamarkuptext}%
|
17175
|
298 |
\isamarkuptrue%
|
|
299 |
\isacommand{theorem}\isamarkupfalse%
|
|
300 |
\ {\isachardoublequoteopen}wf{\isacharparenleft}step{\isadigit{1}}\ f{\isacharparenright}\ {\isasymLongrightarrow}\ f{\isacharparenleft}find{\isadigit{2}}\ f\ x{\isacharparenright}\ {\isacharequal}\ find{\isadigit{2}}\ f\ x{\isachardoublequoteclose}\isanewline
|
17056
|
301 |
%
|
|
302 |
\isadelimproof
|
|
303 |
%
|
|
304 |
\endisadelimproof
|
|
305 |
%
|
|
306 |
\isatagproof
|
17175
|
307 |
\isacommand{apply}\isamarkupfalse%
|
|
308 |
{\isacharparenleft}drule{\isacharunderscore}tac\ x\ {\isacharequal}\ x\ \isakeyword{in}\ lem{\isacharparenright}\isanewline
|
|
309 |
\isacommand{apply}\isamarkupfalse%
|
|
310 |
{\isacharparenleft}auto\ simp\ add{\isacharcolon}\ find{\isadigit{2}}{\isacharunderscore}def{\isacharparenright}\isanewline
|
|
311 |
\isacommand{done}\isamarkupfalse%
|
|
312 |
%
|
17056
|
313 |
\endisatagproof
|
|
314 |
{\isafoldproof}%
|
|
315 |
%
|
|
316 |
\isadelimproof
|
|
317 |
%
|
|
318 |
\endisadelimproof
|
11866
|
319 |
%
|
10654
|
320 |
\begin{isamarkuptext}%
|
|
321 |
Let us conclude this section on partial functions by a
|
|
322 |
discussion of the merits of the \isa{while} combinator. We have
|
11494
|
323 |
already seen that the advantage of not having to
|
11310
|
324 |
provide a termination argument when defining a function via \isa{while} merely puts off the evil hour. On top of that, tail recursive
|
10654
|
325 |
functions tend to be more complicated to reason about. So why use
|
|
326 |
\isa{while} at all? The only reason is executability: the recursion
|
|
327 |
equation for \isa{while} is a directly executable functional
|
|
328 |
program. This is in stark contrast to guarded recursion as introduced
|
|
329 |
above which requires an explicit test \isa{x\ {\isasymin}\ dom\ f} in the
|
|
330 |
function body. Unless \isa{dom} is trivial, this leads to a
|
11196
|
331 |
definition that is impossible to execute or prohibitively slow.
|
10878
|
332 |
Thus, if you are aiming for an efficiently executable definition
|
10654
|
333 |
of a partial function, you are likely to need \isa{while}.%
|
|
334 |
\end{isamarkuptext}%
|
17175
|
335 |
\isamarkuptrue%
|
17056
|
336 |
%
|
|
337 |
\isadelimtheory
|
|
338 |
%
|
|
339 |
\endisadelimtheory
|
|
340 |
%
|
|
341 |
\isatagtheory
|
|
342 |
%
|
|
343 |
\endisatagtheory
|
|
344 |
{\isafoldtheory}%
|
|
345 |
%
|
|
346 |
\isadelimtheory
|
|
347 |
%
|
|
348 |
\endisadelimtheory
|
10654
|
349 |
\end{isabellebody}%
|
|
350 |
%%% Local Variables:
|
|
351 |
%%% mode: latex
|
|
352 |
%%% TeX-master: "root"
|
|
353 |
%%% End:
|