src/HOL/Probability/ex/Koepf_Duermuth_Countermeasure.thy
changeset 66804 3f9bb52082c4
parent 66453 cc19f7ca2ed6
child 67399 eab6ce8368fa
     1.1 --- a/src/HOL/Probability/ex/Koepf_Duermuth_Countermeasure.thy	Sun Oct 08 22:28:20 2017 +0200
     1.2 +++ b/src/HOL/Probability/ex/Koepf_Duermuth_Countermeasure.thy	Sun Oct 08 22:28:20 2017 +0200
     1.3 @@ -321,7 +321,7 @@
     1.4      apply metis
     1.5      done
     1.6    also have "\<dots> = - (\<Sum>y\<in>Y`msgs. (\<Sum>x\<in>X`msgs. (\<P>(X ; Y) {(x, y)}) * log b ((\<P>(X ; Y) {(x, y)}) / (\<P>(Y) {y}))))"
     1.7 -    by (subst sum.commute) rule
     1.8 +    by (subst sum.swap) rule
     1.9    also have "\<dots> = -(\<Sum>y\<in>Y`msgs. (\<P>(Y) {y}) * (\<Sum>x\<in>X`msgs. (\<P>(X ; Y) {(x,y)}) / (\<P>(Y) {y}) * log b ((\<P>(X ; Y) {(x,y)}) / (\<P>(Y) {y}))))"
    1.10      by (auto simp add: sum_distrib_left vimage_def intro!: sum.cong prob_conj_imp1)
    1.11    finally show "- (\<Sum>(x, y)\<in>(\<lambda>x. (X x, Y x)) ` msgs. (\<P>(X ; Y) {(x, y)}) * log b ((\<P>(X ; Y) {(x, y)}) / (\<P>(Y) {y}))) =