Field of a relation, and some Domain/Range rules

--- a/src/HOL/Relation.ML	Fri Jan 05 10:18:46 2001 +0100
+++ b/src/HOL/Relation.ML	Fri Jan 05 10:19:14 2001 +0100
@@ -233,6 +233,15 @@
 AddIs  [DomainI];
 AddSEs [DomainE];
 
+Goal "Domain {} = {}";
+by (Blast_tac 1); 
+qed "Domain_empty";
+Addsimps [Domain_empty];
+
+Goal "Domain (insert (a, b) r) = insert a (Domain r)";
+by (Blast_tac 1); 
+qed "Domain_insert";
+
 Goal "Domain Id = UNIV";
 by (Blast_tac 1);
 qed "Domain_Id";
@@ -284,6 +293,15 @@
 AddIs  [RangeI];
 AddSEs [RangeE];
 
+Goal "Range {} = {}";
+by (Blast_tac 1); 
+qed "Range_empty";
+Addsimps [Range_empty];
+
+Goal "Range (insert (a, b) r) = insert b (Range r)";
+by (Blast_tac 1); 
+qed "Range_insert";
+
 Goal "Range Id = UNIV";
 by (Blast_tac 1);
 qed "Range_Id";
@@ -350,7 +368,6 @@
 by (Blast_tac 1);
 qed "rev_ImageI";
 
-
 Goal "R^^{} = {}";
 by (Blast_tac 1);
 qed "Image_empty";

--- a/src/HOL/Relation.thy	Fri Jan 05 10:18:46 2001 +0100
+++ b/src/HOL/Relation.thy	Fri Jan 05 10:19:14 2001 +0100
@@ -31,6 +31,9 @@
   Range  :: "('a*'b) set => 'b set"
     "Range(r) == Domain(r^-1)"
 
+  Field :: "('a*'a)set=>'a set"
+    "Field r == Domain r Un Range r"
+
   refl   :: "['a set, ('a*'a) set] => bool" (*reflexivity over a set*)
     "refl A r == r <= A <*> A & (ALL x: A. (x,x) : r)"