src/HOL/Library/Multiset_Permutations.thy
 author wenzelm Tue May 15 13:57:39 2018 +0200 (16 months ago) changeset 68189 6163c90694ef parent 67399 eab6ce8368fa child 68406 6beb45f6cf67 permissions -rw-r--r--
```     1 (*  Title:      HOL/Library/Multiset_Permutations.thy
```
```     2     Author:     Manuel Eberl (TU München)
```
```     3
```
```     4 Defines the set of permutations of a given multiset (or set), i.e. the set of all lists whose
```
```     5 entries correspond to the multiset (resp. set).
```
```     6 *)
```
```     7
```
```     8 section \<open>Permutations of a Multiset\<close>
```
```     9
```
```    10 theory Multiset_Permutations
```
```    11 imports
```
```    12   Complex_Main
```
```    13   Multiset
```
```    14   Permutations
```
```    15 begin
```
```    16
```
```    17 (* TODO Move *)
```
```    18 lemma mset_tl: "xs \<noteq> [] \<Longrightarrow> mset (tl xs) = mset xs - {#hd xs#}"
```
```    19   by (cases xs) simp_all
```
```    20
```
```    21 lemma mset_set_image_inj:
```
```    22   assumes "inj_on f A"
```
```    23   shows   "mset_set (f ` A) = image_mset f (mset_set A)"
```
```    24 proof (cases "finite A")
```
```    25   case True
```
```    26   from this and assms show ?thesis by (induction A) auto
```
```    27 qed (insert assms, simp add: finite_image_iff)
```
```    28
```
```    29 lemma 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"
```
```    32 proof (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
```
```    45 qed
```
```    46
```
```    47 lemma 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
```
```    50 lemma mset_eq_mset_set_imp_distinct:
```
```    51   "finite A \<Longrightarrow> mset_set A = mset xs \<Longrightarrow> distinct xs"
```
```    52 proof (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)
```
```    63 qed simp_all
```
```    64 (* END TODO *)
```
```    65
```
```    66
```
```    67 subsection \<open>Permutations of a multiset\<close>
```
```    68
```
```    69 definition permutations_of_multiset :: "'a multiset \<Rightarrow> 'a list set" where
```
```    70   "permutations_of_multiset A = {xs. mset xs = A}"
```
```    71
```
```    72 lemma permutations_of_multisetI: "mset xs = A \<Longrightarrow> xs \<in> permutations_of_multiset A"
```
```    73   by (simp add: permutations_of_multiset_def)
```
```    74
```
```    75 lemma permutations_of_multisetD: "xs \<in> permutations_of_multiset A \<Longrightarrow> mset xs = A"
```
```    76   by (simp add: permutations_of_multiset_def)
```
```    77
```
```    78 lemma 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
```
```    82 lemma permutations_of_multiset_empty [simp]: "permutations_of_multiset {#} = {[]}"
```
```    83   unfolding permutations_of_multiset_def by simp
```
```    84
```
```    85 lemma 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")
```
```    89 proof 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
```
```    97 qed (auto simp: permutations_of_multiset_def)
```
```    98
```
```    99 lemma permutations_of_multiset_singleton [simp]: "permutations_of_multiset {#x#} = {[x]}"
```
```   100   by (simp add: permutations_of_multiset_nonempty)
```
```   101
```
```   102 lemma 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
```
```   106 lemma rev_permutations_of_multiset [simp]:
```
```   107   "rev ` permutations_of_multiset A = permutations_of_multiset A"
```
```   108 proof
```
```   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" .
```
```   114 next
```
```   115   show "rev ` permutations_of_multiset A \<subseteq> permutations_of_multiset A"
```
```   116     unfolding permutations_of_multiset_def by auto
```
```   117 qed
```
```   118
```
```   119 lemma 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
```
```   123 lemma permutations_of_multiset_lists: "permutations_of_multiset A \<subseteq> lists (set_mset A)"
```
```   124   by (auto simp: permutations_of_multiset_def)
```
```   125
```
```   126 lemma finite_permutations_of_multiset [simp]: "finite (permutations_of_multiset A)"
```
```   127 proof (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
```
```   132 qed
```
```   133
```
```   134 lemma permutations_of_multiset_not_empty [simp]: "permutations_of_multiset A \<noteq> {}"
```
```   135 proof -
```
```   136   from ex_mset[of A] guess xs ..
```
```   137   thus ?thesis by (auto simp: permutations_of_multiset_def)
```
```   138 qed
```
```   139
```
```   140 lemma permutations_of_multiset_image:
```
```   141   "permutations_of_multiset (image_mset f A) = map f ` permutations_of_multiset A"
```
```   142 proof 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
```
```   153 qed (auto simp: permutations_of_multiset_def)
```
```   154
```
```   155
```
```   156 subsection \<open>Cardinality of permutations\<close>
```
```   157
```
```   158 text \<open>
```
```   159   In this section, we prove some basic facts about the number of permutations of a multiset.
```
```   160 \<close>
```
```   161
```
```   162 context
```
```   163 begin
```
```   164
```
```   165 private 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))"
```
```   168 proof -
```
```   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 .
```
```   177 qed
```
```   178
```
```   179 private 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
```
```   184 lemma card_permutations_of_multiset_aux:
```
```   185   "card (permutations_of_multiset A) * (\<Prod>x\<in>set_mset A. fact (count A x)) = fact (size A)"
```
```   186 proof (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 .
```
```   214 qed simp_all
```
```   215
```
```   216 theorem 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 add: card_permutations_of_multiset_aux[of A, symmetric])
```
```   220
```
```   221 lemma 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)"
```
```   224 proof -
```
```   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
```
```   234 qed
```
```   235
```
```   236 lemma 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#}))"
```
```   240 proof -
```
```   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)
```
```   247 qed
```
```   248
```
```   249 lemma 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
```
```   255 lemma 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
```
```   261 end
```
```   262
```
```   263
```
```   264
```
```   265 subsection \<open>Permutations of a set\<close>
```
```   266
```
```   267 definition permutations_of_set :: "'a set \<Rightarrow> 'a list set" where
```
```   268   "permutations_of_set A = {xs. set xs = A \<and> distinct xs}"
```
```   269
```
```   270 lemma 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
```
```   275 lemma 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
```
```   280 lemma 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
```
```   285 lemma permutations_of_set_lists: "permutations_of_set A \<subseteq> lists A"
```
```   286   unfolding permutations_of_set_def by auto
```
```   287
```
```   288 lemma permutations_of_set_empty [simp]: "permutations_of_set {} = {[]}"
```
```   289   by (auto simp: permutations_of_set_def)
```
```   290
```
```   291 lemma 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
```
```   295 lemma permutations_of_set_infinite:
```
```   296   "\<not>finite A \<Longrightarrow> permutations_of_set A = {}"
```
```   297   by (auto simp: permutations_of_set_def)
```
```   298
```
```   299 lemma 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
```
```   306 lemma permutations_of_set_singleton [simp]: "permutations_of_set {x} = {[x]}"
```
```   307   by (subst permutations_of_set_nonempty) auto
```
```   308
```
```   309 lemma 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
```
```   314 lemma 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
```
```   318 lemma 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
```
```   322 lemma 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
```
```   325 lemma 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
```
```   329 lemma 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
```
```   333 lemma 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
```
```   340 lemma 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
```
```   346 subsection \<open>Code generation\<close>
```
```   347
```
```   348 text \<open>
```
```   349   First, we give code an implementation for permutations of lists.
```
```   350 \<close>
```
```   351
```
```   352 declare length_remove1 [termination_simp]
```
```   353
```
```   354 fun 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
```
```   358 fun 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
```
```   362 declare permutations_of_list_impl_aux.simps [simp del]
```
```   363 declare permutations_of_list_impl.simps [simp del]
```
```   364
```
```   365 lemma permutations_of_list_impl_Nil [simp]:
```
```   366   "permutations_of_list_impl [] = [[]]"
```
```   367   by (simp add: permutations_of_list_impl.simps)
```
```   368
```
```   369 lemma 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
```
```   374 lemma 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
```
```   380 lemma 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
```
```   386 lemma 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
```
```   393 lemma 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
```
```   397 lemma 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
```
```   402 lemma 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
```
```   406 declare set_permutations_of_list_impl_aux [symmetric, code]
```
```   407
```
```   408 value [code] "permutations_of_multiset {#1,2,3,4::int#}"
```
```   409
```
```   410
```
```   411
```
```   412 text \<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>
```
```   416 function 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})))"
```
```   420 by auto
```
```   421 termination by (relation "Wellfounded.measure (card \<circ> snd)") (simp_all add: card_gt_0_iff)
```
```   422
```
```   423 lemma permutations_of_set_aux_altdef:
```
```   424   "permutations_of_set_aux acc A = (\<lambda>xs. rev xs @ acc) ` permutations_of_set A"
```
```   425 proof (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
```
```   445 qed (simp_all add: permutations_of_set_infinite)
```
```   446
```
```   447 declare permutations_of_set_aux.simps [simp del]
```
```   448
```
```   449 lemma 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
```
```   454 text \<open>
```
```   455   In another refinement step, we define a version on lists.
```
```   456 \<close>
```
```   457 declare length_remove1 [termination_simp]
```
```   458
```
```   459 fun 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
```
```   464 definition permutations_of_set_list where
```
```   465   "permutations_of_set_list xs = permutations_of_set_aux_list [] xs"
```
```   466
```
```   467 declare permutations_of_set_aux_list.simps [simp del]
```
```   468
```
```   469 lemma 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
```
```   479 text \<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>
```
```   486 lemma 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
```
```   493 lemma 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
```
```   497 lemma 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
```
```   502 lemma 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
```
```   509 value [code] "permutations_of_set (set ''abcd'')"
```
```   510
```
```   511 end
```