author blanchet Wed Mar 25 17:51:34 2015 +0100 (2015-03-25) changeset 59813 6320064f22bb parent 59812 675d0c692c41 child 59814 2d9cf954a829
more multiset theorems
 CONTRIBUTORS file | annotate | diff | revisions NEWS file | annotate | diff | revisions src/HOL/Library/Library.thy file | annotate | diff | revisions src/HOL/Library/Multiset.thy file | annotate | diff | revisions src/HOL/Library/Multiset_Order.thy file | annotate | diff | revisions
```     1.1 --- a/CONTRIBUTORS	Wed Mar 25 14:39:40 2015 +0100
1.2 +++ b/CONTRIBUTORS	Wed Mar 25 17:51:34 2015 +0100
1.3 @@ -6,6 +6,9 @@
1.4  Contributions to this Isabelle version
1.5  --------------------------------------
1.6
1.7 +* March 2015: Jasmin Blanchette, Inria & LORIA & MPII, Mathias Fleury, MPII, and Dmitriy Traytel, TUM
1.8 +  More multiset theorems, syntax, and operations.
1.9 +
1.10  * December 2014: Johannes Hölzl, Manuel Eberl, Sudeep Kanav, TUM and Jeremy Avigad, Luke Serafin, CMU
1.11    Various integration theorems: mostly integration on intervals and substitution.
1.12
```
```     2.1 --- a/NEWS	Wed Mar 25 14:39:40 2015 +0100
2.2 +++ b/NEWS	Wed Mar 25 17:51:34 2015 +0100
2.3 @@ -262,6 +262,24 @@
2.4  The "sos_cert" functionality is invoked as "sos" with additional
2.5  argument. Minor INCOMPATIBILITY.
2.6
2.7 +* Theory "Library/Multiset":
2.8 +  - Introduced "replicate_mset" operation.
2.9 +  - Introduced alternative characterizations of the multiset ordering in
2.10 +    "Library/Multiset_Order".
2.11 +  - Renamed
2.12 +      in_multiset_of ~> in_multiset_in_set
2.13 +    INCOMPATIBILITY.
2.14 +  - Added attributes:
2.15 +      image_mset.id [simp]
2.16 +      image_mset_id [simp]
2.17 +      elem_multiset_of_set [simp, intro]
2.18 +      comp_fun_commute_plus_mset [simp]
2.19 +      comp_fun_commute.fold_mset_insert [OF comp_fun_commute_plus_mset, simp]
2.20 +      in_mset_fold_plus_iff [iff]
2.21 +      set_of_Union_mset [simp]
2.22 +      in_Union_mset_iff [iff]
2.23 +    INCOMPATIBILITY.
2.24 +
2.25  * HOL-Decision_Procs:
2.26    - New counterexample generator quickcheck[approximation] for
2.27      inequalities of transcendental functions.
```
```     3.1 --- a/src/HOL/Library/Library.thy	Wed Mar 25 14:39:40 2015 +0100
3.2 +++ b/src/HOL/Library/Library.thy	Wed Mar 25 17:51:34 2015 +0100
3.3 @@ -42,7 +42,7 @@
3.4    Mapping
3.6    More_List
3.7 -  Multiset
3.8 +  Multiset_Order
3.9    Numeral_Type
3.10    NthRoot_Limits
3.11    OptionalSugar
```
```     4.1 --- a/src/HOL/Library/Multiset.thy	Wed Mar 25 14:39:40 2015 +0100
4.2 +++ b/src/HOL/Library/Multiset.thy	Wed Mar 25 17:51:34 2015 +0100
4.3 @@ -1,6 +1,9 @@
4.4  (*  Title:      HOL/Library/Multiset.thy
4.5      Author:     Tobias Nipkow, Markus Wenzel, Lawrence C Paulson, Norbert Voelker
4.6      Author:     Andrei Popescu, TU Muenchen
4.7 +    Author:     Jasmin Blanchette, Inria, LORIA, MPII
4.8 +    Author:     Dmitriy Traytel, TU Muenchen
4.9 +    Author:     Mathias Fleury, MPII
4.10  *)
4.11
4.12  section {* (Finite) multisets *}
4.13 @@ -382,8 +385,7 @@
4.14  lemma multi_psub_self[simp]: "(A::'a multiset) < A = False"
4.15    by simp
4.16
4.18 -  "T + {#x#} < S + {#x#} \<Longrightarrow> T < S"
4.19 +lemma mset_less_add_bothsides: "N + {#x#} < M + {#x#} \<Longrightarrow> N < M"
4.20    by (fact add_less_imp_less_right)
4.21
4.22  lemma mset_less_empty_nonempty:
4.23 @@ -593,6 +595,10 @@
4.24  lemma set_of_mono: "A \<le> B \<Longrightarrow> set_of A \<subseteq> set_of B"
4.25    by (metis mset_leD subsetI mem_set_of_iff)
4.26
4.27 +lemma ball_set_of_iff: "(\<forall>x \<in> set_of M. P x) \<longleftrightarrow> (\<forall>x. x \<in># M \<longrightarrow> P x)"
4.28 +  by auto
4.29 +
4.30 +
4.31  subsubsection {* Size *}
4.32
4.33  definition wcount where "wcount f M = (\<lambda>x. count M x * Suc (f x))"
4.34 @@ -895,12 +901,24 @@
4.35  translations
4.36    "{#e. x:#M#}" == "CONST image_mset (%x. e) M"
4.37
4.38 +syntax (xsymbols)
4.39 +  "_comprehension2_mset" :: "'a \<Rightarrow> 'b \<Rightarrow> 'b multiset \<Rightarrow> 'a multiset"
4.40 +      ("({#_/. _ \<in># _#})")
4.41 +translations
4.42 +  "{#e. x \<in># M#}" == "CONST image_mset (\<lambda>x. e) M"
4.43 +
4.44  syntax
4.45 -  "_comprehension2_mset" :: "'a \<Rightarrow> 'b \<Rightarrow> 'b multiset \<Rightarrow> bool \<Rightarrow> 'a multiset"
4.46 +  "_comprehension3_mset" :: "'a \<Rightarrow> 'b \<Rightarrow> 'b multiset \<Rightarrow> bool \<Rightarrow> 'a multiset"
4.47        ("({#_/ | _ :# _./ _#})")
4.48  translations
4.49    "{#e | x:#M. P#}" => "{#e. x :# {# x:#M. P#}#}"
4.50
4.51 +syntax
4.52 +  "_comprehension4_mset" :: "'a \<Rightarrow> 'b \<Rightarrow> 'b multiset \<Rightarrow> bool \<Rightarrow> 'a multiset"
4.53 +      ("({#_/ | _ \<in># _./ _#})")
4.54 +translations
4.55 +  "{#e | x\<in>#M. P#}" => "{#e. x \<in># {# x\<in>#M. P#}#}"
4.56 +
4.57  text {*
4.58    This allows to write not just filters like @{term "{#x:#M. x<c#}"}
4.59    but also images like @{term "{#x+x. x:#M #}"} and @{term [source]
4.60 @@ -908,6 +926,9 @@
4.61    @{term "{#x+x|x:#M. x<c#}"}.
4.62  *}
4.63
4.64 +lemma in_image_mset: "y \<in># {#f x. x \<in># M#} \<longleftrightarrow> y \<in> f ` set_of M"
4.65 +  by (metis mem_set_of_iff set_of_image_mset)
4.66 +
4.67  functor image_mset: image_mset
4.68  proof -
4.69    fix f g show "image_mset f \<circ> image_mset g = image_mset (f \<circ> g)"
4.70 @@ -924,7 +945,19 @@
4.71    qed
4.72  qed
4.73
4.74 -declare image_mset.identity [simp]
4.75 +declare
4.76 +  image_mset.id [simp]
4.77 +  image_mset.identity [simp]
4.78 +
4.79 +lemma image_mset_id[simp]: "image_mset id x = x"
4.80 +  unfolding id_def by auto
4.81 +
4.82 +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#}"
4.83 +  by (induct M) auto
4.84 +
4.85 +lemma image_mset_cong_pair:
4.86 +  "(\<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#}"
4.87 +  by (metis image_mset_cong split_cong)
4.88
4.89
4.90  subsection {* Further conversions *}
4.91 @@ -942,7 +975,7 @@
4.92    by (induct xs) simp_all
4.93
4.94  lemma multiset_of_zero_iff[simp]: "(multiset_of x = {#}) = (x = [])"
4.95 -by (induct x) auto
4.96 +  by (induct x) auto
4.97
4.98  lemma multiset_of_zero_iff_right[simp]: "({#} = multiset_of x) = (x = [])"
4.99  by (induct x) auto
4.100 @@ -1059,10 +1092,6 @@
4.101    "multiset_of (insort x xs) = multiset_of xs + {#x#}"
4.102    by (induct xs) (simp_all add: ac_simps)
4.103
4.104 -lemma in_multiset_of:
4.105 -  "x \<in># multiset_of xs \<longleftrightarrow> x \<in> set xs"
4.106 -  by (induct xs) simp_all
4.107 -
4.108  lemma multiset_of_map:
4.109    "multiset_of (map f xs) = image_mset f (multiset_of xs)"
4.110    by (induct xs) simp_all
4.111 @@ -1098,6 +1127,9 @@
4.112    by (auto elim!: Set.set_insert)
4.113  qed -- {* TODO: maybe define @{const multiset_of_set} also in terms of @{const Abs_multiset} *}
4.114
4.115 +lemma elem_multiset_of_set[simp, intro]: "finite A \<Longrightarrow> x \<in># multiset_of_set A \<longleftrightarrow> x \<in> A"
4.116 +  by (induct A rule: finite_induct) simp_all
4.117 +
4.118  context linorder
4.119  begin
4.120
4.121 @@ -1186,6 +1218,14 @@
4.122
4.123  end
4.124
4.125 +lemma comp_fun_commute_plus_mset[simp]: "comp_fun_commute (op + \<Colon> 'a multiset \<Rightarrow> _ \<Rightarrow> _)"
4.126 +  by default (simp add: add_ac comp_def)
4.127 +
4.128 +declare comp_fun_commute.fold_mset_insert[OF comp_fun_commute_plus_mset, simp]
4.129 +
4.130 +lemma in_mset_fold_plus_iff[iff]: "x \<in># Multiset.fold (op +) M NN \<longleftrightarrow> x \<in># M \<or> (\<exists>N. N \<in># NN \<and> x \<in># N)"
4.131 +  by (induct NN) auto
4.132 +
4.133  notation times (infixl "*" 70)
4.134  notation Groups.one ("1")
4.135
4.136 @@ -1210,6 +1250,22 @@
4.137
4.138  end
4.139
4.140 +lemma msetsum_diff:
4.141 +  fixes M N :: "('a \<Colon> ordered_cancel_comm_monoid_diff) multiset"
4.142 +  shows "N \<le> M \<Longrightarrow> msetsum (M - N) = msetsum M - msetsum N"
4.143 +  by (metis add_diff_cancel_left' msetsum.union ordered_cancel_comm_monoid_diff_class.add_diff_inverse)
4.144 +
4.145 +abbreviation Union_mset :: "'a multiset multiset \<Rightarrow> 'a multiset" where
4.146 +  "Union_mset MM \<equiv> msetsum MM"
4.147 +
4.148 +notation (xsymbols) Union_mset ("\<Union>#_" [900] 900)
4.149 +
4.150 +lemma set_of_Union_mset[simp]: "set_of (\<Union># MM) = (\<Union>M \<in> set_of MM. set_of M)"
4.151 +  by (induct MM) auto
4.152 +
4.153 +lemma in_Union_mset_iff[iff]: "x \<in># \<Union># MM \<longleftrightarrow> (\<exists>M. M \<in># MM \<and> x \<in># M)"
4.154 +  by (induct MM) auto
4.155 +
4.156  syntax
4.157    "_msetsum_image" :: "pttrn \<Rightarrow> 'b set \<Rightarrow> 'a \<Rightarrow> 'a::comm_monoid_add"
4.158        ("(3SUM _:#_. _)" [0, 51, 10] 10)
4.159 @@ -1338,6 +1394,46 @@
4.160  lemma mcard_filter_lesseq[simp]: "mcard (Multiset.filter f M) \<le> mcard M"
4.161    by (rule mcard_mono[OF multiset_filter_subset])
4.162
4.163 +lemma mcard_1_singleton:
4.164 +  assumes card: "mcard AA = 1"
4.165 +  shows "\<exists>A. AA = {#A#}"
4.166 +  using card by (cases AA) auto
4.167 +
4.168 +lemma mcard_Diff_subset:
4.169 +  assumes "M \<le> M'"
4.170 +  shows "mcard (M' - M) = mcard M' - mcard M"
4.171 +  by (metis add_diff_cancel_left' assms mcard_plus mset_le_exists_conv)
4.172 +
4.173 +
4.174 +subsection {* Replicate operation *}
4.175 +
4.176 +definition replicate_mset :: "nat \<Rightarrow> 'a \<Rightarrow> 'a multiset" where
4.177 +  "replicate_mset n x = ((op + {#x#}) ^^ n) {#}"
4.178 +
4.179 +lemma replicate_mset_0[simp]: "replicate_mset 0 x = {#}"
4.180 +  unfolding replicate_mset_def by simp
4.181 +
4.182 +lemma replicate_mset_Suc[simp]: "replicate_mset (Suc n) x = replicate_mset n x + {#x#}"
4.183 +  unfolding replicate_mset_def by (induct n) (auto intro: add.commute)
4.184 +
4.185 +lemma in_replicate_mset[simp]: "x \<in># replicate_mset n y \<longleftrightarrow> n > 0 \<and> x = y"
4.186 +  unfolding replicate_mset_def by (induct n) simp_all
4.187 +
4.188 +lemma count_replicate_mset[simp]: "count (replicate_mset n x) y = (if y = x then n else 0)"
4.189 +  unfolding replicate_mset_def by (induct n) simp_all
4.190 +
4.191 +lemma set_of_replicate_mset_subset[simp]: "set_of (replicate_mset n x) = (if n = 0 then {} else {x})"
4.192 +  by (auto split: if_splits)
4.193 +
4.194 +lemma mcard_replicate_mset[simp]: "mcard (replicate_mset n M) = n"
4.195 +  by (induct n, simp_all)
4.196 +
4.197 +lemma count_le_replicate_mset_le: "n \<le> count M x \<longleftrightarrow> replicate_mset n x \<le> M"
4.198 +  by (auto simp add: assms mset_less_eqI) (metis count_replicate_mset less_eq_multiset.rep_eq)
4.199 +
4.200 +lemma filter_eq_replicate_mset: "{#y \<in># D. y = x#} = replicate_mset (count D x) x"
4.201 +  by (induct D) simp_all
4.202 +
4.203
4.204  subsection {* Alternative representations *}
4.205
4.206 @@ -1790,7 +1886,7 @@
4.207  qed (auto simp add: le_multiset_def intro: union_less_mono2)
4.208
4.209
4.210 -subsection {* Termination proofs with multiset orders *}
4.211 +subsubsection {* Termination proofs with multiset orders *}
4.212
4.213  lemma multi_member_skip: "x \<in># XS \<Longrightarrow> x \<in># {# y #} + XS"
4.214    and multi_member_this: "x \<in># {# x #} + XS"
4.215 @@ -2082,9 +2178,7 @@
4.216    then show ?thesis by simp
4.217  qed
4.218
4.219 -lemma [code_unfold]:
4.220 -  "x \<in># multiset_of xs \<longleftrightarrow> x \<in> set xs"
4.221 -  by (simp add: in_multiset_of)
4.222 +declare in_multiset_in_set [code_unfold]
4.223
4.224  lemma [code]:
4.225    "count (multiset_of xs) x = fold (\<lambda>y. if x = y then Suc else id) xs 0"
4.226 @@ -2094,25 +2188,19 @@
4.227    then show ?thesis by simp
4.228  qed
4.229
4.230 -lemma [code]:
4.231 -  "set_of (multiset_of xs) = set xs"
4.232 -  by simp
4.233 -
4.234 -lemma [code]:
4.235 -  "sorted_list_of_multiset (multiset_of xs) = sort xs"
4.236 -  by (induct xs) simp_all
4.237 +declare set_of_multiset_of [code]
4.238 +
4.239 +declare sorted_list_of_multiset_multiset_of [code]
4.240
4.241  lemma [code]: -- {* not very efficient, but representation-ignorant! *}
4.242    "multiset_of_set A = multiset_of (sorted_list_of_set A)"
4.243    apply (cases "finite A")
4.244    apply simp_all
4.245    apply (induct A rule: finite_induct)
4.246 -  apply (simp_all add: union_commute)
4.248    done
4.249
4.250 -lemma [code]:
4.251 -  "mcard (multiset_of xs) = length xs"
4.252 -  by (simp add: mcard_multiset_of)
4.253 +declare mcard_multiset_of [code]
4.254
4.255  fun ms_lesseq_impl :: "'a list \<Rightarrow> 'a list \<Rightarrow> bool option" where
4.256    "ms_lesseq_impl [] ys = Some (ys \<noteq> [])"
4.257 @@ -2287,7 +2375,7 @@
4.258    have "multiset_of xs' = {#x#} + multiset_of xsa"
4.259      unfolding xsa_def using j_len nth_j
4.260      by (metis (no_types) ab_semigroup_add_class.add_ac(1) append_take_drop_id Cons_nth_drop_Suc
4.261 -      multiset_of.simps(2) union_code union_commute)
4.262 +      multiset_of.simps(2) union_code add.commute)
4.263    hence ms_x: "multiset_of xsa = multiset_of xs"
4.264      by (metis Cons.prems add.commute add_right_imp_eq multiset_of.simps(2))
4.265    then obtain ysa where
4.266 @@ -2344,7 +2432,7 @@
4.267      by (rule image_mset.id)
4.268  next
4.269    show "\<And>f g. image_mset (g \<circ> f) = image_mset g \<circ> image_mset f"
4.270 -    unfolding comp_def by (rule ext) (simp add: image_mset.compositionality comp_def)
4.271 +    unfolding comp_def by (rule ext) (simp add: comp_def image_mset.compositionality)
4.272  next
4.273    fix X :: "'a multiset"
4.274    show "\<And>f g. (\<And>z. z \<in> set_of X \<Longrightarrow> f z = g z) \<Longrightarrow> image_mset f X = image_mset g X"
```
```     5.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
5.2 +++ b/src/HOL/Library/Multiset_Order.thy	Wed Mar 25 17:51:34 2015 +0100
5.3 @@ -0,0 +1,308 @@
5.4 +(*  Title:      HOL/Library/Multiset_Order.thy
5.5 +    Author:     Dmitriy Traytel, TU Muenchen
5.6 +    Author:     Jasmin Blanchette, Inria, LORIA, MPII
5.7 +*)
5.8 +
5.9 +section {* More Theorems about the Multiset Order *}
5.10 +
5.11 +theory Multiset_Order
5.12 +imports Multiset
5.13 +begin
5.14 +
5.15 +subsubsection {* Alternative characterizations *}
5.16 +
5.17 +context order
5.18 +begin
5.19 +
5.20 +lemma reflp_le: "reflp (op \<le>)"
5.21 +  unfolding reflp_def by simp
5.22 +
5.23 +lemma antisymP_le: "antisymP (op \<le>)"
5.24 +  unfolding antisym_def by auto
5.25 +
5.26 +lemma transp_le: "transp (op \<le>)"
5.27 +  unfolding transp_def by auto
5.28 +
5.29 +lemma irreflp_less: "irreflp (op <)"
5.30 +  unfolding irreflp_def by simp
5.31 +
5.32 +lemma antisymP_less: "antisymP (op <)"
5.33 +  unfolding antisym_def by auto
5.34 +
5.35 +lemma transp_less: "transp (op <)"
5.36 +  unfolding transp_def by auto
5.37 +
5.38 +lemmas le_trans = transp_le[unfolded transp_def, rule_format]
5.39 +
5.40 +lemma order_mult: "class.order
5.41 +  (\<lambda>M N. (M, N) \<in> mult {(x, y). x < y} \<or> M = N)
5.42 +  (\<lambda>M N. (M, N) \<in> mult {(x, y). x < y})"
5.43 +  (is "class.order ?le ?less")
5.44 +proof -
5.45 +  have irrefl: "\<And>M :: 'a multiset. \<not> ?less M M"
5.46 +  proof
5.47 +    fix M :: "'a multiset"
5.48 +    have "trans {(x'::'a, x). x' < x}"
5.49 +      by (rule transI) simp
5.50 +    moreover
5.51 +    assume "(M, M) \<in> mult {(x, y). x < y}"
5.52 +    ultimately have "\<exists>I J K. M = I + J \<and> M = I + K
5.53 +      \<and> J \<noteq> {#} \<and> (\<forall>k\<in>set_of K. \<exists>j\<in>set_of J. (k, j) \<in> {(x, y). x < y})"
5.54 +      by (rule mult_implies_one_step)
5.55 +    then obtain I J K where "M = I + J" and "M = I + K"
5.56 +      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
5.57 +    then have aux1: "K \<noteq> {#}" and aux2: "\<forall>k\<in>set_of K. \<exists>j\<in>set_of K. k < j" by auto
5.58 +    have "finite (set_of K)" by simp
5.59 +    moreover note aux2
5.60 +    ultimately have "set_of K = {}"
5.61 +      by (induct rule: finite_induct)
5.62 +       (simp, metis (mono_tags) insert_absorb insert_iff insert_not_empty less_irrefl less_trans)
5.63 +    with aux1 show False by simp
5.64 +  qed
5.65 +  have trans: "\<And>K M N :: 'a multiset. ?less K M \<Longrightarrow> ?less M N \<Longrightarrow> ?less K N"
5.66 +    unfolding mult_def by (blast intro: trancl_trans)
5.67 +  show "class.order ?le ?less"
5.68 +    by default (auto simp add: le_multiset_def irrefl dest: trans)
5.69 +qed
5.70 +
5.71 +text {* The Dershowitz--Manna ordering: *}
5.72 +
5.73 +definition less_multiset\<^sub>D\<^sub>M where
5.74 +  "less_multiset\<^sub>D\<^sub>M M N \<longleftrightarrow>
5.75 +   (\<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)))"
5.76 +
5.77 +
5.78 +text {* The Huet--Oppen ordering: *}
5.79 +
5.80 +definition less_multiset\<^sub>H\<^sub>O where
5.81 +  "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))"
5.82 +
5.83 +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"
5.84 +proof (unfold mult_def less_multiset\<^sub>H\<^sub>O_def, induct rule: trancl_induct)
5.85 +  case (base P)
5.86 +  then show ?case unfolding mult1_def by force
5.87 +next
5.88 +  case (step N P)
5.89 +  from step(2) obtain M0 a K where
5.90 +    *: "P = M0 + {#a#}" "N = M0 + K" "\<And>b. b \<in># K \<Longrightarrow> b < a"
5.91 +    unfolding mult1_def by blast
5.92 +  then have count_K_a: "count K a = 0" by auto
5.93 +  with step(3) *(1,2) have "M \<noteq> P" by (force dest: *(3) split: if_splits)
5.94 +  moreover
5.95 +  { assume "count P a \<le> count M a"
5.96 +    with count_K_a have "count N a < count M a" unfolding *(1,2) by auto
5.97 +      with step(3) obtain z where z: "z > a" "count M z < count N z" by blast
5.98 +      with * have "count N z \<le> count P z" by force
5.99 +      with z have "\<exists>z > a. count M z < count P z" by auto
5.100 +  } note count_a = this
5.101 +  { fix y
5.102 +    assume count_y: "count P y < count M y"
5.103 +    have "\<exists>x>y. count M x < count P x"
5.104 +    proof (cases "y = a")
5.105 +      case True
5.106 +      with count_y count_a show ?thesis by auto
5.107 +    next
5.108 +      case False
5.109 +      show ?thesis
5.110 +      proof (cases "y \<in># K")
5.111 +        case True
5.112 +        with *(3) have "y < a" by simp
5.113 +        then show ?thesis by (cases "count P a \<le> count M a") (auto dest: count_a intro: less_trans)
5.114 +      next
5.115 +        case False
5.116 +        with `y \<noteq> a` have "count P y = count N y" unfolding *(1,2) by simp
5.117 +        with count_y step(3) obtain z where z: "z > y" "count M z < count N z" by auto
5.118 +        show ?thesis
5.119 +        proof (cases "z \<in># K")
5.120 +          case True
5.121 +          with *(3) have "z < a" by simp
5.122 +          with z(1) show ?thesis
5.123 +            by (cases "count P a \<le> count M a") (auto dest!: count_a intro: less_trans)
5.124 +        next
5.125 +          case False
5.126 +          with count_K_a have "count N z \<le> count P z" unfolding * by auto
5.127 +          with z show ?thesis by auto
5.128 +        qed
5.129 +      qed
5.130 +    qed
5.131 +  }
5.132 +  ultimately show ?case by blast
5.133 +qed
5.134 +
5.135 +lemma less_multiset\<^sub>D\<^sub>M_imp_mult:
5.136 +  "less_multiset\<^sub>D\<^sub>M M N \<Longrightarrow> (M, N) \<in> mult {(x, y). x < y}"
5.137 +proof -
5.138 +  assume "less_multiset\<^sub>D\<^sub>M M N"
5.139 +  then obtain X Y where
5.140 +    "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)"
5.141 +    unfolding less_multiset\<^sub>D\<^sub>M_def by blast
5.142 +  then have "(N - X + Y, N - X + X) \<in> mult {(x, y). x < y}"
5.143 +    by (intro one_step_implies_mult) (auto simp: Bex_def trans_def)
5.144 +  with `M = N - X + Y` `X \<le> N` show "(M, N) \<in> mult {(x, y). x < y}"
5.145 +    by (metis ordered_cancel_comm_monoid_diff_class.diff_add)
5.146 +qed
5.147 +
5.148 +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"
5.149 +unfolding less_multiset\<^sub>D\<^sub>M_def
5.150 +proof (intro iffI exI conjI)
5.151 +  assume "less_multiset\<^sub>H\<^sub>O M N"
5.152 +  then obtain z where z: "count M z < count N z"
5.153 +    unfolding less_multiset\<^sub>H\<^sub>O_def by (auto simp: multiset_eq_iff nat_neq_iff)
5.154 +  def X \<equiv> "N - M"
5.155 +  def Y \<equiv> "M - N"
5.156 +  from z show "X \<noteq> {#}" unfolding X_def by (auto simp: multiset_eq_iff not_less_eq_eq Suc_le_eq)
5.157 +  from z show "X \<le> N" unfolding X_def by auto
5.158 +  show "M = (N - X) + Y" unfolding X_def Y_def multiset_eq_iff count_union count_diff by force
5.159 +  show "\<forall>k. k \<in># Y \<longrightarrow> (\<exists>a. a \<in># X \<and> k < a)"
5.160 +  proof (intro allI impI)
5.161 +    fix k
5.162 +    assume "k \<in># Y"
5.163 +    then have "count N k < count M k" unfolding Y_def by auto
5.164 +    with `less_multiset\<^sub>H\<^sub>O M N` obtain a where "k < a" and "count M a < count N a"
5.165 +      unfolding less_multiset\<^sub>H\<^sub>O_def by blast
5.166 +    then show "\<exists>a. a \<in># X \<and> k < a" unfolding X_def by auto
5.167 +  qed
5.168 +qed
5.169 +
5.170 +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"
5.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)
5.172 +
5.173 +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"
5.174 +  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)
5.175 +
5.176 +lemmas mult\<^sub>D\<^sub>M = mult_less_multiset\<^sub>D\<^sub>M[unfolded less_multiset\<^sub>D\<^sub>M_def]
5.177 +lemmas mult\<^sub>H\<^sub>O = mult_less_multiset\<^sub>H\<^sub>O[unfolded less_multiset\<^sub>H\<^sub>O_def]
5.178 +
5.179 +end
5.180 +
5.181 +context linorder
5.182 +begin
5.183 +
5.184 +lemma total_le: "total {(a \<Colon> 'a, b). a \<le> b}"
5.185 +  unfolding total_on_def by auto
5.186 +
5.187 +lemma total_less: "total {(a \<Colon> 'a, b). a < b}"
5.188 +  unfolding total_on_def by auto
5.189 +
5.190 +lemma linorder_mult: "class.linorder
5.191 +  (\<lambda>M N. (M, N) \<in> mult {(x, y). x < y} \<or> M = N)
5.192 +  (\<lambda>M N. (M, N) \<in> mult {(x, y). x < y})"
5.193 +proof -
5.194 +  interpret o: order
5.195 +    "(\<lambda>M N. (M, N) \<in> mult {(x, y). x < y} \<or> M = N)"
5.196 +    "(\<lambda>M N. (M, N) \<in> mult {(x, y). x < y})"
5.197 +    by (rule order_mult)
5.198 +  show ?thesis by unfold_locales (auto 0 3 simp: mult\<^sub>H\<^sub>O not_less_iff_gr_or_eq)
5.199 +qed
5.200 +
5.201 +end
5.202 +
5.203 +lemma less_multiset_less_multiset\<^sub>H\<^sub>O:
5.204 +  "M \<subset># N \<longleftrightarrow> less_multiset\<^sub>H\<^sub>O M N"
5.205 +  unfolding less_multiset_def mult\<^sub>H\<^sub>O less_multiset\<^sub>H\<^sub>O_def ..
5.206 +
5.207 +lemmas less_multiset\<^sub>D\<^sub>M = mult\<^sub>D\<^sub>M[folded less_multiset_def]
5.208 +lemmas less_multiset\<^sub>H\<^sub>O = mult\<^sub>H\<^sub>O[folded less_multiset_def]
5.209 +
5.210 +lemma le_multiset\<^sub>H\<^sub>O:
5.211 +  fixes M N :: "('a \<Colon> linorder) multiset"
5.212 +  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))"
5.213 +  by (auto simp: le_multiset_def less_multiset\<^sub>H\<^sub>O)
5.214 +
5.215 +lemma wf_less_multiset: "wf {(M \<Colon> ('a \<Colon> wellorder) multiset, N). M \<subset># N}"
5.216 +  unfolding less_multiset_def by (auto intro: wf_mult wf)
5.217 +
5.218 +lemma order_multiset: "class.order
5.219 +  (le_multiset :: ('a \<Colon> order) multiset \<Rightarrow> ('a \<Colon> order) multiset \<Rightarrow> bool)
5.220 +  (less_multiset :: ('a \<Colon> order) multiset \<Rightarrow> ('a \<Colon> order) multiset \<Rightarrow> bool)"
5.221 +  by unfold_locales
5.222 +
5.223 +lemma linorder_multiset: "class.linorder
5.224 +  (le_multiset :: ('a \<Colon> linorder) multiset \<Rightarrow> ('a \<Colon> linorder) multiset \<Rightarrow> bool)
5.225 +  (less_multiset :: ('a \<Colon> linorder) multiset \<Rightarrow> ('a \<Colon> linorder) multiset \<Rightarrow> bool)"
5.226 +  by unfold_locales (fastforce simp add: less_multiset\<^sub>H\<^sub>O le_multiset_def not_less_iff_gr_or_eq)
5.227 +
5.228 +interpretation multiset_linorder: linorder
5.229 +  "le_multiset :: ('a \<Colon> linorder) multiset \<Rightarrow> ('a \<Colon> linorder) multiset \<Rightarrow> bool"
5.230 +  "less_multiset :: ('a \<Colon> linorder) multiset \<Rightarrow> ('a \<Colon> linorder) multiset \<Rightarrow> bool"
5.231 +  by (rule linorder_multiset)
5.232 +
5.233 +interpretation multiset_wellorder: wellorder
5.234 +  "le_multiset :: ('a \<Colon> wellorder) multiset \<Rightarrow> ('a \<Colon> wellorder) multiset \<Rightarrow> bool"
5.235 +  "less_multiset :: ('a \<Colon> wellorder) multiset \<Rightarrow> ('a \<Colon> wellorder) multiset \<Rightarrow> bool"
5.236 +  by unfold_locales (blast intro: wf_less_multiset[unfolded wf_def, rule_format])
5.237 +
5.238 +lemma le_multiset_total:
5.239 +  fixes M N :: "('a \<Colon> linorder) multiset"
5.240 +  shows "\<not> M \<subseteq># N \<Longrightarrow> N \<subseteq># M"
5.241 +  by (metis multiset_linorder.le_cases)
5.242 +
5.243 +lemma less_eq_imp_le_multiset:
5.244 +  fixes M N :: "('a \<Colon> linorder) multiset"
5.245 +  shows "M \<le> N \<Longrightarrow> M \<subseteq># N"
5.246 +  unfolding le_multiset_def less_multiset\<^sub>H\<^sub>O
5.247 +  by (auto dest: leD simp add: less_eq_multiset.rep_eq)
5.248 +
5.249 +lemma less_multiset_right_total:
5.250 +  fixes M :: "('a \<Colon> linorder) multiset"
5.251 +  shows "M \<subset># M + {#undefined#}"
5.252 +  unfolding le_multiset_def less_multiset\<^sub>H\<^sub>O by simp
5.253 +
5.254 +lemma le_multiset_empty_left[simp]:
5.255 +  fixes M :: "('a \<Colon> linorder) multiset"
5.256 +  shows "{#} \<subseteq># M"
5.257 +  by (simp add: less_eq_imp_le_multiset)
5.258 +
5.259 +lemma le_multiset_empty_right[simp]:
5.260 +  fixes M :: "('a \<Colon> linorder) multiset"
5.261 +  shows "M \<noteq> {#} \<Longrightarrow> \<not> M \<subseteq># {#}"
5.262 +  by (metis le_multiset_empty_left multiset_order.antisym)
5.263 +
5.264 +lemma less_multiset_empty_left[simp]:
5.265 +  fixes M :: "('a \<Colon> linorder) multiset"
5.266 +  shows "M \<noteq> {#} \<Longrightarrow> {#} \<subset># M"
5.267 +  by (simp add: less_multiset\<^sub>H\<^sub>O)
5.268 +
5.269 +lemma less_multiset_empty_right[simp]:
5.270 +  fixes M :: "('a \<Colon> linorder) multiset"
5.271 +  shows "\<not> M \<subset># {#}"
5.272 +  using le_empty less_multiset\<^sub>D\<^sub>M by blast
5.273 +
5.274 +lemma
5.275 +  fixes M N :: "('a \<Colon> linorder) multiset"
5.276 +  shows
5.277 +    le_multiset_plus_left[simp]: "N \<subseteq># (M + N)" and
5.278 +    le_multiset_plus_right[simp]: "M \<subseteq># (M + N)"
5.279 +  using [[metis_verbose = false]] by (metis less_eq_imp_le_multiset mset_le_add_left add.commute)+
5.280 +
5.281 +lemma
5.282 +  fixes M N :: "('a \<Colon> linorder) multiset"
5.283 +  shows
5.284 +    less_multiset_plus_plus_left_iff[simp]: "M + N \<subset># M' + N \<longleftrightarrow> M \<subset># M'" and
5.285 +    less_multiset_plus_plus_right_iff[simp]: "M + N \<subset># M + N' \<longleftrightarrow> N \<subset># N'"
5.286 +  unfolding less_multiset\<^sub>H\<^sub>O by auto
5.287 +
5.288 +lemma add_eq_self_empty_iff: "M + N = M \<longleftrightarrow> N = {#}"
5.290 +
5.291 +lemma
5.292 +  fixes M N :: "('a \<Colon> linorder) multiset"
5.293 +  shows
5.294 +    less_multiset_plus_left_nonempty[simp]: "M \<noteq> {#} \<Longrightarrow> N \<subset># M + N" and
5.295 +    less_multiset_plus_right_nonempty[simp]: "N \<noteq> {#} \<Longrightarrow> M \<subset># M + N"
5.296 +  using [[metis_verbose = false]]
5.297 +  by (metis add.right_neutral less_multiset_empty_left less_multiset_plus_plus_right_iff
5.299 +
5.300 +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"
5.301 +  unfolding less_multiset\<^sub>H\<^sub>O by (metis less_irrefl less_nat_zero_code not_gr0)
5.302 +
5.303 +lemma ex_gt_count_imp_less_multiset:
5.304 +  "(\<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"
5.305 +  unfolding less_multiset\<^sub>H\<^sub>O by (metis UnCI comm_monoid_diff_class.diff_cancel dual_order.asym
5.306 +    less_imp_diff_less mem_set_of_iff order.not_eq_order_implies_strict set_of_union)
5.307 +
5.308 +lemma union_less_diff_plus: "P \<le> M \<Longrightarrow> N \<subset># P \<Longrightarrow> M - P + N \<subset># M"
5.309 +  by (drule ordered_cancel_comm_monoid_diff_class.diff_add[symmetric]) (metis union_less_mono2)
5.310 +
5.311 +end
```