Quelle Koepf_Duermuth_Countermeasure.thy Sprache: Isabelle

(* Author: Johannes Hölzl, TU München *)

section \<open>Formalization of a Countermeasure by Koepf \& Duermuth 2009\<close>

theory Koepf_Duermuth_Countermeasure
 imports "HOL-Probability.Information"
begin

lemma SIGMA_image_vimage:
 "snd ` (SIGMA x:f`X. f -` {x} \ X) = X"
 by (auto simp: image_iff)

declare inj_split_Cons[simp]

definition extensionalD :: "'b \ 'a set \ ('a \ 'b) set" where
 "extensionalD d A = {f. \x. x \ A \ f x = d}"

lemma extensionalD_empty[simp]: "extensionalD d {} = {\x. d}"
 unfolding extensionalD_def by (simp add: set_eq_iff fun_eq_iff)

lemma funset_eq_UN_fun_upd_I:
 assumes *: "\f. f \ F (insert a A) \ f(a := d) \ F A"
 and **: "\f. f \ F (insert a A) \ f a \ G (f(a:=d))"
 and ***: "\f x. \ f \ F A ; x \ G f \ \ f(a:=x) \ F (insert a A)"
 shows "F (insert a A) = (\f\F A. fun_upd f a ` (G f))"
proof safe
 fix f assume f: "f \ F (insert a A)"
 show "f \ (\f\F A. fun_upd f a ` G f)"
 proof (rule UN_I[of "f(a := d)"])
 show "f(a := d) \ F A" using *[OF f] .
 show "f \ fun_upd (f(a:=d)) a ` G (f(a:=d))"
 proof (rule image_eqI[of _ _ "f a"])
 show "f a \ G (f(a := d))" using **[OF f] .
 qed simp
 qed
next
 fix f x assume "f \ F A" "x \ G f"
 from ***[OF this] show "f(a := x) \ F (insert a A)" .
qed

lemma extensionalD_insert[simp]:
 assumes "a \ A"
 shows "extensionalD d (insert a A) \ (insert a A \ B) = (\f \ extensionalD d A \ (A \ B). (\b. f(a := b)) ` B)"
 apply (rule funset_eq_UN_fun_upd_I)
 using assms
 by (auto intro!: inj_onI dest: inj_onD split: if_split_asm simp: extensionalD_def)

lemma finite_extensionalD_funcset[simp, intro]:
 assumes "finite A" "finite B"
 shows "finite (extensionalD d A \ (A \ B))"
 using assms by induct auto

lemma fun_upd_eq_iff: "f(a := b) = g(a := b') \ b = b' \ f(a := d) = g(a := d)"
 by (auto simp: fun_eq_iff)

lemma card_funcset:
 assumes "finite A" "finite B"
 shows "card (extensionalD d A \ (A \ B)) = card B ^ card A"
using \<open>finite A\<close> proof induct
 case (insert a A) thus ?case unfolding extensionalD_insert[OF \<open>a \<notin> A\<close>]
 proof (subst card_UN_disjoint, safe, simp_all)
 show "finite (extensionalD d A \ (A \ B))" "\f. finite (fun_upd f a ` B)"
 using \<open>finite B\<close> \<open>finite A\<close> by simp_all
 next
 fix f g b b' assume "f \ g" and eq: "f(a := b) = g(a := b')" and
 ext: "f \ extensionalD d A" "g \ extensionalD d A"
 have "f a = d" "g a = d"
 using ext \<open>a \<notin> A\<close> by (auto simp add: extensionalD_def)
 with \<open>f \<noteq> g\<close> eq show False unfolding fun_upd_eq_iff[of _ _ b _ _ d]
 by (auto simp: fun_upd_idem fun_upd_eq_iff)
 next
 have "card (fun_upd f a ` B) = card B"
 if "f \ extensionalD d A \ (A \ B)" for f
 proof (auto intro!: card_image inj_onI)
 fix b b' assume "f(a := b) = f(a := b')"
 from fun_upd_eq_iff[THEN iffD1, OF this] show "b = b'" by simp
 qed
 then show "(\i\extensionalD d A \ (A \ B). card (fun_upd i a ` B)) = card B * card B ^ card A"
 using insert by simp
 qed
