--- a/src/HOL/Probability/ex/Dining_Cryptographers.thy Thu Dec 01 15:41:58 2011 +0100
+++ b/src/HOL/Probability/ex/Dining_Cryptographers.thy Thu Dec 01 15:41:58 2011 +0100
@@ -2,6 +2,12 @@
imports "~~/src/HOL/Probability/Information"
begin
+lemma image_ex1_eq: "inj_on f A \<Longrightarrow> (b \<in> f ` A) \<longleftrightarrow> (\<exists>!x \<in> A. b = f x)"
+ by (unfold inj_on_def) blast
+
+lemma Ex1_eq: "\<exists>! x. P x \<Longrightarrow> P x \<Longrightarrow> P y \<Longrightarrow> x = y"
+ by auto
+
locale finite_space =
fixes S :: "'a set"
assumes finite[simp]: "finite S"
@@ -28,45 +34,6 @@
lemma (in finite_space) \<mu>'_eq[simp]: "\<mu>' A = (if A \<subseteq> S then card A / card S else 0)"
unfolding \<mu>'_def by (auto simp: M_def)
-lemma set_of_list_extend:
- "{xs. length xs = Suc n \<and> (\<forall>x\<in>set xs. x \<in> A)} =
- (\<lambda>(xs, n). n#xs) ` ({xs. length xs = n \<and> (\<forall>x\<in>set xs. x \<in> A)} \<times> A)"
- (is "?lists (Suc n) = _")
-proof
- show "(\<lambda>(xs, n). n#xs) ` (?lists n \<times> A) \<subseteq> ?lists (Suc n)" by auto
- show "?lists (Suc n) \<subseteq> (\<lambda>(xs, n). n#xs) ` (?lists n \<times> A)"
- proof
- fix x assume "x \<in> ?lists (Suc n)"
- moreover
- hence "x \<noteq> []" by auto
- then obtain t h where "x = h # t" by (cases x) auto
- ultimately show "x \<in> (\<lambda>(xs, n). n#xs) ` (?lists n \<times> A)"
- by (auto intro!: image_eqI[where x="(t, h)"])
- qed
-qed
-
-lemma card_finite_list_length:
- assumes "finite A"
- shows "(card {xs. length xs = n \<and> (\<forall>x\<in>set xs. x \<in> A)} = (card A)^n) \<and>
- finite {xs. length xs = n \<and> (\<forall>x\<in>set xs. x \<in> A)}"
- (is "card (?lists n) = _ \<and> _")
-proof (induct n)
- case 0 have "{xs. length xs = 0 \<and> (\<forall>x\<in>set xs. x \<in> A)} = {[]}" by auto
- thus ?case by simp
-next
- case (Suc n)
- moreover note set_of_list_extend[of n A]
- moreover have "inj_on (\<lambda>(xs, n). n#xs) (?lists n \<times> A)"
- by (auto intro!: inj_onI)
- ultimately show ?case using assms by (auto simp: card_image)
-qed
-
-lemma
- assumes "finite A"
- shows finite_lists: "finite {xs. length xs = n \<and> (\<forall>x\<in>set xs. x \<in> A)}"
- and card_list_length: "card {xs. length xs = n \<and> (\<forall>x\<in>set xs. x \<in> A)} = (card A)^n"
- using card_finite_list_length[OF assms, of n] by auto
-
section "Define the state space"
text {*
@@ -171,12 +138,6 @@
unfolding payer_def_raw dc_crypto fst_image_times if_not_P[OF *] ..
qed
-lemma image_ex1_eq: "inj_on f A \<Longrightarrow> (b \<in> f ` A) \<longleftrightarrow> (\<exists>!x \<in> A. b = f x)"
- by (unfold inj_on_def) blast
-
-lemma Ex1_eq: "\<exists>! x. P x \<Longrightarrow> P x \<Longrightarrow> P y \<Longrightarrow> x = y"
- by auto
-
lemma card_payer_and_inversion:
assumes "xs \<in> inversion ` dc_crypto" and "i < n"
shows "card {dc \<in> dc_crypto. payer dc = Some i \<and> inversion dc = xs} = 2"
@@ -341,7 +302,7 @@
qed
lemma finite_dc_crypto: "finite dc_crypto"
- using finite_lists[where A="UNIV :: bool set"]
+ using finite_lists_length_eq[where A="UNIV :: bool set"]
unfolding dc_crypto by simp
lemma card_inversion:
@@ -401,7 +362,7 @@
lemma card_dc_crypto:
"card dc_crypto = n * 2^n"
unfolding dc_crypto
- using card_list_length[of "UNIV :: bool set"]
+ using card_lists_length_eq[of "UNIV :: bool set"]
by (simp add: card_cartesian_product card_image)
lemma card_image_inversion:
@@ -512,7 +473,7 @@
from z have "payer -` {z} \<inter> dc_crypto = {z} \<times> {xs. length xs = n}"
by (auto simp: dc_crypto payer_def)
hence "card (payer -` {z} \<inter> dc_crypto) = 2^n"
- using card_list_length[where A="UNIV::bool set"]
+ using card_lists_length_eq[where A="UNIV::bool set"]
by (simp add: card_cartesian_product_singleton)
hence "?dP {z} = 1 / real n"
by (simp add: distribution_def card_dc_crypto)
--- a/src/HOL/Probability/ex/Koepf_Duermuth_Countermeasure.thy Thu Dec 01 15:41:58 2011 +0100
+++ b/src/HOL/Probability/ex/Koepf_Duermuth_Countermeasure.thy Thu Dec 01 15:41:58 2011 +0100
@@ -6,87 +6,11 @@
imports "~~/src/HOL/Probability/Information" "~~/src/HOL/Library/Permutation"
begin
-lemma
- fixes p u :: "'a \<Rightarrow> real"
- assumes "1 < b"
- assumes sum: "(\<Sum>i\<in>S. p i) = (\<Sum>i\<in>S. u i)"
- and pos: "\<And>i. i \<in> S \<Longrightarrow> 0 \<le> p i" "\<And>i. i \<in> S \<Longrightarrow> 0 \<le> u i"
- and cont: "\<And>i. i \<in> S \<Longrightarrow> 0 < p i \<Longrightarrow> 0 < u i"
- shows "(\<Sum>i\<in>S. p i * log b (u i)) \<le> (\<Sum>i\<in>S. p i * log b (p i))"
-proof -
- have "(\<Sum>i\<in>S. p i * ln (u i) - p i * ln (p i)) \<le> (\<Sum>i\<in>S. u i - p i)"
- proof (intro setsum_mono)
- fix i assume [intro, simp]: "i \<in> S"
- show "p i * ln (u i) - p i * ln (p i) \<le> u i - p i"
- proof cases
- assume "p i = 0" with pos[of i] show ?thesis by simp
- next
- assume "p i \<noteq> 0"
- then have "0 < p i" "0 < u i" using pos[of i] cont[of i] by auto
- then have *: "0 < u i / p i" by (blast intro: divide_pos_pos cont)
- from `0 < p i` `0 < u i`
- have "p i * ln (u i) - p i * ln (p i) = p i * ln (u i / p i)"
- by (simp add: ln_div field_simps)
- also have "\<dots> \<le> p i * (u i / p i - 1)"
- using exp_ge_add_one_self[of "ln (u i / p i)"] pos[of i] exp_ln[OF *]
- by (auto intro!: mult_left_mono)
- also have "\<dots> = u i - p i"
- using `p i \<noteq> 0` by (simp add: field_simps)
- finally show ?thesis by simp
- qed
- qed
- also have "\<dots> = 0" using sum by (simp add: setsum_subtractf)
- finally show ?thesis using `1 < b` unfolding log_def setsum_subtractf
- by (auto intro!: divide_right_mono
- simp: times_divide_eq_right setsum_divide_distrib[symmetric])
-qed
-
-definition (in prob_space)
- "ordered_variable_partition X = (SOME f. bij_betw f {0..<card (X`space M)} (X`space M) \<and>
- (\<forall>i<card (X`space M). \<forall>j<card (X`space M). i \<le> j \<longrightarrow> distribution X {f i} \<le> distribution X {f j}))"
+lemma SIGMA_image_vimage:
+ "snd ` (SIGMA x:f`X. f -` {x} \<inter> X) = X"
+ by (auto simp: image_iff)
-lemma ex_ordered_bij_betw_nat_finite:
- fixes order :: "nat \<Rightarrow> 'a\<Colon>linorder"
- assumes "finite S"
- shows "\<exists>f. bij_betw f {0..<card S} S \<and> (\<forall>i<card S. \<forall>j<card S. i \<le> j \<longrightarrow> order (f i) \<le> order (f j))"
-proof -
- from ex_bij_betw_nat_finite [OF `finite S`] guess f .. note f = this
- let ?xs = "sort_key order (map f [0 ..< card S])"
-
- have "?xs <~~> map f [0 ..< card S]"
- unfolding multiset_of_eq_perm[symmetric] by (rule multiset_of_sort)
- from permutation_Ex_bij [OF this]
- obtain g where g: "bij_betw g {0..<card S} {0..<card S}" and
- map: "\<And>i. i<card S \<Longrightarrow> ?xs ! i = map f [0 ..< card S] ! g i"
- by (auto simp: atLeast0LessThan)
-
- { fix i assume "i < card S"
- then have "g i < card S" using g by (auto simp: bij_betw_def)
- with map [OF `i < card S`] have "f (g i) = ?xs ! i" by simp }
- note this[simp]
-
- show ?thesis
- proof (intro exI allI conjI impI)
- show "bij_betw (f\<circ>g) {0..<card S} S"
- using g f by (rule bij_betw_trans)
- fix i j assume [simp]: "i < card S" "j < card S" "i \<le> j"
- from sorted_nth_mono[of "map order ?xs" i j]
- show "order ((f\<circ>g) i) \<le> order ((f\<circ>g) j)" by simp
- qed
-qed
-
-definition (in prob_space)
- "order_distribution X i = real (distribution X {ordered_variable_partition X i})"
-
-definition (in prob_space)
- "guessing_entropy b X = (\<Sum>i<card(X`space M). real i * log b (order_distribution X i))"
-
-abbreviation (in information_space)
- finite_guessing_entropy ("\<G>'(_')") where
- "\<G>(X) \<equiv> guessing_entropy b X"
-
-lemma zero_notin_Suc_image[simp]: "0 \<notin> Suc ` A"
- by auto
+declare inj_split_Cons[simp]
definition extensionalD :: "'b \<Rightarrow> 'a set \<Rightarrow> ('a \<Rightarrow> 'b) set" where
"extensionalD d A = {f. \<forall>x. x \<notin> A \<longrightarrow> f x = d}"
@@ -156,32 +80,73 @@
qed
qed simp
-lemma set_of_list_extend:
- "{xs. length xs = Suc n \<and> (\<forall>x\<in>set xs. x \<in> A)} =
- (\<lambda>(xs, n). n#xs) ` ({xs. length xs = n \<and> (\<forall>x\<in>set xs. x \<in> A)} \<times> A)"
- by (auto simp: length_Suc_conv)
+lemma zero_notin_Suc_image[simp]: "0 \<notin> Suc ` A"
+ by auto
-lemma
- assumes "finite A"
- shows finite_lists:
- "finite {xs. length xs = n \<and> (\<forall>x\<in>set xs. x \<in> A)}" (is "finite (?lists n)")
- and card_list_length:
- "card {xs. length xs = n \<and> (\<forall>x\<in>set xs. x \<in> A)} = (card A)^n"
+lemma setprod_setsum_distrib_lists:
+ fixes P and S :: "'a set" and f :: "'a \<Rightarrow> _::semiring_0" assumes "finite S"
+ shows "(\<Sum>ms\<in>{ms. set ms \<subseteq> S \<and> length ms = n \<and> (\<forall>i<n. P i (ms!i))}. \<Prod>x<n. f (ms ! x)) =
+ (\<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 \<subseteq> S \<and> length ms = Suc n \<and> (\<forall>i<Suc n. P i (ms ! 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 "\<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])
+qed
+
+lemma ex_ordered_bij_betw_nat_finite:
+ fixes order :: "nat \<Rightarrow> 'a\<Colon>linorder"
+ assumes "finite S"
+ shows "\<exists>f. bij_betw f {0..<card S} S \<and> (\<forall>i<card S. \<forall>j<card S. i \<le> j \<longrightarrow> order (f i) \<le> order (f j))"
proof -
- from `finite A`
- have "(card {xs. length xs = n \<and> (\<forall>x\<in>set xs. x \<in> A)} = (card A)^n) \<and>
- finite {xs. length xs = n \<and> (\<forall>x\<in>set xs. x \<in> A)}"
- proof (induct n)
- case (Suc n)
- moreover note set_of_list_extend[of n A]
- moreover have "inj_on (\<lambda>(xs, n). n#xs) (?lists n \<times> A)"
- by (auto intro!: inj_onI)
- ultimately show ?case using assms by (auto simp: card_image)
- qed (simp cong: conj_cong)
- then show "finite (?lists n)" "card (?lists n) = card A ^ n"
- by auto
+ from ex_bij_betw_nat_finite [OF `finite S`] guess f .. note f = this
+ let ?xs = "sort_key order (map f [0 ..< card S])"
+
+ have "?xs <~~> map f [0 ..< card S]"
+ unfolding multiset_of_eq_perm[symmetric] by (rule multiset_of_sort)
+ from permutation_Ex_bij [OF this]
+ obtain g where g: "bij_betw g {0..<card S} {0..<card S}" and
+ map: "\<And>i. i<card S \<Longrightarrow> ?xs ! i = map f [0 ..< card S] ! g i"
+ by (auto simp: atLeast0LessThan)
+
+ { fix i assume "i < card S"
+ then have "g i < card S" using g by (auto simp: bij_betw_def)
+ with map [OF `i < card S`] have "f (g i) = ?xs ! i" by simp }
+ note this[simp]
+
+ show ?thesis
+ proof (intro exI allI conjI impI)
+ show "bij_betw (f\<circ>g) {0..<card S} S"
+ using g f by (rule bij_betw_trans)
+ fix i j assume [simp]: "i < card S" "j < card S" "i \<le> j"
+ from sorted_nth_mono[of "map order ?xs" i j]
+ show "order ((f\<circ>g) i) \<le> order ((f\<circ>g) j)" by simp
+ qed
qed
+definition (in prob_space)
+ "ordered_variable_partition X = (SOME f. bij_betw f {0..<card (X`space M)} (X`space M) \<and>
+ (\<forall>i<card (X`space M). \<forall>j<card (X`space M). i \<le> j \<longrightarrow> distribution X {f i} \<le> distribution X {f j}))"
+
+definition (in prob_space)
+ "order_distribution X i = real (distribution X {ordered_variable_partition X i})"
+
+definition (in prob_space)
+ "guessing_entropy b X = (\<Sum>i<card(X`space M). real i * log b (order_distribution X i))"
+
+abbreviation (in information_space)
+ finite_guessing_entropy ("\<G>'(_')") where
+ "\<G>(X) \<equiv> guessing_entropy b X"
+
locale finite_information =
fixes \<Omega> :: "'a set"
and p :: "'a \<Rightarrow> real"
@@ -215,7 +180,7 @@
begin
definition msgs :: "('key \<times> 'message list) set" where
- "msgs = keys \<times> {ms. length ms = n \<and> (\<forall>M\<in>set ms. M \<in> messages)}"
+ "msgs = keys \<times> {ms. set ms \<subseteq> messages \<and> length ms = n}"
definition P :: "('key \<times> 'message list) \<Rightarrow> real" where
"P = (\<lambda>(k, ms). K k * (\<Prod>i<length ms. M (ms ! i)))"
@@ -225,7 +190,7 @@
sublocale koepf_duermuth \<subseteq> finite_information msgs P b
proof default
show "finite msgs" unfolding msgs_def
- using finite_lists[OF M.finite_space, of n]
+ using finite_lists_length_eq[OF M.finite_space, of n]
by auto
have [simp]: "\<And>A. inj_on (\<lambda>(xs, n). n # xs) A" by (force intro!: inj_onI)
@@ -234,13 +199,13 @@
note setsum_left_distrib[symmetric, simp]
note setsum_cartesian_product'[simp]
- have "(\<Sum>ms | length ms = n \<and> (\<forall>M\<in>set ms. M \<in> messages). \<Prod>x<length ms. M (ms ! x)) = 1"
+ have "(\<Sum>ms | set ms \<subseteq> messages \<and> length ms = n. \<Prod>x<length ms. M (ms ! x)) = 1"
proof (induct n)
case 0 then show ?case by (simp cong: conj_cong)
next
case (Suc n)
then show ?case
- by (simp add: comp_def set_of_list_extend lessThan_Suc_eq_insert_0
+ by (simp add: lists_length_Suc_eq lessThan_Suc_eq_insert_0
setsum_reindex setprod_reindex)
qed
then show "setsum P msgs = 1"
@@ -251,32 +216,6 @@
unfolding P_def by (auto split: prod.split simp: zero_le_mult_iff)
qed auto
-lemma SIGMA_image_vimage:
- "snd ` (SIGMA x:f`X. f -` {x} \<inter> X) = X"
- by (auto simp: image_iff)
-
-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"
- shows "(\<Sum>ms\<in>{ms. length ms = n \<and> set ms \<subseteq> S \<and> (\<forall>i<n. P i (ms!i))}. \<Prod>x<n. f (ms ! x)) =
- (\<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. length ms = Suc n \<and> set ms \<subseteq> S \<and> (\<forall>i<Suc n. P i (ms ! i))} =
- (\<lambda>(xs, x). x#xs) ` ({ms. length ms = n \<and> set ms \<subseteq> S \<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 "\<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])
-qed
-
context koepf_duermuth
begin
@@ -296,7 +235,7 @@
proof -
have "(t\<circ>OB)`msgs \<subseteq> extensionalD 0 observations \<inter> (observations \<rightarrow> {.. n})"
unfolding observations_def extensionalD_def OB_def msgs_def
- by (auto simp add: t_def comp_def image_iff)
+ by (auto simp add: t_def comp_def image_iff subset_eq)
with finite_extensionalD_funcset
have "card ((t\<circ>OB)`msgs) \<le> card (extensionalD 0 observations \<inter> (observations \<rightarrow> {.. n}))"
by (rule card_mono) auto
@@ -339,7 +278,7 @@
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)}"
+ "fst -` {k} \<inter> msgs = {k}\<times>{ms. set ms \<subseteq> messages \<and> length ms = n}"
unfolding msgs_def by auto
show "\<P>(fst) {k} = K k"
apply (simp add: \<mu>'_eq distribution_def)
@@ -352,7 +291,7 @@
lemma fst_image_msgs[simp]: "fst`msgs = keys"
proof -
from M.not_empty obtain m where "m \<in> messages" by auto
- then have *: "{m. length m = n \<and> (\<forall>x\<in>set m. x\<in>messages)} \<noteq> {}"
+ then have *: "{m. set m \<subseteq> messages \<and> length m = n} \<noteq> {}"
by (auto intro!: exI[of _ "replicate n m"])
then show ?thesis
unfolding msgs_def fst_image_times if_not_P[OF *] by simp
@@ -382,7 +321,7 @@
(\<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]) ..
+ apply (subst setprod_setsum_distrib_lists[OF M.finite_space]) ..
finally have "\<P>(OB, fst) {(obs, k)} / K k =
(\<Prod>i<n. \<Sum>m\<in>{m\<in>messages. observe k m = obs ! i}. M m)" . }
note * = this