21 have the test produce a factor of the input as a witness to |
21 have the test produce a factor of the input as a witness to |
22 non-primality. This is only an example, and we ignore the converse |
22 non-primality. This is only an example, and we ignore the converse |
23 certificate, that for primality, although it, too, can be treated in the |
23 certificate, that for primality, although it, too, can be treated in the |
24 same manner. |
24 same manner. |
25 |
25 |
26 The example we looking at here is an ML function for finding a factor |
26 The example we are looking at here is an ML function for finding a factor |
27 of a number. We first declare its type: |
27 of a number. We first declare its type: |
28 *} |
28 *} |
29 |
29 |
30 consts factor :: "nat \<Rightarrow> nat" |
30 consts factor :: "nat \<Rightarrow> nat" |
31 |
31 |
34 we can prove non-primality via @{const factor}, no matter what its |
34 we can prove non-primality via @{const factor}, no matter what its |
35 actual definition is: |
35 actual definition is: |
36 *} |
36 *} |
37 |
37 |
38 lemma factor_non_prime: |
38 lemma factor_non_prime: |
39 assumes "let k = factor n in k \<noteq> 1 \<and> k \<noteq> n \<and> k dvd n" |
39 "let k = factor n in k \<noteq> 1 \<and> k \<noteq> n \<and> k dvd n \<Longrightarrow> \<not> prime n" |
40 shows "\<not> prime n" |
40 by (auto simp: prime_nat_def Let_def) |
41 using assms by(auto simp: prime_nat_def Let_def) |
|
42 |
41 |
43 text{* |
42 text{* |
44 Note that the premise is executable once we have defined |
43 Note that the premise is executable once we have defined |
45 @{const factor}. Here is a trivial definition in ML: |
44 @{const factor}. Here is a trivial definition in ML: |
46 *} |
45 *} |
79 apply(rule factor_non_prime) |
78 apply(rule factor_non_prime) |
80 apply eval |
79 apply eval |
81 done |
80 done |
82 |
81 |
83 text{* |
82 text{* |
84 Note, hawever, the command \isacommand{code\_const} cannot check that the ML function |
83 Note, however, the command \isacommand{code\_const} cannot check that the ML function |
85 has the required type. Therefore in the worst case a type mismatch will be detected by |
84 has the required type. Therefore in the worst case a type mismatch will be detected by |
86 the ML-compiler when we try to evaluate an expression involving @{const |
85 the ML-compiler when we try to evaluate an expression involving @{const |
87 factor}. It could also happen that @{const factor} is (accidentally) |
86 factor}. It could also happen that @{const factor} is (accidentally) |
88 redefined on the ML level later on. But remember that we do not assume |
87 redefined on the ML level later on. But remember that we do not assume |
89 anything about @{const factor} on the HOL-level. Hence no definition of |
88 anything about @{const factor} on the HOL-level. Hence no definition of |
90 @{const factor} can ever lead to an incorrect proof. Of course ``wrong'' |
89 @{const factor} can ever lead to an incorrect proof. Of course ``wrong'' |
91 definitions can lead to compile time or run time exceptions, or to failed |
90 definitions can lead to compile time or run time exceptions, or to failed |
92 proofs. |
91 proofs. |
93 |
92 |
94 The above example was easy because we forced Iabelle (via the inclusion of @{theory |
93 The above example was easy because we forced Isabelle (via the inclusion of the |
|
94 theory @{theory |
95 Efficient_Nat}) to implement @{typ nat} by @{text int}, a predefined |
95 Efficient_Nat}) to implement @{typ nat} by @{text int}, a predefined |
96 ML-type. By default, Isabelle implements, for example, the HOL-type |
96 ML-type. By default, Isabelle implements, for example, the HOL-type |
97 @{text list} by the corresponding ML-type. Thus the following variation |
97 @{text list} by the corresponding ML-type. Thus the following variation |
98 on @{const factor} also works: |
98 on @{const factor} also works: |
99 *} |
99 *} |
107 text{* |
107 text{* |
108 The first line declares the type of @{const factor2}; the second |
108 The first line declares the type of @{const factor2}; the second |
109 gives its implementation in ML; the third makes it executable |
109 gives its implementation in ML; the third makes it executable |
110 in HOL, and the last is just a test. In this way, you can easily |
110 in HOL, and the last is just a test. In this way, you can easily |
111 interface with ML-functions whose types involve |
111 interface with ML-functions whose types involve |
112 @{text bool}, @{text int}, @{text list}, @{text option} and @{text pairs}, |
112 @{text bool}, @{text int}, @{text list}, @{text option} and pairs, |
113 only. If you have arbitrary tuples, for example, then you have to code |
113 only. If you have arbitrary tuples, for example, then you have to code |
114 them as nested pairs. |
114 them as nested pairs. |
115 |
115 |
116 Let us now look at how to refer to user-defined HOL-datatypes from the |
116 Let us now look at how to refer to user-defined HOL-datatypes from the |
117 ML-level. We modify our @{const factor} example a little by introducing a new |
117 ML-level. We modify our @{const factor} example a little by introducing a new |