src/HOL/Probability/Random_Permutations.thy
author eberlm <eberlm@in.tum.de>
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