src/HOL/Library/Multiset_Permutations.thy
author haftmann
Mon Jan 14 18:35:03 2019 +0000 (7 months ago)
changeset 69661 a03a63b81f44
parent 68406 6beb45f6cf67
permissions -rw-r--r--
tuned proofs
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 \<open>Permutations of a Multiset\<close>
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 \<noteq> [] \<Longrightarrow> 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 {#}" "\<And>A. A \<noteq> {#} \<Longrightarrow> (\<And>x. x \<in># A \<Longrightarrow> P (A - {#x#})) \<Longrightarrow> 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 \<subset># 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 \<in># 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 \<circ> 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 \<Longrightarrow> mset_set A = mset xs \<Longrightarrow> 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 \<in># mset_set A" by simp
eberlm@63965
    55
  with Cons.prems(1) have [simp]: "x \<in> A" by simp
eberlm@63965
    56
  from Cons.prems have "x \<notin># 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 "\<dots> - {#x#} = mset xs" by simp
eberlm@63965
    61
  finally have [simp]: "x \<notin> 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 \<open>Permutations of a multiset\<close>
eberlm@63965
    68
eberlm@63965
    69
definition permutations_of_multiset :: "'a multiset \<Rightarrow> '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 \<Longrightarrow> xs \<in> 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 \<in> permutations_of_multiset A \<Longrightarrow> 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 \<in> permutations_of_multiset A \<longleftrightarrow> x \<in># A \<and> xs \<in> 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 \<noteq> {#}"
eberlm@63965
    87
  shows   "permutations_of_multiset A = 
nipkow@67399
    88
             (\<Union>x\<in>set_mset A. ((#) x) ` permutations_of_multiset (A - {#x#}))" (is "_ = ?rhs")
eberlm@63965
    89
proof safe
eberlm@63965
    90
  fix xs assume "xs \<in> 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 \<noteq> []" 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 \<in> set_mset A" "xs' \<in> permutations_of_multiset (A - {#x#})"
eberlm@63965
    95
    by (auto simp: permutations_of_multiset_def)
eberlm@63965
    96
  with xs show "xs \<in> ?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 \<subseteq> 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 \<subseteq> rev ` permutations_of_multiset A" .
eberlm@63965
   114
next
eberlm@63965
   115
  show "rev ` permutations_of_multiset A \<subseteq> 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 \<in> permutations_of_multiset A \<Longrightarrow> 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 \<subseteq> 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 \<subseteq> {xs. set xs \<subseteq> set_mset A \<and> length xs = size A}" 
eberlm@63965
   129
    by (auto simp: permutations_of_multiset_def)
eberlm@63965
   130
  show "finite {xs. set xs \<subseteq> set_mset A \<and> 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 \<noteq> {}"
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 \<in> 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 \<sigma> . note \<sigma> = this
eberlm@63965
   148
  with ys have "xs = map f (permute_list \<sigma> ys)"
eberlm@63965
   149
    by (simp add: permute_list_map)
eberlm@63965
   150
  moreover from \<sigma> ys have "permute_list \<sigma> ys \<in> permutations_of_multiset A"
eberlm@63965
   151
    by (simp add: permutations_of_multiset_def)
eberlm@63965
   152
  ultimately show "xs \<in> 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 \<open>Cardinality of permutations\<close>
eberlm@63965
   157
eberlm@63965
   158
text \<open>
eberlm@63965
   159
  In this section, we prove some basic facts about the number of permutations of a multiset.
eberlm@63965
   160
\<close>
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
  "(\<Prod>y\<in>set_mset (A+{#x#}). fact (count (A+{#x#}) y)) =
eberlm@63965
   167
     (count A x + 1) * (\<Prod>y\<in>set_mset A. fact (count A y))"
eberlm@63965
   168
proof -
eberlm@63965
   169
  have "(\<Prod>y\<in>set_mset (A+{#x#}). fact (count (A+{#x#}) y)) =
eberlm@63965
   170
          (\<Prod>y\<in>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 "\<dots> = (count A x + 1) * (\<Prod>y\<in>set_mset (A+{#x#}). fact (count A y))"
haftmann@69661
   173
    by (simp add: prod.distrib)
eberlm@63965
   174
  also have "(\<Prod>y\<in>set_mset (A+{#x#}). fact (count A y)) = (\<Prod>y\<in>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 \<in># A \<Longrightarrow> (\<Prod>y\<in>set_mset A. fact (count A y)) =
eberlm@63965
   181
                   count A x * (\<Prod>y\<in>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) * (\<Prod>x\<in>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) = 
nipkow@67399
   189
          card (\<Union>x\<in>set_mset A. (#) x ` permutations_of_multiset (A - {#x#}))"
eberlm@63965
   190
    by (simp add: permutations_of_multiset_nonempty remove.hyps)
eberlm@63965
   191
  also have "\<dots> = (\<Sum>x\<in>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 "\<dots> * (\<Prod>x\<in>set_mset A. fact (count A x)) = 
eberlm@63965
   194
               (\<Sum>x\<in>set_mset A. card (permutations_of_multiset (A - {#x#})) * 
eberlm@63965
   195
                 (\<Prod>y\<in>set_mset A. fact (count A y)))"
nipkow@64267
   196
    by (subst sum_distrib_right) simp_all
eberlm@63965
   197
  also have "\<dots> = (\<Sum>x\<in>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 \<in># A"
eberlm@63965
   200
    have "card (permutations_of_multiset (A - {#x#})) * (\<Prod>y\<in>set_mset A. fact (count A y)) = 
eberlm@63965
   201
            count A x * (card (permutations_of_multiset (A - {#x#})) * 
eberlm@63965
   202
              (\<Prod>y\<in>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 "(\<Sum>x\<in>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 "\<dots> = 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 (\<Prod>x\<in>set_mset A. fact (count A x))"
eberlm@63965
   218
  "(\<Prod>x\<in>set_mset A. fact (count A x) :: nat) dvd fact (size A)"
nipkow@68406
   219
  by (simp_all flip: card_permutations_of_multiset_aux[of A])
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
                    (\<Prod>y\<in>set_mset A. fact (count A y)) =
eberlm@63965
   231
                (size A + 1) * card (permutations_of_multiset A) *
eberlm@63965
   232
                    (\<Prod>x\<in>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 \<in># 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 \<in># 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 \<in># 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 \<open>Permutations of a set\<close>
eberlm@63965
   266
eberlm@63965
   267
definition permutations_of_set :: "'a set \<Rightarrow> 'a list set" where
eberlm@63965
   268
  "permutations_of_set A = {xs. set xs = A \<and> distinct xs}"
eberlm@63965
   269
eberlm@63965
   270
lemma permutations_of_set_altdef:
eberlm@63965
   271
  "finite A \<Longrightarrow> 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 \<in> 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 \<in> 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 \<subseteq> 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 \<Longrightarrow> (\<Union>xs\<in>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
  "\<not>finite A \<Longrightarrow> 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 \<noteq> {} \<Longrightarrow> permutations_of_set A = 
eberlm@63965
   301
                  (\<Union>x\<in>A. (\<lambda>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 \<noteq> y \<Longrightarrow> 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 \<in> permutations_of_set A \<Longrightarrow> 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 = {} \<longleftrightarrow> \<not>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 \<Longrightarrow> 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
  "\<sigma> permutes A \<Longrightarrow> map \<sigma> ` 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 \<open>Code generation\<close>
eberlm@63965
   347
eberlm@63965
   348
text \<open>
eberlm@63965
   349
  First, we give code an implementation for permutations of lists.
eberlm@63965
   350
\<close>
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
nipkow@67399
   356
     List.bind (remdups xs) (\<lambda>x. map ((#) 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) (\<lambda>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 \<noteq> [] \<Longrightarrow> permutations_of_list_impl xs = 
nipkow@67399
   371
     List.bind (remdups xs) (\<lambda>x. map ((#) 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 (\<lambda>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 \<open>
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
\<close>
eberlm@63965
   416
function permutations_of_set_aux where
eberlm@63965
   417
  "permutations_of_set_aux acc A = 
eberlm@63965
   418
     (if \<not>finite A then {} else if A = {} then {acc} else 
eberlm@63965
   419
        (\<Union>x\<in>A. permutations_of_set_aux (x#acc) (A - {x})))"
eberlm@63965
   420
by auto
eberlm@63965
   421
termination by (relation "Wellfounded.measure (card \<circ> 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 = (\<lambda>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
                (\<Union>y\<in>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 "\<dots> = (\<Union>y\<in>A. (\<lambda>xs. rev xs @ acc) ` (\<lambda>xs. y # xs) ` permutations_of_set (A - {y}))"
haftmann@69661
   439
        apply (rule arg_cong [of _ _ Union], rule image_cong)
haftmann@69661
   440
         apply (simp_all add: image_image)
haftmann@69661
   441
        apply (subst psubset)
haftmann@69661
   442
         apply auto
haftmann@69661
   443
        done
eberlm@63965
   444
      also from False have "\<dots> = (\<lambda>xs. rev xs @ acc) ` permutations_of_set A"
eberlm@63965
   445
        by (subst (2) permutations_of_set_nonempty) (simp_all add: image_UN)
eberlm@63965
   446
      finally show ?thesis .
eberlm@63965
   447
    qed simp_all
eberlm@63965
   448
  qed
eberlm@63965
   449
qed (simp_all add: permutations_of_set_infinite)
eberlm@63965
   450
eberlm@63965
   451
declare permutations_of_set_aux.simps [simp del]
eberlm@63965
   452
eberlm@63965
   453
lemma permutations_of_set_aux_correct:
eberlm@63965
   454
  "permutations_of_set_aux [] A = permutations_of_set A"
eberlm@63965
   455
  by (simp add: permutations_of_set_aux_altdef)
eberlm@63965
   456
eberlm@63965
   457
eberlm@63965
   458
text \<open>
eberlm@63965
   459
  In another refinement step, we define a version on lists.
eberlm@63965
   460
\<close>
eberlm@63965
   461
declare length_remove1 [termination_simp]
eberlm@63965
   462
eberlm@63965
   463
fun permutations_of_set_aux_list where
eberlm@63965
   464
  "permutations_of_set_aux_list acc xs = 
eberlm@63965
   465
     (if xs = [] then [acc] else 
eberlm@63965
   466
        List.bind xs (\<lambda>x. permutations_of_set_aux_list (x#acc) (List.remove1 x xs)))"
eberlm@63965
   467
eberlm@63965
   468
definition permutations_of_set_list where
eberlm@63965
   469
  "permutations_of_set_list xs = permutations_of_set_aux_list [] xs"
eberlm@63965
   470
eberlm@63965
   471
declare permutations_of_set_aux_list.simps [simp del]
eberlm@63965
   472
eberlm@63965
   473
lemma permutations_of_set_aux_list_refine:
eberlm@63965
   474
  assumes "distinct xs"
eberlm@63965
   475
  shows   "set (permutations_of_set_aux_list acc xs) = permutations_of_set_aux acc (set xs)"
eberlm@63965
   476
  using assms
eberlm@63965
   477
  by (induction acc xs rule: permutations_of_set_aux_list.induct)
eberlm@63965
   478
     (subst permutations_of_set_aux_list.simps,
eberlm@63965
   479
      subst permutations_of_set_aux.simps,
haftmann@69661
   480
      simp_all add: set_list_bind)
eberlm@63965
   481
eberlm@63965
   482
eberlm@63965
   483
text \<open>
eberlm@63965
   484
  The permutation lists contain no duplicates if the inputs contain no duplicates.
eberlm@63965
   485
  Therefore, these functions can easily be used when working with a representation of
eberlm@63965
   486
  sets by distinct lists.
eberlm@63965
   487
  The same approach should generalise to any kind of set implementation that supports
eberlm@63965
   488
  a monadic bind operation, and since the results are disjoint, merging should be cheap.
eberlm@63965
   489
\<close>
eberlm@63965
   490
lemma distinct_permutations_of_set_aux_list:
eberlm@63965
   491
  "distinct xs \<Longrightarrow> distinct (permutations_of_set_aux_list acc xs)"
eberlm@63965
   492
  by (induction acc xs rule: permutations_of_set_aux_list.induct)
eberlm@63965
   493
     (subst permutations_of_set_aux_list.simps,
eberlm@63965
   494
      auto intro!: distinct_list_bind simp: disjoint_family_on_def 
eberlm@63965
   495
         permutations_of_set_aux_list_refine permutations_of_set_aux_altdef)
eberlm@63965
   496
eberlm@63965
   497
lemma distinct_permutations_of_set_list:
eberlm@63965
   498
    "distinct xs \<Longrightarrow> distinct (permutations_of_set_list xs)"
eberlm@63965
   499
  by (simp add: permutations_of_set_list_def distinct_permutations_of_set_aux_list)
eberlm@63965
   500
eberlm@63965
   501
lemma permutations_of_list:
eberlm@63965
   502
    "permutations_of_set (set xs) = set (permutations_of_set_list (remdups xs))"
eberlm@63965
   503
  by (simp add: permutations_of_set_aux_correct [symmetric] 
eberlm@63965
   504
        permutations_of_set_aux_list_refine permutations_of_set_list_def)
eberlm@63965
   505
eberlm@63965
   506
lemma permutations_of_list_code [code]:
eberlm@63965
   507
  "permutations_of_set (set xs) = set (permutations_of_set_list (remdups xs))"
eberlm@63965
   508
  "permutations_of_set (List.coset xs) = 
eberlm@63965
   509
     Code.abort (STR ''Permutation of set complement not supported'') 
eberlm@63965
   510
       (\<lambda>_. permutations_of_set (List.coset xs))"
eberlm@63965
   511
  by (simp_all add: permutations_of_list)
eberlm@63965
   512
eberlm@63965
   513
value [code] "permutations_of_set (set ''abcd'')"
eberlm@63965
   514
nipkow@64267
   515
end