35 please let us know. It is impossible for us to know every environment, |
35 please let us know. It is impossible for us to know every environment, |
36 operating system or editor in which Isabelle is used. If you have comments, |
36 operating system or editor in which Isabelle is used. If you have comments, |
37 criticism or like to add to the tutorial, please feel free---you are most |
37 criticism or like to add to the tutorial, please feel free---you are most |
38 welcome!! The tutorial is meant to be gentle and comprehensive. To achieve |
38 welcome!! The tutorial is meant to be gentle and comprehensive. To achieve |
39 this we need your help and feedback. |
39 this we need your help and feedback. |
40 *} |
40 \<close> |
41 |
41 |
42 section {* Intended Audience and Prior Knowledge *} |
42 section \<open>Intended Audience and Prior Knowledge\<close> |
43 |
43 |
44 text {* |
44 text \<open> |
45 This tutorial targets readers who already know how to use Isabelle for |
45 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 |
46 writing theories and proofs. We also assume that readers are familiar with |
47 the functional programming language ML, the language in which most of |
47 the functional programming language ML, the language in which most of |
48 Isabelle is implemented. If you are unfamiliar with either of these two |
48 Isabelle is implemented. If you are unfamiliar with either of these two |
49 subjects, then you should first work through the Isabelle/HOL tutorial |
49 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, |
50 \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 |
51 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 |
52 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 |
53 tutorial, since it mostly does not concern the regular Isabelle |
54 developer. |
54 developer. |
55 *} |
55 \<close> |
56 |
56 |
57 section {* Existing Documentation *} |
57 section \<open>Existing Documentation\<close> |
58 |
58 |
59 text {* |
59 text \<open> |
60 The following documentation about Isabelle programming already exists (and is |
60 The following documentation about Isabelle programming already exists (and is |
61 part of the distribution of Isabelle): |
61 part of the distribution of Isabelle): |
62 |
62 |
63 \begin{description} |
63 \begin{description} |
64 \item[The Isabelle/Isar Implementation Manual] describes Isabelle |
64 \item[The Isabelle/Isar Implementation Manual] describes Isabelle |
84 code is uncommented, some parts have very helpful comments---particularly |
84 code is uncommented, some parts have very helpful comments---particularly |
85 the code about theorems and terms. Despite the lack of comments in most |
85 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 |
86 parts, it is often good to look at code that does similar things as you |
87 want to do and learn from it. |
87 want to do and learn from it. |
88 This tutorial contains frequently pointers to the |
88 This tutorial contains frequently pointers to the |
89 Isabelle sources. Still, the UNIX command \mbox{@{text "grep -R"}} is |
89 Isabelle sources. Still, the UNIX command \mbox{\<open>grep -R\<close>} is |
90 often your best friend while programming with Isabelle.\footnote{Or |
90 often your best friend while programming with Isabelle.\footnote{Or |
91 hypersearch if you work with jEdit.} To understand the sources, |
91 hypersearch if you work with jEdit.} To understand the sources, |
92 it is often also necessary to track the change history of a file or |
92 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/}} |
93 files. The Mercurial repository\footnote{\url{http://isabelle.in.tum.de/repos/isabelle/}} |
94 for Isabelle provides convenient interfaces to query the history of |
94 for Isabelle provides convenient interfaces to query the history of |
95 files and ``change sets''. |
95 files and ``change sets''. |
96 \end{description} |
96 \end{description} |
97 *} |
97 \<close> |
98 |
98 |
99 section {* Typographic Conventions *} |
99 section \<open>Typographic Conventions\<close> |
100 |
100 |
101 text {* |
101 text \<open> |
102 All ML-code in this tutorial is typeset in shaded boxes, like the following |
102 All ML-code in this tutorial is typeset in shaded boxes, like the following |
103 simple ML-expression: |
103 simple ML-expression: |
104 |
104 |
105 \begin{isabelle} |
105 \begin{isabelle} |
106 \begin{graybox} |
106 \begin{graybox} |
107 \isacommand{ML}~@{text "\<verbopen>"}\isanewline |
107 \isacommand{ML}~\<open>\<verbopen>\<close>\isanewline |
108 \hspace{5mm}@{ML "3 + 4"}\isanewline |
108 \hspace{5mm}@{ML "3 + 4"}\isanewline |
109 @{text "\<verbclose>"} |
109 \<open>\<verbclose>\<close> |
110 \end{graybox} |
110 \end{graybox} |
111 \end{isabelle} |
111 \end{isabelle} |
112 |
112 |
113 These boxes correspond to how code can be processed inside the interactive |
113 These boxes correspond to how code can be processed inside the interactive |
114 environment of Isabelle. It is therefore easy to experiment with the code |
114 environment of Isabelle. It is therefore easy to experiment with the code |
115 that is shown in this tutorial. However, for better readability we will drop |
115 that is shown in this tutorial. However, for better readability we will drop |
116 the enclosing \isacommand{ML}~@{text "\<verbopen> \<dots> \<verbclose>"} and just |
116 the enclosing \isacommand{ML}~\<open>\<verbopen> \<dots> \<verbclose>\<close> and just |
117 write: |
117 write: |
118 |
118 |
119 @{ML [display,gray] "3 + 4"} |
119 @{ML [display,gray] "3 + 4"} |
120 |
120 |
121 Whenever appropriate we also show the response the code |
121 Whenever appropriate we also show the response the code |
124 |
124 |
125 @{ML_response [display,gray] "3 + 4" "7"} |
125 @{ML_response [display,gray] "3 + 4" "7"} |
126 |
126 |
127 The user-level commands of Isabelle (i.e., the non-ML code) are written |
127 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}, |
128 in \isacommand{bold face} (e.g., \isacommand{lemma}, \isacommand{apply}, |
129 \isacommand{foobar} and so on). We use @{text "$ \<dots>"} to indicate that a |
129 \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: |
130 command needs to be run in a UNIX-shell, for example: |
131 |
131 |
132 @{text [display] "$ grep -R Thy_Output *"} |
132 @{text [display] "$ grep -R Thy_Output *"} |
133 |
133 |
134 Pointers to further information and Isabelle files are typeset in |
134 Pointers to further information and Isabelle files are typeset in |
144 of Isabelle. |
144 of Isabelle. |
145 |
145 |
146 A few exercises are scattered around the text. Their solutions are given |
146 A few exercises are scattered around the text. Their solutions are given |
147 in Appendix~\ref{ch:solutions}. Of course, you learn most, if you first try |
147 in Appendix~\ref{ch:solutions}. Of course, you learn most, if you first try |
148 to solve the exercises on your own, and then look at the solutions. |
148 to solve the exercises on your own, and then look at the solutions. |
149 *} |
149 \<close> |
150 |
150 |
151 section {* How To Understand Isabelle Code *} |
151 section \<open>How To Understand Isabelle Code\<close> |
152 |
152 |
153 text {* |
153 text \<open> |
154 One of the more difficult aspects of any kind of programming is to |
154 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 |
155 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 |
156 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: |
157 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 |
158 ML is an interactive programming environment, which means you can evaluate |
159 code on the fly (for example inside an \isacommand{ML}~@{text |
159 code on the fly (for example inside an \isacommand{ML}~\<open>\<verbopen>\<dots>\<verbclose>\<close> section). So you can copy (self-contained) |
160 "\<verbopen>\<dots>\<verbclose>"} section). So you can copy (self-contained) |
|
161 chunks of existing code into a separate theory file and then study it |
160 chunks of existing code into a separate theory file and then study it |
162 alongside with examples. You can also install ``probes'' inside the copied |
161 alongside with examples. You can also install ``probes'' inside the copied |
163 code without having to recompile the whole Isabelle distribution. Such |
162 code without having to recompile the whole Isabelle distribution. Such |
164 probes might be messages or printouts of variables (see chapter |
163 probes might be messages or printouts of variables (see chapter |
165 \ref{chp:firststeps}). Although PolyML also contains a debugger, it seems |
164 \ref{chp:firststeps}). Although PolyML also contains a debugger, it seems |
166 probing the code with explicit print statements is the most effective method |
165 probing the code with explicit print statements is the most effective method |
167 for understanding what some piece of code is doing. However do not expect |
166 for understanding what some piece of code is doing. However do not expect |
168 quick results with this! It is painful. Depending on the size of the code |
167 quick results with this! It is painful. Depending on the size of the code |
169 you are looking at, you will spend the better part of a quiet afternoon with |
168 you are looking at, you will spend the better part of a quiet afternoon with |
170 it. And there seems to be no better way for understanding code in Isabelle. |
169 it. And there seems to be no better way for understanding code in Isabelle. |
171 *} |
170 \<close> |
172 |
171 |
173 |
172 |
174 section {* Aaaaargh! My Code Does not Work Anymore *} |
173 section \<open>Aaaaargh! My Code Does not Work Anymore\<close> |
175 |
174 |
176 text {* |
175 text \<open> |
177 One unpleasant aspect of any code development inside a larger system is that |
176 One unpleasant aspect of any code development inside a larger system is that |
178 one has to aim at a ``moving target''. Isabelle is no exception of this. Every |
177 one has to aim at a ``moving target''. Isabelle is no exception of this. Every |
179 update lets potentially all hell break loose, because other developers have |
178 update lets potentially all hell break loose, because other developers have |
180 changed code you are relying on. Cursing is somewhat helpful in such situations, |
179 changed code you are relying on. Cursing is somewhat helpful in such situations, |
181 but taking the view that incompatible code changes are a fact of life |
180 but taking the view that incompatible code changes are a fact of life |
206 problem with updating your code after submission. At the moment developers |
205 problem with updating your code after submission. At the moment developers |
207 are not as diligent with checking their code against the AFP than with |
206 are not as diligent with checking their code against the AFP than with |
208 checking agains the distribution, but generally problems will be caught and |
207 checking agains the distribution, but generally problems will be caught and |
209 the developer, who caused them, is expected to fix them. So also in this |
208 the developer, who caused them, is expected to fix them. So also in this |
210 case code maintenance is done for you. |
209 case code maintenance is done for you. |
211 *} |
210 \<close> |
212 |
211 |
213 section {* Serious Isabelle ML-Programming *} |
212 section \<open>Serious Isabelle ML-Programming\<close> |
214 |
213 |
215 text {* |
214 text \<open> |
216 As already pointed out in the previous section, Isabelle is a joint effort |
215 As already pointed out in the previous section, Isabelle is a joint effort |
217 of many developers. Therefore, disruptions that break the work of others |
216 of many developers. Therefore, disruptions that break the work of others |
218 are generally frowned upon. ``Accidents'' however do happen and everybody knows |
217 are generally frowned upon. ``Accidents'' however do happen and everybody knows |
219 this. Still to keep them to a minimum, you can submit your changes first to a rather |
218 this. Still to keep them to a minimum, you can submit your changes first to a rather |
220 sophisticated \emph{testboard}, which will perform checks of your changes against the |
219 sophisticated \emph{testboard}, which will perform checks of your changes against the |
234 |
233 |
235 @{text [display] "$ hg push -f ssh://...@hgbroy.informatik.tu-muenchen.de\\ |
234 @{text [display] "$ hg push -f ssh://...@hgbroy.informatik.tu-muenchen.de\\ |
236 //home/isabelle-repository/repos/testboard"} |
235 //home/isabelle-repository/repos/testboard"} |
237 |
236 |
238 where the dots need to be replaced by your login name. Note that for |
237 where the dots need to be replaced by your login name. Note that for |
239 pushing changes to the testboard you need to add the option @{text "-f"}, |
238 pushing changes to the testboard you need to add the option \<open>-f\<close>, |
240 which should \emph{never} be used with the main Isabelle |
239 which should \emph{never} be used with the main Isabelle |
241 repository. While the testboard is a great system for supporting Isabelle |
240 repository. While the testboard is a great system for supporting Isabelle |
242 developers, its disadvantage is that it needs login permissions for the |
241 developers, its disadvantage is that it needs login permissions for the |
243 computers in Munich. So in order to use it, you might have to ask other |
242 computers in Munich. So in order to use it, you might have to ask other |
244 developers to obtain one. |
243 developers to obtain one. |
245 *} |
244 \<close> |
246 |
245 |
247 |
246 |
248 section {* Some Naming Conventions in the Isabelle Sources *} |
247 section \<open>Some Naming Conventions in the Isabelle Sources\<close> |
249 |
248 |
250 text {* |
249 text \<open> |
251 There are a few naming conventions in the Isabelle code that might aid reading |
250 There are a few naming conventions in the Isabelle code that might aid reading |
252 and writing code. (Remember that code is written once, but read many |
251 and writing code. (Remember that code is written once, but read many |
253 times.) The most important conventions are: |
252 times.) The most important conventions are: |
254 |
253 |
255 \begin{itemize} |
254 \begin{itemize} |
256 \item @{text t}, @{text u}, @{text trm} for (raw) terms; ML-type: @{ML_type term} |
255 \item \<open>t\<close>, \<open>u\<close>, \<open>trm\<close> for (raw) terms; ML-type: @{ML_type term} |
257 \item @{text ct}, @{text cu} for certified terms; ML-type: @{ML_type cterm} |
256 \item \<open>ct\<close>, \<open>cu\<close> for certified terms; ML-type: @{ML_type cterm} |
258 \item @{text "ty"}, @{text T}, @{text U} for (raw) types; ML-type: @{ML_type typ} |
257 \item \<open>ty\<close>, \<open>T\<close>, \<open>U\<close> for (raw) types; ML-type: @{ML_type typ} |
259 \item @{text "S"} for sorts; ML-type: @{ML_type sort} |
258 \item \<open>S\<close> for sorts; ML-type: @{ML_type sort} |
260 \item @{text th}, @{text thm} for theorems; ML-type: @{ML_type thm} |
259 \item \<open>th\<close>, \<open>thm\<close> for theorems; ML-type: @{ML_type thm} |
261 \item @{text "foo_tac"} for tactics; ML-type: @{ML_type tactic} |
260 \item \<open>foo_tac\<close> for tactics; ML-type: @{ML_type tactic} |
262 \item @{text thy} for theories; ML-type: @{ML_type theory} |
261 \item \<open>thy\<close> for theories; ML-type: @{ML_type theory} |
263 \item @{text ctxt} for proof contexts; ML-type: @{ML_type Proof.context} |
262 \item \<open>ctxt\<close> for proof contexts; ML-type: @{ML_type Proof.context} |
264 \item @{text lthy} for local theories; ML-type: @{ML_type local_theory} |
263 \item \<open>lthy\<close> for local theories; ML-type: @{ML_type local_theory} |
265 \item @{text context} for generic contexts; ML-type @{ML_type Context.generic} |
264 \item \<open>context\<close> for generic contexts; ML-type @{ML_type Context.generic} |
266 \item @{text mx} for mixfix syntax annotations; ML-type @{ML_type mixfix} |
265 \item \<open>mx\<close> for mixfix syntax annotations; ML-type @{ML_type mixfix} |
267 \item @{text prt} for pretty printing; ML-type @{ML_type Pretty.T} |
266 \item \<open>prt\<close> for pretty printing; ML-type @{ML_type Pretty.T} |
268 \item @{text phi} for morphisms; ML-type @{ML_type morphism} |
267 \item \<open>phi\<close> for morphisms; ML-type @{ML_type morphism} |
269 \end{itemize} |
268 \end{itemize} |
270 *} |
269 \<close> |
271 |
270 |
272 section {* Acknowledgements *} |
271 section \<open>Acknowledgements\<close> |
273 |
272 |
274 text {* |
273 text \<open> |
275 Financial support for this tutorial was provided by the German |
274 Financial support for this tutorial was provided by the German |
276 Research Council (DFG) under grant number URB 165/5-1. The following |
275 Research Council (DFG) under grant number URB 165/5-1. The following |
277 people contributed to the text: |
276 people contributed to the text: |
278 |
277 |
279 \begin{itemize} |
278 \begin{itemize} |
280 \item {\bf Stefan Berghofer} wrote nearly all of the ML-code of the |
279 \item {\bf Stefan Berghofer} wrote nearly all of the ML-code of the |
281 \simpleinductive-package and the code for the @{text |
280 \simpleinductive-package and the code for the \<open>chunk\<close>-antiquotation. He also wrote the first version of chapter |
282 "chunk"}-antiquotation. He also wrote the first version of chapter |
|
283 \ref{chp:package} describing this package and has been helpful \emph{beyond |
281 \ref{chp:package} describing this package and has been helpful \emph{beyond |
284 measure} with answering questions about Isabelle. |
282 measure} with answering questions about Isabelle. |
285 |
283 |
286 \item {\bf Jasmin Blanchette} helped greatly with section \ref{sec:pretty} |
284 \item {\bf Jasmin Blanchette} helped greatly with section \ref{sec:pretty} |
287 and exercise \ref{fun:killqnt}. |
285 and exercise \ref{fun:killqnt}. |
288 |
286 |
289 \item {\bf Sascha Böhme} contributed the recipes in \ref{rec:timeout}, |
287 \item {\bf Sascha B�hme} contributed the recipes in \ref{rec:timeout}, |
290 \ref{rec:external} and \ref{rec:oracle}. He also wrote section \ref{sec:conversion} |
288 \ref{rec:external} and \ref{rec:oracle}. He also wrote section \ref{sec:conversion} |
291 and helped with recipe \ref{rec:timing}. Parts of section \ref{sec:storing} |
289 and helped with recipe \ref{rec:timing}. Parts of section \ref{sec:storing} |
292 are by him. |
290 are by him. |
293 |
291 |
294 \item {\bf Lukas Bulwahn} made me aware of a problem with recursive |
292 \item {\bf Lukas Bulwahn} made me aware of a problem with recursive |