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