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.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.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.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.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)
```