src/HOL/Library/Set_Idioms.thy
 author haftmann Fri Mar 22 19:18:08 2019 +0000 (4 months ago) changeset 69946 494934c30f38 parent 69918 eddcc7c726f3 permissions -rw-r--r--
improved code equations taken over from AFP
```     1 (*  Title:      HOL/Library/Set_Idioms.thy
```
```     2     Author:     Lawrence Paulson (but borrowed from HOL Light)
```
```     3 *)
```
```     4
```
```     5 section \<open>Set Idioms\<close>
```
```     6
```
```     7 theory Set_Idioms
```
```     8 imports Countable_Set
```
```     9
```
```    10 begin
```
```    11
```
```    12
```
```    13 subsection\<open>Idioms for being a suitable union/intersection of something\<close>
```
```    14
```
```    15 definition union_of :: "('a set set \<Rightarrow> bool) \<Rightarrow> ('a set \<Rightarrow> bool) \<Rightarrow> 'a set \<Rightarrow> bool"
```
```    16   (infixr "union'_of" 60)
```
```    17   where "P union_of Q \<equiv> \<lambda>S. \<exists>\<U>. P \<U> \<and> \<U> \<subseteq> Collect Q \<and> \<Union>\<U> = S"
```
```    18
```
```    19 definition intersection_of :: "('a set set \<Rightarrow> bool) \<Rightarrow> ('a set \<Rightarrow> bool) \<Rightarrow> 'a set \<Rightarrow> bool"
```
```    20   (infixr "intersection'_of" 60)
```
```    21   where "P intersection_of Q \<equiv> \<lambda>S. \<exists>\<U>. P \<U> \<and> \<U> \<subseteq> Collect Q \<and> \<Inter>\<U> = S"
```
```    22
```
```    23 definition arbitrary:: "'a set set \<Rightarrow> bool" where "arbitrary \<U> \<equiv> True"
```
```    24
```
```    25 lemma union_of_inc: "\<lbrakk>P {S}; Q S\<rbrakk> \<Longrightarrow> (P union_of Q) S"
```
```    26   by (auto simp: union_of_def)
```
```    27
```
```    28 lemma intersection_of_inc:
```
```    29    "\<lbrakk>P {S}; Q S\<rbrakk> \<Longrightarrow> (P intersection_of Q) S"
```
```    30   by (auto simp: intersection_of_def)
```
```    31
```
```    32 lemma union_of_mono:
```
```    33    "\<lbrakk>(P union_of Q) S; \<And>x. Q x \<Longrightarrow> Q' x\<rbrakk> \<Longrightarrow> (P union_of Q') S"
```
```    34   by (auto simp: union_of_def)
```
```    35
```
```    36 lemma intersection_of_mono:
```
```    37    "\<lbrakk>(P intersection_of Q) S; \<And>x. Q x \<Longrightarrow> Q' x\<rbrakk> \<Longrightarrow> (P intersection_of Q') S"
```
```    38   by (auto simp: intersection_of_def)
```
```    39
```
```    40 lemma all_union_of:
```
```    41      "(\<forall>S. (P union_of Q) S \<longrightarrow> R S) \<longleftrightarrow> (\<forall>T. P T \<and> T \<subseteq> Collect Q \<longrightarrow> R(\<Union>T))"
```
```    42   by (auto simp: union_of_def)
```
```    43
```
```    44 lemma all_intersection_of:
```
```    45      "(\<forall>S. (P intersection_of Q) S \<longrightarrow> R S) \<longleftrightarrow> (\<forall>T. P T \<and> T \<subseteq> Collect Q \<longrightarrow> R(\<Inter>T))"
```
```    46   by (auto simp: intersection_of_def)
```
```    47
```
```    48 lemma intersection_ofE:
```
```    49      "\<lbrakk>(P intersection_of Q) S; \<And>T. \<lbrakk>P T; T \<subseteq> Collect Q\<rbrakk> \<Longrightarrow> R(\<Inter>T)\<rbrakk> \<Longrightarrow> R S"
```
```    50   by (auto simp: intersection_of_def)
```
```    51
```
```    52 lemma union_of_empty:
```
```    53      "P {} \<Longrightarrow> (P union_of Q) {}"
```
```    54   by (auto simp: union_of_def)
```
```    55
```
```    56 lemma intersection_of_empty:
```
```    57      "P {} \<Longrightarrow> (P intersection_of Q) UNIV"
```
```    58   by (auto simp: intersection_of_def)
```
```    59
```
```    60 text\<open> The arbitrary and finite cases\<close>
```
```    61
```
```    62 lemma arbitrary_union_of_alt:
```
```    63    "(arbitrary union_of Q) S \<longleftrightarrow> (\<forall>x \<in> S. \<exists>U. Q U \<and> x \<in> U \<and> U \<subseteq> S)"
```
```    64  (is "?lhs = ?rhs")
```
```    65 proof
```
```    66   assume ?lhs
```
```    67   then show ?rhs
```
```    68     by (force simp: union_of_def arbitrary_def)
```
```    69 next
```
```    70   assume ?rhs
```
```    71   then have "{U. Q U \<and> U \<subseteq> S} \<subseteq> Collect Q" "\<Union>{U. Q U \<and> U \<subseteq> S} = S"
```
```    72     by auto
```
```    73   then show ?lhs
```
```    74     unfolding union_of_def arbitrary_def by blast
```
```    75 qed
```
```    76
```
```    77 lemma arbitrary_union_of_empty [simp]: "(arbitrary union_of P) {}"
```
```    78   by (force simp: union_of_def arbitrary_def)
```
```    79
```
```    80 lemma arbitrary_intersection_of_empty [simp]:
```
```    81   "(arbitrary intersection_of P) UNIV"
```
```    82   by (force simp: intersection_of_def arbitrary_def)
```
```    83
```
```    84 lemma arbitrary_union_of_inc:
```
```    85   "P S \<Longrightarrow> (arbitrary union_of P) S"
```
```    86   by (force simp: union_of_inc arbitrary_def)
```
```    87
```
```    88 lemma arbitrary_intersection_of_inc:
```
```    89   "P S \<Longrightarrow> (arbitrary intersection_of P) S"
```
```    90   by (force simp: intersection_of_inc arbitrary_def)
```
```    91
```
```    92 lemma arbitrary_union_of_complement:
```
```    93    "(arbitrary union_of P) S \<longleftrightarrow> (arbitrary intersection_of (\<lambda>S. P(- S))) (- S)"  (is "?lhs = ?rhs")
```
```    94 proof
```
```    95   assume ?lhs
```
```    96   then obtain \<U> where "\<U> \<subseteq> Collect P" "S = \<Union>\<U>"
```
```    97     by (auto simp: union_of_def arbitrary_def)
```
```    98   then show ?rhs
```
```    99     unfolding intersection_of_def arbitrary_def
```
```   100     by (rule_tac x="uminus ` \<U>" in exI) auto
```
```   101 next
```
```   102   assume ?rhs
```
```   103   then obtain \<U> where "\<U> \<subseteq> {S. P (- S)}" "\<Inter>\<U> = - S"
```
```   104     by (auto simp: union_of_def intersection_of_def arbitrary_def)
```
```   105   then show ?lhs
```
```   106     unfolding union_of_def arbitrary_def
```
```   107     by (rule_tac x="uminus ` \<U>" in exI) auto
```
```   108 qed
```
```   109
```
```   110 lemma arbitrary_intersection_of_complement:
```
```   111    "(arbitrary intersection_of P) S \<longleftrightarrow> (arbitrary union_of (\<lambda>S. P(- S))) (- S)"
```
```   112   by (simp add: arbitrary_union_of_complement)
```
```   113
```
```   114 lemma arbitrary_union_of_idempot [simp]:
```
```   115   "arbitrary union_of arbitrary union_of P = arbitrary union_of P"
```
```   116 proof -
```
```   117   have 1: "\<exists>\<U>'\<subseteq>Collect P. \<Union>\<U>' = \<Union>\<U>" if "\<U> \<subseteq> {S. \<exists>\<V>\<subseteq>Collect P. \<Union>\<V> = S}" for \<U>
```
```   118   proof -
```
```   119     let ?\<W> = "{V. \<exists>\<V>. \<V>\<subseteq>Collect P \<and> V \<in> \<V> \<and> (\<exists>S \<in> \<U>. \<Union>\<V> = S)}"
```
```   120     have *: "\<And>x U. \<lbrakk>x \<in> U; U \<in> \<U>\<rbrakk> \<Longrightarrow> x \<in> \<Union>?\<W>"
```
```   121       using that
```
```   122       apply simp
```
```   123       apply (drule subsetD, assumption, auto)
```
```   124       done
```
```   125     show ?thesis
```
```   126     apply (rule_tac x="{V. \<exists>\<V>. \<V>\<subseteq>Collect P \<and> V \<in> \<V> \<and> (\<exists>S \<in> \<U>. \<Union>\<V> = S)}" in exI)
```
```   127       using that by (blast intro: *)
```
```   128   qed
```
```   129   have 2: "\<exists>\<U>'\<subseteq>{S. \<exists>\<U>\<subseteq>Collect P. \<Union>\<U> = S}. \<Union>\<U>' = \<Union>\<U>" if "\<U> \<subseteq> Collect P" for \<U>
```
```   130     by (metis (mono_tags, lifting) union_of_def arbitrary_union_of_inc that)
```
```   131   show ?thesis
```
```   132     unfolding union_of_def arbitrary_def by (force simp: 1 2)
```
```   133 qed
```
```   134
```
```   135 lemma arbitrary_intersection_of_idempot:
```
```   136    "arbitrary intersection_of arbitrary intersection_of P = arbitrary intersection_of P" (is "?lhs = ?rhs")
```
```   137 proof -
```
```   138   have "- ?lhs = - ?rhs"
```
```   139     unfolding arbitrary_intersection_of_complement by simp
```
```   140   then show ?thesis
```
```   141     by simp
```
```   142 qed
```
```   143
```
```   144 lemma arbitrary_union_of_Union:
```
```   145    "(\<And>S. S \<in> \<U> \<Longrightarrow> (arbitrary union_of P) S) \<Longrightarrow> (arbitrary union_of P) (\<Union>\<U>)"
```
```   146   by (metis union_of_def arbitrary_def arbitrary_union_of_idempot mem_Collect_eq subsetI)
```
```   147
```
```   148 lemma arbitrary_union_of_Un:
```
```   149    "\<lbrakk>(arbitrary union_of P) S; (arbitrary union_of P) T\<rbrakk>
```
```   150            \<Longrightarrow> (arbitrary union_of P) (S \<union> T)"
```
```   151   using arbitrary_union_of_Union [of "{S,T}"] by auto
```
```   152
```
```   153 lemma arbitrary_intersection_of_Inter:
```
```   154    "(\<And>S. S \<in> \<U> \<Longrightarrow> (arbitrary intersection_of P) S) \<Longrightarrow> (arbitrary intersection_of P) (\<Inter>\<U>)"
```
```   155   by (metis intersection_of_def arbitrary_def arbitrary_intersection_of_idempot mem_Collect_eq subsetI)
```
```   156
```
```   157 lemma arbitrary_intersection_of_Int:
```
```   158    "\<lbrakk>(arbitrary intersection_of P) S; (arbitrary intersection_of P) T\<rbrakk>
```
```   159            \<Longrightarrow> (arbitrary intersection_of P) (S \<inter> T)"
```
```   160   using arbitrary_intersection_of_Inter [of "{S,T}"] by auto
```
```   161
```
```   162 lemma arbitrary_union_of_Int_eq:
```
```   163   "(\<forall>S T. (arbitrary union_of P) S \<and> (arbitrary union_of P) T
```
```   164                \<longrightarrow> (arbitrary union_of P) (S \<inter> T))
```
```   165    \<longleftrightarrow> (\<forall>S T. P S \<and> P T \<longrightarrow> (arbitrary union_of P) (S \<inter> T))"  (is "?lhs = ?rhs")
```
```   166 proof
```
```   167   assume ?lhs
```
```   168   then show ?rhs
```
```   169     by (simp add: arbitrary_union_of_inc)
```
```   170 next
```
```   171   assume R: ?rhs
```
```   172   show ?lhs
```
```   173   proof clarify
```
```   174     fix S :: "'a set" and T :: "'a set"
```
```   175     assume "(arbitrary union_of P) S" and "(arbitrary union_of P) T"
```
```   176     then obtain \<U> \<V> where *: "\<U> \<subseteq> Collect P" "\<Union>\<U> = S" "\<V> \<subseteq> Collect P" "\<Union>\<V> = T"
```
```   177       by (auto simp: union_of_def)
```
```   178     then have "(arbitrary union_of P) (\<Union>C\<in>\<U>. \<Union>D\<in>\<V>. C \<inter> D)"
```
```   179      using R by (blast intro: arbitrary_union_of_Union)
```
```   180    then show "(arbitrary union_of P) (S \<inter> T)"
```
```   181      by (simp add: Int_UN_distrib2 *)
```
```   182  qed
```
```   183 qed
```
```   184
```
```   185 lemma arbitrary_intersection_of_Un_eq:
```
```   186    "(\<forall>S T. (arbitrary intersection_of P) S \<and> (arbitrary intersection_of P) T
```
```   187                \<longrightarrow> (arbitrary intersection_of P) (S \<union> T)) \<longleftrightarrow>
```
```   188         (\<forall>S T. P S \<and> P T \<longrightarrow> (arbitrary intersection_of P) (S \<union> T))"
```
```   189   apply (simp add: arbitrary_intersection_of_complement)
```
```   190   using arbitrary_union_of_Int_eq [of "\<lambda>S. P (- S)"]
```
```   191   by (metis (no_types, lifting) arbitrary_def double_compl union_of_inc)
```
```   192
```
```   193 lemma finite_union_of_empty [simp]: "(finite union_of P) {}"
```
```   194   by (simp add: union_of_empty)
```
```   195
```
```   196 lemma finite_intersection_of_empty [simp]: "(finite intersection_of P) UNIV"
```
```   197   by (simp add: intersection_of_empty)
```
```   198
```
```   199 lemma finite_union_of_inc:
```
```   200    "P S \<Longrightarrow> (finite union_of P) S"
```
```   201   by (simp add: union_of_inc)
```
```   202
```
```   203 lemma finite_intersection_of_inc:
```
```   204    "P S \<Longrightarrow> (finite intersection_of P) S"
```
```   205   by (simp add: intersection_of_inc)
```
```   206
```
```   207 lemma finite_union_of_complement:
```
```   208   "(finite union_of P) S \<longleftrightarrow> (finite intersection_of (\<lambda>S. P(- S))) (- S)"
```
```   209   unfolding union_of_def intersection_of_def
```
```   210   apply safe
```
```   211    apply (rule_tac x="uminus ` \<U>" in exI, fastforce)+
```
```   212   done
```
```   213
```
```   214 lemma finite_intersection_of_complement:
```
```   215    "(finite intersection_of P) S \<longleftrightarrow> (finite union_of (\<lambda>S. P(- S))) (- S)"
```
```   216   by (simp add: finite_union_of_complement)
```
```   217
```
```   218 lemma finite_union_of_idempot [simp]:
```
```   219   "finite union_of finite union_of P = finite union_of P"
```
```   220 proof -
```
```   221   have "(finite union_of P) S" if S: "(finite union_of finite union_of P) S" for S
```
```   222   proof -
```
```   223     obtain \<U> where "finite \<U>" "S = \<Union>\<U>" and \<U>: "\<forall>U\<in>\<U>. \<exists>\<U>. finite \<U> \<and> (\<U> \<subseteq> Collect P) \<and> \<Union>\<U> = U"
```
```   224       using S unfolding union_of_def by (auto simp: subset_eq)
```
```   225     then obtain f where "\<forall>U\<in>\<U>. finite (f U) \<and> (f U \<subseteq> Collect P) \<and> \<Union>(f U) = U"
```
```   226       by metis
```
```   227     then show ?thesis
```
```   228       unfolding union_of_def \<open>S = \<Union>\<U>\<close>
```
```   229       by (rule_tac x = "snd ` Sigma \<U> f" in exI) (fastforce simp: \<open>finite \<U>\<close>)
```
```   230   qed
```
```   231   moreover
```
```   232   have "(finite union_of finite union_of P) S" if "(finite union_of P) S" for S
```
```   233     by (simp add: finite_union_of_inc that)
```
```   234   ultimately show ?thesis
```
```   235     by force
```
```   236 qed
```
```   237
```
```   238 lemma finite_intersection_of_idempot [simp]:
```
```   239    "finite intersection_of finite intersection_of P = finite intersection_of P"
```
```   240   by (force simp: finite_intersection_of_complement)
```
```   241
```
```   242 lemma finite_union_of_Union:
```
```   243    "\<lbrakk>finite \<U>; \<And>S. S \<in> \<U> \<Longrightarrow> (finite union_of P) S\<rbrakk> \<Longrightarrow> (finite union_of P) (\<Union>\<U>)"
```
```   244   using finite_union_of_idempot [of P]
```
```   245   by (metis mem_Collect_eq subsetI union_of_def)
```
```   246
```
```   247 lemma finite_union_of_Un:
```
```   248    "\<lbrakk>(finite union_of P) S; (finite union_of P) T\<rbrakk> \<Longrightarrow> (finite union_of P) (S \<union> T)"
```
```   249   by (auto simp: union_of_def)
```
```   250
```
```   251 lemma finite_intersection_of_Inter:
```
```   252    "\<lbrakk>finite \<U>; \<And>S. S \<in> \<U> \<Longrightarrow> (finite intersection_of P) S\<rbrakk> \<Longrightarrow> (finite intersection_of P) (\<Inter>\<U>)"
```
```   253   using finite_intersection_of_idempot [of P]
```
```   254   by (metis intersection_of_def mem_Collect_eq subsetI)
```
```   255
```
```   256 lemma finite_intersection_of_Int:
```
```   257    "\<lbrakk>(finite intersection_of P) S; (finite intersection_of P) T\<rbrakk>
```
```   258            \<Longrightarrow> (finite intersection_of P) (S \<inter> T)"
```
```   259   by (auto simp: intersection_of_def)
```
```   260
```
```   261 lemma finite_union_of_Int_eq:
```
```   262    "(\<forall>S T. (finite union_of P) S \<and> (finite union_of P) T \<longrightarrow> (finite union_of P) (S \<inter> T))
```
```   263     \<longleftrightarrow> (\<forall>S T. P S \<and> P T \<longrightarrow> (finite union_of P) (S \<inter> T))"
```
```   264 (is "?lhs = ?rhs")
```
```   265 proof
```
```   266   assume ?lhs
```
```   267   then show ?rhs
```
```   268     by (simp add: finite_union_of_inc)
```
```   269 next
```
```   270   assume R: ?rhs
```
```   271   show ?lhs
```
```   272   proof clarify
```
```   273     fix S :: "'a set" and T :: "'a set"
```
```   274     assume "(finite union_of P) S" and "(finite union_of P) T"
```
```   275     then obtain \<U> \<V> where *: "\<U> \<subseteq> Collect P" "\<Union>\<U> = S" "finite \<U>" "\<V> \<subseteq> Collect P" "\<Union>\<V> = T" "finite \<V>"
```
```   276       by (auto simp: union_of_def)
```
```   277     then have "(finite union_of P) (\<Union>C\<in>\<U>. \<Union>D\<in>\<V>. C \<inter> D)"
```
```   278       using R
```
```   279       by (blast intro: finite_union_of_Union)
```
```   280    then show "(finite union_of P) (S \<inter> T)"
```
```   281      by (simp add: Int_UN_distrib2 *)
```
```   282  qed
```
```   283 qed
```
```   284
```
```   285 lemma finite_intersection_of_Un_eq:
```
```   286    "(\<forall>S T. (finite intersection_of P) S \<and>
```
```   287                (finite intersection_of P) T
```
```   288                \<longrightarrow> (finite intersection_of P) (S \<union> T)) \<longleftrightarrow>
```
```   289         (\<forall>S T. P S \<and> P T \<longrightarrow> (finite intersection_of P) (S \<union> T))"
```
```   290   apply (simp add: finite_intersection_of_complement)
```
```   291   using finite_union_of_Int_eq [of "\<lambda>S. P (- S)"]
```
```   292   by (metis (no_types, lifting) double_compl)
```
```   293
```
```   294
```
```   295 abbreviation finite' :: "'a set \<Rightarrow> bool"
```
```   296   where "finite' A \<equiv> finite A \<and> A \<noteq> {}"
```
```   297
```
```   298 lemma finite'_intersection_of_Int:
```
```   299    "\<lbrakk>(finite' intersection_of P) S; (finite' intersection_of P) T\<rbrakk>
```
```   300            \<Longrightarrow> (finite' intersection_of P) (S \<inter> T)"
```
```   301   by (auto simp: intersection_of_def)
```
```   302
```
```   303 lemma finite'_intersection_of_inc:
```
```   304    "P S \<Longrightarrow> (finite' intersection_of P) S"
```
```   305   by (simp add: intersection_of_inc)
```
```   306
```
```   307
```
```   308 subsection \<open>The ``Relative to'' operator\<close>
```
```   309
```
```   310 text\<open>A somewhat cheap but handy way of getting localized forms of various topological concepts
```
```   311 (open, closed, borel, fsigma, gdelta etc.)\<close>
```
```   312
```
```   313 definition relative_to :: "['a set \<Rightarrow> bool, 'a set, 'a set] \<Rightarrow> bool" (infixl "relative'_to" 55)
```
```   314   where "P relative_to S \<equiv> \<lambda>T. \<exists>U. P U \<and> S \<inter> U = T"
```
```   315
```
```   316 lemma relative_to_UNIV [simp]: "(P relative_to UNIV) S \<longleftrightarrow> P S"
```
```   317   by (simp add: relative_to_def)
```
```   318
```
```   319 lemma relative_to_imp_subset:
```
```   320    "(P relative_to S) T \<Longrightarrow> T \<subseteq> S"
```
```   321   by (auto simp: relative_to_def)
```
```   322
```
```   323 lemma all_relative_to: "(\<forall>S. (P relative_to U) S \<longrightarrow> Q S) \<longleftrightarrow> (\<forall>S. P S \<longrightarrow> Q(U \<inter> S))"
```
```   324   by (auto simp: relative_to_def)
```
```   325
```
```   326 lemma relative_toE: "\<lbrakk>(P relative_to U) S; \<And>S. P S \<Longrightarrow> Q(U \<inter> S)\<rbrakk> \<Longrightarrow> Q S"
```
```   327   by (auto simp: relative_to_def)
```
```   328
```
```   329 lemma relative_to_inc:
```
```   330    "P S \<Longrightarrow> (P relative_to U) (U \<inter> S)"
```
```   331   by (auto simp: relative_to_def)
```
```   332
```
```   333 lemma relative_to_relative_to [simp]:
```
```   334    "P relative_to S relative_to T = P relative_to (S \<inter> T)"
```
```   335   unfolding relative_to_def
```
```   336   by auto
```
```   337
```
```   338 lemma relative_to_compl:
```
```   339    "S \<subseteq> U \<Longrightarrow> ((P relative_to U) (U - S) \<longleftrightarrow> ((\<lambda>c. P(- c)) relative_to U) S)"
```
```   340   unfolding relative_to_def
```
```   341   by (metis Diff_Diff_Int Diff_eq double_compl inf.absorb_iff2)
```
```   342
```
```   343 lemma relative_to_subset:
```
```   344    "S \<subseteq> T \<and> P S \<Longrightarrow> (P relative_to T) S"
```
```   345   unfolding relative_to_def by auto
```
```   346
```
```   347 lemma relative_to_subset_trans:
```
```   348    "(P relative_to U) S \<and> S \<subseteq> T \<and> T \<subseteq> U \<Longrightarrow> (P relative_to T) S"
```
```   349   unfolding relative_to_def by auto
```
```   350
```
```   351 lemma relative_to_mono:
```
```   352    "\<lbrakk>(P relative_to U) S; \<And>S. P S \<Longrightarrow> Q S\<rbrakk> \<Longrightarrow> (Q relative_to U) S"
```
```   353   unfolding relative_to_def by auto
```
```   354
```
```   355 lemma relative_to_subset_inc: "\<lbrakk>S \<subseteq> U; P S\<rbrakk> \<Longrightarrow> (P relative_to U) S"
```
```   356   unfolding relative_to_def by auto
```
```   357
```
```   358 lemma relative_to_Int:
```
```   359    "\<lbrakk>(P relative_to S) C; (P relative_to S) D; \<And>X Y. \<lbrakk>P X; P Y\<rbrakk> \<Longrightarrow> P(X \<inter> Y)\<rbrakk>
```
```   360          \<Longrightarrow>  (P relative_to S) (C \<inter> D)"
```
```   361   unfolding relative_to_def by auto
```
```   362
```
```   363 lemma relative_to_Un:
```
```   364    "\<lbrakk>(P relative_to S) C; (P relative_to S) D; \<And>X Y. \<lbrakk>P X; P Y\<rbrakk> \<Longrightarrow> P(X \<union> Y)\<rbrakk>
```
```   365          \<Longrightarrow>  (P relative_to S) (C \<union> D)"
```
```   366   unfolding relative_to_def by auto
```
```   367
```
```   368 lemma arbitrary_union_of_relative_to:
```
```   369   "((arbitrary union_of P) relative_to U) = (arbitrary union_of (P relative_to U))" (is "?lhs = ?rhs")
```
```   370 proof -
```
```   371   have "?rhs S" if L: "?lhs S" for S
```
```   372   proof -
```
```   373     obtain \<U> where "S = U \<inter> \<Union>\<U>" "\<U> \<subseteq> Collect P"
```
```   374       using L unfolding relative_to_def union_of_def by auto
```
```   375     then show ?thesis
```
```   376       unfolding relative_to_def union_of_def arbitrary_def
```
```   377       by (rule_tac x="(\<lambda>X. U \<inter> X) ` \<U>" in exI) auto
```
```   378   qed
```
```   379   moreover have "?lhs S" if R: "?rhs S" for S
```
```   380   proof -
```
```   381     obtain \<U> where "S = \<Union>\<U>" "\<forall>T\<in>\<U>. \<exists>V. P V \<and> U \<inter> V = T"
```
```   382       using R unfolding relative_to_def union_of_def by auto
```
```   383     then obtain f where f: "\<And>T. T \<in> \<U> \<Longrightarrow> P (f T)" "\<And>T. T \<in> \<U> \<Longrightarrow> U \<inter> (f T) = T"
```
```   384       by metis
```
```   385     then have "\<exists>\<U>'\<subseteq>Collect P. \<Union>\<U>' = \<Union> (f ` \<U>)"
```
```   386       by (metis image_subset_iff mem_Collect_eq)
```
```   387     moreover have eq: "U \<inter> \<Union> (f ` \<U>) = \<Union>\<U>"
```
```   388       using f by auto
```
```   389     ultimately show ?thesis
```
```   390       unfolding relative_to_def union_of_def arbitrary_def \<open>S = \<Union>\<U>\<close>
```
```   391       by metis
```
```   392   qed
```
```   393   ultimately show ?thesis
```
```   394     by blast
```
```   395 qed
```
```   396
```
```   397 lemma finite_union_of_relative_to:
```
```   398   "((finite union_of P) relative_to U) = (finite union_of (P relative_to U))" (is "?lhs = ?rhs")
```
```   399 proof -
```
```   400   have "?rhs S" if L: "?lhs S" for S
```
```   401   proof -
```
```   402     obtain \<U> where "S = U \<inter> \<Union>\<U>" "\<U> \<subseteq> Collect P" "finite \<U>"
```
```   403       using L unfolding relative_to_def union_of_def by auto
```
```   404     then show ?thesis
```
```   405       unfolding relative_to_def union_of_def
```
```   406       by (rule_tac x="(\<lambda>X. U \<inter> X) ` \<U>" in exI) auto
```
```   407   qed
```
```   408   moreover have "?lhs S" if R: "?rhs S" for S
```
```   409   proof -
```
```   410     obtain \<U> where "S = \<Union>\<U>" "\<forall>T\<in>\<U>. \<exists>V. P V \<and> U \<inter> V = T" "finite \<U>"
```
```   411       using R unfolding relative_to_def union_of_def by auto
```
```   412     then obtain f where f: "\<And>T. T \<in> \<U> \<Longrightarrow> P (f T)" "\<And>T. T \<in> \<U> \<Longrightarrow> U \<inter> (f T) = T"
```
```   413       by metis
```
```   414     then have "\<exists>\<U>'\<subseteq>Collect P. \<Union>\<U>' = \<Union> (f ` \<U>)"
```
```   415       by (metis image_subset_iff mem_Collect_eq)
```
```   416     moreover have eq: "U \<inter> \<Union> (f ` \<U>) = \<Union>\<U>"
```
```   417       using f by auto
```
```   418     ultimately show ?thesis
```
```   419       using \<open>finite \<U>\<close> f
```
```   420       unfolding relative_to_def union_of_def \<open>S = \<Union>\<U>\<close>
```
```   421       by (rule_tac x="\<Union> (f ` \<U>)" in exI) (metis finite_imageI image_subsetI mem_Collect_eq)
```
```   422   qed
```
```   423   ultimately show ?thesis
```
```   424     by blast
```
```   425 qed
```
```   426
```
```   427 lemma countable_union_of_relative_to:
```
```   428   "((countable union_of P) relative_to U) = (countable union_of (P relative_to U))" (is "?lhs = ?rhs")
```
```   429 proof -
```
```   430   have "?rhs S" if L: "?lhs S" for S
```
```   431   proof -
```
```   432     obtain \<U> where "S = U \<inter> \<Union>\<U>" "\<U> \<subseteq> Collect P" "countable \<U>"
```
```   433       using L unfolding relative_to_def union_of_def by auto
```
```   434     then show ?thesis
```
```   435       unfolding relative_to_def union_of_def
```
```   436       by (rule_tac x="(\<lambda>X. U \<inter> X) ` \<U>" in exI) auto
```
```   437   qed
```
```   438   moreover have "?lhs S" if R: "?rhs S" for S
```
```   439   proof -
```
```   440     obtain \<U> where "S = \<Union>\<U>" "\<forall>T\<in>\<U>. \<exists>V. P V \<and> U \<inter> V = T" "countable \<U>"
```
```   441       using R unfolding relative_to_def union_of_def by auto
```
```   442     then obtain f where f: "\<And>T. T \<in> \<U> \<Longrightarrow> P (f T)" "\<And>T. T \<in> \<U> \<Longrightarrow> U \<inter> (f T) = T"
```
```   443       by metis
```
```   444     then have "\<exists>\<U>'\<subseteq>Collect P. \<Union>\<U>' = \<Union> (f ` \<U>)"
```
```   445       by (metis image_subset_iff mem_Collect_eq)
```
```   446     moreover have eq: "U \<inter> \<Union> (f ` \<U>) = \<Union>\<U>"
```
```   447       using f by auto
```
```   448     ultimately show ?thesis
```
```   449       using \<open>countable \<U>\<close> f
```
```   450       unfolding relative_to_def union_of_def \<open>S = \<Union>\<U>\<close>
```
```   451       by (rule_tac x="\<Union> (f ` \<U>)" in exI) (metis countable_image image_subsetI mem_Collect_eq)
```
```   452   qed
```
```   453   ultimately show ?thesis
```
```   454     by blast
```
```   455 qed
```
```   456
```
```   457
```
```   458 lemma arbitrary_intersection_of_relative_to:
```
```   459   "((arbitrary intersection_of P) relative_to U) = ((arbitrary intersection_of (P relative_to U)) relative_to U)" (is "?lhs = ?rhs")
```
```   460 proof -
```
```   461   have "?rhs S" if L: "?lhs S" for S
```
```   462   proof -
```
```   463     obtain \<U> where \<U>: "S = U \<inter> \<Inter>\<U>" "\<U> \<subseteq> Collect P"
```
```   464       using L unfolding relative_to_def intersection_of_def by auto
```
```   465     show ?thesis
```
```   466       unfolding relative_to_def intersection_of_def arbitrary_def
```
```   467     proof (intro exI conjI)
```
```   468       show "U \<inter> (\<Inter>X\<in>\<U>. U \<inter> X) = S" "(\<inter>) U ` \<U> \<subseteq> {T. \<exists>Ua. P Ua \<and> U \<inter> Ua = T}"
```
```   469         using \<U> by blast+
```
```   470     qed auto
```
```   471   qed
```
```   472   moreover have "?lhs S" if R: "?rhs S" for S
```
```   473   proof -
```
```   474     obtain \<U> where "S = U \<inter> \<Inter>\<U>" "\<forall>T\<in>\<U>. \<exists>V. P V \<and> U \<inter> V = T"
```
```   475       using R unfolding relative_to_def intersection_of_def  by auto
```
```   476     then obtain f where f: "\<And>T. T \<in> \<U> \<Longrightarrow> P (f T)" "\<And>T. T \<in> \<U> \<Longrightarrow> U \<inter> (f T) = T"
```
```   477       by metis
```
```   478     then have "f `  \<U> \<subseteq> Collect P"
```
```   479       by auto
```
```   480     moreover have eq: "U \<inter> \<Inter>(f ` \<U>) = U \<inter> \<Inter>\<U>"
```
```   481       using f by auto
```
```   482     ultimately show ?thesis
```
```   483       unfolding relative_to_def intersection_of_def arbitrary_def \<open>S = U \<inter> \<Inter>\<U>\<close>
```
```   484       by auto
```
```   485   qed
```
```   486   ultimately show ?thesis
```
```   487     by blast
```
```   488 qed
```
```   489
```
```   490 lemma finite_intersection_of_relative_to:
```
```   491   "((finite intersection_of P) relative_to U) = ((finite intersection_of (P relative_to U)) relative_to U)" (is "?lhs = ?rhs")
```
```   492 proof -
```
```   493   have "?rhs S" if L: "?lhs S" for S
```
```   494   proof -
```
```   495     obtain \<U> where \<U>: "S = U \<inter> \<Inter>\<U>" "\<U> \<subseteq> Collect P" "finite \<U>"
```
```   496       using L unfolding relative_to_def intersection_of_def by auto
```
```   497     show ?thesis
```
```   498       unfolding relative_to_def intersection_of_def
```
```   499     proof (intro exI conjI)
```
```   500       show "U \<inter> (\<Inter>X\<in>\<U>. U \<inter> X) = S" "(\<inter>) U ` \<U> \<subseteq> {T. \<exists>Ua. P Ua \<and> U \<inter> Ua = T}"
```
```   501         using \<U> by blast+
```
```   502       show "finite ((\<inter>) U ` \<U>)"
```
```   503         by (simp add: \<open>finite \<U>\<close>)
```
```   504     qed auto
```
```   505   qed
```
```   506   moreover have "?lhs S" if R: "?rhs S" for S
```
```   507   proof -
```
```   508     obtain \<U> where "S = U \<inter> \<Inter>\<U>" "\<forall>T\<in>\<U>. \<exists>V. P V \<and> U \<inter> V = T" "finite \<U>"
```
```   509       using R unfolding relative_to_def intersection_of_def  by auto
```
```   510     then obtain f where f: "\<And>T. T \<in> \<U> \<Longrightarrow> P (f T)" "\<And>T. T \<in> \<U> \<Longrightarrow> U \<inter> (f T) = T"
```
```   511       by metis
```
```   512     then have "f `  \<U> \<subseteq> Collect P"
```
```   513       by auto
```
```   514     moreover have eq: "U \<inter> \<Inter> (f ` \<U>) = U \<inter> \<Inter> \<U>"
```
```   515       using f by auto
```
```   516     ultimately show ?thesis
```
```   517       unfolding relative_to_def intersection_of_def \<open>S = U \<inter> \<Inter>\<U>\<close>
```
```   518       using \<open>finite \<U>\<close>
```
```   519       by auto
```
```   520   qed
```
```   521   ultimately show ?thesis
```
```   522     by blast
```
```   523 qed
```
```   524
```
```   525 lemma countable_intersection_of_relative_to:
```
```   526   "((countable intersection_of P) relative_to U) = ((countable intersection_of (P relative_to U)) relative_to U)" (is "?lhs = ?rhs")
```
```   527 proof -
```
```   528   have "?rhs S" if L: "?lhs S" for S
```
```   529   proof -
```
```   530     obtain \<U> where \<U>: "S = U \<inter> \<Inter>\<U>" "\<U> \<subseteq> Collect P" "countable \<U>"
```
```   531       using L unfolding relative_to_def intersection_of_def by auto
```
```   532     show ?thesis
```
```   533       unfolding relative_to_def intersection_of_def
```
```   534     proof (intro exI conjI)
```
```   535       show "U \<inter> (\<Inter>X\<in>\<U>. U \<inter> X) = S" "(\<inter>) U ` \<U> \<subseteq> {T. \<exists>Ua. P Ua \<and> U \<inter> Ua = T}"
```
```   536         using \<U> by blast+
```
```   537       show "countable ((\<inter>) U ` \<U>)"
```
```   538         by (simp add: \<open>countable \<U>\<close>)
```
```   539     qed auto
```
```   540   qed
```
```   541   moreover have "?lhs S" if R: "?rhs S" for S
```
```   542   proof -
```
```   543     obtain \<U> where "S = U \<inter> \<Inter>\<U>" "\<forall>T\<in>\<U>. \<exists>V. P V \<and> U \<inter> V = T" "countable \<U>"
```
```   544       using R unfolding relative_to_def intersection_of_def  by auto
```
```   545     then obtain f where f: "\<And>T. T \<in> \<U> \<Longrightarrow> P (f T)" "\<And>T. T \<in> \<U> \<Longrightarrow> U \<inter> (f T) = T"
```
```   546       by metis
```
```   547     then have "f `  \<U> \<subseteq> Collect P"
```
```   548       by auto
```
```   549     moreover have eq: "U \<inter> \<Inter> (f ` \<U>) = U \<inter> \<Inter> \<U>"
```
```   550       using f by auto
```
```   551     ultimately show ?thesis
```
```   552       unfolding relative_to_def intersection_of_def \<open>S = U \<inter> \<Inter>\<U>\<close>
```
```   553       using \<open>countable \<U>\<close> countable_image
```
```   554       by auto
```
```   555   qed
```
```   556   ultimately show ?thesis
```
```   557     by blast
```
```   558 qed
```
```   559
```
```   560 end
```