author | bulwahn |
Mon, 30 Nov 2009 08:44:08 +0100 | |
changeset 33926 | dd017d9db05f |
parent 33707 | 68841fb382e0 |
child 34155 | 14aaccb399b3 |
permissions | -rw-r--r-- |
28213 | 1 |
theory Program |
28419 | 2 |
imports Introduction |
28213 | 3 |
begin |
4 |
||
28419 | 5 |
section {* Turning Theories into Programs \label{sec:program} *} |
28213 | 6 |
|
7 |
subsection {* The @{text "Isabelle/HOL"} default setup *} |
|
8 |
||
28419 | 9 |
text {* |
10 |
We have already seen how by default equations stemming from |
|
11 |
@{command definition}/@{command primrec}/@{command fun} |
|
28447 | 12 |
statements are used for code generation. This default behaviour |
29560 | 13 |
can be changed, e.g. by providing different code equations. |
28593 | 14 |
All kinds of customisation shown in this section is \emph{safe} |
28447 | 15 |
in the sense that the user does not have to worry about |
16 |
correctness -- all programs generatable that way are partially |
|
17 |
correct. |
|
18 |
*} |
|
19 |
||
20 |
subsection {* Selecting code equations *} |
|
21 |
||
22 |
text {* |
|
23 |
Coming back to our introductory example, we |
|
29560 | 24 |
could provide an alternative code equations for @{const dequeue} |
28447 | 25 |
explicitly: |
28419 | 26 |
*} |
27 |
||
28564 | 28 |
lemma %quote [code]: |
29798 | 29 |
"dequeue (AQueue xs []) = |
30 |
(if xs = [] then (None, AQueue [] []) |
|
31 |
else dequeue (AQueue [] (rev xs)))" |
|
32 |
"dequeue (AQueue xs (y # ys)) = |
|
33 |
(Some y, AQueue xs ys)" |
|
28419 | 34 |
by (cases xs, simp_all) (cases "rev xs", simp_all) |
35 |
||
36 |
text {* |
|
28562 | 37 |
\noindent The annotation @{text "[code]"} is an @{text Isar} |
28419 | 38 |
@{text attribute} which states that the given theorems should be |
29560 | 39 |
considered as code equations for a @{text fun} statement -- |
28419 | 40 |
the corresponding constant is determined syntactically. The resulting code: |
41 |
*} |
|
42 |
||
28564 | 43 |
text %quote {*@{code_stmts dequeue (consts) dequeue (Haskell)}*} |
28419 | 44 |
|
45 |
text {* |
|
46 |
\noindent You may note that the equality test @{term "xs = []"} has been |
|
47 |
replaced by the predicate @{term "null xs"}. This is due to the default |
|
48 |
setup in the \qn{preprocessor} to be discussed further below (\secref{sec:preproc}). |
|
49 |
||
50 |
Changing the default constructor set of datatypes is also |
|
29794 | 51 |
possible. See \secref{sec:datatypes} for an example. |
28419 | 52 |
|
53 |
As told in \secref{sec:concept}, code generation is based |
|
54 |
on a structured collection of code theorems. |
|
55 |
For explorative purpose, this collection |
|
56 |
may be inspected using the @{command code_thms} command: |
|
57 |
*} |
|
58 |
||
28564 | 59 |
code_thms %quote dequeue |
28419 | 60 |
|
61 |
text {* |
|
29560 | 62 |
\noindent prints a table with \emph{all} code equations |
28419 | 63 |
for @{const dequeue}, including |
29560 | 64 |
\emph{all} code equations those equations depend |
28419 | 65 |
on recursively. |
66 |
||
67 |
Similarly, the @{command code_deps} command shows a graph |
|
29560 | 68 |
visualising dependencies between code equations. |
28419 | 69 |
*} |
70 |
||
71 |
subsection {* @{text class} and @{text instantiation} *} |
|
72 |
||
73 |
text {* |
|
28447 | 74 |
Concerning type classes and code generation, let us examine an example |
28419 | 75 |
from abstract algebra: |
76 |
*} |
|
77 |
||
29794 | 78 |
class %quote semigroup = |
28419 | 79 |
fixes mult :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "\<otimes>" 70) |
80 |
assumes assoc: "(x \<otimes> y) \<otimes> z = x \<otimes> (y \<otimes> z)" |
|
81 |
||
28564 | 82 |
class %quote monoid = semigroup + |
28419 | 83 |
fixes neutral :: 'a ("\<one>") |
84 |
assumes neutl: "\<one> \<otimes> x = x" |
|
85 |
and neutr: "x \<otimes> \<one> = x" |
|
86 |
||
28564 | 87 |
instantiation %quote nat :: monoid |
28419 | 88 |
begin |
89 |
||
28564 | 90 |
primrec %quote mult_nat where |
28419 | 91 |
"0 \<otimes> n = (0\<Colon>nat)" |
92 |
| "Suc m \<otimes> n = n + m \<otimes> n" |
|
93 |
||
28564 | 94 |
definition %quote neutral_nat where |
28419 | 95 |
"\<one> = Suc 0" |
28213 | 96 |
|
28564 | 97 |
lemma %quote add_mult_distrib: |
28419 | 98 |
fixes n m q :: nat |
99 |
shows "(n + m) \<otimes> q = n \<otimes> q + m \<otimes> q" |
|
100 |
by (induct n) simp_all |
|
101 |
||
28564 | 102 |
instance %quote proof |
28419 | 103 |
fix m n q :: nat |
104 |
show "m \<otimes> n \<otimes> q = m \<otimes> (n \<otimes> q)" |
|
105 |
by (induct m) (simp_all add: add_mult_distrib) |
|
106 |
show "\<one> \<otimes> n = n" |
|
107 |
by (simp add: neutral_nat_def) |
|
108 |
show "m \<otimes> \<one> = m" |
|
109 |
by (induct m) (simp_all add: neutral_nat_def) |
|
110 |
qed |
|
111 |
||
28564 | 112 |
end %quote |
28419 | 113 |
|
114 |
text {* |
|
115 |
\noindent We define the natural operation of the natural numbers |
|
116 |
on monoids: |
|
117 |
*} |
|
118 |
||
28564 | 119 |
primrec %quote (in monoid) pow :: "nat \<Rightarrow> 'a \<Rightarrow> 'a" where |
28419 | 120 |
"pow 0 a = \<one>" |
121 |
| "pow (Suc n) a = a \<otimes> pow n a" |
|
122 |
||
123 |
text {* |
|
124 |
\noindent This we use to define the discrete exponentiation function: |
|
125 |
*} |
|
126 |
||
28564 | 127 |
definition %quote bexp :: "nat \<Rightarrow> nat" where |
28419 | 128 |
"bexp n = pow n (Suc (Suc 0))" |
129 |
||
130 |
text {* |
|
131 |
\noindent The corresponding code: |
|
132 |
*} |
|
133 |
||
28564 | 134 |
text %quote {*@{code_stmts bexp (Haskell)}*} |
28419 | 135 |
|
136 |
text {* |
|
28447 | 137 |
\noindent This is a convenient place to show how explicit dictionary construction |
28419 | 138 |
manifests in generated code (here, the same example in @{text SML}): |
139 |
*} |
|
140 |
||
28564 | 141 |
text %quote {*@{code_stmts bexp (SML)}*} |
28419 | 142 |
|
28447 | 143 |
text {* |
144 |
\noindent Note the parameters with trailing underscore (@{verbatim "A_"}) |
|
145 |
which are the dictionary parameters. |
|
146 |
*} |
|
28419 | 147 |
|
148 |
subsection {* The preprocessor \label{sec:preproc} *} |
|
149 |
||
150 |
text {* |
|
151 |
Before selected function theorems are turned into abstract |
|
152 |
code, a chain of definitional transformation steps is carried |
|
153 |
out: \emph{preprocessing}. In essence, the preprocessor |
|
154 |
consists of two components: a \emph{simpset} and \emph{function transformers}. |
|
155 |
||
32000 | 156 |
The \emph{simpset} allows to employ the full generality of the |
157 |
Isabelle simplifier. Due to the interpretation of theorems as code |
|
158 |
equations, rewrites are applied to the right hand side and the |
|
159 |
arguments of the left hand side of an equation, but never to the |
|
160 |
constant heading the left hand side. An important special case are |
|
161 |
\emph{unfold theorems} which may be declared and undeclared using |
|
162 |
the @{attribute code_unfold} or \emph{@{attribute code_unfold} del} |
|
163 |
attribute respectively. |
|
28213 | 164 |
|
28419 | 165 |
Some common applications: |
166 |
*} |
|
167 |
||
168 |
text_raw {* |
|
169 |
\begin{itemize} |
|
170 |
*} |
|
171 |
||
172 |
text {* |
|
173 |
\item replacing non-executable constructs by executable ones: |
|
174 |
*} |
|
175 |
||
32000 | 176 |
lemma %quote [code_inline]: |
28419 | 177 |
"x \<in> set xs \<longleftrightarrow> x mem xs" by (induct xs) simp_all |
178 |
||
179 |
text {* |
|
180 |
\item eliminating superfluous constants: |
|
181 |
*} |
|
182 |
||
32000 | 183 |
lemma %quote [code_inline]: |
28419 | 184 |
"1 = Suc 0" by simp |
185 |
||
186 |
text {* |
|
187 |
\item replacing executable but inconvenient constructs: |
|
188 |
*} |
|
189 |
||
32000 | 190 |
lemma %quote [code_inline]: |
28419 | 191 |
"xs = [] \<longleftrightarrow> List.null xs" by (induct xs) simp_all |
192 |
||
193 |
text_raw {* |
|
194 |
\end{itemize} |
|
195 |
*} |
|
196 |
||
197 |
text {* |
|
28447 | 198 |
\noindent \emph{Function transformers} provide a very general interface, |
28419 | 199 |
transforming a list of function theorems to another |
200 |
list of function theorems, provided that neither the heading |
|
201 |
constant nor its type change. The @{term "0\<Colon>nat"} / @{const Suc} |
|
202 |
pattern elimination implemented in |
|
203 |
theory @{text Efficient_Nat} (see \secref{eff_nat}) uses this |
|
204 |
interface. |
|
205 |
||
206 |
\noindent The current setup of the preprocessor may be inspected using |
|
31254 | 207 |
the @{command print_codeproc} command. |
28419 | 208 |
@{command code_thms} provides a convenient |
209 |
mechanism to inspect the impact of a preprocessor setup |
|
29560 | 210 |
on code equations. |
28419 | 211 |
|
212 |
\begin{warn} |
|
32000 | 213 |
|
214 |
Attribute @{attribute code_unfold} also applies to the |
|
215 |
preprocessor of the ancient @{text "SML code generator"}; in case |
|
216 |
this is not what you intend, use @{attribute code_inline} instead. |
|
28419 | 217 |
\end{warn} |
218 |
*} |
|
219 |
||
220 |
subsection {* Datatypes \label{sec:datatypes} *} |
|
221 |
||
222 |
text {* |
|
223 |
Conceptually, any datatype is spanned by a set of |
|
29794 | 224 |
\emph{constructors} of type @{text "\<tau> = \<dots> \<Rightarrow> \<kappa> \<alpha>\<^isub>1 \<dots> \<alpha>\<^isub>n"} where @{text |
225 |
"{\<alpha>\<^isub>1, \<dots>, \<alpha>\<^isub>n}"} is exactly the set of \emph{all} type variables in |
|
226 |
@{text "\<tau>"}. The HOL datatype package by default registers any new |
|
227 |
datatype in the table of datatypes, which may be inspected using the |
|
228 |
@{command print_codesetup} command. |
|
28419 | 229 |
|
29794 | 230 |
In some cases, it is appropriate to alter or extend this table. As |
231 |
an example, we will develop an alternative representation of the |
|
232 |
queue example given in \secref{sec:intro}. The amortised |
|
233 |
representation is convenient for generating code but exposes its |
|
234 |
\qt{implementation} details, which may be cumbersome when proving |
|
235 |
theorems about it. Therefore, here a simple, straightforward |
|
236 |
representation of queues: |
|
28419 | 237 |
*} |
238 |
||
29794 | 239 |
datatype %quote 'a queue = Queue "'a list" |
240 |
||
241 |
definition %quote empty :: "'a queue" where |
|
242 |
"empty = Queue []" |
|
28419 | 243 |
|
29794 | 244 |
primrec %quote enqueue :: "'a \<Rightarrow> 'a queue \<Rightarrow> 'a queue" where |
245 |
"enqueue x (Queue xs) = Queue (xs @ [x])" |
|
246 |
||
247 |
fun %quote dequeue :: "'a queue \<Rightarrow> 'a option \<times> 'a queue" where |
|
248 |
"dequeue (Queue []) = (None, Queue [])" |
|
249 |
| "dequeue (Queue (x # xs)) = (Some x, Queue xs)" |
|
28213 | 250 |
|
28419 | 251 |
text {* |
29794 | 252 |
\noindent This we can use directly for proving; for executing, |
253 |
we provide an alternative characterisation: |
|
28419 | 254 |
*} |
255 |
||
29794 | 256 |
definition %quote AQueue :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a queue" where |
257 |
"AQueue xs ys = Queue (ys @ rev xs)" |
|
258 |
||
259 |
code_datatype %quote AQueue |
|
260 |
||
29798 | 261 |
text {* |
262 |
\noindent Here we define a \qt{constructor} @{const "AQueue"} which |
|
263 |
is defined in terms of @{text "Queue"} and interprets its arguments |
|
264 |
according to what the \emph{content} of an amortised queue is supposed |
|
265 |
to be. Equipped with this, we are able to prove the following equations |
|
266 |
for our primitive queue operations which \qt{implement} the simple |
|
267 |
queues in an amortised fashion: |
|
268 |
*} |
|
29794 | 269 |
|
270 |
lemma %quote empty_AQueue [code]: |
|
271 |
"empty = AQueue [] []" |
|
272 |
unfolding AQueue_def empty_def by simp |
|
273 |
||
274 |
lemma %quote enqueue_AQueue [code]: |
|
275 |
"enqueue x (AQueue xs ys) = AQueue (x # xs) ys" |
|
276 |
unfolding AQueue_def by simp |
|
28419 | 277 |
|
29794 | 278 |
lemma %quote dequeue_AQueue [code]: |
279 |
"dequeue (AQueue xs []) = |
|
29798 | 280 |
(if xs = [] then (None, AQueue [] []) |
281 |
else dequeue (AQueue [] (rev xs)))" |
|
29794 | 282 |
"dequeue (AQueue xs (y # ys)) = (Some y, AQueue xs ys)" |
283 |
unfolding AQueue_def by simp_all |
|
284 |
||
29798 | 285 |
text {* |
286 |
\noindent For completeness, we provide a substitute for the |
|
287 |
@{text case} combinator on queues: |
|
288 |
*} |
|
29794 | 289 |
|
30227 | 290 |
lemma %quote queue_case_AQueue [code]: |
291 |
"queue_case f (AQueue xs ys) = f (ys @ rev xs)" |
|
292 |
unfolding AQueue_def by simp |
|
29794 | 293 |
|
29798 | 294 |
text {* |
295 |
\noindent The resulting code looks as expected: |
|
296 |
*} |
|
29794 | 297 |
|
298 |
text %quote {*@{code_stmts empty enqueue dequeue (SML)}*} |
|
28419 | 299 |
|
300 |
text {* |
|
29794 | 301 |
\noindent From this example, it can be glimpsed that using own |
302 |
constructor sets is a little delicate since it changes the set of |
|
303 |
valid patterns for values of that type. Without going into much |
|
304 |
detail, here some practical hints: |
|
28419 | 305 |
|
306 |
\begin{itemize} |
|
29794 | 307 |
|
308 |
\item When changing the constructor set for datatypes, take care |
|
30227 | 309 |
to provide alternative equations for the @{text case} combinator. |
29794 | 310 |
|
311 |
\item Values in the target language need not to be normalised -- |
|
312 |
different values in the target language may represent the same |
|
313 |
value in the logic. |
|
314 |
||
315 |
\item Usually, a good methodology to deal with the subtleties of |
|
316 |
pattern matching is to see the type as an abstract type: provide |
|
317 |
a set of operations which operate on the concrete representation |
|
318 |
of the type, and derive further operations by combinations of |
|
319 |
these primitive ones, without relying on a particular |
|
320 |
representation. |
|
321 |
||
28419 | 322 |
\end{itemize} |
323 |
*} |
|
324 |
||
28213 | 325 |
|
30938
c6c9359e474c
wellsortedness is no issue for a user manual any more
haftmann
parents:
30227
diff
changeset
|
326 |
subsection {* Equality *} |
28213 | 327 |
|
28419 | 328 |
text {* |
329 |
Surely you have already noticed how equality is treated |
|
330 |
by the code generator: |
|
331 |
*} |
|
332 |
||
28564 | 333 |
primrec %quote collect_duplicates :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list \<Rightarrow> 'a list" where |
28447 | 334 |
"collect_duplicates xs ys [] = xs" |
28419 | 335 |
| "collect_duplicates xs ys (z#zs) = (if z \<in> set xs |
336 |
then if z \<in> set ys |
|
337 |
then collect_duplicates xs ys zs |
|
338 |
else collect_duplicates xs (z#ys) zs |
|
339 |
else collect_duplicates (z#xs) (z#ys) zs)" |
|
340 |
||
341 |
text {* |
|
28428 | 342 |
\noindent The membership test during preprocessing is rewritten, |
28419 | 343 |
resulting in @{const List.member}, which itself |
344 |
performs an explicit equality check. |
|
345 |
*} |
|
346 |
||
28564 | 347 |
text %quote {*@{code_stmts collect_duplicates (SML)}*} |
28419 | 348 |
|
349 |
text {* |
|
350 |
\noindent Obviously, polymorphic equality is implemented the Haskell |
|
351 |
way using a type class. How is this achieved? HOL introduces |
|
352 |
an explicit class @{class eq} with a corresponding operation |
|
353 |
@{const eq_class.eq} such that @{thm eq [no_vars]}. |
|
28447 | 354 |
The preprocessing framework does the rest by propagating the |
29560 | 355 |
@{class eq} constraints through all dependent code equations. |
28419 | 356 |
For datatypes, instances of @{class eq} are implicitly derived |
357 |
when possible. For other types, you may instantiate @{text eq} |
|
358 |
manually like any other type class. |
|
359 |
*} |
|
360 |
||
361 |
||
28462 | 362 |
subsection {* Explicit partiality *} |
363 |
||
364 |
text {* |
|
365 |
Partiality usually enters the game by partial patterns, as |
|
366 |
in the following example, again for amortised queues: |
|
367 |
*} |
|
368 |
||
29798 | 369 |
definition %quote strict_dequeue :: "'a queue \<Rightarrow> 'a \<times> 'a queue" where |
370 |
"strict_dequeue q = (case dequeue q |
|
371 |
of (Some x, q') \<Rightarrow> (x, q'))" |
|
372 |
||
373 |
lemma %quote strict_dequeue_AQueue [code]: |
|
374 |
"strict_dequeue (AQueue xs (y # ys)) = (y, AQueue xs ys)" |
|
375 |
"strict_dequeue (AQueue xs []) = |
|
376 |
(case rev xs of y # ys \<Rightarrow> (y, AQueue [] ys))" |
|
377 |
by (simp_all add: strict_dequeue_def dequeue_AQueue split: list.splits) |
|
28462 | 378 |
|
379 |
text {* |
|
380 |
\noindent In the corresponding code, there is no equation |
|
29798 | 381 |
for the pattern @{term "AQueue [] []"}: |
28462 | 382 |
*} |
383 |
||
28564 | 384 |
text %quote {*@{code_stmts strict_dequeue (consts) strict_dequeue (Haskell)}*} |
28462 | 385 |
|
386 |
text {* |
|
387 |
\noindent In some cases it is desirable to have this |
|
388 |
pseudo-\qt{partiality} more explicitly, e.g.~as follows: |
|
389 |
*} |
|
390 |
||
28564 | 391 |
axiomatization %quote empty_queue :: 'a |
28462 | 392 |
|
29798 | 393 |
definition %quote strict_dequeue' :: "'a queue \<Rightarrow> 'a \<times> 'a queue" where |
394 |
"strict_dequeue' q = (case dequeue q of (Some x, q') \<Rightarrow> (x, q') | _ \<Rightarrow> empty_queue)" |
|
28213 | 395 |
|
29798 | 396 |
lemma %quote strict_dequeue'_AQueue [code]: |
397 |
"strict_dequeue' (AQueue xs []) = (if xs = [] then empty_queue |
|
398 |
else strict_dequeue' (AQueue [] (rev xs)))" |
|
399 |
"strict_dequeue' (AQueue xs (y # ys)) = |
|
400 |
(y, AQueue xs ys)" |
|
401 |
by (simp_all add: strict_dequeue'_def dequeue_AQueue split: list.splits) |
|
28462 | 402 |
|
403 |
text {* |
|
29798 | 404 |
Observe that on the right hand side of the definition of @{const |
405 |
"strict_dequeue'"} the constant @{const empty_queue} occurs |
|
406 |
which is unspecified. |
|
28462 | 407 |
|
29798 | 408 |
Normally, if constants without any code equations occur in a |
409 |
program, the code generator complains (since in most cases this is |
|
410 |
not what the user expects). But such constants can also be thought |
|
411 |
of as function definitions with no equations which always fail, |
|
412 |
since there is never a successful pattern match on the left hand |
|
413 |
side. In order to categorise a constant into that category |
|
414 |
explicitly, use @{command "code_abort"}: |
|
28462 | 415 |
*} |
416 |
||
28564 | 417 |
code_abort %quote empty_queue |
28462 | 418 |
|
419 |
text {* |
|
420 |
\noindent Then the code generator will just insert an error or |
|
421 |
exception at the appropriate position: |
|
422 |
*} |
|
423 |
||
28564 | 424 |
text %quote {*@{code_stmts strict_dequeue' (consts) empty_queue strict_dequeue' (Haskell)}*} |
28462 | 425 |
|
426 |
text {* |
|
427 |
\noindent This feature however is rarely needed in practice. |
|
428 |
Note also that the @{text HOL} default setup already declares |
|
429 |
@{const undefined} as @{command "code_abort"}, which is most |
|
430 |
likely to be used in such situations. |
|
431 |
*} |
|
28213 | 432 |
|
33926
dd017d9db05f
adding subsection about the predicate compiler to the code generator tutorial
bulwahn
parents:
33707
diff
changeset
|
433 |
subsection {* Inductive Predicates *} |
dd017d9db05f
adding subsection about the predicate compiler to the code generator tutorial
bulwahn
parents:
33707
diff
changeset
|
434 |
(*<*) |
dd017d9db05f
adding subsection about the predicate compiler to the code generator tutorial
bulwahn
parents:
33707
diff
changeset
|
435 |
hide const append |
dd017d9db05f
adding subsection about the predicate compiler to the code generator tutorial
bulwahn
parents:
33707
diff
changeset
|
436 |
|
dd017d9db05f
adding subsection about the predicate compiler to the code generator tutorial
bulwahn
parents:
33707
diff
changeset
|
437 |
inductive append |
dd017d9db05f
adding subsection about the predicate compiler to the code generator tutorial
bulwahn
parents:
33707
diff
changeset
|
438 |
where |
dd017d9db05f
adding subsection about the predicate compiler to the code generator tutorial
bulwahn
parents:
33707
diff
changeset
|
439 |
"append [] ys ys" |
dd017d9db05f
adding subsection about the predicate compiler to the code generator tutorial
bulwahn
parents:
33707
diff
changeset
|
440 |
| "append xs ys zs ==> append (x # xs) ys (x # zs)" |
dd017d9db05f
adding subsection about the predicate compiler to the code generator tutorial
bulwahn
parents:
33707
diff
changeset
|
441 |
(*>*) |
dd017d9db05f
adding subsection about the predicate compiler to the code generator tutorial
bulwahn
parents:
33707
diff
changeset
|
442 |
text {* |
dd017d9db05f
adding subsection about the predicate compiler to the code generator tutorial
bulwahn
parents:
33707
diff
changeset
|
443 |
To execute inductive predicates, a special preprocessor, the predicate |
dd017d9db05f
adding subsection about the predicate compiler to the code generator tutorial
bulwahn
parents:
33707
diff
changeset
|
444 |
compiler, generates code equations from the introduction rules of the predicates. |
dd017d9db05f
adding subsection about the predicate compiler to the code generator tutorial
bulwahn
parents:
33707
diff
changeset
|
445 |
The mechanisms of this compiler are described in \cite{Berghofer-Bulwahn-Haftmann:2009:TPHOL}. |
dd017d9db05f
adding subsection about the predicate compiler to the code generator tutorial
bulwahn
parents:
33707
diff
changeset
|
446 |
Consider the simple predicate @{const append} given by these two |
dd017d9db05f
adding subsection about the predicate compiler to the code generator tutorial
bulwahn
parents:
33707
diff
changeset
|
447 |
introduction rules: |
dd017d9db05f
adding subsection about the predicate compiler to the code generator tutorial
bulwahn
parents:
33707
diff
changeset
|
448 |
*} |
dd017d9db05f
adding subsection about the predicate compiler to the code generator tutorial
bulwahn
parents:
33707
diff
changeset
|
449 |
text %quote {* |
dd017d9db05f
adding subsection about the predicate compiler to the code generator tutorial
bulwahn
parents:
33707
diff
changeset
|
450 |
@{thm append.intros(1)[of ys]}\\ |
dd017d9db05f
adding subsection about the predicate compiler to the code generator tutorial
bulwahn
parents:
33707
diff
changeset
|
451 |
\noindent@{thm append.intros(2)[of xs ys zs x]} |
dd017d9db05f
adding subsection about the predicate compiler to the code generator tutorial
bulwahn
parents:
33707
diff
changeset
|
452 |
*} |
dd017d9db05f
adding subsection about the predicate compiler to the code generator tutorial
bulwahn
parents:
33707
diff
changeset
|
453 |
text {* |
dd017d9db05f
adding subsection about the predicate compiler to the code generator tutorial
bulwahn
parents:
33707
diff
changeset
|
454 |
\noindent To invoke the compiler, simply use @{command_def "code_pred"}: |
dd017d9db05f
adding subsection about the predicate compiler to the code generator tutorial
bulwahn
parents:
33707
diff
changeset
|
455 |
*} |
dd017d9db05f
adding subsection about the predicate compiler to the code generator tutorial
bulwahn
parents:
33707
diff
changeset
|
456 |
code_pred %quote append . |
dd017d9db05f
adding subsection about the predicate compiler to the code generator tutorial
bulwahn
parents:
33707
diff
changeset
|
457 |
text {* |
dd017d9db05f
adding subsection about the predicate compiler to the code generator tutorial
bulwahn
parents:
33707
diff
changeset
|
458 |
\noindent The @{command "code_pred"} command takes the name |
dd017d9db05f
adding subsection about the predicate compiler to the code generator tutorial
bulwahn
parents:
33707
diff
changeset
|
459 |
of the inductive predicate and then you put a period to discharge |
dd017d9db05f
adding subsection about the predicate compiler to the code generator tutorial
bulwahn
parents:
33707
diff
changeset
|
460 |
a trivial correctness proof. |
dd017d9db05f
adding subsection about the predicate compiler to the code generator tutorial
bulwahn
parents:
33707
diff
changeset
|
461 |
The compiler infers possible modes |
dd017d9db05f
adding subsection about the predicate compiler to the code generator tutorial
bulwahn
parents:
33707
diff
changeset
|
462 |
for the predicate and produces the derived code equations. |
dd017d9db05f
adding subsection about the predicate compiler to the code generator tutorial
bulwahn
parents:
33707
diff
changeset
|
463 |
Modes annotate which (parts of the) arguments are to be taken as input, |
dd017d9db05f
adding subsection about the predicate compiler to the code generator tutorial
bulwahn
parents:
33707
diff
changeset
|
464 |
and which output. Modes are similar to types, but use the notation @{text "i"} |
dd017d9db05f
adding subsection about the predicate compiler to the code generator tutorial
bulwahn
parents:
33707
diff
changeset
|
465 |
for input and @{text "o"} for output. |
dd017d9db05f
adding subsection about the predicate compiler to the code generator tutorial
bulwahn
parents:
33707
diff
changeset
|
466 |
|
dd017d9db05f
adding subsection about the predicate compiler to the code generator tutorial
bulwahn
parents:
33707
diff
changeset
|
467 |
For @{term "append"}, the compiler can infer the following modes: |
dd017d9db05f
adding subsection about the predicate compiler to the code generator tutorial
bulwahn
parents:
33707
diff
changeset
|
468 |
\begin{itemize} |
dd017d9db05f
adding subsection about the predicate compiler to the code generator tutorial
bulwahn
parents:
33707
diff
changeset
|
469 |
\item @{text "i \<Rightarrow> i \<Rightarrow> i \<Rightarrow> bool"} |
dd017d9db05f
adding subsection about the predicate compiler to the code generator tutorial
bulwahn
parents:
33707
diff
changeset
|
470 |
\item @{text "i \<Rightarrow> i \<Rightarrow> o \<Rightarrow> bool"} |
dd017d9db05f
adding subsection about the predicate compiler to the code generator tutorial
bulwahn
parents:
33707
diff
changeset
|
471 |
\item @{text "o \<Rightarrow> o \<Rightarrow> i \<Rightarrow> bool"} |
dd017d9db05f
adding subsection about the predicate compiler to the code generator tutorial
bulwahn
parents:
33707
diff
changeset
|
472 |
\end{itemize} |
dd017d9db05f
adding subsection about the predicate compiler to the code generator tutorial
bulwahn
parents:
33707
diff
changeset
|
473 |
You can compute sets of predicates using @{command_def "values"}: |
dd017d9db05f
adding subsection about the predicate compiler to the code generator tutorial
bulwahn
parents:
33707
diff
changeset
|
474 |
*} |
dd017d9db05f
adding subsection about the predicate compiler to the code generator tutorial
bulwahn
parents:
33707
diff
changeset
|
475 |
values %quote "{zs. append [(1::nat),2,3] [4,5] zs}" |
dd017d9db05f
adding subsection about the predicate compiler to the code generator tutorial
bulwahn
parents:
33707
diff
changeset
|
476 |
text {* \noindent outputs @{text "{[1, 2, 3, 4, 5]}"}, and *} |
dd017d9db05f
adding subsection about the predicate compiler to the code generator tutorial
bulwahn
parents:
33707
diff
changeset
|
477 |
values %quote "{(xs, ys). append xs ys [(2::nat),3]}" |
dd017d9db05f
adding subsection about the predicate compiler to the code generator tutorial
bulwahn
parents:
33707
diff
changeset
|
478 |
text {* \noindent outputs @{text "{([], [2, 3]), ([2], [3]), ([2, 3], [])}"}. *} |
dd017d9db05f
adding subsection about the predicate compiler to the code generator tutorial
bulwahn
parents:
33707
diff
changeset
|
479 |
text {* |
dd017d9db05f
adding subsection about the predicate compiler to the code generator tutorial
bulwahn
parents:
33707
diff
changeset
|
480 |
\noindent If you are only interested in the first elements of the set |
dd017d9db05f
adding subsection about the predicate compiler to the code generator tutorial
bulwahn
parents:
33707
diff
changeset
|
481 |
comprehension (with respect to a depth-first search on the introduction rules), you can |
dd017d9db05f
adding subsection about the predicate compiler to the code generator tutorial
bulwahn
parents:
33707
diff
changeset
|
482 |
pass an argument to |
dd017d9db05f
adding subsection about the predicate compiler to the code generator tutorial
bulwahn
parents:
33707
diff
changeset
|
483 |
@{command "values"} to specify the number of elements you want: |
dd017d9db05f
adding subsection about the predicate compiler to the code generator tutorial
bulwahn
parents:
33707
diff
changeset
|
484 |
*} |
dd017d9db05f
adding subsection about the predicate compiler to the code generator tutorial
bulwahn
parents:
33707
diff
changeset
|
485 |
|
dd017d9db05f
adding subsection about the predicate compiler to the code generator tutorial
bulwahn
parents:
33707
diff
changeset
|
486 |
values %quote 1 "{(xs, ys). append xs ys [(1::nat),2,3,4]}" |
dd017d9db05f
adding subsection about the predicate compiler to the code generator tutorial
bulwahn
parents:
33707
diff
changeset
|
487 |
values %quote 3 "{(xs, ys). append xs ys [(1::nat),2,3,4]}" |
dd017d9db05f
adding subsection about the predicate compiler to the code generator tutorial
bulwahn
parents:
33707
diff
changeset
|
488 |
|
dd017d9db05f
adding subsection about the predicate compiler to the code generator tutorial
bulwahn
parents:
33707
diff
changeset
|
489 |
text {* |
dd017d9db05f
adding subsection about the predicate compiler to the code generator tutorial
bulwahn
parents:
33707
diff
changeset
|
490 |
\noindent The @{command "values"} command can only compute set |
dd017d9db05f
adding subsection about the predicate compiler to the code generator tutorial
bulwahn
parents:
33707
diff
changeset
|
491 |
comprehensions for which a mode has been inferred. |
dd017d9db05f
adding subsection about the predicate compiler to the code generator tutorial
bulwahn
parents:
33707
diff
changeset
|
492 |
|
dd017d9db05f
adding subsection about the predicate compiler to the code generator tutorial
bulwahn
parents:
33707
diff
changeset
|
493 |
The code equations for a predicate are made available as theorems with |
dd017d9db05f
adding subsection about the predicate compiler to the code generator tutorial
bulwahn
parents:
33707
diff
changeset
|
494 |
the suffix @{text "equation"}, and can be inspected with: |
dd017d9db05f
adding subsection about the predicate compiler to the code generator tutorial
bulwahn
parents:
33707
diff
changeset
|
495 |
*} |
dd017d9db05f
adding subsection about the predicate compiler to the code generator tutorial
bulwahn
parents:
33707
diff
changeset
|
496 |
thm %quote append.equation |
dd017d9db05f
adding subsection about the predicate compiler to the code generator tutorial
bulwahn
parents:
33707
diff
changeset
|
497 |
text {* |
dd017d9db05f
adding subsection about the predicate compiler to the code generator tutorial
bulwahn
parents:
33707
diff
changeset
|
498 |
\noindent More advanced options are described in the following subsections. |
dd017d9db05f
adding subsection about the predicate compiler to the code generator tutorial
bulwahn
parents:
33707
diff
changeset
|
499 |
*} |
dd017d9db05f
adding subsection about the predicate compiler to the code generator tutorial
bulwahn
parents:
33707
diff
changeset
|
500 |
subsubsection {* Alternative names for functions *} |
dd017d9db05f
adding subsection about the predicate compiler to the code generator tutorial
bulwahn
parents:
33707
diff
changeset
|
501 |
text {* |
dd017d9db05f
adding subsection about the predicate compiler to the code generator tutorial
bulwahn
parents:
33707
diff
changeset
|
502 |
By default, the functions generated from a predicate are named after the predicate with the |
dd017d9db05f
adding subsection about the predicate compiler to the code generator tutorial
bulwahn
parents:
33707
diff
changeset
|
503 |
mode mangled into the name (e.g., @{text "append_i_i_o"}). |
dd017d9db05f
adding subsection about the predicate compiler to the code generator tutorial
bulwahn
parents:
33707
diff
changeset
|
504 |
You can specify your own names as follows: |
dd017d9db05f
adding subsection about the predicate compiler to the code generator tutorial
bulwahn
parents:
33707
diff
changeset
|
505 |
*} |
dd017d9db05f
adding subsection about the predicate compiler to the code generator tutorial
bulwahn
parents:
33707
diff
changeset
|
506 |
code_pred %quote (modes: i => i => o => bool as concat, |
dd017d9db05f
adding subsection about the predicate compiler to the code generator tutorial
bulwahn
parents:
33707
diff
changeset
|
507 |
o => o => i => bool as split, |
dd017d9db05f
adding subsection about the predicate compiler to the code generator tutorial
bulwahn
parents:
33707
diff
changeset
|
508 |
i => o => i => bool as suffix) append . |
dd017d9db05f
adding subsection about the predicate compiler to the code generator tutorial
bulwahn
parents:
33707
diff
changeset
|
509 |
|
dd017d9db05f
adding subsection about the predicate compiler to the code generator tutorial
bulwahn
parents:
33707
diff
changeset
|
510 |
subsubsection {* Alternative introduction rules *} |
dd017d9db05f
adding subsection about the predicate compiler to the code generator tutorial
bulwahn
parents:
33707
diff
changeset
|
511 |
text {* |
dd017d9db05f
adding subsection about the predicate compiler to the code generator tutorial
bulwahn
parents:
33707
diff
changeset
|
512 |
Sometimes the introduction rules of an predicate are not executable because they contain |
dd017d9db05f
adding subsection about the predicate compiler to the code generator tutorial
bulwahn
parents:
33707
diff
changeset
|
513 |
non-executable constants or specific modes could not be inferred. |
dd017d9db05f
adding subsection about the predicate compiler to the code generator tutorial
bulwahn
parents:
33707
diff
changeset
|
514 |
It is also possible that the introduction rules yield a function that loops forever |
dd017d9db05f
adding subsection about the predicate compiler to the code generator tutorial
bulwahn
parents:
33707
diff
changeset
|
515 |
due to the execution in a depth-first search manner. |
dd017d9db05f
adding subsection about the predicate compiler to the code generator tutorial
bulwahn
parents:
33707
diff
changeset
|
516 |
Therefore, you can declare alternative introduction rules for predicates with the attribute |
dd017d9db05f
adding subsection about the predicate compiler to the code generator tutorial
bulwahn
parents:
33707
diff
changeset
|
517 |
@{attribute "code_pred_intro"}. |
dd017d9db05f
adding subsection about the predicate compiler to the code generator tutorial
bulwahn
parents:
33707
diff
changeset
|
518 |
For example, the transitive closure is defined by: |
dd017d9db05f
adding subsection about the predicate compiler to the code generator tutorial
bulwahn
parents:
33707
diff
changeset
|
519 |
*} |
dd017d9db05f
adding subsection about the predicate compiler to the code generator tutorial
bulwahn
parents:
33707
diff
changeset
|
520 |
text %quote {* |
dd017d9db05f
adding subsection about the predicate compiler to the code generator tutorial
bulwahn
parents:
33707
diff
changeset
|
521 |
@{thm tranclp.intros(1)[of r a b]}\\ |
dd017d9db05f
adding subsection about the predicate compiler to the code generator tutorial
bulwahn
parents:
33707
diff
changeset
|
522 |
\noindent @{thm tranclp.intros(2)[of r a b c]} |
dd017d9db05f
adding subsection about the predicate compiler to the code generator tutorial
bulwahn
parents:
33707
diff
changeset
|
523 |
*} |
dd017d9db05f
adding subsection about the predicate compiler to the code generator tutorial
bulwahn
parents:
33707
diff
changeset
|
524 |
text {* |
dd017d9db05f
adding subsection about the predicate compiler to the code generator tutorial
bulwahn
parents:
33707
diff
changeset
|
525 |
\noindent These rules do not suit well for executing the transitive closure |
dd017d9db05f
adding subsection about the predicate compiler to the code generator tutorial
bulwahn
parents:
33707
diff
changeset
|
526 |
with the mode @{text "(i \<Rightarrow> o \<Rightarrow> bool) \<Rightarrow> i \<Rightarrow> o \<Rightarrow> bool"}, as the second rule will |
dd017d9db05f
adding subsection about the predicate compiler to the code generator tutorial
bulwahn
parents:
33707
diff
changeset
|
527 |
cause an infinite loop in the recursive call. |
dd017d9db05f
adding subsection about the predicate compiler to the code generator tutorial
bulwahn
parents:
33707
diff
changeset
|
528 |
This can be avoided using the following alternative rules which are |
dd017d9db05f
adding subsection about the predicate compiler to the code generator tutorial
bulwahn
parents:
33707
diff
changeset
|
529 |
declared to the predicate compiler by the attribute @{attribute "code_pred_intro"}: |
dd017d9db05f
adding subsection about the predicate compiler to the code generator tutorial
bulwahn
parents:
33707
diff
changeset
|
530 |
*} |
dd017d9db05f
adding subsection about the predicate compiler to the code generator tutorial
bulwahn
parents:
33707
diff
changeset
|
531 |
lemma %quote [code_pred_intro]: |
dd017d9db05f
adding subsection about the predicate compiler to the code generator tutorial
bulwahn
parents:
33707
diff
changeset
|
532 |
"r a b \<Longrightarrow> r\<^sup>+\<^sup>+ a b" |
dd017d9db05f
adding subsection about the predicate compiler to the code generator tutorial
bulwahn
parents:
33707
diff
changeset
|
533 |
"r a b \<Longrightarrow> r\<^sup>+\<^sup>+ b c \<Longrightarrow> r\<^sup>+\<^sup>+ a c" |
dd017d9db05f
adding subsection about the predicate compiler to the code generator tutorial
bulwahn
parents:
33707
diff
changeset
|
534 |
by auto |
dd017d9db05f
adding subsection about the predicate compiler to the code generator tutorial
bulwahn
parents:
33707
diff
changeset
|
535 |
text {* |
dd017d9db05f
adding subsection about the predicate compiler to the code generator tutorial
bulwahn
parents:
33707
diff
changeset
|
536 |
\noindent After declaring all alternative rules for the transitive closure, |
dd017d9db05f
adding subsection about the predicate compiler to the code generator tutorial
bulwahn
parents:
33707
diff
changeset
|
537 |
you invoke @{command "code_pred"} as usual. |
dd017d9db05f
adding subsection about the predicate compiler to the code generator tutorial
bulwahn
parents:
33707
diff
changeset
|
538 |
As you have declared alternative rules for the predicate, you are urged to prove that these |
dd017d9db05f
adding subsection about the predicate compiler to the code generator tutorial
bulwahn
parents:
33707
diff
changeset
|
539 |
introduction rules are complete, i.e., that you can derive an elimination rule for the |
dd017d9db05f
adding subsection about the predicate compiler to the code generator tutorial
bulwahn
parents:
33707
diff
changeset
|
540 |
alternative rules: |
dd017d9db05f
adding subsection about the predicate compiler to the code generator tutorial
bulwahn
parents:
33707
diff
changeset
|
541 |
*} |
dd017d9db05f
adding subsection about the predicate compiler to the code generator tutorial
bulwahn
parents:
33707
diff
changeset
|
542 |
code_pred %quote tranclp |
dd017d9db05f
adding subsection about the predicate compiler to the code generator tutorial
bulwahn
parents:
33707
diff
changeset
|
543 |
proof - |
dd017d9db05f
adding subsection about the predicate compiler to the code generator tutorial
bulwahn
parents:
33707
diff
changeset
|
544 |
case tranclp |
dd017d9db05f
adding subsection about the predicate compiler to the code generator tutorial
bulwahn
parents:
33707
diff
changeset
|
545 |
from this converse_tranclpE[OF this(1)] show thesis by metis |
dd017d9db05f
adding subsection about the predicate compiler to the code generator tutorial
bulwahn
parents:
33707
diff
changeset
|
546 |
qed |
dd017d9db05f
adding subsection about the predicate compiler to the code generator tutorial
bulwahn
parents:
33707
diff
changeset
|
547 |
text {* |
dd017d9db05f
adding subsection about the predicate compiler to the code generator tutorial
bulwahn
parents:
33707
diff
changeset
|
548 |
\noindent Alternative rules can also be used for constants that have not |
dd017d9db05f
adding subsection about the predicate compiler to the code generator tutorial
bulwahn
parents:
33707
diff
changeset
|
549 |
been defined inductively. For example, the lexicographic order which |
dd017d9db05f
adding subsection about the predicate compiler to the code generator tutorial
bulwahn
parents:
33707
diff
changeset
|
550 |
is defined as: *} |
dd017d9db05f
adding subsection about the predicate compiler to the code generator tutorial
bulwahn
parents:
33707
diff
changeset
|
551 |
text %quote {* |
dd017d9db05f
adding subsection about the predicate compiler to the code generator tutorial
bulwahn
parents:
33707
diff
changeset
|
552 |
@{thm [display] lexord_def[of "r"]} |
dd017d9db05f
adding subsection about the predicate compiler to the code generator tutorial
bulwahn
parents:
33707
diff
changeset
|
553 |
*} |
dd017d9db05f
adding subsection about the predicate compiler to the code generator tutorial
bulwahn
parents:
33707
diff
changeset
|
554 |
text {* |
dd017d9db05f
adding subsection about the predicate compiler to the code generator tutorial
bulwahn
parents:
33707
diff
changeset
|
555 |
\noindent To make it executable, you can derive the following two rules and prove the |
dd017d9db05f
adding subsection about the predicate compiler to the code generator tutorial
bulwahn
parents:
33707
diff
changeset
|
556 |
elimination rule: |
dd017d9db05f
adding subsection about the predicate compiler to the code generator tutorial
bulwahn
parents:
33707
diff
changeset
|
557 |
*} |
dd017d9db05f
adding subsection about the predicate compiler to the code generator tutorial
bulwahn
parents:
33707
diff
changeset
|
558 |
(*<*) |
dd017d9db05f
adding subsection about the predicate compiler to the code generator tutorial
bulwahn
parents:
33707
diff
changeset
|
559 |
lemma append: "append xs ys zs = (xs @ ys = zs)" |
dd017d9db05f
adding subsection about the predicate compiler to the code generator tutorial
bulwahn
parents:
33707
diff
changeset
|
560 |
by (induct xs arbitrary: ys zs) (auto elim: append.cases intro: append.intros) |
dd017d9db05f
adding subsection about the predicate compiler to the code generator tutorial
bulwahn
parents:
33707
diff
changeset
|
561 |
(*>*) |
dd017d9db05f
adding subsection about the predicate compiler to the code generator tutorial
bulwahn
parents:
33707
diff
changeset
|
562 |
lemma %quote [code_pred_intro]: |
dd017d9db05f
adding subsection about the predicate compiler to the code generator tutorial
bulwahn
parents:
33707
diff
changeset
|
563 |
"append xs (a # v) ys \<Longrightarrow> lexord r (xs, ys)" |
dd017d9db05f
adding subsection about the predicate compiler to the code generator tutorial
bulwahn
parents:
33707
diff
changeset
|
564 |
(*<*)unfolding lexord_def Collect_def by (auto simp add: append)(*>*) |
dd017d9db05f
adding subsection about the predicate compiler to the code generator tutorial
bulwahn
parents:
33707
diff
changeset
|
565 |
|
dd017d9db05f
adding subsection about the predicate compiler to the code generator tutorial
bulwahn
parents:
33707
diff
changeset
|
566 |
lemma %quote [code_pred_intro]: |
dd017d9db05f
adding subsection about the predicate compiler to the code generator tutorial
bulwahn
parents:
33707
diff
changeset
|
567 |
"append u (a # v) xs \<Longrightarrow> append u (b # w) ys \<Longrightarrow> r (a, b) |
dd017d9db05f
adding subsection about the predicate compiler to the code generator tutorial
bulwahn
parents:
33707
diff
changeset
|
568 |
\<Longrightarrow> lexord r (xs, ys)" |
dd017d9db05f
adding subsection about the predicate compiler to the code generator tutorial
bulwahn
parents:
33707
diff
changeset
|
569 |
(*<*)unfolding lexord_def Collect_def append mem_def apply simp |
dd017d9db05f
adding subsection about the predicate compiler to the code generator tutorial
bulwahn
parents:
33707
diff
changeset
|
570 |
apply (rule disjI2) by auto |
dd017d9db05f
adding subsection about the predicate compiler to the code generator tutorial
bulwahn
parents:
33707
diff
changeset
|
571 |
(*>*) |
dd017d9db05f
adding subsection about the predicate compiler to the code generator tutorial
bulwahn
parents:
33707
diff
changeset
|
572 |
|
dd017d9db05f
adding subsection about the predicate compiler to the code generator tutorial
bulwahn
parents:
33707
diff
changeset
|
573 |
code_pred %quote lexord |
dd017d9db05f
adding subsection about the predicate compiler to the code generator tutorial
bulwahn
parents:
33707
diff
changeset
|
574 |
(*<*) |
dd017d9db05f
adding subsection about the predicate compiler to the code generator tutorial
bulwahn
parents:
33707
diff
changeset
|
575 |
proof - |
dd017d9db05f
adding subsection about the predicate compiler to the code generator tutorial
bulwahn
parents:
33707
diff
changeset
|
576 |
fix r a1 |
dd017d9db05f
adding subsection about the predicate compiler to the code generator tutorial
bulwahn
parents:
33707
diff
changeset
|
577 |
assume lexord: "lexord r a1" |
dd017d9db05f
adding subsection about the predicate compiler to the code generator tutorial
bulwahn
parents:
33707
diff
changeset
|
578 |
assume 1: "\<And> xs ys a v. a1 = (xs, ys) \<Longrightarrow> append xs (a # v) ys \<Longrightarrow> thesis" |
dd017d9db05f
adding subsection about the predicate compiler to the code generator tutorial
bulwahn
parents:
33707
diff
changeset
|
579 |
assume 2: "\<And> xs ys u a v b w. a1 = (xs, ys) \<Longrightarrow> append u (a # v) xs \<Longrightarrow> append u (b # w) ys \<Longrightarrow> r (a, b) \<Longrightarrow> thesis" |
dd017d9db05f
adding subsection about the predicate compiler to the code generator tutorial
bulwahn
parents:
33707
diff
changeset
|
580 |
obtain xs ys where a1: "a1 = (xs, ys)" by fastsimp |
dd017d9db05f
adding subsection about the predicate compiler to the code generator tutorial
bulwahn
parents:
33707
diff
changeset
|
581 |
{ |
dd017d9db05f
adding subsection about the predicate compiler to the code generator tutorial
bulwahn
parents:
33707
diff
changeset
|
582 |
assume "\<exists>a v. ys = xs @ a # v" |
dd017d9db05f
adding subsection about the predicate compiler to the code generator tutorial
bulwahn
parents:
33707
diff
changeset
|
583 |
from this 1 a1 have thesis |
dd017d9db05f
adding subsection about the predicate compiler to the code generator tutorial
bulwahn
parents:
33707
diff
changeset
|
584 |
by (fastsimp simp add: append) |
dd017d9db05f
adding subsection about the predicate compiler to the code generator tutorial
bulwahn
parents:
33707
diff
changeset
|
585 |
} moreover |
dd017d9db05f
adding subsection about the predicate compiler to the code generator tutorial
bulwahn
parents:
33707
diff
changeset
|
586 |
{ |
dd017d9db05f
adding subsection about the predicate compiler to the code generator tutorial
bulwahn
parents:
33707
diff
changeset
|
587 |
assume "\<exists>u a b v w. (a, b) \<in> r \<and> xs = u @ a # v \<and> ys = u @ b # w" |
dd017d9db05f
adding subsection about the predicate compiler to the code generator tutorial
bulwahn
parents:
33707
diff
changeset
|
588 |
from this 2 a1 have thesis by (fastsimp simp add: append mem_def) |
dd017d9db05f
adding subsection about the predicate compiler to the code generator tutorial
bulwahn
parents:
33707
diff
changeset
|
589 |
} moreover |
dd017d9db05f
adding subsection about the predicate compiler to the code generator tutorial
bulwahn
parents:
33707
diff
changeset
|
590 |
note lexord[simplified a1] |
dd017d9db05f
adding subsection about the predicate compiler to the code generator tutorial
bulwahn
parents:
33707
diff
changeset
|
591 |
ultimately show thesis |
dd017d9db05f
adding subsection about the predicate compiler to the code generator tutorial
bulwahn
parents:
33707
diff
changeset
|
592 |
unfolding lexord_def |
dd017d9db05f
adding subsection about the predicate compiler to the code generator tutorial
bulwahn
parents:
33707
diff
changeset
|
593 |
by (fastsimp simp add: Collect_def) |
dd017d9db05f
adding subsection about the predicate compiler to the code generator tutorial
bulwahn
parents:
33707
diff
changeset
|
594 |
qed |
dd017d9db05f
adding subsection about the predicate compiler to the code generator tutorial
bulwahn
parents:
33707
diff
changeset
|
595 |
(*>*) |
dd017d9db05f
adding subsection about the predicate compiler to the code generator tutorial
bulwahn
parents:
33707
diff
changeset
|
596 |
subsubsection {* Options for values *} |
dd017d9db05f
adding subsection about the predicate compiler to the code generator tutorial
bulwahn
parents:
33707
diff
changeset
|
597 |
text {* |
dd017d9db05f
adding subsection about the predicate compiler to the code generator tutorial
bulwahn
parents:
33707
diff
changeset
|
598 |
In the presence of higher-order predicates, multiple modes for some predicate could be inferred |
dd017d9db05f
adding subsection about the predicate compiler to the code generator tutorial
bulwahn
parents:
33707
diff
changeset
|
599 |
that are not disambiguated by the pattern of the set comprehension. |
dd017d9db05f
adding subsection about the predicate compiler to the code generator tutorial
bulwahn
parents:
33707
diff
changeset
|
600 |
To disambiguate the modes for the arguments of a predicate, you can state |
dd017d9db05f
adding subsection about the predicate compiler to the code generator tutorial
bulwahn
parents:
33707
diff
changeset
|
601 |
the modes explicitly in the @{command "values"} command. |
dd017d9db05f
adding subsection about the predicate compiler to the code generator tutorial
bulwahn
parents:
33707
diff
changeset
|
602 |
Consider the simple predicate @{term "succ"}: |
dd017d9db05f
adding subsection about the predicate compiler to the code generator tutorial
bulwahn
parents:
33707
diff
changeset
|
603 |
*} |
dd017d9db05f
adding subsection about the predicate compiler to the code generator tutorial
bulwahn
parents:
33707
diff
changeset
|
604 |
inductive succ :: "nat \<Rightarrow> nat \<Rightarrow> bool" |
dd017d9db05f
adding subsection about the predicate compiler to the code generator tutorial
bulwahn
parents:
33707
diff
changeset
|
605 |
where |
dd017d9db05f
adding subsection about the predicate compiler to the code generator tutorial
bulwahn
parents:
33707
diff
changeset
|
606 |
"succ 0 (Suc 0)" |
dd017d9db05f
adding subsection about the predicate compiler to the code generator tutorial
bulwahn
parents:
33707
diff
changeset
|
607 |
| "succ x y \<Longrightarrow> succ (Suc x) (Suc y)" |
dd017d9db05f
adding subsection about the predicate compiler to the code generator tutorial
bulwahn
parents:
33707
diff
changeset
|
608 |
|
dd017d9db05f
adding subsection about the predicate compiler to the code generator tutorial
bulwahn
parents:
33707
diff
changeset
|
609 |
code_pred succ . |
dd017d9db05f
adding subsection about the predicate compiler to the code generator tutorial
bulwahn
parents:
33707
diff
changeset
|
610 |
|
dd017d9db05f
adding subsection about the predicate compiler to the code generator tutorial
bulwahn
parents:
33707
diff
changeset
|
611 |
text {* |
dd017d9db05f
adding subsection about the predicate compiler to the code generator tutorial
bulwahn
parents:
33707
diff
changeset
|
612 |
\noindent For this, the predicate compiler can infer modes @{text "o \<Rightarrow> o \<Rightarrow> bool"}, @{text "i \<Rightarrow> o \<Rightarrow> bool"}, |
dd017d9db05f
adding subsection about the predicate compiler to the code generator tutorial
bulwahn
parents:
33707
diff
changeset
|
613 |
@{text "o \<Rightarrow> i \<Rightarrow> bool"} and @{text "i \<Rightarrow> i \<Rightarrow> bool"}. |
dd017d9db05f
adding subsection about the predicate compiler to the code generator tutorial
bulwahn
parents:
33707
diff
changeset
|
614 |
The invocation of @{command "values"} @{text "{n. tranclp succ 10 n}"} loops, as multiple |
dd017d9db05f
adding subsection about the predicate compiler to the code generator tutorial
bulwahn
parents:
33707
diff
changeset
|
615 |
modes for the predicate @{text "succ"} are possible and here the first mode @{text "o \<Rightarrow> o \<Rightarrow> bool"} |
dd017d9db05f
adding subsection about the predicate compiler to the code generator tutorial
bulwahn
parents:
33707
diff
changeset
|
616 |
is chosen. To choose another mode for the argument, you can declare the mode for the argument between |
dd017d9db05f
adding subsection about the predicate compiler to the code generator tutorial
bulwahn
parents:
33707
diff
changeset
|
617 |
the @{command "values"} and the number of elements. |
dd017d9db05f
adding subsection about the predicate compiler to the code generator tutorial
bulwahn
parents:
33707
diff
changeset
|
618 |
*} |
dd017d9db05f
adding subsection about the predicate compiler to the code generator tutorial
bulwahn
parents:
33707
diff
changeset
|
619 |
values %quote [mode: i => o => bool] 20 "{n. tranclp succ 10 n}" |
dd017d9db05f
adding subsection about the predicate compiler to the code generator tutorial
bulwahn
parents:
33707
diff
changeset
|
620 |
values %quote [mode: o => i => bool] 10 "{n. tranclp succ n 10}" |
dd017d9db05f
adding subsection about the predicate compiler to the code generator tutorial
bulwahn
parents:
33707
diff
changeset
|
621 |
|
dd017d9db05f
adding subsection about the predicate compiler to the code generator tutorial
bulwahn
parents:
33707
diff
changeset
|
622 |
subsubsection {* Embedding into functional code within Isabelle/HOL *} |
dd017d9db05f
adding subsection about the predicate compiler to the code generator tutorial
bulwahn
parents:
33707
diff
changeset
|
623 |
text {* |
dd017d9db05f
adding subsection about the predicate compiler to the code generator tutorial
bulwahn
parents:
33707
diff
changeset
|
624 |
To embed the computation of an inductive predicate into functions that are defined in Isabelle/HOL, |
dd017d9db05f
adding subsection about the predicate compiler to the code generator tutorial
bulwahn
parents:
33707
diff
changeset
|
625 |
you have a number of options: |
dd017d9db05f
adding subsection about the predicate compiler to the code generator tutorial
bulwahn
parents:
33707
diff
changeset
|
626 |
\begin{itemize} |
dd017d9db05f
adding subsection about the predicate compiler to the code generator tutorial
bulwahn
parents:
33707
diff
changeset
|
627 |
\item You want to use the first-order predicate with the mode |
dd017d9db05f
adding subsection about the predicate compiler to the code generator tutorial
bulwahn
parents:
33707
diff
changeset
|
628 |
where all arguments are input. Then you can use the predicate directly, e.g. |
dd017d9db05f
adding subsection about the predicate compiler to the code generator tutorial
bulwahn
parents:
33707
diff
changeset
|
629 |
\begin{quote} |
dd017d9db05f
adding subsection about the predicate compiler to the code generator tutorial
bulwahn
parents:
33707
diff
changeset
|
630 |
@{text "valid_suffix ys zs = "}\\ |
dd017d9db05f
adding subsection about the predicate compiler to the code generator tutorial
bulwahn
parents:
33707
diff
changeset
|
631 |
@{text "(if append [Suc 0, 2] ys zs then Some ys else None)"} |
dd017d9db05f
adding subsection about the predicate compiler to the code generator tutorial
bulwahn
parents:
33707
diff
changeset
|
632 |
\end{quote} |
dd017d9db05f
adding subsection about the predicate compiler to the code generator tutorial
bulwahn
parents:
33707
diff
changeset
|
633 |
\item If you know that the execution returns only one value (it is deterministic), then you can |
dd017d9db05f
adding subsection about the predicate compiler to the code generator tutorial
bulwahn
parents:
33707
diff
changeset
|
634 |
use the combinator @{term "Predicate.the"}, e.g., a functional concatenation of lists |
dd017d9db05f
adding subsection about the predicate compiler to the code generator tutorial
bulwahn
parents:
33707
diff
changeset
|
635 |
is defined with |
dd017d9db05f
adding subsection about the predicate compiler to the code generator tutorial
bulwahn
parents:
33707
diff
changeset
|
636 |
\begin{quote} |
dd017d9db05f
adding subsection about the predicate compiler to the code generator tutorial
bulwahn
parents:
33707
diff
changeset
|
637 |
@{term "functional_concat xs ys = Predicate.the (append_i_i_o xs ys)"} |
dd017d9db05f
adding subsection about the predicate compiler to the code generator tutorial
bulwahn
parents:
33707
diff
changeset
|
638 |
\end{quote} |
dd017d9db05f
adding subsection about the predicate compiler to the code generator tutorial
bulwahn
parents:
33707
diff
changeset
|
639 |
Note that if the evaluation does not return a unique value, it raises a run-time error |
dd017d9db05f
adding subsection about the predicate compiler to the code generator tutorial
bulwahn
parents:
33707
diff
changeset
|
640 |
@{term "not_unique"}. |
dd017d9db05f
adding subsection about the predicate compiler to the code generator tutorial
bulwahn
parents:
33707
diff
changeset
|
641 |
\end{itemize} |
dd017d9db05f
adding subsection about the predicate compiler to the code generator tutorial
bulwahn
parents:
33707
diff
changeset
|
642 |
*} |
dd017d9db05f
adding subsection about the predicate compiler to the code generator tutorial
bulwahn
parents:
33707
diff
changeset
|
643 |
subsubsection {* Further Examples *} |
dd017d9db05f
adding subsection about the predicate compiler to the code generator tutorial
bulwahn
parents:
33707
diff
changeset
|
644 |
text {* Further examples for compiling inductive predicates can be found in |
dd017d9db05f
adding subsection about the predicate compiler to the code generator tutorial
bulwahn
parents:
33707
diff
changeset
|
645 |
the @{text "HOL/ex/Predicate_Compile_ex"} theory file. |
dd017d9db05f
adding subsection about the predicate compiler to the code generator tutorial
bulwahn
parents:
33707
diff
changeset
|
646 |
There are also some examples in the Archive of Formal Proofs, notably |
dd017d9db05f
adding subsection about the predicate compiler to the code generator tutorial
bulwahn
parents:
33707
diff
changeset
|
647 |
in the @{text "POPLmark-deBruijn"} and the @{text "FeatherweightJava"} sessions. |
dd017d9db05f
adding subsection about the predicate compiler to the code generator tutorial
bulwahn
parents:
33707
diff
changeset
|
648 |
*} |
28213 | 649 |
end |