1.1 --- a/src/HOL/Library/Multiset.thy Wed May 12 22:33:10 2010 -0700
1.2 +++ b/src/HOL/Library/Multiset.thy Thu May 13 14:34:05 2010 +0200
1.3 @@ -24,13 +24,13 @@
1.4 notation (xsymbols)
1.5 Melem (infix "\<in>#" 50)
1.6
1.7 -lemma multiset_eq_conv_count_eq:
1.8 +lemma multiset_ext_iff:
1.9 "M = N \<longleftrightarrow> (\<forall>a. count M a = count N a)"
1.10 by (simp only: count_inject [symmetric] expand_fun_eq)
1.11
1.12 -lemma multi_count_ext:
1.13 +lemma multiset_ext:
1.14 "(\<And>x. count A x = count B x) \<Longrightarrow> A = B"
1.15 - using multiset_eq_conv_count_eq by auto
1.16 + using multiset_ext_iff by auto
1.17
1.18 text {*
1.19 \medskip Preservation of the representing set @{term multiset}.
1.20 @@ -127,7 +127,7 @@
1.21 by (simp add: union_def in_multiset multiset_typedef)
1.22
1.23 instance multiset :: (type) cancel_comm_monoid_add proof
1.24 -qed (simp_all add: multiset_eq_conv_count_eq)
1.25 +qed (simp_all add: multiset_ext_iff)
1.26
1.27
1.28 subsubsection {* Difference *}
1.29 @@ -146,56 +146,62 @@
1.30 by (simp add: diff_def in_multiset multiset_typedef)
1.31
1.32 lemma diff_empty [simp]: "M - {#} = M \<and> {#} - M = {#}"
1.33 - by (simp add: Mempty_def diff_def in_multiset multiset_typedef)
1.34 +by(simp add: multiset_ext_iff)
1.35
1.36 -lemma diff_union_inverse2 [simp]: "M + {#a#} - {#a#} = M"
1.37 - by (rule multi_count_ext)
1.38 - (auto simp del: count_single simp add: union_def diff_def in_multiset multiset_typedef)
1.39 +lemma diff_cancel[simp]: "A - A = {#}"
1.40 +by (rule multiset_ext) simp
1.41
1.42 -lemma diff_cancel: "A - A = {#}"
1.43 - by (rule multi_count_ext) simp
1.44 +lemma diff_union_cancelR [simp]: "M + N - N = (M::'a multiset)"
1.45 +by(simp add: multiset_ext_iff)
1.46 +
1.47 +lemma diff_union_cancelL [simp]: "N + M - N = (M::'a multiset)"
1.48 +by(simp add: multiset_ext_iff)
1.49
1.50 lemma insert_DiffM:
1.51 "x \<in># M \<Longrightarrow> {#x#} + (M - {#x#}) = M"
1.52 - by (clarsimp simp: multiset_eq_conv_count_eq)
1.53 + by (clarsimp simp: multiset_ext_iff)
1.54
1.55 lemma insert_DiffM2 [simp]:
1.56 "x \<in># M \<Longrightarrow> M - {#x#} + {#x#} = M"
1.57 - by (clarsimp simp: multiset_eq_conv_count_eq)
1.58 + by (clarsimp simp: multiset_ext_iff)
1.59
1.60 lemma diff_right_commute:
1.61 "(M::'a multiset) - N - Q = M - Q - N"
1.62 - by (auto simp add: multiset_eq_conv_count_eq)
1.63 + by (auto simp add: multiset_ext_iff)
1.64 +
1.65 +lemma diff_add:
1.66 + "(M::'a multiset) - (N + Q) = M - N - Q"
1.67 +by (simp add: multiset_ext_iff)
1.68
1.69 lemma diff_union_swap:
1.70 "a \<noteq> b \<Longrightarrow> M - {#a#} + {#b#} = M + {#b#} - {#a#}"
1.71 - by (auto simp add: multiset_eq_conv_count_eq)
1.72 + by (auto simp add: multiset_ext_iff)
1.73
1.74 lemma diff_union_single_conv:
1.75 "a \<in># J \<Longrightarrow> I + J - {#a#} = I + (J - {#a#})"
1.76 - by (simp add: multiset_eq_conv_count_eq)
1.77 + by (simp add: multiset_ext_iff)
1.78
1.79
1.80 subsubsection {* Equality of multisets *}
1.81
1.82 lemma single_not_empty [simp]: "{#a#} \<noteq> {#} \<and> {#} \<noteq> {#a#}"
1.83 - by (simp add: multiset_eq_conv_count_eq)
1.84 + by (simp add: multiset_ext_iff)
1.85
1.86 lemma single_eq_single [simp]: "{#a#} = {#b#} \<longleftrightarrow> a = b"
1.87 - by (auto simp add: multiset_eq_conv_count_eq)
1.88 + by (auto simp add: multiset_ext_iff)
1.89
1.90 lemma union_eq_empty [iff]: "M + N = {#} \<longleftrightarrow> M = {#} \<and> N = {#}"
1.91 - by (auto simp add: multiset_eq_conv_count_eq)
1.92 + by (auto simp add: multiset_ext_iff)
1.93
1.94 lemma empty_eq_union [iff]: "{#} = M + N \<longleftrightarrow> M = {#} \<and> N = {#}"
1.95 - by (auto simp add: multiset_eq_conv_count_eq)
1.96 + by (auto simp add: multiset_ext_iff)
1.97
1.98 lemma multi_self_add_other_not_self [simp]: "M = M + {#x#} \<longleftrightarrow> False"
1.99 - by (auto simp add: multiset_eq_conv_count_eq)
1.100 + by (auto simp add: multiset_ext_iff)
1.101
1.102 lemma diff_single_trivial:
1.103 "\<not> x \<in># M \<Longrightarrow> M - {#x#} = M"
1.104 - by (auto simp add: multiset_eq_conv_count_eq)
1.105 + by (auto simp add: multiset_ext_iff)
1.106
1.107 lemma diff_single_eq_union:
1.108 "x \<in># M \<Longrightarrow> M - {#x#} = N \<longleftrightarrow> M = N + {#x#}"
1.109 @@ -210,27 +216,11 @@
1.110 by auto
1.111
1.112 lemma union_is_single:
1.113 - "M + N = {#a#} \<longleftrightarrow> M = {#a#} \<and> N={#} \<or> M = {#} \<and> N = {#a#}" (is "?lhs = ?rhs")
1.114 -proof
1.115 + "M + N = {#a#} \<longleftrightarrow> M = {#a#} \<and> N={#} \<or> M = {#} \<and> N = {#a#}" (is "?lhs = ?rhs")proof
1.116 assume ?rhs then show ?lhs by auto
1.117 next
1.118 - assume ?lhs
1.119 - then have "\<And>b. count (M + N) b = (if b = a then 1 else 0)" by auto
1.120 - then have *: "\<And>b. count M b + count N b = (if b = a then 1 else 0)" by auto
1.121 - then have "count M a + count N a = 1" by auto
1.122 - then have **: "count M a = 1 \<and> count N a = 0 \<or> count M a = 0 \<and> count N a = 1"
1.123 - by auto
1.124 - from * have "\<And>b. b \<noteq> a \<Longrightarrow> count M b + count N b = 0" by auto
1.125 - then have ***: "\<And>b. b \<noteq> a \<Longrightarrow> count M b = 0 \<and> count N b = 0" by auto
1.126 - from ** and *** have
1.127 - "(\<forall>b. count M b = (if b = a then 1 else 0) \<and> count N b = 0) \<or>
1.128 - (\<forall>b. count M b = 0 \<and> count N b = (if b = a then 1 else 0))"
1.129 - by auto
1.130 - then have
1.131 - "(\<forall>b. count M b = (if b = a then 1 else 0)) \<and> (\<forall>b. count N b = 0) \<or>
1.132 - (\<forall>b. count M b = 0) \<and> (\<forall>b. count N b = (if b = a then 1 else 0))"
1.133 - by auto
1.134 - then show ?rhs by (auto simp add: multiset_eq_conv_count_eq)
1.135 + assume ?lhs thus ?rhs
1.136 + by(simp add: multiset_ext_iff split:if_splits) (metis add_is_1)
1.137 qed
1.138
1.139 lemma single_is_union:
1.140 @@ -239,6 +229,7 @@
1.141
1.142 lemma add_eq_conv_diff:
1.143 "M + {#a#} = N + {#b#} \<longleftrightarrow> M = N \<and> a = b \<or> M = N - {#a#} + {#b#} \<and> N = M - {#b#} + {#a#}" (is "?lhs = ?rhs")
1.144 +(* shorter: by (simp add: multiset_ext_iff) fastsimp *)
1.145 proof
1.146 assume ?rhs then show ?lhs
1.147 by (auto simp add: add_assoc add_commute [of "{#b#}"])
1.148 @@ -287,7 +278,7 @@
1.149 mset_less_def: "(A::'a multiset) < B \<longleftrightarrow> A \<le> B \<and> A \<noteq> B"
1.150
1.151 instance proof
1.152 -qed (auto simp add: mset_le_def mset_less_def multiset_eq_conv_count_eq intro: order_trans antisym)
1.153 +qed (auto simp add: mset_le_def mset_less_def multiset_ext_iff intro: order_trans antisym)
1.154
1.155 end
1.156
1.157 @@ -298,7 +289,7 @@
1.158 lemma mset_le_exists_conv:
1.159 "(A::'a multiset) \<le> B \<longleftrightarrow> (\<exists>C. B = A + C)"
1.160 apply (unfold mset_le_def, rule iffI, rule_tac x = "B - A" in exI)
1.161 -apply (auto intro: multiset_eq_conv_count_eq [THEN iffD2])
1.162 +apply (auto intro: multiset_ext_iff [THEN iffD2])
1.163 done
1.164
1.165 lemma mset_le_mono_add_right_cancel [simp]:
1.166 @@ -327,11 +318,11 @@
1.167
1.168 lemma multiset_diff_union_assoc:
1.169 "C \<le> B \<Longrightarrow> (A::'a multiset) + B - C = A + (B - C)"
1.170 - by (simp add: multiset_eq_conv_count_eq mset_le_def)
1.171 + by (simp add: multiset_ext_iff mset_le_def)
1.172
1.173 lemma mset_le_multiset_union_diff_commute:
1.174 "B \<le> A \<Longrightarrow> (A::'a multiset) - B + C = A + C - B"
1.175 -by (simp add: multiset_eq_conv_count_eq mset_le_def)
1.176 +by (simp add: multiset_ext_iff mset_le_def)
1.177
1.178 lemma mset_lessD: "A < B \<Longrightarrow> x \<in># A \<Longrightarrow> x \<in># B"
1.179 apply (clarsimp simp: mset_le_def mset_less_def)
1.180 @@ -361,7 +352,7 @@
1.181 done
1.182
1.183 lemma mset_less_of_empty[simp]: "A < {#} \<longleftrightarrow> False"
1.184 - by (auto simp add: mset_less_def mset_le_def multiset_eq_conv_count_eq)
1.185 + by (auto simp add: mset_less_def mset_le_def multiset_ext_iff)
1.186
1.187 lemma multi_psub_of_add_self[simp]: "A < A + {#x#}"
1.188 by (auto simp: mset_le_def mset_less_def)
1.189 @@ -379,7 +370,7 @@
1.190
1.191 lemma mset_less_diff_self:
1.192 "c \<in># B \<Longrightarrow> B - {#c#} < B"
1.193 - by (auto simp: mset_le_def mset_less_def multiset_eq_conv_count_eq)
1.194 + by (auto simp: mset_le_def mset_less_def multiset_ext_iff)
1.195
1.196
1.197 subsubsection {* Intersection *}
1.198 @@ -406,15 +397,15 @@
1.199 by (simp add: multiset_inter_def multiset_typedef)
1.200
1.201 lemma multiset_inter_single: "a \<noteq> b \<Longrightarrow> {#a#} #\<inter> {#b#} = {#}"
1.202 - by (rule multi_count_ext) (auto simp add: multiset_inter_count)
1.203 + by (rule multiset_ext) (auto simp add: multiset_inter_count)
1.204
1.205 lemma multiset_union_diff_commute:
1.206 assumes "B #\<inter> C = {#}"
1.207 shows "A + B - C = A - C + B"
1.208 -proof (rule multi_count_ext)
1.209 +proof (rule multiset_ext)
1.210 fix x
1.211 from assms have "min (count B x) (count C x) = 0"
1.212 - by (auto simp add: multiset_inter_count multiset_eq_conv_count_eq)
1.213 + by (auto simp add: multiset_inter_count multiset_ext_iff)
1.214 then have "count B x = 0 \<or> count C x = 0"
1.215 by auto
1.216 then show "count (A + B - C) x = count (A - C + B) x"
1.217 @@ -429,15 +420,15 @@
1.218 by (simp add: MCollect_def in_multiset multiset_typedef)
1.219
1.220 lemma MCollect_empty [simp]: "MCollect {#} P = {#}"
1.221 - by (rule multi_count_ext) simp
1.222 + by (rule multiset_ext) simp
1.223
1.224 lemma MCollect_single [simp]:
1.225 "MCollect {#x#} P = (if P x then {#x#} else {#})"
1.226 - by (rule multi_count_ext) simp
1.227 + by (rule multiset_ext) simp
1.228
1.229 lemma MCollect_union [simp]:
1.230 "MCollect (M + N) f = MCollect M f + MCollect N f"
1.231 - by (rule multi_count_ext) simp
1.232 + by (rule multiset_ext) simp
1.233
1.234
1.235 subsubsection {* Set of elements *}
1.236 @@ -455,7 +446,7 @@
1.237 by (auto simp add: set_of_def)
1.238
1.239 lemma set_of_eq_empty_iff [simp]: "(set_of M = {}) = (M = {#})"
1.240 -by (auto simp add: set_of_def multiset_eq_conv_count_eq)
1.241 +by (auto simp add: set_of_def multiset_ext_iff)
1.242
1.243 lemma mem_set_of_iff [simp]: "(x \<in> set_of M) = (x :# M)"
1.244 by (auto simp add: set_of_def)
1.245 @@ -503,7 +494,7 @@
1.246 done
1.247
1.248 lemma size_eq_0_iff_empty [iff]: "(size M = 0) = (M = {#})"
1.249 -by (auto simp add: size_def multiset_eq_conv_count_eq)
1.250 +by (auto simp add: size_def multiset_ext_iff)
1.251
1.252 lemma nonempty_has_size: "(S \<noteq> {#}) = (0 < size S)"
1.253 by (metis gr0I gr_implies_not0 size_empty size_eq_0_iff_empty)
1.254 @@ -624,7 +615,7 @@
1.255 by (cases "B = {#}") (auto dest: multi_member_split)
1.256
1.257 lemma multiset_partition: "M = {# x:#M. P x #} + {# x:#M. \<not> P x #}"
1.258 -apply (subst multiset_eq_conv_count_eq)
1.259 +apply (subst multiset_ext_iff)
1.260 apply auto
1.261 done
1.262
1.263 @@ -756,12 +747,12 @@
1.264
1.265 lemma multiset_of_eq_setD:
1.266 "multiset_of xs = multiset_of ys \<Longrightarrow> set xs = set ys"
1.267 -by (rule) (auto simp add:multiset_eq_conv_count_eq set_count_greater_0)
1.268 +by (rule) (auto simp add:multiset_ext_iff set_count_greater_0)
1.269
1.270 lemma set_eq_iff_multiset_of_eq_distinct:
1.271 "distinct x \<Longrightarrow> distinct y \<Longrightarrow>
1.272 (set x = set y) = (multiset_of x = multiset_of y)"
1.273 -by (auto simp: multiset_eq_conv_count_eq distinct_count_atmost_1)
1.274 +by (auto simp: multiset_ext_iff distinct_count_atmost_1)
1.275
1.276 lemma set_eq_iff_multiset_of_remdups_eq:
1.277 "(set x = set y) = (multiset_of (remdups x) = multiset_of (remdups y))"
1.278 @@ -787,8 +778,9 @@
1.279 apply auto
1.280 done
1.281
1.282 -lemma multiset_of_remove1: "multiset_of (remove1 a xs) = multiset_of xs - {#a#}"
1.283 -by (induct xs) (auto simp add: multiset_eq_conv_count_eq)
1.284 +lemma multiset_of_remove1[simp]:
1.285 + "multiset_of (remove1 a xs) = multiset_of xs - {#a#}"
1.286 +by (induct xs) (auto simp add: multiset_ext_iff)
1.287
1.288 lemma multiset_of_eq_length:
1.289 assumes "multiset_of xs = multiset_of ys"
1.290 @@ -925,15 +917,15 @@
1.291
1.292 lemma Mempty_Bag [code]:
1.293 "{#} = Bag []"
1.294 - by (simp add: multiset_eq_conv_count_eq)
1.295 + by (simp add: multiset_ext_iff)
1.296
1.297 lemma single_Bag [code]:
1.298 "{#x#} = Bag [(x, 1)]"
1.299 - by (simp add: multiset_eq_conv_count_eq)
1.300 + by (simp add: multiset_ext_iff)
1.301
1.302 lemma MCollect_Bag [code]:
1.303 "MCollect (Bag xs) P = Bag (filter (P \<circ> fst) xs)"
1.304 - by (simp add: multiset_eq_conv_count_eq count_of_filter)
1.305 + by (simp add: multiset_ext_iff count_of_filter)
1.306
1.307 lemma mset_less_eq_Bag [code]:
1.308 "Bag xs \<le> A \<longleftrightarrow> (\<forall>(x, n) \<in> set xs. count_of xs x \<le> count A x)"
1.309 @@ -1140,10 +1132,10 @@
1.310 apply (rule_tac x = "J + {#a#}" in exI)
1.311 apply (rule_tac x = "K + Ka" in exI)
1.312 apply (rule conjI)
1.313 - apply (simp add: multiset_eq_conv_count_eq split: nat_diff_split)
1.314 + apply (simp add: multiset_ext_iff split: nat_diff_split)
1.315 apply (rule conjI)
1.316 apply (drule_tac f = "\<lambda>M. M - {#a#}" in arg_cong, simp)
1.317 - apply (simp add: multiset_eq_conv_count_eq split: nat_diff_split)
1.318 + apply (simp add: multiset_ext_iff split: nat_diff_split)
1.319 apply (simp (no_asm_use) add: trans_def)
1.320 apply blast
1.321 apply (subgoal_tac "a :# (M0 + {#a#})")
1.322 @@ -1658,7 +1650,7 @@
1.323
1.324 subsection {* Legacy theorem bindings *}
1.325
1.326 -lemmas multi_count_eq = multiset_eq_conv_count_eq [symmetric]
1.327 +lemmas multi_count_eq = multiset_ext_iff [symmetric]
1.328
1.329 lemma union_commute: "M + N = N + (M::'a multiset)"
1.330 by (fact add_commute)