Theory Set_Simple_Orders

(* Title: Examples/TTS_Foundations/Orders/Set_Simple_Orders.thy
   Author: Mihails Milehins
   Copyright 2021 (C) Mihails Milehins
*)
section‹Abstract orders on explicit sets›
theory Set_Simple_Orders
  imports 
    Type_Simple_Orders 
    "../Foundations/FNDS_Set_Ext"
begin



subsection‹Background›


text‹
Some of the results presented in this section were ported 
(with amendments and additions) from the theories text‹Orderings› 
and text‹Set_Interval› in the main library of Isabelle/HOL.
›



subsection‹Order operations›

locale ord_ow =
  fixes U :: "'a set" and le ls :: "['a, 'a] ⇒ bool" 
begin

tts_register_sbts le | U
proof-
  assume "Domainp AB = (λx. x ∈ U)" "bi_unique AB" "right_total AB" 
  from tts_AA_eq_transfer[OF this] show ?thesis by auto
qed

tts_register_sbts ls | U
proof-
  assume "Domainp AB = (λx. x ∈ U)" "bi_unique AB" "right_total AB" 
  from tts_AA_eq_transfer[OF this] show ?thesis by auto
qed

end

locale ord_syntax_ow = ord_ow U le ls
  for U :: "'a set" and le ls :: "['a, 'a] ⇒ bool" 
begin

notation
  le ("'(≤a')") and
  le (infix "≤a" 50) and
  ls ("'(<a')") and
  ls (infix "<a" 50)

abbreviation (input) ge (infix "≥a" 50)
  where "x ≥a y ≡ y ≤a x"
abbreviation (input) gt (infix ">a" 50)
  where "x >a y ≡ y <a x"

notation
  ge ("'(≥a')") and
  ge (infix "≥a" 50) and
  gt ("'(>a')") and
  gt (infix ">a" 50)

abbreviation Least where "Least ≡ Type_Simple_Orders.Least U (≤a)"
abbreviation Greatest where "Greatest ≡ Type_Simple_Orders.Least U (≥a)"

abbreviation min where "min ≡ Type_Simple_Orders.min (≤a)"
abbreviation max where "max ≡ Type_Simple_Orders.min (≥a)"

abbreviation lessThan (‹{..<a_}›) where "{..<au} ≡ on U with (<a) : {..⊏u}"
abbreviation atMost (‹{..≤a_}›) where "{..≤au} ≡ on U with (≤a) : {..⊏u}"
abbreviation greaterThan (‹{_<a..}›) where "{l<a..} ≡ on U with (>a) : {..⊏l}"
abbreviation atLeast (‹{_≤a..}›) where "{l≤a..} ≡ on U with (≥a) : {..⊏l}"
abbreviation greaterThanLessThan (‹{_<a..<a_}›) 
  where "{l<a..<au} ≡ on U with (<a) (<a) : {l⊏..⊏u}"
abbreviation atLeastLessThan (‹{_≤a..<a_}›) 
  where "{l≤a..<au} ≡ on U with (≤a) (<a) : {l⊏..⊏u}"
abbreviation greaterThanAtMost (‹{_<a..≤a_}›) 
  where "{l<a..≤au} ≡ on U with (<a) (≤a) : {l⊏..⊏u}"
abbreviation atLeastAtMost (‹{_≤a..≤a_}›) 
  where "{l≤a..≤au} ≡ on U with (≤a) (≤a) : {l⊏..⊏u}"
abbreviation lessThanGreaterThan (‹{_>a..>a_}›) 
  where "{l>a..>au} ≡ on U with (>a) (>a) : {l⊏..⊏u}"
abbreviation lessThanAtLeast (‹{_≥a..>a_}›) 
  where "{l≥a..>au} ≡ on U with (≥a) (>a) : {l⊏..⊏u}"
abbreviation atMostGreaterThan (‹{_>a..≥a_}›) 
  where "{l>a..≥au} ≡ on U with (>a) (≥a) : {l⊏..⊏u}"
abbreviation atMostAtLeast (‹{_≥a..≥a_}›) 
  where "{l≥a..≥au} ≡ on U with (≥a) (≥a) : {l⊏..⊏u}"

abbreviation bdd_above where "bdd_above ≡ bdd U (≤a)"
abbreviation bdd_below where "bdd_below ≡ bdd U (≥a)"

end

locale ord_dual_ow = ord_syntax_ow U le ls
  for U :: "'a set" and le ls :: "['a, 'a] ⇒ bool"
begin

sublocale dual: ord_ow U ge gt .

end

locale ord_pair_ow = orda: ord_ow Ua lea lsa + ordb: ord_ow Ub leb lsb
  for Ua :: "'a set" and lea lsa and Ub :: "'b set" and leb lsb
begin

sublocale rev: ord_pair_ow Ub leb lsb Ua lea lsa .

end

locale ord_pair_syntax_ow = ord_pair_ow Ua lea lsa Ub leb lsb
  for Ua :: "'a set" and lea lsa and Ub :: "'b set" and leb lsb
begin

sublocale orda: ord_syntax_ow Ua lea lsa + ordb: ord_syntax_ow Ub leb lsb .

notation lea (‹'(≤a')›)
  and lea (infix ‹≤a› 50) 
  and lsa (‹'(<a')›) 
  and lsa (infix ‹<a› 50)
  and leb (‹'(≤b')›)
  and leb (infix ‹≤b› 50) 
  and lsb (‹'(<b')›) 
  and lsb (infix ‹<b› 50)

notation orda.ge (‹'(≥a')›) 
  and orda.ge (infix ‹≥a› 50) 
  and orda.gt (‹'(>a')›) 
  and orda.gt (infix ‹>a› 50)
  and ordb.ge (‹'(≥b')›) 
  and ordb.ge (infix ‹≥b› 50) 
  and ordb.gt (‹'(>b')›) 
  and ordb.gt (infix ‹>b› 50)

abbreviation monoab 
  where "monoab ≡ Type_Simple_Orders.mono Ua (≤a) (≤b)"
abbreviation monoba 
  where "monoba ≡ Type_Simple_Orders.mono Ub (≤b) (≤a)"
abbreviation antimonoab 
  where "antimonoab ≡ Type_Simple_Orders.mono Ua (≤a) (≥b)"
abbreviation antimonoba 
  where "antimonoba ≡ Type_Simple_Orders.mono Ub (≤b) (≥a)"
abbreviation strict_monoab 
  where "strict_monoab ≡ Type_Simple_Orders.mono Ua (<a) (<b)"
abbreviation strict_monoba 
  where "strict_monoba ≡ Type_Simple_Orders.mono Ub (<b) (<a)"
abbreviation strict_antimonoab 
  where "strict_antimonoab ≡ Type_Simple_Orders.mono Ua (<a) (>b)"
abbreviation strict_antimonoba 
  where "strict_antimonoba ≡ Type_Simple_Orders.mono Ub (<b) (>a)"

notation orda.lessThan (‹{..<a_}›) 
  and orda.atMost (‹{..≤a_}›) 
  and orda.greaterThan (‹{_<a..}›) 
  and orda.atLeast (‹{_≤a..}›) 
  and orda.greaterThanLessThan (‹{_<a..<a_}›) 
  and orda.atLeastLessThan (‹{_≤a..<a_}›) 
  and orda.greaterThanAtMost (‹{_<a..≤a_}›) 
  and orda.atLeastAtMost (‹{_≤a..≤a_}›) 
  and orda.lessThanGreaterThan (‹{_>a..>a_}›)
  and orda.lessThanAtLeast (‹{_≥a..>a_}›) 
  and orda.atMostGreaterThan (‹{_>a..≥a_}›) 
  and orda.atMostAtLeast (‹{_≥a..≥a_}›) 
  and ordb.lessThan (‹{..<b_}›) 
  and ordb.atMost (‹{..≤b_}›) 
  and ordb.greaterThan (‹{_<b..}›) 
  and ordb.atLeast (‹{_≤b..}›) 
  and ordb.greaterThanLessThan (‹{_<b..<b_}›) 
  and ordb.atLeastLessThan (‹{_≤b..<b_}›) 
  and ordb.greaterThanAtMost (‹{_<b..≤b_}›) 
  and ordb.atLeastAtMost (‹{_≤b..≤b_}›)
  and ordb.lessThanGreaterThan (‹{_>b..>b_}›)
  and ordb.lessThanAtLeast (‹{_≥b..>b_}›) 
  and ordb.atMostGreaterThan (‹{_>b..≥b_}›) 
  and ordb.atMostAtLeast (‹{_≥b..≥b_}›)

