new material about connectedness, etc.

--- a/src/HOL/Analysis/Cauchy_Integral_Theorem.thy	Sun Oct 08 16:50:37 2017 +0200
+++ b/src/HOL/Analysis/Cauchy_Integral_Theorem.thy	Mon Oct 09 15:34:23 2017 +0100
@@ -180,7 +180,7 @@
         have "f differentiable at x within ({a<..<c} - s)"
           apply (rule differentiable_at_withinI)
           using x le st
-          by (metis (no_types, lifting) DiffD1 DiffD2 DiffI UnCI atLeastAtMost_diff_ends atLeastAtMost_iff at_within_interior insert_iff interior_atLeastAtMost le st(3) x)
+          by (metis (no_types, lifting) DiffD1 DiffD2 DiffI UnCI atLeastAtMost_diff_ends atLeastAtMost_iff at_within_interior insert_iff interior_atLeastAtMost_real le st(3) x)
         moreover have "open ({a<..<c} - s)"
           by (blast intro: open_greaterThanLessThan \<open>finite s\<close> finite_imp_closed)
         ultimately show "f differentiable at x within {a..b}"
@@ -192,7 +192,7 @@
         have "g differentiable at x within ({c<..<b} - t)"
           apply (rule differentiable_at_withinI)
           using x ge st
-          by (metis DiffD1 DiffD2 DiffI UnCI atLeastAtMost_diff_ends atLeastAtMost_iff at_within_interior insert_iff interior_atLeastAtMost)
+          by (metis DiffD1 DiffD2 DiffI UnCI atLeastAtMost_diff_ends atLeastAtMost_iff at_within_interior insert_iff interior_atLeastAtMost_real)
         moreover have "open ({c<..<b} - t)"
           by (blast intro: open_greaterThanLessThan \<open>finite t\<close> finite_imp_closed)
         ultimately show "g differentiable at x within {a..b}"
@@ -1446,7 +1446,7 @@
   show ?thesis
     apply (rule fundamental_theorem_of_calculus_interior_strong)
     using k assms cfg *
-    apply (auto simp: at_within_closed_interval)
+    apply (auto simp: at_within_Icc_at)
     done
 qed
 
@@ -4158,7 +4158,7 @@
 
 subsection\<open>Winding number is zero "outside" a curve, in various senses\<close>
 
-lemma winding_number_zero_in_outside:
+proposition winding_number_zero_in_outside:
   assumes \<gamma>: "path \<gamma>" and loop: "pathfinish \<gamma> = pathstart \<gamma>" and z: "z \<in> outside (path_image \<gamma>)"
     shows "winding_number \<gamma> z = 0"
 proof -
@@ -4210,7 +4210,11 @@
   finally show ?thesis .
 qed
 
-lemma winding_number_zero_outside:
+corollary winding_number_zero_const: "a \<noteq> z \<Longrightarrow> winding_number (\<lambda>t. a) z = 0"
+  by (rule winding_number_zero_in_outside)
+     (auto simp: pathfinish_def pathstart_def path_polynomial_function)
+
+corollary winding_number_zero_outside:
     "\<lbrakk>path \<gamma>; convex s; pathfinish \<gamma> = pathstart \<gamma>; z \<notin> s; path_image \<gamma> \<subseteq> s\<rbrakk> \<Longrightarrow> winding_number \<gamma> z = 0"
   by (meson convex_in_outside outside_mono subsetCE winding_number_zero_in_outside)
 

--- a/src/HOL/Analysis/Complex_Transcendental.thy	Sun Oct 08 16:50:37 2017 +0200
+++ b/src/HOL/Analysis/Complex_Transcendental.thy	Mon Oct 09 15:34:23 2017 +0100
@@ -1233,7 +1233,7 @@
 lemma continuous_on_Ln [continuous_intros]: "(\<And>z. z \<in> s \<Longrightarrow> z \<notin> \<real>\<^sub>\<le>\<^sub>0) \<Longrightarrow> continuous_on s Ln"
   by (simp add: continuous_at_imp_continuous_on continuous_within_Ln)
 
-lemma holomorphic_on_Ln: "(\<And>z. z \<in> s \<Longrightarrow> z \<notin> \<real>\<^sub>\<le>\<^sub>0) \<Longrightarrow> Ln holomorphic_on s"
+lemma holomorphic_on_Ln [holomorphic_intros]: "(\<And>z. z \<in> s \<Longrightarrow> z \<notin> \<real>\<^sub>\<le>\<^sub>0) \<Longrightarrow> Ln holomorphic_on s"
   by (simp add: field_differentiable_within_Ln holomorphic_on_def)
 
 lemma divide_ln_mono:

--- a/src/HOL/Analysis/Conformal_Mappings.thy	Sun Oct 08 16:50:37 2017 +0200
+++ b/src/HOL/Analysis/Conformal_Mappings.thy	Mon Oct 09 15:34:23 2017 +0100
@@ -1454,6 +1454,15 @@
   qed
 qed
 
+corollary Schwarz_Lemma':
+  assumes holf: "f holomorphic_on (ball 0 1)" and [simp]: "f 0 = 0"
+      and no: "\<And>z. norm z < 1 \<Longrightarrow> norm (f z) < 1"
+    shows "((\<forall>\<xi>. norm \<xi> < 1 \<longrightarrow> norm (f \<xi>) \<le> norm \<xi>) \<and> norm(deriv f 0) \<le> 1) \<and>
+           (((\<exists>z. norm z < 1 \<and> z \<noteq> 0 \<and> norm(f z) = norm z) \<or> norm(deriv f 0) = 1)
+           \<longrightarrow> (\<exists>\<alpha>. (\<forall>z. norm z < 1 \<longrightarrow> f z = \<alpha> * z) \<and> norm \<alpha> = 1))"
+  using Schwarz_Lemma [OF assms]
+  by (metis (no_types) norm_eq_zero zero_less_one)
+
 subsection\<open>The Schwarz reflection principle\<close>
 
 lemma hol_pal_lem0:

--- a/src/HOL/Analysis/Convex_Euclidean_Space.thy	Sun Oct 08 16:50:37 2017 +0200
+++ b/src/HOL/Analysis/Convex_Euclidean_Space.thy	Mon Oct 09 15:34:23 2017 +0100
@@ -4696,6 +4696,15 @@
   finally show ?thesis .
 qed
 
