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