--- a/src/HOL/RComplete.thy Wed Sep 23 11:06:32 2009 +0100
+++ b/src/HOL/RComplete.thy Fri Sep 25 13:47:28 2009 +0100
@@ -14,6 +14,9 @@
lemma real_sum_of_halves: "x/2 + x/2 = (x::real)"
by simp
+lemma abs_diff_less_iff:
+ "(\<bar>x - a\<bar> < (r::'a::ordered_idom)) = (a - r < x \<and> x < a + r)"
+ by auto
subsection {* Completeness of Positive Reals *}
@@ -301,6 +304,20 @@
qed
qed
+text{*A version of the same theorem without all those predicates!*}
+lemma reals_complete2:
+ fixes S :: "(real set)"
+ assumes "\<exists>y. y\<in>S" and "\<exists>(x::real). \<forall>y\<in>S. y \<le> x"
+ shows "\<exists>x. (\<forall>y\<in>S. y \<le> x) &
+ (\<forall>z. ((\<forall>y\<in>S. y \<le> z) --> x \<le> z))"
+proof -
+ have "\<exists>x. isLub UNIV S x"
+ by (rule reals_complete)
+ (auto simp add: isLub_def isUb_def leastP_def setle_def setge_def prems)
+ thus ?thesis
+ by (metis UNIV_I isLub_isUb isLub_le_isUb isUbD isUb_def setleI)
+qed
+
subsection {* The Archimedean Property of the Reals *}
--- a/src/HOL/SEQ.thy Wed Sep 23 11:06:32 2009 +0100
+++ b/src/HOL/SEQ.thy Fri Sep 25 13:47:28 2009 +0100
@@ -500,6 +500,28 @@
apply (drule LIMSEQ_minus, auto)
done
+lemma lim_le:
+ fixes x :: real
+ assumes f: "convergent f" and fn_le: "!!n. f n \<le> x"
+ shows "lim f \<le> x"
+proof (rule classical)
+ assume "\<not> lim f \<le> x"
+ hence 0: "0 < lim f - x" by arith
+ have 1: "f----> lim f"
+ by (metis convergent_LIMSEQ_iff f)
+ thus ?thesis
+ proof (simp add: LIMSEQ_iff)
+ assume "\<forall>r>0. \<exists>no. \<forall>n\<ge>no. \<bar>f n - lim f\<bar> < r"
+ hence "\<exists>no. \<forall>n\<ge>no. \<bar>f n - lim f\<bar> < lim f - x"
+ by (metis 0)
+ from this obtain no where "\<forall>n\<ge>no. \<bar>f n - lim f\<bar> < lim f - x"
+ by blast
+ thus "lim f \<le> x"
+ by (metis add_cancel_end add_minus_cancel diff_def linorder_linear
+ linorder_not_le minus_diff_eq abs_diff_less_iff fn_le)
+ qed
+qed
+
text{* Given a binary function @{text "f:: nat \<Rightarrow> 'a \<Rightarrow> 'a"}, its values are uniquely determined by a function g *}
lemma nat_function_unique: "EX! g. g 0 = e \<and> (\<forall>n. g (Suc n) = f n (g n))"
@@ -1082,10 +1104,6 @@
lemma isUb_UNIV_I: "(\<And>y. y \<in> S \<Longrightarrow> y \<le> u) \<Longrightarrow> isUb UNIV S u"
by (simp add: isUbI setleI)
-lemma real_abs_diff_less_iff:
- "(\<bar>x - a\<bar> < (r::real)) = (a - r < x \<and> x < a + r)"
-by auto
-
locale real_Cauchy =
fixes X :: "nat \<Rightarrow> real"
assumes X: "Cauchy X"
@@ -1122,13 +1140,13 @@
show "\<exists>x. x \<in> S"
proof
from N have "\<forall>n\<ge>N. X N - 1 < X n"
- by (simp add: real_abs_diff_less_iff)
+ by (simp add: abs_diff_less_iff)
thus "X N - 1 \<in> S" by (rule mem_S)
qed
show "\<exists>u. isUb UNIV S u"
proof
from N have "\<forall>n\<ge>N. X n < X N + 1"
- by (simp add: real_abs_diff_less_iff)
+ by (simp add: abs_diff_less_iff)
thus "isUb UNIV S (X N + 1)"
by (rule bound_isUb)
qed
@@ -1144,7 +1162,7 @@
using CauchyD [OF X r] by auto
hence "\<forall>n\<ge>N. norm (X n - X N) < r/2" by simp
hence N: "\<forall>n\<ge>N. X N - r/2 < X n \<and> X n < X N + r/2"
- by (simp only: real_norm_def real_abs_diff_less_iff)
+ by (simp only: real_norm_def abs_diff_less_iff)
from N have "\<forall>n\<ge>N. X N - r/2 < X n" by fast
hence "X N - r/2 \<in> S" by (rule mem_S)
@@ -1159,7 +1177,7 @@
fix n assume n: "N \<le> n"
from N n have "X n < X N + r/2" and "X N - r/2 < X n" by simp+
thus "norm (X n - x) < r" using 1 2
- by (simp add: real_abs_diff_less_iff)
+ by (simp add: abs_diff_less_iff)
qed
qed
--- a/src/HOL/Series.thy Wed Sep 23 11:06:32 2009 +0100
+++ b/src/HOL/Series.thy Fri Sep 25 13:47:28 2009 +0100
@@ -104,6 +104,9 @@
"summable f ==> (%n. setsum f {0..<n}) ----> (suminf f)"
by (rule summable_sums [unfolded sums_def])
+lemma suminf_eq_lim: "suminf f = lim (%n. setsum f {0..<n})"
+ by (simp add: suminf_def sums_def lim_def)
+
(*-------------------
sum is unique
------------------*)
@@ -112,6 +115,9 @@
apply (auto intro!: LIMSEQ_unique simp add: sums_def)
done
+lemma sums_iff: "f sums x \<longleftrightarrow> summable f \<and> (suminf f = x)"
+ by (metis summable_sums sums_summable sums_unique)
+
lemma sums_split_initial_segment: "f sums s ==>
(%n. f(n + k)) sums (s - (SUM i = 0..< k. f i))"
apply (unfold sums_def);
@@ -368,6 +374,11 @@
apply (drule_tac x="n" in spec, simp)
done
+lemma suminf_le:
+ fixes x :: real
+ shows "summable f \<Longrightarrow> (!!n. setsum f {0..<n} \<le> x) \<Longrightarrow> suminf f \<le> x"
+ by (simp add: summable_convergent_sumr_iff suminf_eq_lim lim_le)
+
lemma summable_Cauchy:
"summable (f::nat \<Rightarrow> 'a::banach) =
(\<forall>e > 0. \<exists>N. \<forall>m \<ge> N. \<forall>n. norm (setsum f {m..<n}) < e)"