Ziele Untersuchung
mit Columbo Integrität von
Datenbanken Interaktion und
Portierbarkeit Ergonomie der
Schnittstellen

Angebot Produkte Projekt Beratung

Mittel Analytik Modellierung Sprachen Algebra Logik Hardware Denken Kreativität

Zusammenhänge Gesellschaft Wirtschaft Branche Firma

Benutzer


products/Sources/formale Sprachen/Isabelle/HOL/Data_Structures/ (Isabelle Prover Version 2025-1^©) Datei vom 16.11.2025 mit Größe 2 kB

SSL ML.thy

Interaktion und
PortierbarkeitIsabelle

(*  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 ‹term‹1 + 1› (* term as symbolic ML datatype value *)›

ML ‹term‹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 context (Syntax.implode_input s);
›

subsection ‹Recursive ML evaluation›

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 \<Rightarrow> 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 \<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

Messung V0.5 in Prozent

¤ Diese beiden folgenden Angebotsgruppen bietet das Unternehmen0.12Angebot (Wie Sie bei der Firma Beratungs- und Dienstleistungen beauftragen können 2026-06-30) ¤

*Eine klare Vorstellung vom Zielzustand

Wurzel

Suchen

PVS Prover

Isabelle Prover

NIST Cobol Testsuite

Cephes Mathematical Library

Vienna Development Method

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.