New material (and some tidying) purely in the Analysis directory
authorpaulson <lp15@cam.ac.uk>
Thu Apr 27 15:59:00 2017 +0100 (2017-04-27)
changeset 6558716a8991ab398
parent 65586 91e451bc0f1f
child 65634 e85004302c83
New material (and some tidying) purely in the Analysis directory
src/HOL/Analysis/Cauchy_Integral_Theorem.thy
src/HOL/Analysis/Complex_Analysis_Basics.thy
src/HOL/Analysis/Complex_Transcendental.thy
src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy
src/HOL/Analysis/Gamma_Function.thy
src/HOL/Analysis/Henstock_Kurzweil_Integration.thy
src/HOL/Analysis/Topology_Euclidean_Space.thy
     1.1 --- a/src/HOL/Analysis/Cauchy_Integral_Theorem.thy	Thu Apr 27 11:06:47 2017 +0100
     1.2 +++ b/src/HOL/Analysis/Cauchy_Integral_Theorem.thy	Thu Apr 27 15:59:00 2017 +0100
     1.3 @@ -831,7 +831,7 @@
     1.4      apply (drule has_integral_affinity01 [where m= "-1" and c=1])
     1.5      apply (auto simp: reversepath_def valid_path_def piecewise_C1_differentiable_on_def)
     1.6      apply (drule has_integral_neg)
     1.7 -    apply (rule_tac s = "(\<lambda>x. 1 - x) ` s" in has_integral_spike_finite)
     1.8 +    apply (rule_tac S = "(\<lambda>x. 1 - x) ` s" in has_integral_spike_finite)
     1.9      apply (auto simp: *)
    1.10      done
    1.11  qed
    1.12 @@ -1114,7 +1114,7 @@
    1.13    have "((\<lambda>x. f (shiftpath a g x) * vector_derivative (shiftpath a g) (at x))
    1.14          has_integral  integral {a..1} (\<lambda>x. f (g x) * vector_derivative g (at x)))  {0..1 - a}"
    1.15      apply (rule has_integral_spike_finite
    1.16 -             [where s = "{1-a} \<union> (\<lambda>x. x-a) ` s" and f = "\<lambda>x. f(g(a+x)) * vector_derivative g (at(a+x))"])
    1.17 +             [where S = "{1-a} \<union> (\<lambda>x. x-a) ` s" and f = "\<lambda>x. f(g(a+x)) * vector_derivative g (at(a+x))"])
    1.18        using s apply blast
    1.19       using a apply (auto simp: algebra_simps vd1)
    1.20       apply (force simp: shiftpath_def add.commute)
    1.21 @@ -1125,7 +1125,7 @@
    1.22    have "((\<lambda>x. f (shiftpath a g x) * vector_derivative (shiftpath a g) (at x))
    1.23          has_integral  integral {0..a} (\<lambda>x. f (g x) * vector_derivative g (at x)))  {1 - a..1}"
    1.24      apply (rule has_integral_spike_finite
    1.25 -             [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))"])
    1.26 +             [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))"])
    1.27        using s apply blast
    1.28       using a apply (auto simp: algebra_simps vd2)
    1.29       apply (force simp: shiftpath_def add.commute)
    1.30 @@ -1324,7 +1324,7 @@
    1.31      apply (cut_tac has_integral_cmul [OF *, where c = "v-u"])
    1.32      using fs assms
    1.33      apply (simp add: False subpath_def has_contour_integral)
    1.34 -    apply (rule_tac s = "(\<lambda>t. ((v-u) *\<^sub>R t + u)) -` s" in has_integral_spike_finite)
    1.35 +    apply (rule_tac S = "(\<lambda>t. ((v-u) *\<^sub>R t + u)) -` s" in has_integral_spike_finite)
    1.36      apply (auto simp: inj_on_def False finite_vimageI vd scaleR_conv_of_real)
    1.37      done
    1.38  qed
    1.39 @@ -3543,6 +3543,63 @@
    1.40    apply (force simp: algebra_simps)
    1.41    done
    1.42  
    1.43 +subsubsection\<open>Some lemmas about negating a path.\<close>
    1.44 +
    1.45 +lemma valid_path_negatepath: "valid_path \<gamma> \<Longrightarrow> valid_path (uminus \<circ> \<gamma>)"
    1.46 +   unfolding o_def using piecewise_C1_differentiable_neg valid_path_def by blast
    1.47 +
    1.48 +lemma has_contour_integral_negatepath:
    1.49 +  assumes \<gamma>: "valid_path \<gamma>" and cint: "((\<lambda>z. f (- z)) has_contour_integral - i) \<gamma>"
    1.50 +  shows "(f has_contour_integral i) (uminus \<circ> \<gamma>)"
    1.51 +proof -
    1.52 +  obtain S where cont: "continuous_on {0..1} \<gamma>" and "finite S" and diff: "\<gamma> C1_differentiable_on {0..1} - S"
    1.53 +    using \<gamma> by (auto simp: valid_path_def piecewise_C1_differentiable_on_def)
    1.54 +  have "((\<lambda>x. - (f (- \<gamma> x) * vector_derivative \<gamma> (at x within {0..1}))) has_integral i) {0..1}"
    1.55 +    using cint by (auto simp: has_contour_integral_def dest: has_integral_neg)
    1.56 +  then
    1.57 +  have "((\<lambda>x. f (- \<gamma> x) * vector_derivative (uminus \<circ> \<gamma>) (at x within {0..1})) has_integral i) {0..1}"
    1.58 +  proof (rule rev_iffD1 [OF _ has_integral_spike_eq])
    1.59 +    show "negligible S"
    1.60 +      by (simp add: \<open>finite S\<close> negligible_finite)
    1.61 +    show "f (- \<gamma> x) * vector_derivative (uminus \<circ> \<gamma>) (at x within {0..1}) =
    1.62 +         - (f (- \<gamma> x) * vector_derivative \<gamma> (at x within {0..1}))"
    1.63 +      if "x \<in> {0..1} - S" for x
    1.64 +    proof -
    1.65 +      have "vector_derivative (uminus \<circ> \<gamma>) (at x within cbox 0 1) = - vector_derivative \<gamma> (at x within cbox 0 1)"
    1.66 +        apply (rule vector_derivative_within_closed_interval)
    1.67 +        using that
    1.68 +          apply (auto simp: o_def)
    1.69 +        apply (rule has_vector_derivative_minus)
    1.70 +        by (metis C1_differentiable_on_def diff has_vector_derivative_at_within that vector_derivative_at_within_ivl zero_less_one)
    1.71 +      then show ?thesis
    1.72 +        by simp
    1.73 +    qed
    1.74 +  qed
    1.75 +  then show ?thesis by (simp add: has_contour_integral_def)
    1.76 +qed
    1.77 +
    1.78 +lemma winding_number_negatepath:
    1.79 +  assumes \<gamma>: "valid_path \<gamma>" and 0: "0 \<notin> path_image \<gamma>"
    1.80 +  shows "winding_number(uminus \<circ> \<gamma>) 0 = winding_number \<gamma> 0"
    1.81 +proof -
    1.82 +  have "op / 1 contour_integrable_on \<gamma>"
    1.83 +    using "0" \<gamma> contour_integrable_inversediff by fastforce
    1.84 +  then have "((\<lambda>z. 1/z) has_contour_integral contour_integral \<gamma> (op / 1)) \<gamma>"
    1.85 +    by (rule has_contour_integral_integral)
    1.86 +  then have "((\<lambda>z. 1 / - z) has_contour_integral - contour_integral \<gamma> (op / 1)) \<gamma>"
    1.87 +    using has_contour_integral_neg by auto
    1.88 +  then show ?thesis
    1.89 +    using assms
    1.90 +    apply (simp add: winding_number_valid_path valid_path_negatepath image_def path_defs)
    1.91 +    apply (simp add: contour_integral_unique has_contour_integral_negatepath)
    1.92 +    done
    1.93 +qed
    1.94 +
    1.95 +lemma contour_integrable_negatepath:
    1.96 +  assumes \<gamma>: "valid_path \<gamma>" and pi: "(\<lambda>z. f (- z)) contour_integrable_on \<gamma>"
    1.97 +  shows "f contour_integrable_on (uminus \<circ> \<gamma>)"
    1.98 +  by (metis \<gamma> add.inverse_inverse contour_integrable_on_def has_contour_integral_negatepath pi)
    1.99 +
   1.100  (* A combined theorem deducing several things piecewise.*)
   1.101  lemma winding_number_join_pos_combined:
   1.102       "\<lbrakk>valid_path \<gamma>1; z \<notin> path_image \<gamma>1; 0 < Re(winding_number \<gamma>1 z);
   1.103 @@ -3551,7 +3608,7 @@
   1.104    by (simp add: valid_path_join path_image_join winding_number_join valid_path_imp_path)
   1.105  
   1.106  
   1.107 -(* Useful sufficient conditions for the winding number to be positive etc.*)
   1.108 +subsubsection\<open>Useful sufficient conditions for the winding number to be positive\<close>
   1.109  
   1.110  lemma Re_winding_number:
   1.111      "\<lbrakk>valid_path \<gamma>; z \<notin> path_image \<gamma>\<rbrakk>
   1.112 @@ -5589,13 +5646,13 @@
   1.113      "\<lbrakk>f holomorphic_on s; open s\<rbrakk> \<Longrightarrow> (deriv f) holomorphic_on s"
   1.114  by (metis DERIV_deriv_iff_field_differentiable at_within_open derivative_is_holomorphic holomorphic_on_def)
   1.115  
   1.116 -lemma analytic_deriv: "f analytic_on s \<Longrightarrow> (deriv f) analytic_on s"
   1.117 +lemma analytic_deriv [analytic_intros]: "f analytic_on s \<Longrightarrow> (deriv f) analytic_on s"
   1.118    using analytic_on_holomorphic holomorphic_deriv by auto
   1.119  
   1.120  lemma holomorphic_higher_deriv [holomorphic_intros]: "\<lbrakk>f holomorphic_on s; open s\<rbrakk> \<Longrightarrow> (deriv ^^ n) f holomorphic_on s"
   1.121    by (induction n) (auto simp: holomorphic_deriv)
   1.122  
   1.123 -lemma analytic_higher_deriv: "f analytic_on s \<Longrightarrow> (deriv ^^ n) f analytic_on s"
   1.124 +lemma analytic_higher_deriv [analytic_intros]: "f analytic_on s \<Longrightarrow> (deriv ^^ n) f analytic_on s"
   1.125    unfolding analytic_on_def using holomorphic_higher_deriv by blast
   1.126  
   1.127  lemma has_field_derivative_higher_deriv:
     2.1 --- a/src/HOL/Analysis/Complex_Analysis_Basics.thy	Thu Apr 27 11:06:47 2017 +0100
     2.2 +++ b/src/HOL/Analysis/Complex_Analysis_Basics.thy	Thu Apr 27 15:59:00 2017 +0100
     2.3 @@ -482,6 +482,8 @@
     2.4    where
     2.5     "f analytic_on s \<equiv> \<forall>x \<in> s. \<exists>e. 0 < e \<and> f holomorphic_on (ball x e)"
     2.6  
     2.7 +named_theorems analytic_intros "introduction rules for proving analyticity"
     2.8 +
     2.9  lemma analytic_imp_holomorphic: "f analytic_on s \<Longrightarrow> f holomorphic_on s"
    2.10    by (simp add: at_within_open [OF _ open_ball] analytic_on_def holomorphic_on_def)
    2.11       (metis centre_in_ball field_differentiable_at_within)
    2.12 @@ -531,16 +533,16 @@
    2.13    finally show ?thesis .
    2.14  qed
    2.15  
    2.16 -lemma analytic_on_linear: "(op * c) analytic_on s"
    2.17 -  by (auto simp add: analytic_on_holomorphic holomorphic_on_linear)
    2.18 +lemma analytic_on_linear [analytic_intros,simp]: "(op * c) analytic_on s"
    2.19 +  by (auto simp add: analytic_on_holomorphic)
    2.20  
    2.21 -lemma analytic_on_const: "(\<lambda>z. c) analytic_on s"
    2.22 +lemma analytic_on_const [analytic_intros,simp]: "(\<lambda>z. c) analytic_on s"
    2.23    by (metis analytic_on_def holomorphic_on_const zero_less_one)
    2.24  
    2.25 -lemma analytic_on_ident: "(\<lambda>x. x) analytic_on s"
    2.26 -  by (simp add: analytic_on_def holomorphic_on_ident gt_ex)
    2.27 +lemma analytic_on_ident [analytic_intros,simp]: "(\<lambda>x. x) analytic_on s"
    2.28 +  by (simp add: analytic_on_def gt_ex)
    2.29  
    2.30 -lemma analytic_on_id: "id analytic_on s"
    2.31 +lemma analytic_on_id [analytic_intros]: "id analytic_on s"
    2.32    unfolding id_def by (rule analytic_on_ident)
    2.33  
    2.34  lemma analytic_on_compose:
    2.35 @@ -572,11 +574,11 @@
    2.36               \<Longrightarrow> g o f analytic_on s"
    2.37  by (metis analytic_on_compose analytic_on_subset image_subset_iff)
    2.38  
    2.39 -lemma analytic_on_neg:
    2.40 +lemma analytic_on_neg [analytic_intros]:
    2.41    "f analytic_on s \<Longrightarrow> (\<lambda>z. -(f z)) analytic_on s"
    2.42  by (metis analytic_on_holomorphic holomorphic_on_minus)
    2.43  
    2.44 -lemma analytic_on_add:
    2.45 +lemma analytic_on_add [analytic_intros]:
    2.46    assumes f: "f analytic_on s"
    2.47        and g: "g analytic_on s"
    2.48      shows "(\<lambda>z. f z + g z) analytic_on s"
    2.49 @@ -596,7 +598,7 @@
    2.50      by (metis e e' min_less_iff_conj)
    2.51  qed
    2.52  
    2.53 -lemma analytic_on_diff:
    2.54 +lemma analytic_on_diff [analytic_intros]:
    2.55    assumes f: "f analytic_on s"
    2.56        and g: "g analytic_on s"
    2.57      shows "(\<lambda>z. f z - g z) analytic_on s"
    2.58 @@ -616,7 +618,7 @@
    2.59      by (metis e e' min_less_iff_conj)
    2.60  qed
    2.61  
    2.62 -lemma analytic_on_mult:
    2.63 +lemma analytic_on_mult [analytic_intros]:
    2.64    assumes f: "f analytic_on s"
    2.65        and g: "g analytic_on s"
    2.66      shows "(\<lambda>z. f z * g z) analytic_on s"
    2.67 @@ -636,7 +638,7 @@
    2.68      by (metis e e' min_less_iff_conj)
    2.69  qed
    2.70  
    2.71 -lemma analytic_on_inverse:
    2.72 +lemma analytic_on_inverse [analytic_intros]:
    2.73    assumes f: "f analytic_on s"
    2.74        and nz: "(\<And>z. z \<in> s \<Longrightarrow> f z \<noteq> 0)"
    2.75      shows "(\<lambda>z. inverse (f z)) analytic_on s"
    2.76 @@ -658,7 +660,7 @@
    2.77      by (metis e e' min_less_iff_conj)
    2.78  qed
    2.79  
    2.80 -lemma analytic_on_divide:
    2.81 +lemma analytic_on_divide [analytic_intros]:
    2.82    assumes f: "f analytic_on s"
    2.83        and g: "g analytic_on s"
    2.84        and nz: "(\<And>z. z \<in> s \<Longrightarrow> g z \<noteq> 0)"
    2.85 @@ -666,11 +668,11 @@
    2.86  unfolding divide_inverse
    2.87  by (metis analytic_on_inverse analytic_on_mult f g nz)
    2.88  
    2.89 -lemma analytic_on_power:
    2.90 +lemma analytic_on_power [analytic_intros]:
    2.91    "f analytic_on s \<Longrightarrow> (\<lambda>z. (f z) ^ n) analytic_on s"
    2.92 -by (induct n) (auto simp: analytic_on_const analytic_on_mult)
    2.93 +by (induct n) (auto simp: analytic_on_mult)
    2.94  
    2.95 -lemma analytic_on_sum:
    2.96 +lemma analytic_on_sum [analytic_intros]:
    2.97    "(\<And>i. i \<in> I \<Longrightarrow> (f i) analytic_on s) \<Longrightarrow> (\<lambda>x. sum (\<lambda>i. f i x) I) analytic_on s"
    2.98    by (induct I rule: infinite_finite_induct) (auto simp: analytic_on_const analytic_on_add)
    2.99  
     3.1 --- a/src/HOL/Analysis/Complex_Transcendental.thy	Thu Apr 27 11:06:47 2017 +0100
     3.2 +++ b/src/HOL/Analysis/Complex_Transcendental.thy	Thu Apr 27 15:59:00 2017 +0100
     3.3 @@ -1401,7 +1401,7 @@
     3.4          Im_Ln_eq_pi [of z] Im_Ln_pos_lt [of z] Re_Ln_pos_le [of z]
     3.5    by (simp add: Ln_times) auto
     3.6  
     3.7 -lemma Ln_of_nat: "0 < n \<Longrightarrow> Ln (of_nat n) = of_real (ln (of_nat n))"
     3.8 +lemma Ln_of_nat [simp]: "0 < n \<Longrightarrow> Ln (of_nat n) = of_real (ln (of_nat n))"
     3.9    by (subst of_real_of_nat_eq[symmetric], subst Ln_of_real[symmetric]) simp_all
    3.10  
    3.11  lemma Ln_of_nat_over_of_nat:
    3.12 @@ -1936,14 +1936,13 @@
    3.13  qed
    3.14  
    3.15  lemma lim_Ln_over_n: "((\<lambda>n. Ln(of_nat n) / of_nat n) \<longlongrightarrow> 0) sequentially"
    3.16 -  using lim_Ln_over_power [of 1]
    3.17 -  by simp
    3.18 -
    3.19 -lemma Ln_Reals_eq: "x \<in> \<real> \<Longrightarrow> Re x > 0 \<Longrightarrow> Ln x = of_real (ln (Re x))"
    3.20 +  using lim_Ln_over_power [of 1] by simp
    3.21 +
    3.22 +lemma Ln_Reals_eq: "\<lbrakk>x \<in> \<real>; Re x > 0\<rbrakk> \<Longrightarrow> Ln x = of_real (ln (Re x))"
    3.23    using Ln_of_real by force
    3.24  
    3.25 -lemma powr_Reals_eq: "x \<in> \<real> \<Longrightarrow> Re x > 0 \<Longrightarrow> x powr complex_of_real y = of_real (x powr y)"
    3.26 -  by (simp add: powr_of_real)
    3.27 +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)"
    3.28 +  by (metis linear not_le of_real_Re powr_of_real)
    3.29  
    3.30  lemma lim_ln_over_power:
    3.31    fixes s :: real
     4.1 --- a/src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy	Thu Apr 27 11:06:47 2017 +0100
     4.2 +++ b/src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy	Thu Apr 27 15:59:00 2017 +0100
     4.3 @@ -683,7 +683,7 @@
     4.4      by (simp add: AE_iff_measurable)
     4.5    show ?thesis
     4.6    proof (rule has_integral_spike_eq[symmetric])
     4.7 -    show "\<forall>x\<in>\<Omega> - N. f x = g x" using N(3) by auto
     4.8 +    show "\<And>x. x\<in>\<Omega> - N \<Longrightarrow> f x = g x" using N(3) by auto
     4.9      show "negligible N"
    4.10        unfolding negligible_def
    4.11      proof (intro allI)
    4.12 @@ -2246,7 +2246,7 @@
    4.13    proof
    4.14      show "(\<lambda>x. norm (g x)) integrable_on s"
    4.15        using le norm_ge_zero[of "f _"]
    4.16 -      by (intro integrable_spike_finite[OF _ _ g, where s="{}"])
    4.17 +      by (intro integrable_spike_finite[OF _ _ g, of "{}"])
    4.18           (auto intro!: abs_of_nonneg intro: order_trans simp del: norm_ge_zero)
    4.19    qed fact
    4.20    show "set_borel_measurable lebesgue s f"
    4.21 @@ -2266,9 +2266,9 @@
    4.22      unfolding absolutely_integrable_on_def
    4.23    proof
    4.24      show "(\<lambda>x. norm (h x)) integrable_on s"
    4.25 -    proof (intro integrable_spike_finite[OF _ _ h, where s="{}"] ballI)
    4.26 +    proof (intro integrable_spike_finite[OF _ _ h, of "{}"] ballI)
    4.27        fix x assume "x \<in> s - {}" then show "norm (h x) = h x"
    4.28 -        using order_trans[OF norm_ge_zero le[THEN bspec, of x]] by auto
    4.29 +        by (metis Diff_empty abs_of_nonneg bot_set_def le norm_ge_zero order_trans real_norm_def)
    4.30      qed auto
    4.31    qed fact
    4.32    have 2: "set_borel_measurable lebesgue s (f k)" for k
     5.1 --- a/src/HOL/Analysis/Gamma_Function.thy	Thu Apr 27 11:06:47 2017 +0100
     5.2 +++ b/src/HOL/Analysis/Gamma_Function.thy	Thu Apr 27 15:59:00 2017 +0100
     5.3 @@ -2785,7 +2785,7 @@
     5.4        by (intro has_integral_spike_finite_eq[of "{0}"]) (simp_all add: powr_def Ln_of_real)
     5.5      also have "fact n * of_nat n / pochhammer z (n+1) * exp ((z - 1) * Ln (of_nat n)) =
     5.6                   (of_nat n powr z * fact n / pochhammer z (n+1))"
     5.7 -      by (auto simp add: powr_def algebra_simps exp_diff)
     5.8 +      by (auto simp add: powr_def algebra_simps exp_diff exp_of_real)
     5.9      finally show ?thesis by (subst has_integral_restrict) simp_all
    5.10    next
    5.11      case False
     6.1 --- a/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy	Thu Apr 27 11:06:47 2017 +0100
     6.2 +++ b/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy	Thu Apr 27 15:59:00 2017 +0100
     6.3 @@ -2238,78 +2238,50 @@
     6.4  
     6.5  lemma has_integral_spike:
     6.6    fixes f :: "'b::euclidean_space \<Rightarrow> 'a::real_normed_vector"
     6.7 -  assumes "negligible s"
     6.8 -    and "(\<forall>x\<in>(t - s). g x = f x)"
     6.9 -    and "(f has_integral y) t"
    6.10 -  shows "(g has_integral y) t"
    6.11 +  assumes "negligible S"
    6.12 +    and gf: "\<And>x. x \<in> T - S \<Longrightarrow> g x = f x"
    6.13 +    and fint: "(f has_integral y) T"
    6.14 +  shows "(g has_integral y) T"
    6.15  proof -
    6.16 -  {
    6.17 -    fix a b :: 'b
    6.18 -    fix f g :: "'b \<Rightarrow> 'a"
    6.19 -    fix y :: 'a
    6.20 -    assume as: "\<forall>x \<in> cbox a b - s. g x = f x" "(f has_integral y) (cbox a b)"
    6.21 +  have *: "(g has_integral y) (cbox a b)"
    6.22 +       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
    6.23 +  proof -
    6.24      have "((\<lambda>x. f x + (g x - f x)) has_integral (y + 0)) (cbox a b)"
    6.25 -      apply (rule has_integral_add[OF as(2)])
    6.26 -      apply (rule has_integral_negligible[OF assms(1)])
    6.27 -      using as
    6.28 -      apply auto
    6.29 -      done
    6.30 -    then have "(g has_integral y) (cbox a b)"
    6.31 +      using that by (intro has_integral_add has_integral_negligible) (auto intro!: \<open>negligible S\<close>)
    6.32 +    then show ?thesis
    6.33        by auto
    6.34 -  } note * = this
    6.35 +  qed
    6.36    show ?thesis
    6.37 +    using fint gf
    6.38      apply (subst has_integral_alt)
    6.39 -    using assms(2-)
    6.40 -    apply -
    6.41 -    apply (rule cond_cases)
    6.42 -    apply safe
    6.43 -    apply (rule *)
    6.44 -    apply assumption+
    6.45 -    apply (subst(asm) has_integral_alt)
    6.46 -    unfolding if_not_P
    6.47 -    apply (erule_tac x=e in allE)
    6.48 -    apply safe
    6.49 -    apply (rule_tac x=B in exI)
    6.50 -    apply safe
    6.51 -    apply (erule_tac x=a in allE)
    6.52 -    apply (erule_tac x=b in allE)
    6.53 -    apply safe
    6.54 -    apply (rule_tac x=z in exI)
    6.55 -    apply safe
    6.56 -    apply (rule *[where fa2="\<lambda>x. if x\<in>t then f x else 0"])
    6.57 -    apply auto
    6.58 +    apply (subst (asm) has_integral_alt)
    6.59 +    apply (simp add: split: if_split_asm)
    6.60 +      apply (blast dest: *)
    6.61 +    apply (elim all_forward imp_forward ex_forward)
    6.62 +    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"])+
    6.63      done
    6.64  qed
    6.65  
    6.66  lemma has_integral_spike_eq:
    6.67 -  assumes "negligible s"
    6.68 -    and "\<forall>x\<in>(t - s). g x = f x"
    6.69 -  shows "((f has_integral y) t \<longleftrightarrow> (g has_integral y) t)"
    6.70 -  apply rule
    6.71 -  apply (rule_tac[!] has_integral_spike[OF assms(1)])
    6.72 -  using assms(2)
    6.73 -  apply auto
    6.74 -  done
    6.75 +  assumes "negligible S"
    6.76 +    and gf: "\<And>x. x \<in> T - S \<Longrightarrow> g x = f x"
    6.77 +  shows "(f has_integral y) T \<longleftrightarrow> (g has_integral y) T"
    6.78 +    using has_integral_spike [OF \<open>negligible S\<close>] gf
    6.79 +    by metis
    6.80  
    6.81  lemma integrable_spike:
    6.82 -  assumes "negligible s"
    6.83 -    and "\<forall>x\<in>(t - s). g x = f x"
    6.84 -    and "f integrable_on t"
    6.85 -  shows "g integrable_on  t"
    6.86 -  using assms
    6.87 -  unfolding integrable_on_def
    6.88 -  apply -
    6.89 -  apply (erule exE)
    6.90 -  apply rule
    6.91 -  apply (rule has_integral_spike)
    6.92 -  apply fastforce+
    6.93 -  done
    6.94 +  assumes "negligible S"
    6.95 +    and "\<And>x. x \<in> T - S \<Longrightarrow> g x = f x"
    6.96 +    and "f integrable_on T"
    6.97 +  shows "g integrable_on T"
    6.98 +  using assms unfolding integrable_on_def by (blast intro: has_integral_spike)
    6.99  
   6.100  lemma integral_spike:
   6.101 -  assumes "negligible s"
   6.102 -    and "\<forall>x\<in>(t - s). g x = f x"
   6.103 -  shows "integral t f = integral t g"
   6.104 -  using has_integral_spike_eq[OF assms] by (simp add: integral_def integrable_on_def)
   6.105 +  assumes "negligible S"
   6.106 +    and "\<And>x. x \<in> T - S \<Longrightarrow> g x = f x"
   6.107 +  shows "integral T f = integral T g"
   6.108 +  using has_integral_spike_eq[OF assms]
   6.109 +    by (auto simp: integral_def integrable_on_def)
   6.110  
   6.111  
   6.112  subsection \<open>Some other trivialities about negligible sets.\<close>
   6.113 @@ -2337,7 +2309,7 @@
   6.114    unfolding negligible_def
   6.115  proof (safe, goal_cases)
   6.116    case (1 a b)
   6.117 -  note assm = assms[unfolded negligible_def,rule_format,of a b]
   6.118 +  note assms[unfolded negligible_def,rule_format,of a b]
   6.119    then show ?case
   6.120      apply (subst has_integral_spike_eq[OF assms(2)])
   6.121      defer
   6.122 @@ -2405,37 +2377,24 @@
   6.123  subsection \<open>Finite case of the spike theorem is quite commonly needed.\<close>
   6.124  
   6.125  lemma has_integral_spike_finite:
   6.126 -  assumes "finite s"
   6.127 -    and "\<forall>x\<in>t-s. g x = f x"
   6.128 -    and "(f has_integral y) t"
   6.129 -  shows "(g has_integral y) t"
   6.130 -  apply (rule has_integral_spike)
   6.131 -  using assms
   6.132 -  apply auto
   6.133 -  done
   6.134 +  assumes "finite S"
   6.135 +    and "\<And>x. x \<in> T - S \<Longrightarrow> g x = f x"
   6.136 +    and "(f has_integral y) T"
   6.137 +  shows "(g has_integral y) T"
   6.138 +  using assms has_integral_spike negligible_finite by blast
   6.139  
   6.140  lemma has_integral_spike_finite_eq:
   6.141 -  assumes "finite s"
   6.142 -    and "\<forall>x\<in>t-s. g x = f x"
   6.143 -  shows "((f has_integral y) t \<longleftrightarrow> (g has_integral y) t)"
   6.144 -  apply rule
   6.145 -  apply (rule_tac[!] has_integral_spike_finite)
   6.146 -  using assms
   6.147 -  apply auto
   6.148 -  done
   6.149 +  assumes "finite S"
   6.150 +    and "\<And>x. x \<in> T - S \<Longrightarrow> g x = f x"
   6.151 +  shows "((f has_integral y) T \<longleftrightarrow> (g has_integral y) T)"
   6.152 +  by (metis assms has_integral_spike_finite)
   6.153  
   6.154  lemma integrable_spike_finite:
   6.155 -  assumes "finite s"
   6.156 -    and "\<forall>x\<in>t-s. g x = f x"
   6.157 -    and "f integrable_on t"
   6.158 -  shows "g integrable_on  t"
   6.159 -  using assms
   6.160 -  unfolding integrable_on_def
   6.161 -  apply safe
   6.162 -  apply (rule_tac x=y in exI)
   6.163 -  apply (rule has_integral_spike_finite)
   6.164 -  apply auto
   6.165 -  done
   6.166 +  assumes "finite S"
   6.167 +    and "\<And>x. x \<in> T - S \<Longrightarrow> g x = f x"
   6.168 +    and "f integrable_on T"
   6.169 +  shows "g integrable_on T"
   6.170 +  using assms has_integral_spike_finite by blast
   6.171  
   6.172  
   6.173  subsection \<open>In particular, the boundary of an interval is negligible.\<close>
     7.1 --- a/src/HOL/Analysis/Topology_Euclidean_Space.thy	Thu Apr 27 11:06:47 2017 +0100
     7.2 +++ b/src/HOL/Analysis/Topology_Euclidean_Space.thy	Thu Apr 27 15:59:00 2017 +0100
     7.3 @@ -1265,6 +1265,11 @@
     7.4  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"
     7.5    by (force simp: cbox_Pair_eq)
     7.6  
     7.7 +lemma cbox_Complex_eq: "cbox (Complex a c) (Complex b d) = (\<lambda>(x,y). Complex x y) ` (cbox a b \<times> cbox c d)"
     7.8 +  apply (auto simp: cbox_def Basis_complex_def)
     7.9 +  apply (rule_tac x = "(Re x, Im x)" in image_eqI)
    7.10 +  using complex_eq by auto
    7.11 +
    7.12  lemma cbox_Pair_eq_0: "cbox (a, c) (b, d) = {} \<longleftrightarrow> cbox a b = {} \<or> cbox c d = {}"
    7.13    by (force simp: cbox_Pair_eq)
    7.14  
    7.15 @@ -3916,19 +3921,6 @@
    7.16  lemma bounded_subset_cball: "bounded S \<longleftrightarrow> (\<exists>e x. S \<subseteq> cball x e \<and> 0 \<le> e)"
    7.17    unfolding bounded_def subset_eq  by auto (meson order_trans zero_le_dist)
    7.18  
    7.19 -lemma bounded_subset_ballD:
    7.20 -  assumes "bounded S" shows "\<exists>r. 0 < r \<and> S \<subseteq> ball x r"
    7.21 -proof -
    7.22 -  obtain e::real and y where "S \<subseteq> cball y e"  "0 \<le> e"
    7.23 -    using assms by (auto simp: bounded_subset_cball)
    7.24 -  then show ?thesis
    7.25 -    apply (rule_tac x="dist x y + e + 1" in exI)
    7.26 -    apply (simp add: add.commute add_pos_nonneg)
    7.27 -    apply (erule subset_trans)
    7.28 -    apply (clarsimp simp add: cball_def)
    7.29 -    by (metis add_le_cancel_right add_strict_increasing dist_commute dist_triangle_le zero_less_one)
    7.30 -qed
    7.31 -
    7.32  lemma bounded_any_center: "bounded S \<longleftrightarrow> (\<exists>e. \<forall>y\<in>S. dist a y \<le> e)"
    7.33    unfolding bounded_def
    7.34    by auto (metis add.commute add_le_cancel_right dist_commute dist_triangle_le)
    7.35 @@ -4014,6 +4006,22 @@
    7.36      by (metis insert_is_Un bounded_Un)
    7.37  qed
    7.38  
    7.39 +lemma bounded_subset_ballI: "S \<subseteq> ball x r \<Longrightarrow> bounded S"
    7.40 +  by (meson bounded_ball bounded_subset)
    7.41 +
    7.42 +lemma bounded_subset_ballD:
    7.43 +  assumes "bounded S" shows "\<exists>r. 0 < r \<and> S \<subseteq> ball x r"
    7.44 +proof -
    7.45 +  obtain e::real and y where "S \<subseteq> cball y e"  "0 \<le> e"
    7.46 +    using assms by (auto simp: bounded_subset_cball)
    7.47 +  then show ?thesis
    7.48 +    apply (rule_tac x="dist x y + e + 1" in exI)
    7.49 +    apply (simp add: add.commute add_pos_nonneg)
    7.50 +    apply (erule subset_trans)
    7.51 +    apply (clarsimp simp add: cball_def)
    7.52 +    by (metis add_le_cancel_right add_strict_increasing dist_commute dist_triangle_le zero_less_one)
    7.53 +qed
    7.54 +
    7.55  lemma finite_imp_bounded [intro]: "finite S \<Longrightarrow> bounded S"
    7.56    by (induct set: finite) simp_all
    7.57