doc-src/TutorialI/preface.tex
 author wenzelm Wed Jul 25 12:38:54 2012 +0200 (2012-07-25) changeset 48497 ba61aceaa18a parent 47822 34b44d28fc4b permissions -rw-r--r--
some updates on "Building a repository version of Isabelle";
 paulson@11408  1 \chapter*{Preface}  paulson@11408  2 \markboth{Preface}{Preface}  paulson@11408  3 paulson@12539  4 This volume is a self-contained introduction to interactive proof  nipkow@16306  5 in higher-order logic (HOL), using the proof assistant Isabelle.  nipkow@16306  6 It is written for potential users rather  paulson@11408  7 than for our colleagues in the research world.  paulson@11408  8 paulson@12539  9 The book has three parts.  paulson@12539  10 \begin{itemize}  paulson@12539  11 \item  wenzelm@12669  12 The first part, \textbf{Elementary Techniques},  paulson@12539  13 shows how to model functional programs in higher-order logic. Early  paulson@12539  14 examples involve lists and the natural numbers. Most proofs  paulson@12539  15 are two steps long, consisting of induction on a chosen variable  paulson@12539  16 followed by the \isa{auto} tactic. But even this elementary part  paulson@12539  17 covers such advanced topics as nested and mutual recursion.  paulson@12539  18 \item  paulson@12539  19 The second part, \textbf{Logic and Sets}, presents a collection of  paulson@12539  20 lower-level tactics that you can use to apply rules selectively. It  paulson@12539  21 also describes Isabelle/HOL's treatment of sets, functions and  paulson@12539  22 relations and explains how to define sets inductively. One of the  paulson@12539  23 examples concerns the theory of model checking, and another is drawn  paulson@12539  24 from a classic textbook on formal languages.  paulson@12539  25 \item  nipkow@16306  26 The third part, \textbf{Advanced Material}, describes a variety of other  nipkow@16306  27 topics. Among these are the real numbers, records and overloading. Advanced  nipkow@16306  28 techniques for induction and recursion are described. A whole chapter is  nipkow@16306  29 devoted to an extended example: the verification of a security protocol.  paulson@12539  30 \end{itemize}  paulson@12539  31 nipkow@12327  32 The typesetting relies on Wenzel's theory presentation tools. An  nipkow@12327  33 annotated source file is run, typesetting the theory  wenzelm@12646  34 in the form of a \LaTeX\ source file. This book is derived almost entirely  wenzelm@12646  35 from output generated in this way. The final chapter of Part~I explains how  wenzelm@12646  36 users may produce their own formal documents in a similar fashion.  paulson@11408  37 wenzelm@47822  38 Isabelle's \hfootref{http://isabelle.in.tum.de/}{web site} contains  wenzelm@47822  39 links to the download area and to documentation and other information.  wenzelm@47822  40 The classic Isabelle user interface is Proof~General~/ Emacs by David  wenzelm@47822  41 Aspinall's\index{Aspinall, David}. This book says very little about  wenzelm@47822  42 Proof General, which has its own documentation.  paulson@12539  43 paulson@11408  44 This tutorial owes a lot to the constant discussions with and the valuable  nipkow@11547  45 feedback from the Isabelle group at Munich: Stefan Berghofer, Olaf  nipkow@11547  46 M{\"u}ller, Wolfgang Naraschewski, David von Oheimb, Leonor Prensa Nieto,  paulson@12812  47 Cornelia Pusch, Norbert Schirmer and Martin Strecker. Stephan  nipkow@11547  48 Merz was also kind enough to read and comment on a draft version. We  paulson@14179  49 received comments from Stefano Bistarelli, Gergely Buday, John Matthews  paulson@14179  50 and Tanja Vos.  paulson@11408  51 nipkow@11547  52 The research has been funded by many sources, including the {\sc dfg} grants  nipkow@16306  53 NI~491/2, NI~491/3, NI~491/4, NI~491/6, {\sc bmbf} project Verisoft, the {\sc  nipkow@16306  54 epsrc} grants GR/K57381, GR/K77051, GR/M75440, GR/R01156/01 GR/S57198/01 and  nipkow@16306  55 by the \textsc{esprit} working groups 21900 and IST-1999-29001 (the  nipkow@16306  56 \emph{Types} project).