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