# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1464099375 -3600
# Node ID 76cb6c6bd7b80b3b98016a17486b7e105dd732a2
# Parent  4ae5da02d6278ddfac8ef602a9d742cab92c72fe# Parent  6a17bcddd6c2b71654851c696bd248d1cceb3b20
Merge

diff -r 4ae5da02d627 -r 76cb6c6bd7b8 src/HOL/Library/Library.thy
--- 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
diff -r 4ae5da02d627 -r 76cb6c6bd7b8 src/HOL/Library/Set_Permutations.thy
--- /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
diff -r 4ae5da02d627 -r 76cb6c6bd7b8 src/HOL/Probability/Probability.thy
--- 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
diff -r 4ae5da02d627 -r 76cb6c6bd7b8 src/HOL/Probability/Random_Permutations.thy
--- /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