# HG changeset patch
# User nipkow
# Date 1108723733 -3600
# Node ID 3ce1cb7a24f0bce04415c15bf118bd9c5f6c8634
# Parent  a0cf3a19ee369fbe95c0473e10c7cc160b0c12a6
starting to get rid of sumr

diff -r a0cf3a19ee36 -r 3ce1cb7a24f0 src/HOL/Hyperreal/HSeries.thy
--- a/src/HOL/Hyperreal/HSeries.thy	Fri Feb 18 11:48:42 2005 +0100
+++ b/src/HOL/Hyperreal/HSeries.thy	Fri Feb 18 11:48:53 2005 +0100
@@ -73,12 +73,12 @@
 
 lemma sumhr_add: "sumhr (m,n,f) + sumhr(m,n,g) = sumhr(m,n,%i. f i + g i)"
 apply (cases m, cases n)
-apply (simp add: sumhr hypreal_add sumr_add)
+apply (simp add: sumhr hypreal_add setsum_addf)
 done
 
 lemma sumhr_mult: "hypreal_of_real r * sumhr(m,n,f) = sumhr(m,n,%n. r * f n)"
 apply (cases m, cases n)
-apply (simp add: sumhr hypreal_of_real_def hypreal_mult sumr_mult)
+apply (simp add: sumhr hypreal_of_real_def hypreal_mult setsum_mult)
 done
 
 lemma sumhr_split_add: "n < p ==> sumhr(0,n,f) + sumhr(n,p,f) = sumhr(0,p,f)"
@@ -92,7 +92,7 @@
 
 lemma sumhr_hrabs: "abs(sumhr(m,n,f)) \<le> sumhr(m,n,%i. abs(f i))"
 apply (cases n, cases m)
-apply (simp add: sumhr hypreal_le hypreal_hrabs sumr_rabs)
+apply (simp add: sumhr hypreal_le hypreal_hrabs setsum_abs)
 done
 
 text{* other general version also needed *}
@@ -100,9 +100,8 @@
    "(\<forall>r. m \<le> r & r < n --> f r = g r) -->  
       sumhr(hypnat_of_nat m, hypnat_of_nat n, f) =  
       sumhr(hypnat_of_nat m, hypnat_of_nat n, g)"
-apply (safe, drule sumr_fun_eq)
-apply (simp add: sumhr hypnat_of_nat_eq)
-done
+by (fastsimp simp add: sumhr hypnat_of_nat_eq intro:setsum_cong)
+
 
 lemma sumhr_const:
      "sumhr(0, n, %i. r) = hypreal_of_hypnat n * hypreal_of_real r"
@@ -119,7 +118,7 @@
 
 lemma sumhr_minus: "sumhr(m, n, %i. - f i) = - sumhr(m, n, f)"
 apply (cases m, cases n)
-apply (simp add: sumhr hypreal_minus sumr_minus)
+apply (simp add: sumhr hypreal_minus setsum_negf)
 done
 
 lemma sumhr_shift_bounds:
diff -r a0cf3a19ee36 -r 3ce1cb7a24f0 src/HOL/Hyperreal/Integration.thy
--- a/src/HOL/Hyperreal/Integration.thy	Fri Feb 18 11:48:42 2005 +0100
+++ b/src/HOL/Hyperreal/Integration.thy	Fri Feb 18 11:48:53 2005 +0100
@@ -343,7 +343,7 @@
 lemma Integral_mult_const: "a \<le> b ==> Integral(a,b) (%x. c)  (c*(b - a))"
 apply (auto simp add: order_le_less rsum_def Integral_def)
 apply (rule_tac x = "%x. b - a" in exI)
-apply (auto simp add: sumr_mult [symmetric] gauge_def abs_interval_iff 
+apply (auto simp add: setsum_mult [symmetric] gauge_def abs_interval_iff 
                right_diff_distrib [symmetric] partition tpart_def)
 done
 
@@ -351,7 +351,7 @@
      "[| a \<le> b; Integral(a,b) f k |] ==> Integral(a,b) (%x. c * f x) (c * k)"
 apply (auto simp add: order_le_less 
             dest: Integral_unique [OF order_refl Integral_zero])
-apply (auto simp add: rsum_def Integral_def sumr_mult [symmetric] mult_assoc)
+apply (auto simp add: rsum_def Integral_def setsum_mult[symmetric] mult_assoc)
 apply (rule_tac a2 = c in abs_ge_zero [THEN real_le_imp_less_or_eq, THEN disjE])
  prefer 2 apply force
 apply (drule_tac x = "e/abs c" in spec, auto)
@@ -459,13 +459,13 @@
         in sumr_partition_eq_diff_bounds)
  apply (simp add: partition_lhs partition_rhs)
 apply (drule sym, simp)
