author | eberlm |
Tue, 31 May 2016 13:02:44 +0200 | |
changeset 63194 | 0b7bdb75f451 |
parent 63134 | aa573306a9cd |
child 63539 | 70d4d9e5707b |
permissions | -rw-r--r-- |
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 |
|
63124 | 14 |
imports "~~/src/HOL/Probability/Probability_Mass_Function" "~~/src/HOL/Library/Set_Permutations" |
63122 | 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 |
|
63134
aa573306a9cd
Removed problematic code equation for set_permutations
eberlm
parents:
63133
diff
changeset
|
43 |
fashion as a left fold over a list. |
63122 | 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) |
|
63194 | 105 |
|
106 |
lemma fold_random_permutation_code [code]: |
|
107 |
"fold_random_permutation f x (set xs) = |
|
108 |
map_pmf (foldl (\<lambda>x y. f y x) x) (pmf_of_set (permutations_of_set (set xs)))" |
|
109 |
by (simp add: fold_random_permutation_foldl) |
|
63122 | 110 |
|
111 |
text \<open> |
|
112 |
We now introduce a slightly generalised version of the above fold |
|
113 |
operation that does not simply return the result in the end, but applies |
|
114 |
a monadic bind to it. |
|
115 |
This may seem somewhat arbitrary, but it is a common use case, e.g. |
|
116 |
in the Social Decision Scheme of Random Serial Dictatorship, where |
|
117 |
voters narrow down a set of possible winners in a random order and |
|
118 |
the winner is chosen from the remaining set uniformly at random. |
|
119 |
\<close> |
|
120 |
function fold_bind_random_permutation |
|
121 |
:: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> ('b \<Rightarrow> 'c pmf) \<Rightarrow> 'b \<Rightarrow> 'a set \<Rightarrow> 'c pmf" where |
|
122 |
"fold_bind_random_permutation f g x {} = g x" |
|
123 |
| "\<not>finite A \<Longrightarrow> fold_bind_random_permutation f g x A = g x" |
|
124 |
| "finite A \<Longrightarrow> A \<noteq> {} \<Longrightarrow> |
|
125 |
fold_bind_random_permutation f g x A = |
|
126 |
pmf_of_set A \<bind> (\<lambda>a. fold_bind_random_permutation f g (f a x) (A - {a}))" |
|
127 |
by (force, simp_all) |
|
128 |
termination proof (relation "Wellfounded.measure (\<lambda>(_,_,_,A). card A)") |
|
129 |
fix A :: "'a set" and f :: "'a \<Rightarrow> 'b \<Rightarrow> 'b" and x :: 'b |
|
130 |
and y :: 'a and g :: "'b \<Rightarrow> 'c pmf" |
|
131 |
assume "finite A" "A \<noteq> {}" "y \<in> set_pmf (pmf_of_set A)" |
|
132 |
moreover from this have "card A > 0" by (simp add: card_gt_0_iff) |
|
133 |
ultimately show "((f, g, f y x, A - {y}), f, g, x, A) \<in> Wellfounded.measure (\<lambda>(_, _, _, A). card A)" |
|
134 |
by simp |
|
135 |
qed simp_all |
|
136 |
||
137 |
text \<open> |
|
138 |
We now show that the recursive definition is equivalent to |
|
139 |
a random fold followed by a monadic bind. |
|
140 |
\<close> |
|
63194 | 141 |
lemma fold_bind_random_permutation_altdef [code]: |
63122 | 142 |
"fold_bind_random_permutation f g x A = fold_random_permutation f x A \<bind> g" |
143 |
proof (induction f x A rule: fold_random_permutation.induct [case_names empty infinite remove]) |
|
144 |
case (remove A f x) |
|
145 |
from remove have "pmf_of_set A \<bind> (\<lambda>a. fold_bind_random_permutation f g (f a x) (A - {a})) = |
|
146 |
pmf_of_set A \<bind> (\<lambda>a. fold_random_permutation f (f a x) (A - {a}) \<bind> g)" |
|
147 |
by (intro bind_pmf_cong) simp_all |
|
148 |
with remove show ?case by (simp add: bind_return_pmf bind_assoc_pmf) |
|
149 |
qed (simp_all add: bind_return_pmf) |
|
150 |
||
151 |
||
152 |
text \<open> |
|
153 |
We can now derive the following nice monadic representations of the |
|
154 |
combined fold-and-bind: |
|
155 |
\<close> |
|
156 |
lemma fold_bind_random_permutation_foldl: |
|
157 |
assumes "finite A" |
|
158 |
shows "fold_bind_random_permutation f g x A = |
|
159 |
do {xs \<leftarrow> pmf_of_set (permutations_of_set A); g (foldl (\<lambda>x y. f y x) x xs)}" |
|
160 |
using assms by (simp add: fold_bind_random_permutation_altdef bind_assoc_pmf |
|
161 |
fold_random_permutation_foldl bind_return_pmf map_pmf_def) |
|
162 |
||
163 |
lemma fold_bind_random_permutation_foldr: |
|
164 |
assumes "finite A" |
|
165 |
shows "fold_bind_random_permutation f g x A = |
|
166 |
do {xs \<leftarrow> pmf_of_set (permutations_of_set A); g (foldr f xs x)}" |
|
167 |
using assms by (simp add: fold_bind_random_permutation_altdef bind_assoc_pmf |
|
168 |
fold_random_permutation_foldr bind_return_pmf map_pmf_def) |
|
169 |
||
170 |
lemma fold_bind_random_permutation_fold: |
|
171 |
assumes "finite A" |
|
172 |
shows "fold_bind_random_permutation f g x A = |
|
173 |
do {xs \<leftarrow> pmf_of_set (permutations_of_set A); g (fold f xs x)}" |
|
174 |
using assms by (simp add: fold_bind_random_permutation_altdef bind_assoc_pmf |
|
175 |
fold_random_permutation_fold bind_return_pmf map_pmf_def) |
|
176 |
||
177 |
end |