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

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

Related books

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

Other editions - View all

Common terms and phrases

References to this book

All Book Search results »

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 ...
www.springerlink.com/ index/ m7621r5258r8n711.pdf

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