src/HOL/Library/Multiset_Order.thy
author wenzelm
Wed Jun 17 11:03:05 2015 +0200 (2015-06-17)
changeset 60500 903bb1495239
parent 60397 f8a513fedb31
child 60502 aa58872267ee
permissions -rw-r--r--
isabelle update_cartouches;
blanchet@59813
     1
(*  Title:      HOL/Library/Multiset_Order.thy
blanchet@59813
     2
    Author:     Dmitriy Traytel, TU Muenchen
blanchet@59813
     3
    Author:     Jasmin Blanchette, Inria, LORIA, MPII
blanchet@59813
     4
*)
blanchet@59813
     5
wenzelm@60500
     6
section \<open>More Theorems about the Multiset Order\<close>
blanchet@59813
     7
blanchet@59813
     8
theory Multiset_Order
blanchet@59813
     9
imports Multiset
blanchet@59813
    10
begin
blanchet@59813
    11
wenzelm@60500
    12
subsubsection \<open>Alternative characterizations\<close>
blanchet@59813
    13
blanchet@59813
    14
context order
blanchet@59813
    15
begin
blanchet@59813
    16
blanchet@59813
    17
lemma reflp_le: "reflp (op \<le>)"
blanchet@59813
    18
  unfolding reflp_def by simp
blanchet@59813
    19
blanchet@59813
    20
lemma antisymP_le: "antisymP (op \<le>)"
blanchet@59813
    21
  unfolding antisym_def by auto
blanchet@59813
    22
blanchet@59813
    23
lemma transp_le: "transp (op \<le>)"
blanchet@59813
    24
  unfolding transp_def by auto
blanchet@59813
    25
blanchet@59813
    26
lemma irreflp_less: "irreflp (op <)"
blanchet@59813
    27
  unfolding irreflp_def by simp
blanchet@59813
    28
blanchet@59813
    29
lemma antisymP_less: "antisymP (op <)"
blanchet@59813
    30
  unfolding antisym_def by auto
blanchet@59813
    31
blanchet@59813
    32
lemma transp_less: "transp (op <)"
blanchet@59813
    33
  unfolding transp_def by auto
blanchet@59813
    34
blanchet@59813
    35
lemmas le_trans = transp_le[unfolded transp_def, rule_format]
blanchet@59813
    36
blanchet@59813
    37
lemma order_mult: "class.order
blanchet@59813
    38
  (\<lambda>M N. (M, N) \<in> mult {(x, y). x < y} \<or> M = N)
blanchet@59813
    39
  (\<lambda>M N. (M, N) \<in> mult {(x, y). x < y})"
blanchet@59813
    40
  (is "class.order ?le ?less")
blanchet@59813
    41
proof -
blanchet@59813
    42
  have irrefl: "\<And>M :: 'a multiset. \<not> ?less M M"
blanchet@59813
    43
  proof
blanchet@59813
    44
    fix M :: "'a multiset"
blanchet@59813
    45
    have "trans {(x'::'a, x). x' < x}"
blanchet@59813
    46
      by (rule transI) simp
blanchet@59813
    47
    moreover
blanchet@59813
    48
    assume "(M, M) \<in> mult {(x, y). x < y}"
blanchet@59813
    49
    ultimately have "\<exists>I J K. M = I + J \<and> M = I + K
