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