(*<*)

theory CallML

imports "~~/src/HOL/Number_Theory/Primes" 

        "~~/src/HOL/Library/Efficient_Nat"

begin

(*>*)

section {* Calling ML Functions from within HOL \label{rec:callml} *}

text{* 

  {\bf Problem:} 

  How to call ML functions from within HOL?\smallskip

  {\bf Solution:} This can be achieved with \isacommand{code\_const}

  and \isacommand{code\_reflect}.\smallskip

  To make it clear we mean here calling unverified ML functions from within

  HOL! The motivation is the paradigm of \emph{result checking}: rather than

  verifying some complicated algorithm, have the algorithm produce an easily

  checkable certificate. For example, instead of verifying an algorithm for 

  testing non-primality, have an algorithm that produces a factor as a witness to

  non-primality. 

  The algorithm is an ML function finding a factor of a number. We first 

  declare its type:

*}

consts factor :: "nat \<Rightarrow> nat"

text{* 

  Its definition will be given below in ML. But the whole point is that

  we can prove non-primality via @{const factor}, no matter what its

  actual definition is: 

*}

lemma factor_non_prime:

  "let k = factor n in k \<noteq> 1 \<and> k \<noteq> n \<and> k dvd n \<Longrightarrow> \<not> prime n"

  by (auto simp: prime_nat_def Let_def)

text{* 

  Note that the premise is executable once we have defined 

  @{const factor}. Here is a trivial definition in ML: 

*}

ML{*fun factor n = if n = 4 then 2 else 1*}

text{* 

  Of course this trivial definition of @{const factor} could have been given

  directly in HOL rather than ML. But by going to the ML level, all of ML is

  at our disposal, including arrays and references, features that are less

  easily emulated in HOL. In fact, we could even call some external software

  from ML, e.g.\ a computer algebra system.

  It should be noted, however, that in this example you need to import the

  theory @{theory Efficient_Nat} in order to force the HOL-type @{typ nat} to

  be implemented by the ML-type @{text "int"}. Thus the ML implementation of

  @{const factor} must be and is of type @{text "int -> int"}. Now it is time

  to connect the two levels:

*}

code_const factor (SML "factor")

text{* 

  The result of this declaration is that the HOL-function @{const factor} 

  is executable and command 

*}

value "factor 4"

text{* 

  yields the expected result @{text 2}. Similarly we can prove that

  @{text 4} is not prime: 

*}

lemma "\<not> prime (4::nat)"

  apply(rule factor_non_prime)

  apply eval

  done

text{* 

  Note, however, the command \isacommand{code\_const} cannot check that the ML function

  has the required type. Therefore in the worst case a type mismatch will be detected by

  the ML-compiler when we try to evaluate an expression involving @{const

  factor}. It could also happen that @{const factor} is (accidentally)

  redefined on the ML level later on. But remember that we do not assume

  anything about @{const factor} on the HOL-level. Hence no definition of

  @{const factor} can ever lead to an incorrect proof. Of course ``wrong''

  definitions can lead to compile time or run time exceptions, or to failed

  proofs.

  The above example was easy because we forced Isabelle (via the inclusion of the

  theory @{theory

  Efficient_Nat}) to implement @{typ nat} by @{text int}, a predefined 

  ML-type.  By default, Isabelle implements, for example, the HOL-type 

  @{text list} by the corresponding ML-type. Thus the following variation 

  on @{const factor} also works: 

*}

consts factor2 :: "nat \<Rightarrow> nat list" (*<*)(*>*)

ML{*fun factor2 n = if n = 4 then [2] else []*}(*<*)(*>*)

code_const factor2 (SML "factor2")

value "factor2 4"

text{* 

  The first line declares the type of @{const factor2}; the second

  gives its implementation in ML; the third makes it executable 

  in HOL, and the last is just a test.  In this way, you can easily 

  interface with ML-functions whose types involve 

  @{text bool}, @{text int}, @{text list}, @{text option} and pairs, 

  only. If you have arbitrary tuples, for example, then you have to code 

  them as nested pairs.

  Let us now look at how to refer to user-defined HOL-datatypes from the

  ML-level. We modify our @{const factor} example a little by introducing a new

  datatype for the result: 

*}

datatype result = Factor nat | Prime

consts factor' :: "nat \<Rightarrow> result"

text{* 

  In order to write ML-code that uses this datatype, we need to define

  this datatype at the ML-level first. The following command does just that. 

*}

code_reflect Result

  datatypes result = Factor | Prime

text{* 

  This creates an ML-structure called @{text Result} (the name can be

  arbitrarily chosen) that contains the datatype @{typ result}. The list 

  of constructors (but not their types) needs to be given. Now we can 

  write ML-code that uses this datatype: 

*}

ML{*fun factor' n = if n = 4 then Result.Factor 2 else Result.Prime*}

text{* 

  Finally we can link the HOL and ML version of @{const factor'} as

  before: 

*}

code_const factor' (SML "factor'")

text{* 

  Now any evaluation of the HOL function @{const factor'} will use the

  corresponding ML-function, like in the examples for @{const factor} above.

  In general, \isacommand{code\_reflect} can export multiple datatypes 

  (separated by \isacommand{and}) and also HOL-functions: simply add a line

  \isacommand{functions} $f_1$ $f_2$ and so on.

*}

(*<*)

value "factor' 4"

end

(*>*)