1.1 --- a/src/HOL/Relation.thy	Thu Jul 25 08:57:16 2013 +0200
     1.2 +++ b/src/HOL/Relation.thy	Thu Jul 25 12:25:07 2013 +0200
     1.3 @@ -131,7 +131,6 @@
     1.4  lemma SUP_Sup_eq2 [pred_set_conv]: "(\<Squnion>i\<in>S. (\<lambda>x y. (x, y) \<in> i)) = (\<lambda>x y. (x, y) \<in> \<Union>S)"
     1.5    by (simp add: fun_eq_iff)
     1.6  
     1.7 -
     1.8  subsection {* Properties of relations *}
     1.9  
    1.10  subsubsection {* Reflexivity *}
    1.11 @@ -706,6 +705,12 @@
    1.12  lemma converse_UNION: "(UNION S r)^-1 = (UN x:S. (r x)^-1)"
    1.13    by blast
    1.14  
    1.15 +lemma converse_mono: "r^-1 \<subseteq> s ^-1 \<longleftrightarrow> r \<subseteq> s"
    1.16 +  by auto
    1.17 +
    1.18 +lemma conversep_mono: "r^--1 \<le> s ^--1 \<longleftrightarrow> r \<le> s"
    1.19 +  by (fact converse_mono[to_pred])
    1.20 +
    1.21  lemma converse_Id [simp]: "Id^-1 = Id"
    1.22    by blast
    1.23