# HG changeset patch
# User paulson
# Date 1077811703 -3600
# Node ID 1f256287d4f0f364b7c511f2eb6859aada3f350b
# Parent  60aa114e2dba782dd28deefb2c8a8f112894e48a
converted Hyperreal/Series to Isar script

diff -r 60aa114e2dba -r 1f256287d4f0 src/HOL/Hyperreal/Series.ML
--- a/src/HOL/Hyperreal/Series.ML	Thu Feb 26 11:31:36 2004 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,600 +0,0 @@
-(*  Title       : Series.ML
-    Author      : Jacques D. Fleuriot
-    Copyright   : 1998  University of Cambridge
-                : 1999  University of Edinburgh
-    Description : Finite summation and infinite series
-*) 
-
-Goal "sumr (Suc n) n f = 0";
-by (induct_tac "n" 1);
-by (Auto_tac);
-qed "sumr_Suc_zero";
-Addsimps [sumr_Suc_zero];
-
-Goal "sumr m m f = 0";
-by (induct_tac "m" 1);
-by (Auto_tac);
-qed "sumr_eq_bounds";
-Addsimps [sumr_eq_bounds];
-
-Goal "sumr m (Suc m) f = f(m)";
-by (Auto_tac);
-qed "sumr_Suc_eq";
-Addsimps [sumr_Suc_eq];
-
-Goal "sumr (m+k) k f = 0";
-by (induct_tac "k" 1);
-by (Auto_tac);
-qed "sumr_add_lbound_zero";
-Addsimps [sumr_add_lbound_zero];
-
-Goal "sumr m n f + sumr m n g = sumr m n (%n. f n + g n)";
-by (induct_tac "n" 1);
-by (auto_tac (claset(),simpset() addsimps add_ac));
-qed "sumr_add";
-
-Goal "r * sumr m n f = sumr m n (%n. r * f n)";
-by (induct_tac "n" 1);
-by (Auto_tac);
-by (auto_tac (claset(),simpset() addsimps 
-    [right_distrib]));
-qed "sumr_mult";
-
-Goal "n < p --> sumr 0 n f + sumr n p f = sumr 0 p f";
-by (induct_tac "p" 1);
-by (auto_tac (claset() addSDs [CLAIM "n < Suc na ==> n <= na",
-    leI] addDs [le_anti_sym], simpset()));
-qed_spec_mp "sumr_split_add";
-
-Goal "n < p ==> sumr 0 p f + \
-\                - sumr 0 n f = sumr n p f";
-by (dres_inst_tac [("f1","f")] (sumr_split_add RS sym) 1);
-by (asm_simp_tac (simpset() addsimps add_ac) 1);
-qed "sumr_split_add_minus";
-
-Goal "0 < n --> n < p --> sumr (Suc 0) n f + sumr n p f = sumr (Suc 0) p f";
-by (induct_tac "p" 1);
-by (auto_tac (claset() addSDs [CLAIM "[| m < Suc n; n <= m |] ==> m = n"],
-    simpset()));
-qed_spec_mp "sumr_split_add2";
-
-Goal "[| 0<n; n <= p |] ==> sumr (Suc 0) n f + sumr n p f = sumr (Suc 0) p f";
-by (dtac le_imp_less_or_eq 1 THEN Auto_tac);
-by (blast_tac (claset() addIs [sumr_split_add2]) 1);
-qed "sumr_split_add3";
-
-Goal "abs(sumr m n f) <= sumr m n (%i. abs(f i))";
-by (induct_tac "n" 1);
-by (auto_tac (claset() addIs [abs_triangle_ineq RS order_trans,
-                              add_right_mono], 
-              simpset()));
-qed "sumr_rabs";
-
-Goal "!!f g. (ALL r. m <= r & r < n --> f r = g r) \
-\                --> sumr m n f = sumr m n g";
-by (induct_tac "n" 1);
-by (Auto_tac);
-qed_spec_mp "sumr_fun_eq";
-
-Goal "sumr 0 n (%i. r) = real n * r";
-by (induct_tac "n" 1);
-by (auto_tac (claset(),
-              simpset() addsimps [left_distrib,real_of_nat_zero,
-                                  real_of_nat_Suc]));
-qed "sumr_const";
-Addsimps [sumr_const];
-
-Goal "sumr 0 n f + -(real n * r) = sumr 0 n (%i. f i + -r)";
-by (full_simp_tac (HOL_ss addsimps [sumr_add RS sym, minus_mult_right]) 1);
-by (Simp_tac 1);
-qed "sumr_add_mult_const";
-
-Goalw [real_diff_def] 
-     "sumr 0 n f - (real n*r) = sumr 0 n (%i. f i - r)";
-by (full_simp_tac (simpset() addsimps [sumr_add_mult_const]) 1);
-qed "sumr_diff_mult_const";
-
-Goal "n < m --> sumr m n f = 0";
-by (induct_tac "n" 1);
-by (auto_tac (claset() addDs [less_imp_le], simpset()));
-qed_spec_mp "sumr_less_bounds_zero";
-Addsimps [sumr_less_bounds_zero];
-
-Goal "sumr m n (%i. - f i) = - sumr m n f";
-by (induct_tac "n" 1);
-by (case_tac "Suc n <= m" 2);
-by (auto_tac (claset(),simpset() addsimps [minus_add_distrib]));
-qed "sumr_minus";
-
-Goal "sumr (m+k) (n+k) f = sumr m n (%i. f(i + k))";
-by (induct_tac "n" 1);
-by (Auto_tac);
-qed "sumr_shift_bounds";
-
-Goal "sumr 0 (2*n) (%i. (-1) ^ Suc i) = 0";
-by (induct_tac "n" 1);
-by (Auto_tac);
-qed "sumr_minus_one_realpow_zero";
-Addsimps [sumr_minus_one_realpow_zero];
-
-Goal "m < Suc n ==> Suc n - m = Suc (n - m)";
-by (dtac less_imp_Suc_add 1);
-by (Auto_tac);
-val Suc_diff_n = result();
-
-Goal "(ALL n. m <= Suc n --> f n = r) & m <= na \
-\                --> sumr m na f = (real (na - m) * r)";
-by (induct_tac "na" 1);
-by (Step_tac 1);
-by (asm_full_simp_tac (simpset() addsimps [le_Suc_eq])  2);
-by (Step_tac 1);
-by (dres_inst_tac [("x","n")] spec 3);
-by (auto_tac (claset() addSDs [le_imp_less_or_eq], simpset()));
-by (asm_simp_tac (simpset() addsimps [left_distrib, Suc_diff_n,
-                                      real_of_nat_Suc]) 1);
-qed_spec_mp "sumr_interval_const";
-
-Goal "(ALL n. m <= n --> f n = r) & m <= na \
-\     --> sumr m na f = (real (na - m) * r)";
-by (induct_tac "na" 1);
-by (Step_tac 1);
-by (asm_full_simp_tac (simpset() addsimps [le_Suc_eq])  2);
-by (Step_tac 1);
-by (dres_inst_tac [("x","n")] spec 3);
-by (auto_tac (claset() addSDs [le_imp_less_or_eq],
-    simpset()));
-by (asm_simp_tac (simpset() addsimps [Suc_diff_n, left_distrib,
-                                      real_of_nat_Suc]) 1);
-qed_spec_mp "sumr_interval_const2";
-
-Goal "(ALL n. m <= n --> 0 <= f n) & m < k --> sumr 0 m f <= sumr 0 k f";
-by (induct_tac "k" 1);
-by (Step_tac 1);
-by (ALLGOALS(asm_full_simp_tac (simpset() addsimps [less_Suc_eq_le])));
-by (ALLGOALS(dres_inst_tac [("x","n")] spec));
-by (Step_tac 1);
-by (dtac le_imp_less_or_eq 1 THEN Step_tac 1);
-by (dres_inst_tac [("a","sumr 0 m f")] add_mono 2);
-by (dres_inst_tac [("a","sumr 0 m f")] (order_refl RS add_mono) 1);
-by (Auto_tac);
-qed_spec_mp "sumr_le";
-
-Goal "!!f g. (ALL r. m <= r & r < n --> f r <= g r) \
-\                --> sumr m n f <= sumr m n g";
-by (induct_tac "n" 1);
-by (auto_tac (claset() addIs [add_mono],
-    simpset() addsimps [le_def]));
-qed_spec_mp "sumr_le2";
-
-Goal "(ALL n. 0 <= f n) --> 0 <= sumr m n f";
-by (induct_tac "n" 1);
-by Auto_tac;
-by (dres_inst_tac [("x","n")] spec 1);
-by (arith_tac 1);
-qed_spec_mp "sumr_ge_zero";
-
-Goal "(ALL n. m <= n --> 0 <= f n) --> 0 <= sumr m n f";
-by (induct_tac "n" 1);
-by Auto_tac;
-by (dres_inst_tac [("x","n")] spec 1);
-by (arith_tac 1);
-qed_spec_mp "sumr_ge_zero2";
-
-Goal "0 <= sumr m n (%n. abs (f n))";
-by (induct_tac "n" 1);
-by Auto_tac;
-by (arith_tac 1);
-qed "sumr_rabs_ge_zero";
-Addsimps [sumr_rabs_ge_zero];
-AddSIs [sumr_rabs_ge_zero]; 
-
-Goal "abs (sumr m n (%n. abs (f n))) = (sumr m n (%n. abs (f n)))";
-by (induct_tac "n" 1);
-by (Auto_tac THEN arith_tac 1);
-qed "rabs_sumr_rabs_cancel";
-Addsimps [rabs_sumr_rabs_cancel];
-
-Goal "ALL n. N <= n --> f n = 0 \
-\     ==> ALL m n. N <= m --> sumr m n f = 0";   
-by (Step_tac 1);
-by (induct_tac "n" 1);
-by (Auto_tac);
-qed "sumr_zero";
-
-Goal "ALL n. N <= n --> f (Suc n) = 0 \
-\     ==> ALL m n. Suc N <= m --> sumr m n f = 0";   
-by (rtac sumr_zero 1 THEN Step_tac 1);
-by (case_tac "n" 1);
-by Auto_tac; 
-qed "Suc_le_imp_diff_ge2";
-
-Goal "sumr (Suc 0) n (%n. f(n) * 0 ^ n) = 0";
-by (induct_tac "n" 1);
-by (case_tac "n" 2);
-by Auto_tac; 
-qed "sumr_one_lb_realpow_zero";
-Addsimps [sumr_one_lb_realpow_zero];
-
-Goalw [real_diff_def] "sumr m n f - sumr m n g = sumr m n (%n. f n - g n)";
-by (simp_tac (simpset() addsimps [sumr_add RS sym,sumr_minus]) 1);
-qed "sumr_diff";
-
-Goal "(ALL p. m <= p & p < m+n --> (f p = g p)) --> sumr m n f = sumr m n g";
-by (induct_tac "n" 1);
-by (Auto_tac);
-qed_spec_mp "sumr_subst";
-
-Goal "(ALL p. m <= p & p < m + n --> (f(p) <= K)) \
-\     --> (sumr m (m + n) f <= (real n * K))";
-by (induct_tac "n" 1);
-by (auto_tac (claset() addIs [add_mono],
-              simpset() addsimps [left_distrib, real_of_nat_Suc]));
-qed_spec_mp "sumr_bound";
-
-Goal "(ALL p. 0 <= p & p < n --> (f(p) <= K)) \
-\     --> (sumr 0 n f <= (real n * K))";
-by (induct_tac "n" 1);
-by (auto_tac (claset() addIs [add_mono],
-        simpset() addsimps [left_distrib, real_of_nat_Suc]));
-qed_spec_mp "sumr_bound2";
-
-Goal "sumr 0 n (%m. sumr (m * k) (m*k + k) f) = sumr 0 (n * k) f";
-by (subgoal_tac "k = 0 | 0 < k" 1);
-by (Auto_tac);
-by (induct_tac "n" 1);
-by (auto_tac (claset(),simpset() addsimps [sumr_split_add,add_commute]));
-qed "sumr_group";
-Addsimps [sumr_group];
-
-(*-------------------------------------------------------------------
-                        Infinite sums
-    Theorems follow from properties of limits and sums
- -------------------------------------------------------------------*)
-(*----------------------
-   suminf is the sum   
- ---------------------*)
-Goalw [sums_def,summable_def] 
-      "f sums l ==> summable f";
-by (Blast_tac 1);
-qed "sums_summable";
-
-Goalw [summable_def,suminf_def]
-     "summable f ==> f sums (suminf f)";
-by (blast_tac (claset() addIs [someI2]) 1);
-qed "summable_sums";
-
-Goalw [summable_def,suminf_def,sums_def]
-     "summable f ==> (%n. sumr 0 n f) ----> (suminf f)";
-by (blast_tac (claset() addIs [someI2]) 1);
-qed "summable_sumr_LIMSEQ_suminf";
-
-(*-------------------
-    sum is unique                    
- ------------------*)
-Goal "f sums s ==> (s = suminf f)";
-by (forward_tac [sums_summable RS summable_sums] 1);
-by (auto_tac (claset() addSIs [LIMSEQ_unique],
-    simpset() addsimps [sums_def]));
-qed "sums_unique";
-
-(*
-Goalw [sums_def,LIMSEQ_def] 
-     "(ALL m. n <= Suc m --> f(m) = 0) ==> f sums (sumr 0 n f)";
-by (Step_tac 1);
-by (res_inst_tac [("x","n")] exI 1);
-by (Step_tac 1 THEN ftac le_imp_less_or_eq 1);
-by (Step_tac 1);
-by (dres_inst_tac [("f","f")] sumr_split_add_minus 1);
-by (ALLGOALS (Asm_simp_tac));
-by (dtac (conjI RS sumr_interval_const) 1);
-by (Auto_tac);
-qed "series_zero";
-next one was called series_zero2
-**********************)
-
-Goalw [sums_def,LIMSEQ_def] 
-     "(ALL m. n <= m --> f(m) = 0) ==> f sums (sumr 0 n f)";
-by (Step_tac 1);
-by (res_inst_tac [("x","n")] exI 1);
-by (Step_tac 1 THEN ftac le_imp_less_or_eq 1);
-by (Step_tac 1);
-by (dres_inst_tac [("f","f")] sumr_split_add_minus 1);
-by (ALLGOALS (Asm_simp_tac));
-by (dtac (conjI RS sumr_interval_const2) 1);
-by (Auto_tac);
-qed "series_zero";
-
-Goalw [sums_def] "x sums x0 ==> (%n. c * x(n)) sums (c * x0)";
-by (auto_tac (claset() addSIs [LIMSEQ_mult] addIs [LIMSEQ_const], 
-              simpset() addsimps [sumr_mult RS sym]));
-qed "sums_mult";
-
-Goal "x sums x' ==> (%n. x(n)/c) sums (x'/c)";
-by (asm_simp_tac (simpset() addsimps [real_divide_def, sums_mult,
-                              inst "w" "inverse c" real_mult_commute]) 1); 
-qed "sums_divide";
-
-Goalw [sums_def] "[| x sums x0; y sums y0 |] ==> (%n. x n - y n) sums (x0-y0)";
-by (auto_tac (claset() addIs [LIMSEQ_diff],
-              simpset() addsimps [sumr_diff RS sym]));
-qed "sums_diff";
-
-Goal "summable f ==> suminf f * c = suminf(%n. f n * c)";
-by (auto_tac (claset() addSIs [sums_unique,sums_mult,summable_sums],
-    simpset() addsimps [real_mult_commute]));
-qed "suminf_mult";
-
-Goal "summable f ==> c * suminf f  = suminf(%n. c * f n)";
-by (auto_tac (claset() addSIs [sums_unique,sums_mult,summable_sums],
-    simpset()));
-qed "suminf_mult2";
-
-Goal "[| summable f; summable g |]  \
-\     ==> suminf f - suminf g  = suminf(%n. f n - g n)";
-by (auto_tac (claset() addSIs [sums_diff,sums_unique,summable_sums], simpset()));
-qed "suminf_diff";
-
-Goalw [sums_def] 
-       "x sums x0 ==> (%n. - x n) sums - x0";
-by (auto_tac (claset() addSIs [LIMSEQ_minus], simpset() addsimps [sumr_minus]));
-qed "sums_minus";
-
-Goal "[|summable f; 0 < k |] \
-\     ==> (%n. sumr (n*k) (n*k + k) f) sums (suminf f)";
-by (dtac summable_sums 1);
-by (auto_tac (claset(),simpset() addsimps [sums_def,LIMSEQ_def]));
-by (dres_inst_tac [("x","r")] spec 1 THEN Step_tac 1); 
-by (res_inst_tac [("x","no")] exI 1 THEN Step_tac 1); 
-by (dres_inst_tac [("x","n*k")] spec 1); 
-by (auto_tac (claset() addSDs [not_leE], simpset()));
-by (dres_inst_tac [("j","no")] less_le_trans 1);
-by (Auto_tac);
-qed "sums_group";
-
-Goal "[|summable f; ALL d. 0 < (f(n + (Suc (Suc 0) * d))) + f(n + ((Suc (Suc 0) * d) + 1))|] \
-\     ==> sumr 0 n f < suminf f";
-by (dtac summable_sums 1);
-by (auto_tac (claset(),simpset() addsimps [sums_def,LIMSEQ_def]));
-by (dres_inst_tac [("x","f(n) + f(n + 1)")] spec 1);
-by (Auto_tac);
-by (rtac ccontr 2 THEN dtac (linorder_not_less RS iffD1) 2);
-by (subgoal_tac "sumr 0 (n + Suc (Suc 0)) f <= sumr 0 (Suc (Suc 0) * (Suc no) + n) f" 2);
-by (induct_tac "no" 3 THEN Simp_tac 3);
-by (res_inst_tac [("y","sumr 0 (Suc (Suc 0)*(Suc na)+n) f")] order_trans 3);
-by (assume_tac 3);
-by (dres_inst_tac [("x","Suc na")] spec 3);
-by (dres_inst_tac [("x","0")] spec 1);
-by (Asm_full_simp_tac 1);
-by (asm_full_simp_tac (simpset() addsimps add_ac) 2);
-by (rotate_tac 1 1 THEN dres_inst_tac [("x","Suc (Suc 0) * (Suc no) + n")] spec 1);
-by (Step_tac 1 THEN Asm_full_simp_tac 1);
-by (subgoal_tac "suminf f + (f(n) + f(n + 1)) <= \
-\                 sumr 0 (Suc (Suc 0) * (Suc no) + n) f" 1);
-by (res_inst_tac [("y","sumr 0 (n+ Suc (Suc 0)) f")] order_trans 2);
-by (assume_tac 3);
-by (res_inst_tac [("y","sumr 0 n f + (f(n) + f(n + 1))")] order_trans 2);
-by (REPEAT(Asm_simp_tac 2));
-by (subgoal_tac "suminf f <= sumr 0 (Suc (Suc 0) * (Suc no) + n) f" 1);
-by (res_inst_tac [("y","suminf f + (f(n) + f(n + 1))")] order_trans 2);
-by (assume_tac 3);
-by (dres_inst_tac [("x","0")] spec 2);
-by (Asm_full_simp_tac 2);
-by (subgoal_tac "0 <= sumr 0 (Suc (Suc 0) * Suc no + n) f + - suminf f" 1);
-by (dtac (abs_eqI1) 1 );
-by (Asm_full_simp_tac 1);
-by (auto_tac (claset(),simpset() addsimps [linorder_not_less RS sym]));
-qed "sumr_pos_lt_pair";
-
-(*-----------------------------------------------------------------
-   Summable series of positive terms has limit >= any partial sum 
- ----------------------------------------------------------------*)
-Goal 
-     "[| summable f; ALL m. n <= m --> 0 <= f(m) |] \
-\          ==> sumr 0 n f <= suminf f";
-by (dtac summable_sums 1);
-by (rewtac sums_def);
-by (cut_inst_tac [("k","sumr 0 n f")] LIMSEQ_const 1);
-by (etac LIMSEQ_le 1 THEN Step_tac 1);
-by (res_inst_tac [("x","n")] exI 1 THEN Step_tac 1);
-by (dtac le_imp_less_or_eq 1 THEN Step_tac 1);
-by (auto_tac (claset() addIs [sumr_le], simpset()));
-qed "series_pos_le";
-
-Goal "[| summable f; ALL m. n <= m --> 0 < f(m) |] \
-\          ==> sumr 0 n f < suminf f";
-by (res_inst_tac [("y","sumr 0 (Suc n) f")] order_less_le_trans 1);
-by (rtac series_pos_le 2);
-by (Auto_tac);
-by (dres_inst_tac [("x","m")] spec 1);
-by (Auto_tac);
-qed "series_pos_less";
-
-(*-------------------------------------------------------------------
-                    sum of geometric progression                 
- -------------------------------------------------------------------*)
-
-Goal "x ~= 1 ==> sumr 0 n (%n. x ^ n) = (x ^ n - 1) / (x - 1)";
-by (induct_tac "n" 1);
-by (Auto_tac);
-by (res_inst_tac [("c1","x - 1")] (real_mult_right_cancel RS iffD1) 1);
-by (auto_tac (claset(),
-       simpset() addsimps [real_mult_assoc, left_distrib]));
-by (auto_tac (claset(),
-       simpset() addsimps [right_distrib,
-                           real_diff_def, real_mult_commute]));
-qed "sumr_geometric";
-
-Goal "abs(x) < 1 ==> (%n. x ^ n) sums (1/(1 - x))";
-by (case_tac "x = 1" 1);
-by (auto_tac (claset() addSDs [LIMSEQ_rabs_realpow_zero2],
-             simpset() addsimps [sumr_geometric ,sums_def,
-                                 real_diff_def, add_divide_distrib]));
-by (subgoal_tac "1 / (1 + -x) = 0/(x - 1) + - 1/(x - 1)" 1); 
-by (asm_full_simp_tac (simpset() addsimps [thm"minus_divide_right"]) 2); 
-by (etac ssubst 1); 
-by (rtac LIMSEQ_add 1 THEN rtac LIMSEQ_divide 1);
-by (auto_tac (claset() addIs [LIMSEQ_const], 
-              simpset() addsimps [real_diff_def, LIMSEQ_rabs_realpow_zero2]));
-qed "geometric_sums";
-
-(*-------------------------------------------------------------------
-    Cauchy-type criterion for convergence of series (c.f. Harrison)
- -------------------------------------------------------------------*)
-Goalw [summable_def,sums_def,convergent_def]
-      "summable f = convergent (%n. sumr 0 n f)";
-by (Auto_tac);
-qed "summable_convergent_sumr_iff";
-
-Goal "summable f = \
-\     (ALL e. 0 < e --> (EX N. ALL m n. N <= m --> abs(sumr m n f) < e))";
-by (auto_tac (claset(),simpset() addsimps [summable_convergent_sumr_iff,
-    Cauchy_convergent_iff RS sym,Cauchy_def]));
-by (ALLGOALS(dtac spec) THEN Auto_tac);
-by (res_inst_tac [("x","M")] exI 1);
-by (res_inst_tac [("x","N")] exI 2);
-by (Auto_tac);
-by (ALLGOALS(cut_inst_tac [("m","m"),("n","n")] less_linear));
-by (Auto_tac);
-by (ftac (le_less_trans RS less_imp_le) 1 THEN assume_tac 1);
-by (dres_inst_tac [("x","n")] spec 1);
-by (dres_inst_tac [("x","m")] spec 1);
-by (auto_tac (claset() addIs [(abs_minus_add_cancel RS subst)],
-    simpset() addsimps [sumr_split_add_minus,abs_minus_add_cancel]));
-qed "summable_Cauchy";
-
-(*-------------------------------------------------------------------
-     Terms of a convergent series tend to zero
-     > Goalw [LIMSEQ_def] "summable f ==> f ----> 0";
-     Proved easily in HSeries after proving nonstandard case.
- -------------------------------------------------------------------*)
-(*-------------------------------------------------------------------
-                    Comparison test
- -------------------------------------------------------------------*)
-Goal "[| EX N. ALL n. N <= n --> abs(f n) <= g n; \
-\        summable g \
-\     |] ==> summable f";
-by (auto_tac (claset(),simpset() addsimps [summable_Cauchy]));
-by (dtac spec 1 THEN Auto_tac);
-by (res_inst_tac [("x","N + Na")] exI 1 THEN Auto_tac);
-by (rotate_tac 2 1);
-by (dres_inst_tac [("x","m")] spec 1);
-by (Auto_tac THEN rotate_tac 2 1 THEN dres_inst_tac [("x","n")] spec 1);
-by (res_inst_tac [("y","sumr m n (%k. abs(f k))")] order_le_less_trans 1);
-by (rtac sumr_rabs 1);
-by (res_inst_tac [("y","sumr m n g")] order_le_less_trans 1);
-by (auto_tac (claset() addIs [sumr_le2],
-    simpset() addsimps [abs_interval_iff]));
-qed "summable_comparison_test";
-
-Goal "[| EX N. ALL n. N <= n --> abs(f n) <= g n; \
-\        summable g \
-\     |] ==> summable (%k. abs (f k))";
-by (rtac summable_comparison_test 1);
-by (auto_tac (claset(),simpset() addsimps [abs_idempotent]));
-qed "summable_rabs_comparison_test";
-
-(*------------------------------------------------------------------*)
-(*       Limit comparison property for series (c.f. jrh)            *)
-(*------------------------------------------------------------------*)
-Goal "[|ALL n. f n <= g n; summable f; summable g |] \
-\     ==> suminf f <= suminf g";
-by (REPEAT(dtac summable_sums 1));
-by (auto_tac (claset() addSIs [LIMSEQ_le], simpset() addsimps [sums_def]));
-by (rtac exI 1);
-by (auto_tac (claset() addSIs [sumr_le2], simpset()));
-qed "summable_le";
-
-Goal "[|ALL n. abs(f n) <= g n; summable g |] \
-\     ==> summable f & suminf f <= suminf g";
-by (auto_tac (claset() addIs [summable_comparison_test]
-    addSIs [summable_le], simpset()));
-by (auto_tac (claset(),simpset() addsimps [abs_le_interval_iff]));
-qed "summable_le2";
-
-(*-------------------------------------------------------------------
-         Absolute convergence imples normal convergence
- -------------------------------------------------------------------*)
-Goal "summable (%n. abs (f n)) ==> summable f";
-by (auto_tac (claset(),simpset() addsimps [sumr_rabs,summable_Cauchy]));
-by (dtac spec 1 THEN Auto_tac);
-by (res_inst_tac [("x","N")] exI 1 THEN Auto_tac);
-by (dtac spec 1 THEN Auto_tac);
-by (res_inst_tac [("y","sumr m n (%n. abs(f n))")] order_le_less_trans 1);
-by (auto_tac (claset() addIs [sumr_rabs], simpset()));
-qed "summable_rabs_cancel";
-
-(*-------------------------------------------------------------------
-         Absolute convergence of series
- -------------------------------------------------------------------*)
-Goal "summable (%n. abs (f n)) ==> abs(suminf f) <= suminf (%n. abs(f n))";
-by (auto_tac (claset() addIs [LIMSEQ_le,LIMSEQ_imp_rabs,summable_rabs_cancel,
-                              summable_sumr_LIMSEQ_suminf,sumr_rabs], 
-              simpset()));
-qed "summable_rabs";
-
-(*-------------------------------------------------------------------
-                        The ratio test
- -------------------------------------------------------------------*)
-
-Goal "[| c <= 0; abs x <= c * abs y |] ==> x = (0::real)";
-by (dtac order_le_imp_less_or_eq 1);
-by Auto_tac;  
-by (subgoal_tac "0 <= c * abs y" 1);
-by (arith_tac 2);
-by (asm_full_simp_tac (simpset() addsimps [zero_le_mult_iff]) 1); 
-qed "rabs_ratiotest_lemma";
-
-(* lemmas *)
-
-Goal "(k::nat) <= l ==> (EX n. l = k + n)";
-by (dtac le_imp_less_or_eq 1);
-by (auto_tac (claset() addDs [less_imp_Suc_add], simpset()));
-qed "le_Suc_ex";
-
-Goal "((k::nat) <= l) = (EX n. l = k + n)";
-by (auto_tac (claset(),simpset() addsimps [le_Suc_ex]));
-qed "le_Suc_ex_iff";
-
-(*All this trouble just to get 0<c *)
-Goal "[| ALL n. N <= n --> abs(f(Suc n)) <= c*abs(f n) |] \
-\     ==> 0 < c | summable f";
-by (simp_tac (simpset() addsimps [linorder_not_le RS sym]) 1); 
-by (asm_full_simp_tac (simpset() addsimps [summable_Cauchy]) 1);
-by (Step_tac 1 THEN subgoal_tac "ALL n. N <= n --> f (Suc n) = 0" 1);
-by (blast_tac (claset() addIs [rabs_ratiotest_lemma]) 2);
-by (res_inst_tac [("x","Suc N")] exI 1);
-by (Clarify_tac 1); 
-by (dtac Suc_le_imp_diff_ge2 1 THEN Auto_tac);
-qed "ratio_test_lemma2";
-
-Goal "[| c < 1; ALL n. N <= n --> abs(f(Suc n)) <= c*abs(f n) |] \
-\     ==> summable f";
-by (ftac ratio_test_lemma2 1);
-by Auto_tac;  
-by (res_inst_tac [("g","%n. (abs (f N)/(c ^ N))*c ^ n")] 
-    summable_comparison_test 1);
-by (res_inst_tac [("x","N")] exI 1 THEN Step_tac 1);
-by (dtac (le_Suc_ex_iff RS iffD1) 1);
-by (auto_tac (claset(),simpset() addsimps [power_add, realpow_not_zero]));
-by (induct_tac "na" 1 THEN Auto_tac);
-by (res_inst_tac [("y","c*abs(f(N + n))")] order_trans 1);
-by (auto_tac (claset() addIs [mult_right_mono],
-              simpset() addsimps [summable_def]));
-by (asm_full_simp_tac (simpset() addsimps mult_ac) 1);
-by (res_inst_tac [("x","abs(f N) * (1/(1 - c)) / (c ^ N)")] exI 1);
-by (rtac sums_divide 1); 
-by (rtac sums_mult 1); 
-by (auto_tac (claset() addSIs [sums_mult,geometric_sums], 
-              simpset() addsimps [real_abs_def]));
-qed "ratio_test";
-
-
-(*--------------------------------------------------------------------------*)
-(* Differentiation of finite sum                                            *)
-(*--------------------------------------------------------------------------*)
-
-Goal "(ALL r. m <= r & r < (m + n) --> DERIV (%x. f r x) x :> (f' r x)) \
-\     --> DERIV (%x. sumr m n (%n. f n x)) x :> sumr m n (%r. f' r x)";
-by (induct_tac "n" 1);
-by (auto_tac (claset() addIs [DERIV_add], simpset()));
-qed_spec_mp "DERIV_sumr";
diff -r 60aa114e2dba -r 1f256287d4f0 src/HOL/Hyperreal/Series.thy
--- a/src/HOL/Hyperreal/Series.thy	Thu Feb 26 11:31:36 2004 +0100
+++ b/src/HOL/Hyperreal/Series.thy	Thu Feb 26 17:08:23 2004 +0100
@@ -1,27 +1,603 @@
 (*  Title       : Series.thy
     Author      : Jacques D. Fleuriot
     Copyright   : 1998  University of Cambridge
-    Description : Finite summation and infinite series
+
+Converted to Isar and polished by lcp
 *) 
 
