Moved important theorems from FPS_Examples to FPS --- they are not
authorchaieb
Wed Jul 15 06:14:25 2009 +0200 (2009-07-15)
changeset 32157adea7a729c7a
parent 32004 6ef7056e5215
child 32158 4dc119d4fc8b
Moved important theorems from FPS_Examples to FPS --- they are not
really examples but useful theorems that are being reproved since
unnoticed.
src/HOL/IsaMakefile
src/HOL/Library/Formal_Power_Series.thy
src/HOL/ex/Formal_Power_Series_Examples.thy
     1.1 --- a/src/HOL/IsaMakefile	Tue Jul 14 12:18:52 2009 +0200
     1.2 +++ b/src/HOL/IsaMakefile	Wed Jul 15 06:14:25 2009 +0200
     1.3 @@ -886,8 +886,7 @@
     1.4    ex/Codegenerator_Pretty_Test.thy ex/Coherent.thy				\
     1.5    ex/Commutative_RingEx.thy ex/Commutative_Ring_Complete.thy		\
     1.6    ex/Efficient_Nat_examples.thy		\
     1.7 -  ex/Eval_Examples.thy				\
     1.8 -  ex/Formal_Power_Series_Examples.thy ex/Fundefs.thy			\
     1.9 +  ex/Eval_Examples.thy	ex/Fundefs.thy			\
    1.10    ex/Groebner_Examples.thy ex/Guess.thy ex/HarmonicSeries.thy		\
    1.11    ex/Hebrew.thy ex/Hex_Bin_Examples.thy ex/Higher_Order_Logic.thy	\
    1.12    ex/Hilbert_Classical.thy			\
     2.1 --- a/src/HOL/Library/Formal_Power_Series.thy	Tue Jul 14 12:18:52 2009 +0200
     2.2 +++ b/src/HOL/Library/Formal_Power_Series.thy	Wed Jul 15 06:14:25 2009 +0200
     2.3 @@ -5,7 +5,7 @@
     2.4  header{* A formalization of formal power series *}
     2.5  
     2.6  theory Formal_Power_Series
     2.7 -imports Complex_Main
     2.8 +imports Complex_Main Binomial
     2.9  begin
    2.10  
    2.11  
    2.12 @@ -2625,6 +2625,29 @@
    2.13    apply (auto simp add: fps_eq_iff E_def fps_compose_def power_mult_distrib)
    2.14    by (simp add: cond_value_iff cond_application_beta setsum_delta' cong del: if_weak_cong)
    2.15  
    2.16 +text{* The generalized binomial theorem as a  consequence of @{thm E_add_mult} *}
    2.17 +
    2.18 +lemma gbinomial_theorem: 
    2.19 +  "((a::'a::{field_char_0, division_by_zero})+b) ^ n = (\<Sum>k=0..n. of_nat (n choose k) * a^k * b^(n-k))"
    2.20 +proof-
    2.21 +  from E_add_mult[of a b] 
    2.22 +  have "(E (a + b)) $ n = (E a * E b)$n" by simp
    2.23 +  then have "(a + b) ^ n = (\<Sum>i\<Colon>nat = 0\<Colon>nat..n. a ^ i * b ^ (n - i)  * (of_nat (fact n) / of_nat (fact i * fact (n - i))))"
    2.24 +    by (simp add: field_simps fps_mult_nth of_nat_mult[symmetric] setsum_right_distrib)
    2.25 +  then show ?thesis 
    2.26 +    apply simp
    2.27 +    apply (rule setsum_cong2)
    2.28 +    apply simp
    2.29 +    apply (frule binomial_fact[where ?'a = 'a, symmetric])
    2.30 +    by (simp add: field_simps of_nat_mult)
    2.31 +qed
    2.32 +
    2.33 +text{* And the nat-form -- also available from Binomial.thy *}
    2.34 +lemma binomial_theorem: "(a+b) ^ n = (\<Sum>k=0..n. (n choose k) * a^k * b^(n-k))"
    2.35 +  using gbinomial_theorem[of "of_nat a" "of_nat b" n]
    2.36 +  unfolding of_nat_add[symmetric] of_nat_power[symmetric] of_nat_mult[symmetric] of_nat_setsum[symmetric]
    2.37 +  by simp
    2.38 +
    2.39  subsubsection{* Logarithmic series *}
    2.40  
    2.41  lemma Abs_fps_if_0: 
    2.42 @@ -2679,6 +2702,137 @@
    2.43      unfolding fps_deriv_eq_iff by simp
    2.44  qed
    2.45  
    2.46 +subsubsection{* Binomial series *}
    2.47 +
    2.48 +definition "fps_binomial a = Abs_fps (\<lambda>n. a gchoose n)"
    2.49 +
    2.50 +lemma fps_binomial_nth[simp]: "fps_binomial a $ n = a gchoose n"
    2.51 +  by (simp add: fps_binomial_def)
    2.52 +
    2.53 +lemma fps_binomial_ODE_unique:
    2.54 +  fixes c :: "'a::field_char_0"
    2.55 +  shows "fps_deriv a = (fps_const c * a) / (1 + X) \<longleftrightarrow> a = fps_const (a$0) * fps_binomial c"
    2.56 +  (is "?lhs \<longleftrightarrow> ?rhs")
    2.57 +proof-
    2.58 +  let ?da = "fps_deriv a"
    2.59 +  let ?x1 = "(1 + X):: 'a fps"
    2.60 +  let ?l = "?x1 * ?da"
    2.61 +  let ?r = "fps_const c * a"
    2.62 +  have x10: "?x1 $ 0 \<noteq> 0" by simp
    2.63 +  have "?l = ?r \<longleftrightarrow> inverse ?x1 * ?l = inverse ?x1 * ?r" by simp
    2.64 +  also have "\<dots> \<longleftrightarrow> ?da = (fps_const c * a) / ?x1"
    2.65 +    apply (simp only: fps_divide_def  mult_assoc[symmetric] inverse_mult_eq_1[OF x10])
    2.66 +    by (simp add: ring_simps)
    2.67 +  finally have eq: "?l = ?r \<longleftrightarrow> ?lhs" by simp
    2.68 +  moreover
    2.69 +  {assume h: "?l = ?r" 
    2.70 +    {fix n
    2.71 +      from h have lrn: "?l $ n = ?r$n" by simp
    2.72 +      
    2.73 +      from lrn 
    2.74 +      have "a$ Suc n = ((c - of_nat n) / of_nat (Suc n)) * a $n" 
    2.75 +	apply (simp add: ring_simps del: of_nat_Suc)
    2.76 +	by (cases n, simp_all add: field_simps del: of_nat_Suc)
    2.77 +    }
    2.78 +    note th0 = this
    2.79 +    {fix n have "a$n = (c gchoose n) * a$0"
    2.80 +      proof(induct n)
    2.81 +	case 0 thus ?case by simp
    2.82 +      next
    2.83 +	case (Suc m)
    2.84 +	thus ?case unfolding th0
    2.85 +	  apply (simp add: field_simps del: of_nat_Suc)
    2.86 +	  unfolding mult_assoc[symmetric] gbinomial_mult_1
    2.87 +	  by (simp add: ring_simps)
    2.88 +      qed}
    2.89 +    note th1 = this
    2.90 +    have ?rhs
    2.91 +      apply (simp add: fps_eq_iff)
    2.92 +      apply (subst th1)
    2.93 +      by (simp add: ring_simps)}
    2.94 +  moreover
    2.95 +  {assume h: ?rhs
    2.96 +  have th00:"\<And>x y. x * (a$0 * y) = a$0 * (x*y)" by (simp add: mult_commute)
    2.97 +    have "?l = ?r" 
    2.98 +      apply (subst h)
    2.99 +      apply (subst (2) h)
   2.100 +      apply (clarsimp simp add: fps_eq_iff ring_simps)
   2.101 +      unfolding mult_assoc[symmetric] th00 gbinomial_mult_1
   2.102 +      by (simp add: ring_simps gbinomial_mult_1)}
   2.103 +  ultimately show ?thesis by blast
   2.104 +qed
   2.105 +
   2.106 +lemma fps_binomial_deriv: "fps_deriv (fps_binomial c) = fps_const c * fps_binomial c / (1 + X)"
   2.107 +proof-
   2.108 +  let ?a = "fps_binomial c"
   2.109 +  have th0: "?a = fps_const (?a$0) * ?a" by (simp)
   2.110 +  from iffD2[OF fps_binomial_ODE_unique, OF th0] show ?thesis .
   2.111 +qed
   2.112 +
   2.113 +lemma fps_binomial_add_mult: "fps_binomial (c+d) = fps_binomial c * fps_binomial d" (is "?l = ?r")
   2.114 +proof-
   2.115 +  let ?P = "?r - ?l"
   2.116 +  let ?b = "fps_binomial"
   2.117 +  let ?db = "\<lambda>x. fps_deriv (?b x)"
   2.118 +  have "fps_deriv ?P = ?db c * ?b d + ?b c * ?db d - ?db (c + d)"  by simp
   2.119 +  also have "\<dots> = inverse (1 + X) * (fps_const c * ?b c * ?b d + fps_const d * ?b c * ?b d - fps_const (c+d) * ?b (c + d))"
   2.120 +    unfolding fps_binomial_deriv
   2.121 +    by (simp add: fps_divide_def ring_simps)
   2.122 +  also have "\<dots> = (fps_const (c + d)/ (1 + X)) * ?P"
   2.123 +    by (simp add: ring_simps fps_divide_def fps_const_add[symmetric] del: fps_const_add)
   2.124 +  finally have th0: "fps_deriv ?P = fps_const (c+d) * ?P / (1 + X)"
   2.125 +    by (simp add: fps_divide_def)
   2.126 +  have "?P = fps_const (?P$0) * ?b (c + d)"
   2.127 +    unfolding fps_binomial_ODE_unique[symmetric]
   2.128 +    using th0 by simp
   2.129 +  hence "?P = 0" by (simp add: fps_mult_nth)
   2.130 +  then show ?thesis by simp
   2.131 +qed
   2.132 +
   2.133 +lemma fps_minomial_minus_one: "fps_binomial (- 1) = inverse (1 + X)"
   2.134 +  (is "?l = inverse ?r")
   2.135 +proof-
   2.136 +  have th: "?r$0 \<noteq> 0" by simp
   2.137 +  have th': "fps_deriv (inverse ?r) = fps_const (- 1) * inverse ?r / (1 + X)"
   2.138 +    by (simp add: fps_inverse_deriv[OF th] fps_divide_def power2_eq_square mult_commute fps_const_neg[symmetric] del: fps_const_neg)
   2.139 +  have eq: "inverse ?r $ 0 = 1"
   2.140 +    by (simp add: fps_inverse_def)
   2.141 +  from iffD1[OF fps_binomial_ODE_unique[of "inverse (1 + X)" "- 1"] th'] eq
   2.142 +  show ?thesis by (simp add: fps_inverse_def)
   2.143 +qed
   2.144 +
   2.145 +text{* Vandermonde's Identity as a consequence *}
   2.146 +lemma gbinomial_Vandermond: "setsum (\<lambda>k. (a gchoose k) * (b gchoose (n - k))) {0..n} = (a + b) gchoose n"
   2.147 +proof-
   2.148 +  let ?ba = "fps_binomial a"
   2.149 +  let ?bb = "fps_binomial b"
   2.150 +  let ?bab = "fps_binomial (a + b)"
   2.151 +  from fps_binomial_add_mult[of a b] have "?bab $ n = (?ba * ?bb)$n" by simp
   2.152 +  then show ?thesis by (simp add: fps_mult_nth)
   2.153 +qed
   2.154 +
   2.155 +lemma binomial_Vandermond: "setsum (\<lambda>k. (a choose k) * (b choose (n - k))) {0..n} = (a + b) choose n"
   2.156 +  using gbinomial_Vandermond[of "(of_nat a)" "of_nat b" n]
   2.157 +  
   2.158 +  apply (simp only: binomial_gbinomial[symmetric] of_nat_mult[symmetric] of_nat_setsum[symmetric] of_nat_add[symmetric])
   2.159 +  by simp
   2.160 +
   2.161 +lemma binomial_symmetric: assumes kn: "k \<le> n" 
   2.162 +  shows "n choose k = n choose (n - k)"
   2.163 +proof-
   2.164 +  from kn have kn': "n - k \<le> n" by arith
   2.165 +  from binomial_fact_lemma[OF kn] binomial_fact_lemma[OF kn']
   2.166 +  have "fact k * fact (n - k) * (n choose k) = fact (n - k) * fact (n - (n - k)) * (n choose (n - k))" by simp
   2.167 +  then show ?thesis using kn by simp
   2.168 +qed
   2.169 +  
   2.170 +lemma binomial_Vandermond_same: "setsum (\<lambda>k. (n choose k)^2) {0..n} = (2*n) choose n"
   2.171 +  using binomial_Vandermond[of n n n,symmetric]
   2.172 +  unfolding nat_mult_2 apply (simp add: power2_eq_square)
   2.173 +  apply (rule setsum_cong2)
   2.174 +  by (auto intro:  binomial_symmetric)
   2.175 +
   2.176 +
   2.177  subsubsection{* Formal trigonometric functions  *}
   2.178  
   2.179  definition "fps_sin (c::'a::field_char_0) =
   2.180 @@ -2869,4 +3023,71 @@
   2.181      by simp
   2.182  qed
   2.183  
   2.184 +text {* Connection to E c over the complex numbers --- Euler and De Moivre*}
   2.185 +lemma Eii_sin_cos:
   2.186 +  "E (ii * c) = fps_cos c + fps_const ii * fps_sin c "
   2.187 +  (is "?l = ?r")
   2.188 +proof-
   2.189 +  {fix n::nat
   2.190 +    {assume en: "even n"
   2.191 +      from en obtain m where m: "n = 2*m" 
   2.192 +	unfolding even_mult_two_ex by blast
   2.193 +      
   2.194 +      have "?l $n = ?r$n" 
   2.195 +	by (simp add: m fps_sin_def fps_cos_def power_mult_distrib
   2.196 +	  power_mult power_minus)}
   2.197 +    moreover
   2.198 +    {assume on: "odd n"
   2.199 +      from on obtain m where m: "n = 2*m + 1" 
   2.200 +	unfolding odd_nat_equiv_def2 by (auto simp add: nat_mult_2)  
   2.201 +      have "?l $n = ?r$n" 
   2.202 +	by (simp add: m fps_sin_def fps_cos_def power_mult_distrib
   2.203 +	  power_mult power_minus)}
   2.204 +    ultimately have "?l $n = ?r$n"  by blast}
   2.205 +  then show ?thesis by (simp add: fps_eq_iff)
   2.206 +qed
   2.207 +
   2.208 +lemma E_minus_ii_sin_cos: "E (- (ii * c)) = fps_cos c - fps_const ii * fps_sin c "
   2.209 +  unfolding minus_mult_right Eii_sin_cos by (simp add: fps_sin_even fps_cos_odd)
   2.210 +
   2.211 +lemma fps_const_minus: "fps_const (c::'a::group_add) - fps_const d = fps_const (c - d)"
   2.212 +  by (simp add: fps_eq_iff fps_const_def)
   2.213 +
   2.214 +lemma fps_number_of_fps_const: "number_of i = fps_const (number_of i :: 'a:: {comm_ring_1, number_ring})"
   2.215 +  apply (subst (2) number_of_eq)
   2.216 +apply(rule int_induct[of _ 0])
   2.217 +apply (simp_all add: number_of_fps_def)
   2.218 +by (simp_all add: fps_const_add[symmetric] fps_const_minus[symmetric])
   2.219 +
   2.220 +lemma fps_cos_Eii:
   2.221 +  "fps_cos c = (E (ii * c) + E (- ii * c)) / fps_const 2"
   2.222 +proof-
   2.223 +  have th: "fps_cos c + fps_cos c = fps_cos c * fps_const 2" 
   2.224 +    by (simp add: fps_eq_iff fps_number_of_fps_const complex_number_of_def[symmetric])
   2.225 +  show ?thesis
   2.226 +  unfolding Eii_sin_cos minus_mult_commute
   2.227 +  by (simp add: fps_sin_even fps_cos_odd fps_number_of_fps_const
   2.228 +    fps_divide_def fps_const_inverse th complex_number_of_def[symmetric])
   2.229 +qed
   2.230 +
   2.231 +lemma fps_sin_Eii:
   2.232 +  "fps_sin c = (E (ii * c) - E (- ii * c)) / fps_const (2*ii)"
   2.233 +proof-
   2.234 +  have th: "fps_const \<i> * fps_sin c + fps_const \<i> * fps_sin c = fps_sin c * fps_const (2 * ii)" 
   2.235 +    by (simp add: fps_eq_iff fps_number_of_fps_const complex_number_of_def[symmetric])
   2.236 +  show ?thesis
   2.237 +  unfolding Eii_sin_cos minus_mult_commute
   2.238 +  by (simp add: fps_sin_even fps_cos_odd fps_divide_def fps_const_inverse th)
   2.239 +qed
   2.240 +
   2.241 +lemma fps_tan_Eii:
   2.242 +  "fps_tan c = (E (ii * c) - E (- ii * c)) / (fps_const ii * (E (ii * c) + E (- ii * c)))"
   2.243 +  unfolding fps_tan_def fps_sin_Eii fps_cos_Eii mult_minus_left E_neg
   2.244 +  apply (simp add: fps_divide_def fps_inverse_mult fps_const_mult[symmetric] fps_const_inverse del: fps_const_mult)
   2.245 +  by simp
   2.246 +
   2.247 +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)"
   2.248 +  unfolding Eii_sin_cos[symmetric] E_power_mult
   2.249 +  by (simp add: mult_ac)
   2.250 +
   2.251  end
     3.1 --- a/src/HOL/ex/Formal_Power_Series_Examples.thy	Tue Jul 14 12:18:52 2009 +0200
     3.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.3 @@ -1,303 +0,0 @@
     3.4 -(*  Title:      Formal_Power_Series_Examples.thy
     3.5 -    ID:         
     3.6 -    Author:     Amine Chaieb, University of Cambridge
     3.7 -*)
     3.8 -
     3.9 -header{* Some applications of formal power series and some properties over complex numbers*}
    3.10 -
    3.11 -theory Formal_Power_Series_Examples
    3.12 -  imports Formal_Power_Series Binomial 
    3.13 -begin
    3.14 -
    3.15 -section{* The generalized binomial theorem *}
    3.16 -lemma gbinomial_theorem: 
    3.17 -  "((a::'a::{field_char_0, division_by_zero})+b) ^ n = (\<Sum>k=0..n. of_nat (n choose k) * a^k * b^(n-k))"
    3.18 -proof-
    3.19 -  from E_add_mult[of a b] 
    3.20 -  have "(E (a + b)) $ n = (E a * E b)$n" by simp
    3.21 -  then have "(a + b) ^ n = (\<Sum>i\<Colon>nat = 0\<Colon>nat..n. a ^ i * b ^ (n - i)  * (of_nat (fact n) / of_nat (fact i * fact (n - i))))"
    3.22 -    by (simp add: field_simps fps_mult_nth of_nat_mult[symmetric] setsum_right_distrib)
    3.23 -  then show ?thesis 
    3.24 -    apply simp
    3.25 -    apply (rule setsum_cong2)
    3.26 -    apply simp
    3.27 -    apply (frule binomial_fact[where ?'a = 'a, symmetric])
    3.28 -    by (simp add: field_simps of_nat_mult)
    3.29 -qed
    3.30 -
    3.31 -text{* And the nat-form -- also available from Binomial.thy *}
    3.32 -lemma binomial_theorem: "(a+b) ^ n = (\<Sum>k=0..n. (n choose k) * a^k * b^(n-k))"
    3.33 -  using gbinomial_theorem[of "of_nat a" "of_nat b" n]
    3.34 -  unfolding of_nat_add[symmetric] of_nat_power[symmetric] of_nat_mult[symmetric] of_nat_setsum[symmetric]
    3.35 -  by simp
    3.36 -
    3.37 -section {* The binomial series and Vandermonde's identity *}
    3.38 -definition "fps_binomial a = Abs_fps (\<lambda>n. a gchoose n)"
    3.39 -
    3.40 -lemma fps_binomial_nth[simp]: "fps_binomial a $ n = a gchoose n"
    3.41 -  by (simp add: fps_binomial_def)
    3.42 -
    3.43 -lemma fps_binomial_ODE_unique:
    3.44 -  fixes c :: "'a::field_char_0"
    3.45 -  shows "fps_deriv a = (fps_const c * a) / (1 + X) \<longleftrightarrow> a = fps_const (a$0) * fps_binomial c"
    3.46 -  (is "?lhs \<longleftrightarrow> ?rhs")
    3.47 -proof-
    3.48 -  let ?da = "fps_deriv a"
    3.49 -  let ?x1 = "(1 + X):: 'a fps"
    3.50 -  let ?l = "?x1 * ?da"
    3.51 -  let ?r = "fps_const c * a"
    3.52 -  have x10: "?x1 $ 0 \<noteq> 0" by simp
    3.53 -  have "?l = ?r \<longleftrightarrow> inverse ?x1 * ?l = inverse ?x1 * ?r" by simp
    3.54 -  also have "\<dots> \<longleftrightarrow> ?da = (fps_const c * a) / ?x1"
    3.55 -    apply (simp only: fps_divide_def  mult_assoc[symmetric] inverse_mult_eq_1[OF x10])
    3.56 -    by (simp add: ring_simps)
    3.57 -  finally have eq: "?l = ?r \<longleftrightarrow> ?lhs" by simp
    3.58 -  moreover
    3.59 -  {assume h: "?l = ?r" 
    3.60 -    {fix n
    3.61 -      from h have lrn: "?l $ n = ?r$n" by simp
    3.62 -      
    3.63 -      from lrn 
    3.64 -      have "a$ Suc n = ((c - of_nat n) / of_nat (Suc n)) * a $n" 
    3.65 -	apply (simp add: ring_simps del: of_nat_Suc)
    3.66 -	by (cases n, simp_all add: field_simps del: of_nat_Suc)
    3.67 -    }
    3.68 -    note th0 = this
    3.69 -    {fix n have "a$n = (c gchoose n) * a$0"
    3.70 -      proof(induct n)
    3.71 -	case 0 thus ?case by simp
    3.72 -      next
    3.73 -	case (Suc m)
    3.74 -	thus ?case unfolding th0
    3.75 -	  apply (simp add: field_simps del: of_nat_Suc)
    3.76 -	  unfolding mult_assoc[symmetric] gbinomial_mult_1
    3.77 -	  by (simp add: ring_simps)
    3.78 -      qed}
    3.79 -    note th1 = this
    3.80 -    have ?rhs
    3.81 -      apply (simp add: fps_eq_iff)
    3.82 -      apply (subst th1)
    3.83 -      by (simp add: ring_simps)}
    3.84 -  moreover
    3.85 -  {assume h: ?rhs
    3.86 -  have th00:"\<And>x y. x * (a$0 * y) = a$0 * (x*y)" by (simp add: mult_commute)
    3.87 -    have "?l = ?r" 
    3.88 -      apply (subst h)
    3.89 -      apply (subst (2) h)
    3.90 -      apply (clarsimp simp add: fps_eq_iff ring_simps)
    3.91 -      unfolding mult_assoc[symmetric] th00 gbinomial_mult_1
    3.92 -      by (simp add: ring_simps gbinomial_mult_1)}
    3.93 -  ultimately show ?thesis by blast
    3.94 -qed
    3.95 -
    3.96 -lemma fps_binomial_deriv: "fps_deriv (fps_binomial c) = fps_const c * fps_binomial c / (1 + X)"
    3.97 -proof-
    3.98 -  let ?a = "fps_binomial c"
    3.99 -  have th0: "?a = fps_const (?a$0) * ?a" by (simp)
   3.100 -  from iffD2[OF fps_binomial_ODE_unique, OF th0] show ?thesis .
   3.101 -qed
   3.102 -
   3.103 -lemma fps_binomial_add_mult: "fps_binomial (c+d) = fps_binomial c * fps_binomial d" (is "?l = ?r")
   3.104 -proof-
   3.105 -  let ?P = "?r - ?l"
   3.106 -  let ?b = "fps_binomial"
   3.107 -  let ?db = "\<lambda>x. fps_deriv (?b x)"
   3.108 -  have "fps_deriv ?P = ?db c * ?b d + ?b c * ?db d - ?db (c + d)"  by simp
   3.109 -  also have "\<dots> = inverse (1 + X) * (fps_const c * ?b c * ?b d + fps_const d * ?b c * ?b d - fps_const (c+d) * ?b (c + d))"
   3.110 -    unfolding fps_binomial_deriv
   3.111 -    by (simp add: fps_divide_def ring_simps)
   3.112 -  also have "\<dots> = (fps_const (c + d)/ (1 + X)) * ?P"
   3.113 -    by (simp add: ring_simps fps_divide_def fps_const_add[symmetric] del: fps_const_add)
   3.114 -  finally have th0: "fps_deriv ?P = fps_const (c+d) * ?P / (1 + X)"
   3.115 -    by (simp add: fps_divide_def)
   3.116 -  have "?P = fps_const (?P$0) * ?b (c + d)"
   3.117 -    unfolding fps_binomial_ODE_unique[symmetric]
   3.118 -    using th0 by simp
   3.119 -  hence "?P = 0" by (simp add: fps_mult_nth)
   3.120 -  then show ?thesis by simp
   3.121 -qed
   3.122 -
   3.123 -lemma fps_minomial_minus_one: "fps_binomial (- 1) = inverse (1 + X)"
   3.124 -  (is "?l = inverse ?r")
   3.125 -proof-
   3.126 -  have th: "?r$0 \<noteq> 0" by simp
   3.127 -  have th': "fps_deriv (inverse ?r) = fps_const (- 1) * inverse ?r / (1 + X)"
   3.128 -    by (simp add: fps_inverse_deriv[OF th] fps_divide_def power2_eq_square mult_commute fps_const_neg[symmetric] del: fps_const_neg)
   3.129 -  have eq: "inverse ?r $ 0 = 1"
   3.130 -    by (simp add: fps_inverse_def)
   3.131 -  from iffD1[OF fps_binomial_ODE_unique[of "inverse (1 + X)" "- 1"] th'] eq
   3.132 -  show ?thesis by (simp add: fps_inverse_def)
   3.133 -qed
   3.134 -
   3.135 -lemma gbinomial_Vandermond: "setsum (\<lambda>k. (a gchoose k) * (b gchoose (n - k))) {0..n} = (a + b) gchoose n"
   3.136 -proof-
   3.137 -  let ?ba = "fps_binomial a"
   3.138 -  let ?bb = "fps_binomial b"
   3.139 -  let ?bab = "fps_binomial (a + b)"
   3.140 -  from fps_binomial_add_mult[of a b] have "?bab $ n = (?ba * ?bb)$n" by simp
   3.141 -  then show ?thesis by (simp add: fps_mult_nth)
   3.142 -qed
   3.143 -
   3.144 -lemma binomial_Vandermond: "setsum (\<lambda>k. (a choose k) * (b choose (n - k))) {0..n} = (a + b) choose n"
   3.145 -  using gbinomial_Vandermond[of "(of_nat a)" "of_nat b" n]
   3.146 -  
   3.147 -  apply (simp only: binomial_gbinomial[symmetric] of_nat_mult[symmetric] of_nat_setsum[symmetric] of_nat_add[symmetric])
   3.148 -  by simp
   3.149 -
   3.150 -lemma binomial_symmetric: assumes kn: "k \<le> n" 
   3.151 -  shows "n choose k = n choose (n - k)"
   3.152 -proof-
   3.153 -  from kn have kn': "n - k \<le> n" by arith
   3.154 -  from binomial_fact_lemma[OF kn] binomial_fact_lemma[OF kn']
   3.155 -  have "fact k * fact (n - k) * (n choose k) = fact (n - k) * fact (n - (n - k)) * (n choose (n - k))" by simp
   3.156 -  then show ?thesis using kn by simp
   3.157 -qed
   3.158 -  
   3.159 -lemma binomial_Vandermond_same: "setsum (\<lambda>k. (n choose k)^2) {0..n} = (2*n) choose n"
   3.160 -  using binomial_Vandermond[of n n n,symmetric]
   3.161 -  unfolding nat_mult_2 apply (simp add: power2_eq_square)
   3.162 -  apply (rule setsum_cong2)
   3.163 -  by (auto intro:  binomial_symmetric)
   3.164 -
   3.165 -section {* Relation between formal sine/cosine and the exponential FPS*}
   3.166 -lemma Eii_sin_cos:
   3.167 -  "E (ii * c) = fps_cos c + fps_const ii * fps_sin c "
   3.168 -  (is "?l = ?r")
   3.169 -proof-
   3.170 -  {fix n::nat
   3.171 -    {assume en: "even n"
   3.172 -      from en obtain m where m: "n = 2*m" 
   3.173 -	unfolding even_mult_two_ex by blast
   3.174 -      
   3.175 -      have "?l $n = ?r$n" 
   3.176 -	by (simp add: m fps_sin_def fps_cos_def power_mult_distrib
   3.177 -	  power_mult power_minus)}
   3.178 -    moreover
   3.179 -    {assume on: "odd n"
   3.180 -      from on obtain m where m: "n = 2*m + 1" 
   3.181 -	unfolding odd_nat_equiv_def2 by (auto simp add: nat_mult_2)  
   3.182 -      have "?l $n = ?r$n" 
   3.183 -	by (simp add: m fps_sin_def fps_cos_def power_mult_distrib
   3.184 -	  power_mult power_minus)}
   3.185 -    ultimately have "?l $n = ?r$n"  by blast}
   3.186 -  then show ?thesis by (simp add: fps_eq_iff)
   3.187 -qed
   3.188 -
   3.189 -lemma E_minus_ii_sin_cos: "E (- (ii * c)) = fps_cos c - fps_const ii * fps_sin c "
   3.190 -  unfolding minus_mult_right Eii_sin_cos by (simp add: fps_sin_even fps_cos_odd)
   3.191 -
   3.192 -lemma fps_const_minus: "fps_const (c::'a::group_add) - fps_const d = fps_const (c - d)"
   3.193 -  by (simp add: fps_eq_iff fps_const_def)
   3.194 -
   3.195 -lemma fps_number_of_fps_const: "number_of i = fps_const (number_of i :: 'a:: {comm_ring_1, number_ring})"
   3.196 -  apply (subst (2) number_of_eq)
   3.197 -apply(rule int_induct[of _ 0])
   3.198 -apply (simp_all add: number_of_fps_def)
   3.199 -by (simp_all add: fps_const_add[symmetric] fps_const_minus[symmetric])
   3.200 -
   3.201 -lemma fps_cos_Eii:
   3.202 -  "fps_cos c = (E (ii * c) + E (- ii * c)) / fps_const 2"
   3.203 -proof-
   3.204 -  have th: "fps_cos c + fps_cos c = fps_cos c * fps_const 2" 
   3.205 -    by (simp add: fps_eq_iff fps_number_of_fps_const complex_number_of_def[symmetric])
   3.206 -  show ?thesis
   3.207 -  unfolding Eii_sin_cos minus_mult_commute
   3.208 -  by (simp add: fps_sin_even fps_cos_odd fps_number_of_fps_const
   3.209 -    fps_divide_def fps_const_inverse th complex_number_of_def[symmetric])
   3.210 -qed
   3.211 -
   3.212 -lemma fps_sin_Eii:
   3.213 -  "fps_sin c = (E (ii * c) - E (- ii * c)) / fps_const (2*ii)"
   3.214 -proof-
   3.215 -  have th: "fps_const \<i> * fps_sin c + fps_const \<i> * fps_sin c = fps_sin c * fps_const (2 * ii)" 
   3.216 -    by (simp add: fps_eq_iff fps_number_of_fps_const complex_number_of_def[symmetric])
   3.217 -  show ?thesis
   3.218 -  unfolding Eii_sin_cos minus_mult_commute
   3.219 -  by (simp add: fps_sin_even fps_cos_odd fps_divide_def fps_const_inverse th)
   3.220 -qed
   3.221 -
   3.222 -lemma fps_const_mult_2: "fps_const (2::'a::number_ring) * a = a +a"
   3.223 -  by (simp add: fps_eq_iff fps_number_of_fps_const)
   3.224 -
   3.225 -lemma fps_const_mult_2_right: "a * fps_const (2::'a::number_ring) = a +a"
   3.226 -  by (simp add: fps_eq_iff fps_number_of_fps_const)
   3.227 -
   3.228 -lemma fps_tan_Eii:
   3.229 -  "fps_tan c = (E (ii * c) - E (- ii * c)) / (fps_const ii * (E (ii * c) + E (- ii * c)))"
   3.230 -  unfolding fps_tan_def fps_sin_Eii fps_cos_Eii mult_minus_left E_neg
   3.231 -  apply (simp add: fps_divide_def fps_inverse_mult fps_const_mult[symmetric] fps_const_inverse del: fps_const_mult)
   3.232 -  by simp
   3.233 -
   3.234 -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)"
   3.235 -  unfolding Eii_sin_cos[symmetric] E_power_mult
   3.236 -  by (simp add: mult_ac)
   3.237 -
   3.238 -text{* Now some trigonometric identities *}
   3.239 -
   3.240 -lemma fps_sin_add: 
   3.241 -  "fps_sin (a+b) = fps_sin (a::complex) * fps_cos b + fps_cos a * fps_sin b"
   3.242 -proof-
   3.243 -  let ?ca = "fps_cos a"
   3.244 -  let ?cb = "fps_cos b"
   3.245 -  let ?sa = "fps_sin a"
   3.246 -  let ?sb = "fps_sin b"
   3.247 -  let ?i = "fps_const ii"
   3.248 -  have i: "?i*?i = fps_const -1" by simp
   3.249 -  have "fps_sin (a + b) = 
   3.250 -    ((?ca + ?i * ?sa) * (?cb + ?i*?sb) - (?ca - ?i*?sa) * (?cb - ?i*?sb)) *
   3.251 -    fps_const (- (\<i> / 2))"
   3.252 -    apply(simp add: fps_sin_Eii[of "a+b"] fps_divide_def minus_mult_commute)
   3.253 -    unfolding right_distrib
   3.254 -    apply (simp add: Eii_sin_cos E_minus_ii_sin_cos fps_const_inverse E_add_mult)
   3.255 -    by (simp add: ring_simps)
   3.256 -  also have "\<dots> = (?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)"
   3.257 -    by (simp add: ring_simps)
   3.258 -  also have "\<dots> = (fps_const 2 * ?i * (?ca * ?sb + ?sa * ?cb)) * fps_const (- ii/2)"
   3.259 -    apply simp
   3.260 -  apply (simp add: ring_simps)
   3.261 -    apply (simp add:  ring_simps add: fps_const_mult[symmetric] del:fps_const_mult)
   3.262 -    unfolding fps_const_mult_2_right
   3.263 -    by (simp add: ring_simps)
   3.264 -  also have "\<dots> = (fps_const 2 * ?i * fps_const (- ii/2)) * (?ca * ?sb + ?sa * ?cb)"
   3.265 -    by (simp only: mult_ac)
   3.266 -  also have "\<dots> = ?sa * ?cb + ?ca*?sb"
   3.267 -    by simp
   3.268 -  finally show ?thesis .
   3.269 -qed
   3.270 -
   3.271 -lemma fps_cos_add: 
   3.272 -  "fps_cos (a+b) = fps_cos (a::complex) * fps_cos b - fps_sin a * fps_sin b"
   3.273 -proof-
   3.274 -  let ?ca = "fps_cos a"
   3.275 -  let ?cb = "fps_cos b"
   3.276 -  let ?sa = "fps_sin a"
   3.277 -  let ?sb = "fps_sin b"
   3.278 -  let ?i = "fps_const ii"
   3.279 -  have i: "?i*?i = fps_const -1" by simp
   3.280 -  have i': "\<And>x. ?i * (?i * x) = - x" 
   3.281 -    apply (simp add: mult_assoc[symmetric] i)
   3.282 -    by (simp add: fps_eq_iff)
   3.283 -  have m1: "\<And>x. x * fps_const (-1 ::complex) = - x" "\<And>x. fps_const (-1 :: complex) * x = - x"
   3.284 -    by (auto simp add: fps_eq_iff)
   3.285 -
   3.286 -  have "fps_cos (a + b) = 
   3.287 -    ((?ca + ?i * ?sa) * (?cb + ?i*?sb) + (?ca - ?i*?sa) * (?cb - ?i*?sb)) *
   3.288 -    fps_const (1/ 2)"
   3.289 -    apply(simp add: fps_cos_Eii[of "a+b"] fps_divide_def minus_mult_commute)
   3.290 -    unfolding right_distrib minus_add_distrib
   3.291 -    apply (simp add: Eii_sin_cos E_minus_ii_sin_cos fps_const_inverse E_add_mult)
   3.292 -    by (simp add: ring_simps)
   3.293 -  also have "\<dots> = (?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)"
   3.294 -    apply simp
   3.295 -    by (simp add: ring_simps i' m1)
   3.296 -  also have "\<dots> = (fps_const 2 * (?ca * ?cb - ?sa * ?sb)) * fps_const (1/2)"
   3.297 -    apply simp
   3.298 -    by (simp add: ring_simps m1 fps_const_mult_2_right)
   3.299 -  also have "\<dots> = (fps_const 2 * fps_const (1/2)) * (?ca * ?cb - ?sa * ?sb)"
   3.300 -    by (simp only: mult_ac)
   3.301 -  also have "\<dots> = ?ca * ?cb - ?sa*?sb"
   3.302 -    by simp
   3.303 -  finally show ?thesis .
   3.304 -qed
   3.305 -
   3.306 -end