License: Creative Commons Attribution 4.0 International license (CC BY 4.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.ITP.2023.34
URN: urn:nbn:de:0030-drops-184092
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2023/18409/
Go to the corresponding LIPIcs Volume Portal

Yamada, Akihisa ; Dubut, Jérémy

Formalizing Results on Directed Sets in Isabelle/HOL (Proof Pearl)

pdf-format:
LIPIcs-ITP-2023-34.pdf (0.8 MB)

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.

BibTeX - Entry

@InProceedings{yamada_et_al:LIPIcs.ITP.2023.34,
  author =	{Yamada, Akihisa and Dubut, J\'{e}r\'{e}my},
  title =	{{Formalizing Results on Directed Sets in Isabelle/HOL (Proof Pearl)}},
  booktitle =	{14th International Conference on Interactive Theorem Proving (ITP 2023)},
  pages =	{34:1--34:13},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-284-6},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{268},
  editor =	{Naumowicz, Adam and Thiemann, Ren\'{e}},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/opus/volltexte/2023/18409},
  URN =		{urn:nbn:de:0030-drops-184092},
  doi =		{10.4230/LIPIcs.ITP.2023.34},
  annote =	{Keywords: Directed Sets, Completeness, Scott Continuous Functions, Ordinals, Isabelle/HOL}
}

Keywords: Directed Sets, Completeness, Scott Continuous Functions, Ordinals, Isabelle/HOL
Collection: 14th International Conference on Interactive Theorem Proving (ITP 2023)
Issue Date: 2023
Date of publication: 26.07.2023

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI