1(* Title: HOL/Types_To_Sets/Examples/T2_Spaces.thy 2 Author: Ond��ej Kun��ar, TU M��nchen 3*) 4 5theory T2_Spaces 6 imports Complex_Main "../Types_To_Sets" Prerequisites 7begin 8 9section \<open>The Type-Based Theorem\<close> 10 11text\<open>We relativize a theorem that contains a type class with an associated (overloaded) operation. 12 The key technique is to compile out the overloaded operation by the dictionary construction 13 using the Unoverloading rule.\<close> 14 15text\<open>This is the type-based statement that we want to relativize.\<close> 16thm compact_imp_closed 17text\<open>The type is class a T2 typological space.\<close> 18typ "'a :: t2_space" 19text\<open>The associated operation is the predicate open that determines the open sets in the T2 space.\<close> 20term "open" 21 22section \<open>Definitions and Setup for The Relativization\<close> 23 24text\<open>We gradually define relativization of topological spaces, t2 spaces, compact and closed 25 predicates and prove that they are indeed the relativization of the original predicates.\<close> 26 27definition topological_space_on_with :: "'a set \<Rightarrow> ('a set \<Rightarrow> bool) \<Rightarrow> bool" 28 where "topological_space_on_with A \<equiv> \<lambda>open. open A \<and> 29 (\<forall>S \<subseteq> A. \<forall>T \<subseteq> A. open S \<longrightarrow> open T \<longrightarrow> open (S \<inter> T)) 30 \<and> (\<forall>K \<subseteq> Pow A. (\<forall>S\<in>K. open S) \<longrightarrow> open (\<Union>K))" 31 32lemma topological_space_transfer[transfer_rule]: 33 includes lifting_syntax 34 assumes [transfer_rule]: "right_total T" "bi_unique T" 35 shows "((rel_set T ===> (=)) ===> (=)) (topological_space_on_with (Collect (Domainp T))) 36 class.topological_space" 37 unfolding topological_space_on_with_def[abs_def] class.topological_space_def[abs_def] 38 apply transfer_prover_start 39 apply transfer_step+ 40 unfolding Pow_def Ball_Collect[symmetric] 41 by blast 42 43definition t2_space_on_with :: "'a set \<Rightarrow> ('a set \<Rightarrow> bool) \<Rightarrow> bool" 44 where "t2_space_on_with A \<equiv> \<lambda>open. topological_space_on_with A open \<and> 45 (\<forall>x \<in> A. \<forall>y \<in> A. x \<noteq> y \<longrightarrow> (\<exists>U\<subseteq>A. \<exists>V\<subseteq>A. open U \<and> open V \<and> x \<in> U \<and> y \<in> V \<and> U \<inter> V = {}))" 46 47lemma t2_space_transfer[transfer_rule]: 48 includes lifting_syntax 49 assumes [transfer_rule]: "right_total T" "bi_unique T" 50 shows "((rel_set T ===> (=)) ===> (=)) (t2_space_on_with (Collect (Domainp T))) class.t2_space" 51 unfolding t2_space_on_with_def[abs_def] class.t2_space_def[abs_def] 52 class.t2_space_axioms_def[abs_def] 53 apply transfer_prover_start 54 apply transfer_step+ 55 unfolding Ball_Collect[symmetric] 56 by blast 57 58definition closed_with :: "('a set \<Rightarrow> bool) \<Rightarrow> 'a set \<Rightarrow> bool" 59 where "closed_with \<equiv> \<lambda>open S. open (- S)" 60 61lemma closed_closed_with: "closed s = closed_with open s" 62 unfolding closed_with_def closed_def[abs_def] .. 63 64definition closed_on_with :: "'a set \<Rightarrow> ('a set \<Rightarrow> bool) \<Rightarrow> 'a set \<Rightarrow> bool" 65 where "closed_on_with A \<equiv> \<lambda>open S. open (-S \<inter> A)" 66 67lemma closed_with_transfer[transfer_rule]: 68 includes lifting_syntax 69 assumes [transfer_rule]: "right_total T" "bi_unique T" 70 shows "((rel_set T ===> (=)) ===> rel_set T===> (=)) (closed_on_with (Collect (Domainp T))) 71 closed_with" 72 unfolding closed_with_def closed_on_with_def by transfer_prover 73 74definition compact_with :: "('a set \<Rightarrow> bool) \<Rightarrow> 'a set \<Rightarrow> bool" 75 where "compact_with \<equiv> \<lambda>open S. (\<forall>C. (\<forall>c\<in>C. open c) \<and> S \<subseteq> \<Union>C \<longrightarrow> (\<exists>D\<subseteq>C. finite D \<and> S \<subseteq> \<Union>D))" 76 77lemma compact_compact_with: "compact s = compact_with open s" 78 unfolding compact_with_def compact_eq_Heine_Borel[abs_def] .. 79 80definition compact_on_with :: "'a set \<Rightarrow> ('a set \<Rightarrow> bool) \<Rightarrow> 'a set \<Rightarrow> bool" 81 where "compact_on_with A \<equiv> \<lambda>open S. (\<forall>C\<subseteq>Pow A. (\<forall>c\<in>C. open c) \<and> S \<subseteq> \<Union>C \<longrightarrow> 82 (\<exists>D\<subseteq>C. finite D \<and> S \<subseteq> \<Union>D))" 83 84lemma compact_on_with_subset_trans: "(\<forall>C\<subseteq>Pow A. (\<forall>c\<in>C. open' c) \<and> S \<subseteq> \<Union>C \<longrightarrow> 85 (\<exists>D\<subseteq>C. finite D \<and> S \<subseteq> \<Union>D)) = 86 ((\<forall>C\<subseteq>Pow A. (\<forall>c\<in>C. open' c) \<and> S \<subseteq> \<Union>C \<longrightarrow> (\<exists>D\<subseteq>Pow A. D\<subseteq>C \<and> finite D \<and> S \<subseteq> \<Union>D)))" 87 by (meson subset_trans) 88 89lemma compact_with_transfer[transfer_rule]: 90 includes lifting_syntax 91 assumes [transfer_rule]: "right_total T" "bi_unique T" 92 shows "((rel_set T ===> (=)) ===> rel_set T===> (=)) (compact_on_with (Collect (Domainp T))) 93 compact_with" 94 unfolding compact_with_def compact_on_with_def 95 apply transfer_prover_start 96 apply transfer_step+ 97 unfolding compact_on_with_subset_trans 98 unfolding Pow_def Ball_Collect[symmetric] Ball_def Bex_def mem_Collect_eq 99 by blast 100 101setup \<open>Sign.add_const_constraint 102 (\<^const_name>\<open>open\<close>, SOME \<^typ>\<open>'a set \<Rightarrow> bool\<close>)\<close> 103 104text\<open>The aforementioned development can be automated. The main part is already automated 105 by the transfer_prover.\<close> 106 107section \<open>The Relativization to The Set-Based Theorem\<close> 108 109text\<open>The first step of the dictionary construction.\<close> 110lemmas dictionary_first_step = compact_imp_closed[unfolded compact_compact_with closed_closed_with] 111thm dictionary_first_step 112 113text\<open>Internalization of the type class t2_space.\<close> 114lemmas internalized_sort = dictionary_first_step[internalize_sort "'a::t2_space"] 115thm internalized_sort 116 117text\<open>We unoverload the overloaded constant open and thus finish compiling out of it.\<close> 118lemmas dictionary_second_step = internalized_sort[unoverload "open :: 'a set \<Rightarrow> bool"] 119text\<open>The theorem with internalized type classes and compiled out operations is the starting point 120 for the original relativization algorithm.\<close> 121thm dictionary_second_step 122 123text \<open>Alternative construction using \<open>unoverload_type\<close> 124 (This does not require fiddling with \<open>Sign.add_const_constraint\<close>).\<close> 125lemmas dictionary_second_step' = dictionary_first_step[unoverload_type 'a] 126 127text\<open>This is the set-based variant of the theorem compact_imp_closed.\<close> 128lemma compact_imp_closed_set_based: 129 assumes "(A::'a set) \<noteq> {}" 130 shows "\<forall>open. t2_space_on_with A open \<longrightarrow> (\<forall>S\<subseteq>A. compact_on_with A open S \<longrightarrow> 131 closed_on_with A open S)" 132proof - 133 { 134 text\<open>We define the type 'b to be isomorphic to A.\<close> 135 assume T: "\<exists>(Rep :: 'b \<Rightarrow> 'a) Abs. type_definition Rep Abs A" 136 from T obtain rep :: "'b \<Rightarrow> 'a" and abs :: "'a \<Rightarrow> 'b" where t: "type_definition rep abs A" 137 by auto 138 139 text\<open>Setup for the Transfer tool.\<close> 140 define cr_b where "cr_b == \<lambda>r a. r = rep a" 141 note type_definition_Domainp[OF t cr_b_def, transfer_domain_rule] 142 note typedef_right_total[OF t cr_b_def, transfer_rule] 143 note typedef_bi_unique[OF t cr_b_def, transfer_rule] 144 145 have ?thesis 146 text\<open>Relativization by the Transfer tool.\<close> 147 using dictionary_second_step[where 'a = 'b, untransferred, simplified] 148 by blast 149 150 } note * = this[cancel_type_definition, OF assms] 151 152 show ?thesis by (rule *) 153qed 154 155setup \<open>Sign.add_const_constraint 156 (\<^const_name>\<open>open\<close>, SOME \<^typ>\<open>'a::topological_space set \<Rightarrow> bool\<close>)\<close> 157 158text\<open>The Final Result. We can compare the type-based and the set-based statement.\<close> 159thm compact_imp_closed compact_imp_closed_set_based 160 161declare [[show_sorts]] 162text\<open>The Final Result. This time with explicitly shown type-class annotations.\<close> 163thm compact_imp_closed compact_imp_closed_set_based 164 165end 166