src/HOL/Library/Formal_Power_Series.thy
changeset 60162 645058aa9d6f
parent 60017 b785d6d06430
child 60500 903bb1495239
     1.1 --- a/src/HOL/Library/Formal_Power_Series.thy	Wed Apr 29 14:04:22 2015 +0100
     1.2 +++ b/src/HOL/Library/Formal_Power_Series.thy	Thu Apr 30 15:28:01 2015 +0100
     1.3 @@ -742,32 +742,28 @@
     1.4      by (auto simp add: expand_fps_eq)
     1.5  qed
     1.6  
     1.7 -lemma fps_inverse_gp: "inverse (Abs_fps(\<lambda>n. (1::'a::field)))
     1.8 -    = Abs_fps (\<lambda>n. if n= 0 then 1 else if n=1 then - 1 else 0)"
     1.9 -  apply (rule fps_inverse_unique)
    1.10 -  apply simp
    1.11 -  apply (simp add: fps_eq_iff fps_mult_nth)
    1.12 -  apply clarsimp
    1.13 +lemma setsum_zero_lemma:
    1.14 +  fixes n::nat
    1.15 +  assumes "0 < n"
    1.16 +  shows "(\<Sum>i = 0..n. if n = i then 1 else if n - i = 1 then - 1 else 0) = (0::'a::field)"
    1.17  proof -
    1.18 -  fix n :: nat
    1.19 -  assume n: "n > 0"
    1.20 -  let ?f = "\<lambda>i. if n = i then (1::'a) else if n - i = 1 then - 1 else 0"
    1.21 -  let ?g = "\<lambda>i. if i = n then 1 else if i=n - 1 then - 1 else 0"
    1.22 +  let ?f = "\<lambda>i. if n = i then 1 else if n - i = 1 then - 1 else 0"
    1.23 +  let ?g = "\<lambda>i. if i = n then 1 else if i = n - 1 then - 1 else 0"
    1.24    let ?h = "\<lambda>i. if i=n - 1 then - 1 else 0"
    1.25    have th1: "setsum ?f {0..n} = setsum ?g {0..n}"
    1.26      by (rule setsum.cong) auto
    1.27    have th2: "setsum ?g {0..n - 1} = setsum ?h {0..n - 1}"
    1.28 -    apply (insert n)
    1.29      apply (rule setsum.cong)
    1.30 +    using assms
    1.31      apply auto
    1.32      done
    1.33    have eq: "{0 .. n} = {0.. n - 1} \<union> {n}"
    1.34      by auto
    1.35 -  from n have d: "{0.. n - 1} \<inter> {n} = {}"
    1.36 +  from assms have d: "{0.. n - 1} \<inter> {n} = {}"
    1.37      by auto
    1.38    have f: "finite {0.. n - 1}" "finite {n}"
    1.39      by auto
    1.40 -  show "setsum ?f {0..n} = 0"
    1.41 +  show ?thesis
    1.42      unfolding th1
    1.43      apply (simp add: setsum.union_disjoint[OF f d, unfolded eq[symmetric]] del: One_nat_def)
    1.44      unfolding th2
    1.45 @@ -775,6 +771,12 @@
    1.46      done
    1.47  qed
    1.48  
    1.49 +lemma fps_inverse_gp: "inverse (Abs_fps(\<lambda>n. (1::'a::field)))
    1.50 +    = Abs_fps (\<lambda>n. if n= 0 then 1 else if n=1 then - 1 else 0)"
    1.51 +  apply (rule fps_inverse_unique)
    1.52 +  apply (simp_all add: fps_eq_iff fps_mult_nth setsum_zero_lemma)
    1.53 +  done
    1.54 +
    1.55  
    1.56  subsection {* Formal Derivatives, and the MacLaurin theorem around 0 *}
    1.57  
    1.58 @@ -2885,8 +2887,7 @@
    1.59        unfolding th
    1.60        using fact_gt_zero
    1.61        apply (simp add: field_simps del: of_nat_Suc fact_Suc)
    1.62 -      apply (drule sym)
    1.63 -      apply (simp add: field_simps of_nat_mult)
    1.64 +      apply simp
    1.65        done
    1.66    }
    1.67    note th' = this
    1.68 @@ -2894,11 +2895,7 @@
    1.69  next
    1.70    assume h: ?rhs
    1.71    show ?lhs
    1.72 -    apply (subst h)
    1.73 -    apply simp
    1.74 -    apply (simp only: h[symmetric])
    1.75 -    apply simp
    1.76 -    done
    1.77 +    by (metis E_deriv fps_deriv_mult_const_left h mult.left_commute)
    1.78  qed
    1.79  
    1.80  lemma E_add_mult: "E (a + b) = E (a::'a::field_char_0) * E b" (is "?l = ?r")
    1.81 @@ -2949,16 +2946,6 @@
    1.82    apply auto
    1.83    done
    1.84  
    1.85 -lemma inverse_one_plus_X:
    1.86 -  "inverse (1 + X) = Abs_fps (\<lambda>n. (- 1 ::'a::field)^n)"
    1.87 -  (is "inverse ?l = ?r")
    1.88 -proof -
    1.89 -  have th: "?l * ?r = 1"
    1.90 -    by (auto simp add: field_simps fps_eq_iff minus_one_power_iff)
    1.91 -  have th': "?l $ 0 \<noteq> 0" by (simp add: )
    1.92 -  from fps_inverse_unique[OF th' th] show ?thesis .
    1.93 -qed
    1.94 -
    1.95  lemma E_power_mult: "(E (c::'a::field_char_0))^n = E (of_nat n * c)"
    1.96    by (induct n) (auto simp add: field_simps E_add_mult)
    1.97  
    1.98 @@ -2993,7 +2980,7 @@
    1.99    where "L c = fps_const (1/c) * Abs_fps (\<lambda>n. if n = 0 then 0 else (- 1) ^ (n - 1) / of_nat n)"
   1.100  
   1.101  lemma fps_deriv_L: "fps_deriv (L c) = fps_const (1/c) * inverse (1 + X)"
   1.102 -  unfolding inverse_one_plus_X
   1.103 +  unfolding fps_inverse_X_plus1
   1.104    by (simp add: L_def fps_eq_iff del: of_nat_Suc)
   1.105  
   1.106  lemma L_nth: "L c $ n = (if n=0 then 0 else 1/c * ((- 1) ^ (n - 1) / of_nat n))"
   1.107 @@ -3438,12 +3425,6 @@
   1.108    finally show ?thesis .
   1.109  qed
   1.110  
   1.111 -lemma divide_eq_iff: "a \<noteq> (0::'a::field) \<Longrightarrow> x / a = y \<longleftrightarrow> x = y * a"
   1.112 -  by auto
   1.113 -
   1.114 -lemma eq_divide_iff: "a \<noteq> (0::'a::field) \<Longrightarrow> x = y / a \<longleftrightarrow> x * a = y"
   1.115 -  by auto
   1.116 -
   1.117  lemma fps_sin_nth_0 [simp]: "fps_sin c $ 0 = 0"
   1.118    unfolding fps_sin_def by simp
   1.119  
   1.120 @@ -3454,7 +3435,7 @@
   1.121    "fps_sin c $ (n + 2) = - (c * c * fps_sin c $ n / (of_nat(n+1) * of_nat(n+2)))"
   1.122    unfolding fps_sin_def
   1.123    apply (cases n, simp)
   1.124 -  apply (simp add: divide_eq_iff eq_divide_iff del: of_nat_Suc fact_Suc)
   1.125 +  apply (simp add: nonzero_divide_eq_eq nonzero_eq_divide_eq del: of_nat_Suc fact_Suc)
   1.126    apply (simp add: of_nat_mult del: of_nat_Suc mult_Suc)
   1.127    done
   1.128  
   1.129 @@ -3467,7 +3448,7 @@
   1.130  lemma fps_cos_nth_add_2:
   1.131    "fps_cos c $ (n + 2) = - (c * c * fps_cos c $ n / (of_nat(n+1) * of_nat(n+2)))"
   1.132    unfolding fps_cos_def
   1.133 -  apply (simp add: divide_eq_iff eq_divide_iff del: of_nat_Suc fact_Suc)
   1.134 +  apply (simp add: nonzero_divide_eq_eq nonzero_eq_divide_eq del: of_nat_Suc fact_Suc)
   1.135    apply (simp add: of_nat_mult del: of_nat_Suc mult_Suc)
   1.136    done
   1.137  
   1.138 @@ -3500,7 +3481,7 @@
   1.139    apply (simp add: nat_add_1_add_1 fps_sin_nth_add_2
   1.140                del: One_nat_def of_nat_Suc of_nat_add add_2_eq_Suc')
   1.141    apply (subst minus_divide_left)
   1.142 -  apply (subst eq_divide_iff)
   1.143 +  apply (subst nonzero_eq_divide_eq)
   1.144    apply (simp del: of_nat_add of_nat_Suc)
   1.145    apply (simp only: ac_simps)
   1.146    done
   1.147 @@ -3518,7 +3499,7 @@
   1.148    apply (simp add: nat_add_1_add_1 fps_cos_nth_add_2
   1.149                del: One_nat_def of_nat_Suc of_nat_add add_2_eq_Suc')
   1.150    apply (subst minus_divide_left)
   1.151 -  apply (subst eq_divide_iff)
   1.152 +  apply (subst nonzero_eq_divide_eq)
   1.153    apply (simp del: of_nat_add of_nat_Suc)
   1.154    apply (simp only: ac_simps)
   1.155    done
   1.156 @@ -3793,7 +3774,8 @@
   1.157          THEN spec, of "\<lambda>x. x < e"]
   1.158        have "eventually (\<lambda>i. inverse (2 ^ i) < e) sequentially"
   1.159          unfolding eventually_nhds
   1.160 -        apply safe
   1.161 +        apply clarsimp
   1.162 +        apply (rule FalseE)
   1.163          apply auto --{*slow*}
   1.164          done
   1.165        then obtain i where "inverse (2 ^ i) < e" by (auto simp: eventually_sequentially)