src/HOL/Library/Multiset.thy
author nipkow
Sat Sep 10 14:11:04 2016 +0200 (2016-09-10)
changeset 63831 ea7471c921f5
parent 63830 2ea3725a34bd
child 63849 0dd6731060d7
permissions -rw-r--r--
more simp
wenzelm@10249
     1
(*  Title:      HOL/Library/Multiset.thy
paulson@15072
     2
    Author:     Tobias Nipkow, Markus Wenzel, Lawrence C Paulson, Norbert Voelker
blanchet@55129
     3
    Author:     Andrei Popescu, TU Muenchen
blanchet@59813
     4
    Author:     Jasmin Blanchette, Inria, LORIA, MPII
blanchet@59813
     5
    Author:     Dmitriy Traytel, TU Muenchen
blanchet@59813
     6
    Author:     Mathias Fleury, MPII
wenzelm@10249
     7
*)
wenzelm@10249
     8
wenzelm@60500
     9
section \<open>(Finite) multisets\<close>
wenzelm@10249
    10
nipkow@15131
    11
theory Multiset
haftmann@51599
    12
imports Main
nipkow@15131
    13
begin
wenzelm@10249
    14
wenzelm@60500
    15
subsection \<open>The type of multisets\<close>
wenzelm@10249
    16
wenzelm@60606
    17
definition "multiset = {f :: 'a \<Rightarrow> nat. finite {x. f x > 0}}"
wenzelm@60606
    18
wenzelm@60606
    19
typedef 'a multiset = "multiset :: ('a \<Rightarrow> nat) set"
haftmann@34943
    20
  morphisms count Abs_multiset
wenzelm@45694
    21
  unfolding multiset_def
wenzelm@10249
    22
proof
wenzelm@45694
    23
  show "(\<lambda>x. 0::nat) \<in> {f. finite {x. f x > 0}}" by simp
wenzelm@10249
    24
qed
wenzelm@10249
    25
bulwahn@47429
    26
setup_lifting type_definition_multiset
wenzelm@19086
    27
wenzelm@60606
    28
lemma multiset_eq_iff: "M = N \<longleftrightarrow> (\<forall>a. count M a = count N a)"
nipkow@39302
    29
  by (simp only: count_inject [symmetric] fun_eq_iff)
haftmann@34943
    30
wenzelm@60606
    31
lemma multiset_eqI: "(\<And>x. count A x = count B x) \<Longrightarrow> A = B"
nipkow@39302
    32
  using multiset_eq_iff by auto
haftmann@34943
    33
wenzelm@60606
    34
text \<open>Preservation of the representing set @{term multiset}.\<close>
wenzelm@60606
    35
wenzelm@60606
    36
lemma const0_in_multiset: "(\<lambda>a. 0) \<in> multiset"
haftmann@34943
    37
  by (simp add: multiset_def)
haftmann@34943
    38
wenzelm@60606
    39
lemma only1_in_multiset: "(\<lambda>b. if b = a then n else 0) \<in> multiset"
haftmann@34943
    40
  by (simp add: multiset_def)
haftmann@34943
    41
wenzelm@60606
    42
lemma union_preserves_multiset: "M \<in> multiset \<Longrightarrow> N \<in> multiset \<Longrightarrow> (\<lambda>a. M a + N a) \<in> multiset"
haftmann@34943
    43
  by (simp add: multiset_def)
haftmann@34943
    44
haftmann@34943
    45
lemma diff_preserves_multiset:
haftmann@34943
    46
  assumes "M \<in> multiset"
haftmann@34943
    47
  shows "(\<lambda>a. M a - N a) \<in> multiset"
haftmann@34943
    48
proof -
haftmann@34943
    49
  have "{x. N x < M x} \<subseteq> {x. 0 < M x}"
haftmann@34943
    50
    by auto
haftmann@34943
    51
  with assms show ?thesis
haftmann@34943
    52
    by (auto simp add: multiset_def intro: finite_subset)
haftmann@34943
    53
qed
haftmann@34943
    54
haftmann@41069
    55
lemma filter_preserves_multiset:
haftmann@34943
    56
  assumes "M \<in> multiset"
haftmann@34943
    57
  shows "(\<lambda>x. if P x then M x else 0) \<in> multiset"
haftmann@34943
    58
proof -
haftmann@34943
    59
  have "{x. (P x \<longrightarrow> 0 < M x) \<and> P x} \<subseteq> {x. 0 < M x}"
haftmann@34943
    60
    by auto
haftmann@34943
    61
  with assms show ?thesis
haftmann@34943
    62
    by (auto simp add: multiset_def intro: finite_subset)
haftmann@34943
    63
qed
haftmann@34943
    64
haftmann@34943
    65
lemmas in_multiset = const0_in_multiset only1_in_multiset
haftmann@41069
    66
  union_preserves_multiset diff_preserves_multiset filter_preserves_multiset
haftmann@34943
    67
haftmann@34943
    68
wenzelm@60500
    69
subsection \<open>Representing multisets\<close>
wenzelm@60500
    70
wenzelm@60500
    71
text \<open>Multiset enumeration\<close>
haftmann@34943
    72
huffman@48008
    73
instantiation multiset :: (type) cancel_comm_monoid_add
haftmann@25571
    74
begin
haftmann@25571
    75
bulwahn@47429
    76
lift_definition zero_multiset :: "'a multiset" is "\<lambda>a. 0"
bulwahn@47429
    77
by (rule const0_in_multiset)
haftmann@25571
    78
haftmann@34943
    79
abbreviation Mempty :: "'a multiset" ("{#}") where
haftmann@34943
    80
  "Mempty \<equiv> 0"
haftmann@25571
    81
wenzelm@60606
    82
lift_definition plus_multiset :: "'a multiset \<Rightarrow> 'a multiset \<Rightarrow> 'a multiset" is "\<lambda>M N. (\<lambda>a. M a + N a)"
bulwahn@47429
    83
by (rule union_preserves_multiset)
haftmann@25571
    84
wenzelm@60606
    85
lift_definition minus_multiset :: "'a multiset \<Rightarrow> 'a multiset \<Rightarrow> 'a multiset" is "\<lambda> M N. \<lambda>a. M a - N a"
haftmann@59815
    86
by (rule diff_preserves_multiset)
haftmann@59815
    87
huffman@48008
    88
instance
wenzelm@60678
    89
  by (standard; transfer; simp add: fun_eq_iff)
haftmann@25571
    90
haftmann@25571
    91
end
wenzelm@10249
    92
eberlm@63195
    93
context
eberlm@63195
    94
begin
eberlm@63195
    95
eberlm@63195
    96
qualified definition is_empty :: "'a multiset \<Rightarrow> bool" where
eberlm@63195
    97
  [code_abbrev]: "is_empty A \<longleftrightarrow> A = {#}"
eberlm@63195
    98
eberlm@63195
    99
end
eberlm@63195
   100
Mathias@63793
   101
lemma add_mset_in_multiset:
Mathias@63793
   102
  assumes M: \<open>M \<in> multiset\<close>
Mathias@63793
   103
  shows \<open>(\<lambda>b. if b = a then Suc (M b) else M b) \<in> multiset\<close>
Mathias@63793
   104
  using assms by (simp add: multiset_def insert_Collect[symmetric])
Mathias@63793
   105
Mathias@63793
   106
lift_definition add_mset :: "'a \<Rightarrow> 'a multiset \<Rightarrow> 'a multiset" is
Mathias@63793
   107
  "\<lambda>a M b. if b = a then Suc (M b) else M b"
Mathias@63793
   108
by (rule add_mset_in_multiset)
kleing@15869
   109
wenzelm@26145
   110
syntax
wenzelm@60606
   111
  "_multiset" :: "args \<Rightarrow> 'a multiset"    ("{#(_)#}")
nipkow@25507
   112
translations
Mathias@63793
   113
  "{#x, xs#}" == "CONST add_mset x {#xs#}"
Mathias@63793
   114
  "{#x#}" == "CONST add_mset x {#}"
nipkow@25507
   115
haftmann@34943
   116
lemma count_empty [simp]: "count {#} a = 0"
bulwahn@47429
   117
  by (simp add: zero_multiset.rep_eq)
wenzelm@10249
   118
Mathias@63793
   119
lemma count_add_mset [simp]:
Mathias@63793
   120
  "count (add_mset b A) a = (if b = a then Suc (count A a) else count A a)"
Mathias@63793
   121
  by (simp add: add_mset.rep_eq)
Mathias@63793
   122
Mathias@63793
   123
lemma count_single: "count {#b#} a = (if b = a then 1 else 0)"
Mathias@63793
   124
  by simp
Mathias@63793
   125
Mathias@63793
   126
lemma
Mathias@63793
   127
  add_mset_not_empty [simp]: \<open>add_mset a A \<noteq> {#}\<close> and
Mathias@63793
   128
  empty_not_add_mset [simp]: "{#} \<noteq> add_mset a A"
Mathias@63793
   129
  by (auto simp: multiset_eq_iff)
Mathias@63793
   130
Mathias@63793
   131
lemma add_mset_add_mset_same_iff [simp]:
Mathias@63793
   132
  "add_mset a A = add_mset a B \<longleftrightarrow> A = B"
Mathias@63793
   133
  by (auto simp: multiset_eq_iff)
Mathias@63793
   134
Mathias@63793
   135
lemma add_mset_commute:
Mathias@63793
   136
  "add_mset x (add_mset y M) = add_mset y (add_mset x M)"
Mathias@63793
   137
  by (auto simp: multiset_eq_iff)
nipkow@29901
   138
wenzelm@10249
   139
wenzelm@60500
   140
subsection \<open>Basic operations\<close>
wenzelm@60500
   141
haftmann@62430
   142
subsubsection \<open>Conversion to set and membership\<close>
haftmann@62430
   143
haftmann@62430
   144
definition set_mset :: "'a multiset \<Rightarrow> 'a set"
haftmann@62430
   145
  where "set_mset M = {x. count M x > 0}"
haftmann@62430
   146
haftmann@62537
   147
abbreviation Melem :: "'a \<Rightarrow> 'a multiset \<Rightarrow> bool"
haftmann@62537
   148
  where "Melem a M \<equiv> a \<in> set_mset M"
haftmann@62537
   149
haftmann@62537
   150
notation
haftmann@62537
   151
  Melem  ("op \<in>#") and
haftmann@62537
   152
  Melem  ("(_/ \<in># _)" [51, 51] 50)
haftmann@62537
   153
haftmann@62537
   154
notation  (ASCII)
haftmann@62537
   155
  Melem  ("op :#") and
haftmann@62537
   156
  Melem  ("(_/ :# _)" [51, 51] 50)
haftmann@62537
   157
haftmann@62537
   158
abbreviation not_Melem :: "'a \<Rightarrow> 'a multiset \<Rightarrow> bool"
haftmann@62537
   159
  where "not_Melem a M \<equiv> a \<notin> set_mset M"
haftmann@62537
   160
haftmann@62537
   161
notation
haftmann@62537
   162
  not_Melem  ("op \<notin>#") and
haftmann@62537
   163
  not_Melem  ("(_/ \<notin># _)" [51, 51] 50)
haftmann@62537
   164
haftmann@62537
   165
notation  (ASCII)
haftmann@62537
   166
  not_Melem  ("op ~:#") and
haftmann@62537
   167
  not_Melem  ("(_/ ~:# _)" [51, 51] 50)
haftmann@62430
   168
haftmann@62430
   169
context
haftmann@62430
   170
begin
haftmann@62430
   171
haftmann@62430
   172
qualified abbreviation Ball :: "'a multiset \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> bool"
haftmann@62430
   173
  where "Ball M \<equiv> Set.Ball (set_mset M)"
haftmann@62430
   174
haftmann@62430
   175
qualified abbreviation Bex :: "'a multiset \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> bool"
haftmann@62430
   176
  where "Bex M \<equiv> Set.Bex (set_mset M)"
haftmann@62430
   177
haftmann@62430
   178
end
haftmann@62430
   179
haftmann@62430
   180
syntax
haftmann@62430
   181
  "_MBall"       :: "pttrn \<Rightarrow> 'a set \<Rightarrow> bool \<Rightarrow> bool"      ("(3\<forall>_\<in>#_./ _)" [0, 0, 10] 10)
haftmann@62430
   182
  "_MBex"        :: "pttrn \<Rightarrow> 'a set \<Rightarrow> bool \<Rightarrow> bool"      ("(3\<exists>_\<in>#_./ _)" [0, 0, 10] 10)
haftmann@62430
   183
haftmann@62537
   184
syntax  (ASCII)
haftmann@62537
   185
  "_MBall"       :: "pttrn \<Rightarrow> 'a set \<Rightarrow> bool \<Rightarrow> bool"      ("(3\<forall>_:#_./ _)" [0, 0, 10] 10)
haftmann@62537
   186
  "_MBex"        :: "pttrn \<Rightarrow> 'a set \<Rightarrow> bool \<Rightarrow> bool"      ("(3\<exists>_:#_./ _)" [0, 0, 10] 10)
haftmann@62537
   187
haftmann@62430
   188
translations
haftmann@62430
   189
  "\<forall>x\<in>#A. P" \<rightleftharpoons> "CONST Multiset.Ball A (\<lambda>x. P)"
haftmann@62430
   190
  "\<exists>x\<in>#A. P" \<rightleftharpoons> "CONST Multiset.Bex A (\<lambda>x. P)"
haftmann@62430
   191
haftmann@62430
   192
lemma count_eq_zero_iff:
haftmann@62430
   193
  "count M x = 0 \<longleftrightarrow> x \<notin># M"
haftmann@62430
   194
  by (auto simp add: set_mset_def)
haftmann@62430
   195
haftmann@62430
   196
lemma not_in_iff:
haftmann@62430
   197
  "x \<notin># M \<longleftrightarrow> count M x = 0"
haftmann@62430
   198
  by (auto simp add: count_eq_zero_iff)
haftmann@62430
   199
haftmann@62430
   200
lemma count_greater_zero_iff [simp]:
haftmann@62430
   201
  "count M x > 0 \<longleftrightarrow> x \<in># M"
haftmann@62430
   202
  by (auto simp add: set_mset_def)
haftmann@62430
   203
haftmann@62430
   204
lemma count_inI:
haftmann@62430
   205
  assumes "count M x = 0 \<Longrightarrow> False"
haftmann@62430
   206
  shows "x \<in># M"
haftmann@62430
   207
proof (rule ccontr)
haftmann@62430
   208
  assume "x \<notin># M"
haftmann@62430
   209
  with assms show False by (simp add: not_in_iff)
haftmann@62430
   210
qed
haftmann@62430
   211
haftmann@62430
   212
lemma in_countE:
haftmann@62430
   213
  assumes "x \<in># M"
haftmann@62430
   214
  obtains n where "count M x = Suc n"
haftmann@62430
   215
proof -
haftmann@62430
   216
  from assms have "count M x > 0" by simp
haftmann@62430
   217
  then obtain n where "count M x = Suc n"
haftmann@62430
   218
    using gr0_conv_Suc by blast
haftmann@62430
   219
  with that show thesis .
haftmann@62430
   220
qed
haftmann@62430
   221
haftmann@62430
   222
lemma count_greater_eq_Suc_zero_iff [simp]:
haftmann@62430
   223
  "count M x \<ge> Suc 0 \<longleftrightarrow> x \<in># M"
haftmann@62430
   224
  by (simp add: Suc_le_eq)
haftmann@62430
   225
haftmann@62430
   226
lemma count_greater_eq_one_iff [simp]:
haftmann@62430
   227
  "count M x \<ge> 1 \<longleftrightarrow> x \<in># M"
haftmann@62430
   228
  by simp
haftmann@62430
   229
haftmann@62430
   230
lemma set_mset_empty [simp]:
haftmann@62430
   231
  "set_mset {#} = {}"
haftmann@62430
   232
  by (simp add: set_mset_def)
haftmann@62430
   233
Mathias@63793
   234
lemma set_mset_single:
haftmann@62430
   235
  "set_mset {#b#} = {b}"
haftmann@62430
   236
  by (simp add: set_mset_def)
haftmann@62430
   237
haftmann@62430
   238
lemma set_mset_eq_empty_iff [simp]:
haftmann@62430
   239
  "set_mset M = {} \<longleftrightarrow> M = {#}"
haftmann@62430
   240
  by (auto simp add: multiset_eq_iff count_eq_zero_iff)
haftmann@62430
   241
haftmann@62430
   242
lemma finite_set_mset [iff]:
haftmann@62430
   243
  "finite (set_mset M)"
haftmann@62430
   244
  using count [of M] by (simp add: multiset_def)
haftmann@62430
   245
Mathias@63793
   246
lemma set_mset_add_mset_insert [simp]: \<open>set_mset (add_mset a A) = insert a (set_mset A)\<close>
Mathias@63793
   247
  by (auto simp del: count_greater_eq_Suc_zero_iff
Mathias@63793
   248
      simp: count_greater_eq_Suc_zero_iff[symmetric] split: if_splits)
Mathias@63793
   249
haftmann@62430
   250
wenzelm@60500
   251
subsubsection \<open>Union\<close>
wenzelm@10249
   252
haftmann@62430
   253
lemma count_union [simp]:
haftmann@62430
   254
  "count (M + N) a = count M a + count N a"
bulwahn@47429
   255
  by (simp add: plus_multiset.rep_eq)
wenzelm@10249
   256
haftmann@62430
   257
lemma set_mset_union [simp]:
haftmann@62430
   258
  "set_mset (M + N) = set_mset M \<union> set_mset N"
haftmann@62430
   259
  by (simp only: set_eq_iff count_greater_zero_iff [symmetric] count_union) simp
haftmann@62430
   260
Mathias@63793
   261
lemma union_mset_add_mset_left [simp]:
Mathias@63793
   262
  "add_mset a A + B = add_mset a (A + B)"
Mathias@63793
   263
  by (auto simp: multiset_eq_iff)
Mathias@63793
   264
Mathias@63793
   265
lemma union_mset_add_mset_right [simp]:
Mathias@63793
   266
  "A + add_mset a B = add_mset a (A + B)"
Mathias@63793
   267
  by (auto simp: multiset_eq_iff)
Mathias@63793
   268
Mathias@63793
   269
lemma add_mset_add_single: \<open>add_mset a A = A + {#a#}\<close>
Mathias@63793
   270
  by (subst union_mset_add_mset_right, subst add.comm_neutral) standard
Mathias@63793
   271
wenzelm@10249
   272
wenzelm@60500
   273
subsubsection \<open>Difference\<close>
wenzelm@10249
   274
haftmann@62430
   275
instance multiset :: (type) comm_monoid_diff
haftmann@62430
   276
  by standard (transfer; simp add: fun_eq_iff)
haftmann@62430
   277
haftmann@62430
   278
lemma count_diff [simp]:
haftmann@62430
   279
  "count (M - N) a = count M a - count N a"
bulwahn@47429
   280
  by (simp add: minus_multiset.rep_eq)
haftmann@34943
   281
Mathias@63793
   282
lemma add_mset_diff_bothsides:
Mathias@63793
   283
  \<open>add_mset a M - add_mset a A = M - A\<close>
Mathias@63793
   284
  by (auto simp: multiset_eq_iff)
Mathias@63793
   285
haftmann@62430
   286
lemma in_diff_count:
haftmann@62430
   287
  "a \<in># M - N \<longleftrightarrow> count N a < count M a"
haftmann@62430
   288
  by (simp add: set_mset_def)
haftmann@62430
   289
haftmann@62430
   290
lemma count_in_diffI:
haftmann@62430
   291
  assumes "\<And>n. count N x = n + count M x \<Longrightarrow> False"
haftmann@62430
   292
  shows "x \<in># M - N"
haftmann@62430
   293
proof (rule ccontr)
haftmann@62430
   294
  assume "x \<notin># M - N"
haftmann@62430
   295
  then have "count N x = (count N x - count M x) + count M x"
haftmann@62430
   296
    by (simp add: in_diff_count not_less)
haftmann@62430
   297
  with assms show False by auto
haftmann@62430
   298
qed
haftmann@62430
   299
haftmann@62430
   300
lemma in_diff_countE:
haftmann@62430
   301
  assumes "x \<in># M - N"
haftmann@62430
   302
  obtains n where "count M x = Suc n + count N x"
haftmann@62430
   303
proof -
haftmann@62430
   304
  from assms have "count M x - count N x > 0" by (simp add: in_diff_count)
haftmann@62430
   305
  then have "count M x > count N x" by simp
haftmann@62430
   306
  then obtain n where "count M x = Suc n + count N x"
haftmann@62430
   307
    using less_iff_Suc_add by auto
haftmann@62430
   308
  with that show thesis .
haftmann@62430
   309
qed
haftmann@62430
   310
haftmann@62430
   311
lemma in_diffD:
haftmann@62430
   312
  assumes "a \<in># M - N"
haftmann@62430
   313
  shows "a \<in># M"
haftmann@62430
   314
proof -
haftmann@62430
   315
  have "0 \<le> count N a" by simp
haftmann@62430
   316
  also from assms have "count N a < count M a"
haftmann@62430
   317
    by (simp add: in_diff_count)
haftmann@62430
   318
  finally show ?thesis by simp
haftmann@62430
   319
qed
haftmann@62430
   320
haftmann@62430
   321
lemma set_mset_diff:
haftmann@62430
   322
  "set_mset (M - N) = {a. count N a < count M a}"
haftmann@62430
   323
  by (simp add: set_mset_def)
haftmann@62430
   324
wenzelm@17161
   325
lemma diff_empty [simp]: "M - {#} = M \<and> {#} - M = {#}"
haftmann@52289
   326
  by rule (fact Groups.diff_zero, fact Groups.zero_diff)
nipkow@36903
   327
Mathias@63793
   328
lemma diff_cancel: "A - A = {#}"
haftmann@52289
   329
  by (fact Groups.diff_cancel)
wenzelm@10249
   330
Mathias@63793
   331
lemma diff_union_cancelR: "M + N - N = (M::'a multiset)"
haftmann@52289
   332
  by (fact add_diff_cancel_right')
wenzelm@10249
   333
Mathias@63793
   334
lemma diff_union_cancelL: "N + M - N = (M::'a multiset)"
haftmann@52289
   335
  by (fact add_diff_cancel_left')
haftmann@34943
   336
haftmann@52289
   337
lemma diff_right_commute:
wenzelm@60606
   338
  fixes M N Q :: "'a multiset"
wenzelm@60606
   339
  shows "M - N - Q = M - Q - N"
haftmann@52289
   340
  by (fact diff_right_commute)
haftmann@52289
   341
haftmann@52289
   342
lemma diff_add:
wenzelm@60606
   343
  fixes M N Q :: "'a multiset"
wenzelm@60606
   344
  shows "M - (N + Q) = M - N - Q"
haftmann@52289
   345
  by (rule sym) (fact diff_diff_add)
blanchet@58425
   346
Mathias@63793
   347
lemma insert_DiffM [simp]: "x \<in># M \<Longrightarrow> add_mset x (M - {#x#}) = M"
nipkow@39302
   348
  by (clarsimp simp: multiset_eq_iff)
haftmann@34943
   349
Mathias@63793
   350
lemma insert_DiffM2: "x \<in># M \<Longrightarrow> (M - {#x#}) + {#x#} = M"
Mathias@63793
   351
  by simp
Mathias@63793
   352
Mathias@63793
   353
lemma diff_union_swap: "a \<noteq> b \<Longrightarrow> add_mset b (M - {#a#}) = add_mset b M - {#a#}"
nipkow@39302
   354
  by (auto simp add: multiset_eq_iff)
haftmann@34943
   355
Mathias@63793
   356
lemma diff_add_mset_swap [simp]: "b \<notin># A \<Longrightarrow> add_mset b M - A = add_mset b (M - A)"
Mathias@63793
   357
  by (auto simp add: multiset_eq_iff simp: not_in_iff)
Mathias@63793
   358
Mathias@63793
   359
lemma diff_union_swap2 [simp]: "y \<in># M \<Longrightarrow> add_mset x M - {#y#} = add_mset x (M - {#y#})"
Mathias@63793
   360
  by (metis add_mset_diff_bothsides diff_union_swap diff_zero insert_DiffM)
Mathias@63793
   361
Mathias@63793
   362
lemma diff_diff_add_mset [simp]: "(M::'a multiset) - N - P = M - (N + P)"
Mathias@63793
   363
  by (rule diff_diff_add)
Mathias@63793
   364
haftmann@62430
   365
lemma diff_union_single_conv:
haftmann@62430
   366
  "a \<in># J \<Longrightarrow> I + J - {#a#} = I + (J - {#a#})"
haftmann@62430
   367
  by (simp add: multiset_eq_iff Suc_le_eq)
haftmann@62430
   368
haftmann@62430
   369
lemma mset_add [elim?]:
haftmann@62430
   370
  assumes "a \<in># A"
Mathias@63793
   371
  obtains B where "A = add_mset a B"
haftmann@62430
   372
proof -
Mathias@63793
   373
  from assms have "A = add_mset a (A - {#a#})"
haftmann@62430
   374
    by simp
haftmann@62430
   375
  with that show thesis .
haftmann@62430
   376
qed
haftmann@62430
   377
haftmann@62430
   378
lemma union_iff:
haftmann@62430
   379
  "a \<in># A + B \<longleftrightarrow> a \<in># A \<or> a \<in># B"
haftmann@62430
   380
  by auto
bulwahn@26143
   381
wenzelm@10249
   382
wenzelm@60500
   383
subsubsection \<open>Equality of multisets\<close>
haftmann@34943
   384
haftmann@34943
   385
lemma single_eq_single [simp]: "{#a#} = {#b#} \<longleftrightarrow> a = b"
nipkow@39302
   386
  by (auto simp add: multiset_eq_iff)
haftmann@34943
   387
haftmann@34943
   388
lemma union_eq_empty [iff]: "M + N = {#} \<longleftrightarrow> M = {#} \<and> N = {#}"
nipkow@39302
   389
  by (auto simp add: multiset_eq_iff)
haftmann@34943
   390
haftmann@34943
   391
lemma empty_eq_union [iff]: "{#} = M + N \<longleftrightarrow> M = {#} \<and> N = {#}"
nipkow@39302
   392
  by (auto simp add: multiset_eq_iff)
haftmann@34943
   393
Mathias@63793
   394
lemma multi_self_add_other_not_self [simp]: "M = add_mset x M \<longleftrightarrow> False"
nipkow@39302
   395
  by (auto simp add: multiset_eq_iff)
haftmann@34943
   396
Mathias@63793
   397
lemma add_mset_remove_trivial [simp]: \<open>add_mset x M - {#x#} = M\<close>
Mathias@63793
   398
  by (auto simp: multiset_eq_iff)
Mathias@63793
   399
wenzelm@60606
   400
lemma diff_single_trivial: "\<not> x \<in># M \<Longrightarrow> M - {#x#} = M"
haftmann@62430
   401
  by (auto simp add: multiset_eq_iff not_in_iff)
haftmann@34943
   402
Mathias@63793
   403
lemma diff_single_eq_union: "x \<in># M \<Longrightarrow> M - {#x#} = N \<longleftrightarrow> M = add_mset x N"
Mathias@63793
   404
  by auto
Mathias@63793
   405
Mathias@63793
   406
lemma union_single_eq_diff: "add_mset x M = N \<Longrightarrow> M = N - {#x#}"
Mathias@63793
   407
  unfolding add_mset_add_single[of _ M] by (fact add_implies_diff)
Mathias@63793
   408
Mathias@63793
   409
lemma union_single_eq_member: "add_mset x M = N \<Longrightarrow> x \<in># N"
haftmann@34943
   410
  by auto
haftmann@34943
   411
Mathias@63793
   412
lemma add_mset_remove_trivial_If:
Mathias@63793
   413
  "add_mset a (N - {#a#}) = (if a \<in># N then N else add_mset a N)"
Mathias@63793
   414
  by (simp add: diff_single_trivial)
Mathias@63793
   415
Mathias@63793
   416
lemma add_mset_remove_trivial_eq: \<open>N = add_mset a (N - {#a#}) \<longleftrightarrow> a \<in># N\<close>
Mathias@63793
   417
  by (auto simp: add_mset_remove_trivial_If)
haftmann@34943
   418
haftmann@62430
   419
lemma union_is_single:
haftmann@62430
   420
  "M + N = {#a#} \<longleftrightarrow> M = {#a#} \<and> N = {#} \<or> M = {#} \<and> N = {#a#}"
wenzelm@60606
   421
  (is "?lhs = ?rhs")
wenzelm@46730
   422
proof
wenzelm@60606
   423
  show ?lhs if ?rhs using that by auto
wenzelm@60606
   424
  show ?rhs if ?lhs
haftmann@62430
   425
    by (metis Multiset.diff_cancel add.commute add_diff_cancel_left' diff_add_zero diff_single_trivial insert_DiffM that)
haftmann@34943
   426
qed
haftmann@34943
   427
wenzelm@60606
   428
lemma single_is_union: "{#a#} = M + N \<longleftrightarrow> {#a#} = M \<and> N = {#} \<or> M = {#} \<and> {#a#} = N"
haftmann@34943
   429
  by (auto simp add: eq_commute [of "{#a#}" "M + N"] union_is_single)
haftmann@34943
   430
haftmann@34943
   431
lemma add_eq_conv_diff:
Mathias@63793
   432
  "add_mset a M = add_mset b N \<longleftrightarrow> M = N \<and> a = b \<or> M = add_mset b (N - {#a#}) \<and> N = add_mset a (M - {#b#})"
wenzelm@60606
   433
  (is "?lhs \<longleftrightarrow> ?rhs")
nipkow@44890
   434
(* shorter: by (simp add: multiset_eq_iff) fastforce *)
haftmann@34943
   435
proof
wenzelm@60606
   436
  show ?lhs if ?rhs
wenzelm@60606
   437
    using that
Mathias@63793
   438
    by (auto simp add: add_mset_commute[of a b])
wenzelm@60606
   439
  show ?rhs if ?lhs
haftmann@34943
   440
  proof (cases "a = b")
wenzelm@60500
   441
    case True with \<open>?lhs\<close> show ?thesis by simp
haftmann@34943
   442
  next
haftmann@34943
   443
    case False
Mathias@63793
   444
    from \<open>?lhs\<close> have "a \<in># add_mset b N" by (rule union_single_eq_member)
haftmann@34943
   445
    with False have "a \<in># N" by auto
Mathias@63793
   446
    moreover from \<open>?lhs\<close> have "M = add_mset b N - {#a#}" by (rule union_single_eq_diff)
haftmann@34943
   447
    moreover note False
Mathias@63793
   448
    ultimately show ?thesis by (auto simp add: diff_right_commute [of _ "{#a#}"])
haftmann@34943
   449
  qed
haftmann@34943
   450
qed
haftmann@34943
   451
Mathias@63793
   452
lemma add_mset_eq_single [iff]: "add_mset b M = {#a#} \<longleftrightarrow> b = a \<and> M = {#}"
Mathias@63793
   453
  by (auto simp: add_eq_conv_diff)
Mathias@63793
   454
Mathias@63793
   455
lemma single_eq_add_mset [iff]: "{#a#} = add_mset b M \<longleftrightarrow> b = a \<and> M = {#}"
Mathias@63793
   456
  by (auto simp: add_eq_conv_diff)
Mathias@63793
   457
blanchet@58425
   458
lemma insert_noteq_member:
Mathias@63793
   459
  assumes BC: "add_mset b B = add_mset c C"
haftmann@34943
   460
   and bnotc: "b \<noteq> c"
haftmann@34943
   461
  shows "c \<in># B"
haftmann@34943
   462
proof -
Mathias@63793
   463
  have "c \<in># add_mset c C" by simp
haftmann@34943
   464
  have nc: "\<not> c \<in># {#b#}" using bnotc by simp
Mathias@63793
   465
  then have "c \<in># add_mset b B" using BC by simp
haftmann@34943
   466
  then show "c \<in># B" using nc by simp
haftmann@34943
   467
qed
haftmann@34943
   468
haftmann@34943
   469
lemma add_eq_conv_ex:
Mathias@63793
   470
  "(add_mset a M = add_mset b N) =
Mathias@63793
   471
    (M = N \<and> a = b \<or> (\<exists>K. M = add_mset b K \<and> N = add_mset a K))"
haftmann@34943
   472
  by (auto simp add: add_eq_conv_diff)
haftmann@34943
   473
Mathias@63793
   474
lemma multi_member_split: "x \<in># M \<Longrightarrow> \<exists>A. M = add_mset x A"
wenzelm@60678
   475
  by (rule exI [where x = "M - {#x#}"]) simp
haftmann@51600
   476
blanchet@58425
   477
lemma multiset_add_sub_el_shuffle:
wenzelm@60606
   478
  assumes "c \<in># B"
wenzelm@60606
   479
    and "b \<noteq> c"
Mathias@63793
   480
  shows "add_mset b (B - {#c#}) = add_mset b B - {#c#}"
haftmann@58098
   481
proof -
Mathias@63793
   482
  from \<open>c \<in># B\<close> obtain A where B: "B = add_mset c A"
haftmann@58098
   483
    by (blast dest: multi_member_split)
Mathias@63793
   484
  have "add_mset b A = add_mset c (add_mset b A) - {#c#}" by simp
Mathias@63793
   485
  then have "add_mset b A = add_mset b (add_mset c A) - {#c#}"
Mathias@63794
   486
    by (simp add: \<open>b \<noteq> c\<close>)
haftmann@58098
   487
  then show ?thesis using B by simp
haftmann@58098
   488
qed
haftmann@58098
   489
haftmann@34943
   490
wenzelm@60500
   491
subsubsection \<open>Pointwise ordering induced by count\<close>
haftmann@34943
   492
wenzelm@61955
   493
definition subseteq_mset :: "'a multiset \<Rightarrow> 'a multiset \<Rightarrow> bool"  (infix "\<subseteq>#" 50)
wenzelm@61955
   494
  where "A \<subseteq># B = (\<forall>a. count A a \<le> count B a)"
wenzelm@61955
   495
wenzelm@61955
   496
definition subset_mset :: "'a multiset \<Rightarrow> 'a multiset \<Rightarrow> bool" (infix "\<subset>#" 50)
wenzelm@61955
   497
  where "A \<subset># B = (A \<subseteq># B \<and> A \<noteq> B)"
wenzelm@61955
   498
haftmann@62430
   499
abbreviation (input) supseteq_mset :: "'a multiset \<Rightarrow> 'a multiset \<Rightarrow> bool"  (infix "\<supseteq>#" 50)
haftmann@62430
   500
  where "supseteq_mset A B \<equiv> B \<subseteq># A"
haftmann@62430
   501
haftmann@62430
   502
abbreviation (input) supset_mset :: "'a multiset \<Rightarrow> 'a multiset \<Rightarrow> bool"  (infix "\<supset>#" 50)
haftmann@62430
   503
  where "supset_mset A B \<equiv> B \<subset># A"
blanchet@62208
   504
wenzelm@61955
   505
notation (input)
blanchet@62208
   506
  subseteq_mset  (infix "\<le>#" 50) and
haftmann@62430
   507
  supseteq_mset  (infix "\<ge>#" 50)
wenzelm@61955
   508
wenzelm@61955
   509
notation (ASCII)
wenzelm@61955
   510
  subseteq_mset  (infix "<=#" 50) and
blanchet@62208
   511
  subset_mset  (infix "<#" 50) and
blanchet@62208
   512
  supseteq_mset  (infix ">=#" 50) and
blanchet@62208
   513
  supset_mset  (infix ">#" 50)
Mathias@60397
   514
wenzelm@60606
   515
interpretation subset_mset: ordered_ab_semigroup_add_imp_le "op +" "op -" "op \<subseteq>#" "op \<subset>#"
wenzelm@60678
   516
  by standard (auto simp add: subset_mset_def subseteq_mset_def multiset_eq_iff intro: order_trans antisym)
wenzelm@62837
   517
  \<comment> \<open>FIXME: avoid junk stemming from type class interpretation\<close>
haftmann@62430
   518
Mathias@63793
   519
interpretation subset_mset: ordered_ab_semigroup_monoid_add_imp_le "op +" 0 "op -" "op \<le>#" "op <#"
Mathias@63793
   520
  by standard
Mathias@63793
   521
Mathias@63310
   522
lemma mset_subset_eqI:
haftmann@62430
   523
  "(\<And>a. count A a \<le> count B a) \<Longrightarrow> A \<subseteq># B"
Mathias@60397
   524
  by (simp add: subseteq_mset_def)
haftmann@34943
   525
Mathias@63310
   526
lemma mset_subset_eq_count:
haftmann@62430
   527
  "A \<subseteq># B \<Longrightarrow> count A a \<le> count B a"
haftmann@62430
   528
  by (simp add: subseteq_mset_def)
haftmann@62430
   529
Mathias@63310
   530
lemma mset_subset_eq_exists_conv: "(A::'a multiset) \<subseteq># B \<longleftrightarrow> (\<exists>C. B = A + C)"
wenzelm@60678
   531
  unfolding subseteq_mset_def
wenzelm@60678
   532
  apply (rule iffI)
wenzelm@60678
   533
   apply (rule exI [where x = "B - A"])
wenzelm@60678
   534
   apply (auto intro: multiset_eq_iff [THEN iffD2])
wenzelm@60678
   535
  done
haftmann@34943
   536
Mathias@63560
   537
interpretation subset_mset: ordered_cancel_comm_monoid_diff "op +" 0 "op \<le>#" "op <#" "op -"
Mathias@63310
   538
  by standard (simp, fact mset_subset_eq_exists_conv)
Mathias@63310
   539
Mathias@63793
   540
lemma mset_subset_eq_mono_add_right_cancel: "(A::'a multiset) + C \<subseteq># B + C \<longleftrightarrow> A \<subseteq># B"
haftmann@62430
   541
   by (fact subset_mset.add_le_cancel_right)
Mathias@63793
   542
Mathias@63793
   543
lemma mset_subset_eq_mono_add_left_cancel: "C + (A::'a multiset) \<subseteq># C + B \<longleftrightarrow> A \<subseteq># B"
haftmann@62430
   544
   by (fact subset_mset.add_le_cancel_left)
Mathias@63793
   545
Mathias@63310
   546
lemma mset_subset_eq_mono_add: "(A::'a multiset) \<subseteq># B \<Longrightarrow> C \<subseteq># D \<Longrightarrow> A + C \<subseteq># B + D"
haftmann@62430
   547
   by (fact subset_mset.add_mono)
Mathias@63793
   548
Mathias@63560
   549
lemma mset_subset_eq_add_left: "(A::'a multiset) \<subseteq># A + B"
Mathias@63560
   550
   by simp
Mathias@63793
   551
Mathias@63560
   552
lemma mset_subset_eq_add_right: "B \<subseteq># (A::'a multiset) + B"
Mathias@63560
   553
   by simp
Mathias@63793
   554
haftmann@62430
   555
lemma single_subset_iff [simp]:
haftmann@62430
   556
  "{#a#} \<subseteq># M \<longleftrightarrow> a \<in># M"
haftmann@62430
   557
  by (auto simp add: subseteq_mset_def Suc_le_eq)
haftmann@62430
   558
Mathias@63310
   559
lemma mset_subset_eq_single: "a \<in># B \<Longrightarrow> {#a#} \<subseteq># B"
Mathias@63795
   560
  by simp
Mathias@63793
   561
Mathias@63793
   562
lemma mset_subset_eq_add_mset_cancel: \<open>add_mset a A \<subseteq># add_mset a B \<longleftrightarrow> A \<subseteq># B\<close>
Mathias@63793
   563
  unfolding add_mset_add_single[of _ A] add_mset_add_single[of _ B]
Mathias@63793
   564
  by (rule mset_subset_eq_mono_add_right_cancel)
Mathias@63793
   565
haftmann@35268
   566
lemma multiset_diff_union_assoc:
wenzelm@60606
   567
  fixes A B C D :: "'a multiset"
haftmann@62430
   568
  shows "C \<subseteq># B \<Longrightarrow> A + B - C = A + (B - C)"
haftmann@62430
   569
  by (fact subset_mset.diff_add_assoc)
Mathias@63793
   570
Mathias@63310
   571
lemma mset_subset_eq_multiset_union_diff_commute:
wenzelm@60606
   572
  fixes A B C D :: "'a multiset"
haftmann@62430
   573
  shows "B \<subseteq># A \<Longrightarrow> A - B + C = A + C - B"
haftmann@62430
   574
  by (fact subset_mset.add_diff_assoc2)
haftmann@62430
   575
Mathias@63310
   576
lemma diff_subset_eq_self[simp]:
haftmann@62430
   577
  "(M::'a multiset) - N \<subseteq># M"
haftmann@62430
   578
  by (simp add: subseteq_mset_def)
haftmann@62430
   579
Mathias@63310
   580
lemma mset_subset_eqD:
haftmann@62430
   581
  assumes "A \<subseteq># B" and "x \<in># A"
haftmann@62430
   582
  shows "x \<in># B"
haftmann@62430
   583
proof -
haftmann@62430
   584
  from \<open>x \<in># A\<close> have "count A x > 0" by simp
haftmann@62430
   585
  also from \<open>A \<subseteq># B\<close> have "count A x \<le> count B x"
haftmann@62430
   586
    by (simp add: subseteq_mset_def)
haftmann@62430
   587
  finally show ?thesis by simp
haftmann@62430
   588
qed
Mathias@63793
   589
Mathias@63310
   590
lemma mset_subsetD:
haftmann@62430
   591
  "A \<subset># B \<Longrightarrow> x \<in># A \<Longrightarrow> x \<in># B"
Mathias@63310
   592
  by (auto intro: mset_subset_eqD [of A])
haftmann@62430
   593
haftmann@62430
   594
lemma set_mset_mono:
haftmann@62430
   595
  "A \<subseteq># B \<Longrightarrow> set_mset A \<subseteq> set_mset B"
Mathias@63310
   596
  by (metis mset_subset_eqD subsetI)
Mathias@63310
   597
Mathias@63310
   598
lemma mset_subset_eq_insertD:
Mathias@63793
   599
  "add_mset x A \<subseteq># B \<Longrightarrow> x \<in># B \<and> A \<subset># B"
haftmann@34943
   600
apply (rule conjI)
Mathias@63310
   601
 apply (simp add: mset_subset_eqD)
haftmann@62430
   602
 apply (clarsimp simp: subset_mset_def subseteq_mset_def)
haftmann@62430
   603
 apply safe
haftmann@62430
   604
  apply (erule_tac x = a in allE)
haftmann@62430
   605
  apply (auto split: if_split_asm)
haftmann@34943
   606
done
haftmann@34943
   607
Mathias@63310
   608
lemma mset_subset_insertD:
Mathias@63793
   609
  "add_mset x A \<subset># B \<Longrightarrow> x \<in># B \<and> A \<subset># B"
Mathias@63310
   610
  by (rule mset_subset_eq_insertD) simp
Mathias@63310
   611
nipkow@63831
   612
lemma mset_subset_of_empty[simp]: "A \<subset># {#} \<longleftrightarrow> False"
Mathias@63795
   613
  by (simp only: subset_mset.not_less_zero)
Mathias@63795
   614
nipkow@63831
   615
lemma empty_subset_add_mset[simp]: "{#} <# add_mset x M"
nipkow@63831
   616
by(auto intro: subset_mset.gr_zeroI)
nipkow@63831
   617
Mathias@63795
   618
lemma empty_le: "{#} \<subseteq># A"
Mathias@63795
   619
  by (fact subset_mset.zero_le)
Mathias@63793
   620
haftmann@62430
   621
lemma insert_subset_eq_iff:
Mathias@63793
   622
  "add_mset a A \<subseteq># B \<longleftrightarrow> a \<in># B \<and> A \<subseteq># B - {#a#}"
haftmann@62430
   623
  using le_diff_conv2 [of "Suc 0" "count B a" "count A a"]
haftmann@62430
   624
  apply (auto simp add: subseteq_mset_def not_in_iff Suc_le_eq)
haftmann@62430
   625
  apply (rule ccontr)
haftmann@62430
   626
  apply (auto simp add: not_in_iff)
haftmann@62430
   627
  done
haftmann@62430
   628
haftmann@62430
   629
lemma insert_union_subset_iff:
Mathias@63793
   630
  "add_mset a A \<subset># B \<longleftrightarrow> a \<in># B \<and> A \<subset># B - {#a#}"
Mathias@63793
   631
  by (auto simp add: insert_subset_eq_iff subset_mset_def)
haftmann@62430
   632
haftmann@62430
   633
lemma subset_eq_diff_conv:
haftmann@62430
   634
  "A - C \<subseteq># B \<longleftrightarrow> A \<subseteq># B + C"
haftmann@62430
   635
  by (simp add: subseteq_mset_def le_diff_conv)
haftmann@62430
   636
nipkow@63831
   637
lemma subset_eq_empty[simp]: "M \<subseteq># {#} \<longleftrightarrow> M = {#}"
Mathias@63793
   638
  by auto
Mathias@63793
   639
Mathias@63793
   640
lemma multi_psub_of_add_self [simp]: "A \<subset># add_mset x A"
Mathias@60397
   641
  by (auto simp: subset_mset_def subseteq_mset_def)
Mathias@60397
   642
haftmann@62430
   643
lemma multi_psub_self[simp]: "(A::'a multiset) \<subset># A = False"
haftmann@35268
   644
  by simp
haftmann@34943
   645
Mathias@63793
   646
lemma mset_subset_add_mset [simp]: "add_mset x N \<subset># add_mset x M \<longleftrightarrow> N \<subset># M"
Mathias@63793
   647
  unfolding add_mset_add_single[of _ N] add_mset_add_single[of _ M]
Mathias@63793
   648
  by (fact subset_mset.add_less_cancel_right)
haftmann@35268
   649
Mathias@63310
   650
lemma mset_subset_empty_nonempty: "{#} \<subset># S \<longleftrightarrow> S \<noteq> {#}"
hoelzl@62378
   651
  by (fact subset_mset.zero_less_iff_neq_zero)
haftmann@35268
   652
Mathias@63310
   653
lemma mset_subset_diff_self: "c \<in># B \<Longrightarrow> B - {#c#} \<subset># B"
haftmann@62430
   654
  by (auto simp: subset_mset_def elim: mset_add)
haftmann@35268
   655
haftmann@35268
   656
wenzelm@60500
   657
subsubsection \<open>Intersection\<close>
haftmann@35268
   658
Mathias@60397
   659
definition inf_subset_mset :: "'a multiset \<Rightarrow> 'a multiset \<Rightarrow> 'a multiset" (infixl "#\<inter>" 70) where
Mathias@60397
   660
  multiset_inter_def: "inf_subset_mset A B = A - (A - B)"
Mathias@60397
   661
haftmann@62430
   662
interpretation subset_mset: semilattice_inf inf_subset_mset "op \<subseteq>#" "op \<subset>#"
wenzelm@46921
   663
proof -
wenzelm@60678
   664
  have [simp]: "m \<le> n \<Longrightarrow> m \<le> q \<Longrightarrow> m \<le> n - (n - q)" for m n q :: nat
wenzelm@60678
   665
    by arith
haftmann@62430
   666
  show "class.semilattice_inf op #\<inter> op \<subseteq># op \<subset>#"
wenzelm@60678
   667
    by standard (auto simp add: multiset_inter_def subseteq_mset_def)
haftmann@35268
   668
qed
wenzelm@62837
   669
  \<comment> \<open>FIXME: avoid junk stemming from type class interpretation\<close>
haftmann@34943
   670
haftmann@41069
   671
lemma multiset_inter_count [simp]:
wenzelm@60606
   672
  fixes A B :: "'a multiset"
wenzelm@60606
   673
  shows "count (A #\<inter> B) x = min (count A x) (count B x)"
bulwahn@47429
   674
  by (simp add: multiset_inter_def)
haftmann@35268
   675
haftmann@62430
   676
lemma set_mset_inter [simp]:
haftmann@62430
   677
  "set_mset (A #\<inter> B) = set_mset A \<inter> set_mset B"
haftmann@62430
   678
  by (simp only: set_eq_iff count_greater_zero_iff [symmetric] multiset_inter_count) simp
haftmann@62430
   679
haftmann@62430
   680
lemma diff_intersect_left_idem [simp]:
haftmann@62430
   681
  "M - M #\<inter> N = M - N"
haftmann@62430
   682
  by (simp add: multiset_eq_iff min_def)
haftmann@62430
   683
haftmann@62430
   684
lemma diff_intersect_right_idem [simp]:
haftmann@62430
   685
  "M - N #\<inter> M = M - N"
haftmann@62430
   686
  by (simp add: multiset_eq_iff min_def)
haftmann@62430
   687
nipkow@63831
   688
lemma multiset_inter_single[simp]: "a \<noteq> b \<Longrightarrow> {#a#} #\<inter> {#b#} = {#}"
wenzelm@46730
   689
  by (rule multiset_eqI) auto
haftmann@34943
   690
haftmann@35268
   691
lemma multiset_union_diff_commute:
haftmann@35268
   692
  assumes "B #\<inter> C = {#}"
haftmann@35268
   693
  shows "A + B - C = A - C + B"
nipkow@39302
   694
proof (rule multiset_eqI)
haftmann@35268
   695
  fix x
haftmann@35268
   696
  from assms have "min (count B x) (count C x) = 0"
wenzelm@46730
   697
    by (auto simp add: multiset_eq_iff)
haftmann@35268
   698
  then have "count B x = 0 \<or> count C x = 0"
haftmann@62430
   699
    unfolding min_def by (auto split: if_splits)
haftmann@35268
   700
  then show "count (A + B - C) x = count (A - C + B) x"
haftmann@35268
   701
    by auto
haftmann@35268
   702
qed
haftmann@35268
   703
haftmann@62430
   704
lemma disjunct_not_in:
haftmann@62430
   705
  "A #\<inter> B = {#} \<longleftrightarrow> (\<forall>a. a \<notin># A \<or> a \<notin># B)" (is "?P \<longleftrightarrow> ?Q")
haftmann@62430
   706
proof
haftmann@62430
   707
  assume ?P
haftmann@62430
   708
  show ?Q
haftmann@62430
   709
  proof
haftmann@62430
   710
    fix a
haftmann@62430
   711
    from \<open>?P\<close> have "min (count A a) (count B a) = 0"
haftmann@62430
   712
      by (simp add: multiset_eq_iff)
haftmann@62430
   713
    then have "count A a = 0 \<or> count B a = 0"
haftmann@62430
   714
      by (cases "count A a \<le> count B a") (simp_all add: min_def)
haftmann@62430
   715
    then show "a \<notin># A \<or> a \<notin># B"
haftmann@62430
   716
      by (simp add: not_in_iff)
haftmann@62430
   717
  qed
haftmann@62430
   718
next
haftmann@62430
   719
  assume ?Q
haftmann@62430
   720
  show ?P
haftmann@62430
   721
  proof (rule multiset_eqI)
haftmann@62430
   722
    fix a
haftmann@62430
   723
    from \<open>?Q\<close> have "count A a = 0 \<or> count B a = 0"
haftmann@62430
   724
      by (auto simp add: not_in_iff)
haftmann@62430
   725
    then show "count (A #\<inter> B) a = count {#} a"
haftmann@62430
   726
      by auto
haftmann@62430
   727
  qed
haftmann@62430
   728
qed
haftmann@62430
   729
nipkow@63831
   730
lemma add_mset_inter_add_mset[simp]:
Mathias@63793
   731
  "add_mset a A #\<inter> add_mset a B = add_mset a (A #\<inter> B)"
Mathias@63793
   732
  by (metis add_mset_add_single add_mset_diff_bothsides diff_subset_eq_self multiset_inter_def
Mathias@63793
   733
      subset_mset.diff_add_assoc2)
Mathias@63793
   734
Mathias@63793
   735
lemma add_mset_disjoint [simp]:
Mathias@63793
   736
  "add_mset a A #\<inter> B = {#} \<longleftrightarrow> a \<notin># B \<and> A #\<inter> B = {#}"
Mathias@63793
   737
  "{#} = add_mset a A #\<inter> B \<longleftrightarrow> a \<notin># B \<and> {#} = A #\<inter> B"
Mathias@63793
   738
  by (auto simp: disjunct_not_in)
Mathias@63793
   739
Mathias@63793
   740
lemma disjoint_add_mset [simp]:
Mathias@63793
   741
  "B #\<inter> add_mset a A = {#} \<longleftrightarrow> a \<notin># B \<and> B #\<inter> A = {#}"
Mathias@63793
   742
  "{#} = A #\<inter> add_mset b B \<longleftrightarrow> b \<notin># A \<and> {#} = A #\<inter> B"
Mathias@63793
   743
  by (auto simp: disjunct_not_in)
Mathias@63793
   744
nipkow@63831
   745
lemma empty_inter[simp]: "{#} #\<inter> M = {#}"
haftmann@51600
   746
  by (simp add: multiset_eq_iff)
haftmann@51600
   747
nipkow@63831
   748
lemma inter_empty[simp]: "M #\<inter> {#} = {#}"
haftmann@51600
   749
  by (simp add: multiset_eq_iff)
haftmann@51600
   750
Mathias@63793
   751
lemma inter_add_left1: "\<not> x \<in># N \<Longrightarrow> (add_mset x M) #\<inter> N = M #\<inter> N"
haftmann@62430
   752
  by (simp add: multiset_eq_iff not_in_iff)
haftmann@51600
   753
Mathias@63793
   754
lemma inter_add_left2: "x \<in># N \<Longrightarrow> (add_mset x M) #\<inter> N = add_mset x (M #\<inter> (N - {#x#}))"
haftmann@62430
   755
  by (auto simp add: multiset_eq_iff elim: mset_add)
haftmann@51600
   756
Mathias@63793
   757
lemma inter_add_right1: "\<not> x \<in># N \<Longrightarrow> N #\<inter> (add_mset x M) = N #\<inter> M"
haftmann@62430
   758
  by (simp add: multiset_eq_iff not_in_iff)
haftmann@51600
   759
Mathias@63793
   760
lemma inter_add_right2: "x \<in># N \<Longrightarrow> N #\<inter> (add_mset x M) = add_mset x ((N - {#x#}) #\<inter> M)"
haftmann@62430
   761
  by (auto simp add: multiset_eq_iff elim: mset_add)
haftmann@62430
   762
haftmann@62430
   763
lemma disjunct_set_mset_diff:
haftmann@62430
   764
  assumes "M #\<inter> N = {#}"
haftmann@62430
   765
  shows "set_mset (M - N) = set_mset M"
haftmann@62430
   766
proof (rule set_eqI)
haftmann@62430
   767
  fix a
haftmann@62430
   768
  from assms have "a \<notin># M \<or> a \<notin># N"
haftmann@62430
   769
    by (simp add: disjunct_not_in)
haftmann@62430
   770
  then show "a \<in># M - N \<longleftrightarrow> a \<in># M"
haftmann@62430
   771
    by (auto dest: in_diffD) (simp add: in_diff_count not_in_iff)
haftmann@62430
   772
qed
haftmann@62430
   773
haftmann@62430
   774
lemma at_most_one_mset_mset_diff:
haftmann@62430
   775
  assumes "a \<notin># M - {#a#}"
haftmann@62430
   776
  shows "set_mset (M - {#a#}) = set_mset M - {a}"
haftmann@62430
   777
  using assms by (auto simp add: not_in_iff in_diff_count set_eq_iff)
haftmann@62430
   778
haftmann@62430
   779
lemma more_than_one_mset_mset_diff:
haftmann@62430
   780
  assumes "a \<in># M - {#a#}"
haftmann@62430
   781
  shows "set_mset (M - {#a#}) = set_mset M"
haftmann@62430
   782
proof (rule set_eqI)
haftmann@62430
   783
  fix b
haftmann@62430
   784
  have "Suc 0 < count M b \<Longrightarrow> count M b > 0" by arith
haftmann@62430
   785
  then show "b \<in># M - {#a#} \<longleftrightarrow> b \<in># M"
haftmann@62430
   786
    using assms by (auto simp add: in_diff_count)
haftmann@62430
   787
qed
haftmann@62430
   788
haftmann@62430
   789
lemma inter_iff:
haftmann@62430
   790
  "a \<in># A #\<inter> B \<longleftrightarrow> a \<in># A \<and> a \<in># B"
haftmann@62430
   791
  by simp
haftmann@62430
   792
haftmann@62430
   793
lemma inter_union_distrib_left:
haftmann@62430
   794
  "A #\<inter> B + C = (A + C) #\<inter> (B + C)"
haftmann@62430
   795
  by (simp add: multiset_eq_iff min_add_distrib_left)
haftmann@62430
   796
haftmann@62430
   797
lemma inter_union_distrib_right:
haftmann@62430
   798
  "C + A #\<inter> B = (C + A) #\<inter> (C + B)"
haftmann@62430
   799
  using inter_union_distrib_left [of A B C] by (simp add: ac_simps)
haftmann@62430
   800
haftmann@62430
   801
lemma inter_subset_eq_union:
haftmann@62430
   802
  "A #\<inter> B \<subseteq># A + B"
haftmann@62430
   803
  by (auto simp add: subseteq_mset_def)
haftmann@51600
   804
haftmann@35268
   805
wenzelm@60500
   806
subsubsection \<open>Bounded union\<close>
wenzelm@60678
   807
wenzelm@60678
   808
definition sup_subset_mset :: "'a multiset \<Rightarrow> 'a multiset \<Rightarrow> 'a multiset"(infixl "#\<union>" 70)
wenzelm@62837
   809
  where "sup_subset_mset A B = A + (B - A)" \<comment> \<open>FIXME irregular fact name\<close>
haftmann@62430
   810
haftmann@62430
   811
interpretation subset_mset: semilattice_sup sup_subset_mset "op \<subseteq>#" "op \<subset>#"
haftmann@51623
   812
proof -
wenzelm@60678
   813
  have [simp]: "m \<le> n \<Longrightarrow> q \<le> n \<Longrightarrow> m + (q - m) \<le> n" for m n q :: nat
wenzelm@60678
   814
    by arith
haftmann@62430
   815
  show "class.semilattice_sup op #\<union> op \<subseteq># op \<subset>#"
wenzelm@60678
   816
    by standard (auto simp add: sup_subset_mset_def subseteq_mset_def)
haftmann@51623
   817
qed
wenzelm@62837
   818
  \<comment> \<open>FIXME: avoid junk stemming from type class interpretation\<close>
wenzelm@62837
   819
Mathias@63795
   820
interpretation subset_mset: bounded_lattice_bot "op #\<inter>" "op \<subseteq>#" "op \<subset>#"
Mathias@63795
   821
  "op #\<union>" "{#}"
Mathias@63795
   822
  by standard auto
Mathias@63795
   823
wenzelm@62837
   824
lemma sup_subset_mset_count [simp]: \<comment> \<open>FIXME irregular fact name\<close>
haftmann@62430
   825
  "count (A #\<union> B) x = max (count A x) (count B x)"
Mathias@60397
   826
  by (simp add: sup_subset_mset_def)
haftmann@51623
   827
haftmann@62430
   828
lemma set_mset_sup [simp]:
haftmann@62430
   829
  "set_mset (A #\<union> B) = set_mset A \<union> set_mset B"
haftmann@62430
   830
  by (simp only: set_eq_iff count_greater_zero_iff [symmetric] sup_subset_mset_count)
haftmann@62430
   831
    (auto simp add: not_in_iff elim: mset_add)
haftmann@62430
   832
Mathias@63795
   833
lemma empty_sup: "{#} #\<union> M = M"
Mathias@63795
   834
  by (fact subset_mset.sup_bot.left_neutral)
Mathias@63795
   835
Mathias@63795
   836
lemma sup_empty: "M #\<union> {#} = M"
Mathias@63795
   837
  by (fact subset_mset.sup_bot.right_neutral)
haftmann@51623
   838
Mathias@63793
   839
lemma sup_union_left1 [simp]: "\<not> x \<in># N \<Longrightarrow> (add_mset x M) #\<union> N = add_mset x (M #\<union> N)"
haftmann@62430
   840
  by (simp add: multiset_eq_iff not_in_iff)
haftmann@62430
   841
Mathias@63793
   842
lemma sup_union_left2: "x \<in># N \<Longrightarrow> (add_mset x M) #\<union> N = add_mset x (M #\<union> (N - {#x#}))"
haftmann@51623
   843
  by (simp add: multiset_eq_iff)
haftmann@51623
   844
Mathias@63793
   845
lemma sup_union_right1 [simp]: "\<not> x \<in># N \<Longrightarrow> N #\<union> (add_mset x M) = add_mset x (N #\<union> M)"
haftmann@62430
   846
  by (simp add: multiset_eq_iff not_in_iff)
haftmann@62430
   847
Mathias@63793
   848
lemma sup_union_right2: "x \<in># N \<Longrightarrow> N #\<union> (add_mset x M) = add_mset x ((N - {#x#}) #\<union> M)"
haftmann@51623
   849
  by (simp add: multiset_eq_iff)
haftmann@51623
   850
haftmann@62430
   851
lemma sup_union_distrib_left:
haftmann@62430
   852
  "A #\<union> B + C = (A + C) #\<union> (B + C)"
haftmann@62430
   853
  by (simp add: multiset_eq_iff max_add_distrib_left)
haftmann@62430
   854
haftmann@62430
   855
lemma union_sup_distrib_right:
haftmann@62430
   856
  "C + A #\<union> B = (C + A) #\<union> (C + B)"
haftmann@62430
   857
  using sup_union_distrib_left [of A B C] by (simp add: ac_simps)
haftmann@62430
   858
haftmann@62430
   859
lemma union_diff_inter_eq_sup:
haftmann@62430
   860
  "A + B - A #\<inter> B = A #\<union> B"
haftmann@62430
   861
  by (auto simp add: multiset_eq_iff)
haftmann@62430
   862
haftmann@62430
   863
lemma union_diff_sup_eq_inter:
haftmann@62430
   864
  "A + B - A #\<union> B = A #\<inter> B"
haftmann@62430
   865
  by (auto simp add: multiset_eq_iff)
haftmann@62430
   866
Mathias@63793
   867
lemma add_mset_union:
Mathias@63793
   868
  \<open>add_mset a A #\<union> add_mset a B = add_mset a (A #\<union> B)\<close>
Mathias@63793
   869
  by (auto simp: multiset_eq_iff max_def)
Mathias@63793
   870
haftmann@51623
   871
wenzelm@60500
   872
subsubsection \<open>Subset is an order\<close>
haftmann@62430
   873
Mathias@60397
   874
interpretation subset_mset: order "op \<le>#" "op <#" by unfold_locales auto
haftmann@51623
   875
blanchet@63409
   876
Mathias@63793
   877
subsubsection \<open>Simprocs\<close>
Mathias@63793
   878
Mathias@63793
   879
fun repeat_mset :: "nat \<Rightarrow> 'a multiset \<Rightarrow> 'a multiset" where
Mathias@63793
   880
  "repeat_mset 0 _ = {#}" |
Mathias@63793
   881
  "repeat_mset (Suc n) A = A + repeat_mset n A"
Mathias@63793
   882
Mathias@63793
   883
lemma count_repeat_mset [simp]: "count (repeat_mset i A) a = i * count A a"
Mathias@63793
   884
  by (induction i) auto
Mathias@63793
   885
Mathias@63793
   886
lemma repeat_mset_right [simp]: "repeat_mset a (repeat_mset b A) = repeat_mset (a * b) A"
Mathias@63793
   887
  by (auto simp: multiset_eq_iff left_diff_distrib')
Mathias@63793
   888
Mathias@63793
   889
lemma left_diff_repeat_mset_distrib': \<open>repeat_mset (i - j) u = repeat_mset i u - repeat_mset j u\<close>
Mathias@63793
   890
  by (auto simp: multiset_eq_iff left_diff_distrib')
Mathias@63793
   891
Mathias@63793
   892
lemma mset_diff_add_eq1:
Mathias@63793
   893
  "j \<le> (i::nat) \<Longrightarrow> ((repeat_mset i u + m) - (repeat_mset j u + n)) = ((repeat_mset (i-j) u + m) - n)"
Mathias@63793
   894
  by (auto simp: multiset_eq_iff nat_diff_add_eq1)
Mathias@63793
   895
Mathias@63793
   896
lemma mset_diff_add_eq2:
Mathias@63793
   897
  "i \<le> (j::nat) \<Longrightarrow> ((repeat_mset i u + m) - (repeat_mset j u + n)) = (m - (repeat_mset (j-i) u + n))"
Mathias@63793
   898
  by (auto simp: multiset_eq_iff nat_diff_add_eq2)
Mathias@63793
   899
Mathias@63793
   900
lemma mset_eq_add_iff1:
Mathias@63793
   901
   "j \<le> (i::nat) \<Longrightarrow> (repeat_mset i u + m = repeat_mset j u + n) = (repeat_mset (i-j) u + m = n)"
Mathias@63793
   902
  by (auto simp: multiset_eq_iff nat_eq_add_iff1)
Mathias@63793
   903
Mathias@63793
   904
lemma mset_eq_add_iff2:
Mathias@63793
   905
   "i \<le> (j::nat) \<Longrightarrow> (repeat_mset i u + m = repeat_mset j u + n) = (m = repeat_mset (j-i) u + n)"
Mathias@63793
   906
  by (auto simp: multiset_eq_iff nat_eq_add_iff2)
Mathias@63793
   907
Mathias@63793
   908
lemma mset_subseteq_add_iff1:
Mathias@63793
   909
  "j \<le> (i::nat) \<Longrightarrow> (repeat_mset i u + m \<subseteq># repeat_mset j u + n) = (repeat_mset (i-j) u + m \<subseteq># n)"
Mathias@63793
   910
  by (auto simp add: subseteq_mset_def nat_le_add_iff1)
Mathias@63793
   911
Mathias@63793
   912
lemma mset_subseteq_add_iff2:
Mathias@63793
   913
  "i \<le> (j::nat) \<Longrightarrow> (repeat_mset i u + m \<subseteq># repeat_mset j u + n) = (m \<subseteq># repeat_mset (j-i) u + n)"
Mathias@63793
   914
  by (auto simp add: subseteq_mset_def nat_le_add_iff2)
Mathias@63793
   915
Mathias@63793
   916
lemma mset_subset_add_iff1:
Mathias@63793
   917
  "j \<le> (i::nat) \<Longrightarrow> (repeat_mset i u + m \<subset># repeat_mset j u + n) = (repeat_mset (i-j) u + m \<subset># n)"
Mathias@63793
   918
  unfolding subset_mset_def by (simp add: mset_eq_add_iff1 mset_subseteq_add_iff1)
Mathias@63793
   919
Mathias@63793
   920
lemma mset_subset_add_iff2:
Mathias@63793
   921
  "i \<le> (j::nat) \<Longrightarrow> (repeat_mset i u + m \<subset># repeat_mset j u + n) = (m \<subset># repeat_mset (j-i) u + n)"
Mathias@63793
   922
  unfolding subset_mset_def by (simp add: mset_eq_add_iff2 mset_subseteq_add_iff2)
Mathias@63793
   923
Mathias@63793
   924
lemma left_add_mult_distrib_mset:
Mathias@63793
   925
  "repeat_mset i u + (repeat_mset j u + k) = repeat_mset (i+j) u + k"
Mathias@63793
   926
  by (auto simp: multiset_eq_iff add_mult_distrib)
Mathias@63793
   927
Mathias@63793
   928
lemma repeat_mset_cancel1: "repeat_mset a A = repeat_mset a B \<longleftrightarrow> A = B \<or> a = 0"
Mathias@63793
   929
  by (auto simp: multiset_eq_iff)
Mathias@63793
   930
Mathias@63793
   931
lemma repeat_mset_cancel2: "repeat_mset a A = repeat_mset b A \<longleftrightarrow> a = b \<or> A = {#}"
Mathias@63793
   932
  by (auto simp: multiset_eq_iff)
Mathias@63793
   933
Mathias@63793
   934
lemma repeat_mset_distrib [simp]:
Mathias@63793
   935
  "repeat_mset n (A + B) = repeat_mset n A + repeat_mset n B"
Mathias@63793
   936
  by (auto simp: multiset_eq_iff add_mult_distrib2)
Mathias@63793
   937
Mathias@63793
   938
lemma repeat_mset_distrib_add_mset [simp]:
Mathias@63793
   939
  "repeat_mset n (add_mset a A) = repeat_mset n {#a#} + repeat_mset n A"
Mathias@63793
   940
  by (auto simp: multiset_eq_iff)
Mathias@63793
   941
Mathias@63793
   942
ML_file "multiset_simprocs_util.ML"
Mathias@63793
   943
ML_file "multiset_simprocs.ML"
Mathias@63793
   944
Mathias@63793
   945
simproc_setup mseteq_cancel_numerals
Mathias@63793
   946
  ("(l::'a multiset) + m = n" | "(l::'a multiset) = m + n" |
Mathias@63793
   947
   "add_mset a m = n" | "m = add_mset a n") =
Mathias@63793
   948
  \<open>fn phi => Multiset_Simprocs.eq_cancel_msets\<close>
Mathias@63793
   949
Mathias@63793
   950
simproc_setup msetless_cancel_numerals
Mathias@63793
   951
  ("(l::'a multiset) + m \<subset># n" | "(l::'a multiset) \<subset># m + n" |
Mathias@63793
   952
   "add_mset a m \<subset># n" | "m \<subset># add_mset a n") =
Mathias@63793
   953
  \<open>fn phi => Multiset_Simprocs.subset_cancel_msets\<close>
Mathias@63793
   954
Mathias@63793
   955
simproc_setup msetle_cancel_numerals
Mathias@63793
   956
  ("(l::'a multiset) + m \<subseteq># n" | "(l::'a multiset) \<subseteq># m + n" |
Mathias@63793
   957
   "add_mset a m \<subseteq># n" | "m \<subseteq># add_mset a n") =
Mathias@63793
   958
  \<open>fn phi => Multiset_Simprocs.subseteq_cancel_msets\<close>
Mathias@63793
   959
Mathias@63793
   960
simproc_setup msetdiff_cancel_numerals
Mathias@63793
   961
  ("((l::'a multiset) + m) - n" | "(l::'a multiset) - (m + n)" |
Mathias@63793
   962
   "add_mset a m - n" | "m - add_mset a n") =
Mathias@63793
   963
  \<open>fn phi => Multiset_Simprocs.diff_cancel_msets\<close>
Mathias@63793
   964
Mathias@63793
   965
eberlm@63358
   966
subsubsection \<open>Conditionally complete lattice\<close>
eberlm@63358
   967
eberlm@63358
   968
instantiation multiset :: (type) Inf
eberlm@63358
   969
begin
eberlm@63358
   970
eberlm@63358
   971
lift_definition Inf_multiset :: "'a multiset set \<Rightarrow> 'a multiset" is
eberlm@63358
   972
  "\<lambda>A i. if A = {} then 0 else Inf ((\<lambda>f. f i) ` A)"
eberlm@63358
   973
proof -
eberlm@63358
   974
  fix A :: "('a \<Rightarrow> nat) set" assume *: "\<And>x. x \<in> A \<Longrightarrow> x \<in> multiset"
eberlm@63358
   975
  have "finite {i. (if A = {} then 0 else Inf ((\<lambda>f. f i) ` A)) > 0}" unfolding multiset_def
eberlm@63358
   976
  proof (cases "A = {}")
eberlm@63358
   977
    case False
eberlm@63358
   978
    then obtain f where "f \<in> A" by blast
eberlm@63358
   979
    hence "{i. Inf ((\<lambda>f. f i) ` A) > 0} \<subseteq> {i. f i > 0}"
eberlm@63358
   980
      by (auto intro: less_le_trans[OF _ cInf_lower])
eberlm@63358
   981
    moreover from \<open>f \<in> A\<close> * have "finite \<dots>" by (simp add: multiset_def)
eberlm@63358
   982
    ultimately have "finite {i. Inf ((\<lambda>f. f i) ` A) > 0}" by (rule finite_subset)
eberlm@63358
   983
    with False show ?thesis by simp
eberlm@63358
   984
  qed simp_all
eberlm@63358
   985
  thus "(\<lambda>i. if A = {} then 0 else INF f:A. f i) \<in> multiset" by (simp add: multiset_def)
eberlm@63358
   986
qed
eberlm@63358
   987
eberlm@63358
   988
instance ..
eberlm@63358
   989
eberlm@63358
   990
end
eberlm@63358
   991
eberlm@63358
   992
lemma Inf_multiset_empty: "Inf {} = {#}"
eberlm@63358
   993
  by transfer simp_all
eberlm@63358
   994
eberlm@63358
   995
lemma count_Inf_multiset_nonempty: "A \<noteq> {} \<Longrightarrow> count (Inf A) x = Inf ((\<lambda>X. count X x) ` A)"
eberlm@63358
   996
  by transfer simp_all
eberlm@63358
   997
eberlm@63358
   998
eberlm@63358
   999
instantiation multiset :: (type) Sup
eberlm@63358
  1000
begin
eberlm@63358
  1001
eberlm@63360
  1002
definition Sup_multiset :: "'a multiset set \<Rightarrow> 'a multiset" where
eberlm@63360
  1003
  "Sup_multiset A = (if A \<noteq> {} \<and> subset_mset.bdd_above A then
eberlm@63360
  1004
           Abs_multiset (\<lambda>i. Sup ((\<lambda>X. count X i) ` A)) else {#})"
eberlm@63360
  1005
eberlm@63360
  1006
lemma Sup_multiset_empty: "Sup {} = {#}"
eberlm@63360
  1007
  by (simp add: Sup_multiset_def)
eberlm@63360
  1008
eberlm@63360
  1009
lemma Sup_multiset_unbounded: "\<not>subset_mset.bdd_above A \<Longrightarrow> Sup A = {#}"
eberlm@63360
  1010
  by (simp add: Sup_multiset_def)
eberlm@63358
  1011
eberlm@63358
  1012
instance ..
eberlm@63358
  1013
eberlm@63358
  1014
end
eberlm@63358
  1015
eberlm@63358
  1016
lemma bdd_below_multiset [simp]: "subset_mset.bdd_below A"
eberlm@63358
  1017
  by (intro subset_mset.bdd_belowI[of _ "{#}"]) simp_all
eberlm@63358
  1018
eberlm@63358
  1019
lemma bdd_above_multiset_imp_bdd_above_count:
eberlm@63358
  1020
  assumes "subset_mset.bdd_above (A :: 'a multiset set)"
eberlm@63358
  1021
  shows   "bdd_above ((\<lambda>X. count X x) ` A)"
eberlm@63358
  1022
proof -
eberlm@63358
  1023
  from assms obtain Y where Y: "\<forall>X\<in>A. X \<subseteq># Y"
eberlm@63358
  1024
    by (auto simp: subset_mset.bdd_above_def)
eberlm@63358
  1025
  hence "count X x \<le> count Y x" if "X \<in> A" for X
eberlm@63358
  1026
    using that by (auto intro: mset_subset_eq_count)
eberlm@63358
  1027
  thus ?thesis by (intro bdd_aboveI[of _ "count Y x"]) auto
eberlm@63358
  1028
qed
eberlm@63358
  1029
eberlm@63358
  1030
lemma bdd_above_multiset_imp_finite_support:
eberlm@63358
  1031
  assumes "A \<noteq> {}" "subset_mset.bdd_above (A :: 'a multiset set)"
eberlm@63358
  1032
  shows   "finite (\<Union>X\<in>A. {x. count X x > 0})"
eberlm@63358
  1033
proof -
eberlm@63358
  1034
  from assms obtain Y where Y: "\<forall>X\<in>A. X \<subseteq># Y"
eberlm@63358
  1035
    by (auto simp: subset_mset.bdd_above_def)
eberlm@63358
  1036
  hence "count X x \<le> count Y x" if "X \<in> A" for X x
eberlm@63358
  1037
    using that by (auto intro: mset_subset_eq_count)
eberlm@63358
  1038
  hence "(\<Union>X\<in>A. {x. count X x > 0}) \<subseteq> {x. count Y x > 0}"
eberlm@63358
  1039
    by safe (erule less_le_trans)
eberlm@63358
  1040
  moreover have "finite \<dots>" by simp
eberlm@63358
  1041
  ultimately show ?thesis by (rule finite_subset)
eberlm@63358
  1042
qed
eberlm@63358
  1043
eberlm@63360
  1044
lemma Sup_multiset_in_multiset:
eberlm@63360
  1045
  assumes "A \<noteq> {}" "subset_mset.bdd_above A"
eberlm@63360
  1046
  shows   "(\<lambda>i. SUP X:A. count X i) \<in> multiset"
eberlm@63360
  1047
  unfolding multiset_def
eberlm@63360
  1048
proof
eberlm@63360
  1049
  have "{i. Sup ((\<lambda>X. count X i) ` A) > 0} \<subseteq> (\<Union>X\<in>A. {i. 0 < count X i})"
eberlm@63360
  1050
  proof safe
eberlm@63360
  1051
    fix i assume pos: "(SUP X:A. count X i) > 0"
eberlm@63360
  1052
    show "i \<in> (\<Union>X\<in>A. {i. 0 < count X i})"
eberlm@63360
  1053
    proof (rule ccontr)
eberlm@63360
  1054
      assume "i \<notin> (\<Union>X\<in>A. {i. 0 < count X i})"
eberlm@63360
  1055
      hence "\<forall>X\<in>A. count X i \<le> 0" by (auto simp: count_eq_zero_iff)
eberlm@63360
  1056
      with assms have "(SUP X:A. count X i) \<le> 0"
eberlm@63360
  1057
        by (intro cSup_least bdd_above_multiset_imp_bdd_above_count) auto
eberlm@63360
  1058
      with pos show False by simp
eberlm@63360
  1059
    qed
eberlm@63360
  1060
  qed
eberlm@63360
  1061
  moreover from assms have "finite \<dots>" by (rule bdd_above_multiset_imp_finite_support)
eberlm@63360
  1062
  ultimately show "finite {i. Sup ((\<lambda>X. count X i) ` A) > 0}" by (rule finite_subset)
eberlm@63360
  1063
qed
eberlm@63360
  1064
eberlm@63358
  1065
lemma count_Sup_multiset_nonempty:
eberlm@63358
  1066
  assumes "A \<noteq> {}" "subset_mset.bdd_above A"
eberlm@63358
  1067
  shows   "count (Sup A) x = (SUP X:A. count X x)"
eberlm@63360
  1068
  using assms by (simp add: Sup_multiset_def Abs_multiset_inverse Sup_multiset_in_multiset)
eberlm@63358
  1069
eberlm@63358
  1070
eberlm@63358
  1071
interpretation subset_mset: conditionally_complete_lattice Inf Sup "op #\<inter>" "op \<subseteq>#" "op \<subset>#" "op #\<union>"
eberlm@63358
  1072
proof
eberlm@63358
  1073
  fix X :: "'a multiset" and A
eberlm@63358
  1074
  assume "X \<in> A"
eberlm@63358
  1075
  show "Inf A \<subseteq># X"
eberlm@63358
  1076
  proof (rule mset_subset_eqI)
eberlm@63358
  1077
    fix x
eberlm@63358
  1078
    from \<open>X \<in> A\<close> have "A \<noteq> {}" by auto
eberlm@63358
  1079
    hence "count (Inf A) x = (INF X:A. count X x)"
eberlm@63358
  1080
      by (simp add: count_Inf_multiset_nonempty)
eberlm@63358
  1081
    also from \<open>X \<in> A\<close> have "\<dots> \<le> count X x"
eberlm@63358
  1082
      by (intro cInf_lower) simp_all
eberlm@63358
  1083
    finally show "count (Inf A) x \<le> count X x" .
eberlm@63358
  1084
  qed
eberlm@63358
  1085
next
eberlm@63358
  1086
  fix X :: "'a multiset" and A
eberlm@63358
  1087
  assume nonempty: "A \<noteq> {}" and le: "\<And>Y. Y \<in> A \<Longrightarrow> X \<subseteq># Y"
eberlm@63358
  1088
  show "X \<subseteq># Inf A"
eberlm@63358
  1089
  proof (rule mset_subset_eqI)
eberlm@63358
  1090
    fix x
eberlm@63358
  1091
    from nonempty have "count X x \<le> (INF X:A. count X x)"
eberlm@63358
  1092
      by (intro cInf_greatest) (auto intro: mset_subset_eq_count le)
eberlm@63358
  1093
    also from nonempty have "\<dots> = count (Inf A) x" by (simp add: count_Inf_multiset_nonempty)
eberlm@63358
  1094
    finally show "count X x \<le> count (Inf A) x" .
eberlm@63358
  1095
  qed
eberlm@63358
  1096
next
eberlm@63358
  1097
  fix X :: "'a multiset" and A
eberlm@63358
  1098
  assume X: "X \<in> A" and bdd: "subset_mset.bdd_above A"
eberlm@63358
  1099
  show "X \<subseteq># Sup A"
eberlm@63358
  1100
  proof (rule mset_subset_eqI)
eberlm@63358
  1101
    fix x
eberlm@63358
  1102
    from X have "A \<noteq> {}" by auto
eberlm@63358
  1103
    have "count X x \<le> (SUP X:A. count X x)"
eberlm@63358
  1104
      by (intro cSUP_upper X bdd_above_multiset_imp_bdd_above_count bdd)
eberlm@63358
  1105
    also from count_Sup_multiset_nonempty[OF \<open>A \<noteq> {}\<close> bdd]
eberlm@63358
  1106
      have "(SUP X:A. count X x) = count (Sup A) x" by simp
eberlm@63358
  1107
    finally show "count X x \<le> count (Sup A) x" .
eberlm@63358
  1108
  qed
eberlm@63358
  1109
next
eberlm@63358
  1110
  fix X :: "'a multiset" and A
eberlm@63358
  1111
  assume nonempty: "A \<noteq> {}" and ge: "\<And>Y. Y \<in> A \<Longrightarrow> Y \<subseteq># X"
eberlm@63358
  1112
  from ge have bdd: "subset_mset.bdd_above A" by (rule subset_mset.bdd_aboveI[of _ X])
eberlm@63358
  1113
  show "Sup A \<subseteq># X"
eberlm@63358
  1114
  proof (rule mset_subset_eqI)
eberlm@63358
  1115
    fix x
eberlm@63358
  1116
    from count_Sup_multiset_nonempty[OF \<open>A \<noteq> {}\<close> bdd]
eberlm@63358
  1117
      have "count (Sup A) x = (SUP X:A. count X x)" .
eberlm@63358
  1118
    also from nonempty have "\<dots> \<le> count X x"
eberlm@63358
  1119
      by (intro cSup_least) (auto intro: mset_subset_eq_count ge)
eberlm@63358
  1120
    finally show "count (Sup A) x \<le> count X x" .
eberlm@63358
  1121
  qed
eberlm@63358
  1122
qed
eberlm@63358
  1123
eberlm@63358
  1124
lemma set_mset_Inf:
eberlm@63358
  1125
  assumes "A \<noteq> {}"
eberlm@63358
  1126
  shows   "set_mset (Inf A) = (\<Inter>X\<in>A. set_mset X)"
eberlm@63358
  1127
proof safe
eberlm@63358
  1128
  fix x X assume "x \<in># Inf A" "X \<in> A"
eberlm@63358
  1129
  hence nonempty: "A \<noteq> {}" by (auto simp: Inf_multiset_empty)
eberlm@63358
  1130
  from \<open>x \<in># Inf A\<close> have "{#x#} \<subseteq># Inf A" by auto
eberlm@63358
  1131
  also from \<open>X \<in> A\<close> have "\<dots> \<subseteq># X" by (rule subset_mset.cInf_lower) simp_all
eberlm@63358
  1132
  finally show "x \<in># X" by simp
eberlm@63358
  1133
next
eberlm@63358
  1134
  fix x assume x: "x \<in> (\<Inter>X\<in>A. set_mset X)"
eberlm@63358
  1135
  hence "{#x#} \<subseteq># X" if "X \<in> A" for X using that by auto
eberlm@63358
  1136
  from assms and this have "{#x#} \<subseteq># Inf A" by (rule subset_mset.cInf_greatest)
eberlm@63358
  1137
  thus "x \<in># Inf A" by simp
eberlm@63358
  1138
qed
eberlm@63358
  1139
eberlm@63358
  1140
lemma in_Inf_multiset_iff:
eberlm@63358
  1141
  assumes "A \<noteq> {}"
eberlm@63358
  1142
  shows   "x \<in># Inf A \<longleftrightarrow> (\<forall>X\<in>A. x \<in># X)"
eberlm@63358
  1143
proof -
eberlm@63358
  1144
  from assms have "set_mset (Inf A) = (\<Inter>X\<in>A. set_mset X)" by (rule set_mset_Inf)
eberlm@63358
  1145
  also have "x \<in> \<dots> \<longleftrightarrow> (\<forall>X\<in>A. x \<in># X)" by simp
eberlm@63358
  1146
  finally show ?thesis .
eberlm@63358
  1147
qed
eberlm@63358
  1148
eberlm@63360
  1149
lemma in_Inf_multisetD: "x \<in># Inf A \<Longrightarrow> X \<in> A \<Longrightarrow> x \<in># X"
eberlm@63360
  1150
  by (subst (asm) in_Inf_multiset_iff) auto
eberlm@63360
  1151
eberlm@63358
  1152
lemma set_mset_Sup:
eberlm@63358
  1153
  assumes "subset_mset.bdd_above A"
eberlm@63358
  1154
  shows   "set_mset (Sup A) = (\<Union>X\<in>A. set_mset X)"
eberlm@63358
  1155
proof safe
eberlm@63358
  1156
  fix x assume "x \<in># Sup A"
eberlm@63358
  1157
  hence nonempty: "A \<noteq> {}" by (auto simp: Sup_multiset_empty)
eberlm@63358
  1158
  show "x \<in> (\<Union>X\<in>A. set_mset X)"
eberlm@63358
  1159
  proof (rule ccontr)
eberlm@63358
  1160
    assume x: "x \<notin> (\<Union>X\<in>A. set_mset X)"
eberlm@63358
  1161
    have "count X x \<le> count (Sup A) x" if "X \<in> A" for X x
eberlm@63358
  1162
      using that by (intro mset_subset_eq_count subset_mset.cSup_upper assms)
eberlm@63358
  1163
    with x have "X \<subseteq># Sup A - {#x#}" if "X \<in> A" for X
eberlm@63358
  1164
      using that by (auto simp: subseteq_mset_def algebra_simps not_in_iff)
eberlm@63358
  1165
    hence "Sup A \<subseteq># Sup A - {#x#}" by (intro subset_mset.cSup_least nonempty)
eberlm@63358
  1166
    with \<open>x \<in># Sup A\<close> show False
eberlm@63358
  1167
      by (auto simp: subseteq_mset_def count_greater_zero_iff [symmetric]
eberlm@63358
  1168
               simp del: count_greater_zero_iff dest!: spec[of _ x])
eberlm@63358
  1169
  qed
eberlm@63358
  1170
next
eberlm@63358
  1171
  fix x X assume "x \<in> set_mset X" "X \<in> A"
eberlm@63358
  1172
  hence "{#x#} \<subseteq># X" by auto
eberlm@63358
  1173
  also have "X \<subseteq># Sup A" by (intro subset_mset.cSup_upper \<open>X \<in> A\<close> assms)
eberlm@63358
  1174
  finally show "x \<in> set_mset (Sup A)" by simp
eberlm@63358
  1175
qed
eberlm@63358
  1176
eberlm@63358
  1177
lemma in_Sup_multiset_iff:
eberlm@63358
  1178
  assumes "subset_mset.bdd_above A"
eberlm@63358
  1179
  shows   "x \<in># Sup A \<longleftrightarrow> (\<exists>X\<in>A. x \<in># X)"
eberlm@63358
  1180
proof -
eberlm@63358
  1181
  from assms have "set_mset (Sup A) = (\<Union>X\<in>A. set_mset X)" by (rule set_mset_Sup)
eberlm@63358
  1182
  also have "x \<in> \<dots> \<longleftrightarrow> (\<exists>X\<in>A. x \<in># X)" by simp
eberlm@63358
  1183
  finally show ?thesis .
eberlm@63358
  1184
qed
eberlm@63358
  1185
Mathias@63793
  1186
lemma in_Sup_multisetD:
eberlm@63360
  1187
  assumes "x \<in># Sup A"
eberlm@63360
  1188
  shows   "\<exists>X\<in>A. x \<in># X"
eberlm@63360
  1189
proof -
eberlm@63360
  1190
  have "subset_mset.bdd_above A"
eberlm@63360
  1191
    by (rule ccontr) (insert assms, simp_all add: Sup_multiset_unbounded)
eberlm@63360
  1192
  with assms show ?thesis by (simp add: in_Sup_multiset_iff)
eberlm@63534
  1193
qed
eberlm@63534
  1194
eberlm@63534
  1195
interpretation subset_mset: distrib_lattice "op #\<inter>" "op \<subseteq>#" "op \<subset>#" "op #\<union>"
eberlm@63534
  1196
proof
eberlm@63534
  1197
  fix A B C :: "'a multiset"
eberlm@63534
  1198
  show "A #\<union> (B #\<inter> C) = A #\<union> B #\<inter> (A #\<union> C)"
eberlm@63534
  1199
    by (intro multiset_eqI) simp_all
eberlm@63534
  1200
qed
eberlm@63360
  1201
haftmann@62430
  1202
wenzelm@60500
  1203
subsubsection \<open>Filter (with comprehension syntax)\<close>
wenzelm@60500
  1204
wenzelm@60500
  1205
text \<open>Multiset comprehension\<close>
haftmann@41069
  1206
nipkow@59998
  1207
lift_definition filter_mset :: "('a \<Rightarrow> bool) \<Rightarrow> 'a multiset \<Rightarrow> 'a multiset"
nipkow@59998
  1208
is "\<lambda>P M. \<lambda>x. if P x then M x else 0"
bulwahn@47429
  1209
by (rule filter_preserves_multiset)
haftmann@35268
  1210
haftmann@62430
  1211
syntax (ASCII)
blanchet@63689
  1212
  "_MCollect" :: "pttrn \<Rightarrow> 'a multiset \<Rightarrow> bool \<Rightarrow> 'a multiset"    ("(1{#_ :# _./ _#})")
haftmann@62430
  1213
syntax
blanchet@63689
  1214
  "_MCollect" :: "pttrn \<Rightarrow> 'a multiset \<Rightarrow> bool \<Rightarrow> 'a multiset"    ("(1{#_ \<in># _./ _#})")
haftmann@62430
  1215
translations
haftmann@62430
  1216
  "{#x \<in># M. P#}" == "CONST filter_mset (\<lambda>x. P) M"
haftmann@62430
  1217
haftmann@62430
  1218
lemma count_filter_mset [simp]:
haftmann@62430
  1219
  "count (filter_mset P M) a = (if P a then count M a else 0)"
nipkow@59998
  1220
  by (simp add: filter_mset.rep_eq)
nipkow@59998
  1221
haftmann@62430
  1222
lemma set_mset_filter [simp]:
haftmann@62430
  1223
  "set_mset (filter_mset P M) = {a \<in> set_mset M. P a}"
haftmann@62430
  1224
  by (simp only: set_eq_iff count_greater_zero_iff [symmetric] count_filter_mset) simp
haftmann@62430
  1225
wenzelm@60606
  1226
lemma filter_empty_mset [simp]: "filter_mset P {#} = {#}"
nipkow@59998
  1227
  by (rule multiset_eqI) simp
nipkow@59998
  1228
Mathias@63793
  1229
lemma filter_single_mset: "filter_mset P {#x#} = (if P x then {#x#} else {#})"
nipkow@39302
  1230
  by (rule multiset_eqI) simp
haftmann@35268
  1231
wenzelm@60606
  1232
lemma filter_union_mset [simp]: "filter_mset P (M + N) = filter_mset P M + filter_mset P N"
haftmann@41069
  1233
  by (rule multiset_eqI) simp
haftmann@41069
  1234
wenzelm@60606
  1235
lemma filter_diff_mset [simp]: "filter_mset P (M - N) = filter_mset P M - filter_mset P N"
nipkow@39302
  1236
  by (rule multiset_eqI) simp
haftmann@35268
  1237
wenzelm@60606
  1238
lemma filter_inter_mset [simp]: "filter_mset P (M #\<inter> N) = filter_mset P M #\<inter> filter_mset P N"
haftmann@41069
  1239
  by (rule multiset_eqI) simp
haftmann@41069
  1240
Mathias@63795
  1241
lemma filter_sup_mset[simp]: "filter_mset P (A #\<union> B) = filter_mset P A #\<union> filter_mset P B"
Mathias@63795
  1242
  by (rule multiset_eqI) simp
Mathias@63795
  1243
Mathias@63793
  1244
lemma filter_mset_add_mset [simp]:
Mathias@63793
  1245
   "filter_mset P (add_mset x A) =
Mathias@63795
  1246
     (if P x then add_mset x (filter_mset P A) else filter_mset P A)"
Mathias@63793
  1247
   by (auto simp: multiset_eq_iff)
Mathias@63793
  1248
haftmann@62430
  1249
lemma multiset_filter_subset[simp]: "filter_mset f M \<subseteq># M"
Mathias@63310
  1250
  by (simp add: mset_subset_eqI)
Mathias@60397
  1251
wenzelm@60606
  1252
lemma multiset_filter_mono:
haftmann@62430
  1253
  assumes "A \<subseteq># B"
haftmann@62430
  1254
  shows "filter_mset f A \<subseteq># filter_mset f B"
blanchet@58035
  1255
proof -
Mathias@63310
  1256
  from assms[unfolded mset_subset_eq_exists_conv]
blanchet@58035
  1257
  obtain C where B: "B = A + C" by auto
blanchet@58035
  1258
  show ?thesis unfolding B by auto
blanchet@58035
  1259
qed
blanchet@58035
  1260
haftmann@62430
  1261
lemma filter_mset_eq_conv:
haftmann@62430
  1262
  "filter_mset P M = N \<longleftrightarrow> N \<subseteq># M \<and> (\<forall>b\<in>#N. P b) \<and> (\<forall>a\<in>#M - N. \<not> P a)" (is "?P \<longleftrightarrow> ?Q")
haftmann@62430
  1263
proof
haftmann@62430
  1264
  assume ?P then show ?Q by auto (simp add: multiset_eq_iff in_diff_count)
haftmann@62430
  1265
next
haftmann@62430
  1266
  assume ?Q
haftmann@62430
  1267
  then obtain Q where M: "M = N + Q"
Mathias@63310
  1268
    by (auto simp add: mset_subset_eq_exists_conv)
haftmann@62430
  1269
  then have MN: "M - N = Q" by simp
haftmann@62430
  1270
  show ?P
haftmann@62430
  1271
  proof (rule multiset_eqI)
haftmann@62430
  1272
    fix a
haftmann@62430
  1273
    from \<open>?Q\<close> MN have *: "\<not> P a \<Longrightarrow> a \<notin># N" "P a \<Longrightarrow> a \<notin># Q"
haftmann@62430
  1274
      by auto
haftmann@62430
  1275
    show "count (filter_mset P M) a = count N a"
haftmann@62430
  1276
    proof (cases "a \<in># M")
haftmann@62430
  1277
      case True
haftmann@62430
  1278
      with * show ?thesis
haftmann@62430
  1279
        by (simp add: not_in_iff M)
haftmann@62430
  1280
    next
haftmann@62430
  1281
      case False then have "count M a = 0"
haftmann@62430
  1282
        by (simp add: not_in_iff)
haftmann@62430
  1283
      with M show ?thesis by simp
Mathias@63793
  1284
    qed
haftmann@62430
  1285
  qed
haftmann@62430
  1286
qed
blanchet@59813
  1287
blanchet@59813
  1288
wenzelm@60500
  1289
subsubsection \<open>Size\<close>
wenzelm@10249
  1290
blanchet@56656
  1291
definition wcount where "wcount f M = (\<lambda>x. count M x * Suc (f x))"
blanchet@56656
  1292
blanchet@56656
  1293
lemma wcount_union: "wcount f (M + N) a = wcount f M a + wcount f N a"
blanchet@56656
  1294
  by (auto simp: wcount_def add_mult_distrib)
blanchet@56656
  1295
Mathias@63793
  1296
lemma wcount_add_mset:
Mathias@63793
  1297
  "wcount f (add_mset x M) a = (if x = a then Suc (f a) else 0) + wcount f M a"
Mathias@63793
  1298
  unfolding add_mset_add_single[of _ M] wcount_union by (auto simp: wcount_def)
Mathias@63793
  1299
blanchet@56656
  1300
definition size_multiset :: "('a \<Rightarrow> nat) \<Rightarrow> 'a multiset \<Rightarrow> nat" where
nipkow@60495
  1301
  "size_multiset f M = setsum (wcount f M) (set_mset M)"
blanchet@56656
  1302
blanchet@56656
  1303
lemmas size_multiset_eq = size_multiset_def[unfolded wcount_def]
blanchet@56656
  1304
wenzelm@60606
  1305
instantiation multiset :: (type) size
wenzelm@60606
  1306
begin
wenzelm@60606
  1307
blanchet@56656
  1308
definition size_multiset where
blanchet@56656
  1309
  size_multiset_overloaded_def: "size_multiset = Multiset.size_multiset (\<lambda>_. 0)"
haftmann@34943
  1310
instance ..
wenzelm@60606
  1311
haftmann@34943
  1312
end
haftmann@34943
  1313
blanchet@56656
  1314
lemmas size_multiset_overloaded_eq =
blanchet@56656
  1315
  size_multiset_overloaded_def[THEN fun_cong, unfolded size_multiset_eq, simplified]
blanchet@56656
  1316
blanchet@56656
  1317
lemma size_multiset_empty [simp]: "size_multiset f {#} = 0"
blanchet@56656
  1318
by (simp add: size_multiset_def)
blanchet@56656
  1319
haftmann@28708
  1320
lemma size_empty [simp]: "size {#} = 0"
blanchet@56656
  1321
by (simp add: size_multiset_overloaded_def)
blanchet@56656
  1322
Mathias@63793
  1323
lemma size_multiset_single : "size_multiset f {#b#} = Suc (f b)"
blanchet@56656
  1324
by (simp add: size_multiset_eq)
wenzelm@10249
  1325
Mathias@63793
  1326
lemma size_single: "size {#b#} = 1"
Mathias@63793
  1327
by (simp add: size_multiset_overloaded_def size_multiset_single)
blanchet@56656
  1328
blanchet@56656
  1329
lemma setsum_wcount_Int:
nipkow@60495
  1330
  "finite A \<Longrightarrow> setsum (wcount f N) (A \<inter> set_mset N) = setsum (wcount f N) A"
haftmann@62430
  1331
  by (induct rule: finite_induct)
haftmann@62430
  1332
    (simp_all add: Int_insert_left wcount_def count_eq_zero_iff)
blanchet@56656
  1333
blanchet@56656
  1334
lemma size_multiset_union [simp]:
blanchet@56656
  1335
  "size_multiset f (M + N::'a multiset) = size_multiset f M + size_multiset f N"
haftmann@57418
  1336
apply (simp add: size_multiset_def setsum_Un_nat setsum.distrib setsum_wcount_Int wcount_union)
blanchet@56656
  1337
apply (subst Int_commute)
blanchet@56656
  1338
apply (simp add: setsum_wcount_Int)
nipkow@26178
  1339
done
wenzelm@10249
  1340
Mathias@63793
  1341
lemma size_multiset_add_mset [simp]:
Mathias@63793
  1342
  "size_multiset f (add_mset a M) = Suc (f a) + size_multiset f M"
Mathias@63793
  1343
  unfolding add_mset_add_single[of _ M] size_multiset_union by (auto simp: size_multiset_single)
Mathias@63793
  1344
Mathias@63793
  1345
lemma size_add_mset [simp]: "size (add_mset a A) = Suc (size A)"
Mathias@63793
  1346
by (simp add: size_multiset_overloaded_def wcount_add_mset)
Mathias@63793
  1347
haftmann@28708
  1348
lemma size_union [simp]: "size (M + N::'a multiset) = size M + size N"
blanchet@56656
  1349
by (auto simp add: size_multiset_overloaded_def)
blanchet@56656
  1350
haftmann@62430
  1351
lemma size_multiset_eq_0_iff_empty [iff]:
haftmann@62430
  1352
  "size_multiset f M = 0 \<longleftrightarrow> M = {#}"
haftmann@62430
  1353
  by (auto simp add: size_multiset_eq count_eq_zero_iff)
wenzelm@10249
  1354
wenzelm@17161
  1355
lemma size_eq_0_iff_empty [iff]: "(size M = 0) = (M = {#})"
blanchet@56656
  1356
by (auto simp add: size_multiset_overloaded_def)
nipkow@26016
  1357
nipkow@26016
  1358
lemma nonempty_has_size: "(S \<noteq> {#}) = (0 < size S)"
nipkow@26178
  1359
by (metis gr0I gr_implies_not0 size_empty size_eq_0_iff_empty)
wenzelm@10249
  1360
wenzelm@60607
  1361
lemma size_eq_Suc_imp_elem: "size M = Suc n \<Longrightarrow> \<exists>a. a \<in># M"
blanchet@56656
  1362
apply (unfold size_multiset_overloaded_eq)
nipkow@26178
  1363
apply (drule setsum_SucD)
nipkow@26178
  1364
apply auto
nipkow@26178
  1365
done
wenzelm@10249
  1366
haftmann@34943
  1367
lemma size_eq_Suc_imp_eq_union:
haftmann@34943
  1368
  assumes "size M = Suc n"
Mathias@63793
  1369
  shows "\<exists>a N. M = add_mset a N"
haftmann@34943
  1370
proof -
haftmann@34943
  1371
  from assms obtain a where "a \<in># M"
haftmann@34943
  1372
    by (erule size_eq_Suc_imp_elem [THEN exE])
Mathias@63793
  1373
  then have "M = add_mset a (M - {#a#})" by simp
haftmann@34943
  1374
  then show ?thesis by blast
nipkow@23611
  1375
qed
kleing@15869
  1376
wenzelm@60606
  1377
lemma size_mset_mono:
wenzelm@60606
  1378
  fixes A B :: "'a multiset"
haftmann@62430
  1379
  assumes "A \<subseteq># B"
wenzelm@60606
  1380
  shows "size A \<le> size B"
nipkow@59949
  1381
proof -
Mathias@63310
  1382
  from assms[unfolded mset_subset_eq_exists_conv]
nipkow@59949
  1383
  obtain C where B: "B = A + C" by auto
wenzelm@60606
  1384
  show ?thesis unfolding B by (induct C) auto
nipkow@59949
  1385
qed
nipkow@59949
  1386
nipkow@59998
  1387
lemma size_filter_mset_lesseq[simp]: "size (filter_mset f M) \<le> size M"
nipkow@59949
  1388
by (rule size_mset_mono[OF multiset_filter_subset])
nipkow@59949
  1389
nipkow@59949
  1390
lemma size_Diff_submset:
haftmann@62430
  1391
  "M \<subseteq># M' \<Longrightarrow> size (M' - M) = size M' - size(M::'a multiset)"
Mathias@63310
  1392
by (metis add_diff_cancel_left' size_union mset_subset_eq_exists_conv)
nipkow@26016
  1393
haftmann@62430
  1394
wenzelm@60500
  1395
subsection \<open>Induction and case splits\<close>
wenzelm@10249
  1396
wenzelm@18258
  1397
theorem multiset_induct [case_names empty add, induct type: multiset]:
huffman@48009
  1398
  assumes empty: "P {#}"
Mathias@63793
  1399
  assumes add: "\<And>x M. P M \<Longrightarrow> P (add_mset x M)"
huffman@48009
  1400
  shows "P M"
huffman@48009
  1401
proof (induct n \<equiv> "size M" arbitrary: M)
huffman@48009
  1402
  case 0 thus "P M" by (simp add: empty)
huffman@48009
  1403
next
huffman@48009
  1404
  case (Suc k)
Mathias@63793
  1405
  obtain N x where "M = add_mset x N"
wenzelm@60500
  1406
    using \<open>Suc k = size M\<close> [symmetric]
huffman@48009
  1407
    using size_eq_Suc_imp_eq_union by fast
huffman@48009
  1408
  with Suc add show "P M" by simp
wenzelm@10249
  1409
qed
wenzelm@10249
  1410
Mathias@63793
  1411
lemma multi_nonempty_split: "M \<noteq> {#} \<Longrightarrow> \<exists>A a. M = add_mset a A"
nipkow@26178
  1412
by (induct M) auto
kleing@25610
  1413
wenzelm@55913
  1414
lemma multiset_cases [cases type]:
wenzelm@55913
  1415
  obtains (empty) "M = {#}"
Mathias@63793
  1416
    | (add) x N where "M = add_mset x N"
wenzelm@63092
  1417
  by (induct M) simp_all
kleing@25610
  1418
haftmann@34943
  1419
lemma multi_drop_mem_not_eq: "c \<in># B \<Longrightarrow> B - {#c#} \<noteq> B"
haftmann@34943
  1420
by (cases "B = {#}") (auto dest: multi_member_split)
haftmann@34943
  1421
wenzelm@60607
  1422
lemma multiset_partition: "M = {# x\<in>#M. P x #} + {# x\<in>#M. \<not> P x #}"
nipkow@39302
  1423
apply (subst multiset_eq_iff)
nipkow@26178
  1424
apply auto
nipkow@26178
  1425
done
wenzelm@10249
  1426
Mathias@63310
  1427
lemma mset_subset_size: "(A::'a multiset) \<subset># B \<Longrightarrow> size A < size B"
haftmann@34943
  1428
proof (induct A arbitrary: B)
haftmann@34943
  1429
  case (empty M)
Mathias@63310
  1430
  then have "M \<noteq> {#}" by (simp add: mset_subset_empty_nonempty)
Mathias@63793
  1431
  then obtain M' x where "M = add_mset x M'"
haftmann@34943
  1432
    by (blast dest: multi_nonempty_split)
haftmann@34943
  1433
  then show ?case by simp
haftmann@34943
  1434
next
Mathias@63793
  1435
  case (add x S T)
haftmann@62430
  1436
  have IH: "\<And>B. S \<subset># B \<Longrightarrow> size S < size B" by fact
Mathias@63793
  1437
  have SxsubT: "add_mset x S \<subset># T" by fact
haftmann@62430
  1438
  then have "x \<in># T" and "S \<subset># T"
Mathias@63310
  1439
    by (auto dest: mset_subset_insertD)
Mathias@63793
  1440
  then obtain T' where T: "T = add_mset x T'"
haftmann@34943
  1441
    by (blast dest: multi_member_split)
haftmann@62430
  1442
  then have "S \<subset># T'" using SxsubT
Mathias@63793
  1443
    by simp
haftmann@34943
  1444
  then have "size S < size T'" using IH by simp
haftmann@34943
  1445
  then show ?case using T by simp
haftmann@34943
  1446
qed
haftmann@34943
  1447
nipkow@59949
  1448
lemma size_1_singleton_mset: "size M = 1 \<Longrightarrow> \<exists>a. M = {#a#}"
nipkow@59949
  1449
by (cases M) auto
nipkow@59949
  1450
haftmann@62430
  1451
wenzelm@60500
  1452
subsubsection \<open>Strong induction and subset induction for multisets\<close>
wenzelm@60500
  1453
wenzelm@60500
  1454
text \<open>Well-foundedness of strict subset relation\<close>
haftmann@58098
  1455
Mathias@63310
  1456
lemma wf_subset_mset_rel: "wf {(M, N :: 'a multiset). M \<subset># N}"
haftmann@34943
  1457
apply (rule wf_measure [THEN wf_subset, where f1=size])
Mathias@63310
  1458
apply (clarsimp simp: measure_def inv_image_def mset_subset_size)
haftmann@34943
  1459
done
haftmann@34943
  1460
haftmann@34943
  1461
lemma full_multiset_induct [case_names less]:
haftmann@62430
  1462
assumes ih: "\<And>B. \<forall>(A::'a multiset). A \<subset># B \<longrightarrow> P A \<Longrightarrow> P B"
haftmann@34943
  1463
shows "P B"
Mathias@63310
  1464
apply (rule wf_subset_mset_rel [THEN wf_induct])
haftmann@58098
  1465
apply (rule ih, auto)
haftmann@34943
  1466
done
haftmann@34943
  1467
haftmann@34943
  1468
lemma multi_subset_induct [consumes 2, case_names empty add]:
haftmann@62430
  1469
  assumes "F \<subseteq># A"
wenzelm@60606
  1470
    and empty: "P {#}"
Mathias@63793
  1471
    and insert: "\<And>a F. a \<in># A \<Longrightarrow> P F \<Longrightarrow> P (add_mset a F)"
wenzelm@60606
  1472
  shows "P F"
haftmann@34943
  1473
proof -
haftmann@62430
  1474
  from \<open>F \<subseteq># A\<close>
haftmann@34943
  1475
  show ?thesis
haftmann@34943
  1476
  proof (induct F)
haftmann@34943
  1477
    show "P {#}" by fact
haftmann@34943
  1478
  next
haftmann@34943
  1479
    fix x F
Mathias@63793
  1480
    assume P: "F \<subseteq># A \<Longrightarrow> P F" and i: "add_mset x F \<subseteq># A"
Mathias@63793
  1481
    show "P (add_mset x F)"
haftmann@34943
  1482
    proof (rule insert)
Mathias@63310
  1483
      from i show "x \<in># A" by (auto dest: mset_subset_eq_insertD)
Mathias@63310
  1484
      from i have "F \<subseteq># A" by (auto dest: mset_subset_eq_insertD)
haftmann@34943
  1485
      with P show "P F" .
haftmann@34943
  1486
    qed
haftmann@34943
  1487
  qed
haftmann@34943
  1488
qed
wenzelm@26145
  1489
wenzelm@17161
  1490
wenzelm@60500
  1491
subsection \<open>The fold combinator\<close>
huffman@48023
  1492
nipkow@59998
  1493
definition fold_mset :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'b \<Rightarrow> 'a multiset \<Rightarrow> 'b"
huffman@48023
  1494
where
nipkow@60495
  1495
  "fold_mset f s M = Finite_Set.fold (\<lambda>x. f x ^^ count M x) s (set_mset M)"
huffman@48023
  1496
wenzelm@60606
  1497
lemma fold_mset_empty [simp]: "fold_mset f s {#} = s"
nipkow@59998
  1498
  by (simp add: fold_mset_def)
huffman@48023
  1499
huffman@48023
  1500
context comp_fun_commute
huffman@48023
  1501
begin
huffman@48023
  1502
Mathias@63793
  1503
lemma fold_mset_add_mset [simp]: "fold_mset f s (add_mset x M) = f x (fold_mset f s M)"
haftmann@49822
  1504
proof -
haftmann@49822
  1505
  interpret mset: comp_fun_commute "\<lambda>y. f y ^^ count M y"
haftmann@49822
  1506
    by (fact comp_fun_commute_funpow)
Mathias@63793
  1507
  interpret mset_union: comp_fun_commute "\<lambda>y. f y ^^ count (add_mset x M) y"
haftmann@49822
  1508
    by (fact comp_fun_commute_funpow)
haftmann@49822
  1509
  show ?thesis
nipkow@60495
  1510
  proof (cases "x \<in> set_mset M")
haftmann@49822
  1511
    case False
Mathias@63793
  1512
    then have *: "count (add_mset x M) x = 1"
haftmann@62430
  1513
      by (simp add: not_in_iff)
Mathias@63793
  1514
    from False have "Finite_Set.fold (\<lambda>y. f y ^^ count (add_mset x M) y) s (set_mset M) =
nipkow@60495
  1515
      Finite_Set.fold (\<lambda>y. f y ^^ count M y) s (set_mset M)"
haftmann@49822
  1516
      by (auto intro!: Finite_Set.fold_cong comp_fun_commute_funpow)
haftmann@49822
  1517
    with False * show ?thesis
Mathias@63793
  1518
      by (simp add: fold_mset_def del: count_add_mset)
huffman@48023
  1519
  next
haftmann@49822
  1520
    case True
wenzelm@63040
  1521
    define N where "N = set_mset M - {x}"
nipkow@60495
  1522
    from N_def True have *: "set_mset M = insert x N" "x \<notin> N" "finite N" by auto
Mathias@63793
  1523
    then have "Finite_Set.fold (\<lambda>y. f y ^^ count (add_mset x M) y) s N =
haftmann@49822
  1524
      Finite_Set.fold (\<lambda>y. f y ^^ count M y) s N"
haftmann@49822
  1525
      by (auto intro!: Finite_Set.fold_cong comp_fun_commute_funpow)
Mathias@63793
  1526
    with * show ?thesis by (simp add: fold_mset_def del: count_add_mset) simp
huffman@48023
  1527
  qed
huffman@48023
  1528
qed
huffman@48023
  1529
Mathias@63793
  1530
corollary fold_mset_single: "fold_mset f s {#x#} = f x s"
Mathias@63793
  1531
  by simp
huffman@48023
  1532
wenzelm@60606
  1533
lemma fold_mset_fun_left_comm: "f x (fold_mset f s M) = fold_mset f (f x s) M"
Mathias@63793
  1534
  by (induct M) (simp_all add: fun_left_comm)
huffman@48023
  1535
wenzelm@60606
  1536
lemma fold_mset_union [simp]: "fold_mset f s (M + N) = fold_mset f (fold_mset f s M) N"
Mathias@63793
  1537
  by (induct M) (simp_all add: fold_mset_fun_left_comm)
huffman@48023
  1538
huffman@48023
  1539
lemma fold_mset_fusion:
huffman@48023
  1540
  assumes "comp_fun_commute g"
wenzelm@60606
  1541
    and *: "\<And>x y. h (g x y) = f x (h y)"
wenzelm@60606
  1542
  shows "h (fold_mset g w A) = fold_mset f (h w) A"
huffman@48023
  1543
proof -
huffman@48023
  1544
  interpret comp_fun_commute g by (fact assms)
wenzelm@60606
  1545
  from * show ?thesis by (induct A) auto
huffman@48023
  1546
qed
huffman@48023
  1547
huffman@48023
  1548
end
huffman@48023
  1549
Mathias@63793
  1550
lemma union_fold_mset_add_mset: "A + B = fold_mset add_mset A B"
Mathias@63793
  1551
proof -
Mathias@63793
  1552
  interpret comp_fun_commute add_mset
Mathias@63793
  1553
    by standard auto
Mathias@63793
  1554
  show ?thesis
Mathias@63793
  1555
    by (induction B) auto
Mathias@63793
  1556
qed
Mathias@63793
  1557
wenzelm@60500
  1558
text \<open>
huffman@48023
  1559
  A note on code generation: When defining some function containing a
nipkow@59998
  1560
  subterm @{term "fold_mset F"}, code generation is not automatic. When
wenzelm@61585
  1561
  interpreting locale \<open>left_commutative\<close> with \<open>F\<close>, the
nipkow@59998
  1562
  would be code thms for @{const fold_mset} become thms like
wenzelm@61585
  1563
  @{term "fold_mset F z {#} = z"} where \<open>F\<close> is not a pattern but
huffman@48023
  1564
  contains defined symbols, i.e.\ is not a code thm. Hence a separate
wenzelm@61585
  1565
  constant with its own code thms needs to be introduced for \<open>F\<close>. See the image operator below.
wenzelm@60500
  1566
\<close>
wenzelm@60500
  1567
wenzelm@60500
  1568
wenzelm@60500
  1569
subsection \<open>Image\<close>
huffman@48023
  1570
huffman@48023
  1571
definition image_mset :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a multiset \<Rightarrow> 'b multiset" where
Mathias@63793
  1572
  "image_mset f = fold_mset (add_mset \<circ> f) {#}"
Mathias@63793
  1573
Mathias@63793
  1574
lemma comp_fun_commute_mset_image: "comp_fun_commute (add_mset \<circ> f)"
haftmann@49823
  1575
proof
Mathias@63794
  1576
qed (simp add: fun_eq_iff)
huffman@48023
  1577
huffman@48023
  1578
lemma image_mset_empty [simp]: "image_mset f {#} = {#}"
haftmann@49823
  1579
  by (simp add: image_mset_def)
huffman@48023
  1580
Mathias@63793
  1581
lemma image_mset_single: "image_mset f {#x#} = {#f x#}"
haftmann@49823
  1582
proof -
Mathias@63793
  1583
  interpret comp_fun_commute "add_mset \<circ> f"
haftmann@49823
  1584
    by (fact comp_fun_commute_mset_image)
haftmann@49823
  1585
  show ?thesis by (simp add: image_mset_def)
haftmann@49823
  1586
qed
huffman@48023
  1587
wenzelm@60606
  1588
lemma image_mset_union [simp]: "image_mset f (M + N) = image_mset f M + image_mset f N"
haftmann@49823
  1589
proof -
Mathias@63793
  1590
  interpret comp_fun_commute "add_mset \<circ> f"
haftmann@49823
  1591
    by (fact comp_fun_commute_mset_image)
Mathias@63794
  1592
  show ?thesis by (induct N) (simp_all add: image_mset_def)
haftmann@49823
  1593
qed
haftmann@49823
  1594
Mathias@63793
  1595
corollary image_mset_add_mset [simp]:
Mathias@63793
  1596
  "image_mset f (add_mset a M) = add_mset (f a) (image_mset f M)"
Mathias@63793
  1597
  unfolding image_mset_union add_mset_add_single[of a M] by (simp add: image_mset_single)
huffman@48023
  1598
wenzelm@60606
  1599
lemma set_image_mset [simp]: "set_mset (image_mset f M) = image f (set_mset M)"
haftmann@49823
  1600
  by (induct M) simp_all
huffman@48040
  1601
wenzelm@60606
  1602
lemma size_image_mset [simp]: "size (image_mset f M) = size M"
haftmann@49823
  1603
  by (induct M) simp_all
huffman@48023
  1604
wenzelm@60606
  1605
lemma image_mset_is_empty_iff [simp]: "image_mset f M = {#} \<longleftrightarrow> M = {#}"
haftmann@49823
  1606
  by (cases M) auto
huffman@48023
  1607
eberlm@63099
  1608
lemma image_mset_If:
Mathias@63793
  1609
  "image_mset (\<lambda>x. if P x then f x else g x) A =
eberlm@63099
  1610
     image_mset f (filter_mset P A) + image_mset g (filter_mset (\<lambda>x. \<not>P x) A)"
Mathias@63794
  1611
  by (induction A) auto
eberlm@63099
  1612
Mathias@63793
  1613
lemma image_mset_Diff:
eberlm@63099
  1614
  assumes "B \<subseteq># A"
eberlm@63099
  1615
  shows   "image_mset f (A - B) = image_mset f A - image_mset f B"
eberlm@63099
  1616
proof -
eberlm@63099
  1617
  have "image_mset f (A - B + B) = image_mset f (A - B) + image_mset f B"
eberlm@63099
  1618
    by simp
eberlm@63099
  1619
  also from assms have "A - B + B = A"
Mathias@63793
  1620
    by (simp add: subset_mset.diff_add)
eberlm@63099
  1621
  finally show ?thesis by simp
eberlm@63099
  1622
qed
eberlm@63099
  1623
Mathias@63793
  1624
lemma count_image_mset:
eberlm@63099
  1625
  "count (image_mset f A) x = (\<Sum>y\<in>f -` {x} \<inter> set_mset A. count A y)"
Mathias@63793
  1626
proof (induction A)
Mathias@63793
  1627
  case empty
Mathias@63793
  1628
  then show ?case by simp
Mathias@63793
  1629
next
Mathias@63793
  1630
  case (add x A)
Mathias@63793
  1631
  moreover have *: "(if x = y then Suc n else n) = n + (if x = y then 1 else 0)" for n y
Mathias@63793
  1632
    by simp
Mathias@63793
  1633
  ultimately show ?case
Mathias@63793
  1634
    by (auto simp: setsum.distrib setsum.delta' intro!: setsum.mono_neutral_left)
Mathias@63793
  1635
qed
eberlm@63099
  1636
Mathias@63795
  1637
lemma image_mset_subseteq_mono: "A \<subseteq># B \<Longrightarrow> image_mset f A \<subseteq># image_mset f B"
Mathias@63795
  1638
  by (metis image_mset_union subset_mset.le_iff_add)
Mathias@63795
  1639
wenzelm@61955
  1640
syntax (ASCII)
wenzelm@61955
  1641
  "_comprehension_mset" :: "'a \<Rightarrow> 'b \<Rightarrow> 'b multiset \<Rightarrow> 'a multiset"  ("({#_/. _ :# _#})")
huffman@48023
  1642
syntax
wenzelm@61955
  1643
  "_comprehension_mset" :: "'a \<Rightarrow> 'b \<Rightarrow> 'b multiset \<Rightarrow> 'a multiset"  ("({#_/. _ \<in># _#})")
blanchet@59813
  1644
translations
wenzelm@61955
  1645
  "{#e. x \<in># M#}" \<rightleftharpoons> "CONST image_mset (\<lambda>x. e) M"
wenzelm@61955
  1646
wenzelm@61955
  1647
syntax (ASCII)
wenzelm@61955
  1648
  "_comprehension_mset'" :: "'a \<Rightarrow> 'b \<Rightarrow> 'b multiset \<Rightarrow> bool \<Rightarrow> 'a multiset"  ("({#_/ | _ :# _./ _#})")
huffman@48023
  1649
syntax
wenzelm@61955
  1650
  "_comprehension_mset'" :: "'a \<Rightarrow> 'b \<Rightarrow> 'b multiset \<Rightarrow> bool \<Rightarrow> 'a multiset"  ("({#_/ | _ \<in># _./ _#})")
blanchet@59813
  1651
translations
wenzelm@60606
  1652
  "{#e | x\<in>#M. P#}" \<rightharpoonup> "{#e. x \<in># {# x\<in>#M. P#}#}"
blanchet@59813
  1653
wenzelm@60500
  1654
text \<open>
wenzelm@60607
  1655
  This allows to write not just filters like @{term "{#x\<in>#M. x<c#}"}
wenzelm@60607
  1656
  but also images like @{term "{#x+x. x\<in>#M #}"} and @{term [source]
wenzelm@60607
  1657
  "{#x+x|x\<in>#M. x<c#}"}, where the latter is currently displayed as
wenzelm@60607
  1658
  @{term "{#x+x|x\<in>#M. x<c#}"}.
wenzelm@60500
  1659
\<close>
huffman@48023
  1660
nipkow@60495
  1661
lemma in_image_mset: "y \<in># {#f x. x \<in># M#} \<longleftrightarrow> y \<in> f ` set_mset M"
haftmann@62430
  1662
by (metis set_image_mset)
blanchet@59813
  1663
blanchet@55467
  1664
functor image_mset: image_mset
huffman@48023
  1665
proof -
huffman@48023
  1666
  fix f g show "image_mset f \<circ> image_mset g = image_mset (f \<circ> g)"
huffman@48023
  1667
  proof
huffman@48023
  1668
    fix A
huffman@48023
  1669
    show "(image_mset f \<circ> image_mset g) A = image_mset (f \<circ> g) A"
huffman@48023
  1670
      by (induct A) simp_all
huffman@48023
  1671
  qed
huffman@48023
  1672
  show "image_mset id = id"
huffman@48023
  1673
  proof
huffman@48023
  1674
    fix A
huffman@48023
  1675
    show "image_mset id A = id A"
huffman@48023
  1676
      by (induct A) simp_all
huffman@48023
  1677
  qed
huffman@48023
  1678
qed
huffman@48023
  1679
blanchet@59813
  1680
declare
blanchet@59813
  1681
  image_mset.id [simp]
blanchet@59813
  1682
  image_mset.identity [simp]
blanchet@59813
  1683
blanchet@59813
  1684
lemma image_mset_id[simp]: "image_mset id x = x"
blanchet@59813
  1685
  unfolding id_def by auto
blanchet@59813
  1686
blanchet@59813
  1687
lemma image_mset_cong: "(\<And>x. x \<in># M \<Longrightarrow> f x = g x) \<Longrightarrow> {#f x. x \<in># M#} = {#g x. x \<in># M#}"
blanchet@59813
  1688
  by (induct M) auto
blanchet@59813
  1689
blanchet@59813
  1690
lemma image_mset_cong_pair:
blanchet@59813
  1691
  "(\<forall>x y. (x, y) \<in># M \<longrightarrow> f x y = g x y) \<Longrightarrow> {#f x y. (x, y) \<in># M#} = {#g x y. (x, y) \<in># M#}"
blanchet@59813
  1692
  by (metis image_mset_cong split_cong)
haftmann@49717
  1693
huffman@48023
  1694
wenzelm@60500
  1695
subsection \<open>Further conversions\<close>
haftmann@34943
  1696
nipkow@60515
  1697
primrec mset :: "'a list \<Rightarrow> 'a multiset" where
nipkow@60515
  1698
  "mset [] = {#}" |
Mathias@63793
  1699
  "mset (a # x) = add_mset a (mset x)"
haftmann@34943
  1700
haftmann@37107
  1701
lemma in_multiset_in_set:
nipkow@60515
  1702
  "x \<in># mset xs \<longleftrightarrow> x \<in> set xs"
haftmann@37107
  1703
  by (induct xs) simp_all
haftmann@37107
  1704
nipkow@60515
  1705
lemma count_mset:
nipkow@60515
  1706
  "count (mset xs) x = length (filter (\<lambda>y. x = y) xs)"
haftmann@37107
  1707
  by (induct xs) simp_all
haftmann@37107
  1708
nipkow@60515
  1709
lemma mset_zero_iff[simp]: "(mset x = {#}) = (x = [])"
blanchet@59813
  1710
  by (induct x) auto
haftmann@34943
  1711
nipkow@60515
  1712
lemma mset_zero_iff_right[simp]: "({#} = mset x) = (x = [])"
haftmann@34943
  1713
by (induct x) auto
haftmann@34943
  1714
nipkow@60515
  1715
lemma set_mset_mset[simp]: "set_mset (mset x) = set x"
haftmann@34943
  1716
by (induct x) auto
haftmann@34943
  1717
haftmann@62430
  1718
lemma set_mset_comp_mset [simp]: "set_mset \<circ> mset = set"
haftmann@62430
  1719
  by (simp add: fun_eq_iff)
haftmann@34943
  1720
nipkow@60515
  1721
lemma size_mset [simp]: "size (mset xs) = length xs"
huffman@48012
  1722
  by (induct xs) simp_all
huffman@48012
  1723
wenzelm@60606
  1724
lemma mset_append [simp]: "mset (xs @ ys) = mset xs + mset ys"
Mathias@63794
  1725
  by (induct xs arbitrary: ys) auto
haftmann@34943
  1726
wenzelm@60607
  1727
lemma mset_filter: "mset (filter P xs) = {#x \<in># mset xs. P x #}"
haftmann@40303
  1728
  by (induct xs) simp_all
haftmann@40303
  1729
nipkow@60515
  1730
lemma mset_rev [simp]:
nipkow@60515
  1731
  "mset (rev xs) = mset xs"
haftmann@40950
  1732
  by (induct xs) simp_all
haftmann@40950
  1733
nipkow@60515
  1734
lemma surj_mset: "surj mset"
haftmann@34943
  1735
apply (unfold surj_def)
haftmann@34943
  1736
apply (rule allI)
haftmann@34943
  1737
apply (rule_tac M = y in multiset_induct)
haftmann@34943
  1738
 apply auto
haftmann@34943
  1739
apply (rule_tac x = "x # xa" in exI)
haftmann@34943
  1740
apply auto
haftmann@34943
  1741
done
haftmann@34943
  1742
haftmann@34943
  1743
lemma distinct_count_atmost_1:
wenzelm@60606
  1744
  "distinct x = (\<forall>a. count (mset x) a = (if a \<in> set x then 1 else 0))"
haftmann@62430
  1745
proof (induct x)
haftmann@62430
  1746
  case Nil then show ?case by simp
haftmann@62430
  1747
next
haftmann@62430
  1748
  case (Cons x xs) show ?case (is "?lhs \<longleftrightarrow> ?rhs")
haftmann@62430
  1749
  proof
haftmann@62430
  1750
    assume ?lhs then show ?rhs using Cons by simp
haftmann@62430
  1751
  next
haftmann@62430
  1752
    assume ?rhs then have "x \<notin> set xs"
haftmann@62430
  1753
      by (simp split: if_splits)
haftmann@62430
  1754
    moreover from \<open>?rhs\<close> have "(\<forall>a. count (mset xs) a =
haftmann@62430
  1755
       (if a \<in> set xs then 1 else 0))"
haftmann@62430
  1756
      by (auto split: if_splits simp add: count_eq_zero_iff)
haftmann@62430
  1757
    ultimately show ?lhs using Cons by simp
haftmann@62430
  1758
  qed
haftmann@62430
  1759
qed
haftmann@62430
  1760
haftmann@62430
  1761
lemma mset_eq_setD:
haftmann@62430
  1762
  assumes "mset xs = mset ys"
haftmann@62430
  1763
  shows "set xs = set ys"
haftmann@62430
  1764
proof -
haftmann@62430
  1765
  from assms have "set_mset (mset xs) = set_mset (mset ys)"
haftmann@62430
  1766
    by simp
haftmann@62430
  1767
  then show ?thesis by simp
haftmann@62430
  1768
qed
haftmann@34943
  1769
nipkow@60515
  1770
lemma set_eq_iff_mset_eq_distinct:
haftmann@34943
  1771
  "distinct x \<Longrightarrow> distinct y \<Longrightarrow>
nipkow@60515
  1772
    (set x = set y) = (mset x = mset y)"
nipkow@39302
  1773
by (auto simp: multiset_eq_iff distinct_count_atmost_1)
haftmann@34943
  1774
nipkow@60515
  1775
lemma set_eq_iff_mset_remdups_eq:
nipkow@60515
  1776
   "(set x = set y) = (mset (remdups x) = mset (remdups y))"
haftmann@34943
  1777
apply (rule iffI)
nipkow@60515
  1778
apply (simp add: set_eq_iff_mset_eq_distinct[THEN iffD1])
haftmann@34943
  1779
apply (drule distinct_remdups [THEN distinct_remdups
nipkow@60515
  1780
      [THEN set_eq_iff_mset_eq_distinct [THEN iffD2]]])
haftmann@34943
  1781
apply simp
haftmann@34943
  1782
done
haftmann@34943
  1783
wenzelm@60606
  1784
lemma mset_compl_union [simp]: "mset [x\<leftarrow>xs. P x] + mset [x\<leftarrow>xs. \<not>P x] = mset xs"
Mathias@63794
  1785
  by (induct xs) auto
haftmann@34943
  1786
wenzelm@60607
  1787
lemma nth_mem_mset: "i < length ls \<Longrightarrow> (ls ! i) \<in># mset ls"
wenzelm@60678
  1788
proof (induct ls arbitrary: i)
wenzelm@60678
  1789
  case Nil
wenzelm@60678
  1790
  then show ?case by simp
wenzelm@60678
  1791
next
wenzelm@60678
  1792
  case Cons
wenzelm@60678
  1793
  then show ?case by (cases i) auto
wenzelm@60678
  1794
qed
haftmann@34943
  1795
wenzelm@60606
  1796
lemma mset_remove1[simp]: "mset (remove1 a xs) = mset xs - {#a#}"
wenzelm@60678
  1797
  by (induct xs) (auto simp add: multiset_eq_iff)
haftmann@34943
  1798
nipkow@60515
  1799
lemma mset_eq_length:
nipkow@60515
  1800
  assumes "mset xs = mset ys"
haftmann@37107
  1801
  shows "length xs = length ys"
nipkow@60515
  1802
  using assms by (metis size_mset)
nipkow@60515
  1803
nipkow@60515
  1804
lemma mset_eq_length_filter:
nipkow@60515
  1805
  assumes "mset xs = mset ys"
haftmann@39533
  1806
  shows "length (filter (\<lambda>x. z = x) xs) = length (filter (\<lambda>y. z = y) ys)"
nipkow@60515
  1807
  using assms by (metis count_mset)
haftmann@39533
  1808
haftmann@45989
  1809
lemma fold_multiset_equiv:
haftmann@45989
  1810
  assumes f: "\<And>x y. x \<in> set xs \<Longrightarrow> y \<in> set xs \<Longrightarrow> f x \<circ> f y = f y \<circ> f x"
nipkow@60515
  1811
    and equiv: "mset xs = mset ys"
haftmann@49822
  1812
  shows "List.fold f xs = List.fold f ys"
wenzelm@60606
  1813
  using f equiv [symmetric]
wenzelm@46921
  1814
proof (induct xs arbitrary: ys)
wenzelm@60678
  1815
  case Nil
wenzelm@60678
  1816
  then show ?case by simp
haftmann@45989
  1817
next
haftmann@45989
  1818
  case (Cons x xs)
wenzelm@60678
  1819
  then have *: "set ys = set (x # xs)"
wenzelm@60678
  1820
    by (blast dest: mset_eq_setD)
blanchet@58425
  1821
  have "\<And>x y. x \<in> set ys \<Longrightarrow> y \<in> set ys \<Longrightarrow> f x \<circ> f y = f y \<circ> f x"
haftmann@45989
  1822
    by (rule Cons.prems(1)) (simp_all add: *)
wenzelm@60678
  1823
  moreover from * have "x \<in> set ys"
wenzelm@60678
  1824
    by simp
wenzelm@60678
  1825
  ultimately have "List.fold f ys = List.fold f (remove1 x ys) \<circ> f x"
wenzelm@60678
  1826
    by (fact fold_remove1_split)
wenzelm@60678
  1827
  moreover from Cons.prems have "List.fold f xs = List.fold f (remove1 x ys)"
wenzelm@60678
  1828
    by (auto intro: Cons.hyps)
haftmann@45989
  1829
  ultimately show ?case by simp
haftmann@45989
  1830
qed
haftmann@45989
  1831
Mathias@63793
  1832
lemma mset_insort [simp]: "mset (insort x xs) = add_mset x (mset xs)"
Mathias@63793
  1833
  by (induct xs) simp_all
haftmann@51548
  1834
Mathias@63524
  1835
lemma mset_map[simp]: "mset (map f xs) = image_mset f (mset xs)"
haftmann@51600
  1836
  by (induct xs) simp_all
haftmann@51600
  1837
Mathias@63793
  1838
global_interpretation mset_set: folding add_mset "{#}"
Mathias@63793
  1839
  defines mset_set = "folding.F add_mset {#}"
Mathias@63794
  1840
  by standard (simp add: fun_eq_iff)
haftmann@51548
  1841
nipkow@60513
  1842
lemma count_mset_set [simp]:
nipkow@60513
  1843
  "finite A \<Longrightarrow> x \<in> A \<Longrightarrow> count (mset_set A) x = 1" (is "PROP ?P")
nipkow@60513
  1844
  "\<not> finite A \<Longrightarrow> count (mset_set A) x = 0" (is "PROP ?Q")
nipkow@60513
  1845
  "x \<notin> A \<Longrightarrow> count (mset_set A) x = 0" (is "PROP ?R")
haftmann@51600
  1846
proof -
wenzelm@60606
  1847
  have *: "count (mset_set A) x = 0" if "x \<notin> A" for A
wenzelm@60606
  1848
  proof (cases "finite A")
wenzelm@60606
  1849
    case False then show ?thesis by simp
wenzelm@60606
  1850
  next
wenzelm@60606
  1851
    case True from True \<open>x \<notin> A\<close> show ?thesis by (induct A) auto
wenzelm@60606
  1852
  qed
haftmann@51600
  1853
  then show "PROP ?P" "PROP ?Q" "PROP ?R"
haftmann@51600
  1854
  by (auto elim!: Set.set_insert)
wenzelm@61585
  1855
qed \<comment> \<open>TODO: maybe define @{const mset_set} also in terms of @{const Abs_multiset}\<close>
nipkow@60513
  1856
nipkow@60513
  1857
lemma elem_mset_set[simp, intro]: "finite A \<Longrightarrow> x \<in># mset_set A \<longleftrightarrow> x \<in> A"
blanchet@59813
  1858
  by (induct A rule: finite_induct) simp_all
blanchet@59813
  1859
Mathias@63793
  1860
lemma mset_set_Union:
eberlm@63099
  1861
  "finite A \<Longrightarrow> finite B \<Longrightarrow> A \<inter> B = {} \<Longrightarrow> mset_set (A \<union> B) = mset_set A + mset_set B"
Mathias@63794
  1862
  by (induction A rule: finite_induct) auto
eberlm@63099
  1863
eberlm@63099
  1864
lemma filter_mset_mset_set [simp]:
eberlm@63099
  1865
  "finite A \<Longrightarrow> filter_mset P (mset_set A) = mset_set {x\<in>A. P x}"
eberlm@63099
  1866
proof (induction A rule: finite_induct)
eberlm@63099
  1867
  case (insert x A)
Mathias@63793
  1868
  from insert.hyps have "filter_mset P (mset_set (insert x A)) =
eberlm@63099
  1869
      filter_mset P (mset_set A) + mset_set (if P x then {x} else {})"
Mathias@63794
  1870
    by simp
eberlm@63099
  1871
  also have "filter_mset P (mset_set A) = mset_set {x\<in>A. P x}"
eberlm@63099
  1872
    by (rule insert.IH)
Mathias@63793
  1873
  also from insert.hyps
eberlm@63099
  1874
    have "\<dots> + mset_set (if P x then {x} else {}) =
eberlm@63099
  1875
            mset_set ({x \<in> A. P x} \<union> (if P x then {x} else {}))" (is "_ = mset_set ?A")
eberlm@63099
  1876
     by (intro mset_set_Union [symmetric]) simp_all
eberlm@63099
  1877
  also from insert.hyps have "?A = {y\<in>insert x A. P y}" by auto
eberlm@63099
  1878
  finally show ?case .
eberlm@63099
  1879
qed simp_all
eberlm@63099
  1880
eberlm@63099
  1881
lemma mset_set_Diff:
eberlm@63099
  1882
  assumes "finite A" "B \<subseteq> A"
eberlm@63099
  1883
  shows  "mset_set (A - B) = mset_set A - mset_set B"
eberlm@63099
  1884
proof -
eberlm@63099
  1885
  from assms have "mset_set ((A - B) \<union> B) = mset_set (A - B) + mset_set B"
eberlm@63099
  1886
    by (intro mset_set_Union) (auto dest: finite_subset)
eberlm@63099
  1887
  also from assms have "A - B \<union> B = A" by blast
eberlm@63099
  1888
  finally show ?thesis by simp
eberlm@63099
  1889
qed
eberlm@63099
  1890
eberlm@63099
  1891
lemma mset_set_set: "distinct xs \<Longrightarrow> mset_set (set xs) = mset xs"
Mathias@63794
  1892
  by (induction xs) simp_all
eberlm@63099
  1893
haftmann@51548
  1894
context linorder
haftmann@51548
  1895
begin
haftmann@51548
  1896
haftmann@51548
  1897
definition sorted_list_of_multiset :: "'a multiset \<Rightarrow> 'a list"
haftmann@51548
  1898
where
nipkow@59998
  1899
  "sorted_list_of_multiset M = fold_mset insort [] M"
haftmann@51548
  1900
haftmann@51548
  1901
lemma sorted_list_of_multiset_empty [simp]:
haftmann@51548
  1902
  "sorted_list_of_multiset {#} = []"
haftmann@51548
  1903
  by (simp add: sorted_list_of_multiset_def)
haftmann@51548
  1904
haftmann@51548
  1905
lemma sorted_list_of_multiset_singleton [simp]:
haftmann@51548
  1906
  "sorted_list_of_multiset {#x#} = [x]"
haftmann@51548
  1907
proof -
haftmann@51548
  1908
  interpret comp_fun_commute insort by (fact comp_fun_commute_insort)
haftmann@51548
  1909
  show ?thesis by (simp add: sorted_list_of_multiset_def)
haftmann@51548
  1910
qed
haftmann@51548
  1911
haftmann@51548
  1912
lemma sorted_list_of_multiset_insert [simp]:
Mathias@63793
  1913
  "sorted_list_of_multiset (add_mset x M) = List.insort x (sorted_list_of_multiset M)"
haftmann@51548
  1914
proof -
haftmann@51548
  1915
  interpret comp_fun_commute insort by (fact comp_fun_commute_insort)
haftmann@51548
  1916
  show ?thesis by (simp add: sorted_list_of_multiset_def)
haftmann@51548
  1917
qed
haftmann@51548
  1918
haftmann@51548
  1919
end
haftmann@51548
  1920
nipkow@60515
  1921
lemma mset_sorted_list_of_multiset [simp]:
nipkow@60515
  1922
  "mset (sorted_list_of_multiset M) = M"
nipkow@60513
  1923
by (induct M) simp_all
haftmann@51548
  1924
nipkow@60515
  1925
lemma sorted_list_of_multiset_mset [simp]:
nipkow@60515
  1926
  "sorted_list_of_multiset (mset xs) = sort xs"
nipkow@60513
  1927
by (induct xs) simp_all
nipkow@60513
  1928
nipkow@60513
  1929
lemma finite_set_mset_mset_set[simp]:
nipkow@60513
  1930
  "finite A \<Longrightarrow> set_mset (mset_set A) = A"
nipkow@60513
  1931
by (induct A rule: finite_induct) simp_all
nipkow@60513
  1932
eberlm@63099
  1933
lemma mset_set_empty_iff: "mset_set A = {#} \<longleftrightarrow> A = {} \<or> infinite A"
eberlm@63099
  1934
  using finite_set_mset_mset_set by fastforce
eberlm@63099
  1935
nipkow@60513
  1936
lemma infinite_set_mset_mset_set:
nipkow@60513
  1937
  "\<not> finite A \<Longrightarrow> set_mset (mset_set A) = {}"
nipkow@60513
  1938
by simp
haftmann@51548
  1939
haftmann@51548
  1940
lemma set_sorted_list_of_multiset [simp]:
nipkow@60495
  1941
  "set (sorted_list_of_multiset M) = set_mset M"
nipkow@60513
  1942
by (induct M) (simp_all add: set_insort)
nipkow@60513
  1943
nipkow@60513
  1944
lemma sorted_list_of_mset_set [simp]:
nipkow@60513
  1945
  "sorted_list_of_multiset (mset_set A) = sorted_list_of_set A"
Mathias@63794
  1946
by (cases "finite A") (induct A rule: finite_induct, simp_all)
haftmann@51548
  1947
eberlm@63099
  1948
lemma mset_upt [simp]: "mset [m..<n] = mset_set {m..<n}"
Mathias@63794
  1949
  by (induction n) (simp_all add: atLeastLessThanSuc)
eberlm@63099
  1950
Mathias@63793
  1951
lemma image_mset_map_of:
eberlm@63099
  1952
  "distinct (map fst xs) \<Longrightarrow> {#the (map_of xs i). i \<in># mset (map fst xs)#} = mset (map snd xs)"
eberlm@63099
  1953
proof (induction xs)
eberlm@63099
  1954
  case (Cons x xs)
Mathias@63793
  1955
  have "{#the (map_of (x # xs) i). i \<in># mset (map fst (x # xs))#} =
Mathias@63793
  1956
          add_mset (snd x) {#the (if i = fst x then Some (snd x) else map_of xs i).
Mathias@63793
  1957
             i \<in># mset (map fst xs)#}" (is "_ = add_mset _ ?A") by simp
eberlm@63099
  1958
  also from Cons.prems have "?A = {#the (map_of xs i). i :# mset (map fst xs)#}"
eberlm@63099
  1959
    by (cases x, intro image_mset_cong) (auto simp: in_multiset_in_set)
eberlm@63099
  1960
  also from Cons.prems have "\<dots> = mset (map snd xs)" by (intro Cons.IH) simp_all
eberlm@63099
  1961
  finally show ?case by simp
Mathias@63793
  1962
qed simp_all
eberlm@63099
  1963
haftmann@51548
  1964
haftmann@60804
  1965
subsection \<open>Replicate operation\<close>
haftmann@60804
  1966
haftmann@60804
  1967
definition replicate_mset :: "nat \<Rightarrow> 'a \<Rightarrow> 'a multiset" where
Mathias@63793
  1968
  "replicate_mset n x = (add_mset x ^^ n) {#}"
haftmann@60804
  1969
haftmann@60804
  1970
lemma replicate_mset_0[simp]: "replicate_mset 0 x = {#}"
haftmann@60804
  1971
  unfolding replicate_mset_def by simp
haftmann@60804
  1972
Mathias@63793
  1973
lemma replicate_mset_Suc [simp]: "replicate_mset (Suc n) x = add_mset x (replicate_mset n x)"
haftmann@60804
  1974
  unfolding replicate_mset_def by (induct n) (auto intro: add.commute)
haftmann@60804
  1975
haftmann@60804
  1976
lemma in_replicate_mset[simp]: "x \<in># replicate_mset n y \<longleftrightarrow> n > 0 \<and> x = y"
haftmann@62430
  1977
  unfolding replicate_mset_def by (induct n) auto
haftmann@60804
  1978
haftmann@60804
  1979
lemma count_replicate_mset[simp]: "count (replicate_mset n x) y = (if y = x then n else 0)"
Mathias@63793
  1980
  unfolding replicate_mset_def by (induct n) auto
haftmann@60804
  1981
haftmann@60804
  1982
lemma set_mset_replicate_mset_subset[simp]: "set_mset (replicate_mset n x) = (if n = 0 then {} else {x})"
haftmann@60804
  1983
  by (auto split: if_splits)
haftmann@60804
  1984
haftmann@60804
  1985
lemma size_replicate_mset[simp]: "size (replicate_mset n M) = n"
haftmann@60804
  1986
  by (induct n, simp_all)
haftmann@60804
  1987
Mathias@63310
  1988
lemma count_le_replicate_mset_subset_eq: "n \<le> count M x \<longleftrightarrow> replicate_mset n x \<subseteq># M"
Mathias@63310
  1989
  by (auto simp add: mset_subset_eqI) (metis count_replicate_mset subseteq_mset_def)
haftmann@60804
  1990
haftmann@60804
  1991
lemma filter_eq_replicate_mset: "{#y \<in># D. y = x#} = replicate_mset (count D x) x"
haftmann@60804
  1992
  by (induct D) simp_all
haftmann@60804
  1993
haftmann@61031
  1994
lemma replicate_count_mset_eq_filter_eq:
haftmann@61031
  1995
  "replicate (count (mset xs) k) k = filter (HOL.eq k) xs"
haftmann@61031
  1996
  by (induct xs) auto
haftmann@61031
  1997
haftmann@62366
  1998
lemma replicate_mset_eq_empty_iff [simp]:
haftmann@62366
  1999
  "replicate_mset n a = {#} \<longleftrightarrow> n = 0"
haftmann@62366
  2000
  by (induct n) simp_all
haftmann@62366
  2001
haftmann@62366
  2002
lemma replicate_mset_eq_iff:
haftmann@62366
  2003
  "replicate_mset m a = replicate_mset n b \<longleftrightarrow>
haftmann@62366
  2004
    m = 0 \<and> n = 0 \<or> m = n \<and> a = b"
haftmann@62366
  2005
  by (auto simp add: multiset_eq_iff)
haftmann@62366
  2006
haftmann@60804
  2007
wenzelm@60500
  2008
subsection \<open>Big operators\<close>
haftmann@51548
  2009
haftmann@51548
  2010
locale comm_monoid_mset = comm_monoid
haftmann@51548
  2011
begin
haftmann@51548
  2012
haftmann@51548
  2013
definition F :: "'a multiset \<Rightarrow> 'a"
haftmann@63290
  2014
  where eq_fold: "F M = fold_mset f \<^bold>1 M"
haftmann@63290
  2015
haftmann@63290
  2016
lemma empty [simp]: "F {#} = \<^bold>1"
haftmann@51548
  2017
  by (simp add: eq_fold)
haftmann@51548
  2018
wenzelm@60678
  2019
lemma singleton [simp]: "F {#x#} = x"
haftmann@51548
  2020
proof -
haftmann@51548
  2021
  interpret comp_fun_commute
wenzelm@60678
  2022
    by standard (simp add: fun_eq_iff left_commute)
haftmann@51548
  2023
  show ?thesis by (simp add: eq_fold)
haftmann@51548
  2024
qed
haftmann@51548
  2025
haftmann@63290
  2026
lemma union [simp]: "F (M + N) = F M \<^bold>* F N"
haftmann@51548
  2027
proof -
haftmann@51548
  2028
  interpret comp_fun_commute f
wenzelm@60678
  2029
    by standard (simp add: fun_eq_iff left_commute)
wenzelm@60678
  2030
  show ?thesis
wenzelm@60678
  2031
    by (induct N) (simp_all add: left_commute eq_fold)
haftmann@51548
  2032
qed
haftmann@51548
  2033
Mathias@63793
  2034
lemma add_mset [simp]: "F (add_mset x N) = x \<^bold>* F N"
Mathias@63793
  2035
  unfolding add_mset_add_single[of x N] union by (simp add: ac_simps)
Mathias@63793
  2036
haftmann@51548
  2037
end
haftmann@51548
  2038
wenzelm@61076
  2039
lemma comp_fun_commute_plus_mset[simp]: "comp_fun_commute (op + :: 'a multiset \<Rightarrow> _ \<Rightarrow> _)"
wenzelm@60678
  2040
  by standard (simp add: add_ac comp_def)
blanchet@59813
  2041
Mathias@63793
  2042
declare comp_fun_commute.fold_mset_add_mset[OF comp_fun_commute_plus_mset, simp]
blanchet@59813
  2043
nipkow@59998
  2044
lemma in_mset_fold_plus_iff[iff]: "x \<in># fold_mset (op +) M NN \<longleftrightarrow> x \<in># M \<or> (\<exists>N. N \<in># NN \<and> x \<in># N)"
blanchet@59813
  2045
  by (induct NN) auto
blanchet@59813
  2046
haftmann@54868
  2047
context comm_monoid_add
haftmann@54868
  2048
begin
haftmann@54868
  2049
nipkow@63830
  2050
sublocale sum_mset: comm_monoid_mset plus 0
nipkow@63830
  2051
  defines sum_mset = sum_mset.F ..
nipkow@63830
  2052
nipkow@63830
  2053
lemma (in semiring_1) sum_mset_replicate_mset [simp]:
nipkow@63830
  2054
  "sum_mset (replicate_mset n a) = of_nat n * a"
haftmann@60804
  2055
  by (induct n) (simp_all add: algebra_simps)
haftmann@60804
  2056
nipkow@63830
  2057
lemma setsum_unfold_sum_mset:
nipkow@63830
  2058
  "setsum f A = sum_mset (image_mset f (mset_set A))"
haftmann@51548
  2059
  by (cases "finite A") (induct A rule: finite_induct, simp_all)
haftmann@51548
  2060
nipkow@63830
  2061
lemma sum_mset_delta: "sum_mset (image_mset (\<lambda>x. if x = y then c else 0) A) = c * count A y"
eberlm@63534
  2062
  by (induction A) simp_all
eberlm@63534
  2063
nipkow@63830
  2064
lemma sum_mset_delta': "sum_mset (image_mset (\<lambda>x. if y = x then c else 0) A) = c * count A y"
eberlm@63534
  2065
  by (induction A) simp_all
eberlm@63534
  2066
haftmann@51548
  2067
end
haftmann@51548
  2068
nipkow@63830
  2069
lemma sum_mset_diff:
wenzelm@61076
  2070
  fixes M N :: "('a :: ordered_cancel_comm_monoid_diff) multiset"
nipkow@63830
  2071
  shows "N \<subseteq># M \<Longrightarrow> sum_mset (M - N) = sum_mset M - sum_mset N"
nipkow@63830
  2072
  by (metis add_diff_cancel_right' sum_mset.union subset_mset.diff_add)
nipkow@63830
  2073
nipkow@63830
  2074
lemma size_eq_sum_mset: "size M = sum_mset (image_mset (\<lambda>_. 1) M)"
nipkow@59949
  2075
proof (induct M)
nipkow@59949
  2076
  case empty then show ?case by simp
nipkow@59949
  2077
next
Mathias@63793
  2078
  case (add x M) then show ?case
nipkow@60495
  2079
    by (cases "x \<in> set_mset M")
Mathias@63793
  2080
      (simp_all add: size_multiset_overloaded_eq not_in_iff setsum.If_cases Diff_eq[symmetric]
Mathias@63793
  2081
        setsum.remove)
nipkow@59949
  2082
qed
nipkow@59949
  2083
eberlm@63099
  2084
lemma size_mset_set [simp]: "size (mset_set A) = card A"
nipkow@63830
  2085
  by (simp only: size_eq_sum_mset card_eq_setsum setsum_unfold_sum_mset)
eberlm@63099
  2086
haftmann@62366
  2087
syntax (ASCII)
nipkow@63830
  2088
  "_sum_mset_image" :: "pttrn \<Rightarrow> 'b set \<Rightarrow> 'a \<Rightarrow> 'a::comm_monoid_add"  ("(3SUM _:#_. _)" [0, 51, 10] 10)
haftmann@62366
  2089
syntax
nipkow@63830
  2090
  "_sum_mset_image" :: "pttrn \<Rightarrow> 'b set \<Rightarrow> 'a \<Rightarrow> 'a::comm_monoid_add"  ("(3\<Sum>_\<in>#_. _)" [0, 51, 10] 10)
haftmann@62366
  2091
translations
nipkow@63830
  2092
  "\<Sum>i \<in># A. b" \<rightleftharpoons> "CONST sum_mset (CONST image_mset (\<lambda>i. b) A)"
nipkow@59949
  2093
wenzelm@61955
  2094
abbreviation Union_mset :: "'a multiset multiset \<Rightarrow> 'a multiset"  ("\<Union>#_" [900] 900)
nipkow@63830
  2095
  where "\<Union># MM \<equiv> sum_mset MM" \<comment> \<open>FIXME ambiguous notation --
wenzelm@62837
  2096
    could likewise refer to \<open>\<Squnion>#\<close>\<close>
blanchet@59813
  2097
nipkow@60495
  2098
lemma set_mset_Union_mset[simp]: "set_mset (\<Union># MM) = (\<Union>M \<in> set_mset MM. set_mset M)"
blanchet@59813
  2099
  by (induct MM) auto
blanchet@59813
  2100
blanchet@59813
  2101
lemma in_Union_mset_iff[iff]: "x \<in># \<Union># MM \<longleftrightarrow> (\<exists>M. M \<in># MM \<and> x \<in># M)"
blanchet@59813
  2102
  by (induct MM) auto
blanchet@59813
  2103
haftmann@62366
  2104
lemma count_setsum:
haftmann@62366
  2105
  "count (setsum f A) x = setsum (\<lambda>a. count (f a) x) A"
haftmann@62366
  2106
  by (induct A rule: infinite_finite_induct) simp_all
haftmann@62366
  2107
haftmann@62366
  2108
lemma setsum_eq_empty_iff:
haftmann@62366
  2109
  assumes "finite A"
haftmann@62366
  2110
  shows "setsum f A = {#} \<longleftrightarrow> (\<forall>a\<in>A. f a = {#})"
haftmann@62366
  2111
  using assms by induct simp_all
haftmann@51548
  2112
Mathias@63795
  2113
lemma Union_mset_empty_conv[simp]: "\<Union># M = {#} \<longleftrightarrow> (\<forall>i\<in>#M. i = {#})"
Mathias@63795
  2114
  by (induction M) auto
Mathias@63795
  2115
haftmann@54868
  2116
context comm_monoid_mult
haftmann@54868
  2117
begin
haftmann@54868
  2118
nipkow@63830
  2119
sublocale prod_mset: comm_monoid_mset times 1
nipkow@63830
  2120
  defines prod_mset = prod_mset.F ..
nipkow@63830
  2121
nipkow@63830
  2122
lemma prod_mset_empty:
nipkow@63830
  2123
  "prod_mset {#} = 1"
nipkow@63830
  2124
  by (fact prod_mset.empty)
nipkow@63830
  2125
nipkow@63830
  2126
lemma prod_mset_singleton:
nipkow@63830
  2127
  "prod_mset {#x#} = x"
nipkow@63830
  2128
  by (fact prod_mset.singleton)
nipkow@63830
  2129
nipkow@63830
  2130
lemma prod_mset_Un:
nipkow@63830
  2131
  "prod_mset (A + B) = prod_mset A * prod_mset B"
nipkow@63830
  2132
  by (fact prod_mset.union)
nipkow@63830
  2133
nipkow@63830
  2134
lemma prod_mset_replicate_mset [simp]:
nipkow@63830
  2135
  "prod_mset (replicate_mset n a) = a ^ n"
Mathias@63794
  2136
  by (induct n) simp_all
haftmann@60804
  2137
nipkow@63830
  2138
lemma setprod_unfold_prod_mset:
nipkow@63830
  2139
  "setprod f A = prod_mset (image_mset f (mset_set A))"
haftmann@51548
  2140
  by (cases "finite A") (induct A rule: finite_induct, simp_all)
haftmann@51548
  2141
nipkow@63830
  2142
lemma prod_mset_multiplicity:
nipkow@63830
  2143
  "prod_mset M = setprod (\<lambda>x. x ^ count M x) (set_mset M)"
nipkow@63830
  2144
  by (simp add: fold_mset_def setprod.eq_fold prod_mset.eq_fold funpow_times_power comp_def)
nipkow@63830
  2145
nipkow@63830
  2146
lemma prod_mset_delta: "prod_mset (image_mset (\<lambda>x. if x = y then c else 1) A) = c ^ count A y"
Mathias@63794
  2147
  by (induction A) simp_all
eberlm@63534
  2148
nipkow@63830
  2149
lemma prod_mset_delta': "prod_mset (image_mset (\<lambda>x. if y = x then c else 1) A) = c ^ count A y"
Mathias@63794
  2150
  by (induction A) simp_all
eberlm@63534
  2151
haftmann@51548
  2152
end
haftmann@51548
  2153
wenzelm@61955
  2154
syntax (ASCII)
nipkow@63830
  2155
  "_prod_mset_image" :: "pttrn \<Rightarrow> 'b set \<Rightarrow> 'a \<Rightarrow> 'a::comm_monoid_mult"  ("(3PROD _:#_. _)" [0, 51, 10] 10)
haftmann@51548
  2156
syntax
nipkow@63830
  2157
  "_prod_mset_image" :: "pttrn \<Rightarrow> 'b set \<Rightarrow> 'a \<Rightarrow> 'a::comm_monoid_mult"  ("(3\<Prod>_\<in>#_. _)" [0, 51, 10] 10)
haftmann@51548
  2158
translations
nipkow@63830
  2159
  "\<Prod>i \<in># A. b" \<rightleftharpoons> "CONST prod_mset (CONST image_mset (\<lambda>i. b) A)"
nipkow@63830
  2160
nipkow@63830
  2161
lemma (in comm_semiring_1) dvd_prod_mset:
haftmann@51548
  2162
  assumes "x \<in># A"
nipkow@63830
  2163
  shows "x dvd prod_mset A"
haftmann@51548
  2164
proof -
Mathias@63793
  2165
  from assms have "A = add_mset x (A - {#x#})" by simp
Mathias@63793
  2166
  then obtain B where "A = add_mset x B" ..
haftmann@51548
  2167
  then show ?thesis by simp
haftmann@51548
  2168
qed
haftmann@51548
  2169
nipkow@63830
  2170
lemma (in semidom) prod_mset_zero_iff [iff]:
nipkow@63830
  2171
  "prod_mset A = 0 \<longleftrightarrow> 0 \<in># A"
haftmann@62366
  2172
  by (induct A) auto
haftmann@62366
  2173
nipkow@63830
  2174
lemma (in semidom_divide) prod_mset_diff:
haftmann@62430
  2175
  assumes "B \<subseteq># A" and "0 \<notin># B"
nipkow@63830
  2176
  shows "prod_mset (A - B) = prod_mset A div prod_mset B"
haftmann@62430
  2177
proof -
haftmann@62430
  2178
  from assms obtain C where "A = B + C"
haftmann@62430
  2179
    by (metis subset_mset.add_diff_inverse)
haftmann@62430
  2180
  with assms show ?thesis by simp
haftmann@62430
  2181
qed
haftmann@62430
  2182
nipkow@63830
  2183
lemma (in semidom_divide) prod_mset_minus:
haftmann@62430
  2184
  assumes "a \<in># A" and "a \<noteq> 0"
nipkow@63830
  2185
  shows "prod_mset (A - {#a#}) = prod_mset A div a"
nipkow@63830
  2186
  using assms prod_mset_diff [of "{#a#}" A] by auto
nipkow@63830
  2187
nipkow@63830
  2188
lemma (in normalization_semidom) normalized_prod_msetI:
haftmann@62430
  2189
  assumes "\<And>a. a \<in># A \<Longrightarrow> normalize a = a"
nipkow@63830
  2190
  shows "normalize (prod_mset A) = prod_mset A"
haftmann@62430
  2191
  using assms by (induct A) (simp_all add: normalize_mult)
haftmann@62430
  2192
haftmann@51548
  2193
wenzelm@60500
  2194
subsection \<open>Alternative representations\<close>
wenzelm@60500
  2195
wenzelm@60500
  2196
subsubsection \<open>Lists\<close>
haftmann@51548
  2197
haftmann@39533
  2198
context linorder
haftmann@39533
  2199
begin
haftmann@39533
  2200
nipkow@60515
  2201
lemma mset_insort [simp]:
Mathias@63793
  2202
  "mset (insort_key k x xs) = add_mset x (mset xs)"
Mathias@63793
  2203
  by (induct xs) simp_all
blanchet@58425
  2204
nipkow@60515
  2205
lemma mset_sort [simp]:
nipkow@60515
  2206
  "mset (sort_key k xs) = mset xs"
Mathias@63794
  2207
  by (induct xs) simp_all
haftmann@37107
  2208
wenzelm@60500
  2209
text \<open>
haftmann@34943
  2210
  This lemma shows which properties suffice to show that a function
wenzelm@61585
  2211
  \<open>f\<close> with \<open>f xs = ys\<close> behaves like sort.
wenzelm@60500
  2212
\<close>
haftmann@37074
  2213
haftmann@39533
  2214
lemma properties_for_sort_key:
nipkow@60515
  2215
  assumes "mset ys = mset xs"
wenzelm@60606
  2216
    and "\<And>k. k \<in> set ys \<Longrightarrow> filter (\<lambda>x. f k = f x) ys = filter (\<lambda>x. f k = f x) xs"
wenzelm@60606
  2217
    and "sorted (map f ys)"
haftmann@39533
  2218
  shows "sort_key f xs = ys"
wenzelm@60606
  2219
  using assms
wenzelm@46921
  2220
proof (induct xs arbitrary: ys)
haftmann@34943
  2221
  case Nil then show ?case by simp
haftmann@34943
  2222
next
haftmann@34943
  2223
  case (Cons x xs)
haftmann@39533
  2224
  from Cons.prems(2) have
haftmann@40305
  2225
    "\<forall>k \<in> set ys. filter (\<lambda>x. f k = f x) (remove1 x ys) = filter (\<lambda>x. f k = f x) xs"
haftmann@39533
  2226
    by (simp add: filter_remove1)
haftmann@39533
  2227
  with Cons.prems have "sort_key f xs = remove1 x ys"
haftmann@39533
  2228
    by (auto intro!: Cons.hyps simp add: sorted_map_remove1)
haftmann@62430
  2229
  moreover from Cons.prems have "x \<in># mset ys"
haftmann@62430
  2230
    by auto
haftmann@62430
  2231
  then have "x \<in> set ys"
haftmann@62430
  2232
    by simp
haftmann@39533
  2233
  ultimately show ?case using Cons.prems by (simp add: insort_key_remove1)
haftmann@34943
  2234
qed
haftmann@34943
  2235
haftmann@39533
  2236
lemma properties_for_sort:
nipkow@60515
  2237
  assumes multiset: "mset ys = mset xs"
wenzelm@60606
  2238
    and "sorted ys"
haftmann@39533
  2239
  shows "sort xs = ys"
haftmann@39533
  2240
proof (rule properties_for_sort_key)
nipkow@60515
  2241
  from multiset show "mset ys = mset xs" .
wenzelm@60500
  2242
  from \<open>sorted ys\<close> show "sorted (map (\<lambda>x. x) ys)" by simp
wenzelm@60678
  2243
  from multiset have "length (filter (\<lambda>y. k = y) ys) = length (filter (\<lambda>x. k = x) xs)" for k
nipkow@60515
  2244
    by (rule mset_eq_length_filter)
wenzelm@60678
  2245
  then have "replicate (length (filter (\<lambda>y. k = y) ys)) k =
wenzelm@60678
  2246
    replicate (length (filter (\<lambda>x. k = x) xs)) k" for k
haftmann@39533
  2247
    by simp
wenzelm@60678
  2248
  then show "k \<in> set ys \<Longrightarrow> filter (\<lambda>y. k = y) ys = filter (\<lambda>x. k = x) xs" for k
haftmann@39533
  2249
    by (simp add: replicate_length_filter)
haftmann@39533
  2250
qed
haftmann@39533
  2251
haftmann@61031
  2252
lemma sort_key_inj_key_eq:
haftmann@61031
  2253
  assumes mset_equal: "mset xs = mset ys"
haftmann@61031
  2254
    and "inj_on f (set xs)"
haftmann@61031
  2255
    and "sorted (map f ys)"
haftmann@61031
  2256
  shows "sort_key f xs = ys"
haftmann@61031
  2257
proof (rule properties_for_sort_key)
haftmann@61031
  2258
  from mset_equal