src/HOL/Relation.thy
changeset 58195 1fee63e0377d
parent 57111 de33f3965ca6
child 58889 5b7a9633cfa8
     1.1 --- a/src/HOL/Relation.thy	Fri Sep 05 16:09:03 2014 +0100
     1.2 +++ b/src/HOL/Relation.thy	Sat Sep 06 20:12:32 2014 +0200
     1.3 @@ -604,7 +604,6 @@
     1.4    "(R O S) O T = R O (S O T)"
     1.5    by blast
     1.6  
     1.7 -
     1.8  lemma relcompp_assoc:
     1.9    "(r OO s) OO t = r OO (s OO t)"
    1.10    by (fact O_assoc [to_pred])
    1.11 @@ -665,6 +664,9 @@
    1.12    "r O s = {(x, z). \<exists>y. (x, y) \<in> r \<and> (y, z) \<in> s}"
    1.13    by (auto simp add: set_eq_iff)
    1.14  
    1.15 +lemma relcompp_apply: "(R OO S) a c \<longleftrightarrow> (\<exists>b. R a b \<and> S b c)"
    1.16 +  unfolding relcomp_unfold [to_pred] ..
    1.17 +
    1.18  lemma eq_OO: "op= OO R = R"
    1.19  by blast
    1.20