-apply (simp (no_asm) add: sumr_diff)
-apply (rule sumr_rabs [THEN order_trans])
+apply (simp (no_asm) add: setsum_subtractf[symmetric])
+apply (rule setsum_abs [THEN order_trans])
 apply (subgoal_tac "ea = sumr 0 (psize D) (%n. (ea / (b - a)) * (D (Suc n) - (D n)))")
 apply (simp add: abs_minus_commute)
 apply (rule_tac t = ea in ssubst, assumption)
 apply (rule sumr_le2)
-apply (rule_tac [2] sumr_mult [THEN subst])
+apply (rule_tac [2] setsum_mult [THEN subst])
 apply (auto simp add: partition_rhs partition_lhs partition_lb partition_ub
           fine_def)
 done
@@ -769,7 +769,7 @@
 done
 
 lemma rsum_add: "rsum (D, p) (%x. f x + g x) =  rsum (D, p) f + rsum(D, p) g"
-by (simp add: rsum_def sumr_add left_distrib)
+by (simp add: rsum_def setsum_addf left_distrib)
 
 text{* Bartle/Sherbert: Theorem 10.1.5 p. 278 *}
 lemma Integral_add_fun:
diff -r a0cf3a19ee36 -r 3ce1cb7a24f0 src/HOL/Hyperreal/MacLaurin.thy
--- a/src/HOL/Hyperreal/MacLaurin.thy	Fri Feb 18 11:48:42 2005 +0100
+++ b/src/HOL/Hyperreal/MacLaurin.thy	Fri Feb 18 11:48:53 2005 +0100
@@ -267,7 +267,7 @@
 apply (rule_tac x = "-t" in exI, auto)
 apply (subgoal_tac "(\<Sum>m = 0..<n. -1 ^ m * diff m 0 * (-h)^m / real(fact m)) =
                     (\<Sum>m = 0..<n. diff m 0 * h ^ m / real(fact m))")
-apply (rule_tac [2] sumr_fun_eq)
+apply (rule_tac [2] setsum_cong[OF refl])
 apply (auto simp add: divide_inverse power_mult_distrib [symmetric])
 done
 
@@ -435,7 +435,7 @@
 apply (drule_tac x = x in spec, simp)
 apply (erule ssubst)
 apply (rule_tac x = t in exI, simp)
-apply (rule sumr_fun_eq)
+apply (rule setsum_cong[OF refl])
 apply (auto simp add: sin_zero_iff odd_Suc_mult_two_ex times_divide_eq)
 done
 
@@ -465,7 +465,7 @@
 apply (simp (no_asm) add: times_divide_eq)
 apply (erule ssubst)
 apply (rule_tac x = t in exI, simp)
-apply (rule sumr_fun_eq)
+apply (rule setsum_cong[OF refl])
 apply (auto simp add: sin_zero_iff odd_Suc_mult_two_ex times_divide_eq)
 done
 
@@ -483,7 +483,7 @@
 apply (simp (no_asm) add: times_divide_eq)
 apply (erule ssubst)
 apply (rule_tac x = t in exI, simp)
-apply (rule sumr_fun_eq)
+apply (rule setsum_cong[OF refl])
 apply (auto simp add: sin_zero_iff odd_Suc_mult_two_ex times_divide_eq)
 done
 
@@ -516,7 +516,7 @@
 apply (drule_tac x = x in spec, simp)
 apply (erule ssubst)
 apply (rule_tac x = t in exI, simp)
-apply (rule sumr_fun_eq)
+apply (rule setsum_cong[OF refl])
 apply (auto simp add: cos_zero_iff even_mult_two_ex)
 done
 
@@ -535,7 +535,7 @@
 apply (simp (no_asm) add: times_divide_eq)
 apply (erule ssubst)
 apply (rule_tac x = t in exI, simp)
-apply (rule sumr_fun_eq)
+apply (rule setsum_cong[OF refl])
 apply (auto simp add: cos_zero_iff even_mult_two_ex)
 done
 
@@ -554,7 +554,7 @@
 apply (simp (no_asm) add: times_divide_eq)
 apply (erule ssubst)
 apply (rule_tac x = t in exI, simp)
-apply (rule sumr_fun_eq)
+apply (rule setsum_cong[OF refl])
 apply (auto simp add: cos_zero_iff even_mult_two_ex)
 done
 
@@ -585,10 +585,10 @@
     apply (rule lemma_DERIV_subst, rule DERIV_minus, rule DERIV_cos, simp)
     apply (erule ssubst)
     apply (rule sin_bound_lemma)
-    apply (rule sumr_fun_eq, safe)
-    apply (rule_tac f = "%u. u * (x^r)" in arg_cong)
+    apply (rule setsum_cong[OF refl])
+    apply (rule_tac f = "%u. u * (x^xa)" in arg_cong)
     apply (subst even_even_mod_4_iff)
-    apply (cut_tac m=r in mod_exhaust_less_4, simp, safe)
+    apply (cut_tac m=xa in mod_exhaust_less_4, simp, safe)
     apply (simp_all add:even_num_iff)
     apply (drule lemma_even_mod_4_div_2[simplified])
     apply(simp add: numeral_2_eq_2 divide_inverse)
diff -r a0cf3a19ee36 -r 3ce1cb7a24f0 src/HOL/Hyperreal/Series.thy
--- a/src/HOL/Hyperreal/Series.thy	Fri Feb 18 11:48:42 2005 +0100
+++ b/src/HOL/Hyperreal/Series.thy	Fri Feb 18 11:48:53 2005 +0100
@@ -11,13 +11,15 @@
 imports SEQ Lim
 begin
 
+declare atLeastLessThan_empty[simp];
+
 syntax sumr :: "[nat,nat,(nat=>real)] => real"
 translations
   "sumr m n f" => "setsum (f::nat=>real) (atLeastLessThan m n)"
 
 constdefs
    sums  :: "[nat=>real,real] => bool"     (infixr "sums" 80)
-   "f sums s  == (%n. sumr 0 n f) ----> s"
+   "f sums s  == (%n. setsum f {0..<n}) ----> s"
 
    summable :: "(nat=>real) => bool"
    "summable f == (\<exists>s. f sums s)"
@@ -27,9 +29,10 @@
 
 
 lemma sumr_Suc [simp]:
-     "sumr m (Suc n) f = (if n < m then 0 else sumr m n f + f(n))"
-by (simp add: atLeastLessThanSuc)
+  "setsum f {m..<Suc n} = (if n < m then 0 else setsum f {m..<n} + f(n))"
+by (simp add: atLeastLessThanSuc add_commute)
 
+(*
 lemma sumr_add: "sumr m n f + sumr m n g = sumr m n (%n. f n + g n)"
 by (simp add: setsum_addf)
 
@@ -42,13 +45,22 @@
 apply (rename_tac k) 
 apply (subgoal_tac "n=k", auto) 
 done
+*)
+
+lemma sumr_split_add: "\<lbrakk> m \<le> n; n \<le> p \<rbrakk> \<Longrightarrow>
+  setsum f {m..<n} + setsum f {n..<p} = setsum f {m..<p::nat}"
+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)"
-apply (drule_tac f1 = f in sumr_split_add [symmetric])
+using sumr_split_add [of 0 n p f,symmetric]
 apply (simp add: add_ac)
 done
 
