1.1 --- a/src/HOL/Relation.thy	Mon Oct 05 11:48:06 2009 +0200
     1.2 +++ b/src/HOL/Relation.thy	Mon Oct 05 16:41:06 2009 +0100
     1.3 @@ -376,6 +376,9 @@
     1.4  lemma Domain_empty [simp]: "Domain {} = {}"
     1.5  by blast
     1.6  
     1.7 +lemma Domain_empty_iff: "Domain r = {} \<longleftrightarrow> r = {}"
     1.8 +  by auto
     1.9 +
    1.10  lemma Domain_insert: "Domain (insert (a, b) r) = insert a (Domain r)"
    1.11  by blast
    1.12  
    1.13 @@ -427,6 +430,9 @@
    1.14  lemma Range_empty [simp]: "Range {} = {}"
    1.15  by blast
    1.16  
    1.17 +lemma Range_empty_iff: "Range r = {} \<longleftrightarrow> r = {}"
    1.18 +  by auto
    1.19 +
    1.20  lemma Range_insert: "Range (insert (a, b) r) = insert b (Range r)"
    1.21  by blast
    1.22  
    1.23 @@ -617,8 +623,11 @@
    1.24    apply simp
    1.25    done
    1.26  
    1.27 -text {* \paragraph{Finiteness of transitive closure} (Thanks to Sidi
    1.28 -Ehmety) *}
    1.29 +lemma finite_Domain: "finite r ==> finite (Domain r)"
    1.30 +  by (induct set: finite) (auto simp add: Domain_insert)
    1.31 +
    1.32 +lemma finite_Range: "finite r ==> finite (Range r)"
    1.33 +  by (induct set: finite) (auto simp add: Range_insert)
    1.34  
    1.35  lemma finite_Field: "finite r ==> finite (Field r)"
    1.36    -- {* A finite relation has a finite field (@{text "= domain \<union> range"}. *}