new lemmas about topology, etc., for Cauchy integral formula
authorpaulson
Mon Oct 26 23:41:27 2015 +0000 (2015-10-26)
changeset 61518ff12606337e9
parent 61515 c64628dbac00
child 61519 df57e4e3c0b7
new lemmas about topology, etc., for Cauchy integral formula
src/HOL/Finite_Set.thy
src/HOL/Library/Convex.thy
src/HOL/Library/Inner_Product.thy
src/HOL/Multivariate_Analysis/Cauchy_Integral_Thm.thy
src/HOL/Multivariate_Analysis/Complex_Analysis_Basics.thy
src/HOL/Multivariate_Analysis/Complex_Transcendental.thy
src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy
src/HOL/Multivariate_Analysis/Derivative.thy
src/HOL/Multivariate_Analysis/Integration.thy
src/HOL/Multivariate_Analysis/Linear_Algebra.thy
src/HOL/Multivariate_Analysis/Multivariate_Analysis.thy
src/HOL/Multivariate_Analysis/Path_Connected.thy
src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy
src/HOL/Set.thy
src/HOL/Transcendental.thy
     1.1 --- a/src/HOL/Finite_Set.thy	Sun Oct 25 17:31:14 2015 +0100
     1.2 +++ b/src/HOL/Finite_Set.thy	Mon Oct 26 23:41:27 2015 +0000
     1.3 @@ -1545,6 +1545,10 @@
     1.4   apply(auto simp add: intro:ccontr)
     1.5   done
     1.6  
     1.7 +lemma card_1_singletonE:
     1.8 +    assumes "card A = 1" obtains x where "A = {x}"
     1.9 +  using assms by (auto simp: card_Suc_eq)
    1.10 +
    1.11  lemma card_le_Suc_iff: "finite A \<Longrightarrow>
    1.12    Suc n \<le> card A = (\<exists>a B. A = insert a B \<and> a \<notin> B \<and> n \<le> card B \<and> finite B)"
    1.13  by (fastforce simp: card_Suc_eq less_eq_nat.simps(2) insert_eq_iff
     2.1 --- a/src/HOL/Library/Convex.thy	Sun Oct 25 17:31:14 2015 +0100
     2.2 +++ b/src/HOL/Library/Convex.thy	Mon Oct 26 23:41:27 2015 +0000
     2.3 @@ -96,7 +96,7 @@
     2.4  lemma convex_halfspace_gt: "convex {x. inner a x > b}"
     2.5     using convex_halfspace_lt[of "-a" "-b"] by auto
     2.6  
     2.7 -lemma convex_real_interval:
     2.8 +lemma convex_real_interval [iff]:
     2.9    fixes a b :: "real"
    2.10    shows "convex {a..}" and "convex {..b}"
    2.11      and "convex {a<..}" and "convex {..<b}"
     3.1 --- a/src/HOL/Library/Inner_Product.thy	Sun Oct 25 17:31:14 2015 +0100
     3.2 +++ b/src/HOL/Library/Inner_Product.thy	Mon Oct 26 23:41:27 2015 +0000
     3.3 @@ -81,6 +81,20 @@
     3.4  lemma power2_norm_eq_inner: "(norm x)\<^sup>2 = inner x x"
     3.5    by (simp add: norm_eq_sqrt_inner)
     3.6  
     3.7 +text \<open>Identities involving real multiplication and division.\<close>
     3.8 +
     3.9 +lemma inner_mult_left: "inner (of_real m * a) b = m * (inner a b)"
    3.10 +  by (metis real_inner_class.inner_scaleR_left scaleR_conv_of_real)
    3.11 +
    3.12 +lemma inner_mult_right: "inner a (of_real m * b) = m * (inner a b)"
    3.13 +  by (metis real_inner_class.inner_scaleR_right scaleR_conv_of_real)
    3.14 +
    3.15 +lemma inner_mult_left': "inner (a * of_real m) b = m * (inner a b)"
    3.16 +  by (simp add: of_real_def)
    3.17 +
    3.18 +lemma inner_mult_right': "inner a (b * of_real m) = (inner a b) * m"
    3.19 +  by (simp add: of_real_def real_inner_class.inner_scaleR_right)
    3.20 +
    3.21  lemma Cauchy_Schwarz_ineq:
    3.22    "(inner x y)\<^sup>2 \<le> inner x x * inner y y"
    3.23  proof (cases)
    3.24 @@ -141,6 +155,16 @@
    3.25  
    3.26  end
    3.27  
    3.28 +lemma inner_divide_left:
    3.29 +  fixes a :: "'a :: {real_inner,real_div_algebra}"
    3.30 +  shows "inner (a / of_real m) b = (inner a b) / m"
    3.31 +  by (metis (no_types) divide_inverse inner_commute inner_scaleR_right mult.left_neutral mult.right_neutral mult_scaleR_right of_real_inverse scaleR_conv_of_real times_divide_eq_left)
    3.32 +
    3.33 +lemma inner_divide_right:
    3.34 +  fixes a :: "'a :: {real_inner,real_div_algebra}"
    3.35 +  shows "inner a (b / of_real m) = (inner a b) / m"
    3.36 +  by (metis inner_commute inner_divide_left)
    3.37 +
    3.38  text \<open>
    3.39    Re-enable constraints for @{term "open"},
    3.40    @{term dist}, and @{term norm}.
     4.1 --- a/src/HOL/Multivariate_Analysis/Cauchy_Integral_Thm.thy	Sun Oct 25 17:31:14 2015 +0100
     4.2 +++ b/src/HOL/Multivariate_Analysis/Cauchy_Integral_Thm.thy	Mon Oct 26 23:41:27 2015 +0000
     4.3 @@ -2484,7 +2484,7 @@
     4.4      shows "convex hull {a,b,c} \<subseteq> s"
     4.5        using s
     4.6        apply (clarsimp simp add: convex_hull_insert [of "{b,c}" a] segment_convex_hull)
     4.7 -      apply (meson subs convexD convex_segment ends_in_segment(1) ends_in_segment(2) subsetCE)
     4.8 +      apply (meson subs convexD convex_closed_segment ends_in_segment(1) ends_in_segment(2) subsetCE)
     4.9        done
    4.10  
    4.11  lemma triangle_path_integrals_starlike_primitive:
    4.12 @@ -3096,7 +3096,6 @@
    4.13    using path_integral_nearby [OF assms, where Ends=False]
    4.14    by simp_all
    4.15  
    4.16 -  thm has_vector_derivative_polynomial_function
    4.17  corollary differentiable_polynomial_function:
    4.18    fixes p :: "real \<Rightarrow> 'a::euclidean_space"
    4.19    shows "polynomial_function p \<Longrightarrow> p differentiable_on s"
    4.20 @@ -3112,6 +3111,11 @@
    4.21    shows "polynomial_function p \<Longrightarrow> valid_path p"
    4.22  by (force simp: valid_path_def piecewise_C1_differentiable_on_def continuous_on_polymonial_function C1_differentiable_polynomial_function)
    4.23  
    4.24 +lemma valid_path_subpath_trivial [simp]:
    4.25 +    fixes g :: "real \<Rightarrow> 'a::euclidean_space"
    4.26 +    shows "z \<noteq> g x \<Longrightarrow> valid_path (subpath x x g)"
    4.27 +  by (simp add: subpath_def valid_path_polynomial_function)
    4.28 +
    4.29  lemma path_integral_bound_exists:
    4.30  assumes s: "open s"
    4.31      and g: "valid_path g"
     5.1 --- a/src/HOL/Multivariate_Analysis/Complex_Analysis_Basics.thy	Sun Oct 25 17:31:14 2015 +0100
     5.2 +++ b/src/HOL/Multivariate_Analysis/Complex_Analysis_Basics.thy	Mon Oct 26 23:41:27 2015 +0000
     5.3 @@ -1083,7 +1083,7 @@
     5.4    also have "... \<le> B * cmod (z - w) ^ n / (fact n) * cmod (w - z)"
     5.5      apply (rule complex_differentiable_bound 
     5.6        [where f' = "\<lambda>w. f (Suc n) w * (z - w)^n / (fact n)"
     5.7 -         and s = "closed_segment w z", OF convex_segment])
     5.8 +         and s = "closed_segment w z", OF convex_closed_segment])
     5.9      apply (auto simp: ends_in_segment real_of_nat_def DERIV_subset [OF sum_deriv wzs]
    5.10                    norm_divide norm_mult norm_power divide_le_cancel cmod_bound)
    5.11      done
    5.12 @@ -1096,7 +1096,7 @@
    5.13  
    5.14  lemma complex_mvt_line:
    5.15    assumes "\<And>u. u \<in> closed_segment w z \<Longrightarrow> (f has_field_derivative f'(u)) (at u)"
    5.16 -    shows "\<exists>u. u \<in> open_segment w z \<and> Re(f z) - Re(f w) = Re(f'(u) * (z - w))"
    5.17 +    shows "\<exists>u. u \<in> closed_segment w z \<and> Re(f z) - Re(f w) = Re(f'(u) * (z - w))"
    5.18  proof -
    5.19    have twz: "\<And>t. (1 - t) *\<^sub>R w + t *\<^sub>R z = w + t *\<^sub>R (z - w)"
    5.20      by (simp add: real_vector.scale_left_diff_distrib real_vector.scale_right_diff_distrib)
    5.21 @@ -1107,11 +1107,10 @@
    5.22                        "\<lambda>u. Re o (\<lambda>h. f'((1 - u) *\<^sub>R w + u *\<^sub>R z) * h) o (\<lambda>t. t *\<^sub>R (z - w))"])
    5.23      apply auto
    5.24      apply (rule_tac x="(1 - x) *\<^sub>R w + x *\<^sub>R z" in exI)
    5.25 -    apply (auto simp add: open_segment_def twz) []
    5.26 -    apply (intro derivative_eq_intros has_derivative_at_within)
    5.27 -    apply simp_all
    5.28 +    apply (auto simp: closed_segment_def twz) []
    5.29 +    apply (intro derivative_eq_intros has_derivative_at_within, simp_all)
    5.30      apply (simp add: fun_eq_iff real_vector.scale_right_diff_distrib)
    5.31 -    apply (force simp add: twz closed_segment_def)
    5.32 +    apply (force simp: twz closed_segment_def)
    5.33      done
    5.34  qed
    5.35  
     6.1 --- a/src/HOL/Multivariate_Analysis/Complex_Transcendental.thy	Sun Oct 25 17:31:14 2015 +0100
     6.2 +++ b/src/HOL/Multivariate_Analysis/Complex_Transcendental.thy	Mon Oct 26 23:41:27 2015 +0000
     6.3 @@ -464,7 +464,7 @@
     6.4    "norm(exp z - (\<Sum>k\<le>n. z ^ k / (fact k))) \<le> exp\<bar>Re z\<bar> * (norm z) ^ (Suc n) / (fact n)"
     6.5  proof (rule complex_taylor [of _ n "\<lambda>k. exp" "exp\<bar>Re z\<bar>" 0 z, simplified])
     6.6    show "convex (closed_segment 0 z)"
     6.7 -    by (rule convex_segment [of 0 z])
     6.8 +    by (rule convex_closed_segment [of 0 z])
     6.9  next
    6.10    fix k x
    6.11    assume "x \<in> closed_segment 0 z" "k \<le> n"
     7.1 --- a/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy	Sun Oct 25 17:31:14 2015 +0100
     7.2 +++ b/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy	Mon Oct 26 23:41:27 2015 +0000
     7.3 @@ -17,10 +17,10 @@
     7.4  (* To be moved elsewhere                                                     *)
     7.5  (* ------------------------------------------------------------------------- *)
     7.6  
     7.7 -lemma linear_scaleR: "linear (\<lambda>x. scaleR c x)"
     7.8 +lemma linear_scaleR  [simp]: "linear (\<lambda>x. scaleR c x)"
     7.9    by (simp add: linear_iff scaleR_add_right)
    7.10  
    7.11 -lemma linear_scaleR_left: "linear (\<lambda>r. scaleR r x)"
    7.12 +lemma linear_scaleR_left [simp]: "linear (\<lambda>r. scaleR r x)"
    7.13    by (simp add: linear_iff scaleR_add_left)
    7.14  
    7.15  lemma injective_scaleR: "c \<noteq> 0 \<Longrightarrow> inj (\<lambda>x::'a::real_vector. scaleR c x)"
    7.16 @@ -259,33 +259,62 @@
    7.17      by blast
    7.18  qed
    7.19  
    7.20 -lemma closure_bounded_linear_image:
    7.21 +lemma closure_bounded_linear_image_subset:
    7.22    assumes f: "bounded_linear f"
    7.23    shows "f ` closure S \<subseteq> closure (f ` S)"
    7.24    using linear_continuous_on [OF f] closed_closure closure_subset
    7.25    by (rule image_closure_subset)
    7.26  
    7.27 -lemma closure_linear_image:
    7.28 +lemma closure_linear_image_subset:
    7.29    fixes f :: "'m::euclidean_space \<Rightarrow> 'n::real_normed_vector"
    7.30    assumes "linear f"
    7.31 -  shows "f ` (closure S) \<le> closure (f ` S)"
    7.32 +  shows "f ` (closure S) \<subseteq> closure (f ` S)"
    7.33    using assms unfolding linear_conv_bounded_linear
    7.34 -  by (rule closure_bounded_linear_image)
    7.35 +  by (rule closure_bounded_linear_image_subset)
    7.36 +
    7.37 +lemma closed_injective_linear_image:
    7.38 +    fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
    7.39 +    assumes S: "closed S" and f: "linear f" "inj f"
    7.40 +    shows "closed (f ` S)"
    7.41 +proof -
    7.42 +  obtain g where g: "linear g" "g \<circ> f = id"
    7.43 +    using linear_injective_left_inverse [OF f] by blast
    7.44 +  then have confg: "continuous_on (range f) g"
    7.45 +    using linear_continuous_on linear_conv_bounded_linear by blast
    7.46 +  have [simp]: "g ` f ` S = S"
    7.47 +    using g by (simp add: image_comp)
    7.48 +  have cgf: "closed (g ` f ` S)"
    7.49 +    by (simp add: `g \<circ> f = id` S image_comp)
    7.50 +  have [simp]: "{x \<in> range f. g x \<in> S} = f ` S"
    7.51 +    using g by (simp add: o_def id_def image_def) metis
    7.52 +  show ?thesis
    7.53 +    apply (rule closedin_closed_trans [of "range f"])
    7.54 +    apply (rule continuous_closedin_preimage [OF confg cgf, simplified])
    7.55 +    apply (rule closed_injective_image_subspace)
    7.56 +    using f
    7.57 +    apply (auto simp: linear_linear linear_injective_0)
    7.58 +    done
    7.59 +qed
    7.60 +
    7.61 +lemma closed_injective_linear_image_eq:
    7.62 +    fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
    7.63 +    assumes f: "linear f" "inj f"
    7.64 +      shows "(closed(image f s) \<longleftrightarrow> closed s)"
    7.65 +  by (metis closed_injective_linear_image closure_eq closure_linear_image_subset closure_subset_eq f(1) f(2) inj_image_subset_iff)
    7.66  
    7.67  lemma closure_injective_linear_image:
    7.68 -  fixes f :: "'n::euclidean_space \<Rightarrow> 'n::euclidean_space"
    7.69 -  assumes "linear f" "inj f"
    7.70 -  shows "f ` (closure S) = closure (f ` S)"
    7.71 -proof -
    7.72 -  obtain f' where f': "linear f' \<and> f \<circ> f' = id \<and> f' \<circ> f = id"
    7.73 -    using assms linear_injective_isomorphism[of f] isomorphism_expand by auto
    7.74 -  then have "f' ` closure (f ` S) \<le> closure (S)"
    7.75 -    using closure_linear_image[of f' "f ` S"] image_comp[of f' f] by auto
    7.76 -  then have "f ` f' ` closure (f ` S) \<le> f ` closure S" by auto
    7.77 -  then have "closure (f ` S) \<le> f ` closure S"
    7.78 -    using image_comp[of f f' "closure (f ` S)"] f' by auto
    7.79 -  then show ?thesis using closure_linear_image[of f S] assms by auto
    7.80 -qed
    7.81 +    fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
    7.82 +    shows "\<lbrakk>linear f; inj f\<rbrakk> \<Longrightarrow> f ` (closure S) = closure (f ` S)"
    7.83 +  apply (rule subset_antisym)
    7.84 +  apply (simp add: closure_linear_image_subset)
    7.85 +  by (simp add: closure_minimal closed_injective_linear_image closure_subset image_mono)
    7.86 +
    7.87 +lemma closure_bounded_linear_image:
    7.88 +    fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
    7.89 +    shows "\<lbrakk>linear f; bounded S\<rbrakk> \<Longrightarrow> f ` (closure S) = closure (f ` S)"
    7.90 +  apply (rule subset_antisym, simp add: closure_linear_image_subset)
    7.91 +  apply (rule closure_minimal, simp add: closure_subset image_mono)
    7.92 +  by (meson bounded_closure closed_closure compact_continuous_image compact_eq_bounded_closed linear_continuous_on linear_conv_bounded_linear)
    7.93  
    7.94  lemma closure_scaleR:
    7.95    fixes S :: "'a::real_normed_vector set"
    7.96 @@ -293,7 +322,7 @@
    7.97  proof
    7.98    show "(op *\<^sub>R c) ` (closure S) \<subseteq> closure ((op *\<^sub>R c) ` S)"
    7.99      using bounded_linear_scaleR_right
   7.100 -    by (rule closure_bounded_linear_image)
   7.101 +    by (rule closure_bounded_linear_image_subset)
   7.102    show "closure ((op *\<^sub>R c) ` S) \<subseteq> (op *\<^sub>R c) ` (closure S)"
   7.103      by (intro closure_minimal image_mono closure_subset closed_scaling closed_closure)
   7.104  qed
   7.105 @@ -1422,12 +1451,12 @@
   7.106    then show ?thesis by (auto simp add: convex_def Ball_def)
   7.107  qed
   7.108  
   7.109 -lemma connected_ball:
   7.110 +lemma connected_ball [iff]:
   7.111    fixes x :: "'a::real_normed_vector"
   7.112    shows "connected (ball x e)"
   7.113    using convex_connected convex_ball by auto
   7.114  
   7.115 -lemma connected_cball:
   7.116 +lemma connected_cball [iff]:
   7.117    fixes x :: "'a::real_normed_vector"
   7.118    shows "connected (cball x e)"
   7.119    using convex_connected convex_cball by auto
   7.120 @@ -2212,140 +2241,6 @@
   7.121  qed
   7.122  
   7.123  
   7.124 -subsection \<open>Caratheodory's theorem.\<close>
   7.125 -
   7.126 -lemma convex_hull_caratheodory:
   7.127 -  fixes p :: "('a::euclidean_space) set"
   7.128 -  shows "convex hull p =
   7.129 -    {y. \<exists>s u. finite s \<and> s \<subseteq> p \<and> card s \<le> DIM('a) + 1 \<and>
   7.130 -      (\<forall>x\<in>s. 0 \<le> u x) \<and> setsum u s = 1 \<and> setsum (\<lambda>v. u v *\<^sub>R v) s = y}"
   7.131 -  unfolding convex_hull_explicit set_eq_iff mem_Collect_eq
   7.132 -proof (rule, rule)
   7.133 -  fix y
   7.134 -  let ?P = "\<lambda>n. \<exists>s u. finite s \<and> card s = n \<and> s \<subseteq> p \<and> (\<forall>x\<in>s. 0 \<le> u x) \<and>
   7.135 -    setsum u s = 1 \<and> (\<Sum>v\<in>s. u v *\<^sub>R v) = y"
   7.136 -  assume "\<exists>s u. finite s \<and> s \<subseteq> p \<and> (\<forall>x\<in>s. 0 \<le> u x) \<and> setsum u s = 1 \<and> (\<Sum>v\<in>s. u v *\<^sub>R v) = y"
   7.137 -  then obtain N where "?P N" by auto
   7.138 -  then have "\<exists>n\<le>N. (\<forall>k<n. \<not> ?P k) \<and> ?P n"
   7.139 -    apply (rule_tac ex_least_nat_le)
   7.140 -    apply auto
   7.141 -    done
   7.142 -  then obtain n where "?P n" and smallest: "\<forall>k<n. \<not> ?P k"
   7.143 -    by blast
   7.144 -  then obtain s u where obt: "finite s" "card s = n" "s\<subseteq>p" "\<forall>x\<in>s. 0 \<le> u x"
   7.145 -    "setsum u s = 1"  "(\<Sum>v\<in>s. u v *\<^sub>R v) = y" by auto
   7.146 -
   7.147 -  have "card s \<le> DIM('a) + 1"
   7.148 -  proof (rule ccontr, simp only: not_le)
   7.149 -    assume "DIM('a) + 1 < card s"
   7.150 -    then have "affine_dependent s"
   7.151 -      using affine_dependent_biggerset[OF obt(1)] by auto
   7.152 -    then obtain w v where wv: "setsum w s = 0" "v\<in>s" "w v \<noteq> 0" "(\<Sum>v\<in>s. w v *\<^sub>R v) = 0"
   7.153 -      using affine_dependent_explicit_finite[OF obt(1)] by auto
   7.154 -    def i \<equiv> "(\<lambda>v. (u v) / (- w v)) ` {v\<in>s. w v < 0}"
   7.155 -    def t \<equiv> "Min i"
   7.156 -    have "\<exists>x\<in>s. w x < 0"
   7.157 -    proof (rule ccontr, simp add: not_less)
   7.158 -      assume as:"\<forall>x\<in>s. 0 \<le> w x"
   7.159 -      then have "setsum w (s - {v}) \<ge> 0"
   7.160 -        apply (rule_tac setsum_nonneg)
   7.161 -        apply auto
   7.162 -        done
   7.163 -      then have "setsum w s > 0"
   7.164 -        unfolding setsum.remove[OF obt(1) \<open>v\<in>s\<close>]
   7.165 -        using as[THEN bspec[where x=v]] and \<open>v\<in>s\<close>
   7.166 -        using \<open>w v \<noteq> 0\<close>
   7.167 -        by auto
   7.168 -      then show False using wv(1) by auto
   7.169 -    qed
   7.170 -    then have "i \<noteq> {}" unfolding i_def by auto
   7.171 -
   7.172 -    then have "t \<ge> 0"
   7.173 -      using Min_ge_iff[of i 0 ] and obt(1)
   7.174 -      unfolding t_def i_def
   7.175 -      using obt(4)[unfolded le_less]
   7.176 -      by (auto simp: divide_le_0_iff)
   7.177 -    have t: "\<forall>v\<in>s. u v + t * w v \<ge> 0"
   7.178 -    proof
   7.179 -      fix v
   7.180 -      assume "v \<in> s"
   7.181 -      then have v: "0 \<le> u v"
   7.182 -        using obt(4)[THEN bspec[where x=v]] by auto
   7.183 -      show "0 \<le> u v + t * w v"
   7.184 -      proof (cases "w v < 0")
   7.185 -        case False
   7.186 -        thus ?thesis using v \<open>t\<ge>0\<close> by auto
   7.187 -      next
   7.188 -        case True
   7.189 -        then have "t \<le> u v / (- w v)"
   7.190 -          using \<open>v\<in>s\<close>
   7.191 -          unfolding t_def i_def
   7.192 -          apply (rule_tac Min_le)
   7.193 -          using obt(1)
   7.194 -          apply auto
   7.195 -          done
   7.196 -        then show ?thesis
   7.197 -          unfolding real_0_le_add_iff
   7.198 -          using pos_le_divide_eq[OF True[unfolded neg_0_less_iff_less[symmetric]]]
   7.199 -          by auto
   7.200 -      qed
   7.201 -    qed
   7.202 -
   7.203 -    obtain a where "a \<in> s" and "t = (\<lambda>v. (u v) / (- w v)) a" and "w a < 0"
   7.204 -      using Min_in[OF _ \<open>i\<noteq>{}\<close>] and obt(1) unfolding i_def t_def by auto
   7.205 -    then have a: "a \<in> s" "u a + t * w a = 0" by auto
   7.206 -    have *: "\<And>f. setsum f (s - {a}) = setsum f s - ((f a)::'b::ab_group_add)"
   7.207 -      unfolding setsum.remove[OF obt(1) \<open>a\<in>s\<close>] by auto
   7.208 -    have "(\<Sum>v\<in>s. u v + t * w v) = 1"
   7.209 -      unfolding setsum.distrib wv(1) setsum_right_distrib[symmetric] obt(5) by auto
   7.210 -    moreover have "(\<Sum>v\<in>s. u v *\<^sub>R v + (t * w v) *\<^sub>R v) - (u a *\<^sub>R a + (t * w a) *\<^sub>R a) = y"
   7.211 -      unfolding setsum.distrib obt(6) scaleR_scaleR[symmetric] scaleR_right.setsum [symmetric] wv(4)
   7.212 -      using a(2) [THEN eq_neg_iff_add_eq_0 [THEN iffD2]] by simp
   7.213 -    ultimately have "?P (n - 1)"
   7.214 -      apply (rule_tac x="(s - {a})" in exI)
   7.215 -      apply (rule_tac x="\<lambda>v. u v + t * w v" in exI)
   7.216 -      using obt(1-3) and t and a
   7.217 -      apply (auto simp add: * scaleR_left_distrib)
   7.218 -      done
   7.219 -    then show False
   7.220 -      using smallest[THEN spec[where x="n - 1"]] by auto
   7.221 -  qed
   7.222 -  then show "\<exists>s u. finite s \<and> s \<subseteq> p \<and> card s \<le> DIM('a) + 1 \<and>
   7.223 -      (\<forall>x\<in>s. 0 \<le> u x) \<and> setsum u s = 1 \<and> (\<Sum>v\<in>s. u v *\<^sub>R v) = y"
   7.224 -    using obt by auto
   7.225 -qed auto
   7.226 -
   7.227 -lemma caratheodory:
   7.228 -  "convex hull p =
   7.229 -    {x::'a::euclidean_space. \<exists>s. finite s \<and> s \<subseteq> p \<and>
   7.230 -      card s \<le> DIM('a) + 1 \<and> x \<in> convex hull s}"
   7.231 -  unfolding set_eq_iff
   7.232 -  apply rule
   7.233 -  apply rule
   7.234 -  unfolding mem_Collect_eq
   7.235 -proof -
   7.236 -  fix x
   7.237 -  assume "x \<in> convex hull p"
   7.238 -  then obtain s u where "finite s" "s \<subseteq> p" "card s \<le> DIM('a) + 1"
   7.239 -    "\<forall>x\<in>s. 0 \<le> u x" "setsum u s = 1" "(\<Sum>v\<in>s. u v *\<^sub>R v) = x"
   7.240 -    unfolding convex_hull_caratheodory by auto
   7.241 -  then show "\<exists>s. finite s \<and> s \<subseteq> p \<and> card s \<le> DIM('a) + 1 \<and> x \<in> convex hull s"
   7.242 -    apply (rule_tac x=s in exI)
   7.243 -    using hull_subset[of s convex]
   7.244 -    using convex_convex_hull[unfolded convex_explicit, of s,
   7.245 -      THEN spec[where x=s], THEN spec[where x=u]]
   7.246 -    apply auto
   7.247 -    done
   7.248 -next
   7.249 -  fix x
   7.250 -  assume "\<exists>s. finite s \<and> s \<subseteq> p \<and> card s \<le> DIM('a) + 1 \<and> x \<in> convex hull s"
   7.251 -  then obtain s where "finite s" "s \<subseteq> p" "card s \<le> DIM('a) + 1" "x \<in> convex hull s"
   7.252 -    by auto
   7.253 -  then show "x \<in> convex hull p"
   7.254 -    using hull_mono[OF \<open>s\<subseteq>p\<close>] by auto
   7.255 -qed
   7.256 -
   7.257 -
   7.258  subsection \<open>Some Properties of Affine Dependent Sets\<close>
   7.259  
   7.260  lemma affine_independent_empty: "\<not> affine_dependent {}"
   7.261 @@ -2572,7 +2467,8 @@
   7.262  
   7.263  subsection \<open>Affine Dimension of a Set\<close>
   7.264  
   7.265 -definition "aff_dim V =
   7.266 +definition aff_dim :: "('a::euclidean_space) set \<Rightarrow> int"
   7.267 +  where "aff_dim V =
   7.268    (SOME d :: int.
   7.269      \<exists>B. affine hull B = affine hull V \<and> \<not> affine_dependent B \<and> of_nat (card B) = d + 1)"
   7.270  
   7.271 @@ -2782,6 +2678,9 @@
   7.272      using aff_independent_finite[of B] card_gt_0_iff[of B] by auto
   7.273  qed
   7.274  
   7.275 +lemma aff_dim_empty_eq [simp]: "aff_dim ({}::'a::euclidean_space set) = -1"
   7.276 +  by (simp add: aff_dim_empty [symmetric])
   7.277 +
   7.278  lemma aff_dim_affine_hull: "aff_dim (affine hull S) = aff_dim S"
   7.279    unfolding aff_dim_def using hull_hull[of _ S] by auto
   7.280  
   7.281 @@ -2829,6 +2728,13 @@
   7.282    shows "of_nat (card B) = aff_dim B + 1"
   7.283    using aff_dim_unique[of B B] assms by auto
   7.284  
   7.285 +lemma affine_independent_iff_card:
   7.286 +    fixes s :: "'a::euclidean_space set"
   7.287 +    shows "~ affine_dependent s \<longleftrightarrow> finite s \<and> aff_dim s = int(card s) - 1"
   7.288 +  apply (rule iffI)
   7.289 +  apply (simp add: aff_dim_affine_independent aff_independent_finite)
   7.290 +  by (metis affine_basis_exists [of s] aff_dim_unique card_subset_eq diff_add_cancel of_nat_eq_iff)
   7.291 +
   7.292  lemma aff_dim_sing:
   7.293    fixes a :: "'n::euclidean_space"
   7.294    shows "aff_dim {a} = 0"
   7.295 @@ -3136,6 +3042,165 @@
   7.296    shows "dim S < DIM ('n) \<Longrightarrow> interior S = {}"
   7.297  by (metis low_dim_interior affine_hull_univ dim_affine_hull less_not_refl dim_UNIV)
   7.298  
   7.299 +subsection \<open>Caratheodory's theorem.\<close>
   7.300 +
   7.301 +lemma convex_hull_caratheodory_aff_dim:
   7.302 +  fixes p :: "('a::euclidean_space) set"
   7.303 +  shows "convex hull p =
   7.304 +    {y. \<exists>s u. finite s \<and> s \<subseteq> p \<and> card s \<le> aff_dim p + 1 \<and>
   7.305 +      (\<forall>x\<in>s. 0 \<le> u x) \<and> setsum u s = 1 \<and> setsum (\<lambda>v. u v *\<^sub>R v) s = y}"
   7.306 +  unfolding convex_hull_explicit set_eq_iff mem_Collect_eq
   7.307 +proof (intro allI iffI)
   7.308 +  fix y
   7.309 +  let ?P = "\<lambda>n. \<exists>s u. finite s \<and> card s = n \<and> s \<subseteq> p \<and> (\<forall>x\<in>s. 0 \<le> u x) \<and>
   7.310 +    setsum u s = 1 \<and> (\<Sum>v\<in>s. u v *\<^sub>R v) = y"
   7.311 +  assume "\<exists>s u. finite s \<and> s \<subseteq> p \<and> (\<forall>x\<in>s. 0 \<le> u x) \<and> setsum u s = 1 \<and> (\<Sum>v\<in>s. u v *\<^sub>R v) = y"
   7.312 +  then obtain N where "?P N" by auto
   7.313 +  then have "\<exists>n\<le>N. (\<forall>k<n. \<not> ?P k) \<and> ?P n"
   7.314 +    apply (rule_tac ex_least_nat_le)
   7.315 +    apply auto
   7.316 +    done
   7.317 +  then obtain n where "?P n" and smallest: "\<forall>k<n. \<not> ?P k"
   7.318 +    by blast
   7.319 +  then obtain s u where obt: "finite s" "card s = n" "s\<subseteq>p" "\<forall>x\<in>s. 0 \<le> u x"
   7.320 +    "setsum u s = 1"  "(\<Sum>v\<in>s. u v *\<^sub>R v) = y" by auto
   7.321 +
   7.322 +  have "card s \<le> aff_dim p + 1"
   7.323 +  proof (rule ccontr, simp only: not_le)
   7.324 +    assume "aff_dim p + 1 < card s"
   7.325 +    then have "affine_dependent s"
   7.326 +      using affine_dependent_biggerset[OF obt(1)] independent_card_le_aff_dim not_less obt(3)
   7.327 +      by blast
   7.328 +    then obtain w v where wv: "setsum w s = 0" "v\<in>s" "w v \<noteq> 0" "(\<Sum>v\<in>s. w v *\<^sub>R v) = 0"
   7.329 +      using affine_dependent_explicit_finite[OF obt(1)] by auto
   7.330 +    def i \<equiv> "(\<lambda>v. (u v) / (- w v)) ` {v\<in>s. w v < 0}"
   7.331 +    def t \<equiv> "Min i"
   7.332 +    have "\<exists>x\<in>s. w x < 0"
   7.333 +    proof (rule ccontr, simp add: not_less)
   7.334 +      assume as:"\<forall>x\<in>s. 0 \<le> w x"
   7.335 +      then have "setsum w (s - {v}) \<ge> 0"
   7.336 +        apply (rule_tac setsum_nonneg)
   7.337 +        apply auto
   7.338 +        done
   7.339 +      then have "setsum w s > 0"
   7.340 +        unfolding setsum.remove[OF obt(1) \<open>v\<in>s\<close>]
   7.341 +        using as[THEN bspec[where x=v]]  \<open>v\<in>s\<close>  \<open>w v \<noteq> 0\<close> by auto
   7.342 +      then show False using wv(1) by auto
   7.343 +    qed
   7.344 +    then have "i \<noteq> {}" unfolding i_def by auto
   7.345 +    then have "t \<ge> 0"
   7.346 +      using Min_ge_iff[of i 0 ] and obt(1)
   7.347 +      unfolding t_def i_def
   7.348 +      using obt(4)[unfolded le_less]
   7.349 +      by (auto simp: divide_le_0_iff)
   7.350 +    have t: "\<forall>v\<in>s. u v + t * w v \<ge> 0"
   7.351 +    proof
   7.352 +      fix v
   7.353 +      assume "v \<in> s"
   7.354 +      then have v: "0 \<le> u v"
   7.355 +        using obt(4)[THEN bspec[where x=v]] by auto
   7.356 +      show "0 \<le> u v + t * w v"
   7.357 +      proof (cases "w v < 0")
   7.358 +        case False
   7.359 +        thus ?thesis using v \<open>t\<ge>0\<close> by auto
   7.360 +      next
   7.361 +        case True
   7.362 +        then have "t \<le> u v / (- w v)"
   7.363 +          using \<open>v\<in>s\<close> unfolding t_def i_def
   7.364 +          apply (rule_tac Min_le)
   7.365 +          using obt(1) apply auto
   7.366 +          done
   7.367 +        then show ?thesis
   7.368 +          unfolding real_0_le_add_iff
   7.369 +          using pos_le_divide_eq[OF True[unfolded neg_0_less_iff_less[symmetric]]]
   7.370 +          by auto
   7.371 +      qed
   7.372 +    qed
   7.373 +    obtain a where "a \<in> s" and "t = (\<lambda>v. (u v) / (- w v)) a" and "w a < 0"
   7.374 +      using Min_in[OF _ \<open>i\<noteq>{}\<close>] and obt(1) unfolding i_def t_def by auto
   7.375 +    then have a: "a \<in> s" "u a + t * w a = 0" by auto
   7.376 +    have *: "\<And>f. setsum f (s - {a}) = setsum f s - ((f a)::'b::ab_group_add)"
   7.377 +      unfolding setsum.remove[OF obt(1) \<open>a\<in>s\<close>] by auto
   7.378 +    have "(\<Sum>v\<in>s. u v + t * w v) = 1"
   7.379 +      unfolding setsum.distrib wv(1) setsum_right_distrib[symmetric] obt(5) by auto
   7.380 +    moreover have "(\<Sum>v\<in>s. u v *\<^sub>R v + (t * w v) *\<^sub>R v) - (u a *\<^sub>R a + (t * w a) *\<^sub>R a) = y"
   7.381 +      unfolding setsum.distrib obt(6) scaleR_scaleR[symmetric] scaleR_right.setsum [symmetric] wv(4)
   7.382 +      using a(2) [THEN eq_neg_iff_add_eq_0 [THEN iffD2]] by simp
   7.383 +    ultimately have "?P (n - 1)"
   7.384 +      apply (rule_tac x="(s - {a})" in exI)
   7.385 +      apply (rule_tac x="\<lambda>v. u v + t * w v" in exI)
   7.386 +      using obt(1-3) and t and a
   7.387 +      apply (auto simp add: * scaleR_left_distrib)
   7.388 +      done
   7.389 +    then show False
   7.390 +      using smallest[THEN spec[where x="n - 1"]] by auto
   7.391 +  qed
   7.392 +  then show "\<exists>s u. finite s \<and> s \<subseteq> p \<and> card s \<le> aff_dim p + 1 \<and>
   7.393 +      (\<forall>x\<in>s. 0 \<le> u x) \<and> setsum u s = 1 \<and> (\<Sum>v\<in>s. u v *\<^sub>R v) = y"
   7.394 +    using obt by auto
   7.395 +qed auto
   7.396 +
   7.397 +lemma caratheodory_aff_dim:
   7.398 +  fixes p :: "('a::euclidean_space) set"
   7.399 +  shows "convex hull p = {x. \<exists>s. finite s \<and> s \<subseteq> p \<and> card s \<le> aff_dim p + 1 \<and> x \<in> convex hull s}"
   7.400 +        (is "?lhs = ?rhs")
   7.401 +proof
   7.402 +  show "?lhs \<subseteq> ?rhs"
   7.403 +    apply (subst convex_hull_caratheodory_aff_dim)
   7.404 +    apply clarify
   7.405 +    apply (rule_tac x="s" in exI)
   7.406 +    apply (simp add: hull_subset convex_explicit [THEN iffD1, OF convex_convex_hull])
   7.407 +    done
   7.408 +next
   7.409 +  show "?rhs \<subseteq> ?lhs"
   7.410 +    using hull_mono by blast
   7.411 +qed
   7.412 +
   7.413 +lemma convex_hull_caratheodory:
   7.414 +  fixes p :: "('a::euclidean_space) set"
   7.415 +  shows "convex hull p =
   7.416 +            {y. \<exists>s u. finite s \<and> s \<subseteq> p \<and> card s \<le> DIM('a) + 1 \<and>
   7.417 +              (\<forall>x\<in>s. 0 \<le> u x) \<and> setsum u s = 1 \<and> setsum (\<lambda>v. u v *\<^sub>R v) s = y}"
   7.418 +        (is "?lhs = ?rhs")
   7.419 +proof (intro set_eqI iffI)
   7.420 +  fix x
   7.421 +  assume "x \<in> ?lhs" then show "x \<in> ?rhs"
   7.422 +    apply (simp only: convex_hull_caratheodory_aff_dim Set.mem_Collect_eq)
   7.423 +    apply (erule ex_forward)+
   7.424 +    using aff_dim_subset_univ [of p]
   7.425 +    apply simp
   7.426 +    done
   7.427 +next
   7.428 +  fix x
   7.429 +  assume "x \<in> ?rhs" then show "x \<in> ?lhs"
   7.430 +    by (auto simp add: convex_hull_explicit)
   7.431 +qed
   7.432 +
   7.433 +theorem caratheodory:
   7.434 +  "convex hull p =
   7.435 +    {x::'a::euclidean_space. \<exists>s. finite s \<and> s \<subseteq> p \<and>
   7.436 +      card s \<le> DIM('a) + 1 \<and> x \<in> convex hull s}"
   7.437 +proof safe
   7.438 +  fix x
   7.439 +  assume "x \<in> convex hull p"
   7.440 +  then obtain s u where "finite s" "s \<subseteq> p" "card s \<le> DIM('a) + 1"
   7.441 +    "\<forall>x\<in>s. 0 \<le> u x" "setsum u s = 1" "(\<Sum>v\<in>s. u v *\<^sub>R v) = x"
   7.442 +    unfolding convex_hull_caratheodory by auto
   7.443 +  then show "\<exists>s. finite s \<and> s \<subseteq> p \<and> card s \<le> DIM('a) + 1 \<and> x \<in> convex hull s"
   7.444 +    apply (rule_tac x=s in exI)
   7.445 +    using hull_subset[of s convex]
   7.446 +    using convex_convex_hull[unfolded convex_explicit, of s,
   7.447 +      THEN spec[where x=s], THEN spec[where x=u]]
   7.448 +    apply auto
   7.449 +    done
   7.450 +next
   7.451 +  fix x s
   7.452 +  assume  "finite s" "s \<subseteq> p" "card s \<le> DIM('a) + 1" "x \<in> convex hull s"
   7.453 +  then show "x \<in> convex hull p"
   7.454 +    using hull_mono[OF \<open>s\<subseteq>p\<close>] by auto
   7.455 +qed
   7.456 +
   7.457 +
   7.458  subsection \<open>Relative interior of a set\<close>
   7.459  
   7.460  definition "rel_interior S =
   7.461 @@ -5708,20 +5773,33 @@
   7.462    shows "is_interval s \<longleftrightarrow> convex s"
   7.463    by (metis is_interval_convex convex_connected is_interval_connected_1)
   7.464  
   7.465 -lemma convex_connected_1:
   7.466 +lemma connected_convex_1:
   7.467    fixes s :: "real set"
   7.468    shows "connected s \<longleftrightarrow> convex s"
   7.469    by (metis is_interval_convex convex_connected is_interval_connected_1)
   7.470  
   7.471 +lemma connected_convex_1_gen:
   7.472 +  fixes s :: "'a :: euclidean_space set"
   7.473 +  assumes "DIM('a) = 1"
   7.474 +  shows "connected s \<longleftrightarrow> convex s"
   7.475 +proof -
   7.476 +  obtain f:: "'a \<Rightarrow> real" where linf: "linear f" and "inj f"
   7.477 +    using subspace_isomorphism [where 'a = 'a and 'b = real]
   7.478 +    by (metis DIM_real dim_UNIV subspace_UNIV assms)
   7.479 +  then have "f -` (f ` s) = s"
   7.480 +    by (simp add: inj_vimage_image_eq)
   7.481 +  then show ?thesis
   7.482 +    by (metis connected_convex_1 convex_linear_vimage linf convex_connected connected_linear_image)
   7.483 +qed
   7.484  
   7.485  subsection \<open>Another intermediate value theorem formulation\<close>
   7.486  
   7.487  lemma ivt_increasing_component_on_1:
   7.488 -  fixes f :: "real \<Rightarrow> 'a::euclidean_space"
   7.489 +  fixes f :: "real \<Rightarrow> 'a::euclidean_space"            
   7.490    assumes "a \<le> b"
   7.491 -    and "continuous_on (cbox a b) f"
   7.492 +    and "continuous_on {a..b} f"
   7.493      and "(f a)\<bullet>k \<le> y" "y \<le> (f b)\<bullet>k"
   7.494 -  shows "\<exists>x\<in>cbox a b. (f x)\<bullet>k = y"
   7.495 +  shows "\<exists>x\<in>{a..b}. (f x)\<bullet>k = y"
   7.496  proof -
   7.497    have "f a \<in> f ` cbox a b" "f b \<in> f ` cbox a b"
   7.498      apply (rule_tac[!] imageI)
   7.499 @@ -5730,24 +5808,22 @@
   7.500      done
   7.501    then show ?thesis
   7.502      using connected_ivt_component[of "f ` cbox a b" "f a" "f b" k y]
   7.503 -    using connected_continuous_image[OF assms(2) convex_connected[OF convex_box(1)]]
   7.504 -    using assms
   7.505 -    by auto
   7.506 +    by (simp add: Topology_Euclidean_Space.connected_continuous_image assms)
   7.507  qed
   7.508  
   7.509  lemma ivt_increasing_component_1:
   7.510    fixes f :: "real \<Rightarrow> 'a::euclidean_space"
   7.511 -  shows "a \<le> b \<Longrightarrow> \<forall>x\<in>cbox a b. continuous (at x) f \<Longrightarrow>
   7.512 -    f a\<bullet>k \<le> y \<Longrightarrow> y \<le> f b\<bullet>k \<Longrightarrow> \<exists>x\<in>cbox a b. (f x)\<bullet>k = y"
   7.513 +  shows "a \<le> b \<Longrightarrow> \<forall>x\<in>{a..b}. continuous (at x) f \<Longrightarrow>
   7.514 +    f a\<bullet>k \<le> y \<Longrightarrow> y \<le> f b\<bullet>k \<Longrightarrow> \<exists>x\<in>{a..b}. (f x)\<bullet>k = y"
   7.515    by (rule ivt_increasing_component_on_1) (auto simp add: continuous_at_imp_continuous_on)
   7.516  
   7.517  lemma ivt_decreasing_component_on_1:
   7.518    fixes f :: "real \<Rightarrow> 'a::euclidean_space"
   7.519    assumes "a \<le> b"
   7.520 -    and "continuous_on (cbox a b) f"
   7.521 +    and "continuous_on {a..b} f"
   7.522      and "(f b)\<bullet>k \<le> y"
   7.523      and "y \<le> (f a)\<bullet>k"
   7.524 -  shows "\<exists>x\<in>cbox a b. (f x)\<bullet>k = y"
   7.525 +  shows "\<exists>x\<in>{a..b}. (f x)\<bullet>k = y"
   7.526    apply (subst neg_equal_iff_equal[symmetric])
   7.527    using ivt_increasing_component_on_1[of a b "\<lambda>x. - f x" k "- y"]
   7.528    using assms using continuous_on_minus
   7.529 @@ -5756,8 +5832,8 @@
   7.530  
   7.531  lemma ivt_decreasing_component_1:
   7.532    fixes f :: "real \<Rightarrow> 'a::euclidean_space"
   7.533 -  shows "a \<le> b \<Longrightarrow> \<forall>x\<in>cbox a b. continuous (at x) f \<Longrightarrow>
   7.534 -    f b\<bullet>k \<le> y \<Longrightarrow> y \<le> f a\<bullet>k \<Longrightarrow> \<exists>x\<in>cbox a b. (f x)\<bullet>k = y"
   7.535 +  shows "a \<le> b \<Longrightarrow> \<forall>x\<in>{a..b}. continuous (at x) f \<Longrightarrow>
   7.536 +    f b\<bullet>k \<le> y \<Longrightarrow> y \<le> f a\<bullet>k \<Longrightarrow> \<exists>x\<in>{a..b}. (f x)\<bullet>k = y"
   7.537    by (rule ivt_decreasing_component_on_1) (auto simp: continuous_at_imp_continuous_on)
   7.538  
   7.539  
   7.540 @@ -6234,12 +6310,12 @@
   7.541  definition midpoint :: "'a::real_vector \<Rightarrow> 'a \<Rightarrow> 'a"
   7.542    where "midpoint a b = (inverse (2::real)) *\<^sub>R (a + b)"
   7.543  
   7.544 -definition open_segment :: "'a::real_vector \<Rightarrow> 'a \<Rightarrow> 'a set"
   7.545 -  where "open_segment a b = {(1 - u) *\<^sub>R a + u *\<^sub>R b | u::real.  0 < u \<and> u < 1}"
   7.546 -
   7.547  definition closed_segment :: "'a::real_vector \<Rightarrow> 'a \<Rightarrow> 'a set"
   7.548    where "closed_segment a b = {(1 - u) *\<^sub>R a + u *\<^sub>R b | u::real. 0 \<le> u \<and> u \<le> 1}"
   7.549  
   7.550 +definition open_segment :: "'a::real_vector \<Rightarrow> 'a \<Rightarrow> 'a set" where
   7.551 +  "open_segment a b \<equiv> closed_segment a b - {a,b}"
   7.552 +
   7.553  definition "between = (\<lambda>(a,b) x. x \<in> closed_segment a b)"
   7.554  
   7.555  lemmas segment = open_segment_def closed_segment_def
   7.556 @@ -6291,7 +6367,7 @@
   7.557      apply (simp add: scaleR_2)
   7.558      done
   7.559    show ?t3
   7.560 -    unfolding midpoint_def dist_norm
   7.561 +    unfolding midpoint_def dist_norm     
   7.562      apply (rule *)
   7.563      apply (simp add: scaleR_right_diff_distrib)
   7.564      apply (simp add: scaleR_2)
   7.565 @@ -6325,37 +6401,28 @@
   7.566    "closed_segment a b = convex hull {a,b}"
   7.567  proof -
   7.568    have *: "\<And>x. {x} \<noteq> {}" by auto
   7.569 -  have **: "\<And>u v. u + v = 1 \<longleftrightarrow> u = 1 - (v::real)" by auto
   7.570    show ?thesis
   7.571      unfolding segment convex_hull_insert[OF *] convex_hull_singleton
   7.572 -    apply (rule set_eqI)
   7.573 -    unfolding mem_Collect_eq
   7.574 -    apply (rule, erule exE)
   7.575 -    apply (rule_tac x="1 - u" in exI)
   7.576 -    apply rule
   7.577 -    defer
   7.578 -    apply (rule_tac x=u in exI)
   7.579 -    defer
   7.580 -    apply (elim exE conjE)
   7.581 -    apply (rule_tac x="1 - u" in exI)
   7.582 -    unfolding **
   7.583 -    apply auto
   7.584 -    done
   7.585 -qed
   7.586 -
   7.587 -lemma convex_segment [iff]: "convex (closed_segment a b)"
   7.588 -  unfolding segment_convex_hull by(rule convex_convex_hull)
   7.589 -
   7.590 -lemma connected_segment [iff]:
   7.591 -  fixes x :: "'a :: real_normed_vector"
   7.592 -  shows "connected (closed_segment x y)"
   7.593 -  by (simp add: convex_connected)
   7.594 +    by (safe; rule_tac x="1 - u" in exI; force)
   7.595 +qed
   7.596 +
   7.597 +lemma segment_open_subset_closed:
   7.598 +   "open_segment a b \<subseteq> closed_segment a b"
   7.599 +  by (auto simp: closed_segment_def open_segment_def)
   7.600 +
   7.601 +lemma bounded_closed_segment:
   7.602 +    fixes a :: "'a::euclidean_space" shows "bounded (closed_segment a b)"
   7.603 +  by (simp add: segment_convex_hull compact_convex_hull compact_imp_bounded)
   7.604 +
   7.605 +lemma bounded_open_segment:
   7.606 +    fixes a :: "'a::euclidean_space" shows "bounded (open_segment a b)"
   7.607 +  by (rule bounded_subset [OF bounded_closed_segment segment_open_subset_closed])
   7.608 +
   7.609 +lemmas bounded_segment = bounded_closed_segment open_closed_segment
   7.610  
   7.611  lemma ends_in_segment [iff]: "a \<in> closed_segment a b" "b \<in> closed_segment a b"
   7.612    unfolding segment_convex_hull
   7.613 -  apply (rule_tac[!] hull_subset[unfolded subset_eq, rule_format])
   7.614 -  apply auto
   7.615 -  done
   7.616 +  by (auto intro!: hull_subset[unfolded subset_eq, rule_format])
   7.617  
   7.618  lemma segment_furthest_le:
   7.619    fixes a b x y :: "'a::euclidean_space"
   7.620 @@ -6403,6 +6470,106 @@
   7.621    fixes u::real shows "closed_segment u v = (\<lambda>x. (v - u) * x + u) ` {0..1}"
   7.622    by (simp add: add.commute [of u] image_affinity_atLeastAtMost [where c=u] closed_segment_eq_real_ivl)
   7.623  
   7.624 +subsubsection\<open>More lemmas, especially for working with the underlying formula\<close>
   7.625 +
   7.626 +lemma segment_eq_compose:
   7.627 +  fixes a :: "'a :: real_vector"
   7.628 +  shows "(\<lambda>u. (1 - u) *\<^sub>R a + u *\<^sub>R b) = (\<lambda>x. a + x) o (\<lambda>u. u *\<^sub>R (b - a))"
   7.629 +    by (simp add: o_def algebra_simps)
   7.630 +
   7.631 +lemma segment_degen_1:
   7.632 +  fixes a :: "'a :: real_vector"
   7.633 +  shows "(1 - u) *\<^sub>R a + u *\<^sub>R b = b \<longleftrightarrow> a=b \<or> u=1"
   7.634 +proof -
   7.635 +  { assume "(1 - u) *\<^sub>R a + u *\<^sub>R b = b"
   7.636 +    then have "(1 - u) *\<^sub>R a = (1 - u) *\<^sub>R b"
   7.637 +      by (simp add: algebra_simps)
   7.638 +    then have "a=b \<or> u=1"
   7.639 +      by simp
   7.640 +  } then show ?thesis
   7.641 +      by (auto simp: algebra_simps)
   7.642 +qed
   7.643 +
   7.644 +lemma segment_degen_0:
   7.645 +    fixes a :: "'a :: real_vector"
   7.646 +    shows "(1 - u) *\<^sub>R a + u *\<^sub>R b = a \<longleftrightarrow> a=b \<or> u=0"
   7.647 +  using segment_degen_1 [of "1-u" b a]
   7.648 +  by (auto simp: algebra_simps)
   7.649 +
   7.650 +lemma closed_segment_image_interval:
   7.651 +     "closed_segment a b = (\<lambda>u. (1 - u) *\<^sub>R a + u *\<^sub>R b) ` {0..1}"
   7.652 +  by (auto simp: set_eq_iff image_iff closed_segment_def)
   7.653 +
   7.654 +lemma open_segment_image_interval:
   7.655 +     "open_segment a b = (if a=b then {} else (\<lambda>u. (1 - u) *\<^sub>R a + u *\<^sub>R b) ` {0<..<1})"
   7.656 +  by (auto simp:  open_segment_def closed_segment_def segment_degen_0 segment_degen_1)
   7.657 +
   7.658 +lemmas segment_image_interval = closed_segment_image_interval open_segment_image_interval
   7.659 +
   7.660 +lemma closure_closed_segment [simp]:
   7.661 +    fixes a :: "'a::euclidean_space"
   7.662 +    shows "closure(closed_segment a b) = closed_segment a b"
   7.663 +  by (simp add: closure_eq compact_imp_closed segment_convex_hull compact_convex_hull)
   7.664 +
   7.665 +lemma closure_open_segment [simp]:
   7.666 +    fixes a :: "'a::euclidean_space"
   7.667 +    shows "closure(open_segment a b) = (if a = b then {} else closed_segment a b)"
   7.668 +proof -
   7.669 +  have "closure ((\<lambda>u. u *\<^sub>R (b - a)) ` {0<..<1}) = (\<lambda>u. u *\<^sub>R (b - a)) ` closure {0<..<1}" if "a \<noteq> b"
   7.670 +    apply (rule closure_injective_linear_image [symmetric])
   7.671 +    apply (simp add:)
   7.672 +    using that by (simp add: inj_on_def)
   7.673 +  then show ?thesis
   7.674 +    by (simp add: segment_image_interval segment_eq_compose closure_greaterThanLessThan [symmetric]
   7.675 +         closure_translation image_comp [symmetric] del: closure_greaterThanLessThan)
   7.676 +qed
   7.677 +
   7.678 +lemma closed_segment [simp]:
   7.679 +    fixes a :: "'a::euclidean_space"  shows "closed (closed_segment a b)"
   7.680 +  using closure_subset_eq by fastforce
   7.681 +
   7.682 +lemma closed_open_segment_iff [simp]:
   7.683 +    fixes a :: "'a::euclidean_space"  shows "closed(open_segment a b) \<longleftrightarrow> a = b"
   7.684 +  by (metis open_segment_def DiffE closure_eq closure_open_segment ends_in_segment(1) insert_iff segment_image_interval(2))
   7.685 +
   7.686 +lemma compact_segment [simp]:
   7.687 +    fixes a :: "'a::euclidean_space"  shows "compact (closed_segment a b)"
   7.688 +  by (simp add: compact_convex_hull segment_convex_hull)
   7.689 +
   7.690 +lemma compact_open_segment_iff [simp]:
   7.691 +    fixes a :: "'a::euclidean_space"  shows "compact(open_segment a b) \<longleftrightarrow> a = b"
   7.692 +  by (simp add: bounded_open_segment compact_eq_bounded_closed)
   7.693 +
   7.694 +lemma convex_closed_segment [iff]: "convex (closed_segment a b)"
   7.695 +  unfolding segment_convex_hull by(rule convex_convex_hull)
   7.696 +
   7.697 +lemma convex_open_segment [iff]: "convex(open_segment a b)"
   7.698 +proof -
   7.699 +  have "convex ((\<lambda>u. u *\<^sub>R (b-a)) ` {0<..<1})"
   7.700 +    by (rule convex_linear_image) auto
   7.701 +  then show ?thesis
   7.702 +    apply (simp add: open_segment_image_interval segment_eq_compose)
   7.703 +    by (metis image_comp convex_translation)
   7.704 +qed
   7.705 +
   7.706 +lemmas convex_segment = convex_closed_segment convex_open_segment
   7.707 +
   7.708 +lemma connected_segment [iff]:
   7.709 +  fixes x :: "'a :: real_normed_vector"
   7.710 +  shows "connected (closed_segment x y)"
   7.711 +  by (simp add: convex_connected)
   7.712 +
   7.713 +lemma affine_hull_closed_segment [simp]:
   7.714 +     "affine hull (closed_segment a b) = affine hull {a,b}"
   7.715 +  by (simp add: segment_convex_hull)
   7.716 +
   7.717 +lemma affine_hull_open_segment [simp]:
   7.718 +    fixes a :: "'a::euclidean_space"
   7.719 +    shows "affine hull (open_segment a b) = (if a = b then {} else affine hull {a,b})"
   7.720 +by (metis affine_hull_convex_hull affine_hull_empty closure_open_segment closure_same_affine_hull segment_convex_hull)
   7.721 +
   7.722 +subsubsection\<open>Betweenness\<close>
   7.723 +
   7.724  lemma between_mem_segment: "between (a,b) x \<longleftrightarrow> x \<in> closed_segment a b"
   7.725    unfolding between_def by auto
   7.726  
   7.727 @@ -6411,7 +6578,7 @@
   7.728    case True
   7.729    then show ?thesis
   7.730      unfolding between_def split_conv
   7.731 -    by (auto simp add:segment_refl dist_commute)
   7.732 +    by (auto simp add: dist_commute)
   7.733  next
   7.734    case False
   7.735    then have Fal: "norm (a - b) \<noteq> 0" and Fal2: "norm (a - b) > 0"
   7.736 @@ -7958,7 +8125,7 @@
   7.737    also have "\<dots> = f ` (closure (rel_interior S))"
   7.738      using convex_closure_rel_interior assms by auto
   7.739    also have "\<dots> \<subseteq> closure (f ` (rel_interior S))"
   7.740 -    using closure_linear_image assms by auto
   7.741 +    using closure_linear_image_subset assms by auto
   7.742    finally have "closure (f ` S) = closure (f ` rel_interior S)"
   7.743      using closure_mono[of "f ` S" "closure (f ` rel_interior S)"] closure_closure
   7.744        closure_mono[of "f ` rel_interior S" "f ` S"] *
   7.745 @@ -8556,7 +8723,7 @@
   7.746    fixes S T :: "'a::real_normed_vector set"
   7.747    shows "closure S + closure T \<subseteq> closure (S + T)"
   7.748    unfolding set_plus_image closure_Times [symmetric] split_def
   7.749 -  by (intro closure_bounded_linear_image bounded_linear_add
   7.750 +  by (intro closure_bounded_linear_image_subset bounded_linear_add
   7.751      bounded_linear_fst bounded_linear_snd)
   7.752  
   7.753  lemma rel_interior_sum:
   7.754 @@ -8929,11 +9096,11 @@
   7.755  
   7.756  lemma interior_atLeastLessThan [simp]:
   7.757    fixes a::real shows "interior {a..<b} = {a<..<b}"
   7.758 -  by (metis atLeastLessThan_def greaterThanLessThan_def interior_atLeastAtMost interior_inter interior_interior interior_real_semiline)
   7.759 +  by (metis atLeastLessThan_def greaterThanLessThan_def interior_atLeastAtMost interior_Int interior_interior interior_real_semiline)
   7.760  
   7.761  lemma interior_lessThanAtMost [simp]:
   7.762    fixes a::real shows "interior {a<..b} = {a<..<b}"
   7.763 -  by (metis atLeastAtMost_def greaterThanAtMost_def interior_atLeastAtMost interior_inter
   7.764 +  by (metis atLeastAtMost_def greaterThanAtMost_def interior_atLeastAtMost interior_Int
   7.765              interior_interior interior_real_semiline)
   7.766  
   7.767  lemma at_within_closed_interval:
     8.1 --- a/src/HOL/Multivariate_Analysis/Derivative.thy	Sun Oct 25 17:31:14 2015 +0100
     8.2 +++ b/src/HOL/Multivariate_Analysis/Derivative.thy	Mon Oct 26 23:41:27 2015 +0000
     8.3 @@ -24,9 +24,6 @@
     8.4      by (rule netlimit_within [of a UNIV])
     8.5  qed simp
     8.6  
     8.7 -(* Because I do not want to type this all the time *)
     8.8 -lemmas linear_linear = linear_conv_bounded_linear[symmetric]
     8.9 -
    8.10  declare has_derivative_bounded_linear[dest]
    8.11  
    8.12  subsection \<open>Derivatives\<close>
     9.1 --- a/src/HOL/Multivariate_Analysis/Integration.thy	Sun Oct 25 17:31:14 2015 +0100
     9.2 +++ b/src/HOL/Multivariate_Analysis/Integration.thy	Mon Oct 26 23:41:27 2015 +0000
     9.3 @@ -1211,7 +1211,7 @@
     9.4        apply (rule arg_cong[of _ _ interior])
     9.5        using p(8) uv by auto
     9.6      also have "\<dots> = {}"
     9.7 -      unfolding interior_inter
     9.8 +      unfolding interior_Int
     9.9        apply (rule inter_interior_unions_intervals)
    9.10        using p(6) p(7)[OF p(2)] p(3)
    9.11        apply auto
    9.12 @@ -4872,7 +4872,7 @@
    9.13              "cbox m n \<inter> {x. \<bar>x \<bullet> k - c\<bar> \<le> d} = cbox u v \<inter> {x. \<bar>x \<bullet> k - c\<bar> \<le> d}"
    9.14            have "(cbox m n \<inter> {x. \<bar>x \<bullet> k - c\<bar> \<le> d}) \<inter> (cbox u v \<inter> {x. \<bar>x \<bullet> k - c\<bar> \<le> d}) \<subseteq> cbox m n \<inter> cbox u v"
    9.15              by blast
    9.16 -          note interior_mono[OF this, unfolded division_ofD(5)[OF p'' as(1-3)] interior_inter[of "cbox m n"]]
    9.17 +          note interior_mono[OF this, unfolded division_ofD(5)[OF p'' as(1-3)] interior_Int[of "cbox m n"]]
    9.18            then have "interior (cbox m n \<inter> {x. \<bar>x \<bullet> k - c\<bar> \<le> d}) = {}"
    9.19              unfolding as Int_absorb by auto
    9.20            then show "content (cbox m n \<inter> {x. \<bar>x \<bullet> k - c\<bar> \<le> d}) = 0"
    9.21 @@ -7341,7 +7341,7 @@
    9.22                guess v' using pa[OF k(2)] .. note v' = conjunctD2[OF this] let ?v = "min v v'"
    9.23                have "box a ?v \<subseteq> k \<inter> k'"
    9.24                  unfolding v v' by (auto simp add: mem_box)
    9.25 -              note interior_mono[OF this,unfolded interior_inter]
    9.26 +              note interior_mono[OF this,unfolded interior_Int]
    9.27                moreover have "(a + ?v)/2 \<in> box a ?v"
    9.28                  using k(3-)
    9.29                  unfolding v v' content_eq_0 not_le
    9.30 @@ -7372,7 +7372,7 @@
    9.31                let ?v = "max v v'"
    9.32                have "box ?v b \<subseteq> k \<inter> k'"
    9.33                  unfolding v v' by (auto simp: mem_box)
    9.34 -                note interior_mono[OF this,unfolded interior_inter]
    9.35 +                note interior_mono[OF this,unfolded interior_Int]
    9.36                moreover have " ((b + ?v)/2) \<in> box ?v b"
    9.37                  using k(3-) unfolding v v' content_eq_0 not_le by (auto simp: mem_box)
    9.38                ultimately have " ((b + ?v)/2) \<in> interior k \<inter> interior k'"
    9.39 @@ -8014,7 +8014,7 @@
    9.40      apply (rule assms(1)[unfolded connected_clopen,rule_format])
    9.41      apply rule
    9.42      defer
    9.43 -    apply (rule continuous_closed_in_preimage[OF assms(4) closed_singleton])
    9.44 +    apply (rule continuous_closedin_preimage[OF assms(4) closed_singleton])
    9.45      apply (rule open_openin_trans[OF assms(2)])
    9.46      unfolding open_contains_ball
    9.47    proof safe
    9.48 @@ -9427,7 +9427,7 @@
    9.49      note kl = tagged_division_ofD(3,4)[OF qq[THEN conjunct1]]
    9.50      from this(2)[OF as(4,1)] guess u v by (elim exE) note uv=this
    9.51      have *: "interior (k \<inter> l) = {}"
    9.52 -      unfolding interior_inter
    9.53 +      unfolding interior_Int
    9.54        apply (rule q')
    9.55        using as
    9.56        unfolding r_def
    9.57 @@ -10771,7 +10771,7 @@
    9.58            proof goal_cases
    9.59              case prems: (1 l y)
    9.60              have "interior (k \<inter> l) \<subseteq> interior (l \<inter> y)"
    9.61 -              apply (subst(2) interior_inter)
    9.62 +              apply (subst(2) interior_Int)
    9.63                apply (rule Int_greatest)
    9.64                defer
    9.65                apply (subst prems(4))
    9.66 @@ -10960,7 +10960,7 @@
    9.67              from d'(4)[OF this(1)] d'(4)[OF this(2)]
    9.68              guess u1 v1 u2 v2 by (elim exE) note uv=this
    9.69              have "{} = interior ((k \<inter> y) \<inter> cbox u v)"
    9.70 -              apply (subst interior_inter)
    9.71 +              apply (subst interior_Int)
    9.72                using d'(5)[OF prems(1-3)]
    9.73                apply auto
    9.74                done
    10.1 --- a/src/HOL/Multivariate_Analysis/Linear_Algebra.thy	Sun Oct 25 17:31:14 2015 +0100
    10.2 +++ b/src/HOL/Multivariate_Analysis/Linear_Algebra.thy	Mon Oct 26 23:41:27 2015 +0000
    10.3 @@ -1507,6 +1507,8 @@
    10.4    show "linear f" ..
    10.5  qed
    10.6  
    10.7 +lemmas linear_linear = linear_conv_bounded_linear[symmetric]
    10.8 +
    10.9  lemma linear_bounded_pos:
   10.10    fixes f :: "'a::euclidean_space \<Rightarrow> 'b::real_normed_vector"
   10.11    assumes lf: "linear f"
    11.1 --- a/src/HOL/Multivariate_Analysis/Multivariate_Analysis.thy	Sun Oct 25 17:31:14 2015 +0100
    11.2 +++ b/src/HOL/Multivariate_Analysis/Multivariate_Analysis.thy	Mon Oct 26 23:41:27 2015 +0000
    11.3 @@ -7,6 +7,7 @@
    11.4    Complex_Analysis_Basics
    11.5    Bounded_Continuous_Function
    11.6    Weierstrass
    11.7 +  Cauchy_Integral_Thm
    11.8  begin
    11.9  
   11.10  end
    12.1 --- a/src/HOL/Multivariate_Analysis/Path_Connected.thy	Sun Oct 25 17:31:14 2015 +0100
    12.2 +++ b/src/HOL/Multivariate_Analysis/Path_Connected.thy	Mon Oct 26 23:41:27 2015 +0000
    12.3 @@ -576,7 +576,7 @@
    12.4    by (rule ext) (auto simp: mult.commute)
    12.5  
    12.6  
    12.7 -subsection\<open>Choosing a subpath of an existing path\<close>
    12.8 +section\<open>Choosing a subpath of an existing path\<close>
    12.9  
   12.10  definition subpath :: "real \<Rightarrow> real \<Rightarrow> (real \<Rightarrow> 'a) \<Rightarrow> real \<Rightarrow> 'a::real_normed_vector"
   12.11    where "subpath a b g \<equiv> \<lambda>x. g((b - a) * x + a)"
   12.12 @@ -747,6 +747,121 @@
   12.13  lemma join_subpaths_middle: "subpath (0) ((1 / 2)) p +++ subpath ((1 / 2)) 1 p = p"
   12.14    by (rule ext) (simp add: joinpaths_def subpath_def divide_simps)
   12.15  
   12.16 +subsection\<open>There is a subpath to the frontier\<close>
   12.17 +
   12.18 +lemma subpath_to_frontier_explicit:
   12.19 +    fixes S :: "'a::metric_space set"
   12.20 +    assumes g: "path g" and "pathfinish g \<notin> S"
   12.21 +    obtains u where "0 \<le> u" "u \<le> 1"
   12.22 +                "\<And>x. 0 \<le> x \<and> x < u \<Longrightarrow> g x \<in> interior S"
   12.23 +                "(g u \<notin> interior S)" "(u = 0 \<or> g u \<in> closure S)"
   12.24 +proof -
   12.25 +  have gcon: "continuous_on {0..1} g"     using g by (simp add: path_def)
   12.26 +  then have com: "compact ({0..1} \<inter> {u. g u \<in> closure (- S)})"
   12.27 +    apply (simp add: Int_commute [of "{0..1}"] compact_eq_bounded_closed closed_vimage_Int [unfolded vimage_def])
   12.28 +    using compact_eq_bounded_closed apply fastforce
   12.29 +    done
   12.30 +  have "1 \<in> {u. g u \<in> closure (- S)}"
   12.31 +    using assms by (simp add: pathfinish_def closure_def)
   12.32 +  then have dis: "{0..1} \<inter> {u. g u \<in> closure (- S)} \<noteq> {}"
   12.33 +    using atLeastAtMost_iff zero_le_one by blast
   12.34 +  then obtain u where "0 \<le> u" "u \<le> 1" and gu: "g u \<in> closure (- S)"
   12.35 +                  and umin: "\<And>t. \<lbrakk>0 \<le> t; t \<le> 1; g t \<in> closure (- S)\<rbrakk> \<Longrightarrow> u \<le> t"
   12.36 +    using compact_attains_inf [OF com dis] by fastforce
   12.37 +  then have umin': "\<And>t. \<lbrakk>0 \<le> t; t \<le> 1; t < u\<rbrakk> \<Longrightarrow>  g t \<in> S"
   12.38 +    using closure_def by fastforce
   12.39 +  { assume "u \<noteq> 0"
   12.40 +    then have "u > 0" using `0 \<le> u` by auto
   12.41 +    { fix e::real assume "e > 0"
   12.42 +      obtain d where "d>0" and d: "\<And>x'. \<lbrakk>x' \<in> {0..1}; dist x' u < d\<rbrakk> \<Longrightarrow> dist (g x') (g u) < e"
   12.43 +        using continuous_onD [OF gcon _ `e > 0`] `0 \<le> _` `_ \<le> 1` atLeastAtMost_iff by auto
   12.44 +      have *: "dist (max 0 (u - d / 2)) u < d"
   12.45 +        using `0 \<le> u` `u \<le> 1` `d > 0` by (simp add: dist_real_def)
   12.46 +      have "\<exists>y\<in>S. dist y (g u) < e"
   12.47 +        using `0 < u` `u \<le> 1` `d > 0`
   12.48 +        by (force intro: d [OF _ *] umin')
   12.49 +    }
   12.50 +    then have "g u \<in> closure S"
   12.51 +      by (simp add: frontier_def closure_approachable)
   12.52 +  }
   12.53 +  then show ?thesis
   12.54 +    apply (rule_tac u=u in that)
   12.55 +    apply (auto simp: `0 \<le> u` `u \<le> 1` gu interior_closure umin)
   12.56 +    using `_ \<le> 1` interior_closure umin apply fastforce
   12.57 +    done
   12.58 +qed
   12.59 +
   12.60 +lemma subpath_to_frontier_strong:
   12.61 +    assumes g: "path g" and "pathfinish g \<notin> S"
   12.62 +    obtains u where "0 \<le> u" "u \<le> 1" "g u \<notin> interior S"
   12.63 +                    "u = 0 \<or> (\<forall>x. 0 \<le> x \<and> x < 1 \<longrightarrow> subpath 0 u g x \<in> interior S)  \<and>  g u \<in> closure S"
   12.64 +proof -
   12.65 +  obtain u where "0 \<le> u" "u \<le> 1"
   12.66 +             and gxin: "\<And>x. 0 \<le> x \<and> x < u \<Longrightarrow> g x \<in> interior S"
   12.67 +             and gunot: "(g u \<notin> interior S)" and u0: "(u = 0 \<or> g u \<in> closure S)"
   12.68 +    using subpath_to_frontier_explicit [OF assms] by blast
   12.69 +  show ?thesis
   12.70 +    apply (rule that [OF `0 \<le> u` `u \<le> 1`])
   12.71 +    apply (simp add: gunot)
   12.72 +    using `0 \<le> u` u0 by (force simp: subpath_def gxin)
   12.73 +qed
   12.74 +
   12.75 +lemma subpath_to_frontier:
   12.76 +    assumes g: "path g" and g0: "pathstart g \<in> closure S" and g1: "pathfinish g \<notin> S"
   12.77 +    obtains u where "0 \<le> u" "u \<le> 1" "g u \<in> frontier S" "(path_image(subpath 0 u g) - {g u}) \<subseteq> interior S"
   12.78 +proof -
   12.79 +  obtain u where "0 \<le> u" "u \<le> 1"
   12.80 +             and notin: "g u \<notin> interior S"
   12.81 +             and disj: "u = 0 \<or>
   12.82 +                        (\<forall>x. 0 \<le> x \<and> x < 1 \<longrightarrow> subpath 0 u g x \<in> interior S) \<and> g u \<in> closure S"
   12.83 +    using subpath_to_frontier_strong [OF g g1] by blast
   12.84 +  show ?thesis
   12.85 +    apply (rule that [OF `0 \<le> u` `u \<le> 1`])
   12.86 +    apply (metis DiffI disj frontier_def g0 notin pathstart_def)
   12.87 +    using `0 \<le> u` g0 disj
   12.88 +    apply (simp add:)
   12.89 +    apply (auto simp: closed_segment_eq_real_ivl pathstart_def pathfinish_def subpath_def)
   12.90 +    apply (rename_tac y)
   12.91 +    apply (drule_tac x="y/u" in spec)
   12.92 +    apply (auto split: split_if_asm)
   12.93 +    done
   12.94 +qed
   12.95 +
   12.96 +lemma exists_path_subpath_to_frontier:
   12.97 +    fixes S :: "'a::real_normed_vector set"
   12.98 +    assumes "path g" "pathstart g \<in> closure S" "pathfinish g \<notin> S"
   12.99 +    obtains h where "path h" "pathstart h = pathstart g" "path_image h \<subseteq> path_image g"
  12.100 +                    "path_image h - {pathfinish h} \<subseteq> interior S"
  12.101 +                    "pathfinish h \<in> frontier S"
  12.102 +proof -
  12.103 +  obtain u where u: "0 \<le> u" "u \<le> 1" "g u \<in> frontier S" "(path_image(subpath 0 u g) - {g u}) \<subseteq> interior S"
  12.104 +    using subpath_to_frontier [OF assms] by blast
  12.105 +  show ?thesis
  12.106 +    apply (rule that [of "subpath 0 u g"])
  12.107 +    using assms u
  12.108 +    apply simp_all
  12.109 +    apply (simp add: pathstart_def)
  12.110 +    apply (force simp: closed_segment_eq_real_ivl path_image_def)
  12.111 +    done
  12.112 +qed
  12.113 +
  12.114 +lemma exists_path_subpath_to_frontier_closed:
  12.115 +    fixes S :: "'a::real_normed_vector set"
  12.116 +    assumes S: "closed S" and g: "path g" and g0: "pathstart g \<in> S" and g1: "pathfinish g \<notin> S"
  12.117 +    obtains h where "path h" "pathstart h = pathstart g" "path_image h \<subseteq> path_image g \<inter> S"
  12.118 +                    "pathfinish h \<in> frontier S"
  12.119 +proof -
  12.120 +  obtain h where h: "path h" "pathstart h = pathstart g" "path_image h \<subseteq> path_image g"
  12.121 +                    "path_image h - {pathfinish h} \<subseteq> interior S"
  12.122 +                    "pathfinish h \<in> frontier S"
  12.123 +    using exists_path_subpath_to_frontier [OF g _ g1] closure_closed [OF S] g0 by auto
  12.124 +  show ?thesis
  12.125 +    apply (rule that [OF `path h`])
  12.126 +    using assms h
  12.127 +    apply auto
  12.128 +    apply (metis diff_single_insert frontier_subset_eq insert_iff interior_subset subset_iff)
  12.129 +    done
  12.130 +qed
  12.131  
  12.132  subsection \<open>Reparametrizing a closed curve to start at some chosen point\<close>
  12.133  
  12.134 @@ -937,7 +1052,7 @@
  12.135  qed
  12.136  
  12.137  
  12.138 -subsection \<open>Path component, considered as a "joinability" relation (from Tom Hales)\<close>
  12.139 +section \<open>Path component, considered as a "joinability" relation (from Tom Hales)\<close>
  12.140  
  12.141  definition "path_component s x y \<longleftrightarrow>
  12.142    (\<exists>g. path g \<and> path_image g \<subseteq> s \<and> pathstart g = x \<and> pathfinish g = y)"
  12.143 @@ -1079,8 +1194,8 @@
  12.144    ultimately show False
  12.145      using *[unfolded connected_local not_ex, rule_format,
  12.146        of "{x\<in>{0..1}. g x \<in> e1}" "{x\<in>{0..1}. g x \<in> e2}"]
  12.147 -    using continuous_open_in_preimage[OF g(1)[unfolded path_def] as(1)]
  12.148 -    using continuous_open_in_preimage[OF g(1)[unfolded path_def] as(2)]
  12.149 +    using continuous_openin_preimage[OF g(1)[unfolded path_def] as(1)]
  12.150 +    using continuous_openin_preimage[OF g(1)[unfolded path_def] as(2)]
  12.151      by auto
  12.152  qed
  12.153  
  12.154 @@ -1199,6 +1314,16 @@
  12.155      done
  12.156  qed
  12.157  
  12.158 +lemma path_connected_segment:
  12.159 +    fixes a :: "'a::real_normed_vector"
  12.160 +    shows "path_connected (closed_segment a b)"
  12.161 +  by (simp add: convex_imp_path_connected)
  12.162 +
  12.163 +lemma path_connected_open_segment:
  12.164 +    fixes a :: "'a::real_normed_vector"
  12.165 +    shows "path_connected (open_segment a b)"
  12.166 +  by (simp add: convex_imp_path_connected)
  12.167 +
  12.168  lemma homeomorphic_path_connectedness:
  12.169    "s homeomorphic t \<Longrightarrow> path_connected s \<longleftrightarrow> path_connected t"
  12.170    unfolding homeomorphic_def homeomorphism_def
  12.171 @@ -1667,7 +1792,7 @@
  12.172    by (meson cobounded_unique_unbounded_components connected_eq_connected_components_eq)
  12.173  
  12.174  
  12.175 -subsection\<open>The "inside" and "outside" of a set\<close>
  12.176 +section\<open>The "inside" and "outside" of a set\<close>
  12.177  
  12.178  text\<open>The inside comprises the points in a bounded connected component of the set's complement.
  12.179    The outside comprises the points in unbounded connected component of the complement.\<close>
  12.180 @@ -1994,6 +2119,14 @@
  12.181  by (metis Diff_subset assms convex_closure frontier_def outside_frontier_misses_closure
  12.182            outside_subset_convex subset_antisym)
  12.183  
  12.184 +lemma inside_frontier_eq_interior:
  12.185 +     fixes s :: "'a :: {real_normed_vector, perfect_space} set"
  12.186 +     shows "\<lbrakk>bounded s; convex s\<rbrakk> \<Longrightarrow> inside(frontier s) = interior s"
  12.187 +  apply (simp add: inside_outside outside_frontier_eq_complement_closure)
  12.188 +  using closure_subset interior_subset
  12.189 +  apply (auto simp add: frontier_def)
  12.190 +  done
  12.191 +
  12.192  lemma open_inside:
  12.193      fixes s :: "'a::real_normed_vector set"
  12.194      assumes "closed s"
  12.195 @@ -2055,4 +2188,271 @@
  12.196      by (simp add: frontier_def open_inside interior_open)
  12.197  qed
  12.198  
  12.199 +lemma closure_outside_subset:
  12.200 +    fixes s :: "'a::real_normed_vector set"
  12.201 +    assumes "closed s"
  12.202 +      shows "closure(outside s) \<subseteq> s \<union> outside s"
  12.203 +  apply (rule closure_minimal, simp)
  12.204 +  by (metis assms closed_open inside_outside open_inside)
  12.205 +
  12.206 +lemma frontier_outside_subset:
  12.207 +    fixes s :: "'a::real_normed_vector set"
  12.208 +    assumes "closed s"
  12.209 +      shows "frontier(outside s) \<subseteq> s"
  12.210 +  apply (simp add: frontier_def open_outside interior_open)
  12.211 +  by (metis Diff_subset_conv assms closure_outside_subset interior_eq open_outside sup.commute)
  12.212 +
  12.213 +lemma inside_complement_unbounded_connected_empty:
  12.214 +     "\<lbrakk>connected (- s); \<not> bounded (- s)\<rbrakk> \<Longrightarrow> inside s = {}"
  12.215 +  apply (simp add: inside_def)
  12.216 +  by (meson Compl_iff bounded_subset connected_component_maximal order_refl)
  12.217 +
  12.218 +lemma inside_bounded_complement_connected_empty:
  12.219 +    fixes s :: "'a::{real_normed_vector, perfect_space} set"
  12.220 +    shows "\<lbrakk>connected (- s); bounded s\<rbrakk> \<Longrightarrow> inside s = {}"
  12.221 +  by (metis inside_complement_unbounded_connected_empty cobounded_imp_unbounded)
  12.222 +
  12.223 +lemma inside_inside:
  12.224 +    assumes "s \<subseteq> inside t"
  12.225 +    shows "inside s - t \<subseteq> inside t"
  12.226 +unfolding inside_def
  12.227 +proof clarify
  12.228 +  fix x
  12.229 +  assume x: "x \<notin> t" "x \<notin> s" and bo: "bounded (connected_component_set (- s) x)"
  12.230 +  show "bounded (connected_component_set (- t) x)"
  12.231 +  proof (cases "s \<inter> connected_component_set (- t) x = {}")
  12.232 +    case True show ?thesis
  12.233 +      apply (rule bounded_subset [OF bo])
  12.234 +      apply (rule connected_component_maximal)
  12.235 +      using x True apply auto
  12.236 +      done
  12.237 +  next
  12.238 +    case False then show ?thesis
  12.239 +      using assms [unfolded inside_def] x
  12.240 +      apply (simp add: disjoint_iff_not_equal, clarify)
  12.241 +      apply (drule subsetD, assumption, auto)
  12.242 +      by (metis (no_types, hide_lams) ComplI connected_component_eq_eq)
  12.243 +  qed
  12.244 +qed
  12.245 +
  12.246 +lemma inside_inside_subset: "inside(inside s) \<subseteq> s"
  12.247 +  using inside_inside union_with_outside by fastforce
  12.248 +
  12.249 +lemma inside_outside_intersect_connected:
  12.250 +      "\<lbrakk>connected t; inside s \<inter> t \<noteq> {}; outside s \<inter> t \<noteq> {}\<rbrakk> \<Longrightarrow> s \<inter> t \<noteq> {}"
  12.251 +  apply (simp add: inside_def outside_def ex_in_conv [symmetric] disjoint_eq_subset_Compl, clarify)
  12.252 +  by (metis (no_types, hide_lams) Compl_anti_mono connected_component_eq connected_component_maximal contra_subsetD double_compl)
  12.253 +
  12.254 +lemma outside_bounded_nonempty:
  12.255 +  fixes s :: "'a :: {real_normed_vector, perfect_space} set"
  12.256 +    assumes "bounded s" shows "outside s \<noteq> {}"
  12.257 +  by (metis (no_types, lifting) Collect_empty_eq Collect_mem_eq Compl_eq_Diff_UNIV Diff_cancel
  12.258 +                   Diff_disjoint UNIV_I assms ball_eq_empty bounded_diff cobounded_outside convex_ball
  12.259 +                   double_complement order_refl outside_convex outside_def)
  12.260 +
  12.261 +lemma outside_compact_in_open:
  12.262 +    fixes s :: "'a :: {real_normed_vector,perfect_space} set"
  12.263 +    assumes s: "compact s" and t: "open t" and "s \<subseteq> t" "t \<noteq> {}"
  12.264 +      shows "outside s \<inter> t \<noteq> {}"
  12.265 +proof -
  12.266 +  have "outside s \<noteq> {}"
  12.267 +    by (simp add: compact_imp_bounded outside_bounded_nonempty s)
  12.268 +  with assms obtain a b where a: "a \<in> outside s" and b: "b \<in> t" by auto
  12.269 +  show ?thesis
  12.270 +  proof (cases "a \<in> t")
  12.271 +    case True with a show ?thesis by blast
  12.272 +  next
  12.273 +    case False
  12.274 +      have front: "frontier t \<subseteq> - s"
  12.275 +        using `s \<subseteq> t` frontier_disjoint_eq t by auto
  12.276 +      { fix \<gamma>
  12.277 +        assume "path \<gamma>" and pimg_sbs: "path_image \<gamma> - {pathfinish \<gamma>} \<subseteq> interior (- t)"
  12.278 +           and pf: "pathfinish \<gamma> \<in> frontier t" and ps: "pathstart \<gamma> = a"
  12.279 +        def c \<equiv> "pathfinish \<gamma>"
  12.280 +        have "c \<in> -s" unfolding c_def using front pf by blast
  12.281 +        moreover have "open (-s)" using s compact_imp_closed by blast
  12.282 +        ultimately obtain \<epsilon>::real where "\<epsilon> > 0" and \<epsilon>: "cball c \<epsilon> \<subseteq> -s"
  12.283 +          using open_contains_cball[of "-s"] s by blast
  12.284 +        then obtain d where "d \<in> t" and d: "dist d c < \<epsilon>"
  12.285 +          using closure_approachable [of c t] pf unfolding c_def
  12.286 +          by (metis Diff_iff frontier_def)
  12.287 +        then have "d \<in> -s" using \<epsilon>
  12.288 +          using dist_commute by (metis contra_subsetD mem_cball not_le not_less_iff_gr_or_eq)
  12.289 +        have pimg_sbs_cos: "path_image \<gamma> \<subseteq> -s"
  12.290 +          using pimg_sbs apply (auto simp: path_image_def)
  12.291 +          apply (drule subsetD)
  12.292 +          using `c \<in> - s` `s \<subseteq> t` interior_subset apply (auto simp: c_def)
  12.293 +          done
  12.294 +        have "closed_segment c d \<le> cball c \<epsilon>"
  12.295 +          apply (simp add: segment_convex_hull)
  12.296 +          apply (rule hull_minimal)
  12.297 +          using  `\<epsilon> > 0` d apply (auto simp: dist_commute)
  12.298 +          done
  12.299 +        with \<epsilon> have "closed_segment c d \<subseteq> -s" by blast
  12.300 +        moreover have con_gcd: "connected (path_image \<gamma> \<union> closed_segment c d)"
  12.301 +          by (rule connected_Un) (auto simp: c_def `path \<gamma>` connected_path_image)
  12.302 +        ultimately have "connected_component (- s) a d"
  12.303 +          unfolding connected_component_def using pimg_sbs_cos ps by blast
  12.304 +        then have "outside s \<inter> t \<noteq> {}"
  12.305 +          using outside_same_component [OF _ a]  by (metis IntI `d \<in> t` empty_iff)
  12.306 +      } note * = this
  12.307 +      have pal: "pathstart (linepath a b) \<in> closure (- t)"
  12.308 +        by (auto simp: False closure_def)
  12.309 +      show ?thesis
  12.310 +        by (rule exists_path_subpath_to_frontier [OF path_linepath pal _ *]) (auto simp: b)
  12.311 +  qed
  12.312 +qed
  12.313 +
  12.314 +lemma inside_inside_compact_connected:
  12.315 +    fixes s :: "'a :: euclidean_space set"
  12.316 +    assumes s: "closed s" and t: "compact t" and "connected t" "s \<subseteq> inside t"
  12.317 +      shows "inside s \<subseteq> inside t"
  12.318 +proof (cases "inside t = {}")
  12.319 +  case True with assms show ?thesis by auto
  12.320 +next
  12.321 +  case False
  12.322 +  consider "DIM('a) = 1" | "DIM('a) \<ge> 2"
  12.323 +    using antisym not_less_eq_eq by fastforce
  12.324 +  then show ?thesis
  12.325 +  proof cases
  12.326 +    case 1 then show ?thesis
  12.327 +             using connected_convex_1_gen assms False inside_convex by blast
  12.328 +  next
  12.329 +    case 2
  12.330 +    have coms: "compact s"
  12.331 +      using assms apply (simp add: s compact_eq_bounded_closed)
  12.332 +       by (meson bounded_inside bounded_subset compact_imp_bounded)
  12.333 +    then have bst: "bounded (s \<union> t)"
  12.334 +      by (simp add: compact_imp_bounded t)
  12.335 +    then obtain r where "0 < r" and r: "s \<union> t \<subseteq> ball 0 r"
  12.336 +      using bounded_subset_ballD by blast
  12.337 +    have outst: "outside s \<inter> outside t \<noteq> {}"
  12.338 +    proof -
  12.339 +      have "- ball 0 r \<subseteq> outside s"
  12.340 +        apply (rule outside_subset_convex)
  12.341 +        using r by auto
  12.342 +      moreover have "- ball 0 r \<subseteq> outside t"
  12.343 +        apply (rule outside_subset_convex)
  12.344 +        using r by auto
  12.345 +      ultimately show ?thesis
  12.346 +        by (metis Compl_subset_Compl_iff Int_subset_iff bounded_ball inf.orderE outside_bounded_nonempty outside_no_overlap)
  12.347 +    qed
  12.348 +    have "s \<inter> t = {}" using assms
  12.349 +      by (metis disjoint_iff_not_equal inside_no_overlap subsetCE)
  12.350 +    moreover have "outside s \<inter> inside t \<noteq> {}"
  12.351 +      by (meson False assms(4) compact_eq_bounded_closed coms open_inside outside_compact_in_open t)
  12.352 +    ultimately have "inside s \<inter> t = {}"
  12.353 +      using inside_outside_intersect_connected [OF `connected t`, of s]
  12.354 +      by (metis "2" compact_eq_bounded_closed coms connected_outside inf.commute inside_outside_intersect_connected outst)
  12.355 +    then show ?thesis
  12.356 +      using inside_inside [OF `s \<subseteq> inside t`] by blast
  12.357 +  qed
  12.358 +qed
  12.359 +
  12.360 +lemma connected_with_inside:
  12.361 +    fixes s :: "'a :: real_normed_vector set"
  12.362 +    assumes s: "closed s" and cons: "connected s"
  12.363 +      shows "connected(s \<union> inside s)"
  12.364 +proof (cases "s \<union> inside s = UNIV")
  12.365 +  case True with assms show ?thesis by auto
  12.366 +next
  12.367 +  case False
  12.368 +  then obtain b where b: "b \<notin> s" "b \<notin> inside s" by blast
  12.369 +  have *: "\<exists>y t. y \<in> s \<and> connected t \<and> a \<in> t \<and> y \<in> t \<and> t \<subseteq> (s \<union> inside s)" if "a \<in> (s \<union> inside s)" for a
  12.370 +  using that proof
  12.371 +    assume "a \<in> s" then show ?thesis
  12.372 +      apply (rule_tac x=a in exI)
  12.373 +      apply (rule_tac x="{a}" in exI)
  12.374 +      apply (simp add:)
  12.375 +      done
  12.376 +  next
  12.377 +    assume a: "a \<in> inside s"
  12.378 +    show ?thesis
  12.379 +      apply (rule exists_path_subpath_to_frontier [OF path_linepath [of a b], of "inside s"])
  12.380 +      using a apply (simp add: closure_def)
  12.381 +      apply (simp add: b)
  12.382 +      apply (rule_tac x="pathfinish h" in exI)
  12.383 +      apply (rule_tac x="path_image h" in exI)
  12.384 +      apply (simp add: pathfinish_in_path_image connected_path_image, auto)
  12.385 +      using frontier_inside_subset s apply fastforce
  12.386 +      by (metis (no_types, lifting) frontier_inside_subset insertE insert_Diff interior_eq open_inside pathfinish_in_path_image s subsetCE)
  12.387 +  qed
  12.388 +  show ?thesis
  12.389 +    apply (simp add: connected_iff_connected_component)
  12.390 +    apply (simp add: connected_component_def)
  12.391 +    apply (clarify dest!: *)
  12.392 +    apply (rename_tac u u' t t')
  12.393 +    apply (rule_tac x="(s \<union> t \<union> t')" in exI)
  12.394 +    apply (auto simp: intro!: connected_Un cons)
  12.395 +    done
  12.396 +qed
  12.397 +
  12.398 +text\<open>The proof is virtually the same as that above.\<close>
  12.399 +lemma connected_with_outside:
  12.400 +    fixes s :: "'a :: real_normed_vector set"
  12.401 +    assumes s: "closed s" and cons: "connected s"
  12.402 +      shows "connected(s \<union> outside s)"
  12.403 +proof (cases "s \<union> outside s = UNIV")
  12.404 +  case True with assms show ?thesis by auto
  12.405 +next
  12.406 +  case False
  12.407 +  then obtain b where b: "b \<notin> s" "b \<notin> outside s" by blast
  12.408 +  have *: "\<exists>y t. y \<in> s \<and> connected t \<and> a \<in> t \<and> y \<in> t \<and> t \<subseteq> (s \<union> outside s)" if "a \<in> (s \<union> outside s)" for a
  12.409 +  using that proof
  12.410 +    assume "a \<in> s" then show ?thesis
  12.411 +      apply (rule_tac x=a in exI)
  12.412 +      apply (rule_tac x="{a}" in exI)
  12.413 +      apply (simp add:)
  12.414 +      done
  12.415 +  next
  12.416 +    assume a: "a \<in> outside s"
  12.417 +    show ?thesis
  12.418 +      apply (rule exists_path_subpath_to_frontier [OF path_linepath [of a b], of "outside s"])
  12.419 +      using a apply (simp add: closure_def)
  12.420 +      apply (simp add: b)
  12.421 +      apply (rule_tac x="pathfinish h" in exI)
  12.422 +      apply (rule_tac x="path_image h" in exI)
  12.423 +      apply (simp add: pathfinish_in_path_image connected_path_image, auto)
  12.424 +      using frontier_outside_subset s apply fastforce
  12.425 +      by (metis (no_types, lifting) frontier_outside_subset insertE insert_Diff interior_eq open_outside pathfinish_in_path_image s subsetCE)
  12.426 +  qed
  12.427 +  show ?thesis
  12.428 +    apply (simp add: connected_iff_connected_component)
  12.429 +    apply (simp add: connected_component_def)
  12.430 +    apply (clarify dest!: *)
  12.431 +    apply (rename_tac u u' t t')
  12.432 +    apply (rule_tac x="(s \<union> t \<union> t')" in exI)
  12.433 +    apply (auto simp: intro!: connected_Un cons)
  12.434 +    done
  12.435 +qed
  12.436 +
  12.437 +lemma inside_inside_eq_empty [simp]:
  12.438 +    fixes s :: "'a :: {real_normed_vector, perfect_space} set"
  12.439 +    assumes s: "closed s" and cons: "connected s"
  12.440 +      shows "inside (inside s) = {}"
  12.441 +  by (metis (no_types) unbounded_outside connected_with_outside [OF assms] bounded_Un
  12.442 +           inside_complement_unbounded_connected_empty unbounded_outside union_with_outside)
  12.443 +
  12.444 +lemma inside_in_components:
  12.445 +     "inside s \<in> components (- s) \<longleftrightarrow> connected(inside s) \<and> inside s \<noteq> {}"
  12.446 +  apply (simp add: in_components_maximal)
  12.447 +  apply (auto intro: inside_same_component connected_componentI)
  12.448 +  apply (metis IntI empty_iff inside_no_overlap)
  12.449 +  done
  12.450 +
  12.451 +text\<open>The proof is virtually the same as that above.\<close>
  12.452 +lemma outside_in_components:
  12.453 +     "outside s \<in> components (- s) \<longleftrightarrow> connected(outside s) \<and> outside s \<noteq> {}"
  12.454 +  apply (simp add: in_components_maximal)
  12.455 +  apply (auto intro: outside_same_component connected_componentI)
  12.456 +  apply (metis IntI empty_iff outside_no_overlap)
  12.457 +  done
  12.458 +
  12.459 +lemma bounded_unique_outside:
  12.460 +    fixes s :: "'a :: euclidean_space set"
  12.461 +    shows "\<lbrakk>bounded s; DIM('a) \<ge> 2\<rbrakk> \<Longrightarrow> (c \<in> components (- s) \<and> ~bounded c \<longleftrightarrow> c = outside s)"
  12.462 +  apply (rule iffI)
  12.463 +  apply (metis cobounded_unique_unbounded_components connected_outside double_compl outside_bounded_nonempty outside_in_components unbounded_outside)
  12.464 +  by (simp add: connected_outside outside_bounded_nonempty outside_in_components unbounded_outside)
  12.465 +
  12.466  end
    13.1 --- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Sun Oct 25 17:31:14 2015 +0100
    13.2 +++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Mon Oct 26 23:41:27 2015 +0000
    13.3 @@ -513,9 +513,6 @@
    13.4  lemma closedin_Int[intro]: "closedin U S \<Longrightarrow> closedin U T \<Longrightarrow> closedin U (S \<inter> T)"
    13.5    using closedin_Inter[of "{S,T}" U] by auto
    13.6  
    13.7 -lemma Diff_Diff_Int: "A - (A - B) = A \<inter> B"
    13.8 -  by blast
    13.9 -
   13.10  lemma openin_closedin_eq: "openin U S \<longleftrightarrow> S \<subseteq> topspace U \<and> closedin U (topspace U - S)"
   13.11    apply (auto simp add: closedin_def Diff_Diff_Int inf_absorb2)
   13.12    apply (metis openin_subset subset_eq)
   13.13 @@ -790,6 +787,13 @@
   13.14  lemma closedin_closed_trans: "closedin (subtopology euclidean T) S \<Longrightarrow> closed T \<Longrightarrow> closed S"
   13.15    by (auto simp add: closedin_closed intro: closedin_trans)
   13.16  
   13.17 +lemma openin_subtopology_inter_subset:
   13.18 +   "openin (subtopology euclidean u) (u \<inter> s) \<and> v \<subseteq> u \<Longrightarrow> openin (subtopology euclidean v) (v \<inter> s)"
   13.19 +  by (auto simp: openin_subtopology)
   13.20 +
   13.21 +lemma openin_open_eq: "open s \<Longrightarrow> (openin (subtopology euclidean s) t \<longleftrightarrow> open t \<and> t \<subseteq> s)"
   13.22 +  using open_subset openin_open_trans openin_subset by fastforce
   13.23 +
   13.24  
   13.25  subsection \<open>Open and closed balls\<close>
   13.26  
   13.27 @@ -805,23 +809,29 @@
   13.28  lemma mem_cball [simp]: "y \<in> cball x e \<longleftrightarrow> dist x y \<le> e"
   13.29    by (simp add: cball_def)
   13.30  
   13.31 -lemma mem_ball_0:
   13.32 +lemma ball_trivial [simp]: "ball x 0 = {}"
   13.33 +  by (simp add: ball_def)
   13.34 +
   13.35 +lemma cball_trivial [simp]: "cball x 0 = {x}"
   13.36 +  by (simp add: cball_def)
   13.37 +
   13.38 +lemma mem_ball_0 [simp]:
   13.39    fixes x :: "'a::real_normed_vector"
   13.40    shows "x \<in> ball 0 e \<longleftrightarrow> norm x < e"
   13.41    by (simp add: dist_norm)
   13.42  
   13.43 -lemma mem_cball_0:
   13.44 +lemma mem_cball_0 [simp]:
   13.45    fixes x :: "'a::real_normed_vector"
   13.46    shows "x \<in> cball 0 e \<longleftrightarrow> norm x \<le> e"
   13.47    by (simp add: dist_norm)
   13.48  
   13.49 -lemma centre_in_ball: "x \<in> ball x e \<longleftrightarrow> 0 < e"
   13.50 +lemma centre_in_ball [simp]: "x \<in> ball x e \<longleftrightarrow> 0 < e"
   13.51    by simp
   13.52  
   13.53 -lemma centre_in_cball: "x \<in> cball x e \<longleftrightarrow> 0 \<le> e"
   13.54 +lemma centre_in_cball [simp]: "x \<in> cball x e \<longleftrightarrow> 0 \<le> e"
   13.55    by simp
   13.56  
   13.57 -lemma ball_subset_cball[simp,intro]: "ball x e \<subseteq> cball x e"
   13.58 +lemma ball_subset_cball [simp,intro]: "ball x e \<subseteq> cball x e"
   13.59    by (simp add: subset_eq)
   13.60  
   13.61  lemma subset_ball[intro]: "d \<le> e \<Longrightarrow> ball x d \<subseteq> ball x e"
   13.62 @@ -1547,7 +1557,12 @@
   13.63    shows "interior S = T"
   13.64    by (intro equalityI assms interior_subset open_interior interior_maximal)
   13.65  
   13.66 -lemma interior_inter [simp]: "interior (S \<inter> T) = interior S \<inter> interior T"
   13.67 +lemma interior_singleton [simp]:
   13.68 +      fixes a :: "'a::perfect_space" shows "interior {a} = {}"
   13.69 +  apply (rule interior_unique, simp_all)
   13.70 +  using not_open_singleton subset_singletonD by fastforce
   13.71 +
   13.72 +lemma interior_Int [simp]: "interior (S \<inter> T) = interior S \<inter> interior T"
   13.73    by (intro equalityI Int_mono Int_greatest interior_mono Int_lower1
   13.74      Int_lower2 interior_maximal interior_subset open_Int open_interior)
   13.75  
   13.76 @@ -1801,6 +1816,10 @@
   13.77    apply (force simp: closure_def)
   13.78    done
   13.79  
   13.80 +lemma closedin_closed_eq:
   13.81 +    "closed s \<Longrightarrow> (closedin (subtopology euclidean s) t \<longleftrightarrow> closed t \<and> t \<subseteq> s)"
   13.82 +  by (meson closed_in_limpt closed_subset closedin_closed_trans)
   13.83 +
   13.84  subsection\<open>Connected components, considered as a connectedness relation or a set\<close>
   13.85  
   13.86  definition
   13.87 @@ -2171,7 +2190,7 @@
   13.88    then show ?thesis using frontier_subset_closed[of S] ..
   13.89  qed
   13.90  
   13.91 -lemma frontier_complement: "frontier (- S) = frontier S"
   13.92 +lemma frontier_complement  [simp]: "frontier (- S) = frontier S"
   13.93    by (auto simp add: frontier_def closure_complement interior_complement)
   13.94  
   13.95  lemma frontier_disjoint_eq: "frontier S \<inter> S = {} \<longleftrightarrow> open S"
   13.96 @@ -5128,6 +5147,11 @@
   13.97  
   13.98  text\<open>Some simple consequential lemmas.\<close>
   13.99  
  13.100 +lemma continuous_onD:
  13.101 +    assumes "continuous_on s f" "x\<in>s" "e>0"
  13.102 +    obtains d where "d>0"  "\<And>x'. \<lbrakk>x' \<in> s; dist x' x < d\<rbrakk> \<Longrightarrow> dist (f x') (f x) < e"
  13.103 +  using assms [unfolded continuous_on_iff] by blast
  13.104 +
  13.105  lemma uniformly_continuous_onE:
  13.106    assumes "uniformly_continuous_on s f" "0 < e"
  13.107    obtains d where "d>0" "\<And>x x'. \<lbrakk>x\<in>s; x'\<in>s; dist x' x < d\<rbrakk> \<Longrightarrow> dist (f x') (f x) < e"
  13.108 @@ -5514,7 +5538,7 @@
  13.109  
  13.110  text \<open>Half-global and completely global cases.\<close>
  13.111  
  13.112 -lemma continuous_open_in_preimage:
  13.113 +lemma continuous_openin_preimage:
  13.114    assumes "continuous_on s f"  "open t"
  13.115    shows "openin (subtopology euclidean s) {x \<in> s. f x \<in> t}"
  13.116  proof -
  13.117 @@ -5527,7 +5551,7 @@
  13.118      using * by auto
  13.119  qed
  13.120  
  13.121 -lemma continuous_closed_in_preimage:
  13.122 +lemma continuous_closedin_preimage:
  13.123    assumes "continuous_on s f" and "closed t"
  13.124    shows "closedin (subtopology euclidean s) {x \<in> s. f x \<in> t}"
  13.125  proof -
  13.126 @@ -5548,7 +5572,7 @@
  13.127    shows "open {x \<in> s. f x \<in> t}"
  13.128  proof-
  13.129    obtain T where T: "open T" "{x \<in> s. f x \<in> t} = s \<inter> T"
  13.130 -    using continuous_open_in_preimage[OF assms(1,3)] unfolding openin_open by auto
  13.131 +    using continuous_openin_preimage[OF assms(1,3)] unfolding openin_open by auto
  13.132    then show ?thesis
  13.133      using open_Int[of s T, OF assms(2)] by auto
  13.134  qed
  13.135 @@ -5560,7 +5584,7 @@
  13.136    shows "closed {x \<in> s. f x \<in> t}"
  13.137  proof-
  13.138    obtain T where "closed T" "{x \<in> s. f x \<in> t} = s \<inter> T"
  13.139 -    using continuous_closed_in_preimage[OF assms(1,3)]
  13.140 +    using continuous_closedin_preimage[OF assms(1,3)]
  13.141      unfolding closedin_closed by auto
  13.142    then show ?thesis using closed_Int[of s T, OF assms(2)] by auto
  13.143  qed
  13.144 @@ -5603,7 +5627,7 @@
  13.145  lemma continuous_closed_in_preimage_constant:
  13.146    fixes f :: "_ \<Rightarrow> 'b::t1_space"
  13.147    shows "continuous_on s f \<Longrightarrow> closedin (subtopology euclidean s) {x \<in> s. f x = a}"
  13.148 -  using continuous_closed_in_preimage[of s f "{a}"] by auto
  13.149 +  using continuous_closedin_preimage[of s f "{a}"] by auto
  13.150  
  13.151  lemma continuous_closed_preimage_constant:
  13.152    fixes f :: "_ \<Rightarrow> 'b::t1_space"
  13.153 @@ -5969,6 +5993,12 @@
  13.154    then show ?thesis
  13.155      unfolding connected_clopen by auto
  13.156  qed
  13.157 +  
  13.158 +lemma connected_linear_image:
  13.159 +  fixes f :: "'a::euclidean_space \<Rightarrow> 'b::real_normed_vector"
  13.160 +  assumes "linear f" and "connected s"
  13.161 +  shows "connected (f ` s)"
  13.162 +using connected_continuous_image assms linear_continuous_on linear_conv_bounded_linear by blast
  13.163  
  13.164  text \<open>Continuity implies uniform continuity on a compact domain.\<close>
  13.165  
  13.166 @@ -5986,7 +6016,7 @@
  13.167    proof safe
  13.168      fix y
  13.169      assume "y \<in> s"
  13.170 -    from continuous_open_in_preimage[OF f open_ball]
  13.171 +    from continuous_openin_preimage[OF f open_ball]
  13.172      obtain T where "open T" and T: "{x \<in> s. f x \<in> ball (f y) (e/2)} = T \<inter> s"
  13.173        unfolding openin_subtopology open_openin by metis
  13.174      then obtain d where "ball y d \<subseteq> T" "0 < d"
    14.1 --- a/src/HOL/Set.thy	Sun Oct 25 17:31:14 2015 +0100
    14.2 +++ b/src/HOL/Set.thy	Mon Oct 26 23:41:27 2015 +0000
    14.3 @@ -1552,6 +1552,9 @@
    14.4  lemma Diff_Int: "A - (B \<inter> C) = (A - B) \<union> (A - C)"
    14.5    by blast
    14.6  
    14.7 +lemma Diff_Diff_Int: "A - (A - B) = A \<inter> B"
    14.8 +  by blast
    14.9 +
   14.10  lemma Un_Diff: "(A \<union> B) - C = (A - C) \<union> (B - C)"
   14.11    by blast
   14.12  
    15.1 --- a/src/HOL/Transcendental.thy	Sun Oct 25 17:31:14 2015 +0100
    15.2 +++ b/src/HOL/Transcendental.thy	Mon Oct 26 23:41:27 2015 +0000
    15.3 @@ -1145,7 +1145,8 @@
    15.4    apply (simp del: of_real_add)
    15.5    done
    15.6  
    15.7 -declare DERIV_exp[THEN DERIV_chain2, derivative_intros]
    15.8 +declare DERIV_exp[THEN DERIV_chain2, derivative_intros] 
    15.9 +        DERIV_exp[THEN DERIV_chain2, unfolded has_field_derivative_def, derivative_intros]
   15.10  
   15.11  lemma norm_exp: "norm (exp x) \<le> exp (norm x)"
   15.12  proof -
   15.13 @@ -1589,6 +1590,8 @@
   15.14    by (rule DERIV_ln[THEN DERIV_cong], simp, simp add: divide_inverse)
   15.15  
   15.16  declare DERIV_ln_divide[THEN DERIV_chain2, derivative_intros]
   15.17 +        DERIV_ln_divide[THEN DERIV_chain2, unfolded has_field_derivative_def, derivative_intros]
   15.18 +
   15.19  
   15.20  lemma ln_series:
   15.21    assumes "0 < x" and "x < 2"
   15.22 @@ -2173,6 +2176,7 @@
   15.23  qed
   15.24  
   15.25  lemmas DERIV_log[THEN DERIV_chain2, derivative_intros]
   15.26 +       DERIV_log[THEN DERIV_chain2, unfolded has_field_derivative_def, derivative_intros]
   15.27  
   15.28  lemma powr_log_cancel [simp]: "0 < a \<Longrightarrow> a \<noteq> 1 \<Longrightarrow> 0 < x \<Longrightarrow> a powr (log a x) = x"
   15.29    by (simp add: powr_def log_def)
   15.30 @@ -2720,6 +2724,7 @@
   15.31    done
   15.32  
   15.33  declare DERIV_sin[THEN DERIV_chain2, derivative_intros]
   15.34 +        DERIV_sin[THEN DERIV_chain2, unfolded has_field_derivative_def, derivative_intros]
   15.35  
   15.36  lemma DERIV_cos [simp]:
   15.37    fixes x :: "'a::{real_normed_field,banach}"
   15.38 @@ -2735,6 +2740,7 @@
   15.39    done
   15.40  
   15.41  declare DERIV_cos[THEN DERIV_chain2, derivative_intros]
   15.42 +        DERIV_cos[THEN DERIV_chain2, unfolded has_field_derivative_def, derivative_intros]
   15.43  
   15.44  lemma isCont_sin:
   15.45    fixes x :: "'a::{real_normed_field,banach}"
   15.46 @@ -4528,8 +4534,11 @@
   15.47  
   15.48  declare
   15.49    DERIV_arcsin[THEN DERIV_chain2, derivative_intros]
   15.50 +  DERIV_arcsin[THEN DERIV_chain2, unfolded has_field_derivative_def, derivative_intros]
   15.51    DERIV_arccos[THEN DERIV_chain2, derivative_intros]
   15.52 +  DERIV_arccos[THEN DERIV_chain2, unfolded has_field_derivative_def, derivative_intros]
   15.53    DERIV_arctan[THEN DERIV_chain2, derivative_intros]
   15.54 +  DERIV_arctan[THEN DERIV_chain2, unfolded has_field_derivative_def, derivative_intros]
   15.55  
   15.56  lemma filterlim_tan_at_right: "filterlim tan at_bot (at_right (- pi/2))"
   15.57    by (rule filterlim_at_bot_at_right[where Q="\<lambda>x. - pi/2 < x \<and> x < pi/2" and P="\<lambda>x. True" and g=arctan])