63122
|
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
|