+lemma interior_atLeastLessThan [simp]:
+  fixes a::real shows "interior {a..<b} = {a<..<b}"
+  by (metis atLeastLessThan_def greaterThanLessThan_def interior_atLeastAtMost_real interior_Int interior_interior interior_real_semiline)
+
+lemma interior_lessThanAtMost [simp]:
+  fixes a::real shows "interior {a<..b} = {a<..<b}"
+  by (metis atLeastAtMost_def greaterThanAtMost_def interior_atLeastAtMost_real interior_Int
+            interior_interior interior_real_semiline)
+
 lemma interior_greaterThanLessThan_real [simp]: "interior {a<..<b} = {a<..<b :: real}"
   by (metis interior_atLeastAtMost_real interior_interior)
 

--- a/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy	Sun Oct 08 16:50:37 2017 +0200
+++ b/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy	Mon Oct 09 15:34:23 2017 +0100
@@ -6467,7 +6467,7 @@
   qed
   have deriv: "(?F has_vector_derivative g' x *\<^sub>R f (g x))
                   (at x)" if "x \<in> {a..b} - (s \<union> {a,b})" for x
-    using deriv[of x] that by (simp add: at_within_closed_interval o_def)
+    using deriv[of x] that by (simp add: at_within_Icc_at o_def)
   have "((\<lambda>x. g' x *\<^sub>R f (g x)) has_integral (?F b - ?F a)) {a..b}"
     using le cont_int s deriv cont_int
     by (intro fundamental_theorem_of_calculus_interior_strong[of "s \<union> {a,b}"]) simp_all

--- a/src/HOL/Analysis/Path_Connected.thy	Sun Oct 08 16:50:37 2017 +0200
+++ b/src/HOL/Analysis/Path_Connected.thy	Mon Oct 09 15:34:23 2017 +0100
@@ -166,6 +166,9 @@
 lemma simple_path_eq_arc: "pathfinish g \<noteq> pathstart g \<Longrightarrow> (simple_path g = arc g)"
   by (simp add: arc_simple_path)
 
+lemma path_image_const [simp]: "path_image (\<lambda>t. a) = {a}"
+  by (force simp: path_image_def)
+
 lemma path_image_nonempty [simp]: "path_image g \<noteq> {}"
   unfolding path_image_def image_is_empty box_eq_empty
   by auto
@@ -1511,13 +1514,7 @@
   assumes "convex s"
   shows "path_connected s"
   unfolding path_connected_def
-  apply rule
-  apply rule
-  apply (rule_tac x = "linepath x y" in exI)
-  unfolding path_image_linepath
-  using assms [unfolded convex_contains_segment]
-  apply auto
-  done
+  using assms convex_contains_segment by fastforce
 
 lemma path_connected_UNIV [iff]: "path_connected (UNIV :: 'a::real_normed_vector set)"
   by (simp add: convex_imp_path_connected)
@@ -1528,13 +1525,7 @@
 lemma path_connected_imp_connected:
   assumes "path_connected S"
   shows "connected S"
-  unfolding connected_def not_ex
-  apply rule
-  apply rule
-  apply (rule ccontr)
-  unfolding not_not
-  apply (elim conjE)
-proof -
+proof (rule connectedI)
   fix e1 e2
   assume as: "open e1" "open e2" "S \<subseteq> e1 \<union> e2" "e1 \<inter> e2 \<inter> S = {}" "e1 \<inter> S \<noteq> {}" "e2 \<inter> S \<noteq> {}"
   then obtain x1 x2 where obt:"x1 \<in> e1 \<inter> S" "x2 \<in> e2 \<inter> S"
@@ -1570,31 +1561,14 @@
   fix y
   assume as: "y \<in> path_component_set S x"
   then have "y \<in> S"
-    apply -
-    apply (rule path_component_mem(2))
-    unfolding mem_Collect_eq
-    apply auto
-    done
+    by (simp add: path_component_mem(2))
   then obtain e where e: "e > 0" "ball y e \<subseteq> S"
     using assms[unfolded open_contains_ball]
     by auto
-  show "\<exists>e > 0. ball y e \<subseteq> path_component_set S x"
-    apply (rule_tac x=e in exI)
-    apply (rule,rule \<open>e>0\<close>)
-    apply rule
-    unfolding mem_ball mem_Collect_eq
-  proof -
-    fix z
-    assume "dist y z < e"
-    then show "path_component S x z"
-      apply (rule_tac path_component_trans[of _ _ y])
-      defer
-      apply (rule path_component_of_subset[OF e(2)])
-      apply (rule convex_imp_path_connected[OF convex_ball, unfolded path_connected_component, rule_format])
-      using \<open>e > 0\<close> as
-      apply auto
-      done
-  qed
+have "\<And>u. dist y u < e \<Longrightarrow> path_component S x u"
+      by (metis (full_types) as centre_in_ball convex_ball convex_imp_path_connected e mem_Collect_eq mem_ball path_component_eq path_component_of_subset path_connected_component)
+  then show "\<exists>e > 0. ball y e \<subseteq> path_component_set S x"
+    using \<open>e>0\<close> by auto
 qed
 
 lemma open_non_path_component:
@@ -1904,6 +1878,8 @@
 using is_interval_connected_1 is_interval_path_connected path_connected_imp_connected by blast
 
 
+subsection\<open>Path components\<close>
+
 lemma Union_path_component [simp]:
    "Union {path_component_set S x |x. x \<in> S} = S"
 apply (rule subset_antisym)
@@ -2151,7 +2127,6 @@
     by (auto simp: path_connected_component)
 qed
 
-
 lemma connected_complement_bounded_convex:
     fixes s :: "'a :: euclidean_space set"
     assumes "bounded s" "convex s" "2 \<le> DIM('a)"
@@ -2300,6 +2275,65 @@
 qed
 
 
