src/HOL/BNF_FP_Base.thy
changeset 55854 ee270328a781
parent 55811 aa1acc25126b
child 55906 abf91ebd0820
     1.1 --- a/src/HOL/BNF_FP_Base.thy	Mon Mar 03 12:48:19 2014 +0100
     1.2 +++ b/src/HOL/BNF_FP_Base.thy	Mon Mar 03 12:48:20 2014 +0100
     1.3 @@ -177,6 +177,9 @@
     1.4      type_definition.Abs_inverse[OF assms(1) UNIV_I]
     1.5      type_definition.Abs_inverse[OF assms(3) UNIV_I] dest: spec[of _ "Abs'' x" for x])
     1.6  
     1.7 +lemma vimage2p_id: "vimage2p id id R = R"
     1.8 +  unfolding vimage2p_def by auto
     1.9 +
    1.10  lemma vimage2p_comp: "vimage2p (f1 o f2) (g1 o g2) = vimage2p f2 g2 o vimage2p f1 g1"
    1.11    unfolding fun_eq_iff vimage2p_def o_apply by simp
    1.12