# HG changeset patch # User nipkow # Date 1428661018 -7200 # Node ID 3fa68bacfa2ba7b159a55806a11754fc1b766fca # Parent 90fb391a15c12e64e170b58bcab91c77e6c99368# Parent c54d36be22ef7701f1dd674570eca8a623f07bc6 merged diff -r 90fb391a15c1 -r 3fa68bacfa2b NEWS --- a/NEWS Fri Apr 10 11:52:55 2015 +0200 +++ b/NEWS Fri Apr 10 12:16:58 2015 +0200 @@ -345,6 +345,8 @@ INCOMPATIBILITY. - Renamed in_multiset_of ~> in_multiset_in_set + Multiset.fold ~> fold_mset + Multiset.filter ~> filter_mset INCOMPATIBILITY. - Removed mcard, is equal to size. - Added attributes: diff -r 90fb391a15c1 -r 3fa68bacfa2b src/HOL/Library/DAList_Multiset.thy --- a/src/HOL/Library/DAList_Multiset.thy Fri Apr 10 11:52:55 2015 +0200 +++ b/src/HOL/Library/DAList_Multiset.thy Fri Apr 10 12:16:58 2015 +0200 @@ -24,7 +24,7 @@ lemma [code, code del]: "image_mset = image_mset" .. -lemma [code, code del]: "Multiset.filter = Multiset.filter" .. +lemma [code, code del]: "filter_mset = filter_mset" .. lemma [code, code del]: "count = count" .. @@ -199,7 +199,7 @@ (simp add: count_of_subtract_entries_raw alist.Alist_inverse distinct_subtract_entries_raw subtract_entries_def) -lemma filter_Bag [code]: "Multiset.filter P (Bag xs) = Bag (DAList.filter (P \ fst) xs)" +lemma filter_Bag [code]: "filter_mset P (Bag xs) = Bag (DAList.filter (P \ fst) xs)" by (rule multiset_eqI) (simp add: count_of_filter DAList.filter.rep_eq) @@ -285,7 +285,7 @@ lemma DAList_Multiset_fold: assumes fn: "\a n x. fn a n x = (f a ^^ n) x" - shows "Multiset.fold f e (Bag al) = DAList_Multiset.fold fn e al" + shows "fold_mset f e (Bag al) = DAList_Multiset.fold fn e al" unfolding DAList_Multiset.fold_def proof (induct al) fix ys @@ -294,12 +294,12 @@ have count[simp]: "\x. count (Abs_multiset (count_of x)) = count_of x" by (rule Abs_multiset_inverse[OF count_of_multiset]) assume ys: "ys \ ?inv" - then show "Multiset.fold f e (Bag (Alist ys)) = fold_impl fn e (DAList.impl_of (Alist ys))" + then show "fold_mset f e (Bag (Alist ys)) = fold_impl fn e (DAList.impl_of (Alist ys))" unfolding Bag_def unfolding Alist_inverse[OF ys] proof (induct ys arbitrary: e rule: list.induct) case Nil show ?case - by (rule trans[OF arg_cong[of _ "{#}" "Multiset.fold f e", OF multiset_eqI]]) + by (rule trans[OF arg_cong[of _ "{#}" "fold_mset f e", OF multiset_eqI]]) (auto, simp add: cs) next case (Cons pair ys e) @@ -388,7 +388,7 @@ apply (auto simp: ac_simps) done -lemma size_fold: "size A = Multiset.fold (\_. Suc) 0 A" (is "_ = Multiset.fold ?f _ _") +lemma size_fold: "size A = fold_mset (\_. Suc) 0 A" (is "_ = fold_mset ?f _ _") proof - interpret comp_fun_commute ?f by default auto show ?thesis by (induct A) auto @@ -403,7 +403,7 @@ qed -lemma set_of_fold: "set_of A = Multiset.fold insert {} A" (is "_ = Multiset.fold ?f _ _") +lemma set_of_fold: "set_of A = fold_mset insert {} A" (is "_ = fold_mset ?f _ _") proof - interpret comp_fun_commute ?f by default auto show ?thesis by (induct A) auto diff -r 90fb391a15c1 -r 3fa68bacfa2b src/HOL/Library/Multiset.thy --- a/src/HOL/Library/Multiset.thy Fri Apr 10 11:52:55 2015 +0200 +++ b/src/HOL/Library/Multiset.thy Fri Apr 10 12:16:58 2015 +0200 @@ -527,40 +527,39 @@ text {* Multiset comprehension *} -lift_definition filter :: "('a \ bool) \ 'a multiset \ 'a multiset" is "\P M. \x. if P x then M x else 0" +lift_definition filter_mset :: "('a \ bool) \ 'a multiset \ 'a multiset" +is "\P M. \x. if P x then M x else 0" by (rule filter_preserves_multiset) -hide_const (open) filter - -lemma count_filter [simp]: - "count (Multiset.filter P M) a = (if P a then count M a else 0)" - by (simp add: filter.rep_eq) - -lemma filter_empty [simp]: - "Multiset.filter P {#} = {#}" +lemma count_filter_mset [simp]: + "count (filter_mset P M) a = (if P a then count M a else 0)" + by (simp add: filter_mset.rep_eq) + +lemma filter_empty_mset [simp]: + "filter_mset P {#} = {#}" + by (rule multiset_eqI) simp + +lemma filter_single_mset [simp]: + "filter_mset P {#x#} = (if P x then {#x#} else {#})" by (rule multiset_eqI) simp -lemma filter_single [simp]: - "Multiset.filter P {#x#} = (if P x then {#x#} else {#})" +lemma filter_union_mset [simp]: + "filter_mset P (M + N) = filter_mset P M + filter_mset P N" by (rule multiset_eqI) simp -lemma filter_union [simp]: - "Multiset.filter P (M + N) = Multiset.filter P M + Multiset.filter P N" +lemma filter_diff_mset [simp]: + "filter_mset P (M - N) = filter_mset P M - filter_mset P N" by (rule multiset_eqI) simp -lemma filter_diff [simp]: - "Multiset.filter P (M - N) = Multiset.filter P M - Multiset.filter P N" +lemma filter_inter_mset [simp]: + "filter_mset P (M #\ N) = filter_mset P M #\ filter_mset 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 - -lemma multiset_filter_subset[simp]: "Multiset.filter f M \ M" +lemma multiset_filter_subset[simp]: "filter_mset f M \ M" unfolding less_eq_multiset.rep_eq by auto lemma multiset_filter_mono: assumes "A \ B" - shows "Multiset.filter f A \ Multiset.filter f B" + shows "filter_mset f A \ filter_mset f B" proof - from assms[unfolded mset_le_exists_conv] obtain C where B: "B = A + C" by auto @@ -572,7 +571,7 @@ syntax (xsymbol) "_MCollect" :: "pttrn \ 'a multiset \ bool \ 'a multiset" ("(1{# _ \# _./ _#})") translations - "{#x \# M. P#}" == "CONST Multiset.filter (\x. P) M" + "{#x \# M. P#}" == "CONST filter_mset (\x. P) M" subsubsection {* Set of elements *} @@ -694,7 +693,7 @@ show ?thesis unfolding B by (induct C, auto) qed -lemma size_filter_mset_lesseq[simp]: "size (Multiset.filter f M) \ size M" +lemma size_filter_mset_lesseq[simp]: "size (filter_mset f M) \ size M" by (rule size_mset_mono[OF multiset_filter_subset]) lemma size_Diff_submset: @@ -798,19 +797,19 @@ subsection {* The fold combinator *} -definition fold :: "('a \ 'b \ 'b) \ 'b \ 'a multiset \ 'b" +definition fold_mset :: "('a \ 'b \ 'b) \ 'b \ 'a multiset \ 'b" where - "fold f s M = Finite_Set.fold (\x. f x ^^ count M x) s (set_of M)" + "fold_mset f s M = Finite_Set.fold (\x. f x ^^ count M x) s (set_of M)" lemma fold_mset_empty [simp]: - "fold f s {#} = s" - by (simp add: fold_def) + "fold_mset f s {#} = s" + by (simp add: fold_mset_def) context comp_fun_commute begin lemma fold_mset_insert: - "fold f s (M + {#x#}) = f x (fold f s M)" + "fold_mset f s (M + {#x#}) = f x (fold_mset f s M)" proof - interpret mset: comp_fun_commute "\y. f y ^^ count M y" by (fact comp_fun_commute_funpow) @@ -824,7 +823,7 @@ Finite_Set.fold (\y. f y ^^ count M y) s (set_of M)" by (auto intro!: Finite_Set.fold_cong comp_fun_commute_funpow) with False * show ?thesis - by (simp add: fold_def del: count_union) + by (simp add: fold_mset_def del: count_union) next case True def N \ "set_of M - {x}" @@ -832,23 +831,23 @@ then have "Finite_Set.fold (\y. f y ^^ count (M + {#x#}) y) s N = Finite_Set.fold (\y. f y ^^ count M y) s N" by (auto intro!: Finite_Set.fold_cong comp_fun_commute_funpow) - with * show ?thesis by (simp add: fold_def del: count_union) simp + with * show ?thesis by (simp add: fold_mset_def del: count_union) simp qed qed corollary fold_mset_single [simp]: - "fold f s {#x#} = f x s" + "fold_mset f s {#x#} = f x s" proof - - have "fold f s ({#} + {#x#}) = f x s" by (simp only: fold_mset_insert) simp + have "fold_mset f s ({#} + {#x#}) = f x s" by (simp only: fold_mset_insert) simp then show ?thesis by simp qed lemma fold_mset_fun_left_comm: - "f x (fold f s M) = fold f (f x s) M" + "f x (fold_mset f s M) = fold_mset f (f x s) M" by (induct M) (simp_all add: fold_mset_insert fun_left_comm) lemma fold_mset_union [simp]: - "fold f s (M + N) = fold f (fold f s M) N" + "fold_mset f s (M + N) = fold_mset f (fold_mset f s M) N" proof (induct M) case empty then show ?case by simp next @@ -860,7 +859,7 @@ lemma fold_mset_fusion: assumes "comp_fun_commute g" - shows "(\x y. h (g x y) = f x (h y)) \ h (fold g w A) = fold f (h w) A" (is "PROP ?P") + shows "(\x y. h (g x y) = f x (h y)) \ h (fold_mset g w A) = fold_mset f (h w) A" (is "PROP ?P") proof - interpret comp_fun_commute g by (fact assms) show "PROP ?P" by (induct A) auto @@ -870,10 +869,10 @@ text {* A note on code generation: When defining some function containing a - subterm @{term "fold F"}, code generation is not automatic. When + subterm @{term "fold_mset F"}, code generation is not automatic. When interpreting locale @{text left_commutative} with @{text F}, the - would be code thms for @{const fold} become thms like - @{term "fold F z {#} = z"} where @{text F} is not a pattern but + would be code thms for @{const fold_mset} become thms like + @{term "fold_mset F z {#} = z"} where @{text F} is not a pattern but contains defined symbols, i.e.\ is not a code thm. Hence a separate constant with its own code thms needs to be introduced for @{text F}. See the image operator below. @@ -883,7 +882,7 @@ subsection {* Image *} definition image_mset :: "('a \ 'b) \ 'a multiset \ 'b multiset" where - "image_mset f = fold (plus o single o f) {#}" + "image_mset f = fold_mset (plus o single o f) {#}" lemma comp_fun_commute_mset_image: "comp_fun_commute (plus o single o f)" @@ -1164,7 +1163,7 @@ definition sorted_list_of_multiset :: "'a multiset \ 'a list" where - "sorted_list_of_multiset M = fold insort [] M" + "sorted_list_of_multiset M = fold_mset insort [] M" lemma sorted_list_of_multiset_empty [simp]: "sorted_list_of_multiset {#} = []" @@ -1223,7 +1222,7 @@ definition F :: "'a multiset \ 'a" where - eq_fold: "F M = Multiset.fold f 1 M" + eq_fold: "F M = fold_mset f 1 M" lemma empty [simp]: "F {#} = 1" @@ -1252,7 +1251,7 @@ declare comp_fun_commute.fold_mset_insert[OF comp_fun_commute_plus_mset, simp] -lemma in_mset_fold_plus_iff[iff]: "x \# Multiset.fold (op +) M NN \ x \# M \ (\N. N \# NN \ x \# N)" +lemma in_mset_fold_plus_iff[iff]: "x \# fold_mset (op +) M NN \ x \# M \ (\N. N \# NN \ x \# N)" by (induct NN) auto notation times (infixl "*" 70) @@ -1353,7 +1352,7 @@ lemma msetprod_multiplicity: "msetprod M = setprod (\x. x ^ count M x) (set_of M)" - by (simp add: Multiset.fold_def setprod.eq_fold msetprod.eq_fold funpow_times_power comp_def) + by (simp add: fold_mset_def setprod.eq_fold msetprod.eq_fold funpow_times_power comp_def) end @@ -2101,8 +2100,6 @@ multiset_postproc *} -hide_const (open) fold - subsection {* Naive implementation using lists *} @@ -2125,7 +2122,7 @@ by (simp add: multiset_of_map) lemma [code]: - "Multiset.filter f (multiset_of xs) = multiset_of (filter f xs)" + "filter_mset f (multiset_of xs) = multiset_of (filter f xs)" by (simp add: multiset_of_filter) lemma [code]: