author | paulson |

Tue Dec 18 16:14:56 2001 +0100 (2001-12-18) | |

changeset 12539 | 368414099877 |

parent 12538 | 150af0a4bb11 |

child 12540 | a5604ff1ef4e |

additional material

1.1 --- a/doc-src/TutorialI/preface.tex Tue Dec 18 16:14:50 2001 +0100 1.2 +++ b/doc-src/TutorialI/preface.tex Tue Dec 18 16:14:56 2001 +0100 1.3 @@ -1,10 +1,11 @@ 1.4 \chapter*{Preface} 1.5 \markboth{Preface}{Preface} 1.6 1.7 -This volume is a self-contained introduction to interactive proof using 1.8 -Isabelle/HOL\@. Compared with existing Isabelle documentation, it 1.9 -provides a straightforward route into higher-order logic, which most 1.10 -people prefer these days. It bypasses first-order logic and minimizes 1.11 +This volume is a self-contained introduction to interactive proof 1.12 +in higher-order logic (HOL), using the proof assistant Isabelle/HOL\@. 1.13 +Compared with existing Isabelle documentation, 1.14 +it provides a direct route into higher-order logic, which most people 1.15 +prefer these days. It bypasses first-order logic and minimizes 1.16 discussion of meta-theory. It is written for potential users rather 1.17 than for our colleagues in the research world. 1.18 1.19 @@ -16,20 +17,56 @@ 1.20 eight simplification tactics with a single method, namely \isa{simp}, 1.21 with associated options. 1.22 1.23 -\REMARK{mention Wenzel once author?} 1.24 +The book has three parts. 1.25 +\begin{itemize} 1.26 +\item 1.27 +The first part, \textbf{Basic Techniques}, 1.28 +shows how to model functional programs in higher-order logic. Early 1.29 +examples involve lists and the natural numbers. Most proofs 1.30 +are two steps long, consisting of induction on a chosen variable 1.31 +followed by the \isa{auto} tactic. But even this elementary part 1.32 +covers such advanced topics as nested and mutual recursion. 1.33 +\item 1.34 +The second part, \textbf{Logic and Sets}, presents a collection of 1.35 +lower-level tactics that you can use to apply rules selectively. It 1.36 +also describes Isabelle/HOL's treatment of sets, functions and 1.37 +relations and explains how to define sets inductively. One of the 1.38 +examples concerns the theory of model checking, and another is drawn 1.39 +from a classic textbook on formal languages. 1.40 +\item 1.41 +The third part, \textbf{Advanced Material}, describes a variety of 1.42 +other topics. Among these are the real numbers, records and 1.43 +overloading. Esoteric techniques are described involving induction and 1.44 +recursion. A whole chapter is devoted to an extended example: the 1.45 +verification of a security protocol. 1.46 +\end{itemize} 1.47 + 1.48 The typesetting relies on Wenzel's theory presentation tools. An 1.49 annotated source file is run, typesetting the theory 1.50 % and any requested Isabelle responses 1.51 in the form of a \TeX\ source file. This book is 1.52 derived almost entirely from output generated in this way. 1.53 1.54 +Isabelle's 1.55 +\href{http://www.cl.cam.ac.uk/Research/HVG/Isabelle/}{web site} 1.56 +contains links to the download area and to documentation and other 1.57 +information. Most Isabelle sessions are now run from within David 1.58 +Aspinall's wonderful user interface, 1.59 +\href{http://www.proofgeneral.org/}{Proof General}. This book says 1.60 +very little about Proof General, which has its own documentation. In 1.61 +order to run Isabelle, you will need a Standard ML compiler. We 1.62 +recommend \href{http://www.polyml.org/}{Poly/ML}, which is free and 1.63 +gives the best performance. The other supported compiler is 1.64 +\href{http://cm.bell-labs.com/cm/cs/what/smlnj/index.html}{Standard 1.65 +ML of New Jersey}. 1.66 + 1.67 This tutorial owes a lot to the constant discussions with and the valuable 1.68 feedback from the Isabelle group at Munich: Stefan Berghofer, Olaf 1.69 M{\"u}ller, Wolfgang Naraschewski, David von Oheimb, Leonor Prensa Nieto, 1.70 Cornelia Pusch, Norbert Schirmer, Martin Strecker and Markus Wenzel. Stephan 1.71 Merz was also kind enough to read and comment on a draft version. We 1.72 received comments from Stefano Bistarelli, Gergely Buday and Tanja 1.73 -Vos.\REMARK{incomplete list!} 1.74 +Vos. 1.75 1.76 The research has been funded by many sources, including the {\sc dfg} grants 1.77 Ni~491/2, Ni~491/3, Ni~491/4 and the {\sc epsrc} grants GR\slash K57381,