# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1493305140 -3600
# Node ID 16a8991ab39879f776fcdbe9287d724d69162aa6
# Parent  91e451bc0f1f354995b4b9291cfb762d001446c1
New material (and some tidying) purely in the Analysis directory

diff -r 91e451bc0f1f -r 16a8991ab398 src/HOL/Analysis/Cauchy_Integral_Theorem.thy
--- a/src/HOL/Analysis/Cauchy_Integral_Theorem.thy	Thu Apr 27 11:06:47 2017 +0100
+++ b/src/HOL/Analysis/Cauchy_Integral_Theorem.thy	Thu Apr 27 15:59:00 2017 +0100
@@ -831,7 +831,7 @@
     apply (drule has_integral_affinity01 [where m= "-1" and c=1])
     apply (auto simp: reversepath_def valid_path_def piecewise_C1_differentiable_on_def)
     apply (drule has_integral_neg)
-    apply (rule_tac s = "(\<lambda>x. 1 - x) ` s" in has_integral_spike_finite)
+    apply (rule_tac S = "(\<lambda>x. 1 - x) ` s" in has_integral_spike_finite)
     apply (auto simp: *)
     done
 qed
@@ -1114,7 +1114,7 @@
   have "((\<lambda>x. f (shiftpath a g x) * vector_derivative (shiftpath a g) (at x))
         has_integral  integral {a..1} (\<lambda>x. f (g x) * vector_derivative g (at x)))  {0..1 - a}"
     apply (rule has_integral_spike_finite
-             [where s = "{1-a} \<union> (\<lambda>x. x-a) ` s" and f = "\<lambda>x. f(g(a+x)) * vector_derivative g (at(a+x))"])
+             [where S = "{1-a} \<union> (\<lambda>x. x-a) ` s" and f = "\<lambda>x. f(g(a+x)) * vector_derivative g (at(a+x))"])
       using s apply blast
      using a apply (auto simp: algebra_simps vd1)
      apply (force simp: shiftpath_def add.commute)
@@ -1125,7 +1125,7 @@
   have "((\<lambda>x. f (shiftpath a g x) * vector_derivative (shiftpath a g) (at x))
         has_integral  integral {0..a} (\<lambda>x. f (g x) * vector_derivative g (at x)))  {1 - a..1}"
     apply (rule has_integral_spike_finite
-             [where s = "{1-a} \<union> (\<lambda>x. x-a+1) ` s" and f = "\<lambda>x. f(g(a+x-1)) * vector_derivative g (at(a+x-1))"])
+             [where S = "{1-a} \<union> (\<lambda>x. x-a+1) ` s" and f = "\<lambda>x. f(g(a+x-1)) * vector_derivative g (at(a+x-1))"])
       using s apply blast
      using a apply (auto simp: algebra_simps vd2)
      apply (force simp: shiftpath_def add.commute)
@@ -1324,7 +1324,7 @@
     apply (cut_tac has_integral_cmul [OF *, where c = "v-u"])
     using fs assms
     apply (simp add: False subpath_def has_contour_integral)
-    apply (rule_tac s = "(\<lambda>t. ((v-u) *\<^sub>R t + u)) -` s" in has_integral_spike_finite)
+    apply (rule_tac S = "(\<lambda>t. ((v-u) *\<^sub>R t + u)) -` s" in has_integral_spike_finite)
     apply (auto simp: inj_on_def False finite_vimageI vd scaleR_conv_of_real)
     done
 qed
@@ -3543,6 +3543,63 @@
   apply (force simp: algebra_simps)
   done
 
