Theory Complete_Non_Orders.Binary_Relations

(*
Author:  Akihisa Yamada (2018-2021)
License: LGPL (see file COPYING.LESSER)
*)
section ‹Binary Relations›

text ‹We start with basic properties of binary relations.›

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

unbundle lattice_syntax

lemma conj_iff_conj_iff_imp_iff: "Trueprop (x  y  x  z)  (x  (y  z))"
  by (auto intro!: equal_intr_rule)

lemma conj_imp_eq_imp_imp: "(P  Q  PROP R)  (P  Q  PROP R)"
  by standard simp_all

lemma tranclp_trancl: "r++ = (λx y. (x,y)  {(a,b). r a b}+)"
  by (auto simp: tranclp_trancl_eq[symmetric])

lemma tranclp_id[simp]: "transp r  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  A  (f^^n) ` A  A" by (induct n, auto)

lemma image_subsetD: "f ` A  B  a  A  f a  B" by auto

text ‹Below we introduce an Isabelle-notation for $\{ \ldots x\ldots \mid x \in X \}$.›

syntax
  "_range" :: "'a  idts  'a set" ("(1{_ /|./ _})")
  "_image" :: "'a  pttrn  'a set  'a set"  ("(1{_ /|./ (_/  _)})")
translations
  "{e |. p}"  "CONST range (λp. e)"
  "{e |. p  A}"  "CONST image (λp. e) A"

lemma image_constant:
  assumes "i. i  I  f i = y"
  shows "f ` I = (if I = {} then {} else {y})"
  using assms by auto


subsection ‹Various Definitions›

text ‹Here we introduce various definitions for binary relations.
The first one is our abbreviation for the dual of a relation.›

abbreviation(input) dual ("(_-)" [1000] 1000) where "r- x y  r y x"

lemma conversep_is_dual[simp]: "conversep = dual" by auto

lemma dual_inf: "(r  s)- = r-  s-" by (auto intro!: ext)

text ‹Monotonicity is already defined in the library, but we want one restricted to a domain.›

lemmas monotone_onE = monotone_on_def[unfolded atomize_eq, THEN iffD1, elim_format, rule_format]

lemma monotone_on_dual: "monotone_on X r s f  monotone_on X r- s- 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  B  monotone_on B  monotone_on A"
   by (intro le_funI, auto simp: monotone_on_def)

text ‹Here we define the following notions in a standard manner›

text ‹The symmetric part of a relation:›

definition sympartp where "sympartp r x y  r x y  r y x"

lemma sympartpI[intro]:
  fixes r (infix "" 50)
  assumes "x  y" and "y  x" shows "sympartp (⊑) x y"
  using assms by (auto simp: sympartp_def)

lemma sympartpE[elim]:
  fixes r (infix "" 50)
  assumes "sympartp (⊑) x y" and "x  y  y  x  thesis" shows thesis
  using assms by (auto simp: sympartp_def)

lemma sympartp_dual: "sympartp r- = sympartp r"
  by (auto intro!:ext simp: sympartp_def)

lemma sympartp_eq[simp]: "sympartp (=) = (=)" by auto

lemma sympartp_sympartp[simp]: "sympartp (sympartp r) = sympartp r" by (auto intro!:ext)

lemma reflclp_sympartp[simp]: "(sympartp r)== = sympartp r==" by auto

definition "equivpartp r x y  x = y  r x y  r y x"

lemma sympartp_reflclp_equivp[simp]: "sympartp r== = equivpartp r" by (auto intro!:ext simp: equivpartp_def)

lemma equivpartI[simp]: "equivpartp r x x"
  and sympartp_equivpartpI: "sympartp r x y  equivpartp r x y"
  and equivpartpCI[intro]: "(x  y  sympartp r x y)  equivpartp r x y"
  by (auto simp:equivpartp_def)

lemma equivpartpE[elim]:
  assumes "equivpartp r x y"
    and "x = y  thesis"
    and "r x y  r y x  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- = equivpartp r"
  by (auto intro!:ext simp: equivpartp_def)

text ‹The asymmetric part:›

definition "asympartp r x y  r x y  ¬ r y x"

lemma asympartpE[elim]:
  fixes r (infix "" 50)
  shows "asympartp (⊑) x y  (x  y  ¬y  x  thesis)  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)

lemma asympartp_dual: "asympartp r- = (asympartp r)-" by auto

text ‹Restriction to a set:›

definition Restrp (infixl "" 60) where "(r  A) a b  a  A  b  A  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_simp[simp]: "a  A  b  A  (r  A) a b  r a b" by auto

lemma Restrp_UNIV[simp]: "r  UNIV  r" by (auto simp: atomize_eq)

lemma Restrp_Restrp[simp]: "r  A  B  r  A  B" by (auto simp: atomize_eq Restrp_def)

lemma sympartp_Restrp[simp]: "sympartp (r  A)  sympartp r  A"
  by (auto simp: atomize_eq)

text ‹Relational images:›
definition Imagep (infixr "```" 59) where "r ``` A  {b. a  A. r a b}"

lemma Imagep_Image: "r ``` A = {(a,b). r a b} `` A"
  by (auto simp: Imagep_def)

lemma in_Imagep: "b  r ``` A  (a  A. r a b)" by (auto simp: Imagep_def)

lemma ImagepI: "a  A  r a b  b  r ``` A" by (auto simp: in_Imagep)

lemma subset_Imagep: "B  r ``` A  (bB. aA. r a b)"
  by (auto simp: Imagep_def)

text ‹Bounds of a set:›
definition "bound X (⊑) b  x  X. x  b" for r (infix "" 50)

lemma
  fixes r (infix "" 50)
  shows boundI[intro!]: "(x. x  X  x  b)  bound X (⊑) b"
    and boundE[elim]: "bound X (⊑) b  ((x. x  X  x  b)  thesis)  thesis"
    and boundD: "bound X (⊑) b  a  X  a  b"
  by (auto simp: bound_def)

lemma bound_empty: "bound {} = (λr x. True)" by auto

lemma bound_cmono: assumes "X  Y" shows "bound Y  bound X"
  using assms by auto

lemmas bound_subset = bound_cmono[THEN le_funD, THEN le_funD, THEN le_boolD, folded atomize_imp]

lemma bound_un: "bound (A  B) = bound A  bound B"
  by auto

lemma bound_insert[simp]:
  fixes r (infix "" 50)
  shows "bound (insert x X) (⊑) b  x  b  bound X (⊑) b" by auto

lemma bound_cong:
  assumes "A = A'"
    and "b = b'"
    and "a. a  A'  le a b' = le' a b'"
  shows "bound A le b = bound A' le' b'"
  by (auto simp: assms)

lemma bound_subsel: "le  le'  bound A le  bound A le'"
  by (auto simp add: bound_def)

text ‹Extreme (greatest) elements in a set:›
definition "extreme X (⊑) e  e  X  (x  X. x  e)" for r (infix "" 50)

lemma
  fixes r (infix "" 50)
  shows extremeI[intro]: "e  X  (x. x  X  x  e)  extreme X (⊑) e"
    and extremeD: "extreme X (⊑) e  e  X" "extreme X (⊑) e  (x. x  X  x  e)"
    and extremeE[elim]: "extreme X (⊑) e  (e  X  (x. x  X  x  e)  thesis)  thesis"
  by (auto simp: extreme_def)

lemma
  fixes r (infix "" 50)
  shows extreme_UNIV[simp]: "extreme UNIV (⊑) t  (x. x  t)" by auto

lemma extreme_iff_bound: "extreme X r e  bound X r e  e  X" by auto

lemma extreme_imp_bound: "extreme X r x  bound X r x" by auto

lemma extreme_inf: "extreme X (r  s) x  extreme X r x  extreme X s x" by auto

lemma extremes_equiv: "extreme X r b  extreme X r c  sympartp r b c" by blast

lemma extreme_cong:
  assumes "A = A'"
    and "b = b'"
    and "a. a  A'  b'  A'  le a b' = le' a b'"
  shows "extreme A le b = extreme A' le' b'"
  by (auto simp: assms extreme_def)

lemma extreme_subset: "X  Y  extreme X r x  extreme Y r y  r x y" by blast

lemma extreme_subrel:
  "le  le'  extreme A le  extreme A le'" by (auto simp: extreme_def)

text ‹Now suprema and infima are given uniformly as follows.
  The definition is restricted to a given set.
›

definition
  "extreme_bound A (⊑) X  extreme {b  A. bound X (⊑) b} (⊑)-" for r (infix "" 50)

lemmas extreme_boundI_extreme = extreme_bound_def[unfolded atomize_eq, THEN fun_cong, THEN iffD2]

lemmas extreme_boundD_extreme = extreme_bound_def[unfolded atomize_eq, THEN fun_cong, THEN iffD1]

context
  fixes A :: "'a set" and less_eq :: "'a  'a  bool" (infix "" 50)
begin

lemma extreme_boundI[intro]:
  assumes "b. bound X (⊑) b  b  A  s  b" and "x. x  X  x  s" and "s  A"
  shows "extreme_bound A (⊑) X s"
  using assms by (auto simp: extreme_bound_def)

lemma extreme_boundD:
  assumes "extreme_bound A (⊑) X s"
  shows "x  X  x  s"
    and "bound X (⊑) b  b  A  s  b"
    and extreme_bound_in: "s  A"
  using assms by (auto simp: extreme_bound_def)

lemma extreme_boundE[elim]:
  assumes "extreme_bound A (⊑) X s"
    and "s  A  bound X (⊑) s  (b. bound X (⊑) b  b  A  s  b)  thesis"
  shows thesis
  using assms by (auto simp: extreme_bound_def)

lemma extreme_bound_imp_bound: "extreme_bound A (⊑) X s  bound X (⊑) s" by auto

lemma extreme_imp_extreme_bound:
  assumes Xs: "extreme X (⊑) s" and XA: "X  A" shows "extreme_bound A (⊑) X s"
  using assms by force

lemma extreme_bound_subset_bound:
  assumes XY: "X  Y"
    and sX: "extreme_bound A (⊑) X s"
    and b: "bound Y (⊑) b" and bA: "b  A"
  shows "s  b"
  using bound_subset[OF XY b] sX bA by auto

lemma extreme_bound_subset:
  assumes XY: "X  Y"
    and sX: "extreme_bound A (⊑) X sX"
    and sY: "extreme_bound A (⊑) Y sY"
  shows "sX  sY"
  using extreme_bound_subset_bound[OF XY sX] sY by auto

lemma extreme_bound_iff:
  "extreme_bound A (⊑) X s  s  A  (c  A. (x  X. x  c)  s  c)  (x  X. x  s)"
  by (auto simp: extreme_bound_def extreme_def)

lemma extreme_bound_empty: "extreme_bound A (⊑) {} x  extreme A (⊑)- x"
  by auto

lemma extreme_bound_singleton_refl[simp]:
  "extreme_bound A (⊑) {x} x  x  A  x  x" by auto

lemma extreme_bound_image_const:
  "x  x  I  {}  (i. i  I  f i = x)  x  A  extreme_bound A (⊑) (f ` I) x"
  by (auto simp: image_constant)

