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

Front Cover
Tobias Nipkow, Lawrence C. Paulson, Markus Wenzel
Springer Science & Business Media, Apr 3, 2002 - Computers - 218 pages
0 Reviews
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

Common terms and phrases

References to this book

All Book Search results »