+lemma sumr_diff_mult_const: "sumr 0 n f - (real n*r) = sumr 0 n (%i. f i - r)"
+by (simp add: diff_minus setsum_addf real_of_nat_def)
+
+(*
 lemma sumr_rabs: "abs(sumr m n  (f::nat=>real)) \<le> sumr m n (%i. abs(f i))"
 by (simp add: setsum_abs)
 
@@ -60,14 +72,12 @@
      "(\<forall>r. m \<le> r & r < n --> f r = g r) ==> sumr m n f = sumr m n g"
 by (auto intro: setsum_cong) 
 
-lemma sumr_diff_mult_const: "sumr 0 n f - (real n*r) = sumr 0 n (%i. f i - r)"
-by (simp add: diff_minus setsum_addf real_of_nat_def)
-
 lemma sumr_less_bounds_zero [simp]: "n < m ==> sumr m n f = 0"
 by (simp add: atLeastLessThan_empty)
 
 lemma sumr_minus: "sumr m n (%i. - f i) = - sumr m n f"
 by (simp add: Finite_Set.setsum_negf)
+*)
 
 lemma sumr_shift_bounds: "sumr (m+k) (n+k) f = sumr m n (%i. f(i + k))"
 by (induct "n", auto)
@@ -114,6 +124,7 @@
 apply (drule_tac x = n in spec, arith)
 done
 
