# 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 = ord⇩a: ord_ow U⇩a le⇩a ls⇩a + ord⇩b: ord_ow U⇩b le⇩b ls⇩b
for U⇩a :: "'a set" and le⇩a ls⇩a and U⇩b :: "'b set" and le⇩b ls⇩b
begin

sublocale rev: ord_pair_ow U⇩b le⇩b ls⇩b U⇩a le⇩a ls⇩a .

end

locale ord_pair_syntax_ow = ord_pair_ow U⇩a le⇩a ls⇩a U⇩b le⇩b ls⇩b
for U⇩a :: "'a set" and le⇩a ls⇩a and U⇩b :: "'b set" and le⇩b ls⇩b
begin

sublocale ord⇩a: ord_syntax_ow U⇩a le⇩a ls⇩a + ord⇩b: ord_syntax_ow U⇩b le⇩b ls⇩b .

notation le⇩a (‹'(≤⇩a')›)
and le⇩a (infix ‹≤⇩a› 50)
and ls⇩a (‹'(<⇩a')›)
and ls⇩a (infix ‹<⇩a› 50)
and le⇩b (‹'(≤⇩b')›)
and le⇩b (infix ‹≤⇩b› 50)
and ls⇩b (‹'(<⇩b')›)
and ls⇩b (infix ‹<⇩b› 50)

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

abbreviation mono⇩a⇩b
where "mono⇩a⇩b ≡ Type_Simple_Orders.mono U⇩a (≤⇩a) (≤⇩b)"
abbreviation mono⇩b⇩a
where "mono⇩b⇩a ≡ Type_Simple_Orders.mono U⇩b (≤⇩b) (≤⇩a)"
abbreviation antimono⇩a⇩b
where "antimono⇩a⇩b ≡ Type_Simple_Orders.mono U⇩a (≤⇩a) (≥⇩b)"
abbreviation antimono⇩b⇩a
where "antimono⇩b⇩a ≡ Type_Simple_Orders.mono U⇩b (≤⇩b) (≥⇩a)"
abbreviation strict_mono⇩a⇩b
where "strict_mono⇩a⇩b ≡ Type_Simple_Orders.mono U⇩a (<⇩a) (<⇩b)"
abbreviation strict_mono⇩b⇩a
where "strict_mono⇩b⇩a ≡ Type_Simple_Orders.mono U⇩b (<⇩b) (<⇩a)"
abbreviation strict_antimono⇩a⇩b
where "strict_antimono⇩a⇩b ≡ Type_Simple_Orders.mono U⇩a (<⇩a) (>⇩b)"
abbreviation strict_antimono⇩b⇩a
where "strict_antimono⇩b⇩a ≡ Type_Simple_Orders.mono U⇩b (<⇩b) (>⇩a)"

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

end

locale ord_pair_dual_ow = ord_pair_syntax_ow U⇩a le⇩a ls⇩a U⇩b le⇩b ls⇩b
for U⇩a :: "'a set" and le⇩a ls⇩a and U⇩b :: "'b set" and le⇩b ls⇩b

context ord_pair_dual_ow
begin

