theory Intro

imports Base

begin

chapter {* Introduction *}

text {*

  The purpose of this Cookbook is to guide the reader through the first steps

  of Isabelle programming, and to explain tricks of the trade. The code

  provided in the Cookbook is as far as possible checked against recent

  versions of Isabelle.  If something does not work, then please let us

  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, to

  learn from other people's code.

  \end{description}

*}

section {* Typographic Conventions *}

text {*

  All ML-code in this Cookbook is typeset in highlighed boxes, like the following 

  ML-expression.

  \begin{isabelle}

  \begin{graybox}

  \isa{\isacommand{ML}

  \isacharverbatimopen\isanewline

  \hspace{5mm}@{ML "3 + 4"}\isanewline

  \isacharverbatimclose}

  \end{graybox}

  \end{isabelle}

  This corresponds to how code can be processed inside the interactive

  environment of Isabelle. It is therefore easy to experiment with the code

  (which by the way is highly recommended). However, for better readability we

  will drop the enclosing \isacommand{ML} \isa{\isacharverbatimopen \ldots

  \isacharverbatimclose} and just write

  @{ML [display,gray] "3 + 4"}

  for the code above. 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 Isabelle commands 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 on the Unix-command line, for example

  @{text [display] "$ ls -la"}

  Pointers to further information and Isabelle files are given 

  as follows:

  \begin{readmore}

  Further information or pointer to file.

  \end{readmore}

*}

end