# HG changeset patch
# User paulson
# Date 1254757266 -3600
# Node ID c34b072518c905def5079389843d09ee06774c97
# Parent  36fa392ba61af0728cd4e24fd1e087da942ca26f
New facts about domain and range in

diff -r 36fa392ba61a -r c34b072518c9 src/HOL/Relation.thy
--- a/src/HOL/Relation.thy	Mon Oct 05 11:48:06 2009 +0200
+++ b/src/HOL/Relation.thy	Mon Oct 05 16:41:06 2009 +0100
@@ -376,6 +376,9 @@
 lemma Domain_empty [simp]: "Domain {} = {}"
 by blast
 
+lemma Domain_empty_iff: "Domain r = {} \<longleftrightarrow> r = {}"
+  by auto
+
 lemma Domain_insert: "Domain (insert (a, b) r) = insert a (Domain r)"
 by blast
 
@@ -427,6 +430,9 @@
 lemma Range_empty [simp]: "Range {} = {}"
 by blast
 
+lemma Range_empty_iff: "Range r = {} \<longleftrightarrow> r = {}"
+  by auto
+
 lemma Range_insert: "Range (insert (a, b) r) = insert b (Range r)"
 by blast
 
@@ -617,8 +623,11 @@
   apply simp
   done
 
-text {* \paragraph{Finiteness of transitive closure} (Thanks to Sidi
-Ehmety) *}
+lemma finite_Domain: "finite r ==> finite (Domain r)"
+  by (induct set: finite) (auto simp add: Domain_insert)
+
+lemma finite_Range: "finite r ==> finite (Range r)"
+  by (induct set: finite) (auto simp add: Range_insert)
 
 lemma finite_Field: "finite r ==> finite (Field r)"
   -- {* A finite relation has a finite field (@{text "= domain \<union> range"}. *}