--- a/src/HOL/Probability/ex/Koepf_Duermuth_Countermeasure.thy Fri Jun 27 22:08:55 2014 +0200
+++ b/src/HOL/Probability/ex/Koepf_Duermuth_Countermeasure.thy Sat Jun 28 09:16:42 2014 +0200
@@ -99,8 +99,8 @@
by force+
show ?case unfolding *
using Suc[of "\<lambda>i. P (Suc i)"]
- by (simp add: setsum_reindex split_conv setsum_cartesian_product'
- lessThan_Suc_eq_insert_0 setprod_reindex setsum_left_distrib[symmetric] setsum_right_distrib[symmetric])
+ by (simp add: setsum.reindex split_conv setsum_cartesian_product'
+ lessThan_Suc_eq_insert_0 setprod.reindex setsum_left_distrib[symmetric] setsum_right_distrib[symmetric])
qed
declare space_point_measure[simp]
@@ -168,7 +168,7 @@
case (Suc n)
then show ?case
by (simp add: lists_length_Suc_eq lessThan_Suc_eq_insert_0
- setsum_reindex setprod_reindex)
+ setsum.reindex setprod.reindex)
qed
then show "setsum P msgs = 1"
unfolding msgs_def P_def by simp
@@ -255,7 +255,7 @@
apply (simp add: * P_def)
apply (simp add: setsum_cartesian_product')
using setprod_setsum_distrib_lists[OF M.finite_space, of M n "\<lambda>x x. True"] `k \<in> keys`
- by (auto simp add: setsum_right_distrib[symmetric] subset_eq setprod_1)
+ by (auto simp add: setsum_right_distrib[symmetric] subset_eq setprod.neutral_const)
qed
lemma fst_image_msgs[simp]: "fst`msgs = keys"
@@ -297,8 +297,8 @@
show "- (\<Sum>x\<in>(\<lambda>x. (X x, Y x)) ` msgs. (\<P>(X ; Y) {x}) * log b (\<P>(X ; Y) {x})) =
- (\<Sum>x\<in>(\<lambda>x. (Y x, X x)) ` msgs. (\<P>(Y ; X) {x}) * log b (\<P>(Y ; X) {x}))"
unfolding eq
- apply (subst setsum_reindex)
- apply (auto simp: vimage_def inj_on_def intro!: setsum_cong arg_cong[where f="\<lambda>x. prob x * log b (prob x)"])
+ apply (subst setsum.reindex)
+ apply (auto simp: vimage_def inj_on_def intro!: setsum.cong arg_cong[where f="\<lambda>x. prob x * log b (prob x)"])
done
qed
@@ -314,15 +314,15 @@
proof -
have "- (\<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}))) =
- (\<Sum>x\<in>X`msgs. (\<Sum>y\<in>Y`msgs. (\<P>(X ; Y) {(x, y)}) * log b ((\<P>(X ; Y) {(x, y)}) / (\<P>(Y) {y}))))"
- unfolding setsum_cartesian_product
- apply (intro arg_cong[where f=uminus] setsum_mono_zero_left)
+ unfolding setsum.cartesian_product
+ apply (intro arg_cong[where f=uminus] setsum.mono_neutral_left)
apply (auto simp: vimage_def image_iff intro!: measure_eq_0I)
apply metis
done
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}))))"
- by (subst setsum_commute) rule
+ by (subst setsum.commute) rule
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}))))"
- by (auto simp add: setsum_right_distrib vimage_def intro!: setsum_cong prob_conj_imp1)
+ by (auto simp add: setsum_right_distrib vimage_def intro!: setsum.cong prob_conj_imp1)
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}))) =
-(\<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}))))" .
qed
@@ -358,7 +358,7 @@
have "(\<P>(OB ; fst) {(obs, k)}) / K k = (\<P>(OB ; fst) {(obs', k)}) / K k"
unfolding *[OF obs] *[OF obs']
- using t_f(1) obs_t_f by (subst (2) t_f(2)) (simp add: setprod_reindex)
+ using t_f(1) obs_t_f by (subst (2) t_f(2)) (simp add: setprod.reindex)
then have "(\<P>(OB ; fst) {(obs, k)}) = (\<P>(OB ; fst) {(obs', k)})"
using `K k \<noteq> 0` by auto }
note t_eq_imp = this
@@ -396,17 +396,17 @@
using finite_measure_mono[of "{x. t (OB x) = t obs \<and> fst x = k} \<inter> msgs" "{x. fst x = k} \<inter> msgs"]
using measure_nonneg[of \<mu> "{x. fst x = k \<and> t (OB x) = t obs} \<inter> msgs"]
apply (simp add: setsum_distribution_cut[of "t\<circ>OB" "t obs" fst])
- apply (auto intro!: setsum_cong simp: subset_eq vimage_def prob_conj_imp1)
+ apply (auto intro!: setsum.cong simp: subset_eq vimage_def prob_conj_imp1)
done
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'})"
using CP_t_K[OF `k\<in>keys` obs] CP_t_K[OF _ obs] `real (card ?S) \<noteq> 0`
by (simp only: setsum_right_distrib[symmetric] ac_simps
mult_divide_mult_cancel_left[OF `real (card ?S) \<noteq> 0`]
- cong: setsum_cong)
+ cong: setsum.cong)
also have "(\<Sum>k'\<in>keys. \<P>(OB|fst) {(obs, k')} * \<P>(fst) {k'}) = \<P>(OB) {obs}"
using setsum_distribution_cut[of OB obs fst]
- by (auto intro!: setsum_cong simp: prob_conj_imp1 vimage_def)
+ by (auto intro!: setsum.cong simp: prob_conj_imp1 vimage_def)
also have "\<P>(OB | fst) {(obs, k)} * \<P>(fst) {k} / \<P>(OB) {obs} = \<P>(fst | OB) {(k, obs)}"
by (auto simp: vimage_def conj_commute prob_conj_imp2)
finally have "\<P>(fst | t\<circ>OB) {(k, t obs)} = \<P>(fst | OB) {(k, obs)}" . }
@@ -440,13 +440,13 @@
unfolding conditional_entropy_eq_ce_with_hypothesis using * by simp
also have "\<dots> = -(\<Sum>obs\<in>t`OB`msgs. \<P>(t\<circ>OB) {obs} * ?Ht obs)"
apply (subst SIGMA_image_vimage[symmetric, of "OB`msgs" t])
- apply (subst setsum_reindex)
+ apply (subst setsum.reindex)
apply (fastforce intro!: inj_onI)
apply simp
- apply (subst setsum_Sigma[symmetric, unfolded split_def])
+ apply (subst setsum.Sigma[symmetric, unfolded split_def])
using finite_space apply fastforce
using finite_space apply fastforce
- apply (safe intro!: setsum_cong)
+ apply (safe intro!: setsum.cong)
using P_t_sum_P_O
by (simp add: setsum_divide_distrib[symmetric] field_simps **
setsum_right_distrib[symmetric] setsum_left_distrib[symmetric])