Theorem Proving with Isabelle/HOL
An Intensive Course
Overview
This course is an introduction to theorem proving with the Isabelle/HOL
system. It is loosely 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
The syntax of terms and types in HOL is introduced.
Recursion and induction on lists
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 recursive functions
A thorough introduction to the definition of datatypes and
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
The concept of (conditional) term rewriting is introduced and its
realization as the proof method simp is explained.
Induction heuristics
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.
Automation
An overview of automatic proof methods in Isabelle.
- 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.
- 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: Fri Feb 12 2010