theory Intro+
−
imports Base+
−
begin+
−
+
−
chapter \<open>Introduction\<close>+
−
+
−
text \<open>+
−
   \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 Isabelle with ML,+
−
  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.+
−
  There is also a considerable amount of code written in Scala that allows+
−
  Isabelle interface with the Jedit GUI. Explanation of this part is beyond+
−
  this tutorial.+
−
+
−
  The best way to get to know the Isabelle/ML 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.+
−
\<close>+
−
+
−
section \<open>Intended Audience and Prior Knowledge\<close>+
−
+
−
text \<open>+
−
  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.+
−
+
−
  The rich Isabelle infrastructure can be categorized by various aspects @{cite "wenzel-technology"}:+
−
+
−
     @{emph \<open>@{bold \<open>Logic\<close>}\<close>} +
−
      \begin{description}+
−
        \item[Isabelle/Pure] is the logical Framework and bootstrap environment. The Pure logic+
−
          is used to represent rules for Higher-Order Natural Deduction declaratively. This allows+
−
          the implementation and definition of object logics like HOL using the Pure logic and+
−
          framework.+
−
        \item[Isabelle/HOL] is the main library of theories and tools for applications that is used +
−
          throughout this tutorial.+
−
      \end{description}+
−
+
−
     @{emph \<open>@{bold\<open>Programming\<close>}\<close>} +
−
      \begin{description}+
−
        \item[Isabelle/ML] is the Isabelle tool implementation and extension language. It is based+
−
          on Poly/ML\footnote{@{url \<open>http://polyml.org\<close>}}. Both Isabelle/Pure and Isabelle/ML emerge +
−
          from the same bootstrap process: the result is a meta-language for programming the logic+
−
          that is intertwined with it from a technological viewpoint, but logic and programming+
−
          remain formally separated.+
−
        \item[Isabelle/Scala] is the Isabelle system programming language. It connects the logical+
−
          environment with the outside world. Most notably resulting in the Prover IDE Isabelle/jEdit +
−
          and the command line tools.+
−
      \end{description}+
−
+
−
     @{emph \<open>@{bold\<open>Proof\<close>}\<close>} +
−
      \begin{description}+
−
        \item[Isabelle/Isar] is the structured proof language of the Isabelle framework. Isar +
−
          means, Intelligible semi-automated reasoning. +
−
        \item[Document language] for HTML output and \LaTeX type-setting of proof text. A proof+
−
          document combines formal and informal text to describe what has been proven to a general+
−
          audience.+
−
      \end{description}+
−
+
−
     @{emph \<open>@{bold\<open>IDE\<close>}\<close>} +
−
      \begin{description}+
−
        \item[Isabelle/jEdit] is the IDE for proof and tool development. It provides a rich interactive+
−
          frontend to the Isabelle framework in which logic and proof development, document creation as+
−
          well as ML programming are seamlessly integrated. +
−
      \end{description}+
−
\<close>+
−
+
−
section \<open>Existing Documentation\<close>+
−
+
−
text \<open>+
−
  The following documentation about Isabelle programming already exists (and is+
−
  part of the distribution of Isabelle):+
−
+
−
  \begin{description}+
−
  \item[The Isabelle/Isar Reference Manual] provides a top level view on the Isabelle system,+
−
  explaining general concepts and specification material (like grammars,+
−
  examples and so on) about Isabelle, Isar, Pure, HOL and the document language.+
−
+
−
  \item[The Isabelle/Isar Implementation Manual] describes Isabelle+
−
  implementation from a high-level perspective, documenting the major +
−
  underlying concepts and interfaces. +
−
+
−
  \item[Isabelle/jEdit] describes the IDE.+
−
+
−
  \item[The Old Introduction to Isabelle] is an older document that used+
−
  to be the main reference of Isabelle at a time when all proof scripts +
−
  were written with ML. Many parts of this manual are outdated +
−
  now, but some  parts, particularly the chapters on tactics, are still +
−
  useful.+
−
+
−
+
−
  \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. The best way is to interactively explore the sources+
−
  within the IDE provided by Isabelle/jEdit. By loading @{ML_file "Pure/ROOT.ML"}+
−
  into Isabelle/jEdit the sources of Pure are annotated with markup and you can+
−
  interactively follow the structure.+
−
  Moreover, the UNIX command \mbox{\<open>grep -R\<close>} or hypersearch within Isabelle/jEdit is+
−
  often your best friend while programming with Isabelle. 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}+
−
\<close>+
−
+
−
section \<open>Typographic Conventions\<close>+
−
+
−
text \<open>+
−
  All ML-code in this tutorial is typeset in shaded boxes, like the following +
−
  simple ML-expression:+
−
+
−
  \begin{isabelle}+
−
  \begin{graybox}+
−
  \isacommand{ML}~\<open>\<verbopen>\<close>\isanewline+
−
  \hspace{5mm}@{ML \<open>3 + 4\<close>}\isanewline+
−
  \<open>\<verbclose>\<close>+
−
  \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}~\<open>\<verbopen> \<dots> \<verbclose>\<close> and just+
