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