# HG changeset patch
# User huffman
# Date 1159069790 -7200
# Node ID 6df83a636e677995a97a06c27d90cb5ce603565d
# Parent  53cbea20e4d91d56c92d6eb58b80e9354ff35203
generalized types of sums, summable, and suminf

diff -r 53cbea20e4d9 -r 6df83a636e67 src/HOL/Hyperreal/HSeries.thy
--- a/src/HOL/Hyperreal/HSeries.thy	Sun Sep 24 04:16:28 2006 +0200
+++ b/src/HOL/Hyperreal/HSeries.thy	Sun Sep 24 05:49:50 2006 +0200
@@ -213,10 +213,6 @@
 apply (auto intro: HNatInfinite_add_one approx_hrabs_zero_cancel)
 done
 
-text{* Easy to prove stsandard case now *}
-lemma summable_LIMSEQ_zero: "summable f ==> f ----> 0"
-by (simp add: summable_NSsummable_iff LIMSEQ_NSLIMSEQ_iff NSsummable_NSLIMSEQ_zero)
-
 text{*Nonstandard comparison test*}
 lemma NSsummable_comparison_test:
      "[| \<exists>N. \<forall>n. N \<le> n --> abs(f n) \<le> g n; NSsummable g |] ==> NSsummable f"
diff -r 53cbea20e4d9 -r 6df83a636e67 src/HOL/Hyperreal/Ln.thy
--- a/src/HOL/Hyperreal/Ln.thy	Sun Sep 24 04:16:28 2006 +0200
+++ b/src/HOL/Hyperreal/Ln.thy	Sun Sep 24 05:49:50 2006 +0200
@@ -109,14 +109,14 @@
   qed
 qed
 
-lemma aux2: "(%n. x ^ 2 / 2 * (1 / 2) ^ n) sums x^2"
+lemma aux2: "(%n. (x::real) ^ 2 / 2 * (1 / 2) ^ n) sums x^2"
 proof -
-  have "(%n. (1 / 2)^n) sums (1 / (1 - (1/2)))"
+  have "(%n. (1 / 2::real)^n) sums (1 / (1 - (1/2)))"
     apply (rule geometric_sums)
     by (simp add: abs_interval_iff)
   also have "(1::real) / (1 - 1/2) = 2"
     by simp
-  finally have "(%n. (1 / 2)^n) sums 2" .
+  finally have "(%n. (1 / 2::real)^n) sums 2" .
   then have "(%n. x ^ 2 / 2 * (1 / 2) ^ n) sums (x^2 / 2 * 2)"
     by (rule sums_mult)
   also have "x^2 / 2 * 2 = x^2"
diff -r 53cbea20e4d9 -r 6df83a636e67 src/HOL/Hyperreal/Series.thy
--- a/src/HOL/Hyperreal/Series.thy	Sun Sep 24 04:16:28 2006 +0200
+++ b/src/HOL/Hyperreal/Series.thy	Sun Sep 24 05:49:50 2006 +0200
@@ -13,21 +13,19 @@
 imports SEQ Lim
 begin
 
-declare atLeastLessThan_iff[iff]
-declare setsum_op_ivl_Suc[simp]
-
 definition
-   sums  :: "(nat => real) => real => bool"     (infixr "sums" 80)
+   sums  :: "(nat \<Rightarrow> 'a::real_normed_vector) \<Rightarrow> 'a \<Rightarrow> bool"
+     (infixr "sums" 80)
    "f sums s = (%n. setsum f {0..<n}) ----> s"
 
-   summable :: "(nat=>real) => bool"
+   summable :: "(nat \<Rightarrow> 'a::real_normed_vector) \<Rightarrow> bool"
    "summable f = (\<exists>s. f sums s)"
 
-   suminf   :: "(nat=>real) => real"
+   suminf   :: "(nat \<Rightarrow> 'a::real_normed_vector) \<Rightarrow> 'a"
    "suminf f = (THE s. f sums s)"
 
 syntax
