equal
deleted
inserted
replaced
6 |
6 |
7 theory "ML" |
7 theory "ML" |
8 imports Main |
8 imports Main |
9 begin |
9 begin |
10 |
10 |
11 section \<open>ML expressions\<close> |
11 subsection \<open>ML expressions\<close> |
12 |
12 |
13 text \<open> |
13 text \<open> |
14 The Isabelle command \<^theory_text>\<open>ML\<close> allows to embed Isabelle/ML source into the |
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. |
15 formal text. It is type-checked, compiled, and run within that environment. |
16 |
16 |
25 ML \<open>val a = 1\<close> |
25 ML \<open>val a = 1\<close> |
26 ML \<open>val b = 1\<close> |
26 ML \<open>val b = 1\<close> |
27 ML \<open>val c = a + b\<close> |
27 ML \<open>val c = a + b\<close> |
28 |
28 |
29 |
29 |
30 section \<open>Antiquotations\<close> |
30 subsection \<open>Antiquotations\<close> |
31 |
31 |
32 text \<open> |
32 text \<open> |
33 There are some language extensions (via antiquotations), as explained in the |
33 There are some language extensions (via antiquotations), as explained in the |
34 ``Isabelle/Isar implementation manual'', chapter 0. |
34 ``Isabelle/Isar implementation manual'', chapter 0. |
35 \<close> |
35 \<close> |
55 (* read term via old-style string interface *) |
55 (* read term via old-style string interface *) |
56 val t = Syntax.read_term \<^context> (Syntax.implode_input s); |
56 val t = Syntax.read_term \<^context> (Syntax.implode_input s); |
57 \<close> |
57 \<close> |
58 |
58 |
59 |
59 |
60 section \<open>Recursive ML evaluation\<close> |
60 subsection \<open>Recursive ML evaluation\<close> |
61 |
61 |
62 ML \<open> |
62 ML \<open> |
63 ML \<open>ML \<open>val a = @{thm refl}\<close>\<close>; |
63 ML \<open>ML \<open>val a = @{thm refl}\<close>\<close>; |
64 ML \<open>val b = @{thm sym}\<close>; |
64 ML \<open>val b = @{thm sym}\<close>; |
65 val c = @{thm trans} |
65 val c = @{thm trans} |
66 val thms = [a, b, c]; |
66 val thms = [a, b, c]; |
67 \<close> |
67 \<close> |
68 |
68 |
69 |
69 |
70 section \<open>IDE support\<close> |
70 subsection \<open>IDE support\<close> |
71 |
71 |
72 text \<open> |
72 text \<open> |
73 ML embedded into the Isabelle environment is connected to the Prover IDE. |
73 ML embedded into the Isabelle environment is connected to the Prover IDE. |
74 Poly/ML provides: |
74 Poly/ML provides: |
75 |
75 |
82 \<close> |
82 \<close> |
83 |
83 |
84 ML \<open>fn i => fn list => length list + i\<close> |
84 ML \<open>fn i => fn list => length list + i\<close> |
85 |
85 |
86 |
86 |
87 section \<open>Example: factorial and ackermann function in Isabelle/ML\<close> |
87 subsection \<open>Example: factorial and ackermann function in Isabelle/ML\<close> |
88 |
88 |
89 ML \<open> |
89 ML \<open> |
90 fun factorial 0 = 1 |
90 fun factorial 0 = 1 |
91 | factorial n = n * factorial (n - 1) |
91 | factorial n = n * factorial (n - 1) |
92 \<close> |
92 \<close> |
103 \<close> |
103 \<close> |
104 |
104 |
105 ML \<open>timeit (fn () => ackermann 3 10)\<close> |
105 ML \<open>timeit (fn () => ackermann 3 10)\<close> |
106 |
106 |
107 |
107 |
108 section \<open>Parallel Isabelle/ML\<close> |
108 subsection \<open>Parallel Isabelle/ML\<close> |
109 |
109 |
110 text \<open> |
110 text \<open> |
111 Future.fork/join/cancel manage parallel evaluation. |
111 Future.fork/join/cancel manage parallel evaluation. |
112 |
112 |
113 Note that within Isabelle theory documents, the top-level command boundary |
113 Note that within Isabelle theory documents, the top-level command boundary |
128 |
128 |
129 ML \<open>timeit (fn () => map (fn n => ackermann 3 n) (1 upto 10))\<close> |
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> |
130 ML \<open>timeit (fn () => Par_List.map (fn n => ackermann 3 n) (1 upto 10))\<close> |
131 |
131 |
132 |
132 |
133 section \<open>Function specifications in Isabelle/HOL\<close> |
133 subsection \<open>Function specifications in Isabelle/HOL\<close> |
134 |
134 |
135 fun factorial :: "nat \<Rightarrow> nat" |
135 fun factorial :: "nat \<Rightarrow> nat" |
136 where |
136 where |
137 "factorial 0 = 1" |
137 "factorial 0 = 1" |
138 | "factorial (Suc n) = Suc n * factorial n" |
138 | "factorial (Suc n) = Suc n * factorial n" |