qed simp

lemma prod_sum_distrib_lists:
 fixes P and S :: "'a set" and f :: "'a \ _::semiring_0" assumes "finite S"
 shows "(\ms\{ms. set ms \ S \ length ms = n \ (\ix
 (\<Prod>i<n. \<Sum>m\<in>{m\<in>S. P i m}. f m)"
proof (induct n arbitrary: P)
 case 0 then show ?case by (simp cong: conj_cong)
next
 case (Suc n)
 have *: "{ms. set ms \ S \ length ms = Suc n \ (\i
 (\<lambda>(xs, x). x#xs) ` ({ms. set ms \<subseteq> S \<and> length ms = n \<and> (\<forall>i<n. P (Suc i) (ms ! i))} \<times> {m\<in>S. P 0 m})"
 apply (auto simp: image_iff length_Suc_conv)
 apply force+
 apply (case_tac i)
 by force+
 show ?case unfolding *
 using Suc[of "\i. P (Suc i)"]
 by (simp add: sum.reindex sum.cartesian_product'
 lessThan_Suc_eq_insert_0 prod.reindex sum_distrib_right[symmetric] sum_distrib_left[symmetric])
qed

declare space_point_measure[simp]

declare sets_point_measure[simp]

lemma measure_point_measure:
 "finite \ \ A \ \ \ (\x. x \ \ \ 0 \ p x) \
 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 sum_nonneg)

locale finite_information =
 fixes \<Omega> :: "'a set"
 and p :: "'a \ real"
 and b :: real
 assumes finite_space[simp, intro]: "finite \"
 and p_sums_1[simp]: "(\\\\. p \) = 1"
 and positive_p[simp, intro]: "\x. 0 \ p x"
 and b_gt_1[simp, intro]: "1 < b"

lemma (in finite_information) positive_p_sum[simp]: "0 \ sum p X"
 by (auto intro!: sum_nonneg)

sublocale finite_information \<subseteq> prob_space "point_measure \<Omega> p"
 by standard (simp add: one_ereal_def emeasure_point_measure_finite)

sublocale finite_information \<subseteq> information_space "point_measure \<Omega> p" b
 by standard simp

lemma (in finite_information) \<mu>'_eq: "A \<subseteq> \<Omega> \<Longrightarrow> prob A = sum p A"
 by (auto simp: measure_point_measure)

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 \ real"
 and messages :: "'message set" and M :: "'message \ real" +
 fixes observe :: "'key \ 'message \ 'observation"
 and n :: nat
begin

definition msgs :: "('key \ 'message list) set" where
 "msgs = keys \ {ms. set ms \ messages \ length ms = n}"

definition P :: "('key \ 'message list) \ real" where
 "P = (\(k, ms). K k * (\i

end

sublocale koepf_duermuth \<subseteq> finite_information msgs P b
proof
 show "finite msgs" unfolding msgs_def
 using finite_lists_length_eq[OF M.finite_space, of n]
 by auto

 have [simp]: "\A. inj_on (\(xs, n). n # xs) A" by (force intro!: inj_onI)

 note sum_distrib_left[symmetric, simp]
 note sum_distrib_right[symmetric, simp]
 note sum.cartesian_product'[simp]

 have "(\ms | set ms \ messages \ length ms = n. \x
 proof (induct n)
 case 0 then show ?case by (simp cong: conj_cong)
 next
 case (Suc n)
 then show ?case
 by (simp add: lists_length_Suc_eq lessThan_Suc_eq_insert_0
 sum.reindex prod.reindex)
 qed
 then show "sum P msgs = 1"
 unfolding msgs_def P_def by simp
 have "0 \ (\x\A. M (f x))" for A f
 by (auto simp: prod_nonneg)
 then show "0 \ P x" for x
 unfolding P_def by (auto split: prod.split simp: zero_le_mult_iff)
qed auto

context koepf_duermuth
begin

definition observations :: "'observation set" where
 "observations = (\f\observe ` keys. f ` messages)"

lemma finite_observations[simp, intro]: "finite observations"
 unfolding observations_def by auto

definition OB :: "'key \ 'message list \ 'observation list" where
 "OB = (\(k, ms). map (observe k) ms)"

definition t :: "'observation list \ 'observation \ nat" where
 t_def2: "t seq obs = card { i. i < length seq \ seq ! i = obs}"

lemma t_def: "t seq obs = length (filter ((=) obs) seq)"
 unfolding t_def2 length_filter_conv_card by (subst eq_commute) simp

lemma card_T_bound: "card ((t\OB)`msgs) \ (n+1)^card observations"
proof -
 have "(t\OB)`msgs \ extensionalD 0 observations \ (observations \ {.. n})"
 unfolding observations_def extensionalD_def OB_def msgs_def
 by (auto simp add: t_def comp_def image_iff subset_eq)
 with finite_extensionalD_funcset
 have "card ((t\OB)`msgs) \ card (extensionalD 0 observations \ (observations \ {.. n}))"
 by (rule card_mono) auto
 also have "\ = (n + 1) ^ card observations"
 by (subst card_funcset) auto
 finally show ?thesis .
qed

abbreviation
"p A \ sum P A"

abbreviation
 "\ \ point_measure msgs P"

abbreviation probability (\<open>\'(_') _\<close>) where
 "\

