diff -r 29fe9bac501b -r 6ab1c7cb0b8d src/HOL/Probability/Caratheodory.thy
--- a/src/HOL/Probability/Caratheodory.thy Fri Jun 27 22:08:55 2014 +0200
+++ b/src/HOL/Probability/Caratheodory.thy Sat Jun 28 09:16:42 2014 +0200
@@ -22,7 +22,7 @@
have g_def: "g = (\m. (\n. f (m,n)))"
using assms by (simp add: fun_eq_iff)
have reindex: "\B. (\x\B. f (prod_decode x)) = setsum f (prod_decode ` B)"
- by (simp add: setsum_reindex[OF inj_prod_decode] comp_def)
+ by (simp add: setsum.reindex[OF inj_prod_decode] comp_def)
{ fix n
let ?M = "\f. Suc (Max (f ` prod_decode ` {..(A`I)) = (\a\A`I. f a)"
unfolding volume_def by blast
also have "\ = (\i\I. f (A i))"
- proof (subst setsum_reindex_nonzero)
+ proof (subst setsum.reindex_nontrivial)
fix i j assume "i \ I" "j \ I" "i \ j" "A i = A j"
with `disjoint_family_on A I` have "A i = {}"
by (auto simp: disjoint_family_on_def)
@@ -753,7 +753,7 @@
fix D assume D: "D \ M" "finite D" "disjoint D"
assume "\C = \D"
have "(\d\D. \ d) = (\d\D. \c\C. \ (c \ d))"
- proof (intro setsum_cong refl)
+ proof (intro setsum.cong refl)
fix d assume "d \ D"
have Un_eq_d: "(\c\C. c \ d) = d"
using `d \ D` `\C = \D` by auto
@@ -775,7 +775,7 @@
assume "\C = \D"
with split_sum[OF C D] split_sum[OF D C]
have "(\d\D. \ d) = (\c\C. \ c)"
- by (simp, subst setsum_commute, simp add: ac_simps) }
+ by (simp, subst setsum.commute, simp add: ac_simps) }
note sum_eq = this
{ fix C assume C: "C \ M" "finite C" "disjoint C"
@@ -810,7 +810,7 @@
also have "\ = (\c\Ca \ Cb. \ c) + (\c\Ca \ Cb. \ c)"
using C_Int_cases volume_empty[OF `volume M \`] by (elim disjE) simp_all
also have "\ = (\c\Ca. \ c) + (\c\Cb. \ c)"
- using Ca Cb by (simp add: setsum_Un_Int)
+ using Ca Cb by (simp add: setsum.union_inter)
also have "\ = \' a + \' b"
using Ca Cb by (simp add: \')
finally show "\' (a \ b) = \' a + \' b"
@@ -863,7 +863,7 @@
by (simp add: sums_iff)
qed
also have "\ = (\c\C. \ c)"
- using F'(2) by (subst (2) F') (simp add: setsum_reindex)
+ using F'(2) by (subst (2) F') (simp add: setsum.reindex)
finally show "\ (\C) = (\c\C. \ c)" .
next
show "\ {} = 0"
@@ -983,7 +983,7 @@
by (intro suminf_setsum_ereal positiveD2[OF pos] G.Int G.finite_Union)
(auto intro: generated_ringI_Basic)
also have "\ = (\c\C'. \_r c)"
- using eq V C' by (auto intro!: setsum_cong)
+ using eq V C' by (auto intro!: setsum.cong)
also have "\ = \_r (\C')"
using C' Un_A
by (subst volume_finite_additive[symmetric, OF V(1)])