src/HOL/Hyperreal/Series.ML
changeset 11468 02cd5d5bc497
parent 10919 144ede948e58
child 11701 3d51fbf81c17
     1.1 --- a/src/HOL/Hyperreal/Series.ML	Mon Aug 06 16:43:40 2001 +0200
     1.2 +++ b/src/HOL/Hyperreal/Series.ML	Tue Aug 07 16:36:52 2001 +0200
     1.3 @@ -191,28 +191,17 @@
     1.4  by (Auto_tac);
     1.5  qed "sumr_zero";
     1.6  
     1.7 -Goal "Suc N <= n --> N <= n - 1";
     1.8 -by (induct_tac "n" 1);
     1.9 -by (Auto_tac);
    1.10 -qed_spec_mp "Suc_le_imp_diff_ge";
    1.11 -
    1.12  Goal "ALL n. N <= n --> f (Suc n) = #0 \
    1.13  \     ==> ALL m n. Suc N <= m --> sumr m n f = #0";   
    1.14  by (rtac sumr_zero 1 THEN Step_tac 1);
    1.15 -by (subgoal_tac "0 < n" 1);
    1.16 -by (dtac Suc_le_imp_diff_ge 1);
    1.17 -by (Auto_tac);
    1.18 +by (case_tac "n" 1);
    1.19 +by Auto_tac; 
    1.20  qed "Suc_le_imp_diff_ge2";
    1.21  
    1.22 -(* proved elsewhere? *)
    1.23 -Goal "(0 < n) = (EX m. n = Suc m)";
    1.24 +Goal "sumr 1' n (%n. f(n) * #0 ^ n) = #0";
    1.25  by (induct_tac "n" 1);
    1.26 -by (Auto_tac);
    1.27 -qed "gt_zero_eq_Ex";
    1.28 -
    1.29 -Goal "sumr 1 n (%n. f(n) * #0 ^ n) = #0";
    1.30 -by (induct_tac "n" 1);
    1.31 -by (auto_tac (claset(),simpset() addsimps [gt_zero_eq_Ex]));
    1.32 +by (case_tac "n" 2);
    1.33 +by Auto_tac; 
    1.34  qed "sumr_one_lb_realpow_zero";
    1.35  Addsimps [sumr_one_lb_realpow_zero];
    1.36  
    1.37 @@ -220,7 +209,7 @@
    1.38  by (simp_tac (simpset() addsimps [sumr_add RS sym,sumr_minus]) 1);
    1.39  qed "sumr_diff";
    1.40  
    1.41 -Goal "(ALL p. (m <= p & p < m + n --> (f p = g p))) --> sumr m n f = sumr m n g";
    1.42 +Goal "(ALL p. m <= p & p < m+n --> (f p = g p)) --> sumr m n f = sumr m n g";
    1.43  by (induct_tac "n" 1);
    1.44  by (Auto_tac);
    1.45  qed_spec_mp "sumr_subst";
    1.46 @@ -564,7 +553,8 @@
    1.47  by (asm_full_simp_tac (simpset() addsimps [summable_Cauchy]) 1);
    1.48  by (Step_tac 1 THEN subgoal_tac "ALL n. N <= n --> f (Suc n) = #0" 1);
    1.49  by (blast_tac (claset() addIs [rabs_ratiotest_lemma]) 2);
    1.50 -by (res_inst_tac [("x","Suc N")] exI 1 THEN Step_tac 1);
    1.51 +by (res_inst_tac [("x","Suc N")] exI 1);
    1.52 +by (Clarify_tac 1); 
    1.53  by (dtac Suc_le_imp_diff_ge2 1 THEN Auto_tac);
    1.54  qed "ratio_test_lemma2";
    1.55