Email Gateway (Sep 13 2023 at 14:51): 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: Apr 29 2024 at 04:18 UTC