src/HOL/Multivariate_Analysis/Cauchy_Integral_Thm.thy

            a' \<in> convex hull {a,b,c} \<and> b' \<in> convex hull {a,b,c} \<and> c' \<in> convex hull {a,b,c} \<and>
            dist a' b' \<le> K/2  \<and>  dist b' c' \<le> K/2  \<and>  dist c' a' \<le> K/2  \<and>
            e * (K/2)^2 \<le> norm(contour_integral(linepath a' b') f + contour_integral(linepath b' c') f + contour_integral(linepath c' a') f)"
 proof -
   note divide_le_eq_numeral1 [simp del]
-  def a' \<equiv> "midpoint b c"
-  def b' \<equiv> "midpoint c a"
-  def c' \<equiv> "midpoint a b"
+  define a' where "a' = midpoint b c"
+  define b' where "b' = midpoint c a"
+  define c' where "c' = midpoint a b"
   have fabc: "continuous_on (closed_segment a b) f" "continuous_on (closed_segment b c) f" "continuous_on (closed_segment c a) f"
     using f continuous_on_subset segments_subset_convex_hull by metis+
   have fcont': "continuous_on (closed_segment c' b') f"
                "continuous_on (closed_segment a' c') f"
                "continuous_on (closed_segment b' a') f"

     by (metis assms holomorphic_on_imp_continuous_on)
   let ?pathint = "\<lambda>x y. contour_integral(linepath x y) f"
   { fix y::complex
     assume fy: "(f has_contour_integral y) (linepath a b +++ linepath b c +++ linepath c a)"
        and ynz: "y \<noteq> 0"
-    def K \<equiv> "1 + max (dist a b) (max (dist b c) (dist c a))"
-    def e \<equiv> "norm y / K^2"
+    define K where "K = 1 + max (dist a b) (max (dist b c) (dist c a))"
+    define e where "e = norm y / K^2"
     have K1: "K \<ge> 1"  by (simp add: K_def max.coboundedI1)
     then have K: "K > 0" by linarith
     have [iff]: "dist a b \<le> K" "dist b c \<le> K" "dist c a \<le> K"
       by (simp_all add: K_def)
     have e: "e > 0"
       unfolding e_def using ynz K1 by simp
-    def At \<equiv> "\<lambda>x y z n. convex hull {x,y,z} \<subseteq> convex hull {a,b,c} \<and>
-                         dist x y \<le> K/2^n \<and> dist y z \<le> K/2^n \<and> dist z x \<le> K/2^n \<and>
-                         norm(?pathint x y + ?pathint y z + ?pathint z x) \<ge> e*(K/2^n)^2"
+    define At where "At x y z n \<longleftrightarrow>
+        convex hull {x,y,z} \<subseteq> convex hull {a,b,c} \<and>
+        dist x y \<le> K/2^n \<and> dist y z \<le> K/2^n \<and> dist z x \<le> K/2^n \<and>
+        norm(?pathint x y + ?pathint y z + ?pathint z x) \<ge> e*(K/2^n)^2"
+      for x y z n
     have At0: "At a b c 0"
       using fy
       by (simp add: At_def e_def has_chain_integral_chain_integral3)
     { fix x y z n
       assume At: "At x y z n"

         by blast
       { fix d1
         assume d1_pos: "0 < d1"
            and d1: "\<And>x x'. \<lbrakk>x\<in>convex hull {a, b, c}; x'\<in>convex hull {a, b, c}; cmod (x' - x) < d1\<rbrakk>
                            \<Longrightarrow> cmod (f x' - f x) < cmod y / (24 * C)"
-        def e      \<equiv> "min 1 (min (d1/(4*C)) ((norm y / 24 / C) / B))"
-        def shrink \<equiv> "\<lambda>x. x - e *\<^sub>R (x - d)"
+        define e where "e = min 1 (min (d1/(4*C)) ((norm y / 24 / C) / B))"
+        define shrink where "shrink x = x - e *\<^sub>R (x - d)" for x
         let ?pathint = "\<lambda>x y. contour_integral(linepath x y) f"
         have e: "0 < e" "e \<le> 1" "e \<le> d1 / (4 * C)" "e \<le> cmod y / 24 / C / B"
           using d1_pos \<open>C>0\<close> \<open>B>0\<close> ynz by (simp_all add: e_def)
         then have eCB: "24 * e * C * B \<le> cmod y"
           using \<open>C>0\<close> \<open>B>0\<close>  by (simp add: field_simps)

 proof -
   have "\<forall>z. \<exists>e. z \<in> path_image p \<longrightarrow> 0 < e \<and> ball z e \<subseteq> s"
     using open_contains_ball os p(2) by blast
   then obtain ee where ee: "\<And>z. z \<in> path_image p \<Longrightarrow> 0 < ee z \<and> ball z (ee z) \<subseteq> s"
     by metis
-  def cover \<equiv> "(\<lambda>z. ball z (ee z/3)) ` (path_image p)"
+  define cover where "cover = (\<lambda>z. ball z (ee z/3)) ` (path_image p)"
   have "compact (path_image p)"
     by (metis p(1) compact_path_image)
   moreover have "path_image p \<subseteq> (\<Union>c\<in>path_image p. ball c (ee c / 3))"
     using ee by auto
   ultimately have "\<exists>D \<subseteq> cover. finite D \<and> path_image p \<subseteq> \<Union>D"

     using D by auto
   have pi: "\<And>i. i \<in> k \<Longrightarrow> p i \<in> path_image p"
     using k  by (auto simp: path_image_def)
   then have eepi: "\<And>i. i \<in> k \<Longrightarrow> 0 < ee((p i))"
     by (metis ee)
-  def e \<equiv> "Min((ee o p) ` k)"
+  define e where "e = Min((ee o p) ` k)"
   have fin_eep: "finite ((ee o p) ` k)"
     using k  by blast
   have enz: "0 < e"
     using ee k  by (simp add: kne e_def Min_gr_iff [OF fin_eep] eepi)
   have "uniformly_continuous_on {0..1} p"

                       (\<forall>f. f holomorphic_on UNIV - {z} \<longrightarrow> contour_integral h2 f = contour_integral h1 f)"
     using contour_integral_nearby_ends [of "UNIV - {z}" \<gamma>] assms by (auto simp: open_delete)
   then obtain h where h: "polynomial_function h \<and> pathstart h = pathstart \<gamma> \<and> pathfinish h = pathfinish \<gamma> \<and>
                           (\<forall>t \<in> {0..1}. norm(h t - \<gamma> t) < d/2)"
     using path_approx_polynomial_function [OF \<open>path \<gamma>\<close>, of "d/2"] d by auto
-  def nn \<equiv> "1/(2* pi*ii) * contour_integral h (\<lambda>w. 1/(w - z))"
+  define nn where "nn = 1/(2* pi*ii) * contour_integral h (\<lambda>w. 1/(w - z))"
   have "\<exists>n. \<forall>e > 0. \<exists>p. valid_path p \<and> z \<notin> path_image p \<and>
                         pathstart p = pathstart \<gamma> \<and>  pathfinish p = pathfinish \<gamma> \<and>
                         (\<forall>t \<in> {0..1}. norm(\<gamma> t - p t) < e) \<and>
                         contour_integral p (\<lambda>w. 1/(w - z)) = 2 * pi * ii * n"
                     (is "\<exists>n. \<forall>e > 0. ?PP e n")

     using z by (auto simp: path_image_def)
   have [simp]: "z \<notin> \<gamma> ` {0..1}"
     using path_image_def z by auto
   have gpd: "\<gamma> piecewise_C1_differentiable_on {0..1}"
     using \<gamma> valid_path_def by blast
-  def r \<equiv> "(w - z) / (\<gamma> 0 - z)"
+  define r where "r = (w - z) / (\<gamma> 0 - z)"
   have [simp]: "r \<noteq> 0"
     using w z by (auto simp: r_def)
   have "Arg r \<le> 2*pi"
     by (simp add: Arg less_eq_real_def)
   also have "... \<le> Im (integral {0..1} (\<lambda>x. vector_derivative \<gamma> (at x) / (\<gamma> x - z)))"

     apply (intro continuous_intros indefinite_integral_continuous winding_number_exp_integral [OF gpd]; simp)
     done
   then obtain t where t:     "t \<in> {0..1}"
                   and eqArg: "Im (integral {0..t} (\<lambda>x. vector_derivative \<gamma> (at x)/(\<gamma> x - z))) = Arg r"
     by blast
-  def i \<equiv> "integral {0..t} (\<lambda>x. vector_derivative \<gamma> (at x) / (\<gamma> x - z))"
+  define i where "i = integral {0..t} (\<lambda>x. vector_derivative \<gamma> (at x) / (\<gamma> x - z))"
   have iArg: "Arg r = Im i"
     using eqArg by (simp add: i_def)
   have gpdt: "\<gamma> piecewise_C1_differentiable_on {0..t}"
     by (metis atLeastAtMost_iff atLeastatMost_subset_iff order_refl piecewise_C1_differentiable_on_subset gpd t)
   have "exp (- i) * (\<gamma> t - z) = \<gamma> 0 - z"

   { assume wnz_12: "\<bar>Re (winding_number \<gamma> z)\<bar> > 1/2"
     have "isCont (winding_number \<gamma>) z"
       by (metis continuous_at_winding_number valid_path_imp_path \<gamma> z)
     then obtain d where "d>0" and d: "\<And>x'. dist x' z < d \<Longrightarrow> dist (winding_number \<gamma> x') (winding_number \<gamma> z) < \<bar>Re(winding_number \<gamma> z)\<bar> - 1/2"
       using continuous_at_eps_delta wnz_12 diff_gt_0_iff_gt by blast
-    def z' \<equiv> "z - (d / (2 * cmod a)) *\<^sub>R a"
+    define z' where "z' = z - (d / (2 * cmod a)) *\<^sub>R a"
     have *: "a \<bullet> z' \<le> b - d / 3 * cmod a"
       unfolding z'_def inner_mult_right' divide_inverse
       apply (simp add: divide_simps algebra_simps dot_square_norm power2_eq_square anz)
       apply (metis \<open>0 < d\<close> add_increasing azb less_eq_real_def mult_nonneg_nonneg mult_right_mono norm_ge_zero norm_numeral)
       done

                       norm(g1 u - k((t1,u))) < d \<and> norm(g2 u - k((t2,u))) < d) \<and>
                       linked_paths atends g1 g2
                       \<longrightarrow> contour_integral g2 f = contour_integral g1 f)))"
     by metis
   note ee_rule = ee [THEN conjunct2, rule_format]
-  def C \<equiv> "(\<lambda>t. ball t (ee t / 3)) ` {0..1}"
+  define C where "C = (\<lambda>t. ball t (ee t / 3)) ` {0..1}"
   have "\<forall>t \<in> C. open t" by (simp add: C_def)
   moreover have "{0..1} \<subseteq> \<Union>C"
     using ee [THEN conjunct1] by (auto simp: C_def dist_norm)
   ultimately obtain C' where C': "C' \<subseteq> C" "finite C'" and C'01: "{0..1} \<subseteq> \<Union>C'"
     by (rule compactE [OF compact_interval])
-  def kk \<equiv> "{t \<in> {0..1}. ball t (ee t / 3) \<in> C'}"
+  define kk where "kk = {t \<in> {0..1}. ball t (ee t / 3) \<in> C'}"
   have kk01: "kk \<subseteq> {0..1}" by (auto simp: kk_def)
-  def e \<equiv> "Min (ee ` kk)"
+  define e where "e = Min (ee ` kk)"
   have C'_eq: "C' = (\<lambda>t. ball t (ee t / 3)) ` kk"
     using C' by (auto simp: kk_def C_def)
   have ee_pos[simp]: "\<And>t. t \<in> {0..1} \<Longrightarrow> ee t > 0"
     by (simp add: kk_def ee)
   moreover have "finite kk"

     have [simp]: "\<bar>r\<bar> = r" using \<open>r > 0\<close> by linarith
     have [simp]: "cmod (complex_of_real t - complex_of_real s) = t-s"
       by (metis "2" abs_of_pos diff_gt_0_iff_gt norm_of_real of_real_diff)
     have "finite (part_circlepath z r s t -` {y} \<inter> {0..1})" if "y \<in> k" for y
     proof -
