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.123 +    by (simp add: ring_simps fps_divide_def fps_const_add[symmetric] del: fps_const_add)
   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.217 +apply (simp_all add: number_of_fps_def)
   1.218 +by (simp_all add: fps_const_add[symmetric] fps_const_minus[symmetric])
   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