# HG changeset patch
# User krauss
# Date 1219769992 -7200
# Node ID f945f8d9ad4da21252a0eed30e902459b61e6811
# Parent  2d0c9329129366bf75056e5626efc97ef7d22fbd
added distributivity of relation composition over union [simp]

diff -r 2d0c93291293 -r f945f8d9ad4d src/HOL/Relation.thy
--- a/src/HOL/Relation.thy	Tue Aug 26 16:36:30 2008 +0200
+++ b/src/HOL/Relation.thy	Tue Aug 26 18:59:52 2008 +0200
@@ -166,6 +166,12 @@
     "s \<subseteq> A \<times> B ==> r \<subseteq> B \<times> C ==> (r O s) \<subseteq> A \<times> C"
 by blast
 
+lemma rel_comp_distrib[simp]: "R O (S \<union> T) = (R O S) \<union> (R O T)" 
+by auto
+
+lemma rel_comp_distrib2[simp]: "(S \<union> T) O R = (S O R) \<union> (T O R)"
+by auto
+
 
 subsection {* Reflexivity *}