end

locale ord_pair_dual_ow = ord_pair_syntax_ow Ua lea lsa Ub leb lsb
  for Ua :: "'a set" and lea lsa and Ub :: "'b set" and leb lsb

context ord_pair_dual_ow
begin

sublocale ord_dual: ord_pair_ow Ua ‹(≤a)› ‹(<a)› Ub ‹(≥b)› ‹(>b)› .
sublocale dual_ord: ord_pair_ow Ua ‹(≥a)› ‹(>a)› Ub ‹(≤b)› ‹(<b)› .
sublocale dual_dual: ord_pair_ow Ua ‹(≥a)› ‹(>a)› Ub ‹(≥b)› ‹(>b)› .

end


subsubsection‹Relativization›

context ord_ow
begin

interpretation ord_syntax_ow .

tts_context
  tts: (?'a to U)
  sbterms: (‹?ls::?'a ⇒ ?'a ⇒ bool› to ls)
  rewriting ctr_simps
  eliminating through auto
begin

tts_lemma lessThan_iff:
  assumes "i ∈ U" and "k ∈ U"
  shows "(i ∈ {..<ak}) = (i <a k)"
    is ord.lessThan_iff.
    
tts_lemma greaterThanLessThan_iff:
  assumes "i ∈ U" and "l ∈ U" and "u ∈ U"
  shows "(i ∈ {l<a..<au}) = (i <a u ∧ l <a i)"
  is ord.greaterThanLessThan_iff.
    
tts_lemma greaterThanLessThan_eq:
  assumes "a ∈ U" and "b ∈ U"
  shows "{a<a..<ab} = {a<a..} ∩ {..<ab}"
    is ord.greaterThanLessThan_eq.

end

tts_context
  tts: (?'a to U)
  sbterms: (‹?le::?'a ⇒ ?'a ⇒ bool› to le)
  rewriting ctr_simps
  eliminating through auto
begin

tts_lemma min_absorb1:
  assumes "x ∈ U" and "y ∈ U" and "x ≤a y"
  shows "min x y = x"
  is ord.min_absorb1.
    
tts_lemma atLeast_iff:
  assumes "i ∈ U" and "k ∈ U"
  shows "(i ∈ {k≤a..}) = (k ≤a i)"
  is ord.atLeast_iff.

tts_lemma atLeastAtMost_iff:
  assumes "i ∈ U" and "l ∈ U" and "u ∈ U"
  shows "(i ∈ {l≤a..≤au}) = (i ≤a u ∧ l ≤a i)"
  is ord.atLeastAtMost_iff.

end

tts_context
  tts: (?'a to U)
  sbterms: (‹?le::?'a ⇒ ?'a ⇒ bool› to le)
    and (‹?ls::?'a ⇒ ?'a ⇒ bool› to ls)
   rewriting ctr_simps
 eliminating through auto
begin

tts_lemma atLeastLessThan_iff:
  assumes "i ∈ U" and "l ∈ U" and "u ∈ U"
  shows "(i ∈ {l≤a..<au}) = (l ≤a i ∧ i <a u)"
    is ord.atLeastLessThan_iff.
    
tts_lemma greaterThanAtMost_iff:
  assumes "i ∈ U" and "l ∈ U" and "u ∈ U"
  shows "(i ∈ {l<a..≤au}) = (i ≤a u ∧ l <a i)"
  is ord.greaterThanAtMost_iff.

end

end

context ord_pair_ow
begin

interpretation ord_pair_syntax_ow .

tts_context
  tts: (?'a to Ua) and (?'b to Ub)
  sbterms: (‹?lea::?'a⇒?'a⇒bool› to lea) and (‹?leb::?'b⇒?'b⇒bool› to leb)
  rewriting ctr_simps
  eliminating through (simp add: Type_Simple_Orders.mono_def)
begin

tts_lemma monoD:
  assumes "x ∈ Ua" and "y ∈ Ua" and "monoab f" and "x ≤a y"
  shows "f x ≤b f y"
  is ord_pair.monoD.
    
tts_lemma monoI:
  assumes "⋀x y. ⟦x ∈ Ua; y ∈ Ua; x ≤a y⟧ ⟹ f x ≤b f y"
  shows "monoab f"
    is ord_pair.monoI.
    
tts_lemma monoE:
  assumes "x ∈ Ua"
    and "y ∈ Ua"
    and "monoab f"
    and "x ≤a y"
    and "f x ≤b f y ⟹ thesis"
  shows thesis
    is ord_pair.monoE.

end

tts_context
  tts: (?'a to Ua) and (?'b to Ub)
  sbterms: (‹?lsa::?'a⇒?'a⇒bool› to lea) and (‹?lsb::?'b⇒?'b⇒bool› to leb)
  rewriting ctr_simps
  eliminating through (simp add: Type_Simple_Orders.mono_def)
begin

tts_lemma strict_monoD:
  assumes "x ∈ Ua"
    and "y ∈ Ua"
    and "monoab f"
    and "x ≤a y"
  shows "f x ≤b f y"
    is ord_pair.strict_monoD.
    
tts_lemma strict_monoI:
  assumes "⋀x y. ⟦x ∈ Ua; y ∈ Ua; x ≤a y⟧ ⟹ f x ≤b f y"
  shows "monoab f"
    is ord_pair.strict_monoI.
    
tts_lemma strict_monoE:
  assumes "x ∈ Ua"
    and "y ∈ Ua"
    and "monoab f"
    and "x ≤a y"
    and "f x ≤b f y ⟹ thesis"
  shows thesis
    is ord_pair.strict_monoE.

end

end



subsection‹Preorders›


subsubsection‹Definitions and common properties›

locale preorder_ow = ord_ow U le ls 
  for U :: "'a set" and le ls +
  assumes less_le_not_le: "⟦ x ∈ U; y ∈ U ⟧ ⟹ ls x y ⟷ le x y ∧ ¬ (le y x)"
    and order_refl[iff]: "x ∈ U ⟹ le x x"
    and order_trans: "⟦ x ∈ U; y ∈ U; z ∈ U; le x y; le y z ⟧ ⟹ le x z"

locale preorder_dual_ow = preorder_ow U le ls for U :: "'a set" and le ls
begin

sublocale ord_dual_ow .

sublocale dual: preorder_ow U ge gt 
  by standard (auto simp: less_le_not_le intro: order_trans)

end

locale ord_preorder_ow = 
  ord_pair_ow Ua lea lsa Ub leb lsb + ordb: preorder_ow Ub leb lsb 
  for Ua :: "'a set" and lea lsa and Ub :: "'b set" and leb lsb

locale ord_preorder_dual_ow = ord_preorder_ow Ua lea lsa Ub leb lsb
  for Ua :: "'a set" and lea lsa and Ub :: "'b set" and leb lsb
begin

sublocale ord_pair_dual_ow .
sublocale ord_dual: ord_preorder_ow Ua ‹(≤a)› ‹(<a)› Ub ‹(≥b)› ‹(>b)›
  by unfold_locales (auto simp: ordb.less_le_not_le intro: ordb.order_trans)
sublocale dual_ord: ord_preorder_ow Ua ‹(≥a)› ‹(>a)› Ub ‹(≤b)› ‹(<b)› 
  by (rule ord_preorder_ow_axioms)
sublocale dual_dual: ord_preorder_ow Ua ‹(≥a)› ‹(>a)› Ub ‹(≥b)› ‹(>b)›
  by (rule ord_dual.ord_preorder_ow_axioms)

end

locale preorder_pair_ow = 
  ord_preorder_ow Ua lea lsa Ub leb lsb + orda: preorder_ow Ua lea lsa
  for Ua :: "'a set" and lea lsa and Ub :: "'b set" and leb lsb
begin

sublocale rev: preorder_pair_ow Ub leb lsb Ua lea lsa ..

end

locale preorder_pair_dual_ow = preorder_pair_ow Ua lea lsa Ub leb lsb
  for Ua :: "'a set" and lea lsa and Ub :: "'b set" and leb lsb
begin

sublocale ord_preorder_dual_ow ..
sublocale ord_dual: preorder_pair_ow Ua ‹(≤a)› ‹(<a)› Ub ‹(≥b)› ‹(>b)› ..
sublocale dual_ord: preorder_pair_ow Ua ‹(≥a)› ‹(>a)› Ub ‹(≤b)› ‹(<b)› 
  by unfold_locales (auto intro: orda.order_trans simp: orda.less_le_not_le)
sublocale dual_dual: preorder_pair_ow Ua ‹(≥a)› ‹(>a)› Ub ‹(≥b)› ‹(>b)› ..

end


subsubsection‹Transfer rules›

lemma preorder_ow[ud_with]: "preorder = preorder_ow UNIV"
  unfolding preorder_def preorder_ow_def by simp

lemma ord_preorder_ow[ud_with]: "ord_preorder = ord_preorder_ow UNIV"
  unfolding ord_preorder_def ord_preorder_ow_def ud_with by simp

lemma preorder_pair_ow[ud_with]: 
  "preorder_pair = 
    (λlea lsa leb lsb. preorder_pair_ow UNIV lea lsa UNIV leb lsb)"
  unfolding preorder_pair_def preorder_pair_ow_def ud_with by simp

context
  includes lifting_syntax
begin

lemma preorder_ow_transfer[transfer_rule]:
  assumes [transfer_rule]: "right_total A"
  shows 
    "(rel_set A ===> (A ===> A ===> (=)) ===> (A ===> A ===> (=)) ===> (=)) 
      preorder_ow preorder_ow"
  by (ow_locale_transfer locale_defs: preorder_ow_def)

lemma ord_preorder_ow_transfer[transfer_rule]:
  assumes [transfer_rule]: "right_total A"
  shows 
    "(rel_set A ===> (A ===> A ===> (=)) ===> (A ===> A ===> (=)) ===> (=)) 
      ord_preorder_ow ord_preorder_ow"
  by (ow_locale_transfer locale_defs: ord_preorder_ow_def)

lemma preorder_pair_ow_transfer[transfer_rule]:
  assumes [transfer_rule]: "right_total A" "right_total B"
  shows 
    "(
      rel_set A ===> (A ===> A ===> (=)) ===> (A ===> A ===> (=)) ===> 
      rel_set B ===> (B ===> B ===> (=)) ===> (B ===> B ===> (=)) ===> 
      (=)
    ) preorder_pair_ow preorder_pair_ow"
  by (ow_locale_transfer locale_defs: preorder_pair_ow_def)

end


subsubsection‹Relativization›

context preorder_ow
begin

interpretation ord_syntax_ow .

tts_context
  tts: (?'a to U) 
  sbterms: (‹?ls::?'a ⇒ ?'a ⇒ bool› to ls)
    and (‹?le::?'a ⇒ ?'a ⇒ bool› to le)
  rewriting ctr_simps
  substituting preorder_ow_axioms
  eliminating through auto
begin

tts_lemma less_irrefl:
  assumes "x ∈ U"
  shows "¬ x <a x"
    is preorder.less_irrefl.

tts_lemma eq_refl:
  assumes "y ∈ U" and "x = y"
  shows "x ≤a y"
  is preorder.eq_refl.

tts_lemma less_imp_le:
  assumes "x ∈ U" and "y ∈ U" and "x <a y"
  shows "x ≤a y"
    is preorder.less_imp_le.

tts_lemma strict_implies_not_eq:
  assumes "b ∈ U" and "a <a b"
  shows "a ≠ b"
    is preorder.strict_implies_not_eq.

tts_lemma less_not_sym:
  assumes "x ∈ U" and "y ∈ U" and "x <a y"
  shows "¬ y <a x"
    is preorder.less_not_sym.

tts_lemma not_empty_eq_Ici_eq_empty:
  assumes "l ∈ U"
  shows "{} ≠ {l≤a..}"
    is preorder.not_empty_eq_Ici_eq_empty.

tts_lemma not_Ici_eq_empty:
  assumes "l ∈ U"
  shows "{l≤a..} ≠ {}"
    is preorder.not_Ici_eq_empty.

tts_lemma asym:
  assumes "a ∈ U" and "b ∈ U" and "a <a b" and "b <a a"
  shows False
    is preorder.asym.

tts_lemma less_asym':
  assumes "a ∈ U" and "b ∈ U" and "a <a b" and "b <a a"
  shows P
    is preorder.less_asym'.

tts_lemma less_imp_not_less:
  assumes "x ∈ U" and "y ∈ U" and "x <a y"
  shows "(¬ y <a x) = True"
    is preorder.less_imp_not_less.

tts_lemma single_Diff_lessThan:
  assumes "k ∈ U"
  shows "{k} - {..<ak} = {k}"
    is preorder.single_Diff_lessThan.

tts_lemma less_imp_triv:
  assumes "x ∈ U" and "y ∈ U" and "x <a y"
  shows "(y <a x ⟶ P) = True"
    is preorder.less_imp_triv.

tts_lemma ivl_disj_int_one:
  assumes "l ∈ U" and "u ∈ U"
  shows 
    "{..≤al} ∩ {l<a..<au} = {}"
    "{..<al} ∩ {l≤a..<au} = {}"
    "{..≤al} ∩ {l<a..≤au} = {}"
    "{..<al} ∩ {l≤a..≤au} = {}"
    "{l<a..≤au} ∩ {u<a..} = {}"
    "{l<a..<au} ∩ {u≤a..} = {}"
    "{l≤a..≤au} ∩ {u<a..} = {}"
    "{l≤a..<au} ∩ {u≤a..} = {}"
    is preorder.ivl_disj_int_one.

tts_lemma atLeastatMost_empty_iff2:
  assumes "a ∈ U" and "b ∈ U"
  shows "({} = {a≤a..≤ab}) = (¬ a ≤a b)"
    is preorder.atLeastatMost_empty_iff2.

tts_lemma atLeastLessThan_empty_iff2:
  assumes "a ∈ U" and "b ∈ U"
  shows "({} = {a≤a..<ab}) = (¬ a <a b)"
    is preorder.atLeastLessThan_empty_iff2.

tts_lemma greaterThanAtMost_empty_iff2:
  assumes "k ∈ U" and "l ∈ U"
  shows "({} = {k<a..≤al}) = (¬ k <a l)"
    is preorder.greaterThanAtMost_empty_iff2.

tts_lemma atLeastatMost_empty_iff:
  assumes "a ∈ U" and "b ∈ U"
  shows "({a≤a..≤ab} = {}) = (¬ a ≤a b)"
    is preorder.atLeastatMost_empty_iff.

tts_lemma atLeastLessThan_empty_iff:
  assumes "a ∈ U" and "b ∈ U"
  shows "({a≤a..<ab} = {}) = (¬ a <a b)"
    is preorder.atLeastLessThan_empty_iff.

tts_lemma greaterThanAtMost_empty_iff:
  assumes "k ∈ U" and "l ∈ U"
  shows "({k<a..≤al} = {}) = (¬ k <a l)"
    is preorder.greaterThanAtMost_empty_iff.

tts_lemma atLeastLessThan_empty:
  assumes "b ∈ U" and "a ∈ U" and "b ≤a a"
  shows "{a≤a..<ab} = {}"
    is preorder.atLeastLessThan_empty.

tts_lemma greaterThanAtMost_empty:
  assumes "l ∈ U" and "k ∈ U" and "l ≤a k"
  shows "{k<a..≤al} = {}"
    is preorder.greaterThanAtMost_empty.

tts_lemma greaterThanLessThan_empty:
  assumes "l ∈ U" and "k ∈ U" and "l ≤a k"
  shows "{k<a..<al} = {}"
    is preorder.greaterThanLessThan_empty.

tts_lemma le_less_trans:
  assumes "x ∈ U" and "y ∈ U" and "z ∈ U" and "x ≤a y" and "y <a z"
  shows "x <a z"
    is preorder.le_less_trans.

tts_lemma atLeastatMost_empty:
  assumes "b ∈ U" and "a ∈ U" and "b <a a"
  shows "{a≤a..≤ab} = {}"
    is preorder.atLeastatMost_empty.

tts_lemma less_le_trans:
  assumes "x ∈ U" and "y ∈ U" and "z ∈ U" and "x <a y" and "y ≤a z"
  shows "x <a z"
    is preorder.less_le_trans.

tts_lemma less_trans:
  assumes "x ∈ U" and "y ∈ U" and "z ∈ U" and "x <a y" and "y <a z"
  shows "x <a z"
    is preorder.less_trans.

tts_lemma ivl_disj_int_two:
  assumes "l ∈ U" and "m ∈ U" and "u ∈ U"
  shows 
    "{l<a..<am} ∩ {m≤a..<au} = {}"
    "{l<a..≤am} ∩ {m<a..<au} = {}"
    "{l≤a..<am} ∩ {m≤a..<au} = {}"
    "{l≤a..≤am} ∩ {m<a..<au} = {}"
    "{l<a..<am} ∩ {m≤a..≤au} = {}"
    "{l<a..≤am} ∩ {m<a..≤au} = {}"
    "{l≤a..<am} ∩ {m≤a..≤au} = {}"
    "{l≤a..≤am} ∩ {m<a..≤au} = {}"
    is preorder.ivl_disj_int_two.

tts_lemma less_asym:
  assumes "x ∈ U" and "y ∈ U" and "x <a y" and "¬ P ⟹ y <a x"
  shows P
    is preorder.less_asym.

tts_lemma Iio_Int_singleton:
  assumes "k ∈ U" and "x ∈ U"
  shows "{..<ak} ∩ {x} = (if x <a k then {x} else {})"
    is preorder.Iio_Int_singleton.

tts_lemma Ioi_le_Ico:
  assumes "a ∈ U"
  shows "{a<a..} ⊆ {a≤a..}"
    is preorder.Ioi_le_Ico.

tts_lemma Icc_subset_Iic_iff:
  assumes "l ∈ U" and "h ∈ U" and "h' ∈ U"
  shows "({l≤a..≤ah} ⊆ {..≤ah'}) = (¬ l ≤a h ∨ h ≤a h')"
    is preorder.Icc_subset_Iic_iff.

tts_lemma atLeast_subset_iff:
  assumes "x ∈ U" and "y ∈ U"
  shows "({x≤a..} ⊆ {y≤a..}) = (y ≤a x)"
    is preorder.atLeast_subset_iff.

tts_lemma Icc_subset_Ici_iff:
  assumes "l ∈ U" and "h ∈ U" and "l' ∈ U"
  shows "({l≤a..≤ah} ⊆ {l'≤a..}) = (¬ l ≤a h ∨ l' ≤a l)"
    is preorder.Icc_subset_Ici_iff.

tts_lemma atLeastatMost_subset_iff:
  assumes "a ∈ U" and "b ∈ U" and "c ∈ U" and "d ∈ U"
  shows "({a≤a..≤ab} ⊆ {c≤a..≤ad}) = (¬ a ≤a b ∨ b ≤a d ∧ c ≤a a)"
    is preorder.atLeastatMost_subset_iff.

tts_lemma atLeastatMost_psubset_iff:
  assumes "a ∈ U" and "b ∈ U" and "c ∈ U" and "d ∈ U"
  shows "({a≤a..≤ab} ⊂ {c≤a..≤ad}) = 
    (c ≤a d ∧ (¬ a ≤a b ∨ c ≤a a ∧ b ≤a d ∧ (c <a a ∨ b <a d)))"
    is preorder.atLeastatMost_psubset_iff.

tts_lemma bdd_above_empty:
  assumes "U ≠ {}"
  shows "bdd_above {}"
    is preorder.bdd_above_empty.

tts_lemma bdd_above_Iic:
  assumes "b ∈ U"
  shows "bdd_above {..≤ab}"
    is preorder.bdd_above_Iic.

tts_lemma bdd_above_Iio:
  assumes "b ∈ U"
  shows "bdd_above {..<ab}"
    is preorder.bdd_above_Iio.

tts_lemma bdd_below_empty:
  assumes "U ≠ {}"
  shows "bdd_below {}"
    is preorder.bdd_below_empty.

tts_lemma bdd_above_Icc:
  assumes "a ∈ U" and "b ∈ U"
  shows "bdd_above {a≤a..≤ab}"
    is preorder.bdd_above_Icc.

tts_lemma bdd_above_Ico:
  assumes "a ∈ U" and "b ∈ U"
  shows "bdd_above {a≤a..<ab}"
    is preorder.bdd_above_Ico.

tts_lemma bdd_above_Ioc:
  assumes "a ∈ U" and "b ∈ U"
  shows "bdd_above {a<a..≤ab}"
    is preorder.bdd_above_Ioc.

tts_lemma bdd_above_Ioo:
  assumes "a ∈ U" and "b ∈ U"
  shows "bdd_above {a<a..<ab}"
    is preorder.bdd_above_Ioo.

tts_lemma bdd_above_Int1:
  assumes "A ⊆ U" and "B ⊆ U" and "bdd_above A"
  shows "bdd_above (A ∩ B)"
    is preorder.bdd_above_Int1.

tts_lemma bdd_above_Int2:
  assumes "B ⊆ U" and "A ⊆ U" and "bdd_above B"
  shows "bdd_above (A ∩ B)"
    is preorder.bdd_above_Int2.

tts_lemma bdd_below_Icc:
  assumes "a ∈ U" and "b ∈ U"
  shows "bdd_below {a≤a..≤ab}"
    is preorder.bdd_below_Icc.

tts_lemma bdd_below_Ico:
  assumes "a ∈ U" and "b ∈ U"
  shows "bdd_below {a≤a..<ab}"
    is preorder.bdd_below_Ico.

tts_lemma bdd_below_Ioc:
  assumes "a ∈ U" and "b ∈ U"
  shows "bdd_below {a<a..≤ab}"
    is preorder.bdd_below_Ioc.

tts_lemma bdd_below_Ioo:
  assumes "a ∈ U" and "b ∈ U"
  shows "bdd_below {a<a..<ab}"
    is preorder.bdd_below_Ioo.

tts_lemma bdd_below_Ici:
  assumes "a ∈ U"
  shows "bdd_below {a≤a..}"
    is preorder.bdd_below_Ici.

tts_lemma bdd_below_Ioi:
  assumes "a ∈ U"
  shows "bdd_below {a<a..}"
    is preorder.bdd_below_Ioi.

tts_lemma bdd_above_mono:
  assumes "B ⊆ U" and "bdd_above B" and "A ⊆ B"
  shows "bdd_above A"
    is preorder.bdd_above_mono.

tts_lemma bdd_aboveI:
  assumes "A ⊆ U" and "M ∈ U" and "⋀x. ⟦x ∈ U; x ∈ A⟧ ⟹ x ≤a M"
  shows "bdd_above A"
    is preorder.bdd_aboveI.

tts_lemma bdd_aboveI2:
  assumes "range f ⊆ U" and "M ∈ U" and "⋀x. x ∈ A ⟹ f x ≤a M"
  shows "bdd_above (f ` A)"
    is preorder.bdd_aboveI2.

tts_lemma bdd_below_Int1:
  assumes "A ⊆ U" and "B ⊆ U" and "bdd_below A" 
  shows "bdd_below (A ∩ B)"
    is preorder.bdd_below_Int1.

tts_lemma bdd_below_Int2:
  assumes "B ⊆ U" and "A ⊆ U" and "bdd_below B"
  shows "bdd_below (A ∩ B)"
    is preorder.bdd_below_Int2.

tts_lemma bdd_belowI:
  assumes "A ⊆ U" and "m ∈ U" and "⋀x. ⟦x ∈ U; x ∈ A⟧ ⟹ m ≤a x"
  shows "bdd_below A"
    is preorder.bdd_belowI.

tts_lemma bdd_below_mono:
  assumes "B ⊆ U" and "bdd_below B" and "A ⊆ B"
  shows "bdd_below A"
    is preorder.bdd_below_mono.

tts_lemma bdd_belowI2:
  assumes "m ∈ U" and "range f ⊆ U" and "⋀x. x ∈ A ⟹ m ≤a f x"
  shows "bdd_below (f ` A)"
    is preorder.bdd_belowI2[where 'b='d].

end
    
end



subsection‹Partial orders›

locale order_ow = preorder_ow U le ls 
  for U :: "'a set" and le ls +
  assumes antisym: "x ∈ U ⟹ y ∈ U ⟹ le x y ⟹ le y x ⟹ x = y"

locale order_dual_ow = order_ow U le ls 
  for U :: "'a set" and le ls
begin

sublocale preorder_dual_ow ..

sublocale dual: order_ow U ge gt 
  unfolding order_ow_def order_ow_axioms_def
  apply unfold_locales
  apply(rule conjI)
  subgoal by (rule dual.preorder_ow_axioms)
  subgoal by (simp add: antisym)
  done

end

locale ord_order_ow = 
  ord_preorder_ow Ua lea lsa Ub leb lsb + ordb: order_ow Ub leb lsb
  for Ua :: "'a set" and lea lsa and Ub :: "'b set" and leb lsb

locale ord_order_dual_ow = ord_order_ow Ua lea lsa Ub leb lsb
  for Ua :: "'a set" and lea lsa and Ub :: "'b set" and leb lsb
begin

sublocale ord_preorder_dual_ow ..
sublocale ord_dual: ord_order_ow Ua ‹(≤a)› ‹(<a)› Ub ‹(≥b)› ‹(>b)›
  by unfold_locales (simp add: ordb.antisym)
sublocale dual_ord: ord_order_ow Ua ‹(≥a)› ‹(>a)› Ub ‹(≤b)› ‹(<b)› 
  by (rule ord_order_ow_axioms)
sublocale dual_dual: ord_order_ow Ua ‹(≥a)› ‹(>a)› Ub ‹(≥b)› ‹(>b)›
  by (rule ord_dual.ord_order_ow_axioms)

end

locale preorder_order_ow = 
  ord_order_ow Ua lea lsa Ub leb lsb + orda: preorder_ow Ua lea lsa
  for Ua :: "'a set" and lea lsa and Ub :: "'b set" and leb lsb
begin

sublocale preorder_pair_ow ..

end

locale preorder_order_dual_ow = preorder_order_ow Ua lea lsa Ub leb lsb
  for Ua :: "'a set" and lea lsa and Ub :: "'b set" and leb lsb
begin

sublocale ord_order_dual_ow ..
sublocale preorder_pair_dual_ow ..
sublocale ord_dual: preorder_order_ow Ua ‹(≤a)› ‹(<a)› Ub ‹(≥b)› ‹(>b)› .. 
sublocale dual_ord: preorder_order_ow Ua ‹(≥a)› ‹(>a)› Ub ‹(≤b)› ‹(<b)› .. 
sublocale dual_dual: preorder_order_ow Ua ‹(≥a)› ‹(>a)› Ub ‹(≥b)› ‹(>b)› ..

end

locale order_pair_ow = 
  preorder_order_ow Ua lea lsa Ub leb lsb + orda: order_ow Ua lea lsa
  for Ua :: "'a set" and lea lsa and Ub :: "'b set" and leb lsb
begin

sublocale rev: order_pair_ow Ub leb lsb Ua lea lsa ..

end

locale order_pair_dual_ow = order_pair_ow Ua lea lsa Ub leb lsb
  for Ua :: "'a set" and lea lsa and Ub :: "'b set" and leb lsb
begin

sublocale preorder_order_dual_ow ..
sublocale ord_dual: order_pair_ow Ua ‹(≤a)› ‹(<a)› Ub ‹(≥b)› ‹(>b)› ..
sublocale dual_ord: order_pair_ow Ua ‹(≥a)› ‹(>a)› Ub ‹(≤b)› ‹(<b)› 
  by unfold_locales (simp add: orda.antisym)
sublocale dual_dual: order_pair_ow Ua ‹(≥a)› ‹(>a)› Ub ‹(≥b)› ‹(>b)› ..

end


subsubsection‹Transfer rules›

lemma order_ow[ud_with]: "order = order_ow UNIV"
  unfolding 
    order_def order_ow_def order_axioms_def order_ow_axioms_def ud_with 
  by simp

lemma ord_order_ow[ud_with]: "ord_order = ord_order_ow UNIV"
  unfolding ord_order_def ord_order_ow_def ud_with by simp

lemma preorder_order_ow[ud_with]: 
  "preorder_order = 
    (λlea lsa leb lsb. preorder_order_ow UNIV lea lsa UNIV leb lsb)"
  unfolding preorder_order_def preorder_order_ow_def ud_with by simp

lemma order_pair_ow[ud_with]: 
  "order_pair = (λlea lsa leb lsb. order_pair_ow UNIV lea lsa UNIV leb lsb)"
  unfolding order_pair_def order_pair_ow_def ud_with by simp

context
  includes lifting_syntax
begin

lemma order_ow_transfer[transfer_rule]:
  assumes [transfer_rule]: "bi_unique A" "right_total A"
  shows 
    "(rel_set A ===> (A ===> A ===> (=)) ===> (A ===> A ===> (=)) ===> (=)) 
      order_ow order_ow"
  by (ow_locale_transfer locale_defs: order_ow_def order_ow_axioms_def)

lemma ord_order_ow_transfer[transfer_rule]:
  assumes [transfer_rule]: "bi_unique A" "right_total A"
  shows 
    "(
      rel_set A ===> (A ===> A ===> (=)) ===> (A ===> A ===> (=)) ===>
      (=)
    ) ord_order_ow ord_order_ow"
  by (ow_locale_transfer locale_defs: ord_order_ow_def)

lemma preorder_order_ow_transfer[transfer_rule]:
  assumes [transfer_rule]: "right_total A" "bi_unique B" "right_total B"
  shows 
    "(
      rel_set A ===> (A ===> A ===> (=)) ===> (A ===> A ===> (=)) ===> 
      rel_set B ===> (B ===> B ===> (=)) ===> (B ===> B ===> (=)) ===> 
      (=)
    ) preorder_order_ow preorder_order_ow"
  by (ow_locale_transfer locale_defs: preorder_order_ow_def)

lemma order_pair_ow_transfer[transfer_rule]:
  assumes [transfer_rule]: 
    "bi_unique A" "right_total A" "bi_unique B" "right_total B"
  shows 
    "(
      rel_set A ===> (A ===> A ===> (=)) ===> (A ===> A ===> (=)) ===> 
      rel_set B ===> (B ===> B ===> (=)) ===> (B ===> B ===> (=)) ===> 
      (=)
    ) order_pair_ow order_pair_ow"
  by (ow_locale_transfer locale_defs: order_pair_ow_def)

