src/HOL/Relation.thy
changeset 64584 142ac30b68fe
parent 63612 7195acc2fe93
child 64632 9df24b8b6c0a
     1.1 --- a/src/HOL/Relation.thy	Sat Dec 17 15:22:00 2016 +0100
     1.2 +++ b/src/HOL/Relation.thy	Sat Dec 17 15:22:00 2016 +0100
     1.3 @@ -389,8 +389,9 @@
     1.4  lemma trans_INTER: "\<forall>x\<in>S. trans (r x) \<Longrightarrow> trans (INTER S r)"
     1.5    by (fast intro: transI elim: transD)
     1.6  
     1.7 -(* FIXME thm trans_INTER [to_pred] *)
     1.8 -
     1.9 +lemma transp_INF: "\<forall>x\<in>S. transp (r x) \<Longrightarrow> transp (INFIMUM S r)"
    1.10 +  by (fact trans_INTER [to_pred])
    1.11 +    
    1.12  lemma trans_join [code]: "trans r \<longleftrightarrow> (\<forall>(x, y1) \<in> r. \<forall>(y2, z) \<in> r. y1 = y2 \<longrightarrow> (x, z) \<in> r)"
    1.13    by (auto simp add: trans_def)
    1.14  
    1.15 @@ -620,13 +621,15 @@
    1.16  lemma relcomp_UNION_distrib: "s O UNION I r = (\<Union>i\<in>I. s O r i) "
    1.17    by auto
    1.18  
    1.19 -(* FIXME thm relcomp_UNION_distrib [to_pred] *)
    1.20 -
    1.21 +lemma relcompp_SUP_distrib: "s OO SUPREMUM I r = (\<Squnion>i\<in>I. s OO r i)"
    1.22 +  by (fact relcomp_UNION_distrib [to_pred])
    1.23 +    
    1.24  lemma relcomp_UNION_distrib2: "UNION I r O s = (\<Union>i\<in>I. r i O s) "
    1.25    by auto
    1.26  
    1.27 -(* FIXME thm relcomp_UNION_distrib2 [to_pred] *)
    1.28 -
    1.29 +lemma relcompp_SUP_distrib2: "SUPREMUM I r OO s = (\<Squnion>i\<in>I. r i OO s)"
    1.30 +  by (fact relcomp_UNION_distrib2 [to_pred])
    1.31 +    
    1.32  lemma single_valued_relcomp: "single_valued r \<Longrightarrow> single_valued s \<Longrightarrow> single_valued (r O s)"
    1.33    unfolding single_valued_def by blast
    1.34