merged
authorwenzelm
Fri, 23 Feb 2018 15:17:51 +0100
changeset 67705 f7e37a94caee
parent 67693 4fa9d5ef95bc (diff)
parent 67704 23d46836a5ac (current diff)
child 67708 f7a686614fe5
child 67709 3c9e0b4709e7
merged
--- a/src/HOL/Analysis/Binary_Product_Measure.thy	Fri Feb 23 15:07:30 2018 +0100
+++ b/src/HOL/Analysis/Binary_Product_Measure.thy	Fri Feb 23 15:17:51 2018 +0100
@@ -759,18 +759,20 @@
   with A B have fin_Pair: "\<And>x. finite (Pair x -` X)"
     by (intro finite_subset[OF _ B]) auto
   have fin_X: "finite X" using X_subset by (rule finite_subset) (auto simp: A B)
-  have pos_card: "(0::ennreal) < of_nat (card (Pair x -` X)) \<longleftrightarrow> Pair x -` X \<noteq> {}" for x
-    by (auto simp: card_eq_0_iff fin_Pair) blast
-
-  show "emeasure ?P X = emeasure ?C X"
-    using X_subset A fin_Pair fin_X
-    apply (subst B.emeasure_pair_measure_alt[OF X])
+  have card: "0 < card (Pair a -` X)" if "(a, b) \<in> X" for a b
+    using card_gt_0_iff fin_Pair that by auto
+  then have "emeasure ?P X = \<integral>\<^sup>+ x. emeasure (count_space B) (Pair x -` X)
+            \<partial>count_space A"
+    by (simp add: B.emeasure_pair_measure_alt X)
+  also have "... = emeasure ?C X"
     apply (subst emeasure_count_space)