end


subsubsection‹Relativization›

context order_ow
begin

interpretation ord_syntax_ow .

tts_context
  tts: (?'a to U)
  sbterms: (‹?ls::?'a ⇒ ?'a ⇒ bool› to ls)
    and (‹?le::?'a ⇒ ?'a ⇒ bool› to le)
  rewriting ctr_simps
  substituting order_ow_axioms
  eliminating through auto
begin

tts_lemma atLeastAtMost_singleton:
  assumes "a ∈ U"
  shows "{a≤a..≤aa} = {a}"
  is order.atLeastAtMost_singleton.
    
tts_lemma less_imp_not_eq:
  assumes "y ∈ U" and "x <a y"
  shows "(x = y) = False"
  is order.less_imp_not_eq.
    
tts_lemma less_imp_not_eq2:
  assumes "y ∈ U" and "x <a y"
  shows "(y = x) = False"
    is order.less_imp_not_eq2.

tts_lemma eq_iff:
  assumes "x ∈ U" and "y ∈ U"
  shows "(x = y) = (x ≤a y ∧ y ≤a x)"
    is order.eq_iff.

tts_lemma le_less:
  assumes "x ∈ U" and "y ∈ U"
  shows "(x ≤a y) = (x <a y ∨ x = y)"
    is order.le_less.

tts_lemma min_absorb2:
  assumes "y ∈ U" and "x ∈ U" and "y ≤a x"
  shows "min x y = y"
    is order.min_absorb2.

tts_lemma less_le:
  assumes "x ∈ U" and "y ∈ U"
  shows "(x <a y) = (x ≤a y ∧ x ≠ y)"
    is order.less_le.

tts_lemma le_imp_less_or_eq:
  assumes "x ∈ U" and "y ∈ U" and "x ≤a y"
  shows "x <a y ∨ x = y"
    is order.le_imp_less_or_eq.

tts_lemma antisym_conv:
  assumes "y ∈ U" and "x ∈ U" and "y ≤a x"
  shows "(x ≤a y) = (x = y)"
    is order.antisym_conv.

tts_lemma le_neq_trans:
  assumes "a ∈ U" and "b ∈ U" and "a ≤a b" and "a ≠ b"
  shows "a <a b"
    is order.le_neq_trans.

tts_lemma neq_le_trans:
  assumes "a ∈ U" and "b ∈ U" and "a ≠ b" and "a ≤a b"
  shows "a <a b"
    is order.neq_le_trans.

tts_lemma atLeastAtMost_singleton':
  assumes "b ∈ U" and "a = b"
  shows "{a≤a..≤ab} = {a}"
    is order.atLeastAtMost_singleton'.

tts_lemma atLeastLessThan_eq_atLeastAtMost_diff:
  assumes "a ∈ U" and "b ∈ U"
  shows "{a≤a..<ab} = {a≤a..≤ab} - {b}"
    is order.atLeastLessThan_eq_atLeastAtMost_diff.

tts_lemma greaterThanAtMost_eq_atLeastAtMost_diff:
  assumes "a ∈ U" and "b ∈ U"
  shows "{a<a..≤ab} = {a≤a..≤ab} - {a}"
    is order.greaterThanAtMost_eq_atLeastAtMost_diff.

tts_lemma atMost_Int_atLeast:
  assumes "n ∈ U"
  shows "{..≤an} ∩ {n≤a..} = {n}"
    is order.atMost_Int_atLeast.

tts_lemma atLeast_eq_iff:
  assumes "x ∈ U" and "y ∈ U"
  shows "({x≤a..} = {y≤a..}) = (x = y)"
    is order.atLeast_eq_iff.

tts_lemma Least_equality:
  assumes "x ∈ U" and "P x" 
    and "⋀y. ⟦y ∈ U; P y⟧ ⟹ x ≤a y"
  shows "Least P = Some x"
    is order.Least_equality.

tts_lemma Icc_eq_Icc:
  assumes "l ∈ U" and "h ∈ U" and "l' ∈ U" and "h' ∈ U"
  shows "({l≤a..≤ah} = {l'≤a..≤ah'}) = 
    (h = h' ∧ l = l' ∨ ¬ l' ≤a h' ∧ ¬ l ≤a h)"
    is order.Icc_eq_Icc.

tts_lemma LeastI2_order:
  assumes "x ∈ U"
    and "P x"
    and "⋀y. ⟦y ∈ U; P y⟧ ⟹ x ≤a y"
    and "⋀x. ⟦x ∈ U; P x; ∀y∈U. P y ⟶ x ≤a y⟧ ⟹ Q x"
    and "⋀z. ⟦z ∈ U; Least P = Some z; Q z⟧ ⟹ thesis"
  shows thesis
    is order.LeastI2_order.

tts_lemma mono_image_least:
  assumes "∀x∈U. f x ∈ U"
    and "m ∈ U"
    and "n ∈ U"
    and "m' ∈ U"
    and "n' ∈ U"
    and "on U with (≤a) (≤a) : «mono» f"
    and "f ` {m≤a..<an} = {m'≤a..<an'}"
    and "m <a n"
  shows "f m = m'"
    is order.mono_image_least.

tts_lemma antisym_conv1:
  assumes "x ∈ U" and "y ∈ U" and "¬ x <a y"
  shows "(x ≤a y) = (x = y)"
    is order.antisym_conv1.

tts_lemma antisym_conv2:
  assumes "x ∈ U" and "y ∈ U" and "x ≤a y"
  shows "(¬ x <a y) = (x = y)"
    is order.antisym_conv2.

tts_lemma leD:
  assumes "y ∈ U" and "x ∈ U" and "y ≤a x"
  shows "¬ x <a y"
    is order.leD.

end

tts_context
  tts: (?'a to U)
  rewriting ctr_simps
  substituting order_ow_axioms
  eliminating ‹?A ≠ {}› through auto
begin

tts_lemma atLeastAtMost_singleton_iff:
  assumes "a ∈ U"
    and "b ∈ U"
    and "c ∈ U"
  shows "({a≤a..≤ab} = {c}) = (a = b ∧ b = c)"
    is order.atLeastAtMost_singleton_iff.

end

tts_context
  tts: (?'a to U)
  sbterms: (‹?ls::?'a ⇒ ?'a ⇒ bool› to ls)
    and (‹?le::?'a ⇒ ?'a ⇒ bool› to le)
  rewriting ctr_simps
  substituting order_ow_axioms
  eliminating through auto
begin

tts_lemma Least_ex1:
  assumes "z ∈ U"
    and "∃!x. x ∈ U ∧ P x ∧ (∀y∈U. P y ⟶ x ≤a y)"
    and "⋀x. ⟦x ∈ U; Least P = Some x; P x; P z ⟹ x ≤a z⟧ ⟹ thesis"
  shows thesis
    is order.Least_ex1.
    
end    

end

context order_pair_ow
begin

interpretation ord_pair_syntax_ow .

tts_context
  tts: (?'a to Ua) and (?'b to Ub)
  sbterms: (‹?lsa::?'a ⇒ ?'a ⇒ bool› to lsa)
    and (‹?lea::?'a ⇒ ?'a ⇒ bool› to lea)
    and (‹?lsb::?'b ⇒ ?'b ⇒ bool› to lsb)
    and (‹?leb::?'b ⇒ ?'b ⇒ bool› to leb)
  rewriting ctr_simps
  substituting order_pair_ow_axioms
  eliminating through (auto simp: mono_def bdd_def)
begin

tts_lemma strict_mono_mono:
  assumes "∀x∈Ua. f x ∈ Ub" and "strict_monoab f"
  shows "monoab f"
    is order_pair.strict_mono_mono.

tts_lemma bdd_above_image_mono:
  assumes "∀x∈Ua. f x ∈ Ub" and "A ⊆ Ua" and "monoab f" and "orda.bdd_above A"
  shows "ordb.bdd_above (f ` A)"
    is order_pair.bdd_above_image_mono.

tts_lemma bdd_below_image_mono:
  assumes "∀x∈Ua. f x ∈ Ub" and "A ⊆ Ua" and "monoab f" and "orda.bdd_below A"
  shows "ordb.bdd_below (f ` A)"
    is order_pair.bdd_below_image_mono.

tts_lemma bdd_below_image_antimono:
  assumes "∀x∈Ua. f x ∈ Ub" 
    and "A ⊆ Ua" 
    and "antimonoab f" 
    and "orda.bdd_above A"
  shows "ordb.bdd_below (f ` A)"
    is order_pair.bdd_below_image_antimono.

tts_lemma bdd_above_image_antimono:
  assumes "∀x∈Ua. f x ∈ Ub"
    and "A ⊆ Ua"
    and "antimonoab f"
    and "orda.bdd_below A"
  shows "ordb.bdd_above (f ` A)"
    is order_pair.bdd_above_image_antimono.

end

end



subsection‹Dense orders›


subsubsection‹Definitions and common properties›

locale dense_order_ow = order_ow U le ls
  for U :: "'a set" and le ls +
  assumes dense: "⟦ x ∈ U; y ∈ U; ls x y ⟧ ⟹ (∃z∈U. ls x z ∧ ls z y)"

locale dense_order_dual_ow = dense_order_ow U le ls
  for U :: "'a set" and le ls
begin

interpretation ord_syntax_ow .

sublocale order_dual_ow ..

sublocale dual: dense_order_ow U ge gt 
  using dense by unfold_locales auto

end

locale ord_dense_order_ow = 
  ord_order_ow Ua lea lsa Ub leb lsb + ordb: dense_order_ow Ub leb lsb
  for Ua :: "'a set" and lea lsa and Ub :: "'b set" and leb lsb

locale ord_dense_order_dual_ow = ord_dense_order_ow Ua lea lsa Ub leb lsb
  for Ua :: "'a set" and lea lsa and Ub :: "'b set" and leb lsb  
begin

sublocale ord_order_dual_ow ..
sublocale ord_dual: ord_dense_order_ow Ua ‹(≤a)› ‹(<a)› Ub ‹(≥b)› ‹(>b)›
  using ordb.dense by unfold_locales blast
sublocale dual_ord: ord_dense_order_ow Ua ‹(≥a)› ‹(>a)› Ub ‹(≤b)› ‹(<b)› 
  by (rule ord_dense_order_ow_axioms)
sublocale dual_dual: ord_dense_order_ow Ua ‹(≥a)› ‹(>a)› Ub ‹(≥b)› ‹(>b)›
  by (rule ord_dual.ord_dense_order_ow_axioms)

end

locale preorder_dense_order_ow = 
  ord_dense_order_ow Ua lea lsa Ub leb lsb + orda: preorder_ow Ua lea lsa
  for Ua :: "'a set" and lea lsa and Ub :: "'b set" and leb lsb
begin

sublocale preorder_order_ow ..

end

locale preorder_dense_order_dual_ow = 
  preorder_dense_order_ow Ua lea lsa Ub leb lsb
  for Ua :: "'a set" and lea lsa and Ub :: "'b set" and leb lsb
begin

sublocale ord_dense_order_dual_ow ..
sublocale preorder_order_dual_ow ..
sublocale ord_dual: preorder_dense_order_ow Ua ‹(≤a)› ‹(<a)› Ub ‹(≥b)› ‹(>b)› 
  ..
sublocale dual_ord: preorder_dense_order_ow Ua ‹(≥a)› ‹(>a)› Ub ‹(≤b)› ‹(<b)› 
  ..    
sublocale dual_dual: preorder_dense_order_ow Ua ‹(≥a)› ‹(>a)› Ub ‹(≥b)› ‹(>b)› 
  ..

end

locale order_dense_order_ow = 
  preorder_dense_order_ow Ua lea lsa Ub leb lsb + orda: order_ow Ua lea lsa
  for Ua :: "'a set" and lea lsa and Ub :: "'b set" and leb lsb
begin

sublocale order_pair_ow ..

end

locale order_dense_order_dual_ow = order_dense_order_ow Ua lea lsa Ub leb lsb
  for Ua :: "'a set" and lea lsa and Ub :: "'b set" and leb lsb
begin

sublocale preorder_dense_order_dual_ow ..
sublocale order_pair_dual_ow ..
sublocale ord_dual: order_dense_order_ow Ua ‹(≤a)› ‹(<a)› Ub ‹(≥b)› ‹(>b)› ..
sublocale dual_ord: order_dense_order_ow Ua ‹(≥a)› ‹(>a)› Ub ‹(≤b)› ‹(<b)› ..    
sublocale dual_dual: order_dense_order_ow Ua ‹(≥a)› ‹(>a)› Ub ‹(≥b)› ‹(>b)› ..

end

locale dense_order_pair_ow = 
  order_dense_order_ow Ua lea lsa Ub leb lsb + orda: dense_order_ow Ua lea lsa
  for Ua :: "'a set" and lea lsa and Ub :: "'b set" and leb lsb

locale dense_order_pair_dual_ow = dense_order_pair_ow Ua lea lsa Ub leb lsb
  for Ua :: "'a set" and lea lsa and Ub :: "'b set" and leb lsb
begin

sublocale order_dense_order_dual_ow ..
sublocale ord_dual: dense_order_pair_ow Ua ‹(≤a)› ‹(<a)› Ub ‹(≥b)› ‹(>b)› ..
sublocale dual_ord: dense_order_pair_ow Ua ‹(≥a)› ‹(>a)› Ub ‹(≤b)› ‹(<b)› 
  using orda.dense by unfold_locales auto
sublocale dual_dual: dense_order_pair_ow Ua ‹(≥a)› ‹(>a)› Ub ‹(≥b)› ‹(>b)› ..

end


subsubsection‹Transfer rules›

lemma dense_order_ow[ud_with]: "dense_order = dense_order_ow UNIV"
  unfolding 
    dense_order_def dense_order_ow_def 
    dense_order_axioms_def dense_order_ow_axioms_def 
    ud_with 
  by simp

lemma ord_dense_order_ow[ud_with]: "ord_dense_order = ord_dense_order_ow UNIV"
  unfolding ord_dense_order_def ord_dense_order_ow_def ud_with by simp

lemma preorder_dense_order_ow[ud_with]: 
  "preorder_dense_order = 
    (λlea lsa leb lsb. preorder_dense_order_ow UNIV lea lsa UNIV leb lsb)"
  unfolding preorder_dense_order_def preorder_dense_order_ow_def ud_with 
  by simp

lemma order_dense_order_ow[ud_with]: 
  "order_dense_order = 
    (λlea lsa leb lsb. order_dense_order_ow UNIV lea lsa UNIV leb lsb)"
  unfolding order_dense_order_def order_dense_order_ow_def ud_with by simp

lemma dense_order_pair_ow[ud_with]: 
  "dense_order_pair = 
    (λlea lsa leb lsb. dense_order_pair_ow UNIV lea lsa UNIV leb lsb)"
  unfolding dense_order_pair_def dense_order_pair_ow_def ud_with by simp

context
  includes lifting_syntax
begin

lemma desne_order_ow_transfer[transfer_rule]:
  assumes [transfer_rule]: "bi_unique A" "right_total A"
  shows 
    "(rel_set A ===> (A ===> A ===> (=)) ===> (A ===> A ===> (=)) ===> (=)) 
      dense_order_ow dense_order_ow"
  by 
    (
      ow_locale_transfer locale_defs: 
        dense_order_ow_def dense_order_ow_axioms_def
    )

lemma ord_dense_order_ow_transfer[transfer_rule]:
  assumes [transfer_rule]: "bi_unique A" "right_total A"
  shows 
    "(
      rel_set A ===> (A ===> A ===> (=)) ===> (A ===> A ===> (=)) ===>
      (=)
    ) ord_dense_order_ow ord_dense_order_ow"
  by (ow_locale_transfer locale_defs: ord_dense_order_ow_def)

lemma preorder_dense_order_ow_transfer[transfer_rule]:
  assumes [transfer_rule]: "right_total A" "bi_unique B" "right_total B"
  shows 
    "(
      rel_set A ===> (A ===> A ===> (=)) ===> (A ===> A ===> (=)) ===> 
      rel_set B ===> (B ===> B ===> (=)) ===> (B ===> B ===> (=)) ===> 
      (=)
    ) preorder_dense_order_ow preorder_dense_order_ow"
  by (ow_locale_transfer locale_defs: preorder_dense_order_ow_def)

lemma order_dense_order_ow_transfer[transfer_rule]:
  assumes [transfer_rule]: 
    "bi_unique A" "right_total A" "bi_unique B" "right_total B"
  shows 
    "(
      rel_set A ===> (A ===> A ===> (=)) ===> (A ===> A ===> (=)) ===> 
      rel_set B ===> (B ===> B ===> (=)) ===> (B ===> B ===> (=)) ===> 
      (=)
    ) order_dense_order_ow order_dense_order_ow"
  by (ow_locale_transfer locale_defs: order_dense_order_ow_def)

