src/HOL/Probability/ex/Koepf_Duermuth_Countermeasure.thy

 (* Author: Johannes Hölzl, TU München *)
 
 header {* Formalization of a Countermeasure by Koepf \& Duermuth 2009 *}
 
 theory Koepf_Duermuth_Countermeasure
-  imports Information "~~/src/HOL/Library/Permutation"
+  imports "~~/src/HOL/Probability/Information" "~~/src/HOL/Library/Permutation"
 begin
 
 lemma
   fixes p u :: "'a \<Rightarrow> real"
   assumes "1 < b"

   and b_gt_1[simp, intro]: "1 < b"
 
 lemma (in finite_information) positive_p_sum[simp]: "0 \<le> setsum p X"
    by (auto intro!: setsum_nonneg)
 
-sublocale finite_information \<subseteq> finite_measure_space "\<lparr> space = \<Omega>, sets = Pow \<Omega>, measure = \<lambda>S. Real (setsum p S)\<rparr>"
+sublocale finite_information \<subseteq> finite_measure_space "\<lparr> space = \<Omega>, sets = Pow \<Omega>, measure = \<lambda>S. extreal (setsum p S)\<rparr>"
   by (rule finite_measure_spaceI) (simp_all add: setsum_Un_disjoint finite_subset)
 
-sublocale finite_information \<subseteq> finite_prob_space "\<lparr> space = \<Omega>, sets = Pow \<Omega>, measure = \<lambda>S. Real (setsum p S)\<rparr>"
+sublocale finite_information \<subseteq> finite_prob_space "\<lparr> space = \<Omega>, sets = Pow \<Omega>, measure = \<lambda>S. extreal (setsum p S)\<rparr>"
+  by default (simp add: one_extreal_def)
+
+sublocale finite_information \<subseteq> information_space "\<lparr> space = \<Omega>, sets = Pow \<Omega>, measure = \<lambda>S. extreal (setsum p S)\<rparr>" b
   by default simp
 
-sublocale finite_information \<subseteq> information_space "\<lparr> space = \<Omega>, sets = Pow \<Omega>, measure = \<lambda>S. Real (setsum p S)\<rparr>" b
-  by default simp
+lemma (in finite_information) \<mu>'_eq: "A \<subseteq> \<Omega> \<Longrightarrow> \<mu>' A = setsum p A"
+  unfolding \<mu>'_def by auto
 
 locale koepf_duermuth = K: finite_information keys K b + M: finite_information messages M b
     for b :: real
     and keys :: "'key set" and K :: "'key \<Rightarrow> real"
     and messages :: "'message set" and M :: "'message \<Rightarrow> real" +

 qed auto
 
 lemma SIGMA_image_vimage:
   "snd ` (SIGMA x:f`X. f -` {x} \<inter> X) = X"
   by (auto simp: image_iff)
-
-lemma zero_le_eq_True: "0 \<le> (x::pextreal) \<longleftrightarrow> True" by simp
-
-lemma Real_setprod:
-  assumes"\<And>i. i\<in>X \<Longrightarrow> 0 \<le> f i"
-  shows "(\<Prod>i\<in>X. Real (f i)) = Real (\<Prod>i\<in>X. f i)"
-proof cases
-  assume "finite X"
-  from this assms show ?thesis by induct (auto simp: mult_le_0_iff)
-qed simp
 
 lemma inj_Cons[simp]: "\<And>X. inj_on (\<lambda>(xs, x). x#xs) X" by (auto intro!: inj_onI)
 
 lemma setprod_setsum_distrib_lists:
   fixes P and S :: "'a set" and f :: "'a \<Rightarrow> _::semiring_0" assumes "finite S"

 
 abbreviation
  "p A \<equiv> setsum P A"
 
 abbreviation probability ("\<P>'(_') _") where
- "\<P>(X) x \<equiv> real (distribution X x)"
+ "\<P>(X) x \<equiv> distribution X x"
 
 abbreviation joint_probability ("\<P>'(_, _') _") where
- "\<P>(X, Y) x \<equiv> real (joint_distribution X Y x)"
+ "\<P>(X, Y) x \<equiv> joint_distribution X Y x"
 
 abbreviation conditional_probability ("\<P>'(_|_') _") where
  "\<P>(X|Y) x \<equiv> \<P>(X, Y) x / \<P>(Y) (snd`x)"
 
 notation

 lemma \<P>_k: assumes "k \<in> keys" shows "\<P>(fst) {k} = K k"
 proof -
   from assms have *:
       "fst -` {k} \<inter> msgs = {k}\<times>{ms. length ms = n \<and> (\<forall>M\<in>set ms. M \<in> messages)}"
     unfolding msgs_def by auto
