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.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)])
```