2
|
1 |
theory Intro
|
75
|
2 |
imports Base
|
2
|
3 |
begin
|
|
4 |
|
346
|
5 |
(*<*)
|
|
6 |
setup{*
|
|
7 |
open_file_with_prelude
|
|
8 |
"Intro_Code.thy"
|
|
9 |
["theory Intro", "imports Main", "begin"]
|
|
10 |
*}
|
|
11 |
(*>*)
|
|
12 |
|
2
|
13 |
chapter {* Introduction *}
|
|
14 |
|
|
15 |
text {*
|
295
24c68350d059
polished the package chapter used FOCUS to explain the subproofs
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
16 |
\begin{flushright}
|
24c68350d059
polished the package chapter used FOCUS to explain the subproofs
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
17 |
{\em
|
24c68350d059
polished the package chapter used FOCUS to explain the subproofs
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
18 |
``My thesis is that programming is not at the bottom of the intellectual \\
|
24c68350d059
polished the package chapter used FOCUS to explain the subproofs
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
19 |
pyramid, but at the top. It's creative design of the highest order. It \\
|
24c68350d059
polished the package chapter used FOCUS to explain the subproofs
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
20 |
isn't monkey or donkey work; rather, as Edsger Dijkstra famously \\
|
24c68350d059
polished the package chapter used FOCUS to explain the subproofs
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
21 |
claimed, it's amongst the hardest intellectual tasks ever attempted.''} \\[1ex]
|
324
|
22 |
Richard Bornat, In {\em Defence of Programming}. \cite{Bornat-lecture}
|
295
24c68350d059
polished the package chapter used FOCUS to explain the subproofs
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
23 |
\end{flushright}
|
24c68350d059
polished the package chapter used FOCUS to explain the subproofs
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
24 |
|
24c68350d059
polished the package chapter used FOCUS to explain the subproofs
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
25 |
\medskip
|
89
|
26 |
If your next project requires you to program on the ML-level of Isabelle,
|
106
bdd82350cf22
renamed in the pdf all instances of cookbook to tutorial (in order to sound more serious)
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
27 |
then this tutorial is for you. It will guide you through the first steps of
|
440
|
28 |
Isabelle programming, and also explain ``tricks of the trade''. We also hope
|
|
29 |
the tutorial will encourage students and researchers to play with Isabelle
|
|
30 |
and implement new ideas. The source code of Isabelle can look intimidating,
|
466
|
31 |
but beginners can get by with knowledge of only a handful of concepts,
|
|
32 |
a small number of functions and a few basic coding conventions.
|
356
|
33 |
|
|
34 |
|
|
35 |
The best way to get to know the ML-level of Isabelle is by experimenting
|
|
36 |
with the many code examples included in the tutorial. The code is as far as
|
|
37 |
possible checked against the Isabelle
|
|
38 |
distribution.\footnote{\input{version}} If something does not work, then
|
|
39 |
please let us know. It is impossible for us to know every environment,
|
|
40 |
operating system or editor in which Isabelle is used. If you have comments,
|
|
41 |
criticism or like to add to the tutorial, please feel free---you are most
|
440
|
42 |
welcome!! The tutorial is meant to be gentle and comprehensive. To achieve
|
414
|
43 |
this we need your help and feedback.
|
2
|
44 |
*}
|
|
45 |
|
|
46 |
section {* Intended Audience and Prior Knowledge *}
|
|
47 |
|
|
48 |
text {*
|
106
bdd82350cf22
renamed in the pdf all instances of cookbook to tutorial (in order to sound more serious)
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
49 |
This tutorial targets readers who already know how to use Isabelle for
|
75
|
50 |
writing theories and proofs. We also assume that readers are familiar with
|
|
51 |
the functional programming language ML, the language in which most of
|
|
52 |
Isabelle is implemented. If you are unfamiliar with either of these two
|
329
|
53 |
subjects, then you should first work through the Isabelle/HOL tutorial
|
466
|
54 |
\cite{isa-tutorial} or Paulson's book on ML \cite{paulson-ml2}. Recently,
|
|
55 |
Isabelle has adopted a sizable amount of Scala code for a slick GUI
|
|
56 |
based on jEdit. This part of the code is beyond the interest of this
|
|
57 |
tutorial, since it mostly does not concern the regular Isabelle
|
|
58 |
developer.
|
2
|
59 |
*}
|
|
60 |
|
5
|
61 |
section {* Existing Documentation *}
|
2
|
62 |
|
|
63 |
text {*
|
43
02f76f1b6e7b
added positions to anti-quotations; removed old antiquotation_setup; tuned the text a bit
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
64 |
The following documentation about Isabelle programming already exists (and is
|
02f76f1b6e7b
added positions to anti-quotations; removed old antiquotation_setup; tuned the text a bit
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
65 |
part of the distribution of Isabelle):
|
2
|
66 |
|
|
67 |
\begin{description}
|
162
|
68 |
\item[The Isabelle/Isar Implementation Manual] describes Isabelle
|
414
|
69 |
from a high-level perspective, documenting some of the underlying
|
|
70 |
concepts and interfaces.
|
2
|
71 |
|
5
|
72 |
\item[The Isabelle Reference Manual] is an older document that used
|
44
dee4b3e66dfe
added a readme chapter for prospective authors; added commands for referring to the Isar Reference Manual
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
73 |
to be the main reference of Isabelle at a time when all proof scripts
|
89
|
74 |
were written on the ML-level. Many parts of this manual are outdated
|
44
dee4b3e66dfe
added a readme chapter for prospective authors; added commands for referring to the Isar Reference Manual
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
75 |
now, but some parts, particularly the chapters on tactics, are still
|
dee4b3e66dfe
added a readme chapter for prospective authors; added commands for referring to the Isar Reference Manual
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
76 |
useful.
|
dee4b3e66dfe
added a readme chapter for prospective authors; added commands for referring to the Isar Reference Manual
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
77 |
|
153
|
78 |
\item[The Isar Reference Manual] provides specification material (like grammars,
|
298
|
79 |
examples and so on) about Isar and its implementation.
|
5
|
80 |
\end{description}
|
2
|
81 |
|
234
|
82 |
Then of course there are:
|
5
|
83 |
|
|
84 |
\begin{description}
|
234
|
85 |
\item[The Isabelle sources.] They are the ultimate reference for how
|
2
|
86 |
things really work. Therefore you should not hesitate to look at the
|
466
|
87 |
way things are actually implemented. While much of the Isabelle
|
|
88 |
code is uncommented, some parts have very helpful comments---particularly
|
|
89 |
the code about theorems and terms. Despite the lack of comments in most
|
|
90 |
parts, it is often good to look at code that does similar things as you
|
|
91 |
want to do and learn from it.
|
|
92 |
This tutorial contains frequently pointers to the
|
329
|
93 |
Isabelle sources. Still, the UNIX command \mbox{@{text "grep -R"}} is
|
414
|
94 |
often your best friend while programming with Isabelle.\footnote{Or
|
441
|
95 |
hypersearch if you work with jEdit.} To understand the sources,
|
263
195c4444dff7
added section about code maintenance and added an example for antiquotations
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
96 |
it is often also necessary to track the change history of a file or
|
195c4444dff7
added section about code maintenance and added an example for antiquotations
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
97 |
files. The Mercurial repository\footnote{\url{http://isabelle.in.tum.de/repos/isabelle/}}
|
195c4444dff7
added section about code maintenance and added an example for antiquotations
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
98 |
for Isabelle provides convenient interfaces to query the history of
|
195c4444dff7
added section about code maintenance and added an example for antiquotations
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
99 |
files and ``change sets''.
|
2
|
100 |
\end{description}
|
|
101 |
*}
|
|
102 |
|
252
|
103 |
section {* Typographic Conventions *}
|
68
|
104 |
|
|
105 |
text {*
|
181
|
106 |
All ML-code in this tutorial is typeset in shaded boxes, like the following
|
329
|
107 |
simple ML-expression:
|
75
|
108 |
|
|
109 |
\begin{isabelle}
|
|
110 |
\begin{graybox}
|
85
|
111 |
\isacommand{ML}~@{text "\<verbopen>"}\isanewline
|
75
|
112 |
\hspace{5mm}@{ML "3 + 4"}\isanewline
|
85
|
113 |
@{text "\<verbclose>"}
|
75
|
114 |
\end{graybox}
|
|
115 |
\end{isabelle}
|
|
116 |
|
195
|
117 |
These boxes correspond to how code can be processed inside the interactive
|
343
|
118 |
environment of Isabelle. It is therefore easy to experiment with the code
|
440
|
119 |
that is shown in this tutorial. However, for better readability we will drop
|
343
|
120 |
the enclosing \isacommand{ML}~@{text "\<verbopen> \<dots> \<verbclose>"} and just
|
|
121 |
write:
|
81
|
122 |
|
75
|
123 |
@{ML [display,gray] "3 + 4"}
|
|
124 |
|
89
|
125 |
Whenever appropriate we also show the response the code
|
81
|
126 |
generates when evaluated. This response is prefixed with a
|
108
8bea3f74889d
added to the tactical chapter; polished; added the tabularstar environment (which is just tabular*)
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
127 |
@{text [quotes] ">"}, like:
|
75
|
128 |
|
|
129 |
@{ML_response [display,gray] "3 + 4" "7"}
|
|
130 |
|
195
|
131 |
The user-level commands of Isabelle (i.e., the non-ML code) are written
|
|
132 |
in \isacommand{bold face} (e.g., \isacommand{lemma}, \isacommand{apply},
|
|
133 |
\isacommand{foobar} and so on). We use @{text "$ \<dots>"} to indicate that a
|
234
|
134 |
command needs to be run in a UNIX-shell, for example:
|
75
|
135 |
|
441
|
136 |
@{text [display] "$ grep -R Thy_Output *"}
|
75
|
137 |
|
89
|
138 |
Pointers to further information and Isabelle files are typeset in
|
195
|
139 |
\textit{italic} and highlighted as follows:
|
75
|
140 |
|
|
141 |
\begin{readmore}
|
102
5e309df58557
general cleaning up; deleted antiquotation ML_text; adjusted pathnames of various files in the distribution
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
142 |
Further information or pointers to files.
|
75
|
143 |
\end{readmore}
|
|
144 |
|
440
|
145 |
Note that pointers to Isabelle files are hyperlinked to the tip of the Mercurial
|
414
|
146 |
repository at \href{http://isabelle.in.tum.de/repos/isabelle/}
|
440
|
147 |
{http://isabelle.in.tum.de/repos/isabelle/}, not the latest stable release
|
414
|
148 |
of Isabelle.
|
182
|
149 |
|
177
|
150 |
A few exercises are scattered around the text. Their solutions are given
|
156
|
151 |
in Appendix~\ref{ch:solutions}. Of course, you learn most, if you first try
|
162
|
152 |
to solve the exercises on your own, and then look at the solutions.
|
233
|
153 |
*}
|
156
|
154 |
|
440
|
155 |
section {* How To Understand Isabelle Code *}
|
421
|
156 |
|
|
157 |
text {*
|
466
|
158 |
One of the more difficult aspects of any kind of programming is to
|
|
159 |
understand code written by somebody else. This is aggravated in Isabelle by
|
|
160 |
the fact that many parts of the code contain none or only few
|
|
161 |
comments. There is one strategy that might be helpful to navigate your way:
|
|
162 |
ML is an interactive programming environment, which means you can evaluate
|
|
163 |
code on the fly (for example inside an \isacommand{ML}~@{text
|
|
164 |
"\<verbopen>\<dots>\<verbclose>"} section). So you can copy (self-contained)
|
|
165 |
chunks of existing code into a separate theory file and then study it
|
|
166 |
alongside with examples. You can also install ``probes'' inside the copied
|
|
167 |
code without having to recompile the whole Isabelle distribution. Such
|
421
|
168 |
probes might be messages or printouts of variables (see chapter
|
|
169 |
\ref{chp:firststeps}). Although PolyML also contains a debugger, it seems
|
440
|
170 |
probing the code with explicit print statements is the most effective method
|
466
|
171 |
for understanding what some piece of code is doing. However do not expect
|
|
172 |
quick results with this! It is painful. Depending on the size of the code
|
|
173 |
you are looking at, you will spend the better part of a quiet afternoon with
|
|
174 |
it. And there seems to be no better way for understanding code in Isabelle.
|
421
|
175 |
*}
|
|
176 |
|
|
177 |
|
263
195c4444dff7
added section about code maintenance and added an example for antiquotations
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
178 |
section {* Aaaaargh! My Code Does not Work Anymore *}
|
195c4444dff7
added section about code maintenance and added an example for antiquotations
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
179 |
|
195c4444dff7
added section about code maintenance and added an example for antiquotations
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
180 |
text {*
|
195c4444dff7
added section about code maintenance and added an example for antiquotations
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
181 |
One unpleasant aspect of any code development inside a larger system is that
|
440
|
182 |
one has to aim at a ``moving target''. Isabelle is no exception of this. Every
|
263
195c4444dff7
added section about code maintenance and added an example for antiquotations
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
183 |
update lets potentially all hell break loose, because other developers have
|
195c4444dff7
added section about code maintenance and added an example for antiquotations
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
184 |
changed code you are relying on. Cursing is somewhat helpful in such situations,
|
195c4444dff7
added section about code maintenance and added an example for antiquotations
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
185 |
but taking the view that incompatible code changes are a fact of life
|
195c4444dff7
added section about code maintenance and added an example for antiquotations
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
186 |
might be more gratifying. Isabelle is a research project. In most circumstances
|
195c4444dff7
added section about code maintenance and added an example for antiquotations
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
187 |
it is just impossible to make research backward compatible (imagine Darwin
|
195c4444dff7
added section about code maintenance and added an example for antiquotations
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
188 |
attempting to make the Theory of Evolution backward compatible).
|
195c4444dff7
added section about code maintenance and added an example for antiquotations
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
189 |
|
329
|
190 |
However, there are a few steps you can take to mitigate unwanted
|
|
191 |
interferences with code changes from other developers. First, you can base
|
|
192 |
your code on the latest stable release of Isabelle (it is aimed to have one
|
|
193 |
such release at least once every year). This might cut you off from the
|
|
194 |
latest feature implemented in Isabelle, but at least you do not have to
|
|
195 |
track side-steps or dead-ends in the Isabelle development. Of course this
|
|
196 |
means also you have to synchronise your code at the next stable release. If
|
|
197 |
you do not synchronise, be warned that code seems to ``rot'' very
|
|
198 |
quickly. Another possibility is to get your code into the Isabelle
|
|
199 |
distribution. For this you have to convince other developers that your code
|
|
200 |
or project is of general interest. If you managed to do this, then the
|
|
201 |
problem of the moving target goes away, because when checking in new code,
|
|
202 |
developers are strongly urged to test it against Isabelle's code base. If
|
|
203 |
your project is part of that code base, then maintenance is done by
|
|
204 |
others. Unfortunately, this might not be a helpful advice for all types of
|
454
|
205 |
projects. A lower threshold for inclusion has the Archive of Formal
|
329
|
206 |
Proofs, short AFP.\footnote{\url{http://afp.sourceforge.net/}} This archive
|
|
207 |
has been created mainly for formalisations that are interesting but not
|
|
208 |
necessarily of general interest. If you have ML-code as part of a
|
|
209 |
formalisation, then this might be the right place for you. There is no
|
|
210 |
problem with updating your code after submission. At the moment developers
|
|
211 |
are not as diligent with checking their code against the AFP than with
|
|
212 |
checking agains the distribution, but generally problems will be caught and
|
|
213 |
the developer, who caused them, is expected to fix them. So also in this
|
|
214 |
case code maintenance is done for you.
|
263
195c4444dff7
added section about code maintenance and added an example for antiquotations
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
215 |
*}
|
195c4444dff7
added section about code maintenance and added an example for antiquotations
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
216 |
|
252
|
217 |
section {* Some Naming Conventions in the Isabelle Sources *}
|
233
|
218 |
|
|
219 |
text {*
|
254
|
220 |
There are a few naming conventions in the Isabelle code that might aid reading
|
|
221 |
and writing code. (Remember that code is written once, but read many
|
233
|
222 |
times.) The most important conventions are:
|
|
223 |
|
|
224 |
\begin{itemize}
|
302
|
225 |
\item @{text t}, @{text u}, @{text trm} for (raw) terms; ML-type: @{ML_type term}
|
234
|
226 |
\item @{text ct}, @{text cu} for certified terms; ML-type: @{ML_type cterm}
|
|
227 |
\item @{text "ty"}, @{text T}, @{text U} for (raw) types; ML-type: @{ML_type typ}
|
390
|
228 |
\item @{text "S"} for sorts; ML-type: @{ML_type sort}
|
234
|
229 |
\item @{text th}, @{text thm} for theorems; ML-type: @{ML_type thm}
|
|
230 |
\item @{text "foo_tac"} for tactics; ML-type: @{ML_type tactic}
|
|
231 |
\item @{text thy} for theories; ML-type: @{ML_type theory}
|
|
232 |
\item @{text ctxt} for proof contexts; ML-type: @{ML_type Proof.context}
|
|
233 |
\item @{text lthy} for local theories; ML-type: @{ML_type local_theory}
|
|
234 |
\item @{text context} for generic contexts; ML-type @{ML_type Context.generic}
|
235
|
235 |
\item @{text mx} for mixfix syntax annotations; ML-type @{ML_type mixfix}
|
248
11851b20fb78
added more to the pretty section and updated the acknowledgements
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
236 |
\item @{text prt} for pretty printing; ML-type @{ML_type Pretty.T}
|
425
|
237 |
\item @{text phi} for morphisms; ML-type @{ML_type morphism}
|
233
|
238 |
\end{itemize}
|
68
|
239 |
*}
|
|
240 |
|
119
|
241 |
section {* Acknowledgements *}
|
|
242 |
|
|
243 |
text {*
|
|
244 |
Financial support for this tutorial was provided by the German
|
122
|
245 |
Research Council (DFG) under grant number URB 165/5-1. The following
|
156
|
246 |
people contributed to the text:
|
119
|
247 |
|
|
248 |
\begin{itemize}
|
122
|
249 |
\item {\bf Stefan Berghofer} wrote nearly all of the ML-code of the
|
|
250 |
\simpleinductive-package and the code for the @{text
|
414
|
251 |
"chunk"}-antiquotation. He also wrote the first version of chapter
|
|
252 |
\ref{chp:package} describing this package and has been helpful \emph{beyond
|
|
253 |
measure} with answering questions about Isabelle.
|
119
|
254 |
|
469
|
255 |
\item {\bf Jasmin Blanchette} helped greatly with section \ref{sec:pretty}
|
|
256 |
and exercise \ref{fun:killqnt}.
|
248
11851b20fb78
added more to the pretty section and updated the acknowledgements
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
257 |
|
119
|
258 |
\item {\bf Sascha Böhme} contributed the recipes in \ref{rec:timeout},
|
328
|
259 |
\ref{rec:external} and \ref{rec:oracle}. He also wrote section \ref{sec:conversion}
|
329
|
260 |
and helped with recipe \ref{rec:timing}. Parts of section \ref{sec:storing}
|
328
|
261 |
are by him.
|
119
|
262 |
|
414
|
263 |
\item {\bf Lukas Bulwahn} made me aware of a problem with recursive
|
392
|
264 |
parsers and contributed exercise \ref{ex:contextfree}.
|
390
|
265 |
|
414
|
266 |
\item {\bf Jeremy Dawson} wrote the first version of chapter \ref{chp:parsing}
|
119
|
267 |
about parsing.
|
|
268 |
|
180
|
269 |
\item {\bf Armin Heller} helped with recipe \ref{rec:sat}.
|
|
270 |
|
414
|
271 |
\item {\bf Alexander Krauss} wrote a very early version of the ``first-steps''
|
343
|
272 |
chapter and also contributed the material on @{ML_funct Named_Thms}.
|
194
|
273 |
|
427
|
274 |
\item {\bf Tobias Nipkow} contributed recipe \ref{rec:callml}.
|
|
275 |
|
417
|
276 |
\item {\bf Michael Norrish} proofread parts of the text.
|
|
277 |
|
435
|
278 |
\item {\bf Andreas Schropp} improved and corrected section \ref{sec:univ} and
|
|
279 |
contributed towards section \ref{sec:sorts}.
|
|
280 |
|
207
|
281 |
\item {\bf Christian Sternagel} proofread the tutorial and made
|
293
|
282 |
many improvemets to the text.
|
119
|
283 |
\end{itemize}
|
|
284 |
|
121
|
285 |
Please let me know of any omissions. Responsibility for any remaining
|
153
|
286 |
errors lies with me.\bigskip
|
|
287 |
|
421
|
288 |
\newpage
|
|
289 |
\mbox{}\\[5cm]
|
|
290 |
|
|
291 |
|
153
|
292 |
{\Large\bf
|
335
|
293 |
This tutorial is still in the process of being written! All of the
|
192
|
294 |
text is still under construction. Sections and
|
153
|
295 |
chapters that are under \underline{heavy} construction are marked
|
|
296 |
with TBD.}
|
|
297 |
|
|
298 |
\vfill
|
306
|
299 |
|
|
300 |
This document (version \input{tip}\hspace{-0.5ex}) was compiled with:\\
|
228
|
301 |
\input{version}\\
|
462
|
302 |
%%\input{pversion}
|
119
|
303 |
*}
|
2
|
304 |
|
195
|
305 |
end
|