author | hoelzl |
Wed, 10 Oct 2012 12:12:29 +0200 | |
changeset 49793 | dd719cdeca8f |
parent 49792 | 43f49922811d |
child 57418 | 6ab1c7cb0b8d |
permissions | -rw-r--r-- |
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41413
diff
changeset
|
1 |
(* Author: Johannes Hölzl, TU München *) |
40859 | 2 |
|
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41413
diff
changeset
|
3 |
header {* Formalization of a Countermeasure by Koepf \& Duermuth 2009 *} |
40859 | 4 |
|
5 |
theory Koepf_Duermuth_Countermeasure |
|
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41689
diff
changeset
|
6 |
imports "~~/src/HOL/Probability/Information" "~~/src/HOL/Library/Permutation" |
40859 | 7 |
begin |
8 |
||
45715
efd2b952f425
use list theorems in Dining Cryptographers and Koepf Duermuth Countermeasure
hoelzl
parents:
45712
diff
changeset
|
9 |
lemma SIGMA_image_vimage: |
efd2b952f425
use list theorems in Dining Cryptographers and Koepf Duermuth Countermeasure
hoelzl
parents:
45712
diff
changeset
|
10 |
"snd ` (SIGMA x:f`X. f -` {x} \<inter> X) = X" |
efd2b952f425
use list theorems in Dining Cryptographers and Koepf Duermuth Countermeasure
hoelzl
parents:
45712
diff
changeset
|
11 |
by (auto simp: image_iff) |
40859 | 12 |
|
45715
efd2b952f425
use list theorems in Dining Cryptographers and Koepf Duermuth Countermeasure
hoelzl
parents:
45712
diff
changeset
|
13 |
declare inj_split_Cons[simp] |
40859 | 14 |
|
42256
461624ffd382
Rename extensional to extensionalD (extensional is also defined in FuncSet)
hoelzl
parents:
41981
diff
changeset
|
15 |
definition extensionalD :: "'b \<Rightarrow> 'a set \<Rightarrow> ('a \<Rightarrow> 'b) set" where |
461624ffd382
Rename extensional to extensionalD (extensional is also defined in FuncSet)
hoelzl
parents:
41981
diff
changeset
|
16 |
"extensionalD d A = {f. \<forall>x. x \<notin> A \<longrightarrow> f x = d}" |
40859 | 17 |
|
42256
461624ffd382
Rename extensional to extensionalD (extensional is also defined in FuncSet)
hoelzl
parents:
41981
diff
changeset
|
18 |
lemma extensionalD_empty[simp]: "extensionalD d {} = {\<lambda>x. d}" |
461624ffd382
Rename extensional to extensionalD (extensional is also defined in FuncSet)
hoelzl
parents:
41981
diff
changeset
|
19 |
unfolding extensionalD_def by (simp add: set_eq_iff fun_eq_iff) |
40859 | 20 |
|
21 |
lemma funset_eq_UN_fun_upd_I: |
|
22 |
assumes *: "\<And>f. f \<in> F (insert a A) \<Longrightarrow> f(a := d) \<in> F A" |
|
23 |
and **: "\<And>f. f \<in> F (insert a A) \<Longrightarrow> f a \<in> G (f(a:=d))" |
|
24 |
and ***: "\<And>f x. \<lbrakk> f \<in> F A ; x \<in> G f \<rbrakk> \<Longrightarrow> f(a:=x) \<in> F (insert a A)" |
|
25 |
shows "F (insert a A) = (\<Union>f\<in>F A. fun_upd f a ` (G f))" |
|
26 |
proof safe |
|
27 |
fix f assume f: "f \<in> F (insert a A)" |
|
28 |
show "f \<in> (\<Union>f\<in>F A. fun_upd f a ` G f)" |
|
29 |
proof (rule UN_I[of "f(a := d)"]) |
|
30 |
show "f(a := d) \<in> F A" using *[OF f] . |
|
31 |
show "f \<in> fun_upd (f(a:=d)) a ` G (f(a:=d))" |
|
32 |
proof (rule image_eqI[of _ _ "f a"]) |
|
33 |
show "f a \<in> G (f(a := d))" using **[OF f] . |
|
34 |
qed simp |
|
35 |
qed |
|
36 |
next |
|
37 |
fix f x assume "f \<in> F A" "x \<in> G f" |
|
38 |
from ***[OF this] show "f(a := x) \<in> F (insert a A)" . |
|
39 |
qed |
|
40 |
||
42256
461624ffd382
Rename extensional to extensionalD (extensional is also defined in FuncSet)
hoelzl
parents:
41981
diff
changeset
|
41 |
lemma extensionalD_insert[simp]: |
40859 | 42 |
assumes "a \<notin> A" |
42256
461624ffd382
Rename extensional to extensionalD (extensional is also defined in FuncSet)
hoelzl
parents:
41981
diff
changeset
|
43 |
shows "extensionalD d (insert a A) \<inter> (insert a A \<rightarrow> B) = (\<Union>f \<in> extensionalD d A \<inter> (A \<rightarrow> B). (\<lambda>b. f(a := b)) ` B)" |
40859 | 44 |
apply (rule funset_eq_UN_fun_upd_I) |
45 |
using assms |
|
42256
461624ffd382
Rename extensional to extensionalD (extensional is also defined in FuncSet)
hoelzl
parents:
41981
diff
changeset
|
46 |
by (auto intro!: inj_onI dest: inj_onD split: split_if_asm simp: extensionalD_def) |
40859 | 47 |
|
42256
461624ffd382
Rename extensional to extensionalD (extensional is also defined in FuncSet)
hoelzl
parents:
41981
diff
changeset
|
48 |
lemma finite_extensionalD_funcset[simp, intro]: |
40859 | 49 |
assumes "finite A" "finite B" |
42256
461624ffd382
Rename extensional to extensionalD (extensional is also defined in FuncSet)
hoelzl
parents:
41981
diff
changeset
|
50 |
shows "finite (extensionalD d A \<inter> (A \<rightarrow> B))" |
40859 | 51 |
using assms by induct auto |
52 |
||
53 |
lemma fun_upd_eq_iff: "f(a := b) = g(a := b') \<longleftrightarrow> b = b' \<and> f(a := d) = g(a := d)" |
|
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41413
diff
changeset
|
54 |
by (auto simp: fun_eq_iff) |
40859 | 55 |
|
56 |
lemma card_funcset: |
|
57 |
assumes "finite A" "finite B" |
|
42256
461624ffd382
Rename extensional to extensionalD (extensional is also defined in FuncSet)
hoelzl
parents:
41981
diff
changeset
|
58 |
shows "card (extensionalD d A \<inter> (A \<rightarrow> B)) = card B ^ card A" |
40859 | 59 |
using `finite A` proof induct |
42256
461624ffd382
Rename extensional to extensionalD (extensional is also defined in FuncSet)
hoelzl
parents:
41981
diff
changeset
|
60 |
case (insert a A) thus ?case unfolding extensionalD_insert[OF `a \<notin> A`] |
40859 | 61 |
proof (subst card_UN_disjoint, safe, simp_all) |
42256
461624ffd382
Rename extensional to extensionalD (extensional is also defined in FuncSet)
hoelzl
parents:
41981
diff
changeset
|
62 |
show "finite (extensionalD d A \<inter> (A \<rightarrow> B))" "\<And>f. finite (fun_upd f a ` B)" |
40859 | 63 |
using `finite B` `finite A` by simp_all |
64 |
next |
|
65 |
fix f g b b' assume "f \<noteq> g" and eq: "f(a := b) = g(a := b')" and |
|
42256
461624ffd382
Rename extensional to extensionalD (extensional is also defined in FuncSet)
hoelzl
parents:
41981
diff
changeset
|
66 |
ext: "f \<in> extensionalD d A" "g \<in> extensionalD d A" |
40859 | 67 |
have "f a = d" "g a = d" |
42256
461624ffd382
Rename extensional to extensionalD (extensional is also defined in FuncSet)
hoelzl
parents:
41981
diff
changeset
|
68 |
using ext `a \<notin> A` by (auto simp add: extensionalD_def) |
40859 | 69 |
with `f \<noteq> g` eq show False unfolding fun_upd_eq_iff[of _ _ b _ _ d] |
70 |
by (auto simp: fun_upd_idem fun_upd_eq_iff) |
|
71 |
next |
|
42256
461624ffd382
Rename extensional to extensionalD (extensional is also defined in FuncSet)
hoelzl
parents:
41981
diff
changeset
|
72 |
{ fix f assume "f \<in> extensionalD d A \<inter> (A \<rightarrow> B)" |
40859 | 73 |
have "card (fun_upd f a ` B) = card B" |
74 |
proof (auto intro!: card_image inj_onI) |
|
75 |
fix b b' assume "f(a := b) = f(a := b')" |
|
76 |
from fun_upd_eq_iff[THEN iffD1, OF this] show "b = b'" by simp |
|
77 |
qed } |
|
42256
461624ffd382
Rename extensional to extensionalD (extensional is also defined in FuncSet)
hoelzl
parents:
41981
diff
changeset
|
78 |
then show "(\<Sum>i\<in>extensionalD d A \<inter> (A \<rightarrow> B). card (fun_upd i a ` B)) = card B * card B ^ card A" |
40859 | 79 |
using insert by simp |
80 |
qed |
|
81 |
qed simp |
|
82 |
||
45715
efd2b952f425
use list theorems in Dining Cryptographers and Koepf Duermuth Countermeasure
hoelzl
parents:
45712
diff
changeset
|
83 |
lemma zero_notin_Suc_image[simp]: "0 \<notin> Suc ` A" |
efd2b952f425
use list theorems in Dining Cryptographers and Koepf Duermuth Countermeasure
hoelzl
parents:
45712
diff
changeset
|
84 |
by auto |
40859 | 85 |
|
45715
efd2b952f425
use list theorems in Dining Cryptographers and Koepf Duermuth Countermeasure
hoelzl
parents:
45712
diff
changeset
|
86 |
lemma setprod_setsum_distrib_lists: |
efd2b952f425
use list theorems in Dining Cryptographers and Koepf Duermuth Countermeasure
hoelzl
parents:
45712
diff
changeset
|
87 |
fixes P and S :: "'a set" and f :: "'a \<Rightarrow> _::semiring_0" assumes "finite S" |
efd2b952f425
use list theorems in Dining Cryptographers and Koepf Duermuth Countermeasure
hoelzl
parents:
45712
diff
changeset
|
88 |
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)) = |
efd2b952f425
use list theorems in Dining Cryptographers and Koepf Duermuth Countermeasure
hoelzl
parents:
45712
diff
changeset
|
89 |
(\<Prod>i<n. \<Sum>m\<in>{m\<in>S. P i m}. f m)" |
efd2b952f425
use list theorems in Dining Cryptographers and Koepf Duermuth Countermeasure
hoelzl
parents:
45712
diff
changeset
|
90 |
proof (induct n arbitrary: P) |
efd2b952f425
use list theorems in Dining Cryptographers and Koepf Duermuth Countermeasure
hoelzl
parents:
45712
diff
changeset
|
91 |
case 0 then show ?case by (simp cong: conj_cong) |
efd2b952f425
use list theorems in Dining Cryptographers and Koepf Duermuth Countermeasure
hoelzl
parents:
45712
diff
changeset
|
92 |
next |
efd2b952f425
use list theorems in Dining Cryptographers and Koepf Duermuth Countermeasure
hoelzl
parents:
45712
diff
changeset
|
93 |
case (Suc n) |
efd2b952f425
use list theorems in Dining Cryptographers and Koepf Duermuth Countermeasure
hoelzl
parents:
45712
diff
changeset
|
94 |
have *: "{ms. set ms \<subseteq> S \<and> length ms = Suc n \<and> (\<forall>i<Suc n. P i (ms ! i))} = |
efd2b952f425
use list theorems in Dining Cryptographers and Koepf Duermuth Countermeasure
hoelzl
parents:
45712
diff
changeset
|
95 |
(\<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})" |
efd2b952f425
use list theorems in Dining Cryptographers and Koepf Duermuth Countermeasure
hoelzl
parents:
45712
diff
changeset
|
96 |
apply (auto simp: image_iff length_Suc_conv) |
efd2b952f425
use list theorems in Dining Cryptographers and Koepf Duermuth Countermeasure
hoelzl
parents:
45712
diff
changeset
|
97 |
apply force+ |
efd2b952f425
use list theorems in Dining Cryptographers and Koepf Duermuth Countermeasure
hoelzl
parents:
45712
diff
changeset
|
98 |
apply (case_tac i) |
efd2b952f425
use list theorems in Dining Cryptographers and Koepf Duermuth Countermeasure
hoelzl
parents:
45712
diff
changeset
|
99 |
by force+ |
efd2b952f425
use list theorems in Dining Cryptographers and Koepf Duermuth Countermeasure
hoelzl
parents:
45712
diff
changeset
|
100 |
show ?case unfolding * |
efd2b952f425
use list theorems in Dining Cryptographers and Koepf Duermuth Countermeasure
hoelzl
parents:
45712
diff
changeset
|
101 |
using Suc[of "\<lambda>i. P (Suc i)"] |
efd2b952f425
use list theorems in Dining Cryptographers and Koepf Duermuth Countermeasure
hoelzl
parents:
45712
diff
changeset
|
102 |
by (simp add: setsum_reindex split_conv setsum_cartesian_product' |
efd2b952f425
use list theorems in Dining Cryptographers and Koepf Duermuth Countermeasure
hoelzl
parents:
45712
diff
changeset
|
103 |
lessThan_Suc_eq_insert_0 setprod_reindex setsum_left_distrib[symmetric] setsum_right_distrib[symmetric]) |
efd2b952f425
use list theorems in Dining Cryptographers and Koepf Duermuth Countermeasure
hoelzl
parents:
45712
diff
changeset
|
104 |
qed |
efd2b952f425
use list theorems in Dining Cryptographers and Koepf Duermuth Countermeasure
hoelzl
parents:
45712
diff
changeset
|
105 |
|
47694 | 106 |
declare space_point_measure[simp] |
45715
efd2b952f425
use list theorems in Dining Cryptographers and Koepf Duermuth Countermeasure
hoelzl
parents:
45712
diff
changeset
|
107 |
|
47694 | 108 |
declare sets_point_measure[simp] |
45715
efd2b952f425
use list theorems in Dining Cryptographers and Koepf Duermuth Countermeasure
hoelzl
parents:
45712
diff
changeset
|
109 |
|
47694 | 110 |
lemma measure_point_measure: |
111 |
"finite \<Omega> \<Longrightarrow> A \<subseteq> \<Omega> \<Longrightarrow> (\<And>x. x \<in> \<Omega> \<Longrightarrow> 0 \<le> p x) \<Longrightarrow> |
|
112 |
measure (point_measure \<Omega> (\<lambda>x. ereal (p x))) A = (\<Sum>i\<in>A. p i)" |
|
113 |
unfolding measure_def by (subst emeasure_point_measure_finite) auto |
|
45715
efd2b952f425
use list theorems in Dining Cryptographers and Koepf Duermuth Countermeasure
hoelzl
parents:
45712
diff
changeset
|
114 |
|
40859 | 115 |
locale finite_information = |
116 |
fixes \<Omega> :: "'a set" |
|
117 |
and p :: "'a \<Rightarrow> real" |
|
118 |
and b :: real |
|
119 |
assumes finite_space[simp, intro]: "finite \<Omega>" |
|
120 |
and p_sums_1[simp]: "(\<Sum>\<omega>\<in>\<Omega>. p \<omega>) = 1" |
|
121 |
and positive_p[simp, intro]: "\<And>x. 0 \<le> p x" |
|
122 |
and b_gt_1[simp, intro]: "1 < b" |
|
123 |
||
124 |
lemma (in finite_information) positive_p_sum[simp]: "0 \<le> setsum p X" |
|
125 |
by (auto intro!: setsum_nonneg) |
|
126 |
||
47694 | 127 |
sublocale finite_information \<subseteq> prob_space "point_measure \<Omega> p" |
128 |
by default (simp add: one_ereal_def emeasure_point_measure_finite) |
|
40859 | 129 |
|
47694 | 130 |
sublocale finite_information \<subseteq> information_space "point_measure \<Omega> p" b |
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41413
diff
changeset
|
131 |
by default simp |
40859 | 132 |
|
47694 | 133 |
lemma (in finite_information) \<mu>'_eq: "A \<subseteq> \<Omega> \<Longrightarrow> prob A = setsum p A" |
134 |
by (auto simp: measure_point_measure) |
|
40859 | 135 |
|
136 |
locale koepf_duermuth = K: finite_information keys K b + M: finite_information messages M b |
|
137 |
for b :: real |
|
138 |
and keys :: "'key set" and K :: "'key \<Rightarrow> real" |
|
139 |
and messages :: "'message set" and M :: "'message \<Rightarrow> real" + |
|
140 |
fixes observe :: "'key \<Rightarrow> 'message \<Rightarrow> 'observation" |
|
141 |
and n :: nat |
|
142 |
begin |
|
143 |
||
144 |
definition msgs :: "('key \<times> 'message list) set" where |
|
45715
efd2b952f425
use list theorems in Dining Cryptographers and Koepf Duermuth Countermeasure
hoelzl
parents:
45712
diff
changeset
|
145 |
"msgs = keys \<times> {ms. set ms \<subseteq> messages \<and> length ms = n}" |
40859 | 146 |
|
147 |
definition P :: "('key \<times> 'message list) \<Rightarrow> real" where |
|
49793 | 148 |
"P = (\<lambda>(k, ms). K k * (\<Prod>i<n. M (ms ! i)))" |
40859 | 149 |
|
150 |
end |
|
151 |
||
152 |
sublocale koepf_duermuth \<subseteq> finite_information msgs P b |
|
153 |
proof default |
|
154 |
show "finite msgs" unfolding msgs_def |
|
45715
efd2b952f425
use list theorems in Dining Cryptographers and Koepf Duermuth Countermeasure
hoelzl
parents:
45712
diff
changeset
|
155 |
using finite_lists_length_eq[OF M.finite_space, of n] |
40859 | 156 |
by auto |
157 |
||
158 |
have [simp]: "\<And>A. inj_on (\<lambda>(xs, n). n # xs) A" by (force intro!: inj_onI) |
|
159 |
||
160 |
note setsum_right_distrib[symmetric, simp] |
|
161 |
note setsum_left_distrib[symmetric, simp] |
|
162 |
note setsum_cartesian_product'[simp] |
|
163 |
||
45715
efd2b952f425
use list theorems in Dining Cryptographers and Koepf Duermuth Countermeasure
hoelzl
parents:
45712
diff
changeset
|
164 |
have "(\<Sum>ms | set ms \<subseteq> messages \<and> length ms = n. \<Prod>x<length ms. M (ms ! x)) = 1" |
40859 | 165 |
proof (induct n) |
166 |
case 0 then show ?case by (simp cong: conj_cong) |
|
167 |
next |
|
168 |
case (Suc n) |
|
169 |
then show ?case |
|
45715
efd2b952f425
use list theorems in Dining Cryptographers and Koepf Duermuth Countermeasure
hoelzl
parents:
45712
diff
changeset
|
170 |
by (simp add: lists_length_Suc_eq lessThan_Suc_eq_insert_0 |
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41413
diff
changeset
|
171 |
setsum_reindex setprod_reindex) |
40859 | 172 |
qed |
173 |
then show "setsum P msgs = 1" |
|
174 |
unfolding msgs_def P_def by simp |
|
175 |
fix x |
|
176 |
have "\<And> A f. 0 \<le> (\<Prod>x\<in>A. M (f x))" by (auto simp: setprod_nonneg) |
|
177 |
then show "0 \<le> P x" |
|
178 |
unfolding P_def by (auto split: prod.split simp: zero_le_mult_iff) |
|
179 |
qed auto |
|
180 |
||
181 |
context koepf_duermuth |
|
182 |
begin |
|
183 |
||
184 |
definition observations :: "'observation set" where |
|
185 |
"observations = (\<Union>f\<in>observe ` keys. f ` messages)" |
|
186 |
||
187 |
lemma finite_observations[simp, intro]: "finite observations" |
|
188 |
unfolding observations_def by auto |
|
189 |
||
190 |
definition OB :: "'key \<times> 'message list \<Rightarrow> 'observation list" where |
|
191 |
"OB = (\<lambda>(k, ms). map (observe k) ms)" |
|
192 |
||
193 |
definition t :: "'observation list \<Rightarrow> 'observation \<Rightarrow> nat" where |
|
49793 | 194 |
t_def2: "t seq obs = card { i. i < length seq \<and> seq ! i = obs}" |
195 |
||
196 |
lemma t_def: "t seq obs = length (filter (op = obs) seq)" |
|
197 |
unfolding t_def2 length_filter_conv_card by (subst eq_commute) simp |
|
40859 | 198 |
|
199 |
lemma card_T_bound: "card ((t\<circ>OB)`msgs) \<le> (n+1)^card observations" |
|
200 |
proof - |
|
42256
461624ffd382
Rename extensional to extensionalD (extensional is also defined in FuncSet)
hoelzl
parents:
41981
diff
changeset
|
201 |
have "(t\<circ>OB)`msgs \<subseteq> extensionalD 0 observations \<inter> (observations \<rightarrow> {.. n})" |
461624ffd382
Rename extensional to extensionalD (extensional is also defined in FuncSet)
hoelzl
parents:
41981
diff
changeset
|
202 |
unfolding observations_def extensionalD_def OB_def msgs_def |
45715
efd2b952f425
use list theorems in Dining Cryptographers and Koepf Duermuth Countermeasure
hoelzl
parents:
45712
diff
changeset
|
203 |
by (auto simp add: t_def comp_def image_iff subset_eq) |
42256
461624ffd382
Rename extensional to extensionalD (extensional is also defined in FuncSet)
hoelzl
parents:
41981
diff
changeset
|
204 |
with finite_extensionalD_funcset |
461624ffd382
Rename extensional to extensionalD (extensional is also defined in FuncSet)
hoelzl
parents:
41981
diff
changeset
|
205 |
have "card ((t\<circ>OB)`msgs) \<le> card (extensionalD 0 observations \<inter> (observations \<rightarrow> {.. n}))" |
40859 | 206 |
by (rule card_mono) auto |
207 |
also have "\<dots> = (n + 1) ^ card observations" |
|
208 |
by (subst card_funcset) auto |
|
209 |
finally show ?thesis . |
|
210 |
qed |
|
211 |
||
212 |
abbreviation |
|
213 |
"p A \<equiv> setsum P A" |
|
214 |
||
47694 | 215 |
abbreviation |
216 |
"\<mu> \<equiv> point_measure msgs P" |
|
217 |
||
40859 | 218 |
abbreviation probability ("\<P>'(_') _") where |
47694 | 219 |
"\<P>(X) x \<equiv> measure \<mu> (X -` x \<inter> msgs)" |
40859 | 220 |
|
47694 | 221 |
abbreviation joint_probability ("\<P>'(_ ; _') _") where |
222 |
"\<P>(X ; Y) x \<equiv> \<P>(\<lambda>x. (X x, Y x)) x" |
|
40859 | 223 |
|
47694 | 224 |
no_notation disj (infixr "|" 30) |
225 |
||
226 |
abbreviation conditional_probability ("\<P>'(_ | _') _") where |
|
227 |
"\<P>(X | Y) x \<equiv> (\<P>(X ; Y) x) / \<P>(Y) (snd`x)" |
|
40859 | 228 |
|
229 |
notation |
|
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41413
diff
changeset
|
230 |
entropy_Pow ("\<H>'( _ ')") |
40859 | 231 |
|
232 |
notation |
|
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41413
diff
changeset
|
233 |
conditional_entropy_Pow ("\<H>'( _ | _ ')") |
40859 | 234 |
|
235 |
notation |
|
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41413
diff
changeset
|
236 |
mutual_information_Pow ("\<I>'( _ ; _ ')") |
40859 | 237 |
|
238 |
lemma t_eq_imp_bij_func: |
|
239 |
assumes "t xs = t ys" |
|
240 |
shows "\<exists>f. bij_betw f {..<length xs} {..<length ys} \<and> (\<forall>i<length xs. xs ! i = ys ! (f i))" |
|
241 |
proof - |
|
242 |
have "count (multiset_of xs) = count (multiset_of ys)" |
|
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41413
diff
changeset
|
243 |
using assms by (simp add: fun_eq_iff count_multiset_of t_def) |
40859 | 244 |
then have "xs <~~> ys" unfolding multiset_of_eq_perm count_inject . |
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41413
diff
changeset
|
245 |
then show ?thesis by (rule permutation_Ex_bij) |
40859 | 246 |
qed |
247 |
||
248 |
lemma \<P>_k: assumes "k \<in> keys" shows "\<P>(fst) {k} = K k" |
|
249 |
proof - |
|
250 |
from assms have *: |
|
45715
efd2b952f425
use list theorems in Dining Cryptographers and Koepf Duermuth Countermeasure
hoelzl
parents:
45712
diff
changeset
|
251 |
"fst -` {k} \<inter> msgs = {k}\<times>{ms. set ms \<subseteq> messages \<and> length ms = n}" |
40859 | 252 |
unfolding msgs_def by auto |
47694 | 253 |
show "(\<P>(fst) {k}) = K k" |
254 |
apply (simp add: \<mu>'_eq) |
|
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41689
diff
changeset
|
255 |
apply (simp add: * P_def) |
40859 | 256 |
apply (simp add: setsum_cartesian_product') |
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41689
diff
changeset
|
257 |
using setprod_setsum_distrib_lists[OF M.finite_space, of M n "\<lambda>x x. True"] `k \<in> keys` |
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41689
diff
changeset
|
258 |
by (auto simp add: setsum_right_distrib[symmetric] subset_eq setprod_1) |
40859 | 259 |
qed |
260 |
||
261 |
lemma fst_image_msgs[simp]: "fst`msgs = keys" |
|
262 |
proof - |
|
263 |
from M.not_empty obtain m where "m \<in> messages" by auto |
|
45715
efd2b952f425
use list theorems in Dining Cryptographers and Koepf Duermuth Countermeasure
hoelzl
parents:
45712
diff
changeset
|
264 |
then have *: "{m. set m \<subseteq> messages \<and> length m = n} \<noteq> {}" |
40859 | 265 |
by (auto intro!: exI[of _ "replicate n m"]) |
266 |
then show ?thesis |
|
267 |
unfolding msgs_def fst_image_times if_not_P[OF *] by simp |
|
268 |
qed |
|
269 |
||
47694 | 270 |
lemma setsum_distribution_cut: |
271 |
"\<P>(X) {x} = (\<Sum>y \<in> Y`space \<mu>. \<P>(X ; Y) {(x, y)})" |
|
272 |
by (subst finite_measure_finite_Union[symmetric]) |
|
273 |
(auto simp add: disjoint_family_on_def inj_on_def |
|
274 |
intro!: arg_cong[where f=prob]) |
|
275 |
||
276 |
lemma prob_conj_imp1: |
|
277 |
"prob ({x. Q x} \<inter> msgs) = 0 \<Longrightarrow> prob ({x. Pr x \<and> Q x} \<inter> msgs) = 0" |
|
278 |
using finite_measure_mono[of "{x. Pr x \<and> Q x} \<inter> msgs" "{x. Q x} \<inter> msgs"] |
|
279 |
using measure_nonneg[of \<mu> "{x. Pr x \<and> Q x} \<inter> msgs"] |
|
280 |
by (simp add: subset_eq) |
|
281 |
||
282 |
lemma prob_conj_imp2: |
|
283 |
"prob ({x. Pr x} \<inter> msgs) = 0 \<Longrightarrow> prob ({x. Pr x \<and> Q x} \<inter> msgs) = 0" |
|
284 |
using finite_measure_mono[of "{x. Pr x \<and> Q x} \<inter> msgs" "{x. Pr x} \<inter> msgs"] |
|
285 |
using measure_nonneg[of \<mu> "{x. Pr x \<and> Q x} \<inter> msgs"] |
|
286 |
by (simp add: subset_eq) |
|
287 |
||
288 |
lemma simple_function_finite: "simple_function \<mu> f" |
|
289 |
by (simp add: simple_function_def) |
|
290 |
||
291 |
lemma entropy_commute: "\<H>(\<lambda>x. (X x, Y x)) = \<H>(\<lambda>x. (Y x, X x))" |
|
292 |
apply (subst (1 2) entropy_simple_distributed[OF simple_distributedI[OF simple_function_finite refl]]) |
|
293 |
unfolding space_point_measure |
|
294 |
proof - |
|
295 |
have eq: "(\<lambda>x. (X x, Y x)) ` msgs = (\<lambda>(x, y). (y, x)) ` (\<lambda>x. (Y x, X x)) ` msgs" |
|
296 |
by auto |
|
297 |
show "- (\<Sum>x\<in>(\<lambda>x. (X x, Y x)) ` msgs. (\<P>(X ; Y) {x}) * log b (\<P>(X ; Y) {x})) = |
|
298 |
- (\<Sum>x\<in>(\<lambda>x. (Y x, X x)) ` msgs. (\<P>(Y ; X) {x}) * log b (\<P>(Y ; X) {x}))" |
|
299 |
unfolding eq |
|
300 |
apply (subst setsum_reindex) |
|
301 |
apply (auto simp: vimage_def inj_on_def intro!: setsum_cong arg_cong[where f="\<lambda>x. prob x * log b (prob x)"]) |
|
302 |
done |
|
303 |
qed |
|
304 |
||
305 |
lemma (in -) measure_eq_0I: "A = {} \<Longrightarrow> measure M A = 0" by simp |
|
306 |
||
307 |
lemma conditional_entropy_eq_ce_with_hypothesis: |
|
308 |
"\<H>(X | Y) = -(\<Sum>y\<in>Y`msgs. (\<P>(Y) {y}) * (\<Sum>x\<in>X`msgs. (\<P>(X ; Y) {(x,y)}) / (\<P>(Y) {y}) * |
|
309 |
log b ((\<P>(X ; Y) {(x,y)}) / (\<P>(Y) {y}))))" |
|
310 |
apply (subst conditional_entropy_eq[OF |
|
311 |
simple_distributedI[OF simple_function_finite refl] |
|
312 |
simple_distributedI[OF simple_function_finite refl]]) |
|
313 |
unfolding space_point_measure |
|
314 |
proof - |
|
315 |
have "- (\<Sum>(x, y)\<in>(\<lambda>x. (X x, Y x)) ` msgs. (\<P>(X ; Y) {(x, y)}) * log b ((\<P>(X ; Y) {(x, y)}) / (\<P>(Y) {y}))) = |
|
316 |
- (\<Sum>x\<in>X`msgs. (\<Sum>y\<in>Y`msgs. (\<P>(X ; Y) {(x, y)}) * log b ((\<P>(X ; Y) {(x, y)}) / (\<P>(Y) {y}))))" |
|
317 |
unfolding setsum_cartesian_product |
|
318 |
apply (intro arg_cong[where f=uminus] setsum_mono_zero_left) |
|
319 |
apply (auto simp: vimage_def image_iff intro!: measure_eq_0I) |
|
320 |
apply metis |
|
321 |
done |
|
322 |
also have "\<dots> = - (\<Sum>y\<in>Y`msgs. (\<Sum>x\<in>X`msgs. (\<P>(X ; Y) {(x, y)}) * log b ((\<P>(X ; Y) {(x, y)}) / (\<P>(Y) {y}))))" |
|
323 |
by (subst setsum_commute) rule |
|
324 |
also have "\<dots> = -(\<Sum>y\<in>Y`msgs. (\<P>(Y) {y}) * (\<Sum>x\<in>X`msgs. (\<P>(X ; Y) {(x,y)}) / (\<P>(Y) {y}) * log b ((\<P>(X ; Y) {(x,y)}) / (\<P>(Y) {y}))))" |
|
325 |
by (auto simp add: setsum_right_distrib vimage_def intro!: setsum_cong prob_conj_imp1) |
|
326 |
finally show "- (\<Sum>(x, y)\<in>(\<lambda>x. (X x, Y x)) ` msgs. (\<P>(X ; Y) {(x, y)}) * log b ((\<P>(X ; Y) {(x, y)}) / (\<P>(Y) {y}))) = |
|
327 |
-(\<Sum>y\<in>Y`msgs. (\<P>(Y) {y}) * (\<Sum>x\<in>X`msgs. (\<P>(X ; Y) {(x,y)}) / (\<P>(Y) {y}) * log b ((\<P>(X ; Y) {(x,y)}) / (\<P>(Y) {y}))))" . |
|
328 |
qed |
|
329 |
||
49793 | 330 |
lemma ce_OB_eq_ce_t: "\<I>(fst ; OB) = \<I>(fst ; t\<circ>OB)" |
40859 | 331 |
proof - |
332 |
txt {* Lemma 2 *} |
|
333 |
||
334 |
{ fix k obs obs' |
|
335 |
assume "k \<in> keys" "K k \<noteq> 0" and obs': "obs' \<in> OB ` msgs" and obs: "obs \<in> OB ` msgs" |
|
336 |
assume "t obs = t obs'" |
|
337 |
from t_eq_imp_bij_func[OF this] |
|
338 |
obtain t_f where "bij_betw t_f {..<n} {..<n}" and |
|
339 |
obs_t_f: "\<And>i. i<n \<Longrightarrow> obs!i = obs' ! t_f i" |
|
340 |
using obs obs' unfolding OB_def msgs_def by auto |
|
341 |
then have t_f: "inj_on t_f {..<n}" "{..<n} = t_f`{..<n}" unfolding bij_betw_def by auto |
|
342 |
||
343 |
{ fix obs assume "obs \<in> OB`msgs" |
|
344 |
then have **: "\<And>ms. length ms = n \<Longrightarrow> OB (k, ms) = obs \<longleftrightarrow> (\<forall>i<n. observe k (ms!i) = obs ! i)" |
|
345 |
unfolding OB_def msgs_def by (simp add: image_iff list_eq_iff_nth_eq) |
|
346 |
||
47694 | 347 |
have "(\<P>(OB ; fst) {(obs, k)}) / K k = |
40859 | 348 |
p ({k}\<times>{ms. (k,ms) \<in> msgs \<and> OB (k,ms) = obs}) / K k" |
47694 | 349 |
apply (simp add: \<mu>'_eq) by (auto intro!: arg_cong[where f=p]) |
40859 | 350 |
also have "\<dots> = |
351 |
(\<Prod>i<n. \<Sum>m\<in>{m\<in>messages. observe k m = obs ! i}. M m)" |
|
352 |
unfolding P_def using `K k \<noteq> 0` `k \<in> keys` |
|
353 |
apply (simp add: setsum_cartesian_product' setsum_divide_distrib msgs_def ** cong: conj_cong) |
|
45715
efd2b952f425
use list theorems in Dining Cryptographers and Koepf Duermuth Countermeasure
hoelzl
parents:
45712
diff
changeset
|
354 |
apply (subst setprod_setsum_distrib_lists[OF M.finite_space]) .. |
47694 | 355 |
finally have "(\<P>(OB ; fst) {(obs, k)}) / K k = |
40859 | 356 |
(\<Prod>i<n. \<Sum>m\<in>{m\<in>messages. observe k m = obs ! i}. M m)" . } |
357 |
note * = this |
|
358 |
||
47694 | 359 |
have "(\<P>(OB ; fst) {(obs, k)}) / K k = (\<P>(OB ; fst) {(obs', k)}) / K k" |
40859 | 360 |
unfolding *[OF obs] *[OF obs'] |
361 |
using t_f(1) obs_t_f by (subst (2) t_f(2)) (simp add: setprod_reindex) |
|
47694 | 362 |
then have "(\<P>(OB ; fst) {(obs, k)}) = (\<P>(OB ; fst) {(obs', k)})" |
40859 | 363 |
using `K k \<noteq> 0` by auto } |
364 |
note t_eq_imp = this |
|
365 |
||
46731 | 366 |
let ?S = "\<lambda>obs. t -`{t obs} \<inter> OB`msgs" |
40859 | 367 |
{ fix k obs assume "k \<in> keys" "K k \<noteq> 0" and obs: "obs \<in> OB`msgs" |
368 |
have *: "((\<lambda>x. (t (OB x), fst x)) -` {(t obs, k)} \<inter> msgs) = |
|
369 |
(\<Union>obs'\<in>?S obs. ((\<lambda>x. (OB x, fst x)) -` {(obs', k)} \<inter> msgs))" by auto |
|
370 |
have df: "disjoint_family_on (\<lambda>obs'. (\<lambda>x. (OB x, fst x)) -` {(obs', k)} \<inter> msgs) (?S obs)" |
|
371 |
unfolding disjoint_family_on_def by auto |
|
47694 | 372 |
have "\<P>(t\<circ>OB ; fst) {(t obs, k)} = (\<Sum>obs'\<in>?S obs. \<P>(OB ; fst) {(obs', k)})" |
373 |
unfolding comp_def |
|
374 |
using finite_measure_finite_Union[OF _ df] |
|
375 |
by (auto simp add: * intro!: setsum_nonneg) |
|
376 |
also have "(\<Sum>obs'\<in>?S obs. \<P>(OB ; fst) {(obs', k)}) = real (card (?S obs)) * \<P>(OB ; fst) {(obs, k)}" |
|
40859 | 377 |
by (simp add: t_eq_imp[OF `k \<in> keys` `K k \<noteq> 0` obs] real_eq_of_nat) |
47694 | 378 |
finally have "\<P>(t\<circ>OB ; fst) {(t obs, k)} = real (card (?S obs)) * \<P>(OB ; fst) {(obs, k)}" .} |
40859 | 379 |
note P_t_eq_P_OB = this |
380 |
||
381 |
{ fix k obs assume "k \<in> keys" and obs: "obs \<in> OB`msgs" |
|
382 |
have "\<P>(t\<circ>OB | fst) {(t obs, k)} = |
|
383 |
real (card (t -` {t obs} \<inter> OB ` msgs)) * \<P>(OB | fst) {(obs, k)}" |
|
384 |
using \<P>_k[OF `k \<in> keys`] P_t_eq_P_OB[OF `k \<in> keys` _ obs] by auto } |
|
385 |
note CP_t_K = this |
|
386 |
||
387 |
{ fix k obs assume "k \<in> keys" and obs: "obs \<in> OB`msgs" |
|
388 |
then have "t -`{t obs} \<inter> OB`msgs \<noteq> {}" (is "?S \<noteq> {}") by auto |
|
389 |
then have "real (card ?S) \<noteq> 0" by auto |
|
390 |
||
391 |
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}" |
|
47694 | 392 |
using finite_measure_mono[of "{x. fst x = k \<and> t (OB x) = t obs} \<inter> msgs" "{x. fst x = k} \<inter> msgs"] |
393 |
using measure_nonneg[of \<mu> "{x. fst x = k \<and> t (OB x) = t obs} \<inter> msgs"] |
|
394 |
by (auto simp add: vimage_def conj_commute subset_eq) |
|
395 |
also have "(\<P>(t\<circ>OB) {t obs}) = (\<Sum>k'\<in>keys. (\<P>(t\<circ>OB|fst) {(t obs, k')}) * (\<P>(fst) {k'}))" |
|
396 |
using finite_measure_mono[of "{x. t (OB x) = t obs \<and> fst x = k} \<inter> msgs" "{x. fst x = k} \<inter> msgs"] |
|
397 |
using measure_nonneg[of \<mu> "{x. fst x = k \<and> t (OB x) = t obs} \<inter> msgs"] |
|
398 |
apply (simp add: setsum_distribution_cut[of "t\<circ>OB" "t obs" fst]) |
|
399 |
apply (auto intro!: setsum_cong simp: subset_eq vimage_def prob_conj_imp1) |
|
400 |
done |
|
40859 | 401 |
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'}) = |
402 |
\<P>(OB | fst) {(obs, k)} * \<P>(fst) {k} / (\<Sum>k'\<in>keys. \<P>(OB|fst) {(obs, k')} * \<P>(fst) {k'})" |
|
403 |
using CP_t_K[OF `k\<in>keys` obs] CP_t_K[OF _ obs] `real (card ?S) \<noteq> 0` |
|
404 |
by (simp only: setsum_right_distrib[symmetric] ac_simps |
|
405 |
mult_divide_mult_cancel_left[OF `real (card ?S) \<noteq> 0`] |
|
406 |
cong: setsum_cong) |
|
407 |
also have "(\<Sum>k'\<in>keys. \<P>(OB|fst) {(obs, k')} * \<P>(fst) {k'}) = \<P>(OB) {obs}" |
|
47694 | 408 |
using setsum_distribution_cut[of OB obs fst] |
409 |
by (auto intro!: setsum_cong simp: prob_conj_imp1 vimage_def) |
|
40859 | 410 |
also have "\<P>(OB | fst) {(obs, k)} * \<P>(fst) {k} / \<P>(OB) {obs} = \<P>(fst | OB) {(k, obs)}" |
47694 | 411 |
by (auto simp: vimage_def conj_commute prob_conj_imp2) |
40859 | 412 |
finally have "\<P>(fst | t\<circ>OB) {(k, t obs)} = \<P>(fst | OB) {(k, obs)}" . } |
413 |
note CP_T_eq_CP_O = this |
|
414 |
||
46731 | 415 |
let ?H = "\<lambda>obs. (\<Sum>k\<in>keys. \<P>(fst|OB) {(k, obs)} * log b (\<P>(fst|OB) {(k, obs)})) :: real" |
416 |
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" |
|
40859 | 417 |
|
418 |
{ fix obs assume obs: "obs \<in> OB`msgs" |
|
419 |
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)}))" |
|
420 |
using CP_T_eq_CP_O[OF _ obs] |
|
421 |
by simp |
|
422 |
then have "?H obs = ?Ht (t obs)" . } |
|
423 |
note * = this |
|
424 |
||
425 |
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 |
|
426 |
||
427 |
{ fix x |
|
428 |
have *: "(\<lambda>x. t (OB x)) -` {t (OB x)} \<inter> msgs = |
|
429 |
(\<Union>obs\<in>?S (OB x). OB -` {obs} \<inter> msgs)" by auto |
|
430 |
have df: "disjoint_family_on (\<lambda>obs. OB -` {obs} \<inter> msgs) (?S (OB x))" |
|
431 |
unfolding disjoint_family_on_def by auto |
|
432 |
have "\<P>(t\<circ>OB) {t (OB x)} = (\<Sum>obs\<in>?S (OB x). \<P>(OB) {obs})" |
|
47694 | 433 |
unfolding comp_def |
434 |
using finite_measure_finite_Union[OF _ df] |
|
40859 | 435 |
by (force simp add: * intro!: setsum_nonneg) } |
436 |
note P_t_sum_P_O = this |
|
437 |
||
438 |
txt {* Lemma 3 *} |
|
439 |
have "\<H>(fst | OB) = -(\<Sum>obs\<in>OB`msgs. \<P>(OB) {obs} * ?Ht (t obs))" |
|
47694 | 440 |
unfolding conditional_entropy_eq_ce_with_hypothesis using * by simp |
40859 | 441 |
also have "\<dots> = -(\<Sum>obs\<in>t`OB`msgs. \<P>(t\<circ>OB) {obs} * ?Ht obs)" |
442 |
apply (subst SIGMA_image_vimage[symmetric, of "OB`msgs" t]) |
|
443 |
apply (subst setsum_reindex) |
|
44890
22f665a2e91c
new fastforce replacing fastsimp - less confusing name
nipkow
parents:
43920
diff
changeset
|
444 |
apply (fastforce intro!: inj_onI) |
40859 | 445 |
apply simp |
446 |
apply (subst setsum_Sigma[symmetric, unfolded split_def]) |
|
44890
22f665a2e91c
new fastforce replacing fastsimp - less confusing name
nipkow
parents:
43920
diff
changeset
|
447 |
using finite_space apply fastforce |
22f665a2e91c
new fastforce replacing fastsimp - less confusing name
nipkow
parents:
43920
diff
changeset
|
448 |
using finite_space apply fastforce |
40859 | 449 |
apply (safe intro!: setsum_cong) |
450 |
using P_t_sum_P_O |
|
451 |
by (simp add: setsum_divide_distrib[symmetric] field_simps ** |
|
452 |
setsum_right_distrib[symmetric] setsum_left_distrib[symmetric]) |
|
453 |
also have "\<dots> = \<H>(fst | t\<circ>OB)" |
|
47694 | 454 |
unfolding conditional_entropy_eq_ce_with_hypothesis |
40859 | 455 |
by (simp add: comp_def image_image[symmetric]) |
49793 | 456 |
finally show ?thesis |
457 |
by (subst (1 2) mutual_information_eq_entropy_conditional_entropy) simp_all |
|
40859 | 458 |
qed |
459 |
||
460 |
theorem "\<I>(fst ; OB) \<le> real (card observations) * log b (real n + 1)" |
|
461 |
proof - |
|
49793 | 462 |
have "\<I>(fst ; OB) = \<H>(fst) - \<H>(fst | t\<circ>OB)" |
463 |
unfolding ce_OB_eq_ce_t |
|
464 |
by (rule mutual_information_eq_entropy_conditional_entropy simple_function_finite)+ |
|
40859 | 465 |
also have "\<dots> = \<H>(t\<circ>OB) - \<H>(t\<circ>OB | fst)" |
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41413
diff
changeset
|
466 |
unfolding entropy_chain_rule[symmetric, OF simple_function_finite simple_function_finite] sign_simps |
47694 | 467 |
by (subst entropy_commute) simp |
40859 | 468 |
also have "\<dots> \<le> \<H>(t\<circ>OB)" |
47694 | 469 |
using conditional_entropy_nonneg[of "t\<circ>OB" fst] by simp |
40859 | 470 |
also have "\<dots> \<le> log b (real (card ((t\<circ>OB)`msgs)))" |
47694 | 471 |
using entropy_le_card[of "t\<circ>OB", OF simple_distributedI[OF simple_function_finite refl]] by simp |
40859 | 472 |
also have "\<dots> \<le> log b (real (n + 1)^card observations)" |
473 |
using card_T_bound not_empty |
|
474 |
by (auto intro!: log_le simp: card_gt_0_iff power_real_of_nat simp del: real_of_nat_power) |
|
475 |
also have "\<dots> = real (card observations) * log b (real n + 1)" |
|
476 |
by (simp add: log_nat_power real_of_nat_Suc) |
|
477 |
finally show ?thesis . |
|
478 |
qed |
|
479 |
||
480 |
end |
|
481 |
||
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41413
diff
changeset
|
482 |
end |