# HG changeset patch
# User hoelzl
# Date 1267713846 -3600
# Node ID 5f6bd3ac99f95970794f624350b75fb15efe99d0
# Parent  56b070cd7ab3236b0f126ec9b408f78ae07260b4
Added vimage_inter_cong

diff -r 56b070cd7ab3 -r 5f6bd3ac99f9 src/HOL/Set.thy
--- a/src/HOL/Set.thy	Thu Mar 04 11:22:06 2010 +0100
+++ b/src/HOL/Set.thy	Thu Mar 04 15:44:06 2010 +0100
@@ -1656,6 +1656,10 @@
     else if d \<in> A then -B else {})"  
   by (auto simp add: vimage_def) 
 
+lemma vimage_inter_cong:
+  "(\<And> w. w \<in> S \<Longrightarrow> f w = g w) \<Longrightarrow> f -` y \<inter> S = g -` y \<inter> S"
+  by auto
+
 lemma image_Int_subset: "f`(A Int B) <= f`A Int f`B"
 by blast