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

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

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)))
class.topological_space"
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]
class.t2_space_axioms_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)))
closed_with"
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)))
compact_with"
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

(@{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 *)
qed