isabelle logo

Theorem Proving with Isabelle/HOL
An Intensive Course

Tobias Nipkow

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):
  1. 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.
  2. 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.
  3. 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.
  4. Propositional logic
    Introduces natural deduction proofs for propositional logic and the proof methods rule and erule for applying introduction and elimination rules.
  5. Predicate logic
    Introduces natural deduction proofs for predicate logic. Also shows how to compose theorems in a forward direction.
  6. Sets
    Set notation and inductively defined sets.
    Automation
    An overview of automatic proof methods in Isabelle.
  7. 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.
  8. 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]

Session 1.1 Slides [pdf] Demo.thy
Session 1.2 Slides [pdf] Demo.thy
Session 2 Slides [pdf] Demo.thy
Session 3.1 Slides [pdf] Demo.thy
Session 3.2 Slides [pdf] Demo.thy
Sessions 4 & 5 Slides [pdf] Demo1.thy Demo2.thy
Session 6.1 Slides [pdf] Demo1.thy Demo2.thy
Session 6.2 Slides [pdf] Demo.thy
Sessions 7 & 8 Slides [pdf] Demo1.thy Demo2.thy


Last modified: Fri Feb 12 2010