Isabelle/HOL: A Proof Assistant for Higher-Order Logic (Lecture Notes in Computer Science, 2283)

Lecture Notes in Computer Science
Springer
Isabelle/HOL
In memoriam Annette Schumann 1959 – 2001
Preface
Table of Contents
	Part I. Elementary Techniques
		The Basics
		Functional Programming in HOL
		More Functional Programming
		Presenting Theories
	Part II. Logic andSets
		The Rules of the Game
		Sets, Functions, andR elations
		Inductively Defined Sets
	Part III. Advanced Material
		More about Types
		Advanced Simplification, Recursion, and Induction
		Case Study: Verifying a Security Protocol
	A. Appendix
	Bibliography
1.The Basics
	1.1 Introduction
	1.2 Theories
	1.3 Types, Terms, and Formulae
	1.4 Variables
	1.5 Interaction and Interfaces
	1.6 Getting Started
2. Functional Programming in HOL
	2.1 An Introductory Theory
	2.2 An Introductory Proof
	2.3 Some Helpful Commands
	2.4 Datatypes
		2.4.1 Lists
		2.4.2 The General Format
		2.4.3 Primitive Recursion
		2.4.4 Case Expressions
		2.4.5 Structural Induction and Case Distinction
		2.4.6 Case Study: Boolean Expressions
	2.5 Some Basic Types
		2.5.1 Natural Numbers
		2.5.2 Pairs
		2.5.3 Datatype option
	2.6 Definitions
		2.6.1 Type Synonyms
		2.6.2 Constant Definitions
	2.7 The Definitional Approach
3. More Functional Programming
	3.1 Simplification
		3.1.1 What Is Simplification?
		3.1.2 Simplification Rules
		3.1.3 The simp Method
		3.1.4A dding and Deleting Simplification Rules
		3.1.5 Assumptions
		3.1.6 Rewriting with Definitions
		3.1.7 Simplifying let-Expressions
		3.1.9 Automatic Case Splits
		3.1.10 Tracing
	3.2 Induction Heuristics
	3.3 Case Study: Compiling Expressions
	3.4 Advanced Datatypes
		3.4.1 Mutual Recursion
		3.4.2 Nested Recursion
		3.4.3 The Limits of Nested Recursion
		3.4.4 Case Study: Tries
	3.5 Total Recursive Functions
		3.5.1 Defining Recursive Functions
		3.5.2 Proving Termination
		3.5.3 Simplification and Recursive Functions
		3.5.4Inducti on and Recursive Functions
4. Presenting Theories
	4.1 Concrete Syntax
		4.1.1 Infix Annotations
		4.1.2 Mathematical Symbols
		4.1.3 Prefix Annotations
		4.1.4 Syntax Translations
	4.2 Document Preparation
		4.2.1 Isabelle Sessions
		4.2.2 Structure Markup
		4.2.3 Formal Comments and Antiquotations
		4.2.4 Interpretation of Symbols
		4.2.5 Suppressing Output
5. The Rules of the Game
	5.1 Natural Deduction
	5.2 Introduction Rules
	5.3 Elimination Rules
	5.4 Destruction Rules: Some Examples
	5.5 Implication
	5.6 Negation
	5.7 Interlude: The Basic Methods for Rules
	5.8 Unification and Substitution
	5.8.1 Substitution and the subst Method
	5.8.2 Unification and Its Pitfalls
	5.9 Quantifiers
		5.9.1 The Universal Introduction Rule
		5.9.2 The Universal Elimination Rule
		5.9.3 The Existential Quantifier
		5.9.4 Renaming an Assumption: rename_tac
		5.9.5 Reusing an Assumption: frule
		5.9.6 Instantiating a Quantifier Explicitly
	5.10 Description Operators
		5.10.1 Definite Descriptions
		5.10.2 Indefinite Descriptions
	5.11 Some Proofs That Fail
	5.12 Proving Theorems Using the blast Method
	5.13 Other Classical Reasoning Methods
	5.14 Forward Proof: Transforming Theorems
		5.14.1 Modifying a Theorem Using of and THEN
		5.14.2 Modifying a Theorem Using OF
	5.15 Forward Reasoning in a Backward Proof
	5.15.1 The Method insert
	5.15.2 The Method subgoal_tac
	5.16 Managing Large Proofs
		5.16.1 Tacticals, or Control Structures
		5.16.2 Subgoal Numbering
	5.17 Proving the Correctness of Euclid’s Algorithm
6. Sets, Functions, and Relations
	6.1 Sets
		6.1.1 Finite Set Notation
		6.1.2 Set Comprehension
		6.1.3 Binding Operators
		6.1.4 Finiteness and Cardinality
	6.2 Functions
		6.2.1 Function Basics
		6.2.2 Injections, Surjections, Bijections
		6.2.3 Function Image
	6.3 Relations
		6.3.1 Relation Basics
		6.3.2 The Reflexive and Transitive Closure
		6.3.3 A Sample Proof
	6.4 Well-Founded Relations and Induction
	6.5 Fixed Point Operators
	6.6 Case Study: Verified Model Checking
		6.6.1 Propositional Dynamic Logic — PDL
		6.6.2 Computation Tree Logic — CTL
7. Inductively Defined Sets
	7.1 The Set of Even Numbers
		7.1.1 Making an Inductive Definition
		7.1.2 Using Introduction Rules
		7.1.3 Rule Induction
		7.1.4 Generalization and Rule Induction
		7.1.5 Rule Inversion
		7.1.6Mutual ly Inductive Definitions
	7.2 The Reflexive Transitive Closure
	7.3 Advanced Inductive Definitions
		7.3.1 Universal Quantifiers in Introduction Rules
		7.3.2 Alternative Definition Using a Monotone Function
		7.3.3 A Proof of Equivalence
		7.3.4 Another Example of Rule Inversion
	7.4 Case Study:A Context Free Grammar
8. More about Types
	8.1 Numbers
		8.1.1 Numeric Literals
		8.1.2 The Type of Natural Numbers, nat
		8.1.3 The Type of Integers, int
		8.1.4 The Type of Real Numbers, real
	8.2 Pairs and Tuples
		8.2.1 Pattern Matching with Tuples
		8.2.2 Theorem Proving
	8.3 Records
		8.3.1 Record Basics
		8.3.2 Extensible Records and Generic Operations
		8.3.3 Record Equality
		8.3.4 Extending and Truncating Records
	8.4 Axiomatic Type Classes
		8.4.1 Overloading
		8.4.2 Axioms
	8.5 Introducing New Types
		8.5.1 Declaring New Types
		8.5.2 Defining New Types
9. Advanced Simplification, Recursion, and Induction
	9.1 Simplification
		9.1.1 Advanced Features
		9.1.2 How the Simplifier Works
	9.2 Advanced Forms of Recursion
		9.2.1 Beyond Measure
		9.2.2 Recursion over Nested Datatypes
		9.2.3 Partial Functions
	9.3 Advanced Induction Techniques
		9.3.1 Massaging the Proposition
		9.3.2 Beyond Structural and Recursion Induction
		9.3.3 Derivation of New Induction Schemas
		9.3.4 CTL Revisited
10. Case Study: Verifying a Security Protocol
	10.1 The Needham-Schroeder Public-Key Protocol
	10.2 Agents and Messages
	10.3 Modelling the Adversary
	10.4 Event Traces
	10.5 Modelling the Protocol
	10.6 Proving Elementary Properties
	10.7 Proving Secrecy Theorems
A. Appendix
Bibliography
Index