-      def w \<equiv> "(y - z)/of_real r / exp(ii * of_real s)"
+      define w where "w = (y - z)/of_real r / exp(ii * of_real s)"
       have fin: "finite (of_real -` {z. cmod z \<le> 1 \<and> exp (\<i> * complex_of_real (t - s) * z) = w})"
         apply (rule finite_vimageI [OF finite_bounded_log2])
         using \<open>s < t\<close> apply (auto simp: inj_of_real)
         done
       show ?thesis

   have *: "x \<in> (\<lambda>u. z + (cmod (x - z)) * exp (\<i> * (of_real u * (of_real pi * 2)))) ` {0..1}" for x
   proof (cases "x = z")
     case True then show ?thesis by force
   next
     case False
-    def w \<equiv> "x - z"
+    define w where "w = x - z"
     then have "w \<noteq> 0" by (simp add: False)
     have **: "\<And>t. \<lbrakk>Re w = cos t * cmod w; Im w = sin t * cmod w\<rbrakk> \<Longrightarrow> w = of_real (cmod w) * exp (\<i> * t)"
       using cis_conv_exp complex_eq_iff by auto
     show ?thesis
       apply (rule sincos_total_2pi [of "Re(w/of_real(norm w))" "Im(w/of_real(norm w))"])

     using assms winding_number_circlepath_centre by auto
 next
   case False
   have [simp]: "r > 0"
     using assms le_less_trans norm_ge_zero by blast
