New theorem Image_eq_UN; deleted the silly vimage_inverse_Image
authorpaulson
Wed Mar 11 11:05:14 1998 +0100 (1998-03-11)
changeset 47332c984ac036f5
parent 4732 10af4886b33f
child 4734 6a7c70b053cc
New theorem Image_eq_UN; deleted the silly vimage_inverse_Image
src/HOL/Relation.ML
     1.1 --- a/src/HOL/Relation.ML	Wed Mar 11 11:03:43 1998 +0100
     1.2 +++ b/src/HOL/Relation.ML	Wed Mar 11 11:05:14 1998 +0100
     1.3 @@ -219,17 +219,15 @@
     1.4      "R ^^ (A Int B) <= R ^^ A Int R ^^ B"
     1.5   (fn _ => [ Blast_tac 1 ]);
     1.6  
     1.7 -qed_goal "Image_Un" thy
     1.8 -    "R ^^ (A Un B) = R ^^ A Un R ^^ B"
     1.9 +qed_goal "Image_Un" thy "R ^^ (A Un B) = R ^^ A Un R ^^ B"
    1.10   (fn _ => [ Blast_tac 1 ]);
    1.11  
    1.12 -
    1.13 -qed_goal "Image_subset" thy
    1.14 -    "!!A B r. r <= A Times B ==> r^^C <= B"
    1.15 +qed_goal "Image_subset" thy "!!A B r. r <= A Times B ==> r^^C <= B"
    1.16   (fn _ =>
    1.17    [ (rtac subsetI 1),
    1.18      (REPEAT (eresolve_tac [asm_rl, ImageE, subsetD RS SigmaD2] 1)) ]);
    1.19  
    1.20 -goal thy "f-``(r^-1 ^^ {x}) = (UN y: r^-1 ^^ {x}. f-``{y})";
    1.21 +(*NOT suitable for rewriting*)
    1.22 +goal thy "r^^B = (UN y: B. r^^{y})";
    1.23  by (Blast_tac 1);
    1.24 -qed "vimage_inverse_Image";
    1.25 +qed "Image_eq_UN";