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