src/HOL/Library/Multiset_Permutations.thy
 author wenzelm Tue Apr 04 11:52:28 2017 +0200 (2017-04-04) changeset 65366 10ca63a18e56 parent 64272 f76b6dda2e56 child 67399 eab6ce8368fa permissions -rw-r--r--
proper imports;
 wenzelm@65366 ` 1` ```(* Title: HOL/Library/Multiset_Permutations.thy ``` wenzelm@65366 ` 2` ``` Author: Manuel Eberl (TU München) ``` eberlm@63965 ` 3` wenzelm@65366 ` 4` ```Defines the set of permutations of a given multiset (or set), i.e. the set of all lists whose ``` wenzelm@65366 ` 5` ```entries correspond to the multiset (resp. set). ``` eberlm@63965 ` 6` ```*) ``` wenzelm@65366 ` 7` eberlm@63965 ` 8` ```section \Permutations of a Multiset\ ``` wenzelm@65366 ` 9` eberlm@63965 ` 10` ```theory Multiset_Permutations ``` eberlm@63965 ` 11` ```imports ``` eberlm@63965 ` 12` ``` Complex_Main ``` wenzelm@65366 ` 13` ``` Multiset ``` wenzelm@65366 ` 14` ``` Permutations ``` eberlm@63965 ` 15` ```begin ``` eberlm@63965 ` 16` eberlm@63965 ` 17` ```(* TODO Move *) ``` eberlm@63965 ` 18` ```lemma mset_tl: "xs \ [] \ mset (tl xs) = mset xs - {#hd xs#}" ``` eberlm@63965 ` 19` ``` by (cases xs) simp_all ``` eberlm@63965 ` 20` eberlm@63965 ` 21` ```lemma mset_set_image_inj: ``` eberlm@63965 ` 22` ``` assumes "inj_on f A" ``` eberlm@63965 ` 23` ``` shows "mset_set (f ` A) = image_mset f (mset_set A)" ``` eberlm@63965 ` 24` ```proof (cases "finite A") ``` eberlm@63965 ` 25` ``` case True ``` eberlm@63965 ` 26` ``` from this and assms show ?thesis by (induction A) auto ``` eberlm@63965 ` 27` ```qed (insert assms, simp add: finite_image_iff) ``` eberlm@63965 ` 28` eberlm@63965 ` 29` ```lemma multiset_remove_induct [case_names empty remove]: ``` eberlm@63965 ` 30` ``` assumes "P {#}" "\A. A \ {#} \ (\x. x \# A \ P (A - {#x#})) \ P A" ``` eberlm@63965 ` 31` ``` shows "P A" ``` eberlm@63965 ` 32` ```proof (induction A rule: full_multiset_induct) ``` eberlm@63965 ` 33` ``` case (less A) ``` eberlm@63965 ` 34` ``` hence IH: "P B" if "B \# A" for B using that by blast ``` eberlm@63965 ` 35` ``` show ?case ``` eberlm@63965 ` 36` ``` proof (cases "A = {#}") ``` eberlm@63965 ` 37` ``` case True ``` eberlm@63965 ` 38` ``` thus ?thesis by (simp add: assms) ``` eberlm@63965 ` 39` ``` next ``` eberlm@63965 ` 40` ``` case False ``` eberlm@63965 ` 41` ``` hence "P (A - {#x#})" if "x \# A" for x ``` eberlm@63965 ` 42` ``` using that by (intro IH) (simp add: mset_subset_diff_self) ``` eberlm@63965 ` 43` ``` from False and this show "P A" by (rule assms) ``` eberlm@63965 ` 44` ``` qed ``` eberlm@63965 ` 45` ```qed ``` eberlm@63965 ` 46` eberlm@63965 ` 47` ```lemma map_list_bind: "map g (List.bind xs f) = List.bind xs (map g \ f)" ``` eberlm@63965 ` 48` ``` by (simp add: List.bind_def map_concat) ``` eberlm@63965 ` 49` eberlm@63965 ` 50` ```lemma mset_eq_mset_set_imp_distinct: ``` eberlm@63965 ` 51` ``` "finite A \ mset_set A = mset xs \ distinct xs" ``` eberlm@63965 ` 52` ```proof (induction xs arbitrary: A) ``` eberlm@63965 ` 53` ``` case (Cons x xs A) ``` eberlm@63965 ` 54` ``` from Cons.prems(2) have "x \# mset_set A" by simp ``` eberlm@63965 ` 55` ``` with Cons.prems(1) have [simp]: "x \ A" by simp ``` eberlm@63965 ` 56` ``` from Cons.prems have "x \# mset_set (A - {x})" by simp ``` eberlm@63965 ` 57` ``` also from Cons.prems have "mset_set (A - {x}) = mset_set A - {#x#}" ``` eberlm@63965 ` 58` ``` by (subst mset_set_Diff) simp_all ``` eberlm@63965 ` 59` ``` also have "mset_set A = mset (x#xs)" by (simp add: Cons.prems) ``` eberlm@63965 ` 60` ``` also have "\ - {#x#} = mset xs" by simp ``` eberlm@63965 ` 61` ``` finally have [simp]: "x \ set xs" by (simp add: in_multiset_in_set) ``` eberlm@63965 ` 62` ``` from Cons.prems show ?case by (auto intro!: Cons.IH[of "A - {x}"] simp: mset_set_Diff) ``` eberlm@63965 ` 63` ```qed simp_all ``` eberlm@63965 ` 64` ```(* END TODO *) ``` eberlm@63965 ` 65` eberlm@63965 ` 66` eberlm@63965 ` 67` ```subsection \Permutations of a multiset\ ``` eberlm@63965 ` 68` eberlm@63965 ` 69` ```definition permutations_of_multiset :: "'a multiset \ 'a list set" where ``` eberlm@63965 ` 70` ``` "permutations_of_multiset A = {xs. mset xs = A}" ``` eberlm@63965 ` 71` eberlm@63965 ` 72` ```lemma permutations_of_multisetI: "mset xs = A \ xs \ permutations_of_multiset A" ``` eberlm@63965 ` 73` ``` by (simp add: permutations_of_multiset_def) ``` eberlm@63965 ` 74` eberlm@63965 ` 75` ```lemma permutations_of_multisetD: "xs \ permutations_of_multiset A \ mset xs = A" ``` eberlm@63965 ` 76` ``` by (simp add: permutations_of_multiset_def) ``` eberlm@63965 ` 77` eberlm@63965 ` 78` ```lemma permutations_of_multiset_Cons_iff: ``` eberlm@63965 ` 79` ``` "x # xs \ permutations_of_multiset A \ x \# A \ xs \ permutations_of_multiset (A - {#x#})" ``` eberlm@63965 ` 80` ``` by (auto simp: permutations_of_multiset_def) ``` eberlm@63965 ` 81` eberlm@63965 ` 82` ```lemma permutations_of_multiset_empty [simp]: "permutations_of_multiset {#} = {[]}" ``` eberlm@63965 ` 83` ``` unfolding permutations_of_multiset_def by simp ``` eberlm@63965 ` 84` eberlm@63965 ` 85` ```lemma permutations_of_multiset_nonempty: ``` eberlm@63965 ` 86` ``` assumes nonempty: "A \ {#}" ``` eberlm@63965 ` 87` ``` shows "permutations_of_multiset A = ``` eberlm@63965 ` 88` ``` (\x\set_mset A. (op # x) ` permutations_of_multiset (A - {#x#}))" (is "_ = ?rhs") ``` eberlm@63965 ` 89` ```proof safe ``` eberlm@63965 ` 90` ``` fix xs assume "xs \ permutations_of_multiset A" ``` eberlm@63965 ` 91` ``` hence mset_xs: "mset xs = A" by (simp add: permutations_of_multiset_def) ``` eberlm@63965 ` 92` ``` hence "xs \ []" by (auto simp: nonempty) ``` eberlm@63965 ` 93` ``` then obtain x xs' where xs: "xs = x # xs'" by (cases xs) simp_all ``` eberlm@63965 ` 94` ``` with mset_xs have "x \ set_mset A" "xs' \ permutations_of_multiset (A - {#x#})" ``` eberlm@63965 ` 95` ``` by (auto simp: permutations_of_multiset_def) ``` eberlm@63965 ` 96` ``` with xs show "xs \ ?rhs" by auto ``` eberlm@63965 ` 97` ```qed (auto simp: permutations_of_multiset_def) ``` eberlm@63965 ` 98` eberlm@63965 ` 99` ```lemma permutations_of_multiset_singleton [simp]: "permutations_of_multiset {#x#} = {[x]}" ``` eberlm@63965 ` 100` ``` by (simp add: permutations_of_multiset_nonempty) ``` eberlm@63965 ` 101` eberlm@63965 ` 102` ```lemma permutations_of_multiset_doubleton: ``` eberlm@63965 ` 103` ``` "permutations_of_multiset {#x,y#} = {[x,y], [y,x]}" ``` eberlm@63965 ` 104` ``` by (simp add: permutations_of_multiset_nonempty insert_commute) ``` eberlm@63965 ` 105` eberlm@63965 ` 106` ```lemma rev_permutations_of_multiset [simp]: ``` eberlm@63965 ` 107` ``` "rev ` permutations_of_multiset A = permutations_of_multiset A" ``` eberlm@63965 ` 108` ```proof ``` eberlm@63965 ` 109` ``` have "rev ` rev ` permutations_of_multiset A \ rev ` permutations_of_multiset A" ``` eberlm@63965 ` 110` ``` unfolding permutations_of_multiset_def by auto ``` eberlm@63965 ` 111` ``` also have "rev ` rev ` permutations_of_multiset A = permutations_of_multiset A" ``` eberlm@63965 ` 112` ``` by (simp add: image_image) ``` eberlm@63965 ` 113` ``` finally show "permutations_of_multiset A \ rev ` permutations_of_multiset A" . ``` eberlm@63965 ` 114` ```next ``` eberlm@63965 ` 115` ``` show "rev ` permutations_of_multiset A \ permutations_of_multiset A" ``` eberlm@63965 ` 116` ``` unfolding permutations_of_multiset_def by auto ``` eberlm@63965 ` 117` ```qed ``` eberlm@63965 ` 118` eberlm@63965 ` 119` ```lemma length_finite_permutations_of_multiset: ``` eberlm@63965 ` 120` ``` "xs \ permutations_of_multiset A \ length xs = size A" ``` eberlm@63965 ` 121` ``` by (auto simp: permutations_of_multiset_def) ``` eberlm@63965 ` 122` eberlm@63965 ` 123` ```lemma permutations_of_multiset_lists: "permutations_of_multiset A \ lists (set_mset A)" ``` eberlm@63965 ` 124` ``` by (auto simp: permutations_of_multiset_def) ``` eberlm@63965 ` 125` eberlm@63965 ` 126` ```lemma finite_permutations_of_multiset [simp]: "finite (permutations_of_multiset A)" ``` eberlm@63965 ` 127` ```proof (rule finite_subset) ``` eberlm@63965 ` 128` ``` show "permutations_of_multiset A \ {xs. set xs \ set_mset A \ length xs = size A}" ``` eberlm@63965 ` 129` ``` by (auto simp: permutations_of_multiset_def) ``` eberlm@63965 ` 130` ``` show "finite {xs. set xs \ set_mset A \ length xs = size A}" ``` eberlm@63965 ` 131` ``` by (rule finite_lists_length_eq) simp_all ``` eberlm@63965 ` 132` ```qed ``` eberlm@63965 ` 133` eberlm@63965 ` 134` ```lemma permutations_of_multiset_not_empty [simp]: "permutations_of_multiset A \ {}" ``` eberlm@63965 ` 135` ```proof - ``` eberlm@63965 ` 136` ``` from ex_mset[of A] guess xs .. ``` eberlm@63965 ` 137` ``` thus ?thesis by (auto simp: permutations_of_multiset_def) ``` eberlm@63965 ` 138` ```qed ``` eberlm@63965 ` 139` eberlm@63965 ` 140` ```lemma permutations_of_multiset_image: ``` eberlm@63965 ` 141` ``` "permutations_of_multiset (image_mset f A) = map f ` permutations_of_multiset A" ``` eberlm@63965 ` 142` ```proof safe ``` eberlm@63965 ` 143` ``` fix xs assume A: "xs \ permutations_of_multiset (image_mset f A)" ``` eberlm@63965 ` 144` ``` from ex_mset[of A] obtain ys where ys: "mset ys = A" .. ``` eberlm@63965 ` 145` ``` with A have "mset xs = mset (map f ys)" ``` eberlm@63965 ` 146` ``` by (simp add: permutations_of_multiset_def) ``` eberlm@63965 ` 147` ``` from mset_eq_permutation[OF this] guess \ . note \ = this ``` eberlm@63965 ` 148` ``` with ys have "xs = map f (permute_list \ ys)" ``` eberlm@63965 ` 149` ``` by (simp add: permute_list_map) ``` eberlm@63965 ` 150` ``` moreover from \ ys have "permute_list \ ys \ permutations_of_multiset A" ``` eberlm@63965 ` 151` ``` by (simp add: permutations_of_multiset_def) ``` eberlm@63965 ` 152` ``` ultimately show "xs \ map f ` permutations_of_multiset A" by blast ``` eberlm@63965 ` 153` ```qed (auto simp: permutations_of_multiset_def) ``` eberlm@63965 ` 154` eberlm@63965 ` 155` eberlm@63965 ` 156` ```subsection \Cardinality of permutations\ ``` eberlm@63965 ` 157` eberlm@63965 ` 158` ```text \ ``` eberlm@63965 ` 159` ``` In this section, we prove some basic facts about the number of permutations of a multiset. ``` eberlm@63965 ` 160` ```\ ``` eberlm@63965 ` 161` eberlm@63965 ` 162` ```context ``` eberlm@63965 ` 163` ```begin ``` eberlm@63965 ` 164` nipkow@64272 ` 165` ```private lemma multiset_prod_fact_insert: ``` eberlm@63965 ` 166` ``` "(\y\set_mset (A+{#x#}). fact (count (A+{#x#}) y)) = ``` eberlm@63965 ` 167` ``` (count A x + 1) * (\y\set_mset A. fact (count A y))" ``` eberlm@63965 ` 168` ```proof - ``` eberlm@63965 ` 169` ``` have "(\y\set_mset (A+{#x#}). fact (count (A+{#x#}) y)) = ``` eberlm@63965 ` 170` ``` (\y\set_mset (A+{#x#}). (if y = x then count A x + 1 else 1) * fact (count A y))" ``` nipkow@64272 ` 171` ``` by (intro prod.cong) simp_all ``` eberlm@63965 ` 172` ``` also have "\ = (count A x + 1) * (\y\set_mset (A+{#x#}). fact (count A y))" ``` nipkow@64272 ` 173` ``` by (simp add: prod.distrib prod.delta) ``` eberlm@63965 ` 174` ``` also have "(\y\set_mset (A+{#x#}). fact (count A y)) = (\y\set_mset A. fact (count A y))" ``` nipkow@64272 ` 175` ``` by (intro prod.mono_neutral_right) (auto simp: not_in_iff) ``` eberlm@63965 ` 176` ``` finally show ?thesis . ``` eberlm@63965 ` 177` ```qed ``` eberlm@63965 ` 178` nipkow@64272 ` 179` ```private lemma multiset_prod_fact_remove: ``` eberlm@63965 ` 180` ``` "x \# A \ (\y\set_mset A. fact (count A y)) = ``` eberlm@63965 ` 181` ``` count A x * (\y\set_mset (A-{#x#}). fact (count (A-{#x#}) y))" ``` nipkow@64272 ` 182` ``` using multiset_prod_fact_insert[of "A - {#x#}" x] by simp ``` eberlm@63965 ` 183` eberlm@63965 ` 184` ```lemma card_permutations_of_multiset_aux: ``` eberlm@63965 ` 185` ``` "card (permutations_of_multiset A) * (\x\set_mset A. fact (count A x)) = fact (size A)" ``` eberlm@63965 ` 186` ```proof (induction A rule: multiset_remove_induct) ``` eberlm@63965 ` 187` ``` case (remove A) ``` eberlm@63965 ` 188` ``` have "card (permutations_of_multiset A) = ``` eberlm@63965 ` 189` ``` card (\x\set_mset A. op # x ` permutations_of_multiset (A - {#x#}))" ``` eberlm@63965 ` 190` ``` by (simp add: permutations_of_multiset_nonempty remove.hyps) ``` eberlm@63965 ` 191` ``` also have "\ = (\x\set_mset A. card (permutations_of_multiset (A - {#x#})))" ``` eberlm@63965 ` 192` ``` by (subst card_UN_disjoint) (auto simp: card_image) ``` eberlm@63965 ` 193` ``` also have "\ * (\x\set_mset A. fact (count A x)) = ``` eberlm@63965 ` 194` ``` (\x\set_mset A. card (permutations_of_multiset (A - {#x#})) * ``` eberlm@63965 ` 195` ``` (\y\set_mset A. fact (count A y)))" ``` nipkow@64267 ` 196` ``` by (subst sum_distrib_right) simp_all ``` eberlm@63965 ` 197` ``` also have "\ = (\x\set_mset A. count A x * fact (size A - 1))" ``` nipkow@64267 ` 198` ``` proof (intro sum.cong refl) ``` eberlm@63965 ` 199` ``` fix x assume x: "x \# A" ``` eberlm@63965 ` 200` ``` have "card (permutations_of_multiset (A - {#x#})) * (\y\set_mset A. fact (count A y)) = ``` eberlm@63965 ` 201` ``` count A x * (card (permutations_of_multiset (A - {#x#})) * ``` eberlm@63965 ` 202` ``` (\y\set_mset (A - {#x#}). fact (count (A - {#x#}) y)))" (is "?lhs = _") ``` nipkow@64272 ` 203` ``` by (subst multiset_prod_fact_remove[OF x]) simp_all ``` eberlm@63965 ` 204` ``` also note remove.IH[OF x] ``` eberlm@63965 ` 205` ``` also from x have "size (A - {#x#}) = size A - 1" by (simp add: size_Diff_submset) ``` eberlm@63965 ` 206` ``` finally show "?lhs = count A x * fact (size A - 1)" . ``` eberlm@63965 ` 207` ``` qed ``` eberlm@63965 ` 208` ``` also have "(\x\set_mset A. count A x * fact (size A - 1)) = ``` eberlm@63965 ` 209` ``` size A * fact (size A - 1)" ``` nipkow@64267 ` 210` ``` by (simp add: sum_distrib_right size_multiset_overloaded_eq) ``` eberlm@63965 ` 211` ``` also from remove.hyps have "\ = fact (size A)" ``` eberlm@63965 ` 212` ``` by (cases "size A") auto ``` eberlm@63965 ` 213` ``` finally show ?case . ``` eberlm@63965 ` 214` ```qed simp_all ``` eberlm@63965 ` 215` eberlm@63965 ` 216` ```theorem card_permutations_of_multiset: ``` eberlm@63965 ` 217` ``` "card (permutations_of_multiset A) = fact (size A) div (\x\set_mset A. fact (count A x))" ``` eberlm@63965 ` 218` ``` "(\x\set_mset A. fact (count A x) :: nat) dvd fact (size A)" ``` eberlm@63965 ` 219` ``` by (simp_all add: card_permutations_of_multiset_aux[of A, symmetric]) ``` eberlm@63965 ` 220` eberlm@63965 ` 221` ```lemma card_permutations_of_multiset_insert_aux: ``` eberlm@63965 ` 222` ``` "card (permutations_of_multiset (A + {#x#})) * (count A x + 1) = ``` eberlm@63965 ` 223` ``` (size A + 1) * card (permutations_of_multiset A)" ``` eberlm@63965 ` 224` ```proof - ``` eberlm@63965 ` 225` ``` note card_permutations_of_multiset_aux[of "A + {#x#}"] ``` eberlm@63965 ` 226` ``` also have "fact (size (A + {#x#})) = (size A + 1) * fact (size A)" by simp ``` nipkow@64272 ` 227` ``` also note multiset_prod_fact_insert[of A x] ``` eberlm@63965 ` 228` ``` also note card_permutations_of_multiset_aux[of A, symmetric] ``` eberlm@63965 ` 229` ``` finally have "card (permutations_of_multiset (A + {#x#})) * (count A x + 1) * ``` eberlm@63965 ` 230` ``` (\y\set_mset A. fact (count A y)) = ``` eberlm@63965 ` 231` ``` (size A + 1) * card (permutations_of_multiset A) * ``` eberlm@63965 ` 232` ``` (\x\set_mset A. fact (count A x))" by (simp only: mult_ac) ``` eberlm@63965 ` 233` ``` thus ?thesis by (subst (asm) mult_right_cancel) simp_all ``` eberlm@63965 ` 234` ```qed ``` eberlm@63965 ` 235` eberlm@63965 ` 236` ```lemma card_permutations_of_multiset_remove_aux: ``` eberlm@63965 ` 237` ``` assumes "x \# A" ``` eberlm@63965 ` 238` ``` shows "card (permutations_of_multiset A) * count A x = ``` eberlm@63965 ` 239` ``` size A * card (permutations_of_multiset (A - {#x#}))" ``` eberlm@63965 ` 240` ```proof - ``` eberlm@63965 ` 241` ``` from assms have A: "A - {#x#} + {#x#} = A" by simp ``` eberlm@63965 ` 242` ``` from assms have B: "size A = size (A - {#x#}) + 1" ``` eberlm@63965 ` 243` ``` by (subst A [symmetric], subst size_union) simp ``` eberlm@63965 ` 244` ``` show ?thesis ``` eberlm@63965 ` 245` ``` using card_permutations_of_multiset_insert_aux[of "A - {#x#}" x, unfolded A] assms ``` eberlm@63965 ` 246` ``` by (simp add: B) ``` eberlm@63965 ` 247` ```qed ``` eberlm@63965 ` 248` eberlm@63965 ` 249` ```lemma real_card_permutations_of_multiset_remove: ``` eberlm@63965 ` 250` ``` assumes "x \# A" ``` eberlm@63965 ` 251` ``` shows "real (card (permutations_of_multiset (A - {#x#}))) = ``` eberlm@63965 ` 252` ``` real (card (permutations_of_multiset A) * count A x) / real (size A)" ``` eberlm@63965 ` 253` ``` using assms by (subst card_permutations_of_multiset_remove_aux[OF assms]) auto ``` eberlm@63965 ` 254` eberlm@63965 ` 255` ```lemma real_card_permutations_of_multiset_remove': ``` eberlm@63965 ` 256` ``` assumes "x \# A" ``` eberlm@63965 ` 257` ``` shows "real (card (permutations_of_multiset A)) = ``` eberlm@63965 ` 258` ``` real (size A * card (permutations_of_multiset (A - {#x#}))) / real (count A x)" ``` eberlm@63965 ` 259` ``` using assms by (subst card_permutations_of_multiset_remove_aux[OF assms, symmetric]) simp ``` eberlm@63965 ` 260` eberlm@63965 ` 261` ```end ``` eberlm@63965 ` 262` eberlm@63965 ` 263` eberlm@63965 ` 264` eberlm@63965 ` 265` ```subsection \Permutations of a set\ ``` eberlm@63965 ` 266` eberlm@63965 ` 267` ```definition permutations_of_set :: "'a set \ 'a list set" where ``` eberlm@63965 ` 268` ``` "permutations_of_set A = {xs. set xs = A \ distinct xs}" ``` eberlm@63965 ` 269` eberlm@63965 ` 270` ```lemma permutations_of_set_altdef: ``` eberlm@63965 ` 271` ``` "finite A \ permutations_of_set A = permutations_of_multiset (mset_set A)" ``` eberlm@63965 ` 272` ``` by (auto simp add: permutations_of_set_def permutations_of_multiset_def mset_set_set ``` eberlm@63965 ` 273` ``` in_multiset_in_set [symmetric] mset_eq_mset_set_imp_distinct) ``` eberlm@63965 ` 274` eberlm@63965 ` 275` ```lemma permutations_of_setI [intro]: ``` eberlm@63965 ` 276` ``` assumes "set xs = A" "distinct xs" ``` eberlm@63965 ` 277` ``` shows "xs \ permutations_of_set A" ``` eberlm@63965 ` 278` ``` using assms unfolding permutations_of_set_def by simp ``` eberlm@63965 ` 279` ``` ``` eberlm@63965 ` 280` ```lemma permutations_of_setD: ``` eberlm@63965 ` 281` ``` assumes "xs \ permutations_of_set A" ``` eberlm@63965 ` 282` ``` shows "set xs = A" "distinct xs" ``` eberlm@63965 ` 283` ``` using assms unfolding permutations_of_set_def by simp_all ``` eberlm@63965 ` 284` ``` ``` eberlm@63965 ` 285` ```lemma permutations_of_set_lists: "permutations_of_set A \ lists A" ``` eberlm@63965 ` 286` ``` unfolding permutations_of_set_def by auto ``` eberlm@63965 ` 287` eberlm@63965 ` 288` ```lemma permutations_of_set_empty [simp]: "permutations_of_set {} = {[]}" ``` eberlm@63965 ` 289` ``` by (auto simp: permutations_of_set_def) ``` eberlm@63965 ` 290` ``` ``` eberlm@63965 ` 291` ```lemma UN_set_permutations_of_set [simp]: ``` eberlm@63965 ` 292` ``` "finite A \ (\xs\permutations_of_set A. set xs) = A" ``` eberlm@63965 ` 293` ``` using finite_distinct_list by (auto simp: permutations_of_set_def) ``` eberlm@63965 ` 294` eberlm@63965 ` 295` ```lemma permutations_of_set_infinite: ``` eberlm@63965 ` 296` ``` "\finite A \ permutations_of_set A = {}" ``` eberlm@63965 ` 297` ``` by (auto simp: permutations_of_set_def) ``` eberlm@63965 ` 298` eberlm@63965 ` 299` ```lemma permutations_of_set_nonempty: ``` eberlm@63965 ` 300` ``` "A \ {} \ permutations_of_set A = ``` eberlm@63965 ` 301` ``` (\x\A. (\xs. x # xs) ` permutations_of_set (A - {x}))" ``` eberlm@63965 ` 302` ``` by (cases "finite A") ``` eberlm@63965 ` 303` ``` (simp_all add: permutations_of_multiset_nonempty mset_set_empty_iff mset_set_Diff ``` eberlm@63965 ` 304` ``` permutations_of_set_altdef permutations_of_set_infinite) ``` eberlm@63965 ` 305` ``` ``` eberlm@63965 ` 306` ```lemma permutations_of_set_singleton [simp]: "permutations_of_set {x} = {[x]}" ``` eberlm@63965 ` 307` ``` by (subst permutations_of_set_nonempty) auto ``` eberlm@63965 ` 308` eberlm@63965 ` 309` ```lemma permutations_of_set_doubleton: ``` eberlm@63965 ` 310` ``` "x \ y \ permutations_of_set {x,y} = {[x,y], [y,x]}" ``` eberlm@63965 ` 311` ``` by (subst permutations_of_set_nonempty) ``` eberlm@63965 ` 312` ``` (simp_all add: insert_Diff_if insert_commute) ``` eberlm@63965 ` 313` eberlm@63965 ` 314` ```lemma rev_permutations_of_set [simp]: ``` eberlm@63965 ` 315` ``` "rev ` permutations_of_set A = permutations_of_set A" ``` eberlm@63965 ` 316` ``` by (cases "finite A") (simp_all add: permutations_of_set_altdef permutations_of_set_infinite) ``` eberlm@63965 ` 317` eberlm@63965 ` 318` ```lemma length_finite_permutations_of_set: ``` eberlm@63965 ` 319` ``` "xs \ permutations_of_set A \ length xs = card A" ``` eberlm@63965 ` 320` ``` by (auto simp: permutations_of_set_def distinct_card) ``` eberlm@63965 ` 321` eberlm@63965 ` 322` ```lemma finite_permutations_of_set [simp]: "finite (permutations_of_set A)" ``` eberlm@63965 ` 323` ``` by (cases "finite A") (simp_all add: permutations_of_set_infinite permutations_of_set_altdef) ``` eberlm@63965 ` 324` eberlm@63965 ` 325` ```lemma permutations_of_set_empty_iff [simp]: ``` eberlm@63965 ` 326` ``` "permutations_of_set A = {} \ \finite A" ``` eberlm@63965 ` 327` ``` unfolding permutations_of_set_def using finite_distinct_list[of A] by auto ``` eberlm@63965 ` 328` eberlm@63965 ` 329` ```lemma card_permutations_of_set [simp]: ``` eberlm@63965 ` 330` ``` "finite A \ card (permutations_of_set A) = fact (card A)" ``` eberlm@63965 ` 331` ``` by (simp add: permutations_of_set_altdef card_permutations_of_multiset del: One_nat_def) ``` eberlm@63965 ` 332` eberlm@63965 ` 333` ```lemma permutations_of_set_image_inj: ``` eberlm@63965 ` 334` ``` assumes inj: "inj_on f A" ``` eberlm@63965 ` 335` ``` shows "permutations_of_set (f ` A) = map f ` permutations_of_set A" ``` eberlm@63965 ` 336` ``` by (cases "finite A") ``` eberlm@63965 ` 337` ``` (simp_all add: permutations_of_set_infinite permutations_of_set_altdef ``` eberlm@63965 ` 338` ``` permutations_of_multiset_image mset_set_image_inj inj finite_image_iff) ``` eberlm@63965 ` 339` eberlm@63965 ` 340` ```lemma permutations_of_set_image_permutes: ``` eberlm@63965 ` 341` ``` "\ permutes A \ map \ ` permutations_of_set A = permutations_of_set A" ``` eberlm@63965 ` 342` ``` by (subst permutations_of_set_image_inj [symmetric]) ``` eberlm@63965 ` 343` ``` (simp_all add: permutes_inj_on permutes_image) ``` eberlm@63965 ` 344` eberlm@63965 ` 345` eberlm@63965 ` 346` ```subsection \Code generation\ ``` eberlm@63965 ` 347` eberlm@63965 ` 348` ```text \ ``` eberlm@63965 ` 349` ``` First, we give code an implementation for permutations of lists. ``` eberlm@63965 ` 350` ```\ ``` eberlm@63965 ` 351` eberlm@63965 ` 352` ```declare length_remove1 [termination_simp] ``` eberlm@63965 ` 353` eberlm@63965 ` 354` ```fun permutations_of_list_impl where ``` eberlm@63965 ` 355` ``` "permutations_of_list_impl xs = (if xs = [] then [[]] else ``` eberlm@63965 ` 356` ``` List.bind (remdups xs) (\x. map (op # x) (permutations_of_list_impl (remove1 x xs))))" ``` eberlm@63965 ` 357` eberlm@63965 ` 358` ```fun permutations_of_list_impl_aux where ``` eberlm@63965 ` 359` ``` "permutations_of_list_impl_aux acc xs = (if xs = [] then [acc] else ``` eberlm@63965 ` 360` ``` List.bind (remdups xs) (\x. permutations_of_list_impl_aux (x#acc) (remove1 x xs)))" ``` eberlm@63965 ` 361` eberlm@63965 ` 362` ```declare permutations_of_list_impl_aux.simps [simp del] ``` eberlm@63965 ` 363` ```declare permutations_of_list_impl.simps [simp del] ``` eberlm@63965 ` 364` ``` ``` eberlm@63965 ` 365` ```lemma permutations_of_list_impl_Nil [simp]: ``` eberlm@63965 ` 366` ``` "permutations_of_list_impl [] = [[]]" ``` eberlm@63965 ` 367` ``` by (simp add: permutations_of_list_impl.simps) ``` eberlm@63965 ` 368` eberlm@63965 ` 369` ```lemma permutations_of_list_impl_nonempty: ``` eberlm@63965 ` 370` ``` "xs \ [] \ permutations_of_list_impl xs = ``` eberlm@63965 ` 371` ``` List.bind (remdups xs) (\x. map (op # x) (permutations_of_list_impl (remove1 x xs)))" ``` eberlm@63965 ` 372` ``` by (subst permutations_of_list_impl.simps) simp_all ``` eberlm@63965 ` 373` eberlm@63965 ` 374` ```lemma set_permutations_of_list_impl: ``` eberlm@63965 ` 375` ``` "set (permutations_of_list_impl xs) = permutations_of_multiset (mset xs)" ``` eberlm@63965 ` 376` ``` by (induction xs rule: permutations_of_list_impl.induct) ``` eberlm@63965 ` 377` ``` (subst permutations_of_list_impl.simps, ``` eberlm@63965 ` 378` ``` simp_all add: permutations_of_multiset_nonempty set_list_bind) ``` eberlm@63965 ` 379` eberlm@63965 ` 380` ```lemma distinct_permutations_of_list_impl: ``` eberlm@63965 ` 381` ``` "distinct (permutations_of_list_impl xs)" ``` eberlm@63965 ` 382` ``` by (induction xs rule: permutations_of_list_impl.induct, ``` eberlm@63965 ` 383` ``` subst permutations_of_list_impl.simps) ``` eberlm@63965 ` 384` ``` (auto intro!: distinct_list_bind simp: distinct_map o_def disjoint_family_on_def) ``` eberlm@63965 ` 385` eberlm@63965 ` 386` ```lemma permutations_of_list_impl_aux_correct': ``` eberlm@63965 ` 387` ``` "permutations_of_list_impl_aux acc xs = ``` eberlm@63965 ` 388` ``` map (\xs. rev xs @ acc) (permutations_of_list_impl xs)" ``` eberlm@63965 ` 389` ``` by (induction acc xs rule: permutations_of_list_impl_aux.induct, ``` eberlm@63965 ` 390` ``` subst permutations_of_list_impl_aux.simps, subst permutations_of_list_impl.simps) ``` eberlm@63965 ` 391` ``` (auto simp: map_list_bind intro!: list_bind_cong) ``` eberlm@63965 ` 392` ``` ``` eberlm@63965 ` 393` ```lemma permutations_of_list_impl_aux_correct: ``` eberlm@63965 ` 394` ``` "permutations_of_list_impl_aux [] xs = map rev (permutations_of_list_impl xs)" ``` eberlm@63965 ` 395` ``` by (simp add: permutations_of_list_impl_aux_correct') ``` eberlm@63965 ` 396` eberlm@63965 ` 397` ```lemma distinct_permutations_of_list_impl_aux: ``` eberlm@63965 ` 398` ``` "distinct (permutations_of_list_impl_aux acc xs)" ``` eberlm@63965 ` 399` ``` by (simp add: permutations_of_list_impl_aux_correct' distinct_map ``` eberlm@63965 ` 400` ``` distinct_permutations_of_list_impl inj_on_def) ``` eberlm@63965 ` 401` eberlm@63965 ` 402` ```lemma set_permutations_of_list_impl_aux: ``` eberlm@63965 ` 403` ``` "set (permutations_of_list_impl_aux [] xs) = permutations_of_multiset (mset xs)" ``` eberlm@63965 ` 404` ``` by (simp add: permutations_of_list_impl_aux_correct set_permutations_of_list_impl) ``` eberlm@63965 ` 405` ``` ``` eberlm@63965 ` 406` ```declare set_permutations_of_list_impl_aux [symmetric, code] ``` eberlm@63965 ` 407` eberlm@63965 ` 408` ```value [code] "permutations_of_multiset {#1,2,3,4::int#}" ``` eberlm@63965 ` 409` eberlm@63965 ` 410` eberlm@63965 ` 411` eberlm@63965 ` 412` ```text \ ``` eberlm@63965 ` 413` ``` Now we turn to permutations of sets. We define an auxiliary version with an ``` eberlm@63965 ` 414` ``` accumulator to avoid having to map over the results. ``` eberlm@63965 ` 415` ```\ ``` eberlm@63965 ` 416` ```function permutations_of_set_aux where ``` eberlm@63965 ` 417` ``` "permutations_of_set_aux acc A = ``` eberlm@63965 ` 418` ``` (if \finite A then {} else if A = {} then {acc} else ``` eberlm@63965 ` 419` ``` (\x\A. permutations_of_set_aux (x#acc) (A - {x})))" ``` eberlm@63965 ` 420` ```by auto ``` eberlm@63965 ` 421` ```termination by (relation "Wellfounded.measure (card \ snd)") (simp_all add: card_gt_0_iff) ``` eberlm@63965 ` 422` eberlm@63965 ` 423` ```lemma permutations_of_set_aux_altdef: ``` eberlm@63965 ` 424` ``` "permutations_of_set_aux acc A = (\xs. rev xs @ acc) ` permutations_of_set A" ``` eberlm@63965 ` 425` ```proof (cases "finite A") ``` eberlm@63965 ` 426` ``` assume "finite A" ``` eberlm@63965 ` 427` ``` thus ?thesis ``` eberlm@63965 ` 428` ``` proof (induction A arbitrary: acc rule: finite_psubset_induct) ``` eberlm@63965 ` 429` ``` case (psubset A acc) ``` eberlm@63965 ` 430` ``` show ?case ``` eberlm@63965 ` 431` ``` proof (cases "A = {}") ``` eberlm@63965 ` 432` ``` case False ``` eberlm@63965 ` 433` ``` note [simp del] = permutations_of_set_aux.simps ``` eberlm@63965 ` 434` ``` from psubset.hyps False ``` eberlm@63965 ` 435` ``` have "permutations_of_set_aux acc A = ``` eberlm@63965 ` 436` ``` (\y\A. permutations_of_set_aux (y#acc) (A - {y}))" ``` eberlm@63965 ` 437` ``` by (subst permutations_of_set_aux.simps) simp_all ``` eberlm@63965 ` 438` ``` also have "\ = (\y\A. (\xs. rev xs @ acc) ` (\xs. y # xs) ` permutations_of_set (A - {y}))" ``` eberlm@63965 ` 439` ``` by (intro SUP_cong refl, subst psubset) (auto simp: image_image) ``` eberlm@63965 ` 440` ``` also from False have "\ = (\xs. rev xs @ acc) ` permutations_of_set A" ``` eberlm@63965 ` 441` ``` by (subst (2) permutations_of_set_nonempty) (simp_all add: image_UN) ``` eberlm@63965 ` 442` ``` finally show ?thesis . ``` eberlm@63965 ` 443` ``` qed simp_all ``` eberlm@63965 ` 444` ``` qed ``` eberlm@63965 ` 445` ```qed (simp_all add: permutations_of_set_infinite) ``` eberlm@63965 ` 446` eberlm@63965 ` 447` ```declare permutations_of_set_aux.simps [simp del] ``` eberlm@63965 ` 448` eberlm@63965 ` 449` ```lemma permutations_of_set_aux_correct: ``` eberlm@63965 ` 450` ``` "permutations_of_set_aux [] A = permutations_of_set A" ``` eberlm@63965 ` 451` ``` by (simp add: permutations_of_set_aux_altdef) ``` eberlm@63965 ` 452` eberlm@63965 ` 453` eberlm@63965 ` 454` ```text \ ``` eberlm@63965 ` 455` ``` In another refinement step, we define a version on lists. ``` eberlm@63965 ` 456` ```\ ``` eberlm@63965 ` 457` ```declare length_remove1 [termination_simp] ``` eberlm@63965 ` 458` eberlm@63965 ` 459` ```fun permutations_of_set_aux_list where ``` eberlm@63965 ` 460` ``` "permutations_of_set_aux_list acc xs = ``` eberlm@63965 ` 461` ``` (if xs = [] then [acc] else ``` eberlm@63965 ` 462` ``` List.bind xs (\x. permutations_of_set_aux_list (x#acc) (List.remove1 x xs)))" ``` eberlm@63965 ` 463` eberlm@63965 ` 464` ```definition permutations_of_set_list where ``` eberlm@63965 ` 465` ``` "permutations_of_set_list xs = permutations_of_set_aux_list [] xs" ``` eberlm@63965 ` 466` eberlm@63965 ` 467` ```declare permutations_of_set_aux_list.simps [simp del] ``` eberlm@63965 ` 468` eberlm@63965 ` 469` ```lemma permutations_of_set_aux_list_refine: ``` eberlm@63965 ` 470` ``` assumes "distinct xs" ``` eberlm@63965 ` 471` ``` shows "set (permutations_of_set_aux_list acc xs) = permutations_of_set_aux acc (set xs)" ``` eberlm@63965 ` 472` ``` using assms ``` eberlm@63965 ` 473` ``` by (induction acc xs rule: permutations_of_set_aux_list.induct) ``` eberlm@63965 ` 474` ``` (subst permutations_of_set_aux_list.simps, ``` eberlm@63965 ` 475` ``` subst permutations_of_set_aux.simps, ``` eberlm@63965 ` 476` ``` simp_all add: set_list_bind cong: SUP_cong) ``` eberlm@63965 ` 477` eberlm@63965 ` 478` eberlm@63965 ` 479` ```text \ ``` eberlm@63965 ` 480` ``` The permutation lists contain no duplicates if the inputs contain no duplicates. ``` eberlm@63965 ` 481` ``` Therefore, these functions can easily be used when working with a representation of ``` eberlm@63965 ` 482` ``` sets by distinct lists. ``` eberlm@63965 ` 483` ``` The same approach should generalise to any kind of set implementation that supports ``` eberlm@63965 ` 484` ``` a monadic bind operation, and since the results are disjoint, merging should be cheap. ``` eberlm@63965 ` 485` ```\ ``` eberlm@63965 ` 486` ```lemma distinct_permutations_of_set_aux_list: ``` eberlm@63965 ` 487` ``` "distinct xs \ distinct (permutations_of_set_aux_list acc xs)" ``` eberlm@63965 ` 488` ``` by (induction acc xs rule: permutations_of_set_aux_list.induct) ``` eberlm@63965 ` 489` ``` (subst permutations_of_set_aux_list.simps, ``` eberlm@63965 ` 490` ``` auto intro!: distinct_list_bind simp: disjoint_family_on_def ``` eberlm@63965 ` 491` ``` permutations_of_set_aux_list_refine permutations_of_set_aux_altdef) ``` eberlm@63965 ` 492` eberlm@63965 ` 493` ```lemma distinct_permutations_of_set_list: ``` eberlm@63965 ` 494` ``` "distinct xs \ distinct (permutations_of_set_list xs)" ``` eberlm@63965 ` 495` ``` by (simp add: permutations_of_set_list_def distinct_permutations_of_set_aux_list) ``` eberlm@63965 ` 496` eberlm@63965 ` 497` ```lemma permutations_of_list: ``` eberlm@63965 ` 498` ``` "permutations_of_set (set xs) = set (permutations_of_set_list (remdups xs))" ``` eberlm@63965 ` 499` ``` by (simp add: permutations_of_set_aux_correct [symmetric] ``` eberlm@63965 ` 500` ``` permutations_of_set_aux_list_refine permutations_of_set_list_def) ``` eberlm@63965 ` 501` eberlm@63965 ` 502` ```lemma permutations_of_list_code [code]: ``` eberlm@63965 ` 503` ``` "permutations_of_set (set xs) = set (permutations_of_set_list (remdups xs))" ``` eberlm@63965 ` 504` ``` "permutations_of_set (List.coset xs) = ``` eberlm@63965 ` 505` ``` Code.abort (STR ''Permutation of set complement not supported'') ``` eberlm@63965 ` 506` ``` (\_. permutations_of_set (List.coset xs))" ``` eberlm@63965 ` 507` ``` by (simp_all add: permutations_of_list) ``` eberlm@63965 ` 508` eberlm@63965 ` 509` ```value [code] "permutations_of_set (set ''abcd'')" ``` eberlm@63965 ` 510` nipkow@64267 ` 511` ```end ```