diff -r 8939b8fd8603 -r 069d525f8f1d CookBook/Intro.thy --- a/CookBook/Intro.thy Wed Mar 18 23:52:51 2009 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,166 +0,0 @@ -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 "\"}\isanewline - \hspace{5mm}@{ML "3 + 4"}\isanewline - @{text "\"} - \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 "\ \ \"} 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 "$ \"} 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