# HG changeset patch
# User krauss
# Date 1334265334 -7200
# Node ID ed0795caec95367293a86095552d3b855d907595
# Parent  69e96e5500df55b406fa8f424a41f8d262212a9b
distributivity of * over Un and UNION

diff -r 69e96e5500df -r ed0795caec95 src/HOL/Library/Set_Algebras.thy
--- a/src/HOL/Library/Set_Algebras.thy	Thu Apr 12 23:07:01 2012 +0200
+++ b/src/HOL/Library/Set_Algebras.thy	Thu Apr 12 23:15:34 2012 +0200
@@ -368,4 +368,14 @@
   shows "f (setsum S I) = setsum (f \<circ> S) I"
   using setsum_set_cond_linear[of "\<lambda>x. True" f I S] assms by auto
 
+lemma set_times_Un_distrib:
+  "A * (B \<union> C) = A * B \<union> A * C"
+  "(A \<union> B) * C = A * C \<union> B * C"
+by (auto simp: set_times_def)
+
+lemma set_times_UNION_distrib:
+  "A * UNION I M = UNION I (%i. A * M i)"
+  "UNION I M * A = UNION I (%i. M i * A)"
+by (auto simp: set_times_def)
+
 end