cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
authorhaftmann
Fri Jan 22 13:38:28 2010 +0100 (2010-01-22)
changeset 34943e97b22500a5c
parent 34942 d62eddd9e253
child 34944 970e1466028d
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
src/HOL/Library/Multiset.thy
     1.1 --- a/src/HOL/Library/Multiset.thy	Thu Jan 21 09:27:57 2010 +0100
     1.2 +++ b/src/HOL/Library/Multiset.thy	Fri Jan 22 13:38:28 2010 +0100
     1.3 @@ -2,34 +2,21 @@
     1.4      Author:     Tobias Nipkow, Markus Wenzel, Lawrence C Paulson, Norbert Voelker
     1.5  *)
     1.6  
     1.7 -header {* Multisets *}
     1.8 +header {* (Finite) multisets *}
     1.9  
    1.10  theory Multiset
    1.11 -imports List Main
    1.12 +imports Main
    1.13  begin
    1.14  
    1.15  subsection {* The type of multisets *}
    1.16  
    1.17 -typedef 'a multiset = "{f::'a => nat. finite {x . f x > 0}}"
    1.18 +typedef 'a multiset = "{f :: 'a => nat. finite {x. f x > 0}}"
    1.19 +  morphisms count Abs_multiset
    1.20  proof
    1.21    show "(\<lambda>x. 0::nat) \<in> ?multiset" by simp
    1.22  qed
    1.23  
    1.24 -lemmas multiset_typedef [simp] =
    1.25 -    Abs_multiset_inverse Rep_multiset_inverse Rep_multiset
    1.26 -  and [simp] = Rep_multiset_inject [symmetric]
    1.27 -
    1.28 -definition Mempty :: "'a multiset"  ("{#}") where
    1.29 -  [code del]: "{#} = Abs_multiset (\<lambda>a. 0)"
    1.30 -
    1.31 -definition single :: "'a => 'a multiset" where
    1.32 -  [code del]: "single a = Abs_multiset (\<lambda>b. if b = a then 1 else 0)"
    1.33 -
    1.34 -definition count :: "'a multiset => 'a => nat" where
    1.35 -  "count = Rep_multiset"
    1.36 -
    1.37 -definition MCollect :: "'a multiset => ('a => bool) => 'a multiset" where
    1.38 -  "MCollect M P = Abs_multiset (\<lambda>x. if P x then Rep_multiset M x else 0)"
    1.39 +lemmas multiset_typedef = Abs_multiset_inverse count_inverse count
    1.40  
    1.41  abbreviation Melem :: "'a => 'a multiset => bool"  ("(_/ :# _)" [50, 51] 50) where
    1.42    "a :# M == 0 < count M a"
    1.43 @@ -37,142 +24,456 @@
    1.44  notation (xsymbols)
    1.45    Melem (infix "\<in>#" 50)
    1.46  
    1.47 +lemma multiset_eq_conv_count_eq:
    1.48 +  "M = N \<longleftrightarrow> (\<forall>a. count M a = count N a)"
    1.49 +  by (simp only: count_inject [symmetric] expand_fun_eq)
    1.50 +
    1.51 +lemma multi_count_ext:
    1.52 +  "(\<And>x. count A x = count B x) \<Longrightarrow> A = B"
    1.53 +  using multiset_eq_conv_count_eq by auto
    1.54 +
    1.55 +text {*
    1.56 + \medskip Preservation of the representing set @{term multiset}.
    1.57 +*}
    1.58 +
    1.59 +lemma const0_in_multiset:
    1.60 +  "(\<lambda>a. 0) \<in> multiset"
    1.61 +  by (simp add: multiset_def)
    1.62 +
    1.63 +lemma only1_in_multiset:
    1.64 +  "(\<lambda>b. if b = a then n else 0) \<in> multiset"
    1.65 +  by (simp add: multiset_def)
    1.66 +
    1.67 +lemma union_preserves_multiset:
    1.68 +  "M \<in> multiset \<Longrightarrow> N \<in> multiset \<Longrightarrow> (\<lambda>a. M a + N a) \<in> multiset"
    1.69 +  by (simp add: multiset_def)
    1.70 +
    1.71 +lemma diff_preserves_multiset:
    1.72 +  assumes "M \<in> multiset"
    1.73 +  shows "(\<lambda>a. M a - N a) \<in> multiset"
    1.74 +proof -
    1.75 +  have "{x. N x < M x} \<subseteq> {x. 0 < M x}"
    1.76 +    by auto
    1.77 +  with assms show ?thesis
    1.78 +    by (auto simp add: multiset_def intro: finite_subset)
    1.79 +qed
    1.80 +
    1.81 +lemma MCollect_preserves_multiset:
    1.82 +  assumes "M \<in> multiset"
    1.83 +  shows "(\<lambda>x. if P x then M x else 0) \<in> multiset"
    1.84 +proof -
    1.85 +  have "{x. (P x \<longrightarrow> 0 < M x) \<and> P x} \<subseteq> {x. 0 < M x}"
    1.86 +    by auto
    1.87 +  with assms show ?thesis
    1.88 +    by (auto simp add: multiset_def intro: finite_subset)
    1.89 +qed
    1.90 +
    1.91 +lemmas in_multiset = const0_in_multiset only1_in_multiset
    1.92 +  union_preserves_multiset diff_preserves_multiset MCollect_preserves_multiset
    1.93 +
    1.94 +
    1.95 +subsection {* Representing multisets *}
    1.96 +
    1.97 +text {* Multiset comprehension *}
    1.98 +
    1.99 +definition MCollect :: "'a multiset => ('a => bool) => 'a multiset" where
   1.100 +  "MCollect M P = Abs_multiset (\<lambda>x. if P x then count M x else 0)"
   1.101 +
   1.102  syntax
   1.103    "_MCollect" :: "pttrn => 'a multiset => bool => 'a multiset"    ("(1{# _ :# _./ _#})")
   1.104  translations
   1.105    "{#x :# M. P#}" == "CONST MCollect M (\<lambda>x. P)"
   1.106  
   1.107 -definition set_of :: "'a multiset => 'a set" where
   1.108 -  "set_of M = {x. x :# M}"
   1.109  
   1.110 -instantiation multiset :: (type) "{plus, minus, zero, size}" 
   1.111 +text {* Multiset enumeration *}
   1.112 +
   1.113 +instantiation multiset :: (type) "{zero, plus}"
   1.114  begin
   1.115  
   1.116 -definition union_def [code del]:
   1.117 -  "M + N = Abs_multiset (\<lambda>a. Rep_multiset M a + Rep_multiset N a)"
   1.118 -
   1.119 -definition diff_def [code del]:
   1.120 -  "M - N = Abs_multiset (\<lambda>a. Rep_multiset M a - Rep_multiset N a)"
   1.121 +definition Mempty_def:
   1.122 +  "0 = Abs_multiset (\<lambda>a. 0)"
   1.123  
   1.124 -definition Zero_multiset_def [simp]:
   1.125 -  "0 = {#}"
   1.126 +abbreviation Mempty :: "'a multiset" ("{#}") where
   1.127 +  "Mempty \<equiv> 0"
   1.128  
   1.129 -definition size_def:
   1.130 -  "size M = setsum (count M) (set_of M)"
   1.131 +definition union_def:
   1.132 +  "M + N = Abs_multiset (\<lambda>a. count M a + count N a)"
   1.133  
   1.134  instance ..
   1.135  
   1.136  end
   1.137  
   1.138 -definition
   1.139 -  multiset_inter :: "'a multiset \<Rightarrow> 'a multiset \<Rightarrow> 'a multiset"  (infixl "#\<inter>" 70) where
   1.140 -  "multiset_inter A B = A - (A - B)"
   1.141 +definition single :: "'a => 'a multiset" where
   1.142 +  "single a = Abs_multiset (\<lambda>b. if b = a then 1 else 0)"
   1.143  
   1.144 -text {* Multiset Enumeration *}
   1.145  syntax
   1.146    "_multiset" :: "args => 'a multiset"    ("{#(_)#}")
   1.147  translations
   1.148    "{#x, xs#}" == "{#x#} + {#xs#}"
   1.149    "{#x#}" == "CONST single x"
   1.150  
   1.151 -
   1.152 -text {*
   1.153 - \medskip Preservation of the representing set @{term multiset}.
   1.154 -*}
   1.155 +lemma count_empty [simp]: "count {#} a = 0"
   1.156 +  by (simp add: Mempty_def in_multiset multiset_typedef)
   1.157  
   1.158 -lemma const0_in_multiset: "(\<lambda>a. 0) \<in> multiset"
   1.159 -by (simp add: multiset_def)
   1.160 -
   1.161 -lemma only1_in_multiset: "(\<lambda>b. if b = a then 1 else 0) \<in> multiset"
   1.162 -by (simp add: multiset_def)
   1.163 -
   1.164 -lemma union_preserves_multiset:
   1.165 -  "M \<in> multiset ==> N \<in> multiset ==> (\<lambda>a. M a + N a) \<in> multiset"
   1.166 -by (simp add: multiset_def)
   1.167 +lemma count_single [simp]: "count {#b#} a = (if b = a then 1 else 0)"
   1.168 +  by (simp add: single_def in_multiset multiset_typedef)
   1.169  
   1.170  
   1.171 -lemma diff_preserves_multiset:
   1.172 -  "M \<in> multiset ==> (\<lambda>a. M a - N a) \<in> multiset"
   1.173 -apply (simp add: multiset_def)
   1.174 -apply (rule finite_subset)
   1.175 - apply auto
   1.176 -done
   1.177 -
   1.178 -lemma MCollect_preserves_multiset:
   1.179 -  "M \<in> multiset ==> (\<lambda>x. if P x then M x else 0) \<in> multiset"
   1.180 -apply (simp add: multiset_def)
   1.181 -apply (rule finite_subset, auto)
   1.182 -done
   1.183 -
   1.184 -lemmas in_multiset = const0_in_multiset only1_in_multiset
   1.185 -  union_preserves_multiset diff_preserves_multiset MCollect_preserves_multiset
   1.186 -
   1.187 -
   1.188 -subsection {* Algebraic properties *}
   1.189 +subsection {* Basic operations *}
   1.190  
   1.191  subsubsection {* Union *}
   1.192  
   1.193 -lemma union_empty [simp]: "M + {#} = M \<and> {#} + M = M"
   1.194 -by (simp add: union_def Mempty_def in_multiset)
   1.195 -
   1.196 -lemma union_commute: "M + N = N + (M::'a multiset)"
   1.197 -by (simp add: union_def add_ac in_multiset)
   1.198 -
   1.199 -lemma union_assoc: "(M + N) + K = M + (N + (K::'a multiset))"
   1.200 -by (simp add: union_def add_ac in_multiset)
   1.201 +lemma count_union [simp]: "count (M + N) a = count M a + count N a"
   1.202 +  by (simp add: union_def in_multiset multiset_typedef)
   1.203  
   1.204 -lemma union_lcomm: "M + (N + K) = N + (M + (K::'a multiset))"
   1.205 -proof -
   1.206 -  have "M + (N + K) = (N + K) + M" by (rule union_commute)
   1.207 -  also have "\<dots> = N + (K + M)" by (rule union_assoc)
   1.208 -  also have "K + M = M + K" by (rule union_commute)
   1.209 -  finally show ?thesis .
   1.210 -qed
   1.211 -
   1.212 -lemmas union_ac = union_assoc union_commute union_lcomm
   1.213 -
   1.214 -instance multiset :: (type) comm_monoid_add
   1.215 -proof
   1.216 -  fix a b c :: "'a multiset"
   1.217 -  show "(a + b) + c = a + (b + c)" by (rule union_assoc)
   1.218 -  show "a + b = b + a" by (rule union_commute)
   1.219 -  show "0 + a = a" by simp
   1.220 -qed
   1.221 +instance multiset :: (type) cancel_comm_monoid_add proof
   1.222 +qed (simp_all add: multiset_eq_conv_count_eq)
   1.223  
   1.224  
   1.225  subsubsection {* Difference *}
   1.226  
   1.227 +instantiation multiset :: (type) minus
   1.228 +begin
   1.229 +
   1.230 +definition diff_def:
   1.231 +  "M - N = Abs_multiset (\<lambda>a. count M a - count N a)"
   1.232 +
   1.233 +instance ..
   1.234 +
   1.235 +end
   1.236 +
   1.237 +lemma count_diff [simp]: "count (M - N) a = count M a - count N a"
   1.238 +  by (simp add: diff_def in_multiset multiset_typedef)
   1.239 +
   1.240  lemma diff_empty [simp]: "M - {#} = M \<and> {#} - M = {#}"
   1.241 -by (simp add: Mempty_def diff_def in_multiset)
   1.242 +  by (simp add: Mempty_def diff_def in_multiset multiset_typedef)
   1.243  
   1.244  lemma diff_union_inverse2 [simp]: "M + {#a#} - {#a#} = M"
   1.245 -by (simp add: union_def diff_def in_multiset)
   1.246 +  by (rule multi_count_ext)
   1.247 +    (auto simp del: count_single simp add: union_def diff_def in_multiset multiset_typedef)
   1.248  
   1.249  lemma diff_cancel: "A - A = {#}"
   1.250 -by (simp add: diff_def Mempty_def)
   1.251 +  by (rule multi_count_ext) simp
   1.252 +
   1.253 +lemma insert_DiffM:
   1.254 +  "x \<in># M \<Longrightarrow> {#x#} + (M - {#x#}) = M"
   1.255 +  by (clarsimp simp: multiset_eq_conv_count_eq)
   1.256 +
   1.257 +lemma insert_DiffM2 [simp]:
   1.258 +  "x \<in># M \<Longrightarrow> M - {#x#} + {#x#} = M"
   1.259 +  by (clarsimp simp: multiset_eq_conv_count_eq)
   1.260 +
   1.261 +lemma diff_right_commute:
   1.262 +  "(M::'a multiset) - N - Q = M - Q - N"
   1.263 +  by (auto simp add: multiset_eq_conv_count_eq)
   1.264 +
   1.265 +lemma diff_union_swap:
   1.266 +  "a \<noteq> b \<Longrightarrow> M - {#a#} + {#b#} = M + {#b#} - {#a#}"
   1.267 +  by (auto simp add: multiset_eq_conv_count_eq)
   1.268 +
   1.269 +lemma diff_union_single_conv:
   1.270 +  "a \<in># J \<Longrightarrow> I + J - {#a#} = I + (J - {#a#})"
   1.271 +  by (simp add: multiset_eq_conv_count_eq)
   1.272  
   1.273  
   1.274 -subsubsection {* Count of elements *}
   1.275 +subsubsection {* Intersection *}
   1.276 +
   1.277 +definition multiset_inter :: "'a multiset \<Rightarrow> 'a multiset \<Rightarrow> 'a multiset" (infixl "#\<inter>" 70) where
   1.278 +  "multiset_inter A B = A - (A - B)"
   1.279 +
   1.280 +lemma multiset_inter_count:
   1.281 +  "count (A #\<inter> B) x = min (count A x) (count B x)"
   1.282 +  by (simp add: multiset_inter_def multiset_typedef)
   1.283  
   1.284 -lemma count_empty [simp]: "count {#} a = 0"
   1.285 -by (simp add: count_def Mempty_def in_multiset)
   1.286 +lemma multiset_inter_commute: "A #\<inter> B = B #\<inter> A"
   1.287 +  by (rule multi_count_ext) (simp add: multiset_inter_count)
   1.288 +
   1.289 +lemma multiset_inter_assoc: "A #\<inter> (B #\<inter> C) = A #\<inter> B #\<inter> C"
   1.290 +  by (rule multi_count_ext) (simp add: multiset_inter_count)
   1.291 +
   1.292 +lemma multiset_inter_left_commute: "A #\<inter> (B #\<inter> C) = B #\<inter> (A #\<inter> C)"
   1.293 +  by (rule multi_count_ext) (simp add: multiset_inter_count)
   1.294  
   1.295 -lemma count_single [simp]: "count {#b#} a = (if b = a then 1 else 0)"
   1.296 -by (simp add: count_def single_def in_multiset)
   1.297 +lemmas multiset_inter_ac =
   1.298 +  multiset_inter_commute
   1.299 +  multiset_inter_assoc
   1.300 +  multiset_inter_left_commute
   1.301 +
   1.302 +lemma multiset_inter_single: "a \<noteq> b \<Longrightarrow> {#a#} #\<inter> {#b#} = {#}"
   1.303 +  by (rule multi_count_ext) (auto simp add: multiset_inter_count)
   1.304  
   1.305 -lemma count_union [simp]: "count (M + N) a = count M a + count N a"
   1.306 -by (simp add: count_def union_def in_multiset)
   1.307 +lemma multiset_union_diff_commute:
   1.308 +  assumes "B #\<inter> C = {#}"
   1.309 +  shows "A + B - C = A - C + B"
   1.310 +proof (rule multi_count_ext)
   1.311 +  fix x
   1.312 +  from assms have "min (count B x) (count C x) = 0"
   1.313 +    by (auto simp add: multiset_inter_count multiset_eq_conv_count_eq)
   1.314 +  then have "count B x = 0 \<or> count C x = 0"
   1.315 +    by auto
   1.316 +  then show "count (A + B - C) x = count (A - C + B) x"
   1.317 +    by auto
   1.318 +qed
   1.319  
   1.320 -lemma count_diff [simp]: "count (M - N) a = count M a - count N a"
   1.321 -by (simp add: count_def diff_def in_multiset)
   1.322 +
   1.323 +subsubsection {* Comprehension (filter) *}
   1.324  
   1.325  lemma count_MCollect [simp]:
   1.326    "count {# x:#M. P x #} a = (if P a then count M a else 0)"
   1.327 -by (simp add: count_def MCollect_def in_multiset)
   1.328 +  by (simp add: MCollect_def in_multiset multiset_typedef)
   1.329 +
   1.330 +lemma MCollect_empty [simp]: "MCollect {#} P = {#}"
   1.331 +  by (rule multi_count_ext) simp
   1.332 +
   1.333 +lemma MCollect_single [simp]:
   1.334 +  "MCollect {#x#} P = (if P x then {#x#} else {#})"
   1.335 +  by (rule multi_count_ext) simp
   1.336 +
   1.337 +lemma MCollect_union [simp]:
   1.338 +  "MCollect (M + N) f = MCollect M f + MCollect N f"
   1.339 +  by (rule multi_count_ext) simp
   1.340 +
   1.341 +
   1.342 +subsubsection {* Equality of multisets *}
   1.343 +
   1.344 +lemma single_not_empty [simp]: "{#a#} \<noteq> {#} \<and> {#} \<noteq> {#a#}"
   1.345 +  by (simp add: multiset_eq_conv_count_eq)
   1.346 +
   1.347 +lemma single_eq_single [simp]: "{#a#} = {#b#} \<longleftrightarrow> a = b"
   1.348 +  by (auto simp add: multiset_eq_conv_count_eq)
   1.349 +
   1.350 +lemma union_eq_empty [iff]: "M + N = {#} \<longleftrightarrow> M = {#} \<and> N = {#}"
   1.351 +  by (auto simp add: multiset_eq_conv_count_eq)
   1.352 +
   1.353 +lemma empty_eq_union [iff]: "{#} = M + N \<longleftrightarrow> M = {#} \<and> N = {#}"
   1.354 +  by (auto simp add: multiset_eq_conv_count_eq)
   1.355 +
   1.356 +lemma multi_self_add_other_not_self [simp]: "M = M + {#x#} \<longleftrightarrow> False"
   1.357 +  by (auto simp add: multiset_eq_conv_count_eq)
   1.358 +
   1.359 +lemma diff_single_trivial:
   1.360 +  "\<not> x \<in># M \<Longrightarrow> M - {#x#} = M"
   1.361 +  by (auto simp add: multiset_eq_conv_count_eq)
   1.362 +
   1.363 +lemma diff_single_eq_union:
   1.364 +  "x \<in># M \<Longrightarrow> M - {#x#} = N \<longleftrightarrow> M = N + {#x#}"
   1.365 +  by auto
   1.366 +
   1.367 +lemma union_single_eq_diff:
   1.368 +  "M + {#x#} = N \<Longrightarrow> M = N - {#x#}"
   1.369 +  by (auto dest: sym)
   1.370 +
   1.371 +lemma union_single_eq_member:
   1.372 +  "M + {#x#} = N \<Longrightarrow> x \<in># N"
   1.373 +  by auto
   1.374 +
   1.375 +lemma union_is_single:
   1.376 +  "M + N = {#a#} \<longleftrightarrow> M = {#a#} \<and> N={#} \<or> M = {#} \<and> N = {#a#}" (is "?lhs = ?rhs")
   1.377 +proof
   1.378 +  assume ?rhs then show ?lhs by auto
   1.379 +next
   1.380 +  assume ?lhs
   1.381 +  then have "\<And>b. count (M + N) b = (if b = a then 1 else 0)" by auto
   1.382 +  then have *: "\<And>b. count M b + count N b = (if b = a then 1 else 0)" by auto
   1.383 +  then have "count M a + count N a = 1" by auto
   1.384 +  then have **: "count M a = 1 \<and> count N a = 0 \<or> count M a = 0 \<and> count N a = 1"
   1.385 +    by auto
   1.386 +  from * have "\<And>b. b \<noteq> a \<Longrightarrow> count M b + count N b = 0" by auto
   1.387 +  then have ***: "\<And>b. b \<noteq> a \<Longrightarrow> count M b = 0 \<and> count N b = 0" by auto
   1.388 +  from ** and *** have
   1.389 +    "(\<forall>b. count M b = (if b = a then 1 else 0) \<and> count N b = 0) \<or>
   1.390 +      (\<forall>b. count M b = 0 \<and> count N b = (if b = a then 1 else 0))"
   1.391 +    by auto
   1.392 +  then have
   1.393 +    "(\<forall>b. count M b = (if b = a then 1 else 0)) \<and> (\<forall>b. count N b = 0) \<or>
   1.394 +      (\<forall>b. count M b = 0) \<and> (\<forall>b. count N b = (if b = a then 1 else 0))"
   1.395 +    by auto
   1.396 +  then show ?rhs by (auto simp add: multiset_eq_conv_count_eq)
   1.397 +qed
   1.398 +
   1.399 +lemma single_is_union:
   1.400 +  "{#a#} = M + N \<longleftrightarrow> {#a#} = M \<and> N = {#} \<or> M = {#} \<and> {#a#} = N"
   1.401 +  by (auto simp add: eq_commute [of "{#a#}" "M + N"] union_is_single)
   1.402 +
   1.403 +lemma add_eq_conv_diff:
   1.404 +  "M + {#a#} = N + {#b#} \<longleftrightarrow> M = N \<and> a = b \<or> M = N - {#a#} + {#b#} \<and> N = M - {#b#} + {#a#}"  (is "?lhs = ?rhs")
   1.405 +proof
   1.406 +  assume ?rhs then show ?lhs
   1.407 +  by (auto simp add: add_assoc add_commute [of "{#b#}"])
   1.408 +    (drule sym, simp add: add_assoc [symmetric])
   1.409 +next
   1.410 +  assume ?lhs
   1.411 +  show ?rhs
   1.412 +  proof (cases "a = b")
   1.413 +    case True with `?lhs` show ?thesis by simp
   1.414 +  next
   1.415 +    case False
   1.416 +    from `?lhs` have "a \<in># N + {#b#}" by (rule union_single_eq_member)
   1.417 +    with False have "a \<in># N" by auto
   1.418 +    moreover from `?lhs` have "M = N + {#b#} - {#a#}" by (rule union_single_eq_diff)
   1.419 +    moreover note False
   1.420 +    ultimately show ?thesis by (auto simp add: diff_right_commute [of _ "{#a#}"] diff_union_swap)
   1.421 +  qed
   1.422 +qed
   1.423 +
   1.424 +lemma insert_noteq_member: 
   1.425 +  assumes BC: "B + {#b#} = C + {#c#}"
   1.426 +   and bnotc: "b \<noteq> c"
   1.427 +  shows "c \<in># B"
   1.428 +proof -
   1.429 +  have "c \<in># C + {#c#}" by simp
   1.430 +  have nc: "\<not> c \<in># {#b#}" using bnotc by simp
   1.431 +  then have "c \<in># B + {#b#}" using BC by simp
   1.432 +  then show "c \<in># B" using nc by simp
   1.433 +qed
   1.434 +
   1.435 +lemma add_eq_conv_ex:
   1.436 +  "(M + {#a#} = N + {#b#}) =
   1.437 +    (M = N \<and> a = b \<or> (\<exists>K. M = K + {#b#} \<and> N = K + {#a#}))"
   1.438 +  by (auto simp add: add_eq_conv_diff)
   1.439 +
   1.440 +
   1.441 +subsubsection {* Pointwise ordering induced by count *}
   1.442 +
   1.443 +definition mset_le :: "'a multiset \<Rightarrow> 'a multiset \<Rightarrow> bool"  (infix "\<le>#" 50) where
   1.444 +  "A \<le># B \<longleftrightarrow> (\<forall>a. count A a \<le> count B a)"
   1.445 +
   1.446 +definition mset_less :: "'a multiset \<Rightarrow> 'a multiset \<Rightarrow> bool"  (infix "<#" 50) where
   1.447 +  "A <# B \<longleftrightarrow> A \<le># B \<and> A \<noteq> B"
   1.448 +
   1.449 +notation mset_le  (infix "\<subseteq>#" 50)
   1.450 +notation mset_less  (infix "\<subset>#" 50)
   1.451 +
   1.452 +lemma mset_less_eqI:
   1.453 +  "(\<And>x. count A x \<le> count B x) \<Longrightarrow> A \<subseteq># B"
   1.454 +  by (simp add: mset_le_def)
   1.455 +
   1.456 +lemma mset_le_refl[simp]: "A \<le># A"
   1.457 +unfolding mset_le_def by auto
   1.458 +
   1.459 +lemma mset_le_trans: "A \<le># B \<Longrightarrow> B \<le># C \<Longrightarrow> A \<le># C"
   1.460 +unfolding mset_le_def by (fast intro: order_trans)
   1.461 +
   1.462 +lemma mset_le_antisym: "A \<le># B \<Longrightarrow> B \<le># A \<Longrightarrow> A = B"
   1.463 +apply (unfold mset_le_def)
   1.464 +apply (rule multiset_eq_conv_count_eq [THEN iffD2])
   1.465 +apply (blast intro: order_antisym)
   1.466 +done
   1.467 +
   1.468 +lemma mset_le_exists_conv: "(A \<le># B) = (\<exists>C. B = A + C)"
   1.469 +apply (unfold mset_le_def, rule iffI, rule_tac x = "B - A" in exI)
   1.470 +apply (auto intro: multiset_eq_conv_count_eq [THEN iffD2])
   1.471 +done
   1.472 +
   1.473 +lemma mset_le_mono_add_right_cancel[simp]: "(A + C \<le># B + C) = (A \<le># B)"
   1.474 +unfolding mset_le_def by auto
   1.475 +
   1.476 +lemma mset_le_mono_add_left_cancel[simp]: "(C + A \<le># C + B) = (A \<le># B)"
   1.477 +unfolding mset_le_def by auto
   1.478 +
   1.479 +lemma mset_le_mono_add: "\<lbrakk> A \<le># B; C \<le># D \<rbrakk> \<Longrightarrow> A + C \<le># B + D"
   1.480 +apply (unfold mset_le_def)
   1.481 +apply auto
   1.482 +apply (erule_tac x = a in allE)+
   1.483 +apply auto
   1.484 +done
   1.485 +
   1.486 +lemma mset_le_add_left[simp]: "A \<le># A + B"
   1.487 +unfolding mset_le_def by auto
   1.488 +
   1.489 +lemma mset_le_add_right[simp]: "B \<le># A + B"
   1.490 +unfolding mset_le_def by auto
   1.491 +
   1.492 +lemma mset_le_single: "a :# B \<Longrightarrow> {#a#} \<le># B"
   1.493 +by (simp add: mset_le_def)
   1.494 +
   1.495 +lemma multiset_diff_union_assoc: "C \<le># B \<Longrightarrow> A + B - C = A + (B - C)"
   1.496 +by (simp add: multiset_eq_conv_count_eq mset_le_def)
   1.497 +
   1.498 +lemma mset_le_multiset_union_diff_commute:
   1.499 +assumes "B \<le># A"
   1.500 +shows "A - B + C = A + C - B"
   1.501 +proof -
   1.502 +  from mset_le_exists_conv [of "B" "A"] assms have "\<exists>D. A = B + D" ..
   1.503 +  from this obtain D where "A = B + D" ..
   1.504 +  then show ?thesis
   1.505 +    apply simp
   1.506 +    apply (subst add_commute)
   1.507 +    apply (subst multiset_diff_union_assoc)
   1.508 +    apply simp
   1.509 +    apply (simp add: diff_cancel)
   1.510 +    apply (subst add_assoc)
   1.511 +    apply (subst add_commute [of "B" _])
   1.512 +    apply (subst multiset_diff_union_assoc)
   1.513 +    apply simp
   1.514 +    apply (simp add: diff_cancel)
   1.515 +    done
   1.516 +qed
   1.517 +
   1.518 +interpretation mset_order: order "op \<le>#" "op <#"
   1.519 +proof qed (auto intro: order.intro mset_le_refl mset_le_antisym
   1.520 +  mset_le_trans simp: mset_less_def)
   1.521 +
   1.522 +interpretation mset_order_cancel_semigroup:
   1.523 +  pordered_cancel_ab_semigroup_add "op +" "op \<le>#" "op <#"
   1.524 +proof qed (erule mset_le_mono_add [OF mset_le_refl])
   1.525 +
   1.526 +interpretation mset_order_semigroup_cancel:
   1.527 +  pordered_ab_semigroup_add_imp_le "op +" "op \<le>#" "op <#"
   1.528 +proof qed simp
   1.529 +
   1.530 +lemma mset_lessD: "A \<subset># B \<Longrightarrow> x \<in># A \<Longrightarrow> x \<in># B"
   1.531 +apply (clarsimp simp: mset_le_def mset_less_def)
   1.532 +apply (erule_tac x=x in allE)
   1.533 +apply auto
   1.534 +done
   1.535 +
   1.536 +lemma mset_leD: "A \<subseteq># B \<Longrightarrow> x \<in># A \<Longrightarrow> x \<in># B"
   1.537 +apply (clarsimp simp: mset_le_def mset_less_def)
   1.538 +apply (erule_tac x = x in allE)
   1.539 +apply auto
   1.540 +done
   1.541 +  
   1.542 +lemma mset_less_insertD: "(A + {#x#} \<subset># B) \<Longrightarrow> (x \<in># B \<and> A \<subset># B)"
   1.543 +apply (rule conjI)
   1.544 + apply (simp add: mset_lessD)
   1.545 +apply (clarsimp simp: mset_le_def mset_less_def)
   1.546 +apply safe
   1.547 + apply (erule_tac x = a in allE)
   1.548 + apply (auto split: split_if_asm)
   1.549 +done
   1.550 +
   1.551 +lemma mset_le_insertD: "(A + {#x#} \<subseteq># B) \<Longrightarrow> (x \<in># B \<and> A \<subseteq># B)"
   1.552 +apply (rule conjI)
   1.553 + apply (simp add: mset_leD)
   1.554 +apply (force simp: mset_le_def mset_less_def split: split_if_asm)
   1.555 +done
   1.556 +
   1.557 +lemma mset_less_of_empty[simp]: "A \<subset># {#} \<longleftrightarrow> False"
   1.558 +  by (auto simp add: mset_less_def mset_le_def multiset_eq_conv_count_eq)
   1.559 +
   1.560 +lemma multi_psub_of_add_self[simp]: "A \<subset># A + {#x#}"
   1.561 +by (auto simp: mset_le_def mset_less_def)
   1.562 +
   1.563 +lemma multi_psub_self[simp]: "A \<subset># A = False"
   1.564 +by (auto simp: mset_le_def mset_less_def)
   1.565 +
   1.566 +lemma mset_less_add_bothsides:
   1.567 +  "T + {#x#} \<subset># S + {#x#} \<Longrightarrow> T \<subset># S"
   1.568 +by (auto simp: mset_le_def mset_less_def)
   1.569 +
   1.570 +lemma mset_less_empty_nonempty: "({#} \<subset># S) = (S \<noteq> {#})"
   1.571 +by (auto simp: mset_le_def mset_less_def)
   1.572 +
   1.573 +lemma mset_less_diff_self: "c \<in># B \<Longrightarrow> B - {#c#} \<subset># B"
   1.574 +  by (auto simp: mset_le_def mset_less_def multiset_eq_conv_count_eq)
   1.575  
   1.576  
   1.577  subsubsection {* Set of elements *}
   1.578  
   1.579 +definition set_of :: "'a multiset => 'a set" where
   1.580 +  "set_of M = {x. x :# M}"
   1.581 +
   1.582  lemma set_of_empty [simp]: "set_of {#} = {}"
   1.583  by (simp add: set_of_def)
   1.584  
   1.585 @@ -183,7 +484,7 @@
   1.586  by (auto simp add: set_of_def)
   1.587  
   1.588  lemma set_of_eq_empty_iff [simp]: "(set_of M = {}) = (M = {#})"
   1.589 -by (auto simp: set_of_def Mempty_def in_multiset count_def expand_fun_eq [where f="Rep_multiset M"])
   1.590 +by (auto simp add: set_of_def multiset_eq_conv_count_eq)
   1.591  
   1.592  lemma mem_set_of_iff [simp]: "(x \<in> set_of M) = (x :# M)"
   1.593  by (auto simp add: set_of_def)
   1.594 @@ -191,18 +492,28 @@
   1.595  lemma set_of_MCollect [simp]: "set_of {# x:#M. P x #} = set_of M \<inter> {x. P x}"
   1.596  by (auto simp add: set_of_def)
   1.597  
   1.598 +lemma finite_set_of [iff]: "finite (set_of M)"
   1.599 +  using count [of M] by (simp add: multiset_def set_of_def)
   1.600 +
   1.601  
   1.602  subsubsection {* Size *}
   1.603  
   1.604 +instantiation multiset :: (type) size
   1.605 +begin
   1.606 +
   1.607 +definition size_def:
   1.608 +  "size M = setsum (count M) (set_of M)"
   1.609 +
   1.610 +instance ..
   1.611 +
   1.612 +end
   1.613 +
   1.614  lemma size_empty [simp]: "size {#} = 0"
   1.615  by (simp add: size_def)
   1.616  
   1.617  lemma size_single [simp]: "size {#b#} = 1"
   1.618  by (simp add: size_def)
   1.619  
   1.620 -lemma finite_set_of [iff]: "finite (set_of M)"
   1.621 -using Rep_multiset [of M] by (simp add: multiset_def set_of_def count_def)
   1.622 -
   1.623  lemma setsum_count_Int:
   1.624    "finite A ==> setsum (count N) (A \<inter> set_of N) = setsum (count N) A"
   1.625  apply (induct rule: finite_induct)
   1.626 @@ -221,9 +532,7 @@
   1.627  done
   1.628  
   1.629  lemma size_eq_0_iff_empty [iff]: "(size M = 0) = (M = {#})"
   1.630 -apply (unfold size_def Mempty_def count_def, auto simp: in_multiset)
   1.631 -apply (simp add: set_of_def count_def in_multiset expand_fun_eq)
   1.632 -done
   1.633 +by (auto simp add: size_def multiset_eq_conv_count_eq)
   1.634  
   1.635  lemma nonempty_has_size: "(S \<noteq> {#}) = (0 < size S)"
   1.636  by (metis gr0I gr_implies_not0 size_empty size_eq_0_iff_empty)
   1.637 @@ -234,149 +543,16 @@
   1.638  apply auto
   1.639  done
   1.640  
   1.641 -
   1.642 -subsubsection {* Equality of multisets *}
   1.643 -
   1.644 -lemma multiset_eq_conv_count_eq: "(M = N) = (\<forall>a. count M a = count N a)"
   1.645 -by (simp add: count_def expand_fun_eq)
   1.646 -
   1.647 -lemma single_not_empty [simp]: "{#a#} \<noteq> {#} \<and> {#} \<noteq> {#a#}"
   1.648 -by (simp add: single_def Mempty_def in_multiset expand_fun_eq)
   1.649 -
   1.650 -lemma single_eq_single [simp]: "({#a#} = {#b#}) = (a = b)"
   1.651 -by (auto simp add: single_def in_multiset expand_fun_eq)
   1.652 -
   1.653 -lemma union_eq_empty [iff]: "(M + N = {#}) = (M = {#} \<and> N = {#})"
   1.654 -by (auto simp add: union_def Mempty_def in_multiset expand_fun_eq)
   1.655 -
   1.656 -lemma empty_eq_union [iff]: "({#} = M + N) = (M = {#} \<and> N = {#})"
   1.657 -by (auto simp add: union_def Mempty_def in_multiset expand_fun_eq)
   1.658 -
   1.659 -lemma union_right_cancel [simp]: "(M + K = N + K) = (M = (N::'a multiset))"
   1.660 -by (simp add: union_def in_multiset expand_fun_eq)
   1.661 -
   1.662 -lemma union_left_cancel [simp]: "(K + M = K + N) = (M = (N::'a multiset))"
   1.663 -by (simp add: union_def in_multiset expand_fun_eq)
   1.664 -
   1.665 -lemma union_is_single:
   1.666 -  "(M + N = {#a#}) = (M = {#a#} \<and> N={#} \<or> M = {#} \<and> N = {#a#})"
   1.667 -apply (simp add: Mempty_def single_def union_def in_multiset add_is_1 expand_fun_eq)
   1.668 -apply blast
   1.669 -done
   1.670 -
   1.671 -lemma single_is_union:
   1.672 -  "({#a#} = M + N) \<longleftrightarrow> ({#a#} = M \<and> N = {#} \<or> M = {#} \<and> {#a#} = N)"
   1.673 -apply (unfold Mempty_def single_def union_def)
   1.674 -apply (simp add: add_is_1 one_is_add in_multiset expand_fun_eq)
   1.675 -apply (blast dest: sym)
   1.676 -done
   1.677 -
   1.678 -lemma add_eq_conv_diff:
   1.679 -  "(M + {#a#} = N + {#b#}) =
   1.680 -   (M = N \<and> a = b \<or> M = N - {#a#} + {#b#} \<and> N = M - {#b#} + {#a#})"
   1.681 -using [[simproc del: neq]]
   1.682 -apply (unfold single_def union_def diff_def)
   1.683 -apply (simp (no_asm) add: in_multiset expand_fun_eq)
   1.684 -apply (rule conjI, force, safe, simp_all)
   1.685 -apply (simp add: eq_sym_conv)
   1.686 -done
   1.687 -
   1.688 -declare Rep_multiset_inject [symmetric, simp del]
   1.689 -
   1.690 -instance multiset :: (type) cancel_ab_semigroup_add
   1.691 -proof
   1.692 -  fix a b c :: "'a multiset"
   1.693 -  show "a + b = a + c \<Longrightarrow> b = c" by simp
   1.694 +lemma size_eq_Suc_imp_eq_union:
   1.695 +  assumes "size M = Suc n"
   1.696 +  shows "\<exists>a N. M = N + {#a#}"
   1.697 +proof -
   1.698 +  from assms obtain a where "a \<in># M"
   1.699 +    by (erule size_eq_Suc_imp_elem [THEN exE])
   1.700 +  then have "M = M - {#a#} + {#a#}" by simp
   1.701 +  then show ?thesis by blast
   1.702  qed
   1.703  
   1.704 -lemma insert_DiffM:
   1.705 -  "x \<in># M \<Longrightarrow> {#x#} + (M - {#x#}) = M"
   1.706 -by (clarsimp simp: multiset_eq_conv_count_eq)
   1.707 -
   1.708 -lemma insert_DiffM2[simp]:
   1.709 -  "x \<in># M \<Longrightarrow> M - {#x#} + {#x#} = M"
   1.710 -by (clarsimp simp: multiset_eq_conv_count_eq)
   1.711 -
   1.712 -lemma multi_union_self_other_eq: 
   1.713 -  "(A::'a multiset) + X = A + Y \<Longrightarrow> X = Y"
   1.714 -by (induct A arbitrary: X Y) auto
   1.715 -
   1.716 -lemma multi_self_add_other_not_self[simp]: "(A = A + {#x#}) = False"
   1.717 -by (metis single_not_empty union_empty union_left_cancel)
   1.718 -
   1.719 -lemma insert_noteq_member: 
   1.720 -  assumes BC: "B + {#b#} = C + {#c#}"
   1.721 -   and bnotc: "b \<noteq> c"
   1.722 -  shows "c \<in># B"
   1.723 -proof -
   1.724 -  have "c \<in># C + {#c#}" by simp
   1.725 -  have nc: "\<not> c \<in># {#b#}" using bnotc by simp
   1.726 -  then have "c \<in># B + {#b#}" using BC by simp
   1.727 -  then show "c \<in># B" using nc by simp
   1.728 -qed
   1.729 -
   1.730 -
   1.731 -lemma add_eq_conv_ex:
   1.732 -  "(M + {#a#} = N + {#b#}) =
   1.733 -    (M = N \<and> a = b \<or> (\<exists>K. M = K + {#b#} \<and> N = K + {#a#}))"
   1.734 -by (auto simp add: add_eq_conv_diff)
   1.735 -
   1.736 -
   1.737 -lemma empty_multiset_count:
   1.738 -  "(\<forall>x. count A x = 0) = (A = {#})"
   1.739 -by (metis count_empty multiset_eq_conv_count_eq)
   1.740 -
   1.741 -
   1.742 -subsubsection {* Intersection *}
   1.743 -
   1.744 -lemma multiset_inter_count:
   1.745 -  "count (A #\<inter> B) x = min (count A x) (count B x)"
   1.746 -by (simp add: multiset_inter_def)
   1.747 -
   1.748 -lemma multiset_inter_commute: "A #\<inter> B = B #\<inter> A"
   1.749 -by (simp add: multiset_eq_conv_count_eq multiset_inter_count
   1.750 -    min_max.inf_commute)
   1.751 -
   1.752 -lemma multiset_inter_assoc: "A #\<inter> (B #\<inter> C) = A #\<inter> B #\<inter> C"
   1.753 -by (simp add: multiset_eq_conv_count_eq multiset_inter_count
   1.754 -    min_max.inf_assoc)
   1.755 -
   1.756 -lemma multiset_inter_left_commute: "A #\<inter> (B #\<inter> C) = B #\<inter> (A #\<inter> C)"
   1.757 -by (simp add: multiset_eq_conv_count_eq multiset_inter_count min_def)
   1.758 -
   1.759 -lemmas multiset_inter_ac =
   1.760 -  multiset_inter_commute
   1.761 -  multiset_inter_assoc
   1.762 -  multiset_inter_left_commute
   1.763 -
   1.764 -lemma multiset_inter_single: "a \<noteq> b \<Longrightarrow> {#a#} #\<inter> {#b#} = {#}"
   1.765 -by (simp add: multiset_eq_conv_count_eq multiset_inter_count)
   1.766 -
   1.767 -lemma multiset_union_diff_commute: "B #\<inter> C = {#} \<Longrightarrow> A + B - C = A - C + B"
   1.768 -apply (simp add: multiset_eq_conv_count_eq multiset_inter_count
   1.769 -    split: split_if_asm)
   1.770 -apply clarsimp
   1.771 -apply (erule_tac x = a in allE)
   1.772 -apply auto
   1.773 -done
   1.774 -
   1.775 -
   1.776 -subsubsection {* Comprehension (filter) *}
   1.777 -
   1.778 -lemma MCollect_empty [simp]: "MCollect {#} P = {#}"
   1.779 -by (simp add: MCollect_def Mempty_def Abs_multiset_inject
   1.780 -    in_multiset expand_fun_eq)
   1.781 -
   1.782 -lemma MCollect_single [simp]:
   1.783 -  "MCollect {#x#} P = (if P x then {#x#} else {#})"
   1.784 -by (simp add: MCollect_def Mempty_def single_def Abs_multiset_inject
   1.785 -    in_multiset expand_fun_eq)
   1.786 -
   1.787 -lemma MCollect_union [simp]:
   1.788 -  "MCollect (M+N) f = MCollect M f + MCollect N f"
   1.789 -by (simp add: MCollect_def union_def Abs_multiset_inject
   1.790 -    in_multiset expand_fun_eq)
   1.791 -
   1.792  
   1.793  subsection {* Induction and case splits *}
   1.794  
   1.795 @@ -434,17 +610,20 @@
   1.796  shows "P M"
   1.797  proof -
   1.798    note defns = union_def single_def Mempty_def
   1.799 +  note add' = add [unfolded defns, simplified]
   1.800 +  have aux: "\<And>a::'a. count (Abs_multiset (\<lambda>b. if b = a then 1 else 0)) =
   1.801 +    (\<lambda>b. if b = a then 1 else 0)" by (simp add: Abs_multiset_inverse in_multiset) 
   1.802    show ?thesis
   1.803 -    apply (rule Rep_multiset_inverse [THEN subst])
   1.804 -    apply (rule Rep_multiset [THEN rep_multiset_induct])
   1.805 +    apply (rule count_inverse [THEN subst])
   1.806 +    apply (rule count [THEN rep_multiset_induct])
   1.807       apply (rule empty [unfolded defns])
   1.808      apply (subgoal_tac "f(b := f b + 1) = (\<lambda>a. f a + (if a=b then 1 else 0))")
   1.809       prefer 2
   1.810       apply (simp add: expand_fun_eq)
   1.811      apply (erule ssubst)
   1.812      apply (erule Abs_multiset_inverse [THEN subst])
   1.813 -    apply (drule add [unfolded defns, simplified])
   1.814 -    apply(simp add:in_multiset)
   1.815 +    apply (drule add')
   1.816 +    apply (simp add: aux)
   1.817      done
   1.818  qed
   1.819  
   1.820 @@ -470,18 +649,379 @@
   1.821  apply (rule_tac x="M - {#x#}" in exI, simp)
   1.822  done
   1.823  
   1.824 +lemma multi_drop_mem_not_eq: "c \<in># B \<Longrightarrow> B - {#c#} \<noteq> B"
   1.825 +by (cases "B = {#}") (auto dest: multi_member_split)
   1.826 +
   1.827  lemma multiset_partition: "M = {# x:#M. P x #} + {# x:#M. \<not> P x #}"
   1.828  apply (subst multiset_eq_conv_count_eq)
   1.829  apply auto
   1.830  done
   1.831  
   1.832 -declare multiset_typedef [simp del]
   1.833 +lemma mset_less_size: "A \<subset># B \<Longrightarrow> size A < size B"
   1.834 +proof (induct A arbitrary: B)
   1.835 +  case (empty M)
   1.836 +  then have "M \<noteq> {#}" by (simp add: mset_less_empty_nonempty)
   1.837 +  then obtain M' x where "M = M' + {#x#}" 
   1.838 +    by (blast dest: multi_nonempty_split)
   1.839 +  then show ?case by simp
   1.840 +next
   1.841 +  case (add S x T)
   1.842 +  have IH: "\<And>B. S \<subset># B \<Longrightarrow> size S < size B" by fact
   1.843 +  have SxsubT: "S + {#x#} \<subset># T" by fact
   1.844 +  then have "x \<in># T" and "S \<subset># T" by (auto dest: mset_less_insertD)
   1.845 +  then obtain T' where T: "T = T' + {#x#}" 
   1.846 +    by (blast dest: multi_member_split)
   1.847 +  then have "S \<subset># T'" using SxsubT 
   1.848 +    by (blast intro: mset_less_add_bothsides)
   1.849 +  then have "size S < size T'" using IH by simp
   1.850 +  then show ?case using T by simp
   1.851 +qed
   1.852 +
   1.853 +
   1.854 +subsubsection {* Strong induction and subset induction for multisets *}
   1.855 +
   1.856 +text {* Well-foundedness of proper subset operator: *}
   1.857 +
   1.858 +text {* proper multiset subset *}
   1.859 +
   1.860 +definition
   1.861 +  mset_less_rel :: "('a multiset * 'a multiset) set" where
   1.862 +  "mset_less_rel = {(A,B). A \<subset># B}"
   1.863  
   1.864 -lemma multi_drop_mem_not_eq: "c \<in># B \<Longrightarrow> B - {#c#} \<noteq> B"
   1.865 -by (cases "B = {#}") (auto dest: multi_member_split)
   1.866 +lemma multiset_add_sub_el_shuffle: 
   1.867 +  assumes "c \<in># B" and "b \<noteq> c" 
   1.868 +  shows "B - {#c#} + {#b#} = B + {#b#} - {#c#}"
   1.869 +proof -
   1.870 +  from `c \<in># B` obtain A where B: "B = A + {#c#}" 
   1.871 +    by (blast dest: multi_member_split)
   1.872 +  have "A + {#b#} = A + {#b#} + {#c#} - {#c#}" by simp
   1.873 +  then have "A + {#b#} = A + {#c#} + {#b#} - {#c#}" 
   1.874 +    by (simp add: add_ac)
   1.875 +  then show ?thesis using B by simp
   1.876 +qed
   1.877 +
   1.878 +lemma wf_mset_less_rel: "wf mset_less_rel"
   1.879 +apply (unfold mset_less_rel_def)
   1.880 +apply (rule wf_measure [THEN wf_subset, where f1=size])
   1.881 +apply (clarsimp simp: measure_def inv_image_def mset_less_size)
   1.882 +done
   1.883 +
   1.884 +text {* The induction rules: *}
   1.885 +
   1.886 +lemma full_multiset_induct [case_names less]:
   1.887 +assumes ih: "\<And>B. \<forall>A. A \<subset># B \<longrightarrow> P A \<Longrightarrow> P B"
   1.888 +shows "P B"
   1.889 +apply (rule wf_mset_less_rel [THEN wf_induct])
   1.890 +apply (rule ih, auto simp: mset_less_rel_def)
   1.891 +done
   1.892 +
   1.893 +lemma multi_subset_induct [consumes 2, case_names empty add]:
   1.894 +assumes "F \<subseteq># A"
   1.895 +  and empty: "P {#}"
   1.896 +  and insert: "\<And>a F. a \<in># A \<Longrightarrow> P F \<Longrightarrow> P (F + {#a#})"
   1.897 +shows "P F"
   1.898 +proof -
   1.899 +  from `F \<subseteq># A`
   1.900 +  show ?thesis
   1.901 +  proof (induct F)
   1.902 +    show "P {#}" by fact
   1.903 +  next
   1.904 +    fix x F
   1.905 +    assume P: "F \<subseteq># A \<Longrightarrow> P F" and i: "F + {#x#} \<subseteq># A"
   1.906 +    show "P (F + {#x#})"
   1.907 +    proof (rule insert)
   1.908 +      from i show "x \<in># A" by (auto dest: mset_le_insertD)
   1.909 +      from i have "F \<subseteq># A" by (auto dest: mset_le_insertD)
   1.910 +      with P show "P F" .
   1.911 +    qed
   1.912 +  qed
   1.913 +qed
   1.914  
   1.915  
   1.916 -subsection {* Orderings *}
   1.917 +subsection {* Alternative representations *}
   1.918 +
   1.919 +subsubsection {* Lists *}
   1.920 +
   1.921 +primrec multiset_of :: "'a list \<Rightarrow> 'a multiset" where
   1.922 +  "multiset_of [] = {#}" |
   1.923 +  "multiset_of (a # x) = multiset_of x + {# a #}"
   1.924 +
   1.925 +lemma multiset_of_zero_iff[simp]: "(multiset_of x = {#}) = (x = [])"
   1.926 +by (induct x) auto
   1.927 +
   1.928 +lemma multiset_of_zero_iff_right[simp]: "({#} = multiset_of x) = (x = [])"
   1.929 +by (induct x) auto
   1.930 +
   1.931 +lemma set_of_multiset_of[simp]: "set_of(multiset_of x) = set x"
   1.932 +by (induct x) auto
   1.933 +
   1.934 +lemma mem_set_multiset_eq: "x \<in> set xs = (x :# multiset_of xs)"
   1.935 +by (induct xs) auto
   1.936 +
   1.937 +lemma multiset_of_append [simp]:
   1.938 +  "multiset_of (xs @ ys) = multiset_of xs + multiset_of ys"
   1.939 +  by (induct xs arbitrary: ys) (auto simp: add_ac)
   1.940 +
   1.941 +lemma surj_multiset_of: "surj multiset_of"
   1.942 +apply (unfold surj_def)
   1.943 +apply (rule allI)
   1.944 +apply (rule_tac M = y in multiset_induct)
   1.945 + apply auto
   1.946 +apply (rule_tac x = "x # xa" in exI)
   1.947 +apply auto
   1.948 +done
   1.949 +
   1.950 +lemma set_count_greater_0: "set x = {a. count (multiset_of x) a > 0}"
   1.951 +by (induct x) auto
   1.952 +
   1.953 +lemma distinct_count_atmost_1:
   1.954 +  "distinct x = (! a. count (multiset_of x) a = (if a \<in> set x then 1 else 0))"
   1.955 +apply (induct x, simp, rule iffI, simp_all)
   1.956 +apply (rule conjI)
   1.957 +apply (simp_all add: set_of_multiset_of [THEN sym] del: set_of_multiset_of)
   1.958 +apply (erule_tac x = a in allE, simp, clarify)
   1.959 +apply (erule_tac x = aa in allE, simp)
   1.960 +done
   1.961 +
   1.962 +lemma multiset_of_eq_setD:
   1.963 +  "multiset_of xs = multiset_of ys \<Longrightarrow> set xs = set ys"
   1.964 +by (rule) (auto simp add:multiset_eq_conv_count_eq set_count_greater_0)
   1.965 +
   1.966 +lemma set_eq_iff_multiset_of_eq_distinct:
   1.967 +  "distinct x \<Longrightarrow> distinct y \<Longrightarrow>
   1.968 +    (set x = set y) = (multiset_of x = multiset_of y)"
   1.969 +by (auto simp: multiset_eq_conv_count_eq distinct_count_atmost_1)
   1.970 +
   1.971 +lemma set_eq_iff_multiset_of_remdups_eq:
   1.972 +   "(set x = set y) = (multiset_of (remdups x) = multiset_of (remdups y))"
   1.973 +apply (rule iffI)
   1.974 +apply (simp add: set_eq_iff_multiset_of_eq_distinct[THEN iffD1])
   1.975 +apply (drule distinct_remdups [THEN distinct_remdups
   1.976 +      [THEN set_eq_iff_multiset_of_eq_distinct [THEN iffD2]]])
   1.977 +apply simp
   1.978 +done
   1.979 +
   1.980 +lemma multiset_of_compl_union [simp]:
   1.981 +  "multiset_of [x\<leftarrow>xs. P x] + multiset_of [x\<leftarrow>xs. \<not>P x] = multiset_of xs"
   1.982 +  by (induct xs) (auto simp: add_ac)
   1.983 +
   1.984 +lemma count_filter:
   1.985 +  "count (multiset_of xs) x = length [y \<leftarrow> xs. y = x]"
   1.986 +by (induct xs) auto
   1.987 +
   1.988 +lemma nth_mem_multiset_of: "i < length ls \<Longrightarrow> (ls ! i) :# multiset_of ls"
   1.989 +apply (induct ls arbitrary: i)
   1.990 + apply simp
   1.991 +apply (case_tac i)
   1.992 + apply auto
   1.993 +done
   1.994 +
   1.995 +lemma multiset_of_remove1: "multiset_of (remove1 a xs) = multiset_of xs - {#a#}"
   1.996 +by (induct xs) (auto simp add: multiset_eq_conv_count_eq)
   1.997 +
   1.998 +lemma multiset_of_eq_length:
   1.999 +assumes "multiset_of xs = multiset_of ys"
  1.1000 +shows "length xs = length ys"
  1.1001 +using assms
  1.1002 +proof (induct arbitrary: ys rule: length_induct)
  1.1003 +  case (1 xs ys)
  1.1004 +  show ?case
  1.1005 +  proof (cases xs)
  1.1006 +    case Nil with "1.prems" show ?thesis by simp
  1.1007 +  next
  1.1008 +    case (Cons x xs')
  1.1009 +    note xCons = Cons
  1.1010 +    show ?thesis
  1.1011 +    proof (cases ys)
  1.1012 +      case Nil
  1.1013 +      with "1.prems" Cons show ?thesis by simp
  1.1014 +    next
  1.1015 +      case (Cons y ys')
  1.1016 +      have x_in_ys: "x = y \<or> x \<in> set ys'"
  1.1017 +      proof (cases "x = y")
  1.1018 +        case True then show ?thesis ..
  1.1019 +      next
  1.1020 +        case False
  1.1021 +        from "1.prems" [symmetric] xCons Cons have "x :# multiset_of ys' + {#y#}" by simp
  1.1022 +        with False show ?thesis by (simp add: mem_set_multiset_eq)
  1.1023 +      qed
  1.1024 +      from "1.hyps" have IH: "length xs' < length xs \<longrightarrow>
  1.1025 +        (\<forall>x. multiset_of xs' = multiset_of x \<longrightarrow> length xs' = length x)" by blast
  1.1026 +      from "1.prems" x_in_ys Cons xCons have "multiset_of xs' = multiset_of (remove1 x (y#ys'))"
  1.1027 +        apply -
  1.1028 +        apply (simp add: multiset_of_remove1, simp only: add_eq_conv_diff)
  1.1029 +        apply fastsimp
  1.1030 +        done
  1.1031 +      with IH xCons have IH': "length xs' = length (remove1 x (y#ys'))" by fastsimp
  1.1032 +      from x_in_ys have "x \<noteq> y \<Longrightarrow> length ys' > 0" by auto
  1.1033 +      with Cons xCons x_in_ys IH' show ?thesis by (auto simp add: length_remove1)
  1.1034 +    qed
  1.1035 +  qed
  1.1036 +qed
  1.1037 +
  1.1038 +text {*
  1.1039 +  This lemma shows which properties suffice to show that a function
  1.1040 +  @{text "f"} with @{text "f xs = ys"} behaves like sort.
  1.1041 +*}
  1.1042 +lemma properties_for_sort:
  1.1043 +  "multiset_of ys = multiset_of xs \<Longrightarrow> sorted ys \<Longrightarrow> sort xs = ys"
  1.1044 +proof (induct xs arbitrary: ys)
  1.1045 +  case Nil then show ?case by simp
  1.1046 +next
  1.1047 +  case (Cons x xs)
  1.1048 +  then have "x \<in> set ys"
  1.1049 +    by (auto simp add:  mem_set_multiset_eq intro!: ccontr)
  1.1050 +  with Cons.prems Cons.hyps [of "remove1 x ys"] show ?case
  1.1051 +    by (simp add: sorted_remove1 multiset_of_remove1 insort_remove1)
  1.1052 +qed
  1.1053 +
  1.1054 +lemma multiset_of_remdups_le: "multiset_of (remdups xs) \<le># multiset_of xs"
  1.1055 +apply (induct xs)
  1.1056 + apply auto
  1.1057 +apply (rule mset_le_trans)
  1.1058 + apply auto
  1.1059 +done
  1.1060 +
  1.1061 +lemma multiset_of_update:
  1.1062 +  "i < length ls \<Longrightarrow> multiset_of (ls[i := v]) = multiset_of ls - {#ls ! i#} + {#v#}"
  1.1063 +proof (induct ls arbitrary: i)
  1.1064 +  case Nil then show ?case by simp
  1.1065 +next
  1.1066 +  case (Cons x xs)
  1.1067 +  show ?case
  1.1068 +  proof (cases i)
  1.1069 +    case 0 then show ?thesis by simp
  1.1070 +  next
  1.1071 +    case (Suc i')
  1.1072 +    with Cons show ?thesis
  1.1073 +      apply simp
  1.1074 +      apply (subst add_assoc)
  1.1075 +      apply (subst add_commute [of "{#v#}" "{#x#}"])
  1.1076 +      apply (subst add_assoc [symmetric])
  1.1077 +      apply simp
  1.1078 +      apply (rule mset_le_multiset_union_diff_commute)
  1.1079 +      apply (simp add: mset_le_single nth_mem_multiset_of)
  1.1080 +      done
  1.1081 +  qed
  1.1082 +qed
  1.1083 +
  1.1084 +lemma multiset_of_swap:
  1.1085 +  "i < length ls \<Longrightarrow> j < length ls \<Longrightarrow>
  1.1086 +    multiset_of (ls[j := ls ! i, i := ls ! j]) = multiset_of ls"
  1.1087 +  by (cases "i = j") (simp_all add: multiset_of_update nth_mem_multiset_of)
  1.1088 +
  1.1089 +
  1.1090 +subsubsection {* Association lists -- including rudimentary code generation *}
  1.1091 +
  1.1092 +definition count_of :: "('a \<times> nat) list \<Rightarrow> 'a \<Rightarrow> nat" where
  1.1093 +  "count_of xs x = (case map_of xs x of None \<Rightarrow> 0 | Some n \<Rightarrow> n)"
  1.1094 +
  1.1095 +lemma count_of_multiset:
  1.1096 +  "count_of xs \<in> multiset"
  1.1097 +proof -
  1.1098 +  let ?A = "{x::'a. 0 < (case map_of xs x of None \<Rightarrow> 0\<Colon>nat | Some (n\<Colon>nat) \<Rightarrow> n)}"
  1.1099 +  have "?A \<subseteq> dom (map_of xs)"
  1.1100 +  proof
  1.1101 +    fix x
  1.1102 +    assume "x \<in> ?A"
  1.1103 +    then have "0 < (case map_of xs x of None \<Rightarrow> 0\<Colon>nat | Some (n\<Colon>nat) \<Rightarrow> n)" by simp
  1.1104 +    then have "map_of xs x \<noteq> None" by (cases "map_of xs x") auto
  1.1105 +    then show "x \<in> dom (map_of xs)" by auto
  1.1106 +  qed
  1.1107 +  with finite_dom_map_of [of xs] have "finite ?A"
  1.1108 +    by (auto intro: finite_subset)
  1.1109 +  then show ?thesis
  1.1110 +    by (simp add: count_of_def expand_fun_eq multiset_def)
  1.1111 +qed
  1.1112 +
  1.1113 +lemma count_simps [simp]:
  1.1114 +  "count_of [] = (\<lambda>_. 0)"
  1.1115 +  "count_of ((x, n) # xs) = (\<lambda>y. if x = y then n else count_of xs y)"
  1.1116 +  by (simp_all add: count_of_def expand_fun_eq)
  1.1117 +
  1.1118 +lemma count_of_empty:
  1.1119 +  "x \<notin> fst ` set xs \<Longrightarrow> count_of xs x = 0"
  1.1120 +  by (induct xs) (simp_all add: count_of_def)
  1.1121 +
  1.1122 +lemma count_of_filter:
  1.1123 +  "count_of (filter (P \<circ> fst) xs) x = (if P x then count_of xs x else 0)"
  1.1124 +  by (induct xs) auto
  1.1125 +
  1.1126 +definition Bag :: "('a \<times> nat) list \<Rightarrow> 'a multiset" where
  1.1127 +  "Bag xs = Abs_multiset (count_of xs)"
  1.1128 +
  1.1129 +code_datatype Bag
  1.1130 +
  1.1131 +lemma count_Bag [simp, code]:
  1.1132 +  "count (Bag xs) = count_of xs"
  1.1133 +  by (simp add: Bag_def count_of_multiset Abs_multiset_inverse)
  1.1134 +
  1.1135 +lemma Mempty_Bag [code]:
  1.1136 +  "{#} = Bag []"
  1.1137 +  by (simp add: multiset_eq_conv_count_eq)
  1.1138 +  
  1.1139 +lemma single_Bag [code]:
  1.1140 +  "{#x#} = Bag [(x, 1)]"
  1.1141 +  by (simp add: multiset_eq_conv_count_eq)
  1.1142 +
  1.1143 +lemma MCollect_Bag [code]:
  1.1144 +  "MCollect (Bag xs) P = Bag (filter (P \<circ> fst) xs)"
  1.1145 +  by (simp add: multiset_eq_conv_count_eq count_of_filter)
  1.1146 +
  1.1147 +lemma mset_less_eq_Bag [code]:
  1.1148 +  "Bag xs \<subseteq># A \<longleftrightarrow> (\<forall>(x, n) \<in> set xs. count_of xs x \<le> count A x)"
  1.1149 +    (is "?lhs \<longleftrightarrow> ?rhs")
  1.1150 +proof
  1.1151 +  assume ?lhs then show ?rhs
  1.1152 +    by (auto simp add: mset_le_def count_Bag)
  1.1153 +next
  1.1154 +  assume ?rhs
  1.1155 +  show ?lhs
  1.1156 +  proof (rule mset_less_eqI)
  1.1157 +    fix x
  1.1158 +    from `?rhs` have "count_of xs x \<le> count A x"
  1.1159 +      by (cases "x \<in> fst ` set xs") (auto simp add: count_of_empty)
  1.1160 +    then show "count (Bag xs) x \<le> count A x"
  1.1161 +      by (simp add: mset_le_def count_Bag)
  1.1162 +  qed
  1.1163 +qed
  1.1164 +
  1.1165 +instantiation multiset :: (eq) eq
  1.1166 +begin
  1.1167 +
  1.1168 +definition
  1.1169 +  "HOL.eq A B \<longleftrightarrow> A \<subseteq># B \<and> B \<subseteq># A"
  1.1170 +
  1.1171 +instance proof
  1.1172 +qed (simp add: eq_multiset_def mset_order.eq_iff)
  1.1173 +
  1.1174 +end
  1.1175 +
  1.1176 +definition (in term_syntax)
  1.1177 +  bagify :: "('a\<Colon>typerep \<times> nat) list \<times> (unit \<Rightarrow> Code_Evaluation.term)
  1.1178 +    \<Rightarrow> 'a multiset \<times> (unit \<Rightarrow> Code_Evaluation.term)" where
  1.1179 +  [code_unfold]: "bagify xs = Code_Evaluation.valtermify Bag {\<cdot>} xs"
  1.1180 +
  1.1181 +notation fcomp (infixl "o>" 60)
  1.1182 +notation scomp (infixl "o\<rightarrow>" 60)
  1.1183 +
  1.1184 +instantiation multiset :: (random) random
  1.1185 +begin
  1.1186 +
  1.1187 +definition
  1.1188 +  "Quickcheck.random i = Quickcheck.random i o\<rightarrow> (\<lambda>xs. Pair (bagify xs))"
  1.1189 +
  1.1190 +instance ..
  1.1191 +
  1.1192 +end
  1.1193 +
  1.1194 +no_notation fcomp (infixl "o>" 60)
  1.1195 +no_notation scomp (infixl "o\<rightarrow>" 60)
  1.1196 +
  1.1197 +hide (open) const bagify
  1.1198 +
  1.1199 +
  1.1200 +subsection {* The multiset order *}
  1.1201  
  1.1202  subsubsection {* Well-foundedness *}
  1.1203  
  1.1204 @@ -490,7 +1030,7 @@
  1.1205        (\<forall>b. b :# K --> (b, a) \<in> r)}"
  1.1206  
  1.1207  definition mult :: "('a \<times> 'a) set => ('a multiset \<times> 'a multiset) set" where
  1.1208 -  "mult r = (mult1 r)\<^sup>+"
  1.1209 +  [code del]: "mult r = (mult1 r)\<^sup>+"
  1.1210  
  1.1211  lemma not_less_empty [iff]: "(M, {#}) \<notin> mult1 r"
  1.1212  by (simp add: mult1_def)
  1.1213 @@ -523,7 +1063,7 @@
  1.1214      next
  1.1215        fix K'
  1.1216        assume "M0' = K' + {#a#}"
  1.1217 -      with N have n: "N = K' + K + {#a#}" by (simp add: union_ac)
  1.1218 +      with N have n: "N = K' + K + {#a#}" by (simp add: add_ac)
  1.1219  
  1.1220        assume "M0 = K' + {#a'#}"
  1.1221        with r have "?R (K' + K) M0" by blast
  1.1222 @@ -568,7 +1108,7 @@
  1.1223            with wf_hyp have "\<forall>M \<in> ?W. M + {#x#} \<in> ?W" by blast
  1.1224            moreover from add have "M0 + K \<in> ?W" by simp
  1.1225            ultimately have "(M0 + K) + {#x#} \<in> ?W" ..
  1.1226 -          then show "M0 + (K + {#x#}) \<in> ?W" by (simp only: union_assoc)
  1.1227 +          then show "M0 + (K + {#x#}) \<in> ?W" by (simp only: add_assoc)
  1.1228          qed
  1.1229          then show "N \<in> ?W" by (simp only: N)
  1.1230        qed
  1.1231 @@ -610,11 +1150,6 @@
  1.1232  
  1.1233  subsubsection {* Closure-free presentation *}
  1.1234  
  1.1235 -(*Badly needed: a linear arithmetic procedure for multisets*)
  1.1236 -
  1.1237 -lemma diff_union_single_conv: "a :# J ==> I + J - {#a#} = I + (J - {#a#})"
  1.1238 -by (simp add: multiset_eq_conv_count_eq)
  1.1239 -
  1.1240  text {* One direction. *}
  1.1241  
  1.1242  lemma mult_implies_one_step:
  1.1243 @@ -628,7 +1163,7 @@
  1.1244   apply (rule_tac x = I in exI)
  1.1245   apply (simp (no_asm))
  1.1246   apply (rule_tac x = "(K - {#a#}) + Ka" in exI)
  1.1247 - apply (simp (no_asm_simp) add: union_assoc [symmetric])
  1.1248 + apply (simp (no_asm_simp) add: add_assoc [symmetric])
  1.1249   apply (drule_tac f = "\<lambda>M. M - {#a#}" in arg_cong)
  1.1250   apply (simp add: diff_union_single_conv)
  1.1251   apply (simp (no_asm_use) add: trans_def)
  1.1252 @@ -649,14 +1184,6 @@
  1.1253  apply (simp (no_asm))
  1.1254  done
  1.1255  
  1.1256 -lemma elem_imp_eq_diff_union: "a :# M ==> M = M - {#a#} + {#a#}"
  1.1257 -by (simp add: multiset_eq_conv_count_eq)
  1.1258 -
  1.1259 -lemma size_eq_Suc_imp_eq_union: "size M = Suc n ==> \<exists>a N. M = N + {#a#}"
  1.1260 -apply (erule size_eq_Suc_imp_elem [THEN exE])
  1.1261 -apply (drule elem_imp_eq_diff_union, auto)
  1.1262 -done
  1.1263 -
  1.1264  lemma one_step_implies_mult_aux:
  1.1265    "trans r ==>
  1.1266      \<forall>I J K. (size J = n \<and> J \<noteq> {#} \<and> (\<forall>k \<in> set_of K. \<exists>j \<in> set_of J. (k, j) \<in> r))
  1.1267 @@ -679,13 +1206,13 @@
  1.1268      (I + {# x :# K. (x, a) \<in> r #}) + J') \<in> mult r")
  1.1269   prefer 2
  1.1270   apply force
  1.1271 -apply (simp (no_asm_use) add: union_assoc [symmetric] mult_def)
  1.1272 +apply (simp (no_asm_use) add: add_assoc [symmetric] mult_def)
  1.1273  apply (erule trancl_trans)
  1.1274  apply (rule r_into_trancl)
  1.1275  apply (simp add: mult1_def set_of_def)
  1.1276  apply (rule_tac x = a in exI)
  1.1277  apply (rule_tac x = "I + J'" in exI)
  1.1278 -apply (simp add: union_ac)
  1.1279 +apply (simp add: add_ac)
  1.1280  done
  1.1281  
  1.1282  lemma one_step_implies_mult:
  1.1283 @@ -699,10 +1226,10 @@
  1.1284  instantiation multiset :: (order) order
  1.1285  begin
  1.1286  
  1.1287 -definition less_multiset_def [code del]:
  1.1288 +definition less_multiset_def:
  1.1289    "M' < M \<longleftrightarrow> (M', M) \<in> mult {(x', x). x' < x}"
  1.1290  
  1.1291 -definition le_multiset_def [code del]:
  1.1292 +definition le_multiset_def:
  1.1293    "M' <= M \<longleftrightarrow> M' = M \<or> M' < (M::'a multiset)"
  1.1294  
  1.1295  lemma trans_base_order: "trans {(x', x). x' < (x::'a::order)}"
  1.1296 @@ -776,7 +1303,7 @@
  1.1297  apply auto
  1.1298  apply (rule_tac x = a in exI)
  1.1299  apply (rule_tac x = "C + M0" in exI)
  1.1300 -apply (simp add: union_assoc)
  1.1301 +apply (simp add: add_assoc)
  1.1302  done
  1.1303  
  1.1304  lemma union_less_mono2: "B < D ==> C + B < C + (D::'a::order multiset)"
  1.1305 @@ -787,8 +1314,8 @@
  1.1306  done
  1.1307  
  1.1308  lemma union_less_mono1: "B < D ==> B + C < D + (C::'a::order multiset)"
  1.1309 -apply (subst union_commute [of B C])
  1.1310 -apply (subst union_commute [of D C])
  1.1311 +apply (subst add_commute [of B C])
  1.1312 +apply (subst add_commute [of D C])
  1.1313  apply (erule union_less_mono2)
  1.1314  done
  1.1315  
  1.1316 @@ -819,7 +1346,7 @@
  1.1317  qed
  1.1318  
  1.1319  lemma union_upper2: "B <= A + (B::'a::order multiset)"
  1.1320 -by (subst union_commute) (rule union_upper1)
  1.1321 +by (subst add_commute) (rule union_upper1)
  1.1322  
  1.1323  instance multiset :: (order) pordered_ab_semigroup_add
  1.1324  apply intro_classes
  1.1325 @@ -827,416 +1354,6 @@
  1.1326  done
  1.1327  
  1.1328  
  1.1329 -subsection {* Link with lists *}
  1.1330 -
  1.1331 -primrec multiset_of :: "'a list \<Rightarrow> 'a multiset" where
  1.1332 -  "multiset_of [] = {#}" |
  1.1333 -  "multiset_of (a # x) = multiset_of x + {# a #}"
  1.1334 -
  1.1335 -lemma multiset_of_zero_iff[simp]: "(multiset_of x = {#}) = (x = [])"
  1.1336 -by (induct x) auto
  1.1337 -
  1.1338 -lemma multiset_of_zero_iff_right[simp]: "({#} = multiset_of x) = (x = [])"
  1.1339 -by (induct x) auto
  1.1340 -
  1.1341 -lemma set_of_multiset_of[simp]: "set_of(multiset_of x) = set x"
  1.1342 -by (induct x) auto
  1.1343 -
  1.1344 -lemma mem_set_multiset_eq: "x \<in> set xs = (x :# multiset_of xs)"
  1.1345 -by (induct xs) auto
  1.1346 -
  1.1347 -lemma multiset_of_append [simp]:
  1.1348 -  "multiset_of (xs @ ys) = multiset_of xs + multiset_of ys"
  1.1349 -by (induct xs arbitrary: ys) (auto simp: union_ac)
  1.1350 -
  1.1351 -lemma surj_multiset_of: "surj multiset_of"
  1.1352 -apply (unfold surj_def)
  1.1353 -apply (rule allI)
  1.1354 -apply (rule_tac M = y in multiset_induct)
  1.1355 - apply auto
  1.1356 -apply (rule_tac x = "x # xa" in exI)
  1.1357 -apply auto
  1.1358 -done
  1.1359 -
  1.1360 -lemma set_count_greater_0: "set x = {a. count (multiset_of x) a > 0}"
  1.1361 -by (induct x) auto
  1.1362 -
  1.1363 -lemma distinct_count_atmost_1:
  1.1364 -  "distinct x = (! a. count (multiset_of x) a = (if a \<in> set x then 1 else 0))"
  1.1365 -apply (induct x, simp, rule iffI, simp_all)
  1.1366 -apply (rule conjI)
  1.1367 -apply (simp_all add: set_of_multiset_of [THEN sym] del: set_of_multiset_of)
  1.1368 -apply (erule_tac x = a in allE, simp, clarify)
  1.1369 -apply (erule_tac x = aa in allE, simp)
  1.1370 -done
  1.1371 -
  1.1372 -lemma multiset_of_eq_setD:
  1.1373 -  "multiset_of xs = multiset_of ys \<Longrightarrow> set xs = set ys"
  1.1374 -by (rule) (auto simp add:multiset_eq_conv_count_eq set_count_greater_0)
  1.1375 -
  1.1376 -lemma set_eq_iff_multiset_of_eq_distinct:
  1.1377 -  "distinct x \<Longrightarrow> distinct y \<Longrightarrow>
  1.1378 -    (set x = set y) = (multiset_of x = multiset_of y)"
  1.1379 -by (auto simp: multiset_eq_conv_count_eq distinct_count_atmost_1)
  1.1380 -
  1.1381 -lemma set_eq_iff_multiset_of_remdups_eq:
  1.1382 -   "(set x = set y) = (multiset_of (remdups x) = multiset_of (remdups y))"
  1.1383 -apply (rule iffI)
  1.1384 -apply (simp add: set_eq_iff_multiset_of_eq_distinct[THEN iffD1])
  1.1385 -apply (drule distinct_remdups [THEN distinct_remdups
  1.1386 -      [THEN set_eq_iff_multiset_of_eq_distinct [THEN iffD2]]])
  1.1387 -apply simp
  1.1388 -done
  1.1389 -
  1.1390 -lemma multiset_of_compl_union [simp]:
  1.1391 -  "multiset_of [x\<leftarrow>xs. P x] + multiset_of [x\<leftarrow>xs. \<not>P x] = multiset_of xs"
  1.1392 -by (induct xs) (auto simp: union_ac)
  1.1393 -
  1.1394 -lemma count_filter:
  1.1395 -  "count (multiset_of xs) x = length [y \<leftarrow> xs. y = x]"
  1.1396 -by (induct xs) auto
  1.1397 -
  1.1398 -lemma nth_mem_multiset_of: "i < length ls \<Longrightarrow> (ls ! i) :# multiset_of ls"
  1.1399 -apply (induct ls arbitrary: i)
  1.1400 - apply simp
  1.1401 -apply (case_tac i)
  1.1402 - apply auto
  1.1403 -done
  1.1404 -
  1.1405 -lemma multiset_of_remove1: "multiset_of (remove1 a xs) = multiset_of xs - {#a#}"
  1.1406 -by (induct xs) (auto simp add: multiset_eq_conv_count_eq)
  1.1407 -
  1.1408 -lemma multiset_of_eq_length:
  1.1409 -assumes "multiset_of xs = multiset_of ys"
  1.1410 -shows "length xs = length ys"
  1.1411 -using assms
  1.1412 -proof (induct arbitrary: ys rule: length_induct)
  1.1413 -  case (1 xs ys)
  1.1414 -  show ?case
  1.1415 -  proof (cases xs)
  1.1416 -    case Nil with "1.prems" show ?thesis by simp
  1.1417 -  next
  1.1418 -    case (Cons x xs')
  1.1419 -    note xCons = Cons
  1.1420 -    show ?thesis
  1.1421 -    proof (cases ys)
  1.1422 -      case Nil
  1.1423 -      with "1.prems" Cons show ?thesis by simp
  1.1424 -    next
  1.1425 -      case (Cons y ys')
  1.1426 -      have x_in_ys: "x = y \<or> x \<in> set ys'"
  1.1427 -      proof (cases "x = y")
  1.1428 -        case True then show ?thesis ..
  1.1429 -      next
  1.1430 -        case False
  1.1431 -        from "1.prems" [symmetric] xCons Cons have "x :# multiset_of ys' + {#y#}" by simp
  1.1432 -        with False show ?thesis by (simp add: mem_set_multiset_eq)
  1.1433 -      qed
  1.1434 -      from "1.hyps" have IH: "length xs' < length xs \<longrightarrow>
  1.1435 -        (\<forall>x. multiset_of xs' = multiset_of x \<longrightarrow> length xs' = length x)" by blast
  1.1436 -      from "1.prems" x_in_ys Cons xCons have "multiset_of xs' = multiset_of (remove1 x (y#ys'))"
  1.1437 -        apply -
  1.1438 -        apply (simp add: multiset_of_remove1, simp only: add_eq_conv_diff)
  1.1439 -        apply fastsimp
  1.1440 -        done
  1.1441 -      with IH xCons have IH': "length xs' = length (remove1 x (y#ys'))" by fastsimp
  1.1442 -      from x_in_ys have "x \<noteq> y \<Longrightarrow> length ys' > 0" by auto
  1.1443 -      with Cons xCons x_in_ys IH' show ?thesis by (auto simp add: length_remove1)
  1.1444 -    qed
  1.1445 -  qed
  1.1446 -qed
  1.1447 -
  1.1448 -text {*
  1.1449 -  This lemma shows which properties suffice to show that a function
  1.1450 -  @{text "f"} with @{text "f xs = ys"} behaves like sort.
  1.1451 -*}
  1.1452 -lemma properties_for_sort:
  1.1453 -  "multiset_of ys = multiset_of xs \<Longrightarrow> sorted ys \<Longrightarrow> sort xs = ys"
  1.1454 -proof (induct xs arbitrary: ys)
  1.1455 -  case Nil then show ?case by simp
  1.1456 -next
  1.1457 -  case (Cons x xs)
  1.1458 -  then have "x \<in> set ys"
  1.1459 -    by (auto simp add:  mem_set_multiset_eq intro!: ccontr)
  1.1460 -  with Cons.prems Cons.hyps [of "remove1 x ys"] show ?case
  1.1461 -    by (simp add: sorted_remove1 multiset_of_remove1 insort_remove1)
  1.1462 -qed
  1.1463 -
  1.1464 -
  1.1465 -subsection {* Pointwise ordering induced by count *}
  1.1466 -
  1.1467 -definition mset_le :: "'a multiset \<Rightarrow> 'a multiset \<Rightarrow> bool"  (infix "\<le>#" 50) where
  1.1468 -  [code del]: "A \<le># B \<longleftrightarrow> (\<forall>a. count A a \<le> count B a)"
  1.1469 -
  1.1470 -definition mset_less :: "'a multiset \<Rightarrow> 'a multiset \<Rightarrow> bool"  (infix "<#" 50) where
  1.1471 -  [code del]: "A <# B \<longleftrightarrow> A \<le># B \<and> A \<noteq> B"
  1.1472 -
  1.1473 -notation mset_le  (infix "\<subseteq>#" 50)
  1.1474 -notation mset_less  (infix "\<subset>#" 50)
  1.1475 -
  1.1476 -lemma mset_le_refl[simp]: "A \<le># A"
  1.1477 -unfolding mset_le_def by auto
  1.1478 -
  1.1479 -lemma mset_le_trans: "A \<le># B \<Longrightarrow> B \<le># C \<Longrightarrow> A \<le># C"
  1.1480 -unfolding mset_le_def by (fast intro: order_trans)
  1.1481 -
  1.1482 -lemma mset_le_antisym: "A \<le># B \<Longrightarrow> B \<le># A \<Longrightarrow> A = B"
  1.1483 -apply (unfold mset_le_def)
  1.1484 -apply (rule multiset_eq_conv_count_eq [THEN iffD2])
  1.1485 -apply (blast intro: order_antisym)
  1.1486 -done
  1.1487 -
  1.1488 -lemma mset_le_exists_conv: "(A \<le># B) = (\<exists>C. B = A + C)"
  1.1489 -apply (unfold mset_le_def, rule iffI, rule_tac x = "B - A" in exI)
  1.1490 -apply (auto intro: multiset_eq_conv_count_eq [THEN iffD2])
  1.1491 -done
  1.1492 -
  1.1493 -lemma mset_le_mono_add_right_cancel[simp]: "(A + C \<le># B + C) = (A \<le># B)"
  1.1494 -unfolding mset_le_def by auto
  1.1495 -
  1.1496 -lemma mset_le_mono_add_left_cancel[simp]: "(C + A \<le># C + B) = (A \<le># B)"
  1.1497 -unfolding mset_le_def by auto
  1.1498 -
  1.1499 -lemma mset_le_mono_add: "\<lbrakk> A \<le># B; C \<le># D \<rbrakk> \<Longrightarrow> A + C \<le># B + D"
  1.1500 -apply (unfold mset_le_def)
  1.1501 -apply auto
  1.1502 -apply (erule_tac x = a in allE)+
  1.1503 -apply auto
  1.1504 -done
  1.1505 -
  1.1506 -lemma mset_le_add_left[simp]: "A \<le># A + B"
  1.1507 -unfolding mset_le_def by auto
  1.1508 -
  1.1509 -lemma mset_le_add_right[simp]: "B \<le># A + B"
  1.1510 -unfolding mset_le_def by auto
  1.1511 -
  1.1512 -lemma mset_le_single: "a :# B \<Longrightarrow> {#a#} \<le># B"
  1.1513 -by (simp add: mset_le_def)
  1.1514 -
  1.1515 -lemma multiset_diff_union_assoc: "C \<le># B \<Longrightarrow> A + B - C = A + (B - C)"
  1.1516 -by (simp add: multiset_eq_conv_count_eq mset_le_def)
  1.1517 -
  1.1518 -lemma mset_le_multiset_union_diff_commute:
  1.1519 -assumes "B \<le># A"
  1.1520 -shows "A - B + C = A + C - B"
  1.1521 -proof -
  1.1522 -  from mset_le_exists_conv [of "B" "A"] assms have "\<exists>D. A = B + D" ..
  1.1523 -  from this obtain D where "A = B + D" ..
  1.1524 -  then show ?thesis
  1.1525 -    apply simp
  1.1526 -    apply (subst union_commute)
  1.1527 -    apply (subst multiset_diff_union_assoc)
  1.1528 -    apply simp
  1.1529 -    apply (simp add: diff_cancel)
  1.1530 -    apply (subst union_assoc)
  1.1531 -    apply (subst union_commute[of "B" _])
  1.1532 -    apply (subst multiset_diff_union_assoc)
  1.1533 -    apply simp
  1.1534 -    apply (simp add: diff_cancel)
  1.1535 -    done
  1.1536 -qed
  1.1537 -
  1.1538 -lemma multiset_of_remdups_le: "multiset_of (remdups xs) \<le># multiset_of xs"
  1.1539 -apply (induct xs)
  1.1540 - apply auto
  1.1541 -apply (rule mset_le_trans)
  1.1542 - apply auto
  1.1543 -done
  1.1544 -
  1.1545 -lemma multiset_of_update:
  1.1546 -  "i < length ls \<Longrightarrow> multiset_of (ls[i := v]) = multiset_of ls - {#ls ! i#} + {#v#}"
  1.1547 -proof (induct ls arbitrary: i)
  1.1548 -  case Nil then show ?case by simp
  1.1549 -next
  1.1550 -  case (Cons x xs)
  1.1551 -  show ?case
  1.1552 -  proof (cases i)
  1.1553 -    case 0 then show ?thesis by simp
  1.1554 -  next
  1.1555 -    case (Suc i')
  1.1556 -    with Cons show ?thesis
  1.1557 -      apply simp
  1.1558 -      apply (subst union_assoc)
  1.1559 -      apply (subst union_commute [where M = "{#v#}" and N = "{#x#}"])
  1.1560 -      apply (subst union_assoc [symmetric])
  1.1561 -      apply simp
  1.1562 -      apply (rule mset_le_multiset_union_diff_commute)
  1.1563 -      apply (simp add: mset_le_single nth_mem_multiset_of)
  1.1564 -      done
  1.1565 -  qed
  1.1566 -qed
  1.1567 -
  1.1568 -lemma multiset_of_swap:
  1.1569 -  "i < length ls \<Longrightarrow> j < length ls \<Longrightarrow>
  1.1570 -    multiset_of (ls[j := ls ! i, i := ls ! j]) = multiset_of ls"
  1.1571 -apply (case_tac "i = j")
  1.1572 - apply simp
  1.1573 -apply (simp add: multiset_of_update)
  1.1574 -apply (subst elem_imp_eq_diff_union[symmetric])
  1.1575 - apply (simp add: nth_mem_multiset_of)
  1.1576 -apply simp
  1.1577 -done
  1.1578 -
  1.1579 -interpretation mset_order: order "op \<le>#" "op <#"
  1.1580 -proof qed (auto intro: order.intro mset_le_refl mset_le_antisym
  1.1581 -  mset_le_trans simp: mset_less_def)
  1.1582 -
  1.1583 -interpretation mset_order_cancel_semigroup:
  1.1584 -  pordered_cancel_ab_semigroup_add "op +" "op \<le>#" "op <#"
  1.1585 -proof qed (erule mset_le_mono_add [OF mset_le_refl])
  1.1586 -
  1.1587 -interpretation mset_order_semigroup_cancel:
  1.1588 -  pordered_ab_semigroup_add_imp_le "op +" "op \<le>#" "op <#"
  1.1589 -proof qed simp
  1.1590 -
  1.1591 -
  1.1592 -lemma mset_lessD: "A \<subset># B \<Longrightarrow> x \<in># A \<Longrightarrow> x \<in># B"
  1.1593 -apply (clarsimp simp: mset_le_def mset_less_def)
  1.1594 -apply (erule_tac x=x in allE)
  1.1595 -apply auto
  1.1596 -done
  1.1597 -
  1.1598 -lemma mset_leD: "A \<subseteq># B \<Longrightarrow> x \<in># A \<Longrightarrow> x \<in># B"
  1.1599 -apply (clarsimp simp: mset_le_def mset_less_def)
  1.1600 -apply (erule_tac x = x in allE)
  1.1601 -apply auto
  1.1602 -done
  1.1603 -  
  1.1604 -lemma mset_less_insertD: "(A + {#x#} \<subset># B) \<Longrightarrow> (x \<in># B \<and> A \<subset># B)"
  1.1605 -apply (rule conjI)
  1.1606 - apply (simp add: mset_lessD)
  1.1607 -apply (clarsimp simp: mset_le_def mset_less_def)
  1.1608 -apply safe
  1.1609 - apply (erule_tac x = a in allE)
  1.1610 - apply (auto split: split_if_asm)
  1.1611 -done
  1.1612 -
  1.1613 -lemma mset_le_insertD: "(A + {#x#} \<subseteq># B) \<Longrightarrow> (x \<in># B \<and> A \<subseteq># B)"
  1.1614 -apply (rule conjI)
  1.1615 - apply (simp add: mset_leD)
  1.1616 -apply (force simp: mset_le_def mset_less_def split: split_if_asm)
  1.1617 -done
  1.1618 -
  1.1619 -lemma mset_less_of_empty[simp]: "A \<subset># {#} = False" 
  1.1620 -by (induct A) (auto simp: mset_le_def mset_less_def)
  1.1621 -
  1.1622 -lemma multi_psub_of_add_self[simp]: "A \<subset># A + {#x#}"
  1.1623 -by (auto simp: mset_le_def mset_less_def)
  1.1624 -
  1.1625 -lemma multi_psub_self[simp]: "A \<subset># A = False"
  1.1626 -by (auto simp: mset_le_def mset_less_def)
  1.1627 -
  1.1628 -lemma mset_less_add_bothsides:
  1.1629 -  "T + {#x#} \<subset># S + {#x#} \<Longrightarrow> T \<subset># S"
  1.1630 -by (auto simp: mset_le_def mset_less_def)
  1.1631 -
  1.1632 -lemma mset_less_empty_nonempty: "({#} \<subset># S) = (S \<noteq> {#})"
  1.1633 -by (auto simp: mset_le_def mset_less_def)
  1.1634 -
  1.1635 -lemma mset_less_size: "A \<subset># B \<Longrightarrow> size A < size B"
  1.1636 -proof (induct A arbitrary: B)
  1.1637 -  case (empty M)
  1.1638 -  then have "M \<noteq> {#}" by (simp add: mset_less_empty_nonempty)
  1.1639 -  then obtain M' x where "M = M' + {#x#}" 
  1.1640 -    by (blast dest: multi_nonempty_split)
  1.1641 -  then show ?case by simp
  1.1642 -next
  1.1643 -  case (add S x T)
  1.1644 -  have IH: "\<And>B. S \<subset># B \<Longrightarrow> size S < size B" by fact
  1.1645 -  have SxsubT: "S + {#x#} \<subset># T" by fact
  1.1646 -  then have "x \<in># T" and "S \<subset># T" by (auto dest: mset_less_insertD)
  1.1647 -  then obtain T' where T: "T = T' + {#x#}" 
  1.1648 -    by (blast dest: multi_member_split)
  1.1649 -  then have "S \<subset># T'" using SxsubT 
  1.1650 -    by (blast intro: mset_less_add_bothsides)
  1.1651 -  then have "size S < size T'" using IH by simp
  1.1652 -  then show ?case using T by simp
  1.1653 -qed
  1.1654 -
  1.1655 -lemmas mset_less_trans = mset_order.less_trans
  1.1656 -
  1.1657 -lemma mset_less_diff_self: "c \<in># B \<Longrightarrow> B - {#c#} \<subset># B"
  1.1658 -by (auto simp: mset_le_def mset_less_def multi_drop_mem_not_eq)
  1.1659 -
  1.1660 -
  1.1661 -subsection {* Strong induction and subset induction for multisets *}
  1.1662 -
  1.1663 -text {* Well-foundedness of proper subset operator: *}
  1.1664 -
  1.1665 -text {* proper multiset subset *}
  1.1666 -definition
  1.1667 -  mset_less_rel :: "('a multiset * 'a multiset) set" where
  1.1668 -  "mset_less_rel = {(A,B). A \<subset># B}"
  1.1669 -
  1.1670 -lemma multiset_add_sub_el_shuffle: 
  1.1671 -  assumes "c \<in># B" and "b \<noteq> c" 
  1.1672 -  shows "B - {#c#} + {#b#} = B + {#b#} - {#c#}"
  1.1673 -proof -
  1.1674 -  from `c \<in># B` obtain A where B: "B = A + {#c#}" 
  1.1675 -    by (blast dest: multi_member_split)
  1.1676 -  have "A + {#b#} = A + {#b#} + {#c#} - {#c#}" by simp
  1.1677 -  then have "A + {#b#} = A + {#c#} + {#b#} - {#c#}" 
  1.1678 -    by (simp add: union_ac)
  1.1679 -  then show ?thesis using B by simp
  1.1680 -qed
  1.1681 -
  1.1682 -lemma wf_mset_less_rel: "wf mset_less_rel"
  1.1683 -apply (unfold mset_less_rel_def)
  1.1684 -apply (rule wf_measure [THEN wf_subset, where f1=size])
  1.1685 -apply (clarsimp simp: measure_def inv_image_def mset_less_size)
  1.1686 -done
  1.1687 -
  1.1688 -text {* The induction rules: *}
  1.1689 -
  1.1690 -lemma full_multiset_induct [case_names less]:
  1.1691 -assumes ih: "\<And>B. \<forall>A. A \<subset># B \<longrightarrow> P A \<Longrightarrow> P B"
  1.1692 -shows "P B"
  1.1693 -apply (rule wf_mset_less_rel [THEN wf_induct])
  1.1694 -apply (rule ih, auto simp: mset_less_rel_def)
  1.1695 -done
  1.1696 -
  1.1697 -lemma multi_subset_induct [consumes 2, case_names empty add]:
  1.1698 -assumes "F \<subseteq># A"
  1.1699 -  and empty: "P {#}"
  1.1700 -  and insert: "\<And>a F. a \<in># A \<Longrightarrow> P F \<Longrightarrow> P (F + {#a#})"
  1.1701 -shows "P F"
  1.1702 -proof -
  1.1703 -  from `F \<subseteq># A`
  1.1704 -  show ?thesis
  1.1705 -  proof (induct F)
  1.1706 -    show "P {#}" by fact
  1.1707 -  next
  1.1708 -    fix x F
  1.1709 -    assume P: "F \<subseteq># A \<Longrightarrow> P F" and i: "F + {#x#} \<subseteq># A"
  1.1710 -    show "P (F + {#x#})"
  1.1711 -    proof (rule insert)
  1.1712 -      from i show "x \<in># A" by (auto dest: mset_le_insertD)
  1.1713 -      from i have "F \<subseteq># A" by (auto dest: mset_le_insertD)
  1.1714 -      with P show "P F" .
  1.1715 -    qed
  1.1716 -  qed
  1.1717 -qed 
  1.1718 -
  1.1719 -text{* A consequence: Extensionality. *}
  1.1720 -
  1.1721 -lemma multi_count_eq: "(\<forall>x. count A x = count B x) = (A = B)"
  1.1722 -apply (rule iffI)
  1.1723 - prefer 2
  1.1724 - apply clarsimp 
  1.1725 -apply (induct A arbitrary: B rule: full_multiset_induct)
  1.1726 -apply (rename_tac C)
  1.1727 -apply (case_tac B rule: multiset_cases)
  1.1728 - apply (simp add: empty_multiset_count)
  1.1729 -apply simp
  1.1730 -apply (case_tac "x \<in># C")
  1.1731 - apply (force dest: multi_member_split)
  1.1732 -apply (erule_tac x = x in allE)
  1.1733 -apply simp
  1.1734 -done
  1.1735 -
  1.1736 -lemmas multi_count_ext = multi_count_eq [THEN iffD1, rule_format]
  1.1737 -
  1.1738 -
  1.1739  subsection {* The fold combinator *}
  1.1740  
  1.1741  text {*
  1.1742 @@ -1282,9 +1399,7 @@
  1.1743  lemma fold_mset_empty[simp]: "fold_mset f z {#} = z"
  1.1744  unfolding fold_mset_def by blast
  1.1745  
  1.1746 -locale left_commutative = 
  1.1747 -fixes f :: "'a => 'b => 'b"
  1.1748 -assumes left_commute: "f x (f y z) = f y (f x z)"
  1.1749 +context fun_left_comm
  1.1750  begin
  1.1751  
  1.1752  lemma fold_msetG_determ:
  1.1753 @@ -1324,7 +1439,7 @@
  1.1754          have cinB: "c \<in># B" and binC: "b \<in># C" using MBb MCc diff
  1.1755            by (auto intro: insert_noteq_member dest: sym)
  1.1756          have "B - {#c#} \<subset># B" using cinB by (rule mset_less_diff_self)
  1.1757 -        then have DsubM: "?D \<subset># M" using BsubM by (blast intro: mset_less_trans)
  1.1758 +        then have DsubM: "?D \<subset># M" using BsubM by (blast intro: mset_order.less_trans)
  1.1759          from MBb MCc have "B + {#b#} = C + {#c#}" by blast
  1.1760          then have [simp]: "B + {#b#} - {#c#} = C"
  1.1761            using MBb MCc binC cinB by auto
  1.1762 @@ -1342,7 +1457,7 @@
  1.1763              dest: fold_msetG.insertI [where x=b])
  1.1764          then have "f b d = v" using IH CsubM Cv by blast
  1.1765          ultimately show ?thesis using x\<^isub>1 x\<^isub>2
  1.1766 -          by (auto simp: left_commute)
  1.1767 +          by (auto simp: fun_left_comm)
  1.1768        qed
  1.1769      qed
  1.1770    qed
  1.1771 @@ -1363,7 +1478,7 @@
  1.1772  
  1.1773  lemma fold_mset_insert:
  1.1774    "fold_mset f z (A + {#x#}) = f x (fold_mset f z A)"
  1.1775 -apply (simp add: fold_mset_def fold_mset_insert_aux union_commute)  
  1.1776 +apply (simp add: fold_mset_def fold_mset_insert_aux add_commute)  
  1.1777  apply (rule the_equality)
  1.1778   apply (auto cong add: conj_cong 
  1.1779       simp add: fold_mset_def [symmetric] fold_mset_equality fold_msetG_nonempty)
  1.1780 @@ -1378,7 +1493,7 @@
  1.1781  done
  1.1782  
  1.1783  lemma fold_mset_commute: "f x (fold_mset f z A) = fold_mset f (f x z) A"
  1.1784 -by (induct A) (auto simp: fold_mset_insert left_commute [of x])
  1.1785 +by (induct A) (auto simp: fold_mset_insert fun_left_comm [of x])
  1.1786  
  1.1787  lemma fold_mset_single [simp]: "fold_mset f z {#x#} = f x z"
  1.1788  using fold_mset_insert [of z "{#}"] by simp
  1.1789 @@ -1389,7 +1504,7 @@
  1.1790    case empty then show ?case by simp
  1.1791  next
  1.1792    case (add A x)
  1.1793 -  have "A + {#x#} + B = (A+B) + {#x#}" by(simp add:union_ac)
  1.1794 +  have "A + {#x#} + B = (A+B) + {#x#}" by (simp add: add_ac)
  1.1795    then have "fold_mset f z (A + {#x#} + B) = f x (fold_mset f z (A + B))" 
  1.1796      by (simp add: fold_mset_insert)
  1.1797    also have "\<dots> = fold_mset f (fold_mset f z (A + {#x#})) B"
  1.1798 @@ -1398,10 +1513,10 @@
  1.1799  qed
  1.1800  
  1.1801  lemma fold_mset_fusion:
  1.1802 -  assumes "left_commutative g"
  1.1803 +  assumes "fun_left_comm g"
  1.1804    shows "(\<And>x y. h (g x y) = f x (h y)) \<Longrightarrow> h (fold_mset g w A) = fold_mset f (h w) A" (is "PROP ?P")
  1.1805  proof -
  1.1806 -  interpret left_commutative g by fact
  1.1807 +  interpret fun_left_comm g by (fact assms)
  1.1808    show "PROP ?P" by (induct A) auto
  1.1809  qed
  1.1810  
  1.1811 @@ -1430,11 +1545,11 @@
  1.1812  
  1.1813  subsection {* Image *}
  1.1814  
  1.1815 -definition [code del]:
  1.1816 - "image_mset f = fold_mset (op + o single o f) {#}"
  1.1817 +definition image_mset :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a multiset \<Rightarrow> 'b multiset" where
  1.1818 +  "image_mset f = fold_mset (op + o single o f) {#}"
  1.1819  
  1.1820 -interpretation image_left_comm: left_commutative "op + o single o f"
  1.1821 -  proof qed (simp add:union_ac)
  1.1822 +interpretation image_left_comm: fun_left_comm "op + o single o f"
  1.1823 +proof qed (simp add: add_ac)
  1.1824  
  1.1825  lemma image_mset_empty [simp]: "image_mset f {#} = {#}"
  1.1826  by (simp add: image_mset_def)
  1.1827 @@ -1450,7 +1565,7 @@
  1.1828    "image_mset f (M+N) = image_mset f M + image_mset f N"
  1.1829  apply (induct N)
  1.1830   apply simp
  1.1831 -apply (simp add: union_assoc [symmetric] image_mset_insert)
  1.1832 +apply (simp add: add_assoc [symmetric] image_mset_insert)
  1.1833  done
  1.1834  
  1.1835  lemma size_image_mset [simp]: "size (image_mset f M) = size M"
  1.1836 @@ -1608,7 +1723,7 @@
  1.1837  
  1.1838    val regroup_munion_conv =
  1.1839        Function_Lib.regroup_conv @{const_name Multiset.Mempty} @{const_name plus}
  1.1840 -        (map (fn t => t RS eq_reflection) (@{thms union_ac} @ @{thms empty_idemp}))
  1.1841 +        (map (fn t => t RS eq_reflection) (@{thms add_ac} @ @{thms empty_idemp}))
  1.1842  
  1.1843    fun unfold_pwleq_tac i =
  1.1844      (rtac @{thm pw_leq_step} i THEN (fn st => unfold_pwleq_tac (i + 1) st))
  1.1845 @@ -1629,4 +1744,31 @@
  1.1846  end
  1.1847  *}
  1.1848  
  1.1849 -end
  1.1850 +
  1.1851 +subsection {* Legacy theorem bindings *}
  1.1852 +
  1.1853 +lemmas multi_count_eq = multiset_eq_conv_count_eq [symmetric]
  1.1854 +
  1.1855 +lemma union_commute: "M + N = N + (M::'a multiset)"
  1.1856 +  by (fact add_commute)
  1.1857 +
  1.1858 +lemma union_assoc: "(M + N) + K = M + (N + (K::'a multiset))"
  1.1859 +  by (fact add_assoc)
  1.1860 +
  1.1861 +lemma union_lcomm: "M + (N + K) = N + (M + (K::'a multiset))"
  1.1862 +  by (fact add_left_commute)
  1.1863 +
  1.1864 +lemmas union_ac = union_assoc union_commute union_lcomm
  1.1865 +
  1.1866 +lemma union_right_cancel: "M + K = N + K \<longleftrightarrow> M = (N::'a multiset)"
  1.1867 +  by (fact add_right_cancel)
  1.1868 +
  1.1869 +lemma union_left_cancel: "K + M = K + N \<longleftrightarrow> M = (N::'a multiset)"
  1.1870 +  by (fact add_left_cancel)
  1.1871 +
  1.1872 +lemma multi_union_self_other_eq: "(A::'a multiset) + X = A + Y \<Longrightarrow> X = Y"
  1.1873 +  by (fact add_imp_eq)
  1.1874 +
  1.1875 +lemmas mset_less_trans = mset_order.less_trans
  1.1876 +
  1.1877 +end
  1.1878 \ No newline at end of file