Theory SML_Product_Topology

(* Title: Examples/SML_Relativization/Topology/SML_Product_Topology.thy
   Author: Mihails Milehins
   Copyright 2021 (C) Mihails Milehins
*)
section‹Relativization of the results about product topologies›
theory SML_Product_Topology
  imports 
    SML_Topological_Space
    "../Foundations/Product_Type_Ext"
begin



subsection‹Definitions and common properties›

ud‹
  open_prod_inst.open_prod::
    ('a::topological_space × 'b::topological_space) set ⇒ _
  ›
ud‹open::('a::topological_space × 'b::topological_space) set ⇒ bool›

ctr relativization
  synthesis ctr_simps
  assumes [transfer_domain_rule, transfer_rule]: 
    "Domainp B = (λx. x ∈ U1)" "Domainp A = (λx. x ∈ U2)"
    and [transfer_rule]: "bi_unique A" "right_total A"
      "bi_unique B" "right_total B"
  trp (?'a A) and (?'b B) 
  in open_ow: open_prod.with_def
    (‹'(/on _ _ with _ _ : «open» _/')› [1000, 999, 1000, 999, 1000] 10) 

locale product_topology_ow =
  ts1: topological_space_ow U1 τ1 + ts2: topological_space_ow U2 τ2 
  for U1 :: "'at set" and τ1 :: "'at set ⇒ bool" 
    and U2 :: "'bt set"and τ2 :: "'bt set ⇒ bool" +
  fixes τ :: "('at × 'bt) set ⇒ bool"
  assumes open_prod[tts_implicit]: "τ = open_ow U1 U2 τ2 τ1"
begin 

sublocale topological_space_ow ‹U1 × U2› τ
proof
  let ?U = "U1 × U2"  
  have open_prod': "τ S = open_ow U1 U2 τ2 τ1 S" for S
    by (simp only: open_prod)
  note op = open_prod'[unfolded open_ow_def, THEN iffD2, rule_format]
  show "τ (U1 × U2)" by (rule op) auto   
  show "⟦ S ⊆ ?U; T ⊆ ?U; τ S; τ T ⟧ ⟹ τ (S ∩ T)" for S T
  proof-
    assume "S ⊆ ?U" and "T ⊆ ?U" and "τ S" and "τ T"
    from ‹S ⊆ ?U› ‹T ⊆ ?U› have "S ∩ T ⊆ ?U" by auto
    show "τ (S ∩ T)"
    proof(rule op)
      fix x assume "x ∈ S ∩ T"
      then have "x ∈ S" and "x ∈ T" by auto
      from open_prod'[
          unfolded open_ow_def, THEN iffD1, rule_format, OF ‹τ S› ‹x ∈ S›
          ]
      obtain AS BS where 
        "AS ⊆ U1" "BS ⊆ U2" "τ1 AS" "τ2 BS" "x ∈ AS × BS" "AS × BS ⊆ S" 
        by auto 
      from open_prod'[
          unfolded open_ow_def, THEN iffD1, rule_format, 
          OF ‹τ T› ‹x ∈ T›
          ]
      obtain AT BT where 
        "AT ⊆ U1" "BT ⊆ U2" "τ1 AT" "τ2 BT" "x ∈ AT × BT" "AT × BT ⊆ T" 
        by auto
      from ‹AS ⊆ U1› ‹AT ⊆ U1› have "AS ∩ AT ⊆ U1" by auto
      moreover from ‹BS ⊆ U2› ‹BT ⊆ U2› have "BS ∩ BT ⊆ U2" by auto
      moreover from ‹AS ⊆ U1› ‹AT ⊆ U1› ‹τ1 AS› ‹τ1 AT› have "τ1 (AS ∩ AT)" 
        by auto
      moreover from ‹BS ⊆ U2› ‹BT ⊆ U2› ‹τ2 BS› ‹τ2 BT› have "τ2 (BS ∩ BT)" 
        by auto
      moreover from ‹x ∈ AS × BS› ‹x ∈ AT × BT› have 
        "x ∈ (AS ∩ AT) × (BS ∩ BT)"
        by clarsimp
      moreover from ‹AS × BS ⊆ S› ‹AT × BT ⊆ T› have 
        "(AS ∩ AT) × (BS ∩ BT) ⊆ S ∩ T"
        by auto
      ultimately show 
        "∃A∈Pow U1. ∃B∈Pow U2. τ1 A ∧ τ2 B ∧ A × B ⊆ S ∩ T ∧ x ∈ A × B" 
        by auto
    qed
  qed
  show "⟦ K ⊆ Pow ?U; ∀S∈K. τ S ⟧ ⟹ τ (⋃K)" for K
  proof -
    assume "K ⊆ Pow ?U" and "∀S∈K. τ S" 
    from ‹K ⊆ Pow ?U› have "⋃K ⊆ ?U" by auto
    show "τ (⋃K)"
    proof(rule op)
      fix x assume "x ∈ ⋃K"
      then obtain k where k: "x ∈ k" and "k ∈ K" by clarsimp
      from ‹k ∈ K› have "k ⊆ ⋃K" by auto
      from ‹k ∈ K› have "τ k" by (rule ‹∀S∈K. τ S›[rule_format])
      from open_prod'[
          unfolded open_ow_def, THEN iffD1, rule_format,
          OF this ‹x ∈ k›
          ]
      obtain A B where 
        "A ⊆ U1" "B ⊆ U2" "τ1 A" "τ2 B" "x ∈ A × B" "A × B ⊆ k"
        by auto
      from ‹A × B ⊆ k› ‹k ⊆ ⋃K› have "A × B ⊆ ⋃K" by simp
      from ‹A ⊆ U1› ‹B ⊆ U2› ‹τ1 A› ‹τ2 B› ‹x ∈ A × B› this show 
        " ∃A∈Pow U1. ∃B∈Pow U2. τ1 A ∧ τ2 B ∧ A × B ⊆ ⋃ K ∧ x ∈ A × B"
        by auto
    qed
  qed
