
diff -r 29fe9bac501b -r 6ab1c7cb0b8d src/HOL/Probability/Information.thy
--- a/src/HOL/Probability/Information.thy	Fri Jun 27 22:08:55 2014 +0200
+++ b/src/HOL/Probability/Information.thy	Sat Jun 28 09:16:42 2014 +0200
@@ -19,7 +19,7 @@
 
 lemma setsum_cartesian_product':
   "(\<Sum>x\<in>A \<times> B. f x) = (\<Sum>x\<in>A. setsum (\<lambda>y. f (x, y)) B)"
-  unfolding setsum_cartesian_product by simp
+  unfolding setsum.cartesian_product by simp
 
 lemma split_pairs:
   "((A, B) = X) \<longleftrightarrow> (fst X = A \<and> snd X = B)" and
@@ -735,8 +735,8 @@
     by auto
   with fin show "(\<integral> x. ?f x \<partial>(count_space (X ` space M) \<Otimes>\<^sub>M count_space (Y ` space M))) =
     (\<Sum>(x, y)\<in>(\<lambda>x. (X x, Y x)) ` space M. Pxy (x, y) * log b (Pxy (x, y) / (Px x * Py y)))"
-    by (auto simp add: pair_measure_count_space lebesgue_integral_count_space_finite setsum_cases split_beta'
-             intro!: setsum_cong)
+    by (auto simp add: pair_measure_count_space lebesgue_integral_count_space_finite setsum.If_cases split_beta'
+             intro!: setsum.cong)
 qed
 
 lemma (in information_space)
@@ -748,7 +748,7 @@
 proof (subst mutual_information_simple_distributed[OF Px Py Pxy])
   have "(\<Sum>(x, y)\<in>(\<lambda>x. (X x, Y x)) ` space M. Pxy (x, y) * log b (Pxy (x, y) / (Px x * Py y))) =
     (\<Sum>(x, y)\<in>(\<lambda>x. (X x, Y x)) ` space M. 0)"
-    by (intro setsum_cong) (auto simp: ae)
+    by (intro setsum.cong) (auto simp: ae)
   then show "(\<Sum>(x, y)\<in>(\<lambda>x. (X x, Y x)) ` space M.
     Pxy (x, y) * log b (Pxy (x, y) / (Px x * Py y))) = 0" by simp
 qed
@@ -1488,7 +1488,7 @@
   have "(\<lambda>(x, y, z). ?i x y z) = (\<lambda>x. if x \<in> (\<lambda>x. (X x, Y x, Z x)) ` space M then ?j (fst x) (fst (snd x)) (snd (snd x)) else 0)"
     by (auto intro!: ext)
   then show "(\<integral> (x, y, z). ?i x y z \<partial>?P) = (\<Sum>(x, y, z)\<in>(\<lambda>x. (X x, Y x, Z x)) ` space M. ?j x y z)"
