1 (*<*)

     2 theory CallML

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

     4 begin

     5 (*>*)

     6 

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

     8 

     9 text{* 

    10   {\bf Problem:} 

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

    12 

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

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

    15 

    16 

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

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

    19   verify some complicated algorithm, have the algorithm produce an easily

    20   checkable certificate. For example, rather than verify a primality test,

    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

    23   certificate, that for primality, although it, too, can be treated in the

    24   same manner. 

    25 

    26   The example we looking at here is an ML function for finding a factor 

    27   of a number. We first declare its type:

    28 *}

    29 

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

    31 

    32 text{* 

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

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

    35   actual definition is: 

    36 *}

    37 

    38 lemma factor_non_prime:

    39   assumes "let k = factor n in k \<noteq> 1 \<and> k \<noteq> n \<and> k dvd n"

    40   shows "\<not> prime n"

    41 using assms by(auto simp: prime_nat_def Let_def)

    42 

    43 text{* 

    44   Note that the premise is executable once we have defined 

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

    46 *}

    47 

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

    49 

    50 text{* 

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

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

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

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

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

    56 

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

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

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

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

    61   to connect the two levels:

    62 *}

    63 

    64 code_const factor (SML "factor")

    65 

    66 text{* 

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

    68   is executable and command 

    69 *}

    70 

    71 value "factor 4"

    72 

    73 text{* 

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

    75   @{text 4} is not prime: 

    76 *}

    77 

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

    79   apply(rule factor_non_prime)

    80   apply eval

    81   done

    82 

    83 text{* 

    84   Note, hawever, 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

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

    87   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

    89   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''

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

    92   proofs.

    93 

    94   The above example was easy because we forced Iabelle (via the inclusion of @{theory

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

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

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

    98   on @{const factor} also works: 

    99 *}

   100 

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

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

   103 code_const factor2 (SML "factor2")

   104 

   105 value "factor2 4"

   106 

   107 text{* 

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

   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 

   111   interface with ML-functions whose types involve 

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

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

   114   them as nested pairs.

   115 

   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

   118   datatype for the result: 

   119 *}

   120 

   121 datatype result = Factor nat | Prime

   122 

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

   124 

   125 text{* 

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

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

   128 *}

   129 

   130 code_reflect Result

   131   datatypes result = Factor | Prime

   132 

   133 text{* 

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

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

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

   137   write ML-code that uses this datatype: 

   138 *}

   139 

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

   141 

   142 text{* 

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

   144   before: 

   145 *}

   146 

   147 code_const factor' (SML "factor'")

   148 

   149 text{* 

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

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

   152 

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

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

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

   156 *}

   157 

   158 (*<*)

   159 value "factor' 4"

   160 

   161 end

   162 (*>*)