# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1449506666 0
# Node ID d2e62ae01cd896866fbbb12048dc24cef550328a
# Parent  4cf66f21b764ee433875f9829ffe965a6ddc0165
Cauchy's integral formula for circles.  Starting to fix eventually_mono.

diff -r 4cf66f21b764 -r d2e62ae01cd8 src/HOL/Filter.thy
--- a/src/HOL/Filter.thy	Mon Dec 07 10:38:04 2015 +0100
+++ b/src/HOL/Filter.thy	Mon Dec 07 16:44:26 2015 +0000
@@ -71,6 +71,11 @@
   unfolding eventually_def
   by (rule is_filter.mono [OF is_filter_Rep_filter])
 
+lemma eventually_mono':
+  "\<lbrakk>eventually P F; \<And>x. P x \<Longrightarrow> Q x\<rbrakk> \<Longrightarrow> eventually Q F"
+  unfolding eventually_def
+  by (blast intro: is_filter.mono [OF is_filter_Rep_filter])
+
 lemma eventually_conj:
   assumes P: "eventually (\<lambda>x. P x) F"
   assumes Q: "eventually (\<lambda>x. Q x) F"
@@ -82,10 +87,11 @@
   assumes "eventually (\<lambda>x. P x \<longrightarrow> Q x) F"
   assumes "eventually (\<lambda>x. P x) F"
   shows "eventually (\<lambda>x. Q x) F"
-proof (rule eventually_mono)
-  show "\<forall>x. (P x \<longrightarrow> Q x) \<and> P x \<longrightarrow> Q x" by simp
-  show "eventually (\<lambda>x. (P x \<longrightarrow> Q x) \<and> P x) F"
+proof -
+  have "eventually (\<lambda>x. (P x \<longrightarrow> Q x) \<and> P x) F"
     using assms by (rule eventually_conj)
