# HG changeset patch # User chaieb # Date 1247631265 -7200 # Node ID adea7a729c7a66ed01bdf8971e12ce92d8673b0d # Parent 6ef7056e5215cfc11cbf2c4c23f5a28c70aa4e26 Moved important theorems from FPS_Examples to FPS --- they are not really examples but useful theorems that are being reproved since unnoticed. diff -r 6ef7056e5215 -r adea7a729c7a src/HOL/IsaMakefile --- a/src/HOL/IsaMakefile Tue Jul 14 12:18:52 2009 +0200 +++ b/src/HOL/IsaMakefile Wed Jul 15 06:14:25 2009 +0200 @@ -886,8 +886,7 @@ ex/Codegenerator_Pretty_Test.thy ex/Coherent.thy \ ex/Commutative_RingEx.thy ex/Commutative_Ring_Complete.thy \ ex/Efficient_Nat_examples.thy \ - ex/Eval_Examples.thy \ - ex/Formal_Power_Series_Examples.thy ex/Fundefs.thy \ + ex/Eval_Examples.thy ex/Fundefs.thy \ ex/Groebner_Examples.thy ex/Guess.thy ex/HarmonicSeries.thy \ ex/Hebrew.thy ex/Hex_Bin_Examples.thy ex/Higher_Order_Logic.thy \ ex/Hilbert_Classical.thy \ diff -r 6ef7056e5215 -r adea7a729c7a src/HOL/Library/Formal_Power_Series.thy --- a/src/HOL/Library/Formal_Power_Series.thy Tue Jul 14 12:18:52 2009 +0200 +++ b/src/HOL/Library/Formal_Power_Series.thy Wed Jul 15 06:14:25 2009 +0200 @@ -5,7 +5,7 @@ header{* A formalization of formal power series *} theory Formal_Power_Series -imports Complex_Main +imports Complex_Main Binomial begin @@ -2625,6 +2625,29 @@ apply (auto simp add: fps_eq_iff E_def fps_compose_def power_mult_distrib) by (simp add: cond_value_iff cond_application_beta setsum_delta' cong del: if_weak_cong) +text{* The generalized binomial theorem as a consequence of @{thm E_add_mult} *} + +lemma gbinomial_theorem: + "((a::'a::{field_char_0, division_by_zero})+b) ^ n = (\k=0..n. of_nat (n choose k) * a^k * b^(n-k))" +proof- + from E_add_mult[of a b] + have "(E (a + b)) $ n = (E a * E b)$n" by simp + 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))))" + by (simp add: field_simps fps_mult_nth of_nat_mult[symmetric] setsum_right_distrib) + then show ?thesis + apply simp + apply (rule setsum_cong2) + apply simp + apply (frule binomial_fact[where ?'a = 'a, symmetric]) + by (simp add: field_simps of_nat_mult) +qed + +text{* And the nat-form -- also available from Binomial.thy *} +lemma binomial_theorem: "(a+b) ^ n = (\k=0..n. (n choose k) * a^k * b^(n-k))" + using gbinomial_theorem[of "of_nat a" "of_nat b" n] + unfolding of_nat_add[symmetric] of_nat_power[symmetric] of_nat_mult[symmetric] of_nat_setsum[symmetric] + by simp + subsubsection{* Logarithmic series *} lemma Abs_fps_if_0: @@ -2679,6 +2702,137 @@ unfolding fps_deriv_eq_iff by simp qed +subsubsection{* Binomial series *} + +definition "fps_binomial a = Abs_fps (\n. a gchoose n)" + +lemma fps_binomial_nth[simp]: "fps_binomial a $ n = a gchoose n" + by (simp add: fps_binomial_def) + +lemma fps_binomial_ODE_unique: + fixes c :: "'a::field_char_0" + shows "fps_deriv a = (fps_const c * a) / (1 + X) \ a = fps_const (a$0) * fps_binomial c" + (is "?lhs \ ?rhs") +proof- + let ?da = "fps_deriv a" + let ?x1 = "(1 + X):: 'a fps" + let ?l = "?x1 * ?da" + let ?r = "fps_const c * a" + have x10: "?x1 $ 0 \ 0" by simp + have "?l = ?r \ inverse ?x1 * ?l = inverse ?x1 * ?r" by simp + also have "\ \ ?da = (fps_const c * a) / ?x1" + apply (simp only: fps_divide_def mult_assoc[symmetric] inverse_mult_eq_1[OF x10]) + by (simp add: ring_simps) + finally have eq: "?l = ?r \ ?lhs" by simp + moreover + {assume h: "?l = ?r" + {fix n + from h have lrn: "?l $ n = ?r$n" by simp + + from lrn + have "a$ Suc n = ((c - of_nat n) / of_nat (Suc n)) * a $n" + apply (simp add: ring_simps del: of_nat_Suc) + by (cases n, simp_all add: field_simps del: of_nat_Suc) + } + note th0 = this + {fix n have "a$n = (c gchoose n) * a$0" + proof(induct n) + case 0 thus ?case by simp + next + case (Suc m) + thus ?case unfolding th0 + apply (simp add: field_simps del: of_nat_Suc) + unfolding mult_assoc[symmetric] gbinomial_mult_1 + by (simp add: ring_simps) + qed} + note th1 = this + have ?rhs + apply (simp add: fps_eq_iff) + apply (subst th1) + by (simp add: ring_simps)} + moreover + {assume h: ?rhs + have th00:"\x y. x * (a$0 * y) = a$0 * (x*y)" by (simp add: mult_commute) + have "?l = ?r" + apply (subst h) + apply (subst (2) h) + apply (clarsimp simp add: fps_eq_iff ring_simps) + unfolding mult_assoc[symmetric] th00 gbinomial_mult_1 + by (simp add: ring_simps gbinomial_mult_1)} + ultimately show ?thesis by blast +qed + +lemma fps_binomial_deriv: "fps_deriv (fps_binomial c) = fps_const c * fps_binomial c / (1 + X)" +proof- + let ?a = "fps_binomial c" + have th0: "?a = fps_const (?a$0) * ?a" by (simp) + from iffD2[OF fps_binomial_ODE_unique, OF th0] show ?thesis . +qed + +lemma fps_binomial_add_mult: "fps_binomial (c+d) = fps_binomial c * fps_binomial d" (is "?l = ?r") +proof- + let ?P = "?r - ?l" + let ?b = "fps_binomial" + let ?db = "\x. fps_deriv (?b x)" + have "fps_deriv ?P = ?db c * ?b d + ?b c * ?db d - ?db (c + d)" by simp + 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))" + unfolding fps_binomial_deriv + by (simp add: fps_divide_def ring_simps) + also have "\ = (fps_const (c + d)/ (1 + X)) * ?P" + by (simp add: ring_simps fps_divide_def fps_const_add[symmetric] del: fps_const_add) + finally have th0: "fps_deriv ?P = fps_const (c+d) * ?P / (1 + X)" + by (simp add: fps_divide_def) + have "?P = fps_const (?P$0) * ?b (c + d)" + unfolding fps_binomial_ODE_unique[symmetric] + using th0 by simp + hence "?P = 0" by (simp add: fps_mult_nth) + then show ?thesis by simp +qed + +lemma fps_minomial_minus_one: "fps_binomial (- 1) = inverse (1 + X)" + (is "?l = inverse ?r") +proof- + have th: "?r$0 \ 0" by simp + have th': "fps_deriv (inverse ?r) = fps_const (- 1) * inverse ?r / (1 + X)" + by (simp add: fps_inverse_deriv[OF th] fps_divide_def power2_eq_square mult_commute fps_const_neg[symmetric] del: fps_const_neg) + have eq: "inverse ?r $ 0 = 1" + by (simp add: fps_inverse_def) + from iffD1[OF fps_binomial_ODE_unique[of "inverse (1 + X)" "- 1"] th'] eq + show ?thesis by (simp add: fps_inverse_def) +qed + +text{* Vandermonde's Identity as a consequence *} +lemma gbinomial_Vandermond: "setsum (\k. (a gchoose k) * (b gchoose (n - k))) {0..n} = (a + b) gchoose n" +proof- + let ?ba = "fps_binomial a" + let ?bb = "fps_binomial b" + let ?bab = "fps_binomial (a + b)" + from fps_binomial_add_mult[of a b] have "?bab $ n = (?ba * ?bb)$n" by simp + then show ?thesis by (simp add: fps_mult_nth) +qed + +lemma binomial_Vandermond: "setsum (\k. (a choose k) * (b choose (n - k))) {0..n} = (a + b) choose n" + using gbinomial_Vandermond[of "(of_nat a)" "of_nat b" n] + + apply (simp only: binomial_gbinomial[symmetric] of_nat_mult[symmetric] of_nat_setsum[symmetric] of_nat_add[symmetric]) + by simp + +lemma binomial_symmetric: assumes kn: "k \ n" + shows "n choose k = n choose (n - k)" +proof- + from kn have kn': "n - k \ n" by arith + from binomial_fact_lemma[OF kn] binomial_fact_lemma[OF kn'] + have "fact k * fact (n - k) * (n choose k) = fact (n - k) * fact (n - (n - k)) * (n choose (n - k))" by simp + then show ?thesis using kn by simp +qed + +lemma binomial_Vandermond_same: "setsum (\k. (n choose k)^2) {0..n} = (2*n) choose n" + using binomial_Vandermond[of n n n,symmetric] + unfolding nat_mult_2 apply (simp add: power2_eq_square) + apply (rule setsum_cong2) + by (auto intro: binomial_symmetric) + + subsubsection{* Formal trigonometric functions *} definition "fps_sin (c::'a::field_char_0) = @@ -2869,4 +3023,71 @@ by simp qed +text {* Connection to E c over the complex numbers --- Euler and De Moivre*} +lemma Eii_sin_cos: + "E (ii * c) = fps_cos c + fps_const ii * fps_sin c " + (is "?l = ?r") +proof- + {fix n::nat + {assume en: "even n" + from en obtain m where m: "n = 2*m" + unfolding even_mult_two_ex by blast + + have "?l $n = ?r$n" + by (simp add: m fps_sin_def fps_cos_def power_mult_distrib + power_mult power_minus)} + moreover + {assume on: "odd n" + from on obtain m where m: "n = 2*m + 1" + unfolding odd_nat_equiv_def2 by (auto simp add: nat_mult_2) + have "?l $n = ?r$n" + by (simp add: m fps_sin_def fps_cos_def power_mult_distrib + power_mult power_minus)} + ultimately have "?l $n = ?r$n" by blast} + then show ?thesis by (simp add: fps_eq_iff) +qed + +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 add: fps_sin_even fps_cos_odd) + +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]) +apply (simp_all add: number_of_fps_def) +by (simp_all add: fps_const_add[symmetric] fps_const_minus[symmetric]) + +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_sin_even fps_cos_odd 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 \ * fps_sin c + fps_const \ * 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_sin_even fps_cos_odd fps_divide_def fps_const_inverse th) +qed + +lemma fps_tan_Eii: + "fps_tan c = (E (ii * c) - E (- ii * c)) / (fps_const ii * (E (ii * c) + E (- ii * c)))" + unfolding fps_tan_def fps_sin_Eii fps_cos_Eii mult_minus_left E_neg + apply (simp add: fps_divide_def fps_inverse_mult fps_const_mult[symmetric] fps_const_inverse del: fps_const_mult) + by simp + +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)" + unfolding Eii_sin_cos[symmetric] E_power_mult + by (simp add: mult_ac) + end diff -r 6ef7056e5215 -r adea7a729c7a src/HOL/ex/Formal_Power_Series_Examples.thy --- a/src/HOL/ex/Formal_Power_Series_Examples.thy Tue Jul 14 12:18:52 2009 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,303 +0,0 @@ -(* Title: Formal_Power_Series_Examples.thy - ID: - Author: Amine Chaieb, University of Cambridge -*) - -header{* Some applications of formal power series and some properties over complex numbers*} - -theory Formal_Power_Series_Examples - imports Formal_Power_Series Binomial -begin - -section{* The generalized binomial theorem *} -lemma gbinomial_theorem: - "((a::'a::{field_char_0, division_by_zero})+b) ^ n = (\k=0..n. of_nat (n choose k) * a^k * b^(n-k))" -proof- - from E_add_mult[of a b] - have "(E (a + b)) $ n = (E a * E b)$n" by simp - 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))))" - by (simp add: field_simps fps_mult_nth of_nat_mult[symmetric] setsum_right_distrib) - then show ?thesis - apply simp - apply (rule setsum_cong2) - apply simp - apply (frule binomial_fact[where ?'a = 'a, symmetric]) - by (simp add: field_simps of_nat_mult) -qed - -text{* And the nat-form -- also available from Binomial.thy *} -lemma binomial_theorem: "(a+b) ^ n = (\k=0..n. (n choose k) * a^k * b^(n-k))" - using gbinomial_theorem[of "of_nat a" "of_nat b" n] - unfolding of_nat_add[symmetric] of_nat_power[symmetric] of_nat_mult[symmetric] of_nat_setsum[symmetric] - by simp - -section {* The binomial series and Vandermonde's identity *} -definition "fps_binomial a = Abs_fps (\n. a gchoose n)" - -lemma fps_binomial_nth[simp]: "fps_binomial a $ n = a gchoose n" - by (simp add: fps_binomial_def) - -lemma fps_binomial_ODE_unique: - fixes c :: "'a::field_char_0" - shows "fps_deriv a = (fps_const c * a) / (1 + X) \ a = fps_const (a$0) * fps_binomial c" - (is "?lhs \ ?rhs") -proof- - let ?da = "fps_deriv a" - let ?x1 = "(1 + X):: 'a fps" - let ?l = "?x1 * ?da" - let ?r = "fps_const c * a" - have x10: "?x1 $ 0 \ 0" by simp - have "?l = ?r \ inverse ?x1 * ?l = inverse ?x1 * ?r" by simp - also have "\ \ ?da = (fps_const c * a) / ?x1" - apply (simp only: fps_divide_def mult_assoc[symmetric] inverse_mult_eq_1[OF x10]) - by (simp add: ring_simps) - finally have eq: "?l = ?r \ ?lhs" by simp - moreover - {assume h: "?l = ?r" - {fix n - from h have lrn: "?l $ n = ?r$n" by simp - - from lrn - have "a$ Suc n = ((c - of_nat n) / of_nat (Suc n)) * a $n" - apply (simp add: ring_simps del: of_nat_Suc) - by (cases n, simp_all add: field_simps del: of_nat_Suc) - } - note th0 = this - {fix n have "a$n = (c gchoose n) * a$0" - proof(induct n) - case 0 thus ?case by simp - next - case (Suc m) - thus ?case unfolding th0 - apply (simp add: field_simps del: of_nat_Suc) - unfolding mult_assoc[symmetric] gbinomial_mult_1 - by (simp add: ring_simps) - qed} - note th1 = this - have ?rhs - apply (simp add: fps_eq_iff) - apply (subst th1) - by (simp add: ring_simps)} - moreover - {assume h: ?rhs - have th00:"\x y. x * (a$0 * y) = a$0 * (x*y)" by (simp add: mult_commute) - have "?l = ?r" - apply (subst h) - apply (subst (2) h) - apply (clarsimp simp add: fps_eq_iff ring_simps) - unfolding mult_assoc[symmetric] th00 gbinomial_mult_1 - by (simp add: ring_simps gbinomial_mult_1)} - ultimately show ?thesis by blast -qed - -lemma fps_binomial_deriv: "fps_deriv (fps_binomial c) = fps_const c * fps_binomial c / (1 + X)" -proof- - let ?a = "fps_binomial c" - have th0: "?a = fps_const (?a$0) * ?a" by (simp) - from iffD2[OF fps_binomial_ODE_unique, OF th0] show ?thesis . -qed - -lemma fps_binomial_add_mult: "fps_binomial (c+d) = fps_binomial c * fps_binomial d" (is "?l = ?r") -proof- - let ?P = "?r - ?l" - let ?b = "fps_binomial" - let ?db = "\x. fps_deriv (?b x)" - have "fps_deriv ?P = ?db c * ?b d + ?b c * ?db d - ?db (c + d)" by simp - 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))" - unfolding fps_binomial_deriv - by (simp add: fps_divide_def ring_simps) - also have "\ = (fps_const (c + d)/ (1 + X)) * ?P" - by (simp add: ring_simps fps_divide_def fps_const_add[symmetric] del: fps_const_add) - finally have th0: "fps_deriv ?P = fps_const (c+d) * ?P / (1 + X)" - by (simp add: fps_divide_def) - have "?P = fps_const (?P$0) * ?b (c + d)" - unfolding fps_binomial_ODE_unique[symmetric] - using th0 by simp - hence "?P = 0" by (simp add: fps_mult_nth) - then show ?thesis by simp -qed - -lemma fps_minomial_minus_one: "fps_binomial (- 1) = inverse (1 + X)" - (is "?l = inverse ?r") -proof- - have th: "?r$0 \ 0" by simp - have th': "fps_deriv (inverse ?r) = fps_const (- 1) * inverse ?r / (1 + X)" - by (simp add: fps_inverse_deriv[OF th] fps_divide_def power2_eq_square mult_commute fps_const_neg[symmetric] del: fps_const_neg) - have eq: "inverse ?r $ 0 = 1" - by (simp add: fps_inverse_def) - from iffD1[OF fps_binomial_ODE_unique[of "inverse (1 + X)" "- 1"] th'] eq - show ?thesis by (simp add: fps_inverse_def) -qed - -lemma gbinomial_Vandermond: "setsum (\k. (a gchoose k) * (b gchoose (n - k))) {0..n} = (a + b) gchoose n" -proof- - let ?ba = "fps_binomial a" - let ?bb = "fps_binomial b" - let ?bab = "fps_binomial (a + b)" - from fps_binomial_add_mult[of a b] have "?bab $ n = (?ba * ?bb)$n" by simp - then show ?thesis by (simp add: fps_mult_nth) -qed - -lemma binomial_Vandermond: "setsum (\k. (a choose k) * (b choose (n - k))) {0..n} = (a + b) choose n" - using gbinomial_Vandermond[of "(of_nat a)" "of_nat b" n] - - apply (simp only: binomial_gbinomial[symmetric] of_nat_mult[symmetric] of_nat_setsum[symmetric] of_nat_add[symmetric]) - by simp - -lemma binomial_symmetric: assumes kn: "k \ n" - shows "n choose k = n choose (n - k)" -proof- - from kn have kn': "n - k \ n" by arith - from binomial_fact_lemma[OF kn] binomial_fact_lemma[OF kn'] - have "fact k * fact (n - k) * (n choose k) = fact (n - k) * fact (n - (n - k)) * (n choose (n - k))" by simp - then show ?thesis using kn by simp -qed - -lemma binomial_Vandermond_same: "setsum (\k. (n choose k)^2) {0..n} = (2*n) choose n" - using binomial_Vandermond[of n n n,symmetric] - unfolding nat_mult_2 apply (simp add: power2_eq_square) - apply (rule setsum_cong2) - by (auto intro: binomial_symmetric) - -section {* Relation between formal sine/cosine and the exponential FPS*} -lemma Eii_sin_cos: - "E (ii * c) = fps_cos c + fps_const ii * fps_sin c " - (is "?l = ?r") -proof- - {fix n::nat - {assume en: "even n" - from en obtain m where m: "n = 2*m" - unfolding even_mult_two_ex by blast - - have "?l $n = ?r$n" - by (simp add: m fps_sin_def fps_cos_def power_mult_distrib - power_mult power_minus)} - moreover - {assume on: "odd n" - from on obtain m where m: "n = 2*m + 1" - unfolding odd_nat_equiv_def2 by (auto simp add: nat_mult_2) - have "?l $n = ?r$n" - by (simp add: m fps_sin_def fps_cos_def power_mult_distrib - power_mult power_minus)} - ultimately have "?l $n = ?r$n" by blast} - then show ?thesis by (simp add: fps_eq_iff) -qed - -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 add: fps_sin_even fps_cos_odd) - -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]) -apply (simp_all add: number_of_fps_def) -by (simp_all add: fps_const_add[symmetric] fps_const_minus[symmetric]) - -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_sin_even fps_cos_odd 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 \ * fps_sin c + fps_const \ * 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_sin_even fps_cos_odd fps_divide_def fps_const_inverse th) -qed - -lemma fps_const_mult_2: "fps_const (2::'a::number_ring) * a = a +a" - by (simp add: fps_eq_iff fps_number_of_fps_const) - -lemma fps_const_mult_2_right: "a * fps_const (2::'a::number_ring) = a +a" - by (simp add: fps_eq_iff fps_number_of_fps_const) - -lemma fps_tan_Eii: - "fps_tan c = (E (ii * c) - E (- ii * c)) / (fps_const ii * (E (ii * c) + E (- ii * c)))" - unfolding fps_tan_def fps_sin_Eii fps_cos_Eii mult_minus_left E_neg - apply (simp add: fps_divide_def fps_inverse_mult fps_const_mult[symmetric] fps_const_inverse del: fps_const_mult) - by simp - -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)" - unfolding Eii_sin_cos[symmetric] E_power_mult - by (simp add: mult_ac) - -text{* Now some trigonometric identities *} - -lemma fps_sin_add: - "fps_sin (a+b) = fps_sin (a::complex) * fps_cos b + fps_cos a * fps_sin b" -proof- - let ?ca = "fps_cos a" - let ?cb = "fps_cos b" - let ?sa = "fps_sin a" - let ?sb = "fps_sin b" - let ?i = "fps_const ii" - have i: "?i*?i = fps_const -1" by simp - have "fps_sin (a + b) = - ((?ca + ?i * ?sa) * (?cb + ?i*?sb) - (?ca - ?i*?sa) * (?cb - ?i*?sb)) * - fps_const (- (\ / 2))" - apply(simp add: fps_sin_Eii[of "a+b"] fps_divide_def minus_mult_commute) - unfolding right_distrib - apply (simp add: Eii_sin_cos E_minus_ii_sin_cos fps_const_inverse E_add_mult) - by (simp add: ring_simps) - 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)" - by (simp add: ring_simps) - also have "\ = (fps_const 2 * ?i * (?ca * ?sb + ?sa * ?cb)) * fps_const (- ii/2)" - apply simp - apply (simp add: ring_simps) - apply (simp add: ring_simps add: fps_const_mult[symmetric] del:fps_const_mult) - unfolding fps_const_mult_2_right - by (simp add: ring_simps) - also have "\ = (fps_const 2 * ?i * fps_const (- ii/2)) * (?ca * ?sb + ?sa * ?cb)" - by (simp only: mult_ac) - also have "\ = ?sa * ?cb + ?ca*?sb" - by simp - finally show ?thesis . -qed - -lemma fps_cos_add: - "fps_cos (a+b) = fps_cos (a::complex) * fps_cos b - fps_sin a * fps_sin b" -proof- - let ?ca = "fps_cos a" - let ?cb = "fps_cos b" - let ?sa = "fps_sin a" - let ?sb = "fps_sin b" - let ?i = "fps_const ii" - have i: "?i*?i = fps_const -1" by simp - have i': "\x. ?i * (?i * x) = - x" - apply (simp add: mult_assoc[symmetric] i) - by (simp add: fps_eq_iff) - have m1: "\x. x * fps_const (-1 ::complex) = - x" "\x. fps_const (-1 :: complex) * x = - x" - by (auto simp add: fps_eq_iff) - - have "fps_cos (a + b) = - ((?ca + ?i * ?sa) * (?cb + ?i*?sb) + (?ca - ?i*?sa) * (?cb - ?i*?sb)) * - fps_const (1/ 2)" - apply(simp add: fps_cos_Eii[of "a+b"] fps_divide_def minus_mult_commute) - unfolding right_distrib minus_add_distrib - apply (simp add: Eii_sin_cos E_minus_ii_sin_cos fps_const_inverse E_add_mult) - by (simp add: ring_simps) - 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)" - apply simp - by (simp add: ring_simps i' m1) - also have "\ = (fps_const 2 * (?ca * ?cb - ?sa * ?sb)) * fps_const (1/2)" - apply simp - by (simp add: ring_simps m1 fps_const_mult_2_right) - also have "\ = (fps_const 2 * fps_const (1/2)) * (?ca * ?cb - ?sa * ?sb)" - by (simp only: mult_ac) - also have "\ = ?ca * ?cb - ?sa*?sb" - by simp - finally show ?thesis . -qed - -end