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 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 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.
Inhaltsverzeichnis
Elementary Techniques. - 1. The Basics. - 2. Functional Programming in HOL. - 3. More Functional Programming. - 4. Presenting Theories. - Logic and Sets. - 5. The Rules of the Game. - 6. Sets, Functions, and Relations. - 7. Inductively Defined Sets. - Advanced Material. - 8. More about Types. - 9. Advanced Simplification, Recursion, and Induction. - 10. Case Study: Verifying a Security Protocol.
