src/HOL/ex/ML.thy
author wenzelm
Wed Jun 22 10:09:20 2016 +0200 (2016-06-22)
changeset 63343 fb5d8a50c641
parent 62910 f37878ebba65
child 63680 6e1e8b5abbfa
permissions -rw-r--r--
bundle lifting_syntax;
     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 \<^theory_text>\<open>ML\<close> allows to embed Isabelle/ML source into the
    15   formal 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>
    33   There are some language extensions (via antiquotations), as explained in the
    34   ``Isabelle/Isar implementation manual'', chapter 0.
    35 \<close>
    36 
    37 ML \<open>length []\<close>
    38 ML \<open>@{assert} (length [] = 0)\<close>
    39 
    40 
    41 text \<open>Formal entities from the surrounding context may be referenced as
    42   follows:\<close>
    43 
    44 term "1 + 1"   \<comment> \<open>term within theory source\<close>
    45 
    46 ML \<open>@{term "1 + 1"}   (* term as symbolic ML datatype value *)\<close>
    47 
    48 ML \<open>@{term "1 + (1::int)"}\<close>
    49 
    50 
    51 ML \<open>
    52   (* formal source with position information *)
    53   val s = \<open>1 + 1\<close>;
    54 
    55   (* read term via old-style string interface *)
    56   val t = Syntax.read_term @{context} (Syntax.implode_input s);
    57 \<close>
    58 
    59 
    60 section \<open>Recursive ML evaluation\<close>
    61 
    62 ML \<open>
    63   ML \<open>ML \<open>val a = @{thm refl}\<close>\<close>;
    64   ML \<open>val b = @{thm sym}\<close>;
    65   val c = @{thm trans}
    66   val thms = [a, b, c];
    67 \<close>
    68 
    69 
    70 section \<open>IDE support\<close>
    71 
    72 text \<open>
    73   ML embedded into the Isabelle environment is connected to the Prover IDE.
    74   Poly/ML provides:
    75 
    76     \<^item> precise positions for warnings / errors
    77     \<^item> markup for defining positions of identifiers
    78     \<^item> markup for inferred types of sub-expressions
    79     \<^item> pretty-printing of ML values with markup
    80     \<^item> completion of ML names
    81     \<^item> source-level debugger
    82 \<close>
    83 
    84 ML \<open>fn i => fn list => length list + i\<close>
    85 
    86 
    87 section \<open>Example: factorial and ackermann function in Isabelle/ML\<close>
    88 
    89 ML \<open>
    90   fun factorial 0 = 1
    91     | factorial n = n * factorial (n - 1)
    92 \<close>
    93 
    94 ML \<open>factorial 42\<close>
    95 ML \<open>factorial 10000 div factorial 9999\<close>
    96 
    97 text \<open>See @{url "http://mathworld.wolfram.com/AckermannFunction.html"}\<close>
    98 
    99 ML \<open>
   100   fun ackermann 0 n = n + 1
   101     | ackermann m 0 = ackermann (m - 1) 1
   102     | ackermann m n = ackermann (m - 1) (ackermann m (n - 1))
   103 \<close>
   104 
   105 ML \<open>timeit (fn () => ackermann 3 10)\<close>
   106 
   107 
   108 section \<open>Parallel Isabelle/ML\<close>
   109 
   110 text \<open>
   111   Future.fork/join/cancel manage parallel evaluation.
   112 
   113   Note that within Isabelle theory documents, the top-level command boundary
   114   may not be transgressed without special precautions. This is normally
   115   managed by the system when performing parallel proof checking.
   116 \<close>
   117 
   118 ML \<open>
   119   val x = Future.fork (fn () => ackermann 3 10);
   120   val y = Future.fork (fn () => ackermann 3 10);
   121   val z = Future.join x + Future.join y
   122 \<close>
   123 
   124 text \<open>
   125   The @{ML_structure Par_List} module provides high-level combinators for
   126   parallel list operations.
   127 \<close>
   128 
   129 ML \<open>timeit (fn () => map (fn n => ackermann 3 n) (1 upto 10))\<close>
   130 ML \<open>timeit (fn () => Par_List.map (fn n => ackermann 3 n) (1 upto 10))\<close>
   131 
   132 
   133 section \<open>Function specifications in Isabelle/HOL\<close>
   134 
   135 fun factorial :: "nat \<Rightarrow> nat"
   136 where
   137   "factorial 0 = 1"
   138 | "factorial (Suc n) = Suc n * factorial n"
   139 
   140 term "factorial 4"  \<comment> \<open>symbolic term\<close>
   141 value "factorial 4"  \<comment> \<open>evaluation via ML code generation in the background\<close>
   142 
   143 declare [[ML_source_trace]]
   144 ML \<open>@{term "factorial 4"}\<close>  \<comment> \<open>symbolic term in ML\<close>
   145 ML \<open>@{code "factorial"}\<close>  \<comment> \<open>ML code from function specification\<close>
   146 
   147 
   148 fun ackermann :: "nat \<Rightarrow> nat \<Rightarrow> nat"
   149 where
   150   "ackermann 0 n = n + 1"
   151 | "ackermann (Suc m) 0 = ackermann m 1"
   152 | "ackermann (Suc m) (Suc n) = ackermann m (ackermann (Suc m) n)"
   153 
   154 value "ackermann 3 5"
   155 
   156 end
   157