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
235
+ − 13
against \input{version}. If something does not work,
+ − 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
235
+ − 63
learn from it. The GNU/UNIX command \mbox{@{text "grep -R"}} is
233
+ − 64
often your best friend while programming with Isabelle, or
235
+ − 65
hypersearch if you program using jEdit under MacOSX.
2
+ − 66
\end{description}
+ − 67
+ − 68
*}
+ − 69
233
+ − 70
section {* Typographic Conventions in the Tutorial *}
68
+ − 71
+ − 72
text {*
75
+ − 73
181
+ − 74
All ML-code in this tutorial is typeset in shaded boxes, like the following
89
+ − 75
ML-expression:
75
+ − 76
+ − 77
\begin{isabelle}
+ − 78
\begin{graybox}
85
+ − 79
\isacommand{ML}~@{text "\<verbopen>"}\isanewline
75
+ − 80
\hspace{5mm}@{ML "3 + 4"}\isanewline
85
+ − 81
@{text "\<verbclose>"}
75
+ − 82
\end{graybox}
+ − 83
\end{isabelle}
+ − 84
195
+ − 85
These boxes correspond to how code can be processed inside the interactive
89
+ − 86
environment of Isabelle. It is therefore easy to experiment with what is
+ − 87
displayed. However, for better readability we will drop the enclosing
+ − 88
\isacommand{ML}~@{text "\<verbopen> \<dots> \<verbclose>"} and just write:
75
+ − 89
81
+ − 90
75
+ − 91
@{ML [display,gray] "3 + 4"}
+ − 92
89
+ − 93
Whenever appropriate we also show the response the code
81
+ − 94
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
+ − 95
@{text [quotes] ">"}, like:
75
+ − 96
+ − 97
@{ML_response [display,gray] "3 + 4" "7"}
+ − 98
195
+ − 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},
+ − 101
\isacommand{foobar} and so on). We use @{text "$ \<dots>"} to indicate that a
234
+ − 102
command needs to be run in a UNIX-shell, for example:
75
+ − 103
181
+ − 104
@{text [display] "$ grep -R ThyOutput *"}
75
+ − 105
89
+ − 106
Pointers to further information and Isabelle files are typeset in
195
+ − 107
\textit{italic} and highlighted as follows:
75
+ − 108
+ − 109
\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
+ − 110
Further information or pointers to files.
75
+ − 111
\end{readmore}
+ − 112
182
+ − 113
The pointers to Isabelle files are hyperlinked to the tip of the Mercurial
+ − 114
repository of Isabelle at \href{http://isabelle.in.tum.de/repos/isabelle/}
+ − 115
{http://isabelle.in.tum.de/repos/isabelle/}.
+ − 116
177
+ − 117
A few exercises are scattered around the text. Their solutions are given
156
+ − 118
in Appendix~\ref{ch:solutions}. Of course, you learn most, if you first try
162
+ − 119
to solve the exercises on your own, and then look at the solutions.
233
+ − 120
*}
156
+ − 121
233
+ − 122
section {* Naming Conventions in the Isabelle Sources *}
+ − 123
+ − 124
text {*
+ − 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
+ − 127
times.) The most important conventions are:
+ − 128
+ − 129
\begin{itemize}
234
+ − 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: @{ML_type cterm}
+ − 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: @{ML_type thm}
+ − 134
\item @{text "foo_tac"} for tactics; ML-type: @{ML_type tactic}
+ − 135
\item @{text thy} for theories; ML-type: @{ML_type theory}
+ − 136
\item @{text ctxt} for proof contexts; ML-type: @{ML_type Proof.context}
+ − 137
\item @{text lthy} for local theories; ML-type: @{ML_type local_theory}
+ − 138
\item @{text context} for generic contexts; ML-type @{ML_type Context.generic}
235
+ − 139
\item @{text mx} for mixfix syntax annotations; ML-type @{ML_type mixfix}
233
+ − 140
\end{itemize}
68
+ − 141
*}
+ − 142
119
+ − 143
section {* Acknowledgements *}
+ − 144
+ − 145
text {*
+ − 146
Financial support for this tutorial was provided by the German
122
+ − 147
Research Council (DFG) under grant number URB 165/5-1. The following
156
+ − 148
people contributed to the text:
119
+ − 149
+ − 150
\begin{itemize}
122
+ − 151
\item {\bf Stefan Berghofer} wrote nearly all of the ML-code of the
+ − 152
\simpleinductive-package and the code for the @{text
+ − 153
"chunk"}-antiquotation. He also wrote the first version of the chapter
+ − 154
describing the package and has been helpful \emph{beyond measure} with
+ − 155
answering questions about Isabelle.
119
+ − 156
+ − 157
\item {\bf Sascha Böhme} contributed the recipes in \ref{rec:timeout},
+ − 158
\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
+ − 159
He also wrote section \ref{sec:conversion} and helped with recipe \ref{rec:timing}.
119
+ − 160
+ − 161
\item {\bf Jeremy Dawson} wrote the first version of the chapter
+ − 162
about parsing.
+ − 163
180
+ − 164
\item {\bf Armin Heller} helped with recipe \ref{rec:sat}.
+ − 165
119
+ − 166
\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
+ − 167
chapter and also contributed the material on @{text NamedThmsFun}.
194
+ − 168
207
+ − 169
\item {\bf Christian Sternagel} proofread the tutorial and made
+ − 170
comments on the text.
119
+ − 171
\end{itemize}
+ − 172
121
+ − 173
Please let me know of any omissions. Responsibility for any remaining
153
+ − 174
errors lies with me.\bigskip
+ − 175
233
+ − 176
\vspace{5cm}
153
+ − 177
{\Large\bf
+ − 178
This document is still in the process of being written! All of the
192
+ − 179
text is still under construction. Sections and
153
+ − 180
chapters that are under \underline{heavy} construction are marked
+ − 181
with TBD.}
+ − 182
+ − 183
+ − 184
\vfill
+ − 185
This document was compiled with:\\
228
+ − 186
\input{version}\\
+ − 187
\input{pversion}
119
+ − 188
*}
2
+ − 189
153
+ − 190
+ − 191
195
+ − 192
end