14 claimed, it's amongst the hardest intellectual tasks ever attempted.''} \\[1ex] |
13 claimed, it's amongst the hardest intellectual tasks ever attempted.''} \\[1ex] |
15 Richard Bornat, In {\em Defence of Programming}. \cite{Bornat-lecture} |
14 Richard Bornat, In {\em Defence of Programming}. \cite{Bornat-lecture} |
16 \end{flushright} |
15 \end{flushright} |
17 |
16 |
18 \medskip |
17 \medskip |
19 If your next project requires you to program on the ML-level of Isabelle, |
18 If your next project requires you to program Isabelle with ML, |
20 then this tutorial is for you. It will guide you through the first steps of |
19 then this tutorial is for you. It will guide you through the first steps of |
21 Isabelle programming, and also explain ``tricks of the trade''. We also hope |
20 Isabelle programming, and also explain ``tricks of the trade''. We also hope |
22 the tutorial will encourage students and researchers to play with Isabelle |
21 the tutorial will encourage students and researchers to play with Isabelle |
23 and implement new ideas. The source code of Isabelle can look intimidating, |
22 and implement new ideas. The source code of Isabelle can look intimidating, |
24 but beginners can get by with knowledge of only a handful of concepts, |
23 but beginners can get by with knowledge of only a handful of concepts, |
25 a small number of functions and a few basic coding conventions. |
24 a small number of functions and a few basic coding conventions. |
26 There is also a considerable amount of code written in Scala that allows |
25 There is also a considerable amount of code written in Scala that allows |
27 Isabelle interface with the Jedit GUI. Explanation of this part is beyond |
26 Isabelle interface with the Jedit GUI. Explanation of this part is beyond |
28 this tutorial. |
27 this tutorial. |
29 |
28 |
30 The best way to get to know the ML-level of Isabelle is by experimenting |
29 The best way to get to know the Isabelle/ML is by experimenting |
31 with the many code examples included in the tutorial. The code is as far as |
30 with the many code examples included in the tutorial. The code is as far as |
32 possible checked against the Isabelle |
31 possible checked against the Isabelle |
33 distribution.%%\footnote{\input{version.tex}} |
32 distribution.%%\footnote{\input{version.tex}} |
34 If something does not work, then |
33 If something does not work, then |
35 please let us know. It is impossible for us to know every environment, |
34 please let us know. It is impossible for us to know every environment, |
45 This tutorial targets readers who already know how to use Isabelle for |
44 This tutorial targets readers who already know how to use Isabelle for |
46 writing theories and proofs. We also assume that readers are familiar with |
45 writing theories and proofs. We also assume that readers are familiar with |
47 the functional programming language ML, the language in which most of |
46 the functional programming language ML, the language in which most of |
48 Isabelle is implemented. If you are unfamiliar with either of these two |
47 Isabelle is implemented. If you are unfamiliar with either of these two |
49 subjects, then you should first work through the Isabelle/HOL tutorial |
48 subjects, then you should first work through the Isabelle/HOL tutorial |
50 \cite{isa-tutorial} or Paulson's book on ML \cite{paulson-ml2}. Recently, |
49 @{cite "isa-tutorial"} or Paulson's book on ML @{cite "paulson-ml2"}. Recently, |
51 Isabelle has adopted a sizable amount of Scala code for a slick GUI |
50 Isabelle has adopted a sizable amount of Scala code for a slick GUI |
52 based on jEdit. This part of the code is beyond the interest of this |
51 based on jEdit. This part of the code is beyond the interest of this |
53 tutorial, since it mostly does not concern the regular Isabelle |
52 tutorial, since it mostly does not concern the regular Isabelle |
54 developer. |
53 developer. |
|
54 |
|
55 The rich Isabelle infrastructure can be categorized by various aspects @{cite "wenzel-technology"}: |
|
56 |
|
57 @{emph \<open>@{bold \<open>Logic\<close>}\<close>} |
|
58 \begin{description} |
|
59 \item[Isabelle/Pure] is the logical Framework and bootstrap environment. The Pure logic |
|
60 is used to represent rules for Higher-Order Natural Deduction declaratively. This allows |
|
61 the implementation and definition of object logics like HOL using the Pure logic and |
|
62 framework. |
|
63 \item[Isabelle/HOL] is the main library of theories and tools for applications that is used |
|
64 throughout this tutorial. |
|
65 \end{description} |
|
66 |
|
67 @{emph \<open>@{bold\<open>Programming\<close>}\<close>} |
|
68 \begin{description} |
|
69 \item[Isabelle/ML] is the Isabelle tool implementation and extension language. It is based |
|
70 on Poly/ML\footnote{@{url \<open>http://polyml.org\<close>}}. Both Isabelle/Pure and Isabelle/ML emerge |
|
71 from the same bootstrap process: the result is a meta-language for programming the logic |
|
72 that is intertwined with it from a technological viewpoint, but logic and programming |
|
73 remain formally separated. |
|
74 \item[Isabelle/Scala] is the Isabelle system programming language. It connects the logical |
|
75 environment with the outside world. Most notably resulting in the Prover IDE Isabelle/jEdit |
|
76 and the command line tools. |
|
77 \end{description} |
|
78 |
|
79 @{emph \<open>@{bold\<open>Proof\<close>}\<close>} |
|
80 \begin{description} |
|
81 \item[Isabelle/Isar] is the structured proof language of the Isabelle framework. Isar |
|
82 means, Intelligible semi-automated reasoning. |
|
83 \item[Document language] for HTML output and \LaTeX type-setting of proof text. A proof |
|
84 document combines formal and informal text to describe what has been proven to a general |
|
85 audience. |
|
86 \end{description} |
|
87 |
|
88 @{emph \<open>@{bold\<open>IDE\<close>}\<close>} |
|
89 \begin{description} |
|
90 \item[Isabelle/jEdit] is the IDE for proof and tool development. It provides a rich interactive |
|
91 frontend to the Isabelle framework in which logic and proof development, document creation as |
|
92 well as ML programming are seamlessly integrated. |
|
93 \end{description} |
55 \<close> |
94 \<close> |
56 |
95 |
57 section \<open>Existing Documentation\<close> |
96 section \<open>Existing Documentation\<close> |
58 |
97 |
59 text \<open> |
98 text \<open> |
60 The following documentation about Isabelle programming already exists (and is |
99 The following documentation about Isabelle programming already exists (and is |
61 part of the distribution of Isabelle): |
100 part of the distribution of Isabelle): |
62 |
101 |
63 \begin{description} |
102 \begin{description} |
|
103 \item[The Isabelle/Isar Reference Manual] provides a top level view on the Isabelle system, |
|
104 explaining general concepts and specification material (like grammars, |
|
105 examples and so on) about Isabelle, Isar, Pure, HOL and the document language. |
|
106 |
64 \item[The Isabelle/Isar Implementation Manual] describes Isabelle |
107 \item[The Isabelle/Isar Implementation Manual] describes Isabelle |
65 from a high-level perspective, documenting some of the underlying |
108 implementation from a high-level perspective, documenting the major |
66 concepts and interfaces. |
109 underlying concepts and interfaces. |
67 |
110 |
68 \item[The Isabelle Reference Manual] is an older document that used |
111 \item[Isabelle/jEdit] describes the IDE. |
|
112 |
|
113 \item[The Old Introduction to Isabelle] is an older document that used |
69 to be the main reference of Isabelle at a time when all proof scripts |
114 to be the main reference of Isabelle at a time when all proof scripts |
70 were written on the ML-level. Many parts of this manual are outdated |
115 were written with ML. Many parts of this manual are outdated |
71 now, but some parts, particularly the chapters on tactics, are still |
116 now, but some parts, particularly the chapters on tactics, are still |
72 useful. |
117 useful. |
73 |
118 |
74 \item[The Isar Reference Manual] provides specification material (like grammars, |
119 |
75 examples and so on) about Isar and its implementation. |
|
76 \end{description} |
120 \end{description} |
77 |
121 |
78 Then of course there are: |
122 Then of course there are: |
79 |
123 |
80 \begin{description} |
124 \begin{description} |
84 code is uncommented, some parts have very helpful comments---particularly |
128 code is uncommented, some parts have very helpful comments---particularly |
85 the code about theorems and terms. Despite the lack of comments in most |
129 the code about theorems and terms. Despite the lack of comments in most |
86 parts, it is often good to look at code that does similar things as you |
130 parts, it is often good to look at code that does similar things as you |
87 want to do and learn from it. |
131 want to do and learn from it. |
88 This tutorial contains frequently pointers to the |
132 This tutorial contains frequently pointers to the |
89 Isabelle sources. Still, the UNIX command \mbox{\<open>grep -R\<close>} is |
133 Isabelle sources. The best way is to interactively explore the sources |
90 often your best friend while programming with Isabelle.\footnote{Or |
134 within the IDE provided by Isabelle/jEdit. By loading @{ML_file "Pure/ROOT.ML"} |
91 hypersearch if you work with jEdit.} To understand the sources, |
135 into Isabelle/jEdit the sources of Pure are annotated with markup and you can |
|
136 interactively follow the structure. |
|
137 Moreover, the UNIX command \mbox{\<open>grep -R\<close>} or hypersearch within Isabelle/jEdit is |
|
138 often your best friend while programming with Isabelle. To understand the sources, |
92 it is often also necessary to track the change history of a file or |
139 it is often also necessary to track the change history of a file or |
93 files. The Mercurial repository\footnote{\url{http://isabelle.in.tum.de/repos/isabelle/}} |
140 files. The Mercurial repository\footnote{\url{http://isabelle.in.tum.de/repos/isabelle/}} |
94 for Isabelle provides convenient interfaces to query the history of |
141 for Isabelle provides convenient interfaces to query the history of |
95 files and ``change sets''. |
142 files and ``change sets''. |
96 \end{description} |
143 \end{description} |
120 |
167 |
121 Whenever appropriate we also show the response the code |
168 Whenever appropriate we also show the response the code |
122 generates when evaluated. This response is prefixed with a |
169 generates when evaluated. This response is prefixed with a |
123 @{text [quotes] ">"}, like: |
170 @{text [quotes] ">"}, like: |
124 |
171 |
125 @{ML_response [display,gray] "3 + 4" "7"} |
172 @{ML_matchresult [display,gray] "3 + 4" "7"} |
126 |
173 |
127 The user-level commands of Isabelle (i.e., the non-ML code) are written |
174 The user-level commands of Isabelle (i.e., the non-ML code) are written |
128 in \isacommand{bold face} (e.g., \isacommand{lemma}, \isacommand{apply}, |
175 in \isacommand{bold face} (e.g., \isacommand{lemma}, \isacommand{apply}, |
129 \isacommand{foobar} and so on). We use \<open>$ \<dots>\<close> to indicate that a |
176 \isacommand{foobar} and so on). We use \<open>$ \<dots>\<close> to indicate that a |
130 command needs to be run in a UNIX-shell, for example: |
177 command needs to be run in a UNIX-shell, for example: |
153 text \<open> |
200 text \<open> |
154 One of the more difficult aspects of any kind of programming is to |
201 One of the more difficult aspects of any kind of programming is to |
155 understand code written by somebody else. This is aggravated in Isabelle by |
202 understand code written by somebody else. This is aggravated in Isabelle by |
156 the fact that many parts of the code contain none or only few |
203 the fact that many parts of the code contain none or only few |
157 comments. There is one strategy that might be helpful to navigate your way: |
204 comments. There is one strategy that might be helpful to navigate your way: |
158 ML is an interactive programming environment, which means you can evaluate |
205 ML and Isabelle/jEdit is an interactive programming environment, which means you can evaluate |
159 code on the fly (for example inside an \isacommand{ML}~\<open>\<verbopen>\<dots>\<verbclose>\<close> section). So you can copy (self-contained) |
206 code on the fly (for example inside an \isacommand{ML}~\<open>\<verbopen>\<dots>\<verbclose>\<close> section). So you can copy (self-contained) |
160 chunks of existing code into a separate theory file and then study it |
207 chunks of existing code into a separate theory file and then study it |
161 alongside with examples. You can also install ``probes'' inside the copied |
208 alongside with examples. You can also install ``probes'' inside the copied |
162 code without having to recompile the whole Isabelle distribution. Such |
209 code without having to recompile the whole Isabelle distribution. Such |
163 probes might be messages or printouts of variables (see chapter |
210 probes might be messages or printouts of variables (see chapter |
303 |
350 |
304 \item {\bf Rafal Kolanski} contributed to the ``introspection'' of theorems |
351 \item {\bf Rafal Kolanski} contributed to the ``introspection'' of theorems |
305 in section \ref{sec:theorems}. |
352 in section \ref{sec:theorems}. |
306 |
353 |
307 \item {\bf Alexander Krauss} wrote a very early version of the ``first-steps'' |
354 \item {\bf Alexander Krauss} wrote a very early version of the ``first-steps'' |
308 chapter and also contributed the material on @{ML_funct Named_Thms}. |
355 chapter and also contributed the material on @{ML_functor Named_Thms}. |
309 |
356 |
310 %%\item {\bf Tobias Nipkow} contributed recipe \ref{rec:callml}. |
357 %%\item {\bf Tobias Nipkow} contributed recipe \ref{rec:callml}. |
311 |
358 |
312 \item {\bf Michael Norrish} proofread parts of the text. |
359 \item {\bf Michael Norrish} proofread parts of the text. |
|
360 |
|
361 \item {\bf Norbert Schirmer} updated the document to work with Isabelle 2018 and |
|
362 later. |
313 |
363 |
314 \item {\bf Andreas Schropp} improved and corrected section \ref{sec:univ} and |
364 \item {\bf Andreas Schropp} improved and corrected section \ref{sec:univ} and |
315 contributed towards section \ref{sec:sorts}. |
365 contributed towards section \ref{sec:sorts}. |
316 |
366 |
317 \item {\bf Christian Sternagel} proofread the tutorial and made |
367 \item {\bf Christian Sternagel} proofread the tutorial and made |