Theory T2_Spaces

theory T2_Spaces
imports Complex_Main Types_To_Sets Prerequisites
(*  Title:      HOL/Types_To_Sets/Examples/T2_Spaces.thy
    Author:     Ondřej Kunčar, TU München

theory T2_Spaces
  imports Complex_Main "../Types_To_Sets" Prerequisites

section ‹The Type-Based Theorem›

text‹We relativize a theorem that contains a type class with an associated (overloaded) operation.
     The key technique is to compile out the overloaded operation by the dictionary construction
     using the Unoverloading rule.›

text‹This is the type-based statement that we want to relativize.›
thm compact_imp_closed
text‹The type is class a T2 typological space.›
typ "'a :: t2_space"
text‹The associated operation is the predicate open that determines the open sets in the T2 space.›
term "open"

section ‹Definitions and Setup for The Relativization›

text‹We gradually define relativization of topological spaces, t2 spaces, compact and closed
     predicates and prove that they are indeed the relativization of the original predicates.›

definition topological_space_on_with :: "'a set ⇒ ('a set ⇒ bool) ⇒ bool"
  where "topological_space_on_with A ≡ λopen. open A ∧
    (∀S ⊆ A. ∀T ⊆ A. open S ⟶ open T ⟶ open (S ∩ T))
    ∧ (∀K ⊆ Pow A. (∀S∈K. open S) ⟶ open (⋃K))"

lemma topological_space_transfer[transfer_rule]:
  includes lifting_syntax
  assumes [transfer_rule]: "right_total T" "bi_unique T"
  shows "((rel_set T ===> (=)) ===> (=)) (topological_space_on_with (Collect (Domainp T)))
  unfolding topological_space_on_with_def[abs_def] class.topological_space_def[abs_def]
  apply transfer_prover_start
  apply transfer_step+
  unfolding Pow_def Ball_Collect[symmetric]
  by blast

definition t2_space_on_with :: "'a set ⇒ ('a set ⇒ bool) ⇒ bool"
  where "t2_space_on_with A ≡ λopen. topological_space_on_with A open ∧
  (∀x ∈ A. ∀y ∈ A. x ≠ y ⟶ (∃U⊆A. ∃V⊆A. open U ∧ open V ∧ x ∈ U ∧ y ∈ V ∧ U ∩ V = {}))"

lemma t2_space_transfer[transfer_rule]:
  includes lifting_syntax
  assumes [transfer_rule]: "right_total T" "bi_unique T"
  shows "((rel_set T ===> (=)) ===> (=)) (t2_space_on_with (Collect (Domainp T))) class.t2_space"
  unfolding t2_space_on_with_def[abs_def] class.t2_space_def[abs_def]
  apply transfer_prover_start
  apply transfer_step+
  unfolding Ball_Collect[symmetric]
  by blast

definition closed_with :: "('a set ⇒ bool) ⇒ 'a set ⇒ bool"
  where "closed_with ≡ λopen S. open (- S)"

lemma closed_closed_with: "closed s = closed_with open s"
  unfolding closed_with_def closed_def[abs_def] ..

definition closed_on_with :: "'a set ⇒ ('a set ⇒ bool) ⇒ 'a set ⇒ bool"
  where "closed_on_with A ≡ λopen S. open (-S ∩ A)"

lemma closed_with_transfer[transfer_rule]:
  includes lifting_syntax
  assumes [transfer_rule]: "right_total T" "bi_unique T"
  shows "((rel_set T ===> (=)) ===> rel_set T===> (=)) (closed_on_with (Collect (Domainp T)))
  unfolding closed_with_def closed_on_with_def by transfer_prover

definition compact_with :: "('a set ⇒ bool) ⇒ 'a set ⇒ bool"
  where "compact_with ≡ λopen S. (∀C. (∀c∈C. open c) ∧ S ⊆ ⋃C ⟶ (∃D⊆C. finite D ∧ S ⊆ ⋃D))"

lemma compact_compact_with: "compact s = compact_with open s"
  unfolding compact_with_def compact_eq_heine_borel[abs_def] ..

definition compact_on_with :: "'a set ⇒ ('a set ⇒ bool) ⇒ 'a set ⇒ bool"
  where "compact_on_with A ≡ λopen S. (∀C⊆Pow A. (∀c∈C. open c) ∧ S ⊆ ⋃C ⟶
    (∃D⊆C. finite D ∧ S ⊆ ⋃D))"

