--- a/src/HOL/Limits.thy Thu Jan 31 11:31:22 2013 +0100
+++ b/src/HOL/Limits.thy Thu Jan 31 11:31:27 2013 +0100
@@ -469,6 +469,12 @@
apply (erule le_less_trans [OF dist_triangle])
done
+lemma eventually_nhds_order:
+ "eventually P (nhds (a::'a::linorder_topology)) \<longleftrightarrow>
+ (\<exists>S. open_interval S \<and> a \<in> S \<and> (\<forall>z\<in>S. P z))"
+ (is "_ \<longleftrightarrow> ?rhs")
+ unfolding eventually_nhds by (auto dest!: open_orderD dest: open_interval_imp_open)
+
lemma nhds_neq_bot [simp]: "nhds a \<noteq> bot"
unfolding trivial_limit_def eventually_nhds by simp
@@ -901,6 +907,36 @@
using le_less_trans by (rule eventually_elim2)
qed
+lemma increasing_tendsto:
+ fixes f :: "_ \<Rightarrow> 'a::linorder_topology"
+ assumes bdd: "eventually (\<lambda>n. f n \<le> l) F"
+ and en: "\<And>x. x < l \<Longrightarrow> eventually (\<lambda>n. x < f n) F"
+ shows "(f ---> l) F"
+proof (rule topological_tendstoI)
+ fix S assume "open S" "l \<in> S"
+ then show "eventually (\<lambda>x. f x \<in> S) F"
+ proof (induct rule: open_order_induct)
+ case (greaterThanLessThan a b) with en bdd show ?case
+ by (auto elim!: eventually_elim2)
+ qed (insert en bdd, auto elim!: eventually_elim1)
+qed
+
+lemma decreasing_tendsto:
+ fixes f :: "_ \<Rightarrow> 'a::linorder_topology"
+ assumes bdd: "eventually (\<lambda>n. l \<le> f n) F"
+ and en: "\<And>x. l < x \<Longrightarrow> eventually (\<lambda>n. f n < x) F"
+ shows "(f ---> l) F"
+proof (rule topological_tendstoI)
+ fix S assume "open S" "l \<in> S"
+ then show "eventually (\<lambda>x. f x \<in> S) F"
+ proof (induct rule: open_order_induct)
+ case (greaterThanLessThan a b)
+ with en have "eventually (\<lambda>n. f n < b) F" by auto
+ with bdd show ?case
+ by eventually_elim (insert greaterThanLessThan, auto)
+ qed (insert en bdd, auto elim!: eventually_elim1)
+qed
+
subsubsection {* Distance and norms *}
lemma tendsto_dist [tendsto_intros]:
@@ -1002,22 +1038,25 @@
by (simp add: tendsto_const)
qed
-lemma real_tendsto_sandwich:
- fixes f g h :: "'a \<Rightarrow> real"
+lemma tendsto_sandwich:
+ fixes f g h :: "'a \<Rightarrow> 'b::linorder_topology"
assumes ev: "eventually (\<lambda>n. f n \<le> g n) net" "eventually (\<lambda>n. g n \<le> h n) net"
assumes lim: "(f ---> c) net" "(h ---> c) net"
shows "(g ---> c) net"
-proof -
- have "((\<lambda>n. g n - f n) ---> 0) net"
- proof (rule metric_tendsto_imp_tendsto)
- show "eventually (\<lambda>n. dist (g n - f n) 0 \<le> dist (h n - f n) 0) net"
- using ev by (rule eventually_elim2) (simp add: dist_real_def)
- show "((\<lambda>n. h n - f n) ---> 0) net"
- using tendsto_diff[OF lim(2,1)] by simp
- qed
- from tendsto_add[OF this lim(1)] show ?thesis by simp
+proof (rule topological_tendstoI)
+ fix S assume "open S" "c \<in> S"
+ from open_orderD[OF this] obtain T where "open_interval T" "c \<in> T" "T \<subseteq> S" by auto
+ with lim[THEN topological_tendstoD, of T]
+ have "eventually (\<lambda>x. f x \<in> T) net" "eventually (\<lambda>x. h x \<in> T) net"
+ by (auto dest: open_interval_imp_open)
+ with ev have "eventually (\<lambda>x. g x \<in> T) net"
+ by eventually_elim (insert `open_interval T`, auto dest: open_intervalD)
+ with `T \<subseteq> S` show "eventually (\<lambda>x. g x \<in> S) net"
+ by (auto elim: eventually_elim1)
qed
+lemmas real_tendsto_sandwich = tendsto_sandwich[where 'b=real]
+
subsubsection {* Linear operators and multiplication *}
lemma (in bounded_linear) tendsto:
@@ -1082,29 +1121,33 @@
by (simp add: tendsto_const)
qed
-lemma tendsto_le_const:
- fixes f :: "_ \<Rightarrow> real"
+lemma tendsto_le:
+ fixes f g :: "'a \<Rightarrow> 'b::linorder_topology"
assumes F: "\<not> trivial_limit F"
- assumes x: "(f ---> x) F" and a: "eventually (\<lambda>x. a \<le> f x) F"
- shows "a \<le> x"
+ assumes x: "(f ---> x) F" and y: "(g ---> y) F"
+ assumes ev: "eventually (\<lambda>x. g x \<le> f x) F"
+ shows "y \<le> x"
proof (rule ccontr)
- assume "\<not> a \<le> x"
- with x have "eventually (\<lambda>x. f x < a) F"
- by (auto simp add: tendsto_def elim!: allE[of _ "{..< a}"])
- with a have "eventually (\<lambda>x. False) F"
- by eventually_elim auto
+ assume "\<not> y \<le> x"
+ then have "x < y" by simp
+ from less_separate[OF this] obtain a b where xy: "x \<in> {..<a}" "y \<in> {b <..}" "{..<a} \<inter> {b<..} = {}"
+ by auto
+ then have less: "\<And>x y. x < a \<Longrightarrow> b < y \<Longrightarrow> x < y"
+ by auto
+ from x[THEN topological_tendstoD, of "{..<a}"] y[THEN topological_tendstoD, of "{b <..}"] xy
+ have "eventually (\<lambda>x. f x \<in> {..<a}) F" "eventually (\<lambda>x. g x \<in> {b <..}) F" by auto
+ with ev have "eventually (\<lambda>x. False) F"
+ by eventually_elim (auto dest!: less)
with F show False
by (simp add: eventually_False)
qed
-lemma tendsto_le:
- fixes f g :: "_ \<Rightarrow> real"
+lemma tendsto_le_const:
+ fixes f :: "'a \<Rightarrow> 'b::linorder_topology"
assumes F: "\<not> trivial_limit F"
- assumes x: "(f ---> x) F" and y: "(g ---> y) F"
- assumes ev: "eventually (\<lambda>x. g x \<le> f x) F"
- shows "y \<le> x"
- using tendsto_le_const[OF F tendsto_diff[OF x y], of 0] ev
- by (simp add: sign_simps)
+ assumes x: "(f ---> x) F" and a: "eventually (\<lambda>x. a \<le> f x) F"
+ shows "a \<le> x"
+ using F x tendsto_const a by (rule tendsto_le)
subsubsection {* Inverse and division *}
--- a/src/HOL/RealVector.thy Thu Jan 31 11:31:22 2013 +0100
+++ b/src/HOL/RealVector.thy Thu Jan 31 11:31:27 2013 +0100
@@ -508,6 +508,110 @@
end
+inductive generate_topology for S where
+ UNIV: "generate_topology S UNIV"
+| Int: "generate_topology S a \<Longrightarrow> generate_topology S b \<Longrightarrow> generate_topology S (a \<inter> b)"
+| UN: "(\<And>k. k \<in> K \<Longrightarrow> generate_topology S k) \<Longrightarrow> generate_topology S (\<Union>K)"
+| Basis: "s \<in> S \<Longrightarrow> generate_topology S s"
+
+hide_fact (open) UNIV Int UN Basis
+
+lemma generate_topology_Union:
+ "(\<And>k. k \<in> I \<Longrightarrow> generate_topology S (K k)) \<Longrightarrow> generate_topology S (\<Union>k\<in>I. K k)"
+ unfolding SUP_def by (intro generate_topology.UN) auto
+
+lemma topological_space_generate_topology:
+ "class.topological_space (generate_topology S)"
+ by default (auto intro: generate_topology.intros)
+
+class order_topology = order + "open" +
+ assumes open_generated_order: "open = generate_topology (range (\<lambda>a. {..< a}) \<union> range (\<lambda>a. {a <..}))"
+begin
+
+subclass topological_space
+ unfolding open_generated_order
+ by (rule topological_space_generate_topology)
+
+lemma open_greaterThan [simp]: "open {a <..}"
+ unfolding open_generated_order by (auto intro: generate_topology.Basis)
+
+lemma open_lessThan [simp]: "open {..< a}"
+ unfolding open_generated_order by (auto intro: generate_topology.Basis)
+
+lemma open_greaterThanLessThan [simp]: "open {a <..< b}"
+ unfolding greaterThanLessThan_eq by (simp add: open_Int)
+
+end
+
+class linorder_topology = linorder + order_topology
+
+lemma closed_atMost [simp]: "closed {.. a::'a::linorder_topology}"
+ by (simp add: closed_open)
+
+lemma closed_atLeast [simp]: "closed {a::'a::linorder_topology ..}"
+ by (simp add: closed_open)
+
+lemma closed_atLeastAtMost [simp]: "closed {a::'a::linorder_topology .. b}"
+proof -
+ have "{a .. b} = {a ..} \<inter> {.. b}"
+ by auto
+ then show ?thesis
+ by (simp add: closed_Int)
+qed
+
+inductive open_interval :: "'a::order set \<Rightarrow> bool" where
+ empty[intro]: "open_interval {}" |
+ UNIV[intro]: "open_interval UNIV" |
+ greaterThan[intro]: "open_interval {a <..}" |
+ lessThan[intro]: "open_interval {..< b}" |
+ greaterThanLessThan[intro]: "open_interval {a <..< b}"
+hide_fact (open) empty UNIV greaterThan lessThan greaterThanLessThan
+
+lemma open_intervalD:
+ "open_interval S \<Longrightarrow> x \<in> S \<Longrightarrow> y \<in> S \<Longrightarrow> x \<le> z \<Longrightarrow> z \<le> y \<Longrightarrow> z \<in> S"
+ by (cases rule: open_interval.cases) auto
+
+lemma open_interval_Int[intro]:
+ fixes S T :: "'a :: linorder set"
+ assumes S: "open_interval S" and T: "open_interval T"
+ shows "open_interval (S \<inter> T)"
+proof -
+ { fix a b :: 'a have "{..<b} \<inter> {a<..} = { a <..} \<inter> {..< b }" by auto } note this[simp]
+ { fix a b :: 'a and A have "{a <..} \<inter> ({b <..} \<inter> A) = {max a b <..} \<inter> A" by auto } note this[simp]
+ { fix a b :: 'a and A have "{..<b} \<inter> (A \<inter> {..<a}) = A \<inter> {..<min a b}" by auto } note this[simp]
+ { fix a b :: 'a have "open_interval ({ a <..} \<inter> {..< b})"
+ unfolding greaterThanLessThan_eq[symmetric] by auto } note this[simp]
+ show ?thesis
+ by (cases rule: open_interval.cases[OF S, case_product open_interval.cases[OF T]])
+ (auto simp: greaterThanLessThan_eq lessThan_Int_lessThan greaterThan_Int_greaterThan Int_assoc)
+qed
+
+lemma open_interval_imp_open: "open_interval S \<Longrightarrow> open (S::'a::order_topology set)"
+ by (cases S rule: open_interval.cases) auto
+
+lemma open_orderD:
+ "open (S::'a::linorder_topology set) \<Longrightarrow> x \<in> S \<Longrightarrow> \<exists>T. open_interval T \<and> T \<subseteq> S \<and> x \<in> T"
+ unfolding open_generated_order
+proof (induct rule: generate_topology.induct)
+ case (UN K) then obtain k where "k \<in> K" "x \<in> k" by auto
+ with UN(2)[of k] show ?case by auto
+qed auto
+
+lemma open_order_induct[consumes 2, case_names subset UNIV lessThan greaterThan greaterThanLessThan]:
+ fixes S :: "'a::linorder_topology set"
+ assumes S: "open S" "x \<in> S"
+ assumes subset: "\<And>S T. P S \<Longrightarrow> S \<subseteq> T \<Longrightarrow> P T"
+ assumes univ: "P UNIV"
+ assumes lt: "\<And>a. x < a \<Longrightarrow> P {..< a}"
+ assumes gt: "\<And>a. a < x \<Longrightarrow> P {a <..}"
+ assumes lgt: "\<And>a b. a < x \<Longrightarrow> x < b \<Longrightarrow> P {a <..< b}"
+ shows "P S"
+proof -
+ from open_orderD[OF S] obtain T where "open_interval T" "T \<subseteq> S" "x \<in> T"
+ by auto
+ then show "P S"
+ by induct (auto intro: univ subset lt gt lgt)
+qed
subsection {* Metric spaces *}
@@ -859,46 +963,46 @@
end
-lemma open_real_lessThan [simp]:
- fixes a :: real shows "open {..<a}"
-unfolding open_real_def dist_real_def
-proof (clarify)
- fix x assume "x < a"
- hence "0 < a - x \<and> (\<forall>y. \<bar>y - x\<bar> < a - x \<longrightarrow> y \<in> {..<a})" by auto
- thus "\<exists>e>0. \<forall>y. \<bar>y - x\<bar> < e \<longrightarrow> y \<in> {..<a}" ..
-qed
-
-lemma open_real_greaterThan [simp]:
- fixes a :: real shows "open {a<..}"
-unfolding open_real_def dist_real_def
-proof (clarify)
- fix x assume "a < x"
- hence "0 < x - a \<and> (\<forall>y. \<bar>y - x\<bar> < x - a \<longrightarrow> y \<in> {a<..})" by auto
- thus "\<exists>e>0. \<forall>y. \<bar>y - x\<bar> < e \<longrightarrow> y \<in> {a<..}" ..
+instance real :: linorder_topology
+proof
+ show "(open :: real set \<Rightarrow> bool) = generate_topology (range lessThan \<union> range greaterThan)"
+ proof (rule ext, safe)
+ fix S :: "real set" assume "open S"
+ then guess f unfolding open_real_def bchoice_iff ..
+ then have *: "S = (\<Union>x\<in>S. {x - f x <..} \<inter> {..< x + f x})"
+ by (fastforce simp: dist_real_def)
+ show "generate_topology (range lessThan \<union> range greaterThan) S"
+ apply (subst *)
+ apply (intro generate_topology_Union generate_topology.Int)
+ apply (auto intro: generate_topology.Basis)
+ done
+ next
+ fix S :: "real set" assume "generate_topology (range lessThan \<union> range greaterThan) S"
+ moreover have "\<And>a::real. open {..<a}"
+ unfolding open_real_def dist_real_def
+ proof clarify
+ fix x a :: real assume "x < a"
+ hence "0 < a - x \<and> (\<forall>y. \<bar>y - x\<bar> < a - x \<longrightarrow> y \<in> {..<a})" by auto
+ thus "\<exists>e>0. \<forall>y. \<bar>y - x\<bar> < e \<longrightarrow> y \<in> {..<a}" ..
+ qed
+ moreover have "\<And>a::real. open {a <..}"
+ unfolding open_real_def dist_real_def
+ proof clarify
+ fix x a :: real assume "a < x"
+ hence "0 < x - a \<and> (\<forall>y. \<bar>y - x\<bar> < x - a \<longrightarrow> y \<in> {a<..})" by auto
+ thus "\<exists>e>0. \<forall>y. \<bar>y - x\<bar> < e \<longrightarrow> y \<in> {a<..}" ..
+ qed
+ ultimately show "open S"
+ by induct auto
+ qed
qed
-lemma open_real_greaterThanLessThan [simp]:
- fixes a b :: real shows "open {a<..<b}"
-proof -
- have "{a<..<b} = {a<..} \<inter> {..<b}" by auto
- thus "open {a<..<b}" by (simp add: open_Int)
-qed
-
-lemma closed_real_atMost [simp]:
- fixes a :: real shows "closed {..a}"
-unfolding closed_open by simp
-
-lemma closed_real_atLeast [simp]:
- fixes a :: real shows "closed {a..}"
-unfolding closed_open by simp
-
-lemma closed_real_atLeastAtMost [simp]:
- fixes a b :: real shows "closed {a..b}"
-proof -
- have "{a..b} = {a..} \<inter> {..b}" by auto
- thus "closed {a..b}" by (simp add: closed_Int)
-qed
-
+lemmas open_real_greaterThan = open_greaterThan[where 'a=real]
+lemmas open_real_lessThan = open_lessThan[where 'a=real]
+lemmas open_real_greaterThanLessThan = open_greaterThanLessThan[where 'a=real]
+lemmas closed_real_atMost = closed_atMost[where 'a=real]
+lemmas closed_real_atLeast = closed_atLeast[where 'a=real]
+lemmas closed_real_atLeastAtMost = closed_atLeastAtMost[where 'a=real]
subsection {* Extra type constraints *}
@@ -1172,6 +1276,30 @@
instance t2_space \<subseteq> t1_space
proof qed (fast dest: hausdorff)
+lemma (in linorder) less_separate:
+ assumes "x < y"
+ shows "\<exists>a b. x \<in> {..< a} \<and> y \<in> {b <..} \<and> {..< a} \<inter> {b <..} = {}"
+proof cases
+ assume "\<exists>z. x < z \<and> z < y"
+ then guess z ..
+ then have "x \<in> {..< z} \<and> y \<in> {z <..} \<and> {z <..} \<inter> {..< z} = {}"
+ by auto
+ then show ?thesis by blast
+next
+ assume "\<not> (\<exists>z. x < z \<and> z < y)"
+ with `x < y` have "x \<in> {..< y} \<and> y \<in> {x <..} \<and> {x <..} \<inter> {..< y} = {}"
+ by auto
+ then show ?thesis by blast
+qed
+
+instance linorder_topology \<subseteq> t2_space
+proof
+ fix x y :: 'a
+ from less_separate[of x y] less_separate[of y x]
+ show "x \<noteq> y \<Longrightarrow> \<exists>U V. open U \<and> open V \<and> x \<in> U \<and> y \<in> V \<and> U \<inter> V = {}"
+ by (elim neqE) (metis open_lessThan open_greaterThan Int_commute)+
+qed
+
instance metric_space \<subseteq> t2_space
proof
fix x y :: "'a::metric_space"
--- a/src/HOL/SEQ.thy Thu Jan 31 11:31:22 2013 +0100
+++ b/src/HOL/SEQ.thy Thu Jan 31 11:31:27 2013 +0100
@@ -368,19 +368,16 @@
and bdd: "\<And>n. f n \<le> l"
and en: "\<And>e. 0 < e \<Longrightarrow> \<exists>n. l \<le> f n + e"
shows "f ----> l"
- unfolding LIMSEQ_def
-proof safe
- fix r :: real assume "0 < r"
- with bdd en[of "r / 2"] obtain n where n: "dist (f n) l \<le> r / 2"
- by (auto simp add: field_simps dist_real_def)
- { fix N assume "n \<le> N"
- then have "dist (f N) l \<le> dist (f n) l"
- using incseq_SucI[of f] inc bdd by (auto dest!: incseqD simp: dist_real_def)
- then have "dist (f N) l < r"
- using `0 < r` n by simp }
- with `0 < r` show "\<exists>no. \<forall>n\<ge>no. dist (f n) l < r"
- by (auto simp add: LIMSEQ_def field_simps intro!: exI[of _ n])
-qed
+proof (rule increasing_tendsto)
+ fix x assume "x < l"
+ with dense[of 0 "l - x"] obtain e where "0 < e" "e < l - x"
+ by auto
+ from en[OF `0 < e`] obtain n where "l - e \<le> f n"
+ by (auto simp: field_simps)
+ with `e < l - x` `0 < e` have "x < f n" by simp
+ with incseq_SucI[of f, OF inc] show "eventually (\<lambda>n. x < f n) sequentially"
+ by (auto simp: eventually_sequentially incseq_def intro: less_le_trans)
+qed (insert bdd, auto)
lemma Bseq_inverse_lemma:
fixes x :: "'a::real_normed_div_algebra"
@@ -437,15 +434,15 @@
by auto
lemma LIMSEQ_le_const:
- "\<lbrakk>X ----> (x::real); \<exists>N. \<forall>n\<ge>N. a \<le> X n\<rbrakk> \<Longrightarrow> a \<le> x"
+ "\<lbrakk>X ----> (x::'a::linorder_topology); \<exists>N. \<forall>n\<ge>N. a \<le> X n\<rbrakk> \<Longrightarrow> a \<le> x"
using tendsto_le_const[of sequentially X x a] by (simp add: eventually_sequentially)
lemma LIMSEQ_le:
- "\<lbrakk>X ----> x; Y ----> y; \<exists>N. \<forall>n\<ge>N. X n \<le> Y n\<rbrakk> \<Longrightarrow> x \<le> (y::real)"
+ "\<lbrakk>X ----> x; Y ----> y; \<exists>N. \<forall>n\<ge>N. X n \<le> Y n\<rbrakk> \<Longrightarrow> x \<le> (y::'a::linorder_topology)"
using tendsto_le[of sequentially Y y X x] by (simp add: eventually_sequentially)
lemma LIMSEQ_le_const2:
- "\<lbrakk>X ----> (x::real); \<exists>N. \<forall>n\<ge>N. X n \<le> a\<rbrakk> \<Longrightarrow> x \<le> a"
+ "\<lbrakk>X ----> (x::'a::linorder_topology); \<exists>N. \<forall>n\<ge>N. X n \<le> a\<rbrakk> \<Longrightarrow> x \<le> a"
by (rule LIMSEQ_le[of X x "\<lambda>n. a"]) (auto simp: tendsto_const)
subsection {* Convergence *}
--- a/src/HOL/Series.thy Thu Jan 31 11:31:22 2013 +0100
+++ b/src/HOL/Series.thy Thu Jan 31 11:31:27 2013 +0100
@@ -367,7 +367,7 @@
lemma pos_summable:
fixes f:: "nat \<Rightarrow> real"
- assumes pos: "!!n. 0 \<le> f n" and le: "!!n. setsum f {0..<n} \<le> x"
+ assumes pos: "\<And>n. 0 \<le> f n" and le: "\<And>n. setsum f {0..<n} \<le> x"
shows "summable f"
proof -
have "convergent (\<lambda>n. setsum f {0..<n})"
@@ -386,35 +386,65 @@
qed
lemma series_pos_le:
- fixes f :: "nat \<Rightarrow> real"
+ fixes f :: "nat \<Rightarrow> 'a::{ordered_comm_monoid_add, linorder_topology}"
shows "\<lbrakk>summable f; \<forall>m\<ge>n. 0 \<le> f m\<rbrakk> \<Longrightarrow> setsum f {0..<n} \<le> suminf f"
-apply (drule summable_sums)
-apply (simp add: sums_def)
-apply (cut_tac k = "setsum f {0..<n}" in tendsto_const)
-apply (erule LIMSEQ_le, blast)
-apply (rule_tac x="n" in exI, clarify)
-apply (rule setsum_mono2)
-apply auto
-done
+ apply (drule summable_sums)
+ apply (simp add: sums_def)
+ apply (rule LIMSEQ_le_const)
+ apply assumption
+ apply (intro exI[of _ n])
+ apply (auto intro!: setsum_mono2)
+ done
lemma series_pos_less:
- fixes f :: "nat \<Rightarrow> real"
+ fixes f :: "nat \<Rightarrow> 'a::{ordered_ab_semigroup_add_imp_le, ordered_comm_monoid_add, linorder_topology}"
shows "\<lbrakk>summable f; \<forall>m\<ge>n. 0 < f m\<rbrakk> \<Longrightarrow> setsum f {0..<n} < suminf f"
-apply (rule_tac y="setsum f {0..<Suc n}" in order_less_le_trans)
-apply simp
-apply (erule series_pos_le)
-apply (simp add: order_less_imp_le)
-done
+ apply (rule_tac y="setsum f {0..<Suc n}" in order_less_le_trans)
+ using add_less_cancel_left [of "setsum f {0..<n}" 0 "f n"]
+ apply simp
+ apply (erule series_pos_le)
+ apply (simp add: order_less_imp_le)
+ done
+
+lemma suminf_eq_zero_iff:
+ fixes f :: "nat \<Rightarrow> 'a::{ordered_comm_monoid_add, linorder_topology}"
+ shows "\<lbrakk>summable f; \<forall>n. 0 \<le> f n\<rbrakk> \<Longrightarrow> suminf f = 0 \<longleftrightarrow> (\<forall>n. f n = 0)"
+proof
+ assume "summable f" "suminf f = 0" and pos: "\<forall>n. 0 \<le> f n"
+ then have "f sums 0"
+ by (simp add: sums_iff)
+ then have f: "(\<lambda>n. \<Sum>i<n. f i) ----> 0"
+ by (simp add: sums_def atLeast0LessThan)
+ have "\<And>i. (\<Sum>n\<in>{i}. f n) \<le> 0"
+ proof (rule LIMSEQ_le_const[OF f])
+ fix i show "\<exists>N. \<forall>n\<ge>N. (\<Sum>n\<in>{i}. f n) \<le> setsum f {..<n}"
+ using pos by (intro exI[of _ "Suc i"] allI impI setsum_mono2) auto
+ qed
+ with pos show "\<forall>n. f n = 0"
+ by (auto intro!: antisym)
+next
+ assume "\<forall>n. f n = 0"
+ then have "f = (\<lambda>n. 0)"
+ by auto
+ then show "suminf f = 0"
+ by simp
+qed
+
+lemma suminf_gt_zero_iff:
+ fixes f :: "nat \<Rightarrow> 'a::{ordered_comm_monoid_add, linorder_topology}"
+ shows "\<lbrakk>summable f; \<forall>n. 0 \<le> f n\<rbrakk> \<Longrightarrow> 0 < suminf f \<longleftrightarrow> (\<exists>i. 0 < f i)"
+ using series_pos_le[of f 0] suminf_eq_zero_iff[of f]
+ by (simp add: less_le)
lemma suminf_gt_zero:
- fixes f :: "nat \<Rightarrow> real"
+ fixes f :: "nat \<Rightarrow> 'a::{ordered_comm_monoid_add, linorder_topology}"
shows "\<lbrakk>summable f; \<forall>n. 0 < f n\<rbrakk> \<Longrightarrow> 0 < suminf f"
-by (drule_tac n="0" in series_pos_less, simp_all)
+ using suminf_gt_zero_iff[of f] by (simp add: less_imp_le)
lemma suminf_ge_zero:
- fixes f :: "nat \<Rightarrow> real"
+ fixes f :: "nat \<Rightarrow> 'a::{ordered_comm_monoid_add, linorder_topology}"
shows "\<lbrakk>summable f; \<forall>n. 0 \<le> f n\<rbrakk> \<Longrightarrow> 0 \<le> suminf f"
-by (drule_tac n="0" in series_pos_le, simp_all)
+ by (drule_tac n="0" in series_pos_le, simp_all)
lemma sumr_pos_lt_pair:
fixes f :: "nat \<Rightarrow> real"
@@ -493,9 +523,14 @@
done
lemma suminf_le:
- fixes x :: real
+ fixes x :: "'a :: {ordered_comm_monoid_add, linorder_topology}"
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)
+ apply (drule summable_sums)
+ apply (simp add: sums_def)
+ apply (rule LIMSEQ_le_const2)
+ apply assumption
+ apply auto
+ done
lemma summable_Cauchy:
"summable (f::nat \<Rightarrow> 'a::banach) =
@@ -575,7 +610,7 @@
text{*Limit comparison property for series (c.f. jrh)*}
lemma summable_le:
- fixes f g :: "nat \<Rightarrow> real"
+ fixes f g :: "nat \<Rightarrow> 'a::{ordered_comm_monoid_add, linorder_topology}"
shows "\<lbrakk>\<forall>n. f n \<le> g n; summable f; summable g\<rbrakk> \<Longrightarrow> suminf f \<le> suminf g"
apply (drule summable_sums)+
apply (simp only: sums_def, erule (1) LIMSEQ_le)
@@ -597,15 +632,7 @@
fixes f::"nat\<Rightarrow>real"
assumes gt0: "\<forall>n. 0 \<le> f n" and sm: "summable f"
shows "0 \<le> suminf f"
-proof -
- let ?g = "(\<lambda>n. (0::real))"
- from gt0 have "\<forall>n. ?g n \<le> f n" by simp
- moreover have "summable ?g" by (rule summable_zero)
- moreover from sm have "summable f" .
- ultimately have "suminf ?g \<le> suminf f" by (rule summable_le)
- then show "0 \<le> suminf f" by simp
-qed
-
+ using suminf_ge_zero[OF sm gt0] by simp
text{*Absolute convergence imples normal convergence*}
lemma summable_norm_cancel:
--- a/src/HOL/Set_Interval.thy Thu Jan 31 11:31:22 2013 +0100
+++ b/src/HOL/Set_Interval.thy Thu Jan 31 11:31:27 2013 +0100
@@ -117,6 +117,11 @@
lemma atMost_Int_atLeast: "!!n:: 'a::order. atMost n Int atLeast n = {n}"
by (blast intro: order_antisym)
+lemma (in linorder) lessThan_Int_lessThan: "{ a <..} \<inter> { b <..} = { max a b <..}"
+ by auto
+
+lemma (in linorder) greaterThan_Int_greaterThan: "{..< a} \<inter> {..< b} = {..< min a b}"
+ by auto
subsection {* Logical Equivalences for Set Inclusion and Equality *}
@@ -190,6 +195,9 @@
breaks many proofs. Since it only helps blast, it is better to leave well
alone *}
+lemma greaterThanLessThan_eq: "{ a <..< b} = { a <..} \<inter> {..< b }"
+ by auto
+
end
subsubsection{* Emptyness, singletons, subset *}