Theory SML_Linorders

(* Title: Examples/SML_Relativization/Lattices/SML_Linorders.thy
   Author: Mihails Milehins
   Copyright 2021 (C) 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 ≤ow y ∨ y ≤ow x"
begin

sublocale min: 
  semilattice_order_ow U ‹(λx y. (with (≤ow) : «min» x y))› ‹(≤ow)› ‹(<ow)›
  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 (≤ow) : «max» x y))› ‹(≥ow)› ‹(>ow)›
  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 U1 le1 ls1 + lo?: linorder_ow U2 le2 ls2
  for U1 :: "'ao set" and le1 ls1 and U2 :: "'bo set" and le2 ls2
begin

sublocale ord_order_ow ..

end

locale preorder_linorder_ow = 
  po?: preorder_ow U1 le1 ls1 + lo?: linorder_ow U2 le2 ls2
  for U1 :: "'ao set" and le1 ls1 and U2 :: "'bo set" and le2 ls2
begin

sublocale preorder_order_ow ..

end

locale order_linorder_ow = 
  order?: order_ow U1 le1 ls1 + lo?: linorder_ow U2 le2 ls2
  for U1 :: "'ao set" and le1 ls1 and U2 :: "'bo set" and le2 ls2
begin

sublocale order_pair_ow ..

end

locale linorder_pair_ow = 
  lo1?: linorder_ow U1 le1 ls1 + lo2?: linorder_ow U2 le2 ls2
  for U1 :: "'ao set" and le1 ls1 and U2 :: "'bo set" and le2 ls2
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 ≤ow y ∨ y <ow x"
  is linorder_class.le_less_linear.

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

tts_lemma lessThan_minus_lessThan:
  assumes "n ∈ U" and "m ∈ U"
  shows "{..<own} - {..<owm} = (on U with (≤ow) (<ow) : {m..<n})"
    is linorder_class.lessThan_minus_lessThan.

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

tts_lemma Iic_subset_Iio_iff:
  assumes "a ∈ U" and "b ∈ U"
  shows "({..owa} ⊆ {..<owb}) = (a <ow b)"
    is linorder_class.Iic_subset_Iio_iff.

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

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

tts_lemma Int_atMost:
  assumes "a ∈ U" and "b ∈ U"
  shows "{..owa} ∩ {..owb} = {..owmin a b}"
    is linorder_class.Int_atMost.

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

tts_lemma greaterThan_Int_greaterThan:
  assumes "a ∈ U" and "b ∈ U"
  shows "{..<owa} ∩ {..<owb} = {..<owmin a b}"
    is linorder_class.greaterThan_Int_greaterThan.

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

tts_lemma Int_atLeastAtMostR2:
  assumes "a ∈ U" and "c ∈ U" and "d ∈ U"
  shows "{a..ow} ∩ {c..owd} = {max a c..owd}"
    is linorder_class.Int_atLeastAtMostR2.

tts_lemma Int_atLeastAtMostR1:
  assumes "b ∈ U" and "c ∈ U" and "d ∈ U"
  shows "{..owb} ∩ {c..owd} = {c..owmin b d}"
    is linorder_class.Int_atLeastAtMostR1.

tts_lemma Int_atLeastAtMostL2:
  assumes "a ∈ U" and "b ∈ U" and "c ∈ U"
  shows "{a..owb} ∩ {c..ow} = {max a c..owb}"
    is linorder_class.Int_atLeastAtMostL2.

tts_lemma Int_atLeastAtMostL1:
  assumes "a ∈ U" and "b ∈ U" and "d ∈ U"
  shows "{a..owb} ∩ {..owd} = {a..owmin b d}"
    is linorder_class.Int_atLeastAtMostL1.

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

tts_lemma not_less_iff_gr_or_eq:
  assumes "x ∈ U" and "y ∈ U"
  shows "(¬ x <ow y) = (y <ow 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..owb} - {a, b} = {a<ow..<owb}"
    is linorder_class.atLeastAtMost_diff_ends.

tts_lemma less_max_iff_disj:
  assumes "z ∈ U" and "x ∈ U" and "y ∈ U"
  shows "(z <ow max x y) = (z <ow x ∨ z <ow 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 <ow min x y) = (z <ow x ∧ z <ow 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 <ow z) = (x <ow z ∧ y <ow 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 <ow z) = (x <ow z ∨ y <ow 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 ≤ow max x y) = (z ≤ow x ∨ z ≤ow 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 ≤ow z) = (x ≤ow z ∨ y ≤ow z)"
    is linorder_class.min_le_iff_disj.