lemma extreme_bound_UN_const:
  "x  x  I  {}  (i y. i  I  P i y  x = y)  x  A 
  extreme_bound A (⊑) (iI. {y. P i y}) x"
  by auto

lemma extreme_bounds_equiv:
  assumes s: "extreme_bound A (⊑) X s" and s': "extreme_bound A (⊑) X s'"
  shows "sympartp (⊑) s s'"
  using s s'
  apply (unfold extreme_bound_def)
  apply (subst sympartp_dual)
  by (rule extremes_equiv)

lemma extreme_bound_sqweeze:
  assumes XY: "X  Y" and YZ: "Y  Z"
    and Xs: "extreme_bound A (⊑) X s" and Zs: "extreme_bound A (⊑) Z s"
  shows "extreme_bound A (⊑) Y s"
proof
  from Xs show "s  A" by auto
  fix b assume Yb: "bound Y (⊑) b" and bA: "b  A"
  from bound_subset[OF XY Yb] have "bound X (⊑) b".
  with Xs bA
  show "s  b" by auto
next
  fix y assume yY: "y  Y"
  with YZ have "y  Z" by auto
  with Zs show "y  s" by auto
qed

lemma bound_closed_imp_extreme_bound_eq_extreme:
  assumes closed: "b  A. bound X (⊑) b  b  X" and XA: "X  A"
  shows "extreme_bound A (⊑) X = extreme X (⊑)"
proof (intro ext iffI extreme_boundI extremeI)
  fix e
  assume "extreme_bound A (⊑) X e"
  then have Xe: "bound X (⊑) e" and "e  A" by auto
  with closed show "e  X" by auto
  fix x assume "x  X"
  with Xe show "x  e" by auto
next
  fix e
  assume Xe: "extreme X (⊑) e"
  then have eX: "e  X" by auto
  with XA show "e  A" by auto
  { fix b assume Xb: "bound X (⊑) b" and "b  A"
    from eX Xb show "e  b" by auto
  }
  fix x assume xX: "x  X" with Xe show "x  e" by auto
qed

end

lemma extreme_bound_cong:
  assumes "A = A'"
    and "X = X'"
    and "a b. a  A'  b  A'  le a b  le' a b"
    and "a b. a  X'  b  A'  le a b  le' a b"
  shows "extreme_bound A le X s = extreme_bound A le' X s"
  apply (unfold extreme_bound_def)
  apply (rule extreme_cong)
  by (auto simp: assms)


text ‹Maximal or Minimal›

definition "extremal X (⊑) x  x  X  (y  X. x  y  y  x)" for r (infix "" 50)

context
  fixes r :: "'a  'a  bool" (infix "" 50)
begin

lemma extremalI:
  assumes "x  X" "y. y  X  x  y  y  x"
  shows "extremal X (⊑) x"
  using assms by (auto simp: extremal_def)

lemma extremalE:
  assumes "extremal X (⊑) x"
    and "x  X  (y. y  X  x  y  y  x)  thesis"
  shows thesis
  using assms by (auto simp: extremal_def)

lemma extremalD:
  assumes "extremal X (⊑) x" shows "x  X" "y  X  x  y  y  x"
  using assms by (auto elim!: extremalE)

end

context
  fixes ir (infix "" 50) and r (infix "" 50) and I f
  assumes mono: "monotone_on I (≼) (⊑) f"
begin

lemma monotone_image_bound:
  assumes "X  I" and "b  I" and "bound X (≼) b"
  shows "bound (f ` X) (⊑) (f b)"
  using assms monotone_onD[OF mono]
  by (auto simp: bound_def)

lemma monotone_image_extreme:
  assumes e: "extreme I (≼) e"
  shows "extreme (f ` I) (⊑) (f e)"
  using e[unfolded extreme_iff_bound] monotone_image_bound[of I e] by auto

end

context
  fixes ir :: "'i  'i  bool" (infix "" 50)
    and r :: "'a  'a  bool" (infix "" 50)
    and f and A and e and I
  assumes fIA: "f ` I  A"
    and mono: "monotone_on I (≼) (⊑) f"
    and e: "extreme I (≼) e"
begin

lemma monotone_extreme_imp_extreme_bound:
  "extreme_bound A (⊑) (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  extreme_bound A (⊑) (f ` I) x"
  using monotone_extreme_imp_extreme_bound by auto

end

subsection ‹Locales for Binary Relations›

text ‹We now define basic properties of binary relations,
in form of \emph{locales}~\cite{Kammuller00,locale}.›

subsubsection ‹Syntactic Locales›

text ‹The following locales do not assume anything, but provide infix notations for
relations.›

locale less_eq_syntax =
  fixes less_eq :: "'a  'a  bool" (infix "" 50)

locale less_syntax =
  fixes less :: "'a  'a  bool" (infix "" 50)

locale equivalence_syntax =
  fixes equiv :: "'a  'a  bool" (infix "" 50)
begin

abbreviation equiv_class ("[_]") where "[x]  { y. x  y }"

end

text ‹Next ones introduce abbreviations for dual etc.
To avoid needless constants, one should be careful when declaring them as sublocales.›

locale less_eq_dualize = less_eq_syntax
begin

abbreviation (input) greater_eq (infix "" 50) where "x  y  y  x"

end

locale less_eq_symmetrize = less_eq_dualize
begin

abbreviation sym (infix "" 50) where "(∼)  sympartp (⊑)"
abbreviation equiv (infix "()" 50) where "()  equivpartp (⊑)"

end

locale less_eq_asymmetrize = less_eq_symmetrize
begin

abbreviation less (infix "" 50) where "(⊏)  asympartp (⊑)"
abbreviation greater (infix "" 50) where "(⊐)  (⊏)-"

lemma asym_cases[consumes 1, case_names asym sym]:
  assumes "x  y" and "x  y  thesis" and "x  y  thesis"
  shows thesis
  using assms by auto

end

locale less_dualize = less_syntax
begin

abbreviation (input) greater (infix "" 50) where "x  y  y  x"

end

locale related_set =
  fixes A :: "'a set" and less_eq :: "'a  'a  bool" (infix "" 50)

subsubsection ‹Basic Properties of Relations›

text ‹In the following we define basic properties in form of locales.›

text ‹Reflexivity restricted on a set:›
locale reflexive = related_set +
  assumes refl[intro]: "x  A  x  x"
begin

lemma eq_implies: "x = y  x  A  x  y" by auto

lemma reflexive_subset: "B  A  reflexive B (⊑)" apply unfold_locales by auto

lemma extreme_singleton[simp]: "x  A  extreme {x} (⊑) y  x = y" by auto

lemma extreme_bound_singleton: "x  A  extreme_bound A (⊑) {x} x" by auto

lemma extreme_bound_cone: "x  A  extreme_bound A (⊑) {a  A. a  x} x" by auto

end

lemmas reflexiveI[intro!] = reflexive.intro

lemma reflexiveE[elim]:
  assumes "reflexive A r" and "(x. x  A  r x x)  thesis" shows thesis
  using assms by (auto simp: reflexive.refl)

lemma reflexive_cong:
  "(a b. a  A  b  A  r a b  r' a b)  reflexive A r  reflexive A r'"
  by (simp add: reflexive_def)

locale irreflexive = related_set A "(⊏)" for A and less (infix "" 50) +
  assumes irrefl: "x  A  ¬ x  x"
begin

lemma irreflD[simp]: "x  x  ¬x  A" by (auto simp: irrefl)

lemma implies_not_eq: "x  y  x  A  x  y" by auto

lemma Restrp_irreflexive: "irreflexive UNIV ((⊏)A)"
  apply unfold_locales by auto

lemma irreflexive_subset: "B  A  irreflexive B (⊏)" apply unfold_locales by auto

end

lemmas irreflexiveI[intro!] = irreflexive.intro

lemma irreflexive_cong:
  "(a b. a  A  b  A  r a b  r' a b)  irreflexive A r  irreflexive A r'"
  by (simp add: irreflexive_def)

context reflexive begin

interpretation less_eq_asymmetrize.

lemma asympartp_irreflexive: "irreflexive A (⊏)" by auto

end

locale transitive = related_set +
  assumes trans[trans]: "x  y  y  z  x  A  y  A  z  A  x  z"
begin

lemma Restrp_transitive: "transitive UNIV ((⊑)A)"
  apply unfold_locales
  by (auto intro: trans)

lemma bound_trans[trans]: "bound X (⊑) b  b  c  X  A  b  A  c  A  bound X (⊑) c"
  by (auto 0 4 dest: trans)

lemma extreme_bound_mono:
  assumes XY: "xX. yY. x  y" and XA: "X  A" and YA: "Y  A"
    and sX: "extreme_bound A (⊑) X sX"
    and sY: "extreme_bound A (⊑) Y sY"
  shows "sX  sY"
proof (intro extreme_boundD(2)[OF sX] CollectI conjI boundI)
  from sY show sYA: "sY  A" by auto
  from sY have "bound Y (⊑) sY" by auto
  fix x assume xX: "x  X" with XY obtain y where yY: "y  Y" and xy: "x  y" by auto
  from yY sY have "y  sY" by auto
  from trans[OF xy this] xX XA yY YA sYA show "x  sY" by auto
qed

lemma transitive_subset:
  assumes BA: "B  A" shows "transitive B (⊑)"
  apply unfold_locales
  using trans BA by blast

lemma asympartp_transitive: "transitive A (asympartp (⊑))"
  apply unfold_locales by (auto dest:trans)

lemma reflclp_transitive: "transitive A (⊑)=="
  apply unfold_locales by (auto dest: trans)

text ‹The symmetric part is also transitive, but this is done in the later semiattractive locale›

end

lemmas transitiveI = transitive.intro

lemma transitive_ball[code]:
  "transitive A (⊑)  (x  A. y  A. z  A. x  y  y  z  x  z)"
  for less_eq (infix "" 50)
  by (auto simp: transitive_def)

lemma transitive_cong:
  assumes r: "a b. a  A  b  A  r a b  r' a b" shows "transitive A r  transitive A r'"
proof (intro iffI)
  show "transitive A r  transitive A r'"
    apply (intro transitive.intro)
    apply (unfold r[symmetric])
    using transitive.trans.
  show "transitive A r'  transitive A r"
    apply (intro transitive.intro)
    apply (unfold r)
    using transitive.trans.
qed

lemma transitive_empty[intro!]: "transitive {} r" by (auto intro!: transitive.intro)

lemma tranclp_transitive: "transitive A (tranclp r)"
  using tranclp_trans by unfold_locales

locale symmetric = related_set A "(∼)" for A and equiv (infix "" 50) +
  assumes sym[sym]: "x  y  x  A  y  A  y  x"
begin

lemma sym_iff: "x  A  y  A  x  y  y  x"
  by (auto dest: sym)

lemma Restrp_symmetric: "symmetric UNIV ((∼)A)"
  apply unfold_locales by (auto simp: sym_iff)

lemma symmetric_subset: "B  A  symmetric B (∼)"
  apply unfold_locales by (auto dest: sym)

