427
|
1 |
(*<*)
|
|
2 |
theory CallML
|
459
|
3 |
imports "~~/src/HOL/Number_Theory/Primes"
|
|
4 |
"~~/src/HOL/Library/Efficient_Nat"
|
427
|
5 |
begin
|
|
6 |
(*>*)
|
|
7 |
|
|
8 |
section {* Calling ML Functions from within HOL \label{rec:callml} *}
|
|
9 |
|
|
10 |
text{*
|
|
11 |
{\bf Problem:}
|
|
12 |
How to call ML functions from within HOL?\smallskip
|
|
13 |
|
|
14 |
{\bf Solution:} This can be achieved with \isacommand{code\_const}
|
|
15 |
and \isacommand{code\_reflect}.\smallskip
|
|
16 |
|
|
17 |
|
|
18 |
To make it clear we mean here calling unverified ML functions from within
|
|
19 |
HOL! The motivation is the paradigm of \emph{result checking}: rather than
|
441
|
20 |
verifying some complicated algorithm, have the algorithm produce an easily
|
|
21 |
checkable certificate. For example, instead of verifying an algorithm for
|
|
22 |
testing non-primality, have an algorithm that produces a factor as a witness to
|
|
23 |
non-primality.
|
427
|
24 |
|
441
|
25 |
The algorithm is an ML function finding a factor of a number. We first
|
|
26 |
declare its type:
|
427
|
27 |
*}
|
|
28 |
|
|
29 |
consts factor :: "nat \<Rightarrow> nat"
|
|
30 |
|
|
31 |
text{*
|
441
|
32 |
Its definition will be given below in ML. But the whole point is that
|
427
|
33 |
we can prove non-primality via @{const factor}, no matter what its
|
|
34 |
actual definition is:
|
|
35 |
*}
|
|
36 |
|
|
37 |
lemma factor_non_prime:
|
428
|
38 |
"let k = factor n in k \<noteq> 1 \<and> k \<noteq> n \<and> k dvd n \<Longrightarrow> \<not> prime n"
|
|
39 |
by (auto simp: prime_nat_def Let_def)
|
427
|
40 |
|
|
41 |
text{*
|
|
42 |
Note that the premise is executable once we have defined
|
|
43 |
@{const factor}. Here is a trivial definition in ML:
|
|
44 |
*}
|
|
45 |
|
517
d8c376662bb4
removed special ML-setup and replaced it by explicit markups (i.e., %grayML)
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
46 |
ML %grayML{*fun factor n = if n = 4 then 2 else 1*}
|
427
|
47 |
|
|
48 |
text{*
|
|
49 |
Of course this trivial definition of @{const factor} could have been given
|
|
50 |
directly in HOL rather than ML. But by going to the ML level, all of ML is
|
|
51 |
at our disposal, including arrays and references, features that are less
|
|
52 |
easily emulated in HOL. In fact, we could even call some external software
|
|
53 |
from ML, e.g.\ a computer algebra system.
|
|
54 |
|
|
55 |
It should be noted, however, that in this example you need to import the
|
|
56 |
theory @{theory Efficient_Nat} in order to force the HOL-type @{typ nat} to
|
|
57 |
be implemented by the ML-type @{text "int"}. Thus the ML implementation of
|
|
58 |
@{const factor} must be and is of type @{text "int -> int"}. Now it is time
|
|
59 |
to connect the two levels:
|
|
60 |
*}
|
|
61 |
|
|
62 |
code_const factor (SML "factor")
|
|
63 |
|
|
64 |
text{*
|
|
65 |
The result of this declaration is that the HOL-function @{const factor}
|
|
66 |
is executable and command
|
|
67 |
*}
|
|
68 |
|
|
69 |
value "factor 4"
|
|
70 |
|
|
71 |
text{*
|
|
72 |
yields the expected result @{text 2}. Similarly we can prove that
|
|
73 |
@{text 4} is not prime:
|
|
74 |
*}
|
|
75 |
|
448
|
76 |
lemma "\<not> prime (4::nat)"
|
427
|
77 |
apply(rule factor_non_prime)
|
|
78 |
apply eval
|
|
79 |
done
|
|
80 |
|
|
81 |
text{*
|
428
|
82 |
Note, however, the command \isacommand{code\_const} cannot check that the ML function
|
427
|
83 |
has the required type. Therefore in the worst case a type mismatch will be detected by
|
|
84 |
the ML-compiler when we try to evaluate an expression involving @{const
|
|
85 |
factor}. It could also happen that @{const factor} is (accidentally)
|
|
86 |
redefined on the ML level later on. But remember that we do not assume
|
|
87 |
anything about @{const factor} on the HOL-level. Hence no definition of
|
|
88 |
@{const factor} can ever lead to an incorrect proof. Of course ``wrong''
|
|
89 |
definitions can lead to compile time or run time exceptions, or to failed
|
|
90 |
proofs.
|
|
91 |
|
428
|
92 |
The above example was easy because we forced Isabelle (via the inclusion of the
|
|
93 |
theory @{theory
|
427
|
94 |
Efficient_Nat}) to implement @{typ nat} by @{text int}, a predefined
|
|
95 |
ML-type. By default, Isabelle implements, for example, the HOL-type
|
|
96 |
@{text list} by the corresponding ML-type. Thus the following variation
|
|
97 |
on @{const factor} also works:
|
|
98 |
*}
|
|
99 |
|
|
100 |
consts factor2 :: "nat \<Rightarrow> nat list" (*<*)(*>*)
|
517
d8c376662bb4
removed special ML-setup and replaced it by explicit markups (i.e., %grayML)
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
101 |
ML %grayML{*fun factor2 n = if n = 4 then [2] else []*}(*<*)(*>*)
|
427
|
102 |
code_const factor2 (SML "factor2")
|
|
103 |
|
|
104 |
value "factor2 4"
|
|
105 |
|
|
106 |
text{*
|
|
107 |
The first line declares the type of @{const factor2}; the second
|
|
108 |
gives its implementation in ML; the third makes it executable
|
|
109 |
in HOL, and the last is just a test. In this way, you can easily
|
|
110 |
interface with ML-functions whose types involve
|
428
|
111 |
@{text bool}, @{text int}, @{text list}, @{text option} and pairs,
|
427
|
112 |
only. If you have arbitrary tuples, for example, then you have to code
|
|
113 |
them as nested pairs.
|
|
114 |
|
|
115 |
Let us now look at how to refer to user-defined HOL-datatypes from the
|
|
116 |
ML-level. We modify our @{const factor} example a little by introducing a new
|
|
117 |
datatype for the result:
|
|
118 |
*}
|
|
119 |
|
|
120 |
datatype result = Factor nat | Prime
|
|
121 |
|
|
122 |
consts factor' :: "nat \<Rightarrow> result"
|
|
123 |
|
|
124 |
text{*
|
|
125 |
In order to write ML-code that uses this datatype, we need to define
|
|
126 |
this datatype at the ML-level first. The following command does just that.
|
|
127 |
*}
|
|
128 |
|
|
129 |
code_reflect Result
|
|
130 |
datatypes result = Factor | Prime
|
|
131 |
|
|
132 |
text{*
|
|
133 |
This creates an ML-structure called @{text Result} (the name can be
|
|
134 |
arbitrarily chosen) that contains the datatype @{typ result}. The list
|
|
135 |
of constructors (but not their types) needs to be given. Now we can
|
|
136 |
write ML-code that uses this datatype:
|
|
137 |
*}
|
|
138 |
|
517
d8c376662bb4
removed special ML-setup and replaced it by explicit markups (i.e., %grayML)
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
139 |
ML %grayML{*fun factor' n = if n = 4 then Result.Factor 2 else Result.Prime*}
|
427
|
140 |
|
|
141 |
text{*
|
|
142 |
Finally we can link the HOL and ML version of @{const factor'} as
|
|
143 |
before:
|
|
144 |
*}
|
|
145 |
|
|
146 |
code_const factor' (SML "factor'")
|
|
147 |
|
|
148 |
text{*
|
|
149 |
Now any evaluation of the HOL function @{const factor'} will use the
|
|
150 |
corresponding ML-function, like in the examples for @{const factor} above.
|
|
151 |
|
|
152 |
In general, \isacommand{code\_reflect} can export multiple datatypes
|
|
153 |
(separated by \isacommand{and}) and also HOL-functions: simply add a line
|
|
154 |
\isacommand{functions} $f_1$ $f_2$ and so on.
|
|
155 |
*}
|
|
156 |
|
|
157 |
(*<*)
|
|
158 |
value "factor' 4"
|
|
159 |
|
|
160 |
end
|
517
d8c376662bb4
removed special ML-setup and replaced it by explicit markups (i.e., %grayML)
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
161 |
(*>*)
|