−
  write:+
−
+
−
  @{ML [display,gray] \<open>3 + 4\<close>}+
−
  +
−
  Whenever appropriate we also show the response the code +
−
  generates when evaluated. This response is prefixed with a +
−
  @{text [quotes] ">"}, like:+
−
+
−
  @{ML_matchresult [display,gray] \<open>3 + 4\<close> \<open>7\<close>}+
−
+
−
  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 \<open>$ \<dots>\<close> 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.+
−
\<close>+
−
+
−
section \<open>How To Understand Isabelle Code\<close>+
−
+
−
text \<open>+
−
  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 and Isabelle/jEdit is an interactive programming environment, which means you can evaluate+
−
  code on the fly (for example inside an \isacommand{ML}~\<open>\<verbopen>\<dots>\<verbclose>\<close> 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}). Moreover, PolyML contains a debugger that is also supported from Isabelle/jEdit+
−
  with breakpoints and stack inspection.+
−
  Still it seems that+
−
  probing the code with explicit print statements is an 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.+
−
  Summarizing: +
−
  \begin{itemize}+
−
     \item Get familiar with the concepts and the applications by studying the Isabelle/Isar +
−
     reference manual and the rich set of theories and libraries in the standard distribution and the AFP.+
−
     \item Get familiar with the implementation and the best practices (like coding style, +
−
     canonical argument ordering, \<open>\<dots>\<close>) by reading the Isabelle/Isar implementation manual and by +
−
     browsing, reading and digesting both the code implementing a function as well and the +
−
     applications of that function.+
−
     \item Interactively experiment with the code.+
−
  \end{itemize}+
−
  +
−
\<close>+
−
+
−
+
−
section \<open>Aaaaargh! My Code Does not Work Anymore\<close>+
−
+
−
text \<open>+
−
  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.+
−
\<close>+
−
+
−
section \<open>Serious Isabelle ML-Programming\<close>+
−
+
−
text \<open>+
−
  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 \<open>-f\<close>,+
−
  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.+
−
\<close>+
−
+
−
+
−
section \<open>Some Naming Conventions in the Isabelle Sources\<close>+
−
+
−
text \<open>+
−
  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 \<open>t\<close>, \<open>u\<close>, \<open>trm\<close> for (raw) terms; ML-type: @{ML_type term}+
−
  \item \<open>ct\<close>, \<open>cu\<close> for certified terms; ML-type: @{ML_type cterm}+
−
  \item \<open>ty\<close>, \<open>T\<close>, \<open>U\<close> for (raw) types; ML-type: @{ML_type typ}+
−
  \item \<open>S\<close> for sorts; ML-type: @{ML_type sort}+
−
  \item \<open>th\<close>, \<open>thm\<close> for theorems; ML-type: @{ML_type thm}+
−
  \item \<open>foo_tac\<close> for tactics; ML-type: @{ML_type tactic}+
−
  \item \<open>thy\<close> for theories; ML-type: @{ML_type theory}+
−
  \item \<open>ctxt\<close> for proof contexts; ML-type: @{ML_type Proof.context}+
−
  \item \<open>lthy\<close> for local theories; ML-type: @{ML_type local_theory}+
−
  \item \<open>context\<close> for generic contexts; ML-type @{ML_type Context.generic}+
−
  \item \<open>mx\<close> for mixfix syntax annotations; ML-type @{ML_type mixfix}+
−
  \item \<open>prt\<close> for pretty printing; ML-type @{ML_type Pretty.T}+
−
  \item \<open>phi\<close> for morphisms; ML-type @{ML_type morphism}+
−
  \end{itemize}+
−
\<close>+
−
+
−
section \<open>Acknowledgements\<close>+
−
+
−
text \<open>+
−
  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 \<open>chunk\<close>-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\"ohme} 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 Florian Haftmann} helped with maintaining recipe \ref{rec:callml}.+
−
+
−
  \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_functor Named_Thms}.+
−
+
−
  %%\item {\bf Tobias Nipkow} contributed recipe \ref{rec:callml}.+
−
+
−
  \item {\bf Michael Norrish} proofread parts of the text.+
−
+
−
  \item {\bf Norbert Schirmer} updated the document to work with Isabelle 2018 and +
−
  later.+
−
+
−
  \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 +
−
  \<open>command_spec\<close> in section~\ref{sec:newcommand}, which simplified the code. +
−
+
−
  \item {\bf Piotr Trojanek} proofread 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.tex}\hspace{-0.5ex}) was compiled with:\\+
−
  %%\input{version.tex}\\+
−
  %% \input{pversion}+
−
\<close>+
−
+
−
end+
−