src/HOL/ex/Formal_Power_Series_Examples.thy
 author chaieb Fri Jan 30 13:41:45 2009 +0000 (2009-01-30) changeset 29698 91feea8e41e4 parent 29696 477c7fcc0777 child 30748 fe67d729a61c permissions -rw-r--r--
Fixed theory name
```     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`