--- a/src/HOL/ROOT Thu Sep 26 22:29:29 2013 +0200
+++ b/src/HOL/ROOT Thu Sep 26 22:34:43 2013 +0200
@@ -560,6 +560,7 @@
IArray_Examples
SVC_Oracle
Simps_Case_Conv_Examples
+ ML
theories [skip_proofs = false]
Meson_Test
theories [condition = SVC_HOME]
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/ex/ML.thy Thu Sep 26 22:34:43 2013 +0200
@@ -0,0 +1,136 @@
+(* Title: HOL/ex/ML.thy
+ Author: Makarius
+*)
+
+header {* Isabelle/ML basics *}
+
+theory "ML"
+imports Main
+begin
+
+section {* ML expressions *}
+
+text {*
+ The Isabelle command 'ML' allows to embed Isabelle/ML source into the formal
+ text. It is type-checked, compiled, and run within that environment.
+
+ Note that side-effects should be avoided, unless the intention is to change
+ global parameters of the run-time environment (rare).
+
+ ML top-level bindings are managed within the theory context.
+*}
+
+ML {* 1 + 1 *}
+
+ML {* val a = 1 *}
+ML {* val b = 1 *}
+ML {* val c = a + b *}
+
+
+section {* Antiquotations *}
+
+text {* There are some language extensions (via antiquotations), as explained in
+ the "Isabelle/Isar implementation manual", chapter 0. *}
+
+ML {* length [] *}
+ML {* @{assert} (length [] = 0) *}
+
+
+text {* Formal entities from the surrounding context may be referenced as
+ follows: *}
+
+term "1 + 1" -- "term within theory source"
+
+ML {*
+ @{term "1 + 1"} (* term as symbolic ML datatype value *)
+*}
+
+ML {*
+ @{term "1 + (1::int)"}
+*}
+
+
+section {* IDE support *}
+
+text {*
+ ML embedded into the Isabelle environment is connected to the Prover IDE.
+ Poly/ML provides:
+ \<bullet> precise positions for warnings / errors
+ \<bullet> markup for defining positions of identifiers
+ \<bullet> markup for inferred types of sub-expressions
+*}
+
+ML {* fn i => fn list => length list + i *}
+
+
+section {* Example: factorial and ackermann function in Isabelle/ML *}
+
+ML {*
+ fun factorial 0 = 1
+ | factorial n = n * factorial (n - 1)
+*}
+
+ML "factorial 42"
+ML "factorial 10000 div factorial 9999"
+
+text {*
+ See http://mathworld.wolfram.com/AckermannFunction.html
+*}
+
+ML {*
+ fun ackermann 0 n = n + 1
+ | ackermann m 0 = ackermann (m - 1) 1
+ | ackermann m n = ackermann (m - 1) (ackermann m (n - 1))
+*}
+
+ML {* timeit (fn () => ackermann 3 10) *}
+
+
+section {* Parallel Isabelle/ML *}
+
+text {*
+ Future.fork/join/cancel manage parallel evaluation.
+
+ Note that within Isabelle theory documents, the top-level command boundary may
+ not be transgressed without special precautions. This is normally managed by
+ the system when performing parallel proof checking. *}
+
+ML {*
+ val x = Future.fork (fn () => ackermann 3 10);
+ val y = Future.fork (fn () => ackermann 3 10);
+ val z = Future.join x + Future.join y
+*}
+
+text {*
+ The @{ML_struct Par_List} module provides high-level combinators for
+ parallel list operations. *}
+
+ML {* timeit (fn () => map (fn n => ackermann 3 n) (1 upto 10)) *}
+ML {* timeit (fn () => Par_List.map (fn n => ackermann 3 n) (1 upto 10)) *}
+
+
+section {* Function specifications in Isabelle/HOL *}
+
+fun factorial :: "nat \<Rightarrow> nat"
+where
+ "factorial 0 = 1"
+| "factorial (Suc n) = Suc n * factorial n"
+
+term "factorial 4" -- "symbolic term"
+value "factorial 4" -- "evaluation via ML code generation in the background"
+
+declare [[ML_trace]]
+ML {* @{term "factorial 4"} *} -- "symbolic term in ML"
+ML {* @{code "factorial"} *} -- "ML code from function specification"
+
+
+fun ackermann :: "nat \<Rightarrow> nat \<Rightarrow> nat"
+where
+ "ackermann 0 n = n + 1"
+| "ackermann (Suc m) 0 = ackermann m 1"
+| "ackermann (Suc m) (Suc n) = ackermann m (ackermann (Suc m) n)"
+
+value "ackermann 3 5"
+
+end
+
--- a/src/Pure/Tools/doc.scala Thu Sep 26 22:29:29 2013 +0200
+++ b/src/Pure/Tools/doc.scala Thu Sep 26 22:34:43 2013 +0200
@@ -59,6 +59,7 @@
val names =
List(
"src/HOL/ex/Seq.thy",
+ "src/HOL/ex/ML.thy",
"src/HOL/Unix/Unix.thy",
"src/HOL/Isar_Examples/Drinker.thy")
Section("Examples") :: names.map(name => text_file(name).get)