src/HOL/Analysis/Cauchy_Integral_Theorem.thy

--- a/src/HOL/Analysis/Cauchy_Integral_Theorem.thy	Mon Aug 28 20:33:20 2017 +0100
+++ b/src/HOL/Analysis/Cauchy_Integral_Theorem.thy	Mon Aug 28 22:31:47 2017 +0100
@@ -3617,22 +3617,24 @@
       and ge: "\<And>x. \<lbrakk>0 < x; x < 1\<rbrakk> \<Longrightarrow> 0 \<le> Im (vector_derivative \<gamma> (at x) * cnj(\<gamma> x - z))"
     shows "0 \<le> Re(winding_number \<gamma> z)"
 proof -
-  have *: "0 \<le> Im (vector_derivative \<gamma> (at x) / (\<gamma> x - z))" if x: "0 < x" "x < 1" for x
+  have ge0: "0 \<le> Im (vector_derivative \<gamma> (at x) / (\<gamma> x - z))" if x: "0 < x" "x < 1" for x
     using ge by (simp add: Complex.Im_divide algebra_simps x)
-  show ?thesis
-    apply (simp add: Re_winding_number [OF \<gamma>] field_simps)
+  have hi: "((\<lambda>x. 1 / (\<gamma> x - z) * vector_derivative \<gamma> (at x)) has_integral contour_integral \<gamma> (\<lambda>w. 1 / (w - z)))
+            (cbox 0 1)"
+    unfolding box_real
+    apply (subst has_contour_integral [symmetric])
+    using \<gamma> by (simp add: contour_integrable_inversediff has_contour_integral_integral)
+  have "0 \<le> Im (contour_integral \<gamma> (\<lambda>w. 1 / (w - z)))"
     apply (rule has_integral_component_nonneg
              [of \<i> "\<lambda>x. if x \<in> {0<..<1}
                          then 1/(\<gamma> x - z) * vector_derivative \<gamma> (at x) else 0", simplified])
-      prefer 3 apply (force simp: *)
+      prefer 3 apply (force simp: ge0)
      apply (simp add: Basis_complex_def)
-    apply (rule has_integral_spike_interior [of 0 1 _ "\<lambda>x. 1/(\<gamma> x - z) * vector_derivative \<gamma> (at x)"])
+    apply (rule has_integral_spike_interior [OF hi])
     apply simp
-    apply (simp only: box_real)
-    apply (subst has_contour_integral [symmetric])
-    using \<gamma>
-    apply (simp add: contour_integrable_inversediff has_contour_integral_integral)
     done
+  then show ?thesis
+    by (simp add: Re_winding_number [OF \<gamma>] field_simps)
 qed
 
 lemma winding_number_pos_lt_lemma:
@@ -3641,19 +3643,20 @@
       and ge: "\<And>x. \<lbrakk>0 < x; x < 1\<rbrakk> \<Longrightarrow> e \<le> Im (vector_derivative \<gamma> (at x) / (\<gamma> x - z))"
     shows "0 < Re(winding_number \<gamma> z)"
 proof -
+  have hi: "((\<lambda>x. 1 / (\<gamma> x - z) * vector_derivative \<gamma> (at x)) has_integral contour_integral \<gamma> (\<lambda>w. 1 / (w - z)))
+            (cbox 0 1)"
+    unfolding box_real
+    apply (subst has_contour_integral [symmetric])
+    using \<gamma> by (simp add: contour_integrable_inversediff has_contour_integral_integral)
   have "e \<le> Im (contour_integral \<gamma> (\<lambda>w. 1 / (w - z)))"
     apply (rule has_integral_component_le
              [of \<i> "\<lambda>x. \<i>*e" "\<i>*e" "{0..1}"
                     "\<lambda>x. if x \<in> {0<..<1} then 1/(\<gamma> x - z) * vector_derivative \<gamma> (at x) else \<i>*e"
                     "contour_integral \<gamma> (\<lambda>w. 1/(w - z))", simplified])
-    using e
-    apply (simp_all add: Basis_complex_def)
+    using e apply (simp_all add: Basis_complex_def)
     using has_integral_const_real [of _ 0 1] apply force
-    apply (rule has_integral_spike_interior [of 0 1 _ "\<lambda>x. 1/(\<gamma> x - z) * vector_derivative \<gamma> (at x)", simplified box_real])
-    apply simp
-    apply (subst has_contour_integral [symmetric])
-    using \<gamma>
-    apply (simp_all add: contour_integrable_inversediff has_contour_integral_integral ge)
+     apply (rule has_integral_spike_interior [OF hi, simplified box_real])
+    apply (simp_all add: ge)
     done
   with e show ?thesis
     by (simp add: Re_winding_number [OF \<gamma>] field_simps)