summary |
shortlog |
changelog |
graph |
tags |
branches |
files |
changeset |
file |
revisions |
annotate |
diff |
raw

src/HOL/Probability/Random_Permutations.thy

author | eberlm <eberlm@in.tum.de> |

Tue Apr 04 08:57:21 2017 +0200 (2017-04-04) | |

changeset 65395 | 7504569a73c7 |

parent 63965 | d510b816ea41 |

child 66453 | cc19f7ca2ed6 |

permissions | -rw-r--r-- |

moved material from AFP to distribution

1 (*

2 Title: Random_Permutations.thy

3 Author: Manuel Eberl, TU München

5 Random permutations and folding over them.

6 This provides the basic theory for the concept of doing something

7 in a random order, e.g. inserting elements from a fixed set into a

8 data structure in random order.

9 *)

11 section \<open>Random Permutations\<close>

13 theory Random_Permutations

14 imports

15 "~~/src/HOL/Probability/Probability_Mass_Function"

16 "~~/src/HOL/Library/Multiset_Permutations"

17 begin

19 text \<open>

20 Choosing a set permutation (i.e. a distinct list with the same elements as the set)

21 uniformly at random is the same as first choosing the first element of the list

22 and then choosing the rest of the list as a permutation of the remaining set.

23 \<close>

24 lemma random_permutation_of_set:

25 assumes "finite A" "A \<noteq> {}"

26 shows "pmf_of_set (permutations_of_set A) =

