summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | haftmann |

Fri, 03 Dec 2010 22:39:34 +0100 | |

changeset 40951 | 6c35a88d8f61 |

parent 40950 | a370b0fb6f09 |

child 40955 | 2dbce761696a |

tuned proposition

--- a/src/HOL/Library/More_List.thy Fri Dec 03 22:34:20 2010 +0100 +++ b/src/HOL/Library/More_List.thy Fri Dec 03 22:39:34 2010 +0100 @@ -85,16 +85,17 @@ using assms by (induct xs) (auto simp add: o_assoc [symmetric]) lemma fold_multiset_equiv: - assumes f: "\<And>x y. x \<in># multiset_of xs \<Longrightarrow> y \<in># multiset_of xs \<Longrightarrow> f x \<circ> f y = f y \<circ> f x" + 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" 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 "\<And>x y. x \<in> set ys \<Longrightarrow> y \<in> set ys \<Longrightarrow> f x \<circ> f y = f y \<circ> f x" - by (rule Cons.prems(1)) (simp_all add: mem_set_multiset_eq Cons.prems(2)) - moreover from Cons.prems have "x \<in> set ys" by (simp add: mem_set_multiset_eq) + by (rule Cons.prems(1)) (simp_all add: *) + moreover from * have "x \<in> set ys" by simp ultimately have "fold f ys = fold f (remove1 x ys) \<circ> 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