qed

end



subsection‹Transfer rules›

lemma (in product_topology_ow) open_with_oo_transfer[transfer_rule]:
  includes lifting_syntax
  fixes A :: "['at, 'a] ⇒ bool"
    and B :: "['bt, 'b] ⇒ bool"
  assumes tdr_U1[transfer_domain_rule]: "Domainp A = (λx. x ∈ U1)"
    and [transfer_rule]: "bi_unique A" "right_total A"  
    and tdr_U2[transfer_domain_rule]: "Domainp B = (λx. x ∈ U2)"
    and [transfer_rule]: "bi_unique B" "right_total B" 
    and τ1τ1'[transfer_rule]: "(rel_set A ===> (=)) τ1 τ1'"
    and τ2τ2'[transfer_rule]: "(rel_set B ===> (=)) τ2 τ2'"
  shows "(rel_set (rel_prod A B) ===> (=)) τ (open_prod.with τ2' τ1')"
  unfolding open_prod.with_def
  apply transfer_prover_start
  apply transfer_step+
  apply simp
  apply(fold subset_eq)
  unfolding open_prod open_ow_def tdr_U1 tdr_U2 
  by (meson Pow_iff)



subsection‹Relativization›

context product_topology_ow
begin

tts_context
  tts: (?'a to U1) and (?'b to U2)
  rewriting ctr_simps
  substituting ts1.topological_space_ow_axioms 
    and ts2.topological_space_ow_axioms
  eliminating ‹?U ≠ {}› through (fold tts_implicit, insert closed_empty, simp)
  applying [folded tts_implicit]
begin

tts_lemma open_prod_intro:
  assumes "S ⊆ U1 × U2"
    and "⋀x. ⟦x ∈ U1 × U2; x ∈ S⟧ ⟹ 
      ∃A∈Pow U1. ∃B∈Pow U2. τ1 A ∧ τ2 B ∧ A × B ⊆ S ∧ x ∈ A × B"
  shows "τ S"
    is open_prod_intro.

tts_lemma open_Times:
  assumes "S ⊆ U1" and "T ⊆ U2" and "τ1 S" and "τ2 T"
  shows "τ (S × T)"
    is open_Times.
    
tts_lemma open_vimage_fst:
  assumes "S ⊆ U1" and "τ1 S"
  shows "τ (fst -` S ∩ U1 × U2)"
    is open_vimage_fst.

tts_lemma closed_vimage_fst:
  assumes "S ⊆ U1" and "ts1.closed S"
  shows "closed (fst -` S ∩ U1 × U2)"
    is closed_vimage_fst.

tts_lemma closed_Times:
  assumes "S ⊆ U1" and "T ⊆ U2" and "ts1.closed S" and "ts2.closed T"
  shows "closed (S × T)"
    is closed_Times.

tts_lemma open_image_fst:
  assumes "S ⊆ U1 × U2" and "τ S"
  shows "τ1 (fst ` S)"
    is open_image_fst.

tts_lemma open_image_snd:
  assumes "S ⊆ U1 × U2" and "τ S"
  shows "τ2 (snd ` S)"
    is open_image_snd.

end

tts_context
  tts: (?'a to U1) and (?'b to U2)
  rewriting ctr_simps
  substituting ts1.topological_space_ow_axioms 
    and ts2.topological_space_ow_axioms
  eliminating ‹?U ≠ {}› 
    through (fold tts_implicit, unfold connected_ow_def, simp)
  applying [folded tts_implicit]
begin

tts_lemma connected_Times:
  assumes "S ⊆ U1" and "T ⊆ U2" and "ts1.connected S" and "ts2.connected T"
  shows "connected (S × T)"
    is connected_Times.
    
tts_lemma connected_Times_eq:
  assumes "S ⊆ U1" and "T ⊆ U2"
  shows 
    "connected (S × T) = (S = {} ∨ T = {} ∨ ts1.connected S ∧ ts2.connected T)"
  is connected_Times_eq.
                
end

tts_context
  tts: (?'b to U1) and (?'a to U2)
  rewriting ctr_simps
  substituting ts1.topological_space_ow_axioms 
    and ts2.topological_space_ow_axioms
  eliminating ‹?U ≠ {}› through (fold tts_implicit, insert closed_empty, simp)
  applying [folded tts_implicit]
begin

tts_lemma open_vimage_snd:
  assumes "S ⊆ U2" and "τ2 S"
  shows "τ (snd -` S ∩ U1 × U2)"
    is open_vimage_snd.

tts_lemma closed_vimage_snd:
  assumes "S ⊆ U2" and "ts2.closed S"
  shows "closed (snd -` S ∩ U1 × U2)"
    is closed_vimage_snd.

end

end

text‹\newpage›

end