Theory SML_Ordered_Topological_Spaces

(* Title: Examples/SML_Relativization/Topology/SML_Ordered_Topological_Spaces.thy
   Author: Mihails Milehins
   Copyright 2021 (C) Mihails Milehins
*)
section‹Relativization of the results about ordered topological spaces›
theory SML_Ordered_Topological_Spaces
  imports 
    SML_Topological_Space
    "../Lattices/SML_Linorders"
begin



subsection‹Ordered topological space›


subsubsection‹Definitions and common properties›

locale order_topology_ow = 
  order_ow U le ls for U :: "'at set" and le ls +
  fixes τ :: "'at set ⇒ bool"
  assumes open_generated_order: "s ⊆ U ⟹ 
    τ s = 
      (
        (
          in_topology_generated_by 
            (
              (λa. (on U with (<ow) : {..< a})) ` U ∪ 
              (λa. (on U with (<ow) : {a <..})) ` U
            ) 
          on U : «open» s 
        )
      )"
begin

sublocale topological_space_ow
proof -
  define τ' where τ': 
    "τ' = generate_topology_on 
      (
        (λa. (on U with (<ow) : {..< a})) ` U ∪ 
        (λa. (on U with (<ow) : {a <..})) ` U
      ) 
      U"
  have 
    "(
      (λa. (on U with (<ow) : {..< a})) ` U ∪ 
      (λa. (on U with (<ow) : {a <..})) ` U
    ) ⊆ Pow U"
    unfolding lessThan_def greaterThan_def lessThan_ow_def greaterThan_ow_def
    by auto
  then have "topological_space_ow U τ'"
    unfolding τ' by (simp add: topological_space_generate_topology)
  moreover then have "s ⊆ U ⟹ τ' s = τ s" for s
    unfolding τ' using open_generated_order by blast
  ultimately show "topological_space_ow U τ"  
    unfolding τ' by (rule ts_open_eq_ts_open)
qed

end

locale ts_ot_ow = 
  ts: topological_space_ow U1 τ1 + ot: order_topology_ow U2 le2 ls2 τ2
  for U1 :: "'at set" and τ1 and U2 :: "'bt set" and le2 ls2 τ2
begin

sublocale topological_space_pair_ow U1 τ1 U2 τ2 ..

end

locale order_topology_pair_ow = 
  ot1: order_topology_ow U1 le1 ls1 τ1 + ot2: order_topology_ow U2 le2 ls2 τ2
  for U1 :: "'at set" and le1 ls1 τ1 and U2 :: "'bt set" and le2 ls2 τ2
begin

sublocale ts_ot_ow U1 τ1 U2 le2 ls2 τ2 ..

end


subsubsection‹Transfer rules›

context
  includes lifting_syntax
begin

lemma order_topology_transfer[transfer_rule]:
  assumes [transfer_rule]: "bi_unique A" "right_total A" 
  shows 
    "(
      (A ===> A ===> (=)) ===> 
      (A ===> A ===> (=)) ===> 
      (rel_set A ===> (=)) ===> 
      (=)
    ) (order_topology_ow (Collect (Domainp A))) class.order_topology"
  unfolding order_topology_ow_def class.order_topology_def
  unfolding order_topology_ow_axioms_def class.order_topology_axioms_def
proof(intro rel_funI, standard; elim conjE)
  let ?U = "Collect (Domainp A)"
  fix le :: "['a, 'a] ⇒ bool" 
    and le' :: "['b, 'b] ⇒ bool"
    and ls :: "['a, 'a] ⇒ bool" 
    and ls' :: "['b, 'b] ⇒ bool"
    and τ :: "'a set ⇒ bool"
    and τ' :: "'b set ⇒ bool"
  assume [transfer_rule]: "(A ===> A ===> (=)) le le'" 
    and [transfer_rule]: "(A ===> A ===> (=)) ls ls'"
    and [transfer_rule]: "(rel_set A ===> (=)) τ τ'"
    and oow: "order_ow (Collect (Domainp A)) le ls"
    and τ: 
      "∀s⊆Collect (Domainp A). τ s =
        generate_topology_on
          (lessThan_ow ?U ls ` ?U ∪ greaterThan_ow ?U ls ` ?U) ?U s" 
  have [transfer_rule]: "Domainp A = (λx. x ∈ Collect (Domainp A))" by auto
  interpret oow: order_ow ?U le ls by (rule oow)
  interpret co: order le' ls' by transfer (rule oow)
  have ineq_fold:
    "lessThan.with ls y ≡ {x. ls x y}" 
    "greaterThan.with ls y ≡ {x. ls y x}"
    for ls :: "'c ⇒ 'c ⇒ bool" and y 
    unfolding lessThan.with_def greaterThan.with_def by auto
  have 
    "τ' = generate_topology (
      range (ord.lessThan ls') ∪ range (ord.greaterThan ls')
      )"
    unfolding co.lessThan_def co.greaterThan_def
    unfolding ineq_fold[symmetric]
    by (transfer, intro allI impI) (auto simp: τ)    
  from co.order_axioms this show
    "class.order le' ls' ∧ 
      τ' = generate_topology (
        range (ord.lessThan ls') ∪ range (ord.greaterThan ls')
      )"
    by simp
