(*<*)
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
(*>*)