+subsection\<open>Every annulus is a connected set\<close>
+
+lemma path_connected_2DIM_I:
+  fixes a :: "'N::euclidean_space"
+  assumes 2: "2 \<le> DIM('N)" and pc: "path_connected {r. 0 \<le> r \<and> P r}"
+  shows "path_connected {x. P(norm(x - a))}"
+proof -
+  have "{x. P(norm(x - a))} = op+a ` {x. P(norm x)}"
+    by force
+  moreover have "path_connected {x::'N. P(norm x)}"
+  proof -
+    let ?D = "{x. 0 \<le> x \<and> P x} \<times> sphere (0::'N) 1"
+    have "x \<in> (\<lambda>z. fst z *\<^sub>R snd z) ` ?D"
+      if "P (norm x)" for x::'N
+    proof (cases "x=0")
+      case True
+      with that show ?thesis
+        apply (simp add: image_iff)
+        apply (rule_tac x=0 in exI, simp)
+        using vector_choose_size zero_le_one by blast
+    next
+      case False
+      with that show ?thesis
+        by (rule_tac x="(norm x, x /\<^sub>R norm x)" in image_eqI) auto
+    qed
+    then have *: "{x::'N. P(norm x)} =  (\<lambda>z. fst z *\<^sub>R snd z) ` ?D"
+      by auto
+    have "continuous_on ?D (\<lambda>z:: real\<times>'N. fst z *\<^sub>R snd z)"
+      by (intro continuous_intros)
+    moreover have "path_connected ?D"
+      by (metis path_connected_Times [OF pc] path_connected_sphere 2)
+    ultimately show ?thesis
+      apply (subst *)
+      apply (rule path_connected_continuous_image, auto)
+      done
+  qed
+  ultimately show ?thesis
+    using path_connected_translation by metis
+qed
+
+lemma path_connected_annulus:
+  fixes a :: "'N::euclidean_space"
+  assumes "2 \<le> DIM('N)"
+  shows "path_connected {x. r1 < norm(x - a) \<and> norm(x - a) < r2}"
+        "path_connected {x. r1 < norm(x - a) \<and> norm(x - a) \<le> r2}"
+        "path_connected {x. r1 \<le> norm(x - a) \<and> norm(x - a) < r2}"
+        "path_connected {x. r1 \<le> norm(x - a) \<and> norm(x - a) \<le> r2}"
+  by (auto simp: is_interval_def intro!: is_interval_convex convex_imp_path_connected path_connected_2DIM_I [OF assms])
+
+lemma connected_annulus:
+  fixes a :: "'N::euclidean_space"
+  assumes "2 \<le> DIM('N::euclidean_space)"
+  shows "connected {x. r1 < norm(x - a) \<and> norm(x - a) < r2}"
+        "connected {x. r1 < norm(x - a) \<and> norm(x - a) \<le> r2}"
+        "connected {x. r1 \<le> norm(x - a) \<and> norm(x - a) < r2}"
+        "connected {x. r1 \<le> norm(x - a) \<and> norm(x - a) \<le> r2}"
+  by (auto simp: path_connected_annulus [OF assms] path_connected_imp_connected)
+
+
 subsection\<open>Relations between components and path components\<close>
 
 lemma open_connected_component:
@@ -2894,11 +2928,21 @@
     shows "outside s = - s"
   by (metis ComplD assms convex_in_outside equalityI inside_Un_outside subsetI sup.cobounded2)
 
+lemma outside_singleton [simp]:
+  fixes x :: "'a :: {real_normed_vector, perfect_space}"
+  shows "outside {x} = -{x}"
+  by (auto simp: outside_convex)
+
 lemma inside_convex:
   fixes s :: "'a :: {real_normed_vector, perfect_space} set"
   shows "convex s \<Longrightarrow> inside s = {}"
   by (simp add: inside_outside outside_convex)
 
+lemma inside_singleton [simp]:
+  fixes x :: "'a :: {real_normed_vector, perfect_space}"
+  shows "inside {x} = {}"
+  by (auto simp: inside_convex)
+
 lemma outside_subset_convex:
   fixes s :: "'a :: {real_normed_vector, perfect_space} set"
   shows "\<lbrakk>convex t; s \<subseteq> t\<rbrakk> \<Longrightarrow> - t \<subseteq> outside s"
@@ -4119,6 +4163,39 @@
     by (blast intro: homotopic_loops_trans)
 qed
 
+lemma homotopic_paths_loop_parts:
+  assumes loops: "homotopic_loops S (p +++ reversepath q) (linepath a a)" and "path q"
+  shows "homotopic_paths S p q"
+proof -
+  have paths: "homotopic_paths S (p +++ reversepath q) (linepath (pathstart p) (pathstart p))"
+    using homotopic_loops_imp_homotopic_paths_null [OF loops] by simp
+  then have "path p"
+    using \<open>path q\<close> homotopic_loops_imp_path loops path_join path_join_path_ends path_reversepath by blast
+  show ?thesis
+  proof (cases "pathfinish p = pathfinish q")
+    case True
+    have pipq: "path_image p \<subseteq> S" "path_image q \<subseteq> S"
+      by (metis Un_subset_iff paths \<open>path p\<close> \<open>path q\<close> homotopic_loops_imp_subset homotopic_paths_imp_path loops
+           path_image_join path_image_reversepath path_imp_reversepath path_join_eq)+
+    have "homotopic_paths S p (p +++ (linepath (pathfinish p) (pathfinish p)))"
+      using \<open>path p\<close> \<open>path_image p \<subseteq> S\<close> homotopic_paths_rid homotopic_paths_sym by blast
+    moreover have "homotopic_paths S (p +++ (linepath (pathfinish p) (pathfinish p))) (p +++ (reversepath q +++ q))"
+      by (simp add: True \<open>path p\<close> \<open>path q\<close> pipq homotopic_paths_join homotopic_paths_linv homotopic_paths_sym)
+    moreover have "homotopic_paths S (p +++ (reversepath q +++ q)) ((p +++ reversepath q) +++ q)"
+      by (simp add: True \<open>path p\<close> \<open>path q\<close> homotopic_paths_assoc pipq)
+    moreover have "homotopic_paths S ((p +++ reversepath q) +++ q) (linepath (pathstart p) (pathstart p) +++ q)"
+      by (simp add: \<open>path q\<close> homotopic_paths_join paths pipq)
+    moreover then have "homotopic_paths S (linepath (pathstart p) (pathstart p) +++ q) q"
+      by (metis \<open>path q\<close> homotopic_paths_imp_path homotopic_paths_lid linepath_trivial path_join_path_ends pathfinish_def pipq(2))
+    ultimately show ?thesis
+      using homotopic_paths_trans by metis
+  next
+    case False
+    then show ?thesis
+      using \<open>path q\<close> homotopic_loops_imp_path loops path_join_path_ends by fastforce
+  qed
+qed
+
 
 subsection\<open> Homotopy of "nearby" function, paths and loops.\<close>
 

--- a/src/HOL/Analysis/Starlike.thy	Sun Oct 08 16:50:37 2017 +0200
+++ b/src/HOL/Analysis/Starlike.thy	Mon Oct 09 15:34:23 2017 +0100
@@ -3776,24 +3776,6 @@
 
 subsection\<open>Explicit formulas for interior and relative interior of convex hull\<close>
 
