theory Introimports Basebeginchapter {* 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