In this paper, we develop an Isabelle/HOL library of order-theoretic concepts, such as various completeness conditions and fixed-point theorems. We keep our formalization as general as possible: we reprove several well-known results about complete orders, often without any property of ordering, thus complete non-orders. In particular, we generalize the Knaster - Tarski theorem so that we ensure the existence of a quasi-fixed point of monotone maps over complete non-orders, and show that the set of quasi-fixed points is complete under a mild condition - attractivity - which is implied by either antisymmetry or transitivity. This result generalizes and strengthens a result by Stauti and Maaden. Finally, we recover Kleene’s fixed-point theorem for omega-complete non-orders, again using attractivity to prove that Kleene’s fixed points are least quasi-fixed points.
@InProceedings{yamada_et_al:LIPIcs.ITP.2019.30, author = {Yamada, Akihisa and Dubut, J\'{e}r\'{e}my}, title = {{Complete Non-Orders and Fixed Points}}, booktitle = {10th International Conference on Interactive Theorem Proving (ITP 2019)}, pages = {30:1--30:16}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-122-1}, ISSN = {1868-8969}, year = {2019}, volume = {141}, editor = {Harrison, John and O'Leary, John and Tolmach, Andrew}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2019.30}, URN = {urn:nbn:de:0030-drops-110852}, doi = {10.4230/LIPIcs.ITP.2019.30}, annote = {Keywords: Order Theory, Lattice Theory, Fixed-Points, Isabelle/HOL} }
Feedback for Dagstuhl Publishing