src/HOL/Relation.ML
changeset 4644 ecf8f17f6fe0
parent 4601 87fc0d44b837
child 4650 91af1ef45d68
     1.1 --- a/src/HOL/Relation.ML	Sun Feb 22 14:12:23 1998 +0100
     1.2 +++ b/src/HOL/Relation.ML	Mon Feb 23 11:15:40 1998 +0100
     1.3 @@ -112,6 +112,11 @@
     1.4  by (Blast_tac 1);
     1.5  qed "inverse_comp";
     1.6  
     1.7 +goal Relation.thy "id^-1 = id";
     1.8 +by (Blast_tac 1);
     1.9 +qed "inverse_id";
    1.10 +Addsimps [inverse_id];
    1.11 +
    1.12  (** Domain **)
    1.13  
    1.14  qed_goalw "Domain_iff" Relation.thy [Domain_def]
    1.15 @@ -130,6 +135,11 @@
    1.16  AddIs  [DomainI];
    1.17  AddSEs [DomainE];
    1.18  
    1.19 +goal thy "Domain id = UNIV";
    1.20 +by (Blast_tac 1);
    1.21 +qed "Domain_id";
    1.22 +Addsimps [Domain_id];
    1.23 +
    1.24  (** Range **)
    1.25  
    1.26  qed_goalw "RangeI" Relation.thy [Range_def] "!!a b r.(a,b): r ==> b : Range(r)"
    1.27 @@ -145,6 +155,11 @@
    1.28  AddIs  [RangeI];
    1.29  AddSEs [RangeE];
    1.30  
    1.31 +goal thy "Range id = UNIV";
    1.32 +by (Blast_tac 1);
    1.33 +qed "Range_id";
    1.34 +Addsimps [Range_id];
    1.35 +
    1.36  (*** Image of a set under a relation ***)
    1.37  
    1.38  qed_goalw "Image_iff" Relation.thy [Image_def]