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 *}