theory Introimports Basebeginchapter {* 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.tex}} 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 {* Serious Isabelle ML-Programming *}text {* As already pointed out in the previous section, Isabelle is a joint effort of many developers. Therefore, disruptions that break the work of others are generally frowned upon. ``Accidents'' however do happen and everybody knows this. Still to keep them to a minimum, you can submit your changes first to a rather sophisticated \emph{testboard}, which will perform checks of your changes against the Isabelle repository and against the AFP. The advantage of the testboard is that the testing is performed by rather powerful machines saving you lengthy tests on, for example, your own laptop. You can see the results of the testboard at \begin{center} \url{http://isabelle.in.tum.de/testboard/Isabelle/} \end{center} which is organised like a Mercurial repository. A green point next to a change indicates that the change passes the corresponding tests (for this of course you have to allow some time). You can summit any changes to the testboard using the command @{text [display] "$ hg push -f ssh://...@hgbroy.informatik.tu-muenchen.de\\ //home/isabelle-repository/repos/testboard"} where the dots need to be replaced by your login name. Note that for pushing changes to the testboard you need to add the option @{text "-f"}, which should \emph{never} be used with the main Isabelle repository. While the testboard is a great system for supporting Isabelle developers, its disadvantage is that it needs login permissions for the computers in Munich. So in order to use it, you might have to ask other developers to obtain one.*}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, contributed exercise \ref{ex:contextfree} and contributed to the ``introspection'' of theorems in section \ref{sec:theorems}. \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 Rafal Kolanski} contributed to the ``introspection'' of theorems in section \ref{sec:theorems}. \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. \item {\bf Dmitriy Traytel} suggested to use the ML-antiquotation @{text "command_spec"} in section~\ref{sec:newcommand}, which simplified the code. \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.tex}\hspace{-0.5ex}) was compiled with:\\ %%\input{version.tex}\\ %% \input{pversion}*}end