Field of a relation, and some Domain/Range rules
authorpaulson
Fri Jan 05 10:19:14 2001 +0100 (2001-01-05)
changeset 1078604ee73606993
parent 10785 53547a02f2a1
child 10787 f42353afd6d3
Field of a relation, and some Domain/Range rules
src/HOL/Relation.ML
src/HOL/Relation.thy
     1.1 --- a/src/HOL/Relation.ML	Fri Jan 05 10:18:46 2001 +0100
     1.2 +++ b/src/HOL/Relation.ML	Fri Jan 05 10:19:14 2001 +0100
     1.3 @@ -233,6 +233,15 @@
     1.4  AddIs  [DomainI];
     1.5  AddSEs [DomainE];
     1.6  
     1.7 +Goal "Domain {} = {}";
     1.8 +by (Blast_tac 1); 
     1.9 +qed "Domain_empty";
    1.10 +Addsimps [Domain_empty];
    1.11 +
    1.12 +Goal "Domain (insert (a, b) r) = insert a (Domain r)";
    1.13 +by (Blast_tac 1); 
    1.14 +qed "Domain_insert";
    1.15 +
    1.16  Goal "Domain Id = UNIV";
    1.17  by (Blast_tac 1);
    1.18  qed "Domain_Id";
    1.19 @@ -284,6 +293,15 @@
    1.20  AddIs  [RangeI];
    1.21  AddSEs [RangeE];
    1.22  
    1.23 +Goal "Range {} = {}";
    1.24 +by (Blast_tac 1); 
    1.25 +qed "Range_empty";
    1.26 +Addsimps [Range_empty];
    1.27 +
    1.28 +Goal "Range (insert (a, b) r) = insert b (Range r)";
    1.29 +by (Blast_tac 1); 
    1.30 +qed "Range_insert";
    1.31 +
    1.32  Goal "Range Id = UNIV";
    1.33  by (Blast_tac 1);
    1.34  qed "Range_Id";
    1.35 @@ -350,7 +368,6 @@
    1.36  by (Blast_tac 1);
    1.37  qed "rev_ImageI";
    1.38  
    1.39 -
    1.40  Goal "R^^{} = {}";
    1.41  by (Blast_tac 1);
    1.42  qed "Image_empty";
     2.1 --- a/src/HOL/Relation.thy	Fri Jan 05 10:18:46 2001 +0100
     2.2 +++ b/src/HOL/Relation.thy	Fri Jan 05 10:19:14 2001 +0100
     2.3 @@ -31,6 +31,9 @@
     2.4    Range  :: "('a*'b) set => 'b set"
     2.5      "Range(r) == Domain(r^-1)"
     2.6  
     2.7 +  Field :: "('a*'a)set=>'a set"
     2.8 +    "Field r == Domain r Un Range r"
     2.9 +
    2.10    refl   :: "['a set, ('a*'a) set] => bool" (*reflexivity over a set*)
    2.11      "refl A r == r <= A <*> A & (ALL x: A. (x,x) : r)"
    2.12