src/HOL/Probability/Caratheodory.thy
changeset 57418 6ab1c7cb0b8d
parent 56994 8d5e5ec1cac3
child 57446 06e195515deb
     1.1 --- a/src/HOL/Probability/Caratheodory.thy	Fri Jun 27 22:08:55 2014 +0200
     1.2 +++ b/src/HOL/Probability/Caratheodory.thy	Sat Jun 28 09:16:42 2014 +0200
     1.3 @@ -22,7 +22,7 @@
     1.4    have g_def: "g = (\<lambda>m. (\<Sum>n. f (m,n)))"
     1.5      using assms by (simp add: fun_eq_iff)
     1.6    have reindex: "\<And>B. (\<Sum>x\<in>B. f (prod_decode x)) = setsum f (prod_decode ` B)"
     1.7 -    by (simp add: setsum_reindex[OF inj_prod_decode] comp_def)
     1.8 +    by (simp add: setsum.reindex[OF inj_prod_decode] comp_def)
     1.9    { fix n
    1.10      let ?M = "\<lambda>f. Suc (Max (f ` prod_decode ` {..<n}))"
    1.11      { fix a b x assume "x < n" and [symmetric]: "(a, b) = prod_decode x"
    1.12 @@ -40,7 +40,7 @@
    1.13        by (auto intro!: setsum_mono3 simp: pos) }
    1.14    ultimately
    1.15    show ?thesis unfolding g_def using pos
    1.16 -    by (auto intro!: SUP_eq  simp: setsum_cartesian_product reindex SUP_upper2
    1.17 +    by (auto intro!: SUP_eq  simp: setsum.cartesian_product reindex SUP_upper2
    1.18                       setsum_nonneg suminf_ereal_eq_SUP SUP_pair
    1.19                       SUP_ereal_setsum[symmetric] incseq_setsumI setsum_nonneg)
    1.20  qed
    1.21 @@ -712,7 +712,7 @@
    1.22    with `volume M f` have "f (\<Union>(A`I)) = (\<Sum>a\<in>A`I. f a)"
    1.23      unfolding volume_def by blast
    1.24    also have "\<dots> = (\<Sum>i\<in>I. f (A i))"
    1.25 -  proof (subst setsum_reindex_nonzero)
    1.26 +  proof (subst setsum.reindex_nontrivial)
    1.27      fix i j assume "i \<in> I" "j \<in> I" "i \<noteq> j" "A i = A j"
    1.28      with `disjoint_family_on A I` have "A i = {}"
    1.29        by (auto simp: disjoint_family_on_def)
    1.30 @@ -753,7 +753,7 @@
    1.31      fix D assume D: "D \<subseteq> M" "finite D" "disjoint D"
    1.32      assume "\<Union>C = \<Union>D"
    1.33      have "(\<Sum>d\<in>D. \<mu> d) = (\<Sum>d\<in>D. \<Sum>c\<in>C. \<mu> (c \<inter> d))"
    1.34 -    proof (intro setsum_cong refl)
    1.35 +    proof (intro setsum.cong refl)
    1.36        fix d assume "d \<in> D"
    1.37        have Un_eq_d: "(\<Union>c\<in>C. c \<inter> d) = d"
    1.38          using `d \<in> D` `\<Union>C = \<Union>D` by auto
    1.39 @@ -775,7 +775,7 @@
    1.40      assume "\<Union>C = \<Union>D"
    1.41      with split_sum[OF C D] split_sum[OF D C]
    1.42      have "(\<Sum>d\<in>D. \<mu> d) = (\<Sum>c\<in>C. \<mu> c)"
    1.43 -      by (simp, subst setsum_commute, simp add: ac_simps) }
    1.44 +      by (simp, subst setsum.commute, simp add: ac_simps) }
    1.45    note sum_eq = this
    1.46  
    1.47    { fix C assume C: "C \<subseteq> M" "finite C" "disjoint C"
    1.48 @@ -810,7 +810,7 @@
    1.49      also have "\<dots> = (\<Sum>c\<in>Ca \<union> Cb. \<mu> c) + (\<Sum>c\<in>Ca \<inter> Cb. \<mu> c)"
    1.50        using C_Int_cases volume_empty[OF `volume M \<mu>`] by (elim disjE) simp_all
    1.51      also have "\<dots> = (\<Sum>c\<in>Ca. \<mu> c) + (\<Sum>c\<in>Cb. \<mu> c)"
    1.52 -      using Ca Cb by (simp add: setsum_Un_Int)
    1.53 +      using Ca Cb by (simp add: setsum.union_inter)
    1.54      also have "\<dots> = \<mu>' a + \<mu>' b"
    1.55        using Ca Cb by (simp add: \<mu>')
    1.56      finally show "\<mu>' (a \<union> b) = \<mu>' a + \<mu>' b"
    1.57 @@ -863,7 +863,7 @@
    1.58          by (simp add: sums_iff)
    1.59      qed
    1.60      also have "\<dots> = (\<Sum>c\<in>C. \<mu> c)"
    1.61 -      using F'(2) by (subst (2) F') (simp add: setsum_reindex)
    1.62 +      using F'(2) by (subst (2) F') (simp add: setsum.reindex)
    1.63      finally show "\<mu> (\<Union>C) = (\<Sum>c\<in>C. \<mu> c)" .
    1.64    next
    1.65      show "\<mu> {} = 0"
    1.66 @@ -983,7 +983,7 @@
    1.67        by (intro suminf_setsum_ereal positiveD2[OF pos] G.Int G.finite_Union)
    1.68           (auto intro: generated_ringI_Basic)
    1.69      also have "\<dots> = (\<Sum>c\<in>C'. \<mu>_r c)"
    1.70 -      using eq V C' by (auto intro!: setsum_cong)
    1.71 +      using eq V C' by (auto intro!: setsum.cong)
    1.72      also have "\<dots> = \<mu>_r (\<Union>C')"
    1.73        using C' Un_A
    1.74        by (subst volume_finite_additive[symmetric, OF V(1)])