# HG changeset patch # User haftmann # Date 1324934230 -3600 # Node ID b39256df5f8a57c81cbdb28d7eabf2122b8a9577 # Parent 40e60897ee07f35a79a5230632ef66abb7b5cf40 moved theorem requiring multisets from More_List to Multiset diff -r 40e60897ee07 -r b39256df5f8a src/HOL/Library/Multiset.thy --- a/src/HOL/Library/Multiset.thy Mon Dec 26 22:17:10 2011 +0100 +++ b/src/HOL/Library/Multiset.thy Mon Dec 26 22:17:10 2011 +0100 @@ -857,6 +857,23 @@ qed qed +lemma fold_multiset_equiv: + assumes f: "\x y. x \ set xs \ y \ set xs \ f x \ f y = f y \ f x" + and equiv: "multiset_of xs = multiset_of ys" + shows "fold f xs = fold f ys" +using f equiv [symmetric] proof (induct xs arbitrary: ys) + case Nil then show ?case by simp +next + case (Cons x xs) + then have *: "set ys = set (x # xs)" by (blast dest: multiset_of_eq_setD) + have "\x y. x \ set ys \ y \ set ys \ f x \ f y = f y \ f x" + by (rule Cons.prems(1)) (simp_all add: *) + moreover from * have "x \ set ys" by simp + ultimately have "fold f ys = fold f (remove1 x ys) \ f x" by (fact fold_remove1_split) + moreover from Cons.prems have "fold f xs = fold f (remove1 x ys)" by (auto intro: Cons.hyps) + ultimately show ?case by simp +qed + context linorder begin