1.1 --- a/src/HOL/SetInterval.thy	Fri Mar 30 14:00:18 2012 +0200
     1.2 +++ b/src/HOL/SetInterval.thy	Fri Mar 30 14:25:32 2012 +0200
     1.3 @@ -1282,19 +1282,21 @@
     1.4  
     1.5  subsection {* The formula for arithmetic sums *}
     1.6  
     1.7 -lemma gauss_sum: (* FIXME: rephrase in terms of "2" *)
     1.8 -  "((1::'a::comm_semiring_1) + 1)*(\<Sum>i\<in>{1..n}. of_nat i) =
     1.9 +lemma gauss_sum:
    1.10 +  "(2::'a::comm_semiring_1)*(\<Sum>i\<in>{1..n}. of_nat i) =
    1.11     of_nat n*((of_nat n)+1)"
    1.12  proof (induct n)
    1.13    case 0
    1.14    show ?case by simp
    1.15  next
    1.16    case (Suc n)
    1.17 -  then show ?case by (simp add: algebra_simps del: one_add_one) (* FIXME *)
    1.18 +  then show ?case
    1.19 +    by (simp add: algebra_simps add: one_add_one [symmetric] del: one_add_one)
    1.20 +      (* FIXME: make numeral cancellation simprocs work for semirings *)
    1.21  qed
    1.22  
    1.23  theorem arith_series_general:
    1.24 -  "((1::'a::comm_semiring_1) + 1) * (\<Sum>i\<in>{..<n}. a + of_nat i * d) =
    1.25 +  "(2::'a::comm_semiring_1) * (\<Sum>i\<in>{..<n}. a + of_nat i * d) =
    1.26    of_nat n * (a + (a + of_nat(n - 1)*d))"
    1.27  proof cases
    1.28    assume ngt1: "n > 1"
    1.29 @@ -1307,26 +1309,27 @@
    1.30    also from ngt1 have "\<dots> = (?n*a + d*(\<Sum>i\<in>{1..<n}. ?I i))"
    1.31      unfolding One_nat_def
    1.32      by (simp add: setsum_right_distrib atLeast0LessThan[symmetric] setsum_shift_lb_Suc0_0_upt mult_ac)
    1.33 -  also have "(1+1)*\<dots> = (1+1)*?n*a + d*(1+1)*(\<Sum>i\<in>{1..<n}. ?I i)"
    1.34 -    by (simp add: left_distrib right_distrib del: one_add_one)
    1.35 +  also have "2*\<dots> = 2*?n*a + d*2*(\<Sum>i\<in>{1..<n}. ?I i)"
    1.36 +    by (simp add: algebra_simps)
    1.37    also from ngt1 have "{1..<n} = {1..n - 1}"
    1.38      by (cases n) (auto simp: atLeastLessThanSuc_atLeastAtMost)
    1.39    also from ngt1
    1.40 -  have "(1+1)*?n*a + d*(1+1)*(\<Sum>i\<in>{1..n - 1}. ?I i) = ((1+1)*?n*a + d*?I (n - 1)*?I n)"
    1.41 +  have "2*?n*a + d*2*(\<Sum>i\<in>{1..n - 1}. ?I i) = (2*?n*a + d*?I (n - 1)*?I n)"
    1.42      by (simp only: mult_ac gauss_sum [of "n - 1"], unfold One_nat_def)
    1.43         (simp add:  mult_ac trans [OF add_commute of_nat_Suc [symmetric]])
    1.44 -  finally show ?thesis by (simp add: algebra_simps del: one_add_one)
    1.45 +  finally show ?thesis
    1.46 +    unfolding mult_2 by (simp add: algebra_simps)
    1.47  next
    1.48    assume "\<not>(n > 1)"
    1.49    hence "n = 1 \<or> n = 0" by auto
    1.50 -  thus ?thesis by (auto simp: algebra_simps mult_2_right)
    1.51 +  thus ?thesis by (auto simp: mult_2)
    1.52  qed
    1.53  
    1.54  lemma arith_series_nat:
    1.55 -  "Suc (Suc 0) * (\<Sum>i\<in>{..<n}. a+i*d) = n * (a + (a+(n - 1)*d))"
    1.56 +  "(2::nat) * (\<Sum>i\<in>{..<n}. a+i*d) = n * (a + (a+(n - 1)*d))"
    1.57  proof -
    1.58    have
    1.59 -    "((1::nat) + 1) * (\<Sum>i\<in>{..<n::nat}. a + of_nat(i)*d) =
    1.60 +    "2 * (\<Sum>i\<in>{..<n::nat}. a + of_nat(i)*d) =
    1.61      of_nat(n) * (a + (a + of_nat(n - 1)*d))"
    1.62      by (rule arith_series_general)
    1.63    thus ?thesis
    1.64 @@ -1334,15 +1337,8 @@
    1.65  qed
    1.66  
    1.67  lemma arith_series_int:
    1.68 -  "(2::int) * (\<Sum>i\<in>{..<n}. a + of_nat i * d) =
    1.69 -  of_nat n * (a + (a + of_nat(n - 1)*d))"
    1.70 -proof -
    1.71 -  have
    1.72 -    "((1::int) + 1) * (\<Sum>i\<in>{..<n}. a + of_nat i * d) =
    1.73 -    of_nat(n) * (a + (a + of_nat(n - 1)*d))"
    1.74 -    by (rule arith_series_general)
    1.75 -  thus ?thesis by simp
    1.76 -qed
    1.77 +  "2 * (\<Sum>i\<in>{..<n}. a + int i * d) = int n * (a + (a + int(n - 1)*d))"
    1.78 +  by (fact arith_series_general) (* FIXME: duplicate *)
    1.79  
    1.80  lemma sum_diff_distrib:
    1.81    fixes P::"nat\<Rightarrow>nat"

     2.1 --- a/src/HOL/ex/Arithmetic_Series_Complex.thy	Fri Mar 30 14:00:18 2012 +0200
     2.2 +++ b/src/HOL/ex/Arithmetic_Series_Complex.thy	Fri Mar 30 14:25:32 2012 +0200
     2.3 @@ -6,18 +6,12 @@
     2.4  header {* Arithmetic Series for Reals *}
     2.5  
     2.6  theory Arithmetic_Series_Complex
     2.7 -imports Complex_Main 
     2.8 +imports "../RealDef"
     2.9  begin
    2.10  
    2.11  lemma arith_series_real:
    2.12    "(2::real) * (\<Sum>i\<in>{..<n}. a + of_nat i * d) =
    2.13    of_nat n * (a + (a + of_nat(n - 1)*d))"
    2.14 -proof -
    2.15 -  have
    2.16 -    "((1::real) + 1) * (\<Sum>i\<in>{..<n}. a + of_nat(i)*d) =
    2.17 -    of_nat(n) * (a + (a + of_nat(n - 1)*d))"
    2.18 -    by (rule arith_series_general)
    2.19 -  thus ?thesis by simp
    2.20 -qed
    2.21 +  by (fact arith_series_general) (* FIXME: duplicate *)
    2.22  
    2.23  end