src/HOL/Real/Hyperreal/Series.ML
changeset 10045 c76b73e16711
child 10212 33fe2d701ddd
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/Real/Hyperreal/Series.ML	Thu Sep 21 12:17:11 2000 +0200
     1.3 @@ -0,0 +1,635 @@
     1.4 +(*  Title       : Series.ML
     1.5 +    Author      : Jacques D. Fleuriot
     1.6 +    Copyright   : 1998  University of Cambridge
     1.7 +                : 1999  University of Edinburgh
     1.8 +    Description : Finite summation and infinite series
     1.9 +*) 
    1.10 +
    1.11 +Goal "sumr (Suc n) n f = #0";
    1.12 +by (induct_tac "n" 1);
    1.13 +by (Auto_tac);
    1.14 +qed "sumr_Suc_zero";
    1.15 +Addsimps [sumr_Suc_zero];
    1.16 +
    1.17 +Goal "sumr m m f = #0";
    1.18 +by (induct_tac "m" 1);
    1.19 +by (Auto_tac);
    1.20 +qed "sumr_eq_bounds";
    1.21 +Addsimps [sumr_eq_bounds];
    1.22 +
    1.23 +Goal "sumr m (Suc m) f = f(m)";
    1.24 +by (Auto_tac);
    1.25 +qed "sumr_Suc_eq";
    1.26 +Addsimps [sumr_Suc_eq];
    1.27 +
    1.28 +Goal "sumr (m+k) k f = #0";
    1.29 +by (induct_tac "k" 1);
    1.30 +by (Auto_tac);
    1.31 +qed "sumr_add_lbound_zero";
    1.32 +Addsimps [sumr_add_lbound_zero];
    1.33 +
    1.34 +Goal "sumr m n f + sumr m n g = sumr m n (%n. f n + g n)";
    1.35 +by (induct_tac "n" 1);
    1.36 +by (auto_tac (claset(),simpset() addsimps real_add_ac));
    1.37 +qed "sumr_add";
    1.38 +
    1.39 +Goal "r * sumr m n f = sumr m n (%n. r * f n)";
    1.40 +by (induct_tac "n" 1);
    1.41 +by (Auto_tac);
    1.42 +by (auto_tac (claset(),simpset() addsimps 
    1.43 +    [real_add_mult_distrib2]));
    1.44 +qed "sumr_mult";
    1.45 +
    1.46 +Goal "n < p --> sumr 0 n f + sumr n p f = sumr 0 p f";
    1.47 +by (induct_tac "p" 1);
    1.48 +by (auto_tac (claset() addSDs [CLAIM "n < Suc na ==> n <= na",
    1.49 +    leI] addDs [le_anti_sym],simpset()));
    1.50 +qed_spec_mp "sumr_split_add";
    1.51 +
    1.52 +Goal "!!n. n < p ==> sumr 0 p f + \
    1.53 +\                - sumr 0 n f = sumr n p f";
    1.54 +by (dres_inst_tac [("f1","f")] (sumr_split_add RS sym) 1);
    1.55 +by (asm_simp_tac (simpset() addsimps real_add_ac) 1);
    1.56 +qed "sumr_split_add_minus";
    1.57 +
    1.58 +Goal "abs(sumr m n f) <= sumr m n (%i. abs(f i))";
    1.59 +by (induct_tac "n" 1);
    1.60 +by (auto_tac (claset() addIs [(abs_triangle_ineq 
    1.61 +    RS real_le_trans),real_add_le_mono1],simpset()));
    1.62 +qed "sumr_rabs";
    1.63 +
    1.64 +Goal "!!f g. (ALL r. m <= r & r < n --> f r = g r) \
    1.65 +\                --> sumr m n f = sumr m n g";
    1.66 +by (induct_tac "n" 1);
    1.67 +by (Auto_tac);
    1.68 +qed_spec_mp "sumr_fun_eq";
    1.69 +
    1.70 +Goal "sumr 0 n (%i. r) = real_of_nat n*r";
    1.71 +by (induct_tac "n" 1);
    1.72 +by (auto_tac (claset(),simpset() addsimps 
    1.73 +    [real_add_mult_distrib,real_of_nat_zero]));
    1.74 +qed "sumr_const";
    1.75 +Addsimps [sumr_const];
    1.76 +
    1.77 +Goal "sumr 0 n f + -(real_of_nat n*r) = sumr 0 n (%i. f i + -r)";
    1.78 +by (full_simp_tac (simpset() addsimps [sumr_add RS sym,
    1.79 +    real_minus_mult_eq2] delsimps [real_minus_mult_eq2 RS sym]) 1);
    1.80 +qed "sumr_add_mult_const";
    1.81 +
    1.82 +goalw Series.thy [real_diff_def] 
    1.83 +     "sumr 0 n f - (real_of_nat n*r) = sumr 0 n (%i. f i - r)";
    1.84 +by (full_simp_tac (simpset() addsimps [sumr_add_mult_const]) 1);
    1.85 +qed "sumr_diff_mult_const";
    1.86 +
    1.87 +Goal "n < m --> sumr m n f = #0";
    1.88 +by (induct_tac "n" 1);
    1.89 +by (auto_tac (claset() addDs [less_imp_le],simpset()));
    1.90 +qed_spec_mp "sumr_less_bounds_zero";
    1.91 +Addsimps [sumr_less_bounds_zero];
    1.92 +
    1.93 +Goal "sumr m n (%i. - f i) = - sumr m n f";
    1.94 +by (induct_tac "n" 1);
    1.95 +by (case_tac "Suc n <= m" 2);
    1.96 +by (auto_tac (claset(),simpset() addsimps 
    1.97 +    [real_minus_add_distrib]));
    1.98 +qed "sumr_minus";
    1.99 +
   1.100 +context Arith.thy;
   1.101 +
   1.102 +goal Arith.thy "!!n. ~ Suc n <= m + k ==> ~ Suc n <= m";
   1.103 +by (auto_tac (claset() addSDs [not_leE],simpset()));
   1.104 +qed "lemma_not_Suc_add";
   1.105 +
   1.106 +context thy;
   1.107 +
   1.108 +Goal "sumr (m+k) (n+k) f = sumr m n (%i. f(i + k))";
   1.109 +by (induct_tac "n" 1);
   1.110 +by (Auto_tac);
   1.111 +qed "sumr_shift_bounds";
   1.112 +
   1.113 +Goal "sumr 0 (n + n) (%i. (- #1) ^ Suc i) = #0";
   1.114 +by (induct_tac "n" 1);
   1.115 +by (Auto_tac);
   1.116 +qed "sumr_minus_one_realpow_zero";
   1.117 +Addsimps [sumr_minus_one_realpow_zero];
   1.118 +
   1.119 +Goal "sumr 0 (n + n) (%i. (#-1) ^ Suc i) = #0";
   1.120 +by (induct_tac "n" 1);
   1.121 +by (Auto_tac);
   1.122 +qed "sumr_minus_one_realpow_zero2";
   1.123 +Addsimps [sumr_minus_one_realpow_zero2];
   1.124 +
   1.125 +Goal "m < Suc n ==> Suc n - m = Suc (n - m)";
   1.126 +by (dtac less_eq_Suc_add 1);
   1.127 +by (Auto_tac);
   1.128 +val Suc_diff_n = result();
   1.129 +
   1.130 +Goal "(ALL n. m <= Suc n --> f n = r) & m <= na \
   1.131 +\                --> sumr m na f = (real_of_nat (na - m) * r)";
   1.132 +by (induct_tac "na" 1);
   1.133 +by (Step_tac 1);
   1.134 +by (asm_full_simp_tac (simpset() addsimps [le_Suc_eq])  2);
   1.135 +by (Step_tac 1);
   1.136 +by (dres_inst_tac [("x","n")] spec 3);
   1.137 +by (auto_tac (claset() addSDs [le_imp_less_or_eq],
   1.138 +    simpset()));
   1.139 +by (asm_simp_tac (simpset() addsimps [real_add_mult_distrib,
   1.140 +    Suc_diff_n]) 1);
   1.141 +qed_spec_mp "sumr_interval_const";
   1.142 +
   1.143 +Goal "(ALL n. m <= n --> f n = r) & m <= na \
   1.144 +\     --> sumr m na f = (real_of_nat (na - m) * r)";
   1.145 +by (induct_tac "na" 1);
   1.146 +by (Step_tac 1);
   1.147 +by (asm_full_simp_tac (simpset() addsimps [le_Suc_eq])  2);
   1.148 +by (Step_tac 1);
   1.149 +by (dres_inst_tac [("x","n")] spec 3);
   1.150 +by (auto_tac (claset() addSDs [le_imp_less_or_eq],
   1.151 +    simpset()));
   1.152 +by (asm_simp_tac (simpset() addsimps [Suc_diff_n,
   1.153 +    real_add_mult_distrib]) 1);
   1.154 +qed_spec_mp "sumr_interval_const2";
   1.155 +
   1.156 +Goal "(m <= n)= (m < Suc n)";
   1.157 +by (Auto_tac);
   1.158 +qed "le_eq_less_Suc";
   1.159 +
   1.160 +Goal "(ALL n. m <= n --> #0 <= f n) & m < na \
   1.161 +\                --> sumr 0 m f <= sumr 0 na f";
   1.162 +by (induct_tac "na" 1);
   1.163 +by (Step_tac 1);
   1.164 +by (ALLGOALS(asm_full_simp_tac (simpset() addsimps 
   1.165 +    [le_eq_less_Suc RS sym])));
   1.166 +by (ALLGOALS(dres_inst_tac [("x","n")] spec));
   1.167 +by (Step_tac 1);
   1.168 +by (dtac le_imp_less_or_eq 1 THEN Step_tac 1);
   1.169 +by (dtac real_add_le_mono 2);
   1.170 +by (dres_inst_tac [("i","sumr 0 m f")] 
   1.171 +    (real_le_refl RS real_add_le_mono) 1);
   1.172 +by (Auto_tac);
   1.173 +qed_spec_mp "sumr_le";
   1.174 +
   1.175 +Goal "!!f g. (ALL r. m <= r & r < n --> f r <= g r) \
   1.176 +\                --> sumr m n f <= sumr m n g";
   1.177 +by (induct_tac "n" 1);
   1.178 +by (auto_tac (claset() addIs [real_add_le_mono],
   1.179 +    simpset() addsimps [le_def]));
   1.180 +qed_spec_mp "sumr_le2";
   1.181 +
   1.182 +Goal "(ALL n. #0 <= f n) --> #0 <= sumr m n f";
   1.183 +by (induct_tac "n" 1);
   1.184 +by (auto_tac (claset(),simpset() addsimps 
   1.185 +    [rename_numerals real_le_add_order]));
   1.186 +qed_spec_mp "sumr_ge_zero";
   1.187 +
   1.188 +Goal "(ALL n. m <= n --> #0 <= f n) --> #0 <= sumr m n f";
   1.189 +by (induct_tac "n" 1);
   1.190 +by (auto_tac (claset() addIs [rename_numerals real_le_add_order] 
   1.191 +    addDs [leI],simpset()));
   1.192 +qed_spec_mp "sumr_ge_zero2";
   1.193 +
   1.194 +Goal "#0 <= sumr m n (%n. abs (f n))";
   1.195 +by (induct_tac "n" 1);
   1.196 +by (auto_tac (claset() addSIs [rename_numerals real_le_add_order,
   1.197 +    abs_ge_zero],simpset()));
   1.198 +qed "sumr_rabs_ge_zero";
   1.199 +Addsimps [sumr_rabs_ge_zero];
   1.200 +AddSIs [sumr_rabs_ge_zero]; 
   1.201 +
   1.202 +Goal "abs (sumr m n (%n. abs (f n))) = (sumr m n (%n. abs (f n)))";
   1.203 +by (induct_tac "n" 1);
   1.204 +by (Auto_tac THEN arith_tac 1);
   1.205 +qed "rabs_sumr_rabs_cancel";
   1.206 +Addsimps [rabs_sumr_rabs_cancel];
   1.207 +
   1.208 +Goal "ALL n. N <= n --> f n = #0 \
   1.209 +\     ==> ALL m n. N <= m --> sumr m n f = #0";   
   1.210 +by (Step_tac 1);
   1.211 +by (induct_tac "n" 1);
   1.212 +by (Auto_tac);
   1.213 +qed "sumr_zero";
   1.214 +
   1.215 +Goal "Suc N <= n --> N <= n - 1";
   1.216 +by (induct_tac "n" 1);
   1.217 +by (Auto_tac);
   1.218 +qed_spec_mp "Suc_le_imp_diff_ge";
   1.219 +
   1.220 +Goal "ALL n. N <= n --> f (Suc n) = #0 \
   1.221 +\     ==> ALL m n. Suc N <= m --> sumr m n f = #0";   
   1.222 +by (rtac sumr_zero 1 THEN Step_tac 1);
   1.223 +by (subgoal_tac "0 < n" 1);
   1.224 +by (dtac Suc_le_imp_diff_ge 1);
   1.225 +by (Auto_tac);
   1.226 +qed "Suc_le_imp_diff_ge2";
   1.227 +
   1.228 +(* proved elsewhere? *)
   1.229 +Goal "(0 < n) = (EX m. n = Suc m)";
   1.230 +by (induct_tac "n" 1);
   1.231 +by (Auto_tac);
   1.232 +qed "gt_zero_eq_Ex";
   1.233 +
   1.234 +Goal "sumr 1 n (%n. f(n) * #0 ^ n) = #0";
   1.235 +by (induct_tac "n" 1);
   1.236 +by (auto_tac (claset(),simpset() addsimps [gt_zero_eq_Ex]));
   1.237 +qed "sumr_one_lb_realpow_zero";
   1.238 +Addsimps [sumr_one_lb_realpow_zero];
   1.239 +
   1.240 +Goalw [real_diff_def] "sumr m n f - sumr m n g = sumr m n (%n. f n - g n)";
   1.241 +by (simp_tac (simpset() addsimps [sumr_add RS sym,sumr_minus]) 1);
   1.242 +qed "sumr_diff";
   1.243 +
   1.244 +Goal "(ALL p. (m <= p & p < m + n --> (f p = g p))) --> sumr m n f = sumr m n g";
   1.245 +by (induct_tac "n" 1);
   1.246 +by (Auto_tac);
   1.247 +qed_spec_mp "sumr_subst";
   1.248 +
   1.249 +Goal "(ALL p. m <= p & p < m + n --> (f(p) <= K)) \
   1.250 +\     --> (sumr m (m + n) f <= (real_of_nat n * K))";
   1.251 +by (induct_tac "n" 1);
   1.252 +by (auto_tac (claset() addIs [real_add_le_mono],
   1.253 +    simpset() addsimps [real_add_mult_distrib]));
   1.254 +qed_spec_mp "sumr_bound";
   1.255 +
   1.256 +Goal "(ALL p. 0 <= p & p < n --> (f(p) <= K)) \
   1.257 +\     --> (sumr 0 n f <= (real_of_nat n * K))";
   1.258 +by (induct_tac "n" 1);
   1.259 +by (auto_tac (claset() addIs [real_add_le_mono],
   1.260 +    simpset() addsimps [real_add_mult_distrib]));
   1.261 +qed_spec_mp "sumr_bound2";
   1.262 +
   1.263 +Goal "sumr 0 n (%m. sumr (m * k) (m*k + k) f) = sumr 0 (n * k) f";
   1.264 +by (subgoal_tac "k = 0 | 0 < k" 1);
   1.265 +by (Auto_tac);
   1.266 +by (induct_tac "n" 1);
   1.267 +by (auto_tac (claset(),simpset() addsimps [sumr_split_add,add_commute]));
   1.268 +qed "sumr_group";
   1.269 +Addsimps [sumr_group];
   1.270 +
   1.271 +Goal "0 < (k::nat) --> ~(n*k < n)";
   1.272 +by (induct_tac "n" 1);
   1.273 +by (Auto_tac);
   1.274 +qed_spec_mp "lemma_summable_group";
   1.275 +Addsimps [lemma_summable_group];
   1.276 +
   1.277 +(*-------------------------------------------------------------------
   1.278 +                        Infinite sums
   1.279 +    Theorems follow from properties of limits and sums
   1.280 + -------------------------------------------------------------------*)
   1.281 +(*----------------------
   1.282 +   suminf is the sum   
   1.283 + ---------------------*)
   1.284 +Goalw [sums_def,summable_def] 
   1.285 +      "!!f. f sums l ==> summable f";
   1.286 +by (Blast_tac 1);
   1.287 +qed "sums_summable";
   1.288 +
   1.289 +Goalw [summable_def,suminf_def]
   1.290 +     "!!f. summable f ==> f sums (suminf f)";
   1.291 +by (blast_tac (claset() addIs [someI2]) 1);
   1.292 +qed "summable_sums";
   1.293 +
   1.294 +Goalw [summable_def,suminf_def,sums_def]
   1.295 +     "!!f. summable f ==> (%n. sumr 0 n f) ----> (suminf f)";
   1.296 +by (blast_tac (claset() addIs [someI2]) 1);
   1.297 +qed "summable_sumr_LIMSEQ_suminf";
   1.298 +
   1.299 +(*-------------------
   1.300 +    sum is unique                    
   1.301 + ------------------*)
   1.302 +Goal "!!f. f sums s ==> (s = suminf f)";
   1.303 +by (forward_tac [sums_summable RS summable_sums] 1);
   1.304 +by (auto_tac (claset() addSIs [LIMSEQ_unique],
   1.305 +    simpset() addsimps [sums_def]));
   1.306 +qed "sums_unique";
   1.307 +
   1.308 +Goalw [sums_def,LIMSEQ_def] 
   1.309 +     "!!f. ALL m. n <= Suc m --> f(m) = #0 \
   1.310 +\                ==> f sums (sumr 0 n f)";
   1.311 +by (Step_tac 1);
   1.312 +by (res_inst_tac [("x","n")] exI 1);
   1.313 +by (Step_tac 1 THEN forward_tac [le_imp_less_or_eq] 1);
   1.314 +by (Step_tac 1);
   1.315 +by (dres_inst_tac [("f","f")] sumr_split_add_minus 1);
   1.316 +by (ALLGOALS (Asm_simp_tac));
   1.317 +by (dtac (conjI RS sumr_interval_const) 1);
   1.318 +by (Auto_tac);
   1.319 +qed "series_zero";
   1.320 +
   1.321 +goalw Series.thy [sums_def,LIMSEQ_def] 
   1.322 +     "!!f. ALL m. n <= m --> f(m) = #0 \
   1.323 +\                ==> f sums (sumr 0 n f)";
   1.324 +by (Step_tac 1);
   1.325 +by (res_inst_tac [("x","n")] exI 1);
   1.326 +by (Step_tac 1 THEN forward_tac [le_imp_less_or_eq] 1);
   1.327 +by (Step_tac 1);
   1.328 +by (dres_inst_tac [("f","f")] sumr_split_add_minus 1);
   1.329 +by (ALLGOALS (Asm_simp_tac));
   1.330 +by (dtac (conjI RS sumr_interval_const2) 1);
   1.331 +by (Auto_tac);
   1.332 +qed "series_zero2";
   1.333 +
   1.334 +Goalw [sums_def] "x sums x0 ==> (%n. c * x(n)) sums (c * x0)";
   1.335 +by (auto_tac (claset() addSIs [LIMSEQ_mult] addIs [LIMSEQ_const], 
   1.336 +    simpset() addsimps [sumr_mult RS sym]));
   1.337 +qed "sums_mult";
   1.338 +
   1.339 +Goalw [sums_def] "[| x sums x0; y sums y0 |] ==> (%n. x n - y n) sums (x0 - y0)";
   1.340 +by (auto_tac (claset() addIs [LIMSEQ_diff],
   1.341 +    simpset() addsimps [sumr_diff RS sym]));
   1.342 +qed "sums_diff";
   1.343 +
   1.344 +goal Series.thy "!!f. summable f ==> suminf f * c = suminf(%n. f n * c)";
   1.345 +by (auto_tac (claset() addSIs [sums_unique,sums_mult,summable_sums],
   1.346 +    simpset() addsimps [real_mult_commute]));
   1.347 +qed "suminf_mult";
   1.348 +
   1.349 +goal Series.thy "!!f. summable f ==> c * suminf f  = suminf(%n. c * f n)";
   1.350 +by (auto_tac (claset() addSIs [sums_unique,sums_mult,summable_sums],
   1.351 +    simpset()));
   1.352 +qed "suminf_mult2";
   1.353 +
   1.354 +Goal "[| summable f; summable g |]  \
   1.355 +\     ==> suminf f - suminf g  = suminf(%n. f n - g n)";
   1.356 +by (auto_tac (claset() addSIs [sums_diff,sums_unique,summable_sums],simpset()));
   1.357 +qed "suminf_diff";
   1.358 +
   1.359 +goalw Series.thy [sums_def] 
   1.360 +       "!!x. x sums x0 ==> (%n. - x n) sums - x0";
   1.361 +by (auto_tac (claset() addSIs [LIMSEQ_minus],simpset() addsimps [sumr_minus]));
   1.362 +qed "sums_minus";
   1.363 +
   1.364 +Goal "[|summable f; 0 < k |] \
   1.365 +\     ==> (%n. sumr (n*k) (n*k + k) f) sums (suminf f)";
   1.366 +by (dtac summable_sums 1);
   1.367 +by (auto_tac (claset(),simpset() addsimps [sums_def,LIMSEQ_def]));
   1.368 +by (dres_inst_tac [("x","r")] spec 1 THEN Step_tac 1); 
   1.369 +by (res_inst_tac [("x","no")] exI 1 THEN Step_tac 1); 
   1.370 +by (dres_inst_tac [("x","n*k")] spec 1); 
   1.371 +by (auto_tac (claset() addSDs [not_leE],simpset()));
   1.372 +by (dres_inst_tac [("j","no")] less_le_trans 1);
   1.373 +by (Auto_tac);
   1.374 +qed "sums_group";
   1.375 +
   1.376 +Goal "[|summable f; ALL d. #0 < (f(n + (2 * d))) + f(n + ((2 * d) + 1))|] \
   1.377 +\     ==> sumr 0 n f < suminf f";
   1.378 +by (dtac summable_sums 1);
   1.379 +by (auto_tac (claset(),simpset() addsimps [sums_def,LIMSEQ_def]));
   1.380 +by (dres_inst_tac [("x","f(n) + f(n + 1)")] spec 1);
   1.381 +by (Auto_tac);
   1.382 +by (rtac ccontr 2 THEN dtac real_leI 2);
   1.383 +by (subgoal_tac "sumr 0 (n + 2) f <= sumr 0 (2 * (Suc no) + n) f" 2);
   1.384 +by (induct_tac "no" 3 THEN Simp_tac 3);
   1.385 +by (res_inst_tac [("j","sumr 0 (2*(Suc na)+n) f")] real_le_trans 3);
   1.386 +by (assume_tac 3);
   1.387 +by (dres_inst_tac [("x","Suc na")] spec 3);
   1.388 +by (dres_inst_tac [("x","0")] spec 1);
   1.389 +by (Asm_full_simp_tac 1);
   1.390 +by (asm_full_simp_tac (simpset() addsimps add_ac) 2);
   1.391 +by (rotate_tac 1 1 THEN dres_inst_tac [("x","2 * (Suc no) + n")] spec 1);
   1.392 +by (Step_tac 1 THEN Asm_full_simp_tac 1);
   1.393 +by (subgoal_tac "suminf f + (f(n) + f(n + 1)) <= \
   1.394 +\                 sumr 0 (2 * (Suc no) + n) f" 1);
   1.395 +by (res_inst_tac [("j","sumr 0 (n+2) f")] real_le_trans 2);
   1.396 +by (assume_tac 3);
   1.397 +by (res_inst_tac [("j","sumr 0 n f + (f(n) + f(n + 1))")] real_le_trans 2);
   1.398 +by (REPEAT(Asm_simp_tac 2));
   1.399 +by (subgoal_tac "suminf f <= sumr 0 (2 * (Suc no) + n) f" 1);
   1.400 +by (res_inst_tac [("j","suminf f + (f(n) + f(n + 1))")] real_le_trans 2);
   1.401 +by (assume_tac 3);
   1.402 +by (dres_inst_tac [("x","0")] spec 2);
   1.403 +by (Asm_full_simp_tac 2);
   1.404 +by (subgoal_tac "#0 <= sumr 0 (2 * Suc no + n) f + - suminf f" 1);
   1.405 +by (dtac (rename_numerals abs_eqI1) 1 );
   1.406 +by (Asm_full_simp_tac 1);
   1.407 +by (auto_tac (claset(),simpset() addsimps [real_le_def]));
   1.408 +qed "sumr_pos_lt_pair";
   1.409 +
   1.410 +(*-----------------------------------------------------------------
   1.411 +   Summable series of positive terms has limit >= any partial sum 
   1.412 + ----------------------------------------------------------------*)
   1.413 +Goal 
   1.414 +     "!!f. [| summable f; ALL m. n <= m --> #0 <= f(m) |] \
   1.415 +\          ==> sumr 0 n f <= suminf f";
   1.416 +by (dtac summable_sums 1);
   1.417 +by (rewtac sums_def);
   1.418 +by (cut_inst_tac [("k","sumr 0 n f")] LIMSEQ_const 1);
   1.419 +by (etac LIMSEQ_le 1 THEN Step_tac 1);
   1.420 +by (res_inst_tac [("x","n")] exI 1 THEN Step_tac 1);
   1.421 +by (dtac le_imp_less_or_eq 1 THEN Step_tac 1);
   1.422 +by (auto_tac (claset() addIs [sumr_le],simpset()));
   1.423 +qed "series_pos_le";
   1.424 +
   1.425 +Goal "!!f. [| summable f; ALL m. n <= m --> #0 < f(m) |] \
   1.426 +\          ==> sumr 0 n f < suminf f";
   1.427 +by (res_inst_tac [("j","sumr 0 (Suc n) f")] real_less_le_trans 1);
   1.428 +by (rtac series_pos_le 2);
   1.429 +by (Auto_tac);
   1.430 +by (dres_inst_tac [("x","m")] spec 1);
   1.431 +by (Auto_tac);
   1.432 +qed "series_pos_less";
   1.433 +
   1.434 +(*-------------------------------------------------------------------
   1.435 +                    sum of geometric progression                 
   1.436 + -------------------------------------------------------------------*)
   1.437 +(* lemma *)
   1.438 +
   1.439 +Goalw [real_diff_def] "x ~= y ==> x - y ~= (#0::real)";
   1.440 +by (asm_full_simp_tac (simpset() addsimps 
   1.441 +   [rename_numerals (real_eq_minus_iff2 RS sym)]) 1);
   1.442 +qed "real_not_eq_diff";
   1.443 +
   1.444 +Goal "x ~= #1 ==> sumr 0 n (%n. x ^ n) = (x ^ n - #1) * rinv(x - #1)";
   1.445 +by (induct_tac "n" 1);
   1.446 +by (Auto_tac);
   1.447 +by (res_inst_tac [("c1","x - #1")] (real_mult_right_cancel RS iffD1) 1);
   1.448 +by (auto_tac (claset(),simpset() addsimps [real_not_eq_diff,
   1.449 +    real_eq_minus_iff2 RS sym,real_mult_assoc,real_add_mult_distrib]));
   1.450 +by (asm_full_simp_tac (simpset() addsimps [real_add_mult_distrib2,
   1.451 +    real_diff_def,real_mult_commute]) 1);
   1.452 +qed "sumr_geometric";
   1.453 +
   1.454 +Goal "abs(x) < #1 ==> (%n. x ^ n) sums rinv(#1 - x)";
   1.455 +by (case_tac "x = #1" 1);
   1.456 +by (auto_tac (claset() addSDs [LIMSEQ_rabs_realpow_zero2],
   1.457 +    simpset() addsimps [sumr_geometric,abs_one,sums_def,
   1.458 +    real_diff_def,real_add_mult_distrib]));
   1.459 +by (rtac (real_add_zero_left RS subst) 1);
   1.460 +by (rtac (real_mult_0 RS subst) 1);
   1.461 +by (rtac LIMSEQ_add 1 THEN rtac LIMSEQ_mult 1);
   1.462 +by (dtac real_not_eq_diff 3);
   1.463 +by (auto_tac (claset() addIs [LIMSEQ_const], simpset() addsimps 
   1.464 +    [real_minus_rinv RS sym,real_diff_def,real_add_commute,
   1.465 +     rename_numerals LIMSEQ_rabs_realpow_zero2]));
   1.466 +qed "geometric_sums";
   1.467 +
   1.468 +(*-------------------------------------------------------------------
   1.469 +    Cauchy-type criterion for convergence of series (c.f. Harrison)
   1.470 + -------------------------------------------------------------------*)
   1.471 +Goalw [summable_def,sums_def,convergent_def]
   1.472 +      "summable f = convergent (%n. sumr 0 n f)";
   1.473 +by (Auto_tac);
   1.474 +qed "summable_convergent_sumr_iff";
   1.475 +
   1.476 +Goal "summable f = \
   1.477 +\     (ALL e. #0 < e --> (EX N. ALL m n. N <= m --> abs(sumr m n f) < e))";
   1.478 +by (auto_tac (claset(),simpset() addsimps [summable_convergent_sumr_iff,
   1.479 +    Cauchy_convergent_iff RS sym,Cauchy_def]));
   1.480 +by (ALLGOALS(dtac spec) THEN Auto_tac);
   1.481 +by (res_inst_tac [("x","M")] exI 1);
   1.482 +by (res_inst_tac [("x","N")] exI 2);
   1.483 +by (Auto_tac);
   1.484 +by (ALLGOALS(cut_inst_tac [("m","m"),("n","n")] less_linear));
   1.485 +by (Auto_tac);
   1.486 +by (ftac (le_less_trans RS less_imp_le) 1 THEN assume_tac 1);
   1.487 +by (dres_inst_tac [("x","n")] spec 1);
   1.488 +by (dres_inst_tac [("x","m")] spec 1);
   1.489 +by (auto_tac (claset() addIs [(abs_minus_add_cancel RS subst)],
   1.490 +    simpset() addsimps [sumr_split_add_minus,abs_minus_add_cancel]));
   1.491 +qed "summable_Cauchy";
   1.492 +
   1.493 +(*-------------------------------------------------------------------
   1.494 +     Terms of a convergent series tend to zero
   1.495 +     > Goalw [LIMSEQ_def] "summable f ==> f ----> #0";
   1.496 +     Proved easily in HSeries after proving nonstandard case.
   1.497 + -------------------------------------------------------------------*)
   1.498 +(*-------------------------------------------------------------------
   1.499 +                    Comparison test
   1.500 + -------------------------------------------------------------------*)
   1.501 +Goal "[| EX N. ALL n. N <= n --> abs(f n) <= g n; \
   1.502 +\        summable g \
   1.503 +\     |] ==> summable f";
   1.504 +by (auto_tac (claset(),simpset() addsimps [summable_Cauchy]));
   1.505 +by (dtac spec 1 THEN Auto_tac);
   1.506 +by (res_inst_tac [("x","N + Na")] exI 1 THEN Auto_tac);
   1.507 +by (rotate_tac 2 1);
   1.508 +by (dres_inst_tac [("x","m")] spec 1);
   1.509 +by (Auto_tac THEN rotate_tac 2 1 THEN dres_inst_tac [("x","n")] spec 1);
   1.510 +by (res_inst_tac [("j","sumr m n (%k. abs(f k))")] real_le_less_trans 1);
   1.511 +by (rtac sumr_rabs 1);
   1.512 +by (res_inst_tac [("j","sumr m n g")] real_le_less_trans 1);
   1.513 +by (auto_tac (claset() addIs [sumr_le2],
   1.514 +    simpset() addsimps [abs_interval_iff]));
   1.515 +qed "summable_comparison_test";
   1.516 +
   1.517 +Goal "[| EX N. ALL n. N <= n --> abs(f n) <= g n; \
   1.518 +\        summable g \
   1.519 +\     |] ==> summable (%k. abs (f k))";
   1.520 +by (rtac summable_comparison_test 1);
   1.521 +by (auto_tac (claset(),simpset() addsimps [abs_idempotent]));
   1.522 +qed "summable_rabs_comparison_test";
   1.523 +
   1.524 +(*------------------------------------------------------------------*)
   1.525 +(*       Limit comparison property for series (c.f. jrh)            *)
   1.526 +(*------------------------------------------------------------------*)
   1.527 +Goal "[|ALL n. f n <= g n; summable f; summable g |] \
   1.528 +\     ==> suminf f <= suminf g";
   1.529 +by (REPEAT(dtac summable_sums 1));
   1.530 +by (auto_tac (claset() addSIs [LIMSEQ_le],simpset() addsimps [sums_def]));
   1.531 +by (rtac exI 1);
   1.532 +by (auto_tac (claset() addSIs [sumr_le2],simpset()));
   1.533 +qed "summable_le";
   1.534 +
   1.535 +Goal "[|ALL n. abs(f n) <= g n; summable g |] \
   1.536 +\     ==> summable f & suminf f <= suminf g";
   1.537 +by (auto_tac (claset() addIs [summable_comparison_test]
   1.538 +    addSIs [summable_le],simpset()));
   1.539 +by (auto_tac (claset(),simpset() addsimps [abs_le_interval_iff]));
   1.540 +qed "summable_le2";
   1.541 +
   1.542 +(*-------------------------------------------------------------------
   1.543 +         Absolute convergence imples normal convergence
   1.544 + -------------------------------------------------------------------*)
   1.545 +Goal "summable (%n. abs (f n)) ==> summable f";
   1.546 +by (auto_tac (claset(),simpset() addsimps [sumr_rabs,summable_Cauchy]));
   1.547 +by (dtac spec 1 THEN Auto_tac);
   1.548 +by (res_inst_tac [("x","N")] exI 1 THEN Auto_tac);
   1.549 +by (dtac spec 1 THEN Auto_tac);
   1.550 +by (res_inst_tac [("j","sumr m n (%n. abs(f n))")] real_le_less_trans 1);
   1.551 +by (auto_tac (claset() addIs [sumr_rabs],simpset()));
   1.552 +qed "summable_rabs_cancel";
   1.553 +
   1.554 +(*-------------------------------------------------------------------
   1.555 +         Absolute convergence of series
   1.556 + -------------------------------------------------------------------*)
   1.557 +Goal "summable (%n. abs (f n)) ==> abs(suminf f) <= suminf (%n. abs(f n))";
   1.558 +by (auto_tac (claset() addIs [LIMSEQ_le,LIMSEQ_imp_rabs,summable_rabs_cancel,
   1.559 +    summable_sumr_LIMSEQ_suminf,sumr_rabs],simpset()));
   1.560 +qed "summable_rabs";
   1.561 +
   1.562 +(*-------------------------------------------------------------------
   1.563 +                        The ratio test
   1.564 + -------------------------------------------------------------------*)
   1.565 +Goal "[| c <= #0; abs x <= c * abs y |] ==> x = (#0::real)";
   1.566 +by (dtac real_le_imp_less_or_eq 1);
   1.567 +by (Auto_tac);
   1.568 +by (dres_inst_tac [("x1","y")] (abs_ge_zero RS 
   1.569 +    rename_numerals real_mult_le_zero) 1);
   1.570 +by (asm_full_simp_tac (simpset() addsimps [real_mult_commute]) 1);
   1.571 +by (dtac real_le_trans 1 THEN assume_tac 1);
   1.572 +by (TRYALL(arith_tac));
   1.573 +qed "rabs_ratiotest_lemma";
   1.574 +
   1.575 +(* lemmas *)
   1.576 +Goal "#0 < r ==> (x * r ^ n) * rinv (r ^ n) = x";
   1.577 +by (auto_tac (claset(),simpset() addsimps 
   1.578 +    [real_mult_assoc,rename_numerals realpow_not_zero]));
   1.579 +val lemma_rinv_realpow = result();
   1.580 +
   1.581 +Goal "[| c ~= #0; ALL n. N <= n --> abs(f(Suc n)) <= c*abs(f n) |] \
   1.582 +\  ==> ALL n. N <= n --> abs(f(Suc n)) <= (c * c ^ n)* (rinv(c ^ n)*abs(f n))";
   1.583 +by (auto_tac (claset(),simpset() addsimps real_mult_ac));
   1.584 +by (res_inst_tac [("z2.1","c ^ n")] (real_mult_left_commute RS subst) 1);
   1.585 +by (auto_tac (claset(),simpset() addsimps [rename_numerals  
   1.586 +    realpow_not_zero]));
   1.587 +val lemma_rinv_realpow2 = result();
   1.588 +
   1.589 +Goal "(k::nat) <= l ==> (EX n. l = k + n)";
   1.590 +by (dtac le_imp_less_or_eq 1);
   1.591 +by (auto_tac (claset() addDs [less_eq_Suc_add],simpset()));
   1.592 +qed "le_Suc_ex";
   1.593 +
   1.594 +Goal "((k::nat) <= l) = (EX n. l = k + n)";
   1.595 +by (auto_tac (claset(),simpset() addsimps [le_Suc_ex]));
   1.596 +qed "le_Suc_ex_iff";
   1.597 +
   1.598 +Goal "!!c. [| c < #1; ALL n. N <= n --> abs(f(Suc n)) <= c*abs(f n) |] \
   1.599 +\     ==> summable f";
   1.600 +by (subgoal_tac "c <= #0 | #0 < c" 1 THEN Auto_tac);
   1.601 +by (asm_full_simp_tac (simpset() addsimps [summable_Cauchy]) 1);
   1.602 +by (Step_tac 1 THEN subgoal_tac "ALL n. N <= n --> f (Suc n) = #0" 1);
   1.603 +by (blast_tac (claset() addIs [rabs_ratiotest_lemma]) 2);
   1.604 +by (res_inst_tac [("x","Suc N")] exI 1 THEN Step_tac 1);
   1.605 +by (dtac Suc_le_imp_diff_ge2 1 THEN Auto_tac);
   1.606 +by (res_inst_tac [("g","%n. (abs (f N)* rinv(c ^ N))*c ^ n")] 
   1.607 +    summable_comparison_test 1);
   1.608 +by (res_inst_tac [("x","N")] exI 1 THEN Step_tac 1);
   1.609 +by (dtac (le_Suc_ex_iff RS iffD1) 1);
   1.610 +by (auto_tac (claset(),simpset() addsimps [realpow_add,
   1.611 +    CLAIM_SIMP "(a * b) * (c * d) = (a * d) * (b * (c::real))" real_mult_ac,
   1.612 +    rename_numerals realpow_not_zero]));
   1.613 +by (induct_tac "na" 1 THEN Auto_tac);
   1.614 +by (res_inst_tac [("j","c*abs(f(N + n))")] real_le_trans 1);
   1.615 +by (auto_tac (claset() addIs [real_mult_le_le_mono1],
   1.616 +    simpset() addsimps [summable_def, CLAIM_SIMP 
   1.617 +    "a * (b * c) = b * (a * (c::real))" real_mult_ac]));
   1.618 +by (res_inst_tac [("x","(abs(f N)*rinv(c ^ N))*rinv(#1 - c)")] exI 1);
   1.619 +by (auto_tac (claset() addSIs [sums_mult,geometric_sums],simpset() addsimps 
   1.620 +    [abs_eqI2]));
   1.621 +qed "ratio_test";
   1.622 +
   1.623 +
   1.624 +(*----------------------------------------------------------------------------*)
   1.625 +(* Differentiation of finite sum                                              *)
   1.626 +(*----------------------------------------------------------------------------*)
   1.627 +
   1.628 +Goal "(ALL r. m <= r & r < (m + n) --> DERIV (%x. f r x) x :> (f' r x)) \
   1.629 +\     --> DERIV (%x. sumr m n (%n. f n x)) x :> sumr m n (%r. f' r x)";
   1.630 +by (induct_tac "n" 1);
   1.631 +by (auto_tac (claset() addIs [DERIV_add],simpset()));
   1.632 +qed "DERIV_sumr";
   1.633 +
   1.634 +
   1.635 +
   1.636 +
   1.637 +
   1.638 +