theory Intro+ −
imports Base+ −
begin+ −
+ −
(*<*)+ −
setup{*+ −
open_file_with_prelude + −
"Intro_Code.thy"+ −
["theory Intro", "imports Main", "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 {\em 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''. We also hope+ −
the tutorial will encourage students and researchers to play with Isabelle+ −
and implement new ideas. The source code of Isabelle can look intimidating,+ −
but beginners can get by with knowledge of only a handful of concepts, + −
a small number of functions and a few basic coding conventions.+ −
+ −
+ −
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 help and 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, then you should first work through the Isabelle/HOL tutorial+ −
\cite{isa-tutorial} or Paulson's book on ML \cite{paulson-ml2}. Recently,+ −
Isabelle has adopted a sizable amount of Scala code for a slick GUI+ −
based on jEdit. This part of the code is beyond the interest of this+ −
tutorial, since it mostly does not concern the regular Isabelle + −
developer.+ −
*}+ −
+ −
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 some of the underlying+ −
concepts and 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,+ −
examples and so on) about Isar and its implementation.+ −
\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. While much of the Isabelle+ −
code is uncommented, some parts have very helpful comments---particularly+ −
the code about theorems and terms. Despite the lack of comments in most+ −
parts, it is often good to look at code that does similar things as you + −
want to do and learn from it. + −
This tutorial contains frequently pointers to the+ −
Isabelle sources. Still, the UNIX command \mbox{@{text "grep -R"}} is+ −
often your best friend while programming with Isabelle.\footnote{Or+ −
hypersearch if you work with jEdit.} 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 + −
simple 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 the code+ −
that is shown in this tutorial. 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 Thy_Output *"}+ −
+ −
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}+ −
+ −
Note that pointers to Isabelle files are hyperlinked to the tip of the Mercurial+ −
repository at \href{http://isabelle.in.tum.de/repos/isabelle/}+ −
{http://isabelle.in.tum.de/repos/isabelle/}, not the latest stable release+ −
of 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 {* How To Understand Isabelle Code *}+ −
+ −
text {*+ −
One of the more difficult aspects of any kind of programming is to+ −
understand code written by somebody else. This is aggravated in Isabelle by+ −
the fact that many parts of the code contain none or only few+ −
comments. There is one strategy that might be helpful to navigate your way:+ −
ML is an interactive programming environment, which means you can evaluate+ −
code on the fly (for example inside an \isacommand{ML}~@{text+ −
"\<verbopen>\<dots>\<verbclose>"} section). So you can copy (self-contained)+ −
chunks of existing code into a separate theory file and then study it+ −
alongside with examples. You can also install ``probes'' inside the copied+ −
code without having to recompile the whole Isabelle distribution. Such+ −
probes might be messages or printouts of variables (see chapter+ −
\ref{chp:firststeps}). Although PolyML also contains a debugger, it seems+ −
probing the code with explicit print statements is the most effective method+ −
for understanding what some piece of code is doing. However do not expect+ −
quick results with this! It is painful. Depending on the size of the code+ −
you are looking at, you will spend the better part of a quiet afternoon with+ −
it. And there seems to be no better way for understanding code in Isabelle.+ −
*}+ −
+ −
+ −
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''. Isabelle is no exception of this. 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. If+ −
you do not synchronise, be warned that code seems to ``rot'' very+ −
quickly. 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 away, because when checking in new code,+ −
developers are strongly urged to test it against Isabelle's code base. If+ −
your project is part of that code base, 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 Formal+ −
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}, @{text trm} 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 "S"} for sorts; ML-type: @{ML_type sort}+ −
\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}+ −
\item @{text phi} for morphisms; ML-type @{ML_type morphism}+ −
\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 chapter+ −
\ref{chp:package} describing this package and has been helpful \emph{beyond+ −
measure} with answering questions about Isabelle.+ −
+ −
\item {\bf Jasmin Blanchette} helped greatly with section \ref{sec:pretty}+ −
and exercise \ref{fun:killqnt}.+ −
+ −
\item {\bf Sascha Böhme} contributed the recipes in \ref{rec:timeout}, + −
\ref{rec:external} and \ref{rec:oracle}. He also wrote section \ref{sec:conversion} + −
and helped with recipe \ref{rec:timing}. Parts of section \ref{sec:storing}+ −
are by him.+ −
+ −
\item {\bf Lukas Bulwahn} made me aware of a problem with recursive+ −
parsers and contributed exercise \ref{ex:contextfree}.+ −
+ −
\item {\bf Jeremy Dawson} wrote the first version of chapter \ref{chp:parsing}+ −
about parsing.+ −
+ −
\item {\bf Armin Heller} helped with recipe \ref{rec:sat}.+ −
+ −
\item {\bf Alexander Krauss} wrote a very early version of the ``first-steps'' + −
chapter and also contributed the material on @{ML_funct Named_Thms}.+ −
+ −
\item {\bf Tobias Nipkow} contributed recipe \ref{rec:callml}.+ −
+ −
\item {\bf Michael Norrish} proofread parts of the text.+ −
+ −
\item {\bf Andreas Schropp} improved and corrected section \ref{sec:univ} and+ −
contributed towards section \ref{sec:sorts}.+ −
+ −
\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+ −
+ −
\newpage+ −
\mbox{}\\[5cm]+ −
+ −
+ −
{\Large\bf+ −
This tutorial 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 (version \input{tip}\hspace{-0.5ex}) was compiled with:\\+ −
\input{version}\\+ −
%%\input{pversion}+ −
*}+ −
+ −
end+ −