1 theory Intro |
1 theory Intro |
2 imports Base |
2 imports Base |
3 |
|
4 begin |
3 begin |
5 |
|
6 |
4 |
7 chapter {* Introduction *} |
5 chapter {* Introduction *} |
8 |
6 |
9 text {* |
7 text {* |
10 If your next project requires you to program on the ML-level of Isabelle, |
8 If your next project requires you to program on the ML-level of Isabelle, |
11 then this tutorial is for you. It will guide you through the first steps of |
9 then this tutorial is for you. It will guide you through the first steps of |
12 Isabelle programming, and also explain tricks of the trade. The best way to |
10 Isabelle programming, and also explain tricks of the trade. The best way to |
13 get to know the ML-level of Isabelle is by experimenting with the many code |
11 get to know the ML-level of Isabelle is by experimenting with the many code |
14 examples included in the tutorial. The code is as far as possible checked |
12 examples included in the tutorial. The code is as far as possible checked |
15 against recent versions of Isabelle. If something does not work, then |
13 against recent versions of Isabelle. If something does not work, then please |
16 please let us know. If you have comments, criticism or like to add to the |
14 let us know. It is impossible for us to know every environment, operating |
17 tutorial, please feel free---you are most welcome! The tutorial is meant to be |
15 system or editor in which Isabelle is used. If you have comments, criticism |
18 gentle and comprehensive. To achieve this we need your feedback. |
16 or like to add to the tutorial, please feel free---you are most welcome! The |
|
17 tutorial is meant to be gentle and comprehensive. To achieve this we need |
|
18 your feedback. |
19 *} |
19 *} |
20 |
20 |
21 section {* Intended Audience and Prior Knowledge *} |
21 section {* Intended Audience and Prior Knowledge *} |
22 |
22 |
23 text {* |
23 text {* |
51 \item[The Isar Reference Manual] provides specification material (like grammars, |
51 \item[The Isar Reference Manual] provides specification material (like grammars, |
52 examples and so on) about Isar and its implementation. It is currently in |
52 examples and so on) about Isar and its implementation. It is currently in |
53 the process of being updated. |
53 the process of being updated. |
54 \end{description} |
54 \end{description} |
55 |
55 |
56 Then of course there is: |
56 Then of course there are: |
57 |
57 |
58 \begin{description} |
58 \begin{description} |
59 \item[The code.] It is the ultimate reference for how |
59 \item[The Isabelle sources.] They are the ultimate reference for how |
60 things really work. Therefore you should not hesitate to look at the |
60 things really work. Therefore you should not hesitate to look at the |
61 way things are actually implemented. More importantly, it is often |
61 way things are actually implemented. More importantly, it is often |
62 good to look at code that does similar things as you want to do and |
62 good to look at code that does similar things as you want to do and |
63 learn from it. The GNU/UNIX command @{text "grep -R"} is |
63 learn from it. The GNU/UNIX command @{text "grep -R"} is |
64 often your best friend while programming with Isabelle, or |
64 often your best friend while programming with Isabelle, or |
97 @{ML_response [display,gray] "3 + 4" "7"} |
97 @{ML_response [display,gray] "3 + 4" "7"} |
98 |
98 |
99 The user-level commands of Isabelle (i.e., the non-ML code) are written |
99 The user-level commands of Isabelle (i.e., the non-ML code) are written |
100 in \isacommand{bold face} (e.g., \isacommand{lemma}, \isacommand{apply}, |
100 in \isacommand{bold face} (e.g., \isacommand{lemma}, \isacommand{apply}, |
101 \isacommand{foobar} and so on). We use @{text "$ \<dots>"} to indicate that a |
101 \isacommand{foobar} and so on). We use @{text "$ \<dots>"} to indicate that a |
102 command needs to be run in a Unix-shell, for example: |
102 command needs to be run in a UNIX-shell, for example: |
103 |
103 |
104 @{text [display] "$ grep -R ThyOutput *"} |
104 @{text [display] "$ grep -R ThyOutput *"} |
105 |
105 |
106 Pointers to further information and Isabelle files are typeset in |
106 Pointers to further information and Isabelle files are typeset in |
107 \textit{italic} and highlighted as follows: |
107 \textit{italic} and highlighted as follows: |
125 There are a few naming conventions in Isabelle that might aid reading |
125 There are a few naming conventions in Isabelle that might aid reading |
126 and writing code. (Remember that code is written once, but read numerous |
126 and writing code. (Remember that code is written once, but read numerous |
127 times.) The most important conventions are: |
127 times.) The most important conventions are: |
128 |
128 |
129 \begin{itemize} |
129 \begin{itemize} |
130 \item @{text t}, @{text u} for (raw) terms, @{ML_type term} |
130 \item @{text t}, @{text u} for (raw) terms; ML-type: @{ML_type term} |
131 \item @{text ct}, @{text cu} for certified terms, @{ML_type cterm} |
131 \item @{text ct}, @{text cu} for certified terms; ML-type: @{ML_type cterm} |
132 \item @{text "ty"}, @{text T}, @{text U} for (raw) types, @{ML_type typ} |
132 \item @{text "ty"}, @{text T}, @{text U} for (raw) types; ML-type: @{ML_type typ} |
133 \item @{text th}, @{text thm} for theorems, @{ML_type thm} |
133 \item @{text th}, @{text thm} for theorems; ML-type: @{ML_type thm} |
134 \item @{text "foo_tac"} for tactics, @{ML_type tactic} |
134 \item @{text "foo_tac"} for tactics; ML-type: @{ML_type tactic} |
135 \item @{text thy} for theories, @{ML_type theory} |
135 \item @{text thy} for theories; ML-type: @{ML_type theory} |
136 \item @{text ctxt} for proof contexts, @{ML_type Proof.context} |
136 \item @{text ctxt} for proof contexts; ML-type: @{ML_type Proof.context} |
137 \item @{text lthy} for local theories, @{ML_type local_theory} |
137 \item @{text lthy} for local theories; ML-type: @{ML_type local_theory} |
138 \item @{text context} for generic contextx, @{ML_type Context.generic} |
138 \item @{text context} for generic contexts; ML-type @{ML_type Context.generic} |
139 \end{itemize} |
139 \end{itemize} |
140 *} |
140 *} |
141 |
141 |
142 section {* Acknowledgements *} |
142 section {* Acknowledgements *} |
143 |
143 |