+(* FIXME generalize *)
 lemma rabs_sumr_rabs_cancel [simp]:
      "abs (sumr m n (%k. abs (f k))) = (sumr m n (%k. abs (f k)))"
 by (induct "n", simp_all add: add_increasing)
@@ -132,10 +143,10 @@
 apply (induct "n")
 apply (case_tac [2] "n", auto)
 done
-
+(*
 lemma sumr_diff: "sumr m n f - sumr m n g = sumr m n (%n. f n - g n)"
-by (simp add: diff_minus sumr_add [symmetric] sumr_minus)
-
+by (simp add: diff_minus setsum_addf setsum_negf)
+*)
 lemma sumr_subst [rule_format (no_asm)]:
      "(\<forall>p. m \<le> p & p < m+n --> (f p = g p)) --> sumr m n f = sumr m n g"
 by (induct "n", auto)
@@ -213,14 +224,14 @@
 done
 
 lemma sums_mult: "x sums x0 ==> (%n. c * x(n)) sums (c * x0)"
-by (auto simp add: sums_def sumr_mult [symmetric]
+by (auto simp add: sums_def setsum_mult [symmetric]
          intro!: LIMSEQ_mult intro: LIMSEQ_const)
 
 lemma sums_divide: "x sums x' ==> (%n. x(n)/c) sums (x'/c)"
 by (simp add: real_divide_def sums_mult mult_commute [of _ "inverse c"])
 
 lemma sums_diff: "[| x sums x0; y sums y0 |] ==> (%n. x n - y n) sums (x0-y0)"
-by (auto simp add: sums_def sumr_diff [symmetric] intro: LIMSEQ_diff)
+by (auto simp add: sums_def setsum_subtractf intro: LIMSEQ_diff)
 
 lemma suminf_mult: "summable f ==> suminf f * c = suminf(%n. f n * c)"
 by (auto intro!: sums_unique sums_mult summable_sums simp add: mult_commute)
@@ -234,7 +245,7 @@
 by (auto intro!: sums_diff sums_unique summable_sums)
 
 lemma sums_minus: "x sums x0 ==> (%n. - x n) sums - x0"
-by (auto simp add: sums_def intro!: LIMSEQ_minus simp add: sumr_minus)
+by (auto simp add: sums_def intro!: LIMSEQ_minus simp add: setsum_negf)
 
 lemma sums_group:
      "[|summable f; 0 < k |] ==> (%n. sumr (n*k) (n*k + k) f) sums (suminf f)"
@@ -356,7 +367,7 @@
 apply (drule_tac x = m in spec)
 apply (auto, rotate_tac 2, drule_tac x = n in spec)
 apply (rule_tac y = "sumr m n (%k. abs (f k))" in order_le_less_trans)
-apply (rule sumr_rabs)
+apply (rule setsum_abs)
 apply (rule_tac y = "sumr m n g" in order_le_less_trans)
 apply (auto intro: sumr_le2 simp add: abs_interval_iff)
 done
@@ -387,18 +398,18 @@
 
 text{*Absolute convergence imples normal convergence*}
 lemma summable_rabs_cancel: "summable (%n. abs (f n)) ==> summable f"
-apply (auto simp add: sumr_rabs summable_Cauchy)
+apply (auto simp add: summable_Cauchy)
 apply (drule spec, auto)
 apply (rule_tac x = N in exI, auto)
 apply (drule spec, auto)
 apply (rule_tac y = "sumr m n (%n. abs (f n))" in order_le_less_trans)
-apply (auto intro: sumr_rabs)
+apply (auto)
 done
 
 text{*Absolute convergence of series*}
 lemma summable_rabs:
      "summable (%n. abs (f n)) ==> abs(suminf f) \<le> suminf (%n. abs(f n))"
-by (auto intro: LIMSEQ_le LIMSEQ_imp_rabs summable_rabs_cancel summable_sumr_LIMSEQ_suminf sumr_rabs)
+by (auto intro: LIMSEQ_le LIMSEQ_imp_rabs summable_rabs_cancel summable_sumr_LIMSEQ_suminf)
 
 
 subsection{* The Ratio Test*}
@@ -465,19 +476,13 @@
 val summable_def = thm"summable_def";
 val suminf_def = thm"suminf_def";
 
-val sumr_add = thm "sumr_add";
-val sumr_mult = thm "sumr_mult";
 val sumr_split_add = thm "sumr_split_add";
-val sumr_rabs = thm "sumr_rabs";
-val sumr_fun_eq = thm "sumr_fun_eq";
-val sumr_diff_mult_const = thm "sumr_diff_mult_const";
 val sumr_minus_one_realpow_zero = thm "sumr_minus_one_realpow_zero";
 val sumr_le2 = thm "sumr_le2";
 val rabs_sumr_rabs_cancel = thm "rabs_sumr_rabs_cancel";
 val sumr_zero = thm "sumr_zero";
 val Suc_le_imp_diff_ge2 = thm "Suc_le_imp_diff_ge2";
 val sumr_one_lb_realpow_zero = thm "sumr_one_lb_realpow_zero";
-val sumr_diff = thm "sumr_diff";
 val sumr_subst = thm "sumr_subst";
 val sumr_bound = thm "sumr_bound";
 val sumr_bound2 = thm "sumr_bound2";
diff -r a0cf3a19ee36 -r 3ce1cb7a24f0 src/HOL/Hyperreal/Transcendental.thy
--- a/src/HOL/Hyperreal/Transcendental.thy	Fri Feb 18 11:48:42 2005 +0100
+++ b/src/HOL/Hyperreal/Transcendental.thy	Fri Feb 18 11:48:53 2005 +0100
@@ -366,7 +366,7 @@
 lemma lemma_realpow_diff_sumr:
      "sumr 0 (Suc n) (%p. (x ^ p) * y ^ ((Suc n) - p)) =  
       y * sumr 0 (Suc n) (%p. (x ^ p) * (y ^ (n - p)))"
-apply (auto simp add: sumr_mult simp del: sumr_Suc)
+apply (auto simp add: setsum_mult simp del: sumr_Suc)
 apply (rule sumr_subst)
 apply (intro strip)
 apply (subst lemma_realpow_diff)
@@ -504,10 +504,10 @@
             simp del: realpow_Suc sumr_Suc)
 apply (auto simp add: lemma_realpow_rev_sumr simp del: sumr_Suc)
 apply (auto simp add: real_of_nat_Suc sumr_diff_mult_const left_distrib 
-                sumdiff lemma_termdiff1 sumr_mult)
+                sumdiff lemma_termdiff1 setsum_mult)
 apply (auto intro!: sumr_subst simp add: diff_minus real_add_assoc)
 apply (simp add: diff_minus [symmetric] less_iff_Suc_add) 
