summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | paulson |

Wed, 11 Mar 1998 11:05:14 +0100 | |

changeset 4733 | 2c984ac036f5 |

parent 4732 | 10af4886b33f |

child 4734 | 6a7c70b053cc |

New theorem Image_eq_UN; deleted the silly vimage_inverse_Image

--- a/src/HOL/Relation.ML Wed Mar 11 11:03:43 1998 +0100 +++ b/src/HOL/Relation.ML Wed Mar 11 11:05:14 1998 +0100 @@ -219,17 +219,15 @@ "R ^^ (A Int B) <= R ^^ A Int R ^^ B" (fn _ => [ Blast_tac 1 ]); -qed_goal "Image_Un" thy - "R ^^ (A Un B) = R ^^ A Un R ^^ B" +qed_goal "Image_Un" thy "R ^^ (A Un B) = R ^^ A Un R ^^ B" (fn _ => [ Blast_tac 1 ]); - -qed_goal "Image_subset" thy - "!!A B r. r <= A Times B ==> r^^C <= B" +qed_goal "Image_subset" thy "!!A B r. r <= A Times B ==> r^^C <= B" (fn _ => [ (rtac subsetI 1), (REPEAT (eresolve_tac [asm_rl, ImageE, subsetD RS SigmaD2] 1)) ]); -goal thy "f-``(r^-1 ^^ {x}) = (UN y: r^-1 ^^ {x}. f-``{y})"; +(*NOT suitable for rewriting*) +goal thy "r^^B = (UN y: B. r^^{y})"; by (Blast_tac 1); -qed "vimage_inverse_Image"; +qed "Image_eq_UN";