diff --git a/thys/Complete_Non_Orders/Binary_Relations.thy b/thys/Complete_Non_Orders/Binary_Relations.thy
--- a/thys/Complete_Non_Orders/Binary_Relations.thy
+++ b/thys/Complete_Non_Orders/Binary_Relations.thy
@@ -1,2245 +1,2245 @@
 (*
 Author:  Akihisa Yamada (2018-2021)
 License: LGPL (see file COPYING.LESSER)
 *)
 section \<open>Binary Relations\<close>
 
 text \<open>We start with basic properties of binary relations.\<close>
 
 theory Binary_Relations
   imports
 (* To verify that we don't use the axiom of choice, import
     HOL.Complete_Partial_Order HOL.Wellfounded
    instead of *) Main
 begin
 
 lemma conj_imp_eq_imp_imp: "(P \<and> Q \<Longrightarrow> PROP R) \<equiv> (P \<Longrightarrow> Q \<Longrightarrow> PROP R)"
   by standard simp_all
 
 lemma tranclp_trancl: "r\<^sup>+\<^sup>+ = (\<lambda>x y. (x,y) \<in> {(a,b). r a b}\<^sup>+)"
   by (auto simp: tranclp_trancl_eq[symmetric])
 
 lemma tranclp_id[simp]: "transp r \<Longrightarrow> tranclp r = r"
   using trancl_id[of "{(x,y). r x y}", folded transp_trans] by (auto simp:tranclp_trancl)
 
 lemma transp_tranclp[simp]: "transp (tranclp r)" by (auto simp: tranclp_trancl transp_trans)
 
 lemma funpow_dom: "f ` A \<subseteq> A \<Longrightarrow> (f^^n) ` A \<subseteq> A" by (induct n, auto)
 
 text \<open>Below we introduce an Isabelle-notation for $\{ \ldots x\ldots \mid x \in X \}$.\<close>
 
 syntax
   "_range" :: "'a \<Rightarrow> idts \<Rightarrow> 'a set" ("(1{_ /|./ _})")
   "_image" :: "'a \<Rightarrow> pttrn \<Rightarrow> 'a set \<Rightarrow> 'a set"  ("(1{_ /|./ (_/ \<in> _)})")
 translations
   "{e |. p}" \<rightleftharpoons> "{e | p. CONST True}"
   "{e |. p \<in> A}" \<rightleftharpoons> "CONST image (\<lambda>p. e) A"
 
 lemma image_constant:
   assumes "\<And>i. i \<in> I \<Longrightarrow> f i = y"
   shows "f ` I = (if I = {} then {} else {y})"
   using assms by auto
 
 
 subsection \<open>Various Definitions\<close>
 
 text \<open>Here we introduce various definitions for binary relations.
 The first one is our abbreviation for the dual of a relation.\<close>
 
 abbreviation(input) dual ("(_\<^sup>-)" [1000] 1000) where "r\<^sup>- x y \<equiv> r y x"
 
 lemma conversep_is_dual[simp]: "conversep = dual" by auto
 
 text \<open>Monotonicity is already defined in the library, but we want one restricted to a domain.\<close>
 
 definition "monotone_on X r s f \<equiv> \<forall>x y. x \<in> X \<longrightarrow> y \<in> X \<longrightarrow> r x y \<longrightarrow> s (f x) (f y)"
 
 lemmas monotone_onI = monotone_on_def[unfolded atomize_eq, THEN iffD2, rule_format]
 lemma monotone_onD: "monotone_on X r s f \<Longrightarrow> r x y \<Longrightarrow> x \<in> X \<Longrightarrow> y \<in> X \<Longrightarrow> s (f x) (f y)"
   by (auto simp: monotone_on_def)
 
 lemmas monotone_onE = monotone_on_def[unfolded atomize_eq, THEN iffD1, elim_format, rule_format]
 
 lemma monotone_on_UNIV[simp]: "monotone_on UNIV = monotone"
   by (intro ext, auto simp: monotone_on_def monotone_def)
 
 lemma monotone_on_dual: "monotone_on X r s f \<Longrightarrow> monotone_on X r\<^sup>- s\<^sup>- f"
   by (auto simp: monotone_on_def)
 
 lemma monotone_on_id: "monotone_on X r r id"
   by (auto simp: monotone_on_def)
 
 lemma monotone_on_cmono: "A \<subseteq> B \<Longrightarrow> monotone_on B \<le> monotone_on A"
    by (intro le_funI, auto simp: monotone_on_def)
 
 text \<open>Here we define the following notions in a standard manner\<close>
 
 text \<open>The symmetric part of a relation:\<close>
 
 definition sympartp where "sympartp r x y \<equiv> r x y \<and> r y x"
 
 lemma sympartpI[intro]:
   fixes r (infix "\<sqsubseteq>" 50)
   assumes "x \<sqsubseteq> y" and "y \<sqsubseteq> x" shows "sympartp (\<sqsubseteq>) x y"
   using assms by (auto simp: sympartp_def)
 
 lemma sympartpE[elim]:
   fixes r (infix "\<sqsubseteq>" 50)
   assumes "sympartp (\<sqsubseteq>) x y" and "x \<sqsubseteq> y \<Longrightarrow> y \<sqsubseteq> x \<Longrightarrow> thesis" shows thesis
   using assms by (auto simp: sympartp_def)
 
 lemma sympartp_dual: "sympartp r\<^sup>- = sympartp r"
   by (auto intro!:ext simp: sympartp_def)
 
 lemma sympartp_eq[simp]: "sympartp (=) = (=)" by auto
 
 lemma reflclp_sympartp[simp]: "(sympartp r)\<^sup>=\<^sup>= = sympartp r\<^sup>=\<^sup>=" by auto
 
 definition "equivpartp r x y \<equiv> x = y \<or> r x y \<and> r y x"
 
 lemma sympartp_reflclp_equivp[simp]: "sympartp r\<^sup>=\<^sup>= = equivpartp r" by (auto intro!:ext simp: equivpartp_def)
 
 lemma equivpartI[simp]: "equivpartp r x x"
   and sympartp_equivpartpI: "sympartp r x y \<Longrightarrow> equivpartp r x y"
   and equivpartpCI[intro]: "(x \<noteq> y \<Longrightarrow> sympartp r x y) \<Longrightarrow> equivpartp r x y"
   by (auto simp:equivpartp_def)
 
 lemma equivpartpE[elim]:
   assumes "equivpartp r x y"
     and "x = y \<Longrightarrow> thesis"
     and "r x y \<Longrightarrow> r y x \<Longrightarrow> thesis"
   shows "thesis"
   using assms by (auto simp: equivpartp_def)
 
 lemma equivpartp_eq[simp]: "equivpartp (=) = (=)" by auto
 
 lemma sympartp_equivpartp[simp]: "sympartp (equivpartp r) = (equivpartp r)"
   and equivpartp_equivpartp[simp]: "equivpartp (equivpartp r) = (equivpartp r)"
   and equivpartp_sympartp[simp]: "equivpartp (sympartp r) = (equivpartp r)"
   by (auto 0 5 intro!:ext)
 
 lemma equivpartp_dual: "equivpartp r\<^sup>- = equivpartp r"
   by (auto intro!:ext simp: equivpartp_def)
 
 text \<open>The asymmetric part:\<close>
 
 definition "asympartp r x y \<equiv> r x y \<and> \<not> r y x"
 
 lemma asympartpE[elim]:
   fixes r (infix "\<sqsubseteq>" 50)
   shows "asympartp (\<sqsubseteq>) x y \<Longrightarrow> (x \<sqsubseteq> y \<Longrightarrow> \<not>y \<sqsubseteq> x \<Longrightarrow> thesis) \<Longrightarrow> thesis"
   by (auto simp: asympartp_def)
 
 lemmas asympartpI[intro] = asympartp_def[unfolded atomize_eq, THEN iffD2, unfolded conj_imp_eq_imp_imp, rule_format] 
 
 lemma asympartp_eq[simp]: "asympartp (=) = bot" by auto
 
 lemma asympartp_sympartp [simp]: "asympartp (sympartp r) = bot"
   and sympartp_asympartp [simp]: "sympartp (asympartp r) = bot"
   by (auto intro!: ext)
 
 text \<open>Restriction to a set:\<close>
 
 definition Restrp (infixl "\<restriction>" 60) where "(r \<restriction> A) a b \<equiv> a \<in> A \<and> b \<in> A \<and> r a b"
 
 lemmas RestrpI[intro!] = Restrp_def[unfolded atomize_eq, THEN iffD2, unfolded conj_imp_eq_imp_imp]
 lemmas RestrpE[elim!] = Restrp_def[unfolded atomize_eq, THEN iffD1, elim_format, unfolded conj_imp_eq_imp_imp]
 
 lemma Restrp_UNIV[simp]: "r \<restriction> UNIV \<equiv> r" by (auto simp: atomize_eq)
 
 lemma Restrp_Restrp[simp]: "r \<restriction> A \<restriction> B \<equiv> r \<restriction> A \<inter> B" by (auto simp: atomize_eq Restrp_def)
 
 lemma sympartp_Restrp[simp]: "sympartp (r \<restriction> A) \<equiv> sympartp r \<restriction> A"
   by (auto simp: atomize_eq)
 
 text \<open>Relational images:\<close>
 definition Imagep (infixr "```" 59) where "r ``` A \<equiv> {b. \<exists>a \<in> A. r a b}"
 
 lemma Imagep_Image: "r ``` A = {(a,b). r a b} `` A"
   by (auto simp: Imagep_def)
 
 lemma in_Imagep: "b \<in> r ``` A \<longleftrightarrow> (\<exists>a \<in> A. r a b)" by (auto simp: Imagep_def)
 
 lemma ImagepI: "a \<in> A \<Longrightarrow> r a b \<Longrightarrow> b \<in> r ``` A" by (auto simp: in_Imagep)
 
 lemma subset_Imagep: "B \<subseteq> r ``` A \<longleftrightarrow> (\<forall>b\<in>B. \<exists>a\<in>A. r a b)"
   by (auto simp: Imagep_def)
 
 text \<open>Bounds of a set:\<close>
 definition "bound X r b \<equiv> \<forall>x \<in> X. r x b"
 
 lemma
   fixes r (infix "\<sqsubseteq>" 50)
   shows boundI[intro!]: "(\<And>x. x \<in> X \<Longrightarrow> x \<sqsubseteq> b) \<Longrightarrow> bound X (\<sqsubseteq>) b"
     and boundE[elim]: "bound X (\<sqsubseteq>) b \<Longrightarrow> ((\<And>x. x \<in> X \<Longrightarrow> x \<sqsubseteq> b) \<Longrightarrow> thesis) \<Longrightarrow> thesis"
   by (auto simp: bound_def)
 
 lemma bound_empty: "bound {} = (\<lambda>r x. True)" by auto
 
 lemma bound_insert[simp]:
   fixes r (infix "\<sqsubseteq>" 50)
   shows "bound (insert x X) (\<sqsubseteq>) b \<longleftrightarrow> x \<sqsubseteq> b \<and> bound X (\<sqsubseteq>) b" by auto
 
 text \<open>Extreme (greatest) elements in a set:\<close>
 definition "extreme X r e \<equiv> e \<in> X \<and> (\<forall>x \<in> X. r x e)"
 
 lemma
   fixes r (infix "\<sqsubseteq>" 50)
   shows extremeI[intro]: "e \<in> X \<Longrightarrow> (\<And>x. x \<in> X \<Longrightarrow> x \<sqsubseteq> e) \<Longrightarrow> extreme X (\<sqsubseteq>) e"
     and extremeD: "extreme X (\<sqsubseteq>) e \<Longrightarrow> e \<in> X" "extreme X (\<sqsubseteq>) e \<Longrightarrow> (\<And>x. x \<in> X \<Longrightarrow> x \<sqsubseteq> e)"
     and extremeE[elim]: "extreme X (\<sqsubseteq>) e \<Longrightarrow> (e \<in> X \<Longrightarrow> (\<And>x. x \<in> X \<Longrightarrow> x \<sqsubseteq> e) \<Longrightarrow> thesis) \<Longrightarrow> thesis"
   by (auto simp: extreme_def)
 
 lemma
   fixes r (infix "\<sqsubseteq>" 50)
   shows extreme_UNIV[simp]: "extreme UNIV (\<sqsubseteq>) t \<longleftrightarrow> (\<forall>x. x \<sqsubseteq> t)" by auto
 
 lemma extremes_equiv: "extreme X r b \<Longrightarrow> extreme X r c \<Longrightarrow> sympartp r b c" by blast
 
 lemma bound_cmono: assumes "X \<subseteq> Y" shows "bound Y \<le> bound X"
   using assms by auto
 
 lemma sympartp_sympartp[simp]: "sympartp (sympartp r) = sympartp r" by (auto intro!:ext)
 
 text \<open>Now suprema and infima are given uniformly as follows.
   The definition is restricted to a given set.
 \<close>
 context
   fixes A :: "'a set" and less_eq :: "'a \<Rightarrow> 'a \<Rightarrow> bool" (infix "\<sqsubseteq>" 50)
 begin
 
 abbreviation "extreme_bound X \<equiv> extreme {b \<in> A. bound X (\<sqsubseteq>) b} (\<lambda>x y. y \<sqsubseteq> x)"
 
 lemma extreme_boundI[intro]:
   assumes "\<And>b. bound X (\<sqsubseteq>) b \<Longrightarrow> b \<in> A \<Longrightarrow> s \<sqsubseteq> b" and "\<And>x. x \<in> X \<Longrightarrow> x \<sqsubseteq> s" and "s \<in> A"
   shows "extreme_bound X s"
   using assms by auto
 
 lemma extreme_bound_bound: "extreme_bound X y \<Longrightarrow> x \<in> X \<Longrightarrow> x \<sqsubseteq> y" by auto
 
 lemma extreme_bound_mono:
   assumes XY: "X \<subseteq> Y"
     and sX: "extreme_bound X sX"
     and sY: "extreme_bound Y sY"
   shows "sX \<sqsubseteq> sY"
 proof-
   have "bound X (\<sqsubseteq>) sY" using XY sY by force
   with sX sY show ?thesis by (auto 0 4)
 qed
 
 lemma extreme_bound_iff:
   shows "extreme_bound X s \<longleftrightarrow> s \<in> A \<and> (\<forall>c \<in> A. (\<forall>x \<in> X. x \<sqsubseteq> c) \<longrightarrow> s \<sqsubseteq> c) \<and> (\<forall>x \<in> X. x \<sqsubseteq> s)"
   by (auto simp: extreme_def)
 
 lemma extreme_bound_singleton_refl[simp]:
   "extreme_bound {x} x \<longleftrightarrow> x \<in> A \<and> x \<sqsubseteq> x" by auto
 
 lemma extreme_bound_image_const:
   "x \<sqsubseteq> x \<Longrightarrow> I \<noteq> {} \<Longrightarrow> (\<And>i. i \<in> I \<Longrightarrow> f i = x) \<Longrightarrow> x \<in> A \<Longrightarrow> extreme_bound (f ` I) x"
   by (auto simp: image_constant)
 
 lemma extreme_bound_UN_const:
   "x \<sqsubseteq> x \<Longrightarrow> I \<noteq> {} \<Longrightarrow> (\<And>i y. i \<in> I \<Longrightarrow> P i y \<longleftrightarrow> x = y) \<Longrightarrow> x \<in> A \<Longrightarrow>
   extreme_bound (\<Union>i\<in>I. {y. P i y}) x"
   by auto
 
 end
 
 context
   fixes ir :: "'i \<Rightarrow> 'i \<Rightarrow> bool" (infix "\<preceq>" 50)
     and r :: "'a \<Rightarrow> 'a \<Rightarrow> bool" (infix "\<sqsubseteq>" 50)
     and f and A and e and I
   assumes fIA: "f ` I \<subseteq> A"
     and mono: "monotone_on I (\<preceq>) (\<sqsubseteq>) f"
     and e: "extreme I (\<preceq>) e"
 begin
 
 lemma monotone_extreme_imp_extreme_bound:
   "extreme_bound A (\<sqsubseteq>) (f ` I) (f e)"
   using monotone_onD[OF mono] e fIA
   by (intro extreme_boundI, auto simp: image_def elim!: extremeE)
 
 lemma monotone_extreme_extreme_boundI:
   "x = f e \<Longrightarrow> extreme_bound A (\<sqsubseteq>) (f ` I) x"
   using monotone_extreme_imp_extreme_bound by auto
 
 end
 
 subsection \<open>Locales for Binary Relations\<close>
 
 text \<open>We now define basic properties of binary relations,
 in form of \emph{locales}~\cite{Kammuller00,locale}.\<close>
 
 subsubsection \<open>Syntactic Locales\<close>
 
 text \<open>The following locales do not assume anything, but provide infix notations for
 relations.\<close>
 
 locale less_eq_syntax =
   fixes less_eq :: "'a \<Rightarrow> 'a \<Rightarrow> bool" (infix "\<sqsubseteq>" 50)
 
 locale less_syntax =
   fixes less :: "'a \<Rightarrow> 'a \<Rightarrow> bool" (infix "\<sqsubset>" 50)
 
 locale equivalence_syntax =
   fixes equiv :: "'a \<Rightarrow> 'a \<Rightarrow> bool" (infix "\<sim>" 50)
 begin
 
 abbreviation equiv_class ("[_]\<^sub>\<sim>") where "[x]\<^sub>\<sim> \<equiv> { y. x \<sim> y }"
 
 end
 
 text \<open>Next ones introduce abbreviations for dual etc.
 To avoid needless constants, one should be careful when declaring them as sublocales.\<close>
 
 locale less_eq_notations = less_eq_syntax
 begin
 
 abbreviation (input) greater_eq (infix "\<sqsupseteq>" 50) where "x \<sqsupseteq> y \<equiv> y \<sqsubseteq> x"
 abbreviation sym (infix "\<sim>" 50) where "(\<sim>) \<equiv> sympartp (\<sqsubseteq>)"
 abbreviation less (infix "\<sqsubset>" 50) where "(\<sqsubset>) \<equiv> asympartp (\<sqsubseteq>)"
 abbreviation greater (infix "\<sqsupset>" 50) where "(\<sqsupset>) \<equiv> (\<sqsubset>)\<^sup>-"
 abbreviation equiv (infix "(\<simeq>)" 50) where "(\<simeq>) \<equiv> equivpartp (\<sqsubseteq>)"
 
 lemma asym_cases[consumes 1, case_names asym sym]:
   assumes "x \<sqsubseteq> y" and "x \<sqsubset> y \<Longrightarrow> thesis" and "x \<sim> y \<Longrightarrow> thesis"
   shows thesis
   using assms by auto
 
 end
 
 locale less_notations = less_syntax
 begin
 
 abbreviation (input) greater (infix "\<sqsupset>" 50) where "x \<sqsupset> y \<equiv> y \<sqsubset> x"
 
 end
 
 locale related_set =
   fixes A :: "'a set" and less_eq :: "'a \<Rightarrow> 'a \<Rightarrow> bool" (infix "\<sqsubseteq>" 50)
 
 subsubsection \<open>Basic Properties of Relations\<close>
 
 text \<open>In the following we define basic properties in form of locales.\<close>
 
 text \<open>Reflexivity restricted on a set:\<close>
 locale reflexive = related_set +
   assumes refl[intro]: "x \<in> A \<Longrightarrow> x \<sqsubseteq> x"
 begin
 
 lemma eq_implies: "x = y \<Longrightarrow> x \<in> A \<Longrightarrow> x \<sqsubseteq> y" by auto
 
 lemma extreme_singleton[simp]: "x \<in> A \<Longrightarrow> extreme {x} (\<sqsubseteq>) y \<longleftrightarrow> x = y" by auto
 
 lemma extreme_bound_singleton: "x \<in> A \<Longrightarrow> extreme_bound A (\<sqsubseteq>) {x} x" by auto
 
 lemma reflexive_subset: "B \<subseteq> A \<Longrightarrow> reflexive B (\<sqsubseteq>)" apply unfold_locales by auto
 
 end
 
 declare reflexive.intro[intro!]
 
 lemma reflexiveE[elim]:
   assumes "reflexive A r" and "(\<And>x. x \<in> A \<Longrightarrow> r x x) \<Longrightarrow> thesis" shows thesis
   using assms by (auto simp: reflexive.refl)
 
 lemma reflexive_cong:
   "(\<And>a b. a \<in> A \<Longrightarrow> b \<in> A \<Longrightarrow> r a b \<longleftrightarrow> r' a b) \<Longrightarrow> reflexive A r \<longleftrightarrow> reflexive A r'"
   by (simp add: reflexive_def)
 
 locale irreflexive = related_set A "(\<sqsubset>)" for A and less (infix "\<sqsubset>" 50) +
   assumes irrefl: "x \<in> A \<Longrightarrow> \<not> x \<sqsubset> x"
 begin
 
 lemma irreflD[simp]: "x \<sqsubset> x \<Longrightarrow> \<not>x \<in> A" by (auto simp: irrefl)
 
 lemma implies_not_eq: "x \<sqsubset> y \<Longrightarrow> x \<in> A \<Longrightarrow> x \<noteq> y" by auto
 
 lemma Restrp_irreflexive: "irreflexive UNIV ((\<sqsubset>)\<restriction>A)"
   apply unfold_locales by auto
 
 lemma irreflexive_subset: "B \<subseteq> A \<Longrightarrow> irreflexive B (\<sqsubset>)" apply unfold_locales by auto
 
 end
 
 declare irreflexive.intro[intro!]
 
 lemma irreflexive_cong:
   "(\<And>a b. a \<in> A \<Longrightarrow> b \<in> A \<Longrightarrow> r a b \<longleftrightarrow> r' a b) \<Longrightarrow> irreflexive A r \<longleftrightarrow> irreflexive A r'"
   by (simp add: irreflexive_def)
 
 locale transitive = related_set +
   assumes trans[trans]: "x \<sqsubseteq> y \<Longrightarrow> y \<sqsubseteq> z \<Longrightarrow> x \<in> A \<Longrightarrow> y \<in> A \<Longrightarrow> z \<in> A \<Longrightarrow> x \<sqsubseteq> z"
 begin
 
 interpretation less_eq_notations.
 
 lemma Restrp_transitive: "transitive UNIV ((\<sqsubseteq>)\<restriction>A)"
   apply unfold_locales
   by (auto intro: trans)
 
 lemma bound_trans[trans]: "bound X (\<sqsubseteq>) b \<Longrightarrow> b \<sqsubseteq> c \<Longrightarrow> X \<subseteq> A \<Longrightarrow> b \<in> A \<Longrightarrow> c \<in> A \<Longrightarrow> bound X (\<sqsubseteq>) c"
   by (auto 0 4 dest: trans)
 
 lemma transitive_subset:
   assumes BA: "B \<subseteq> A" shows "transitive B (\<sqsubseteq>)"
   apply unfold_locales
   using trans BA by blast
 
 lemma asympartp_transitive: "transitive A (\<sqsubset>)"
   apply unfold_locales by (auto dest:trans)
 
 lemma reflclp_transitive: "transitive A (\<sqsubseteq>)\<^sup>=\<^sup>="
   apply unfold_locales by (auto dest: trans)
 
 text \<open>The symmetric part is also transitive, but this is done in the later semiattractive locale\<close>
 
 end
 
 declare transitive.intro[intro?]
 
 lemma transitive_cong:
   assumes r: "\<And>a b. a \<in> A \<Longrightarrow> b \<in> A \<Longrightarrow> r a b \<longleftrightarrow> r' a b" shows "transitive A r \<longleftrightarrow> transitive A r'"
 proof (intro iffI)
   show "transitive A r \<Longrightarrow> transitive A r'"
     apply (intro transitive.intro)
     apply (unfold r[symmetric])
     using transitive.trans.
   show "transitive A r' \<Longrightarrow> transitive A r"
     apply (intro transitive.intro)
     apply (unfold r)
     using transitive.trans.
 qed
 
 lemma tranclp_transitive: "transitive A (tranclp r)"
   using tranclp_trans by unfold_locales
 
 locale symmetric = related_set A "(\<sim>)" for A and equiv (infix "\<sim>" 50) +
   assumes sym[sym]: "x \<sim> y \<Longrightarrow> x \<in> A \<Longrightarrow> y \<in> A \<Longrightarrow> y \<sim> x"
 begin
 
 lemma sym_iff: "x \<in> A \<Longrightarrow> y \<in> A \<Longrightarrow> x \<sim> y \<longleftrightarrow> y \<sim> x"
   by (auto dest: sym)
 
 lemma Restrp_symmetric: "symmetric UNIV ((\<sim>)\<restriction>A)"
   apply unfold_locales by (auto simp: sym_iff)
 
 lemma symmetric_subset: "B \<subseteq> A \<Longrightarrow> symmetric B (\<sim>)"
   apply unfold_locales by (auto dest: sym)
 
 end
 
 declare symmetric.intro[intro]
 
 lemma symmetric_cong:
   "(\<And>a b. a \<in> A \<Longrightarrow> b \<in> A \<Longrightarrow> r a b \<longleftrightarrow> r' a b) \<Longrightarrow> symmetric A r \<longleftrightarrow> symmetric A r'"
   by (auto simp: symmetric_def)
 
 
 global_interpretation sympartp: symmetric UNIV "sympartp r"
   rewrites "\<And>r. r \<restriction> UNIV \<equiv> r"
     and "\<And>x. x \<in> UNIV \<equiv> True"
     and "\<And>P1. (True \<Longrightarrow> P1) \<equiv> Trueprop P1"
     and "\<And>P1 P2. (True \<Longrightarrow> PROP P1 \<Longrightarrow> PROP P2) \<equiv> (PROP P1 \<Longrightarrow> PROP P2)"
   by auto
 
 lemma sympartp_symmetric: "symmetric A (sympartp r)" by auto
 
 locale antisymmetric = related_set +
   assumes antisym: "x \<sqsubseteq> y \<Longrightarrow> y \<sqsubseteq> x \<Longrightarrow> x \<in> A \<Longrightarrow> y \<in> A \<Longrightarrow> x = y"
 begin
 
 interpretation less_eq_notations.
 
 lemma sym_iff_eq_refl: "x \<in> A \<Longrightarrow> y \<in> A \<Longrightarrow> x \<sim> y \<longleftrightarrow> x = y \<and> y \<sqsubseteq> y" by (auto dest: antisym)
 
 lemma equiv_iff_eq[simp]: "x \<in> A \<Longrightarrow> y \<in> A \<Longrightarrow> x \<simeq> y \<longleftrightarrow> x = y" by (auto dest: antisym elim: equivpartpE)
 
 lemma extreme_unique: "X \<subseteq> A \<Longrightarrow> extreme X (\<sqsubseteq>) x \<Longrightarrow> extreme X (\<sqsubseteq>) y \<longleftrightarrow> x = y"
   by (elim extremeE, auto dest!: antisym[OF _ _ subsetD])
 
 lemma ex_extreme_iff_ex1:
   "X \<subseteq> A \<Longrightarrow> Ex (extreme X (\<sqsubseteq>)) \<longleftrightarrow> Ex1 (extreme X (\<sqsubseteq>))" by (auto simp: extreme_unique)
 
 lemma ex_extreme_iff_the:
    "X \<subseteq> A \<Longrightarrow> Ex (extreme X (\<sqsubseteq>)) \<longleftrightarrow> extreme X (\<sqsubseteq>) (The (extreme X (\<sqsubseteq>)))"
   apply (rule iffI)
   apply (rule theI')
   using extreme_unique by auto
 
 lemma Restrp_antisymmetric: "antisymmetric UNIV ((\<sqsubseteq>)\<restriction>A)"
    apply unfold_locales
   by (auto dest: antisym)
 
 lemma antisymmetric_subset: "B \<subseteq> A \<Longrightarrow> antisymmetric B (\<sqsubseteq>)"
   apply unfold_locales using antisym by auto
 
 end
 
 declare antisymmetric.intro[intro]
 
 lemma antisymmetric_cong:
   "(\<And>a b. a \<in> A \<Longrightarrow> b \<in> A \<Longrightarrow> r a b \<longleftrightarrow> r' a b) \<Longrightarrow> antisymmetric A r \<longleftrightarrow> antisymmetric A r'"
   by (auto simp: antisymmetric_def)
 
 lemma antisymmetric_union:
   fixes less_eq (infix "\<sqsubseteq>" 50)
   assumes A: "antisymmetric A (\<sqsubseteq>)" and B: "antisymmetric B (\<sqsubseteq>)"
     and AB: "\<forall>a \<in> A. \<forall>b \<in> B. a \<sqsubseteq> b \<longrightarrow> b \<sqsubseteq> a \<longrightarrow> a = b"
   shows "antisymmetric (A \<union> B) (\<sqsubseteq>)"
 proof-
   interpret A: antisymmetric A "(\<sqsubseteq>)" using A.
   interpret B: antisymmetric B "(\<sqsubseteq>)" using B.
   show ?thesis by (auto dest: AB[rule_format] A.antisym B.antisym)
 qed
 
 text \<open>The following notion is new, generalizing antisymmetry and transitivity.\<close>
 
 locale semiattractive = related_set +
   assumes attract: "x \<sqsubseteq> y \<Longrightarrow> y \<sqsubseteq> x \<Longrightarrow> y \<sqsubseteq> z \<Longrightarrow> x \<in> A \<Longrightarrow> y \<in> A \<Longrightarrow> z \<in> A \<Longrightarrow> x \<sqsubseteq> z"
 begin
 
 interpretation less_eq_notations.
 
 lemma equiv_order_trans[trans]:
   assumes xy: "x \<simeq> y" and yz: "y \<sqsubseteq> z" and x: "x \<in> A" and y: "y \<in> A" and z: "z \<in> A"
   shows "x \<sqsubseteq> z"
   using attract[OF _ _ _ x y z] xy yz by (auto elim: equivpartpE)
 
 lemma equiv_transitive: "transitive A (\<simeq>)"
 proof unfold_locales
   fix x y z
   assume x: "x \<in> A" and y: "y \<in> A" and z: "z \<in> A" and xy: "x \<simeq> y" and yz: "y \<simeq> z"
   show "x \<simeq> z"
     using equiv_order_trans[OF xy _ x y z] attract[OF _ _ _ z y x] xy yz by (auto simp:equivpartp_def)
 qed
 
 lemma sym_order_trans[trans]:
   assumes xy: "x \<sim> y" and yz: "y \<sqsubseteq> z" and x: "x \<in> A" and y: "y \<in> A" and z: "z \<in> A"
   shows "x \<sqsubseteq> z"
   using attract[OF _ _ _ x y z] xy yz by auto
 
 interpretation sym: transitive A "(\<sim>)"
 proof unfold_locales
   fix x y z
   assume x: "x \<in> A" and y: "y \<in> A" and z: "z \<in> A" and xy: "x \<sim> y" and yz: "y \<sim> z"
   show "x \<sim> z"
     using sym_order_trans[OF xy _ x y z] attract[OF _ _ _ z y x] xy yz by auto
 qed
 
 lemmas sym_transitive = sym.transitive_axioms
 
 lemma extreme_bound_quasi_const:
   assumes C: "C \<subseteq> A" and x: "x \<in> A" and C0: "C \<noteq> {}" and const: "\<forall>y \<in> C. y \<sim> x"
   shows "extreme_bound A (\<sqsubseteq>) C x"
 proof (intro extreme_boundI x)
   from C0 obtain c where cC: "c \<in> C" by auto
   with C have c: "c \<in> A" by auto
   from cC const have cx: "c \<sim> x" by auto
   fix b assume b: "b \<in> A" and "bound C (\<sqsubseteq>) b"
   with cC have cb: "c \<sqsubseteq> b" by auto
   from attract[OF _ _ cb x c b] cx show "x \<sqsubseteq> b" by auto
 next
   fix c assume "c \<in> C"
   with const show "c \<sqsubseteq> x" by auto
 qed
 
 lemma extreme_bound_quasi_const_iff:
   assumes C: "C \<subseteq> A" and x: "x \<in> A" and y: "y \<in> A" and C0: "C \<noteq> {}" and const: "\<forall>z \<in> C. z \<sim> x"
   shows "extreme_bound A (\<sqsubseteq>) C y \<longleftrightarrow> x \<sim> y"
 proof (intro iffI)
   assume y: "extreme_bound A (\<sqsubseteq>) C y"
   note x = extreme_bound_quasi_const[OF C x C0 const]
   from extremes_equiv[OF y x]
   show "x \<sim> y" by auto
 next
   assume xy: "x \<sim> y"
   with const C sym.trans[OF _ xy _ x y] have Cy: "\<forall>z \<in> C. z \<sim> y" by auto
   show "extreme_bound A (\<sqsubseteq>) C y"
     using extreme_bound_quasi_const[OF C y C0 Cy].
 qed
 
 lemma Restrp_semiattractive: "semiattractive UNIV ((\<sqsubseteq>)\<restriction>A)"
   apply unfold_locales
   by (auto dest: attract)
 
 lemma semiattractive_subset: "B \<subseteq> A \<Longrightarrow> semiattractive B (\<sqsubseteq>)"
   apply unfold_locales using attract by blast
 
 end
 
 lemma semiattractive_cong:
   assumes r: "\<And>a b. a \<in> A \<Longrightarrow> b \<in> A \<Longrightarrow> r a b \<longleftrightarrow> r' a b"
   shows "semiattractive A r \<longleftrightarrow> semiattractive A r'" (is "?l \<longleftrightarrow> ?r")
 proof
   show "?l \<Longrightarrow> ?r"
     apply (intro semiattractive.intro)
     apply (unfold r[symmetric])
     using semiattractive.attract.
   show "?r \<Longrightarrow> ?l"
     apply (intro semiattractive.intro)
     apply (unfold r)
     using semiattractive.attract.
 qed
 
 locale attractive = semiattractive +
   assumes "semiattractive A (\<sqsubseteq>)\<^sup>-"
 begin
 
 interpretation less_eq_notations.
 
 sublocale dual: semiattractive A "(\<sqsubseteq>)\<^sup>-"
   rewrites "\<And>r. sympartp (r \<restriction> A) \<equiv> sympartp r \<restriction> A"
     and "\<And>r. sympartp (sympartp r) \<equiv> sympartp r"
     and "sympartp ((\<sqsubseteq>) \<restriction> A)\<^sup>- \<equiv> (\<sim>) \<restriction> A"
     and "sympartp (\<sqsubseteq>)\<^sup>- \<equiv> (\<sim>)"
     and "equivpartp (\<sqsubseteq>)\<^sup>- \<equiv> (\<simeq>)"
   using attractive_axioms[unfolded attractive_def]
   by (auto intro!: ext simp: attractive_axioms_def atomize_eq equivpartp_def)
 
 lemma order_equiv_trans[trans]:
   assumes xy: "x \<sqsubseteq> y" and yz: "y \<simeq> z" and x: "x \<in> A" and y: "y \<in> A" and z: "z \<in> A"
   shows "x \<sqsubseteq> z"
   using dual.attract[OF _ _ _ z y x] xy yz by auto
 
 lemma order_sym_trans[trans]:
   assumes xy: "x \<sqsubseteq> y" and yz: "y \<sim> z" and x: "x \<in> A" and y: "y \<in> A" and z: "z \<in> A"
   shows "x \<sqsubseteq> z"
   using dual.attract[OF _ _ _ z y x] xy yz by auto
 
 interpretation Restrp: semiattractive UNIV "(\<sqsubseteq>)\<restriction>A" using Restrp_semiattractive.
 interpretation dual.Restrp: semiattractive UNIV "(\<sqsubseteq>)\<^sup>-\<restriction>A" using dual.Restrp_semiattractive.
 
 lemma Restrp_attractive: "attractive UNIV ((\<sqsubseteq>)\<restriction>A)"
   apply unfold_locales
   using dual.Restrp.attract by auto
 
 lemma attractive_subset: "B \<subseteq> A \<Longrightarrow> attractive B (\<sqsubseteq>)"
   apply (intro attractive.intro attractive_axioms.intro)
   using semiattractive_subset dual.semiattractive_subset by auto
 
 end
 
 lemma attractive_cong:
   assumes r: "\<And>a b. a \<in> A \<Longrightarrow> b \<in> A \<Longrightarrow> r a b \<longleftrightarrow> r' a b"
   shows "attractive A r \<longleftrightarrow> attractive A r'"
   by (simp add: attractive_def attractive_axioms_def r cong: semiattractive_cong)
 
 context antisymmetric begin
 
 sublocale attractive
   apply unfold_locales by (auto dest: antisym)
 
 end
 
 context transitive begin
 
 sublocale attractive
   rewrites "\<And>r. sympartp (r \<restriction> A) \<equiv> sympartp r \<restriction> A"
     and "\<And>r. sympartp (sympartp r) \<equiv> sympartp r"
     and "sympartp (\<sqsubseteq>)\<^sup>- \<equiv> sympartp (\<sqsubseteq>)"
     and "(sympartp (\<sqsubseteq>))\<^sup>- \<equiv> sympartp (\<sqsubseteq>)"
     and "(sympartp (\<sqsubseteq>) \<restriction> A)\<^sup>- \<equiv> sympartp (\<sqsubseteq>) \<restriction> A"
     and "asympartp (asympartp (\<sqsubseteq>)) = asympartp (\<sqsubseteq>)"
     and "asympartp (sympartp (\<sqsubseteq>)) = bot"
     and "asympartp (\<sqsubseteq>) \<restriction> A = asympartp ((\<sqsubseteq>) \<restriction> A)"
   apply unfold_locales
   by (auto intro!:ext dest: trans simp: atomize_eq)
 
 end
 
 subsection \<open>Combined Properties\<close>
 
 text \<open>Some combinations of the above basic properties are given names.\<close>
 
 locale asymmetric = related_set A "(\<sqsubset>)" for A and less (infix "\<sqsubset>" 50) +
   assumes asym: "x \<sqsubset> y \<Longrightarrow> y \<sqsubset> x \<Longrightarrow> x \<in> A \<Longrightarrow> y \<in> A \<Longrightarrow> False"
 begin
 
 sublocale irreflexive
   apply unfold_locales by (auto dest: asym)
 
 lemma antisymmetric_axioms: "antisymmetric A (\<sqsubset>)"
   apply unfold_locales by (auto dest: asym)
 
 lemma Restrp_asymmetric: "asymmetric UNIV ((\<sqsubset>)\<restriction>A)"
   apply unfold_locales
   by (auto dest:asym)
 
 lemma asymmetric_subset: "B \<subseteq> A \<Longrightarrow> asymmetric B (\<sqsubset>)"
   apply unfold_locales using asym by auto
 
 end
 
 lemma asymmetric_iff_irreflexive_antisymmetric:
   fixes less (infix "\<sqsubset>" 50)
   shows "asymmetric A (\<sqsubset>) \<longleftrightarrow> irreflexive A (\<sqsubset>) \<and> antisymmetric A (\<sqsubset>)" (is "?l \<longleftrightarrow> ?r")
 proof
   assume ?l
   then interpret asymmetric.
   show ?r by (auto dest: asym)
 next
   assume ?r
   then interpret irreflexive + antisymmetric A "(\<sqsubset>)" by auto
   show ?l by (auto intro!:asymmetric.intro dest: antisym irrefl)
 qed
 
 lemma asymmetric_cong:
   assumes r: "\<And>a b. a \<in> A \<Longrightarrow> b \<in> A \<Longrightarrow> r a b \<longleftrightarrow> r' a b"
   shows "asymmetric A r \<longleftrightarrow> asymmetric A r'"
   by (simp add: asymmetric_iff_irreflexive_antisymmetric r cong: irreflexive_cong antisymmetric_cong)
 
 locale quasi_ordered_set = reflexive + transitive
 begin
 
 lemma quasi_ordered_subset: "B \<subseteq> A \<Longrightarrow> quasi_ordered_set B (\<sqsubseteq>)"
   apply intro_locales
   using reflexive_subset transitive_subset by auto
 
 end
 
 lemma quasi_ordered_set_cong:
   assumes r: "\<And>a b. a \<in> A \<Longrightarrow> b \<in> A \<Longrightarrow> r a b \<longleftrightarrow> r' a b"
   shows "quasi_ordered_set A r \<longleftrightarrow> quasi_ordered_set A r'"
   by (simp add: quasi_ordered_set_def r cong: reflexive_cong transitive_cong)
 
 locale near_ordered_set = antisymmetric + transitive
 begin
 
 interpretation Restrp: antisymmetric UNIV "(\<sqsubseteq>)\<restriction>A" using Restrp_antisymmetric.
 interpretation Restrp: transitive UNIV "(\<sqsubseteq>)\<restriction>A" using Restrp_transitive.
 
 lemma Restrp_near_order: "near_ordered_set UNIV ((\<sqsubseteq>)\<restriction>A)"..
 
 lemma near_ordered_subset: "B \<subseteq> A \<Longrightarrow> near_ordered_set B (\<sqsubseteq>)"
   apply intro_locales
   using antisymmetric_subset transitive_subset by auto
 
 end
 
 lemma near_ordered_set_cong:
   assumes r: "\<And>a b. a \<in> A \<Longrightarrow> b \<in> A \<Longrightarrow> r a b \<longleftrightarrow> r' a b"
   shows "near_ordered_set A r \<longleftrightarrow> near_ordered_set A r'"
   by (simp add: near_ordered_set_def r cong: antisymmetric_cong transitive_cong)
 
 locale pseudo_ordered_set = reflexive + antisymmetric
 begin
 
 interpretation less_eq_notations.
 
 lemma sym_eq[simp]: "x \<in> A \<Longrightarrow> y \<in> A \<Longrightarrow> x \<sim> y \<longleftrightarrow> x = y"
   by (auto simp: refl dest: antisym)
 
 lemma extreme_bound_singleton_eq[simp]: "x \<in> A \<Longrightarrow> extreme_bound A (\<sqsubseteq>) {x} y \<longleftrightarrow> x = y"
   by (auto intro!: antisym)
 
 lemma eq_iff: "x \<in> A \<Longrightarrow> y \<in> A \<Longrightarrow> x = y \<longleftrightarrow> x \<sqsubseteq> y \<and> y \<sqsubseteq> x" by (auto dest: antisym simp:refl)
 
 lemma extreme_order_iff_eq: "e \<in> A \<Longrightarrow> extreme {x \<in> A. x \<sqsubseteq> e} (\<sqsubseteq>) s \<longleftrightarrow> e = s"
   by (auto intro!: antisym)
 
 lemma pseudo_ordered_subset: "B \<subseteq> A \<Longrightarrow> pseudo_ordered_set B (\<sqsubseteq>)"
   apply intro_locales
   using reflexive_subset antisymmetric_subset by auto
 
 end
 
 lemma pseudo_ordered_set_cong:
   assumes r: "\<And>a b. a \<in> A \<Longrightarrow> b \<in> A \<Longrightarrow> r a b \<longleftrightarrow> r' a b"
   shows "pseudo_ordered_set A r \<longleftrightarrow> pseudo_ordered_set A r'"
   by (simp add: pseudo_ordered_set_def r cong: reflexive_cong antisymmetric_cong)
 
 locale partially_ordered_set = reflexive + antisymmetric + transitive
 begin
 
 sublocale pseudo_ordered_set + quasi_ordered_set + near_ordered_set ..
 
 lemma partially_ordered_subset: "B \<subseteq> A \<Longrightarrow> partially_ordered_set B (\<sqsubseteq>)"
   apply intro_locales
   using reflexive_subset transitive_subset antisymmetric_subset by auto
 
 end
 
 lemma partially_ordered_set_cong:
   assumes r: "\<And>a b. a \<in> A \<Longrightarrow> b \<in> A \<Longrightarrow> r a b \<longleftrightarrow> r' a b"
   shows "partially_ordered_set A r \<longleftrightarrow> partially_ordered_set A r'"
   by (simp add: partially_ordered_set_def r cong: reflexive_cong antisymmetric_cong transitive_cong)
 
 locale strict_ordered_set = irreflexive + transitive A "(\<sqsubset>)"
 begin
 
 sublocale asymmetric
 proof
   fix x y
   assume x: "x \<in> A" and y: "y \<in> A"
   assume xy: "x \<sqsubset> y"
   also assume yx: "y \<sqsubset> x"
   finally have "x \<sqsubset> x" using x y by auto
   with x show False by auto
 qed
 
 lemma near_ordered_set_axioms: "near_ordered_set A (\<sqsubset>)"
   using antisymmetric_axioms by intro_locales
 
 interpretation Restrp: asymmetric UNIV "(\<sqsubset>)\<restriction>A" using Restrp_asymmetric.
 interpretation Restrp: transitive UNIV "(\<sqsubset>)\<restriction>A" using Restrp_transitive.
 
 lemma Restrp_strict_order: "strict_ordered_set UNIV ((\<sqsubset>)\<restriction>A)"..
 
 lemma strict_ordered_subset: "B \<subseteq> A \<Longrightarrow> strict_ordered_set B (\<sqsubset>)"
   apply intro_locales
   using irreflexive_subset transitive_subset by auto
 
 end
 
 lemma strict_ordered_set_cong:
   assumes r: "\<And>a b. a \<in> A \<Longrightarrow> b \<in> A \<Longrightarrow> r a b \<longleftrightarrow> r' a b"
   shows "strict_ordered_set A r \<longleftrightarrow> strict_ordered_set A r'"
   by (simp add: strict_ordered_set_def r cong: irreflexive_cong transitive_cong)
 
 locale tolerance = symmetric + reflexive A "(\<sim>)"
 begin
 
 lemma tolerance_subset: "B \<subseteq> A \<Longrightarrow> tolerance B (\<sim>)"
   apply intro_locales
   using symmetric_subset reflexive_subset by auto
 
 end
 
 lemma tolerance_cong:
   assumes r: "\<And>a b. a \<in> A \<Longrightarrow> b \<in> A \<Longrightarrow> r a b \<longleftrightarrow> r' a b"
   shows "tolerance A r \<longleftrightarrow> tolerance A r'"
   by (simp add: tolerance_def r cong: reflexive_cong symmetric_cong)
 
 global_interpretation equiv: tolerance UNIV "equivpartp r"
   rewrites "\<And>r. r \<restriction> UNIV \<equiv> r"
     and "\<And>x. x \<in> UNIV \<equiv> True"
     and "\<And>P1. (True \<Longrightarrow> P1) \<equiv> Trueprop P1"
     and "\<And>P1 P2. (True \<Longrightarrow> PROP P1 \<Longrightarrow> PROP P2) \<equiv> (PROP P1 \<Longrightarrow> PROP P2)"
   by unfold_locales (auto simp:equivpartp_def)
 
 locale partial_equivalence = symmetric +
   assumes "transitive A (\<sim>)"
 begin
 
 sublocale transitive A "(\<sim>)"
   rewrites "sympartp (\<sim>)\<restriction>A \<equiv> (\<sim>)\<restriction>A"
     and "sympartp ((\<sim>)\<restriction>A) \<equiv> (\<sim>)\<restriction>A"
   using partial_equivalence_axioms
   unfolding partial_equivalence_axioms_def partial_equivalence_def
   by (auto simp: atomize_eq sym intro!:ext)
 
 lemma partial_equivalence_subset: "B \<subseteq> A \<Longrightarrow> partial_equivalence B (\<sim>)"
   apply (intro partial_equivalence.intro partial_equivalence_axioms.intro)
   using symmetric_subset transitive_subset by auto
 
 end
 
 lemma partial_equivalence_cong:
   assumes r: "\<And>a b. a \<in> A \<Longrightarrow> b \<in> A \<Longrightarrow> r a b \<longleftrightarrow> r' a b"
   shows "partial_equivalence A r \<longleftrightarrow> partial_equivalence A r'"
   by (simp add: partial_equivalence_def partial_equivalence_axioms_def r
       cong: transitive_cong symmetric_cong)
 
 locale equivalence = symmetric + reflexive A "(\<sim>)" + transitive A "(\<sim>)"
 begin
 
 sublocale tolerance + partial_equivalence + quasi_ordered_set A "(\<sim>)"..
 
 lemma equivalence_subset: "B \<subseteq> A \<Longrightarrow> equivalence B (\<sim>)"
   apply (intro equivalence.intro)
   using symmetric_subset transitive_subset by auto
 
 end
 
 lemma equivalence_cong:
   assumes r: "\<And>a b. a \<in> A \<Longrightarrow> b \<in> A \<Longrightarrow> r a b \<longleftrightarrow> r' a b"
   shows "equivalence A r \<longleftrightarrow> equivalence A r'"
   by (simp add: equivalence_def r cong: reflexive_cong transitive_cong symmetric_cong)
 
 text \<open>Some combinations lead to uninteresting relations.\<close>
 
 context
   fixes r :: "'a \<Rightarrow> 'a \<Rightarrow> bool" (infix "\<bowtie>" 50)
 begin
 
 proposition reflexive_irreflexive_is_empty:
   assumes r: "reflexive A (\<bowtie>)" and ir: "irreflexive A (\<bowtie>)"
   shows "A = {}"
 proof (rule ccontr)
   interpret irreflexive A "(\<bowtie>)" using ir.
   interpret reflexive A "(\<bowtie>)" using r.
   assume "A \<noteq> {}"
   then obtain a where a: "a \<in> A" by auto
   from a refl have "a \<bowtie> a" by auto
   with irrefl a show False by auto
 qed
 
 proposition symmetric_antisymmetric_imp_eq:
   assumes s: "symmetric A (\<bowtie>)" and as: "antisymmetric A (\<bowtie>)"
   shows "(\<bowtie>)\<restriction>A \<le> (=)"
 proof-
   interpret symmetric A "(\<bowtie>)" + antisymmetric A "(\<bowtie>)" using assms by auto
   show "?thesis" using antisym by (auto dest: sym)
 qed
 
 proposition nontolerance:
   shows "irreflexive A (\<bowtie>) \<and> symmetric A (\<bowtie>) \<longleftrightarrow> tolerance A (\<lambda>x y. \<not> x \<bowtie> y)"
 proof (intro iffI conjI, elim conjE)
   assume "irreflexive A (\<bowtie>)" and "symmetric A (\<bowtie>)"
   then interpret irreflexive A "(\<bowtie>)" + symmetric A "(\<bowtie>)".
   show "tolerance A (\<lambda>x y. \<not> x \<bowtie> y)" by (unfold_locales, auto dest: sym irrefl)
 next
   assume "tolerance A (\<lambda>x y. \<not> x \<bowtie> y)"
   then interpret tolerance A "\<lambda>x y. \<not> x \<bowtie> y".
   show "irreflexive A (\<bowtie>)" by (auto simp: eq_implies)
   show "symmetric A (\<bowtie>)" using sym by auto
 qed
 
 proposition irreflexive_transitive_symmetric_is_empty:
   assumes irr: "irreflexive A (\<bowtie>)" and tr: "transitive A (\<bowtie>)" and sym: "symmetric A (\<bowtie>)"
   shows "(\<bowtie>)\<restriction>A = bot"
 proof (intro ext, unfold bot_fun_def bot_bool_def eq_False, rule notI, erule RestrpE)
   interpret strict_ordered_set A "(\<bowtie>)" using assms by (unfold strict_ordered_set_def, auto)
   interpret symmetric A "(\<bowtie>)" using assms by auto
   fix x y assume x: "x \<in> A" and y: "y \<in> A"
   assume xy: "x \<bowtie> y"
   also note sym[OF xy x y]
   finally have "x \<bowtie> x" using x y by auto
   with x show False by auto
 qed
 
 end
 
 subsection \<open>Totality\<close>
 
 locale semiconnex = related_set A "(\<sqsubset>)" for A and less (infix "\<sqsubset>" 50) +
   assumes semiconnex: "x \<in> A \<Longrightarrow> y \<in> A \<Longrightarrow> x \<sqsubset> y \<or> x = y \<or> y \<sqsubset> x"
 begin
 
 lemma cases[consumes 2, case_names less eq greater]:
   assumes "x \<in> A" and "y \<in> A" and "x \<sqsubset> y \<Longrightarrow> P" and "x = y \<Longrightarrow> P" and "y \<sqsubset> x \<Longrightarrow> P"
   shows "P" using semiconnex assms by auto
 
 lemma neqE:
   assumes "x \<in> A" and "y \<in> A"
   shows "x \<noteq> y \<Longrightarrow> (x \<sqsubset> y \<Longrightarrow> P) \<Longrightarrow> (y \<sqsubset> x \<Longrightarrow> P) \<Longrightarrow> P"
   by (cases rule: cases[OF assms], auto)
 
 lemma semiconnex_subset: "B \<subseteq> A \<Longrightarrow> semiconnex B (\<sqsubset>)"
   apply (intro semiconnex.intro)
   using semiconnex by auto
 
 end
 
 declare semiconnex.intro[intro]
 
 text \<open>Totality is negated antisymmetry \cite[Proposition 2.2.4]{Schmidt1993}.\<close>
 proposition semiconnex_iff_neg_antisymmetric:
   fixes less (infix "\<sqsubset>" 50)
   shows "semiconnex A (\<sqsubset>) \<longleftrightarrow> antisymmetric A (\<lambda>x y. \<not> x \<sqsubset> y)" (is "?l \<longleftrightarrow> ?r")
 proof (intro iffI semiconnex.intro antisymmetric.intro)
   assume ?l
   then interpret semiconnex.
   fix x y
   assume "x \<in> A" "y \<in> A" "\<not> x \<sqsubset> y" and "\<not> y \<sqsubset> x"
   then show "x = y" by (cases rule: cases, auto)
 next
   assume ?r
   then interpret neg: antisymmetric A "(\<lambda>x y. \<not> x \<sqsubset> y)".
   fix x y
   show "x \<in> A \<Longrightarrow> y \<in> A \<Longrightarrow> x \<sqsubset> y \<or> x = y \<or> y \<sqsubset> x" using neg.antisym by auto
 qed
 
 lemma semiconnex_cong:
   assumes r: "\<And>a b. a \<in> A \<Longrightarrow> b \<in> A \<Longrightarrow> r a b \<longleftrightarrow> r' a b"
   shows "semiconnex A r \<longleftrightarrow> semiconnex A r'"
   by (simp add: semiconnex_iff_neg_antisymmetric r cong: antisymmetric_cong)
 
 locale semiconnex_irreflexive = semiconnex + irreflexive
 begin
 
 lemma neq_iff: "x \<in> A \<Longrightarrow> y \<in> A \<Longrightarrow> x \<noteq> y \<longleftrightarrow> x \<sqsubset> y \<or> y \<sqsubset> x" by (auto elim:neqE dest: irrefl)
 
 lemma semiconnex_irreflexive_subset: "B \<subseteq> A \<Longrightarrow> semiconnex_irreflexive B (\<sqsubset>)"
   apply (intro semiconnex_irreflexive.intro)
   using semiconnex_subset irreflexive_subset by auto
 
 end
 
 lemma semiconnex_irreflexive_cong:
   assumes r: "\<And>a b. a \<in> A \<Longrightarrow> b \<in> A \<Longrightarrow> r a b \<longleftrightarrow> r' a b"
   shows "semiconnex_irreflexive A r \<longleftrightarrow> semiconnex_irreflexive A r'"
   by (simp add: semiconnex_irreflexive_def r cong: semiconnex_cong irreflexive_cong)
 
 locale connex = related_set +
   assumes comparable: "x \<in> A \<Longrightarrow> y \<in> A \<Longrightarrow> x \<sqsubseteq> y \<or> y \<sqsubseteq> x"
 begin
 
 interpretation less_eq_notations.
 
 sublocale reflexive apply unfold_locales using comparable by auto
 
 lemma comparable_cases[consumes 2, case_names le ge]:
   assumes "x \<in> A" and "y \<in> A" and "x \<sqsubseteq> y \<Longrightarrow> P" and "y \<sqsubseteq> x \<Longrightarrow> P" shows "P"
   using assms comparable by auto
 
 lemma comparable_three_cases[consumes 2, case_names less eq greater]:
   assumes "x \<in> A" and "y \<in> A" and "x \<sqsubset> y \<Longrightarrow> P" and "x \<sim> y \<Longrightarrow> P" and "y \<sqsubset> x \<Longrightarrow> P" shows "P"
   using assms comparable by auto
 
 lemma
   assumes x: "x \<in> A" and y: "y \<in> A"
   shows not_iff_asym: "\<not>x \<sqsubseteq> y \<longleftrightarrow> y \<sqsubset> x"
     and not_asym_iff[simp]: "\<not>x \<sqsubset> y \<longleftrightarrow> y \<sqsubseteq> x"
   using comparable[OF x y] by auto
 
 lemma connex_subset: "B \<subseteq> A \<Longrightarrow> connex B (\<sqsubseteq>)"
   by (intro connex.intro comparable, auto)
 
 end
 
 lemmas connexE = connex.comparable_cases
 
 lemmas connexI[intro] = connex.intro
 
 context
   fixes less_eq :: "'a \<Rightarrow> 'a \<Rightarrow> bool" (infix "\<sqsubseteq>" 50)
 begin
 
 lemma connex_iff_semiconnex_reflexive: "connex A (\<sqsubseteq>) \<longleftrightarrow> semiconnex A (\<sqsubseteq>) \<and> reflexive A (\<sqsubseteq>)"
   (is "?c \<longleftrightarrow> ?t \<and> ?r")
 proof (intro iffI conjI; (elim conjE)?)
   assume ?c then interpret connex.
   show ?t apply unfold_locales using comparable by auto
   show ?r by unfold_locales
 next
   assume ?t then interpret semiconnex A "(\<sqsubseteq>)".
   assume ?r then interpret reflexive.
   from semiconnex show ?c by auto
 qed
 
 lemma chain_connect: "Complete_Partial_Order.chain r A \<equiv> connex A r"
   by (auto intro!: ext simp: atomize_eq connex_def Complete_Partial_Order.chain_def)
 
 lemma connex_union:
   assumes "connex X (\<sqsubseteq>)" and "connex Y (\<sqsubseteq>)" and "\<forall>x \<in> X. \<forall>y \<in> Y. x \<sqsubseteq> y \<or> y \<sqsubseteq> x"
   shows "connex (X\<union>Y) (\<sqsubseteq>)"
   using assms by (auto simp: connex_def)
 
 end
 
 lemma connex_cong:
   assumes r: "\<And>a b. a \<in> A \<Longrightarrow> b \<in> A \<Longrightarrow> r a b \<longleftrightarrow> r' a b"
   shows "connex A r \<longleftrightarrow> connex A r'"
   by (simp add: connex_iff_semiconnex_reflexive r cong: semiconnex_cong reflexive_cong)
 
 locale total_pseudo_ordered_set = connex + antisymmetric
 begin
 
 sublocale pseudo_ordered_set ..
 
 lemma not_weak_iff:
   assumes x: "x \<in> A" and y: "y \<in> A" shows "\<not> y \<sqsubseteq> x \<longleftrightarrow> x \<sqsubseteq> y \<and> x \<noteq> y"
 using x y by (cases rule: comparable_cases, auto intro:antisym)
 
 lemma total_pseudo_ordered_subset: "B \<subseteq> A \<Longrightarrow> total_pseudo_ordered_set B (\<sqsubseteq>)"
   apply (intro_locales)
   using antisymmetric_subset connex_subset by auto
 
 end
 
 lemma total_pseudo_ordered_set_cong:
   assumes r: "\<And>a b. a \<in> A \<Longrightarrow> b \<in> A \<Longrightarrow> r a b \<longleftrightarrow> r' a b"
   shows "total_pseudo_ordered_set A r \<longleftrightarrow> total_pseudo_ordered_set A r'"
   by (simp add: total_pseudo_ordered_set_def r cong: connex_cong antisymmetric_cong)
 
 locale total_quasi_ordered_set = connex + transitive
 begin
 
 sublocale quasi_ordered_set ..
 
 lemma total_quasi_ordered_subset: "B \<subseteq> A \<Longrightarrow> total_quasi_ordered_set B (\<sqsubseteq>)"
   using transitive_subset connex_subset by intro_locales
 
 end
 
 lemma total_quasi_ordered_set_cong:
   assumes r: "\<And>a b. a \<in> A \<Longrightarrow> b \<in> A \<Longrightarrow> r a b \<longleftrightarrow> r' a b"
   shows "total_quasi_ordered_set A r \<longleftrightarrow> total_quasi_ordered_set A r'"
   by (simp add: total_quasi_ordered_set_def r cong: connex_cong transitive_cong)
 
 locale total_ordered_set = total_quasi_ordered_set + antisymmetric
 begin
 
 sublocale partially_ordered_set + total_pseudo_ordered_set ..
 
 lemma total_ordered_subset: "B \<subseteq> A \<Longrightarrow> total_ordered_set B (\<sqsubseteq>)"
   using total_quasi_ordered_subset antisymmetric_subset by (intro total_ordered_set.intro)
 
 end
 
 lemma total_ordered_set_cong:
   assumes r: "\<And>a b. a \<in> A \<Longrightarrow> b \<in> A \<Longrightarrow> r a b \<longleftrightarrow> r' a b"
   shows "total_ordered_set A r \<longleftrightarrow> total_ordered_set A r'"
   by (simp add: total_ordered_set_def r cong: total_quasi_ordered_set_cong antisymmetric_cong)
 
 subsection \<open>Well-Foundedness\<close>
 
 locale well_founded = related_set A "(\<sqsubset>)" for A and less (infix "\<sqsubset>" 50) +
   assumes induct[consumes 1, case_names less, induct set]:
     "a \<in> A \<Longrightarrow> (\<And>x. x \<in> A \<Longrightarrow> (\<And>y. y \<in> A \<Longrightarrow> y \<sqsubset> x \<Longrightarrow> P y) \<Longrightarrow> P x) \<Longrightarrow> P a"
 begin
 
 sublocale asymmetric
 proof (intro asymmetric.intro notI)
   fix x y
   assume xA: "x \<in> A"
   then show "y \<in> A \<Longrightarrow> x \<sqsubset> y \<Longrightarrow> y \<sqsubset> x \<Longrightarrow> False"
     by (induct arbitrary: y rule: induct, auto)
 qed
 
 lemma prefixed_Imagep_imp_empty:
   assumes a: "X \<subseteq> ((\<sqsubset>) ``` X) \<inter> A" shows "X = {}"
 proof -
   from a have XA: "X \<subseteq> A" by auto
   have "x \<in> A \<Longrightarrow> x \<notin> X" for x
   proof (induct x rule: induct)
     case (less x)
     with a show ?case by (auto simp: Imagep_def)
   qed
   with XA show ?thesis by auto
 qed
 
-lemma nonempty_imp_ex_minimal:
+lemma nonempty_imp_ex_extremal:
   assumes QA: "Q \<subseteq> A" and Q: "Q \<noteq> {}"
   shows "\<exists>z \<in> Q. \<forall>y \<in> Q. \<not> y \<sqsubset> z"
   using Q prefixed_Imagep_imp_empty[of Q] QA by (auto simp: Imagep_def)
 
 interpretation Restrp: well_founded UNIV "(\<sqsubset>)\<restriction>A"
   rewrites "\<And>x. x \<in> UNIV \<equiv> True"
     and "(\<sqsubset>)\<restriction>A\<restriction>UNIV = (\<sqsubset>)\<restriction>A"
     and "\<And>P1. (True \<Longrightarrow> PROP P1) \<equiv> PROP P1"
     and "\<And>P1. (True \<Longrightarrow> P1) \<equiv> Trueprop P1"
     and "\<And>P1 P2. (True \<Longrightarrow> PROP P1 \<Longrightarrow> PROP P2) \<equiv> (PROP P1 \<Longrightarrow> PROP P2)"
 proof -
   have "(\<And>x. (\<And>y. ((\<sqsubset>) \<restriction> A) y x \<Longrightarrow> P y) \<Longrightarrow> P x) \<Longrightarrow> P a" for a P
     using induct[of a P] by (auto simp: Restrp_def)
   then show "well_founded UNIV ((\<sqsubset>)\<restriction>A)" apply unfold_locales by auto
 qed auto
 
 lemmas Restrp_well_founded = Restrp.well_founded_axioms
 lemmas Restrp_induct[consumes 0, case_names less] = Restrp.induct
 
 interpretation Restrp.tranclp: well_founded UNIV "((\<sqsubset>)\<restriction>A)\<^sup>+\<^sup>+"
   rewrites "\<And>x. x \<in> UNIV \<equiv> True"
     and "((\<sqsubset>)\<restriction>A)\<^sup>+\<^sup>+ \<restriction> UNIV = ((\<sqsubset>)\<restriction>A)\<^sup>+\<^sup>+"
     and "(((\<sqsubset>)\<restriction>A)\<^sup>+\<^sup>+)\<^sup>+\<^sup>+ = ((\<sqsubset>)\<restriction>A)\<^sup>+\<^sup>+"
     and "\<And>P1. (True \<Longrightarrow> PROP P1) \<equiv> PROP P1"
     and "\<And>P1. (True \<Longrightarrow> P1) \<equiv> Trueprop P1"
     and "\<And>P1 P2. (True \<Longrightarrow> PROP P1 \<Longrightarrow> PROP P2) \<equiv> (PROP P1 \<Longrightarrow> PROP P2)"
 proof-
   { fix P x
     assume induct_step: "\<And>x. (\<And>y. ((\<sqsubset>)\<restriction>A)\<^sup>+\<^sup>+ y x \<Longrightarrow> P y) \<Longrightarrow> P x"
     have "P x"
     proof (rule induct_step)
       show "\<And>y. ((\<sqsubset>)\<restriction>A)\<^sup>+\<^sup>+ y x \<Longrightarrow> P y"
       proof (induct x rule: Restrp_induct)
         case (less x)
         from \<open>((\<sqsubset>)\<restriction>A)\<^sup>+\<^sup>+ y x\<close>
         show ?case
         proof (cases rule: tranclp.cases)
           case r_into_trancl
           with induct_step less show ?thesis by auto
         next
           case (trancl_into_trancl b)
           with less show ?thesis by auto
         qed
       qed
     qed
   }
   then show "well_founded UNIV ((\<sqsubset>)\<restriction>A)\<^sup>+\<^sup>+" by unfold_locales auto
 qed auto
 
 lemmas Restrp_tranclp_well_founded = Restrp.tranclp.well_founded_axioms
 lemmas Restrp_tranclp_induct[consumes 0, case_names less] = Restrp.tranclp.induct
 
 end
 
 context
   fixes A :: "'a set" and less :: "'a \<Rightarrow> 'a \<Rightarrow> bool" (infix "\<sqsubset>" 50)
 begin
 
 lemma well_foundedI_pf:
   assumes pre: "\<And>X. X \<subseteq> A \<Longrightarrow> X \<subseteq> ((\<sqsubset>) ``` X) \<inter> A \<Longrightarrow> X = {}"
   shows "well_founded A (\<sqsubset>)"
 proof
   fix P a assume aA: "a \<in> A" and Ind: "\<And>x. x \<in> A \<Longrightarrow> (\<And>y. y \<in> A \<Longrightarrow> y \<sqsubset> x \<Longrightarrow> P y) \<Longrightarrow> P x"
   from Ind have "{a\<in>A. \<not>P a} \<subseteq> ((\<sqsubset>) ``` {a\<in>A. \<not>P a}) \<inter> A" by (auto simp: Imagep_def)
   from pre[OF _ this] aA
   show "P a" by auto
 qed
 
-lemma well_foundedI_min:
+lemma well_foundedI_extremal:
   assumes a: "\<And>X. X \<subseteq> A \<Longrightarrow> X \<noteq> {} \<Longrightarrow> \<exists>x \<in> X. \<forall>y \<in> X. \<not> y \<sqsubset> x"
   shows "well_founded A (\<sqsubset>)"
 proof (rule well_foundedI_pf)
   fix X assume XA: "X \<subseteq> A" and pf: "X \<subseteq> ((\<sqsubset>) ``` X) \<inter> A"
   from a[OF XA] pf show "X = {}" by (auto simp: Imagep_def)
 qed
 
-lemma well_founded_iff_ex_minimal:
+lemma well_founded_iff_ex_extremal:
   "well_founded A (\<sqsubset>) \<longleftrightarrow> (\<forall>X \<subseteq> A. X \<noteq> {} \<longrightarrow> (\<exists>x \<in> X. \<forall>z \<in> X. \<not> z \<sqsubset> x))"
-  using well_founded.nonempty_imp_ex_minimal well_foundedI_min by blast
+  using well_founded.nonempty_imp_ex_extremal well_foundedI_extremal by blast
 
 end
 
 lemma well_founded_cong:
   assumes r: "\<And>a b. a \<in> A \<Longrightarrow> b \<in> A \<Longrightarrow> r a b \<longleftrightarrow> r' a b"
     and A: "\<And>a b. r' a b \<Longrightarrow> a \<in> A \<longleftrightarrow> a \<in> A'"
     and B: "\<And>a b. r' a b \<Longrightarrow> b \<in> A \<longleftrightarrow> b \<in> A'"
   shows "well_founded A r \<longleftrightarrow> well_founded A' r'"
 proof (intro iffI)
   assume wf: "well_founded A r"
   show "well_founded A' r'"
-  proof (intro well_foundedI_min)
+  proof (intro well_foundedI_extremal)
     fix X
     assume X: "X \<subseteq> A'" and X0: "X \<noteq> {}"
     show "\<exists>x\<in>X. \<forall>y\<in>X. \<not> r' y x"
     proof (cases "X \<inter> A = {}")
       case True
       from X0 obtain x where xX: "x \<in> X" by auto
       with True have "x \<notin> A" by auto
       with xX X have "\<forall>y\<in>X. \<not> r' y x" by (auto simp: B)
       with xX show ?thesis by auto
     next
       case False
-      from well_founded.nonempty_imp_ex_minimal[OF wf _ this]
+      from well_founded.nonempty_imp_ex_extremal[OF wf _ this]
       obtain x where x: "x \<in> X \<inter> A" and Ar: "\<And>y. y \<in> X \<Longrightarrow> y \<in> A \<Longrightarrow> \<not> r y x" by auto
       have "\<forall>y \<in> X. \<not> r' y x"
       proof (intro ballI notI)
         fix y assume yX: "y \<in> X" and yx: "r' y x"
         from yX X have yA': "y \<in> A'" by auto
         show False
         proof (cases "y \<in> A")
           case True with x Ar[OF yX] yx r show ?thesis by auto
         next
           case False with yA' x A[OF yx] r X show ?thesis by (auto simp:)
         qed
       qed
       with x show "\<exists>x \<in> X. \<forall>y \<in> X. \<not> r' y x" by auto
     qed
   qed
 next
   assume wf: "well_founded A' r'"
   show "well_founded A r"
-  proof (intro well_foundedI_min)
+  proof (intro well_foundedI_extremal)
     fix X
     assume X: "X \<subseteq> A" and X0: "X \<noteq> {}"
     show "\<exists>x\<in>X. \<forall>y\<in>X. \<not> r y x"
     proof (cases "X \<inter> A' = {}")
       case True
       from X0 obtain x where xX: "x \<in> X" by auto
       with True have "x \<notin> A'" by auto
       with xX X B have "\<forall>y\<in>X. \<not> r y x" by (auto simp: r in_mono)
       with xX show ?thesis by auto
     next
       case False
-      from well_founded.nonempty_imp_ex_minimal[OF wf _ this]
+      from well_founded.nonempty_imp_ex_extremal[OF wf _ this]
       obtain x where x: "x \<in> X \<inter> A'" and Ar: "\<And>y. y \<in> X \<Longrightarrow> y \<in> A' \<Longrightarrow> \<not> r' y x" by auto
       have "\<forall>y \<in> X. \<not> r y x"
       proof (intro ballI notI)
         fix y assume yX: "y \<in> X" and yx: "r y x"
         from yX X have y: "y \<in> A" by auto
         show False
         proof (cases "y \<in> A'")
           case True with x Ar[OF yX] yx r X y show ?thesis by auto
         next
           case False with y x A yx r X show ?thesis by auto
         qed
       qed
       with x show "\<exists>x \<in> X. \<forall>y \<in> X. \<not> r y x" by auto
     qed
   qed
 qed
 
 lemma wfP_iff_well_founded_UNIV: "wfP r \<longleftrightarrow> well_founded UNIV r"
   by (auto simp: wfP_def wf_def well_founded_def)
 
 lemma well_founded_singleton:
   assumes "\<not>r x x" shows "well_founded {x} r"
-  using assms by (auto simp: well_founded_iff_ex_minimal)
+  using assms by (auto simp: well_founded_iff_ex_extremal)
 
 lemma well_founded_Restrp[simp]: "well_founded A (r\<restriction>B) \<longleftrightarrow> well_founded (A\<inter>B) r" (is "?l \<longleftrightarrow> ?r")
-proof (intro iffI well_foundedI_min)
+proof (intro iffI well_foundedI_extremal)
   assume l: ?l
   fix X assume XAB: "X \<subseteq> A \<inter> B" and X0: "X \<noteq> {}"
-  with l[THEN well_founded.nonempty_imp_ex_minimal]
+  with l[THEN well_founded.nonempty_imp_ex_extremal]
   have "\<exists>x\<in>X. \<forall>z\<in>X. \<not> (r \<restriction> B) z x" by auto
   with XAB show "\<exists>x\<in>X. \<forall>y\<in>X. \<not> r y x" by (auto simp: Restrp_def)
 next
   assume r: ?r
   fix X assume XA: "X \<subseteq> A" and X0: "X \<noteq> {}"
   show "\<exists>x\<in>X. \<forall>y\<in>X. \<not> (r \<restriction> B) y x"
   proof (cases "X \<subseteq> B")
     case True
-    with r[THEN well_founded.nonempty_imp_ex_minimal, of X] XA X0
+    with r[THEN well_founded.nonempty_imp_ex_extremal, of X] XA X0
     have "\<exists>z\<in>X. \<forall>y\<in>X. \<not> r y z" by auto
     then show ?thesis by auto
   next
     case False
     then obtain x where x: "x \<in> X - B" by auto
     then have "\<forall>y\<in>X. \<not> (r \<restriction> B) y x" by auto
     with x show ?thesis by auto
   qed
 qed
 
 lemma (in well_founded) well_founded_subset:
   assumes "B \<subseteq> A" shows "well_founded B (\<sqsubset>)"
-  using assms well_founded_axioms by (auto simp: well_founded_iff_ex_minimal)
+  using assms well_founded_axioms by (auto simp: well_founded_iff_ex_extremal)
 
 lemma well_founded_extend:
   fixes less (infix "\<sqsubset>" 50)
   assumes A: "well_founded A (\<sqsubset>)"
   assumes B: "well_founded B (\<sqsubset>)"
   assumes AB: "\<forall>a \<in> A. \<forall>b \<in> B. \<not>b \<sqsubset> a"
   shows "well_founded (A \<union> B) (\<sqsubset>)"
-proof (intro well_foundedI_min)
+proof (intro well_foundedI_extremal)
   interpret A: well_founded A "(\<sqsubset>)" using A.
   interpret B: well_founded B "(\<sqsubset>)" using B.
   fix X assume XAB: "X \<subseteq> A \<union> B" and X0: "X \<noteq> {}"
   show "\<exists>x\<in>X. \<forall>y\<in>X. \<not> y \<sqsubset> x"
   proof (cases "X \<inter> A = {}")
     case True
     with XAB have XB: "X \<subseteq> B" by auto
-    from B.nonempty_imp_ex_minimal[OF XB X0] show ?thesis.
+    from B.nonempty_imp_ex_extremal[OF XB X0] show ?thesis.
   next
     case False
-    with A.nonempty_imp_ex_minimal[OF _ this]
+    with A.nonempty_imp_ex_extremal[OF _ this]
     obtain e where XAe: "e \<in> X \<inter> A" "\<forall>y\<in>X \<inter> A. \<not> y \<sqsubset> e" by auto
     then have eX: "e \<in> X" and eA: "e \<in> A" by auto
     { fix x assume xX: "x \<in> X"
       have "\<not>x \<sqsubset> e"
       proof (cases "x \<in> A")
         case True with XAe xX show ?thesis by auto
       next
         case False
         with xX XAB have "x \<in> B" by auto
         with AB eA show ?thesis by auto
       qed
     }
     with eX show ?thesis by auto
   qed
 qed
 
-lemma lower_UN_well_founded:
+lemma closed_UN_well_founded:
   fixes r (infix "\<sqsubset>" 50)
   assumes XX: "\<forall>X\<in>XX. well_founded X (\<sqsubset>) \<and> (\<forall>x\<in>X. \<forall>y\<in>\<Union>XX. y \<sqsubset> x \<longrightarrow> y \<in> X)"
   shows "well_founded (\<Union>XX) (\<sqsubset>)"
-proof (intro well_foundedI_min)
+proof (intro well_foundedI_extremal)
   have *: "X \<in> XX \<Longrightarrow> x\<in>X \<Longrightarrow> y \<in> \<Union>XX \<Longrightarrow> y \<sqsubset> x \<Longrightarrow> y \<in> X" for X x y using XX by blast
   fix S
   assume S: "S \<subseteq> \<Union>XX" and S0: "S \<noteq> {}"
   from S0 obtain x where xS: "x \<in> S" by auto
   with S obtain X where X: "X \<in> XX" and xX: "x \<in> X" by auto
   from xS xX have Sx0: "S \<inter> X \<noteq> {}" by auto
   from X XX interpret well_founded X "(\<sqsubset>)" by auto
-  from nonempty_imp_ex_minimal[OF _ Sx0]
+  from nonempty_imp_ex_extremal[OF _ Sx0]
   obtain z where zS: "z \<in> S" and zX: "z \<in> X" and min: "\<forall>y \<in> S \<inter> X. \<not> y \<sqsubset> z" by auto
   show "\<exists>x\<in>S. \<forall>y\<in>S. \<not> y \<sqsubset> x"
   proof (intro bexI[OF _ zS] ballI notI)
     fix y
     assume yS: "y \<in> S" and yz: "y \<sqsubset> z"
     have yXX: "y \<in> \<Union> XX" using S yS by auto
     from *[OF X zX yXX yz] yS have "y \<in> X \<inter> S" by auto
     with min yz show False by auto
   qed
 qed
 
 lemma well_founded_cmono:
   assumes r': "r' \<le> r" and wf: "well_founded A r"
   shows "well_founded A r'"
-proof (intro well_foundedI_min)
+proof (intro well_foundedI_extremal)
   fix X assume "X \<subseteq> A" and "X \<noteq> {}"
-  from well_founded.nonempty_imp_ex_minimal[OF wf this]
+  from well_founded.nonempty_imp_ex_extremal[OF wf this]
   show "\<exists>x\<in>X. \<forall>y\<in>X. \<not> r' y x" using r' by auto
 qed
 
 locale well_founded_ordered_set = well_founded + transitive _ "(\<sqsubset>)"
 begin
 
 sublocale strict_ordered_set..
 
 interpretation Restrp: strict_ordered_set UNIV "(\<sqsubset>)\<restriction>A" + Restrp: well_founded UNIV "(\<sqsubset>)\<restriction>A"
   using Restrp_strict_order Restrp_well_founded .
 
 lemma Restrp_well_founded_order: "well_founded_ordered_set UNIV ((\<sqsubset>)\<restriction>A)"..
 
 lemma well_founded_ordered_subset: "B \<subseteq> A \<Longrightarrow> well_founded_ordered_set B (\<sqsubset>)"
   apply intro_locales
   using well_founded_subset transitive_subset by auto
 
 end
 
 lemma (in well_founded) Restrp_tranclp_well_founded_ordered: "well_founded_ordered_set UNIV ((\<sqsubset>)\<restriction>A)\<^sup>+\<^sup>+"
   using Restrp_tranclp_well_founded tranclp_transitive by intro_locales
 
 locale well_related_set = related_set +
   assumes nonempty_imp_ex_extreme: "X \<subseteq> A \<Longrightarrow> X \<noteq> {} \<Longrightarrow> \<exists>e. extreme X (\<sqsubseteq>)\<^sup>- e"
 begin
 
 sublocale connex
 proof
   fix x y assume "x \<in> A" and "y \<in> A"
   with nonempty_imp_ex_extreme[of "{x,y}"] show "x \<sqsubseteq> y \<or> y \<sqsubseteq> x" by auto 
 qed
 
 lemmas connex_axioms = connex_axioms
 
 interpretation less_eq_notations.
 
 sublocale asym: well_founded A "(\<sqsubset>)"
-proof (unfold well_founded_iff_ex_minimal, intro allI impI)
+proof (unfold well_founded_iff_ex_extremal, intro allI impI)
   fix X
   assume XA: "X \<subseteq> A" and X0: "X \<noteq> {}"
   from nonempty_imp_ex_extreme[OF XA X0] obtain e where "extreme X (\<sqsubseteq>)\<^sup>- e" by auto
   then show "\<exists>x\<in>X. \<forall>z\<in>X. \<not>z \<sqsubset> x" by (auto intro!: bexI[of _ e])
 qed
 
 lemma well_related_subset: "B \<subseteq> A \<Longrightarrow> well_related_set B (\<sqsubseteq>)"
   by (auto intro!: well_related_set.intro nonempty_imp_ex_extreme)
 
 end
 
 context
   fixes less_eq :: "'a \<Rightarrow> 'a \<Rightarrow> bool" (infix "\<sqsubseteq>" 50)
 begin
 
 lemma well_related_iff_neg_well_founded:
   "well_related_set A (\<sqsubseteq>) \<longleftrightarrow> well_founded A (\<lambda>x y. \<not> y \<sqsubseteq> x)"
-  by (simp add: well_related_set_def well_founded_iff_ex_minimal extreme_def Bex_def)
+  by (simp add: well_related_set_def well_founded_iff_ex_extremal extreme_def Bex_def)
 
 lemma well_related_singleton_refl: 
   assumes "x \<sqsubseteq> x" shows "well_related_set {x} (\<sqsubseteq>)"
   by (intro well_related_set.intro exI[of _ x], auto simp: subset_singleton_iff assms)
 
-lemma lower_UN_well_related:
+lemma closed_UN_well_related:
   assumes XX: "\<forall>X\<in>XX. well_related_set X (\<sqsubseteq>) \<and> (\<forall>x\<in>X. \<forall>y\<in>\<Union>XX. \<not>x \<sqsubseteq> y \<longrightarrow> y \<in> X)"
   shows "well_related_set (\<Union>XX) (\<sqsubseteq>)"
   using XX
   apply (unfold well_related_iff_neg_well_founded)
-  using lower_UN_well_founded[of _ "\<lambda>x y. \<not> y \<sqsubseteq> x"].
+  using closed_UN_well_founded[of _ "\<lambda>x y. \<not> y \<sqsubseteq> x"].
 
 end
 
 lemma well_related_extend:
   fixes r (infix "\<sqsubseteq>" 50)
   assumes "well_related_set A (\<sqsubseteq>)" and "well_related_set B (\<sqsubseteq>)" and "\<forall>a \<in> A. \<forall>b \<in> B. a \<sqsubseteq> b"
   shows "well_related_set (A \<union> B) (\<sqsubseteq>)"
   using well_founded_extend[of _ "\<lambda>x y. \<not> y \<sqsubseteq> x", folded well_related_iff_neg_well_founded]
   using assms by auto
 
 locale pre_well_ordered_set = semiattractive + well_related_set
 begin
 
 interpretation less_eq_notations.
 
 sublocale transitive
 proof
   fix x y z assume xy: "x \<sqsubseteq> y" and yz: "y \<sqsubseteq> z" and x: "x \<in> A" and y: "y \<in> A" and z: "z \<in> A"
   from x y z have "\<exists>e. extreme {x,y,z} (\<sqsupseteq>) e" (is "\<exists>e. ?P e") by (auto intro!: nonempty_imp_ex_extreme)
   then have "?P x \<or> ?P y \<or> ?P z" by auto
   then show "x \<sqsubseteq> z"
   proof (elim disjE)
     assume "?P x"
     then show ?thesis by auto
   next
     assume "?P y"
     then have "y \<sqsubseteq> x" by auto
     from attract[OF xy this yz] x y z show ?thesis by auto
   next
     assume "?P z"
     then have zx: "z \<sqsubseteq> x" and zy: "z \<sqsubseteq> y" by auto
     from attract[OF yz zy zx] x y z have yx: "y \<sqsubseteq> x" by auto
     from attract[OF xy yx yz] x y z show ?thesis by auto
   qed
 qed
 
 sublocale total_quasi_ordered_set..
 
 lemmas connex_axioms = connex_axioms
 
 lemma strict_weak_trans[trans]:
   assumes xy: "x \<sqsubset> y" and yz: "y \<sqsubseteq> z" and x: "x \<in> A" and y: "y \<in> A" and z: "z \<in> A"
   shows "x \<sqsubset> z"
 proof (intro asympartpI notI)
   from trans xy yz x y z show "x \<sqsubseteq> z" by auto
   assume "z \<sqsubseteq> x"
   from trans[OF yz this] y z x have "y \<sqsubseteq> x" by auto
   with xy show False by auto
 qed
 
 lemma weak_strict_trans[trans]:
   assumes xy: "x \<sqsubseteq> y" and yz: "y \<sqsubset> z" and x: "x \<in> A" and y: "y \<in> A" and z: "z \<in> A"
   shows "x \<sqsubset> z"
 proof (intro asympartpI notI)
   from trans xy yz x y z show "x \<sqsubseteq> z" by auto
   assume "z \<sqsubseteq> x"
   from trans[OF this xy] z x y have "z \<sqsubseteq> y" by auto
   with yz show False by auto
 qed
 
 end
 
 lemma pre_well_ordered_iff:
   "pre_well_ordered_set A r \<longleftrightarrow> total_quasi_ordered_set A r \<and> well_founded A (asympartp r)"
   (is "?p \<longleftrightarrow> ?t \<and> ?w")
 proof safe
   assume ?p
   then interpret pre_well_ordered_set A r.
   show ?t ?w by unfold_locales
 next
   assume ?t
   then interpret total_quasi_ordered_set A r.
   assume ?w
   then have "well_founded UNIV (asympartp r \<restriction> A)" by simp
   also have "asympartp r \<restriction> A = (\<lambda>x y. \<not> r y x) \<restriction> A" by (intro ext, auto simp: not_iff_asym)
   finally have "well_related_set A r" by (simp add: well_related_iff_neg_well_founded)
   then show ?p by intro_locales
 qed
 
 lemma (in semiattractive) pre_well_ordered_iff_well_related:
   assumes XA: "X \<subseteq> A"
   shows "pre_well_ordered_set X (\<sqsubseteq>) \<longleftrightarrow> well_related_set X (\<sqsubseteq>)" (is "?l \<longleftrightarrow> ?r")
 proof
   interpret X: semiattractive X using semiattractive_subset[OF XA].
   { assume ?l
     then interpret X: pre_well_ordered_set X.
     show ?r by unfold_locales
   }
   assume ?r
   then interpret X: well_related_set X.
   show ?l by unfold_locales
 qed
 
 lemma semiattractive_extend:
   fixes r (infix "\<sqsubseteq>" 50)
   assumes A: "semiattractive A (\<sqsubseteq>)" and B: "semiattractive B (\<sqsubseteq>)"
     and AB: "\<forall>a \<in> A. \<forall>b \<in> B. a \<sqsubseteq> b \<and> \<not> b \<sqsubseteq> a"
   shows "semiattractive (A \<union> B) (\<sqsubseteq>)"
 proof-
   interpret A: semiattractive A "(\<sqsubseteq>)" using A.
   interpret B: semiattractive B "(\<sqsubseteq>)" using B.
   {
     fix x y z
     assume yB: "y \<in> B" and zA: "z \<in> A" and yz: "y \<sqsubseteq> z"
     have False using AB[rule_format, OF zA yB] yz by auto
   }
   note * = this
   show ?thesis 
     by (auto intro!: semiattractive.intro dest:* AB[rule_format] A.attract B.attract)
 qed
 
 lemma pre_well_order_extend:
   fixes r (infix "\<sqsubseteq>" 50)
   assumes A: "pre_well_ordered_set A (\<sqsubseteq>)" and B: "pre_well_ordered_set B (\<sqsubseteq>)"
     and AB: "\<forall>a \<in> A. \<forall>b \<in> B. a \<sqsubseteq> b \<and> \<not> b \<sqsubseteq> a"
   shows "pre_well_ordered_set (A\<union>B) (\<sqsubseteq>)"
 proof-
   interpret A: pre_well_ordered_set A "(\<sqsubseteq>)" using A.
   interpret B: pre_well_ordered_set B "(\<sqsubseteq>)" using B.
   show ?thesis
     apply (intro pre_well_ordered_set.intro well_related_extend semiattractive_extend)
     apply unfold_locales
     by (auto dest: AB[rule_format])
 qed
 
 locale well_ordered_set = antisymmetric + well_related_set
 begin
 
 sublocale pre_well_ordered_set..
 
 sublocale total_ordered_set..
 
 lemma well_ordered_subset: "B \<subseteq> A \<Longrightarrow> well_ordered_set B (\<sqsubseteq>)"
   using well_related_subset antisymmetric_subset by (intro well_ordered_set.intro)
 
 lemmas connex_axioms = connex_axioms
 
 end
 
 lemma (in antisymmetric) well_ordered_iff_well_related:
   assumes XA: "X \<subseteq> A"
   shows "well_ordered_set X (\<sqsubseteq>) \<longleftrightarrow> well_related_set X (\<sqsubseteq>)" (is "?l \<longleftrightarrow> ?r")
 proof
   interpret X: antisymmetric X using antisymmetric_subset[OF XA].
   { assume ?l
     then interpret X: well_ordered_set X.
     show ?r by unfold_locales
   }
   assume ?r
   then interpret X: well_related_set X.
   show ?l by unfold_locales
 qed
 
 context
   fixes A and less_eq (infix "\<sqsubseteq>" 50)
   assumes A: "\<forall>a \<in> A. \<forall>b \<in> A. a \<sqsubseteq> b"
 begin
 
 interpretation well_related_set A "(\<sqsubseteq>)"
   apply unfold_locales
   using A by blast
 
 lemmas trivial_well_related = well_related_set_axioms
 
 lemma trivial_pre_well_order: "pre_well_ordered_set A (\<sqsubseteq>)"
   apply unfold_locales
   using A by blast
 
 end
 
 context
   fixes less_eq :: "'a \<Rightarrow> 'a \<Rightarrow> bool" (infix "\<sqsubseteq>" 50)
 begin
 
 interpretation less_eq_notations.
 
 lemma well_order_extend:
   assumes A: "well_ordered_set A (\<sqsubseteq>)" and B: "well_ordered_set B (\<sqsubseteq>)"
     and ABa: "\<forall>a \<in> A. \<forall>b \<in> B. a \<sqsubseteq> b \<longrightarrow> b \<sqsubseteq> a \<longrightarrow> a = b"
     and AB: "\<forall>a \<in> A. \<forall>b \<in> B. a \<sqsubseteq> b"
   shows "well_ordered_set (A\<union>B) (\<sqsubseteq>)"
 proof-
   interpret A: well_ordered_set A "(\<sqsubseteq>)" using A.
   interpret B: well_ordered_set B "(\<sqsubseteq>)" using B.
   show ?thesis
     apply (intro well_ordered_set.intro antisymmetric_union well_related_extend ABa AB)
     by unfold_locales
 qed
 
 interpretation singleton: antisymmetric "{a}" "(\<sqsubseteq>)" for a apply unfold_locales by auto
 
 lemmas singleton_antisymmetric[intro!] = singleton.antisymmetric_axioms
 
 lemma singleton_well_ordered[intro!]: "a \<sqsubseteq> a \<Longrightarrow> well_ordered_set {a} (\<sqsubseteq>)"
   apply unfold_locales by auto
 
-lemma lower_UN_well_ordered:
+lemma closed_UN_well_ordered:
   assumes anti: "antisymmetric (\<Union> XX) (\<sqsubseteq>)"
     and XX: "\<forall>X\<in>XX. well_ordered_set X (\<sqsubseteq>) \<and> (\<forall>x\<in>X. \<forall>y\<in>\<Union>XX. \<not> x \<sqsubseteq> y \<longrightarrow> y \<in> X)"
   shows "well_ordered_set (\<Union>XX) (\<sqsubseteq>)"
-  apply (intro well_ordered_set.intro lower_UN_well_related anti)
+  apply (intro well_ordered_set.intro closed_UN_well_related anti)
   using XX well_ordered_set.axioms by fast
 
 end
 
 text \<open>Directed sets:\<close>
 
 definition "directed A r \<equiv> \<forall>x \<in> A. \<forall>y \<in> A. \<exists>z \<in> A. r x z \<and> r y z"
 
 lemmas directedI[intro] = directed_def[unfolded atomize_eq, THEN iffD2, rule_format]
 
 lemmas directedD = directed_def[unfolded atomize_eq, THEN iffD1, rule_format]
 
 context
   fixes less_eq :: "'a \<Rightarrow> 'a \<Rightarrow> bool" (infix "\<sqsubseteq>" 50)
 begin
 
 lemma directedE:
   assumes "directed A (\<sqsubseteq>)" and "x \<in> A" and "y \<in> A"
     and "\<And>z. z \<in> A \<Longrightarrow> x \<sqsubseteq> z \<Longrightarrow> y \<sqsubseteq> z \<Longrightarrow> thesis"
   shows "thesis"
   using assms by (auto dest: directedD)
 
 lemma directed_empty[simp]: "directed {} (\<sqsubseteq>)" by auto
 
 lemma directed_union:
   assumes dX: "directed X (\<sqsubseteq>)" and dY: "directed Y (\<sqsubseteq>)"
     and XY: "\<forall>x\<in>X. \<forall>y\<in>Y. \<exists>z \<in> X \<union> Y. x \<sqsubseteq> z \<and> y \<sqsubseteq> z"
   shows "directed (X \<union> Y) (\<sqsubseteq>)"
   using directedD[OF dX] directedD[OF dY] XY
   apply (intro directedI) by blast
 
 lemma directed_extend:
   assumes X: "directed X (\<sqsubseteq>)" and Y: "directed Y (\<sqsubseteq>)" and XY: "\<forall>x\<in>X. \<forall>y\<in>Y. x \<sqsubseteq> y"
   shows "directed (X \<union> Y) (\<sqsubseteq>)"
 proof -
   { fix x y
     assume xX: "x \<in> X" and yY: "y \<in> Y"
     let ?g = "\<exists>z\<in>X \<union> Y. x \<sqsubseteq> z \<and> y \<sqsubseteq> z"
     from directedD[OF Y yY yY] obtain z where zY: "z \<in> Y" and yz: "y \<sqsubseteq> z" by auto
     from xX XY zY yz have ?g by auto
   }
   then show ?thesis by (auto intro!: directed_union[OF X Y])
 qed
 
 end
 
 context connex begin
 
 lemma directed: "directed A (\<sqsubseteq>)"
 proof
   fix x y
   assume x: "x \<in> A" and y: "y \<in> A"
   then show "\<exists>z\<in>A. x \<sqsubseteq> z \<and> y \<sqsubseteq> z"
   proof (cases rule: comparable_cases)
     case le
     with refl[OF y] y show ?thesis by (intro bexI[of _ y], auto)
   next
     case ge
     with refl[OF x] x show ?thesis by (intro bexI[of _ x], auto)
   qed
 qed
 
 end
 
 context
   fixes ir :: "'i \<Rightarrow> 'i \<Rightarrow> bool" (infix "\<preceq>" 50)
   fixes r :: "'a \<Rightarrow> 'a \<Rightarrow> bool" (infix "\<sqsubseteq>" 50)
 begin
 
 lemma monotone_connex_image:
   assumes mono: "monotone_on I (\<preceq>) (\<sqsubseteq>) f"
   assumes connex: "connex I (\<preceq>)"
   shows "connex (f ` I) (\<sqsubseteq>)"
 proof (rule connexI)
   fix x y
   assume "x \<in> f ` I" and "y \<in> f ` I"
   then obtain i j where ij: "i \<in> I" "j \<in> I" and [simp]: "x = f i" "y = f j" by auto
   from connex ij have "i \<preceq> j \<or> j \<preceq> i" by (auto elim: connexE)
   with ij mono show "x \<sqsubseteq> y \<or> y \<sqsubseteq> x" by (elim disjE, auto dest: monotone_onD) 
 qed
 
 lemma monotone_directed_image:
   assumes mono: "monotone_on I (\<preceq>) (\<sqsubseteq>) f"
   assumes dir: "directed I (\<preceq>)" shows "directed (f ` I) (\<sqsubseteq>)"
 proof (rule directedI, safe)
   fix x y assume x: "x \<in> I" and y: "y \<in> I"
   with dir obtain z where z: "z \<in> I" and "x \<preceq> z" and "y \<preceq> z" by (auto elim: directedE)
   with mono x y have "f x \<sqsubseteq> f z" and "f y \<sqsubseteq> f z" by (auto dest: monotone_onD)
   with z show "\<exists>fz \<in> f ` I. f x \<sqsubseteq> fz \<and> f y \<sqsubseteq> fz" by auto
 qed
 
 end
 
 subsection \<open>Order Pairs\<close>
 
 locale compatible = related_set + related_set A "(\<sqsubset>)" for less (infix "\<sqsubset>" 50) +
   assumes compat_right[trans]: "x \<sqsubseteq> y \<Longrightarrow> y \<sqsubset> z \<Longrightarrow> x \<in> A \<Longrightarrow> y \<in> A \<Longrightarrow> z \<in> A \<Longrightarrow> x \<sqsubset> z"
   assumes compat_left[trans]: "x \<sqsubset> y \<Longrightarrow> y \<sqsubseteq> z \<Longrightarrow> x \<in> A \<Longrightarrow> y \<in> A \<Longrightarrow> z \<in> A \<Longrightarrow> x \<sqsubset> z"
 
 locale compatible_ordering = reflexive + irreflexive + compatible +
   assumes strict_implies_weak: "x \<sqsubset> y \<Longrightarrow> x \<in> A \<Longrightarrow> y \<in> A \<Longrightarrow> x \<sqsubseteq> y"
 begin
 
 text \<open>The strict part is necessarily transitive.\<close>
 
 text \<open>The following sequence of declarations are in order to obtain fact names in a manner
 similar to the Isabelle/HOL facts of orders.\<close>
 
 sublocale strict: transitive A "(\<sqsubset>)"
   using compat_right[OF strict_implies_weak] by unfold_locales
 
 sublocale strict_ordered_set A "(\<sqsubset>)" ..
 
 thm strict.trans asym irrefl
 
 lemma strict_implies_not_weak: "x \<sqsubset> y \<Longrightarrow> x \<in> A \<Longrightarrow> y \<in> A \<Longrightarrow> \<not> y \<sqsubseteq> x"
   using irrefl compat_left by blast
 
 end
 
 context transitive begin
 
 interpretation less_eq_notations.
 
 lemma asym_trans[trans]:
   shows "x \<sqsubset> y \<Longrightarrow> y \<sqsubseteq> z \<Longrightarrow> x \<in> A \<Longrightarrow> y \<in> A \<Longrightarrow> z \<in> A \<Longrightarrow> x \<sqsubset> z"
     and "x \<sqsubseteq> y \<Longrightarrow> y \<sqsubset> z \<Longrightarrow> x \<in> A \<Longrightarrow> y \<in> A \<Longrightarrow> z \<in> A \<Longrightarrow> x \<sqsubset> z"
   by (auto 0 3 dest: trans)
 
 end
 
 locale attractive_ordering = compatible_ordering + attractive
 
 locale pseudo_ordering = compatible_ordering + pseudo_ordered_set
 begin
 
 sublocale attractive_ordering ..
 
 end
 
 locale quasi_ordering = compatible_ordering + quasi_ordered_set
 begin
 
 sublocale attractive_ordering ..
 
 end
 
 locale partial_ordering = compatible_ordering + partially_ordered_set
 begin
 
 sublocale pseudo_ordering + quasi_ordering ..
 
 end
 
 locale well_founded_ordering = quasi_ordering + well_founded
 
 locale total_ordering = compatible_ordering + total_ordered_set
 begin
 
 sublocale partial_ordering ..
 
 end
 
 locale strict_total_ordering = partial_ordering + semiconnex A "(\<sqsubset>)"
 begin
 
 sublocale semiconnex_irreflexive ..
 
 sublocale connex
 proof
   fix x y assume x: "x \<in> A" and y: "y \<in> A"
   then show "x \<sqsubseteq> y \<or> y \<sqsubseteq> x"
     apply (cases rule: cases[OF x y])
     by (auto dest: strict_implies_weak)
 qed
 
 sublocale total_ordering ..
 (*
 sublocale old: ordering "(\<sqsubseteq>)" "(\<sqsubset>)"
 proof-
   have "a \<sqsubseteq> b \<Longrightarrow> a \<noteq> b \<Longrightarrow> a \<sqsubset> b" for a b
     by (cases a b rule: cases, auto dest: strict_implies_weak)
   then show "ordering (\<sqsubseteq>) (\<sqsubset>)"
     by (unfold_locales, auto dest:strict_implies_weak trans)
 qed
 *)
 
 lemma not_weak[simp]:
   assumes "x \<in> A" and "y \<in> A" shows "\<not> x \<sqsubseteq> y \<longleftrightarrow> y \<sqsubset> x"
   using assms by (cases rule:cases, auto simp: strict_implies_not_weak dest: strict_implies_weak)
 
 lemma not_strict[simp]: "x \<in> A \<Longrightarrow> y \<in> A \<Longrightarrow> \<not> x \<sqsubset> y \<longleftrightarrow> y \<sqsubseteq> x"
   using not_weak by blast
 
 end
 
 subsection \<open>Relating to Classes\<close>
 
 text \<open>In Isabelle 2020, we should declare sublocales in class before declaring dual
 sublocales, since otherwise facts would be prefixed by ``dual.dual.''\<close>
 
 context ord begin
 
 abbreviation least where "least X \<equiv> extreme X (\<lambda>x y. y \<le> x)"
 
 abbreviation greatest where "greatest X \<equiv> extreme X (\<le>)"
 
 abbreviation supremum where "supremum X \<equiv> least (Collect (bound X (\<le>)))"
 
 abbreviation infimum where "infimum X \<equiv> greatest (Collect (bound X (\<lambda>x y. y \<le> x)))"
 
 lemma Least_eq_The_least: "Least P = The (least {x. P x})"
   by (auto simp: Least_def extreme_def[unfolded atomize_eq, THEN ext])
 
 lemma Greatest_eq_The_greatest: "Greatest P = The (greatest {x. P x})"
   by (auto simp: Greatest_def extreme_def[unfolded atomize_eq, THEN ext])
 
 end
 
 lemma Ball_UNIV[simp]: "Ball UNIV = All" by auto
 lemma Bex_UNIV[simp]: "Bex UNIV = Ex" by auto
 
 class compat = ord + assumes "compatible_ordering UNIV (\<le>) (<)"
 begin
 
 sublocale order: compatible_ordering UNIV
   rewrites "\<And>x. x \<in> UNIV \<equiv> True"
     and "\<And>X. X \<subseteq> UNIV \<equiv> True"
     and "\<And>r. r \<restriction> UNIV \<equiv> r"
     and "\<And>P. True \<and> P \<equiv> P"
     and "Ball UNIV \<equiv> All"
     and "Bex UNIV \<equiv> Ex"
     and "sympartp (\<le>)\<^sup>- \<equiv> sympartp (\<le>)"
     and "\<And>P1. (True \<Longrightarrow> PROP P1) \<equiv> PROP P1"
     and "\<And>P1. (True \<Longrightarrow> P1) \<equiv> Trueprop P1"
     and "\<And>P1 P2. (True \<Longrightarrow> PROP P1 \<Longrightarrow> PROP P2) \<equiv> (PROP P1 \<Longrightarrow> PROP P2)"
   using compat_axioms unfolding class.compat_def by (auto 0 4 simp:atomize_eq)
 
 end
 
 text \<open>We should have imported locale-based facts in classes, e.g.:\<close>
 thm order.trans order.strict.trans order.refl order.irrefl order.asym order.extreme_bound_singleton
 
 class attractive_order = ord + assumes "attractive_ordering UNIV (\<le>) (<)"
 begin
 
 text \<open>We need to declare subclasses before sublocales in order to preserve facts for superclasses.\<close>
 
 interpretation attractive_ordering UNIV
   using attractive_order_axioms unfolding class.attractive_order_def.
 
 subclass compat ..
 
 sublocale order: attractive_ordering UNIV
   rewrites "\<And>x. x \<in> UNIV \<equiv> True"
     and "\<And>X. X \<subseteq> UNIV \<equiv> True"
     and "\<And>r. r \<restriction> UNIV \<equiv> r"
     and "\<And>P. True \<and> P \<equiv> P"
     and "Ball UNIV \<equiv> All"
     and "Bex UNIV \<equiv> Ex"
     and "sympartp (\<le>)\<^sup>- \<equiv> sympartp (\<le>)"
     and "\<And>P1. (True \<Longrightarrow> PROP P1) \<equiv> PROP P1"
     and "\<And>P1. (True \<Longrightarrow> P1) \<equiv> Trueprop P1"
     and "\<And>P1 P2. (True \<Longrightarrow> PROP P1 \<Longrightarrow> PROP P2) \<equiv> (PROP P1 \<Longrightarrow> PROP P2)"
   apply unfold_locales by (auto simp:atomize_eq)
 
 end
 
 thm order.extreme_bound_quasi_const
 
 class psorder = ord + assumes "pseudo_ordering UNIV (\<le>) (<)"
 begin
 
 interpretation pseudo_ordering UNIV using psorder_axioms unfolding class.psorder_def.
 
 subclass attractive_order ..
 
 sublocale order: pseudo_ordering UNIV
   rewrites "\<And>x. x \<in> UNIV \<equiv> True"
     and "\<And>X. X \<subseteq> UNIV \<equiv> True"
     and "\<And>r. r \<restriction> UNIV \<equiv> r"
     and "\<And>P. True \<and> P \<equiv> P"
     and "Ball UNIV \<equiv> All"
     and "Bex UNIV \<equiv> Ex"
     and "sympartp (\<le>)\<^sup>- \<equiv> sympartp (\<le>)"
     and "\<And>P1. (True \<Longrightarrow> PROP P1) \<equiv> PROP P1"
     and "\<And>P1. (True \<Longrightarrow> P1) \<equiv> Trueprop P1"
     and "\<And>P1 P2. (True \<Longrightarrow> PROP P1 \<Longrightarrow> PROP P2) \<equiv> (PROP P1 \<Longrightarrow> PROP P2)"
   apply unfold_locales by (auto simp:atomize_eq)
 
 end
 
 class qorder = ord + assumes "quasi_ordering UNIV (\<le>) (<)"
 begin
 
 interpretation quasi_ordering UNIV using qorder_axioms unfolding class.qorder_def.
 
 subclass attractive_order ..
 
 sublocale order: quasi_ordering UNIV
   rewrites "\<And>x. x \<in> UNIV \<equiv> True"
     and "\<And>X. X \<subseteq> UNIV \<equiv> True"
     and "\<And>r. r \<restriction> UNIV \<equiv> r"
     and "\<And>P. True \<and> P \<equiv> P"
     and "Ball UNIV \<equiv> All"
     and "Bex UNIV \<equiv> Ex"
     and "sympartp (\<le>)\<^sup>- \<equiv> sympartp (\<le>)"
     and "\<And>P1. (True \<Longrightarrow> PROP P1) \<equiv> PROP P1"
     and "\<And>P1. (True \<Longrightarrow> P1) \<equiv> Trueprop P1"
     and "\<And>P1 P2. (True \<Longrightarrow> PROP P1 \<Longrightarrow> PROP P2) \<equiv> (PROP P1 \<Longrightarrow> PROP P2)"
   apply unfold_locales by (auto simp:atomize_eq)
 
 end
 
 class porder = ord + assumes "partial_ordering UNIV (\<le>) (<)"
 begin
 
 interpretation partial_ordering UNIV
   using porder_axioms unfolding class.porder_def.
 
 subclass psorder ..
 subclass qorder ..
 
 sublocale order: partial_ordering UNIV
   rewrites "\<And>x. x \<in> UNIV \<equiv> True"
     and "\<And>X. X \<subseteq> UNIV \<equiv> True"
     and "\<And>r. r \<restriction> UNIV \<equiv> r"
     and "\<And>P. True \<and> P \<equiv> P"
     and "Ball UNIV \<equiv> All"
     and "Bex UNIV \<equiv> Ex"
     and "sympartp (\<le>)\<^sup>- \<equiv> sympartp (\<le>)"
     and "\<And>P1. (True \<Longrightarrow> PROP P1) \<equiv> PROP P1"
     and "\<And>P1. (True \<Longrightarrow> P1) \<equiv> Trueprop P1"
     and "\<And>P1 P2. (True \<Longrightarrow> PROP P1 \<Longrightarrow> PROP P2) \<equiv> (PROP P1 \<Longrightarrow> PROP P2)"
   apply unfold_locales by (auto simp:atomize_eq)
 
 end
 
 class wf_qorder = ord + assumes "well_founded_ordering UNIV (\<le>) (<)"
 begin
 
 interpretation well_founded_ordering UNIV
   using wf_qorder_axioms unfolding class.wf_qorder_def.
 
 subclass qorder ..
 
 sublocale order: well_founded_ordering UNIV
   rewrites "\<And>x. x \<in> UNIV \<equiv> True"
     and "\<And>X. X \<subseteq> UNIV \<equiv> True"
     and "\<And>r. r \<restriction> UNIV \<equiv> r"
     and "\<And>P. True \<and> P \<equiv> P"
     and "Ball UNIV \<equiv> All"
     and "Bex UNIV \<equiv> Ex"
     and "sympartp (\<le>)\<^sup>- \<equiv> sympartp (\<le>)"
     and "\<And>P1. (True \<Longrightarrow> PROP P1) \<equiv> PROP P1"
     and "\<And>P1. (True \<Longrightarrow> P1) \<equiv> Trueprop P1"
     and "\<And>P1 P2. (True \<Longrightarrow> PROP P1 \<Longrightarrow> PROP P2) \<equiv> (PROP P1 \<Longrightarrow> PROP P2)"
   apply unfold_locales by (auto simp:atomize_eq)
 
 end
 
 class totalorder = ord + assumes "total_ordering UNIV (\<le>) (<)"
 begin
 
 interpretation total_ordering UNIV
   using totalorder_axioms unfolding class.totalorder_def.
 
 subclass porder ..
 
 sublocale order: total_ordering UNIV
   rewrites "\<And>x. x \<in> UNIV \<equiv> True"
     and "\<And>X. X \<subseteq> UNIV \<equiv> True"
     and "\<And>r. r \<restriction> UNIV \<equiv> r"
     and "\<And>P. True \<and> P \<equiv> P"
     and "Ball UNIV \<equiv> All"
     and "Bex UNIV \<equiv> Ex"
     and "sympartp (\<le>)\<^sup>- \<equiv> sympartp (\<le>)"
     and "\<And>P1. (True \<Longrightarrow> PROP P1) \<equiv> PROP P1"
     and "\<And>P1. (True \<Longrightarrow> P1) \<equiv> Trueprop P1"
     and "\<And>P1 P2. (True \<Longrightarrow> PROP P1 \<Longrightarrow> PROP P2) \<equiv> (PROP P1 \<Longrightarrow> PROP P2)"
   apply unfold_locales by (auto simp:atomize_eq)
 
 end
 
 text \<open>Isabelle/HOL's @{class preorder} belongs to @{class qorder}, but not vice versa.\<close>
 
 subclass (in preorder) qorder
   apply unfold_locales
   using order_refl apply assumption
   apply simp
   using le_less_trans apply assumption
   using less_le_trans apply assumption
   using less_imp_le apply assumption
   using  order_trans apply assumption
   done
 
 subclass (in order) porder by (unfold_locales, auto)
 
 subclass (in wellorder) wf_qorder
   apply (unfold_locales)
   using less_induct by auto
 
 text \<open>Isabelle/HOL's @{class linorder} is equivalent to our locale @{locale strict_total_ordering}.\<close>
 
 context linorder begin
 
 interpretation strict_total_ordering UNIV
   apply unfold_locales by auto
 
 subclass totalorder ..
 
 sublocale order: strict_total_ordering UNIV
   rewrites "\<And>x. x \<in> UNIV \<equiv> True"
     and "\<And>X. X \<subseteq> UNIV \<equiv> True"
     and "\<And>r. r \<restriction> UNIV \<equiv> r"
     and "\<And>P. True \<and> P \<equiv> P"
     and "Ball UNIV \<equiv> All"
     and "Bex UNIV \<equiv> Ex"
     and "sympartp (\<le>)\<^sup>- \<equiv> sympartp (\<le>)"
     and "\<And>P1. (True \<Longrightarrow> PROP P1) \<equiv> PROP P1"
     and "\<And>P1. (True \<Longrightarrow> P1) \<equiv> Trueprop P1"
     and "\<And>P1 P2. (True \<Longrightarrow> PROP P1 \<Longrightarrow> PROP P2) \<equiv> (PROP P1 \<Longrightarrow> PROP P2)"
   apply unfold_locales by (auto simp:atomize_eq)
 
 end
 
 text \<open>Tests: facts should be available in the most general classes.\<close>
 
 thm order.strict.trans[where 'a="'a::compat"]
 thm order.extreme_bound_quasi_const[where 'a="'a::attractive_order"]
 thm order.extreme_bound_singleton_eq[where 'a="'a::psorder"]
 thm order.trans[where 'a="'a::qorder"]
 thm order.comparable_cases[where 'a="'a::totalorder"]
 thm order.cases[where 'a="'a::linorder"]
 
 subsection \<open>Declaring Duals\<close>
 
 sublocale reflexive \<subseteq> sym: reflexive A "sympartp (\<sqsubseteq>)"
   rewrites "sympartp (\<sqsubseteq>)\<^sup>- \<equiv> sympartp (\<sqsubseteq>)"
     and "\<And>r. sympartp (sympartp r) \<equiv> sympartp r"
     and "\<And>r. sympartp r \<restriction> A \<equiv> sympartp (r \<restriction> A)"
   by (auto 0 4 simp:atomize_eq)
 
 sublocale quasi_ordered_set \<subseteq> sym: quasi_ordered_set A "sympartp (\<sqsubseteq>)"
   rewrites "sympartp (\<sqsubseteq>)\<^sup>- = sympartp (\<sqsubseteq>)"
     and "sympartp (sympartp (\<sqsubseteq>)) = sympartp (\<sqsubseteq>)"
    apply unfold_locales by (auto 0 4 dest: trans)
   
 text \<open>At this point, we declare dual as sublocales.
 In the following, ``rewrites'' eventually cleans up redundant facts.\<close>
 
 sublocale reflexive \<subseteq> dual: reflexive A "(\<sqsubseteq>)\<^sup>-"
   rewrites "sympartp (\<sqsubseteq>)\<^sup>- \<equiv> sympartp (\<sqsubseteq>)"
     and "\<And>r. sympartp (r \<restriction> A) \<equiv> sympartp r \<restriction> A"
     and "(\<sqsubseteq>)\<^sup>- \<restriction> A \<equiv> ((\<sqsubseteq>) \<restriction> A)\<^sup>-"
   by (auto simp: atomize_eq)
 
 context attractive begin
 
 interpretation less_eq_notations.
 
 sublocale dual: attractive A "(\<sqsupseteq>)"
   rewrites "sympartp (\<sqsupseteq>) = (\<sim>)"
     and "equivpartp (\<sqsupseteq>) \<equiv> (\<simeq>)"
     and "\<And>r. sympartp (r \<restriction> A) \<equiv> sympartp r \<restriction> A"
     and "\<And>r. sympartp (sympartp r) \<equiv> sympartp r"
     and "(\<sqsubseteq>)\<^sup>- \<restriction> A \<equiv> ((\<sqsubseteq>) \<restriction> A)\<^sup>-"
   apply unfold_locales by (auto intro!: ext dest: attract dual.attract simp: atomize_eq)
 
 end
 
 context irreflexive begin
 
 sublocale dual: irreflexive A "(\<sqsubset>)\<^sup>-"
   rewrites "(\<sqsubset>)\<^sup>- \<restriction> A \<equiv> ((\<sqsubset>) \<restriction> A)\<^sup>-"
   apply unfold_locales by (auto dest: irrefl simp: atomize_eq)
 
 end
 
 sublocale transitive \<subseteq> dual: transitive A "(\<sqsubseteq>)\<^sup>-"
   rewrites "(\<sqsubseteq>)\<^sup>- \<restriction> A \<equiv> ((\<sqsubseteq>) \<restriction> A)\<^sup>-"
     and "sympartp (\<sqsubseteq>)\<^sup>- = sympartp (\<sqsubseteq>)"
     and "asympartp (\<sqsubseteq>)\<^sup>- = (asympartp (\<sqsubseteq>))\<^sup>-"
   apply unfold_locales by (auto dest: trans simp: atomize_eq intro!:ext)
 
 sublocale antisymmetric \<subseteq> dual: antisymmetric A "(\<sqsubseteq>)\<^sup>-"
   rewrites "(\<sqsubseteq>)\<^sup>- \<restriction> A \<equiv> ((\<sqsubseteq>) \<restriction> A)\<^sup>-"
     and "sympartp (\<sqsubseteq>)\<^sup>- = sympartp (\<sqsubseteq>)"
   by (auto dest: antisym simp: atomize_eq)
 
 sublocale semiconnex \<subseteq> dual: semiconnex A "(\<sqsubset>)\<^sup>-"
   rewrites "sympartp (\<sqsubset>)\<^sup>- = sympartp (\<sqsubset>)"
   using semiconnex by auto
 
 sublocale connex \<subseteq> dual: connex A "(\<sqsubseteq>)\<^sup>-"
   rewrites "sympartp (\<sqsubseteq>)\<^sup>- = sympartp (\<sqsubseteq>)"
   by (auto intro!: chainI dest:comparable)
 
 sublocale semiconnex_irreflexive \<subseteq> dual: semiconnex_irreflexive A "(\<sqsubset>)\<^sup>-"
   rewrites "sympartp (\<sqsubset>)\<^sup>- = sympartp (\<sqsubset>)"
   by unfold_locales auto
 
 sublocale pseudo_ordered_set \<subseteq> dual: pseudo_ordered_set A "(\<sqsubseteq>)\<^sup>-"
   rewrites "sympartp (\<sqsubseteq>)\<^sup>- = sympartp (\<sqsubseteq>)"
   by unfold_locales (auto 0 4)
 
 sublocale quasi_ordered_set \<subseteq> dual: quasi_ordered_set A "(\<sqsubseteq>)\<^sup>-"
   rewrites "sympartp (\<sqsubseteq>)\<^sup>- = sympartp (\<sqsubseteq>)"
   by unfold_locales auto
 
 sublocale partially_ordered_set \<subseteq> dual: partially_ordered_set A "(\<sqsubseteq>)\<^sup>-"
   rewrites "sympartp (\<sqsubseteq>)\<^sup>- = sympartp (\<sqsubseteq>)"
   by unfold_locales (auto 0 4)
 
 sublocale total_pseudo_ordered_set \<subseteq> dual: total_pseudo_ordered_set A "(\<sqsubseteq>)\<^sup>-"
   rewrites "sympartp (\<sqsubseteq>)\<^sup>- = sympartp (\<sqsubseteq>)"
   by unfold_locales (auto 0 4)
 
 sublocale total_quasi_ordered_set \<subseteq> dual: total_quasi_ordered_set A "(\<sqsubseteq>)\<^sup>-"
   rewrites "sympartp (\<sqsubseteq>)\<^sup>- = sympartp (\<sqsubseteq>)"
   by unfold_locales auto
 
 sublocale compatible_ordering \<subseteq> dual: compatible_ordering A "(\<sqsubseteq>)\<^sup>-" "(\<sqsubset>)\<^sup>-"
   rewrites "sympartp (\<sqsubseteq>)\<^sup>- = sympartp (\<sqsubseteq>)"
   apply unfold_locales
   by (auto dest: compat_left compat_right strict_implies_weak)
 
 sublocale attractive_ordering \<subseteq> dual: attractive_ordering A "(\<sqsubseteq>)\<^sup>-" "(\<sqsubset>)\<^sup>-"
   rewrites "sympartp (\<sqsubseteq>)\<^sup>- = sympartp (\<sqsubseteq>)"
   by unfold_locales auto
 
 sublocale pseudo_ordering \<subseteq> dual: pseudo_ordering A "(\<sqsubseteq>)\<^sup>-" "(\<sqsubset>)\<^sup>-"
   rewrites "sympartp (\<sqsubseteq>)\<^sup>- = sympartp (\<sqsubseteq>)"
   by unfold_locales (auto 0 4)
 
 sublocale quasi_ordering \<subseteq> dual: quasi_ordering A "(\<sqsubseteq>)\<^sup>-" "(\<sqsubset>)\<^sup>-"
   rewrites "sympartp (\<sqsubseteq>)\<^sup>- = sympartp (\<sqsubseteq>)"
   by unfold_locales auto
 
 sublocale partial_ordering \<subseteq> dual: partial_ordering A "(\<sqsubseteq>)\<^sup>-" "(\<sqsubset>)\<^sup>-"
   rewrites "sympartp (\<sqsubseteq>)\<^sup>- = sympartp (\<sqsubseteq>)"
   by unfold_locales (auto 0 4)
 
 sublocale total_ordering \<subseteq> dual: total_ordering A "(\<sqsubseteq>)\<^sup>-" "(\<sqsubset>)\<^sup>-"
   rewrites "sympartp (\<sqsubseteq>)\<^sup>- = sympartp (\<sqsubseteq>)"
   by unfold_locales (auto 0 4)
 
 lemma(in antisymmetric) monotone_extreme_imp_extreme_bound_iff:
   fixes ir (infix "\<preceq>" 50)
   assumes "f ` C \<subseteq> A" and "monotone_on C (\<preceq>) (\<sqsubseteq>) f" and i: "extreme C (\<preceq>) i"
   shows "extreme_bound A (\<sqsubseteq>) (f ` C) x \<longleftrightarrow> f i = x"
   using dual.extreme_unique monotone_extreme_extreme_boundI[OF assms] by auto
 
 
 subsection \<open>Instantiations\<close>
 
 text \<open>Finally, we instantiate our classes for sanity check.\<close>
 
 instance nat :: linorder ..
 
 text \<open>Pointwise ordering of functions are compatible only if the weak part is transitive.\<close>
 
 instance "fun" :: (type,qorder) compat
 proof (intro_classes, unfold_locales)
   note [simp] = le_fun_def less_fun_def
   fix f g h :: "'a \<Rightarrow> 'b"
   { assume fg: "f \<le> g" and gh: "g < h"
     show "f < h"
     proof (unfold less_fun_def, intro conjI le_funI notI)
       from fg have "f x \<le> g x" for x by auto
       also from gh have "g x \<le> h x" for x by auto
       finally (order.trans) show "f x \<le> h x" for x.
       assume hf: "h \<le> f"
       then have "h x \<le> f x" for x by auto
       also from fg have "f x \<le> g x" for x by auto
       finally have "h \<le> g" by auto
       with gh show False by auto
     qed
   }
   { assume fg: "f < g" and gh: "g \<le> h"
     show "f < h"
     proof (unfold less_fun_def, intro conjI le_funI notI)
       from fg have "f x \<le> g x" for x by auto
       also from gh have "g x \<le> h x" for x by auto
       finally show "f x \<le> h x" for x.
       from gh have "g x \<le> h x" for x by auto
       also assume hf: "h \<le> f"
       then have "h x \<le> f x" for x by auto
       finally have "g \<le> f" by auto
       with fg show False by auto
     qed
   }
   show "f < g \<Longrightarrow> f \<le> g" by auto
   show "\<not>f < f" by auto
   show "f \<le> f" by auto
 qed
 
 instance "fun" :: (type,qorder) qorder
   apply intro_classes
   apply unfold_locales
   by (auto simp: le_fun_def dest: order.trans)
 
 instance "fun" :: (type,porder) porder
   apply intro_classes
   apply unfold_locales
 proof (intro ext)
   fix f g :: "'a \<Rightarrow> 'b" and x :: 'a
   assume fg: "f \<le> g" and gf: "g \<le> f"
   then have "f x \<le> g x" and "g x \<le> f x" by (auto elim: le_funE)
   from order.antisym[OF this] show "f x = g x" by auto
 qed
 
 end
diff --git a/thys/Complete_Non_Orders/Fixed_Points.thy b/thys/Complete_Non_Orders/Fixed_Points.thy
--- a/thys/Complete_Non_Orders/Fixed_Points.thy
+++ b/thys/Complete_Non_Orders/Fixed_Points.thy
@@ -1,1236 +1,1236 @@
 (*
 Author:  Jérémy Dubut (2019-2021)
 Author:  Akihisa Yamada (2019-2021)
 License: LGPL (see file COPYING.LESSER)
 *)
 
 theory Fixed_Points
   imports Complete_Relations
 begin
 
 section \<open>Existence of Fixed Points in Complete Related Sets\<close>
 text \<open>\label{sec:qfp-exists}\<close>
 
 text \<open>The following proof is simplified and generalized from
   Stouti--Maaden \cite{SM13}. We construct some set whose extreme bounds 
   -- if they exist, typically when the underlying related set is complete -- 
   are fixed points of a monotone or inflationary function on any 
   related set. When the related set is attractive, those are actually the least fixed points.
   This generalizes \cite{SM13}, relaxing reflexivity and antisymmetry.\<close>
 
 locale fixed_point_proof = related_set +
   fixes f
   assumes f: "f ` A \<subseteq> A"
 begin
 
 sublocale less_eq_notations.
 
 definition AA where "AA \<equiv>
   {X. X \<subseteq> A \<and> f ` X \<subseteq> X \<and> (\<forall>Y s. Y \<subseteq> X \<longrightarrow> extreme_bound A (\<sqsubseteq>) Y s \<longrightarrow> s \<in> X)}"
 
 lemma AA_I:
   "X \<subseteq> A \<Longrightarrow> f ` X \<subseteq> X \<Longrightarrow> (\<And>Y s. Y \<subseteq> X \<Longrightarrow> extreme_bound A (\<sqsubseteq>) Y s \<Longrightarrow> s \<in> X) \<Longrightarrow> X \<in> AA"
   by (unfold AA_def, safe)
 
 lemma AA_E:
   "X \<in> AA \<Longrightarrow>
    (X \<subseteq> A \<Longrightarrow> f ` X \<subseteq> X \<Longrightarrow> (\<And>Y s. Y \<subseteq> X \<Longrightarrow> extreme_bound A (\<sqsubseteq>) Y s \<Longrightarrow> s \<in> X) \<Longrightarrow> thesis) \<Longrightarrow> thesis"
   by (auto simp: AA_def)
 
 definition C where "C \<equiv> \<Inter> AA"
 
 lemma A_AA: "A \<in> AA" by (auto intro!:AA_I f)
 
 lemma C_AA: "C \<in> AA"
 proof (intro AA_I)
   show "C \<subseteq> A" using C_def A_AA f by auto
   show "f ` C \<subseteq> C" unfolding C_def AA_def by auto
   fix B b assume B: "B \<subseteq> C" "extreme_bound A (\<sqsubseteq>) B b"
   { fix X assume X: "X \<in> AA"
     with B have "B \<subseteq> X" by (auto simp: C_def)
     with X B have "b\<in>X" by (auto elim!: AA_E)
   }
   then show "b \<in> C" by (auto simp: C_def AA_def)
 qed
 
 lemma CA: "C \<subseteq> A" using A_AA by (auto simp: C_def)
 
 lemma fC: "f ` C \<subseteq> C" using C_AA by (auto elim!: AA_E)
 
 context
   fixes c assumes Cc: "extreme_bound A (\<sqsubseteq>) C c"
 begin
 
 private lemma cA: "c \<in> A" using Cc by auto
 private lemma cC: "c \<in> C" using Cc C_AA by (blast elim!:AA_E) 
 private lemma fcC: "f c \<in> C" using cC AA_def C_AA by auto
 private lemma fcA: "f c \<in> A" using fcC CA by auto
 
 lemma qfp_as_extreme_bound:
   assumes infl_mono: "\<forall>x \<in> A. x \<sqsubseteq> f x \<or> (\<forall>y \<in> A. y \<sqsubseteq> x \<longrightarrow> f y \<sqsubseteq> f x)"
   shows "f c \<sim> c"
 proof (intro conjI bexI sympartpI)
   show "f c \<sqsubseteq> c" using fcC Cc by auto
   from infl_mono[rule_format, OF cA]
   show "c \<sqsubseteq> f c"
   proof (safe)
     text \<open>Monotone case:\<close>
     assume mono: "\<forall>b\<in>A. b \<sqsubseteq> c \<longrightarrow> f b \<sqsubseteq> f c"
     define D where "D \<equiv> {x \<in> C. x \<sqsubseteq> f c}"
     have "D \<in> AA"
     proof (intro AA_I)
       show "D \<subseteq> A" unfolding D_def C_def using A_AA f by auto
       have fxC: "x \<in> C \<Longrightarrow> x \<sqsubseteq> f c \<Longrightarrow> f x \<in> C" for x using C_AA by (auto simp: AA_def)
       show "f ` D \<subseteq> D"
       proof (unfold D_def, safe intro!: fxC)
         fix x assume xC: "x \<in> C"
         have "x \<sqsubseteq> c" "x \<in> A" using Cc xC CA by auto
         then show "f x \<sqsubseteq> f c" using mono by (auto dest:monotoneD)
       qed
       have DC: "D \<subseteq> C" unfolding D_def by auto
       fix B b assume BD: "B \<subseteq> D" and Bb: "extreme_bound A (\<sqsubseteq>) B b"
       have "B \<subseteq> C" using DC BD by auto
       then have bC: "b \<in> C" using C_AA Bb BD by (auto elim!: AA_E)
       have bfc: "\<forall>a\<in>B. a \<sqsubseteq> f c" using BD unfolding D_def by auto
       with f cA Bb
       have "b \<sqsubseteq> f c" by (auto simp: extreme_def image_subset_iff)
       with bC show "b \<in> D" unfolding D_def by auto
     qed
     then have "C \<subseteq> D" unfolding C_def by auto
     then show "c \<sqsubseteq> f c" using cC unfolding D_def by auto
   qed
 qed
 
 lemma extreme_qfp:
   assumes attract: "\<forall>q \<in> A. \<forall>x \<in> A. f q \<sim> q \<longrightarrow> x \<sqsubseteq> f q \<longrightarrow> x \<sqsubseteq> q"
     and mono: "monotone_on A (\<sqsubseteq>) (\<sqsubseteq>) f"
   shows "extreme {q \<in> A. f q \<sim> q \<or> f q = q} (\<sqsupseteq>) c"
 proof-
   have fcc: "f c \<sim> c"
     apply (rule qfp_as_extreme_bound)
     using mono by (auto elim!: monotone_onE)
   define L where [simp]: "L \<equiv> {a \<in> A. \<forall>s \<in> A. (f s \<sim> s \<or> f s = s) \<longrightarrow> a \<sqsubseteq> s}"
   have "L \<in> AA"
   proof (unfold AA_def, intro CollectI conjI allI impI)
     show XA: "L \<subseteq> A" by auto  
     show "f ` L \<subseteq> L"
     proof safe
       fix x assume xL: "x \<in> L"
       show "f x \<in> L"
       proof (unfold L_def, safe)
         have xA: "x \<in> A" using xL by auto 
         then show fxA: "f x \<in> A" using f by auto
         { fix s assume sA: "s \<in> A" and sf: "f s \<sim> s \<or> f s = s"
           then have "x \<sqsubseteq> s" using xL sA sf by auto
           then have "f x \<sqsubseteq> f s" using mono fxA sA xA by (auto elim!:monotone_onE)}
         note fxfs = this
         { fix s assume sA: "s \<in> A" and sf: "f s \<sim> s"
           then show "f x \<sqsubseteq> s" using fxfs attract mono sf fxA sA xA by (auto elim!:monotone_onE)
         }
         { fix s assume sA: "s \<in> A" and sf: "f s = s"
           with fxfs[OF sA] show "f x \<sqsubseteq> s" by simp}
       qed 
     qed
     fix B b assume BL: "B \<subseteq> L" and b: "extreme_bound A (\<sqsubseteq>) B b"
     then have BA: "B \<subseteq> A" by auto
     with BL b have bA: "b \<in> A" by auto
     show "b \<in> L"
     proof (unfold L_def, safe intro!: bA)
       { fix s assume sA: "s \<in> A" and sf: "f s \<sim> s \<or> f s = s"
         have "bound B (\<sqsubseteq>) s" using sA BL b sf by auto
       }
       note Bs = this
       { fix s assume sA: "s \<in> A" and sf: "f s \<sim> s"
         with b sA Bs show "b \<sqsubseteq> s" by auto
       }
       { fix s assume sA: "s \<in> A" and sf: "f s = s"
         with b sA Bs show "b \<sqsubseteq> s" by auto
       }
     qed
   qed
   then have "C \<subseteq> L" by (simp add: C_def Inf_lower)
   with cC have "c \<in> L" by auto
   with L_def fcc
   show ?thesis by auto
 qed
 
 end
 
 lemma ex_qfp:
   assumes comp: "CC-complete A (\<sqsubseteq>)" and C: "C \<in> CC"
     and infl_mono: "\<forall>a \<in> A. a \<sqsubseteq> f a \<or> (\<forall>b \<in> A. b \<sqsubseteq> a \<longrightarrow> f b \<sqsubseteq> f a)"
   shows "\<exists>s \<in> A. f s \<sim> s"
   using qfp_as_extreme_bound[OF _  infl_mono] completeD[OF comp CA C] by auto
 
 lemma ex_extreme_qfp_fp:
   assumes comp: "CC-complete A (\<sqsubseteq>)" and C: "C \<in> CC"
     and attract: "\<forall>q \<in> A. \<forall>x \<in> A. f q \<sim> q \<longrightarrow> x \<sqsubseteq> f q \<longrightarrow> x \<sqsubseteq> q"
     and mono: "monotone_on A (\<sqsubseteq>) (\<sqsubseteq>) f"
   shows "\<exists>c. extreme {q \<in> A. f q \<sim> q \<or> f q = q} (\<sqsupseteq>) c"
   using extreme_qfp[OF _ attract mono] completeD[OF comp CA C] by auto
 
 lemma ex_extreme_qfp:
   assumes comp: "CC-complete A (\<sqsubseteq>)" and C: "C \<in> CC"
     and attract: "\<forall>q \<in> A. \<forall>x \<in> A. f q \<sim> q \<longrightarrow> x \<sqsubseteq> f q \<longrightarrow> x \<sqsubseteq> q"
     and mono: "monotone_on A (\<sqsubseteq>) (\<sqsubseteq>) f"
   shows "\<exists>c. extreme {q \<in> A. f q \<sim> q} (\<sqsupseteq>) c"
 proof-
   from completeD[OF comp CA C]
   obtain c where Cc: "extreme_bound A (\<sqsubseteq>) C c" by auto
   from extreme_qfp[OF Cc attract mono]
   have Qc: "bound {q \<in> A. f q \<sim> q} (\<sqsupseteq>) c" by auto
   have fcc: "f c \<sim> c"
     apply (rule qfp_as_extreme_bound[OF Cc])
     using mono by (auto simp: monotone_onD)
   from Cc CA have cA: "c \<in> A" by auto
   from Qc fcc cA show ?thesis by (auto intro!: exI[of _ c])
 qed
 
 end
 
 context
   fixes less_eq :: "'a \<Rightarrow> 'a \<Rightarrow> bool" (infix "\<sqsubseteq>" 50) and A :: "'a set" and f
   assumes f: "f ` A \<subseteq> A"
 begin
 
 interpretation less_eq_notations.
 interpretation fixed_point_proof A "(\<sqsubseteq>)" f using f by unfold_locales
 
 theorem complete_infl_mono_imp_ex_qfp:
   assumes comp: "UNIV-complete A (\<sqsubseteq>)" and infl_mono: "\<forall>a\<in>A. a \<sqsubseteq> f a \<or> (\<forall>b\<in>A. b \<sqsubseteq> a \<longrightarrow> f b \<sqsubseteq> f a)"
   shows "\<exists>s\<in>A. f s \<sim> s"
   apply (rule ex_qfp[OF comp _ infl_mono]) by auto
 
 end
 
 corollary (in antisymmetric) complete_infl_mono_imp_ex_fp:
   assumes comp: "UNIV-complete A (\<sqsubseteq>)" and f: "f ` A \<subseteq> A"
     and infl_mono: "\<forall>a\<in>A. a \<sqsubseteq> f a \<or> (\<forall>b\<in>A. b \<sqsubseteq> a \<longrightarrow> f b \<sqsubseteq> f a)"
   shows "\<exists>s \<in> A. f s = s"
 proof-
   interpret less_eq_notations.
   from complete_infl_mono_imp_ex_qfp[OF f comp infl_mono]
   obtain s where sA: "s \<in> A" and fss: "f s \<sim> s" by auto
   from f sA have fsA: "f s \<in> A" by auto
   have "f s = s" using antisym fsA sA fss by auto
   with sA show ?thesis by auto
 qed
 
 context semiattractive begin
 
 interpretation less_eq_notations.
 
 theorem complete_mono_imp_ex_extreme_qfp:
   assumes comp: "UNIV-complete A (\<sqsubseteq>)" and f: "f ` A \<subseteq> A"
     and mono: "monotone_on A (\<sqsubseteq>) (\<sqsubseteq>) f"
   shows "\<exists>s. extreme {p \<in> A. f p \<sim> p} (\<sqsubseteq>) s"
 proof-
   interpret dual: fixed_point_proof A "(\<sqsupseteq>)" rewrites "dual.sym = (\<sim>)"
     using f by unfold_locales (auto intro!:ext)
   show ?thesis
     apply (rule dual.ex_extreme_qfp[OF complete_dual[OF comp] _ _ monotone_on_dual[OF mono]])
     apply simp
     using f sym_order_trans by blast
 qed
 
 end
 
 corollary (in antisymmetric) complete_mono_imp_ex_extreme_fp:
   assumes comp: "UNIV-complete A (\<sqsubseteq>)" and f: "f ` A \<subseteq> A"
     and mono: "monotone_on A (\<sqsubseteq>) (\<sqsubseteq>) f"
   shows "\<exists>s. extreme {s \<in> A. f s = s} (\<sqsubseteq>)\<^sup>- s"
 proof-
   interpret less_eq_notations.
   interpret fixed_point_proof A "(\<sqsubseteq>)" f using f by unfold_locales
   have "\<exists>c. extreme {q \<in> A. f q \<sim> q \<or> f q = q} (\<sqsupseteq>) c"
     apply (rule ex_extreme_qfp_fp[OF comp _ _ mono])
     using antisym f by (auto dest: order_sym_trans)
   then obtain c where c: "extreme {q \<in> A. f q \<sim> q \<or> f q = q} (\<sqsupseteq>) c" by auto
   then have "f c = c" using antisym f by blast
   with c have "extreme {q \<in> A. f q = q} (\<sqsupseteq>) c" by auto
   then show ?thesis by auto
 qed
 
 section \<open>Fixed Points in Well-Complete Antisymmetric Sets\<close>
 text \<open>\label{sec:well-complete}\<close>
 
 text \<open>In this section, we prove that an
 inflationary or monotone map over a well-complete antisymmetric set
 has a fixed point.
 
 In order to formalize such a theorem in Isabelle,
 we followed Grall's~\cite{grall10} elementary proof for Bourbaki--Witt and Markowsky's theorems.
 His idea is to consider well-founded derivation trees over $A$,
 where from a set $C \subseteq A$ of premises
-one can derive $f\:(\SUP C)$ if $C$ is a chain.
+one can derive $f\:(\bigsqcup C)$ if $C$ is a chain.
 The main observation is as follows:
 Let $D$ be the set of all the derivable elements; that is,
 for each $d \in D$ there exists a well-founded derivation
 whose root is $d$.
 It is shown that $D$ is a chain,
-and hence one can build a derivation yielding $f\:(\SUP D)$,
-and $f\:(\SUP D)$ is shown to be a fixed point.\<close>
+and hence one can build a derivation yielding $f\:(\bigsqcup D)$,
+and $f\:(\bigsqcup D)$ is shown to be a fixed point.\<close>
 
 lemma bound_monotone_on:
   assumes mono: "monotone_on A r s f" and XA: "X \<subseteq> A" and aA: "a \<in> A" and rXa: "bound X r a"
   shows "bound (f`X) s (f a)"
 proof (safe)
   fix x assume xX: "x \<in> X" 
   from rXa xX have "r x a" by auto
   with xX XA mono aA show "s (f x) (f a)" by (auto elim!:monotone_onE)
 qed
 
 context fixed_point_proof begin
 
 text \<open>To avoid the usage of the axiom of choice, we carefully define derivations so that any derivable element
 determines its lower set. This led to the following definition:\<close>
 
 definition "derivation X \<equiv> X \<subseteq> A \<and> well_ordered_set X (\<sqsubseteq>) \<and>
   (\<forall>x \<in> X. let Y = {y \<in> X. y \<sqsubset> x} in
     (\<exists>y. extreme Y (\<sqsubseteq>) y \<and> x = f y) \<or>
     f ` Y \<subseteq> Y \<and> extreme_bound A (\<sqsubseteq>) Y x)"
 
 lemma assumes "derivation P"
   shows derivation_A: "P \<subseteq> A" and derivation_well_ordered: "well_ordered_set P (\<sqsubseteq>)"
   using assms by (auto simp: derivation_def)
 
 lemma derivation_cases[consumes 2, case_names suc lim]:
   assumes "derivation X" and "x \<in> X"
     and "\<And>Y y. Y = {y \<in> X. y \<sqsubset> x} \<Longrightarrow> extreme Y (\<sqsubseteq>) y \<Longrightarrow> x = f y \<Longrightarrow> thesis"
     and "\<And>Y. Y = {y \<in> X. y \<sqsubset> x} \<Longrightarrow> f ` Y \<subseteq> Y \<Longrightarrow> extreme_bound A (\<sqsubseteq>) Y x \<Longrightarrow> thesis"
   shows thesis
   using assms unfolding derivation_def Let_def by auto
 
 definition "derivable x \<equiv> \<exists>X. derivation X \<and> x \<in> X"
 
 lemma derivableI[intro?]: "derivation X \<Longrightarrow> x \<in> X \<Longrightarrow> derivable x" by (auto simp: derivable_def)
 lemma derivableE: "derivable x \<Longrightarrow> (\<And>P. derivation P \<Longrightarrow> x \<in> P \<Longrightarrow> thesis) \<Longrightarrow> thesis"
   by (auto simp: derivable_def)
 
 lemma derivable_A: "derivable x \<Longrightarrow> x \<in> A" by (auto elim: derivableE dest:derivation_A)
 
 lemma UN_derivations_eq_derivable: "(\<Union>{P. derivation P}) = {x. derivable x}"
   by (auto simp: derivable_def)
 
 context
   assumes ord: "antisymmetric A (\<sqsubseteq>)"
 begin
 
 interpretation antisymmetric using ord.
 
 lemma derivation_lim:
   assumes P: "derivation P" and fP: "f ` P \<subseteq> P" and Pp: "extreme_bound A (\<sqsubseteq>) P p"
   shows "derivation (P \<union> {p})"
 proof (cases "p \<in> P")
   case True
   with P show ?thesis by (auto simp: insert_absorb)
 next
   case pP: False
   interpret P: well_ordered_set P "(\<sqsubseteq>)" using derivation_well_ordered[OF P].
   have PA: "P \<subseteq> A" using derivation_A[OF P].
   from Pp have pA: "p \<in> A" by auto
   have bp: "bound P (\<sqsubseteq>) p" using Pp by auto
   then have pp: "p \<sqsubseteq> p" using Pp by auto
   have 1: "y \<in> P \<longrightarrow> {x. (x = p \<or> x \<in> P) \<and> x \<sqsubset> y} = {x \<in> P. x \<sqsubset> y}" for y
     using Pp by (auto dest:extreme_bound_bound)
   { fix x assume xP: "x \<in> P" and px: "p \<sqsubseteq> x"
     from xP Pp have "x \<sqsubseteq> p" by auto
     with px have "p = x" using xP PA pA by (auto intro!: antisym)
     with xP pP
     have "False" by auto
   }
   note 2 = this
   then have 3: "{x. (x = p \<or> x \<in> P) \<and> x \<sqsubset> p} = P" using Pp by (auto intro!: asympartpI)
   have wr: "well_ordered_set (P \<union> {p}) (\<sqsubseteq>)"
     apply (rule well_order_extend[OF P.well_ordered_set_axioms])
     using pp bp pP 2 by auto
   from P fP Pp
   show "derivation (P \<union> {p})" by (auto simp: derivation_def pA wr[simplified] 1 3)
 qed
 
 context
   assumes derivation_infl: "\<forall>X x y. derivation X \<longrightarrow> x \<in> X \<longrightarrow> y \<in> X \<longrightarrow> x \<sqsubseteq> y \<longrightarrow> x \<sqsubseteq> f y"
     and derivation_f_refl: "\<forall>X x. derivation X \<longrightarrow> x \<in> X \<longrightarrow> f x \<sqsubseteq> f x"
 begin
 
 lemma derivation_suc:
   assumes P: "derivation P" and Pp: "extreme P (\<sqsubseteq>) p" shows "derivation (P \<union> {f p})"
 proof (cases "f p \<in> P")
   case True
   with P show ?thesis by (auto simp: insert_absorb)
 next
   case fpP: False
   interpret P: well_ordered_set P "(\<sqsubseteq>)" using derivation_well_ordered[OF P].
   have PA: "P \<subseteq> A" using derivation_A[OF P].
   with Pp have pP: "p \<in> P" and pA: "p \<in> A" by auto
   with f have fpA: "f p \<in> A" by auto 
   from pP have pp: "p \<sqsubseteq> p" by auto
   from derivation_infl[rule_format, OF P pP pP pp] have "p \<sqsubseteq> f p".
   { fix x assume xP: "x \<in> P"
     then have xA: "x \<in> A" using PA by auto
     have xp: "x \<sqsubseteq> p" using xP Pp by auto
     from derivation_infl[rule_format, OF P xP pP this]
     have "x \<sqsubseteq> f p".
   }
   note Pfp = this
   then have bfp: "bound P (\<sqsubseteq>) (f p)" by auto
   { fix y assume yP: "y \<in> P"
     note yfp = Pfp[OF yP]
     { assume fpy: "f p \<sqsubseteq> y"
       with yfp have "f p = y" using yP PA pA fpA antisym by auto
       with yP fpP have "False" by auto
     }
     with Pfp yP have "y \<sqsubset> f p" by auto
   }
   note Pfp = this
   have 1: "\<And>y. y \<in> P \<longrightarrow> {x. (x = f p \<or> x \<in> P) \<and> x \<sqsubset> y} = {x \<in> P. x \<sqsubset> y}"
    and 2: "{x. (x = f p \<or> x \<in> P) \<and> x \<sqsubset> f p} = P" using Pfp by auto
   have wr: "well_ordered_set (P \<union> {f p}) (\<sqsubseteq>)"
     apply (rule well_order_extend[OF P.well_ordered_set_axioms singleton_well_ordered])
     using Pfp derivation_f_refl[rule_format, OF P pP] by auto
   from P Pp
   show "derivation (P \<union> {f p})" by (auto simp: derivation_def wr[simplified] 1 2 fpA)
 qed
 
 lemma derivable_closed:
   assumes x: "derivable x" shows "derivable (f x)"
 proof (insert x, elim derivableE)
   fix P
   assume P: "derivation P" and xP: "x \<in> P"
   note PA = derivation_A[OF P]
   then have xA: "x \<in> A" using xP by auto
   interpret P: well_ordered_set P "(\<sqsubseteq>)" using derivation_well_ordered[OF P].
   interpret P.asympartp: transitive P "(\<sqsubset>)" using P.asympartp_transitive.
   define Px where "Px \<equiv> {y. y \<in> P \<and> y \<sqsubset> x} \<union> {x}"
   then have PxP: "Px \<subseteq> P" using xP by auto
   have "x \<sqsubseteq> x" using xP by auto
   then have Pxx: "extreme Px (\<sqsubseteq>) x" using xP PA by (auto simp: Px_def)
   have wr: "well_ordered_set Px (\<sqsubseteq>)" using P.well_ordered_subset[OF PxP].
   { fix z y assume zPx: "z \<in> Px" and yP: "y \<in> P" and yz: "y \<sqsubset> z"
     then have zP: "z \<in> P" using PxP by auto
     have "y \<sqsubset> x"
     proof (cases "z = x")
       case True
       then show ?thesis using yz by auto
     next
       case False
       then have zx: "z \<sqsubset> x" using zPx by (auto simp: Px_def)
       from P.asympartp.trans[OF yz zx yP zP xP] show ?thesis.
     qed
   }
   then have 1: "\<And>z. z \<in> Px \<longrightarrow> {y \<in> Px. y \<sqsubset> z} = {y \<in> P. y \<sqsubset> z}" using Px_def by blast
   have Px: "derivation Px" using PxP PA P by (auto simp: wr derivation_def 1)
   from derivation_suc[OF Px Pxx]
   show ?thesis by (auto intro!: derivableI)
 qed
 
 text \<open>The following lemma is derived from Grall’s proof. We simplify the claim so that we
 consider two elements from one derivation, instead of two derivations.\<close>
 
 lemma derivation_useful:
   assumes X: "derivation X" and xX: "x \<in> X" and yX: "y \<in> X" and xy: "x \<sqsubset> y"
   shows "f x \<sqsubseteq> y"
 proof-
   interpret X: well_ordered_set X "(\<sqsubseteq>)" using derivation_well_ordered[OF X].
   note XA = derivation_A[OF X]
   { fix x y assume xX: "x \<in> X" and yX: "y \<in> X"
     from xX yX have "(x \<sqsubset> y \<longrightarrow> f x \<sqsubseteq> y \<and> f x \<in> X) \<and> (y \<sqsubset> x \<longrightarrow> f y \<sqsubseteq> x \<and> f y \<in> X)"
     proof (induct x arbitrary: y)
       case (less x)
       note xX = \<open>x \<in> X\<close> and IHx = this(2)
       with XA have xA: "x \<in> A" by auto
       from \<open>y \<in> X\<close> show ?case
       proof (induct y)
         case (less y)
         note yX = \<open>y \<in> X\<close> and IHy = this(2)
         with XA have yA: "y \<in> A" by auto
         show ?case
         proof (rule conjI; intro impI)
           assume xy: "x \<sqsubset> y"
           from X yX
           show "f x \<sqsubseteq> y \<and> f x \<in> X"
           proof (cases rule:derivation_cases)
             case (suc Z z)
             with XA have zX: "z \<in> X" and zA: "z \<in> A" and zy: "z \<sqsubset> y" and yfz: "y = f z" by auto
             from xX zX show ?thesis
             proof (cases rule: X.comparable_three_cases)
               case xz: less
               with IHy[OF zX zy] have fxz: "f x \<sqsubseteq> z" and fxX: "f x \<in> X" by auto
               from derivation_infl[rule_format, OF X fxX zX fxz] have "f x \<sqsubseteq> y" by (auto simp: yfz)
               with fxX show ?thesis by auto
             next
               case eq
               with xX zX have "x = z" by auto
               with yX yfz show ?thesis by auto
             next
               case zx: greater
               with IHy[OF zX zy] yfz xy have False by auto
               then show ?thesis by auto
             qed
           next
             case (lim Z)
             note Z = \<open>Z = {z \<in> X. z \<sqsubset> y}\<close> and fZ = \<open>f ` Z \<subseteq> Z\<close>
             from xX xy have "x \<in> Z" by (auto simp: Z)
             with fZ have "f x \<in> Z" by auto
             then have "f x \<sqsubset> y" and "f x \<in> X" by (auto simp: Z)
             then show ?thesis by auto
           qed
         next
           assume yx: "y \<sqsubset> x"
           from X xX
           show "f y \<sqsubseteq> x \<and> f y \<in> X"
           proof (cases rule:derivation_cases)
             case (suc Z z)
             with XA have zX: "z \<in> X" and zA: "z \<in> A" and zx: "z \<sqsubset> x" and xfz: "x = f z" by auto
             from yX zX show ?thesis
             proof (cases rule: X.comparable_three_cases)
               case yz: less
               with IHx[OF zX zx yX] have fyz: "f y \<sqsubseteq> z" and fyX: "f y \<in> X" by auto
               from derivation_infl[rule_format, OF X fyX zX fyz] have "f y \<sqsubseteq> x" by (auto simp: xfz)
               with fyX show ?thesis by auto
             next
               case eq
               with yX zX have "y = z" by auto
               with xX xfz show ?thesis by auto
             next
               case greater
               with IHx[OF zX zx yX] xfz yx have False by auto
               then show ?thesis by auto
             qed
           next
             case (lim Z)
             note Z = \<open>Z = {z \<in> X. z \<sqsubset> x}\<close> and fZ = \<open>f ` Z \<subseteq> Z\<close>
             from yX yx have "y \<in> Z" by (auto simp: Z)
             with fZ have "f y \<in> Z" by auto
             then have "f y \<sqsubset> x" and "f y \<in> X" by (auto simp: Z)
             then show ?thesis by auto
           qed
         qed
       qed
     qed
   }
   with assms show "f x \<sqsubseteq> y" by auto
 qed
 
 text \<open>Next one is the main lemma of this section, stating that elements from two possibly different 
 derivations are comparable, and moreover the lower one is in the derivation of the upper one. 
 The latter claim, not found in Grall’s proof, is crucial in proving that the union of all 
 derivations is well-related.\<close>
 
 lemma derivations_cross_compare:
   assumes X: "derivation X" and Y: "derivation Y" and xX: "x \<in> X" and yY: "y \<in> Y"
   shows "(x \<sqsubset> y \<and> x \<in> Y) \<or> x = y \<or> (y \<sqsubset> x \<and> y \<in> X)" 
 proof-
   { fix X Y x y
     assume X: "derivation X" and Y: "derivation Y" and xX: "x \<in> X" and yY: "y \<in> Y"
     interpret X: well_ordered_set X "(\<sqsubseteq>)" using derivation_well_ordered[OF X].
     interpret X.asympartp: transitive X "(\<sqsubset>)" using X.asympartp_transitive.
     interpret Y: well_ordered_set Y "(\<sqsubseteq>)" using derivation_well_ordered[OF Y].
     have XA: "X \<subseteq> A" using derivation_A[OF X].
     then have xA: "x \<in> A" using xX by auto
     with f have fxA: "f x \<in> A" by auto
     have YA: "Y \<subseteq> A" using derivation_A[OF Y].
     then have yA: "y \<in> A" using yY by auto
     with f have fyA: "f y \<in> A" by auto
     { fix Z
       assume Z: "Z = {z \<in> X. z \<sqsubset> x}"
         and fZ: "f ` Z \<subseteq> Z"
         and Zx: "extreme_bound A (\<sqsubseteq>) Z x"
         and IHx: "\<forall>z \<in> X. z \<sqsubset> x \<longrightarrow> (z \<sqsubset> y \<and> z \<in> Y) \<or> z = y \<or> (y \<sqsubset> z \<and> y \<in> X)"
       have "(y \<sqsubset> x \<and> y \<in> X) \<or> x \<sqsubseteq> y"
       proof (cases "\<exists>z \<in> Z. y \<sqsubset> z")
         case True
         then obtain z where zZ: "z \<in> Z" and yz: "y \<sqsubset> z" by auto
         from zZ Z have zX: "z \<in> X" and zx: "z \<sqsubset> x" by auto
         from IHx[rule_format, OF zX zx] yz have yX: "y \<in> X" by auto
         from X.asympartp.trans[OF yz zx yX zX xX] have "y \<sqsubset> x".
         with yX show ?thesis by auto
       next
         case False
         have "bound Z (\<sqsubseteq>) y"
         proof
           fix z assume "z \<in> Z"
           then have zX: "z \<in> X" and zx: "z \<sqsubset> x" and nyz: "\<not> y \<sqsubset> z" using Z False by auto
           with IHx[rule_format, OF zX zx] X show "z \<sqsubseteq> y" by auto
         qed
         with yA Zx have xy: "x \<sqsubseteq> y" by auto
         then show ?thesis by auto
       qed
     }
     note lim_any = this
     { fix z Z
       assume Z: "Z = {z \<in> X. z \<sqsubset> x}"
         and Zz: "extreme Z (\<sqsubseteq>) z"
         and xfz: "x = f z"
         and IHx: "(z \<sqsubset> y \<and> z \<in> Y) \<or> z = y \<or> (y \<sqsubset> z \<and> y \<in> X)"
       have zX: "z \<in> X" and zx: "z \<sqsubset> x" using Zz Z by (auto simp: extreme_def)
       then have zA: "z \<in> A" using XA by auto
       from IHx have "(y \<sqsubset> x \<and> y \<in> X) \<or> x \<sqsubseteq> y"
       proof (elim disjE conjE)
         assume zy: "z \<sqsubset> y" and zY: "z \<in> Y"
         from derivation_useful[OF Y zY yY zy] xfz have xy: "x \<sqsubseteq> y" by auto
         then show ?thesis by auto
       next
         assume zy: "z = y"
         then have "y \<sqsubset> x" using zx by auto
         with zy zX show ?thesis by auto
       next
         assume yz: "y \<sqsubset> z" and yX: "y \<in> X"
         from X.asympartp.trans[OF yz zx yX zX xX] have "y \<sqsubset> x".
         with yX show ?thesis by auto
       qed
     }
     note lim_any this
   }
   note lim_any = this(1) and suc_any = this(2)
   interpret X: well_ordered_set X "(\<sqsubseteq>)" using derivation_well_ordered[OF X].
   interpret Y: well_ordered_set Y "(\<sqsubseteq>)" using derivation_well_ordered[OF Y].
   have XA: "X \<subseteq> A" using derivation_A[OF X].
   have YA: "Y \<subseteq> A" using derivation_A[OF Y].
   from xX yY show ?thesis
   proof (induct x arbitrary: y)
     case (less x)
     note xX = \<open>x \<in> X\<close> and IHx = this(2)
     from xX XA f have xA: "x \<in> A" and fxA: "f x \<in> A" by auto
     from \<open>y \<in> Y\<close>
     show ?case
     proof (induct y)
       case (less y)
       note yY = \<open>y \<in> Y\<close> and IHy = less(2)
       from yY YA f have yA: "y \<in> A" and fyA: "f y \<in> A" by auto
       from X xX show ?case
       proof (cases rule: derivation_cases)
         case (suc Z z)
         note Z = \<open>Z = {z \<in> X. z \<sqsubset> x}\<close> and Zz = \<open>extreme Z (\<sqsubseteq>) z\<close> and xfz = \<open>x = f z\<close>
         then have zx: "z \<sqsubset> x" and zX: "z \<in> X" by auto
         note IHz = IHx[OF zX zx yY]
         have 1: "y \<sqsubset> x \<and> y \<in> X \<or> x \<sqsubseteq> y" using suc_any[OF X Y xX yY Z Zz xfz IHz] IHy by auto
         from Y yY show ?thesis
         proof (cases rule: derivation_cases)
           case (suc W w)
           note W = \<open>W = {w \<in> Y. w \<sqsubset> y}\<close> and Ww = \<open>extreme W (\<sqsubseteq>) w\<close> and yfw = \<open>y = f w\<close> 
           then have wY: "w \<in> Y" and wy: "w \<sqsubset> y" by auto
           have IHw: "w \<sqsubset> x \<and> w \<in> X \<or> w = x  \<or> x \<sqsubset> w \<and> x \<in> Y" using IHy[OF wY wy] by auto
           have "x \<sqsubset> y \<and> x \<in> Y \<or> y \<sqsubseteq> x" using suc_any[OF Y X yY xX W Ww yfw IHw] by auto
           with 1 show ?thesis using antisym xA yA by auto
         next
           case (lim W)
           note W = \<open>W = {w \<in> Y. w \<sqsubset> y}\<close> and fW = \<open>f ` W \<subseteq> W\<close> and Wy = \<open>extreme_bound A (\<sqsubseteq>) W y\<close>
           have "x \<sqsubset> y \<and> x \<in> Y \<or> y \<sqsubseteq> x" using lim_any[OF Y X yY xX W fW Wy] IHy by auto
           with 1 show ?thesis using antisym xA yA by auto
         qed
       next
         case (lim Z)
         note Z = \<open>Z = {z \<in> X. z \<sqsubset> x}\<close> and fZ = \<open>f ` Z \<subseteq> Z\<close> and Zx = \<open>extreme_bound A (\<sqsubseteq>) Z x\<close>
         have 1: "y \<sqsubset> x \<and> y \<in> X \<or> x \<sqsubseteq> y" using lim_any[OF X Y xX yY Z fZ Zx] IHx[OF _ _ yY] by auto
         from Y yY show ?thesis
         proof (cases rule: derivation_cases)
           case (suc W w)
           note W = \<open>W = {w \<in> Y. w \<sqsubset> y}\<close> and Ww = \<open>extreme W (\<sqsubseteq>) w\<close> and yfw = \<open>y = f w\<close>
           then have wY: "w \<in> Y" and wy: "w \<sqsubset> y" by auto
           have IHw: "w \<sqsubset> x \<and> w \<in> X \<or>  w = x  \<or>  x \<sqsubset> w \<and> x \<in> Y" using IHy[OF wY wy] by auto
           have "x \<sqsubset> y \<and> x \<in> Y \<or> y \<sqsubseteq> x" using suc_any[OF Y X yY xX W Ww yfw IHw] by auto
           with 1 show ?thesis using antisym xA yA by auto
         next
           case (lim W)
           note W = \<open>W = {w \<in> Y. w \<sqsubset> y}\<close> and fW = \<open>f ` W \<subseteq> W\<close> and Wy = \<open>extreme_bound A (\<sqsubseteq>) W y\<close>
           have "x \<sqsubset> y \<and> x \<in> Y \<or> y \<sqsubseteq> x" using lim_any[OF Y X yY xX W fW Wy] IHy by auto
           with 1 show ?thesis using antisym xA yA by auto
         qed
       qed
     qed
   qed
 qed
 
 interpretation derivable: well_ordered_set "{x. derivable x}" "(\<sqsubseteq>)"
 proof (rule well_ordered_set.intro)
   show "antisymmetric {x. derivable x} (\<sqsubseteq>)"
     apply unfold_locales by (auto dest: derivable_A antisym)
   show "well_related_set {x. derivable x} (\<sqsubseteq>)"
   apply (fold UN_derivations_eq_derivable)
-  apply (rule lower_UN_well_related)
+  apply (rule closed_UN_well_related)
   by (auto dest: derivation_well_ordered derivations_cross_compare well_ordered_set.axioms)
 qed
 
 lemmas derivable_well_ordered = derivable.well_ordered_set_axioms
 lemmas derivable_total_ordered = derivable.total_ordered_set_axioms
 lemmas derivable_well_related = derivable.well_related_set_axioms
 
 lemma pred_unique:
   assumes X: "derivation X" and xX: "x \<in> X"
   shows "{z \<in> X. z \<sqsubset> x} = {z. derivable z \<and> z \<sqsubset> x}"
 proof
   { fix z assume "z \<in> X" and "z \<sqsubset> x"
     then have "derivable z \<and> z \<sqsubset> x" using X by (auto simp: derivable_def)
   }
   then show "{z \<in> X. z \<sqsubset> x} \<subseteq> {z. derivable z \<and> z \<sqsubset> x}" by auto
   { fix z assume "derivable z" and zx: "z \<sqsubset> x"
     then obtain Y where Y: "derivation Y" and zY: "z \<in> Y" by (auto simp: derivable_def)
     then have "z \<in> X" using derivations_cross_compare[OF X Y xX zY] zx by auto
   }
   then show "{z \<in> X. z \<sqsubset> x} \<supseteq> {z. derivable z \<and> z \<sqsubset> x}" by auto
 qed
 
 text \<open>The set of all derivable elements is itself a derivation.\<close>
 
 lemma derivation_derivable: "derivation {x. derivable x}"
   apply (unfold derivation_def)
   apply (safe intro!: derivable_A derivable.well_ordered_set_axioms elim!: derivableE)
   apply (unfold mem_Collect_eq pred_unique[symmetric])
   by (auto simp: derivation_def)
 
 text \<open>Finally, if the set of all derivable elements admits a supremum, then it is a fixed point.\<close>
 
 lemma
   assumes p: "extreme_bound A (\<sqsubseteq>) {x. derivable x} p"
   shows sup_derivable_qfp: "f p \<sim> p" and sup_derivable_fp: "f p = p"
 proof (intro antisym sympartpI)
   define P where "P \<equiv> {x. derivable x}"
   have pA: "p \<in> A" using p by auto
   have P: "derivation P" using derivation_derivable by (simp add: P_def)
   from derivable_closed have fP: "f ` P \<subseteq> P" by (auto simp: P_def)
   from derivation_lim[OF P fP] p
   have pP: "p \<in> P" by (auto simp: P_def intro:derivableI)
   with fP have "f p \<in> P" by auto
   with p show fpp: "f p \<sqsubseteq> p" by (auto simp: P_def)
   show pfp: "p \<sqsubseteq> f p" apply (rule derivation_infl[rule_format, OF P]) using pP by (auto simp: P_def)
   from fpp pfp p f show "f p = p" by (auto intro!: antisym)
 qed
 
 end
 
 text "The assumptions are satisfied by monotone functions."
 
 context
   assumes mono: "monotone_on A (\<sqsubseteq>) (\<sqsubseteq>) f"
 begin
 
 lemma mono_imp_derivation_infl:
   "\<forall>X x y. derivation X \<longrightarrow> x \<in> X \<longrightarrow> y \<in> X \<longrightarrow> x \<sqsubseteq> y \<longrightarrow> x \<sqsubseteq> f y"
 proof (intro allI impI)
   fix X x y
   assume X: "derivation X" and xX: "x \<in> X" and yX: "y \<in> X" and xy: "x \<sqsubseteq> y"
   interpret X: well_ordered_set X "(\<sqsubseteq>)" using derivation_well_ordered[OF X].
   note XA = derivation_A[OF X]
   from xX yX xy show "x \<sqsubseteq> f y"
   proof (induct x)
     case (less x)
     note IH = this(2) and xX = \<open>x \<in> X\<close> and yX = \<open>y \<in> X\<close> and xy = \<open>x \<sqsubseteq> y\<close>
     from xX yX XA have xA: "x \<in> A" and yA: "y \<in> A" by auto
     from X xX show ?case
     proof (cases rule: derivation_cases)
       case (suc Z z)
       then have zX: "z \<in> X" and zsx: "z \<sqsubset> x" and xfz: "x = f z" by auto
       then have zx: "z \<sqsubseteq> x" by auto
       from X.trans[OF zx xy zX xX yX] have zy: "z \<sqsubseteq> y".
       from zX XA have zA: "z \<in> A" by auto
       from zy monotone_onD[OF mono] zA yA xfz show "x \<sqsubseteq> f y" by auto
     next
       case (lim Z)
       note Z = \<open>Z = {z \<in> X. z \<sqsubset> x}\<close> and Zx = \<open>extreme_bound A (\<sqsubseteq>) Z x\<close>
       from f yA have fyA: "f y \<in> A" by auto
       have "bound Z (\<sqsubseteq>) (f y)"
       proof
         fix z assume zZ: "z \<in> Z"
         with Z xX have zsx: "z \<sqsubset> x" and zX: "z \<in> X" by auto
         then have zx: "z \<sqsubseteq> x" by auto
         from X.trans[OF zx xy zX xX yX] have zy: "z \<sqsubseteq> y".
         from IH[OF zX zsx yX] zy show "z \<sqsubseteq> f y" by auto
       qed
       with Zx fyA show ?thesis by auto
     qed
   qed
 qed
 
 lemma mono_imp_derivation_f_refl:
   "\<forall>X x. derivation X \<longrightarrow> x \<in> X \<longrightarrow> f x \<sqsubseteq> f x"
 proof (intro allI impI)
   fix X x
   assume X: "derivation X" and xX: "x \<in> X"
   interpret X: well_ordered_set X "(\<sqsubseteq>)" using derivation_well_ordered[OF X].
   note XA = derivation_A[OF X]
   from xX have "x \<sqsubseteq> x" by auto
   from monotone_onD[OF mono this] xX XA show "f x \<sqsubseteq> f x" by auto
 qed
 
 corollary mono_imp_sup_derivable_fp:
   assumes p: "extreme_bound A (\<sqsubseteq>) {x. derivable x} p"
   shows "f p = p"
   by (simp add: sup_derivable_fp[OF mono_imp_derivation_infl mono_imp_derivation_f_refl p])
 
 lemma mono_imp_sup_derivable_lfp:
   assumes p: "extreme_bound A (\<sqsubseteq>) {x. derivable x} p"
   shows "extreme {q \<in> A. f q = q} (\<sqsupseteq>) p"
 proof (safe intro!: extremeI)
   from p show "p \<in> A" by auto
   from sup_derivable_fp[OF mono_imp_derivation_infl mono_imp_derivation_f_refl p]
   show "f p = p".
   fix q assume qA: "q \<in> A" and fqq: "f q = q"
   have "bound {x. derivable x} (\<sqsubseteq>) q"
   proof (safe intro!: boundI elim!:derivableE)
     fix x X
     assume X: "derivation X" and xX: "x \<in> X"
     from X interpret well_ordered_set X "(\<sqsubseteq>)" by (rule derivation_well_ordered)
     from xX show "x \<sqsubseteq> q"
     proof (induct x)
       case (less x)
       note xP = this(1) and IH = this(2)
       with X show ?case
       proof (cases rule: derivation_cases)
         case (suc Z z)
         with IH[of z] have zq: "z \<sqsubseteq> q" and zX: "z \<in> X" by auto
         from monotone_onD[OF mono zq] zX qA derivation_A[OF X]
         show ?thesis by (auto simp: fqq suc)
       next
         case lim
         with IH have "bound {z \<in> X. z \<sqsubset> x} (\<sqsubseteq>) q" by auto
         with lim qA show ?thesis by auto
       qed
     qed
   qed
   with p qA show "p \<sqsubseteq> q" by auto
 qed
 
 lemma mono_imp_ex_least_fp:
   assumes comp: "well_complete A (\<sqsubseteq>)"
   shows "\<exists>p. extreme {q \<in> A. f q = q} (\<sqsupseteq>) p"
 proof-
   interpret fixed_point_proof using f by unfold_locales
   note as = antisymmetric_axioms
   note infl = mono_imp_derivation_infl
   note refl = mono_imp_derivation_f_refl
   have wr: "well_related_set {x. derivable x} (\<sqsubseteq>)"
     using derivable_well_related[OF infl refl].
   have "\<exists>p. extreme_bound A (\<sqsubseteq>) {x. derivable x} p"
     apply (rule completeD[OF comp])
     using derivable_A wr by auto
   then obtain p where p: "extreme_bound A (\<sqsubseteq>) {x. derivable x} p" by auto
   from p mono_imp_sup_derivable_lfp[OF p] sup_derivable_qfp[OF infl refl p]
   show ?thesis by auto
 qed
 
 end
 
 end
 
 end
 
 text \<open>Bourbaki-Witt Theorem on well-complete pseudo-ordered set:\<close>
 theorem (in pseudo_ordered_set) well_complete_infl_imp_ex_fp:
   assumes comp: "well_complete A (\<sqsubseteq>)"
     and f: "f ` A \<subseteq> A" and infl: "\<forall>x \<in> A. \<forall>y \<in> A. x \<sqsubseteq> y \<longrightarrow> x \<sqsubseteq> f y"
   shows "\<exists>p \<in> A. f p = p"
 proof-
   note as = antisymmetric_axioms
   interpret fixed_point_proof using f by unfold_locales
   have dinfl: "\<forall>X x y. derivation X \<longrightarrow> x \<in> X \<longrightarrow> y \<in> X \<longrightarrow> x \<sqsubseteq> y \<longrightarrow> x \<sqsubseteq> f y"
     using infl by (auto dest!:derivation_A)
   have drefl: "\<forall>X x. derivation X \<longrightarrow> x \<in> X \<longrightarrow> f x \<sqsubseteq> f x" using f by (auto dest!: derivation_A)
   have "\<exists>p. extreme_bound A (\<sqsubseteq>) {x. derivable x} p"
     apply (rule completeD[OF comp])
     using derivable_well_related[OF as dinfl drefl] derivable_A by auto
   with sup_derivable_fp[OF as dinfl drefl]
   show ?thesis by auto
 qed
 
 
 section \<open>Completeness of (Quasi-)Fixed Points\<close>
 
 text \<open>We now prove that, under attractivity, the set of quasi-fixed points is complete.\<close>
 
 definition setwise where "setwise r X Y \<equiv> \<forall>x\<in>X. \<forall>y\<in>Y. r x y"
 
 lemmas setwiseI[intro] = setwise_def[unfolded atomize_eq, THEN iffD2, rule_format]
 lemmas setwiseE[elim] = setwise_def[unfolded atomize_eq, THEN iffD1, elim_format, rule_format]
 
 context fixed_point_proof begin
 
 abbreviation setwise_less_eq (infix "\<sqsubseteq>\<^sup>s" 50) where "(\<sqsubseteq>\<^sup>s) \<equiv> setwise (\<sqsubseteq>)"
 
 subsection \<open>Least Quasi-Fixed Points for Attractive Relations.\<close>
 
 lemma attract_mono_imp_least_qfp:
   assumes attract: "attractive A (\<sqsubseteq>)"
     and comp: "well_complete A (\<sqsubseteq>)"
     and mono: "monotone_on A (\<sqsubseteq>) (\<sqsubseteq>) f"
   shows "\<exists>c. extreme {p \<in> A. f p \<sim> p \<or> f p = p} (\<sqsupseteq>) c \<and> f c \<sim> c"
 proof-
   interpret attractive using attract by auto
   interpret sym: transitive A "(\<sim>)" using sym_transitive.
   define ecl ("[_]\<^sub>\<sim>") where "[x]\<^sub>\<sim> \<equiv> {y \<in> A. x \<sim> y} \<union> {x}" for x
   define Q where "Q \<equiv> {[x]\<^sub>\<sim> |. x \<in> A}"
   { fix X x assume XQ: "X \<in> Q" and xX: "x \<in> X"
     then have XA: "X \<subseteq> A" by (auto simp: Q_def ecl_def)
     then have xA: "x \<in> A" using xX by auto
     obtain q where qA: "q \<in> A" and X: "X = [q]\<^sub>\<sim>" using XQ by (auto simp: Q_def)
     have xqqx: "x \<sim> q \<or> x = q" using X xX by (auto simp: ecl_def)
     {fix y assume yX: "y \<in> X"
       then have yA: "y \<in> A" using XA by auto
       have "y \<sim> q \<or> y = q" using yX X by (auto simp: ecl_def)
       then have "x \<sim> y \<or> y = x" using sym_order_trans xqqx xA qA yA by blast
     }
     then have 1: "X \<subseteq> [x]\<^sub>\<sim>" using X qA by (auto simp: ecl_def)
     { fix y assume "y \<in> A" and "x \<sim> y \<or> y = x"
       then have "q \<sim> y \<or> y = q" using sym_order_trans xqqx xA qA by blast
     }
     then have 2: "X \<supseteq> [x]\<^sub>\<sim>" using X xX by (auto simp: ecl_def)
     from 1 2 have "X = [x]\<^sub>\<sim>" by auto
   }
   then have XQx: "\<forall>X \<in> Q. \<forall>x \<in> X. X = [x]\<^sub>\<sim>" by auto
   have RSLE_eq: "X \<in> Q \<Longrightarrow> Y \<in> Q \<Longrightarrow> x \<in> X \<Longrightarrow> y \<in> Y \<Longrightarrow> x \<sqsubseteq> y \<Longrightarrow> X \<sqsubseteq>\<^sup>s Y" for X Y x y
   proof-
     assume XQ: "X \<in> Q" and YQ: "Y \<in> Q" and xX: "x \<in> X" and yY: "y \<in> Y" and xy: "x \<sqsubseteq> y"
     then have XA: "X \<subseteq> A" and YA: "Y \<subseteq> A" by (auto simp: Q_def ecl_def)
     then have xA: "x \<in> A" and yA: "y \<in> A" using xX yY by auto
     { fix xp yp assume xpX: "xp \<in> X" and ypY: "yp \<in> Y"
       then have xpA: "xp \<in> A" and ypA: "yp \<in> A" using XA YA by auto
       then have "xp \<sim> x \<or> xp = x" using xpX XQx xX XQ by (auto simp: ecl_def)
       then have xpy: "xp \<sqsubseteq> y" using attract[OF _ _ xy xpA xA yA] xy by blast
       have "yp \<sim> y \<or> yp = y" using ypY XQx yY YQ by (auto simp: ecl_def)
       then have "xp \<sqsubseteq> yp" using dual.attract[OF _ _ xpy ypA yA xpA] xpy by blast
     }
     then show "X \<sqsubseteq>\<^sup>s Y" using XQ YQ XA YA by auto
   qed
   have compQ: "well_complete Q (\<sqsubseteq>\<^sup>s)"
   proof (intro completeI, safe)
     fix XX assume XXQ: "XX \<subseteq> Q" and XX: "well_related_set XX (\<sqsubseteq>\<^sup>s)"
     have BA: "\<Union>XX \<subseteq> A" using XXQ by (auto simp: Q_def ecl_def)
     from XX interpret XX: well_related_set XX "(\<sqsubseteq>\<^sup>s)".
     interpret UXX: semiattractive "\<Union>XX" "(\<sqsubseteq>)" by (rule semiattractive_subset[OF BA])
     have "well_related_set (\<Union>XX) (\<sqsubseteq>)"
     proof(unfold_locales)
       fix Y assume YXX: "Y \<subseteq> \<Union>XX" and Y0: "Y \<noteq> {}"
       have "{X \<in> XX. X \<inter> Y \<noteq> {}} \<noteq> {}" using YXX Y0 by auto
       from XX.nonempty_imp_ex_extreme[OF _ this]
       obtain E where E: "extreme {X \<in> XX. X \<inter> Y \<noteq> {}} (\<sqsubseteq>\<^sup>s)\<^sup>- E" by auto
       then have "E \<inter> Y \<noteq> {}" by auto
       then obtain e where eE: "e \<in> E" and eX: "e \<in> Y" by auto
       have "extreme Y (\<sqsupseteq>) e"
       proof (intro extremeI eX)
         fix x assume xY: "x \<in> Y"
         with YXX obtain X where XXX: "X \<in> XX" and xX: "x \<in> X" by auto
         with xY E XXX have "E \<sqsubseteq>\<^sup>s X" by auto
         with eE xX show "e \<sqsubseteq> x" by auto
       qed
       then show "\<exists>e. extreme Y (\<sqsupseteq>) e" by auto
     qed
     with completeD[OF comp BA]
     obtain b where extb: "extreme_bound A (\<sqsubseteq>) (\<Union>XX) b" by auto
     then have bb: "b \<sqsubseteq> b" using extreme_def bound_def by auto
     have bA: "b \<in> A" using extb extreme_def by auto
     then have XQ: "[b]\<^sub>\<sim> \<in> Q" using Q_def bA by auto
     have bX: "b \<in> [b]\<^sub>\<sim>" by (auto simp: ecl_def)
     have "extreme_bound Q (\<sqsubseteq>\<^sup>s) XX [b]\<^sub>\<sim>"
     proof(intro extreme_boundI)
       show "[b]\<^sub>\<sim> \<in> Q" using XQ.
     next
       fix Y assume YXX: "Y \<in> XX"
       then have YQ: "Y \<in> Q" using XXQ by auto
       then obtain y where yA: "y \<in> A" and Yy: "Y = [y]\<^sub>\<sim>" by (auto simp: Q_def)
       then have yY: "y \<in> Y" by (auto simp: ecl_def)
       then have "y \<in> \<Union>XX" using yY YXX by auto
       then have "y \<sqsubseteq> b" using extb by auto
       then show "Y \<sqsubseteq>\<^sup>s [b]\<^sub>\<sim>" using RSLE_eq[OF YQ XQ yY bX] by auto
     next
       fix Z assume boundZ: "bound XX (\<sqsubseteq>\<^sup>s) Z" and ZQ: "Z \<in> Q"
       then obtain z where zA: "z \<in> A" and Zz: "Z = [z]\<^sub>\<sim>" by (auto simp: Q_def)
       then have zZ: "z \<in> Z" by (auto simp: ecl_def)
       { fix y assume "y \<in> \<Union>XX"
         then obtain Y where yY: "y \<in> Y" and YXX: "Y \<in> XX" by auto
         then have YA: "Y \<subseteq> A" using XXQ Q_def by (auto simp: ecl_def)
         then have "Y \<sqsubseteq>\<^sup>s Z" using YXX boundZ bound_def by auto
         then have "y \<sqsubseteq> z" using yY zZ by auto
       }
       then have "bound (\<Union>XX) (\<sqsubseteq>) z" by auto
       then have "b \<sqsubseteq> z" using extb zA by auto
       then show "[b]\<^sub>\<sim> \<sqsubseteq>\<^sup>s Z" using RSLE_eq[OF XQ ZQ bX zZ] by auto
     qed
     then show "Ex (extreme_bound Q (\<sqsubseteq>\<^sup>s) XX)" by auto
   qed
   interpret Q: antisymmetric Q "(\<sqsubseteq>\<^sup>s)"
   proof
     fix X Y assume XY: "X \<sqsubseteq>\<^sup>s Y" and YX: "Y \<sqsubseteq>\<^sup>s X" and XQ: "X \<in> Q" and YQ: "Y \<in> Q"
     then obtain q where qA: "q \<in> A" and X: "X = [q]\<^sub>\<sim>" using Q_def by auto
     then have qX: "q \<in> X" using X by (auto simp: ecl_def)
     then obtain p where pA: "p \<in> A" and Y: "Y = [p]\<^sub>\<sim>" using YQ Q_def by auto
     then have pY: "p \<in> Y" using X by (auto simp: ecl_def)
     have pq: "p \<sqsubseteq> q" using  XQ YQ YX qX pY by auto
     have "q \<sqsubseteq> p" using XQ YQ XY qX pY by auto
     then have "p \<in> X" using pq X pA by (auto simp: ecl_def)
     then have "X = [p]\<^sub>\<sim>" using XQ XQx by auto
     then show "X = Y" using Y by (auto simp: ecl_def)
   qed
   define F where "F X \<equiv> {y \<in> A. \<exists>x \<in> X. y \<sim> f x} \<union> f ` X" for X
   have XQFXQ: "\<And>X. X \<in> Q \<Longrightarrow> F X \<in> Q"
   proof-
     fix X assume XQ: "X \<in> Q"
     then obtain x where xA: "x \<in> A" and X: "X = [x]\<^sub>\<sim>" using Q_def by auto
     then have xX: "x \<in> X" by (auto simp: ecl_def)
     have fxA: "f x \<in> A" using xA f by auto
     have FXA: "F X \<subseteq> A" using f fxA X by (auto simp: F_def ecl_def)
     have "F X = [f x]\<^sub>\<sim>"
     proof (unfold X, intro equalityI subsetI)
       fix z assume zFX: "z \<in> F [x]\<^sub>\<sim>"
       then obtain y where yX: "y \<in> [x]\<^sub>\<sim>" and zfy: "z \<sim> f y \<or> z = f y" by (auto simp: F_def)
       have yA: "y \<in> A" using yX xA by (auto simp: ecl_def)
       with f have fyA: "f y \<in> A" by auto
       have zA: "z \<in> A" using zFX FXA by (auto simp: X)
       have "y \<sim> x \<or> y = x" using X yX by (auto simp: ecl_def)
       then have "f y \<sim> f x \<or> f y = f x" using mono xA yA by (auto simp: monotone_on_def)
       then have "z \<sim> f x \<or> z = f x" using zfy sym.trans[OF _ _ zA fyA fxA] by (auto simp:)
       with zA show "z \<in> [f x]\<^sub>\<sim>" by (auto simp: ecl_def)
     qed (auto simp: xX F_def ecl_def)
     with FXA show "F X \<in> Q" by (auto simp: Q_def ecl_def)
   qed
   then have F: "F ` Q \<subseteq> Q" by auto
   then interpret Q: fixed_point_proof Q "(\<sqsubseteq>\<^sup>s)" F by unfold_locales
   have monoQ: "monotone_on Q (\<sqsubseteq>\<^sup>s) (\<sqsubseteq>\<^sup>s) F" 
   proof (intro monotone_onI)
     fix X Y assume XQ: "X \<in> Q" and YQ: "Y \<in> Q" and XY: "X \<sqsubseteq>\<^sup>s Y"
     then obtain x y where xX: "x \<in> X" and yY: "y \<in> Y" using Q_def by (auto simp: ecl_def)
     then have xA: "x \<in> A" and yA: "y \<in> A" using XQ YQ by (auto simp: Q_def ecl_def)
     have "x \<sqsubseteq> y" using XY xX yY by auto
     then have fxfy: "f x \<sqsubseteq> f y" using monotone_on_def[of A "(\<sqsubseteq>)" "(\<sqsubseteq>)" f] xA yA mono by auto
     have fxgX: "f x \<in> F X" using xX F_def by blast
     have fygY: "f y \<in> F Y" using yY F_def by blast
     show "F X \<sqsubseteq>\<^sup>s F Y" using RSLE_eq[OF XQFXQ[OF XQ] XQFXQ[OF YQ] fxgX fygY fxfy].
   qed
   have QdA: "{x. Q.derivable x} \<subseteq> Q" using Q.derivable_A by auto
   note asQ = Q.antisymmetric_axioms
   note infl = Q.mono_imp_derivation_infl[OF asQ monoQ]
   note f_refl = Q.mono_imp_derivation_f_refl[OF asQ monoQ]
   from Q.mono_imp_ex_least_fp[OF asQ monoQ compQ]
   obtain P where P: "extreme {q \<in> Q. F q = q} (\<sqsubseteq>\<^sup>s)\<^sup>- P" by auto
   then have PQ: "P \<in> Q" by (auto simp: extreme_def)
   from P have FPP: "F P = P" using PQ by auto
   with P have PP: "P \<sqsubseteq>\<^sup>s P" by auto
   from P obtain p where pA: "p \<in> A" and Pp: "P = [p]\<^sub>\<sim>" using Q_def by auto
   then have pP: "p \<in> P" by (auto simp: ecl_def)
   then have fpA: "f p \<in> A" using pA f by auto
   have "f p \<in> F P" using pP F_def fpA by auto
   then have "F P = [f p]\<^sub>\<sim>" using XQx XQFXQ[OF PQ] by auto
   then have fp: "f p \<sim> p \<or> f p = p" using pP FPP by (auto simp: ecl_def)
   have "p \<sqsubseteq> p" using PP pP by auto
   with fp have fpp: "f p \<sim> p" by auto
   have e: "extreme {p \<in> A. f p \<sim> p \<or> f p = p} (\<sqsupseteq>) p"
   proof (intro extremeI CollectI conjI pA fp, elim CollectE conjE)
     fix q assume qA: "q \<in> A" and fq: "f q \<sim> q \<or> f q = q"
     define Z where "Z \<equiv> {z \<in> A. q \<sim> z}\<union>{q}"
     then have qZ: "q \<in> Z" using qA by auto
     then have ZQ: "Z \<in> Q" using qA by (auto simp: Z_def Q_def ecl_def)
     have fqA: "f q \<in> A" using qA f by auto
     then have "f q \<in> Z" using fq by (auto simp: Z_def)
     then have 1: "Z = [f q]\<^sub>\<sim>" using XQx ZQ by auto
     then have "f q \<in> F Z" using qZ fqA by (auto simp: F_def)
     then have "F Z = [f q]\<^sub>\<sim>" using XQx XQFXQ[OF ZQ] by auto
     with 1 have "Z = F Z" by auto
     then have "P \<sqsubseteq>\<^sup>s Z" using P ZQ by auto
     then show "p \<sqsubseteq> q" using pP qZ by auto
   qed
   with fpp show ?thesis using e by auto
 qed
 
 subsection \<open>General Completeness\<close>
 
 lemma attract_mono_imp_fp_qfp_complete:
   assumes attract: "attractive A (\<sqsubseteq>)"
     and comp: "CC-complete A (\<sqsubseteq>)"
     and wr_CC: "\<forall>C \<subseteq> A. well_related_set C (\<sqsubseteq>) \<longrightarrow> C \<in> CC"
     and extend: "\<forall>X \<in> CC. \<forall>Y \<in> CC. X \<sqsubseteq>\<^sup>s Y \<longrightarrow> X \<union> Y \<in> CC"
     and mono: "monotone_on A (\<sqsubseteq>) (\<sqsubseteq>) f"
     and P: "P \<subseteq> {x \<in> A. f x = x}"
   shows "CC-complete ({q \<in> A. f q \<sim> q} \<union> P) (\<sqsubseteq>)"
 proof (intro completeI)
   interpret attractive using attract.
   fix X assume Xfix: "X \<subseteq> {q \<in> A. f q \<sim> q} \<union> P" and XCC: "X \<in> CC"
   with P have XA: "X \<subseteq> A" by auto
   define B where "B \<equiv> {b \<in> A. \<forall>a \<in> X. a \<sqsubseteq> b}"
   { fix s a assume sA: "s \<in> A" and as: "\<forall>a \<in> X. a \<sqsubseteq> s" and aX: "a \<in> X"
     then have aA: "a \<in> A" using XA by auto
     then have fafs: "f a \<sqsubseteq> f s" using mono f aX sA as by (auto elim!: monotone_onE)
     have "a \<sqsubseteq> f s"
     proof (cases "f a = a")
       case True
       then show ?thesis using fafs by auto
     next
       case False
       then have "a \<sim> f a" using P aX Xfix by auto
       also from fafs have "f a \<sqsubseteq> f s" by auto
       finally show ?thesis using f aA sA by auto
     qed
   }
   with f have fBB: "f ` B \<subseteq> B" unfolding B_def by auto
   have BA: "B \<subseteq> A" by (auto simp: B_def)
   have compB: "CC-complete B (\<sqsubseteq>)"
   proof (unfold complete_def, intro allI impI)
     fix Y assume YS: "Y \<subseteq> B" and YCC: "Y \<in> CC"
     with BA have YA: "Y \<subseteq> A" by auto
     define C where "C \<equiv> X\<union>Y"
     then have CA: "C \<subseteq> A" using XA YA C_def by auto
     have XY: "X \<sqsubseteq>\<^sup>s Y" using B_def YS by auto
     then have CCC: "C \<in> CC" using extend XA YA XCC YCC C_def by auto
     then obtain s where s: "extreme_bound A (\<sqsubseteq>) C s"
       using completeD[OF comp CA CCC] by auto
     then have sA: "s \<in> A" by auto
     show "Ex (extreme_bound B (\<sqsubseteq>) Y)"
     proof (intro exI extreme_boundI)
       { fix x assume "x \<in> X"
         then have "x \<sqsubseteq> s" using s C_def by auto
       }
       then show "s \<in> B" using sA B_def by auto
     next
       fix y assume "y \<in> Y"
       then show "y \<sqsubseteq> s" using s C_def using extremeD by auto
     next
       fix c assume cS: "c \<in> B" and "bound Y (\<sqsubseteq>) c"
       then have "bound C (\<sqsubseteq>) c" using C_def B_def by auto
       then show "s \<sqsubseteq> c" using s BA cS by auto
     qed
   qed
   from fBB interpret B: fixed_point_proof B "(\<sqsubseteq>)" f by unfold_locales
   from BA have *: "{x \<in> A. f x \<sim> x} \<inter> B = {x \<in> B. f x \<sim> x}" by auto
   have asB: "attractive B (\<sqsubseteq>)" using attractive_subset[OF BA] by auto
   have monoB: "monotone_on B (\<sqsubseteq>) (\<sqsubseteq>) f" using monotone_on_cmono[OF BA] mono by (auto dest!: le_funD)
   have compB: "well_complete B (\<sqsubseteq>)"
     using wr_CC compB BA by (simp add: complete_def) 
   from B.attract_mono_imp_least_qfp[OF asB compB monoB]
   obtain l where "extreme {p \<in> B. f p \<sim> p \<or> f p = p} (\<sqsupseteq>) l" and fll: "f l \<sim> l" by auto
   with P have l: "extreme ({p \<in> B. f p \<sim> p} \<union> P \<inter> B) (\<sqsupseteq>) l" by auto
   show "Ex (extreme_bound ({q \<in> A. f q \<sim> q} \<union> P) (\<sqsubseteq>) X)"
   proof (intro exI extreme_boundI)
     show "l \<in> {q \<in> A. f q \<sim> q} \<union> P" using l BA by auto
     fix a assume "a \<in> X"
     with l show "a \<sqsubseteq> l" by (auto simp: B_def)
   next
     fix c assume c: "bound X (\<sqsubseteq>) c" and cfix: "c \<in> {q \<in> A. f q \<sim> q} \<union> P"
     with P have cA: "c \<in> A" by auto
     with c have "c \<in> B" by (auto simp: B_def)
     with cfix l show "l \<sqsubseteq> c" by auto
   qed
 qed
 
 lemma attract_mono_imp_qfp_complete:
   assumes "attractive A (\<sqsubseteq>)"
     and "CC-complete A (\<sqsubseteq>)"
     and "\<forall>C \<subseteq> A. well_related_set C (\<sqsubseteq>) \<longrightarrow> C \<in> CC"
     and "\<forall>X \<in> CC. \<forall>Y \<in> CC. X \<sqsubseteq>\<^sup>s Y \<longrightarrow> X \<union> Y \<in> CC"
     and "monotone_on A (\<sqsubseteq>) (\<sqsubseteq>) f"
   shows "CC-complete {p \<in> A. f p \<sim> p} (\<sqsubseteq>)"
   using attract_mono_imp_fp_qfp_complete[OF assms, of "{}"] by simp
 
 lemma antisym_mono_imp_fp_complete:
   assumes anti: "antisymmetric A (\<sqsubseteq>)"
     and comp: "CC-complete A (\<sqsubseteq>)"
     and wr_CC: "\<forall>C \<subseteq> A. well_related_set C (\<sqsubseteq>) \<longrightarrow> C \<in> CC"
     and extend: "\<forall>X \<in> CC. \<forall>Y \<in> CC. X \<sqsubseteq>\<^sup>s Y \<longrightarrow> X \<union> Y \<in> CC"
     and mono: "monotone_on A (\<sqsubseteq>) (\<sqsubseteq>) f"
   shows "CC-complete {p \<in> A. f p = p} (\<sqsubseteq>)"
 proof-
   interpret antisymmetric using anti.
   have *: "{q \<in> A. f q \<sim> q} \<subseteq> {p \<in> A. f p = p}" using f by (auto intro!: antisym)
   from * attract_mono_imp_fp_qfp_complete[OF attractive_axioms comp wr_CC extend mono, of "{p\<in>A. f p = p}"]
   show ?thesis by (auto simp: subset_Un_eq)
 qed
 
 end
 
 subsection \<open>Instances\<close>
 
 subsubsection \<open>Instances under attractivity\<close>
 
 context attractive begin
 
 interpretation less_eq_notations.
 
 text \<open>Full completeness\<close>
 theorem mono_imp_qfp_UNIV_complete:
   assumes comp: "UNIV-complete A (\<sqsubseteq>)" and f: "f ` A \<subseteq> A" and mono: "monotone_on A (\<sqsubseteq>) (\<sqsubseteq>) f"
   shows "UNIV-complete {p \<in> A. f p \<sim> p} (\<sqsubseteq>)"
   apply (intro fixed_point_proof.attract_mono_imp_qfp_complete comp mono)
     apply unfold_locales
   by (auto simp: f)
 
 text \<open>Connex completeness\<close>
 theorem mono_imp_qfp_connex_complete:
   assumes comp: "{X. connex X (\<sqsubseteq>)}-complete A (\<sqsubseteq>)"
     and f: "f ` A \<subseteq> A" and mono: "monotone_on A (\<sqsubseteq>) (\<sqsubseteq>) f"
   shows "{X. connex X (\<sqsubseteq>)}-complete {p \<in> A. f p \<sim> p} (\<sqsubseteq>)"
   apply (intro fixed_point_proof.attract_mono_imp_qfp_complete mono comp)
     apply unfold_locales
   by (auto simp: f intro: connex_union well_related_set.connex_axioms)
 
 text \<open>Directed completeness\<close>
 theorem mono_imp_qfp_directed_complete:
   assumes comp: "{X. directed X (\<sqsubseteq>)}-complete A (\<sqsubseteq>)"
     and f: "f ` A \<subseteq> A" and mono: "monotone_on A (\<sqsubseteq>) (\<sqsubseteq>) f"
   shows "{X. directed X (\<sqsubseteq>)}-complete {p \<in> A. f p \<sim> p} (\<sqsubseteq>)"
   apply (intro fixed_point_proof.attract_mono_imp_qfp_complete mono comp)
     apply unfold_locales
   by (auto simp: f intro!: directed_extend intro: well_related_set.connex_axioms connex.directed)
 
 text \<open>Well Completeness\<close>
 theorem mono_imp_qfp_well_complete:
   assumes comp: "well_complete A (\<sqsubseteq>)"
     and f: "f ` A \<subseteq> A" and mono: "monotone_on A (\<sqsubseteq>) (\<sqsubseteq>) f"
   shows "well_complete {p \<in> A. f p \<sim> p} (\<sqsubseteq>)"
   apply (intro fixed_point_proof.attract_mono_imp_qfp_complete mono comp)
     apply unfold_locales
   by (auto simp: f well_related_extend)
 
 end
 
 subsubsection \<open>Usual instances under antisymmetry \<close>
 
 context antisymmetric begin
 
 text \<open>Knaster--Tarski\<close>
 theorem mono_imp_fp_complete:
   assumes comp: "UNIV-complete A (\<sqsubseteq>)"
     and f: "f ` A \<subseteq> A" and mono: "monotone_on A (\<sqsubseteq>) (\<sqsubseteq>) f"
   shows "UNIV-complete {p \<in> A. f p = p} (\<sqsubseteq>)"
 proof-
   interpret fixed_point_proof using f by unfold_locales
   show ?thesis
     apply (intro antisym_mono_imp_fp_complete mono antisymmetric_axioms comp)
     by auto
 qed
 
 text \<open>Markowsky 1976\<close>
 theorem mono_imp_fp_connex_complete:
   assumes comp: "{X. connex X (\<sqsubseteq>)}-complete A (\<sqsubseteq>)"
     and f: "f ` A \<subseteq> A" and mono: "monotone_on A (\<sqsubseteq>) (\<sqsubseteq>) f"
   shows "{X. connex X (\<sqsubseteq>)}-complete {p \<in> A. f p = p} (\<sqsubseteq>)"
 proof-
   interpret fixed_point_proof using f by unfold_locales
   show ?thesis
     apply (intro antisym_mono_imp_fp_complete antisymmetric_axioms mono comp)
     by (auto intro: connex_union well_related_set.connex_axioms)
 qed
 
 text \<open>Pataraia\<close>
 theorem mono_imp_fp_directed_complete:
   assumes comp: "{X. directed X (\<sqsubseteq>)}-complete A (\<sqsubseteq>)"
     and f: "f ` A \<subseteq> A" and mono: "monotone_on A (\<sqsubseteq>) (\<sqsubseteq>) f"
   shows "{X. directed X (\<sqsubseteq>)}-complete {p \<in> A. f p = p} (\<sqsubseteq>)"
 proof-
   interpret fixed_point_proof using f by unfold_locales
   show ?thesis
     apply (intro antisym_mono_imp_fp_complete mono antisymmetric_axioms comp)
      by (auto intro: directed_extend connex.directed well_related_set.connex_axioms)
 qed
 
 text \<open>Bhatta \& George 2011\<close>
 theorem mono_imp_fp_well_complete:
   assumes comp: "well_complete A (\<sqsubseteq>)"
     and f: "f ` A \<subseteq> A" and mono: "monotone_on A (\<sqsubseteq>) (\<sqsubseteq>) f"
   shows "well_complete {p \<in> A. f p = p} (\<sqsubseteq>)"
 proof-
   interpret fixed_point_proof using f by unfold_locales
   show ?thesis
     apply (intro antisym_mono_imp_fp_complete mono antisymmetric_axioms comp)
     by (auto intro!: antisym well_related_extend)
 qed
 
 end
 
 end