moved theorem requiring multisets from More_List to Multiset
authorhaftmann
Mon Dec 26 22:17:10 2011 +0100 (2011-12-26)
changeset 45989b39256df5f8a
parent 45988 40e60897ee07
child 45990 b7b905b23b2a
moved theorem requiring multisets from More_List to Multiset
src/HOL/Library/Multiset.thy
     1.1 --- a/src/HOL/Library/Multiset.thy	Mon Dec 26 22:17:10 2011 +0100
     1.2 +++ b/src/HOL/Library/Multiset.thy	Mon Dec 26 22:17:10 2011 +0100
     1.3 @@ -857,6 +857,23 @@
     1.4    qed
     1.5  qed
     1.6  
     1.7 +lemma fold_multiset_equiv:
     1.8 +  assumes f: "\<And>x y. x \<in> set xs \<Longrightarrow> y \<in> set xs \<Longrightarrow> f x \<circ> f y = f y \<circ> f x"
     1.9 +    and equiv: "multiset_of xs = multiset_of ys"
    1.10 +  shows "fold f xs = fold f ys"
    1.11 +using f equiv [symmetric] proof (induct xs arbitrary: ys)
    1.12 +  case Nil then show ?case by simp
    1.13 +next
    1.14 +  case (Cons x xs)
    1.15 +  then have *: "set ys = set (x # xs)" by (blast dest: multiset_of_eq_setD)
    1.16 +  have "\<And>x y. x \<in> set ys \<Longrightarrow> y \<in> set ys \<Longrightarrow> f x \<circ> f y = f y \<circ> f x" 
    1.17 +    by (rule Cons.prems(1)) (simp_all add: *)
    1.18 +  moreover from * have "x \<in> set ys" by simp
    1.19 +  ultimately have "fold f ys = fold f (remove1 x ys) \<circ> f x" by (fact fold_remove1_split)
    1.20 +  moreover from Cons.prems have "fold f xs = fold f (remove1 x ys)" by (auto intro: Cons.hyps)
    1.21 +  ultimately show ?case by simp
    1.22 +qed
    1.23 +
    1.24  context linorder
    1.25  begin
    1.26