--- a/src/HOL/IMP/Util.thy Thu Dec 01 14:29:14 2011 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,25 +0,0 @@
-(* Author: Tobias Nipkow *)
-
-theory Util imports Main
-begin
-
-subsection "Show sets of variables as lists"
-
-text {* Sets may be infinite and are not always displayed by element
- if computed as values. Lists do not have this problem.
-
- We define a function @{text show} that converts a set of
- variable names into a list. To keep things simple, we rely on
- the convention that we only use single letter names.
-*}
-definition
- letters :: "string list" where
- "letters = map (\<lambda>c. [c]) chars"
-
-definition
- "show" :: "string set \<Rightarrow> string list" where
- "show S = filter (\<lambda>x. x \<in> S) letters"
-
-value "show {''x'', ''z''}"
-
-end
--- a/src/HOL/IMP/Vars.thy Thu Dec 01 14:29:14 2011 +0100
+++ b/src/HOL/IMP/Vars.thy Thu Dec 01 20:54:48 2011 +0100
@@ -2,9 +2,28 @@
header "Definite Assignment Analysis"
-theory Vars imports Util BExp
+theory Vars imports BExp
begin
+subsection "Show sets of variables as lists"
+
+text {* Sets may be infinite and are not always displayed by element
+ if computed as values. Lists do not have this problem.
+
+ We define a function @{text show} that converts a set of
+ variable names into a list. To keep things simple, we rely on
+ the convention that we only use single letter names.
+*}
+definition
+ letters :: "string list" where
+ "letters = map (\<lambda>c. [c]) chars"
+
+definition
+ "show" :: "string set \<Rightarrow> string list" where
+ "show S = filter (\<lambda>x. x \<in> S) letters"
+
+value "show {''x'', ''z''}"
+
subsection "The Variables in an Expression"
text{* We need to collect the variables in both arithmetic and boolean
--- a/src/HOL/IsaMakefile Thu Dec 01 14:29:14 2011 +0100
+++ b/src/HOL/IsaMakefile Thu Dec 01 20:54:48 2011 +0100
@@ -530,7 +530,7 @@
IMP/Procs_Dyn_Vars_Dyn.thy IMP/Procs_Stat_Vars_Dyn.thy \
IMP/Procs_Stat_Vars_Stat.thy IMP/Sec_Type_Expr.thy IMP/Sec_Typing.thy \
IMP/Sec_TypingT.thy IMP/Small_Step.thy IMP/Star.thy IMP/Types.thy \
- IMP/Util.thy IMP/VC.thy IMP/Vars.thy \
+ IMP/VC.thy IMP/Vars.thy \
IMP/ROOT.ML IMP/document/root.tex IMP/document/root.bib
@cd IMP && $(ISABELLE_TOOL) usedir -g true -b $(OUT)/HOL HOL-IMP
--- a/src/HOL/List.thy Thu Dec 01 14:29:14 2011 +0100
+++ b/src/HOL/List.thy Thu Dec 01 20:54:48 2011 +0100
@@ -505,6 +505,8 @@
qed
qed
+lemma inj_split_Cons: "inj_on (\<lambda>(xs, n). n#xs) X"
+ by (auto intro!: inj_onI)
subsubsection {* @{const length} *}
@@ -3709,18 +3711,18 @@
thus ?case ..
qed
-lemma finite_lists_length_eq:
-assumes "finite A"
-shows "finite {xs. set xs \<subseteq> A \<and> length xs = n}" (is "finite (?S n)")
-proof(induct n)
- case 0 show ?case by simp
-next
- case (Suc n)
- have "?S (Suc n) = (\<Union>x\<in>A. (\<lambda>xs. x#xs) ` ?S n)"
- by (auto simp:length_Suc_conv)
- then show ?case using `finite A`
- by (auto intro: Suc) (* FIXME metis? *)
-qed
+lemma lists_length_Suc_eq:
+ "{xs. set xs \<subseteq> A \<and> length xs = Suc n} =
+ (\<lambda>(xs, n). n#xs) ` ({xs. set xs \<subseteq> A \<and> length xs = n} \<times> A)"
+ by (auto simp: length_Suc_conv)
+
+lemma
+ assumes "finite A"
+ shows finite_lists_length_eq: "finite {xs. set xs \<subseteq> A \<and> length xs = n}"
+ and card_lists_length_eq: "card {xs. set xs \<subseteq> A \<and> length xs = n} = (card A)^n"
+ using `finite A`
+ by (induct n)
+ (auto simp: card_image inj_split_Cons lists_length_Suc_eq cong: conj_cong)
lemma finite_lists_length_le:
assumes "finite A" shows "finite {xs. set xs \<subseteq> A \<and> length xs \<le> n}"
@@ -3730,6 +3732,18 @@
thus ?thesis by (auto intro: finite_lists_length_eq[OF `finite A`])
qed
+lemma card_lists_length_le:
+ assumes "finite A" shows "card {xs. set xs \<subseteq> A \<and> length xs \<le> n} = (\<Sum>i\<le>n. card A^i)"
+proof -
+ have "(\<Sum>i\<le>n. card A^i) = card (\<Union>i\<le>n. {xs. set xs \<subseteq> A \<and> length xs = i})"
+ using `finite A`
+ by (subst card_UN_disjoint)
+ (auto simp add: card_lists_length_eq finite_lists_length_eq)
+ also have "(\<Union>i\<le>n. {xs. set xs \<subseteq> A \<and> length xs = i}) = {xs. set xs \<subseteq> A \<and> length xs \<le> n}"
+ by auto
+ finally show ?thesis by simp
+qed
+
lemma infinite_UNIV_listI: "~ finite(UNIV::'a list set)"
apply(rule notI)
apply(drule finite_maxlen)
--- a/src/HOL/Probability/Information.thy Thu Dec 01 14:29:14 2011 +0100
+++ b/src/HOL/Probability/Information.thy Thu Dec 01 20:54:48 2011 +0100
@@ -1009,24 +1009,6 @@
by (simp add: setsum_cartesian_product' distribution_remove_const)
qed
-lemma (in prob_space) distribution_unit[simp]: "distribution (\<lambda>x. ()) {()} = 1"
- unfolding distribution_def using prob_space by auto
-
-lemma (in prob_space) joint_distribution_unit[simp]: "distribution (\<lambda>x. (X x, ())) {(a, ())} = distribution X {a}"
- unfolding distribution_def by (auto intro!: arg_cong[where f=\<mu>'])
-
-lemma (in prob_space) setsum_distribution:
- assumes X: "finite_random_variable MX X" shows "(\<Sum>a\<in>space MX. distribution X {a}) = 1"
- using setsum_joint_distribution[OF assms, of "\<lparr> space = UNIV, sets = Pow UNIV \<rparr>" "\<lambda>x. ()" "{()}"]
- using sigma_algebra_Pow[of "UNIV::unit set" "()"] by simp
-
-lemma (in prob_space) setsum_real_distribution:
- fixes MX :: "('c, 'd) measure_space_scheme"
- assumes X: "finite_random_variable MX X" shows "(\<Sum>a\<in>space MX. distribution X {a}) = 1"
- using setsum_joint_distribution[OF assms, of "\<lparr> space = UNIV, sets = Pow UNIV, measure = undefined \<rparr>" "\<lambda>x. ()" "{()}"]
- using sigma_algebra_Pow[of "UNIV::unit set" "\<lparr> measure = undefined \<rparr>"]
- by auto
-
lemma (in information_space) conditional_mutual_information_generic_positive:
assumes X: "finite_random_variable MX X" and Y: "finite_random_variable MY Y" and Z: "finite_random_variable MZ Z"
shows "0 \<le> conditional_mutual_information b MX MY MZ X Y Z"
@@ -1101,7 +1083,7 @@
setsum_joint_distribution_singleton[OF Y Z]
intro!: setsum_cong)
also have "log b (\<Sum>z\<in>space MZ. ?dZ {z}) = 0"
- unfolding setsum_real_distribution[OF Z] by simp
+ unfolding setsum_distribution[OF Z] by simp
finally show ?thesis by simp
qed
--- a/src/HOL/Probability/Probability.thy Thu Dec 01 14:29:14 2011 +0100
+++ b/src/HOL/Probability/Probability.thy Thu Dec 01 20:54:48 2011 +0100
@@ -6,7 +6,5 @@
Independent_Family
Conditional_Probability
Information
- "ex/Dining_Cryptographers"
- "ex/Koepf_Duermuth_Countermeasure"
begin
end
--- a/src/HOL/Probability/Probability_Measure.thy Thu Dec 01 14:29:14 2011 +0100
+++ b/src/HOL/Probability/Probability_Measure.thy Thu Dec 01 20:54:48 2011 +0100
@@ -70,6 +70,12 @@
"joint_distribution X X {(x, x)} = distribution X {x}"
unfolding distribution_def by (auto intro!: arg_cong[where f=\<mu>'])
+lemma (in prob_space) distribution_unit[simp]: "distribution (\<lambda>x. ()) {()} = 1"
+ unfolding distribution_def using prob_space by auto
+
+lemma (in prob_space) joint_distribution_unit[simp]: "distribution (\<lambda>x. (X x, ())) {(a, ())} = distribution X {a}"
+ unfolding distribution_def by (auto intro!: arg_cong[where f=\<mu>'])
+
lemma (in prob_space) not_empty: "space M \<noteq> {}"
using prob_space empty_measure' by auto
@@ -743,6 +749,11 @@
finite_random_variableD[OF Y(1)]
finite_random_variable_imp_sets[OF Y]] by simp
+lemma (in prob_space) setsum_distribution:
+ assumes X: "finite_random_variable MX X" shows "(\<Sum>a\<in>space MX. distribution X {a}) = 1"
+ using setsum_joint_distribution[OF assms, of "\<lparr> space = UNIV, sets = Pow UNIV \<rparr>" "\<lambda>x. ()" "{()}"]
+ using sigma_algebra_Pow[of "UNIV::unit set" "()"] by simp
+
locale pair_finite_prob_space = M1: finite_prob_space M1 + M2: finite_prob_space M2 for M1 M2
sublocale pair_finite_prob_space \<subseteq> pair_prob_space M1 M2 by default
@@ -962,7 +973,7 @@
(auto simp add: disjoint_family_on_def sets_eq_Pow inj_on_def
intro!: arg_cong[where f=prob])
-lemma (in finite_prob_space) setsum_distribution:
+lemma (in finite_prob_space) setsum_distribution_cut:
"(\<Sum>x \<in> X`space M. joint_distribution X Y {(x, y)}) = distribution Y {y}"
"(\<Sum>y \<in> Y`space M. joint_distribution X Y {(x, y)}) = distribution X {x}"
"(\<Sum>x \<in> X`space M. joint_distribution X (\<lambda>x. (Y x, Z x)) {(x, y, z)}) = joint_distribution Y Z {(y, z)}"
--- a/src/HOL/Probability/ROOT.ML Thu Dec 01 14:29:14 2011 +0100
+++ b/src/HOL/Probability/ROOT.ML Thu Dec 01 20:54:48 2011 +0100
@@ -1,1 +1,9 @@
-use_thys ["Probability"];
+no_document use_thys [
+ "~~/src/HOL/Library/Countable",
+ "~~/src/HOL/Multivariate_Analysis/Extended_Real_Limits",
+ "~~/src/HOL/Library/Permutation"];
+
+use_thys [
+ "Probability",
+ "ex/Dining_Cryptographers",
+ "ex/Koepf_Duermuth_Countermeasure" ];
--- a/src/HOL/Probability/ex/Dining_Cryptographers.thy Thu Dec 01 14:29:14 2011 +0100
+++ b/src/HOL/Probability/ex/Dining_Cryptographers.thy Thu Dec 01 20:54:48 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 14:29:14 2011 +0100
+++ b/src/HOL/Probability/ex/Koepf_Duermuth_Countermeasure.thy Thu Dec 01 20:54:48 2011 +0100
@@ -6,94 +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
-
-lemma (in prob_space)
- assumes "finite (X`space M)"
- shows "bij_betw (ordered_variable_partition X) {0..<card (X`space M)} (X`space M)"
- and "\<And>i j. \<lbrakk> i < card (X`space M) ; j < card (X`space M) ; i \<le> j \<rbrakk> \<Longrightarrow>
- distribution X {ordered_variable_partition X i} \<le> distribution X {ordered_variable_partition X j}"
- oops
-
-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}"
@@ -163,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"
@@ -222,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)))"
@@ -232,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)
@@ -241,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"
@@ -258,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
@@ -303,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
@@ -346,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)
@@ -359,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
@@ -389,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
@@ -430,7 +362,7 @@
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_distribution(2)[of "t\<circ>OB" fst "t obs", symmetric]
+ using setsum_distribution_cut(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'})"
@@ -439,7 +371,7 @@
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_distribution(2)[of OB fst obs, symmetric]
+ using setsum_distribution_cut(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)}"
by (subst joint_distribution_commute) (auto intro!: distribution_order(8))