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