src/HOL/Probability/Random_Permutations.thy
 author eberlm Tue Apr 04 08:57:21 2017 +0200 (2017-04-04) changeset 65395 7504569a73c7 parent 63965 d510b816ea41 child 66453 cc19f7ca2ed6 permissions -rw-r--r--
moved material from AFP to distribution
```     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
```
```    15   "~~/src/HOL/Probability/Probability_Mass_Function"
```
```    16   "~~/src/HOL/Library/Multiset_Permutations"
```
```    17 begin
```
```    18
```
```    19 text \<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>
```
```    24 lemma 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")
```
```    32 proof -
```
```    33   from assms have "permutations_of_set A = (\<Union>x\<in>A. op # 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 .
```
```    39 qed
```
```    40
```
```    41
```
```    42 text \<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>
```
```    48 function 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}))"
```
```    54 by (force, simp_all)
```
```    55 termination 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
```
```    61 qed simp_all
```
```    62
```
```    63
```
```    64 text \<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>
```
```    68 lemma 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))"
```
```    72 using assms
```
```    73 proof (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 (op # 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 .
```
```    85 qed (simp_all add: pmf_of_set_singleton)
```
```    86
```
```    87 lemma 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))"
```
```    91 proof -
```
```    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 .
```
```    99 qed
```
```   100
```
```   101 lemma 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
```
```   108 lemma 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
```
```   113 text \<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>
```
```   122 function 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}))"
```
```   129 by (force, simp_all)
```
```   130 termination 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
```
```   137 qed simp_all
```
```   138
```
```   139 text \<open>
```
```   140   We now show that the recursive definition is equivalent to
```
```   141   a random fold followed by a monadic bind.
```
```   142 \<close>
```
```   143 lemma fold_bind_random_permutation_altdef [code]:
```
```   144   "fold_bind_random_permutation f g x A = fold_random_permutation f x A \<bind> g"
```
```   145 proof (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)
```
```   151 qed (simp_all add: bind_return_pmf)
```
```   152
```
```   153
```
```   154 text \<open>
```
```   155   We can now derive the following nice monadic representations of the
```
```   156   combined fold-and-bind:
```
```   157 \<close>
```
```   158 lemma 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
```
```   165 lemma 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
```
```   172 lemma 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
```
```   179 text \<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>
```
```   183 lemma 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")
```
```   188 proof (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)} = shuffle xs ys"
```
```   208       using True by (intro inv_image_partition) (auto simp: permutations_of_set_def)
```
```   209     also have "permutations_of_set A \<inter> shuffle xs ys = shuffle xs ys"
```
```   210       using True distinct_disjoint_shuffle[of xs ys]
```
```   211       by (auto simp: permutations_of_set_def dest: set_shuffle)
```
```   212     also have "card (shuffle xs ys) = length xs + length ys choose length xs"
```
```   213       using True by (intro card_disjoint_shuffle) (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: divide_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
```
```   229 qed
```
```   230
```
```   231 end
```