lemma dense_order_pair_ow_transfer[transfer_rule]:
  assumes [transfer_rule]: 
    "bi_unique A" "right_total A" "bi_unique B" "right_total B"
  shows 
    "(
      rel_set A ===> (A ===> A ===> (=)) ===> (A ===> A ===> (=)) ===> 
      rel_set B ===> (B ===> B ===> (=)) ===> (B ===> B ===> (=)) ===> 
      (=)
    ) dense_order_pair_ow dense_order_pair_ow"
  by (ow_locale_transfer locale_defs: dense_order_pair_ow_def)

end



subsection‹(Unique) top and bottom elements›

locale extremum_ow =
  fixes U :: "'a set" and extremum 
  assumes extremum_closed[simp]: "extremum ∈ U"

locale bot_ow = extremum_ow U bot for U :: "'a set" and bot
begin

notation bot ("⊥")

end

locale top_ow = extremum_ow U top for U :: "'a set" and top
begin

notation top ("⊤")

end

locale ord_extremum_ow = ord_ow U le ls + extremum_ow U extremum 
  for U :: "'a set" and le ls extremum

locale order_extremum_ow = ord_extremum_ow U le ls extremum + order_ow U le ls
  for U :: "'a set" and le ls extremum +
  assumes extremum[simp]: "a ∈ U ⟹ le a extremum"

