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