# HG changeset patch # User haftmann # Date 1291755516 -3600 # Node ID 7204024077a8c6edcf1390ffc9f949532b082506 # Parent 7e643e07be7f57f67a11952b3c68f78ab32d8940# Parent 36cec0e3491fbfb0f3262aa8e386336e538e2119 merged diff -r 7e643e07be7f -r 7204024077a8 src/HOL/Library/Multiset.thy --- 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 \ multiset" shows "(\x. if P x then M x else 0) \ 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 (\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 (\x. P)" - - text {* Multiset enumeration *} instantiation multiset :: (type) "{zero, plus}" @@ -395,7 +384,7 @@ abbreviation multiset_inter :: "'a multiset \ 'a multiset \ 'a multiset" (infixl "#\" 70) where "multiset_inter \ inf" -lemma multiset_inter_count: +lemma multiset_inter_count [simp]: "count (A #\ 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 \ bool) \ 'a multiset \ 'a multiset" where + "filter P M = Abs_multiset (\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 #\ N) = Multiset.filter P M #\ Multiset.filter P N" by (rule multiset_eqI) simp +syntax + "_MCollect" :: "pttrn \ 'a multiset \ bool \ 'a multiset" ("(1{# _ :# _./ _#})") +syntax (xsymbol) + "_MCollect" :: "pttrn \ 'a multiset \ bool \ 'a multiset" ("(1{# _ \# _./ _#})") +translations + "{#x \# M. P#}" == "CONST Multiset.filter (\x. P) M" + subsubsection {* Set of elements *} @@ -454,7 +466,7 @@ lemma mem_set_of_iff [simp]: "(x \ 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 \ {x. P x}" +lemma set_of_filter [simp]: "set_of {# x:#M. P x #} = set_of M \ {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\xs. P x] + multiset_of [x\xs. \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 (\y. x = y) xs)" by (induct xs) auto @@ -823,7 +835,7 @@ proof (cases "z \# multiset_of xs") case False moreover have "\ z \# 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 \# 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 \ fst) xs)" - by (simp add: multiset_eq_iff count_of_filter) +lemma filter_Bag [code]: + "Multiset.filter P (Bag xs) = Bag (filter (P \ fst) xs)" + by (rule multiset_eqI) (simp add: count_of_filter) lemma mset_less_eq_Bag [code]: "Bag xs \ A \ (\(x, n) \ set xs. count_of xs x \ count A x)" diff -r 7e643e07be7f -r 7204024077a8 src/HOL/Quotient_Examples/FSet.thy --- 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 = {||} \ P" and insert_fset_case: "\x S'. S = insert_fset x S' \ 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: "\x S. P S \ 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: "\x S. \x |\| S; P S\ \ 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 |\| S") (simp_all) @@ -990,10 +990,10 @@ and card_fset_Suc_case: "\S T. Suc (card_fset S) = (card_fset T) \ P S \ 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 |\| 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 "\x. x \ fset A \ x \ 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 "\z. z \ fset A \ z \ 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 |\| 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 *}