# HG changeset patch # User paulson # Date 912419015 -3600 # Node ID 450cd1f0270bb4b564b5879423377b03c9f9d65a # Parent 7b84677315edecb8969b21fe143770e4dbd868b2 new theorems about diag diff -r 7b84677315ed -r 450cd1f0270b src/HOL/Relation.ML --- a/src/HOL/Relation.ML Sun Nov 29 13:21:38 1998 +0100 +++ b/src/HOL/Relation.ML Mon Nov 30 10:43:35 1998 +0100 @@ -54,7 +54,7 @@ Goal "diag(A) <= A Times A"; by (Blast_tac 1); -qed "diag_subset_Sigma"; +qed "diag_subset_Times"; @@ -161,6 +161,11 @@ qed "converse_Id"; Addsimps [converse_Id]; +Goal "(diag A) ^-1 = diag A"; +by (Blast_tac 1); +qed "converse_diag"; +Addsimps [converse_diag]; + (** Domain **) Goalw [Domain_def] "a: Domain(r) = (EX y. (a,y): r)"; @@ -226,6 +231,11 @@ qed "Range_Id"; Addsimps [Range_Id]; +Goal "Range (diag A) = A"; +by Auto_tac; +qed "Range_diag"; +Addsimps [Range_diag]; + Goal "Range(A Un B) = Range(A) Un Range(B)"; by (Blast_tac 1); qed "Range_Un_eq"; @@ -284,7 +294,11 @@ by (Blast_tac 1); qed "Image_Id"; -Addsimps [Image_Id]; +Goal "B<=A ==> diag A ^^ B = B"; +by (Blast_tac 1); +qed "Image_diag"; + +Addsimps [Image_Id, Image_diag]; qed_goal "Image_Int_subset" thy "R ^^ (A Int B) <= R ^^ A Int R ^^ B"