more setsum tuning
authornipkow
Tue Feb 22 10:54:30 2005 +0100 (2005-02-22)
changeset 155430024472afce7
parent 15542 ee6cd48cf840
child 15544 5f3ef1ddda1f
more setsum tuning
src/HOL/Finite_Set.thy
src/HOL/Hyperreal/HSeries.thy
src/HOL/Hyperreal/Series.thy
     1.1 --- a/src/HOL/Finite_Set.thy	Mon Feb 21 19:23:46 2005 +0100
     1.2 +++ b/src/HOL/Finite_Set.thy	Tue Feb 22 10:54:30 2005 +0100
     1.3 @@ -905,11 +905,8 @@
     1.4  apply (erule finite_induct, auto simp:ACf.fold_insert [OF ACf_add])
     1.5  done
     1.6  
     1.7 -lemma setsum_0': "ALL a:F. f a = 0 ==> setsum f F = 0"
     1.8 -  apply (subgoal_tac "setsum f F = setsum (%x. 0) F")
     1.9 -  apply (erule ssubst, rule setsum_0)
    1.10 -  apply (rule setsum_cong, auto)
    1.11 -  done
    1.12 +lemma setsum_0': "ALL a:A. f a = 0 ==> setsum f A = 0"
    1.13 +by(simp add:setsum_cong)
    1.14  
    1.15  lemma setsum_Un_Int: "finite A ==> finite B ==>
    1.16    setsum g (A Un B) + setsum g (A Int B) = setsum g A + setsum g B"
    1.17 @@ -954,7 +951,7 @@
    1.18   apply (cases "finite B") 
    1.19    apply (simp add: setsum_Sigma)
    1.20   apply (cases "A={}", simp)
    1.21 - apply (simp add: setsum_0) 
    1.22 + apply (simp) 
    1.23  apply (auto simp add: setsum_def
    1.24              dest: finite_cartesian_productD1 finite_cartesian_productD2) 
    1.25  done
     2.1 --- a/src/HOL/Hyperreal/HSeries.thy	Mon Feb 21 19:23:46 2005 +0100
     2.2 +++ b/src/HOL/Hyperreal/HSeries.thy	Tue Feb 22 10:54:30 2005 +0100
     2.3 @@ -232,7 +232,7 @@
     2.4       "[| \<exists>N. \<forall>n. N \<le> n --> abs(f n) \<le> g n; NSsummable g |]
     2.5        ==> NSsummable (%k. abs (f k))"
     2.6  apply (rule NSsummable_comparison_test)
     2.7 -apply (auto simp add: abs_idempotent)
     2.8 +apply (auto)
     2.9  done
    2.10  
    2.11  ML
     3.1 --- a/src/HOL/Hyperreal/Series.thy	Mon Feb 21 19:23:46 2005 +0100
     3.2 +++ b/src/HOL/Hyperreal/Series.thy	Tue Feb 22 10:54:30 2005 +0100
     3.3 @@ -11,13 +11,13 @@
     3.4  theory Series
     3.5  imports SEQ Lim
     3.6  begin
     3.7 -
     3.8 +thm atLeastLessThan_empty
     3.9  (* FIXME why not globally? *)
    3.10  declare atLeastLessThan_empty[simp];
    3.11  declare atLeastLessThan_iff[iff]
    3.12  
    3.13  constdefs
    3.14 -   sums  :: "[nat=>real,real] => bool"     (infixr "sums" 80)
    3.15 +   sums  :: "(nat => real) => real => bool"     (infixr "sums" 80)
    3.16     "f sums s  == (%n. setsum f {0..<n}) ----> s"
    3.17  
    3.18     summable :: "(nat=>real) => bool"
    3.19 @@ -42,18 +42,9 @@
    3.20  
    3.21  (* Generalize from real to some algebraic structure? *)
    3.22  lemma sumr_minus_one_realpow_zero [simp]:
    3.23 -  "setsum (%i. (-1) ^ Suc i) {0..<2*n} = (0::real)"
    3.24 +  "(\<Sum>i=0..<2*n. (-1) ^ Suc i) = (0::real)"
    3.25  by (induct "n", auto)
    3.26  
    3.27 -(* FIXME get rid of this one! *)
    3.28 -lemma Suc_le_imp_diff_ge2:
    3.29 -     "[|\<forall>n \<ge> N. f (Suc n) = 0; Suc N \<le> m|] ==> setsum f {m..<n} = 0"
    3.30 -apply (rule setsum_0')
    3.31 -apply (case_tac "n", auto)
    3.32 -apply(erule_tac x = "a - 1" in allE)
    3.33 -apply (simp split:nat_diff_split)
    3.34 -done
    3.35 -
    3.36  (* FIXME this is an awful lemma! *)
    3.37  lemma sumr_one_lb_realpow_zero [simp]:
    3.38    "(\<Sum>n=Suc 0..<n. f(n) * (0::real) ^ n) = 0"
    3.39 @@ -61,10 +52,9 @@
    3.40  apply (case_tac [2] "n", auto)
    3.41  done
    3.42  
    3.43 -(* FIXME a bit specialized for [simp]! *)
    3.44 -lemma sumr_group [simp]:
    3.45 +lemma sumr_group:
    3.46       "(\<Sum>m=0..<n::nat. setsum f {m * k ..< m*k + k}) = setsum f {0 ..< n * k}"
    3.47 -apply (subgoal_tac "k = 0 | 0 < k", auto simp:setsum_0')
    3.48 +apply (subgoal_tac "k = 0 | 0 < k", auto)
    3.49  apply (induct "n")
    3.50  apply (simp_all add: setsum_add_nat_ivl add_commute)
    3.51  done
    3.52 @@ -132,7 +122,7 @@
    3.53  lemma sums_group:
    3.54       "[|summable f; 0 < k |] ==> (%n. setsum f {n*k..<n*k+k}) sums (suminf f)"
    3.55  apply (drule summable_sums)
    3.56 -apply (auto simp add: sums_def LIMSEQ_def)
    3.57 +apply (auto simp add: sums_def LIMSEQ_def sumr_group)
    3.58  apply (drule_tac x = r in spec, safe)
    3.59  apply (rule_tac x = no in exI, safe)
    3.60  apply (drule_tac x = "n*k" in spec)
    3.61 @@ -263,7 +253,7 @@
    3.62       "[| \<exists>N. \<forall>n \<ge> N. abs(f n) \<le> g n; summable g |] 
    3.63        ==> summable (%k. abs (f k))"
    3.64  apply (rule summable_comparison_test)
    3.65 -apply (auto simp add: abs_idempotent)
    3.66 +apply (auto)
    3.67  done
    3.68  
    3.69  text{*Limit comparison property for series (c.f. jrh)*}
    3.70 @@ -321,10 +311,14 @@
    3.71        ==> 0 < c | summable f"
    3.72  apply (simp (no_asm) add: linorder_not_le [symmetric])
    3.73  apply (simp add: summable_Cauchy)
    3.74 -apply (safe, subgoal_tac "\<forall>n. N \<le> n --> f (Suc n) = 0")
    3.75 -prefer 2 apply (blast intro: rabs_ratiotest_lemma)
    3.76 +apply (safe, subgoal_tac "\<forall>n. N < n --> f (n) = 0")
    3.77 + prefer 2
    3.78 + apply clarify
    3.79 + apply(erule_tac x = "n - 1" in allE)
    3.80 + apply (simp add:diff_Suc split:nat.splits)
    3.81 + apply (blast intro: rabs_ratiotest_lemma)
    3.82  apply (rule_tac x = "Suc N" in exI, clarify)
    3.83 -apply (drule_tac n=n in Suc_le_imp_diff_ge2, auto) 
    3.84 +apply(simp cong:setsum_ivl_cong)
    3.85  done
    3.86  
    3.87  lemma ratio_test:
    3.88 @@ -363,7 +357,6 @@
    3.89  val suminf_def = thm"suminf_def";
    3.90  
    3.91  val sumr_minus_one_realpow_zero = thm "sumr_minus_one_realpow_zero";
    3.92 -val Suc_le_imp_diff_ge2 = thm "Suc_le_imp_diff_ge2";
    3.93  val sumr_one_lb_realpow_zero = thm "sumr_one_lb_realpow_zero";
    3.94  val sumr_group = thm "sumr_group";
    3.95  val sums_summable = thm "sums_summable";