-lemma interior_atLeastAtMost [simp]:
-  fixes a::real shows "interior {a..b} = {a<..<b}"
-  using interior_cbox [of a b] by auto
-
-lemma interior_atLeastLessThan [simp]:
-  fixes a::real shows "interior {a..<b} = {a<..<b}"
-  by (metis atLeastLessThan_def greaterThanLessThan_def interior_atLeastAtMost interior_Int interior_interior interior_real_semiline)
-
-lemma interior_lessThanAtMost [simp]:
-  fixes a::real shows "interior {a<..b} = {a<..<b}"
-  by (metis atLeastAtMost_def greaterThanAtMost_def interior_atLeastAtMost interior_Int
-            interior_interior interior_real_semiline)
-
-lemma at_within_closed_interval:
-    fixes x::real
-    shows "a < x \<Longrightarrow> x < b \<Longrightarrow> (at x within {a..b}) = at x"
-  by (metis at_within_interior greaterThanLessThan_iff interior_atLeastAtMost)
-
 lemma at_within_cbox_finite:
   assumes "x \<in> box a b" "x \<notin> S" "finite S"
   shows "(at x within cbox a b - S) = at x"
@@ -5087,7 +5069,6 @@
 using separation_closures [of S T]
 by (metis assms closure_closed disjnt_def inf_commute)
 
-
 lemma separation_normal_local:
   fixes S :: "'a::euclidean_space set"
   assumes US: "closedin (subtopology euclidean U) S"
@@ -5147,6 +5128,139 @@
     by auto (meson bounded_ball bounded_subset compl_le_swap2 disjoint_eq_subset_Compl)
 qed
 
+subsection\<open>Connectedness of the intersection of a chain\<close>
+
+proposition connected_chain:
+  fixes \<F> :: "'a :: euclidean_space set set"
+  assumes cc: "\<And>S. S \<in> \<F> \<Longrightarrow> compact S \<and> connected S"
+      and linear: "\<And>S T. S \<in> \<F> \<and> T \<in> \<F> \<Longrightarrow> S \<subseteq> T \<or> T \<subseteq> S"
+  shows "connected(\<Inter>\<F>)"
+proof (cases "\<F> = {}")
+  case True then show ?thesis
+    by auto
+next
+  case False
+  then have cf: "compact(\<Inter>\<F>)"
+    by (simp add: cc compact_Inter)
+  have False if AB: "closed A" "closed B" "A \<inter> B = {}"
+                and ABeq: "A \<union> B = \<Inter>\<F>" and "A \<noteq> {}" "B \<noteq> {}" for A B
+  proof -
+    obtain U V where "open U" "open V" "A \<subseteq> U" "B \<subseteq> V" "U \<inter> V = {}"
+      using separation_normal [OF AB] by metis
+    obtain K where "K \<in> \<F>" "compact K"
+      using cc False by blast
+    then obtain N where "open N" and "K \<subseteq> N"
+      by blast
+    let ?\<C> = "insert (U \<union> V) ((\<lambda>S. N - S) ` \<F>)"
+    obtain \<D> where "\<D> \<subseteq> ?\<C>" "finite \<D>" "K \<subseteq> \<Union>\<D>"
+    proof (rule compactE [OF \<open>compact K\<close>])
+      show "K \<subseteq> \<Union>insert (U \<union> V) (op - N ` \<F>)"
+        using \<open>K \<subseteq> N\<close> ABeq \<open>A \<subseteq> U\<close> \<open>B \<subseteq> V\<close> by auto
+      show "\<And>B. B \<in> insert (U \<union> V) (op - N ` \<F>) \<Longrightarrow> open B"
+        by (auto simp:  \<open>open U\<close> \<open>open V\<close> open_Un \<open>open N\<close> cc compact_imp_closed open_Diff)
+    qed
+    then have "finite(\<D> - {U \<union> V})"
+      by blast
+    moreover have "\<D> - {U \<union> V} \<subseteq> (\<lambda>S. N - S) ` \<F>"
+      using \<open>\<D> \<subseteq> ?\<C>\<close> by blast
+    ultimately obtain \<G> where "\<G> \<subseteq> \<F>" "finite \<G>" and Deq: "\<D> - {U \<union> V} = (\<lambda>S. N-S) ` \<G>"
+      using finite_subset_image by metis
+    obtain J where "J \<in> \<F>" and J: "(\<Union>S\<in>\<G>. N - S) \<subseteq> N - J"
+    proof (cases "\<G> = {}")
+      case True
+      with \<open>\<F> \<noteq> {}\<close> that show ?thesis
+        by auto
+    next
+      case False
+      have "\<And>S T. \<lbrakk>S \<in> \<G>; T \<in> \<G>\<rbrakk> \<Longrightarrow> S \<subseteq> T \<or> T \<subseteq> S"
+        by (meson \<open>\<G> \<subseteq> \<F>\<close> in_mono local.linear)
+      with \<open>finite \<G>\<close> \<open>\<G> \<noteq> {}\<close>
+      have "\<exists>J \<in> \<G>. (\<Union>S\<in>\<G>. N - S) \<subseteq> N - J"
+      proof induction
+        case (insert X \<H>)
+        show ?case
+        proof (cases "\<H> = {}")
+          case True then show ?thesis by auto
+        next
+          case False
+          then have "\<And>S T. \<lbrakk>S \<in> \<H>; T \<in> \<H>\<rbrakk> \<Longrightarrow> S \<subseteq> T \<or> T \<subseteq> S"
+            by (simp add: insert.prems)
+          with insert.IH False obtain J where "J \<in> \<H>" and J: "(\<Union>Y\<in>\<H>. N - Y) \<subseteq> N - J"
+            by metis
+          have "N - J \<subseteq> N - X \<or> N - X \<subseteq> N - J"
+            by (meson Diff_mono \<open>J \<in> \<H>\<close> insert.prems(2) insert_iff order_refl)
+          then show ?thesis
+          proof
+            assume "N - J \<subseteq> N - X" with J show ?thesis
+              by auto
+          next
+            assume "N - X \<subseteq> N - J"
+            with J have "N - X \<union> UNION \<H> (op - N) \<subseteq> N - J"
+              by auto
+            with \<open>J \<in> \<H>\<close> show ?thesis
+              by blast
+          qed
+        qed
+      qed simp
+      with \<open>\<G> \<subseteq> \<F>\<close> show ?thesis by (blast intro: that)
+    qed
+    have "K \<subseteq> \<Union>(insert (U \<union> V) (\<D> - {U \<union> V}))"
+      using \<open>K \<subseteq> \<Union>\<D>\<close> by auto
+    also have "... \<subseteq> (U \<union> V) \<union> (N - J)"
+      by (metis (no_types, hide_lams) Deq Un_subset_iff Un_upper2 J Union_insert order_trans sup_ge1)
+    finally have "J \<inter> K \<subseteq> U \<union> V"
+      by blast
+    moreover have "connected(J \<inter> K)"
+      by (metis Int_absorb1 \<open>J \<in> \<F>\<close> \<open>K \<in> \<F>\<close> cc inf.orderE local.linear)
+    moreover have "U \<inter> (J \<inter> K) \<noteq> {}"
+      using ABeq \<open>J \<in> \<F>\<close> \<open>K \<in> \<F>\<close> \<open>A \<noteq> {}\<close> \<open>A \<subseteq> U\<close> by blast
+    moreover have "V \<inter> (J \<inter> K) \<noteq> {}"
+      using ABeq \<open>J \<in> \<F>\<close> \<open>K \<in> \<F>\<close> \<open>B \<noteq> {}\<close> \<open>B \<subseteq> V\<close> by blast
+    ultimately show False
+        using connectedD [of "J \<inter> K" U V] \<open>open U\<close> \<open>open V\<close> \<open>U \<inter> V = {}\<close>  by auto
+  qed
+  with cf show ?thesis
+    by (auto simp: connected_closed_set compact_imp_closed)
+qed
+
+lemma connected_chain_gen:
+  fixes \<F> :: "'a :: euclidean_space set set"
+  assumes X: "X \<in> \<F>" "compact X"
+      and cc: "\<And>T. T \<in> \<F> \<Longrightarrow> closed T \<and> connected T"
+      and linear: "\<And>S T. S \<in> \<F> \<and> T \<in> \<F> \<Longrightarrow> S \<subseteq> T \<or> T \<subseteq> S"
+  shows "connected(\<Inter>\<F>)"
+proof -
+  have "\<Inter>\<F> = (\<Inter>T\<in>\<F>. X \<inter> T)"
+    using X by blast
+  moreover have "connected (\<Inter>T\<in>\<F>. X \<inter> T)"
+  proof (rule connected_chain)
+    show "\<And>T. T \<in> op \<inter> X ` \<F> \<Longrightarrow> compact T \<and> connected T"
+      using cc X by auto (metis inf.absorb2 inf.orderE local.linear)
+    show "\<And>S T. S \<in> op \<inter> X ` \<F> \<and> T \<in> op \<inter> X ` \<F> \<Longrightarrow> S \<subseteq> T \<or> T \<subseteq> S"
+      using local.linear by blast
+  qed
+  ultimately show ?thesis
+    by metis
+qed
+
+lemma connected_nest:
+  fixes S :: "'a::linorder \<Rightarrow> 'b::euclidean_space set"
+  assumes S: "\<And>n. compact(S n)" "\<And>n. connected(S n)"
+    and nest: "\<And>m n. m \<le> n \<Longrightarrow> S n \<subseteq> S m"
+  shows "connected(\<Inter> (range S))"
+  apply (rule connected_chain)
+  using S apply blast
+  by (metis image_iff le_cases nest)
+
+lemma connected_nest_gen:
+  fixes S :: "'a::linorder \<Rightarrow> 'b::euclidean_space set"
+  assumes S: "\<And>n. closed(S n)" "\<And>n. connected(S n)" "compact(S k)"
+    and nest: "\<And>m n. m \<le> n \<Longrightarrow> S n \<subseteq> S m"
+  shows "connected(\<Inter> (range S))"
+  apply (rule connected_chain_gen [of "S k"])
+  using S apply auto
+  by (meson le_cases nest subsetCE)
+
 subsection\<open>Proper maps, including projections out of compact sets\<close>
 
 lemma finite_indexed_bound:

