src/HOL/Probability/Infinite_Product_Measure.thy
changeset 57418 6ab1c7cb0b8d
parent 56996 891e992e510f
child 57512 cc97b347b301
     1.1 --- a/src/HOL/Probability/Infinite_Product_Measure.thy	Fri Jun 27 22:08:55 2014 +0200
     1.2 +++ b/src/HOL/Probability/Infinite_Product_Measure.thy	Sat Jun 28 09:16:42 2014 +0200
     1.3 @@ -322,12 +322,12 @@
     1.4        using J  `I \<noteq> {}` by (subst mu_G_spec[OF _ _ _ refl]) (auto simp: emeasure_PiM Pi_iff)
     1.5      also have "\<dots> = (\<Prod>j\<in>J \<union> {i \<in> I. emeasure (M i) (space (M i)) \<noteq> 1}.
     1.6        if j \<in> J then emeasure (M j) (X j) else emeasure (M j) (space (M j)))"
     1.7 -      using J `I \<noteq> {}` by (intro setprod_mono_one_right) (auto simp: M.emeasure_space_1)
     1.8 +      using J `I \<noteq> {}` by (intro setprod.mono_neutral_right) (auto simp: M.emeasure_space_1)
     1.9      finally show "\<mu> (emb I J (Pi\<^sub>E J X)) = \<dots>" .
    1.10    next
    1.11      let ?F = "\<lambda>j. if j \<in> J then emeasure (M j) (X j) else emeasure (M j) (space (M j))"
    1.12      have "(\<Prod>j\<in>J \<union> {i \<in> I. emeasure (M i) (space (M i)) \<noteq> 1}. ?F j) = (\<Prod>j\<in>J. ?F j)"
    1.13 -      using X `I \<noteq> {}` by (intro setprod_mono_one_right) (auto simp: M.emeasure_space_1)
    1.14 +      using X `I \<noteq> {}` by (intro setprod.mono_neutral_right) (auto simp: M.emeasure_space_1)
    1.15      then show "(\<Prod>j\<in>J \<union> {i \<in> I. emeasure (M i) (space (M i)) \<noteq> 1}. ?F j) =
    1.16        emeasure (Pi\<^sub>M J M) (Pi\<^sub>E J X)"
    1.17        using X by (auto simp add: emeasure_PiM) 
    1.18 @@ -560,12 +560,12 @@
    1.19    also have "emeasure S ?F = (\<Prod>j\<in>(op + i) -` J. emeasure M (E (i + j)))"
    1.20      using J by (intro emeasure_PiM_emb) (simp_all add: finite_vimageI inj_on_def)
    1.21    also have "\<dots> = (\<Prod>j\<in>J - (J \<inter> {..<i}). emeasure M (E j))"
    1.22 -    by (rule strong_setprod_reindex_cong[where f="\<lambda>x. x - i"])
    1.23 +    by (rule setprod.reindex_cong [of "\<lambda>x. x - i"])
    1.24         (auto simp: image_iff Bex_def not_less nat_eq_diff_eq ac_simps cong: conj_cong intro!: inj_onI)
    1.25    also have "emeasure S ?E = (\<Prod>j\<in>J \<inter> {..<i}. emeasure M (E j))"
    1.26      using J by (intro emeasure_PiM_emb) simp_all
    1.27    also have "(\<Prod>j\<in>J \<inter> {..<i}. emeasure M (E j)) * (\<Prod>j\<in>J - (J \<inter> {..<i}). emeasure M (E j)) = (\<Prod>j\<in>J. emeasure M (E j))"
    1.28 -    by (subst mult_commute) (auto simp: J setprod_subset_diff[symmetric])
    1.29 +    by (subst mult_commute) (auto simp: J setprod.subset_diff[symmetric])
    1.30    finally show "emeasure ?D ?X = (\<Prod>j\<in>J. emeasure M (E j))" .
    1.31  qed simp_all
    1.32  
    1.33 @@ -591,7 +591,7 @@
    1.34    also have "emeasure S ?F = (\<Prod>j\<in>Suc -` J. emeasure M (E (Suc j)))"
    1.35      using J by (intro emeasure_PiM_emb) (simp_all add: finite_vimageI)
    1.36    also have "\<dots> = (\<Prod>j\<in>J - {0}. emeasure M (E j))"
    1.37 -    by (rule strong_setprod_reindex_cong[where f="\<lambda>x. x - 1"])
    1.38 +    by (rule setprod.reindex_cong [of "\<lambda>x. x - 1"])
    1.39         (auto simp: image_iff Bex_def not_less nat_eq_diff_eq ac_simps cong: conj_cong intro!: inj_onI)
    1.40    also have "emeasure M ?E * (\<Prod>j\<in>J - {0}. emeasure M (E j)) = (\<Prod>j\<in>J. emeasure M (E j))"
    1.41      by (auto simp: M.emeasure_space_1 setprod.remove J)