8 % |
8 % |
9 \isatagtheory |
9 \isatagtheory |
10 \isacommand{theory}\isamarkupfalse% |
10 \isacommand{theory}\isamarkupfalse% |
11 \ Inductive{\isacharunderscore}Predicate\isanewline |
11 \ Inductive{\isacharunderscore}Predicate\isanewline |
12 \isakeyword{imports}\ Setup\isanewline |
12 \isakeyword{imports}\ Setup\isanewline |
13 \isakeyword{begin}% |
13 \isakeyword{begin}\isanewline |
|
14 % |
14 \endisatagtheory |
15 \endisatagtheory |
15 {\isafoldtheory}% |
16 {\isafoldtheory}% |
16 % |
17 % |
17 \isadelimtheory |
18 \isadelimtheory |
18 % |
19 % |
19 \endisadelimtheory |
20 \endisadelimtheory |
20 % |
21 % |
|
22 \isadeliminvisible |
|
23 % |
|
24 \endisadeliminvisible |
|
25 % |
|
26 \isataginvisible |
|
27 % |
|
28 \endisataginvisible |
|
29 {\isafoldinvisible}% |
|
30 % |
|
31 \isadeliminvisible |
|
32 % |
|
33 \endisadeliminvisible |
|
34 % |
21 \isamarkupsection{Inductive Predicates \label{sec:inductive}% |
35 \isamarkupsection{Inductive Predicates \label{sec:inductive}% |
22 } |
36 } |
23 \isamarkuptrue% |
37 \isamarkuptrue% |
24 % |
38 % |
25 \begin{isamarkuptext}% |
39 \begin{isamarkuptext}% |
26 To execute inductive predicates, a special preprocessor, the predicate |
40 The \isa{predicate{\isacharunderscore}compiler} is an extension of the code generator |
27 compiler, generates code equations from the introduction rules of the predicates. |
41 which turns inductive specifications into equational ones, from |
28 The mechanisms of this compiler are described in \cite{Berghofer-Bulwahn-Haftmann:2009:TPHOL}. |
42 which in turn executable code can be generated. The mechanisms of |
29 Consider the simple predicate \isa{append} given by these two |
43 this compiler are described in detail in |
30 introduction rules:% |
44 \cite{Berghofer-Bulwahn-Haftmann:2009:TPHOL}. |
31 \end{isamarkuptext}% |
45 |
32 \isamarkuptrue% |
46 Consider the simple predicate \isa{append} given by these two |
33 % |
47 introduction rules:% |
34 \isadelimquote |
48 \end{isamarkuptext}% |
35 % |
49 \isamarkuptrue% |
36 \endisadelimquote |
50 % |
37 % |
51 \isadelimquote |
38 \isatagquote |
52 % |
39 % |
53 \endisadelimquote |
40 \begin{isamarkuptext}% |
54 % |
41 \isa{append\ {\isacharbrackleft}{\isacharbrackright}\ ys\ ys}\\ |
55 \isatagquote |
42 \noindent\isa{append\ xs\ ys\ zs\ {\isasymLongrightarrow}\ append\ {\isacharparenleft}x\ {\isacharhash}\ xs{\isacharparenright}\ ys\ {\isacharparenleft}x\ {\isacharhash}\ zs{\isacharparenright}}% |
56 % |
|
57 \begin{isamarkuptext}% |
|
58 \isa{append\ {\isacharbrackleft}{\isacharbrackright}\ ys\ ys} \\ |
|
59 \isa{append\ xs\ ys\ zs\ {\isasymLongrightarrow}\ append\ {\isacharparenleft}x\ {\isacharhash}\ xs{\isacharparenright}\ ys\ {\isacharparenleft}x\ {\isacharhash}\ zs{\isacharparenright}}% |
43 \end{isamarkuptext}% |
60 \end{isamarkuptext}% |
44 \isamarkuptrue% |
61 \isamarkuptrue% |
45 % |
62 % |
46 \endisatagquote |
63 \endisatagquote |
47 {\isafoldquote}% |
64 {\isafoldquote}% |
69 \isadelimquote |
86 \isadelimquote |
70 % |
87 % |
71 \endisadelimquote |
88 \endisadelimquote |
72 % |
89 % |
73 \begin{isamarkuptext}% |
90 \begin{isamarkuptext}% |
74 \noindent The \hyperlink{command.code-pred}{\mbox{\isa{\isacommand{code{\isacharunderscore}pred}}}} command takes the name |
91 \noindent The \hyperlink{command.code-pred}{\mbox{\isa{\isacommand{code{\isacharunderscore}pred}}}} command takes the name of the |
75 of the inductive predicate and then you put a period to discharge |
92 inductive predicate and then you put a period to discharge a trivial |
76 a trivial correctness proof. |
93 correctness proof. The compiler infers possible modes for the |
77 The compiler infers possible modes |
94 predicate and produces the derived code equations. Modes annotate |
78 for the predicate and produces the derived code equations. |
95 which (parts of the) arguments are to be taken as input, and which |
79 Modes annotate which (parts of the) arguments are to be taken as input, |
96 output. Modes are similar to types, but use the notation \isa{i} |
80 and which output. Modes are similar to types, but use the notation \isa{i} |
97 for input and \isa{o} for output. |
81 for input and \isa{o} for output. |
|
82 |
98 |
83 For \isa{append}, the compiler can infer the following modes: |
99 For \isa{append}, the compiler can infer the following modes: |
84 \begin{itemize} |
100 \begin{itemize} |
85 \item \isa{i\ {\isasymRightarrow}\ i\ {\isasymRightarrow}\ i\ {\isasymRightarrow}\ bool} |
101 \item \isa{i\ {\isasymRightarrow}\ i\ {\isasymRightarrow}\ i\ {\isasymRightarrow}\ bool} |
86 \item \isa{i\ {\isasymRightarrow}\ i\ {\isasymRightarrow}\ o\ {\isasymRightarrow}\ bool} |
102 \item \isa{i\ {\isasymRightarrow}\ i\ {\isasymRightarrow}\ o\ {\isasymRightarrow}\ bool} |
87 \item \isa{o\ {\isasymRightarrow}\ o\ {\isasymRightarrow}\ i\ {\isasymRightarrow}\ bool} |
103 \item \isa{o\ {\isasymRightarrow}\ o\ {\isasymRightarrow}\ i\ {\isasymRightarrow}\ bool} |
88 \end{itemize} |
104 \end{itemize} |
89 You can compute sets of predicates using \indexdef{}{command}{values}\hypertarget{command.values}{\hyperlink{command.values}{\mbox{\isa{\isacommand{values}}}}}:% |
105 You can compute sets of predicates using \indexdef{}{command}{values}\hypertarget{command.values}{\hyperlink{command.values}{\mbox{\isa{\isacommand{values}}}}}:% |
90 \end{isamarkuptext}% |
106 \end{isamarkuptext}% |
91 \isamarkuptrue% |
107 \isamarkuptrue% |
92 % |
108 % |
93 \isadelimquote |
109 \isadelimquote |
94 % |
110 % |
127 \noindent outputs \isa{{\isacharbraceleft}{\isacharparenleft}{\isacharbrackleft}{\isacharbrackright}{\isacharcomma}\ {\isacharbrackleft}{\isadigit{2}}{\isacharcomma}\ {\isadigit{3}}{\isacharbrackright}{\isacharparenright}{\isacharcomma}\ {\isacharparenleft}{\isacharbrackleft}{\isadigit{2}}{\isacharbrackright}{\isacharcomma}\ {\isacharbrackleft}{\isadigit{3}}{\isacharbrackright}{\isacharparenright}{\isacharcomma}\ {\isacharparenleft}{\isacharbrackleft}{\isadigit{2}}{\isacharcomma}\ {\isadigit{3}}{\isacharbrackright}{\isacharcomma}\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}{\isacharbraceright}}.% |
143 \noindent outputs \isa{{\isacharbraceleft}{\isacharparenleft}{\isacharbrackleft}{\isacharbrackright}{\isacharcomma}\ {\isacharbrackleft}{\isadigit{2}}{\isacharcomma}\ {\isadigit{3}}{\isacharbrackright}{\isacharparenright}{\isacharcomma}\ {\isacharparenleft}{\isacharbrackleft}{\isadigit{2}}{\isacharbrackright}{\isacharcomma}\ {\isacharbrackleft}{\isadigit{3}}{\isacharbrackright}{\isacharparenright}{\isacharcomma}\ {\isacharparenleft}{\isacharbrackleft}{\isadigit{2}}{\isacharcomma}\ {\isadigit{3}}{\isacharbrackright}{\isacharcomma}\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}{\isacharbraceright}}.% |
128 \end{isamarkuptext}% |
144 \end{isamarkuptext}% |
129 \isamarkuptrue% |
145 \isamarkuptrue% |
130 % |
146 % |
131 \begin{isamarkuptext}% |
147 \begin{isamarkuptext}% |
132 \noindent If you are only interested in the first elements of the set |
148 \noindent If you are only interested in the first elements of the |
133 comprehension (with respect to a depth-first search on the introduction rules), you can |
149 set comprehension (with respect to a depth-first search on the |
134 pass an argument to |
150 introduction rules), you can pass an argument to \hyperlink{command.values}{\mbox{\isa{\isacommand{values}}}} |
135 \hyperlink{command.values}{\mbox{\isa{\isacommand{values}}}} to specify the number of elements you want:% |
151 to specify the number of elements you want:% |
136 \end{isamarkuptext}% |
152 \end{isamarkuptext}% |
137 \isamarkuptrue% |
153 \isamarkuptrue% |
138 % |
154 % |
139 \isadelimquote |
155 \isadelimquote |
140 % |
156 % |
141 \endisadelimquote |
157 \endisadelimquote |
142 % |
158 % |
143 \isatagquote |
159 \isatagquote |
144 \isacommand{values}\isamarkupfalse% |
160 \isacommand{values}\isamarkupfalse% |
145 \ {\isadigit{1}}\ {\isachardoublequoteopen}{\isacharbraceleft}{\isacharparenleft}xs{\isacharcomma}\ ys{\isacharparenright}{\isachardot}\ append\ xs\ ys\ {\isacharbrackleft}{\isacharparenleft}{\isadigit{1}}{\isacharcolon}{\isacharcolon}nat{\isacharparenright}{\isacharcomma}{\isadigit{2}}{\isacharcomma}{\isadigit{3}}{\isacharcomma}{\isadigit{4}}{\isacharbrackright}{\isacharbraceright}{\isachardoublequoteclose}\isanewline |
161 \ {\isadigit{1}}\ {\isachardoublequoteopen}{\isacharbraceleft}{\isacharparenleft}xs{\isacharcomma}\ ys{\isacharparenright}{\isachardot}\ append\ xs\ ys\ {\isacharbrackleft}{\isacharparenleft}{\isadigit{1}}{\isacharcolon}{\isacharcolon}nat{\isacharparenright}{\isacharcomma}\ {\isadigit{2}}{\isacharcomma}\ {\isadigit{3}}{\isacharcomma}\ {\isadigit{4}}{\isacharbrackright}{\isacharbraceright}{\isachardoublequoteclose}\isanewline |
146 \isacommand{values}\isamarkupfalse% |
162 \isacommand{values}\isamarkupfalse% |
147 \ {\isadigit{3}}\ {\isachardoublequoteopen}{\isacharbraceleft}{\isacharparenleft}xs{\isacharcomma}\ ys{\isacharparenright}{\isachardot}\ append\ xs\ ys\ {\isacharbrackleft}{\isacharparenleft}{\isadigit{1}}{\isacharcolon}{\isacharcolon}nat{\isacharparenright}{\isacharcomma}{\isadigit{2}}{\isacharcomma}{\isadigit{3}}{\isacharcomma}{\isadigit{4}}{\isacharbrackright}{\isacharbraceright}{\isachardoublequoteclose}% |
163 \ {\isadigit{3}}\ {\isachardoublequoteopen}{\isacharbraceleft}{\isacharparenleft}xs{\isacharcomma}\ ys{\isacharparenright}{\isachardot}\ append\ xs\ ys\ {\isacharbrackleft}{\isacharparenleft}{\isadigit{1}}{\isacharcolon}{\isacharcolon}nat{\isacharparenright}{\isacharcomma}\ {\isadigit{2}}{\isacharcomma}\ {\isadigit{3}}{\isacharcomma}\ {\isadigit{4}}{\isacharbrackright}{\isacharbraceright}{\isachardoublequoteclose}% |
148 \endisatagquote |
164 \endisatagquote |
149 {\isafoldquote}% |
165 {\isafoldquote}% |
150 % |
166 % |
151 \isadelimquote |
167 \isadelimquote |
152 % |
168 % |
153 \endisadelimquote |
169 \endisadelimquote |
154 % |
170 % |
155 \begin{isamarkuptext}% |
171 \begin{isamarkuptext}% |
156 \noindent The \hyperlink{command.values}{\mbox{\isa{\isacommand{values}}}} command can only compute set |
172 \noindent The \hyperlink{command.values}{\mbox{\isa{\isacommand{values}}}} command can only compute set |
157 comprehensions for which a mode has been inferred. |
173 comprehensions for which a mode has been inferred. |
158 |
174 |
159 The code equations for a predicate are made available as theorems with |
175 The code equations for a predicate are made available as theorems with |
160 the suffix \isa{equation}, and can be inspected with:% |
176 the suffix \isa{equation}, and can be inspected with:% |
161 \end{isamarkuptext}% |
177 \end{isamarkuptext}% |
162 \isamarkuptrue% |
178 \isamarkuptrue% |
163 % |
179 % |
164 \isadelimquote |
180 \isadelimquote |
165 % |
181 % |
178 \begin{isamarkuptext}% |
194 \begin{isamarkuptext}% |
179 \noindent More advanced options are described in the following subsections.% |
195 \noindent More advanced options are described in the following subsections.% |
180 \end{isamarkuptext}% |
196 \end{isamarkuptext}% |
181 \isamarkuptrue% |
197 \isamarkuptrue% |
182 % |
198 % |
183 \isamarkupsubsubsection{Alternative names for functions% |
199 \isamarkupsubsection{Alternative names for functions% |
184 } |
200 } |
185 \isamarkuptrue% |
201 \isamarkuptrue% |
186 % |
202 % |
187 \begin{isamarkuptext}% |
203 \begin{isamarkuptext}% |
188 By default, the functions generated from a predicate are named after the predicate with the |
204 By default, the functions generated from a predicate are named after |
189 mode mangled into the name (e.g., \isa{append{\isacharunderscore}i{\isacharunderscore}i{\isacharunderscore}o}). |
205 the predicate with the mode mangled into the name (e.g., \isa{append{\isacharunderscore}i{\isacharunderscore}i{\isacharunderscore}o}). You can specify your own names as follows:% |
190 You can specify your own names as follows:% |
|
191 \end{isamarkuptext}% |
206 \end{isamarkuptext}% |
192 \isamarkuptrue% |
207 \isamarkuptrue% |
193 % |
208 % |
194 \isadelimquote |
209 \isadelimquote |
195 % |
210 % |
206 % |
221 % |
207 \isadelimquote |
222 \isadelimquote |
208 % |
223 % |
209 \endisadelimquote |
224 \endisadelimquote |
210 % |
225 % |
211 \isamarkupsubsubsection{Alternative introduction rules% |
226 \isamarkupsubsection{Alternative introduction rules% |
212 } |
227 } |
213 \isamarkuptrue% |
228 \isamarkuptrue% |
214 % |
229 % |
215 \begin{isamarkuptext}% |
230 \begin{isamarkuptext}% |
216 Sometimes the introduction rules of an predicate are not executable because they contain |
231 Sometimes the introduction rules of an predicate are not executable |
217 non-executable constants or specific modes could not be inferred. |
232 because they contain non-executable constants or specific modes |
218 It is also possible that the introduction rules yield a function that loops forever |
233 could not be inferred. It is also possible that the introduction |
219 due to the execution in a depth-first search manner. |
234 rules yield a function that loops forever due to the execution in a |
220 Therefore, you can declare alternative introduction rules for predicates with the attribute |
235 depth-first search manner. Therefore, you can declare alternative |
221 \hyperlink{attribute.code-pred-intro}{\mbox{\isa{code{\isacharunderscore}pred{\isacharunderscore}intro}}}. |
236 introduction rules for predicates with the attribute \hyperlink{attribute.code-pred-intro}{\mbox{\isa{code{\isacharunderscore}pred{\isacharunderscore}intro}}}. For example, the transitive closure is defined |
222 For example, the transitive closure is defined by:% |
237 by:% |
223 \end{isamarkuptext}% |
238 \end{isamarkuptext}% |
224 \isamarkuptrue% |
239 \isamarkuptrue% |
225 % |
240 % |
226 \isadelimquote |
241 \isadelimquote |
227 % |
242 % |
228 \endisadelimquote |
243 \endisadelimquote |
229 % |
244 % |
230 \isatagquote |
245 \isatagquote |
231 % |
246 % |
232 \begin{isamarkuptext}% |
247 \begin{isamarkuptext}% |
233 \isa{r\ a\ b\ {\isasymLongrightarrow}\ r\isactrlsup {\isacharplus}\isactrlsup {\isacharplus}\ a\ b}\\ |
248 \isa{r\ a\ b\ {\isasymLongrightarrow}\ r\isactrlsup {\isacharplus}\isactrlsup {\isacharplus}\ a\ b} \\ |
234 \noindent \isa{{\isasymlbrakk}r\isactrlsup {\isacharplus}\isactrlsup {\isacharplus}\ a\ b{\isacharsemicolon}\ r\ b\ c{\isasymrbrakk}\ {\isasymLongrightarrow}\ r\isactrlsup {\isacharplus}\isactrlsup {\isacharplus}\ a\ c}% |
249 \isa{r\isactrlsup {\isacharplus}\isactrlsup {\isacharplus}\ a\ b\ {\isasymLongrightarrow}\ r\ b\ c\ {\isasymLongrightarrow}\ r\isactrlsup {\isacharplus}\isactrlsup {\isacharplus}\ a\ c}% |
235 \end{isamarkuptext}% |
250 \end{isamarkuptext}% |
236 \isamarkuptrue% |
251 \isamarkuptrue% |
237 % |
252 % |
238 \endisatagquote |
253 \endisatagquote |
239 {\isafoldquote}% |
254 {\isafoldquote}% |
240 % |
255 % |
241 \isadelimquote |
256 \isadelimquote |
242 % |
257 % |
243 \endisadelimquote |
258 \endisadelimquote |
244 % |
259 % |
245 \begin{isamarkuptext}% |
260 \begin{isamarkuptext}% |
246 \noindent These rules do not suit well for executing the transitive closure |
261 \noindent These rules do not suit well for executing the transitive |
247 with the mode \isa{{\isacharparenleft}i\ {\isasymRightarrow}\ o\ {\isasymRightarrow}\ bool{\isacharparenright}\ {\isasymRightarrow}\ i\ {\isasymRightarrow}\ o\ {\isasymRightarrow}\ bool}, as the second rule will |
262 closure with the mode \isa{{\isacharparenleft}i\ {\isasymRightarrow}\ o\ {\isasymRightarrow}\ bool{\isacharparenright}\ {\isasymRightarrow}\ i\ {\isasymRightarrow}\ o\ {\isasymRightarrow}\ bool}, as |
248 cause an infinite loop in the recursive call. |
263 the second rule will cause an infinite loop in the recursive call. |
249 This can be avoided using the following alternative rules which are |
264 This can be avoided using the following alternative rules which are |
250 declared to the predicate compiler by the attribute \hyperlink{attribute.code-pred-intro}{\mbox{\isa{code{\isacharunderscore}pred{\isacharunderscore}intro}}}:% |
265 declared to the predicate compiler by the attribute \hyperlink{attribute.code-pred-intro}{\mbox{\isa{code{\isacharunderscore}pred{\isacharunderscore}intro}}}:% |
251 \end{isamarkuptext}% |
266 \end{isamarkuptext}% |
252 \isamarkuptrue% |
267 \isamarkuptrue% |
253 % |
268 % |
254 \isadelimquote |
269 \isadelimquote |
255 % |
270 % |
268 \isadelimquote |
283 \isadelimquote |
269 % |
284 % |
270 \endisadelimquote |
285 \endisadelimquote |
271 % |
286 % |
272 \begin{isamarkuptext}% |
287 \begin{isamarkuptext}% |
273 \noindent After declaring all alternative rules for the transitive closure, |
288 \noindent After declaring all alternative rules for the transitive |
274 you invoke \hyperlink{command.code-pred}{\mbox{\isa{\isacommand{code{\isacharunderscore}pred}}}} as usual. |
289 closure, you invoke \hyperlink{command.code-pred}{\mbox{\isa{\isacommand{code{\isacharunderscore}pred}}}} as usual. As you have |
275 As you have declared alternative rules for the predicate, you are urged to prove that these |
290 declared alternative rules for the predicate, you are urged to prove |
276 introduction rules are complete, i.e., that you can derive an elimination rule for the |
291 that these introduction rules are complete, i.e., that you can |
277 alternative rules:% |
292 derive an elimination rule for the alternative rules:% |
278 \end{isamarkuptext}% |
293 \end{isamarkuptext}% |
279 \isamarkuptrue% |
294 \isamarkuptrue% |
280 % |
295 % |
281 \isadelimquote |
296 \isadelimquote |
282 % |
297 % |
288 \isacommand{proof}\isamarkupfalse% |
303 \isacommand{proof}\isamarkupfalse% |
289 \ {\isacharminus}\isanewline |
304 \ {\isacharminus}\isanewline |
290 \ \ \isacommand{case}\isamarkupfalse% |
305 \ \ \isacommand{case}\isamarkupfalse% |
291 \ tranclp\isanewline |
306 \ tranclp\isanewline |
292 \ \ \isacommand{from}\isamarkupfalse% |
307 \ \ \isacommand{from}\isamarkupfalse% |
293 \ this\ converse{\isacharunderscore}tranclpE{\isacharbrackleft}OF\ this{\isacharparenleft}{\isadigit{1}}{\isacharparenright}{\isacharbrackright}\ \isacommand{show}\isamarkupfalse% |
308 \ this\ converse{\isacharunderscore}tranclpE\ {\isacharbrackleft}OF\ this{\isacharparenleft}{\isadigit{1}}{\isacharparenright}{\isacharbrackright}\ \isacommand{show}\isamarkupfalse% |
294 \ thesis\ \isacommand{by}\isamarkupfalse% |
309 \ thesis\ \isacommand{by}\isamarkupfalse% |
295 \ metis\isanewline |
310 \ metis\isanewline |
296 \isacommand{qed}\isamarkupfalse% |
311 \isacommand{qed}\isamarkupfalse% |
297 % |
312 % |
298 \endisatagquote |
313 \endisatagquote |
370 % |
372 % |
371 \isadelimquote |
373 \isadelimquote |
372 % |
374 % |
373 \endisadelimquote |
375 \endisadelimquote |
374 % |
376 % |
375 \isamarkupsubsubsection{Options for values% |
377 \isamarkupsubsection{Options for values% |
376 } |
378 } |
377 \isamarkuptrue% |
379 \isamarkuptrue% |
378 % |
380 % |
379 \begin{isamarkuptext}% |
381 \begin{isamarkuptext}% |
380 In the presence of higher-order predicates, multiple modes for some predicate could be inferred |
382 In the presence of higher-order predicates, multiple modes for some |
381 that are not disambiguated by the pattern of the set comprehension. |
383 predicate could be inferred that are not disambiguated by the |
382 To disambiguate the modes for the arguments of a predicate, you can state |
384 pattern of the set comprehension. To disambiguate the modes for the |
383 the modes explicitly in the \hyperlink{command.values}{\mbox{\isa{\isacommand{values}}}} command. |
385 arguments of a predicate, you can state the modes explicitly in the |
384 Consider the simple predicate \isa{succ}:% |
386 \hyperlink{command.values}{\mbox{\isa{\isacommand{values}}}} command. Consider the simple predicate \isa{succ}:% |
385 \end{isamarkuptext}% |
387 \end{isamarkuptext}% |
386 \isamarkuptrue% |
388 \isamarkuptrue% |
|
389 % |
|
390 \isadelimquote |
|
391 % |
|
392 \endisadelimquote |
|
393 % |
|
394 \isatagquote |
387 \isacommand{inductive}\isamarkupfalse% |
395 \isacommand{inductive}\isamarkupfalse% |
388 \ succ\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}nat\ {\isasymRightarrow}\ nat\ {\isasymRightarrow}\ bool{\isachardoublequoteclose}\isanewline |
396 \ succ\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}nat\ {\isasymRightarrow}\ nat\ {\isasymRightarrow}\ bool{\isachardoublequoteclose}\ \isakeyword{where}\isanewline |
389 \isakeyword{where}\isanewline |
|
390 \ \ {\isachardoublequoteopen}succ\ {\isadigit{0}}\ {\isacharparenleft}Suc\ {\isadigit{0}}{\isacharparenright}{\isachardoublequoteclose}\isanewline |
397 \ \ {\isachardoublequoteopen}succ\ {\isadigit{0}}\ {\isacharparenleft}Suc\ {\isadigit{0}}{\isacharparenright}{\isachardoublequoteclose}\isanewline |
391 {\isacharbar}\ {\isachardoublequoteopen}succ\ x\ y\ {\isasymLongrightarrow}\ succ\ {\isacharparenleft}Suc\ x{\isacharparenright}\ {\isacharparenleft}Suc\ y{\isacharparenright}{\isachardoublequoteclose}\isanewline |
398 {\isacharbar}\ {\isachardoublequoteopen}succ\ x\ y\ {\isasymLongrightarrow}\ succ\ {\isacharparenleft}Suc\ x{\isacharparenright}\ {\isacharparenleft}Suc\ y{\isacharparenright}{\isachardoublequoteclose}\isanewline |
392 \isanewline |
399 \isanewline |
393 \isacommand{code{\isacharunderscore}pred}\isamarkupfalse% |
400 \isacommand{code{\isacharunderscore}pred}\isamarkupfalse% |
394 \ succ% |
401 \ succ\ \isacommand{{\isachardot}}\isamarkupfalse% |
395 \isadelimproof |
402 % |
396 \ % |
403 \endisatagquote |
397 \endisadelimproof |
404 {\isafoldquote}% |
398 % |
405 % |
399 \isatagproof |
406 \isadelimquote |
400 \isacommand{{\isachardot}}\isamarkupfalse% |
407 % |
401 % |
408 \endisadelimquote |
402 \endisatagproof |
409 % |
403 {\isafoldproof}% |
410 \begin{isamarkuptext}% |
404 % |
411 \noindent For this, the predicate compiler can infer modes \isa{o\ {\isasymRightarrow}\ o\ {\isasymRightarrow}\ bool}, \isa{i\ {\isasymRightarrow}\ o\ {\isasymRightarrow}\ bool}, \isa{o\ {\isasymRightarrow}\ i\ {\isasymRightarrow}\ bool} and |
405 \isadelimproof |
412 \isa{i\ {\isasymRightarrow}\ i\ {\isasymRightarrow}\ bool}. The invocation of \hyperlink{command.values}{\mbox{\isa{\isacommand{values}}}} |
406 % |
413 \isa{{\isacharbraceleft}n{\isachardot}\ tranclp\ succ\ {\isadigit{1}}{\isadigit{0}}\ n{\isacharbraceright}} loops, as multiple modes for the |
407 \endisadelimproof |
414 predicate \isa{succ} are possible and here the first mode \isa{o\ {\isasymRightarrow}\ o\ {\isasymRightarrow}\ bool} is chosen. To choose another mode for the argument, |
408 % |
415 you can declare the mode for the argument between the \hyperlink{command.values}{\mbox{\isa{\isacommand{values}}}} and the number of elements.% |
409 \begin{isamarkuptext}% |
|
410 \noindent For this, the predicate compiler can infer modes \isa{o\ {\isasymRightarrow}\ o\ {\isasymRightarrow}\ bool}, \isa{i\ {\isasymRightarrow}\ o\ {\isasymRightarrow}\ bool}, |
|
411 \isa{o\ {\isasymRightarrow}\ i\ {\isasymRightarrow}\ bool} and \isa{i\ {\isasymRightarrow}\ i\ {\isasymRightarrow}\ bool}. |
|
412 The invocation of \hyperlink{command.values}{\mbox{\isa{\isacommand{values}}}} \isa{{\isacharbraceleft}n{\isachardot}\ tranclp\ succ\ {\isadigit{1}}{\isadigit{0}}\ n{\isacharbraceright}} loops, as multiple |
|
413 modes for the predicate \isa{succ} are possible and here the first mode \isa{o\ {\isasymRightarrow}\ o\ {\isasymRightarrow}\ bool} |
|
414 is chosen. To choose another mode for the argument, you can declare the mode for the argument between |
|
415 the \hyperlink{command.values}{\mbox{\isa{\isacommand{values}}}} and the number of elements.% |
|
416 \end{isamarkuptext}% |
416 \end{isamarkuptext}% |
417 \isamarkuptrue% |
417 \isamarkuptrue% |
418 % |
418 % |
419 \isadelimquote |
419 \isadelimquote |
420 % |
420 % |
430 % |
430 % |
431 \isadelimquote |
431 \isadelimquote |
432 % |
432 % |
433 \endisadelimquote |
433 \endisadelimquote |
434 % |
434 % |
435 \isamarkupsubsubsection{Embedding into functional code within Isabelle/HOL% |
435 \isamarkupsubsection{Embedding into functional code within Isabelle/HOL% |
436 } |
436 } |
437 \isamarkuptrue% |
437 \isamarkuptrue% |
438 % |
438 % |
439 \begin{isamarkuptext}% |
439 \begin{isamarkuptext}% |
440 To embed the computation of an inductive predicate into functions that are defined in Isabelle/HOL, |
440 To embed the computation of an inductive predicate into functions |
441 you have a number of options: |
441 that are defined in Isabelle/HOL, you have a number of options: |
442 \begin{itemize} |
442 |
443 \item You want to use the first-order predicate with the mode |
443 \begin{itemize} |
444 where all arguments are input. Then you can use the predicate directly, e.g. |
444 |
445 \begin{quote} |
445 \item You want to use the first-order predicate with the mode |
446 \isa{valid{\isacharunderscore}suffix\ ys\ zs\ {\isacharequal}}\\ |
446 where all arguments are input. Then you can use the predicate directly, e.g. |
447 \isa{{\isacharparenleft}if\ append\ {\isacharbrackleft}Suc\ {\isadigit{0}}{\isacharcomma}\ {\isadigit{2}}{\isacharbrackright}\ ys\ zs\ then\ Some\ ys\ else\ None{\isacharparenright}} |
447 |
448 \end{quote} |
448 \begin{quote} |
449 \item If you know that the execution returns only one value (it is deterministic), then you can |
449 \isa{valid{\isacharunderscore}suffix\ ys\ zs\ {\isacharequal}} \\ |
450 use the combinator \isa{Predicate{\isachardot}the}, e.g., a functional concatenation of lists |
450 \isa{{\isacharparenleft}if\ append\ {\isacharbrackleft}Suc\ {\isadigit{0}}{\isacharcomma}\ {\isadigit{2}}{\isacharbrackright}\ ys\ zs\ then\ Some\ ys\ else\ None{\isacharparenright}} |
451 is defined with |
451 \end{quote} |
452 \begin{quote} |
452 |
453 \isa{functional{\isacharunderscore}concat\ xs\ ys\ {\isacharequal}\ Predicate{\isachardot}the\ {\isacharparenleft}append{\isacharunderscore}i{\isacharunderscore}i{\isacharunderscore}o\ xs\ ys{\isacharparenright}} |
453 \item If you know that the execution returns only one value (it is |
454 \end{quote} |
454 deterministic), then you can use the combinator \isa{Predicate{\isachardot}the}, e.g., a functional concatenation of lists is |
455 Note that if the evaluation does not return a unique value, it raises a run-time error |
455 defined with |
456 \isa{not{\isacharunderscore}unique}. |
456 |
457 \end{itemize}% |
457 \begin{quote} |
458 \end{isamarkuptext}% |
458 \isa{functional{\isacharunderscore}concat\ xs\ ys\ {\isacharequal}\ Predicate{\isachardot}the\ {\isacharparenleft}append{\isacharunderscore}i{\isacharunderscore}i{\isacharunderscore}o\ xs\ ys{\isacharparenright}} |
459 \isamarkuptrue% |
459 \end{quote} |
460 % |
460 |
461 \isamarkupsubsubsection{Further Examples% |
461 Note that if the evaluation does not return a unique value, it |
|
462 raises a run-time error \isa{not{\isacharunderscore}unique}. |
|
463 |
|
464 \end{itemize}% |
|
465 \end{isamarkuptext}% |
|
466 \isamarkuptrue% |
|
467 % |
|
468 \isamarkupsubsection{Further Examples% |
462 } |
469 } |
463 \isamarkuptrue% |
470 \isamarkuptrue% |
464 % |
471 % |
465 \begin{isamarkuptext}% |
472 \begin{isamarkuptext}% |
466 Further examples for compiling inductive predicates can be found in |
473 Further examples for compiling inductive predicates can be found in |
467 the \isa{HOL{\isacharslash}ex{\isacharslash}Predicate{\isacharunderscore}Compile{\isacharunderscore}ex} theory file. |
474 the \isa{HOL{\isacharslash}ex{\isacharslash}Predicate{\isacharunderscore}Compile{\isacharunderscore}ex{\isacharcomma}thy} theory file. There are |
468 There are also some examples in the Archive of Formal Proofs, notably |
475 also some examples in the Archive of Formal Proofs, notably in the |
469 in the \isa{POPLmark{\isacharminus}deBruijn} and the \isa{FeatherweightJava} sessions.% |
476 \isa{POPLmark{\isacharminus}deBruijn} and the \isa{FeatherweightJava} |
|
477 sessions.% |
470 \end{isamarkuptext}% |
478 \end{isamarkuptext}% |
471 \isamarkuptrue% |
479 \isamarkuptrue% |
472 % |
480 % |
473 \isadelimtheory |
481 \isadelimtheory |
474 % |
482 % |