Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] New in the AFP: Relational Divisibility


view this post on Zulip Email Gateway (Oct 10 2025 at 11:39):

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