1 theory Intro |
1 theory Intro |
2 imports Main |
2 imports Base |
3 |
3 |
4 begin |
4 begin |
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 The purpose of this Cookbook is to guide the reader through the first steps |
11 of Isabelle programming, and to explain some tricks of the trade. The code |
11 of Isabelle programming, and to explain tricks of the trade. The code |
12 provided in the Cookbook is as far as possible checked against recent |
12 provided in the Cookbook is as far as possible checked against recent |
13 versions of Isabelle. If something does not work, then please let us |
13 versions of Isabelle. If something does not work, then please let us |
14 know. If you have comments or like to add to the Cookbook, you are very |
14 know. If you have comments or like to add to the Cookbook, you are very |
15 welcome. |
15 welcome! The Cookbook will {\bf only} remain to be helpful, if it gets constantly |
|
16 updated. |
16 |
17 |
17 *} |
18 *} |
18 |
19 |
19 section {* Intended Audience and Prior Knowledge *} |
20 section {* Intended Audience and Prior Knowledge *} |
20 |
21 |
21 text {* |
22 text {* |
22 This Cookbook targets readers who already know how to use Isabelle |
23 This Cookbook targets readers who already know how to use Isabelle for |
23 for writing theories and proofs. We also assume that readers are |
24 writing theories and proofs. We also assume that readers are familiar with |
24 familiar with the functional programming language ML, the language in |
25 the functional programming language ML, the language in which most of |
25 which most of Isabelle is implemented. If you are unfamiliar with either of |
26 Isabelle is implemented. If you are unfamiliar with either of these two |
26 these two subjects, you should first work through the Isabelle/HOL |
27 subjects, you should first work through the Isabelle/HOL tutorial |
27 tutorial \cite{isa-tutorial} or Paulson's book on ML |
28 \cite{isa-tutorial} or Paulson's book on ML \cite{paulson-ml2}. |
28 \cite{paulson-ml2}. |
|
29 |
29 |
30 *} |
30 *} |
31 |
31 |
32 section {* Existing Documentation *} |
32 section {* Existing Documentation *} |
33 |
33 |
65 *} |
65 *} |
66 |
66 |
67 section {* Conventions *} |
67 section {* Conventions *} |
68 |
68 |
69 text {* |
69 text {* |
70 We use @{text "$"} to indicate a command needs to be run on the Unix-command |
70 |
71 line. |
71 All ML-code in this Cookbook is shown in highlighed displays, such as: |
|
72 |
|
73 \begin{isabelle} |
|
74 \begin{graybox} |
|
75 \isa{\isacommand{ML} |
|
76 \isacharverbatimopen\isanewline |
|
77 \hspace{5mm}@{ML "3 + 4"}\isanewline |
|
78 \isacharverbatimclose} |
|
79 \end{graybox} |
|
80 \end{isabelle} |
|
81 |
|
82 This corresponds to how code can be processed inside the interactive |
|
83 environment of Isabelle. However, for better readability we will drop |
|
84 the enclosing \isacommand{ML} \isa{\isacharverbatimopen \ldots |
|
85 \isacharverbatimclose} and just show |
|
86 |
|
87 @{ML [display,gray] "3 + 4"} |
|
88 |
|
89 for the code above. Whenever appropriate we show the response of the code |
|
90 when evaluated. The response is prefixed with a @{text [quotes] ">"}", like |
|
91 |
|
92 @{ML_response [display,gray] "3 + 4" "7"} |
|
93 |
|
94 Isabelle commands are written in bold. For example \isacommand{lemma}, |
|
95 \isacommand{foobar} and so on. We use @{text "$"} to indicate a command |
|
96 needs to be run on the Unix-command line, like |
|
97 |
|
98 @{text [display] "$ ls -la"} |
|
99 |
|
100 Pointers to further information and files are indicated as follows: |
|
101 |
|
102 \begin{readmore} |
|
103 Further information. |
|
104 \end{readmore} |
|
105 |
72 *} |
106 *} |
73 |
107 |
74 |
108 |
75 end |
109 end |