merged
authorwenzelm
Thu Jul 09 22:04:10 2009 +0200 (2009-07-09)
changeset 31973a89f758dba5b
parent 31971 8c1b845ed105
parent 31972 02f02097e1e4
child 31974 e81979a703a4
child 31978 e5b698bca555
merged
     1.1 --- a/src/HOL/ex/Formal_Power_Series_Examples.thy	Thu Jul 09 22:01:41 2009 +0200
     1.2 +++ b/src/HOL/ex/Formal_Power_Series_Examples.thy	Thu Jul 09 22:04:10 2009 +0200
     1.3 @@ -184,9 +184,10 @@
     1.4  qed
     1.5  
     1.6  lemma E_minus_ii_sin_cos: "E (- (ii * c)) = fps_cos c - fps_const ii * fps_sin c "
     1.7 -  unfolding minus_mult_right Eii_sin_cos by simp
     1.8 +  unfolding minus_mult_right Eii_sin_cos by (simp add: fps_sin_even fps_cos_odd)
     1.9  
    1.10 -lemma fps_const_minus: "fps_const (c::'a::group_add) - fps_const d = fps_const (c - d)  "by (simp add: fps_eq_iff fps_const_def)
    1.11 +lemma fps_const_minus: "fps_const (c::'a::group_add) - fps_const d = fps_const (c - d)"
    1.12 +  by (simp add: fps_eq_iff fps_const_def)
    1.13  
    1.14  lemma fps_number_of_fps_const: "number_of i = fps_const (number_of i :: 'a:: {comm_ring_1, number_ring})"
    1.15    apply (subst (2) number_of_eq)
    1.16 @@ -201,7 +202,8 @@
    1.17      by (simp add: fps_eq_iff fps_number_of_fps_const complex_number_of_def[symmetric])
    1.18    show ?thesis
    1.19    unfolding Eii_sin_cos minus_mult_commute
    1.20 -  by (simp add: fps_number_of_fps_const fps_divide_def fps_const_inverse th complex_number_of_def[symmetric])
    1.21 +  by (simp add: fps_sin_even fps_cos_odd fps_number_of_fps_const
    1.22 +    fps_divide_def fps_const_inverse th complex_number_of_def[symmetric])
    1.23  qed
    1.24  
    1.25  lemma fps_sin_Eii:
    1.26 @@ -211,7 +213,7 @@
    1.27      by (simp add: fps_eq_iff fps_number_of_fps_const complex_number_of_def[symmetric])
    1.28    show ?thesis
    1.29    unfolding Eii_sin_cos minus_mult_commute
    1.30 -  by (simp add: fps_divide_def fps_const_inverse th)
    1.31 +  by (simp add: fps_sin_even fps_cos_odd fps_divide_def fps_const_inverse th)
    1.32  qed
    1.33  
    1.34  lemma fps_const_mult_2: "fps_const (2::'a::number_ring) * a = a +a"