src/HOL/Library/Multiset.thy
changeset 45989 b39256df5f8a
parent 45866 e62b319c7696
child 46168 bef8c811df20
equal deleted inserted replaced
45988:40e60897ee07 45989:b39256df5f8a
   853     from * have "length (filter (\<lambda>x. z = x) xs) = length (filter (\<lambda>y. z = y) (remove1 x ys))" by (rule Cons.hyps)
   853     from * have "length (filter (\<lambda>x. z = x) xs) = length (filter (\<lambda>y. z = y) (remove1 x ys))" by (rule Cons.hyps)
   854     moreover from `x \<in> set ys` have "length (filter (\<lambda>y. x = y) ys) > 0" by (simp add: filter_empty_conv)
   854     moreover from `x \<in> set ys` have "length (filter (\<lambda>y. x = y) ys) > 0" by (simp add: filter_empty_conv)
   855     ultimately show ?case using `x \<in> set ys`
   855     ultimately show ?case using `x \<in> set ys`
   856       by (simp add: filter_remove1) (auto simp add: length_remove1)
   856       by (simp add: filter_remove1) (auto simp add: length_remove1)
   857   qed
   857   qed
       
   858 qed
       
   859 
       
   860 lemma fold_multiset_equiv:
       
   861   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"
       
   862     and equiv: "multiset_of xs = multiset_of ys"
       
   863   shows "fold f xs = fold f ys"
       
   864 using f equiv [symmetric] proof (induct xs arbitrary: ys)
       
   865   case Nil then show ?case by simp
       
   866 next
       
   867   case (Cons x xs)
       
   868   then have *: "set ys = set (x # xs)" by (blast dest: multiset_of_eq_setD)
       
   869   have "\<And>x y. x \<in> set ys \<Longrightarrow> y \<in> set ys \<Longrightarrow> f x \<circ> f y = f y \<circ> f x" 
       
   870     by (rule Cons.prems(1)) (simp_all add: *)
       
   871   moreover from * have "x \<in> set ys" by simp
       
   872   ultimately have "fold f ys = fold f (remove1 x ys) \<circ> f x" by (fact fold_remove1_split)
       
   873   moreover from Cons.prems have "fold f xs = fold f (remove1 x ys)" by (auto intro: Cons.hyps)
       
   874   ultimately show ?case by simp
   858 qed
   875 qed
   859 
   876 
   860 context linorder
   877 context linorder
   861 begin
   878 begin
   862 
   879