-    by (auto intro!: setsum_cong simp add: `?P = ?C` lebesgue_integral_count_space_finite simple_distributed_finite setsum_cases split_beta')
+    by (auto intro!: setsum.cong simp add: `?P = ?C` lebesgue_integral_count_space_finite simple_distributed_finite setsum.If_cases split_beta')
 qed
 
 lemma (in information_space) conditional_mutual_information_nonneg:
@@ -1640,7 +1640,7 @@
     by auto
   from Y show "- (\<integral> (x, y). ?f (x, y) * log b (?f (x, y) / Py y) \<partial>?P) =
     - (\<Sum>(x, y)\<in>(\<lambda>x. (X x, Y x)) ` space M. Pxy (x, y) * log b (Pxy (x, y) / Py y))"
-    by (auto intro!: setsum_cong simp add: `?P = ?C` lebesgue_integral_count_space_finite simple_distributed_finite eq setsum_cases split_beta')
+    by (auto intro!: setsum.cong simp add: `?P = ?C` lebesgue_integral_count_space_finite simple_distributed_finite eq setsum.If_cases split_beta')
 qed
 
 lemma (in information_space) conditional_mutual_information_eq_conditional_entropy:
@@ -1671,7 +1671,7 @@
   then show ?thesis
     apply (subst conditional_mutual_information_eq[OF Py Pxy Pxy Pxxy])
     apply (subst conditional_entropy_eq[OF Py Pxy])
-    apply (auto intro!: setsum_cong simp: Pxxy_eq setsum_negf[symmetric] eq setsum_reindex[OF inj]
+    apply (auto intro!: setsum.cong simp: Pxxy_eq setsum_negf[symmetric] eq setsum.reindex[OF inj]
                 log_simps zero_less_mult_iff zero_le_mult_iff field_simps mult_less_0_iff AE_count_space)
     using Py[THEN simple_distributed, THEN distributed_real_AE] Pxy[THEN simple_distributed, THEN distributed_real_AE]
   apply (auto simp add: not_le[symmetric] AE_count_space)
@@ -1857,13 +1857,13 @@
   have "\<H>(\<lambda>x. (X x, Y x)) = - (\<Sum>x\<in>(\<lambda>x. (X x, Y x)) ` space M. ?f x * log b (?f x))"
     using XY by (rule entropy_simple_distributed)
   also have "\<dots> = - (\<Sum>x\<in>(\<lambda>(x, y). (y, x)) ` (\<lambda>x. (X x, Y x)) ` space M. ?g x * log b (?g x))"
-    by (subst (2) setsum_reindex) (auto simp: inj_on_def intro!: setsum_cong arg_cong[where f="\<lambda>A. prob A * log b (prob A)"])
+    by (subst (2) setsum.reindex) (auto simp: inj_on_def intro!: setsum.cong arg_cong[where f="\<lambda>A. prob A * log b (prob A)"])
   also have "\<dots> = - (\<Sum>x\<in>(\<lambda>x. (Y x, X x)) ` space M. ?h x * log b (?h x))"
-    by (auto intro!: setsum_cong)
+    by (auto intro!: setsum.cong)
   also have "\<dots> = entropy b (count_space (Y ` space M) \<Otimes>\<^sub>M count_space (X ` space M)) (\<lambda>x. (Y x, X x))"
     by (subst entropy_distr[OF simple_distributed_joint[OF YX]])
        (auto simp: pair_measure_count_space sigma_finite_measure_count_space_finite lebesgue_integral_count_space_finite
-             cong del: setsum_cong  intro!: setsum_mono_zero_left)
+             cong del: setsum.cong  intro!: setsum.mono_neutral_left)
   finally have "\<H>(\<lambda>x. (X x, Y x)) = entropy b (count_space (Y ` space M) \<Otimes>\<^sub>M count_space (X ` space M)) (\<lambda>x. (Y x, X x))" .
   then show ?thesis
     unfolding conditional_entropy_eq_entropy_simple[OF Y X] by simp
@@ -1882,8 +1882,8 @@
     apply (subst entropy_simple_distributed[OF simple_distributedI[OF simple_function_Pair[OF fX X] refl]])
     apply (subst entropy_simple_distributed[OF simple_distributedI[OF X refl]])
     unfolding eq
-    apply (subst setsum_reindex[OF inj])
-    apply (auto intro!: setsum_cong arg_cong[where f="\<lambda>A. prob A * log b (prob A)"])
+    apply (subst setsum.reindex[OF inj])
+    apply (auto intro!: setsum.cong arg_cong[where f="\<lambda>A. prob A * log b (prob A)"])
     done
 qed
 
@@ -1908,7 +1908,7 @@
     unfolding o_assoc
     apply (subst entropy_simple_distributed[OF simple_distributedI[OF X refl]])
     apply (subst entropy_simple_distributed[OF simple_distributedI[OF simple_function_compose[OF X]], where f="\<lambda>x. prob (X -` {x} \<inter> space M)"])
-    apply (auto intro!: setsum_cong arg_cong[where f=prob] image_eqI simp: the_inv_into_f_f[OF inj] comp_def)
+    apply (auto intro!: setsum.cong arg_cong[where f=prob] image_eqI simp: the_inv_into_f_f[OF inj] comp_def)
     done
   also have "... \<le> \<H>(f \<circ> X)"
     using entropy_data_processing[OF sf] .




