theory Intro
imports Base
begin

chapter {* Introduction *}

text {*
  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. 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 code.\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 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, you should first work through the Isabelle/HOL tutorial
  \cite{isa-tutorial} or Paulson's book on ML \cite{paulson-ml2}.

*}

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 both the underlying
  concepts and some of the 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. It is currently in
  the process of being updated.
  \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. More importantly, it is often
  good to look at code that does similar things as you want to do and
  learn from it. The GNU/UNIX command \mbox{@{text "grep -R"}} is
  often your best friend while programming with Isabelle, or
  hypersearch if you program using jEdit under MacOSX.
  \end{description}

*}

section {* Typographic Conventions *}

text {*

  All ML-code in this tutorial is typeset in shaded boxes, like the following 
  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 what is 
  displayed. 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 ThyOutput *"}

  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}

  The pointers to Isabelle files are hyperlinked to the tip of the Mercurial
  repository of Isabelle at \href{http://isabelle.in.tum.de/repos/isabelle/}
  {http://isabelle.in.tum.de/repos/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 {* Some Naming Conventions in the Isabelle Sources *}

text {*
  There are a few naming conventions in Isabelle that might aid reading 
  and writing code. (Remember that code is written once, but read numerous 
  times.) The most important conventions are:

  \begin{itemize}
  \item @{text t}, @{text u} 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 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}
  \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 the chapter
  describing the package and has been helpful \emph{beyond measure} with
  answering questions about Isabelle.

  \item {\bf Jasmin Blanchette} helped greatly with section \ref{sec:pretty}.

  \item {\bf Sascha Böhme} contributed the recipes in \ref{rec:timeout}, 
  \ref{rec:config}, \ref{rec:storingdata}, \ref{rec:external} and \ref{rec:oracle}.
  He also wrote section \ref{sec:conversion} and helped with recipe \ref{rec:timing}.

  \item {\bf Jeremy Dawson} wrote the first version of the chapter
  about parsing.

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

  \item {\bf Alexander Krauss} wrote the first version of the ``first-steps'' 
  chapter and also contributed the material on @{text NamedThmsFun}.

  \item {\bf Christian Sternagel} proofread the tutorial and made 
  comments on the text. 
  \end{itemize}

  Please let me know of any omissions. Responsibility for any remaining
  errors lies with me.\bigskip

  \vspace{5cm}
  {\Large\bf
  This document 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 was compiled with:\\
  \input{version}\\
  \input{pversion}
*}



end