merged
authorchaieb
Thu Jul 23 21:13:21 2009 +0200 (2009-07-23)
changeset 32161abda97d2deea
parent 32152 53716a67c3b1
parent 32160 63686057cbe8
child 32162 c6a045559ce6
merged
src/HOL/IsaMakefile
src/HOL/Library/Binomial.thy
src/HOL/Library/Formal_Power_Series.thy
src/HOL/ex/Formal_Power_Series_Examples.thy
     1.1 --- a/src/HOL/IsaMakefile	Thu Jul 23 20:05:20 2009 +0200
     1.2 +++ b/src/HOL/IsaMakefile	Thu Jul 23 21:13:21 2009 +0200
     1.3 @@ -887,8 +887,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/Binomial.thy	Thu Jul 23 20:05:20 2009 +0200
     2.2 +++ b/src/HOL/Library/Binomial.thy	Thu Jul 23 21:13:21 2009 +0200
     2.3 @@ -282,6 +282,56 @@
     2.4      pochhammer_of_nat_eq_0_lemma'[of k n, where ?'a = 'a]
     2.5    by (auto simp add: not_le[symmetric])
     2.6  
     2.7 +
     2.8 +lemma pochhammer_eq_0_iff: 
     2.9 +  "pochhammer a n = (0::'a::field_char_0) \<longleftrightarrow> (EX k < n . a = - of_nat k) "
    2.10 +  apply (auto simp add: pochhammer_of_nat_eq_0_iff)
    2.11 +  apply (cases n, auto simp add: pochhammer_def algebra_simps group_add_class.eq_neg_iff_add_eq_0)
    2.12 +  apply (rule_tac x=x in exI)
    2.13 +  apply auto
    2.14 +  done
    2.15 +
    2.16 +
    2.17 +lemma pochhammer_eq_0_mono: 
    2.18 +  "pochhammer a n = (0::'a::field_char_0) \<Longrightarrow> m \<ge> n \<Longrightarrow> pochhammer a m = 0"
    2.19 +  unfolding pochhammer_eq_0_iff by auto 
    2.20 +
    2.21 +lemma pochhammer_neq_0_mono: 
    2.22 +  "pochhammer a m \<noteq> (0::'a::field_char_0) \<Longrightarrow> m \<ge> n \<Longrightarrow> pochhammer a n \<noteq> 0"
    2.23 +  unfolding pochhammer_eq_0_iff by auto 
    2.24 +
    2.25 +lemma pochhammer_minus:
    2.26 +  assumes kn: "k \<le> n" 
    2.27 +  shows "pochhammer (- b) k = ((- 1) ^ k :: 'a::comm_ring_1) * pochhammer (b - of_nat k + 1) k"
    2.28 +proof-
    2.29 +  {assume k0: "k = 0" then have ?thesis by simp}
    2.30 +  moreover 
    2.31 +  {fix h assume h: "k = Suc h"
    2.32 +    have eq: "((- 1) ^ Suc h :: 'a) = setprod (%i. - 1) {0 .. h}"
    2.33 +      using setprod_constant[where A="{0 .. h}" and y="- 1 :: 'a"]
    2.34 +      by auto
    2.35 +    have ?thesis
    2.36 +      unfolding h h pochhammer_Suc_setprod eq setprod_timesf[symmetric]
    2.37 +      apply (rule strong_setprod_reindex_cong[where f = "%i. h - i"])
    2.38 +      apply (auto simp add: inj_on_def image_def h )
    2.39 +      apply (rule_tac x="h - x" in bexI)
    2.40 +      by (auto simp add: expand_fun_eq h of_nat_diff)}
    2.41 +  ultimately show ?thesis by (cases k, auto)
    2.42 +qed
    2.43 +
    2.44 +lemma pochhammer_minus':
    2.45 +  assumes kn: "k \<le> n" 
    2.46 +  shows "pochhammer (b - of_nat k + 1) k = ((- 1) ^ k :: 'a::comm_ring_1) * pochhammer (- b) k"
    2.47 +  unfolding pochhammer_minus[OF kn, where b=b]
    2.48 +  unfolding mult_assoc[symmetric]
    2.49 +  unfolding power_add[symmetric]
    2.50 +  apply simp
    2.51 +  done
    2.52 +
    2.53 +lemma pochhammer_same: "pochhammer (- of_nat n) n = ((- 1) ^ n :: 'a::comm_ring_1) * of_nat (fact n)"
    2.54 +  unfolding pochhammer_minus[OF le_refl[of n]]
    2.55 +  by (simp add: of_nat_diff pochhammer_fact)
    2.56 +
    2.57  subsection{* Generalized binomial coefficients *}
    2.58  
    2.59  definition gbinomial :: "'a::field_char_0 \<Rightarrow> nat \<Rightarrow> 'a" (infixl "gchoose" 65)
    2.60 @@ -453,4 +503,14 @@
    2.61    ultimately show ?thesis by (cases k, auto)
    2.62  qed
    2.63  
    2.64 +
    2.65 +lemma binomial_symmetric: assumes kn: "k \<le> n" 
    2.66 +  shows "n choose k = n choose (n - k)"
    2.67 +proof-
    2.68 +  from kn have kn': "n - k \<le> n" by arith
    2.69 +  from binomial_fact_lemma[OF kn] binomial_fact_lemma[OF kn']
    2.70 +  have "fact k * fact (n - k) * (n choose k) = fact (n - k) * fact (n - (n - k)) * (n choose (n - k))" by simp
    2.71 +  then show ?thesis using kn by simp
    2.72 +qed
    2.73 +
    2.74  end
     3.1 --- a/src/HOL/Library/Formal_Power_Series.thy	Thu Jul 23 20:05:20 2009 +0200
     3.2 +++ b/src/HOL/Library/Formal_Power_Series.thy	Thu Jul 23 21:13:21 2009 +0200
     3.3 @@ -5,7 +5,7 @@
     3.4  header{* A formalization of formal power series *}
     3.5  
     3.6  theory Formal_Power_Series
     3.7 -imports Complex_Main
     3.8 +imports Complex_Main Binomial
     3.9  begin
    3.10  
    3.11  
    3.12 @@ -469,7 +469,6 @@
    3.13  
    3.14  lemma dist_fps_sym: "dist (a::'a fps) b = dist b a"
    3.15    apply (auto simp add: dist_fps_def)
    3.16 -  thm cong[OF refl]
    3.17    apply (rule cong[OF refl, where x="(\<lambda>n\<Colon>nat. a $ n \<noteq> b $ n)"])
    3.18    apply (rule ext)
    3.19    by auto
    3.20 @@ -2333,7 +2332,6 @@
    3.21  
    3.22  from a0 have ia0: "?ia $ 0 \<noteq> 0" by (simp )
    3.23  from a0 have ab0: "?ab $ 0 \<noteq> 0" by (simp add: fps_compose_def)
    3.24 -thm inverse_mult_eq_1[OF ab0]
    3.25  have "(?ia oo b) *  (a oo b) = 1"
    3.26  unfolding fps_compose_mult_distrib[OF b0, symmetric]
    3.27  unfolding inverse_mult_eq_1[OF a0]
    3.28 @@ -2606,7 +2604,8 @@
    3.29  lemma E_power_mult: "(E (c::'a::field_char_0))^n = E (of_nat n * c)"
    3.30    by (induct n, auto simp add: ring_simps E_add_mult power_Suc)
    3.31  
    3.32 -lemma assumes r: "r (Suc k) 1 = 1" 
    3.33 +lemma radical_E:
    3.34 +  assumes r: "r (Suc k) 1 = 1" 
    3.35    shows "fps_radical r (Suc k) (E (c::'a::{field_char_0})) = E (c / of_nat (Suc k))"
    3.36  proof-
    3.37    let ?ck = "(c / of_nat (Suc k))"
    3.38 @@ -2625,6 +2624,29 @@
    3.39    apply (auto simp add: fps_eq_iff E_def fps_compose_def power_mult_distrib)
    3.40    by (simp add: cond_value_iff cond_application_beta setsum_delta' cong del: if_weak_cong)
    3.41  
    3.42 +text{* The generalized binomial theorem as a  consequence of @{thm E_add_mult} *}
    3.43 +
    3.44 +lemma gbinomial_theorem: 
    3.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))"
    3.46 +proof-
    3.47 +  from E_add_mult[of a b] 
    3.48 +  have "(E (a + b)) $ n = (E a * E b)$n" by simp
    3.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))))"
    3.50 +    by (simp add: field_simps fps_mult_nth of_nat_mult[symmetric] setsum_right_distrib)
    3.51 +  then show ?thesis 
    3.52 +    apply simp
    3.53 +    apply (rule setsum_cong2)
    3.54 +    apply simp
    3.55 +    apply (frule binomial_fact[where ?'a = 'a, symmetric])
    3.56 +    by (simp add: field_simps of_nat_mult)
    3.57 +qed
    3.58 +
    3.59 +text{* And the nat-form -- also available from Binomial.thy *}
    3.60 +lemma binomial_theorem: "(a+b) ^ n = (\<Sum>k=0..n. (n choose k) * a^k * b^(n-k))"
    3.61 +  using gbinomial_theorem[of "of_nat a" "of_nat b" n]
    3.62 +  unfolding of_nat_add[symmetric] of_nat_power[symmetric] of_nat_mult[symmetric] of_nat_setsum[symmetric]
    3.63 +  by simp
    3.64 +
    3.65  subsubsection{* Logarithmic series *}
    3.66  
    3.67  lemma Abs_fps_if_0: 
    3.68 @@ -2679,6 +2701,278 @@
    3.69      unfolding fps_deriv_eq_iff by simp
    3.70  qed
    3.71  
    3.72 +subsubsection{* Binomial series *}
    3.73 +
    3.74 +definition "fps_binomial a = Abs_fps (\<lambda>n. a gchoose n)"
    3.75 +
    3.76 +lemma fps_binomial_nth[simp]: "fps_binomial a $ n = a gchoose n"
    3.77 +  by (simp add: fps_binomial_def)
    3.78 +
    3.79 +lemma fps_binomial_ODE_unique:
    3.80 +  fixes c :: "'a::field_char_0"
    3.81 +  shows "fps_deriv a = (fps_const c * a) / (1 + X) \<longleftrightarrow> a = fps_const (a$0) * fps_binomial c"
    3.82 +  (is "?lhs \<longleftrightarrow> ?rhs")
    3.83 +proof-
    3.84 +  let ?da = "fps_deriv a"
    3.85 +  let ?x1 = "(1 + X):: 'a fps"
    3.86 +  let ?l = "?x1 * ?da"
    3.87 +  let ?r = "fps_const c * a"
    3.88 +  have x10: "?x1 $ 0 \<noteq> 0" by simp
    3.89 +  have "?l = ?r \<longleftrightarrow> inverse ?x1 * ?l = inverse ?x1 * ?r" by simp
    3.90 +  also have "\<dots> \<longleftrightarrow> ?da = (fps_const c * a) / ?x1"
    3.91 +    apply (simp only: fps_divide_def  mult_assoc[symmetric] inverse_mult_eq_1[OF x10])
    3.92 +    by (simp add: ring_simps)
    3.93 +  finally have eq: "?l = ?r \<longleftrightarrow> ?lhs" by simp
    3.94 +  moreover
    3.95 +  {assume h: "?l = ?r" 
    3.96 +    {fix n
    3.97 +      from h have lrn: "?l $ n = ?r$n" by simp
    3.98 +      
    3.99 +      from lrn 
   3.100 +      have "a$ Suc n = ((c - of_nat n) / of_nat (Suc n)) * a $n" 
   3.101 +	apply (simp add: ring_simps del: of_nat_Suc)
   3.102 +	by (cases n, simp_all add: field_simps del: of_nat_Suc)
   3.103 +    }
   3.104 +    note th0 = this
   3.105 +    {fix n have "a$n = (c gchoose n) * a$0"
   3.106 +      proof(induct n)
   3.107 +	case 0 thus ?case by simp
   3.108 +      next
   3.109 +	case (Suc m)
   3.110 +	thus ?case unfolding th0
   3.111 +	  apply (simp add: field_simps del: of_nat_Suc)
   3.112 +	  unfolding mult_assoc[symmetric] gbinomial_mult_1
   3.113 +	  by (simp add: ring_simps)
   3.114 +      qed}
   3.115 +    note th1 = this
   3.116 +    have ?rhs
   3.117 +      apply (simp add: fps_eq_iff)
   3.118 +      apply (subst th1)
   3.119 +      by (simp add: ring_simps)}
   3.120 +  moreover
   3.121 +  {assume h: ?rhs
   3.122 +  have th00:"\<And>x y. x * (a$0 * y) = a$0 * (x*y)" by (simp add: mult_commute)
   3.123 +    have "?l = ?r" 
   3.124 +      apply (subst h)
   3.125 +      apply (subst (2) h)
   3.126 +      apply (clarsimp simp add: fps_eq_iff ring_simps)
   3.127 +      unfolding mult_assoc[symmetric] th00 gbinomial_mult_1
   3.128 +      by (simp add: ring_simps gbinomial_mult_1)}
   3.129 +  ultimately show ?thesis by blast
   3.130 +qed
   3.131 +
   3.132 +lemma fps_binomial_deriv: "fps_deriv (fps_binomial c) = fps_const c * fps_binomial c / (1 + X)"
   3.133 +proof-
   3.134 +  let ?a = "fps_binomial c"
   3.135 +  have th0: "?a = fps_const (?a$0) * ?a" by (simp)
   3.136 +  from iffD2[OF fps_binomial_ODE_unique, OF th0] show ?thesis .
   3.137 +qed
   3.138 +
   3.139 +lemma fps_binomial_add_mult: "fps_binomial (c+d) = fps_binomial c * fps_binomial d" (is "?l = ?r")
   3.140 +proof-
   3.141 +  let ?P = "?r - ?l"
   3.142 +  let ?b = "fps_binomial"
   3.143 +  let ?db = "\<lambda>x. fps_deriv (?b x)"
   3.144 +  have "fps_deriv ?P = ?db c * ?b d + ?b c * ?db d - ?db (c + d)"  by simp
   3.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))"
   3.146 +    unfolding fps_binomial_deriv
   3.147 +    by (simp add: fps_divide_def ring_simps)
   3.148 +  also have "\<dots> = (fps_const (c + d)/ (1 + X)) * ?P"
   3.149 +    by (simp add: ring_simps fps_divide_def fps_const_add[symmetric] del: fps_const_add)
   3.150 +  finally have th0: "fps_deriv ?P = fps_const (c+d) * ?P / (1 + X)"
   3.151 +    by (simp add: fps_divide_def)
   3.152 +  have "?P = fps_const (?P$0) * ?b (c + d)"
   3.153 +    unfolding fps_binomial_ODE_unique[symmetric]
   3.154 +    using th0 by simp
   3.155 +  hence "?P = 0" by (simp add: fps_mult_nth)
   3.156 +  then show ?thesis by simp
   3.157 +qed
   3.158 +
   3.159 +lemma fps_minomial_minus_one: "fps_binomial (- 1) = inverse (1 + X)"
   3.160 +  (is "?l = inverse ?r")
   3.161 +proof-
   3.162 +  have th: "?r$0 \<noteq> 0" by simp
   3.163 +  have th': "fps_deriv (inverse ?r) = fps_const (- 1) * inverse ?r / (1 + X)"
   3.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)
   3.165 +  have eq: "inverse ?r $ 0 = 1"
   3.166 +    by (simp add: fps_inverse_def)
   3.167 +  from iffD1[OF fps_binomial_ODE_unique[of "inverse (1 + X)" "- 1"] th'] eq
   3.168 +  show ?thesis by (simp add: fps_inverse_def)
   3.169 +qed
   3.170 +
   3.171 +text{* Vandermonde's Identity as a consequence *}
   3.172 +lemma gbinomial_Vandermonde: "setsum (\<lambda>k. (a gchoose k) * (b gchoose (n - k))) {0..n} = (a + b) gchoose n"
   3.173 +proof-
   3.174 +  let ?ba = "fps_binomial a"
   3.175 +  let ?bb = "fps_binomial b"
   3.176 +  let ?bab = "fps_binomial (a + b)"
   3.177 +  from fps_binomial_add_mult[of a b] have "?bab $ n = (?ba * ?bb)$n" by simp
   3.178 +  then show ?thesis by (simp add: fps_mult_nth)
   3.179 +qed
   3.180 +
   3.181 +lemma binomial_Vandermonde: "setsum (\<lambda>k. (a choose k) * (b choose (n - k))) {0..n} = (a + b) choose n"
   3.182 +  using gbinomial_Vandermonde[of "(of_nat a)" "of_nat b" n]
   3.183 +  
   3.184 +  apply (simp only: binomial_gbinomial[symmetric] of_nat_mult[symmetric] of_nat_setsum[symmetric] of_nat_add[symmetric])
   3.185 +  by simp
   3.186 +  
   3.187 +lemma binomial_Vandermonde_same: "setsum (\<lambda>k. (n choose k)^2) {0..n} = (2*n) choose n"
   3.188 +  using binomial_Vandermonde[of n n n,symmetric]
   3.189 +  unfolding nat_mult_2 apply (simp add: power2_eq_square)
   3.190 +  apply (rule setsum_cong2)
   3.191 +  by (auto intro:  binomial_symmetric)
   3.192 +
   3.193 +lemma Vandermonde_pochhammer_lemma:
   3.194 +  fixes a :: "'a::field_char_0"
   3.195 +  assumes b: "\<forall> j\<in>{0 ..<n}. b \<noteq> of_nat j"
   3.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")
   3.197 +proof-
   3.198 +  let ?m1 = "%m. (- 1 :: 'a) ^ m"
   3.199 +  let ?f = "%m. of_nat (fact m)"
   3.200 +  let ?p = "%(x::'a). pochhammer (- x)"
   3.201 +  from b have bn0: "?p b n \<noteq> 0" unfolding pochhammer_eq_0_iff by simp
   3.202 +  {fix k assume kn: "k \<in> {0..n}"
   3.203 +    {assume c:"pochhammer (b - of_nat n + 1) n = 0"
   3.204 +      then obtain j where j: "j < n" "b - of_nat n + 1 = - of_nat j"
   3.205 +	unfolding pochhammer_eq_0_iff by blast
   3.206 +      from j have "b = of_nat n - of_nat j - of_nat 1" 
   3.207 +	by (simp add: algebra_simps)
   3.208 +      then have "b = of_nat (n - j - 1)" 
   3.209 +	using j kn by (simp add: of_nat_diff)
   3.210 +      with b have False using j by auto}
   3.211 +    then have nz: "pochhammer (1 + b - of_nat n) n \<noteq> 0" 
   3.212 +      by (auto simp add: algebra_simps)
   3.213 +    
   3.214 +    from nz kn have nz': "pochhammer (1 + b - of_nat n) k \<noteq> 0" 
   3.215 +      by (simp add: pochhammer_neq_0_mono)
   3.216 +    {assume k0: "k = 0 \<or> n =0" 
   3.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)" 
   3.218 +	using kn
   3.219 +	by (cases "k=0", simp_all add: gbinomial_pochhammer)}
   3.220 +    moreover
   3.221 +    {assume n0: "n \<noteq> 0" and k0: "k \<noteq> 0" 
   3.222 +      then obtain m where m: "n = Suc m" by (cases n, auto)
   3.223 +      from k0 obtain h where h: "k = Suc h" by (cases k, auto)
   3.224 +      {assume kn: "k = n"
   3.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)"
   3.226 +	  using kn pochhammer_minus'[where k=k and n=n and b=b]
   3.227 +	  apply (simp add:  pochhammer_same)
   3.228 +	  using bn0
   3.229 +	  by (simp add: field_simps power_add[symmetric])}
   3.230 +      moreover
   3.231 +      {assume nk: "k \<noteq> n"
   3.232 +	have m1nk: "?m1 n = setprod (%i. - 1) {0..m}" 
   3.233 +	  "?m1 k = setprod (%i. - 1) {0..h}"
   3.234 +	  by (simp_all add: setprod_constant m h)
   3.235 +	from kn nk have kn': "k < n" by simp
   3.236 +	have bnz0: "pochhammer (b - of_nat n + 1) k \<noteq> 0"
   3.237 +	  using bn0 kn 
   3.238 +	  unfolding pochhammer_eq_0_iff
   3.239 +	  apply auto
   3.240 +	  apply (erule_tac x= "n - ka - 1" in allE)
   3.241 +	  by (auto simp add: algebra_simps of_nat_diff)
   3.242 +	have eq1: "setprod (%k. (1::'a) + of_nat m - of_nat k) {0 .. h} = setprod of_nat {Suc (m - h) .. Suc m}"	
   3.243 +	  apply (rule strong_setprod_reindex_cong[where f="%k. Suc m - k "])
   3.244 +	  using kn' h m
   3.245 +	  apply (auto simp add: inj_on_def image_def)
   3.246 +	  apply (rule_tac x="Suc m - x" in bexI)
   3.247 +	  apply (simp_all add: of_nat_diff)
   3.248 +	  done
   3.249 +	
   3.250 +	have th1: "(?m1 k * ?p (of_nat n) k) / ?f n = 1 / of_nat(fact (n - k))"
   3.251 +	  unfolding m1nk 
   3.252 +	  
   3.253 +	  unfolding m h pochhammer_Suc_setprod
   3.254 +	  apply (simp add: field_simps del: fact_Suc id_def)
   3.255 +	  unfolding fact_setprod id_def
   3.256 +	  unfolding of_nat_setprod
   3.257 +	  unfolding setprod_timesf[symmetric]
   3.258 +	  apply auto
   3.259 +	  unfolding eq1
   3.260 +	  apply (subst setprod_Un_disjoint[symmetric])
   3.261 +	  apply (auto)
   3.262 +	  apply (rule setprod_cong)
   3.263 +	  apply auto
   3.264 +	  done
   3.265 +	have th20: "?m1 n * ?p b n = setprod (%i. b - of_nat i) {0..m}"
   3.266 +	  unfolding m1nk 
   3.267 +	  unfolding m h pochhammer_Suc_setprod
   3.268 +	  unfolding setprod_timesf[symmetric]
   3.269 +	  apply (rule setprod_cong)
   3.270 +	  apply auto
   3.271 +	  done
   3.272 +	have th21:"pochhammer (b - of_nat n + 1) k = setprod (%i. b - of_nat i) {n - k .. n - 1}"
   3.273 +	  unfolding h m 
   3.274 +	  unfolding pochhammer_Suc_setprod
   3.275 +	  apply (rule strong_setprod_reindex_cong[where f="%k. n - 1 - k"])
   3.276 +	  using kn
   3.277 +	  apply (auto simp add: inj_on_def m h image_def)
   3.278 +	  apply (rule_tac x= "m - x" in bexI)
   3.279 +	  by (auto simp add: of_nat_diff)
   3.280 +	
   3.281 +	have "?m1 n * ?p b n = pochhammer (b - of_nat n + 1) k * setprod (%i. b - of_nat i) {0.. n - k - 1}"
   3.282 +	  unfolding th20 th21
   3.283 +	  unfolding h m
   3.284 +	  apply (subst setprod_Un_disjoint[symmetric])
   3.285 +	  using kn' h m
   3.286 +	  apply auto
   3.287 +	  apply (rule setprod_cong)
   3.288 +	  apply auto
   3.289 +	  done
   3.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}" 
   3.291 +	  using nz' by (simp add: field_simps)
   3.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)"
   3.293 +	  using bnz0
   3.294 +	  by (simp add: field_simps)
   3.295 +	also have "\<dots> = b gchoose (n - k)" 
   3.296 +	  unfolding th1 th2
   3.297 +	  using kn' by (simp add: gbinomial_def)
   3.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}
   3.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)"
   3.300 +	by (cases "k =n", auto)}
   3.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 "
   3.302 +      using nz' 
   3.303 +      apply (cases "n=0", auto)
   3.304 +      by (cases "k", auto)}
   3.305 +  note th00 = this
   3.306 +  have "?r = ((a + b) gchoose n) * (of_nat (fact n)/ (?m1 n * pochhammer (- b) n))"
   3.307 +    unfolding gbinomial_pochhammer 
   3.308 +    using bn0 by (auto simp add: field_simps)
   3.309 +  also have "\<dots> = ?l"
   3.310 +    unfolding gbinomial_Vandermonde[symmetric]
   3.311 +    apply (simp add: th00)
   3.312 +    unfolding gbinomial_pochhammer
   3.313 +    using bn0 apply (simp add: setsum_left_distrib setsum_right_distrib field_simps)
   3.314 +    apply (rule setsum_cong2)
   3.315 +    apply (drule th00(2))
   3.316 +    by (simp add: field_simps power_add[symmetric])
   3.317 +  finally show ?thesis by simp
   3.318 +qed 
   3.319 +
   3.320 +    
   3.321 +lemma Vandermonde_pochhammer:
   3.322 +   fixes a :: "'a::field_char_0"
   3.323 +  assumes c: "ALL i : {0..< n}. c \<noteq> - of_nat i"
   3.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"
   3.325 +proof-
   3.326 +  let ?a = "- a"
   3.327 +  let ?b = "c + of_nat n - 1"
   3.328 +  have h: "\<forall> j \<in>{0..< n}. ?b \<noteq> of_nat j" using c
   3.329 +    apply (auto simp add: algebra_simps of_nat_diff)
   3.330 +    apply (erule_tac x= "n - j - 1" in ballE)
   3.331 +    by (auto simp add: of_nat_diff algebra_simps)
   3.332 +  have th0: "pochhammer (- (?a + ?b)) n = (- 1)^n * pochhammer (c - a) n"
   3.333 +    unfolding pochhammer_minus[OF le_refl]
   3.334 +    by (simp add: algebra_simps)
   3.335 +  have th1: "pochhammer (- ?b) n = (- 1)^n * pochhammer c n"
   3.336 +    unfolding pochhammer_minus[OF le_refl]
   3.337 +    by simp
   3.338 +  have nz: "pochhammer c n \<noteq> 0" using c
   3.339 +    by (simp add: pochhammer_eq_0_iff)
   3.340 +  from Vandermonde_pochhammer_lemma[where a = "?a" and b="?b" and n=n, OF h, unfolded th0 th1]
   3.341 +  show ?thesis using nz by (simp add: field_simps setsum_right_distrib)
   3.342 +qed
   3.343 +
   3.344  subsubsection{* Formal trigonometric functions  *}
   3.345  
   3.346  definition "fps_sin (c::'a::field_char_0) =
   3.347 @@ -2866,4 +3160,171 @@
   3.348      by simp
   3.349  qed
   3.350  
   3.351 +text {* Connection to E c over the complex numbers --- Euler and De Moivre*}
   3.352 +lemma Eii_sin_cos:
   3.353 +  "E (ii * c) = fps_cos c + fps_const ii * fps_sin c "
   3.354 +  (is "?l = ?r")
   3.355 +proof-
   3.356 +  {fix n::nat
   3.357 +    {assume en: "even n"
   3.358 +      from en obtain m where m: "n = 2*m" 
   3.359 +	unfolding even_mult_two_ex by blast
   3.360 +      
   3.361 +      have "?l $n = ?r$n" 
   3.362 +	by (simp add: m fps_sin_def fps_cos_def power_mult_distrib
   3.363 +	  power_mult power_minus)}
   3.364 +    moreover
   3.365 +    {assume on: "odd n"
   3.366 +      from on obtain m where m: "n = 2*m + 1" 
   3.367 +	unfolding odd_nat_equiv_def2 by (auto simp add: nat_mult_2)  
   3.368 +      have "?l $n = ?r$n" 
   3.369 +	by (simp add: m fps_sin_def fps_cos_def power_mult_distrib
   3.370 +	  power_mult power_minus)}
   3.371 +    ultimately have "?l $n = ?r$n"  by blast}
   3.372 +  then show ?thesis by (simp add: fps_eq_iff)
   3.373 +qed
   3.374 +
   3.375 +lemma E_minus_ii_sin_cos: "E (- (ii * c)) = fps_cos c - fps_const ii * fps_sin c "
   3.376 +  unfolding minus_mult_right Eii_sin_cos by (simp add: fps_sin_even fps_cos_odd)
   3.377 +
   3.378 +lemma fps_const_minus: "fps_const (c::'a::group_add) - fps_const d = fps_const (c - d)"
   3.379 +  by (simp add: fps_eq_iff fps_const_def)
   3.380 +
   3.381 +lemma fps_number_of_fps_const: "number_of i = fps_const (number_of i :: 'a:: {comm_ring_1, number_ring})"
   3.382 +  apply (subst (2) number_of_eq)
   3.383 +apply(rule int_induct[of _ 0])
   3.384 +apply (simp_all add: number_of_fps_def)
   3.385 +by (simp_all add: fps_const_add[symmetric] fps_const_minus[symmetric])
   3.386 +
   3.387 +lemma fps_cos_Eii:
   3.388 +  "fps_cos c = (E (ii * c) + E (- ii * c)) / fps_const 2"
   3.389 +proof-
   3.390 +  have th: "fps_cos c + fps_cos c = fps_cos c * fps_const 2" 
   3.391 +    by (simp add: fps_eq_iff fps_number_of_fps_const complex_number_of_def[symmetric])
   3.392 +  show ?thesis
   3.393 +  unfolding Eii_sin_cos minus_mult_commute
   3.394 +  by (simp add: fps_sin_even fps_cos_odd fps_number_of_fps_const
   3.395 +    fps_divide_def fps_const_inverse th complex_number_of_def[symmetric])
   3.396 +qed
   3.397 +
   3.398 +lemma fps_sin_Eii:
   3.399 +  "fps_sin c = (E (ii * c) - E (- ii * c)) / fps_const (2*ii)"
   3.400 +proof-
   3.401 +  have th: "fps_const \<i> * fps_sin c + fps_const \<i> * fps_sin c = fps_sin c * fps_const (2 * ii)" 
   3.402 +    by (simp add: fps_eq_iff fps_number_of_fps_const complex_number_of_def[symmetric])
   3.403 +  show ?thesis
   3.404 +  unfolding Eii_sin_cos minus_mult_commute
   3.405 +  by (simp add: fps_sin_even fps_cos_odd fps_divide_def fps_const_inverse th)
   3.406 +qed
   3.407 +
   3.408 +lemma fps_tan_Eii:
   3.409 +  "fps_tan c = (E (ii * c) - E (- ii * c)) / (fps_const ii * (E (ii * c) + E (- ii * c)))"
   3.410 +  unfolding fps_tan_def fps_sin_Eii fps_cos_Eii mult_minus_left E_neg
   3.411 +  apply (simp add: fps_divide_def fps_inverse_mult fps_const_mult[symmetric] fps_const_inverse del: fps_const_mult)
   3.412 +  by simp
   3.413 +
   3.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)"
   3.415 +  unfolding Eii_sin_cos[symmetric] E_power_mult
   3.416 +  by (simp add: mult_ac)
   3.417 +
   3.418 +subsection {* Hypergeometric series *}
   3.419 +
   3.420 +
   3.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)))"
   3.422 +
   3.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))"
   3.424 +  by (simp add: F_def)
   3.425 +
   3.426 +lemma foldl_mult_start:
   3.427 +  "foldl (%r x. r * f x) (v::'a::comm_ring_1) as * x = foldl (%r x. r * f x) (v * x) as "
   3.428 +  by (induct as arbitrary: x v, auto simp add: algebra_simps)
   3.429 +
   3.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"
   3.431 +  by (induct as arbitrary: v, auto simp add: foldl_mult_start)
   3.432 +
   3.433 +lemma F_nth_alt: "F as bs c $ n = foldr (\<lambda>a r. r * pochhammer a n) as (c ^ n) /
   3.434 +    foldr (\<lambda>b r. r * pochhammer b n) bs (of_nat (fact n))"
   3.435 +  by (simp add: foldl_mult_start foldr_mult_foldl)
   3.436 +
   3.437 +lemma F_E[simp]: "F [] [] c = E c" 
   3.438 +  by (simp add: fps_eq_iff)
   3.439 +
   3.440 +lemma F_1_0[simp]: "F [1] [] c = 1/(1 - fps_const c * X)"
   3.441 +proof-
   3.442 +  let ?a = "(Abs_fps (\<lambda>n. 1)) oo (fps_const c * X)"
   3.443 +  thm gp
   3.444 +  have th0: "(fps_const c * X) $ 0 = 0" by simp
   3.445 +  show ?thesis unfolding gp[OF th0, symmetric]
   3.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)
   3.447 +qed
   3.448 +
   3.449 +lemma F_B[simp]: "F [-a] [] (- 1) = fps_binomial a"
   3.450 +  by (simp add: fps_eq_iff gbinomial_pochhammer algebra_simps)
   3.451 +
   3.452 +lemma F_0[simp]: "F as bs c $0 = 1"
   3.453 +  apply simp
   3.454 +  apply (subgoal_tac "ALL as. foldl (%(r::'a) (a::'a). r) 1 as = 1")
   3.455 +  apply auto
   3.456 +  apply (induct_tac as, auto)
   3.457 +  done
   3.458 +
   3.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"
   3.460 +  by (induct as arbitrary: v w, auto simp add: algebra_simps)
   3.461 +
   3.462 +
   3.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"
   3.464 +  apply (simp del: of_nat_Suc of_nat_add fact_Suc)
   3.465 +  apply (simp add: foldl_mult_start del: fact_Suc of_nat_Suc)
   3.466 +  unfolding foldl_prod_prod[unfolded foldl_mult_start] pochhammer_Suc
   3.467 +  by (simp add: algebra_simps of_nat_mult)
   3.468 +
   3.469 +lemma XD_nth[simp]: "XD a $ n = (if n=0 then 0 else of_nat n * a$n)"
   3.470 +  by (simp add: XD_def)
   3.471 +
   3.472 +lemma XD_0th[simp]: "XD a $ 0 = 0" by simp
   3.473 +lemma XD_Suc[simp]:" XD a $ Suc n = of_nat (Suc n) * a $ Suc n" by simp
   3.474 +
   3.475 +definition "XDp c a = XD a + fps_const c * a"
   3.476 +
   3.477 +lemma XDp_nth[simp]: "XDp c a $ n = (c + of_nat n) * a$n"
   3.478 +  by (simp add: XDp_def algebra_simps)
   3.479 +
   3.480 +lemma XDp_commute:
   3.481 +  shows "XDp b o XDp (c::'a::comm_ring_1) = XDp c o XDp b"
   3.482 +  by (auto simp add: XDp_def expand_fun_eq fps_eq_iff algebra_simps)
   3.483 +
   3.484 +lemma XDp0[simp]: "XDp 0 = XD"
   3.485 +  by (simp add: expand_fun_eq fps_eq_iff)
   3.486 +
   3.487 +lemma XDp_fps_integral[simp]:"XDp 0 (fps_integral a c) = X * a"
   3.488 +  by (simp add: fps_eq_iff fps_integral_def)
   3.489 +
   3.490 +lemma F_minus_nat: 
   3.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 /
   3.492 +    (pochhammer (- of_nat (n + m)) k * of_nat (fact k)) else 0)"
   3.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 /
   3.494 +    (pochhammer (- of_nat (m + n)) k * of_nat (fact k)) else 0)"
   3.495 +  by (auto simp add: pochhammer_eq_0_iff)
   3.496 +
   3.497 +lemma setsum_eq_if: "setsum f {(n::nat) .. m} = (if m < n then 0 else f n + setsum f {n+1 .. m})"
   3.498 +  apply simp
   3.499 +  apply (subst setsum_insert[symmetric])
   3.500 +  by (auto simp add: not_less setsum_head_Suc)
   3.501 +
   3.502 +lemma pochhammer_rec_if: 
   3.503 +  "pochhammer a n = (if n = 0 then 1 else a * pochhammer (a + 1) (n - 1))"
   3.504 +  by (cases n, simp_all add: pochhammer_rec)
   3.505 +
   3.506 +lemma XDp_foldr_nth[simp]: "foldr (%c r. XDp c o r) cs (%c. XDp c a) c0 $ n = 
   3.507 +  foldr (%c r. (c + of_nat n) * r) cs (c0 + of_nat n) * a$n"
   3.508 +  by (induct cs arbitrary: c0, auto simp add: algebra_simps)
   3.509 +
   3.510 +lemma genric_XDp_foldr_nth:
   3.511 +  assumes 
   3.512 +  f: "ALL n c a. f c a $ n = (of_nat n + k c) * a$n"
   3.513 +
   3.514 +  shows "foldr (%c r. f c o r) cs (%c. g c a) c0 $ n = 
   3.515 +  foldr (%c r. (k c + of_nat n) * r) cs (g c0 a $ n)"
   3.516 +  by (induct cs arbitrary: c0, auto simp add: algebra_simps f )
   3.517 +
   3.518  end
     4.1 --- a/src/HOL/ex/Formal_Power_Series_Examples.thy	Thu Jul 23 20:05:20 2009 +0200
     4.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     4.3 @@ -1,303 +0,0 @@
     4.4 -(*  Title:      Formal_Power_Series_Examples.thy
     4.5 -    ID:         
     4.6 -    Author:     Amine Chaieb, University of Cambridge
     4.7 -*)
     4.8 -
     4.9 -header{* Some applications of formal power series and some properties over complex numbers*}
    4.10 -
    4.11 -theory Formal_Power_Series_Examples
    4.12 -  imports Formal_Power_Series Binomial 
    4.13 -begin
    4.14 -
    4.15 -section{* The generalized binomial theorem *}
    4.16 -lemma gbinomial_theorem: 
    4.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))"
    4.18 -proof-
    4.19 -  from E_add_mult[of a b] 
    4.20 -  have "(E (a + b)) $ n = (E a * E b)$n" by simp
    4.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))))"
    4.22 -    by (simp add: field_simps fps_mult_nth of_nat_mult[symmetric] setsum_right_distrib)
    4.23 -  then show ?thesis 
    4.24 -    apply simp
    4.25 -    apply (rule setsum_cong2)
    4.26 -    apply simp
    4.27 -    apply (frule binomial_fact[where ?'a = 'a, symmetric])
    4.28 -    by (simp add: field_simps of_nat_mult)
    4.29 -qed
    4.30 -
    4.31 -text{* And the nat-form -- also available from Binomial.thy *}
    4.32 -lemma binomial_theorem: "(a+b) ^ n = (\<Sum>k=0..n. (n choose k) * a^k * b^(n-k))"
    4.33 -  using gbinomial_theorem[of "of_nat a" "of_nat b" n]
    4.34 -  unfolding of_nat_add[symmetric] of_nat_power[symmetric] of_nat_mult[symmetric] of_nat_setsum[symmetric]
    4.35 -  by simp
    4.36 -
    4.37 -section {* The binomial series and Vandermonde's identity *}
    4.38 -definition "fps_binomial a = Abs_fps (\<lambda>n. a gchoose n)"
    4.39 -
    4.40 -lemma fps_binomial_nth[simp]: "fps_binomial a $ n = a gchoose n"
    4.41 -  by (simp add: fps_binomial_def)
    4.42 -
    4.43 -lemma fps_binomial_ODE_unique:
    4.44 -  fixes c :: "'a::field_char_0"
    4.45 -  shows "fps_deriv a = (fps_const c * a) / (1 + X) \<longleftrightarrow> a = fps_const (a$0) * fps_binomial c"
    4.46 -  (is "?lhs \<longleftrightarrow> ?rhs")
    4.47 -proof-
    4.48 -  let ?da = "fps_deriv a"
    4.49 -  let ?x1 = "(1 + X):: 'a fps"
    4.50 -  let ?l = "?x1 * ?da"
    4.51 -  let ?r = "fps_const c * a"
    4.52 -  have x10: "?x1 $ 0 \<noteq> 0" by simp
    4.53 -  have "?l = ?r \<longleftrightarrow> inverse ?x1 * ?l = inverse ?x1 * ?r" by simp
    4.54 -  also have "\<dots> \<longleftrightarrow> ?da = (fps_const c * a) / ?x1"
    4.55 -    apply (simp only: fps_divide_def  mult_assoc[symmetric] inverse_mult_eq_1[OF x10])
    4.56 -    by (simp add: ring_simps)
    4.57 -  finally have eq: "?l = ?r \<longleftrightarrow> ?lhs" by simp
    4.58 -  moreover
    4.59 -  {assume h: "?l = ?r" 
    4.60 -    {fix n
    4.61 -      from h have lrn: "?l $ n = ?r$n" by simp
    4.62 -      
    4.63 -      from lrn 
    4.64 -      have "a$ Suc n = ((c - of_nat n) / of_nat (Suc n)) * a $n" 
    4.65 -	apply (simp add: ring_simps del: of_nat_Suc)
    4.66 -	by (cases n, simp_all add: field_simps del: of_nat_Suc)
    4.67 -    }
    4.68 -    note th0 = this
    4.69 -    {fix n have "a$n = (c gchoose n) * a$0"
    4.70 -      proof(induct n)
    4.71 -	case 0 thus ?case by simp
    4.72 -      next
    4.73 -	case (Suc m)
    4.74 -	thus ?case unfolding th0
    4.75 -	  apply (simp add: field_simps del: of_nat_Suc)
    4.76 -	  unfolding mult_assoc[symmetric] gbinomial_mult_1
    4.77 -	  by (simp add: ring_simps)
    4.78 -      qed}
    4.79 -    note th1 = this
    4.80 -    have ?rhs
    4.81 -      apply (simp add: fps_eq_iff)
    4.82 -      apply (subst th1)
    4.83 -      by (simp add: ring_simps)}
    4.84 -  moreover
    4.85 -  {assume h: ?rhs
    4.86 -  have th00:"\<And>x y. x * (a$0 * y) = a$0 * (x*y)" by (simp add: mult_commute)
    4.87 -    have "?l = ?r" 
    4.88 -      apply (subst h)
    4.89 -      apply (subst (2) h)
    4.90 -      apply (clarsimp simp add: fps_eq_iff ring_simps)
    4.91 -      unfolding mult_assoc[symmetric] th00 gbinomial_mult_1
    4.92 -      by (simp add: ring_simps gbinomial_mult_1)}
    4.93 -  ultimately show ?thesis by blast
    4.94 -qed
    4.95 -
    4.96 -lemma fps_binomial_deriv: "fps_deriv (fps_binomial c) = fps_const c * fps_binomial c / (1 + X)"
    4.97 -proof-
    4.98 -  let ?a = "fps_binomial c"
    4.99 -  have th0: "?a = fps_const (?a$0) * ?a" by (simp)
   4.100 -  from iffD2[OF fps_binomial_ODE_unique, OF th0] show ?thesis .
   4.101 -qed
   4.102 -
   4.103 -lemma fps_binomial_add_mult: "fps_binomial (c+d) = fps_binomial c * fps_binomial d" (is "?l = ?r")
   4.104 -proof-
   4.105 -  let ?P = "?r - ?l"
   4.106 -  let ?b = "fps_binomial"
   4.107 -  let ?db = "\<lambda>x. fps_deriv (?b x)"
   4.108 -  have "fps_deriv ?P = ?db c * ?b d + ?b c * ?db d - ?db (c + d)"  by simp
   4.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))"
   4.110 -    unfolding fps_binomial_deriv
   4.111 -    by (simp add: fps_divide_def ring_simps)
   4.112 -  also have "\<dots> = (fps_const (c + d)/ (1 + X)) * ?P"
   4.113 -    by (simp add: ring_simps fps_divide_def fps_const_add[symmetric] del: fps_const_add)
   4.114 -  finally have th0: "fps_deriv ?P = fps_const (c+d) * ?P / (1 + X)"
   4.115 -    by (simp add: fps_divide_def)
   4.116 -  have "?P = fps_const (?P$0) * ?b (c + d)"
   4.117 -    unfolding fps_binomial_ODE_unique[symmetric]
   4.118 -    using th0 by simp
   4.119 -  hence "?P = 0" by (simp add: fps_mult_nth)
   4.120 -  then show ?thesis by simp
   4.121 -qed
   4.122 -
   4.123 -lemma fps_minomial_minus_one: "fps_binomial (- 1) = inverse (1 + X)"
   4.124 -  (is "?l = inverse ?r")
   4.125 -proof-
   4.126 -  have th: "?r$0 \<noteq> 0" by simp
   4.127 -  have th': "fps_deriv (inverse ?r) = fps_const (- 1) * inverse ?r / (1 + X)"
   4.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)
   4.129 -  have eq: "inverse ?r $ 0 = 1"
   4.130 -    by (simp add: fps_inverse_def)
   4.131 -  from iffD1[OF fps_binomial_ODE_unique[of "inverse (1 + X)" "- 1"] th'] eq
   4.132 -  show ?thesis by (simp add: fps_inverse_def)
   4.133 -qed
   4.134 -
   4.135 -lemma gbinomial_Vandermond: "setsum (\<lambda>k. (a gchoose k) * (b gchoose (n - k))) {0..n} = (a + b) gchoose n"
   4.136 -proof-
   4.137 -  let ?ba = "fps_binomial a"
   4.138 -  let ?bb = "fps_binomial b"
   4.139 -  let ?bab = "fps_binomial (a + b)"
   4.140 -  from fps_binomial_add_mult[of a b] have "?bab $ n = (?ba * ?bb)$n" by simp
   4.141 -  then show ?thesis by (simp add: fps_mult_nth)
   4.142 -qed
   4.143 -
   4.144 -lemma binomial_Vandermond: "setsum (\<lambda>k. (a choose k) * (b choose (n - k))) {0..n} = (a + b) choose n"
   4.145 -  using gbinomial_Vandermond[of "(of_nat a)" "of_nat b" n]
   4.146 -  
   4.147 -  apply (simp only: binomial_gbinomial[symmetric] of_nat_mult[symmetric] of_nat_setsum[symmetric] of_nat_add[symmetric])
   4.148 -  by simp
   4.149 -
   4.150 -lemma binomial_symmetric: assumes kn: "k \<le> n" 
   4.151 -  shows "n choose k = n choose (n - k)"
   4.152 -proof-
   4.153 -  from kn have kn': "n - k \<le> n" by arith
   4.154 -  from binomial_fact_lemma[OF kn] binomial_fact_lemma[OF kn']
   4.155 -  have "fact k * fact (n - k) * (n choose k) = fact (n - k) * fact (n - (n - k)) * (n choose (n - k))" by simp
   4.156 -  then show ?thesis using kn by simp
   4.157 -qed
   4.158 -  
   4.159 -lemma binomial_Vandermond_same: "setsum (\<lambda>k. (n choose k)^2) {0..n} = (2*n) choose n"
   4.160 -  using binomial_Vandermond[of n n n,symmetric]
   4.161 -  unfolding nat_mult_2 apply (simp add: power2_eq_square)
   4.162 -  apply (rule setsum_cong2)
   4.163 -  by (auto intro:  binomial_symmetric)
   4.164 -
   4.165 -section {* Relation between formal sine/cosine and the exponential FPS*}
   4.166 -lemma Eii_sin_cos:
   4.167 -  "E (ii * c) = fps_cos c + fps_const ii * fps_sin c "
   4.168 -  (is "?l = ?r")
   4.169 -proof-
   4.170 -  {fix n::nat
   4.171 -    {assume en: "even n"
   4.172 -      from en obtain m where m: "n = 2*m" 
   4.173 -	unfolding even_mult_two_ex by blast
   4.174 -      
   4.175 -      have "?l $n = ?r$n" 
   4.176 -	by (simp add: m fps_sin_def fps_cos_def power_mult_distrib
   4.177 -	  power_mult power_minus)}
   4.178 -    moreover
   4.179 -    {assume on: "odd n"
   4.180 -      from on obtain m where m: "n = 2*m + 1" 
   4.181 -	unfolding odd_nat_equiv_def2 by (auto simp add: nat_mult_2)  
   4.182 -      have "?l $n = ?r$n" 
   4.183 -	by (simp add: m fps_sin_def fps_cos_def power_mult_distrib
   4.184 -	  power_mult power_minus)}
   4.185 -    ultimately have "?l $n = ?r$n"  by blast}
   4.186 -  then show ?thesis by (simp add: fps_eq_iff)
   4.187 -qed
   4.188 -
   4.189 -lemma E_minus_ii_sin_cos: "E (- (ii * c)) = fps_cos c - fps_const ii * fps_sin c "
   4.190 -  unfolding minus_mult_right Eii_sin_cos by (simp add: fps_sin_even fps_cos_odd)
   4.191 -
   4.192 -lemma fps_const_minus: "fps_const (c::'a::group_add) - fps_const d = fps_const (c - d)"
   4.193 -  by (simp add: fps_eq_iff fps_const_def)
   4.194 -
   4.195 -lemma fps_number_of_fps_const: "number_of i = fps_const (number_of i :: 'a:: {comm_ring_1, number_ring})"
   4.196 -  apply (subst (2) number_of_eq)
   4.197 -apply(rule int_induct[of _ 0])
   4.198 -apply (simp_all add: number_of_fps_def)
   4.199 -by (simp_all add: fps_const_add[symmetric] fps_const_minus[symmetric])
   4.200 -
   4.201 -lemma fps_cos_Eii:
   4.202 -  "fps_cos c = (E (ii * c) + E (- ii * c)) / fps_const 2"
   4.203 -proof-
   4.204 -  have th: "fps_cos c + fps_cos c = fps_cos c * fps_const 2" 
   4.205 -    by (simp add: fps_eq_iff fps_number_of_fps_const complex_number_of_def[symmetric])
   4.206 -  show ?thesis
   4.207 -  unfolding Eii_sin_cos minus_mult_commute
   4.208 -  by (simp add: fps_sin_even fps_cos_odd fps_number_of_fps_const
   4.209 -    fps_divide_def fps_const_inverse th complex_number_of_def[symmetric])
   4.210 -qed
   4.211 -
   4.212 -lemma fps_sin_Eii:
   4.213 -  "fps_sin c = (E (ii * c) - E (- ii * c)) / fps_const (2*ii)"
   4.214 -proof-
   4.215 -  have th: "fps_const \<i> * fps_sin c + fps_const \<i> * fps_sin c = fps_sin c * fps_const (2 * ii)" 
   4.216 -    by (simp add: fps_eq_iff fps_number_of_fps_const complex_number_of_def[symmetric])
   4.217 -  show ?thesis
   4.218 -  unfolding Eii_sin_cos minus_mult_commute
   4.219 -  by (simp add: fps_sin_even fps_cos_odd fps_divide_def fps_const_inverse th)
   4.220 -qed
   4.221 -
   4.222 -lemma fps_const_mult_2: "fps_const (2::'a::number_ring) * a = a +a"
   4.223 -  by (simp add: fps_eq_iff fps_number_of_fps_const)
   4.224 -
   4.225 -lemma fps_const_mult_2_right: "a * fps_const (2::'a::number_ring) = a +a"
   4.226 -  by (simp add: fps_eq_iff fps_number_of_fps_const)
   4.227 -
   4.228 -lemma fps_tan_Eii:
   4.229 -  "fps_tan c = (E (ii * c) - E (- ii * c)) / (fps_const ii * (E (ii * c) + E (- ii * c)))"
   4.230 -  unfolding fps_tan_def fps_sin_Eii fps_cos_Eii mult_minus_left E_neg
   4.231 -  apply (simp add: fps_divide_def fps_inverse_mult fps_const_mult[symmetric] fps_const_inverse del: fps_const_mult)
   4.232 -  by simp
   4.233 -
   4.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)"
   4.235 -  unfolding Eii_sin_cos[symmetric] E_power_mult
   4.236 -  by (simp add: mult_ac)
   4.237 -
   4.238 -text{* Now some trigonometric identities *}
   4.239 -
   4.240 -lemma fps_sin_add: 
   4.241 -  "fps_sin (a+b) = fps_sin (a::complex) * fps_cos b + fps_cos a * fps_sin b"
   4.242 -proof-
   4.243 -  let ?ca = "fps_cos a"
   4.244 -  let ?cb = "fps_cos b"
   4.245 -  let ?sa = "fps_sin a"
   4.246 -  let ?sb = "fps_sin b"
   4.247 -  let ?i = "fps_const ii"
   4.248 -  have i: "?i*?i = fps_const -1" by simp
   4.249 -  have "fps_sin (a + b) = 
   4.250 -    ((?ca + ?i * ?sa) * (?cb + ?i*?sb) - (?ca - ?i*?sa) * (?cb - ?i*?sb)) *
   4.251 -    fps_const (- (\<i> / 2))"
   4.252 -    apply(simp add: fps_sin_Eii[of "a+b"] fps_divide_def minus_mult_commute)
   4.253 -    unfolding right_distrib
   4.254 -    apply (simp add: Eii_sin_cos E_minus_ii_sin_cos fps_const_inverse E_add_mult)
   4.255 -    by (simp add: ring_simps)
   4.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)"
   4.257 -    by (simp add: ring_simps)
   4.258 -  also have "\<dots> = (fps_const 2 * ?i * (?ca * ?sb + ?sa * ?cb)) * fps_const (- ii/2)"
   4.259 -    apply simp
   4.260 -  apply (simp add: ring_simps)
   4.261 -    apply (simp add:  ring_simps add: fps_const_mult[symmetric] del:fps_const_mult)
   4.262 -    unfolding fps_const_mult_2_right
   4.263 -    by (simp add: ring_simps)
   4.264 -  also have "\<dots> = (fps_const 2 * ?i * fps_const (- ii/2)) * (?ca * ?sb + ?sa * ?cb)"
   4.265 -    by (simp only: mult_ac)
   4.266 -  also have "\<dots> = ?sa * ?cb + ?ca*?sb"
   4.267 -    by simp
   4.268 -  finally show ?thesis .
   4.269 -qed
   4.270 -
   4.271 -lemma fps_cos_add: 
   4.272 -  "fps_cos (a+b) = fps_cos (a::complex) * fps_cos b - fps_sin a * fps_sin b"
   4.273 -proof-
   4.274 -  let ?ca = "fps_cos a"
   4.275 -  let ?cb = "fps_cos b"
   4.276 -  let ?sa = "fps_sin a"
   4.277 -  let ?sb = "fps_sin b"
   4.278 -  let ?i = "fps_const ii"
   4.279 -  have i: "?i*?i = fps_const -1" by simp
   4.280 -  have i': "\<And>x. ?i * (?i * x) = - x" 
   4.281 -    apply (simp add: mult_assoc[symmetric] i)
   4.282 -    by (simp add: fps_eq_iff)
   4.283 -  have m1: "\<And>x. x * fps_const (-1 ::complex) = - x" "\<And>x. fps_const (-1 :: complex) * x = - x"
   4.284 -    by (auto simp add: fps_eq_iff)
   4.285 -
   4.286 -  have "fps_cos (a + b) = 
   4.287 -    ((?ca + ?i * ?sa) * (?cb + ?i*?sb) + (?ca - ?i*?sa) * (?cb - ?i*?sb)) *
   4.288 -    fps_const (1/ 2)"
   4.289 -    apply(simp add: fps_cos_Eii[of "a+b"] fps_divide_def minus_mult_commute)
   4.290 -    unfolding right_distrib minus_add_distrib
   4.291 -    apply (simp add: Eii_sin_cos E_minus_ii_sin_cos fps_const_inverse E_add_mult)
   4.292 -    by (simp add: ring_simps)
   4.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)"
   4.294 -    apply simp
   4.295 -    by (simp add: ring_simps i' m1)
   4.296 -  also have "\<dots> = (fps_const 2 * (?ca * ?cb - ?sa * ?sb)) * fps_const (1/2)"
   4.297 -    apply simp
   4.298 -    by (simp add: ring_simps m1 fps_const_mult_2_right)
   4.299 -  also have "\<dots> = (fps_const 2 * fps_const (1/2)) * (?ca * ?cb - ?sa * ?sb)"
   4.300 -    by (simp only: mult_ac)
   4.301 -  also have "\<dots> = ?ca * ?cb - ?sa*?sb"
   4.302 -    by simp
   4.303 -  finally show ?thesis .
   4.304 -qed
   4.305 -
   4.306 -end