added Isabelle/ML example;
authorwenzelm
Thu Sep 26 22:34:43 2013 +0200 (2013-09-26)
changeset 5393559c6dbdf0a38
parent 53934 787242dbb49e
child 53936 eed09ad6c5df
added Isabelle/ML example;
src/HOL/ROOT
src/HOL/ex/ML.thy
src/Pure/Tools/doc.scala
     1.1 --- a/src/HOL/ROOT	Thu Sep 26 22:29:29 2013 +0200
     1.2 +++ b/src/HOL/ROOT	Thu Sep 26 22:34:43 2013 +0200
     1.3 @@ -560,6 +560,7 @@
     1.4      IArray_Examples
     1.5      SVC_Oracle
     1.6      Simps_Case_Conv_Examples
     1.7 +    ML
     1.8    theories [skip_proofs = false]
     1.9      Meson_Test
    1.10    theories [condition = SVC_HOME]
     2.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.2 +++ b/src/HOL/ex/ML.thy	Thu Sep 26 22:34:43 2013 +0200
     2.3 @@ -0,0 +1,136 @@
     2.4 +(*  Title:      HOL/ex/ML.thy
     2.5 +    Author:     Makarius
     2.6 +*)
     2.7 +
     2.8 +header {* Isabelle/ML basics *}
     2.9 +
    2.10 +theory "ML"
    2.11 +imports Main
    2.12 +begin
    2.13 +
    2.14 +section {* ML expressions *}
    2.15 +
    2.16 +text {*
    2.17 +  The Isabelle command 'ML' allows to embed Isabelle/ML source into the formal
    2.18 +  text. It is type-checked, compiled, and run within that environment.
    2.19 +
    2.20 +  Note that side-effects should be avoided, unless the intention is to change
    2.21 +  global parameters of the run-time environment (rare).
    2.22 +
    2.23 +  ML top-level bindings are managed within the theory context.
    2.24 +*}
    2.25 +
    2.26 +ML {* 1 + 1 *}
    2.27 +
    2.28 +ML {* val a = 1 *}
    2.29 +ML {* val b = 1 *}
    2.30 +ML {* val c = a + b *}
    2.31 +
    2.32 +
    2.33 +section {* Antiquotations *}
    2.34 +
    2.35 +text {* There are some language extensions (via antiquotations), as explained in
    2.36 +  the "Isabelle/Isar implementation manual", chapter 0. *}
    2.37 +
    2.38 +ML {* length [] *}
    2.39 +ML {* @{assert} (length [] = 0) *}
    2.40 +
    2.41 +
    2.42 +text {* Formal entities from the surrounding context may be referenced as
    2.43 +  follows: *}
    2.44 +
    2.45 +term "1 + 1"   -- "term within theory source"
    2.46 +
    2.47 +ML {*
    2.48 +  @{term "1 + 1"}   (* term as symbolic ML datatype value *)
    2.49 +*}
    2.50 +
    2.51 +ML {*
    2.52 +  @{term "1 + (1::int)"}
    2.53 +*}
    2.54 +
    2.55 +
    2.56 +section {* IDE support *}
    2.57 +
    2.58 +text {*
    2.59 +  ML embedded into the Isabelle environment is connected to the Prover IDE.
    2.60 +  Poly/ML provides:
    2.61 +    \<bullet> precise positions for warnings / errors
    2.62 +    \<bullet> markup for defining positions of identifiers
    2.63 +    \<bullet> markup for inferred types of sub-expressions
    2.64 +*}
    2.65 +
    2.66 +ML {* fn i => fn list => length list + i *}
    2.67 +
    2.68 +
    2.69 +section {* Example: factorial and ackermann function in Isabelle/ML *}
    2.70 +
    2.71 +ML {*
    2.72 +  fun factorial 0 = 1
    2.73 +    | factorial n = n * factorial (n - 1)
    2.74 +*}
    2.75 +
    2.76 +ML "factorial 42"
    2.77 +ML "factorial 10000 div factorial 9999"
    2.78 +
    2.79 +text {*
    2.80 +  See http://mathworld.wolfram.com/AckermannFunction.html
    2.81 +*}
    2.82 +
    2.83 +ML {*
    2.84 +  fun ackermann 0 n = n + 1
    2.85 +    | ackermann m 0 = ackermann (m - 1) 1
    2.86 +    | ackermann m n = ackermann (m - 1) (ackermann m (n - 1))
    2.87 +*}
    2.88 +
    2.89 +ML {* timeit (fn () => ackermann 3 10) *}
    2.90 +
    2.91 +
    2.92 +section {* Parallel Isabelle/ML *}
    2.93 +
    2.94 +text {*
    2.95 +  Future.fork/join/cancel manage parallel evaluation.
    2.96 +
    2.97 +  Note that within Isabelle theory documents, the top-level command boundary may
    2.98 +  not be transgressed without special precautions. This is normally managed by
    2.99 +  the system when performing parallel proof checking. *}
   2.100 +
   2.101 +ML {*
   2.102 +  val x = Future.fork (fn () => ackermann 3 10);
   2.103 +  val y = Future.fork (fn () => ackermann 3 10);
   2.104 +  val z = Future.join x + Future.join y
   2.105 +*}
   2.106 +
   2.107 +text {*
   2.108 +  The @{ML_struct Par_List} module provides high-level combinators for
   2.109 +  parallel list operations. *}
   2.110 +
   2.111 +ML {* timeit (fn () => map (fn n => ackermann 3 n) (1 upto 10)) *}
   2.112 +ML {* timeit (fn () => Par_List.map (fn n => ackermann 3 n) (1 upto 10)) *}
   2.113 +
   2.114 +
   2.115 +section {* Function specifications in Isabelle/HOL *}
   2.116 +
   2.117 +fun factorial :: "nat \<Rightarrow> nat"
   2.118 +where
   2.119 +  "factorial 0 = 1"
   2.120 +| "factorial (Suc n) = Suc n * factorial n"
   2.121 +
   2.122 +term "factorial 4"  -- "symbolic term"
   2.123 +value "factorial 4"  -- "evaluation via ML code generation in the background"
   2.124 +
   2.125 +declare [[ML_trace]]
   2.126 +ML {* @{term "factorial 4"} *}  -- "symbolic term in ML"
   2.127 +ML {* @{code "factorial"} *}  -- "ML code from function specification"
   2.128 +
   2.129 +
   2.130 +fun ackermann :: "nat \<Rightarrow> nat \<Rightarrow> nat"
   2.131 +where
   2.132 +  "ackermann 0 n = n + 1"
   2.133 +| "ackermann (Suc m) 0 = ackermann m 1"
   2.134 +| "ackermann (Suc m) (Suc n) = ackermann m (ackermann (Suc m) n)"
   2.135 +
   2.136 +value "ackermann 3 5"
   2.137 +
   2.138 +end
   2.139 +
     3.1 --- a/src/Pure/Tools/doc.scala	Thu Sep 26 22:29:29 2013 +0200
     3.2 +++ b/src/Pure/Tools/doc.scala	Thu Sep 26 22:34:43 2013 +0200
     3.3 @@ -59,6 +59,7 @@
     3.4      val names =
     3.5        List(
     3.6          "src/HOL/ex/Seq.thy",
     3.7 +        "src/HOL/ex/ML.thy",
     3.8          "src/HOL/Unix/Unix.thy",
     3.9          "src/HOL/Isar_Examples/Drinker.thy")
    3.10      Section("Examples") :: names.map(name => text_file(name).get)