# HG changeset patch # User Lars Hupel # Date 1499697522 -7200 # Node ID fb6efe575c6dbe47dbf677bb6472af61922b6a0f # Parent 3bc892346a6b1fbd4a4962957fb7f5914309ae7c lift sum to finite sets diff -r 3bc892346a6b -r fb6efe575c6d src/HOL/Library/FSet.thy --- a/src/HOL/Library/FSet.thy Sat Jul 08 17:33:11 2017 +0200 +++ b/src/HOL/Library/FSet.thy Mon Jul 10 16:38:42 2017 +0200 @@ -202,9 +202,10 @@ lift_definition ffold :: "('a \ 'b \ 'b) \ 'b \ 'a fset \ 'b" is Finite_Set.fold . +lift_definition fsum :: "('a \ 'b::comm_monoid_add) \ 'a fset \ 'b" is sum . + lift_definition fset_of_list :: "'a list \ 'a fset" is set by (rule finite_set) - subsection \Transferred lemmas from Set.thy\ lemmas fset_eqI = set_eqI[Transfer.transferred] @@ -713,6 +714,13 @@ end +lemmas fsum_cong[fundef_cong] = sum.cong[Transfer.transferred] + +lemma fsum_strong_cong[cong]: + assumes "A = B" "\x. x |\| B =simp=> g x = h x" + shows "fsum (\x. g x) A = fsum (\x. h x) B" +using assms unfolding simp_implies_def by (auto cong: fsum_cong) + subsection \Choice in fsets\ @@ -1174,4 +1182,4 @@ no_notation scomp (infixl "\\" 60) -end +end \ No newline at end of file