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.21 -lemma setsum_power_add:
    1.22 +lemma sum_power_add:
    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.57      by (simp add: algebra_simps) (metis le_add_diff_inverse power_add)
    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