author paulson Mon, 05 Oct 2020 20:58:23 +0100 changeset 72382 6cacbdb53637 parent 72381 15ea20d8a4d6 child 72383 698b58513fd1
still not quite fixed...
```--- a/src/HOL/Complex_Analysis/Cauchy_Integral_Theorem.thy	Mon Oct 05 18:48:41 2020 +0100
+++ b/src/HOL/Complex_Analysis/Cauchy_Integral_Theorem.thy	Mon Oct 05 20:58:23 2020 +0100
@@ -1366,11 +1366,7 @@
and p: "polynomial_function p" "path_image p \<subseteq> S"
and pi: "\<And>f. f holomorphic_on S \<Longrightarrow> contour_integral g f = contour_integral p f"
using contour_integral_nearby_ends [OF S \<open>path g\<close> pag]
-    apply clarify
-    apply (drule_tac x=g in spec)
-    apply (simp only: assms)
-    apply (force simp: valid_path_polynomial_function dest: path_approx_polynomial_function)
-    done
+    by (metis cancel_comm_monoid_add_class.diff_cancel g norm_zero path_approx_polynomial_function valid_path_polynomial_function)
then obtain p' where p': "polynomial_function p'"
"\<And>x. (p has_vector_derivative (p' x)) (at x)"
by (blast intro: has_vector_derivative_polynomial_function that)```
```--- a/src/HOL/Complex_Analysis/Winding_Numbers.thy	Mon Oct 05 18:48:41 2020 +0100
+++ b/src/HOL/Complex_Analysis/Winding_Numbers.thy	Mon Oct 05 20:58:23 2020 +0100
@@ -41,7 +41,8 @@
assume e: "e>0"
obtain p where p: "polynomial_function p \<and>
pathstart p = pathstart \<gamma> \<and> pathfinish p = pathfinish \<gamma> \<and> (\<forall>t\<in>{0..1}. cmod (p t - \<gamma> t) < min e (d/2))"
-        using path_approx_polynomial_function [OF \<open>path \<gamma>\<close>, of "min e (d/2)"] d \<open>0<e\<close> by auto
+        using path_approx_polynomial_function [OF \<open>path \<gamma>\<close>, of "min e (d/2)"] d \<open>0<e\<close>
+        by (metis min_less_iff_conj zero_less_divide_iff zero_less_numeral)
have "(\<lambda>w. 1 / (w - z)) holomorphic_on UNIV - {z}"
by (auto simp: intro!: holomorphic_intros)
then have "winding_number_prop \<gamma> z e p nn"
@@ -845,7 +846,8 @@
obtain p where p: "polynomial_function p" "pathstart p = pathstart \<gamma>" "pathfinish p = pathfinish \<gamma>"
and pg1: "(\<And>t. \<lbrakk>0 \<le> t; t \<le> 1\<rbrakk> \<Longrightarrow> cmod (p t - \<gamma> t) < 1)"
and pge: "(\<And>t. \<lbrakk>0 \<le> t; t \<le> 1\<rbrakk> \<Longrightarrow> cmod (p t - \<gamma> t) < e)"
-        using path_approx_polynomial_function [OF \<gamma>, of "min 1 e"] \<open>e>0\<close> by force
+        using path_approx_polynomial_function [OF \<gamma>, of "min 1 e"] \<open>e>0\<close>
+        by (metis atLeastAtMost_iff min_less_iff_conj zero_less_one)
have pip: "path_image p \<subseteq> ball 0 (B + 1)"
using B
apply (clarsimp simp add: path_image_def dist_norm ball_def)```