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