# 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 \ B = {}" + shows "Finite_Set.fold f z (A \ 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}: *}