# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1456329061 0
# Node ID 5ae24f33d3437e696d7bc4140bbc7b7abd643537
# Parent  ff5d7a9831ef826f506076b3f34f66454e8dabc5
Substantial new material for multivariate analysis. Also removal of some duplicates.

diff -r ff5d7a9831ef -r 5ae24f33d343 src/HOL/Deriv.thy
--- a/src/HOL/Deriv.thy	Tue Feb 23 15:49:17 2016 +0000
+++ b/src/HOL/Deriv.thy	Wed Feb 24 15:51:01 2016 +0000
@@ -387,8 +387,7 @@
     done
 next
   fix y::'a assume h: "y \<noteq> x" "dist y x < norm x"
-  then have "y \<noteq> 0"
-    by (auto simp: norm_conv_dist dist_commute)
+  then have "y \<noteq> 0" by auto
   have "norm (?inv y - ?inv x - ?f (y -x)) / norm (y - x) = norm ((?inv y - ?inv x) * (y - x) * ?inv x) / norm (y - x)"
     apply (subst inverse_diff_inverse [OF \<open>y \<noteq> 0\<close> x])
     apply (subst minus_diff_minus)
diff -r ff5d7a9831ef -r 5ae24f33d343 src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy
--- a/src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy	Tue Feb 23 15:49:17 2016 +0000
+++ b/src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy	Wed Feb 24 15:51:01 2016 +0000
@@ -332,6 +332,140 @@
   using setsum_norm_allsubsets_bound[OF assms]
   by simp
 
