1(* 2 Title: Random_Permutations.thy 3 Author: Manuel Eberl, TU M��nchen 4 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*) 10 11section \<open>Random Permutations\<close> 12 13theory Random_Permutations 14imports 15 "~~/src/HOL/Probability/Probability_Mass_Function" 16 "HOL-Library.Multiset_Permutations" 17begin 18 19text \<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> 24lemma 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") 32proof - 33 from assms have "permutations_of_set A = (\<Union>x\<in>A. (#) 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 . 39qed 40 41 42text \<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> 48function 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}))" 54by (force, simp_all) 55termination 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 61qed simp_all 62 63 64text \<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> 68lemma 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))" 72using assms 73proof (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 ((#) 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 . 85qed (simp_all add: pmf_of_set_singleton) 86 87lemma 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))" 91proof - 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 . 99qed 100 101lemma 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) 107 108lemma 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) 112 113text \<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> 122function 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}))" 129by (force, simp_all) 130termination 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 137qed simp_all 138 139text \<open> 140 We now show that the recursive definition is equivalent to 141 a random fold followed by a monadic bind. 142\<close> 143lemma fold_bind_random_permutation_altdef [code]: 144 "fold_bind_random_permutation f g x A = fold_random_permutation f x A \<bind> g" 145proof (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) 151qed (simp_all add: bind_return_pmf) 152 153 154text \<open> 155 We can now derive the following nice monadic representations of the 156 combined fold-and-bind: 157\<close> 158lemma 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) 164 165lemma 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) 171 172lemma 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) 178 179text \<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> 183lemma 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") 188proof (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 201 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)} = shuffles xs ys" 208 using True by (intro inv_image_partition) (auto simp: permutations_of_set_def) 209 also have "permutations_of_set A \<inter> shuffles xs ys = shuffles xs ys" 210 using True distinct_disjoint_shuffles[of xs ys] 211 by (auto simp: permutations_of_set_def dest: set_shuffles) 212 also have "card (shuffles xs ys) = length xs + length ys choose length xs" 213 using True by (intro card_disjoint_shuffles) (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: field_split_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 229qed 230 231end 232