# HG changeset patch # User nipkow # Date 1118085654 -7200 # Node ID 8117e2037d3b668e22117408c4626feb1c6ac415 # Parent 5e7b6731b004b61ae9e481dad9bf486a07b96601 updating... diff -r 5e7b6731b004 -r 8117e2037d3b doc-src/TutorialI/basics.tex --- a/doc-src/TutorialI/basics.tex Mon Jun 06 19:09:49 2005 +0200 +++ b/doc-src/TutorialI/basics.tex Mon Jun 06 21:20:54 2005 +0200 @@ -77,24 +77,27 @@ constructs is found in the Isabelle/Isar Reference Manual~\cite{isabelle-isar-ref}. -HOL's theory collection is available online at -\begin{center}\small - \url{http://isabelle.in.tum.de/library/HOL/} -\end{center} -and is recommended browsing. Note that most of the theories -are based on classical Isabelle without the Isar extension. This means that -they look slightly different than the theories in this tutorial, and that all -proofs are in separate ML files. - \begin{warn} HOL contains a theory \thydx{Main}, the union of all the basic predefined theories like arithmetic, lists, sets, etc. Unless you know what you are doing, always include \isa{Main} as a direct or indirect parent of all your theories. \end{warn} +HOL's theory collection is available online at +\begin{center}\small + \url{http://isabelle.in.tum.de/library/HOL/} +\end{center} +and is recommended browsing. There is also a growing Library~\cite{HOL-Library}\index{Library} of useful theories that are not part of \isa{Main} but can be included -among the parents of a theory and will then be loaded automatically.% +among the parents of a theory and will then be loaded automatically. + +For the more adventurous, there is the \emph{Archive of Formal Proofs}, +a journal-like collection of more advanced Isabelle theories: +\begin{center}\small + \url{http://afp.sourceforge.net/} +\end{center} +We hope that you will contribute to it yourself one day.% \index{theories|)} @@ -137,18 +140,9 @@ the user, Isabelle infers the type of all variables automatically (this is called \bfindex{type inference}) and keeps quiet about it. Occasionally this may lead to misunderstandings between you and the system. If anything - strange happens, we recommend that you set the flag\index{flags} - \isa{show_types}\index{*show_types (flag)}. - Isabelle will then display type information - that is usually suppressed. Simply type -\begin{ttbox} -ML "set show_types" -\end{ttbox} - -\noindent -This can be reversed by \texttt{ML "reset show_types"}. Various other flags, -which we introduce as we go along, can be set and reset in the same manner.% -\index{flags!setting and resetting} + strange happens, we recommend that you ask Isabelle to display all type + information. This is best done through the Proof General interface; see + \S\ref{sec:interface} for details. \end{warn}% \index{types|)} @@ -308,6 +302,7 @@ \index{variables|)} \section{Interaction and Interfaces} +\label{sec:interface} Interaction with Isabelle can either occur at the shell level or through more advanced interfaces. To keep the tutorial independent of the interface, we @@ -320,16 +315,26 @@ Isabelle/Isar is the Emacs-based \bfindex{Proof General}~\cite{proofgeneral,Aspinall:TACAS:2000}. -Some interfaces (including the shell level) offer special fonts with -mathematical symbols. For those that do not, remember that \textsc{ascii}-equivalents -are shown in table~\ref{tab:ascii} in the appendix. +\begin{pgnote} +Proof General specific information is always displayed in paragraphs +identified by this miniature Proof General icon. -Finally, a word about semicolons.\indexbold{$Isar@\texttt{;}} -Commands may but need not be terminated by semicolons. -At the shell level it is advisable to use semicolons to enforce that a command -is executed immediately; otherwise Isabelle may wait for the next keyword -before it knows that the command is complete. +On particularly nice feature of Proof General is its support for a special +fonts with mathematical symbols. Most symbols have +\textsc{ascii}-equivalents: for example, you can enter either \verb!&! +or \verb!\! to obtain $\land$. For a list of the most frequent symbols +see table~\ref{tab:ascii} in the appendix. +\end{pgnote} +\begin{pgnote} +Proof General offers an \texttt{Isabelle} menu for displaying information +and setting flags. A particularly useful flag is \texttt{Show Types} +which causes Isabelle to output the type information that is usually +suppressed. This is indispensible in case of errors of all kinds +because often the types reveal the source of the problem. Once you have +diagnosed the problem you may no longer want to see the types because they +clutter all output. Simply reset the flag. +\end{pgnote} \section{Getting Started} diff -r 5e7b6731b004 -r 8117e2037d3b doc-src/TutorialI/preface.tex --- a/doc-src/TutorialI/preface.tex Mon Jun 06 19:09:49 2005 +0200 +++ b/doc-src/TutorialI/preface.tex Mon Jun 06 21:20:54 2005 +0200 @@ -2,20 +2,10 @@ \markboth{Preface}{Preface} This volume is a self-contained introduction to interactive proof -in higher-order logic (HOL), using the proof assistant Isabelle 2002. -Compared with existing Isabelle documentation, -it provides a direct route into higher-order logic, which most people -prefer these days. It bypasses first-order logic and minimizes -discussion of meta-theory. It is written for potential users rather +in higher-order logic (HOL), using the proof assistant Isabelle. +It is written for potential users rather than for our colleagues in the research world. -Another departure from previous documentation is that we describe Markus -Wenzel's proof script notation instead of ML tactic scripts. The latter -make it easier to introduce new tactics on the fly, but hardly anybody -does that. Wenzel's dedicated syntax is elegant, replacing for example -eight simplification tactics with a single method, namely \isa{simp}, -with associated options. - The book has three parts. \begin{itemize} \item @@ -33,16 +23,14 @@ examples concerns the theory of model checking, and another is drawn from a classic textbook on formal languages. \item -The third part, \textbf{Advanced Material}, describes a variety of -other topics. Among these are the real numbers, records and -overloading. Esoteric techniques are described involving induction and -recursion. A whole chapter is devoted to an extended example: the -verification of a security protocol. +The third part, \textbf{Advanced Material}, describes a variety of other +topics. Among these are the real numbers, records and overloading. Advanced +techniques for induction and recursion are described. A whole chapter is +devoted to an extended example: the verification of a security protocol. \end{itemize} The typesetting relies on Wenzel's theory presentation tools. An annotated source file is run, typesetting the theory -% and any requested Isabelle responses in the form of a \LaTeX\ source file. This book is derived almost entirely from output generated in this way. The final chapter of Part~I explains how users may produce their own formal documents in a similar fashion. @@ -57,8 +45,7 @@ In order to run Isabelle, you will need a Standard ML compiler. We recommend \hfootref{http://www.polyml.org/}{Poly/ML}, which is free and gives the best performance. The other fully supported compiler is -\hfootref{http://cm.bell-labs.com/cm/cs/what/smlnj/index.html}{Standard ML of - New Jersey}. +\hfootref{http://www.smlnj.org/index.html}{Standard ML of New Jersey}. This tutorial owes a lot to the constant discussions with and the valuable feedback from the Isabelle group at Munich: Stefan Berghofer, Olaf @@ -69,7 +56,7 @@ and Tanja Vos. The research has been funded by many sources, including the {\sc dfg} grants -Ni~491/2, Ni~491/3, Ni~491/4 and the {\sc epsrc} grants GR\slash K57381, -GR\slash K77051, GR\slash M75440, GR\slash R01156\slash 01 and by the -\textsc{esprit} working groups 21900 and IST-1999-29001 (the \emph{Types} -project). +NI~491/2, NI~491/3, NI~491/4, NI~491/6, {\sc bmbf} project Verisoft, the {\sc +epsrc} grants GR/K57381, GR/K77051, GR/M75440, GR/R01156/01 GR/S57198/01 and +by the \textsc{esprit} working groups 21900 and IST-1999-29001 (the +\emph{Types} project).