-  "_suminf" :: "idt => real => real"    ("\<Sum>_. _" [0, 10] 10)
+  "_suminf" :: "idt \<Rightarrow> 'a \<Rightarrow> 'a" ("\<Sum>_. _" [0, 10] 10)
 translations
   "\<Sum>i. b" == "suminf (%i. b)"
 
@@ -50,9 +48,7 @@
 (* FIXME this is an awful lemma! *)
 lemma sumr_one_lb_realpow_zero [simp]:
   "(\<Sum>n=Suc 0..<n. f(n) * (0::real) ^ n) = 0"
-apply (induct "n")
-apply (case_tac [2] "n", auto)
-done
+by (rule setsum_0', simp)
 
 lemma sumr_group:
      "(\<Sum>m=0..<n::nat. setsum f {m * k ..< m*k + k}) = setsum f {0 ..< n * k}"
@@ -61,23 +57,24 @@
 apply (simp_all add: setsum_add_nat_ivl add_commute)
 done
 
-(* FIXME generalize? *)
+lemma sumr_offset3:
+  "setsum f {0::nat..<n+k} = (\<Sum>m=0..<n. f (m+k)) + setsum f {0..<k}"
+apply (subst setsum_shift_bounds_nat_ivl [symmetric])
+apply (simp add: setsum_add_nat_ivl add_commute)
+done
+
 lemma sumr_offset:
- "(\<Sum>m=0..<n::nat. f(m+k)::real) = setsum f {0..<n+k} - setsum f {0..<k}"
-by (induct "n", auto)
+  fixes f :: "nat \<Rightarrow> 'a::ab_group_add"
+  shows "(\<Sum>m=0..<n. f(m+k)) = setsum f {0..<n+k} - setsum f {0..<k}"
+by (simp add: sumr_offset3)
 
 lemma sumr_offset2:
  "\<forall>f. (\<Sum>m=0..<n::nat. f(m+k)::real) = setsum f {0..<n+k} - setsum f {0..<k}"
-by (induct "n", auto)
-
-lemma sumr_offset3:
-  "setsum f {0::nat..<n+k} = (\<Sum>m=0..<n. f (m+k)::real) + setsum f {0..<k}"
-by (simp  add: sumr_offset)
+by (simp add: sumr_offset)
 
 lemma sumr_offset4:
- "\<forall>n f. setsum f {0::nat..<n+k} =
-        (\<Sum>m=0..<n. f (m+k)::real) + setsum f {0..<k}"
-by (simp add: sumr_offset)
+  "\<forall>n f. setsum f {0::nat..<n+k} = (\<Sum>m=0..<n. f (m+k)::real) + setsum f {0..<k}"
+by (clarify, rule sumr_offset3)
 
 (*
 lemma sumr_from_1_from_0: "0 < n ==>
@@ -165,45 +162,61 @@
   apply (rule sums_zero);
 done;
   
-lemma sums_mult: "f sums a ==> (%n. c * f n) sums (c * a)"
+lemma sums_mult:
+  fixes c :: "'a::real_normed_algebra"
+  shows "f sums a \<Longrightarrow> (\<lambda>n. c * f n) sums (c * a)"
 by (auto simp add: sums_def setsum_right_distrib [symmetric]
          intro!: LIMSEQ_mult intro: LIMSEQ_const)
 
-lemma summable_mult: "summable f ==> summable (%n. c * f n)";
+lemma summable_mult:
+  fixes c :: "'a::real_normed_algebra"
+  shows "summable f \<Longrightarrow> summable (%n. c * f n)";
   apply (unfold summable_def);
   apply (auto intro: sums_mult);
 done;
 
-lemma suminf_mult: "summable f ==> suminf (%n. c * f n) = c * suminf f";
+lemma suminf_mult:
+  fixes c :: "'a::real_normed_algebra"
+  shows "summable f \<Longrightarrow> suminf (\<lambda>n. c * f n) = c * suminf f";
   apply (rule sym);
   apply (rule sums_unique);
   apply (rule sums_mult);
   apply (erule summable_sums);
 done;
 
-lemma sums_mult2: "f sums a ==> (%n. f n * c) sums (a * c)"
-apply (subst mult_commute)
-apply (subst mult_commute);back;
-apply (erule sums_mult)
-done
+lemma sums_mult2:
+  fixes c :: "'a::real_normed_algebra"
+  shows "f sums a \<Longrightarrow> (\<lambda>n. f n * c) sums (a * c)"
+by (auto simp add: sums_def setsum_left_distrib [symmetric]
+         intro!: LIMSEQ_mult LIMSEQ_const)
 
-lemma summable_mult2: "summable f ==> summable (%n. f n * c)"
+lemma summable_mult2:
+  fixes c :: "'a::real_normed_algebra"
+  shows "summable f \<Longrightarrow> summable (\<lambda>n. f n * c)"
   apply (unfold summable_def)
   apply (auto intro: sums_mult2)
 done
 
-lemma suminf_mult2: "summable f ==> suminf f * c = (\<Sum>n. f n * c)"
-by (auto intro!: sums_unique sums_mult summable_sums simp add: mult_commute)
+lemma suminf_mult2:
+  fixes c :: "'a::real_normed_algebra"
+  shows "summable f \<Longrightarrow> suminf f * c = (\<Sum>n. f n * c)"
+by (auto intro!: sums_unique sums_mult2 summable_sums)
 
-lemma sums_divide: "f sums a ==> (%n. (f n)/c) sums (a/c)"
-by (simp add: real_divide_def sums_mult mult_commute [of _ "inverse c"])
+lemma sums_divide:
+  fixes c :: "'a::real_normed_field"
+  shows "f sums a \<Longrightarrow> (\<lambda>n. f n / c) sums (a / c)"
+by (simp add: divide_inverse sums_mult2)
 
-lemma summable_divide: "summable f ==> summable (%n. (f n) / c)";
+lemma summable_divide:
+  fixes c :: "'a::real_normed_field"
+  shows "summable f \<Longrightarrow> summable (\<lambda>n. f n / c)"
   apply (unfold summable_def);
   apply (auto intro: sums_divide);
 done;
 
-lemma suminf_divide: "summable f ==> suminf (%n. (f n) / c) = (suminf f) / c";
+lemma suminf_divide:
+  fixes c :: "'a::real_normed_field"
+  shows "summable f \<Longrightarrow> suminf (\<lambda>n. f n / c) = suminf f / c"
   apply (rule sym);
   apply (rule sums_unique);
   apply (rule sums_divide);
@@ -258,78 +271,94 @@
 lemma sums_group:
      "[|summable f; 0 < k |] ==> (%n. setsum f {n*k..<n*k+k}) sums (suminf f)"
 apply (drule summable_sums)
-apply (auto simp add: sums_def LIMSEQ_def sumr_group)
-apply (drule_tac x = r in spec, safe)
-apply (rule_tac x = no in exI, safe)
-apply (drule_tac x = "n*k" in spec)
-apply (auto dest!: not_leE)
-apply (drule_tac j = no in less_le_trans, auto)
-done
-
-lemma sumr_pos_lt_pair_lemma:
-  "[|\<forall>d. - f (n + (d + d)) < (f (Suc (n + (d + d))) :: real) |]
-   ==> setsum f {0..<n+Suc(Suc 0)} \<le> setsum f {0..<Suc(Suc 0) * Suc no + n}"
-apply (induct "no", auto)
-apply (drule_tac x = "Suc no" in spec)
-apply (simp add: add_ac)
-done
-
-lemma sumr_pos_lt_pair:
-     "[|summable f; 
-        \<forall>d. 0 < (f(n + (Suc(Suc 0) * d))) + f(n + ((Suc(Suc 0) * d) + 1))|]  
-      ==> setsum f {0..<n} < suminf f"
-apply (drule summable_sums)
-apply (auto simp add: sums_def LIMSEQ_def)
-apply (drule_tac x = "f (n) + f (n + 1)" in spec)
-apply (auto iff: real_0_less_add_iff)
-   --{*legacy proof: not necessarily better!*}
-apply (rule_tac [2] ccontr, drule_tac [2] linorder_not_less [THEN iffD1])
-apply (frule_tac [2] no=no in sumr_pos_lt_pair_lemma) 
-apply (drule_tac x = 0 in spec, simp)
-apply (rotate_tac 1, drule_tac x = "Suc (Suc 0) * (Suc no) + n" in spec)
-apply (safe, simp)
-apply (subgoal_tac "suminf f + (f (n) + f (n + 1)) \<le>
- setsum f {0 ..< Suc (Suc 0) * (Suc no) + n}")
-apply (rule_tac [2] y = "setsum f {0..<n+ Suc (Suc 0)}" in order_trans)
-prefer 3 apply assumption
-apply (rule_tac [2] y = "setsum f {0..<n} + (f (n) + f (n + 1))" in order_trans)
-apply simp_all
+apply (simp only: sums_def sumr_group)
+apply (unfold LIMSEQ_def, safe)
+apply (drule_tac x="r" in spec, safe)
+apply (rule_tac x="no" in exI, safe)
+apply (drule_tac x="n*k" in spec)
+apply (erule mp)
+apply (erule order_trans)
+apply simp
 done
 
 text{*A summable series of positive terms has limit that is at least as
 great as any partial sum.*}
 
-lemma series_pos_le: 
-     "[| summable f; \<forall>m \<ge> n. 0 \<le> f(m) |] ==> setsum f {0..<n} \<le> suminf f"
+lemma series_pos_le:
+  fixes f :: "nat \<Rightarrow> real"
+  shows "\<lbrakk>summable f; \<forall>m\<ge>n. 0 \<le> f m\<rbrakk> \<Longrightarrow> setsum f {0..<n} \<le> suminf f"
 apply (drule summable_sums)
 apply (simp add: sums_def)
 apply (cut_tac k = "setsum f {0..<n}" in LIMSEQ_const)
 apply (erule LIMSEQ_le, blast)
-apply (rule_tac x = n in exI, clarify)
+apply (rule_tac x="n" in exI, clarify)
 apply (rule setsum_mono2)
 apply auto
 done
 
 lemma series_pos_less:
-     "[| summable f; \<forall>m \<ge> n. 0 < f(m) |] ==> setsum f {0..<n} < suminf f"
-apply (rule_tac y = "setsum f {0..<Suc n}" in order_less_le_trans)
-apply (rule_tac [2] series_pos_le, auto)
-apply (drule_tac x = m in spec, auto)
+  fixes f :: "nat \<Rightarrow> real"
+  shows "\<lbrakk>summable f; \<forall>m\<ge>n. 0 < f m\<rbrakk> \<Longrightarrow> setsum f {0..<n} < suminf f"
+apply (rule_tac y="setsum f {0..<Suc n}" in order_less_le_trans)
+apply simp
+apply (erule series_pos_le)
+apply (simp add: order_less_imp_le)
+done
+
+lemma suminf_gt_zero:
+  fixes f :: "nat \<Rightarrow> real"
+  shows "\<lbrakk>summable f; \<forall>n. 0 < f n\<rbrakk> \<Longrightarrow> 0 < suminf f"
+by (drule_tac n="0" in series_pos_less, simp_all)
+
+lemma suminf_ge_zero:
+  fixes f :: "nat \<Rightarrow> real"
+  shows "\<lbrakk>summable f; \<forall>n. 0 \<le> f n\<rbrakk> \<Longrightarrow> 0 \<le> suminf f"
+by (drule_tac n="0" in series_pos_le, simp_all)
+
+lemma sumr_pos_lt_pair:
+  fixes f :: "nat \<Rightarrow> real"
+  shows "\<lbrakk>summable f;
+        \<forall>d. 0 < f (k + (Suc(Suc 0) * d)) + f (k + ((Suc(Suc 0) * d) + 1))\<rbrakk>
+      \<Longrightarrow> setsum f {0..<k} < suminf f"
+apply (subst suminf_split_initial_segment [where k="k"])
+apply assumption
+apply simp
+apply (drule_tac k="k" in summable_ignore_initial_segment)
+apply (drule_tac k="Suc (Suc 0)" in sums_group, simp)
+apply simp
+apply (frule sums_unique)
+apply (drule sums_summable)
+apply simp
+apply (erule suminf_gt_zero)
+apply (simp add: add_ac)
 done
 
 text{*Sum of a geometric progression.*}
 
 lemmas sumr_geometric = geometric_sum [where 'a = real]
 
-lemma geometric_sums: "abs(x) < 1 ==> (%n. x ^ n) sums (1/(1 - x))"
-apply (case_tac "x = 1")
-apply (auto dest!: LIMSEQ_rabs_realpow_zero2 
-        simp add: sumr_geometric sums_def diff_minus add_divide_distrib)
-apply (subgoal_tac "1 / (1 + -x) = 0/ (x - 1) + - 1/ (x - 1) ")
-apply (erule ssubst)
-apply (rule LIMSEQ_add, rule LIMSEQ_divide)
-apply (auto intro: LIMSEQ_const simp add: diff_minus minus_divide_right LIMSEQ_rabs_realpow_zero2)
-done
+lemma geometric_sums:
+  fixes x :: "'a::{real_normed_field,recpower,division_by_zero}"
+  shows "norm x < 1 \<Longrightarrow> (\<lambda>n. x ^ n) sums (1 / (1 - x))"
+proof -
+  assume less_1: "norm x < 1"
+  hence neq_1: "x \<noteq> 1" by auto
+  hence neq_0: "x - 1 \<noteq> 0" by simp
+  from less_1 have lim_0: "(\<lambda>n. x ^ n) ----> 0"
+    by (rule LIMSEQ_power_zero)
+  hence "(\<lambda>n. x ^ n / (x - 1) - 1 / (x - 1)) ----> 0 / (x - 1) - 1 / (x
+- 1)"
+    using neq_0 by (intro LIMSEQ_divide LIMSEQ_diff LIMSEQ_const)
+  hence "(\<lambda>n. (x ^ n - 1) / (x - 1)) ----> 1 / (1 - x)"
+    by (simp add: nonzero_minus_divide_right [OF neq_0] diff_divide_distrib)
+  thus "(\<lambda>n. x ^ n) sums (1 / (1 - x))"
+    by (simp add: sums_def geometric_sum neq_1)
+qed
+
+lemma summable_geometric:
+  fixes x :: "'a::{real_normed_field,recpower,division_by_zero}"
+  shows "norm x < 1 \<Longrightarrow> summable (\<lambda>n. x ^ n)"
+by (rule geometric_sums [THEN sums_summable])
 
 text{*Cauchy-type criterion for convergence of series (c.f. Harrison)*}
 
@@ -339,7 +368,7 @@
 
 lemma summable_LIMSEQ_zero: "summable f \<Longrightarrow> f ----> 0"
 apply (drule summable_convergent_sumr_iff [THEN iffD1])
-apply (drule Cauchy_convergent_iff [THEN iffD2])
+apply (drule convergent_Cauchy)
 apply (simp only: Cauchy_def LIMSEQ_def, safe)
 apply (drule_tac x="r" in spec, safe)
 apply (rule_tac x="M" in exI, safe)
@@ -348,7 +377,7 @@
 done
 
 lemma summable_Cauchy:
-     "summable f =  
+     "summable (f::nat \<Rightarrow> real) =  
       (\<forall>e > 0. \<exists>N. \<forall>m \<ge> N. \<forall>n. abs(setsum f {m..<n}) < e)"
 apply (simp only: summable_convergent_sumr_iff Cauchy_convergent_iff [symmetric] Cauchy_def diff_minus [symmetric], safe)
 apply (drule spec, drule (1) mp)
@@ -369,11 +398,23 @@
 
 text{*Comparison test*}
 
+lemma norm_setsum:
+  fixes f :: "'a \<Rightarrow> 'b::real_normed_vector"
+  shows "norm (setsum f A) \<le> (\<Sum>i\<in>A. norm (f i))"
+apply (case_tac "finite A")
+apply (erule finite_induct)
+apply simp
+apply simp
+apply (erule order_trans [OF norm_triangle_ineq add_left_mono])
+apply simp
+done
+
 lemma summable_comparison_test:
-     "[| \<exists>N. \<forall>n \<ge> N. abs(f n) \<le> g n; summable g |] ==> summable f"
-apply (auto simp add: summable_Cauchy)
-apply (drule spec, auto)
-apply (rule_tac x = "N + Na" in exI, auto)
+  fixes f :: "nat \<Rightarrow> real"
+  shows "\<lbrakk>\<exists>N. \<forall>n\<ge>N. \<bar>f n\<bar> \<le> g n; summable g\<rbrakk> \<Longrightarrow> summable f"
+apply (simp add: summable_Cauchy, safe)
+apply (drule_tac x="e" in spec, safe)
+apply (rule_tac x = "N + Na" in exI, safe)
 apply (rotate_tac 2)
 apply (drule_tac x = m in spec)
 apply (auto, rotate_tac 2, drule_tac x = n in spec)
@@ -384,8 +425,8 @@
 done
 
 lemma summable_rabs_comparison_test:
-     "[| \<exists>N. \<forall>n \<ge> N. abs(f n) \<le> g n; summable g |] 
-      ==> summable (%k. abs (f k))"
+  fixes f :: "nat \<Rightarrow> real"
+  shows "\<lbrakk>\<exists>N. \<forall>n\<ge>N. \<bar>f n\<bar> \<le> g n; summable g\<rbrakk> \<Longrightarrow> summable (\<lambda>n. \<bar>f n\<bar>)"
 apply (rule summable_comparison_test)
 apply (auto)
 done
@@ -393,16 +434,17 @@
 text{*Limit comparison property for series (c.f. jrh)*}
 
 lemma summable_le:
-     "[|\<forall>n. f n \<le> g n; summable f; summable g |] ==> suminf f \<le> suminf g"
+  fixes f g :: "nat \<Rightarrow> real"
+  shows "\<lbrakk>\<forall>n. f n \<le> g n; summable f; summable g\<rbrakk> \<Longrightarrow> suminf f \<le> suminf g"
 apply (drule summable_sums)+
-apply (auto intro!: LIMSEQ_le simp add: sums_def)
+apply (simp only: sums_def, erule (1) LIMSEQ_le)
 apply (rule exI)
 apply (auto intro!: setsum_mono)
 done
 
 lemma summable_le2:
-     "[|\<forall>n. abs(f n) \<le> g n; summable g |]  
-      ==> summable f & suminf f \<le> suminf g"
+  fixes f g :: "nat \<Rightarrow> real"
+  shows "\<lbrakk>\<forall>n. \<bar>f n\<bar> \<le> g n; summable g\<rbrakk> \<Longrightarrow> summable f \<and> suminf f \<le> suminf g"
 apply (auto intro: summable_comparison_test intro!: summable_le)
 apply (simp add: abs_le_interval_iff)
 done
@@ -423,18 +465,21 @@
 
 
 text{*Absolute convergence imples normal convergence*}
-lemma summable_rabs_cancel: "summable (%n. abs (f n)) ==> summable f"
-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 = "\<Sum>n=m..<n. abs(f n)" in order_le_less_trans)
-apply (auto)
+lemma summable_rabs_cancel:
+  fixes f :: "nat \<Rightarrow> real"
+  shows "summable (\<lambda>n. \<bar>f n\<bar>) \<Longrightarrow> summable f"
+apply (simp only: summable_Cauchy, safe)
+apply (drule_tac x="e" in spec, safe)
+apply (rule_tac x="N" in exI, safe)
+apply (drule_tac x="m" in spec, safe)
+apply (rule order_le_less_trans [OF setsum_abs])
+apply simp
 done
 
 text{*Absolute convergence of series*}
 lemma summable_rabs:
-     "summable (%n. abs (f n)) ==> abs(suminf f) \<le> (\<Sum>n. abs(f n))"
+  fixes f :: "nat \<Rightarrow> real"
+  shows "summable (\<lambda>n. \<bar>f n\<bar>) \<Longrightarrow> \<bar>suminf f\<bar> \<le> (\<Sum>n. \<bar>f n\<bar>)"
 by (auto intro: LIMSEQ_le LIMSEQ_imp_rabs summable_rabs_cancel summable_sumr_LIMSEQ_suminf)
 
 
@@ -456,8 +501,8 @@
 
 (*All this trouble just to get 0<c *)
 lemma ratio_test_lemma2:
-     "[| \<forall>n \<ge> N. abs(f(Suc n)) \<le> c*abs(f n) |]  
-      ==> 0 < c | summable f"
+  fixes f :: "nat \<Rightarrow> real"
+  shows "\<lbrakk>\<forall>n\<ge>N. \<bar>f (Suc n)\<bar> \<le> c * \<bar>f n\<bar>\<rbrakk> \<Longrightarrow> 0 < c \<or> summable f"
 apply (simp (no_asm) add: linorder_not_le [symmetric])
 apply (simp add: summable_Cauchy)
 apply (safe, subgoal_tac "\<forall>n. N < n --> f (n) = 0")
@@ -471,8 +516,8 @@
 done
 
 lemma ratio_test:
-     "[| c < 1; \<forall>n \<ge> N. abs(f(Suc n)) \<le> c*abs(f n) |]  
-      ==> summable f"
+  fixes f :: "nat \<Rightarrow> real"
+  shows "\<lbrakk>c < 1; \<forall>n\<ge>N. \<bar>f (Suc n)\<bar> \<le> c * \<bar>f n\<bar>\<rbrakk> \<Longrightarrow> summable f"
 apply (frule ratio_test_lemma2, auto)
 apply (rule_tac g = "%n. (abs (f N) / (c ^ N))*c ^ n" 
        in summable_comparison_test)
diff -r 53cbea20e4d9 -r 6df83a636e67 src/HOL/Hyperreal/Transcendental.thy
--- a/src/HOL/Hyperreal/Transcendental.thy	Sun Sep 24 04:16:28 2006 +0200
+++ b/src/HOL/Hyperreal/Transcendental.thy	Sun Sep 24 05:49:50 2006 +0200
@@ -176,6 +176,8 @@
 x}, then it sums absolutely for @{term z} with @{term "\<bar>z\<bar> < \<bar>x\<bar>"}.*}
 
 lemma powser_insidea:
+  fixes f :: "nat \<Rightarrow> real"
+  shows
      "[| summable (%n. f(n) * (x ^ n)); \<bar>z\<bar> < \<bar>x\<bar> |]  
       ==> summable (%n. \<bar>f(n)\<bar> * (z ^ n))"
 apply (drule summable_LIMSEQ_zero)
@@ -207,6 +209,8 @@
 done
 
 lemma powser_inside:
+  fixes f :: "nat \<Rightarrow> real"
+  shows
      "[| summable (%n. f(n) * (x ^ n)); \<bar>z\<bar> < \<bar>x\<bar> |]  
       ==> summable (%n. f(n) * (z ^ n))"
 apply (drule_tac z = "\<bar>z\<bar>" in powser_insidea)
@@ -342,7 +346,7 @@
 done
 
 lemma lemma_termdiff5:
-     "[| 0 < k;  
+     "[| 0 < (k::real);  
             summable f;  
             \<forall>h. 0 < \<bar>h\<bar> & \<bar>h\<bar> < k -->  
                     (\<forall>n. abs(g(h) (n::nat)) \<le> (f(n) * \<bar>h\<bar>)) |]