1.1 --- a/src/HOL/Probability/Projective_Family.thy	Thu Nov 22 10:09:54 2012 +0100
     1.2 +++ b/src/HOL/Probability/Projective_Family.thy	Tue Nov 27 11:29:47 2012 +0100
     1.3 @@ -25,7 +25,7 @@
     1.4    show "range ?F \<subseteq> ?J" "(\<Union>i. ?F i) = ?\<Omega>"
     1.5      using `finite J` by (auto intro!: prod_algebraI_finite)
     1.6    { fix i show "emeasure ?P (?F i) \<noteq> \<infinity>" by simp }
     1.7 -  show "?J \<subseteq> Pow ?\<Omega>" by (auto simp: Pi_iff dest: sets_into_space)
     1.8 +  show "?J \<subseteq> Pow ?\<Omega>" by (auto simp: Pi_iff dest: sets.sets_into_space)
     1.9    show "sets (\<Pi>\<^isub>M i\<in>J. M i) = sigma_sets ?\<Omega> ?J" "sets ?D = sigma_sets ?\<Omega> ?J"
    1.10      using `finite J` by (simp_all add: sets_PiM prod_algebra_eq_finite Pi_iff)
    1.11  
    1.12 @@ -44,7 +44,7 @@
    1.13    also have "\<dots> = emeasure (Pi\<^isub>M K M) (\<Pi>\<^isub>E i\<in>K. if i \<in> J then E i else space (M i))"
    1.14      using E by (simp add: K.measure_times)
    1.15    also have "(\<Pi>\<^isub>E i\<in>K. if i \<in> J then E i else space (M i)) = (\<lambda>f. restrict f J) -` Pi\<^isub>E J E \<inter> (\<Pi>\<^isub>E i\<in>K. space (M i))"
    1.16 -    using `J \<subseteq> K` sets_into_space E by (force simp: Pi_iff PiE_def split: split_if_asm)
    1.17 +    using `J \<subseteq> K` sets.sets_into_space E by (force simp: Pi_iff PiE_def split: split_if_asm)
    1.18    finally show "emeasure (Pi\<^isub>M J M) X = emeasure ?D X"
    1.19      using X `J \<subseteq> K` apply (subst emeasure_distr)
    1.20      by (auto intro!: measurable_restrict_subset simp: space_PiM)
    1.21 @@ -93,10 +93,10 @@
    1.22    shows "emeasure (limP J M P) (Pi\<^isub>E J A) = emeasure (P J) (Pi\<^isub>E J A)"
    1.23  proof -
    1.24    have "Pi\<^isub>E J (restrict A J) \<subseteq> (\<Pi>\<^isub>E i\<in>J. space (M i))"
    1.25 -    using sets_into_space[OF A] by (auto simp: PiE_iff) blast
    1.26 +    using sets.sets_into_space[OF A] by (auto simp: PiE_iff) blast
    1.27    hence "emeasure (limP J M P) (Pi\<^isub>E J A) =
    1.28      emeasure (limP J M P) (prod_emb J M J (Pi\<^isub>E J A))"
    1.29 -    using assms(1-3) sets_into_space by (auto simp add: prod_emb_id PiE_def Pi_def)
    1.30 +    using assms(1-3) sets.sets_into_space by (auto simp add: prod_emb_id PiE_def Pi_def)
    1.31    also have "\<dots> = emeasure (P J) (Pi\<^isub>E J A)"
    1.32    proof (rule emeasure_extend_measure_Pair[OF limP_def])
    1.33      show "positive (sets (limP J M P)) (P J)" unfolding positive_def by auto
    1.34 @@ -133,12 +133,12 @@
    1.35    then obtain E where X: "X = Pi\<^isub>E J E" and E: "\<forall>i\<in>J. E i \<in> sets (M i)" by auto
    1.36    with `finite J` have "X \<in> sets (limP J M P)" by simp
    1.37    have emb_self: "prod_emb J M J (Pi\<^isub>E J E) = Pi\<^isub>E J E"
    1.38 -    using E sets_into_space
    1.39 +    using E sets.sets_into_space
    1.40      by (auto intro!: prod_emb_PiE_same_index)
    1.41    show "emeasure (limP J M P) X = emeasure (P J) X"
    1.42      unfolding X using E
    1.43      by (intro emeasure_limP assms) simp
    1.44 -qed (auto simp: Pi_iff dest: sets_into_space intro: Int_stable_PiE)
    1.45 +qed (auto simp: Pi_iff dest: sets.sets_into_space intro: Int_stable_PiE)
    1.46  
    1.47  lemma emeasure_fun_emb[simp]:
    1.48    assumes L: "J \<noteq> {}" "J \<subseteq> L" "finite L" "L \<subseteq> I" and X: "X \<in> sets (PiM J M)"
    1.49 @@ -155,7 +155,7 @@
    1.50    shows "X = Y"
    1.51  proof (rule injective_vimage_restrict)
    1.52    show "X \<subseteq> (\<Pi>\<^isub>E i\<in>J. space (M i))" "Y \<subseteq> (\<Pi>\<^isub>E i\<in>J. space (M i))"
    1.53 -    using sets[THEN sets_into_space] by (auto simp: space_PiM)
    1.54 +    using sets[THEN sets.sets_into_space] by (auto simp: space_PiM)
    1.55    have "\<forall>i\<in>L. \<exists>x. x \<in> space (M i)"
    1.56    proof
    1.57      fix i assume "i \<in> L"
    1.58 @@ -219,7 +219,7 @@
    1.59        fix A assume "A \<in> prod_algebra I M" with `I \<noteq> {}` show "A \<in> generator"
    1.60          by (auto intro!: generatorI' sets_PiM_I_finite elim!: prod_algebraE)
    1.61      qed
    1.62 -  qed (auto simp: generator_def space_PiM[symmetric] intro!: sigma_sets_subset)
    1.63 +  qed (auto simp: generator_def space_PiM[symmetric] intro!: sets.sigma_sets_subset)
    1.64  qed
    1.65  
    1.66  lemma generatorI:
    1.67 @@ -317,14 +317,14 @@
    1.68      have JK_disj: "emb (J \<union> K) J X \<inter> emb (J \<union> K) K Y = {}"
    1.69        apply (rule prod_emb_injective[of "J \<union> K" I])
    1.70        apply (insert `A \<inter> B = {}` JK J K)
    1.71 -      apply (simp_all add: Int prod_emb_Int)
    1.72 +      apply (simp_all add: sets.Int prod_emb_Int)
    1.73        done
    1.74      have AB: "A = emb I (J \<union> K) (emb (J \<union> K) J X)" "B = emb I (J \<union> K) (emb (J \<union> K) K Y)"
    1.75        using J K by simp_all
    1.76      then have "\<mu>G (A \<union> B) = \<mu>G (emb I (J \<union> K) (emb (J \<union> K) J X \<union> emb (J \<union> K) K Y))"
    1.77        by simp
    1.78      also have "\<dots> = emeasure (limP (J \<union> K) M P) (emb (J \<union> K) J X \<union> emb (J \<union> K) K Y)"
    1.79 -      using JK J(1, 4) K(1, 4) by (simp add: \<mu>G_eq Un del: prod_emb_Un)
    1.80 +      using JK J(1, 4) K(1, 4) by (simp add: \<mu>G_eq sets.Un del: prod_emb_Un)
    1.81      also have "\<dots> = \<mu>G A + \<mu>G B"
    1.82        using J K JK_disj by (simp add: plus_emeasure[symmetric])
    1.83      finally show "\<mu>G (A \<union> B) = \<mu>G A + \<mu>G B" .