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