--- a/src/HOL/Probability/ex/Dining_Cryptographers.thy Wed Oct 16 22:07:04 2024 +0200
+++ b/src/HOL/Probability/ex/Dining_Cryptographers.thy Wed Oct 16 23:13:02 2024 +0200
@@ -124,32 +124,31 @@
hence "length ys = n" by (simp add: dc_crypto)
have [simp]: "length xs = n" using xs_inv[symmetric] by (simp add: inversion_def)
- { fix b
- have "inj_on (\<lambda>x. inversion (Some i, x)) {ys. ys ! 0 = b \<and> length ys = length xs}"
- proof (rule inj_onI)
- fix x y
- assume "x \<in> {ys. ys ! 0 = b \<and> length ys = length xs}"
- and "y \<in> {ys. ys ! 0 = b \<and> length ys = length xs}"
- and inv: "inversion (Some i, x) = inversion (Some i, y)"
- hence [simp]: "x ! 0 = y ! 0" "length y = n" "length x = n"
- using \<open>length xs = n\<close> by simp_all
- have *: "\<And>j. j < n \<Longrightarrow>
- (x ! j = x ! (Suc j mod n)) = (y ! j = y ! (Suc j mod n))"
- using inv unfolding inversion_def map_eq_conv payer_def coin_def
- by fastforce
- show "x = y"
- proof (rule nth_equalityI, simp)
- fix j assume "j < length x" hence "j < n" using \<open>length xs = n\<close> by simp
- thus "x ! j = y ! j"
- proof (induct j)
- case (Suc j)
- hence "j < n" by simp
- with Suc show ?case using *[OF \<open>j < n\<close>]
- by (cases "y ! j") simp_all
- qed simp
- qed
- qed }
- note inj_inv = this
+ have inj_inv: "inj_on (\<lambda>x. inversion (Some i, x)) {ys. ys ! 0 = b \<and> length ys = length xs}"
+ for b
+ proof (rule inj_onI)
+ fix x y
+ assume "x \<in> {ys. ys ! 0 = b \<and> length ys = length xs}"
+ and "y \<in> {ys. ys ! 0 = b \<and> length ys = length xs}"
+ and inv: "inversion (Some i, x) = inversion (Some i, y)"
+ hence [simp]: "x ! 0 = y ! 0" "length y = n" "length x = n"
+ using \<open>length xs = n\<close> by simp_all
+ have *: "\<And>j. j < n \<Longrightarrow>
+ (x ! j = x ! (Suc j mod n)) = (y ! j = y ! (Suc j mod n))"
+ using inv unfolding inversion_def map_eq_conv payer_def coin_def
+ by fastforce
+ show "x = y"
+ proof (rule nth_equalityI, simp)
+ fix j assume "j < length x" hence "j < n" using \<open>length xs = n\<close> by simp
+ thus "x ! j = y ! j"
+ proof (induct j)
+ case (Suc j)
+ hence "j < n" by simp
+ with Suc show ?case using *[OF \<open>j < n\<close>]
+ by (cases "y ! j") simp_all
+ qed simp
+ qed
+ qed
txt \<open>
We now construct the possible inversions for \<^term>\<open>xs\<close> when the payer is
@@ -162,16 +161,20 @@
have "\<And>l. l < max i j \<Longrightarrow> Suc l mod n = Suc l"
using \<open>i < n\<close> \<open>j < n\<close> by auto
- { fix l assume "l < n"
- hence "(((l < min i j \<or> l = min i j) \<or> (min i j < l \<and> l < max i j)) \<or> l = max i j) \<or> max i j < l" by auto
- hence "((i = l) = (zs ! l = zs ! (Suc l mod n))) = ((j = l) = (ys ! l = ys ! (Suc l mod n)))"
- apply - proof ((erule disjE)+)
- assume "l < min i j"
+ have "((i = l) = (zs ! l = zs ! (Suc l mod n))) = ((j = l) = (ys ! l = ys ! (Suc l mod n)))"
+ if "l < n" for l
+ proof -
+ from that consider "l < min i j" | "l = min i j" | "min i j < l" "l < max i j"
+ | "l = max i j" | "max i j < l"
+ by linarith
+ thus ?thesis
+ proof cases
+ case 1
hence "l \<noteq> i" and "l \<noteq> j" and "zs ! l = ys ! l" and
"zs ! (Suc l mod n) = ys ! (Suc l mod n)" using \<open>i < n\<close> \<open>j < n\<close> unfolding zs_def by auto
thus ?thesis by simp
next
- assume "l = min i j"
+ case 2
show ?thesis
proof (cases rule: linorder_cases)
assume "i < j"
@@ -192,13 +195,13 @@
thus ?thesis by simp
qed
next
- assume "min i j < l \<and> l < max i j"
+ case 3
hence "i \<noteq> l" and "j \<noteq> l" and "zs ! l = (\<not> ys ! l)"
"zs ! (Suc l mod n) = (\<not> ys ! (Suc l mod n))"
using \<open>i < n\<close> \<open>j < n\<close> by (auto simp: zs_def)
thus ?thesis by simp
next
- assume "l = max i j"
+ case 4
show ?thesis
proof (cases rule: linorder_cases)
assume "i < j"
@@ -223,14 +226,15 @@
thus ?thesis by simp
qed
next
- assume "max i j < l"
+ case 5
hence "j \<noteq> l" and "i \<noteq> l" by simp_all
have "zs ! (Suc l mod n) = ys ! (Suc l mod n)"
using \<open>l < n\<close> \<open>max i j < l\<close> by (cases "Suc l = n") (auto simp add: zs_def)
moreover have "zs ! l = ys ! l"
using \<open>l < n\<close> \<open>max i j < l\<close> by (auto simp add: zs_def)
ultimately show ?thesis using \<open>j \<noteq> l\<close> \<open>i \<noteq> l\<close> by auto
- qed }
+ qed
+ qed
hence zs: "inversion (Some i, zs) = xs"
by (simp add: xs_inv[symmetric] inversion_def coin_def payer_def)
moreover
@@ -297,15 +301,12 @@
have card_double: "2 * card ?sets = card (\<Union>?sets)"
proof (rule card_partition)
show "finite ?sets" by simp
- { fix i assume "i < n"
- have "?set i \<subseteq> dc_crypto" by auto
- have "finite (?set i)" using finite_dc_crypto by auto }
+ have "finite (?set i)" for i
+ using finite_dc_crypto by auto
thus "finite (\<Union>?sets)" by auto
-
next
fix c assume "c \<in> ?sets"
thus "card c = 2" using card_payer_and_inversion[OF assms] by auto
-
next
fix x y assume "x \<in> ?sets" and "y \<in> ?sets" "x \<noteq> y"
then obtain i j where xy: "x = ?set i" "y = ?set j" by auto
@@ -315,17 +316,20 @@
have sets: "?sets = ?set ` {..< n}"
unfolding image_def by auto
- { fix i j :: nat assume asm: "i \<noteq> j" "i < n" "j < n"
- { assume iasm: "?set i = {}"
+ have "?set i \<noteq> ?set j" if asm: "i \<noteq> j" "i < n" "j < n" for i j
+ proof -
+ have False if iasm: "?set i = {}"
+ proof -
have "card (?set i) = 2"
using card_payer_and_inversion[OF assms \<open>i < n\<close>] by auto
- hence "False"
- using iasm by auto }
+ thus ?thesis using iasm by auto
+ qed
then obtain c where ci: "c \<in> ?set i" by blast
hence cj: "c \<notin> ?set j" using asm by auto
- { assume "?set i = ?set j"
- hence "False" using ci cj by auto }
- hence "?set i \<noteq> ?set j" by auto }
+ have False if "?set i = ?set j"
+ using that ci cj by auto
+ thus ?thesis by auto
+ qed
hence "inj_on ?set {..< n}" unfolding inj_on_def by auto
from card_image[OF this]
have "card (?set ` {..< n}) = n" by auto
@@ -345,16 +349,13 @@
let ?P = "{inversion -` {x} \<inter> dc_crypto |x. x \<in> inversion ` dc_crypto}"
have "\<Union>?P = dc_crypto" by auto
- { fix a b assume *: "(a, b) \<in> dc_crypto"
- have inv_SOME: "inversion (SOME x. inversion x = inversion (a, b) \<and> x \<in> dc_crypto) = inversion (a, b)"
- apply (rule someI2)
- by (auto simp: *) }
- note inv_SOME = this
+ have inv_SOME: "inversion (SOME x. inversion x = inversion (a, b) \<and> x \<in> dc_crypto) = inversion (a, b)"
+ if "(a, b) \<in> dc_crypto" for a b
+ by (rule someI2) (auto simp: that)
- { fix a b assume *: "(a, b) \<in> dc_crypto"
- have "(SOME x. inversion x = inversion (a, b) \<and> x \<in> dc_crypto) \<in> dc_crypto"
- by (rule someI2) (auto simp: *) }
- note SOME_inv_dc = this
+ have SOME_inv_dc: "(SOME x. inversion x = inversion (a, b) \<and> x \<in> dc_crypto) \<in> dc_crypto"
+ if "(a, b) \<in> dc_crypto" for a b
+ by (rule someI2) (auto simp: that)
have "bij_betw (\<lambda>s. inversion (SOME x. x \<in> s \<and> x \<in> dc_crypto))
{inversion -` {x} \<inter> dc_crypto |x. x \<in> inversion ` dc_crypto}
@@ -373,13 +374,11 @@
have "?P = (\<lambda>x. inversion -` {x} \<inter> dc_crypto) ` (inversion ` dc_crypto)"
by auto
thus "finite ?P" using finite_dc_crypto by auto
-
next
fix c assume "c \<in> {inversion -` {x} \<inter> dc_crypto |x. x \<in> inversion ` dc_crypto}"
then obtain x where "c = inversion -` {x} \<inter> dc_crypto" and x: "x \<in> inversion ` dc_crypto" by auto
hence "c = {dc \<in> dc_crypto. inversion dc = x}" by auto
thus "card c = 2 * n" using card_inversion[OF x] by simp
-
next
fix x y assume "x \<in> ?P" "y \<in> ?P" and "x \<noteq> y"
then obtain i j where
--- a/src/HOL/Probability/ex/Koepf_Duermuth_Countermeasure.thy Wed Oct 16 22:07:04 2024 +0200
+++ b/src/HOL/Probability/ex/Koepf_Duermuth_Countermeasure.thy Wed Oct 16 23:13:02 2024 +0200
@@ -69,12 +69,12 @@
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
- { fix f assume "f \<in> extensionalD d A \<inter> (A \<rightarrow> B)"
- have "card (fun_upd f a ` B) = card B"
- 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 }
+ have "card (fun_upd f a ` B) = card B"
+ if "f \<in> extensionalD d A \<inter> (A \<rightarrow> 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 "(\<Sum>i\<in>extensionalD d A \<inter> (A \<rightarrow> B). card (fun_upd i a ` B)) = card B * card B ^ card A"
using insert by simp
qed
@@ -170,9 +170,9 @@
qed
then show "sum P msgs = 1"
unfolding msgs_def P_def by simp
- fix x
- have "\<And> A f. 0 \<le> (\<Prod>x\<in>A. M (f x))" by (auto simp: prod_nonneg)
- then show "0 \<le> P x"
+ have "0 \<le> (\<Prod>x\<in>A. M (f x))" for A f
+ by (auto simp: prod_nonneg)
+ then show "0 \<le> P x" for x
unfolding P_def by (auto split: prod.split simp: zero_le_mult_iff)
qed auto
@@ -333,40 +333,45 @@
proof -
txt \<open>Lemma 2\<close>
- { fix k obs obs'
- assume "k \<in> keys" "K k \<noteq> 0" and obs': "obs' \<in> OB ` msgs" and obs: "obs \<in> OB ` msgs"
- assume "t obs = t obs'"
- from t_eq_imp_bij_func[OF this]
+ have t_eq_imp: "(\<P>(OB ; fst) {(obs, k)}) = (\<P>(OB ; fst) {(obs', k)})"
+ if "k \<in> keys" "K k \<noteq> 0" and obs': "obs' \<in> OB ` msgs" and obs: "obs \<in> 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 {..<n} {..<n}" and
obs_t_f: "\<And>i. i<n \<Longrightarrow> obs!i = obs' ! t_f i"
using obs obs' unfolding OB_def msgs_def by auto
then have t_f: "inj_on t_f {..<n}" "{..<n} = t_f`{..<n}" unfolding bij_betw_def by auto
- { fix obs assume "obs \<in> OB`msgs"
- then have **: "\<And>ms. length ms = n \<Longrightarrow> OB (k, ms) = obs \<longleftrightarrow> (\<forall>i<n. observe k (ms!i) = obs ! i)"
+ have *: "(\<P>(OB ; fst) {(obs, k)}) / K k =
+ (\<Prod>i<n. \<Sum>m\<in>{m\<in>messages. observe k m = obs ! i}. M m)"
+ if "obs \<in> OB`msgs" for obs
+ proof -
+ from that have **: "length ms = n \<Longrightarrow> OB (k, ms) = obs \<longleftrightarrow> (\<forall>i<n. observe k (ms!i) = obs ! i)"
+ for ms
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"
- apply (simp add: \<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)"
+ by (simp add: \<mu>'_eq) (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 \<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 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
+ finally show ?thesis .
+ qed
have "(\<P>(OB ; fst) {(obs, k)}) / K k = (\<P>(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 have "(\<P>(OB ; fst) {(obs, k)}) = (\<P>(OB ; fst) {(obs', k)})"
- using \<open>K k \<noteq> 0\<close> by auto }
- note t_eq_imp = this
+ then show ?thesis using \<open>K k \<noteq> 0\<close> by auto
+ qed
let ?S = "\<lambda>obs. t -`{t obs} \<inter> OB`msgs"
- { fix k obs assume "k \<in> keys" "K k \<noteq> 0" and obs: "obs \<in> OB`msgs"
+ have P_t_eq_P_OB: "\<P>(t\<circ>OB ; fst) {(t obs, k)} = real (card (?S obs)) * \<P>(OB ; fst) {(obs, k)}"
+ if "k \<in> keys" "K k \<noteq> 0" and obs: "obs \<in> OB`msgs"
+ for k obs
+ proof -
have *: "((\<lambda>x. (t (OB x), fst x)) -` {(t obs, k)} \<inter> msgs) =
(\<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)"
@@ -377,17 +382,18 @@
by (auto simp add: * intro!: sum_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])
- 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
+ finally show ?thesis .
+ qed
- { fix k obs assume "k \<in> keys" and obs: "obs \<in> OB`msgs"
- have "\<P>(t\<circ>OB | fst) {(t obs, k)} =
- real (card (t -` {t obs} \<inter> OB ` msgs)) * \<P>(OB | fst) {(obs, k)}"
- using \<P>_k[OF \<open>k \<in> keys\<close>] P_t_eq_P_OB[OF \<open>k \<in> keys\<close> _ obs] by auto }
- note CP_t_K = this
+ have CP_t_K: "\<P>(t\<circ>OB | fst) {(t obs, k)} =
+ real (card (t -` {t obs} \<inter> OB ` msgs)) * \<P>(OB | fst) {(obs, k)}"
+ if k: "k \<in> keys" and obs: "obs \<in> OB`msgs" for k obs
+ using \<P>_k[OF k] P_t_eq_P_OB[OF k _ obs] by auto
- { 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
+ have CP_T_eq_CP_O: "\<P>(fst | t\<circ>OB) {(k, t obs)} = \<P>(fst | OB) {(k, obs)}"
+ if "k \<in> keys" and obs: "obs \<in> OB`msgs" for k obs
+ proof -
+ from that 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}"
@@ -411,31 +417,33 @@
by (auto intro!: sum.cong simp: prob_conj_imp1 vimage_def)
also have "\<P>(OB | fst) {(obs, k)} * \<P>(fst) {k} / \<P>(OB) {obs} = \<P>(fst | OB) {(k, obs)}"
by (auto simp: vimage_def conj_commute prob_conj_imp2)
- finally have "\<P>(fst | t\<circ>OB) {(k, t obs)} = \<P>(fst | OB) {(k, obs)}" . }
- note CP_T_eq_CP_O = this
+ finally show ?thesis .
+ qed
let ?H = "\<lambda>obs. (\<Sum>k\<in>keys. \<P>(fst|OB) {(k, obs)} * log b (\<P>(fst|OB) {(k, obs)})) :: real"
let ?Ht = "\<lambda>obs. (\<Sum>k\<in>keys. \<P>(fst|t\<circ>OB) {(k, obs)} * log b (\<P>(fst|t\<circ>OB) {(k, obs)})) :: real"
- { fix obs assume obs: "obs \<in> OB`msgs"
+ have *: "?H obs = ?Ht (t obs)" if obs: "obs \<in> OB`msgs" for obs
+ proof -
have "?H obs = (\<Sum>k\<in>keys. \<P>(fst|t\<circ>OB) {(k, t obs)} * log b (\<P>(fst|t\<circ>OB) {(k, t obs)}))"
using CP_T_eq_CP_O[OF _ obs]
by simp
- then have "?H obs = ?Ht (t obs)" . }
- note * = this
+ then show ?thesis .
+ qed
have **: "\<And>x f A. (\<Sum>y\<in>t-`{x}\<inter>A. f y (t y)) = (\<Sum>y\<in>t-`{x}\<inter>A. f y x)" by auto
- { fix x
+ have P_t_sum_P_O: "\<P>(t\<circ>OB) {t (OB x)} = (\<Sum>obs\<in>?S (OB x). \<P>(OB) {obs})" for x
+ proof -
have *: "(\<lambda>x. t (OB x)) -` {t (OB x)} \<inter> msgs =
(\<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})"
+ show ?thesis
unfolding comp_def
using finite_measure_finite_Union[OF _ _ df]
- by (force simp add: * intro!: sum_nonneg) }
- note P_t_sum_P_O = this
+ by (force simp add: * intro!: sum_nonneg)
+ qed
txt \<open>Lemma 3\<close>
have "\<H>(fst | OB) = -(\<Sum>obs\<in>OB`msgs. \<P>(OB) {obs} * ?Ht (t obs))"
--- a/src/HOL/Probability/ex/Measure_Not_CCC.thy Wed Oct 16 22:07:04 2024 +0200
+++ b/src/HOL/Probability/ex/Measure_Not_CCC.thy Wed Oct 16 23:13:02 2024 +0200
@@ -44,28 +44,30 @@
proof induction
case (Union F)
moreover
- { fix i assume "countable (UNIV - F i)"
- then have "countable (UNIV - (\<Union>i. F i))"
- by (rule countable_subset[rotated]) auto }
+ have "countable (UNIV - (\<Union>i. F i))" if "countable (UNIV - F i)" for i
+ using that by (rule countable_subset[rotated]) auto
ultimately show "countable (\<Union>i. F i) \<or> countable (UNIV - (\<Union>i. F i))"
by blast
qed (auto simp: Diff_Diff_Int)
next
assume "countable A \<or> countable (UNIV - A)"
moreover
- { fix A :: "real set" assume A: "countable A"
+ have A: "A \<in> COCOUNT" if "countable A" for A :: "real set"
+ proof -
have "A = (\<Union>a\<in>A. {a})"
by auto
also have "\<dots> \<in> COCOUNT"
- by (intro sets.countable_UN' A) (auto simp: COCOUNT_def)
- finally have "A \<in> COCOUNT" . }
- note A = this
+ by (intro sets.countable_UN' that) (auto simp: COCOUNT_def)
+ finally show ?thesis .
+ qed
note A[of A]
moreover
- { assume "countable (UNIV - A)"
- with A have "space COCOUNT - (UNIV - A) \<in> COCOUNT" by simp
- then have "A \<in> COCOUNT"
- by (auto simp: COCOUNT_def Diff_Diff_Int) }
+ have "A \<in> COCOUNT" if "countable (UNIV - A)"
+ proof -
+ from A that have "space COCOUNT - (UNIV - A) \<in> COCOUNT" by simp
+ then show ?thesis
+ by (auto simp: COCOUNT_def Diff_Diff_Int)
+ qed
ultimately show "A \<in> COCOUNT"
by blast
qed
@@ -121,12 +123,14 @@
lemma space_EXP: "space EXP = measurable COCOUNT BOOL"
proof -
- { fix f
+ have "f \<in> space EXP \<longleftrightarrow> f \<in> measurable COCOUNT BOOL" for f
+ proof -
have "f \<in> space EXP \<longleftrightarrow> (\<lambda>(a, b). f b) \<in> measurable (POW \<Otimes>\<^sub>M COCOUNT) BOOL"
using eq[of "\<lambda>x. f"] by (simp add: measurable_const_iff)
also have "\<dots> \<longleftrightarrow> f \<in> measurable COCOUNT BOOL"
by auto
- finally have "f \<in> space EXP \<longleftrightarrow> f \<in> measurable COCOUNT BOOL" . }
+ finally show ?thesis .
+ qed
then show ?thesis by auto
qed