# HG changeset patch
# User haftmann
# Date 1349532221 -7200
# Node ID a5842f026d4ce1e8741800f661f5d2c5db8775ea
# Parent  bbc2942ba09f59d6a19212fc83643e796e7bbe61
congruence rule for Finite_Set.fold

diff -r bbc2942ba09f -r a5842f026d4c src/HOL/Finite_Set.thy
--- a/src/HOL/Finite_Set.thy	Sat Oct 06 11:08:52 2012 +0200
+++ b/src/HOL/Finite_Set.thy	Sat Oct 06 16:03:41 2012 +0200
@@ -710,6 +710,25 @@
 
 end
 
+lemma fold_cong:
+  assumes "comp_fun_commute f" "comp_fun_commute g"
+  assumes "finite A" and cong: "\<And>x. x \<in> A \<Longrightarrow> f x = g x"
+    and "A = B" and "s = t"
+  shows "Finite_Set.fold f s A = Finite_Set.fold g t B"
+proof -
+  have "Finite_Set.fold f s A = Finite_Set.fold g s A"  
+  using `finite A` cong proof (induct A)
+    case empty then show ?case by simp
+  next
+    case (insert x A)
+    interpret f: comp_fun_commute f by (fact `comp_fun_commute f`)
+    interpret g: comp_fun_commute g by (fact `comp_fun_commute g`)
+    from insert show ?case by simp
+  qed
+  with assms show ?thesis by simp
+qed
+
+
 text{* A simplified version for idempotent functions: *}
 
 locale comp_fun_idem = comp_fun_commute +