theory Intro

imports Base

begin

chapter {* Introduction *}

text {*

   \begin{flushright}

  {\em

  ``My thesis is that programming is not at the bottom of the intellectual \\

  pyramid, but at the top. It's creative design of the highest order. It \\

  isn't monkey or donkey work; rather, as Edsger Dijkstra famously \\

  claimed, it's amongst the hardest intellectual tasks ever attempted.''} \\[1ex]

  Richard Bornat, In Defence of Programming \cite{Bornat-lecture}

  \end{flushright}

  \medskip

  If your next project requires you to program on the ML-level of Isabelle,

  then this tutorial 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 tutorial. The code is as far as possible checked

  against the Isabelle distribution.\footnote{\input{version}} If something does not work, 

  then please let us know. It is impossible for us to know every environment, 

  operating system or editor in which Isabelle is used. If you have comments, 

  criticism or like to add to the tutorial, please feel free---you are most 

  welcome! The tutorial is meant to be gentle and comprehensive. To achieve 

  this we need your feedback.

*}

section {* Intended Audience and Prior Knowledge *}

text {* 

  This tutorial 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 Isabelle/Isar 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] provides specification material (like grammars,

  \end{description}

  Then of course there are:

  \begin{description}

  \item[The Isabelle sources.] They are 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

  learn from it. The UNIX command \mbox{@{text "grep -R"}} is

  often your best friend while programming with Isabelle, or

  hypersearch if you program using jEdit under MacOSX. To understand the sources,

  it is often also necessary to track the change history of a file or

  files. The Mercurial repository\footnote{\url{http://isabelle.in.tum.de/repos/isabelle/}} 

  for Isabelle  provides convenient interfaces to query the history of

  files and ``change sets''.

  \end{description}

*}

section {* Typographic Conventions *}

text {*

  All ML-code in this tutorial is typeset in shaded 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 correspond 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 user-level commands of Isabelle (i.e., the non-ML code) are written

  in \isacommand{bold face} (e.g., \isacommand{lemma}, \isacommand{apply},

  \isacommand{foobar} and so on).  We use @{text "$ \<dots>"} to indicate that a

  command needs to be run in a UNIX-shell, for example:

  @{text [display] "$ grep -R ThyOutput *"}

  Pointers to further information and Isabelle files are typeset in 

  \textit{italic} and highlighted as follows:

  \begin{readmore}

  Further information or pointers to files.

  \end{readmore}

  The pointers to Isabelle files are hyperlinked to the tip of the Mercurial

  repository of Isabelle at \href{http://isabelle.in.tum.de/repos/isabelle/}

  {http://isabelle.in.tum.de/repos/isabelle/}.

  A few exercises are scattered around the text. Their solutions are given 

  in Appendix~\ref{ch:solutions}. Of course, you learn most, if you first try

  to solve the exercises on your own, and then look at the solutions.

*}

section {* Aaaaargh! My Code Does not Work Anymore *}

text {*

  One unpleasant aspect of any code development inside a larger system is that

  one has to aim at a ``moving target''. The Isabelle system is no exception. Every 

  update lets potentially all hell break loose, because other developers have

  changed code you are relying on. Cursing is somewhat helpful in such situations, 

  but taking the view that incompatible code changes are a fact of life 

  might be more gratifying. Isabelle is a research project. In most circumstances 

  it is just impossible to make research backward compatible (imagine Darwin 

  attempting to make the Theory of Evolution backward compatible).

  However, there are a few steps you can take to mitigate unwanted interferences

  with code changes from other developers. First, you can base your code on the latest 

  stable release of Isabelle (it is aimed to have one such release at least 

  once every year). This 

  might cut you off from the latest feature

  implemented in Isabelle, but at least you do not have to track side-steps

  or dead-ends in the Isabelle development. Of course this means also you have

  to synchronise your code at the next stable release. Another possibility

  is to get your code into the Isabelle distribution. For this you have

  to convince other developers that your code or project is of general interest. 

  If you managed to do this, then the problem of the moving target goes 

  then maintenance is done by others. Unfortunately, this might not

  be a helpful advice for all types of projects. A lower threshold for inclusion has the 

  Archive of Formalised Proofs, short AFP.\footnote{\url{http://afp.sourceforge.net/}}

  This archive has been created mainly for formalisations that are

  interesting but not necessarily of general interest. If you have ML-code as

  part of a formalisation, then this might be the right place for you. There

  is no problem with updating your code after submission. At the moment

  developers are not as diligent with checking their code against the AFP than

  with checking agains the distribution, but generally problems will be caught

  and the developer, who caused them, is expected to fix them. So also

  in this case code maintenance is done for you. 

*}

section {* Some Naming Conventions in the Isabelle Sources *}

text {*

  There are a few naming conventions in the Isabelle code that might aid reading 

  and writing code. (Remember that code is written once, but read many 

  times.) The most important conventions are:

  \begin{itemize}

  \item @{text t}, @{text u} for (raw) terms; ML-type: @{ML_type term}

  \item @{text ct}, @{text cu} for certified terms; ML-type: @{ML_type cterm}

  \item @{text "ty"}, @{text T}, @{text U} for (raw) types; ML-type: @{ML_type typ}

  \item @{text th}, @{text thm} for theorems; ML-type: @{ML_type thm}

  \item @{text "foo_tac"} for tactics; ML-type: @{ML_type tactic}

  \item @{text thy} for theories; ML-type: @{ML_type theory}

  \item @{text ctxt} for proof contexts; ML-type: @{ML_type Proof.context}

  \item @{text lthy} for local theories; ML-type: @{ML_type local_theory}

  \item @{text context} for generic contexts; ML-type @{ML_type Context.generic}

  \item @{text mx} for mixfix syntax annotations; ML-type @{ML_type mixfix}

  \item @{text prt} for pretty printing; ML-type @{ML_type Pretty.T}

  \end{itemize}

*}

section {* Acknowledgements *}

text {*

  Financial support for this tutorial was provided by the German 

  Research Council (DFG) under grant number URB 165/5-1. The following

  people contributed to the text:

  \begin{itemize}

  \item {\bf Stefan Berghofer} wrote nearly all of the ML-code of the

  \simpleinductive-package and the code for the @{text

  "chunk"}-antiquotation. He also wrote the first version of this chapter

  describing the package and has been helpful \emph{beyond measure} with

  answering questions about Isabelle.

  \item {\bf Jasmin Blanchette} helped greatly with section \ref{sec:pretty}.

  \item {\bf Sascha Böhme} contributed the recipes in \ref{rec:timeout}, 

  \ref{rec:config}, \ref{rec:storingdata}, \ref{rec:external} and \ref{rec:oracle}.

  He also wrote section \ref{sec:conversion} and helped with recipe \ref{rec:timing}.

  \item {\bf Jeremy Dawson} wrote the first version of the chapter

  about parsing.

  \item {\bf Armin Heller} helped with recipe \ref{rec:sat}.

  \item {\bf Alexander Krauss} wrote the first version of the ``first-steps'' 

  chapter and also contributed the material on @{ML_functor Named_Thms}.

  \item {\bf Christian Sternagel} proofread the tutorial and made 

  many improvemets to the text. 

  \end{itemize}

  Please let me know of any omissions. Responsibility for any remaining

  errors lies with me.\bigskip

  \vspace{5cm}

  {\Large\bf

  This document is still in the process of being written! All of the

  text is still under construction. Sections and 

  chapters that are under \underline{heavy} construction are marked 

  with TBD.}

  \vfill

  This document was compiled with:\\

  \input{version}\\

  \input{pversion}

*}

end