Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] new in AFP 2023: Directed Sets

Email Gateway (Sep 13 2023 at 14:51):

From: Gerwin Klein <cl-isabelle-users@lists.cam.ac.uk>
The following entry has now become available in the AFO release version:

Formalizing Results on Directed Sets
by Akihisa Yamada and Jérémy Dubut

Directed sets are of fundamental interest in domain theory and topology. In this paper, we formalize some results on directed sets in Isabelle/HOL, most notably: under the axiom of choice, a poset has a supremum for every directed set if and only if it does so for every chain; and a function between such posets preserves suprema of directed sets if and only if it preserves suprema of chains. The known pen-and-paper proofs of these results crucially use uncountable transfinite sequences, which are not directly implementable in Isabelle/HOL. We show how to emulate such proofs by utilizing Isabelle/HOL's ordinal and cardinal library. Thanks to the formalization, we relax some conditions for the above results.

https://www.isa-afp.org/entries/Directed_Sets.html

Enjoy!
Gerwin

Last updated: Jan 04 2025 at 20:18 UTC