(X) x \ measure \ (X -` x \ msgs)"

abbreviation joint_probability (\<open>\'(_ ; _') _\<close>) where
"\

(X ; Y) x \ \

(\x. (X x, Y x)) x"

no_notation disj (infixr \<open>|\<close> 30)

abbreviation conditional_probability (\<open>\'(_ | _') _\<close>) where
"\

(X | Y) x \ (\

(X ; Y) x) / \

(Y) (snd`x)"

notation
 entropy_Pow (\<open>\<H>'( _ ')\<close>)

notation
 conditional_entropy_Pow (\<open>\<H>'( _ | _ ')\<close>)

notation
 mutual_information_Pow (\<open>\'( _ ; _ ')\<close>)

lemma t_eq_imp_bij_func:
 assumes "t xs = t ys"
 shows "\f. bij_betw f {.. (\i
proof -
 from assms have \<open>mset xs = mset ys\<close>
 using assms by (simp add: fun_eq_iff t_def multiset_eq_iff count_mset count_list_eq_length_filter)
 then obtain p where \<open>p permutes {..<length ys}\<close> \<open>permute_list p ys = xs\<close>
 by (rule mset_eq_permutation)
 then have \<open>bij_betw p {..<length xs} {..<length ys}\<close> \<open>\<forall>i<length xs. xs ! i = ys ! p i\<close>
 by (auto dest: permutes_imp_bij simp add: permute_list_nth)
 then show ?thesis
 by blast
qed

lemma \_k: assumes "k \<in> keys" shows "\(fst) {k} = K k"
proof -
 from assms have *:
 "fst -` {k} \ msgs = {k}\{ms. set ms \ messages \ length ms = n}"
 unfolding msgs_def by auto
 show "(\

