src/HOL/Hyperreal/Series.thy
 changeset 15047 fa62de5862b9 parent 15003 6145dd7538d7 child 15053 405be2b48f5b
```--- a/src/HOL/Hyperreal/Series.thy	Thu Jul 15 13:24:45 2004 +0200
+++ b/src/HOL/Hyperreal/Series.thy	Thu Jul 15 15:32:32 2004 +0200
@@ -9,10 +9,9 @@

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))"
+syntax sumr :: "[nat,nat,(nat=>real)] => real"
+translations
+  "sumr m n f" => "setsum (f::nat=>real) (atLeastLessThan m n)"

constdefs
sums  :: "[nat=>real,real] => bool"     (infixr "sums" 80)
@@ -25,83 +24,52 @@
"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)
+text{*This simprule replaces @{text "sumr 0 n"} by a term involving
+  @{term lessThan}, making other simprules inapplicable.*}
+declare atLeast0LessThan [simp del]

-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_Suc [simp]:
+     "sumr m (Suc n) f = (if n < m then 0 else sumr m n f + f(n))"

lemma sumr_add: "sumr m n f + sumr m n g = sumr m n (%n. f n + g n)"
-apply (induct_tac "n")
-done

-lemma sumr_mult: "r * sumr m n f = sumr m n (%n. r * f n)"
-apply (induct_tac "n")
-done
+lemma sumr_mult: "r * sumr m n (f::nat=>real) = sumr m n (%n. r * f n)"

-     "n < p --> sumr 0 n f + sumr n p f = sumr 0 p f"
+     "n < p --> sumr 0 n f + sumr n p f = sumr 0 p (f::nat=>real)"
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"
+     "n < p ==> sumr 0 p f + - sumr 0 n f = sumr n p (f::nat=>real)"
apply (drule_tac f1 = f in sumr_split_add [symmetric])
done

-     "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
-
-     "[| 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)
-done
+lemma sumr_rabs: "abs(sumr m n  (f::nat=>real)) \<le> sumr m n (%i. abs(f i))"

-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_rabs_ge_zero [iff]: "0 \<le> sumr m n (%n. abs (f n))"

-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
-
-     "sumr 0 n f + -(real n * r) = sumr 0 n (%i. f i + -r)"
-by (simp only: sumr_add [symmetric] minus_mult_right, simp)
+text{*Just a congruence rule*}
+lemma sumr_fun_eq:
+     "(\<forall>r. m \<le> r & r < n --> f r = g r) ==> sumr m n f = sumr m n g"
+by (auto intro: setsum_cong)

lemma sumr_diff_mult_const: "sumr 0 n f - (real n*r) = sumr 0 n (%i. f i - r)"

-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_less_bounds_zero [simp]: "n < m ==> sumr m n f = 0"

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)
@@ -109,15 +77,12 @@
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)"
-
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)
+apply (simp add: left_distrib real_of_nat_Suc split: nat_diff_split)
done

lemma sumr_interval_const2 [rule_format (no_asm)]:
@@ -126,16 +91,17 @@
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)
+apply (simp add: left_distrib real_of_nat_Suc split: nat_diff_split)
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 (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 (arith)
apply (drule_tac a = "sumr 0 m f" in order_refl [THEN add_mono], auto)
done

@@ -156,9 +122,6 @@
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)
-
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")
@@ -198,7 +161,7 @@
"(\<forall>p. 0 \<le> p & p < n --> (f(p) \<le> K))
--> (sumr 0 n f \<le> (real n * K))"
apply (induct_tac "n")
done

lemma sumr_group [simp]:
@@ -523,35 +486,18 @@

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_mult = thm "sumr_mult";
val sumr_rabs = thm "sumr_rabs";
val sumr_fun_eq = thm "sumr_fun_eq";
-val sumr_const = thm "sumr_const";