(* 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 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