(fst) {k}) = K k"
 apply (simp add: \<mu>'_eq)
 apply (simp add: * P_def)
 apply (simp add: sum.cartesian_product')
 using prod_sum_distrib_lists[OF M.finite_space, of M n "\x x. True"] \k \ keys\
 by (auto simp add: sum_distrib_left[symmetric] subset_eq prod.neutral_const)
qed

lemma fst_image_msgs[simp]: "fst`msgs = keys"
proof -
 from M.not_empty obtain m where "m \ messages" by auto
 then have *: "{m. set m \ messages \ length m = n} \ {}"
 by (auto intro!: exI[of _ "replicate n m"])
 then show ?thesis
 unfolding msgs_def fst_image_times if_not_P[OF *] by simp
qed

lemma sum_distribution_cut:
 "\

(X) {x} = (\y \ Y`space \. \

(X ; Y) {(x, y)})"
 by (subst finite_measure_finite_Union[symmetric])
 (auto simp add: disjoint_family_on_def inj_on_def
 intro!: arg_cong[where f=prob])

lemma prob_conj_imp1:
 "prob ({x. Q x} \ msgs) = 0 \ prob ({x. Pr x \ Q x} \ msgs) = 0"
 using finite_measure_mono[of "{x. Pr x \ Q x} \ msgs" "{x. Q x} \ msgs"]
 using measure_nonneg[of \<mu> "{x. Pr x \<and> Q x} \<inter> msgs"]
 by (simp add: subset_eq)

lemma prob_conj_imp2:
 "prob ({x. Pr x} \ msgs) = 0 \ prob ({x. Pr x \ Q x} \ msgs) = 0"
 using finite_measure_mono[of "{x. Pr x \ Q x} \ msgs" "{x. Pr x} \ msgs"]
 using measure_nonneg[of \<mu> "{x. Pr x \<and> Q x} \<inter> msgs"]
 by (simp add: subset_eq)

lemma simple_function_finite: "simple_function \ f"
 by (simp add: simple_function_def)

lemma entropy_commute: "\(\x. (X x, Y x)) = \(\x. (Y x, X x))"
 apply (subst (1 2) entropy_simple_distributed[OF simple_distributedI[OF simple_function_finite _ refl]])
 unfolding space_point_measure
proof -
 have eq: "(\x. (X x, Y x)) ` msgs = (\(x, y). (y, x)) ` (\x. (Y x, X x)) ` msgs"
 by auto
 show "- (\x\(\x. (X x, Y x)) ` msgs. (\

(X ; Y) {x}) * log b (\

(X ; Y) {x})) =
 - (\<Sum>x\<in>(\<lambda>x. (Y x, X x)) ` msgs. (\(Y ; X) {x}) * log b (\(Y ; X) {x}))"
 unfolding eq
 apply (subst sum.reindex)
 apply (auto simp: vimage_def inj_on_def intro!: sum.cong arg_cong[where f="\x. prob x * log b (prob x)"])
 done
qed simp_all

lemma (in -) measure_eq_0I: "A = {} \ measure M A = 0" by simp

lemma conditional_entropy_eq_ce_with_hypothesis:
 "\(X | Y) = -(\y\Y`msgs. (\

(Y) {y}) * (\x\X`msgs. (\

(X ; Y) {(x,y)}) / (\

(Y) {y}) *
 log b ((\(X ; Y) {(x,y)}) / (\(Y) {y}))))"
 apply (subst conditional_entropy_eq[OF
 simple_distributedI[OF simple_function_finite _ refl]
 simple_distributedI[OF simple_function_finite _ refl]])
 unfolding space_point_measure
proof -
 have "- (\(x, y)\(\x. (X x, Y x)) ` msgs. (\

(X ; Y) {(x, y)}) * log b ((\

(X ; Y) {(x, y)}) / (\

(Y) {y}))) =
 - (\<Sum>x\<in>X`msgs. (\<Sum>y\<in>Y`msgs. (\(X ; Y) {(x, y)}) * log b ((\(X ; Y) {(x, y)}) / (\(Y) {y}))))"
 unfolding sum.cartesian_product
 apply (intro arg_cong[where f=uminus] sum.mono_neutral_left)
 apply (auto simp: vimage_def image_iff intro!: measure_eq_0I)
 apply metis
 done
 also have "\ = - (\y\Y`msgs. (\x\X`msgs. (\

(X ; Y) {(x, y)}) * log b ((\

(X ; Y) {(x, y)}) / (\

(Y) {y}))))"
by (subst sum.swap) rule
also have "\ = -(\y\Y`msgs. (\

