Theory CZH_EX_TS

(* Copyright 2021 (C) Mihails Milehins *)

section‹Example II: topological spaces›
theory CZH_EX_TS
  imports CZH_Sets_ZQR
begin



subsection‹Background›


text‹
The section presents elements of the foundations of the theory of topological
spaces formalized in ‹ZFC in HOL›. The definitions were adopted 
(with amendments) from the main library of Isabelle/HOL and 
cite‹"kelley_general_1955"›.
›

named_theorems ts_struct_field_simps



subsection‹‹𝒵›-sequence›

locale 𝒵_vfsequence = 𝒵 α + vfsequence 𝔖 for α 𝔖 +
  assumes vrange_vsubset_Vset: "ℛ∘ 𝔖 ⊆∘ Vset α"


text‹Rules.›

lemma 𝒵_vfsequenceI[intro]:
  assumes "𝒵 α" and "vfsequence 𝔖" and "ℛ∘ 𝔖 ⊆∘ Vset α"
  shows "𝒵_vfsequence α 𝔖"
  using assms unfolding 𝒵_vfsequence_def 𝒵_vfsequence_axioms_def by simp

lemmas 𝒵_vfsequenceD[dest] = 𝒵_vfsequence.axioms

lemma 𝒵_vfsequenceE[elim]:
  assumes "𝒵_vfsequence α 𝔖"
  obtains "𝒵 α" and "vfsequence 𝔖" and "ℛ∘ 𝔖 ⊆∘ Vset α"
  using assms by (simp add: 𝒵_vfsequence.axioms(1,2) 𝒵_vfsequence.vrange_vsubset_Vset)
  

text‹Elementary properties.›

context 𝒵_vfsequence
begin

lemma (in 𝒵_vfsequence) 𝒵_vfsequence_vdomain_in_Vset[intro, simp]: 
  "𝒟∘ 𝔖 ∈∘ Vset α"
  using Axiom_of_Infinity vfsequence_vdomain_in_omega by auto

lemma (in 𝒵_vfsequence) 𝒵_vfsequence_vrange_in_Vset[intro, simp]: 
  "ℛ∘ 𝔖 ∈∘ Vset α"
  using vrange_vsubset_Vset vfsequence_vdomain_in_omega by auto

lemma (in 𝒵_vfsequence) 𝒵_vfsequence_struct_in_Vset: "𝔖 ∈∘ Vset α"
  by (auto simp: vrange_vsubset_Vset vsv_Limit_vsv_in_VsetI)

end


subsection‹Topological space›

definition 𝒜 where [ts_struct_field_simps]: "𝒜 = 0"
definition 𝒯 where [ts_struct_field_simps]: "𝒯 = 1ℕ"

locale 𝒵_ts = 𝒵_vfsequence α 𝔖 for α 𝔖 +
  assumes 𝒵_ts_length: "2ℕ ≤ vcard 𝔖" 
    and 𝒵_ts_closed[intro]: "A ∈∘ 𝔖⦇𝒯⦈ ⟹ A ⊆∘ 𝔖⦇𝒜⦈"
    and 𝒵_ts_domain[intro, simp]: "𝔖⦇𝒜⦈ ∈∘ 𝔖⦇𝒯⦈"
    and 𝒵_ts_vintersection[intro]: 
      "A ∈∘ 𝔖⦇𝒯⦈ ⟹ B ∈∘ 𝔖⦇𝒯⦈ ⟹ A ∩∘ B ∈∘ 𝔖⦇𝒯⦈"
    and 𝒵_ts_VUnion[intro]: "X ⊆∘ 𝔖⦇𝒯⦈ ⟹ ⋃∘X ∈∘ 𝔖⦇𝒯⦈"


text‹Rules.›

lemma 𝒵_tsI[intro]:
  assumes "𝒵_vfsequence α 𝔖"
    and "2ℕ ≤ vcard 𝔖"
    and "⋀A. A ∈∘ 𝔖⦇𝒯⦈ ⟹ A ⊆∘ 𝔖⦇𝒜⦈"
    and "𝔖⦇𝒜⦈ ∈∘ 𝔖⦇𝒯⦈"
    and "⋀A B. A ∈∘ 𝔖⦇𝒯⦈ ⟹ B ∈∘ 𝔖⦇𝒯⦈ ⟹ A ∩∘ B ∈∘ 𝔖⦇𝒯⦈"
    and "⋀X. X ⊆∘ 𝔖⦇𝒯⦈ ⟹ ⋃∘X ∈∘ 𝔖⦇𝒯⦈"
  shows "𝒵_ts α 𝔖"
  using assms unfolding 𝒵_ts_def 𝒵_ts_axioms_def by simp

