author chaieb Fri, 27 Mar 2009 17:35:21 +0000 changeset 30748 fe67d729a61c parent 30747 b8ca7e450de3 child 30752 5272864d6892 child 30792 809c38c1a26c
fixed proof
```--- a/src/HOL/ex/Formal_Power_Series_Examples.thy	Fri Mar 27 14:44:18 2009 +0000
+++ b/src/HOL/ex/Formal_Power_Series_Examples.thy	Fri Mar 27 17:35:21 2009 +0000
@@ -191,31 +191,39 @@
lemma E_minus_ii_sin_cos: "E (- (ii * c)) = fps_cos c - fps_const ii * fps_sin c "
unfolding minus_mult_right Eii_sin_cos by simp

+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)
+
+lemma fps_number_of_fps_const: "number_of i = fps_const (number_of i :: 'a:: {comm_ring_1, number_ring})"
+  apply (subst (2) number_of_eq)
+apply(rule int_induct[of _ 0])
+
lemma fps_cos_Eii:
"fps_cos c = (E (ii * c) + E (- ii * c)) / fps_const 2"
proof-
have th: "fps_cos c + fps_cos c = fps_cos c * fps_const 2"
+    by (simp add: fps_eq_iff fps_number_of_fps_const complex_number_of_def[symmetric])
show ?thesis
unfolding Eii_sin_cos minus_mult_commute
-  by (simp add: fps_divide_def fps_const_inverse th)
+  by (simp add: fps_number_of_fps_const fps_divide_def fps_const_inverse th complex_number_of_def[symmetric])
qed

lemma fps_sin_Eii:
"fps_sin c = (E (ii * c) - E (- ii * c)) / fps_const (2*ii)"
proof-
have th: "fps_const \<i> * fps_sin c + fps_const \<i> * fps_sin c = fps_sin c * fps_const (2 * ii)"
+    by (simp add: fps_eq_iff fps_number_of_fps_const complex_number_of_def[symmetric])
show ?thesis
unfolding Eii_sin_cos minus_mult_commute
by (simp add: fps_divide_def fps_const_inverse th)
qed

lemma fps_const_mult_2: "fps_const (2::'a::number_ring) * a = a +a"