next
  let ?U = "Collect (Domainp A)"
  fix le :: "['a, 'a] ⇒ bool" 
    and le' :: "['b, 'b] ⇒ bool"
    and ls :: "['a, 'a] ⇒ bool" 
    and ls' :: "['b, 'b] ⇒ bool"
    and τ :: "'a set ⇒ bool"
    and τ' :: "'b set ⇒ bool"
  assume [transfer_rule]: "(A ===> A ===> (=)) le le'" 
    and [transfer_rule]: "(A ===> A ===> (=)) ls ls'"
    and [transfer_rule]: "(rel_set A ===> (=)) τ τ'"
    and co: "class.order le' ls'"
    and τ': "τ' = generate_topology
      (range (ord.lessThan ls') ∪ range (ord.greaterThan ls'))"
  have [transfer_rule]: "Domainp A = (λx. x ∈ Collect (Domainp A))" by auto
  interpret co: order le' ls' by (rule co)
  have ineq_fold:
    "lessThan.with ls y ≡ {x. ls x y}" 
    "greaterThan.with ls y ≡ {x. ls y x}"
    for ls :: "'c ⇒ 'c ⇒ bool" and y 
    unfolding lessThan.with_def greaterThan.with_def by auto
  from co have "order_ow ?U le ls" by transfer
  moreover have 
    "∀s⊆Collect (Domainp A). τ s =
      SML_Topological_Space.generate_topology_on
        (lessThan_ow ?U ls ` ?U ∪ greaterThan_ow ?U ls ` ?U) ?U s"
    by 
      (
        rule τ'[
          unfolded co.lessThan_def co.greaterThan_def,
          folded ineq_fold,
          untransferred
          ]
       )
  ultimately show 
    "order_ow ?U le ls ∧
      (
        ∀s⊆Collect (Domainp A). τ s = 
          SML_Topological_Space.generate_topology_on
            (lessThan_ow ?U ls ` ?U ∪ greaterThan_ow ?U ls ` ?U) ?U s
      )"
    by simp
qed
  
end


subsubsection‹Relativization›

context order_topology_ow 
begin

