New material about paths, winding numbers, etc. Added lemmas to divide_const_simps. Misc tuning.
authorpaulson <lp15@cam.ac.uk>
Mon Nov 23 16:57:54 2015 +0000 (2015-11-23)
changeset 61738c4f6031f1310
parent 61736 d6b2d638af23
child 61739 94ea89d7c5eb
New material about paths, winding numbers, etc. Added lemmas to divide_const_simps. Misc tuning.
src/HOL/Archimedean_Field.thy
src/HOL/Binomial.thy
src/HOL/Int.thy
src/HOL/Library/Extended_Real.thy
src/HOL/Limits.thy
src/HOL/Multivariate_Analysis/Cauchy_Integral_Thm.thy
src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy
src/HOL/Multivariate_Analysis/Path_Connected.thy
src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy
src/HOL/Topological_Spaces.thy
src/HOL/Transcendental.thy
     1.1 --- a/src/HOL/Archimedean_Field.thy	Sun Nov 22 23:19:43 2015 +0100
     1.2 +++ b/src/HOL/Archimedean_Field.thy	Mon Nov 23 16:57:54 2015 +0000
     1.3 @@ -657,7 +657,7 @@
     1.4  proof (cases "of_int m \<ge> z")
     1.5    case True
     1.6    hence "\<bar>z - of_int (round z)\<bar> \<le> \<bar>of_int (ceiling z) - z\<bar>"
     1.7 -    unfolding round_altdef by (simp add: ceiling_altdef frac_def) linarith?
     1.8 +    unfolding round_altdef by (simp add: field_simps ceiling_altdef frac_def) linarith?
     1.9    also have "of_int \<lceil>z\<rceil> - z \<ge> 0" by linarith
    1.10    with True have "\<bar>of_int (ceiling z) - z\<bar> \<le> \<bar>z - of_int m\<bar>"
    1.11      by (simp add: ceiling_le_iff)
    1.12 @@ -665,7 +665,7 @@
    1.13  next
    1.14    case False
    1.15    hence "\<bar>z - of_int (round z)\<bar> \<le> \<bar>of_int (floor z) - z\<bar>"
    1.16 -    unfolding round_altdef by (simp add: ceiling_altdef frac_def) linarith?
    1.17 +    unfolding round_altdef by (simp add: field_simps ceiling_altdef frac_def) linarith?
    1.18    also have "z - of_int \<lfloor>z\<rfloor> \<ge> 0" by linarith
    1.19    with False have "\<bar>of_int (floor z) - z\<bar> \<le> \<bar>z - of_int m\<bar>"
    1.20      by (simp add: le_floor_iff)
     2.1 --- a/src/HOL/Binomial.thy	Sun Nov 22 23:19:43 2015 +0100
     2.2 +++ b/src/HOL/Binomial.thy	Mon Nov 23 16:57:54 2015 +0000
     2.3 @@ -842,7 +842,7 @@
     2.4  next
     2.5    case (Suc m)
     2.6    from Suc show ?case
     2.7 -    by (simp add: algebra_simps distrib gbinomial_mult_1)
     2.8 +    by (simp add: field_simps distrib gbinomial_mult_1)
     2.9  qed
    2.10  
    2.11  lemma binomial_symmetric:
    2.12 @@ -1131,7 +1131,7 @@
    2.13  proof (induction m)
    2.14    case (Suc mm)
    2.15    hence "(\<Sum>k\<le>Suc mm. (r gchoose k) * (r / 2 - of_nat k)) = 
    2.16 -             (r - of_nat (Suc mm)) * (r gchoose Suc mm) / 2" by (simp add: algebra_simps)
    2.17 +             (r - of_nat (Suc mm)) * (r gchoose Suc mm) / 2" by (simp add: field_simps)
    2.18    also have "\<dots> = r * (r - 1 gchoose Suc mm) / 2" by (subst gbinomial_absorb_comp) (rule refl)
    2.19    also have "\<dots> = (of_nat (Suc mm) + 1) / 2 * (r gchoose (Suc mm + 1))"
    2.20      by (subst gbinomial_absorption [symmetric]) simp
     3.1 --- a/src/HOL/Int.thy	Sun Nov 22 23:19:43 2015 +0100
     3.2 +++ b/src/HOL/Int.thy	Mon Nov 23 16:57:54 2015 +0000
     3.3 @@ -1263,27 +1263,29 @@
     3.4  
     3.5  text \<open>Multiplying out constant divisors in comparisons (@{text "<"}, @{text "\<le>"} and @{text "="})\<close>
     3.6  
     3.7 -lemmas le_divide_eq_numeral1 [simp] =
     3.8 +named_theorems divide_const_simps "simplification rules to simplify comparisons involving constant divisors"
     3.9 +
    3.10 +lemmas le_divide_eq_numeral1 [simp,divide_const_simps] =
    3.11    pos_le_divide_eq [of "numeral w", OF zero_less_numeral]
    3.12    neg_le_divide_eq [of "- numeral w", OF neg_numeral_less_zero] for w
    3.13  
    3.14 -lemmas divide_le_eq_numeral1 [simp] =
    3.15 +lemmas divide_le_eq_numeral1 [simp,divide_const_simps] =
    3.16    pos_divide_le_eq [of "numeral w", OF zero_less_numeral]
    3.17    neg_divide_le_eq [of "- numeral w", OF neg_numeral_less_zero] for w
    3.18  
    3.19 -lemmas less_divide_eq_numeral1 [simp] =
    3.20 +lemmas less_divide_eq_numeral1 [simp,divide_const_simps] =
    3.21    pos_less_divide_eq [of "numeral w", OF zero_less_numeral]
    3.22    neg_less_divide_eq [of "- numeral w", OF neg_numeral_less_zero] for w
    3.23  
    3.24 -lemmas divide_less_eq_numeral1 [simp] =
    3.25 +lemmas divide_less_eq_numeral1 [simp,divide_const_simps] =
    3.26    pos_divide_less_eq [of "numeral w", OF zero_less_numeral]
    3.27    neg_divide_less_eq [of "- numeral w", OF neg_numeral_less_zero] for w
    3.28  
    3.29 -lemmas eq_divide_eq_numeral1 [simp] =
    3.30 +lemmas eq_divide_eq_numeral1 [simp,divide_const_simps] =
    3.31    eq_divide_eq [of _ _ "numeral w"]
    3.32    eq_divide_eq [of _ _ "- numeral w"] for w
    3.33  
    3.34 -lemmas divide_eq_eq_numeral1 [simp] =
    3.35 +lemmas divide_eq_eq_numeral1 [simp,divide_const_simps] =
    3.36    divide_eq_eq [of _ "numeral w"]
    3.37    divide_eq_eq [of _ "- numeral w"] for w
    3.38  
    3.39 @@ -1292,36 +1294,33 @@
    3.40  
    3.41  text\<open>Simplify quotients that are compared with a literal constant.\<close>
    3.42  
    3.43 -lemmas le_divide_eq_numeral =
    3.44 +lemmas le_divide_eq_numeral [divide_const_simps] =
    3.45    le_divide_eq [of "numeral w"]
    3.46    le_divide_eq [of "- numeral w"] for w
    3.47  
    3.48 -lemmas divide_le_eq_numeral =
    3.49 +lemmas divide_le_eq_numeral [divide_const_simps] =
    3.50    divide_le_eq [of _ _ "numeral w"]
    3.51    divide_le_eq [of _ _ "- numeral w"] for w
    3.52  
    3.53 -lemmas less_divide_eq_numeral =
    3.54 +lemmas less_divide_eq_numeral [divide_const_simps] =
    3.55    less_divide_eq [of "numeral w"]
    3.56    less_divide_eq [of "- numeral w"] for w
    3.57  
    3.58 -lemmas divide_less_eq_numeral =
    3.59 +lemmas divide_less_eq_numeral [divide_const_simps] =
    3.60    divide_less_eq [of _ _ "numeral w"]
    3.61    divide_less_eq [of _ _ "- numeral w"] for w
    3.62  
    3.63 -lemmas eq_divide_eq_numeral =
    3.64 +lemmas eq_divide_eq_numeral [divide_const_simps] =
    3.65    eq_divide_eq [of "numeral w"]
    3.66    eq_divide_eq [of "- numeral w"] for w
    3.67  
    3.68 -lemmas divide_eq_eq_numeral =
    3.69 +lemmas divide_eq_eq_numeral [divide_const_simps] =
    3.70    divide_eq_eq [of _ _ "numeral w"]
    3.71    divide_eq_eq [of _ _ "- numeral w"] for w
    3.72  
    3.73  
    3.74  text\<open>Not good as automatic simprules because they cause case splits.\<close>
    3.75 -lemmas divide_const_simps =
    3.76 -  le_divide_eq_numeral divide_le_eq_numeral less_divide_eq_numeral
    3.77 -  divide_less_eq_numeral eq_divide_eq_numeral divide_eq_eq_numeral
    3.78 -  le_divide_eq_1 divide_le_eq_1 less_divide_eq_1 divide_less_eq_1
    3.79 +lemmas [divide_const_simps] = le_divide_eq_1 divide_le_eq_1 less_divide_eq_1 divide_less_eq_1 
    3.80  
    3.81  
    3.82  subsection \<open>The divides relation\<close>
     4.1 --- a/src/HOL/Library/Extended_Real.thy	Sun Nov 22 23:19:43 2015 +0100
     4.2 +++ b/src/HOL/Library/Extended_Real.thy	Mon Nov 23 16:57:54 2015 +0000
     4.3 @@ -36,7 +36,7 @@
     4.4    assume "x = bot" then show ?thesis
     4.5      by (simp add: trivial_limit_at_left_bot)
     4.6  next
     4.7 -  assume x: "x \<noteq> bot" 
     4.8 +  assume x: "x \<noteq> bot"
     4.9    show ?thesis
    4.10      unfolding continuous_within
    4.11    proof (intro tendsto_at_left_sequentially[of bot])
    4.12 @@ -54,7 +54,7 @@
    4.13    shows "sup_continuous f \<longleftrightarrow> (\<forall>x. continuous (at_left x) f) \<and> mono f"
    4.14    using sup_continuous_at_left[of f] continuous_at_left_imp_sup_continuous[of f]
    4.15      sup_continuous_mono[of f] by auto
    4.16 -  
    4.17 +
    4.18  lemma continuous_at_right_imp_inf_continuous:
    4.19    fixes f :: "'a \<Rightarrow> 'a::{complete_linorder, linorder_topology}"
    4.20    assumes "mono f" "\<And>x. continuous (at_right x) f"
    4.21 @@ -73,7 +73,7 @@
    4.22    assume "x = top" then show ?thesis
    4.23      by (simp add: trivial_limit_at_right_top)
    4.24  next
    4.25 -  assume x: "x \<noteq> top" 
    4.26 +  assume x: "x \<noteq> top"
    4.27    show ?thesis
    4.28      unfolding continuous_within
    4.29    proof (intro tendsto_at_right_sequentially[of _ top])
    4.30 @@ -593,7 +593,7 @@
    4.31    by (cases x) auto
    4.32  
    4.33  lemma ereal_abs_leI:
    4.34 -  fixes x y :: ereal 
    4.35 +  fixes x y :: ereal
    4.36    shows "\<lbrakk> x \<le> y; -x \<le> y \<rbrakk> \<Longrightarrow> \<bar>x\<bar> \<le> y"
    4.37  by(cases x y rule: ereal2_cases)(simp_all)
    4.38  
    4.39 @@ -881,7 +881,7 @@
    4.40  
    4.41  end
    4.42  
    4.43 -lemma [simp]: 
    4.44 +lemma [simp]:
    4.45    shows ereal_1_times: "ereal 1 * x = x"
    4.46    and times_ereal_1: "x * ereal 1 = x"
    4.47  by(simp_all add: one_ereal_def[symmetric])
    4.48 @@ -1034,7 +1034,7 @@
    4.49    shows  "c = d \<Longrightarrow> (d \<noteq> 0 \<Longrightarrow> a = b) \<Longrightarrow> a * c = b * d"
    4.50    by (cases "c = 0") simp_all
    4.51  
    4.52 -lemma ereal_right_mult_cong: 
    4.53 +lemma ereal_right_mult_cong:
    4.54    fixes a b c :: ereal
    4.55    shows "c = d \<Longrightarrow> (d \<noteq> 0 \<Longrightarrow> a = b) \<Longrightarrow> c * a = d * b"
    4.56    by (cases "c = 0") simp_all
    4.57 @@ -1402,7 +1402,7 @@
    4.58    by (cases x y rule: ereal2_cases) simp_all
    4.59  
    4.60  lemma ereal_diff_add_eq_diff_diff_swap:
    4.61 -  fixes x y z :: ereal 
    4.62 +  fixes x y z :: ereal
    4.63    shows "\<bar>y\<bar> \<noteq> \<infinity> \<Longrightarrow> x - (y + z) = x - y - z"
    4.64  by(cases x y z rule: ereal3_cases) simp_all
    4.65  
    4.66 @@ -1414,8 +1414,8 @@
    4.67  lemma ereal_add_uminus_conv_diff: fixes x y z :: ereal shows "- x + y = y - x"
    4.68  by(cases x y rule: ereal2_cases) simp_all
    4.69  
    4.70 -lemma ereal_minus_diff_eq: 
    4.71 -  fixes x y :: ereal 
    4.72 +lemma ereal_minus_diff_eq:
    4.73 +  fixes x y :: ereal
    4.74    shows "\<lbrakk> x = \<infinity> \<longrightarrow> y \<noteq> \<infinity>; x = -\<infinity> \<longrightarrow> y \<noteq> - \<infinity> \<rbrakk> \<Longrightarrow> - (x - y) = y - x"
    4.75  by(cases x y rule: ereal2_cases) simp_all
    4.76  
    4.77 @@ -1745,13 +1745,9 @@
    4.78  
    4.79  end
    4.80  
    4.81 -lemma continuous_on_compose': 
    4.82 -  "continuous_on s f \<Longrightarrow> continuous_on t g \<Longrightarrow> f`s \<subseteq> t \<Longrightarrow> continuous_on s (\<lambda>x. g (f x))"
    4.83 -  using continuous_on_compose[of s f g] continuous_on_subset[of t g "f`s"] by auto
    4.84 -
    4.85  lemma continuous_on_ereal[continuous_intros]:
    4.86    assumes f: "continuous_on s f" shows "continuous_on s (\<lambda>x. ereal (f x))"
    4.87 -  by (rule continuous_on_compose'[OF f continuous_onI_mono[of ereal UNIV]]) auto
    4.88 +  by (rule continuous_on_compose2 [OF continuous_onI_mono[of ereal UNIV] f]) auto
    4.89  
    4.90  lemma tendsto_ereal[tendsto_intros, simp, intro]: "(f ---> x) F \<Longrightarrow> ((\<lambda>x. ereal (f x)) ---> ereal x) F"
    4.91    using isCont_tendsto_compose[of x ereal f F] continuous_on_ereal[of UNIV "\<lambda>x. x"]
    4.92 @@ -1807,7 +1803,7 @@
    4.93        by (auto simp: ereal_uminus_reorder ereal_less_uminus_reorder[of 0])
    4.94      then have "((\<lambda>x. (- c) * f x) ---> (- c) * x) F"
    4.95        by (rule *)
    4.96 -    from tendsto_uminus_ereal[OF this] show ?thesis 
    4.97 +    from tendsto_uminus_ereal[OF this] show ?thesis
    4.98        by simp
    4.99    qed (auto intro!: *)
   4.100  qed
   4.101 @@ -2119,7 +2115,7 @@
   4.102               intro!: ereal_mult_left_mono c)
   4.103  qed
   4.104  
   4.105 -lemma countable_approach: 
   4.106 +lemma countable_approach:
   4.107    fixes x :: ereal
   4.108    assumes "x \<noteq> -\<infinity>"
   4.109    shows "\<exists>f. incseq f \<and> (\<forall>i::nat. f i < x) \<and> (f ----> x)"
   4.110 @@ -2129,7 +2125,7 @@
   4.111      by (intro tendsto_intros LIMSEQ_inverse_real_of_nat)
   4.112    ultimately show ?thesis
   4.113      by (intro exI[of _ "\<lambda>n. x - inverse (Suc n)"]) (auto simp: incseq_def)
   4.114 -next 
   4.115 +next
   4.116    case PInf with LIMSEQ_SUP[of "\<lambda>n::nat. ereal (real n)"] show ?thesis
   4.117      by (intro exI[of _ "\<lambda>n. ereal (real n)"]) (auto simp: incseq_def SUP_nat_Infty)
   4.118  qed (simp add: assms)
   4.119 @@ -3275,7 +3271,7 @@
   4.120      next
   4.121        fix i j assume "i \<in> I" "j \<in> I"
   4.122        from directed[OF \<open>insert n N \<subseteq> A\<close> this] guess k ..
   4.123 -      then show "\<exists>k\<in>I. f n i + (\<Sum>l\<in>N. f l j) \<le> f n k + (\<Sum>l\<in>N. f l k)" 
   4.124 +      then show "\<exists>k\<in>I. f n i + (\<Sum>l\<in>N. f l j) \<le> f n k + (\<Sum>l\<in>N. f l k)"
   4.125          by (intro bexI[of _ k]) (auto intro!: ereal_add_mono setsum_mono)
   4.126      qed
   4.127      ultimately show ?case
   4.128 @@ -3475,7 +3471,7 @@
   4.129    shows "X ----> L"
   4.130  proof -
   4.131    from 1 2 have "limsup X \<le> liminf X" by auto
   4.132 -  hence 3: "limsup X = liminf X"  
   4.133 +  hence 3: "limsup X = liminf X"
   4.134      apply (subst eq_iff, rule conjI)
   4.135      by (rule Liminf_le_Limsup, auto)
   4.136    hence 4: "convergent (\<lambda>n. ereal (X n))"
   4.137 @@ -3486,7 +3482,7 @@
   4.138    finally have "lim (\<lambda>n. ereal(X n)) = L" ..
   4.139    hence "(\<lambda>n. ereal (X n)) ----> L"
   4.140      apply (elim subst)
   4.141 -    by (subst convergent_LIMSEQ_iff [symmetric], rule 4) 
   4.142 +    by (subst convergent_LIMSEQ_iff [symmetric], rule 4)
   4.143    thus ?thesis by simp
   4.144  qed
   4.145  
   4.146 @@ -3642,14 +3638,14 @@
   4.147  proof -
   4.148    have **: "((\<lambda>x. ereal (inverse x)) ---> ereal 0) at_infinity"
   4.149      by (intro tendsto_intros tendsto_inverse_0)
   4.150 -  
   4.151 +
   4.152    show ?thesis
   4.153      by (simp add: at_infty_ereal_eq_at_top tendsto_compose_filtermap[symmetric] comp_def)
   4.154         (auto simp: eventually_at_top_linorder exI[of _ 1] zero_ereal_def at_top_le_at_infinity
   4.155               intro!: filterlim_mono_eventually[OF **])
   4.156  qed
   4.157  
   4.158 -lemma inverse_ereal_tendsto_pos: 
   4.159 +lemma inverse_ereal_tendsto_pos:
   4.160    fixes x :: ereal assumes "0 < x"
   4.161    shows "inverse -- x --> inverse x"
   4.162  proof (cases x)
     5.1 --- a/src/HOL/Limits.thy	Sun Nov 22 23:19:43 2015 +0100
     5.2 +++ b/src/HOL/Limits.thy	Mon Nov 23 16:57:54 2015 +0000
     5.3 @@ -631,7 +631,7 @@
     5.4    unfolding continuous_def by (rule tendsto_diff)
     5.5  
     5.6  lemma continuous_on_diff [continuous_intros]:
     5.7 -  fixes f g :: "'a::t2_space \<Rightarrow> 'b::real_normed_vector"
     5.8 +  fixes f g :: "_ \<Rightarrow> 'b::real_normed_vector"
     5.9    shows "continuous_on s f \<Longrightarrow> continuous_on s g \<Longrightarrow> continuous_on s (\<lambda>x. f x - g x)"
    5.10    unfolding continuous_on_def by (auto intro: tendsto_diff)
    5.11  
     6.1 --- a/src/HOL/Multivariate_Analysis/Cauchy_Integral_Thm.thy	Sun Nov 22 23:19:43 2015 +0100
     6.2 +++ b/src/HOL/Multivariate_Analysis/Cauchy_Integral_Thm.thy	Mon Nov 23 16:57:54 2015 +0000
     6.3 @@ -3,7 +3,7 @@
     6.4  text\<open>By John Harrison et al.  Ported from HOL Light by L C Paulson (2015)\<close>
     6.5  
     6.6  theory Cauchy_Integral_Thm
     6.7 -imports Complex_Transcendental Weierstrass
     6.8 +imports Complex_Transcendental Weierstrass Ordered_Euclidean_Space
     6.9  begin
    6.10  
    6.11  subsection \<open>Piecewise differentiable functions\<close>
    6.12 @@ -553,33 +553,33 @@
    6.13  
    6.14  text\<open>piecewise differentiable function on [0,1]\<close>
    6.15  
    6.16 -definition has_path_integral :: "(complex \<Rightarrow> complex) \<Rightarrow> complex \<Rightarrow> (real \<Rightarrow> complex) \<Rightarrow> bool"
    6.17 -           (infixr "has'_path'_integral" 50)
    6.18 -  where "(f has_path_integral i) g \<equiv>
    6.19 +definition has_contour_integral :: "(complex \<Rightarrow> complex) \<Rightarrow> complex \<Rightarrow> (real \<Rightarrow> complex) \<Rightarrow> bool"
    6.20 +           (infixr "has'_contour'_integral" 50)
    6.21 +  where "(f has_contour_integral i) g \<equiv>
    6.22             ((\<lambda>x. f(g x) * vector_derivative g (at x within {0..1}))
    6.23              has_integral i) {0..1}"
    6.24  
    6.25 -definition path_integrable_on
    6.26 -           (infixr "path'_integrable'_on" 50)
    6.27 -  where "f path_integrable_on g \<equiv> \<exists>i. (f has_path_integral i) g"
    6.28 -
    6.29 -definition path_integral
    6.30 -  where "path_integral g f \<equiv> @i. (f has_path_integral i) g"
    6.31 -
    6.32 -lemma path_integral_unique: "(f has_path_integral i)  g \<Longrightarrow> path_integral g f = i"
    6.33 -  by (auto simp: path_integral_def has_path_integral_def integral_def [symmetric])
    6.34 -
    6.35 -lemma has_path_integral_integral:
    6.36 -    "f path_integrable_on i \<Longrightarrow> (f has_path_integral (path_integral i f)) i"
    6.37 -  by (metis path_integral_unique path_integrable_on_def)
    6.38 -
    6.39 -lemma has_path_integral_unique:
    6.40 -    "(f has_path_integral i) g \<Longrightarrow> (f has_path_integral j) g \<Longrightarrow> i = j"
    6.41 +definition contour_integrable_on
    6.42 +           (infixr "contour'_integrable'_on" 50)
    6.43 +  where "f contour_integrable_on g \<equiv> \<exists>i. (f has_contour_integral i) g"
    6.44 +
    6.45 +definition contour_integral
    6.46 +  where "contour_integral g f \<equiv> @i. (f has_contour_integral i) g"
    6.47 +
    6.48 +lemma contour_integral_unique: "(f has_contour_integral i)  g \<Longrightarrow> contour_integral g f = i"
    6.49 +  by (auto simp: contour_integral_def has_contour_integral_def integral_def [symmetric])
    6.50 +
    6.51 +lemma has_contour_integral_integral:
    6.52 +    "f contour_integrable_on i \<Longrightarrow> (f has_contour_integral (contour_integral i f)) i"
    6.53 +  by (metis contour_integral_unique contour_integrable_on_def)
    6.54 +
    6.55 +lemma has_contour_integral_unique:
    6.56 +    "(f has_contour_integral i) g \<Longrightarrow> (f has_contour_integral j) g \<Longrightarrow> i = j"
    6.57    using has_integral_unique
    6.58 -  by (auto simp: has_path_integral_def)
    6.59 -
    6.60 -lemma has_path_integral_integrable: "(f has_path_integral i) g \<Longrightarrow> f path_integrable_on g"
    6.61 -  using path_integrable_on_def by blast
    6.62 +  by (auto simp: has_contour_integral_def)
    6.63 +
    6.64 +lemma has_contour_integral_integrable: "(f has_contour_integral i) g \<Longrightarrow> f contour_integrable_on g"
    6.65 +  using contour_integrable_on_def by blast
    6.66  
    6.67  (* Show that we can forget about the localized derivative.*)
    6.68  
    6.69 @@ -607,15 +607,15 @@
    6.70       (\<lambda>x. f (g x) * vector_derivative g (at x)) integrable_on {a..b}"
    6.71    by (simp add: integrable_on_def has_integral_localized_vector_derivative)
    6.72  
    6.73 -lemma has_path_integral:
    6.74 -     "(f has_path_integral i) g \<longleftrightarrow>
    6.75 +lemma has_contour_integral:
    6.76 +     "(f has_contour_integral i) g \<longleftrightarrow>
    6.77        ((\<lambda>x. f (g x) * vector_derivative g (at x)) has_integral i) {0..1}"
    6.78 -  by (simp add: has_integral_localized_vector_derivative has_path_integral_def)
    6.79 -
    6.80 -lemma path_integrable_on:
    6.81 -     "f path_integrable_on g \<longleftrightarrow>
    6.82 +  by (simp add: has_integral_localized_vector_derivative has_contour_integral_def)
    6.83 +
    6.84 +lemma contour_integrable_on:
    6.85 +     "f contour_integrable_on g \<longleftrightarrow>
    6.86        (\<lambda>t. f(g t) * vector_derivative g (at t)) integrable_on {0..1}"
    6.87 -  by (simp add: has_path_integral integrable_on_def path_integrable_on_def)
    6.88 +  by (simp add: has_contour_integral integrable_on_def contour_integrable_on_def)
    6.89  
    6.90  subsection\<open>Reversing a path\<close>
    6.91  
    6.92 @@ -640,9 +640,9 @@
    6.93  lemma valid_path_reversepath: "valid_path(reversepath g) \<longleftrightarrow> valid_path g"
    6.94    using valid_path_imp_reverse by force
    6.95  
    6.96 -lemma has_path_integral_reversepath:
    6.97 -  assumes "valid_path g" "(f has_path_integral i) g"
    6.98 -    shows "(f has_path_integral (-i)) (reversepath g)"
    6.99 +lemma has_contour_integral_reversepath:
   6.100 +  assumes "valid_path g" "(f has_contour_integral i) g"
   6.101 +    shows "(f has_contour_integral (-i)) (reversepath g)"
   6.102  proof -
   6.103    { fix s x
   6.104      assume xs: "g C1_differentiable_on ({0..1} - s)" "x \<notin> op - 1 ` s" "0 \<le> x" "x \<le> 1"
   6.105 @@ -667,7 +667,7 @@
   6.106    have 01: "{0..1::real} = cbox 0 1"
   6.107      by simp
   6.108    show ?thesis using assms
   6.109 -    apply (auto simp: has_path_integral_def)
   6.110 +    apply (auto simp: has_contour_integral_def)
   6.111      apply (drule has_integral_affinity01 [where m= "-1" and c=1])
   6.112      apply (auto simp: reversepath_def valid_path_def piecewise_C1_differentiable_on_def)
   6.113      apply (drule has_integral_neg)
   6.114 @@ -676,17 +676,17 @@
   6.115      done
   6.116  qed
   6.117  
   6.118 -lemma path_integrable_reversepath:
   6.119 -    "valid_path g \<Longrightarrow> f path_integrable_on g \<Longrightarrow> f path_integrable_on (reversepath g)"
   6.120 -  using has_path_integral_reversepath path_integrable_on_def by blast
   6.121 -
   6.122 -lemma path_integrable_reversepath_eq:
   6.123 -    "valid_path g \<Longrightarrow> (f path_integrable_on (reversepath g) \<longleftrightarrow> f path_integrable_on g)"
   6.124 -  using path_integrable_reversepath valid_path_reversepath by fastforce
   6.125 -
   6.126 -lemma path_integral_reversepath:
   6.127 -    "\<lbrakk>valid_path g; f path_integrable_on g\<rbrakk> \<Longrightarrow> path_integral (reversepath g) f = -(path_integral g f)"
   6.128 -  using has_path_integral_reversepath path_integrable_on_def path_integral_unique by blast
   6.129 +lemma contour_integrable_reversepath:
   6.130 +    "valid_path g \<Longrightarrow> f contour_integrable_on g \<Longrightarrow> f contour_integrable_on (reversepath g)"
   6.131 +  using has_contour_integral_reversepath contour_integrable_on_def by blast
   6.132 +
   6.133 +lemma contour_integrable_reversepath_eq:
   6.134 +    "valid_path g \<Longrightarrow> (f contour_integrable_on (reversepath g) \<longleftrightarrow> f contour_integrable_on g)"
   6.135 +  using contour_integrable_reversepath valid_path_reversepath by fastforce
   6.136 +
   6.137 +lemma contour_integral_reversepath:
   6.138 +    "\<lbrakk>valid_path g; f contour_integrable_on g\<rbrakk> \<Longrightarrow> contour_integral (reversepath g) f = -(contour_integral g f)"
   6.139 +  using has_contour_integral_reversepath contour_integrable_on_def contour_integral_unique by blast
   6.140  
   6.141  
   6.142  subsection\<open>Joining two paths together\<close>
   6.143 @@ -733,10 +733,10 @@
   6.144    shows "pathfinish g1 = pathstart g2 \<Longrightarrow> (valid_path(g1 +++ g2) \<longleftrightarrow> valid_path g1 \<and> valid_path g2)"
   6.145    using valid_path_join_D1 valid_path_join_D2 valid_path_join by blast
   6.146  
   6.147 -lemma has_path_integral_join:
   6.148 -  assumes "(f has_path_integral i1) g1" "(f has_path_integral i2) g2"
   6.149 +lemma has_contour_integral_join:
   6.150 +  assumes "(f has_contour_integral i1) g1" "(f has_contour_integral i2) g2"
   6.151            "valid_path g1" "valid_path g2"
   6.152 -    shows "(f has_path_integral (i1 + i2)) (g1 +++ g2)"
   6.153 +    shows "(f has_contour_integral (i1 + i2)) (g1 +++ g2)"
   6.154  proof -
   6.155    obtain s1 s2
   6.156      where s1: "finite s1" "\<forall>x\<in>{0..1} - s1. g1 differentiable at x"
   6.157 @@ -746,7 +746,7 @@
   6.158    have 1: "((\<lambda>x. f (g1 x) * vector_derivative g1 (at x)) has_integral i1) {0..1}"
   6.159     and 2: "((\<lambda>x. f (g2 x) * vector_derivative g2 (at x)) has_integral i2) {0..1}"
   6.160      using assms
   6.161 -    by (auto simp: has_path_integral)
   6.162 +    by (auto simp: has_contour_integral)
   6.163    have i1: "((\<lambda>x. (2*f (g1 (2*x))) * vector_derivative g1 (at (2*x))) has_integral i1) {0..1/2}"
   6.164     and i2: "((\<lambda>x. (2*f (g2 (2*x - 1))) * vector_derivative g2 (at (2*x - 1))) has_integral i2) {1/2..1}"
   6.165      using has_integral_affinity01 [OF 1, where m= 2 and c=0, THEN has_integral_cmul [where c=2]]
   6.166 @@ -786,28 +786,28 @@
   6.167      done
   6.168    ultimately
   6.169    show ?thesis
   6.170 -    apply (simp add: has_path_integral)
   6.171 +    apply (simp add: has_contour_integral)
   6.172      apply (rule has_integral_combine [where c = "1/2"], auto)
   6.173      done
   6.174  qed
   6.175  
   6.176 -lemma path_integrable_joinI:
   6.177 -  assumes "f path_integrable_on g1" "f path_integrable_on g2"
   6.178 +lemma contour_integrable_joinI:
   6.179 +  assumes "f contour_integrable_on g1" "f contour_integrable_on g2"
   6.180            "valid_path g1" "valid_path g2"
   6.181 -    shows "f path_integrable_on (g1 +++ g2)"
   6.182 +    shows "f contour_integrable_on (g1 +++ g2)"
   6.183    using assms
   6.184 -  by (meson has_path_integral_join path_integrable_on_def)
   6.185 -
   6.186 -lemma path_integrable_joinD1:
   6.187 -  assumes "f path_integrable_on (g1 +++ g2)" "valid_path g1"
   6.188 -    shows "f path_integrable_on g1"
   6.189 +  by (meson has_contour_integral_join contour_integrable_on_def)
   6.190 +
   6.191 +lemma contour_integrable_joinD1:
   6.192 +  assumes "f contour_integrable_on (g1 +++ g2)" "valid_path g1"
   6.193 +    shows "f contour_integrable_on g1"
   6.194  proof -
   6.195    obtain s1
   6.196      where s1: "finite s1" "\<forall>x\<in>{0..1} - s1. g1 differentiable at x"
   6.197      using assms by (auto simp: valid_path_def piecewise_C1_differentiable_on_def C1_differentiable_on_eq)
   6.198    have "(\<lambda>x. f ((g1 +++ g2) (x/2)) * vector_derivative (g1 +++ g2) (at (x/2))) integrable_on {0..1}"
   6.199      using assms
   6.200 -    apply (auto simp: path_integrable_on)
   6.201 +    apply (auto simp: contour_integrable_on)
   6.202      apply (drule integrable_on_subcbox [where a=0 and b="1/2"])
   6.203      apply (auto intro: integrable_affinity [of _ 0 "1/2::real" "1/2" 0, simplified])
   6.204      done
   6.205 @@ -824,22 +824,22 @@
   6.206      done
   6.207    show ?thesis
   6.208      using s1
   6.209 -    apply (auto simp: path_integrable_on)
   6.210 +    apply (auto simp: contour_integrable_on)
   6.211      apply (rule integrable_spike_finite [of "{0,1} \<union> s1", OF _ _ *])
   6.212      apply (auto simp: joinpaths_def scaleR_conv_of_real g1)
   6.213      done
   6.214  qed
   6.215  
   6.216 -lemma path_integrable_joinD2:
   6.217 -  assumes "f path_integrable_on (g1 +++ g2)" "valid_path g2"
   6.218 -    shows "f path_integrable_on g2"
   6.219 +lemma contour_integrable_joinD2:
   6.220 +  assumes "f contour_integrable_on (g1 +++ g2)" "valid_path g2"
   6.221 +    shows "f contour_integrable_on g2"
   6.222  proof -
   6.223    obtain s2
   6.224      where s2: "finite s2" "\<forall>x\<in>{0..1} - s2. g2 differentiable at x"
   6.225      using assms by (auto simp: valid_path_def piecewise_C1_differentiable_on_def C1_differentiable_on_eq)
   6.226    have "(\<lambda>x. f ((g1 +++ g2) (x/2 + 1/2)) * vector_derivative (g1 +++ g2) (at (x/2 + 1/2))) integrable_on {0..1}"
   6.227      using assms
   6.228 -    apply (auto simp: path_integrable_on)
   6.229 +    apply (auto simp: contour_integrable_on)
   6.230      apply (drule integrable_on_subcbox [where a="1/2" and b=1], auto)
   6.231      apply (drule integrable_affinity [of _ "1/2::real" 1 "1/2" "1/2", simplified])
   6.232      apply (simp add: image_affinity_atLeastAtMost_diff)
   6.233 @@ -859,23 +859,23 @@
   6.234      done
   6.235    show ?thesis
   6.236      using s2
   6.237 -    apply (auto simp: path_integrable_on)
   6.238 +    apply (auto simp: contour_integrable_on)
   6.239      apply (rule integrable_spike_finite [of "{0,1} \<union> s2", OF _ _ *])
   6.240      apply (auto simp: joinpaths_def scaleR_conv_of_real g2)
   6.241      done
   6.242  qed
   6.243  
   6.244 -lemma path_integrable_join [simp]:
   6.245 +lemma contour_integrable_join [simp]:
   6.246    shows
   6.247      "\<lbrakk>valid_path g1; valid_path g2\<rbrakk>
   6.248 -     \<Longrightarrow> f path_integrable_on (g1 +++ g2) \<longleftrightarrow> f path_integrable_on g1 \<and> f path_integrable_on g2"
   6.249 -using path_integrable_joinD1 path_integrable_joinD2 path_integrable_joinI by blast
   6.250 -
   6.251 -lemma path_integral_join [simp]:
   6.252 +     \<Longrightarrow> f contour_integrable_on (g1 +++ g2) \<longleftrightarrow> f contour_integrable_on g1 \<and> f contour_integrable_on g2"
   6.253 +using contour_integrable_joinD1 contour_integrable_joinD2 contour_integrable_joinI by blast
   6.254 +
   6.255 +lemma contour_integral_join [simp]:
   6.256    shows
   6.257 -    "\<lbrakk>f path_integrable_on g1; f path_integrable_on g2; valid_path g1; valid_path g2\<rbrakk>
   6.258 -        \<Longrightarrow> path_integral (g1 +++ g2) f = path_integral g1 f + path_integral g2 f"
   6.259 -  by (simp add: has_path_integral_integral has_path_integral_join path_integral_unique)
   6.260 +    "\<lbrakk>f contour_integrable_on g1; f contour_integrable_on g2; valid_path g1; valid_path g2\<rbrakk>
   6.261 +        \<Longrightarrow> contour_integral (g1 +++ g2) f = contour_integral g1 f + contour_integral g2 f"
   6.262 +  by (simp add: has_contour_integral_integral has_contour_integral_join contour_integral_unique)
   6.263  
   6.264  
   6.265  subsection\<open>Shifting the starting point of a (closed) path\<close>
   6.266 @@ -896,16 +896,16 @@
   6.267    apply (auto simp: pathfinish_def pathstart_def elim: piecewise_C1_differentiable_on_subset)
   6.268    done
   6.269  
   6.270 -lemma has_path_integral_shiftpath:
   6.271 -  assumes f: "(f has_path_integral i) g" "valid_path g"
   6.272 +lemma has_contour_integral_shiftpath:
   6.273 +  assumes f: "(f has_contour_integral i) g" "valid_path g"
   6.274        and a: "a \<in> {0..1}"
   6.275 -    shows "(f has_path_integral i) (shiftpath a g)"
   6.276 +    shows "(f has_contour_integral i) (shiftpath a g)"
   6.277  proof -
   6.278    obtain s
   6.279      where s: "finite s" and g: "\<forall>x\<in>{0..1} - s. g differentiable at x"
   6.280      using assms by (auto simp: valid_path_def piecewise_C1_differentiable_on_def C1_differentiable_on_eq)
   6.281    have *: "((\<lambda>x. f (g x) * vector_derivative g (at x)) has_integral i) {0..1}"
   6.282 -    using assms by (auto simp: has_path_integral)
   6.283 +    using assms by (auto simp: has_contour_integral)
   6.284    then have i: "i = integral {a..1} (\<lambda>x. f (g x) * vector_derivative g (at x)) +
   6.285                      integral {0..a} (\<lambda>x. f (g x) * vector_derivative g (at x))"
   6.286      apply (rule has_integral_unique)
   6.287 @@ -967,13 +967,13 @@
   6.288      done
   6.289    ultimately show ?thesis
   6.290      using a
   6.291 -    by (auto simp: i has_path_integral intro: has_integral_combine [where c = "1-a"])
   6.292 +    by (auto simp: i has_contour_integral intro: has_integral_combine [where c = "1-a"])
   6.293  qed
   6.294  
   6.295 -lemma has_path_integral_shiftpath_D:
   6.296 -  assumes "(f has_path_integral i) (shiftpath a g)"
   6.297 +lemma has_contour_integral_shiftpath_D:
   6.298 +  assumes "(f has_contour_integral i) (shiftpath a g)"
   6.299            "valid_path g" "pathfinish g = pathstart g" "a \<in> {0..1}"
   6.300 -    shows "(f has_path_integral i) g"
   6.301 +    shows "(f has_contour_integral i) g"
   6.302  proof -
   6.303    obtain s
   6.304      where s: "finite s" and g: "\<forall>x\<in>{0..1} - s. g differentiable at x"
   6.305 @@ -994,25 +994,25 @@
   6.306        apply (auto simp: dist_real_def shiftpath_shiftpath abs_if)
   6.307        done
   6.308    } note vd = this
   6.309 -  have fi: "(f has_path_integral i) (shiftpath (1 - a) (shiftpath a g))"
   6.310 -    using assms  by (auto intro!: has_path_integral_shiftpath)
   6.311 +  have fi: "(f has_contour_integral i) (shiftpath (1 - a) (shiftpath a g))"
   6.312 +    using assms  by (auto intro!: has_contour_integral_shiftpath)
   6.313    show ?thesis
   6.314 -    apply (simp add: has_path_integral_def)
   6.315 -    apply (rule has_integral_spike_finite [of "{0,1} \<union> s", OF _ _  fi [unfolded has_path_integral_def]])
   6.316 +    apply (simp add: has_contour_integral_def)
   6.317 +    apply (rule has_integral_spike_finite [of "{0,1} \<union> s", OF _ _  fi [unfolded has_contour_integral_def]])
   6.318      using s assms vd
   6.319      apply (auto simp: Path_Connected.shiftpath_shiftpath)
   6.320      done
   6.321  qed
   6.322  
   6.323 -lemma has_path_integral_shiftpath_eq:
   6.324 +lemma has_contour_integral_shiftpath_eq:
   6.325    assumes "valid_path g" "pathfinish g = pathstart g" "a \<in> {0..1}"
   6.326 -    shows "(f has_path_integral i) (shiftpath a g) \<longleftrightarrow> (f has_path_integral i) g"
   6.327 -  using assms has_path_integral_shiftpath has_path_integral_shiftpath_D by blast
   6.328 -
   6.329 -lemma path_integral_shiftpath:
   6.330 +    shows "(f has_contour_integral i) (shiftpath a g) \<longleftrightarrow> (f has_contour_integral i) g"
   6.331 +  using assms has_contour_integral_shiftpath has_contour_integral_shiftpath_D by blast
   6.332 +
   6.333 +lemma contour_integral_shiftpath:
   6.334    assumes "valid_path g" "pathfinish g = pathstart g" "a \<in> {0..1}"
   6.335 -    shows "path_integral (shiftpath a g) f = path_integral g f"
   6.336 -   using assms by (simp add: path_integral_def has_path_integral_shiftpath_eq)
   6.337 +    shows "contour_integral (shiftpath a g) f = contour_integral g f"
   6.338 +   using assms by (simp add: contour_integral_def has_contour_integral_shiftpath_eq)
   6.339  
   6.340  
   6.341  subsection\<open>More about straight-line paths\<close>
   6.342 @@ -1040,10 +1040,10 @@
   6.343    apply (fastforce simp add: continuous_on_eq_continuous_within)
   6.344    done
   6.345  
   6.346 -lemma has_path_integral_linepath:
   6.347 -  shows "(f has_path_integral i) (linepath a b) \<longleftrightarrow>
   6.348 +lemma has_contour_integral_linepath:
   6.349 +  shows "(f has_contour_integral i) (linepath a b) \<longleftrightarrow>
   6.350           ((\<lambda>x. f(linepath a b x) * (b - a)) has_integral i) {0..1}"
   6.351 -  by (simp add: has_path_integral vector_derivative_linepath_at)
   6.352 +  by (simp add: has_contour_integral vector_derivative_linepath_at)
   6.353  
   6.354  lemma linepath_in_path:
   6.355    shows "x \<in> {0..1} \<Longrightarrow> linepath a b x \<in> closed_segment a b"
   6.356 @@ -1075,11 +1075,11 @@
   6.357  lemma of_real_linepath: "of_real (linepath a b x) = linepath (of_real a) (of_real b) x"
   6.358    by (metis linepath_of_real mult.right_neutral of_real_def real_scaleR_def)
   6.359  
   6.360 -lemma has_path_integral_trivial [iff]: "(f has_path_integral 0) (linepath a a)"
   6.361 -  by (simp add: has_path_integral_linepath)
   6.362 -
   6.363 -lemma path_integral_trivial [simp]: "path_integral (linepath a a) f = 0"
   6.364 -  using has_path_integral_trivial path_integral_unique by blast
   6.365 +lemma has_contour_integral_trivial [iff]: "(f has_contour_integral 0) (linepath a a)"
   6.366 +  by (simp add: has_contour_integral_linepath)
   6.367 +
   6.368 +lemma contour_integral_trivial [simp]: "contour_integral (linepath a a) f = 0"
   6.369 +  using has_contour_integral_trivial contour_integral_unique by blast
   6.370  
   6.371  
   6.372  subsection\<open>Relation to subpath construction\<close>
   6.373 @@ -1108,24 +1108,24 @@
   6.374      by (auto simp: o_def valid_path_def subpath_def)
   6.375  qed
   6.376  
   6.377 -lemma has_path_integral_subpath_refl [iff]: "(f has_path_integral 0) (subpath u u g)"
   6.378 -  by (simp add: has_path_integral subpath_def)
   6.379 -
   6.380 -lemma path_integrable_subpath_refl [iff]: "f path_integrable_on (subpath u u g)"
   6.381 -  using has_path_integral_subpath_refl path_integrable_on_def by blast
   6.382 -
   6.383 -lemma path_integral_subpath_refl [simp]: "path_integral (subpath u u g) f = 0"
   6.384 -  by (simp add: has_path_integral_subpath_refl path_integral_unique)
   6.385 -
   6.386 -lemma has_path_integral_subpath:
   6.387 -  assumes f: "f path_integrable_on g" and g: "valid_path g"
   6.388 +lemma has_contour_integral_subpath_refl [iff]: "(f has_contour_integral 0) (subpath u u g)"
   6.389 +  by (simp add: has_contour_integral subpath_def)
   6.390 +
   6.391 +lemma contour_integrable_subpath_refl [iff]: "f contour_integrable_on (subpath u u g)"
   6.392 +  using has_contour_integral_subpath_refl contour_integrable_on_def by blast
   6.393 +
   6.394 +lemma contour_integral_subpath_refl [simp]: "contour_integral (subpath u u g) f = 0"
   6.395 +  by (simp add: has_contour_integral_subpath_refl contour_integral_unique)
   6.396 +
   6.397 +lemma has_contour_integral_subpath:
   6.398 +  assumes f: "f contour_integrable_on g" and g: "valid_path g"
   6.399        and uv: "u \<in> {0..1}" "v \<in> {0..1}" "u \<le> v"
   6.400 -    shows "(f has_path_integral  integral {u..v} (\<lambda>x. f(g x) * vector_derivative g (at x)))
   6.401 +    shows "(f has_contour_integral  integral {u..v} (\<lambda>x. f(g x) * vector_derivative g (at x)))
   6.402             (subpath u v g)"
   6.403  proof (cases "v=u")
   6.404    case True
   6.405    then show ?thesis
   6.406 -    using f   by (simp add: path_integrable_on_def subpath_def has_path_integral)
   6.407 +    using f   by (simp add: contour_integrable_on_def subpath_def has_contour_integral)
   6.408  next
   6.409    case False
   6.410    obtain s where s: "\<And>x. x \<in> {0..1} - s \<Longrightarrow> g differentiable at x" and fs: "finite s"
   6.411 @@ -1134,7 +1134,7 @@
   6.412              has_integral (1 / (v - u)) * integral {u..v} (\<lambda>t. f (g t) * vector_derivative g (at t)))
   6.413             {0..1}"
   6.414      using f uv
   6.415 -    apply (simp add: path_integrable_on subpath_def has_path_integral)
   6.416 +    apply (simp add: contour_integrable_on subpath_def has_contour_integral)
   6.417      apply (drule integrable_on_subcbox [where a=u and b=v, simplified])
   6.418      apply (simp_all add: has_integral_integral)
   6.419      apply (drule has_integral_affinity [where m="v-u" and c=u, simplified])
   6.420 @@ -1155,58 +1155,58 @@
   6.421    show ?thesis
   6.422      apply (cut_tac has_integral_cmul [OF *, where c = "v-u"])
   6.423      using fs assms
   6.424 -    apply (simp add: False subpath_def has_path_integral)
   6.425 +    apply (simp add: False subpath_def has_contour_integral)
   6.426      apply (rule_tac s = "(\<lambda>t. ((v-u) *\<^sub>R t + u)) -` s" in has_integral_spike_finite)
   6.427      apply (auto simp: inj_on_def False finite_vimageI vd scaleR_conv_of_real)
   6.428      done
   6.429  qed
   6.430  
   6.431 -lemma path_integrable_subpath:
   6.432 -  assumes "f path_integrable_on g" "valid_path g" "u \<in> {0..1}" "v \<in> {0..1}"
   6.433 -    shows "f path_integrable_on (subpath u v g)"
   6.434 +lemma contour_integrable_subpath:
   6.435 +  assumes "f contour_integrable_on g" "valid_path g" "u \<in> {0..1}" "v \<in> {0..1}"
   6.436 +    shows "f contour_integrable_on (subpath u v g)"
   6.437    apply (cases u v rule: linorder_class.le_cases)
   6.438 -   apply (metis path_integrable_on_def has_path_integral_subpath [OF assms])
   6.439 +   apply (metis contour_integrable_on_def has_contour_integral_subpath [OF assms])
   6.440    apply (subst reversepath_subpath [symmetric])
   6.441 -  apply (rule path_integrable_reversepath)
   6.442 +  apply (rule contour_integrable_reversepath)
   6.443     using assms apply (blast intro: valid_path_subpath)
   6.444 -  apply (simp add: path_integrable_on_def)
   6.445 -  using assms apply (blast intro: has_path_integral_subpath)
   6.446 +  apply (simp add: contour_integrable_on_def)
   6.447 +  using assms apply (blast intro: has_contour_integral_subpath)
   6.448    done
   6.449  
   6.450  lemma has_integral_integrable_integral: "(f has_integral i) s \<longleftrightarrow> f integrable_on s \<and> integral s f = i"
   6.451    by blast
   6.452  
   6.453 -lemma has_integral_path_integral_subpath:
   6.454 -  assumes "f path_integrable_on g" "valid_path g" "u \<in> {0..1}" "v \<in> {0..1}" "u \<le> v"
   6.455 +lemma has_integral_contour_integral_subpath:
   6.456 +  assumes "f contour_integrable_on g" "valid_path g" "u \<in> {0..1}" "v \<in> {0..1}" "u \<le> v"
   6.457      shows "(((\<lambda>x. f(g x) * vector_derivative g (at x)))
   6.458 -            has_integral  path_integral (subpath u v g) f) {u..v}"
   6.459 +            has_integral  contour_integral (subpath u v g) f) {u..v}"
   6.460    using assms
   6.461    apply (auto simp: has_integral_integrable_integral)
   6.462    apply (rule integrable_on_subcbox [where a=u and b=v and s = "{0..1}", simplified])
   6.463 -  apply (auto simp: path_integral_unique [OF has_path_integral_subpath] path_integrable_on)
   6.464 +  apply (auto simp: contour_integral_unique [OF has_contour_integral_subpath] contour_integrable_on)
   6.465    done
   6.466  
   6.467 -lemma path_integral_subpath_integral:
   6.468 -  assumes "f path_integrable_on g" "valid_path g" "u \<in> {0..1}" "v \<in> {0..1}" "u \<le> v"
   6.469 -    shows "path_integral (subpath u v g) f =
   6.470 +lemma contour_integral_subcontour_integral:
   6.471 +  assumes "f contour_integrable_on g" "valid_path g" "u \<in> {0..1}" "v \<in> {0..1}" "u \<le> v"
   6.472 +    shows "contour_integral (subpath u v g) f =
   6.473             integral {u..v} (\<lambda>x. f(g x) * vector_derivative g (at x))"
   6.474 -  using assms has_path_integral_subpath path_integral_unique by blast
   6.475 -
   6.476 -lemma path_integral_subpath_combine_less:
   6.477 -  assumes "f path_integrable_on g" "valid_path g" "u \<in> {0..1}" "v \<in> {0..1}" "w \<in> {0..1}"
   6.478 +  using assms has_contour_integral_subpath contour_integral_unique by blast
   6.479 +
   6.480 +lemma contour_integral_subpath_combine_less:
   6.481 +  assumes "f contour_integrable_on g" "valid_path g" "u \<in> {0..1}" "v \<in> {0..1}" "w \<in> {0..1}"
   6.482            "u<v" "v<w"
   6.483 -    shows "path_integral (subpath u v g) f + path_integral (subpath v w g) f =
   6.484 -           path_integral (subpath u w g) f"
   6.485 -  using assms apply (auto simp: path_integral_subpath_integral)
   6.486 +    shows "contour_integral (subpath u v g) f + contour_integral (subpath v w g) f =
   6.487 +           contour_integral (subpath u w g) f"
   6.488 +  using assms apply (auto simp: contour_integral_subcontour_integral)
   6.489    apply (rule integral_combine, auto)
   6.490    apply (rule integrable_on_subcbox [where a=u and b=w and s = "{0..1}", simplified])
   6.491 -  apply (auto simp: path_integrable_on)
   6.492 +  apply (auto simp: contour_integrable_on)
   6.493    done
   6.494  
   6.495 -lemma path_integral_subpath_combine:
   6.496 -  assumes "f path_integrable_on g" "valid_path g" "u \<in> {0..1}" "v \<in> {0..1}" "w \<in> {0..1}"
   6.497 -    shows "path_integral (subpath u v g) f + path_integral (subpath v w g) f =
   6.498 -           path_integral (subpath u w g) f"
   6.499 +lemma contour_integral_subpath_combine:
   6.500 +  assumes "f contour_integrable_on g" "valid_path g" "u \<in> {0..1}" "v \<in> {0..1}" "w \<in> {0..1}"
   6.501 +    shows "contour_integral (subpath u v g) f + contour_integral (subpath v w g) f =
   6.502 +           contour_integral (subpath u w g) f"
   6.503  proof (cases "u\<noteq>v \<and> v\<noteq>w \<and> u\<noteq>w")
   6.504    case True
   6.505      have *: "subpath v u g = reversepath(subpath u v g) \<and>
   6.506 @@ -1221,28 +1221,28 @@
   6.507            w < v \<and> v < u"
   6.508        using True assms by linarith
   6.509      with assms show ?thesis
   6.510 -      using path_integral_subpath_combine_less [of f g u v w]
   6.511 -            path_integral_subpath_combine_less [of f g u w v]
   6.512 -            path_integral_subpath_combine_less [of f g v u w]
   6.513 -            path_integral_subpath_combine_less [of f g v w u]
   6.514 -            path_integral_subpath_combine_less [of f g w u v]
   6.515 -            path_integral_subpath_combine_less [of f g w v u]
   6.516 +      using contour_integral_subpath_combine_less [of f g u v w]
   6.517 +            contour_integral_subpath_combine_less [of f g u w v]
   6.518 +            contour_integral_subpath_combine_less [of f g v u w]
   6.519 +            contour_integral_subpath_combine_less [of f g v w u]
   6.520 +            contour_integral_subpath_combine_less [of f g w u v]
   6.521 +            contour_integral_subpath_combine_less [of f g w v u]
   6.522        apply simp
   6.523        apply (elim disjE)
   6.524 -      apply (auto simp: * path_integral_reversepath path_integrable_subpath
   6.525 +      apply (auto simp: * contour_integral_reversepath contour_integrable_subpath
   6.526                     valid_path_reversepath valid_path_subpath algebra_simps)
   6.527        done
   6.528  next
   6.529    case False
   6.530    then show ?thesis
   6.531 -    apply (auto simp: path_integral_subpath_refl)
   6.532 +    apply (auto simp: contour_integral_subpath_refl)
   6.533      using assms
   6.534 -    by (metis eq_neg_iff_add_eq_0 path_integrable_subpath path_integral_reversepath reversepath_subpath valid_path_subpath)
   6.535 +    by (metis eq_neg_iff_add_eq_0 contour_integrable_subpath contour_integral_reversepath reversepath_subpath valid_path_subpath)
   6.536  qed
   6.537  
   6.538 -lemma path_integral_integral:
   6.539 -  shows "path_integral g f = integral {0..1} (\<lambda>x. f (g x) * vector_derivative g (at x))"
   6.540 -  by (simp add: path_integral_def integral_def has_path_integral)
   6.541 +lemma contour_integral_integral:
   6.542 +  shows "contour_integral g f = integral {0..1} (\<lambda>x. f (g x) * vector_derivative g (at x))"
   6.543 +  by (simp add: contour_integral_def integral_def has_contour_integral)
   6.544  
   6.545  
   6.546  subsection\<open>Segments via convex hulls\<close>
   6.547 @@ -1283,7 +1283,7 @@
   6.548  
   6.549  text\<open>Cauchy's theorem where there's a primitive\<close>
   6.550  
   6.551 -lemma path_integral_primitive_lemma:
   6.552 +lemma contour_integral_primitive_lemma:
   6.553    fixes f :: "complex \<Rightarrow> complex" and g :: "real \<Rightarrow> complex"
   6.554    assumes "a \<le> b"
   6.555        and "\<And>x. x \<in> s \<Longrightarrow> (f has_field_derivative f' x) (at x within s)"
   6.556 @@ -1321,34 +1321,34 @@
   6.557      done
   6.558  qed
   6.559  
   6.560 -lemma path_integral_primitive:
   6.561 +lemma contour_integral_primitive:
   6.562    assumes "\<And>x. x \<in> s \<Longrightarrow> (f has_field_derivative f' x) (at x within s)"
   6.563        and "valid_path g" "path_image g \<subseteq> s"
   6.564 -    shows "(f' has_path_integral (f(pathfinish g) - f(pathstart g))) g"
   6.565 +    shows "(f' has_contour_integral (f(pathfinish g) - f(pathstart g))) g"
   6.566    using assms
   6.567 -  apply (simp add: valid_path_def path_image_def pathfinish_def pathstart_def has_path_integral_def)
   6.568 -  apply (auto intro!: piecewise_C1_imp_differentiable path_integral_primitive_lemma [of 0 1 s])
   6.569 +  apply (simp add: valid_path_def path_image_def pathfinish_def pathstart_def has_contour_integral_def)
   6.570 +  apply (auto intro!: piecewise_C1_imp_differentiable contour_integral_primitive_lemma [of 0 1 s])
   6.571    done
   6.572  
   6.573  corollary Cauchy_theorem_primitive:
   6.574    assumes "\<And>x. x \<in> s \<Longrightarrow> (f has_field_derivative f' x) (at x within s)"
   6.575        and "valid_path g"  "path_image g \<subseteq> s" "pathfinish g = pathstart g"
   6.576 -    shows "(f' has_path_integral 0) g"
   6.577 +    shows "(f' has_contour_integral 0) g"
   6.578    using assms
   6.579 -  by (metis diff_self path_integral_primitive)
   6.580 +  by (metis diff_self contour_integral_primitive)
   6.581  
   6.582  
   6.583  text\<open>Existence of path integral for continuous function\<close>
   6.584 -lemma path_integrable_continuous_linepath:
   6.585 +lemma contour_integrable_continuous_linepath:
   6.586    assumes "continuous_on (closed_segment a b) f"
   6.587 -  shows "f path_integrable_on (linepath a b)"
   6.588 +  shows "f contour_integrable_on (linepath a b)"
   6.589  proof -
   6.590    have "continuous_on {0..1} ((\<lambda>x. f x * (b - a)) o linepath a b)"
   6.591      apply (rule continuous_on_compose [OF continuous_on_linepath], simp add: linepath_image_01)
   6.592      apply (rule continuous_intros | simp add: assms)+
   6.593      done
   6.594    then show ?thesis
   6.595 -    apply (simp add: path_integrable_on_def has_path_integral_def integrable_on_def [symmetric])
   6.596 +    apply (simp add: contour_integrable_on_def has_contour_integral_def integrable_on_def [symmetric])
   6.597      apply (rule integrable_continuous [of 0 "1::real", simplified])
   6.598      apply (rule continuous_on_eq [where f = "\<lambda>x. f(linepath a b x)*(b - a)"])
   6.599      apply (auto simp: vector_derivative_linepath_within)
   6.600 @@ -1359,59 +1359,59 @@
   6.601    by (rule has_derivative_imp_has_field_derivative)
   6.602       (rule derivative_intros | simp)+
   6.603  
   6.604 -lemma path_integral_id [simp]: "path_integral (linepath a b) (\<lambda>y. y) = (b^2 - a^2)/2"
   6.605 -  apply (rule path_integral_unique)
   6.606 -  using path_integral_primitive [of UNIV "\<lambda>x. x^2/2" "\<lambda>x. x" "linepath a b"]
   6.607 +lemma contour_integral_id [simp]: "contour_integral (linepath a b) (\<lambda>y. y) = (b^2 - a^2)/2"
   6.608 +  apply (rule contour_integral_unique)
   6.609 +  using contour_integral_primitive [of UNIV "\<lambda>x. x^2/2" "\<lambda>x. x" "linepath a b"]
   6.610    apply (auto simp: field_simps has_field_der_id)
   6.611    done
   6.612  
   6.613 -lemma path_integrable_on_const [iff]: "(\<lambda>x. c) path_integrable_on (linepath a b)"
   6.614 -  by (simp add: continuous_on_const path_integrable_continuous_linepath)
   6.615 -
   6.616 -lemma path_integrable_on_id [iff]: "(\<lambda>x. x) path_integrable_on (linepath a b)"
   6.617 -  by (simp add: continuous_on_id path_integrable_continuous_linepath)
   6.618 +lemma contour_integrable_on_const [iff]: "(\<lambda>x. c) contour_integrable_on (linepath a b)"
   6.619 +  by (simp add: continuous_on_const contour_integrable_continuous_linepath)
   6.620 +
   6.621 +lemma contour_integrable_on_id [iff]: "(\<lambda>x. x) contour_integrable_on (linepath a b)"
   6.622 +  by (simp add: continuous_on_id contour_integrable_continuous_linepath)
   6.623  
   6.624  
   6.625  subsection\<open>Arithmetical combining theorems\<close>
   6.626  
   6.627 -lemma has_path_integral_neg:
   6.628 -    "(f has_path_integral i) g \<Longrightarrow> ((\<lambda>x. -(f x)) has_path_integral (-i)) g"
   6.629 -  by (simp add: has_integral_neg has_path_integral_def)
   6.630 -
   6.631 -lemma has_path_integral_add:
   6.632 -    "\<lbrakk>(f1 has_path_integral i1) g; (f2 has_path_integral i2) g\<rbrakk>
   6.633 -     \<Longrightarrow> ((\<lambda>x. f1 x + f2 x) has_path_integral (i1 + i2)) g"
   6.634 -  by (simp add: has_integral_add has_path_integral_def algebra_simps)
   6.635 -
   6.636 -lemma has_path_integral_diff:
   6.637 -  "\<lbrakk>(f1 has_path_integral i1) g; (f2 has_path_integral i2) g\<rbrakk>
   6.638 -         \<Longrightarrow> ((\<lambda>x. f1 x - f2 x) has_path_integral (i1 - i2)) g"
   6.639 -  by (simp add: has_integral_sub has_path_integral_def algebra_simps)
   6.640 -
   6.641 -lemma has_path_integral_lmul:
   6.642 -  "(f has_path_integral i) g \<Longrightarrow> ((\<lambda>x. c * (f x)) has_path_integral (c*i)) g"
   6.643 -apply (simp add: has_path_integral_def)
   6.644 +lemma has_contour_integral_neg:
   6.645 +    "(f has_contour_integral i) g \<Longrightarrow> ((\<lambda>x. -(f x)) has_contour_integral (-i)) g"
   6.646 +  by (simp add: has_integral_neg has_contour_integral_def)
   6.647 +
   6.648 +lemma has_contour_integral_add:
   6.649 +    "\<lbrakk>(f1 has_contour_integral i1) g; (f2 has_contour_integral i2) g\<rbrakk>
   6.650 +     \<Longrightarrow> ((\<lambda>x. f1 x + f2 x) has_contour_integral (i1 + i2)) g"
   6.651 +  by (simp add: has_integral_add has_contour_integral_def algebra_simps)
   6.652 +
   6.653 +lemma has_contour_integral_diff:
   6.654 +  "\<lbrakk>(f1 has_contour_integral i1) g; (f2 has_contour_integral i2) g\<rbrakk>
   6.655 +         \<Longrightarrow> ((\<lambda>x. f1 x - f2 x) has_contour_integral (i1 - i2)) g"
   6.656 +  by (simp add: has_integral_sub has_contour_integral_def algebra_simps)
   6.657 +
   6.658 +lemma has_contour_integral_lmul:
   6.659 +  "(f has_contour_integral i) g \<Longrightarrow> ((\<lambda>x. c * (f x)) has_contour_integral (c*i)) g"
   6.660 +apply (simp add: has_contour_integral_def)
   6.661  apply (drule has_integral_mult_right)
   6.662  apply (simp add: algebra_simps)
   6.663  done
   6.664  
   6.665 -lemma has_path_integral_rmul:
   6.666 -  "(f has_path_integral i) g \<Longrightarrow> ((\<lambda>x. (f x) * c) has_path_integral (i*c)) g"
   6.667 -apply (drule has_path_integral_lmul)
   6.668 +lemma has_contour_integral_rmul:
   6.669 +  "(f has_contour_integral i) g \<Longrightarrow> ((\<lambda>x. (f x) * c) has_contour_integral (i*c)) g"
   6.670 +apply (drule has_contour_integral_lmul)
   6.671  apply (simp add: mult.commute)
   6.672  done
   6.673  
   6.674 -lemma has_path_integral_div:
   6.675 -  "(f has_path_integral i) g \<Longrightarrow> ((\<lambda>x. f x/c) has_path_integral (i/c)) g"
   6.676 -  by (simp add: field_class.field_divide_inverse) (metis has_path_integral_rmul)
   6.677 -
   6.678 -lemma has_path_integral_eq:
   6.679 -    "\<lbrakk>(f has_path_integral y) p; \<And>x. x \<in> path_image p \<Longrightarrow> f x = g x\<rbrakk> \<Longrightarrow> (g has_path_integral y) p"
   6.680 -apply (simp add: path_image_def has_path_integral_def)
   6.681 +lemma has_contour_integral_div:
   6.682 +  "(f has_contour_integral i) g \<Longrightarrow> ((\<lambda>x. f x/c) has_contour_integral (i/c)) g"
   6.683 +  by (simp add: field_class.field_divide_inverse) (metis has_contour_integral_rmul)
   6.684 +
   6.685 +lemma has_contour_integral_eq:
   6.686 +    "\<lbrakk>(f has_contour_integral y) p; \<And>x. x \<in> path_image p \<Longrightarrow> f x = g x\<rbrakk> \<Longrightarrow> (g has_contour_integral y) p"
   6.687 +apply (simp add: path_image_def has_contour_integral_def)
   6.688  by (metis (no_types, lifting) image_eqI has_integral_eq)
   6.689  
   6.690 -lemma has_path_integral_bound_linepath:
   6.691 -  assumes "(f has_path_integral i) (linepath a b)"
   6.692 +lemma has_contour_integral_bound_linepath:
   6.693 +  assumes "(f has_contour_integral i) (linepath a b)"
   6.694            "0 \<le> B" "\<And>x. x \<in> closed_segment a b \<Longrightarrow> norm(f x) \<le> B"
   6.695      shows "norm i \<le> B * norm(b - a)"
   6.696  proof -
   6.697 @@ -1424,7 +1424,7 @@
   6.698    have "norm i \<le> (B * norm (b - a)) * content (cbox 0 (1::real))"
   6.699      apply (rule has_integral_bound
   6.700         [of _ "\<lambda>x. f (linepath a b x) * vector_derivative (linepath a b) (at x within {0..1})"])
   6.701 -    using assms * unfolding has_path_integral_def
   6.702 +    using assms * unfolding has_contour_integral_def
   6.703      apply (auto simp: norm_mult)
   6.704      done
   6.705    then show ?thesis
   6.706 @@ -1432,163 +1432,163 @@
   6.707  qed
   6.708  
   6.709  (*UNUSED
   6.710 -lemma has_path_integral_bound_linepath_strong:
   6.711 +lemma has_contour_integral_bound_linepath_strong:
   6.712    fixes a :: real and f :: "complex \<Rightarrow> real"
   6.713 -  assumes "(f has_path_integral i) (linepath a b)"
   6.714 +  assumes "(f has_contour_integral i) (linepath a b)"
   6.715            "finite k"
   6.716            "0 \<le> B" "\<And>x::real. x \<in> closed_segment a b - k \<Longrightarrow> norm(f x) \<le> B"
   6.717      shows "norm i \<le> B*norm(b - a)"
   6.718  *)
   6.719  
   6.720 -lemma has_path_integral_const_linepath: "((\<lambda>x. c) has_path_integral c*(b - a))(linepath a b)"
   6.721 -  unfolding has_path_integral_linepath
   6.722 +lemma has_contour_integral_const_linepath: "((\<lambda>x. c) has_contour_integral c*(b - a))(linepath a b)"
   6.723 +  unfolding has_contour_integral_linepath
   6.724    by (metis content_real diff_0_right has_integral_const_real lambda_one of_real_1 scaleR_conv_of_real zero_le_one)
   6.725  
   6.726 -lemma has_path_integral_0: "((\<lambda>x. 0) has_path_integral 0) g"
   6.727 -  by (simp add: has_path_integral_def)
   6.728 -
   6.729 -lemma has_path_integral_is_0:
   6.730 -    "(\<And>z. z \<in> path_image g \<Longrightarrow> f z = 0) \<Longrightarrow> (f has_path_integral 0) g"
   6.731 -  by (rule has_path_integral_eq [OF has_path_integral_0]) auto
   6.732 -
   6.733 -lemma has_path_integral_setsum:
   6.734 -    "\<lbrakk>finite s; \<And>a. a \<in> s \<Longrightarrow> (f a has_path_integral i a) p\<rbrakk>
   6.735 -     \<Longrightarrow> ((\<lambda>x. setsum (\<lambda>a. f a x) s) has_path_integral setsum i s) p"
   6.736 -  by (induction s rule: finite_induct) (auto simp: has_path_integral_0 has_path_integral_add)
   6.737 +lemma has_contour_integral_0: "((\<lambda>x. 0) has_contour_integral 0) g"
   6.738 +  by (simp add: has_contour_integral_def)
   6.739 +
   6.740 +lemma has_contour_integral_is_0:
   6.741 +    "(\<And>z. z \<in> path_image g \<Longrightarrow> f z = 0) \<Longrightarrow> (f has_contour_integral 0) g"
   6.742 +  by (rule has_contour_integral_eq [OF has_contour_integral_0]) auto
   6.743 +
   6.744 +lemma has_contour_integral_setsum:
   6.745 +    "\<lbrakk>finite s; \<And>a. a \<in> s \<Longrightarrow> (f a has_contour_integral i a) p\<rbrakk>
   6.746 +     \<Longrightarrow> ((\<lambda>x. setsum (\<lambda>a. f a x) s) has_contour_integral setsum i s) p"
   6.747 +  by (induction s rule: finite_induct) (auto simp: has_contour_integral_0 has_contour_integral_add)
   6.748  
   6.749  
   6.750  subsection \<open>Operations on path integrals\<close>
   6.751  
   6.752 -lemma path_integral_const_linepath [simp]: "path_integral (linepath a b) (\<lambda>x. c) = c*(b - a)"
   6.753 -  by (rule path_integral_unique [OF has_path_integral_const_linepath])
   6.754 -
   6.755 -lemma path_integral_neg:
   6.756 -    "f path_integrable_on g \<Longrightarrow> path_integral g (\<lambda>x. -(f x)) = -(path_integral g f)"
   6.757 -  by (simp add: path_integral_unique has_path_integral_integral has_path_integral_neg)
   6.758 -
   6.759 -lemma path_integral_add:
   6.760 -    "f1 path_integrable_on g \<Longrightarrow> f2 path_integrable_on g \<Longrightarrow> path_integral g (\<lambda>x. f1 x + f2 x) =
   6.761 -                path_integral g f1 + path_integral g f2"
   6.762 -  by (simp add: path_integral_unique has_path_integral_integral has_path_integral_add)
   6.763 -
   6.764 -lemma path_integral_diff:
   6.765 -    "f1 path_integrable_on g \<Longrightarrow> f2 path_integrable_on g \<Longrightarrow> path_integral g (\<lambda>x. f1 x - f2 x) =
   6.766 -                path_integral g f1 - path_integral g f2"
   6.767 -  by (simp add: path_integral_unique has_path_integral_integral has_path_integral_diff)
   6.768 -
   6.769 -lemma path_integral_lmul:
   6.770 -  shows "f path_integrable_on g
   6.771 -           \<Longrightarrow> path_integral g (\<lambda>x. c * f x) = c*path_integral g f"
   6.772 -  by (simp add: path_integral_unique has_path_integral_integral has_path_integral_lmul)
   6.773 -
   6.774 -lemma path_integral_rmul:
   6.775 -  shows "f path_integrable_on g
   6.776 -        \<Longrightarrow> path_integral g (\<lambda>x. f x * c) = path_integral g f * c"
   6.777 -  by (simp add: path_integral_unique has_path_integral_integral has_path_integral_rmul)
   6.778 -
   6.779 -lemma path_integral_div:
   6.780 -  shows "f path_integrable_on g
   6.781 -        \<Longrightarrow> path_integral g (\<lambda>x. f x / c) = path_integral g f / c"
   6.782 -  by (simp add: path_integral_unique has_path_integral_integral has_path_integral_div)
   6.783 -
   6.784 -lemma path_integral_eq:
   6.785 -    "(\<And>x. x \<in> path_image p \<Longrightarrow> f x = g x) \<Longrightarrow> path_integral p f = path_integral p g"
   6.786 -  by (simp add: path_integral_def) (metis has_path_integral_eq)
   6.787 -
   6.788 -lemma path_integral_eq_0:
   6.789 -    "(\<And>z. z \<in> path_image g \<Longrightarrow> f z = 0) \<Longrightarrow> path_integral g f = 0"
   6.790 -  by (simp add: has_path_integral_is_0 path_integral_unique)
   6.791 -
   6.792 -lemma path_integral_bound_linepath:
   6.793 +lemma contour_integral_const_linepath [simp]: "contour_integral (linepath a b) (\<lambda>x. c) = c*(b - a)"
   6.794 +  by (rule contour_integral_unique [OF has_contour_integral_const_linepath])
   6.795 +
   6.796 +lemma contour_integral_neg:
   6.797 +    "f contour_integrable_on g \<Longrightarrow> contour_integral g (\<lambda>x. -(f x)) = -(contour_integral g f)"
   6.798 +  by (simp add: contour_integral_unique has_contour_integral_integral has_contour_integral_neg)
   6.799 +
   6.800 +lemma contour_integral_add:
   6.801 +    "f1 contour_integrable_on g \<Longrightarrow> f2 contour_integrable_on g \<Longrightarrow> contour_integral g (\<lambda>x. f1 x + f2 x) =
   6.802 +                contour_integral g f1 + contour_integral g f2"
   6.803 +  by (simp add: contour_integral_unique has_contour_integral_integral has_contour_integral_add)
   6.804 +
   6.805 +lemma contour_integral_diff:
   6.806 +    "f1 contour_integrable_on g \<Longrightarrow> f2 contour_integrable_on g \<Longrightarrow> contour_integral g (\<lambda>x. f1 x - f2 x) =
   6.807 +                contour_integral g f1 - contour_integral g f2"
   6.808 +  by (simp add: contour_integral_unique has_contour_integral_integral has_contour_integral_diff)
   6.809 +
   6.810 +lemma contour_integral_lmul:
   6.811 +  shows "f contour_integrable_on g
   6.812 +           \<Longrightarrow> contour_integral g (\<lambda>x. c * f x) = c*contour_integral g f"
   6.813 +  by (simp add: contour_integral_unique has_contour_integral_integral has_contour_integral_lmul)
   6.814 +
   6.815 +lemma contour_integral_rmul:
   6.816 +  shows "f contour_integrable_on g
   6.817 +        \<Longrightarrow> contour_integral g (\<lambda>x. f x * c) = contour_integral g f * c"
   6.818 +  by (simp add: contour_integral_unique has_contour_integral_integral has_contour_integral_rmul)
   6.819 +
   6.820 +lemma contour_integral_div:
   6.821 +  shows "f contour_integrable_on g
   6.822 +        \<Longrightarrow> contour_integral g (\<lambda>x. f x / c) = contour_integral g f / c"
   6.823 +  by (simp add: contour_integral_unique has_contour_integral_integral has_contour_integral_div)
   6.824 +
   6.825 +lemma contour_integral_eq:
   6.826 +    "(\<And>x. x \<in> path_image p \<Longrightarrow> f x = g x) \<Longrightarrow> contour_integral p f = contour_integral p g"
   6.827 +  by (simp add: contour_integral_def) (metis has_contour_integral_eq)
   6.828 +
   6.829 +lemma contour_integral_eq_0:
   6.830 +    "(\<And>z. z \<in> path_image g \<Longrightarrow> f z = 0) \<Longrightarrow> contour_integral g f = 0"
   6.831 +  by (simp add: has_contour_integral_is_0 contour_integral_unique)
   6.832 +
   6.833 +lemma contour_integral_bound_linepath:
   6.834    shows
   6.835 -    "\<lbrakk>f path_integrable_on (linepath a b);
   6.836 +    "\<lbrakk>f contour_integrable_on (linepath a b);
   6.837        0 \<le> B; \<And>x. x \<in> closed_segment a b \<Longrightarrow> norm(f x) \<le> B\<rbrakk>
   6.838 -     \<Longrightarrow> norm(path_integral (linepath a b) f) \<le> B*norm(b - a)"
   6.839 -  apply (rule has_path_integral_bound_linepath [of f])
   6.840 -  apply (auto simp: has_path_integral_integral)
   6.841 +     \<Longrightarrow> norm(contour_integral (linepath a b) f) \<le> B*norm(b - a)"
   6.842 +  apply (rule has_contour_integral_bound_linepath [of f])
   6.843 +  apply (auto simp: has_contour_integral_integral)
   6.844    done
   6.845  
   6.846 -lemma path_integral_0: "path_integral g (\<lambda>x. 0) = 0"
   6.847 -  by (simp add: path_integral_unique has_path_integral_0)
   6.848 -
   6.849 -lemma path_integral_setsum:
   6.850 -    "\<lbrakk>finite s; \<And>a. a \<in> s \<Longrightarrow> (f a) path_integrable_on p\<rbrakk>
   6.851 -     \<Longrightarrow> path_integral p (\<lambda>x. setsum (\<lambda>a. f a x) s) = setsum (\<lambda>a. path_integral p (f a)) s"
   6.852 -  by (auto simp: path_integral_unique has_path_integral_setsum has_path_integral_integral)
   6.853 -
   6.854 -lemma path_integrable_eq:
   6.855 -    "\<lbrakk>f path_integrable_on p; \<And>x. x \<in> path_image p \<Longrightarrow> f x = g x\<rbrakk> \<Longrightarrow> g path_integrable_on p"
   6.856 -  unfolding path_integrable_on_def
   6.857 -  by (metis has_path_integral_eq)
   6.858 +lemma contour_integral_0: "contour_integral g (\<lambda>x. 0) = 0"
   6.859 +  by (simp add: contour_integral_unique has_contour_integral_0)
   6.860 +
   6.861 +lemma contour_integral_setsum:
   6.862 +    "\<lbrakk>finite s; \<And>a. a \<in> s \<Longrightarrow> (f a) contour_integrable_on p\<rbrakk>
   6.863 +     \<Longrightarrow> contour_integral p (\<lambda>x. setsum (\<lambda>a. f a x) s) = setsum (\<lambda>a. contour_integral p (f a)) s"
   6.864 +  by (auto simp: contour_integral_unique has_contour_integral_setsum has_contour_integral_integral)
   6.865 +
   6.866 +lemma contour_integrable_eq:
   6.867 +    "\<lbrakk>f contour_integrable_on p; \<And>x. x \<in> path_image p \<Longrightarrow> f x = g x\<rbrakk> \<Longrightarrow> g contour_integrable_on p"
   6.868 +  unfolding contour_integrable_on_def
   6.869 +  by (metis has_contour_integral_eq)
   6.870  
   6.871  
   6.872  subsection \<open>Arithmetic theorems for path integrability\<close>
   6.873  
   6.874 -lemma path_integrable_neg:
   6.875 -    "f path_integrable_on g \<Longrightarrow> (\<lambda>x. -(f x)) path_integrable_on g"
   6.876 -  using has_path_integral_neg path_integrable_on_def by blast
   6.877 -
   6.878 -lemma path_integrable_add:
   6.879 -    "\<lbrakk>f1 path_integrable_on g; f2 path_integrable_on g\<rbrakk> \<Longrightarrow> (\<lambda>x. f1 x + f2 x) path_integrable_on g"
   6.880 -  using has_path_integral_add path_integrable_on_def
   6.881 +lemma contour_integrable_neg:
   6.882 +    "f contour_integrable_on g \<Longrightarrow> (\<lambda>x. -(f x)) contour_integrable_on g"
   6.883 +  using has_contour_integral_neg contour_integrable_on_def by blast
   6.884 +
   6.885 +lemma contour_integrable_add:
   6.886 +    "\<lbrakk>f1 contour_integrable_on g; f2 contour_integrable_on g\<rbrakk> \<Longrightarrow> (\<lambda>x. f1 x + f2 x) contour_integrable_on g"
   6.887 +  using has_contour_integral_add contour_integrable_on_def
   6.888    by fastforce
   6.889  
   6.890 -lemma path_integrable_diff:
   6.891 -    "\<lbrakk>f1 path_integrable_on g; f2 path_integrable_on g\<rbrakk> \<Longrightarrow> (\<lambda>x. f1 x - f2 x) path_integrable_on g"
   6.892 -  using has_path_integral_diff path_integrable_on_def
   6.893 +lemma contour_integrable_diff:
   6.894 +    "\<lbrakk>f1 contour_integrable_on g; f2 contour_integrable_on g\<rbrakk> \<Longrightarrow> (\<lambda>x. f1 x - f2 x) contour_integrable_on g"
   6.895 +  using has_contour_integral_diff contour_integrable_on_def
   6.896    by fastforce
   6.897  
   6.898 -lemma path_integrable_lmul:
   6.899 -    "f path_integrable_on g \<Longrightarrow> (\<lambda>x. c * f x) path_integrable_on g"
   6.900 -  using has_path_integral_lmul path_integrable_on_def
   6.901 +lemma contour_integrable_lmul:
   6.902 +    "f contour_integrable_on g \<Longrightarrow> (\<lambda>x. c * f x) contour_integrable_on g"
   6.903 +  using has_contour_integral_lmul contour_integrable_on_def
   6.904    by fastforce
   6.905  
   6.906 -lemma path_integrable_rmul:
   6.907 -    "f path_integrable_on g \<Longrightarrow> (\<lambda>x. f x * c) path_integrable_on g"
   6.908 -  using has_path_integral_rmul path_integrable_on_def
   6.909 +lemma contour_integrable_rmul:
   6.910 +    "f contour_integrable_on g \<Longrightarrow> (\<lambda>x. f x * c) contour_integrable_on g"
   6.911 +  using has_contour_integral_rmul contour_integrable_on_def
   6.912    by fastforce
   6.913  
   6.914 -lemma path_integrable_div:
   6.915 -    "f path_integrable_on g \<Longrightarrow> (\<lambda>x. f x / c) path_integrable_on g"
   6.916 -  using has_path_integral_div path_integrable_on_def
   6.917 +lemma contour_integrable_div:
   6.918 +    "f contour_integrable_on g \<Longrightarrow> (\<lambda>x. f x / c) contour_integrable_on g"
   6.919 +  using has_contour_integral_div contour_integrable_on_def
   6.920    by fastforce
   6.921  
   6.922 -lemma path_integrable_setsum:
   6.923 -    "\<lbrakk>finite s; \<And>a. a \<in> s \<Longrightarrow> (f a) path_integrable_on p\<rbrakk>
   6.924 -     \<Longrightarrow> (\<lambda>x. setsum (\<lambda>a. f a x) s) path_integrable_on p"
   6.925 -   unfolding path_integrable_on_def
   6.926 -   by (metis has_path_integral_setsum)
   6.927 +lemma contour_integrable_setsum:
   6.928 +    "\<lbrakk>finite s; \<And>a. a \<in> s \<Longrightarrow> (f a) contour_integrable_on p\<rbrakk>
   6.929 +     \<Longrightarrow> (\<lambda>x. setsum (\<lambda>a. f a x) s) contour_integrable_on p"
   6.930 +   unfolding contour_integrable_on_def
   6.931 +   by (metis has_contour_integral_setsum)
   6.932  
   6.933  
   6.934  subsection\<open>Reversing a path integral\<close>
   6.935  
   6.936 -lemma has_path_integral_reverse_linepath:
   6.937 -    "(f has_path_integral i) (linepath a b)
   6.938 -     \<Longrightarrow> (f has_path_integral (-i)) (linepath b a)"
   6.939 -  using has_path_integral_reversepath valid_path_linepath by fastforce
   6.940 -
   6.941 -lemma path_integral_reverse_linepath:
   6.942 +lemma has_contour_integral_reverse_linepath:
   6.943 +    "(f has_contour_integral i) (linepath a b)
   6.944 +     \<Longrightarrow> (f has_contour_integral (-i)) (linepath b a)"
   6.945 +  using has_contour_integral_reversepath valid_path_linepath by fastforce
   6.946 +
   6.947 +lemma contour_integral_reverse_linepath:
   6.948      "continuous_on (closed_segment a b) f
   6.949 -     \<Longrightarrow> path_integral (linepath a b) f = - (path_integral(linepath b a) f)"
   6.950 -apply (rule path_integral_unique)
   6.951 -apply (rule has_path_integral_reverse_linepath)
   6.952 -by (simp add: closed_segment_commute path_integrable_continuous_linepath has_path_integral_integral)
   6.953 +     \<Longrightarrow> contour_integral (linepath a b) f = - (contour_integral(linepath b a) f)"
   6.954 +apply (rule contour_integral_unique)
   6.955 +apply (rule has_contour_integral_reverse_linepath)
   6.956 +by (simp add: closed_segment_commute contour_integrable_continuous_linepath has_contour_integral_integral)
   6.957  
   6.958  
   6.959  (* Splitting a path integral in a flat way.*)
   6.960  
   6.961 -lemma has_path_integral_split:
   6.962 -  assumes f: "(f has_path_integral i) (linepath a c)" "(f has_path_integral j) (linepath c b)"
   6.963 +lemma has_contour_integral_split:
   6.964 +  assumes f: "(f has_contour_integral i) (linepath a c)" "(f has_contour_integral j) (linepath c b)"
   6.965        and k: "0 \<le> k" "k \<le> 1"
   6.966        and c: "c - a = k *\<^sub>R (b - a)"
   6.967 -    shows "(f has_path_integral (i + j)) (linepath a b)"
   6.968 +    shows "(f has_contour_integral (i + j)) (linepath a b)"
   6.969  proof (cases "k = 0 \<or> k = 1")
   6.970    case True
   6.971    then show ?thesis
   6.972      using assms
   6.973      apply auto
   6.974 -    apply (metis add.left_neutral has_path_integral_trivial has_path_integral_unique)
   6.975 -    apply (metis add.right_neutral has_path_integral_trivial has_path_integral_unique)
   6.976 +    apply (metis add.left_neutral has_contour_integral_trivial has_contour_integral_unique)
   6.977 +    apply (metis add.right_neutral has_contour_integral_trivial has_contour_integral_unique)
   6.978      done
   6.979  next
   6.980    case False
   6.981 @@ -1632,7 +1632,7 @@
   6.982    } note fj = this
   6.983    show ?thesis
   6.984      using f k
   6.985 -    apply (simp add: has_path_integral_linepath)
   6.986 +    apply (simp add: has_contour_integral_linepath)
   6.987      apply (simp add: linepath_def)
   6.988      apply (rule has_integral_combine [OF _ _ fi fj], simp_all)
   6.989      done
   6.990 @@ -1655,11 +1655,11 @@
   6.991      done
   6.992  qed
   6.993  
   6.994 -lemma path_integral_split:
   6.995 +lemma contour_integral_split:
   6.996    assumes f: "continuous_on (closed_segment a b) f"
   6.997        and k: "0 \<le> k" "k \<le> 1"
   6.998        and c: "c - a = k *\<^sub>R (b - a)"
   6.999 -    shows "path_integral(linepath a b) f = path_integral(linepath a c) f + path_integral(linepath c b) f"
  6.1000 +    shows "contour_integral(linepath a b) f = contour_integral(linepath a c) f + contour_integral(linepath c b) f"
  6.1001  proof -
  6.1002    have c': "c = (1 - k) *\<^sub>R a + k *\<^sub>R b"
  6.1003      using c by (simp add: algebra_simps)
  6.1004 @@ -1671,35 +1671,35 @@
  6.1005      apply (auto simp: hull_inc c' Convex.convexD_alt)
  6.1006      done
  6.1007    show ?thesis
  6.1008 -    apply (rule path_integral_unique)
  6.1009 -    apply (rule has_path_integral_split [OF has_path_integral_integral has_path_integral_integral k c])
  6.1010 -    apply (rule path_integrable_continuous_linepath *)+
  6.1011 +    apply (rule contour_integral_unique)
  6.1012 +    apply (rule has_contour_integral_split [OF has_contour_integral_integral has_contour_integral_integral k c])
  6.1013 +    apply (rule contour_integrable_continuous_linepath *)+
  6.1014      done
  6.1015  qed
  6.1016  
  6.1017 -lemma path_integral_split_linepath:
  6.1018 +lemma contour_integral_split_linepath:
  6.1019    assumes f: "continuous_on (closed_segment a b) f"
  6.1020        and c: "c \<in> closed_segment a b"
  6.1021 -    shows "path_integral(linepath a b) f = path_integral(linepath a c) f + path_integral(linepath c b) f"
  6.1022 +    shows "contour_integral(linepath a b) f = contour_integral(linepath a c) f + contour_integral(linepath c b) f"
  6.1023    using c
  6.1024 -  by (auto simp: closed_segment_def algebra_simps intro!: path_integral_split [OF f])
  6.1025 +  by (auto simp: closed_segment_def algebra_simps intro!: contour_integral_split [OF f])
  6.1026  
  6.1027  (* The special case of midpoints used in the main quadrisection.*)
  6.1028  
  6.1029 -lemma has_path_integral_midpoint:
  6.1030 -  assumes "(f has_path_integral i) (linepath a (midpoint a b))"
  6.1031 -          "(f has_path_integral j) (linepath (midpoint a b) b)"
  6.1032 -    shows "(f has_path_integral (i + j)) (linepath a b)"
  6.1033 -  apply (rule has_path_integral_split [where c = "midpoint a b" and k = "1/2"])
  6.1034 +lemma has_contour_integral_midpoint:
  6.1035 +  assumes "(f has_contour_integral i) (linepath a (midpoint a b))"
  6.1036 +          "(f has_contour_integral j) (linepath (midpoint a b) b)"
  6.1037 +    shows "(f has_contour_integral (i + j)) (linepath a b)"
  6.1038 +  apply (rule has_contour_integral_split [where c = "midpoint a b" and k = "1/2"])
  6.1039    using assms
  6.1040    apply (auto simp: midpoint_def algebra_simps scaleR_conv_of_real)
  6.1041    done
  6.1042  
  6.1043 -lemma path_integral_midpoint:
  6.1044 +lemma contour_integral_midpoint:
  6.1045     "continuous_on (closed_segment a b) f
  6.1046 -    \<Longrightarrow> path_integral (linepath a b) f =
  6.1047 -        path_integral (linepath a (midpoint a b)) f + path_integral (linepath (midpoint a b) b) f"
  6.1048 -  apply (rule path_integral_split [where c = "midpoint a b" and k = "1/2"])
  6.1049 +    \<Longrightarrow> contour_integral (linepath a b) f =
  6.1050 +        contour_integral (linepath a (midpoint a b)) f + contour_integral (linepath (midpoint a b) b) f"
  6.1051 +  apply (rule contour_integral_split [where c = "midpoint a b" and k = "1/2"])
  6.1052    using assms
  6.1053    apply (auto simp: midpoint_def algebra_simps scaleR_conv_of_real)
  6.1054    done
  6.1055 @@ -1708,16 +1708,16 @@
  6.1056  text\<open>A couple of special case lemmas that are useful below\<close>
  6.1057  
  6.1058  lemma triangle_linear_has_chain_integral:
  6.1059 -    "((\<lambda>x. m*x + d) has_path_integral 0) (linepath a b +++ linepath b c +++ linepath c a)"
  6.1060 +    "((\<lambda>x. m*x + d) has_contour_integral 0) (linepath a b +++ linepath b c +++ linepath c a)"
  6.1061    apply (rule Cauchy_theorem_primitive [of UNIV "\<lambda>x. m/2 * x^2 + d*x"])
  6.1062    apply (auto intro!: derivative_eq_intros)
  6.1063    done
  6.1064  
  6.1065  lemma has_chain_integral_chain_integral3:
  6.1066 -     "(f has_path_integral i) (linepath a b +++ linepath b c +++ linepath c d)
  6.1067 -      \<Longrightarrow> path_integral (linepath a b) f + path_integral (linepath b c) f + path_integral (linepath c d) f = i"
  6.1068 -  apply (subst path_integral_unique [symmetric], assumption)
  6.1069 -  apply (drule has_path_integral_integrable)
  6.1070 +     "(f has_contour_integral i) (linepath a b +++ linepath b c +++ linepath c d)
  6.1071 +      \<Longrightarrow> contour_integral (linepath a b) f + contour_integral (linepath b c) f + contour_integral (linepath c d) f = i"
  6.1072 +  apply (subst contour_integral_unique [symmetric], assumption)
  6.1073 +  apply (drule has_contour_integral_integrable)
  6.1074    apply (simp add: valid_path_join)
  6.1075    done
  6.1076  
  6.1077 @@ -1731,13 +1731,13 @@
  6.1078  lemma snd_im_cbox [simp]: "cbox a b \<noteq> {} \<Longrightarrow> (snd ` cbox (a,c) (b,d)) = cbox c d"
  6.1079    by (auto simp: cbox_Pair_eq)
  6.1080  
  6.1081 -lemma path_integral_swap:
  6.1082 +lemma contour_integral_swap:
  6.1083    assumes fcon:  "continuous_on (path_image g \<times> path_image h) (\<lambda>(y1,y2). f y1 y2)"
  6.1084        and vp:    "valid_path g" "valid_path h"
  6.1085        and gvcon: "continuous_on {0..1} (\<lambda>t. vector_derivative g (at t))"
  6.1086        and hvcon: "continuous_on {0..1} (\<lambda>t. vector_derivative h (at t))"
  6.1087 -  shows "path_integral g (\<lambda>w. path_integral h (f w)) =
  6.1088 -         path_integral h (\<lambda>z. path_integral g (\<lambda>w. f w z))"
  6.1089 +  shows "contour_integral g (\<lambda>w. contour_integral h (f w)) =
  6.1090 +         contour_integral h (\<lambda>z. contour_integral g (\<lambda>w. f w z))"
  6.1091  proof -
  6.1092    have gcon: "continuous_on {0..1} g" and hcon: "continuous_on {0..1} h"
  6.1093      using assms by (auto simp: valid_path_def piecewise_C1_differentiable_on_def)
  6.1094 @@ -1774,31 +1774,31 @@
  6.1095      apply (rule gcon hcon continuous_intros | simp)+
  6.1096      apply (auto simp: path_image_def intro: continuous_on_subset [OF fcon])
  6.1097      done
  6.1098 -  have "integral {0..1} (\<lambda>x. path_integral h (f (g x)) * vector_derivative g (at x)) =
  6.1099 -        integral {0..1} (\<lambda>x. path_integral h (\<lambda>y. f (g x) y * vector_derivative g (at x)))"
  6.1100 -    apply (rule integral_cong [OF path_integral_rmul [symmetric]])
  6.1101 -    apply (clarsimp simp: path_integrable_on)
  6.1102 +  have "integral {0..1} (\<lambda>x. contour_integral h (f (g x)) * vector_derivative g (at x)) =
  6.1103 +        integral {0..1} (\<lambda>x. contour_integral h (\<lambda>y. f (g x) y * vector_derivative g (at x)))"
  6.1104 +    apply (rule integral_cong [OF contour_integral_rmul [symmetric]])
  6.1105 +    apply (clarsimp simp: contour_integrable_on)
  6.1106      apply (rule integrable_continuous_real)
  6.1107      apply (rule continuous_on_mult [OF _ hvcon])
  6.1108      apply (subst fgh1)
  6.1109      apply (rule fcon_im1 hcon continuous_intros | simp)+
  6.1110      done
  6.1111    also have "... = integral {0..1}
  6.1112 -                     (\<lambda>y. path_integral g (\<lambda>x. f x (h y) * vector_derivative h (at y)))"
  6.1113 -    apply (simp add: path_integral_integral)
  6.1114 +                     (\<lambda>y. contour_integral g (\<lambda>x. f x (h y) * vector_derivative h (at y)))"
  6.1115 +    apply (simp add: contour_integral_integral)
  6.1116      apply (subst integral_swap_continuous [where 'a = real and 'b = real, of 0 0 1 1, simplified])
  6.1117      apply (rule fgh gvcon' hvcon' continuous_intros | simp add: split_def)+
  6.1118      apply (simp add: algebra_simps)
  6.1119      done
  6.1120 -  also have "... = path_integral h (\<lambda>z. path_integral g (\<lambda>w. f w z))"
  6.1121 -    apply (simp add: path_integral_integral)
  6.1122 +  also have "... = contour_integral h (\<lambda>z. contour_integral g (\<lambda>w. f w z))"
  6.1123 +    apply (simp add: contour_integral_integral)
  6.1124      apply (rule integral_cong)
  6.1125      apply (subst integral_mult_left [symmetric])
  6.1126      apply (blast intro: vdg)
  6.1127      apply (simp add: algebra_simps)
  6.1128      done
  6.1129    finally show ?thesis
  6.1130 -    by (simp add: path_integral_integral)
  6.1131 +    by (simp add: contour_integral_integral)
  6.1132  qed
  6.1133  
  6.1134  
  6.1135 @@ -1828,11 +1828,11 @@
  6.1136    assumes f: "continuous_on (convex hull {a,b,c}) f"
  6.1137        and dist: "dist a b \<le> K" "dist b c \<le> K" "dist c a \<le> K"
  6.1138        and e: "e * K^2 \<le>
  6.1139 -              norm (path_integral(linepath a b) f + path_integral(linepath b c) f + path_integral(linepath c a) f)"
  6.1140 +              norm (contour_integral(linepath a b) f + contour_integral(linepath b c) f + contour_integral(linepath c a) f)"
  6.1141    shows "\<exists>a' b' c'.
  6.1142             a' \<in> convex hull {a,b,c} \<and> b' \<in> convex hull {a,b,c} \<and> c' \<in> convex hull {a,b,c} \<and>
  6.1143             dist a' b' \<le> K/2  \<and>  dist b' c' \<le> K/2  \<and>  dist c' a' \<le> K/2  \<and>
  6.1144 -           e * (K/2)^2 \<le> norm(path_integral(linepath a' b') f + path_integral(linepath b' c') f + path_integral(linepath c' a') f)"
  6.1145 +           e * (K/2)^2 \<le> norm(contour_integral(linepath a' b') f + contour_integral(linepath b' c') f + contour_integral(linepath c' a') f)"
  6.1146  proof -
  6.1147    note divide_le_eq_numeral1 [simp del]
  6.1148    def a' \<equiv> "midpoint b c"
  6.1149 @@ -1847,14 +1847,14 @@
  6.1150      apply (rule continuous_on_subset [OF f],
  6.1151             metis midpoints_in_convex_hull convex_hull_subset hull_subset insert_subset segment_convex_hull)+
  6.1152      done
  6.1153 -  let ?pathint = "\<lambda>x y. path_integral(linepath x y) f"
  6.1154 +  let ?pathint = "\<lambda>x y. contour_integral(linepath x y) f"
  6.1155    have *: "?pathint a b + ?pathint b c + ?pathint c a =
  6.1156            (?pathint a c' + ?pathint c' b' + ?pathint b' a) +
  6.1157            (?pathint a' c' + ?pathint c' b + ?pathint b a') +
  6.1158            (?pathint a' c + ?pathint c b' + ?pathint b' a') +
  6.1159            (?pathint a' b' + ?pathint b' c' + ?pathint c' a')"
  6.1160 -    apply (simp add: fcont' path_integral_reverse_linepath)
  6.1161 -    apply (simp add: a'_def b'_def c'_def path_integral_midpoint fabc)
  6.1162 +    apply (simp add: fcont' contour_integral_reverse_linepath)
  6.1163 +    apply (simp add: a'_def b'_def c'_def contour_integral_midpoint fabc)
  6.1164      done
  6.1165    have [simp]: "\<And>x y. cmod (x * 2 - y * 2) = cmod (x - y) * 2"
  6.1166      by (metis left_diff_distrib mult.commute norm_mult_numeral1)
  6.1167 @@ -1926,8 +1926,8 @@
  6.1168        and e: "0 < e"
  6.1169      shows "\<exists>k>0. \<forall>a b c. dist a b \<le> k \<and> dist b c \<le> k \<and> dist c a \<le> k \<and>
  6.1170                x \<in> convex hull {a,b,c} \<and> convex hull {a,b,c} \<subseteq> s
  6.1171 -              \<longrightarrow> norm(path_integral(linepath a b) f + path_integral(linepath b c) f +
  6.1172 -                       path_integral(linepath c a) f)
  6.1173 +              \<longrightarrow> norm(contour_integral(linepath a b) f + contour_integral(linepath b c) f +
  6.1174 +                       contour_integral(linepath c a) f)
  6.1175                    \<le> e*(dist a b + dist b c + dist c a)^2"
  6.1176             (is "\<exists>k>0. \<forall>a b c. _ \<longrightarrow> ?normle a b c")
  6.1177  proof -
  6.1178 @@ -1937,22 +1937,22 @@
  6.1179    have disj_le: "\<lbrakk>x \<le> a \<or> x \<le> b \<or> x \<le> c; 0 \<le> a; 0 \<le> b; 0 \<le> c\<rbrakk> \<Longrightarrow> x \<le> a + b + c"
  6.1180               for x::real and a b c
  6.1181      by linarith
  6.1182 -  have fabc: "f path_integrable_on linepath a b" "f path_integrable_on linepath b c" "f path_integrable_on linepath c a"
  6.1183 +  have fabc: "f contour_integrable_on linepath a b" "f contour_integrable_on linepath b c" "f contour_integrable_on linepath c a"
  6.1184                if "convex hull {a, b, c} \<subseteq> s" for a b c
  6.1185      using segments_subset_convex_hull that
  6.1186 -    by (metis continuous_on_subset f path_integrable_continuous_linepath)+
  6.1187 -  note path_bound = has_path_integral_bound_linepath [simplified norm_minus_commute, OF has_path_integral_integral]
  6.1188 +    by (metis continuous_on_subset f contour_integrable_continuous_linepath)+
  6.1189 +  note path_bound = has_contour_integral_bound_linepath [simplified norm_minus_commute, OF has_contour_integral_integral]
  6.1190    { fix f' a b c d
  6.1191      assume d: "0 < d"
  6.1192         and f': "\<And>y. \<lbrakk>cmod (y - x) \<le> d; y \<in> s\<rbrakk> \<Longrightarrow> cmod (f y - f x - f' * (y - x)) \<le> e * cmod (y - x)"
  6.1193         and le: "cmod (a - b) \<le> d" "cmod (b - c) \<le> d" "cmod (c - a) \<le> d"
  6.1194         and xc: "x \<in> convex hull {a, b, c}"
  6.1195         and s: "convex hull {a, b, c} \<subseteq> s"
  6.1196 -    have pa: "path_integral (linepath a b) f + path_integral (linepath b c) f + path_integral (linepath c a) f =
  6.1197 -              path_integral (linepath a b) (\<lambda>y. f y - f x - f'*(y - x)) +
  6.1198 -              path_integral (linepath b c) (\<lambda>y. f y - f x - f'*(y - x)) +
  6.1199 -              path_integral (linepath c a) (\<lambda>y. f y - f x - f'*(y - x))"
  6.1200 -      apply (simp add: path_integral_diff path_integral_lmul path_integrable_lmul path_integrable_diff fabc [OF s])
  6.1201 +    have pa: "contour_integral (linepath a b) f + contour_integral (linepath b c) f + contour_integral (linepath c a) f =
  6.1202 +              contour_integral (linepath a b) (\<lambda>y. f y - f x - f'*(y - x)) +
  6.1203 +              contour_integral (linepath b c) (\<lambda>y. f y - f x - f'*(y - x)) +
  6.1204 +              contour_integral (linepath c a) (\<lambda>y. f y - f x - f'*(y - x))"
  6.1205 +      apply (simp add: contour_integral_diff contour_integral_lmul contour_integrable_lmul contour_integrable_diff fabc [OF s])
  6.1206        apply (simp add: field_simps)
  6.1207        done
  6.1208      { fix y
  6.1209 @@ -1971,7 +1971,7 @@
  6.1210        using f' xc s e
  6.1211        apply simp_all
  6.1212        apply (intro norm_triangle_le add_mono path_bound)
  6.1213 -      apply (simp_all add: path_integral_diff path_integral_lmul path_integrable_lmul path_integrable_diff fabc)
  6.1214 +      apply (simp_all add: contour_integral_diff contour_integral_lmul contour_integrable_lmul contour_integrable_diff fabc)
  6.1215        apply (blast intro: cm_le elim: dest: segments_subset_convex_hull [THEN subsetD])+
  6.1216        done
  6.1217    } note * = this
  6.1218 @@ -2031,13 +2031,13 @@
  6.1219  
  6.1220  lemma Cauchy_theorem_triangle:
  6.1221    assumes "f holomorphic_on (convex hull {a,b,c})"
  6.1222 -    shows "(f has_path_integral 0) (linepath a b +++ linepath b c +++ linepath c a)"
  6.1223 +    shows "(f has_contour_integral 0) (linepath a b +++ linepath b c +++ linepath c a)"
  6.1224  proof -
  6.1225    have contf: "continuous_on (convex hull {a,b,c}) f"
  6.1226      by (metis assms holomorphic_on_imp_continuous_on)
  6.1227 -  let ?pathint = "\<lambda>x y. path_integral(linepath x y) f"
  6.1228 +  let ?pathint = "\<lambda>x y. contour_integral(linepath x y) f"
  6.1229    { fix y::complex
  6.1230 -    assume fy: "(f has_path_integral y) (linepath a b +++ linepath b c +++ linepath c a)"
  6.1231 +    assume fy: "(f has_contour_integral y) (linepath a b +++ linepath b c +++ linepath c a)"
  6.1232         and ynz: "y \<noteq> 0"
  6.1233      def K \<equiv> "1 + max (dist a b) (max (dist b c) (dist c a))"
  6.1234      def e \<equiv> "norm y / K^2"
  6.1235 @@ -2133,11 +2133,11 @@
  6.1236        apply (rule_tac x1="K/k" in exE [OF real_arch_pow2], blast)
  6.1237        done
  6.1238    }
  6.1239 -  moreover have "f path_integrable_on (linepath a b +++ linepath b c +++ linepath c a)"
  6.1240 -    by simp (meson contf continuous_on_subset path_integrable_continuous_linepath segments_subset_convex_hull(1)
  6.1241 +  moreover have "f contour_integrable_on (linepath a b +++ linepath b c +++ linepath c a)"
  6.1242 +    by simp (meson contf continuous_on_subset contour_integrable_continuous_linepath segments_subset_convex_hull(1)
  6.1243                     segments_subset_convex_hull(3) segments_subset_convex_hull(5))
  6.1244    ultimately show ?thesis
  6.1245 -    using has_path_integral_integral by fastforce
  6.1246 +    using has_contour_integral_integral by fastforce
  6.1247  qed
  6.1248  
  6.1249  
  6.1250 @@ -2147,21 +2147,21 @@
  6.1251    assumes f: "continuous_on (convex hull {a,b,c}) f"
  6.1252        and c: "c - a = k *\<^sub>R (b - a)"
  6.1253        and k: "0 \<le> k"
  6.1254 -    shows "path_integral (linepath a b) f + path_integral (linepath b c) f +
  6.1255 -          path_integral (linepath c a) f = 0"
  6.1256 +    shows "contour_integral (linepath a b) f + contour_integral (linepath b c) f +
  6.1257 +          contour_integral (linepath c a) f = 0"
  6.1258  proof -
  6.1259    have fabc: "continuous_on (closed_segment a b) f" "continuous_on (closed_segment b c) f" "continuous_on (closed_segment c a) f"
  6.1260      using f continuous_on_subset segments_subset_convex_hull by metis+
  6.1261    show ?thesis
  6.1262    proof (cases "k \<le> 1")
  6.1263      case True show ?thesis
  6.1264 -      by (simp add: path_integral_split [OF fabc(1) k True c] path_integral_reverse_linepath fabc)
  6.1265 +      by (simp add: contour_integral_split [OF fabc(1) k True c] contour_integral_reverse_linepath fabc)
  6.1266    next
  6.1267      case False then show ?thesis
  6.1268        using fabc c
  6.1269 -      apply (subst path_integral_split [of a c f "1/k" b, symmetric])
  6.1270 +      apply (subst contour_integral_split [of a c f "1/k" b, symmetric])
  6.1271        apply (metis closed_segment_commute fabc(3))
  6.1272 -      apply (auto simp: k path_integral_reverse_linepath)
  6.1273 +      apply (auto simp: k contour_integral_reverse_linepath)
  6.1274        done
  6.1275    qed
  6.1276  qed
  6.1277 @@ -2169,9 +2169,9 @@
  6.1278  lemma Cauchy_theorem_flat:
  6.1279    assumes f: "continuous_on (convex hull {a,b,c}) f"
  6.1280        and c: "c - a = k *\<^sub>R (b - a)"
  6.1281 -    shows "path_integral (linepath a b) f +
  6.1282 -           path_integral (linepath b c) f +
  6.1283 -           path_integral (linepath c a) f = 0"
  6.1284 +    shows "contour_integral (linepath a b) f +
  6.1285 +           contour_integral (linepath b c) f +
  6.1286 +           contour_integral (linepath c a) f = 0"
  6.1287  proof (cases "0 \<le> k")
  6.1288    case True with assms show ?thesis
  6.1289      by (blast intro: Cauchy_theorem_flat_lemma)
  6.1290 @@ -2179,14 +2179,14 @@
  6.1291    case False
  6.1292    have "continuous_on (closed_segment a b) f" "continuous_on (closed_segment b c) f" "continuous_on (closed_segment c a) f"
  6.1293      using f continuous_on_subset segments_subset_convex_hull by metis+
  6.1294 -  moreover have "path_integral (linepath b a) f + path_integral (linepath a c) f +
  6.1295 -        path_integral (linepath c b) f = 0"
  6.1296 +  moreover have "contour_integral (linepath b a) f + contour_integral (linepath a c) f +
  6.1297 +        contour_integral (linepath c b) f = 0"
  6.1298      apply (rule Cauchy_theorem_flat_lemma [of b a c f "1-k"])
  6.1299      using False c
  6.1300      apply (auto simp: f insert_commute scaleR_conv_of_real algebra_simps)
  6.1301      done
  6.1302    ultimately show ?thesis
  6.1303 -    apply (auto simp: path_integral_reverse_linepath)
  6.1304 +    apply (auto simp: contour_integral_reverse_linepath)
  6.1305      using add_eq_0_iff by force
  6.1306  qed
  6.1307  
  6.1308 @@ -2194,7 +2194,7 @@
  6.1309  lemma Cauchy_theorem_triangle_interior:
  6.1310    assumes contf: "continuous_on (convex hull {a,b,c}) f"
  6.1311        and holf:  "f holomorphic_on interior (convex hull {a,b,c})"
  6.1312 -     shows "(f has_path_integral 0) (linepath a b +++ linepath b c +++ linepath c a)"
  6.1313 +     shows "(f has_contour_integral 0) (linepath a b +++ linepath b c +++ linepath c a)"
  6.1314  proof -
  6.1315    have fabc: "continuous_on (closed_segment a b) f" "continuous_on (closed_segment b c) f" "continuous_on (closed_segment c a) f"
  6.1316      using contf continuous_on_subset segments_subset_convex_hull by metis+
  6.1317 @@ -2219,16 +2219,16 @@
  6.1318    have contf': "continuous_on (convex hull {b,a,c}) f"
  6.1319      using contf by (simp add: insert_commute)
  6.1320    { fix y::complex
  6.1321 -    assume fy: "(f has_path_integral y) (linepath a b +++ linepath b c +++ linepath c a)"
  6.1322 +    assume fy: "(f has_contour_integral y) (linepath a b +++ linepath b c +++ linepath c a)"
  6.1323         and ynz: "y \<noteq> 0"
  6.1324 -    have pi_eq_y: "path_integral (linepath a b) f + path_integral (linepath b c) f + path_integral (linepath c a) f = y"
  6.1325 +    have pi_eq_y: "contour_integral (linepath a b) f + contour_integral (linepath b c) f + contour_integral (linepath c a) f = y"
  6.1326        by (rule has_chain_integral_chain_integral3 [OF fy])
  6.1327      have ?thesis
  6.1328      proof (cases "c=a \<or> a=b \<or> b=c")
  6.1329        case True then show ?thesis
  6.1330          using Cauchy_theorem_flat [OF contf, of 0]
  6.1331          using has_chain_integral_chain_integral3 [OF fy] ynz
  6.1332 -        by (force simp: fabc path_integral_reverse_linepath)
  6.1333 +        by (force simp: fabc contour_integral_reverse_linepath)
  6.1334      next
  6.1335        case False
  6.1336        then have car3: "card {a, b, c} = Suc (DIM(complex))"
  6.1337 @@ -2242,7 +2242,7 @@
  6.1338            apply (clarsimp simp add: collinear_3 collinear_lemma)
  6.1339            apply (drule Cauchy_theorem_flat [OF contf'])
  6.1340            using pi_eq_y ynz
  6.1341 -          apply (simp add: fabc add_eq_0_iff path_integral_reverse_linepath)
  6.1342 +          apply (simp add: fabc add_eq_0_iff contour_integral_reverse_linepath)
  6.1343            done
  6.1344        }
  6.1345        then obtain d where d: "d \<in> interior (convex hull {a, b, c})"
  6.1346 @@ -2253,7 +2253,7 @@
  6.1347                             \<Longrightarrow> cmod (f x' - f x) < cmod y / (24 * C)"
  6.1348          def e      \<equiv> "min 1 (min (d1/(4*C)) ((norm y / 24 / C) / B))"
  6.1349          def shrink \<equiv> "\<lambda>x. x - e *\<^sub>R (x - d)"
  6.1350 -        let ?pathint = "\<lambda>x y. path_integral(linepath x y) f"
  6.1351 +        let ?pathint = "\<lambda>x y. contour_integral(linepath x y) f"
  6.1352          have e: "0 < e" "e \<le> 1" "e \<le> d1 / (4 * C)" "e \<le> cmod y / 24 / C / B"
  6.1353            using d1_pos \<open>C>0\<close> \<open>B>0\<close> ynz by (simp_all add: e_def)
  6.1354          then have eCB: "24 * e * C * B \<le> cmod y"
  6.1355 @@ -2264,15 +2264,15 @@
  6.1356               "shrink b \<in> interior(convex hull {a,b,c})"
  6.1357               "shrink c \<in> interior(convex hull {a,b,c})"
  6.1358            using d e by (auto simp: hull_inc mem_interior_convex_shrink shrink_def)
  6.1359 -        then have fhp0: "(f has_path_integral 0)
  6.1360 +        then have fhp0: "(f has_contour_integral 0)
  6.1361                  (linepath (shrink a) (shrink b) +++ linepath (shrink b) (shrink c) +++ linepath (shrink c) (shrink a))"
  6.1362            by (simp add: Cauchy_theorem_triangle holomorphic_on_subset [OF holf] hull_minimal convex_interior)
  6.1363          then have f_0_shrink: "?pathint (shrink a) (shrink b) + ?pathint (shrink b) (shrink c) + ?pathint (shrink c) (shrink a) = 0"
  6.1364            by (simp add: has_chain_integral_chain_integral3)
  6.1365 -        have fpi_abc: "f path_integrable_on linepath (shrink a) (shrink b)"
  6.1366 -                      "f path_integrable_on linepath (shrink b) (shrink c)"
  6.1367 -                      "f path_integrable_on linepath (shrink c) (shrink a)"
  6.1368 -          using fhp0  by (auto simp: valid_path_join dest: has_path_integral_integrable)
  6.1369 +        have fpi_abc: "f contour_integrable_on linepath (shrink a) (shrink b)"
  6.1370 +                      "f contour_integrable_on linepath (shrink b) (shrink c)"
  6.1371 +                      "f contour_integrable_on linepath (shrink c) (shrink a)"
  6.1372 +          using fhp0  by (auto simp: valid_path_join dest: has_contour_integral_integrable)
  6.1373          have cmod_shr: "\<And>x y. cmod (shrink y - shrink x - (y - x)) = e * cmod (x - y)"
  6.1374            using e by (simp add: shrink_def real_vector.scale_right_diff_distrib [symmetric])
  6.1375          have sh_eq: "\<And>a b d::complex. (b - e *\<^sub>R (b - d)) - (a - e *\<^sub>R (a - d)) - (b - a) = e *\<^sub>R (a - b)"
  6.1376 @@ -2285,7 +2285,7 @@
  6.1377            using Cno [of u] mult_left_le_one_le [of "cmod u" x] le_less_trans norm_ge_zero by blast
  6.1378          { fix u v
  6.1379            assume uv: "u \<in> convex hull {a, b, c}" "v \<in> convex hull {a, b, c}" "u\<noteq>v"
  6.1380 -             and fpi_uv: "f path_integrable_on linepath (shrink u) (shrink v)"
  6.1381 +             and fpi_uv: "f contour_integrable_on linepath (shrink u) (shrink v)"
  6.1382            have shr_uv: "shrink u \<in> interior(convex hull {a,b,c})"
  6.1383                         "shrink v \<in> interior(convex hull {a,b,c})"
  6.1384              using d e uv
  6.1385 @@ -2343,8 +2343,8 @@
  6.1386                          _ 0 1 ])
  6.1387              using ynz \<open>0 < B\<close> \<open>0 < C\<close>
  6.1388              apply (simp_all del: le_divide_eq_numeral1)
  6.1389 -            apply (simp add: has_integral_sub has_path_integral_linepath [symmetric] has_path_integral_integral
  6.1390 -                             fpi_uv f_uv path_integrable_continuous_linepath, clarify)
  6.1391 +            apply (simp add: has_integral_sub has_contour_integral_linepath [symmetric] has_contour_integral_integral
  6.1392 +                             fpi_uv f_uv contour_integrable_continuous_linepath, clarify)
  6.1393              apply (simp only: **)
  6.1394              apply (simp add: norm_triangle_le norm_mult cmod_diff_le del: le_divide_eq_numeral1)
  6.1395              done
  6.1396 @@ -2382,10 +2382,10 @@
  6.1397          then show ?thesis ..
  6.1398        qed
  6.1399    }
  6.1400 -  moreover have "f path_integrable_on (linepath a b +++ linepath b c +++ linepath c a)"
  6.1401 -    using fabc path_integrable_continuous_linepath by auto
  6.1402 +  moreover have "f contour_integrable_on (linepath a b +++ linepath b c +++ linepath c a)"
  6.1403 +    using fabc contour_integrable_continuous_linepath by auto
  6.1404    ultimately show ?thesis
  6.1405 -    using has_path_integral_integral by fastforce
  6.1406 +    using has_contour_integral_integral by fastforce
  6.1407  qed
  6.1408  
  6.1409  
  6.1410 @@ -2395,7 +2395,7 @@
  6.1411    assumes "continuous_on (convex hull {a,b,c}) f"
  6.1412        and "finite s"
  6.1413        and "(\<And>x. x \<in> interior(convex hull {a,b,c}) - s \<Longrightarrow> f complex_differentiable (at x))"
  6.1414 -     shows "(f has_path_integral 0) (linepath a b +++ linepath b c +++ linepath c a)"
  6.1415 +     shows "(f has_contour_integral 0) (linepath a b +++ linepath b c +++ linepath c a)"
  6.1416  using assms
  6.1417  proof (induction "card s" arbitrary: a b c s rule: less_induct)
  6.1418    case (less s a b c)
  6.1419 @@ -2411,7 +2411,7 @@
  6.1420      then show ?thesis
  6.1421      proof (cases "d \<in> convex hull {a,b,c}")
  6.1422        case False
  6.1423 -      show "(f has_path_integral 0) (linepath a b +++ linepath b c +++ linepath c a)"
  6.1424 +      show "(f has_contour_integral 0) (linepath a b +++ linepath b c +++ linepath c a)"
  6.1425          apply (rule less.hyps [of "s'"])
  6.1426          using False d \<open>finite s\<close> interior_subset
  6.1427          apply (auto intro!: less.prems)
  6.1428 @@ -2420,7 +2420,7 @@
  6.1429        case True
  6.1430        have *: "convex hull {a, b, d} \<subseteq> convex hull {a, b, c}"
  6.1431          by (meson True hull_subset insert_subset convex_hull_subset)
  6.1432 -      have abd: "(f has_path_integral 0) (linepath a b +++ linepath b d +++ linepath d a)"
  6.1433 +      have abd: "(f has_contour_integral 0) (linepath a b +++ linepath b d +++ linepath d a)"
  6.1434          apply (rule less.hyps [of "s'"])
  6.1435          using True d  \<open>finite s\<close> not_in_interior_convex_hull_3
  6.1436          apply (auto intro!: less.prems continuous_on_subset [OF  _ *])
  6.1437 @@ -2428,7 +2428,7 @@
  6.1438          done
  6.1439        have *: "convex hull {b, c, d} \<subseteq> convex hull {a, b, c}"
  6.1440          by (meson True hull_subset insert_subset convex_hull_subset)
  6.1441 -      have bcd: "(f has_path_integral 0) (linepath b c +++ linepath c d +++ linepath d b)"
  6.1442 +      have bcd: "(f has_contour_integral 0) (linepath b c +++ linepath c d +++ linepath d b)"
  6.1443          apply (rule less.hyps [of "s'"])
  6.1444          using True d  \<open>finite s\<close> not_in_interior_convex_hull_3
  6.1445          apply (auto intro!: less.prems continuous_on_subset [OF _ *])
  6.1446 @@ -2436,25 +2436,25 @@
  6.1447          done
  6.1448        have *: "convex hull {c, a, d} \<subseteq> convex hull {a, b, c}"
  6.1449          by (meson True hull_subset insert_subset convex_hull_subset)
  6.1450 -      have cad: "(f has_path_integral 0) (linepath c a +++ linepath a d +++ linepath d c)"
  6.1451 +      have cad: "(f has_contour_integral 0) (linepath c a +++ linepath a d +++ linepath d c)"
  6.1452          apply (rule less.hyps [of "s'"])
  6.1453          using True d  \<open>finite s\<close> not_in_interior_convex_hull_3
  6.1454          apply (auto intro!: less.prems continuous_on_subset [OF _ *])
  6.1455          apply (metis * insert_absorb insert_subset interior_mono)
  6.1456          done
  6.1457 -      have "f path_integrable_on linepath a b"
  6.1458 +      have "f contour_integrable_on linepath a b"
  6.1459          using less.prems
  6.1460 -        by (metis continuous_on_subset insert_commute path_integrable_continuous_linepath segments_subset_convex_hull(3))
  6.1461 -      moreover have "f path_integrable_on linepath b c"
  6.1462 +        by (metis continuous_on_subset insert_commute contour_integrable_continuous_linepath segments_subset_convex_hull(3))
  6.1463 +      moreover have "f contour_integrable_on linepath b c"
  6.1464          using less.prems
  6.1465 -        by (metis continuous_on_subset path_integrable_continuous_linepath segments_subset_convex_hull(3))
  6.1466 -      moreover have "f path_integrable_on linepath c a"
  6.1467 +        by (metis continuous_on_subset contour_integrable_continuous_linepath segments_subset_convex_hull(3))
  6.1468 +      moreover have "f contour_integrable_on linepath c a"
  6.1469          using less.prems
  6.1470 -        by (metis continuous_on_subset insert_commute path_integrable_continuous_linepath segments_subset_convex_hull(3))
  6.1471 -      ultimately have fpi: "f path_integrable_on (linepath a b +++ linepath b c +++ linepath c a)"
  6.1472 +        by (metis continuous_on_subset insert_commute contour_integrable_continuous_linepath segments_subset_convex_hull(3))
  6.1473 +      ultimately have fpi: "f contour_integrable_on (linepath a b +++ linepath b c +++ linepath c a)"
  6.1474          by auto
  6.1475        { fix y::complex
  6.1476 -        assume fy: "(f has_path_integral y) (linepath a b +++ linepath b c +++ linepath c a)"
  6.1477 +        assume fy: "(f has_contour_integral y) (linepath a b +++ linepath b c +++ linepath c a)"
  6.1478             and ynz: "y \<noteq> 0"
  6.1479          have cont_ad: "continuous_on (closed_segment a d) f"
  6.1480            by (meson "*" continuous_on_subset less.prems(1) segments_subset_convex_hull(3))
  6.1481 @@ -2462,18 +2462,18 @@
  6.1482            by (meson True closed_segment_subset_convex_hull continuous_on_subset hull_subset insert_subset less.prems(1))
  6.1483          have cont_cd: "continuous_on (closed_segment c d) f"
  6.1484            by (meson "*" continuous_on_subset less.prems(1) segments_subset_convex_hull(2))
  6.1485 -        have "path_integral  (linepath a b) f = - (path_integral (linepath b d) f + (path_integral (linepath d a) f))"
  6.1486 -                "path_integral  (linepath b c) f = - (path_integral (linepath c d) f + (path_integral (linepath d b) f))"
  6.1487 -                "path_integral  (linepath c a) f = - (path_integral (linepath a d) f + path_integral (linepath d c) f)"
  6.1488 +        have "contour_integral  (linepath a b) f = - (contour_integral (linepath b d) f + (contour_integral (linepath d a) f))"
  6.1489 +                "contour_integral  (linepath b c) f = - (contour_integral (linepath c d) f + (contour_integral (linepath d b) f))"
  6.1490 +                "contour_integral  (linepath c a) f = - (contour_integral (linepath a d) f + contour_integral (linepath d c) f)"
  6.1491              using has_chain_integral_chain_integral3 [OF abd]
  6.1492                    has_chain_integral_chain_integral3 [OF bcd]
  6.1493                    has_chain_integral_chain_integral3 [OF cad]
  6.1494              by (simp_all add: algebra_simps add_eq_0_iff)
  6.1495          then have ?thesis
  6.1496 -          using cont_ad cont_bd cont_cd fy has_chain_integral_chain_integral3 path_integral_reverse_linepath by fastforce
  6.1497 +          using cont_ad cont_bd cont_cd fy has_chain_integral_chain_integral3 contour_integral_reverse_linepath by fastforce
  6.1498        }
  6.1499        then show ?thesis
  6.1500 -        using fpi path_integrable_on_def by blast
  6.1501 +        using fpi contour_integrable_on_def by blast
  6.1502      qed
  6.1503    qed
  6.1504  qed
  6.1505 @@ -2489,17 +2489,17 @@
  6.1506        apply (meson subs convexD convex_closed_segment ends_in_segment(1) ends_in_segment(2) subsetCE)
  6.1507        done
  6.1508  
  6.1509 -lemma triangle_path_integrals_starlike_primitive:
  6.1510 +lemma triangle_contour_integrals_starlike_primitive:
  6.1511    assumes contf: "continuous_on s f"
  6.1512        and s: "a \<in> s" "open s"
  6.1513        and x: "x \<in> s"
  6.1514        and subs: "\<And>y. y \<in> s \<Longrightarrow> closed_segment a y \<subseteq> s"
  6.1515        and zer: "\<And>b c. closed_segment b c \<subseteq> s
  6.1516 -                   \<Longrightarrow> path_integral (linepath a b) f + path_integral (linepath b c) f +
  6.1517 -                       path_integral (linepath c a) f = 0"
  6.1518 -    shows "((\<lambda>x. path_integral(linepath a x) f) has_field_derivative f x) (at x)"
  6.1519 +                   \<Longrightarrow> contour_integral (linepath a b) f + contour_integral (linepath b c) f +
  6.1520 +                       contour_integral (linepath c a) f = 0"
  6.1521 +    shows "((\<lambda>x. contour_integral(linepath a x) f) has_field_derivative f x) (at x)"
  6.1522  proof -
  6.1523 -  let ?pathint = "\<lambda>x y. path_integral(linepath x y) f"
  6.1524 +  let ?pathint = "\<lambda>x y. contour_integral(linepath x y) f"
  6.1525    { fix e y
  6.1526      assume e: "0 < e" and bxe: "ball x e \<subseteq> s" and close: "cmod (y - x) < e"
  6.1527      have y: "y \<in> s"
  6.1528 @@ -2511,7 +2511,7 @@
  6.1529        using close
  6.1530        by (auto simp: dist_norm ball_def norm_minus_commute dest: segment_bound)
  6.1531      have "?pathint a y - ?pathint a x = ?pathint x y"
  6.1532 -      using zer [OF xys]  path_integral_reverse_linepath [OF cont_ayf]  add_eq_0_iff by force
  6.1533 +      using zer [OF xys]  contour_integral_reverse_linepath [OF cont_ayf]  add_eq_0_iff by force
  6.1534    } note [simp] = this
  6.1535    { fix e::real
  6.1536      assume e: "0 < e"
  6.1537 @@ -2527,18 +2527,18 @@
  6.1538        assume yx: "y \<noteq> x" and close: "cmod (y - x) < min d1 d2"
  6.1539        have y: "y \<in> s"
  6.1540          using d2 close  by (force simp: dist_norm norm_minus_commute)
  6.1541 -      have fxy: "f path_integrable_on linepath x y"
  6.1542 -        apply (rule path_integrable_continuous_linepath)
  6.1543 +      have fxy: "f contour_integrable_on linepath x y"
  6.1544 +        apply (rule contour_integrable_continuous_linepath)
  6.1545          apply (rule continuous_on_subset [OF contf])
  6.1546          using close d2
  6.1547          apply (auto simp: dist_norm norm_minus_commute dest!: segment_bound(1))
  6.1548          done
  6.1549 -      then obtain i where i: "(f has_path_integral i) (linepath x y)"
  6.1550 -        by (auto simp: path_integrable_on_def)
  6.1551 -      then have "((\<lambda>w. f w - f x) has_path_integral (i - f x * (y - x))) (linepath x y)"
  6.1552 -        by (rule has_path_integral_diff [OF _ has_path_integral_const_linepath])
  6.1553 +      then obtain i where i: "(f has_contour_integral i) (linepath x y)"
  6.1554 +        by (auto simp: contour_integrable_on_def)
  6.1555 +      then have "((\<lambda>w. f w - f x) has_contour_integral (i - f x * (y - x))) (linepath x y)"
  6.1556 +        by (rule has_contour_integral_diff [OF _ has_contour_integral_const_linepath])
  6.1557        then have "cmod (i - f x * (y - x)) \<le> e / 2 * cmod (y - x)"
  6.1558 -        apply (rule has_path_integral_bound_linepath [where B = "e/2"])
  6.1559 +        apply (rule has_contour_integral_bound_linepath [where B = "e/2"])
  6.1560          using e apply simp
  6.1561          apply (rule d1_less [THEN less_imp_le])
  6.1562          using close segment_bound
  6.1563 @@ -2547,7 +2547,7 @@
  6.1564        also have "... < e * cmod (y - x)"
  6.1565          by (simp add: e yx)
  6.1566        finally have "cmod (?pathint x y - f x * (y-x)) / cmod (y-x) < e"
  6.1567 -        using i yx  by (simp add: path_integral_unique divide_less_eq)
  6.1568 +        using i yx  by (simp add: contour_integral_unique divide_less_eq)
  6.1569      }
  6.1570      then have "\<exists>d>0. \<forall>y. y \<noteq> x \<and> cmod (y-x) < d \<longrightarrow> cmod (?pathint x y - f x * (y-x)) / cmod (y-x) < e"
  6.1571        using dpos by blast
  6.1572 @@ -2580,7 +2580,7 @@
  6.1573        by (simp add: a a_cs starlike_convex_subset)
  6.1574      then have *: "continuous_on (convex hull {a, b, c}) f"
  6.1575        by (simp add: continuous_on_subset [OF contf])
  6.1576 -    have "(f has_path_integral 0) (linepath a b +++ linepath b c +++ linepath c a)"
  6.1577 +    have "(f has_contour_integral 0) (linepath a b +++ linepath b c +++ linepath c a)"
  6.1578        apply (rule Cauchy_theorem_triangle_cofinite [OF _ k])
  6.1579        using abcs apply (simp add: continuous_on_subset [OF contf])
  6.1580        using * abcs interior_subset apply (auto intro: fcd)
  6.1581 @@ -2588,7 +2588,7 @@
  6.1582    } note 0 = this
  6.1583    show ?thesis
  6.1584      apply (intro exI ballI)
  6.1585 -    apply (rule triangle_path_integrals_starlike_primitive [OF contf a os], assumption)
  6.1586 +    apply (rule triangle_contour_integrals_starlike_primitive [OF contf a os], assumption)
  6.1587      apply (metis a_cs)
  6.1588      apply (metis has_chain_integral_chain_integral3 0)
  6.1589      done
  6.1590 @@ -2598,12 +2598,12 @@
  6.1591   "\<lbrakk>open s; starlike s; finite k; continuous_on s f;
  6.1592     \<And>x. x \<in> s - k \<Longrightarrow> f complex_differentiable at x;
  6.1593     valid_path g; path_image g \<subseteq> s; pathfinish g = pathstart g\<rbrakk>
  6.1594 -   \<Longrightarrow> (f has_path_integral 0)  g"
  6.1595 +   \<Longrightarrow> (f has_contour_integral 0)  g"
  6.1596    by (metis holomorphic_starlike_primitive Cauchy_theorem_primitive at_within_open)
  6.1597  
  6.1598  lemma Cauchy_theorem_starlike_simple:
  6.1599    "\<lbrakk>open s; starlike s; f holomorphic_on s; valid_path g; path_image g \<subseteq> s; pathfinish g = pathstart g\<rbrakk>
  6.1600 -   \<Longrightarrow> (f has_path_integral 0) g"
  6.1601 +   \<Longrightarrow> (f has_contour_integral 0) g"
  6.1602  apply (rule Cauchy_theorem_starlike [OF _ _ finite.emptyI])
  6.1603  apply (simp_all add: holomorphic_on_imp_continuous_on)
  6.1604  apply (metis at_within_open holomorphic_on_def)
  6.1605 @@ -2614,16 +2614,16 @@
  6.1606  
  6.1607  text\<open>For a convex set we can avoid assuming openness and boundary analyticity\<close>
  6.1608  
  6.1609 -lemma triangle_path_integrals_convex_primitive:
  6.1610 +lemma triangle_contour_integrals_convex_primitive:
  6.1611    assumes contf: "continuous_on s f"
  6.1612        and s: "a \<in> s" "convex s"
  6.1613        and x: "x \<in> s"
  6.1614        and zer: "\<And>b c. \<lbrakk>b \<in> s; c \<in> s\<rbrakk>
  6.1615 -                   \<Longrightarrow> path_integral (linepath a b) f + path_integral (linepath b c) f +
  6.1616 -                       path_integral (linepath c a) f = 0"
  6.1617 -    shows "((\<lambda>x. path_integral(linepath a x) f) has_field_derivative f x) (at x within s)"
  6.1618 +                   \<Longrightarrow> contour_integral (linepath a b) f + contour_integral (linepath b c) f +
  6.1619 +                       contour_integral (linepath c a) f = 0"
  6.1620 +    shows "((\<lambda>x. contour_integral(linepath a x) f) has_field_derivative f x) (at x within s)"
  6.1621  proof -
  6.1622 -  let ?pathint = "\<lambda>x y. path_integral(linepath x y) f"
  6.1623 +  let ?pathint = "\<lambda>x y. contour_integral(linepath x y) f"
  6.1624    { fix y
  6.1625      assume y: "y \<in> s"
  6.1626      have cont_ayf: "continuous_on (closed_segment a y) f"
  6.1627 @@ -2631,7 +2631,7 @@
  6.1628      have xys: "closed_segment x y \<subseteq> s"  (*?*)
  6.1629        using convex_contains_segment s x y by auto
  6.1630      have "?pathint a y - ?pathint a x = ?pathint x y"
  6.1631 -      using zer [OF x y]  path_integral_reverse_linepath [OF cont_ayf]  add_eq_0_iff by force
  6.1632 +      using zer [OF x y]  contour_integral_reverse_linepath [OF cont_ayf]  add_eq_0_iff by force
  6.1633    } note [simp] = this
  6.1634    { fix e::real
  6.1635      assume e: "0 < e"
  6.1636 @@ -2642,15 +2642,15 @@
  6.1637        by (drule_tac x="e/2" in spec) force
  6.1638      { fix y
  6.1639        assume yx: "y \<noteq> x" and close: "cmod (y - x) < d1" and y: "y \<in> s"
  6.1640 -      have fxy: "f path_integrable_on linepath x y"
  6.1641 +      have fxy: "f contour_integrable_on linepath x y"
  6.1642          using convex_contains_segment s x y
  6.1643 -        by (blast intro!: path_integrable_continuous_linepath continuous_on_subset [OF contf])
  6.1644 -      then obtain i where i: "(f has_path_integral i) (linepath x y)"
  6.1645 -        by (auto simp: path_integrable_on_def)
  6.1646 -      then have "((\<lambda>w. f w - f x) has_path_integral (i - f x * (y - x))) (linepath x y)"
  6.1647 -        by (rule has_path_integral_diff [OF _ has_path_integral_const_linepath])
  6.1648 +        by (blast intro!: contour_integrable_continuous_linepath continuous_on_subset [OF contf])
  6.1649 +      then obtain i where i: "(f has_contour_integral i) (linepath x y)"
  6.1650 +        by (auto simp: contour_integrable_on_def)
  6.1651 +      then have "((\<lambda>w. f w - f x) has_contour_integral (i - f x * (y - x))) (linepath x y)"
  6.1652 +        by (rule has_contour_integral_diff [OF _ has_contour_integral_const_linepath])
  6.1653        then have "cmod (i - f x * (y - x)) \<le> e / 2 * cmod (y - x)"
  6.1654 -        apply (rule has_path_integral_bound_linepath [where B = "e/2"])
  6.1655 +        apply (rule has_contour_integral_bound_linepath [where B = "e/2"])
  6.1656          using e apply simp
  6.1657          apply (rule d1_less [THEN less_imp_le])
  6.1658          using convex_contains_segment s(2) x y apply blast
  6.1659 @@ -2659,12 +2659,12 @@
  6.1660        also have "... < e * cmod (y - x)"
  6.1661          by (simp add: e yx)
  6.1662        finally have "cmod (?pathint x y - f x * (y-x)) / cmod (y-x) < e"
  6.1663 -        using i yx  by (simp add: path_integral_unique divide_less_eq)
  6.1664 +        using i yx  by (simp add: contour_integral_unique divide_less_eq)
  6.1665      }
  6.1666      then have "\<exists>d>0. \<forall>y\<in>s. y \<noteq> x \<and> cmod (y-x) < d \<longrightarrow> cmod (?pathint x y - f x * (y-x)) / cmod (y-x) < e"
  6.1667        using d1 by blast
  6.1668    }
  6.1669 -  then have *: "((\<lambda>y. (path_integral (linepath x y) f - f x * (y - x)) /\<^sub>R cmod (y - x)) ---> 0) (at x within s)"
  6.1670 +  then have *: "((\<lambda>y. (contour_integral (linepath x y) f - f x * (y - x)) /\<^sub>R cmod (y - x)) ---> 0) (at x within s)"
  6.1671      by (simp add: Lim_within dist_norm inverse_eq_divide)
  6.1672    show ?thesis
  6.1673      apply (simp add: has_field_derivative_def has_derivative_within bounded_linear_mult_right)
  6.1674 @@ -2676,11 +2676,11 @@
  6.1675  
  6.1676  lemma pathintegral_convex_primitive:
  6.1677    "\<lbrakk>convex s; continuous_on s f;
  6.1678 -    \<And>a b c. \<lbrakk>a \<in> s; b \<in> s; c \<in> s\<rbrakk> \<Longrightarrow> (f has_path_integral 0) (linepath a b +++ linepath b c +++ linepath c a)\<rbrakk>
  6.1679 +    \<And>a b c. \<lbrakk>a \<in> s; b \<in> s; c \<in> s\<rbrakk> \<Longrightarrow> (f has_contour_integral 0) (linepath a b +++ linepath b c +++ linepath c a)\<rbrakk>
  6.1680           \<Longrightarrow> \<exists>g. \<forall>x \<in> s. (g has_field_derivative f x) (at x within s)"
  6.1681    apply (cases "s={}")
  6.1682    apply (simp_all add: ex_in_conv [symmetric])
  6.1683 -  apply (blast intro: triangle_path_integrals_convex_primitive has_chain_integral_chain_integral3)
  6.1684 +  apply (blast intro: triangle_contour_integrals_convex_primitive has_chain_integral_chain_integral3)
  6.1685    done
  6.1686  
  6.1687  lemma holomorphic_convex_primitive:
  6.1688 @@ -2694,16 +2694,16 @@
  6.1689  by (metis Diff_iff convex_contains_segment insert_absorb insert_subset interior_mono segment_convex_hull subset_hull)
  6.1690  
  6.1691  lemma Cauchy_theorem_convex:
  6.1692 -    "\<lbrakk>continuous_on s f;convex s; finite k;
  6.1693 +    "\<lbrakk>continuous_on s f; convex s; finite k;
  6.1694        \<And>x. x \<in> interior s - k \<Longrightarrow> f complex_differentiable at x;
  6.1695       valid_path g; path_image g \<subseteq> s;
  6.1696 -     pathfinish g = pathstart g\<rbrakk> \<Longrightarrow> (f has_path_integral 0) g"
  6.1697 +     pathfinish g = pathstart g\<rbrakk> \<Longrightarrow> (f has_contour_integral 0) g"
  6.1698    by (metis holomorphic_convex_primitive Cauchy_theorem_primitive)
  6.1699  
  6.1700  lemma Cauchy_theorem_convex_simple:
  6.1701      "\<lbrakk>f holomorphic_on s; convex s;
  6.1702       valid_path g; path_image g \<subseteq> s;
  6.1703 -     pathfinish g = pathstart g\<rbrakk> \<Longrightarrow> (f has_path_integral 0) g"
  6.1704 +     pathfinish g = pathstart g\<rbrakk> \<Longrightarrow> (f has_contour_integral 0) g"
  6.1705    apply (rule Cauchy_theorem_convex)
  6.1706    apply (simp_all add: holomorphic_on_imp_continuous_on)
  6.1707    apply (rule finite.emptyI)
  6.1708 @@ -2715,20 +2715,20 @@
  6.1709      "\<lbrakk>finite k; continuous_on (cball a e) f;
  6.1710        \<And>x. x \<in> ball a e - k \<Longrightarrow> f complex_differentiable at x;
  6.1711       valid_path g; path_image g \<subseteq> cball a e;
  6.1712 -     pathfinish g = pathstart g\<rbrakk> \<Longrightarrow> (f has_path_integral 0) g"
  6.1713 +     pathfinish g = pathstart g\<rbrakk> \<Longrightarrow> (f has_contour_integral 0) g"
  6.1714    apply (rule Cauchy_theorem_convex)
  6.1715    apply (auto simp: convex_cball interior_cball)
  6.1716    done
  6.1717  
  6.1718  lemma Cauchy_theorem_disc_simple:
  6.1719      "\<lbrakk>f holomorphic_on (ball a e); valid_path g; path_image g \<subseteq> ball a e;
  6.1720 -     pathfinish g = pathstart g\<rbrakk> \<Longrightarrow> (f has_path_integral 0) g"
  6.1721 +     pathfinish g = pathstart g\<rbrakk> \<Longrightarrow> (f has_contour_integral 0) g"
  6.1722  by (simp add: Cauchy_theorem_convex_simple)
  6.1723  
  6.1724  
  6.1725  subsection\<open>Generalize integrability to local primitives\<close>
  6.1726  
  6.1727 -lemma path_integral_local_primitive_lemma:
  6.1728 +lemma contour_integral_local_primitive_lemma:
  6.1729    fixes f :: "complex\<Rightarrow>complex"
  6.1730    shows
  6.1731      "\<lbrakk>g piecewise_differentiable_on {a..b};
  6.1732 @@ -2739,10 +2739,10 @@
  6.1733    apply (cases "cbox a b = {}", force)
  6.1734    apply (simp add: integrable_on_def)
  6.1735    apply (rule exI)
  6.1736 -  apply (rule path_integral_primitive_lemma, assumption+)
  6.1737 +  apply (rule contour_integral_primitive_lemma, assumption+)
  6.1738    using atLeastAtMost_iff by blast
  6.1739  
  6.1740 -lemma path_integral_local_primitive_any:
  6.1741 +lemma contour_integral_local_primitive_any:
  6.1742    fixes f :: "complex \<Rightarrow> complex"
  6.1743    assumes gpd: "g piecewise_differentiable_on {a..b}"
  6.1744        and dh: "\<And>x. x \<in> s
  6.1745 @@ -2769,7 +2769,7 @@
  6.1746        apply (rule_tac x=e in exI)
  6.1747        using e
  6.1748        apply (simp add: integrable_on_localized_vector_derivative [symmetric], clarify)
  6.1749 -      apply (rule_tac f = h and s = "g ` {u..v}" in path_integral_local_primitive_lemma)
  6.1750 +      apply (rule_tac f = h and s = "g ` {u..v}" in contour_integral_local_primitive_lemma)
  6.1751          apply (meson atLeastatMost_subset_iff gpd piecewise_differentiable_on_subset)
  6.1752         apply (force simp: ball_def dist_norm intro: lessd gs DERIV_subset [OF h], force)
  6.1753        done
  6.1754 @@ -2778,29 +2778,29 @@
  6.1755      by (force simp: intro!: integrable_on_little_subintervals [of a b, simplified])
  6.1756  qed
  6.1757  
  6.1758 -lemma path_integral_local_primitive:
  6.1759 +lemma contour_integral_local_primitive:
  6.1760    fixes f :: "complex \<Rightarrow> complex"
  6.1761    assumes g: "valid_path g" "path_image g \<subseteq> s"
  6.1762        and dh: "\<And>x. x \<in> s
  6.1763                 \<Longrightarrow> \<exists>d h. 0 < d \<and>
  6.1764                           (\<forall>y. norm(y - x) < d \<longrightarrow> (h has_field_derivative f y) (at y within s))"
  6.1765 -  shows "f path_integrable_on g"
  6.1766 +  shows "f contour_integrable_on g"
  6.1767    using g
  6.1768 -  apply (simp add: valid_path_def path_image_def path_integrable_on_def has_path_integral_def
  6.1769 +  apply (simp add: valid_path_def path_image_def contour_integrable_on_def has_contour_integral_def
  6.1770              has_integral_localized_vector_derivative integrable_on_def [symmetric])
  6.1771 -  using path_integral_local_primitive_any [OF _ dh]
  6.1772 +  using contour_integral_local_primitive_any [OF _ dh]
  6.1773    by (meson image_subset_iff piecewise_C1_imp_differentiable)
  6.1774  
  6.1775  
  6.1776  text\<open>In particular if a function is holomorphic\<close>
  6.1777  
  6.1778 -lemma path_integrable_holomorphic:
  6.1779 +lemma contour_integrable_holomorphic:
  6.1780    assumes contf: "continuous_on s f"
  6.1781        and os: "open s"
  6.1782        and k: "finite k"
  6.1783        and g: "valid_path g" "path_image g \<subseteq> s"
  6.1784        and fcd: "\<And>x. x \<in> s - k \<Longrightarrow> f complex_differentiable at x"
  6.1785 -    shows "f path_integrable_on g"
  6.1786 +    shows "f contour_integrable_on g"
  6.1787  proof -
  6.1788    { fix z
  6.1789      assume z: "z \<in> s"
  6.1790 @@ -2819,25 +2819,25 @@
  6.1791        using d by blast
  6.1792    }
  6.1793    then show ?thesis
  6.1794 -    by (rule path_integral_local_primitive [OF g])
  6.1795 +    by (rule contour_integral_local_primitive [OF g])
  6.1796  qed
  6.1797  
  6.1798 -lemma path_integrable_holomorphic_simple:
  6.1799 +lemma contour_integrable_holomorphic_simple:
  6.1800    assumes contf: "continuous_on s f"
  6.1801        and os: "open s"
  6.1802        and g: "valid_path g" "path_image g \<subseteq> s"
  6.1803        and fh: "f holomorphic_on s"
  6.1804 -    shows "f path_integrable_on g"
  6.1805 -  apply (rule path_integrable_holomorphic [OF contf os Finite_Set.finite.emptyI g])
  6.1806 +    shows "f contour_integrable_on g"
  6.1807 +  apply (rule contour_integrable_holomorphic [OF contf os Finite_Set.finite.emptyI g])
  6.1808    using fh  by (simp add: complex_differentiable_def holomorphic_on_open os)
  6.1809  
  6.1810  lemma continuous_on_inversediff:
  6.1811    fixes z:: "'a::real_normed_field" shows "z \<notin> s \<Longrightarrow> continuous_on s (\<lambda>w. 1 / (w - z))"
  6.1812    by (rule continuous_intros | force)+
  6.1813  
  6.1814 -corollary path_integrable_inversediff:
  6.1815 -    "\<lbrakk>valid_path g; z \<notin> path_image g\<rbrakk> \<Longrightarrow> (\<lambda>w. 1 / (w-z)) path_integrable_on g"
  6.1816 -apply (rule path_integrable_holomorphic_simple [of "UNIV-{z}", OF continuous_on_inversediff])
  6.1817 +corollary contour_integrable_inversediff:
  6.1818 +    "\<lbrakk>valid_path g; z \<notin> path_image g\<rbrakk> \<Longrightarrow> (\<lambda>w. 1 / (w-z)) contour_integrable_on g"
  6.1819 +apply (rule contour_integrable_holomorphic_simple [of "UNIV-{z}", OF continuous_on_inversediff])
  6.1820  apply (auto simp: holomorphic_on_open open_delete intro!: derivative_eq_intros)
  6.1821  done
  6.1822  
  6.1823 @@ -2858,7 +2858,7 @@
  6.1824  
  6.1825  text\<open>This formulation covers two cases: @{term g} and @{term h} share their
  6.1826        start and end points; @{term g} and @{term h} both loop upon themselves.\<close>
  6.1827 -lemma path_integral_nearby:
  6.1828 +lemma contour_integral_nearby:
  6.1829    assumes os: "open s" and p: "path p" "path_image p \<subseteq> s"
  6.1830      shows
  6.1831         "\<exists>d. 0 < d \<and>
  6.1832 @@ -2866,7 +2866,7 @@
  6.1833                    (\<forall>t \<in> {0..1}. norm(g t - p t) < d \<and> norm(h t - p t) < d) \<and>
  6.1834                    linked_paths atends g h
  6.1835                    \<longrightarrow> path_image g \<subseteq> s \<and> path_image h \<subseteq> s \<and>
  6.1836 -                      (\<forall>f. f holomorphic_on s \<longrightarrow> path_integral h f = path_integral g f))"
  6.1837 +                      (\<forall>f. f holomorphic_on s \<longrightarrow> contour_integral h f = contour_integral g f))"
  6.1838  proof -
  6.1839    have "\<forall>z. \<exists>e. z \<in> path_image p \<longrightarrow> 0 < e \<and> ball z e \<subseteq> s"
  6.1840      using open_contains_ball os p(2) by blast
  6.1841 @@ -2931,8 +2931,8 @@
  6.1842      moreover
  6.1843      { fix f
  6.1844        assume fhols: "f holomorphic_on s"
  6.1845 -      then have fpa: "f path_integrable_on g"  "f path_integrable_on h"
  6.1846 -        using g ghs h holomorphic_on_imp_continuous_on os path_integrable_holomorphic_simple
  6.1847 +      then have fpa: "f contour_integrable_on g"  "f contour_integrable_on h"
  6.1848 +        using g ghs h holomorphic_on_imp_continuous_on os contour_integrable_holomorphic_simple
  6.1849          by blast+
  6.1850        have contf: "continuous_on s f"
  6.1851          by (simp add: fhols holomorphic_on_imp_continuous_on)
  6.1852 @@ -2949,8 +2949,8 @@
  6.1853          by metis
  6.1854        { fix n
  6.1855          assume n: "n \<le> N"
  6.1856 -        then have "path_integral(subpath 0 (n/N) h) f - path_integral(subpath 0 (n/N) g) f =
  6.1857 -                   path_integral(linepath (g(n/N)) (h(n/N))) f - path_integral(linepath (g 0) (h 0)) f"
  6.1858 +        then have "contour_integral(subpath 0 (n/N) h) f - contour_integral(subpath 0 (n/N) g) f =
  6.1859 +                   contour_integral(linepath (g(n/N)) (h(n/N))) f - contour_integral(linepath (g 0) (h 0)) f"
  6.1860          proof (induct n)
  6.1861            case 0 show ?case by simp
  6.1862          next
  6.1863 @@ -3014,7 +3014,7 @@
  6.1864              using \<open>N>0\<close> Suc.prems
  6.1865              apply (auto simp: dist_norm field_simps closed_segment_eq_real_ivl ptgh_ee)
  6.1866              done
  6.1867 -          have pi0: "(f has_path_integral 0)
  6.1868 +          have pi0: "(f has_contour_integral 0)
  6.1869                         (subpath (n/ N) ((Suc n)/N) g +++ linepath(g ((Suc n) / N)) (h((Suc n) / N)) +++
  6.1870                          subpath ((Suc n) / N) (n/N) h +++ linepath(h (n/N)) (g (n/N)))"
  6.1871              apply (rule Cauchy_theorem_primitive [of "ball(p t) (ee(p t))" "ff (p t)" "f"])
  6.1872 @@ -3022,50 +3022,50 @@
  6.1873              apply (intro valid_path_join)
  6.1874              using Suc.prems pi_subset_ball apply (simp_all add: valid_path_subpath g h)
  6.1875              done
  6.1876 -          have fpa1: "f path_integrable_on subpath (real n / real N) (real (Suc n) / real N) g"
  6.1877 -            using Suc.prems by (simp add: path_integrable_subpath g fpa)
  6.1878 -          have fpa2: "f path_integrable_on linepath (g (real (Suc n) / real N)) (h (real (Suc n) / real N))"
  6.1879 +          have fpa1: "f contour_integrable_on subpath (real n / real N) (real (Suc n) / real N) g"
  6.1880 +            using Suc.prems by (simp add: contour_integrable_subpath g fpa)
  6.1881 +          have fpa2: "f contour_integrable_on linepath (g (real (Suc n) / real N)) (h (real (Suc n) / real N))"
  6.1882              using gh_n's
  6.1883 -            by (auto intro!: path_integrable_continuous_linepath continuous_on_subset [OF contf])
  6.1884 -          have fpa3: "f path_integrable_on linepath (h (real n / real N)) (g (real n / real N))"
  6.1885 +            by (auto intro!: contour_integrable_continuous_linepath continuous_on_subset [OF contf])
  6.1886 +          have fpa3: "f contour_integrable_on linepath (h (real n / real N)) (g (real n / real N))"
  6.1887              using gh_ns
  6.1888 -            by (auto simp: closed_segment_commute intro!: path_integrable_continuous_linepath continuous_on_subset [OF contf])
  6.1889 -          have eq0: "path_integral (subpath (n/N) ((Suc n) / real N) g) f +
  6.1890 -                     path_integral (linepath (g ((Suc n) / N)) (h ((Suc n) / N))) f +
  6.1891 -                     path_integral (subpath ((Suc n) / N) (n/N) h) f +
  6.1892 -                     path_integral (linepath (h (n/N)) (g (n/N))) f = 0"
  6.1893 -            using path_integral_unique [OF pi0] Suc.prems
  6.1894 -            by (simp add: g h fpa valid_path_subpath path_integrable_subpath
  6.1895 +            by (auto simp: closed_segment_commute intro!: contour_integrable_continuous_linepath continuous_on_subset [OF contf])
  6.1896 +          have eq0: "contour_integral (subpath (n/N) ((Suc n) / real N) g) f +
  6.1897 +                     contour_integral (linepath (g ((Suc n) / N)) (h ((Suc n) / N))) f +
  6.1898 +                     contour_integral (subpath ((Suc n) / N) (n/N) h) f +
  6.1899 +                     contour_integral (linepath (h (n/N)) (g (n/N))) f = 0"
  6.1900 +            using contour_integral_unique [OF pi0] Suc.prems
  6.1901 +            by (simp add: g h fpa valid_path_subpath contour_integrable_subpath
  6.1902                            fpa1 fpa2 fpa3 algebra_simps del: of_nat_Suc)
  6.1903            have *: "\<And>hn he hn' gn gd gn' hgn ghn gh0 ghn'.
  6.1904                      \<lbrakk>hn - gn = ghn - gh0;
  6.1905                       gd + ghn' + he + hgn = (0::complex);
  6.1906                       hn - he = hn'; gn + gd = gn'; hgn = -ghn\<rbrakk> \<Longrightarrow> hn' - gn' = ghn' - gh0"
  6.1907              by (auto simp: algebra_simps)
  6.1908 -          have "path_integral (subpath 0 (n/N) h) f - path_integral (subpath ((Suc n) / N) (n/N) h) f =
  6.1909 -                path_integral (subpath 0 (n/N) h) f + path_integral (subpath (n/N) ((Suc n) / N) h) f"
  6.1910 +          have "contour_integral (subpath 0 (n/N) h) f - contour_integral (subpath ((Suc n) / N) (n/N) h) f =
  6.1911 +                contour_integral (subpath 0 (n/N) h) f + contour_integral (subpath (n/N) ((Suc n) / N) h) f"
  6.1912              unfolding reversepath_subpath [symmetric, of "((Suc n) / N)"]
  6.1913 -            using Suc.prems by (simp add: h fpa path_integral_reversepath valid_path_subpath path_integrable_subpath)
  6.1914 -          also have "... = path_integral (subpath 0 ((Suc n) / N) h) f"
  6.1915 -            using Suc.prems by (simp add: path_integral_subpath_combine h fpa)
  6.1916 +            using Suc.prems by (simp add: h fpa contour_integral_reversepath valid_path_subpath contour_integrable_subpath)
  6.1917 +          also have "... = contour_integral (subpath 0 ((Suc n) / N) h) f"
  6.1918 +            using Suc.prems by (simp add: contour_integral_subpath_combine h fpa)
  6.1919            finally have pi0_eq:
  6.1920 -               "path_integral (subpath 0 (n/N) h) f - path_integral (subpath ((Suc n) / N) (n/N) h) f =
  6.1921 -                path_integral (subpath 0 ((Suc n) / N) h) f" .
  6.1922 +               "contour_integral (subpath 0 (n/N) h) f - contour_integral (subpath ((Suc n) / N) (n/N) h) f =
  6.1923 +                contour_integral (subpath 0 ((Suc n) / N) h) f" .
  6.1924            show ?case
  6.1925              apply (rule * [OF Suc.hyps eq0 pi0_eq])
  6.1926              using Suc.prems
  6.1927 -            apply (simp_all add: g h fpa path_integral_subpath_combine
  6.1928 -                     path_integral_reversepath [symmetric] path_integrable_continuous_linepath
  6.1929 +            apply (simp_all add: g h fpa contour_integral_subpath_combine
  6.1930 +                     contour_integral_reversepath [symmetric] contour_integrable_continuous_linepath
  6.1931                       continuous_on_subset [OF contf gh_ns])
  6.1932              done
  6.1933        qed
  6.1934        } note ind = this
  6.1935 -      have "path_integral h f = path_integral g f"
  6.1936 +      have "contour_integral h f = contour_integral g f"
  6.1937          using ind [OF order_refl] N joins
  6.1938          by (simp add: linked_paths_def pathstart_def pathfinish_def split: split_if_asm)
  6.1939      }
  6.1940      ultimately
  6.1941 -    have "path_image g \<subseteq> s \<and> path_image h \<subseteq> s \<and> (\<forall>f. f holomorphic_on s \<longrightarrow> path_integral h f = path_integral g f)"
  6.1942 +    have "path_image g \<subseteq> s \<and> path_image h \<subseteq> s \<and> (\<forall>f. f holomorphic_on s \<longrightarrow> contour_integral h f = contour_integral g f)"
  6.1943        by metis
  6.1944    } note * = this
  6.1945    show ?thesis
  6.1946 @@ -3080,7 +3080,7 @@
  6.1947  
  6.1948  lemma
  6.1949    assumes "open s" "path p" "path_image p \<subseteq> s"
  6.1950 -    shows path_integral_nearby_ends:
  6.1951 +    shows contour_integral_nearby_ends:
  6.1952        "\<exists>d. 0 < d \<and>
  6.1953                (\<forall>g h. valid_path g \<and> valid_path h \<and>
  6.1954                      (\<forall>t \<in> {0..1}. norm(g t - p t) < d \<and> norm(h t - p t) < d) \<and>
  6.1955 @@ -3088,8 +3088,8 @@
  6.1956                      \<longrightarrow> path_image g \<subseteq> s \<and>
  6.1957                          path_image h \<subseteq> s \<and>
  6.1958                          (\<forall>f. f holomorphic_on s
  6.1959 -                            \<longrightarrow> path_integral h f = path_integral g f))"
  6.1960 -    and path_integral_nearby_loops:
  6.1961 +                            \<longrightarrow> contour_integral h f = contour_integral g f))"
  6.1962 +    and contour_integral_nearby_loops:
  6.1963        "\<exists>d. 0 < d \<and>
  6.1964                (\<forall>g h. valid_path g \<and> valid_path h \<and>
  6.1965                      (\<forall>t \<in> {0..1}. norm(g t - p t) < d \<and> norm(h t - p t) < d) \<and>
  6.1966 @@ -3097,9 +3097,9 @@
  6.1967                      \<longrightarrow> path_image g \<subseteq> s \<and>
  6.1968                          path_image h \<subseteq> s \<and>
  6.1969                          (\<forall>f. f holomorphic_on s
  6.1970 -                            \<longrightarrow> path_integral h f = path_integral g f))"
  6.1971 -  using path_integral_nearby [OF assms, where atends=True]
  6.1972 -  using path_integral_nearby [OF assms, where atends=False]
  6.1973 +                            \<longrightarrow> contour_integral h f = contour_integral g f))"
  6.1974 +  using contour_integral_nearby [OF assms, where atends=True]
  6.1975 +  using contour_integral_nearby [OF assms, where atends=False]
  6.1976    unfolding linked_paths_def by simp_all
  6.1977  
  6.1978  corollary differentiable_polynomial_function:
  6.1979 @@ -3122,21 +3122,21 @@
  6.1980      shows "z \<noteq> g x \<Longrightarrow> valid_path (subpath x x g)"
  6.1981    by (simp add: subpath_def valid_path_polynomial_function)
  6.1982  
  6.1983 -lemma path_integral_bound_exists:
  6.1984 +lemma contour_integral_bound_exists:
  6.1985  assumes s: "open s"
  6.1986      and g: "valid_path g"
  6.1987      and pag: "path_image g \<subseteq> s"
  6.1988    shows "\<exists>L. 0 < L \<and>
  6.1989         (\<forall>f B. f holomorphic_on s \<and> (\<forall>z \<in> s. norm(f z) \<le> B)
  6.1990 -         \<longrightarrow> norm(path_integral g f) \<le> L*B)"
  6.1991 +         \<longrightarrow> norm(contour_integral g f) \<le> L*B)"
  6.1992  proof -
  6.1993  have "path g" using g
  6.1994    by (simp add: valid_path_imp_path)
  6.1995  then obtain d::real and p
  6.1996    where d: "0 < d"
  6.1997      and p: "polynomial_function p" "path_image p \<subseteq> s"
  6.1998 -    and pi: "\<And>f. f holomorphic_on s \<Longrightarrow> path_integral g f = path_integral p f"
  6.1999 -  using path_integral_nearby_ends [OF s \<open>path g\<close> pag]
  6.2000 +    and pi: "\<And>f. f holomorphic_on s \<Longrightarrow> contour_integral g f = contour_integral p f"
  6.2001 +  using contour_integral_nearby_ends [OF s \<open>path g\<close> pag]
  6.2002    apply clarify
  6.2003    apply (drule_tac x=g in spec)
  6.2004    apply (simp only: assms)
  6.2005 @@ -3153,24 +3153,24 @@
  6.2006  { fix f B
  6.2007    assume f: "f holomorphic_on s"
  6.2008       and B: "\<And>z. z\<in>s \<Longrightarrow> cmod (f z) \<le> B"
  6.2009 -  then have "f path_integrable_on p \<and> valid_path p"
  6.2010 +  then have "f contour_integrable_on p \<and> valid_path p"
  6.2011      using p s
  6.2012 -    by (blast intro: valid_path_polynomial_function path_integrable_holomorphic_simple holomorphic_on_imp_continuous_on)
  6.2013 +    by (blast intro: valid_path_polynomial_function contour_integrable_holomorphic_simple holomorphic_on_imp_continuous_on)
  6.2014    moreover have "\<And>x. x \<in> {0..1} \<Longrightarrow> cmod (vector_derivative p (at x)) * cmod (f (p x)) \<le> L * B"
  6.2015      apply (rule mult_mono)
  6.2016      apply (subst Derivative.vector_derivative_at; force intro: p' nop')
  6.2017      using L B p
  6.2018      apply (auto simp: path_image_def image_subset_iff)
  6.2019      done
  6.2020 -  ultimately have "cmod (path_integral g f) \<le> L * B"
  6.2021 +  ultimately have "cmod (contour_integral g f) \<le> L * B"
  6.2022      apply (simp add: pi [OF f])
  6.2023 -    apply (simp add: path_integral_integral)
  6.2024 +    apply (simp add: contour_integral_integral)
  6.2025      apply (rule order_trans [OF integral_norm_bound_integral])
  6.2026 -    apply (auto simp: mult.commute integral_norm_bound_integral path_integrable_on [symmetric] norm_mult)
  6.2027 +    apply (auto simp: mult.commute integral_norm_bound_integral contour_integrable_on [symmetric] norm_mult)
  6.2028      done
  6.2029  } then
  6.2030  show ?thesis
  6.2031 -  by (force simp: L path_integral_integral)
  6.2032 +  by (force simp: L contour_integral_integral)
  6.2033  qed
  6.2034  
  6.2035  subsection\<open>Constancy of a function from a connected set into a finite, disconnected or discrete set\<close>
  6.2036 @@ -3343,7 +3343,7 @@
  6.2037                      pathstart p = pathstart \<gamma> \<and>
  6.2038                      pathfinish p = pathfinish \<gamma> \<and>
  6.2039                      (\<forall>t \<in> {0..1}. norm(\<gamma> t - p t) < e) \<and>
  6.2040 -                    path_integral p (\<lambda>w. 1/(w - z)) = 2 * pi * ii * n"
  6.2041 +                    contour_integral p (\<lambda>w. 1/(w - z)) = 2 * pi * ii * n"
  6.2042  
  6.2043  lemma winding_number:
  6.2044    assumes "path \<gamma>" "z \<notin> path_image \<gamma>" "0 < e"
  6.2045 @@ -3351,7 +3351,7 @@
  6.2046                 pathstart p = pathstart \<gamma> \<and>
  6.2047                 pathfinish p = pathfinish \<gamma> \<and>
  6.2048                 (\<forall>t \<in> {0..1}. norm (\<gamma> t - p t) < e) \<and>
  6.2049 -               path_integral p (\<lambda>w. 1/(w - z)) = 2 * pi * ii * winding_number \<gamma> z"
  6.2050 +               contour_integral p (\<lambda>w. 1/(w - z)) = 2 * pi * ii * winding_number \<gamma> z"
  6.2051  proof -
  6.2052    have "path_image \<gamma> \<subseteq> UNIV - {z}"
  6.2053      using assms by blast
  6.2054 @@ -3361,16 +3361,16 @@
  6.2055                      (\<forall>t\<in>{0..1}. cmod (h1 t - \<gamma> t) < d \<and> cmod (h2 t - \<gamma> t) < d) \<and>
  6.2056                      pathstart h2 = pathstart h1 \<and> pathfinish h2 = pathfinish h1 \<longrightarrow>
  6.2057                        path_image h1 \<subseteq> UNIV - {z} \<and> path_image h2 \<subseteq> UNIV - {z} \<and>
  6.2058 -                      (\<forall>f. f holomorphic_on UNIV - {z} \<longrightarrow> path_integral h2 f = path_integral h1 f)"
  6.2059 -    using path_integral_nearby_ends [of "UNIV - {z}" \<gamma>] assms by (auto simp: open_delete)
  6.2060 +                      (\<forall>f. f holomorphic_on UNIV - {z} \<longrightarrow> contour_integral h2 f = contour_integral h1 f)"
  6.2061 +    using contour_integral_nearby_ends [of "UNIV - {z}" \<gamma>] assms by (auto simp: open_delete)
  6.2062    then obtain h where h: "polynomial_function h \<and> pathstart h = pathstart \<gamma> \<and> pathfinish h = pathfinish \<gamma> \<and>
  6.2063                            (\<forall>t \<in> {0..1}. norm(h t - \<gamma> t) < d/2)"
  6.2064      using path_approx_polynomial_function [OF `path \<gamma>`, of "d/2"] d by auto
  6.2065 -  def nn \<equiv> "1/(2* pi*ii) * path_integral h (\<lambda>w. 1/(w - z))"
  6.2066 +  def nn \<equiv> "1/(2* pi*ii) * contour_integral h (\<lambda>w. 1/(w - z))"
  6.2067    have "\<exists>n. \<forall>e > 0. \<exists>p. valid_path p \<and> z \<notin> path_image p \<and>
  6.2068                          pathstart p = pathstart \<gamma> \<and>  pathfinish p = pathfinish \<gamma> \<and>
  6.2069                          (\<forall>t \<in> {0..1}. norm(\<gamma> t - p t) < e) \<and>
  6.2070 -                        path_integral p (\<lambda>w. 1/(w - z)) = 2 * pi * ii * n"
  6.2071 +                        contour_integral p (\<lambda>w. 1/(w - z)) = 2 * pi * ii * n"
  6.2072                      (is "\<exists>n. \<forall>e > 0. ?PP e n")
  6.2073      proof (rule_tac x=nn in exI, clarify)
  6.2074        fix e::real
  6.2075 @@ -3399,7 +3399,7 @@
  6.2076          "\<And>e. e>0 \<Longrightarrow> \<exists>p. valid_path p \<and> z \<notin> path_image p \<and>
  6.2077                            pathstart p = pathstart \<gamma> \<and> pathfinish p = pathfinish \<gamma> \<and>
  6.2078                            (\<forall>t \<in> {0..1}. norm (\<gamma> t - p t) < e) \<and>
  6.2079 -                          path_integral p (\<lambda>w. 1/(w - z)) = 2 * pi * ii * n"
  6.2080 +                          contour_integral p (\<lambda>w. 1/(w - z)) = 2 * pi * ii * n"
  6.2081     shows "winding_number \<gamma> z = n"
  6.2082  proof -
  6.2083    have "path_image \<gamma> \<subseteq> UNIV - {z}"
  6.2084 @@ -3409,22 +3409,22 @@
  6.2085        and pi_eq: "\<And>h1 h2 f. \<lbrakk>valid_path h1; valid_path h2;
  6.2086                      (\<forall>t\<in>{0..1}. cmod (h1 t - \<gamma> t) < e \<and> cmod (h2 t - \<gamma> t) < e);
  6.2087                      pathstart h2 = pathstart h1; pathfinish h2 = pathfinish h1; f holomorphic_on UNIV - {z}\<rbrakk> \<Longrightarrow>
  6.2088 -                    path_integral h2 f = path_integral h1 f"
  6.2089 -    using path_integral_nearby_ends [of "UNIV - {z}" \<gamma>] assms  by (auto simp: open_delete)
  6.2090 +                    contour_integral h2 f = contour_integral h1 f"
  6.2091 +    using contour_integral_nearby_ends [of "UNIV - {z}" \<gamma>] assms  by (auto simp: open_delete)
  6.2092    obtain p where p:
  6.2093       "valid_path p \<and> z \<notin> path_image p \<and>
  6.2094        pathstart p = pathstart \<gamma> \<and> pathfinish p = pathfinish \<gamma> \<and>
  6.2095        (\<forall>t \<in> {0..1}. norm (\<gamma> t - p t) < e) \<and>
  6.2096 -      path_integral p (\<lambda>w. 1/(w - z)) = 2 * pi * ii * n"
  6.2097 +      contour_integral p (\<lambda>w. 1/(w - z)) = 2 * pi * ii * n"
  6.2098      using pi [OF e] by blast
  6.2099    obtain q where q:
  6.2100       "valid_path q \<and> z \<notin> path_image q \<and>
  6.2101        pathstart q = pathstart \<gamma> \<and> pathfinish q = pathfinish \<gamma> \<and>
  6.2102 -      (\<forall>t\<in>{0..1}. cmod (\<gamma> t - q t) < e) \<and> path_integral q (\<lambda>w. 1 / (w - z)) = complex_of_real (2 * pi) * \<i> * winding_number \<gamma> z"
  6.2103 +      (\<forall>t\<in>{0..1}. cmod (\<gamma> t - q t) < e) \<and> contour_integral q (\<lambda>w. 1 / (w - z)) = complex_of_real (2 * pi) * \<i> * winding_number \<gamma> z"
  6.2104      using winding_number [OF \<gamma> e] by blast
  6.2105 -  have "2 * complex_of_real pi * \<i> * n = path_integral p (\<lambda>w. 1 / (w - z))"
  6.2106 +  have "2 * complex_of_real pi * \<i> * n = contour_integral p (\<lambda>w. 1 / (w - z))"
  6.2107      using p by auto
  6.2108 -  also have "... = path_integral q (\<lambda>w. 1 / (w - z))"
  6.2109 +  also have "... = contour_integral q (\<lambda>w. 1 / (w - z))"
  6.2110      apply (rule pi_eq)
  6.2111      using p q
  6.2112      by (auto simp: valid_path_polynomial_function norm_minus_commute intro!: holomorphic_intros)
  6.2113 @@ -3442,7 +3442,7 @@
  6.2114          "\<And>e. e>0 \<Longrightarrow> \<exists>p. valid_path p \<and> z \<notin> path_image p \<and>
  6.2115                             pathfinish p = pathstart p \<and>
  6.2116                             (\<forall>t \<in> {0..1}. norm (\<gamma> t - p t) < e) \<and>
  6.2117 -                           path_integral p (\<lambda>w. 1/(w - z)) = 2 * pi * ii * n"
  6.2118 +                           contour_integral p (\<lambda>w. 1/(w - z)) = 2 * pi * ii * n"
  6.2119     shows "winding_number \<gamma> z = n"
  6.2120  proof -
  6.2121    have "path_image \<gamma> \<subseteq> UNIV - {z}"
  6.2122 @@ -3452,22 +3452,22 @@
  6.2123        and pi_eq: "\<And>h1 h2 f. \<lbrakk>valid_path h1; valid_path h2;
  6.2124                      (\<forall>t\<in>{0..1}. cmod (h1 t - \<gamma> t) < e \<and> cmod (h2 t - \<gamma> t) < e);
  6.2125                      pathfinish h1 = pathstart h1; pathfinish h2 = pathstart h2; f holomorphic_on UNIV - {z}\<rbrakk> \<Longrightarrow>
  6.2126 -                    path_integral h2 f = path_integral h1 f"
  6.2127 -    using path_integral_nearby_loops [of "UNIV - {z}" \<gamma>] assms  by (auto simp: open_delete)
  6.2128 +                    contour_integral h2 f = contour_integral h1 f"
  6.2129 +    using contour_integral_nearby_loops [of "UNIV - {z}" \<gamma>] assms  by (auto simp: open_delete)
  6.2130    obtain p where p:
  6.2131       "valid_path p \<and> z \<notin> path_image p \<and>
  6.2132        pathfinish p = pathstart p \<and>
  6.2133        (\<forall>t \<in> {0..1}. norm (\<gamma> t - p t) < e) \<and>
  6.2134 -      path_integral p (\<lambda>w. 1/(w - z)) = 2 * pi * ii * n"
  6.2135 +      contour_integral p (\<lambda>w. 1/(w - z)) = 2 * pi * ii * n"
  6.2136      using pi [OF e] by blast
  6.2137    obtain q where q:
  6.2138       "valid_path q \<and> z \<notin> path_image q \<and>
  6.2139        pathstart q = pathstart \<gamma> \<and> pathfinish q = pathfinish \<gamma> \<and>
  6.2140 -      (\<forall>t\<in>{0..1}. cmod (\<gamma> t - q t) < e) \<and> path_integral q (\<lambda>w. 1 / (w - z)) = complex_of_real (2 * pi) * \<i> * winding_number \<gamma> z"
  6.2141 +      (\<forall>t\<in>{0..1}. cmod (\<gamma> t - q t) < e) \<and> contour_integral q (\<lambda>w. 1 / (w - z)) = complex_of_real (2 * pi) * \<i> * winding_number \<gamma> z"
  6.2142      using winding_number [OF \<gamma> e] by blast
  6.2143 -  have "2 * complex_of_real pi * \<i> * n = path_integral p (\<lambda>w. 1 / (w - z))"
  6.2144 +  have "2 * complex_of_real pi * \<i> * n = contour_integral p (\<lambda>w. 1 / (w - z))"
  6.2145      using p by auto
  6.2146 -  also have "... = path_integral q (\<lambda>w. 1 / (w - z))"
  6.2147 +  also have "... = contour_integral q (\<lambda>w. 1 / (w - z))"
  6.2148      apply (rule pi_eq)
  6.2149      using p q loop
  6.2150      by (auto simp: valid_path_polynomial_function norm_minus_commute intro!: holomorphic_intros)
  6.2151 @@ -3480,13 +3480,13 @@
  6.2152  
  6.2153  lemma winding_number_valid_path:
  6.2154    assumes "valid_path \<gamma>" "z \<notin> path_image \<gamma>"
  6.2155 -    shows "winding_number \<gamma> z = 1/(2*pi*ii) * path_integral \<gamma> (\<lambda>w. 1/(w - z))"
  6.2156 +    shows "winding_number \<gamma> z = 1/(2*pi*ii) * contour_integral \<gamma> (\<lambda>w. 1/(w - z))"
  6.2157    using assms by (auto simp: valid_path_imp_path intro!: winding_number_unique)
  6.2158  
  6.2159 -lemma has_path_integral_winding_number:
  6.2160 +lemma has_contour_integral_winding_number:
  6.2161    assumes \<gamma>: "valid_path \<gamma>" "z \<notin> path_image \<gamma>"
  6.2162 -    shows "((\<lambda>w. 1/(w - z)) has_path_integral (2*pi*ii*winding_number \<gamma> z)) \<gamma>"
  6.2163 -by (simp add: winding_number_valid_path has_path_integral_integral path_integrable_inversediff assms)
  6.2164 +    shows "((\<lambda>w. 1/(w - z)) has_contour_integral (2*pi*ii*winding_number \<gamma> z)) \<gamma>"
  6.2165 +by (simp add: winding_number_valid_path has_contour_integral_integral contour_integrable_inversediff assms)
  6.2166  
  6.2167  lemma winding_number_trivial [simp]: "z \<noteq> a \<Longrightarrow> winding_number(linepath a a) z = 0"
  6.2168    by (simp add: winding_number_valid_path)
  6.2169 @@ -3505,7 +3505,7 @@
  6.2170    apply (frule winding_number [OF g1], clarify)
  6.2171    apply (rename_tac p2 p1)
  6.2172    apply (rule_tac x="p1+++p2" in exI)
  6.2173 -  apply (simp add: not_in_path_image_join path_integrable_inversediff algebra_simps)
  6.2174 +  apply (simp add: not_in_path_image_join contour_integrable_inversediff algebra_simps)
  6.2175    apply (auto simp: joinpaths_def)
  6.2176    done
  6.2177  
  6.2178 @@ -3517,7 +3517,7 @@
  6.2179    apply simp_all
  6.2180    apply (frule winding_number [OF assms], clarify)
  6.2181    apply (rule_tac x="reversepath p" in exI)
  6.2182 -  apply (simp add: path_integral_reversepath path_integrable_inversediff valid_path_imp_reverse)
  6.2183 +  apply (simp add: contour_integral_reversepath contour_integrable_inversediff valid_path_imp_reverse)
  6.2184    apply (auto simp: reversepath_def)
  6.2185    done
  6.2186  
  6.2187 @@ -3530,7 +3530,7 @@
  6.2188    apply (simp_all add: path_shiftpath path_image_shiftpath pathfinish_shiftpath pathstart_shiftpath)
  6.2189    apply (frule winding_number [OF \<gamma>], clarify)
  6.2190    apply (rule_tac x="shiftpath a p" in exI)
  6.2191 -  apply (simp add: path_integral_shiftpath path_image_shiftpath pathfinish_shiftpath pathstart_shiftpath valid_path_shiftpath)
  6.2192 +  apply (simp add: contour_integral_shiftpath path_image_shiftpath pathfinish_shiftpath pathstart_shiftpath valid_path_shiftpath)
  6.2193    apply (auto simp: shiftpath_def)
  6.2194    done
  6.2195  
  6.2196 @@ -3543,7 +3543,7 @@
  6.2197      using assms  by (meson convex_contains_segment convex_segment ends_in_segment(2) subsetCE)
  6.2198    then show ?thesis
  6.2199      using assms
  6.2200 -    by (simp add: winding_number_valid_path path_integral_split_linepath [symmetric] continuous_on_inversediff field_simps)
  6.2201 +    by (simp add: winding_number_valid_path contour_integral_split_linepath [symmetric] continuous_on_inversediff field_simps)
  6.2202  qed
  6.2203  
  6.2204  lemma winding_number_cong:
  6.2205 @@ -3551,7 +3551,7 @@
  6.2206    by (simp add: winding_number_def pathstart_def pathfinish_def)
  6.2207  
  6.2208  lemma winding_number_offset: "winding_number p z = winding_number (\<lambda>w. p w - z) 0"
  6.2209 -  apply (simp add: winding_number_def path_integral_integral path_image_def valid_path_def pathstart_def pathfinish_def)
  6.2210 +  apply (simp add: winding_number_def contour_integral_integral path_image_def valid_path_def pathstart_def pathfinish_def)
  6.2211    apply (intro ext arg_cong [where f = Eps] arg_cong [where f = All] imp_cong refl, safe)
  6.2212    apply (rename_tac g)
  6.2213    apply (rule_tac x="\<lambda>t. g t - z" in exI)
  6.2214 @@ -3574,7 +3574,7 @@
  6.2215  
  6.2216  lemma Re_winding_number:
  6.2217      "\<lbrakk>valid_path \<gamma>; z \<notin> path_image \<gamma>\<rbrakk>
  6.2218 -     \<Longrightarrow> Re(winding_number \<gamma> z) = Im(path_integral \<gamma> (\<lambda>w. 1/(w - z))) / (2*pi)"
  6.2219 +     \<Longrightarrow> Re(winding_number \<gamma> z) = Im(contour_integral \<gamma> (\<lambda>w. 1/(w - z))) / (2*pi)"
  6.2220  by (simp add: winding_number_valid_path field_simps Re_divide power2_eq_square)
  6.2221  
  6.2222  lemma winding_number_pos_le:
  6.2223 @@ -3594,9 +3594,9 @@
  6.2224      apply (rule has_integral_spike_interior [of 0 1 _ "\<lambda>x. 1/(\<gamma> x - z) * vector_derivative \<gamma> (at x)"])
  6.2225      apply simp
  6.2226      apply (simp only: box_real)
  6.2227 -    apply (subst has_path_integral [symmetric])
  6.2228 +    apply (subst has_contour_integral [symmetric])
  6.2229      using \<gamma>
  6.2230 -    apply (simp add: path_integrable_inversediff has_path_integral_integral)
  6.2231 +    apply (simp add: contour_integrable_inversediff has_contour_integral_integral)
  6.2232      done
  6.2233  qed
  6.2234  
  6.2235 @@ -3606,19 +3606,19 @@
  6.2236        and ge: "\<And>x. \<lbrakk>0 < x; x < 1\<rbrakk> \<Longrightarrow> e \<le> Im (vector_derivative \<gamma> (at x) / (\<gamma> x - z))"
  6.2237      shows "0 < Re(winding_number \<gamma> z)"
  6.2238  proof -
  6.2239 -  have "e \<le> Im (path_integral \<gamma> (\<lambda>w. 1 / (w - z)))"
  6.2240 +  have "e \<le> Im (contour_integral \<gamma> (\<lambda>w. 1 / (w - z)))"
  6.2241      apply (rule has_integral_component_le
  6.2242               [of ii "\<lambda>x. ii*e" "ii*e" "{0..1}"
  6.2243                      "\<lambda>x. if x \<in> {0<..<1} then 1/(\<gamma> x - z) * vector_derivative \<gamma> (at x) else ii*e"
  6.2244 -                    "path_integral \<gamma> (\<lambda>w. 1/(w - z))", simplified])
  6.2245 +                    "contour_integral \<gamma> (\<lambda>w. 1/(w - z))", simplified])
  6.2246      using e
  6.2247      apply (simp_all add: Basis_complex_def)
  6.2248      using has_integral_const_real [of _ 0 1] apply force
  6.2249      apply (rule has_integral_spike_interior [of 0 1 _ "\<lambda>x. 1/(\<gamma> x - z) * vector_derivative \<gamma> (at x)", simplified box_real])
  6.2250      apply simp
  6.2251 -    apply (subst has_path_integral [symmetric])
  6.2252 +    apply (subst has_contour_integral [symmetric])
  6.2253      using \<gamma>
  6.2254 -    apply (simp_all add: path_integrable_inversediff has_path_integral_integral ge)
  6.2255 +    apply (simp_all add: contour_integrable_inversediff has_contour_integral_integral ge)
  6.2256      done
  6.2257    with e show ?thesis
  6.2258      by (simp add: Re_winding_number [OF \<gamma>] field_simps)
  6.2259 @@ -3711,7 +3711,7 @@
  6.2260      by meson
  6.2261    have exy: "\<exists>y. ((\<lambda>x. inverse (\<gamma> x - z) * ?D\<gamma> x) has_integral y) {a..b}"
  6.2262      unfolding integrable_on_def [symmetric]
  6.2263 -    apply (rule path_integral_local_primitive_any [OF piecewise_C1_imp_differentiable [OF \<gamma>], of "-{z}"])
  6.2264 +    apply (rule contour_integral_local_primitive_any [OF piecewise_C1_imp_differentiable [OF \<gamma>], of "-{z}"])
  6.2265      apply (rename_tac w)
  6.2266      apply (rule_tac x="norm(w - z)" in exI)
  6.2267      apply (simp_all add: inverse_eq_divide)
  6.2268 @@ -3766,7 +3766,7 @@
  6.2269      "\<lbrakk>path p; z \<notin> path_image p\<rbrakk>
  6.2270       \<Longrightarrow> pathfinish p - z = exp (2 * pi * ii * winding_number p z) * (pathstart p - z)"
  6.2271  using winding_number [of p z 1] unfolding valid_path_def path_image_def pathstart_def pathfinish_def
  6.2272 -  by (force dest: winding_number_exp_integral(2) [of _ 0 1 z] simp: field_simps path_integral_integral exp_minus)
  6.2273 +  by (force dest: winding_number_exp_integral(2) [of _ 0 1 z] simp: field_simps contour_integral_integral exp_minus)
  6.2274  
  6.2275  
  6.2276  subsection\<open>The version with complex integers and equality\<close>
  6.2277 @@ -3779,15 +3779,15 @@
  6.2278        by (simp add: field_simps) algebra
  6.2279    obtain p where p: "valid_path p" "z \<notin> path_image p"
  6.2280                      "pathstart p = pathstart \<gamma>" "pathfinish p = pathfinish \<gamma>"
  6.2281 -                    "path_integral p (\<lambda>w. 1 / (w - z)) = complex_of_real (2 * pi) * \<i> * winding_number \<gamma> z"
  6.2282 +                    "contour_integral p (\<lambda>w. 1 / (w - z)) = complex_of_real (2 * pi) * \<i> * winding_number \<gamma> z"
  6.2283      using winding_number [OF assms, of 1] by auto
  6.2284 -  have [simp]: "(winding_number \<gamma> z \<in> \<int>) = (Exp (path_integral p (\<lambda>w. 1 / (w - z))) = 1)"
  6.2285 +  have [simp]: "(winding_number \<gamma> z \<in> \<int>) = (Exp (contour_integral p (\<lambda>w. 1 / (w - z))) = 1)"
  6.2286        using p by (simp add: exp_eq_1 complex_is_Int_iff)
  6.2287    have "winding_number p z \<in> \<int> \<longleftrightarrow> pathfinish p = pathstart p"
  6.2288      using p z
  6.2289      apply (simp add: winding_number_valid_path valid_path_def path_image_def pathstart_def pathfinish_def)
  6.2290      using winding_number_exp_integral(2) [of p 0 1 z]
  6.2291 -    apply (simp add: field_simps path_integral_integral exp_minus)
  6.2292 +    apply (simp add: field_simps contour_integral_integral exp_minus)
  6.2293      apply (rule *)
  6.2294      apply (auto simp: path_image_def field_simps)
  6.2295      done
  6.2296 @@ -3822,7 +3822,7 @@
  6.2297      by (simp add: Arg less_eq_real_def)
  6.2298    also have "... \<le> Im (integral {0..1} (\<lambda>x. vector_derivative \<gamma> (at x) / (\<gamma> x - z)))"
  6.2299      using 1
  6.2300 -    apply (simp add: winding_number_valid_path [OF \<gamma> z] Cauchy_Integral_Thm.path_integral_integral)
  6.2301 +    apply (simp add: winding_number_valid_path [OF \<gamma> z] Cauchy_Integral_Thm.contour_integral_integral)
  6.2302      apply (simp add: Complex.Re_divide field_simps power2_eq_square)
  6.2303      done
  6.2304    finally have "Arg r \<le> Im (integral {0..1} (\<lambda>x. vector_derivative \<gamma> (at x) / (\<gamma> x - z)))" .
  6.2305 @@ -3927,12 +3927,12 @@
  6.2306               \<Longrightarrow>
  6.2307                 path_image h1 \<subseteq> - cball z (e / 2) \<and>
  6.2308                 path_image h2 \<subseteq> - cball z (e / 2) \<and>
  6.2309 -               (\<forall>f. f holomorphic_on - cball z (e / 2) \<longrightarrow> path_integral h2 f = path_integral h1 f)"
  6.2310 -    using path_integral_nearby_ends [OF oc \<gamma> ppag] by metis
  6.2311 +               (\<forall>f. f holomorphic_on - cball z (e / 2) \<longrightarrow> contour_integral h2 f = contour_integral h1 f)"
  6.2312 +    using contour_integral_nearby_ends [OF oc \<gamma> ppag] by metis
  6.2313    obtain p where p: "valid_path p" "z \<notin> path_image p"
  6.2314                      "pathstart p = pathstart \<gamma> \<and> pathfinish p = pathfinish \<gamma>"
  6.2315                and pg: "\<And>t. t\<in>{0..1} \<Longrightarrow> cmod (\<gamma> t - p t) < min d e / 2"
  6.2316 -              and pi: "path_integral p (\<lambda>x. 1 / (x - z)) = complex_of_real (2 * pi) * \<i> * winding_number \<gamma> z"
  6.2317 +              and pi: "contour_integral p (\<lambda>x. 1 / (x - z)) = complex_of_real (2 * pi) * \<i> * winding_number \<gamma> z"
  6.2318      using winding_number [OF \<gamma> z, of "min d e / 2"] `d>0` `e>0` by auto
  6.2319    { fix w
  6.2320      assume d2: "cmod (w - z) < d/2" and e2: "cmod (w - z) < e/2"
  6.2321 @@ -3950,17 +3950,17 @@
  6.2322        then obtain q where q: "valid_path q" "w \<notin> path_image q"
  6.2323                               "pathstart q = pathstart \<gamma> \<and> pathfinish q = pathfinish \<gamma>"
  6.2324                      and qg: "\<And>t. t \<in> {0..1} \<Longrightarrow> cmod (\<gamma> t - q t) < min k (min d e) / 2"
  6.2325 -                    and qi: "path_integral q (\<lambda>u. 1 / (u - w)) = complex_of_real (2 * pi) * \<i> * winding_number \<gamma> w"
  6.2326 +                    and qi: "contour_integral q (\<lambda>u. 1 / (u - w)) = complex_of_real (2 * pi) * \<i> * winding_number \<gamma> w"
  6.2327          using winding_number [OF \<gamma> wnotg, of "min k (min d e) / 2"] `d>0` `e>0` k
  6.2328          by (force simp: min_divide_distrib_right)
  6.2329 -      have "path_integral p (\<lambda>u. 1 / (u - w)) = path_integral q (\<lambda>u. 1 / (u - w))"
  6.2330 +      have "contour_integral p (\<lambda>u. 1 / (u - w)) = contour_integral q (\<lambda>u. 1 / (u - w))"
  6.2331          apply (rule pi_eq [OF `valid_path q` `valid_path p`, THEN conjunct2, THEN conjunct2, rule_format])
  6.2332          apply (frule pg)
  6.2333          apply (frule qg)
  6.2334          using p q `d>0` e2
  6.2335          apply (auto simp: dist_norm norm_minus_commute intro!: holomorphic_intros)
  6.2336          done
  6.2337 -      then have "path_integral p (\<lambda>x. 1 / (x - w)) = complex_of_real (2 * pi) * \<i> * winding_number \<gamma> w"
  6.2338 +      then have "contour_integral p (\<lambda>x. 1 / (x - w)) = complex_of_real (2 * pi) * \<i> * winding_number \<gamma> w"
  6.2339          by (simp add: pi qi)
  6.2340      } note pip = this
  6.2341      have "path p"
  6.2342 @@ -3978,16 +3978,16 @@
  6.2343      where "L>0"
  6.2344        and L: "\<And>f B. \<lbrakk>f holomorphic_on - cball z (3 / 4 * pe);
  6.2345                        \<forall>z \<in> - cball z (3 / 4 * pe). cmod (f z) \<le> B\<rbrakk> \<Longrightarrow>
  6.2346 -                      cmod (path_integral p f) \<le> L * B"
  6.2347 -    using path_integral_bound_exists [of "- cball z (3/4*pe)" p] cbp `valid_path p` by force
  6.2348 +                      cmod (contour_integral p f) \<le> L * B"
  6.2349 +    using contour_integral_bound_exists [of "- cball z (3/4*pe)" p] cbp `valid_path p` by force
  6.2350    { fix e::real and w::complex
  6.2351      assume e: "0 < e" and w: "cmod (w - z) < pe/4" "cmod (w - z) < e * pe\<^sup>2 / (8 * L)"
  6.2352      then have [simp]: "w \<notin> path_image p"
  6.2353        using cbp p(2) `0 < pe`
  6.2354        by (force simp: dist_norm norm_minus_commute path_image_def cball_def)
  6.2355 -    have [simp]: "path_integral p (\<lambda>x. 1/(x - w)) - path_integral p (\<lambda>x. 1/(x - z)) =
  6.2356 -                  path_integral p (\<lambda>x. 1/(x - w) - 1/(x - z))"
  6.2357 -      by (simp add: p path_integrable_inversediff path_integral_diff)
  6.2358 +    have [simp]: "contour_integral p (\<lambda>x. 1/(x - w)) - contour_integral p (\<lambda>x. 1/(x - z)) =
  6.2359 +                  contour_integral p (\<lambda>x. 1/(x - w) - 1/(x - z))"
  6.2360 +      by (simp add: p contour_integrable_inversediff contour_integral_diff)
  6.2361      { fix x
  6.2362        assume pe: "3/4 * pe < cmod (z - x)"
  6.2363        have "cmod (w - x) < pe/4 + cmod (z - x)"
  6.2364 @@ -4025,14 +4025,14 @@
  6.2365          apply (auto simp: divide_simps mult_less_0_iff norm_minus_commute norm_divide norm_mult power2_eq_square)
  6.2366          done
  6.2367      } note L_cmod_le = this
  6.2368 -    have *: "cmod (path_integral p (\<lambda>x. 1 / (x - w) - 1 / (x - z))) \<le> L * (e * pe\<^sup>2 / L / 4 * (inverse (pe / 2))\<^sup>2)"
  6.2369 +    have *: "cmod (contour_integral p (\<lambda>x. 1 / (x - w) - 1 / (x - z))) \<le> L * (e * pe\<^sup>2 / L / 4 * (inverse (pe / 2))\<^sup>2)"
  6.2370        apply (rule L)
  6.2371        using `pe>0` w
  6.2372        apply (force simp: dist_norm norm_minus_commute intro!: holomorphic_intros)
  6.2373        using `pe>0` w `L>0`
  6.2374        apply (auto simp: cball_def dist_norm field_simps L_cmod_le  simp del: less_divide_eq_numeral1 le_divide_eq_numeral1)
  6.2375        done
  6.2376 -    have "cmod (path_integral p (\<lambda>x. 1 / (x - w)) - path_integral p (\<lambda>x. 1 / (x - z))) < 2*e"
  6.2377 +    have "cmod (contour_integral p (\<lambda>x. 1 / (x - w)) - contour_integral p (\<lambda>x. 1 / (x - z))) < 2*e"
  6.2378        apply (simp add:)
  6.2379        apply (rule le_less_trans [OF *])
  6.2380        using `L>0` e
  6.2381 @@ -4142,12 +4142,12 @@
  6.2382        then have "w \<notin> path_image p"  using w by blast
  6.2383        then have "\<exists>p. valid_path p \<and> w \<notin> path_image p \<and>
  6.2384                       pathstart p = pathstart \<gamma> \<and> pathfinish p = pathfinish \<gamma> \<and>
  6.2385 -                     (\<forall>t\<in>{0..1}. cmod (\<gamma> t - p t) < e) \<and> path_integral p (\<lambda>wa. 1 / (wa - w)) = 0"
  6.2386 +                     (\<forall>t\<in>{0..1}. cmod (\<gamma> t - p t) < e) \<and> contour_integral p (\<lambda>wa. 1 / (wa - w)) = 0"
  6.2387          apply (rule_tac x=p in exI)
  6.2388          apply (simp add: p valid_path_polynomial_function)
  6.2389          apply (intro conjI)
  6.2390          using pge apply (simp add: norm_minus_commute)
  6.2391 -        apply (rule path_integral_unique [OF Cauchy_theorem_convex_simple [OF _ convex_ball [of 0 "B+1"]]])
  6.2392 +        apply (rule contour_integral_unique [OF Cauchy_theorem_convex_simple [OF _ convex_ball [of 0 "B+1"]]])
  6.2393          apply (rule holomorphic_intros | simp add: dist_norm)+
  6.2394          using mem_ball_0 w apply blast
  6.2395          using p apply (simp_all add: valid_path_polynomial_function loop pip)
  6.2396 @@ -4218,9 +4218,9 @@
  6.2397           if x: "0 \<le> x" "x \<le> 1" for x
  6.2398    proof -
  6.2399      have "integral {0..x} (\<lambda>t. vector_derivative \<gamma> (at t) / (\<gamma> t - z)) / (2 * of_real pi * \<i>) =
  6.2400 -          1 / (2*pi*ii) * path_integral (subpath 0 x \<gamma>) (\<lambda>w. 1/(w - z))"
  6.2401 +          1 / (2*pi*ii) * contour_integral (subpath 0 x \<gamma>) (\<lambda>w. 1/(w - z))"
  6.2402        using assms x
  6.2403 -      apply (simp add: path_integral_subpath_integral [OF path_integrable_inversediff])
  6.2404 +      apply (simp add: contour_integral_subcontour_integral [OF contour_integrable_inversediff])
  6.2405        done
  6.2406      also have "... = winding_number (subpath 0 x \<gamma>) z"
  6.2407        apply (subst winding_number_valid_path)
  6.2408 @@ -4235,7 +4235,7 @@
  6.2409                                   integral {0..x} (\<lambda>t. 1/(\<gamma> t - z) * vector_derivative \<gamma> (at t))"])
  6.2410      apply (rule continuous_intros)+
  6.2411      apply (rule indefinite_integral_continuous)
  6.2412 -    apply (rule path_integrable_inversediff [OF assms, unfolded path_integrable_on])
  6.2413 +    apply (rule contour_integrable_inversediff [OF assms, unfolded contour_integrable_on])
  6.2414        using assms
  6.2415      apply (simp add: *)
  6.2416      done
  6.2417 @@ -4379,7 +4379,7 @@
  6.2418          and fcd: "(\<And>x. x \<in> interior s - k \<Longrightarrow> f complex_differentiable at x)"
  6.2419          and z: "z \<in> interior s - k" and vpg: "valid_path \<gamma>"
  6.2420          and pasz: "path_image \<gamma> \<subseteq> s - {z}" and loop: "pathfinish \<gamma> = pathstart \<gamma>"
  6.2421 -      shows "((\<lambda>w. f w / (w - z)) has_path_integral (2*pi * ii * winding_number \<gamma> z * f z)) \<gamma>"
  6.2422 +      shows "((\<lambda>w. f w / (w - z)) has_contour_integral (2*pi * ii * winding_number \<gamma> z * f z)) \<gamma>"
  6.2423  proof -
  6.2424    obtain f' where f': "(f has_field_derivative f') (at z)"
  6.2425      using fcd [OF z] by (auto simp: complex_differentiable_def)
  6.2426 @@ -4404,7 +4404,7 @@
  6.2427        using False by auto
  6.2428    qed
  6.2429    have fink': "finite (insert z k)" using \<open>finite k\<close> by blast
  6.2430 -  have *: "((\<lambda>w. if w = z then f' else (f w - f z) / (w - z)) has_path_integral 0) \<gamma>"
  6.2431 +  have *: "((\<lambda>w. if w = z then f' else (f w - f z) / (w - z)) has_contour_integral 0) \<gamma>"
  6.2432      apply (rule Cauchy_theorem_convex [OF _ s fink' _ vpg pas loop])
  6.2433      using c apply (force simp: continuous_on_eq_continuous_within)
  6.2434      apply (rename_tac w)
  6.2435 @@ -4414,8 +4414,8 @@
  6.2436      apply (rule derivative_intros fcd | simp)+
  6.2437      done
  6.2438    show ?thesis
  6.2439 -    apply (rule has_path_integral_eq)
  6.2440 -    using znotin has_path_integral_add [OF has_path_integral_lmul [OF has_path_integral_winding_number [OF vpg znotin], of "f z"] *]
  6.2441 +    apply (rule has_contour_integral_eq)
  6.2442 +    using znotin has_contour_integral_add [OF has_contour_integral_lmul [OF has_contour_integral_winding_number [OF vpg znotin], of "f z"] *]
  6.2443      apply (auto simp: mult_ac divide_simps)
  6.2444      done
  6.2445  qed
  6.2446 @@ -4423,9 +4423,309 @@
  6.2447  theorem Cauchy_integral_formula_convex_simple:
  6.2448      "\<lbrakk>convex s; f holomorphic_on s; z \<in> interior s; valid_path \<gamma>; path_image \<gamma> \<subseteq> s - {z};
  6.2449        pathfinish \<gamma> = pathstart \<gamma>\<rbrakk>
  6.2450 -     \<Longrightarrow> ((\<lambda>w. f w / (w - z)) has_path_integral (2*pi * ii * winding_number \<gamma> z * f z)) \<gamma>"
  6.2451 +     \<Longrightarrow> ((\<lambda>w. f w / (w - z)) has_contour_integral (2*pi * ii * winding_number \<gamma> z * f z)) \<gamma>"
  6.2452    apply (rule Cauchy_integral_formula_weak [where k = "{}"])
  6.2453    using holomorphic_on_imp_continuous_on
  6.2454    by auto (metis at_within_interior holomorphic_on_def interiorE subsetCE)
  6.2455  
  6.2456 +
  6.2457 +subsection\<open>Homotopy forms of Cauchy's theorem\<close>
  6.2458 +
  6.2459 +proposition Cauchy_theorem_homotopic:
  6.2460 +    assumes hom: "if atends then homotopic_paths s g h else homotopic_loops s g h"
  6.2461 +        and "open s" and f: "f holomorphic_on s"
  6.2462 +        and vpg: "valid_path g" and vph: "valid_path h"
  6.2463 +    shows "contour_integral g f = contour_integral h f"
  6.2464 +proof -
  6.2465 +  have pathsf: "linked_paths atends g h"
  6.2466 +    using hom  by (auto simp: linked_paths_def homotopic_paths_imp_pathstart homotopic_paths_imp_pathfinish homotopic_loops_imp_loop)
  6.2467 +  obtain k :: "real \<times> real \<Rightarrow> complex"
  6.2468 +    where contk: "continuous_on ({0..1} \<times> {0..1}) k"
  6.2469 +      and ks: "k ` ({0..1} \<times> {0..1}) \<subseteq> s"
  6.2470 +      and k [simp]: "\<forall>x. k (0, x) = g x" "\<forall>x. k (1, x) = h x"
  6.2471 +      and ksf: "\<forall>t\<in>{0..1}. linked_paths atends g (\<lambda>x. k (t, x))"
  6.2472 +      using hom pathsf by (auto simp: linked_paths_def homotopic_paths_def homotopic_loops_def homotopic_with_def split: split_if_asm)
  6.2473 +  have ucontk: "uniformly_continuous_on ({0..1} \<times> {0..1}) k"
  6.2474 +    by (blast intro: compact_Times compact_uniformly_continuous [OF contk])
  6.2475 +  { fix t::real assume t: "t \<in> {0..1}"
  6.2476 +    have pak: "path (k o (\<lambda>u. (t, u)))"
  6.2477 +      unfolding path_def
  6.2478 +      apply (rule continuous_intros continuous_on_subset [OF contk])+
  6.2479 +      using t by force
  6.2480 +    have pik: "path_image (k \<circ> Pair t) \<subseteq> s"
  6.2481 +      using ks t by (auto simp: path_image_def)
  6.2482 +    obtain e where "e>0" and e:
  6.2483 +         "\<And>g h. \<lbrakk>valid_path g; valid_path h;
  6.2484 +                  \<forall>u\<in>{0..1}. cmod (g u - (k \<circ> Pair t) u) < e \<and> cmod (h u - (k \<circ> Pair t) u) < e;
  6.2485 +                  linked_paths atends g h\<rbrakk>
  6.2486 +                 \<Longrightarrow> contour_integral h f = contour_integral g f"
  6.2487 +      using contour_integral_nearby [OF \<open>open s\<close> pak pik, of atends] f by metis
  6.2488 +    obtain d where "d>0" and d:
  6.2489 +        "\<And>x x'. \<lbrakk>x \<in> {0..1} \<times> {0..1}; x' \<in> {0..1} \<times> {0..1}; norm (x'-x) < d\<rbrakk> \<Longrightarrow> norm (k x' - k x) < e/4"
  6.2490 +      by (rule uniformly_continuous_onE [OF ucontk, of "e/4"]) (auto simp: dist_norm `e>0`)
  6.2491 +    { fix t1 t2
  6.2492 +      assume t1: "0 \<le> t1" "t1 \<le> 1" and t2: "0 \<le> t2" "t2 \<le> 1" and ltd: "\<bar>t1 - t\<bar> < d" "\<bar>t2 - t\<bar> < d"
  6.2493 +      have no2: "\<And>g1 k1 kt. \<lbrakk>norm(g1 - k1) < e/4; norm(k1 - kt) < e/4\<rbrakk> \<Longrightarrow> norm(g1 - kt) < e"
  6.2494 +        using \<open>e > 0\<close>
  6.2495 +        apply (rule_tac y = k1 in norm_triangle_half_l)
  6.2496 +        apply (auto simp: norm_minus_commute intro: order_less_trans)
  6.2497 +        done
  6.2498 +      have "\<exists>d>0. \<forall>g1 g2. valid_path g1 \<and> valid_path g2 \<and>
  6.2499 +                          (\<forall>u\<in>{0..1}. cmod (g1 u - k (t1, u)) < d \<and> cmod (g2 u - k (t2, u)) < d) \<and>
  6.2500 +                          linked_paths atends g1 g2 \<longrightarrow>
  6.2501 +                          contour_integral g2 f = contour_integral g1 f"
  6.2502 +        apply (rule_tac x="e/4" in exI)
  6.2503 +        using t t1 t2 ltd \<open>e > 0\<close>
  6.2504 +        apply (auto intro!: e simp: d no2 simp del: less_divide_eq_numeral1)
  6.2505 +        done
  6.2506 +    }
  6.2507 +    then have "\<exists>e. 0 < e \<and>
  6.2508 +              (\<forall>t1 t2. t1 \<in> {0..1} \<and> t2 \<in> {0..1} \<and> abs(t1 - t) < e \<and> abs(t2 - t) < e
  6.2509 +                \<longrightarrow> (\<exists>d. 0 < d \<and>
  6.2510 +                     (\<forall>g1 g2. valid_path g1 \<and> valid_path g2 \<and>
  6.2511 +                       (\<forall>u \<in> {0..1}.
  6.2512 +                          norm(g1 u - k((t1,u))) < d \<and> norm(g2 u - k((t2,u))) < d) \<and>
  6.2513 +                          linked_paths atends g1 g2
  6.2514 +                          \<longrightarrow> contour_integral g2 f = contour_integral g1 f)))"
  6.2515 +      by (rule_tac x=d in exI) (simp add: \<open>d > 0\<close>)
  6.2516 +  }
  6.2517 +  then obtain ee where ee:
  6.2518 +       "\<And>t. t \<in> {0..1} \<Longrightarrow> ee t > 0 \<and>
  6.2519 +          (\<forall>t1 t2. t1 \<in> {0..1} \<longrightarrow> t2 \<in> {0..1} \<longrightarrow> abs(t1 - t) < ee t \<longrightarrow> abs(t2 - t) < ee t
  6.2520 +            \<longrightarrow> (\<exists>d. 0 < d \<and>
  6.2521 +                 (\<forall>g1 g2. valid_path g1 \<and> valid_path g2 \<and>
  6.2522 +                   (\<forall>u \<in> {0..1}.
  6.2523 +                      norm(g1 u - k((t1,u))) < d \<and> norm(g2 u - k((t2,u))) < d) \<and>
  6.2524 +                      linked_paths atends g1 g2
  6.2525 +                      \<longrightarrow> contour_integral g2 f = contour_integral g1 f)))"
  6.2526 +    by metis
  6.2527 +  note ee_rule = ee [THEN conjunct2, rule_format]
  6.2528 +  def C \<equiv> "(\<lambda>t. ball t (ee t / 3)) ` {0..1}"
  6.2529 +  have "\<forall>t \<in> C. open t" by (simp add: C_def)
  6.2530 +  moreover have "{0..1} \<subseteq> \<Union>C"
  6.2531 +    using ee [THEN conjunct1] by (auto simp: C_def dist_norm)
  6.2532 +  ultimately obtain C' where C': "C' \<subseteq> C" "finite C'" and C'01: "{0..1} \<subseteq> \<Union>C'"
  6.2533 +    by (rule compactE [OF compact_interval])
  6.2534 +  def kk \<equiv> "{t \<in> {0..1}. ball t (ee t / 3) \<in> C'}"
  6.2535 +  have kk01: "kk \<subseteq> {0..1}" by (auto simp: kk_def)
  6.2536 +  def e \<equiv> "Min (ee ` kk)"
  6.2537 +  have C'_eq: "C' = (\<lambda>t. ball t (ee t / 3)) ` kk"
  6.2538 +    using C' by (auto simp: kk_def C_def)
  6.2539 +  have ee_pos[simp]: "\<And>t. t \<in> {0..1} \<Longrightarrow> ee t > 0"
  6.2540 +    by (simp add: kk_def ee)
  6.2541 +  moreover have "finite kk"
  6.2542 +    using \<open>finite C'\<close> kk01 by (force simp: C'_eq inj_on_def ball_eq_ball_iff dest: ee_pos finite_imageD)
  6.2543 +  moreover have "kk \<noteq> {}" using \<open>{0..1} \<subseteq> \<Union>C'\<close> C'_eq by force
  6.2544 +  ultimately have "e > 0"
  6.2545 +    using finite_less_Inf_iff [of "ee ` kk" 0] kk01 by (force simp: e_def)
  6.2546 +  then obtain N::nat where "N > 0" and N: "1/N < e/3"
  6.2547 +    by (meson divide_pos_pos nat_approx_posE zero_less_Suc zero_less_numeral)
  6.2548 +  have e_le_ee: "\<And>i. i \<in> kk \<Longrightarrow> e \<le> ee i"
  6.2549 +    using \<open>finite kk\<close> by (simp add: e_def Min_le_iff [of "ee ` kk"])
  6.2550 +  have plus: "\<exists>t \<in> kk. x \<in> ball t (ee t / 3)" if "x \<in> {0..1}" for x
  6.2551 +    using C' subsetD [OF C'01 that]  unfolding C'_eq by blast
  6.2552 +  have [OF order_refl]:
  6.2553 +      "\<exists>d. 0 < d \<and> (\<forall>j. valid_path j \<and> (\<forall>u \<in> {0..1}. norm(j u - k (n/N, u)) < d) \<and> linked_paths atends g j
  6.2554 +                        \<longrightarrow> contour_integral j f = contour_integral g f)"
  6.2555 +       if "n \<le> N" for n
  6.2556 +  using that
  6.2557 +  proof (induct n)
  6.2558 +    case 0 show ?case using ee_rule [of 0 0 0]
  6.2559 +      apply clarsimp
  6.2560 +      apply (rule_tac x=d in exI, safe)
  6.2561 +      by (metis diff_self vpg norm_zero)
  6.2562 +  next
  6.2563 +    case (Suc n)
  6.2564 +    then have N01: "n/N \<in> {0..1}" "(Suc n)/N \<in> {0..1}"  by auto
  6.2565 +    then obtain t where t: "t \<in> kk" "n/N \<in> ball t (ee t / 3)"
  6.2566 +      using plus [of "n/N"] by blast
  6.2567 +    then have nN_less: "\<bar>n/N - t\<bar> < ee t"
  6.2568 +      by (simp add: dist_norm del: less_divide_eq_numeral1)
  6.2569 +    have n'N_less: "\<bar>real (Suc n) / real N - t\<bar> < ee t"
  6.2570 +      using t N \<open>N > 0\<close> e_le_ee [of t]
  6.2571 +      by (simp add: dist_norm add_divide_distrib abs_diff_less_iff del: less_divide_eq_numeral1) (simp add: field_simps)
  6.2572 +    have t01: "t \<in> {0..1}" using `kk \<subseteq> {0..1}` `t \<in> kk` by blast
  6.2573 +    obtain d1 where "d1 > 0" and d1:
  6.2574 +        "\<And>g1 g2. \<lbrakk>valid_path g1; valid_path g2;
  6.2575 +                   \<forall>u\<in>{0..1}. cmod (g1 u - k (n/N, u)) < d1 \<and> cmod (g2 u - k ((Suc n) / N, u)) < d1;
  6.2576 +                   linked_paths atends g1 g2\<rbrakk>
  6.2577 +                   \<Longrightarrow> contour_integral g2 f = contour_integral g1 f"
  6.2578 +      using ee [THEN conjunct2, rule_format, OF t01 N01 nN_less n'N_less] by fastforce
  6.2579 +    have "n \<le> N" using Suc.prems by auto
  6.2580 +    with Suc.hyps
  6.2581 +    obtain d2 where "d2 > 0"
  6.2582 +      and d2: "\<And>j. \<lbrakk>valid_path j; \<forall>u\<in>{0..1}. cmod (j u - k (n/N, u)) < d2; linked_paths atends g j\<rbrakk>
  6.2583 +                     \<Longrightarrow> contour_integral j f = contour_integral g f"
  6.2584 +        by auto
  6.2585 +    have "continuous_on {0..1} (k o (\<lambda>u. (n/N, u)))"
  6.2586 +      apply (rule continuous_intros continuous_on_subset [OF contk])+
  6.2587 +      using N01 by auto
  6.2588 +    then have pkn: "path (\<lambda>u. k (n/N, u))"
  6.2589 +      by (simp add: path_def)
  6.2590 +    have min12: "min d1 d2 > 0" by (simp add: `0 < d1` `0 < d2`)
  6.2591 +    obtain p where "polynomial_function p"
  6.2592 +        and psf: "pathstart p = pathstart (\<lambda>u. k (n/N, u))"
  6.2593 +                 "pathfinish p = pathfinish (\<lambda>u. k (n/N, u))"
  6.2594 +        and pk_le:  "\<And>t. t\<in>{0..1} \<Longrightarrow> cmod (p t - k (n/N, t)) < min d1 d2"
  6.2595 +      using path_approx_polynomial_function [OF pkn min12] by blast
  6.2596 +    then have vpp: "valid_path p" using valid_path_polynomial_function by blast
  6.2597 +    have lpa: "linked_paths atends g p"
  6.2598 +      by (metis (mono_tags, lifting) N01(1) ksf linked_paths_def pathfinish_def pathstart_def psf)
  6.2599 +    show ?case
  6.2600 +      apply (rule_tac x="min d1 d2" in exI)
  6.2601 +      apply (simp add: `0 < d1` `0 < d2`, clarify)
  6.2602 +      apply (rule_tac s="contour_integral p f" in trans)
  6.2603 +      using pk_le N01(1) ksf pathfinish_def pathstart_def
  6.2604 +      apply (force intro!: vpp d1 simp add: linked_paths_def psf ksf)
  6.2605 +      using pk_le N01 apply (force intro!: vpp d2 lpa simp add: linked_paths_def psf ksf)
  6.2606 +      done
  6.2607 +  qed
  6.2608 +  then obtain d where "0 < d"
  6.2609 +                       "\<And>j. valid_path j \<and> (\<forall>u \<in> {0..1}. norm(j u - k (1,u)) < d) \<and>
  6.2610 +                            linked_paths atends g j
  6.2611 +                            \<Longrightarrow> contour_integral j f = contour_integral g f"
  6.2612 +    using \<open>N>0\<close> by auto
  6.2613 +  then have "linked_paths atends g h \<Longrightarrow> contour_integral h f = contour_integral g f"
  6.2614 +    using \<open>N>0\<close> vph by fastforce
  6.2615 +  then show ?thesis
  6.2616 +    by (simp add: pathsf)
  6.2617 +qed
  6.2618 +
  6.2619 +proposition Cauchy_theorem_homotopic_paths:
  6.2620 +    assumes hom: "homotopic_paths s g h"
  6.2621 +        and "open s" and f: "f holomorphic_on s"
  6.2622 +        and vpg: "valid_path g" and vph: "valid_path h"
  6.2623 +    shows "contour_integral g f = contour_integral h f"
  6.2624 +  using Cauchy_theorem_homotopic [of True s g h] assms by simp
  6.2625 +
  6.2626 +proposition Cauchy_theorem_homotopic_loops:
  6.2627 +    assumes hom: "homotopic_loops s g h"
  6.2628 +        and "open s" and f: "f holomorphic_on s"
  6.2629 +        and vpg: "valid_path g" and vph: "valid_path h"
  6.2630 +    shows "contour_integral g f = contour_integral h f"
  6.2631 +  using Cauchy_theorem_homotopic [of False s g h] assms by simp
  6.2632 +
  6.2633 +lemma has_contour_integral_newpath:
  6.2634 +    "\<lbrakk>(f has_contour_integral y) h; f contour_integrable_on g; contour_integral g f = contour_integral h f\<rbrakk>
  6.2635 +     \<Longrightarrow> (f has_contour_integral y) g"
  6.2636 +  using has_contour_integral_integral contour_integral_unique by auto
  6.2637 +
  6.2638 +lemma Cauchy_theorem_null_homotopic:
  6.2639 +     "\<lbrakk>f holomorphic_on s; open s; valid_path g; homotopic_loops s g (linepath a a)\<rbrakk> \<Longrightarrow> (f has_contour_integral 0) g"
  6.2640 +  apply (rule has_contour_integral_newpath [where h = "linepath a a"], simp)
  6.2641 +  using contour_integrable_holomorphic_simple
  6.2642 +    apply (blast dest: holomorphic_on_imp_continuous_on homotopic_loops_imp_subset)
  6.2643 +  by (simp add: Cauchy_theorem_homotopic_loops)
  6.2644 +
  6.2645 +
  6.2646 +
  6.2647 +subsection\<open>More winding number properties\<close>
  6.2648 +
  6.2649 +text\<open>including the fact that it's +-1 inside a simple closed curve.\<close>
  6.2650 +
  6.2651 +lemma winding_number_homotopic_paths:
  6.2652 +    assumes "homotopic_paths (-{z}) g h"
  6.2653 +      shows "winding_number g z = winding_number h z"
  6.2654 +proof -
  6.2655 +  have "path g" "path h" using homotopic_paths_imp_path [OF assms] by auto
  6.2656 +  moreover have pag: "z \<notin> path_image g" and pah: "z \<notin> path_image h"
  6.2657 +    using homotopic_paths_imp_subset [OF assms] by auto
  6.2658 +  ultimately obtain d e where "d > 0" "e > 0"
  6.2659 +      and d: "\<And>p. \<lbrakk>path p; pathstart p = pathstart g; pathfinish p = pathfinish g; \<forall>t\<in>{0..1}. norm (p t - g t) < d\<rbrakk>
  6.2660 +            \<Longrightarrow> homotopic_paths (-{z}) g p"
  6.2661 +      and e: "\<And>q. \<lbrakk>path q; pathstart q = pathstart h; pathfinish q = pathfinish h; \<forall>t\<in>{0..1}. norm (q t - h t) < e\<rbrakk>
  6.2662 +            \<Longrightarrow> homotopic_paths (-{z}) h q"
  6.2663 +    using homotopic_nearby_paths [of g "-{z}"] homotopic_nearby_paths [of h "-{z}"] by force
  6.2664 +  obtain p where p:
  6.2665 +       "valid_path p" "z \<notin> path_image p"
  6.2666 +       "pathstart p = pathstart g" "pathfinish p = pathfinish g"
  6.2667 +       and gp_less:"\<forall>t\<in>{0..1}. cmod (g t - p t) < d"
  6.2668 +       and pap: "contour_integral p (\<lambda>w. 1 / (w - z)) = complex_of_real (2 * pi) * \<i> * winding_number g z"
  6.2669 +    using winding_number [OF \<open>path g\<close> pag \<open>0 < d\<close>] by blast
  6.2670 +  obtain q where q:
  6.2671 +       "valid_path q" "z \<notin> path_image q"
  6.2672 +       "pathstart q = pathstart h" "pathfinish q = pathfinish h"
  6.2673 +       and hq_less: "\<forall>t\<in>{0..1}. cmod (h t - q t) < e"
  6.2674 +       and paq:  "contour_integral q (\<lambda>w. 1 / (w - z)) = complex_of_real (2 * pi) * \<i> * winding_number h z"
  6.2675 +    using winding_number [OF \<open>path h\<close> pah \<open>0 < e\<close>] by blast
  6.2676 +  have gp: "homotopic_paths (- {z}) g p"
  6.2677 +    by (simp add: d p valid_path_imp_path norm_minus_commute gp_less)
  6.2678 +  have hq: "homotopic_paths (- {z}) h q"
  6.2679 +    by (simp add: e q valid_path_imp_path norm_minus_commute hq_less)
  6.2680 +  have "contour_integral p (\<lambda>w. 1/(w - z)) = contour_integral q (\<lambda>w. 1/(w - z))"
  6.2681 +    apply (rule Cauchy_theorem_homotopic_paths [of "-{z}"])
  6.2682 +    apply (blast intro: homotopic_paths_trans homotopic_paths_sym gp hq assms)
  6.2683 +    apply (auto intro!: holomorphic_intros simp: p q)
  6.2684 +    done
  6.2685 +  then show ?thesis
  6.2686 +    by (simp add: pap paq)
  6.2687 +qed
  6.2688 +
  6.2689 +lemma winding_number_homotopic_loops:
  6.2690 +    assumes "homotopic_loops (-{z}) g h"
  6.2691 +      shows "winding_number g z = winding_number h z"
  6.2692 +proof -
  6.2693 +  have "path g" "path h" using homotopic_loops_imp_path [OF assms] by auto
  6.2694 +  moreover have pag: "z \<notin> path_image g" and pah: "z \<notin> path_image h"
  6.2695 +    using homotopic_loops_imp_subset [OF assms] by auto
  6.2696 +  moreover have gloop: "pathfinish g = pathstart g" and hloop: "pathfinish h = pathstart h"
  6.2697 +    using homotopic_loops_imp_loop [OF assms] by auto
  6.2698 +  ultimately obtain d e where "d > 0" "e > 0"
  6.2699 +      and d: "\<And>p. \<lbrakk>path p; pathfinish p = pathstart p; \<forall>t\<in>{0..1}. norm (p t - g t) < d\<rbrakk>
  6.2700 +            \<Longrightarrow> homotopic_loops (-{z}) g p"
  6.2701 +      and e: "\<And>q. \<lbrakk>path q; pathfinish q = pathstart q; \<forall>t\<in>{0..1}. norm (q t - h t) < e\<rbrakk>
  6.2702 +            \<Longrightarrow> homotopic_loops (-{z}) h q"
  6.2703 +    using homotopic_nearby_loops [of g "-{z}"] homotopic_nearby_loops [of h "-{z}"] by force
  6.2704 +  obtain p where p:
  6.2705 +       "valid_path p" "z \<notin> path_image p"
  6.2706 +       "pathstart p = pathstart g" "pathfinish p = pathfinish g"
  6.2707 +       and gp_less:"\<forall>t\<in>{0..1}. cmod (g t - p t) < d"
  6.2708 +       and pap: "contour_integral p (\<lambda>w. 1 / (w - z)) = complex_of_real (2 * pi) * \<i> * winding_number g z"
  6.2709 +    using winding_number [OF \<open>path g\<close> pag \<open>0 < d\<close>] by blast
  6.2710 +  obtain q where q:
  6.2711 +       "valid_path q" "z \<notin> path_image q"
  6.2712 +       "pathstart q = pathstart h" "pathfinish q = pathfinish h"
  6.2713 +       and hq_less: "\<forall>t\<in>{0..1}. cmod (h t - q t) < e"
  6.2714 +       and paq:  "contour_integral q (\<lambda>w. 1 / (w - z)) = complex_of_real (2 * pi) * \<i> * winding_number h z"
  6.2715 +    using winding_number [OF \<open>path h\<close> pah \<open>0 < e\<close>] by blast
  6.2716 +  have gp: "homotopic_loops (- {z}) g p"
  6.2717 +    by (simp add: gloop d gp_less norm_minus_commute p valid_path_imp_path)
  6.2718 +  have hq: "homotopic_loops (- {z}) h q"
  6.2719 +    by (simp add: e hloop hq_less norm_minus_commute q valid_path_imp_path)
  6.2720 +  have "contour_integral p (\<lambda>w. 1/(w - z)) = contour_integral q (\<lambda>w. 1/(w - z))"
  6.2721 +    apply (rule Cauchy_theorem_homotopic_loops [of "-{z}"])
  6.2722 +    apply (blast intro: homotopic_loops_trans homotopic_loops_sym gp hq assms)
  6.2723 +    apply (auto intro!: holomorphic_intros simp: p q)
  6.2724 +    done
  6.2725 +  then show ?thesis
  6.2726 +    by (simp add: pap paq)
  6.2727 +qed
  6.2728 +
  6.2729 +lemma winding_number_paths_linear_eq:
  6.2730 +  "\<lbrakk>path g; path h; pathstart h = pathstart g; pathfinish h = pathfinish g;
  6.2731 +    \<And>t. t \<in> {0..1} \<Longrightarrow> z \<notin> closed_segment (g t) (h t)\<rbrakk>
  6.2732 +        \<Longrightarrow> winding_number h z = winding_number g z"
  6.2733 +  by (blast intro: sym homotopic_paths_linear winding_number_homotopic_paths elim: )
  6.2734 +
  6.2735 +lemma winding_number_loops_linear_eq:
  6.2736 +  "\<lbrakk>path g; path h; pathfinish g = pathstart g; pathfinish h = pathstart h;
  6.2737 +    \<And>t. t \<in> {0..1} \<Longrightarrow> z \<notin> closed_segment (g t) (h t)\<rbrakk>
  6.2738 +        \<Longrightarrow> winding_number h z = winding_number g z"
  6.2739 +  by (blast intro: sym homotopic_loops_linear winding_number_homotopic_loops elim: )
  6.2740 +
  6.2741 +lemma winding_number_nearby_paths_eq:
  6.2742 +     "\<lbrakk>path g; path h;
  6.2743 +      pathstart h = pathstart g; pathfinish h = pathfinish g;
  6.2744 +      \<And>t. t \<in> {0..1} \<Longrightarrow> norm(h t - g t) < norm(g t - z)\<rbrakk>
  6.2745 +      \<Longrightarrow> winding_number h z = winding_number g z"
  6.2746 +  by (metis segment_bound(2) norm_minus_commute not_le winding_number_paths_linear_eq)
  6.2747 +
  6.2748 +lemma winding_number_nearby_loops_eq:
  6.2749 +     "\<lbrakk>path g; path h;
  6.2750 +      pathfinish g = pathstart g;
  6.2751 +        pathfinish h = pathstart h;
  6.2752 +      \<And>t. t \<in> {0..1} \<Longrightarrow> norm(h t - g t) < norm(g t - z)\<rbrakk>
  6.2753 +      \<Longrightarrow> winding_number h z = winding_number g z"
  6.2754 +  by (metis segment_bound(2) norm_minus_commute not_le winding_number_loops_linear_eq)
  6.2755 +
  6.2756  end
     7.1 --- a/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy	Sun Nov 22 23:19:43 2015 +0100
     7.2 +++ b/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy	Mon Nov 23 16:57:54 2015 +0000
     7.3 @@ -6410,14 +6410,6 @@
     7.4      by (auto simp add:norm_minus_commute)
     7.5  qed
     7.6  
     7.7 -lemma segment_bound:
     7.8 -  fixes x a b :: "'a::euclidean_space"
     7.9 -  assumes "x \<in> closed_segment a b"
    7.10 -  shows "norm (x - a) \<le> norm (b - a)" "norm (x - b) \<le> norm (b - a)"
    7.11 -  using segment_furthest_le[OF assms, of a]
    7.12 -  using segment_furthest_le[OF assms, of b]
    7.13 -  by (auto simp add:norm_minus_commute)
    7.14 -
    7.15  lemma closed_segment_commute: "closed_segment a b = closed_segment b a"
    7.16  proof -
    7.17    have "{a, b} = {b, a}" by auto
    7.18 @@ -6425,6 +6417,25 @@
    7.19      by (simp add: segment_convex_hull)
    7.20  qed
    7.21  
    7.22 +lemma segment_bound1:
    7.23 +  assumes "x \<in> closed_segment a b"
    7.24 +  shows "norm (x - a) \<le> norm (b - a)"
    7.25 +proof -
    7.26 +  obtain u where "x = (1 - u) *\<^sub>R a + u *\<^sub>R b" "0 \<le> u" "u \<le> 1"
    7.27 +    using assms by (auto simp add: closed_segment_def)
    7.28 +  then show "norm (x - a) \<le> norm (b - a)"
    7.29 +    apply clarify
    7.30 +    apply (auto simp: algebra_simps)
    7.31 +    apply (simp add: scaleR_diff_right [symmetric] mult_left_le_one_le)
    7.32 +    done
    7.33 +qed
    7.34 +
    7.35 +lemma segment_bound:
    7.36 +  assumes "x \<in> closed_segment a b"
    7.37 +  shows "norm (x - a) \<le> norm (b - a)" "norm (x - b) \<le> norm (b - a)"
    7.38 +apply (simp add: assms segment_bound1)
    7.39 +by (metis assms closed_segment_commute dist_commute dist_norm segment_bound1)
    7.40 +
    7.41  lemma open_segment_commute: "open_segment a b = open_segment b a"
    7.42  proof -
    7.43    have "{a, b} = {b, a}" by auto
    7.44 @@ -6489,6 +6500,28 @@
    7.45  
    7.46  lemmas segment_image_interval = closed_segment_image_interval open_segment_image_interval
    7.47  
    7.48 +lemma open_segment_eq: "open_segment a b = (if a=b then {} else {(1 - u) *\<^sub>R a + u *\<^sub>R b | u::real. 0 < u \<and> u < 1})"
    7.49 +  by (auto simp: open_segment_def closed_segment_def segment_degen_0 segment_degen_1)
    7.50 +
    7.51 +lemma open_segment_bound1:
    7.52 +  assumes "x \<in> open_segment a b"
    7.53 +  shows "norm (x - a) < norm (b - a)"
    7.54 +proof -
    7.55 +  obtain u where "x = (1 - u) *\<^sub>R a + u *\<^sub>R b" "0 < u" "u < 1" "a \<noteq> b"
    7.56 +    using assms by (auto simp add: open_segment_eq split: split_if_asm)
    7.57 +  then show "norm (x - a) < norm (b - a)"
    7.58 +    apply clarify
    7.59 +    apply (auto simp: algebra_simps)
    7.60 +    apply (simp add: scaleR_diff_right [symmetric])
    7.61 +    done
    7.62 +qed
    7.63 +
    7.64 +lemma open_segment_bound:
    7.65 +  assumes "x \<in> open_segment a b"
    7.66 +  shows "norm (x - a) < norm (b - a)" "norm (x - b) < norm (b - a)"
    7.67 +apply (simp add: assms open_segment_bound1)
    7.68 +by (metis assms norm_minus_commute open_segment_bound1 open_segment_commute)
    7.69 +
    7.70  lemma closure_closed_segment [simp]:
    7.71      fixes a :: "'a::euclidean_space"
    7.72      shows "closure(closed_segment a b) = closed_segment a b"
     8.1 --- a/src/HOL/Multivariate_Analysis/Path_Connected.thy	Sun Nov 22 23:19:43 2015 +0100
     8.2 +++ b/src/HOL/Multivariate_Analysis/Path_Connected.thy	Mon Nov 23 16:57:54 2015 +0000
     8.3 @@ -1,5 +1,5 @@
     8.4  (*  Title:      HOL/Multivariate_Analysis/Path_Connected.thy
     8.5 -    Author:     Robert Himmelmann, TU Muenchen, and LCP with material from HOL Light
     8.6 +    Author:     Robert Himmelmann, TU Muenchen, and LC Paulson with material from HOL Light
     8.7  *)
     8.8  
     8.9  section \<open>Continuous paths and path-connected sets\<close>
    8.10 @@ -8,21 +8,6 @@
    8.11  imports Convex_Euclidean_Space
    8.12  begin
    8.13  
    8.14 -(*FIXME move up?*)
    8.15 -lemma image_affinity_interval:
    8.16 -  fixes c :: "'a::ordered_real_vector"
    8.17 -  shows "((\<lambda>x. m *\<^sub>R x + c) ` {a..b}) = (if {a..b}={} then {}
    8.18 -            else if 0 <= m then {m *\<^sub>R a + c .. m  *\<^sub>R b + c}
    8.19 -            else {m *\<^sub>R b + c .. m *\<^sub>R a + c})"
    8.20 -  apply (case_tac "m=0", force)
    8.21 -  apply (auto simp: scaleR_left_mono)
    8.22 -  apply (rule_tac x="inverse m *\<^sub>R (x-c)" in rev_image_eqI, auto simp: pos_le_divideR_eq le_diff_eq scaleR_left_mono_neg)
    8.23 -  apply (metis diff_le_eq inverse_inverse_eq order.not_eq_order_implies_strict pos_le_divideR_eq positive_imp_inverse_positive)
    8.24 -  apply (rule_tac x="inverse m *\<^sub>R (x-c)" in rev_image_eqI, auto simp: not_le neg_le_divideR_eq diff_le_eq)
    8.25 -  using le_diff_eq scaleR_le_cancel_left_neg
    8.26 -  apply fastforce
    8.27 -  done
    8.28 -
    8.29  subsection \<open>Paths and Arcs\<close>
    8.30  
    8.31  definition path :: "(real \<Rightarrow> 'a::topological_space) \<Rightarrow> bool"
    8.32 @@ -1019,7 +1004,7 @@
    8.33  
    8.34  lemma linepath_trivial [simp]: "linepath a a x = a"
    8.35    by (simp add: linepath_def real_vector.scale_left_diff_distrib)
    8.36 -    
    8.37 +
    8.38  lemma subpath_refl: "subpath a a g = linepath (g a) (g a)"
    8.39    by (simp add: subpath_def linepath_def algebra_simps)
    8.40  
    8.41 @@ -1333,14 +1318,7 @@
    8.42  
    8.43  lemma homeomorphic_path_connectedness:
    8.44    "s homeomorphic t \<Longrightarrow> path_connected s \<longleftrightarrow> path_connected t"
    8.45 -  unfolding homeomorphic_def homeomorphism_def
    8.46 -  apply (erule exE|erule conjE)+
    8.47 -  apply rule
    8.48 -  apply (drule_tac f=f in path_connected_continuous_image)
    8.49 -  prefer 3
    8.50 -  apply (drule_tac f=g in path_connected_continuous_image)
    8.51 -  apply auto
    8.52 -  done
    8.53 +  unfolding homeomorphic_def homeomorphism_def by (metis path_connected_continuous_image)
    8.54  
    8.55  lemma path_connected_empty: "path_connected {}"
    8.56    unfolding path_connected_def by auto
    8.57 @@ -2809,8 +2787,11 @@
    8.58  proposition homotopic_paths_refl [simp]: "homotopic_paths s p p \<longleftrightarrow> path p \<and> path_image p \<subseteq> s"
    8.59  by (simp add: homotopic_paths_def homotopic_with_refl path_def path_image_def)
    8.60  
    8.61 -proposition homotopic_paths_sym: "homotopic_paths s p q \<longleftrightarrow> homotopic_paths s q p"
    8.62 -  by (metis (mono_tags) homotopic_paths_def homotopic_paths_imp_pathfinish homotopic_paths_imp_pathstart homotopic_with_symD)+
    8.63 +proposition homotopic_paths_sym: "homotopic_paths s p q \<Longrightarrow> homotopic_paths s q p"
    8.64 +  by (metis (mono_tags) homotopic_paths_def homotopic_paths_imp_pathfinish homotopic_paths_imp_pathstart homotopic_with_symD)
    8.65 +
    8.66 +proposition homotopic_paths_sym_eq: "homotopic_paths s p q \<longleftrightarrow> homotopic_paths s q p"
    8.67 +  by (metis homotopic_paths_sym)
    8.68  
    8.69  proposition homotopic_paths_trans:
    8.70       "\<lbrakk>homotopic_paths s p q; homotopic_paths s q r\<rbrakk> \<Longrightarrow> homotopic_paths s p r"
    8.71 @@ -2938,7 +2919,7 @@
    8.72  proposition homotopic_paths_lid:
    8.73     "\<lbrakk>path p; path_image p \<subseteq> s\<rbrakk> \<Longrightarrow> homotopic_paths s (linepath (pathstart p) (pathstart p) +++ p) p"
    8.74  using homotopic_paths_rid [of "reversepath p" s]
    8.75 -  by (metis homotopic_paths_reversepath path_image_reversepath path_reversepath pathfinish_linepath 
    8.76 +  by (metis homotopic_paths_reversepath path_image_reversepath path_reversepath pathfinish_linepath
    8.77          pathfinish_reversepath reversepath_joinpaths reversepath_linepath)
    8.78  
    8.79  proposition homotopic_paths_assoc:
    8.80 @@ -2961,7 +2942,7 @@
    8.81      shows "homotopic_paths s (p +++ reversepath p) (linepath (pathstart p) (pathstart p))"
    8.82  proof -
    8.83    have "continuous_on ({0..1} \<times> {0..1}) (\<lambda>x. (subpath 0 (fst x) p +++ reversepath (subpath 0 (fst x) p)) (snd x))"
    8.84 -    using assms 
    8.85 +    using assms
    8.86      apply (simp add: joinpaths_def subpath_def reversepath_def path_def del: le_divide_eq_numeral1)
    8.87      apply (rule continuous_on_cases_le)
    8.88      apply (rule_tac [2] continuous_on_compose [of _ _ p, unfolded o_def])
    8.89 @@ -2971,8 +2952,8 @@
    8.90      done
    8.91    then show ?thesis
    8.92      using assms
    8.93 -    apply (subst homotopic_paths_sym)
    8.94 -    apply (simp add: homotopic_paths_def homotopic_with_def)
    8.95 +    apply (subst homotopic_paths_sym_eq)
    8.96 +    unfolding homotopic_paths_def homotopic_with_def
    8.97      apply (rule_tac x="(\<lambda>y. (subpath 0 (fst y) p +++ reversepath(subpath 0 (fst y) p)) (snd y))" in exI)
    8.98      apply (simp add: path_defs joinpaths_def subpath_def reversepath_def)
    8.99      apply (force simp: mult_le_one)
   8.100 @@ -3009,25 +2990,22 @@
   8.101    unfolding homotopic_loops_def path_def
   8.102    using homotopic_with_imp_continuous by blast
   8.103  
   8.104 -proposition homotopic_loops_imp_subset1:
   8.105 -     "homotopic_loops s p q \<Longrightarrow> path_image p \<subseteq> s"
   8.106 +proposition homotopic_loops_imp_subset:
   8.107 +     "homotopic_loops s p q \<Longrightarrow> path_image p \<subseteq> s \<and> path_image q \<subseteq> s"
   8.108    unfolding homotopic_loops_def path_image_def
   8.109 -  using homotopic_with_imp_subset1  by blast
   8.110 -
   8.111 -proposition homotopic_loops_imp_subset2:
   8.112 -     "homotopic_loops s p q \<Longrightarrow> path_image q \<subseteq> s"
   8.113 -  unfolding homotopic_loops_def path_image_def
   8.114 -  using homotopic_with_imp_subset2 by blast
   8.115 +  by (metis homotopic_with_imp_subset1 homotopic_with_imp_subset2)
   8.116  
   8.117  proposition homotopic_loops_refl:
   8.118       "homotopic_loops s p p \<longleftrightarrow>
   8.119        path p \<and> path_image p \<subseteq> s \<and> pathfinish p = pathstart p"
   8.120    by (simp add: homotopic_loops_def homotopic_with_refl path_image_def path_def)
   8.121  
   8.122 -proposition homotopic_loops_sym:
   8.123 -   "homotopic_loops s p q \<longleftrightarrow> homotopic_loops s q p"
   8.124 +proposition homotopic_loops_sym: "homotopic_loops s p q \<Longrightarrow> homotopic_loops s q p"
   8.125    by (simp add: homotopic_loops_def homotopic_with_sym)
   8.126  
   8.127 +proposition homotopic_loops_sym_eq: "homotopic_loops s p q \<longleftrightarrow> homotopic_loops s q p"
   8.128 +  by (metis homotopic_loops_sym)
   8.129 +
   8.130  proposition homotopic_loops_trans:
   8.131     "\<lbrakk>homotopic_loops s p q; homotopic_loops s q r\<rbrakk> \<Longrightarrow> homotopic_loops s p r"
   8.132    unfolding homotopic_loops_def by (blast intro: homotopic_with_trans)
   8.133 @@ -3065,7 +3043,7 @@
   8.134  proof -
   8.135    have "path p" by (metis assms homotopic_loops_imp_path)
   8.136    have ploop: "pathfinish p = pathstart p" by (metis assms homotopic_loops_imp_loop)
   8.137 -  have pip: "path_image p \<subseteq> s" by (metis assms homotopic_loops_imp_subset1)
   8.138 +  have pip: "path_image p \<subseteq> s" by (metis assms homotopic_loops_imp_subset)
   8.139    obtain h where conth: "continuous_on ({0..1::real} \<times> {0..1}) h"
   8.140               and hs: "h ` ({0..1} \<times> {0..1}) \<subseteq> s"
   8.141               and [simp]: "\<And>x. x \<in> {0..1} \<Longrightarrow> h(0,x) = p x"
   8.142 @@ -3105,22 +3083,22 @@
   8.143                homotopic_paths_trans homotopic_paths_sym homotopic_paths_rinv)
   8.144    have 1: "homotopic_paths s p (p +++ linepath (pathfinish p) (pathfinish p))"
   8.145      using \<open>path p\<close> homotopic_paths_rid homotopic_paths_sym pip by blast
   8.146 -  moreover have "homotopic_paths s (p +++ linepath (pathfinish p) (pathfinish p)) 
   8.147 +  moreover have "homotopic_paths s (p +++ linepath (pathfinish p) (pathfinish p))
   8.148                                     (linepath (pathstart p) (pathstart p) +++ p +++ linepath (pathfinish p) (pathfinish p))"
   8.149 -    apply (subst homotopic_paths_sym)
   8.150 +    apply (rule homotopic_paths_sym)
   8.151      using homotopic_paths_lid [of "p +++ linepath (pathfinish p) (pathfinish p)" s]
   8.152      by (metis 1 homotopic_paths_imp_path homotopic_paths_imp_pathstart homotopic_paths_imp_subset)
   8.153 -  moreover have "homotopic_paths s (linepath (pathstart p) (pathstart p) +++ p +++ linepath (pathfinish p) (pathfinish p)) 
   8.154 +  moreover have "homotopic_paths s (linepath (pathstart p) (pathstart p) +++ p +++ linepath (pathfinish p) (pathfinish p))
   8.155                                     ((\<lambda>u. h (u, 0)) +++ linepath a a +++ reversepath (\<lambda>u. h (u, 0)))"
   8.156      apply (simp add: homotopic_paths_def homotopic_with_def)
   8.157      apply (rule_tac x="\<lambda>y. (subpath 0 (fst y) (\<lambda>u. h (u, 0)) +++ (\<lambda>u. h (Pair (fst y) u)) +++ subpath (fst y) 0 (\<lambda>u. h (u, 0))) (snd y)" in exI)
   8.158      apply (simp add: subpath_reversepath)
   8.159      apply (intro conjI homotopic_join_lemma)
   8.160 -    using ploop 
   8.161 +    using ploop
   8.162      apply (simp_all add: path_defs joinpaths_def o_def subpath_def conth c1 c2)
   8.163      apply (force simp: algebra_simps mult_le_one mult_left_le intro: hs [THEN subsetD] adhoc_le)
   8.164      done
   8.165 -  moreover have "homotopic_paths s ((\<lambda>u. h (u, 0)) +++ linepath a a +++ reversepath (\<lambda>u. h (u, 0))) 
   8.166 +  moreover have "homotopic_paths s ((\<lambda>u. h (u, 0)) +++ linepath a a +++ reversepath (\<lambda>u. h (u, 0)))
   8.167                                     (linepath (pathstart p) (pathstart p))"
   8.168      apply (rule *)
   8.169      apply (simp add: pih0 pathstart_def pathfinish_def conth0)
   8.170 @@ -3132,7 +3110,7 @@
   8.171  
   8.172  proposition homotopic_loops_conjugate:
   8.173    fixes s :: "'a::real_normed_vector set"
   8.174 -  assumes "path p" "path q" and pip: "path_image p \<subseteq> s" and piq: "path_image q \<subseteq> s" 
   8.175 +  assumes "path p" "path q" and pip: "path_image p \<subseteq> s" and piq: "path_image q \<subseteq> s"
   8.176        and papp: "pathfinish p = pathstart q" and qloop: "pathfinish q = pathstart q"
   8.177      shows "homotopic_loops s (p +++ q +++ reversepath p) q"
   8.178  proof -
   8.179 @@ -3151,17 +3129,17 @@
   8.180      apply (auto simp: algebra_simps add_increasing2 mult_left_le_one_le)
   8.181      done
   8.182    have ps1: "\<And>a b. \<lbrakk>b * 2 \<le> 1; 0 \<le> b; 0 \<le> a; a \<le> 1\<rbrakk> \<Longrightarrow> p ((1 - a) * (2 * b) + a) \<in> s"
   8.183 -    using sum_le_prod1   
   8.184 +    using sum_le_prod1
   8.185      by (force simp: algebra_simps add_increasing2 mult_left_le intro: pip [unfolded path_image_def, THEN subsetD])
   8.186    have ps2: "\<And>a b. \<lbrakk>\<not> 4 * b \<le> 3; b \<le> 1; 0 \<le> a; a \<le> 1\<rbrakk> \<Longrightarrow> p ((a - 1) * (4 * b - 3) + 1) \<in> s"
   8.187      apply (rule pip [unfolded path_image_def, THEN subsetD])
   8.188      apply (rule image_eqI, blast)
   8.189      apply (simp add: algebra_simps)
   8.190 -    by (metis add_mono_thms_linordered_semiring(1) affine_ineq linear mult.commute mult.left_neutral mult_right_mono not_le 
   8.191 +    by (metis add_mono_thms_linordered_semiring(1) affine_ineq linear mult.commute mult.left_neutral mult_right_mono not_le
   8.192                add.commute zero_le_numeral)
   8.193    have qs: "\<And>a b. \<lbrakk>4 * b \<le> 3; \<not> b * 2 \<le> 1\<rbrakk> \<Longrightarrow> q (4 * b - 2) \<in> s"
   8.194      using path_image_def piq by fastforce
   8.195 -  have "homotopic_loops s (p +++ q +++ reversepath p) 
   8.196 +  have "homotopic_loops s (p +++ q +++ reversepath p)
   8.197                            (linepath (pathstart q) (pathstart q) +++ q +++ linepath (pathstart q) (pathstart q))"
   8.198      apply (simp add: homotopic_loops_def homotopic_with_def)
   8.199      apply (rule_tac x="(\<lambda>y. (subpath (fst y) 1 p +++ q +++ subpath 1 (fst y) p) (snd y))" in exI)
   8.200 @@ -3178,14 +3156,14 @@
   8.201        using \<open>path q\<close> homotopic_paths_lid qloop piq by auto
   8.202      hence 1: "\<And>f. homotopic_paths s f q \<or> \<not> homotopic_paths s f (linepath (pathfinish q) (pathfinish q) +++ q)"
   8.203        using homotopic_paths_trans by blast
   8.204 -    hence "homotopic_paths s (linepath (pathfinish q) (pathfinish q) +++ q +++ linepath (pathfinish q) (pathfinish q)) q"    
   8.205 +    hence "homotopic_paths s (linepath (pathfinish q) (pathfinish q) +++ q +++ linepath (pathfinish q) (pathfinish q)) q"
   8.206      proof -
   8.207        have "homotopic_paths s (q +++ linepath (pathfinish q) (pathfinish q)) q"
   8.208          by (simp add: \<open>path q\<close> homotopic_paths_rid piq)
   8.209        thus ?thesis
   8.210 -        by (metis (no_types) 1 \<open>path q\<close> homotopic_paths_join homotopic_paths_rinv homotopic_paths_sym 
   8.211 +        by (metis (no_types) 1 \<open>path q\<close> homotopic_paths_join homotopic_paths_rinv homotopic_paths_sym
   8.212                    homotopic_paths_trans qloop pathfinish_linepath piq)
   8.213 -    qed 
   8.214 +    qed
   8.215      thus ?thesis
   8.216        by (metis (no_types) qloop homotopic_loops_sym homotopic_paths_imp_homotopic_loops homotopic_paths_imp_pathfinish homotopic_paths_sym)
   8.217    qed
   8.218 @@ -3193,4 +3171,95 @@
   8.219      by (blast intro: homotopic_loops_trans)
   8.220  qed
   8.221  
   8.222 +
   8.223 +subsection\<open> Homotopy of "nearby" function, paths and loops.\<close>
   8.224 +
   8.225 +lemma homotopic_with_linear:
   8.226 +  fixes f g :: "_ \<Rightarrow> 'b::real_normed_vector"
   8.227 +  assumes contf: "continuous_on s f"
   8.228 +      and contg:"continuous_on s g"
   8.229 +      and sub: "\<And>x. x \<in> s \<Longrightarrow> closed_segment (f x) (g x) \<subseteq> t"
   8.230 +    shows "homotopic_with (\<lambda>z. True) s t f g"
   8.231 +  apply (simp add: homotopic_with_def)
   8.232 +  apply (rule_tac x="\<lambda>y. ((1 - (fst y)) *\<^sub>R f(snd y) + (fst y) *\<^sub>R g(snd y))" in exI)
   8.233 +  apply (intro conjI)
   8.234 +  apply (rule subset_refl continuous_intros continuous_on_subset [OF contf] continuous_on_compose2 [where g=f]
   8.235 +                                            continuous_on_subset [OF contg] continuous_on_compose2 [where g=g]| simp)+
   8.236 +  using sub closed_segment_def apply fastforce+
   8.237 +  done
   8.238 +
   8.239 +lemma homotopic_paths_linear:
   8.240 +  fixes g h :: "real \<Rightarrow> 'a::real_normed_vector"
   8.241 +  assumes "path g" "path h" "pathstart h = pathstart g" "pathfinish h = pathfinish g"
   8.242 +          "\<And>t x. t \<in> {0..1} \<Longrightarrow> closed_segment (g t) (h t) \<subseteq> s"
   8.243 +    shows "homotopic_paths s g h"
   8.244 +  using assms
   8.245 +  unfolding path_def
   8.246 +  apply (simp add: pathstart_def pathfinish_def homotopic_paths_def homotopic_with_def)
   8.247 +  apply (rule_tac x="\<lambda>y. ((1 - (fst y)) *\<^sub>R g(snd y) + (fst y) *\<^sub>R h(snd y))" in exI)
   8.248 +  apply (auto intro!: continuous_intros intro: continuous_on_compose2 [where g=g] continuous_on_compose2 [where g=h] )
   8.249 +  apply (force simp: closed_segment_def)
   8.250 +  apply (simp_all add: algebra_simps)
   8.251 +  done
   8.252 +
   8.253 +lemma homotopic_loops_linear:
   8.254 +  fixes g h :: "real \<Rightarrow> 'a::real_normed_vector"
   8.255 +  assumes "path g" "path h" "pathfinish g = pathstart g" "pathfinish h = pathstart h"
   8.256 +          "\<And>t x. t \<in> {0..1} \<Longrightarrow> closed_segment (g t) (h t) \<subseteq> s"
   8.257 +    shows "homotopic_loops s g h"
   8.258 +  using assms
   8.259 +  unfolding path_def
   8.260 +  apply (simp add: pathstart_def pathfinish_def homotopic_loops_def homotopic_with_def)
   8.261 +  apply (rule_tac x="\<lambda>y. ((1 - (fst y)) *\<^sub>R g(snd y) + (fst y) *\<^sub>R h(snd y))" in exI)
   8.262 +  apply (auto intro!: continuous_intros intro: continuous_on_compose2 [where g=g] continuous_on_compose2 [where g=h])
   8.263 +  apply (force simp: closed_segment_def)
   8.264 +  done
   8.265 +
   8.266 +lemma homotopic_paths_nearby_explicit:
   8.267 +  assumes "path g" "path h" "pathstart h = pathstart g" "pathfinish h = pathfinish g"
   8.268 +      and no: "\<And>t x. \<lbrakk>t \<in> {0..1}; x \<notin> s\<rbrakk> \<Longrightarrow> norm(h t - g t) < norm(g t - x)"
   8.269 +    shows "homotopic_paths s g h"
   8.270 +  apply (rule homotopic_paths_linear [OF assms(1-4)])
   8.271 +  by (metis no segment_bound(1) subsetI norm_minus_commute not_le)
   8.272 +
   8.273 +lemma homotopic_loops_nearby_explicit:
   8.274 +  assumes "path g" "path h" "pathfinish g = pathstart g" "pathfinish h = pathstart h"
   8.275 +      and no: "\<And>t x. \<lbrakk>t \<in> {0..1}; x \<notin> s\<rbrakk> \<Longrightarrow> norm(h t - g t) < norm(g t - x)"
   8.276 +    shows "homotopic_loops s g h"
   8.277 +  apply (rule homotopic_loops_linear [OF assms(1-4)])
   8.278 +  by (metis no segment_bound(1) subsetI norm_minus_commute not_le)
   8.279 +
   8.280 +lemma homotopic_nearby_paths:
   8.281 +  fixes g h :: "real \<Rightarrow> 'a::euclidean_space"
   8.282 +  assumes "path g" "open s" "path_image g \<subseteq> s"
   8.283 +    shows "\<exists>e. 0 < e \<and>
   8.284 +               (\<forall>h. path h \<and>
   8.285 +                    pathstart h = pathstart g \<and> pathfinish h = pathfinish g \<and>
   8.286 +                    (\<forall>t \<in> {0..1}. norm(h t - g t) < e) \<longrightarrow> homotopic_paths s g h)"
   8.287 +proof -
   8.288 +  obtain e where "e > 0" and e: "\<And>x y. x \<in> path_image g \<Longrightarrow> y \<in> - s \<Longrightarrow> e \<le> dist x y"
   8.289 +    using separate_compact_closed [of "path_image g" "-s"] assms by force
   8.290 +  show ?thesis
   8.291 +    apply (intro exI conjI)
   8.292 +    using e [unfolded dist_norm]
   8.293 +    apply (auto simp: intro!: homotopic_paths_nearby_explicit assms  \<open>e > 0\<close>)
   8.294 +    by (metis atLeastAtMost_iff imageI le_less_trans not_le path_image_def)
   8.295 +qed
   8.296 +
   8.297 +lemma homotopic_nearby_loops:
   8.298 +  fixes g h :: "real \<Rightarrow> 'a::euclidean_space"
   8.299 +  assumes "path g" "open s" "path_image g \<subseteq> s" "pathfinish g = pathstart g"
   8.300 +    shows "\<exists>e. 0 < e \<and>
   8.301 +               (\<forall>h. path h \<and> pathfinish h = pathstart h \<and>
   8.302 +                    (\<forall>t \<in> {0..1}. norm(h t - g t) < e) \<longrightarrow> homotopic_loops s g h)"
   8.303 +proof -
   8.304 +  obtain e where "e > 0" and e: "\<And>x y. x \<in> path_image g \<Longrightarrow> y \<in> - s \<Longrightarrow> e \<le> dist x y"
   8.305 +    using separate_compact_closed [of "path_image g" "-s"] assms by force
   8.306 +  show ?thesis
   8.307 +    apply (intro exI conjI)
   8.308 +    using e [unfolded dist_norm]
   8.309 +    apply (auto simp: intro!: homotopic_loops_nearby_explicit assms  \<open>e > 0\<close>)
   8.310 +    by (metis atLeastAtMost_iff imageI le_less_trans not_le path_image_def)
   8.311 +qed
   8.312 +
   8.313  end
     9.1 --- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Sun Nov 22 23:19:43 2015 +0100
     9.2 +++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Mon Nov 23 16:57:54 2015 +0000
     9.3 @@ -15,6 +15,20 @@
     9.4    Norm_Arith
     9.5  begin
     9.6  
     9.7 +lemma image_affinity_interval:
     9.8 +  fixes c :: "'a::ordered_real_vector"
     9.9 +  shows "((\<lambda>x. m *\<^sub>R x + c) ` {a..b}) = (if {a..b}={} then {}
    9.10 +            else if 0 <= m then {m *\<^sub>R a + c .. m  *\<^sub>R b + c}
    9.11 +            else {m *\<^sub>R b + c .. m *\<^sub>R a + c})"
    9.12 +  apply (case_tac "m=0", force)
    9.13 +  apply (auto simp: scaleR_left_mono)
    9.14 +  apply (rule_tac x="inverse m *\<^sub>R (x-c)" in rev_image_eqI, auto simp: pos_le_divideR_eq le_diff_eq scaleR_left_mono_neg)
    9.15 +  apply (metis diff_le_eq inverse_inverse_eq order.not_eq_order_implies_strict pos_le_divideR_eq positive_imp_inverse_positive)
    9.16 +  apply (rule_tac x="inverse m *\<^sub>R (x-c)" in rev_image_eqI, auto simp: not_le neg_le_divideR_eq diff_le_eq)
    9.17 +  using le_diff_eq scaleR_le_cancel_left_neg
    9.18 +  apply fastforce
    9.19 +  done
    9.20 +
    9.21  lemma dist_0_norm:
    9.22    fixes x :: "'a::real_normed_vector"
    9.23    shows "dist 0 x = norm x"
    10.1 --- a/src/HOL/Topological_Spaces.thy	Sun Nov 22 23:19:43 2015 +0100
    10.2 +++ b/src/HOL/Topological_Spaces.thy	Mon Nov 23 16:57:54 2015 +0000
    10.3 @@ -1484,13 +1484,16 @@
    10.4  lemma continuous_on_const[continuous_intros]: "continuous_on s (\<lambda>x. c)"
    10.5    unfolding continuous_on_def by auto
    10.6  
    10.7 +lemma continuous_on_subset: "continuous_on s f \<Longrightarrow> t \<subseteq> s \<Longrightarrow> continuous_on t f"
    10.8 +  unfolding continuous_on_def by (metis subset_eq tendsto_within_subset)
    10.9 +
   10.10  lemma continuous_on_compose[continuous_intros]:
   10.11    "continuous_on s f \<Longrightarrow> continuous_on (f ` s) g \<Longrightarrow> continuous_on s (g o f)"
   10.12    unfolding continuous_on_topological by simp metis
   10.13  
   10.14  lemma continuous_on_compose2:
   10.15 -  "continuous_on t g \<Longrightarrow> continuous_on s f \<Longrightarrow> t = f ` s \<Longrightarrow> continuous_on s (\<lambda>x. g (f x))"
   10.16 -  using continuous_on_compose[of s f g] by (simp add: comp_def)
   10.17 +  "continuous_on t g \<Longrightarrow> continuous_on s f \<Longrightarrow> f ` s \<subseteq> t \<Longrightarrow> continuous_on s (\<lambda>x. g (f x))"
   10.18 +  using continuous_on_compose[of s f g] continuous_on_subset by (force simp add: comp_def)
   10.19  
   10.20  lemma continuous_on_generate_topology:
   10.21    assumes *: "open = generate_topology X"
   10.22 @@ -1601,9 +1604,6 @@
   10.23  lemma continuous_on_eq_continuous_at: "open s \<Longrightarrow> continuous_on s f \<longleftrightarrow> (\<forall>x\<in>s. isCont f x)"
   10.24    by (simp add: continuous_on_def continuous_at at_within_open[of _ s])
   10.25  
   10.26 -lemma continuous_on_subset: "continuous_on s f \<Longrightarrow> t \<subseteq> s \<Longrightarrow> continuous_on t f"
   10.27 -  unfolding continuous_on_def by (metis subset_eq tendsto_within_subset)
   10.28 -
   10.29  lemma continuous_at_imp_continuous_on: "\<forall>x\<in>s. isCont f x \<Longrightarrow> continuous_on s f"
   10.30    by (auto intro: continuous_at_imp_continuous_at_within simp: continuous_on_eq_continuous_within)
   10.31  
    11.1 --- a/src/HOL/Transcendental.thy	Sun Nov 22 23:19:43 2015 +0100
    11.2 +++ b/src/HOL/Transcendental.thy	Mon Nov 23 16:57:54 2015 +0000
    11.3 @@ -713,7 +713,7 @@
    11.4      using K less_trans zero_less_norm_iff by blast
    11.5    then obtain r::real where r: "norm x < norm r" "norm r < K" "r>0"
    11.6      using K False
    11.7 -    by (auto simp: abs_less_iff add_pos_pos intro: that [of "(norm x + K) / 2"])
    11.8 +    by (auto simp: field_simps abs_less_iff add_pos_pos intro: that [of "(norm x + K) / 2"])
    11.9    have "(\<lambda>n. of_nat n * (x / of_real r) ^ n) ----> 0"
   11.10      using r by (simp add: norm_divide powser_times_n_limit_0 [of "x / of_real r"])
   11.11    then obtain N where N: "\<And>n. n\<ge>N \<Longrightarrow> real_of_nat n * norm x ^ n < r ^ n"
   11.12 @@ -725,7 +725,7 @@
   11.13      apply (rule summable_comparison_test' [of "\<lambda>n. norm(c n * (of_real r) ^ n)" N])
   11.14      apply (rule powser_insidea [OF sm [of "of_real ((r+K)/2)"]])
   11.15      using N r norm_of_real [of "r+K", where 'a = 'a]
   11.16 -    apply (auto simp add: norm_divide norm_mult norm_power )
   11.17 +    apply (auto simp add: norm_divide norm_mult norm_power field_simps)
   11.18      using less_eq_real_def by fastforce
   11.19    then have "summable (\<lambda>n. (of_nat (Suc n) * c(Suc n)) * x ^ Suc n)"
   11.20      using summable_iff_shift [of "\<lambda>n. of_nat n * c n * x ^ n" 1]
   11.21 @@ -754,7 +754,7 @@
   11.22  proof -
   11.23    have K2: "norm ((of_real (norm K) + of_real (norm x)) / 2 :: 'a) < norm K"
   11.24      using K
   11.25 -    apply (auto simp: norm_divide)
   11.26 +    apply (auto simp: norm_divide field_simps)
   11.27      apply (rule le_less_trans [of _ "of_real (norm K) + of_real (norm x)"])
   11.28      apply (auto simp: mult_2_right norm_triangle_mono)
   11.29      done
   11.30 @@ -768,7 +768,7 @@
   11.31      by (blast intro: sm termdiff_converges powser_inside)
   11.32    ultimately show ?thesis
   11.33      apply (rule termdiffs [where K = "of_real (norm x + norm K) / 2"])
   11.34 -    apply (auto simp: algebra_simps)
   11.35 +    apply (auto simp: field_simps)
   11.36      using K
   11.37      apply (simp_all add: of_real_add [symmetric] del: of_real_add)
   11.38      done
   11.39 @@ -990,11 +990,11 @@
   11.40        show "summable (\<lambda> n. \<bar>f n * real (Suc n) * R'^n\<bar>)"
   11.41        proof -
   11.42          have "(R' + R) / 2 < R" and "0 < (R' + R) / 2"
   11.43 -          using \<open>0 < R'\<close> \<open>0 < R\<close> \<open>R' < R\<close> by auto
   11.44 +          using \<open>0 < R'\<close> \<open>0 < R\<close> \<open>R' < R\<close> by (auto simp: field_simps)
   11.45          hence in_Rball: "(R' + R) / 2 \<in> {-R <..< R}"
   11.46            using \<open>R' < R\<close> by auto
   11.47          have "norm R' < norm ((R' + R) / 2)"
   11.48 -          using \<open>0 < R'\<close> \<open>0 < R\<close> \<open>R' < R\<close> by auto
   11.49 +          using \<open>0 < R'\<close> \<open>0 < R\<close> \<open>R' < R\<close> by (auto simp: field_simps)
   11.50          from powser_insidea[OF converges[OF in_Rball] this] show ?thesis
   11.51            by auto
   11.52        qed
   11.53 @@ -1072,7 +1072,7 @@
   11.54      qed
   11.55    } note for_subinterval = this
   11.56    let ?R = "(R + \<bar>x0\<bar>) / 2"
   11.57 -  have "\<bar>x0\<bar> < ?R" using assms by auto
   11.58 +  have "\<bar>x0\<bar> < ?R" using assms by (auto simp: field_simps)
   11.59    hence "- ?R < x0"
   11.60    proof (cases "x0 < 0")
   11.61      case True
   11.62 @@ -1085,7 +1085,7 @@
   11.63      finally show ?thesis .
   11.64    qed
   11.65    hence "0 < ?R" "?R < R" "- ?R < x0" and "x0 < ?R"
   11.66 -    using assms by auto
   11.67 +    using assms by (auto simp: field_simps)
   11.68    from for_subinterval[OF this]
   11.69    show ?thesis .
   11.70  qed
   11.71 @@ -2342,11 +2342,11 @@
   11.72  lemma powr_realpow: "0 < x ==> x powr (real n) = x^n"
   11.73    by (induct n) (simp_all add: ac_simps powr_add of_nat_Suc)
   11.74  
   11.75 -lemma powr_realpow_numeral: "0 < x \<Longrightarrow> x powr (numeral n :: real) = x ^ (numeral n)"
   11.76 +lemma powr_numeral: "0 < x \<Longrightarrow> x powr (numeral n :: real) = x ^ (numeral n)"
   11.77    by (metis of_nat_numeral powr_realpow)
   11.78  
   11.79  lemma powr2_sqrt[simp]: "0 < x \<Longrightarrow> sqrt x powr 2 = x"
   11.80 -by(simp add: powr_realpow_numeral)
   11.81 +by(simp add: powr_numeral)
   11.82  
   11.83  lemma powr_realpow2: "0 <= x ==> 0 < n ==> x^n = (if (x = 0) then 0 else x powr (real n))"
   11.84    apply (case_tac "x = 0", simp, simp)
   11.85 @@ -2378,10 +2378,6 @@
   11.86    using powr_realpow [of x 1]
   11.87    by simp
   11.88  
   11.89 -lemma powr_numeral:
   11.90 -  fixes x::real shows "0 < x \<Longrightarrow> x powr numeral n = x ^ numeral n"
   11.91 -  by (fact powr_realpow_numeral)
   11.92 -
   11.93  lemma powr_neg_one:
   11.94    fixes x::real shows "0 < x \<Longrightarrow> x powr - 1 = 1 / x"
   11.95    using powr_int [of x "- 1"] by simp