@inproceedings{4ffab090a7364397939665528ae662f8,
title = "Formalizing Results on Directed Sets in Isabelle/HOL (Proof Pearl)",
abstract = "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.",
keywords = "Completeness, Directed Sets, Isabelle/HOL, Ordinals, Scott Continuous Functions",
author = "Akihisa Yamada and J{\'e}r{\'e}my Dubut",
note = "Publisher Copyright: {\textcopyright} Akihisa Yamada and J{\'e}r{\'e}my Dubut; licensed under Creative Commons License CC-BY 4.0 14th International Conference on Interactive Theorem Proving (ITP 2023); 14th International Conference on Interactive Theorem Proving, ITP 2023 ; Conference date: 31-07-2023 Through 04-08-2023",
year = "2023",
month = jul,
day = "1",
doi = "10.4230/LIPIcs.ITP.2023.34",
language = "English",
series = "Leibniz International Proceedings in Informatics, LIPIcs",
publisher = "Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing",
editor = "Adam Naumowicz and Rene Thiemann",
booktitle = "14th International Conference on Interactive Theorem Proving, ITP 2023",
}