Theory SML_Simple_Orders

(* Title: Examples/SML_Relativization/Simple_Orders/SML_Simple_Orders.thy
   Author: Mihails Milehins
   Copyright 2021 (C) Mihails Milehins
*)
section‹Relativization of the results about orders›
theory SML_Simple_Orders
  imports 
    "../../Introduction"
    "../Foundations/SML_Relations"
    Complex_Main
begin



subsection‹Class class‹ord››


subsubsection‹Definitions and common properties›

locale ord_ow =
  fixes U :: "'ao set"
    and le :: "['ao, 'ao] ⇒ bool" (infix ‹≤ow› 50) 
    and ls :: "['ao, 'ao] ⇒ bool" (infix ‹<ow› 50)
begin

notation le (‹'(≤ow')›)
  and le (infix ‹≤ow› 50) 
  and ls (‹'(<ow')›) 
  and ls (infix ‹<ow› 50)

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

notation ge (‹'(≥ow')›) 
  and ge (infix ‹≥ow› 50) 
  and gt (‹'(>ow')›) 
  and gt (infix ‹>ow› 50)

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

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

end

locale ord_pair_ow = ord1: ord_ow U1 le1 ls1 + ord2: ord_ow U2 le2 ls2
  for U1 :: "'ao set" and le1 ls1 and U2 :: "'bo set" and le2 ls2
begin

notation le1 (‹'(≤ow.1')›)
  and le1 (infix ‹≤ow.1› 50) 
  and ls1 (‹'(<ow.1')›) 
  and ls1 (infix ‹<ow.1› 50)
  and le2 (‹'(≤ow.2')›)
  and le2 (infix ‹≤ow.2› 50) 
  and ls2 (‹'(<ow.2')›) 
  and ls2 (infix ‹<ow.2› 50)

notation ord1.ge (‹'(≥ow.1')›) 
  and ord1.ge (infix ‹≥ow.1› 50) 
  and ord1.gt (‹'(>ow.1')›) 
  and ord1.gt (infix ‹>ow.1› 50)
  and ord2.ge (‹'(≥ow.2')›) 
  and ord2.ge (infix ‹≥ow.2› 50) 
  and ord2.gt (‹'(>ow.2')›) 
  and ord2.gt (infix ‹>ow.2› 50)

end

ud ‹ord.lessThan› (‹(with _ : ({..<_}))› [1000] 10)
ud lessThan' ‹lessThan› 
ud ‹ord.atMost› (‹(with _ : ({.._}))› [1000] 10) 
ud atMost' ‹atMost› 
ud ‹ord.greaterThan› (‹(with _ : ({_<..}))› [1000] 10) 
ud greaterThan' ‹greaterThan› 
ud ‹ord.atLeast› (‹(with _ : ({_..}))› [1000] 10) 
ud atLeast' ‹atLeast› 
ud ‹ord.greaterThanLessThan› (‹(with _ : ({_<..<_}))› [1000, 999, 1000] 10) 
ud greaterThanLessThan' ‹greaterThanLessThan› 
ud ‹ord.atLeastLessThan› (‹(with _ _ : ({_..<_}))› [1000, 999, 1000, 1000] 10)
ud atLeastLessThan' ‹atLeastLessThan› 
ud ‹ord.greaterThanAtMost› (‹(with _ _ : ({_<.._}))› [1000, 999, 1000, 999] 10) 
ud greaterThanAtMost' ‹greaterThanAtMost› 
ud ‹ord.atLeastAtMost› (‹(with _ : ({_.._}))› [1000, 1000, 1000] 10) 
ud atLeastAtMost' ‹atLeastAtMost› 
ud ‹ord.min› (‹(with _ : «min» _ _)› [1000, 1000, 999] 10)
ud min' ‹min› 
ud ‹ord.max› (‹(with _ : «max» _ _)› [1000, 1000, 999] 10)
ud max' ‹max›

