14 and \isacommand{code\_reflect}.\smallskip |
14 and \isacommand{code\_reflect}.\smallskip |
15 |
15 |
16 |
16 |
17 To make it clear we mean here calling unverified ML functions from within |
17 To make it clear we mean here calling unverified ML functions from within |
18 HOL! The motivation is the paradigm of \emph{result checking}: rather than |
18 HOL! The motivation is the paradigm of \emph{result checking}: rather than |
19 verify some complicated algorithm, have the algorithm produce an easily |
19 verifying some complicated algorithm, have the algorithm produce an easily |
20 checkable certificate. For example, rather than verify a primality test, |
20 checkable certificate. For example, instead of verifying an algorithm for |
21 have the test produce a factor of the input as a witness to |
21 testing non-primality, have an algorithm that produces a factor as a witness to |
22 non-primality. This is only an example, and we ignore the converse |
22 non-primality. |
23 certificate, that for primality, although it, too, can be treated in the |
|
24 same manner. |
|
25 |
23 |
26 The example we are looking at here is an ML function for finding a factor |
24 The algorithm is an ML function finding a factor of a number. We first |
27 of a number. We first declare its type: |
25 declare its type: |
28 *} |
26 *} |
29 |
27 |
30 consts factor :: "nat \<Rightarrow> nat" |
28 consts factor :: "nat \<Rightarrow> nat" |
31 |
29 |
32 text{* |
30 text{* |
33 Its definition will be given in ML below. But the whole point is that |
31 Its definition will be given below in ML. But the whole point is that |
34 we can prove non-primality via @{const factor}, no matter what its |
32 we can prove non-primality via @{const factor}, no matter what its |
35 actual definition is: |
33 actual definition is: |
36 *} |
34 *} |
37 |
35 |
38 lemma factor_non_prime: |
36 lemma factor_non_prime: |