src/HOL/Hyperreal/Series.thy
changeset 15360 300e09825d8b
parent 15251 bb6f072c8d10
child 15536 3ce1cb7a24f0
     1.1 --- a/src/HOL/Hyperreal/Series.thy	Thu Dec 02 11:09:19 2004 +0100
     1.2 +++ b/src/HOL/Hyperreal/Series.thy	Thu Dec 02 11:42:01 2004 +0100
     1.3 @@ -84,7 +84,7 @@
     1.4  done
     1.5  
     1.6  lemma sumr_interval_const2:
     1.7 -     "[|\<forall>n. m \<le> n --> f n = r; m \<le> k|]
     1.8 +     "[|\<forall>n\<ge>m. f n = r; m \<le> k|]
     1.9        ==> sumr m k f = (real (k - m) * r)"
    1.10  apply (induct "k", auto) 
    1.11  apply (drule_tac x = k in spec)
    1.12 @@ -94,7 +94,7 @@
    1.13  
    1.14  
    1.15  lemma sumr_le:
    1.16 -     "[|\<forall>n. m \<le> n --> 0 \<le> f n; m < k|] ==> sumr 0 m f \<le> sumr 0 k f"
    1.17 +     "[|\<forall>n\<ge>m. 0 \<le> f n; m < k|] ==> sumr 0 m f \<le> sumr 0 k f"
    1.18  apply (induct "k")
    1.19  apply (auto simp add: less_Suc_eq_le)
    1.20  apply (drule_tac x = k in spec, safe)
    1.21 @@ -109,7 +109,7 @@
    1.22  apply (auto intro: add_mono simp add: le_def)
    1.23  done
    1.24  
    1.25 -lemma sumr_ge_zero: "(\<forall>n. m \<le> n --> 0 \<le> f n) --> 0 \<le> sumr m n f"
    1.26 +lemma sumr_ge_zero: "(\<forall>n\<ge>m. 0 \<le> f n) --> 0 \<le> sumr m n f"
    1.27  apply (induct "n", auto)
    1.28  apply (drule_tac x = n in spec, arith)
    1.29  done
    1.30 @@ -119,11 +119,11 @@
    1.31  by (induct "n", simp_all add: add_increasing)
    1.32  
    1.33  lemma sumr_zero [rule_format]:
    1.34 -     "\<forall>n. N \<le> n --> f n = 0 ==> N \<le> m --> sumr m n f = 0"
    1.35 +     "\<forall>n \<ge> N. f n = 0 ==> N \<le> m --> sumr m n f = 0"
    1.36  by (induct "n", auto)
    1.37  
    1.38  lemma Suc_le_imp_diff_ge2:
    1.39 -     "[|\<forall>n. N \<le> n --> f (Suc n) = 0; Suc N \<le> m|] ==> sumr m n f = 0"
    1.40 +     "[|\<forall>n \<ge> N. f (Suc n) = 0; Suc N \<le> m|] ==> sumr m n f = 0"
    1.41  apply (rule sumr_zero) 
    1.42  apply (case_tac "n", auto)
    1.43  done
    1.44 @@ -289,7 +289,7 @@
    1.45  great as any partial sum.*}
    1.46  
    1.47  lemma series_pos_le: 
    1.48 -     "[| summable f; \<forall>m. n \<le> m --> 0 \<le> f(m) |] ==> sumr 0 n f \<le> suminf f"
    1.49 +     "[| summable f; \<forall>m \<ge> n. 0 \<le> f(m) |] ==> sumr 0 n f \<le> suminf f"
    1.50  apply (drule summable_sums)
    1.51  apply (simp add: sums_def)
    1.52  apply (cut_tac k = "sumr 0 n f" in LIMSEQ_const)
    1.53 @@ -300,7 +300,7 @@
    1.54  done
    1.55  
    1.56  lemma series_pos_less:
    1.57 -     "[| summable f; \<forall>m. n \<le> m --> 0 < f(m) |] ==> sumr 0 n f < suminf f"
    1.58 +     "[| summable f; \<forall>m \<ge> n. 0 < f(m) |] ==> sumr 0 n f < suminf f"
    1.59  apply (rule_tac y = "sumr 0 (Suc n) f" in order_less_le_trans)
    1.60  apply (rule_tac [2] series_pos_le, auto)
    1.61  apply (drule_tac x = m in spec, auto)
    1.62 @@ -332,14 +332,14 @@
    1.63  
    1.64  lemma summable_Cauchy:
    1.65       "summable f =  
    1.66 -      (\<forall>e. 0 < e --> (\<exists>N. \<forall>m n. N \<le> m --> abs(sumr m n f) < e))"
    1.67 +      (\<forall>e > 0. \<exists>N. \<forall>m \<ge> N. \<forall>n. abs(sumr m n f) < e)"
    1.68  apply (auto simp add: summable_convergent_sumr_iff Cauchy_convergent_iff [symmetric] Cauchy_def)
    1.69  apply (drule_tac [!] spec, auto) 
    1.70  apply (rule_tac x = M in exI)
    1.71  apply (rule_tac [2] x = N in exI, auto)
    1.72  apply (cut_tac [!] m = m and n = n in less_linear, auto)
    1.73  apply (frule le_less_trans [THEN less_imp_le], assumption)
    1.74 -apply (drule_tac x = n in spec)
    1.75 +apply (drule_tac x = n in spec, simp)
    1.76  apply (drule_tac x = m in spec)
    1.77  apply (auto intro: abs_minus_add_cancel [THEN subst]
    1.78              simp add: sumr_split_add_minus abs_minus_add_cancel)
    1.79 @@ -348,7 +348,7 @@
    1.80  text{*Comparison test*}
    1.81  
    1.82  lemma summable_comparison_test:
    1.83 -     "[| \<exists>N. \<forall>n. N \<le> n --> abs(f n) \<le> g n; summable g |] ==> summable f"
    1.84 +     "[| \<exists>N. \<forall>n \<ge> N. abs(f n) \<le> g n; summable g |] ==> summable f"
    1.85  apply (auto simp add: summable_Cauchy)
    1.86  apply (drule spec, auto)
    1.87  apply (rule_tac x = "N + Na" in exI, auto)
    1.88 @@ -362,7 +362,7 @@
    1.89  done
    1.90  
    1.91  lemma summable_rabs_comparison_test:
    1.92 -     "[| \<exists>N. \<forall>n. N \<le> n --> abs(f n) \<le> g n; summable g |] 
    1.93 +     "[| \<exists>N. \<forall>n \<ge> N. abs(f n) \<le> g n; summable g |] 
    1.94        ==> summable (%k. abs (f k))"
    1.95  apply (rule summable_comparison_test)
    1.96  apply (auto simp add: abs_idempotent)
    1.97 @@ -419,7 +419,7 @@
    1.98  
    1.99  (*All this trouble just to get 0<c *)
   1.100  lemma ratio_test_lemma2:
   1.101 -     "[| \<forall>n. N \<le> n --> abs(f(Suc n)) \<le> c*abs(f n) |]  
   1.102 +     "[| \<forall>n \<ge> N. abs(f(Suc n)) \<le> c*abs(f n) |]  
   1.103        ==> 0 < c | summable f"
   1.104  apply (simp (no_asm) add: linorder_not_le [symmetric])
   1.105  apply (simp add: summable_Cauchy)
   1.106 @@ -430,7 +430,7 @@
   1.107  done
   1.108  
   1.109  lemma ratio_test:
   1.110 -     "[| c < 1; \<forall>n. N \<le> n --> abs(f(Suc n)) \<le> c*abs(f n) |]  
   1.111 +     "[| c < 1; \<forall>n \<ge> N. abs(f(Suc n)) \<le> c*abs(f n) |]  
   1.112        ==> summable f"
   1.113  apply (frule ratio_test_lemma2, auto)
   1.114  apply (rule_tac g = "%n. (abs (f N) / (c ^ N))*c ^ n"