src/HOL/Types_To_Sets/Examples/T2_Spaces.thy
 author wenzelm Mon Dec 12 11:33:14 2016 +0100 (2016-12-12 ago) changeset 64551 79e9587dbcca child 67399 eab6ce8368fa permissions -rw-r--r--
proper session HOL-Types_To_Sets;
NEWS;
CONTRIBUTORS;
tuned whitespace;
```     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
```