src/HOL/Fun.thy
changeset 55066 4e5ddf3162ac
parent 55019 0d5e831175de
child 55414 eab03e9cee8a
     1.1 --- a/src/HOL/Fun.thy	Mon Jan 20 18:24:56 2014 +0100
     1.2 +++ b/src/HOL/Fun.thy	Mon Jan 20 18:24:56 2014 +0100
     1.3 @@ -65,6 +65,12 @@
     1.4    "a o b = c o d \<Longrightarrow> ((\<And>v. a (b v) = c (d v)) \<Longrightarrow> R) \<Longrightarrow> R"
     1.5    by (simp add: fun_eq_iff) 
     1.6  
     1.7 +lemma comp_eq_dest_lhs: "a o b = c \<Longrightarrow> a (b v) = c v"
     1.8 +  by clarsimp
     1.9 +
    1.10 +lemma comp_eq_id_dest: "a o b = id o c \<Longrightarrow> a (b v) = c v"
    1.11 +  by clarsimp
    1.12 +
    1.13  lemma image_comp:
    1.14    "(f o g) ` r = f ` (g ` r)"
    1.15    by auto
    1.16 @@ -915,6 +921,8 @@
    1.17  lemmas o_id = comp_id
    1.18  lemmas o_eq_dest = comp_eq_dest
    1.19  lemmas o_eq_elim = comp_eq_elim
    1.20 +lemmas o_eq_dest_lhs = comp_eq_dest_lhs
    1.21 +lemmas o_eq_id_dest = comp_eq_id_dest
    1.22  lemmas image_compose = image_comp
    1.23  lemmas vimage_compose = vimage_comp
    1.24