new material about connectedness, etc.
authorpaulson <lp15@cam.ac.uk>
Mon Oct 09 15:34:23 2017 +0100 (19 months ago)
changeset 66793deabce3ccf1f
parent 66792 6b76a5d1b7a5
child 66794 83bf64da6938
new material about connectedness, etc.
src/HOL/Analysis/Cauchy_Integral_Theorem.thy
src/HOL/Analysis/Complex_Transcendental.thy
src/HOL/Analysis/Conformal_Mappings.thy
src/HOL/Analysis/Convex_Euclidean_Space.thy
src/HOL/Analysis/Henstock_Kurzweil_Integration.thy
src/HOL/Analysis/Path_Connected.thy
src/HOL/Analysis/Starlike.thy
src/HOL/Analysis/Topology_Euclidean_Space.thy
src/HOL/Archimedean_Field.thy
src/HOL/Complex.thy
src/HOL/Limits.thy
src/HOL/Real.thy
src/HOL/Real_Vector_Spaces.thy
src/HOL/Rings.thy
     1.1 --- a/src/HOL/Analysis/Cauchy_Integral_Theorem.thy	Sun Oct 08 16:50:37 2017 +0200
     1.2 +++ b/src/HOL/Analysis/Cauchy_Integral_Theorem.thy	Mon Oct 09 15:34:23 2017 +0100
     1.3 @@ -180,7 +180,7 @@
     1.4          have "f differentiable at x within ({a<..<c} - s)"
     1.5            apply (rule differentiable_at_withinI)
     1.6            using x le st
     1.7 -          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)
     1.8 +          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)
     1.9          moreover have "open ({a<..<c} - s)"
    1.10            by (blast intro: open_greaterThanLessThan \<open>finite s\<close> finite_imp_closed)
    1.11          ultimately show "f differentiable at x within {a..b}"
    1.12 @@ -192,7 +192,7 @@
    1.13          have "g differentiable at x within ({c<..<b} - t)"
    1.14            apply (rule differentiable_at_withinI)
    1.15            using x ge st
    1.16 -          by (metis DiffD1 DiffD2 DiffI UnCI atLeastAtMost_diff_ends atLeastAtMost_iff at_within_interior insert_iff interior_atLeastAtMost)
    1.17 +          by (metis DiffD1 DiffD2 DiffI UnCI atLeastAtMost_diff_ends atLeastAtMost_iff at_within_interior insert_iff interior_atLeastAtMost_real)
    1.18          moreover have "open ({c<..<b} - t)"
    1.19            by (blast intro: open_greaterThanLessThan \<open>finite t\<close> finite_imp_closed)
    1.20          ultimately show "g differentiable at x within {a..b}"
    1.21 @@ -1446,7 +1446,7 @@
    1.22    show ?thesis
    1.23      apply (rule fundamental_theorem_of_calculus_interior_strong)
    1.24      using k assms cfg *
    1.25 -    apply (auto simp: at_within_closed_interval)
    1.26 +    apply (auto simp: at_within_Icc_at)
    1.27      done
    1.28  qed
    1.29  
    1.30 @@ -4158,7 +4158,7 @@
    1.31  
    1.32  subsection\<open>Winding number is zero "outside" a curve, in various senses\<close>
    1.33  
    1.34 -lemma winding_number_zero_in_outside:
    1.35 +proposition winding_number_zero_in_outside:
    1.36    assumes \<gamma>: "path \<gamma>" and loop: "pathfinish \<gamma> = pathstart \<gamma>" and z: "z \<in> outside (path_image \<gamma>)"
    1.37      shows "winding_number \<gamma> z = 0"
    1.38  proof -
    1.39 @@ -4210,7 +4210,11 @@
    1.40    finally show ?thesis .
    1.41  qed
    1.42  
    1.43 -lemma winding_number_zero_outside:
    1.44 +corollary winding_number_zero_const: "a \<noteq> z \<Longrightarrow> winding_number (\<lambda>t. a) z = 0"
    1.45 +  by (rule winding_number_zero_in_outside)
    1.46 +     (auto simp: pathfinish_def pathstart_def path_polynomial_function)
    1.47 +
    1.48 +corollary winding_number_zero_outside:
    1.49      "\<lbrakk>path \<gamma>; convex s; pathfinish \<gamma> = pathstart \<gamma>; z \<notin> s; path_image \<gamma> \<subseteq> s\<rbrakk> \<Longrightarrow> winding_number \<gamma> z = 0"
    1.50    by (meson convex_in_outside outside_mono subsetCE winding_number_zero_in_outside)
    1.51  
     2.1 --- a/src/HOL/Analysis/Complex_Transcendental.thy	Sun Oct 08 16:50:37 2017 +0200
     2.2 +++ b/src/HOL/Analysis/Complex_Transcendental.thy	Mon Oct 09 15:34:23 2017 +0100
     2.3 @@ -1233,7 +1233,7 @@
     2.4  lemma continuous_on_Ln [continuous_intros]: "(\<And>z. z \<in> s \<Longrightarrow> z \<notin> \<real>\<^sub>\<le>\<^sub>0) \<Longrightarrow> continuous_on s Ln"
     2.5    by (simp add: continuous_at_imp_continuous_on continuous_within_Ln)
     2.6  
     2.7 -lemma holomorphic_on_Ln: "(\<And>z. z \<in> s \<Longrightarrow> z \<notin> \<real>\<^sub>\<le>\<^sub>0) \<Longrightarrow> Ln holomorphic_on s"
     2.8 +lemma holomorphic_on_Ln [holomorphic_intros]: "(\<And>z. z \<in> s \<Longrightarrow> z \<notin> \<real>\<^sub>\<le>\<^sub>0) \<Longrightarrow> Ln holomorphic_on s"
     2.9    by (simp add: field_differentiable_within_Ln holomorphic_on_def)
    2.10  
    2.11  lemma divide_ln_mono:
     3.1 --- a/src/HOL/Analysis/Conformal_Mappings.thy	Sun Oct 08 16:50:37 2017 +0200
     3.2 +++ b/src/HOL/Analysis/Conformal_Mappings.thy	Mon Oct 09 15:34:23 2017 +0100
     3.3 @@ -1454,6 +1454,15 @@
     3.4    qed
     3.5  qed
     3.6  
     3.7 +corollary Schwarz_Lemma':
     3.8 +  assumes holf: "f holomorphic_on (ball 0 1)" and [simp]: "f 0 = 0"
     3.9 +      and no: "\<And>z. norm z < 1 \<Longrightarrow> norm (f z) < 1"
    3.10 +    shows "((\<forall>\<xi>. norm \<xi> < 1 \<longrightarrow> norm (f \<xi>) \<le> norm \<xi>) \<and> norm(deriv f 0) \<le> 1) \<and>
    3.11 +           (((\<exists>z. norm z < 1 \<and> z \<noteq> 0 \<and> norm(f z) = norm z) \<or> norm(deriv f 0) = 1)
    3.12 +           \<longrightarrow> (\<exists>\<alpha>. (\<forall>z. norm z < 1 \<longrightarrow> f z = \<alpha> * z) \<and> norm \<alpha> = 1))"
    3.13 +  using Schwarz_Lemma [OF assms]
    3.14 +  by (metis (no_types) norm_eq_zero zero_less_one)
    3.15 +
    3.16  subsection\<open>The Schwarz reflection principle\<close>
    3.17  
    3.18  lemma hol_pal_lem0:
     4.1 --- a/src/HOL/Analysis/Convex_Euclidean_Space.thy	Sun Oct 08 16:50:37 2017 +0200
     4.2 +++ b/src/HOL/Analysis/Convex_Euclidean_Space.thy	Mon Oct 09 15:34:23 2017 +0100
     4.3 @@ -4696,6 +4696,15 @@
     4.4    finally show ?thesis .
     4.5  qed
     4.6  
     4.7 +lemma interior_atLeastLessThan [simp]:
     4.8 +  fixes a::real shows "interior {a..<b} = {a<..<b}"
     4.9 +  by (metis atLeastLessThan_def greaterThanLessThan_def interior_atLeastAtMost_real interior_Int interior_interior interior_real_semiline)
    4.10 +
    4.11 +lemma interior_lessThanAtMost [simp]:
    4.12 +  fixes a::real shows "interior {a<..b} = {a<..<b}"
    4.13 +  by (metis atLeastAtMost_def greaterThanAtMost_def interior_atLeastAtMost_real interior_Int
    4.14 +            interior_interior interior_real_semiline)
    4.15 +
    4.16  lemma interior_greaterThanLessThan_real [simp]: "interior {a<..<b} = {a<..<b :: real}"
    4.17    by (metis interior_atLeastAtMost_real interior_interior)
    4.18  
     5.1 --- a/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy	Sun Oct 08 16:50:37 2017 +0200
     5.2 +++ b/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy	Mon Oct 09 15:34:23 2017 +0100
     5.3 @@ -6467,7 +6467,7 @@
     5.4    qed
     5.5    have deriv: "(?F has_vector_derivative g' x *\<^sub>R f (g x))
     5.6                    (at x)" if "x \<in> {a..b} - (s \<union> {a,b})" for x
     5.7 -    using deriv[of x] that by (simp add: at_within_closed_interval o_def)
     5.8 +    using deriv[of x] that by (simp add: at_within_Icc_at o_def)
     5.9    have "((\<lambda>x. g' x *\<^sub>R f (g x)) has_integral (?F b - ?F a)) {a..b}"
    5.10      using le cont_int s deriv cont_int
    5.11      by (intro fundamental_theorem_of_calculus_interior_strong[of "s \<union> {a,b}"]) simp_all
     6.1 --- a/src/HOL/Analysis/Path_Connected.thy	Sun Oct 08 16:50:37 2017 +0200
     6.2 +++ b/src/HOL/Analysis/Path_Connected.thy	Mon Oct 09 15:34:23 2017 +0100
     6.3 @@ -166,6 +166,9 @@
     6.4  lemma simple_path_eq_arc: "pathfinish g \<noteq> pathstart g \<Longrightarrow> (simple_path g = arc g)"
     6.5    by (simp add: arc_simple_path)
     6.6  
     6.7 +lemma path_image_const [simp]: "path_image (\<lambda>t. a) = {a}"
     6.8 +  by (force simp: path_image_def)
     6.9 +
    6.10  lemma path_image_nonempty [simp]: "path_image g \<noteq> {}"
    6.11    unfolding path_image_def image_is_empty box_eq_empty
    6.12    by auto
    6.13 @@ -1511,13 +1514,7 @@
    6.14    assumes "convex s"
    6.15    shows "path_connected s"
    6.16    unfolding path_connected_def
    6.17 -  apply rule
    6.18 -  apply rule
    6.19 -  apply (rule_tac x = "linepath x y" in exI)
    6.20 -  unfolding path_image_linepath
    6.21 -  using assms [unfolded convex_contains_segment]
    6.22 -  apply auto
    6.23 -  done
    6.24 +  using assms convex_contains_segment by fastforce
    6.25  
    6.26  lemma path_connected_UNIV [iff]: "path_connected (UNIV :: 'a::real_normed_vector set)"
    6.27    by (simp add: convex_imp_path_connected)
    6.28 @@ -1528,13 +1525,7 @@
    6.29  lemma path_connected_imp_connected:
    6.30    assumes "path_connected S"
    6.31    shows "connected S"
    6.32 -  unfolding connected_def not_ex
    6.33 -  apply rule
    6.34 -  apply rule
    6.35 -  apply (rule ccontr)
    6.36 -  unfolding not_not
    6.37 -  apply (elim conjE)
    6.38 -proof -
    6.39 +proof (rule connectedI)
    6.40    fix e1 e2
    6.41    assume as: "open e1" "open e2" "S \<subseteq> e1 \<union> e2" "e1 \<inter> e2 \<inter> S = {}" "e1 \<inter> S \<noteq> {}" "e2 \<inter> S \<noteq> {}"
    6.42    then obtain x1 x2 where obt:"x1 \<in> e1 \<inter> S" "x2 \<in> e2 \<inter> S"
    6.43 @@ -1570,31 +1561,14 @@
    6.44    fix y
    6.45    assume as: "y \<in> path_component_set S x"
    6.46    then have "y \<in> S"
    6.47 -    apply -
    6.48 -    apply (rule path_component_mem(2))
    6.49 -    unfolding mem_Collect_eq
    6.50 -    apply auto
    6.51 -    done
    6.52 +    by (simp add: path_component_mem(2))
    6.53    then obtain e where e: "e > 0" "ball y e \<subseteq> S"
    6.54      using assms[unfolded open_contains_ball]
    6.55      by auto
    6.56 -  show "\<exists>e > 0. ball y e \<subseteq> path_component_set S x"
    6.57 -    apply (rule_tac x=e in exI)
    6.58 -    apply (rule,rule \<open>e>0\<close>)
    6.59 -    apply rule
    6.60 -    unfolding mem_ball mem_Collect_eq
    6.61 -  proof -
    6.62 -    fix z
    6.63 -    assume "dist y z < e"
    6.64 -    then show "path_component S x z"
    6.65 -      apply (rule_tac path_component_trans[of _ _ y])
    6.66 -      defer
    6.67 -      apply (rule path_component_of_subset[OF e(2)])
    6.68 -      apply (rule convex_imp_path_connected[OF convex_ball, unfolded path_connected_component, rule_format])
    6.69 -      using \<open>e > 0\<close> as
    6.70 -      apply auto
    6.71 -      done
    6.72 -  qed
    6.73 +have "\<And>u. dist y u < e \<Longrightarrow> path_component S x u"
    6.74 +      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)
    6.75 +  then show "\<exists>e > 0. ball y e \<subseteq> path_component_set S x"
    6.76 +    using \<open>e>0\<close> by auto
    6.77  qed
    6.78  
    6.79  lemma open_non_path_component:
    6.80 @@ -1904,6 +1878,8 @@
    6.81  using is_interval_connected_1 is_interval_path_connected path_connected_imp_connected by blast
    6.82  
    6.83  
    6.84 +subsection\<open>Path components\<close>
    6.85 +
    6.86  lemma Union_path_component [simp]:
    6.87     "Union {path_component_set S x |x. x \<in> S} = S"
    6.88  apply (rule subset_antisym)
    6.89 @@ -2151,7 +2127,6 @@
    6.90      by (auto simp: path_connected_component)
    6.91  qed
    6.92  
    6.93 -
    6.94  lemma connected_complement_bounded_convex:
    6.95      fixes s :: "'a :: euclidean_space set"
    6.96      assumes "bounded s" "convex s" "2 \<le> DIM('a)"
    6.97 @@ -2300,6 +2275,65 @@
    6.98  qed
    6.99  
   6.100  
   6.101 +subsection\<open>Every annulus is a connected set\<close>
   6.102 +
   6.103 +lemma path_connected_2DIM_I:
   6.104 +  fixes a :: "'N::euclidean_space"
   6.105 +  assumes 2: "2 \<le> DIM('N)" and pc: "path_connected {r. 0 \<le> r \<and> P r}"
   6.106 +  shows "path_connected {x. P(norm(x - a))}"
   6.107 +proof -
   6.108 +  have "{x. P(norm(x - a))} = op+a ` {x. P(norm x)}"
   6.109 +    by force
   6.110 +  moreover have "path_connected {x::'N. P(norm x)}"
   6.111 +  proof -
   6.112 +    let ?D = "{x. 0 \<le> x \<and> P x} \<times> sphere (0::'N) 1"
   6.113 +    have "x \<in> (\<lambda>z. fst z *\<^sub>R snd z) ` ?D"
   6.114 +      if "P (norm x)" for x::'N
   6.115 +    proof (cases "x=0")
   6.116 +      case True
   6.117 +      with that show ?thesis
   6.118 +        apply (simp add: image_iff)
   6.119 +        apply (rule_tac x=0 in exI, simp)
   6.120 +        using vector_choose_size zero_le_one by blast
   6.121 +    next
   6.122 +      case False
   6.123 +      with that show ?thesis
   6.124 +        by (rule_tac x="(norm x, x /\<^sub>R norm x)" in image_eqI) auto
   6.125 +    qed
   6.126 +    then have *: "{x::'N. P(norm x)} =  (\<lambda>z. fst z *\<^sub>R snd z) ` ?D"
   6.127 +      by auto
   6.128 +    have "continuous_on ?D (\<lambda>z:: real\<times>'N. fst z *\<^sub>R snd z)"
   6.129 +      by (intro continuous_intros)
   6.130 +    moreover have "path_connected ?D"
   6.131 +      by (metis path_connected_Times [OF pc] path_connected_sphere 2)
   6.132 +    ultimately show ?thesis
   6.133 +      apply (subst *)
   6.134 +      apply (rule path_connected_continuous_image, auto)
   6.135 +      done
   6.136 +  qed
   6.137 +  ultimately show ?thesis
   6.138 +    using path_connected_translation by metis
   6.139 +qed
   6.140 +
   6.141 +lemma path_connected_annulus:
   6.142 +  fixes a :: "'N::euclidean_space"
   6.143 +  assumes "2 \<le> DIM('N)"
   6.144 +  shows "path_connected {x. r1 < norm(x - a) \<and> norm(x - a) < r2}"
   6.145 +        "path_connected {x. r1 < norm(x - a) \<and> norm(x - a) \<le> r2}"
   6.146 +        "path_connected {x. r1 \<le> norm(x - a) \<and> norm(x - a) < r2}"
   6.147 +        "path_connected {x. r1 \<le> norm(x - a) \<and> norm(x - a) \<le> r2}"
   6.148 +  by (auto simp: is_interval_def intro!: is_interval_convex convex_imp_path_connected path_connected_2DIM_I [OF assms])
   6.149 +
   6.150 +lemma connected_annulus:
   6.151 +  fixes a :: "'N::euclidean_space"
   6.152 +  assumes "2 \<le> DIM('N::euclidean_space)"
   6.153 +  shows "connected {x. r1 < norm(x - a) \<and> norm(x - a) < r2}"
   6.154 +        "connected {x. r1 < norm(x - a) \<and> norm(x - a) \<le> r2}"
   6.155 +        "connected {x. r1 \<le> norm(x - a) \<and> norm(x - a) < r2}"
   6.156 +        "connected {x. r1 \<le> norm(x - a) \<and> norm(x - a) \<le> r2}"
   6.157 +  by (auto simp: path_connected_annulus [OF assms] path_connected_imp_connected)
   6.158 +
   6.159 +
   6.160  subsection\<open>Relations between components and path components\<close>
   6.161  
   6.162  lemma open_connected_component:
   6.163 @@ -2894,11 +2928,21 @@
   6.164      shows "outside s = - s"
   6.165    by (metis ComplD assms convex_in_outside equalityI inside_Un_outside subsetI sup.cobounded2)
   6.166  
   6.167 +lemma outside_singleton [simp]:
   6.168 +  fixes x :: "'a :: {real_normed_vector, perfect_space}"
   6.169 +  shows "outside {x} = -{x}"
   6.170 +  by (auto simp: outside_convex)
   6.171 +
   6.172  lemma inside_convex:
   6.173    fixes s :: "'a :: {real_normed_vector, perfect_space} set"
   6.174    shows "convex s \<Longrightarrow> inside s = {}"
   6.175    by (simp add: inside_outside outside_convex)
   6.176  
   6.177 +lemma inside_singleton [simp]:
   6.178 +  fixes x :: "'a :: {real_normed_vector, perfect_space}"
   6.179 +  shows "inside {x} = {}"
   6.180 +  by (auto simp: inside_convex)
   6.181 +
   6.182  lemma outside_subset_convex:
   6.183    fixes s :: "'a :: {real_normed_vector, perfect_space} set"
   6.184    shows "\<lbrakk>convex t; s \<subseteq> t\<rbrakk> \<Longrightarrow> - t \<subseteq> outside s"
   6.185 @@ -4119,6 +4163,39 @@
   6.186      by (blast intro: homotopic_loops_trans)
   6.187  qed
   6.188  
   6.189 +lemma homotopic_paths_loop_parts:
   6.190 +  assumes loops: "homotopic_loops S (p +++ reversepath q) (linepath a a)" and "path q"
   6.191 +  shows "homotopic_paths S p q"
   6.192 +proof -
   6.193 +  have paths: "homotopic_paths S (p +++ reversepath q) (linepath (pathstart p) (pathstart p))"
   6.194 +    using homotopic_loops_imp_homotopic_paths_null [OF loops] by simp
   6.195 +  then have "path p"
   6.196 +    using \<open>path q\<close> homotopic_loops_imp_path loops path_join path_join_path_ends path_reversepath by blast
   6.197 +  show ?thesis
   6.198 +  proof (cases "pathfinish p = pathfinish q")
   6.199 +    case True
   6.200 +    have pipq: "path_image p \<subseteq> S" "path_image q \<subseteq> S"
   6.201 +      by (metis Un_subset_iff paths \<open>path p\<close> \<open>path q\<close> homotopic_loops_imp_subset homotopic_paths_imp_path loops
   6.202 +           path_image_join path_image_reversepath path_imp_reversepath path_join_eq)+
   6.203 +    have "homotopic_paths S p (p +++ (linepath (pathfinish p) (pathfinish p)))"
   6.204 +      using \<open>path p\<close> \<open>path_image p \<subseteq> S\<close> homotopic_paths_rid homotopic_paths_sym by blast
   6.205 +    moreover have "homotopic_paths S (p +++ (linepath (pathfinish p) (pathfinish p))) (p +++ (reversepath q +++ q))"
   6.206 +      by (simp add: True \<open>path p\<close> \<open>path q\<close> pipq homotopic_paths_join homotopic_paths_linv homotopic_paths_sym)
   6.207 +    moreover have "homotopic_paths S (p +++ (reversepath q +++ q)) ((p +++ reversepath q) +++ q)"
   6.208 +      by (simp add: True \<open>path p\<close> \<open>path q\<close> homotopic_paths_assoc pipq)
   6.209 +    moreover have "homotopic_paths S ((p +++ reversepath q) +++ q) (linepath (pathstart p) (pathstart p) +++ q)"
   6.210 +      by (simp add: \<open>path q\<close> homotopic_paths_join paths pipq)
   6.211 +    moreover then have "homotopic_paths S (linepath (pathstart p) (pathstart p) +++ q) q"
   6.212 +      by (metis \<open>path q\<close> homotopic_paths_imp_path homotopic_paths_lid linepath_trivial path_join_path_ends pathfinish_def pipq(2))
   6.213 +    ultimately show ?thesis
   6.214 +      using homotopic_paths_trans by metis
   6.215 +  next
   6.216 +    case False
   6.217 +    then show ?thesis
   6.218 +      using \<open>path q\<close> homotopic_loops_imp_path loops path_join_path_ends by fastforce
   6.219 +  qed
   6.220 +qed
   6.221 +
   6.222  
   6.223  subsection\<open> Homotopy of "nearby" function, paths and loops.\<close>
   6.224  
     7.1 --- a/src/HOL/Analysis/Starlike.thy	Sun Oct 08 16:50:37 2017 +0200
     7.2 +++ b/src/HOL/Analysis/Starlike.thy	Mon Oct 09 15:34:23 2017 +0100
     7.3 @@ -3776,24 +3776,6 @@
     7.4  
     7.5  subsection\<open>Explicit formulas for interior and relative interior of convex hull\<close>
     7.6  
     7.7 -lemma interior_atLeastAtMost [simp]:
     7.8 -  fixes a::real shows "interior {a..b} = {a<..<b}"
     7.9 -  using interior_cbox [of a b] by auto
    7.10 -
    7.11 -lemma interior_atLeastLessThan [simp]:
    7.12 -  fixes a::real shows "interior {a..<b} = {a<..<b}"
    7.13 -  by (metis atLeastLessThan_def greaterThanLessThan_def interior_atLeastAtMost interior_Int interior_interior interior_real_semiline)
    7.14 -
    7.15 -lemma interior_lessThanAtMost [simp]:
    7.16 -  fixes a::real shows "interior {a<..b} = {a<..<b}"
    7.17 -  by (metis atLeastAtMost_def greaterThanAtMost_def interior_atLeastAtMost interior_Int
    7.18 -            interior_interior interior_real_semiline)
    7.19 -
    7.20 -lemma at_within_closed_interval:
    7.21 -    fixes x::real
    7.22 -    shows "a < x \<Longrightarrow> x < b \<Longrightarrow> (at x within {a..b}) = at x"
    7.23 -  by (metis at_within_interior greaterThanLessThan_iff interior_atLeastAtMost)
    7.24 -
    7.25  lemma at_within_cbox_finite:
    7.26    assumes "x \<in> box a b" "x \<notin> S" "finite S"
    7.27    shows "(at x within cbox a b - S) = at x"
    7.28 @@ -5087,7 +5069,6 @@
    7.29  using separation_closures [of S T]
    7.30  by (metis assms closure_closed disjnt_def inf_commute)
    7.31  
    7.32 -
    7.33  lemma separation_normal_local:
    7.34    fixes S :: "'a::euclidean_space set"
    7.35    assumes US: "closedin (subtopology euclidean U) S"
    7.36 @@ -5147,6 +5128,139 @@
    7.37      by auto (meson bounded_ball bounded_subset compl_le_swap2 disjoint_eq_subset_Compl)
    7.38  qed
    7.39  
    7.40 +subsection\<open>Connectedness of the intersection of a chain\<close>
    7.41 +
    7.42 +proposition connected_chain:
    7.43 +  fixes \<F> :: "'a :: euclidean_space set set"
    7.44 +  assumes cc: "\<And>S. S \<in> \<F> \<Longrightarrow> compact S \<and> connected S"
    7.45 +      and linear: "\<And>S T. S \<in> \<F> \<and> T \<in> \<F> \<Longrightarrow> S \<subseteq> T \<or> T \<subseteq> S"
    7.46 +  shows "connected(\<Inter>\<F>)"
    7.47 +proof (cases "\<F> = {}")
    7.48 +  case True then show ?thesis
    7.49 +    by auto
    7.50 +next
    7.51 +  case False
    7.52 +  then have cf: "compact(\<Inter>\<F>)"
    7.53 +    by (simp add: cc compact_Inter)
    7.54 +  have False if AB: "closed A" "closed B" "A \<inter> B = {}"
    7.55 +                and ABeq: "A \<union> B = \<Inter>\<F>" and "A \<noteq> {}" "B \<noteq> {}" for A B
    7.56 +  proof -
    7.57 +    obtain U V where "open U" "open V" "A \<subseteq> U" "B \<subseteq> V" "U \<inter> V = {}"
    7.58 +      using separation_normal [OF AB] by metis
    7.59 +    obtain K where "K \<in> \<F>" "compact K"
    7.60 +      using cc False by blast
    7.61 +    then obtain N where "open N" and "K \<subseteq> N"
    7.62 +      by blast
    7.63 +    let ?\<C> = "insert (U \<union> V) ((\<lambda>S. N - S) ` \<F>)"
    7.64 +    obtain \<D> where "\<D> \<subseteq> ?\<C>" "finite \<D>" "K \<subseteq> \<Union>\<D>"
    7.65 +    proof (rule compactE [OF \<open>compact K\<close>])
    7.66 +      show "K \<subseteq> \<Union>insert (U \<union> V) (op - N ` \<F>)"
    7.67 +        using \<open>K \<subseteq> N\<close> ABeq \<open>A \<subseteq> U\<close> \<open>B \<subseteq> V\<close> by auto
    7.68 +      show "\<And>B. B \<in> insert (U \<union> V) (op - N ` \<F>) \<Longrightarrow> open B"
    7.69 +        by (auto simp:  \<open>open U\<close> \<open>open V\<close> open_Un \<open>open N\<close> cc compact_imp_closed open_Diff)
    7.70 +    qed
    7.71 +    then have "finite(\<D> - {U \<union> V})"
    7.72 +      by blast
    7.73 +    moreover have "\<D> - {U \<union> V} \<subseteq> (\<lambda>S. N - S) ` \<F>"
    7.74 +      using \<open>\<D> \<subseteq> ?\<C>\<close> by blast
    7.75 +    ultimately obtain \<G> where "\<G> \<subseteq> \<F>" "finite \<G>" and Deq: "\<D> - {U \<union> V} = (\<lambda>S. N-S) ` \<G>"
    7.76 +      using finite_subset_image by metis
    7.77 +    obtain J where "J \<in> \<F>" and J: "(\<Union>S\<in>\<G>. N - S) \<subseteq> N - J"
    7.78 +    proof (cases "\<G> = {}")
    7.79 +      case True
    7.80 +      with \<open>\<F> \<noteq> {}\<close> that show ?thesis
    7.81 +        by auto
    7.82 +    next
    7.83 +      case False
    7.84 +      have "\<And>S T. \<lbrakk>S \<in> \<G>; T \<in> \<G>\<rbrakk> \<Longrightarrow> S \<subseteq> T \<or> T \<subseteq> S"
    7.85 +        by (meson \<open>\<G> \<subseteq> \<F>\<close> in_mono local.linear)
    7.86 +      with \<open>finite \<G>\<close> \<open>\<G> \<noteq> {}\<close>
    7.87 +      have "\<exists>J \<in> \<G>. (\<Union>S\<in>\<G>. N - S) \<subseteq> N - J"
    7.88 +      proof induction
    7.89 +        case (insert X \<H>)
    7.90 +        show ?case
    7.91 +        proof (cases "\<H> = {}")
    7.92 +          case True then show ?thesis by auto
    7.93 +        next
    7.94 +          case False
    7.95 +          then have "\<And>S T. \<lbrakk>S \<in> \<H>; T \<in> \<H>\<rbrakk> \<Longrightarrow> S \<subseteq> T \<or> T \<subseteq> S"
    7.96 +            by (simp add: insert.prems)
    7.97 +          with insert.IH False obtain J where "J \<in> \<H>" and J: "(\<Union>Y\<in>\<H>. N - Y) \<subseteq> N - J"
    7.98 +            by metis
    7.99 +          have "N - J \<subseteq> N - X \<or> N - X \<subseteq> N - J"
   7.100 +            by (meson Diff_mono \<open>J \<in> \<H>\<close> insert.prems(2) insert_iff order_refl)
   7.101 +          then show ?thesis
   7.102 +          proof
   7.103 +            assume "N - J \<subseteq> N - X" with J show ?thesis
   7.104 +              by auto
   7.105 +          next
   7.106 +            assume "N - X \<subseteq> N - J"
   7.107 +            with J have "N - X \<union> UNION \<H> (op - N) \<subseteq> N - J"
   7.108 +              by auto
   7.109 +            with \<open>J \<in> \<H>\<close> show ?thesis
   7.110 +              by blast
   7.111 +          qed
   7.112 +        qed
   7.113 +      qed simp
   7.114 +      with \<open>\<G> \<subseteq> \<F>\<close> show ?thesis by (blast intro: that)
   7.115 +    qed
   7.116 +    have "K \<subseteq> \<Union>(insert (U \<union> V) (\<D> - {U \<union> V}))"
   7.117 +      using \<open>K \<subseteq> \<Union>\<D>\<close> by auto
   7.118 +    also have "... \<subseteq> (U \<union> V) \<union> (N - J)"
   7.119 +      by (metis (no_types, hide_lams) Deq Un_subset_iff Un_upper2 J Union_insert order_trans sup_ge1)
   7.120 +    finally have "J \<inter> K \<subseteq> U \<union> V"
   7.121 +      by blast
   7.122 +    moreover have "connected(J \<inter> K)"
   7.123 +      by (metis Int_absorb1 \<open>J \<in> \<F>\<close> \<open>K \<in> \<F>\<close> cc inf.orderE local.linear)
   7.124 +    moreover have "U \<inter> (J \<inter> K) \<noteq> {}"
   7.125 +      using ABeq \<open>J \<in> \<F>\<close> \<open>K \<in> \<F>\<close> \<open>A \<noteq> {}\<close> \<open>A \<subseteq> U\<close> by blast
   7.126 +    moreover have "V \<inter> (J \<inter> K) \<noteq> {}"
   7.127 +      using ABeq \<open>J \<in> \<F>\<close> \<open>K \<in> \<F>\<close> \<open>B \<noteq> {}\<close> \<open>B \<subseteq> V\<close> by blast
   7.128 +    ultimately show False
   7.129 +        using connectedD [of "J \<inter> K" U V] \<open>open U\<close> \<open>open V\<close> \<open>U \<inter> V = {}\<close>  by auto
   7.130 +  qed
   7.131 +  with cf show ?thesis
   7.132 +    by (auto simp: connected_closed_set compact_imp_closed)
   7.133 +qed
   7.134 +
   7.135 +lemma connected_chain_gen:
   7.136 +  fixes \<F> :: "'a :: euclidean_space set set"
   7.137 +  assumes X: "X \<in> \<F>" "compact X"
   7.138 +      and cc: "\<And>T. T \<in> \<F> \<Longrightarrow> closed T \<and> connected T"
   7.139 +      and linear: "\<And>S T. S \<in> \<F> \<and> T \<in> \<F> \<Longrightarrow> S \<subseteq> T \<or> T \<subseteq> S"
   7.140 +  shows "connected(\<Inter>\<F>)"
   7.141 +proof -
   7.142 +  have "\<Inter>\<F> = (\<Inter>T\<in>\<F>. X \<inter> T)"
   7.143 +    using X by blast
   7.144 +  moreover have "connected (\<Inter>T\<in>\<F>. X \<inter> T)"
   7.145 +  proof (rule connected_chain)
   7.146 +    show "\<And>T. T \<in> op \<inter> X ` \<F> \<Longrightarrow> compact T \<and> connected T"
   7.147 +      using cc X by auto (metis inf.absorb2 inf.orderE local.linear)
   7.148 +    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"
   7.149 +      using local.linear by blast
   7.150 +  qed
   7.151 +  ultimately show ?thesis
   7.152 +    by metis
   7.153 +qed
   7.154 +
   7.155 +lemma connected_nest:
   7.156 +  fixes S :: "'a::linorder \<Rightarrow> 'b::euclidean_space set"
   7.157 +  assumes S: "\<And>n. compact(S n)" "\<And>n. connected(S n)"
   7.158 +    and nest: "\<And>m n. m \<le> n \<Longrightarrow> S n \<subseteq> S m"
   7.159 +  shows "connected(\<Inter> (range S))"
   7.160 +  apply (rule connected_chain)
   7.161 +  using S apply blast
   7.162 +  by (metis image_iff le_cases nest)
   7.163 +
   7.164 +lemma connected_nest_gen:
   7.165 +  fixes S :: "'a::linorder \<Rightarrow> 'b::euclidean_space set"
   7.166 +  assumes S: "\<And>n. closed(S n)" "\<And>n. connected(S n)" "compact(S k)"
   7.167 +    and nest: "\<And>m n. m \<le> n \<Longrightarrow> S n \<subseteq> S m"
   7.168 +  shows "connected(\<Inter> (range S))"
   7.169 +  apply (rule connected_chain_gen [of "S k"])
   7.170 +  using S apply auto
   7.171 +  by (meson le_cases nest subsetCE)
   7.172 +
   7.173  subsection\<open>Proper maps, including projections out of compact sets\<close>
   7.174  
   7.175  lemma finite_indexed_bound:
     8.1 --- a/src/HOL/Analysis/Topology_Euclidean_Space.thy	Sun Oct 08 16:50:37 2017 +0200
     8.2 +++ b/src/HOL/Analysis/Topology_Euclidean_Space.thy	Mon Oct 09 15:34:23 2017 +0100
     8.3 @@ -676,6 +676,10 @@
     8.4      using openin_INT[of _ _ U, OF assms(1) assms(3)] by (simp add: inf.absorb2 inf_commute)
     8.5  qed
     8.6  
     8.7 +lemma openin_Inter [intro]:
     8.8 +  assumes "finite \<F>" "\<F> \<noteq> {}" "\<And>X. X \<in> \<F> \<Longrightarrow> openin T X" shows "openin T (\<Inter>\<F>)"
     8.9 +  by (metis (full_types) assms openin_INT2 image_ident)
    8.10 +
    8.11  
    8.12  subsubsection \<open>Closed sets\<close>
    8.13  
    8.14 @@ -2404,6 +2408,11 @@
    8.15  lemma closedin_closed_eq: "closed S \<Longrightarrow> closedin (subtopology euclidean S) T \<longleftrightarrow> closed T \<and> T \<subseteq> S"
    8.16    by (meson closedin_limpt closed_subset closedin_closed_trans)
    8.17  
    8.18 +lemma connected_closed_set:
    8.19 +   "closed S
    8.20 +    \<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 = {})"
    8.21 +  unfolding connected_closedin_eq closedin_closed_eq connected_closedin_eq by blast
    8.22 +
    8.23  lemma closedin_subset_trans:
    8.24    "closedin (subtopology euclidean U) S \<Longrightarrow> S \<subseteq> T \<Longrightarrow> T \<subseteq> U \<Longrightarrow>
    8.25      closedin (subtopology euclidean T) S"
    8.26 @@ -5407,6 +5416,13 @@
    8.27      by auto
    8.28  qed
    8.29  
    8.30 +lemma compact_Inter:
    8.31 +  fixes \<F> :: "'a :: heine_borel set set"
    8.32 +  assumes com: "\<And>S. S \<in> \<F> \<Longrightarrow> compact S" and "\<F> \<noteq> {}"
    8.33 +  shows "compact(\<Inter> \<F>)"
    8.34 +  using assms
    8.35 +  by (meson Inf_lower all_not_in_conv bounded_subset closed_Inter compact_eq_bounded_closed)
    8.36 +
    8.37  lemma compact_closure [simp]:
    8.38    fixes S :: "'a::heine_borel set"
    8.39    shows "compact(closure S) \<longleftrightarrow> bounded S"
    8.40 @@ -5819,19 +5835,6 @@
    8.41    then show ?thesis unfolding complete_def by auto
    8.42  qed
    8.43  
    8.44 -lemma nat_approx_posE:
    8.45 -  fixes e::real
    8.46 -  assumes "0 < e"
    8.47 -  obtains n :: nat where "1 / (Suc n) < e"
    8.48 -proof atomize_elim
    8.49 -  have "1 / real (Suc (nat \<lceil>1/e\<rceil>)) < 1 / \<lceil>1/e\<rceil>"
    8.50 -    by (rule divide_strict_left_mono) (auto simp: \<open>0 < e\<close>)
    8.51 -  also have "1 / \<lceil>1/e\<rceil> \<le> 1 / (1/e)"
    8.52 -    by (rule divide_left_mono) (auto simp: \<open>0 < e\<close> ceiling_correct)
    8.53 -  also have "\<dots> = e" by simp
    8.54 -  finally show  "\<exists>n. 1 / real (Suc n) < e" ..
    8.55 -qed
    8.56 -
    8.57  lemma compact_eq_totally_bounded:
    8.58    "compact s \<longleftrightarrow> complete s \<and> (\<forall>e>0. \<exists>k. finite k \<and> s \<subseteq> (\<Union>x\<in>k. ball x e))"
    8.59      (is "_ \<longleftrightarrow> ?rhs")
    8.60 @@ -9679,6 +9682,43 @@
    8.61        simp: dist_commute dist_norm pos_divide_less_eq mult_strict_left_mono)
    8.62      done
    8.63  
    8.64 +lemma homeomorphic_ball01_UNIV:
    8.65 +  "ball (0::'a::real_normed_vector) 1 homeomorphic (UNIV:: 'a set)"
    8.66 +  (is "?B homeomorphic ?U")
    8.67 +proof
    8.68 +  have "x \<in> (\<lambda>z. z /\<^sub>R (1 - norm z)) ` ball 0 1" for x::'a
    8.69 +    apply (rule_tac x="x /\<^sub>R (1 + norm x)" in image_eqI)
    8.70 +     apply (auto simp: divide_simps)
    8.71 +    using norm_ge_zero [of x] apply linarith+
    8.72 +    done
    8.73 +  then show "(\<lambda>z::'a. z /\<^sub>R (1 - norm z)) ` ?B = ?U"
    8.74 +    by blast
    8.75 +  have "x \<in> range (\<lambda>z. (1 / (1 + norm z)) *\<^sub>R z)" if "norm x < 1" for x::'a
    8.76 +    apply (rule_tac x="x /\<^sub>R (1 - norm x)" in image_eqI)
    8.77 +    using that apply (auto simp: divide_simps)
    8.78 +    done
    8.79 +  then show "(\<lambda>z::'a. z /\<^sub>R (1 + norm z)) ` ?U = ?B"
    8.80 +    by (force simp: divide_simps dest: add_less_zeroD)
    8.81 +  show "continuous_on (ball 0 1) (\<lambda>z. z /\<^sub>R (1 - norm z))"
    8.82 +    by (rule continuous_intros | force)+
    8.83 +  show "continuous_on UNIV (\<lambda>z. z /\<^sub>R (1 + norm z))"
    8.84 +    apply (intro continuous_intros)
    8.85 +    apply (metis le_add_same_cancel1 norm_ge_zero not_le zero_less_one)
    8.86 +    done
    8.87 +  show "\<And>x. x \<in> ball 0 1 \<Longrightarrow>
    8.88 +         x /\<^sub>R (1 - norm x) /\<^sub>R (1 + norm (x /\<^sub>R (1 - norm x))) = x"
    8.89 +    by (auto simp: divide_simps)
    8.90 +  show "\<And>y. y /\<^sub>R (1 + norm y) /\<^sub>R (1 - norm (y /\<^sub>R (1 + norm y))) = y"
    8.91 +    apply (auto simp: divide_simps)
    8.92 +    apply (metis le_add_same_cancel1 norm_ge_zero not_le zero_less_one)
    8.93 +    done
    8.94 +qed
    8.95 +
    8.96 +proposition homeomorphic_ball_UNIV:
    8.97 +  fixes a ::"'a::real_normed_vector"
    8.98 +  assumes "0 < r" shows "ball a r homeomorphic (UNIV:: 'a set)"
    8.99 +  using assms homeomorphic_ball01_UNIV homeomorphic_balls(1) homeomorphic_trans zero_less_one by blast
   8.100 +
   8.101  subsection\<open>Inverse function property for open/closed maps\<close>
   8.102  
   8.103  lemma continuous_on_inverse_open_map:
   8.104 @@ -10711,7 +10751,7 @@
   8.105    then show ?thesis by blast
   8.106  qed
   8.107  
   8.108 -lemma closed_imp_fip_compact:
   8.109 +lemma clconnected_closedin_eqosed_imp_fip_compact:
   8.110    fixes S :: "'a::heine_borel set"
   8.111    shows
   8.112     "\<lbrakk>closed S; \<And>T. T \<in> \<F> \<Longrightarrow> compact T;
   8.113 @@ -11043,38 +11083,38 @@
   8.114  text\<open>Still missing: versions for a set that is smaller than R, or countable.\<close>
   8.115  
   8.116  lemma continuous_disconnected_range_constant:
   8.117 -  assumes s: "connected s"
   8.118 -      and conf: "continuous_on s f"
   8.119 -      and fim: "f ` s \<subseteq> t"
   8.120 +  assumes S: "connected S"
   8.121 +      and conf: "continuous_on S f"
   8.122 +      and fim: "f ` S \<subseteq> t"
   8.123        and cct: "\<And>y. y \<in> t \<Longrightarrow> connected_component_set t y = {y}"
   8.124 -    shows "\<exists>a. \<forall>x \<in> s. f x = a"
   8.125 -proof (cases "s = {}")
   8.126 +    shows "\<exists>a. \<forall>x \<in> S. f x = a"
   8.127 +proof (cases "S = {}")
   8.128    case True then show ?thesis by force
   8.129  next
   8.130    case False
   8.131 -  { fix x assume "x \<in> s"
   8.132 -    then have "f ` s \<subseteq> {f x}"
   8.133 -    by (metis connected_continuous_image conf connected_component_maximal fim image_subset_iff rev_image_eqI s cct)
   8.134 +  { fix x assume "x \<in> S"
   8.135 +    then have "f ` S \<subseteq> {f x}"
   8.136 +    by (metis connected_continuous_image conf connected_component_maximal fim image_subset_iff rev_image_eqI S cct)
   8.137    }
   8.138    with False show ?thesis
   8.139      by blast
   8.140  qed
   8.141  
   8.142  lemma discrete_subset_disconnected:
   8.143 -  fixes s :: "'a::topological_space set"
   8.144 +  fixes S :: "'a::topological_space set"
   8.145    fixes t :: "'b::real_normed_vector set"
   8.146 -  assumes conf: "continuous_on s f"
   8.147 -      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)"
   8.148 -   shows "f ` s \<subseteq> {y. connected_component_set (f ` s) y = {y}}"
   8.149 -proof -
   8.150 -  { fix x assume x: "x \<in> s"
   8.151 -    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)"
   8.152 +  assumes conf: "continuous_on S f"
   8.153 +      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)"
   8.154 +   shows "f ` S \<subseteq> {y. connected_component_set (f ` S) y = {y}}"
   8.155 +proof -
   8.156 +  { fix x assume x: "x \<in> S"
   8.157 +    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)"
   8.158        using conf no [OF x] by auto
   8.159      then have e2: "0 \<le> e / 2"
   8.160        by simp
   8.161 -    have "f y = f x" if "y \<in> s" and ccs: "f y \<in> connected_component_set (f ` s) (f x)" for y
   8.162 +    have "f y = f x" if "y \<in> S" and ccs: "f y \<in> connected_component_set (f ` S) (f x)" for y
   8.163        apply (rule ccontr)
   8.164 -      using connected_closed [of "connected_component_set (f ` s) (f x)"] \<open>e>0\<close>
   8.165 +      using connected_closed [of "connected_component_set (f ` S) (f x)"] \<open>e>0\<close>
   8.166        apply (simp add: del: ex_simps)
   8.167        apply (drule spec [where x="cball (f x) (e / 2)"])
   8.168        apply (drule spec [where x="- ball(f x) e"])
   8.169 @@ -11082,11 +11122,11 @@
   8.170          apply (metis diff_self e2 ele norm_minus_commute norm_zero not_less)
   8.171         using centre_in_cball connected_component_refl_eq e2 x apply blast
   8.172        using ccs
   8.173 -      apply (force simp: cball_def dist_norm norm_minus_commute dest: ele [OF \<open>y \<in> s\<close>])
   8.174 +      apply (force simp: cball_def dist_norm norm_minus_commute dest: ele [OF \<open>y \<in> S\<close>])
   8.175        done
   8.176 -    moreover have "connected_component_set (f ` s) (f x) \<subseteq> f ` s"
   8.177 +    moreover have "connected_component_set (f ` S) (f x) \<subseteq> f ` S"
   8.178        by (auto simp: connected_component_in)
   8.179 -    ultimately have "connected_component_set (f ` s) (f x) = {f x}"
   8.180 +    ultimately have "connected_component_set (f ` S) (f x) = {f x}"
   8.181        by (auto simp: x)
   8.182    }
   8.183    with assms show ?thesis
   8.184 @@ -11094,22 +11134,22 @@
   8.185  qed
   8.186  
   8.187  lemma finite_implies_discrete:
   8.188 -  fixes s :: "'a::topological_space set"
   8.189 -  assumes "finite (f ` s)"
   8.190 -  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))"
   8.191 -proof -
   8.192 -  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
   8.193 -  proof (cases "f ` s - {f x} = {}")
   8.194 +  fixes S :: "'a::topological_space set"
   8.195 +  assumes "finite (f ` S)"
   8.196 +  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))"
   8.197 +proof -
   8.198 +  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
   8.199 +  proof (cases "f ` S - {f x} = {}")
   8.200      case True
   8.201      with zero_less_numeral show ?thesis
   8.202        by (fastforce simp add: Set.image_subset_iff cong: conj_cong)
   8.203    next
   8.204      case False
   8.205 -    then obtain z where z: "z \<in> s" "f z \<noteq> f x"
   8.206 +    then obtain z where z: "z \<in> S" "f z \<noteq> f x"
   8.207        by blast
   8.208 -    have finn: "finite {norm (z - f x) |z. z \<in> f ` s - {f x}}"
   8.209 +    have finn: "finite {norm (z - f x) |z. z \<in> f ` S - {f x}}"
   8.210        using assms by simp
   8.211 -    then have *: "0 < Inf{norm(z - f x) | z. z \<in> f ` s - {f x}}"
   8.212 +    then have *: "0 < Inf{norm(z - f x) | z. z \<in> f ` S - {f x}}"
   8.213        apply (rule finite_imp_less_Inf)
   8.214        using z apply force+
   8.215        done
   8.216 @@ -11123,20 +11163,20 @@
   8.217  text\<open>This proof requires the existence of two separate values of the range type.\<close>
   8.218  lemma finite_range_constant_imp_connected:
   8.219    assumes "\<And>f::'a::topological_space \<Rightarrow> 'b::real_normed_algebra_1.
   8.220 -              \<lbrakk>continuous_on s f; finite(f ` s)\<rbrakk> \<Longrightarrow> \<exists>a. \<forall>x \<in> s. f x = a"
   8.221 -    shows "connected s"
   8.222 +              \<lbrakk>continuous_on S f; finite(f ` S)\<rbrakk> \<Longrightarrow> \<exists>a. \<forall>x \<in> S. f x = a"
   8.223 +    shows "connected S"
   8.224  proof -
   8.225    { fix t u
   8.226 -    assume clt: "closedin (subtopology euclidean s) t"
   8.227 -       and clu: "closedin (subtopology euclidean s) u"
   8.228 -       and tue: "t \<inter> u = {}" and tus: "t \<union> u = s"
   8.229 -    have conif: "continuous_on s (\<lambda>x. if x \<in> t then 0 else 1)"
   8.230 +    assume clt: "closedin (subtopology euclidean S) t"
   8.231 +       and clu: "closedin (subtopology euclidean S) u"
   8.232 +       and tue: "t \<inter> u = {}" and tus: "t \<union> u = S"
   8.233 +    have conif: "continuous_on S (\<lambda>x. if x \<in> t then 0 else 1)"
   8.234        apply (subst tus [symmetric])
   8.235        apply (rule continuous_on_cases_local)
   8.236        using clt clu tue
   8.237        apply (auto simp: tus continuous_on_const)
   8.238        done
   8.239 -    have fi: "finite ((\<lambda>x. if x \<in> t then 0 else 1) ` s)"
   8.240 +    have fi: "finite ((\<lambda>x. if x \<in> t then 0 else 1) ` S)"
   8.241        by (rule finite_subset [of _ "{0,1}"]) auto
   8.242      have "t = {} \<or> u = {}"
   8.243        using assms [OF conif fi] tus [symmetric]
     9.1 --- a/src/HOL/Archimedean_Field.thy	Sun Oct 08 16:50:37 2017 +0200
     9.2 +++ b/src/HOL/Archimedean_Field.thy	Mon Oct 09 15:34:23 2017 +0100
     9.3 @@ -526,7 +526,8 @@
     9.4    shows "finite {k \<in> \<int>. \<bar>k\<bar> \<le> a}" 
     9.5    using finite_int_segment [of "-a" a] by (auto simp add: abs_le_iff conj_commute minus_le_iff)
     9.6  
     9.7 -text \<open>Ceiling with numerals.\<close>
     9.8 +
     9.9 +subsubsection \<open>Ceiling with numerals.\<close>
    9.10  
    9.11  lemma ceiling_zero [simp]: "\<lceil>0\<rceil> = 0"
    9.12    using ceiling_of_int [of 0] by simp
    9.13 @@ -595,7 +596,7 @@
    9.14    by (simp add: ceiling_altdef)
    9.15  
    9.16  
    9.17 -text \<open>Addition and subtraction of integers.\<close>
    9.18 +subsubsection \<open>Addition and subtraction of integers.\<close>
    9.19  
    9.20  lemma ceiling_add_of_int [simp]: "\<lceil>x + of_int z\<rceil> = \<lceil>x\<rceil> + z"
    9.21    using ceiling_correct [of x] by (simp add: ceiling_def)
    9.22 @@ -630,6 +631,24 @@
    9.23      unfolding of_int_less_iff by simp
    9.24  qed
    9.25  
    9.26 +lemma nat_approx_posE:
    9.27 +  fixes e:: "'a::{archimedean_field,floor_ceiling}"
    9.28 +  assumes "0 < e"
    9.29 +  obtains n :: nat where "1 / of_nat(Suc n) < e"
    9.30 +proof 
    9.31 +  have "(1::'a) / of_nat (Suc (nat \<lceil>1/e\<rceil>)) < 1 / of_int (\<lceil>1/e\<rceil>)"
    9.32 +  proof (rule divide_strict_left_mono)
    9.33 +    show "(of_int \<lceil>1 / e\<rceil>::'a) < of_nat (Suc (nat \<lceil>1 / e\<rceil>))"
    9.34 +      using assms by (simp add: field_simps)
    9.35 +    show "(0::'a) < of_nat (Suc (nat \<lceil>1 / e\<rceil>)) * of_int \<lceil>1 / e\<rceil>"
    9.36 +      using assms by (auto simp: zero_less_mult_iff pos_add_strict)
    9.37 +  qed auto
    9.38 +  also have "1 / of_int (\<lceil>1/e\<rceil>) \<le> 1 / (1/e)"
    9.39 +    by (rule divide_left_mono) (auto simp: \<open>0 < e\<close> ceiling_correct)
    9.40 +  also have "\<dots> = e" by simp
    9.41 +  finally show  "1 / of_nat (Suc (nat \<lceil>1 / e\<rceil>)) < e"
    9.42 +    by metis 
    9.43 +qed
    9.44  
    9.45  subsection \<open>Negation\<close>
    9.46  
    10.1 --- a/src/HOL/Complex.thy	Sun Oct 08 16:50:37 2017 +0200
    10.2 +++ b/src/HOL/Complex.thy	Mon Oct 09 15:34:23 2017 +0100
    10.3 @@ -1077,7 +1077,7 @@
    10.4      and Complex_mult_complex_of_real: "Complex x y * complex_of_real r = Complex (x*r) (y*r)"
    10.5      and complex_of_real_mult_Complex: "complex_of_real r * Complex x y = Complex (r*x) (r*y)"
    10.6      and complex_eq_cancel_iff2: "(Complex x y = complex_of_real xa) = (x = xa \<and> y = 0)"
    10.7 -    and complex_cn: "cnj (Complex a b) = Complex a (- b)"
    10.8 +    and complex_cnj: "cnj (Complex a b) = Complex a (- b)"
    10.9      and Complex_sum': "sum (\<lambda>x. Complex (f x) 0) s = Complex (sum f s) 0"
   10.10      and Complex_sum: "Complex (sum f s) 0 = sum (\<lambda>x. Complex (f x) 0) s"
   10.11      and complex_of_real_def: "complex_of_real r = Complex r 0"
    11.1 --- a/src/HOL/Limits.thy	Sun Oct 08 16:50:37 2017 +0200
    11.2 +++ b/src/HOL/Limits.thy	Mon Oct 09 15:34:23 2017 +0100
    11.3 @@ -820,6 +820,11 @@
    11.4  lemmas tendsto_mult_right_zero =
    11.5    bounded_bilinear.tendsto_right_zero [OF bounded_bilinear_mult]
    11.6  
    11.7 +lemma tendsto_divide_zero:
    11.8 +  fixes c :: "'a::real_normed_field"
    11.9 +  shows "(f \<longlongrightarrow> 0) F \<Longrightarrow> ((\<lambda>x. f x / c) \<longlongrightarrow> 0) F"
   11.10 +  by (cases "c=0") (simp_all add: divide_inverse tendsto_mult_left_zero)
   11.11 +
   11.12  lemma tendsto_power [tendsto_intros]: "(f \<longlongrightarrow> a) F \<Longrightarrow> ((\<lambda>x. f x ^ n) \<longlongrightarrow> a ^ n) F"
   11.13    for f :: "'a \<Rightarrow> 'b::{power,real_normed_algebra}"
   11.14    by (induct n) (simp_all add: tendsto_mult)
    12.1 --- a/src/HOL/Real.thy	Sun Oct 08 16:50:37 2017 +0200
    12.2 +++ b/src/HOL/Real.thy	Mon Oct 09 15:34:23 2017 +0100
    12.3 @@ -23,6 +23,11 @@
    12.4  
    12.5  subsection \<open>Preliminary lemmas\<close>
    12.6  
    12.7 +text{*Useful in convergence arguments*}
    12.8 +lemma inverse_of_nat_le:
    12.9 +  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"
   12.10 +  by (simp add: frac_le)
   12.11 +
   12.12  lemma inj_add_left [simp]: "inj (op + x)"
   12.13    for x :: "'a::cancel_semigroup_add"
   12.14    by (meson add_left_imp_eq injI)
    13.1 --- a/src/HOL/Real_Vector_Spaces.thy	Sun Oct 08 16:50:37 2017 +0200
    13.2 +++ b/src/HOL/Real_Vector_Spaces.thy	Mon Oct 09 15:34:23 2017 +0100
    13.3 @@ -1469,17 +1469,14 @@
    13.4  begin
    13.5  
    13.6  lemma pos_bounded: "\<exists>K>0. \<forall>a b. norm (a ** b) \<le> norm a * norm b * K"
    13.7 -  apply (insert bounded)
    13.8 -  apply (erule exE)
    13.9 -  apply (rule_tac x="max 1 K" in exI)
   13.10 -  apply safe
   13.11 -   apply (rule order_less_le_trans [OF zero_less_one max.cobounded1])
   13.12 -  apply (drule spec)
   13.13 -  apply (drule spec)
   13.14 -  apply (erule order_trans)
   13.15 -  apply (rule mult_left_mono [OF max.cobounded2])
   13.16 -  apply (intro mult_nonneg_nonneg norm_ge_zero)
   13.17 -  done
   13.18 +proof -
   13.19 +  obtain K where "\<And>a b. norm (a ** b) \<le> norm a * norm b * K"
   13.20 +    using bounded by blast
   13.21 +  then have "norm (a ** b) \<le> norm a * norm b * (max 1 K)" for a b
   13.22 +    by (rule order.trans) (simp add: mult_left_mono)
   13.23 +  then show ?thesis
   13.24 +    by force
   13.25 +qed
   13.26  
   13.27  lemma nonneg_bounded: "\<exists>K\<ge>0. \<forall>a b. norm (a ** b) \<le> norm a * norm b * K"
   13.28    using pos_bounded by (auto intro: order_less_imp_le)
    14.1 --- a/src/HOL/Rings.thy	Sun Oct 08 16:50:37 2017 +0200
    14.2 +++ b/src/HOL/Rings.thy	Mon Oct 09 15:34:23 2017 +0100
    14.3 @@ -2241,6 +2241,10 @@
    14.4  lemma minus_less_iff_1 [simp, no_atp]: "- a < 1 \<longleftrightarrow> - 1 < a"
    14.5    by (fact minus_less_iff)
    14.6  
    14.7 +lemma add_less_zeroD:
    14.8 +  shows "x+y < 0 \<Longrightarrow> x<0 \<or> y<0"
    14.9 +  by (auto simp: not_less intro: le_less_trans [of _ "x+y"])
   14.10 +
   14.11  end
   14.12  
   14.13  text \<open>Simprules for comparisons where common factors can be cancelled.\<close>