+header{*Finite Summation and Infinite Series*}
 
-Series = SEQ + Lim +
+theory Series = SEQ + Lim:
 
 consts sumr :: "[nat,nat,(nat=>real)] => real"
 primrec
-   sumr_0   "sumr m 0 f = 0"
-   sumr_Suc "sumr m (Suc n) f = (if n < m then 0 
-                               else sumr m n f + f(n))"
+   sumr_0:   "sumr m 0 f = 0"
+   sumr_Suc: "sumr m (Suc n) f = (if n < m then 0 else sumr m n f + f(n))"
 
 constdefs
-   sums  :: [nat=>real,real] => bool     (infixr 80)
+   sums  :: "[nat=>real,real] => bool"     (infixr "sums" 80)
    "f sums s  == (%n. sumr 0 n f) ----> s"
 
-   summable :: (nat=>real) => bool
-   "summable f == (EX s. f sums s)"
+   summable :: "(nat=>real) => bool"
+   "summable f == (\<exists>s. f sums s)"
+
+   suminf   :: "(nat=>real) => real"
+   "suminf f == (@s. f sums s)"
+
+
+lemma sumr_Suc_zero [simp]: "sumr (Suc n) n f = 0"
+by (induct_tac "n", auto)
+
+lemma sumr_eq_bounds [simp]: "sumr m m f = 0"
+by (induct_tac "m", auto)
+
+lemma sumr_Suc_eq [simp]: "sumr m (Suc m) f = f(m)"
+by auto
+
+lemma sumr_add_lbound_zero [simp]: "sumr (m+k) k f = 0"
+by (induct_tac "k", auto)
+
+lemma sumr_add: "sumr m n f + sumr m n g = sumr m n (%n. f n + g n)"
+apply (induct_tac "n")
+apply (simp_all add: add_ac)
+done
+
+lemma sumr_mult: "r * sumr m n f = sumr m n (%n. r * f n)"
+apply (induct_tac "n")
+apply (simp_all add: right_distrib)
+done
+
+lemma sumr_split_add [rule_format]:
+     "n < p --> sumr 0 n f + sumr n p f = sumr 0 p f"
+apply (induct_tac "p", auto)
+apply (rename_tac k) 
+apply (subgoal_tac "n=k", auto) 
+done
+
+lemma sumr_split_add_minus: "n < p ==> sumr 0 p f + - sumr 0 n f = sumr n p f"
+apply (drule_tac f1 = f in sumr_split_add [symmetric])
+apply (simp add: add_ac)
+done
+
+lemma sumr_split_add2 [rule_format]:
+     "0 < n --> n < p --> sumr (Suc 0) n f + sumr n p f = sumr (Suc 0) p f"
+apply (induct_tac "p", auto) 
+apply (rename_tac k) 
+apply (subgoal_tac "n=k", auto)
+done
+
+lemma sumr_split_add3:
+     "[| 0<n; n \<le> p |] ==> sumr (Suc 0) n f + sumr n p f = sumr (Suc 0) p f"
+apply (drule le_imp_less_or_eq, auto)
+apply (blast intro: sumr_split_add2)
+done
+
+lemma sumr_rabs: "abs(sumr m n f) \<le> sumr m n (%i. abs(f i))"
+apply (induct_tac "n")
+apply (auto intro: abs_triangle_ineq [THEN order_trans] add_right_mono)
+done
+
+lemma sumr_fun_eq [rule_format (no_asm)]:
+     "(\<forall>r. m \<le> r & r < n --> f r = g r) --> sumr m n f = sumr m n g"
+by (induct_tac "n", auto)
+
+lemma sumr_const [simp]: "sumr 0 n (%i. r) = real n * r"
+apply (induct_tac "n")
+apply (simp_all add: left_distrib real_of_nat_zero real_of_nat_Suc)
+done
+
+lemma sumr_add_mult_const:
+     "sumr 0 n f + -(real n * r) = sumr 0 n (%i. f i + -r)"
+by (simp only: sumr_add [symmetric] minus_mult_right, simp)
+
+lemma sumr_diff_mult_const: "sumr 0 n f - (real n*r) = sumr 0 n (%i. f i - r)"
+by (simp add: real_diff_def sumr_add_mult_const)
+
+lemma sumr_less_bounds_zero [rule_format, simp]: "n < m --> sumr m n f = 0"
+apply (induct_tac "n")
+apply (auto dest: less_imp_le)
+done
+
+lemma sumr_minus: "sumr m n (%i. - f i) = - sumr m n f"
+apply (induct_tac "n")
+apply (case_tac [2] "Suc n \<le> m", simp_all)
+done
+
+lemma sumr_shift_bounds: "sumr (m+k) (n+k) f = sumr m n (%i. f(i + k))"
+by (induct_tac "n", auto)
+
+lemma sumr_minus_one_realpow_zero [simp]: "sumr 0 (2*n) (%i. (-1) ^ Suc i) = 0"
+by (induct_tac "n", auto)
+
+lemma Suc_diff_n: "m < Suc n ==> Suc n - m = Suc (n - m)"
+by (drule less_imp_Suc_add, auto)
+
+lemma sumr_interval_const [rule_format (no_asm)]:
+     "(\<forall>n. m \<le> Suc n --> f n = r) --> m \<le> k --> sumr m k f = (real(k-m) * r)"
+apply (induct_tac "k", auto) 
+apply (drule_tac x = n in spec)
+apply (auto dest!: le_imp_less_or_eq)
+apply (simp (no_asm_simp) add: left_distrib Suc_diff_n real_of_nat_Suc)
+done
+
+lemma sumr_interval_const2 [rule_format (no_asm)]:
+     "(\<forall>n. m \<le> n --> f n = r) --> m \<le> k  
+      --> sumr m k f = (real (k - m) * r)"
+apply (induct_tac "k", auto) 
+apply (drule_tac x = n in spec)
+apply (auto dest!: le_imp_less_or_eq)
+apply (simp (no_asm_simp) add: Suc_diff_n left_distrib real_of_nat_Suc)
+done
+
+lemma sumr_le [rule_format (no_asm)]:
+     "(\<forall>n. m \<le> n --> 0 \<le> f n) --> m < k --> sumr 0 m f \<le> sumr 0 k f"
+apply (induct_tac "k")
+apply (auto simp add: less_Suc_eq_le)
+apply (drule_tac [!] x = n in spec, safe)
+apply (drule le_imp_less_or_eq, safe)
+apply (drule_tac [2] a = "sumr 0 m f" in add_mono)
+apply (drule_tac a = "sumr 0 m f" in order_refl [THEN add_mono], auto)
+done
+
+lemma sumr_le2 [rule_format (no_asm)]:
+     "(\<forall>r. m \<le> r & r < n --> f r \<le> g r) --> sumr m n f \<le> sumr m n g"
+apply (induct_tac "n")
+apply (auto intro: add_mono simp add: le_def)
+done
+
+lemma sumr_ge_zero [rule_format (no_asm)]: "(\<forall>n. 0 \<le> f n) --> 0 \<le> sumr m n f"
+apply (induct_tac "n", auto)
+apply (drule_tac x = n in spec, arith)
+done
+
+lemma sumr_ge_zero2 [rule_format (no_asm)]:
+     "(\<forall>n. m \<le> n --> 0 \<le> f n) --> 0 \<le> sumr m n f"
+apply (induct_tac "n", auto)
+apply (drule_tac x = n in spec, arith)
+done
+
+lemma sumr_rabs_ge_zero [iff]: "0 \<le> sumr m n (%n. abs (f n))"
+by (induct_tac "n", auto, arith)
 
