Quelle ML.thy Sprache: Isabelle

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

section \<open>Isabelle/ML basics\<close>

theory "ML"
  imports Main
begin

subsection \<open>ML expressions\<close>

text \<open>
  The Isabelle command \<^theory_text>\<open>ML\<close> 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.
\<close>

ML \<open>1 + 1\<close>

ML \<open>val a = 1\<close>
ML \<open>val b = 1\<close>
ML \<open>val c = a + b\<close>

subsection \<open>Antiquotations\<close>

text \<open>
  There are some language extensions (via antiquotations), as explained in the
  ``Isabelle/Isar implementation manual'', chapter 0.
\<close>

ML \<open>length []\<close>
ML \<open>\<^assert> (length [] = 0)\<close>

text \<open>Formal entities from the surrounding context may be referenced as
  follows:\<close>

term "1 + 1"   \<comment> \<open>term within theory source\<close>

ML \<open>\<^term>\<open>1 + 1\<close>   (* term as symbolic ML datatype value *)\<close>

ML \<open>\<^term>\<open>1 + (1::int)\<close>\<close>

ML \<open>
  (* formal source with position information *)
  val s = \<open>1 + 1\<close>;

  (* read term via old-style string interface *)
  val t = Syntax.read_term \<^context> (Syntax.implode_input s);
\<close>

subsection \<open>Recursive ML evaluation\<close>

ML \<open>
  ML \<open>ML \<open>val a = @{thm refl}\<close>\<close>;
  ML \<open>val b = @{thm sym}\<close>;
  val c = @{thm trans}
  val thms = [a, b, c];
\<close>

subsection \<open>IDE support\<close>

text \<open>
  ML embedded into the Isabelle environment is connected to the Prover IDE.
  Poly/ML provides:

    \<^item> precise positions for warnings / errors
    \<^item> markup for defining positions of identifiers
    \<^item> markup for inferred types of sub-expressions
    \<^item> pretty-printing of ML values with markup
    \<^item> completion of ML names
    \<^item> source-level debugger
\<close>

ML \<open>fn i => fn list => length list + i\<close>

subsection \<open>Example: factorial and ackermann function in Isabelle/ML\<close>

ML \<open>
  fun factorial 0 = 1
    | factorial n = n * factorial (n - 1)
\<close>

ML \<open>factorial 42\<close>
ML \<open>factorial 10000 div factorial 9999\<close>

text \<open>See \<^url>\<open>http://mathworld.wolfram.com/AckermannFunction.html\<close>.\<close>

ML \<open>
  fun ackermann 0 n = n + 1
    | ackermann m 0 = ackermann (m - 1) 1
    | ackermann m n = ackermann (m - 1) (ackermann m (n - 1))
\<close>

ML \<open>timeit (fn () => ackermann 3 10)\<close>

subsection \<open>Parallel Isabelle/ML\<close>

text \<open>
  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.
\<close>

ML \<open>
  val x = Future.fork (fn () => ackermann 3 10);
  val y = Future.fork (fn () => ackermann 3 10);
  val z = Future.join x + Future.join y
\<close>

text \<open>
  The \<^ML_structure>\<open>Par_List\<close> module provides high-level combinators for
  parallel list operations.
\<close>

ML \<open>timeit (fn () => map (fn n => ackermann 3 n) (1 upto 10))\<close>
ML \<open>timeit (fn () => Par_List.map (fn n => ackermann 3 n) (1 upto 10))\<close>

subsection \<open>Function specifications in Isabelle/HOL\<close>

fun factorial :: "nat \ nat"
where
  "factorial 0 = 1"
| "factorial (Suc n) = Suc n * factorial n"

term "factorial 4"  \<comment> \<open>symbolic term\<close>
value "factorial 4"  \<comment> \<open>evaluation via ML code generation in the background\<close>

declare [[ML_source_trace]]
ML \<open>\<^term>\<open>factorial 4\<close>\<close>  \<comment> \<open>symbolic term in ML\<close>
ML \<open>@{code "factorial"}\<close>  \<comment> \<open>ML code from function specification\<close>

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

quality89%

¤ Dauer der Verarbeitung: 0.13 Sekunden (vorverarbeitet) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.