src/HOL/Analysis/Cauchy_Integral_Theorem.thy
 changeset 66793 deabce3ccf1f parent 66708 015a95f15040 child 66827 c94531b5007d
```     1.1 --- a/src/HOL/Analysis/Cauchy_Integral_Theorem.thy	Sun Oct 08 16:50:37 2017 +0200
1.2 +++ b/src/HOL/Analysis/Cauchy_Integral_Theorem.thy	Mon Oct 09 15:34:23 2017 +0100
1.3 @@ -180,7 +180,7 @@
1.4          have "f differentiable at x within ({a<..<c} - s)"
1.5            apply (rule differentiable_at_withinI)
1.6            using x le st
1.7 -          by (metis (no_types, lifting) DiffD1 DiffD2 DiffI UnCI atLeastAtMost_diff_ends atLeastAtMost_iff at_within_interior insert_iff interior_atLeastAtMost le st(3) x)
1.8 +          by (metis (no_types, lifting) DiffD1 DiffD2 DiffI UnCI atLeastAtMost_diff_ends atLeastAtMost_iff at_within_interior insert_iff interior_atLeastAtMost_real le st(3) x)
1.9          moreover have "open ({a<..<c} - s)"
1.10            by (blast intro: open_greaterThanLessThan \<open>finite s\<close> finite_imp_closed)
1.11          ultimately show "f differentiable at x within {a..b}"
1.12 @@ -192,7 +192,7 @@
1.13          have "g differentiable at x within ({c<..<b} - t)"
1.14            apply (rule differentiable_at_withinI)
1.15            using x ge st
1.16 -          by (metis DiffD1 DiffD2 DiffI UnCI atLeastAtMost_diff_ends atLeastAtMost_iff at_within_interior insert_iff interior_atLeastAtMost)
1.17 +          by (metis DiffD1 DiffD2 DiffI UnCI atLeastAtMost_diff_ends atLeastAtMost_iff at_within_interior insert_iff interior_atLeastAtMost_real)
1.18          moreover have "open ({c<..<b} - t)"
1.19            by (blast intro: open_greaterThanLessThan \<open>finite t\<close> finite_imp_closed)
1.20          ultimately show "g differentiable at x within {a..b}"
1.21 @@ -1446,7 +1446,7 @@
1.22    show ?thesis
1.23      apply (rule fundamental_theorem_of_calculus_interior_strong)
1.24      using k assms cfg *
1.25 -    apply (auto simp: at_within_closed_interval)
1.26 +    apply (auto simp: at_within_Icc_at)
1.27      done
1.28  qed
1.29
1.30 @@ -4158,7 +4158,7 @@
1.31
1.32  subsection\<open>Winding number is zero "outside" a curve, in various senses\<close>
1.33
1.34 -lemma winding_number_zero_in_outside:
1.35 +proposition winding_number_zero_in_outside:
1.36    assumes \<gamma>: "path \<gamma>" and loop: "pathfinish \<gamma> = pathstart \<gamma>" and z: "z \<in> outside (path_image \<gamma>)"
1.37      shows "winding_number \<gamma> z = 0"
1.38  proof -
1.39 @@ -4210,7 +4210,11 @@
1.40    finally show ?thesis .
1.41  qed
1.42
1.43 -lemma winding_number_zero_outside:
1.44 +corollary winding_number_zero_const: "a \<noteq> z \<Longrightarrow> winding_number (\<lambda>t. a) z = 0"
1.45 +  by (rule winding_number_zero_in_outside)
1.46 +     (auto simp: pathfinish_def pathstart_def path_polynomial_function)
1.47 +
1.48 +corollary winding_number_zero_outside:
1.49      "\<lbrakk>path \<gamma>; convex s; pathfinish \<gamma> = pathstart \<gamma>; z \<notin> s; path_image \<gamma> \<subseteq> s\<rbrakk> \<Longrightarrow> winding_number \<gamma> z = 0"
1.50    by (meson convex_in_outside outside_mono subsetCE winding_number_zero_in_outside)
1.51
```