Interactive Theorem Proving in Isabelle/HOL

Slides

The slides will be made avaiable during the semester.

1. Organization, Introduction, Higher-Order Logic (4 on 1) and Demo01.thy
2. Pure Framework, Structured Proofs (4 on 1) and Demo02.thy
3. Structured Proofs Continued, Case Analysis and Induction (4 on 1) and Demo03.thy
4. Induction Revisited, Calculation Reasoning, Simplifier (4 on 1) and Demo04.thy
5. Function Definitions Revisited, Manual Termination Proofs, Attributes (4 on 1) and Demo05.thy
6. Projects, Proof Methods, Sledgehammer (4 on 1) and Demo06.thy
7. Inductive Definitions, Rule Inversion and Induction (4 on 1) and Demo07.thy
8. Sets and Lists in Isabelle, Case Study: Binary Search Trees (4 on 1) and Demo08.thy (Demo08_completed.thy)
9. Typedef, Lifting and Transfer (4 on 1) and Demo09.thy
10. Code Generation – Part 1 (4 on 1) and Demo10.thy
11. Code Generation – Part 2 (4 on 1) and Demo11.thy
12. Sessions, Document Preparation, Type Classes (4 on 1) and Demo12.thy and session12.tgz
13. Further Topics, Master Projects (4 on 1) and Demo13.thy