new Domain/Range rules
authorpaulson
Mon Nov 09 11:00:44 1998 +0100 (1998-11-09)
changeset 58110867068942e6
parent 5810 829cae93f132
child 5812 cbc106ddcc83
new Domain/Range rules
src/HOL/Relation.ML
     1.1 --- a/src/HOL/Relation.ML	Mon Nov 09 10:59:47 1998 +0100
     1.2 +++ b/src/HOL/Relation.ML	Mon Nov 09 11:00:44 1998 +0100
     1.3 @@ -131,9 +131,9 @@
     1.4  
     1.5  (** Domain **)
     1.6  
     1.7 -qed_goalw "Domain_iff" thy [Domain_def]
     1.8 -    "a: Domain(r) = (EX y. (a,y): r)"
     1.9 - (fn _=> [ (Blast_tac 1) ]);
    1.10 +Goalw [Domain_def] "a: Domain(r) = (EX y. (a,y): r)";
    1.11 +by (Blast_tac 1);
    1.12 +qed "Domain_iff";
    1.13  
    1.14  qed_goal "DomainI" thy "!!a b r. (a,b): r ==> a: Domain(r)"
    1.15   (fn _ => [ (etac (exI RS (Domain_iff RS iffD2)) 1) ]);
    1.16 @@ -152,8 +152,25 @@
    1.17  qed "Domain_Id";
    1.18  Addsimps [Domain_Id];
    1.19  
    1.20 +Goal "Domain(A Un B) = Domain(A) Un Domain(B)";
    1.21 +by (Blast_tac 1);
    1.22 +qed "Domain_Un_eq";
    1.23 +
    1.24 +Goal "Domain(A Int B) <= Domain(A) Int Domain(B)";
    1.25 +by (Blast_tac 1);
    1.26 +qed "Domain_Int_subset";
    1.27 +
    1.28 +Goal "Domain(A) - Domain(B) <= Domain(A - B)";
    1.29 +by (Blast_tac 1);
    1.30 +qed "Domain_Diff_subset";
    1.31 +
    1.32 +
    1.33  (** Range **)
    1.34  
    1.35 +Goalw [Domain_def, Range_def] "a: Range(r) = (EX y. (y,a): r)";
    1.36 +by (Blast_tac 1);
    1.37 +qed "Range_iff";
    1.38 +
    1.39  qed_goalw "RangeI" thy [Range_def] "!!a b r.(a,b): r ==> b : Range(r)"
    1.40   (fn _ => [ (etac (converseI RS DomainI) 1) ]);
    1.41  
    1.42 @@ -172,6 +189,19 @@
    1.43  qed "Range_Id";
    1.44  Addsimps [Range_Id];
    1.45  
    1.46 +Goal "Range(A Un B) = Range(A) Un Range(B)";
    1.47 +by (Blast_tac 1);
    1.48 +qed "Range_Un_eq";
    1.49 +
    1.50 +Goal "Range(A Int B) <= Range(A) Int Range(B)";
    1.51 +by (Blast_tac 1);
    1.52 +qed "Range_Int_subset";
    1.53 +
    1.54 +Goal "Range(A) - Range(B) <= Range(A - B)";
    1.55 +by (Blast_tac 1);
    1.56 +qed "Range_Diff_subset";
    1.57 +
    1.58 +
    1.59  (*** Image of a set under a relation ***)
    1.60  
    1.61  overload_1st_set "Relation.op ^^";