--- a/src/HOL/Analysis/Topology_Euclidean_Space.thy	Sun Oct 08 16:50:37 2017 +0200
+++ b/src/HOL/Analysis/Topology_Euclidean_Space.thy	Mon Oct 09 15:34:23 2017 +0100
@@ -676,6 +676,10 @@
     using openin_INT[of _ _ U, OF assms(1) assms(3)] by (simp add: inf.absorb2 inf_commute)
 qed
 
+lemma openin_Inter [intro]:
+  assumes "finite \<F>" "\<F> \<noteq> {}" "\<And>X. X \<in> \<F> \<Longrightarrow> openin T X" shows "openin T (\<Inter>\<F>)"
+  by (metis (full_types) assms openin_INT2 image_ident)
+
 
 subsubsection \<open>Closed sets\<close>
 
@@ -2404,6 +2408,11 @@
 lemma closedin_closed_eq: "closed S \<Longrightarrow> closedin (subtopology euclidean S) T \<longleftrightarrow> closed T \<and> T \<subseteq> S"
   by (meson closedin_limpt closed_subset closedin_closed_trans)
 
+lemma connected_closed_set:
+   "closed S
+    \<Longrightarrow> connected S \<longleftrightarrow> (\<nexists>A B. closed A \<and> closed B \<and> A \<noteq> {} \<and> B \<noteq> {} \<and> A \<union> B = S \<and> A \<inter> B = {})"
+  unfolding connected_closedin_eq closedin_closed_eq connected_closedin_eq by blast
+
 lemma closedin_subset_trans:
   "closedin (subtopology euclidean U) S \<Longrightarrow> S \<subseteq> T \<Longrightarrow> T \<subseteq> U \<Longrightarrow>
     closedin (subtopology euclidean T) S"
@@ -5407,6 +5416,13 @@
     by auto
 qed
 
+lemma compact_Inter:
+  fixes \<F> :: "'a :: heine_borel set set"
+  assumes com: "\<And>S. S \<in> \<F> \<Longrightarrow> compact S" and "\<F> \<noteq> {}"
+  shows "compact(\<Inter> \<F>)"
+  using assms
+  by (meson Inf_lower all_not_in_conv bounded_subset closed_Inter compact_eq_bounded_closed)
+
 lemma compact_closure [simp]:
   fixes S :: "'a::heine_borel set"
   shows "compact(closure S) \<longleftrightarrow> bounded S"
@@ -5819,19 +5835,6 @@
   then show ?thesis unfolding complete_def by auto
 qed
 
