# HG changeset patch
# User huffman
# Date 1334825387 -7200
# Node ID 28f6f4ad69bfbd6d5f346293463e14227cc7d167
# Parent  d83254265530d7e300455b2571795c9abadf4262
tuned lemmas (v)image_id;
removed duplicate of vimage_id

diff -r d83254265530 -r 28f6f4ad69bf src/HOL/Fun.thy
--- a/src/HOL/Fun.thy	Thu Apr 19 11:10:03 2012 +0200
+++ b/src/HOL/Fun.thy	Thu Apr 19 10:49:47 2012 +0200
@@ -24,11 +24,11 @@
 lemma id_apply [simp]: "id x = x"
   by (simp add: id_def)
 
-lemma image_id [simp]: "id ` Y = Y"
-  by (simp add: id_def)
+lemma image_id [simp]: "image id = id"
+  by (simp add: id_def fun_eq_iff)
 
-lemma vimage_id [simp]: "id -` A = A"
-  by (simp add: id_def)
+lemma vimage_id [simp]: "vimage id = id"
+  by (simp add: id_def fun_eq_iff)
 
 
 subsection {* The Composition Operator @{text "f \<circ> g"} *}
diff -r d83254265530 -r 28f6f4ad69bf src/HOL/Quotient.thy
--- a/src/HOL/Quotient.thy	Thu Apr 19 11:10:03 2012 +0200
+++ b/src/HOL/Quotient.thy	Thu Apr 19 10:49:47 2012 +0200
@@ -38,10 +38,6 @@
 
 definition "set_rel R xs ys \<equiv> \<forall>x y. R x y \<longrightarrow> x \<in> xs \<longleftrightarrow> y \<in> ys"
 
-lemma vimage_id:
-  "vimage id = id"
-  unfolding vimage_def fun_eq_iff by auto
-
 lemma set_rel_eq:
   "set_rel op = = op ="
   by (subst fun_eq_iff, subst fun_eq_iff) (simp add: set_eq_iff set_rel_def)