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