2
+ − 1
theory Intro
75
+ − 2
imports Base
2
+ − 3
begin
+ − 4
+ − 5
chapter {* Introduction *}
+ − 6
+ − 7
text {*
89
+ − 8
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
+ − 9
then this tutorial is for you. It will guide you through the first steps of
89
+ − 10
Isabelle programming, and also explain tricks of the trade. The best way to
+ − 11
get to know the ML-level of Isabelle is by experimenting with the many code
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
+ − 12
examples included in the tutorial. The code is as far as possible checked
254
+ − 13
against the Isabelle distribution.\footnote{\input{version}} If something does not work,
235
+ − 14
then please let us know. It is impossible for us to know every environment,
+ − 15
operating system or editor in which Isabelle is used. If you have comments,
+ − 16
criticism or like to add to the tutorial, please feel free---you are most
+ − 17
welcome! The tutorial is meant to be gentle and comprehensive. To achieve
+ − 18
this we need your feedback.
2
+ − 19
*}
+ − 20
+ − 21
section {* Intended Audience and Prior Knowledge *}
+ − 22
+ − 23
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
+ − 24
This tutorial targets readers who already know how to use Isabelle for
75
+ − 25
writing theories and proofs. We also assume that readers are familiar with
+ − 26
the functional programming language ML, the language in which most of
+ − 27
Isabelle is implemented. If you are unfamiliar with either of these two
+ − 28
subjects, you should first work through the Isabelle/HOL tutorial
+ − 29
\cite{isa-tutorial} or Paulson's book on ML \cite{paulson-ml2}.
2
+ − 30
+ − 31
*}
+ − 32
5
+ − 33
section {* Existing Documentation *}
2
+ − 34
+ − 35
text {*
+ − 36
43
02f76f1b6e7b
added positions to anti-quotations; removed old antiquotation_setup; tuned the text a bit
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 37
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
+ − 38
part of the distribution of Isabelle):
2
+ − 39
+ − 40
\begin{description}
162
+ − 41
\item[The Isabelle/Isar Implementation Manual] describes Isabelle
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
+ − 42
from a high-level perspective, documenting both the underlying
6
+ − 43
concepts and some of the interfaces.
2
+ − 44
5
+ − 45
\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
+ − 46
to be the main reference of Isabelle at a time when all proof scripts
89
+ − 47
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
+ − 48
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
+ − 49
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
+ − 50
153
+ − 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
156
+ − 53
the process of being updated.
5
+ − 54
\end{description}
2
+ − 55
234
+ − 56
Then of course there are:
5
+ − 57
+ − 58
\begin{description}
234
+ − 59
\item[The Isabelle sources.] They are the ultimate reference for how
2
+ − 60
things really work. Therefore you should not hesitate to look at the
+ − 61
way things are actually implemented. More importantly, it is often
89
+ − 62
good to look at code that does similar things as you want to do and
254
+ − 63
learn from it. The UNIX command \mbox{@{text "grep -R"}} is
233
+ − 64
often your best friend while programming with Isabelle, or
263
195c4444dff7
added section about code maintenance and added an example for antiquotations
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 65
hypersearch if you program using jEdit under MacOSX. To understand the sources,
195c4444dff7
added section about code maintenance and added an example for antiquotations
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 66
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
+ − 67
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
+ − 68
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
+ − 69
files and ``change sets''.
2
+ − 70
\end{description}
+ − 71
263
195c4444dff7
added section about code maintenance and added an example for antiquotations
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 72
2
+ − 73
*}
+ − 74
252
+ − 75
section {* Typographic Conventions *}
68
+ − 76
+ − 77
text {*
75
+ − 78
181
+ − 79
All ML-code in this tutorial is typeset in shaded boxes, like the following
89
+ − 80
ML-expression:
75
+ − 81
+ − 82
\begin{isabelle}
+ − 83
\begin{graybox}
85
+ − 84
\isacommand{ML}~@{text "\<verbopen>"}\isanewline
75
+ − 85
\hspace{5mm}@{ML "3 + 4"}\isanewline
85
+ − 86
@{text "\<verbclose>"}
75
+ − 87
\end{graybox}
+ − 88
\end{isabelle}
+ − 89
195
+ − 90
These boxes correspond to how code can be processed inside the interactive
89
+ − 91
environment of Isabelle. It is therefore easy to experiment with what is
+ − 92
displayed. However, for better readability we will drop the enclosing
+ − 93
\isacommand{ML}~@{text "\<verbopen> \<dots> \<verbclose>"} and just write:
75
+ − 94
81
+ − 95
75
+ − 96
@{ML [display,gray] "3 + 4"}
+ − 97
89
+ − 98
Whenever appropriate we also show the response the code
81
+ − 99
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
+ − 100
@{text [quotes] ">"}, like:
75
+ − 101
+ − 102
@{ML_response [display,gray] "3 + 4" "7"}
+ − 103
195
+ − 104
The user-level commands of Isabelle (i.e., the non-ML code) are written
+ − 105
in \isacommand{bold face} (e.g., \isacommand{lemma}, \isacommand{apply},
+ − 106
\isacommand{foobar} and so on). We use @{text "$ \<dots>"} to indicate that a
234
+ − 107
command needs to be run in a UNIX-shell, for example:
75
+ − 108
181
+ − 109
@{text [display] "$ grep -R ThyOutput *"}
75
+ − 110
89
+ − 111
Pointers to further information and Isabelle files are typeset in
195
+ − 112
\textit{italic} and highlighted as follows:
75
+ − 113
+ − 114
\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
+ − 115
Further information or pointers to files.
75
+ − 116
\end{readmore}
+ − 117
182
+ − 118
The pointers to Isabelle files are hyperlinked to the tip of the Mercurial
+ − 119
repository of Isabelle at \href{http://isabelle.in.tum.de/repos/isabelle/}
+ − 120
{http://isabelle.in.tum.de/repos/isabelle/}.
+ − 121
177
+ − 122
A few exercises are scattered around the text. Their solutions are given
156
+ − 123
in Appendix~\ref{ch:solutions}. Of course, you learn most, if you first try
162
+ − 124
to solve the exercises on your own, and then look at the solutions.
233
+ − 125
*}
156
+ − 126
263
195c4444dff7
added section about code maintenance and added an example for antiquotations
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 127
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
+ − 128
195c4444dff7
added section about code maintenance and added an example for antiquotations
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 129
text {*
195c4444dff7
added section about code maintenance and added an example for antiquotations
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 130
One unpleasant aspect of any code development inside a larger system is that
195c4444dff7
added section about code maintenance and added an example for antiquotations
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 131
one has to aim for a ``moving target''. The Isabelle system is no exception. Every
195c4444dff7
added section about code maintenance and added an example for antiquotations
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 132
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
+ − 133
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
+ − 134
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
+ − 135
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
+ − 136
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
+ − 137
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
+ − 138
195c4444dff7
added section about code maintenance and added an example for antiquotations
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 139
However, there are a few steps you can take to mitigate unwanted interferences
195c4444dff7
added section about code maintenance and added an example for antiquotations
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 140
with code changes from other developers. First, you can base your code on the latest
195c4444dff7
added section about code maintenance and added an example for antiquotations
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 141
stable release of Isabelle (it is aimed to have one such release at least
195c4444dff7
added section about code maintenance and added an example for antiquotations
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 142
once every year). This
195c4444dff7
added section about code maintenance and added an example for antiquotations
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 143
might cut you off from the latest feature
195c4444dff7
added section about code maintenance and added an example for antiquotations
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 144
implemented in Isabelle, but at least you do not have to track side-steps
195c4444dff7
added section about code maintenance and added an example for antiquotations
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 145
or dead-ends in the Isabelle development. Of course this means also you have
195c4444dff7
added section about code maintenance and added an example for antiquotations
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 146
to synchronise your code at the next stable release. Another possibility
195c4444dff7
added section about code maintenance and added an example for antiquotations
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 147
is to get your code into the Isabelle distribution. For this you have
195c4444dff7
added section about code maintenance and added an example for antiquotations
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 148
to convince other developers that your code or project is of general interest.
195c4444dff7
added section about code maintenance and added an example for antiquotations
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 149
If you managed to do this, then the problem of the moving target goes
195c4444dff7
added section about code maintenance and added an example for antiquotations
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 150
away, because when checking in code, developers are strongly urged to
195c4444dff7
added section about code maintenance and added an example for antiquotations
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 151
test against Isabelle's code base. If your project is part of that code base,
195c4444dff7
added section about code maintenance and added an example for antiquotations
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 152
then code maintenance is done by others. Unfortunately, this might not
195c4444dff7
added section about code maintenance and added an example for antiquotations
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 153
be a helpful advice for all types of projects. A lower threshold for inclusion has the
195c4444dff7
added section about code maintenance and added an example for antiquotations
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 154
Archive of Formalised Proofs, short AFP.\footnote{\url{http://afp.sourceforge.net/}}
195c4444dff7
added section about code maintenance and added an example for antiquotations
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 155
This archive has been created mainly for formalisations that are
195c4444dff7
added section about code maintenance and added an example for antiquotations
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 156
interesting but not necessarily of general interest. If you have ML-code as
195c4444dff7
added section about code maintenance and added an example for antiquotations
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 157
part of a formalisation, then this might be the right place for you. There
195c4444dff7
added section about code maintenance and added an example for antiquotations
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 158
is no problem with updating your code after submission. At the moment
195c4444dff7
added section about code maintenance and added an example for antiquotations
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 159
developers are not as diligent with checking their code against the AFP than
195c4444dff7
added section about code maintenance and added an example for antiquotations
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 160
with checking agains the distribution, but generally problems will be caught
195c4444dff7
added section about code maintenance and added an example for antiquotations
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 161
and the developer, who caused them, is expected to fix them. So also
195c4444dff7
added section about code maintenance and added an example for antiquotations
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 162
in this case code maintenance is done for you.
195c4444dff7
added section about code maintenance and added an example for antiquotations
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 163
195c4444dff7
added section about code maintenance and added an example for antiquotations
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 164
*}
195c4444dff7
added section about code maintenance and added an example for antiquotations
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 165
252
+ − 166
section {* Some Naming Conventions in the Isabelle Sources *}
233
+ − 167
+ − 168
text {*
254
+ − 169
There are a few naming conventions in the Isabelle code that might aid reading
+ − 170
and writing code. (Remember that code is written once, but read many
233
+ − 171
times.) The most important conventions are:
+ − 172
+ − 173
\begin{itemize}
234
+ − 174
\item @{text t}, @{text u} for (raw) terms; ML-type: @{ML_type term}
+ − 175
\item @{text ct}, @{text cu} for certified terms; ML-type: @{ML_type cterm}
+ − 176
\item @{text "ty"}, @{text T}, @{text U} for (raw) types; ML-type: @{ML_type typ}
+ − 177
\item @{text th}, @{text thm} for theorems; ML-type: @{ML_type thm}
+ − 178
\item @{text "foo_tac"} for tactics; ML-type: @{ML_type tactic}
+ − 179
\item @{text thy} for theories; ML-type: @{ML_type theory}
+ − 180
\item @{text ctxt} for proof contexts; ML-type: @{ML_type Proof.context}
+ − 181
\item @{text lthy} for local theories; ML-type: @{ML_type local_theory}
+ − 182
\item @{text context} for generic contexts; ML-type @{ML_type Context.generic}
235
+ − 183
\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
+ − 184
\item @{text prt} for pretty printing; ML-type @{ML_type Pretty.T}
233
+ − 185
\end{itemize}
68
+ − 186
*}
+ − 187
119
+ − 188
section {* Acknowledgements *}
+ − 189
+ − 190
text {*
+ − 191
Financial support for this tutorial was provided by the German
122
+ − 192
Research Council (DFG) under grant number URB 165/5-1. The following
156
+ − 193
people contributed to the text:
119
+ − 194
+ − 195
\begin{itemize}
122
+ − 196
\item {\bf Stefan Berghofer} wrote nearly all of the ML-code of the
+ − 197
\simpleinductive-package and the code for the @{text
+ − 198
"chunk"}-antiquotation. He also wrote the first version of the chapter
+ − 199
describing the package and has been helpful \emph{beyond measure} with
+ − 200
answering questions about Isabelle.
119
+ − 201
248
11851b20fb78
added more to the pretty section and updated the acknowledgements
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 202
\item {\bf Jasmin Blanchette} helped greatly with section \ref{sec:pretty}.
11851b20fb78
added more to the pretty section and updated the acknowledgements
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 203
119
+ − 204
\item {\bf Sascha Böhme} contributed the recipes in \ref{rec:timeout},
+ − 205
\ref{rec:config}, \ref{rec:storingdata}, \ref{rec:external} and \ref{rec:oracle}.
167
3e30ea95c7aa
added temporarily some timing test about conversions and simprocs
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 206
He also wrote section \ref{sec:conversion} and helped with recipe \ref{rec:timing}.
119
+ − 207
+ − 208
\item {\bf Jeremy Dawson} wrote the first version of the chapter
+ − 209
about parsing.
+ − 210
180
+ − 211
\item {\bf Armin Heller} helped with recipe \ref{rec:sat}.
+ − 212
119
+ − 213
\item {\bf Alexander Krauss} wrote the first version of the ``first-steps''
151
7e0bf13bf743
added more material to the attribute section; merged the recipe about named theorems into the main body; added a solution to an exercise in the conversion section
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 214
chapter and also contributed the material on @{text NamedThmsFun}.
194
+ − 215
207
+ − 216
\item {\bf Christian Sternagel} proofread the tutorial and made
254
+ − 217
many comments on the text.
119
+ − 218
\end{itemize}
+ − 219
121
+ − 220
Please let me know of any omissions. Responsibility for any remaining
153
+ − 221
errors lies with me.\bigskip
+ − 222
233
+ − 223
\vspace{5cm}
153
+ − 224
{\Large\bf
+ − 225
This document is still in the process of being written! All of the
192
+ − 226
text is still under construction. Sections and
153
+ − 227
chapters that are under \underline{heavy} construction are marked
+ − 228
with TBD.}
+ − 229
+ − 230
+ − 231
\vfill
+ − 232
This document was compiled with:\\
228
+ − 233
\input{version}\\
+ − 234
\input{pversion}
119
+ − 235
*}
2
+ − 236
153
+ − 237
+ − 238
195
+ − 239
end