# HG changeset patch
# User hoelzl
# Date 1322744637 -3600
# Node ID a2c32e196d49d507b817431f6a8176cab1bb5fd4
# Parent  10192f9616195159ba0c7d028bfb09b7d628f7a3
rename finite_prob_space.setsum_distribution, it collides with prob_space.setsum_distribution

diff -r 10192f961619 -r a2c32e196d49 src/HOL/Probability/Probability_Measure.thy
--- a/src/HOL/Probability/Probability_Measure.thy	Thu Dec 01 14:03:57 2011 +0100
+++ b/src/HOL/Probability/Probability_Measure.thy	Thu Dec 01 14:03:57 2011 +0100
@@ -962,7 +962,7 @@
      (auto simp add: disjoint_family_on_def sets_eq_Pow inj_on_def
       intro!: arg_cong[where f=prob])
 
-lemma (in finite_prob_space) setsum_distribution:
+lemma (in finite_prob_space) setsum_distribution_cut:
   "(\<Sum>x \<in> X`space M. joint_distribution X Y {(x, y)}) = distribution Y {y}"
   "(\<Sum>y \<in> Y`space M. joint_distribution X Y {(x, y)}) = distribution X {x}"
   "(\<Sum>x \<in> X`space M. joint_distribution X (\<lambda>x. (Y x, Z x)) {(x, y, z)}) = joint_distribution Y Z {(y, z)}"
diff -r 10192f961619 -r a2c32e196d49 src/HOL/Probability/ex/Koepf_Duermuth_Countermeasure.thy
--- a/src/HOL/Probability/ex/Koepf_Duermuth_Countermeasure.thy	Thu Dec 01 14:03:57 2011 +0100
+++ b/src/HOL/Probability/ex/Koepf_Duermuth_Countermeasure.thy	Thu Dec 01 14:03:57 2011 +0100
@@ -430,7 +430,7 @@
       using distribution_order(7,8)[where X=fst and x=k and Y="t\<circ>OB" and y="t obs"]
       by (subst joint_distribution_commute) auto
     also have "\<P>(t\<circ>OB) {t obs} = (\<Sum>k'\<in>keys. \<P>(t\<circ>OB|fst) {(t obs, k')} * \<P>(fst) {k'})"
-      using setsum_distribution(2)[of "t\<circ>OB" fst "t obs", symmetric]
+      using setsum_distribution_cut(2)[of "t\<circ>OB" fst "t obs", symmetric]
       by (auto intro!: setsum_cong distribution_order(8))
     also have "\<P>(t\<circ>OB | fst) {(t obs, k)} * \<P>(fst) {k} / (\<Sum>k'\<in>keys. \<P>(t\<circ>OB|fst) {(t obs, k')} * \<P>(fst) {k'}) =
       \<P>(OB | fst) {(obs, k)} * \<P>(fst) {k} / (\<Sum>k'\<in>keys. \<P>(OB|fst) {(obs, k')} * \<P>(fst) {k'})"
@@ -439,7 +439,7 @@
           mult_divide_mult_cancel_left[OF `real (card ?S) \<noteq> 0`]
         cong: setsum_cong)
     also have "(\<Sum>k'\<in>keys. \<P>(OB|fst) {(obs, k')} * \<P>(fst) {k'}) = \<P>(OB) {obs}"
-      using setsum_distribution(2)[of OB fst obs, symmetric]
+      using setsum_distribution_cut(2)[of OB fst obs, symmetric]
       by (auto intro!: setsum_cong distribution_order(8))
     also have "\<P>(OB | fst) {(obs, k)} * \<P>(fst) {k} / \<P>(OB) {obs} = \<P>(fst | OB) {(k, obs)}"
       by (subst joint_distribution_commute) (auto intro!: distribution_order(8))