1 (*<*)

     2 theory CallML

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

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

     5 begin

     6 (*>*)

     7 

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

     9 

    10 text{* 

    11   {\bf Problem:} 

    12   How to call ML functions from within HOL?\smallskip

    13 

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

    15   and \isacommand{code\_reflect}.\smallskip

    16 

    17 

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

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

    20   verifying some complicated algorithm, have the algorithm produce an easily

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

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

    23   non-primality. 

    24 

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

    26   declare its type:

    27 *}

    28 

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

    30 

    31 text{* 

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

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

    34   actual definition is: 

    35 *}

    36 

    37 lemma factor_non_prime:

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

    39   by (auto simp: prime_nat_def Let_def)

    40 

    41 text{* 

    42   Note that the premise is executable once we have defined 

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

    44 *}

    45 

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

    47 

    48 text{* 

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

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

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

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

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

    54 

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

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

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

    58 

    59   \begin{graybox}\small

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

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

    62   ...

    63   \end{graybox}

    64 

    65 

    66   Thus the ML implementation of

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

    68   to connect the two levels:

    69 *}

    70 

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

    72 where

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

    74 

    75 lemma [code]:

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

    77   by (simp add: factor_integer_def fun_eq_iff)

    78 

    79 code_const factor_integer (SML "factor")

    80 code_reserved SML factor

    81 

    82 text{* 

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

    84   is executable and command 

    85 *}

    86 

    87 value "factor 4"

    88 

    89 text{* 

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

    91   @{text 4} is not prime: 

    92 *}

    93 

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

    95   apply(rule factor_non_prime)

    96   apply eval

    97   done

    98 

    99 text{* 

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

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

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

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

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

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

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

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

   108   proofs.

   109 

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

   111   theory @{theory

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

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

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

   115   on @{const factor} also works: 

   116 *}

   117 

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

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

   120 

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

   122 where

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

   124 

   125 lemma [code]:

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

   127   by (simp add: factor2_integer_def fun_eq_iff comp_def)

   128 

   129 code_const factor2_integer (SML "factor2")

   130 code_reserved SML factor2

   131 

   132 text{* 

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

   134   gives its implementation in ML; the third makes it executable 

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

   136   interface with ML-functions whose types involve 

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

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

   139   them as nested pairs.

   140 *}

   141 

   142 value "factor2 4"

   143 

   144 end

   145 (*>*)