--- a/src/HOL/Hyperreal/HSeries.thy Fri Feb 18 11:48:42 2005 +0100
+++ b/src/HOL/Hyperreal/HSeries.thy Fri Feb 18 11:48:53 2005 +0100
@@ -73,12 +73,12 @@
lemma sumhr_add: "sumhr (m,n,f) + sumhr(m,n,g) = sumhr(m,n,%i. f i + g i)"
apply (cases m, cases n)
-apply (simp add: sumhr hypreal_add sumr_add)
+apply (simp add: sumhr hypreal_add setsum_addf)
done
lemma sumhr_mult: "hypreal_of_real r * sumhr(m,n,f) = sumhr(m,n,%n. r * f n)"
apply (cases m, cases n)
-apply (simp add: sumhr hypreal_of_real_def hypreal_mult sumr_mult)
+apply (simp add: sumhr hypreal_of_real_def hypreal_mult setsum_mult)
done
lemma sumhr_split_add: "n < p ==> sumhr(0,n,f) + sumhr(n,p,f) = sumhr(0,p,f)"
@@ -92,7 +92,7 @@
lemma sumhr_hrabs: "abs(sumhr(m,n,f)) \<le> sumhr(m,n,%i. abs(f i))"
apply (cases n, cases m)
-apply (simp add: sumhr hypreal_le hypreal_hrabs sumr_rabs)
+apply (simp add: sumhr hypreal_le hypreal_hrabs setsum_abs)
done
text{* other general version also needed *}
@@ -100,9 +100,8 @@
"(\<forall>r. m \<le> r & r < n --> f r = g r) -->
sumhr(hypnat_of_nat m, hypnat_of_nat n, f) =
sumhr(hypnat_of_nat m, hypnat_of_nat n, g)"
-apply (safe, drule sumr_fun_eq)
-apply (simp add: sumhr hypnat_of_nat_eq)
-done
+by (fastsimp simp add: sumhr hypnat_of_nat_eq intro:setsum_cong)
+
lemma sumhr_const:
"sumhr(0, n, %i. r) = hypreal_of_hypnat n * hypreal_of_real r"
@@ -119,7 +118,7 @@
lemma sumhr_minus: "sumhr(m, n, %i. - f i) = - sumhr(m, n, f)"
apply (cases m, cases n)
-apply (simp add: sumhr hypreal_minus sumr_minus)
+apply (simp add: sumhr hypreal_minus setsum_negf)
done
lemma sumhr_shift_bounds:
--- a/src/HOL/Hyperreal/Integration.thy Fri Feb 18 11:48:42 2005 +0100
+++ b/src/HOL/Hyperreal/Integration.thy Fri Feb 18 11:48:53 2005 +0100
@@ -343,7 +343,7 @@
lemma Integral_mult_const: "a \<le> b ==> Integral(a,b) (%x. c) (c*(b - a))"
apply (auto simp add: order_le_less rsum_def Integral_def)
apply (rule_tac x = "%x. b - a" in exI)
-apply (auto simp add: sumr_mult [symmetric] gauge_def abs_interval_iff
+apply (auto simp add: setsum_mult [symmetric] gauge_def abs_interval_iff
right_diff_distrib [symmetric] partition tpart_def)
done
@@ -351,7 +351,7 @@
"[| a \<le> b; Integral(a,b) f k |] ==> Integral(a,b) (%x. c * f x) (c * k)"
apply (auto simp add: order_le_less
dest: Integral_unique [OF order_refl Integral_zero])
-apply (auto simp add: rsum_def Integral_def sumr_mult [symmetric] mult_assoc)
+apply (auto simp add: rsum_def Integral_def setsum_mult[symmetric] mult_assoc)
apply (rule_tac a2 = c in abs_ge_zero [THEN real_le_imp_less_or_eq, THEN disjE])
prefer 2 apply force
apply (drule_tac x = "e/abs c" in spec, auto)
@@ -459,13 +459,13 @@
in sumr_partition_eq_diff_bounds)
apply (simp add: partition_lhs partition_rhs)
apply (drule sym, simp)
-apply (simp (no_asm) add: sumr_diff)
-apply (rule sumr_rabs [THEN order_trans])
+apply (simp (no_asm) add: setsum_subtractf[symmetric])
+apply (rule setsum_abs [THEN order_trans])
apply (subgoal_tac "ea = sumr 0 (psize D) (%n. (ea / (b - a)) * (D (Suc n) - (D n)))")
apply (simp add: abs_minus_commute)
apply (rule_tac t = ea in ssubst, assumption)
apply (rule sumr_le2)
-apply (rule_tac [2] sumr_mult [THEN subst])
+apply (rule_tac [2] setsum_mult [THEN subst])
apply (auto simp add: partition_rhs partition_lhs partition_lb partition_ub
fine_def)
done
@@ -769,7 +769,7 @@
done
lemma rsum_add: "rsum (D, p) (%x. f x + g x) = rsum (D, p) f + rsum(D, p) g"
-by (simp add: rsum_def sumr_add left_distrib)
+by (simp add: rsum_def setsum_addf left_distrib)
text{* Bartle/Sherbert: Theorem 10.1.5 p. 278 *}
lemma Integral_add_fun:
--- a/src/HOL/Hyperreal/MacLaurin.thy Fri Feb 18 11:48:42 2005 +0100
+++ b/src/HOL/Hyperreal/MacLaurin.thy Fri Feb 18 11:48:53 2005 +0100
@@ -267,7 +267,7 @@
apply (rule_tac x = "-t" in exI, auto)
apply (subgoal_tac "(\<Sum>m = 0..<n. -1 ^ m * diff m 0 * (-h)^m / real(fact m)) =
(\<Sum>m = 0..<n. diff m 0 * h ^ m / real(fact m))")
-apply (rule_tac [2] sumr_fun_eq)
+apply (rule_tac [2] setsum_cong[OF refl])
apply (auto simp add: divide_inverse power_mult_distrib [symmetric])
done
@@ -435,7 +435,7 @@
apply (drule_tac x = x in spec, simp)
apply (erule ssubst)
apply (rule_tac x = t in exI, simp)
-apply (rule sumr_fun_eq)
+apply (rule setsum_cong[OF refl])
apply (auto simp add: sin_zero_iff odd_Suc_mult_two_ex times_divide_eq)
done
@@ -465,7 +465,7 @@
apply (simp (no_asm) add: times_divide_eq)
apply (erule ssubst)
apply (rule_tac x = t in exI, simp)
-apply (rule sumr_fun_eq)
+apply (rule setsum_cong[OF refl])
apply (auto simp add: sin_zero_iff odd_Suc_mult_two_ex times_divide_eq)
done
@@ -483,7 +483,7 @@
apply (simp (no_asm) add: times_divide_eq)
apply (erule ssubst)
apply (rule_tac x = t in exI, simp)
-apply (rule sumr_fun_eq)
+apply (rule setsum_cong[OF refl])
apply (auto simp add: sin_zero_iff odd_Suc_mult_two_ex times_divide_eq)
done
@@ -516,7 +516,7 @@
apply (drule_tac x = x in spec, simp)
apply (erule ssubst)
apply (rule_tac x = t in exI, simp)
-apply (rule sumr_fun_eq)
+apply (rule setsum_cong[OF refl])
apply (auto simp add: cos_zero_iff even_mult_two_ex)
done
@@ -535,7 +535,7 @@
apply (simp (no_asm) add: times_divide_eq)
apply (erule ssubst)
apply (rule_tac x = t in exI, simp)
-apply (rule sumr_fun_eq)
+apply (rule setsum_cong[OF refl])
apply (auto simp add: cos_zero_iff even_mult_two_ex)
done
@@ -554,7 +554,7 @@
apply (simp (no_asm) add: times_divide_eq)
apply (erule ssubst)
apply (rule_tac x = t in exI, simp)
-apply (rule sumr_fun_eq)
+apply (rule setsum_cong[OF refl])
apply (auto simp add: cos_zero_iff even_mult_two_ex)
done
@@ -585,10 +585,10 @@
apply (rule lemma_DERIV_subst, rule DERIV_minus, rule DERIV_cos, simp)
apply (erule ssubst)
apply (rule sin_bound_lemma)
- apply (rule sumr_fun_eq, safe)
- apply (rule_tac f = "%u. u * (x^r)" in arg_cong)
+ apply (rule setsum_cong[OF refl])
+ apply (rule_tac f = "%u. u * (x^xa)" in arg_cong)
apply (subst even_even_mod_4_iff)
- apply (cut_tac m=r in mod_exhaust_less_4, simp, safe)
+ apply (cut_tac m=xa in mod_exhaust_less_4, simp, safe)
apply (simp_all add:even_num_iff)
apply (drule lemma_even_mod_4_div_2[simplified])
apply(simp add: numeral_2_eq_2 divide_inverse)
--- a/src/HOL/Hyperreal/Series.thy Fri Feb 18 11:48:42 2005 +0100
+++ b/src/HOL/Hyperreal/Series.thy Fri Feb 18 11:48:53 2005 +0100
@@ -11,13 +11,15 @@
imports SEQ Lim
begin
+declare atLeastLessThan_empty[simp];
+
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)
- "f sums s == (%n. sumr 0 n f) ----> s"
+ "f sums s == (%n. setsum f {0..<n}) ----> s"
summable :: "(nat=>real) => bool"
"summable f == (\<exists>s. f sums s)"
@@ -27,9 +29,10 @@
lemma sumr_Suc [simp]:
- "sumr m (Suc n) f = (if n < m then 0 else sumr m n f + f(n))"
-by (simp add: atLeastLessThanSuc)
+ "setsum f {m..<Suc n} = (if n < m then 0 else setsum f {m..<n} + f(n))"
+by (simp add: atLeastLessThanSuc add_commute)
+(*
lemma sumr_add: "sumr m n f + sumr m n g = sumr m n (%n. f n + g n)"
by (simp add: setsum_addf)
@@ -42,13 +45,22 @@
apply (rename_tac k)
apply (subgoal_tac "n=k", auto)
done
+*)
+
+lemma sumr_split_add: "\<lbrakk> m \<le> n; n \<le> p \<rbrakk> \<Longrightarrow>
+ setsum f {m..<n} + setsum f {n..<p} = setsum f {m..<p::nat}"
+by (simp add:setsum_Un_disjoint[symmetric] ivl_disj_int ivl_disj_un)
lemma sumr_split_add_minus:
"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])
+using sumr_split_add [of 0 n p f,symmetric]
apply (simp add: add_ac)
done
+lemma sumr_diff_mult_const: "sumr 0 n f - (real n*r) = sumr 0 n (%i. f i - r)"
+by (simp add: diff_minus setsum_addf real_of_nat_def)
+
+(*
lemma sumr_rabs: "abs(sumr m n (f::nat=>real)) \<le> sumr m n (%i. abs(f i))"
by (simp add: setsum_abs)
@@ -60,14 +72,12 @@
"(\<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)"
-by (simp add: diff_minus setsum_addf real_of_nat_def)
-
lemma sumr_less_bounds_zero [simp]: "n < m ==> sumr m n f = 0"
by (simp add: atLeastLessThan_empty)
lemma sumr_minus: "sumr m n (%i. - f i) = - sumr m n f"
by (simp add: Finite_Set.setsum_negf)
+*)
lemma sumr_shift_bounds: "sumr (m+k) (n+k) f = sumr m n (%i. f(i + k))"
by (induct "n", auto)
@@ -114,6 +124,7 @@
apply (drule_tac x = n in spec, arith)
done
+(* FIXME generalize *)
lemma rabs_sumr_rabs_cancel [simp]:
"abs (sumr m n (%k. abs (f k))) = (sumr m n (%k. abs (f k)))"
by (induct "n", simp_all add: add_increasing)
@@ -132,10 +143,10 @@
apply (induct "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)
-
+by (simp add: diff_minus setsum_addf setsum_negf)
+*)
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 "n", auto)
@@ -213,14 +224,14 @@
done
lemma sums_mult: "x sums x0 ==> (%n. c * x(n)) sums (c * x0)"
-by (auto simp add: sums_def sumr_mult [symmetric]
+by (auto simp add: sums_def setsum_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)
+by (auto simp add: sums_def setsum_subtractf 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)
@@ -234,7 +245,7 @@
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)
+by (auto simp add: sums_def intro!: LIMSEQ_minus simp add: setsum_negf)
lemma sums_group:
"[|summable f; 0 < k |] ==> (%n. sumr (n*k) (n*k + k) f) sums (suminf f)"
@@ -356,7 +367,7 @@
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 setsum_abs)
apply (rule_tac y = "sumr m n g" in order_le_less_trans)
apply (auto intro: sumr_le2 simp add: abs_interval_iff)
done
@@ -387,18 +398,18 @@
text{*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 (auto simp add: 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)
+apply (auto)
done
text{*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)
+by (auto intro: LIMSEQ_le LIMSEQ_imp_rabs summable_rabs_cancel summable_sumr_LIMSEQ_suminf)
subsection{* The Ratio Test*}
@@ -465,19 +476,13 @@
val summable_def = thm"summable_def";
val suminf_def = thm"suminf_def";
-val sumr_add = thm "sumr_add";
-val sumr_mult = thm "sumr_mult";
val sumr_split_add = thm "sumr_split_add";
-val sumr_rabs = thm "sumr_rabs";
-val sumr_fun_eq = thm "sumr_fun_eq";
-val sumr_diff_mult_const = thm "sumr_diff_mult_const";
val sumr_minus_one_realpow_zero = thm "sumr_minus_one_realpow_zero";
val sumr_le2 = thm "sumr_le2";
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";
--- a/src/HOL/Hyperreal/Transcendental.thy Fri Feb 18 11:48:42 2005 +0100
+++ b/src/HOL/Hyperreal/Transcendental.thy Fri Feb 18 11:48:53 2005 +0100
@@ -366,7 +366,7 @@
lemma lemma_realpow_diff_sumr:
"sumr 0 (Suc n) (%p. (x ^ p) * y ^ ((Suc n) - p)) =
y * sumr 0 (Suc n) (%p. (x ^ p) * (y ^ (n - p)))"
-apply (auto simp add: sumr_mult simp del: sumr_Suc)
+apply (auto simp add: setsum_mult simp del: sumr_Suc)
apply (rule sumr_subst)
apply (intro strip)
apply (subst lemma_realpow_diff)
@@ -504,10 +504,10 @@
simp del: realpow_Suc sumr_Suc)
apply (auto simp add: lemma_realpow_rev_sumr simp del: sumr_Suc)
apply (auto simp add: real_of_nat_Suc sumr_diff_mult_const left_distrib
- sumdiff lemma_termdiff1 sumr_mult)
+ sumdiff lemma_termdiff1 setsum_mult)
apply (auto intro!: sumr_subst simp add: diff_minus real_add_assoc)
apply (simp add: diff_minus [symmetric] less_iff_Suc_add)
-apply (auto simp add: sumr_mult lemma_realpow_diff_sumr2 mult_ac simp
+apply (auto simp add: setsum_mult lemma_realpow_diff_sumr2 mult_ac simp
del: sumr_Suc realpow_Suc)
done
@@ -518,7 +518,7 @@
apply (subst lemma_termdiff2, assumption)
apply (simp add: abs_mult mult_commute)
apply (simp add: mult_commute [of _ "K ^ (n - 2)"])
-apply (rule sumr_rabs [THEN real_le_trans])
+apply (rule setsum_abs [THEN real_le_trans])
apply (simp add: mult_assoc [symmetric])
apply (simp add: mult_commute [of _ "real (n - Suc 0)"])
apply (auto intro!: sumr_bound2 simp add: abs_mult)
@@ -535,7 +535,7 @@
apply (subgoal_tac [2] "0 \<le> K")
apply (drule_tac [2] n = d in zero_le_power)
apply (auto simp del: sumr_Suc)
-apply (rule sumr_rabs [THEN real_le_trans])
+apply (rule setsum_abs [THEN real_le_trans])
apply (rule sumr_bound2, auto dest!: less_add_one intro!: mult_mono simp add: abs_mult power_add)
apply (auto intro!: power_mono zero_le_power simp add: power_abs, arith+)
done
--- a/src/HOL/Real/Real.thy Fri Feb 18 11:48:42 2005 +0100
+++ b/src/HOL/Real/Real.thy Fri Feb 18 11:48:53 2005 +0100
@@ -1,2 +1,4 @@
-
-Real = RComplete + RealPow
+theory Real
+imports RComplete RealPow
+begin
+end
\ No newline at end of file