# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1530202480 -3600
# Node ID f8b98d31ad4535d4a550c597d9c0e677c94ec646
# Parent  d31e986fbebce4754e9e7d75ceb306cea7e7b096
Incorporating new/strengthened proofs from Library and AFP entries

diff -r d31e986fbebc -r f8b98d31ad45 CONTRIBUTORS
--- a/CONTRIBUTORS	Thu Jun 28 14:14:05 2018 +0100
+++ b/CONTRIBUTORS	Thu Jun 28 17:14:40 2018 +0100
@@ -12,6 +12,9 @@
 * June 2018: Martin Baillon and Paulo Emílio de Vilhena
   A variety of contributions to HOL-Algebra.
 
+* June 2018: Wenda Li
+  New/strengthened results involving analysis, topology, etc.
+
 * May 2018: Manuel Eberl
   Landau symbols and asymptotic equivalence (moved from the AFP).
 
diff -r d31e986fbebc -r f8b98d31ad45 src/HOL/Analysis/Cauchy_Integral_Theorem.thy
--- a/src/HOL/Analysis/Cauchy_Integral_Theorem.thy	Thu Jun 28 14:14:05 2018 +0100
+++ b/src/HOL/Analysis/Cauchy_Integral_Theorem.thy	Thu Jun 28 17:14:40 2018 +0100
@@ -774,7 +774,27 @@
   ultimately show ?thesis unfolding valid_path_def piecewise_C1_differentiable_on_def path_def
     using \<open>finite S\<close> by auto
 qed
-
+  
+lemma valid_path_uminus_comp[simp]:
+  fixes g::"real \<Rightarrow> 'a ::real_normed_field"
+  shows "valid_path (uminus \<circ> g) \<longleftrightarrow> valid_path g"
+proof 
+  show "valid_path g \<Longrightarrow> valid_path (uminus \<circ> g)" for g::"real \<Rightarrow> 'a"
+    by (auto intro!: valid_path_compose derivative_intros simp add: deriv_linear[of "-1",simplified])  
+  then show "valid_path g" when "valid_path (uminus \<circ> g)"
+    by (metis fun.map_comp group_add_class.minus_comp_minus id_comp that)
+qed
+
+lemma valid_path_offset[simp]:
+  shows "valid_path (\<lambda>t. g t - z) \<longleftrightarrow> valid_path g"  
+proof 
+  show *: "valid_path (g::real\<Rightarrow>'a) \<Longrightarrow> valid_path (\<lambda>t. g t - z)" for g z
+    unfolding valid_path_def
+    by (fastforce intro:derivative_intros C1_differentiable_imp_piecewise piecewise_C1_differentiable_diff)
+  show "valid_path (\<lambda>t. g t - z) \<Longrightarrow> valid_path g"
+    using *[of "\<lambda>t. g t - z" "-z",simplified] .
+qed
+  
 
 subsection\<open>Contour Integrals along a path\<close>
 
@@ -3554,6 +3574,19 @@
    "(\<And>t. \<lbrakk>0 \<le> t; t \<le> 1\<rbrakk> \<Longrightarrow> p t = q t) \<Longrightarrow> winding_number p z = winding_number q z"
   by (simp add: winding_number_def winding_number_prop_def pathstart_def pathfinish_def)
 
+lemma winding_number_constI:
+  assumes "c\<noteq>z" "\<And>t. \<lbrakk>0\<le>t; t\<le>1\<rbrakk> \<Longrightarrow> g t = c" 
+  shows "winding_number g z = 0"
+proof -
+  have "winding_number g z = winding_number (linepath c c) z"
+    apply (rule winding_number_cong)
+    using assms unfolding linepath_def by auto
+  moreover have "winding_number (linepath c c) z =0"
+    apply (rule winding_number_trivial)
+    using assms by auto
+  ultimately show ?thesis by auto
+qed
+
 lemma winding_number_offset: "winding_number p z = winding_number (\<lambda>w. p w - z) 0"
   unfolding winding_number_def
 proof (intro ext arg_cong [where f = Eps] arg_cong [where f = All] imp_cong refl, safe)
@@ -4812,8 +4845,7 @@
           winding_number (subpath u w g) z"
 apply (rule trans [OF winding_number_join [THEN sym]
                       winding_number_homotopic_paths [OF homotopic_join_subpaths]])
-apply (auto dest: path_image_subpath_subset)
-done
+  using path_image_subpath_subset by auto
 
 
 subsection\<open>Partial circle path\<close>
