src/HOL/Relation.thy
 changeset 45012 060f76635bfe parent 44921 58eef4843641 child 45137 6e422d180de8
```     1.1 --- a/src/HOL/Relation.thy	Tue Sep 20 15:23:17 2011 +0200
1.2 +++ b/src/HOL/Relation.thy	Tue Sep 20 21:47:52 2011 +0200
1.3 @@ -275,6 +275,10 @@
1.4
1.5  subsection {* Transitivity *}
1.6
1.7 +lemma trans_join:
1.8 +  "trans r \<longleftrightarrow> (\<forall>(x, y1) \<in> r. \<forall>(y2, z) \<in> r. y1 = y2 \<longrightarrow> (x, z) \<in> r)"
1.9 +  by (auto simp add: trans_def)
1.10 +
1.11  lemma transI:
1.12    "(!!x y z. (x, y) : r ==> (y, z) : r ==> (x, z) : r) ==> trans r"
1.13  by (unfold trans_def) iprover
1.14 @@ -296,6 +300,10 @@
1.15
1.16  subsection {* Irreflexivity *}
1.17
1.18 +lemma irrefl_distinct:
1.19 +  "irrefl r \<longleftrightarrow> (\<forall>(x, y) \<in> r. x \<noteq> y)"
1.20 +  by (auto simp add: irrefl_def)
1.21 +
1.22  lemma irrefl_diff_Id[simp]: "irrefl(r-Id)"
1.24
1.25 @@ -386,6 +394,10 @@
1.26    "a : Domain r ==> (!!y. (a, y) : r ==> P) ==> P"
1.27  by (iprover dest!: iffD1 [OF Domain_iff])
1.28
1.29 +lemma Domain_fst:
1.30 +  "Domain r = fst ` r"
1.31 +  by (auto simp add: image_def Bex_def)
1.32 +
1.33  lemma Domain_empty [simp]: "Domain {} = {}"
1.34  by blast
1.35
1.36 @@ -440,6 +452,10 @@
1.37  lemma RangeE [elim!]: "b : Range r ==> (!!x. (x, b) : r ==> P) ==> P"
1.38  by (unfold Range_def) (iprover elim!: DomainE dest!: converseD)
1.39
1.40 +lemma Range_snd:
1.41 +  "Range r = snd ` r"
1.42 +  by (auto simp add: image_def Bex_def)
1.43 +
1.44  lemma Range_empty [simp]: "Range {} = {}"
1.45  by blast
1.46
```