# HG changeset patch
# User traytel
# Date 1374747907 -7200
# Node ID 6bf02eb4ddf7dac47d20c8633198dcf7ffa44a33
# Parent  412c9e0381a19643f5e18de8bcc971b18e87cb34
two useful relation theorems

diff -r 412c9e0381a1 -r 6bf02eb4ddf7 src/HOL/BNF/BNF_Def.thy
--- a/src/HOL/BNF/BNF_Def.thy	Thu Jul 25 08:57:16 2013 +0200
+++ b/src/HOL/BNF/BNF_Def.thy	Thu Jul 25 12:25:07 2013 +0200
@@ -17,10 +17,6 @@
 lemma collect_o: "collect F o g = collect ((\<lambda>f. f o g) ` F)"
 by (rule ext) (auto simp only: o_apply collect_def)
 
-lemma conversep_mono:
-"R1 ^--1 \<le> R2 ^--1 \<longleftrightarrow> R1 \<le> R2"
-unfolding conversep.simps by auto
-
 lemma converse_shift:
 "R1 \<subseteq> R2 ^-1 \<Longrightarrow> R1 ^-1 \<subseteq> R2"
 unfolding converse_def by auto
diff -r 412c9e0381a1 -r 6bf02eb4ddf7 src/HOL/Relation.thy
--- a/src/HOL/Relation.thy	Thu Jul 25 08:57:16 2013 +0200
+++ b/src/HOL/Relation.thy	Thu Jul 25 12:25:07 2013 +0200
@@ -131,7 +131,6 @@
 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)"
   by (simp add: fun_eq_iff)
 
-
 subsection {* Properties of relations *}
 
 subsubsection {* Reflexivity *}
@@ -706,6 +705,12 @@
 lemma converse_UNION: "(UNION S r)^-1 = (UN x:S. (r x)^-1)"
   by blast
 
+lemma converse_mono: "r^-1 \<subseteq> s ^-1 \<longleftrightarrow> r \<subseteq> s"
+  by auto
+
+lemma conversep_mono: "r^--1 \<le> s ^--1 \<longleftrightarrow> r \<le> s"
+  by (fact converse_mono[to_pred])
+
 lemma converse_Id [simp]: "Id^-1 = Id"
   by blast