An Intensive Course

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.

**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.

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