-apply (auto simp add: sumr_mult lemma_realpow_diff_sumr2 mult_ac simp
+apply (auto simp add: setsum_mult lemma_realpow_diff_sumr2 mult_ac simp
                  del: sumr_Suc realpow_Suc)
 done
 
@@ -518,7 +518,7 @@
 apply (subst lemma_termdiff2, assumption)
 apply (simp add: abs_mult mult_commute) 
 apply (simp add: mult_commute [of _ "K ^ (n - 2)"]) 
-apply (rule sumr_rabs [THEN real_le_trans])
+apply (rule setsum_abs [THEN real_le_trans])
 apply (simp add: mult_assoc [symmetric])
 apply (simp add: mult_commute [of _ "real (n - Suc 0)"])
 apply (auto intro!: sumr_bound2 simp add: abs_mult)
@@ -535,7 +535,7 @@
 apply (subgoal_tac [2] "0 \<le> K")
 apply (drule_tac [2] n = d in zero_le_power)
 apply (auto simp del: sumr_Suc)
-apply (rule sumr_rabs [THEN real_le_trans])
+apply (rule setsum_abs [THEN real_le_trans])
 apply (rule sumr_bound2, auto dest!: less_add_one intro!: mult_mono simp add: abs_mult power_add)
 apply (auto intro!: power_mono zero_le_power simp add: power_abs, arith+)
 done
diff -r a0cf3a19ee36 -r 3ce1cb7a24f0 src/HOL/Real/Real.thy
--- a/src/HOL/Real/Real.thy	Fri Feb 18 11:48:42 2005 +0100
+++ b/src/HOL/Real/Real.thy	Fri Feb 18 11:48:53 2005 +0100
@@ -1,2 +1,4 @@
-
-Real = RComplete + RealPow
+theory Real
+imports RComplete RealPow
+begin
+end
\ No newline at end of file