+  then show ?thesis
+    by (blast intro: eventually_mono')
 qed
 
 lemma eventually_rev_mp:
@@ -172,7 +178,7 @@
 
 lemma frequently_mp:
   assumes ev: "\<forall>\<^sub>Fx in F. P x \<longrightarrow> Q x" and P: "\<exists>\<^sub>Fx in F. P x" shows "\<exists>\<^sub>Fx in F. Q x"
-proof - 
+proof -
   from ev have "eventually (\<lambda>x. \<not> Q x \<longrightarrow> \<not> P x) F"
     by (rule eventually_rev_mp) (auto intro!: always_eventually)
   from eventually_mp[OF this] P show ?thesis
@@ -225,7 +231,7 @@
   "(\<forall>\<^sub>Fx in F. C \<longrightarrow> P x) \<longleftrightarrow> (C \<longrightarrow> (\<forall>\<^sub>Fx in F. P x))"
   by (cases C; simp add: not_frequently)+
 
-lemmas eventually_frequently_simps = 
+lemmas eventually_frequently_simps =
   eventually_frequently_const_simps
   not_eventually
   eventually_conj_iff
@@ -340,7 +346,7 @@
     unfolding le_filter_def eventually_inf by (auto intro: eventually_True) }
   { assume "F \<le> F'" and "F \<le> F''" thus "F \<le> inf F' F''"
     unfolding le_filter_def eventually_inf
-    by (auto elim!: eventually_mono intro: eventually_conj) }
+    by (auto intro: eventually_mono' [OF eventually_conj]) }
   { show "F \<le> sup F F'" and "F' \<le> sup F F'"
     unfolding le_filter_def eventually_sup by simp_all }
   { assume "F \<le> F''" and "F' \<le> F''" thus "sup F F' \<le> F''"
@@ -404,10 +410,13 @@
 lemma trivial_limit_def: "trivial_limit F \<longleftrightarrow> eventually (\<lambda>x. False) F"
   by (rule eventually_False [symmetric])
 
+lemma False_imp_not_eventually: "(\<forall>x. \<not> P x ) \<Longrightarrow> \<not> trivial_limit net \<Longrightarrow> \<not> eventually (\<lambda>x. P x) net"
+  by (simp add: eventually_False)
+
 lemma eventually_Inf: "eventually P (Inf B) \<longleftrightarrow> (\<exists>X\<subseteq>B. finite X \<and> eventually P (Inf X))"
 proof -
   let ?F = "\<lambda>P. \<exists>X\<subseteq>B. finite X \<and> eventually P (Inf X)"
-  
+
   { fix P have "eventually P (Abs_filter ?F) \<longleftrightarrow> ?F P"
     proof (rule eventually_Abs_filter is_filter.intro)+
       show "?F (\<lambda>x. True)"
@@ -605,7 +614,7 @@
   have "eventually P (INF k. principal {k <..}) \<longleftrightarrow> (\<exists>N::'a. \<forall>n>N. P n)"
     by (subst eventually_INF_base) (auto simp: eventually_principal intro: max.cobounded1 max.cobounded2)
   also have "(INF k. principal {k::'a <..}) = at_top"
-    unfolding at_top_def 
+    unfolding at_top_def
     by (intro INF_eq) (auto intro: less_imp_le simp: Ici_subset_Ioi_iff gt_ex)
   finally show ?thesis .
 qed
@@ -645,7 +654,7 @@
   have "eventually P (INF k. principal {..< k}) \<longleftrightarrow> (\<exists>N::'a. \<forall>n<N. P n)"
     by (subst eventually_INF_base) (auto simp: eventually_principal intro: min.cobounded1 min.cobounded2)
   also have "(INF k. principal {..< k::'a}) = at_bot"
-    unfolding at_bot_def 
+    unfolding at_bot_def
     by (intro INF_eq) (auto intro: less_imp_le simp: Iic_subset_Iio_iff lt_ex)
   finally show ?thesis .
 qed
@@ -828,11 +837,11 @@
   unfolding filterlim_def by (rule order_trans[OF filtermap_INF INF_mono])
 
 lemma filterlim_base:
-  "(\<And>m x. m \<in> J \<Longrightarrow> i m \<in> I) \<Longrightarrow> (\<And>m x. m \<in> J \<Longrightarrow> x \<in> F (i m) \<Longrightarrow> f x \<in> G m) \<Longrightarrow> 
+  "(\<And>m x. m \<in> J \<Longrightarrow> i m \<in> I) \<Longrightarrow> (\<And>m x. m \<in> J \<Longrightarrow> x \<in> F (i m) \<Longrightarrow> f x \<in> G m) \<Longrightarrow>
     LIM x (INF i:I. principal (F i)). f x :> (INF j:J. principal (G j))"
   by (force intro!: filterlim_INF_INF simp: image_subset_iff)
 
-lemma filterlim_base_iff: 
+lemma filterlim_base_iff:
   assumes "I \<noteq> {}" and chain: "\<And>i j. i \<in> I \<Longrightarrow> j \<in> I \<Longrightarrow> F i \<subseteq> F j \<or> F j \<subseteq> F i"
   shows "(LIM x (INF i:I. principal (F i)). f x :> INF j:J. principal (G j)) \<longleftrightarrow>
     (\<forall>j\<in>J. \<exists>i\<in>I. \<forall>x\<in>F i. f x \<in> G j)"
@@ -912,7 +921,7 @@
   shows "(LIM x F. f x :> at_top) \<longleftrightarrow> (\<forall>Z>c. eventually (\<lambda>x. Z \<le> f x) F)"
   by (metis filterlim_at_top order_less_le_trans gt_ex filterlim_at_top_ge)
 
-lemma filterlim_at_bot: 
+lemma filterlim_at_bot:
   fixes f :: "'a \<Rightarrow> ('b::linorder)"
   shows "(LIM x F. f x :> at_bot) \<longleftrightarrow> (\<forall>Z. eventually (\<lambda>x. f x \<le> Z) F)"
   by (auto simp: filterlim_iff eventually_at_bot_linorder elim!: eventually_elim1)
@@ -926,12 +935,12 @@
   assume "\<forall>Z. eventually (\<lambda>x. f x \<le> Z) F"
   hence "eventually (\<lambda>x. f x \<le> Z') F" by auto
   thus "eventually (\<lambda>x. f x < Z) F"
-    apply (rule eventually_mono[rotated])
+    apply (rule eventually_mono')
     using 1 by auto
-  next 
-    fix Z :: 'b 
+  next
+    fix Z :: 'b
     show "\<forall>Z. eventually (\<lambda>x. f x < Z) F \<Longrightarrow> eventually (\<lambda>x. f x \<le> Z) F"
-      by (drule spec [of _ Z], erule eventually_mono[rotated], auto simp add: less_imp_le)
+      by (drule spec [of _ Z], erule eventually_mono', auto simp add: less_imp_le)
 qed
 
 lemma filterlim_at_bot_le:
@@ -958,7 +967,7 @@
 where "rel_filter R F G = ((R ===> op =) ===> op =) (Rep_filter F) (Rep_filter G)"
 
 lemma rel_filter_eventually:
-  "rel_filter R F G \<longleftrightarrow> 
+  "rel_filter R F G \<longleftrightarrow>
   ((R ===> op =) ===> op =) (\<lambda>P. eventually P F) (\<lambda>P. eventually P G)"
 by(simp add: rel_filter_def eventually_def)
 
@@ -984,7 +993,7 @@
   from Q have *: "\<And>x. T (Rep x) x" unfolding Quotient_alt_def by blast
 
   fix F
-  show "rel_filter T (filtermap Rep F) F" 
+  show "rel_filter T (filtermap Rep F) F"
     by(auto elim: rel_funD intro: * intro!: ext arg_cong[where f="\<lambda>P. eventually P F"] rel_funI
             del: iffI simp add: eventually_filtermap rel_filter_eventually)
 qed(auto simp add: map_fun_def o_def eventually_filtermap filter_eq_iff fun_eq_iff rel_filter_eventually
@@ -1063,7 +1072,7 @@
 proof(rule left_totalI)
   fix F :: "'a filter"
   from bi_total_fun[OF bi_unique_fun[OF \<open>bi_total A\<close> bi_unique_eq] bi_total_eq]
-  obtain G where [transfer_rule]: "((A ===> op =) ===> op =) (\<lambda>P. eventually P F) G" 
+  obtain G where [transfer_rule]: "((A ===> op =) ===> op =) (\<lambda>P. eventually P F) G"
     unfolding  bi_total_def by blast
   moreover have "is_filter (\<lambda>P. eventually P F) \<longleftrightarrow> is_filter G" by transfer_prover
   hence "is_filter G" by(simp add: eventually_def is_filter_Rep_filter)
@@ -1094,7 +1103,7 @@
     fix P :: "'a \<Rightarrow> bool"
     obtain P' where [transfer_rule]: "(A ===> op =) P P'"
       using left_total_fun[OF assms left_total_eq] unfolding left_total_def by blast
-    have "eventually P F = eventually P' G" 
+    have "eventually P F = eventually P' G"
       and "eventually P F' = eventually P' G" by transfer_prover+
     thus "eventually P F = eventually P F'" by simp
   qed
@@ -1139,7 +1148,7 @@
 
 context
   fixes A :: "'a \<Rightarrow> 'b \<Rightarrow> bool"
-  assumes [transfer_rule]: "bi_unique A" 
+  assumes [transfer_rule]: "bi_unique A"
 begin
 
 lemma le_filter_parametric [transfer_rule]:
@@ -1173,4 +1182,4 @@
 
 end
 
-end
\ No newline at end of file
+end
diff -r 4cf66f21b764 -r d2e62ae01cd8 src/HOL/Library/Extended_Real.thy
--- a/src/HOL/Library/Extended_Real.thy	Mon Dec 07 10:38:04 2015 +0100
+++ b/src/HOL/Library/Extended_Real.thy	Mon Dec 07 16:44:26 2015 +0000
@@ -2443,11 +2443,8 @@
   assume "open S" and "x \<in> S"
   then have S: "open S" "ereal x \<in> ereal ` S"
     by (simp_all add: inj_image_mem_iff)
-  have "\<forall>x. f x \<in> ereal ` S \<longrightarrow> real_of_ereal (f x) \<in> S"
-    by auto
-  from this lim[THEN topological_tendstoD, OF open_ereal, OF S]
   show "eventually (\<lambda>x. real_of_ereal (f x) \<in> S) net"
-    by (rule eventually_mono)
+    by (auto intro: eventually_mono' [OF lim[THEN topological_tendstoD, OF open_ereal, OF S]])
 qed
 
 lemma lim_ereal[simp]: "((\<lambda>n. ereal (f n)) ---> ereal x) net \<longleftrightarrow> (f ---> x) net"
diff -r 4cf66f21b764 -r d2e62ae01cd8 src/HOL/Library/Liminf_Limsup.thy
--- a/src/HOL/Library/Liminf_Limsup.thy	Mon Dec 07 10:38:04 2015 +0100
+++ b/src/HOL/Library/Liminf_Limsup.thy	Mon Dec 07 16:44:26 2015 +0000
@@ -100,7 +100,7 @@
 lemma Liminf_eq:
   assumes "eventually (\<lambda>x. f x = g x) F"
   shows "Liminf F f = Liminf F g"
-  by (intro antisym Liminf_mono eventually_mono[OF _ assms]) auto
+  by (intro antisym Liminf_mono eventually_mono'[OF assms]) auto
 
 lemma Limsup_mono:
   assumes ev: "eventually (\<lambda>x. f x \<le> g x) F"
@@ -116,7 +116,7 @@
 lemma Limsup_eq:
   assumes "eventually (\<lambda>x. f x = g x) net"
   shows "Limsup net f = Limsup net g"
-  by (intro antisym Limsup_mono eventually_mono[OF _ assms]) auto
+  by (intro antisym Limsup_mono eventually_mono'[OF assms]) auto
 
 lemma Liminf_le_Limsup:
   assumes ntriv: "\<not> trivial_limit F"
diff -r 4cf66f21b764 -r d2e62ae01cd8 src/HOL/Limits.thy
--- a/src/HOL/Limits.thy	Mon Dec 07 10:38:04 2015 +0100
+++ b/src/HOL/Limits.thy	Mon Dec 07 16:44:26 2015 +0000
@@ -661,6 +661,10 @@
 
 subsubsection \<open>Linear operators and multiplication\<close>
 
+lemma linear_times:
+  fixes c::"'a::real_algebra" shows "linear (\<lambda>x. c * x)"
+  by (auto simp: linearI distrib_left)
+
 lemma (in bounded_linear) tendsto:
   "(g ---> a) F \<Longrightarrow> ((\<lambda>x. f (g x)) ---> f a) F"
   by (simp only: tendsto_Zfun_iff diff [symmetric] Zfun)
@@ -713,6 +717,16 @@
 lemmas tendsto_mult [tendsto_intros] =
   bounded_bilinear.tendsto [OF bounded_bilinear_mult]
 
+lemma tendsto_mult_left:
+  fixes c::"'a::real_normed_algebra"
+  shows "(f ---> l) F \<Longrightarrow> ((\<lambda>x. c * (f x)) ---> c * l) F"
+by (rule tendsto_mult [OF tendsto_const])
+
+lemma tendsto_mult_right:
+  fixes c::"'a::real_normed_algebra"
+  shows "(f ---> l) F \<Longrightarrow> ((\<lambda>x. (f x) * c) ---> l * c) F"
+by (rule tendsto_mult [OF _ tendsto_const])
+
 lemmas continuous_of_real [continuous_intros] =
   bounded_linear.continuous [OF bounded_linear_of_real]
 
diff -r 4cf66f21b764 -r d2e62ae01cd8 src/HOL/Multivariate_Analysis/Cauchy_Integral_Thm.thy
--- a/src/HOL/Multivariate_Analysis/Cauchy_Integral_Thm.thy	Mon Dec 07 10:38:04 2015 +0100
+++ b/src/HOL/Multivariate_Analysis/Cauchy_Integral_Thm.thy	Mon Dec 07 16:44:26 2015 +0000
@@ -1508,7 +1508,7 @@
   apply (auto simp: has_contour_integral_integral)
   done
 
-lemma contour_integral_0: "contour_integral g (\<lambda>x. 0) = 0"
+lemma contour_integral_0 [simp]: "contour_integral g (\<lambda>x. 0) = 0"
   by (simp add: contour_integral_unique has_contour_integral_0)
 
 lemma contour_integral_setsum:
@@ -4728,4 +4728,472 @@
       \<Longrightarrow> winding_number h z = winding_number g z"
   by (metis segment_bound(2) norm_minus_commute not_le winding_number_loops_linear_eq)
 
+
+proposition winding_number_subpath_combine:
+    "\<lbrakk>path g; z \<notin> path_image g;
+      u \<in> {0..1}; v \<in> {0..1}; w \<in> {0..1}\<rbrakk>
+      \<Longrightarrow> winding_number (subpath u v g) z + winding_number (subpath v w g) z =
+          winding_number (subpath u w g) z"
+apply (rule trans [OF winding_number_join [THEN sym]
+                      winding_number_homotopic_paths [OF homotopic_join_subpaths]])
+apply (auto dest: path_image_subpath_subset)
+done
+
+
+subsection\<open>Partial circle path\<close>
+
+definition part_circlepath :: "[complex, real, real, real, real] \<Rightarrow> complex"
+  where "part_circlepath z r s t \<equiv> \<lambda>x. z + of_real r * exp (ii * of_real (linepath s t x))"
+
+lemma pathstart_part_circlepath [simp]:
+     "pathstart(part_circlepath z r s t) = z + r*exp(ii * s)"
+by (metis part_circlepath_def pathstart_def pathstart_linepath)
+
+lemma pathfinish_part_circlepath [simp]:
+     "pathfinish(part_circlepath z r s t) = z + r*exp(ii*t)"
+by (metis part_circlepath_def pathfinish_def pathfinish_linepath)
+
+proposition has_vector_derivative_part_circlepath [derivative_intros]:
+    "((part_circlepath z r s t) has_vector_derivative
+      (ii * r * (of_real t - of_real s) * exp(ii * linepath s t x)))
+     (at x within X)"
+  apply (simp add: part_circlepath_def linepath_def scaleR_conv_of_real)
+  apply (rule has_vector_derivative_real_complex)
+  apply (rule derivative_eq_intros | simp)+
+  done
+
+corollary vector_derivative_part_circlepath:
+    "vector_derivative (part_circlepath z r s t) (at x) =
+       ii * r * (of_real t - of_real s) * exp(ii * linepath s t x)"
+  using has_vector_derivative_part_circlepath vector_derivative_at by blast
+
+corollary vector_derivative_part_circlepath01:
+    "\<lbrakk>0 \<le> x; x \<le> 1\<rbrakk>
+     \<Longrightarrow> vector_derivative (part_circlepath z r s t) (at x within {0..1}) =
+          ii * r * (of_real t - of_real s) * exp(ii * linepath s t x)"
+  using has_vector_derivative_part_circlepath
+  by (auto simp: vector_derivative_at_within_ivl)
+
+lemma valid_path_part_circlepath [simp]: "valid_path (part_circlepath z r s t)"
+  apply (simp add: valid_path_def)
+  apply (rule C1_differentiable_imp_piecewise)
+  apply (auto simp: C1_differentiable_on_eq vector_derivative_works vector_derivative_part_circlepath has_vector_derivative_part_circlepath
+              intro!: continuous_intros)
+  done
+
+lemma path_part_circlepath [simp]: "path (part_circlepath z r s t)"
+  by (simp add: valid_path_imp_path)
+
+proposition path_image_part_circlepath:
+  assumes "s \<le> t"
+    shows "path_image (part_circlepath z r s t) = {z + r * exp(ii * of_real x) | x. s \<le> x \<and> x \<le> t}"
+proof -
+  { fix z::real
+    assume "0 \<le> z" "z \<le> 1"
+    with \<open>s \<le> t\<close> have "\<exists>x. (exp (\<i> * linepath s t z) = exp (\<i> * of_real x)) \<and> s \<le> x \<and> x \<le> t"
+      apply (rule_tac x="(1 - z) * s + z * t" in exI)
+      apply (simp add: linepath_def scaleR_conv_of_real algebra_simps)
+      apply (rule conjI)
+      using mult_right_mono apply blast
+      using affine_ineq  by (metis "mult.commute")
+  }
+  moreover
+  { fix z
+    assume "s \<le> z" "z \<le> t"
+    then have "z + of_real r * exp (\<i> * of_real z) \<in> (\<lambda>x. z + of_real r * exp (\<i> * linepath s t x)) ` {0..1}"
+      apply (rule_tac x="(z - s)/(t - s)" in image_eqI)
+      apply (simp add: linepath_def scaleR_conv_of_real divide_simps exp_eq)
+      apply (auto simp: algebra_simps divide_simps)
+      done
+  }
+  ultimately show ?thesis
+    by (fastforce simp add: path_image_def part_circlepath_def)
+qed
+
+corollary path_image_part_circlepath_subset:
+    "\<lbrakk>s \<le> t; 0 \<le> r\<rbrakk> \<Longrightarrow> path_image(part_circlepath z r s t) \<subseteq> sphere z r"
+by (auto simp: path_image_part_circlepath sphere_def dist_norm algebra_simps norm_mult)
+
+proposition in_path_image_part_circlepath:
+  assumes "w \<in> path_image(part_circlepath z r s t)" "s \<le> t" "0 \<le> r"
+    shows "norm(w - z) = r"
+proof -
+  have "w \<in> {c. dist z c = r}"
+    by (metis (no_types) path_image_part_circlepath_subset sphere_def subset_eq assms)
+  thus ?thesis
+    by (simp add: dist_norm norm_minus_commute)
+qed
+
+proposition finite_bounded_log: "finite {z::complex. norm z \<le> b \<and> exp z = w}"
+proof (cases "w = 0")
+  case True then show ?thesis by auto
+next
+  case False
+  have *: "finite {x. cmod (complex_of_real (2 * real_of_int x * pi) * \<i>) \<le> b + cmod (Ln w)}"
+    apply (simp add: norm_mult finite_int_iff_bounded_le)
+    apply (rule_tac x="floor ((b + cmod (Ln w)) / (2*pi))" in exI)
+    apply (auto simp: divide_simps le_floor_iff)
+    done
+  have [simp]: "\<And>P f. {z. P z \<and> (\<exists>n. z = f n)} = f ` {n. P (f n)}"
+    by blast
+  show ?thesis
+    apply (subst exp_Ln [OF False, symmetric])
+    apply (simp add: exp_eq)
+    using norm_add_leD apply (fastforce intro: finite_subset [OF _ *])
+    done
+qed
+
+lemma finite_bounded_log2:
+  fixes a::complex
+    assumes "a \<noteq> 0"
+    shows "finite {z. norm z \<le> b \<and> exp(a*z) = w}"
+proof -
+  have *: "finite ((\<lambda>z. z / a) ` {z. cmod z \<le> b * cmod a \<and> exp z = w})"
+    by (rule finite_imageI [OF finite_bounded_log])
+  show ?thesis
+    by (rule finite_subset [OF _ *]) (force simp: assms norm_mult)
+qed
+
+proposition has_contour_integral_bound_part_circlepath_strong:
+  assumes fi: "(f has_contour_integral i) (part_circlepath z r s t)"
+      and "finite k" and le: "0 \<le> B" "0 < r" "s \<le> t"
+      and B: "\<And>x. x \<in> path_image(part_circlepath z r s t) - k \<Longrightarrow> norm(f x) \<le> B"
+    shows "cmod i \<le> B * r * (t - s)"
+proof -
+  consider "s = t" | "s < t" using \<open>s \<le> t\<close> by linarith
+  then show ?thesis
+  proof cases
+    case 1 with fi [unfolded has_contour_integral]
+    have "i = 0"  by (simp add: vector_derivative_part_circlepath)
+    with assms show ?thesis by simp
+  next
+    case 2
+    have [simp]: "abs r = r" using \<open>r > 0\<close> by linarith
+    have [simp]: "cmod (complex_of_real t - complex_of_real s) = t-s"
+      by (metis "2" abs_of_pos diff_gt_0_iff_gt norm_of_real of_real_diff)
+    have "finite (part_circlepath z r s t -` {y} \<inter> {0..1})" if "y \<in> k" for y
+    proof -
+      def w \<equiv> "(y - z)/of_real r / exp(ii * of_real s)"
+      have fin: "finite (of_real -` {z. cmod z \<le> 1 \<and> exp (\<i> * complex_of_real (t - s) * z) = w})"
+        apply (rule finite_vimageI [OF finite_bounded_log2])
+        using \<open>s < t\<close> apply (auto simp: inj_of_real)
+        done
+      show ?thesis
+        apply (simp add: part_circlepath_def linepath_def vimage_def)
+        apply (rule finite_subset [OF _ fin])
+        using le
+        apply (auto simp: w_def algebra_simps scaleR_conv_of_real exp_add exp_diff)
+        done
+    qed
+    then have fin01: "finite ((part_circlepath z r s t) -` k \<inter> {0..1})"
+      by (rule finite_finite_vimage_IntI [OF \<open>finite k\<close>])
+    have **: "((\<lambda>x. if (part_circlepath z r s t x) \<in> k then 0
+                    else f(part_circlepath z r s t x) *
+                       vector_derivative (part_circlepath z r s t) (at x)) has_integral i)  {0..1}"
+      apply (rule has_integral_spike
+              [where f = "\<lambda>x. f(part_circlepath z r s t x) * vector_derivative (part_circlepath z r s t) (at x)"])
+      apply (rule negligible_finite [OF fin01])
+      using fi has_contour_integral
+      apply auto
+      done
+    have *: "\<And>x. \<lbrakk>0 \<le> x; x \<le> 1; part_circlepath z r s t x \<notin> k\<rbrakk> \<Longrightarrow> cmod (f (part_circlepath z r s t x)) \<le> B"
+      by (auto intro!: B [unfolded path_image_def image_def, simplified])
+    show ?thesis
+      apply (rule has_integral_bound [where 'a=real, simplified, OF _ **, simplified])
+      using assms apply force
+      apply (simp add: norm_mult vector_derivative_part_circlepath)
+      using le * "2" \<open>r > 0\<close> by auto
+  qed
+qed
+
+corollary has_contour_integral_bound_part_circlepath:
+      "\<lbrakk>(f has_contour_integral i) (part_circlepath z r s t);
+        0 \<le> B; 0 < r; s \<le> t;
+        \<And>x. x \<in> path_image(part_circlepath z r s t) \<Longrightarrow> norm(f x) \<le> B\<rbrakk>
+       \<Longrightarrow> norm i \<le> B*r*(t - s)"
+  by (auto intro: has_contour_integral_bound_part_circlepath_strong)
+
+proposition contour_integrable_continuous_part_circlepath:
+     "continuous_on (path_image (part_circlepath z r s t)) f
+      \<Longrightarrow> f contour_integrable_on (part_circlepath z r s t)"
+  apply (simp add: contour_integrable_on has_contour_integral_def vector_derivative_part_circlepath path_image_def)
+  apply (rule integrable_continuous_real)
+  apply (fast intro: path_part_circlepath [unfolded path_def] continuous_intros continuous_on_compose2 [where g=f, OF _ _ order_refl])
+  done
+
+proposition winding_number_part_circlepath_pos_less:
+  assumes "s < t" and no: "norm(w - z) < r"
+    shows "0 < Re (winding_number(part_circlepath z r s t) w)"
+proof -
+  have "0 < r" by (meson no norm_not_less_zero not_le order.strict_trans2)
+  note valid_path_part_circlepath
+  moreover have " w \<notin> path_image (part_circlepath z r s t)"
+    using assms by (auto simp: path_image_def image_def part_circlepath_def norm_mult linepath_def)
+  moreover have "0 < r * (t - s) * (r - cmod (w - z))"
+    using assms by (metis \<open>0 < r\<close> diff_gt_0_iff_gt mult_pos_pos)
+  ultimately show ?thesis
+    apply (rule winding_number_pos_lt [where e = "r*(t - s)*(r - norm(w - z))"])
+    apply (simp add: vector_derivative_part_circlepath right_diff_distrib [symmetric] mult_ac)
+    apply (rule mult_left_mono)+
+    using Re_Im_le_cmod [of "w-z" "linepath s t x" for x]
+    apply (simp add: exp_Euler cos_of_real sin_of_real part_circlepath_def algebra_simps cos_squared_eq [unfolded power2_eq_square])
+    using assms \<open>0 < r\<close> by auto
+qed
+
+proposition simple_path_part_circlepath:
+    "simple_path(part_circlepath z r s t) \<longleftrightarrow> (r \<noteq> 0 \<and> s \<noteq> t \<and> abs(s - t) \<le> 2*pi)"
+proof (cases "r = 0 \<or> s = t")
+  case True
+  then show ?thesis
+    apply (rule disjE)
+    apply (force simp: part_circlepath_def simple_path_def intro: bexI [where x = "1/4"] bexI [where x = "1/3"])+
+    done
+next
+  case False then have "r \<noteq> 0" "s \<noteq> t" by auto
+  have *: "\<And>x y z s t. ii*((1 - x) * s + x * t) = ii*(((1 - y) * s + y * t)) + z  \<longleftrightarrow> ii*(x - y) * (t - s) = z"
+    by (simp add: algebra_simps)
+  have abs01: "\<And>x y::real. 0 \<le> x \<and> x \<le> 1 \<and> 0 \<le> y \<and> y \<le> 1
+                      \<Longrightarrow> (x = y \<or> x = 0 \<and> y = 1 \<or> x = 1 \<and> y = 0 \<longleftrightarrow> abs(x - y) \<in> {0,1})"
+    by auto
+  have abs_away: "\<And>P. (\<forall>x\<in>{0..1}. \<forall>y\<in>{0..1}. P(abs(x - y))) \<longleftrightarrow> (\<forall>x::real. 0 \<le> x \<and> x \<le> 1 \<longrightarrow> P x)"
+    by force
+  have **: "\<And>x y. (\<exists>n. (complex_of_real x - of_real y) * (of_real t - of_real s) = 2 * (of_int n * of_real pi)) \<longleftrightarrow>
+                  (\<exists>n. abs(x - y) * (t - s) = 2 * (of_int n * pi))"
+    by (force simp: algebra_simps abs_if dest: arg_cong [where f=Re] arg_cong [where f=complex_of_real]
+                    intro: exI [where x = "-n" for n])
+  have 1: "\<forall>x. 0 \<le> x \<and> x \<le> 1 \<longrightarrow> (\<exists>n. x * (t - s) = 2 * (real_of_int n * pi)) \<longrightarrow> x = 0 \<or> x = 1 \<Longrightarrow> \<bar>s - t\<bar> \<le> 2 * pi"
+    apply (rule ccontr)
+    apply (drule_tac x="2*pi / abs(t-s)" in spec)
+    using False
+    apply (simp add: abs_minus_commute divide_simps)
+    apply (frule_tac x=1 in spec)
+    apply (drule_tac x="-1" in spec)
+    apply (simp add:)
+    done
+  have 2: "\<bar>s - t\<bar> = \<bar>2 * (real_of_int n * pi) / x\<bar>" if "x \<noteq> 0" "x * (t - s) = 2 * (real_of_int n * pi)" for x n
+  proof -
+    have "t-s = 2 * (real_of_int n * pi)/x"
+      using that by (simp add: field_simps)
+    then show ?thesis by (metis abs_minus_commute)
+  qed
+  show ?thesis using False
+    apply (simp add: simple_path_def path_part_circlepath)
+    apply (simp add: part_circlepath_def linepath_def exp_eq  * ** abs01  del: Set.insert_iff)
+    apply (subst abs_away)
+    apply (auto simp: 1)
+    apply (rule ccontr)
+    apply (auto simp: 2 divide_simps abs_mult dest: of_int_leD)
+    done
+qed
+
+proposition arc_part_circlepath:
+  assumes "r \<noteq> 0" "s \<noteq> t" "abs(s - t) < 2*pi"
+    shows "arc (part_circlepath z r s t)"
+proof -
+  have *: "x = y" if eq: "\<i> * (linepath s t x) = \<i> * (linepath s t y) + 2 * of_int n * complex_of_real pi * \<i>"
+                  and x: "x \<in> {0..1}" and y: "y \<in> {0..1}" for x y n
+    proof -
+      have "(linepath s t x) = (linepath s t y) + 2 * of_int n * complex_of_real pi"
+        by (metis add_divide_eq_iff complex_i_not_zero mult.commute nonzero_mult_divide_cancel_left eq)
+      then have "s*y + t*x = s*x + (t*y + of_int n * (pi * 2))"
+        by (force simp: algebra_simps linepath_def dest: arg_cong [where f=Re])
+      then have st: "x \<noteq> y \<Longrightarrow> (s-t) = (of_int n * (pi * 2) / (y-x))"
+        by (force simp: field_simps)
+      show ?thesis
+        apply (rule ccontr)
+        using assms x y
+        apply (simp add: st abs_mult field_simps)
+        using st
+        apply (auto simp: dest: of_int_lessD)
+        done
+    qed
+  show ?thesis
+    using assms
+    apply (simp add: arc_def)
+    apply (simp add: part_circlepath_def inj_on_def exp_eq)
+    apply (blast intro: *)
+    done
+qed
+
+
+subsection\<open>Special case of one complete circle\<close>
+
+definition circlepath :: "[complex, real, real] \<Rightarrow> complex"
+  where "circlepath z r \<equiv> part_circlepath z r 0 (2*pi)"
+
+lemma circlepath: "circlepath z r = (\<lambda>x. z + r * exp(2 * of_real pi * ii * of_real x))"
+  by (simp add: circlepath_def part_circlepath_def linepath_def algebra_simps)
+
+lemma pathstart_circlepath [simp]: "pathstart (circlepath z r) = z + r"
+  by (simp add: circlepath_def)
+
+lemma pathfinish_circlepath [simp]: "pathfinish (circlepath z r) = z + r"
+  by (simp add: circlepath_def) (metis exp_two_pi_i mult.commute)
+
+proposition has_vector_derivative_circlepath [derivative_intros]:
+ "((circlepath z r) has_vector_derivative (2 * pi * ii * r * exp (2 * of_real pi * ii * of_real x)))
+   (at x within X)"
+  apply (simp add: circlepath_def scaleR_conv_of_real)
+  apply (rule derivative_eq_intros)
+  apply (simp add: algebra_simps)
+  done
+
+corollary vector_derivative_circlepath:
+   "vector_derivative (circlepath z r) (at x) =
+    2 * pi * ii * r * exp(2 * of_real pi * ii * x)"
+using has_vector_derivative_circlepath vector_derivative_at by blast
+
+corollary vector_derivative_circlepath01:
+    "\<lbrakk>0 \<le> x; x \<le> 1\<rbrakk>
+     \<Longrightarrow> vector_derivative (circlepath z r) (at x within {0..1}) =
+          2 * pi * ii * r * exp(2 * of_real pi * ii * x)"
+  using has_vector_derivative_circlepath
+  by (auto simp: vector_derivative_at_within_ivl)
+
+lemma valid_path_circlepath [simp]: "valid_path (circlepath z r)"
+  by (simp add: circlepath_def)
+
+lemma path_circlepath [simp]: "path (circlepath z r)"
+  by (simp add: valid_path_imp_path)
+
+proposition path_image_circlepath [simp]:
+  assumes "0 \<le> r" shows "path_image (circlepath z r) = sphere z r"
+proof -
+  have *: "x \<in> (\<lambda>u. z + (cmod (x - z)) * exp (\<i> * (of_real u * (of_real pi * 2)))) ` {0..1}" for x
+  proof (cases "x = z")
+    case True then show ?thesis by force
+  next
+    case False
+    def w \<equiv> "x - z"
+    then have "w \<noteq> 0" by (simp add: False)
+    have **: "\<And>t. \<lbrakk>Re w = cos t * cmod w; Im w = sin t * cmod w\<rbrakk> \<Longrightarrow> w = of_real (cmod w) * exp (\<i> * t)"
+      using cis_conv_exp complex_eq_iff by auto
+    show ?thesis
+      apply (rule sincos_total_2pi [of "Re(w/of_real(norm w))" "Im(w/of_real(norm w))"])
+      apply (simp add: divide_simps \<open>w \<noteq> 0\<close> cmod_power2 [symmetric])
+      apply (rule_tac x="t / (2*pi)" in image_eqI)
+      apply (simp add: divide_simps \<open>w \<noteq> 0\<close>)
+      using False **
+      apply (auto simp: w_def)
+      done
+  qed
+  show ?thesis
+    unfolding circlepath path_image_def sphere_def dist_norm
+    by (force simp: assms algebra_simps norm_mult norm_minus_commute intro: *)
+qed
+
+lemma has_contour_integral_bound_circlepath_strong:
+      "\<lbrakk>(f has_contour_integral i) (circlepath z r);
+        finite k; 0 \<le> B; 0 < r;
+        \<And>x. \<lbrakk>norm(x - z) = r; x \<notin> k\<rbrakk> \<Longrightarrow> norm(f x) \<le> B\<rbrakk>
+        \<Longrightarrow> norm i \<le> B*(2*pi*r)"
+  unfolding circlepath_def
+  by (auto simp: algebra_simps in_path_image_part_circlepath dest!: has_contour_integral_bound_part_circlepath_strong)
+
+corollary has_contour_integral_bound_circlepath:
+      "\<lbrakk>(f has_contour_integral i) (circlepath z r);
+        0 \<le> B; 0 < r; \<And>x. norm(x - z) = r \<Longrightarrow> norm(f x) \<le> B\<rbrakk>
+        \<Longrightarrow> norm i \<le> B*(2*pi*r)"
+  by (auto intro: has_contour_integral_bound_circlepath_strong)
+
+proposition contour_integrable_continuous_circlepath:
+    "continuous_on (path_image (circlepath z r)) f
+     \<Longrightarrow> f contour_integrable_on (circlepath z r)"
+  by (simp add: circlepath_def contour_integrable_continuous_part_circlepath)
+
+lemma simple_path_circlepath: "simple_path(circlepath z r) \<longleftrightarrow> (r \<noteq> 0)"
+  by (simp add: circlepath_def simple_path_part_circlepath)
+
+lemma notin_path_image_circlepath [simp]: "cmod (w - z) < r \<Longrightarrow> w \<notin> path_image (circlepath z r)"
+  apply (subst path_image_circlepath)
+  apply (meson le_cases less_le_trans norm_not_less_zero)
+  apply (simp add: sphere_def dist_norm norm_minus_commute)
+  done
+
+proposition contour_integral_circlepath:
+     "0 < r \<Longrightarrow> contour_integral (circlepath z r) (\<lambda>w. 1 / (w - z)) = 2 * complex_of_real pi * \<i>"
+  apply (rule contour_integral_unique)
+  apply (simp add: has_contour_integral_def)
+  apply (subst has_integral_cong)
+  apply (simp add: vector_derivative_circlepath01)
+  using has_integral_const_real [of _ 0 1]
+  apply (force simp: circlepath)
+  done
+
+lemma winding_number_circlepath_centre: "0 < r \<Longrightarrow> winding_number (circlepath z r) z = 1"
+  apply (rule winding_number_unique_loop)
+  apply (simp_all add: sphere_def valid_path_imp_path)
+  apply (rule_tac x="circlepath z r" in exI)
+  apply (simp add: sphere_def contour_integral_circlepath)
+  done
+
+proposition winding_number_circlepath:
+  assumes "norm(w - z) < r" shows "winding_number(circlepath z r) w = 1"
+proof (cases "w = z")
+  case True then show ?thesis
+    using assms winding_number_circlepath_centre by auto
+next
+  case False
+  have [simp]: "r > 0"
+    using assms le_less_trans norm_ge_zero by blast
+  def r' \<equiv> "norm(w - z)"
+  have "r' < r"
+    by (simp add: assms r'_def)
+  have disjo: "cball z r' \<inter> sphere z r = {}"
+    using \<open>r' < r\<close> by (force simp: cball_def sphere_def)
+  have "winding_number(circlepath z r) w = winding_number(circlepath z r) z"
+    apply (rule winding_number_around_inside [where s = "cball z r'"])
+    apply (simp_all add: disjo order.strict_implies_order winding_number_circlepath_centre)
+    apply (simp_all add: False r'_def dist_norm norm_minus_commute)
+    done
+  also have "... = 1"
+    by (simp add: winding_number_circlepath_centre)
+  finally show ?thesis .
+qed
+
+
+text\<open> Hence the Cauchy formula for points inside a circle.\<close>
+
+theorem Cauchy_integral_circlepath:
+  assumes "continuous_on (cball z r) f" "f holomorphic_on (ball z r)" "norm(w - z) < r"
+  shows "((\<lambda>u. f u/(u - w)) has_contour_integral (2 * of_real pi * ii * f w))
+         (circlepath z r)"
+proof -
+  have "r > 0"
+    using assms le_less_trans norm_ge_zero by blast
+  have "((\<lambda>u. f u / (u - w)) has_contour_integral (2 * pi) * \<i> * winding_number (circlepath z r) w * f w)
+        (circlepath z r)"
+    apply (rule Cauchy_integral_formula_weak [where s = "cball z r" and k = "{}"])
+    using assms  \<open>r > 0\<close>
+    apply (simp_all add: dist_norm norm_minus_commute)
+    apply (metis at_within_interior dist_norm holomorphic_on_def interior_ball mem_ball norm_minus_commute)
+    apply (simp add: cball_def sphere_def dist_norm, clarify)
+    apply (simp add:)
+    by (metis dist_commute dist_norm less_irrefl)
+  then show ?thesis
+    by (simp add: winding_number_circlepath assms)
+qed
+
+corollary Cauchy_integral_circlepath_simple:
+  assumes "f holomorphic_on cball z r" "norm(w - z) < r"
+  shows "((\<lambda>u. f u/(u - w)) has_contour_integral (2 * of_real pi * ii * f w))
+         (circlepath z r)"
+using assms by (force simp: holomorphic_on_imp_continuous_on holomorphic_on_subset Cauchy_integral_circlepath)
+
+
+lemma no_bounded_connected_component_imp_winding_number_zero:
+  assumes g: "path g" "path_image g \<subseteq> s" "pathfinish g = pathstart g" "z \<notin> s"
+      and nb: "\<And>z. bounded (connected_component_set (- s) z) \<longrightarrow> z \<in> s"
+  shows "winding_number g z = 0"
+apply (rule winding_number_zero_in_outside)
+apply (simp_all add: assms)
+by (metis nb [of z] \<open>path_image g \<subseteq> s\<close> \<open>z \<notin> s\<close> contra_subsetD mem_Collect_eq outside outside_mono)
+
+lemma no_bounded_path_component_imp_winding_number_zero:
+  assumes g: "path g" "path_image g \<subseteq> s" "pathfinish g = pathstart g" "z \<notin> s"
+      and nb: "\<And>z. bounded (path_component_set (- s) z) \<longrightarrow> z \<in> s"
+  shows "winding_number g z = 0"
+apply (rule no_bounded_connected_component_imp_winding_number_zero [OF g])
+by (simp add: bounded_subset nb path_component_subset_connected_component)
+
 end
diff -r 4cf66f21b764 -r d2e62ae01cd8 src/HOL/Multivariate_Analysis/Complex_Analysis_Basics.thy
--- a/src/HOL/Multivariate_Analysis/Complex_Analysis_Basics.thy	Mon Dec 07 10:38:04 2015 +0100
+++ b/src/HOL/Multivariate_Analysis/Complex_Analysis_Basics.thy	Mon Dec 07 16:44:26 2015 +0000
@@ -24,8 +24,8 @@
   using bounded_linear.has_derivative[OF bounded_linear_of_real] .
 
 lemma has_vector_derivative_real_complex:
-  "DERIV f (of_real a) :> f' \<Longrightarrow> ((\<lambda>x. f (of_real x)) has_vector_derivative f') (at a)"
-  using has_derivative_compose[of of_real of_real a UNIV f "op * f'"]
+  "DERIV f (of_real a) :> f' \<Longrightarrow> ((\<lambda>x. f (of_real x)) has_vector_derivative f') (at a within s)"
+  using has_derivative_compose[of of_real of_real a _ f "op * f'"]
   by (simp add: scaleR_conv_of_real ac_simps has_vector_derivative_def has_field_derivative_def)
 
 lemma fact_cancel:
@@ -33,10 +33,6 @@
   shows "of_nat (Suc n) * c / (fact (Suc n)) = c / (fact n)"
   by (simp add: of_nat_mult del: of_nat_Suc times_nat.simps)
 
-lemma linear_times:
-  fixes c::"'a::real_algebra" shows "linear (\<lambda>x. c * x)"
-  by (auto simp: linearI distrib_left)
-
 lemma bilinear_times:
   fixes c::"'a::real_algebra" shows "bilinear (\<lambda>x y::'a. x*y)"
   by (auto simp: bilinear_def distrib_left distrib_right intro!: linearI)
@@ -44,16 +40,6 @@
 lemma linear_cnj: "linear cnj"
   using bounded_linear.linear[OF bounded_linear_cnj] .
 
-lemma tendsto_mult_left:
-  fixes c::"'a::real_normed_algebra"
-  shows "(f ---> l) F \<Longrightarrow> ((\<lambda>x. c * (f x)) ---> c * l) F"
-by (rule tendsto_mult [OF tendsto_const])
-
-lemma tendsto_mult_right:
-  fixes c::"'a::real_normed_algebra"
-  shows "(f ---> l) F \<Longrightarrow> ((\<lambda>x. (f x) * c) ---> l * c) F"
-by (rule tendsto_mult [OF _ tendsto_const])
-
 lemma tendsto_Re_upper:
   assumes "~ (trivial_limit F)"
           "(f ---> l) F"
diff -r 4cf66f21b764 -r d2e62ae01cd8 src/HOL/Multivariate_Analysis/Complex_Transcendental.thy
--- a/src/HOL/Multivariate_Analysis/Complex_Transcendental.thy	Mon Dec 07 10:38:04 2015 +0100
+++ b/src/HOL/Multivariate_Analysis/Complex_Transcendental.thy	Mon Dec 07 16:44:26 2015 +0000
@@ -854,6 +854,13 @@
   obtains r a::real where "z = complex_of_real r * (cos a + \<i> * sin a)" "0 \<le> r" "0 \<le> a" "a < 2*pi"
   using Arg cis.ctr cis_conv_exp by fastforce
 
+lemma Re_Im_le_cmod: "Im w * sin \<phi> + Re w * cos \<phi> \<le> cmod w"
+proof (cases w rule: complex_split_polar)
+  case (1 r a) with sin_cos_le1 [of a \<phi>] show ?thesis
+    apply (simp add: norm_mult cmod_unit_one)
+    by (metis (no_types, hide_lams) abs_le_D1 distrib_left mult.commute mult.left_commute mult_left_le)
+qed
+
 subsection\<open>Analytic properties of tangent function\<close>
 
 lemma cnj_tan: "cnj(tan z) = tan(cnj z)"
diff -r 4cf66f21b764 -r d2e62ae01cd8 src/HOL/Multivariate_Analysis/Integration.thy
--- a/src/HOL/Multivariate_Analysis/Integration.thy	Mon Dec 07 10:38:04 2015 +0100
+++ b/src/HOL/Multivariate_Analysis/Integration.thy	Mon Dec 07 16:44:26 2015 +0000
@@ -2622,7 +2622,7 @@
 lemma integral_neg: "f integrable_on s \<Longrightarrow> integral s (\<lambda>x. - f x) = - integral s f"
   by (rule integral_unique) (metis integrable_integral has_integral_neg)
 
-lemma integral_sub: "f integrable_on s \<Longrightarrow> g integrable_on s \<Longrightarrow>
+lemma integral_diff: "f integrable_on s \<Longrightarrow> g integrable_on s \<Longrightarrow>
     integral s (\<lambda>x. f x - g x) = integral s f - integral s g"
   by (rule integral_unique) (metis integrable_integral has_integral_sub)
 
@@ -2645,7 +2645,7 @@
 lemma integrable_neg: "f integrable_on s \<Longrightarrow> (\<lambda>x. -f(x)) integrable_on s"
   unfolding integrable_on_def by(auto intro: has_integral_neg)
 
-lemma integrable_sub:
+lemma integrable_diff:
   "f integrable_on s \<Longrightarrow> g integrable_on s \<Longrightarrow> (\<lambda>x. f x - g x) integrable_on s"
   unfolding integrable_on_def by(auto intro: has_integral_sub)
 
@@ -4623,6 +4623,8 @@
   qed
 qed
 
+lemmas integrable_uniform_limit_real = integrable_uniform_limit [where 'a=real, simplified]
+
 
 subsection \<open>Negligible sets.\<close>
 
@@ -8933,19 +8935,19 @@
       have *: "\<And>x f g. (if x \<in> s then f x else 0) - (if x \<in> s then g x else 0) =
         (if x \<in> s then f x - g x else (0::real))"
         by auto
-      note ** = abs_of_nonneg[OF integral_nonneg[OF integrable_sub, OF h g]]
+      note ** = abs_of_nonneg[OF integral_nonneg[OF integrable_diff, OF h g]]
       show "norm (integral (cbox a b) (\<lambda>x. if x \<in> s then h x else 0) -
           integral (cbox a b) (\<lambda>x. if x \<in> s then g x else 0)) \<le>
         norm (integral (cbox c d) (\<lambda>x. if x \<in> s then h x else 0) -
           integral (cbox c d) (\<lambda>x. if x \<in> s then g x else 0))"
-        unfolding integral_sub[OF h g,symmetric] real_norm_def
+        unfolding integral_diff[OF h g,symmetric] real_norm_def
         apply (subst **)
         defer
         apply (subst **)
         defer
         apply (rule has_integral_subset_le)
         defer
-        apply (rule integrable_integral integrable_sub h g)+
+        apply (rule integrable_integral integrable_diff h g)+
       proof safe
         fix x
         assume "x \<in> cbox a b"
@@ -10123,7 +10125,7 @@
   qed
 
   have sub: "\<And>k. integral s (\<lambda>x. f k x - f 0 x) = integral s (f k) - integral s (f 0)"
-    apply (subst integral_sub)
+    apply (subst integral_diff)
     apply (rule assms(1)[rule_format])+
     apply rule
     done
@@ -10144,7 +10146,7 @@
   next
     case (2 k)
     then show ?case
-      apply (rule integrable_sub)
+      apply (rule integrable_diff)
       using assms(1)
       apply auto
       done
@@ -10182,7 +10184,7 @@
     apply -
     apply rule
     defer
-    apply (subst(asm) integral_sub)
+    apply (subst(asm) integral_diff)
     using assms(1)
     apply auto
     apply (rule LIMSEQ_imp_Suc)
@@ -11653,11 +11655,11 @@
             "J = integral (cbox a b) g"
           using I[of n] J by (simp_all add: integral_unique)
         then have "dist (I n) J = norm (integral (cbox a b) (\<lambda>x. f n x - g x))"
-          by (simp add: integral_sub dist_norm)
+          by (simp add: integral_diff dist_norm)
         also have "\<dots> \<le> integral (cbox a b) (\<lambda>x. (e' / content (cbox a b)))"
           using elim
           by (intro integral_norm_bound_integral)
-            (auto intro!: integrable_sub absolutely_integrable_onI)
+            (auto intro!: integrable_diff absolutely_integrable_onI)
         also have "\<dots> < e"
           using \<open>0 < e\<close>
           by (simp add: e'_def)
@@ -12029,12 +12031,12 @@
       apply clarify
       apply (rule le_less_trans [OF _ e2_less])
       apply (rule integrable_bound)
-      apply (auto intro: integrable_sub continuous_on_imp_integrable_on_Pair1)
+      apply (auto intro: integrable_diff continuous_on_imp_integrable_on_Pair1)
       done
   } note * = this
   show ?thesis
     apply (rule integrable_continuous)
-    apply (simp add: * continuous_on_iff dist_norm integral_sub [symmetric] continuous_on_imp_integrable_on_Pair1 [OF assms])
+    apply (simp add: * continuous_on_iff dist_norm integral_diff [symmetric] continuous_on_imp_integrable_on_Pair1 [OF assms])
     done
 qed
 
@@ -12217,10 +12219,10 @@
         by (blast intro: continuous_on_imp_integrable_on_Pair1)
       have 1: "norm (integral (cbox (u,w) (v,z)) f - integral (cbox (u,w) (v,z)) (\<lambda>x. f (t1,t2)))
          \<le> e * content (cbox (u,w) (v,z)) / content ?CBOX / 2"
-        apply (simp only: integral_sub [symmetric] f_int_uwvz integrable_const)
+        apply (simp only: integral_diff [symmetric] f_int_uwvz integrable_const)
         apply (rule order_trans [OF integrable_bound [of "e / content ?CBOX / 2"]])
         using cbp e' nf'
-        apply (auto simp: integrable_sub f_int_uwvz integrable_const)
+        apply (auto simp: integrable_diff f_int_uwvz integrable_const)
         done
       have int_integrable: "(\<lambda>x. integral (cbox w z) (\<lambda>y. f (x, y))) integrable_on cbox u v"
         using assms integral_integrable_2dim continuous_on_subset uwvz_sub(2) by blast
@@ -12228,24 +12230,24 @@
          "\<And>x. x \<in> cbox u v \<Longrightarrow>
                norm (integral (cbox w z) (\<lambda>y. f (x, y)) - integral (cbox w z) (\<lambda>y. f (t1, t2)))
                \<le> e * content (cbox w z) / content (cbox (a, c) (b, d)) / 2"
-        apply (simp only: integral_sub [symmetric] f_int_uv integrable_const)
+        apply (simp only: integral_diff [symmetric] f_int_uv integrable_const)
         apply (rule order_trans [OF integrable_bound [of "e / content ?CBOX / 2"]])
         using cbp e' nf'
-        apply (auto simp: integrable_sub f_int_uv integrable_const)
+        apply (auto simp: integrable_diff f_int_uv integrable_const)
         done
       have "norm (integral (cbox u v)
                (\<lambda>x. integral (cbox w z) (\<lambda>y. f (x,y)) - integral (cbox w z) (\<lambda>y. f (t1,t2))))
             \<le> e * content (cbox w z) / content ?CBOX / 2 * content (cbox u v)"
         apply (rule integrable_bound [OF _ _ normint_wz])
         using cbp e'
-        apply (auto simp: divide_simps content_pos_le integrable_sub int_integrable integrable_const)
+        apply (auto simp: divide_simps content_pos_le integrable_diff int_integrable integrable_const)
         done
       also have "... \<le> e * content (cbox (u,w) (v,z)) / content ?CBOX / 2"
         by (simp add: content_Pair divide_simps)
       finally have 2: "norm (integral (cbox u v) (\<lambda>x. integral (cbox w z) (\<lambda>y. f (x,y))) -
                       integral (cbox u v) (\<lambda>x. integral (cbox w z) (\<lambda>y. f (t1,t2))))
                 \<le> e * content (cbox (u,w) (v,z)) / content ?CBOX / 2"
-        by (simp only: integral_sub [symmetric] int_integrable integrable_const)
+        by (simp only: integral_diff [symmetric] int_integrable integrable_const)
       have norm_xx: "\<lbrakk>x' = y'; norm(x - x') \<le> e/2; norm(y - y') \<le> e/2\<rbrakk> \<Longrightarrow> norm(x - y) \<le> e" for x::'c and y x' y' e
         using norm_triangle_mono [of "x-y'" "e/2" "y'-y" "e/2"] real_sum_of_halves
         by (simp add: norm_minus_commute)
diff -r 4cf66f21b764 -r d2e62ae01cd8 src/HOL/Multivariate_Analysis/Path_Connected.thy
--- a/src/HOL/Multivariate_Analysis/Path_Connected.thy	Mon Dec 07 10:38:04 2015 +0100
+++ b/src/HOL/Multivariate_Analysis/Path_Connected.thy	Mon Dec 07 16:44:26 2015 +0000
@@ -1,5 +1,5 @@
 (*  Title:      HOL/Multivariate_Analysis/Path_Connected.thy
-    Author:     Robert Himmelmann, TU Muenchen, and LC Paulson with material from HOL Light
+    Authors:    LC Paulson and Robert Himmelmann (TU Muenchen), based on material from HOL Light
 *)
 
 section \<open>Continuous paths and path-connected sets\<close>
diff -r 4cf66f21b764 -r d2e62ae01cd8 src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy
--- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Mon Dec 07 10:38:04 2015 +0100
+++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Mon Dec 07 16:44:26 2015 +0000
@@ -2282,15 +2282,6 @@
 lemma trivial_limit_eq: "trivial_limit net \<longleftrightarrow> (\<forall>P. eventually P net)"
   by (simp add: filter_eq_iff)
 
-text\<open>Combining theorems for "eventually"\<close>
-
-lemma eventually_rev_mono:
-  "eventually P net \<Longrightarrow> (\<forall>x. P x \<longrightarrow> Q x) \<Longrightarrow> eventually Q net"
-  using eventually_mono [of P Q] by fast
-
-lemma not_eventually: "(\<forall>x. \<not> P x ) \<Longrightarrow> \<not> trivial_limit net \<Longrightarrow> \<not> eventually (\<lambda>x. P x) net"
-  by (simp add: eventually_False)
-
 
 subsection \<open>Limits\<close>
 
@@ -2319,7 +2310,7 @@
   by (auto simp add: tendsto_iff eventually_at_infinity)
 
 lemma Lim_eventually: "eventually (\<lambda>x. f x = l) net \<Longrightarrow> (f ---> l) net"
-  by (rule topological_tendstoI, auto elim: eventually_rev_mono)
+  by (rule topological_tendstoI, auto elim: eventually_mono')
 
 text\<open>The expected monotonicity property.\<close>
 
@@ -2998,7 +2989,7 @@
     by fast
 qed
 
-lemma closure_ball:
+lemma closure_ball [simp]:
   fixes x :: "'a::real_normed_vector"
   shows "0 < e \<Longrightarrow> closure (ball x e) = cball x e"
   apply (rule equalityI)
@@ -3016,7 +3007,7 @@
   done
 
 (* In a trivial vector space, this fails for e = 0. *)
-lemma interior_cball:
+lemma interior_cball [simp]:
   fixes x :: "'a::{real_normed_vector, perfect_space}"
   shows "interior (cball x e) = ball x e"
 proof (cases "e \<ge> 0")
@@ -3108,12 +3099,12 @@
   apply arith
   done
 
-lemma cball_eq_empty: "cball x e = {} \<longleftrightarrow> e < 0"
+lemma cball_eq_empty [simp]: "cball x e = {} \<longleftrightarrow> e < 0"
   apply (simp add: set_eq_iff not_le)
   apply (metis zero_le_dist dist_self order_less_le_trans)
   done
 
-lemma cball_empty: "e < 0 \<Longrightarrow> cball x e = {}"
+lemma cball_empty [simp]: "e < 0 \<Longrightarrow> cball x e = {}"
   by (simp add: cball_eq_empty)
 
 lemma cball_eq_sing:
@@ -3133,6 +3124,26 @@
   shows "e = 0 \<Longrightarrow> cball x e = {x}"
   by (auto simp add: set_eq_iff)
 
+lemma ball_divide_subset: "d \<ge> 1 \<Longrightarrow> ball x (e/d) \<subseteq> ball x e"
+  apply (cases "e \<le> 0")
+  apply (simp add: ball_empty divide_simps)
+  apply (rule subset_ball)
+  apply (simp add: divide_simps)
+  done
+
+lemma ball_divide_subset_numeral: "ball x (e / numeral w) \<subseteq> ball x e"
+  using ball_divide_subset one_le_numeral by blast
+
+lemma cball_divide_subset: "d \<ge> 1 \<Longrightarrow> cball x (e/d) \<subseteq> cball x e"
+  apply (cases "e < 0")
+  apply (simp add: divide_simps)
+  apply (rule subset_cball)
+  apply (metis divide_1 frac_le not_le order_refl zero_less_one)
+  done
+
+lemma cball_divide_subset_numeral: "cball x (e / numeral w) \<subseteq> cball x e"
+  using cball_divide_subset one_le_numeral by blast
+
 
 subsection \<open>Boundedness\<close>
 
@@ -5723,7 +5734,7 @@
     using \<open>open U\<close> and \<open>f x \<in> U\<close>
     unfolding tendsto_def by fast
   then have "eventually (\<lambda>y. f y \<noteq> a) (at x within s)"
-    using \<open>a \<notin> U\<close> by (fast elim: eventually_mono [rotated])
+    using \<open>a \<notin> U\<close> by (fast elim: eventually_mono')
   then show ?thesis
     using \<open>f x \<noteq> a\<close> by (auto simp: dist_commute zero_less_dist_iff eventually_at)
 qed
@@ -8206,9 +8217,8 @@
   qed
 next
   assume ?rhs then show ?lhs
-    apply (auto simp: ball_def dist_norm )
+    apply (auto simp: ball_def dist_norm)
     apply (metis add.commute add_le_cancel_right dist_norm dist_triangle_alt order_trans)
-    using le_less_trans apply fastforce
     done
 qed
 
@@ -8249,7 +8259,6 @@
   assume ?rhs then show ?lhs
     apply (auto simp: ball_def dist_norm )
     apply (metis add.commute add_le_cancel_right dist_norm dist_triangle_alt le_less_trans)
-    using le_less_trans apply fastforce
     done
 qed
 
@@ -8361,8 +8370,7 @@
     using \<open>?lhs\<close> ball_eq_empty cball_eq_empty apply blast+
     done
 next
-  assume ?rhs then show ?lhs
-    by (auto simp add: set_eq_subset ball_subset_cball_iff cball_subset_ball_iff)
+  assume ?rhs then show ?lhs by auto
 qed
 
 lemma cball_eq_ball_iff:
@@ -8377,8 +8385,7 @@
     using \<open>?lhs\<close> ball_eq_empty cball_eq_empty apply blast+
     done
 next
-  assume ?rhs then show ?lhs
-    by (auto simp add: set_eq_subset ball_subset_cball_iff cball_subset_ball_iff)
+  assume ?rhs then show ?lhs  using ball_eq_cball_iff by blast
 qed
 
 no_notation
diff -r 4cf66f21b764 -r d2e62ae01cd8 src/HOL/Multivariate_Analysis/Uniform_Limit.thy
--- a/src/HOL/Multivariate_Analysis/Uniform_Limit.thy	Mon Dec 07 10:38:04 2015 +0100
+++ b/src/HOL/Multivariate_Analysis/Uniform_Limit.thy	Mon Dec 07 16:44:26 2015 +0000
@@ -477,9 +477,7 @@
 
 lemma uniform_limit_on_subset:
   "uniform_limit J f g F \<Longrightarrow> I \<subseteq> J \<Longrightarrow> uniform_limit I f g F"
-  by (auto intro!: uniform_limitI dest!: uniform_limitD intro: eventually_rev_mono)
-
-
+  by (auto intro!: uniform_limitI dest!: uniform_limitD intro: eventually_mono')
 
 lemma uniformly_convergent_add:
   "uniformly_convergent_on A f \<Longrightarrow> uniformly_convergent_on A g\<Longrightarrow>
diff -r 4cf66f21b764 -r d2e62ae01cd8 src/HOL/NSA/HyperDef.thy
--- a/src/HOL/NSA/HyperDef.thy	Mon Dec 07 10:38:04 2015 +0100
+++ b/src/HOL/NSA/HyperDef.thy	Mon Dec 07 16:44:26 2015 +0000
@@ -231,7 +231,7 @@
 
 text{*A few lemmas first*}
 
-lemma lemma_omega_empty_singleton_disj: 
+lemma lemma_omega_empty_singleton_disj:
   "{n::nat. x = real n} = {} \<or> (\<exists>y. {n::nat. x = real n} = {y})"
 by force
 
@@ -243,8 +243,7 @@
 apply (simp add: omega_def star_of_def star_n_eq_iff)
 apply clarify
 apply (rule_tac x2="x-1" in lemma_finite_omega_set [THEN FreeUltrafilterNat.finite, THEN notE])
-apply (rule eventually_mono)
-prefer 2 apply assumption
+apply (erule eventually_mono')
 apply auto
 done
 
diff -r 4cf66f21b764 -r d2e62ae01cd8 src/HOL/NSA/NSA.thy
--- a/src/HOL/NSA/NSA.thy	Mon Dec 07 10:38:04 2015 +0100
+++ b/src/HOL/NSA/NSA.thy	Mon Dec 07 16:44:26 2015 +0000
@@ -2106,7 +2106,7 @@
 apply (simp add: omega_def)
 apply (rule FreeUltrafilterNat_HInfinite)
 apply clarify
-apply (rule_tac u1 = "u-1" in eventually_mono [OF _ FreeUltrafilterNat_nat_gt_real])
+apply (rule_tac u1 = "u-1" in eventually_mono' [OF FreeUltrafilterNat_nat_gt_real])
 apply auto
 done
 
diff -r 4cf66f21b764 -r d2e62ae01cd8 src/HOL/Topological_Spaces.thy
--- a/src/HOL/Topological_Spaces.thy	Mon Dec 07 10:38:04 2015 +0100
+++ b/src/HOL/Topological_Spaces.thy	Mon Dec 07 16:44:26 2015 +0000
@@ -1758,7 +1758,7 @@
   with \<open>finite D\<close> have "eventually (\<lambda>y. y \<notin> \<Union>D) (nhds y)"
     by (simp add: eventually_ball_finite)
   with \<open>s \<subseteq> \<Union>D\<close> have "eventually (\<lambda>y. y \<notin> s) (nhds y)"
-    by (auto elim!: eventually_mono [rotated])
+    by (auto elim!: eventually_mono')
   thus "\<exists>t. open t \<and> y \<in> t \<and> t \<subseteq> - s"
     by (simp add: eventually_nhds subset_eq)
 qed