lemma 𝒵_tsD[dest]:
  assumes "𝒵_ts α 𝔖"
  shows "𝒵_vfsequence α 𝔖"
    and "2ℕ ≤ vcard 𝔖"
    and "⋀A. A ∈∘ 𝔖⦇𝒯⦈ ⟹ A ⊆∘ 𝔖⦇𝒜⦈"
    and "𝔖⦇𝒜⦈ ∈∘ 𝔖⦇𝒯⦈"
    and "⋀A B. A ∈∘ 𝔖⦇𝒯⦈ ⟹ B ∈∘ 𝔖⦇𝒯⦈ ⟹ A ∩∘ B ∈∘ 𝔖⦇𝒯⦈"
    and "⋀X. X ⊆∘ 𝔖⦇𝒯⦈ ⟹ ⋃∘X ∈∘ 𝔖⦇𝒯⦈"
  using assms unfolding 𝒵_ts_def 𝒵_ts_axioms_def by auto

lemma 𝒵_tsE[elim]:
  assumes "𝒵_ts α 𝔖"
  obtains "𝒵_vfsequence α 𝔖"
    and "2ℕ ≤ vcard 𝔖"
    and "⋀A. A ∈∘ 𝔖⦇𝒯⦈ ⟹ A ⊆∘ 𝔖⦇𝒜⦈"
    and "𝔖⦇𝒜⦈ ∈∘ 𝔖⦇𝒯⦈"
    and "⋀A B. A ∈∘ 𝔖⦇𝒯⦈ ⟹ B ∈∘ 𝔖⦇𝒯⦈ ⟹ A ∩∘ B ∈∘ 𝔖⦇𝒯⦈"
    and "⋀X. X ⊆∘ 𝔖⦇𝒯⦈ ⟹ ⋃∘X ∈∘ 𝔖⦇𝒯⦈"
  using assms by auto


text‹Elementary properties.›

lemma (in 𝒵_ts) 𝒵_ts_vempty_in_ts: "0 ∈∘ 𝔖⦇𝒯⦈" 
  using 𝒵_ts_VUnion[of 0] by simp



subsection‹Indiscrete topology›

definition ts_indiscrete :: "V ⇒ V"
  where "ts_indiscrete A = [A, set {0, A}]∘"

named_theorems ts_indiscrete_simps

lemma ts_indiscrete_𝒜[ts_indiscrete_simps]: "ts_indiscrete A⦇𝒜⦈ = A"
  unfolding ts_indiscrete_def by (auto simp: ts_struct_field_simps)

lemma ts_indiscrete_𝒯[ts_indiscrete_simps]: "ts_indiscrete A⦇𝒯⦈ = set {0, A}"
  unfolding ts_indiscrete_def 
  by (simp add: ts_struct_field_simps nat_omega_simps)

lemma (in 𝒵) 𝒵_ts_ts_indiscrete:
  assumes "A ∈∘ Vset α"
  shows "𝒵_ts α (ts_indiscrete A)"
proof(intro 𝒵_tsI)

  show struct: "𝒵_vfsequence α (ts_indiscrete A)"
  proof(intro 𝒵_vfsequenceI)
    show "vfsequence (ts_indiscrete A)" unfolding ts_indiscrete_def by auto
    show "ℛ∘ (ts_indiscrete A) ⊆∘ Vset α"
    proof(intro vsubsetI)
      fix x assume "x ∈∘ ℛ∘ (ts_indiscrete A)" 
      then consider ‹x = A› | ‹x = set {0, A}›
        unfolding ts_indiscrete_def by auto
      then show "x ∈∘ Vset α" by cases (simp_all add: Axiom_of_Pairing assms)
    qed
  qed (simp_all add: 𝒵_axioms)
  
  interpret struct: 𝒵_vfsequence α ‹ts_indiscrete A› by (rule struct)

  show "X ⊆∘ ts_indiscrete A⦇𝒯⦈ ⟹ ⋃∘X ∈∘ ts_indiscrete A⦇𝒯⦈" for X
    unfolding ts_indiscrete_simps
  proof-
    assume "X ⊆∘ set {0, A}"
    then have "X ∈∘ VPow (set {0, A})" by force
    then consider ‹X = 0› | ‹X = set {0}› | ‹X = set {A}› | ‹X = set {0, A}›
      by auto
    then show "⋃∘X ∈∘ set {0, A}" by cases auto
  qed

  show "2ℕ ⊆∘ vcard (ts_indiscrete A)" unfolding ts_indiscrete_def by fastforce

qed (auto simp: ts_indiscrete_simps)

text‹\newpage›

end