src/HOL/Library/Multiset_Order.thy
author wenzelm
Sat Nov 04 15:24:40 2017 +0100 (21 months ago)
changeset 67003 49850a679c2c
parent 65546 7c58f69451b0
child 67020 c32254ab1901
permissions -rw-r--r--
more robust sorted_entries;
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
blanchet@65546
    12
subsection \<open>Alternative Characterizations\<close>
blanchet@59813
    13
Mathias@63410
    14
context preorder
blanchet@59813
    15
begin
blanchet@59813
    16
blanchet@59813
    17
lemma order_mult: "class.order
blanchet@59813
    18
  (\<lambda>M N. (M, N) \<in> mult {(x, y). x < y} \<or> M = N)
blanchet@59813
    19
  (\<lambda>M N. (M, N) \<in> mult {(x, y). x < y})"
blanchet@59813
    20
  (is "class.order ?le ?less")
blanchet@59813
    21
proof -
blanchet@59813
    22
  have irrefl: "\<And>M :: 'a multiset. \<not> ?less M M"
blanchet@59813
    23
  proof
blanchet@59813
    24
    fix M :: "'a multiset"
blanchet@59813
    25
    have "trans {(x'::'a, x). x' < x}"
Mathias@63410
    26
      by (rule transI) (blast intro: less_trans)
blanchet@59813
    27
    moreover
blanchet@59813
    28
    assume "(M, M) \<in> mult {(x, y). x < y}"
blanchet@59813
    29
    ultimately have "\<exists>I J K. M = I + J \<and> M = I + K
