# HG changeset patch
# User krauss
# Date 1256596044 -3600
# Node ID ecb5cd453ef224382231ace451b9d1766f50aa15
# Parent  ab979f6e99f42572dbe7fc639e5dca69bb7dcd67
lemma converse_inv_image

diff -r ab979f6e99f4 -r ecb5cd453ef2 src/HOL/Relation.thy
--- 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 *}