lemma compact_on_with_subset_trans: "(∀C⊆Pow A. (∀c∈C. open' c) ∧ S ⊆ ⋃C ⟶
  (∃D⊆C. finite D ∧ S ⊆ ⋃D)) =
  ((∀C⊆Pow A. (∀c∈C. open' c) ∧ S ⊆ ⋃C ⟶ (∃D⊆Pow A. D⊆C ∧ finite D ∧ S ⊆ ⋃D)))"
  by (meson subset_trans)

lemma compact_with_transfer[transfer_rule]:
  includes lifting_syntax
  assumes [transfer_rule]: "right_total T" "bi_unique T"
  shows "((rel_set T ===> (=)) ===> rel_set T===> (=)) (compact_on_with (Collect (Domainp T)))
  unfolding compact_with_def compact_on_with_def
  apply transfer_prover_start
  apply transfer_step+
  unfolding compact_on_with_subset_trans
  unfolding Pow_def Ball_Collect[symmetric] Ball_def Bex_def mem_Collect_eq
  by blast

setup ‹Sign.add_const_constraint
  (@{const_name "open"}, SOME @{typ "'a set ⇒ bool"})›

text‹The aforementioned development can be automated. The main part is already automated
     by the transfer_prover.›

section ‹The Relativization to The Set-Based Theorem›

text‹The first step of the dictionary construction.›
lemmas dictionary_first_step = compact_imp_closed[unfolded compact_compact_with closed_closed_with]
thm dictionary_first_step

text‹Internalization of the type class t2_space.›
lemmas internalized_sort = dictionary_first_step[internalize_sort "'a::t2_space"]
thm internalized_sort

text‹We unoverload the overloaded constant open and thus finish compiling out of it.›
lemmas dictionary_second_step =  internalized_sort[unoverload "open :: 'a set ⇒ bool"]
text‹The theorem with internalized type classes and compiled out operations is the starting point
     for the original relativization algorithm.›
thm dictionary_second_step

text ‹Alternative construction using ‹unoverload_type›
  (This does not require fiddling with ‹Sign.add_const_constraint›).›
lemmas dictionary_second_step' = dictionary_first_step[unoverload_type 'a]

text‹This is the set-based variant of the theorem compact_imp_closed.›
lemma compact_imp_closed_set_based:
  assumes "(A::'a set) ≠ {}"
  shows "∀open. t2_space_on_with A open ⟶ (∀S⊆A. compact_on_with A open S ⟶
    closed_on_with A open S)"
proof -
    text‹We define the type 'b to be isomorphic to A.›
    assume T: "∃(Rep :: 'b ⇒ 'a) Abs. type_definition Rep Abs A"
    from T obtain rep :: "'b ⇒ 'a" and abs :: "'a ⇒ 'b" where t: "type_definition rep abs A"
      by auto

    text‹Setup for the Transfer tool.›
    define cr_b where "cr_b == λr a. r = rep a"
    note type_definition_Domainp[OF t cr_b_def, transfer_domain_rule]
    note typedef_right_total[OF t cr_b_def, transfer_rule]
    note typedef_bi_unique[OF t cr_b_def, transfer_rule]

    have ?thesis
      text‹Relativization by the Transfer tool.›
      using dictionary_second_step[where 'a = 'b, untransferred, simplified]
      by blast

  } note * = this[cancel_type_definition, OF assms]

  show ?thesis by (rule *)

setup ‹Sign.add_const_constraint
  (@{const_name "open"}, SOME @{typ "'a::topological_space set ⇒ bool"})›

text‹The Final Result. We can compare the type-based and the set-based statement.›
thm compact_imp_closed compact_imp_closed_set_based

declare [[show_sorts]]
text‹The Final Result. This time with explicitly shown type-class annotations.›
thm compact_imp_closed compact_imp_closed_set_based