Three new facts about Image
authorpaulson
Mon Feb 02 12:55:39 1998 +0100 (1998-02-02)
changeset 45936fc8f224655f
parent 4592 ff0c5c57fdfb
child 4594 f8d4387b40d9
Three new facts about Image
src/HOL/Relation.ML
     1.1 --- a/src/HOL/Relation.ML	Mon Feb 02 12:48:11 1998 +0100
     1.2 +++ b/src/HOL/Relation.ML	Mon Feb 02 12:55:39 1998 +0100
     1.3 @@ -171,6 +171,22 @@
     1.4  AddIs  [ImageI];
     1.5  AddSEs [ImageE];
     1.6  
     1.7 +
     1.8 +qed_goal "Image_empty" Relation.thy
     1.9 +    "R^^{} = {}"
    1.10 + (fn _ => [ Blast_tac 1 ]);
    1.11 +
    1.12 +Addsimps [Image_empty];
    1.13 +
    1.14 +qed_goal "Image_Int_subset" Relation.thy
    1.15 +    "R ^^ (A Int B) <= R ^^ A Int R ^^ B"
    1.16 + (fn _ => [ Blast_tac 1 ]);
    1.17 +
    1.18 +qed_goal "Image_Un" Relation.thy
    1.19 +    "R ^^ (A Un B) = R ^^ A Un R ^^ B"
    1.20 + (fn _ => [ Blast_tac 1 ]);
    1.21 +
    1.22 +
    1.23  qed_goal "Image_subset" Relation.thy
    1.24      "!!A B r. r <= A Times B ==> r^^C <= B"
    1.25   (fn _ =>