64551
|
1 |
(* Title: HOL/Types_To_Sets/Examples/T2_Spaces.thy
|
|
2 |
Author: Ondřej Kunčar, TU München
|
|
3 |
*)
|
|
4 |
|
|
5 |
theory T2_Spaces
|
|
6 |
imports Complex_Main "../Types_To_Sets" Prerequisites
|
|
7 |
begin
|
|
8 |
|
|
9 |
section \<open>The Type-Based Theorem\<close>
|
|
10 |
|
|
11 |
text\<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 |
|
|
15 |
text\<open>This is the type-based statement that we want to relativize.\<close>
|
|
16 |
thm compact_imp_closed
|
|
17 |
text\<open>The type is class a T2 typological space.\<close>
|
|
18 |
typ "'a :: t2_space"
|
|
19 |
text\<open>The associated operation is the predicate open that determines the open sets in the T2 space.\<close>
|
|
20 |
term "open"
|
|
21 |
|
|
22 |
section \<open>Definitions and Setup for The Relativization\<close>
|
|
23 |
|
|
24 |
text\<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 |
|
|
27 |
definition 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 |
|
|
32 |
lemma topological_space_transfer[transfer_rule]:
|
|
33 |
includes lifting_syntax
|
|
34 |
assumes [transfer_rule]: "right_total T" "bi_unique T"
|
|
35 |
shows "((rel_set T ===> op=) ===> op=) (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 |
|
|
43 |
definition 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 |
|
|
47 |
lemma t2_space_transfer[transfer_rule]:
|
|
48 |
includes lifting_syntax
|
|
49 |
assumes [transfer_rule]: "right_total T" "bi_unique T"
|
|
50 |
shows "((rel_set T ===> op=) ===> op=) (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 |
|
|
58 |
definition closed_with :: "('a set \<Rightarrow> bool) \<Rightarrow> 'a set \<Rightarrow> bool"
|
|
59 |
where "closed_with \<equiv> \<lambda>open S. open (- S)"
|
|
60 |
|
|
61 |
lemma closed_closed_with: "closed s = closed_with open s"
|
|
62 |
unfolding closed_with_def closed_def[abs_def] ..
|
|
63 |
|
|
64 |
definition 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 |
|
|
67 |
lemma closed_with_transfer[transfer_rule]:
|
|
68 |
includes lifting_syntax
|
|
69 |
assumes [transfer_rule]: "right_total T" "bi_unique T"
|
|
70 |
shows "((rel_set T ===> op=) ===> rel_set T===> op=) (closed_on_with (Collect (Domainp T)))
|
|
71 |
closed_with"
|
|
72 |
unfolding closed_with_def closed_on_with_def by transfer_prover
|
|
73 |
|
|
74 |
definition 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 |
|
|
77 |
lemma compact_compact_with: "compact s = compact_with open s"
|
|
78 |
unfolding compact_with_def compact_eq_heine_borel[abs_def] ..
|
|
79 |
|
|
80 |
definition 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 |
|
|
84 |
lemma 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 |
|
|
89 |
lemma compact_with_transfer[transfer_rule]:
|
|
90 |
includes lifting_syntax
|
|
91 |
assumes [transfer_rule]: "right_total T" "bi_unique T"
|
|
92 |
shows "((rel_set T ===> op=) ===> rel_set T===> op=) (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 |
|
|
101 |
setup \<open>Sign.add_const_constraint
|
|
102 |
(@{const_name "open"}, SOME @{typ "'a set \<Rightarrow> bool"})\<close>
|
|
103 |
|
|
104 |
text\<open>The aforementioned development can be automated. The main part is already automated
|
|
105 |
by the transfer_prover.\<close>
|
|
106 |
|
|
107 |
section \<open>The Relativization to The Set-Based Theorem\<close>
|
|
108 |
|
|
109 |
text\<open>The first step of the dictionary construction.\<close>
|
|
110 |
lemmas dictionary_first_step = compact_imp_closed[unfolded compact_compact_with closed_closed_with]
|
|
111 |
thm dictionary_first_step
|
|
112 |
|
|
113 |
text\<open>Internalization of the type class t2_space.\<close>
|
|
114 |
lemmas internalized_sort = dictionary_first_step[internalize_sort "'a::t2_space"]
|
|
115 |
thm internalized_sort
|
|
116 |
|
|
117 |
text\<open>We unoverload the overloaded constant open and thus finish compiling out of it.\<close>
|
|
118 |
lemmas dictionary_second_step = internalized_sort[unoverload "open :: 'a set \<Rightarrow> bool"]
|
|
119 |
text\<open>The theorem with internalized type classes and compiled out operations is the starting point
|
|
120 |
for the original relativization algorithm.\<close>
|
|
121 |
thm dictionary_second_step
|
|
122 |
|
|
123 |
|
|
124 |
text\<open>This is the set-based variant of the theorem compact_imp_closed.\<close>
|
|
125 |
lemma compact_imp_closed_set_based:
|
|
126 |
assumes "(A::'a set) \<noteq> {}"
|
|
127 |
shows "\<forall>open. t2_space_on_with A open \<longrightarrow> (\<forall>S\<subseteq>A. compact_on_with A open S \<longrightarrow>
|
|
128 |
closed_on_with A open S)"
|
|
129 |
proof -
|
|
130 |
{
|
|
131 |
text\<open>We define the type 'b to be isomorphic to A.\<close>
|
|
132 |
assume T: "\<exists>(Rep :: 'b \<Rightarrow> 'a) Abs. type_definition Rep Abs A"
|
|
133 |
from T obtain rep :: "'b \<Rightarrow> 'a" and abs :: "'a \<Rightarrow> 'b" where t: "type_definition rep abs A"
|
|
134 |
by auto
|
|
135 |
|
|
136 |
text\<open>Setup for the Transfer tool.\<close>
|
|
137 |
define cr_b where "cr_b == \<lambda>r a. r = rep a"
|
|
138 |
note type_definition_Domainp[OF t cr_b_def, transfer_domain_rule]
|
|
139 |
note typedef_right_total[OF t cr_b_def, transfer_rule]
|
|
140 |
note typedef_bi_unique[OF t cr_b_def, transfer_rule]
|
|
141 |
|
|
142 |
have ?thesis
|
|
143 |
text\<open>Relativization by the Transfer tool.\<close>
|
|
144 |
using dictionary_second_step[where 'a = 'b, untransferred, simplified]
|
|
145 |
by blast
|
|
146 |
|
|
147 |
} note * = this[cancel_type_definition, OF assms]
|
|
148 |
|
|
149 |
show ?thesis by (rule *)
|
|
150 |
qed
|
|
151 |
|
|
152 |
setup \<open>Sign.add_const_constraint
|
|
153 |
(@{const_name "open"}, SOME @{typ "'a::topological_space set \<Rightarrow> bool"})\<close>
|
|
154 |
|
|
155 |
text\<open>The Final Result. We can compare the type-based and the set-based statement.\<close>
|
|
156 |
thm compact_imp_closed compact_imp_closed_set_based
|
|
157 |
|
|
158 |
declare [[show_sorts]]
|
|
159 |
text\<open>The Final Result. This time with explicitly shown type-class annotations.\<close>
|
|
160 |
thm compact_imp_closed compact_imp_closed_set_based
|
|
161 |
|
|
162 |
end
|