# HG changeset patch
# User nipkow
# Date 1108736427 -3600
# Node ID 5538d3244b4da50f1e7e325bc9db7425fdcd8991
# Parent  3ce1cb7a24f0bce04415c15bf118bd9c5f6c8634
continued eliminating sumr

diff -r 3ce1cb7a24f0 -r 5538d3244b4d src/HOL/Hyperreal/Series.thy
--- a/src/HOL/Hyperreal/Series.thy	Fri Feb 18 11:48:53 2005 +0100
+++ b/src/HOL/Hyperreal/Series.thy	Fri Feb 18 15:20:27 2005 +0100
@@ -52,8 +52,10 @@
 by (simp add:setsum_Un_disjoint[symmetric] ivl_disj_int ivl_disj_un)
 
 lemma sumr_split_add_minus:
-     "n < p ==> sumr 0 p f + - sumr 0 n f = sumr n p (f::nat=>real)"
-using sumr_split_add [of 0 n p f,symmetric]
+fixes f :: "nat \<Rightarrow> 'a::ab_group_add"
+shows "\<lbrakk> m \<le> n; n \<le> p \<rbrakk> \<Longrightarrow>
+  setsum f {m..<p} - setsum f {m..<n} = setsum f {n..<p}"
+using sumr_split_add [of m n p f,symmetric]
 apply (simp add: add_ac)
 done
 
@@ -216,10 +218,9 @@
 
 lemma series_zero: 
      "(\<forall>m. n \<le> m --> f(m) = 0) ==> f sums (sumr 0 n f)"
-apply (simp add: sums_def LIMSEQ_def, safe)
+apply (simp add: sums_def LIMSEQ_def diff_minus[symmetric], safe)
 apply (rule_tac x = n in exI)
-apply (safe, frule le_imp_less_or_eq, safe)
-apply (drule_tac f = f in sumr_split_add_minus, simp_all)
+apply (clarsimp simp:sumr_split_add_minus)
 apply (drule sumr_interval_const2, auto)
 done
 
@@ -344,7 +345,7 @@
 lemma summable_Cauchy:
      "summable f =  
       (\<forall>e > 0. \<exists>N. \<forall>m \<ge> N. \<forall>n. abs(sumr m n f) < e)"
-apply (auto simp add: summable_convergent_sumr_iff Cauchy_convergent_iff [symmetric] Cauchy_def)
+apply (auto simp add: summable_convergent_sumr_iff Cauchy_convergent_iff [symmetric] Cauchy_def diff_minus[symmetric])
 apply (drule_tac [!] spec, auto) 
 apply (rule_tac x = M in exI)
 apply (rule_tac [2] x = N in exI, auto)
@@ -352,8 +353,10 @@
 apply (frule le_less_trans [THEN less_imp_le], assumption)
 apply (drule_tac x = n in spec, simp)
 apply (drule_tac x = m in spec)
-apply (auto intro: abs_minus_add_cancel [THEN subst]
-            simp add: sumr_split_add_minus abs_minus_add_cancel)
+apply(simp add: sumr_split_add_minus)
+apply(subst abs_minus_commute)
+apply(simp add: sumr_split_add_minus)
+apply (simp add: sumr_split_add_minus)
 done
 
 text{*Comparison test*}
diff -r 3ce1cb7a24f0 -r 5538d3244b4d src/HOL/NumberTheory/Quadratic_Reciprocity.thy
--- a/src/HOL/NumberTheory/Quadratic_Reciprocity.thy	Fri Feb 18 11:48:53 2005 +0100
+++ b/src/HOL/NumberTheory/Quadratic_Reciprocity.thy	Fri Feb 18 15:20:27 2005 +0100
@@ -124,8 +124,7 @@
     by auto
   moreover have "0 \<le> setsum (%x. ((x * a) div p)) A"
     proof (intro setsum_nonneg)
-      from finite_A show "finite A".
-      next show "\<forall>x \<in> A. 0 \<le> x * a div p"
+      show "\<forall>x \<in> A. 0 \<le> x * a div p"
       proof
         fix x
         assume "x \<in> A"