|
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 |
|
11 section \<open>Random Permutations\<close> |
|
12 |
|
13 theory Random_Permutations |
|
14 imports "~~/src/HOL/Probability/Probability" "~~/src/HOL/Library/Set_Permutations" |
|
15 begin |
|
16 |
|
17 text \<open> |
|
18 Choosing a set permutation (i.e. a distinct list with the same elements as the set) |
|
19 uniformly at random is the same as first choosing the first element of the list |
|
20 and then choosing the rest of the list as a permutation of the remaining set. |
|
21 \<close> |
|
22 lemma random_permutation_of_set: |
|
23 assumes "finite A" "A \<noteq> {}" |
|
24 shows "pmf_of_set (permutations_of_set A) = |
|
25 do { |
|
26 x \<leftarrow> pmf_of_set A; |
|
27 xs \<leftarrow> pmf_of_set (permutations_of_set (A - {x})); |
|
28 return_pmf (x#xs) |
|
29 }" (is "?lhs = ?rhs") |
|
30 proof - |
|
31 from assms have "permutations_of_set A = (\<Union>x\<in>A. op # x ` permutations_of_set (A - {x}))" |
|
32 by (simp add: permutations_of_set_nonempty) |
|
33 also from assms have "pmf_of_set \<dots> = ?rhs" |
|
34 by (subst pmf_of_set_UN[where n = "fact (card A - 1)"]) |
|
35 (auto simp: card_image disjoint_family_on_def map_pmf_def [symmetric] map_pmf_of_set_inj) |
|
36 finally show ?thesis . |
|
37 qed |
|
38 |
|
39 |
|
40 text \<open> |
|
41 A generic fold function that takes a function, an initial state, and a set |
|
42 and chooses a random order in which it then traverses the set in the same |
|
43 fashion as a left-fold over a list. |
|
44 We first give a recursive definition. |
|
45 \<close> |
|
46 function fold_random_permutation :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'b \<Rightarrow> 'a set \<Rightarrow> 'b pmf" where |
|
47 "fold_random_permutation f x {} = return_pmf x" |
|
48 | "\<not>finite A \<Longrightarrow> fold_random_permutation f x A = return_pmf x" |
|
49 | "finite A \<Longrightarrow> A \<noteq> {} \<Longrightarrow> |
|
50 fold_random_permutation f x A = |
|
51 pmf_of_set A \<bind> (\<lambda>a. fold_random_permutation f (f a x) (A - {a}))" |
|
52 by (force, simp_all) |
|
53 termination proof (relation "Wellfounded.measure (\<lambda>(_,_,A). card A)") |
|
54 fix A :: "'a set" and f :: "'a \<Rightarrow> 'b \<Rightarrow> 'b" and x :: 'b and y :: 'a |
|
55 assume "finite A" "A \<noteq> {}" "y \<in> set_pmf (pmf_of_set A)" |
|
56 moreover from this have "card A > 0" by (simp add: card_gt_0_iff) |
|
57 ultimately show "((f, f y x, A - {y}), f, x, A) \<in> Wellfounded.measure (\<lambda>(_, _, A). card A)" |
|
58 by simp |
|
59 qed simp_all |
|
60 |
|
61 |
|
62 text \<open> |
|
63 We can now show that the above recursive definition is equivalent to |
|
64 choosing a random set permutation and folding over it (in any direction). |
|
65 \<close> |
|
66 lemma fold_random_permutation_foldl: |
|
67 assumes "finite A" |
|
68 shows "fold_random_permutation f x A = |
|
69 map_pmf (foldl (\<lambda>x y. f y x) x) (pmf_of_set (permutations_of_set A))" |
|
70 using assms |
|
71 proof (induction f x A rule: fold_random_permutation.induct [case_names empty infinite remove]) |
|
72 case (remove A f x) |
|
73 from remove |
|
74 have "fold_random_permutation f x A = |
|
75 pmf_of_set A \<bind> (\<lambda>a. fold_random_permutation f (f a x) (A - {a}))" by simp |
|
76 also from remove |
|
77 have "\<dots> = pmf_of_set A \<bind> (\<lambda>a. map_pmf (foldl (\<lambda>x y. f y x) x) |
|
78 (map_pmf (op # a) (pmf_of_set (permutations_of_set (A - {a})))))" |
|
79 by (intro bind_pmf_cong) (simp_all add: pmf.map_comp o_def) |
|
80 also from remove have "\<dots> = map_pmf (foldl (\<lambda>x y. f y x) x) (pmf_of_set (permutations_of_set A))" |
|
81 by (simp_all add: random_permutation_of_set map_bind_pmf map_pmf_def [symmetric]) |
|
82 finally show ?case . |
|
83 qed (simp_all add: pmf_of_set_singleton) |
|
84 |
|
85 lemma fold_random_permutation_foldr: |
|
86 assumes "finite A" |
|
87 shows "fold_random_permutation f x A = |
|
88 map_pmf (\<lambda>xs. foldr f xs x) (pmf_of_set (permutations_of_set A))" |
|
89 proof - |
|
90 have "fold_random_permutation f x A = |
|
91 map_pmf (foldl (\<lambda>x y. f y x) x \<circ> rev) (pmf_of_set (permutations_of_set A))" |
|
92 using assms by (subst fold_random_permutation_foldl [OF assms]) |
|
93 (simp_all add: pmf.map_comp [symmetric] map_pmf_of_set_inj) |
|
94 also have "foldl (\<lambda>x y. f y x) x \<circ> rev = (\<lambda>xs. foldr f xs x)" |
|
95 by (intro ext) (simp add: foldl_conv_foldr) |
|
96 finally show ?thesis . |
|
97 qed |
|
98 |
|
99 lemma fold_random_permutation_fold: |
|
100 assumes "finite A" |
|
101 shows "fold_random_permutation f x A = |
|
102 map_pmf (\<lambda>xs. fold f xs x) (pmf_of_set (permutations_of_set A))" |
|
103 by (subst fold_random_permutation_foldl [OF assms], intro map_pmf_cong) |
|
104 (simp_all add: foldl_conv_fold) |
|
105 |
|
106 |
|
107 text \<open> |
|
108 We now introduce a slightly generalised version of the above fold |
|
109 operation that does not simply return the result in the end, but applies |
|
110 a monadic bind to it. |
|
111 This may seem somewhat arbitrary, but it is a common use case, e.g. |
|
112 in the Social Decision Scheme of Random Serial Dictatorship, where |
|
113 voters narrow down a set of possible winners in a random order and |
|
114 the winner is chosen from the remaining set uniformly at random. |
|
115 \<close> |
|
116 function fold_bind_random_permutation |
|
117 :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> ('b \<Rightarrow> 'c pmf) \<Rightarrow> 'b \<Rightarrow> 'a set \<Rightarrow> 'c pmf" where |
|
118 "fold_bind_random_permutation f g x {} = g x" |
|
119 | "\<not>finite A \<Longrightarrow> fold_bind_random_permutation f g x A = g x" |
|
120 | "finite A \<Longrightarrow> A \<noteq> {} \<Longrightarrow> |
|
121 fold_bind_random_permutation f g x A = |
|
122 pmf_of_set A \<bind> (\<lambda>a. fold_bind_random_permutation f g (f a x) (A - {a}))" |
|
123 by (force, simp_all) |
|
124 termination proof (relation "Wellfounded.measure (\<lambda>(_,_,_,A). card A)") |
|
125 fix A :: "'a set" and f :: "'a \<Rightarrow> 'b \<Rightarrow> 'b" and x :: 'b |
|
126 and y :: 'a and g :: "'b \<Rightarrow> 'c pmf" |
|
127 assume "finite A" "A \<noteq> {}" "y \<in> set_pmf (pmf_of_set A)" |
|
128 moreover from this have "card A > 0" by (simp add: card_gt_0_iff) |
|
129 ultimately show "((f, g, f y x, A - {y}), f, g, x, A) \<in> Wellfounded.measure (\<lambda>(_, _, _, A). card A)" |
|
130 by simp |
|
131 qed simp_all |
|
132 |
|
133 text \<open> |
|
134 We now show that the recursive definition is equivalent to |
|
135 a random fold followed by a monadic bind. |
|
136 \<close> |
|
137 lemma fold_bind_random_permutation_altdef: |
|
138 "fold_bind_random_permutation f g x A = fold_random_permutation f x A \<bind> g" |
|
139 proof (induction f x A rule: fold_random_permutation.induct [case_names empty infinite remove]) |
|
140 case (remove A f x) |
|
141 from remove have "pmf_of_set A \<bind> (\<lambda>a. fold_bind_random_permutation f g (f a x) (A - {a})) = |
|
142 pmf_of_set A \<bind> (\<lambda>a. fold_random_permutation f (f a x) (A - {a}) \<bind> g)" |
|
143 by (intro bind_pmf_cong) simp_all |
|
144 with remove show ?case by (simp add: bind_return_pmf bind_assoc_pmf) |
|
145 qed (simp_all add: bind_return_pmf) |
|
146 |
|
147 |
|
148 text \<open> |
|
149 We can now derive the following nice monadic representations of the |
|
150 combined fold-and-bind: |
|
151 \<close> |
|
152 lemma fold_bind_random_permutation_foldl: |
|
153 assumes "finite A" |
|
154 shows "fold_bind_random_permutation f g x A = |
|
155 do {xs \<leftarrow> pmf_of_set (permutations_of_set A); g (foldl (\<lambda>x y. f y x) x xs)}" |
|
156 using assms by (simp add: fold_bind_random_permutation_altdef bind_assoc_pmf |
|
157 fold_random_permutation_foldl bind_return_pmf map_pmf_def) |
|
158 |
|
159 lemma fold_bind_random_permutation_foldr: |
|
160 assumes "finite A" |
|
161 shows "fold_bind_random_permutation f g x A = |
|
162 do {xs \<leftarrow> pmf_of_set (permutations_of_set A); g (foldr f xs x)}" |
|
163 using assms by (simp add: fold_bind_random_permutation_altdef bind_assoc_pmf |
|
164 fold_random_permutation_foldr bind_return_pmf map_pmf_def) |
|
165 |
|
166 lemma fold_bind_random_permutation_fold: |
|
167 assumes "finite A" |
|
168 shows "fold_bind_random_permutation f g x A = |
|
169 do {xs \<leftarrow> pmf_of_set (permutations_of_set A); g (fold f xs x)}" |
|
170 using assms by (simp add: fold_bind_random_permutation_altdef bind_assoc_pmf |
|
171 fold_random_permutation_fold bind_return_pmf map_pmf_def) |
|
172 |
|
173 end |