summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | paulson <lp15@cam.ac.uk> |

Tue, 24 May 2016 15:16:15 +0100 | |

changeset 63131 | 76cb6c6bd7b8 |

parent 63130 | 4ae5da02d627 (current diff) |

parent 63124 | 6a17bcddd6c2 (diff) |

child 63132 | 8230358fab88 |

Merge

--- a/src/HOL/Library/Library.thy Tue May 24 15:08:33 2016 +0100 +++ b/src/HOL/Library/Library.thy Tue May 24 15:16:15 2016 +0100 @@ -72,6 +72,7 @@ Reflection Saturated Set_Algebras + Set_Permutations State_Monad Stirling Stream

--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Library/Set_Permutations.thy Tue May 24 15:16:15 2016 +0100 @@ -0,0 +1,250 @@ +(* + Title: Set_Permutations.thy + Author: Manuel Eberl, TU München + + The set of permutations of a finite set, i.e. the set of all + lists that contain every element of the set once. +*) + +section \<open>Set Permutations\<close> + +theory Set_Permutations +imports + Complex_Main + "~~/src/HOL/Library/Disjoint_Sets" + "~~/src/HOL/Library/Permutations" +begin + +subsection \<open>Definition and general facts\<close> + +definition permutations_of_set :: "'a set \<Rightarrow> 'a list set" where + "permutations_of_set A = {xs. set xs = A \<and> distinct xs}" + +lemma permutations_of_setI [intro]: + assumes "set xs = A" "distinct xs" + shows "xs \<in> permutations_of_set A" + using assms unfolding permutations_of_set_def by simp + +lemma permutations_of_setD: + assumes "xs \<in> permutations_of_set A" + shows "set xs = A" "distinct xs" + using assms unfolding permutations_of_set_def by simp_all + +lemma permutations_of_set_lists: "permutations_of_set A \<subseteq> lists A" + unfolding permutations_of_set_def by auto + +lemma permutations_of_set_empty [simp]: "permutations_of_set {} = {[]}" + by (auto simp: permutations_of_set_def) + +lemma UN_set_permutations_of_set [simp]: + "finite A \<Longrightarrow> (\<Union>xs\<in>permutations_of_set A. set xs) = A" + using finite_distinct_list by (auto simp: permutations_of_set_def) + +lemma permutations_of_set_nonempty: + assumes "A \<noteq> {}" + shows "permutations_of_set A = + (\<Union>x\<in>A. (\<lambda>xs. x # xs) ` permutations_of_set (A - {x}))" (is "?lhs = ?rhs") +proof (intro equalityI subsetI) + fix ys assume ys: "ys \<in> permutations_of_set A" + with assms have "ys \<noteq> []" by (auto simp: permutations_of_set_def) + then obtain x xs where xs: "ys = x # xs" by (cases ys) simp_all + from xs ys have "x \<in> A" "xs \<in> permutations_of_set (A - {x})" + by (auto simp: permutations_of_set_def) + with xs show "ys \<in> ?rhs" by auto +next + fix ys assume ys: "ys \<in> ?rhs" + then obtain x xs where xs: "ys = x # xs" "x \<in> A" "xs \<in> permutations_of_set (A - {x})" + by auto + with ys show "ys \<in> ?lhs" by (auto simp: permutations_of_set_def) +qed + +lemma permutations_of_set_singleton [simp]: "permutations_of_set {x} = {[x]}" + by (subst permutations_of_set_nonempty) auto + +lemma permutations_of_set_doubleton: + "x \<noteq> y \<Longrightarrow> permutations_of_set {x,y} = {[x,y], [y,x]}" + by (subst permutations_of_set_nonempty) + (simp_all add: insert_Diff_if insert_commute) + +lemma rev_permutations_of_set [simp]: + "rev ` permutations_of_set A = permutations_of_set A" +proof + have "rev ` rev ` permutations_of_set A \<subseteq> rev ` permutations_of_set A" + unfolding permutations_of_set_def by auto + also have "rev ` rev ` permutations_of_set A = permutations_of_set A" + by (simp add: image_image) + finally show "permutations_of_set A \<subseteq> rev ` permutations_of_set A" . +next + show "rev ` permutations_of_set A \<subseteq> permutations_of_set A" + unfolding permutations_of_set_def by auto +qed + +lemma length_finite_permutations_of_set: + "xs \<in> permutations_of_set A \<Longrightarrow> length xs = card A" + by (auto simp: permutations_of_set_def distinct_card) + +lemma permutations_of_set_infinite: + "\<not>finite A \<Longrightarrow> permutations_of_set A = {}" + by (auto simp: permutations_of_set_def) + +lemma finite_permutations_of_set [simp]: "finite (permutations_of_set A)" +proof (cases "finite A") + assume fin: "finite A" + have "permutations_of_set A \<subseteq> {xs. set xs \<subseteq> A \<and> length xs = card A}" + unfolding permutations_of_set_def by (auto simp: distinct_card) + moreover from fin have "finite \<dots>" using finite_lists_length_eq by blast + ultimately show ?thesis by (rule finite_subset) +qed (simp_all add: permutations_of_set_infinite) + +lemma permutations_of_set_empty_iff [simp]: + "permutations_of_set A = {} \<longleftrightarrow> \<not>finite A" + unfolding permutations_of_set_def using finite_distinct_list[of A] by auto + +lemma card_permutations_of_set [simp]: + "finite A \<Longrightarrow> card (permutations_of_set A) = fact (card A)" +proof (induction A rule: finite_remove_induct) + case (remove A) + hence "card (permutations_of_set A) = + card (\<Union>x\<in>A. op # x ` permutations_of_set (A - {x}))" + by (simp add: permutations_of_set_nonempty) + also from remove.hyps have "\<dots> = (\<Sum>i\<in>A. card (op # i ` permutations_of_set (A - {i})))" + by (intro card_UN_disjoint) auto + also have "\<dots> = (\<Sum>i\<in>A. card (permutations_of_set (A - {i})))" + by (intro setsum.cong) (simp_all add: card_image) + also from remove have "\<dots> = card A * fact (card A - 1)" by simp + also from remove.hyps have "\<dots> = fact (card A)" + by (cases "card A") simp_all + finally show ?case . +qed simp_all + +lemma permutations_of_set_image_inj: + assumes inj: "inj_on f A" + shows "permutations_of_set (f ` A) = map f ` permutations_of_set A" +proof (cases "finite A") + assume "\<not>finite A" + with inj show ?thesis + by (auto simp add: permutations_of_set_infinite dest: finite_imageD) +next + assume finite: "finite A" + show ?thesis + proof (rule sym, rule card_seteq) + from inj show "map f ` permutations_of_set A \<subseteq> permutations_of_set (f ` A)" + by (auto simp: permutations_of_set_def distinct_map) + + from inj have "card (map f ` permutations_of_set A) = card (permutations_of_set A)" + by (intro card_image inj_on_mapI) (auto simp: permutations_of_set_def) + also from finite inj have "\<dots> = card (permutations_of_set (f ` A))" + by (simp add: card_image) + finally show "card (permutations_of_set (f ` A)) \<le> + card (map f ` permutations_of_set A)" by simp + qed simp_all +qed + +lemma permutations_of_set_image_permutes: + "\<sigma> permutes A \<Longrightarrow> map \<sigma> ` permutations_of_set A = permutations_of_set A" + by (subst permutations_of_set_image_inj [symmetric]) + (simp_all add: permutes_inj_on permutes_image) + + +subsection \<open>Code generation\<close> + +text \<open> + We define an auxiliary version with an accumulator to avoid + having to map over the results. +\<close> +function permutations_of_set_aux where + "permutations_of_set_aux acc A = + (if \<not>finite A then {} else if A = {} then {acc} else + (\<Union>x\<in>A. permutations_of_set_aux (x#acc) (A - {x})))" +by auto +termination by (relation "Wellfounded.measure (card \<circ> snd)") (simp_all add: card_gt_0_iff) + +lemma permutations_of_set_aux_altdef: + "permutations_of_set_aux acc A = (\<lambda>xs. rev xs @ acc) ` permutations_of_set A" +proof (cases "finite A") + assume "finite A" + thus ?thesis + proof (induction A arbitrary: acc rule: finite_psubset_induct) + case (psubset A acc) + show ?case + proof (cases "A = {}") + case False + note [simp del] = permutations_of_set_aux.simps + from psubset.hyps False + have "permutations_of_set_aux acc A = + (\<Union>y\<in>A. permutations_of_set_aux (y#acc) (A - {y}))" + by (subst permutations_of_set_aux.simps) simp_all + also have "\<dots> = (\<Union>y\<in>A. (\<lambda>xs. rev xs @ acc) ` (\<lambda>xs. y # xs) ` permutations_of_set (A - {y}))" + by (intro SUP_cong refl, subst psubset) (auto simp: image_image) + also from False have "\<dots> = (\<lambda>xs. rev xs @ acc) ` permutations_of_set A" + by (subst (2) permutations_of_set_nonempty) (simp_all add: image_UN) + finally show ?thesis . + qed simp_all + qed +qed (simp_all add: permutations_of_set_infinite) + +declare permutations_of_set_aux.simps [simp del] + +lemma permutations_of_set_aux_correct: + "permutations_of_set_aux [] A = permutations_of_set A" + by (simp add: permutations_of_set_aux_altdef) + + +text \<open> + In another refinement step, we define a version on lists. +\<close> +declare length_remove1 [termination_simp] + +fun permutations_of_set_aux_list where + "permutations_of_set_aux_list acc xs = + (if xs = [] then [acc] else + List.bind xs (\<lambda>x. permutations_of_set_aux_list (x#acc) (List.remove1 x xs)))" + +definition permutations_of_set_list where + "permutations_of_set_list xs = permutations_of_set_aux_list [] xs" + +declare permutations_of_set_aux_list.simps [simp del] + +lemma permutations_of_set_aux_list_refine: + assumes "distinct xs" + shows "set (permutations_of_set_aux_list acc xs) = permutations_of_set_aux acc (set xs)" + using assms + by (induction acc xs rule: permutations_of_set_aux_list.induct) + (subst permutations_of_set_aux_list.simps, + subst permutations_of_set_aux.simps, + simp_all add: set_list_bind cong: SUP_cong) + + +text \<open> + The permutation lists contain no duplicates if the inputs contain no duplicates. + Therefore, these functions can easily be used when working with a representation of + sets by distinct lists. + The same approach should generalise to any kind of set implementation that supports + a monadic bind operation, and since the results are disjoint, merging should be cheap. +\<close> +lemma distinct_permutations_of_set_aux_list: + "distinct xs \<Longrightarrow> distinct (permutations_of_set_aux_list acc xs)" + by (induction acc xs rule: permutations_of_set_aux_list.induct) + (subst permutations_of_set_aux_list.simps, + auto intro!: distinct_list_bind simp: disjoint_family_on_def + permutations_of_set_aux_list_refine permutations_of_set_aux_altdef) + +lemma distinct_permutations_of_set_list: + "distinct xs \<Longrightarrow> distinct (permutations_of_set_list xs)" + by (simp add: permutations_of_set_list_def distinct_permutations_of_set_aux_list) + +lemma permutations_of_list: + "permutations_of_set (set xs) = set (permutations_of_set_list (remdups xs))" + by (simp add: permutations_of_set_aux_correct [symmetric] + permutations_of_set_aux_list_refine permutations_of_set_list_def) + +lemma permutations_of_list_code [code]: + "permutations_of_set (set xs) = set (permutations_of_set_list (remdups xs))" + "permutations_of_set (List.coset xs) = + Code.abort (STR ''Permutation of set complement not supported'') + (\<lambda>_. permutations_of_set (List.coset xs))" + by (simp_all add: permutations_of_list) + +value [code] "permutations_of_set (set ''abcd'')" + +end \ No newline at end of file

