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