Isabelle/HOL – A Proof Assistant for Higher-Order Logic

This volume is a self-contained introduction to interactive proof in higherorder logic (HOL), using the proof assistant Isabelle. It is written for potential users rather than for our colleagues in the research world. The book has three parts.

• The first part, Elementary Techniques, shows how to model functional programs in higher-order logic. Early examples involve lists and natural numbers. Most proofs are two steps long, consisting of induction on a chosen variable followed by the auto tactic. But even this elementary part covers such advanced topics as nested and mutual recursion.
• The second part, 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.
• The third part, 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.

The typesetting relies on Wenzel’s theory presentation tools. An annotated source file is run, typesetting the theory in the form of a LATEX source file. This book is derived almost entirely from the output generated in this way. The final chapter of Part I explains how users may produce their own formal documents in a similar fashion.

Isabelle’s website contains links to the download area and to documentation and other information. The classic Isabelle user interface is Proof General / Emacs by David Aspinall’s. This book says very little about Proof General, which has its own documentation.

This tutorial owes a lot to the constant discussions with and the valuable feedback from the Isabelle group at Munich: Stefan Berghofer, Olaf Müller, Wolfgang Naraschewski, David von Oheimb, Leonor Prensa Nieto, Cornelia Pusch, Norbert Schirmer, and Martin Strecker. Stephan Merz was also kind enough to read and comment on a draft version. We received comments from Stefano Bistarelli, Gergely Buday, John Matthews, and Tanja Vos