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{_ /|./ (_/ ∈ _)})›)
syntax_consts
  "_range" ⇌ range and
  "_image" ⇌ image
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 simp: fun_eq_iff)

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 simp: sympartp_def)

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

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

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 simp: fun_eq_iff 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 simp: fun_eq_iff)

lemma equivpartp_dual: "equivpartp r⇧- = equivpartp r"
  by (auto simp: fun_eq_iff 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 simp: fun_eq_iff)

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 ⟷ (∀b∈B. ∃a∈A. 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 (⊑) (⋃i∈I. {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: "∀x∈X. ∃y∈Y. 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)

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

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 simp: fun_eq_iff 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 dest: trans simp: fun_eq_iff 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 fun_eq_iff)

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 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 (X∪Y) (⊑)"
  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 {x∈A. 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 (intro extreme_boundI, auto 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 "∃z∈A. 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 simp: fun_eq_iff intro!: pointwiseI)

lemma dual_pointwise[simp]: "(pointwise I r)⇧- = pointwise I r⇧-"
  by (auto simp: fun_eq_iff intro!: 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 (I∪J) r = pointwise I r ⊓ pointwise J r"
  by (auto simp: fun_eq_iff intro!: 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 simp: fun_eq_iff)
lemma extreme_bound_infimum[simp]: "extreme_bound UNIV (≥) = infimum" by (auto simp: fun_eq_iff)

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 The_least_eq_Least: "The (least X) = Least (λx. x ∈ X)"
  by (simp add: Least_eq_The_least)

lemma least_imp_infimum: assumes "least X x" shows "infimum X x"
  using extreme_imp_extreme_bound[OF assms, of UNIV] by simp

lemma least_LeastI_ex1:
  assumes ex1: "∃!x. least {x. P x} x"
  shows "least {x. P x} (LEAST x. P x)"
  using theI'[OF ex1] by (simp add: Least_eq_The_least)

end (* TODO: Greatest should also be defined in ord. *)
context order begin

lemma Greatest_eq_The_greatest: "Greatest P = The (greatest {x. P x})"
  by (auto simp: Greatest_def extreme_def[unfolded atomize_eq, THEN ext])

lemma The_greatest_eq_Greatest: "The (greatest X) = Greatest (λx. x ∈ X)"
  by (simp add: Greatest_eq_The_greatest)

lemma greatest_imp_supremum: assumes "greatest X x" shows "supremum X x"
  using extreme_imp_extreme_bound[OF assms, of UNIV] by simp

lemma greatest_GreatestI_ex1:
  assumes ex1: "∃!x. greatest {x. P x} x"
  shows "greatest {x. P x} (GREATEST x. P x)"
  using theI'[OF ex1] by (simp add: Greatest_eq_The_greatest)

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

(* TODO: move to psorder. *)
context order begin

lemma ex_greatest_iff_Greatest:
  "Ex (greatest X) ⟷ greatest X (Greatest (λx. x ∈ X))"
  using order.ex_extreme_iff_the[of X]
  by (simp add: The_greatest_eq_Greatest)

lemma greatest_imp_supremum_Greatest:
  "greatest X x ⟹ supremum X (Greatest (λx. x ∈ X))"
  using ex_greatest_iff_Greatest[THEN iffD1, THEN greatest_imp_supremum]
  by auto

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 dest: attract dual.attract simp: fun_eq_iff 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 fun_eq_iff)

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

lemma (in psorder) least_Least:
  fixes X :: "'a set"
  shows "Ex (least X) ⟷ least X (LEAST x. x ∈ X)"
  using order.dual.ex_extreme_iff_the[of X, unfolded The_least_eq_Least].

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