src/HOL/Library/Formal_Power_Series.thy
changeset 32161 abda97d2deea
parent 32047 c141f139ce26
parent 32160 63686057cbe8
child 32162 c6a045559ce6
     1.1 --- a/src/HOL/Library/Formal_Power_Series.thy	Thu Jul 23 20:05:20 2009 +0200
     1.2 +++ b/src/HOL/Library/Formal_Power_Series.thy	Thu Jul 23 21:13:21 2009 +0200
     1.3 @@ -5,7 +5,7 @@
     1.4  header{* A formalization of formal power series *}
     1.5  
     1.6  theory Formal_Power_Series
     1.7 -imports Complex_Main
     1.8 +imports Complex_Main Binomial
     1.9  begin
    1.10  
    1.11  
    1.12 @@ -469,7 +469,6 @@
    1.13  
    1.14  lemma dist_fps_sym: "dist (a::'a fps) b = dist b a"
    1.15    apply (auto simp add: dist_fps_def)
    1.16 -  thm cong[OF refl]
    1.17    apply (rule cong[OF refl, where x="(\<lambda>n\<Colon>nat. a $ n \<noteq> b $ n)"])
    1.18    apply (rule ext)
    1.19    by auto
    1.20 @@ -2333,7 +2332,6 @@
    1.21  
    1.22  from a0 have ia0: "?ia $ 0 \<noteq> 0" by (simp )
    1.23  from a0 have ab0: "?ab $ 0 \<noteq> 0" by (simp add: fps_compose_def)
    1.24 -thm inverse_mult_eq_1[OF ab0]
    1.25  have "(?ia oo b) *  (a oo b) = 1"
    1.26  unfolding fps_compose_mult_distrib[OF b0, symmetric]
    1.27  unfolding inverse_mult_eq_1[OF a0]
    1.28 @@ -2606,7 +2604,8 @@
    1.29  lemma E_power_mult: "(E (c::'a::field_char_0))^n = E (of_nat n * c)"
    1.30    by (induct n, auto simp add: ring_simps E_add_mult power_Suc)
    1.31  
    1.32 -lemma assumes r: "r (Suc k) 1 = 1" 
    1.33 +lemma radical_E:
    1.34 +  assumes r: "r (Suc k) 1 = 1" 
    1.35    shows "fps_radical r (Suc k) (E (c::'a::{field_char_0})) = E (c / of_nat (Suc k))"
    1.36  proof-
    1.37    let ?ck = "(c / of_nat (Suc k))"
    1.38 @@ -2625,6 +2624,29 @@
    1.39    apply (auto simp add: fps_eq_iff E_def fps_compose_def power_mult_distrib)
    1.40    by (simp add: cond_value_iff cond_application_beta setsum_delta' cong del: if_weak_cong)
    1.41  
    1.42 +text{* The generalized binomial theorem as a  consequence of @{thm E_add_mult} *}
    1.43 +
    1.44 +lemma gbinomial_theorem: 
    1.45 +  "((a::'a::{field_char_0, division_by_zero})+b) ^ n = (\<Sum>k=0..n. of_nat (n choose k) * a^k * b^(n-k))"
    1.46 +proof-
    1.47 +  from E_add_mult[of a b] 
    1.48 +  have "(E (a + b)) $ n = (E a * E b)$n" by simp
    1.49 +  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))))"
    1.50 +    by (simp add: field_simps fps_mult_nth of_nat_mult[symmetric] setsum_right_distrib)
    1.51 +  then show ?thesis 
    1.52 +    apply simp
    1.53 +    apply (rule setsum_cong2)
    1.54 +    apply simp
    1.55 +    apply (frule binomial_fact[where ?'a = 'a, symmetric])
    1.56 +    by (simp add: field_simps of_nat_mult)
    1.57 +qed
    1.58 +
    1.59 +text{* And the nat-form -- also available from Binomial.thy *}
    1.60 +lemma binomial_theorem: "(a+b) ^ n = (\<Sum>k=0..n. (n choose k) * a^k * b^(n-k))"
    1.61 +  using gbinomial_theorem[of "of_nat a" "of_nat b" n]
    1.62 +  unfolding of_nat_add[symmetric] of_nat_power[symmetric] of_nat_mult[symmetric] of_nat_setsum[symmetric]
    1.63 +  by simp
    1.64 +
    1.65  subsubsection{* Logarithmic series *}
    1.66  
    1.67  lemma Abs_fps_if_0: 
    1.68 @@ -2679,6 +2701,278 @@
    1.69      unfolding fps_deriv_eq_iff by simp
    1.70  qed
    1.71  
    1.72 +subsubsection{* Binomial series *}
    1.73 +
    1.74 +definition "fps_binomial a = Abs_fps (\<lambda>n. a gchoose n)"
    1.75 +
    1.76 +lemma fps_binomial_nth[simp]: "fps_binomial a $ n = a gchoose n"
    1.77 +  by (simp add: fps_binomial_def)
    1.78 +
    1.79 +lemma fps_binomial_ODE_unique:
    1.80 +  fixes c :: "'a::field_char_0"
    1.81 +  shows "fps_deriv a = (fps_const c * a) / (1 + X) \<longleftrightarrow> a = fps_const (a$0) * fps_binomial c"
    1.82 +  (is "?lhs \<longleftrightarrow> ?rhs")
    1.83 +proof-
    1.84 +  let ?da = "fps_deriv a"
    1.85 +  let ?x1 = "(1 + X):: 'a fps"
    1.86 +  let ?l = "?x1 * ?da"
    1.87 +  let ?r = "fps_const c * a"
    1.88 +  have x10: "?x1 $ 0 \<noteq> 0" by simp
    1.89 +  have "?l = ?r \<longleftrightarrow> inverse ?x1 * ?l = inverse ?x1 * ?r" by simp
    1.90 +  also have "\<dots> \<longleftrightarrow> ?da = (fps_const c * a) / ?x1"
    1.91 +    apply (simp only: fps_divide_def  mult_assoc[symmetric] inverse_mult_eq_1[OF x10])
    1.92 +    by (simp add: ring_simps)
    1.93 +  finally have eq: "?l = ?r \<longleftrightarrow> ?lhs" by simp
    1.94 +  moreover
    1.95 +  {assume h: "?l = ?r" 
    1.96 +    {fix n
    1.97 +      from h have lrn: "?l $ n = ?r$n" by simp
    1.98 +      
    1.99 +      from lrn 
   1.100 +      have "a$ Suc n = ((c - of_nat n) / of_nat (Suc n)) * a $n" 
   1.101 +	apply (simp add: ring_simps del: of_nat_Suc)
   1.102 +	by (cases n, simp_all add: field_simps del: of_nat_Suc)
   1.103 +    }
   1.104 +    note th0 = this
   1.105 +    {fix n have "a$n = (c gchoose n) * a$0"
   1.106 +      proof(induct n)
   1.107 +	case 0 thus ?case by simp
   1.108 +      next
   1.109 +	case (Suc m)
   1.110 +	thus ?case unfolding th0
   1.111 +	  apply (simp add: field_simps del: of_nat_Suc)
   1.112 +	  unfolding mult_assoc[symmetric] gbinomial_mult_1
   1.113 +	  by (simp add: ring_simps)
   1.114 +      qed}
   1.115 +    note th1 = this
   1.116 +    have ?rhs
   1.117 +      apply (simp add: fps_eq_iff)
   1.118 +      apply (subst th1)
   1.119 +      by (simp add: ring_simps)}
   1.120 +  moreover
   1.121 +  {assume h: ?rhs
   1.122 +  have th00:"\<And>x y. x * (a$0 * y) = a$0 * (x*y)" by (simp add: mult_commute)
   1.123 +    have "?l = ?r" 
   1.124 +      apply (subst h)
   1.125 +      apply (subst (2) h)
   1.126 +      apply (clarsimp simp add: fps_eq_iff ring_simps)
   1.127 +      unfolding mult_assoc[symmetric] th00 gbinomial_mult_1
   1.128 +      by (simp add: ring_simps gbinomial_mult_1)}
   1.129 +  ultimately show ?thesis by blast
   1.130 +qed
   1.131 +
   1.132 +lemma fps_binomial_deriv: "fps_deriv (fps_binomial c) = fps_const c * fps_binomial c / (1 + X)"
   1.133 +proof-
   1.134 +  let ?a = "fps_binomial c"
   1.135 +  have th0: "?a = fps_const (?a$0) * ?a" by (simp)
   1.136 +  from iffD2[OF fps_binomial_ODE_unique, OF th0] show ?thesis .
   1.137 +qed
   1.138 +
   1.139 +lemma fps_binomial_add_mult: "fps_binomial (c+d) = fps_binomial c * fps_binomial d" (is "?l = ?r")
   1.140 +proof-
   1.141 +  let ?P = "?r - ?l"
   1.142 +  let ?b = "fps_binomial"
   1.143 +  let ?db = "\<lambda>x. fps_deriv (?b x)"
   1.144 +  have "fps_deriv ?P = ?db c * ?b d + ?b c * ?db d - ?db (c + d)"  by simp
   1.145 +  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))"
   1.146 +    unfolding fps_binomial_deriv
   1.147 +    by (simp add: fps_divide_def ring_simps)
   1.148 +  also have "\<dots> = (fps_const (c + d)/ (1 + X)) * ?P"
   1.149 +    by (simp add: ring_simps fps_divide_def fps_const_add[symmetric] del: fps_const_add)
   1.150 +  finally have th0: "fps_deriv ?P = fps_const (c+d) * ?P / (1 + X)"
   1.151 +    by (simp add: fps_divide_def)
   1.152 +  have "?P = fps_const (?P$0) * ?b (c + d)"
   1.153 +    unfolding fps_binomial_ODE_unique[symmetric]
   1.154 +    using th0 by simp
   1.155 +  hence "?P = 0" by (simp add: fps_mult_nth)
   1.156 +  then show ?thesis by simp
   1.157 +qed
   1.158 +
   1.159 +lemma fps_minomial_minus_one: "fps_binomial (- 1) = inverse (1 + X)"
   1.160 +  (is "?l = inverse ?r")
   1.161 +proof-
   1.162 +  have th: "?r$0 \<noteq> 0" by simp
   1.163 +  have th': "fps_deriv (inverse ?r) = fps_const (- 1) * inverse ?r / (1 + X)"
   1.164 +    by (simp add: fps_inverse_deriv[OF th] fps_divide_def power2_eq_square mult_commute fps_const_neg[symmetric] del: fps_const_neg)
   1.165 +  have eq: "inverse ?r $ 0 = 1"
   1.166 +    by (simp add: fps_inverse_def)
   1.167 +  from iffD1[OF fps_binomial_ODE_unique[of "inverse (1 + X)" "- 1"] th'] eq
   1.168 +  show ?thesis by (simp add: fps_inverse_def)
   1.169 +qed
   1.170 +
   1.171 +text{* Vandermonde's Identity as a consequence *}
   1.172 +lemma gbinomial_Vandermonde: "setsum (\<lambda>k. (a gchoose k) * (b gchoose (n - k))) {0..n} = (a + b) gchoose n"
   1.173 +proof-
   1.174 +  let ?ba = "fps_binomial a"
   1.175 +  let ?bb = "fps_binomial b"
   1.176 +  let ?bab = "fps_binomial (a + b)"
   1.177 +  from fps_binomial_add_mult[of a b] have "?bab $ n = (?ba * ?bb)$n" by simp
   1.178 +  then show ?thesis by (simp add: fps_mult_nth)
   1.179 +qed
   1.180 +
   1.181 +lemma binomial_Vandermonde: "setsum (\<lambda>k. (a choose k) * (b choose (n - k))) {0..n} = (a + b) choose n"
   1.182 +  using gbinomial_Vandermonde[of "(of_nat a)" "of_nat b" n]
   1.183 +  
   1.184 +  apply (simp only: binomial_gbinomial[symmetric] of_nat_mult[symmetric] of_nat_setsum[symmetric] of_nat_add[symmetric])
   1.185 +  by simp
   1.186 +  
   1.187 +lemma binomial_Vandermonde_same: "setsum (\<lambda>k. (n choose k)^2) {0..n} = (2*n) choose n"
   1.188 +  using binomial_Vandermonde[of n n n,symmetric]
   1.189 +  unfolding nat_mult_2 apply (simp add: power2_eq_square)
   1.190 +  apply (rule setsum_cong2)
   1.191 +  by (auto intro:  binomial_symmetric)
   1.192 +
   1.193 +lemma Vandermonde_pochhammer_lemma:
   1.194 +  fixes a :: "'a::field_char_0"
   1.195 +  assumes b: "\<forall> j\<in>{0 ..<n}. b \<noteq> of_nat j"
   1.196 +  shows "setsum (%k. (pochhammer (- a) k * pochhammer (- (of_nat n)) k) / (of_nat (fact k) * pochhammer (b - of_nat n + 1) k)) {0..n} = pochhammer (- (a+ b)) n / pochhammer (- b) n" (is "?l = ?r")
   1.197 +proof-
   1.198 +  let ?m1 = "%m. (- 1 :: 'a) ^ m"
   1.199 +  let ?f = "%m. of_nat (fact m)"
   1.200 +  let ?p = "%(x::'a). pochhammer (- x)"
   1.201 +  from b have bn0: "?p b n \<noteq> 0" unfolding pochhammer_eq_0_iff by simp
   1.202 +  {fix k assume kn: "k \<in> {0..n}"
   1.203 +    {assume c:"pochhammer (b - of_nat n + 1) n = 0"
   1.204 +      then obtain j where j: "j < n" "b - of_nat n + 1 = - of_nat j"
   1.205 +	unfolding pochhammer_eq_0_iff by blast
   1.206 +      from j have "b = of_nat n - of_nat j - of_nat 1" 
   1.207 +	by (simp add: algebra_simps)
   1.208 +      then have "b = of_nat (n - j - 1)" 
   1.209 +	using j kn by (simp add: of_nat_diff)
   1.210 +      with b have False using j by auto}
   1.211 +    then have nz: "pochhammer (1 + b - of_nat n) n \<noteq> 0" 
   1.212 +      by (auto simp add: algebra_simps)
   1.213 +    
   1.214 +    from nz kn have nz': "pochhammer (1 + b - of_nat n) k \<noteq> 0" 
   1.215 +      by (simp add: pochhammer_neq_0_mono)
   1.216 +    {assume k0: "k = 0 \<or> n =0" 
   1.217 +      then have "b gchoose (n - k) = (?m1 n * ?p b n * ?m1 k * ?p (of_nat n) k) / (?f n * pochhammer (b - of_nat n + 1) k)" 
   1.218 +	using kn
   1.219 +	by (cases "k=0", simp_all add: gbinomial_pochhammer)}
   1.220 +    moreover
   1.221 +    {assume n0: "n \<noteq> 0" and k0: "k \<noteq> 0" 
   1.222 +      then obtain m where m: "n = Suc m" by (cases n, auto)
   1.223 +      from k0 obtain h where h: "k = Suc h" by (cases k, auto)
   1.224 +      {assume kn: "k = n"
   1.225 +	then have "b gchoose (n - k) = (?m1 n * ?p b n * ?m1 k * ?p (of_nat n) k) / (?f n * pochhammer (b - of_nat n + 1) k)"
   1.226 +	  using kn pochhammer_minus'[where k=k and n=n and b=b]
   1.227 +	  apply (simp add:  pochhammer_same)
   1.228 +	  using bn0
   1.229 +	  by (simp add: field_simps power_add[symmetric])}
   1.230 +      moreover
   1.231 +      {assume nk: "k \<noteq> n"
   1.232 +	have m1nk: "?m1 n = setprod (%i. - 1) {0..m}" 
   1.233 +	  "?m1 k = setprod (%i. - 1) {0..h}"
   1.234 +	  by (simp_all add: setprod_constant m h)
   1.235 +	from kn nk have kn': "k < n" by simp
   1.236 +	have bnz0: "pochhammer (b - of_nat n + 1) k \<noteq> 0"
   1.237 +	  using bn0 kn 
   1.238 +	  unfolding pochhammer_eq_0_iff
   1.239 +	  apply auto
   1.240 +	  apply (erule_tac x= "n - ka - 1" in allE)
   1.241 +	  by (auto simp add: algebra_simps of_nat_diff)
   1.242 +	have eq1: "setprod (%k. (1::'a) + of_nat m - of_nat k) {0 .. h} = setprod of_nat {Suc (m - h) .. Suc m}"	
   1.243 +	  apply (rule strong_setprod_reindex_cong[where f="%k. Suc m - k "])
   1.244 +	  using kn' h m
   1.245 +	  apply (auto simp add: inj_on_def image_def)
   1.246 +	  apply (rule_tac x="Suc m - x" in bexI)
   1.247 +	  apply (simp_all add: of_nat_diff)
   1.248 +	  done
   1.249 +	
   1.250 +	have th1: "(?m1 k * ?p (of_nat n) k) / ?f n = 1 / of_nat(fact (n - k))"
   1.251 +	  unfolding m1nk 
   1.252 +	  
   1.253 +	  unfolding m h pochhammer_Suc_setprod
   1.254 +	  apply (simp add: field_simps del: fact_Suc id_def)
   1.255 +	  unfolding fact_setprod id_def
   1.256 +	  unfolding of_nat_setprod
   1.257 +	  unfolding setprod_timesf[symmetric]
   1.258 +	  apply auto
   1.259 +	  unfolding eq1
   1.260 +	  apply (subst setprod_Un_disjoint[symmetric])
   1.261 +	  apply (auto)
   1.262 +	  apply (rule setprod_cong)
   1.263 +	  apply auto
   1.264 +	  done
   1.265 +	have th20: "?m1 n * ?p b n = setprod (%i. b - of_nat i) {0..m}"
   1.266 +	  unfolding m1nk 
   1.267 +	  unfolding m h pochhammer_Suc_setprod
   1.268 +	  unfolding setprod_timesf[symmetric]
   1.269 +	  apply (rule setprod_cong)
   1.270 +	  apply auto
   1.271 +	  done
   1.272 +	have th21:"pochhammer (b - of_nat n + 1) k = setprod (%i. b - of_nat i) {n - k .. n - 1}"
   1.273 +	  unfolding h m 
   1.274 +	  unfolding pochhammer_Suc_setprod
   1.275 +	  apply (rule strong_setprod_reindex_cong[where f="%k. n - 1 - k"])
   1.276 +	  using kn
   1.277 +	  apply (auto simp add: inj_on_def m h image_def)
   1.278 +	  apply (rule_tac x= "m - x" in bexI)
   1.279 +	  by (auto simp add: of_nat_diff)
   1.280 +	
   1.281 +	have "?m1 n * ?p b n = pochhammer (b - of_nat n + 1) k * setprod (%i. b - of_nat i) {0.. n - k - 1}"
   1.282 +	  unfolding th20 th21
   1.283 +	  unfolding h m
   1.284 +	  apply (subst setprod_Un_disjoint[symmetric])
   1.285 +	  using kn' h m
   1.286 +	  apply auto
   1.287 +	  apply (rule setprod_cong)
   1.288 +	  apply auto
   1.289 +	  done
   1.290 +	then have th2: "(?m1 n * ?p b n)/pochhammer (b - of_nat n + 1) k = setprod (%i. b - of_nat i) {0.. n - k - 1}" 
   1.291 +	  using nz' by (simp add: field_simps)
   1.292 +	have "(?m1 n * ?p b n * ?m1 k * ?p (of_nat n) k) / (?f n * pochhammer (b - of_nat n + 1) k) = ((?m1 k * ?p (of_nat n) k) / ?f n) * ((?m1 n * ?p b n)/pochhammer (b - of_nat n + 1) k)"
   1.293 +	  using bnz0
   1.294 +	  by (simp add: field_simps)
   1.295 +	also have "\<dots> = b gchoose (n - k)" 
   1.296 +	  unfolding th1 th2
   1.297 +	  using kn' by (simp add: gbinomial_def)
   1.298 +	finally have "b gchoose (n - k) = (?m1 n * ?p b n * ?m1 k * ?p (of_nat n) k) / (?f n * pochhammer (b - of_nat n + 1) k)" by simp}
   1.299 +      ultimately have "b gchoose (n - k) = (?m1 n * ?p b n * ?m1 k * ?p (of_nat n) k) / (?f n * pochhammer (b - of_nat n + 1) k)"
   1.300 +	by (cases "k =n", auto)}
   1.301 +    ultimately have "b gchoose (n - k) = (?m1 n * ?p b n * ?m1 k * ?p (of_nat n) k) / (?f n * pochhammer (b - of_nat n + 1) k)" "pochhammer (1 + b - of_nat n) k \<noteq> 0 "
   1.302 +      using nz' 
   1.303 +      apply (cases "n=0", auto)
   1.304 +      by (cases "k", auto)}
   1.305 +  note th00 = this
   1.306 +  have "?r = ((a + b) gchoose n) * (of_nat (fact n)/ (?m1 n * pochhammer (- b) n))"
   1.307 +    unfolding gbinomial_pochhammer 
   1.308 +    using bn0 by (auto simp add: field_simps)
   1.309 +  also have "\<dots> = ?l"
   1.310 +    unfolding gbinomial_Vandermonde[symmetric]
   1.311 +    apply (simp add: th00)
   1.312 +    unfolding gbinomial_pochhammer
   1.313 +    using bn0 apply (simp add: setsum_left_distrib setsum_right_distrib field_simps)
   1.314 +    apply (rule setsum_cong2)
   1.315 +    apply (drule th00(2))
   1.316 +    by (simp add: field_simps power_add[symmetric])
   1.317 +  finally show ?thesis by simp
   1.318 +qed 
   1.319 +
   1.320 +    
   1.321 +lemma Vandermonde_pochhammer:
   1.322 +   fixes a :: "'a::field_char_0"
   1.323 +  assumes c: "ALL i : {0..< n}. c \<noteq> - of_nat i"
   1.324 +  shows "setsum (%k. (pochhammer a k * pochhammer (- (of_nat n)) k) / (of_nat (fact k) * pochhammer c k)) {0..n} = pochhammer (c - a) n / pochhammer c n"
   1.325 +proof-
   1.326 +  let ?a = "- a"
   1.327 +  let ?b = "c + of_nat n - 1"
   1.328 +  have h: "\<forall> j \<in>{0..< n}. ?b \<noteq> of_nat j" using c
   1.329 +    apply (auto simp add: algebra_simps of_nat_diff)
   1.330 +    apply (erule_tac x= "n - j - 1" in ballE)
   1.331 +    by (auto simp add: of_nat_diff algebra_simps)
   1.332 +  have th0: "pochhammer (- (?a + ?b)) n = (- 1)^n * pochhammer (c - a) n"
   1.333 +    unfolding pochhammer_minus[OF le_refl]
   1.334 +    by (simp add: algebra_simps)
   1.335 +  have th1: "pochhammer (- ?b) n = (- 1)^n * pochhammer c n"
   1.336 +    unfolding pochhammer_minus[OF le_refl]
   1.337 +    by simp
   1.338 +  have nz: "pochhammer c n \<noteq> 0" using c
   1.339 +    by (simp add: pochhammer_eq_0_iff)
   1.340 +  from Vandermonde_pochhammer_lemma[where a = "?a" and b="?b" and n=n, OF h, unfolded th0 th1]
   1.341 +  show ?thesis using nz by (simp add: field_simps setsum_right_distrib)
   1.342 +qed
   1.343 +
   1.344  subsubsection{* Formal trigonometric functions  *}
   1.345  
   1.346  definition "fps_sin (c::'a::field_char_0) =
   1.347 @@ -2866,4 +3160,171 @@
   1.348      by simp
   1.349  qed
   1.350  
   1.351 +text {* Connection to E c over the complex numbers --- Euler and De Moivre*}
   1.352 +lemma Eii_sin_cos:
   1.353 +  "E (ii * c) = fps_cos c + fps_const ii * fps_sin c "
   1.354 +  (is "?l = ?r")
   1.355 +proof-
   1.356 +  {fix n::nat
   1.357 +    {assume en: "even n"
   1.358 +      from en obtain m where m: "n = 2*m" 
   1.359 +	unfolding even_mult_two_ex by blast
   1.360 +      
   1.361 +      have "?l $n = ?r$n" 
   1.362 +	by (simp add: m fps_sin_def fps_cos_def power_mult_distrib
   1.363 +	  power_mult power_minus)}
   1.364 +    moreover
   1.365 +    {assume on: "odd n"
   1.366 +      from on obtain m where m: "n = 2*m + 1" 
   1.367 +	unfolding odd_nat_equiv_def2 by (auto simp add: nat_mult_2)  
   1.368 +      have "?l $n = ?r$n" 
   1.369 +	by (simp add: m fps_sin_def fps_cos_def power_mult_distrib
   1.370 +	  power_mult power_minus)}
   1.371 +    ultimately have "?l $n = ?r$n"  by blast}
   1.372 +  then show ?thesis by (simp add: fps_eq_iff)
   1.373 +qed
   1.374 +
   1.375 +lemma E_minus_ii_sin_cos: "E (- (ii * c)) = fps_cos c - fps_const ii * fps_sin c "
   1.376 +  unfolding minus_mult_right Eii_sin_cos by (simp add: fps_sin_even fps_cos_odd)
   1.377 +
   1.378 +lemma fps_const_minus: "fps_const (c::'a::group_add) - fps_const d = fps_const (c - d)"
   1.379 +  by (simp add: fps_eq_iff fps_const_def)
   1.380 +
   1.381 +lemma fps_number_of_fps_const: "number_of i = fps_const (number_of i :: 'a:: {comm_ring_1, number_ring})"
   1.382 +  apply (subst (2) number_of_eq)
   1.383 +apply(rule int_induct[of _ 0])
   1.384 +apply (simp_all add: number_of_fps_def)
   1.385 +by (simp_all add: fps_const_add[symmetric] fps_const_minus[symmetric])
   1.386 +
   1.387 +lemma fps_cos_Eii:
   1.388 +  "fps_cos c = (E (ii * c) + E (- ii * c)) / fps_const 2"
   1.389 +proof-
   1.390 +  have th: "fps_cos c + fps_cos c = fps_cos c * fps_const 2" 
   1.391 +    by (simp add: fps_eq_iff fps_number_of_fps_const complex_number_of_def[symmetric])
   1.392 +  show ?thesis
   1.393 +  unfolding Eii_sin_cos minus_mult_commute
   1.394 +  by (simp add: fps_sin_even fps_cos_odd fps_number_of_fps_const
   1.395 +    fps_divide_def fps_const_inverse th complex_number_of_def[symmetric])
   1.396 +qed
   1.397 +
   1.398 +lemma fps_sin_Eii:
   1.399 +  "fps_sin c = (E (ii * c) - E (- ii * c)) / fps_const (2*ii)"
   1.400 +proof-
   1.401 +  have th: "fps_const \<i> * fps_sin c + fps_const \<i> * fps_sin c = fps_sin c * fps_const (2 * ii)" 
   1.402 +    by (simp add: fps_eq_iff fps_number_of_fps_const complex_number_of_def[symmetric])
   1.403 +  show ?thesis
   1.404 +  unfolding Eii_sin_cos minus_mult_commute
   1.405 +  by (simp add: fps_sin_even fps_cos_odd fps_divide_def fps_const_inverse th)
   1.406 +qed
   1.407 +
   1.408 +lemma fps_tan_Eii:
   1.409 +  "fps_tan c = (E (ii * c) - E (- ii * c)) / (fps_const ii * (E (ii * c) + E (- ii * c)))"
   1.410 +  unfolding fps_tan_def fps_sin_Eii fps_cos_Eii mult_minus_left E_neg
   1.411 +  apply (simp add: fps_divide_def fps_inverse_mult fps_const_mult[symmetric] fps_const_inverse del: fps_const_mult)
   1.412 +  by simp
   1.413 +
   1.414 +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)"
   1.415 +  unfolding Eii_sin_cos[symmetric] E_power_mult
   1.416 +  by (simp add: mult_ac)
   1.417 +
   1.418 +subsection {* Hypergeometric series *}
   1.419 +
   1.420 +
   1.421 +definition "F as bs (c::'a::{field_char_0, division_by_zero}) = Abs_fps (%n. (foldl (%r a. r* pochhammer a n) 1 as * c^n)/ (foldl (%r b. r * pochhammer b n) 1 bs * of_nat (fact n)))"
   1.422 +
   1.423 +lemma F_nth[simp]: "F as bs c $ n =  (foldl (%r a. r* pochhammer a n) 1 as * c^n)/ (foldl (%r b. r * pochhammer b n) 1 bs * of_nat (fact n))"
   1.424 +  by (simp add: F_def)
   1.425 +
   1.426 +lemma foldl_mult_start:
   1.427 +  "foldl (%r x. r * f x) (v::'a::comm_ring_1) as * x = foldl (%r x. r * f x) (v * x) as "
   1.428 +  by (induct as arbitrary: x v, auto simp add: algebra_simps)
   1.429 +
   1.430 +lemma foldr_mult_foldl: "foldr (%x r. r * f x) as v = foldl (%r x. r * f x) (v :: 'a::comm_ring_1) as"
   1.431 +  by (induct as arbitrary: v, auto simp add: foldl_mult_start)
   1.432 +
   1.433 +lemma F_nth_alt: "F as bs c $ n = foldr (\<lambda>a r. r * pochhammer a n) as (c ^ n) /
   1.434 +    foldr (\<lambda>b r. r * pochhammer b n) bs (of_nat (fact n))"
   1.435 +  by (simp add: foldl_mult_start foldr_mult_foldl)
   1.436 +
   1.437 +lemma F_E[simp]: "F [] [] c = E c" 
   1.438 +  by (simp add: fps_eq_iff)
   1.439 +
   1.440 +lemma F_1_0[simp]: "F [1] [] c = 1/(1 - fps_const c * X)"
   1.441 +proof-
   1.442 +  let ?a = "(Abs_fps (\<lambda>n. 1)) oo (fps_const c * X)"
   1.443 +  thm gp
   1.444 +  have th0: "(fps_const c * X) $ 0 = 0" by simp
   1.445 +  show ?thesis unfolding gp[OF th0, symmetric]
   1.446 +    by (auto simp add: fps_eq_iff pochhammer_fact[symmetric] fps_compose_nth power_mult_distrib cond_value_iff setsum_delta' cong del: if_weak_cong)
   1.447 +qed
   1.448 +
   1.449 +lemma F_B[simp]: "F [-a] [] (- 1) = fps_binomial a"
   1.450 +  by (simp add: fps_eq_iff gbinomial_pochhammer algebra_simps)
   1.451 +
   1.452 +lemma F_0[simp]: "F as bs c $0 = 1"
   1.453 +  apply simp
   1.454 +  apply (subgoal_tac "ALL as. foldl (%(r::'a) (a::'a). r) 1 as = 1")
   1.455 +  apply auto
   1.456 +  apply (induct_tac as, auto)
   1.457 +  done
   1.458 +
   1.459 +lemma foldl_prod_prod: "foldl (%(r::'b::comm_ring_1) (x::'a::comm_ring_1). r * f x) v as * foldl (%r x. r * g x) w as = foldl (%r x. r * f x * g x) (v*w) as"
   1.460 +  by (induct as arbitrary: v w, auto simp add: algebra_simps)
   1.461 +
   1.462 +
   1.463 +lemma F_rec: "F as bs c $ Suc n = ((foldl (%r a. r* (a + of_nat n)) c as)/ (foldl (%r b. r * (b + of_nat n)) (of_nat (Suc n)) bs )) * F as bs c $ n"
   1.464 +  apply (simp del: of_nat_Suc of_nat_add fact_Suc)
   1.465 +  apply (simp add: foldl_mult_start del: fact_Suc of_nat_Suc)
   1.466 +  unfolding foldl_prod_prod[unfolded foldl_mult_start] pochhammer_Suc
   1.467 +  by (simp add: algebra_simps of_nat_mult)
   1.468 +
   1.469 +lemma XD_nth[simp]: "XD a $ n = (if n=0 then 0 else of_nat n * a$n)"
   1.470 +  by (simp add: XD_def)
   1.471 +
   1.472 +lemma XD_0th[simp]: "XD a $ 0 = 0" by simp
   1.473 +lemma XD_Suc[simp]:" XD a $ Suc n = of_nat (Suc n) * a $ Suc n" by simp
   1.474 +
   1.475 +definition "XDp c a = XD a + fps_const c * a"
   1.476 +
   1.477 +lemma XDp_nth[simp]: "XDp c a $ n = (c + of_nat n) * a$n"
   1.478 +  by (simp add: XDp_def algebra_simps)
   1.479 +
   1.480 +lemma XDp_commute:
   1.481 +  shows "XDp b o XDp (c::'a::comm_ring_1) = XDp c o XDp b"
   1.482 +  by (auto simp add: XDp_def expand_fun_eq fps_eq_iff algebra_simps)
   1.483 +
   1.484 +lemma XDp0[simp]: "XDp 0 = XD"
   1.485 +  by (simp add: expand_fun_eq fps_eq_iff)
   1.486 +
   1.487 +lemma XDp_fps_integral[simp]:"XDp 0 (fps_integral a c) = X * a"
   1.488 +  by (simp add: fps_eq_iff fps_integral_def)
   1.489 +
   1.490 +lemma F_minus_nat: 
   1.491 +  "F [- of_nat n] [- of_nat (n + m)] (c::'a::{field_char_0, division_by_zero}) $ k = (if k <= n then pochhammer (- of_nat n) k * c ^ k /
   1.492 +    (pochhammer (- of_nat (n + m)) k * of_nat (fact k)) else 0)"
   1.493 +  "F [- of_nat m] [- of_nat (m + n)] (c::'a::{field_char_0, division_by_zero}) $ k = (if k <= m then pochhammer (- of_nat m) k * c ^ k /
   1.494 +    (pochhammer (- of_nat (m + n)) k * of_nat (fact k)) else 0)"
   1.495 +  by (auto simp add: pochhammer_eq_0_iff)
   1.496 +
   1.497 +lemma setsum_eq_if: "setsum f {(n::nat) .. m} = (if m < n then 0 else f n + setsum f {n+1 .. m})"
   1.498 +  apply simp
   1.499 +  apply (subst setsum_insert[symmetric])
   1.500 +  by (auto simp add: not_less setsum_head_Suc)
   1.501 +
   1.502 +lemma pochhammer_rec_if: 
   1.503 +  "pochhammer a n = (if n = 0 then 1 else a * pochhammer (a + 1) (n - 1))"
   1.504 +  by (cases n, simp_all add: pochhammer_rec)
   1.505 +
   1.506 +lemma XDp_foldr_nth[simp]: "foldr (%c r. XDp c o r) cs (%c. XDp c a) c0 $ n = 
   1.507 +  foldr (%c r. (c + of_nat n) * r) cs (c0 + of_nat n) * a$n"
   1.508 +  by (induct cs arbitrary: c0, auto simp add: algebra_simps)
   1.509 +
   1.510 +lemma genric_XDp_foldr_nth:
   1.511 +  assumes 
   1.512 +  f: "ALL n c a. f c a $ n = (of_nat n + k c) * a$n"
   1.513 +
   1.514 +  shows "foldr (%c r. f c o r) cs (%c. g c a) c0 $ n = 
   1.515 +  foldr (%c r. (k c + of_nat n) * r) cs (g c0 a $ n)"
   1.516 +  by (induct cs arbitrary: c0, auto simp add: algebra_simps f )
   1.517 +
   1.518  end