author | haftmann |

Mon Dec 26 22:17:10 2011 +0100 (2011-12-26) | |

changeset 45989 | b39256df5f8a |

parent 45988 | 40e60897ee07 |

child 45990 | b7b905b23b2a |

moved theorem requiring multisets from More_List to Multiset

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