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