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