# HG changeset patch
# User hoelzl
# Date 1359628287 -3600
# Node ID 3de230ed05479067f5aff0347228a4c6324a7304
# Parent  501200635659a5c40d23013881270256310d44c4
introduce order topology

diff -r 501200635659 -r 3de230ed0547 src/HOL/Limits.thy
--- 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 *}
 
diff -r 501200635659 -r 3de230ed0547 src/HOL/RealVector.thy
--- 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"
diff -r 501200635659 -r 3de230ed0547 src/HOL/SEQ.thy
--- 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 *}
diff -r 501200635659 -r 3de230ed0547 src/HOL/Series.thy
--- 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:
diff -r 501200635659 -r 3de230ed0547 src/HOL/Set_Interval.thy
--- 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 *}