## 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):
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