--- 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 \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'b \<Rightarrow> 'a fset \<Rightarrow> 'b" is Finite_Set.fold .
+lift_definition fsum :: "('a \<Rightarrow> 'b::comm_monoid_add) \<Rightarrow> 'a fset \<Rightarrow> 'b" is sum .
+
lift_definition fset_of_list :: "'a list \<Rightarrow> 'a fset" is set by (rule finite_set)
-
subsection \<open>Transferred lemmas from Set.thy\<close>
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" "\<And>x. x |\<in>| B =simp=> g x = h x"
+ shows "fsum (\<lambda>x. g x) A = fsum (\<lambda>x. h x) B"
+using assms unfolding simp_implies_def by (auto cong: fsum_cong)
+
subsection \<open>Choice in fsets\<close>
@@ -1174,4 +1182,4 @@
no_notation scomp (infixl "\<circ>\<rightarrow>" 60)
-end
+end
\ No newline at end of file