author nipkow Mon, 06 Jun 2005 21:20:54 +0200 changeset 16306 8117e2037d3b parent 16305 5e7b6731b004 child 16307 cb0f9e96d456
updating...
 doc-src/TutorialI/basics.tex file | annotate | diff | comparison | revisions doc-src/TutorialI/preface.tex file | annotate | diff | comparison | revisions
--- 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!\<and>! 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}

--- 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
-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
+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).