Isabelle/HOL

This volume is a self-contained introduction to interactive proof in high- 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 ?rst-order logic and minimizes discussion of meta-theory. 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 l- ter make it easier to introduce new tactics on the ?y, but hardly anybody does that. Wenzel s dedicated syntax is elegant, replacing for example eight simpli?cation tactics with a single method, namely simp, with associated - tions. The book has three parts. The ?rst part, Elementary Techniques, shows how to model functional programs in higher-order logic. Early examples involve lists and the natural numbers. Most proofsare 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 I- belle/HOL s treatment of sets, functions, and relations and explains how to de?ne sets inductively. One of the examples concerns the theory of model checking, and another is drawn from a classic textbook on formal languages.