src/HOL/Types_To_Sets/Examples/T2_Spaces.thy
changeset 64551 79e9587dbcca
child 67399 eab6ce8368fa
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/Types_To_Sets/Examples/T2_Spaces.thy	Mon Dec 12 11:33:14 2016 +0100
     1.3 @@ -0,0 +1,162 @@
     1.4 +(*  Title:      HOL/Types_To_Sets/Examples/T2_Spaces.thy
     1.5 +    Author:     Ondřej Kunčar, TU München
     1.6 +*)
     1.7 +
     1.8 +theory T2_Spaces
     1.9 +  imports Complex_Main "../Types_To_Sets" Prerequisites
    1.10 +begin
    1.11 +
    1.12 +section \<open>The Type-Based Theorem\<close>
    1.13 +
    1.14 +text\<open>We relativize a theorem that contains a type class with an associated (overloaded) operation.
    1.15 +     The key technique is to compile out the overloaded operation by the dictionary construction
    1.16 +     using the Unoverloading rule.\<close>
    1.17 +
    1.18 +text\<open>This is the type-based statement that we want to relativize.\<close>
    1.19 +thm compact_imp_closed
    1.20 +text\<open>The type is class a T2 typological space.\<close>
    1.21 +typ "'a :: t2_space"
    1.22 +text\<open>The associated operation is the predicate open that determines the open sets in the T2 space.\<close>
    1.23 +term "open"
    1.24 +
    1.25 +section \<open>Definitions and Setup for The Relativization\<close>
    1.26 +
    1.27 +text\<open>We gradually define relativization of topological spaces, t2 spaces, compact and closed
    1.28 +     predicates and prove that they are indeed the relativization of the original predicates.\<close>
    1.29 +
    1.30 +definition topological_space_on_with :: "'a set \<Rightarrow> ('a set \<Rightarrow> bool) \<Rightarrow> bool"
    1.31 +  where "topological_space_on_with A \<equiv> \<lambda>open. open A \<and>
    1.32 +    (\<forall>S \<subseteq> A. \<forall>T \<subseteq> A. open S \<longrightarrow> open T \<longrightarrow> open (S \<inter> T))
    1.33 +    \<and> (\<forall>K \<subseteq> Pow A. (\<forall>S\<in>K. open S) \<longrightarrow> open (\<Union>K))"
    1.34 +
    1.35 +lemma topological_space_transfer[transfer_rule]:
    1.36 +  includes lifting_syntax
    1.37 +  assumes [transfer_rule]: "right_total T" "bi_unique T"
    1.38 +  shows "((rel_set T ===> op=) ===> op=) (topological_space_on_with (Collect (Domainp T)))
    1.39 +    class.topological_space"
    1.40 +  unfolding topological_space_on_with_def[abs_def] class.topological_space_def[abs_def]
    1.41 +  apply transfer_prover_start
    1.42 +  apply transfer_step+
    1.43 +  unfolding Pow_def Ball_Collect[symmetric]
    1.44 +  by blast
    1.45 +
    1.46 +definition t2_space_on_with :: "'a set \<Rightarrow> ('a set \<Rightarrow> bool) \<Rightarrow> bool"
    1.47 +  where "t2_space_on_with A \<equiv> \<lambda>open. topological_space_on_with A open \<and>
    1.48 +  (\<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 = {}))"
    1.49 +
    1.50 +lemma t2_space_transfer[transfer_rule]:
    1.51 +  includes lifting_syntax
    1.52 +  assumes [transfer_rule]: "right_total T" "bi_unique T"
    1.53 +  shows "((rel_set T ===> op=) ===> op=) (t2_space_on_with (Collect (Domainp T))) class.t2_space"
    1.54 +  unfolding t2_space_on_with_def[abs_def] class.t2_space_def[abs_def]
    1.55 +    class.t2_space_axioms_def[abs_def]
    1.56 +  apply transfer_prover_start
    1.57 +  apply transfer_step+
    1.58 +  unfolding Ball_Collect[symmetric]
    1.59 +  by blast
    1.60 +
    1.61 +definition closed_with :: "('a set \<Rightarrow> bool) \<Rightarrow> 'a set \<Rightarrow> bool"
    1.62 +  where "closed_with \<equiv> \<lambda>open S. open (- S)"
    1.63 +
    1.64 +lemma closed_closed_with: "closed s = closed_with open s"
    1.65 +  unfolding closed_with_def closed_def[abs_def] ..
    1.66 +
    1.67 +definition closed_on_with :: "'a set \<Rightarrow> ('a set \<Rightarrow> bool) \<Rightarrow> 'a set \<Rightarrow> bool"
    1.68 +  where "closed_on_with A \<equiv> \<lambda>open S. open (-S \<inter> A)"
    1.69 +
    1.70 +lemma closed_with_transfer[transfer_rule]:
    1.71 +  includes lifting_syntax
    1.72 +  assumes [transfer_rule]: "right_total T" "bi_unique T"
    1.73 +  shows "((rel_set T ===> op=) ===> rel_set T===> op=) (closed_on_with (Collect (Domainp T)))
    1.74 +    closed_with"
    1.75 +  unfolding closed_with_def closed_on_with_def by transfer_prover
    1.76 +
    1.77 +definition compact_with :: "('a set \<Rightarrow> bool) \<Rightarrow> 'a set \<Rightarrow> bool"
    1.78 +  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))"
    1.79 +
    1.80 +lemma compact_compact_with: "compact s = compact_with open s"
    1.81 +  unfolding compact_with_def compact_eq_heine_borel[abs_def] ..
    1.82 +
    1.83 +definition compact_on_with :: "'a set \<Rightarrow> ('a set \<Rightarrow> bool) \<Rightarrow> 'a set \<Rightarrow> bool"
    1.84 +  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>
    1.85 +    (\<exists>D\<subseteq>C. finite D \<and> S \<subseteq> \<Union>D))"
    1.86 +
    1.87 +lemma compact_on_with_subset_trans: "(\<forall>C\<subseteq>Pow A. (\<forall>c\<in>C. open' c) \<and> S \<subseteq> \<Union>C \<longrightarrow>
    1.88 +  (\<exists>D\<subseteq>C. finite D \<and> S \<subseteq> \<Union>D)) =
    1.89 +  ((\<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)))"
    1.90 +  by (meson subset_trans)
    1.91 +
    1.92 +lemma compact_with_transfer[transfer_rule]:
    1.93 +  includes lifting_syntax
    1.94 +  assumes [transfer_rule]: "right_total T" "bi_unique T"
    1.95 +  shows "((rel_set T ===> op=) ===> rel_set T===> op=) (compact_on_with (Collect (Domainp T)))
    1.96 +    compact_with"
    1.97 +  unfolding compact_with_def compact_on_with_def
    1.98 +  apply transfer_prover_start
    1.99 +  apply transfer_step+
   1.100 +  unfolding compact_on_with_subset_trans
   1.101 +  unfolding Pow_def Ball_Collect[symmetric] Ball_def Bex_def mem_Collect_eq
   1.102 +  by blast
   1.103 +
   1.104 +setup \<open>Sign.add_const_constraint
   1.105 +  (@{const_name "open"}, SOME @{typ "'a set \<Rightarrow> bool"})\<close>
   1.106 +
   1.107 +text\<open>The aforementioned development can be automated. The main part is already automated
   1.108 +     by the transfer_prover.\<close>
   1.109 +
   1.110 +section \<open>The Relativization to The Set-Based Theorem\<close>
   1.111 +
   1.112 +text\<open>The first step of the dictionary construction.\<close>
   1.113 +lemmas dictionary_first_step = compact_imp_closed[unfolded compact_compact_with closed_closed_with]
   1.114 +thm dictionary_first_step
   1.115 +
   1.116 +text\<open>Internalization of the type class t2_space.\<close>
   1.117 +lemmas internalized_sort = dictionary_first_step[internalize_sort "'a::t2_space"]
   1.118 +thm internalized_sort
   1.119 +
   1.120 +text\<open>We unoverload the overloaded constant open and thus finish compiling out of it.\<close>
   1.121 +lemmas dictionary_second_step =  internalized_sort[unoverload "open :: 'a set \<Rightarrow> bool"]
   1.122 +text\<open>The theorem with internalized type classes and compiled out operations is the starting point
   1.123 +     for the original relativization algorithm.\<close>
   1.124 +thm dictionary_second_step
   1.125 +
   1.126 +
   1.127 +text\<open>This is the set-based variant of the theorem compact_imp_closed.\<close>
   1.128 +lemma compact_imp_closed_set_based:
   1.129 +  assumes "(A::'a set) \<noteq> {}"
   1.130 +  shows "\<forall>open. t2_space_on_with A open \<longrightarrow> (\<forall>S\<subseteq>A. compact_on_with A open S \<longrightarrow>
   1.131 +    closed_on_with A open S)"
   1.132 +proof -
   1.133 +  {
   1.134 +    text\<open>We define the type 'b to be isomorphic to A.\<close>
   1.135 +    assume T: "\<exists>(Rep :: 'b \<Rightarrow> 'a) Abs. type_definition Rep Abs A"
   1.136 +    from T obtain rep :: "'b \<Rightarrow> 'a" and abs :: "'a \<Rightarrow> 'b" where t: "type_definition rep abs A"
   1.137 +      by auto
   1.138 +
   1.139 +    text\<open>Setup for the Transfer tool.\<close>
   1.140 +    define cr_b where "cr_b == \<lambda>r a. r = rep a"
   1.141 +    note type_definition_Domainp[OF t cr_b_def, transfer_domain_rule]
   1.142 +    note typedef_right_total[OF t cr_b_def, transfer_rule]
   1.143 +    note typedef_bi_unique[OF t cr_b_def, transfer_rule]
   1.144 +
   1.145 +    have ?thesis
   1.146 +      text\<open>Relativization by the Transfer tool.\<close>
   1.147 +      using dictionary_second_step[where 'a = 'b, untransferred, simplified]
   1.148 +      by blast
   1.149 +
   1.150 +  } note * = this[cancel_type_definition, OF assms]
   1.151 +
   1.152 +  show ?thesis by (rule *)
   1.153 +qed
   1.154 +
   1.155 +setup \<open>Sign.add_const_constraint
   1.156 +  (@{const_name "open"}, SOME @{typ "'a::topological_space set \<Rightarrow> bool"})\<close>
   1.157 +
   1.158 +text\<open>The Final Result. We can compare the type-based and the set-based statement.\<close>
   1.159 +thm compact_imp_closed compact_imp_closed_set_based
   1.160 +
   1.161 +declare [[show_sorts]]
   1.162 +text\<open>The Final Result. This time with explicitly shown type-class annotations.\<close>
   1.163 +thm compact_imp_closed compact_imp_closed_set_based
   1.164 +
   1.165 +end