src/HOL/Relation.thy
 changeset 32876 c34b072518c9 parent 32850 d95a7fd00bd4 child 33218 ecb5cd453ef2
```     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"}. *}
```