--- a/ProgTutorial/Advanced.thy Mon Dec 31 20:20:55 2012 +0000
+++ b/ProgTutorial/Advanced.thy Mon Feb 25 00:33:48 2013 +0000
@@ -699,7 +699,6 @@
text {*
@{ML_ind prove_future in Goal}
@{ML_ind future_result in Goal}
- @{ML_ind fork_pri in Future}
*}
section {* Parse and Print Translations (TBD) *}
--- a/ProgTutorial/Intro.thy Mon Dec 31 20:20:55 2012 +0000
+++ b/ProgTutorial/Intro.thy Mon Feb 25 00:33:48 2013 +0000
@@ -296,6 +296,8 @@
\item {\bf Jeremy Dawson} wrote the first version of chapter \ref{chp:parsing}
about parsing.
+ \item {\bf Florian Haftmann} helped with maintaining recipe \ref{rec:callml}.
+
\item {\bf Armin Heller} helped with recipe \ref{rec:sat}.
\item {\bf Rafal Kolanski} contributed to the ``introspection'' of theorems
--- a/ProgTutorial/Package/Ind_Interface.thy Mon Dec 31 20:20:55 2012 +0000
+++ b/ProgTutorial/Package/Ind_Interface.thy Mon Feb 25 00:33:48 2013 +0000
@@ -161,7 +161,7 @@
@{text "add_inductive_cmd"} is a call to @{ML read_spec in Specification}.
*}
-ML_val{*fun add_inductive_cmd pred_specs rule_specs lthy =
+ML_val%grayML{*fun add_inductive_cmd pred_specs rule_specs lthy =
let
val ((pred_specs', rule_specs'), _) =
Specification.read_spec pred_specs rule_specs lthy
--- a/ProgTutorial/Recipes/CallML.thy Mon Dec 31 20:20:55 2012 +0000
+++ b/ProgTutorial/Recipes/CallML.thy Mon Feb 25 00:33:48 2013 +0000
@@ -1,7 +1,7 @@
(*<*)
theory CallML
imports "~~/src/HOL/Number_Theory/Primes"
- "~~/src/HOL/Library/Efficient_Nat"
+ "~~/src/HOL/Library/Code_Target_Numeral"
begin
(*>*)
@@ -53,12 +53,12 @@
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
+ 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/Efficient_Nat"}\\
+ \isacommand{imports}~@{text Main} @{text [quotes] "~~/src/HOL/Library/Code_Target_Numeral"}\\
...
\end{graybox}
@@ -68,7 +68,16 @@
to connect the two levels:
*}
-code_const factor (SML "factor")
+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}
@@ -100,7 +109,7 @@
The above example was easy because we forced Isabelle (via the inclusion of the
theory @{theory
- Efficient_Nat}) to implement @{typ nat} by @{text int}, a predefined
+ 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:
@@ -108,9 +117,17 @@
consts factor2 :: "nat \<Rightarrow> nat list" (*<*)(*>*)
ML %grayML{*fun factor2 n = if n = 4 then [2] else []*}(*<*)(*>*)
-code_const factor2 (SML "factor2")
+
+definition factor2_integer :: "integer \<Rightarrow> integer list"
+where
+ [code del]: "factor2_integer = map integer_of_nat \<circ> factor2 \<circ> nat_of_integer"
-value "factor2 4"
+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
@@ -120,51 +137,9 @@
@{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.
-
- 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 %grayML{*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"
+value "factor2 4"
end
(*>*)
--- a/ROOT Mon Dec 31 20:20:55 2012 +0000
+++ b/ROOT Mon Feb 25 00:33:48 2013 +0000
@@ -3,7 +3,8 @@
"Base"
"Package/Simple_Inductive_Package"
"~~/src/HOL/Number_Theory/Primes"
- "~~/src/HOL/Library/Efficient_Nat"
+ "~~/src/HOL/Library/Code_Target_Numeral"
+ "~~/src/HOL/Library/Code_Abstract_Nat"
"Helper/Command/Command"
theories [quick_and_dirty, document = false]
"Intro"
@@ -35,7 +36,8 @@
"Base"
"Package/Simple_Inductive_Package"
"~~/src/HOL/Number_Theory/Primes"
- "~~/src/HOL/Library/Efficient_Nat"
+ "~~/src/HOL/Library/Code_Target_Numeral"
+ "~~/src/HOL/Library/Code_Abstract_Nat"
"Helper/Command/Command"
theories [quick_and_dirty, document = true]
"Intro"
Binary file progtutorial.pdf has changed