Theory SML_Ordered_Topological_Spaces

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

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
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

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 τ:
"sCollect (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
"sCollect (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
(
sCollect (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

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 "zU. 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 "zU. 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 "xS. yS. y ow x"
is linorder_topology_class.compact_attains_sup.

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

end

end

text‹\newpage›

end