Theory T2_Spaces
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
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)))
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
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 *)
qed
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
end