-lemma nat_approx_posE:
-  fixes e::real
-  assumes "0 < e"
-  obtains n :: nat where "1 / (Suc n) < e"
-proof atomize_elim
-  have "1 / real (Suc (nat \<lceil>1/e\<rceil>)) < 1 / \<lceil>1/e\<rceil>"
-    by (rule divide_strict_left_mono) (auto simp: \<open>0 < e\<close>)
-  also have "1 / \<lceil>1/e\<rceil> \<le> 1 / (1/e)"
-    by (rule divide_left_mono) (auto simp: \<open>0 < e\<close> ceiling_correct)
-  also have "\<dots> = e" by simp
-  finally show  "\<exists>n. 1 / real (Suc n) < e" ..
-qed
-
 lemma compact_eq_totally_bounded:
   "compact s \<longleftrightarrow> complete s \<and> (\<forall>e>0. \<exists>k. finite k \<and> s \<subseteq> (\<Union>x\<in>k. ball x e))"
     (is "_ \<longleftrightarrow> ?rhs")
@@ -9679,6 +9682,43 @@
       simp: dist_commute dist_norm pos_divide_less_eq mult_strict_left_mono)
     done
 
+lemma homeomorphic_ball01_UNIV:
+  "ball (0::'a::real_normed_vector) 1 homeomorphic (UNIV:: 'a set)"
+  (is "?B homeomorphic ?U")
+proof
+  have "x \<in> (\<lambda>z. z /\<^sub>R (1 - norm z)) ` ball 0 1" for x::'a
+    apply (rule_tac x="x /\<^sub>R (1 + norm x)" in image_eqI)
+     apply (auto simp: divide_simps)
+    using norm_ge_zero [of x] apply linarith+
+    done
+  then show "(\<lambda>z::'a. z /\<^sub>R (1 - norm z)) ` ?B = ?U"
+    by blast
+  have "x \<in> range (\<lambda>z. (1 / (1 + norm z)) *\<^sub>R z)" if "norm x < 1" for x::'a
+    apply (rule_tac x="x /\<^sub>R (1 - norm x)" in image_eqI)
+    using that apply (auto simp: divide_simps)
+    done
+  then show "(\<lambda>z::'a. z /\<^sub>R (1 + norm z)) ` ?U = ?B"
+    by (force simp: divide_simps dest: add_less_zeroD)
+  show "continuous_on (ball 0 1) (\<lambda>z. z /\<^sub>R (1 - norm z))"
+    by (rule continuous_intros | force)+
+  show "continuous_on UNIV (\<lambda>z. z /\<^sub>R (1 + norm z))"
+    apply (intro continuous_intros)
+    apply (metis le_add_same_cancel1 norm_ge_zero not_le zero_less_one)
+    done
+  show "\<And>x. x \<in> ball 0 1 \<Longrightarrow>
+         x /\<^sub>R (1 - norm x) /\<^sub>R (1 + norm (x /\<^sub>R (1 - norm x))) = x"
+    by (auto simp: divide_simps)
+  show "\<And>y. y /\<^sub>R (1 + norm y) /\<^sub>R (1 - norm (y /\<^sub>R (1 + norm y))) = y"
+    apply (auto simp: divide_simps)
+    apply (metis le_add_same_cancel1 norm_ge_zero not_le zero_less_one)
+    done
+qed
+
+proposition homeomorphic_ball_UNIV:
+  fixes a ::"'a::real_normed_vector"
+  assumes "0 < r" shows "ball a r homeomorphic (UNIV:: 'a set)"
+  using assms homeomorphic_ball01_UNIV homeomorphic_balls(1) homeomorphic_trans zero_less_one by blast
+
 subsection\<open>Inverse function property for open/closed maps\<close>
 
 lemma continuous_on_inverse_open_map:
@@ -10711,7 +10751,7 @@
   then show ?thesis by blast
 qed
 
-lemma closed_imp_fip_compact:
+lemma clconnected_closedin_eqosed_imp_fip_compact:
   fixes S :: "'a::heine_borel set"
   shows
    "\<lbrakk>closed S; \<And>T. T \<in> \<F> \<Longrightarrow> compact T;
@@ -11043,38 +11083,38 @@
 text\<open>Still missing: versions for a set that is smaller than R, or countable.\<close>
 
 lemma continuous_disconnected_range_constant:
-  assumes s: "connected s"
-      and conf: "continuous_on s f"
-      and fim: "f ` s \<subseteq> t"
+  assumes S: "connected S"
+      and conf: "continuous_on S f"
+      and fim: "f ` S \<subseteq> t"
       and cct: "\<And>y. y \<in> t \<Longrightarrow> connected_component_set t y = {y}"
-    shows "\<exists>a. \<forall>x \<in> s. f x = a"
-proof (cases "s = {}")
+    shows "\<exists>a. \<forall>x \<in> S. f x = a"
+proof (cases "S = {}")
   case True then show ?thesis by force
 next
   case False
