more multiset theorems
authorblanchet
Wed Mar 25 17:51:34 2015 +0100 (2015-03-25)
changeset 598136320064f22bb
parent 59812 675d0c692c41
child 59814 2d9cf954a829
more multiset theorems
CONTRIBUTORS
NEWS
src/HOL/Library/Library.thy
src/HOL/Library/Multiset.thy
src/HOL/Library/Multiset_Order.thy
     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.5    Monad_Syntax
     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.17 -lemma mset_less_add_bothsides:
    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.247 +  apply (simp_all add: add.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.289 +  by (metis add.commute add_diff_cancel_right' monoid_add_class.add.left_neutral)
   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.298 +    add.commute)+
   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