4 begin |
4 begin |
5 |
5 |
6 chapter {* Introduction *} |
6 chapter {* Introduction *} |
7 |
7 |
8 text {* |
8 text {* |
9 The purpose of this document is to guide the reader through the |
9 The purpose of this cookbook is to guide the reader through the |
10 first steps in Isabelle programming, and to provide recipes for |
10 first steps in Isabelle programming, and to provide recipes for |
11 solving common problems. |
11 solving common problems. |
12 *} |
12 *} |
13 |
13 |
14 section {* Intended Audience and Prior Knowledge *} |
14 section {* Intended Audience and Prior Knowledge *} |
15 |
15 |
16 text {* |
16 text {* |
17 This cookbook targets an audience who already knows how to use the Isabelle |
17 This cookbook targets an audience who already knows how to use Isabelle |
18 system to write theories and proofs, but without using ML. |
18 for writing theories and proofs. It is also assumed that the reader is |
19 You should also be familiar with the \emph{Standard ML} programming |
19 familiar with the \emph{Standard ML} programming language, in which |
20 language, which is used for Isabelle programming. If you are unfamiliar with any of |
20 most of Isabelle is implemented. If you are unfamiliar with any of |
21 these two subjects, you should first work through the Isabelle/HOL |
21 these two subjects, you should first work through the Isabelle/HOL |
22 tutorial \cite{isa-tutorial} and Paulson's book on Standard ML |
22 tutorial \cite{isa-tutorial} and Paulson's book on Standard ML |
23 \cite{paulson-ml2}. |
23 \cite{paulson-ml2}. |
24 |
24 |
25 *} |
25 *} |
26 |
26 |
27 section {* Primary Documentation *} |
27 section {* Existing Documentation *} |
28 |
28 |
29 text {* |
29 text {* |
30 |
30 |
|
31 The following documents about ML-coding for Isabelle already exist (they are |
|
32 included in the Isabelle distribution): |
31 |
33 |
32 \begin{description} |
34 \begin{description} |
33 \item[The Implementation Manual \cite{isa-imp}] describes Isabelle |
35 \item[The Implementation Manual] describes Isabelle |
34 from a programmer's perspective, documenting both the underlying |
36 from a programmer's perspective, documenting both the underlying |
35 concepts and the concrete interfaces. |
37 concepts and the concrete interfaces. |
36 |
38 |
37 \item[The Isabelle Reference Manual \cite{isabelle-ref}] is an older document that used |
39 \item[The Isabelle Reference Manual] is an older document that used |
38 to be the main reference, when all reasoning happened on the ML |
40 to be the main reference, when all reasoning happened on the ML |
39 level. Many parts of it are outdated now, but some parts, mainly the |
41 level. Many parts of it are outdated now, but some parts, mainly the |
40 chapters on tactics, are still useful. |
42 chapters on tactics, are still useful. |
|
43 \end{description} |
41 |
44 |
|
45 Then of ourse there is: |
|
46 |
|
47 \begin{description} |
42 \item[The code] is of course the ultimate reference for how |
48 \item[The code] is of course the ultimate reference for how |
43 things really work. Therefore you should not hesitate to look at the |
49 things really work. Therefore you should not hesitate to look at the |
44 way things are actually implemented. More importantly, it is often |
50 way things are actually implemented. More importantly, it is often |
45 good to look at code that does similar things as you want to do, to |
51 good to look at code that does similar things as you want to do, to |
46 learn from other people's code. |
52 learn from other people's code. |
47 \end{description} |
53 \end{description} |
48 |
54 |
49 Since Isabelle is not a finished product, these manuals, just like |
55 Since Isabelle is not a finished product, these manuals, just like |
50 the implementation itself, are always under construction. This can |
56 the implementation itself, are always under construction. This can |
51 be dificult and frustrating at times, when interfaces are changing |
57 be difficult and frustrating at times, especially when interfaces changes |
52 frequently. But it is a reality that progress means changing |
58 occur frequently. But it is a reality that progress means changing |
53 things (FIXME: need some short and convincing comment that this |
59 things (FIXME: need some short and convincing comment that this |
54 is a strategy, not a problem that should be solved). |
60 is a strategy, not a problem that should be solved). |
55 *} |
61 *} |
56 |
62 |
57 |
63 |