+subsubsection\<open>Some lemmas about negating a path.\<close>
+
+lemma valid_path_negatepath: "valid_path \<gamma> \<Longrightarrow> valid_path (uminus \<circ> \<gamma>)"
+   unfolding o_def using piecewise_C1_differentiable_neg valid_path_def by blast
+
+lemma has_contour_integral_negatepath:
+  assumes \<gamma>: "valid_path \<gamma>" and cint: "((\<lambda>z. f (- z)) has_contour_integral - i) \<gamma>"
+  shows "(f has_contour_integral i) (uminus \<circ> \<gamma>)"
+proof -
+  obtain S where cont: "continuous_on {0..1} \<gamma>" and "finite S" and diff: "\<gamma> C1_differentiable_on {0..1} - S"
+    using \<gamma> by (auto simp: valid_path_def piecewise_C1_differentiable_on_def)
+  have "((\<lambda>x. - (f (- \<gamma> x) * vector_derivative \<gamma> (at x within {0..1}))) has_integral i) {0..1}"
+    using cint by (auto simp: has_contour_integral_def dest: has_integral_neg)
+  then
+  have "((\<lambda>x. f (- \<gamma> x) * vector_derivative (uminus \<circ> \<gamma>) (at x within {0..1})) has_integral i) {0..1}"
+  proof (rule rev_iffD1 [OF _ has_integral_spike_eq])
+    show "negligible S"
+      by (simp add: \<open>finite S\<close> negligible_finite)
+    show "f (- \<gamma> x) * vector_derivative (uminus \<circ> \<gamma>) (at x within {0..1}) =
+         - (f (- \<gamma> x) * vector_derivative \<gamma> (at x within {0..1}))"
+      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)
+        using that
+          apply (auto simp: o_def)
+        apply (rule has_vector_derivative_minus)
+        by (metis C1_differentiable_on_def diff has_vector_derivative_at_within that vector_derivative_at_within_ivl zero_less_one)
+      then show ?thesis
+        by simp
+    qed
+  qed
+  then show ?thesis by (simp add: has_contour_integral_def)
+qed
+
+lemma winding_number_negatepath:
+  assumes \<gamma>: "valid_path \<gamma>" and 0: "0 \<notin> path_image \<gamma>"
+  shows "winding_number(uminus \<circ> \<gamma>) 0 = winding_number \<gamma> 0"
+proof -
+  have "op / 1 contour_integrable_on \<gamma>"
+    using "0" \<gamma> contour_integrable_inversediff by fastforce
+  then have "((\<lambda>z. 1/z) has_contour_integral contour_integral \<gamma> (op / 1)) \<gamma>"
+    by (rule has_contour_integral_integral)
+  then have "((\<lambda>z. 1 / - z) has_contour_integral - contour_integral \<gamma> (op / 1)) \<gamma>"
+    using has_contour_integral_neg by auto
+  then show ?thesis
+    using assms
+    apply (simp add: winding_number_valid_path valid_path_negatepath image_def path_defs)
+    apply (simp add: contour_integral_unique has_contour_integral_negatepath)
+    done
+qed
+
+lemma contour_integrable_negatepath:
+  assumes \<gamma>: "valid_path \<gamma>" and pi: "(\<lambda>z. f (- z)) contour_integrable_on \<gamma>"
+  shows "f contour_integrable_on (uminus \<circ> \<gamma>)"
+  by (metis \<gamma> add.inverse_inverse contour_integrable_on_def has_contour_integral_negatepath pi)
+
 (* A combined theorem deducing several things piecewise.*)
 lemma winding_number_join_pos_combined:
      "\<lbrakk>valid_path \<gamma>1; z \<notin> path_image \<gamma>1; 0 < Re(winding_number \<gamma>1 z);
@@ -3551,7 +3608,7 @@
   by (simp add: valid_path_join path_image_join winding_number_join valid_path_imp_path)
 
 
-(* Useful sufficient conditions for the winding number to be positive etc.*)
+subsubsection\<open>Useful sufficient conditions for the winding number to be positive\<close>
 
 lemma Re_winding_number:
     "\<lbrakk>valid_path \<gamma>; z \<notin> path_image \<gamma>\<rbrakk>
@@ -5589,13 +5646,13 @@
     "\<lbrakk>f holomorphic_on s; open s\<rbrakk> \<Longrightarrow> (deriv f) holomorphic_on s"
 by (metis DERIV_deriv_iff_field_differentiable at_within_open derivative_is_holomorphic holomorphic_on_def)
 
-lemma analytic_deriv: "f analytic_on s \<Longrightarrow> (deriv f) analytic_on s"
+lemma analytic_deriv [analytic_intros]: "f analytic_on s \<Longrightarrow> (deriv f) analytic_on s"
   using analytic_on_holomorphic holomorphic_deriv by auto
 
 lemma holomorphic_higher_deriv [holomorphic_intros]: "\<lbrakk>f holomorphic_on s; open s\<rbrakk> \<Longrightarrow> (deriv ^^ n) f holomorphic_on s"
   by (induction n) (auto simp: holomorphic_deriv)
 
