# Theory SML_Linorders

```(* Title: Examples/SML_Relativization/Lattices/SML_Linorders.thy
Author: Mihails Milehins
*)
section‹Relativization of the results about linear orders›
theory SML_Linorders
imports SML_Semilattices
begin

subsection‹Linear orders›

subsubsection‹Definitions and further properties›

locale linorder_ow = order_ow +
assumes linear: "⟦ x ∈ U; y ∈ U ⟧ ⟹ x ≤⇩o⇩w y ∨ y ≤⇩o⇩w x"
begin

sublocale min:
semilattice_order_ow U ‹(λx y. (with (≤⇩o⇩w) : «min» x y))› ‹(≤⇩o⇩w)› ‹(<⇩o⇩w)›
apply unfold_locales
subgoal unfolding min.with_def by simp
subgoal by (metis linear order_trans min.with_def)
subgoal unfolding min.with_def by (auto dest: linear simp: antisym)
subgoal unfolding min.with_def by simp
subgoal unfolding min.with_def by (simp add: eq_iff)
subgoal unfolding min.with_def by (simp add: less_le)
done

sublocale max:
semilattice_order_ow U ‹(λx y. (with (≤⇩o⇩w) : «max» x y))› ‹(≥⇩o⇩w)› ‹(>⇩o⇩w)›
apply unfold_locales
subgoal unfolding max.with_def by simp
subgoal by (metis linear order_trans max.with_def)
subgoal unfolding max.with_def by (auto dest: linear simp: antisym)
subgoal unfolding max.with_def by simp
subgoal unfolding max.with_def by (auto dest: linear simp: antisym)
subgoal unfolding max.with_def by (auto dest: linear simp: less_le_not_le)
done

end

locale ord_linorder_ow =
ord?: ord_ow U⇩1 le⇩1 ls⇩1 + lo?: linorder_ow U⇩2 le⇩2 ls⇩2
for U⇩1 :: "'ao set" and le⇩1 ls⇩1 and U⇩2 :: "'bo set" and le⇩2 ls⇩2
begin

sublocale ord_order_ow ..

end

locale preorder_linorder_ow =
po?: preorder_ow U⇩1 le⇩1 ls⇩1 + lo?: linorder_ow U⇩2 le⇩2 ls⇩2
for U⇩1 :: "'ao set" and le⇩1 ls⇩1 and U⇩2 :: "'bo set" and le⇩2 ls⇩2
begin

sublocale preorder_order_ow ..

end

locale order_linorder_ow =
order?: order_ow U⇩1 le⇩1 ls⇩1 + lo?: linorder_ow U⇩2 le⇩2 ls⇩2
for U⇩1 :: "'ao set" and le⇩1 ls⇩1 and U⇩2 :: "'bo set" and le⇩2 ls⇩2
begin

sublocale order_pair_ow ..

end

locale linorder_pair_ow =
lo⇩1?: linorder_ow U⇩1 le⇩1 ls⇩1 + lo⇩2?: linorder_ow U⇩2 le⇩2 ls⇩2
for U⇩1 :: "'ao set" and le⇩1 ls⇩1 and U⇩2 :: "'bo set" and le⇩2 ls⇩2
begin

sublocale order_linorder_ow ..

end

subsubsection‹Transfer rules›

context
includes lifting_syntax
begin

lemma linorder_transfer[transfer_rule]:
assumes [transfer_rule]: "bi_unique A" "right_total A"
shows
"((A ===> A ===> (=)) ===> (A ===> A ===> (=)) ===> (=))
(linorder_ow (Collect (Domainp A))) class.linorder"
unfolding
linorder_ow_def class.linorder_def
linorder_ow_axioms_def class.linorder_axioms_def
apply transfer_prover_start
apply transfer_step+
by simp

end

subsubsection‹Relativization›

context linorder_ow
begin

tts_context
tts: (?'a to U)
rewriting ctr_simps
substituting linorder_ow_axioms
eliminating through simp
begin

tts_lemma le_less_linear:
assumes "x ∈ U" and "y ∈ U"
shows "x ≤⇩o⇩w y ∨ y <⇩o⇩w x"
is linorder_class.le_less_linear.

tts_lemma not_less:
assumes "x ∈ U" and "y ∈ U"
shows "(¬ x <⇩o⇩w y) = (y ≤⇩o⇩w x)"
is linorder_class.not_less.

tts_lemma not_le:
assumes "x ∈ U" and "y ∈ U"
shows "(¬ x ≤⇩o⇩w y) = (y <⇩o⇩w x)"
is linorder_class.not_le.

tts_lemma lessThan_minus_lessThan:
assumes "n ∈ U" and "m ∈ U"
shows "{..<⇩o⇩wn} - {..<⇩o⇩wm} = (on U with (≤⇩o⇩w) (<⇩o⇩w) : {m..<n})"
is linorder_class.lessThan_minus_lessThan.

tts_lemma Ici_subset_Ioi_iff:
assumes "a ∈ U" and "b ∈ U"
shows "({a..⇩o⇩w} ⊆ {b<⇩o⇩w..}) = (b <⇩o⇩w a)"
is linorder_class.Ici_subset_Ioi_iff.

tts_lemma Iic_subset_Iio_iff:
assumes "a ∈ U" and "b ∈ U"
shows "({..⇩o⇩wa} ⊆ {..<⇩o⇩wb}) = (a <⇩o⇩w b)"
is linorder_class.Iic_subset_Iio_iff.

tts_lemma leI:
assumes "x ∈ U" and "y ∈ U" and "¬ x <⇩o⇩w y"
shows "y ≤⇩o⇩w x"
is linorder_class.leI.

tts_lemma not_le_imp_less:
assumes "y ∈ U" and "x ∈ U" and "¬ y ≤⇩o⇩w x"
shows "x <⇩o⇩w y"
is linorder_class.not_le_imp_less.

tts_lemma Int_atMost:
assumes "a ∈ U" and "b ∈ U"
shows "{..⇩o⇩wa} ∩ {..⇩o⇩wb} = {..⇩o⇩wmin a b}"
is linorder_class.Int_atMost.

tts_lemma lessThan_Int_lessThan:
assumes "a ∈ U" and "b ∈ U"
shows "{a<⇩o⇩w..} ∩ {b<⇩o⇩w..} = {max a b<⇩o⇩w..}"
is linorder_class.lessThan_Int_lessThan.

tts_lemma greaterThan_Int_greaterThan:
assumes "a ∈ U" and "b ∈ U"
shows "{..<⇩o⇩wa} ∩ {..<⇩o⇩wb} = {..<⇩o⇩wmin a b}"
is linorder_class.greaterThan_Int_greaterThan.

tts_lemma less_linear:
assumes "x ∈ U" and "y ∈ U"
shows "x <⇩o⇩w y ∨ x = y ∨ y <⇩o⇩w x"
is linorder_class.less_linear.

tts_lemma Int_atLeastAtMostR2:
assumes "a ∈ U" and "c ∈ U" and "d ∈ U"
shows "{a..⇩o⇩w} ∩ {c..⇩o⇩wd} = {max a c..⇩o⇩wd}"
is linorder_class.Int_atLeastAtMostR2.

tts_lemma Int_atLeastAtMostR1:
assumes "b ∈ U" and "c ∈ U" and "d ∈ U"
shows "{..⇩o⇩wb} ∩ {c..⇩o⇩wd} = {c..⇩o⇩wmin b d}"
is linorder_class.Int_atLeastAtMostR1.

tts_lemma Int_atLeastAtMostL2:
assumes "a ∈ U" and "b ∈ U" and "c ∈ U"
shows "{a..⇩o⇩wb} ∩ {c..⇩o⇩w} = {max a c..⇩o⇩wb}"
is linorder_class.Int_atLeastAtMostL2.

tts_lemma Int_atLeastAtMostL1:
assumes "a ∈ U" and "b ∈ U" and "d ∈ U"
shows "{a..⇩o⇩wb} ∩ {..⇩o⇩wd} = {a..⇩o⇩wmin b d}"
is linorder_class.Int_atLeastAtMostL1.

tts_lemma neq_iff:
assumes "x ∈ U" and "y ∈ U"
shows "(x ≠ y) = (x <⇩o⇩w y ∨ y <⇩o⇩w x)"
is linorder_class.neq_iff.

tts_lemma not_less_iff_gr_or_eq:
assumes "x ∈ U" and "y ∈ U"
shows "(¬ x <⇩o⇩w y) = (y <⇩o⇩w x ∨ x = y)"
is linorder_class.not_less_iff_gr_or_eq.

tts_lemma max_min_distrib2:
assumes "a ∈ U" and "b ∈ U" and "c ∈ U"
shows "max a (min b c) = min (max a b) (max a c)"
is linorder_class.max_min_distrib2.

tts_lemma max_min_distrib1:
assumes "b ∈ U" and "c ∈ U" and "a ∈ U"
shows "max (min b c) a = min (max b a) (max c a)"
is linorder_class.max_min_distrib1.

tts_lemma min_max_distrib2:
assumes "a ∈ U" and "b ∈ U" and "c ∈ U"
shows "min a (max b c) = max (min a b) (min a c)"
is linorder_class.min_max_distrib2.

tts_lemma min_max_distrib1:
assumes "b ∈ U" and "c ∈ U" and "a ∈ U"
shows "min (max b c) a = max (min b a) (min c a)"
is linorder_class.min_max_distrib1.

tts_lemma atLeastAtMost_diff_ends:
assumes "a ∈ U" and "b ∈ U"
shows "{a..⇩o⇩wb} - {a, b} = {a<⇩o⇩w..<⇩o⇩wb}"
is linorder_class.atLeastAtMost_diff_ends.

tts_lemma less_max_iff_disj:
assumes "z ∈ U" and "x ∈ U" and "y ∈ U"
shows "(z <⇩o⇩w max x y) = (z <⇩o⇩w x ∨ z <⇩o⇩w y)"
is linorder_class.less_max_iff_disj.

tts_lemma min_less_iff_conj:
assumes "z ∈ U" and "x ∈ U" and "y ∈ U"
shows "(z <⇩o⇩w min x y) = (z <⇩o⇩w x ∧ z <⇩o⇩w y)"
is linorder_class.min_less_iff_conj.

tts_lemma max_less_iff_conj:
assumes "x ∈ U" and "y ∈ U" and "z ∈ U"
shows "(max x y <⇩o⇩w z) = (x <⇩o⇩w z ∧ y <⇩o⇩w z)"
is linorder_class.max_less_iff_conj.

tts_lemma min_less_iff_disj:
assumes "x ∈ U" and "y ∈ U" and "z ∈ U"
shows "(min x y <⇩o⇩w z) = (x <⇩o⇩w z ∨ y <⇩o⇩w z)"
is linorder_class.min_less_iff_disj.

tts_lemma le_max_iff_disj:
assumes "z ∈ U" and "x ∈ U" and "y ∈ U"
shows "(z ≤⇩o⇩w max x y) = (z ≤⇩o⇩w x ∨ z ≤⇩o⇩w y)"
is linorder_class.le_max_iff_disj.

tts_lemma min_le_iff_disj:
assumes "x ∈ U" and "y ∈ U" and "z ∈ U"
shows "(min x y ≤⇩o⇩w z) = (x ≤⇩o⇩w z ∨ y ≤⇩o⇩w z)"
is linorder_class.min_le_iff_disj.

tts_lemma antisym_conv3:
assumes "y ∈ U" and "x ∈ U" and "¬ y <⇩o⇩w x"
shows "(¬ x <⇩o⇩w y) = (x = y)"
is linorder_class.antisym_conv3.

tts_lemma Int_atLeastAtMost:
assumes "a ∈ U" and "b ∈ U" and "c ∈ U" and "d ∈ U"
shows "{a..⇩o⇩wb} ∩ {c..⇩o⇩wd} = {max a c..⇩o⇩wmin b d}"
is linorder_class.Int_atLeastAtMost.

tts_lemma Int_atLeastLessThan:
assumes "a ∈ U" and "b ∈ U" and "c ∈ U" and "d ∈ U"
shows
"(on U with (≤⇩o⇩w) (<⇩o⇩w) : {a..<b}) ∩ (on U with (≤⇩o⇩w) (<⇩o⇩w) : {c..<d}) =
(on U with (≤⇩o⇩w) (<⇩o⇩w) : {(max a c)..<(min b d)})"
is linorder_class.Int_atLeastLessThan.

tts_lemma Int_greaterThanAtMost:
assumes "a ∈ U" and "b ∈ U" and "c ∈ U" and "d ∈ U"
shows "{a<⇩o⇩w..b} ∩ {c<⇩o⇩w..d} = {max a c<⇩o⇩w..min b d}"
is linorder_class.Int_greaterThanAtMost.

tts_lemma Int_greaterThanLessThan:
assumes "a ∈ U" and "b ∈ U" and "c ∈ U" and "d ∈ U"
shows "{a<⇩o⇩w..<⇩o⇩wb} ∩ {c<⇩o⇩w..<⇩o⇩wd} = {max a c<⇩o⇩w..<⇩o⇩wmin b d}"
is linorder_class.Int_greaterThanLessThan.

tts_lemma le_cases:
assumes "x ∈ U" and "y ∈ U" and "x ≤⇩o⇩w y ⟹ P" and "y ≤⇩o⇩w x ⟹ P"
shows P
is linorder_class.le_cases.

tts_lemma split_max:
assumes "i ∈ U" and "j ∈ U"
shows "P (max i j) = ((i ≤⇩o⇩w j ⟶ P j) ∧ (¬ i ≤⇩o⇩w j ⟶ P i))"
is linorder_class.split_max.

tts_lemma split_min:
assumes "i ∈ U" and "j ∈ U"
shows "P (min i j) = ((i ≤⇩o⇩w j ⟶ P i) ∧ (¬ i ≤⇩o⇩w j ⟶ P j))"
is linorder_class.split_min.

tts_lemma Ioc_subset_iff:
assumes "a ∈ U" and "b ∈ U" and "c ∈ U" and "d ∈ U"
shows "({a<⇩o⇩w..b} ⊆ {c<⇩o⇩w..d}) = (b ≤⇩o⇩w a ∨ b ≤⇩o⇩w d ∧ c ≤⇩o⇩w a)"
is linorder_class.Ioc_subset_iff.

tts_lemma atLeastLessThan_subset_iff:
assumes "a ∈ U"
and "b ∈ U"
and "c ∈ U"
and "d ∈ U"
and "(on U with (≤⇩o⇩w) (<⇩o⇩w) : {a..<b}) ⊆ (on U with (≤⇩o⇩w) (<⇩o⇩w) : {c..<d})"
shows "b ≤⇩o⇩w a ∨ b ≤⇩o⇩w d ∧ c ≤⇩o⇩w a"
is linorder_class.atLeastLessThan_subset_iff.

tts_lemma Ioc_inj:
assumes "a ∈ U" and "b ∈ U" and "c ∈ U" and "d ∈ U"
shows "({a<⇩o⇩w..b} = {c<⇩o⇩w..d}) = (b ≤⇩o⇩w a ∧ d ≤⇩o⇩w c ∨ a = c ∧ b = d)"
is linorder_class.Ioc_inj.

tts_lemma neqE:
assumes "x ∈ U"
and "y ∈ U"
and "x ≠ y"
and "x <⇩o⇩w y ⟹ R"
and "y <⇩o⇩w x ⟹ R"
shows R
is linorder_class.neqE.

tts_lemma Ioc_disjoint:
assumes "a ∈ U" and "b ∈ U" and "c ∈ U" and "d ∈ U"
shows
"({a<⇩o⇩w..b} ∩ {c<⇩o⇩w..d} = {}) = (b ≤⇩o⇩w a ∨ d ≤⇩o⇩w c ∨ b ≤⇩o⇩w c ∨ d ≤⇩o⇩w a)"
is linorder_class.Ioc_disjoint.

tts_lemma linorder_cases:
assumes "x ∈ U"
and "y ∈ U"
and "x <⇩o⇩w y ⟹ P"
and "x = y ⟹ P"
and "y <⇩o⇩w x ⟹ P"
shows P
is linorder_class.linorder_cases.

tts_lemma le_cases3:
assumes "x ∈ U"
and "y ∈ U"
and "z ∈ U"
and "⟦x ≤⇩o⇩w y; y ≤⇩o⇩w z⟧ ⟹ P"
and "⟦y ≤⇩o⇩w x; x ≤⇩o⇩w z⟧ ⟹ P"
and "⟦x ≤⇩o⇩w z; z ≤⇩o⇩w y⟧ ⟹ P"
and "⟦z ≤⇩o⇩w y; y ≤⇩o⇩w x⟧ ⟹ P"
and "⟦y ≤⇩o⇩w z; z ≤⇩o⇩w x⟧ ⟹ P"
and "⟦z ≤⇩o⇩w x; x ≤⇩o⇩w y⟧ ⟹ P"
shows P
is linorder_class.le_cases3.

end

end

subsection‹Dense linear orders›

subsubsection‹Definitions and further properties›

locale dense_linorder_ow = linorder_ow U le ls + dense_order_ow U le ls
for U :: "'ao set" and le (infix ‹≤⇩o⇩w› 50) and ls (infix ‹<⇩o⇩w› 50)

subsubsection‹Transfer rules›

context
includes lifting_syntax
begin

lemma dense_linorder_transfer[transfer_rule]:
assumes [transfer_rule]: "bi_unique A" "right_total A"
shows
"((A ===> A ===> (=)) ===> (A ===> A ===> (=))  ===> (=))
(dense_linorder_ow (Collect (Domainp A))) class.dense_linorder"
unfolding dense_linorder_ow_def class.dense_linorder_def
apply transfer_prover_start
apply transfer_step+
by auto

end

subsubsection‹Relativization›

context dense_linorder_ow
begin

tts_context
tts: (?'a to U)
rewriting ctr_simps
substituting dense_linorder_ow_axioms
eliminating through simp
begin

tts_lemma infinite_Icc:
assumes "a ∈ U" and "b ∈ U" and "a <⇩o⇩w b"
shows "infinite {a..⇩o⇩wb}"
is dense_linorder_class.infinite_Icc.

tts_lemma infinite_Ico:
assumes "a ∈ U" and "b ∈ U" and "a <⇩o⇩w b"
shows "infinite (on U with (≤⇩o⇩w) (<⇩o⇩w) : {a..<b})"
is dense_linorder_class.infinite_Ico.

tts_lemma infinite_Ioc:
assumes "a ∈ U" and "b ∈ U" and "a <⇩o⇩w b"
shows "infinite {a<⇩o⇩w..b}"
is dense_linorder_class.infinite_Ioc.

tts_lemma infinite_Ioo:
assumes "a ∈ U" and "b ∈ U" and "a <⇩o⇩w b"
shows "infinite {a<⇩o⇩w..<⇩o⇩wb}"
is dense_linorder_class.infinite_Ioo.

tts_lemma atLeastLessThan_subseteq_atLeastAtMost_iff:
assumes "a ∈ U" and "b ∈ U" and "c ∈ U" and "d ∈ U"
shows
"((on U with (≤⇩o⇩w) (<⇩o⇩w) : {a..<b}) ⊆ {c..⇩o⇩wd}) =
(a <⇩o⇩w b ⟶ b ≤⇩o⇩w d ∧ c ≤⇩o⇩w a)"
is dense_linorder_class.atLeastLessThan_subseteq_atLeastAtMost_iff.

tts_lemma greaterThanAtMost_subseteq_atLeastAtMost_iff:
assumes "a ∈ U" and "b ∈ U" and "c ∈ U" and "d ∈ U"
shows "({a<⇩o⇩w..b} ⊆ {c..⇩o⇩wd}) = (a <⇩o⇩w b ⟶ b ≤⇩o⇩w d ∧ c ≤⇩o⇩w a)"
is dense_linorder_class.greaterThanAtMost_subseteq_atLeastAtMost_iff.

tts_lemma greaterThanAtMost_subseteq_atLeastLessThan_iff:
assumes "a ∈ U"
and "b ∈ U"
and "c ∈ U"
and "d ∈ U"
shows "({a<⇩o⇩w..b} ⊆ (on U with (≤⇩o⇩w) (<⇩o⇩w) : {c..<d})) =
(a <⇩o⇩w b ⟶ b <⇩o⇩w d ∧ c ≤⇩o⇩w a)"
is dense_linorder_class.greaterThanAtMost_subseteq_atLeastLessThan_iff.

tts_lemma greaterThanLessThan_subseteq_atLeastAtMost_iff:
assumes "a ∈ U" and "b ∈ U" and "c ∈ U" and "d ∈ U"
shows "({a<⇩o⇩w..<⇩o⇩wb} ⊆ {c..⇩o⇩wd}) = (a <⇩o⇩w b ⟶ b ≤⇩o⇩w d ∧ c ≤⇩o⇩w a)"
is dense_linorder_class.greaterThanLessThan_subseteq_atLeastAtMost_iff.

tts_lemma greaterThanLessThan_subseteq_atLeastLessThan_iff:
assumes "a ∈ U" and "b ∈ U" and "c ∈ U" and "d ∈ U"
shows
"({a<⇩o⇩w..<⇩o⇩wb} ⊆ (on U with (≤⇩o⇩w) (<⇩o⇩w) : {c..<d})) =
(a <⇩o⇩w b ⟶ b ≤⇩o⇩w d ∧ c ≤⇩o⇩w a)"
is dense_linorder_class.greaterThanLessThan_subseteq_atLeastLessThan_iff.

tts_lemma greaterThanLessThan_subseteq_greaterThanAtMost_iff:
assumes "a ∈ U" and "b ∈ U" and "c ∈ U" and "d ∈ U"
shows "({a<⇩o⇩w..<⇩o⇩wb} ⊆ {c<⇩o⇩w..d}) = (a <⇩o⇩w b ⟶ b ≤⇩o⇩w d ∧ c ≤⇩o⇩w a)"
is dense_linorder_class.greaterThanLessThan_subseteq_greaterThanAtMost_iff.

tts_lemma greaterThanLessThan_subseteq_greaterThanLessThan:
assumes "a ∈ U" and "b ∈ U" and "c ∈ U" and "d ∈ U"
shows "({a<⇩o⇩w..<⇩o⇩wb} ⊆ {c<⇩o⇩w..<⇩o⇩wd}) = (a <⇩o⇩w b ⟶ b ≤⇩o⇩w d ∧ c ≤⇩o⇩w a)"
is dense_linorder_class.greaterThanLessThan_subseteq_greaterThanLessThan.

end

end

text‹\newpage›

end```