tts_lemma antisym_conv3:
  assumes "y ∈ U" and "x ∈ U" and "¬ y <ow x"
  shows "(¬ x <ow 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..owb} ∩ {c..owd} = {max a c..owmin 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 (≤ow) (<ow) : {a..<b}) ∩ (on U with (≤ow) (<ow) : {c..<d}) = 
      (on U with (≤ow) (<ow) : {(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<ow..b} ∩ {c<ow..d} = {max a c<ow..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<ow..<owb} ∩ {c<ow..<owd} = {max a c<ow..<owmin b d}"
    is linorder_class.Int_greaterThanLessThan.

tts_lemma le_cases:
  assumes "x ∈ U" and "y ∈ U" and "x ≤ow y ⟹ P" and "y ≤ow 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 ≤ow j ⟶ P j) ∧ (¬ i ≤ow j ⟶ P i))"
    is linorder_class.split_max.

tts_lemma split_min:
  assumes "i ∈ U" and "j ∈ U"
  shows "P (min i j) = ((i ≤ow j ⟶ P i) ∧ (¬ i ≤ow 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<ow..b} ⊆ {c<ow..d}) = (b ≤ow a ∨ b ≤ow d ∧ c ≤ow 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 (≤ow) (<ow) : {a..<b}) ⊆ (on U with (≤ow) (<ow) : {c..<d})"
  shows "b ≤ow a ∨ b ≤ow d ∧ c ≤ow 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<ow..b} = {c<ow..d}) = (b ≤ow a ∧ d ≤ow c ∨ a = c ∧ b = d)"
    is linorder_class.Ioc_inj.

tts_lemma neqE:
  assumes "x ∈ U"
    and "y ∈ U"
    and "x ≠ y"
    and "x <ow y ⟹ R"
    and "y <ow 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<ow..b} ∩ {c<ow..d} = {}) = (b ≤ow a ∨ d ≤ow c ∨ b ≤ow c ∨ d ≤ow a)"
    is linorder_class.Ioc_disjoint.

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

tts_lemma le_cases3:
  assumes "x ∈ U"
    and "y ∈ U"
    and "z ∈ U"
    and "⟦x ≤ow y; y ≤ow z⟧ ⟹ P"
    and "⟦y ≤ow x; x ≤ow z⟧ ⟹ P"
    and "⟦x ≤ow z; z ≤ow y⟧ ⟹ P"
    and "⟦z ≤ow y; y ≤ow x⟧ ⟹ P"
    and "⟦y ≤ow z; z ≤ow x⟧ ⟹ P"
    and "⟦z ≤ow x; x ≤ow 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 ‹≤ow› 50) and ls (infix ‹<ow› 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 <ow b"
  shows "infinite {a..owb}"
    is dense_linorder_class.infinite_Icc.

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

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

tts_lemma infinite_Ioo:
  assumes "a ∈ U" and "b ∈ U" and "a <ow b"
  shows "infinite {a<ow..<owb}"
    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 (≤ow) (<ow) : {a..<b}) ⊆ {c..owd}) = 
      (a <ow b ⟶ b ≤ow d ∧ c ≤ow 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<ow..b} ⊆ {c..owd}) = (a <ow b ⟶ b ≤ow d ∧ c ≤ow 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<ow..b} ⊆ (on U with (≤ow) (<ow) : {c..<d})) = 
    (a <ow b ⟶ b <ow d ∧ c ≤ow 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<ow..<owb} ⊆ {c..owd}) = (a <ow b ⟶ b ≤ow d ∧ c ≤ow 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<ow..<owb} ⊆ (on U with (≤ow) (<ow) : {c..<d})) = 
      (a <ow b ⟶ b ≤ow d ∧ c ≤ow 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<ow..<owb} ⊆ {c<ow..d}) = (a <ow b ⟶ b ≤ow d ∧ c ≤ow 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<ow..<owb} ⊆ {c<ow..<owd}) = (a <ow b ⟶ b ≤ow d ∧ c ≤ow a)"
    is dense_linorder_class.greaterThanLessThan_subseteq_greaterThanLessThan.

end

end

text‹\newpage›

end