lemma converse_inv_image

--- a/src/HOL/Relation.thy	Mon Oct 26 23:27:16 2009 +0100
+++ b/src/HOL/Relation.thy	Mon Oct 26 23:27:24 2009 +0100
@@ -607,6 +607,9 @@
 lemma in_inv_image[simp]: "((x,y) : inv_image r f) = ((f x, f y) : r)"
   by (auto simp:inv_image_def)
 
+lemma converse_inv_image[simp]: "(inv_image R f)^-1 = inv_image (R^-1) f"
+unfolding inv_image_def converse_def by auto
+
 
 subsection {* Finiteness *}