src/HOL/Probability/Infinite_Product_Measure.thy

     from assms show "(J \<noteq> {} \<or> I = {}) \<and> finite J \<and> J \<subseteq> I \<and> X \<in> (\<Pi> j\<in>J. sets (M j))"
       by (simp add: Pi_iff)
   next
     fix J X assume J: "(J \<noteq> {} \<or> I = {}) \<and> finite J \<and> J \<subseteq> I \<and> X \<in> (\<Pi> j\<in>J. sets (M j))"
     then show "emb I J (Pi\<^isub>E J X) \<in> Pow (\<Pi>\<^isub>E i\<in>I. space (M i))"
-      by (auto simp: Pi_iff prod_emb_def dest: sets_into_space)
+      by (auto simp: Pi_iff prod_emb_def dest: sets.sets_into_space)
     have "emb I J (Pi\<^isub>E J X) \<in> generator"
       using J `I \<noteq> {}` by (intro generatorI') (auto simp: Pi_iff)
     then have "\<mu> (emb I J (Pi\<^isub>E J X)) = \<mu>G (emb I J (Pi\<^isub>E J X))"
       using \<mu> by simp
     also have "\<dots> = (\<Prod> j\<in>J. if j \<in> J then emeasure (M j) (X j) else emeasure (M j) (space (M j)))"

   using sets_Collect_single[of i I "{x\<in>space (M i). P x}" M]
   by (simp add: space_PiM PiE_iff cong: conj_cong)
 
 lemma (in finite_product_prob_space) finite_measure_PiM_emb:
   "(\<And>i. i \<in> I \<Longrightarrow> A i \<in> sets (M i)) \<Longrightarrow> measure (PiM I M) (Pi\<^isub>E I A) = (\<Prod>i\<in>I. measure (M i) (A i))"
-  using measure_PiM_emb[of I A] finite_index prod_emb_PiE_same_index[OF sets_into_space, of I A M]
+  using measure_PiM_emb[of I A] finite_index prod_emb_PiE_same_index[OF sets.sets_into_space, of I A M]
   by auto
 
 lemma (in product_prob_space) PiM_component:
   assumes "i \<in> I"
   shows "distr (PiM I M) (M i) (\<lambda>\<omega>. \<omega> i) = M i"

     by (auto simp: space_pair_measure space_PiM PiE_iff split: split_comb_seq)
   fix j :: nat and A assume A: "A \<in> sets M"
   then have *: "{\<omega> \<in> space ((\<Pi>\<^isub>M i\<in>UNIV. M) \<Otimes>\<^isub>M (\<Pi>\<^isub>M i\<in>UNIV. M)). prod_case (comb_seq i) \<omega> j \<in> A} =
     (if j < i then {\<omega> \<in> space (\<Pi>\<^isub>M i\<in>UNIV. M). \<omega> j \<in> A} \<times> space (\<Pi>\<^isub>M i\<in>UNIV. M)
               else space (\<Pi>\<^isub>M i\<in>UNIV. M) \<times> {\<omega> \<in> space (\<Pi>\<^isub>M i\<in>UNIV. M). \<omega> (j - i) \<in> A})"
-    by (auto simp: space_PiM space_pair_measure comb_seq_def dest: sets_into_space)
+    by (auto simp: space_PiM space_pair_measure comb_seq_def dest: sets.sets_into_space)
   show "{\<omega> \<in> space ((\<Pi>\<^isub>M i\<in>UNIV. M) \<Otimes>\<^isub>M (\<Pi>\<^isub>M i\<in>UNIV. M)). prod_case (comb_seq i) \<omega> j \<in> A} \<in> sets ((\<Pi>\<^isub>M i\<in>UNIV. M) \<Otimes>\<^isub>M (\<Pi>\<^isub>M i\<in>UNIV. M))"
     unfolding * by (auto simp: A intro!: sets_Collect_single)
 qed
 
 lemma measurable_comb_seq'[measurable (raw)]:

 lemma infprod_in_sets[intro]:
   fixes E :: "nat \<Rightarrow> 'a set" assumes E: "\<And>i. E i \<in> sets M"
   shows "Pi UNIV E \<in> sets S"
 proof -
   have "Pi UNIV E = (\<Inter>i. emb UNIV {..i} (\<Pi>\<^isub>E j\<in>{..i}. E j))"
-    using E E[THEN sets_into_space]
+    using E E[THEN sets.sets_into_space]
     by (auto simp: prod_emb_def Pi_iff extensional_def) blast
   with E show ?thesis by auto
 qed
 
 lemma measure_PiM_countable:

 proof -
   let ?E = "\<lambda>n. emb UNIV {..n} (Pi\<^isub>E {.. n} E)"
   have "\<And>n. (\<Prod>i\<le>n. measure M (E i)) = measure S (?E n)"
     using E by (simp add: measure_PiM_emb)
   moreover have "Pi UNIV E = (\<Inter>n. ?E n)"
-    using E E[THEN sets_into_space]
+    using E E[THEN sets.sets_into_space]
     by (auto simp: prod_emb_def extensional_def Pi_iff) blast
   moreover have "range ?E \<subseteq> sets S"
     using E by auto
   moreover have "decseq ?E"
     by (auto simp: prod_emb_def Pi_iff decseq_def)

   let "distr _ _ ?f" = "?D"
 
   fix J E assume J: "finite J" "J \<subseteq> ?I" "\<And>j. j \<in> J \<Longrightarrow> E j \<in> sets M"
   let ?X = "prod_emb ?I ?M J (\<Pi>\<^isub>E j\<in>J. E j)"
   have "\<And>j x. j \<in> J \<Longrightarrow> x \<in> E j \<Longrightarrow> x \<in> space M"
-    using J(3)[THEN sets_into_space] by (auto simp: space_PiM Pi_iff subset_eq)
+    using J(3)[THEN sets.sets_into_space] by (auto simp: space_PiM Pi_iff subset_eq)
   with J have "?f -` ?X \<inter> space (S \<Otimes>\<^isub>M S) =
     (prod_emb ?I ?M (J \<inter> {..<i}) (PIE j:J \<inter> {..<i}. E j)) \<times>
     (prod_emb ?I ?M ((op + i) -` J) (PIE j:(op + i) -` J. E (i + j)))" (is "_ = ?E \<times> ?F")
    by (auto simp: space_pair_measure space_PiM prod_emb_def all_conj_distrib PiE_iff
                split: split_comb_seq split_comb_seq_asm)

   let "distr _ _ ?f" = "?D"
 
   fix J E assume J: "finite J" "J \<subseteq> ?I" "\<And>j. j \<in> J \<Longrightarrow> E j \<in> sets M"
   let ?X = "prod_emb ?I ?M J (PIE j:J. E j)"
   have "\<And>j x. j \<in> J \<Longrightarrow> x \<in> E j \<Longrightarrow> x \<in> space M"
-    using J(3)[THEN sets_into_space] by (auto simp: space_PiM Pi_iff subset_eq)
+    using J(3)[THEN sets.sets_into_space] by (auto simp: space_PiM Pi_iff subset_eq)
   with J have "?f -` ?X \<inter> space (M \<Otimes>\<^isub>M S) = (if 0 \<in> J then E 0 else space M) \<times>
     (prod_emb ?I ?M (Suc -` J) (PIE j:Suc -` J. E (Suc j)))" (is "_ = ?E \<times> ?F")
    by (auto simp: space_pair_measure space_PiM PiE_iff prod_emb_def all_conj_distrib
       split: nat.split nat.split_asm)
   then have "emeasure ?D ?X = emeasure (M \<Otimes>\<^isub>M S) (?E \<times> ?F)"