src/HOL/ex/Formal_Power_Series_Examples.thy
 author nipkow Fri Mar 06 17:38:47 2009 +0100 (2009-03-06) changeset 30313 b2441b0c8d38 parent 29698 91feea8e41e4 child 30748 fe67d729a61c permissions -rw-r--r--
 chaieb@29696 ` 1` ```(* Title: Formal_Power_Series_Examples.thy ``` chaieb@29696 ` 2` ``` ID: ``` chaieb@29696 ` 3` ``` Author: Amine Chaieb, University of Cambridge ``` chaieb@29696 ` 4` ```*) ``` chaieb@29696 ` 5` chaieb@29696 ` 6` ```header{* Some applications of formal power series and some properties over complex numbers*} ``` chaieb@29696 ` 7` chaieb@29698 ` 8` ```theory Formal_Power_Series_Examples ``` chaieb@29696 ` 9` ``` imports Formal_Power_Series Binomial Complex ``` chaieb@29696 ` 10` ```begin ``` chaieb@29696 ` 11` chaieb@29696 ` 12` ```section{* The generalized binomial theorem *} ``` chaieb@29696 ` 13` ```lemma gbinomial_theorem: ``` chaieb@29696 ` 14` ``` "((a::'a::{ring_char_0, field, division_by_zero, recpower})+b) ^ n = (\k=0..n. of_nat (n choose k) * a^k * b^(n-k))" ``` chaieb@29696 ` 15` ```proof- ``` chaieb@29696 ` 16` ``` from E_add_mult[of a b] ``` chaieb@29696 ` 17` ``` have "(E (a + b)) \$ n = (E a * E b)\$n" by simp ``` chaieb@29696 ` 18` ``` then have "(a + b) ^ n = (\i\nat = 0\nat..n. a ^ i * b ^ (n - i) * (of_nat (fact n) / of_nat (fact i * fact (n - i))))" ``` chaieb@29696 ` 19` ``` by (simp add: field_simps fps_mult_nth of_nat_mult[symmetric] setsum_right_distrib) ``` chaieb@29696 ` 20` ``` then show ?thesis ``` chaieb@29696 ` 21` ``` apply simp ``` chaieb@29696 ` 22` ``` apply (rule setsum_cong2) ``` chaieb@29696 ` 23` ``` apply simp ``` chaieb@29696 ` 24` ``` apply (frule binomial_fact[where ?'a = 'a, symmetric]) ``` chaieb@29696 ` 25` ``` by (simp add: field_simps of_nat_mult) ``` chaieb@29696 ` 26` ```qed ``` chaieb@29696 ` 27` chaieb@29696 ` 28` ```text{* And the nat-form -- also available from Binomial.thy *} ``` chaieb@29696 ` 29` ```lemma binomial_theorem: "(a+b) ^ n = (\k=0..n. (n choose k) * a^k * b^(n-k))" ``` chaieb@29696 ` 30` ``` using gbinomial_theorem[of "of_nat a" "of_nat b" n] ``` chaieb@29696 ` 31` ``` unfolding of_nat_add[symmetric] of_nat_power[symmetric] of_nat_mult[symmetric] of_nat_setsum[symmetric] ``` chaieb@29696 ` 32` ``` by simp ``` chaieb@29696 ` 33` chaieb@29696 ` 34` ```section {* The binomial series and Vandermonde's identity *} ``` chaieb@29696 ` 35` ```definition "fps_binomial a = Abs_fps (\n. a gchoose n)" ``` chaieb@29696 ` 36` chaieb@29696 ` 37` ```lemma fps_binomial_nth[simp]: "fps_binomial a \$ n = a gchoose n" ``` chaieb@29696 ` 38` ``` by (simp add: fps_binomial_def) ``` chaieb@29696 ` 39` chaieb@29696 ` 40` ```lemma fps_binomial_ODE_unique: ``` chaieb@29696 ` 41` ``` fixes c :: "'a::{field, recpower,ring_char_0}" ``` chaieb@29696 ` 42` ``` shows "fps_deriv a = (fps_const c * a) / (1 + X) \ a = fps_const (a\$0) * fps_binomial c" ``` chaieb@29696 ` 43` ``` (is "?lhs \ ?rhs") ``` chaieb@29696 ` 44` ```proof- ``` chaieb@29696 ` 45` ``` let ?da = "fps_deriv a" ``` chaieb@29696 ` 46` ``` let ?x1 = "(1 + X):: 'a fps" ``` chaieb@29696 ` 47` ``` let ?l = "?x1 * ?da" ``` chaieb@29696 ` 48` ``` let ?r = "fps_const c * a" ``` chaieb@29696 ` 49` ``` have x10: "?x1 \$ 0 \ 0" by simp ``` chaieb@29696 ` 50` ``` have "?l = ?r \ inverse ?x1 * ?l = inverse ?x1 * ?r" by simp ``` chaieb@29696 ` 51` ``` also have "\ \ ?da = (fps_const c * a) / ?x1" ``` chaieb@29696 ` 52` ``` apply (simp only: fps_divide_def mult_assoc[symmetric] inverse_mult_eq_1[OF x10]) ``` chaieb@29696 ` 53` ``` by (simp add: ring_simps) ``` chaieb@29696 ` 54` ``` finally have eq: "?l = ?r \ ?lhs" by simp ``` chaieb@29696 ` 55` ``` moreover ``` chaieb@29696 ` 56` ``` {assume h: "?l = ?r" ``` chaieb@29696 ` 57` ``` {fix n ``` chaieb@29696 ` 58` ``` from h have lrn: "?l \$ n = ?r\$n" by simp ``` chaieb@29696 ` 59` ``` ``` chaieb@29696 ` 60` ``` from lrn ``` chaieb@29696 ` 61` ``` have "a\$ Suc n = ((c - of_nat n) / of_nat (Suc n)) * a \$n" ``` chaieb@29696 ` 62` ``` apply (simp add: ring_simps del: of_nat_Suc) ``` chaieb@29696 ` 63` ``` by (cases n, simp_all add: field_simps del: of_nat_Suc) ``` chaieb@29696 ` 64` ``` } ``` chaieb@29696 ` 65` ``` note th0 = this ``` chaieb@29696 ` 66` ``` {fix n have "a\$n = (c gchoose n) * a\$0" ``` chaieb@29696 ` 67` ``` proof(induct n) ``` chaieb@29696 ` 68` ``` case 0 thus ?case by simp ``` chaieb@29696 ` 69` ``` next ``` chaieb@29696 ` 70` ``` case (Suc m) ``` chaieb@29696 ` 71` ``` thus ?case unfolding th0 ``` chaieb@29696 ` 72` ``` apply (simp add: field_simps del: of_nat_Suc) ``` chaieb@29696 ` 73` ``` unfolding mult_assoc[symmetric] gbinomial_mult_1 ``` chaieb@29696 ` 74` ``` by (simp add: ring_simps) ``` chaieb@29696 ` 75` ``` qed} ``` chaieb@29696 ` 76` ``` note th1 = this ``` chaieb@29696 ` 77` ``` have ?rhs ``` chaieb@29696 ` 78` ``` apply (simp add: fps_eq_iff) ``` chaieb@29696 ` 79` ``` apply (subst th1) ``` chaieb@29696 ` 80` ``` by (simp add: ring_simps)} ``` chaieb@29696 ` 81` ``` moreover ``` chaieb@29696 ` 82` ``` {assume h: ?rhs ``` chaieb@29696 ` 83` ``` have th00:"\x y. x * (a\$0 * y) = a\$0 * (x*y)" by (simp add: mult_commute) ``` chaieb@29696 ` 84` ``` have "?l = ?r" ``` chaieb@29696 ` 85` ``` apply (subst h) ``` chaieb@29696 ` 86` ``` apply (subst (2) h) ``` chaieb@29696 ` 87` ``` apply (clarsimp simp add: fps_eq_iff ring_simps) ``` chaieb@29696 ` 88` ``` unfolding mult_assoc[symmetric] th00 gbinomial_mult_1 ``` chaieb@29696 ` 89` ``` by (simp add: ring_simps gbinomial_mult_1)} ``` chaieb@29696 ` 90` ``` ultimately show ?thesis by blast ``` chaieb@29696 ` 91` ```qed ``` chaieb@29696 ` 92` chaieb@29696 ` 93` ```lemma fps_binomial_deriv: "fps_deriv (fps_binomial c) = fps_const c * fps_binomial c / (1 + X)" ``` chaieb@29696 ` 94` ```proof- ``` chaieb@29696 ` 95` ``` let ?a = "fps_binomial c" ``` chaieb@29696 ` 96` ``` have th0: "?a = fps_const (?a\$0) * ?a" by (simp) ``` chaieb@29696 ` 97` ``` from iffD2[OF fps_binomial_ODE_unique, OF th0] show ?thesis . ``` chaieb@29696 ` 98` ```qed ``` chaieb@29696 ` 99` chaieb@29696 ` 100` ```lemma fps_binomial_add_mult: "fps_binomial (c+d) = fps_binomial c * fps_binomial d" (is "?l = ?r") ``` chaieb@29696 ` 101` ```proof- ``` chaieb@29696 ` 102` ``` let ?P = "?r - ?l" ``` chaieb@29696 ` 103` ``` let ?b = "fps_binomial" ``` chaieb@29696 ` 104` ``` let ?db = "\x. fps_deriv (?b x)" ``` chaieb@29696 ` 105` ``` have "fps_deriv ?P = ?db c * ?b d + ?b c * ?db d - ?db (c + d)" by simp ``` chaieb@29696 ` 106` ``` also have "\ = inverse (1 + X) * (fps_const c * ?b c * ?b d + fps_const d * ?b c * ?b d - fps_const (c+d) * ?b (c + d))" ``` chaieb@29696 ` 107` ``` unfolding fps_binomial_deriv ``` chaieb@29696 ` 108` ``` by (simp add: fps_divide_def ring_simps) ``` chaieb@29696 ` 109` ``` also have "\ = (fps_const (c + d)/ (1 + X)) * ?P" ``` chaieb@29696 ` 110` ``` by (simp add: ring_simps fps_divide_def fps_const_add[symmetric] del: fps_const_add) ``` chaieb@29696 ` 111` ``` finally have th0: "fps_deriv ?P = fps_const (c+d) * ?P / (1 + X)" ``` chaieb@29696 ` 112` ``` by (simp add: fps_divide_def) ``` chaieb@29696 ` 113` ``` have "?P = fps_const (?P\$0) * ?b (c + d)" ``` chaieb@29696 ` 114` ``` unfolding fps_binomial_ODE_unique[symmetric] ``` chaieb@29696 ` 115` ``` using th0 by simp ``` chaieb@29696 ` 116` ``` hence "?P = 0" by (simp add: fps_mult_nth) ``` chaieb@29696 ` 117` ``` then show ?thesis by simp ``` chaieb@29696 ` 118` ```qed ``` chaieb@29696 ` 119` chaieb@29696 ` 120` ```lemma fps_minomial_minus_one: "fps_binomial (- 1) = inverse (1 + X)" ``` chaieb@29696 ` 121` ``` (is "?l = inverse ?r") ``` chaieb@29696 ` 122` ```proof- ``` chaieb@29696 ` 123` ``` have th: "?r\$0 \ 0" by simp ``` chaieb@29696 ` 124` ``` have th': "fps_deriv (inverse ?r) = fps_const (- 1) * inverse ?r / (1 + X)" ``` chaieb@29696 ` 125` ``` by (simp add: fps_inverse_deriv[OF th] fps_divide_def power2_eq_square mult_commute fps_const_neg[symmetric] del: fps_const_neg) ``` chaieb@29696 ` 126` ``` have eq: "inverse ?r \$ 0 = 1" ``` chaieb@29696 ` 127` ``` by (simp add: fps_inverse_def) ``` chaieb@29696 ` 128` ``` from iffD1[OF fps_binomial_ODE_unique[of "inverse (1 + X)" "- 1"] th'] eq ``` chaieb@29696 ` 129` ``` show ?thesis by (simp add: fps_inverse_def) ``` chaieb@29696 ` 130` ```qed ``` chaieb@29696 ` 131` chaieb@29696 ` 132` ```lemma gbinomial_Vandermond: "setsum (\k. (a gchoose k) * (b gchoose (n - k))) {0..n} = (a + b) gchoose n" ``` chaieb@29696 ` 133` ```proof- ``` chaieb@29696 ` 134` ``` let ?ba = "fps_binomial a" ``` chaieb@29696 ` 135` ``` let ?bb = "fps_binomial b" ``` chaieb@29696 ` 136` ``` let ?bab = "fps_binomial (a + b)" ``` chaieb@29696 ` 137` ``` from fps_binomial_add_mult[of a b] have "?bab \$ n = (?ba * ?bb)\$n" by simp ``` chaieb@29696 ` 138` ``` then show ?thesis by (simp add: fps_mult_nth) ``` chaieb@29696 ` 139` ```qed ``` chaieb@29696 ` 140` chaieb@29696 ` 141` ```lemma binomial_Vandermond: "setsum (\k. (a choose k) * (b choose (n - k))) {0..n} = (a + b) choose n" ``` chaieb@29696 ` 142` ``` using gbinomial_Vandermond[of "(of_nat a)" "of_nat b" n] ``` chaieb@29696 ` 143` ``` ``` chaieb@29696 ` 144` ``` apply (simp only: binomial_gbinomial[symmetric] of_nat_mult[symmetric] of_nat_setsum[symmetric] of_nat_add[symmetric]) ``` chaieb@29696 ` 145` ``` by simp ``` chaieb@29696 ` 146` chaieb@29696 ` 147` ```lemma binomial_symmetric: assumes kn: "k \ n" ``` chaieb@29696 ` 148` ``` shows "n choose k = n choose (n - k)" ``` chaieb@29696 ` 149` ```proof- ``` chaieb@29696 ` 150` ``` from kn have kn': "n - k \ n" by arith ``` chaieb@29696 ` 151` ``` from binomial_fact_lemma[OF kn] binomial_fact_lemma[OF kn'] ``` chaieb@29696 ` 152` ``` have "fact k * fact (n - k) * (n choose k) = fact (n - k) * fact (n - (n - k)) * (n choose (n - k))" by simp ``` chaieb@29696 ` 153` ``` then show ?thesis using kn by simp ``` chaieb@29696 ` 154` ```qed ``` chaieb@29696 ` 155` ``` ``` chaieb@29696 ` 156` ```lemma binomial_Vandermond_same: "setsum (\k. (n choose k)^2) {0..n} = (2*n) choose n" ``` chaieb@29696 ` 157` ``` using binomial_Vandermond[of n n n,symmetric] ``` chaieb@29696 ` 158` ``` unfolding nat_mult_2 apply (simp add: power2_eq_square) ``` chaieb@29696 ` 159` ``` apply (rule setsum_cong2) ``` chaieb@29696 ` 160` ``` by (auto intro: binomial_symmetric) ``` chaieb@29696 ` 161` chaieb@29696 ` 162` ```section {* Relation between formal sine/cosine and the exponential FPS*} ``` chaieb@29696 ` 163` ```lemma Eii_sin_cos: ``` chaieb@29696 ` 164` ``` "E (ii * c) = fps_cos c + fps_const ii * fps_sin c " ``` chaieb@29696 ` 165` ``` (is "?l = ?r") ``` chaieb@29696 ` 166` ```proof- ``` chaieb@29696 ` 167` ``` {fix n::nat ``` chaieb@29696 ` 168` ``` {assume en: "even n" ``` chaieb@29696 ` 169` ``` from en obtain m where m: "n = 2*m" ``` chaieb@29696 ` 170` ``` unfolding even_mult_two_ex by blast ``` chaieb@29696 ` 171` ``` ``` chaieb@29696 ` 172` ``` have "?l \$n = ?r\$n" ``` chaieb@29696 ` 173` ``` by (simp add: m fps_sin_def fps_cos_def power_mult_distrib ``` chaieb@29696 ` 174` ``` power_mult power_minus)} ``` chaieb@29696 ` 175` ``` moreover ``` chaieb@29696 ` 176` ``` {assume on: "odd n" ``` chaieb@29696 ` 177` ``` from on obtain m where m: "n = 2*m + 1" ``` chaieb@29696 ` 178` ``` unfolding odd_nat_equiv_def2 by (auto simp add: nat_mult_2) ``` chaieb@29696 ` 179` ``` have "?l \$n = ?r\$n" ``` chaieb@29696 ` 180` ``` by (simp add: m fps_sin_def fps_cos_def power_mult_distrib ``` chaieb@29696 ` 181` ``` power_mult power_minus)} ``` chaieb@29696 ` 182` ``` ultimately have "?l \$n = ?r\$n" by blast} ``` chaieb@29696 ` 183` ``` then show ?thesis by (simp add: fps_eq_iff) ``` chaieb@29696 ` 184` ```qed ``` chaieb@29696 ` 185` chaieb@29696 ` 186` ```lemma fps_sin_neg[simp]: "fps_sin (- c) = - fps_sin c" ``` chaieb@29696 ` 187` ```by (simp add: fps_eq_iff fps_sin_def) ``` chaieb@29696 ` 188` chaieb@29696 ` 189` ```lemma fps_cos_neg[simp]: "fps_cos (- c) = fps_cos c" ``` chaieb@29696 ` 190` ``` by (simp add: fps_eq_iff fps_cos_def) ``` chaieb@29696 ` 191` ```lemma E_minus_ii_sin_cos: "E (- (ii * c)) = fps_cos c - fps_const ii * fps_sin c " ``` chaieb@29696 ` 192` ``` unfolding minus_mult_right Eii_sin_cos by simp ``` chaieb@29696 ` 193` chaieb@29696 ` 194` ```lemma fps_cos_Eii: ``` chaieb@29696 ` 195` ``` "fps_cos c = (E (ii * c) + E (- ii * c)) / fps_const 2" ``` chaieb@29696 ` 196` ```proof- ``` chaieb@29696 ` 197` ``` have th: "fps_cos c + fps_cos c = fps_cos c * fps_const 2" ``` chaieb@29696 ` 198` ``` by (simp add: fps_eq_iff) ``` chaieb@29696 ` 199` ``` show ?thesis ``` chaieb@29696 ` 200` ``` unfolding Eii_sin_cos minus_mult_commute ``` chaieb@29696 ` 201` ``` by (simp add: fps_divide_def fps_const_inverse th) ``` chaieb@29696 ` 202` ```qed ``` chaieb@29696 ` 203` chaieb@29696 ` 204` ```lemma fps_sin_Eii: ``` chaieb@29696 ` 205` ``` "fps_sin c = (E (ii * c) - E (- ii * c)) / fps_const (2*ii)" ``` chaieb@29696 ` 206` ```proof- ``` chaieb@29696 ` 207` ``` have th: "fps_const \ * fps_sin c + fps_const \ * fps_sin c = fps_sin c * fps_const (2 * ii)" ``` chaieb@29696 ` 208` ``` by (simp add: fps_eq_iff) ``` chaieb@29696 ` 209` ``` show ?thesis ``` chaieb@29696 ` 210` ``` unfolding Eii_sin_cos minus_mult_commute ``` chaieb@29696 ` 211` ``` by (simp add: fps_divide_def fps_const_inverse th) ``` chaieb@29696 ` 212` ```qed ``` chaieb@29696 ` 213` chaieb@29696 ` 214` ```lemma fps_const_mult_2: "fps_const (2::'a::number_ring) * a = a +a" ``` chaieb@29696 ` 215` ``` by (simp add: fps_eq_iff) ``` chaieb@29696 ` 216` chaieb@29696 ` 217` ```lemma fps_const_mult_2_right: "a * fps_const (2::'a::number_ring) = a +a" ``` chaieb@29696 ` 218` ``` by (simp add: fps_eq_iff) ``` chaieb@29696 ` 219` chaieb@29696 ` 220` ```lemma fps_tan_Eii: ``` chaieb@29696 ` 221` ``` "fps_tan c = (E (ii * c) - E (- ii * c)) / (fps_const ii * (E (ii * c) + E (- ii * c)))" ``` chaieb@29696 ` 222` ``` unfolding fps_tan_def fps_sin_Eii fps_cos_Eii mult_minus_left E_neg ``` chaieb@29696 ` 223` ``` apply (simp add: fps_divide_def fps_inverse_mult fps_const_mult[symmetric] fps_const_inverse del: fps_const_mult) ``` chaieb@29696 ` 224` ``` by simp ``` chaieb@29696 ` 225` chaieb@29696 ` 226` ```lemma fps_demoivre: "(fps_cos a + fps_const ii * fps_sin a)^n = fps_cos (of_nat n * a) + fps_const ii * fps_sin (of_nat n * a)" ``` chaieb@29696 ` 227` ``` unfolding Eii_sin_cos[symmetric] E_power_mult ``` chaieb@29696 ` 228` ``` by (simp add: mult_ac) ``` chaieb@29696 ` 229` chaieb@29696 ` 230` ```text{* Now some trigonometric identities *} ``` chaieb@29696 ` 231` ```lemma fps_sin_add: ``` chaieb@29696 ` 232` ``` "fps_sin (a+b) = fps_sin (a::complex) * fps_cos b + fps_cos a * fps_sin b" ``` chaieb@29696 ` 233` ```proof- ``` chaieb@29696 ` 234` ``` let ?ca = "fps_cos a" ``` chaieb@29696 ` 235` ``` let ?cb = "fps_cos b" ``` chaieb@29696 ` 236` ``` let ?sa = "fps_sin a" ``` chaieb@29696 ` 237` ``` let ?sb = "fps_sin b" ``` chaieb@29696 ` 238` ``` let ?i = "fps_const ii" ``` chaieb@29696 ` 239` ``` have i: "?i*?i = fps_const -1" by simp ``` chaieb@29696 ` 240` ``` have "fps_sin (a + b) = ``` chaieb@29696 ` 241` ``` ((?ca + ?i * ?sa) * (?cb + ?i*?sb) - (?ca - ?i*?sa) * (?cb - ?i*?sb)) * ``` chaieb@29696 ` 242` ``` fps_const (- (\ / 2))" ``` chaieb@29696 ` 243` ``` apply(simp add: fps_sin_Eii[of "a+b"] fps_divide_def minus_mult_commute) ``` chaieb@29696 ` 244` ``` unfolding right_distrib ``` chaieb@29696 ` 245` ``` apply (simp add: Eii_sin_cos E_minus_ii_sin_cos fps_const_inverse E_add_mult) ``` chaieb@29696 ` 246` ``` by (simp add: ring_simps) ``` chaieb@29696 ` 247` ``` also have "\ = (?ca * ?cb + ?i*?ca * ?sb + ?i * ?sa * ?cb + (?i*?i)*?sa*?sb - ?ca*?cb + ?i*?ca * ?sb + ?i*?sa*?cb - (?i*?i)*?sa * ?sb) * fps_const (- ii/2)" ``` chaieb@29696 ` 248` ``` by (simp add: ring_simps) ``` chaieb@29696 ` 249` ``` also have "\ = (fps_const 2 * ?i * (?ca * ?sb + ?sa * ?cb)) * fps_const (- ii/2)" ``` chaieb@29696 ` 250` ``` apply simp ``` chaieb@29696 ` 251` ``` apply (simp add: ring_simps) ``` chaieb@29696 ` 252` ``` apply (simp add: ring_simps add: fps_const_mult[symmetric] del:fps_const_mult) ``` chaieb@29696 ` 253` ``` unfolding fps_const_mult_2_right ``` chaieb@29696 ` 254` ``` by (simp add: ring_simps) ``` chaieb@29696 ` 255` ``` also have "\ = (fps_const 2 * ?i * fps_const (- ii/2)) * (?ca * ?sb + ?sa * ?cb)" ``` chaieb@29696 ` 256` ``` by (simp only: mult_ac) ``` chaieb@29696 ` 257` ``` also have "\ = ?sa * ?cb + ?ca*?sb" ``` chaieb@29696 ` 258` ``` by simp ``` chaieb@29696 ` 259` ``` finally show ?thesis . ``` chaieb@29696 ` 260` ```qed ``` chaieb@29696 ` 261` chaieb@29696 ` 262` ```lemma fps_cos_add: ``` chaieb@29696 ` 263` ``` "fps_cos (a+b) = fps_cos (a::complex) * fps_cos b - fps_sin a * fps_sin b" ``` chaieb@29696 ` 264` ```proof- ``` chaieb@29696 ` 265` ``` let ?ca = "fps_cos a" ``` chaieb@29696 ` 266` ``` let ?cb = "fps_cos b" ``` chaieb@29696 ` 267` ``` let ?sa = "fps_sin a" ``` chaieb@29696 ` 268` ``` let ?sb = "fps_sin b" ``` chaieb@29696 ` 269` ``` let ?i = "fps_const ii" ``` chaieb@29696 ` 270` ``` have i: "?i*?i = fps_const -1" by simp ``` chaieb@29696 ` 271` ``` have i': "\x. ?i * (?i * x) = - x" ``` chaieb@29696 ` 272` ``` apply (simp add: mult_assoc[symmetric] i) ``` chaieb@29696 ` 273` ``` by (simp add: fps_eq_iff) ``` chaieb@29696 ` 274` ``` have m1: "\x. x * fps_const (-1 ::complex) = - x" "\x. fps_const (-1 :: complex) * x = - x" ``` chaieb@29696 ` 275` ``` by (auto simp add: fps_eq_iff) ``` chaieb@29696 ` 276` chaieb@29696 ` 277` ``` have "fps_cos (a + b) = ``` chaieb@29696 ` 278` ``` ((?ca + ?i * ?sa) * (?cb + ?i*?sb) + (?ca - ?i*?sa) * (?cb - ?i*?sb)) * ``` chaieb@29696 ` 279` ``` fps_const (1/ 2)" ``` chaieb@29696 ` 280` ``` apply(simp add: fps_cos_Eii[of "a+b"] fps_divide_def minus_mult_commute) ``` chaieb@29696 ` 281` ``` unfolding right_distrib minus_add_distrib ``` chaieb@29696 ` 282` ``` apply (simp add: Eii_sin_cos E_minus_ii_sin_cos fps_const_inverse E_add_mult) ``` chaieb@29696 ` 283` ``` by (simp add: ring_simps) ``` chaieb@29696 ` 284` ``` also have "\ = (?ca * ?cb + ?i*?ca * ?sb + ?i * ?sa * ?cb + (?i*?i)*?sa*?sb + ?ca*?cb - ?i*?ca * ?sb - ?i*?sa*?cb + (?i*?i)*?sa * ?sb) * fps_const (1/2)" ``` chaieb@29696 ` 285` ``` apply simp ``` chaieb@29696 ` 286` ``` by (simp add: ring_simps i' m1) ``` chaieb@29696 ` 287` ``` also have "\ = (fps_const 2 * (?ca * ?cb - ?sa * ?sb)) * fps_const (1/2)" ``` chaieb@29696 ` 288` ``` apply simp ``` chaieb@29696 ` 289` ``` by (simp add: ring_simps m1 fps_const_mult_2_right) ``` chaieb@29696 ` 290` ``` also have "\ = (fps_const 2 * fps_const (1/2)) * (?ca * ?cb - ?sa * ?sb)" ``` chaieb@29696 ` 291` ``` by (simp only: mult_ac) ``` chaieb@29696 ` 292` ``` also have "\ = ?ca * ?cb - ?sa*?sb" ``` chaieb@29696 ` 293` ``` by simp ``` chaieb@29696 ` 294` ``` finally show ?thesis . ``` chaieb@29696 ` 295` ```qed ``` chaieb@29696 ` 296` chaieb@29696 ` 297` `end`