1.1 --- a/src/HOL/Fun.thy	Thu Dec 17 23:44:48 2009 +0100
     1.2 +++ b/src/HOL/Fun.thy	Mon Dec 21 08:32:03 2009 +0100
     1.3 @@ -74,6 +74,14 @@
     1.4  lemma o_id [simp]: "f o id = f"
     1.5  by (simp add: comp_def)
     1.6  
     1.7 +lemma o_eq_dest:
     1.8 +  "a o b = c o d \<Longrightarrow> a (b v) = c (d v)"
     1.9 +  by (simp only: o_def) (fact fun_cong)
    1.10 +
    1.11 +lemma o_eq_elim:
    1.12 +  "a o b = c o d \<Longrightarrow> ((\<And>v. a (b v) = c (d v)) \<Longrightarrow> R) \<Longrightarrow> R"
    1.13 +  by (erule meta_mp) (fact o_eq_dest) 
    1.14 +
    1.15  lemma image_compose: "(f o g) ` r = f`(g`r)"
    1.16  by (simp add: comp_def, blast)
    1.17