--- a/src/HOL/Library/Multiset.thy Tue Dec 07 21:32:47 2010 +0100
+++ b/src/HOL/Library/Multiset.thy Tue Dec 07 21:58:36 2010 +0100
@@ -58,7 +58,7 @@
by (auto simp add: multiset_def intro: finite_subset)
qed
-lemma MCollect_preserves_multiset:
+lemma filter_preserves_multiset:
assumes "M \<in> multiset"
shows "(\<lambda>x. if P x then M x else 0) \<in> multiset"
proof -
@@ -69,22 +69,11 @@
qed
lemmas in_multiset = const0_in_multiset only1_in_multiset
- union_preserves_multiset diff_preserves_multiset MCollect_preserves_multiset
+ union_preserves_multiset diff_preserves_multiset filter_preserves_multiset
subsection {* Representing multisets *}
-text {* Multiset comprehension *}
-
-definition MCollect :: "'a multiset => ('a => bool) => 'a multiset" where
- "MCollect M P = Abs_multiset (\<lambda>x. if P x then count M x else 0)"
-
-syntax
- "_MCollect" :: "pttrn => 'a multiset => bool => 'a multiset" ("(1{# _ :# _./ _#})")
-translations
- "{#x :# M. P#}" == "CONST MCollect M (\<lambda>x. P)"
-
-
text {* Multiset enumeration *}
instantiation multiset :: (type) "{zero, plus}"
@@ -395,7 +384,7 @@
abbreviation multiset_inter :: "'a multiset \<Rightarrow> 'a multiset \<Rightarrow> 'a multiset" (infixl "#\<inter>" 70) where
"multiset_inter \<equiv> inf"
-lemma multiset_inter_count:
+lemma multiset_inter_count [simp]:
"count (A #\<inter> B) x = min (count A x) (count B x)"
by (simp add: multiset_inter_def multiset_typedef)
@@ -416,23 +405,46 @@
qed
-subsubsection {* Comprehension (filter) *}
+subsubsection {* Filter (with comprehension syntax) *}
+
+text {* Multiset comprehension *}
+
+definition filter :: "('a \<Rightarrow> bool) \<Rightarrow> 'a multiset \<Rightarrow> 'a multiset" where
+ "filter P M = Abs_multiset (\<lambda>x. if P x then count M x else 0)"
-lemma count_MCollect [simp]:
- "count {# x:#M. P x #} a = (if P a then count M a else 0)"
- by (simp add: MCollect_def in_multiset multiset_typedef)
+hide_const (open) filter
-lemma MCollect_empty [simp]: "MCollect {#} P = {#}"
+lemma count_filter [simp]:
+ "count (Multiset.filter P M) a = (if P a then count M a else 0)"
+ by (simp add: filter_def in_multiset multiset_typedef)
+
+lemma filter_empty [simp]:
+ "Multiset.filter P {#} = {#}"
by (rule multiset_eqI) simp
-lemma MCollect_single [simp]:
- "MCollect {#x#} P = (if P x then {#x#} else {#})"
+lemma filter_single [simp]:
+ "Multiset.filter P {#x#} = (if P x then {#x#} else {#})"
+ by (rule multiset_eqI) simp
+
+lemma filter_union [simp]:
+ "Multiset.filter P (M + N) = Multiset.filter P M + Multiset.filter P N"
by (rule multiset_eqI) simp
-lemma MCollect_union [simp]:
- "MCollect (M + N) f = MCollect M f + MCollect N f"
+lemma filter_diff [simp]:
+ "Multiset.filter P (M - N) = Multiset.filter P M - Multiset.filter P N"
+ by (rule multiset_eqI) simp
+
+lemma filter_inter [simp]:
+ "Multiset.filter P (M #\<inter> N) = Multiset.filter P M #\<inter> Multiset.filter P N"
by (rule multiset_eqI) simp
+syntax
+ "_MCollect" :: "pttrn \<Rightarrow> 'a multiset \<Rightarrow> bool \<Rightarrow> 'a multiset" ("(1{# _ :# _./ _#})")
+syntax (xsymbol)
+ "_MCollect" :: "pttrn \<Rightarrow> 'a multiset \<Rightarrow> bool \<Rightarrow> 'a multiset" ("(1{# _ \<in># _./ _#})")
+translations
+ "{#x \<in># M. P#}" == "CONST Multiset.filter (\<lambda>x. P) M"
+
subsubsection {* Set of elements *}
@@ -454,7 +466,7 @@
lemma mem_set_of_iff [simp]: "(x \<in> set_of M) = (x :# M)"
by (auto simp add: set_of_def)
-lemma set_of_MCollect [simp]: "set_of {# x:#M. P x #} = set_of M \<inter> {x. P x}"
+lemma set_of_filter [simp]: "set_of {# x:#M. P x #} = set_of M \<inter> {x. P x}"
by (auto simp add: set_of_def)
lemma finite_set_of [iff]: "finite (set_of M)"
@@ -786,7 +798,7 @@
"multiset_of [x\<leftarrow>xs. P x] + multiset_of [x\<leftarrow>xs. \<not>P x] = multiset_of xs"
by (induct xs) (auto simp: add_ac)
-lemma count_filter:
+lemma count_multiset_of_length_filter:
"count (multiset_of xs) x = length (filter (\<lambda>y. x = y) xs)"
by (induct xs) auto
@@ -823,7 +835,7 @@
proof (cases "z \<in># multiset_of xs")
case False
moreover have "\<not> z \<in># multiset_of ys" using assms False by simp
- ultimately show ?thesis by (simp add: count_filter)
+ ultimately show ?thesis by (simp add: count_multiset_of_length_filter)
next
case True
moreover have "z \<in># multiset_of ys" using assms True by simp
@@ -1062,9 +1074,9 @@
"{#x#} = Bag [(x, 1)]"
by (simp add: multiset_eq_iff)
-lemma MCollect_Bag [code]:
- "MCollect (Bag xs) P = Bag (filter (P \<circ> fst) xs)"
- by (simp add: multiset_eq_iff count_of_filter)
+lemma filter_Bag [code]:
+ "Multiset.filter P (Bag xs) = Bag (filter (P \<circ> fst) xs)"
+ by (rule multiset_eqI) (simp add: 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)"
--- a/src/HOL/Quotient_Examples/FSet.thy Tue Dec 07 21:32:47 2010 +0100
+++ b/src/HOL/Quotient_Examples/FSet.thy Tue Dec 07 21:58:36 2010 +0100
@@ -958,28 +958,28 @@
section {* Induction and Cases rules for fsets *}
-lemma fset_exhaust [case_names empty_fset insert_fset, cases type: fset]:
+lemma fset_exhaust [case_names empty insert, cases type: fset]:
assumes empty_fset_case: "S = {||} \<Longrightarrow> P"
and insert_fset_case: "\<And>x S'. S = insert_fset x S' \<Longrightarrow> P"
shows "P"
using assms by (lifting list.exhaust)
-lemma fset_induct [case_names empty_fset insert_fset]:
+lemma fset_induct [case_names empty insert]:
assumes empty_fset_case: "P {||}"
and insert_fset_case: "\<And>x S. P S \<Longrightarrow> P (insert_fset x S)"
shows "P S"
using assms
by (descending) (blast intro: list.induct)
-lemma fset_induct_stronger [case_names empty_fset insert_fset, induct type: fset]:
+lemma fset_induct_stronger [case_names empty insert, induct type: fset]:
assumes empty_fset_case: "P {||}"
and insert_fset_case: "\<And>x S. \<lbrakk>x |\<notin>| S; P S\<rbrakk> \<Longrightarrow> P (insert_fset x S)"
shows "P S"
proof(induct S rule: fset_induct)
- case empty_fset
+ case empty
show "P {||}" using empty_fset_case by simp
next
- case (insert_fset x S)
+ case (insert x S)
have "P S" by fact
then show "P (insert_fset x S)" using insert_fset_case
by (cases "x |\<in>| S") (simp_all)
@@ -990,10 +990,10 @@
and card_fset_Suc_case: "\<And>S T. Suc (card_fset S) = (card_fset T) \<Longrightarrow> P S \<Longrightarrow> P T"
shows "P S"
proof (induct S)
- case empty_fset
+ case empty
show "P {||}" by (rule empty_fset_case)
next
- case (insert_fset x S)
+ case (insert x S)
have h: "P S" by fact
have "x |\<notin>| S" by fact
then have "Suc (card_fset S) = card_fset (insert_fset x S)"
@@ -1058,7 +1058,22 @@
apply simp_all
done
+text {* Extensionality *}
+lemma fset_eqI:
+ assumes "\<And>x. x \<in> fset A \<longleftrightarrow> x \<in> fset B"
+ shows "A = B"
+using assms proof (induct A arbitrary: B)
+ case empty then show ?case
+ by (auto simp add: in_fset none_in_empty_fset [symmetric] sym)
+next
+ case (insert x A)
+ from insert.prems insert.hyps(1) have "\<And>z. z \<in> fset A \<longleftrightarrow> z \<in> fset (B - {|x|})"
+ by (auto simp add: in_fset)
+ then have "A = B - {|x|}" by (rule insert.hyps(2))
+ moreover with insert.prems [symmetric, of x] have "x |\<in>| B" by (simp add: in_fset)
+ ultimately show ?case by (metis in_fset_mdef)
+qed
subsection {* alternate formulation with a different decomposition principle
and a proof of equivalence *}