locale order_bot_ow = 
  order_dual_ow U le ls + dual: order_extremum_ow U ge gt bot + bot_ow U bot 
  for U :: "'a set" and le ls bot

locale order_top = 
  order_dual_ow U le ls + order_extremum_ow U le ls top + top_ow U top
  for U :: "'a set" and le ls top


subsubsection‹Transfer rules›

lemma order_extremum_ow[ud_with]: "order_extremum = order_extremum_ow UNIV"
  unfolding 
    order_extremum_def order_extremum_axioms_def 
    order_extremum_ow_def order_extremum_ow_axioms_def
    ord_extremum_ow_def extremum_ow_def
    ud_with 
  by simp

context
  includes lifting_syntax
begin

lemma extremum_ow_transfer[transfer_rule]:
  assumes [transfer_rule]: "bi_unique A"
  shows "(rel_set A ===> A ===> (=)) extremum_ow extremum_ow"
  by (ow_locale_transfer locale_defs: extremum_ow_def)

lemma ord_extremum_ow_transfer[transfer_rule]:
  assumes [transfer_rule]: "bi_unique A"
  shows "(rel_set A ===> A ===> (=)) ord_extremum_ow ord_extremum_ow"
  by (ow_locale_transfer locale_defs: ord_extremum_ow_def)

