Programming and automating mathematics in the Tarski–Kleene hierarchy

• A reference formalisation of Kleene and relation algebras in Isabelle/HOL is given.
• This includes the most important models of these algebras.
• Libraries contain laws for important relation-algebraic concepts.
• These include vectors, functions, reflexive transitive closure.
• Direct relational products are presented as an advanced formalisation example.

We present examples from a reference implementation of variants of Kleene algebras and Tarski's relation algebras in the theorem proving environment Isabelle/HOL. For Kleene algebras we show how models can be programmed, including sets of traces and paths, languages, binary relations, max-plus and min-plus algebras, matrices, formal power series. For relation algebras we discuss primarily proof automation in a comprehensive library and present an advanced formalisation example.