-  { fix x assume "x \<in> s"
-    then have "f ` s \<subseteq> {f x}"
-    by (metis connected_continuous_image conf connected_component_maximal fim image_subset_iff rev_image_eqI s cct)
+  { fix x assume "x \<in> S"
+    then have "f ` S \<subseteq> {f x}"
+    by (metis connected_continuous_image conf connected_component_maximal fim image_subset_iff rev_image_eqI S cct)
   }
   with False show ?thesis
     by blast
 qed
 
 lemma discrete_subset_disconnected:
-  fixes s :: "'a::topological_space set"
+  fixes S :: "'a::topological_space set"
   fixes t :: "'b::real_normed_vector set"
-  assumes conf: "continuous_on s f"
-      and no: "\<And>x. x \<in> s \<Longrightarrow> \<exists>e>0. \<forall>y. y \<in> s \<and> f y \<noteq> f x \<longrightarrow> e \<le> norm (f y - f x)"
-   shows "f ` s \<subseteq> {y. connected_component_set (f ` s) y = {y}}"
-proof -
-  { fix x assume x: "x \<in> s"
-    then obtain e where "e>0" and ele: "\<And>y. \<lbrakk>y \<in> s; f y \<noteq> f x\<rbrakk> \<Longrightarrow> e \<le> norm (f y - f x)"
+  assumes conf: "continuous_on S f"
+      and no: "\<And>x. x \<in> S \<Longrightarrow> \<exists>e>0. \<forall>y. y \<in> S \<and> f y \<noteq> f x \<longrightarrow> e \<le> norm (f y - f x)"
+   shows "f ` S \<subseteq> {y. connected_component_set (f ` S) y = {y}}"
+proof -
+  { fix x assume x: "x \<in> S"
+    then obtain e where "e>0" and ele: "\<And>y. \<lbrakk>y \<in> S; f y \<noteq> f x\<rbrakk> \<Longrightarrow> e \<le> norm (f y - f x)"
       using conf no [OF x] by auto
     then have e2: "0 \<le> e / 2"
       by simp
-    have "f y = f x" if "y \<in> s" and ccs: "f y \<in> connected_component_set (f ` s) (f x)" for y
+    have "f y = f x" if "y \<in> S" and ccs: "f y \<in> connected_component_set (f ` S) (f x)" for y
       apply (rule ccontr)
-      using connected_closed [of "connected_component_set (f ` s) (f x)"] \<open>e>0\<close>
+      using connected_closed [of "connected_component_set (f ` S) (f x)"] \<open>e>0\<close>
       apply (simp add: del: ex_simps)
       apply (drule spec [where x="cball (f x) (e / 2)"])
       apply (drule spec [where x="- ball(f x) e"])
@@ -11082,11 +11122,11 @@
         apply (metis diff_self e2 ele norm_minus_commute norm_zero not_less)
        using centre_in_cball connected_component_refl_eq e2 x apply blast
       using ccs
-      apply (force simp: cball_def dist_norm norm_minus_commute dest: ele [OF \<open>y \<in> s\<close>])
+      apply (force simp: cball_def dist_norm norm_minus_commute dest: ele [OF \<open>y \<in> S\<close>])
       done
-    moreover have "connected_component_set (f ` s) (f x) \<subseteq> f ` s"
+    moreover have "connected_component_set (f ` S) (f x) \<subseteq> f ` S"
       by (auto simp: connected_component_in)
-    ultimately have "connected_component_set (f ` s) (f x) = {f x}"
+    ultimately have "connected_component_set (f ` S) (f x) = {f x}"
       by (auto simp: x)
   }
   with assms show ?thesis
@@ -11094,22 +11134,22 @@
 qed
 
 lemma finite_implies_discrete:
-  fixes s :: "'a::topological_space set"
-  assumes "finite (f ` s)"
-  shows "(\<forall>x \<in> s. \<exists>e>0. \<forall>y. y \<in> s \<and> f y \<noteq> f x \<longrightarrow> e \<le> norm (f y - f x))"
-proof -
-  have "\<exists>e>0. \<forall>y. y \<in> s \<and> f y \<noteq> f x \<longrightarrow> e \<le> norm (f y - f x)" if "x \<in> s" for x
-  proof (cases "f ` s - {f x} = {}")
+  fixes S :: "'a::topological_space set"
+  assumes "finite (f ` S)"
+  shows "(\<forall>x \<in> S. \<exists>e>0. \<forall>y. y \<in> S \<and> f y \<noteq> f x \<longrightarrow> e \<le> norm (f y - f x))"
+proof -
+  have "\<exists>e>0. \<forall>y. y \<in> S \<and> f y \<noteq> f x \<longrightarrow> e \<le> norm (f y - f x)" if "x \<in> S" for x
+  proof (cases "f ` S - {f x} = {}")
     case True
     with zero_less_numeral show ?thesis
       by (fastforce simp add: Set.image_subset_iff cong: conj_cong)
   next
     case False
-    then obtain z where z: "z \<in> s" "f z \<noteq> f x"
+    then obtain z where z: "z \<in> S" "f z \<noteq> f x"
       by blast
-    have finn: "finite {norm (z - f x) |z. z \<in> f ` s - {f x}}"
+    have finn: "finite {norm (z - f x) |z. z \<in> f ` S - {f x}}"
       using assms by simp
-    then have *: "0 < Inf{norm(z - f x) | z. z \<in> f ` s - {f x}}"
+    then have *: "0 < Inf{norm(z - f x) | z. z \<in> f ` S - {f x}}"
       apply (rule finite_imp_less_Inf)
       using z apply force+
       done
@@ -11123,20 +11163,20 @@
 text\<open>This proof requires the existence of two separate values of the range type.\<close>
 lemma finite_range_constant_imp_connected:
   assumes "\<And>f::'a::topological_space \<Rightarrow> 'b::real_normed_algebra_1.
-              \<lbrakk>continuous_on s f; finite(f ` s)\<rbrakk> \<Longrightarrow> \<exists>a. \<forall>x \<in> s. f x = a"
-    shows "connected s"
+              \<lbrakk>continuous_on S f; finite(f ` S)\<rbrakk> \<Longrightarrow> \<exists>a. \<forall>x \<in> S. f x = a"
+    shows "connected S"
 proof -
   { fix t u
-    assume clt: "closedin (subtopology euclidean s) t"
-       and clu: "closedin (subtopology euclidean s) u"
-       and tue: "t \<inter> u = {}" and tus: "t \<union> u = s"
-    have conif: "continuous_on s (\<lambda>x. if x \<in> t then 0 else 1)"
+    assume clt: "closedin (subtopology euclidean S) t"
+       and clu: "closedin (subtopology euclidean S) u"
+       and tue: "t \<inter> u = {}" and tus: "t \<union> u = S"
+    have conif: "continuous_on S (\<lambda>x. if x \<in> t then 0 else 1)"
       apply (subst tus [symmetric])
       apply (rule continuous_on_cases_local)
       using clt clu tue
       apply (auto simp: tus continuous_on_const)
       done
-    have fi: "finite ((\<lambda>x. if x \<in> t then 0 else 1) ` s)"
+    have fi: "finite ((\<lambda>x. if x \<in> t then 0 else 1) ` S)"
       by (rule finite_subset [of _ "{0,1}"]) auto
     have "t = {} \<or> u = {}"
       using assms [OF conif fi] tus [symmetric]

--- a/src/HOL/Archimedean_Field.thy	Sun Oct 08 16:50:37 2017 +0200
+++ b/src/HOL/Archimedean_Field.thy	Mon Oct 09 15:34:23 2017 +0100
@@ -526,7 +526,8 @@
   shows "finite {k \<in> \<int>. \<bar>k\<bar> \<le> a}" 
   using finite_int_segment [of "-a" a] by (auto simp add: abs_le_iff conj_commute minus_le_iff)
 
-text \<open>Ceiling with numerals.\<close>
+
+subsubsection \<open>Ceiling with numerals.\<close>
 
 lemma ceiling_zero [simp]: "\<lceil>0\<rceil> = 0"
   using ceiling_of_int [of 0] by simp
@@ -595,7 +596,7 @@
   by (simp add: ceiling_altdef)
 
 
-text \<open>Addition and subtraction of integers.\<close>
+subsubsection \<open>Addition and subtraction of integers.\<close>
 
 lemma ceiling_add_of_int [simp]: "\<lceil>x + of_int z\<rceil> = \<lceil>x\<rceil> + z"
   using ceiling_correct [of x] by (simp add: ceiling_def)
@@ -630,6 +631,24 @@
     unfolding of_int_less_iff by simp
 qed
 
+lemma nat_approx_posE:
+  fixes e:: "'a::{archimedean_field,floor_ceiling}"
+  assumes "0 < e"
+  obtains n :: nat where "1 / of_nat(Suc n) < e"
+proof 
+  have "(1::'a) / of_nat (Suc (nat \<lceil>1/e\<rceil>)) < 1 / of_int (\<lceil>1/e\<rceil>)"
+  proof (rule divide_strict_left_mono)
+    show "(of_int \<lceil>1 / e\<rceil>::'a) < of_nat (Suc (nat \<lceil>1 / e\<rceil>))"
+      using assms by (simp add: field_simps)
+    show "(0::'a) < of_nat (Suc (nat \<lceil>1 / e\<rceil>)) * of_int \<lceil>1 / e\<rceil>"
+      using assms by (auto simp: zero_less_mult_iff pos_add_strict)
+  qed auto
+  also have "1 / of_int (\<lceil>1/e\<rceil>) \<le> 1 / (1/e)"
+    by (rule divide_left_mono) (auto simp: \<open>0 < e\<close> ceiling_correct)
+  also have "\<dots> = e" by simp
+  finally show  "1 / of_nat (Suc (nat \<lceil>1 / e\<rceil>)) < e"
+    by metis 
+qed
 
 subsection \<open>Negation\<close>
 

--- a/src/HOL/Complex.thy	Sun Oct 08 16:50:37 2017 +0200
+++ b/src/HOL/Complex.thy	Mon Oct 09 15:34:23 2017 +0100
@@ -1077,7 +1077,7 @@
     and Complex_mult_complex_of_real: "Complex x y * complex_of_real r = Complex (x*r) (y*r)"
     and complex_of_real_mult_Complex: "complex_of_real r * Complex x y = Complex (r*x) (r*y)"
     and complex_eq_cancel_iff2: "(Complex x y = complex_of_real xa) = (x = xa \<and> y = 0)"
-    and complex_cn: "cnj (Complex a b) = Complex a (- b)"
+    and complex_cnj: "cnj (Complex a b) = Complex a (- b)"
     and Complex_sum': "sum (\<lambda>x. Complex (f x) 0) s = Complex (sum f s) 0"
     and Complex_sum: "Complex (sum f s) 0 = sum (\<lambda>x. Complex (f x) 0) s"
     and complex_of_real_def: "complex_of_real r = Complex r 0"

--- a/src/HOL/Limits.thy	Sun Oct 08 16:50:37 2017 +0200
+++ b/src/HOL/Limits.thy	Mon Oct 09 15:34:23 2017 +0100
@@ -820,6 +820,11 @@
 lemmas tendsto_mult_right_zero =
   bounded_bilinear.tendsto_right_zero [OF bounded_bilinear_mult]
 
+lemma tendsto_divide_zero:
+  fixes c :: "'a::real_normed_field"
+  shows "(f \<longlongrightarrow> 0) F \<Longrightarrow> ((\<lambda>x. f x / c) \<longlongrightarrow> 0) F"
+  by (cases "c=0") (simp_all add: divide_inverse tendsto_mult_left_zero)
+
 lemma tendsto_power [tendsto_intros]: "(f \<longlongrightarrow> a) F \<Longrightarrow> ((\<lambda>x. f x ^ n) \<longlongrightarrow> a ^ n) F"
   for f :: "'a \<Rightarrow> 'b::{power,real_normed_algebra}"
   by (induct n) (simp_all add: tendsto_mult)

--- a/src/HOL/Real.thy	Sun Oct 08 16:50:37 2017 +0200
+++ b/src/HOL/Real.thy	Mon Oct 09 15:34:23 2017 +0100
@@ -23,6 +23,11 @@
 
 subsection \<open>Preliminary lemmas\<close>
 
+text{*Useful in convergence arguments*}
+lemma inverse_of_nat_le:
+  fixes n::nat shows "\<lbrakk>n \<le> m; n\<noteq>0\<rbrakk> \<Longrightarrow> 1 / of_nat m \<le> (1::'a::linordered_field) / of_nat n"
+  by (simp add: frac_le)
+
 lemma inj_add_left [simp]: "inj (op + x)"
   for x :: "'a::cancel_semigroup_add"
   by (meson add_left_imp_eq injI)

--- a/src/HOL/Real_Vector_Spaces.thy	Sun Oct 08 16:50:37 2017 +0200
+++ b/src/HOL/Real_Vector_Spaces.thy	Mon Oct 09 15:34:23 2017 +0100
@@ -1469,17 +1469,14 @@
 begin
 
 lemma pos_bounded: "\<exists>K>0. \<forall>a b. norm (a ** b) \<le> norm a * norm b * K"
-  apply (insert bounded)
-  apply (erule exE)
-  apply (rule_tac x="max 1 K" in exI)
-  apply safe
-   apply (rule order_less_le_trans [OF zero_less_one max.cobounded1])
-  apply (drule spec)
-  apply (drule spec)
-  apply (erule order_trans)
-  apply (rule mult_left_mono [OF max.cobounded2])
-  apply (intro mult_nonneg_nonneg norm_ge_zero)
-  done
+proof -
+  obtain K where "\<And>a b. norm (a ** b) \<le> norm a * norm b * K"
+    using bounded by blast
+  then have "norm (a ** b) \<le> norm a * norm b * (max 1 K)" for a b
+    by (rule order.trans) (simp add: mult_left_mono)
+  then show ?thesis
+    by force
+qed
 
 lemma nonneg_bounded: "\<exists>K\<ge>0. \<forall>a b. norm (a ** b) \<le> norm a * norm b * K"
   using pos_bounded by (auto intro: order_less_imp_le)

--- a/src/HOL/Rings.thy	Sun Oct 08 16:50:37 2017 +0200
+++ b/src/HOL/Rings.thy	Mon Oct 09 15:34:23 2017 +0100
@@ -2241,6 +2241,10 @@
 lemma minus_less_iff_1 [simp, no_atp]: "- a < 1 \<longleftrightarrow> - 1 < a"
   by (fact minus_less_iff)
 
+lemma add_less_zeroD:
+  shows "x+y < 0 \<Longrightarrow> x<0 \<or> y<0"
+  by (auto simp: not_less intro: le_less_trans [of _ "x+y"])
+
 end
 
 text \<open>Simprules for comparisons where common factors can be cancelled.\<close>