+subsection\<open>Closures and interiors of halfspaces\<close>
+
+lemma interior_halfspace_le [simp]:
+  assumes "a \<noteq> 0"
+    shows "interior {x. a \<bullet> x \<le> b} = {x. a \<bullet> x < b}"
+proof -
+  have *: "a \<bullet> x < b" if x: "x \<in> S" and S: "S \<subseteq> {x. a \<bullet> x \<le> b}" and "open S" for S x
+  proof -
+    obtain e where "e>0" and e: "cball x e \<subseteq> S"
+      using \<open>open S\<close> open_contains_cball x by blast
+    then have "x + (e / norm a) *\<^sub>R a \<in> cball x e"
+      by (simp add: dist_norm)
+    then have "x + (e / norm a) *\<^sub>R a \<in> S"
+      using e by blast
+    then have "x + (e / norm a) *\<^sub>R a \<in> {x. a \<bullet> x \<le> b}"
+      using S by blast
+    moreover have "e * (a \<bullet> a) / norm a > 0"
+      by (simp add: \<open>0 < e\<close> assms)
+    ultimately show ?thesis
+      by (simp add: algebra_simps)
+  qed
+  show ?thesis
+    by (rule interior_unique) (auto simp: open_halfspace_lt *)
+qed
+
+lemma interior_halfspace_ge [simp]:
+   "a \<noteq> 0 \<Longrightarrow> interior {x. a \<bullet> x \<ge> b} = {x. a \<bullet> x > b}"
+using interior_halfspace_le [of "-a" "-b"] by simp
+
+lemma interior_halfspace_component_le [simp]:
+     "interior {x. x$k \<le> a} = {x :: (real,'n::finite) vec. x$k < a}" (is "?LE")
+  and interior_halfspace_component_ge [simp]:
+     "interior {x. x$k \<ge> a} = {x :: (real,'n::finite) vec. x$k > a}" (is "?GE")
+proof -
+  have "axis k (1::real) \<noteq> 0"
+    by (simp add: axis_def vec_eq_iff)
+  moreover have "axis k (1::real) \<bullet> x = x$k" for x
+    by (simp add: cart_eq_inner_axis inner_commute)
+  ultimately show ?LE ?GE
+    using interior_halfspace_le [of "axis k (1::real)" a]
+          interior_halfspace_ge [of "axis k (1::real)" a] by auto
+qed
+
+lemma closure_halfspace_lt [simp]:
+  assumes "a \<noteq> 0"
+    shows "closure {x. a \<bullet> x < b} = {x. a \<bullet> x \<le> b}"
+proof -
+  have [simp]: "-{x. a \<bullet> x < b} = {x. a \<bullet> x \<ge> b}"
+    by (force simp:)
+  then show ?thesis
+    using interior_halfspace_ge [of a b] assms
+    by (force simp: closure_interior)
+qed
+
+lemma closure_halfspace_gt [simp]:
+   "a \<noteq> 0 \<Longrightarrow> closure {x. a \<bullet> x > b} = {x. a \<bullet> x \<ge> b}"
+using closure_halfspace_lt [of "-a" "-b"] by simp
+
+lemma closure_halfspace_component_lt [simp]:
+     "closure {x. x$k < a} = {x :: (real,'n::finite) vec. x$k \<le> a}" (is "?LE")
+  and closure_halfspace_component_gt [simp]:
+     "closure {x. x$k > a} = {x :: (real,'n::finite) vec. x$k \<ge> a}" (is "?GE")
+proof -
+  have "axis k (1::real) \<noteq> 0"
+    by (simp add: axis_def vec_eq_iff)
+  moreover have "axis k (1::real) \<bullet> x = x$k" for x
+    by (simp add: cart_eq_inner_axis inner_commute)
+  ultimately show ?LE ?GE
+    using closure_halfspace_lt [of "axis k (1::real)" a]
+          closure_halfspace_gt [of "axis k (1::real)" a] by auto
+qed
+
+lemma interior_hyperplane [simp]:
+  assumes "a \<noteq> 0"
+    shows "interior {x. a \<bullet> x = b} = {}"
+proof -
+  have [simp]: "{x. a \<bullet> x = b} = {x. a \<bullet> x \<le> b} \<inter> {x. a \<bullet> x \<ge> b}"
+    by (force simp:)
+  then show ?thesis
+    by (auto simp: assms)
+qed
+
+lemma frontier_halfspace_le:
+  assumes "a \<noteq> 0 \<or> b \<noteq> 0"
+    shows "frontier {x. a \<bullet> x \<le> b} = {x. a \<bullet> x = b}"
+proof (cases "a = 0")
+  case True with assms show ?thesis by simp
+next
+  case False then show ?thesis
+    by (force simp: frontier_def closed_halfspace_le)
+qed
+
+lemma frontier_halfspace_ge:
+  assumes "a \<noteq> 0 \<or> b \<noteq> 0"
+    shows "frontier {x. a \<bullet> x \<ge> b} = {x. a \<bullet> x = b}"
+proof (cases "a = 0")
+  case True with assms show ?thesis by simp
+next
+  case False then show ?thesis
+    by (force simp: frontier_def closed_halfspace_ge)
+qed
+
+lemma frontier_halfspace_lt:
+  assumes "a \<noteq> 0 \<or> b \<noteq> 0"
+    shows "frontier {x. a \<bullet> x < b} = {x. a \<bullet> x = b}"
+proof (cases "a = 0")
+  case True with assms show ?thesis by simp
+next
+  case False then show ?thesis
+    by (force simp: frontier_def interior_open open_halfspace_lt)
+qed
+
+lemma frontier_halfspace_gt:
+  assumes "a \<noteq> 0 \<or> b \<noteq> 0"
+    shows "frontier {x. a \<bullet> x > b} = {x. a \<bullet> x = b}"
+proof (cases "a = 0")
+  case True with assms show ?thesis by simp
+next
+  case False then show ?thesis
+    by (force simp: frontier_def interior_open open_halfspace_gt)
+qed
+
+lemma interior_standard_hyperplane:
+   "interior {x :: (real,'n::finite) vec. x$k = a} = {}"
+proof -
+  have "axis k (1::real) \<noteq> 0"
+    by (simp add: axis_def vec_eq_iff)
+  moreover have "axis k (1::real) \<bullet> x = x$k" for x
+    by (simp add: cart_eq_inner_axis inner_commute)
+  ultimately show ?thesis
+    using interior_hyperplane [of "axis k (1::real)" a]
+    by force
+qed
+
 subsection \<open>Matrix operations\<close>
 
 text\<open>Matrix notation. NB: an MxN matrix is of type @{typ "'a^'n^'m"}, not @{typ "'a^'m^'n"}\<close>
diff -r ff5d7a9831ef -r 5ae24f33d343 src/HOL/Multivariate_Analysis/Cauchy_Integral_Thm.thy
--- a/src/HOL/Multivariate_Analysis/Cauchy_Integral_Thm.thy	Tue Feb 23 15:49:17 2016 +0000
+++ b/src/HOL/Multivariate_Analysis/Cauchy_Integral_Thm.thy	Wed Feb 24 15:51:01 2016 +0000
@@ -573,7 +573,7 @@
   by (auto simp: contour_integral_def has_contour_integral_def integral_def [symmetric])
 
 corollary has_contour_integral_eqpath:
-     "\<lbrakk>(f has_contour_integral y) p; f contour_integrable_on \<gamma>; 
+     "\<lbrakk>(f has_contour_integral y) p; f contour_integrable_on \<gamma>;
        contour_integral p f = contour_integral \<gamma> f\<rbrakk>
       \<Longrightarrow> (f has_contour_integral y) \<gamma>"
 using contour_integrable_on_def contour_integral_unique by auto
@@ -1730,6 +1730,14 @@
   apply (simp add: valid_path_join)
   done
 
