(*<*)

theory CallML

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

        "~~/src/HOL/Library/Code_Target_Numeral"

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 %grayML{*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 Code_Target_Numeral} in order to force the HOL-type @{typ nat} to

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

  \begin{graybox}\small

  \isacommand{theory}~@{text CallML}\\

  \isacommand{imports}~@{text Main} @{text [quotes] "~~/src/HOL/Library/Code_Target_Numeral"}\\

  ...

  \end{graybox}

  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:

*}

definition factor_integer :: "integer \<Rightarrow> integer"

where

  [code del]: "factor_integer = integer_of_nat \<circ> factor \<circ> nat_of_integer"

lemma [code]:

  "factor = nat_of_integer \<circ> factor_integer \<circ> integer_of_nat"

  by (simp add: factor_integer_def fun_eq_iff)

code_const factor_integer (SML "factor")

code_reserved 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

  Code_Target_Numeral}) 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 %grayML{*fun factor2 n = if n = 4 then [2] else []*}(*<*)(*>*)

definition factor2_integer :: "integer \<Rightarrow> integer list"

where

  [code del]: "factor2_integer = map integer_of_nat \<circ> factor2 \<circ> nat_of_integer"

lemma [code]:

  "factor2 = map nat_of_integer \<circ> factor2_integer \<circ> integer_of_nat"

  by (simp add: factor2_integer_def fun_eq_iff comp_def)

code_const factor2_integer (SML "factor2")

code_reserved SML factor2

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.

*}

value "factor2 4"

end

(*>*)