nipkow@60495
    30
      \<and> J \<noteq> {#} \<and> (\<forall>k\<in>set_mset K. \<exists>j\<in>set_mset J. (k, j) \<in> {(x, y). x < y})"
blanchet@59813
    31
      by (rule mult_implies_one_step)
blanchet@59813
    32
    then obtain I J K where "M = I + J" and "M = I + K"
nipkow@60495
    33
      and "J \<noteq> {#}" and "(\<forall>k\<in>set_mset K. \<exists>j\<in>set_mset J. (k, j) \<in> {(x, y). x < y})" by blast
nipkow@60495
    34
    then have aux1: "K \<noteq> {#}" and aux2: "\<forall>k\<in>set_mset K. \<exists>j\<in>set_mset K. k < j" by auto
nipkow@60495
    35
    have "finite (set_mset K)" by simp
blanchet@59813
    36
    moreover note aux2
nipkow@60495
    37
    ultimately have "set_mset K = {}"
blanchet@59813
    38
      by (induct rule: finite_induct)
blanchet@59813
    39
       (simp, metis (mono_tags) insert_absorb insert_iff insert_not_empty less_irrefl less_trans)
blanchet@59813
    40
    with aux1 show False by simp
blanchet@59813
    41
  qed
blanchet@59813
    42
  have trans: "\<And>K M N :: 'a multiset. ?less K M \<Longrightarrow> ?less M N \<Longrightarrow> ?less K N"
blanchet@59813
    43
    unfolding mult_def by (blast intro: trancl_trans)
blanchet@59813
    44
  show "class.order ?le ?less"
Mathias@63388
    45
    by standard (auto simp add: less_eq_multiset_def irrefl dest: trans)
blanchet@59813
    46
qed
blanchet@59813
    47
wenzelm@60500
    48
text \<open>The Dershowitz--Manna ordering:\<close>
blanchet@59813
    49
blanchet@59813
    50
definition less_multiset\<^sub>D\<^sub>M where
blanchet@59813
    51
  "less_multiset\<^sub>D\<^sub>M M N \<longleftrightarrow>
haftmann@64587
    52
   (\<exists>X Y. X \<noteq> {#} \<and> X \<subseteq># N \<and> M = (N - X) + Y \<and> (\<forall>k. k \<in># Y \<longrightarrow> (\<exists>a. a \<in># X \<and> k < a)))"
blanchet@59813
    53
blanchet@59813
    54
wenzelm@60500
    55
text \<open>The Huet--Oppen ordering:\<close>
blanchet@59813
    56
blanchet@59813
    57
definition less_multiset\<^sub>H\<^sub>O where
blanchet@59813
    58
  "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
    59
haftmann@62430
    60
lemma mult_imp_less_multiset\<^sub>H\<^sub>O:
haftmann@62430
    61
  "(M, N) \<in> mult {(x, y). x < y} \<Longrightarrow> less_multiset\<^sub>H\<^sub>O M N"
haftmann@62430
    62
proof (unfold mult_def, induct rule: trancl_induct)
blanchet@59813
    63
  case (base P)
haftmann@62430
    64
  then show ?case
haftmann@62430
    65
    by (auto elim!: mult1_lessE simp add: count_eq_zero_iff less_multiset\<^sub>H\<^sub>O_def split: if_splits dest!: Suc_lessD)
blanchet@59813
    66
next
blanchet@59813
    67
  case (step N P)
haftmann@62430
    68
  from step(3) have "M \<noteq> N" and
haftmann@62430
    69
    **: "\<And>y. count N y < count M y \<Longrightarrow> (\<exists>x>y. count M x < count N x)"
haftmann@62430
    70
    by (simp_all add: less_multiset\<^sub>H\<^sub>O_def)
blanchet@59813
    71
  from step(2) obtain M0 a K where
Mathias@63793
    72
    *: "P = add_mset a M0" "N = M0 + K" "a \<notin># K" "\<And>b. b \<in># K \<Longrightarrow> b < a"
haftmann@62430
    73
    by (blast elim: mult1_lessE)
Mathias@63410
    74
  from \<open>M \<noteq> N\<close> ** *(1,2,3) have "M \<noteq> P" by (force dest: *(4) elim!: less_asym split: if_splits )
blanchet@59813
    75
  moreover
blanchet@59813
    76
  { assume "count P a \<le> count M a"
haftmann@62430
    77
    with \<open>a \<notin># K\<close> have "count N a < count M a" unfolding *(1,2)
haftmann@62430
    78
      by (auto simp add: not_in_iff)
haftmann@62430
    79
      with ** obtain z where z: "z > a" "count M z < count N z"
haftmann@62430
    80
        by blast
haftmann@62430
    81
      with * have "count N z \<le> count P z" 
Mathias@63410
    82
        by (auto elim: less_asym intro: count_inI)
blanchet@59813
    83
      with z have "\<exists>z > a. count M z < count P z" by auto
blanchet@59813
    84
  } note count_a = this
blanchet@59813
    85
  { fix y
blanchet@59813
    86
    assume count_y: "count P y < count M y"
blanchet@59813
    87
    have "\<exists>x>y. count M x < count P x"
blanchet@59813
    88
    proof (cases "y = a")
blanchet@59813
    89
      case True
blanchet@59813
    90
      with count_y count_a show ?thesis by auto
blanchet@59813
    91
    next
blanchet@59813
    92
      case False
blanchet@59813
    93
      show ?thesis
blanchet@59813
    94
      proof (cases "y \<in># K")
blanchet@59813
    95
        case True
haftmann@62430
    96
        with *(4) have "y < a" by simp
blanchet@59813
    97
        then show ?thesis by (cases "count P a \<le> count M a") (auto dest: count_a intro: less_trans)
blanchet@59813
    98
      next
blanchet@59813
    99
        case False
haftmann@62430
   100
        with \<open>y \<noteq> a\<close> have "count P y = count N y" unfolding *(1,2)
haftmann@62430
   101
          by (simp add: not_in_iff)
haftmann@62430
   102
        with count_y ** obtain z where z: "z > y" "count M z < count N z" by auto
blanchet@59813
   103
        show ?thesis
blanchet@59813
   104
        proof (cases "z \<in># K")
blanchet@59813
   105
          case True
haftmann@62430
   106
          with *(4) have "z < a" by simp
blanchet@59813
   107
          with z(1) show ?thesis
blanchet@59813
   108
            by (cases "count P a \<le> count M a") (auto dest!: count_a intro: less_trans)
blanchet@59813
   109
        next
blanchet@59813
   110
          case False
haftmann@62430
   111
          with \<open>a \<notin># K\<close> have "count N z \<le> count P z" unfolding *
haftmann@62430
   112
            by (auto simp add: not_in_iff)
blanchet@59813
   113
          with z show ?thesis by auto
blanchet@59813
   114
        qed
blanchet@59813
   115
      qed
blanchet@59813
   116
    qed
blanchet@59813
   117
  }
haftmann@62430
   118
  ultimately show ?case unfolding less_multiset\<^sub>H\<^sub>O_def by blast
blanchet@59813
   119
qed
blanchet@59813
   120
blanchet@59813
   121
lemma less_multiset\<^sub>D\<^sub>M_imp_mult:
blanchet@59813
   122
  "less_multiset\<^sub>D\<^sub>M M N \<Longrightarrow> (M, N) \<in> mult {(x, y). x < y}"
blanchet@59813
   123
proof -
blanchet@59813
   124
  assume "less_multiset\<^sub>D\<^sub>M M N"
blanchet@59813
   125
  then obtain X Y where
haftmann@64587
   126
    "X \<noteq> {#}" and "X \<subseteq># N" and "M = N - X + Y" and "\<forall>k. k \<in># Y \<longrightarrow> (\<exists>a. a \<in># X \<and> k < a)"
blanchet@59813
   127
    unfolding less_multiset\<^sub>D\<^sub>M_def by blast
blanchet@59813
   128
  then have "(N - X + Y, N - X + X) \<in> mult {(x, y). x < y}"
blanchet@59813
   129
    by (intro one_step_implies_mult) (auto simp: Bex_def trans_def)
haftmann@64587
   130
  with \<open>M = N - X + Y\<close> \<open>X \<subseteq># N\<close> show "(M, N) \<in> mult {(x, y). x < y}"
Mathias@60397
   131
    by (metis subset_mset.diff_add)
blanchet@59813
   132
qed
blanchet@59813
   133
blanchet@59813
   134
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
   135
unfolding less_multiset\<^sub>D\<^sub>M_def
blanchet@59813
   136
proof (intro iffI exI conjI)
blanchet@59813
   137
  assume "less_multiset\<^sub>H\<^sub>O M N"
blanchet@59813
   138
  then obtain z where z: "count M z < count N z"
blanchet@59813
   139
    unfolding less_multiset\<^sub>H\<^sub>O_def by (auto simp: multiset_eq_iff nat_neq_iff)
wenzelm@63040
   140
  define X where "X = N - M"
wenzelm@63040
   141
  define Y where "Y = M - N"
blanchet@59813
   142
  from z show "X \<noteq> {#}" unfolding X_def by (auto simp: multiset_eq_iff not_less_eq_eq Suc_le_eq)
haftmann@64587
   143
  from z show "X \<subseteq># N" unfolding X_def by auto
blanchet@59813
   144
  show "M = (N - X) + Y" unfolding X_def Y_def multiset_eq_iff count_union count_diff by force
blanchet@59813
   145
  show "\<forall>k. k \<in># Y \<longrightarrow> (\<exists>a. a \<in># X \<and> k < a)"
blanchet@59813
   146
  proof (intro allI impI)
blanchet@59813
   147
    fix k
blanchet@59813
   148
    assume "k \<in># Y"
haftmann@62430
   149
    then have "count N k < count M k" unfolding Y_def
haftmann@62430
   150
      by (auto simp add: in_diff_count)
wenzelm@60500
   151
    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
   152
      unfolding less_multiset\<^sub>H\<^sub>O_def by blast
haftmann@62430
   153
    then show "\<exists>a. a \<in># X \<and> k < a" unfolding X_def
haftmann@62430
   154
      by (auto simp add: in_diff_count)
blanchet@59813
   155
  qed
blanchet@59813
   156
qed
blanchet@59813
   157
blanchet@59813
   158
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
   159
  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
   160
blanchet@59813
   161
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
   162
  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
   163
blanchet@59813
   164
lemmas mult\<^sub>D\<^sub>M = mult_less_multiset\<^sub>D\<^sub>M[unfolded less_multiset\<^sub>D\<^sub>M_def]
blanchet@59813
   165
lemmas mult\<^sub>H\<^sub>O = mult_less_multiset\<^sub>H\<^sub>O[unfolded less_multiset\<^sub>H\<^sub>O_def]
blanchet@59813
   166
blanchet@59813
   167
end
blanchet@59813
   168
blanchet@59813
   169
lemma less_multiset_less_multiset\<^sub>H\<^sub>O:
Mathias@63388
   170
  "M < N \<longleftrightarrow> less_multiset\<^sub>H\<^sub>O M N"
blanchet@59813
   171
  unfolding less_multiset_def mult\<^sub>H\<^sub>O less_multiset\<^sub>H\<^sub>O_def ..
blanchet@59813
   172
blanchet@59813
   173
lemmas less_multiset\<^sub>D\<^sub>M = mult\<^sub>D\<^sub>M[folded less_multiset_def]
blanchet@59813
   174
lemmas less_multiset\<^sub>H\<^sub>O = mult\<^sub>H\<^sub>O[folded less_multiset_def]
blanchet@59813
   175
Mathias@63388
   176
lemma subset_eq_imp_le_multiset:
haftmann@64587
   177
  shows "M \<subseteq># N \<Longrightarrow> M \<le> N"
Mathias@63388
   178
  unfolding less_eq_multiset_def less_multiset\<^sub>H\<^sub>O
Mathias@60397
   179
  by (simp add: less_le_not_le subseteq_mset_def)
blanchet@59813
   180
Mathias@63388
   181
lemma le_multiset_right_total:
Mathias@63793
   182
  shows "M < add_mset x M"
Mathias@63388
   183
  unfolding less_eq_multiset_def less_multiset\<^sub>H\<^sub>O by simp
Mathias@63388
   184
Mathias@63388
   185
lemma less_eq_multiset_empty_left[simp]:
Mathias@63388
   186
  shows "{#} \<le> M"
Mathias@63388
   187
  by (simp add: subset_eq_imp_le_multiset)
Mathias@63388
   188
blanchet@63409
   189
lemma ex_gt_imp_less_multiset: "(\<exists>y. y \<in># N \<and> (\<forall>x. x \<in># M \<longrightarrow> x < y)) \<Longrightarrow> M < N"
blanchet@63409
   190
  unfolding less_multiset\<^sub>H\<^sub>O
blanchet@63409
   191
  by (metis count_eq_zero_iff count_greater_zero_iff less_le_not_le)
blanchet@63409
   192
Mathias@63388
   193
lemma less_eq_multiset_empty_right[simp]:
blanchet@63409
   194
  "M \<noteq> {#} \<Longrightarrow> \<not> M \<le> {#}"
Mathias@63388
   195
  by (metis less_eq_multiset_empty_left antisym)
blanchet@59813
   196
blanchet@63409
   197
lemma le_multiset_empty_left[simp]: "M \<noteq> {#} \<Longrightarrow> {#} < M"
Mathias@63388
   198
  by (simp add: less_multiset\<^sub>H\<^sub>O)
blanchet@59813
   199
blanchet@63409
   200
lemma le_multiset_empty_right[simp]: "\<not> M < {#}"
Mathias@64076
   201
  using subset_mset.le_zero_eq less_multiset\<^sub>D\<^sub>M by blast
blanchet@59813
   202
haftmann@64587
   203
lemma union_le_diff_plus: "P \<subseteq># M \<Longrightarrow> N < P \<Longrightarrow> M - P + N < M"
blanchet@63409
   204
  by (drule subset_mset.diff_add[symmetric]) (metis union_le_mono2)
blanchet@63409
   205
Mathias@63525
   206
instantiation multiset :: (preorder) ordered_ab_semigroup_monoid_add_imp_le
blanchet@63409
   207
begin
blanchet@63409
   208
blanchet@63409
   209
lemma less_eq_multiset\<^sub>H\<^sub>O:
blanchet@63409
   210
  "M \<le> N \<longleftrightarrow> (\<forall>y. count N y < count M y \<longrightarrow> (\<exists>x. y < x \<and> count M x < count N x))"
blanchet@63409
   211
  by (auto simp: less_eq_multiset_def less_multiset\<^sub>H\<^sub>O)
blanchet@63409
   212
Mathias@63410
   213
instance by standard (auto simp: less_eq_multiset\<^sub>H\<^sub>O)
blanchet@63409
   214
blanchet@59813
   215
lemma
blanchet@63409
   216
  fixes M N :: "'a multiset"
blanchet@59813
   217
  shows
Mathias@63525
   218
    less_eq_multiset_plus_left: "N \<le> (M + N)" and
Mathias@63525
   219
    less_eq_multiset_plus_right: "M \<le> (M + N)"
Mathias@63410
   220
  by simp_all
blanchet@59813
   221
blanchet@59813
   222
lemma
blanchet@63409
   223
  fixes M N :: "'a multiset"
blanchet@59813
   224
  shows
Mathias@63525
   225
    le_multiset_plus_left_nonempty: "M \<noteq> {#} \<Longrightarrow> N < M + N" and
Mathias@63525
   226
    le_multiset_plus_right_nonempty: "N \<noteq> {#} \<Longrightarrow> M < M + N"
Mathias@63525
   227
    by simp_all
Mathias@63388
   228
Mathias@63410
   229
end
Mathias@63410
   230
blanchet@65546
   231
lemma all_lt_Max_imp_lt_mset: "N \<noteq> {#} \<Longrightarrow> (\<forall>a \<in># M. a < Max (set_mset N)) \<Longrightarrow> M < N"
blanchet@65546
   232
  by (meson Max_in[OF finite_set_mset] ex_gt_imp_less_multiset set_mset_eq_empty_iff)
blanchet@65546
   233
blanchet@65546
   234
lemma lt_imp_ex_count_lt: "M < N \<Longrightarrow> \<exists>y. count M y < count N y"
blanchet@65546
   235
  by (meson less_eq_multiset\<^sub>H\<^sub>O less_le_not_le)
blanchet@65546
   236
blanchet@65546
   237
lemma subset_imp_less_mset: "A \<subset># B \<Longrightarrow> A < B"
blanchet@65546
   238
  by (simp add: order.not_eq_order_implies_strict subset_eq_imp_le_multiset)
blanchet@65546
   239
blanchet@65546
   240
lemma image_mset_strict_mono:
blanchet@65546
   241
  assumes
blanchet@65546
   242
    mono_f: "\<forall>x \<in> set_mset M. \<forall>y \<in> set_mset N. x < y \<longrightarrow> f x < f y" and
blanchet@65546
   243
    less: "M < N"
blanchet@65546
   244
  shows "image_mset f M < image_mset f N"
blanchet@65546
   245
proof -
blanchet@65546
   246
  obtain Y X where
blanchet@65546
   247
    y_nemp: "Y \<noteq> {#}" and y_sub_N: "Y \<subseteq># N" and M_eq: "M = N - Y + X" and
blanchet@65546
   248
    ex_y: "\<forall>x. x \<in># X \<longrightarrow> (\<exists>y. y \<in># Y \<and> x < y)"
blanchet@65546
   249
    using less[unfolded less_multiset\<^sub>D\<^sub>M] by blast
blanchet@65546
   250
blanchet@65546
   251
  have x_sub_M: "X \<subseteq># M"
blanchet@65546
   252
    using M_eq by simp
blanchet@65546
   253
blanchet@65546
   254
  let ?fY = "image_mset f Y"
blanchet@65546
   255
  let ?fX = "image_mset f X"
blanchet@65546
   256
blanchet@65546
   257
  show ?thesis
blanchet@65546
   258
    unfolding less_multiset\<^sub>D\<^sub>M
blanchet@65546
   259
  proof (intro exI conjI)
blanchet@65546
   260
    show "image_mset f M = image_mset f N - ?fY + ?fX"
blanchet@65546
   261
      using M_eq[THEN arg_cong, of "image_mset f"] y_sub_N
blanchet@65546
   262
      by (metis image_mset_Diff image_mset_union)
blanchet@65546
   263
  next
blanchet@65546
   264
    obtain y where y: "\<forall>x. x \<in># X \<longrightarrow> y x \<in># Y \<and> x < y x"
blanchet@65546
   265
      using ex_y by moura
blanchet@65546
   266
blanchet@65546
   267
    show "\<forall>fx. fx \<in># ?fX \<longrightarrow> (\<exists>fy. fy \<in># ?fY \<and> fx < fy)"
blanchet@65546
   268
    proof (intro allI impI)
blanchet@65546
   269
      fix fx
blanchet@65546
   270
      assume "fx \<in># ?fX"
blanchet@65546
   271
      then obtain x where fx: "fx = f x" and x_in: "x \<in># X"
blanchet@65546
   272
        by auto
blanchet@65546
   273
      hence y_in: "y x \<in># Y" and y_gt: "x < y x"
blanchet@65546
   274
        using y[rule_format, OF x_in] by blast+
blanchet@65546
   275
      hence "f (y x) \<in># ?fY \<and> f x < f (y x)"
blanchet@65546
   276
        using mono_f y_sub_N x_sub_M x_in
blanchet@65546
   277
        by (metis image_eqI in_image_mset mset_subset_eqD)
blanchet@65546
   278
      thus "\<exists>fy. fy \<in># ?fY \<and> fx < fy"
blanchet@65546
   279
        unfolding fx by auto
blanchet@65546
   280
    qed
blanchet@65546
   281
  qed (auto simp: y_nemp y_sub_N image_mset_subseteq_mono)
blanchet@65546
   282
qed
blanchet@65546
   283
blanchet@65546
   284
lemma image_mset_mono:
blanchet@65546
   285
  assumes
blanchet@65546
   286
    mono_f: "\<forall>x \<in> set_mset M. \<forall>y \<in> set_mset N. x < y \<longrightarrow> f x < f y" and
blanchet@65546
   287
    less: "M \<le> N"
blanchet@65546
   288
  shows "image_mset f M \<le> image_mset f N"
blanchet@65546
   289
  by (metis eq_iff image_mset_strict_mono less less_imp_le mono_f order.not_eq_order_implies_strict)
blanchet@65546
   290
blanchet@65546
   291
lemma mset_lt_single_right_iff[simp]: "M < {#y#} \<longleftrightarrow> (\<forall>x \<in># M. x < y)" for y :: "'a::linorder"
blanchet@65546
   292
proof (rule iffI)
blanchet@65546
   293
  assume M_lt_y: "M < {#y#}"
blanchet@65546
   294
  show "\<forall>x \<in># M. x < y"
blanchet@65546
   295
  proof
blanchet@65546
   296
    fix x
blanchet@65546
   297
    assume x_in: "x \<in># M"
blanchet@65546
   298
    hence M: "M - {#x#} + {#x#} = M"
blanchet@65546
   299
      by (meson insert_DiffM2)
blanchet@65546
   300
    hence "\<not> {#x#} < {#y#} \<Longrightarrow> x < y"
blanchet@65546
   301
      using x_in M_lt_y
blanchet@65546
   302
      by (metis diff_single_eq_union le_multiset_empty_left less_add_same_cancel2 mset_le_trans)
blanchet@65546
   303
    also have "\<not> {#y#} < M"
blanchet@65546
   304
      using M_lt_y mset_le_not_sym by blast
blanchet@65546
   305
    ultimately show "x < y"
blanchet@65546
   306
      by (metis (no_types) Max_ge all_lt_Max_imp_lt_mset empty_iff finite_set_mset insertE
blanchet@65546
   307
        less_le_trans linorder_less_linear mset_le_not_sym set_mset_add_mset_insert
blanchet@65546
   308
        set_mset_eq_empty_iff x_in)
blanchet@65546
   309
  qed
blanchet@65546
   310
next
blanchet@65546
   311
  assume y_max: "\<forall>x \<in># M. x < y"
blanchet@65546
   312
  show "M < {#y#}"
blanchet@65546
   313
    by (rule all_lt_Max_imp_lt_mset) (auto intro!: y_max)
blanchet@65546
   314
qed
blanchet@65546
   315
blanchet@65546
   316
lemma mset_le_single_right_iff[simp]:
blanchet@65546
   317
  "M \<le> {#y#} \<longleftrightarrow> M = {#y#} \<or> (\<forall>x \<in># M. x < y)" for y :: "'a::linorder"
blanchet@65546
   318
  by (meson less_eq_multiset_def mset_lt_single_right_iff)
blanchet@65546
   319
Mathias@63793
   320
Mathias@63793
   321
subsection \<open>Simprocs\<close>
Mathias@63793
   322
Mathias@63793
   323
lemma mset_le_add_iff1:
Mathias@63793
   324
  "j \<le> (i::nat) \<Longrightarrow> (repeat_mset i u + m \<le> repeat_mset j u + n) = (repeat_mset (i-j) u + m \<le> n)"
Mathias@63793
   325
proof -
Mathias@63793
   326
  assume "j \<le> i"
Mathias@63793
   327
  then have "j + (i - j) = i"
Mathias@63793
   328
    using le_add_diff_inverse by blast
Mathias@63793
   329
  then show ?thesis
Mathias@63793
   330
    by (metis (no_types) add_le_cancel_left left_add_mult_distrib_mset)
Mathias@63793
   331
qed
Mathias@63793
   332
Mathias@63793
   333
lemma mset_le_add_iff2:
Mathias@63793
   334
  "i \<le> (j::nat) \<Longrightarrow> (repeat_mset i u + m \<le> repeat_mset j u + n) = (m \<le> repeat_mset (j-i) u + n)"
Mathias@63793
   335
proof -
Mathias@63793
   336
  assume "i \<le> j"
Mathias@63793
   337
  then have "i + (j - i) = j"
Mathias@63793
   338
    using le_add_diff_inverse by blast
Mathias@63793
   339
  then show ?thesis
Mathias@63793
   340
    by (metis (no_types) add_le_cancel_left left_add_mult_distrib_mset)
Mathias@63793
   341
qed
Mathias@63793
   342
Mathias@65027
   343
simproc_setup msetless_cancel
Mathias@63793
   344
  ("(l::'a::preorder multiset) + m < n" | "(l::'a multiset) < m + n" |
Mathias@65028
   345
   "add_mset a m < n" | "m < add_mset a n" |
Mathias@65028
   346
   "replicate_mset p a < n" | "m < replicate_mset p a" |
Mathias@65028
   347
   "repeat_mset p m < n" | "m < repeat_mset p n") =
Mathias@65031
   348
  \<open>fn phi => Cancel_Simprocs.less_cancel\<close>
Mathias@63793
   349
Mathias@65027
   350
simproc_setup msetle_cancel
Mathias@63793
   351
  ("(l::'a::preorder multiset) + m \<le> n" | "(l::'a multiset) \<le> m + n" |
Mathias@65028
   352
   "add_mset a m \<le> n" | "m \<le> add_mset a n" |
Mathias@65028
   353
   "replicate_mset p a \<le> n" | "m \<le> replicate_mset p a" |
Mathias@65028
   354
   "repeat_mset p m \<le> n" | "m \<le> repeat_mset p n") =
Mathias@65031
   355
  \<open>fn phi => Cancel_Simprocs.less_eq_cancel\<close>
Mathias@63793
   356
Mathias@63793
   357
Mathias@63793
   358
subsection \<open>Additional facts and instantiations\<close>
Mathias@63793
   359
Mathias@63388
   360
lemma ex_gt_count_imp_le_multiset:
Mathias@63410
   361
  "(\<forall>y :: 'a :: order. y \<in># M + N \<longrightarrow> y \<le> x) \<Longrightarrow> count M x < count N x \<Longrightarrow> M < N"
haftmann@62430
   362
  unfolding less_multiset\<^sub>H\<^sub>O
Mathias@63410
   363
  by (metis count_greater_zero_iff le_imp_less_or_eq less_imp_not_less not_gr_zero union_iff)
Mathias@63410
   364
Mathias@64418
   365
lemma mset_lt_single_iff[iff]: "{#x#} < {#y#} \<longleftrightarrow> x < y"
Mathias@64418
   366
  unfolding less_multiset\<^sub>H\<^sub>O by simp
Mathias@64418
   367
Mathias@64418
   368
lemma mset_le_single_iff[iff]: "{#x#} \<le> {#y#} \<longleftrightarrow> x \<le> y" for x y :: "'a::order"
Mathias@64418
   369
  unfolding less_eq_multiset\<^sub>H\<^sub>O by force
Mathias@64418
   370
Mathias@63410
   371
instance multiset :: (linorder) linordered_cancel_ab_semigroup_add
Mathias@63410
   372
  by standard (metis less_eq_multiset\<^sub>H\<^sub>O not_less_iff_gr_or_eq)
Mathias@63410
   373
Mathias@63410
   374
lemma less_eq_multiset_total:
Mathias@63410
   375
  fixes M N :: "'a :: linorder multiset"
Mathias@63410
   376
  shows "\<not> M \<le> N \<Longrightarrow> N \<le> M"
Mathias@63410
   377
  by simp
blanchet@63409
   378
blanchet@63409
   379
instantiation multiset :: (wellorder) wellorder
blanchet@63409
   380
begin
blanchet@63409
   381
blanchet@63409
   382
lemma wf_less_multiset: "wf {(M :: 'a multiset, N). M < N}"
blanchet@63409
   383
  unfolding less_multiset_def by (auto intro: wf_mult wf)
blanchet@63409
   384
blanchet@63409
   385
instance by standard (metis less_multiset_def wf wf_def wf_mult)
blanchet@59813
   386
blanchet@59813
   387
end
blanchet@63409
   388
Mathias@63410
   389
instantiation multiset :: (preorder) order_bot
Mathias@63410
   390
begin
Mathias@63410
   391
Mathias@63410
   392
definition bot_multiset :: "'a multiset" where "bot_multiset = {#}"
Mathias@63410
   393
Mathias@63410
   394
instance by standard (simp add: bot_multiset_def)
Mathias@63410
   395
blanchet@63409
   396
end
Mathias@63410
   397
Mathias@63410
   398
instance multiset :: (preorder) no_top
Mathias@63410
   399
proof standard
Mathias@63410
   400
  fix x :: "'a multiset"
Mathias@63410
   401
  obtain a :: 'a where True by simp
Mathias@63410
   402
  have "x < x + (x + {#a#})"
Mathias@63410
   403
    by simp
Mathias@63410
   404
  then show "\<exists>y. x < y"
Mathias@63410
   405
    by blast
Mathias@63410
   406
qed
Mathias@63410
   407
Mathias@63410
   408
instance multiset :: (preorder) ordered_cancel_comm_monoid_add
Mathias@63410
   409
  by standard
Mathias@63410
   410
blanchet@65546
   411
instantiation multiset :: (linorder) distrib_lattice
blanchet@65546
   412
begin
blanchet@65546
   413
blanchet@65546
   414
definition inf_multiset :: "'a multiset \<Rightarrow> 'a multiset \<Rightarrow> 'a multiset" where
blanchet@65546
   415
  "inf_multiset A B = (if A < B then A else B)"
blanchet@65546
   416
blanchet@65546
   417
definition sup_multiset :: "'a multiset \<Rightarrow> 'a multiset \<Rightarrow> 'a multiset" where
blanchet@65546
   418
  "sup_multiset A B = (if B > A then B else A)"
blanchet@65546
   419
blanchet@65546
   420
instance
blanchet@65546
   421
  by intro_classes (auto simp: inf_multiset_def sup_multiset_def)
blanchet@65546
   422
Mathias@63410
   423
end
blanchet@65546
   424
blanchet@65546
   425
end