-    apply (auto simp add: emeasure_count_space nn_integral_count_space
-                          pos_card of_nat_sum[symmetric] card_SigmaI[symmetric]
-                simp del: of_nat_sum card_SigmaI
+    using card X_subset A fin_Pair fin_X
+    apply (auto simp add: nn_integral_count_space
+                           of_nat_sum[symmetric] card_SigmaI[symmetric]
+                simp del:  card_SigmaI
                 intro!: arg_cong[where f=card])
     done
+  finally show "emeasure ?P X = emeasure ?C X" .
 qed
 
 
--- a/src/HOL/Analysis/Borel_Space.thy	Fri Feb 23 15:07:30 2018 +0100
+++ b/src/HOL/Analysis/Borel_Space.thy	Fri Feb 23 15:17:51 2018 +0100
@@ -242,6 +242,11 @@
   shows "S \<noteq> {} \<Longrightarrow> bdd_above S \<Longrightarrow> closed S \<Longrightarrow> Sup S \<in> S"
   by (subst closure_closed[symmetric], assumption, rule closure_contains_Sup)
 
+lemma closed_subset_contains_Sup:
+  fixes A C :: "real set"
+  shows "closed C \<Longrightarrow> A \<subseteq> C \<Longrightarrow> A \<noteq> {} \<Longrightarrow> bdd_above A \<Longrightarrow> Sup A \<in> C"
+  by (metis closure_contains_Sup closure_minimal subset_eq)
+
 lemma deriv_nonneg_imp_mono:
   assumes deriv: "\<And>x. x \<in> {a..b} \<Longrightarrow> (g has_real_derivative g' x) (at x)"
   assumes nonneg: "\<And>x. x \<in> {a..b} \<Longrightarrow> g' x \<ge> 0"
--- a/src/HOL/Analysis/Bounded_Linear_Function.thy	Fri Feb 23 15:07:30 2018 +0100
+++ b/src/HOL/Analysis/Bounded_Linear_Function.thy	Fri Feb 23 15:17:51 2018 +0100
@@ -8,8 +8,35 @@
 imports
   Topology_Euclidean_Space
   Operator_Norm
+  Uniform_Limit
 begin
 
+lemma onorm_componentwise:
+  assumes "bounded_linear f"
+  shows "onorm f \<le> (\<Sum>i\<in>Basis. norm (f i))"
+proof -
+  {
+    fix i::'a
+    assume "i \<in> Basis"
+    hence "onorm (\<lambda>x. (x \<bullet> i) *\<^sub>R f i) \<le> onorm (\<lambda>x. (x \<bullet> i)) * norm (f i)"
+      by (auto intro!: onorm_scaleR_left_lemma bounded_linear_inner_left)
+    also have "\<dots> \<le>  norm i * norm (f i)"
+      by (rule mult_right_mono)
+        (auto simp: ac_simps Cauchy_Schwarz_ineq2 intro!: onorm_le)
+    finally have "onorm (\<lambda>x. (x \<bullet> i) *\<^sub>R f i) \<le> norm (f i)" using \<open>i \<in> Basis\<close>
+      by simp
+  } hence "onorm (\<lambda>x. \<Sum>i\<in>Basis. (x \<bullet> i) *\<^sub>R f i) \<le> (\<Sum>i\<in>Basis. norm (f i))"
+    by (auto intro!: order_trans[OF onorm_sum_le] bounded_linear_scaleR_const
+      sum_mono bounded_linear_inner_left)
+  also have "(\<lambda>x. \<Sum>i\<in>Basis. (x \<bullet> i) *\<^sub>R f i) = (\<lambda>x. f (\<Sum>i\<in>Basis. (x \<bullet> i) *\<^sub>R i))"
+    by (simp add: linear_sum bounded_linear.linear assms linear_simps)
+  also have "\<dots> = f"
+    by (simp add: euclidean_representation)
+  finally show ?thesis .
+qed
+
+lemmas onorm_componentwise_le = order_trans[OF onorm_componentwise]
+
 subsection \<open>Intro rules for @{term bounded_linear}\<close>
 
 named_theorems bounded_linear_intros
@@ -447,6 +474,15 @@
   shows "continuous F f"
   using assms by (auto simp: continuous_def intro!: tendsto_componentwise1)
 
+lemma
+  continuous_on_blinfun_componentwise:
+  fixes f:: "'d::t2_space \<Rightarrow> 'e::euclidean_space \<Rightarrow>\<^sub>L 'f::real_normed_vector"
+  assumes "\<And>i. i \<in> Basis \<Longrightarrow> continuous_on s (\<lambda>x. f x i)"
+  shows "continuous_on s f"
+  using assms
+  by (auto intro!: continuous_at_imp_continuous_on intro!: tendsto_componentwise1
+    simp: continuous_on_eq_continuous_within continuous_def)
+
 lemma bounded_linear_blinfun_matrix: "bounded_linear (\<lambda>x. (x::_\<Rightarrow>\<^sub>L _) j \<bullet> i)"
   by (auto intro!: bounded_linearI' bounded_linear_intros)
 
@@ -692,4 +728,9 @@
 lemma bounded_linear_blinfun_mult_left[bounded_linear]: "bounded_linear blinfun_mult_left"
   by transfer (rule bounded_bilinear.flip[OF bounded_bilinear_mult])
 
+lemmas bounded_linear_function_uniform_limit_intros[uniform_limit_intros] =
+  bounded_linear.uniform_limit[OF bounded_linear_apply_blinfun]
+  bounded_linear.uniform_limit[OF bounded_linear_blinfun_apply]
+  bounded_linear.uniform_limit[OF bounded_linear_blinfun_matrix]
+
 end
--- a/src/HOL/Analysis/Cartesian_Euclidean_Space.thy	Fri Feb 23 15:07:30 2018 +0100
+++ b/src/HOL/Analysis/Cartesian_Euclidean_Space.thy	Fri Feb 23 15:17:51 2018 +0100
@@ -1,7 +1,7 @@
 section \<open>Instantiates the finite Cartesian product of Euclidean spaces as a Euclidean space.\<close>
 
 theory Cartesian_Euclidean_Space
-imports Finite_Cartesian_Product Derivative 
+imports Finite_Cartesian_Product Derivative
 begin
 
 lemma subspace_special_hyperplane: "subspace {x. x $ k = 0}"
@@ -277,14 +277,22 @@
   by (simp add: vec_eq_iff)
 
 lemma norm_eq_0_imp: "norm x = 0 ==> x = (0::real ^'n)" by (metis norm_eq_zero)
+
+lemma norm_axis_1 [simp]: "norm (axis m (1::real)) = 1"
+  by (simp add: inner_axis' norm_eq_1)
+
 lemma vector_mul_eq_0[simp]: "(a *s x = 0) \<longleftrightarrow> a = (0::'a::idom) \<or> x = 0"
   by vector
+
 lemma vector_mul_lcancel[simp]: "a *s x = a *s y \<longleftrightarrow> a = (0::real) \<or> x = y"
   by (metis eq_iff_diff_eq_0 vector_mul_eq_0 vector_ssub_ldistrib)
+
 lemma vector_mul_rcancel[simp]: "a *s x = b *s x \<longleftrightarrow> (a::real) = b \<or> x = 0"
   by (metis eq_iff_diff_eq_0 vector_mul_eq_0 vector_sub_rdistrib)
+
 lemma vector_mul_lcancel_imp: "a \<noteq> (0::real) ==>  a *s x = a *s y ==> (x = y)"
   by (metis vector_mul_lcancel)
+
 lemma vector_mul_rcancel_imp: "x \<noteq> 0 \<Longrightarrow> (a::real) *s x = b *s x ==> a = b"
   by (metis vector_mul_rcancel)
 
@@ -563,7 +571,7 @@
 lemma transpose_mat [simp]: "transpose (mat n) = mat n"
   by (vector transpose_def mat_def)
 
-lemma transpose_transpose: "transpose(transpose A) = A"
+lemma transpose_transpose [simp]: "transpose(transpose A) = A"
   by (vector transpose_def)
 
 lemma row_transpose [simp]:
@@ -576,10 +584,10 @@
   shows "column i (transpose A) = row i A"
   by (simp add: row_def column_def transpose_def vec_eq_iff)
 
-lemma rows_transpose: "rows(transpose (A::'a::semiring_1^_^_)) = columns A"
+lemma rows_transpose [simp]: "rows(transpose (A::'a::semiring_1^_^_)) = columns A"
   by (auto simp add: rows_def columns_def row_transpose intro: set_eqI)
 
-lemma columns_transpose: "columns(transpose (A::'a::semiring_1^_^_)) = rows A"
+lemma columns_transpose [simp]: "columns(transpose (A::'a::semiring_1^_^_)) = rows A"
   by (metis transpose_transpose rows_transpose)
 
 lemma matrix_mult_transpose_dot_column:
@@ -642,6 +650,12 @@
   by (simp add: linear_iff matrix_vector_mult_def vec_eq_iff
       field_simps sum_distrib_left sum.distrib)
 
+lemma
+  fixes A :: "real^'n^'m"
+  shows matrix_vector_mult_linear_continuous_at [continuous_intros]: "isCont (( *v) A) z"
+    and matrix_vector_mult_linear_continuous_on [continuous_intros]: "continuous_on S (( *v) A)"
+  by (simp_all add: linear_linear linear_continuous_at linear_continuous_on matrix_vector_mul_linear)
+
 lemma matrix_vector_mult_add_distrib [algebra_simps]:
   fixes A :: "real^'n^'m"
   shows "A *v (x + y) = A *v x + A *v y"
@@ -682,6 +696,8 @@
 lemma matrix_vector_mul: "linear f ==> f = (\<lambda>x. matrix f *v (x::real ^ 'n))"
   by (simp add: ext matrix_works)
 
+declare matrix_vector_mul [symmetric, simp]
+
 lemma matrix_of_matrix_vector_mul [simp]: "matrix(\<lambda>x. A *v (x :: real ^ 'n)) = A"
   by (simp add: matrix_eq matrix_vector_mul_linear matrix_works)
 
@@ -1455,4 +1471,9 @@
   unfolding vec_lambda_beta
   by auto
 
+lemmas cartesian_euclidean_space_uniform_limit_intros[uniform_limit_intros] =
+  bounded_linear.uniform_limit[OF blinfun.bounded_linear_right]
+  bounded_linear.uniform_limit[OF bounded_linear_vec_nth]
+  bounded_linear.uniform_limit[OF bounded_linear_component_cart]
+
 end
--- a/src/HOL/Analysis/Cauchy_Integral_Theorem.thy	Fri Feb 23 15:07:30 2018 +0100
+++ b/src/HOL/Analysis/Cauchy_Integral_Theorem.thy	Fri Feb 23 15:17:51 2018 +0100
@@ -1199,7 +1199,7 @@
 
 lemma vector_derivative_linepath_within:
     "x \<in> {0..1} \<Longrightarrow> vector_derivative (linepath a b) (at x within {0..1}) = b - a"
-  apply (rule vector_derivative_within_closed_interval [of 0 "1::real", simplified])
+  apply (rule vector_derivative_within_cbox [of 0 "1::real", simplified])
   apply (auto simp: has_vector_derivative_linepath_within)
   done
 
@@ -2695,7 +2695,7 @@
   then have *: "(\<lambda>y. (?pathint x y - f x * (y - x)) /\<^sub>R cmod (y - x)) \<midarrow>x\<rightarrow> 0"
     by (simp add: Lim_at dist_norm inverse_eq_divide)
   show ?thesis
-    apply (simp add: has_field_derivative_def has_derivative_at bounded_linear_mult_right)
+    apply (simp add: has_field_derivative_def has_derivative_at2 bounded_linear_mult_right)
     apply (rule Lim_transform [OF * Lim_eventually])
     apply (simp add: inverse_eq_divide [symmetric] eventually_at)
     using \<open>open s\<close> x
@@ -3573,7 +3573,7 @@
       if "x \<in> {0..1} - S" for x
     proof -
       have "vector_derivative (uminus \<circ> \<gamma>) (at x within cbox 0 1) = - vector_derivative \<gamma> (at x within cbox 0 1)"
-        apply (rule vector_derivative_within_closed_interval)
+        apply (rule vector_derivative_within_cbox)
         using that
           apply (auto simp: o_def)
         apply (rule has_vector_derivative_minus)
--- a/src/HOL/Analysis/Connected.thy	Fri Feb 23 15:07:30 2018 +0100
+++ b/src/HOL/Analysis/Connected.thy	Fri Feb 23 15:17:51 2018 +0100
@@ -1095,6 +1095,43 @@
   qed
 qed
 
+text \<open>Hence some handy theorems on distance, diameter etc. of/from a set.\<close>
+
+lemma distance_attains_sup:
+  assumes "compact s" "s \<noteq> {}"
+  shows "\<exists>x\<in>s. \<forall>y\<in>s. dist a y \<le> dist a x"
+proof (rule continuous_attains_sup [OF assms])
+  {
+    fix x
+    assume "x\<in>s"
+    have "(dist a \<longlongrightarrow> dist a x) (at x within s)"
+      by (intro tendsto_dist tendsto_const tendsto_ident_at)
+  }
+  then show "continuous_on s (dist a)"
+    unfolding continuous_on ..
+qed
+
+text \<open>For \emph{minimal} distance, we only need closure, not compactness.\<close>
+
+lemma distance_attains_inf:
+  fixes a :: "'a::heine_borel"
+  assumes "closed s" and "s \<noteq> {}"
+  obtains x where "x\<in>s" "\<And>y. y \<in> s \<Longrightarrow> dist a x \<le> dist a y"
+proof -
+  from assms obtain b where "b \<in> s" by auto
+  let ?B = "s \<inter> cball a (dist b a)"
+  have "?B \<noteq> {}" using \<open>b \<in> s\<close>
+    by (auto simp: dist_commute)
+  moreover have "continuous_on ?B (dist a)"
+    by (auto intro!: continuous_at_imp_continuous_on continuous_dist continuous_ident continuous_const)
+  moreover have "compact ?B"
+    by (intro closed_Int_compact \<open>closed s\<close> compact_cball)
+  ultimately obtain x where "x \<in> ?B" "\<forall>y\<in>?B. dist a x \<le> dist a y"
+    by (metis continuous_attains_inf)
+  with that show ?thesis by fastforce
+qed
+
+
 subsection\<open>Relations among convergence and absolute convergence for power series.\<close>
 
 lemma summable_imp_bounded:
@@ -1353,6 +1390,24 @@
   shows "infdist x S > 0"
 using in_closed_iff_infdist_zero[OF assms(1) assms(2), of x] assms(3) infdist_nonneg le_less by fastforce
 
+lemma
+  infdist_attains_inf:
+  fixes X::"'a::heine_borel set"
+  assumes "closed X"
+  assumes "X \<noteq> {}"
+  obtains x where "x \<in> X" "infdist y X = dist y x"
+proof -
+  have "bdd_below (dist y ` X)"
+    by auto
+  from distance_attains_inf[OF assms, of y]
+  obtain x where INF: "x \<in> X" "\<And>z. z \<in> X \<Longrightarrow> dist y x \<le> dist y z" by auto
+  have "infdist y X = dist y x"
+    by (auto simp: infdist_def assms
+      intro!: antisym cINF_lower[OF _ \<open>x \<in> X\<close>] cINF_greatest[OF assms(2) INF(2)])
+  with \<open>x \<in> X\<close> show ?thesis ..
+qed
+
+
 text \<open>Every metric space is a T4 space:\<close>
 
 instance metric_space \<subseteq> t4_space
@@ -1423,6 +1478,36 @@
   shows "continuous F (\<lambda>x. infdist (f x) A)"
   using assms unfolding continuous_def by (rule tendsto_infdist)
 
+lemma compact_infdist_le:
+  fixes A::"'a::heine_borel set"
+  assumes "A \<noteq> {}"
+  assumes "compact A"
+  assumes "e > 0"
+  shows "compact {x. infdist x A \<le> e}"
+proof -
+  from continuous_closed_vimage[of "{0..e}" "\<lambda>x. infdist x A"]
+    continuous_infdist[OF continuous_ident, of _ UNIV A]
+  have "closed {x. infdist x A \<le> e}" by (auto simp: vimage_def infdist_nonneg)
+  moreover
+  from assms obtain x0 b where b: "\<And>x. x \<in> A \<Longrightarrow> dist x0 x \<le> b" "closed A"
+    by (auto simp: compact_eq_bounded_closed bounded_def)
+  {
+    fix y
+    assume le: "infdist y A \<le> e"
+    from infdist_attains_inf[OF \<open>closed A\<close> \<open>A \<noteq> {}\<close>, of y]
+    obtain z where z: "z \<in> A" "infdist y A = dist y z" by blast
+    have "dist x0 y \<le> dist y z + dist x0 z"
+      by (metis dist_commute dist_triangle)
+    also have "dist y z \<le> e" using le z by simp
+    also have "dist x0 z \<le> b" using b z by simp
+    finally have "dist x0 y \<le> b + e" by arith
+  } then
+  have "bounded {x. infdist x A \<le> e}"
+    by (auto simp: bounded_any_center[where a=x0] intro!: exI[where x="b + e"])
+  ultimately show "compact {x. infdist x A \<le> e}"
+    by (simp add: compact_eq_bounded_closed)
+qed
+
 subsection \<open>Equality of continuous functions on closure and related results.\<close>
 
 lemma continuous_closedin_preimage_constant:
@@ -2209,6 +2294,13 @@
     by (metis assms continuous_open_vimage vimage_def)
 qed
 
+lemma open_neg_translation:
+  fixes s :: "'a::real_normed_vector set"
+  assumes "open s"
+  shows "open((\<lambda>x. a - x) ` s)"
+  using open_translation[OF open_negations[OF assms], of a]
+  by (auto simp: image_image)
+
 lemma open_affinity:
   fixes S :: "'a::real_normed_vector set"
   assumes "open S"  "c \<noteq> 0"
@@ -2392,42 +2484,6 @@
     (\<forall>x \<in> s. \<forall>e>0. \<exists>d>0. (\<forall>x' \<in> s. norm(x' - x) < d \<longrightarrow> \<bar>f x' - f x\<bar> < e))"
   unfolding continuous_on_iff dist_norm by simp
 
-text \<open>Hence some handy theorems on distance, diameter etc. of/from a set.\<close>
-
-lemma distance_attains_sup:
-  assumes "compact s" "s \<noteq> {}"
-  shows "\<exists>x\<in>s. \<forall>y\<in>s. dist a y \<le> dist a x"
-proof (rule continuous_attains_sup [OF assms])
-  {
-    fix x
-    assume "x\<in>s"
-    have "(dist a \<longlongrightarrow> dist a x) (at x within s)"
-      by (intro tendsto_dist tendsto_const tendsto_ident_at)
-  }
-  then show "continuous_on s (dist a)"
-    unfolding continuous_on ..
-qed
-
-text \<open>For \emph{minimal} distance, we only need closure, not compactness.\<close>
-
-lemma distance_attains_inf:
-  fixes a :: "'a::heine_borel"
-  assumes "closed s" and "s \<noteq> {}"
-  obtains x where "x\<in>s" "\<And>y. y \<in> s \<Longrightarrow> dist a x \<le> dist a y"
-proof -
-  from assms obtain b where "b \<in> s" by auto
-  let ?B = "s \<inter> cball a (dist b a)"
-  have "?B \<noteq> {}" using \<open>b \<in> s\<close>
-    by (auto simp: dist_commute)
-  moreover have "continuous_on ?B (dist a)"
-    by (auto intro!: continuous_at_imp_continuous_on continuous_dist continuous_ident continuous_const)
-  moreover have "compact ?B"
-    by (intro closed_Int_compact \<open>closed s\<close> compact_cball)
-  ultimately obtain x where "x \<in> ?B" "\<forall>y\<in>?B. dist a x \<le> dist a y"
-    by (metis continuous_attains_inf)
-  with that show ?thesis by fastforce
-qed
-
 
 subsection \<open>Cartesian products\<close>
 
@@ -2911,6 +2967,38 @@
     using separate_compact_closed[OF assms(2,1) *] by (force simp: dist_commute)
 qed
 
+lemma compact_in_open_separated:
+  fixes A::"'a::heine_borel set"
+  assumes "A \<noteq> {}"
+  assumes "compact A"
+  assumes "open B"
+  assumes "A \<subseteq> B"
+  obtains e where "e > 0" "{x. infdist x A \<le> e} \<subseteq> B"
+proof atomize_elim
+  have "closed (- B)" "compact A" "- B \<inter> A = {}"
+    using assms by (auto simp: open_Diff compact_eq_bounded_closed)
+  from separate_closed_compact[OF this]
+  obtain d'::real where d': "d'>0" "\<And>x y. x \<notin> B \<Longrightarrow> y \<in> A \<Longrightarrow> d' \<le> dist x y"
+    by auto
+  define d where "d = d' / 2"
+  hence "d>0" "d < d'" using d' by auto
+  with d' have d: "\<And>x y. x \<notin> B \<Longrightarrow> y \<in> A \<Longrightarrow> d < dist x y"
+    by force
+  show "\<exists>e>0. {x. infdist x A \<le> e} \<subseteq> B"
+  proof (rule ccontr)
+    assume "\<nexists>e. 0 < e \<and> {x. infdist x A \<le> e} \<subseteq> B"
+    with \<open>d > 0\<close> obtain x where x: "infdist x A \<le> d" "x \<notin> B"
+      by auto
+    from assms have "closed A" "A \<noteq> {}" by (auto simp: compact_eq_bounded_closed)
+    from infdist_attains_inf[OF this]
+    obtain y where y: "y \<in> A" "infdist x A = dist x y"
+      by auto
+    have "dist x y \<le> d" using x y by simp
+    also have "\<dots> < dist x y" using y d x by auto
+    finally show False by simp
+  qed
+qed
+
 
 subsection \<open>Compact sets and the closure operation.\<close>
 
@@ -4221,6 +4309,14 @@
     using \<open>x\<in>s\<close> by blast
 qed
 
+lemma banach_fix_type:
+  fixes f::"'a::complete_space\<Rightarrow>'a"
+  assumes c:"0 \<le> c" "c < 1"
+      and lipschitz:"\<forall>x. \<forall>y. dist (f x) (f y) \<le> c * dist x y"
+  shows "\<exists>!x. (f x = x)"
+  using assms banach_fix[OF complete_UNIV UNIV_not_empty assms(1,2) subset_UNIV, of f]
+  by auto
+
 
 subsection \<open>Edelstein fixed point theorem\<close>
 
@@ -4687,6 +4783,21 @@
     by (simp add: \<open>countable \<F>'\<close> countable_subset)
 qed
 
+lemma countable_disjoint_nonempty_interior_subsets:
+  fixes \<F> :: "'a::euclidean_space set set"
+  assumes pw: "pairwise disjnt \<F>" and int: "\<And>S. \<lbrakk>S \<in> \<F>; interior S = {}\<rbrakk> \<Longrightarrow> S = {}"
+  shows "countable \<F>"
+proof (rule countable_image_inj_on)
+  have "disjoint (interior ` \<F>)"
+    using pw by (simp add: disjoint_image_subset interior_subset)
+  then show "countable (interior ` \<F>)"
+    by (auto intro: countable_disjoint_open_subsets)
+  show "inj_on interior \<F>"
+    using pw apply (clarsimp simp: inj_on_def pairwise_def)
+    apply (metis disjnt_def disjnt_subset1 inf.orderE int interior_subset)
+    done
+qed
+
 lemma closedin_compact:
    "\<lbrakk>compact S; closedin (subtopology euclidean S) T\<rbrakk> \<Longrightarrow> compact T"
 by (metis closedin_closed compact_Int_closed)
--- a/src/HOL/Analysis/Convex_Euclidean_Space.thy	Fri Feb 23 15:07:30 2018 +0100
+++ b/src/HOL/Analysis/Convex_Euclidean_Space.thy	Fri Feb 23 15:17:51 2018 +0100
@@ -6659,9 +6659,13 @@
 
 subsection \<open>On \<open>real\<close>, \<open>is_interval\<close>, \<open>convex\<close> and \<open>connected\<close> are all equivalent.\<close>
 
-lemma is_interval_1:
-  "is_interval (s::real set) \<longleftrightarrow> (\<forall>a\<in>s. \<forall>b\<in>s. \<forall> x. a \<le> x \<and> x \<le> b \<longrightarrow> x \<in> s)"
-  unfolding is_interval_def by auto
+lemma mem_is_interval_1_I:
+  fixes a b c::real
+  assumes "is_interval S"
+  assumes "a \<in> S" "c \<in> S"
+  assumes "a \<le> b" "b \<le> c"
+  shows "b \<in> S"
+  using assms is_interval_1 by blast
 
 lemma is_interval_connected_1:
   fixes s :: "real set"
@@ -6708,6 +6712,9 @@
   shows "is_interval s \<longleftrightarrow> convex s"
   by (metis is_interval_convex convex_connected is_interval_connected_1)
 
+lemma is_interval_ball_real: "is_interval (ball a b)" for a b::real
+  by (metis connected_ball is_interval_connected_1)
+
 lemma connected_compact_interval_1:
      "connected S \<and> compact S \<longleftrightarrow> (\<exists>a b. S = {a..b::real})"
   by (auto simp: is_interval_connected_1 [symmetric] is_interval_compact)
@@ -6731,6 +6738,10 @@
     by (metis connected_convex_1 convex_linear_vimage linf convex_connected connected_linear_image)
 qed
 
+lemma is_interval_cball_1[intro, simp]: "is_interval (cball a b)" for a b::real
+  by (auto simp: is_interval_convex_1 convex_cball)
+
+
 subsection \<open>Another intermediate value theorem formulation\<close>
 
 lemma ivt_increasing_component_on_1:
--- a/src/HOL/Analysis/Derivative.thy	Fri Feb 23 15:07:30 2018 +0100
+++ b/src/HOL/Analysis/Derivative.thy	Fri Feb 23 15:17:51 2018 +0100
@@ -48,18 +48,6 @@
   shows "((\<lambda>x. h (f x) (g x)) has_derivative (\<lambda>d. h (f x) (g' d) + h (f' d) (g x))) (at x)"
   using has_derivative_bilinear_within[of f f' x UNIV g g' h] assms by simp
 
-text \<open>These are the only cases we'll care about, probably.\<close>
-
-lemma has_derivative_within: "(f has_derivative f') (at x within s) \<longleftrightarrow>
-    bounded_linear f' \<and> ((\<lambda>y. (1 / norm(y - x)) *\<^sub>R (f y - (f x + f' (y - x)))) \<longlongrightarrow> 0) (at x within s)"
-  unfolding has_derivative_def Lim
-  by (auto simp add: netlimit_within field_simps)
-
-lemma has_derivative_at: "(f has_derivative f') (at x) \<longleftrightarrow>
-    bounded_linear f' \<and> ((\<lambda>y. (1 / (norm(y - x))) *\<^sub>R (f y - (f x + f' (y - x)))) \<longlongrightarrow> 0) (at x)"
-  using has_derivative_within [of f f' x UNIV]
-  by simp
-
 text \<open>More explicit epsilon-delta forms.\<close>
 
 lemma has_derivative_within':
@@ -131,27 +119,6 @@
     by (auto simp add: continuous_within DERIV_within_iff cong: Lim_cong_within)
 qed
 
-subsubsection \<open>Limit transformation for derivatives\<close>
-
-lemma has_derivative_transform_within:
-  assumes "(f has_derivative f') (at x within s)"
-    and "0 < d"
-    and "x \<in> s"
-    and "\<And>x'. \<lbrakk>x' \<in> s; dist x' x < d\<rbrakk> \<Longrightarrow> f x' = g x'"
-  shows "(g has_derivative f') (at x within s)"
-  using assms
-  unfolding has_derivative_within
-  by (force simp add: intro: Lim_transform_within)
-
-lemma has_derivative_transform_within_open:
-  assumes "(f has_derivative f') (at x)"
-    and "open s"
-    and "x \<in> s"
-    and "\<And>x. x\<in>s \<Longrightarrow> f x = g x"
-  shows "(g has_derivative f') (at x)"
-  using assms  unfolding has_derivative_at
-  by (force simp add: intro: Lim_transform_within_open)
-
 subsection \<open>Differentiability\<close>
 
 definition
@@ -304,6 +271,10 @@
   unfolding differentiable_on_def
   by auto
 
+lemma has_derivative_continuous_on:
+  "(\<And>x. x \<in> s \<Longrightarrow> (f has_derivative f' x) (at x within s)) \<Longrightarrow> continuous_on s f"
+  by (auto intro!: differentiable_imp_continuous_on differentiableI simp: differentiable_on_def)
+
 text \<open>Results about neighborhoods filter.\<close>
 
 lemma eventually_nhds_metric_le:
@@ -1143,6 +1114,20 @@
     by (simp add: g_def field_simps linear_diff[OF has_derivative_linear[OF f']])
 qed
 
+lemma vector_differentiable_bound_linearization:
+  fixes f::"real \<Rightarrow> 'b::real_normed_vector"
+  assumes f': "\<And>x. x \<in> S \<Longrightarrow> (f has_vector_derivative f' x) (at x within S)"
+  assumes "closed_segment a b \<subseteq> S"
+  assumes B: "\<forall>x\<in>S. norm (f' x - f' x0) \<le> B"
+  assumes "x0 \<in> S"
+  shows "norm (f b - f a - (b - a) *\<^sub>R f' x0) \<le> norm (b - a) * B"
+  using assms
+  by (intro differentiable_bound_linearization[of a b S f "\<lambda>x h. h *\<^sub>R f' x" x0 B])
+    (force simp: closed_segment_real_eq has_vector_derivative_def
+      scaleR_diff_right[symmetric] mult.commute[of B]
+      intro!: onorm_le mult_left_mono)+
+
+
 text \<open>In particular.\<close>
 
 lemma has_derivative_zero_constant:
@@ -1169,6 +1154,14 @@
     using assms(2)[of x] by (simp add: has_field_derivative_def A)
 qed fact
 
+lemma
+  has_vector_derivative_zero_constant:
+  assumes "convex s"
+  assumes "\<And>x. x \<in> s \<Longrightarrow> (f has_vector_derivative 0) (at x within s)"
+  obtains c where "\<And>x. x \<in> s \<Longrightarrow> f x = c"
+  using has_derivative_zero_constant[of s f] assms
+  by (auto simp: has_vector_derivative_def)
+
 lemma has_derivative_zero_unique:
   fixes f :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_vector"
   assumes "convex s"
@@ -2510,7 +2503,7 @@
 apply (auto simp: vector_derivative_works has_vector_derivative_def has_field_derivative_def mult_commute_abs)
 done
 
-lemma vector_derivative_within_closed_interval:
+lemma vector_derivative_within_cbox:
   assumes ab: "a < b" "x \<in> cbox a b"
   assumes f: "(f has_vector_derivative f') (at x within cbox a b)"
   shows "vector_derivative f (at x within cbox a b) = f'"
@@ -2518,6 +2511,14 @@
             vector_derivative_works[THEN iffD1] differentiableI_vector)
      fact
 
+lemma vector_derivative_within_closed_interval:
+  fixes f::"real \<Rightarrow> 'a::euclidean_space"
+  assumes "a < b" and "x \<in> {a .. b}"
+  assumes "(f has_vector_derivative f') (at x within {a .. b})"
+  shows "vector_derivative f (at x within {a .. b}) = f'"
+  using assms vector_derivative_within_cbox
+  by fastforce
+
 lemma has_vector_derivative_within_subset:
   "(f has_vector_derivative f') (at x within s) \<Longrightarrow> t \<subseteq> s \<Longrightarrow> (f has_vector_derivative f') (at x within t)"
   by (auto simp: has_vector_derivative_def intro: has_derivative_within_subset)
@@ -2561,6 +2562,14 @@
   unfolding has_vector_derivative_def
   by (rule has_derivative_transform_within_open)
 
+lemma has_vector_derivative_transform:
+  assumes "x \<in> s" "\<And>x. x \<in> s \<Longrightarrow> g x = f x"
+  assumes f': "(f has_vector_derivative f') (at x within s)"
+  shows "(g has_vector_derivative f') (at x within s)"
+  using assms
+  unfolding has_vector_derivative_def
+  by (rule has_derivative_transform)
+
 lemma vector_diff_chain_at:
   assumes "(f has_vector_derivative f') (at x)"
     and "(g has_vector_derivative g') (at (f x))"
@@ -2589,7 +2598,7 @@
 lemma vector_derivative_at_within_ivl:
   "(f has_vector_derivative f') (at x) \<Longrightarrow>
     a \<le> x \<Longrightarrow> x \<le> b \<Longrightarrow> a<b \<Longrightarrow> vector_derivative f (at x within {a..b}) = f'"
-using has_vector_derivative_at_within vector_derivative_within_closed_interval by fastforce
+  using has_vector_derivative_at_within vector_derivative_within_cbox by fastforce
 
 lemma vector_derivative_chain_at:
   assumes "f differentiable at x" "(g differentiable at (f x))"
@@ -2917,21 +2926,19 @@
 qed
 
 lemma has_derivative_partialsI:
-  assumes fx: "\<And>x y. x \<in> X \<Longrightarrow> y \<in> Y \<Longrightarrow> ((\<lambda>x. f x y) has_derivative blinfun_apply (fx x y)) (at x within X)"
+  fixes f::"'a::real_normed_vector \<Rightarrow> 'b::real_normed_vector \<Rightarrow> 'c::real_normed_vector"
+  assumes fx: "((\<lambda>x. f x y) has_derivative fx) (at x within X)"
   assumes fy: "\<And>x y. x \<in> X \<Longrightarrow> y \<in> Y \<Longrightarrow> ((\<lambda>y. f x y) has_derivative blinfun_apply (fy x y)) (at y within Y)"
-  assumes fx_cont: "continuous_on (X \<times> Y) (\<lambda>(x, y). fx x y)"
-  assumes fy_cont: "continuous_on (X \<times> Y) (\<lambda>(x, y). fy x y)"
-  assumes "x \<in> X" "y \<in> Y"
-  assumes "convex X" "convex Y"
-  shows "((\<lambda>(x, y). f x y) has_derivative (\<lambda>(tx, ty). fx x y tx + fy x y ty)) (at (x, y) within X \<times> Y)"
+  assumes fy_cont[unfolded continuous_within]: "continuous (at (x, y) within X \<times> Y) (\<lambda>(x, y). fy x y)"
+  assumes "y \<in> Y" "convex Y"
+  shows "((\<lambda>(x, y). f x y) has_derivative (\<lambda>(tx, ty). fx tx + fy x y ty)) (at (x, y) within X \<times> Y)"
 proof (safe intro!: has_derivativeI tendstoI, goal_cases)
   case (2 e')
+  interpret fx: bounded_linear "fx" using fx by (rule has_derivative_bounded_linear)
   define e where "e = e' / 9"
   have "e > 0" using \<open>e' > 0\<close> by (simp add: e_def)
 
-  have "(x, y) \<in> X \<times> Y" using assms by auto
-  from fy_cont[unfolded continuous_on_eq_continuous_within, rule_format, OF this,
-    unfolded continuous_within, THEN tendstoD, OF \<open>e > 0\<close>]
+  from fy_cont[THEN tendstoD, OF \<open>e > 0\<close>]
   have "\<forall>\<^sub>F (x', y') in at (x, y) within X \<times> Y. dist (fy x' y') (fy x y) < e"
     by (auto simp: split_beta')
   from this[unfolded eventually_at] obtain d' where
@@ -2971,12 +2978,12 @@
   } note onorm = this
 
   have ev_mem: "\<forall>\<^sub>F (x', y') in at (x, y) within X \<times> Y. (x', y') \<in> X \<times> Y"
-    using \<open>x \<in> X\<close> \<open>y \<in> Y\<close>
+    using \<open>y \<in> Y\<close>
     by (auto simp: eventually_at intro!: zero_less_one)
   moreover
   have ev_dist: "\<forall>\<^sub>F xy in at (x, y) within X \<times> Y. dist xy (x, y) < d" if "d > 0" for d
     using eventually_at_ball[OF that]
-    by (rule eventually_elim2) (auto simp: dist_commute intro!: eventually_True)
+    by (rule eventually_elim2) (auto simp: dist_commute mem_ball intro!: eventually_True)
   note ev_dist[OF \<open>0 < d\<close>]
   ultimately
   have "\<forall>\<^sub>F (x', y') in at (x, y) within X \<times> Y.
@@ -2997,32 +3004,31 @@
       have "\<dots> \<subseteq> ball y d \<inter> Y"
         using \<open>y \<in> Y\<close> \<open>0 < d\<close> dy y'
         by (intro \<open>convex ?S\<close>[unfolded convex_contains_segment, rule_format, of y y'])
-          (auto simp: dist_commute)
+          (auto simp: dist_commute mem_ball)
       finally have "y + t *\<^sub>R (y' - y) \<in> ?S" .
     } note seg = this
 
     have "\<forall>x\<in>ball y d \<inter> Y. onorm (blinfun_apply (fy x' x) - blinfun_apply (fy x' y)) \<le> e + e"
-      by (safe intro!: onorm less_imp_le \<open>x' \<in> X\<close> dx) (auto simp: dist_commute \<open>0 < d\<close> \<open>y \<in> Y\<close>)
+      by (safe intro!: onorm less_imp_le \<open>x' \<in> X\<close> dx) (auto simp: mem_ball dist_commute \<open>0 < d\<close> \<open>y \<in> Y\<close>)
     with seg has_derivative_within_subset[OF assms(2)[OF \<open>x' \<in> X\<close>]]
     show "norm (f x' y' - f x' y - (fy x' y) (y' - y)) \<le> norm (y' - y) * (e + e)"
       by (rule differentiable_bound_linearization[where S="?S"])
         (auto intro!: \<open>0 < d\<close> \<open>y \<in> Y\<close>)
   qed
   moreover
-  let ?le = "\<lambda>x'. norm (f x' y - f x y - (fx x y) (x' - x)) \<le> norm (x' - x) * e"
-  from fx[OF \<open>x \<in> X\<close> \<open>y \<in> Y\<close>, unfolded has_derivative_within, THEN conjunct2, THEN tendstoD, OF \<open>0 < e\<close>]
+  let ?le = "\<lambda>x'. norm (f x' y - f x y - (fx) (x' - x)) \<le> norm (x' - x) * e"
+  from fx[unfolded has_derivative_within, THEN conjunct2, THEN tendstoD, OF \<open>0 < e\<close>]
   have "\<forall>\<^sub>F x' in at x within X. ?le x'"
     by eventually_elim
-       (auto simp: dist_norm divide_simps blinfun.bilinear_simps field_simps split: if_split_asm)
+       (auto simp: dist_norm divide_simps blinfun.bilinear_simps field_simps fx.zero split: if_split_asm)
   then have "\<forall>\<^sub>F (x', y') in at (x, y) within X \<times> Y. ?le x'"
     by (rule eventually_at_Pair_within_TimesI1)
-       (simp add: blinfun.bilinear_simps)
+       (simp add: blinfun.bilinear_simps fx.zero)
   moreover have "\<forall>\<^sub>F (x', y') in at (x, y) within X \<times> Y. norm ((x', y') - (x, y)) \<noteq> 0"
     unfolding norm_eq_zero right_minus_eq
     by (auto simp: eventually_at intro!: zero_less_one)
   moreover
-  from fy_cont[unfolded continuous_on_eq_continuous_within, rule_format, OF SigmaI[OF \<open>x \<in> X\<close> \<open>y \<in> Y\<close>],
-      unfolded continuous_within, THEN tendstoD, OF \<open>0 < e\<close>]
+  from fy_cont[THEN tendstoD, OF \<open>0 < e\<close>]
   have "\<forall>\<^sub>F x' in at x within X. norm (fy x' y - fy x y) < e"
     unfolding eventually_at
     using \<open>y \<in> Y\<close>
@@ -3032,22 +3038,22 @@
        (simp add: blinfun.bilinear_simps \<open>0 < e\<close>)
   ultimately
   have "\<forall>\<^sub>F (x', y') in at (x, y) within X \<times> Y.
-            norm ((f x' y' - f x y - (fx x y (x' - x) + fy x y (y' - y))) /\<^sub>R
+            norm ((f x' y' - f x y - (fx (x' - x) + fy x y (y' - y))) /\<^sub>R
               norm ((x', y') - (x, y)))
             < e'"
     apply eventually_elim
   proof safe
     fix x' y'
-    have "norm (f x' y' - f x y - (fx x y (x' - x) + fy x y (y' - y))) \<le>
+    have "norm (f x' y' - f x y - (fx (x' - x) + fy x y (y' - y))) \<le>
         norm (f x' y' - f x' y - fy x' y (y' - y)) +
         norm (fy x y (y' - y) - fy x' y (y' - y)) +
-        norm (f x' y - f x y - fx x y (x' - x))"
+        norm (f x' y - f x y - fx (x' - x))"
       by norm
     also
     assume nz: "norm ((x', y') - (x, y)) \<noteq> 0"
       and nfy: "norm (fy x' y - fy x y) < e"
     assume "norm (f x' y' - f x' y - blinfun_apply (fy x' y) (y' - y)) \<le> norm (y' - y) * (e + e)"
-    also assume "norm (f x' y - f x y - blinfun_apply (fx x y) (x' - x)) \<le> norm (x' - x) * e"
+    also assume "norm (f x' y - f x y - (fx) (x' - x)) \<le> norm (x' - x) * e"
     also
     have "norm ((fy x y) (y' - y) - (fy x' y) (y' - y)) \<le> norm ((fy x y) - (fy x' y)) * norm (y' - y)"
       by (auto simp: blinfun.bilinear_simps[symmetric] intro!: norm_blinfun)
@@ -3070,11 +3076,80 @@
     also have "\<dots> < norm ((x', y') - (x, y)) * e'"
       using \<open>0 < e'\<close> nz
       by (auto simp: e_def)
-    finally show "norm ((f x' y' - f x y - (fx x y (x' - x) + fy x y (y' - y))) /\<^sub>R norm ((x', y') - (x, y))) < e'"
+    finally show "norm ((f x' y' - f x y - (fx (x' - x) + fy x y (y' - y))) /\<^sub>R norm ((x', y') - (x, y))) < e'"
       by (auto simp: divide_simps dist_norm mult.commute)
   qed
   then show ?case
     by eventually_elim (auto simp: dist_norm field_simps)
-qed (auto intro!: bounded_linear_intros simp: split_beta')
+next
+  from has_derivative_bounded_linear[OF fx]
+  obtain fxb where "fx = blinfun_apply fxb"
+    by (metis bounded_linear_Blinfun_apply)
+  then show "bounded_linear (\<lambda>(tx, ty). fx tx + blinfun_apply (fy x y) ty)"
+    by (auto intro!: bounded_linear_intros simp: split_beta')
+qed
+
+
+subsection \<open>Differentiable case distinction\<close>
+
+lemma has_derivative_within_If_eq:
+  "((\<lambda>x. if P x then f x else g x) has_derivative f') (at x within s) =
+    (bounded_linear f' \<and>
+     ((\<lambda>y.(if P y then (f y - ((if P x then f x else g x) + f' (y - x)))/\<^sub>R norm (y - x)
+           else (g y - ((if P x then f x else g x) + f' (y - x)))/\<^sub>R norm (y - x)))
+      \<longlongrightarrow> 0) (at x within s))"
+  (is "_ = (_ \<and> (?if \<longlongrightarrow> 0) _)")
+proof -
+  have "(\<lambda>y. (1 / norm (y - x)) *\<^sub>R
+           ((if P y then f y else g y) -
+            ((if P x then f x else g x) + f' (y - x)))) = ?if"
+    by (auto simp: inverse_eq_divide)
+  thus ?thesis by (auto simp: has_derivative_within)
+qed
+
+lemma has_derivative_If_within_closures:
+  assumes f': "x \<in> s \<union> (closure s \<inter> closure t) \<Longrightarrow>
+    (f has_derivative f' x) (at x within s \<union> (closure s \<inter> closure t))"
+  assumes g': "x \<in> t \<union> (closure s \<inter> closure t) \<Longrightarrow>
+    (g has_derivative g' x) (at x within t \<union> (closure s \<inter> closure t))"
+  assumes connect: "x \<in> closure s \<Longrightarrow> x \<in> closure t \<Longrightarrow> f x = g x"
+  assumes connect': "x \<in> closure s \<Longrightarrow> x \<in> closure t \<Longrightarrow> f' x = g' x"
+  assumes x_in: "x \<in> s \<union> t"
+  shows "((\<lambda>x. if x \<in> s then f x else g x) has_derivative
+      (if x \<in> s then f' x else g' x)) (at x within (s \<union> t))"
+proof -
+  from f' x_in interpret f': bounded_linear "if x \<in> s then f' x else (\<lambda>x. 0)"
+    by (auto simp add: has_derivative_within)
+  from g' interpret g': bounded_linear "if x \<in> t then g' x else (\<lambda>x. 0)"
+    by (auto simp add: has_derivative_within)
+  have bl: "bounded_linear (if x \<in> s then f' x else g' x)"
+    using f'.scaleR f'.bounded f'.add g'.scaleR g'.bounded g'.add x_in
+    by (unfold_locales; force)
+  show ?thesis
+    using f' g' closure_subset[of t] closure_subset[of s]
+    unfolding has_derivative_within_If_eq
+    by (intro conjI bl tendsto_If_within_closures x_in)
+      (auto simp: has_derivative_within inverse_eq_divide connect connect' set_mp)
+qed
+
+lemma has_vector_derivative_If_within_closures:
+  assumes x_in: "x \<in> s \<union> t"
+  assumes "u = s \<union> t"
+  assumes f': "x \<in> s \<union> (closure s \<inter> closure t) \<Longrightarrow>
+    (f has_vector_derivative f' x) (at x within s \<union> (closure s \<inter> closure t))"
+  assumes g': "x \<in> t \<union> (closure s \<inter> closure t) \<Longrightarrow>
+    (g has_vector_derivative g' x) (at x within t \<union> (closure s \<inter> closure t))"
+  assumes connect: "x \<in> closure s \<Longrightarrow> x \<in> closure t \<Longrightarrow> f x = g x"
+  assumes connect': "x \<in> closure s \<Longrightarrow> x \<in> closure t \<Longrightarrow> f' x = g' x"
+  shows "((\<lambda>x. if x \<in> s then f x else g x) has_vector_derivative
+    (if x \<in> s then f' x else g' x)) (at x within u)"
+  unfolding has_vector_derivative_def assms
+  using x_in
+  apply (intro has_derivative_If_within_closures[where
+        ?f' = "\<lambda>x a. a *\<^sub>R f' x" and ?g' = "\<lambda>x a. a *\<^sub>R g' x",
+        THEN has_derivative_eq_rhs])
+  subgoal by (rule f'[unfolded has_vector_derivative_def]; assumption)
+  subgoal by (rule g'[unfolded has_vector_derivative_def]; assumption)
+  by (auto simp: assms)
 
 end
--- a/src/HOL/Analysis/Determinants.thy	Fri Feb 23 15:07:30 2018 +0100
+++ b/src/HOL/Analysis/Determinants.thy	Fri Feb 23 15:17:51 2018 +0100
@@ -929,7 +929,7 @@
     by auto
 qed
 
-text \<open>Orthogonality of a transformation and matrix.\<close>
+subsection \<open>Orthogonality of a transformation and matrix.\<close>
 
 definition "orthogonal_transformation f \<longleftrightarrow> linear f \<and> (\<forall>v w. f v \<bullet> f w = v \<bullet> w)"
 
@@ -945,6 +945,51 @@
 definition "orthogonal_matrix (Q::'a::semiring_1^'n^'n) \<longleftrightarrow>
   transpose Q ** Q = mat 1 \<and> Q ** transpose Q = mat 1"
 
+lemma orthogonal_transformation_id [simp]: "orthogonal_transformation (\<lambda>x. x)"
+  by (simp add: linear_iff orthogonal_transformation_def)
+
+lemma orthogonal_orthogonal_transformation:
+    "orthogonal_transformation f \<Longrightarrow> orthogonal (f x) (f y) \<longleftrightarrow> orthogonal x y"
+  by (simp add: orthogonal_def orthogonal_transformation_def)
+
+lemma orthogonal_transformation_compose:
+   "\<lbrakk>orthogonal_transformation f; orthogonal_transformation g\<rbrakk> \<Longrightarrow> orthogonal_transformation(f \<circ> g)"
+  by (simp add: orthogonal_transformation_def linear_compose)
+
+lemma orthogonal_transformation_neg:
+  fixes f :: "real^'n \<Rightarrow> real^'n"
+  shows "orthogonal_transformation(\<lambda>x. -(f x)) \<longleftrightarrow> orthogonal_transformation f"
+  by (auto simp: orthogonal_transformation_def dest: linear_compose_neg)
+
+lemma orthogonal_transformation_linear:
+   "orthogonal_transformation f \<Longrightarrow> linear f"
+  by (simp add: orthogonal_transformation_def)
+
+lemma orthogonal_transformation_inj:
+  fixes f :: "real^'n \<Rightarrow> real^'n"
+  shows "orthogonal_transformation f \<Longrightarrow> inj f"
+  unfolding orthogonal_transformation_def inj_on_def by (metis euclidean_eqI)
+
+lemma orthogonal_transformation_surj:
+  fixes f :: "real^'n \<Rightarrow> real^'n"
+  shows "orthogonal_transformation f \<Longrightarrow> surj f"
+  by (simp add: linear_injective_imp_surjective orthogonal_transformation_inj orthogonal_transformation_linear)
+
+lemma orthogonal_transformation_bij:
+  fixes f :: "real^'n \<Rightarrow> real^'n"
+  shows "orthogonal_transformation f \<Longrightarrow> bij f"
+  by (simp add: bij_def orthogonal_transformation_inj orthogonal_transformation_surj)
+
+lemma orthogonal_transformation_inv:
+  fixes f :: "real^'n \<Rightarrow> real^'n"
+  shows "orthogonal_transformation f \<Longrightarrow> orthogonal_transformation (inv f)"
+  by (metis (no_types, hide_lams) bijection.inv_right bijection_def inj_linear_imp_inv_linear orthogonal_transformation orthogonal_transformation_bij orthogonal_transformation_inj)
+
+lemma orthogonal_transformation_norm:
+  fixes f :: "real^'n \<Rightarrow> real^'n"
+  shows "orthogonal_transformation f \<Longrightarrow> norm (f x) = norm x"
+  by (metis orthogonal_transformation)
+
 lemma orthogonal_matrix: "orthogonal_matrix (Q:: real ^'n^'n) \<longleftrightarrow> transpose Q ** Q = mat 1"
   by (metis matrix_left_right_inverse orthogonal_matrix_def)
 
@@ -1038,7 +1083,13 @@
   then show ?thesis unfolding th .
 qed
 
-text \<open>Linearity of scaling, and hence isometry, that preserves origin.\<close>
+lemma orthogonal_transformation_det [simp]:
+  fixes f :: "real^'n \<Rightarrow> real^'n"
+  shows "orthogonal_transformation f \<Longrightarrow> \<bar>det (matrix f)\<bar> = 1"
+  using det_orthogonal_matrix orthogonal_transformation_matrix by fastforce
+
+
+subsection \<open>Linearity of scaling, and hence isometry, that preserves origin.\<close>
 
 lemma scaling_linear:
   fixes f :: "real ^'n \<Rightarrow> real ^'n"
@@ -1071,20 +1122,138 @@
 lemma orthogonal_transformation_isometry:
   "orthogonal_transformation f \<longleftrightarrow> f(0::real^'n) = (0::real^'n) \<and> (\<forall>x y. dist(f x) (f y) = dist x y)"
   unfolding orthogonal_transformation
-  apply (rule iffI)
-  apply clarify
-  apply (clarsimp simp add: linear_0 linear_diff[symmetric] dist_norm)
-  apply (rule conjI)
-  apply (rule isometry_linear)
-  apply simp
-  apply simp
-  apply clarify
-  apply (erule_tac x=v in allE)
-  apply (erule_tac x=0 in allE)
-  apply (simp add: dist_norm)
-  done
+  apply (auto simp: linear_0 isometry_linear)
+   apply (metis (no_types, hide_lams) dist_norm linear_diff)
+  by (metis dist_0_norm)
+
+
+lemma image_orthogonal_transformation_ball:
+  fixes f :: "real^'n \<Rightarrow> real^'n"
+  assumes "orthogonal_transformation f"
+  shows "f ` ball x r = ball (f x) r"
+proof (intro equalityI subsetI)
+  fix y assume "y \<in> f ` ball x r"
+  with assms show "y \<in> ball (f x) r"
+    by (auto simp: orthogonal_transformation_isometry)
+next
+  fix y assume y: "y \<in> ball (f x) r"
+  then obtain z where z: "y = f z"
+    using assms orthogonal_transformation_surj by blast
+  with y assms show "y \<in> f ` ball x r"
+    by (auto simp: orthogonal_transformation_isometry)
+qed
+
+lemma image_orthogonal_transformation_cball:
+  fixes f :: "real^'n \<Rightarrow> real^'n"
+  assumes "orthogonal_transformation f"
+  shows "f ` cball x r = cball (f x) r"
+proof (intro equalityI subsetI)
+  fix y assume "y \<in> f ` cball x r"
+  with assms show "y \<in> cball (f x) r"
+    by (auto simp: orthogonal_transformation_isometry)
+next
+  fix y assume y: "y \<in> cball (f x) r"
+  then obtain z where z: "y = f z"
+    using assms orthogonal_transformation_surj by blast
+  with y assms show "y \<in> f ` cball x r"
+    by (auto simp: orthogonal_transformation_isometry)
+qed
+
+subsection\<open> We can find an orthogonal matrix taking any unit vector to any other.\<close>
+
+lemma orthogonal_matrix_transpose [simp]:
+     "orthogonal_matrix(transpose A) \<longleftrightarrow> orthogonal_matrix A"
+  by (auto simp: orthogonal_matrix_def)
+
+lemma orthogonal_matrix_orthonormal_columns:
+  fixes A :: "real^'n^'n"
+  shows "orthogonal_matrix A \<longleftrightarrow>
+          (\<forall>i. norm(column i A) = 1) \<and>
+          (\<forall>i j. i \<noteq> j \<longrightarrow> orthogonal (column i A) (column j A))"
+  by (auto simp: orthogonal_matrix matrix_mult_transpose_dot_column vec_eq_iff mat_def norm_eq_1 orthogonal_def)
+
+lemma orthogonal_matrix_orthonormal_rows:
+  fixes A :: "real^'n^'n"
+  shows "orthogonal_matrix A \<longleftrightarrow>
+          (\<forall>i. norm(row i A) = 1) \<and>
+          (\<forall>i j. i \<noteq> j \<longrightarrow> orthogonal (row i A) (row j A))"
+  using orthogonal_matrix_orthonormal_columns [of "transpose A"] by simp
 
-text \<open>Can extend an isometry from unit sphere.\<close>
+lemma orthogonal_matrix_exists_basis:
+  fixes a :: "real^'n"
+  assumes "norm a = 1"
+  obtains A where "orthogonal_matrix A" "A *v (axis k 1) = a"
+proof -
+  obtain S where "a \<in> S" "pairwise orthogonal S" and noS: "\<And>x. x \<in> S \<Longrightarrow> norm x = 1"
+   and "independent S" "card S = CARD('n)" "span S = UNIV"
+    using vector_in_orthonormal_basis assms by force
+  with independent_imp_finite obtain f0 where "bij_betw f0 (UNIV::'n set) S"
+    by (metis finite_class.finite_UNIV finite_same_card_bij)
+  then obtain f where f: "bij_betw f (UNIV::'n set) S" and a: "a = f k"
+    using bij_swap_iff [of k "inv f0 a" f0]
+    by (metis UNIV_I \<open>a \<in> S\<close> bij_betw_inv_into_right bij_betw_swap_iff swap_apply1)
+  show thesis
+  proof
+    have [simp]: "\<And>i. norm (f i) = 1"
+      using bij_betwE [OF \<open>bij_betw f UNIV S\<close>] by (blast intro: noS)
+    have [simp]: "\<And>i j. i \<noteq> j \<Longrightarrow> orthogonal (f i) (f j)"
+      using \<open>pairwise orthogonal S\<close> \<open>bij_betw f UNIV S\<close>
+      by (auto simp: pairwise_def bij_betw_def inj_on_def)
+    show "orthogonal_matrix (\<chi> i j. f j $ i)"
+      by (simp add: orthogonal_matrix_orthonormal_columns column_def)
+    show "(\<chi> i j. f j $ i) *v axis k 1 = a"
+      by (simp add: matrix_vector_mult_def axis_def a if_distrib cong: if_cong)
+  qed
+qed
+
+lemma orthogonal_transformation_exists_1:
+  fixes a b :: "real^'n"
+  assumes "norm a = 1" "norm b = 1"
+  obtains f where "orthogonal_transformation f" "f a = b"
+proof -
+  obtain k::'n where True
+    by simp
+  obtain A B where AB: "orthogonal_matrix A" "orthogonal_matrix B" and eq: "A *v (axis k 1) = a" "B *v (axis k 1) = b"
+    using orthogonal_matrix_exists_basis assms by metis
+  let ?f = "\<lambda>x. (B ** transpose A) *v x"
+  show thesis
+  proof
+    show "orthogonal_transformation ?f"
+      by (simp add: AB orthogonal_matrix_mul matrix_vector_mul_linear orthogonal_transformation_matrix)
+  next
+    show "?f a = b"
+      using \<open>orthogonal_matrix A\<close> unfolding orthogonal_matrix_def
+      by (metis eq matrix_mul_rid matrix_vector_mul_assoc)
+  qed
+qed
+
+lemma orthogonal_transformation_exists:
+  fixes a b :: "real^'n"
+  assumes "norm a = norm b"
+  obtains f where "orthogonal_transformation f" "f a = b"
+proof (cases "a = 0 \<or> b = 0")
+  case True
+  with assms show ?thesis
+    using orthogonal_transformation_isometry that by fastforce
+next
+  case False
+  then obtain f where f: "orthogonal_transformation f" and eq: "f (a /\<^sub>R norm a) = (b /\<^sub>R norm b)"
+    by (auto intro: orthogonal_transformation_exists_1 [of "a /\<^sub>R norm a" "b /\<^sub>R norm b"])
+  show ?thesis
+  proof
+    have "linear f"
+      using f by (simp add: orthogonal_transformation_linear)
+    then have "f a /\<^sub>R norm a = f (a /\<^sub>R norm a)"
+      by (simp add: linear_cmul [of f])
+    also have "\<dots> = b /\<^sub>R norm a"
+      by (simp add: eq assms [symmetric])
+    finally show "f a = b"
+      using False by auto
+  qed (use f in auto)
+qed
+
+
+subsection \<open>Can extend an isometry from unit sphere.\<close>
 
 lemma isometry_sphere_extend:
   fixes f:: "real ^'n \<Rightarrow> real ^'n"
@@ -1182,7 +1351,7 @@
     done
 qed
 
-text \<open>Rotation, reflection, rotoinversion.\<close>
+subsection \<open>Rotation, reflection, rotoinversion.\<close>
 
 definition "rotation_matrix Q \<longleftrightarrow> orthogonal_matrix Q \<and> det Q = 1"
 definition "rotoinversion_matrix Q \<longleftrightarrow> orthogonal_matrix Q \<and> det Q = - 1"
@@ -1238,4 +1407,111 @@
     by (simp add: sign_swap_id permutation_swap_id sign_compose sign_id swap_id_eq)
 qed
 
+text\<open> Slightly stronger results giving rotation, but only in two or more dimensions.\<close>
+
+lemma rotation_matrix_exists_basis:
+  fixes a :: "real^'n"
+  assumes 2: "2 \<le> CARD('n)" and "norm a = 1"
+  obtains A where "rotation_matrix A" "A *v (axis k 1) = a"
+proof -
+  obtain A where "orthogonal_matrix A" and A: "A *v (axis k 1) = a"
+    using orthogonal_matrix_exists_basis assms by metis
+  with orthogonal_rotation_or_rotoinversion
+  consider "rotation_matrix A" | "rotoinversion_matrix A"
+    by metis
+  then show thesis
+  proof cases
+    assume "rotation_matrix A"
+    then show ?thesis
+      using \<open>A *v axis k 1 = a\<close> that by auto
+  next
+    obtain j where "j \<noteq> k"
+      by (metis (full_types) 2 card_2_exists ex_card)
+    let ?TA = "transpose A"
+    let ?A = "\<chi> i. if i = j then - 1 *\<^sub>R (?TA $ i) else ?TA $i"
+    assume "rotoinversion_matrix A"
+    then have [simp]: "det A = -1"
+      by (simp add: rotoinversion_matrix_def)
+    show ?thesis
+    proof
+      have [simp]: "row i (\<chi> i. if i = j then - 1 *\<^sub>R ?TA $ i else ?TA $ i) = (if i = j then - row i ?TA else row i ?TA)" for i
+        by (auto simp: row_def)
+      have "orthogonal_matrix ?A"
+        unfolding orthogonal_matrix_orthonormal_rows
+        using \<open>orthogonal_matrix A\<close> by (auto simp: orthogonal_matrix_orthonormal_columns orthogonal_clauses)
+      then show "rotation_matrix (transpose ?A)"
+        unfolding rotation_matrix_def
+        by (simp add: det_row_mul[of j _ "\<lambda>i. ?TA $ i", unfolded scalar_mult_eq_scaleR])
+      show "transpose ?A *v axis k 1 = a"
+        using \<open>j \<noteq> k\<close> A by (simp add: matrix_vector_column axis_def scalar_mult_eq_scaleR if_distrib [of "\<lambda>z. z *\<^sub>R c" for c] cong: if_cong)
+    qed
+  qed
+qed
+
+lemma rotation_exists_1:
+  fixes a :: "real^'n"
+  assumes "2 \<le> CARD('n)" "norm a = 1" "norm b = 1"
+  obtains f where "orthogonal_transformation f" "det(matrix f) = 1" "f a = b"
+proof -
+  obtain k::'n where True
+    by simp
+  obtain A B where AB: "rotation_matrix A" "rotation_matrix B"
+               and eq: "A *v (axis k 1) = a" "B *v (axis k 1) = b"
+    using rotation_matrix_exists_basis assms by metis
+  let ?f = "\<lambda>x. (B ** transpose A) *v x"
+  show thesis
+  proof
+    show "orthogonal_transformation ?f"
+      using AB orthogonal_matrix_mul orthogonal_transformation_matrix rotation_matrix_def matrix_vector_mul_linear by force
+    show "det (matrix ?f) = 1"
+      using AB by (auto simp: det_mul rotation_matrix_def)
+    show "?f a = b"
+      using AB unfolding orthogonal_matrix_def rotation_matrix_def
+      by (metis eq matrix_mul_rid matrix_vector_mul_assoc)
+  qed
+qed
+
+lemma rotation_exists:
+  fixes a :: "real^'n"
+  assumes 2: "2 \<le> CARD('n)" and eq: "norm a = norm b"
+  obtains f where "orthogonal_transformation f" "det(matrix f) = 1" "f a = b"
+proof (cases "a = 0 \<or> b = 0")
+  case True
+  with assms have "a = 0" "b = 0"
+    by auto
+  then show ?thesis
+    by (metis eq_id_iff matrix_id orthogonal_transformation_id that)
+next
+  case False
+  with that show thesis
+    by (auto simp: eq linear_cmul orthogonal_transformation_def
+             intro: rotation_exists_1 [of "a /\<^sub>R norm a" "b /\<^sub>R norm b", OF 2])
+qed
+
+lemma rotation_rightward_line:
+  fixes a :: "real^'n"
+  obtains f where "orthogonal_transformation f" "2 \<le> CARD('n) \<Longrightarrow> det(matrix f) = 1"
+                  "f(norm a *\<^sub>R axis k 1) = a"
+proof (cases "CARD('n) = 1")
+  case True
+  obtain f where "orthogonal_transformation f" "f (norm a *\<^sub>R axis k (1::real)) = a"
+  proof (rule orthogonal_transformation_exists)
+    show "norm (norm a *\<^sub>R axis k (1::real)) = norm a"
+      by simp
+  qed auto
+  then show thesis
+    using True that by auto
+next
+  case False
+  obtain f where "orthogonal_transformation f" "det(matrix f) = 1" "f (norm a *\<^sub>R axis k 1) = a"
+  proof (rule rotation_exists)
+    show "2 \<le> CARD('n)"
+      using False one_le_card_finite [where 'a='n] by linarith
+    show "norm (norm a *\<^sub>R axis k (1::real)) = norm a"
+      by simp
+  qed auto
+  then show thesis
+    using that by blast
+qed
+
 end
--- a/src/HOL/Analysis/Euclidean_Space.thy	Fri Feb 23 15:07:30 2018 +0100
+++ b/src/HOL/Analysis/Euclidean_Space.thy	Fri Feb 23 15:17:51 2018 +0100
@@ -84,6 +84,10 @@
 lemma (in euclidean_space) euclidean_representation: "(\<Sum>b\<in>Basis. inner x b *\<^sub>R b) = x"
   unfolding euclidean_representation_sum by simp
 
+lemma (in euclidean_space) euclidean_inner: "inner x y = (\<Sum>b\<in>Basis. (inner x b) * (inner y b))"
+  by (subst (1 2) euclidean_representation [symmetric])
+    (simp add: inner_sum_right inner_Basis ac_simps)
+
 lemma (in euclidean_space) choice_Basis_iff:
   fixes P :: "'a \<Rightarrow> real \<Rightarrow> bool"
   shows "(\<forall>i\<in>Basis. \<exists>x. P i x) \<longleftrightarrow> (\<exists>x. \<forall>i\<in>Basis. P i (inner x i))"
--- a/src/HOL/Analysis/Finite_Cartesian_Product.thy	Fri Feb 23 15:07:30 2018 +0100
+++ b/src/HOL/Analysis/Finite_Cartesian_Product.thy	Fri Feb 23 15:17:51 2018 +0100
@@ -20,9 +20,19 @@
 
 declare vec_lambda_inject [simplified, simp]
 
+bundle vec_syntax begin
 notation
   vec_nth (infixl "$" 90) and
   vec_lambda (binder "\<chi>" 10)
+end
+
+bundle no_vec_syntax begin
+no_notation
+  vec_nth (infixl "$" 90) and
+  vec_lambda (binder "\<chi>" 10)
+end
+
+unbundle vec_syntax
 
 (*
   Translate "'b ^ 'n" into "'b ^ ('n :: finite)". When 'n has already more than
@@ -134,6 +144,28 @@
   qed
 qed (simp_all add: infinite_UNIV_vec)
 
+lemma countable_vector:
+  fixes B:: "'n::finite \<Rightarrow> 'a set"
+  assumes "\<And>i. countable (B i)"
+  shows "countable {V. \<forall>i::'n::finite. V $ i \<in> B i}"
+proof -
+  have "f \<in> ($) ` {V. \<forall>i. V $ i \<in> B i}" if "f \<in> Pi\<^sub>E UNIV B" for f
+  proof -
+    have "\<exists>W. (\<forall>i. W $ i \<in> B i) \<and> ($) W = f"
+      by (metis that PiE_iff UNIV_I vec_lambda_inverse)
+    then show "f \<in> ($) ` {v. \<forall>i. v $ i \<in> B i}"
+      by blast
+  qed
+  then have "Pi\<^sub>E UNIV B = vec_nth ` {V. \<forall>i::'n. V $ i \<in> B i}"
+    by blast
+  then have "countable (vec_nth ` {V. \<forall>i. V $ i \<in> B i})"
+    by (metis finite_class.finite_UNIV countable_PiE assms)
+  then have "countable (vec_lambda ` vec_nth ` {V. \<forall>i. V $ i \<in> B i})"
+    by auto
+  then show ?thesis
+    by (simp add: image_comp o_def vec_nth_inverse)
+qed
+
 subsection \<open>Group operations and class instances\<close>
 
 instantiation vec :: (zero, finite) zero
@@ -591,6 +623,9 @@
   apply (simp add: axis_def)
   done
 
+lemma inner_axis': "inner(axis i y) x = inner y (x $ i)"
+  by (simp add: inner_axis inner_commute)
+
 instantiation vec :: (euclidean_space, finite) euclidean_space
 begin
 
--- a/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy	Fri Feb 23 15:07:30 2018 +0100
+++ b/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy	Fri Feb 23 15:17:51 2018 +0100
@@ -621,6 +621,11 @@
   with False show ?thesis by (simp add: not_integrable_integral)
 qed
 
+lemma integral_mult:
+  fixes K::real
+  shows "f integrable_on X \<Longrightarrow> K * integral X f = integral X (\<lambda>x. K * f x)"
+  unfolding real_scaleR_def[symmetric] integral_cmul ..
+
 lemma integral_neg [simp]: "integral S (\<lambda>x. - f x) = - integral S f"
 proof (cases "f integrable_on S")
   case True then show ?thesis
@@ -2549,6 +2554,13 @@
 
 lemmas integrable_continuous_real = integrable_continuous_interval[where 'b=real]
 
+lemma integrable_continuous_closed_segment:
+  fixes f :: "real \<Rightarrow> 'a::banach"
+  assumes "continuous_on (closed_segment a b) f"
+  shows "f integrable_on (closed_segment a b)"
+  using assms
+  by (auto intro!: integrable_continuous_interval simp: closed_segment_eq_real_ivl)
+
 
 subsection \<open>Specialization of additivity to one dimension.\<close>
 
@@ -2722,6 +2734,32 @@
 
 subsection \<open>Taylor series expansion\<close>
 
+lemma mvt_integral:
+  fixes f::"'a::real_normed_vector\<Rightarrow>'b::banach"
+  assumes f'[derivative_intros]:
+    "\<And>x. x \<in> S \<Longrightarrow> (f has_derivative f' x) (at x within S)"
+  assumes line_in: "\<And>t. t \<in> {0..1} \<Longrightarrow> x + t *\<^sub>R y \<in> S"
+  shows "f (x + y) - f x = integral {0..1} (\<lambda>t. f' (x + t *\<^sub>R y) y)" (is ?th1)
+proof -
+  from assms have subset: "(\<lambda>xa. x + xa *\<^sub>R y) ` {0..1} \<subseteq> S" by auto
+  note [derivative_intros] =
+    has_derivative_subset[OF _ subset]
+    has_derivative_in_compose[where f="(\<lambda>xa. x + xa *\<^sub>R y)" and g = f]
+  note [continuous_intros] =
+    continuous_on_compose2[where f="(\<lambda>xa. x + xa *\<^sub>R y)"]
+    continuous_on_subset[OF _ subset]
+  have "\<And>t. t \<in> {0..1} \<Longrightarrow>
+    ((\<lambda>t. f (x + t *\<^sub>R y)) has_vector_derivative f' (x + t *\<^sub>R y) y)
+    (at t within {0..1})"
+    using assms
+    by (auto simp: has_vector_derivative_def
+        linear_cmul[OF has_derivative_linear[OF f'], symmetric]
+      intro!: derivative_eq_intros)
+  from fundamental_theorem_of_calculus[rule_format, OF _ this]
+  show ?th1
+    by (auto intro!: integral_unique[symmetric])
+qed
+
 lemma (in bounded_bilinear) sum_prod_derivatives_has_vector_derivative:
   assumes "p>0"
   and f0: "Df 0 = f"
@@ -2835,7 +2873,6 @@
 qed
 
 
-
 subsection \<open>Only need trivial subintervals if the interval itself is trivial.\<close>
 
 proposition division_of_nontrivial:
@@ -3024,6 +3061,21 @@
   unfolding integrable_on_def
   by (auto intro!: has_integral_combine)
 
+lemma integral_minus_sets:
+  fixes f::"real \<Rightarrow> 'a::banach"
+  shows "c \<le> a \<Longrightarrow> c \<le> b \<Longrightarrow> f integrable_on {c .. max a b} \<Longrightarrow>
+    integral {c .. a} f - integral {c .. b} f =
+    (if a \<le> b then - integral {a .. b} f else integral {b .. a} f)"
+  using integral_combine[of c a b f]  integral_combine[of c b a f]
+  by (auto simp: algebra_simps max_def)
+
+lemma integral_minus_sets':
+  fixes f::"real \<Rightarrow> 'a::banach"
+  shows "c \<ge> a \<Longrightarrow> c \<ge> b \<Longrightarrow> f integrable_on {min a b .. c} \<Longrightarrow>
+    integral {a .. c} f - integral {b .. c} f =
+    (if a \<le> b then integral {a .. b} f else - integral {b .. a} f)"
+  using integral_combine[of b a c f] integral_combine[of a b c f]
+  by (auto simp: algebra_simps min_def)
 
 subsection \<open>Reduce integrability to "local" integrability.\<close>
 
@@ -3129,13 +3181,19 @@
 using assms integral_has_vector_derivative_continuous_at [OF integrable_continuous_real]
   by (fastforce simp: continuous_on_eq_continuous_within)
 
+lemma integral_has_real_derivative:
+  assumes "continuous_on {a..b} g"
+  assumes "t \<in> {a..b}"
+  shows "((\<lambda>x. integral {a..x} g) has_real_derivative g t) (at t within {a..b})"
+  using integral_has_vector_derivative[of a b g t] assms
+  by (auto simp: has_field_derivative_iff_has_vector_derivative)
+
 lemma antiderivative_continuous:
   fixes q b :: real
   assumes "continuous_on {a..b} f"
   obtains g where "\<And>x. x \<in> {a..b} \<Longrightarrow> (g has_vector_derivative (f x::_::banach)) (at x within {a..b})"
   using integral_has_vector_derivative[OF assms] by auto
 
-
 subsection \<open>Combined fundamental theorem of calculus.\<close>
 
 lemma antiderivative_integral_continuous:
@@ -3149,7 +3207,8 @@
   have "(f has_integral g v - g u) {u..v}" if "u \<in> {a..b}" "v \<in> {a..b}" "u \<le> v" for u v
   proof -
     have "\<And>x. x \<in> cbox u v \<Longrightarrow> (g has_vector_derivative f x) (at x within cbox u v)"
-      by (meson g has_vector_derivative_within_subset interval_subset_is_interval is_interval_closed_interval subsetCE that(1) that(2))
+      by (metis atLeastAtMost_iff atLeastatMost_subset_iff box_real(2) g
+          has_vector_derivative_within_subset subsetCE that(1,2))
     then show ?thesis
       by (metis box_real(2) that(3) fundamental_theorem_of_calculus)
   qed
@@ -4125,6 +4184,28 @@
     by (rule continuous_on_eq) (auto intro!: continuous_intros indefinite_integral_continuous_1 assms)
 qed
 
+theorem integral_has_vector_derivative':
+  fixes f :: "real \<Rightarrow> 'b::banach"
+  assumes "continuous_on {a..b} f"
+    and "x \<in> {a..b}"
+  shows "((\<lambda>u. integral {u..b} f) has_vector_derivative - f x) (at x within {a..b})"
+proof -
+  have *: "integral {x..b} f = integral {a .. b} f - integral {a .. x} f" if "a \<le> x" "x \<le> b" for x
+    using integral_combine[of a x b for x, OF that integrable_continuous_real[OF assms(1)]]
+    by (simp add: algebra_simps)
+  show ?thesis
+    using \<open>x \<in> _\<close> *
+    by (rule has_vector_derivative_transform)
+      (auto intro!: derivative_eq_intros assms integral_has_vector_derivative)
+qed
+
+lemma integral_has_real_derivative':
+  assumes "continuous_on {a..b} g"
+  assumes "t \<in> {a..b}"
+  shows "((\<lambda>x. integral {x..b} g) has_real_derivative -g t) (at t within {a..b})"
+  using integral_has_vector_derivative'[OF assms]
+  by (auto simp: has_field_derivative_iff_has_vector_derivative)
+
 
 subsection \<open>This doesn't directly involve integration, but that gives an easy proof.\<close>
 
@@ -4661,6 +4742,10 @@
   shows "f integrable_on S \<longleftrightarrow> f integrable_on T"
   by (blast intro: integrable_spike_set assms negligible_subset)
 
+lemma integrable_on_insert_iff: "f integrable_on (insert x X) \<longleftrightarrow> f integrable_on X"
+  for f::"_ \<Rightarrow> 'a::banach"
+  by (rule integrable_spike_set_eq) (auto simp: insert_Diff_if)
+
 lemma has_integral_interior:
   fixes f :: "'a :: euclidean_space \<Rightarrow> 'b :: banach"
   shows "negligible(frontier S) \<Longrightarrow> (f has_integral y) (interior S) \<longleftrightarrow> (f has_integral y) S"
@@ -5136,7 +5221,7 @@
   fixes f :: "'n::euclidean_space \<Rightarrow> 'a::banach"
   assumes \<T>: "finite \<T>"
     and int: "\<And>S. S \<in> \<T> \<Longrightarrow> (f has_integral (i S)) S"
-    and neg: "\<And>S S'. \<lbrakk>S \<in> \<T>; S' \<in> \<T>; S \<noteq> S'\<rbrakk> \<Longrightarrow> negligible (S \<inter> S')"
+    and neg: "pairwise (\<lambda>S S'. negligible (S \<inter> S')) \<T>"
   shows "(f has_integral (sum i \<T>)) (\<Union>\<T>)"
 proof -
   let ?\<U> = "((\<lambda>(a,b). a \<inter> b) ` {(a,b). a \<in> \<T> \<and> b \<in> {y. y \<in> \<T> \<and> a \<noteq> y}})"
@@ -5151,7 +5236,7 @@
       ultimately show "finite ?\<U>"
         by (blast intro: finite_subset[of _ "\<T> \<times> \<T>"])
       show "\<And>t. t \<in> ?\<U> \<Longrightarrow> negligible t"
-        using neg by auto
+        using neg unfolding pairwise_def by auto
     qed
   next
     show "(if x \<in> \<Union>\<T> then f x else 0) = (\<Sum>A\<in>\<T>. if x \<in> A then f x else 0)"
@@ -5162,7 +5247,7 @@
         using that by blast
       ultimately show "f x = (\<Sum>A\<in>\<T>. if x \<in> A then f x else 0)"
         by (simp add: sum.delta[OF \<T>])
-    qed 
+    qed
   next
     show "((\<lambda>x. \<Sum>A\<in>\<T>. if x \<in> A then f x else 0) has_integral (\<Sum>A\<in>\<T>. i A)) UNIV"
       apply (rule has_integral_sum [OF \<T>])
@@ -5192,7 +5277,7 @@
   qed
   show ?thesis
     unfolding \<D>(6)[symmetric]
-    by (auto intro: \<D> neg assms has_integral_Union)
+    by (auto intro: \<D> neg assms has_integral_Union pairwiseI)
 qed
 
 lemma integral_combine_division_bottomup:
@@ -6049,6 +6134,26 @@
   qed
 qed
 
+lemma continuous_on_imp_absolutely_integrable_on:
+  fixes f::"real \<Rightarrow> 'a::banach"
+  shows "continuous_on {a..b} f \<Longrightarrow>
+    norm (integral {a..b} f) \<le> integral {a..b} (\<lambda>x. norm (f x))"
+  by (intro integral_norm_bound_integral integrable_continuous_real continuous_on_norm) auto
+
+lemma integral_bound:
+  fixes f::"real \<Rightarrow> 'a::banach"
+  assumes "a \<le> b"
+  assumes "continuous_on {a .. b} f"
+  assumes "\<And>t. t \<in> {a .. b} \<Longrightarrow> norm (f t) \<le> B"
+  shows "norm (integral {a .. b} f) \<le> B * (b - a)"
+proof -
+  note continuous_on_imp_absolutely_integrable_on[OF assms(2)]
+  also have "integral {a..b} (\<lambda>x. norm (f x)) \<le> integral {a..b} (\<lambda>_. B)"
+    by (rule integral_le)
+      (auto intro!: integrable_continuous_real continuous_intros assms)
+  also have "\<dots> = B * (b - a)" using assms by simp
+  finally show ?thesis .
+qed
 
 lemma integral_norm_bound_integral_component:
   fixes f :: "'n::euclidean_space \<Rightarrow> 'a::banach"
--- a/src/HOL/Analysis/L2_Norm.thy	Fri Feb 23 15:07:30 2018 +0100
+++ b/src/HOL/Analysis/L2_Norm.thy	Fri Feb 23 15:17:51 2018 +0100
@@ -98,13 +98,6 @@
   qed
 qed
 
-lemma sqrt_sum_squares_le_sum:
-  "\<lbrakk>0 \<le> x; 0 \<le> y\<rbrakk> \<Longrightarrow> sqrt (x\<^sup>2 + y\<^sup>2) \<le> x + y"
-  apply (rule power2_le_imp_le)
-  apply (simp add: power2_sum)
-  apply simp
-  done
-
 lemma L2_set_le_sum [rule_format]:
   "(\<forall>i\<in>A. 0 \<le> f i) \<longrightarrow> L2_set f A \<le> sum f A"
   apply (cases "finite A")
--- a/src/HOL/Analysis/Linear_Algebra.thy	Fri Feb 23 15:07:30 2018 +0100
+++ b/src/HOL/Analysis/Linear_Algebra.thy	Fri Feb 23 15:17:51 2018 +0100
@@ -2987,10 +2987,6 @@
 lemma infnorm_le_norm: "infnorm x \<le> norm x"
   by (simp add: Basis_le_norm infnorm_Max)
 
-lemma (in euclidean_space) euclidean_inner: "inner x y = (\<Sum>b\<in>Basis. (x \<bullet> b) * (y \<bullet> b))"
-  by (subst (1 2) euclidean_representation [symmetric])
-    (simp add: inner_sum_right inner_Basis ac_simps)
-
 lemma norm_le_infnorm:
   fixes x :: "'a::euclidean_space"
   shows "norm x \<le> sqrt DIM('a) * infnorm x"
--- a/src/HOL/Analysis/Operator_Norm.thy	Fri Feb 23 15:07:30 2018 +0100
+++ b/src/HOL/Analysis/Operator_Norm.thy	Fri Feb 23 15:17:51 2018 +0100
@@ -235,4 +235,13 @@
   shows "onorm (\<lambda>x. f x + g x) < e"
   using assms by (rule onorm_triangle [THEN order_le_less_trans])
 
+lemma onorm_sum:
+  assumes "finite S"
+  assumes "\<And>s. s \<in> S \<Longrightarrow> bounded_linear (f s)"
+  shows "onorm (\<lambda>x. sum (\<lambda>s. f s x) S) \<le> sum (\<lambda>s. onorm (f s)) S"
+  using assms
+  by (induction) (auto simp: onorm_zero intro!: onorm_triangle_le bounded_linear_sum)
+
+lemmas onorm_sum_le = onorm_sum[THEN order_trans]
+
 end
--- a/src/HOL/Analysis/Ordered_Euclidean_Space.thy	Fri Feb 23 15:07:30 2018 +0100
+++ b/src/HOL/Analysis/Ordered_Euclidean_Space.thy	Fri Feb 23 15:17:51 2018 +0100
@@ -214,9 +214,20 @@
   using image_smult_cbox[of m a b]
   by (simp add: cbox_interval)
 
-lemma is_interval_closed_interval [simp]:
-  "is_interval {a .. (b::'a::ordered_euclidean_space)}"
-  by (metis cbox_interval is_interval_cbox)
+lemma [simp]:
+  fixes a b::"'a::ordered_euclidean_space" and r s::real
+  shows is_interval_io: "is_interval {..<r}"
+    and is_interval_ic: "is_interval {..a}"
+    and is_interval_oi: "is_interval {r<..}"
+    and is_interval_ci: "is_interval {a..}"
+    and is_interval_oo: "is_interval {r<..<s}"
+    and is_interval_oc: "is_interval {r<..s}"
+    and is_interval_co: "is_interval {r..<s}"
+    and is_interval_cc: "is_interval {b..a}"
+  by (force simp: is_interval_def eucl_le[where 'a='a])+
+
+lemma is_interval_real_ereal_oo: "is_interval (real_of_ereal ` {N<..<M::ereal})"
+  by (auto simp: real_atLeastGreaterThan_eq)
 
 lemma compact_interval [simp]:
   fixes a b::"'a::ordered_euclidean_space"
--- a/src/HOL/Analysis/Product_Vector.thy	Fri Feb 23 15:07:30 2018 +0100
+++ b/src/HOL/Analysis/Product_Vector.thy	Fri Feb 23 15:17:51 2018 +0100
@@ -306,6 +306,11 @@
     by (simp add: norm_Pair divide_right_mono order_trans [OF sqrt_add_le_add_sqrt])
 qed simp
 
+lemma differentiable_Pair [simp, derivative_intros]:
+  "f differentiable at x within s \<Longrightarrow> g differentiable at x within s \<Longrightarrow>
+    (\<lambda>x. (f x, g x)) differentiable at x within s"
+  unfolding differentiable_def by (blast intro: has_derivative_Pair)
+
 lemmas has_derivative_fst [derivative_intros] = bounded_linear.has_derivative [OF bounded_linear_fst]
 lemmas has_derivative_snd [derivative_intros] = bounded_linear.has_derivative [OF bounded_linear_snd]
 
@@ -313,6 +318,17 @@
   "((\<lambda>p. f (fst p) (snd p)) has_derivative f') F \<Longrightarrow> ((\<lambda>(a, b). f a b) has_derivative f') F"
   unfolding split_beta' .
 
+
+subsubsection \<open>Vector derivatives involving pairs\<close>
+
+lemma has_vector_derivative_Pair[derivative_intros]:
+  assumes "(f has_vector_derivative f') (at x within s)"
+    "(g has_vector_derivative g') (at x within s)"
+  shows "((\<lambda>x. (f x, g x)) has_vector_derivative (f', g')) (at x within s)"
+  using assms
+  by (auto simp: has_vector_derivative_def intro!: derivative_eq_intros)
+
+
 subsection \<open>Product is an inner product space\<close>
 
 instantiation prod :: (real_inner, real_inner) real_inner
@@ -368,4 +384,9 @@
 lemma norm_snd_le: "norm y \<le> norm (x,y)"
   by (metis dist_snd_le snd_conv snd_zero norm_conv_dist)
 
+lemma norm_Pair_le:
+  shows "norm (x, y) \<le> norm x + norm y"
+  unfolding norm_Pair
+  by (metis norm_ge_zero sqrt_sum_squares_le_sum)
+
 end
--- a/src/HOL/Analysis/Riemann_Mapping.thy	Fri Feb 23 15:07:30 2018 +0100
+++ b/src/HOL/Analysis/Riemann_Mapping.thy	Fri Feb 23 15:17:51 2018 +0100
@@ -489,7 +489,7 @@
     let ?g = "\<lambda>z. (SOME g. polynomial_function g \<and> path_image g \<subseteq> S \<and> pathstart g = a \<and> pathfinish g = z)"
     show "((\<lambda>z. contour_integral (?g z) f) has_field_derivative f x)
           (at x)"
-    proof (simp add: has_field_derivative_def has_derivative_at bounded_linear_mult_right, rule Lim_transform)
+    proof (simp add: has_field_derivative_def has_derivative_at2 bounded_linear_mult_right, rule Lim_transform)
       show "(\<lambda>y. inverse(norm(y - x)) *\<^sub>R (contour_integral(linepath x y) f - f x * (y - x))) \<midarrow>x\<rightarrow> 0"
       proof (clarsimp simp add: Lim_at)
         fix e::real assume "e > 0"
--- a/src/HOL/Analysis/Starlike.thy	Fri Feb 23 15:07:30 2018 +0100
+++ b/src/HOL/Analysis/Starlike.thy	Fri Feb 23 15:17:51 2018 +0100
@@ -13,9 +13,87 @@
 
 begin
 
+subsection \<open>Midpoint\<close>
+
 definition midpoint :: "'a::real_vector \<Rightarrow> 'a \<Rightarrow> 'a"
   where "midpoint a b = (inverse (2::real)) *\<^sub>R (a + b)"
 
+lemma midpoint_idem [simp]: "midpoint x x = x"
+  unfolding midpoint_def
+  unfolding scaleR_right_distrib
+  unfolding scaleR_left_distrib[symmetric]
+  by auto
+
+lemma midpoint_sym: "midpoint a b = midpoint b a"
+  unfolding midpoint_def by (auto simp add: scaleR_right_distrib)
+
+lemma midpoint_eq_iff: "midpoint a b = c \<longleftrightarrow> a + b = c + c"
+proof -
+  have "midpoint a b = c \<longleftrightarrow> scaleR 2 (midpoint a b) = scaleR 2 c"
+    by simp
+  then show ?thesis
+    unfolding midpoint_def scaleR_2 [symmetric] by simp
+qed
+
+lemma
+  fixes a::real
+  assumes "a \<le> b" shows ge_midpoint_1: "a \<le> midpoint a b"
+                    and le_midpoint_1: "midpoint a b \<le> b"
+  by (simp_all add: midpoint_def assms)
+
+lemma dist_midpoint:
+  fixes a b :: "'a::real_normed_vector" shows
+  "dist a (midpoint a b) = (dist a b) / 2" (is ?t1)
+  "dist b (midpoint a b) = (dist a b) / 2" (is ?t2)
+  "dist (midpoint a b) a = (dist a b) / 2" (is ?t3)
+  "dist (midpoint a b) b = (dist a b) / 2" (is ?t4)
+proof -
+  have *: "\<And>x y::'a. 2 *\<^sub>R x = - y \<Longrightarrow> norm x = (norm y) / 2"
+    unfolding equation_minus_iff by auto
+  have **: "\<And>x y::'a. 2 *\<^sub>R x =   y \<Longrightarrow> norm x = (norm y) / 2"
+    by auto
+  note scaleR_right_distrib [simp]
+  show ?t1
+    unfolding midpoint_def dist_norm
+    apply (rule **)
+    apply (simp add: scaleR_right_diff_distrib)
+    apply (simp add: scaleR_2)
+    done
+  show ?t2
+    unfolding midpoint_def dist_norm
+    apply (rule *)
+    apply (simp add: scaleR_right_diff_distrib)
+    apply (simp add: scaleR_2)
+    done
+  show ?t3
+    unfolding midpoint_def dist_norm
+    apply (rule *)
+    apply (simp add: scaleR_right_diff_distrib)
+    apply (simp add: scaleR_2)
+    done
+  show ?t4
+    unfolding midpoint_def dist_norm
+    apply (rule **)
+    apply (simp add: scaleR_right_diff_distrib)
+    apply (simp add: scaleR_2)
+    done
+qed
+
+lemma midpoint_eq_endpoint [simp]:
+  "midpoint a b = a \<longleftrightarrow> a = b"
+  "midpoint a b = b \<longleftrightarrow> a = b"
+  unfolding midpoint_eq_iff by auto
+
+lemma midpoint_plus_self [simp]: "midpoint a b + midpoint a b = a + b"
+  using midpoint_eq_iff by metis
+
+lemma midpoint_linear_image:
+   "linear f \<Longrightarrow> midpoint(f a)(f b) = f(midpoint a b)"
+by (simp add: linear_iff midpoint_def)
+
+
+subsection \<open>Line segments\<close>
+
 definition closed_segment :: "'a::real_vector \<Rightarrow> 'a \<Rightarrow> 'a set"
   where "closed_segment a b = {(1 - u) *\<^sub>R a + u *\<^sub>R b | u::real. 0 \<le> u \<and> u \<le> 1}"
 
@@ -106,86 +184,6 @@
   apply (auto simp: in_segment scaleR_conv_of_real elim!: ex_forward del: exE)
   using of_real_eq_iff by fastforce
 
-lemma midpoint_idem [simp]: "midpoint x x = x"
-  unfolding midpoint_def
-  unfolding scaleR_right_distrib
-  unfolding scaleR_left_distrib[symmetric]
-  by auto
-
-lemma midpoint_sym: "midpoint a b = midpoint b a"
-  unfolding midpoint_def by (auto simp add: scaleR_right_distrib)
-
-lemma midpoint_eq_iff: "midpoint a b = c \<longleftrightarrow> a + b = c + c"
-proof -
-  have "midpoint a b = c \<longleftrightarrow> scaleR 2 (midpoint a b) = scaleR 2 c"
-    by simp
-  then show ?thesis
-    unfolding midpoint_def scaleR_2 [symmetric] by simp
-qed
-
-lemma
-  fixes a::real
-  assumes "a \<le> b" shows ge_midpoint_1: "a \<le> midpoint a b"
-                    and le_midpoint_1: "midpoint a b \<le> b"
-  by (simp_all add: midpoint_def assms)
-
-lemma dist_midpoint:
-  fixes a b :: "'a::real_normed_vector" shows
-  "dist a (midpoint a b) = (dist a b) / 2" (is ?t1)
-  "dist b (midpoint a b) = (dist a b) / 2" (is ?t2)
-  "dist (midpoint a b) a = (dist a b) / 2" (is ?t3)
-  "dist (midpoint a b) b = (dist a b) / 2" (is ?t4)
-proof -
-  have *: "\<And>x y::'a. 2 *\<^sub>R x = - y \<Longrightarrow> norm x = (norm y) / 2"
-    unfolding equation_minus_iff by auto
-  have **: "\<And>x y::'a. 2 *\<^sub>R x =   y \<Longrightarrow> norm x = (norm y) / 2"
-    by auto
-  note scaleR_right_distrib [simp]
-  show ?t1
-    unfolding midpoint_def dist_norm
-    apply (rule **)
-    apply (simp add: scaleR_right_diff_distrib)
-    apply (simp add: scaleR_2)
-    done
-  show ?t2
-    unfolding midpoint_def dist_norm
-    apply (rule *)
-    apply (simp add: scaleR_right_diff_distrib)
-    apply (simp add: scaleR_2)
-    done
-  show ?t3
-    unfolding midpoint_def dist_norm
-    apply (rule *)
-    apply (simp add: scaleR_right_diff_distrib)
-    apply (simp add: scaleR_2)
-    done
-  show ?t4
-    unfolding midpoint_def dist_norm
-    apply (rule **)
-    apply (simp add: scaleR_right_diff_distrib)
-    apply (simp add: scaleR_2)
-    done
-qed
-
-lemma midpoint_eq_endpoint [simp]:
-  "midpoint a b = a \<longleftrightarrow> a = b"
-  "midpoint a b = b \<longleftrightarrow> a = b"
-  unfolding midpoint_eq_iff by auto
-
-lemma midpoint_plus_self [simp]: "midpoint a b + midpoint a b = a + b"
-  using midpoint_eq_iff by metis
-
-lemma midpoint_linear_image:
-   "linear f \<Longrightarrow> midpoint(f a)(f b) = f(midpoint a b)"
-by (simp add: linear_iff midpoint_def)
-
-subsection\<open>Starlike sets\<close>
-
-definition "starlike S \<longleftrightarrow> (\<exists>a\<in>S. \<forall>x\<in>S. closed_segment a x \<subseteq> S)"
-
-lemma starlike_UNIV [simp]: "starlike UNIV"
-  by (simp add: starlike_def)
-
 lemma convex_contains_segment:
   "convex S \<longleftrightarrow> (\<forall>a\<in>S. \<forall>b\<in>S. closed_segment a b \<subseteq> S)"
   unfolding convex_alt closed_segment_def by auto
@@ -197,10 +195,6 @@
     "\<lbrakk>x \<in> convex hull S; y \<in> convex hull S\<rbrakk> \<Longrightarrow> closed_segment x y \<subseteq> convex hull S"
   using convex_contains_segment by blast
 
-lemma convex_imp_starlike:
-  "convex S \<Longrightarrow> S \<noteq> {} \<Longrightarrow> starlike S"
-  unfolding convex_contains_segment starlike_def by auto
-
 lemma segment_convex_hull:
   "closed_segment a b = convex hull {a,b}"
 proof -
@@ -349,7 +343,7 @@
   proof -
     have "norm ((1 - 1 * u) *\<^sub>R (a - b)) = (1 - 1 * u) * norm (a - b)"
       using \<open>u \<le> 1\<close> by force
-    then show ?thesis                     
+    then show ?thesis
       by (simp add: dist_norm real_vector.scale_right_diff_distrib)
   qed
   also have "... \<le> dist a b"
@@ -581,7 +575,6 @@
     by (metis image_comp convex_translation)
 qed
 
-
 lemmas convex_segment = convex_closed_segment convex_open_segment
 
 lemma connected_segment [iff]:
@@ -589,6 +582,33 @@
   shows "connected (closed_segment x y)"
   by (simp add: convex_connected)
 
+lemma is_interval_closed_segment_1[intro, simp]: "is_interval (closed_segment a b)" for a b::real
+  by (auto simp: is_interval_convex_1)
+
+lemma IVT'_closed_segment_real:
+  fixes f :: "real \<Rightarrow> real"
+  assumes "y \<in> closed_segment (f a) (f b)"
+  assumes "continuous_on (closed_segment a b) f"
+  shows "\<exists>x \<in> closed_segment a b. f x = y"
+  using IVT'[of f a y b]
+    IVT'[of "-f" a "-y" b]
+    IVT'[of f b y a]
+    IVT'[of "-f" b "-y" a] assms
+  by (cases "a \<le> b"; cases "f b \<ge> f a") (auto simp: closed_segment_eq_real_ivl continuous_on_minus)
+
+
+subsection\<open>Starlike sets\<close>
+
+definition "starlike S \<longleftrightarrow> (\<exists>a\<in>S. \<forall>x\<in>S. closed_segment a x \<subseteq> S)"
+
+lemma starlike_UNIV [simp]: "starlike UNIV"
+  by (simp add: starlike_def)
+
+lemma convex_imp_starlike:
+  "convex S \<Longrightarrow> S \<noteq> {} \<Longrightarrow> starlike S"
+  unfolding convex_contains_segment starlike_def by auto
+
+
 lemma affine_hull_closed_segment [simp]:
      "affine hull (closed_segment a b) = affine hull {a,b}"
   by (simp add: segment_convex_hull)
@@ -7261,6 +7281,66 @@
   with assms show ?thesis by auto
 qed
 
+lemma vector_in_orthogonal_spanningset:
+  fixes a :: "'a::euclidean_space"
+  obtains S where "a \<in> S" "pairwise orthogonal S" "span S = UNIV"
+  by (metis UNIV_I Un_iff empty_iff insert_subset orthogonal_extension pairwise_def pairwise_orthogonal_insert span_UNIV subsetI subset_antisym)
+
+lemma vector_in_orthogonal_basis:
+  fixes a :: "'a::euclidean_space"
+  assumes "a \<noteq> 0"
+  obtains S where "a \<in> S" "0 \<notin> S" "pairwise orthogonal S" "independent S" "finite S"
+                  "span S = UNIV" "card S = DIM('a)"
+proof -
+  obtain S where S: "a \<in> S" "pairwise orthogonal S" "span S = UNIV"
+    using vector_in_orthogonal_spanningset .
+  show thesis
+  proof
+    show "pairwise orthogonal (S - {0})"
+      using pairwise_mono S(2) by blast
+    show "independent (S - {0})"
+      by (simp add: \<open>pairwise orthogonal (S - {0})\<close> pairwise_orthogonal_independent)
+    show "finite (S - {0})"
+      using \<open>independent (S - {0})\<close> independent_finite by blast
+    show "card (S - {0}) = DIM('a)"
+      using span_delete_0 [of S] S
+      by (simp add: \<open>independent (S - {0})\<close> indep_card_eq_dim_span)
+  qed (use S \<open>a \<noteq> 0\<close> in auto)
+qed
+
+lemma vector_in_orthonormal_basis:
+  fixes a :: "'a::euclidean_space"
+  assumes "norm a = 1"
+  obtains S where "a \<in> S" "pairwise orthogonal S" "\<And>x. x \<in> S \<Longrightarrow> norm x = 1"
+    "independent S" "card S = DIM('a)" "span S = UNIV"
+proof -
+  have "a \<noteq> 0"
+    using assms by auto
+  then obtain S where "a \<in> S" "0 \<notin> S" "finite S"
+          and S: "pairwise orthogonal S" "independent S" "span S = UNIV" "card S = DIM('a)"
+    by (metis vector_in_orthogonal_basis)
+  let ?S = "(\<lambda>x. x /\<^sub>R norm x) ` S"
+  show thesis
+  proof
+    show "a \<in> ?S"
+      using \<open>a \<in> S\<close> assms image_iff by fastforce
+  next
+    show "pairwise orthogonal ?S"
+      using \<open>pairwise orthogonal S\<close> by (auto simp: pairwise_def orthogonal_def)
+    show "\<And>x. x \<in> (\<lambda>x. x /\<^sub>R norm x) ` S \<Longrightarrow> norm x = 1"
+      using \<open>0 \<notin> S\<close> by (auto simp: divide_simps)
+    then show "independent ?S"
+      by (metis \<open>pairwise orthogonal ((\<lambda>x. x /\<^sub>R norm x) ` S)\<close> norm_zero pairwise_orthogonal_independent zero_neq_one)
+    have "inj_on (\<lambda>x. x /\<^sub>R norm x) S"
+      unfolding inj_on_def
+      by (metis (full_types) S(1) \<open>0 \<notin> S\<close> inverse_nonzero_iff_nonzero norm_eq_zero orthogonal_scaleR orthogonal_self pairwise_def)
+    then show "card ?S = DIM('a)"
+      by (simp add: card_image S)
+    show "span ?S = UNIV"
+      by (metis (no_types) \<open>0 \<notin> S\<close> \<open>finite S\<close> \<open>span S = UNIV\<close> field_class.field_inverse_zero inverse_inverse_eq less_irrefl span_image_scale zero_less_norm_iff)
+  qed
+qed
+
 proposition dim_orthogonal_sum:
   fixes A :: "'a::euclidean_space set"
   assumes "\<And>x y. \<lbrakk>x \<in> A; y \<in> B\<rbrakk> \<Longrightarrow> x \<bullet> y = 0"
--- a/src/HOL/Analysis/Topology_Euclidean_Space.thy	Fri Feb 23 15:07:30 2018 +0100
+++ b/src/HOL/Analysis/Topology_Euclidean_Space.thy	Fri Feb 23 15:17:51 2018 +0100
@@ -7,7 +7,7 @@
 section \<open>Elementary topology in Euclidean space.\<close>
 
 theory Topology_Euclidean_Space
-imports                                                         
+imports
   "HOL-Library.Indicator_Function"
   "HOL-Library.Countable_Set"
   "HOL-Library.FuncSet"
@@ -1112,6 +1112,9 @@
 lemma ball_subset_cball [simp, intro]: "ball x e \<subseteq> cball x e"
   by (simp add: subset_eq)
 
+lemma mem_ball_imp_mem_cball: "x \<in> ball y e \<Longrightarrow> x \<in> cball y e"
+  by (auto simp: mem_ball mem_cball)
+
 lemma sphere_cball [simp,intro]: "sphere z r \<subseteq> cball z r"
   by force
 
@@ -1124,6 +1127,22 @@
 lemma subset_cball[intro]: "d \<le> e \<Longrightarrow> cball x d \<subseteq> cball x e"
   by (simp add: subset_eq)
 
+lemma mem_ball_leI: "x \<in> ball y e \<Longrightarrow> e \<le> f \<Longrightarrow> x \<in> ball y f"
+  by (auto simp: mem_ball mem_cball)
+
+lemma mem_cball_leI: "x \<in> cball y e \<Longrightarrow> e \<le> f \<Longrightarrow> x \<in> cball y f"
+  by (auto simp: mem_ball mem_cball)
+
+lemma cball_trans: "y \<in> cball z b \<Longrightarrow> x \<in> cball y a \<Longrightarrow> x \<in> cball z (b + a)"
+  unfolding mem_cball
+proof -
+  have "dist z x \<le> dist z y + dist y x"
+    by (rule dist_triangle)
+  also assume "dist z y \<le> b"
+  also assume "dist y x \<le> a"
+  finally show "dist z x \<le> b + a" by arith
+qed
+
 lemma ball_max_Un: "ball a (max r s) = ball a r \<union> ball a s"
   by (simp add: set_eq_iff) arith
 
@@ -1253,6 +1272,17 @@
   unfolding dist_norm norm_eq_sqrt_inner L2_set_def
   by (subst euclidean_inner) (simp add: power2_eq_square inner_diff_left)
 
+lemma norm_nth_le: "norm (x \<bullet> i) \<le> norm x" if "i \<in> Basis"
+proof -
+  have "(x \<bullet> i)\<^sup>2 = (\<Sum>i\<in>{i}. (x \<bullet> i)\<^sup>2)"
+    by simp
+  also have "\<dots> \<le> (\<Sum>i\<in>Basis. (x \<bullet> i)\<^sup>2)"
+    by (intro sum_mono2) (auto simp: that)
+  finally show ?thesis
+    unfolding norm_conv_dist euclidean_dist_l2[of x] L2_set_def
+    by (auto intro!: real_le_rsqrt)
+qed
+
 lemma eventually_nhds_ball: "d > 0 \<Longrightarrow> eventually (\<lambda>x. x \<in> ball z d) (nhds z)"
   by (rule eventually_nhds_in_open) simp_all
 
@@ -1262,6 +1292,20 @@
 lemma eventually_at_ball': "d > 0 \<Longrightarrow> eventually (\<lambda>t. t \<in> ball z d \<and> t \<noteq> z \<and> t \<in> A) (at z within A)"
   unfolding eventually_at by (intro exI[of _ d]) (simp_all add: dist_commute)
 
+lemma at_within_ball: "e > 0 \<Longrightarrow> dist x y < e \<Longrightarrow> at y within ball x e = at y"
+  by (subst at_within_open) auto
+
+lemma atLeastAtMost_eq_cball:
+  fixes a b::real
+  shows "{a .. b} = cball ((a + b)/2) ((b - a)/2)"
+  by (auto simp: dist_real_def field_simps mem_cball)
+
+lemma greaterThanLessThan_eq_ball:
+  fixes a b::real
+  shows "{a <..< b} = ball ((a + b)/2) ((b - a)/2)"
+  by (auto simp: dist_real_def field_simps mem_ball)
+
+
 subsection \<open>Boxes\<close>
 
 abbreviation One :: "'a::euclidean_space"
@@ -1834,6 +1878,14 @@
 definition "is_interval (s::('a::euclidean_space) set) \<longleftrightarrow>
   (\<forall>a\<in>s. \<forall>b\<in>s. \<forall>x. (\<forall>i\<in>Basis. ((a\<bullet>i \<le> x\<bullet>i \<and> x\<bullet>i \<le> b\<bullet>i) \<or> (b\<bullet>i \<le> x\<bullet>i \<and> x\<bullet>i \<le> a\<bullet>i))) \<longrightarrow> x \<in> s)"
 
+lemma is_interval_1:
+  "is_interval (s::real set) \<longleftrightarrow> (\<forall>a\<in>s. \<forall>b\<in>s. \<forall> x. a \<le> x \<and> x \<le> b \<longrightarrow> x \<in> s)"
+  unfolding is_interval_def by auto
+
+lemma is_interval_inter: "is_interval X \<Longrightarrow> is_interval Y \<Longrightarrow> is_interval (X \<inter> Y)"
+  unfolding is_interval_def
+  by blast
+
 lemma is_interval_cbox [simp]: "is_interval (cbox a (b::'a::euclidean_space))" (is ?th1)
   and is_interval_box [simp]: "is_interval (box a b)" (is ?th2)
   unfolding is_interval_def mem_box Ball_def atLeastAtMost_iff
@@ -1916,6 +1968,88 @@
     by blast
 qed
 
+lemma is_real_interval_union:
+  "is_interval (X \<union> Y)"
+  if X: "is_interval X" and Y: "is_interval Y" and I: "(X \<noteq> {} \<Longrightarrow> Y \<noteq> {} \<Longrightarrow> X \<inter> Y \<noteq> {})"
+  for X Y::"real set"
+proof -
+  consider "X \<noteq> {}" "Y \<noteq> {}" | "X = {}" | "Y = {}" by blast
+  then show ?thesis
+  proof cases
+    case 1
+    then obtain r where "r \<in> X \<or> X \<inter> Y = {}" "r \<in> Y \<or> X \<inter> Y = {}"
+      by blast
+    then show ?thesis
+      using I 1 X Y unfolding is_interval_1
+      by (metis (full_types) Un_iff le_cases)
+  qed (use that in auto)
+qed
+
+lemma is_interval_translationI:
+  assumes "is_interval X"
+  shows "is_interval ((+) x ` X)"
+  unfolding is_interval_def
+proof safe
+  fix b d e
+  assume "b \<in> X" "d \<in> X"
+    "\<forall>i\<in>Basis. (x + b) \<bullet> i \<le> e \<bullet> i \<and> e \<bullet> i \<le> (x + d) \<bullet> i \<or>
+       (x + d) \<bullet> i \<le> e \<bullet> i \<and> e \<bullet> i \<le> (x + b) \<bullet> i"
+  hence "e - x \<in> X"
+    by (intro mem_is_intervalI[OF assms \<open>b \<in> X\<close> \<open>d \<in> X\<close>, of "e - x"])
+      (auto simp: algebra_simps)
+  thus "e \<in> (+) x ` X" by force
+qed
+
+lemma is_interval_uminusI:
+  assumes "is_interval X"
+  shows "is_interval (uminus ` X)"
+  unfolding is_interval_def
+proof safe
+  fix b d e
+  assume "b \<in> X" "d \<in> X"
+    "\<forall>i\<in>Basis. (- b) \<bullet> i \<le> e \<bullet> i \<and> e \<bullet> i \<le> (- d) \<bullet> i \<or>
+       (- d) \<bullet> i \<le> e \<bullet> i \<and> e \<bullet> i \<le> (- b) \<bullet> i"
+  hence "- e \<in> X"
+    by (intro mem_is_intervalI[OF assms \<open>b \<in> X\<close> \<open>d \<in> X\<close>, of "- e"])
+      (auto simp: algebra_simps)
+  thus "e \<in> uminus ` X" by force
+qed
+
+lemma is_interval_uminus[simp]: "is_interval (uminus ` x) = is_interval x"
+  using is_interval_uminusI[of x] is_interval_uminusI[of "uminus ` x"]
+  by (auto simp: image_image)
+
+lemma is_interval_neg_translationI:
+  assumes "is_interval X"
+  shows "is_interval ((-) x ` X)"
+proof -
+  have "(-) x ` X = (+) x ` uminus ` X"
+    by (force simp: algebra_simps)
+  also have "is_interval \<dots>"
+    by (metis is_interval_uminusI is_interval_translationI assms)
+  finally show ?thesis .
+qed
+
+lemma is_interval_translation[simp]:
+  "is_interval ((+) x ` X) = is_interval X"
+  using is_interval_neg_translationI[of "(+) x ` X" x]
+  by (auto intro!: is_interval_translationI simp: image_image)
+
+lemma is_interval_minus_translation[simp]:
+  shows "is_interval ((-) x ` X) = is_interval X"
+proof -
+  have "(-) x ` X = (+) x ` uminus ` X"
+    by (force simp: algebra_simps)
+  also have "is_interval \<dots> = is_interval X"
+    by simp
+  finally show ?thesis .
+qed
+
+lemma is_interval_minus_translation'[simp]:
+  shows "is_interval ((\<lambda>x. x - c) ` X) = is_interval X"
+  using is_interval_translation[of "-c" X]
+  by (metis image_cong uminus_add_conv_diff)
+
 
 subsection \<open>Limit points\<close>
 
@@ -2629,6 +2763,15 @@
 lemma not_trivial_limit_within: "\<not> trivial_limit (at x within S) = (x \<in> closure (S - {x}))"
   using islimpt_in_closure by (metis trivial_limit_within)
 
+lemma not_in_closure_trivial_limitI:
+  "x \<notin> closure s \<Longrightarrow> trivial_limit (at x within s)"
+  using not_trivial_limit_within[of x s]
+  by safe (metis Diff_empty Diff_insert0 closure_subset contra_subsetD)
+
+lemma filterlim_at_within_closure_implies_filterlim: "filterlim f l (at x within s)"
+  if "x \<in> closure s \<Longrightarrow> filterlim f l (at x within s)"
+  by (metis bot.extremum filterlim_filtercomap filterlim_mono not_in_closure_trivial_limitI that)
+
 lemma at_within_eq_bot_iff: "at c within A = bot \<longleftrightarrow> c \<notin> closure (A - {c})"
   using not_trivial_limit_within[of c A] by blast
 
@@ -3229,6 +3372,28 @@
   qed
 qed
 
+lemma tendsto_If_within_closures:
+  assumes f: "x \<in> s \<union> (closure s \<inter> closure t) \<Longrightarrow>
+      (f \<longlongrightarrow> l x) (at x within s \<union> (closure s \<inter> closure t))"
+  assumes g: "x \<in> t \<union> (closure s \<inter> closure t) \<Longrightarrow>
+      (g \<longlongrightarrow> l x) (at x within t \<union> (closure s \<inter> closure t))"
+  assumes "x \<in> s \<union> t"
+  shows "((\<lambda>x. if x \<in> s then f x else g x) \<longlongrightarrow> l x) (at x within s \<union> t)"
+proof -
+  have *: "(s \<union> t) \<inter> {x. x \<in> s} = s" "(s \<union> t) \<inter> {x. x \<notin> s} = t - s"
+    by auto
+  have "(f \<longlongrightarrow> l x) (at x within s)"
+    by (rule filterlim_at_within_closure_implies_filterlim)
+       (use \<open>x \<in> _\<close> in \<open>auto simp: inf_commute closure_def intro: tendsto_within_subset[OF f]\<close>)
+  moreover
+  have "(g \<longlongrightarrow> l x) (at x within t - s)"
+    by (rule filterlim_at_within_closure_implies_filterlim)
+      (use \<open>x \<in> _\<close> in
+        \<open>auto intro!: tendsto_within_subset[OF g] simp: closure_def intro: islimpt_subset\<close>)
+  ultimately show ?thesis
+    by (intro filterlim_at_within_If) (simp_all only: *)
+qed
+
 
 subsection \<open>Boundedness\<close>
 
@@ -3487,12 +3652,26 @@
     using assms by (fastforce simp: bounded_iff)
 qed
 
+lemma bounded_plus:
+  fixes S ::"'a::real_normed_vector set"
+  assumes "bounded S" "bounded T"
+  shows "bounded ((\<lambda>(x,y). x + y) ` (S \<times> T))"
+  using bounded_plus_comp [of fst "S \<times> T" snd] assms
+  by (auto simp: split_def split: if_split_asm)
+
 lemma bounded_minus_comp:
   "bounded (f ` S) \<Longrightarrow> bounded (g ` S) \<Longrightarrow> bounded ((\<lambda>x. f x - g x) ` S)"
   for f g::"'a \<Rightarrow> 'b::real_normed_vector"
   using bounded_plus_comp[of "f" S "\<lambda>x. - g x"]
   by auto
 
+lemma bounded_minus:
+  fixes S ::"'a::real_normed_vector set"
+  assumes "bounded S" "bounded T"
+  shows "bounded ((\<lambda>(x,y). x - y) ` (S \<times> T))"
+  using bounded_minus_comp [of fst "S \<times> T" snd] assms
+  by (auto simp: split_def split: if_split_asm)
+
 
 subsection \<open>Compactness\<close>
 
@@ -3849,7 +4028,6 @@
          \<Longrightarrow> openin (subtopology euclidean u) (s - {a})"
 by (metis Int_Diff open_delete openin_open)
 
-
 text\<open>Compactness expressed with filters\<close>
 
 lemma closure_iff_nhds_not_empty:
@@ -4478,6 +4656,27 @@
   shows "~ compact (UNIV::'a set)"
     by (simp add: compact_eq_bounded_closed)
 
+text\<open>Representing sets as the union of a chain of compact sets.\<close>
+lemma closed_Union_compact_subsets:
+  fixes S :: "'a::{heine_borel,real_normed_vector} set"
+  assumes "closed S"
+  obtains F where "\<And>n. compact(F n)" "\<And>n. F n \<subseteq> S" "\<And>n. F n \<subseteq> F(Suc n)"
+                  "(\<Union>n. F n) = S" "\<And>K. \<lbrakk>compact K; K \<subseteq> S\<rbrakk> \<Longrightarrow> \<exists>N. \<forall>n \<ge> N. K \<subseteq> F n"
+proof
+  show "compact (S \<inter> cball 0 (of_nat n))" for n
+    using assms compact_eq_bounded_closed by auto
+next
+  show "(\<Union>n. S \<inter> cball 0 (real n)) = S"
+    by (auto simp: real_arch_simple)
+next
+  fix K :: "'a set"
+  assume "compact K" "K \<subseteq> S"
+  then obtain N where "K \<subseteq> cball 0 N"
+    by (meson bounded_pos mem_cball_0 compact_imp_bounded subsetI)
+  then show "\<exists>N. \<forall>n\<ge>N. K \<subseteq> S \<inter> cball 0 (real n)"
+    by (metis of_nat_le_iff Int_subset_iff \<open>K \<subseteq> S\<close> real_arch_simple subset_cball subset_trans)
+qed auto
+
 instance real :: heine_borel
 proof
   fix f :: "nat \<Rightarrow> real"
@@ -4897,10 +5096,7 @@
 
 lemma continuous_within_eps_delta:
   "continuous (at x within s) f \<longleftrightarrow> (\<forall>e>0. \<exists>d>0. \<forall>x'\<in> s.  dist x' x < d --> dist (f x') (f x) < e)"
-  unfolding continuous_within and Lim_within
-  apply auto
-  apply (metis dist_nz dist_self, blast)
-  done
+  unfolding continuous_within and Lim_within  by fastforce
 
 corollary continuous_at_eps_delta:
   "continuous (at x) f \<longleftrightarrow> (\<forall>e > 0. \<exists>d > 0. \<forall>x'. dist x' x < d \<longrightarrow> dist (f x') (f x) < e)"
--- a/src/HOL/Analysis/Uniform_Limit.thy	Fri Feb 23 15:07:30 2018 +0100
+++ b/src/HOL/Analysis/Uniform_Limit.thy	Fri Feb 23 15:17:51 2018 +0100
@@ -438,6 +438,7 @@
   bounded_linear.uniform_limit[OF bounded_linear_mult_right]
   bounded_linear.uniform_limit[OF bounded_linear_scaleR_left]
 
+
 lemmas uniform_limit_uminus[uniform_limit_intros] =
   bounded_linear.uniform_limit[OF bounded_linear_minus[OF bounded_linear_ident]]
 
@@ -728,5 +729,7 @@
 apply (rule continuous_on_cong [THEN iffD1, OF refl _ powser_continuous_suminf [OF r]])
 using sm sums_unique by fastforce
 
+lemmas uniform_limit_subset_union = uniform_limit_on_subset[OF uniform_limit_on_Union]
+
 end
 
--- a/src/HOL/Deriv.thy	Fri Feb 23 15:07:30 2018 +0100
+++ b/src/HOL/Deriv.thy	Fri Feb 23 15:17:51 2018 +0100
@@ -26,6 +26,13 @@
   most cases @{term s} is either a variable or @{term UNIV}.
 \<close>
 
+text \<open>These are the only cases we'll care about, probably.\<close>
+
+lemma has_derivative_within: "(f has_derivative f') (at x within s) \<longleftrightarrow>
+    bounded_linear f' \<and> ((\<lambda>y. (1 / norm(y - x)) *\<^sub>R (f y - (f x + f' (y - x)))) \<longlongrightarrow> 0) (at x within s)"
+  unfolding has_derivative_def tendsto_iff
+  by (subst eventually_Lim_ident_at) (auto simp add: field_simps)
+
 lemma has_derivative_eq_rhs: "(f has_derivative f') F \<Longrightarrow> f' = g' \<Longrightarrow> (f has_derivative g') F"
   by simp
 
@@ -189,6 +196,52 @@
 
 lemmas has_derivative_within_subset = has_derivative_subset
 
+lemma has_derivative_within_singleton_iff:
+  "(f has_derivative g) (at x within {x}) \<longleftrightarrow> bounded_linear g"
+  by (auto intro!: has_derivativeI_sandwich[where e=1] has_derivative_bounded_linear)
+
+
+subsubsection \<open>Limit transformation for derivatives\<close>
+
+lemma has_derivative_transform_within:
+  assumes "(f has_derivative f') (at x within s)"
+    and "0 < d"
+    and "x \<in> s"
+    and "\<And>x'. \<lbrakk>x' \<in> s; dist x' x < d\<rbrakk> \<Longrightarrow> f x' = g x'"
+  shows "(g has_derivative f') (at x within s)"
+  using assms
+  unfolding has_derivative_within
+  by (force simp add: intro: Lim_transform_within)
+
+lemma has_derivative_transform_within_open:
+  assumes "(f has_derivative f') (at x within t)"
+    and "open s"
+    and "x \<in> s"
+    and "\<And>x. x\<in>s \<Longrightarrow> f x = g x"
+  shows "(g has_derivative f') (at x within t)"
+  using assms unfolding has_derivative_within
+  by (force simp add: intro: Lim_transform_within_open)
+
+lemma has_derivative_transform:
+  assumes "x \<in> s" "\<And>x. x \<in> s \<Longrightarrow> g x = f x"
+  assumes "(f has_derivative f') (at x within s)"
+  shows "(g has_derivative f') (at x within s)"
+  using assms
+  by (intro has_derivative_transform_within[OF _ zero_less_one, where g=g]) auto
+
+lemma has_derivative_transform_eventually:
+  assumes "(f has_derivative f') (at x within s)"
+    "(\<forall>\<^sub>F x' in at x within s. f x' = g x')"
+  assumes "f x = g x" "x \<in> s"
+  shows "(g has_derivative f') (at x within s)"
+  using assms
+proof -
+  from assms(2,3) obtain d where "d > 0" "\<And>x'. x' \<in> s \<Longrightarrow> dist x' x < d \<Longrightarrow> f x' = g x'"
+    by (force simp: eventually_at)
+  from has_derivative_transform_within[OF assms(1) this(1) assms(4) this(2)]
+  show ?thesis .
+qed
+
 
 subsection \<open>Continuity\<close>
 
@@ -295,6 +348,14 @@
   ((\<lambda>x. g (f x)) has_derivative (\<lambda>x. g' (f' x))) (at x within s)"
   by (blast intro: has_derivative_in_compose has_derivative_subset)
 
+lemma has_derivative_in_compose2:
+  assumes "\<And>x. x \<in> t \<Longrightarrow> (g has_derivative g' x) (at x within t)"
+  assumes "f ` s \<subseteq> t" "x \<in> s"
+  assumes "(f has_derivative f') (at x within s)"
+  shows "((\<lambda>x. g (f x)) has_derivative (\<lambda>y. g' (f x) (f' y))) (at x within s)"
+  using assms
+  by (auto intro: has_derivative_within_subset intro!: has_derivative_in_compose[of f f' x s g])
+
 lemma (in bounded_bilinear) FDERIV:
   assumes f: "(f has_derivative f') (at x within s)" and g: "(g has_derivative g') (at x within s)"
   shows "((\<lambda>x. f x ** g x) has_derivative (\<lambda>h. f x ** g' h + f' h ** g x)) (at x within s)"
@@ -467,6 +528,10 @@
 all directions. There is a proof in \<open>Analysis\<close> for \<open>euclidean_space\<close>.
 \<close>
 
+lemma has_derivative_at2: "(f has_derivative f') (at x) \<longleftrightarrow>
+    bounded_linear f' \<and> ((\<lambda>y. (1 / (norm(y - x))) *\<^sub>R (f y - (f x + f' (y - x)))) \<longlongrightarrow> 0) (at x)"
+  using has_derivative_within [of f f' x UNIV]
+  by simp
 lemma has_derivative_zero_unique:
   assumes "((\<lambda>x. 0) has_derivative F) (at x)"
   shows "F = (\<lambda>h. 0)"
@@ -542,10 +607,19 @@
     (\<lambda>x. f (g x)) differentiable (at x within s)"
   by (blast intro: differentiable_in_compose differentiable_subset)
 
-lemma differentiable_sum [simp, derivative_intros]:
+lemma differentiable_add [simp, derivative_intros]:
   "f differentiable F \<Longrightarrow> g differentiable F \<Longrightarrow> (\<lambda>x. f x + g x) differentiable F"
   unfolding differentiable_def by (blast intro: has_derivative_add)
 
+lemma differentiable_sum[simp, derivative_intros]:
+  assumes "finite s" "\<forall>a\<in>s. (f a) differentiable net"
+  shows "(\<lambda>x. sum (\<lambda>a. f a x) s) differentiable net"
+proof -
+  from bchoice[OF assms(2)[unfolded differentiable_def]]
+  show ?thesis
+    by (auto intro!: has_derivative_sum simp: differentiable_def)
+qed
+
 lemma differentiable_minus [simp, derivative_intros]:
   "f differentiable F \<Longrightarrow> (\<lambda>x. - f x) differentiable F"
   unfolding differentiable_def by (blast intro: has_derivative_minus)
@@ -651,6 +725,14 @@
   for c :: "'a::ab_semigroup_mult"
   by (simp add: fun_eq_iff mult.commute)
 
+lemma DERIV_compose_FDERIV:
+  fixes f::"real\<Rightarrow>real"
+  assumes "DERIV f (g x) :> f'"
+  assumes "(g has_derivative g') (at x within s)"
+  shows "((\<lambda>x. f (g x)) has_derivative (\<lambda>x. g' x * f')) (at x within s)"
+  using assms has_derivative_compose[of g g' x s f "( * ) f'"]
+  by (auto simp: has_field_derivative_def ac_simps)
+
 
 subsection \<open>Vector derivative\<close>
 
@@ -998,6 +1080,8 @@
     by eventually_elim auto
 qed
 
+lemmas has_derivative_floor[derivative_intros] =
+  floor_has_real_derivative[THEN DERIV_compose_FDERIV]
 
 text \<open>Caratheodory formulation of derivative at a point\<close>
 
--- a/src/HOL/Groups_Big.thy	Fri Feb 23 15:07:30 2018 +0100
+++ b/src/HOL/Groups_Big.thy	Fri Feb 23 15:17:51 2018 +0100
@@ -332,34 +332,6 @@
     by (intro reindex_bij_betw_not_neutral[OF _ _ bij]) auto
 qed
 
-lemma delta [simp]:
-  assumes fS: "finite S"
-  shows "F (\<lambda>k. if k = a then b k else \<^bold>1) S = (if a \<in> S then b a else \<^bold>1)"
-proof -
-  let ?f = "(\<lambda>k. if k = a then b k else \<^bold>1)"
-  show ?thesis
-  proof (cases "a \<in> S")
-    case False
-    then have "\<forall>k\<in>S. ?f k = \<^bold>1" by simp
-    with False show ?thesis by simp
-  next
-    case True
-    let ?A = "S - {a}"
-    let ?B = "{a}"
-    from True have eq: "S = ?A \<union> ?B" by blast
-    have dj: "?A \<inter> ?B = {}" by simp
-    from fS have fAB: "finite ?A" "finite ?B" by auto
-    have "F ?f S = F ?f ?A \<^bold>* F ?f ?B"
-      using union_disjoint [OF fAB dj, of ?f, unfolded eq [symmetric]] by simp
-    with True show ?thesis by simp
-  qed
-qed
-
-lemma delta' [simp]:
-  assumes fin: "finite S"
-  shows "F (\<lambda>k. if a = k then b k else \<^bold>1) S = (if a \<in> S then b a else \<^bold>1)"
-  using delta [OF fin, of a b, symmetric] by (auto intro: cong)
-
 lemma delta_remove:
   assumes fS: "finite S"
   shows "F (\<lambda>k. if k = a then b k else c k) S = (if a \<in> S then b a \<^bold>* F c (S-{a}) else F c (S-{a}))"
@@ -384,6 +356,16 @@
   qed
 qed
 
+lemma delta [simp]:
+  assumes fS: "finite S"
+  shows "F (\<lambda>k. if k = a then b k else \<^bold>1) S = (if a \<in> S then b a else \<^bold>1)"
+  by (simp add: delta_remove [OF assms])
+
+lemma delta' [simp]:
+  assumes fin: "finite S"
+  shows "F (\<lambda>k. if a = k then b k else \<^bold>1) S = (if a \<in> S then b a else \<^bold>1)"
+  using delta [OF fin, of a b, symmetric] by (auto intro: cong)
+
 lemma If_cases:
   fixes P :: "'b \<Rightarrow> bool" and g h :: "'b \<Rightarrow> 'a"
   assumes fin: "finite A"
--- a/src/HOL/Library/Extended_Nat.thy	Fri Feb 23 15:07:30 2018 +0100
+++ b/src/HOL/Library/Extended_Nat.thy	Fri Feb 23 15:17:51 2018 +0100
@@ -383,6 +383,8 @@
     by (simp split: enat.splits)
   show "a < b \<Longrightarrow> c < d \<Longrightarrow> a + c < b + d" for a b c d :: enat
     by (cases a b c d rule: enat2_cases[case_product enat2_cases]) auto
+  show "a < b \<Longrightarrow> a + 1 < b + 1"
+    by (metis add_right_mono eSuc_minus_1 eSuc_plus_1 less_le)
 qed (simp add: zero_enat_def one_enat_def)
 
 (* BH: These equations are already proven generally for any type in
--- a/src/HOL/Library/Extended_Nonnegative_Real.thy	Fri Feb 23 15:07:30 2018 +0100
+++ b/src/HOL/Library/Extended_Nonnegative_Real.thy	Fri Feb 23 15:17:51 2018 +0100
@@ -11,7 +11,7 @@
 lemma ereal_ineq_diff_add:
   assumes "b \<noteq> (-\<infinity>::ereal)" "a \<ge> b"
   shows "a = b + (a-b)"
-by (metis add.commute assms(1) assms(2) ereal_eq_minus_iff ereal_minus_le_iff ereal_plus_eq_PInfty)
+by (metis add.commute assms ereal_eq_minus_iff ereal_minus_le_iff ereal_plus_eq_PInfty)
 
 lemma Limsup_const_add:
   fixes c :: "'a::{complete_linorder, linorder_topology, topological_monoid_add, ordered_ab_semigroup_add}"
@@ -345,7 +345,11 @@
      (transfer ; auto intro: add_mono mult_mono mult_ac ereal_left_distrib ereal_mult_left_mono)+
 
 instance ennreal :: linordered_nonzero_semiring
-  proof qed (transfer; simp)
+proof
+  fix a b::ennreal
+  show "a < b \<Longrightarrow> a + 1 < b + 1"
+    by transfer (simp add: add_right_mono ereal_add_cancel_right less_le)
+qed (transfer; simp)
 
 instance ennreal :: strict_ordered_ab_semigroup_add
 proof
--- a/src/HOL/Library/Extended_Real.thy	Fri Feb 23 15:07:30 2018 +0100
+++ b/src/HOL/Library/Extended_Real.thy	Fri Feb 23 15:17:51 2018 +0100
@@ -1800,8 +1800,176 @@
 lemma max_MInf2 [simp]: "max x (-\<infinity>::ereal) = x"
 by (metis max_bot2 bot_ereal_def)
 
-
-subsubsection "Topological space"
+subsection \<open>Extended real intervals\<close>
+
+lemma real_greaterThanLessThan_infinity_eq:
+  "real_of_ereal ` {N::ereal<..<\<infinity>} =
+    (if N = \<infinity> then {} else if N = -\<infinity> then UNIV else {real_of_ereal N<..})"
+proof -
+  {
+    fix x::real
+    have "x \<in> real_of_ereal ` {- \<infinity><..<\<infinity>::ereal}"
+      by (auto intro!: image_eqI[where x="ereal x"])
+  } moreover {
+    fix x::ereal
+    assume "N \<noteq> - \<infinity>" "N < x" "x \<noteq> \<infinity>"
+    then have "real_of_ereal N < real_of_ereal x"
+      by (cases N; cases x; simp)
+  } moreover {
+    fix x::real
+    assume "N \<noteq> \<infinity>" "real_of_ereal N < x"
+    then have "x \<in> real_of_ereal ` {N<..<\<infinity>}"
+      by (cases N) (auto intro!: image_eqI[where x="ereal x"])
+  } ultimately show ?thesis by auto
+qed
+
+lemma real_greaterThanLessThan_minus_infinity_eq:
+  "real_of_ereal ` {-\<infinity><..<N::ereal} =
+    (if N = \<infinity> then UNIV else if N = -\<infinity> then {} else {..<real_of_ereal N})"
+proof -
+  have "real_of_ereal ` {-\<infinity><..<N::ereal} = uminus ` real_of_ereal ` {-N<..<\<infinity>}"
+    by (auto simp: ereal_uminus_less_reorder intro!: image_eqI[where x="-x" for x])
+  also note real_greaterThanLessThan_infinity_eq
+  finally show ?thesis by (auto intro!: image_eqI[where x="-x" for x])
+qed
+
+lemma real_greaterThanLessThan_inter:
+  "real_of_ereal ` {N<..<M::ereal} = real_of_ereal ` {-\<infinity><..<M} \<inter> real_of_ereal ` {N<..<\<infinity>}"
+  apply safe
+  subgoal by force
+  subgoal by force
+  subgoal for x y z
+    by (cases y; cases z) (auto intro!: image_eqI[where x=z] simp: )
+  done
+
+lemma real_atLeastGreaterThan_eq: "real_of_ereal ` {N<..<M::ereal} =
+   (if N = \<infinity> then {} else
+   if N = -\<infinity> then
+    (if M = \<infinity> then UNIV
+    else if M = -\<infinity> then {}
+    else {..< real_of_ereal M})
+  else if M = - \<infinity> then {}
+  else if M = \<infinity> then {real_of_ereal N<..}
+  else {real_of_ereal N <..< real_of_ereal M})"
+  apply (subst real_greaterThanLessThan_inter)
+  apply (subst real_greaterThanLessThan_minus_infinity_eq)
+  apply (subst real_greaterThanLessThan_infinity_eq)
+  apply auto
+  done
+
+lemma real_image_ereal_ivl:
+  fixes a b::ereal
+  shows
+  "real_of_ereal ` {a<..<b} =
+  (if a < b then (if a = - \<infinity> then if b = \<infinity> then UNIV else {..<real_of_ereal b}
+  else if b = \<infinity> then {real_of_ereal a<..} else {real_of_ereal a <..< real_of_ereal b}) else {})"
+  by (cases a; cases b; simp add: real_atLeastGreaterThan_eq not_less)
+
+lemma fixes a b c::ereal
+  shows not_inftyI: "a < b \<Longrightarrow> b < c \<Longrightarrow> abs b \<noteq> \<infinity>"
+  by force
+
+lemma
+  interval_neqs:
+  fixes r s t::real
+  shows "{r<..<s} \<noteq> {t<..}"
+    and "{r<..<s} \<noteq> {..<t}"
+    and "{r<..<ra} \<noteq> UNIV"
+    and "{r<..} \<noteq> {..<s}"
+    and "{r<..} \<noteq> UNIV"
+    and "{..<r} \<noteq> UNIV"
+    and "{} \<noteq> {r<..}"
+    and "{} \<noteq> {..<r}"
+  subgoal
+    by (metis dual_order.strict_trans greaterThanLessThan_iff greaterThan_iff gt_ex not_le order_refl)
+  subgoal
+    by (metis (no_types, hide_lams) greaterThanLessThan_empty_iff greaterThanLessThan_iff gt_ex
+        lessThan_iff minus_minus neg_less_iff_less not_less order_less_irrefl)
+  subgoal by force
+  subgoal
+    by (metis greaterThanLessThan_empty_iff greaterThanLessThan_eq greaterThan_iff inf.idem
+        lessThan_iff lessThan_non_empty less_irrefl not_le)
+  subgoal by force
+  subgoal by force
+  subgoal using greaterThan_non_empty by blast
+  subgoal using lessThan_non_empty by blast
+  done
+
+lemma greaterThanLessThan_eq_iff:
+  fixes r s t u::real
+  shows "({r<..<s} = {t<..<u}) = (r \<ge> s \<and> u \<le> t \<or> r = t \<and> s = u)"
+  by (metis cInf_greaterThanLessThan cSup_greaterThanLessThan greaterThanLessThan_empty_iff not_le)
+
+lemma real_of_ereal_image_greaterThanLessThan_iff:
+  "real_of_ereal ` {a <..< b} = real_of_ereal ` {c <..< d} \<longleftrightarrow> (a \<ge> b \<and> c \<ge> d \<or> a = c \<and> b = d)"
+  unfolding real_atLeastGreaterThan_eq
+  by (cases a; cases b; cases c; cases d;
+    simp add: greaterThanLessThan_eq_iff interval_neqs interval_neqs[symmetric])
+
+lemma uminus_image_real_of_ereal_image_greaterThanLessThan:
+  "uminus ` real_of_ereal ` {l <..< u} = real_of_ereal ` {-u <..< -l}"
+  by (force simp: algebra_simps ereal_less_uminus_reorder
+    ereal_uminus_less_reorder intro: image_eqI[where x="-x" for x])
+
+lemma add_image_real_of_ereal_image_greaterThanLessThan:
+  "(+) c ` real_of_ereal ` {l <..< u} = real_of_ereal ` {c + l <..< c + u}"
+  apply safe
+  subgoal for x
+    using ereal_less_add[of c]
+    by (force simp: real_of_ereal_add add.commute)
+  subgoal for _ x
+    by (force simp: add.commute real_of_ereal_minus ereal_minus_less ereal_less_minus
+      intro: image_eqI[where x="x - c"])
+  done
+
+lemma add2_image_real_of_ereal_image_greaterThanLessThan:
+  "(\<lambda>x. x + c) ` real_of_ereal ` {l <..< u} = real_of_ereal ` {l + c <..< u + c}"
+  using add_image_real_of_ereal_image_greaterThanLessThan[of c l u]
+  by (metis add.commute image_cong)
+
+lemma minus_image_real_of_ereal_image_greaterThanLessThan:
+  "(-) c ` real_of_ereal ` {l <..< u} = real_of_ereal ` {c - u <..< c - l}"
+  (is "?l = ?r")
+proof -
+  have "?l = (+) c ` uminus ` real_of_ereal ` {l <..< u}" by auto
+  also note uminus_image_real_of_ereal_image_greaterThanLessThan
+  also note add_image_real_of_ereal_image_greaterThanLessThan
+  finally show ?thesis by (simp add: minus_ereal_def)
+qed
+
+lemma real_ereal_bound_lemma_up:
+  assumes "s \<in> real_of_ereal ` {a<..<b}"
+  assumes "t \<notin> real_of_ereal ` {a<..<b}"
+  assumes "s \<le> t"
+  shows "b \<noteq> \<infinity>"
+  using assms
+  apply (cases b)
+  subgoal by force
+  subgoal by (metis PInfty_neq_ereal(2) assms dual_order.strict_trans1 ereal_infty_less(1)
+    ereal_less_ereal_Ex greaterThanLessThan_empty_iff greaterThanLessThan_iff greaterThan_iff
+    image_eqI less_imp_le linordered_field_no_ub not_less order_trans
+    real_greaterThanLessThan_infinity_eq real_image_ereal_ivl real_of_ereal.simps(1))
+  subgoal by force
+  done
+
+lemma real_ereal_bound_lemma_down:
+  assumes "s \<in> real_of_ereal ` {a<..<b}"
+  assumes "t \<notin> real_of_ereal ` {a<..<b}"
+  assumes "t \<le> s"
+  shows "a \<noteq> - \<infinity>"
+  using assms
+  apply (cases b)
+  subgoal
+    apply safe
+    using assms(1)
+    apply (auto simp: real_greaterThanLessThan_minus_infinity_eq)
+    done
+  subgoal by (auto simp: real_greaterThanLessThan_minus_infinity_eq)
+  subgoal by auto
+  done
+
+
+subsection "Topological space"
 
 instantiation ereal :: linear_continuum_topology
 begin
@@ -2469,6 +2637,21 @@
      by auto
 qed (auto simp add: image_Union image_Int)
 
+lemma open_image_real_of_ereal:
+  fixes X::"ereal set"
+  assumes "open X"
+  assumes "\<infinity> \<notin> X"
+  assumes "-\<infinity> \<notin> X"
+  shows "open (real_of_ereal ` X)"
+proof -
+  have "real_of_ereal ` X = ereal -` X"
+    apply safe
+    subgoal by (metis assms(2) assms(3) real_of_ereal.elims vimageI)
+    subgoal using image_iff by fastforce
+    done
+  thus ?thesis
+    by (auto intro!: open_ereal_vimage assms)
+qed
 
 lemma eventually_finite:
   fixes x :: ereal
--- a/src/HOL/Library/Indicator_Function.thy	Fri Feb 23 15:07:30 2018 +0100
+++ b/src/HOL/Library/Indicator_Function.thy	Fri Feb 23 15:17:51 2018 +0100
@@ -10,6 +10,9 @@
 
 definition "indicator S x = (if x \<in> S then 1 else 0)"
 
+text\<open>Type constrained version\<close>
+abbreviation indicat_real :: "'a set \<Rightarrow> 'a \<Rightarrow> real" where "indicat_real S \<equiv> indicator S"
+
 lemma indicator_simps[simp]:
   "x \<in> S \<Longrightarrow> indicator S x = 1"
   "x \<notin> S \<Longrightarrow> indicator S x = 0"
--- a/src/HOL/Limits.thy	Fri Feb 23 15:07:30 2018 +0100
+++ b/src/HOL/Limits.thy	Fri Feb 23 15:17:51 2018 +0100
@@ -52,6 +52,9 @@
   for f :: "_ \<Rightarrow> real"
   by (rule filterlim_mono[OF _ at_top_le_at_infinity order_refl])
 
+lemma filterlim_real_at_infinity_sequentially: "filterlim real at_infinity sequentially"
+  by (simp add: filterlim_at_top_imp_at_infinity filterlim_real_sequentially)
+
 lemma lim_infinity_imp_sequentially: "(f \<longlongrightarrow> l) at_infinity \<Longrightarrow> ((\<lambda>n. f(n)) \<longlongrightarrow> l) sequentially"
   by (simp add: filterlim_at_top_imp_at_infinity filterlim_compose filterlim_real_sequentially)
 
@@ -1256,6 +1259,20 @@
   for a :: real
   unfolding at_right_to_0[of a] by (simp add: eventually_filtermap)
 
+lemma at_to_0: "at a = filtermap (\<lambda>x. x + a) (at 0)"
+  for a :: "'a::real_normed_vector"
+  using filtermap_at_shift[of "-a" 0] by simp
+
+lemma filterlim_at_to_0:
+  "filterlim f F (at a) \<longleftrightarrow> filterlim (\<lambda>x. f (x + a)) F (at 0)"
+  for a :: "'a::real_normed_vector"
+  unfolding filterlim_def filtermap_filtermap at_to_0[of a] ..
+
+lemma eventually_at_to_0:
+  "eventually P (at a) \<longleftrightarrow> eventually (\<lambda>x. P (x + a)) (at 0)"
+  for a ::  "'a::real_normed_vector"
+  unfolding at_to_0[of a] by (simp add: eventually_filtermap)
+
 lemma filtermap_at_minus: "filtermap (\<lambda>x. - x) (at a) = at (- a)"
   for a :: "'a::real_normed_vector"
   by (simp add: filter_eq_iff eventually_filtermap eventually_at_filter filtermap_nhds_minus[symmetric])
@@ -1268,6 +1285,7 @@
   for a :: real
   by (simp add: filter_eq_iff eventually_filtermap eventually_at_filter filtermap_nhds_minus[symmetric])
 
+
 lemma filterlim_at_left_to_right:
   "filterlim f F (at_left a) \<longleftrightarrow> filterlim (\<lambda>x. f (- x)) F (at_right (-a))"
   for a :: real
@@ -1486,6 +1504,36 @@
   for c :: nat
   by (rule filterlim_subseq) (auto simp: strict_mono_def)
 
+lemma filterlim_times_pos:
+  "LIM x F1. c * f x :> at_right l"
+  if "filterlim f (at_right p) F1" "0 < c" "l = c * p"
+  for c::"'a::{linordered_field, linorder_topology}"
+  unfolding filterlim_iff
+proof safe
+  fix P
+  assume "\<forall>\<^sub>F x in at_right l. P x"
+  then obtain d where "c * p < d" "\<And>y. y > c * p \<Longrightarrow> y < d \<Longrightarrow> P y"
+    unfolding \<open>l = _ \<close> eventually_at_right_field
+    by auto
+  then have "\<forall>\<^sub>F a in at_right p. P (c * a)"
+    by (auto simp: eventually_at_right_field \<open>0 < c\<close> field_simps intro!: exI[where x="d/c"])
+  from that(1)[unfolded filterlim_iff, rule_format, OF this]
+  show "\<forall>\<^sub>F x in F1. P (c * f x)" .
+qed
+
+lemma filtermap_nhds_times: "c \<noteq> 0 \<Longrightarrow> filtermap (times c) (nhds a) = nhds (c * a)"
+  for a c :: "'a::real_normed_field"
+  by (rule filtermap_fun_inverse[where g="\<lambda>x. inverse c * x"])
+    (auto intro!: tendsto_eq_intros filterlim_ident)
+
+lemma filtermap_times_pos_at_right:
+  fixes c::"'a::{linordered_field, linorder_topology}"
+  assumes "c > 0"
+  shows "filtermap (times c) (at_right p) = at_right (c * p)"
+  using assms
+  by (intro filtermap_fun_inverse[where g="\<lambda>x. inverse c * x"])
+    (auto intro!: filterlim_ident filterlim_times_pos)
+
 lemma at_to_infinity: "(at (0::'a::{real_normed_field,field})) = filtermap inverse at_infinity"
 proof (rule antisym)
   have "(inverse \<longlongrightarrow> (0::'a)) at_infinity"
@@ -1936,6 +1984,10 @@
 lemma lim_inverse_n: "((\<lambda>n. inverse(of_nat n)) \<longlongrightarrow> (0::'a::real_normed_field)) sequentially"
   using lim_1_over_n by (simp add: inverse_eq_divide)
 
+lemma lim_inverse_n': "((\<lambda>n. 1 / n) \<longlongrightarrow> 0) sequentially"
+  using lim_inverse_n
+  by (simp add: inverse_eq_divide)
+
 lemma LIMSEQ_Suc_n_over_n: "(\<lambda>n. of_nat (Suc n) / of_nat n :: 'a :: real_normed_field) \<longlonglongrightarrow> 1"
 proof (rule Lim_transform_eventually)
   show "eventually (\<lambda>n. 1 + inverse (of_nat n :: 'a) = of_nat (Suc n) / of_nat n) sequentially"
--- a/src/HOL/List.thy	Fri Feb 23 15:07:30 2018 +0100
+++ b/src/HOL/List.thy	Fri Feb 23 15:17:51 2018 +0100
@@ -388,6 +388,10 @@
 abbreviation "insort \<equiv> insort_key (\<lambda>x. x)"
 abbreviation "insort_insert \<equiv> insort_insert_key (\<lambda>x. x)"
 
+definition stable_sort_key :: "(('b \<Rightarrow> 'a) \<Rightarrow> 'b list \<Rightarrow> 'b list) \<Rightarrow> bool" where
+"stable_sort_key sk =
+   (\<forall>f xs k. filter (\<lambda>y. f y = k) (sk f xs) = filter (\<lambda>y. f y = k) xs)"
+
 end
 
 
@@ -5375,61 +5379,35 @@
 lemma sorted_enumerate [simp]: "sorted (map fst (enumerate n xs))"
 by (simp add: enumerate_eq_zip)
 
-text \<open>Stability of function @{const sort_key}:\<close>
-
-lemma sort_key_stable:
-  "x \<in> set xs \<Longrightarrow> [y <- sort_key f xs. f y = f x] = [y <- xs. f y = f x]"
-proof (induction xs arbitrary: x)
+text \<open>Stability of @{const sort_key}:\<close>
+
+lemma sort_key_stable: "[y <- sort_key f xs. f y = k] = [y <- xs. f y = k]"
+proof (induction xs)
   case Nil thus ?case by simp
 next
   case (Cons a xs)
   thus ?case
-  proof (cases "x \<in> set xs")
+  proof (cases "f a = k")
+    case False thus ?thesis
+      using Cons.IH by (metis (mono_tags) filter.simps(2) filter_sort)
+  next
     case True
-    thus ?thesis
-    proof (cases "f a = f x")
-      case False thus ?thesis
-        using Cons.IH by (metis (mono_tags) True filter.simps(2) filter_sort)
-    next
-      case True
-      hence ler: "[y <- (a # xs). f y = f x] = a # [y <- xs. f y = f a]" by simp
-      have "\<forall>y \<in> set (sort_key f [y <- xs. f y = f a]). f y = f a" by simp
-      hence "insort_key f a (sort_key f [y <- xs. f y = f a])
-              = a # (sort_key f [y <- xs. f y = f a])"
-        by (simp add: insort_is_Cons)
-      hence lel: "[y <- sort_key f (a # xs). f y = f x] = a # [y <- sort_key f xs. f y = f a]"
-        by (metis True filter_sort ler sort_key_simps(2))
-      from lel ler show ?thesis using Cons.IH \<open>x \<in> set xs\<close> by (metis True filter_sort)
-    qed
-  next
-    case False
-    from Cons.prems have "x = a" by (metis False set_ConsD)
-    have ler: "[y <- (a # xs). f y = f a] = a # [y <- xs. f y = f a]" by simp
+    hence ler: "[y <- (a # xs). f y = k] = a # [y <- xs. f y = f a]" by simp
     have "\<forall>y \<in> set (sort_key f [y <- xs. f y = f a]). f y = f a" by simp
     hence "insort_key f a (sort_key f [y <- xs. f y = f a])
-           = a # (sort_key f [y <- xs. f y = f a])"
+            = a # (sort_key f [y <- xs. f y = f a])"
       by (simp add: insort_is_Cons)
-    hence lel: "[y <- sort_key f (a # xs). f y = f a] = a # [y <- sort_key f xs. f y = f a]"
-      by (metis (mono_tags) filter.simps(2) filter_sort sort_key_simps(2))
-    show ?thesis (is "?l = ?r")
-    proof (cases "f a \<in> set (map f xs)")
-      case False
-      hence "\<forall>y \<in> set xs. f y \<noteq> f a" by (metis image_eqI set_map)
-      hence R: "?r = [a]" using ler \<open>x=a\<close> by simp
-      have L: "?l = [a]" using lel \<open>x=a\<close> by (metis R filter_sort insort_key.simps(1) sort_key_simps)
-      from L R show ?thesis ..
-    next
-      case True
-      then obtain z where Z: "z \<in> set xs \<and> f z = f a" by auto
-      hence L: "[y <- sort_key f xs. f y = f z] = [y <- sort_key f xs. f y = f a]" by simp
-      from Z have R: "[y <- xs. f y = f z] = [y <- xs. f y = f a]" by simp
-      from L R Z show ?thesis using Cons.IH ler lel \<open>x=a\<close> by metis
-    qed
+    hence lel: "[y <- sort_key f (a # xs). f y = k] = a # [y <- sort_key f xs. f y = f a]"
+      by (metis True filter_sort ler sort_key_simps(2))
+    from lel ler show ?thesis using Cons.IH True by (auto)
   qed
 qed
 
+corollary stable_sort_key_sort_key: "stable_sort_key sort_key"
+by(simp add: stable_sort_key_def sort_key_stable)
+
 lemma sort_key_const: "sort_key (\<lambda>x. c) xs = xs"
-by (metis (mono_tags) filter_False filter_True sort_key_simps(1) sort_key_stable)
+by (metis (mono_tags) filter_True sort_key_stable)
 
 
 subsubsection \<open>@{const transpose} on sorted lists\<close>
--- a/src/HOL/Nat.thy	Fri Feb 23 15:07:30 2018 +0100
+++ b/src/HOL/Nat.thy	Fri Feb 23 15:17:51 2018 +0100
@@ -1774,7 +1774,7 @@
 
 class ring_char_0 = ring_1 + semiring_char_0
 
-context linordered_semidom
+context linordered_nonzero_semiring
 begin
 
 lemma of_nat_0_le_iff [simp]: "0 \<le> of_nat n"
@@ -1783,8 +1783,21 @@
 lemma of_nat_less_0_iff [simp]: "\<not> of_nat m < 0"
   by (simp add: not_less)
 
+lemma of_nat_mono[simp]: "i \<le> j \<Longrightarrow> of_nat i \<le> of_nat j"
+  by (auto simp: le_iff_add intro!: add_increasing2)
+
 lemma of_nat_less_iff [simp]: "of_nat m < of_nat n \<longleftrightarrow> m < n"
-  by (induct m n rule: diff_induct) (simp_all add: add_pos_nonneg)
+proof(induct m n rule: diff_induct)
+  case (1 m) then show ?case
+    by auto
+next
+  case (2 n) then show ?case
+    by (simp add: add_pos_nonneg)
+next
+  case (3 m n)
+  then show ?case
+    by (auto simp: add_commute [of 1] add_mono1 not_less add_right_mono leD)
+qed
 
 lemma of_nat_le_iff [simp]: "of_nat m \<le> of_nat n \<longleftrightarrow> m \<le> n"
   by (simp add: not_less [symmetric] linorder_not_less [symmetric])
@@ -1795,7 +1808,7 @@
 lemma of_nat_less_imp_less: "of_nat m < of_nat n \<Longrightarrow> m < n"
   by simp
 
-text \<open>Every \<open>linordered_semidom\<close> has characteristic zero.\<close>
+text \<open>Every \<open>linordered_nonzero_semiring\<close> has characteristic zero.\<close>
 
 subclass semiring_char_0
   by standard (auto intro!: injI simp add: eq_iff)
@@ -1810,6 +1823,14 @@
 
 end
 
+
+context linordered_semidom
+begin
+subclass linordered_nonzero_semiring ..
+subclass semiring_char_0 ..
+end
+
+
 context linordered_idom
 begin
 
--- a/src/HOL/NthRoot.thy	Fri Feb 23 15:07:30 2018 +0100
+++ b/src/HOL/NthRoot.thy	Fri Feb 23 15:17:51 2018 +0100
@@ -480,6 +480,9 @@
 lemma sqrt_le_D: "sqrt x \<le> y \<Longrightarrow> x \<le> y\<^sup>2"
   by (meson not_le real_less_rsqrt)
 
+lemma sqrt_ge_absD: "\<bar>x\<bar> \<le> sqrt y \<Longrightarrow> x\<^sup>2 \<le> y"
+  using real_sqrt_le_iff[of "x\<^sup>2"] by simp
+
 lemma sqrt_even_pow2:
   assumes n: "even n"
   shows "sqrt (2 ^ n) = 2 ^ (n div 2)"
@@ -538,6 +541,8 @@
   DERIV_real_sqrt_generic[THEN DERIV_chain2, derivative_intros]
   DERIV_real_root_generic[THEN DERIV_chain2, derivative_intros]
 
+lemmas has_derivative_real_sqrt[derivative_intros] = DERIV_real_sqrt[THEN DERIV_compose_FDERIV]
+
 lemma not_real_square_gt_zero [simp]: "\<not> 0 < x * x \<longleftrightarrow> x = 0"
   for x :: real
   apply auto
@@ -658,6 +663,13 @@
 lemma le_real_sqrt_sumsq [simp]: "x \<le> sqrt (x * x + y * y)"
   by (simp add: power2_eq_square [symmetric])
 
+lemma sqrt_sum_squares_le_sum:
+  "\<lbrakk>0 \<le> x; 0 \<le> y\<rbrakk> \<Longrightarrow> sqrt (x\<^sup>2 + y\<^sup>2) \<le> x + y"
+  apply (rule power2_le_imp_le)
+  apply (simp add: power2_sum)
+  apply simp
+  done
+
 lemma real_sqrt_sum_squares_triangle_ineq:
   "sqrt ((a + c)\<^sup>2 + (b + d)\<^sup>2) \<le> sqrt (a\<^sup>2 + b\<^sup>2) + sqrt (c\<^sup>2 + d\<^sup>2)"
   apply (rule power2_le_imp_le)
--- a/src/HOL/Rings.thy	Fri Feb 23 15:07:30 2018 +0100
+++ b/src/HOL/Rings.thy	Fri Feb 23 15:17:51 2018 +0100
@@ -2245,7 +2245,8 @@
 
 end
 
-class linordered_nonzero_semiring = ordered_comm_semiring + monoid_mult + linorder + zero_less_one
+class linordered_nonzero_semiring = ordered_comm_semiring + monoid_mult + linorder + zero_less_one +
+  assumes add_mono1: "a < b \<Longrightarrow> a + 1 < b + 1"
 begin
 
 subclass zero_neq_one
@@ -2278,7 +2279,15 @@
   assumes le_add_diff_inverse2 [simp]: "b \<le> a \<Longrightarrow> a - b + b = a"
 begin
 
-subclass linordered_nonzero_semiring ..
+subclass linordered_nonzero_semiring 
+proof
+  show "a + 1 < b + 1" if "a < b" for a b
+  proof (rule ccontr, simp add: not_less)
+    assume "b \<le> a"
+    with that show False
+      by (simp add: )
+  qed
+qed
 
 text \<open>Addition is the inverse of subtraction.\<close>
 
--- a/src/HOL/Set_Interval.thy	Fri Feb 23 15:07:30 2018 +0100
+++ b/src/HOL/Set_Interval.thy	Fri Feb 23 15:17:51 2018 +0100
@@ -222,6 +222,10 @@
   "{a..<b} = {a..b} - {b}"
   by (auto simp add: atLeastLessThan_def atLeastAtMost_def)
 
+lemma (in order) greaterThanAtMost_eq_atLeastAtMost_diff:
+  "{a<..b} = {a..b} - {a}"
+  by (auto simp add: greaterThanAtMost_def atLeastAtMost_def)
+
 end
 
 subsubsection\<open>Emptyness, singletons, subset\<close>
@@ -869,6 +873,19 @@
 context linordered_semidom
 begin
 
+lemma image_add_atLeast[simp]: "plus k ` {i..} = {k + i..}"
+proof -
+  have "n = k + (n - k)" if "i + k \<le> n" for n
+  proof -
+    have "n = (n - (k + i)) + (k + i)" using that
+      by (metis add_commute le_add_diff_inverse)
+    then show "n = k + (n - k)"
+      by (metis local.add_diff_cancel_left' add_assoc add_commute)
+  qed
+  then show ?thesis
+    by (fastforce simp: add_le_imp_le_diff add.commute)
+qed
+
 lemma image_add_atLeastAtMost [simp]:
   "plus k ` {i..j} = {i + k..j + k}" (is "?A = ?B")
 proof
@@ -911,112 +928,11 @@
   "(\<lambda>n. n + k) ` {i..<j} = {i + k..<j + k}"
   by (simp add: add.commute [of _ k])
 
+lemma image_add_greaterThanAtMost[simp]: "(+) c ` {a<..b} = {c + a<..c + b}"
+  by (simp add: image_set_diff greaterThanAtMost_eq_atLeastAtMost_diff ac_simps)
+
 end
 
-lemma image_Suc_atLeastAtMost [simp]:
-  "Suc ` {i..j} = {Suc i..Suc j}"
-  using image_add_atLeastAtMost [of 1 i j]
-    by (simp only: plus_1_eq_Suc) simp
-
-lemma image_Suc_atLeastLessThan [simp]:
-  "Suc ` {i..<j} = {Suc i..<Suc j}"
-  using image_add_atLeastLessThan [of 1 i j]
-    by (simp only: plus_1_eq_Suc) simp
-
-corollary image_Suc_atMost:
-  "Suc ` {..n} = {1..Suc n}"
-  by (simp add: atMost_atLeast0 atLeastLessThanSuc_atLeastAtMost)
-
-corollary image_Suc_lessThan:
-  "Suc ` {..<n} = {1..n}"
-  by (simp add: lessThan_atLeast0 atLeastLessThanSuc_atLeastAtMost)
-  
-lemma image_diff_atLeastAtMost [simp]:
-  fixes d::"'a::linordered_idom" shows "((-) d ` {a..b}) = {d-b..d-a}"
-  apply auto
-  apply (rule_tac x="d-x" in rev_image_eqI, auto)
-  done
-
-lemma image_mult_atLeastAtMost [simp]:
-  fixes d::"'a::linordered_field"
-  assumes "d>0" shows "(( * ) d ` {a..b}) = {d*a..d*b}"
-  using assms
-  by (auto simp: field_simps mult_le_cancel_right intro: rev_image_eqI [where x="x/d" for x])
-
-lemma image_affinity_atLeastAtMost:
-  fixes c :: "'a::linordered_field"
-  shows "((\<lambda>x. m*x + c) ` {a..b}) = (if {a..b}={} then {}
-            else if 0 \<le> m then {m*a + c .. m *b + c}
-            else {m*b + c .. m*a + c})"
-  apply (case_tac "m=0", auto simp: mult_le_cancel_left)
-  apply (rule_tac x="inverse m*(x-c)" in rev_image_eqI, auto simp: field_simps)
-  apply (rule_tac x="inverse m*(x-c)" in rev_image_eqI, auto simp: field_simps)
-  done
-
-lemma image_affinity_atLeastAtMost_diff:
-  fixes c :: "'a::linordered_field"
-  shows "((\<lambda>x. m*x - c) ` {a..b}) = (if {a..b}={} then {}
-            else if 0 \<le> m then {m*a - c .. m*b - c}
-            else {m*b - c .. m*a - c})"
-  using image_affinity_atLeastAtMost [of m "-c" a b]
-  by simp
-
-lemma image_affinity_atLeastAtMost_div:
-  fixes c :: "'a::linordered_field"
-  shows "((\<lambda>x. x/m + c) ` {a..b}) = (if {a..b}={} then {}
-            else if 0 \<le> m then {a/m + c .. b/m + c}
-            else {b/m + c .. a/m + c})"
-  using image_affinity_atLeastAtMost [of "inverse m" c a b]
-  by (simp add: field_class.field_divide_inverse algebra_simps)
-
-lemma image_affinity_atLeastAtMost_div_diff:
-  fixes c :: "'a::linordered_field"
-  shows "((\<lambda>x. x/m - c) ` {a..b}) = (if {a..b}={} then {}
-            else if 0 \<le> m then {a/m - c .. b/m - c}
-            else {b/m - c .. a/m - c})"
-  using image_affinity_atLeastAtMost_diff [of "inverse m" c a b]
-  by (simp add: field_class.field_divide_inverse algebra_simps)
-
-lemma atLeast1_lessThan_eq_remove0:
-  "{Suc 0..<n} = {..<n} - {0}"
-  by auto
-
-lemma atLeast1_atMost_eq_remove0:
-  "{Suc 0..n} = {..n} - {0}"
-  by auto
-
-lemma image_add_int_atLeastLessThan:
-    "(%x. x + (l::int)) ` {0..<u-l} = {l..<u}"
-  apply (auto simp add: image_def)
-  apply (rule_tac x = "x - l" in bexI)
-  apply auto
-  done
-
-lemma image_minus_const_atLeastLessThan_nat:
-  fixes c :: nat
-  shows "(\<lambda>i. i - c) ` {x ..< y} =
-      (if c < y then {x - c ..< y - c} else if x < y then {0} else {})"
-    (is "_ = ?right")
-proof safe
-  fix a assume a: "a \<in> ?right"
-  show "a \<in> (\<lambda>i. i - c) ` {x ..< y}"
-  proof cases
-    assume "c < y" with a show ?thesis
-      by (auto intro!: image_eqI[of _ _ "a + c"])
-  next
-    assume "\<not> c < y" with a show ?thesis
-      by (auto intro!: image_eqI[of _ _ x] split: if_split_asm)
-  qed
-qed auto
-
-lemma image_int_atLeastLessThan:
-  "int ` {a..<b} = {int a..<int b}"
-  by (auto intro!: image_eqI [where x = "nat x" for x])
-
-lemma image_int_atLeastAtMost:
-  "int ` {a..b} = {int a..int b}"
-  by (auto intro!: image_eqI [where x = "nat x" for x])
-
 context ordered_ab_group_add
 begin
 
@@ -1057,8 +973,184 @@
   and image_uminus_greaterThanLessThan[simp]: "uminus ` {x<..<y} = {-y<..<-x}"
   by (simp_all add: atLeastAtMost_def greaterThanAtMost_def atLeastLessThan_def
       greaterThanLessThan_def image_Int[OF inj_uminus] Int_commute)
+
+lemma image_add_atMost[simp]: "(+) c ` {..a} = {..c + a}"
+  by (auto intro!: image_eqI[where x="x - c" for x] simp: algebra_simps)
+
 end
 
+lemma image_Suc_atLeastAtMost [simp]:
+  "Suc ` {i..j} = {Suc i..Suc j}"
+  using image_add_atLeastAtMost [of 1 i j]
+    by (simp only: plus_1_eq_Suc) simp
+
+lemma image_Suc_atLeastLessThan [simp]:
+  "Suc ` {i..<j} = {Suc i..<Suc j}"
+  using image_add_atLeastLessThan [of 1 i j]
+    by (simp only: plus_1_eq_Suc) simp
+
+corollary image_Suc_atMost:
+  "Suc ` {..n} = {1..Suc n}"
+  by (simp add: atMost_atLeast0 atLeastLessThanSuc_atLeastAtMost)
+
+corollary image_Suc_lessThan:
+  "Suc ` {..<n} = {1..n}"
+  by (simp add: lessThan_atLeast0 atLeastLessThanSuc_atLeastAtMost)
+
+lemma image_diff_atLeastAtMost [simp]:
+  fixes d::"'a::linordered_idom" shows "((-) d ` {a..b}) = {d-b..d-a}"
+  apply auto
+  apply (rule_tac x="d-x" in rev_image_eqI, auto)
+  done
+
+lemma image_diff_atLeastLessThan [simp]:
+  fixes a b c::"'a::linordered_idom"
+  shows "(-) c ` {a..<b} = {c - b<..c - a}"
+proof -
+  have "(-) c ` {a..<b} = (+) c ` uminus ` {a ..<b}"
+    unfolding image_image by simp
+  also have "\<dots> = {c - b<..c - a}" by simp
+  finally show ?thesis by simp
+qed
+
+lemma image_minus_const_greaterThanAtMost_real[simp]:
+  fixes a b c::"'a::linordered_idom"
+  shows "(-) c ` {a<..b} = {c - b..<c - a}"
+proof -
+  have "(-) c ` {a<..b} = (+) c ` uminus ` {a<..b}"
+    unfolding image_image by simp
+  also have "\<dots> = {c - b..<c - a}" by simp
+  finally show ?thesis by simp
+qed
+
+lemma image_minus_const_atLeast_real[simp]:
+  fixes a c::"'a::linordered_idom"
+  shows "(-) c ` {a..} = {..c - a}"
+proof -
+  have "(-) c ` {a..} = (+) c ` uminus ` {a ..}"
+    unfolding image_image by simp
+  also have "\<dots> = {..c - a}" by simp
+  finally show ?thesis by simp
+qed
+
+lemma image_minus_const_AtMost_real[simp]:
+  fixes b c::"'a::linordered_idom"
+  shows "(-) c ` {..b} = {c - b..}"
+proof -
+  have "(-) c ` {..b} = (+) c ` uminus ` {..b}"
+    unfolding image_image by simp
+  also have "\<dots> = {c - b..}" by simp
+  finally show ?thesis by simp
+qed
+
+context linordered_field begin
+
+lemma image_mult_atLeastAtMost [simp]:
+  "(( * ) d ` {a..b}) = {d*a..d*b}" if "d>0"
+  using that
+  by (auto simp: field_simps mult_le_cancel_right intro: rev_image_eqI [where x="x/d" for x])
+
+lemma image_mult_atLeastAtMost_if:
+  "( * ) c ` {x .. y} =
+    (if c > 0 then {c * x .. c * y} else if x \<le> y then {c * y .. c * x} else {})"
+proof -
+  consider "c < 0" "x \<le> y" | "c = 0" "x \<le> y" | "c > 0" "x \<le> y" | "x > y"
+    using local.antisym_conv3 local.leI by blast
+  then show ?thesis
+  proof cases
+    case 1
+    have "( * ) c ` {x .. y} = uminus ` ( * ) (- c) ` {x .. y}"
+      by (simp add: image_image)
+    also have "\<dots> = {c * y .. c * x}"
+      using \<open>c < 0\<close>
+      by simp
+    finally show ?thesis
+      using \<open>c < 0\<close> by auto
+  qed (auto simp: not_le local.mult_less_cancel_left_pos)
+qed
+
+lemma image_mult_atLeastAtMost_if':
+  "(\<lambda>x. x * c) ` {x..y} =
+    (if x \<le> y then if c > 0 then {x * c .. y * c} else {y * c .. x * c} else {})"
+  by (subst mult.commute)
+    (simp add: image_mult_atLeastAtMost_if mult.commute mult_le_cancel_left_pos)
+
+lemma image_affinity_atLeastAtMost:
+  "((\<lambda>x. m*x + c) ` {a..b}) = (if {a..b}={} then {}
+            else if 0 \<le> m then {m*a + c .. m *b + c}
+            else {m*b + c .. m*a + c})"
+proof -
+  have "(\<lambda>x. m*x + c) = ((\<lambda>x. x + c) o ( * ) m)"
+    unfolding image_comp[symmetric]
+    by (simp add: o_def)
+  then show ?thesis
+    by (auto simp add: image_comp[symmetric] image_mult_atLeastAtMost_if mult_le_cancel_left)
+qed
+
+lemma image_affinity_atLeastAtMost_diff:
+  "((\<lambda>x. m*x - c) ` {a..b}) = (if {a..b}={} then {}
+            else if 0 \<le> m then {m*a - c .. m*b - c}
+            else {m*b - c .. m*a - c})"
+  using image_affinity_atLeastAtMost [of m "-c" a b]
+  by simp
+
+lemma image_affinity_atLeastAtMost_div:
+  "((\<lambda>x. x/m + c) ` {a..b}) = (if {a..b}={} then {}
+            else if 0 \<le> m then {a/m + c .. b/m + c}
+            else {b/m + c .. a/m + c})"
+  using image_affinity_atLeastAtMost [of "inverse m" c a b]
+  by (simp add: field_class.field_divide_inverse algebra_simps inverse_eq_divide)
+
+lemma image_affinity_atLeastAtMost_div_diff:
+  "((\<lambda>x. x/m - c) ` {a..b}) = (if {a..b}={} then {}
+            else if 0 \<le> m then {a/m - c .. b/m - c}
+            else {b/m - c .. a/m - c})"
+  using image_affinity_atLeastAtMost_diff [of "inverse m" c a b]
+  by (simp add: field_class.field_divide_inverse algebra_simps inverse_eq_divide)
+
+end
+
+lemma atLeast1_lessThan_eq_remove0:
+  "{Suc 0..<n} = {..<n} - {0}"
+  by auto
+
+lemma atLeast1_atMost_eq_remove0:
+  "{Suc 0..n} = {..n} - {0}"
+  by auto
+
+lemma image_add_int_atLeastLessThan:
+    "(%x. x + (l::int)) ` {0..<u-l} = {l..<u}"
+  apply (auto simp add: image_def)
+  apply (rule_tac x = "x - l" in bexI)
+  apply auto
+  done
+
+lemma image_minus_const_atLeastLessThan_nat:
+  fixes c :: nat
+  shows "(\<lambda>i. i - c) ` {x ..< y} =
+      (if c < y then {x - c ..< y - c} else if x < y then {0} else {})"
+    (is "_ = ?right")
+proof safe
+  fix a assume a: "a \<in> ?right"
+  show "a \<in> (\<lambda>i. i - c) ` {x ..< y}"
+  proof cases
+    assume "c < y" with a show ?thesis
+      by (auto intro!: image_eqI[of _ _ "a + c"])
+  next
+    assume "\<not> c < y" with a show ?thesis
+      by (auto intro!: image_eqI[of _ _ x] split: if_split_asm)
+  qed
+qed auto
+
+lemma image_int_atLeastLessThan:
+  "int ` {a..<b} = {int a..<int b}"
+  by (auto intro!: image_eqI [where x = "nat x" for x])
+
+lemma image_int_atLeastAtMost:
+  "int ` {a..b} = {int a..int b}"
+  by (auto intro!: image_eqI [where x = "nat x" for x])
+
+
 subsubsection \<open>Finiteness\<close>
 
 lemma finite_lessThan [iff]: fixes k :: nat shows "finite {..<k}"
--- a/src/HOL/Topological_Spaces.thy	Fri Feb 23 15:07:30 2018 +0100
+++ b/src/HOL/Topological_Spaces.thy	Fri Feb 23 15:17:51 2018 +0100
@@ -609,7 +609,6 @@
     and "filterlim g G (at x within {x. \<not>P x})"
   shows "filterlim (\<lambda>x. if P x then f x else g x) G (at x)"
   using assms by (intro filterlim_at_within_If) simp_all
-
 lemma (in linorder_topology) at_within_order:
   assumes "UNIV \<noteq> {x}"
   shows "at x within s =
@@ -692,7 +691,18 @@
      (\<exists>S. open S \<and> A \<in> S \<and> (\<forall>x. f x \<in> S \<inter> B - {A} \<longrightarrow> P x))" (is "?lhs = ?rhs")
   unfolding at_within_def filtercomap_inf eventually_inf_principal filtercomap_principal 
           eventually_filtercomap_nhds eventually_principal by blast
-    
+
+lemma eventually_at_right_field:
+  "eventually P (at_right x) \<longleftrightarrow> (\<exists>b>x. \<forall>y>x. y < b \<longrightarrow> P y)"
+  for x :: "'a::{linordered_field, linorder_topology}"
+  using linordered_field_no_ub[rule_format, of x]
+  by (auto simp: eventually_at_right)
+
+lemma eventually_at_left_field:
+  "eventually P (at_left x) \<longleftrightarrow> (\<exists>b<x. \<forall>y>b. y < x \<longrightarrow> P y)"
+  for x :: "'a::{linordered_field, linorder_topology}"
+  using linordered_field_no_lb[rule_format, of x]
+  by (auto simp: eventually_at_left)
 
 
 subsubsection \<open>Tendsto\<close>
@@ -762,9 +772,11 @@
 
 end
 
-lemma tendsto_within_subset:
-  "(f \<longlongrightarrow> l) (at x within S) \<Longrightarrow> T \<subseteq> S \<Longrightarrow> (f \<longlongrightarrow> l) (at x within T)"
-  by (blast intro: tendsto_mono at_le)
+lemma (in topological_space) filterlim_within_subset:
+  "filterlim f l (at x within S) \<Longrightarrow> T \<subseteq> S \<Longrightarrow> filterlim f l (at x within T)"
+  by (blast intro: filterlim_mono at_le)
+
+lemmas tendsto_within_subset = filterlim_within_subset
 
 lemma (in order_topology) order_tendsto_iff:
   "(f \<longlongrightarrow> x) F \<longleftrightarrow> (\<forall>l<x. eventually (\<lambda>x. l < f x) F) \<and> (\<forall>u>x. eventually (\<lambda>x. f x < u) F)"
@@ -963,6 +975,11 @@
 lemma Lim_ident_at: "\<not> trivial_limit (at x within s) \<Longrightarrow> Lim (at x within s) (\<lambda>x. x) = x"
   by (rule tendsto_Lim[OF _ tendsto_ident_at]) auto
 
+lemma eventually_Lim_ident_at:
+  "(\<forall>\<^sub>F y in at x within X. P (Lim (at x within X) (\<lambda>x. x)) y) \<longleftrightarrow>
+    (\<forall>\<^sub>F y in at x within X. P x y)" for x::"'a::t2_space"
+  by (cases "at x within X = bot") (auto simp: Lim_ident_at)
+
 lemma filterlim_at_bot_at_right:
   fixes f :: "'a::linorder_topology \<Rightarrow> 'b::linorder"
   assumes mono: "\<And>x y. Q x \<Longrightarrow> Q y \<Longrightarrow> x \<le> y \<Longrightarrow> f x \<le> f y"
@@ -2612,6 +2629,37 @@
     by (metis less_le)
 qed
 
+lemma (in linorder_topology) not_in_connected_cases:
+  assumes conn: "connected S"
+  assumes nbdd: "x \<notin> S"
+  assumes ne: "S \<noteq> {}"
+  obtains "bdd_above S" "\<And>y. y \<in> S \<Longrightarrow> x \<ge> y" | "bdd_below S" "\<And>y. y \<in> S \<Longrightarrow> x \<le> y"
+proof -
+  obtain s where "s \<in> S" using ne by blast
+  {
+    assume "s \<le> x"
+    have "False" if "x \<le> y" "y \<in> S" for y
+      using connectedD_interval[OF conn \<open>s \<in> S\<close> \<open>y \<in> S\<close> \<open>s \<le> x\<close> \<open>x \<le> y\<close>] \<open>x \<notin> S\<close>
+      by simp
+    then have wit: "y \<in> S \<Longrightarrow> x \<ge> y" for y
+      using le_cases by blast
+    then have "bdd_above S"
+      by (rule local.bdd_aboveI)
+    note this wit
+  } moreover {
+    assume "x \<le> s"
+    have "False" if "x \<ge> y" "y \<in> S" for y
+      using connectedD_interval[OF conn \<open>y \<in> S\<close> \<open>s \<in> S\<close> \<open>x \<ge> y\<close> \<open>s \<ge> x\<close> ] \<open>x \<notin> S\<close>
+      by simp
+    then have wit: "y \<in> S \<Longrightarrow> x \<le> y" for y
+      using le_cases by blast
+    then have "bdd_below S"
+      by (rule bdd_belowI)
+    note this wit
+  } ultimately show ?thesis
+    by (meson le_cases that)
+qed
+
 lemma connected_continuous_image:
   assumes *: "continuous_on s f"
     and "connected s"
@@ -3454,6 +3502,15 @@
 lemma isCont_Pair [simp]: "\<lbrakk>isCont f a; isCont g a\<rbrakk> \<Longrightarrow> isCont (\<lambda>x. (f x, g x)) a"
   by (fact continuous_Pair)
 
+lemma continuous_on_compose_Pair:
+  assumes f: "continuous_on (Sigma A B) (\<lambda>(a, b). f a b)"
+  assumes g: "continuous_on C g"
+  assumes h: "continuous_on C h"
+  assumes subset: "\<And>c. c \<in> C \<Longrightarrow> g c \<in> A" "\<And>c. c \<in> C \<Longrightarrow> h c \<in> B (g c)"
+  shows "continuous_on C (\<lambda>c. f (g c) (h c))"
+  using continuous_on_compose2[OF f continuous_on_Pair[OF g h]] subset
+  by auto
+
 
 subsubsection \<open>Connectedness of products\<close>
 
--- a/src/HOL/Transcendental.thy	Fri Feb 23 15:07:30 2018 +0100
+++ b/src/HOL/Transcendental.thy	Fri Feb 23 15:17:51 2018 +0100
@@ -1389,6 +1389,8 @@
 declare DERIV_exp[THEN DERIV_chain2, derivative_intros]
   and DERIV_exp[THEN DERIV_chain2, unfolded has_field_derivative_def, derivative_intros]
 
+lemmas has_derivative_exp[derivative_intros] = DERIV_exp[THEN DERIV_compose_FDERIV]
+
 lemma norm_exp: "norm (exp x) \<le> exp (norm x)"
 proof -
   from summable_norm[OF summable_norm_exp, of x]
@@ -1883,6 +1885,8 @@
 declare DERIV_ln_divide[THEN DERIV_chain2, derivative_intros]
   and DERIV_ln_divide[THEN DERIV_chain2, unfolded has_field_derivative_def, derivative_intros]
 
+lemmas has_derivative_ln[derivative_intros] = DERIV_ln[THEN DERIV_compose_FDERIV]
+
 lemma ln_series:
   assumes "0 < x" and "x < 2"
   shows "ln x = (\<Sum> n. (-1)^n * (1 / real (n + 1)) * (x - 1)^(Suc n))"
@@ -3094,24 +3098,33 @@
   shows "((\<lambda>x. f x powr g x) \<longlongrightarrow> a powr b) F"
   using tendsto_powr'[of f a F g b] assms by auto
 
+lemma has_derivative_powr[derivative_intros]:
+  assumes g[derivative_intros]: "(g has_derivative g') (at x within X)"
+    and f[derivative_intros]:"(f has_derivative f') (at x within X)"
+  assumes pos: "0 < g x" and "x \<in> X"
+  shows "((\<lambda>x. g x powr f x::real) has_derivative (\<lambda>h. (g x powr f x) * (f' h * ln (g x) + g' h * f x / g x))) (at x within X)"
+proof -
+  have "\<forall>\<^sub>F x in at x within X. g x > 0"
+    by (rule order_tendstoD[OF _ pos])
+      (rule has_derivative_continuous[OF g, unfolded continuous_within])
+  then obtain d where "d > 0" and pos': "\<And>x'. x' \<in> X \<Longrightarrow> dist x' x < d \<Longrightarrow> 0 < g x'"
+    using pos unfolding eventually_at by force
+  have "((\<lambda>x. exp (f x * ln (g x))) has_derivative
+    (\<lambda>h. (g x powr f x) * (f' h * ln (g x) + g' h * f x / g x))) (at x within X)"
+    using pos
+    by (auto intro!: derivative_eq_intros simp: divide_simps powr_def)
+  then show ?thesis
+    by (rule has_derivative_transform_within[OF _ \<open>d > 0\<close> \<open>x \<in> X\<close>]) (auto simp: powr_def dest: pos')
+qed
+
 lemma DERIV_powr:
   fixes r :: real
   assumes g: "DERIV g x :> m"
     and pos: "g x > 0"
     and f: "DERIV f x :> r"
   shows "DERIV (\<lambda>x. g x powr f x) x :> (g x powr f x) * (r * ln (g x) + m * f x / g x)"
-proof -
-  have "DERIV (\<lambda>x. exp (f x * ln (g x))) x :> (g x powr f x) * (r * ln (g x) + m * f x / g x)"
-    using pos
-    by (auto intro!: derivative_eq_intros g pos f simp: powr_def field_simps exp_diff)
-  then show ?thesis
-  proof (rule DERIV_cong_ev[OF refl _ refl, THEN iffD1, rotated])
-    from DERIV_isCont[OF g] pos have "\<forall>\<^sub>F x in at x. 0 < g x"
-      unfolding isCont_def by (rule order_tendstoD(1))
-    with pos show "\<forall>\<^sub>F x in nhds x. exp (f x * ln (g x)) = g x powr f x"
-      by (auto simp: eventually_at_filter powr_def elim: eventually_mono)
-  qed
-qed
+  using assms
+  by (auto intro!: derivative_eq_intros ext simp: has_field_derivative_def algebra_simps)
 
 lemma DERIV_fun_powr:
   fixes r :: real
@@ -3344,6 +3357,8 @@
 declare DERIV_sin[THEN DERIV_chain2, derivative_intros]
   and DERIV_sin[THEN DERIV_chain2, unfolded has_field_derivative_def, derivative_intros]
 
+lemmas has_derivative_sin[derivative_intros] = DERIV_sin[THEN DERIV_compose_FDERIV]
+
 lemma DERIV_cos [simp]: "DERIV cos x :> - sin x"
   for x :: "'a::{real_normed_field,banach}"
   unfolding sin_def cos_def scaleR_conv_of_real
@@ -3359,6 +3374,8 @@
 declare DERIV_cos[THEN DERIV_chain2, derivative_intros]
   and DERIV_cos[THEN DERIV_chain2, unfolded has_field_derivative_def, derivative_intros]
 
+lemmas has_derivative_cos[derivative_intros] = DERIV_cos[THEN DERIV_compose_FDERIV]
+
 lemma isCont_sin: "isCont sin x"
   for x :: "'a::{real_normed_field,banach}"
   by (rule DERIV_sin [THEN DERIV_isCont])
@@ -4598,6 +4615,8 @@
   unfolding tan_def
   by (auto intro!: derivative_eq_intros, simp add: divide_inverse power2_eq_square)
 
+lemmas has_derivative_tan[derivative_intros] = DERIV_tan[THEN DERIV_compose_FDERIV]
+
 lemma isCont_tan: "cos x \<noteq> 0 \<Longrightarrow> isCont tan x"
   for x :: "'a::{real_normed_field,banach}"
   by (rule DERIV_tan [THEN DERIV_isCont])
@@ -5265,6 +5284,10 @@
   DERIV_arctan[THEN DERIV_chain2, derivative_intros]
   DERIV_arctan[THEN DERIV_chain2, unfolded has_field_derivative_def, derivative_intros]
 
+lemmas has_derivative_arctan[derivative_intros] = DERIV_arctan[THEN DERIV_compose_FDERIV]
+  and has_derivative_arccos[derivative_intros] = DERIV_arccos[THEN DERIV_compose_FDERIV]
+  and has_derivative_arcsin[derivative_intros] = DERIV_arcsin[THEN DERIV_compose_FDERIV]
+
 lemma filterlim_tan_at_right: "filterlim tan at_bot (at_right (- (pi/2)))"
   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])
      (auto simp: arctan le_less eventually_at dist_real_def simp del: less_divide_eq_numeral1
--- a/src/HOL/ex/Radix_Sort.thy	Fri Feb 23 15:07:30 2018 +0100
+++ b/src/HOL/ex/Radix_Sort.thy	Fri Feb 23 15:17:51 2018 +0100
@@ -2,27 +2,42 @@
 
 theory Radix_Sort
 imports
-  "HOL-Library.Multiset" 
   "HOL-Library.List_lexord" 
   "HOL-Library.Sublist" 
+  "HOL-Library.Multiset" 
+begin
+
+locale Radix_Sort =
+fixes sort1 :: "('a list \<Rightarrow> 'a::linorder) \<Rightarrow> 'a list list \<Rightarrow> 'a list list"
+assumes sorted: "sorted (map f (sort1 f xs))"
+assumes mset: "mset (sort1 f xs) = mset xs"
+assumes stable: "stable_sort_key sort1"
 begin
 
-fun radix_sort :: "nat \<Rightarrow> 'a::linorder list list \<Rightarrow> 'a list list" where
+lemma set_sort1[simp]: "set(sort1 f xs) = set xs"
+by (metis mset set_mset_mset)
+
+abbreviation "sort_col i xss \<equiv> sort1 (\<lambda>xs. xs ! i) xss"
+abbreviation "sorted_col i xss \<equiv> sorted (map (\<lambda>xs. xs ! i) xss)"
+
+fun radix_sort :: "nat \<Rightarrow> 'a list list \<Rightarrow> 'a list list" where
 "radix_sort 0 xss = xss" |
-"radix_sort (Suc n) xss = radix_sort n (sort_key (\<lambda>xs. xs ! n) xss)"
+"radix_sort (Suc i) xss = radix_sort i (sort_col i xss)"
+
+lemma mset_radix_sort: "mset (radix_sort i xss) = mset xss"
+by(induction i arbitrary: xss) (auto simp: mset)
 
 abbreviation "sorted_from i xss \<equiv> sorted (map (drop i) xss)"
 
-definition "cols xss k = (\<forall>xs \<in> set xss. length xs = k)"
+definition "cols xss n = (\<forall>xs \<in> set xss. length xs = n)"
 
-lemma mset_radix_sort: "mset (radix_sort k xss) = mset xss"
-by(induction k arbitrary: xss) (auto)
-
-lemma cols_sort_key: "cols xss n \<Longrightarrow> cols (sort_key f xss) n"
+lemma cols_sort1: "cols xss n \<Longrightarrow> cols (sort1 f xss) n"
 by(simp add: cols_def)
 
-lemma sorted_from_Suc2: "\<lbrakk> cols xss n; i < n;
-  sorted (map (\<lambda>xs. xs!i) xss);  \<forall>xs \<in> set xss. sorted_from (i+1) [ys \<leftarrow> xss. ys!i = xs!i] \<rbrakk>
+lemma sorted_from_Suc2:
+  "\<lbrakk> cols xss n; i < n;
+    sorted_col i xss;
+    \<And>x. sorted_from (i+1) [ys \<leftarrow> xss. ys!i = x] \<rbrakk>
   \<Longrightarrow> sorted_from i xss"
 proof(induction xss rule: induct_list012)
   case 1 show ?case by simp
@@ -36,7 +51,8 @@
   proof -
     have "drop i xs1 = xs1!i # drop (i+1) xs1"
       using \<open>i < n\<close> by (simp add: Cons_nth_drop_Suc lxs1)
-    also have "\<dots> \<le> xs2!i # drop (i+1) xs2" using "3.prems"(3,4) by(auto)
+    also have "\<dots> \<le> xs2!i # drop (i+1) xs2"
+      using "3.prems"(3) "3.prems"(4)[of "xs2!i"] by(auto)
     also have "\<dots> = drop i xs2"
       using \<open>i < n\<close> by (simp add: Cons_nth_drop_Suc lxs2)
     finally show ?thesis .
@@ -44,8 +60,8 @@
   have "sorted_from i (xs2 # xss)"
   proof(rule "3.IH"[OF _ "3.prems"(2)])
     show "cols (xs2 # xss) n" using "3.prems"(1) by(simp add: cols_def)
-    show "sorted (map (\<lambda>xs. xs ! i) (xs2 # xss))" using "3.prems"(3) by simp
-    show "\<forall>xs\<in>set (xs2 # xss). sorted_from (i+1) [ys\<leftarrow>xs2 # xss . ys ! i = xs ! i]"
+    show "sorted_col i (xs2 # xss)" using "3.prems"(3) by simp
+    show "\<And>x. sorted_from (i+1) [ys\<leftarrow>xs2 # xss . ys ! i = x]"
       using "3.prems"(4)
         sorted_antimono_suffix[OF map_mono_suffix[OF filter_mono_suffix[OF suffix_ConsI[OF suffix_order.order.refl]]]]
       by fastforce
@@ -54,21 +70,34 @@
 qed
 
 lemma sorted_from_radix_sort_step:
-  "\<lbrakk> cols xss n; i < n; sorted_from (Suc i) xss \<rbrakk> \<Longrightarrow> sorted_from i (sort_key (\<lambda>xs. xs ! i) xss)"
-apply (rule sorted_from_Suc2)
-apply (auto simp add: sort_key_stable[of _ xss "%xs. xs!i"] sorted_filter cols_def)
-done
+assumes "cols xss n" and "i < n" and "sorted_from (i+1) xss"
+shows "sorted_from i (sort_col i xss)"
+proof (rule sorted_from_Suc2[OF cols_sort1[OF assms(1)] assms(2)])
+  show "sorted_col i (sort_col i xss)" by(simp add: sorted)
+  fix x show "sorted_from (i+1) [ys \<leftarrow> sort_col i xss . ys ! i = x]"
+  proof -
+    from assms(3)
+    have "sorted_from (i+1) (filter (\<lambda>ys. ys!i = x) xss)"
+      by(rule sorted_filter)
+    thus "sorted (map (drop (i+1)) (filter (\<lambda>ys. ys!i = x) (sort_col i xss)))"
+      by (metis stable stable_sort_key_def)
+  qed
+qed
 
 lemma sorted_from_radix_sort:
-  "cols xss n \<Longrightarrow> i \<le> n \<Longrightarrow> sorted_from i xss \<Longrightarrow> sorted_from 0 (radix_sort i xss)"
-apply(induction i arbitrary: xss)
- apply(simp add: sort_key_const)
-apply(simp add: sorted_from_radix_sort_step cols_sort_key)
-done
+  "\<lbrakk> cols xss n;  i \<le> n;  sorted_from i xss \<rbrakk> \<Longrightarrow> sorted_from 0 (radix_sort i xss)"
+proof(induction i arbitrary: xss)
+  case 0 thus ?case by simp
+next
+  case (Suc i)
+  thus ?case by(simp add: sorted_from_radix_sort_step cols_sort1)
+qed
 
-lemma sorted_radix_sort: "cols xss n \<Longrightarrow> sorted (radix_sort n xss)"
+corollary sorted_radix_sort: "cols xss n \<Longrightarrow> sorted (radix_sort n xss)"
 apply(frule sorted_from_radix_sort[OF _ le_refl])
  apply(auto simp add: cols_def sorted_equals_nth_mono)
 done
 
 end
+
+end