--- a/src/HOL/Probability/Probability.thy Tue May 24 15:08:33 2016 +0100 +++ b/src/HOL/Probability/Probability.thy Tue May 24 15:16:15 2016 +0100 @@ -9,6 +9,7 @@ Projective_Limit Probability_Mass_Function Stream_Space + Random_Permutations Embed_Measure Central_Limit_Theorem begin

--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Probability/Random_Permutations.thy Tue May 24 15:16:15 2016 +0100 @@ -0,0 +1,173 @@ +(* + Title: Random_Permutations.thy + Author: Manuel Eberl, TU München + + Random permutations and folding over them. + This provides the basic theory for the concept of doing something + in a random order, e.g. inserting elements from a fixed set into a + data structure in random order. +*) + +section \<open>Random Permutations\<close> + +theory Random_Permutations +imports "~~/src/HOL/Probability/Probability_Mass_Function" "~~/src/HOL/Library/Set_Permutations" +begin + +text \<open> + Choosing a set permutation (i.e. a distinct list with the same elements as the set) + uniformly at random is the same as first choosing the first element of the list + and then choosing the rest of the list as a permutation of the remaining set. +\<close> +lemma random_permutation_of_set: + assumes "finite A" "A \<noteq> {}" + shows "pmf_of_set (permutations_of_set A) = + do { + x \<leftarrow> pmf_of_set A; + xs \<leftarrow> pmf_of_set (permutations_of_set (A - {x})); + return_pmf (x#xs) + }" (is "?lhs = ?rhs") +proof - + from assms have "permutations_of_set A = (\<Union>x\<in>A. op # x ` permutations_of_set (A - {x}))" + by (simp add: permutations_of_set_nonempty) + also from assms have "pmf_of_set \<dots> = ?rhs" + by (subst pmf_of_set_UN[where n = "fact (card A - 1)"]) + (auto simp: card_image disjoint_family_on_def map_pmf_def [symmetric] map_pmf_of_set_inj) + finally show ?thesis . +qed + + +text \<open> + A generic fold function that takes a function, an initial state, and a set + and chooses a random order in which it then traverses the set in the same + fashion as a left-fold over a list. + We first give a recursive definition. +\<close> +function fold_random_permutation :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'b \<Rightarrow> 'a set \<Rightarrow> 'b pmf" where + "fold_random_permutation f x {} = return_pmf x" +| "\<not>finite A \<Longrightarrow> fold_random_permutation f x A = return_pmf x" +| "finite A \<Longrightarrow> A \<noteq> {} \<Longrightarrow> + fold_random_permutation f x A = + pmf_of_set A \<bind> (\<lambda>a. fold_random_permutation f (f a x) (A - {a}))" +by (force, simp_all) +termination proof (relation "Wellfounded.measure (\<lambda>(_,_,A). card A)") + fix A :: "'a set" and f :: "'a \<Rightarrow> 'b \<Rightarrow> 'b" and x :: 'b and y :: 'a + assume "finite A" "A \<noteq> {}" "y \<in> set_pmf (pmf_of_set A)" + moreover from this have "card A > 0" by (simp add: card_gt_0_iff) + ultimately show "((f, f y x, A - {y}), f, x, A) \<in> Wellfounded.measure (\<lambda>(_, _, A). card A)" + by simp +qed simp_all + + +text \<open> + We can now show that the above recursive definition is equivalent to + choosing a random set permutation and folding over it (in any direction). +\<close> +lemma fold_random_permutation_foldl: + assumes "finite A" + shows "fold_random_permutation f x A = + map_pmf (foldl (\<lambda>x y. f y x) x) (pmf_of_set (permutations_of_set A))" +using assms +proof (induction f x A rule: fold_random_permutation.induct [case_names empty infinite remove]) + case (remove A f x) + from remove + have "fold_random_permutation f x A = + pmf_of_set A \<bind> (\<lambda>a. fold_random_permutation f (f a x) (A - {a}))" by simp + also from remove + have "\<dots> = pmf_of_set A \<bind> (\<lambda>a. map_pmf (foldl (\<lambda>x y. f y x) x) + (map_pmf (op # a) (pmf_of_set (permutations_of_set (A - {a})))))" + by (intro bind_pmf_cong) (simp_all add: pmf.map_comp o_def) + also from remove have "\<dots> = map_pmf (foldl (\<lambda>x y. f y x) x) (pmf_of_set (permutations_of_set A))" + by (simp_all add: random_permutation_of_set map_bind_pmf map_pmf_def [symmetric]) + finally show ?case . +qed (simp_all add: pmf_of_set_singleton) + +lemma fold_random_permutation_foldr: + assumes "finite A" + shows "fold_random_permutation f x A = + map_pmf (\<lambda>xs. foldr f xs x) (pmf_of_set (permutations_of_set A))" +proof - + have "fold_random_permutation f x A = + map_pmf (foldl (\<lambda>x y. f y x) x \<circ> rev) (pmf_of_set (permutations_of_set A))" + using assms by (subst fold_random_permutation_foldl [OF assms]) + (simp_all add: pmf.map_comp [symmetric] map_pmf_of_set_inj) + also have "foldl (\<lambda>x y. f y x) x \<circ> rev = (\<lambda>xs. foldr f xs x)" + by (intro ext) (simp add: foldl_conv_foldr) + finally show ?thesis . +qed + +lemma fold_random_permutation_fold: + assumes "finite A" + shows "fold_random_permutation f x A = + map_pmf (\<lambda>xs. fold f xs x) (pmf_of_set (permutations_of_set A))" + by (subst fold_random_permutation_foldl [OF assms], intro map_pmf_cong) + (simp_all add: foldl_conv_fold) + + +text \<open> + We now introduce a slightly generalised version of the above fold + operation that does not simply return the result in the end, but applies + a monadic bind to it. + This may seem somewhat arbitrary, but it is a common use case, e.g. + in the Social Decision Scheme of Random Serial Dictatorship, where + voters narrow down a set of possible winners in a random order and + the winner is chosen from the remaining set uniformly at random. +\<close> +function fold_bind_random_permutation + :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> ('b \<Rightarrow> 'c pmf) \<Rightarrow> 'b \<Rightarrow> 'a set \<Rightarrow> 'c pmf" where + "fold_bind_random_permutation f g x {} = g x" +| "\<not>finite A \<Longrightarrow> fold_bind_random_permutation f g x A = g x" +| "finite A \<Longrightarrow> A \<noteq> {} \<Longrightarrow> + fold_bind_random_permutation f g x A = + pmf_of_set A \<bind> (\<lambda>a. fold_bind_random_permutation f g (f a x) (A - {a}))" +by (force, simp_all) +termination proof (relation "Wellfounded.measure (\<lambda>(_,_,_,A). card A)") + fix A :: "'a set" and f :: "'a \<Rightarrow> 'b \<Rightarrow> 'b" and x :: 'b + and y :: 'a and g :: "'b \<Rightarrow> 'c pmf" + assume "finite A" "A \<noteq> {}" "y \<in> set_pmf (pmf_of_set A)" + moreover from this have "card A > 0" by (simp add: card_gt_0_iff) + ultimately show "((f, g, f y x, A - {y}), f, g, x, A) \<in> Wellfounded.measure (\<lambda>(_, _, _, A). card A)" + by simp +qed simp_all + +text \<open> + We now show that the recursive definition is equivalent to + a random fold followed by a monadic bind. +\<close> +lemma fold_bind_random_permutation_altdef: + "fold_bind_random_permutation f g x A = fold_random_permutation f x A \<bind> g" +proof (induction f x A rule: fold_random_permutation.induct [case_names empty infinite remove]) + case (remove A f x) + from remove have "pmf_of_set A \<bind> (\<lambda>a. fold_bind_random_permutation f g (f a x) (A - {a})) = + pmf_of_set A \<bind> (\<lambda>a. fold_random_permutation f (f a x) (A - {a}) \<bind> g)" + by (intro bind_pmf_cong) simp_all + with remove show ?case by (simp add: bind_return_pmf bind_assoc_pmf) +qed (simp_all add: bind_return_pmf) + + +text \<open> + We can now derive the following nice monadic representations of the + combined fold-and-bind: +\<close> +lemma fold_bind_random_permutation_foldl: + assumes "finite A" + shows "fold_bind_random_permutation f g x A = + do {xs \<leftarrow> pmf_of_set (permutations_of_set A); g (foldl (\<lambda>x y. f y x) x xs)}" + using assms by (simp add: fold_bind_random_permutation_altdef bind_assoc_pmf + fold_random_permutation_foldl bind_return_pmf map_pmf_def) + +lemma fold_bind_random_permutation_foldr: + assumes "finite A" + shows "fold_bind_random_permutation f g x A = + do {xs \<leftarrow> pmf_of_set (permutations_of_set A); g (foldr f xs x)}" + using assms by (simp add: fold_bind_random_permutation_altdef bind_assoc_pmf + fold_random_permutation_foldr bind_return_pmf map_pmf_def) + +lemma fold_bind_random_permutation_fold: + assumes "finite A" + shows "fold_bind_random_permutation f g x A = + do {xs \<leftarrow> pmf_of_set (permutations_of_set A); g (fold f xs x)}" + using assms by (simp add: fold_bind_random_permutation_altdef bind_assoc_pmf + fold_random_permutation_fold bind_return_pmf map_pmf_def) + +end