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