end

lemmas symmetricI[intro] = symmetric.intro

lemma symmetric_cong:
  "(a b. a  A  b  A  r a b  r' a b)  symmetric A r  symmetric A r'"
  by (auto simp: symmetric_def)

lemma symmetric_empty[intro!]: "symmetric {} r" by auto

global_interpretation sympartp: symmetric UNIV "sympartp r"
  rewrites "r. r  UNIV  r"
    and "x. x  UNIV  True"
    and "P1. (True  P1)  Trueprop P1"
    and "P1 P2. (True  PROP P1  PROP P2)  (PROP P1  PROP P2)"
  by auto

lemma sympartp_symmetric: "symmetric A (sympartp r)" by auto

locale antisymmetric = related_set +
  assumes antisym: "x  y  y  x  x  A  y  A  x = y"
begin

interpretation less_eq_symmetrize.

lemma sym_iff_eq_refl: "x  A  y  A  x  y  x = y  y  y" by (auto dest: antisym)

lemma equiv_iff_eq[simp]: "x  A  y  A  x  y  x = y" by (auto dest: antisym elim: equivpartpE)

lemma extreme_unique: "X  A  extreme X (⊑) x  extreme X (⊑) y  x = y"
  by (elim extremeE, auto dest!: antisym[OF _ _ subsetD])

lemma ex_extreme_iff_ex1:
  "X  A  Ex (extreme X (⊑))  Ex1 (extreme X (⊑))" by (auto simp: extreme_unique)

