src/HOL/Relation.ML
changeset 5995 450cd1f0270b
parent 5978 fa2c2dd74f8c
child 5998 b2ecd577b8a3
     1.1 --- a/src/HOL/Relation.ML	Sun Nov 29 13:21:38 1998 +0100
     1.2 +++ b/src/HOL/Relation.ML	Mon Nov 30 10:43:35 1998 +0100
     1.3 @@ -54,7 +54,7 @@
     1.4  
     1.5  Goal "diag(A) <= A Times A";
     1.6  by (Blast_tac 1);
     1.7 -qed "diag_subset_Sigma";
     1.8 +qed "diag_subset_Times";
     1.9  
    1.10  
    1.11  
    1.12 @@ -161,6 +161,11 @@
    1.13  qed "converse_Id";
    1.14  Addsimps [converse_Id];
    1.15  
    1.16 +Goal "(diag A) ^-1 = diag A";
    1.17 +by (Blast_tac 1);
    1.18 +qed "converse_diag";
    1.19 +Addsimps [converse_diag];
    1.20 +
    1.21  (** Domain **)
    1.22  
    1.23  Goalw [Domain_def] "a: Domain(r) = (EX y. (a,y): r)";
    1.24 @@ -226,6 +231,11 @@
    1.25  qed "Range_Id";
    1.26  Addsimps [Range_Id];
    1.27  
    1.28 +Goal "Range (diag A) = A";
    1.29 +by Auto_tac;
    1.30 +qed "Range_diag";
    1.31 +Addsimps [Range_diag];
    1.32 +
    1.33  Goal "Range(A Un B) = Range(A) Un Range(B)";
    1.34  by (Blast_tac 1);
    1.35  qed "Range_Un_eq";
    1.36 @@ -284,7 +294,11 @@
    1.37  by (Blast_tac 1);
    1.38  qed "Image_Id";
    1.39  
    1.40 -Addsimps [Image_Id];
    1.41 +Goal "B<=A ==> diag A ^^ B = B";
    1.42 +by (Blast_tac 1);
    1.43 +qed "Image_diag";
    1.44 +
    1.45 +Addsimps [Image_Id, Image_diag];
    1.46  
    1.47  qed_goal "Image_Int_subset" thy
    1.48      "R ^^ (A Int B) <= R ^^ A Int R ^^ B"