author traytel Thu Jul 25 12:25:07 2013 +0200 (2013-07-25) changeset 52730 6bf02eb4ddf7 parent 52729 412c9e0381a1 child 52731 dacd47a0633f
two useful relation theorems
 src/HOL/BNF/BNF_Def.thy file | annotate | diff | revisions src/HOL/Relation.thy file | annotate | diff | revisions
```     1.1 --- a/src/HOL/BNF/BNF_Def.thy	Thu Jul 25 08:57:16 2013 +0200
1.2 +++ b/src/HOL/BNF/BNF_Def.thy	Thu Jul 25 12:25:07 2013 +0200
1.3 @@ -17,10 +17,6 @@
1.4  lemma collect_o: "collect F o g = collect ((\<lambda>f. f o g) ` F)"
1.5  by (rule ext) (auto simp only: o_apply collect_def)
1.6
1.7 -lemma conversep_mono:
1.8 -"R1 ^--1 \<le> R2 ^--1 \<longleftrightarrow> R1 \<le> R2"
1.9 -unfolding conversep.simps by auto
1.10 -
1.11  lemma converse_shift:
1.12  "R1 \<subseteq> R2 ^-1 \<Longrightarrow> R1 ^-1 \<subseteq> R2"
1.13  unfolding converse_def by auto
```
```     2.1 --- a/src/HOL/Relation.thy	Thu Jul 25 08:57:16 2013 +0200
2.2 +++ b/src/HOL/Relation.thy	Thu Jul 25 12:25:07 2013 +0200
2.3 @@ -131,7 +131,6 @@
2.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)"
2.6
2.7 -
2.8  subsection {* Properties of relations *}
2.9
2.10  subsubsection {* Reflexivity *}
2.11 @@ -706,6 +705,12 @@
2.12  lemma converse_UNION: "(UNION S r)^-1 = (UN x:S. (r x)^-1)"
2.13    by blast
2.14
2.15 +lemma converse_mono: "r^-1 \<subseteq> s ^-1 \<longleftrightarrow> r \<subseteq> s"
2.16 +  by auto
2.17 +
2.18 +lemma conversep_mono: "r^--1 \<le> s ^--1 \<longleftrightarrow> r \<le> s"
2.19 +  by (fact converse_mono[to_pred])
2.20 +
2.21  lemma converse_Id [simp]: "Id^-1 = Id"
2.22    by blast
2.23
```