-  def r' \<equiv> "norm(w - z)"
+  define r' where "r' = norm(w - z)"
   have "r' < r"
     by (simp add: assms r'_def)
   have disjo: "cball z r' \<inter> sphere z r = {}"
     using \<open>r' < r\<close> by (force simp: cball_def sphere_def)
   have "winding_number(circlepath z r) w = winding_number(circlepath z r) z"

   then show lintg: "l contour_integrable_on \<gamma>"
     apply (simp add: contour_integrable_on)
     apply (blast intro: integrable_uniform_limit_real)
     done
   { fix e::real
-    def B' \<equiv> "B+1"
+    define B' where "B' = B + 1"
     have B': "B' > 0" "B' > B" using  \<open>0 \<le> B\<close> by (auto simp: B'_def)
     assume "0 < e"
     then have ev_no': "\<forall>\<^sub>F n in F. \<forall>x\<in>path_image \<gamma>. 2 * cmod (f n x - l x) < e / B'"
       using ev_no [of "e / B' / 2"] B' by (simp add: field_simps)
     have ie: "integral {0..1::real} (\<lambda>x. e / 2) < e" using \<open>0 < e\<close> by simp

     have *: "cmod ((inverse (x - u) ^ k - inverse (x - w) ^ k) / ((u - w) * k) - inverse (x - w) ^ Suc k)   < e"
             if x: "x \<in> path_image \<gamma>" and "u \<noteq> w" and uwd: "cmod (u - w) < d/2"
                 and uw_less: "cmod (u - w) < e * (d / 2) ^ (k+2) / (1 + real k)"
             for u x
     proof -
-      def ff \<equiv> "\<lambda>n::nat. \<lambda>w. if n = 0 then inverse(x - w)^k
-                              else if n = 1 then k / (x - w)^(Suc k)
-                              else (k * of_real(Suc k)) / (x - w)^(k + 2)"
+      define ff where [abs_def]:
+        "ff n w =
+          (if n = 0 then inverse(x - w)^k
+           else if n = 1 then k / (x - w)^(Suc k)
+           else (k * of_real(Suc k)) / (x - w)^(k + 2))" for n :: nat and w
       have km1: "\<And>z::complex. z \<noteq> 0 \<Longrightarrow> z ^ (k - Suc 0) = z ^ k / z"
         by (simp add: field_simps) (metis Suc_pred \<open>k \<noteq> 0\<close> neq0_conv power_Suc)
       have ff1: "(ff i has_field_derivative ff (Suc i) z) (at z within ball w (d / 2))"
               if "z \<in> ball w (d / 2)" "i \<le> 1" for i z
       proof -

 proof (rule ccontr)
   assume fz: "f z \<noteq> 0"
   with inf [unfolded Lim_at_infinity, rule_format, of "norm(f z)/2"]
   obtain B where B: "\<And>x. B \<le> cmod x \<Longrightarrow> norm (f x) * 2 < cmod (f z)"
     by (auto simp: dist_norm)
-  def R \<equiv> "1 + \<bar>B\<bar> + norm z"
+  define R where "R = 1 + \<bar>B\<bar> + norm z"
   have "R > 0" unfolding R_def 
   proof -
     have "0 \<le> cmod z + \<bar>B\<bar>"
       by (metis (full_types) add_nonneg_nonneg norm_ge_zero real_norm_def)
     then show "0 < 1 + \<bar>B\<bar> + cmod z"

     apply (rule continuous_intros continuous_on_subset [OF contg])+
     using \<open>0 < r\<close> by auto
   have 2: "((\<lambda>u. 1 / (2 * of_real pi * \<i>) * g u / (u - w) ^ 1) has_contour_integral g w) (circlepath z r)"
        if w: "w \<in> ball z r" for w
   proof -
-    def d \<equiv> "(r - norm(w - z))"
+    define d where "d = (r - norm(w - z))"
     have "0 < d"  "d \<le> r" using w by (auto simp: norm_minus_commute d_def dist_norm)
     have dle: "\<And>u. cmod (z - u) = r \<Longrightarrow> d \<le> cmod (u - w)"
       unfolding d_def by (metis add_diff_eq diff_add_cancel norm_diff_ineq norm_minus_commute)
     have ev_int: "\<forall>\<^sub>F n in F. (\<lambda>u. f n u / (u - w)) contour_integrable_on circlepath z r"
       apply (rule eventually_mono [OF cont])

       then have f': "f' n w = 1 / (2 * of_real pi * \<i>) * ?conint (\<lambda>u. f n u / (u - w)\<^sup>2)"
         using DERIV_unique [OF fnd] w by blast
       show ?thesis
         by (simp add: f' Cauchy_contour_integral_circlepath_2 [OF g w] derg [OF w] divide_simps)
     qed
-    def d \<equiv> "(r - norm(w - z))^2"
+    define d where "d = (r - norm(w - z))^2"
     have "d > 0"
       using w by (simp add: dist_commute dist_norm d_def)
     have dle: "\<And>y. r = cmod (z - y) \<Longrightarrow> d \<le> cmod ((y - w)\<^sup>2)"
       apply (simp add: d_def norm_power)
       apply (rule power_mono)

     using has_vector_derivative_polynomial_function [OF \<gamma>] by blast
   then have "bounded(path_image \<gamma>')"
     by (simp add: path_image_def compact_imp_bounded compact_continuous_image continuous_on_polymonial_function)
   then obtain B where "B>0" and B: "\<And>x. x \<in> path_image \<gamma>' \<Longrightarrow> norm x \<le> B"
     using bounded_pos by force
-  def d \<equiv> "\<lambda>z w. if w = z then deriv f z else (f w - f z)/(w - z)"
-  def v \<equiv> "{w. w \<notin> path_image \<gamma> \<and> winding_number \<gamma> w = 0}"
+  define d where [abs_def]: "d z w = (if w = z then deriv f z else (f w - f z)/(w - z))" for z w
+  define v where "v = {w. w \<notin> path_image \<gamma> \<and> winding_number \<gamma> w = 0}"
   have "path \<gamma>" "valid_path \<gamma>" using \<gamma>
     by (auto simp: path_polynomial_function valid_path_polynomial_function)
   then have ov: "open v"
     by (simp add: v_def open_winding_number_levelsets loop)
   have uv_Un: "u \<union> v = UNIV"

     using \<open>valid_path \<gamma>\<close> pasz
     apply (auto simp: u open_delete)
     apply (rule continuous_intros holomorphic_intros continuous_on_subset [OF conf] holomorphic_on_subset [OF holf] |
                 force simp add: that)+
     done
-  def h \<equiv> "\<lambda>z. if z \<in> u then contour_integral \<gamma> (d z) else contour_integral \<gamma> (\<lambda>w. f w/(w - z))"
+  define h where
+    "h z = (if z \<in> u then contour_integral \<gamma> (d z) else contour_integral \<gamma> (\<lambda>w. f w/(w - z)))" for z
   have U: "\<And>z. z \<in> u \<Longrightarrow> ((d z) has_contour_integral h z) \<gamma>"
     apply (simp add: h_def)
     apply (rule has_contour_integral_integral [OF contour_integrable_holomorphic_simple [where s=u]])
     using u pasz \<open>valid_path \<gamma>\<close>
     apply (auto intro: holomorphic_on_imp_continuous_on hol_d)