--- a/src/HOL/Relation.thy Tue Sep 20 15:23:17 2011 +0200
+++ b/src/HOL/Relation.thy Tue Sep 20 21:47:52 2011 +0200
@@ -275,6 +275,10 @@
subsection {* Transitivity *}
+lemma trans_join:
+ "trans r \<longleftrightarrow> (\<forall>(x, y1) \<in> r. \<forall>(y2, z) \<in> r. y1 = y2 \<longrightarrow> (x, z) \<in> r)"
+ by (auto simp add: trans_def)
+
lemma transI:
"(!!x y z. (x, y) : r ==> (y, z) : r ==> (x, z) : r) ==> trans r"
by (unfold trans_def) iprover
@@ -296,6 +300,10 @@
subsection {* Irreflexivity *}
+lemma irrefl_distinct:
+ "irrefl r \<longleftrightarrow> (\<forall>(x, y) \<in> r. x \<noteq> y)"
+ by (auto simp add: irrefl_def)
+
lemma irrefl_diff_Id[simp]: "irrefl(r-Id)"
by(simp add:irrefl_def)
@@ -386,6 +394,10 @@
"a : Domain r ==> (!!y. (a, y) : r ==> P) ==> P"
by (iprover dest!: iffD1 [OF Domain_iff])
+lemma Domain_fst:
+ "Domain r = fst ` r"
+ by (auto simp add: image_def Bex_def)
+
lemma Domain_empty [simp]: "Domain {} = {}"
by blast
@@ -440,6 +452,10 @@
lemma RangeE [elim!]: "b : Range r ==> (!!x. (x, b) : r ==> P) ==> P"
by (unfold Range_def) (iprover elim!: DomainE dest!: converseD)
+lemma Range_snd:
+ "Range r = snd ` r"
+ by (auto simp add: image_def Bex_def)
+
lemma Range_empty [simp]: "Range {} = {}"
by blast