lemma order_extremum_ow_transfer[transfer_rule]:
  assumes [transfer_rule]: "bi_unique A" "right_total A"
  shows 
    "(
      rel_set A ===> (A ===> A ===> (=)) ===> (A ===> A ===> (=)) ===> A ===> 
      (=)
    ) order_extremum_ow order_extremum_ow"
  by 
    (
      ow_locale_transfer locale_defs: 
        order_extremum_ow_def order_extremum_ow_axioms_def
    )

end


subsubsection‹Relativization›

context order_extremum_ow
begin

interpretation ord_syntax_ow .

tts_context
  tts: (?'a to U)
  sbterms: (‹?le::?'a ⇒ ?'a ⇒ bool› to le)
    and (‹?ls::?'a ⇒ ?'a ⇒ bool› to ls)
  rewriting ctr_simps
  substituting order_extremum_ow_axioms
  eliminating through force
begin

tts_lemma extremum_strict:
  assumes "a ∈ U"
  shows "¬ extremum <a a"
    is order_extremum.extremum_strict.
    
tts_lemma bdd_above_top:
  assumes "A ⊆ U"
  shows "bdd_above A"
    is order_extremum.bdd_above_top.
    
tts_lemma min_top:
  assumes "x ∈ U"
  shows "min extremum x = x"
  is order_extremum.min_top.

tts_lemma min_top2:
  assumes "x ∈ U"
  shows "min x extremum = x"
  is order_extremum.min_top2.
    
tts_lemma extremum_unique:
  assumes "a ∈ U"
  shows "(extremum ≤a a) = (a = extremum)"
is order_extremum.extremum_unique.
    
tts_lemma not_eq_extremum:
  assumes "a ∈ U"
  shows "(a ≠ extremum) = (a <a extremum)"
  is order_extremum.not_eq_extremum.
    
tts_lemma extremum_uniqueI:
  assumes "a ∈ U" and "extremum ≤a a"
  shows "a = extremum"
    is order_extremum.extremum_uniqueI.
    
tts_lemma max_top:
  assumes "x ∈ U"
  shows "max extremum x = extremum"
    is order_extremum.max_top.

tts_lemma max_top2:
  assumes "x ∈ U"
  shows "max x extremum = extremum"
    is order_extremum.max_top2.

tts_lemma atMost_eq_UNIV_iff:
  assumes "x ∈ U"
  shows "({..≤ax} = U) = (x = extremum)"
    is order_extremum.atMost_eq_UNIV_iff.

end

end



subsection‹Absence of top or bottom elements›

locale no_extremum_ow = order_ow U le ls for U :: "'a set" and le ls +
  assumes gt_ex: "x ∈ U ⟹ ∃y∈U. ls x y"

locale no_top_ow = order_dual_ow U le ls + no_extremum_ow U le ls 
  for U :: "'a set" and le ls

locale no_bot_ow = order_dual_ow U le ls + dual: no_extremum_ow U ge gt 
  for U :: "'a set" and le ls

subsubsection‹Transfer rules›

lemma no_extremum_ow[ud_with]: "no_extremum = no_extremum_ow UNIV"
  unfolding 
    no_extremum_def no_extremum_ow_def 
    no_extremum_axioms_def no_extremum_ow_axioms_def
    ud_with
  by simp

context
  includes lifting_syntax
begin

lemma no_extremum_ow_axioms_transfer[transfer_rule]:
  assumes [transfer_rule]: "bi_unique A" "right_total A"
  shows 
    "(rel_set A ===> (A ===> A ===> (=)) ===> (=)) 
      no_extremum_ow_axioms no_extremum_ow_axioms"
  by (ow_locale_transfer locale_defs:  no_extremum_ow_axioms_def)

lemma no_extremum_ow_transfer[transfer_rule]:
  assumes [transfer_rule]: "bi_unique A" "right_total A"
  shows 
    "(rel_set A ===> (A ===> A ===> (=)) ===> (A ===> A ===> (=)) ===> (=)) 
      no_extremum_ow no_extremum_ow"
  by (ow_locale_transfer locale_defs: no_extremum_ow_def)

end


subsubsection‹Relativization›

lemma right_total_UNIV_transfer'[transfer_rule]: 
  assumes "right_total A" and "Domainp A = (λx. x ∈ U)"
  shows "rel_set A U UNIV"
  using assms right_total_UNIV_transfer by fastforce

context no_extremum_ow
begin

interpretation ord_syntax_ow .

tts_context
  tts: (?'a to U)
  sbterms: (‹?le::?'a ⇒ ?'a ⇒ bool› to le)
    and (‹?ls::?'a ⇒ ?'a ⇒ bool› to ls)
  rewriting ctr_simps
  substituting no_extremum_ow_axioms
  eliminating through force
begin

tts_lemma not_UNIV_eq_Iic:
  assumes "h' ∈ U"
  shows "U ≠ {..≤ah'}"
  is no_extremum.not_UNIV_eq_Iic.

tts_lemma not_Iic_eq_UNIV:
  assumes "h' ∈ U"
  shows "{..≤ah'} ≠ U"
    is no_extremum.not_Iic_eq_UNIV.

tts_lemma not_UNIV_le_Iic:
  assumes "h ∈ U"
  shows "¬ U ⊆ {..≤ah}"
    is no_extremum.not_UNIV_le_Iic.

tts_lemma not_UNIV_eq_Icc:
  assumes "l' ∈ U" and "h' ∈ U"
  shows "U ≠ {l'≤a..≤ah'}"
    is no_extremum.not_UNIV_eq_Icc.

tts_lemma not_Icc_eq_UNIV:
  assumes "l' ∈ U" and "h' ∈ U"
  shows "{l'≤a..≤ah'} ≠ U"
    is no_extremum.not_Icc_eq_UNIV.

tts_lemma not_UNIV_le_Icc:
  assumes "l ∈ U" and "h ∈ U"
  shows "¬ U ⊆ {l≤a..≤ah}"
    is no_extremum.not_UNIV_le_Icc.

tts_lemma greaterThan_non_empty:
  assumes "x ∈ U"
  shows "{x<a..} ≠ {}"
    is no_extremum.greaterThan_non_empty.

tts_lemma not_Iic_eq_Ici:
  assumes "h ∈ U" and "l' ∈ U"
  shows "{..≤ah} ≠ {l'≤a..}"
    is no_extremum.not_Iic_eq_Ici.

tts_lemma not_Ici_eq_Iic:
  assumes "l' ∈ U" and "h ∈ U"
  shows "{l'≤a..} ≠ {..≤ah}"
    is no_extremum.not_Ici_eq_Iic.

tts_lemma not_Ici_le_Iic:
  assumes "l ∈ U" and "h' ∈ U"
  shows "¬ {l≤a..} ⊆ {..≤ah'}"
    is no_extremum.not_Ici_le_Iic.

tts_lemma not_Icc_eq_Ici:
  assumes "l ∈ U" and "h ∈ U" and "l' ∈ U"
  shows "{l≤a..≤ah} ≠ {l'≤a..}"
    is no_extremum.not_Icc_eq_Ici.

tts_lemma not_Ici_eq_Icc:
  assumes "l' ∈ U" and "l ∈ U" and "h ∈ U"
  shows "{l'≤a..} ≠ {l≤a..≤ah}"
    is no_extremum.not_Ici_eq_Icc.

tts_lemma not_Ici_le_Icc:
  assumes "l ∈ U" and "l' ∈ U" and "h' ∈ U"
  shows "¬ {l≤a..} ⊆ {l'≤a..≤ah'}"
    is no_extremum.not_Ici_le_Icc.

end

end

declare right_total_UNIV_transfer'[transfer_rule del]

text‹\newpage›

end