+lemma has_chain_integral_chain_integral4:
+     "(f has_contour_integral i) (linepath a b +++ linepath b c +++ linepath c d +++ linepath d e)
+      \<Longrightarrow> contour_integral (linepath a b) f + contour_integral (linepath b c) f + contour_integral (linepath c d) f + contour_integral (linepath d e) f = i"
+  apply (subst contour_integral_unique [symmetric], assumption)
+  apply (drule has_contour_integral_integrable)
+  apply (simp add: valid_path_join)
+  done
+
 subsection\<open>Reversing the order in a double path integral\<close>
 
 text\<open>The condition is stronger than needed but it's often true in typical situations\<close>
@@ -6489,7 +6497,7 @@
        if "z \<in> s" for z
   proof -
     obtain d h N where "0 < d" "summable h" and le_h: "\<And>n y. \<lbrakk>N \<le> n; y \<in> ball z d\<rbrakk> \<Longrightarrow> norm(f n y) \<le> h n"
-      using to_g \<open>z \<in> s\<close> by meson 
+      using to_g \<open>z \<in> s\<close> by meson
     then obtain r where "r>0" and r: "ball z r \<subseteq> ball z d \<inter> s" using \<open>z \<in> s\<close> s
       by (metis Int_iff open_ball centre_in_ball open_Int open_contains_ball_eq)
     have 1: "open (ball z d \<inter> s)"
@@ -6588,7 +6596,7 @@
   using power_series_and_derivative_0 [OF assms]
   apply clarify
   apply (rule_tac g="(\<lambda>z. g(z - w))" in that)
-  using DERIV_shift [where z="-w"] 
+  using DERIV_shift [where z="-w"]
   apply (auto simp: norm_minus_commute Ball_def dist_norm)
   done
 
