# Isabelle/HOL: A Proof Assistant for Higher-Order Logic (Google eBook)

Tobias Nipkow, Lawrence C. Paulson, Markus Wenzel
Springer, Apr 3, 2002 - Computers - 218 pages
This textbook-like tutorial is a self-contained introduction to interactive proof, specification, and verification in higher-order logic, using the proof assistant Isabelle 2002. In contrast to existing Isabelle documentation, this book provides a direct route into higher-order logic by bypassing first-order logic and minimizing discussion of meta-theory.
Isabelle is a generic system for implementing logical formalisms, and Isabelle/HOL is the specialization of Isabelle for higher-order logic; this theorem prover is well suited as a specification and verification system.

### 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

### References from web pages

LNAI 4130 - Importing HOL into Isabelle/HOL
Importing HOL into Isabelle/HOL. Steven Obua. ⋆. and Sebastian Skalberg. Technische Universitat Munchen. D-85748 Garching, Boltzmannstr. 3, Germany ...

Integrating Isabelle/HOL with Specware
Integrating Isabelle/HOL with Specware. Stephen J. Westfold. Kestrel Institute, Palo Alto, California, USA. Abstract. Isabelle/HOL is integrated with ...
es.informatik.uni-kl.de/ TPHOLs-2007/ proceedings/ B-210.pdf

Isabelle/HOL. A Proof Assistant for Higher-Order Logic
Isabelle/HOL. A Proof Assistant for Higher-Order Logic. Tobias Nipkow · Lawrence C. Paulson · Markus Wenzel. This book is a self-contained introduction to ...
www.in.tum.de/ ~nipkow/ LNCS2283/

Isabelle HOL - The Tutorial - Nipkow, HOL (researchindex)
Ion over pairs and tuples is merely a convenient shorthand for a more complex internal representation. Thus the internal and external form of a term may ...
citeseer.ist.psu.edu/ 181281.html

Java Definite Assignment in Isabelle/HOL
Java Definite Assignment in Isabelle/HOL. ⋆. Norbert Schirmer. Technische Universitat Munchen. Department of Informatics. 80290 Munich, Germany ...
www4.informatik.tu-muenchen.de/ ~schirmer/ pub/ da-paper-ftfjp.pdf

Reasoning About CBV Functional Programs in Isabelle/HOL
Reasoning About CBV Functional Programs in. Isabelle/HOL. ⋆ ⋆⋆. John Longley and Randy Pollack. Edinburgh University, uk {rap,jrl}@inf.ed.ac.uk ...
homepages.inf.ed.ac.uk/ rpollack/ export/ LongleyPollack04.pdf

Isabelle (theorem prover) - Wikipedia, the free encyclopedia
... Computer Science 1349, Springer Verlag, 1997. Tobias Nipkow, Lawrence C. Paulson, Markus Wenzel: Isabelle/HOL - A Proof Assistant for Higher-Order Logic ...
en.wikipedia.org/ wiki/ Isabelle_theorem_prover

A Formal Correctness Proof for Code Generation from SSA Form in ...
A Formal Correctness Proof for Code Generation. from SSA Form in Isabelle/HOL. Jan Olaf Blech and Sabine Glesner. Institut fur Programmstrukturen und ...
pes.cs.tu-berlin.de/ pes/ uploads/ publikationen/ 79/ Blech-Glesner-ATPS-2004.pdf

Hoare logic for Java in Isabelle/HOL
CONCURRENCY AND COMPUTATION: PRACTICE AND EXPERIENCE. Concurrency Computat.: Pract. Exper. 2001; 13:1173–1214 (DOI: 10.1002/cpe.598). Hoare logic for Java ...
doi.wiley.com/ 10.1002/ cpe.598

Reasoning about Semantic Web in Isabelle/HOL
Reasoning about Semantic Web in Isabelle/HOL. Yue Tang. School of Computing. National University of Singapore. Republic of Singapore. tangy@comp.nus.edu.sg ...
www.cs.auckland.ac.nz/ ~jingsun/ papers/ PDFs/ APSEC.2004.46-53.pdf