5 |
5 |
6 |
6 |
7 chapter {* Introduction *} |
7 chapter {* Introduction *} |
8 |
8 |
9 text {* |
9 text {* |
10 The purpose of this Cookbook is to guide the reader through the first steps |
10 If your next project requires you to program on the ML-level of Isabelle, |
11 of Isabelle programming, and to explain tricks of the trade. The code |
11 then this Cookbook is for you. It will guide you through the first steps of |
12 provided in the Cookbook is as far as possible checked against recent |
12 Isabelle programming, and also explain tricks of the trade. The best way to |
13 versions of Isabelle. If something does not work, then please let us |
13 get to know the ML-level of Isabelle is by experimenting with the many code |
14 know. If you have comments, criticism or like to add to the Cookbook, |
14 examples included in the Cookbook. The code is as far as possible checked |
15 feel free---you are most welcome! |
15 against recent versions of Isabelle. If something does not work, then |
|
16 please let us know. If you have comments, criticism or like to add to the |
|
17 Cookbook, feel free---you are most welcome! |
16 *} |
18 *} |
17 |
19 |
18 section {* Intended Audience and Prior Knowledge *} |
20 section {* Intended Audience and Prior Knowledge *} |
19 |
21 |
20 text {* |
22 text {* |
39 from a high-level perspective, documenting both the underlying |
41 from a high-level perspective, documenting both the underlying |
40 concepts and some of the interfaces. |
42 concepts and some of the interfaces. |
41 |
43 |
42 \item[The Isabelle Reference Manual] is an older document that used |
44 \item[The Isabelle Reference Manual] is an older document that used |
43 to be the main reference of Isabelle at a time when all proof scripts |
45 to be the main reference of Isabelle at a time when all proof scripts |
44 were written on the ML level. Many parts of this manual are outdated |
46 were written on the ML-level. Many parts of this manual are outdated |
45 now, but some parts, particularly the chapters on tactics, are still |
47 now, but some parts, particularly the chapters on tactics, are still |
46 useful. |
48 useful. |
47 |
49 |
48 \item[The Isar Reference Manual] is also an older document that provides |
50 \item[The Isar Reference Manual] is also an older document that provides |
49 material about Isar and its implementation. Some material in it |
51 material about Isar and its implementation. Some material in it |
54 |
56 |
55 \begin{description} |
57 \begin{description} |
56 \item[The code] is of course the ultimate reference for how |
58 \item[The code] is of course the ultimate reference for how |
57 things really work. Therefore you should not hesitate to look at the |
59 things really work. Therefore you should not hesitate to look at the |
58 way things are actually implemented. More importantly, it is often |
60 way things are actually implemented. More importantly, it is often |
59 good to look at code that does similar things as you want to do, to |
61 good to look at code that does similar things as you want to do and |
60 learn from other people's code. |
62 to learn from other people's code. |
61 \end{description} |
63 \end{description} |
62 |
64 |
63 *} |
65 *} |
64 |
66 |
65 section {* Typographic Conventions *} |
67 section {* Typographic Conventions *} |
66 |
68 |
67 text {* |
69 text {* |
68 |
70 |
69 All ML-code in this Cookbook is typeset in highlighed boxes, like the following |
71 All ML-code in this Cookbook is typeset in highlighted boxes, like the following |
70 ML-expression. |
72 ML-expression: |
71 |
73 |
72 \begin{isabelle} |
74 \begin{isabelle} |
73 \begin{graybox} |
75 \begin{graybox} |
74 \isacommand{ML}~@{text "\<verbopen>"}\isanewline |
76 \isacommand{ML}~@{text "\<verbopen>"}\isanewline |
75 \hspace{5mm}@{ML "3 + 4"}\isanewline |
77 \hspace{5mm}@{ML "3 + 4"}\isanewline |
76 @{text "\<verbclose>"} |
78 @{text "\<verbclose>"} |
77 \end{graybox} |
79 \end{graybox} |
78 \end{isabelle} |
80 \end{isabelle} |
79 |
81 |
80 This corresponds to how code can be processed inside the interactive |
82 These boxes corresponds to how code can be processed inside the interactive |
81 environment of Isabelle. It is therefore easy to experiment with the code |
83 environment of Isabelle. It is therefore easy to experiment with what is |
82 (which by the way is highly recommended). However, for better readability we |
84 displayed. However, for better readability we will drop the enclosing |
83 will drop the enclosing \isacommand{ML}~@{text "\<verbopen> \<dots> \<verbclose>"} and just write |
85 \isacommand{ML}~@{text "\<verbopen> \<dots> \<verbclose>"} and just write: |
84 |
86 |
85 |
87 |
86 @{ML [display,gray] "3 + 4"} |
88 @{ML [display,gray] "3 + 4"} |
87 |
89 |
88 for the code above. Whenever appropriate we also show the response the code |
90 Whenever appropriate we also show the response the code |
89 generates when evaluated. This response is prefixed with a |
91 generates when evaluated. This response is prefixed with a |
90 @{text [quotes] ">"} like |
92 @{text [quotes] ">"} like: |
91 |
93 |
92 @{ML_response [display,gray] "3 + 4" "7"} |
94 @{ML_response [display,gray] "3 + 4" "7"} |
93 |
95 |
94 The usual Isabelle commands are written in bold, for example \isacommand{lemma}, |
96 The usual Isabelle commands are written in bold, for example \isacommand{lemma}, |
95 \isacommand{foobar} and so on. We use @{text "$"} to indicate that |
97 \isacommand{foobar} and so on. We use @{text "$"} to indicate that |
96 a command needs to be run on the Unix-command line, for example |
98 a command needs to be run in the Unix-shell, for example |
97 |
99 |
98 @{text [display] "$ ls -la"} |
100 @{text [display] "$ ls -la"} |
99 |
101 |
100 Pointers to further information and Isabelle files are given |
102 Pointers to further information and Isabelle files are typeset in |
101 as follows: |
103 italic and highlighted as follows: |
102 |
104 |
103 \begin{readmore} |
105 \begin{readmore} |
104 Further information or pointer to file. |
106 Further information or pointer to file. |
105 \end{readmore} |
107 \end{readmore} |
106 |
108 |