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