From: Dmitriy Traytel <cl-isabelle-users@lists.cam.ac.uk>
Dear all,
Walter Guttmann has formalized divisibility of natural numbers from the relation-algebraic perspective in Isabelle:
Relational Divisibility
We formalise key concepts and axioms of the divisibility relation on natural numbers using relation algebras. They use standard relational constructions for extrema, bounds, suprema, the univalent part and symmetric quotients, which we also formalise. We moreover prove that mono-atomic elements correspond to join-irreducible elements under the divisibility axioms.
https://www.isa-afp.org/entries/Relational_Divisibility.html
Enjoy!
Last updated: Oct 20 2025 at 16:27 UTC