# Isabelle/HOL: A Proof Assistant for Higher-Order Logic

Springer Science & Business Media, Apr 3, 2002 - Computers - 218 pages
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.

### What people are saying -Write a review

We haven't found any reviews in the usual places.

### Contents

 1 The Basics 3 12 Theories 4 14 Variables 7 16 Getting Started 8 2 Functional Programming in HOL 9 22 An Introductory Proof 11 23 Some Helpful Commands 15 24 Datatypes 17
 5152 The Method subgoal_tac 98 516 Managing Large Proofs 99 5162 Subgoal Numbering 100 517 Proving the Correctness of Euclids Algorithm 101 6 Sets Functions and Relations 105 611 Finite Set Notation 107 613 Binding Operators 108 614 Finiteness and Cardinality 109

 243 Primitive Recursion 18 245 Structural Induction and Case Distinction 19 25 Some Basic Types 22 252 Pairs 24 261 Type Synonyms 25 27 The Definitional Approach 26 3 More Functional Programming 27 312 Simplification Rules 28 314 Adding and Deleting Simplification Rules 29 316 Rewriting with Definitions 30 317 Simplifying letExpressions 31 3110 Tracing 33 Compiling Expressions 36 34 Advanced Datatypes 38 342 Nested Recursion 40 343 The Limits of Nested Recursion 42 Tries 43 35 Total Recursive Functions 46 352 Proving Termination 48 353 Simplification and Recursive Functions 49 354 Induction and Recursive Functions 50 4 Presenting Theories 53 412 Mathematical Symbols 54 413 Prefix Annotations 55 414 Syntax Translations 56 42 Document Preparation 57 421 Isabelle Sessions 58 422 Structure Markup 59 423 Formal Comments and Antiquotations 60 424 Interpretation of Symbols 63 Logic and Sets 65 5 The Rules of the Game 67 52 Introduction Rules 68 53 Elimination Rules 69 Some Examples 71 55 Implication 72 56 Negation 73 The Basic Methods for Rules 75 58 Unification and Substitution 76 581 Substitution and the subst Method 77 582 Unification and Its Pitfalls 78 59 Quantifiers 79 591 The Universal Introduction Rule 80 593 The Existential Quantifier 82 frule 83 596 Instantiating a Quantifier Explicitly 84 510 Description Operators 85 5102 Indefinite Descriptions 86 511 Some Proofs That Fail 87 512 Proving Theorems Using the blast Method 89 513 Other Classical Reasoning Methods 90 Transforming Theorems 92 5141 Modifying a Theorem Using of and THEN 93 5142 Modifying a Theorem Using OF 95 515 Forward Reasoning in a Backward Proof 96 5151 The Method insert 97
 622 Injections Surjections Bijections 110 623 Function Image 111 631 Relation Basics 112 633 A Sample Proof 113 64 WeilFounded Relations and Induction 114 Verified Model Checking 116 661 Prepositional Dynamic Logic PDL 118 662 Computation Tree Logic CTL 121 7 Inductively Defined Sets 127 712 Using Introduction Rules 128 714 Generalization and Rule Induction 129 715 Rule Inversion 130 716 Mutually Inductive Definitions 131 72 The Reflexive Transitive Closure 132 73 Advanced Inductive Definitions 135 732 Alternative Definition Using a Monotone Function 137 733 A Proof of Equivalence 138 734 Another Example of Rule Inversion 139 A Context Free Grammar 140 Advanced Material 147 8 More about Types 149 811 Numeric Literals 150 812 The Type of Natural Numbers nat 151 813 The Type of Integers int 153 814 The Type of Real Numbers real 154 82 Pairs and Tuples 155 822 Theorem Proving 156 83 Records 158 832 Extensible Records and Generic Operations 159 833 Record Equality 161 834 Extending and Truncating Records 163 84 Axiomatic Type Classes 164 842 Axioms 167 Fig 81 Subclass Diagram 170 851 Declaring New Types 171 9 Advanced Simplification Recursion and Induction 175 912 How the Simplifier Works 177 92 Advanced Forms of Recursion 178 922 Recursion over Nested Datatypes 180 923 Partial Functions 182 93 Advanced Induction Techniques 186 932 Beyond Structural and Recursion Induction 188 933 Derivation of New Induction Schemas 190 934 CTL Revisited 191 Verifying a Security Protocol 195 102 Agents and Messages 197 103 Modelling the Adversary 198 104 Event Traces 199 105 Modelling the Protocol 200 106 Proving Elementary Properties 201 107 Proving Secrecy Theorems 203 A Appendix 207 Bibliography 209 Index 213 Copyright