-lemma analytic_higher_deriv: "f analytic_on s \<Longrightarrow> (deriv ^^ n) f analytic_on s"
+lemma analytic_higher_deriv [analytic_intros]: "f analytic_on s \<Longrightarrow> (deriv ^^ n) f analytic_on s"
   unfolding analytic_on_def using holomorphic_higher_deriv by blast
 
 lemma has_field_derivative_higher_deriv:
diff -r 91e451bc0f1f -r 16a8991ab398 src/HOL/Analysis/Complex_Analysis_Basics.thy
--- a/src/HOL/Analysis/Complex_Analysis_Basics.thy	Thu Apr 27 11:06:47 2017 +0100
+++ b/src/HOL/Analysis/Complex_Analysis_Basics.thy	Thu Apr 27 15:59:00 2017 +0100
@@ -482,6 +482,8 @@
   where
    "f analytic_on s \<equiv> \<forall>x \<in> s. \<exists>e. 0 < e \<and> f holomorphic_on (ball x e)"
 
+named_theorems analytic_intros "introduction rules for proving analyticity"
+
 lemma analytic_imp_holomorphic: "f analytic_on s \<Longrightarrow> f holomorphic_on s"
   by (simp add: at_within_open [OF _ open_ball] analytic_on_def holomorphic_on_def)
      (metis centre_in_ball field_differentiable_at_within)
@@ -531,16 +533,16 @@
   finally show ?thesis .
 qed
 
-lemma analytic_on_linear: "(op * c) analytic_on s"
-  by (auto simp add: analytic_on_holomorphic holomorphic_on_linear)
+lemma analytic_on_linear [analytic_intros,simp]: "(op * c) analytic_on s"
+  by (auto simp add: analytic_on_holomorphic)
 
-lemma analytic_on_const: "(\<lambda>z. c) analytic_on s"
+lemma analytic_on_const [analytic_intros,simp]: "(\<lambda>z. c) analytic_on s"
   by (metis analytic_on_def holomorphic_on_const zero_less_one)
 
-lemma analytic_on_ident: "(\<lambda>x. x) analytic_on s"
-  by (simp add: analytic_on_def holomorphic_on_ident gt_ex)
+lemma analytic_on_ident [analytic_intros,simp]: "(\<lambda>x. x) analytic_on s"
+  by (simp add: analytic_on_def gt_ex)
 
-lemma analytic_on_id: "id analytic_on s"
+lemma analytic_on_id [analytic_intros]: "id analytic_on s"
   unfolding id_def by (rule analytic_on_ident)
 
 lemma analytic_on_compose:
@@ -572,11 +574,11 @@
              \<Longrightarrow> g o f analytic_on s"
 by (metis analytic_on_compose analytic_on_subset image_subset_iff)
 
-lemma analytic_on_neg:
+lemma analytic_on_neg [analytic_intros]:
   "f analytic_on s \<Longrightarrow> (\<lambda>z. -(f z)) analytic_on s"
 by (metis analytic_on_holomorphic holomorphic_on_minus)
 
-lemma analytic_on_add:
+lemma analytic_on_add [analytic_intros]:
   assumes f: "f analytic_on s"
       and g: "g analytic_on s"
     shows "(\<lambda>z. f z + g z) analytic_on s"
