Quelle  ML.thy

(*  Title:      HOL/Examples/ML.thy
  Author: Makarius
*)

section ‹Isabelle/ML basics›

theory "ML"
  imports Main
begin

subsection ‹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›


subsection ‹Antiquotations›

text ‹
  There are some language extensions (via antiquotations), as explained in the
  ``Isabelle/Isar implementation manual'', chapter 0.
 ›

ML ‹length []›
ML ‹🍋 (length [] = 0)›


text ‹Formal entities from the surrounding context may be referenced as
  follows:›

term "1 + 1"   🍋 ‹term within theory source›

ML ‹🍋‹1 + 1› (* term as symbolic ML datatype value *)›

ML ‹🍋‹1 + (1::int)›\›


ML ‹
  (* formal source with position information *)
  val s = ‹1 + 1›;

  (* read term via old-style string interface *)
  val t = Syntax.read_term 🍋 (Syntax.implode_input s);
›


subsection ‹Recursive ML evaluation›

ML ‹
  ML ‹ML ‹val a = @{thm refl}›\   ML ‹val b = @{thm sym}›;
  val c = @{thm trans}
  val thms = [a, b, c];
›


subsection ‹IDE support›

text ‹
  ML embedded into the Isabelle environment is connected to the Prover IDE.
  Poly/ML provides:
 
  🪙 precise positions for warnings / errors
  🪙 markup for defining positions of identifiers
  🪙 markup for inferred types of sub-expressions
  🪙 pretty-printing of ML values with markup
  🪙 completion of ML names
  🪙 source-level debugger
 ›

ML ‹fn i => fn list => length list + i›


subsection ‹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›.\<close>

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


subsection ‹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 🪙‹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))›


subsection ‹Function specifications in Isabelle/HOL›

fun factorial :: "nat ==> 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_source_trace]]
ML ‹🍋‹factorial 4›\›  🍋 ‹symbolic term in ML›
ML ‹@{code "factorial"}›  🍋 ‹ML code from function specification›


fun ackermann :: "nat ==> nat ==> 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