src/HOL/Probability/Random_Permutations.thy
 changeset 65395 7504569a73c7 parent 63965 d510b816ea41 child 66453 cc19f7ca2ed6
```     1.1 --- a/src/HOL/Probability/Random_Permutations.thy	Mon Apr 03 22:18:56 2017 +0200
1.2 +++ b/src/HOL/Probability/Random_Permutations.thy	Tue Apr 04 08:57:21 2017 +0200
1.3 @@ -176,4 +176,56 @@
1.4    using assms by (simp add: fold_bind_random_permutation_altdef bind_assoc_pmf
1.5                              fold_random_permutation_fold bind_return_pmf map_pmf_def)
1.6
1.7 +text \<open>
1.8 +  The following useful lemma allows us to swap partitioning a set w.\,r.\,t.\ a
1.9 +  predicate and drawing a random permutation of that set.
1.10 +\<close>
1.11 +lemma partition_random_permutations:
1.12 +  assumes "finite A"
1.13 +  shows   "map_pmf (partition P) (pmf_of_set (permutations_of_set A)) =
1.14 +             pair_pmf (pmf_of_set (permutations_of_set {x\<in>A. P x}))
1.15 +                      (pmf_of_set (permutations_of_set {x\<in>A. \<not>P x}))" (is "?lhs = ?rhs")
1.16 +proof (rule pmf_eqI, clarify, goal_cases)
1.17 +  case (1 xs ys)
1.18 +  show ?case
1.19 +  proof (cases "xs \<in> permutations_of_set {x\<in>A. P x} \<and> ys \<in> permutations_of_set {x\<in>A. \<not>P x}")
1.20 +    case True
1.21 +    let ?n1 = "card {x\<in>A. P x}" and ?n2 = "card {x\<in>A. \<not>P x}"
1.22 +    have card_eq: "card A = ?n1 + ?n2"
1.23 +    proof -
1.24 +      have "?n1 + ?n2 = card ({x\<in>A. P x} \<union> {x\<in>A. \<not>P x})"
1.25 +        using assms by (intro card_Un_disjoint [symmetric]) auto
1.26 +      also have "{x\<in>A. P x} \<union> {x\<in>A. \<not>P x} = A" by blast
1.27 +      finally show ?thesis ..
1.28 +    qed
1.29 +
1.30 +    from True have lengths [simp]: "length xs = ?n1" "length ys = ?n2"
1.31 +      by (auto intro!: length_finite_permutations_of_set)
1.32 +    have "pmf ?lhs (xs, ys) =
1.33 +            real (card (permutations_of_set A \<inter> partition P -` {(xs, ys)})) / fact (card A)"
1.34 +      using assms by (auto simp: pmf_map measure_pmf_of_set)
1.35 +    also have "partition P -` {(xs, ys)} = shuffle xs ys"
1.36 +      using True by (intro inv_image_partition) (auto simp: permutations_of_set_def)
1.37 +    also have "permutations_of_set A \<inter> shuffle xs ys = shuffle xs ys"
1.38 +      using True distinct_disjoint_shuffle[of xs ys]
1.39 +      by (auto simp: permutations_of_set_def dest: set_shuffle)
1.40 +    also have "card (shuffle xs ys) = length xs + length ys choose length xs"
1.41 +      using True by (intro card_disjoint_shuffle) (auto simp: permutations_of_set_def)
1.42 +    also have "length xs + length ys = card A" by (simp add: card_eq)
1.43 +    also have "real (card A choose length xs) = fact (card A) / (fact ?n1 * fact (card A - ?n1))"
1.44 +      by (subst binomial_fact) (auto intro!: card_mono assms)
1.45 +    also have "\<dots> / fact (card A) = 1 / (fact ?n1 * fact ?n2)"
1.46 +      by (simp add: divide_simps card_eq)
1.47 +    also have "\<dots> = pmf ?rhs (xs, ys)" using True assms by (simp add: pmf_pair)
1.48 +    finally show ?thesis .
1.49 +  next
1.50 +    case False
1.51 +    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
1.52 +    hence eq: "permutations_of_set A \<inter> (partition P -` {(xs, ys)}) = {}"
1.53 +      by (auto simp: o_def permutations_of_set_def)
1.54 +    from * show ?thesis
1.55 +      by (elim disjE) (insert assms eq, simp_all add: pmf_pair pmf_map measure_pmf_of_set)
1.56 +  qed
1.57 +qed
1.58 +
1.59  end
```