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