WARNING The printed book is out of date because it describes Isabelle 2002. It is strongly recommended to download its updated version which is part of the documentation of the latest Isabelle release. A new tutorial Programming and Proving in Isabelle/HOL is available with Isabelle 2012. It introduces Isabelle's structured proof language Isar missing from the tutorial below.
cover

Isabelle/HOL

A Proof Assistant for Higher-Order Logic

Tobias Nipkow
Lawrence C. Paulson
Markus Wenzel

This book is a self-contained introduction to interactive proof in higher-order logic (HOL), using the proof assistant Isabelle2002. It is a tutorial for potential users rather than a monograph for researchers.

The book has three parts.
  1. Elementary 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 auto tactic. But even this elementary part covers such advanced topics as nested and mutual recursion.
  2. 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.
  3. Advanced Material describes a variety of other topics. Among these are the real numbers, records and overloading. Advanced techniques are described involving induction and recursion. A whole chapter is devoted to an extended example: the verification of a security protocol.
It is published by Springer Verlag as volume 2283 of Lecture Notes in Computer Science in the Tutorials subseries.
  • Bibtex entry
  • Errata
    • I recommend it to anyone wanting to embark upon machine-supported proof in higher-order logic.
    (Simon Thompson in Computing Reviews)

    Tobias Nipkow