27 do {

28 x \<leftarrow> pmf_of_set A;

29 xs \<leftarrow> pmf_of_set (permutations_of_set (A - {x}));

30 return_pmf (x#xs)

31 }" (is "?lhs = ?rhs")

32 proof -

33 from assms have "permutations_of_set A = (\<Union>x\<in>A. op # x ` permutations_of_set (A - {x}))"

34 by (simp add: permutations_of_set_nonempty)

35 also from assms have "pmf_of_set \<dots> = ?rhs"

36 by (subst pmf_of_set_UN[where n = "fact (card A - 1)"])

37 (auto simp: card_image disjoint_family_on_def map_pmf_def [symmetric] map_pmf_of_set_inj)

38 finally show ?thesis .

39 qed

42 text \<open>

43 A generic fold function that takes a function, an initial state, and a set

44 and chooses a random order in which it then traverses the set in the same

45 fashion as a left fold over a list.

46 We first give a recursive definition.

47 \<close>

48 function fold_random_permutation :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'b \<Rightarrow> 'a set \<Rightarrow> 'b pmf" where

49 "fold_random_permutation f x {} = return_pmf x"

50 | "\<not>finite A \<Longrightarrow> fold_random_permutation f x A = return_pmf x"

51 | "finite A \<Longrightarrow> A \<noteq> {} \<Longrightarrow>

52 fold_random_permutation f x A =

53 pmf_of_set A \<bind> (\<lambda>a. fold_random_permutation f (f a x) (A - {a}))"

54 by (force, simp_all)

55 termination proof (relation "Wellfounded.measure (\<lambda>(_,_,A). card A)")

56 fix A :: "'a set" and f :: "'a \<Rightarrow> 'b \<Rightarrow> 'b" and x :: 'b and y :: 'a

57 assume A: "finite A" "A \<noteq> {}" "y \<in> set_pmf (pmf_of_set A)"

58 then have "card A > 0" by (simp add: card_gt_0_iff)

59 with A show "((f, f y x, A - {y}), f, x, A) \<in> Wellfounded.measure (\<lambda>(_, _, A). card A)"

60 by simp

61 qed simp_all

64 text \<open>

65 We can now show that the above recursive definition is equivalent to

66 choosing a random set permutation and folding over it (in any direction).

67 \<close>

68 lemma fold_random_permutation_foldl:

69 assumes "finite A"

70 shows "fold_random_permutation f x A =

71 map_pmf (foldl (\<lambda>x y. f y x) x) (pmf_of_set (permutations_of_set A))"

72 using assms

73 proof (induction f x A rule: fold_random_permutation.induct [case_names empty infinite remove])

74 case (remove A f x)

75 from remove

76 have "fold_random_permutation f x A =

77 pmf_of_set A \<bind> (\<lambda>a. fold_random_permutation f (f a x) (A - {a}))" by simp

78 also from remove

79 have "\<dots> = pmf_of_set A \<bind> (\<lambda>a. map_pmf (foldl (\<lambda>x y. f y x) x)

80 (map_pmf (op # a) (pmf_of_set (permutations_of_set (A - {a})))))"

81 by (intro bind_pmf_cong) (simp_all add: pmf.map_comp o_def)

82 also from remove have "\<dots> = map_pmf (foldl (\<lambda>x y. f y x) x) (pmf_of_set (permutations_of_set A))"

83 by (simp_all add: random_permutation_of_set map_bind_pmf map_pmf_def [symmetric])

84 finally show ?case .

85 qed (simp_all add: pmf_of_set_singleton)

87 lemma fold_random_permutation_foldr:

88 assumes "finite A"

89 shows "fold_random_permutation f x A =

90 map_pmf (\<lambda>xs. foldr f xs x) (pmf_of_set (permutations_of_set A))"

91 proof -

92 have "fold_random_permutation f x A =

93 map_pmf (foldl (\<lambda>x y. f y x) x \<circ> rev) (pmf_of_set (permutations_of_set A))"

94 using assms by (subst fold_random_permutation_foldl [OF assms])

95 (simp_all add: pmf.map_comp [symmetric] map_pmf_of_set_inj)

96 also have "foldl (\<lambda>x y. f y x) x \<circ> rev = (\<lambda>xs. foldr f xs x)"

97 by (intro ext) (simp add: foldl_conv_foldr)

98 finally show ?thesis .

99 qed

101 lemma fold_random_permutation_fold:

102 assumes "finite A"

103 shows "fold_random_permutation f x A =

104 map_pmf (\<lambda>xs. fold f xs x) (pmf_of_set (permutations_of_set A))"

105 by (subst fold_random_permutation_foldl [OF assms], intro map_pmf_cong)

106 (simp_all add: foldl_conv_fold)

108 lemma fold_random_permutation_code [code]:

109 "fold_random_permutation f x (set xs) =

110 map_pmf (foldl (\<lambda>x y. f y x) x) (pmf_of_set (permutations_of_set (set xs)))"

111 by (simp add: fold_random_permutation_foldl)

113 text \<open>

114 We now introduce a slightly generalised version of the above fold

115 operation that does not simply return the result in the end, but applies

116 a monadic bind to it.

117 This may seem somewhat arbitrary, but it is a common use case, e.g.

118 in the Social Decision Scheme of Random Serial Dictatorship, where

119 voters narrow down a set of possible winners in a random order and

120 the winner is chosen from the remaining set uniformly at random.

121 \<close>

122 function fold_bind_random_permutation

123 :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> ('b \<Rightarrow> 'c pmf) \<Rightarrow> 'b \<Rightarrow> 'a set \<Rightarrow> 'c pmf" where

124 "fold_bind_random_permutation f g x {} = g x"

125 | "\<not>finite A \<Longrightarrow> fold_bind_random_permutation f g x A = g x"

126 | "finite A \<Longrightarrow> A \<noteq> {} \<Longrightarrow>

127 fold_bind_random_permutation f g x A =

128 pmf_of_set A \<bind> (\<lambda>a. fold_bind_random_permutation f g (f a x) (A - {a}))"

129 by (force, simp_all)

130 termination proof (relation "Wellfounded.measure (\<lambda>(_,_,_,A). card A)")

131 fix A :: "'a set" and f :: "'a \<Rightarrow> 'b \<Rightarrow> 'b" and x :: 'b

132 and y :: 'a and g :: "'b \<Rightarrow> 'c pmf"

133 assume A: "finite A" "A \<noteq> {}" "y \<in> set_pmf (pmf_of_set A)"

134 then have "card A > 0" by (simp add: card_gt_0_iff)

135 with A show "((f, g, f y x, A - {y}), f, g, x, A) \<in> Wellfounded.measure (\<lambda>(_, _, _, A). card A)"

136 by simp

137 qed simp_all

139 text \<open>

140 We now show that the recursive definition is equivalent to

141 a random fold followed by a monadic bind.

142 \<close>

143 lemma fold_bind_random_permutation_altdef [code]:

144 "fold_bind_random_permutation f g x A = fold_random_permutation f x A \<bind> g"

145 proof (induction f x A rule: fold_random_permutation.induct [case_names empty infinite remove])

146 case (remove A f x)

147 from remove have "pmf_of_set A \<bind> (\<lambda>a. fold_bind_random_permutation f g (f a x) (A - {a})) =

148 pmf_of_set A \<bind> (\<lambda>a. fold_random_permutation f (f a x) (A - {a}) \<bind> g)"

149 by (intro bind_pmf_cong) simp_all

150 with remove show ?case by (simp add: bind_return_pmf bind_assoc_pmf)

151 qed (simp_all add: bind_return_pmf)

154 text \<open>

155 We can now derive the following nice monadic representations of the

156 combined fold-and-bind:

157 \<close>

158 lemma fold_bind_random_permutation_foldl:

159 assumes "finite A"

160 shows "fold_bind_random_permutation f g x A =

161 do {xs \<leftarrow> pmf_of_set (permutations_of_set A); g (foldl (\<lambda>x y. f y x) x xs)}"

162 using assms by (simp add: fold_bind_random_permutation_altdef bind_assoc_pmf

163 fold_random_permutation_foldl bind_return_pmf map_pmf_def)

165 lemma fold_bind_random_permutation_foldr:

166 assumes "finite A"

167 shows "fold_bind_random_permutation f g x A =

168 do {xs \<leftarrow> pmf_of_set (permutations_of_set A); g (foldr f xs x)}"

169 using assms by (simp add: fold_bind_random_permutation_altdef bind_assoc_pmf

170 fold_random_permutation_foldr bind_return_pmf map_pmf_def)

172 lemma fold_bind_random_permutation_fold:

173 assumes "finite A"

174 shows "fold_bind_random_permutation f g x A =

175 do {xs \<leftarrow> pmf_of_set (permutations_of_set A); g (fold f xs x)}"

176 using assms by (simp add: fold_bind_random_permutation_altdef bind_assoc_pmf

177 fold_random_permutation_fold bind_return_pmf map_pmf_def)

179 text \<open>

180 The following useful lemma allows us to swap partitioning a set w.\,r.\,t.\ a

181 predicate and drawing a random permutation of that set.

182 \<close>

183 lemma partition_random_permutations:

184 assumes "finite A"

185 shows "map_pmf (partition P) (pmf_of_set (permutations_of_set A)) =

186 pair_pmf (pmf_of_set (permutations_of_set {x\<in>A. P x}))

187 (pmf_of_set (permutations_of_set {x\<in>A. \<not>P x}))" (is "?lhs = ?rhs")

188 proof (rule pmf_eqI, clarify, goal_cases)

189 case (1 xs ys)

190 show ?case

191 proof (cases "xs \<in> permutations_of_set {x\<in>A. P x} \<and> ys \<in> permutations_of_set {x\<in>A. \<not>P x}")

192 case True

193 let ?n1 = "card {x\<in>A. P x}" and ?n2 = "card {x\<in>A. \<not>P x}"

194 have card_eq: "card A = ?n1 + ?n2"

195 proof -

196 have "?n1 + ?n2 = card ({x\<in>A. P x} \<union> {x\<in>A. \<not>P x})"

197 using assms by (intro card_Un_disjoint [symmetric]) auto

198 also have "{x\<in>A. P x} \<union> {x\<in>A. \<not>P x} = A" by blast

199 finally show ?thesis ..

200 qed

202 from True have lengths [simp]: "length xs = ?n1" "length ys = ?n2"

203 by (auto intro!: length_finite_permutations_of_set)

204 have "pmf ?lhs (xs, ys) =

205 real (card (permutations_of_set A \<inter> partition P -` {(xs, ys)})) / fact (card A)"

206 using assms by (auto simp: pmf_map measure_pmf_of_set)

207 also have "partition P -` {(xs, ys)} = shuffle xs ys"

208 using True by (intro inv_image_partition) (auto simp: permutations_of_set_def)

209 also have "permutations_of_set A \<inter> shuffle xs ys = shuffle xs ys"

210 using True distinct_disjoint_shuffle[of xs ys]

211 by (auto simp: permutations_of_set_def dest: set_shuffle)

212 also have "card (shuffle xs ys) = length xs + length ys choose length xs"

213 using True by (intro card_disjoint_shuffle) (auto simp: permutations_of_set_def)

214 also have "length xs + length ys = card A" by (simp add: card_eq)

215 also have "real (card A choose length xs) = fact (card A) / (fact ?n1 * fact (card A - ?n1))"

216 by (subst binomial_fact) (auto intro!: card_mono assms)

217 also have "\<dots> / fact (card A) = 1 / (fact ?n1 * fact ?n2)"

218 by (simp add: divide_simps card_eq)

219 also have "\<dots> = pmf ?rhs (xs, ys)" using True assms by (simp add: pmf_pair)

220 finally show ?thesis .

221 next

222 case False

223 hence *: "xs \<notin> permutations_of_set {x\<in>A. P x} \<or> ys \<notin> permutations_of_set {x\<in>A. \<not>P x}" by blast

224 hence eq: "permutations_of_set A \<inter> (partition P -` {(xs, ys)}) = {}"

225 by (auto simp: o_def permutations_of_set_def)

226 from * show ?thesis

227 by (elim disjE) (insert assms eq, simp_all add: pmf_pair pmf_map measure_pmf_of_set)

228 qed

229 qed

231 end