-   suminf   :: (nat=>real) => real
-   "suminf f == (@s. f sums s)"
-end
+lemma rabs_sumr_rabs_cancel [simp]:
+     "abs (sumr m n (%n. abs (f n))) = (sumr m n (%n. abs (f n)))"
+apply (induct_tac "n")
+apply (auto, arith)
+done
+
+lemma sumr_zero [rule_format]:
+     "\<forall>n. N \<le> n --> f n = 0 ==> N \<le> m --> sumr m n f = 0"
+by (induct_tac "n", auto)
+
+lemma Suc_le_imp_diff_ge2:
+     "[|\<forall>n. N \<le> n --> f (Suc n) = 0; Suc N \<le> m|] ==> sumr m n f = 0"
+apply (rule sumr_zero) 
+apply (case_tac "n", auto)
+done
+
+lemma sumr_one_lb_realpow_zero [simp]: "sumr (Suc 0) n (%n. f(n) * 0 ^ n) = 0"
+apply (induct_tac "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)
+
+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_tac "n", auto)
+
+lemma sumr_bound [rule_format (no_asm)]:
+     "(\<forall>p. m \<le> p & p < m + n --> (f(p) \<le> K))  
+      --> (sumr m (m + n) f \<le> (real n * K))"
+apply (induct_tac "n")
+apply (auto intro: add_mono simp add: left_distrib real_of_nat_Suc)
+done
+
+lemma sumr_bound2 [rule_format (no_asm)]:
+     "(\<forall>p. 0 \<le> p & p < n --> (f(p) \<le> K))  
+      --> (sumr 0 n f \<le> (real n * K))"
+apply (induct_tac "n")
+apply (auto intro: add_mono simp add: left_distrib real_of_nat_Suc)
+done
+
+lemma sumr_group [simp]:
+     "sumr 0 n (%m. sumr (m * k) (m*k + k) f) = sumr 0 (n * k) f"
+apply (subgoal_tac "k = 0 | 0 < k", auto)
+apply (induct_tac "n")
+apply (simp_all add: sumr_split_add add_commute)
+done
+
+subsection{* Infinite Sums, by the Properties of Limits*}
+
+(*----------------------
+   suminf is the sum   
+ ---------------------*)
+lemma sums_summable: "f sums l ==> summable f"
+by (simp add: sums_def summable_def, blast)
+
+lemma summable_sums: "summable f ==> f sums (suminf f)"
+apply (simp add: summable_def suminf_def)
+apply (blast intro: someI2)
+done
+
+lemma summable_sumr_LIMSEQ_suminf: 
+     "summable f ==> (%n. sumr 0 n f) ----> (suminf f)"
+apply (simp add: summable_def suminf_def sums_def)
+apply (blast intro: someI2)
+done
+
+(*-------------------
+    sum is unique                    
+ ------------------*)
+lemma sums_unique: "f sums s ==> (s = suminf f)"
+apply (frule sums_summable [THEN summable_sums])
+apply (auto intro!: LIMSEQ_unique simp add: sums_def)
+done
+
+(*
+Goalw [sums_def,LIMSEQ_def] 
+     "(\<forall>m. n \<le> Suc m --> f(m) = 0) ==> f sums (sumr 0 n f)"
+by safe
+by (res_inst_tac [("x","n")] exI 1);
+by (safe THEN ftac le_imp_less_or_eq 1)
+by safe
+by (dres_inst_tac [("f","f")] sumr_split_add_minus 1);
+by (ALLGOALS (Asm_simp_tac));
+by (dtac (conjI RS sumr_interval_const) 1);
+by Auto_tac
+qed "series_zero";
+next one was called series_zero2
+**********************)
+
+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 (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 (drule sumr_interval_const2, auto)
+done
+
+lemma sums_mult: "x sums x0 ==> (%n. c * x(n)) sums (c * x0)"
+by (auto simp add: sums_def sumr_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)
+
+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)
+
+lemma suminf_mult2: "summable f ==> c * suminf f  = suminf(%n. c * f n)"
+by (auto intro!: sums_unique sums_mult summable_sums)
+
+lemma suminf_diff:
+     "[| summable f; summable g |]   
+      ==> suminf f - suminf g  = suminf(%n. f n - g n)"
+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)
+
+lemma sums_group:
+     "[|summable f; 0 < k |] ==> (%n. sumr (n*k) (n*k + k) f) sums (suminf f)"
+apply (drule summable_sums)
+apply (auto simp add: sums_def LIMSEQ_def)
+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)))|]
+      ==> sumr 0 (n + Suc (Suc 0)) f \<le> sumr 0 (Suc (Suc 0) * Suc no + n) f"
+apply (induct_tac "no", simp)
+apply (rule_tac y = "sumr 0 (Suc (Suc 0) * (Suc na) +n) f" in order_trans)
+apply assumption
+apply (drule_tac x = "Suc na" 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))|]  
+      ==> sumr 0 n f < 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
+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> sumr 0 (Suc (Suc 0) * (Suc no) + n) f")
+apply (rule_tac [2] y = "sumr 0 (n+ Suc (Suc 0)) f" in order_trans)
+prefer 3 apply assumption
+apply (rule_tac [2] y = "sumr 0 n f + (f (n) + f (n + 1))" in order_trans)
+apply simp_all 
+apply (subgoal_tac "suminf f \<le> sumr 0 (Suc (Suc 0) * (Suc no) + n) f")
+apply (rule_tac [2] y = "suminf f + (f (n) + f (n + 1))" in order_trans)
+prefer 3 apply simp 
+apply (drule_tac [2] x = 0 in spec)
+ prefer 2 apply simp 
+apply (subgoal_tac "0 \<le> sumr 0 (Suc (Suc 0) * Suc no + n) f + - suminf f")
+apply (simp add: abs_if) 
+apply (auto simp add: linorder_not_less [symmetric])
+done
+
+
+
+(*-----------------------------------------------------------------
+   Summable series of positive terms has limit >= any partial sum 
+ ----------------------------------------------------------------*)
+lemma series_pos_le: 
+     "[| summable f; \<forall>m. n \<le> m --> 0 \<le> f(m) |] ==> sumr 0 n f \<le> suminf f"
+apply (drule summable_sums)
+apply (simp add: sums_def)
+apply (cut_tac k = "sumr 0 n f" in LIMSEQ_const)
+apply (erule LIMSEQ_le, blast) 
+apply (rule_tac x = n in exI, clarify) 
+apply (drule le_imp_less_or_eq)
+apply (auto intro: sumr_le)
+done
+
+lemma series_pos_less:
+     "[| summable f; \<forall>m. n \<le> m --> 0 < f(m) |] ==> sumr 0 n f < suminf f"
+apply (rule_tac y = "sumr 0 (Suc n) f" in order_less_le_trans)
+apply (rule_tac [2] series_pos_le, auto)
+apply (drule_tac x = m in spec, auto)
+done
+
+(*-------------------------------------------------------------------
+                    sum of geometric progression                 
+ -------------------------------------------------------------------*)
+
+lemma sumr_geometric: "x ~= 1 ==> sumr 0 n (%n. x ^ n) = (x ^ n - 1) / (x - 1)"
+apply (induct_tac "n", auto)
+apply (rule_tac c1 = "x - 1" in real_mult_right_cancel [THEN iffD1])
+apply (auto simp add: real_mult_assoc left_distrib)
+apply (simp add: right_distrib real_diff_def real_mult_commute)
+done
+
+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 real_diff_def 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: real_diff_def minus_divide_right LIMSEQ_rabs_realpow_zero2)
+done
+
+(*-------------------------------------------------------------------
+    Cauchy-type criterion for convergence of series (c.f. Harrison)
+ -------------------------------------------------------------------*)
+lemma summable_convergent_sumr_iff: "summable f = convergent (%n. sumr 0 n f)"
+by (simp add: summable_def sums_def convergent_def)
+
+lemma summable_Cauchy:
+     "summable f =  
+      (\<forall>e. 0 < e --> (\<exists>N. \<forall>m n. N \<le> m --> abs(sumr m n f) < e))"
+apply (auto simp add: summable_convergent_sumr_iff Cauchy_convergent_iff [symmetric] Cauchy_def)
+apply (drule_tac [!] spec, auto) 
+apply (rule_tac x = M in exI)
+apply (rule_tac [2] x = N in exI, auto)
+apply (cut_tac [!] m = m and n = n in less_linear, auto)
+apply (frule le_less_trans [THEN less_imp_le], assumption)
+apply (drule_tac x = n in spec)
+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)
+done
+
+(*-------------------------------------------------------------------
+     Terms of a convergent series tend to zero
+     > Goalw [LIMSEQ_def] "summable f ==> f ----> 0"
+     Proved easily in HSeries after proving nonstandard case.
+ -------------------------------------------------------------------*)
+(*-------------------------------------------------------------------
+                    Comparison test
+ -------------------------------------------------------------------*)
+lemma summable_comparison_test:
+     "[| \<exists>N. \<forall>n. N \<le> 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)
+apply (rotate_tac 2)
+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_tac y = "sumr m n g" in order_le_less_trans)
+apply (auto intro: sumr_le2 simp add: abs_interval_iff)
+done
+
+lemma summable_rabs_comparison_test:
+     "[| \<exists>N. \<forall>n. N \<le> n --> abs(f n) \<le> g n; summable g |] 
+      ==> summable (%k. abs (f k))"
+apply (rule summable_comparison_test)
+apply (auto simp add: abs_idempotent)
+done
+
+(*------------------------------------------------------------------*)
+(*       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"
+apply (drule summable_sums)+
+apply (auto intro!: LIMSEQ_le simp add: sums_def)
+apply (rule exI)
+apply (auto intro!: sumr_le2)
+done
+
+lemma summable_le2:
+     "[|\<forall>n. abs(f n) \<le> g n; summable g |]  
+      ==> summable f & suminf f \<le> suminf g"
+apply (auto intro: summable_comparison_test intro!: summable_le)
+apply (simp add: abs_le_interval_iff)
+done
+
+(*-------------------------------------------------------------------
+         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 (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)
+done
+
+(*-------------------------------------------------------------------
+         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)
+
+
+subsection{* The Ratio Test*}
+
+lemma rabs_ratiotest_lemma: "[| c \<le> 0; abs x \<le> c * abs y |] ==> x = (0::real)"
+apply (drule order_le_imp_less_or_eq, auto)
+apply (subgoal_tac "0 \<le> c * abs y")
+apply (simp add: zero_le_mult_iff, arith)
+done
+
+lemma le_Suc_ex: "(k::nat) \<le> l ==> (\<exists>n. l = k + n)"
+apply (drule le_imp_less_or_eq)
+apply (auto dest: less_imp_Suc_add)
+done
+
+lemma le_Suc_ex_iff: "((k::nat) \<le> l) = (\<exists>n. l = k + n)"
+by (auto simp add: le_Suc_ex)
+
+(*All this trouble just to get 0<c *)
+lemma ratio_test_lemma2:
+     "[| \<forall>n. N \<le> n --> abs(f(Suc n)) \<le> c*abs(f n) |]  
+      ==> 0 < c | summable f"
+apply (simp (no_asm) add: linorder_not_le [symmetric])
+apply (simp add: summable_Cauchy)
+apply (safe, subgoal_tac "\<forall>n. N \<le> n --> f (Suc n) = 0")
+prefer 2 apply (blast intro: rabs_ratiotest_lemma)
+apply (rule_tac x = "Suc N" in exI, clarify)
+apply (drule_tac n=n in Suc_le_imp_diff_ge2, auto) 
+done
+
+lemma ratio_test:
+     "[| c < 1; \<forall>n. N \<le> n --> abs(f(Suc n)) \<le> c*abs(f n) |]  
+      ==> summable f"
+apply (frule ratio_test_lemma2, auto)
+apply (rule_tac g = "%n. (abs (f N) / (c ^ N))*c ^ n" in summable_comparison_test)
+apply (rule_tac x = N in exI, safe)
+apply (drule le_Suc_ex_iff [THEN iffD1])
+apply (auto simp add: power_add realpow_not_zero)
+apply (induct_tac "na", auto)
+apply (rule_tac y = "c*abs (f (N + n))" in order_trans)
+apply (auto intro: mult_right_mono simp add: summable_def)
+apply (simp add: mult_ac)
+apply (rule_tac x = "abs (f N) * (1/ (1 - c)) / (c ^ N) " in exI)
+apply (rule sums_divide)
+apply (rule sums_mult)
+apply (auto intro!: sums_mult geometric_sums simp add: real_abs_def)
+done
+
+
+(*--------------------------------------------------------------------------*)
+(* Differentiation of finite sum                                            *)
+(*--------------------------------------------------------------------------*)
+
+lemma DERIV_sumr [rule_format (no_asm)]:
+     "(\<forall>r. m \<le> r & r < (m + n) --> DERIV (%x. f r x) x :> (f' r x))  
+      --> DERIV (%x. sumr m n (%n. f n x)) x :> sumr m n (%r. f' r x)"
+apply (induct_tac "n")
+apply (auto intro: DERIV_add)
+done
+
+ML
+{*
+val sumr_0 = thm"sumr_0";
+val sumr_Suc = thm"sumr_Suc";
+val sums_def = thm"sums_def";
+val summable_def = thm"summable_def";
+val suminf_def = thm"suminf_def";
+
+val sumr_Suc_zero = thm "sumr_Suc_zero";
+val sumr_eq_bounds = thm "sumr_eq_bounds";
+val sumr_Suc_eq = thm "sumr_Suc_eq";
+val sumr_add_lbound_zero = thm "sumr_add_lbound_zero";
+val sumr_add = thm "sumr_add";
+val sumr_mult = thm "sumr_mult";
+val sumr_split_add = thm "sumr_split_add";
+val sumr_split_add_minus = thm "sumr_split_add_minus";
+val sumr_split_add2 = thm "sumr_split_add2";
+val sumr_split_add3 = thm "sumr_split_add3";
+val sumr_rabs = thm "sumr_rabs";
+val sumr_fun_eq = thm "sumr_fun_eq";
+val sumr_const = thm "sumr_const";
+val sumr_add_mult_const = thm "sumr_add_mult_const";
+val sumr_diff_mult_const = thm "sumr_diff_mult_const";
+val sumr_less_bounds_zero = thm "sumr_less_bounds_zero";
+val sumr_minus = thm "sumr_minus";
+val sumr_shift_bounds = thm "sumr_shift_bounds";
+val sumr_minus_one_realpow_zero = thm "sumr_minus_one_realpow_zero";
+val Suc_diff_n = thm "Suc_diff_n";
+val sumr_interval_const = thm "sumr_interval_const";
+val sumr_interval_const2 = thm "sumr_interval_const2";
+val sumr_le = thm "sumr_le";
+val sumr_le2 = thm "sumr_le2";
+val sumr_ge_zero = thm "sumr_ge_zero";
+val sumr_ge_zero2 = thm "sumr_ge_zero2";
+val sumr_rabs_ge_zero = thm "sumr_rabs_ge_zero";
+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";
+val sumr_group = thm "sumr_group";
+val sums_summable = thm "sums_summable";
+val summable_sums = thm "summable_sums";
+val summable_sumr_LIMSEQ_suminf = thm "summable_sumr_LIMSEQ_suminf";
+val sums_unique = thm "sums_unique";
+val series_zero = thm "series_zero";
+val sums_mult = thm "sums_mult";
+val sums_divide = thm "sums_divide";
+val sums_diff = thm "sums_diff";
+val suminf_mult = thm "suminf_mult";
+val suminf_mult2 = thm "suminf_mult2";
+val suminf_diff = thm "suminf_diff";
+val sums_minus = thm "sums_minus";
+val sums_group = thm "sums_group";
+val sumr_pos_lt_pair_lemma = thm "sumr_pos_lt_pair_lemma";
+val sumr_pos_lt_pair = thm "sumr_pos_lt_pair";
+val series_pos_le = thm "series_pos_le";
+val series_pos_less = thm "series_pos_less";
+val sumr_geometric = thm "sumr_geometric";
+val geometric_sums = thm "geometric_sums";
+val summable_convergent_sumr_iff = thm "summable_convergent_sumr_iff";
+val summable_Cauchy = thm "summable_Cauchy";
+val summable_comparison_test = thm "summable_comparison_test";
+val summable_rabs_comparison_test = thm "summable_rabs_comparison_test";
+val summable_le = thm "summable_le";
+val summable_le2 = thm "summable_le2";
+val summable_rabs_cancel = thm "summable_rabs_cancel";
+val summable_rabs = thm "summable_rabs";
+val rabs_ratiotest_lemma = thm "rabs_ratiotest_lemma";
+val le_Suc_ex = thm "le_Suc_ex";
+val le_Suc_ex_iff = thm "le_Suc_ex_iff";
+val ratio_test_lemma2 = thm "ratio_test_lemma2";
+val ratio_test = thm "ratio_test";
+val DERIV_sumr = thm "DERIV_sumr";
+*}
+
+end
diff -r 60aa114e2dba -r 1f256287d4f0 src/HOL/IsaMakefile
--- a/src/HOL/IsaMakefile	Thu Feb 26 11:31:36 2004 +0100
+++ b/src/HOL/IsaMakefile	Thu Feb 26 17:08:23 2004 +0100
@@ -153,7 +153,7 @@
   Hyperreal/MacLaurin.ML Hyperreal/MacLaurin.thy Hyperreal/NatStar.thy\
   Hyperreal/NSA.thy Hyperreal/NthRoot.thy\
   Hyperreal/Poly.ML Hyperreal/Poly.thy\
-  Hyperreal/SEQ.ML Hyperreal/SEQ.thy Hyperreal/Series.ML Hyperreal/Series.thy\
+  Hyperreal/SEQ.ML Hyperreal/SEQ.thy Hyperreal/Series.thy\
   Hyperreal/Star.thy Hyperreal/Transcendental.ML\
   Hyperreal/Transcendental.thy Hyperreal/fuf.ML Hyperreal/hypreal_arith.ML \
   Complex/Complex_Main.thy Complex/CLim.thy Complex/CSeries.thy\