Theorem Proving with Isabelle/HOL
An Intensive Course
Overview
This course is an introduction to theorem proving with the Isabelle/HOL
system. It is largely based on the book
Isabelle/HOL — A Proof Assistant for Higher-Order Logic
and covers the most important definition mechanisms and proof methods.
The course ends with an introduction to Isar, Isabelle's
structured proof language.
The course is aimed at students who are seriously interested in becoming
acquainted with computer-assisted theorem proving. It combines a practical
how-to approach with the necessary logical background material. At the end of
the course students are able to define and reason about functional programs,
logical and set-theoretic formulae, and simple mathematical models of
discrete systems (for example in a set-theoretic style).
No prior background in theorem proving is required, but familiarity with and
a basic understanding of logical and mathematical notation and some minimal
exposure to functional programming is assumed.
Contents
The course is divided into 8 sessions of roughly 90 minutes each (at a quick
pace):
- Basic notation. Recursion and induction on lists.
In the first half of the session the syntax of terms and types in HOL is
introduced. This is followed by a prototypical example of recursion and
induction on lists: the append and reverse functions are defined and
rev(rev xs) = xs is proved. This introduces the proof methods
induct and auto and allows students to start with
proofs about lists.
- Datatypes and primitive recursive functions
A thorough introduction to the definition of datatypes and primitive
recursive functions. This generalizes and extends the material of session 1.
It starts with a few words on the meta-logic just to
explain the notation.
- Simplification. Induction heuristics.
The concept of (conditional) term rewriting is introduced and its
realization as the proof method simp is explained.
Important generalization heuristics for inductive proofs are discussed
by way of an example, the correctness proof of an iterative list reversal
function.
- Propositional logic.
Introduces natural deduction proofs for propositional logic and
the proof methods rule and erule for applying
introduction and elimination rules.
- Predicate logic.
Introduces natural deduction proofs for predicate logic. Also shows
how to compose theorems in a forward direction.
- Sets.
Set notation and inductively defined sets.
- Isar: Propositional and predicate logic.
So far all proofs are just linear lists of proof commands, without any
structure. This is typical for interactive proof assistants. Now we introduce
Isar, Isabelle's structured and readable proof language, a stylized
language of mathematical proofs. The presentation is based on
this paper
- Isar: Induction and calculational proofs.
We introduce constructs for inductive and calculational proofs.
The latter are chains of equalities and inequalities.
Material
All slides [pdf] (printable version: [ps])
Last modified: 9/8/2004