src/HOL/Library/Set_Algebras.thy
changeset 47446 ed0795caec95
parent 47445 69e96e5500df
child 53596 d29d63460d84
     1.1 --- a/src/HOL/Library/Set_Algebras.thy	Thu Apr 12 23:07:01 2012 +0200
     1.2 +++ b/src/HOL/Library/Set_Algebras.thy	Thu Apr 12 23:15:34 2012 +0200
     1.3 @@ -368,4 +368,14 @@
     1.4    shows "f (setsum S I) = setsum (f \<circ> S) I"
     1.5    using setsum_set_cond_linear[of "\<lambda>x. True" f I S] assms by auto
     1.6  
     1.7 +lemma set_times_Un_distrib:
     1.8 +  "A * (B \<union> C) = A * B \<union> A * C"
     1.9 +  "(A \<union> B) * C = A * C \<union> B * C"
    1.10 +by (auto simp: set_times_def)
    1.11 +
    1.12 +lemma set_times_UNION_distrib:
    1.13 +  "A * UNION I M = UNION I (%i. A * M i)"
    1.14 +  "UNION I M * A = UNION I (%i. M i * A)"
    1.15 +by (auto simp: set_times_def)
    1.16 +
    1.17  end