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.31
1.32 -lemma assumes r: "r (Suc k) 1 = 1"
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.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.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.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.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  [] 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.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
```