2026-07-23T18:55:23Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:18409 2024-03-06T11:01:49Z ddc:004 open_access

Formalizing Results on Directed Sets in Isabelle/HOL (Proof Pearl) Yamada, Akihisa Dubut, Jérémy Directed Sets Completeness Scott Continuous Functions Ordinals Isabelle/HOL 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. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Akihisa Yamada and Jérémy Dubut 2023 Is Part Of LIPIcs, Volume 268, 14th International Conference on Interactive Theorem Proving (ITP 2023) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.ITP.2023.34 urn:nbn:de:0030-drops-184092 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2023.34 eng https://creativecommons.org/licenses/by/4.0/legalcode