# HG changeset patch
# User Andreas Lochbihler
# Date 1405957871 -7200
# Node ID 56ed992b6d65b1f7d9f2296b9cdcfa47ae1058a2
# Parent  155b7e3b729e70b918df11d411b8e5cd49f1156d
add lemma

diff -r 155b7e3b729e -r 56ed992b6d65 src/HOL/Finite_Set.thy
--- a/src/HOL/Finite_Set.thy	Sun Jul 20 22:05:35 2014 +0200
+++ b/src/HOL/Finite_Set.thy	Mon Jul 21 17:51:11 2014 +0200
@@ -733,6 +733,11 @@
   then show ?thesis by simp
 qed
 
+lemma fold_set_union_disj:
+  assumes "finite A" "finite B" "A \<inter> B = {}"
+  shows "Finite_Set.fold f z (A \<union> B) = Finite_Set.fold f (Finite_Set.fold f z A) B"
+using assms(2,1,3) by induction simp_all
+
 end
 
 text{* Other properties of @{const fold}: *}