1 theory Intro

     2 imports Base

     3 

     4 begin

     5 

     6 

     7 chapter {* Introduction *}

     8 

     9 text {*

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

    11   then this tutorial is for you. It will guide you through the first steps of

    12   Isabelle programming, and also explain tricks of the trade. The best way to

    13   get to know the ML-level of Isabelle is by experimenting with the many code

    14   examples included in the tutorial. The code is as far as possible checked

    15   against recent versions of Isabelle.  If something does not work, then

    16   please let us know. If you have comments, criticism or like to add to the

    17   tutorial, please feel free---you are most welcome! The tutorial is meant to be 

    18   gentle and comprehensive. To achieve this we need your feedback. 

    19 *}

    20 

    21 section {* Intended Audience and Prior Knowledge *}

    22 

    23 text {* 

    24   This tutorial targets readers who already know how to use Isabelle for

    25   writing theories and proofs. We also assume that readers are familiar with

    26   the functional programming language ML, the language in which most of

    27   Isabelle is implemented. If you are unfamiliar with either of these two

    28   subjects, you should first work through the Isabelle/HOL tutorial

    29   \cite{isa-tutorial} or Paulson's book on ML \cite{paulson-ml2}.

    30 

    31 *}

    32 

    33 section {* Existing Documentation *}

    34 

    35 text {*

    36   

    37   The following documentation about Isabelle programming already exists (and is

    38   part of the distribution of Isabelle):

    39 

    40   \begin{description}

    41   \item[The Isabelle/Isar Implementation Manual] describes Isabelle

    42   from a high-level perspective, documenting both the underlying

    43   concepts and some of the interfaces. 

    44 

    45   \item[The Isabelle Reference Manual] is an older document that used

    46   to be the main reference of Isabelle at a time when all proof scripts 

    47   were written on the ML-level. Many parts of this manual are outdated 

    48   now, but some  parts, particularly the chapters on tactics, are still 

    49   useful.

    50 

    51   \item[The Isar Reference Manual] provides specification material (like grammars,

    52   examples and so on) about Isar and its implementation. It is currently in

    53   the process of being updated.

    54   \end{description}

    55 

    56   Then of course there is:

    57 

    58   \begin{description}

    59   \item[The code] is of course the ultimate reference for how

    60   things really work. Therefore you should not hesitate to look at the

    61   way things are actually implemented. More importantly, it is often

    62   good to look at code that does similar things as you want to do and

    63   to learn from that code. The UNIX command @{text "grep -R"} is

    64   often your best friend while programming with Isabelle. 

    65   \end{description}

    66 

    67 *}

    68 

    69 section {* Typographic Conventions *}

    70 

    71 text {*

    72 

    73   All ML-code in this tutorial is typeset in shaded boxes, like the following 

    74   ML-expression:

    75 

    76   \begin{isabelle}

    77   \begin{graybox}

    78   \isacommand{ML}~@{text "\<verbopen>"}\isanewline

    79   \hspace{5mm}@{ML "3 + 4"}\isanewline

    80   @{text "\<verbclose>"}

    81   \end{graybox}

    82   \end{isabelle}

    83   

    84   These boxes corresponds to how code can be processed inside the interactive

    85   environment of Isabelle. It is therefore easy to experiment with what is 

    86   displayed. However, for better readability we will drop the enclosing 

    87   \isacommand{ML}~@{text "\<verbopen> \<dots> \<verbclose>"} and just write:

    88 

    89 

    90   @{ML [display,gray] "3 + 4"}

    91   

    92   Whenever appropriate we also show the response the code 

    93   generates when evaluated. This response is prefixed with a 

    94   @{text [quotes] ">"}, like:

    95 

    96   @{ML_response [display,gray] "3 + 4" "7"}

    97 

    98   The user-level commands of Isabelle (i.e.~the non-ML code) are written

    99   in bold, for example \isacommand{lemma}, \isacommand{apply},

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

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

   102 

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

   104 

   105   Pointers to further information and Isabelle files are typeset in 

   106   italic and highlighted as follows:

   107 

   108   \begin{readmore}

   109   Further information or pointers to files.

   110   \end{readmore}

   111 

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

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

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

   115 

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

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

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

   119 

   120 *}

   121 

   122 section {* Acknowledgements *}

   123 

   124 text {*

   125   Financial support for this tutorial was provided by the German 

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

   127   people contributed to the text:

   128 

   129   \begin{itemize}

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

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

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

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

   134   answering questions about Isabelle.

   135 

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

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

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

   139 

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

   141   about parsing.

   142 

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

   144 

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

   146   chapter and also contributed the material on @{text NamedThmsFun}.

   147   \end{itemize}

   148 

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

   150   errors lies with me.\bigskip

   151 

   152   {\Large\bf

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

   154   text is still under constructions. Sections and 

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

   156   with TBD.}

   157 

   158   

   159   \vfill

   160   This document was compiled with:\\

   161   \input{version}

   162 *}

   163 

   164 

   165 

   166 end