@@ -4829,6 +4861,11 @@
      "pathfinish(part_circlepath z r s t) = z + r*exp(\<i>*t)"
 by (metis part_circlepath_def pathfinish_def pathfinish_linepath)
 
+lemma reversepath_part_circlepath[simp]:
+    "reversepath (part_circlepath z r s t) = part_circlepath z r t s"
+  unfolding part_circlepath_def reversepath_def linepath_def 
+  by (auto simp:algebra_simps)
+    
 proposition has_vector_derivative_part_circlepath [derivative_intros]:
     "((part_circlepath z r s t) has_vector_derivative
       (\<i> * r * (of_real t - of_real s) * exp(\<i> * linepath s t x)))
diff -r d31e986fbebc -r f8b98d31ad45 src/HOL/Analysis/Change_Of_Vars.thy
--- a/src/HOL/Analysis/Change_Of_Vars.thy	Thu Jun 28 14:14:05 2018 +0100
+++ b/src/HOL/Analysis/Change_Of_Vars.thy	Thu Jun 28 17:14:40 2018 +0100
@@ -2937,7 +2937,7 @@
   moreover have "integral (g ` S) (h n) \<le> integral S (\<lambda>x. ?D x * f (g x))" for n
     using hint by (blast intro: le order_trans)
   ultimately show ?thesis
-    by (auto intro: Lim_bounded_ereal)
+    by (auto intro: Lim_bounded)
 qed
 
 
diff -r d31e986fbebc -r f8b98d31ad45 src/HOL/Analysis/Interval_Integral.thy
--- a/src/HOL/Analysis/Interval_Integral.thy	Thu Jun 28 14:14:05 2018 +0100
+++ b/src/HOL/Analysis/Interval_Integral.thy	Thu Jun 28 17:14:40 2018 +0100
@@ -875,7 +875,7 @@
       using A apply (auto simp: einterval_def tendsto_at_iff_sequentially comp_def)
       by (drule_tac x = "\<lambda>i. ereal (l i)" in spec, auto)
     hence A3: "\<And>i. g (l i) \<ge> A"
-      by (intro decseq_le, auto simp: decseq_def)
+      by (intro decseq_ge, auto simp: decseq_def)
     have B2: "(\<lambda>i. g (u i)) \<longlonglongrightarrow> B"
       using B apply (auto simp: einterval_def tendsto_at_iff_sequentially comp_def)
       by (drule_tac x = "\<lambda>i. ereal (u i)" in spec, auto)
@@ -972,7 +972,7 @@
       using A apply (auto simp: einterval_def tendsto_at_iff_sequentially comp_def)
       by (drule_tac x = "\<lambda>i. ereal (l i)" in spec, auto)
     hence A3: "\<And>i. g (l i) \<ge> A"
-      by (intro decseq_le, auto simp: decseq_def)
+      by (intro decseq_ge, auto simp: decseq_def)
     have B2: "(\<lambda>i. g (u i)) \<longlonglongrightarrow> B"
       using B apply (auto simp: einterval_def tendsto_at_iff_sequentially comp_def)
       by (drule_tac x = "\<lambda>i. ereal (u i)" in spec, auto)
diff -r d31e986fbebc -r f8b98d31ad45 src/HOL/Analysis/Measure_Space.thy
--- a/src/HOL/Analysis/Measure_Space.thy	Thu Jun 28 14:14:05 2018 +0100
+++ b/src/HOL/Analysis/Measure_Space.thy	Thu Jun 28 17:14:40 2018 +0100
@@ -389,7 +389,7 @@
     show "range (\<lambda>i. A i - (\<Inter>i. A i)) \<subseteq> M" "(\<Inter>i. A i - (\<Inter>i. A i)) = {}"
       using A by auto
   qed
-  from INF_Lim_ereal[OF decseq_f this]
+  from INF_Lim[OF decseq_f this]
   have "(INF n. f (A n - (\<Inter>i. A i))) = 0" .
   moreover have "(INF n. f (\<Inter>i. A i)) = f (\<Inter>i. A i)"
     by auto
@@ -2020,7 +2020,7 @@
     finally show ?thesis by simp
   qed
   ultimately have "emeasure M (\<Union>N. B N) \<le> ennreal (\<Sum>n. measure M (A n))"
-    by (simp add: Lim_bounded_ereal)
+    by (simp add: Lim_bounded)
   then show "emeasure M (\<Union>n. A n) \<le> (\<Sum>n. measure M (A n))"
     unfolding B_def by (metis UN_UN_flatten UN_lessThan_UNIV)
   then show "emeasure M (\<Union>n. A n) < \<infinity>"
diff -r d31e986fbebc -r f8b98d31ad45 src/HOL/Analysis/Path_Connected.thy
--- a/src/HOL/Analysis/Path_Connected.thy	Thu Jun 28 14:14:05 2018 +0100
+++ b/src/HOL/Analysis/Path_Connected.thy	Thu Jun 28 17:14:40 2018 +0100
@@ -929,10 +929,10 @@
     done
 
 lemma path_image_subpath_subset:
-    "\<lbrakk>path g; u \<in> {0..1}; v \<in> {0..1}\<rbrakk> \<Longrightarrow> path_image(subpath u v g) \<subseteq> path_image g"
+    "\<lbrakk>u \<in> {0..1}; v \<in> {0..1}\<rbrakk> \<Longrightarrow> path_image(subpath u v g) \<subseteq> path_image g"
   apply (simp add: closed_segment_real_eq image_affinity_atLeastAtMost path_image_subpath)
   apply (auto simp: path_image_def)
-  done
+  done  
 
 lemma join_subpaths_middle: "subpath (0) ((1 / 2)) p +++ subpath ((1 / 2)) 1 p = p"
   by (rule ext) (simp add: joinpaths_def subpath_def divide_simps)
@@ -1751,14 +1751,14 @@
     by (simp add: path_connected_def)
 qed
 
-lemma path_component: "path_component s x y \<longleftrightarrow> (\<exists>t. path_connected t \<and> t \<subseteq> s \<and> x \<in> t \<and> y \<in> t)"
+lemma path_component: "path_component S x y \<longleftrightarrow> (\<exists>t. path_connected t \<and> t \<subseteq> S \<and> x \<in> t \<and> y \<in> t)"
   apply (intro iffI)
   apply (metis path_connected_path_image path_defs(5) pathfinish_in_path_image pathstart_in_path_image)
   using path_component_of_subset path_connected_component by blast
 
 lemma path_component_path_component [simp]:
-   "path_component_set (path_component_set s x) x = path_component_set s x"
-proof (cases "x \<in> s")
+   "path_component_set (path_component_set S x) x = path_component_set S x"
+proof (cases "x \<in> S")
   case True show ?thesis
     apply (rule subset_antisym)
     apply (simp add: path_component_subset)
@@ -1769,11 +1769,11 @@
 qed
 
 lemma path_component_subset_connected_component:
-   "(path_component_set s x) \<subseteq> (connected_component_set s x)"
-proof (cases "x \<in> s")
+   "(path_component_set S x) \<subseteq> (connected_component_set S x)"
+proof (cases "x \<in> S")
   case True show ?thesis
     apply (rule connected_component_maximal)
-    apply (auto simp: True path_component_subset path_component_refl path_connected_imp_connected path_connected_path_component)
+    apply (auto simp: True path_component_subset path_component_refl path_connected_imp_connected)
     done
 next
   case False then show ?thesis
@@ -1784,11 +1784,11 @@
 
 lemma path_connected_linear_image:
   fixes f :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_vector"
-  assumes "path_connected s" "bounded_linear f"
-    shows "path_connected(f ` s)"
+  assumes "path_connected S" "bounded_linear f"
+    shows "path_connected(f ` S)"
 by (auto simp: linear_continuous_on assms path_connected_continuous_image)
 
-lemma is_interval_path_connected: "is_interval s \<Longrightarrow> path_connected s"
+lemma is_interval_path_connected: "is_interval S \<Longrightarrow> path_connected S"
   by (simp add: convex_imp_path_connected is_interval_convex)
 
 lemma linear_homeomorphism_image:
diff -r d31e986fbebc -r f8b98d31ad45 src/HOL/Analysis/Summation_Tests.thy
--- a/src/HOL/Analysis/Summation_Tests.thy	Thu Jun 28 14:14:05 2018 +0100
+++ b/src/HOL/Analysis/Summation_Tests.thy	Thu Jun 28 17:14:40 2018 +0100
@@ -752,7 +752,7 @@
   assumes lim: "(\<lambda>n. ereal (norm (f n) / norm (f (Suc n)))) \<longlonglongrightarrow> c"
   shows   "conv_radius f = c"
 proof (rule conv_radius_eqI')
-  show "c \<ge> 0" by (intro Lim_bounded2_ereal[OF lim]) simp_all
+  show "c \<ge> 0" by (intro Lim_bounded2[OF lim]) simp_all
 next
   fix r assume r: "0 < r" "ereal r < c"
   let ?l = "liminf (\<lambda>n. ereal (norm (f n * of_real r ^ n) / norm (f (Suc n) * of_real r ^ Suc n)))"
diff -r d31e986fbebc -r f8b98d31ad45 src/HOL/Analysis/Topology_Euclidean_Space.thy
--- a/src/HOL/Analysis/Topology_Euclidean_Space.thy	Thu Jun 28 14:14:05 2018 +0100
+++ b/src/HOL/Analysis/Topology_Euclidean_Space.thy	Thu Jun 28 17:14:40 2018 +0100
@@ -2068,32 +2068,45 @@
 lemma islimpt_EMPTY[simp]: "\<not> x islimpt {}"
   by (auto simp: islimpt_def)
 
+lemma finite_ball_include:
+  fixes a :: "'a::metric_space"
+  assumes "finite S" 
+  shows "\<exists>e>0. S \<subseteq> ball a e"
+  using assms
+proof induction
+  case (insert x S)
+  then obtain e0 where "e0>0" and e0:"S \<subseteq> ball a e0" by auto
+  define e where "e = max e0 (2 * dist a x)"
+  have "e>0" unfolding e_def using \<open>e0>0\<close> by auto
+  moreover have "insert x S \<subseteq> ball a e"
+    using e0 \<open>e>0\<close> unfolding e_def by auto
+  ultimately show ?case by auto
+qed (auto intro: zero_less_one)
+
 lemma finite_set_avoid:
   fixes a :: "'a::metric_space"
-  assumes fS: "finite S"
+  assumes "finite S"
   shows "\<exists>d>0. \<forall>x\<in>S. x \<noteq> a \<longrightarrow> d \<le> dist a x"
-proof (induct rule: finite_induct[OF fS])
-  case 1
-  then show ?case by (auto intro: zero_less_one)
-next
-  case (2 x F)
-  from 2 obtain d where d: "d > 0" "\<forall>x\<in>F. x \<noteq> a \<longrightarrow> d \<le> dist a x"
+  using assms
+proof induction
+  case (insert x S)
+  then obtain d where "d > 0" and d: "\<forall>x\<in>S. x \<noteq> a \<longrightarrow> d \<le> dist a x"
     by blast
   show ?case
   proof (cases "x = a")
     case True
-    with d show ?thesis by auto
+    with \<open>d > 0 \<close>d show ?thesis by auto
   next
     case False
     let ?d = "min d (dist a x)"
-    from False d(1) have dp: "?d > 0"
+    from False \<open>d > 0\<close> have dp: "?d > 0"
       by auto
-    from d have d': "\<forall>x\<in>F. x \<noteq> a \<longrightarrow> ?d \<le> dist a x"
+    from d have d': "\<forall>x\<in>S. x \<noteq> a \<longrightarrow> ?d \<le> dist a x"
       by auto
     with dp False show ?thesis
-      by (auto intro!: exI[where x="?d"])
+      by (metis insert_iff le_less min_less_iff_conj not_less)
   qed
-qed
+qed (auto intro: zero_less_one)
 
 lemma islimpt_Un: "x islimpt (S \<union> T) \<longleftrightarrow> x islimpt S \<or> x islimpt T"
   by (simp add: islimpt_iff_eventually eventually_conj_iff)
diff -r d31e986fbebc -r f8b98d31ad45 src/HOL/Computational_Algebra/Polynomial.thy
--- a/src/HOL/Computational_Algebra/Polynomial.thy	Thu Jun 28 14:14:05 2018 +0100
+++ b/src/HOL/Computational_Algebra/Polynomial.thy	Thu Jun 28 17:14:40 2018 +0100
@@ -1832,10 +1832,13 @@
     by simp
 qed
 
-(* Next two lemmas contributed by Wenda Li *)
+(* Next three lemmas contributed by Wenda Li *)
 lemma order_1_eq_0 [simp]:"order x 1 = 0"
   by (metis order_root poly_1 zero_neq_one)
 
+lemma order_uminus[simp]: "order x (-p) = order x p"
+  by (metis neg_equal_0_iff_equal order_smult smult_1_left smult_minus_left) 
+
 lemma order_power_n_n: "order a ([:-a,1:]^n)=n"
 proof (induct n) (*might be proved more concisely using nat_less_induct*)
   case 0
@@ -2575,17 +2578,28 @@
 lemma poly_DERIV [simp]: "DERIV (\<lambda>x. poly p x) x :> poly (pderiv p) x"
   by (induct p) (auto intro!: derivative_eq_intros simp add: pderiv_pCons)
 
+lemma poly_isCont[simp]: 
+  fixes x::"'a::real_normed_field"
+  shows "isCont (\<lambda>x. poly p x) x"
+by (rule poly_DERIV [THEN DERIV_isCont])
+
+lemma tendsto_poly [tendsto_intros]: "(f \<longlongrightarrow> a) F \<Longrightarrow> ((\<lambda>x. poly p (f x)) \<longlongrightarrow> poly p a) F"
+  for f :: "_ \<Rightarrow> 'a::real_normed_field"  
+  by (rule isCont_tendsto_compose [OF poly_isCont])
+
+lemma continuous_within_poly: "continuous (at z within s) (poly p)"
+  for z :: "'a::{real_normed_field}"
+  by (simp add: continuous_within tendsto_poly)  
+    
+lemma continuous_poly [continuous_intros]: "continuous F f \<Longrightarrow> continuous F (\<lambda>x. poly p (f x))"
+  for f :: "_ \<Rightarrow> 'a::real_normed_field"
+  unfolding continuous_def by (rule tendsto_poly)
+      
 lemma continuous_on_poly [continuous_intros]:
   fixes p :: "'a :: {real_normed_field} poly"
   assumes "continuous_on A f"
   shows "continuous_on A (\<lambda>x. poly p (f x))"
-proof -
-  have "continuous_on A (\<lambda>x. (\<Sum>i\<le>degree p. (f x) ^ i * coeff p i))"
-    by (intro continuous_intros assms)
-  also have "\<dots> = (\<lambda>x. poly p (f x))"
-    by (rule ext) (simp add: poly_altdef mult_ac)
-  finally show ?thesis .
-qed
+  by (metis DERIV_continuous_on assms continuous_on_compose2 poly_DERIV subset_UNIV)
 
 text \<open>Consequences of the derivative theorem above.\<close>
 
@@ -2593,10 +2607,6 @@
   for x :: real
   by (simp add: real_differentiable_def) (blast intro: poly_DERIV)
 
-lemma poly_isCont[simp]: "isCont (\<lambda>x. poly p x) x"
-  for x :: real
-  by (rule poly_DERIV [THEN DERIV_isCont])
-
 lemma poly_IVT_pos: "a < b \<Longrightarrow> poly p a < 0 \<Longrightarrow> 0 < poly p b \<Longrightarrow> \<exists>x. a < x \<and> x < b \<and> poly p x = 0"
   for a b :: real
   using IVT_objl [of "poly p" a 0 b] by (auto simp add: order_le_less)
diff -r d31e986fbebc -r f8b98d31ad45 src/HOL/Library/Extended_Real.thy
--- a/src/HOL/Library/Extended_Real.thy	Thu Jun 28 14:14:05 2018 +0100
+++ b/src/HOL/Library/Extended_Real.thy	Thu Jun 28 17:14:40 2018 +0100
@@ -2921,17 +2921,6 @@
 lemma Lim_bounded_PInfty2: "f \<longlonglongrightarrow> l \<Longrightarrow> \<forall>n\<ge>N. f n \<le> ereal B \<Longrightarrow> l \<noteq> \<infinity>"
   using LIMSEQ_le_const2[of f l "ereal B"] by fastforce
 
-lemma Lim_bounded_ereal: "f \<longlonglongrightarrow> (l :: 'a::linorder_topology) \<Longrightarrow> \<forall>n\<ge>M. f n \<le> C \<Longrightarrow> l \<le> C"
-  by (intro LIMSEQ_le_const2) auto
-
-lemma Lim_bounded2_ereal:
-  assumes lim:"f \<longlonglongrightarrow> (l :: 'a::linorder_topology)"
-    and ge: "\<forall>n\<ge>N. f n \<ge> C"
-  shows "l \<ge> C"
-  using ge
-  by (intro tendsto_le[OF trivial_limit_sequentially lim tendsto_const])
-     (auto simp: eventually_sequentially)
-
 lemma real_of_ereal_mult[simp]:
   fixes a b :: ereal
   shows "real_of_ereal (a * b) = real_of_ereal a * real_of_ereal b"
@@ -3341,7 +3330,7 @@
   assumes "\<forall>N. (\<Sum>n<N. f n) \<le> x"
     and pos: "\<And>n. 0 \<le> f n"
   shows "suminf f \<le> x"
-proof (rule Lim_bounded_ereal)
+proof (rule Lim_bounded)
   have "summable f" using pos[THEN summable_ereal_pos] .
   then show "(\<lambda>N. \<Sum>n<N. f n) \<longlonglongrightarrow> suminf f"
     by (auto dest!: summable_sums simp: sums_def atLeast0LessThan)
@@ -3879,66 +3868,6 @@
   shows "X \<longlonglongrightarrow> -\<infinity> \<longleftrightarrow> limsup X = -\<infinity>"
   by (metis Limsup_MInfty trivial_limit_sequentially)
 
-lemma ereal_lim_mono:
-  fixes X Y :: "nat \<Rightarrow> 'a::linorder_topology"
-  assumes "\<And>n. N \<le> n \<Longrightarrow> X n \<le> Y n"
-    and "X \<longlonglongrightarrow> x"
-    and "Y \<longlonglongrightarrow> y"
-  shows "x \<le> y"
-  using assms(1) by (intro LIMSEQ_le[OF assms(2,3)]) auto
-
-lemma incseq_le_ereal:
-  fixes X :: "nat \<Rightarrow> 'a::linorder_topology"
-  assumes inc: "incseq X"
-    and lim: "X \<longlonglongrightarrow> L"
-  shows "X N \<le> L"
-  using inc
-  by (intro ereal_lim_mono[of N, OF _ tendsto_const lim]) (simp add: incseq_def)
-
-lemma decseq_ge_ereal:
-  assumes dec: "decseq X"
-    and lim: "X \<longlonglongrightarrow> (L::'a::linorder_topology)"
-  shows "X N \<ge> L"
-  using dec by (intro ereal_lim_mono[of N, OF _ lim tendsto_const]) (simp add: decseq_def)
-
-lemma bounded_abs:
-  fixes a :: real
-  assumes "a \<le> x"
-    and "x \<le> b"
-  shows "\<bar>x\<bar> \<le> max \<bar>a\<bar> \<bar>b\<bar>"
-  by (metis abs_less_iff assms leI le_max_iff_disj
-    less_eq_real_def less_le_not_le less_minus_iff minus_minus)
-
-lemma ereal_Sup_lim:
-  fixes a :: "'a::{complete_linorder,linorder_topology}"
-  assumes "\<And>n. b n \<in> s"
-    and "b \<longlonglongrightarrow> a"
-  shows "a \<le> Sup s"
-  by (metis Lim_bounded_ereal assms complete_lattice_class.Sup_upper)
-
-lemma ereal_Inf_lim:
-  fixes a :: "'a::{complete_linorder,linorder_topology}"
-  assumes "\<And>n. b n \<in> s"
-    and "b \<longlonglongrightarrow> a"
-  shows "Inf s \<le> a"
-  by (metis Lim_bounded2_ereal assms complete_lattice_class.Inf_lower)
-
-lemma SUP_Lim_ereal:
-  fixes X :: "nat \<Rightarrow> 'a::{complete_linorder,linorder_topology}"
-  assumes inc: "incseq X"
-    and l: "X \<longlonglongrightarrow> l"
-  shows "(SUP n. X n) = l"
-  using LIMSEQ_SUP[OF inc] tendsto_unique[OF trivial_limit_sequentially l]
-  by simp
-
-lemma INF_Lim_ereal:
-  fixes X :: "nat \<Rightarrow> 'a::{complete_linorder,linorder_topology}"
-  assumes dec: "decseq X"
-    and l: "X \<longlonglongrightarrow> l"
-  shows "(INF n. X n) = l"
-  using LIMSEQ_INF[OF dec] tendsto_unique[OF trivial_limit_sequentially l]
-  by simp
-
 lemma SUP_eq_LIMSEQ:
   assumes "mono f"
   shows "(SUP n. ereal (f n)) = ereal x \<longleftrightarrow> f \<longlonglongrightarrow> x"
@@ -3949,7 +3878,7 @@
     assume "f \<longlonglongrightarrow> x"
     then have "(\<lambda>i. ereal (f i)) \<longlonglongrightarrow> ereal x"
       by auto
-    from SUP_Lim_ereal[OF inc this] show "(SUP n. ereal (f n)) = ereal x" .
+    from SUP_Lim[OF inc this] show "(SUP n. ereal (f n)) = ereal x" .
   next
     assume "(SUP n. ereal (f n)) = ereal x"
     with LIMSEQ_SUP[OF inc] show "f \<longlonglongrightarrow> x" by auto
diff -r d31e986fbebc -r f8b98d31ad45 src/HOL/Limits.thy
--- a/src/HOL/Limits.thy	Thu Jun 28 14:14:05 2018 +0100
+++ b/src/HOL/Limits.thy	Thu Jun 28 17:14:40 2018 +0100
@@ -1347,12 +1347,17 @@
   unfolding filterlim_at_bot eventually_at_top_dense
   by (metis leI less_minus_iff order_less_asym)
 
-lemma at_top_mirror: "at_top = filtermap uminus (at_bot :: real filter)"
-  by (rule filtermap_fun_inverse[symmetric, of uminus])
-     (auto intro: filterlim_uminus_at_bot_at_top filterlim_uminus_at_top_at_bot)
-
-lemma at_bot_mirror: "at_bot = filtermap uminus (at_top :: real filter)"
-  unfolding at_top_mirror filtermap_filtermap by (simp add: filtermap_ident)
+lemma at_bot_mirror : 
+  shows "(at_bot::('a::{ordered_ab_group_add,linorder} filter)) = filtermap uminus at_top" 
+  apply (rule filtermap_fun_inverse[of uminus, symmetric])
+  subgoal unfolding filterlim_at_top eventually_at_bot_linorder using le_minus_iff by auto
+  subgoal unfolding filterlim_at_bot eventually_at_top_linorder using minus_le_iff by auto
+  by auto
+
+lemma at_top_mirror : 
+  shows "(at_top::('a::{ordered_ab_group_add,linorder} filter)) = filtermap uminus at_bot"  
+  apply (subst at_bot_mirror)
+  by (auto simp add: filtermap_filtermap)
 
 lemma filterlim_at_top_mirror: "(LIM x at_top. f x :> F) \<longleftrightarrow> (LIM x at_bot. f (-x::real) :> F)"
   unfolding filterlim_def at_top_mirror filtermap_filtermap ..
@@ -2294,7 +2299,7 @@
   obtain L where "X \<longlonglongrightarrow> L"
     by (auto simp: convergent_def monoseq_def decseq_def)
   with \<open>decseq X\<close> show "\<exists>L. X \<longlonglongrightarrow> L \<and> (\<forall>i. L \<le> X i)"
-    by (auto intro!: exI[of _ L] decseq_le)
+    by (auto intro!: exI[of _ L] decseq_ge)
 qed
 
 
diff -r d31e986fbebc -r f8b98d31ad45 src/HOL/Probability/Distribution_Functions.thy
--- a/src/HOL/Probability/Distribution_Functions.thy	Thu Jun 28 14:14:05 2018 +0100
+++ b/src/HOL/Probability/Distribution_Functions.thy	Thu Jun 28 17:14:40 2018 +0100
@@ -107,7 +107,7 @@
     using \<open>decseq f\<close> unfolding cdf_def
     by (intro finite_Lim_measure_decseq) (auto simp: decseq_def)
   also have "(\<Inter>i. {.. f i}) = {.. a}"
-    using decseq_le[OF f] by (auto intro: order_trans LIMSEQ_le_const[OF f(2)])
+    using decseq_ge[OF f] by (auto intro: order_trans LIMSEQ_le_const[OF f(2)])
   finally show "(\<lambda>n. cdf M (f n)) \<longlonglongrightarrow> cdf M a"
     by (simp add: cdf_def)
 qed simp
diff -r d31e986fbebc -r f8b98d31ad45 src/HOL/Real_Vector_Spaces.thy
--- a/src/HOL/Real_Vector_Spaces.thy	Thu Jun 28 14:14:05 2018 +0100
+++ b/src/HOL/Real_Vector_Spaces.thy	Thu Jun 28 17:14:40 2018 +0100
@@ -1092,7 +1092,7 @@
   then show ?thesis
     by simp
 qed
-
+  
 subclass uniform_space
 proof
   fix E x
diff -r d31e986fbebc -r f8b98d31ad45 src/HOL/Topological_Spaces.thy
--- a/src/HOL/Topological_Spaces.thy	Thu Jun 28 14:14:05 2018 +0100
+++ b/src/HOL/Topological_Spaces.thy	Thu Jun 28 17:14:40 2018 +0100
@@ -1109,7 +1109,7 @@
   unfolding Lim_def ..
 
 
-subsubsection \<open>Monotone sequences and subsequences\<close>
+subsection \<open>Monotone sequences and subsequences\<close>
 
 text \<open>
   Definition of monotonicity.
@@ -1132,7 +1132,7 @@
 lemma decseq_def: "decseq X \<longleftrightarrow> (\<forall>m. \<forall>n\<ge>m. X n \<le> X m)"
   unfolding antimono_def ..
 
-text \<open>Definition of subsequence.\<close>
+subsubsection \<open>Definition of subsequence.\<close>
 
 (* For compatibility with the old "subseq" *)
 lemma strict_mono_leD: "strict_mono r \<Longrightarrow> m \<le> n \<Longrightarrow> r m \<le> r n"
@@ -1205,7 +1205,7 @@
 qed
 
 
-text \<open>Subsequence (alternative definition, (e.g. Hoskins)\<close>
+subsubsection \<open>Subsequence (alternative definition, (e.g. Hoskins)\<close>
 
 lemma strict_mono_Suc_iff: "strict_mono f \<longleftrightarrow> (\<forall>n. f n < f (Suc n))"
 proof (intro iffI strict_monoI)
@@ -1351,7 +1351,7 @@
   by (rule LIMSEQ_offset [where k="Suc 0"]) simp
 
 lemma LIMSEQ_Suc_iff: "(\<lambda>n. f (Suc n)) \<longlonglongrightarrow> l = f \<longlonglongrightarrow> l"
-  by (blast intro: LIMSEQ_imp_Suc LIMSEQ_Suc)
+  by (rule filterlim_sequentially_Suc)
 
 lemma LIMSEQ_lessThan_iff_atMost:
   shows "(\<lambda>n. f {..<n}) \<longlonglongrightarrow> x \<longleftrightarrow> (\<lambda>n. f {..n}) \<longlonglongrightarrow> x"
@@ -1375,6 +1375,56 @@
   for a x :: "'a::linorder_topology"
   by (rule LIMSEQ_le[of X x "\<lambda>n. a"]) auto
 
+lemma Lim_bounded: "f \<longlonglongrightarrow> l \<Longrightarrow> \<forall>n\<ge>M. f n \<le> C \<Longrightarrow> l \<le> C"
+  for l :: "'a::linorder_topology"
+  by (intro LIMSEQ_le_const2) auto
+
+lemma Lim_bounded2:
+  fixes f :: "nat \<Rightarrow> 'a::linorder_topology"
+  assumes lim:"f \<longlonglongrightarrow> l" and ge: "\<forall>n\<ge>N. f n \<ge> C"
+  shows "l \<ge> C"
+  using ge
+  by (intro tendsto_le[OF trivial_limit_sequentially lim tendsto_const])
+     (auto simp: eventually_sequentially)
+
+lemma lim_mono:
+  fixes X Y :: "nat \<Rightarrow> 'a::linorder_topology"
+  assumes "\<And>n. N \<le> n \<Longrightarrow> X n \<le> Y n"
+    and "X \<longlonglongrightarrow> x"
+    and "Y \<longlonglongrightarrow> y"
+  shows "x \<le> y"
+  using assms(1) by (intro LIMSEQ_le[OF assms(2,3)]) auto
+
+lemma Sup_lim:
+  fixes a :: "'a::{complete_linorder,linorder_topology}"
+  assumes "\<And>n. b n \<in> s"
+    and "b \<longlonglongrightarrow> a"
+  shows "a \<le> Sup s"
+  by (metis Lim_bounded assms complete_lattice_class.Sup_upper)
+
+lemma Inf_lim:
+  fixes a :: "'a::{complete_linorder,linorder_topology}"
+  assumes "\<And>n. b n \<in> s"
+    and "b \<longlonglongrightarrow> a"
+  shows "Inf s \<le> a"
+  by (metis Lim_bounded2 assms complete_lattice_class.Inf_lower)
+
+lemma SUP_Lim:
+  fixes X :: "nat \<Rightarrow> 'a::{complete_linorder,linorder_topology}"
+  assumes inc: "incseq X"
+    and l: "X \<longlonglongrightarrow> l"
+  shows "(SUP n. X n) = l"
+  using LIMSEQ_SUP[OF inc] tendsto_unique[OF trivial_limit_sequentially l]
+  by simp
+
+lemma INF_Lim:
+  fixes X :: "nat \<Rightarrow> 'a::{complete_linorder,linorder_topology}"
+  assumes dec: "decseq X"
+    and l: "X \<longlonglongrightarrow> l"
+  shows "(INF n. X n) = l"
+  using LIMSEQ_INF[OF dec] tendsto_unique[OF trivial_limit_sequentially l]
+  by simp
+
 lemma convergentD: "convergent X \<Longrightarrow> \<exists>L. X \<longlonglongrightarrow> L"
   by (simp add: convergent_def)
 
@@ -1417,7 +1467,7 @@
   for L :: "'a::linorder_topology"
   by (metis incseq_def LIMSEQ_le_const)
 
-lemma decseq_le: "decseq X \<Longrightarrow> X \<longlonglongrightarrow> L \<Longrightarrow> L \<le> X n"
+lemma decseq_ge: "decseq X \<Longrightarrow> X \<longlonglongrightarrow> L \<Longrightarrow> L \<le> X n"
   for L :: "'a::linorder_topology"
   by (metis decseq_def LIMSEQ_le_const2)