Idempotent Relations in Isabelle/HOL

摘要

A characterization of idempotent relations is presented first as a paper-style proof, then by its formalization in Isabelle/HOL. The novel characterization gives rise to the construction of idempotent relations by an abstract algorithm. This algorithm is rigorously developed inside Isabelle/HOL using primitive recursive function definitions. Whilst the characterisation and algorithm appear to be new, we regard this as an interesting demonstration of the interplay between mathematical reasoning and program development, in particular using Isabelle/HOL.