src/HOL/Hyperreal/Series.thy
changeset 15229 1eb23f805c06
parent 15140 322485b816ac
child 15234 ec91a90c604e
     1.1 --- a/src/HOL/Hyperreal/Series.thy	Mon Oct 04 15:28:03 2004 +0200
     1.2 +++ b/src/HOL/Hyperreal/Series.thy	Tue Oct 05 15:30:50 2004 +0200
     1.3 @@ -109,22 +109,14 @@
     1.4  apply (auto intro: add_mono simp add: le_def)
     1.5  done
     1.6  
     1.7 -lemma sumr_ge_zero [rule_format (no_asm)]: "(\<forall>n. 0 \<le> f n) --> 0 \<le> sumr m n f"
     1.8 -apply (induct_tac "n", auto)
     1.9 -apply (drule_tac x = n in spec, arith)
    1.10 -done
    1.11 -
    1.12 -lemma sumr_ge_zero2 [rule_format (no_asm)]:
    1.13 -     "(\<forall>n. m \<le> n --> 0 \<le> f n) --> 0 \<le> sumr m n f"
    1.14 +lemma sumr_ge_zero [rule_format]: "(\<forall>n. m \<le> n --> 0 \<le> f n) --> 0 \<le> sumr m n f"
    1.15  apply (induct_tac "n", auto)
    1.16  apply (drule_tac x = n in spec, arith)
    1.17  done
    1.18  
    1.19  lemma rabs_sumr_rabs_cancel [simp]:
    1.20 -     "abs (sumr m n (%n. abs (f n))) = (sumr m n (%n. abs (f n)))"
    1.21 -apply (induct_tac "n")
    1.22 -apply (auto, arith)
    1.23 -done
    1.24 +     "abs (sumr m n (%k. abs (f k))) = (sumr m n (%k. abs (f k)))"
    1.25 +by (induct_tac "n", simp_all add: add_increasing)
    1.26  
    1.27  lemma sumr_zero [rule_format]:
    1.28       "\<forall>n. N \<le> n --> f n = 0 ==> N \<le> m --> sumr m n f = 0"
    1.29 @@ -480,9 +472,6 @@
    1.30  val sumr_diff_mult_const = thm "sumr_diff_mult_const";
    1.31  val sumr_minus_one_realpow_zero = thm "sumr_minus_one_realpow_zero";
    1.32  val sumr_le2 = thm "sumr_le2";
    1.33 -val sumr_ge_zero = thm "sumr_ge_zero";
    1.34 -val sumr_ge_zero2 = thm "sumr_ge_zero2";
    1.35 -val sumr_rabs_ge_zero = thm "sumr_rabs_ge_zero";
    1.36  val rabs_sumr_rabs_cancel = thm "rabs_sumr_rabs_cancel";
    1.37  val sumr_zero = thm "sumr_zero";
    1.38  val Suc_le_imp_diff_ge2 = thm "Suc_le_imp_diff_ge2";