author haftmann Fri Jan 22 13:38:28 2010 +0100 (2010-01-22) changeset 34943 e97b22500a5c 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
```     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.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.160 -
1.161 -lemma only1_in_multiset: "(\<lambda>b. if b = a then 1 else 0) \<in> multiset"
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.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.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.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.198 -
1.199 -lemma union_assoc: "(M + N) + K = M + (N + (K::'a 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.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.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.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.436 +  "(M + {#a#} = N + {#b#}) =
1.437 +    (M = N \<and> a = b \<or> (\<exists>K. M = K + {#b#} \<and> N = K + {#a#}))"
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.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.507 +    apply (subst multiset_diff_union_assoc)
1.508 +    apply simp
1.509 +    apply (simp add: diff_cancel)
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.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.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.616
1.617  lemma size_single [simp]: "size {#b#} = 1"
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.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.675 -apply (blast dest: sym)
1.676 -done
1.677 -
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.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.732 -  "(M + {#a#} = N + {#b#}) =
1.733 -    (M = N \<and> a = b \<or> (\<exists>K. M = K + {#b#} \<and> N = K + {#a#}))"
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.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.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.811      apply (erule ssubst)
1.812      apply (erule Abs_multiset_inverse [THEN subst])
1.813 -    apply (drule add [unfolded defns, simplified])
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.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.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.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.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.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.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.1249   apply (drule_tac f = "\<lambda>M. M - {#a#}" in arg_cong)
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.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.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.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.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.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.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.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.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.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.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.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.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.1824
1.1825  lemma image_mset_empty [simp]: "image_mset f {#} = {#}"
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.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.1857 +
1.1858 +lemma union_assoc: "(M + N) + K = M + (N + (K::'a multiset))"
1.1860 +
1.1861 +lemma union_lcomm: "M + (N + K) = N + (M + (K::'a multiset))"
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)"