-  show "\<P>(fst) {k} = K k" unfolding distribution_def
-    apply (simp add: *) unfolding P_def
+  show "\<P>(fst) {k} = K k"
+    apply (simp add: \<mu>'_eq distribution_def)
+    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"]
-    by (simp add: setsum_right_distrib[symmetric] subset_eq setprod_1)
+    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)
 qed
 
 lemma fst_image_msgs[simp]: "fst`msgs = keys"
 proof -
   from M.not_empty obtain m where "m \<in> messages" by auto

       then have **: "\<And>ms. length ms = n \<Longrightarrow> OB (k, ms) = obs \<longleftrightarrow> (\<forall>i<n. observe k (ms!i) = obs ! i)"
         unfolding OB_def msgs_def by (simp add: image_iff list_eq_iff_nth_eq)
 
       have "\<P>(OB, fst) {(obs, k)} / K k =
           p ({k}\<times>{ms. (k,ms) \<in> msgs \<and> OB (k,ms) = obs}) / K k"
-        unfolding distribution_def by (auto intro!: arg_cong[where f=p])
+        apply (simp add: distribution_def \<mu>'_eq) by (auto intro!: arg_cong[where f=p])
       also have "\<dots> =
           (\<Prod>i<n. \<Sum>m\<in>{m\<in>messages. observe k m = obs ! i}. M m)"
         unfolding P_def using `K k \<noteq> 0` `k \<in> keys`
         apply (simp add: setsum_cartesian_product' setsum_divide_distrib msgs_def ** cong: conj_cong)
         apply (subst setprod_setsum_distrib_lists[OF M.finite_space, unfolded subset_eq]) ..

       (\<Union>obs'\<in>?S obs. ((\<lambda>x. (OB x, fst x)) -` {(obs', k)} \<inter> msgs))" by auto
     have df: "disjoint_family_on (\<lambda>obs'. (\<lambda>x. (OB x, fst x)) -` {(obs', k)} \<inter> msgs) (?S obs)"
       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 distribution_def comp_def
-      using real_finite_measure_finite_Union[OF _ df]
+      using finite_measure_finite_Union[OF _ _ df]
       by (force 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 `k \<in> keys` `K k \<noteq> 0` obs] real_eq_of_nat)
     finally have "\<P>(t\<circ>OB, fst) {(t obs, k)} = real (card (?S obs)) * \<P>(OB, fst) {(obs, k)}" .}
   note P_t_eq_P_OB = this

   { fix k obs assume "k \<in> keys" and obs: "obs \<in> OB`msgs"
     then have "t -`{t obs} \<inter> OB`msgs \<noteq> {}" (is "?S \<noteq> {}") by auto
     then have "real (card ?S) \<noteq> 0" by auto
 
     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 real_distribution_order'[of fst k "t\<circ>OB" "t obs"]
+      using distribution_order(7,8)[where X=fst and x=k and Y="t\<circ>OB" and y="t obs"]
       by (subst joint_distribution_commute) auto
     also have "\<P>(t\<circ>OB) {t obs} = (\<Sum>k'\<in>keys. \<P>(t\<circ>OB|fst) {(t obs, k')} * \<P>(fst) {k'})"
-      using setsum_real_distribution(2)[of "t\<circ>OB" fst "t obs", symmetric]
-      using real_distribution_order'[of fst _ "t\<circ>OB" "t obs"] by (auto intro!: setsum_cong)
+      using setsum_distribution(2)[of "t\<circ>OB" fst "t obs", symmetric]
+      by (auto intro!: setsum_cong distribution_order(8))
     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)
     also have "(\<Sum>k'\<in>keys. \<P>(OB|fst) {(obs, k')} * \<P>(fst) {k'}) = \<P>(OB) {obs}"
-      using setsum_real_distribution(2)[of OB fst obs, symmetric]
-      using real_distribution_order'[of fst _ OB obs] by (auto intro!: setsum_cong)
+      using setsum_distribution(2)[of OB fst obs, symmetric]
+      by (auto intro!: setsum_cong distribution_order(8))
     also have "\<P>(OB | fst) {(obs, k)} * \<P>(fst) {k} / \<P>(OB) {obs} = \<P>(fst | OB) {(k, obs)}"
-      using real_distribution_order'[of fst k OB obs]
-      by (subst joint_distribution_commute) auto
+      by (subst joint_distribution_commute) (auto intro!: distribution_order(8))
     finally have "\<P>(fst | t\<circ>OB) {(k, t obs)} = \<P>(fst | OB) {(k, obs)}" . }
   note CP_T_eq_CP_O = this
 
   let "?H obs" = "(\<Sum>k\<in>keys. \<P>(fst|OB) {(k, obs)} * log b (\<P>(fst|OB) {(k, obs)})) :: real"
   let "?Ht obs" = "(\<Sum>k\<in>keys. \<P>(fst|t\<circ>OB) {(k, obs)} * log b (\<P>(fst|t\<circ>OB) {(k, obs)})) :: real"

       (\<Union>obs\<in>?S (OB x). OB -` {obs} \<inter> msgs)" by auto
     have df: "disjoint_family_on (\<lambda>obs. OB -` {obs} \<inter> msgs) (?S (OB x))"
       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 distribution_def comp_def
-      using real_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
 
   txt {* Lemma 3 *}
   have "\<H>(fst | OB) = -(\<Sum>obs\<in>OB`msgs. \<P>(OB) {obs} * ?Ht (t obs))"