Fixed Points Theorems for Non-Transitive Relations

In this paper, we develop an Isabelle/HOL library of order-theoreticfixed-point theorems. We keep our formalization as general as possible: wereprove several well-known results about complete orders, often with onlyantisymmetry or attractivity, a mild condition implied by either antisymmetryor transitivity. In particular, we generalize various theorems ensuring theexistence of a quasi-fixed point of monotone maps over complete relations, andshow that the set of (quasi-)fixed points is itself complete. This resultgeneralizes and strengthens theorems of Knaster-Tarski, Bourbaki-Witt, Kleene,Markowsky, Pataraia, Mashburn, Bhatta-George, and Stouti-Maaden