# HG changeset patch # User Christian Urban # Date 1275129002 -7200 # Node ID 94538ddcac9b3920b1b18822eaa2ad27417e241a # Parent d94755882e367d25ade10d021f115af8ce17747f added example from Tobias and changed the title diff -r d94755882e36 -r 94538ddcac9b ProgTutorial/Intro.thy --- a/ProgTutorial/Intro.thy Thu May 27 10:39:07 2010 +0200 +++ b/ProgTutorial/Intro.thy Sat May 29 12:30:02 2010 +0200 @@ -262,6 +262,8 @@ \item {\bf Alexander Krauss} wrote a very early version of the ``first-steps'' chapter and also contributed the material on @{ML_funct Named_Thms}. + \item {\bf Tobias Nipkow} contributed recipe \ref{rec:callml}. + \item {\bf Michael Norrish} proofread parts of the text. \item {\bf Christian Sternagel} proofread the tutorial and made diff -r d94755882e36 -r 94538ddcac9b ProgTutorial/ROOT.ML --- a/ProgTutorial/ROOT.ML Thu May 27 10:39:07 2010 +0200 +++ b/ProgTutorial/ROOT.ML Sat May 29 12:30:02 2010 +0200 @@ -2,6 +2,8 @@ no_document use_thy "Base"; no_document use_thy "Package/Simple_Inductive_Package"; +no_document use_thy "~~/src/HOL/Number_Theory/Primes"; +no_document use_thy "Efficient_Nat"; use_thy "Intro"; use_thy "FirstSteps"; @@ -23,6 +25,7 @@ use_thy "Recipes/Antiquotes"; use_thy "Recipes/TimeLimit"; use_thy "Recipes/Timing"; +use_thy "Recipes/CallML"; use_thy "Recipes/ExternalSolver"; use_thy "Recipes/Oracle"; use_thy "Recipes/Sat"; diff -r d94755882e36 -r 94538ddcac9b ProgTutorial/Recipes/CallML.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/ProgTutorial/Recipes/CallML.thy Sat May 29 12:30:02 2010 +0200 @@ -0,0 +1,162 @@ +(*<*) +theory CallML +imports "~~/src/HOL/Number_Theory/Primes" 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 + verify some complicated algorithm, have the algorithm produce an easily + checkable certificate. For example, rather than verify a primality test, + have the test produce a factor of the input as a witness to + non-primality. This is only an example, and we ignore the converse + certificate, that for primality, although it, too, can be treated in the + same manner. + + The example we looking at here is an ML function for finding a factor + of a number. We first declare its type: +*} + +consts factor :: "nat \ nat" + +text{* + Its definition will be given in ML below. 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: + assumes "let k = factor n in k \ 1 \ k \ n \ k dvd n" + shows "\ prime n" +using assms 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 "\ prime(4::nat)" + apply(rule factor_non_prime) + apply eval + done + +text{* + Note, hawever, 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 Iabelle (via the inclusion of @{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 \ 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 @{text 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 \ 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 +(*>*) \ No newline at end of file diff -r d94755882e36 -r 94538ddcac9b ProgTutorial/document/root.tex --- a/ProgTutorial/document/root.tex Thu May 27 10:39:07 2010 +0200 +++ b/ProgTutorial/document/root.tex Sat May 29 12:30:02 2010 +0200 @@ -152,7 +152,8 @@ \title{\mbox{}\\[-10ex] \includegraphics[scale=0.5]{tutorial-logo.jpg}\\[3ex] - The Isabelle Programming Tutorial (draft)} + {\huge\bf The Isabelle Cookbook}\\ + \mbox{A Tutorial for Programming on the ML-Level of Isabelle}\\ (draft)} \author{by Christian Urban with contributions from:\\[2ex] \begin{tabular}{r@{\hspace{1.8mm}}l} @@ -162,6 +163,7 @@ Lukas & Bulwahn\\ Jeremy & Dawson\\ Alexander & Krauss\\ + Tobias & Nipkow\\ Christian & Sternagel\\ \end{tabular}} diff -r d94755882e36 -r 94538ddcac9b progtutorial.pdf Binary file progtutorial.pdf has changed