@@ -596,7 +598,7 @@
     by (metis e e' min_less_iff_conj)
 qed
 
-lemma analytic_on_diff:
+lemma analytic_on_diff [analytic_intros]:
   assumes f: "f analytic_on s"
       and g: "g analytic_on s"
     shows "(\<lambda>z. f z - g z) analytic_on s"
@@ -616,7 +618,7 @@
     by (metis e e' min_less_iff_conj)
 qed
 
-lemma analytic_on_mult:
+lemma analytic_on_mult [analytic_intros]:
   assumes f: "f analytic_on s"
       and g: "g analytic_on s"
     shows "(\<lambda>z. f z * g z) analytic_on s"
@@ -636,7 +638,7 @@
     by (metis e e' min_less_iff_conj)
 qed
 
-lemma analytic_on_inverse:
+lemma analytic_on_inverse [analytic_intros]:
   assumes f: "f analytic_on s"
       and nz: "(\<And>z. z \<in> s \<Longrightarrow> f z \<noteq> 0)"
     shows "(\<lambda>z. inverse (f z)) analytic_on s"
@@ -658,7 +660,7 @@
     by (metis e e' min_less_iff_conj)
 qed
 
-lemma analytic_on_divide:
+lemma analytic_on_divide [analytic_intros]:
   assumes f: "f analytic_on s"
       and g: "g analytic_on s"
       and nz: "(\<And>z. z \<in> s \<Longrightarrow> g z \<noteq> 0)"
@@ -666,11 +668,11 @@
 unfolding divide_inverse
 by (metis analytic_on_inverse analytic_on_mult f g nz)
 
-lemma analytic_on_power:
+lemma analytic_on_power [analytic_intros]:
   "f analytic_on s \<Longrightarrow> (\<lambda>z. (f z) ^ n) analytic_on s"
-by (induct n) (auto simp: analytic_on_const analytic_on_mult)
+by (induct n) (auto simp: analytic_on_mult)
 
-lemma analytic_on_sum:
+lemma analytic_on_sum [analytic_intros]:
   "(\<And>i. i \<in> I \<Longrightarrow> (f i) analytic_on s) \<Longrightarrow> (\<lambda>x. sum (\<lambda>i. f i x) I) analytic_on s"
   by (induct I rule: infinite_finite_induct) (auto simp: analytic_on_const analytic_on_add)
 
diff -r 91e451bc0f1f -r 16a8991ab398 src/HOL/Analysis/Complex_Transcendental.thy
--- a/src/HOL/Analysis/Complex_Transcendental.thy	Thu Apr 27 11:06:47 2017 +0100
+++ b/src/HOL/Analysis/Complex_Transcendental.thy	Thu Apr 27 15:59:00 2017 +0100
@@ -1401,7 +1401,7 @@
         Im_Ln_eq_pi [of z] Im_Ln_pos_lt [of z] Re_Ln_pos_le [of z]
   by (simp add: Ln_times) auto
 
-lemma Ln_of_nat: "0 < n \<Longrightarrow> Ln (of_nat n) = of_real (ln (of_nat n))"
+lemma Ln_of_nat [simp]: "0 < n \<Longrightarrow> Ln (of_nat n) = of_real (ln (of_nat n))"
   by (subst of_real_of_nat_eq[symmetric], subst Ln_of_real[symmetric]) simp_all
 
 lemma Ln_of_nat_over_of_nat:
@@ -1936,14 +1936,13 @@
 qed
 
 lemma lim_Ln_over_n: "((\<lambda>n. Ln(of_nat n) / of_nat n) \<longlongrightarrow> 0) sequentially"
-  using lim_Ln_over_power [of 1]
-  by simp
-
-lemma Ln_Reals_eq: "x \<in> \<real> \<Longrightarrow> Re x > 0 \<Longrightarrow> Ln x = of_real (ln (Re x))"
+  using lim_Ln_over_power [of 1] by simp
+
+lemma Ln_Reals_eq: "\<lbrakk>x \<in> \<real>; Re x > 0\<rbrakk> \<Longrightarrow> Ln x = of_real (ln (Re x))"
   using Ln_of_real by force
 
-lemma powr_Reals_eq: "x \<in> \<real> \<Longrightarrow> Re x > 0 \<Longrightarrow> x powr complex_of_real y = of_real (x powr y)"
-  by (simp add: powr_of_real)
+lemma powr_Reals_eq: "\<lbrakk>x \<in> \<real>; y \<in> \<real>; Re x > 0\<rbrakk> \<Longrightarrow> x powr y = of_real (Re x powr Re y)"
+  by (metis linear not_le of_real_Re powr_of_real)
 
 lemma lim_ln_over_power:
   fixes s :: real
diff -r 91e451bc0f1f -r 16a8991ab398 src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy
--- a/src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy	Thu Apr 27 11:06:47 2017 +0100
+++ b/src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy	Thu Apr 27 15:59:00 2017 +0100
@@ -683,7 +683,7 @@
     by (simp add: AE_iff_measurable)
   show ?thesis
   proof (rule has_integral_spike_eq[symmetric])
-    show "\<forall>x\<in>\<Omega> - N. f x = g x" using N(3) by auto
+    show "\<And>x. x\<in>\<Omega> - N \<Longrightarrow> f x = g x" using N(3) by auto
     show "negligible N"
       unfolding negligible_def
     proof (intro allI)
@@ -2246,7 +2246,7 @@
   proof
     show "(\<lambda>x. norm (g x)) integrable_on s"
       using le norm_ge_zero[of "f _"]
-      by (intro integrable_spike_finite[OF _ _ g, where s="{}"])
+      by (intro integrable_spike_finite[OF _ _ g, of "{}"])
          (auto intro!: abs_of_nonneg intro: order_trans simp del: norm_ge_zero)
   qed fact
   show "set_borel_measurable lebesgue s f"
@@ -2266,9 +2266,9 @@
     unfolding absolutely_integrable_on_def
   proof
     show "(\<lambda>x. norm (h x)) integrable_on s"
-    proof (intro integrable_spike_finite[OF _ _ h, where s="{}"] ballI)
+    proof (intro integrable_spike_finite[OF _ _ h, of "{}"] ballI)
       fix x assume "x \<in> s - {}" then show "norm (h x) = h x"
-        using order_trans[OF norm_ge_zero le[THEN bspec, of x]] by auto
+        by (metis Diff_empty abs_of_nonneg bot_set_def le norm_ge_zero order_trans real_norm_def)
     qed auto
   qed fact
   have 2: "set_borel_measurable lebesgue s (f k)" for k
diff -r 91e451bc0f1f -r 16a8991ab398 src/HOL/Analysis/Gamma_Function.thy
--- a/src/HOL/Analysis/Gamma_Function.thy	Thu Apr 27 11:06:47 2017 +0100
+++ b/src/HOL/Analysis/Gamma_Function.thy	Thu Apr 27 15:59:00 2017 +0100
@@ -2785,7 +2785,7 @@
       by (intro has_integral_spike_finite_eq[of "{0}"]) (simp_all add: powr_def Ln_of_real)
     also have "fact n * of_nat n / pochhammer z (n+1) * exp ((z - 1) * Ln (of_nat n)) =
                  (of_nat n powr z * fact n / pochhammer z (n+1))"
-      by (auto simp add: powr_def algebra_simps exp_diff)
+      by (auto simp add: powr_def algebra_simps exp_diff exp_of_real)
     finally show ?thesis by (subst has_integral_restrict) simp_all
   next
     case False
diff -r 91e451bc0f1f -r 16a8991ab398 src/HOL/Analysis/Henstock_Kurzweil_Integration.thy
--- a/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy	Thu Apr 27 11:06:47 2017 +0100
+++ b/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy	Thu Apr 27 15:59:00 2017 +0100
@@ -2238,78 +2238,50 @@
 
 lemma has_integral_spike:
   fixes f :: "'b::euclidean_space \<Rightarrow> 'a::real_normed_vector"
-  assumes "negligible s"
-    and "(\<forall>x\<in>(t - s). g x = f x)"
-    and "(f has_integral y) t"
-  shows "(g has_integral y) t"
+  assumes "negligible S"
+    and gf: "\<And>x. x \<in> T - S \<Longrightarrow> g x = f x"
+    and fint: "(f has_integral y) T"
+  shows "(g has_integral y) T"
 proof -
-  {
-    fix a b :: 'b
-    fix f g :: "'b \<Rightarrow> 'a"
-    fix y :: 'a
-    assume as: "\<forall>x \<in> cbox a b - s. g x = f x" "(f has_integral y) (cbox a b)"
+  have *: "(g has_integral y) (cbox a b)"
+       if "(f has_integral y) (cbox a b)" "\<forall>x \<in> cbox a b - S. g x = f x" for a b f and g:: "'b \<Rightarrow> 'a" and y
+  proof -
     have "((\<lambda>x. f x + (g x - f x)) has_integral (y + 0)) (cbox a b)"
-      apply (rule has_integral_add[OF as(2)])
-      apply (rule has_integral_negligible[OF assms(1)])
-      using as
-      apply auto
-      done
-    then have "(g has_integral y) (cbox a b)"
+      using that by (intro has_integral_add has_integral_negligible) (auto intro!: \<open>negligible S\<close>)
+    then show ?thesis
       by auto
-  } note * = this
+  qed
   show ?thesis
+    using fint gf
     apply (subst has_integral_alt)
-    using assms(2-)
-    apply -
-    apply (rule cond_cases)
-    apply safe
-    apply (rule *)
-    apply assumption+
-    apply (subst(asm) has_integral_alt)
-    unfolding if_not_P
-    apply (erule_tac x=e in allE)
-    apply safe
-    apply (rule_tac x=B in exI)
-    apply safe
-    apply (erule_tac x=a in allE)
-    apply (erule_tac x=b in allE)
-    apply safe
-    apply (rule_tac x=z in exI)
-    apply safe
-    apply (rule *[where fa2="\<lambda>x. if x\<in>t then f x else 0"])
-    apply auto
+    apply (subst (asm) has_integral_alt)
+    apply (simp add: split: if_split_asm)
+      apply (blast dest: *)
+    apply (elim all_forward imp_forward ex_forward)
+    apply (force dest: *[where f="\<lambda>x. if x\<in>T then f x else 0" and g="\<lambda>x. if x \<in> T then g x else 0"])+
     done
 qed
 
 lemma has_integral_spike_eq:
-  assumes "negligible s"
-    and "\<forall>x\<in>(t - s). g x = f x"
-  shows "((f has_integral y) t \<longleftrightarrow> (g has_integral y) t)"
-  apply rule
-  apply (rule_tac[!] has_integral_spike[OF assms(1)])
-  using assms(2)
-  apply auto
-  done
+  assumes "negligible S"
+    and gf: "\<And>x. x \<in> T - S \<Longrightarrow> g x = f x"
+  shows "(f has_integral y) T \<longleftrightarrow> (g has_integral y) T"
+    using has_integral_spike [OF \<open>negligible S\<close>] gf
+    by metis
 
 lemma integrable_spike:
-  assumes "negligible s"
-    and "\<forall>x\<in>(t - s). g x = f x"
-    and "f integrable_on t"
-  shows "g integrable_on  t"
-  using assms
-  unfolding integrable_on_def
-  apply -
-  apply (erule exE)
-  apply rule
-  apply (rule has_integral_spike)
-  apply fastforce+
-  done
+  assumes "negligible S"
+    and "\<And>x. x \<in> T - S \<Longrightarrow> g x = f x"
+    and "f integrable_on T"
+  shows "g integrable_on T"
+  using assms unfolding integrable_on_def by (blast intro: has_integral_spike)
 
 lemma integral_spike:
-  assumes "negligible s"
-    and "\<forall>x\<in>(t - s). g x = f x"
-  shows "integral t f = integral t g"
-  using has_integral_spike_eq[OF assms] by (simp add: integral_def integrable_on_def)
+  assumes "negligible S"
+    and "\<And>x. x \<in> T - S \<Longrightarrow> g x = f x"
+  shows "integral T f = integral T g"
+  using has_integral_spike_eq[OF assms]
+    by (auto simp: integral_def integrable_on_def)
 
 
 subsection \<open>Some other trivialities about negligible sets.\<close>
@@ -2337,7 +2309,7 @@
   unfolding negligible_def
 proof (safe, goal_cases)
   case (1 a b)
-  note assm = assms[unfolded negligible_def,rule_format,of a b]
+  note assms[unfolded negligible_def,rule_format,of a b]
   then show ?case
     apply (subst has_integral_spike_eq[OF assms(2)])
     defer
@@ -2405,37 +2377,24 @@
 subsection \<open>Finite case of the spike theorem is quite commonly needed.\<close>
 
 lemma has_integral_spike_finite:
-  assumes "finite s"
-    and "\<forall>x\<in>t-s. g x = f x"
-    and "(f has_integral y) t"
-  shows "(g has_integral y) t"
-  apply (rule has_integral_spike)
-  using assms
-  apply auto
-  done
+  assumes "finite S"
+    and "\<And>x. x \<in> T - S \<Longrightarrow> g x = f x"
+    and "(f has_integral y) T"
+  shows "(g has_integral y) T"
+  using assms has_integral_spike negligible_finite by blast
 
 lemma has_integral_spike_finite_eq:
-  assumes "finite s"
-    and "\<forall>x\<in>t-s. g x = f x"
-  shows "((f has_integral y) t \<longleftrightarrow> (g has_integral y) t)"
-  apply rule
-  apply (rule_tac[!] has_integral_spike_finite)
-  using assms
-  apply auto
-  done
+  assumes "finite S"
+    and "\<And>x. x \<in> T - S \<Longrightarrow> g x = f x"
+  shows "((f has_integral y) T \<longleftrightarrow> (g has_integral y) T)"
+  by (metis assms has_integral_spike_finite)
 
 lemma integrable_spike_finite:
-  assumes "finite s"
-    and "\<forall>x\<in>t-s. g x = f x"
-    and "f integrable_on t"
-  shows "g integrable_on  t"
-  using assms
-  unfolding integrable_on_def
-  apply safe
-  apply (rule_tac x=y in exI)
-  apply (rule has_integral_spike_finite)
-  apply auto
-  done
+  assumes "finite S"
+    and "\<And>x. x \<in> T - S \<Longrightarrow> g x = f x"
+    and "f integrable_on T"
+  shows "g integrable_on T"
+  using assms has_integral_spike_finite by blast
 
 
 subsection \<open>In particular, the boundary of an interval is negligible.\<close>
diff -r 91e451bc0f1f -r 16a8991ab398 src/HOL/Analysis/Topology_Euclidean_Space.thy
--- a/src/HOL/Analysis/Topology_Euclidean_Space.thy	Thu Apr 27 11:06:47 2017 +0100
+++ b/src/HOL/Analysis/Topology_Euclidean_Space.thy	Thu Apr 27 15:59:00 2017 +0100
@@ -1265,6 +1265,11 @@
 lemma cbox_Pair_iff [iff]: "(x, y) \<in> cbox (a, c) (b, d) \<longleftrightarrow> x \<in> cbox a b \<and> y \<in> cbox c d"
   by (force simp: cbox_Pair_eq)
 
+lemma cbox_Complex_eq: "cbox (Complex a c) (Complex b d) = (\<lambda>(x,y). Complex x y) ` (cbox a b \<times> cbox c d)"
+  apply (auto simp: cbox_def Basis_complex_def)
+  apply (rule_tac x = "(Re x, Im x)" in image_eqI)
+  using complex_eq by auto
+
 lemma cbox_Pair_eq_0: "cbox (a, c) (b, d) = {} \<longleftrightarrow> cbox a b = {} \<or> cbox c d = {}"
   by (force simp: cbox_Pair_eq)
 
@@ -3916,19 +3921,6 @@
 lemma bounded_subset_cball: "bounded S \<longleftrightarrow> (\<exists>e x. S \<subseteq> cball x e \<and> 0 \<le> e)"
   unfolding bounded_def subset_eq  by auto (meson order_trans zero_le_dist)
 
-lemma bounded_subset_ballD:
-  assumes "bounded S" shows "\<exists>r. 0 < r \<and> S \<subseteq> ball x r"
-proof -
-  obtain e::real and y where "S \<subseteq> cball y e"  "0 \<le> e"
-    using assms by (auto simp: bounded_subset_cball)
-  then show ?thesis
-    apply (rule_tac x="dist x y + e + 1" in exI)
-    apply (simp add: add.commute add_pos_nonneg)
-    apply (erule subset_trans)
-    apply (clarsimp simp add: cball_def)
-    by (metis add_le_cancel_right add_strict_increasing dist_commute dist_triangle_le zero_less_one)
-qed
-
 lemma bounded_any_center: "bounded S \<longleftrightarrow> (\<exists>e. \<forall>y\<in>S. dist a y \<le> e)"
   unfolding bounded_def
   by auto (metis add.commute add_le_cancel_right dist_commute dist_triangle_le)
@@ -4014,6 +4006,22 @@
     by (metis insert_is_Un bounded_Un)
 qed
 
+lemma bounded_subset_ballI: "S \<subseteq> ball x r \<Longrightarrow> bounded S"
+  by (meson bounded_ball bounded_subset)
+
+lemma bounded_subset_ballD:
+  assumes "bounded S" shows "\<exists>r. 0 < r \<and> S \<subseteq> ball x r"
+proof -
+  obtain e::real and y where "S \<subseteq> cball y e"  "0 \<le> e"
+    using assms by (auto simp: bounded_subset_cball)
+  then show ?thesis
+    apply (rule_tac x="dist x y + e + 1" in exI)
+    apply (simp add: add.commute add_pos_nonneg)
+    apply (erule subset_trans)
+    apply (clarsimp simp add: cball_def)
+    by (metis add_le_cancel_right add_strict_increasing dist_commute dist_triangle_le zero_less_one)
+qed
+
 lemma finite_imp_bounded [intro]: "finite S \<Longrightarrow> bounded S"
   by (induct set: finite) simp_all