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

--- 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";

--- /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 \<Rightarrow> 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 \<noteq> 1 \<and> k \<noteq> n \<and> k dvd n"
+  shows "\<not> 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 "\<not> 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 \<Rightarrow> 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 \<Rightarrow> 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

--- 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}}
 

Binary file progtutorial.pdf has changed