tuned lemmas (v)image_id;
authorhuffman
Thu Apr 19 10:49:47 2012 +0200 (2012-04-19)
changeset 4757928f6f4ad69bf
parent 47578 d83254265530
child 47580 d99c883cdf2c
tuned lemmas (v)image_id;
removed duplicate of vimage_id
src/HOL/Fun.thy
src/HOL/Quotient.thy
     1.1 --- a/src/HOL/Fun.thy	Thu Apr 19 11:10:03 2012 +0200
     1.2 +++ b/src/HOL/Fun.thy	Thu Apr 19 10:49:47 2012 +0200
     1.3 @@ -24,11 +24,11 @@
     1.4  lemma id_apply [simp]: "id x = x"
     1.5    by (simp add: id_def)
     1.6  
     1.7 -lemma image_id [simp]: "id ` Y = Y"
     1.8 -  by (simp add: id_def)
     1.9 +lemma image_id [simp]: "image id = id"
    1.10 +  by (simp add: id_def fun_eq_iff)
    1.11  
    1.12 -lemma vimage_id [simp]: "id -` A = A"
    1.13 -  by (simp add: id_def)
    1.14 +lemma vimage_id [simp]: "vimage id = id"
    1.15 +  by (simp add: id_def fun_eq_iff)
    1.16  
    1.17  
    1.18  subsection {* The Composition Operator @{text "f \<circ> g"} *}
     2.1 --- a/src/HOL/Quotient.thy	Thu Apr 19 11:10:03 2012 +0200
     2.2 +++ b/src/HOL/Quotient.thy	Thu Apr 19 10:49:47 2012 +0200
     2.3 @@ -38,10 +38,6 @@
     2.4  
     2.5  definition "set_rel R xs ys \<equiv> \<forall>x y. R x y \<longrightarrow> x \<in> xs \<longleftrightarrow> y \<in> ys"
     2.6  
     2.7 -lemma vimage_id:
     2.8 -  "vimage id = id"
     2.9 -  unfolding vimage_def fun_eq_iff by auto
    2.10 -
    2.11  lemma set_rel_eq:
    2.12    "set_rel op = = op ="
    2.13    by (subst fun_eq_iff, subst fun_eq_iff) (simp add: set_eq_iff set_rel_def)