theory Intro+ −
imports Base+ −
+ −
begin+ −
+ −
+ −
chapter {* Introduction *}+ −
+ −
text {*+ −
If your next project requires you to program on the ML-level of Isabelle,+ −
then this Cookbook is for you. It will guide you through the first steps of+ −
Isabelle programming, and also explain tricks of the trade. The best way to+ −
get to know the ML-level of Isabelle is by experimenting with the many code+ −
examples included in the Cookbook. The code is as far as possible checked+ −
against recent versions of Isabelle. If something does not work, then+ −
please let us know. If you have comments, criticism or like to add to the+ −
Cookbook, feel free---you are most welcome!+ −
*}+ −
+ −
section {* Intended Audience and Prior Knowledge *}+ −
+ −
text {* + −
This Cookbook targets readers who already know how to use Isabelle for+ −
writing theories and proofs. We also assume that readers are familiar with+ −
the functional programming language ML, the language in which most of+ −
Isabelle is implemented. If you are unfamiliar with either of these two+ −
subjects, you should first work through the Isabelle/HOL tutorial+ −
\cite{isa-tutorial} or Paulson's book on ML \cite{paulson-ml2}.+ −
+ −
*}+ −
+ −
section {* Existing Documentation *}+ −
+ −
text {*+ −
+ −
The following documentation about Isabelle programming already exists (and is+ −
part of the distribution of Isabelle):+ −
+ −
\begin{description}+ −
\item[The Implementation Manual] describes Isabelle+ −
from a high-level perspective, documenting both the underlying+ −
concepts and some of the interfaces. + −
+ −
\item[The Isabelle Reference Manual] is an older document that used+ −
to be the main reference of Isabelle at a time when all proof scripts + −
were written on the ML-level. Many parts of this manual are outdated + −
now, but some parts, particularly the chapters on tactics, are still + −
useful.+ −
+ −
\item[The Isar Reference Manual] is also an older document that provides+ −
material about Isar and its implementation. Some material in it+ −
is still useful.+ −
\end{description}+ −
+ −
Then of course there is:+ −
+ −
\begin{description}+ −
\item[The code] is of course the ultimate reference for how+ −
things really work. Therefore you should not hesitate to look at the+ −
way things are actually implemented. More importantly, it is often+ −
good to look at code that does similar things as you want to do and+ −
to learn from other people's code.+ −
\end{description}+ −
+ −
*}+ −
+ −
section {* Typographic Conventions *}+ −
+ −
text {*+ −
+ −
All ML-code in this Cookbook is typeset in highlighted boxes, like the following + −
ML-expression:+ −
+ −
\begin{isabelle}+ −
\begin{graybox}+ −
\isacommand{ML}~@{text "\<verbopen>"}\isanewline+ −
\hspace{5mm}@{ML "3 + 4"}\isanewline+ −
@{text "\<verbclose>"}+ −
\end{graybox}+ −
\end{isabelle}+ −
+ −
These boxes corresponds to how code can be processed inside the interactive+ −
environment of Isabelle. It is therefore easy to experiment with what is + −
displayed. However, for better readability we will drop the enclosing + −
\isacommand{ML}~@{text "\<verbopen> \<dots> \<verbclose>"} and just write:+ −
+ −
+ −
@{ML [display,gray] "3 + 4"}+ −
+ −
Whenever appropriate we also show the response the code + −
generates when evaluated. This response is prefixed with a + −
@{text [quotes] ">"} like:+ −
+ −
@{ML_response [display,gray] "3 + 4" "7"}+ −
+ −
The usual user-level commands of Isabelle are written in bold, for + −
example \isacommand{lemma}, \isacommand{foobar} and so on. + −
We use @{text "$"} to indicate that a command needs to be run + −
in the Unix-shell, for example+ −
+ −
@{text [display] "$ ls -la"}+ −
+ −
Pointers to further information and Isabelle files are typeset in + −
italic and highlighted as follows:+ −
+ −
\begin{readmore}+ −
Further information or pointer to file.+ −
\end{readmore}+ −
+ −
*}+ −
+ −
+ −
end+ −