sublocale ord_dual: ord_pair_ow U⇩a ‹(≤⇩a)› ‹(<⇩a)› U⇩b ‹(≥⇩b)› ‹(>⇩b)› .
sublocale dual_ord: ord_pair_ow U⇩a ‹(≥⇩a)› ‹(>⇩a)› U⇩b ‹(≤⇩b)› ‹(<⇩b)› .
sublocale dual_dual: ord_pair_ow U⇩a ‹(≥⇩a)› ‹(>⇩a)› U⇩b ‹(≥⇩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 U⇩a) and (?'b to U⇩b)
sbterms: (‹?le⇩a::?'a⇒?'a⇒bool› to le⇩a) and (‹?le⇩b::?'b⇒?'b⇒bool› to le⇩b)
rewriting ctr_simps
eliminating through (simp add: Type_Simple_Orders.mono_def)
begin

tts_lemma monoD:
assumes "x ∈ U⇩a" and "y ∈ U⇩a" and "mono⇩a⇩b f" and "x ≤⇩a y"
shows "f x ≤⇩b f y"
is ord_pair.monoD.

tts_lemma monoI:
assumes "⋀x y. ⟦x ∈ U⇩a; y ∈ U⇩a; x ≤⇩a y⟧ ⟹ f x ≤⇩b f y"
shows "mono⇩a⇩b f"
is ord_pair.monoI.

tts_lemma monoE:
assumes "x ∈ U⇩a"
and "y ∈ U⇩a"
and "mono⇩a⇩b f"
and "x ≤⇩a y"
and "f x ≤⇩b f y ⟹ thesis"
shows thesis
is ord_pair.monoE.

end

tts_context
tts: (?'a to U⇩a) and (?'b to U⇩b)
sbterms: (‹?ls⇩a::?'a⇒?'a⇒bool› to le⇩a) and (‹?ls⇩b::?'b⇒?'b⇒bool› to le⇩b)
rewriting ctr_simps
eliminating through (simp add: Type_Simple_Orders.mono_def)
begin

tts_lemma strict_monoD:
assumes "x ∈ U⇩a"
and "y ∈ U⇩a"
and "mono⇩a⇩b f"
and "x ≤⇩a y"
shows "f x ≤⇩b f y"
is ord_pair.strict_monoD.

tts_lemma strict_monoI:
assumes "⋀x y. ⟦x ∈ U⇩a; y ∈ U⇩a; x ≤⇩a y⟧ ⟹ f x ≤⇩b f y"
shows "mono⇩a⇩b f"
is ord_pair.strict_monoI.

tts_lemma strict_monoE:
assumes "x ∈ U⇩a"
and "y ∈ U⇩a"
and "mono⇩a⇩b 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 U⇩a le⇩a ls⇩a U⇩b le⇩b ls⇩b + ord⇩b: preorder_ow U⇩b le⇩b ls⇩b
for U⇩a :: "'a set" and le⇩a ls⇩a and U⇩b :: "'b set" and le⇩b ls⇩b

locale ord_preorder_dual_ow = ord_preorder_ow U⇩a le⇩a ls⇩a U⇩b le⇩b ls⇩b
for U⇩a :: "'a set" and le⇩a ls⇩a and U⇩b :: "'b set" and le⇩b ls⇩b
begin

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

end

locale preorder_pair_ow =
ord_preorder_ow U⇩a le⇩a ls⇩a U⇩b le⇩b ls⇩b + ord⇩a: preorder_ow U⇩a le⇩a ls⇩a
for U⇩a :: "'a set" and le⇩a ls⇩a and U⇩b :: "'b set" and le⇩b ls⇩b
begin

sublocale rev: preorder_pair_ow U⇩b le⇩b ls⇩b U⇩a le⇩a ls⇩a ..

end

locale preorder_pair_dual_ow = preorder_pair_ow U⇩a le⇩a ls⇩a U⇩b le⇩b ls⇩b
for U⇩a :: "'a set" and le⇩a ls⇩a and U⇩b :: "'b set" and le⇩b ls⇩b
begin

sublocale ord_preorder_dual_ow ..
sublocale ord_dual: preorder_pair_ow U⇩a ‹(≤⇩a)› ‹(<⇩a)› U⇩b ‹(≥⇩b)› ‹(>⇩b)› ..
sublocale dual_ord: preorder_pair_ow U⇩a ‹(≥⇩a)› ‹(>⇩a)› U⇩b ‹(≤⇩b)› ‹(<⇩b)›
by unfold_locales (auto intro: ord⇩a.order_trans simp: ord⇩a.less_le_not_le)
sublocale dual_dual: preorder_pair_ow U⇩a ‹(≥⇩a)› ‹(>⇩a)› U⇩b ‹(≥⇩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 =
(λle⇩a ls⇩a le⇩b ls⇩b. preorder_pair_ow UNIV le⇩a ls⇩a UNIV le⇩b ls⇩b)"
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 U⇩a le⇩a ls⇩a U⇩b le⇩b ls⇩b + ord⇩b: order_ow U⇩b le⇩b ls⇩b
for U⇩a :: "'a set" and le⇩a ls⇩a and U⇩b :: "'b set" and le⇩b ls⇩b

locale ord_order_dual_ow = ord_order_ow U⇩a le⇩a ls⇩a U⇩b le⇩b ls⇩b
for U⇩a :: "'a set" and le⇩a ls⇩a and U⇩b :: "'b set" and le⇩b ls⇩b
begin

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

end

locale preorder_order_ow =
ord_order_ow U⇩a le⇩a ls⇩a U⇩b le⇩b ls⇩b + ord⇩a: preorder_ow U⇩a le⇩a ls⇩a
for U⇩a :: "'a set" and le⇩a ls⇩a and U⇩b :: "'b set" and le⇩b ls⇩b
begin

sublocale preorder_pair_ow ..

end

locale preorder_order_dual_ow = preorder_order_ow U⇩a le⇩a ls⇩a U⇩b le⇩b ls⇩b
for U⇩a :: "'a set" and le⇩a ls⇩a and U⇩b :: "'b set" and le⇩b ls⇩b
begin

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

end

locale order_pair_ow =
preorder_order_ow U⇩a le⇩a ls⇩a U⇩b le⇩b ls⇩b + ord⇩a: order_ow U⇩a le⇩a ls⇩a
for U⇩a :: "'a set" and le⇩a ls⇩a and U⇩b :: "'b set" and le⇩b ls⇩b
begin

sublocale rev: order_pair_ow U⇩b le⇩b ls⇩b U⇩a le⇩a ls⇩a ..

end

locale order_pair_dual_ow = order_pair_ow U⇩a le⇩a ls⇩a U⇩b le⇩b ls⇩b
for U⇩a :: "'a set" and le⇩a ls⇩a and U⇩b :: "'b set" and le⇩b ls⇩b
begin

sublocale preorder_order_dual_ow ..
sublocale ord_dual: order_pair_ow U⇩a ‹(≤⇩a)› ‹(<⇩a)› U⇩b ‹(≥⇩b)› ‹(>⇩b)› ..
sublocale dual_ord: order_pair_ow U⇩a ‹(≥⇩a)› ‹(>⇩a)› U⇩b ‹(≤⇩b)› ‹(<⇩b)›
by unfold_locales (simp add: ord⇩a.antisym)
sublocale dual_dual: order_pair_ow U⇩a ‹(≥⇩a)› ‹(>⇩a)› U⇩b ‹(≥⇩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 =
(λle⇩a ls⇩a le⇩b ls⇩b. preorder_order_ow UNIV le⇩a ls⇩a UNIV le⇩b ls⇩b)"
unfolding preorder_order_def preorder_order_ow_def ud_with by simp

lemma order_pair_ow[ud_with]:
"order_pair = (λle⇩a ls⇩a le⇩b ls⇩b. order_pair_ow UNIV le⇩a ls⇩a UNIV le⇩b ls⇩b)"
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 U⇩a) and (?'b to U⇩b)
sbterms: (‹?ls⇩a::?'a ⇒ ?'a ⇒ bool› to ls⇩a)
and (‹?le⇩a::?'a ⇒ ?'a ⇒ bool› to le⇩a)
and (‹?ls⇩b::?'b ⇒ ?'b ⇒ bool› to ls⇩b)
and (‹?le⇩b::?'b ⇒ ?'b ⇒ bool› to le⇩b)
rewriting ctr_simps
substituting order_pair_ow_axioms
eliminating through (auto simp: mono_def bdd_def)
begin

tts_lemma strict_mono_mono:
assumes "∀x∈U⇩a. f x ∈ U⇩b" and "strict_mono⇩a⇩b f"
shows "mono⇩a⇩b f"
is order_pair.strict_mono_mono.

tts_lemma bdd_above_image_mono:
assumes "∀x∈U⇩a. f x ∈ U⇩b" and "A ⊆ U⇩a" and "mono⇩a⇩b f" and "ord⇩a.bdd_above A"
shows "ord⇩b.bdd_above (f ` A)"
is order_pair.bdd_above_image_mono.

tts_lemma bdd_below_image_mono:
assumes "∀x∈U⇩a. f x ∈ U⇩b" and "A ⊆ U⇩a" and "mono⇩a⇩b f" and "ord⇩a.bdd_below A"
shows "ord⇩b.bdd_below (f ` A)"
is order_pair.bdd_below_image_mono.

tts_lemma bdd_below_image_antimono:
assumes "∀x∈U⇩a. f x ∈ U⇩b"
and "A ⊆ U⇩a"
and "antimono⇩a⇩b f"
and "ord⇩a.bdd_above A"
shows "ord⇩b.bdd_below (f ` A)"
is order_pair.bdd_below_image_antimono.

tts_lemma bdd_above_image_antimono:
assumes "∀x∈U⇩a. f x ∈ U⇩b"
and "A ⊆ U⇩a"
and "antimono⇩a⇩b f"
and "ord⇩a.bdd_below A"
shows "ord⇩b.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 U⇩a le⇩a ls⇩a U⇩b le⇩b ls⇩b + ord⇩b: dense_order_ow U⇩b le⇩b ls⇩b
for U⇩a :: "'a set" and le⇩a ls⇩a and U⇩b :: "'b set" and le⇩b ls⇩b

locale ord_dense_order_dual_ow = ord_dense_order_ow U⇩a le⇩a ls⇩a U⇩b le⇩b ls⇩b
for U⇩a :: "'a set" and le⇩a ls⇩a and U⇩b :: "'b set" and le⇩b ls⇩b
begin

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

end

locale preorder_dense_order_ow =
ord_dense_order_ow U⇩a le⇩a ls⇩a U⇩b le⇩b ls⇩b + ord⇩a: preorder_ow U⇩a le⇩a ls⇩a
for U⇩a :: "'a set" and le⇩a ls⇩a and U⇩b :: "'b set" and le⇩b ls⇩b
begin

sublocale preorder_order_ow ..

end

locale preorder_dense_order_dual_ow =
preorder_dense_order_ow U⇩a le⇩a ls⇩a U⇩b le⇩b ls⇩b
for U⇩a :: "'a set" and le⇩a ls⇩a and U⇩b :: "'b set" and le⇩b ls⇩b
begin

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

end

locale order_dense_order_ow =
preorder_dense_order_ow U⇩a le⇩a ls⇩a U⇩b le⇩b ls⇩b + ord⇩a: order_ow U⇩a le⇩a ls⇩a
for U⇩a :: "'a set" and le⇩a ls⇩a and U⇩b :: "'b set" and le⇩b ls⇩b
begin

sublocale order_pair_ow ..

end

locale order_dense_order_dual_ow = order_dense_order_ow U⇩a le⇩a ls⇩a U⇩b le⇩b ls⇩b
for U⇩a :: "'a set" and le⇩a ls⇩a and U⇩b :: "'b set" and le⇩b ls⇩b
begin

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

end

locale dense_order_pair_ow =
order_dense_order_ow U⇩a le⇩a ls⇩a U⇩b le⇩b ls⇩b + ord⇩a: dense_order_ow U⇩a le⇩a ls⇩a
for U⇩a :: "'a set" and le⇩a ls⇩a and U⇩b :: "'b set" and le⇩b ls⇩b

locale dense_order_pair_dual_ow = dense_order_pair_ow U⇩a le⇩a ls⇩a U⇩b le⇩b ls⇩b
for U⇩a :: "'a set" and le⇩a ls⇩a and U⇩b :: "'b set" and le⇩b ls⇩b
begin

sublocale order_dense_order_dual_ow ..
sublocale ord_dual: dense_order_pair_ow U⇩a ‹(≤⇩a)› ‹(<⇩a)› U⇩b ‹(≥⇩b)› ‹(>⇩b)› ..
sublocale dual_ord: dense_order_pair_ow U⇩a ‹(≥⇩a)› ‹(>⇩a)› U⇩b ‹(≤⇩b)› ‹(<⇩b)›
using ord⇩a.dense by unfold_locales auto
sublocale dual_dual: dense_order_pair_ow U⇩a ‹(≥⇩a)› ‹(>⇩a)› U⇩b ‹(≥⇩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 =
(λle⇩a ls⇩a le⇩b ls⇩b. preorder_dense_order_ow UNIV le⇩a ls⇩a UNIV le⇩b ls⇩b)"
unfolding preorder_dense_order_def preorder_dense_order_ow_def ud_with
by simp

lemma order_dense_order_ow[ud_with]:
"order_dense_order =
(λle⇩a ls⇩a le⇩b ls⇩b. order_dense_order_ow UNIV le⇩a ls⇩a UNIV le⇩b ls⇩b)"
unfolding order_dense_order_def order_dense_order_ow_def ud_with by simp

lemma dense_order_pair_ow[ud_with]:
"dense_order_pair =
(λle⇩a ls⇩a le⇩b ls⇩b. dense_order_pair_ow UNIV le⇩a ls⇩a UNIV le⇩b ls⇩b)"
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```