summary |
shortlog |
changelog |
graph |
tags |
branches |
files |
changeset |
file |
revisions |
annotate |
diff |
raw

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