(Y) {y}) * (\x\X`msgs. (\

(X ; Y) {(x,y)}) / (\

(Y) {y}) * log b ((\

(X ; Y) {(x,y)}) / (\

(Y) {y}))))"
by (auto simp add: sum_distrib_left vimage_def intro!: sum.cong prob_conj_imp1)
finally show "- (\(x, y)\(\x. (X x, Y x)) ` msgs. (\

(X ; Y) {(x, y)}) * log b ((\

(X ; Y) {(x, y)}) / (\

(Y) {y}))) =
 -(\<Sum>y\<in>Y`msgs. (\(Y) {y}) * (\<Sum>x\<in>X`msgs. (\(X ; Y) {(x,y)}) / (\(Y) {y}) * log b ((\(X ; Y) {(x,y)}) / (\(Y) {y}))))" .
qed simp_all

lemma ce_OB_eq_ce_t: "\(fst ; OB) = \(fst ; t\OB)"
proof -
 txt \<open>Lemma 2\<close>

 have t_eq_imp: "(\

(OB ; fst) {(obs, k)}) = (\

(OB ; fst) {(obs', k)})"
    if "k \ keys" "K k \ 0" and obs': "obs' \ OB ` msgs" and obs: "obs \ OB ` msgs"
      and eq: "t obs = t obs'"
    for k obs obs'
  proof -
    from t_eq_imp_bij_func[OF eq]
    obtain t_f where "bij_betw t_f {.. and
      obs_t_f: "\i. i obs!i = obs' ! t_f i"
      using obs obs' unfolding OB_def msgs_def by auto
    then have t_f: "inj_on t_f {.. "{.. unfolding bij_betw_def by auto

    have *: "(\

(OB ; fst) {(obs, k)}) / K k =
 (\<Prod>i<n. \<Sum>m\<in>{m\<in>messages. observe k m = obs ! i}. M m)"
 if "obs \ OB`msgs" for obs
 proof -
 from that have **: "length ms = n \ OB (k, ms) = obs \ (\i
 for ms
 unfolding OB_def msgs_def by (simp add: image_iff list_eq_iff_nth_eq)
 have "(\

(OB ; fst) {(obs, k)}) / K k =
 p ({k}\<times>{ms. (k,ms) \<in> msgs \<and> OB (k,ms) = obs}) / K k"
 by (simp add: \<mu>'_eq) (auto intro!: arg_cong[where f=p])
 also have "\ = (\im\{m\messages. observe k m = obs ! i}. M m)"
 unfolding P_def using \<open>K k \<noteq> 0\<close> \<open>k \<in> keys\<close>
 apply (simp add: sum.cartesian_product' sum_divide_distrib msgs_def ** cong: conj_cong)
 apply (subst prod_sum_distrib_lists[OF M.finite_space]) ..
 finally show ?thesis .
 qed

 have "(\

(OB ; fst) {(obs, k)}) / K k = (\

(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: prod.reindex)
 then show ?thesis using \<open>K k \<noteq> 0\<close> by auto
 qed

 let ?S = "\obs. t -`{t obs} \ OB`msgs"
 have P_t_eq_P_OB: "\

(t\OB ; fst) {(t obs, k)} = real (card (?S obs)) * \

(OB ; fst) {(obs, k)}"
 if "k \ keys" "K k \ 0" and obs: "obs \ OB`msgs"
 for k obs
 proof -
 have *: "((\x. (t (OB x), fst x)) -` {(t obs, k)} \ msgs) =
 (\<Union>obs'\<in>?S obs. ((\<lambda>x. (OB x, fst x)) -` {(obs', k)} \<inter> msgs))" by auto
 have df: "disjoint_family_on (\obs'. (\x. (OB x, fst x)) -` {(obs', k)} \ msgs) (?S obs)"
 unfolding disjoint_family_on_def by auto
 have "\

(t\OB ; fst) {(t obs, k)} = (\obs'\?S obs. \

(OB ; fst) {(obs', k)})"
      unfolding comp_def
      using finite_measure_finite_Union[OF _ _ df]
      by (auto simp add: * intro!: sum_nonneg)
    also have "(\obs'\?S obs. \

(OB ; fst) {(obs', k)}) = real (card (?S obs)) * \

(OB ; fst) {(obs, k)}"
 by (simp add: t_eq_imp[OF \<open>k \<in> keys\<close> \<open>K k \<noteq> 0\<close> obs])
 finally show ?thesis .
 qed

 have CP_t_K: "\

(t\OB | fst) {(t obs, k)} =
 real (card (t -` {t obs} \<inter> OB ` msgs)) * \(OB | fst) {(obs, k)}"
 if k: "k \ keys" and obs: "obs \ OB`msgs" for k obs
 using \_k[OF k] P_t_eq_P_OB[OF k _ obs] by auto

 have CP_T_eq_CP_O: "\

(fst | t\OB) {(k, t obs)} = \

(fst | OB) {(k, obs)}"
    if "k \ keys" and obs: "obs \ OB`msgs" for k obs
  proof -
    from that have "t -`{t obs} \ OB`msgs \ {}" (is "?S \ {}") by auto
    then have "real (card ?S) \ 0" by auto

    have "\

(fst | t\OB) {(k, t obs)} = \

(t\OB | fst) {(t obs, k)} * \

(fst) {k} / \

(t\OB) {t obs}"
 using finite_measure_mono[of "{x. fst x = k \ t (OB x) = t obs} \ msgs" "{x. fst x = k} \ 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 simp del: measure_nonneg)
 also have "(\

(t\OB) {t obs}) = (\k'\keys. (\

(t\OB|fst) {(t obs, k')}) * (\

(fst) {k'}))"
 using finite_measure_mono[of "{x. t (OB x) = t obs \ fst x = k} \ msgs" "{x. fst x = k} \ msgs"]
 using measure_nonneg[of \<mu> "{x. fst x = k \<and> t (OB x) = t obs} \<inter> msgs"]
 apply (simp add: sum_distribution_cut[of "t\OB" "t obs" fst])
 apply (auto intro!: sum.cong simp: subset_eq vimage_def prob_conj_imp1)
 done
 also have "\

(t\OB | fst) {(t obs, k)} * \

(fst) {k} / (\k'\keys. \

(t\OB|fst) {(t obs, k')} * \

(fst) {k'}) =
 \(OB | fst) {(obs, k)} * \(fst) {k} / (\<Sum>k'\<in>keys. \(OB|fst) {(obs, k')} * \(fst) {k'})"
 using CP_t_K[OF \<open>k\<in>keys\<close> obs] CP_t_K[OF _ obs] \<open>real (card ?S) \<noteq> 0\<close>
 by (simp only: sum_distrib_left[symmetric] ac_simps
 mult_divide_mult_cancel_left[OF \<open>real (card ?S) \<noteq> 0\<close>]
 cong: sum.cong)
 also have "(\k'\keys. \

(OB|fst) {(obs, k')} * \

(fst) {k'}) = \

(OB) {obs}"
      using sum_distribution_cut[of OB obs fst]
      by (auto intro!: sum.cong simp: prob_conj_imp1 vimage_def)
    also have "\

(OB | fst) {(obs, k)} * \

(fst) {k} / \

(OB) {obs} = \

(fst | OB) {(k, obs)}"
      by (auto simp: vimage_def conj_commute prob_conj_imp2)
    finally show ?thesis .
  qed

  let ?H = "\obs. (\k\keys. \

(fst|OB) {(k, obs)} * log b (\

(fst|OB) {(k, obs)})) :: real"
let ?Ht = "\obs. (\k\keys. \

(fst|t\OB) {(k, obs)} * log b (\

(fst|t\OB) {(k, obs)})) :: real"

  have *: "?H obs = ?Ht (t obs)" if obs: "obs \ OB`msgs" for obs
  proof -
    have "?H obs = (\k\keys. \

(fst|t\OB) {(k, t obs)} * log b (\

(fst|t\OB) {(k, t obs)}))"
      using CP_T_eq_CP_O[OF _ obs]
      by simp
    then show ?thesis .
  qed

  have **: "\x f A. (\y\t-`{x}\A. f y (t y)) = (\y\t-`{x}\A. f y x)" by auto

  have P_t_sum_P_O: "\

(t\OB) {t (OB x)} = (\obs\?S (OB x). \

(OB) {obs})" for x
 proof -
 have *: "(\x. t (OB x)) -` {t (OB x)} \ msgs =
 (\<Union>obs\<in>?S (OB x). OB -` {obs} \<inter> msgs)" by auto
 have df: "disjoint_family_on (\obs. OB -` {obs} \ msgs) (?S (OB x))"
 unfolding disjoint_family_on_def by auto
 show ?thesis
 unfolding comp_def
 using finite_measure_finite_Union[OF _ _ df]
 by (force simp add: * intro!: sum_nonneg)
 qed

 txt \<open>Lemma 3\<close>
 have "\(fst | OB) = -(\obs\OB`msgs. \

(OB) {obs} * ?Ht (t obs))"
unfolding conditional_entropy_eq_ce_with_hypothesis using * by simp
also have "\ = -(\obs\t`OB`msgs. \

(t\OB) {obs} * ?Ht obs)"
    apply (subst SIGMA_image_vimage[symmetric, of "OB`msgs" t])
    apply (subst sum.reindex)
    apply (fastforce intro!: inj_onI)
    apply simp
    apply (subst sum.Sigma[symmetric, unfolded split_def])
    using finite_space apply fastforce
    using finite_space apply fastforce
    apply (safe intro!: sum.cong)
    using P_t_sum_P_O
    by (simp add: sum_divide_distrib[symmetric] field_simps **
                  sum_distrib_left[symmetric] sum_distrib_right[symmetric])
  also have "\ = \(fst | t\OB)"
    unfolding conditional_entropy_eq_ce_with_hypothesis
    by (simp add: comp_def image_image[symmetric])
  finally show ?thesis
    by (subst (1 2) mutual_information_eq_entropy_conditional_entropy) simp_all
qed

theorem "\(fst ; OB) \ real (card observations) * log b (real n + 1)"
proof -
  have "\(fst ; OB) = \(fst) - \(fst | t\OB)"
    unfolding ce_OB_eq_ce_t
    by (rule mutual_information_eq_entropy_conditional_entropy simple_function_finite)+
  also have "\ = \(t\OB) - \(t\OB | fst)"
    unfolding entropy_chain_rule[symmetric, OF simple_function_finite simple_function_finite] algebra_simps
    by (subst entropy_commute) simp
  also have "\ \ \(t\OB)"
    using conditional_entropy_nonneg[of "t\OB" fst] by simp
  also have "\ \ log b (real (card ((t\OB)`msgs)))"
    using entropy_le_card[of "t\OB", OF simple_distributedI[OF simple_function_finite _ refl]] by simp
  also have "\ \ log b (real (n + 1)^card observations)"
    using card_T_bound not_empty
    by (auto intro!: log_mono simp: card_gt_0_iff of_nat_power [symmetric] simp del: of_nat_power of_nat_Suc)
  also have "\ = real (card observations) * log b (real n + 1)"
    by (simp add: log_nat_power add.commute)
  finally show ?thesis  .
qed

end

end

quality99%

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.

Quelle Koepf_Duermuth_Countermeasure.thy Sprache: Isabelle

¤ Dauer der Verarbeitung: 0.17 Sekunden (vorverarbeitet) ¤

Haftungshinweis

Bemerkung: