src/HOL/ex/ML.thy
author haftmann
Fri Oct 10 19:55:32 2014 +0200 (2014-10-10)
changeset 58646 cd63a4b12a33
parent 58616 4257a7f2bf39
child 58889 5b7a9633cfa8
permissions -rw-r--r--
specialized specification: avoid trivial instances
wenzelm@53935
     1
(*  Title:      HOL/ex/ML.thy
wenzelm@53935
     2
    Author:     Makarius
wenzelm@53935
     3
*)
wenzelm@53935
     4
wenzelm@58616
     5
header \<open>Isabelle/ML basics\<close>
wenzelm@53935
     6
wenzelm@53935
     7
theory "ML"
wenzelm@53935
     8
imports Main
wenzelm@53935
     9
begin
wenzelm@53935
    10
wenzelm@58616
    11
section \<open>ML expressions\<close>
wenzelm@53935
    12
wenzelm@58616
    13
text \<open>
wenzelm@53935
    14
  The Isabelle command 'ML' allows to embed Isabelle/ML source into the formal
wenzelm@53935
    15
  text. It is type-checked, compiled, and run within that environment.
wenzelm@53935
    16
wenzelm@53935
    17
  Note that side-effects should be avoided, unless the intention is to change
wenzelm@53935
    18
  global parameters of the run-time environment (rare).
wenzelm@53935
    19
wenzelm@53935
    20
  ML top-level bindings are managed within the theory context.
wenzelm@58616
    21
\<close>
wenzelm@53935
    22
wenzelm@58616
    23
ML \<open>1 + 1\<close>
wenzelm@53935
    24
wenzelm@58616
    25
ML \<open>val a = 1\<close>
wenzelm@58616
    26
ML \<open>val b = 1\<close>
wenzelm@58616
    27
ML \<open>val c = a + b\<close>
wenzelm@53935
    28
wenzelm@53935
    29
wenzelm@58616
    30
section \<open>Antiquotations\<close>
wenzelm@53935
    31
wenzelm@58616
    32
text \<open>There are some language extensions (via antiquotations), as explained in
wenzelm@58616
    33
  the ``Isabelle/Isar implementation manual'', chapter 0.\<close>
wenzelm@53935
    34
wenzelm@58616
    35
ML \<open>length []\<close>
wenzelm@58616
    36
ML \<open>@{assert} (length [] = 0)\<close>
wenzelm@53935
    37
wenzelm@53935
    38
wenzelm@58616
    39
text \<open>Formal entities from the surrounding context may be referenced as
wenzelm@58616
    40
  follows:\<close>
wenzelm@58616
    41
wenzelm@58616
    42
term "1 + 1"   -- \<open>term within theory source\<close>
wenzelm@58616
    43
wenzelm@58616
    44
ML \<open>@{term "1 + 1"}   (* term as symbolic ML datatype value *)\<close>
wenzelm@53935
    45
wenzelm@58616
    46
ML \<open>@{term "1 + (1::int)"}\<close>
wenzelm@58616
    47
wenzelm@58616
    48
wenzelm@58616
    49
section \<open>IDE support\<close>
wenzelm@58616
    50
wenzelm@58616
    51
text \<open>
wenzelm@53935
    52
  ML embedded into the Isabelle environment is connected to the Prover IDE.
wenzelm@53935
    53
  Poly/ML provides:
wenzelm@53948
    54
  \begin{itemize}
wenzelm@53948
    55
    \item precise positions for warnings / errors
wenzelm@53948
    56
    \item markup for defining positions of identifiers
wenzelm@53948
    57
    \item markup for inferred types of sub-expressions
wenzelm@53948
    58
  \end{itemize}
wenzelm@58616
    59
\<close>
wenzelm@53935
    60
wenzelm@58616
    61
ML \<open>fn i => fn list => length list + i\<close>
wenzelm@53935
    62
wenzelm@53935
    63
wenzelm@58616
    64
section \<open>Example: factorial and ackermann function in Isabelle/ML\<close>
wenzelm@53935
    65
wenzelm@58616
    66
ML \<open>
wenzelm@53935
    67
  fun factorial 0 = 1
wenzelm@53935
    68
    | factorial n = n * factorial (n - 1)
wenzelm@58616
    69
\<close>
wenzelm@53935
    70
wenzelm@58616
    71
ML \<open>factorial 42\<close>
wenzelm@58616
    72
ML \<open>factorial 10000 div factorial 9999\<close>
wenzelm@53935
    73
wenzelm@58616
    74
text \<open>See @{url "http://mathworld.wolfram.com/AckermannFunction.html"}\<close>
wenzelm@58616
    75
wenzelm@58616
    76
ML \<open>
wenzelm@53935
    77
  fun ackermann 0 n = n + 1
wenzelm@53935
    78
    | ackermann m 0 = ackermann (m - 1) 1
wenzelm@53935
    79
    | ackermann m n = ackermann (m - 1) (ackermann m (n - 1))
wenzelm@58616
    80
\<close>
wenzelm@53935
    81
wenzelm@58616
    82
ML \<open>timeit (fn () => ackermann 3 10)\<close>
wenzelm@53935
    83
wenzelm@53935
    84
wenzelm@58616
    85
section \<open>Parallel Isabelle/ML\<close>
wenzelm@53935
    86
wenzelm@58616
    87
text \<open>
wenzelm@53935
    88
  Future.fork/join/cancel manage parallel evaluation.
wenzelm@53935
    89
wenzelm@53935
    90
  Note that within Isabelle theory documents, the top-level command boundary may
wenzelm@53935
    91
  not be transgressed without special precautions. This is normally managed by
wenzelm@58616
    92
  the system when performing parallel proof checking.\<close>
wenzelm@53935
    93
wenzelm@58616
    94
ML \<open>
wenzelm@53935
    95
  val x = Future.fork (fn () => ackermann 3 10);
wenzelm@53935
    96
  val y = Future.fork (fn () => ackermann 3 10);
wenzelm@53935
    97
  val z = Future.join x + Future.join y
wenzelm@58616
    98
\<close>
wenzelm@53935
    99
wenzelm@58616
   100
text \<open>The @{ML_structure Par_List} module provides high-level combinators
wenzelm@58616
   101
  for parallel list operations.\<close>
wenzelm@53935
   102
wenzelm@58616
   103
ML \<open>timeit (fn () => map (fn n => ackermann 3 n) (1 upto 10))\<close>
wenzelm@58616
   104
ML \<open>timeit (fn () => Par_List.map (fn n => ackermann 3 n) (1 upto 10))\<close>
wenzelm@53935
   105
wenzelm@53935
   106
wenzelm@58616
   107
section \<open>Function specifications in Isabelle/HOL\<close>
wenzelm@53935
   108
wenzelm@53935
   109
fun factorial :: "nat \<Rightarrow> nat"
wenzelm@53935
   110
where
wenzelm@53935
   111
  "factorial 0 = 1"
wenzelm@53935
   112
| "factorial (Suc n) = Suc n * factorial n"
wenzelm@53935
   113
wenzelm@58616
   114
term "factorial 4"  -- \<open>symbolic term\<close>
wenzelm@58616
   115
value "factorial 4"  -- \<open>evaluation via ML code generation in the background\<close>
wenzelm@53935
   116
wenzelm@56279
   117
declare [[ML_source_trace]]
wenzelm@58616
   118
ML \<open>@{term "factorial 4"}\<close>  -- \<open>symbolic term in ML\<close>
wenzelm@58616
   119
ML \<open>@{code "factorial"}\<close>  -- \<open>ML code from function specification\<close>
wenzelm@53935
   120
wenzelm@53935
   121
wenzelm@53935
   122
fun ackermann :: "nat \<Rightarrow> nat \<Rightarrow> nat"
wenzelm@53935
   123
where
wenzelm@53935
   124
  "ackermann 0 n = n + 1"
wenzelm@53935
   125
| "ackermann (Suc m) 0 = ackermann m 1"
wenzelm@53935
   126
| "ackermann (Suc m) (Suc n) = ackermann m (ackermann (Suc m) n)"
wenzelm@53935
   127
wenzelm@53935
   128
value "ackermann 3 5"
wenzelm@53935
   129
wenzelm@53935
   130
end
wenzelm@53935
   131