Interactive theorem proving

Isabelle has support for many different types of logic. In this course we will use higher order logic (Isabelle/HOL). An extensive tutorial which will serve as the course literature can be found here. More information can be found on the Isabelle home page, but this book is sufficient for this course.

The schedule for the course can be found here.

1. 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.
   Slides: slide1.pdf slide1_2.pdf
   Isabelle sources: demo1.thy demo1_2.thy
   
   
2. Datatypes and primitive recursive functions
   Slides: slide2.pdf
   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.
   Isabelle sources: demo2.thy
   
   
3. 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.
   Slides: slide3.pdf slide3_2.pdf
   Isabelle sources: demo3.thy demo3_2.thy
   
   
4. Propositional logic
   Introduces natural deduction proofs for propositional logic and the proof methods rule and erule for applying introduction and elimination rules.
   Slides: slide4-5.pdf
   Isabelle sources: demo4.thy
   
   
5. Predicate logic
   Introduces natural deduction proofs for predicate logic. Also shows how to compose theorems in a forward direction.
   Isabelle sources: demo5.thy
   
   
6. Sets
   Set notation and inductively defined sets.
   Slides: slide6.pdf
   Isabelle sources: demo6.thy demo6_2.thy
   
   
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. The presentation is based on this paper.
   Slides: slide7-8.pdf
   Isabelle sources: demo7.thy
   
   
8. Isar: Induction and calculational proofs
   We introduce constructs for inductive and calculational proofs. The latter are chains of equalities and inequalities.
   Isabelle sources: demo8.thy

The excercises for the course can be found here. You should have the ambition to do at least half of these excercises during the course. As you can see the solutions are available on this page. You should not look at these. This is a graduate course and as such I will trust you with this :)

At the end of the course there will be a larger project. You can choose a project of your own or take one from the page, but I would prefer that you choose one yourself. Your project shall be written in Isar, which will be covered in lectures 7 and 8.

Stefan Berghofer from the Isabelle group will be visiting between the 18:th of April to the 1:st of May. We will try to fit in a seminar with him on how Isabelle works in the real world.