Inductive and Coinductive Reasoning with Isabelle/HOL (ISA)

Course at Midlands Graduate School 2021

Andrei Popescu

University of Sheffield

This course will provide an accessible, hands-on description of basic and advanced mechanisms for inductive and coinductive reasoning. It welcomes participants who use rigorous mathematical constructions in their day-to-day research and wish to widen their perspective on, and improve their arsenal of, practical induction and coinduction. The concepts will be illustrated with examples and exercises formalized in the proof assistant Isabelle/HOL, taking advantage of the substantial extension of Isabelle/HOL's (co)induction infrastructure in recent years. People who already have some familiarity with Isabelle will make the most of the exercises. However, the presented concepts themselves are proof-assistant independent hence understandable without any knowledge of Isabelle. The topics covered range from basic ones such as to more advanced ones such as Links to course material will be provided here. Please refresh your browser window when you access this page.

Isabelle exercises Slides Recordings
Monday Lecture 1 Lecture 1
Tuesday Exercise Session 1


Inductive Predicates
Wednesday Exercise Session 2


Coinductive Predicates Lecture 3
Thursday Characterization Theorem — list-based

Characterization Theorem — set-based

Friday Datatypes and Codatatypes

Other links: