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