--- a/src/HOL/Library/Multiset.thy Wed May 12 22:33:10 2010 -0700
+++ b/src/HOL/Library/Multiset.thy Thu May 13 14:34:05 2010 +0200
@@ -24,13 +24,13 @@
notation (xsymbols)
Melem (infix "\<in>#" 50)
-lemma multiset_eq_conv_count_eq:
+lemma multiset_ext_iff:
"M = N \<longleftrightarrow> (\<forall>a. count M a = count N a)"
by (simp only: count_inject [symmetric] expand_fun_eq)
-lemma multi_count_ext:
+lemma multiset_ext:
"(\<And>x. count A x = count B x) \<Longrightarrow> A = B"
- using multiset_eq_conv_count_eq by auto
+ using multiset_ext_iff by auto
text {*
\medskip Preservation of the representing set @{term multiset}.
@@ -127,7 +127,7 @@
by (simp add: union_def in_multiset multiset_typedef)
instance multiset :: (type) cancel_comm_monoid_add proof
-qed (simp_all add: multiset_eq_conv_count_eq)
+qed (simp_all add: multiset_ext_iff)
subsubsection {* Difference *}
@@ -146,56 +146,62 @@
by (simp add: diff_def in_multiset multiset_typedef)
lemma diff_empty [simp]: "M - {#} = M \<and> {#} - M = {#}"
- by (simp add: Mempty_def diff_def in_multiset multiset_typedef)
+by(simp add: multiset_ext_iff)
+
+lemma diff_cancel[simp]: "A - A = {#}"
+by (rule multiset_ext) simp
-lemma diff_union_inverse2 [simp]: "M + {#a#} - {#a#} = M"
- by (rule multi_count_ext)
- (auto simp del: count_single simp add: union_def diff_def in_multiset multiset_typedef)
+lemma diff_union_cancelR [simp]: "M + N - N = (M::'a multiset)"
+by(simp add: multiset_ext_iff)
-lemma diff_cancel: "A - A = {#}"
- by (rule multi_count_ext) simp
+lemma diff_union_cancelL [simp]: "N + M - N = (M::'a multiset)"
+by(simp add: multiset_ext_iff)
lemma insert_DiffM:
"x \<in># M \<Longrightarrow> {#x#} + (M - {#x#}) = M"
- by (clarsimp simp: multiset_eq_conv_count_eq)
+ by (clarsimp simp: multiset_ext_iff)
lemma insert_DiffM2 [simp]:
"x \<in># M \<Longrightarrow> M - {#x#} + {#x#} = M"
- by (clarsimp simp: multiset_eq_conv_count_eq)
+ by (clarsimp simp: multiset_ext_iff)
lemma diff_right_commute:
"(M::'a multiset) - N - Q = M - Q - N"
- by (auto simp add: multiset_eq_conv_count_eq)
+ by (auto simp add: multiset_ext_iff)
+
+lemma diff_add:
+ "(M::'a multiset) - (N + Q) = M - N - Q"
+by (simp add: multiset_ext_iff)
lemma diff_union_swap:
"a \<noteq> b \<Longrightarrow> M - {#a#} + {#b#} = M + {#b#} - {#a#}"
- by (auto simp add: multiset_eq_conv_count_eq)
+ by (auto simp add: multiset_ext_iff)
lemma diff_union_single_conv:
"a \<in># J \<Longrightarrow> I + J - {#a#} = I + (J - {#a#})"
- by (simp add: multiset_eq_conv_count_eq)
+ by (simp add: multiset_ext_iff)
subsubsection {* Equality of multisets *}
lemma single_not_empty [simp]: "{#a#} \<noteq> {#} \<and> {#} \<noteq> {#a#}"
- by (simp add: multiset_eq_conv_count_eq)
+ by (simp add: multiset_ext_iff)
lemma single_eq_single [simp]: "{#a#} = {#b#} \<longleftrightarrow> a = b"
- by (auto simp add: multiset_eq_conv_count_eq)
+ by (auto simp add: multiset_ext_iff)
lemma union_eq_empty [iff]: "M + N = {#} \<longleftrightarrow> M = {#} \<and> N = {#}"
- by (auto simp add: multiset_eq_conv_count_eq)
+ by (auto simp add: multiset_ext_iff)
lemma empty_eq_union [iff]: "{#} = M + N \<longleftrightarrow> M = {#} \<and> N = {#}"
- by (auto simp add: multiset_eq_conv_count_eq)
+ by (auto simp add: multiset_ext_iff)
lemma multi_self_add_other_not_self [simp]: "M = M + {#x#} \<longleftrightarrow> False"
- by (auto simp add: multiset_eq_conv_count_eq)
+ by (auto simp add: multiset_ext_iff)
lemma diff_single_trivial:
"\<not> x \<in># M \<Longrightarrow> M - {#x#} = M"
- by (auto simp add: multiset_eq_conv_count_eq)
+ by (auto simp add: multiset_ext_iff)
lemma diff_single_eq_union:
"x \<in># M \<Longrightarrow> M - {#x#} = N \<longleftrightarrow> M = N + {#x#}"
@@ -210,27 +216,11 @@
by auto
lemma union_is_single:
- "M + N = {#a#} \<longleftrightarrow> M = {#a#} \<and> N={#} \<or> M = {#} \<and> N = {#a#}" (is "?lhs = ?rhs")
-proof
+ "M + N = {#a#} \<longleftrightarrow> M = {#a#} \<and> N={#} \<or> M = {#} \<and> N = {#a#}" (is "?lhs = ?rhs")proof
assume ?rhs then show ?lhs by auto
next
- assume ?lhs
- then have "\<And>b. count (M + N) b = (if b = a then 1 else 0)" by auto
- then have *: "\<And>b. count M b + count N b = (if b = a then 1 else 0)" by auto
- then have "count M a + count N a = 1" by auto
- then have **: "count M a = 1 \<and> count N a = 0 \<or> count M a = 0 \<and> count N a = 1"
- by auto
- from * have "\<And>b. b \<noteq> a \<Longrightarrow> count M b + count N b = 0" by auto
- then have ***: "\<And>b. b \<noteq> a \<Longrightarrow> count M b = 0 \<and> count N b = 0" by auto
- from ** and *** have
- "(\<forall>b. count M b = (if b = a then 1 else 0) \<and> count N b = 0) \<or>
- (\<forall>b. count M b = 0 \<and> count N b = (if b = a then 1 else 0))"
- by auto
- then have
- "(\<forall>b. count M b = (if b = a then 1 else 0)) \<and> (\<forall>b. count N b = 0) \<or>
- (\<forall>b. count M b = 0) \<and> (\<forall>b. count N b = (if b = a then 1 else 0))"
- by auto
- then show ?rhs by (auto simp add: multiset_eq_conv_count_eq)
+ assume ?lhs thus ?rhs
+ by(simp add: multiset_ext_iff split:if_splits) (metis add_is_1)
qed
lemma single_is_union:
@@ -239,6 +229,7 @@
lemma add_eq_conv_diff:
"M + {#a#} = N + {#b#} \<longleftrightarrow> M = N \<and> a = b \<or> M = N - {#a#} + {#b#} \<and> N = M - {#b#} + {#a#}" (is "?lhs = ?rhs")
+(* shorter: by (simp add: multiset_ext_iff) fastsimp *)
proof
assume ?rhs then show ?lhs
by (auto simp add: add_assoc add_commute [of "{#b#}"])
@@ -287,7 +278,7 @@
mset_less_def: "(A::'a multiset) < B \<longleftrightarrow> A \<le> B \<and> A \<noteq> B"
instance proof
-qed (auto simp add: mset_le_def mset_less_def multiset_eq_conv_count_eq intro: order_trans antisym)
+qed (auto simp add: mset_le_def mset_less_def multiset_ext_iff intro: order_trans antisym)
end
@@ -298,7 +289,7 @@
lemma mset_le_exists_conv:
"(A::'a multiset) \<le> B \<longleftrightarrow> (\<exists>C. B = A + C)"
apply (unfold mset_le_def, rule iffI, rule_tac x = "B - A" in exI)
-apply (auto intro: multiset_eq_conv_count_eq [THEN iffD2])
+apply (auto intro: multiset_ext_iff [THEN iffD2])
done
lemma mset_le_mono_add_right_cancel [simp]:
@@ -327,11 +318,11 @@
lemma multiset_diff_union_assoc:
"C \<le> B \<Longrightarrow> (A::'a multiset) + B - C = A + (B - C)"
- by (simp add: multiset_eq_conv_count_eq mset_le_def)
+ by (simp add: multiset_ext_iff mset_le_def)
lemma mset_le_multiset_union_diff_commute:
"B \<le> A \<Longrightarrow> (A::'a multiset) - B + C = A + C - B"
-by (simp add: multiset_eq_conv_count_eq mset_le_def)
+by (simp add: multiset_ext_iff mset_le_def)
lemma mset_lessD: "A < B \<Longrightarrow> x \<in># A \<Longrightarrow> x \<in># B"
apply (clarsimp simp: mset_le_def mset_less_def)
@@ -361,7 +352,7 @@
done
lemma mset_less_of_empty[simp]: "A < {#} \<longleftrightarrow> False"
- by (auto simp add: mset_less_def mset_le_def multiset_eq_conv_count_eq)
+ by (auto simp add: mset_less_def mset_le_def multiset_ext_iff)
lemma multi_psub_of_add_self[simp]: "A < A + {#x#}"
by (auto simp: mset_le_def mset_less_def)
@@ -379,7 +370,7 @@
lemma mset_less_diff_self:
"c \<in># B \<Longrightarrow> B - {#c#} < B"
- by (auto simp: mset_le_def mset_less_def multiset_eq_conv_count_eq)
+ by (auto simp: mset_le_def mset_less_def multiset_ext_iff)
subsubsection {* Intersection *}
@@ -406,15 +397,15 @@
by (simp add: multiset_inter_def multiset_typedef)
lemma multiset_inter_single: "a \<noteq> b \<Longrightarrow> {#a#} #\<inter> {#b#} = {#}"
- by (rule multi_count_ext) (auto simp add: multiset_inter_count)
+ by (rule multiset_ext) (auto simp add: multiset_inter_count)
lemma multiset_union_diff_commute:
assumes "B #\<inter> C = {#}"
shows "A + B - C = A - C + B"
-proof (rule multi_count_ext)
+proof (rule multiset_ext)
fix x
from assms have "min (count B x) (count C x) = 0"
- by (auto simp add: multiset_inter_count multiset_eq_conv_count_eq)
+ by (auto simp add: multiset_inter_count multiset_ext_iff)
then have "count B x = 0 \<or> count C x = 0"
by auto
then show "count (A + B - C) x = count (A - C + B) x"
@@ -429,15 +420,15 @@
by (simp add: MCollect_def in_multiset multiset_typedef)
lemma MCollect_empty [simp]: "MCollect {#} P = {#}"
- by (rule multi_count_ext) simp
+ by (rule multiset_ext) simp
lemma MCollect_single [simp]:
"MCollect {#x#} P = (if P x then {#x#} else {#})"
- by (rule multi_count_ext) simp
+ by (rule multiset_ext) simp
lemma MCollect_union [simp]:
"MCollect (M + N) f = MCollect M f + MCollect N f"
- by (rule multi_count_ext) simp
+ by (rule multiset_ext) simp
subsubsection {* Set of elements *}
@@ -455,7 +446,7 @@
by (auto simp add: set_of_def)
lemma set_of_eq_empty_iff [simp]: "(set_of M = {}) = (M = {#})"
-by (auto simp add: set_of_def multiset_eq_conv_count_eq)
+by (auto simp add: set_of_def multiset_ext_iff)
lemma mem_set_of_iff [simp]: "(x \<in> set_of M) = (x :# M)"
by (auto simp add: set_of_def)
@@ -503,7 +494,7 @@
done
lemma size_eq_0_iff_empty [iff]: "(size M = 0) = (M = {#})"
-by (auto simp add: size_def multiset_eq_conv_count_eq)
+by (auto simp add: size_def multiset_ext_iff)
lemma nonempty_has_size: "(S \<noteq> {#}) = (0 < size S)"
by (metis gr0I gr_implies_not0 size_empty size_eq_0_iff_empty)
@@ -624,7 +615,7 @@
by (cases "B = {#}") (auto dest: multi_member_split)
lemma multiset_partition: "M = {# x:#M. P x #} + {# x:#M. \<not> P x #}"
-apply (subst multiset_eq_conv_count_eq)
+apply (subst multiset_ext_iff)
apply auto
done
@@ -756,12 +747,12 @@
lemma multiset_of_eq_setD:
"multiset_of xs = multiset_of ys \<Longrightarrow> set xs = set ys"
-by (rule) (auto simp add:multiset_eq_conv_count_eq set_count_greater_0)
+by (rule) (auto simp add:multiset_ext_iff set_count_greater_0)
lemma set_eq_iff_multiset_of_eq_distinct:
"distinct x \<Longrightarrow> distinct y \<Longrightarrow>
(set x = set y) = (multiset_of x = multiset_of y)"
-by (auto simp: multiset_eq_conv_count_eq distinct_count_atmost_1)
+by (auto simp: multiset_ext_iff distinct_count_atmost_1)
lemma set_eq_iff_multiset_of_remdups_eq:
"(set x = set y) = (multiset_of (remdups x) = multiset_of (remdups y))"
@@ -787,8 +778,9 @@
apply auto
done
-lemma multiset_of_remove1: "multiset_of (remove1 a xs) = multiset_of xs - {#a#}"
-by (induct xs) (auto simp add: multiset_eq_conv_count_eq)
+lemma multiset_of_remove1[simp]:
+ "multiset_of (remove1 a xs) = multiset_of xs - {#a#}"
+by (induct xs) (auto simp add: multiset_ext_iff)
lemma multiset_of_eq_length:
assumes "multiset_of xs = multiset_of ys"
@@ -925,15 +917,15 @@
lemma Mempty_Bag [code]:
"{#} = Bag []"
- by (simp add: multiset_eq_conv_count_eq)
+ by (simp add: multiset_ext_iff)
lemma single_Bag [code]:
"{#x#} = Bag [(x, 1)]"
- by (simp add: multiset_eq_conv_count_eq)
+ by (simp add: multiset_ext_iff)
lemma MCollect_Bag [code]:
"MCollect (Bag xs) P = Bag (filter (P \<circ> fst) xs)"
- by (simp add: multiset_eq_conv_count_eq count_of_filter)
+ by (simp add: multiset_ext_iff count_of_filter)
lemma mset_less_eq_Bag [code]:
"Bag xs \<le> A \<longleftrightarrow> (\<forall>(x, n) \<in> set xs. count_of xs x \<le> count A x)"
@@ -1140,10 +1132,10 @@
apply (rule_tac x = "J + {#a#}" in exI)
apply (rule_tac x = "K + Ka" in exI)
apply (rule conjI)
- apply (simp add: multiset_eq_conv_count_eq split: nat_diff_split)
+ apply (simp add: multiset_ext_iff split: nat_diff_split)
apply (rule conjI)
apply (drule_tac f = "\<lambda>M. M - {#a#}" in arg_cong, simp)
- apply (simp add: multiset_eq_conv_count_eq split: nat_diff_split)
+ apply (simp add: multiset_ext_iff split: nat_diff_split)
apply (simp (no_asm_use) add: trans_def)
apply blast
apply (subgoal_tac "a :# (M0 + {#a#})")
@@ -1658,7 +1650,7 @@
subsection {* Legacy theorem bindings *}
-lemmas multi_count_eq = multiset_eq_conv_count_eq [symmetric]
+lemmas multi_count_eq = multiset_ext_iff [symmetric]
lemma union_commute: "M + N = N + (M::'a multiset)"
by (fact add_commute)