Abstract
The theory of residuated lattices, first proposed by Ward and Dilworth, is
formalised in Isabelle/HOL. This includes concepts of residuated functions;
their adjoints and conjugates. It also contains necessary and sufficient
conditions for the existence of these operations in an arbitrary lattice.
The mathematical components for residuated lattices are linked to the AFP
entry for relation algebra. In particular, we prove Jonsson and Tsinakis
conditions for a residuated boolean algebra to form a relation algebra.