author | wenzelm |
Sat, 10 Sep 2022 16:12:52 +0200 | |
changeset 76107 | 4dedb6e2dac2 |
parent 74584 | c14787d73db6 |
child 76659 | 2afbd514b654 |
permissions | -rw-r--r-- |
65041 | 1 |
theory Computations |
69422
472af2d7835d
clarified session dependencies: faster build_doc/build_release;
wenzelm
parents:
68028
diff
changeset
|
2 |
imports Setup |
66453
cc19f7ca2ed6
session-qualified theory imports: isabelle imports -U -i -d '~~/src/Benchmarks' -a;
wenzelm
parents:
65044
diff
changeset
|
3 |
"HOL-Library.Code_Target_Int" |
65041 | 4 |
begin |
5 |
||
6 |
section \<open>Computations \label{sec:computations}\<close> |
|
7 |
||
69505 | 8 |
subsection \<open>Prelude -- The \<open>code\<close> antiquotation \label{sec:code_antiq}\<close> |
65041 | 9 |
|
10 |
text \<open> |
|
11 |
The @{ML_antiquotation_def code} antiquotation allows to include constants |
|
12 |
from |
|
13 |
generated code directly into ML system code, as in the following toy |
|
14 |
example: |
|
15 |
\<close> |
|
16 |
||
17 |
datatype %quote form = T | F | And form form | Or form form (*<*) |
|
18 |
||
69660
2bc2a8599369
canonical operation to typeset generated code makes dedicated environment obsolete
haftmann
parents:
69597
diff
changeset
|
19 |
(*>*) ML %quote \<open> |
65041 | 20 |
fun eval_form @{code T} = true |
21 |
| eval_form @{code F} = false |
|
22 |
| eval_form (@{code And} (p, q)) = |
|
23 |
eval_form p andalso eval_form q |
|
24 |
| eval_form (@{code Or} (p, q)) = |
|
25 |
eval_form p orelse eval_form q; |
|
26 |
\<close> |
|
27 |
||
28 |
text \<open> |
|
29 |
\noindent The antiquotation @{ML_antiquotation code} takes |
|
30 |
the name of a constant as argument; |
|
31 |
the required code is generated |
|
32 |
transparently and the corresponding constant names are inserted |
|
33 |
for the given antiquotations. This technique allows to use pattern |
|
34 |
matching on constructors stemming from compiled datatypes. |
|
35 |
Note that the @{ML_antiquotation code} |
|
36 |
antiquotation may not refer to constants which carry adaptations; |
|
37 |
here you have to refer to the corresponding adapted code directly. |
|
38 |
\<close> |
|
39 |
||
40 |
||
41 |
subsection \<open>The concept of computations\<close> |
|
42 |
||
43 |
text \<open> |
|
44 |
Computations embody the simple idea that for each |
|
69505 | 45 |
monomorphic Isabelle/HOL term of type \<open>\<tau>\<close> by virtue of |
46 |
code generation there exists an corresponding ML type \<open>T\<close> and |
|
47 |
a morphism \<open>\<Phi> :: \<tau> \<rightarrow> T\<close> satisfying |
|
48 |
\<open>\<Phi> (t\<^sub>1 \<cdot> t\<^sub>2) = \<Phi> t\<^sub>1 \<cdot> \<Phi> t\<^sub>2\<close>, with \<open>\<cdot>\<close> denoting |
|
65041 | 49 |
term application. |
50 |
||
69505 | 51 |
For a given Isabelle/HOL type \<open>\<tau>\<close>, parts of \<open>\<Phi>\<close> can be |
52 |
implemented by a corresponding ML function \<open>\<phi>\<^sub>\<tau> :: term \<rightarrow> T\<close>. |
|
65041 | 53 |
How? |
54 |
||
55 |
\<^descr> \<open>Let input be a constant C :: \<tau>.\<close> \\ |
|
69505 | 56 |
Then \<open>\<phi>\<^sub>\<tau> C = f\<^sub>C\<close> with \<open>f\<^sub>C\<close> being |
57 |
the image of \<open>C\<close> under code generation. |
|
65041 | 58 |
|
59 |
\<^descr> \<open>Let input be an application (t\<^sub>1 \<cdot> t\<^sub>2) :: \<tau>.\<close> \\ |
|
69505 | 60 |
Then \<open>\<phi>\<^sub>\<tau> (t\<^sub>1 \<cdot> t\<^sub>2) = \<phi>\<^sub>\<tau> t\<^sub>1 (\<phi>\<^sub>\<tau> t\<^sub>2)\<close>. |
65041 | 61 |
|
62 |
\noindent Using these trivial properties, each monomorphic constant |
|
69505 | 63 |
\<open>C : \<^vec>\<tau>\<^sub>n \<rightarrow> \<tau>\<close> yields the following |
65041 | 64 |
equations: |
65 |
\<close> |
|
66 |
||
67 |
text %quote \<open> |
|
69505 | 68 |
\<open>\<phi>\<^bsub>(\<tau>\<^sub>1 \<rightarrow> \<tau>\<^sub>2 \<rightarrow> \<dots> \<rightarrow> \<tau>\<^sub>n \<rightarrow> \<tau>)\<^esub> C = f\<^sub>C\<close> \\ |
69 |
\<open>\<phi>\<^bsub>(\<tau>\<^sub>2 \<rightarrow> \<dots> \<rightarrow> \<tau>\<^sub>n \<rightarrow> \<tau>)\<^esub> (C \<cdot> t\<^sub>1) = f\<^sub>C (\<phi>\<^bsub>\<tau>\<^sub>1\<^esub> t\<^sub>1)\<close> \\ |
|
70 |
\<open>\<dots>\<close> \\ |
|
71 |
\<open>\<phi>\<^bsub>\<tau>\<^esub> (C \<cdot> t\<^sub>1 \<cdot> \<dots> \<cdot> t\<^sub>n) = f\<^sub>C (\<phi>\<^bsub>\<tau>\<^sub>1\<^esub> t\<^sub>1) \<dots> (\<phi>\<^bsub>\<tau>\<^sub>n\<^esub> t\<^sub>n)\<close> |
|
65041 | 72 |
\<close> |
73 |
||
74 |
text \<open> |
|
75 |
\noindent Hence a computation is characterized as follows: |
|
76 |
||
69505 | 77 |
\<^item> Let \<open>input constants\<close> denote a set of monomorphic constants. |
65041 | 78 |
|
69505 | 79 |
\<^item> Let \<open>\<tau>\<close> denote a monomorphic type and \<open>'ml\<close> be a schematic |
65041 | 80 |
placeholder for its corresponding type in ML under code generation. |
81 |
||
82 |
\<^item> Then the corresponding computation is an ML function of type |
|
69597 | 83 |
\<^ML_type>\<open>Proof.context -> term -> 'ml\<close> |
69505 | 84 |
partially implementing the morphism \<open>\<Phi> :: \<tau> \<rightarrow> T\<close> for all |
65041 | 85 |
\<^emph>\<open>input terms\<close> consisting only of input constants and applications. |
86 |
||
87 |
\noindent The charming idea is that all required code is automatically generated |
|
88 |
by the code generator for givens input constants and types; |
|
89 |
that code is directly inserted into the Isabelle/ML runtime system |
|
90 |
by means of antiquotations. |
|
91 |
\<close> |
|
92 |
||
93 |
||
69505 | 94 |
subsection \<open>The \<open>computation\<close> antiquotation\<close> |
65041 | 95 |
|
96 |
text \<open> |
|
97 |
The following example illustrates its basic usage: |
|
98 |
\<close> |
|
99 |
||
69660
2bc2a8599369
canonical operation to typeset generated code makes dedicated environment obsolete
haftmann
parents:
69597
diff
changeset
|
100 |
ML %quote \<open> |
65041 | 101 |
local |
102 |
||
103 |
fun int_of_nat @{code "0 :: nat"} = 0 |
|
104 |
| int_of_nat (@{code Suc} n) = int_of_nat n + 1; |
|
105 |
||
106 |
in |
|
107 |
||
108 |
val comp_nat = @{computation nat terms: |
|
109 |
"plus :: nat \<Rightarrow> nat \<Rightarrow> nat" "times :: nat \<Rightarrow> nat \<Rightarrow> nat" |
|
110 |
"sum_list :: nat list \<Rightarrow> nat" "prod_list :: nat list \<Rightarrow> nat" |
|
111 |
datatypes: nat "nat list"} |
|
112 |
(fn post => post o HOLogic.mk_nat o int_of_nat o the); |
|
113 |
||
114 |
end |
|
115 |
\<close> |
|
116 |
||
117 |
text \<open> |
|
118 |
\<^item> Antiquotations occurring in the |
|
119 |
same ML block always refer to the same transparently generated code; |
|
120 |
particularly, they share the same transparently generated datatype |
|
121 |
declarations. |
|
122 |
||
123 |
\<^item> The type of a computation is specified as first argument. |
|
124 |
||
125 |
\<^item> Input constants are specified the following ways: |
|
126 |
||
69505 | 127 |
\<^item> Each term following \<open>terms:\<close> specifies all constants |
65041 | 128 |
it contains as input constants. |
129 |
||
69505 | 130 |
\<^item> Each type following \<open>datatypes:\<close> specifies all constructors |
65041 | 131 |
of the corresponding code datatype as input constants. Note that |
132 |
this does not increase expressiveness but succinctness for datatypes |
|
67327
89be5a4f514b
skip abstract constructors silently in datatype clauses of computations
haftmann
parents:
67299
diff
changeset
|
133 |
with many constructors. Abstract type constructors are skipped |
89be5a4f514b
skip abstract constructors silently in datatype clauses of computations
haftmann
parents:
67299
diff
changeset
|
134 |
silently. |
65041 | 135 |
|
69505 | 136 |
\<^item> The code generated by a \<open>computation\<close> antiquotation takes a functional argument |
65041 | 137 |
which describes how to conclude the computation. What's the rationale |
138 |
behind this? |
|
139 |
||
140 |
\<^item> There is no automated way to generate a reconstruction function |
|
141 |
from the resulting ML type to a Isabelle term -- this is in the |
|
142 |
responsibility of the implementor. One possible approach |
|
69505 | 143 |
for robust term reconstruction is the \<open>code\<close> antiquotation. |
65041 | 144 |
|
145 |
\<^item> Both statically specified input constants and dynamically provided input |
|
146 |
terms are subject to preprocessing. Likewise the result |
|
147 |
is supposed to be subject to postprocessing; the implementor |
|
65044 | 148 |
is expected to take care for this explicitly. |
65041 | 149 |
|
150 |
\<^item> Computations follow the partiality principle (cf.~\secref{sec:partiality_principle}): |
|
151 |
failures due to pattern matching or unspecified functions |
|
152 |
are interpreted as partiality; therefore resulting ML values |
|
153 |
are optional. |
|
154 |
||
155 |
Hence the functional argument accepts the following parameters |
|
156 |
||
69597 | 157 |
\<^item> A postprocessor function \<^ML_type>\<open>term -> term\<close>. |
65041 | 158 |
|
159 |
\<^item> The resulting value as optional argument. |
|
160 |
||
161 |
The functional argument is supposed to compose the final result |
|
162 |
from these in a suitable manner. |
|
163 |
||
164 |
\noindent A simple application: |
|
165 |
\<close> |
|
166 |
||
69660
2bc2a8599369
canonical operation to typeset generated code makes dedicated environment obsolete
haftmann
parents:
69597
diff
changeset
|
167 |
ML_val %quote \<open> |
69597 | 168 |
comp_nat \<^context> \<^term>\<open>sum_list [Suc 0, Suc (Suc 0)] * Suc (Suc 0)\<close> |
65041 | 169 |
\<close> |
170 |
||
171 |
text \<open> |
|
172 |
\noindent A single ML block may contain an arbitrary number of computation |
|
173 |
antiquotations. These share the \<^emph>\<open>same\<close> set of possible |
|
174 |
input constants. In other words, it does not matter in which |
|
175 |
antiquotation constants are specified; in the following example, |
|
176 |
\<^emph>\<open>all\<close> constants are specified by the first antiquotation once |
|
177 |
and for all: |
|
178 |
\<close> |
|
179 |
||
69660
2bc2a8599369
canonical operation to typeset generated code makes dedicated environment obsolete
haftmann
parents:
69597
diff
changeset
|
180 |
ML %quote \<open> |
65041 | 181 |
local |
182 |
||
183 |
fun int_of_nat @{code "0 :: nat"} = 0 |
|
184 |
| int_of_nat (@{code Suc} n) = int_of_nat n + 1; |
|
185 |
||
186 |
in |
|
187 |
||
188 |
val comp_nat = @{computation nat terms: |
|
189 |
"plus :: nat \<Rightarrow> nat \<Rightarrow> nat" "times :: nat \<Rightarrow> nat \<Rightarrow> nat" |
|
190 |
"sum_list :: nat list \<Rightarrow> nat" "prod_list :: nat list \<Rightarrow> nat" |
|
191 |
"replicate :: nat \<Rightarrow> nat \<Rightarrow> nat list" |
|
192 |
datatypes: nat "nat list"} |
|
193 |
(fn post => post o HOLogic.mk_nat o int_of_nat o the); |
|
194 |
||
195 |
val comp_nat_list = @{computation "nat list"} |
|
69597 | 196 |
(fn post => post o HOLogic.mk_list \<^typ>\<open>nat\<close> o |
65041 | 197 |
map (HOLogic.mk_nat o int_of_nat) o the); |
198 |
||
199 |
end |
|
200 |
\<close> |
|
201 |
||
202 |
||
203 |
subsection \<open>Pitfalls when specifying input constants \label{sec:input_constants_pitfalls}\<close> |
|
204 |
||
205 |
text \<open> |
|
206 |
\<^descr> \<open>Complete type coverage.\<close> Specified input constants must |
|
207 |
be \<^emph>\<open>complete\<close> in the sense that for each |
|
69505 | 208 |
required type \<open>\<tau>\<close> there is at least one corresponding |
65041 | 209 |
input constant which can actually \<^emph>\<open>construct\<close> a concrete |
69505 | 210 |
value of type \<open>\<tau>\<close>, potentially requiring more types recursively; |
65041 | 211 |
otherwise the system of equations cannot be generated properly. |
212 |
Hence such incomplete input constants sets are rejected immediately. |
|
213 |
||
214 |
\<^descr> \<open>Unsuitful right hand sides.\<close> The generated code for a computation |
|
215 |
must compile in the strict ML runtime environment. This imposes |
|
216 |
the technical restriction that each compiled input constant |
|
69505 | 217 |
\<open>f\<^sub>C\<close> on the right hand side of a generated equations |
65041 | 218 |
must compile without throwing an exception. That rules |
219 |
out pathological examples like @{term [source] "undefined :: nat"} |
|
220 |
as input constants, as well as abstract constructors (cf. \secref{sec:invariant}). |
|
221 |
||
222 |
\<^descr> \<open>Preprocessing.\<close> For consistency, input constants are subject |
|
223 |
to preprocessing; however, the overall approach requires |
|
69505 | 224 |
to operate on constants \<open>C\<close> and their respective compiled images |
225 |
\<open>f\<^sub>C\<close>.\footnote{Technical restrictions of the implementation |
|
65041 | 226 |
enforce this, although those could be lifted in the future.} |
227 |
This is a problem whenever preprocessing maps an input constant |
|
228 |
to a non-constant. |
|
229 |
||
230 |
To circumvent these situations, the computation machinery |
|
231 |
has a dedicated preprocessor which is applied \<^emph>\<open>before\<close> |
|
232 |
the regular preprocessing, both to input constants as well as |
|
233 |
input terms. This can be used to map problematic constants |
|
234 |
to other ones that are not subject to regular preprocessing. |
|
235 |
Rewrite rules are added using attribute @{attribute code_computation_unfold}. |
|
236 |
There should rarely be a need to use this beyond the few default |
|
237 |
setups in HOL, which deal with literals (see also \secref{sec:literal_input}). |
|
238 |
\<close> |
|
239 |
||
240 |
||
241 |
subsection \<open>Pitfalls concerning input terms\<close> |
|
242 |
||
243 |
text \<open> |
|
244 |
\<^descr> \<open>No polymorphims.\<close> Input terms must be monomorphic: compilation |
|
245 |
to ML requires dedicated choice of monomorphic types. |
|
246 |
||
247 |
\<^descr> \<open>No abstractions.\<close> Only constants and applications are admissible |
|
248 |
as input; abstractions are not possible. In theory, the |
|
249 |
compilation schema could be extended to cover abstractions also, |
|
250 |
but this would increase the trusted code base. If abstractions |
|
251 |
are required, they can always be eliminated by a dedicated preprocessing |
|
252 |
step, e.g.~using combinatorial logic. |
|
253 |
||
254 |
\<^descr> \<open>Potential interfering of the preprocessor.\<close> As described in \secref{sec:input_constants_pitfalls} |
|
255 |
regular preprocessing can have a disruptive effect for input constants. |
|
256 |
The same also applies to input terms; however the same measures |
|
257 |
to circumvent that problem for input constants apply to input terms also. |
|
258 |
\<close> |
|
259 |
||
260 |
||
69505 | 261 |
subsection \<open>Computations using the \<open>computation_conv\<close> antiquotation\<close> |
65041 | 262 |
|
263 |
text \<open> |
|
264 |
Computations are a device to implement fast proof procedures. |
|
265 |
Then results of a computation are often assumed to be trustable |
|
67299 | 266 |
and thus wrapped in oracles (see @{cite "isabelle-isar-ref"}), |
65041 | 267 |
as in the following example:\footnote{ |
268 |
The technical details how numerals are dealt with are given later in |
|
269 |
\secref{sec:literal_input}.} |
|
270 |
\<close> |
|
271 |
||
69660
2bc2a8599369
canonical operation to typeset generated code makes dedicated environment obsolete
haftmann
parents:
69597
diff
changeset
|
272 |
ML %quote \<open> |
65041 | 273 |
local |
274 |
||
74582 | 275 |
fun raw_dvd (b, ct) = |
276 |
\<^instantiate>\<open>x = ct and y = \<open>if b then \<^cterm>\<open>True\<close> else \<^cterm>\<open>False\<close>\<close> |
|
74584 | 277 |
in cterm \<open>x \<equiv> y\<close> for x y :: bool\<close>; |
65041 | 278 |
|
279 |
val (_, dvd_oracle) = Context.>>> (Context.map_theory_result |
|
69597 | 280 |
(Thm.add_oracle (\<^binding>\<open>dvd\<close>, raw_dvd))); |
65041 | 281 |
|
282 |
in |
|
283 |
||
284 |
val conv_dvd = @{computation_conv bool terms: |
|
285 |
"Rings.dvd :: int \<Rightarrow> int \<Rightarrow> bool" |
|
286 |
"plus :: int \<Rightarrow> int \<Rightarrow> int" |
|
287 |
"minus :: int \<Rightarrow> int \<Rightarrow> int" |
|
288 |
"times :: int \<Rightarrow> int \<Rightarrow> int" |
|
289 |
"0 :: int" "1 :: int" "2 :: int" "3 :: int" "-1 :: int" |
|
65043
fd753468786f
explicit dynamic context for gap-bridging function
haftmann
parents:
65041
diff
changeset
|
290 |
} (K (curry dvd_oracle)) |
65041 | 291 |
|
292 |
end |
|
293 |
\<close> |
|
294 |
||
295 |
text \<open> |
|
296 |
\<^item> Antiquotation @{ML_antiquotation computation_conv} basically yields |
|
69597 | 297 |
a conversion of type \<^ML_type>\<open>Proof.context -> cterm -> thm\<close> |
67299 | 298 |
(see further @{cite "isabelle-implementation"}). |
65041 | 299 |
|
300 |
\<^item> The antiquotation expects one functional argument to bridge the |
|
301 |
\qt{untrusted gap}; this can be done e.g.~using an oracle. Since that oracle |
|
302 |
will only yield \qt{valid} results in the context of that particular |
|
303 |
computation, the implementor must make sure that it does not leave |
|
304 |
the local ML scope; in this example, this is achieved using |
|
69505 | 305 |
an explicit \<open>local\<close> ML block. The very presence of the oracle |
65041 | 306 |
in the code acknowledges that each computation requires explicit thinking |
307 |
before it can be considered trustworthy! |
|
308 |
||
309 |
\<^item> Postprocessing just operates as further conversion after normalization. |
|
310 |
||
311 |
\<^item> Partiality makes the whole conversion fall back to reflexivity. |
|
312 |
\<close> (*<*) |
|
313 |
||
69660
2bc2a8599369
canonical operation to typeset generated code makes dedicated environment obsolete
haftmann
parents:
69597
diff
changeset
|
314 |
(*>*) ML_val %quote \<open> |
69597 | 315 |
conv_dvd \<^context> \<^cterm>\<open>7 dvd ( 62437867527846782 :: int)\<close>; |
316 |
conv_dvd \<^context> \<^cterm>\<open>7 dvd (-62437867527846783 :: int)\<close>; |
|
65041 | 317 |
\<close> |
318 |
||
319 |
text \<open> |
|
320 |
\noindent An oracle is not the only way to construct a valid theorem. |
|
321 |
A computation result can be used to construct an appropriate certificate: |
|
322 |
\<close> |
|
323 |
||
324 |
lemma %quote conv_div_cert: |
|
325 |
"(Code_Target_Int.positive r * Code_Target_Int.positive s) |
|
326 |
div Code_Target_Int.positive s \<equiv> (numeral r :: int)" (is "?lhs \<equiv> ?rhs") |
|
327 |
proof (rule eq_reflection) |
|
328 |
have "?lhs = numeral r * numeral s div numeral s" |
|
329 |
by simp |
|
330 |
also have "numeral r * numeral s div numeral s = ?rhs" |
|
331 |
by (rule nonzero_mult_div_cancel_right) simp |
|
332 |
finally show "?lhs = ?rhs" . |
|
333 |
qed |
|
334 |
||
335 |
lemma %quote positive_mult: |
|
336 |
"Code_Target_Int.positive r * Code_Target_Int.positive s = |
|
337 |
Code_Target_Int.positive (r * s)" |
|
338 |
by simp |
|
339 |
||
69660
2bc2a8599369
canonical operation to typeset generated code makes dedicated environment obsolete
haftmann
parents:
69597
diff
changeset
|
340 |
ML %quote \<open> |
65041 | 341 |
local |
342 |
||
343 |
fun integer_of_int (@{code int_of_integer} k) = k |
|
344 |
||
69597 | 345 |
val cterm_of_int = Thm.cterm_of \<^context> o HOLogic.mk_numeral o integer_of_int; |
65041 | 346 |
|
347 |
val divisor = Thm.dest_arg o Thm.dest_arg; |
|
348 |
||
65043
fd753468786f
explicit dynamic context for gap-bridging function
haftmann
parents:
65041
diff
changeset
|
349 |
val evaluate_simps = map mk_eq @{thms arith_simps positive_mult}; |
65041 | 350 |
|
65043
fd753468786f
explicit dynamic context for gap-bridging function
haftmann
parents:
65041
diff
changeset
|
351 |
fun evaluate ctxt = |
fd753468786f
explicit dynamic context for gap-bridging function
haftmann
parents:
65041
diff
changeset
|
352 |
Simplifier.rewrite_rule ctxt evaluate_simps; |
fd753468786f
explicit dynamic context for gap-bridging function
haftmann
parents:
65041
diff
changeset
|
353 |
|
fd753468786f
explicit dynamic context for gap-bridging function
haftmann
parents:
65041
diff
changeset
|
354 |
fun revaluate ctxt k ct = |
65041 | 355 |
@{thm conv_div_cert} |
356 |
|> Thm.instantiate' [] [SOME (cterm_of_int k), SOME (divisor ct)] |
|
65043
fd753468786f
explicit dynamic context for gap-bridging function
haftmann
parents:
65041
diff
changeset
|
357 |
|> evaluate ctxt; |
65041 | 358 |
|
359 |
in |
|
360 |
||
361 |
val conv_div = @{computation_conv int terms: |
|
362 |
"divide :: int \<Rightarrow> int \<Rightarrow> int" |
|
363 |
"0 :: int" "1 :: int" "2 :: int" "3 :: int" |
|
364 |
} revaluate |
|
365 |
||
366 |
end |
|
367 |
\<close> |
|
368 |
||
69660
2bc2a8599369
canonical operation to typeset generated code makes dedicated environment obsolete
haftmann
parents:
69597
diff
changeset
|
369 |
ML_val %quote \<open> |
69597 | 370 |
conv_div \<^context> |
371 |
\<^cterm>\<open>46782454343499999992777742432342242323423425 div (7 :: int)\<close> |
|
65041 | 372 |
\<close> |
373 |
||
374 |
text \<open> |
|
375 |
\noindent The example is intentionally kept simple: only positive |
|
376 |
integers are covered, only remainder-free divisions are feasible, |
|
377 |
and the input term is expected to have a particular shape. |
|
378 |
This exhibits the idea more clearly: |
|
379 |
the result of the computation is used as a mere |
|
380 |
hint how to instantiate @{fact conv_div_cert}, from which the required |
|
381 |
theorem is obtained by performing multiplication using the |
|
382 |
simplifier; hence that theorem is built of proper inferences, |
|
383 |
with no oracles involved. |
|
384 |
\<close> |
|
385 |
||
386 |
||
69505 | 387 |
subsection \<open>Computations using the \<open>computation_check\<close> antiquotation\<close> |
65041 | 388 |
|
389 |
text \<open> |
|
69505 | 390 |
The \<open>computation_check\<close> antiquotation is convenient if |
65041 | 391 |
only a positive checking of propositions is desired, because then |
69597 | 392 |
the result type is fixed (\<^typ>\<open>prop\<close>) and all the technical |
65041 | 393 |
matter concerning postprocessing and oracles is done in the framework |
394 |
once and for all: |
|
395 |
\<close> |
|
396 |
||
69660
2bc2a8599369
canonical operation to typeset generated code makes dedicated environment obsolete
haftmann
parents:
69597
diff
changeset
|
397 |
ML %quote \<open> |
65041 | 398 |
val check_nat = @{computation_check terms: |
399 |
Trueprop "less :: nat \<Rightarrow> nat \<Rightarrow> bool" "plus :: nat \<Rightarrow> nat \<Rightarrow> nat" |
|
400 |
"times :: nat \<Rightarrow> nat \<Rightarrow> nat" |
|
401 |
"0 :: nat" Suc |
|
402 |
} |
|
403 |
\<close> |
|
404 |
||
405 |
text \<open> |
|
69597 | 406 |
\noindent The HOL judgement \<^term>\<open>Trueprop\<close> embeds an expression |
407 |
of type \<^typ>\<open>bool\<close> into \<^typ>\<open>prop\<close>. |
|
65041 | 408 |
\<close> |
409 |
||
69660
2bc2a8599369
canonical operation to typeset generated code makes dedicated environment obsolete
haftmann
parents:
69597
diff
changeset
|
410 |
ML_val %quote \<open> |
69597 | 411 |
check_nat \<^context> \<^cprop>\<open>less (Suc (Suc 0)) (Suc (Suc (Suc 0)))\<close> |
65041 | 412 |
\<close> |
413 |
||
414 |
text \<open> |
|
415 |
\noindent Note that such computations can only \<^emph>\<open>check\<close> |
|
69597 | 416 |
for \<^typ>\<open>prop\<close>s to hold but not \<^emph>\<open>decide\<close>. |
65041 | 417 |
\<close> |
418 |
||
419 |
||
420 |
subsection \<open>Some practical hints\<close> |
|
421 |
||
422 |
subsubsection \<open>Inspecting generated code\<close> |
|
423 |
||
424 |
text \<open> |
|
425 |
The antiquotations for computations attempt to produce meaningful error |
|
426 |
messages. If these are not sufficient, it might by useful to |
|
427 |
inspect the generated code, which can be achieved using |
|
428 |
\<close> |
|
429 |
||
430 |
declare %quote [[ML_source_trace]] (*<*) declare %quote [[ML_source_trace = false]] (*>*) |
|
431 |
||
432 |
||
433 |
subsubsection \<open>Literals as input constants \label{sec:literal_input}\<close> |
|
434 |
||
435 |
text \<open> |
|
436 |
Literals (characters, numerals) in computations cannot be processed |
|
437 |
naively: the compilation pattern for computations fails whenever |
|
438 |
target-language literals are involved; since various |
|
439 |
common code generator setups (see \secref{sec:common_adaptation}) |
|
69597 | 440 |
implement \<^typ>\<open>nat\<close> and \<^typ>\<open>int\<close> by target-language literals, |
65041 | 441 |
this problem manifests whenever numeric types are involved. |
442 |
In practice, this is circumvented with a dedicated preprocessor |
|
443 |
setup for literals (see also \secref{sec:input_constants_pitfalls}). |
|
444 |
||
445 |
The following examples illustrate the pattern |
|
446 |
how to specify input constants when literals are involved, without going into |
|
447 |
too much detail: |
|
448 |
\<close> |
|
449 |
||
69597 | 450 |
paragraph \<open>An example for \<^typ>\<open>nat\<close>\<close> |
65041 | 451 |
|
69660
2bc2a8599369
canonical operation to typeset generated code makes dedicated environment obsolete
haftmann
parents:
69597
diff
changeset
|
452 |
ML %quote \<open> |
65041 | 453 |
val check_nat = @{computation_check terms: |
454 |
Trueprop "even :: nat \<Rightarrow> bool" "plus :: nat \<Rightarrow> nat \<Rightarrow> nat" |
|
455 |
"0 :: nat" Suc "1 :: nat" "2 :: nat" "3 :: nat" |
|
456 |
} |
|
457 |
\<close> |
|
458 |
||
69660
2bc2a8599369
canonical operation to typeset generated code makes dedicated environment obsolete
haftmann
parents:
69597
diff
changeset
|
459 |
ML_val %quote \<open> |
69597 | 460 |
check_nat \<^context> \<^cprop>\<open>even (Suc 0 + 1 + 2 + 3 + 4 + 5)\<close> |
65041 | 461 |
\<close> |
462 |
||
69597 | 463 |
paragraph \<open>An example for \<^typ>\<open>int\<close>\<close> |
65041 | 464 |
|
69660
2bc2a8599369
canonical operation to typeset generated code makes dedicated environment obsolete
haftmann
parents:
69597
diff
changeset
|
465 |
ML %quote \<open> |
65041 | 466 |
val check_int = @{computation_check terms: |
467 |
Trueprop "even :: int \<Rightarrow> bool" "plus :: int \<Rightarrow> int \<Rightarrow> int" |
|
468 |
"0 :: int" "1 :: int" "2 :: int" "3 :: int" "-1 :: int" |
|
469 |
} |
|
470 |
\<close> |
|
471 |
||
69660
2bc2a8599369
canonical operation to typeset generated code makes dedicated environment obsolete
haftmann
parents:
69597
diff
changeset
|
472 |
ML_val %quote \<open> |
69597 | 473 |
check_int \<^context> \<^cprop>\<open>even ((0::int) + 1 + 2 + 3 + -1 + -2 + -3)\<close> |
65041 | 474 |
\<close> |
475 |
||
69597 | 476 |
paragraph \<open>An example for \<^typ>\<open>String.literal\<close>\<close> |
65041 | 477 |
|
68028 | 478 |
definition %quote is_cap_letter :: "String.literal \<Rightarrow> bool" |
479 |
where "is_cap_letter s \<longleftrightarrow> (case String.asciis_of_literal s |
|
480 |
of [] \<Rightarrow> False | k # _ \<Rightarrow> 65 \<le> k \<and> k \<le> 90)" (*<*) |
|
65041 | 481 |
|
69660
2bc2a8599369
canonical operation to typeset generated code makes dedicated environment obsolete
haftmann
parents:
69597
diff
changeset
|
482 |
(*>*) ML %quote \<open> |
68028 | 483 |
val check_literal = @{computation_check terms: |
484 |
Trueprop is_cap_letter datatypes: bool String.literal |
|
65041 | 485 |
} |
486 |
\<close> |
|
487 |
||
69660
2bc2a8599369
canonical operation to typeset generated code makes dedicated environment obsolete
haftmann
parents:
69597
diff
changeset
|
488 |
ML_val %quote \<open> |
69597 | 489 |
check_literal \<^context> \<^cprop>\<open>is_cap_letter (STR ''Q'')\<close> |
65041 | 490 |
\<close> |
491 |
||
492 |
||
493 |
subsubsection \<open>Preprocessing HOL terms into evaluable shape\<close> |
|
494 |
||
495 |
text \<open> |
|
496 |
When integrating decision procedures developed inside HOL into HOL itself, |
|
497 |
a common approach is to use a deep embedding where operators etc. |
|
498 |
are represented by datatypes in Isabelle/HOL. Then it is necessary |
|
499 |
to turn generic shallowly embedded statements into that particular |
|
500 |
deep embedding (\qt{reification}). |
|
501 |
||
502 |
One option is to hardcode using code antiquotations (see \secref{sec:code_antiq}). |
|
503 |
Another option is to use pre-existing infrastructure in HOL: |
|
69597 | 504 |
\<^ML>\<open>Reification.conv\<close> and \<^ML>\<open>Reification.tac\<close>. |
65041 | 505 |
|
506 |
A simplistic example: |
|
507 |
\<close> |
|
508 |
||
509 |
datatype %quote form_ord = T | F | Less nat nat |
|
510 |
| And form_ord form_ord | Or form_ord form_ord | Neg form_ord |
|
511 |
||
512 |
primrec %quote interp :: "form_ord \<Rightarrow> 'a::order list \<Rightarrow> bool" |
|
513 |
where |
|
514 |
"interp T vs \<longleftrightarrow> True" |
|
515 |
| "interp F vs \<longleftrightarrow> False" |
|
516 |
| "interp (Less i j) vs \<longleftrightarrow> vs ! i < vs ! j" |
|
517 |
| "interp (And f1 f2) vs \<longleftrightarrow> interp f1 vs \<and> interp f2 vs" |
|
518 |
| "interp (Or f1 f2) vs \<longleftrightarrow> interp f1 vs \<or> interp f2 vs" |
|
519 |
| "interp (Neg f) vs \<longleftrightarrow> \<not> interp f vs" |
|
520 |
||
521 |
text \<open> |
|
69597 | 522 |
\noindent The datatype \<^type>\<open>form_ord\<close> represents formulae whose semantics is given by |
523 |
\<^const>\<open>interp\<close>. Note that values are represented by variable indices (\<^typ>\<open>nat\<close>) |
|
524 |
whose concrete values are given in list \<^term>\<open>vs\<close>. |
|
65041 | 525 |
\<close> |
526 |
||
69660
2bc2a8599369
canonical operation to typeset generated code makes dedicated environment obsolete
haftmann
parents:
69597
diff
changeset
|
527 |
ML %quote (*<*) \<open>\<close> |
65041 | 528 |
lemma "thm": fixes x y z :: "'a::order" shows "x < y \<and> x < z \<equiv> interp (And (Less (Suc 0) (Suc (Suc 0))) (Less (Suc 0) 0)) [z, x, y]" |
69660
2bc2a8599369
canonical operation to typeset generated code makes dedicated environment obsolete
haftmann
parents:
69597
diff
changeset
|
529 |
ML_prf %quote |
65041 | 530 |
(*>*) \<open>val thm = |
69597 | 531 |
Reification.conv \<^context> @{thms interp.simps} \<^cterm>\<open>x < y \<and> x < z\<close>\<close> (*<*) |
532 |
by (tactic \<open>ALLGOALS (resolve_tac \<^context> [thm])\<close>) |
|
69660
2bc2a8599369
canonical operation to typeset generated code makes dedicated environment obsolete
haftmann
parents:
69597
diff
changeset
|
533 |
(*>*) |
65041 | 534 |
|
535 |
text \<open> |
|
69597 | 536 |
\noindent By virtue of @{fact interp.simps}, \<^ML>\<open>Reification.conv\<close> provides a conversion |
65041 | 537 |
which, for this concrete example, yields @{thm thm [no_vars]}. Note that the argument |
69597 | 538 |
to \<^const>\<open>interp\<close> does not contain any free variables and can thus be evaluated |
65041 | 539 |
using evaluation. |
540 |
||
69505 | 541 |
A less meager example can be found in the AFP, session \<open>Regular-Sets\<close>, |
542 |
theory \<open>Regexp_Method\<close>. |
|
65041 | 543 |
\<close> |
544 |
||
545 |
end |