src/HOL/Analysis/Poly_Roots.thy
 changeset 64267 b9a1486e79be parent 63918 6bf55e6e0b75 child 65578 e4997c181cce
```     1.1 --- a/src/HOL/Analysis/Poly_Roots.thy	Sun Oct 16 22:43:51 2016 +0200
1.2 +++ b/src/HOL/Analysis/Poly_Roots.thy	Mon Oct 17 11:46:22 2016 +0200
1.3 @@ -10,67 +10,67 @@
1.4
1.5  subsection\<open>Geometric progressions\<close>
1.6
1.7 -lemma setsum_gp_basic:
1.8 +lemma sum_gp_basic:
1.9    fixes x :: "'a::{comm_ring,monoid_mult}"
1.10    shows "(1 - x) * (\<Sum>i\<le>n. x^i) = 1 - x^Suc n"
1.11    by (simp only: one_diff_power_eq [of "Suc n" x] lessThan_Suc_atMost)
1.12
1.13 -lemma setsum_gp0:
1.14 +lemma sum_gp0:
1.15    fixes x :: "'a::{comm_ring,division_ring}"
1.16    shows   "(\<Sum>i\<le>n. x^i) = (if x = 1 then of_nat(n + 1) else (1 - x^Suc n) / (1 - x))"
1.17 -  using setsum_gp_basic[of x n]
1.18 +  using sum_gp_basic[of x n]
1.19    by (simp add: mult.commute divide_simps)
1.20
1.23    fixes x :: "'a::{comm_ring,monoid_mult}"
1.24    shows "(\<Sum>i\<in>I. x^(m+i)) = x^m * (\<Sum>i\<in>I. x^i)"
1.25 -  by (simp add: setsum_distrib_left power_add)
1.26 +  by (simp add: sum_distrib_left power_add)
1.27
1.28 -lemma setsum_power_shift:
1.29 +lemma sum_power_shift:
1.30    fixes x :: "'a::{comm_ring,monoid_mult}"
1.31    assumes "m \<le> n"
1.32    shows "(\<Sum>i=m..n. x^i) = x^m * (\<Sum>i\<le>n-m. x^i)"
1.33  proof -
1.34    have "(\<Sum>i=m..n. x^i) = x^m * (\<Sum>i=m..n. x^(i-m))"
1.35 -    by (simp add: setsum_distrib_left power_add [symmetric])
1.36 +    by (simp add: sum_distrib_left power_add [symmetric])
1.37    also have "(\<Sum>i=m..n. x^(i-m)) = (\<Sum>i\<le>n-m. x^i)"
1.38 -    using \<open>m \<le> n\<close> by (intro setsum.reindex_bij_witness[where j="\<lambda>i. i - m" and i="\<lambda>i. i + m"]) auto
1.39 +    using \<open>m \<le> n\<close> by (intro sum.reindex_bij_witness[where j="\<lambda>i. i - m" and i="\<lambda>i. i + m"]) auto
1.40    finally show ?thesis .
1.41  qed
1.42
1.43 -lemma setsum_gp_multiplied:
1.44 +lemma sum_gp_multiplied:
1.45    fixes x :: "'a::{comm_ring,monoid_mult}"
1.46    assumes "m \<le> n"
1.47    shows "(1 - x) * (\<Sum>i=m..n. x^i) = x^m - x^Suc n"
1.48  proof -
1.49    have  "(1 - x) * (\<Sum>i=m..n. x^i) = x^m * (1 - x) * (\<Sum>i\<le>n-m. x^i)"
1.50 -    by (metis mult.assoc mult.commute assms setsum_power_shift)
1.51 +    by (metis mult.assoc mult.commute assms sum_power_shift)
1.52    also have "... =x^m * (1 - x^Suc(n-m))"
1.53 -    by (metis mult.assoc setsum_gp_basic)
1.54 +    by (metis mult.assoc sum_gp_basic)
1.55    also have "... = x^m - x^Suc n"
1.56      using assms
1.58    finally show ?thesis .
1.59  qed
1.60
1.61 -lemma setsum_gp:
1.62 +lemma sum_gp:
1.63    fixes x :: "'a::{comm_ring,division_ring}"
1.64    shows   "(\<Sum>i=m..n. x^i) =
1.65                 (if n < m then 0
1.66                  else if x = 1 then of_nat((n + 1) - m)
1.67                  else (x^m - x^Suc n) / (1 - x))"
1.68 -using setsum_gp_multiplied [of m n x]
1.69 +using sum_gp_multiplied [of m n x]
1.70  apply auto
1.71  by (metis eq_iff_diff_eq_0 mult.commute nonzero_divide_eq_eq)
1.72
1.73 -lemma setsum_gp_offset:
1.74 +lemma sum_gp_offset:
1.75    fixes x :: "'a::{comm_ring,division_ring}"
1.76    shows   "(\<Sum>i=m..m+n. x^i) =
1.77         (if x = 1 then of_nat n + 1 else x^m * (1 - x^Suc n) / (1 - x))"
1.78 -  using setsum_gp [of x m "m+n"]
1.79 +  using sum_gp [of x m "m+n"]
1.80    by (auto simp: power_add algebra_simps)
1.81
1.82 -lemma setsum_gp_strict:
1.83 +lemma sum_gp_strict:
1.84    fixes x :: "'a::{comm_ring,division_ring}"
1.85    shows "(\<Sum>i<n. x^i) = (if x = 1 then of_nat n else (1 - x^n) / (1 - x))"
1.86    by (induct n) (auto simp: algebra_simps divide_simps)
1.87 @@ -84,13 +84,13 @@
1.88  proof -
1.89    have "(\<Sum>i\<le>n. a i * x^i) - (\<Sum>i\<le>n. a i * y^i) =
1.90          (\<Sum>i\<le>n. a i * (x^i - y^i))"
1.91 -    by (simp add: algebra_simps setsum_subtractf [symmetric])
1.92 +    by (simp add: algebra_simps sum_subtractf [symmetric])
1.93    also have "... = (\<Sum>i\<le>n. a i * (x - y) * (\<Sum>j<i. y^(i - Suc j) * x^j))"
1.94      by (simp add: power_diff_sumr2 ac_simps)
1.95    also have "... = (x - y) * (\<Sum>i\<le>n. (\<Sum>j<i. a i * y^(i - Suc j) * x^j))"
1.96 -    by (simp add: setsum_distrib_left ac_simps)
1.97 +    by (simp add: sum_distrib_left ac_simps)
1.98    also have "... = (x - y) * (\<Sum>j<n. (\<Sum>i=Suc j..n. a i * y^(i - Suc j) * x^j))"
1.99 -    by (simp add: nested_setsum_swap')
1.100 +    by (simp add: nested_sum_swap')
1.101    finally show ?thesis .
1.102  qed
1.103
1.104 @@ -102,7 +102,7 @@
1.105    { fix j
1.106      have "(\<Sum>k = Suc j..n. a k * y^(k - Suc j) * x^j) =
1.107            (\<Sum>k <n - j. a (Suc (j + k)) * y^k * x^j)"
1.108 -      by (rule setsum.reindex_bij_witness[where i="\<lambda>i. i + Suc j" and j="\<lambda>i. i - Suc j"]) auto }
1.109 +      by (rule sum.reindex_bij_witness[where i="\<lambda>i. i + Suc j" and j="\<lambda>i. i - Suc j"]) auto }
1.110    then show ?thesis
1.111      by (simp add: sub_polyfun)
1.112  qed
1.113 @@ -115,7 +115,7 @@
1.114    { fix z
1.115      have "(\<Sum>i\<le>n. c i * z^i) - (\<Sum>i\<le>n. c i * a^i) =
1.116            (z - a) * (\<Sum>j<n. (\<Sum>k = Suc j..n. c k * a^(k - Suc j)) * z^j)"
1.117 -      by (simp add: sub_polyfun setsum_distrib_right)
1.118 +      by (simp add: sub_polyfun sum_distrib_right)
1.119      then have "(\<Sum>i\<le>n. c i * z^i) =
1.120            (z - a) * (\<Sum>j<n. (\<Sum>k = Suc j..n. c k * a^(k - Suc j)) * z^j)
1.121            + (\<Sum>i\<le>n. c i * a^i)"
1.122 @@ -241,7 +241,7 @@
1.123     have "\<exists>k\<le>n. b k \<noteq> 0"
1.124       apply (rule ccontr)
1.125       using polyfun_extremal [OF extr_prem, of 1]
1.126 -     apply (auto simp: eventually_at_infinity b simp del: setsum_atMost_Suc)
1.127 +     apply (auto simp: eventually_at_infinity b simp del: sum_atMost_Suc)
1.128       apply (drule_tac x="of_real ba" in spec, simp)
1.129       done
1.130     then show ?thesis using Suc.IH [of b] ins_ab
```