--- a/src/HOL/Probability/ex/Dining_Cryptographers.thy Thu Apr 14 15:55:00 2016 +0200
+++ b/src/HOL/Probability/ex/Dining_Cryptographers.thy Fri Apr 15 11:15:40 2016 +0200
@@ -429,7 +429,7 @@
using \<open>0 < n\<close>
by (simp add: card_inversion card_dc_crypto finite_dc_crypto
subset_eq space_uniform_count_measure measure_uniform_count_measure)
- qed
+ qed simp
show "simple_distributed (uniform_count_measure dc_crypto) payer (\<lambda>x. 1 / real n)"
proof (rule simple_distributedI)
@@ -445,7 +445,7 @@
then show "1 / real n = prob (payer -` {z} \<inter> space (uniform_count_measure dc_crypto))"
using finite_dc_crypto
by (subst measure_uniform_count_measure) (auto simp add: card_dc_crypto space_uniform_count_measure)
- qed
+ qed simp
show "simple_distributed (uniform_count_measure dc_crypto) (\<lambda>x. (inversion x, payer x)) (\<lambda>x. 2 / (real n *2^n))"
proof (rule simple_distributedI)
@@ -467,7 +467,7 @@
then show "2 / (real n * 2 ^ n) = prob ((\<lambda>x. (inversion x, payer x)) -` {x} \<inter> space (uniform_count_measure dc_crypto))"
using \<open>i < n\<close> ys
by (simp add: measure_uniform_count_measure card_payer_and_inversion finite_dc_crypto subset_eq card_dc_crypto)
- qed
+ qed simp
show "\<forall>x\<in>space (uniform_count_measure dc_crypto). 2 / (real n * 2 ^ n) = 2 / 2 ^ n * (1 / real n) "
by simp
--- a/src/HOL/Probability/ex/Koepf_Duermuth_Countermeasure.thy Thu Apr 14 15:55:00 2016 +0200
+++ b/src/HOL/Probability/ex/Koepf_Duermuth_Countermeasure.thy Fri Apr 15 11:15:40 2016 +0200
@@ -109,8 +109,9 @@
lemma measure_point_measure:
"finite \<Omega> \<Longrightarrow> A \<subseteq> \<Omega> \<Longrightarrow> (\<And>x. x \<in> \<Omega> \<Longrightarrow> 0 \<le> p x) \<Longrightarrow>
- measure (point_measure \<Omega> (\<lambda>x. ereal (p x))) A = (\<Sum>i\<in>A. p i)"
- unfolding measure_def by (subst emeasure_point_measure_finite) auto
+ measure (point_measure \<Omega> (\<lambda>x. ennreal (p x))) A = (\<Sum>i\<in>A. p i)"
+ unfolding measure_def
+ by (subst emeasure_point_measure_finite) (auto simp: subset_eq setsum_nonneg)
locale finite_information =
fixes \<Omega> :: "'a set"
@@ -289,7 +290,7 @@
by (simp add: simple_function_def)
lemma entropy_commute: "\<H>(\<lambda>x. (X x, Y x)) = \<H>(\<lambda>x. (Y x, X x))"
- apply (subst (1 2) entropy_simple_distributed[OF simple_distributedI[OF simple_function_finite refl]])
+ apply (subst (1 2) entropy_simple_distributed[OF simple_distributedI[OF simple_function_finite _ refl]])
unfolding space_point_measure
proof -
have eq: "(\<lambda>x. (X x, Y x)) ` msgs = (\<lambda>(x, y). (y, x)) ` (\<lambda>x. (Y x, X x)) ` msgs"
@@ -300,7 +301,7 @@
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
+qed simp_all
lemma (in -) measure_eq_0I: "A = {} \<Longrightarrow> measure M A = 0" by simp
@@ -308,8 +309,8 @@
"\<H>(X | 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}))))"
apply (subst conditional_entropy_eq[OF
- simple_distributedI[OF simple_function_finite refl]
- simple_distributedI[OF simple_function_finite refl]])
+ simple_distributedI[OF simple_function_finite _ refl]
+ simple_distributedI[OF simple_function_finite _ refl]])
unfolding space_point_measure
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}))) =
@@ -325,7 +326,7 @@
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
+qed simp_all
lemma ce_OB_eq_ce_t: "\<I>(fst ; OB) = \<I>(fst ; t\<circ>OB)"
proof -
@@ -371,7 +372,7 @@
unfolding disjoint_family_on_def by auto
have "\<P>(t\<circ>OB ; fst) {(t obs, k)} = (\<Sum>obs'\<in>?S obs. \<P>(OB ; fst) {(obs', k)})"
unfolding comp_def
- using finite_measure_finite_Union[OF _ df]
+ using finite_measure_finite_Union[OF _ _ df]
by (auto simp add: * intro!: setsum_nonneg)
also have "(\<Sum>obs'\<in>?S obs. \<P>(OB ; fst) {(obs', k)}) = real (card (?S obs)) * \<P>(OB ; fst) {(obs, k)}"
by (simp add: t_eq_imp[OF \<open>k \<in> keys\<close> \<open>K k \<noteq> 0\<close> obs])
@@ -391,7 +392,7 @@
have "\<P>(fst | t\<circ>OB) {(k, t obs)} = \<P>(t\<circ>OB | fst) {(t obs, k)} * \<P>(fst) {k} / \<P>(t\<circ>OB) {t obs}"
using finite_measure_mono[of "{x. fst x = k \<and> t (OB x) = t obs} \<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"]
- by (auto simp add: vimage_def conj_commute subset_eq)
+ by (auto simp add: vimage_def conj_commute subset_eq simp del: measure_nonneg)
also have "(\<P>(t\<circ>OB) {t obs}) = (\<Sum>k'\<in>keys. (\<P>(t\<circ>OB|fst) {(t obs, k')}) * (\<P>(fst) {k'}))"
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"]
@@ -431,7 +432,7 @@
unfolding disjoint_family_on_def by auto
have "\<P>(t\<circ>OB) {t (OB x)} = (\<Sum>obs\<in>?S (OB x). \<P>(OB) {obs})"
unfolding comp_def
- using finite_measure_finite_Union[OF _ df]
+ using finite_measure_finite_Union[OF _ _ df]
by (force simp add: * intro!: setsum_nonneg) }
note P_t_sum_P_O = this
@@ -468,7 +469,7 @@
also have "\<dots> \<le> \<H>(t\<circ>OB)"
using conditional_entropy_nonneg[of "t\<circ>OB" fst] by simp
also have "\<dots> \<le> log b (real (card ((t\<circ>OB)`msgs)))"
- using entropy_le_card[of "t\<circ>OB", OF simple_distributedI[OF simple_function_finite refl]] by simp
+ using entropy_le_card[of "t\<circ>OB", OF simple_distributedI[OF simple_function_finite _ refl]] by simp
also have "\<dots> \<le> log b (real (n + 1)^card observations)"
using card_T_bound not_empty
by (auto intro!: log_le simp: card_gt_0_iff of_nat_power [symmetric] simp del: of_nat_power of_nat_Suc)