blanchet@59813
    50
      \<and> J \<noteq> {#} \<and> (\<forall>k\<in>set_of K. \<exists>j\<in>set_of J. (k, j) \<in> {(x, y). x < y})"
blanchet@59813
    51
      by (rule mult_implies_one_step)
blanchet@59813
    52
    then obtain I J K where "M = I + J" and "M = I + K"
blanchet@59813
    53
      and "J \<noteq> {#}" and "(\<forall>k\<in>set_of K. \<exists>j\<in>set_of J. (k, j) \<in> {(x, y). x < y})" by blast
blanchet@59813
    54
    then have aux1: "K \<noteq> {#}" and aux2: "\<forall>k\<in>set_of K. \<exists>j\<in>set_of K. k < j" by auto
blanchet@59813
    55
    have "finite (set_of K)" by simp
blanchet@59813
    56
    moreover note aux2
blanchet@59813
    57
    ultimately have "set_of K = {}"
blanchet@59813
    58
      by (induct rule: finite_induct)
blanchet@59813
    59
       (simp, metis (mono_tags) insert_absorb insert_iff insert_not_empty less_irrefl less_trans)
blanchet@59813
    60
    with aux1 show False by simp
blanchet@59813
    61
  qed
blanchet@59813
    62
  have trans: "\<And>K M N :: 'a multiset. ?less K M \<Longrightarrow> ?less M N \<Longrightarrow> ?less K N"
blanchet@59813
    63
    unfolding mult_def by (blast intro: trancl_trans)
blanchet@59813
    64
  show "class.order ?le ?less"
blanchet@59813
    65
    by default (auto simp add: le_multiset_def irrefl dest: trans)
blanchet@59813
    66
qed
blanchet@59813
    67
wenzelm@60500
    68
text \<open>The Dershowitz--Manna ordering:\<close>
blanchet@59813
    69
blanchet@59813
    70
definition less_multiset\<^sub>D\<^sub>M where
blanchet@59813
    71
  "less_multiset\<^sub>D\<^sub>M M N \<longleftrightarrow>
Mathias@60397
    72
   (\<exists>X Y. X \<noteq> {#} \<and> X \<le># N \<and> M = (N - X) + Y \<and> (\<forall>k. k \<in># Y \<longrightarrow> (\<exists>a. a \<in># X \<and> k < a)))"
blanchet@59813
    73
blanchet@59813
    74
wenzelm@60500
    75
text \<open>The Huet--Oppen ordering:\<close>
blanchet@59813
    76
blanchet@59813
    77
definition less_multiset\<^sub>H\<^sub>O where
blanchet@59813
    78
  "less_multiset\<^sub>H\<^sub>O M N \<longleftrightarrow> M \<noteq> N \<and> (\<forall>y. count N y < count M y \<longrightarrow> (\<exists>x. y < x \<and> count M x < count N x))"
blanchet@59813
    79
blanchet@59813
    80
lemma mult_imp_less_multiset\<^sub>H\<^sub>O: "(M, N) \<in> mult {(x, y). x < y} \<Longrightarrow> less_multiset\<^sub>H\<^sub>O M N"
blanchet@59813
    81
proof (unfold mult_def less_multiset\<^sub>H\<^sub>O_def, induct rule: trancl_induct)
blanchet@59813
    82
  case (base P)
blanchet@59813
    83
  then show ?case unfolding mult1_def by force
blanchet@59813
    84
next
blanchet@59813
    85
  case (step N P)
blanchet@59813
    86
  from step(2) obtain M0 a K where
blanchet@59813
    87
    *: "P = M0 + {#a#}" "N = M0 + K" "\<And>b. b \<in># K \<Longrightarrow> b < a"
blanchet@59813
    88
    unfolding mult1_def by blast
blanchet@59813
    89
  then have count_K_a: "count K a = 0" by auto
blanchet@59813
    90
  with step(3) *(1,2) have "M \<noteq> P" by (force dest: *(3) split: if_splits)
blanchet@59813
    91
  moreover
blanchet@59813
    92
  { assume "count P a \<le> count M a"
blanchet@59813
    93
    with count_K_a have "count N a < count M a" unfolding *(1,2) by auto
blanchet@59813
    94
      with step(3) obtain z where z: "z > a" "count M z < count N z" by blast
blanchet@59813
    95
      with * have "count N z \<le> count P z" by force
blanchet@59813
    96
      with z have "\<exists>z > a. count M z < count P z" by auto
blanchet@59813
    97
  } note count_a = this
blanchet@59813
    98
  { fix y
blanchet@59813
    99
    assume count_y: "count P y < count M y"
blanchet@59813
   100
    have "\<exists>x>y. count M x < count P x"
blanchet@59813
   101
    proof (cases "y = a")
blanchet@59813
   102
      case True
blanchet@59813
   103
      with count_y count_a show ?thesis by auto
blanchet@59813
   104
    next
blanchet@59813
   105
      case False
blanchet@59813
   106
      show ?thesis
blanchet@59813
   107
      proof (cases "y \<in># K")
blanchet@59813
   108
        case True
blanchet@59813
   109
        with *(3) have "y < a" by simp
blanchet@59813
   110
        then show ?thesis by (cases "count P a \<le> count M a") (auto dest: count_a intro: less_trans)
blanchet@59813
   111
      next
blanchet@59813
   112
        case False
wenzelm@60500
   113
        with \<open>y \<noteq> a\<close> have "count P y = count N y" unfolding *(1,2) by simp
blanchet@59813
   114
        with count_y step(3) obtain z where z: "z > y" "count M z < count N z" by auto
blanchet@59813
   115
        show ?thesis
blanchet@59813
   116
        proof (cases "z \<in># K")
blanchet@59813
   117
          case True
blanchet@59813
   118
          with *(3) have "z < a" by simp
blanchet@59813
   119
          with z(1) show ?thesis
blanchet@59813
   120
            by (cases "count P a \<le> count M a") (auto dest!: count_a intro: less_trans)
blanchet@59813
   121
        next
blanchet@59813
   122
          case False
blanchet@59813
   123
          with count_K_a have "count N z \<le> count P z" unfolding * by auto
blanchet@59813
   124
          with z show ?thesis by auto
blanchet@59813
   125
        qed
blanchet@59813
   126
      qed
blanchet@59813
   127
    qed
blanchet@59813
   128
  }
blanchet@59813
   129
  ultimately show ?case by blast
blanchet@59813
   130
qed
blanchet@59813
   131
blanchet@59813
   132
lemma less_multiset\<^sub>D\<^sub>M_imp_mult:
blanchet@59813
   133
  "less_multiset\<^sub>D\<^sub>M M N \<Longrightarrow> (M, N) \<in> mult {(x, y). x < y}"
blanchet@59813
   134
proof -
blanchet@59813
   135
  assume "less_multiset\<^sub>D\<^sub>M M N"
blanchet@59813
   136
  then obtain X Y where
Mathias@60397
   137
    "X \<noteq> {#}" and "X \<le># N" and "M = N - X + Y" and "\<forall>k. k \<in># Y \<longrightarrow> (\<exists>a. a \<in># X \<and> k < a)"
blanchet@59813
   138
    unfolding less_multiset\<^sub>D\<^sub>M_def by blast
blanchet@59813
   139
  then have "(N - X + Y, N - X + X) \<in> mult {(x, y). x < y}"
blanchet@59813
   140
    by (intro one_step_implies_mult) (auto simp: Bex_def trans_def)
wenzelm@60500
   141
  with \<open>M = N - X + Y\<close> \<open>X \<le># N\<close> show "(M, N) \<in> mult {(x, y). x < y}"
Mathias@60397
   142
    by (metis subset_mset.diff_add)
blanchet@59813
   143
qed
blanchet@59813
   144
blanchet@59813
   145
lemma less_multiset\<^sub>H\<^sub>O_imp_less_multiset\<^sub>D\<^sub>M: "less_multiset\<^sub>H\<^sub>O M N \<Longrightarrow> less_multiset\<^sub>D\<^sub>M M N"
blanchet@59813
   146
unfolding less_multiset\<^sub>D\<^sub>M_def
blanchet@59813
   147
proof (intro iffI exI conjI)
blanchet@59813
   148
  assume "less_multiset\<^sub>H\<^sub>O M N"
blanchet@59813
   149
  then obtain z where z: "count M z < count N z"
blanchet@59813
   150
    unfolding less_multiset\<^sub>H\<^sub>O_def by (auto simp: multiset_eq_iff nat_neq_iff)
blanchet@59813
   151
  def X \<equiv> "N - M"
blanchet@59813
   152
  def Y \<equiv> "M - N"
blanchet@59813
   153
  from z show "X \<noteq> {#}" unfolding X_def by (auto simp: multiset_eq_iff not_less_eq_eq Suc_le_eq)
Mathias@60397
   154
  from z show "X \<le># N" unfolding X_def by auto
blanchet@59813
   155
  show "M = (N - X) + Y" unfolding X_def Y_def multiset_eq_iff count_union count_diff by force
blanchet@59813
   156
  show "\<forall>k. k \<in># Y \<longrightarrow> (\<exists>a. a \<in># X \<and> k < a)"
blanchet@59813
   157
  proof (intro allI impI)
blanchet@59813
   158
    fix k
blanchet@59813
   159
    assume "k \<in># Y"
blanchet@59813
   160
    then have "count N k < count M k" unfolding Y_def by auto
wenzelm@60500
   161
    with \<open>less_multiset\<^sub>H\<^sub>O M N\<close> obtain a where "k < a" and "count M a < count N a"
blanchet@59813
   162
      unfolding less_multiset\<^sub>H\<^sub>O_def by blast
blanchet@59813
   163
    then show "\<exists>a. a \<in># X \<and> k < a" unfolding X_def by auto
blanchet@59813
   164
  qed
blanchet@59813
   165
qed
blanchet@59813
   166
blanchet@59813
   167
lemma mult_less_multiset\<^sub>D\<^sub>M: "(M, N) \<in> mult {(x, y). x < y} \<longleftrightarrow> less_multiset\<^sub>D\<^sub>M M N"
blanchet@59813
   168
  by (metis less_multiset\<^sub>D\<^sub>M_imp_mult less_multiset\<^sub>H\<^sub>O_imp_less_multiset\<^sub>D\<^sub>M mult_imp_less_multiset\<^sub>H\<^sub>O)
blanchet@59813
   169
blanchet@59813
   170
lemma mult_less_multiset\<^sub>H\<^sub>O: "(M, N) \<in> mult {(x, y). x < y} \<longleftrightarrow> less_multiset\<^sub>H\<^sub>O M N"
blanchet@59813
   171
  by (metis less_multiset\<^sub>D\<^sub>M_imp_mult less_multiset\<^sub>H\<^sub>O_imp_less_multiset\<^sub>D\<^sub>M mult_imp_less_multiset\<^sub>H\<^sub>O)
blanchet@59813
   172
blanchet@59813
   173
lemmas mult\<^sub>D\<^sub>M = mult_less_multiset\<^sub>D\<^sub>M[unfolded less_multiset\<^sub>D\<^sub>M_def]
blanchet@59813
   174
lemmas mult\<^sub>H\<^sub>O = mult_less_multiset\<^sub>H\<^sub>O[unfolded less_multiset\<^sub>H\<^sub>O_def]
blanchet@59813
   175
blanchet@59813
   176
end
blanchet@59813
   177
blanchet@59813
   178
context linorder
blanchet@59813
   179
begin
blanchet@59813
   180
blanchet@59813
   181
lemma total_le: "total {(a \<Colon> 'a, b). a \<le> b}"
blanchet@59813
   182
  unfolding total_on_def by auto
blanchet@59813
   183
blanchet@59813
   184
lemma total_less: "total {(a \<Colon> 'a, b). a < b}"
blanchet@59813
   185
  unfolding total_on_def by auto
blanchet@59813
   186
blanchet@59813
   187
lemma linorder_mult: "class.linorder
blanchet@59813
   188
  (\<lambda>M N. (M, N) \<in> mult {(x, y). x < y} \<or> M = N)
blanchet@59813
   189
  (\<lambda>M N. (M, N) \<in> mult {(x, y). x < y})"
blanchet@59813
   190
proof -
blanchet@59813
   191
  interpret o: order
blanchet@59813
   192
    "(\<lambda>M N. (M, N) \<in> mult {(x, y). x < y} \<or> M = N)"
blanchet@59813
   193
    "(\<lambda>M N. (M, N) \<in> mult {(x, y). x < y})"
blanchet@59813
   194
    by (rule order_mult)
blanchet@59813
   195
  show ?thesis by unfold_locales (auto 0 3 simp: mult\<^sub>H\<^sub>O not_less_iff_gr_or_eq)
blanchet@59813
   196
qed
blanchet@59813
   197
blanchet@59813
   198
end
blanchet@59813
   199
blanchet@59813
   200
lemma less_multiset_less_multiset\<^sub>H\<^sub>O:
blanchet@59958
   201
  "M #\<subset># N \<longleftrightarrow> less_multiset\<^sub>H\<^sub>O M N"
blanchet@59813
   202
  unfolding less_multiset_def mult\<^sub>H\<^sub>O less_multiset\<^sub>H\<^sub>O_def ..
blanchet@59813
   203
blanchet@59813
   204
lemmas less_multiset\<^sub>D\<^sub>M = mult\<^sub>D\<^sub>M[folded less_multiset_def]
blanchet@59813
   205
lemmas less_multiset\<^sub>H\<^sub>O = mult\<^sub>H\<^sub>O[folded less_multiset_def]
blanchet@59813
   206
blanchet@59813
   207
lemma le_multiset\<^sub>H\<^sub>O:
blanchet@59813
   208
  fixes M N :: "('a \<Colon> linorder) multiset"
blanchet@59958
   209
  shows "M #\<subseteq># N \<longleftrightarrow> (\<forall>y. count N y < count M y \<longrightarrow> (\<exists>x. y < x \<and> count M x < count N x))"
blanchet@59813
   210
  by (auto simp: le_multiset_def less_multiset\<^sub>H\<^sub>O)
blanchet@59813
   211
blanchet@59958
   212
lemma wf_less_multiset: "wf {(M \<Colon> ('a \<Colon> wellorder) multiset, N). M #\<subset># N}"
blanchet@59813
   213
  unfolding less_multiset_def by (auto intro: wf_mult wf)
blanchet@59813
   214
blanchet@59813
   215
lemma order_multiset: "class.order
blanchet@59813
   216
  (le_multiset :: ('a \<Colon> order) multiset \<Rightarrow> ('a \<Colon> order) multiset \<Rightarrow> bool)
blanchet@59813
   217
  (less_multiset :: ('a \<Colon> order) multiset \<Rightarrow> ('a \<Colon> order) multiset \<Rightarrow> bool)"
blanchet@59813
   218
  by unfold_locales
blanchet@59813
   219
blanchet@59813
   220
lemma linorder_multiset: "class.linorder
blanchet@59813
   221
  (le_multiset :: ('a \<Colon> linorder) multiset \<Rightarrow> ('a \<Colon> linorder) multiset \<Rightarrow> bool)
blanchet@59813
   222
  (less_multiset :: ('a \<Colon> linorder) multiset \<Rightarrow> ('a \<Colon> linorder) multiset \<Rightarrow> bool)"
blanchet@59813
   223
  by unfold_locales (fastforce simp add: less_multiset\<^sub>H\<^sub>O le_multiset_def not_less_iff_gr_or_eq)
blanchet@59813
   224
blanchet@59813
   225
interpretation multiset_linorder: linorder
blanchet@59813
   226
  "le_multiset :: ('a \<Colon> linorder) multiset \<Rightarrow> ('a \<Colon> linorder) multiset \<Rightarrow> bool"
blanchet@59813
   227
  "less_multiset :: ('a \<Colon> linorder) multiset \<Rightarrow> ('a \<Colon> linorder) multiset \<Rightarrow> bool"
blanchet@59813
   228
  by (rule linorder_multiset)
blanchet@59813
   229
blanchet@59813
   230
interpretation multiset_wellorder: wellorder
blanchet@59813
   231
  "le_multiset :: ('a \<Colon> wellorder) multiset \<Rightarrow> ('a \<Colon> wellorder) multiset \<Rightarrow> bool"
blanchet@59813
   232
  "less_multiset :: ('a \<Colon> wellorder) multiset \<Rightarrow> ('a \<Colon> wellorder) multiset \<Rightarrow> bool"
blanchet@59813
   233
  by unfold_locales (blast intro: wf_less_multiset[unfolded wf_def, rule_format])
blanchet@59813
   234
blanchet@59813
   235
lemma le_multiset_total:
blanchet@59813
   236
  fixes M N :: "('a \<Colon> linorder) multiset"
blanchet@59958
   237
  shows "\<not> M #\<subseteq># N \<Longrightarrow> N #\<subseteq># M"
blanchet@59813
   238
  by (metis multiset_linorder.le_cases)
blanchet@59813
   239
blanchet@59813
   240
lemma less_eq_imp_le_multiset:
blanchet@59813
   241
  fixes M N :: "('a \<Colon> linorder) multiset"
Mathias@60397
   242
  shows "M \<le># N \<Longrightarrow> M #\<subseteq># N"
blanchet@59813
   243
  unfolding le_multiset_def less_multiset\<^sub>H\<^sub>O
Mathias@60397
   244
  by (simp add: less_le_not_le subseteq_mset_def)
blanchet@59813
   245
blanchet@59813
   246
lemma less_multiset_right_total:
blanchet@59813
   247
  fixes M :: "('a \<Colon> linorder) multiset"
blanchet@59958
   248
  shows "M #\<subset># M + {#undefined#}"
blanchet@59813
   249
  unfolding le_multiset_def less_multiset\<^sub>H\<^sub>O by simp
blanchet@59813
   250
blanchet@59813
   251
lemma le_multiset_empty_left[simp]:
blanchet@59813
   252
  fixes M :: "('a \<Colon> linorder) multiset"
blanchet@59958
   253
  shows "{#} #\<subseteq># M"
blanchet@59813
   254
  by (simp add: less_eq_imp_le_multiset)
blanchet@59813
   255
blanchet@59813
   256
lemma le_multiset_empty_right[simp]:
blanchet@59813
   257
  fixes M :: "('a \<Colon> linorder) multiset"
blanchet@59958
   258
  shows "M \<noteq> {#} \<Longrightarrow> \<not> M #\<subseteq># {#}"
blanchet@59813
   259
  by (metis le_multiset_empty_left multiset_order.antisym)
blanchet@59813
   260
blanchet@59813
   261
lemma less_multiset_empty_left[simp]:
blanchet@59813
   262
  fixes M :: "('a \<Colon> linorder) multiset"
blanchet@59958
   263
  shows "M \<noteq> {#} \<Longrightarrow> {#} #\<subset># M"
blanchet@59813
   264
  by (simp add: less_multiset\<^sub>H\<^sub>O)
blanchet@59813
   265
blanchet@59813
   266
lemma less_multiset_empty_right[simp]:
blanchet@59813
   267
  fixes M :: "('a \<Colon> linorder) multiset"
blanchet@59958
   268
  shows "\<not> M #\<subset># {#}"
blanchet@59813
   269
  using le_empty less_multiset\<^sub>D\<^sub>M by blast
blanchet@59813
   270
blanchet@59813
   271
lemma
blanchet@59813
   272
  fixes M N :: "('a \<Colon> linorder) multiset"
blanchet@59813
   273
  shows
blanchet@59958
   274
    le_multiset_plus_left[simp]: "N #\<subseteq># (M + N)" and
blanchet@59958
   275
    le_multiset_plus_right[simp]: "M #\<subseteq># (M + N)"
blanchet@59813
   276
  using [[metis_verbose = false]] by (metis less_eq_imp_le_multiset mset_le_add_left add.commute)+
blanchet@59813
   277
blanchet@59813
   278
lemma
blanchet@59813
   279
  fixes M N :: "('a \<Colon> linorder) multiset"
blanchet@59813
   280
  shows
blanchet@59958
   281
    less_multiset_plus_plus_left_iff[simp]: "M + N #\<subset># M' + N \<longleftrightarrow> M #\<subset># M'" and
blanchet@59958
   282
    less_multiset_plus_plus_right_iff[simp]: "M + N #\<subset># M + N' \<longleftrightarrow> N #\<subset># N'"
blanchet@59813
   283
  unfolding less_multiset\<^sub>H\<^sub>O by auto
blanchet@59813
   284
blanchet@59813
   285
lemma add_eq_self_empty_iff: "M + N = M \<longleftrightarrow> N = {#}"
blanchet@59813
   286
  by (metis add.commute add_diff_cancel_right' monoid_add_class.add.left_neutral)
blanchet@59813
   287
blanchet@59813
   288
lemma
blanchet@59813
   289
  fixes M N :: "('a \<Colon> linorder) multiset"
blanchet@59813
   290
  shows
blanchet@59958
   291
    less_multiset_plus_left_nonempty[simp]: "M \<noteq> {#} \<Longrightarrow> N #\<subset># M + N" and
blanchet@59958
   292
    less_multiset_plus_right_nonempty[simp]: "N \<noteq> {#} \<Longrightarrow> M #\<subset># M + N"
blanchet@59813
   293
  using [[metis_verbose = false]]
blanchet@59813
   294
  by (metis add.right_neutral less_multiset_empty_left less_multiset_plus_plus_right_iff
blanchet@59813
   295
    add.commute)+
blanchet@59813
   296
blanchet@59958
   297
lemma ex_gt_imp_less_multiset: "(\<exists>y \<Colon> 'a \<Colon> linorder. y \<in># N \<and> (\<forall>x. x \<in># M \<longrightarrow> x < y)) \<Longrightarrow> M #\<subset># N"
blanchet@59813
   298
  unfolding less_multiset\<^sub>H\<^sub>O by (metis less_irrefl less_nat_zero_code not_gr0)
blanchet@59813
   299
blanchet@59813
   300
lemma ex_gt_count_imp_less_multiset:
blanchet@59958
   301
  "(\<forall>y \<Colon> 'a \<Colon> linorder. y \<in># M + N \<longrightarrow> y \<le> x) \<Longrightarrow> count M x < count N x \<Longrightarrow> M #\<subset># N"
haftmann@59817
   302
  unfolding less_multiset\<^sub>H\<^sub>O by (metis add.left_neutral add_lessD1 dual_order.strict_iff_order
haftmann@59817
   303
    less_not_sym mset_leD mset_le_add_left)  
blanchet@59813
   304
Mathias@60397
   305
lemma union_less_diff_plus: "P \<le># M \<Longrightarrow> N #\<subset># P \<Longrightarrow> M - P + N #\<subset># M"
Mathias@60397
   306
  by (drule subset_mset.diff_add[symmetric]) (metis union_less_mono2)
blanchet@59813
   307
blanchet@59813
   308
end