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': "(\x\A \ B. f x) = (\x\A. setsum (\y. f (x, y)) B)" - unfolding setsum_cartesian_product by simp + unfolding setsum.cartesian_product by simp lemma split_pairs: "((A, B) = X) \ (fst X = A \ snd X = B)" and @@ -735,8 +735,8 @@ by auto with fin show "(\ x. ?f x \(count_space (X ` space M) \\<^sub>M count_space (Y ` space M))) = (\(x, y)\(\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 "(\(x, y)\(\x. (X x, Y x)) ` space M. Pxy (x, y) * log b (Pxy (x, y) / (Px x * Py y))) = (\(x, y)\(\x. (X x, Y x)) ` space M. 0)" - by (intro setsum_cong) (auto simp: ae) + by (intro setsum.cong) (auto simp: ae) then show "(\(x, y)\(\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 "(\(x, y, z). ?i x y z) = (\x. if x \ (\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 "(\ (x, y, z). ?i x y z \?P) = (\(x, y, z)\(\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 "- (\ (x, y). ?f (x, y) * log b (?f (x, y) / Py y) \?P) = - (\(x, y)\(\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 "\(\x. (X x, Y x)) = - (\x\(\x. (X x, Y x)) ` space M. ?f x * log b (?f x))" using XY by (rule entropy_simple_distributed) also have "\ = - (\x\(\(x, y). (y, x)) ` (\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="\A. prob A * log b (prob A)"]) + by (subst (2) setsum.reindex) (auto simp: inj_on_def intro!: setsum.cong arg_cong[where f="\A. prob A * log b (prob A)"]) also have "\ = - (\x\(\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 "\ = entropy b (count_space (Y ` space M) \\<^sub>M count_space (X ` space M)) (\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 "\(\x. (X x, Y x)) = entropy b (count_space (Y ` space M) \\<^sub>M count_space (X ` space M)) (\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="\A. prob A * log b (prob A)"]) + apply (subst setsum.reindex[OF inj]) + apply (auto intro!: setsum.cong arg_cong[where f="\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="\x. prob (X -` {x} \ 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 "... \ \(f \ X)" using entropy_data_processing[OF sf] .