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