ctr relativization
  synthesis ctr_simps
  assumes [transfer_domain_rule, transfer_rule]: "Domainp A = (λx. x ∈ U)"
    and [transfer_rule]: "right_total A" 
  trp (?'a A)
  in lessThan_ow: lessThan.with_def 
    (‹(on _ with _ : ({..<_}))› [1000, 1000, 1000] 10) 
    and atMost_ow: atMost.with_def 
      (‹(on _ with _ : ({.._}))› [1000, 1000, 1000] 10) 
    and greaterThan_ow: greaterThan.with_def
      (‹(on _ with _: ({_<..}))› [1000, 1000, 1000] 10) 
    and atLeast_ow: atLeast.with_def
      (‹(on _ with _ : ({_..}))› [1000, 1000, 1000] 10) 

ctr relativization
  synthesis ctr_simps
  assumes [transfer_domain_rule, transfer_rule]: "Domainp A = (λx. x ∈ U)"
    and [transfer_rule]: "bi_unique A" "right_total A" 
  trp (?'a A)
  in greaterThanLessThan_ow: greaterThanLessThan.with_def 
      (‹(on _ with _ : ({_<..<_}))› [1000, 1000, 1000, 1000] 10) 
    and atLeastLessThan_ow: atLeastLessThan.with_def 
      (‹(on _ with _ _ : ({_..<_}))› [1000, 1000, 999, 1000, 1000] 10)
    and greaterThanAtMost_ow: greaterThanAtMost.with_def 
      (‹(on _ with _ _ : ({_<.._}))› [1000, 1000, 999, 1000, 1000] 10) 
    and atLeastAtMost_ow: atLeastAtMost.with_def 
      (‹(on _ with _ : ({_.._}))› [1000, 1000, 1000, 1000] 10)

ctr parametricity
  in min_ow: min.with_def
    and max_ow: max.with_def

context ord_ow
begin

abbreviation lessThan :: "'ao ⇒ 'ao set" ("(1{..<ow_})") 
  where "{..<ow u} ≡ on U with (<ow) : {..<u}"
abbreviation atMost :: "'ao ⇒ 'ao set" ("(1{..ow_})") 
  where "{..ow u} ≡ on U with (≤ow) : {..u}"
abbreviation greaterThan :: "'ao ⇒ 'ao set" ("(1{_<ow..})")  
  where "{l<ow..} ≡ on U with (<ow) : {l<..}"
abbreviation atLeast :: "'ao ⇒ 'ao set" ("(1{_..ow})") 
  where "atLeast l ≡ on U with (≤ow) : {l..}"
abbreviation greaterThanLessThan :: "'ao ⇒ 'ao ⇒ 'ao set" ("(1{_<ow..<ow_})")
  where "{l<ow..<owu} ≡ on U with (<ow) : {l<..<u}"
abbreviation atLeastLessThan :: "'ao ⇒ 'ao ⇒ 'ao set" ("(1{_..<ow_})")
  where "{l..<ow u} ≡ on U with (≤ow) (<ow) : {l<..u}"
abbreviation greaterThanAtMost :: "'ao ⇒ 'ao ⇒ 'ao set" ("(1{_<ow.._})")
  where "{l<ow..u}  ≡ on U with (≤ow) (<ow) : {l<..u}"
abbreviation atLeastAtMost :: "'ao ⇒ 'ao ⇒ 'ao set" ("(1{_..ow_})")
  where "{l..owu} ≡ on U with (≤ow) : {l..u}"
abbreviation min :: "'ao ⇒ 'ao ⇒ 'ao" where "min ≡ min.with (≤ow)"
abbreviation max :: "'ao ⇒ 'ao ⇒ 'ao" where "max ≡ max.with (≤ow)"

end

context ord_pair_ow
begin

notation ord1.lessThan ("(1{..<ow.1_})") 
notation ord1.atMost ("(1{..ow.1_})") 
notation ord1.greaterThan ("(1{_<ow.1..})")  
notation ord1.atLeast ("(1{_..ow.1})") 
notation ord1.greaterThanLessThan ("(1{_<ow.1..<ow.1_})")
notation ord1.atLeastLessThan ("(1{_..<ow.1_})")
notation ord1.greaterThanAtMost ("(1{_<ow.1.._})")
notation ord1.atLeastAtMost ("(1{_..ow.1_})")

notation ord2.lessThan ("(1{..<ow.2_})") 
notation ord2.atMost ("(1{..ow.2_})") 
notation ord2.greaterThan ("(1{_<ow.2..})")  
notation ord2.atLeast ("(1{_..ow.2})") 
notation ord2.greaterThanLessThan ("(1{_<ow.2..<ow.2_})")
notation ord2.atLeastLessThan ("(1{_..<ow.2_})")
notation ord2.greaterThanAtMost ("(1{_<ow.2.._})")
notation ord2.atLeastAtMost ("(1{_..ow.2_})")

end



subsection‹Preorders›


subsubsection‹Definitions and common properties›

locale partial_preordering_ow =
  fixes U :: "'ao set"
    and le :: "'ao ⇒ 'ao ⇒ bool" (infix "≤ow" 50)
  assumes refl: "a ∈ U ⟹ a ≤ow a"
    and trans: "⟦ a ∈ U; b ∈ U; c ∈ U; a ≤ow b; b ≤ow c ⟧ ⟹ a ≤ow c"
begin

notation le (infix "≤ow" 50)

end

locale preordering_ow = partial_preordering_ow U le 
  for U :: "'ao set"
    and le :: "'ao ⇒ 'ao ⇒ bool" (infix "≤ow" 50) +
  fixes ls :: ‹'ao ⇒ 'ao ⇒ bool› (infix "<ow" 50)
  assumes strict_iff_not: 
    "⟦ a ∈ U; b ∈ U ⟧ ⟹ a <ow b ⟷ a ≤ow b ∧ ¬ b ≤ow a"

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

sublocale 
  order: preordering_ow U ‹(≤ow)› ‹(<ow)› + 
  dual_order: preordering_ow U ‹(≥ow)› ‹(>ow)›
  apply unfold_locales
  subgoal by auto
  subgoal by (meson order_trans)
  subgoal using less_le_not_le by simp
  subgoal by (meson order_trans)
  subgoal by (metis less_le_not_le)
  done

end

locale ord_preorder_ow = 
  ord1: ord_ow U1 le1 ls1 + ord2: preorder_ow U2 le2 ls2
  for U1 :: "'ao set" and le1 ls1 and U2 :: "'bo set" and le2 ls2
begin

sublocale ord_pair_ow .

end

locale preorder_pair_ow = 
  ord1: preorder_ow U1 le1 ls1 + ord2: preorder_ow U2 le2 ls2
  for U1 :: "'ao set" and le1 and ls1 and U2 :: "'bo set" and le2 and ls2
begin

sublocale ord_preorder_ow ..

end

ud ‹preordering_bdd.bdd›
ud ‹preorder.bdd_above›
ud bdd_above' ‹bdd_above› 
ud ‹preorder.bdd_below› 
ud bdd_below' ‹bdd_below› 

ctr relativization
  synthesis ctr_simps
  assumes [transfer_domain_rule, transfer_rule]: "Domainp A = (λx. x ∈ U)"
    and [transfer_rule]: "right_total A"
  trp (?'a A)
  in bdd_ow: bdd.with_def
    (‹(on _ with _ : «bdd» _)› [1000, 1000, 1000] 10)
    and bdd_above_ow: bdd_above.with_def
    (‹(on _ with _ : «bdd'_above» _)› [1000, 1000, 1000] 10)
    and bdd_below_ow: bdd_below.with_def
    (‹(on _ with _ : «bdd'_below» _)› [1000, 1000, 1000] 10)

declare bdd.with[ud_with del]

context preorder_ow
begin

abbreviation bdd_above :: "'ao set ⇒ bool" 
  where "bdd_above ≡ bdd_above_ow U (≤ow)"
abbreviation bdd_below :: "'ao set ⇒ bool" 
  where "bdd_below ≡ bdd_below_ow U (≤ow)"

end


subsubsection‹Transfer rules›

context
  includes lifting_syntax
begin

lemma partial_preordering_transfer[transfer_rule]:
  assumes [transfer_rule]: "right_total A"
  shows 
    "((A ===> A ===> (=)) ===> (=))
      (partial_preordering_ow (Collect (Domainp A))) partial_preordering"
  unfolding partial_preordering_ow_def partial_preordering_def
  apply transfer_prover_start
  apply transfer_step+
  by blast

lemma preordering_transfer[transfer_rule]:
  assumes [transfer_rule]: "right_total A"
  shows 
    "((A ===> A ===> (=)) ===> (A ===> A ===> (=)) ===> (=))
      (preordering_ow (Collect (Domainp A))) preordering"
  unfolding 
    preordering_ow_def preordering_ow_axioms_def 
    preordering_def preordering_axioms_def
  apply transfer_prover_start
  apply transfer_step+
  by blast

lemma preorder_transfer[transfer_rule]:
  assumes [transfer_rule]: "right_total A"
  shows 
    "((A ===> A ===> (=)) ===> (A ===> A ===> (=))  ===> (=)) 
      (preorder_ow (Collect (Domainp A))) class.preorder"
  unfolding preorder_ow_def class.preorder_def
  apply transfer_prover_start
  apply transfer_step+
  by blast

end


subsubsection‹Relativization›

context preordering_ow
begin

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

tts_lemma strict_implies_order:
  assumes "a ∈ U" and "b ∈ U" and "a <ow b"
  shows "a ≤ow b"
    is preordering.strict_implies_order.

tts_lemma irrefl:
  assumes "a ∈ U"
  shows "¬a <ow a"
    is preordering.irrefl.

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

tts_lemma strict_trans1:
  assumes "a ∈ U" and "b ∈ U" and "c ∈ U" and "a ≤ow b" and "b <ow c"
  shows "a <ow c"
    is preordering.strict_trans1.

tts_lemma strict_trans2:
  assumes "a ∈ U" and "b ∈ U" and "c ∈ U" and "a <ow b" and "b ≤ow c"
  shows "a <ow c"
    is preordering.strict_trans2.

tts_lemma strict_trans:
  assumes "a ∈ U" and "b ∈ U" and "c ∈ U" and "a <ow b" and "b <ow c"
  shows "a <ow c"
    is preordering.strict_trans.

end

end

context preorder_ow
begin

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

tts_lemma less_irrefl:
  assumes "x ∈ U"
  shows "¬ x <ow x"
  is preorder_class.less_irrefl.
    
tts_lemma bdd_below_Ioc:
  assumes "a ∈ U" and "b ∈ U"
  shows "bdd_below {a<ow..b}"
  is preorder_class.bdd_below_Ioc.
    
tts_lemma bdd_above_Ioc:
  assumes "a ∈ U" and "b ∈ U"
  shows "bdd_above {a<ow..b}"
    is preorder_class.bdd_above_Ioc.

tts_lemma bdd_above_Iic:
  assumes "b ∈ U"
  shows "bdd_above {..owb}"
    is preorder_class.bdd_above_Iic.

tts_lemma bdd_above_Iio:
  assumes "b ∈ U"
  shows "bdd_above {..<owb}"
    is preorder_class.bdd_above_Iio.

tts_lemma bdd_below_Ici:
  assumes "a ∈ U"
  shows "bdd_below {a..ow}"
    is preorder_class.bdd_below_Ici.

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

tts_lemma bdd_above_Icc:
  assumes "a ∈ U" and "b ∈ U"
  shows "bdd_above {a..owb}"
    is preorder_class.bdd_above_Icc.

tts_lemma bdd_above_Ioo:
  assumes "a ∈ U" and "b ∈ U"
  shows "bdd_above {a<ow..<owb}"
    is preorder_class.bdd_above_Ioo.

tts_lemma bdd_below_Icc:
  assumes "a ∈ U" and "b ∈ U"
  shows "bdd_below {a..owb}"
    is preorder_class.bdd_below_Icc.

tts_lemma bdd_below_Ioo:
  assumes "a ∈ U" and "b ∈ U"
  shows "bdd_below {a<ow..<owb}"
    is preorder_class.bdd_below_Ioo.

tts_lemma bdd_above_Ico:
  assumes "a ∈ U" and "b ∈ U"
  shows "bdd_above (on U with (≤ow) (<ow) : {a..<b})"
    is preorder_class.bdd_above_Ico.

tts_lemma bdd_below_Ico:
  assumes "a ∈ U" and "b ∈ U"
  shows "bdd_below (on U with (≤ow) (<ow) : {a..<b})"
    is preorder_class.bdd_below_Ico.

tts_lemma Ioi_le_Ico:
  assumes "a ∈ U"
  shows "{a<ow..} ⊆ {a..ow}"
    is preorder_class.Ioi_le_Ico.

tts_lemma eq_refl:
  assumes "y ∈ U" and "x = y"
  shows "x ≤ow y"
    is preorder_class.eq_refl.

tts_lemma less_imp_le:
  assumes "x ∈ U" and "y ∈ U" and "x <ow y"
  shows "x ≤ow y"
    is preorder_class.less_imp_le.

tts_lemma less_not_sym:
  assumes "x ∈ U" and "y ∈ U" and "x <ow y"
  shows "¬ y <ow x"
    is preorder_class.less_not_sym.

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

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

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

tts_lemma less_trans:
  assumes "x ∈ U" and "y ∈ U" and "z ∈ U" and "x <ow y" and "y <ow z"
  shows "x <ow z"
    is preorder_class.less_trans.

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

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

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

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

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

tts_lemma bdd_above_Int1:
  assumes "A ⊆ U" and "B ⊆ U" and "bdd_above A"
  shows "bdd_above (A ∩ B)"
    is preorder_class.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_class.bdd_above_Int2.

tts_lemma bdd_below_Int1:
  assumes "A ⊆ U" and "B ⊆ U" and "bdd_below A"
  shows "bdd_below (A ∩ B)"
    is preorder_class.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_class.bdd_below_Int2.

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

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

tts_lemma atLeastAtMost_subseteq_atLeastLessThan_iff:
  assumes "a ∈ U" and "b ∈ U" and "c ∈ U" and "d ∈ U"
  shows "({a..owb} ⊆ (on U with (≤ow) (<ow) : {c..<d})) = 
    (a ≤ow b ⟶ b <ow d ∧ c ≤ow a)"
    is preorder_class.atLeastAtMost_subseteq_atLeastLessThan_iff.

tts_lemma atMost_subset_iff:
  assumes "x ∈ U" and "y ∈ U"
  shows "({..owx} ⊆ {..owy}) = (x ≤ow y)"
    is Set_Interval.atMost_subset_iff.

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

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

tts_lemma atLeastatMost_psubset_iff:
  assumes "a ∈ U" and "b ∈ U" and "c ∈ U" and "d ∈ U"
  shows 
    "({a..owb} ⊂ {c..owd}) = 
      (c ≤ow d ∧ (¬ a ≤ow b ∨ c ≤ow a ∧ b ≤ow d ∧ (c <ow a ∨ b <ow d)))"
    is preorder_class.atLeastatMost_psubset_iff.

tts_lemma not_empty_eq_Iic_eq_empty:
  assumes "h ∈ U"
  shows "{} ≠ {..owh}"
    is preorder_class.not_empty_eq_Iic_eq_empty.
    
tts_lemma atLeastatMost_subset_iff:
  assumes "a ∈ U" and "b ∈ U" and "c ∈ U" and "d ∈ U"
  shows "({a..owb} ⊆ {c..owd}) = (¬ a ≤ow b ∨ b ≤ow d ∧ c ≤ow a)"
    is preorder_class.atLeastatMost_subset_iff.

tts_lemma Icc_subset_Ici_iff:
  assumes "l ∈ U" and "h ∈ U" and "l' ∈ U"
  shows "({l..owh} ⊆ {l'..ow}) = (¬ l ≤ow h ∨ l' ≤ow l)"
    is preorder_class.Icc_subset_Ici_iff.
    
tts_lemma Icc_subset_Iic_iff:
  assumes "l ∈ U" and "h ∈ U" and "h' ∈ U"
  shows "({l..owh} ⊆ {..owh'}) = (¬ l ≤ow h ∨ h ≤ow h')"
    is preorder_class.Icc_subset_Iic_iff.

tts_lemma not_empty_eq_Ici_eq_empty:
  assumes "l ∈ U"
  shows "{} ≠ {l..ow}"
  is preorder_class.not_empty_eq_Ici_eq_empty.
    
tts_lemma not_Ici_eq_empty:
  assumes "l ∈ U"
  shows "{l..ow} ≠ {}"
is preorder_class.not_Ici_eq_empty.
    
tts_lemma not_Iic_eq_empty:
  assumes "h ∈ U"
  shows "{..owh} ≠ {}"
    is preorder_class.not_Iic_eq_empty.

tts_lemma atLeastatMost_empty_iff2:
  assumes "a ∈ U" and "b ∈ U"
  shows "({} = {a..owb}) = (¬ a ≤ow b)"
    is preorder_class.atLeastatMost_empty_iff2.
    
tts_lemma atLeastLessThan_empty_iff2:
  assumes "a ∈ U" and "b ∈ U"
  shows "({} = (on U with (≤ow) (<ow) : {a..<b})) = (¬ a <ow b)"
    is preorder_class.atLeastLessThan_empty_iff2.
    
tts_lemma greaterThanAtMost_empty_iff2:
  assumes "k ∈ U" and "l ∈ U"
  shows "({} = {k<ow..l}) = (¬ k <ow l)"
    is preorder_class.greaterThanAtMost_empty_iff2.
    
tts_lemma atLeastatMost_empty_iff:
  assumes "a ∈ U" and "b ∈ U"
  shows "({a..owb} = {}) = (¬ a ≤ow b)"
    is preorder_class.atLeastatMost_empty_iff.
    
tts_lemma atLeastLessThan_empty_iff:
  assumes "a ∈ U" and "b ∈ U"
  shows "((on U with (≤ow) (<ow) : {a..<b}) = {}) = (¬ a <ow b)"
    is preorder_class.atLeastLessThan_empty_iff.
    
tts_lemma greaterThanAtMost_empty_iff:
  assumes "k ∈ U" and "l ∈ U"
  shows "({k<ow..l} = {}) = (¬ k <ow l)"
    is preorder_class.greaterThanAtMost_empty_iff.

end

tts_context
  tts: (?'a to U)
  substituting preorder_ow_axioms
begin

tts_lemma bdd_above_empty:
  assumes "U ≠ {}"
  shows "bdd_above {}"
    is preorder_class.bdd_above_empty.
    
tts_lemma bdd_below_empty:
  assumes "U ≠ {}"
  shows "bdd_below {}"
    is preorder_class.bdd_below_empty.
    
end

tts_context
  tts: (?'a to U) and (?'b to ‹U2::'a set›)
  rewriting ctr_simps
  substituting preorder_ow_axioms
  eliminating through (auto intro: bdd_above_empty bdd_below_empty)
begin

tts_lemma bdd_belowI2:
  assumes "A ⊆ U2"
    and "m ∈ U"
    and "∀x∈U2. f x ∈ U"
    and "⋀x. x ∈ A ⟹ m ≤ow f x"
  shows "bdd_below (f ` A)"
    given preorder_class.bdd_belowI2
  by blast

tts_lemma bdd_aboveI2:
  assumes "A ⊆ U2"
    and "∀x∈U2. f x ∈ U"
    and "M ∈ U"
    and "⋀x. x ∈ A ⟹ f x ≤ow M"
  shows "bdd_above (f ` A)"
    given preorder_class.bdd_aboveI2
  by blast
    
end

end



subsection‹Partial orders›


subsubsection‹Definitions and common properties›

locale ordering_ow = partial_preordering_ow U le 
  for U :: "'ao set" and le :: "'ao ⇒ 'ao ⇒ bool" (infix "≤ow" 50) +
  fixes ls :: "'ao ⇒ 'ao ⇒ bool" (infix "<ow" 50)
  assumes strict_iff_order: "⟦ a ∈ U; b ∈ U ⟧ ⟹ a <ow b ⟷ a ≤ow b ∧ a ≠ b"
    and antisym: "⟦ a ∈ U; b ∈ U; a ≤ow b; b ≤ow a ⟧ ⟹ a = b"
begin

notation le (infix "≤ow" 50)
  and ls (infix "<ow" 50)

sublocale preordering_ow U ‹(≤ow)› ‹(<ow)›  
  using local.antisym strict_iff_order by unfold_locales blast

end

locale order_ow = preorder_ow U le ls for U :: "'ao set" and le ls +
  assumes antisym: "⟦ x ∈ U; y ∈ U; x ≤ow y; y ≤ow x ⟧ ⟹ x = y" 
begin

sublocale 
  order: ordering_ow U ‹(≤ow)› ‹(<ow)› + 
  dual_order: ordering_ow U ‹(≥ow)› ‹(>ow)›
  apply unfold_locales
  subgoal by (force simp: less_le_not_le antisym)
  subgoal by (simp add: antisym)
  subgoal by (force simp: less_le_not_le antisym)
  subgoal by (simp add: antisym)
  done

no_notation le (infix "≤ow" 50)
  and ls (infix "<ow" 50)

end

locale ord_order_ow = ord1: ord_ow U1 le1 ls1 + ord2: order_ow U2 le2 ls2
  for U1 :: "'ao set" and le1 ls1 and U2 :: "'bo set" and le2 ls2

sublocale ord_order_ow ⊆ ord_preorder_ow ..

locale preorder_order_ow =
  ord1: preorder_ow U1 le1 ls1 + ord2: order_ow U2 le2 ls2
  for U1 :: "'ao set" and le1 ls1 and U2 :: "'bo set" and le2 ls2

sublocale preorder_order_ow ⊆ preorder_pair_ow ..

locale order_pair_ow = ord1: order_ow U1 le1 ls1 + ord2: order_ow U2 le2 ls2
  for U1 :: "'ao set" and le1 ls1 and U2 :: "'bo set" and le2 ls2

sublocale order_pair_ow ⊆ preorder_order_ow ..

ud ‹monoseq› (‹(with _ : «monoseq» _)› [1000, 1000] 10)

ctr relativization
  synthesis ctr_simps
  assumes [transfer_domain_rule, transfer_rule]: 
    "Domainp (B::'c⇒'d⇒bool) = (λx. x ∈ U2)"
    and [transfer_rule]: "right_total B" 
  trp (?'b ‹A::'a⇒'b⇒bool›) and (?'a B)
  in  monoseq_ow: monoseq.with_def


subsubsection‹Transfer rules›

context
  includes lifting_syntax
begin

lemma ordering_transfer[transfer_rule]:
  assumes [transfer_rule]: "bi_unique A" "right_total A" 
  shows 
    "((A ===> A ===> (=)) ===> (A ===> A ===> (=)) ===> (=)) 
      (ordering_ow (Collect (Domainp A))) ordering"
  unfolding ordering_ow_def ordering_ow_axioms_def ordering_def ordering_axioms_def 
  apply transfer_prover_start
  apply transfer_step+
  unfolding Ball_Collect[symmetric]
  by (intro ext HOL.arg_cong2[where f="(∧)"]) auto

lemma order_transfer[transfer_rule]:
  assumes [transfer_rule]: "bi_unique A" "right_total A" 
  shows 
    "((A ===> A ===> (=)) ===> (A ===> A ===> (=)) ===> (=)) 
      (order_ow (Collect (Domainp A))) class.order"
  unfolding 
    order_ow_def class.order_def order_ow_axioms_def class.order_axioms_def
  apply transfer_prover_start
  apply transfer_step+
  by simp

end


subsubsection‹Relativization›

context ordering_ow
begin

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

tts_lemma strict_implies_not_eq:
  assumes "a ∈ U" and "b ∈ U" and "a <ow b"
  shows "a ≠ b"
    is ordering.strict_implies_not_eq.
    
tts_lemma order_iff_strict:
  assumes "a ∈ U" and "b ∈ U"
  shows "(a ≤ow b) = (a <ow b ∨ a = b)"
    is ordering.order_iff_strict.
   
tts_lemma not_eq_order_implies_strict:
  assumes "a ∈ U" and "b ∈ U" and "a ≠ b" and "a ≤ow b"
  shows "a <ow b"
    is ordering.not_eq_order_implies_strict.

tts_lemma eq_iff:
  assumes "a ∈ U" and "b ∈ U"
  shows "(a = b) = (a ≤ow b ∧ b ≤ow a)"
    is ordering.eq_iff.

end

end

context order_ow 
begin

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

tts_lemma atLeastAtMost_singleton:
  assumes "a ∈ U"
  shows "{a..owa} = {a}"
  is order_class.atLeastAtMost_singleton.
    
tts_lemma less_imp_neq:
  assumes "y ∈ U" and "x <ow y"
  shows "x ≠ y"
    is order_class.less_imp_neq.
    
tts_lemma atLeastatMost_empty:
  assumes "b ∈ U" and "a ∈ U" and "b <ow a"
  shows "{a..owb} = {}"
    is order_class.atLeastatMost_empty.
    
tts_lemma less_imp_not_eq:
  assumes "y ∈ U" and "x <ow y"
  shows "(x = y) = False"
    is order_class.less_imp_not_eq.
    
tts_lemma less_imp_not_eq2:
  assumes "y ∈ U" and "x <ow y"
  shows "(y = x) = False"
    is order_class.less_imp_not_eq2.
    
tts_lemma atLeastLessThan_empty:
  assumes "b ∈ U" and "a ∈ U" and "b ≤ow a"
  shows "(on U with (≤ow) (<ow) : {a..<b}) = {}"
    is order_class.atLeastLessThan_empty.
    
tts_lemma greaterThanAtMost_empty:
  assumes "l ∈ U" and "k ∈ U" and "l ≤ow k"
  shows "{k<ow..l} = {}"
    is order_class.greaterThanAtMost_empty.

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

tts_lemma antisym_conv2:
  assumes "x ∈ U" and "y ∈ U" and "x ≤ow y"
  shows "(¬ x <ow y) = (x = y)"
    is order_class.antisym_conv2.
    
tts_lemma greaterThanLessThan_empty:
  assumes "l ∈ U" and "k ∈ U" and "l ≤ow k"
  shows "{k<ow..<owl} = {}"
    is order_class.greaterThanLessThan_empty.
    
tts_lemma atLeastLessThan_eq_atLeastAtMost_diff:
  assumes "a ∈ U" and "b ∈ U"
  shows "(on U with (≤ow) (<ow) : {a..<b}) = {a..owb} - {b}"
    is order_class.atLeastLessThan_eq_atLeastAtMost_diff.
    
tts_lemma greaterThanAtMost_eq_atLeastAtMost_diff:
  assumes "a ∈ U" and "b ∈ U"
  shows "{a<ow..b} = {a..owb} - {a}"
    is order_class.greaterThanAtMost_eq_atLeastAtMost_diff.

tts_lemma less_separate:
  assumes "x ∈ U" and "y ∈ U" and "x <ow y"
  shows 
    "∃x'∈U. ∃y'∈U. x ∈ {..<owx'} ∧ y ∈ {y'<ow..} ∧ {..<owx'} ∩ {y'<ow..} = {}"
    is order_class.less_separate.

tts_lemma order_iff_strict:
  assumes "a ∈ U" and "b ∈ U"
  shows "(a ≤ow b) = (a <ow b ∨ a = b)"
    is order_class.order.order_iff_strict.
    
tts_lemma le_less:
  assumes "x ∈ U" and "y ∈ U"
  shows "(x ≤ow y) = (x <ow y ∨ x = y)"
    is order_class.le_less.
    
tts_lemma strict_iff_order:
  assumes "a ∈ U" and "b ∈ U"
  shows "(a <ow b) = (a ≤ow b ∧ a ≠ b)"
    is order_class.order.strict_iff_order.
    
tts_lemma less_le:
  assumes "x ∈ U" and "y ∈ U"
  shows "(x <ow y) = (x ≤ow y ∧ x ≠ y)"
    is order_class.less_le.

tts_lemma atLeastAtMost_singleton':
  assumes "b ∈ U" and "a = b"
  shows "{a..owb} = {a}"
    is order_class.atLeastAtMost_singleton'.
    
tts_lemma le_imp_less_or_eq:
  assumes "x ∈ U" and "y ∈ U" and "x ≤ow y"
  shows "x <ow y ∨ x = y"
    is order_class.le_imp_less_or_eq.
  
tts_lemma antisym_conv:
  assumes "y ∈ U" and "x ∈ U" and "y ≤ow x"
  shows "(x ≤ow y) = (x = y)"
    is order_class.antisym_conv.

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

tts_lemma neq_le_trans:
  assumes "a ∈ U" and "b ∈ U" and "a ≠ b" and "a ≤ow b"
  shows "a <ow b"
    is order_class.neq_le_trans.
    
tts_lemma Iio_Int_singleton:
  assumes "k ∈ U" and "x ∈ U"
  shows "{..<owk} ∩ {x} = (if x <ow k then {x} else {})"
    is order_class.Iio_Int_singleton.
    
tts_lemma atLeastAtMost_singleton_iff:
  assumes "a ∈ U" and "b ∈ U" and "c ∈ U"
  shows "({a..owb} = {c}) = (a = b ∧ b = c)"
    is order_class.atLeastAtMost_singleton_iff.
    
tts_lemma Icc_eq_Icc:
  assumes "l ∈ U" and "h ∈ U" and "l' ∈ U" and "h' ∈ U"
  shows "({l..owh} = {l'..owh'}) = (h = h' ∧ l = l' ∨ ¬ l' ≤ow h' ∧ ¬ l ≤ow h)"
    is order_class.Icc_eq_Icc.
    
tts_lemma lift_Suc_mono_less_iff:
  assumes "range f ⊆ U" and "⋀n. f n <ow f (Suc n)"
  shows "(f n <ow f m) = (n < m)"
    is order_class.lift_Suc_mono_less_iff.

tts_lemma lift_Suc_mono_less:
  assumes "range f ⊆ U" and "⋀n. f n <ow f (Suc n)" and "n < n'"
  shows "f n <ow f n'"
    is order_class.lift_Suc_mono_less.
  
tts_lemma lift_Suc_mono_le:
  assumes "range f ⊆ U" and "⋀n. f n ≤ow f (Suc n)" and "n ≤ n'"
  shows "f n ≤ow f n'"
    is order_class.lift_Suc_mono_le.
    
tts_lemma lift_Suc_antimono_le:
  assumes "range f ⊆ U" and "⋀n. f (Suc n) ≤ow f n" and "n ≤ n'"
  shows "f n' ≤ow f n"
    is order_class.lift_Suc_antimono_le.

tts_lemma ivl_disj_int_two:
  assumes "l ∈ U" and "m ∈ U" and "u ∈ U"
  shows 
    "{l<ow..<owm} ∩ (on U with (≤ow) (<ow) : {m..<u}) = {}"
    "{l<ow..m} ∩ {m<ow..<owu} = {}"
    "(on U with (≤ow) (<ow) : {l..<m}) ∩ (on U with (≤ow) (<ow) : {m..<u}) = {}"
    "{l..owm} ∩ {m<ow..<owu} = {}"
    "{l<ow..<owm} ∩ {m..owu} = {}"
    "{l<ow..m} ∩ {m<ow..u} = {}"
    "(on U with (≤ow) (<ow) : {l..<m}) ∩ {m..owu} = {}"
    "{l..owm} ∩ {m<ow..u} = {}"
    is Set_Interval.ivl_disj_int_two.
  
tts_lemma ivl_disj_int_one:
  assumes "l ∈ U" and "u ∈ U"
  shows 
    "{..owl} ∩ {l<ow..<owu} = {}"
    "{..<owl} ∩ (on U with (≤ow) (<ow) : {l..<u}) = {}"
    "{..owl} ∩ {l<ow..u} = {}"
    "{..<owl} ∩ {l..owu} = {}"
    "{l<ow..u} ∩ {u<ow..} = {}"
    "{l<ow..<owu} ∩ {u..ow} = {}"
    "{l..owu} ∩ {u<ow..} = {}"
    "(on U with (≤ow) (<ow) : {l..<u}) ∩ {u..ow} = {}"
    is Set_Interval.ivl_disj_int_one.

tts_lemma min_absorb2:
  assumes "y ∈ U" and "x ∈ U" and "y ≤ow x"
  shows "local.min x y = y"
    is Orderings.min_absorb2.
    
tts_lemma max_absorb1:
  assumes "y ∈ U" and "x ∈ U" and "y ≤ow x"
  shows "local.max x y = x"
    is Orderings.max_absorb1.

tts_lemma atMost_Int_atLeast:
  assumes "n ∈ U"
  shows "{..own} ∩ {n..ow} = {n}"
    is Set_Interval.atMost_Int_atLeast.

tts_lemma monoseq_Suc:
  assumes "range X ⊆ U"
  shows 
    "(with (≤ow) : «monoseq» X) = 
      ((∀x. X x ≤ow X (Suc x)) ∨ (∀x. X (Suc x) ≤ow X x))"
    is Topological_Spaces.monoseq_Suc.

tts_lemma mono_SucI2:
  assumes "range X ⊆ U" and "∀x. X (Suc x) ≤ow X x"
  shows "with (≤ow) : «monoseq» X"
    is Topological_Spaces.mono_SucI2.

tts_lemma mono_SucI1:
  assumes "range X ⊆ U" and "∀x. X x ≤ow X (Suc x)"
  shows "with (≤ow) : «monoseq» X"
    is Topological_Spaces.mono_SucI1.

tts_lemma monoI2:
  assumes "range X ⊆ U" and "∀x y. x ≤ y ⟶ X y ≤ow X x"
  shows "with (≤ow) : «monoseq» X"
    is Topological_Spaces.monoI2.

tts_lemma monoI1:
  assumes "range X ⊆ U" and "∀x y. x ≤ y ⟶ X x ≤ow X y"
  shows "with (≤ow) : «monoseq» X"
    is Topological_Spaces.monoI1.

end

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

tts_lemma ex_min_if_finite:
  assumes "S ⊆ U"
    and "finite S"
    and "S ≠ {}"
  shows "∃x∈S. ¬ (∃y∈S. y <ow x)"
    is Lattices_Big.ex_min_if_finite.
    
end

tts_context
  tts: (?'a to U)
  sbterms: (‹(≤)::['a::order, 'a::order] ⇒ bool› to ‹(≤ow)›) 
    and (‹(<)::['a::order, 'a::order] ⇒ bool› to ‹(<ow)›)
  substituting order_ow_axioms
  eliminating through clarsimp
begin

tts_lemma xt1:
  shows 
    "⟦a = b; c <ow b⟧ ⟹ c <ow a"
    "⟦b <ow a; b = c⟧ ⟹ c <ow a"
    "⟦a = b; c ≤ow b⟧ ⟹ c ≤ow a"
    "⟦b ≤ow a; b = c⟧ ⟹ c ≤ow a"
    "⟦y ∈ U; x ∈ U; y ≤ow x; x ≤ow y⟧ ⟹ x = y"
    "⟦y ∈ U; x ∈ U; z ∈ U; y ≤ow x; z ≤ow y⟧ ⟹ z ≤ow x"
    "⟦y ∈ U; x ∈ U; z ∈ U; y <ow x; z ≤ow y⟧ ⟹ z <ow x"
    "⟦y ∈ U; x ∈ U; z ∈ U; y ≤ow x; z <ow y⟧ ⟹ z <ow x"
    "⟦b ∈ U; a ∈ U; b <ow a; a <ow b⟧ ⟹ P"
    "⟦y ∈ U; x ∈ U; z ∈ U; y <ow x; z <ow y⟧ ⟹ z <ow x"
    "⟦b ∈ U; a ∈ U; b ≤ow a; a ≠ b⟧ ⟹ b <ow a"
    "⟦a ∈ U; b ∈ U; a ≠ b; b ≤ow a⟧ ⟹ b <ow a"
    "⟦
      b ∈ U;
      c ∈ U;
      a = f b;
      c <ow b;
      ⋀x y. ⟦x ∈ U; y ∈ U; y <ow x⟧ ⟹ f y <ow f x
     ⟧ ⟹ f c <ow a"
    "⟦
      b ∈ U;
      a ∈ U;
      b <ow a;
      f b = c;
      ⋀x y. ⟦x ∈ U; y ∈ U; y <ow x⟧ ⟹ f y <ow f x
      ⟧ ⟹ c <ow f a"
    "⟦
      b ∈ U;
      c ∈ U;
      a = f b;
      c ≤ow b;
      ⋀x y. ⟦x ∈ U; y ∈ U; y ≤ow x⟧ ⟹ f y ≤ow f x
     ⟧ ⟹ f c ≤ow a"
    "⟦
      b ∈ U; 
      a ∈ U; 
      b ≤ow a; 
      f b = c; 
      ⋀x y. ⟦x ∈ U; y ∈ U; y ≤ow x⟧ ⟹ f y ≤ow f x
     ⟧ ⟹ c ≤ow f a"
    is Orderings.xt1.

end

end

context ord_order_ow 
begin

tts_context
  tts: (?'a to U2) and (?'b to U1)
  sbterms: (‹(≤)::[?'a::order, ?'a::order] ⇒ bool› to ‹(≤ow.2)›) 
    and (‹(<)::[?'a::order, ?'a::order] ⇒ bool› to ‹(<ow.2)›) 
    and (‹(≤)::[?'b::ord, ?'b::ord] ⇒ bool› to ‹(≤ow.1)›) 
    and (‹(<)::[?'b::ord, ?'b::ord] ⇒ bool› to ‹(<ow.1)›) 
  rewriting ctr_simps
  substituting ord2.order_ow_axioms
  eliminating through clarsimp
begin

tts_lemma xt2:
  assumes "∀x∈U1. f x ∈ U2"
    and "b ∈ U1"
    and "a ∈ U2"
    and "c ∈ U1"
    and "f b ≤ow.2 a"
    and "c ≤ow.1 b"
    and "⋀x y. ⟦x ∈ U1; y ∈ U1; y ≤ow.1 x⟧ ⟹ f y ≤ow.2 f x"
  shows "f c ≤ow.2 a"
  is Orderings.xt2.
    
tts_lemma xt6:
  assumes "∀x∈U1. f x ∈ U2"
    and "b ∈ U1"
    and "a ∈ U2"
    and "c ∈ U1"
    and "f b ≤ow.2 a"
    and "c <ow.1 b"
    and "⋀x y. ⟦x ∈ U1; y ∈ U1; y <ow.1 x⟧ ⟹ f y <ow.2 f x"
  shows "f c <ow.2 a"
    is Orderings.xt6.

end

end

context order_pair_ow 
begin

tts_context
  tts: (?'a to U1) and (?'b to U2)
  sbterms: (‹(≤)::[?'a::order, ?'a::order] ⇒ bool› to ‹(≤ow.1)›) 
    and (‹(<)::[?'a::order, ?'a::order] ⇒ bool› to ‹(<ow.1)›) 
    and (‹(≤)::[?'b::order, ?'b::order] ⇒ bool› to ‹(≤ow.2)›) 
    and (‹(<)::[?'b::order, ?'b::order] ⇒ bool› to ‹(<ow.2)›)
  rewriting ctr_simps
  substituting ord1.order_ow_axioms and ord2.order_ow_axioms
  eliminating through clarsimp
begin

tts_lemma xt3:
  assumes "b ∈ U1"
    and "a ∈ U1"
    and "c ∈ U2"
    and "∀x∈U1. f x ∈ U2"
    and "b ≤ow.1 a"
    and "c ≤ow.2 f b"
    and "⋀x y. ⟦x ∈ U1; y ∈ U1; y ≤ow.1 x⟧ ⟹ f y ≤ow.2 f x"
  shows "c ≤ow.2 f a"
    is Orderings.xt3.
    
tts_lemma xt4:
  assumes "∀x∈U2. f x ∈ U1"
    and "b ∈ U2"
    and "a ∈ U1"
    and "c ∈ U2"
    and "f b <ow.1 a"
    and "c ≤ow.2 b"
    and "⋀x y. ⟦x ∈ U2; y ∈ U2; y ≤ow.2 x⟧ ⟹ f y ≤ow.1 f x"
  shows "f c <ow.1 a"
    is Orderings.xt4.
    
tts_lemma xt5:
  assumes "b ∈ U1"
    and "a ∈ U1"
    and "c ∈ U2"
    and "∀x∈U1. f x ∈ U2"
    and "b <ow.1 a"
    and "c ≤ow.2 f b"
    and "⋀x y. ⟦x ∈ U1; y ∈ U1; y <ow.1 x⟧ ⟹ f y <ow.2 f x"
  shows "c <ow.2 f a"
    is Orderings.xt5.
    
tts_lemma xt7:
  assumes "b ∈ U1"
    and "a ∈ U1"
    and "c ∈ U2"
    and "∀x∈U1. f x ∈ U2"
    and "b ≤ow.1 a"
    and "c <ow.2 f b"
    and "⋀x y. ⟦x ∈ U1; y ∈ U1; y ≤ow.1 x⟧ ⟹ f y ≤ow.2 f x"
  shows "c <ow.2 f a"
    is Orderings.xt7.

tts_lemma xt8:
  assumes "∀x∈U2. f x ∈ U1"
    and "b ∈ U2"
    and "a ∈ U1"
    and "c ∈ U2"
    and "f b <ow.1 a"
    and "c <ow.2 b"
    and "⋀x y. ⟦x ∈ U2; y ∈ U2; y <ow.2 x⟧ ⟹ f y <ow.1 f x"
  shows "f c <ow.1 a"
    is Orderings.xt8.

tts_lemma xt9:
  assumes "b ∈ U1"
    and "a ∈ U1"
    and "c ∈ U2"
    and "∀x∈U1. f x ∈ U2"
    and "b <ow.1 a"
    and "c <ow.2 f b"
    and "⋀x y. ⟦x ∈ U1; y ∈ U1; y <ow.1 x⟧ ⟹ f y <ow.2 f x"
  shows "c <ow.2 f a"
    is Orderings.xt9.

end

tts_context
  tts: (?'a to U1) and (?'b to U2)
  sbterms: (‹(≤)::[?'a::order, ?'a::order] ⇒ bool› to ‹(≤ow.1)›) 
    and (‹(<)::[?'a::order, ?'a::order] ⇒ bool› to ‹(<ow.1)›)  
    and (‹(≤)::[?'b::order, ?'b::order] ⇒ bool› to ‹(≤ow.2)›) 
    and (‹(<)::[?'b::order, ?'b::order] ⇒ bool› to ‹(<ow.2)›)
  rewriting ctr_simps
  substituting ord1.order_ow_axioms and ord2.order_ow_axioms
  eliminating through simp
begin

tts_lemma order_less_subst1:
  assumes "a ∈ U1"
    and "∀x∈U2. f x ∈ U1"
    and "b ∈ U2"
    and "c ∈ U2"
    and "a <ow.1 f b"
    and "b <ow.2 c"
    and "⋀x y. ⟦x ∈ U2; y ∈ U2; x <ow.2 y⟧ ⟹ f x <ow.1 f y"
  shows "a <ow.1 f c"
    is Orderings.order_less_subst1.
    
tts_lemma order_subst1:
  assumes "a ∈ U1"
    and "∀x∈U2. f x ∈ U1"
    and "b ∈ U2"
    and "c ∈ U2"
    and "a ≤ow.1 f b"
    and "b ≤ow.2 c"
    and "⋀x y. ⟦x ∈ U2; y ∈ U2; x ≤ow.2 y⟧ ⟹ f x ≤ow.1 f y"
  shows "a ≤ow.1 f c"
    is Orderings.order_subst1.

end

tts_context
  tts: (?'a to U1) and (?'c to U2)
  sbterms: (‹(≤)::[?'a::order, ?'a::order] ⇒ bool› to ‹(≤ow.1)›) 
    and (‹(<)::[?'a::order, ?'a::order] ⇒ bool› to ‹(<ow.1)›) 
    and (‹(≤)::[?'c::order, ?'c::order] ⇒ bool› to ‹(≤ow.2)›) 
    and (‹(<)::[?'c::order, ?'c::order] ⇒ bool› to ‹(<ow.2)›)
  rewriting ctr_simps
  substituting ord1.order_ow_axioms and ord2.order_ow_axioms
  eliminating through simp
begin

tts_lemma order_less_le_subst2:
  assumes "a ∈ U1"
    and "b ∈ U1"
    and "∀x∈U1. f x ∈ U2"
    and "c ∈ U2"
    and "a <ow.1 b"
    and "f b ≤ow.2 c"
    and "⋀x y. ⟦x ∈ U1; y ∈ U1; x <ow.1 y⟧ ⟹ f x <ow.2 f y"
  shows "f a <ow.2 c"
    is Orderings.order_less_le_subst2.
    
tts_lemma order_le_less_subst2:
  assumes "a ∈ U1"
    and "b ∈ U1"
    and "∀x∈U1. f x ∈ U2"
    and "c ∈ U2"
    and "a ≤ow.1 b"
    and "f b <ow.2 c"
    and "⋀x y. ⟦x ∈ U1; y ∈ U1; x ≤ow.1 y⟧ ⟹ f x ≤ow.2 f y"
  shows "f a <ow.2 c"
    is Orderings.order_le_less_subst2.
    
tts_lemma order_less_subst2:
  assumes "a ∈ U1"
    and "b ∈ U1"
    and "∀x∈U1. f x ∈ U2"
    and "c ∈ U2"
    and "a <ow.1 b"
    and "f b <ow.2 c"
    and "⋀x y. ⟦x ∈ U1; y ∈ U1; x <ow.1 y⟧ ⟹ f x <ow.2 f y"
  shows "f a <ow.2 c"
    is Orderings.order_less_subst2.

tts_lemma order_subst2:
  assumes "a ∈ U1"
    and "b ∈ U1"
    and "∀x∈U1. f x ∈ U2"
    and "c ∈ U2"
    and "a ≤ow.1 b"
    and "f b ≤ow.2 c"
    and "⋀x y. ⟦x ∈ U1; y ∈ U1; x ≤ow.1 y⟧ ⟹ f x ≤ow.2 f y"
  shows "f a ≤ow.2 c"
    is Orderings.order_subst2.

end

end



subsection‹Dense orders›


subsubsection‹Definitions and common properties›

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


subsubsection‹Transfer rules›

context
  includes lifting_syntax
begin

lemma dense_order_transfer[transfer_rule]:
  assumes [transfer_rule]: "bi_unique A" "right_total A" 
  shows 
    "((A ===> A ===> (=)) ===> (A ===> A ===> (=)) ===> (=)) 
      (dense_order_ow (Collect (Domainp A))) class.dense_order"
  unfolding 
    dense_order_ow_def class.dense_order_def
    dense_order_ow_axioms_def class.dense_order_axioms_def
  apply transfer_prover_start
  apply transfer_step+
  by simp
  
end



subsection‹
Partial orders with the greatest element and 
partial orders with the least elements
›


subsubsection‹Definitions and common properties›

locale ordering_top_ow = ordering_ow U le ls 
  for U :: "'ao set" and le ls  +
  fixes top :: "'ao" ("⊤ow")
  assumes top_closed[simp]: "⊤ow ∈ U"
  assumes extremum[simp]: "a ∈ U ⟹ a ≤ow ⊤ow"
begin

notation top ("⊤ow")

end

locale bot_ow = 
  fixes U :: "'ao set" and bot (‹⊥ow›)
  assumes bot_closed[simp]: "⊥ow ∈ U"
begin

notation bot (‹⊥ow›)

end

locale bot_pair_ow = ord1: bot_ow U1 bot1 + ord2: bot_ow U2 bot2
  for U1 :: "'ao set" and bot1 and U2 :: "'bo set" and bot2
begin

notation bot1 (‹⊥ow.1›)
notation bot2 (‹⊥ow.2›)

end

locale order_bot_ow = order_ow U le ls + bot_ow U bot
  for U :: "'ao set" and bot le ls  +
  assumes bot_least: "a ∈ U ⟹ ⊥ow ≤ow a"
begin

sublocale bot: ordering_top_ow U ‹(≥ow)› ‹(>ow)› ‹⊥ow›
  apply unfold_locales
  subgoal by simp
  subgoal by (simp add: bot_least)
  done

no_notation le (infix "≤ow" 50)
  and ls (infix "<ow" 50)
  and top ("⊤ow")

end

locale order_bot_pair_ow = 
  ord1: order_bot_ow U1 bot1 le1 ls1 + ord2: order_bot_ow U2 bot2 le2 ls2 
  for U1 :: "'ao set" and bot1 le1 ls1 and U2 :: "'bo set" and bot2 le2 ls2  
begin

sublocale bot_pair_ow ..
sublocale order_pair_ow ..

end


locale top_ow = 
  fixes U :: "'ao set" and top (‹⊤ow›)
  assumes top_closed[simp]: "⊤ow ∈ U"
begin

notation top (‹⊤ow›)

end

locale top_pair_ow = ord1: top_ow U1 top1 + ord2: top_ow U2 top2
  for U1 :: "'ao set" and top1 and U2 :: "'bo set" and top2
begin

notation top1 (‹⊤ow.1›)
notation top2 (‹⊤ow.2›)

end

locale order_top_ow = order_ow U le ls + top_ow U top
  for U :: "'ao set" and le ls top  +
  assumes top_greatest: "a ∈ U ⟹ a ≤ow ⊤ow"
begin

sublocale top: ordering_top_ow U ‹(≤ow)› ‹(<ow)› ‹⊤ow›
  apply unfold_locales
  subgoal by simp
  subgoal by (simp add: top_greatest)
  done

no_notation le (infix "≤ow" 50)
  and ls (infix "<ow" 50)
  and top ("⊤ow")

end

locale order_top_pair_ow = 
  ord1: order_top_ow U1 le1 ls1 top1 + ord2: order_top_ow U2 le2 ls2 top2
  for U1 :: "'ao set" and le1 ls1 top1 and U2 :: "'bo set" and le2 ls2 top2 
begin

sublocale top_pair_ow ..
sublocale order_pair_ow ..

end


subsubsection‹Transfer rules›

context
  includes lifting_syntax
begin

lemma ordering_top_transfer[transfer_rule]:
  assumes [transfer_rule]: "bi_unique A" "right_total A" 
  shows 
    "((A ===> A ===> (=)) ===> (A ===> A ===> (=)) ===> A ===> (=)) 
      (ordering_top_ow (Collect (Domainp A))) ordering_top"
proof-
  let ?P = "((A ===> A ===> (=)) ===> (A ===> A ===> (=)) ===> A ===> (=))"
  let ?ordering_top_ow = "ordering_top_ow (Collect (Domainp A))"
  have 
    "?P ?ordering_top_ow (λle ls ext. ext ∈ UNIV ∧ ordering_top le ls ext)"
    unfolding 
      ordering_top_ow_def ordering_top_def
      ordering_top_ow_axioms_def ordering_top_axioms_def
    apply transfer_prover_start
    apply transfer_step+
    by blast 
  thus ?thesis by simp
qed

lemma order_bot_transfer[transfer_rule]:
  assumes [transfer_rule]: "bi_unique A" "right_total A"
  shows 
    "(A ===> (A ===> A ===> (=)) ===> (A ===> A ===> (=)) ===> (=)) 
      (order_bot_ow (Collect (Domainp A))) class.order_bot"
proof-
  let ?P = "(A ===> (A ===> A ===> (=)) ===> (A ===> A ===> (=)) ===> (=))"
  let ?order_bot_ow = "order_bot_ow (Collect (Domainp A))"
  have 
    "?P ?order_bot_ow (λbot le ls. bot ∈ UNIV ∧ class.order_bot bot le ls)"
    unfolding 
      class.order_bot_def order_bot_ow_def 
      class.order_bot_axioms_def order_bot_ow_axioms_def
      bot_ow_def
    apply transfer_prover_start
    apply transfer_step+
    by blast 
  thus ?thesis by simp
qed

lemma order_top_transfer[transfer_rule]:
  assumes [transfer_rule]: "bi_unique A" "right_total A" 
  shows 
    "((A ===> A ===> (=)) ===> (A ===> A ===> (=)) ===> A ===> (=)) 
      (order_top_ow (Collect (Domainp A))) class.order_top"
proof-
  let ?P = "((A ===> A ===> (=)) ===> (A ===> A ===> (=)) ===> A ===> (=))"
  let ?order_top_ow = "order_top_ow (Collect (Domainp A))"
  have 
    "?P ?order_top_ow (λle ls top. top ∈ UNIV ∧ class.order_top le ls top)"
    unfolding 
      class.order_top_def order_top_ow_def 
      class.order_top_axioms_def order_top_ow_axioms_def
      top_ow_def
    apply transfer_prover_start
    apply transfer_step+
    by blast 
  thus ?thesis by simp
qed
  
end


subsubsection‹Relativization›

context ordering_top_ow 
begin

tts_context
  tts: (?'a to U)
  rewriting ctr_simps
  substituting ordering_top_ow_axioms
  eliminating through simp
  applying [OF top_closed]
begin

tts_lemma extremum_uniqueI:
  assumes "⊤ow ≤ow ⊤ow"
  shows "⊤ow = ⊤ow"
    is ordering_top.extremum_uniqueI.
    
tts_lemma extremum_unique:
  shows "(⊤ow ≤ow ⊤ow) = (⊤ow = ⊤ow)"
    is ordering_top.extremum_unique.
    
tts_lemma extremum_strict:
  shows "¬ ⊤ow <ow ⊤ow"
    is ordering_top.extremum_strict.
    
tts_lemma not_eq_extremum:
  shows "(⊤ow ≠ ⊤ow) = (⊤ow <ow ⊤ow)"
    is ordering_top.not_eq_extremum.

end
  
end

context order_bot_ow 
begin

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

tts_lemma bdd_above_bot:
  assumes "A ⊆ U"
  shows "bdd_below A"
    is order_bot_class.bdd_below_bot.

tts_lemma not_less_bot:
  assumes "a ∈ U"
  shows "¬ a <ow ⊥ow"
  is order_bot_class.not_less_bot.
    
tts_lemma max_bot:
  assumes "x ∈ U"
  shows "max ⊥ow x = x"
    is order_bot_class.max_bot.

tts_lemma max_bot2:
  assumes "x ∈ U"
  shows "max x ⊥ow = x"
    is order_bot_class.max_bot2.

tts_lemma min_bot:
  assumes "x ∈ U"
  shows "min ⊥ow x = ⊥ow"
    is order_bot_class.min_bot.

tts_lemma min_bot2:
  assumes "x ∈ U"
  shows "min x ⊥ow = ⊥ow"
    is order_bot_class.min_bot2.

tts_lemma bot_unique:
  assumes "a ∈ U"
  shows "(a ≤ow ⊥ow) = (a = ⊥ow)"
    is order_bot_class.bot_unique.

tts_lemma bot_less:
  assumes "a ∈ U"
  shows "(a ≠ ⊥ow) = (⊥ow <ow a)"
    is order_bot_class.bot_less.

tts_lemma atLeast_eq_UNIV_iff:
  assumes "x ∈ U"
  shows "({x..ow} = U) = (x = ⊥ow)"
    is order_bot_class.atLeast_eq_UNIV_iff.

tts_lemma le_bot:
  assumes "a ∈ U" and "a ≤ow ⊥ow"
  shows "a = ⊥ow"
    is order_bot_class.le_bot.

end

end

context order_top_ow 
begin

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

tts_lemma bdd_above_top:
  assumes "A ⊆ U"
  shows "bdd_above A"
  is order_top_class.bdd_above_top.

tts_lemma not_top_less:
  assumes "a ∈ U"
  shows "¬ ⊤ow <ow a"
    is order_top_class.not_top_less.

tts_lemma max_top:
  assumes "x ∈ U"
  shows "max ⊤ow x = ⊤ow"
    is order_top_class.max_top.

tts_lemma max_top2:
  assumes "x ∈ U"
  shows "max x ⊤ow = ⊤ow"
    is order_top_class.max_top2.

tts_lemma min_top:
  assumes "x ∈ U"
  shows "min ⊤ow x = x"
    is order_top_class.min_top.

tts_lemma min_top2:
  assumes "x ∈ U"
  shows "min x ⊤ow = x"
    is order_top_class.min_top2.

tts_lemma top_unique:
  assumes "a ∈ U"
  shows "(⊤ow ≤ow a) = (a = ⊤ow)"
    is order_top_class.top_unique.

tts_lemma less_top:
  assumes "a ∈ U"
  shows "(a ≠ ⊤ow) = (a <ow ⊤ow)"
    is order_top_class.less_top.

tts_lemma atMost_eq_UNIV_iff:
  assumes "x ∈ U"
  shows "({..owx} = U) = (x = ⊤ow)"
    is order_top_class.atMost_eq_UNIV_iff.

tts_lemma top_le:
  assumes "a ∈ U" and "⊤ow ≤ow a"
  shows "a = ⊤ow"
    is order_top_class.top_le.

end

end

text‹\newpage›

end