--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/ProgTutorial/Intro.thy Thu Mar 19 13:28:16 2009 +0100
@@ -0,0 +1,166 @@
+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 recent versions of Isabelle. If something does not work, then
+ please let us know. 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 is:
+
+ \begin{description}
+ \item[The code] is of course 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
+ to learn from that code. The UNIX command @{text "grep -R"} is
+ often your best friend while programming with Isabelle.
+ \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 corresponds 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 bold, for example \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
+ 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 {* 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 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}.
+ \end{itemize}
+
+ Please let me know of any omissions. Responsibility for any remaining
+ errors lies with me.\bigskip
+
+ {\Large\bf
+ This document is still in the process of being written! All of the
+ text is still under constructions. Sections and
+ chapters that are under \underline{heavy} construction are marked
+ with TBD.}
+
+
+ \vfill
+ This document was compiled with:\\
+ \input{version}
+*}
+
+
+
+end
\ No newline at end of file