@@ -6917,7 +6925,7 @@
                          dist ((\<lambda>(x,y). F x y) x') ((\<lambda>(x,y). F x y) x) < \<epsilon>/norm(b - a)"
       apply (rule uniformly_continuous_onE [where e = "\<epsilon>/norm(b - a)"])
       using \<open>0 < \<epsilon>\<close> \<open>a \<noteq> b\<close> by auto
-    have \<eta>: "\<lbrakk>norm (w - x1) \<le> \<delta>;   x2 \<in> closed_segment a b; 
+    have \<eta>: "\<lbrakk>norm (w - x1) \<le> \<delta>;   x2 \<in> closed_segment a b;
               norm (w - x1') \<le> \<delta>;  x2' \<in> closed_segment a b; norm ((x1', x2') - (x1, x2)) < \<eta>\<rbrakk>
               \<Longrightarrow> norm (F x1' x2' - F x1 x2) \<le> \<epsilon> / cmod (b - a)"
              for x1 x2 x1' x2'
@@ -6940,12 +6948,12 @@
       apply (auto simp: dist_norm contour_integral_diff [OF cont_dw cont_dw, symmetric] \<open>w \<in> u\<close> intro: le_ee)
       done
   qed
-  show ?thesis 
+  show ?thesis
     apply (rule continuous_onI)
     apply (cases "a=b")
     apply (auto intro: *)
     done
-qed  
+qed
 
 text\<open>This version has @{term"polynomial_function \<gamma>"} as an additional assumption.\<close>
 lemma Cauchy_integral_formula_global_weak:
@@ -7189,7 +7197,7 @@
       by (simp add: V)
     have cond_uu: "continuous_on (u \<times> u) (\<lambda>(x,y). d x y)"
       apply (simp add: continuous_on_eq_continuous_within d_def continuous_within tendsto_f')
-      apply (simp add: Lim_within_open_NO_MATCH open_Times u, clarify)
+      apply (simp add: tendsto_within_open_NO_MATCH open_Times u, clarify)
       apply (rule Lim_transform_within_open [OF _ open_uu_Id, where f = "(\<lambda>(x,y). (f y - f x) / (y - x))"])
       using con_ff
       apply (auto simp: continuous_within)
diff -r ff5d7a9831ef -r 5ae24f33d343 src/HOL/Multivariate_Analysis/Complex_Analysis_Basics.thy
--- a/src/HOL/Multivariate_Analysis/Complex_Analysis_Basics.thy	Tue Feb 23 15:49:17 2016 +0000
+++ b/src/HOL/Multivariate_Analysis/Complex_Analysis_Basics.thy	Wed Feb 24 15:51:01 2016 +0000
@@ -508,44 +508,47 @@
     \<Longrightarrow> deriv (g o f) x = deriv g (f x) * deriv f x"
   by (metis DERIV_deriv_iff_complex_differentiable DERIV_chain DERIV_imp_deriv)
 
-lemma deriv_linear: "deriv (\<lambda>w. c * w) = (\<lambda>z. c)"
+lemma deriv_linear [simp]: "deriv (\<lambda>w. c * w) = (\<lambda>z. c)"
   by (metis DERIV_imp_deriv DERIV_cmult_Id)
 
-lemma deriv_ident: "deriv (\<lambda>w. w) = (\<lambda>z. 1)"
+lemma deriv_ident [simp]: "deriv (\<lambda>w. w) = (\<lambda>z. 1)"
   by (metis DERIV_imp_deriv DERIV_ident)
 
-lemma deriv_const: "deriv (\<lambda>w. c) = (\<lambda>z. 0)"
+lemma deriv_id [simp]: "deriv id = (\<lambda>z. 1)"
+  by (simp add: id_def)
+
+lemma deriv_const [simp]: "deriv (\<lambda>w. c) = (\<lambda>z. 0)"
   by (metis DERIV_imp_deriv DERIV_const)
 
-lemma complex_derivative_add:
+lemma complex_derivative_add [simp]:
   "\<lbrakk>f complex_differentiable at z; g complex_differentiable at z\<rbrakk>
    \<Longrightarrow> deriv (\<lambda>w. f w + g w) z = deriv f z + deriv g z"
   unfolding DERIV_deriv_iff_complex_differentiable[symmetric]
   by (auto intro!: DERIV_imp_deriv derivative_intros)
 
-lemma complex_derivative_diff:
+lemma complex_derivative_diff [simp]:
   "\<lbrakk>f complex_differentiable at z; g complex_differentiable at z\<rbrakk>
    \<Longrightarrow> deriv (\<lambda>w. f w - g w) z = deriv f z - deriv g z"
   unfolding DERIV_deriv_iff_complex_differentiable[symmetric]
   by (auto intro!: DERIV_imp_deriv derivative_intros)
 
-lemma complex_derivative_mult:
+lemma complex_derivative_mult [simp]:
   "\<lbrakk>f complex_differentiable at z; g complex_differentiable at z\<rbrakk>
    \<Longrightarrow> deriv (\<lambda>w. f w * g w) z = f z * deriv g z + deriv f z * g z"
   unfolding DERIV_deriv_iff_complex_differentiable[symmetric]
   by (auto intro!: DERIV_imp_deriv derivative_eq_intros)
 
-lemma complex_derivative_cmult:
+lemma complex_derivative_cmult [simp]:
   "f complex_differentiable at z \<Longrightarrow> deriv (\<lambda>w. c * f w) z = c * deriv f z"
   unfolding DERIV_deriv_iff_complex_differentiable[symmetric]
   by (auto intro!: DERIV_imp_deriv derivative_eq_intros)
 
-lemma complex_derivative_cmult_right:
+lemma complex_derivative_cmult_right [simp]:
   "f complex_differentiable at z \<Longrightarrow> deriv (\<lambda>w. f w * c) z = deriv f z * c"
   unfolding DERIV_deriv_iff_complex_differentiable[symmetric]
   by (auto intro!: DERIV_imp_deriv derivative_eq_intros)
 
-lemma complex_derivative_cdivide_right:
+lemma complex_derivative_cdivide_right [simp]:
   "f complex_differentiable at z \<Longrightarrow> deriv (\<lambda>w. f w / c) z = deriv f z / c"
   unfolding Fields.field_class.field_divide_inverse
   by (blast intro: complex_derivative_cmult_right)
diff -r ff5d7a9831ef -r 5ae24f33d343 src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy
--- a/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy	Tue Feb 23 15:49:17 2016 +0000
+++ b/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy	Wed Feb 24 15:51:01 2016 +0000
@@ -107,13 +107,14 @@
     fix x :: "'n::euclidean_space"
     def y \<equiv> "(e / norm x) *\<^sub>R x"
     then have "y \<in> cball 0 e"
-      using cball_def dist_norm[of 0 y] assms by auto
+      using assms by auto
     moreover have *: "x = (norm x / e) *\<^sub>R y"
       using y_def assms by simp
     moreover from * have "x = (norm x/e) *\<^sub>R y"
       by auto
     ultimately have "x \<in> span (cball 0 e)"
-      using span_mul[of y "cball 0 e" "norm x/e"] span_inc[of "cball 0 e"] by auto
+      using span_mul[of y "cball 0 e" "norm x/e"] span_inc[of "cball 0 e"]
+      by (simp add: span_superset)
   }
   then have "span (cball 0 e) = (UNIV :: 'n::euclidean_space set)"
     by auto
@@ -5183,9 +5184,7 @@
     done
   ultimately obtain u y where obt: "u\<ge>0" "u \<le> b / norm x" "y = u *\<^sub>R x"
     "y \<in> ?A" "y \<in> s" "\<forall>z\<in>?A \<inter> s. dist 0 z \<le> dist 0 y"
-    using distance_attains_sup[OF compact_inter[OF _ assms(1), of ?A], of 0]
-    by auto
-
+    using distance_attains_sup[OF compact_inter[OF _ assms(1), of ?A], of 0] by blast
   have "norm x > 0"
     using assms(3)[unfolded zero_less_norm_iff[symmetric]] by auto
   {
diff -r ff5d7a9831ef -r 5ae24f33d343 src/HOL/Multivariate_Analysis/Fashoda.thy
--- a/src/HOL/Multivariate_Analysis/Fashoda.thy	Tue Feb 23 15:49:17 2016 +0000
+++ b/src/HOL/Multivariate_Analysis/Fashoda.thy	Wed Feb 24 15:51:01 2016 +0000
@@ -8,14 +8,6 @@
 imports Brouwer_Fixpoint Path_Connected Cartesian_Euclidean_Space
 begin
 
-(* move *)
-
-lemma cart_eq_inner_axis: "a $ i = a \<bullet> axis i 1"
-  by (simp add: inner_axis)
-
-lemma axis_in_Basis: "a \<in> Basis \<Longrightarrow> axis i a \<in> Basis"
-  by (auto simp add: Basis_vec_def axis_eq_axis)
-
 subsection \<open>Bijections between intervals.\<close>
 
 definition interval_bij :: "'a \<times> 'a \<Rightarrow> 'a \<times> 'a \<Rightarrow> 'a \<Rightarrow> 'a::euclidean_space"
diff -r ff5d7a9831ef -r 5ae24f33d343 src/HOL/Multivariate_Analysis/Finite_Cartesian_Product.thy
--- a/src/HOL/Multivariate_Analysis/Finite_Cartesian_Product.thy	Tue Feb 23 15:49:17 2016 +0000
+++ b/src/HOL/Multivariate_Analysis/Finite_Cartesian_Product.thy	Wed Feb 24 15:51:01 2016 +0000
@@ -549,4 +549,10 @@
 
 end
 
+lemma cart_eq_inner_axis: "a $ i = inner a (axis i 1)"
+  by (simp add: inner_axis)
+
+lemma axis_in_Basis: "a \<in> Basis \<Longrightarrow> axis i a \<in> Basis"
+  by (auto simp add: Basis_vec_def axis_eq_axis)
+
 end
diff -r ff5d7a9831ef -r 5ae24f33d343 src/HOL/Multivariate_Analysis/Gamma.thy
--- a/src/HOL/Multivariate_Analysis/Gamma.thy	Tue Feb 23 15:49:17 2016 +0000
+++ b/src/HOL/Multivariate_Analysis/Gamma.thy	Wed Feb 24 15:51:01 2016 +0000
@@ -1738,7 +1738,7 @@
 
     moreover from z double_in_nonpos_Ints_imp[of z] have "2 * z \<notin> \<int>\<^sub>\<le>\<^sub>0" by auto
     hence "?g \<longlonglongrightarrow> ?powr 2 (2*z) * Gamma z * Gamma (z+1/2) / Gamma (2*z)"
-      using lim_subseq[of "op * 2", OF _ Gamma_series'_LIMSEQ, of "2*z"]
+      using LIMSEQ_subseq_LIMSEQ[OF Gamma_series'_LIMSEQ, of "op*2" "2*z"]
       by (intro tendsto_intros Gamma_series'_LIMSEQ)
          (simp_all add: o_def subseq_def Gamma_eq_zero_iff)
     ultimately have "?h \<longlonglongrightarrow> ?powr 2 (2*z) * Gamma z * Gamma (z+1/2) / Gamma (2*z)"
diff -r ff5d7a9831ef -r 5ae24f33d343 src/HOL/Multivariate_Analysis/Linear_Algebra.thy
--- a/src/HOL/Multivariate_Analysis/Linear_Algebra.thy	Tue Feb 23 15:49:17 2016 +0000
+++ b/src/HOL/Multivariate_Analysis/Linear_Algebra.thy	Wed Feb 24 15:51:01 2016 +0000
@@ -683,23 +683,6 @@
   apply (metis Suc_pred of_nat_Suc)
   done
 
-lemma real_archimedian_rdiv_eq_0:
-  assumes x0: "x \<ge> 0"
-    and c: "c \<ge> 0"
-    and xc: "\<forall>(m::nat) > 0. real m * x \<le> c"
-  shows "x = 0"
-proof (rule ccontr)
-  assume "x \<noteq> 0"
-  with x0 have xp: "x > 0" by arith
-  from reals_Archimedean3[OF xp, rule_format, of c]
-  obtain n :: nat where n: "c < real n * x"
-    by blast
-  with xc[rule_format, of n] have "n = 0"
-    by arith
-  with n c show False
-    by simp
-qed
-
 
 subsection\<open>A bit of linear algebra.\<close>
 
diff -r ff5d7a9831ef -r 5ae24f33d343 src/HOL/Multivariate_Analysis/Path_Connected.thy
--- a/src/HOL/Multivariate_Analysis/Path_Connected.thy	Tue Feb 23 15:49:17 2016 +0000
+++ b/src/HOL/Multivariate_Analysis/Path_Connected.thy	Wed Feb 24 15:51:01 2016 +0000
@@ -444,7 +444,7 @@
     done
   show ?thesis
     apply (subst *)
-    apply (rule continuous_on_union)
+    apply (rule continuous_on_closed_Un)
     using 1 2
     apply auto
     done
@@ -757,9 +757,9 @@
   { assume "u \<noteq> 0"
     then have "u > 0" using \<open>0 \<le> u\<close> by auto
     { fix e::real assume "e > 0"
-      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"
-        using continuous_onD [OF gcon _ \<open>e > 0\<close>] \<open>0 \<le> _\<close> \<open>_ \<le> 1\<close> atLeastAtMost_iff by auto
-      have *: "dist (max 0 (u - d / 2)) u < d"
+      obtain d where "d>0" and d: "\<And>x'. \<lbrakk>x' \<in> {0..1}; dist x' u \<le> d\<rbrakk> \<Longrightarrow> dist (g x') (g u) < e"
+        using continuous_onE [OF gcon _ \<open>e > 0\<close>] \<open>0 \<le> _\<close> \<open>_ \<le> 1\<close> atLeastAtMost_iff by auto
+      have *: "dist (max 0 (u - d / 2)) u \<le> d"
         using \<open>0 \<le> u\<close> \<open>u \<le> 1\<close> \<open>d > 0\<close> by (simp add: dist_real_def)
       have "\<exists>y\<in>S. dist y (g u) < e"
         using \<open>0 < u\<close> \<open>u \<le> 1\<close> \<open>d > 0\<close>
@@ -891,7 +891,7 @@
     by auto
   show ?thesis
     unfolding path_def shiftpath_def *
-    apply (rule continuous_on_union)
+    apply (rule continuous_on_closed_Un)
     apply (rule closed_real_atLeastAtMost)+
     apply (rule continuous_on_eq[of _ "g \<circ> (\<lambda>x. a + x)"])
     prefer 3
diff -r ff5d7a9831ef -r 5ae24f33d343 src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy
--- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Tue Feb 23 15:49:17 2016 +0000
+++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Wed Feb 24 15:51:01 2016 +0000
@@ -29,36 +29,10 @@
   apply fastforce
   done
 
-lemma dist_0_norm:
-  fixes x :: "'a::real_normed_vector"
-  shows "dist 0 x = norm x"
-unfolding dist_norm by simp
-
-lemma dist_double: "dist x y < d / 2 \<Longrightarrow> dist x z < d / 2 \<Longrightarrow> dist y z < d"
-  using dist_triangle[of y z x] by (simp add: dist_commute)
-
-(* LEGACY *)
-lemma lim_subseq: "subseq r \<Longrightarrow> s \<longlonglongrightarrow> l \<Longrightarrow> (s \<circ> r) \<longlonglongrightarrow> l"
-  by (rule LIMSEQ_subseq_LIMSEQ)
-
 lemma countable_PiE:
   "finite I \<Longrightarrow> (\<And>i. i \<in> I \<Longrightarrow> countable (F i)) \<Longrightarrow> countable (PiE I F)"
   by (induct I arbitrary: F rule: finite_induct) (auto simp: PiE_insert_eq)
 
-lemma Lim_within_open:
-  fixes f :: "'a::topological_space \<Rightarrow> 'b::topological_space"
-  shows "a \<in> S \<Longrightarrow> open S \<Longrightarrow> (f \<longlongrightarrow> l)(at a within S) \<longleftrightarrow> (f \<longlongrightarrow> l)(at a)"
-  by (fact tendsto_within_open)
-
-lemma Lim_within_open_NO_MATCH:
-  fixes f :: "'a::topological_space \<Rightarrow> 'b::topological_space"
-  shows "a \<in> S \<Longrightarrow> NO_MATCH UNIV S \<Longrightarrow> open S \<Longrightarrow> (f \<longlongrightarrow> l)(at a within S) \<longleftrightarrow> (f \<longlongrightarrow> l)(at a)"
-using tendsto_within_open by blast
-
-lemma continuous_on_union:
-  "closed s \<Longrightarrow> closed t \<Longrightarrow> continuous_on s f \<Longrightarrow> continuous_on t f \<Longrightarrow> continuous_on (s \<union> t) f"
-  by (fact continuous_on_closed_Un)
-
 lemma continuous_on_cases:
   "closed s \<Longrightarrow> closed t \<Longrightarrow> continuous_on s f \<Longrightarrow> continuous_on t g \<Longrightarrow>
     \<forall>x. (x\<in>s \<and> \<not> P x) \<or> (x \<in> t \<and> P x) \<longrightarrow> f x = g x \<Longrightarrow>
@@ -4405,7 +4379,7 @@
       fix y
       assume "y \<in> ball k r"
       with \<open>r < e / 2\<close> \<open>x \<in> ball k r\<close> have "dist x y < e"
-        by (intro dist_double[where x = k and d=e]) (auto simp: dist_commute)
+        by (intro dist_triangle_half_r [of k _ e]) (auto simp: dist_commute)
       with \<open>ball x e \<subseteq> T\<close> show "y \<in> T"
         by auto
     next
@@ -5374,10 +5348,14 @@
 
 text\<open>Some simple consequential lemmas.\<close>
 
-lemma continuous_onD:
+lemma continuous_onE:
     assumes "continuous_on s f" "x\<in>s" "e>0"
-    obtains d where "d>0"  "\<And>x'. \<lbrakk>x' \<in> s; dist x' x < d\<rbrakk> \<Longrightarrow> dist (f x') (f x) < e"
-  using assms [unfolded continuous_on_iff] by blast
+    obtains d where "d>0"  "\<And>x'. \<lbrakk>x' \<in> s; dist x' x \<le> d\<rbrakk> \<Longrightarrow> dist (f x') (f x) < e"
+  using assms
+  apply (simp add: continuous_on_iff)
+  apply (elim ballE allE)
+  apply (auto intro: that [where d="d/2" for d])
+  done
 
 lemma uniformly_continuous_onE:
   assumes "uniformly_continuous_on s f" "0 < e"
@@ -6291,9 +6269,9 @@
       by blast
     moreover assume "dist x x' < Min (snd`D) / 2"
     ultimately have "dist y x' < d"
-      by (intro dist_double[where x=x and d=d]) (auto simp: dist_commute)
+      by (intro dist_triangle_half_r[of x _ d]) (auto simp: dist_commute)
     with D x in_s show  "dist (f x) (f x') < e"
-      by (intro dist_double[where x="f y" and d=e]) (auto simp: dist_commute subset_eq)
+      by (intro dist_triangle_half_r[of "f y" _ e]) (auto simp: dist_commute subset_eq)
   qed (insert D, auto)
 qed auto
 
diff -r ff5d7a9831ef -r 5ae24f33d343 src/HOL/Probability/Helly_Selection.thy
--- a/src/HOL/Probability/Helly_Selection.thy	Tue Feb 23 15:49:17 2016 +0000
+++ b/src/HOL/Probability/Helly_Selection.thy	Wed Feb 24 15:51:01 2016 +0000
@@ -263,7 +263,7 @@
   qed
   ultimately have M: "real_distribution (interval_measure F)" "cdf (interval_measure F) = F"
     using F by (auto intro!: real_distribution_interval_measure cdf_interval_measure simp: mono_def)
-  with lim_F lim_subseq M have "weak_conv_m (\<mu> \<circ> s \<circ> r) (interval_measure F)"
+  with lim_F LIMSEQ_subseq_LIMSEQ M have "weak_conv_m (\<mu> \<circ> s \<circ> r) (interval_measure F)"
     by (auto simp: weak_conv_def weak_conv_m_def f_def comp_def)
   then show "\<exists>r M. subseq r \<and> (real_distribution M \<and> weak_conv_m (\<mu> \<circ> s \<circ> r) M)"
     using F M by auto
diff -r ff5d7a9831ef -r 5ae24f33d343 src/HOL/Probability/Levy.thy
--- a/src/HOL/Probability/Levy.thy	Tue Feb 23 15:49:17 2016 +0000
+++ b/src/HOL/Probability/Levy.thy	Wed Feb 24 15:51:01 2016 +0000
@@ -527,12 +527,11 @@
     have 3: "\<And>t. (\<lambda>n. char ((M \<circ> s) n) t) \<longlonglongrightarrow> char \<nu> t" by (intro levy_continuity1 [OF 2 * nu])
     have 4: "\<And>t. (\<lambda>n. char ((M \<circ> s) n) t) = ((\<lambda>n. char (M n) t) \<circ> s)" by (rule ext, simp)
     have 5: "\<And>t. (\<lambda>n. char ((M \<circ> s) n) t) \<longlonglongrightarrow> char M' t"
-      by (subst 4, rule lim_subseq [OF s], rule assms)
+      by (subst 4, rule LIMSEQ_subseq_LIMSEQ [OF _ s], rule assms)
     hence "char \<nu> = char M'" by (intro ext, intro LIMSEQ_unique [OF 3 5])
     hence "\<nu> = M'" by (rule Levy_uniqueness [OF * `real_distribution M'`])
     thus "weak_conv_m (M \<circ> s) M'" 
-      apply (elim subst)
-      by (rule nu)  
+      by (elim subst) (rule nu)  
   qed
 qed
 
diff -r ff5d7a9831ef -r 5ae24f33d343 src/HOL/Probability/Projective_Limit.thy
--- a/src/HOL/Probability/Projective_Limit.thy	Tue Feb 23 15:49:17 2016 +0000
+++ b/src/HOL/Probability/Projective_Limit.thy	Wed Feb 24 15:51:01 2016 +0000
@@ -413,7 +413,7 @@
     have "(\<lambda>i. fm n (y (Suc (diagseq i)))) \<longlonglongrightarrow> finmap_of (Utn ` J n) z"
       by (rule tendsto_finmap)
     hence "((\<lambda>i. fm n (y (Suc (diagseq i)))) o (\<lambda>i. i + n)) \<longlonglongrightarrow> finmap_of (Utn ` J n) z"
-      by (intro lim_subseq) (simp add: subseq_def)
+      by (rule LIMSEQ_subseq_LIMSEQ) (simp add: subseq_def)
     moreover
     have "(\<forall>i. ((\<lambda>i. fm n (y (Suc (diagseq i)))) o (\<lambda>i. i + n)) i \<in> K' n)"
       apply (auto simp add: o_def intro!: fm_in_K' \<open>1 \<le> n\<close> le_SucI)
diff -r ff5d7a9831ef -r 5ae24f33d343 src/HOL/Real.thy
--- a/src/HOL/Real.thy	Tue Feb 23 15:49:17 2016 +0000
+++ b/src/HOL/Real.thy	Wed Feb 24 15:51:01 2016 +0000
@@ -1143,6 +1143,13 @@
   shows "\<forall>y. \<exists>n. y < real n * x"
   using \<open>0 < x\<close> by (auto intro: ex_less_of_nat_mult)
 
+lemma real_archimedian_rdiv_eq_0:
+  assumes x0: "x \<ge> 0"
+      and c: "c \<ge> 0"
+      and xc: "\<And>m::nat. m > 0 \<Longrightarrow> real m * x \<le> c"
+    shows "x = 0"
+by (metis reals_Archimedean3 dual_order.order_iff_strict le0 le_less_trans not_le x0 xc)
+
 
 subsection\<open>Rationals\<close>
 
diff -r ff5d7a9831ef -r 5ae24f33d343 src/HOL/Real_Vector_Spaces.thy
--- a/src/HOL/Real_Vector_Spaces.thy	Tue Feb 23 15:49:17 2016 +0000
+++ b/src/HOL/Real_Vector_Spaces.thy	Wed Feb 24 15:51:01 2016 +0000
@@ -1308,6 +1308,11 @@
 
 declare norm_conv_dist [symmetric, simp]
 
+lemma dist_0_norm [simp]:
+  fixes x :: "'a::real_normed_vector"
+  shows "dist 0 x = norm x"
+unfolding dist_norm by simp
+
 lemma dist_diff [simp]: "dist a (a - b) = norm b"  "dist (a - b) a = norm b"
   by (simp_all add: dist_norm)
 
diff -r ff5d7a9831ef -r 5ae24f33d343 src/HOL/Topological_Spaces.thy
--- a/src/HOL/Topological_Spaces.thy	Tue Feb 23 15:49:17 2016 +0000
+++ b/src/HOL/Topological_Spaces.thy	Wed Feb 24 15:51:01 2016 +0000
@@ -1296,6 +1296,11 @@
 lemma tendsto_within_open: "a \<in> S \<Longrightarrow> open S \<Longrightarrow> (f \<longlongrightarrow> l) (at a within S) \<longleftrightarrow> (f \<midarrow>a\<rightarrow> l)"
   unfolding tendsto_def by (simp add: at_within_open[where S=S])
 
+lemma tendsto_within_open_NO_MATCH:
+  fixes f :: "'a::topological_space \<Rightarrow> 'b::topological_space"
+  shows "a \<in> S \<Longrightarrow> NO_MATCH UNIV S \<Longrightarrow> open S \<Longrightarrow> (f \<longlongrightarrow> l)(at a within S) \<longleftrightarrow> (f \<longlongrightarrow> l)(at a)"
+using tendsto_within_open by blast
+
 lemma LIM_const_not_eq[tendsto_intros]:
   fixes a :: "'a::perfect_space"
   fixes k L :: "'b::t2_space"
@@ -2012,6 +2017,9 @@
 apply (fastforce simp add: open_closed [symmetric])
 done
 
+lemma connected_closedD:
+    "\<lbrakk>connected s; A \<inter> B \<inter> s = {}; s \<subseteq> A \<union> B; closed A; closed B\<rbrakk> \<Longrightarrow> A \<inter> s = {} \<or> B \<inter> s = {}"
+by (simp add: connected_closed)
 
 lemma connected_Union:
   assumes cs: "\<And>s. s \<in> S \<Longrightarrow> connected s" and ne: "\<Inter>S \<noteq> {}"