lemma ex_extreme_iff_the:
   "X  A  Ex (extreme X (⊑))  extreme X (⊑) (The (extreme X (⊑)))"
  apply (rule iffI)
  apply (rule theI')
  using extreme_unique by auto

lemma eq_The_extreme: "X  A  extreme X (⊑) x  x = The (extreme X (⊑))"
  by (rule the1_equality[symmetric], auto simp: ex_extreme_iff_ex1[symmetric])

lemma Restrp_antisymmetric: "antisymmetric UNIV ((⊑)A)"
   apply unfold_locales
  by (auto dest: antisym)

lemma antisymmetric_subset: "B  A  antisymmetric B (⊑)"
  apply unfold_locales using antisym by auto

end

lemmas antisymmetricI[intro] = antisymmetric.intro

lemma antisymmetric_cong:
  "(a b. a  A  b  A  r a b  r' a b)  antisymmetric A r  antisymmetric A r'"
  by (auto simp: antisymmetric_def)

lemma antisymmetric_empty[intro!]: "antisymmetric {} r" by auto

lemma antisymmetric_union:
  fixes less_eq (infix "" 50)
  assumes A: "antisymmetric A (⊑)" and B: "antisymmetric B (⊑)"
    and AB: "a  A. b  B. a  b  b  a  a = b"
  shows "antisymmetric (A  B) (⊑)"
proof-
  interpret A: antisymmetric A "(⊑)" using A.
  interpret B: antisymmetric B "(⊑)" using B.
  show ?thesis by (auto dest: AB[rule_format] A.antisym B.antisym)
qed

text ‹The following notion is new, generalizing antisymmetry and transitivity.›

locale semiattractive = related_set +
  assumes attract: "x  y  y  x  y  z  x  A  y  A  z  A  x  z"
begin

interpretation less_eq_symmetrize.

lemma equiv_order_trans[trans]:
  assumes xy: "x  y" and yz: "y  z" and x: "x  A" and y: "y  A" and z: "z  A"
  shows "x  z"
  using attract[OF _ _ _ x y z] xy yz by (auto elim: equivpartpE)

lemma equiv_transitive: "transitive A ()"
proof unfold_locales
  fix x y z
  assume x: "x  A" and y: "y  A" and z: "z  A" and xy: "x  y" and yz: "y  z"
  show "x  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  y" and yz: "y  z" and x: "x  A" and y: "y  A" and z: "z  A"
  shows "x  z"
  using attract[OF _ _ _ x y z] xy yz by auto

interpretation sym: transitive A "(∼)"
proof unfold_locales
  fix x y z
  assume x: "x  A" and y: "y  A" and z: "z  A" and xy: "x  y" and yz: "y  z"
  show "x  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  A" and x: "x  A" and C0: "C  {}" and const: "y  C. y  x"
  shows "extreme_bound A (⊑) C x"
proof (intro extreme_boundI x)
  from C0 obtain c where cC: "c  C" by auto
  with C have c: "c  A" by auto
  from cC const have cx: "c  x" by auto
  fix b assume b: "b  A" and "bound C (⊑) b"
  with cC have cb: "c  b" by auto
  from attract[OF _ _ cb x c b] cx show "x  b" by auto
next
  fix c assume "c  C"
  with const show "c  x" by auto
qed

lemma extreme_bound_quasi_const_iff:
  assumes C: "C  A" and x: "x  A" and y: "y  A" and C0: "C  {}" and const: "z  C. z  x"
  shows "extreme_bound A (⊑) C y  x  y"
proof (intro iffI)
  assume y: "extreme_bound A (⊑) C y"
  note x = extreme_bound_quasi_const[OF C x C0 const]
  from extreme_bounds_equiv[OF y x]
  show "x  y" by auto
next
  assume xy: "x  y"
  with const C sym.trans[OF _ xy _ x y] have Cy: "z  C. z  y" by auto
  show "extreme_bound A (⊑) C y"
    using extreme_bound_quasi_const[OF C y C0 Cy].
qed

lemma Restrp_semiattractive: "semiattractive UNIV ((⊑)A)"
  apply unfold_locales
  by (auto dest: attract)

lemma semiattractive_subset: "B  A  semiattractive B (⊑)"
  apply unfold_locales using attract by blast

end

lemmas semiattractiveI = semiattractive.intro

lemma semiattractive_cong:
  assumes r: "a b. a  A  b  A  r a b  r' a b"
  shows "semiattractive A r  semiattractive A r'" (is "?l  ?r")
proof
  show "?l  ?r"
    apply (intro semiattractive.intro)
    apply (unfold r[symmetric])
    using semiattractive.attract.
  show "?r  ?l"
    apply (intro semiattractive.intro)
    apply (unfold r)
    using semiattractive.attract.
qed

lemma semiattractive_empty[intro!]: "semiattractive {} r"
  by (auto intro!: semiattractiveI)

locale attractive = semiattractive +
  assumes "semiattractive A (⊑)-"
begin

interpretation less_eq_symmetrize.

sublocale dual: semiattractive A "(⊑)-"
  rewrites "r. sympartp (r  A)  sympartp r  A"
    and "r. sympartp (sympartp r)  sympartp r"
    and "sympartp ((⊑)  A)-  (∼)  A"
    and "sympartp (⊑)-  (∼)"
    and "equivpartp (⊑)-  ()"
  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  y" and yz: "y  z" and x: "x  A" and y: "y  A" and z: "z  A"
  shows "x  z"
  using dual.attract[OF _ _ _ z y x] xy yz by auto

lemma order_sym_trans[trans]:
  assumes xy: "x  y" and yz: "y  z" and x: "x  A" and y: "y  A" and z: "z  A"
  shows "x  z"
  using dual.attract[OF _ _ _ z y x] xy yz by auto

lemma extreme_bound_sym_trans:
  assumes XA: "X  A" and Xx: "extreme_bound A (⊑) X x"
    and xy: "x  y" and yA: "y  A"
  shows "extreme_bound A (⊑) X y"
proof (intro extreme_boundI yA)
  from Xx have xA: "x  A" by auto
  {
    fix b assume Xb: "bound X (⊑) b" and bA: "b  A"
    with Xx have xb: "x  b" by auto
    from sym_order_trans[OF _ xb yA xA bA] xy show "y  b" by auto
  }
  fix a assume aX: "a  X"
  with Xx have ax: "a  x" by auto
  from aX XA have aA: "a  A" by auto
  from order_sym_trans[OF ax xy aA xA yA] show "a  y" by auto
qed

interpretation Restrp: semiattractive UNIV "(⊑)A" using Restrp_semiattractive.
interpretation dual.Restrp: semiattractive UNIV "(⊑)-A" using dual.Restrp_semiattractive.

lemma Restrp_attractive: "attractive UNIV ((⊑)A)"
  apply unfold_locales
  using dual.Restrp.attract by auto

lemma attractive_subset: "B  A  attractive B (⊑)"
  apply (intro attractive.intro attractive_axioms.intro)
  using semiattractive_subset dual.semiattractive_subset by auto

end

lemmas attractiveI = attractive.intro[OF _ attractive_axioms.intro]

lemma attractive_cong:
  assumes r: "a b. a  A  b  A  r a b  r' a b"
  shows "attractive A r  attractive A r'"
  by (simp add: attractive_def attractive_axioms_def r cong: semiattractive_cong)

lemma attractive_empty[intro!]: "attractive {} r"
  by (auto intro!: attractiveI)

context antisymmetric begin

sublocale attractive
  apply unfold_locales by (auto dest: antisym)

end

context transitive begin

sublocale attractive
  rewrites "r. sympartp (r  A)  sympartp r  A"
    and "r. sympartp (sympartp r)  sympartp r"
    and "sympartp (⊑)-  sympartp (⊑)"
    and "(sympartp (⊑))-  sympartp (⊑)"
    and "(sympartp (⊑)  A)-  sympartp (⊑)  A"
    and "asympartp (asympartp (⊑)) = asympartp (⊑)"
    and "asympartp (sympartp (⊑)) = bot"
    and "asympartp (⊑)  A = asympartp ((⊑)  A)"
  apply unfold_locales
  by (auto intro!:ext dest: trans simp: atomize_eq)

end

subsection ‹Combined Properties›

text ‹Some combinations of the above basic properties are given names.›

locale asymmetric = related_set A "(⊏)" for A and less (infix "" 50) +
  assumes asym: "x  y  y  x  x  A  y  A  False"
begin

sublocale irreflexive
  apply unfold_locales by (auto dest: asym)

lemma antisymmetric_axioms: "antisymmetric A (⊏)"
  apply unfold_locales by (auto dest: asym)

lemma Restrp_asymmetric: "asymmetric UNIV ((⊏)A)"
  apply unfold_locales
  by (auto dest:asym)

lemma asymmetric_subset: "B  A  asymmetric B (⊏)"
  apply unfold_locales using asym by auto

end

lemmas asymmetricI = asymmetric.intro

lemma asymmetric_iff_irreflexive_antisymmetric:
  fixes less (infix "" 50)
  shows "asymmetric A (⊏)  irreflexive A (⊏)  antisymmetric A (⊏)" (is "?l  ?r")
proof
  assume ?l
  then interpret asymmetric.
  show ?r by (auto dest: asym)
next
  assume ?r
  then interpret irreflexive + antisymmetric A "(⊏)" by auto
  show ?l by (auto intro!:asymmetricI dest: antisym irrefl)
qed

lemma asymmetric_cong:
  assumes r: "a b. a  A  b  A  r a b  r' a b"
  shows "asymmetric A r  asymmetric A r'"
  by (simp add: asymmetric_iff_irreflexive_antisymmetric r cong: irreflexive_cong antisymmetric_cong)

lemma asymmetric_empty: "asymmetric {} r"
  by (auto simp: asymmetric_iff_irreflexive_antisymmetric)

locale quasi_ordered_set = reflexive + transitive
begin

lemma quasi_ordered_subset: "B  A  quasi_ordered_set B (⊑)"
  apply intro_locales
  using reflexive_subset transitive_subset by auto

end

lemmas quasi_ordered_setI = quasi_ordered_set.intro

lemma quasi_ordered_set_cong:
  assumes r: "a b. a  A  b  A  r a b  r' a b"
  shows "quasi_ordered_set A r  quasi_ordered_set A r'"
  by (simp add: quasi_ordered_set_def r cong: reflexive_cong transitive_cong)

lemma quasi_ordered_set_empty[intro!]: "quasi_ordered_set {} r"
  by (auto intro!: quasi_ordered_set.intro)

lemma rtranclp_quasi_ordered: "quasi_ordered_set A (rtranclp r)"
  by (unfold_locales, auto)

locale near_ordered_set = antisymmetric + transitive
begin

interpretation Restrp: antisymmetric UNIV "(⊑)A" using Restrp_antisymmetric.
interpretation Restrp: transitive UNIV "(⊑)A" using Restrp_transitive.

lemma Restrp_near_order: "near_ordered_set UNIV ((⊑)A)"..

lemma near_ordered_subset: "B  A  near_ordered_set B (⊑)"
  apply intro_locales
  using antisymmetric_subset transitive_subset by auto

end

lemmas near_ordered_setI = near_ordered_set.intro

lemma near_ordered_set_cong:
  assumes r: "a b. a  A  b  A  r a b  r' a b"
  shows "near_ordered_set A r  near_ordered_set A r'"
  by (simp add: near_ordered_set_def r cong: antisymmetric_cong transitive_cong)

lemma near_ordered_set_empty[intro!]: "near_ordered_set {} r"
  by (auto intro!: near_ordered_set.intro)

locale pseudo_ordered_set = reflexive + antisymmetric
begin

interpretation less_eq_symmetrize.

lemma sym_eq[simp]: "x  A  y  A  x  y  x = y"
  by (auto simp: refl dest: antisym)

lemma extreme_bound_singleton_eq[simp]: "x  A  extreme_bound A (⊑) {x} y  x = y"
  by (auto intro!: antisym)

lemma eq_iff: "x  A  y  A  x = y  x  y  y  x" by (auto dest: antisym simp:refl)

lemma extreme_order_iff_eq: "e  A  extreme {x  A. x  e} (⊑) s  e = s"
  by (auto intro!: antisym)

lemma pseudo_ordered_subset: "B  A  pseudo_ordered_set B (⊑)"
  apply intro_locales
  using reflexive_subset antisymmetric_subset by auto

end

lemmas pseudo_ordered_setI = pseudo_ordered_set.intro

lemma pseudo_ordered_set_cong:
  assumes r: "a b. a  A  b  A  r a b  r' a b"
  shows "pseudo_ordered_set A r  pseudo_ordered_set A r'"
  by (simp add: pseudo_ordered_set_def r cong: reflexive_cong antisymmetric_cong)

lemma pseudo_ordered_set_empty[intro!]: "pseudo_ordered_set {} r"
  by (auto intro!: pseudo_ordered_setI)

locale partially_ordered_set = reflexive + antisymmetric + transitive
begin

sublocale pseudo_ordered_set + quasi_ordered_set + near_ordered_set ..

lemma partially_ordered_subset: "B  A  partially_ordered_set B (⊑)"
  apply intro_locales
  using reflexive_subset transitive_subset antisymmetric_subset by auto

end

lemmas partially_ordered_setI = partially_ordered_set.intro

lemma partially_ordered_set_cong:
  assumes r: "a b. a  A  b  A  r a b  r' a b"
  shows "partially_ordered_set A r  partially_ordered_set A r'"
  by (simp add: partially_ordered_set_def r cong: reflexive_cong antisymmetric_cong transitive_cong)

lemma partially_ordered_set_empty[intro!]: "partially_ordered_set {} r"
  by (auto intro!: partially_ordered_setI)

locale strict_ordered_set = irreflexive + transitive A "(⊏)"
begin

sublocale asymmetric
proof
  fix x y
  assume x: "x  A" and y: "y  A"
  assume xy: "x  y"
  also assume yx: "y  x"
  finally have "x  x" using x y by auto
  with x show False by auto
qed

lemma near_ordered_set_axioms: "near_ordered_set A (⊏)"
  using antisymmetric_axioms by intro_locales

interpretation Restrp: asymmetric UNIV "(⊏)A" using Restrp_asymmetric.
interpretation Restrp: transitive UNIV "(⊏)A" using Restrp_transitive.

lemma Restrp_strict_order: "strict_ordered_set UNIV ((⊏)A)"..

lemma strict_ordered_subset: "B  A  strict_ordered_set B (⊏)"
  apply intro_locales
  using irreflexive_subset transitive_subset by auto

end

lemmas strict_ordered_setI = strict_ordered_set.intro

lemma strict_ordered_set_cong:
  assumes r: "a b. a  A  b  A  r a b  r' a b"
  shows "strict_ordered_set A r  strict_ordered_set A r'"
  by (simp add: strict_ordered_set_def r cong: irreflexive_cong transitive_cong)

lemma strict_ordered_set_empty[intro!]: "strict_ordered_set {} r"
  by (auto intro!: strict_ordered_set.intro)

locale tolerance = symmetric + reflexive A "(∼)"
begin

lemma tolerance_subset: "B  A  tolerance B (∼)"
  apply intro_locales
  using symmetric_subset reflexive_subset by auto

end

lemmas toleranceI = tolerance.intro

lemma tolerance_cong:
  assumes r: "a b. a  A  b  A  r a b  r' a b"
  shows "tolerance A r  tolerance A r'"
  by (simp add: tolerance_def r cong: reflexive_cong symmetric_cong)

lemma tolerance_empty[intro!]: "tolerance {} r" by (auto intro!: toleranceI)

global_interpretation equiv: tolerance UNIV "equivpartp r"
  rewrites "r. r  UNIV  r"
    and "x. x  UNIV  True"
    and "P1. (True  P1)  Trueprop P1"
    and "P1 P2. (True  PROP P1  PROP P2)  (PROP P1  PROP P2)"
  by unfold_locales (auto simp:equivpartp_def)

locale partial_equivalence = symmetric +
  assumes "transitive A (∼)"
begin

sublocale transitive A "(∼)"
  rewrites "sympartp (∼)A  (∼)A"
    and "sympartp ((∼)A)  (∼)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  A  partial_equivalence B (∼)"
  apply (intro partial_equivalence.intro partial_equivalence_axioms.intro)
  using symmetric_subset transitive_subset by auto

end

lemmas partial_equivalenceI = partial_equivalence.intro[OF _ partial_equivalence_axioms.intro]

lemma partial_equivalence_cong:
  assumes r: "a b. a  A  b  A  r a b  r' a b"
  shows "partial_equivalence A r  partial_equivalence A r'"
  by (simp add: partial_equivalence_def partial_equivalence_axioms_def r
      cong: transitive_cong symmetric_cong)

lemma partial_equivalence_empty[intro!]: "partial_equivalence {} r"
  by (auto intro!: partial_equivalenceI)

locale equivalence = symmetric + reflexive A "(∼)" + transitive A "(∼)"
begin

sublocale tolerance + partial_equivalence + quasi_ordered_set A "(∼)"..

lemma equivalence_subset: "B  A  equivalence B (∼)"
  apply (intro equivalence.intro)
  using symmetric_subset transitive_subset by auto

end

lemmas equivalenceI = equivalence.intro

lemma equivalence_cong:
  assumes r: "a b. a  A  b  A  r a b  r' a b"
  shows "equivalence A r  equivalence A r'"
  by (simp add: equivalence_def r cong: reflexive_cong transitive_cong symmetric_cong)

text ‹Some combinations lead to uninteresting relations.›

context
  fixes r :: "'a  'a  bool" (infix "" 50)
begin

proposition reflexive_irreflexive_is_empty:
  assumes r: "reflexive A (⨝)" and ir: "irreflexive A (⨝)"
  shows "A = {}"
proof (rule ccontr)
  interpret irreflexive A "(⨝)" using ir.
  interpret reflexive A "(⨝)" using r.
  assume "A  {}"
  then obtain a where a: "a  A" by auto
  from a refl have "a  a" by auto
  with irrefl a show False by auto
qed

proposition symmetric_antisymmetric_imp_eq:
  assumes s: "symmetric A (⨝)" and as: "antisymmetric A (⨝)"
  shows "(⨝)A  (=)"
proof-
  interpret symmetric A "(⨝)" + antisymmetric A "(⨝)" using assms by auto
  show "?thesis" using antisym by (auto dest: sym)
qed

proposition nontolerance:
  shows "irreflexive A (⨝)  symmetric A (⨝)  tolerance A (λx y. ¬ x  y)"
proof (intro iffI conjI, elim conjE)
  assume "irreflexive A (⨝)" and "symmetric A (⨝)"
  then interpret irreflexive A "(⨝)" + symmetric A "(⨝)".
  show "tolerance A (λx y. ¬ x  y)" by (unfold_locales, auto dest: sym irrefl)
next
  assume "tolerance A (λx y. ¬ x  y)"
  then interpret tolerance A "λx y. ¬ x  y".
  show "irreflexive A (⨝)" by (auto simp: eq_implies)
  show "symmetric A (⨝)" using sym by auto
qed

proposition irreflexive_transitive_symmetric_is_empty:
  assumes irr: "irreflexive A (⨝)" and tr: "transitive A (⨝)" and sym: "symmetric A (⨝)"
  shows "(⨝)A = bot"
proof (intro ext, unfold bot_fun_def bot_bool_def eq_False, rule notI, erule RestrpE)
  interpret strict_ordered_set A "(⨝)" using assms by (unfold strict_ordered_set_def, auto)
  interpret symmetric A "(⨝)" using assms by auto
  fix x y assume x: "x  A" and y: "y  A"
  assume xy: "x  y"
  also note sym[OF xy x y]
  finally have "x  x" using x y by auto
  with x show False by auto
qed

end

subsection ‹Totality›

locale semiconnex = related_set _ "(⊏)" + less_syntax +
  assumes semiconnex: "x  A  y  A  x  y  x = y  y  x"
begin

lemma cases[consumes 2, case_names less eq greater]:
  assumes "x  A" and "y  A" and "x  y  P" and "x = y  P" and "y  x  P"
  shows "P" using semiconnex assms by auto

lemma neqE:
  assumes "x  A" and "y  A"
  shows "x  y  (x  y  P)  (y  x  P)  P"
  by (cases rule: cases[OF assms], auto)

lemma semiconnex_subset: "B  A  semiconnex B (⊏)"
  apply (intro semiconnex.intro)
  using semiconnex by auto

end

lemmas semiconnexI[intro] = semiconnex.intro

text ‹Totality is negated antisymmetry \cite[Proposition 2.2.4]{Schmidt1993}.›
proposition semiconnex_iff_neg_antisymmetric:
  fixes less (infix "" 50)
  shows "semiconnex A (⊏)  antisymmetric A (λx y. ¬ x  y)" (is "?l  ?r")
proof (intro iffI semiconnexI antisymmetricI)
  assume ?l
  then interpret semiconnex.
  fix x y
  assume "x  A" "y  A" "¬ x  y" and "¬ y  x"
  then show "x = y" by (cases rule: cases, auto)
next
  assume ?r
  then interpret neg: antisymmetric A "(λx y. ¬ x  y)".
  fix x y
  show "x  A  y  A  x  y  x = y  y  x" using neg.antisym by auto
qed

lemma semiconnex_cong:
  assumes r: "a b. a  A  b  A  r a b  r' a b"
  shows "semiconnex A r  semiconnex A r'"
  by (simp add: semiconnex_iff_neg_antisymmetric r cong: antisymmetric_cong)

locale semiconnex_irreflexive = semiconnex + irreflexive
begin

lemma neq_iff: "x  A  y  A  x  y  x  y  y  x" by (auto elim:neqE dest: irrefl)

lemma semiconnex_irreflexive_subset: "B  A  semiconnex_irreflexive B (⊏)"
  apply (intro semiconnex_irreflexive.intro)
  using semiconnex_subset irreflexive_subset by auto

end

lemmas semiconnex_irreflexiveI = semiconnex_irreflexive.intro

lemma semiconnex_irreflexive_cong:
  assumes r: "a b. a  A  b  A  r a b  r' a b"
  shows "semiconnex_irreflexive A r  semiconnex_irreflexive A r'"
  by (simp add: semiconnex_irreflexive_def r cong: semiconnex_cong irreflexive_cong)

locale connex = related_set +
  assumes comparable: "x  A  y  A  x  y  y  x"
begin

interpretation less_eq_asymmetrize.

sublocale reflexive apply unfold_locales using comparable by auto

lemma comparable_cases[consumes 2, case_names le ge]:
  assumes "x  A" and "y  A" and "x  y  P" and "y  x  P" shows "P"
  using assms comparable by auto

lemma comparable_three_cases[consumes 2, case_names less eq greater]:
  assumes "x  A" and "y  A" and "x  y  P" and "x  y  P" and "y  x  P" shows "P"
  using assms comparable by auto

lemma
  assumes x: "x  A" and y: "y  A"
  shows not_iff_asym: "¬x  y  y  x"
    and not_asym_iff: "¬x  y  y  x"
  using comparable[OF x y] by auto

lemma connex_subset: "B  A  connex B (⊑)"
  by (intro connex.intro comparable, auto)

interpretation less_eq_asymmetrize.

end

lemmas connexI[intro] = connex.intro

lemmas connexE = connex.comparable_cases

lemma connex_empty: "connex {} A" by auto

context
  fixes less_eq :: "'a  'a  bool" (infix "" 50)
begin

lemma connex_iff_semiconnex_reflexive: "connex A (⊑)  semiconnex A (⊑)  reflexive A (⊑)"
  (is "?c  ?t  ?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 "(⊑)".
  assume ?r then interpret reflexive.
  from semiconnex show ?c by auto
qed

lemma chain_connect: "Complete_Partial_Order.chain r A  connex A r"
  by (auto intro!: ext simp: atomize_eq connex_def Complete_Partial_Order.chain_def)

lemma connex_union:
  assumes "connex X (⊑)" and "connex Y (⊑)" and "x  X. y  Y. x  y  y  x"
  shows "connex (XY) (⊑)"
  using assms by (auto simp: connex_def)

end

lemma connex_cong:
  assumes r: "a b. a  A  b  A  r a b  r' a b"
  shows "connex A r  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  A" and y: "y  A" shows "¬ y  x  x  y  x  y"
using x y by (cases rule: comparable_cases, auto intro:antisym)

lemma total_pseudo_ordered_subset: "B  A  total_pseudo_ordered_set B (⊑)"
  apply (intro_locales)
  using antisymmetric_subset connex_subset by auto

interpretation less_eq_asymmetrize.

interpretation asympartp: semiconnex_irreflexive A "(⊏)"
proof (intro semiconnex_irreflexive.intro asympartp_irreflexive semiconnexI)
  fix x y assume xA: "x  A" and yA: "y  A"
  with comparable antisym
  show "x  y  x = y  y  x" by (auto simp: asympartp_def)
qed

lemmas asympartp_semiconnex = asympartp.semiconnex_axioms
lemmas asympartp_semiconnex_irreflexive = asympartp.semiconnex_irreflexive_axioms

end

lemmas total_pseudo_ordered_setI = total_pseudo_ordered_set.intro

lemma total_pseudo_ordered_set_cong:
  assumes r: "a b. a  A  b  A  r a b  r' a b"
  shows "total_pseudo_ordered_set A r  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  A  total_quasi_ordered_set B (⊑)"
  using transitive_subset connex_subset by intro_locales

end

lemmas total_quasi_ordered_setI = total_quasi_ordered_set.intro

lemma total_quasi_ordered_set_cong:
  assumes r: "a b. a  A  b  A  r a b  r' a b"
  shows "total_quasi_ordered_set A r  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  A  total_ordered_set B (⊑)"
  using total_quasi_ordered_subset antisymmetric_subset by (intro total_ordered_set.intro)

lemma weak_semiconnex: "semiconnex A (⊑)"
  using connex_axioms by (simp add: connex_iff_semiconnex_reflexive)

interpretation less_eq_asymmetrize.

end

lemmas total_ordered_setI = total_ordered_set.intro[OF total_quasi_ordered_setI]

lemma total_ordered_set_cong:
  assumes r: "a b. a  A  b  A  r a b  r' a b"
  shows "total_ordered_set A r  total_ordered_set A r'"
  by (simp add: total_ordered_set_def r cong: total_quasi_ordered_set_cong antisymmetric_cong)


lemma monotone_connex_image:
  fixes ir (infix "" 50) and r (infix "" 50)
  assumes mono: "monotone_on I (≼) (⊑) f" and connex: "connex I (≼)"
  shows "connex (f ` I) (⊑)"
proof (rule connexI)
  fix x y
  assume "x  f ` I" and "y  f ` I"
  then obtain i j where ij: "i  I" "j  I" and [simp]: "x = f i" "y = f j" by auto
  from connex ij have "i  j  j  i" by (auto elim: connexE)
  with ij mono show "x  y  y  x" by (elim disjE, auto dest: monotone_onD) 
qed

subsection ‹Order Pairs›

text ‹We pair a relation (weak part) with a well-behaving ``strict'' part. Here no assumption is
 put on the ``weak'' part.›

locale compatible_ordering =
  related_set + irreflexive +
  assumes strict_implies_weak: "x  y  x  A  y  A  x  y"
  assumes weak_strict_trans[trans]: "x  y  y  z  x  A  y  A  z  A  x  z"
  assumes strict_weak_trans[trans]: "x  y  y  z  x  A  y  A  z  A  x  z"
begin

text ‹The following sequence of declarations are in order to obtain fact names in a manner
similar to the Isabelle/HOL facts of orders.›

text ‹The strict part is necessarily transitive.›

sublocale strict: transitive A "(⊏)"
  using weak_strict_trans[OF strict_implies_weak] by unfold_locales

sublocale strict_ordered_set A "(⊏)" ..

thm strict.trans asym irrefl

lemma Restrp_compatible_ordering: "compatible_ordering UNIV ((⊑)A) ((⊏)A)"
  apply (unfold_locales)
  by (auto dest: weak_strict_trans strict_weak_trans strict_implies_weak)

lemma strict_implies_not_weak: "x  y  x  A  y  A  ¬ y  x"
  using irrefl weak_strict_trans by blast

lemma weak_implies_not_strict:
  assumes xy: "x  y" and [simp]: "x  A" "y  A"
  shows "¬y  x"
proof 
  assume "y  x"
  also note xy
  finally show False using irrefl by auto
qed

lemma compatible_ordering_subset: assumes "X  A" shows "compatible_ordering X (⊑) (⊏)"
  apply unfold_locales
  using assms strict_implies_weak by (auto intro: strict_weak_trans weak_strict_trans)

end

context transitive begin

interpretation less_eq_asymmetrize.

lemma asym_trans[trans]:
  shows "x  y  y  z  x  A  y  A  z  A  x  z"
    and "x  y  y  z  x  A  y  A  z  A  x  z"
  by (auto 0 3 dest: trans)

lemma asympartp_compatible_ordering: "compatible_ordering A (⊑) (⊏)"
  apply unfold_locales
  by (auto dest: asym_trans)

end

locale reflexive_ordering = reflexive + compatible_ordering

locale reflexive_attractive_ordering = reflexive_ordering + attractive

locale pseudo_ordering = pseudo_ordered_set + compatible_ordering
begin

sublocale reflexive_attractive_ordering..

end

locale quasi_ordering = quasi_ordered_set + compatible_ordering
begin

sublocale reflexive_attractive_ordering..

lemma quasi_ordering_subset: assumes "X  A" shows "quasi_ordering X (⊑) (⊏)"
  by (intro quasi_ordering.intro quasi_ordered_subset compatible_ordering_subset assms)

end

context quasi_ordered_set begin

interpretation less_eq_asymmetrize.

lemma asympartp_quasi_ordering: "quasi_ordering A (⊑) (⊏)"
  by (intro quasi_ordering.intro quasi_ordered_set_axioms asympartp_compatible_ordering)

end

locale partial_ordering = partially_ordered_set + compatible_ordering
begin

sublocale quasi_ordering + pseudo_ordering..

lemma partial_ordering_subset: assumes "X  A" shows "partial_ordering X (⊑) (⊏)"
  by (intro partial_ordering.intro partially_ordered_subset compatible_ordering_subset assms)

end

context partially_ordered_set begin

interpretation less_eq_asymmetrize.

lemma asympartp_partial_ordering: "partial_ordering A (⊑) (⊏)"
  by (intro partial_ordering.intro partially_ordered_set_axioms asympartp_compatible_ordering)

end

locale total_quasi_ordering = total_quasi_ordered_set + compatible_ordering
begin

sublocale quasi_ordering..

lemma total_quasi_ordering_subset: assumes "X  A" shows "total_quasi_ordering X (⊑) (⊏)"
  by (intro total_quasi_ordering.intro total_quasi_ordered_subset compatible_ordering_subset assms)

end

context total_quasi_ordered_set begin

interpretation less_eq_asymmetrize.

lemma asympartp_total_quasi_ordering: "total_quasi_ordering A (⊑) (⊏)"
  by (intro total_quasi_ordering.intro total_quasi_ordered_set_axioms asympartp_compatible_ordering)

end


text ‹Fixing the definition of the strict part is very common, though it looks restrictive
to the author.›
locale strict_quasi_ordering = quasi_ordered_set + less_syntax +
  assumes strict_iff: "x  A  y  A  x  y  x  y  ¬y  x"
begin

sublocale compatible_ordering
proof unfold_locales
  fix x y z
  show "x  A  ¬ x  x" by (auto simp: strict_iff)
  { assume xy: "x  y" and yz: "y  z" and x: "x  A" and y: "y  A" and z: "z  A"
    from yz y z have ywz: "y  z" and zy: "¬z  y" by (auto simp: strict_iff)
    from trans[OF xy ywz]x y z have xz: "x  z" by auto
    from trans[OF _ xy] x y z zy have zx: "¬z  x" by auto 
    from xz zx x z show "x  z" by (auto simp: strict_iff)
  }
  { assume xy: "x  y" and yz: "y  z" and x: "x  A" and y: "y  A" and z: "z  A"
    from xy x y have xwy: "x  y" and yx: "¬y  x" by (auto simp: strict_iff)
    from trans[OF xwy yz]x y z have xz: "x  z" by auto
    from trans[OF yz] x y z yx have zx: "¬z  x" by auto 
    from xz zx x z show "x  z" by (auto simp: strict_iff)
  }
  { show "x  y  x  A  y  A  x  y" by (auto simp: strict_iff) }
qed

end

locale strict_partial_ordering = strict_quasi_ordering + antisymmetric
begin

sublocale partial_ordering..

lemma strict_iff_neq: "x  A  y  A  x  y  x  y  x  y"
  by (auto simp: strict_iff antisym)

end

locale total_ordering = reflexive + compatible_ordering + semiconnex A "(⊏)"
begin

sublocale semiconnex_irreflexive ..

sublocale connex
proof
  fix x y assume x: "x  A" and y: "y  A"
  then show "x  y  y  x"
    by (cases rule: cases, auto dest: strict_implies_weak)
qed

lemma not_weak:
  assumes "x  A" and "y  A" shows "¬ x  y  y  x"
  using assms by (cases rule:cases, auto simp: strict_implies_not_weak dest: strict_implies_weak)

lemma not_strict: "x  A  y  A  ¬ x  y  y  x"
  using not_weak by blast

sublocale strict_partial_ordering
proof
  fix a b
  assume a: "a  A" and b: "b  A"
  then show "a  b  a  b  ¬ b  a" by (auto simp: not_strict[symmetric] dest: asym)
next
  fix x y z assume xy: "x  y" and yz: "y  z" and xA: "x  A" and yA: "y  A" and zA: "z  A"
  with weak_strict_trans[OF yz] show "x  z" by (auto simp: not_strict[symmetric])
next
  fix x y assume xy: "x  y" and yx: "y  x" and xA: "x  A" and yA: "y  A"
  with semiconnex show "x = y" by (auto dest: weak_implies_not_strict)
qed

sublocale total_ordered_set..

context
  fixes s
  assumes s: "x  A. x  s  (z  A. x  z  z  s)" and sA: "s  A"
begin

lemma dense_weakI:
  assumes bound: "x. x  s  x  A  x  y" and yA: "y  A"
  shows "s  y"
proof (rule ccontr)
  assume "¬ ?thesis"
  with yA sA have "y  s" by (simp add: not_weak)
  from s[rule_format, OF yA this]
  obtain x where xA: "x  A" and xs: "x  s" and yx: "y  x" by safe
  have xy: "x  y" using bound[OF xs xA] .
  from yx xy xA yA
  show False by (simp add: weak_implies_not_strict)
qed

lemma dense_bound_iff:
  assumes bA: "b  A" shows "bound {xA. x  s} (⊑) b  s  b"
  using assms sA
  by (auto simp: bound_def intro: strict_implies_weak strict_weak_trans dense_weakI)

lemma dense_extreme_bound:
  "extreme_bound A (⊑) {x  A. x  s} s"
  by (auto intro!: extreme_boundI intro: strict_implies_weak simp: dense_bound_iff sA)

end

lemma ordinal_cases[consumes 1, case_names suc lim]:
  assumes aA: "a  A"
    and suc: "p. extreme {x  A. x  a} (⊑) p  thesis"
    and lim: "extreme_bound A (⊑) {x  A. x  a} a  thesis"
  shows "thesis"
proof (cases "p. extreme {x  A. x  a} (⊑) p")
  case True
  with suc show ?thesis by auto
next
  case False
  show ?thesis
  proof (rule lim, rule dense_extreme_bound, safe intro!: aA)
    fix x assume xA: "x  A" and xa: "x  a"
    show "zA. x  z  z  a"
    proof (rule ccontr)
      assume "¬?thesis"
      with xA xa have "extreme {x  A. x  a} (⊑) x" by (auto simp: not_strict)
      with False show False by auto
    qed
  qed
qed

end

context total_ordered_set begin

interpretation less_eq_asymmetrize.

lemma asympartp_total_ordering: "total_ordering A (⊑) (⊏)"
  by (intro total_ordering.intro reflexive_axioms asympartp_compatible_ordering asympartp_semiconnex)

end

subsection ‹Functions›

definition "pointwise I r f g  i  I. r (f i) (g i)"

lemmas pointwiseI = pointwise_def[unfolded atomize_eq, THEN iffD2, rule_format]

lemmas pointwiseD[simp] = pointwise_def[unfolded atomize_eq, THEN iffD1, rule_format]

lemma pointwise_cong:
  assumes "r = r'" "i. i  I  f i = f' i" "i. i  I  g i = g' i"
  shows "pointwise I r f g = pointwise I r' f' g'"
  using assms by (auto simp: pointwise_def)

lemma pointwise_empty[simp]: "pointwise {} = " by (auto intro!: ext pointwiseI)

lemma dual_pointwise[simp]: "(pointwise I r)- = pointwise I r-"
  by (auto intro!: ext pointwiseI dest: pointwiseD)

lemma pointwise_dual: "pointwise I r- f g  pointwise I r g f" by (auto simp: pointwise_def)

lemma pointwise_un: "pointwise (IJ) r = pointwise I r  pointwise J r"
  by (auto intro!: ext pointwiseI)

lemma pointwise_unI[intro!]: "pointwise I r f g  pointwise J r f g  pointwise (I  J) r f g"
  by (auto simp: pointwise_un)

lemma pointwise_bound: "bound F (pointwise I r) f  (i  I. bound {f i |. f  F} r (f i))"
  by (auto intro!:pointwiseI elim!: boundE)

lemma pointwise_extreme:
  shows "extreme F (pointwise X r) e  e  F  (x  X. extreme {f x |. f  F} r (e x))"
  by (auto intro!: pointwiseI extremeI elim!: extremeE)

lemma pointwise_extreme_bound:
  fixes r (infix "" 50)
  assumes F: "F  {f. f ` X  A}"
  shows "extreme_bound {f. f ` X  A} (pointwise X (⊑)) F s 
    (x  X. extreme_bound A (⊑) {f x |. f  F} (s x))" (is "?p  ?a")
proof (safe intro!: extreme_boundI pointwiseI)
  fix x
  assume s: ?p and xX: "x  X"
  { fix b
    assume b: "bound {f x |. f  F} (⊑) b" and bA: "b  A"
    have "pointwise X (⊑) s (s(x:=b))"
    proof (rule extreme_boundD(2)[OF s], safe intro!: pointwiseI)
      fix f y
      assume fF: "f  F" and yX: "y  X"
      show "f y  (s(x:=b)) y"
      proof (cases "x = y")
        case True
        with b fF show "?thesis" by auto
      next
        case False
        with s[THEN extreme_bound_imp_bound] fF yX show ?thesis by (auto dest: boundD)
      qed
    next
      fix y assume "y  X" with bA s show "(s(x := b)) y  A" by auto
    qed
    with xX show "s x  b" by (auto dest: pointwiseD)
  next
    fix f assume "f  F"
    from extreme_boundD(1)[OF s this] F xX
    show "f x  s x" by auto
  next
    show "s x  A" using s xX by auto
  }
next
  fix x
  assume s: ?a and xX: "x  X"
  { from s xX show "s x  A" by auto
  next
    fix b assume b: "bound F (pointwise X (⊑)) b" and bA: "b ` X  A"
    with xX have "bound {f x |. f  F} (⊑) (b x)" by (auto simp: pointwise_bound)
    with s[rule_format, OF xX] bA xX show "s x  b x" by auto
  next
    fix f assume "f  F"
    with s[rule_format, OF xX] show "f x  s x" by auto
  }
qed

lemma dual_pointwise_extreme_bound:
  "extreme_bound FA (pointwise X r)- F = extreme_bound FA (pointwise X r-) F"
  by (simp)

lemma pointwise_monotone_on:
  fixes less_eq (infix "" 50) and prec_eq (infix "" 50)
  shows "monotone_on I (≼) (pointwise A (⊑)) f 
   (a  A. monotone_on I (≼) (⊑) (λi. f i a))" (is "?l  ?r")
proof (safe intro!: monotone_onI pointwiseI)
  fix a i j assume aA: "a  A" and *: ?l "i  j" "i  I" "j  I"
  then
  show "f i a  f j a" by (auto dest: monotone_onD)
next
  fix a i j assume ?r and "a  A" and ij: "i  j" "i  I" "j  I"
  then have "monotone_on I (≼) (⊑) (λi. f i a)" by auto
  from monotone_onD[OF this]ij
  show "f i a  f j a" by auto
qed

lemmas pointwise_monotone = pointwise_monotone_on[of UNIV]

lemma (in reflexive) pointwise_reflexive: "reflexive {f. f ` I  A} (pointwise I (⊑))"
  apply unfold_locales by (auto intro!: pointwiseI simp: subsetD[OF _ imageI])

lemma (in irreflexive) pointwise_irreflexive:
  assumes I0: "I  {}" shows "irreflexive {f. f ` I  A} (pointwise I (⊏))"
proof (safe intro!: irreflexive.intro)
  fix f
  assume f: "f ` I  A" and ff: "pointwise I (⊏) f f"
  from I0 obtain i where i: "i  I" by auto
  with ff have "f i  f i" by auto
  with f i show False by auto
qed

lemma (in semiattractive) pointwise_semiattractive: "semiattractive {f. f ` I  A} (pointwise I (⊑))"
proof (unfold_locales, safe intro!: pointwiseI)
  fix f g h i
  assume fg: "pointwise I (⊑) f g" and gf: "pointwise I (⊑) g f" and gh: "pointwise I (⊑) g h"
    and [simp]: "i  I" and f: "f ` I  A" and g: "g ` I  A" and h: "h ` I  A"
  show "f i  h i"
  proof (rule attract)
    from fg show "f i  g i" by auto
    from gf show "g i  f i" by auto
    from gh show "g i  h i" by auto
  qed (insert f g h, auto simp: subsetD[OF _ imageI])
qed

lemma (in attractive) pointwise_attractive: "attractive {f. f ` I  A} (pointwise I (⊑))"
  apply (intro attractive.intro attractive_axioms.intro)
  using pointwise_semiattractive dual.pointwise_semiattractive by auto

text ‹Antisymmetry will not be preserved by pointwise extension over restricted domain.›
lemma (in antisymmetric) pointwise_antisymmetric:
  "antisymmetric {f. f ` I  A} (pointwise I (⊑))"
  oops

lemma (in transitive) pointwise_transitive: "transitive {f. f ` I  A} (pointwise I (⊑))"
proof (unfold_locales, safe intro!: pointwiseI)
  fix f g h i
  assume fg: "pointwise I (⊑) f g" and gh: "pointwise I (⊑) g h"
    and [simp]: "i  I" and f: "f ` I  A" and g: "g ` I  A" and h: "h ` I  A"
  from fg have "f i  g i" by auto
  also from gh have "g i  h i" by auto
  finally show "f i  h i" using f g h by (auto simp: subsetD[OF _ imageI])
qed

lemma (in quasi_ordered_set) pointwise_quasi_order:
  "quasi_ordered_set {f. f ` I  A} (pointwise I (⊑))"
  by (intro quasi_ordered_setI pointwise_transitive pointwise_reflexive)

lemma (in compatible_ordering) pointwise_compatible_ordering:
  assumes I0: "I  {}"
  shows "compatible_ordering {f. f ` I  A} (pointwise I (⊑)) (pointwise I (⊏))"
proof (intro compatible_ordering.intro compatible_ordering_axioms.intro pointwise_irreflexive[OF I0], safe intro!: pointwiseI)
  fix f g h i
  assume fg: "pointwise I (⊑) f g" and gh: "pointwise I (⊏) g h"
    and [simp]: "i  I" and f: "f ` I  A" and g: "g ` I  A" and h: "h ` I  A"
  from fg have "f i  g i" by auto
  also from gh have "g i  h i" by auto
  finally show "f i  h i" using f g h by (auto simp: subsetD[OF _ imageI])
next
  fix f g h i
  assume fg: "pointwise I (⊏) f g" and gh: "pointwise I (⊑) g h"
    and [simp]: "i  I" and f: "f ` I  A" and g: "g ` I  A" and h: "h ` I  A"
  from fg have "f i  g i" by auto
  also from gh have "g i  h i" by auto
  finally show "f i  h i" using f g h by (auto simp: subsetD[OF _ imageI])
next
  fix f g i
  assume fg: "pointwise I (⊏) f g"
    and [simp]: "i  I"
    and f: "f ` I  A" and g: "g ` I  A"
  from fg have "f i  g i" by auto
  with f g show "f i  g i" by (auto simp: subsetD[OF _ imageI] strict_implies_weak)
qed

subsection ‹Relating to Classes›

text ‹In Isabelle 2020, we should declare sublocales in class before declaring dual
sublocales, since otherwise facts would be prefixed by ``dual.dual.''›

context ord begin

abbreviation least where "least X  extreme X (λx y. y  x)"

abbreviation greatest where "greatest X  extreme X (≤)"

abbreviation supremum where "supremum X  least (Collect (bound X (≤)))"

abbreviation infimum where "infimum X  greatest (Collect (bound X (λx y. y  x)))"

lemma supremumI: "bound X (≤) s  (b. bound X (≤) b  s  b)  supremum X s"
  and infimumI: "bound X (≥) i  (b. bound X (≥) b  b  i)  infimum X i"
  by (auto intro!: extremeI)

lemma supremumE: "supremum X s 
    (bound X (≤) s  (b. bound X (≤) b  s  b)  thesis)  thesis"
  and infimumE: "infimum X i 
    (bound X (≥) i  (b. bound X (≥) b  b  i)  thesis)  thesis"
  by (auto)

lemma extreme_bound_supremum[simp]: "extreme_bound UNIV (≤) = supremum" by (auto intro!: ext)
lemma extreme_bound_infimum[simp]: "extreme_bound UNIV (≥) = infimum" by (auto intro!: ext)

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

lemma pointwise_UNIV_le[simp]: "pointwise UNIV (≤) = (≤)" by (intro ext, simp add: pointwise_def le_fun_def)
lemma pointwise_UNIV_ge[simp]: "pointwise UNIV (≥) = (≥)" by (intro ext, simp add: pointwise_def le_fun_def)

lemma fun_supremum_iff: "supremum F e  (x. supremum {f x |. f  F} (e x))"
  using pointwise_extreme_bound[of F UNIV UNIV "(≤)"] by simp

lemma fun_infimum_iff: "infimum F e  (x. infimum {f x |. f  F} (e x))"
  using pointwise_extreme_bound[of F UNIV UNIV "(≥)"] by simp


class reflorder = ord + assumes "reflexive_ordering UNIV (≤) (<)"
begin

sublocale order: reflexive_ordering UNIV
  rewrites "x. x  UNIV  True"
    and "X. X  UNIV  True"
    and "r. r  UNIV  r"
    and "P. True  P  P"
    and "Ball UNIV  All"
    and "Bex UNIV  Ex"
    and "sympartp (≤)-  sympartp (≤)"
    and "P1. (True  PROP P1)  PROP P1"
    and "P1. (True  P1)  Trueprop P1"
    and "P1 P2. (True  PROP P1  PROP P2)  (PROP P1  PROP P2)"
  using reflorder_axioms unfolding class.reflorder_def by (auto 0 4 simp:atomize_eq)

end

text ‹We should have imported locale-based facts in classes, e.g.:›
thm order.trans order.strict.trans order.refl order.irrefl order.asym order.extreme_bound_singleton

class attrorder = ord +
  assumes "reflexive_attractive_ordering UNIV (≤) (<)"
begin

text ‹We need to declare subclasses before sublocales in order to preserve facts for superclasses.›

subclass reflorder
proof-
  interpret reflexive_attractive_ordering UNIV
    using attrorder_axioms unfolding class.attrorder_def by auto
  show "class.reflorder (≤) (<)"..
qed

sublocale order: reflexive_attractive_ordering UNIV
  rewrites "x. x  UNIV  True"
    and "X. X  UNIV  True"
    and "r. r  UNIV  r"
    and "P. True  P  P"
    and "Ball UNIV  All"
    and "Bex UNIV  Ex"
    and "sympartp (≤)-  sympartp (≤)"
    and "P1. (True  PROP P1)  PROP P1"
    and "P1. (True  P1)  Trueprop P1"
    and "P1 P2. (True  PROP P1  PROP P2)  (PROP P1  PROP P2)"
  using attrorder_axioms unfolding class.attrorder_def
  by (auto simp:atomize_eq)

end

thm order.extreme_bound_quasi_const

class psorder = ord + assumes "pseudo_ordering UNIV (≤) (<)"
begin

subclass attrorder
proof-
  interpret pseudo_ordering UNIV
    using psorder_axioms unfolding class.psorder_def by auto
  show "class.attrorder (≤) (<)"..
qed

sublocale order: pseudo_ordering UNIV
  rewrites "x. x  UNIV  True"
    and "X. X  UNIV  True"
    and "r. r  UNIV  r"
    and "P. True  P  P"
    and "Ball UNIV  All"
    and "Bex UNIV  Ex"
    and "sympartp (≤)-  sympartp (≤)"
    and "P1. (True  PROP P1)  PROP P1"
    and "P1. (True  P1)  Trueprop P1"
    and "P1 P2. (True  PROP P1  PROP P2)  (PROP P1  PROP P2)"
  using psorder_axioms unfolding class.psorder_def by (auto simp:atomize_eq)

end

class qorder = ord + assumes "quasi_ordering UNIV (≤) (<)"
begin

subclass attrorder
proof-
  interpret quasi_ordering UNIV
    using qorder_axioms unfolding class.qorder_def by auto
  show "class.attrorder (≤) (<)"..
qed

sublocale order: quasi_ordering UNIV
  rewrites "x. x  UNIV  True"
    and "X. X  UNIV  True"
    and "r. r  UNIV  r"
    and "P. True  P  P"
    and "Ball UNIV  All"
    and "Bex UNIV  Ex"
    and "sympartp (≤)-  sympartp (≤)"
    and "P1. (True  PROP P1)  PROP P1"
    and "P1. (True  P1)  Trueprop P1"
    and "P1 P2. (True  PROP P1  PROP P2)  (PROP P1  PROP P2)"
  using qorder_axioms unfolding class.qorder_def by (auto simp:atomize_eq)

lemmas [intro!] = order.quasi_ordered_subset

end

class porder = ord + assumes "partial_ordering UNIV (≤) (<)"
begin

interpretation partial_ordering UNIV
  using porder_axioms unfolding class.porder_def by auto

subclass psorder..

subclass qorder..

sublocale order: partial_ordering UNIV
  rewrites "x. x  UNIV  True"
    and "X. X  UNIV  True"
    and "r. r  UNIV  r"
    and "P. True  P  P"
    and "Ball UNIV  All"
    and "Bex UNIV  Ex"
    and "sympartp (≤)-  sympartp (≤)"
    and "P1. (True  PROP P1)  PROP P1"
    and "P1. (True  P1)  Trueprop P1"
    and "P1 P2. (True  PROP P1  PROP P2)  (PROP P1  PROP P2)"
  apply unfold_locales by (auto simp:atomize_eq)

end

class linqorder = ord + assumes "total_quasi_ordering UNIV (≤) (<)"
begin

interpretation total_quasi_ordering UNIV
  using linqorder_axioms unfolding class.linqorder_def by auto

subclass qorder..

sublocale order: total_quasi_ordering UNIV
  rewrites "x. x  UNIV  True"
    and "X. X  UNIV  True"
    and "r. r  UNIV  r"
    and "P. True  P  P"
    and "Ball UNIV  All"
    and "Bex UNIV  Ex"
    and "sympartp (≤)-  sympartp (≤)"
    and "P1. (True  PROP P1)  PROP P1"
    and "P1. (True  P1)  Trueprop P1"
    and "P1 P2. (True  PROP P1  PROP P2)  (PROP P1  PROP P2)"
    using linqorder_axioms unfolding class.linqorder_def
    by (auto simp:atomize_eq)

lemmas asympartp_le = order.not_iff_asym[symmetric, abs_def]

end


text ‹Isabelle/HOL's @{class preorder} belongs to @{class qorder}, but not vice versa.›

context preorder begin

text ‹The relation @{term "(<)"} is defined as the antisymmetric part of @{term "(≤)"}.›
lemma [simp]:
  shows asympartp_le: "asympartp (≤) = (<)"
    and asympartp_ge: "asympartp (≥) = (>)"
  by (intro ext, auto simp: asympartp_def less_le_not_le)

interpretation strict_quasi_ordering UNIV "(≤)" "(<)"
  apply unfold_locales
  using order_refl apply assumption
  using order_trans apply assumption
  using less_le_not_le apply assumption
  done

subclass qorder..

sublocale order: strict_quasi_ordering UNIV
  rewrites "x. x  UNIV  True"
    and "X. X  UNIV  True"
    and "r. r  UNIV  r"
    and "P. True  P  P"
    and "Ball UNIV  All"
    and "Bex UNIV  Ex"
    and "sympartp (≤)-  sympartp (≤)"
    and "P1. (True  PROP P1)  PROP P1"
    and "P1. (True  P1)  Trueprop P1"
    and "P1 P2. (True  PROP P1  PROP P2)  (PROP P1  PROP P2)"
  apply unfold_locales
    by (auto simp:atomize_eq)

end

context order begin

interpretation strict_partial_ordering UNIV "(≤)" "(<)"
  apply unfold_locales
  using order_antisym by assumption

subclass porder..

sublocale order: strict_partial_ordering UNIV
  rewrites "x. x  UNIV  True"
    and "X. X  UNIV  True"
    and "r. r  UNIV  r"
    and "P. True  P  P"
    and "Ball UNIV  All"
    and "Bex UNIV  Ex"
    and "sympartp (≤)-  sympartp (≤)"
    and "P1. (True  PROP P1)  PROP P1"
    and "P1. (True  P1)  Trueprop P1"
    and "P1 P2. (True  PROP P1  PROP P2)  (PROP P1  PROP P2)"
  apply unfold_locales
    by (auto simp:atomize_eq)

end

text ‹Isabelle/HOL's @{class linorder} is equivalent to our locale @{locale total_ordering}.›

context linorder begin

subclass linqorder apply unfold_locales by auto

sublocale order: total_ordering UNIV
  rewrites "x. x  UNIV  True"
    and "X. X  UNIV  True"
    and "r. r  UNIV  r"
    and "P. True  P  P"
    and "Ball UNIV  All"
    and "Bex UNIV  Ex"
    and "sympartp (≤)-  sympartp (≤)"
    and "P1. (True  PROP P1)  PROP P1"
    and "P1. (True  P1)  Trueprop P1"
    and "P1 P2. (True  PROP P1  PROP P2)  (PROP P1  PROP P2)"
  apply unfold_locales by (auto simp:atomize_eq)

end

text ‹Tests: facts should be available in the most general classes.›

thm order.strict.trans[where 'a="'a::reflorder"]
thm order.extreme_bound_quasi_const[where 'a="'a::attrorder"]
thm order.extreme_bound_singleton_eq[where 'a="'a::psorder"]
thm order.trans[where 'a="'a::qorder"]
thm order.comparable_cases[where 'a="'a::linqorder"]
thm order.cases[where 'a="'a::linorder"]

subsection ‹Declaring Duals›

sublocale reflexive  sym: reflexive A "sympartp (⊑)"
  rewrites "sympartp (⊑)-  sympartp (⊑)"
    and "r. sympartp (sympartp r)  sympartp r"
    and "r. sympartp r  A  sympartp (r  A)"
  by (auto 0 4 simp:atomize_eq)

sublocale quasi_ordered_set  sym: quasi_ordered_set A "sympartp (⊑)"
  rewrites "sympartp (⊑)- = sympartp (⊑)"
    and "sympartp (sympartp (⊑)) = sympartp (⊑)"
   apply unfold_locales by (auto 0 4 dest: trans)
  
text ‹At this point, we declare dual as sublocales.
In the following, ``rewrites'' eventually cleans up redundant facts.›

sublocale reflexive  dual: reflexive A "(⊑)-"
  rewrites "sympartp (⊑)-  sympartp (⊑)"
    and "r. sympartp (r  A)  sympartp r  A"
    and "(⊑)-  A  ((⊑)  A)-"
  by (auto simp: atomize_eq)

context attractive begin

interpretation less_eq_symmetrize.

sublocale dual: attractive A "(⊒)"
  rewrites "sympartp (⊒) = (∼)"
    and "equivpartp (⊒)  ()"
    and "r. sympartp (r  A)  sympartp r  A"
    and "r. sympartp (sympartp r)  sympartp r"
    and "(⊑)-  A  ((⊑)  A)-"
  apply unfold_locales by (auto intro!: ext dest: attract dual.attract simp: atomize_eq)

end

context irreflexive begin

sublocale dual: irreflexive A "(⊏)-"
  rewrites "(⊏)-  A  ((⊏)  A)-"
  apply unfold_locales by (auto dest: irrefl simp: atomize_eq)

end

sublocale transitive  dual: transitive A "(⊑)-"
  rewrites "(⊑)-  A  ((⊑)  A)-"
    and "sympartp (⊑)- = sympartp (⊑)"
    and "asympartp (⊑)- = (asympartp (⊑))-"
  apply unfold_locales by (auto dest: trans simp: atomize_eq intro!:ext)

sublocale antisymmetric  dual: antisymmetric A "(⊑)-"
  rewrites "(⊑)-  A  ((⊑)  A)-"
    and "sympartp (⊑)- = sympartp (⊑)"
  by (auto dest: antisym simp: atomize_eq)

context antisymmetric begin

lemma extreme_bound_unique:
  "extreme_bound A (⊑) X x  extreme_bound A (⊑) X y  x = y"
  apply (unfold extreme_bound_def)
  apply (rule dual.extreme_unique) by auto

lemma ex_extreme_bound_iff_ex1:
  "Ex (extreme_bound A (⊑) X)  Ex1 (extreme_bound A (⊑) X)"
  apply (unfold extreme_bound_def)
  apply (rule dual.ex_extreme_iff_ex1) by auto

lemma ex_extreme_bound_iff_the:
   "Ex (extreme_bound A (⊑) X)  extreme_bound A (⊑) X (The (extreme_bound A (⊑) X))"
  apply (rule iffI)
  apply (rule theI')
  using extreme_bound_unique by auto

end

sublocale semiconnex  dual: semiconnex A "(⊏)-"
  rewrites "sympartp (⊏)- = sympartp (⊏)"
  using semiconnex by auto

sublocale connex  dual: connex A "(⊑)-"
  rewrites "sympartp (⊑)- = sympartp (⊑)"
  by (auto intro!: chainI dest:comparable)

sublocale semiconnex_irreflexive  dual: semiconnex_irreflexive A "(⊏)-"
  rewrites "sympartp (⊏)- = sympartp (⊏)"
  by unfold_locales auto

sublocale pseudo_ordered_set  dual: pseudo_ordered_set A "(⊑)-"
  rewrites "sympartp (⊑)- = sympartp (⊑)"
  by unfold_locales (auto 0 4)

sublocale quasi_ordered_set  dual: quasi_ordered_set A "(⊑)-"
  rewrites "sympartp (⊑)- = sympartp (⊑)"
  by unfold_locales auto

sublocale partially_ordered_set  dual: partially_ordered_set A "(⊑)-"
  rewrites "sympartp (⊑)- = sympartp (⊑)"
  by unfold_locales (auto 0 4)

sublocale total_pseudo_ordered_set  dual: total_pseudo_ordered_set A "(⊑)-"
  rewrites "sympartp (⊑)- = sympartp (⊑)"
  by unfold_locales (auto 0 4)

sublocale total_quasi_ordered_set  dual: total_quasi_ordered_set A "(⊑)-"
  rewrites "sympartp (⊑)- = sympartp (⊑)"
  by unfold_locales auto

sublocale compatible_ordering  dual: compatible_ordering A "(⊑)-" "(⊏)-"
  rewrites "sympartp (⊑)- = sympartp (⊑)"
  apply unfold_locales
  by (auto dest: strict_implies_weak strict_weak_trans weak_strict_trans)

lemmas(in qorder) [intro!] = order.dual.quasi_ordered_subset

sublocale reflexive_ordering  dual: reflexive_ordering A "(⊑)-" "(⊏)-"
  rewrites "sympartp (⊑)- = sympartp (⊑)"
  by unfold_locales auto

sublocale reflexive_attractive_ordering  dual: reflexive_attractive_ordering A "(⊑)-" "(⊏)-"
  rewrites "sympartp (⊑)- = sympartp (⊑)"
  by unfold_locales auto

sublocale pseudo_ordering  dual: pseudo_ordering A "(⊑)-" "(⊏)-"
  rewrites "sympartp (⊑)- = sympartp (⊑)"
  by unfold_locales auto

sublocale quasi_ordering  dual: quasi_ordering A "(⊑)-" "(⊏)-"
  rewrites "sympartp (⊑)- = sympartp (⊑)"
  by unfold_locales auto

sublocale partial_ordering  dual: partial_ordering A "(⊑)-" "(⊏)-"
  rewrites "sympartp (⊑)- = sympartp (⊑)"
  by unfold_locales auto

sublocale total_quasi_ordering  dual: total_quasi_ordering A "(⊑)-" "(⊏)-"
  rewrites "sympartp (⊑)- = sympartp (⊑)"
  by unfold_locales auto

sublocale total_ordering  dual: total_ordering A "(⊑)-" "(⊏)-"
  rewrites "sympartp (⊑)- = sympartp (⊑)"
  by unfold_locales auto

sublocale strict_quasi_ordering  dual: strict_quasi_ordering A "(⊑)-" "(⊏)-"
  rewrites "sympartp (⊑)- = sympartp (⊑)"
  by unfold_locales (auto simp: strict_iff)

sublocale strict_partial_ordering  dual: strict_partial_ordering A "(⊑)-" "(⊏)-"
  rewrites "sympartp (⊑)- = sympartp (⊑)"
  by unfold_locales auto

sublocale total_ordering  dual: total_ordering A "(⊑)-" "(⊏)-"
  rewrites "sympartp (⊑)- = sympartp (⊑)"
  by unfold_locales auto

lemma(in antisymmetric) monotone_extreme_imp_extreme_bound_iff:
  fixes ir (infix "" 50)
  assumes "f ` C  A" and "monotone_on C (≼) (⊑) f" and i: "extreme C (≼) i"
  shows "extreme_bound A (⊑) (f ` C) x  f i = x"
  using dual.extreme_unique monotone_extreme_extreme_boundI[OF assms]
  by (auto simp: extreme_bound_def)

subsection ‹Instantiations›

text ‹Finally, we instantiate our classes for sanity check.›

instance nat :: linorder ..

text ‹Pointwise ordering of functions are compatible only if the weak part is transitive.›

instance "fun" :: (type,qorder) reflorder
proof (intro_classes, unfold_locales)
  note [simp] = le_fun_def less_fun_def
  fix f g h :: "'a  'b"
  { assume fg: "f  g" and gh: "g < h"
    show "f < h"
    proof (unfold less_fun_def, intro conjI le_funI notI)
      from fg have "f x  g x" for x by auto
      also from gh have "g x  h x" for x by auto
      finally (order.trans) show "f x  h x" for x.
      assume hf: "h  f"
      then have "h x  f x" for x by auto
      also from fg have "f x  g x" for x by auto
      finally have "h  g" by auto
      with gh show False by auto
    qed
  }
  { assume fg: "f < g" and gh: "g  h"
    show "f < h"
    proof (unfold less_fun_def, intro conjI le_funI notI)
      from fg have "f x  g x" for x by auto
      also from gh have "g x  h x" for x by auto
      finally show "f x  h x" for x.
      from gh have "g x  h x" for x by auto
      also assume hf: "h  f"
      then have "h x  f x" for x by auto
      finally have "g  f" by auto
      with fg show False by auto
    qed
  }
  show "f < g  f  g" by auto
  show "¬f < f" by auto
  show "f  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  'b" and x :: 'a
  assume fg: "f  g" and gf: "g  f"
  then have "f x  g x" and "g x  f x" by (auto elim: le_funE)
  from order.antisym[OF this] show "f x = g x" by auto
qed

end