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.23  by(simp add:irrefl_def)
    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