<commit_before>\chapter*{Preface}
\markboth{Preface}{Preface}

This volume is a self-contained introduction to interactive proof
in higher-order logic (HOL), using the proof assistant Isabelle/HOL\@. 
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
than for our colleagues in the research world.

\index{Wenzel, Markus}%
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 
The first part, \textbf{Basic Techniques},
shows how to model functional programs in higher-order logic.  Early
examples involve lists and the natural numbers.  Most proofs
are two steps long, consisting of induction on a chosen variable
followed by the \isa{auto} tactic.  But even this elementary part
covers such advanced topics as nested and mutual recursion.
\item 
The second part, \textbf{Logic and Sets}, presents a collection of
lower-level tactics that you can use to apply rules selectively.  It
also describes Isabelle/HOL's treatment of sets, functions and
relations and explains how to define sets inductively.  One of the
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.
\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 end of Part~I explains how users may produce their own formal documents in
the same manner.

Isabelle's
\hfootref{http://isabelle.in.tum.de/}{web site}
contains links to the download area and to documentation and other
information.  Most Isabelle sessions are now run from within David
Aspinall's wonderful user interface,
\hfootref{http://www.proofgeneral.org/}{Proof General}.  This book says
very little about Proof General, which has its own documentation.  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}.<commit_msg>mention X-Symbol; \index{Aspinall, David};<commit_after>\chapter*{Preface}
\markboth{Preface}{Preface}

This volume is a self-contained introduction to interactive proof
in higher-order logic (HOL), using the proof assistant Isabelle/HOL\@. 
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
than for our colleagues in the research world.

\index{Wenzel, Markus}%
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 
The first part, \textbf{Basic Techniques},
shows how to model functional programs in higher-order logic.  Early
examples involve lists and the natural numbers.  Most proofs
are two steps long, consisting of induction on a chosen variable
followed by the \isa{auto} tactic.  But even this elementary part
covers such advanced topics as nested and mutual recursion.
\item 
The second part, \textbf{Logic and Sets}, presents a collection of
lower-level tactics that you can use to apply rules selectively.  It
also describes Isabelle/HOL's treatment of sets, functions and
relations and explains how to define sets inductively.  One of the
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.
\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 end of Part~I explains how users may produce their own formal documents in
the same manner.

Isabelle's \hfootref{http://isabelle.in.tum.de/}{web site} contains links to
the download area and to documentation and other information.  Most Isabelle
sessions are now run from within David Aspinall's\index{Aspinall, David}
wonderful user interface, \hfootref{http://www.proofgeneral.org/}{Proof
  General}, even together with the
\hfootref{http://www.fmi.uni-passau.de/~wedler/x-symbol/}{X-Symbol} package
for XEmacs.  This book says very little about Proof General, which has its own
documentation.  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}.
{'fraction_non_alphanumeric': 0.05786561264822134, 'fraction_numerical': 0.0, 'mean_word_length': 4.719710669077758, 'pattern_counts': {'":': 0, '<': 3, '<?xml version=': 0, '>': 3, 'https://': 0, 'lorem ipsum': 0, 'www.': 5, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 2, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '6411894', 'n_tokens_mistral': 1685, 'n_tokens_neox': 1609, 'n_words': 855}