--- a/ProgTutorial/Recipes/CallML.thy	Sun Dec 15 23:49:05 2013 +0000
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,145 +0,0 @@
-(*<*)
-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
-(*>*)