Interactive Proof: Introduction to Isabelle/HOL
This paper introduces interactive theorem proving with the Isabelle/HOL system. The following topics are covered:
- Verified functional programming: The logic HOL contains an ML-style
functional programming language. It is shown how to verify
functional programs in this language by induction and simplification.
-
Predicate logic: Formulas of predicate logic and set theory are
introduced, together with methods for proof automation.
- Inductively defined predicates.
-
Structured proofs: We introduce the proof language Isar and show how
to write structured proofs that are readable by both the machine and
the human.
We assume basic familiarity with some functional programming
language of the ML or Haskell family, in particular with recursive
data types and pattern matching. No specific background in logic is
necessary beyond the ability to read predicate logic formulas.
BibTeX:
@inproceedings{Nipkow-MOD2011,author={Tobias Nipkow},
title={Interactive Proof: Introduction to {Isabelle/HOL}},
booktitle={Software Safety and Security},
publisher={IOS Press},editor={O. Grumberg and T. Nipkow and B. Hauptmann},
pages={254--285},year=2012}
This article is superseded by the manual
Programming and Proving in Isabelle/HOL.