tts_context
  tts: (?'a to U)
  substituting order_topology_ow_axioms
  eliminating ‹?U ≠ {}› through simp
begin

tts_lemma open_greaterThan:
  assumes "a ∈ U"
  shows "τ {a<ow..}"
    is order_topology_class.open_greaterThan.
    
tts_lemma open_lessThan:
  assumes "a ∈ U"
  shows "τ {..<owa}"
  is order_topology_class.open_lessThan.

tts_lemma open_greaterThanLessThan:
  assumes "a ∈ U" and "b ∈ U"
  shows "τ {a<ow..<owb}"
    is order_topology_class.open_greaterThanLessThan.

end

end



subsection‹Linearly ordered topological space›


subsubsection‹Definitions and common properties›

locale linorder_topology_ow = 
  linorder_ow U le ls + order_topology_ow U le ls τ 
  for U :: "'at set" and le ls τ

locale ts_lt_ow = 
  ts: topological_space_ow U1 τ1 + lt: linorder_topology_ow U2 le2 ls2 τ2
  for U1 :: "'at set" and τ1 and U2 :: "'bt set" and le2 ls2 τ2
begin

sublocale ts_ot_ow U1 τ1 U2 le2 ls2 τ2 ..

end

locale ot_lt_ow = 
  ot: order_topology_ow U1 le1 ls1 τ1 + lt: linorder_topology_ow U2 le2 ls2 τ2
  for U1 :: "'at set" and le1 ls1 τ1 and U2 :: "'bt set" and le2 ls2 τ2
begin

sublocale ts_lt_ow U1 τ1 U2 le2 ls2 τ2 ..
sublocale order_topology_pair_ow U1 le1 ls1 τ1 U2 le2 ls2 τ2 ..

end

locale linorder_topology_pair_ow = 
  lt1: linorder_topology_ow U1 le1 ls1 τ1 + lt2: linorder_topology_ow U2 le2 ls2 τ2
  for U1 :: "'at set" and le1 ls1 τ1 and U2 :: "'bt set" and le2 ls2 τ2
begin

sublocale ot_lt_ow U1 le1 ls1 τ1 U2 le2 ls2 τ2 ..

end


subsubsection‹Transfer rules›

context
  includes lifting_syntax
begin

lemma linorder_topology_transfer[transfer_rule]:
  assumes [transfer_rule]: "bi_unique A" "right_total A" 
  shows 
    "(
      (A ===> A ===> (=)) ===> 
      (A ===> A ===> (=)) ===> 
      (rel_set A ===> (=)) ===> 
      (=)
    ) 
    (linorder_topology_ow (Collect (Domainp A))) class.linorder_topology"
  unfolding linorder_topology_ow_def class.linorder_topology_def
  by transfer_prover

end


subsubsection‹Relativization›

context linorder_topology_ow 
begin

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

tts_lemma open_right:
  assumes "S ⊆ U"
    and "x ∈ U"
    and "y ∈ U"
    and "τ S"
    and "x ∈ S"
    and "x <ow y"
  shows "∃z∈U. x <ow z ∧ (on U with (≤ow) (<ow) : {x..<z}) ⊆ S"
    is linorder_topology_class.open_right.
    
tts_lemma open_left:
  assumes "S ⊆ U"
    and "x ∈ U"
    and "y ∈ U"
    and "τ S"
    and "x ∈ S"
    and "y <ow x"
  shows "∃z∈U. z <ow x ∧ {z<ow..x} ⊆ S"
    is linorder_topology_class.open_left.

tts_lemma connectedD_interval:
  assumes "U ⊆ U"
    and "x ∈ U"
    and "y ∈ U"
    and "z ∈ U"
    and "connected U"
    and "x ∈ U"
    and "y ∈ U"
    and "x ≤ow z"
    and "z ≤ow y"
  shows "z ∈ U"
    is linorder_topology_class.connectedD_interval.

tts_lemma connected_contains_Icc:
  assumes "A ⊆ U"
    and "a ∈ U"
    and "b ∈ U"
    and "connected A"
    and "a ∈ A"
    and "b ∈ A"
  shows "{a..owb} ⊆ A"
    is Topological_Spaces.connected_contains_Icc.

tts_lemma connected_contains_Ioo:
  assumes "A ⊆ U"
    and "a ∈ U"
    and "b ∈ U"
    and "connected A"
    and "a ∈ A"
    and "b ∈ A"
  shows "{a<ow..<owb} ⊆ A"
    is Topological_Spaces.connected_contains_Ioo.

end

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

tts_lemma not_in_connected_cases:
  assumes "S ⊆ U"
    and "x ∈ U"
    and "connected S"
    and "x ∉ S"
    and "S ≠ {}"
    and "⟦bdd_above S; ⋀y. ⟦y ∈ U; y ∈ S⟧ ⟹ y ≤ow x⟧ ⟹ thesis"
    and "⟦bdd_below S; ⋀y. ⟦y ∈ U; y ∈ S⟧ ⟹ x ≤ow y⟧ ⟹ thesis"
  shows thesis
    is linorder_topology_class.not_in_connected_cases.

tts_lemma compact_attains_sup:
  assumes "S ⊆ U"
    and "compact S"
    and "S ≠ {}"
  shows "∃x∈S. ∀y∈S. y ≤ow x"
    is linorder_topology_class.compact_attains_sup.

tts_lemma compact_attains_inf:
  assumes "S ⊆ U"
    and "compact S"
    and "S ≠ {}"
  shows "∃x∈S. Ball S ((≤ow) x)"
    is linorder_topology_class.compact_attains_inf.

end

end

text‹\newpage›

end