author wenzelm Thu Jul 09 22:04:10 2009 +0200 (2009-07-09) changeset 31973 a89f758dba5b 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"
```