src/HOL/ex/Formal_Power_Series_Examples.thy
author nipkow
Fri Mar 06 17:38:47 2009 +0100 (2009-03-06)
changeset 30313 b2441b0c8d38
parent 29698 91feea8e41e4
child 30748 fe67d729a61c
permissions -rw-r--r--
added lemmas
     1 (*  Title:      Formal_Power_Series_Examples.thy
     2     ID:         
     3     Author:     Amine Chaieb, University of Cambridge
     4 *)
     5 
     6 header{* Some applications of formal power series and some properties over complex numbers*}
     7 
     8 theory Formal_Power_Series_Examples
     9   imports Formal_Power_Series Binomial Complex
    10 begin
    11 
    12 section{* The generalized binomial theorem *}
    13 lemma gbinomial_theorem: 
    14   "((a::'a::{ring_char_0, field, division_by_zero, recpower})+b) ^ n = (\<Sum>k=0..n. of_nat (n choose k) * a^k * b^(n-k))"
    15 proof-
    16   from E_add_mult[of a b] 
    17   have "(E (a + b)) $ n = (E a * E b)$n" by simp
    18   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))))"
    19     by (simp add: field_simps fps_mult_nth of_nat_mult[symmetric] setsum_right_distrib)
    20   then show ?thesis 
    21     apply simp
    22     apply (rule setsum_cong2)
    23     apply simp
    24     apply (frule binomial_fact[where ?'a = 'a, symmetric])
    25     by (simp add: field_simps of_nat_mult)
    26 qed
    27 
    28 text{* And the nat-form -- also available from Binomial.thy *}
    29 lemma binomial_theorem: "(a+b) ^ n = (\<Sum>k=0..n. (n choose k) * a^k * b^(n-k))"
    30   using gbinomial_theorem[of "of_nat a" "of_nat b" n]
    31   unfolding of_nat_add[symmetric] of_nat_power[symmetric] of_nat_mult[symmetric] of_nat_setsum[symmetric]
    32   by simp
    33 
    34 section {* The binomial series and Vandermonde's identity *}
    35 definition "fps_binomial a = Abs_fps (\<lambda>n. a gchoose n)"
    36 
    37 lemma fps_binomial_nth[simp]: "fps_binomial a $ n = a gchoose n"
    38   by (simp add: fps_binomial_def)
    39 
    40 lemma fps_binomial_ODE_unique:
    41   fixes c :: "'a::{field, recpower,ring_char_0}"
    42   shows "fps_deriv a = (fps_const c * a) / (1 + X) \<longleftrightarrow> a = fps_const (a$0) * fps_binomial c"
    43   (is "?lhs \<longleftrightarrow> ?rhs")
    44 proof-
    45   let ?da = "fps_deriv a"
    46   let ?x1 = "(1 + X):: 'a fps"
    47   let ?l = "?x1 * ?da"
    48   let ?r = "fps_const c * a"
    49   have x10: "?x1 $ 0 \<noteq> 0" by simp
    50   have "?l = ?r \<longleftrightarrow> inverse ?x1 * ?l = inverse ?x1 * ?r" by simp
    51   also have "\<dots> \<longleftrightarrow> ?da = (fps_const c * a) / ?x1"
    52     apply (simp only: fps_divide_def  mult_assoc[symmetric] inverse_mult_eq_1[OF x10])
    53     by (simp add: ring_simps)
    54   finally have eq: "?l = ?r \<longleftrightarrow> ?lhs" by simp
    55   moreover
    56   {assume h: "?l = ?r" 
    57     {fix n
    58       from h have lrn: "?l $ n = ?r$n" by simp
    59       
    60       from lrn 
    61       have "a$ Suc n = ((c - of_nat n) / of_nat (Suc n)) * a $n" 
    62 	apply (simp add: ring_simps del: of_nat_Suc)
    63 	by (cases n, simp_all add: field_simps del: of_nat_Suc)
    64     }
    65     note th0 = this
    66     {fix n have "a$n = (c gchoose n) * a$0"
    67       proof(induct n)
    68 	case 0 thus ?case by simp
    69       next
    70 	case (Suc m)
    71 	thus ?case unfolding th0
    72 	  apply (simp add: field_simps del: of_nat_Suc)
    73 	  unfolding mult_assoc[symmetric] gbinomial_mult_1
    74 	  by (simp add: ring_simps)
    75       qed}
    76     note th1 = this
    77     have ?rhs
    78       apply (simp add: fps_eq_iff)
    79       apply (subst th1)
    80       by (simp add: ring_simps)}
    81   moreover
    82   {assume h: ?rhs
    83   have th00:"\<And>x y. x * (a$0 * y) = a$0 * (x*y)" by (simp add: mult_commute)
    84     have "?l = ?r" 
    85       apply (subst h)
    86       apply (subst (2) h)
    87       apply (clarsimp simp add: fps_eq_iff ring_simps)
    88       unfolding mult_assoc[symmetric] th00 gbinomial_mult_1
    89       by (simp add: ring_simps gbinomial_mult_1)}
    90   ultimately show ?thesis by blast
    91 qed
    92 
    93 lemma fps_binomial_deriv: "fps_deriv (fps_binomial c) = fps_const c * fps_binomial c / (1 + X)"
    94 proof-
    95   let ?a = "fps_binomial c"
    96   have th0: "?a = fps_const (?a$0) * ?a" by (simp)
    97   from iffD2[OF fps_binomial_ODE_unique, OF th0] show ?thesis .
    98 qed
    99 
   100 lemma fps_binomial_add_mult: "fps_binomial (c+d) = fps_binomial c * fps_binomial d" (is "?l = ?r")
   101 proof-
   102   let ?P = "?r - ?l"
   103   let ?b = "fps_binomial"
   104   let ?db = "\<lambda>x. fps_deriv (?b x)"
   105   have "fps_deriv ?P = ?db c * ?b d + ?b c * ?db d - ?db (c + d)"  by simp
   106   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))"
   107     unfolding fps_binomial_deriv
   108     by (simp add: fps_divide_def ring_simps)
   109   also have "\<dots> = (fps_const (c + d)/ (1 + X)) * ?P"
   110     by (simp add: ring_simps fps_divide_def fps_const_add[symmetric] del: fps_const_add)
   111   finally have th0: "fps_deriv ?P = fps_const (c+d) * ?P / (1 + X)"
   112     by (simp add: fps_divide_def)
   113   have "?P = fps_const (?P$0) * ?b (c + d)"
   114     unfolding fps_binomial_ODE_unique[symmetric]
   115     using th0 by simp
   116   hence "?P = 0" by (simp add: fps_mult_nth)
   117   then show ?thesis by simp
   118 qed
   119 
   120 lemma fps_minomial_minus_one: "fps_binomial (- 1) = inverse (1 + X)"
   121   (is "?l = inverse ?r")
   122 proof-
   123   have th: "?r$0 \<noteq> 0" by simp
   124   have th': "fps_deriv (inverse ?r) = fps_const (- 1) * inverse ?r / (1 + X)"
   125     by (simp add: fps_inverse_deriv[OF th] fps_divide_def power2_eq_square mult_commute fps_const_neg[symmetric] del: fps_const_neg)
   126   have eq: "inverse ?r $ 0 = 1"
   127     by (simp add: fps_inverse_def)
   128   from iffD1[OF fps_binomial_ODE_unique[of "inverse (1 + X)" "- 1"] th'] eq
   129   show ?thesis by (simp add: fps_inverse_def)
   130 qed
   131 
   132 lemma gbinomial_Vandermond: "setsum (\<lambda>k. (a gchoose k) * (b gchoose (n - k))) {0..n} = (a + b) gchoose n"
   133 proof-
   134   let ?ba = "fps_binomial a"
   135   let ?bb = "fps_binomial b"
   136   let ?bab = "fps_binomial (a + b)"
   137   from fps_binomial_add_mult[of a b] have "?bab $ n = (?ba * ?bb)$n" by simp
   138   then show ?thesis by (simp add: fps_mult_nth)
   139 qed
   140 
   141 lemma binomial_Vandermond: "setsum (\<lambda>k. (a choose k) * (b choose (n - k))) {0..n} = (a + b) choose n"
   142   using gbinomial_Vandermond[of "(of_nat a)" "of_nat b" n]
   143   
   144   apply (simp only: binomial_gbinomial[symmetric] of_nat_mult[symmetric] of_nat_setsum[symmetric] of_nat_add[symmetric])
   145   by simp
   146 
   147 lemma binomial_symmetric: assumes kn: "k \<le> n" 
   148   shows "n choose k = n choose (n - k)"
   149 proof-
   150   from kn have kn': "n - k \<le> n" by arith
   151   from binomial_fact_lemma[OF kn] binomial_fact_lemma[OF kn']
   152   have "fact k * fact (n - k) * (n choose k) = fact (n - k) * fact (n - (n - k)) * (n choose (n - k))" by simp
   153   then show ?thesis using kn by simp
   154 qed
   155   
   156 lemma binomial_Vandermond_same: "setsum (\<lambda>k. (n choose k)^2) {0..n} = (2*n) choose n"
   157   using binomial_Vandermond[of n n n,symmetric]
   158   unfolding nat_mult_2 apply (simp add: power2_eq_square)
   159   apply (rule setsum_cong2)
   160   by (auto intro:  binomial_symmetric)
   161 
   162 section {* Relation between formal sine/cosine and the exponential FPS*}
   163 lemma Eii_sin_cos:
   164   "E (ii * c) = fps_cos c + fps_const ii * fps_sin c "
   165   (is "?l = ?r")
   166 proof-
   167   {fix n::nat
   168     {assume en: "even n"
   169       from en obtain m where m: "n = 2*m" 
   170 	unfolding even_mult_two_ex by blast
   171       
   172       have "?l $n = ?r$n" 
   173 	by (simp add: m fps_sin_def fps_cos_def power_mult_distrib
   174 	  power_mult power_minus)}
   175     moreover
   176     {assume on: "odd n"
   177       from on obtain m where m: "n = 2*m + 1" 
   178 	unfolding odd_nat_equiv_def2 by (auto simp add: nat_mult_2)  
   179       have "?l $n = ?r$n" 
   180 	by (simp add: m fps_sin_def fps_cos_def power_mult_distrib
   181 	  power_mult power_minus)}
   182     ultimately have "?l $n = ?r$n"  by blast}
   183   then show ?thesis by (simp add: fps_eq_iff)
   184 qed
   185 
   186 lemma fps_sin_neg[simp]: "fps_sin (- c) = - fps_sin c"
   187 by (simp add: fps_eq_iff fps_sin_def)
   188 
   189 lemma fps_cos_neg[simp]: "fps_cos (- c) = fps_cos c"
   190   by (simp add: fps_eq_iff fps_cos_def)
   191 lemma E_minus_ii_sin_cos: "E (- (ii * c)) = fps_cos c - fps_const ii * fps_sin c "
   192   unfolding minus_mult_right Eii_sin_cos by simp
   193 
   194 lemma fps_cos_Eii:
   195   "fps_cos c = (E (ii * c) + E (- ii * c)) / fps_const 2"
   196 proof-
   197   have th: "fps_cos c + fps_cos c = fps_cos c * fps_const 2" 
   198     by (simp add: fps_eq_iff)
   199   show ?thesis
   200   unfolding Eii_sin_cos minus_mult_commute
   201   by (simp add: fps_divide_def fps_const_inverse th)
   202 qed
   203 
   204 lemma fps_sin_Eii:
   205   "fps_sin c = (E (ii * c) - E (- ii * c)) / fps_const (2*ii)"
   206 proof-
   207   have th: "fps_const \<i> * fps_sin c + fps_const \<i> * fps_sin c = fps_sin c * fps_const (2 * ii)" 
   208     by (simp add: fps_eq_iff)
   209   show ?thesis
   210   unfolding Eii_sin_cos minus_mult_commute
   211   by (simp add: fps_divide_def fps_const_inverse th)
   212 qed
   213 
   214 lemma fps_const_mult_2: "fps_const (2::'a::number_ring) * a = a +a"
   215   by (simp add: fps_eq_iff)
   216 
   217 lemma fps_const_mult_2_right: "a * fps_const (2::'a::number_ring) = a +a"
   218   by (simp add: fps_eq_iff)
   219 
   220 lemma fps_tan_Eii:
   221   "fps_tan c = (E (ii * c) - E (- ii * c)) / (fps_const ii * (E (ii * c) + E (- ii * c)))"
   222   unfolding fps_tan_def fps_sin_Eii fps_cos_Eii mult_minus_left E_neg
   223   apply (simp add: fps_divide_def fps_inverse_mult fps_const_mult[symmetric] fps_const_inverse del: fps_const_mult)
   224   by simp
   225 
   226 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)"
   227   unfolding Eii_sin_cos[symmetric] E_power_mult
   228   by (simp add: mult_ac)
   229 
   230 text{* Now some trigonometric identities *}
   231 lemma fps_sin_add: 
   232   "fps_sin (a+b) = fps_sin (a::complex) * fps_cos b + fps_cos a * fps_sin b"
   233 proof-
   234   let ?ca = "fps_cos a"
   235   let ?cb = "fps_cos b"
   236   let ?sa = "fps_sin a"
   237   let ?sb = "fps_sin b"
   238   let ?i = "fps_const ii"
   239   have i: "?i*?i = fps_const -1" by simp
   240   have "fps_sin (a + b) = 
   241     ((?ca + ?i * ?sa) * (?cb + ?i*?sb) - (?ca - ?i*?sa) * (?cb - ?i*?sb)) *
   242     fps_const (- (\<i> / 2))"
   243     apply(simp add: fps_sin_Eii[of "a+b"] fps_divide_def minus_mult_commute)
   244     unfolding right_distrib
   245     apply (simp add: Eii_sin_cos E_minus_ii_sin_cos fps_const_inverse E_add_mult)
   246     by (simp add: ring_simps)
   247   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)"
   248     by (simp add: ring_simps)
   249   also have "\<dots> = (fps_const 2 * ?i * (?ca * ?sb + ?sa * ?cb)) * fps_const (- ii/2)"
   250     apply simp
   251   apply (simp add: ring_simps)
   252     apply (simp add:  ring_simps add: fps_const_mult[symmetric] del:fps_const_mult)
   253     unfolding fps_const_mult_2_right
   254     by (simp add: ring_simps)
   255   also have "\<dots> = (fps_const 2 * ?i * fps_const (- ii/2)) * (?ca * ?sb + ?sa * ?cb)"
   256     by (simp only: mult_ac)
   257   also have "\<dots> = ?sa * ?cb + ?ca*?sb"
   258     by simp
   259   finally show ?thesis .
   260 qed
   261 
   262 lemma fps_cos_add: 
   263   "fps_cos (a+b) = fps_cos (a::complex) * fps_cos b - fps_sin a * fps_sin b"
   264 proof-
   265   let ?ca = "fps_cos a"
   266   let ?cb = "fps_cos b"
   267   let ?sa = "fps_sin a"
   268   let ?sb = "fps_sin b"
   269   let ?i = "fps_const ii"
   270   have i: "?i*?i = fps_const -1" by simp
   271   have i': "\<And>x. ?i * (?i * x) = - x" 
   272     apply (simp add: mult_assoc[symmetric] i)
   273     by (simp add: fps_eq_iff)
   274   have m1: "\<And>x. x * fps_const (-1 ::complex) = - x" "\<And>x. fps_const (-1 :: complex) * x = - x"
   275     by (auto simp add: fps_eq_iff)
   276 
   277   have "fps_cos (a + b) = 
   278     ((?ca + ?i * ?sa) * (?cb + ?i*?sb) + (?ca - ?i*?sa) * (?cb - ?i*?sb)) *
   279     fps_const (1/ 2)"
   280     apply(simp add: fps_cos_Eii[of "a+b"] fps_divide_def minus_mult_commute)
   281     unfolding right_distrib minus_add_distrib
   282     apply (simp add: Eii_sin_cos E_minus_ii_sin_cos fps_const_inverse E_add_mult)
   283     by (simp add: ring_simps)
   284   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)"
   285     apply simp
   286     by (simp add: ring_simps i' m1)
   287   also have "\<dots> = (fps_const 2 * (?ca * ?cb - ?sa * ?sb)) * fps_const (1/2)"
   288     apply simp
   289     by (simp add: ring_simps m1 fps_const_mult_2_right)
   290   also have "\<dots> = (fps_const 2 * fps_const (1/2)) * (?ca * ?cb - ?sa * ?sb)"
   291     by (simp only: mult_ac)
   292   also have "\<dots> = ?ca * ?cb - ?sa*?sb"
   293     by simp
   294   finally show ?thesis .
   295 qed
   296 
   297 end