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