src/HOL/Library/Formal_Power_Series.thy
 changeset 32157 adea7a729c7a parent 31968 0314441a53a6 child 32160 63686057cbe8
```     1.1 --- a/src/HOL/Library/Formal_Power_Series.thy	Tue Jul 14 12:18:52 2009 +0200
1.2 +++ b/src/HOL/Library/Formal_Power_Series.thy	Wed Jul 15 06:14:25 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 @@ -2625,6 +2625,29 @@
1.13    apply (auto simp add: fps_eq_iff E_def fps_compose_def power_mult_distrib)
1.14    by (simp add: cond_value_iff cond_application_beta setsum_delta' cong del: if_weak_cong)
1.15
1.16 +text{* The generalized binomial theorem as a  consequence of @{thm E_add_mult} *}
1.17 +
1.18 +lemma gbinomial_theorem:
1.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))"
1.20 +proof-
1.21 +  from E_add_mult[of a b]
1.22 +  have "(E (a + b)) \$ n = (E a * E b)\$n" by simp
1.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))))"
1.24 +    by (simp add: field_simps fps_mult_nth of_nat_mult[symmetric] setsum_right_distrib)
1.25 +  then show ?thesis
1.26 +    apply simp
1.27 +    apply (rule setsum_cong2)
1.28 +    apply simp
1.29 +    apply (frule binomial_fact[where ?'a = 'a, symmetric])
1.30 +    by (simp add: field_simps of_nat_mult)
1.31 +qed
1.32 +
1.33 +text{* And the nat-form -- also available from Binomial.thy *}
1.34 +lemma binomial_theorem: "(a+b) ^ n = (\<Sum>k=0..n. (n choose k) * a^k * b^(n-k))"
1.35 +  using gbinomial_theorem[of "of_nat a" "of_nat b" n]
1.36 +  unfolding of_nat_add[symmetric] of_nat_power[symmetric] of_nat_mult[symmetric] of_nat_setsum[symmetric]
1.37 +  by simp
1.38 +
1.39  subsubsection{* Logarithmic series *}
1.40
1.41  lemma Abs_fps_if_0:
1.42 @@ -2679,6 +2702,137 @@
1.43      unfolding fps_deriv_eq_iff by simp
1.44  qed
1.45
1.46 +subsubsection{* Binomial series *}
1.47 +
1.48 +definition "fps_binomial a = Abs_fps (\<lambda>n. a gchoose n)"
1.49 +
1.50 +lemma fps_binomial_nth[simp]: "fps_binomial a \$ n = a gchoose n"
1.51 +  by (simp add: fps_binomial_def)
1.52 +
1.53 +lemma fps_binomial_ODE_unique:
1.54 +  fixes c :: "'a::field_char_0"
1.55 +  shows "fps_deriv a = (fps_const c * a) / (1 + X) \<longleftrightarrow> a = fps_const (a\$0) * fps_binomial c"
1.56 +  (is "?lhs \<longleftrightarrow> ?rhs")
1.57 +proof-
1.58 +  let ?da = "fps_deriv a"
1.59 +  let ?x1 = "(1 + X):: 'a fps"
1.60 +  let ?l = "?x1 * ?da"
1.61 +  let ?r = "fps_const c * a"
1.62 +  have x10: "?x1 \$ 0 \<noteq> 0" by simp
1.63 +  have "?l = ?r \<longleftrightarrow> inverse ?x1 * ?l = inverse ?x1 * ?r" by simp
1.64 +  also have "\<dots> \<longleftrightarrow> ?da = (fps_const c * a) / ?x1"
1.65 +    apply (simp only: fps_divide_def  mult_assoc[symmetric] inverse_mult_eq_1[OF x10])
1.66 +    by (simp add: ring_simps)
1.67 +  finally have eq: "?l = ?r \<longleftrightarrow> ?lhs" by simp
1.68 +  moreover
1.69 +  {assume h: "?l = ?r"
1.70 +    {fix n
1.71 +      from h have lrn: "?l \$ n = ?r\$n" by simp
1.72 +
1.73 +      from lrn
1.74 +      have "a\$ Suc n = ((c - of_nat n) / of_nat (Suc n)) * a \$n"
1.75 +	apply (simp add: ring_simps del: of_nat_Suc)
1.76 +	by (cases n, simp_all add: field_simps del: of_nat_Suc)
1.77 +    }
1.78 +    note th0 = this
1.79 +    {fix n have "a\$n = (c gchoose n) * a\$0"
1.80 +      proof(induct n)
1.81 +	case 0 thus ?case by simp
1.82 +      next
1.83 +	case (Suc m)
1.84 +	thus ?case unfolding th0
1.85 +	  apply (simp add: field_simps del: of_nat_Suc)
1.86 +	  unfolding mult_assoc[symmetric] gbinomial_mult_1
1.87 +	  by (simp add: ring_simps)
1.88 +      qed}
1.89 +    note th1 = this
1.90 +    have ?rhs
1.91 +      apply (simp add: fps_eq_iff)
1.92 +      apply (subst th1)
1.93 +      by (simp add: ring_simps)}
1.94 +  moreover
1.95 +  {assume h: ?rhs
1.96 +  have th00:"\<And>x y. x * (a\$0 * y) = a\$0 * (x*y)" by (simp add: mult_commute)
1.97 +    have "?l = ?r"
1.98 +      apply (subst h)
1.99 +      apply (subst (2) h)
1.100 +      apply (clarsimp simp add: fps_eq_iff ring_simps)
1.101 +      unfolding mult_assoc[symmetric] th00 gbinomial_mult_1
1.102 +      by (simp add: ring_simps gbinomial_mult_1)}
1.103 +  ultimately show ?thesis by blast
1.104 +qed
1.105 +
1.106 +lemma fps_binomial_deriv: "fps_deriv (fps_binomial c) = fps_const c * fps_binomial c / (1 + X)"
1.107 +proof-
1.108 +  let ?a = "fps_binomial c"
1.109 +  have th0: "?a = fps_const (?a\$0) * ?a" by (simp)
1.110 +  from iffD2[OF fps_binomial_ODE_unique, OF th0] show ?thesis .
1.111 +qed
1.112 +
1.113 +lemma fps_binomial_add_mult: "fps_binomial (c+d) = fps_binomial c * fps_binomial d" (is "?l = ?r")
1.114 +proof-
1.115 +  let ?P = "?r - ?l"
1.116 +  let ?b = "fps_binomial"
1.117 +  let ?db = "\<lambda>x. fps_deriv (?b x)"
1.118 +  have "fps_deriv ?P = ?db c * ?b d + ?b c * ?db d - ?db (c + d)"  by simp
1.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))"
1.120 +    unfolding fps_binomial_deriv
1.121 +    by (simp add: fps_divide_def ring_simps)
1.122 +  also have "\<dots> = (fps_const (c + d)/ (1 + X)) * ?P"
1.124 +  finally have th0: "fps_deriv ?P = fps_const (c+d) * ?P / (1 + X)"
1.125 +    by (simp add: fps_divide_def)
1.126 +  have "?P = fps_const (?P\$0) * ?b (c + d)"
1.127 +    unfolding fps_binomial_ODE_unique[symmetric]
1.128 +    using th0 by simp
1.129 +  hence "?P = 0" by (simp add: fps_mult_nth)
1.130 +  then show ?thesis by simp
1.131 +qed
1.132 +
1.133 +lemma fps_minomial_minus_one: "fps_binomial (- 1) = inverse (1 + X)"
1.134 +  (is "?l = inverse ?r")
1.135 +proof-
1.136 +  have th: "?r\$0 \<noteq> 0" by simp
1.137 +  have th': "fps_deriv (inverse ?r) = fps_const (- 1) * inverse ?r / (1 + X)"
1.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)
1.139 +  have eq: "inverse ?r \$ 0 = 1"
1.140 +    by (simp add: fps_inverse_def)
1.141 +  from iffD1[OF fps_binomial_ODE_unique[of "inverse (1 + X)" "- 1"] th'] eq
1.142 +  show ?thesis by (simp add: fps_inverse_def)
1.143 +qed
1.144 +
1.145 +text{* Vandermonde's Identity as a consequence *}
1.146 +lemma gbinomial_Vandermond: "setsum (\<lambda>k. (a gchoose k) * (b gchoose (n - k))) {0..n} = (a + b) gchoose n"
1.147 +proof-
1.148 +  let ?ba = "fps_binomial a"
1.149 +  let ?bb = "fps_binomial b"
1.150 +  let ?bab = "fps_binomial (a + b)"
1.151 +  from fps_binomial_add_mult[of a b] have "?bab \$ n = (?ba * ?bb)\$n" by simp
1.152 +  then show ?thesis by (simp add: fps_mult_nth)
1.153 +qed
1.154 +
1.155 +lemma binomial_Vandermond: "setsum (\<lambda>k. (a choose k) * (b choose (n - k))) {0..n} = (a + b) choose n"
1.156 +  using gbinomial_Vandermond[of "(of_nat a)" "of_nat b" n]
1.157 +
1.158 +  apply (simp only: binomial_gbinomial[symmetric] of_nat_mult[symmetric] of_nat_setsum[symmetric] of_nat_add[symmetric])
1.159 +  by simp
1.160 +
1.161 +lemma binomial_symmetric: assumes kn: "k \<le> n"
1.162 +  shows "n choose k = n choose (n - k)"
1.163 +proof-
1.164 +  from kn have kn': "n - k \<le> n" by arith
1.165 +  from binomial_fact_lemma[OF kn] binomial_fact_lemma[OF kn']
1.166 +  have "fact k * fact (n - k) * (n choose k) = fact (n - k) * fact (n - (n - k)) * (n choose (n - k))" by simp
1.167 +  then show ?thesis using kn by simp
1.168 +qed
1.169 +
1.170 +lemma binomial_Vandermond_same: "setsum (\<lambda>k. (n choose k)^2) {0..n} = (2*n) choose n"
1.171 +  using binomial_Vandermond[of n n n,symmetric]
1.172 +  unfolding nat_mult_2 apply (simp add: power2_eq_square)
1.173 +  apply (rule setsum_cong2)
1.174 +  by (auto intro:  binomial_symmetric)
1.175 +
1.176 +
1.177  subsubsection{* Formal trigonometric functions  *}
1.178
1.179  definition "fps_sin (c::'a::field_char_0) =
1.180 @@ -2869,4 +3023,71 @@
1.181      by simp
1.182  qed
1.183
1.184 +text {* Connection to E c over the complex numbers --- Euler and De Moivre*}
1.185 +lemma Eii_sin_cos:
1.186 +  "E (ii * c) = fps_cos c + fps_const ii * fps_sin c "
1.187 +  (is "?l = ?r")
1.188 +proof-
1.189 +  {fix n::nat
1.190 +    {assume en: "even n"
1.191 +      from en obtain m where m: "n = 2*m"
1.192 +	unfolding even_mult_two_ex by blast
1.193 +
1.194 +      have "?l \$n = ?r\$n"
1.195 +	by (simp add: m fps_sin_def fps_cos_def power_mult_distrib
1.196 +	  power_mult power_minus)}
1.197 +    moreover
1.198 +    {assume on: "odd n"
1.199 +      from on obtain m where m: "n = 2*m + 1"
1.200 +	unfolding odd_nat_equiv_def2 by (auto simp add: nat_mult_2)
1.201 +      have "?l \$n = ?r\$n"
1.202 +	by (simp add: m fps_sin_def fps_cos_def power_mult_distrib
1.203 +	  power_mult power_minus)}
1.204 +    ultimately have "?l \$n = ?r\$n"  by blast}
1.205 +  then show ?thesis by (simp add: fps_eq_iff)
1.206 +qed
1.207 +
1.208 +lemma E_minus_ii_sin_cos: "E (- (ii * c)) = fps_cos c - fps_const ii * fps_sin c "
1.209 +  unfolding minus_mult_right Eii_sin_cos by (simp add: fps_sin_even fps_cos_odd)
1.210 +
1.211 +lemma fps_const_minus: "fps_const (c::'a::group_add) - fps_const d = fps_const (c - d)"
1.212 +  by (simp add: fps_eq_iff fps_const_def)
1.213 +
1.214 +lemma fps_number_of_fps_const: "number_of i = fps_const (number_of i :: 'a:: {comm_ring_1, number_ring})"
1.215 +  apply (subst (2) number_of_eq)
1.216 +apply(rule int_induct[of _ 0])
1.219 +
1.220 +lemma fps_cos_Eii:
1.221 +  "fps_cos c = (E (ii * c) + E (- ii * c)) / fps_const 2"
1.222 +proof-
1.223 +  have th: "fps_cos c + fps_cos c = fps_cos c * fps_const 2"
1.224 +    by (simp add: fps_eq_iff fps_number_of_fps_const complex_number_of_def[symmetric])
1.225 +  show ?thesis
1.226 +  unfolding Eii_sin_cos minus_mult_commute
1.227 +  by (simp add: fps_sin_even fps_cos_odd fps_number_of_fps_const
1.228 +    fps_divide_def fps_const_inverse th complex_number_of_def[symmetric])
1.229 +qed
1.230 +
1.231 +lemma fps_sin_Eii:
1.232 +  "fps_sin c = (E (ii * c) - E (- ii * c)) / fps_const (2*ii)"
1.233 +proof-
1.234 +  have th: "fps_const \<i> * fps_sin c + fps_const \<i> * fps_sin c = fps_sin c * fps_const (2 * ii)"
1.235 +    by (simp add: fps_eq_iff fps_number_of_fps_const complex_number_of_def[symmetric])
1.236 +  show ?thesis
1.237 +  unfolding Eii_sin_cos minus_mult_commute
1.238 +  by (simp add: fps_sin_even fps_cos_odd fps_divide_def fps_const_inverse th)
1.239 +qed
1.240 +
1.241 +lemma fps_tan_Eii:
1.242 +  "fps_tan c = (E (ii * c) - E (- ii * c)) / (fps_const ii * (E (ii * c) + E (- ii * c)))"
1.243 +  unfolding fps_tan_def fps_sin_Eii fps_cos_Eii mult_minus_left E_neg
1.244 +  apply (simp add: fps_divide_def fps_inverse_mult fps_const_mult[symmetric] fps_const_inverse del: fps_const_mult)
1.245 +  by simp
1.246 +
1.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)"
1.248 +  unfolding Eii_sin_cos[symmetric] E_power_mult
1.249 +  by (simp add: mult_ac)
1.250 +
1.251  end
```