added lemmas rel_comp_UNION_distrib(2)
authorkrauss
Sun May 09 12:00:43 2010 +0200 (2010-05-09)
changeset 36772ef97c5006840
parent 36771 3e08b6789e66
child 36773 acb789f3936b
added lemmas rel_comp_UNION_distrib(2)
src/HOL/Relation.thy
     1.1 --- a/src/HOL/Relation.thy	Sat May 08 22:29:44 2010 +0200
     1.2 +++ b/src/HOL/Relation.thy	Sun May 09 12:00:43 2010 +0200
     1.3 @@ -181,6 +181,12 @@
     1.4  lemma rel_comp_distrib2[simp]: "(S \<union> T) O R = (S O R) \<union> (T O R)"
     1.5  by auto
     1.6  
     1.7 +lemma rel_comp_UNION_distrib: "s O UNION I r = UNION I (%i. s O r i)"
     1.8 +by auto
     1.9 +
    1.10 +lemma rel_comp_UNION_distrib2: "UNION I r O s = UNION I (%i. r i O s)"
    1.11 +by auto
    1.12 +
    1.13  
    1.14  subsection {* Reflexivity *}
    1.15