Isabelle/Hol

by Nipkow, Tobias; Paulson, Lawrence C.; Wenzel, Markus

• ISBN13: 9783540433767
• ISBN10: 3540433767
• Format: Paperback
• Copyright: 2002-05-01
• Publisher: Springer Verlag

Summary

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.

Table of Contents

Part I. Elementary Techniques
The Basics	3	(6)
Introduction	3	(1)
Theories	4	(1)
Types, Terms, and Formulae	4	(3)
Variables	7	(1)
Interaction and Interfaces	7	(1)
Getting Started	8	(1)
Functional Programming in HOL	9	(18)
An Introductory Theory	9	(2)
An Introductory Proof	11	(4)
Some Helpful Commands	15	(2)
Datatypes	17	(5)
Lists	17	(1)
The General Format	17	(1)
Primitive Recursion	18	(1)
Case Expressions	18	(1)
Structural Induction and Case Distinction	19	(1)
Case Study: Boolean Expressions	19	(3)
Some Basic Types	22	(2)
Natural Numbers	22	(2)
Pairs	24	(1)
Datatype option	24	(1)
Definitions	24	(2)
Type Synonyms	25	(1)
Constant Definitions	25	(1)
The Definitional Approach	26	(1)
More Functional Programming	27	(26)
Simplification	27	(6)
What Is Simplification?	27	(1)
Simplification Rules	28	(1)
The simp Method	28	(1)
Adding and Deleting Simplification Rules	29	(1)
Assumptions	29	(1)
Rewriting with Definitions	30	(1)
Simplifying let-Expressions	31	(1)
Conditional Simplification Rules	31	(1)
Automatic Case Splits	31	(2)
Tracing	33	(1)
Induction Heuristics	33	(3)
Case Study: Compiling Expressions	36	(2)
Advanced Datatypes	38	(8)
Mutual Recursion	38	(2)
Nested Recursion	40	(2)
The Limits of Nested Recursion	42	(1)
Case Study: Tries	43	(3)
Total Recursive Functions	46	(7)
Defining Recursive Functions	46	(2)
Proving Termination	48	(1)
Simplification and Recursive Functions	49	(1)
Induction and Recursive Functions	50	(3)
Presenting Theories	53	(14)
Concrete Syntax	53	(4)
Infix Annotations	53	(1)
Mathematical Symbols	54	(1)
Prefix Annotations	55	(1)
Syntax Translations	56	(1)
Document Preparation	57	(10)
Isabelle Sessions	58	(1)
Structure Markup	59	(1)
Formal Comments and Antiquotations	60	(3)
Interpretation of Symbols	63	(1)
Suppressing Output	63	(4)
Part II. Logic and Sets
The Rules of the Game	67	(38)
Natural Deduction	67	(1)
Introduction Rules	68	(1)
Elimination Rules	69	(2)
Destruction Rules: Some Examples	71	(1)
Implication	72	(1)
Negation	73	(2)
Interlude: The Basic Methods for Rules	75	(1)
Unification and Substitution	76	(3)
Substitution and the subst Method	77	(1)
Unification and Its Pitfalls	78	(1)
Quantifiers	79	(6)
The Universal Introduction Rule	80	(1)
The Universal Elimination Rule	80	(2)
The Existential Quantifier	82	(1)
Renaming an Assumption: rename_tac	82	(1)
Reusing an Assumption: frule	83	(1)
Instantiating a Quantifier Explicitly	84	(1)
Description Operators	85	(2)
Definite Descriptions	85	(1)
Indefinite Descriptions	86	(1)
Some Proofs That Fail	87	(2)
Proving Theorems Using the blast Method	89	(1)
Other Classical Reasoning Methods	90	(2)
Forward Proof: Transforming Theorems	92	(4)
Modifying a Theorem Using of and THEN	93	(2)
Modifying a Theorem Using OF	95	(1)
Forward Reasoning in a Backward Proof	96	(3)
The Method insert	97	(1)
The Method subgoal_tac	98	(1)
Managing Large Proofs	99	(2)
Tacticals, or Control Structures	99	(1)
Subgoal Numbering	100	(1)
Proving the Correctness of Euclid's Algorithm	101	(4)
Sets, Functions, and Relations	105	(22)
Sets	105	(4)
Finite Set Notation	107	(1)
Set Comprehension	107	(1)
Binding Operators	108	(1)
Finiteness and Cardinality	109	(1)
Functions	109	(2)
Function Basics	109	(1)
Injections, Surjections, Bijections	110	(1)
Function Image	111	(1)
Relations	111	(3)
Relation Basics	112	(1)
The Reflexive and Transitive Closure	112	(1)
A Sample Proof	113	(1)
Well-Founded Relations and Induction	114	(2)
Fixed Point Operators	116	(1)
Case Study: Verified Model Checking	116	(11)
Propositional Dynamic Logic - PDL	118	(3)
Computation Tree Logic - CTL	121	(6)
Inductively Defined Sets	127	(22)
The Set of Even Numbers	127	(5)
Making an Inductive Definition	127	(1)
Using Introduction Rules	128	(1)
Rule Induction	128	(1)
Generalization and Rule Induction	129	(1)
Rule Inversion	130	(1)
Mutually Inductive Definitions	131	(1)
The Reflexive Transitive Closure	132	(3)
Advanced Inductive Definitions	135	(5)
Universal Quantifiers in Introduction Rules	135	(2)
Alternative Definition Using a Monotone Function	137	(1)
A Proof of Equivalence	138	(1)
Another Example of Rule Inversion	139	(1)
Case Study: A Context Free Grammar	140	(9)
Part III. Advanced Material
More about Types	149	(26)
Numbers	149	(6)
Numeric Literals	150	(1)
The Type of Natural Numbers, nat	151	(2)
The Type of Integers, int	153	(1)
The Type of Real Numbers, real	154	(1)
Pairs and Tuples	155	(3)
Pattern Matching with Tuples	155	(1)
Theorem Proving	156	(2)
Records	158	(6)
Record Basics	158	(1)
Extensible Records and Generic Operations	159	(2)
Record Equality	161	(2)
Extending and Truncating Records	163	(1)
Axiomatic Type Classes	164	(6)
Overloading	164	(3)
Axioms	167	(3)
Introducing New Types	170	(5)
Declaring New Types	171	(1)
Defining New Types	171	(4)
Advanced Simplification, Recursion, and Induction	175	(20)
Simplification	175	(3)
Advanced Features	175	(2)
How the Simplifier Works	177	(1)
Advanced Forms of Recursion	178	(8)
Beyond Measure	178	(2)
Recursion over Nested Datatypes	180	(2)
Partial Functions	182	(4)
Advanced Induction Techniques	186	(9)
Massaging the Proposition	186	(2)
Beyond Structural and Recursion Induction	188	(2)
Derivation of New Induction Schemas	190	(1)
CTL Revisited	191	(4)
Case Study: Verifying a Security Protocol	195	(12)
The Needham-Schroeder Public-Key Protocol	195	(2)
Agents and Messages	197	(1)
Modelling the Adversary	198	(1)
Event Traces	199	(1)
Modelling the Protocol	200	(1)
Proving Elementary Properties	201	(2)
Proving Secrecy Theorems	203	(4)
A. Appendix	207	(2)
Bibliography	209	(4)
Index	213