# HG changeset patch
# User Lars Hupel <lars.hupel@mytum.de>
# 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 \<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