# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1529927478 -3600
# Node ID 143b4cc8fc7451585b7f2f333023c67e4220f8d9
# Parent  f0f83ce0badd797fed176e5e385949e65114a74a
Renaming Arg -> Arg2pi

diff -r f0f83ce0badd -r 143b4cc8fc74 src/HOL/Analysis/Cauchy_Integral_Theorem.thy
--- a/src/HOL/Analysis/Cauchy_Integral_Theorem.thy	Sun Jun 24 22:13:23 2018 +0200
+++ b/src/HOL/Analysis/Cauchy_Integral_Theorem.thy	Mon Jun 25 12:51:18 2018 +0100
@@ -84,7 +84,7 @@
     shows "\<lbrakk>simple_path \<gamma>; x \<in> inside(path_image \<gamma>)\<rbrakk> \<Longrightarrow> pathfinish \<gamma> = pathstart \<gamma>"
   using arc_simple_path  inside_arc_empty by blast
 
-    
+
 subsection \<open>Piecewise differentiable functions\<close>
 
 definition piecewise_differentiable_on
@@ -466,7 +466,7 @@
 next
   case False
   have *: "\<And>x. finite (S \<inter> {y. m * y + c = x})"
-    using False not_finite_existsD by fastforce 
+    using False not_finite_existsD by fastforce
   show ?thesis
     apply (rule piecewise_C1_differentiable_compose [OF C1_differentiable_imp_piecewise])
     apply (rule * assms derivative_intros | simp add: False vimage_def)+
@@ -601,7 +601,7 @@
   have g1D: "g1 differentiable at x" if "x \<in> {0..1} - insert 1 (( *) 2 ` S)" for x
   proof (rule differentiable_transform_within)
     show "g1 +++ g2 \<circ> ( *) (inverse 2) differentiable at x"
-      using that g12D 
+      using that g12D
       apply (simp only: joinpaths_def)
       by (rule differentiable_chain_at derivative_intros | force)+
     show "\<And>x'. \<lbrakk>dist x' x < dist (x/2) (1/2)\<rbrakk>
@@ -740,7 +740,7 @@
         by (meson C1_differentiable_on_eq \<open>g C1_differentiable_on {0..1} - S\<close> that)
     next
       have "g t\<in>path_image g" using that DiffD1 image_eqI path_image_def by metis
-      then show "f differentiable at (g t)" 
+      then show "f differentiable at (g t)"
         using der[THEN field_differentiable_imp_differentiable] by auto
     qed
   moreover have "continuous_on ({0..1} - S) (\<lambda>x. vector_derivative (f \<circ> g) (at x))"
@@ -767,7 +767,7 @@
     qed
   ultimately have "f \<circ> g C1_differentiable_on {0..1} - S"
     using C1_differentiable_on_eq by blast
-  moreover have "path (f \<circ> g)" 
+  moreover have "path (f \<circ> g)"
     apply (rule path_continuous_image[OF valid_path_imp_path[OF \<open>valid_path g\<close>]])
     using der
     by (simp add: continuous_at_imp_continuous_on field_differentiable_imp_continuous_at)
@@ -898,7 +898,7 @@
        {0..1}"
     using has_integral_affinity01 [where m= "-1" and c=1, OF f [unfolded has_contour_integral_def]]
     by (simp add: has_integral_neg)
-  then show ?thesis 
+  then show ?thesis
     using S
     apply (clarsimp simp: reversepath_def has_contour_integral_def)
     apply (rule_tac S = "(\<lambda>x. 1 - x) ` S" in has_integral_spike_finite)
@@ -2155,7 +2155,7 @@
       done
   } note * = this
   show ?thesis
-    using cd e 
+    using cd e
     apply (simp add: field_differentiable_def has_field_derivative_def has_derivative_within_alt approachable_lt_le2 Ball_def)
     apply (clarify dest!: spec mp)
     using * unfolding dist_norm
@@ -2508,7 +2508,7 @@
             by (blast intro: uv continuous_on_subset [OF contf closed_segment_subset_convex_hull])
           have **: "\<And>f' x' f x::complex. f'*x' - f*x = f'*(x' - x) + x*(f' - f)"
             by (simp add: algebra_simps)
-          have "norm (?pathint (shrink u) (shrink v) - ?pathint u v) 
+          have "norm (?pathint (shrink u) (shrink v) - ?pathint u v)
                 \<le> (B*(norm y /24/C/B)*2*C + (2*C)*(norm y/24/C)) * content (cbox 0 (1::real))"
             apply (rule has_integral_bound
                     [of _ "\<lambda>x. f(linepath (shrink u) (shrink v) x) * (shrink v - shrink u) - f(linepath u v x)*(v - u)"
@@ -2835,7 +2835,7 @@
 qed
 
 lemma contour_integral_convex_primitive:
-  assumes "convex S" "continuous_on S f" 
+  assumes "convex S" "continuous_on S f"
           "\<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)"
   obtains g where "\<And>x. x \<in> S \<Longrightarrow> (g has_field_derivative f x) (at x within S)"
 proof (cases "S={}")
@@ -2846,7 +2846,7 @@
 
 lemma holomorphic_convex_primitive:
   fixes f :: "complex \<Rightarrow> complex"
-  assumes "convex S" "finite K" and contf: "continuous_on S f" 
+  assumes "convex S" "finite K" and contf: "continuous_on S f"
     and fd: "\<And>x. x \<in> interior S - K \<Longrightarrow> f field_differentiable at x"
   obtains g where "\<And>x. x \<in> S \<Longrightarrow> (g has_field_derivative f x) (at x within S)"
 proof (rule contour_integral_convex_primitive [OF \<open>convex S\<close> contf Cauchy_theorem_triangle_cofinite])
@@ -2871,7 +2871,7 @@
 corollary Cauchy_theorem_convex:
     "\<lbrakk>continuous_on S f; convex S; finite K;
       \<And>x. x \<in> interior S - K \<Longrightarrow> f field_differentiable at x;
-      valid_path g; path_image g \<subseteq> S; pathfinish g = pathstart g\<rbrakk> 
+      valid_path g; path_image g \<subseteq> S; pathfinish g = pathstart g\<rbrakk>
      \<Longrightarrow> (f has_contour_integral 0) g"
   by (metis holomorphic_convex_primitive Cauchy_theorem_primitive)
 
@@ -3561,14 +3561,14 @@
   assume "0 < e" and g: "winding_number_prop p z e g n"
   then show "\<exists>r. winding_number_prop (\<lambda>w. p w - z) 0 e r n"
     by (rule_tac x="\<lambda>t. g t - z" in exI)
-       (force simp: winding_number_prop_def contour_integral_integral valid_path_def path_defs  
+       (force simp: winding_number_prop_def contour_integral_integral valid_path_def path_defs
                 vector_derivative_def has_vector_derivative_diff_const piecewise_C1_differentiable_diff C1_differentiable_imp_piecewise)
 next
   fix n e g
   assume "0 < e" and g: "winding_number_prop (\<lambda>w. p w - z) 0 e g n"
   then show "\<exists>r. winding_number_prop p z e r n"
     apply (rule_tac x="\<lambda>t. g t + z" in exI)
-    apply (simp add: winding_number_prop_def contour_integral_integral valid_path_def path_defs 
+    apply (simp add: winding_number_prop_def contour_integral_integral valid_path_def path_defs
         piecewise_C1_differentiable_add vector_derivative_def has_vector_derivative_add_const C1_differentiable_imp_piecewise)
     apply (force simp: algebra_simps)
     done
@@ -3665,7 +3665,7 @@
       by (force simp: ge0)
     show "((\<lambda>x. if 0 < x \<and> x < 1 then ?vd x else 0) has_integral ?int z) (cbox 0 1)"
       by (rule has_integral_spike_interior [OF hi]) simp
-  qed 
+  qed
   then show ?thesis
     by (simp add: Re_winding_number [OF \<gamma>] field_simps)
 qed
@@ -3679,7 +3679,7 @@
   let ?vd = "\<lambda>x. 1 / (\<gamma> x - z) * vector_derivative \<gamma> (at x)"
   let ?int = "\<lambda>z. contour_integral \<gamma> (\<lambda>w. 1 / (w - z))"
   have hi: "(?vd has_integral ?int z) (cbox 0 1)"
-    unfolding box_real 
+    unfolding box_real
     apply (subst has_contour_integral [symmetric])
     using \<gamma> by (simp add: contour_integrable_inversediff has_contour_integral_integral)
   have "e \<le> Im (contour_integral \<gamma> (\<lambda>w. 1 / (w - z)))"
@@ -3782,7 +3782,7 @@
     unfolding integrable_on_def [symmetric]
   proof (rule contour_integral_local_primitive_any [OF piecewise_C1_imp_differentiable [OF \<gamma>]])
     show "\<exists>d h. 0 < d \<and>
-               (\<forall>y. cmod (y - w) < d \<longrightarrow> (h has_field_derivative inverse (y - z))(at y within - {z}))" 
+               (\<forall>y. cmod (y - w) < d \<longrightarrow> (h has_field_derivative inverse (y - z))(at y within - {z}))"
           if "w \<in> - {z}" for w
       apply (rule_tac x="norm(w - z)" in exI)
       using that inverse_eq_divide has_field_derivative_at_within h
@@ -3899,21 +3899,21 @@
   have cont: "continuous_on {0..1}
      (\<lambda>x. Im (integral {0..x} (\<lambda>x. vector_derivative \<gamma> (at x) / (\<gamma> x - z))))"
     by (intro continuous_intros indefinite_integral_continuous_1 winding_number_exp_integral [OF gpd]; simp)
-  have "Arg r \<le> 2*pi"
-    by (simp add: Arg less_eq_real_def)
+  have "Arg2pi r \<le> 2*pi"
+    by (simp add: Arg2pi less_eq_real_def)
   also have "\<dots> \<le> Im (integral {0..1} (\<lambda>x. vector_derivative \<gamma> (at x) / (\<gamma> x - z)))"
     using 1
     apply (simp add: winding_number_valid_path [OF \<gamma> z] contour_integral_integral)
     apply (simp add: Complex.Re_divide field_simps power2_eq_square)
     done
-  finally have "Arg r \<le> Im (integral {0..1} (\<lambda>x. vector_derivative \<gamma> (at x) / (\<gamma> x - z)))" .
-  then have "\<exists>t. t \<in> {0..1} \<and> Im(integral {0..t} (\<lambda>x. vector_derivative \<gamma> (at x)/(\<gamma> x - z))) = Arg r"
-    by (simp add: Arg_ge_0 cont IVT')
+  finally have "Arg2pi r \<le> Im (integral {0..1} (\<lambda>x. vector_derivative \<gamma> (at x) / (\<gamma> x - z)))" .
+  then have "\<exists>t. t \<in> {0..1} \<and> Im(integral {0..t} (\<lambda>x. vector_derivative \<gamma> (at x)/(\<gamma> x - z))) = Arg2pi r"
+    by (simp add: Arg2pi_ge_0 cont IVT')
   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"
+                  and eqArg: "Im (integral {0..t} (\<lambda>x. vector_derivative \<gamma> (at x)/(\<gamma> x - z))) = Arg2pi r"
     by blast
   define i where "i = integral {0..t} (\<lambda>x. vector_derivative \<gamma> (at x) / (\<gamma> x - z))"
-  have iArg: "Arg r = Im i"
+  have iArg: "Arg2pi 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)
@@ -3927,7 +3927,7 @@
     by (simp add: r_def)
   then have "z + complex_of_real (exp (Re i)) * (w - z) / complex_of_real (cmod r) = \<gamma> t"
     apply simp
-    apply (subst Complex_Transcendental.Arg_eq [of r])
+    apply (subst Complex_Transcendental.Arg2pi_eq [of r])
     apply (simp add: iArg)
     using * apply (simp add: exp_eq_polar field_simps)
     done
@@ -4158,7 +4158,7 @@
 lemma winding_number_eq:
      "\<lbrakk>path \<gamma>; pathfinish \<gamma> = pathstart \<gamma>; w \<in> S; z \<in> S; connected S; S \<inter> path_image \<gamma> = {}\<rbrakk>
       \<Longrightarrow> winding_number \<gamma> w = winding_number \<gamma> z"
-  using winding_number_constant by (metis constant_on_def) 
+  using winding_number_constant by (metis constant_on_def)
 
 lemma open_winding_number_levelsets:
   assumes \<gamma>: "path \<gamma>" and loop: "pathfinish \<gamma> = pathstart \<gamma>"
@@ -5329,7 +5329,7 @@
       using \<open>0 \<le> B\<close>  \<open>0 < e\<close> by (simp add: divide_simps)
     have "\<exists>h. (\<forall>x\<in>{0..1}. cmod (l (\<gamma> x) * vector_derivative \<gamma> (at x) - h x) \<le> e) \<and> h integrable_on {0..1}"
     proof (intro exI conjI ballI)
-      show "cmod (l (\<gamma> x) * vector_derivative \<gamma> (at x) - f a (\<gamma> x) * vector_derivative \<gamma> (at x)) \<le> e" 
+      show "cmod (l (\<gamma> x) * vector_derivative \<gamma> (at x) - f a (\<gamma> x) * vector_derivative \<gamma> (at x)) \<le> e"
         if "x \<in> {0..1}" for x
         apply (rule order_trans [OF _ Ble])
         using noleB [OF that] fga [OF that] \<open>0 \<le> B\<close> \<open>0 < e\<close>
@@ -5339,13 +5339,13 @@
     qed (rule inta)
   }
   then show lintg: "l contour_integrable_on \<gamma>"
-    unfolding contour_integrable_on by (metis (mono_tags, lifting)integrable_uniform_limit_real) 
+    unfolding contour_integrable_on by (metis (mono_tags, lifting)integrable_uniform_limit_real)
   { fix e::real
     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 ul_f [unfolded uniform_limit_iff dist_norm, rule_format, of "e / B' / 2"] B' 
+      using ul_f [unfolded uniform_limit_iff dist_norm, rule_format, 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 (f x (\<gamma> t) * vector_derivative \<gamma> (at t) - l (\<gamma> t) * vector_derivative \<gamma> (at t)) \<le> e / 2"
@@ -6024,7 +6024,7 @@
             \<Longrightarrow> f field_differentiable at x" for a b c x
         by (metis cdf Diff_iff Int_iff ball_min_Int subsetD convex_ball e interior_mono interior_subset subset_hull)
       obtain g where "\<And>w. w \<in> ball z (min d e) \<Longrightarrow> (g has_field_derivative f w) (at w within ball z (min d e))"
-        apply (rule contour_integral_convex_primitive 
+        apply (rule contour_integral_convex_primitive
                      [OF convex_ball fde Cauchy_theorem_triangle_cofinite [OF _ K]])
         using cont fd by auto
       then have "f holomorphic_on ball z (min d e)"
@@ -6040,7 +6040,7 @@
 
 lemma no_isolated_singularity':
   fixes z::complex
-  assumes f: "\<And>z. z \<in> K \<Longrightarrow> (f \<longlongrightarrow> f z) (at z within S)" 
+  assumes f: "\<And>z. z \<in> K \<Longrightarrow> (f \<longlongrightarrow> f z) (at z within S)"
       and holf: "f holomorphic_on (S - K)" and S: "open S" and K: "finite K"
     shows "f holomorphic_on S"
 proof (rule no_isolated_singularity[OF _ assms(2-)])
@@ -6050,9 +6050,9 @@
     show "(f \<longlongrightarrow> f z) (at z within S)"
     proof (cases "z \<in> K")
       case False
-      from holf have "continuous_on (S - K) f" 
+      from holf have "continuous_on (S - K) f"
         by (rule holomorphic_on_imp_continuous_on)
-      with z False have "(f \<longlongrightarrow> f z) (at z within (S - K))" 
+      with z False have "(f \<longlongrightarrow> f z) (at z within (S - K))"
         by (simp add: continuous_on_def)
       also from z K S False have "at z within (S - K) = at z within S"
         by (subst (1 2) at_within_open) (auto intro: finite_imp_closed)
@@ -6071,7 +6071,7 @@
   have *: "\<And>x. x \<in> interior S \<Longrightarrow> f field_differentiable at x"
     unfolding holomorphic_on_open [symmetric] field_differentiable_def
     using no_isolated_singularity [where S = "interior S"]
-    by (meson K contf continuous_at_imp_continuous_on continuous_on_interior fcd 
+    by (meson K contf continuous_at_imp_continuous_on continuous_on_interior fcd
           field_differentiable_at_within field_differentiable_def holomorphic_onI
           holomorphic_on_imp_differentiable_at open_interior)
   show ?thesis
@@ -6159,7 +6159,7 @@
 proof -
   \<comment> \<open>Replacing @{term r} and the original (weak) premises with stronger ones\<close>
   obtain r where "r > 0" and holfc: "f holomorphic_on cball z r" and w: "w \<in> ball z r"
-  proof 
+  proof
     have "cball z ((r + dist w z) / 2) \<subseteq> ball z r"
       using w by (simp add: dist_commute real_sum_of_halves subset_eq)
     then show "f holomorphic_on cball z ((r + dist w z) / 2)"
@@ -6169,7 +6169,7 @@
     then show "0 < (r + dist w z) / 2"
       by simp (use zero_le_dist [of w z] in linarith)
   qed (use w in \<open>auto simp: dist_commute\<close>)
-  then have holf: "f holomorphic_on ball z r" 
+  then have holf: "f holomorphic_on ball z r"
     using ball_subset_cball holomorphic_on_subset by blast
   have contf: "continuous_on (cball z r) f"
     by (simp add: holfc holomorphic_on_imp_continuous_on)
@@ -6179,12 +6179,12 @@
     by (metis (no_types) bounded_pos compact_cball compact_continuous_image compact_imp_bounded contf image_eqI)
   obtain k where k: "0 < k" "k \<le> r" and wz_eq: "norm(w - z) = r - k"
              and kle: "\<And>u. norm(u - z) = r \<Longrightarrow> k \<le> norm(u - w)"
-  proof 
+  proof
     show "\<And>u. cmod (u - z) = r \<Longrightarrow> r - dist z w \<le> cmod (u - w)"
       by (metis add_diff_eq diff_add_cancel dist_norm norm_diff_ineq)
   qed (use w in \<open>auto simp: dist_norm norm_minus_commute\<close>)
   have ul: "uniform_limit (sphere z r) (\<lambda>n x. (\<Sum>k<n. (w - z) ^ k * (f x / (x - z) ^ Suc k))) (\<lambda>x. f x / (x - w)) sequentially"
-    unfolding uniform_limit_iff dist_norm 
+    unfolding uniform_limit_iff dist_norm
   proof clarify
     fix e::real
     assume "0 < e"
@@ -6378,7 +6378,7 @@
       apply (auto intro: Cauchy_higher_derivative_integral_circlepath [where k=0, simplified])
       done
     have ul_less: "uniform_limit (sphere z r) (\<lambda>n x. f n x / (x - w)) (\<lambda>x. g x / (x - w)) F"
-      using greater \<open>0 < d\<close> 
+      using greater \<open>0 < d\<close>
       apply (clarsimp simp add: uniform_limit_iff dist_norm norm_divide diff_divide_distrib [symmetric] divide_simps)
       apply (rule_tac e1="e * d" in eventually_mono [OF uniform_limitD [OF ulim]])
        apply (force simp: dist_norm intro: dle mult_left_mono less_le_trans)+
@@ -6389,7 +6389,7 @@
       by (rule contour_integral_uniform_limit_circlepath [OF ev_int ul_less F \<open>0 < r\<close>])
     have f_tends_cig: "((\<lambda>n. 2 * of_real pi * \<i> * f n w) \<longlongrightarrow> contour_integral (circlepath z r) (\<lambda>u. g u / (u - w))) F"
     proof (rule Lim_transform_eventually)
-      show "\<forall>\<^sub>F x in F. contour_integral (circlepath z r) (\<lambda>u. f x u / (u - w)) 
+      show "\<forall>\<^sub>F x in F. contour_integral (circlepath z r) (\<lambda>u. f x u / (u - w))
                      = 2 * of_real pi * \<i> * f x w"
         apply (rule eventually_mono [OF cont contour_integral_unique [OF Cauchy_integral_circlepath]])
         using w\<open>0 < d\<close> d_def by auto
@@ -6507,7 +6507,7 @@
   proof -
     obtain r where "0 < r" and r: "cball z r \<subseteq> S"
                and ul: "uniform_limit (cball z r) f g sequentially"
-      using ulim_g [OF \<open>z \<in> S\<close>] by blast 
+      using ulim_g [OF \<open>z \<in> S\<close>] by blast
     have *: "\<forall>\<^sub>F n in sequentially. continuous_on (cball z r) (f n) \<and> f n holomorphic_on ball z r"
     proof (intro eventuallyI conjI)
       show "continuous_on (cball z r) (f x)" for x
@@ -6537,7 +6537,7 @@
   proof -
     obtain r where "0 < r" and r: "cball z r \<subseteq> S"
                and ul: "uniform_limit (cball z r) f g sequentially"
-      using ulim_g [OF \<open>z \<in> S\<close>] by blast 
+      using ulim_g [OF \<open>z \<in> S\<close>] by blast
     have *: "\<forall>\<^sub>F n in sequentially. continuous_on (cball z r) (f n) \<and>
                                    (\<forall>w \<in> ball z r. ((f n) has_field_derivative (f' n w)) (at w))"
     proof (intro eventuallyI conjI ballI)
@@ -6555,7 +6555,7 @@
 
 
 subsection\<open>On analytic functions defined by a series\<close>
- 
+
 lemma series_and_derivative_comparison:
   fixes S :: "complex set"
   assumes S: "open S"
@@ -6878,7 +6878,7 @@
     have "isCont (\<lambda>z. if z = a then deriv f a else (f z - f a) / (z - a)) x"
             if "dist a x < e" for x
     proof (cases "x=a")
-      case True 
+      case True
       then have "f field_differentiable at a"
         using holfb \<open>0 < e\<close> holomorphic_on_imp_differentiable_at by auto
       with True show ?thesis
@@ -6961,10 +6961,10 @@
              \<Longrightarrow> \<exists>d. 0 < d \<and> (\<forall>w \<in> ball z d - {a}. g w = (w - a) * f w)"
     shows "(\<lambda>z. if z = a then deriv g a else f z - g a/(z - a)) analytic_on S" (is "?F analytic_on S")
   unfolding analytic_on_def
-proof 
+proof
   fix x
   assume "x \<in> S"
-  with g obtain e where "0 < e" and e: "g holomorphic_on ball x e" 
+  with g obtain e where "0 < e" and e: "g holomorphic_on ball x e"
     by (auto simp add: analytic_on_def)
   obtain d where "0 < d" and d: "\<And>w. w \<in> ball x d - {a} \<Longrightarrow> g w = (w - a) * f w"
     using \<open>x \<in> S\<close> eq by blast
@@ -7279,7 +7279,7 @@
       obtain k1 where "k1>0" and k1: "\<And>x'. norm (x' - x) \<le> k1 \<Longrightarrow> norm (deriv f x' - deriv f x) < e"
         using \<open>0 < e\<close> continuous_within_E [OF con_derf [OF \<open>x \<in> U\<close>]]
         by (metis UNIV_I dist_norm)
-      obtain k2 where "k2>0" and k2: "ball x k2 \<subseteq> U" 
+      obtain k2 where "k2>0" and k2: "ball x k2 \<subseteq> U"
         by (blast intro: openE [OF \<open>open U\<close>] \<open>x \<in> U\<close>)
       have neq: "norm ((f z' - f x') / (z' - x') - deriv f x) \<le> e"
                     if "z' \<noteq> x'" and less_k1: "norm (x'-x, z'-x) < k1" and less_k2: "norm (x'-x, z'-x) < k2"
@@ -7518,7 +7518,7 @@
   then have wn0: "\<And>w. w \<notin> S \<Longrightarrow> winding_number p w = 0"
     by (simp add: zero)
   show ?thesis
-    using Cauchy_integral_formula_global_weak [OF S holf z polyp paps ploop wn0] hols 
+    using Cauchy_integral_formula_global_weak [OF S holf z polyp paps ploop wn0] hols
     by (metis wn_eq cint_eq has_contour_integral_eqpath cint_fw cint_eq)
 qed
 
@@ -7579,7 +7579,7 @@
 using valid_path_imp_path by blast
 
 proposition holomorphic_logarithm_exists:
-  assumes A: "convex A" "open A" 
+  assumes A: "convex A" "open A"
       and f: "f holomorphic_on A" "\<And>x. x \<in> A \<Longrightarrow> f x \<noteq> 0"
       and z0: "z0 \<in> A"
     obtains g where "g holomorphic_on A" and "\<And>x. x \<in> A \<Longrightarrow> exp (g x) = f x"
diff -r f0f83ce0badd -r 143b4cc8fc74 src/HOL/Analysis/Complex_Transcendental.thy
--- a/src/HOL/Analysis/Complex_Transcendental.thy	Sun Jun 24 22:13:23 2018 +0200
+++ b/src/HOL/Analysis/Complex_Transcendental.thy	Mon Jun 25 12:51:18 2018 +0100
@@ -60,7 +60,7 @@
     shows "(cmod z)\<^sup>2 < 1 + cmod (1 - z\<^sup>2)"
 proof (cases "Im z = 0 \<or> Re z = 0")
   case True
-  with assms abs_square_less_1 show ?thesis 
+  with assms abs_square_less_1 show ?thesis
     by (force simp add: Re_power2 Im_power2 cmod_def)
 next
   case False
@@ -210,7 +210,7 @@
 
 lemma exp_eq_1: "exp z = 1 \<longleftrightarrow> Re(z) = 0 \<and> (\<exists>n::int. Im(z) = of_int (2 * n) * pi)"
                  (is "?lhs = ?rhs")
-proof 
+proof
   assume "exp z = 1"
   then have "Re z = 0"
     by (metis exp_eq_one_iff norm_exp_eq_Re norm_one)
@@ -770,15 +770,15 @@
 
 subsection\<open>The argument of a complex number\<close>
 
-definition Arg :: "complex \<Rightarrow> real" where
- "Arg z \<equiv> if z = 0 then 0
+definition Arg2pi :: "complex \<Rightarrow> real" where
+ "Arg2pi z \<equiv> if z = 0 then 0
            else THE t. 0 \<le> t \<and> t < 2*pi \<and>
                     z = of_real(norm z) * exp(\<i> * of_real t)"
 
-lemma Arg_0 [simp]: "Arg(0) = 0"
-  by (simp add: Arg_def)
-
-lemma Arg_unique_lemma:
+lemma Arg2pi_0 [simp]: "Arg2pi(0) = 0"
+  by (simp add: Arg2pi_def)
+
+lemma Arg2pi_unique_lemma:
   assumes z:  "z = of_real(norm z) * exp(\<i> * of_real t)"
       and z': "z = of_real(norm z) * exp(\<i> * of_real t')"
       and t:  "0 \<le> t"  "t < 2*pi"
@@ -803,10 +803,10 @@
     by (simp add: n)
 qed
 
-lemma Arg: "0 \<le> Arg z & Arg z < 2*pi & z = of_real(norm z) * exp(\<i> * of_real(Arg z))"
+lemma Arg2pi: "0 \<le> Arg2pi z & Arg2pi z < 2*pi & z = of_real(norm z) * exp(\<i> * of_real(Arg2pi z))"
 proof (cases "z=0")
   case True then show ?thesis
-    by (simp add: Arg_def)
+    by (simp add: Arg2pi_def)
 next
   case False
   obtain t where t: "0 \<le> t" "t < 2*pi"
@@ -819,70 +819,70 @@
     apply (auto simp: exp_Euler sin_of_real cos_of_real divide_simps)
     done
   show ?thesis
-    apply (simp add: Arg_def False)
+    apply (simp add: Arg2pi_def False)
     apply (rule theI [where a=t])
     using t z False
-    apply (auto intro: Arg_unique_lemma)
+    apply (auto intro: Arg2pi_unique_lemma)
     done
 qed
 
 corollary
-  shows Arg_ge_0: "0 \<le> Arg z"
-    and Arg_lt_2pi: "Arg z < 2*pi"
-    and Arg_eq: "z = of_real(norm z) * exp(\<i> * of_real(Arg z))"
-  using Arg by auto
-
-lemma complex_norm_eq_1_exp: "norm z = 1 \<longleftrightarrow> exp(\<i> * of_real (Arg z)) = z"
-  by (metis Arg_eq cis_conv_exp mult.left_neutral norm_cis of_real_1)
-
-lemma Arg_unique: "\<lbrakk>of_real r * exp(\<i> * of_real a) = z; 0 < r; 0 \<le> a; a < 2*pi\<rbrakk> \<Longrightarrow> Arg z = a"
-  by (rule Arg_unique_lemma [OF _ Arg_eq])
-  (use Arg [of z] in \<open>auto simp: norm_mult\<close>)
-
-lemma Arg_minus: "z \<noteq> 0 \<Longrightarrow> Arg (-z) = (if Arg z < pi then Arg z + pi else Arg z - pi)"
-  apply (rule Arg_unique [of "norm z"])
+  shows Arg2pi_ge_0: "0 \<le> Arg2pi z"
+    and Arg2pi_lt_2pi: "Arg2pi z < 2*pi"
+    and Arg2pi_eq: "z = of_real(norm z) * exp(\<i> * of_real(Arg2pi z))"
+  using Arg2pi by auto
+
+lemma complex_norm_eq_1_exp: "norm z = 1 \<longleftrightarrow> exp(\<i> * of_real (Arg2pi z)) = z"
+  by (metis Arg2pi_eq cis_conv_exp mult.left_neutral norm_cis of_real_1)
+
+lemma Arg2pi_unique: "\<lbrakk>of_real r * exp(\<i> * of_real a) = z; 0 < r; 0 \<le> a; a < 2*pi\<rbrakk> \<Longrightarrow> Arg2pi z = a"
+  by (rule Arg2pi_unique_lemma [OF _ Arg2pi_eq])
+  (use Arg2pi [of z] in \<open>auto simp: norm_mult\<close>)
+
+lemma Arg2pi_minus: "z \<noteq> 0 \<Longrightarrow> Arg2pi (-z) = (if Arg2pi z < pi then Arg2pi z + pi else Arg2pi z - pi)"
+  apply (rule Arg2pi_unique [of "norm z"])
   apply (rule complex_eqI)
-  using Arg_ge_0 [of z] Arg_eq [of z] Arg_lt_2pi [of z] 
+  using Arg2pi_ge_0 [of z] Arg2pi_eq [of z] Arg2pi_lt_2pi [of z]
   apply (auto simp: Re_exp Im_exp cos_diff sin_diff cis_conv_exp [symmetric])
   apply (metis Re_rcis Im_rcis rcis_def)+
   done
 
-lemma Arg_times_of_real [simp]:
-  assumes "0 < r" shows "Arg (of_real r * z) = Arg z"
+lemma Arg2pi_times_of_real [simp]:
+  assumes "0 < r" shows "Arg2pi (of_real r * z) = Arg2pi z"
 proof (cases "z=0")
   case False
   show ?thesis
-    by (rule Arg_unique [of "r * norm z"]) (use Arg False assms in auto)
+    by (rule Arg2pi_unique [of "r * norm z"]) (use Arg2pi False assms in auto)
 qed auto
 
-lemma Arg_times_of_real2 [simp]: "0 < r \<Longrightarrow> Arg (z * of_real r) = Arg z"
-  by (metis Arg_times_of_real mult.commute)
-
-lemma Arg_divide_of_real [simp]: "0 < r \<Longrightarrow> Arg (z / of_real r) = Arg z"
-  by (metis Arg_times_of_real2 less_numeral_extra(3) nonzero_eq_divide_eq of_real_eq_0_iff)
-
-lemma Arg_le_pi: "Arg z \<le> pi \<longleftrightarrow> 0 \<le> Im z"
+lemma Arg2pi_times_of_real2 [simp]: "0 < r \<Longrightarrow> Arg2pi (z * of_real r) = Arg2pi z"
+  by (metis Arg2pi_times_of_real mult.commute)
+
+lemma Arg2pi_divide_of_real [simp]: "0 < r \<Longrightarrow> Arg2pi (z / of_real r) = Arg2pi z"
+  by (metis Arg2pi_times_of_real2 less_numeral_extra(3) nonzero_eq_divide_eq of_real_eq_0_iff)
+
+lemma Arg2pi_le_pi: "Arg2pi z \<le> pi \<longleftrightarrow> 0 \<le> Im z"
 proof (cases "z=0")
   case False
-  have "0 \<le> Im z \<longleftrightarrow> 0 \<le> Im (of_real (cmod z) * exp (\<i> * complex_of_real (Arg z)))"
-    by (metis Arg_eq)
-  also have "... = (0 \<le> Im (exp (\<i> * complex_of_real (Arg z))))"
+  have "0 \<le> Im z \<longleftrightarrow> 0 \<le> Im (of_real (cmod z) * exp (\<i> * complex_of_real (Arg2pi z)))"
+    by (metis Arg2pi_eq)
+  also have "... = (0 \<le> Im (exp (\<i> * complex_of_real (Arg2pi z))))"
     using False  by (simp add: zero_le_mult_iff)
-  also have "... \<longleftrightarrow> Arg z \<le> pi"
-    by (simp add: Im_exp) (metis Arg_ge_0 Arg_lt_2pi sin_lt_zero sin_ge_zero not_le)
+  also have "... \<longleftrightarrow> Arg2pi z \<le> pi"
+    by (simp add: Im_exp) (metis Arg2pi_ge_0 Arg2pi_lt_2pi sin_lt_zero sin_ge_zero not_le)
   finally show ?thesis
     by blast
 qed auto
 
-lemma Arg_lt_pi: "0 < Arg z \<and> Arg z < pi \<longleftrightarrow> 0 < Im z"
+lemma Arg2pi_lt_pi: "0 < Arg2pi z \<and> Arg2pi z < pi \<longleftrightarrow> 0 < Im z"
 proof (cases "z=0")
   case False
-  have "0 < Im z \<longleftrightarrow> 0 < Im (of_real (cmod z) * exp (\<i> * complex_of_real (Arg z)))"
-    by (metis Arg_eq)
-  also have "... = (0 < Im (exp (\<i> * complex_of_real (Arg z))))"
+  have "0 < Im z \<longleftrightarrow> 0 < Im (of_real (cmod z) * exp (\<i> * complex_of_real (Arg2pi z)))"
+    by (metis Arg2pi_eq)
+  also have "... = (0 < Im (exp (\<i> * complex_of_real (Arg2pi z))))"
     using False by (simp add: zero_less_mult_iff)
-  also have "... \<longleftrightarrow> 0 < Arg z \<and> Arg z < pi"
-    using Arg_ge_0 Arg_lt_2pi sin_le_zero sin_gt_zero
+  also have "... \<longleftrightarrow> 0 < Arg2pi z \<and> Arg2pi z < pi"
+    using Arg2pi_ge_0 Arg2pi_lt_2pi sin_le_zero sin_gt_zero
     apply (auto simp: Im_exp)
     using le_less apply fastforce
     using not_le by blast
@@ -890,19 +890,19 @@
     by blast
 qed auto
 
-lemma Arg_eq_0: "Arg z = 0 \<longleftrightarrow> z \<in> \<real> \<and> 0 \<le> Re z"
+lemma Arg2pi_eq_0: "Arg2pi z = 0 \<longleftrightarrow> z \<in> \<real> \<and> 0 \<le> Re z"
 proof (cases "z=0")
   case False
-  have "z \<in> \<real> \<and> 0 \<le> Re z \<longleftrightarrow> z \<in> \<real> \<and> 0 \<le> Re (of_real (cmod z) * exp (\<i> * complex_of_real (Arg z)))"
-    by (metis Arg_eq)
-  also have "... \<longleftrightarrow> z \<in> \<real> \<and> 0 \<le> Re (exp (\<i> * complex_of_real (Arg z)))"
+  have "z \<in> \<real> \<and> 0 \<le> Re z \<longleftrightarrow> z \<in> \<real> \<and> 0 \<le> Re (of_real (cmod z) * exp (\<i> * complex_of_real (Arg2pi z)))"
+    by (metis Arg2pi_eq)
+  also have "... \<longleftrightarrow> z \<in> \<real> \<and> 0 \<le> Re (exp (\<i> * complex_of_real (Arg2pi z)))"
     using False  by (simp add: zero_le_mult_iff)
-  also have "... \<longleftrightarrow> Arg z = 0"
+  also have "... \<longleftrightarrow> Arg2pi z = 0"
   proof -
-    have [simp]: "Arg z = 0 \<Longrightarrow> z \<in> \<real>"
-      using Arg_eq [of z] by (auto simp: Reals_def)
-    moreover have "\<lbrakk>z \<in> \<real>; 0 \<le> cos (Arg z)\<rbrakk> \<Longrightarrow> Arg z = 0"
-      by (metis Arg_lt_pi Arg_ge_0 Arg_le_pi cos_pi complex_is_Real_iff leD less_linear less_minus_one_simps(2) minus_minus neg_less_eq_nonneg order_refl)
+    have [simp]: "Arg2pi z = 0 \<Longrightarrow> z \<in> \<real>"
+      using Arg2pi_eq [of z] by (auto simp: Reals_def)
+    moreover have "\<lbrakk>z \<in> \<real>; 0 \<le> cos (Arg2pi z)\<rbrakk> \<Longrightarrow> Arg2pi z = 0"
+      by (metis Arg2pi_lt_pi Arg2pi_ge_0 Arg2pi_le_pi cos_pi complex_is_Real_iff leD less_linear less_minus_one_simps(2) minus_minus neg_less_eq_nonneg order_refl)
     ultimately show ?thesis
       by (auto simp: Re_exp)
   qed
@@ -910,104 +910,104 @@
     by blast
 qed auto
 
-corollary Arg_gt_0:
+corollary Arg2pi_gt_0:
   assumes "z \<in> \<real> \<Longrightarrow> Re z < 0"
-    shows "Arg z > 0"
-  using Arg_eq_0 Arg_ge_0 assms dual_order.strict_iff_order by fastforce
-
-lemma Arg_of_real: "Arg(of_real x) = 0 \<longleftrightarrow> 0 \<le> x"
-  by (simp add: Arg_eq_0)
-
-lemma Arg_eq_pi: "Arg z = pi \<longleftrightarrow> z \<in> \<real> \<and> Re z < 0"
-  using Arg_eq_0 [of "-z"]
-  by (metis Arg_eq_0 Arg_gt_0 Arg_le_pi Arg_lt_pi complex_is_Real_iff dual_order.order_iff_strict not_less pi_neq_zero)
-
-lemma Arg_eq_0_pi: "Arg z = 0 \<or> Arg z = pi \<longleftrightarrow> z \<in> \<real>"
-  using Arg_eq_0 Arg_eq_pi not_le by auto
-
-lemma Arg_inverse: "Arg(inverse z) = (if z \<in> \<real> \<and> 0 \<le> Re z then Arg z else 2*pi - Arg z)"
+    shows "Arg2pi z > 0"
+  using Arg2pi_eq_0 Arg2pi_ge_0 assms dual_order.strict_iff_order by fastforce
+
+lemma Arg2pi_of_real: "Arg2pi(of_real x) = 0 \<longleftrightarrow> 0 \<le> x"
+  by (simp add: Arg2pi_eq_0)
+
+lemma Arg2pi_eq_pi: "Arg2pi z = pi \<longleftrightarrow> z \<in> \<real> \<and> Re z < 0"
+  using Arg2pi_eq_0 [of "-z"]
+  by (metis Arg2pi_eq_0 Arg2pi_gt_0 Arg2pi_le_pi Arg2pi_lt_pi complex_is_Real_iff dual_order.order_iff_strict not_less pi_neq_zero)
+
+lemma Arg2pi_eq_0_pi: "Arg2pi z = 0 \<or> Arg2pi z = pi \<longleftrightarrow> z \<in> \<real>"
+  using Arg2pi_eq_0 Arg2pi_eq_pi not_le by auto
+
+lemma Arg2pi_inverse: "Arg2pi(inverse z) = (if z \<in> \<real> \<and> 0 \<le> Re z then Arg2pi z else 2*pi - Arg2pi z)"
 proof (cases "z=0")
   case False
   show ?thesis
-    apply (rule Arg_unique [of "inverse (norm z)"])
-    using False Arg_ge_0 [of z] Arg_lt_2pi [of z] Arg_eq [of z] Arg_eq_0 [of z] 
+    apply (rule Arg2pi_unique [of "inverse (norm z)"])
+    using False Arg2pi_ge_0 [of z] Arg2pi_lt_2pi [of z] Arg2pi_eq [of z] Arg2pi_eq_0 [of z]
        apply (auto simp: exp_diff field_simps)
     done
 qed auto
 
-lemma Arg_eq_iff:
+lemma Arg2pi_eq_iff:
   assumes "w \<noteq> 0" "z \<noteq> 0"
-     shows "Arg w = Arg z \<longleftrightarrow> (\<exists>x. 0 < x & w = of_real x * z)"
-  using assms Arg_eq [of z] Arg_eq [of w]
+     shows "Arg2pi w = Arg2pi z \<longleftrightarrow> (\<exists>x. 0 < x & w = of_real x * z)"
+  using assms Arg2pi_eq [of z] Arg2pi_eq [of w]
   apply auto
   apply (rule_tac x="norm w / norm z" in exI)
   apply (simp add: divide_simps)
   by (metis mult.commute mult.left_commute)
 
-lemma Arg_inverse_eq_0: "Arg(inverse z) = 0 \<longleftrightarrow> Arg z = 0"
-  by (metis Arg_eq_0 Arg_inverse inverse_inverse_eq)
-
-lemma Arg_divide:
-  assumes "w \<noteq> 0" "z \<noteq> 0" "Arg w \<le> Arg z"
-    shows "Arg(z / w) = Arg z - Arg w"
-  apply (rule Arg_unique [of "norm(z / w)"])
-  using assms Arg_eq Arg_ge_0 [of w] Arg_lt_2pi [of z]
+lemma Arg2pi_inverse_eq_0: "Arg2pi(inverse z) = 0 \<longleftrightarrow> Arg2pi z = 0"
+  by (metis Arg2pi_eq_0 Arg2pi_inverse inverse_inverse_eq)
+
+lemma Arg2pi_divide:
+  assumes "w \<noteq> 0" "z \<noteq> 0" "Arg2pi w \<le> Arg2pi z"
+    shows "Arg2pi(z / w) = Arg2pi z - Arg2pi w"
+  apply (rule Arg2pi_unique [of "norm(z / w)"])
+  using assms Arg2pi_eq Arg2pi_ge_0 [of w] Arg2pi_lt_2pi [of z]
   apply (auto simp: exp_diff norm_divide field_simps)
   done
 
-lemma Arg_le_div_sum:
-  assumes "w \<noteq> 0" "z \<noteq> 0" "Arg w \<le> Arg z"
-    shows "Arg z = Arg w + Arg(z / w)"
-  by (simp add: Arg_divide assms)
-
-lemma Arg_le_div_sum_eq:
+lemma Arg2pi_le_div_sum:
+  assumes "w \<noteq> 0" "z \<noteq> 0" "Arg2pi w \<le> Arg2pi z"
+    shows "Arg2pi z = Arg2pi w + Arg2pi(z / w)"
+  by (simp add: Arg2pi_divide assms)
+
+lemma Arg2pi_le_div_sum_eq:
   assumes "w \<noteq> 0" "z \<noteq> 0"
-    shows "Arg w \<le> Arg z \<longleftrightarrow> Arg z = Arg w + Arg(z / w)"
-  using assms by (auto simp: Arg_ge_0 intro: Arg_le_div_sum)
-
-lemma Arg_diff:
+    shows "Arg2pi w \<le> Arg2pi z \<longleftrightarrow> Arg2pi z = Arg2pi w + Arg2pi(z / w)"
+  using assms by (auto simp: Arg2pi_ge_0 intro: Arg2pi_le_div_sum)
+
+lemma Arg2pi_diff:
   assumes "w \<noteq> 0" "z \<noteq> 0"
-    shows "Arg w - Arg z = (if Arg z \<le> Arg w then Arg(w / z) else Arg(w/z) - 2*pi)"
-  using assms Arg_divide Arg_inverse [of "w/z"]
-  apply (clarsimp simp add: Arg_ge_0 Arg_divide not_le)
-  by (metis Arg_eq_0 less_irrefl minus_diff_eq right_minus_eq)
-
-lemma Arg_add:
+    shows "Arg2pi w - Arg2pi z = (if Arg2pi z \<le> Arg2pi w then Arg2pi(w / z) else Arg2pi(w/z) - 2*pi)"
+  using assms Arg2pi_divide Arg2pi_inverse [of "w/z"]
+  apply (clarsimp simp add: Arg2pi_ge_0 Arg2pi_divide not_le)
+  by (metis Arg2pi_eq_0 less_irrefl minus_diff_eq right_minus_eq)
+
+lemma Arg2pi_add:
   assumes "w \<noteq> 0" "z \<noteq> 0"
-    shows "Arg w + Arg z = (if Arg w + Arg z < 2*pi then Arg(w * z) else Arg(w * z) + 2*pi)"
-  using assms Arg_diff [of "w*z" z] Arg_le_div_sum_eq [of z "w*z"]
-  apply (auto simp: Arg_ge_0 Arg_divide not_le)
-  apply (metis Arg_lt_2pi add.commute)
-  apply (metis (no_types) Arg add.commute diff_0 diff_add_cancel diff_less_eq diff_minus_eq_add not_less)
+    shows "Arg2pi w + Arg2pi z = (if Arg2pi w + Arg2pi z < 2*pi then Arg2pi(w * z) else Arg2pi(w * z) + 2*pi)"
+  using assms Arg2pi_diff [of "w*z" z] Arg2pi_le_div_sum_eq [of z "w*z"]
+  apply (auto simp: Arg2pi_ge_0 Arg2pi_divide not_le)
+  apply (metis Arg2pi_lt_2pi add.commute)
+  apply (metis (no_types) Arg2pi add.commute diff_0 diff_add_cancel diff_less_eq diff_minus_eq_add not_less)
   done
 
-lemma Arg_times:
+lemma Arg2pi_times:
   assumes "w \<noteq> 0" "z \<noteq> 0"
-    shows "Arg (w * z) = (if Arg w + Arg z < 2*pi then Arg w + Arg z
-                            else (Arg w + Arg z) - 2*pi)"
-  using Arg_add [OF assms]
+    shows "Arg2pi (w * z) = (if Arg2pi w + Arg2pi z < 2*pi then Arg2pi w + Arg2pi z
+                            else (Arg2pi w + Arg2pi z) - 2*pi)"
+  using Arg2pi_add [OF assms]
   by auto
 
-lemma Arg_cnj_eq_inverse: "z\<noteq>0 \<Longrightarrow> Arg (cnj z) = Arg (inverse z)"
-  apply (simp add: Arg_eq_iff divide_simps complex_norm_square [symmetric] mult.commute)
+lemma Arg2pi_cnj_eq_inverse: "z\<noteq>0 \<Longrightarrow> Arg2pi (cnj z) = Arg2pi (inverse z)"
+  apply (simp add: Arg2pi_eq_iff divide_simps complex_norm_square [symmetric] mult.commute)
   by (metis of_real_power zero_less_norm_iff zero_less_power)
 
-lemma Arg_cnj: "Arg(cnj z) = (if z \<in> \<real> \<and> 0 \<le> Re z then Arg z else 2*pi - Arg z)"
+lemma Arg2pi_cnj: "Arg2pi(cnj z) = (if z \<in> \<real> \<and> 0 \<le> Re z then Arg2pi z else 2*pi - Arg2pi z)"
 proof (cases "z=0")
   case False
   then show ?thesis
-    by (simp add: Arg_cnj_eq_inverse Arg_inverse)
+    by (simp add: Arg2pi_cnj_eq_inverse Arg2pi_inverse)
 qed auto
 
-lemma Arg_real: "z \<in> \<real> \<Longrightarrow> Arg z = (if 0 \<le> Re z then 0 else pi)"
-  using Arg_eq_0 Arg_eq_0_pi by auto
-
-lemma Arg_exp: "0 \<le> Im z \<Longrightarrow> Im z < 2*pi \<Longrightarrow> Arg(exp z) = Im z"
-  by (rule Arg_unique [of "exp(Re z)"]) (auto simp: exp_eq_polar)
+lemma Arg2pi_real: "z \<in> \<real> \<Longrightarrow> Arg2pi z = (if 0 \<le> Re z then 0 else pi)"
+  using Arg2pi_eq_0 Arg2pi_eq_0_pi by auto
+
+lemma Arg2pi_exp: "0 \<le> Im z \<Longrightarrow> Im z < 2*pi \<Longrightarrow> Arg2pi(exp z) = Im z"
+  by (rule Arg2pi_unique [of "exp(Re z)"]) (auto simp: exp_eq_polar)
 
 lemma complex_split_polar:
   obtains r a::real where "z = complex_of_real r * (cos a + \<i> * sin a)" "0 \<le> r" "0 \<le> a" "a < 2*pi"
-  using Arg cis.ctr cis_conv_exp unfolding Complex_eq by fastforce
+  using Arg2pi cis.ctr cis_conv_exp unfolding Complex_eq by fastforce
 
 lemma Re_Im_le_cmod: "Im w * sin \<phi> + Re w * cos \<phi> \<le> cmod w"
 proof (cases w rule: complex_split_polar)
@@ -1108,10 +1108,10 @@
   have "ln (exp 0) = (0::complex)"
     by (simp add: del: exp_zero)
   then show ?thesis
-    by simp                              
+    by simp
 qed
 
-  
+
 lemma Ln_eq_zero_iff [simp]: "x \<notin> \<real>\<^sub>\<le>\<^sub>0 \<Longrightarrow> ln x = 0 \<longleftrightarrow> x = 1" for x::complex
   by auto (metis exp_Ln exp_zero nonpos_Reals_zero_I)
 
@@ -1214,7 +1214,7 @@
 lemma continuous_on_Ln [continuous_intros]: "(\<And>z. z \<in> S \<Longrightarrow> z \<notin> \<real>\<^sub>\<le>\<^sub>0) \<Longrightarrow> continuous_on S Ln"
   by (simp add: continuous_at_imp_continuous_on continuous_within_Ln)
 
-lemma continuous_on_Ln' [continuous_intros]: 
+lemma continuous_on_Ln' [continuous_intros]:
   "continuous_on S f \<Longrightarrow> (\<And>z. z \<in> S \<Longrightarrow> f z \<notin> \<real>\<^sub>\<le>\<^sub>0) \<Longrightarrow> continuous_on S (\<lambda>x. Ln (f x))"
   by (rule continuous_on_compose2[OF continuous_on_Ln, of "UNIV - nonpos_Reals" S f]) auto
 
@@ -1254,7 +1254,7 @@
       using exp_le \<open>3 \<le> x\<close> x by (simp add: eq) (simp add: power_eq_if divide_simps ln_ge_iff)
   qed
 qed
-    
+
 
 subsection\<open>Quadrant-type results for Ln\<close>
 
@@ -1367,7 +1367,7 @@
       have "\<bar>Im (cnj (Ln z))\<bar> < pi"
         by (simp add: False Im_Ln_less_pi abs_if assms minus_less_iff mpi_less_Im_Ln)
       moreover have "\<bar>Im (Ln (cnj z))\<bar> \<le> pi"
-        by (meson abs_le_iff complex_cnj_zero_iff less_eq_real_def minus_less_iff  False Im_Ln_le_pi mpi_less_Im_Ln) 
+        by (meson abs_le_iff complex_cnj_zero_iff less_eq_real_def minus_less_iff  False Im_Ln_le_pi mpi_less_Im_Ln)
       ultimately show ?thesis
         by simp
     qed
@@ -1375,7 +1375,7 @@
       by simp
     show "exp (cnj (Ln z)) = exp (Ln (cnj z))"
       by (metis False complex_cnj_zero_iff exp_Ln exp_cnj)
-  qed 
+  qed
 qed (use assms in auto)
 
 
@@ -1395,11 +1395,11 @@
       ultimately show ?thesis
         by simp
     qed
-    finally show "\<bar>Im (Ln (inverse z)) - Im (- Ln z)\<bar> < 2 * pi" 
+    finally show "\<bar>Im (Ln (inverse z)) - Im (- Ln z)\<bar> < 2 * pi"
       by simp
     show "exp (Ln (inverse z)) = exp (- Ln z)"
       by (simp add: False exp_minus)
-  qed 
+  qed
 qed (use assms in auto)
 
 lemma Ln_minus1 [simp]: "Ln(-1) = \<i> * pi"
@@ -1529,28 +1529,28 @@
   using assms by (simp add: powr_def)
 
 
-subsection\<open>Relation between Ln and Arg, and hence continuity of Arg\<close>
-
-lemma Arg_Ln:
-  assumes "0 < Arg z" shows "Arg z = Im(Ln(-z)) + pi"
+subsection\<open>Relation between Ln and Arg2pi, and hence continuity of Arg2pi\<close>
+
+lemma Arg2pi_Ln:
+  assumes "0 < Arg2pi z" shows "Arg2pi z = Im(Ln(-z)) + pi"
 proof (cases "z = 0")
   case True
   with assms show ?thesis
     by simp
 next
   case False
-  then have "z / of_real(norm z) = exp(\<i> * of_real(Arg z))"
-    using Arg [of z]
+  then have "z / of_real(norm z) = exp(\<i> * of_real(Arg2pi z))"
+    using Arg2pi [of z]
     by (metis abs_norm_cancel nonzero_mult_div_cancel_left norm_of_real zero_less_norm_iff)
-  then have "- z / of_real(norm z) = exp (\<i> * (of_real (Arg z) - pi))"
+  then have "- z / of_real(norm z) = exp (\<i> * (of_real (Arg2pi z) - pi))"
     using cis_conv_exp cis_pi
     by (auto simp: exp_diff algebra_simps)
-  then have "ln (- z / of_real(norm z)) = ln (exp (\<i> * (of_real (Arg z) - pi)))"
+  then have "ln (- z / of_real(norm z)) = ln (exp (\<i> * (of_real (Arg2pi z) - pi)))"
     by simp
-  also have "... = \<i> * (of_real(Arg z) - pi)"
-    using Arg [of z] assms pi_not_less_zero
+  also have "... = \<i> * (of_real(Arg2pi z) - pi)"
+    using Arg2pi [of z] assms pi_not_less_zero
     by auto
-  finally have "Arg z =  Im (Ln (- z / of_real (cmod z))) + pi"
+  finally have "Arg2pi z =  Im (Ln (- z / of_real (cmod z))) + pi"
     by simp
   also have "... = Im (Ln (-z) - ln (cmod z)) + pi"
     by (metis diff_0_right minus_diff_eq zero_less_norm_iff Ln_divide_of_real False)
@@ -1559,23 +1559,23 @@
   finally show ?thesis .
 qed
 
-lemma continuous_at_Arg:
+lemma continuous_at_Arg2pi:
   assumes "z \<notin> \<real>\<^sub>\<ge>\<^sub>0"
-    shows "continuous (at z) Arg"
+    shows "continuous (at z) Arg2pi"
 proof -
   have *: "isCont (\<lambda>z. Im (Ln (- z)) + pi) z"
     by (rule Complex.isCont_Im isCont_Ln' continuous_intros | simp add: assms complex_is_Real_iff)+
-  have [simp]: "\<And>x. \<lbrakk>Im x \<noteq> 0\<rbrakk> \<Longrightarrow> Im (Ln (- x)) + pi = Arg x"
-    using Arg_Ln Arg_gt_0 complex_is_Real_iff by auto
+  have [simp]: "\<And>x. \<lbrakk>Im x \<noteq> 0\<rbrakk> \<Longrightarrow> Im (Ln (- x)) + pi = Arg2pi x"
+    using Arg2pi_Ln Arg2pi_gt_0 complex_is_Real_iff by auto
   consider "Re z < 0" | "Im z \<noteq> 0" using assms
     using complex_nonneg_Reals_iff not_le by blast
-  then have [simp]: "(\<lambda>z. Im (Ln (- z)) + pi) \<midarrow>z\<rightarrow> Arg z"
-    using "*"  by (simp add: isCont_def) (metis Arg_Ln Arg_gt_0 complex_is_Real_iff)
+  then have [simp]: "(\<lambda>z. Im (Ln (- z)) + pi) \<midarrow>z\<rightarrow> Arg2pi z"
+    using "*"  by (simp add: isCont_def) (metis Arg2pi_Ln Arg2pi_gt_0 complex_is_Real_iff)
   show ?thesis
     unfolding continuous_at
   proof (rule Lim_transform_within_open)
-    show "\<And>x. \<lbrakk>x \<in> - \<real>\<^sub>\<ge>\<^sub>0; x \<noteq> z\<rbrakk> \<Longrightarrow> Im (Ln (- x)) + pi = Arg x"
-      by (auto simp add: Arg_Ln [OF Arg_gt_0] complex_nonneg_Reals_iff)
+    show "\<And>x. \<lbrakk>x \<in> - \<real>\<^sub>\<ge>\<^sub>0; x \<noteq> z\<rbrakk> \<Longrightarrow> Im (Ln (- x)) + pi = Arg2pi x"
+      by (auto simp add: Arg2pi_Ln [OF Arg2pi_gt_0] complex_nonneg_Reals_iff)
   qed (use assms in auto)
 qed
 
@@ -1662,8 +1662,8 @@
        (auto simp: norm_power norm_inverse norm_mult mult_ac simp del: of_nat_add of_nat_Suc)
   also have "norm ((-z)^2 * (-z)^i) * inverse (of_nat (i+2)) \<le> norm ((-z)^2 * (-z)^i) * 1" for i
     by (intro mult_left_mono) (simp_all add: divide_simps)
-  hence "(\<Sum>i. norm (-(z^2) * inverse (of_nat (i+2)) * (-z)^i)) 
-         \<le> (\<Sum>i. norm (-(z^2) * (-z)^i))" 
+  hence "(\<Sum>i. norm (-(z^2) * inverse (of_nat (i+2)) * (-z)^i))
+         \<le> (\<Sum>i. norm (-(z^2) * (-z)^i))"
     using A assms
     apply (simp_all only: norm_power norm_inverse norm_divide norm_mult)
     apply (intro suminf_le summable_mult summable_geometric)
@@ -1678,14 +1678,14 @@
 qed
 
 
-text\<open>Relation between Arg and arctangent in upper halfplane\<close>
-lemma Arg_arctan_upperhalf:
+text\<open>Relation between Arg2pi and arctangent in upper halfplane\<close>
+lemma Arg2pi_arctan_upperhalf:
   assumes "0 < Im z"
-    shows "Arg z = pi/2 - arctan(Re z / Im z)"
+    shows "Arg2pi z = pi/2 - arctan(Re z / Im z)"
 proof (cases "z = 0")
   case False
   show ?thesis
-  proof (rule Arg_unique [of "norm z"])
+  proof (rule Arg2pi_unique [of "norm z"])
     show "(cmod z) * exp (\<i> * (pi / 2 - arctan (Re z / Im z))) = z"
       apply (auto simp: exp_Euler cos_diff sin_diff)
       using assms norm_complex_def [of z, symmetric]
@@ -1695,34 +1695,34 @@
   qed (use False arctan [of "Re z / Im z"] in auto)
 qed (use assms in auto)
 
-lemma Arg_eq_Im_Ln:
+lemma Arg2pi_eq_Im_Ln:
   assumes "0 \<le> Im z" "0 < Re z"
-    shows "Arg z = Im (Ln z)"
+    shows "Arg2pi z = Im (Ln z)"
 proof (cases "Im z = 0")
   case True then show ?thesis
-    using Arg_eq_0 Ln_in_Reals assms(2) complex_is_Real_iff by auto
+    using Arg2pi_eq_0 Ln_in_Reals assms(2) complex_is_Real_iff by auto
 next
   case False
-  then have *: "Arg z > 0"
-    using Arg_gt_0 complex_is_Real_iff by blast
+  then have *: "Arg2pi z > 0"
+    using Arg2pi_gt_0 complex_is_Real_iff by blast
   then have "z \<noteq> 0"
     by auto
   with * assms False show ?thesis
-    by (subst Arg_Ln) (auto simp: Ln_minus)
+    by (subst Arg2pi_Ln) (auto simp: Ln_minus)
 qed
 
-lemma continuous_within_upperhalf_Arg:
+lemma continuous_within_upperhalf_Arg2pi:
   assumes "z \<noteq> 0"
-    shows "continuous (at z within {z. 0 \<le> Im z}) Arg"
+    shows "continuous (at z within {z. 0 \<le> Im z}) Arg2pi"
 proof (cases "z \<in> \<real>\<^sub>\<ge>\<^sub>0")
   case False then show ?thesis
-    using continuous_at_Arg continuous_at_imp_continuous_within by auto
+    using continuous_at_Arg2pi continuous_at_imp_continuous_within by auto
 next
   case True
   then have z: "z \<in> \<real>" "0 < Re z"
     using assms  by (auto simp: complex_nonneg_Reals_iff complex_is_Real_iff complex_neq_0)
-  then have [simp]: "Arg z = 0" "Im (Ln z) = 0"
-    by (auto simp: Arg_eq_0 Im_Ln_eq_0 assms complex_is_Real_iff)
+  then have [simp]: "Arg2pi z = 0" "Im (Ln z) = 0"
+    by (auto simp: Arg2pi_eq_0 Im_Ln_eq_0 assms complex_is_Real_iff)
   show ?thesis
   proof (clarsimp simp add: continuous_within Lim_within dist_norm)
     fix e::real
@@ -1739,50 +1739,50 @@
       then have "0 < Re x"
         using z by linarith
     }
-    then show "\<exists>d>0. \<forall>x. 0 \<le> Im x \<longrightarrow> x \<noteq> z \<and> cmod (x - z) < d \<longrightarrow> \<bar>Arg x\<bar> < e"
+    then show "\<exists>d>0. \<forall>x. 0 \<le> Im x \<longrightarrow> x \<noteq> z \<and> cmod (x - z) < d \<longrightarrow> \<bar>Arg2pi x\<bar> < e"
       apply (rule_tac x="min d (Re z / 2)" in exI)
       using z d
-      apply (auto simp: Arg_eq_Im_Ln)
+      apply (auto simp: Arg2pi_eq_Im_Ln)
       done
   qed
 qed
 
-lemma continuous_on_upperhalf_Arg: "continuous_on ({z. 0 \<le> Im z} - {0}) Arg"
+lemma continuous_on_upperhalf_Arg2pi: "continuous_on ({z. 0 \<le> Im z} - {0}) Arg2pi"
   unfolding continuous_on_eq_continuous_within
-  by (metis DiffE Diff_subset continuous_within_subset continuous_within_upperhalf_Arg insertCI)
-
-lemma open_Arg_less_Int:
+  by (metis DiffE Diff_subset continuous_within_subset continuous_within_upperhalf_Arg2pi insertCI)
+
+lemma open_Arg2pi2pi_less_Int:
   assumes "0 \<le> s" "t \<le> 2*pi"
-    shows "open ({y. s < Arg y} \<inter> {y. Arg y < t})"
+    shows "open ({y. s < Arg2pi y} \<inter> {y. Arg2pi y < t})"
 proof -
-  have 1: "continuous_on (UNIV - \<real>\<^sub>\<ge>\<^sub>0) Arg"
-    using continuous_at_Arg continuous_at_imp_continuous_within
+  have 1: "continuous_on (UNIV - \<real>\<^sub>\<ge>\<^sub>0) Arg2pi"
+    using continuous_at_Arg2pi continuous_at_imp_continuous_within
     by (auto simp: continuous_on_eq_continuous_within)
   have 2: "open (UNIV - \<real>\<^sub>\<ge>\<^sub>0 :: complex set)"  by (simp add: open_Diff)
   have "open ({z. s < z} \<inter> {z. z < t})"
     using open_lessThan [of t] open_greaterThan [of s]
     by (metis greaterThan_def lessThan_def open_Int)
-  moreover have "{y. s < Arg y} \<inter> {y. Arg y < t} \<subseteq> - \<real>\<^sub>\<ge>\<^sub>0"
-    using assms by (auto simp: Arg_real complex_nonneg_Reals_iff complex_is_Real_iff)
+  moreover have "{y. s < Arg2pi y} \<inter> {y. Arg2pi y < t} \<subseteq> - \<real>\<^sub>\<ge>\<^sub>0"
+    using assms by (auto simp: Arg2pi_real complex_nonneg_Reals_iff complex_is_Real_iff)
   ultimately show ?thesis
     using continuous_imp_open_vimage [OF 1 2, of  "{z. Re z > s} \<inter> {z. Re z < t}"]
     by auto
 qed
 
-lemma open_Arg_gt: "open {z. t < Arg z}"
+lemma open_Arg2pi2pi_gt: "open {z. t < Arg2pi z}"
 proof (cases "t < 0")
-  case True then have "{z. t < Arg z} = UNIV"
-    using Arg_ge_0 less_le_trans by auto
+  case True then have "{z. t < Arg2pi z} = UNIV"
+    using Arg2pi_ge_0 less_le_trans by auto
   then show ?thesis
     by simp
 next
   case False then show ?thesis
-    using open_Arg_less_Int [of t "2*pi"] Arg_lt_2pi
+    using open_Arg2pi2pi_less_Int [of t "2*pi"] Arg2pi_lt_2pi
     by auto
 qed
 
-lemma closed_Arg_le: "closed {z. Arg z \<le> t}"
-  using open_Arg_gt [of t]
+lemma closed_Arg2pi2pi_le: "closed {z. Arg2pi z \<le> t}"
+  using open_Arg2pi2pi_gt [of t]
   by (simp add: closed_def Set.Collect_neg_eq [symmetric] not_le)
 
 subsection\<open>Complex Powers\<close>
@@ -1890,7 +1890,7 @@
 declare has_field_derivative_powr[THEN DERIV_chain2, derivative_intros]
 
 lemma has_field_derivative_powr_of_int:
-  fixes z :: complex 
+  fixes z :: complex
   assumes gderiv:"(g has_field_derivative gd) (at z within s)" and "g z\<noteq>0"
   shows "((\<lambda>z. g z powr of_int n) has_field_derivative (n * g z powr (of_int n - 1) * gd)) (at z within s)"
 proof -
@@ -1905,7 +1905,7 @@
       case False
       then have "n-1 \<ge>0" using \<open>n\<ge>0\<close> by auto
       then have "g z powr (of_int (n - 1)) = g z ^ (nat n - 1)"
-        using powr_of_int[OF \<open>g z\<noteq>0\<close>,of "n-1"] by (simp add: nat_diff_distrib') 
+        using powr_of_int[OF \<open>g z\<noteq>0\<close>,of "n-1"] by (simp add: nat_diff_distrib')
       then show ?thesis unfolding dd_def dd'_def by simp
     qed (simp add:dd_def dd'_def)
     then have "((\<lambda>z. g z powr of_int n) has_field_derivative dd) (at z within s)
@@ -1958,7 +1958,7 @@
 qed
 
 lemma field_differentiable_powr_of_int:
-  fixes z :: complex 
+  fixes z :: complex
   assumes gderiv:"g field_differentiable (at z within s)" and "g z\<noteq>0"
   shows "(\<lambda>z. g z powr of_int n) field_differentiable (at z within s)"
 using has_field_derivative_powr_of_int assms(2) field_differentiable_def gderiv by blast
@@ -1972,7 +1972,7 @@
     apply (rule_tac holomorphic_cong)
     using assms(2) by (auto simp add:powr_of_int)
   moreover have "(\<lambda>z. (f z) ^ nat n) holomorphic_on s"
-    using assms(1) by (auto intro:holomorphic_intros)    
+    using assms(1) by (auto intro:holomorphic_intros)
   ultimately show ?thesis by auto
 next
   case False
@@ -1980,7 +1980,7 @@
     apply (rule_tac holomorphic_cong)
     using assms(2) by (auto simp add:powr_of_int power_inverse)
   moreover have "(\<lambda>z. inverse (f z) ^ nat (-n)) holomorphic_on s"
-    using assms by (auto intro!:holomorphic_intros) 
+    using assms by (auto intro!:holomorphic_intros)
   ultimately show ?thesis by auto
 qed
 
@@ -2194,7 +2194,7 @@
     apply (auto simp: norm_divide norm_powr_real divide_simps)
     apply (metis exp_less_mono exp_ln not_le of_nat_0_less_iff)
     done
-  then show "\<exists>no. \<forall>n\<ge>no. norm (Ln (of_nat n) / of_nat n powr s) < e" 
+  then show "\<exists>no. \<forall>n\<ge>no. norm (Ln (of_nat n) / of_nat n powr s) < e"
     by blast
 qed
 
@@ -2504,7 +2504,7 @@
 proof -
   have nz0: "1 + \<i>*z \<noteq> 0"
     using assms
-    by (metis abs_one add_diff_cancel_left' complex_i_mult_minus diff_0 i_squared imaginary_unit.simps 
+    by (metis abs_one add_diff_cancel_left' complex_i_mult_minus diff_0 i_squared imaginary_unit.simps
                 less_asym neg_equal_iff_equal)
   have "z \<noteq> -\<i>" using assms
     by auto
@@ -2847,7 +2847,7 @@
   using arctan_bounds[of "1/5"   4]
         arctan_bounds[of "1/239" 4]
   by (simp_all add: eval_nat_numeral)
-    
+
 corollary pi_gt3: "pi > 3"
   using pi_approx by simp
 
@@ -2987,7 +2987,7 @@
 lemma has_field_derivative_Arcsin:
   assumes "Im z = 0 \<Longrightarrow> \<bar>Re z\<bar> < 1"
     shows "(Arcsin has_field_derivative inverse(cos(Arcsin z))) (at z)"
-proof - 
+proof -
   have "(sin (Arcsin z))\<^sup>2 \<noteq> 1"
     using assms one_minus_z2_notin_nonpos_Reals by force
   then have "cos (Arcsin z) \<noteq> 0"
@@ -3682,8 +3682,8 @@
 lemma homotopic_loops_imp_homotopic_circlemaps:
   assumes "homotopic_loops S p q"
     shows "homotopic_with (\<lambda>h. True) (sphere 0 1) S
-                          (p \<circ> (\<lambda>z. (Arg z / (2 * pi))))
-                          (q \<circ> (\<lambda>z. (Arg z / (2 * pi))))"
+                          (p \<circ> (\<lambda>z. (Arg2pi z / (2 * pi))))
+                          (q \<circ> (\<lambda>z. (Arg2pi z / (2 * pi))))"
 proof -
   obtain h where conth: "continuous_on ({0..1::real} \<times> {0..1}) h"
              and him: "h ` ({0..1} \<times> {0..1}) \<subseteq> S"
@@ -3693,41 +3693,41 @@
     using assms
     by (auto simp: homotopic_loops_def sphere_def homotopic_with_def pathstart_def pathfinish_def)
   define j where "j \<equiv> \<lambda>z. if 0 \<le> Im (snd z)
-                          then h (fst z, Arg (snd z) / (2 * pi))
-                          else h (fst z, 1 - Arg (cnj (snd z)) / (2 * pi))"
-  have Arg_eq: "1 - Arg (cnj y) / (2 * pi) = Arg y / (2 * pi) \<or> Arg y = 0 \<and> Arg (cnj y) = 0" if "cmod y = 1" for y
-    using that Arg_eq_0_pi Arg_eq_pi by (force simp: Arg_cnj divide_simps)
+                          then h (fst z, Arg2pi (snd z) / (2 * pi))
+                          else h (fst z, 1 - Arg2pi (cnj (snd z)) / (2 * pi))"
+  have Arg2pi_eq: "1 - Arg2pi (cnj y) / (2 * pi) = Arg2pi y / (2 * pi) \<or> Arg2pi y = 0 \<and> Arg2pi (cnj y) = 0" if "cmod y = 1" for y
+    using that Arg2pi_eq_0_pi Arg2pi_eq_pi by (force simp: Arg2pi_cnj divide_simps)
   show ?thesis
   proof (simp add: homotopic_with; intro conjI ballI exI)
-    show "continuous_on ({0..1} \<times> sphere 0 1) (\<lambda>w. h (fst w, Arg (snd w) / (2 * pi)))"
+    show "continuous_on ({0..1} \<times> sphere 0 1) (\<lambda>w. h (fst w, Arg2pi (snd w) / (2 * pi)))"
     proof (rule continuous_on_eq)
-      show j: "j x = h (fst x, Arg (snd x) / (2 * pi))" if "x \<in> {0..1} \<times> sphere 0 1" for x
-        using Arg_eq that h01 by (force simp: j_def)
+      show j: "j x = h (fst x, Arg2pi (snd x) / (2 * pi))" if "x \<in> {0..1} \<times> sphere 0 1" for x
+        using Arg2pi_eq that h01 by (force simp: j_def)
       have eq:  "S = S \<inter> (UNIV \<times> {z. 0 \<le> Im z}) \<union> S \<inter> (UNIV \<times> {z. Im z \<le> 0})" for S :: "(real*complex)set"
         by auto
-      have c1: "continuous_on ({0..1} \<times> sphere 0 1 \<inter> UNIV \<times> {z. 0 \<le> Im z}) (\<lambda>x. h (fst x, Arg (snd x) / (2 * pi)))"
-        apply (intro continuous_intros continuous_on_compose2 [OF conth]  continuous_on_compose2 [OF continuous_on_upperhalf_Arg])
-            apply (auto simp: Arg)
-        apply (meson Arg_lt_2pi linear not_le)
+      have c1: "continuous_on ({0..1} \<times> sphere 0 1 \<inter> UNIV \<times> {z. 0 \<le> Im z}) (\<lambda>x. h (fst x, Arg2pi (snd x) / (2 * pi)))"
+        apply (intro continuous_intros continuous_on_compose2 [OF conth]  continuous_on_compose2 [OF continuous_on_upperhalf_Arg2pi])
+            apply (auto simp: Arg2pi)
+        apply (meson Arg2pi_lt_2pi linear not_le)
         done
-      have c2: "continuous_on ({0..1} \<times> sphere 0 1 \<inter> UNIV \<times> {z. Im z \<le> 0}) (\<lambda>x. h (fst x, 1 - Arg (cnj (snd x)) / (2 * pi)))"
-        apply (intro continuous_intros continuous_on_compose2 [OF conth]  continuous_on_compose2 [OF continuous_on_upperhalf_Arg])
-            apply (auto simp: Arg)
-        apply (meson Arg_lt_2pi linear not_le)
+      have c2: "continuous_on ({0..1} \<times> sphere 0 1 \<inter> UNIV \<times> {z. Im z \<le> 0}) (\<lambda>x. h (fst x, 1 - Arg2pi (cnj (snd x)) / (2 * pi)))"
+        apply (intro continuous_intros continuous_on_compose2 [OF conth]  continuous_on_compose2 [OF continuous_on_upperhalf_Arg2pi])
+            apply (auto simp: Arg2pi)
+        apply (meson Arg2pi_lt_2pi linear not_le)
         done
       show "continuous_on ({0..1} \<times> sphere 0 1) j"
         apply (simp add: j_def)
         apply (subst eq)
         apply (rule continuous_on_cases_local)
             apply (simp_all add: eq [symmetric] closedin_closed_Int closed_Times closed_halfspace_Im_le closed_halfspace_Im_ge c1 c2)
-        using Arg_eq h01
+        using Arg2pi_eq h01
         by force
     qed
-    have "(\<lambda>w. h (fst w, Arg (snd w) / (2 * pi))) ` ({0..1} \<times> sphere 0 1) \<subseteq> h ` ({0..1} \<times> {0..1})"
-      by (auto simp: Arg_ge_0 Arg_lt_2pi less_imp_le)
+    have "(\<lambda>w. h (fst w, Arg2pi (snd w) / (2 * pi))) ` ({0..1} \<times> sphere 0 1) \<subseteq> h ` ({0..1} \<times> {0..1})"
+      by (auto simp: Arg2pi_ge_0 Arg2pi_lt_2pi less_imp_le)
     also have "... \<subseteq> S"
       using him by blast
-    finally show "(\<lambda>w. h (fst w, Arg (snd w) / (2 * pi))) ` ({0..1} \<times> sphere 0 1) \<subseteq> S" .
+    finally show "(\<lambda>w. h (fst w, Arg2pi (snd w) / (2 * pi))) ` ({0..1} \<times> sphere 0 1) \<subseteq> S" .
   qed (auto simp: h0 h1)
 qed
 
@@ -3794,7 +3794,7 @@
   assume p: "path p" "path_image p \<subseteq> S" "pathfinish p = pathstart p"
   then have "homotopic_loops S p p"
     by (simp add: homotopic_loops_refl)
-  then obtain a where homp: "homotopic_with (\<lambda>h. True) (sphere 0 1) S (p \<circ> (\<lambda>z. Arg z / (2 * pi))) (\<lambda>x. a)"
+  then obtain a where homp: "homotopic_with (\<lambda>h. True) (sphere 0 1) S (p \<circ> (\<lambda>z. Arg2pi z / (2 * pi))) (\<lambda>x. a)"
     by (metis homotopic_with_imp_subset2 homotopic_loops_imp_homotopic_circlemaps homotopic_with_imp_continuous hom)
   show "\<exists>a. a \<in> S \<and> homotopic_loops S p (linepath a a)"
   proof (intro exI conjI)
@@ -3802,11 +3802,11 @@
       using homotopic_with_imp_subset2 [OF homp]
       by (metis dist_0_norm image_subset_iff mem_sphere norm_one)
     have teq: "\<And>t. \<lbrakk>0 \<le> t; t \<le> 1\<rbrakk>
-               \<Longrightarrow> t = Arg (exp (2 * of_real pi * of_real t * \<i>)) / (2 * pi) \<or> t=1 \<and> Arg (exp (2 * of_real pi * of_real t * \<i>)) = 0"
+               \<Longrightarrow> t = Arg2pi (exp (2 * of_real pi * of_real t * \<i>)) / (2 * pi) \<or> t=1 \<and> Arg2pi (exp (2 * of_real pi * of_real t * \<i>)) = 0"
       apply (rule disjCI)
-      using Arg_of_real [of 1] apply (auto simp: Arg_exp)
+      using Arg2pi_of_real [of 1] apply (auto simp: Arg2pi_exp)
       done
-    have "homotopic_loops S p (p \<circ> (\<lambda>z. Arg z / (2 * pi)) \<circ> exp \<circ> (\<lambda>t. 2 * complex_of_real pi * complex_of_real t * \<i>))"
+    have "homotopic_loops S p (p \<circ> (\<lambda>z. Arg2pi z / (2 * pi)) \<circ> exp \<circ> (\<lambda>t. 2 * complex_of_real pi * complex_of_real t * \<i>))"
       apply (rule homotopic_loops_eq [OF p])
       using p teq apply (fastforce simp: pathfinish_def pathstart_def)
       done
@@ -3855,45 +3855,45 @@
   have "homotopic_loops (path_image \<gamma>) \<gamma> \<gamma>"
     by (simp add: assms homotopic_loops_refl simple_path_imp_path)
   then have hom: "homotopic_with (\<lambda>h. True) (sphere 0 1) (path_image \<gamma>)
-               (\<gamma> \<circ> (\<lambda>z. Arg z / (2*pi))) (\<gamma> \<circ> (\<lambda>z. Arg z / (2*pi)))"
+               (\<gamma> \<circ> (\<lambda>z. Arg2pi z / (2*pi))) (\<gamma> \<circ> (\<lambda>z. Arg2pi z / (2*pi)))"
     by (rule homotopic_loops_imp_homotopic_circlemaps)
-  have "\<exists>g. homeomorphism (sphere 0 1) (path_image \<gamma>) (\<gamma> \<circ> (\<lambda>z. Arg z / (2*pi))) g"
+  have "\<exists>g. homeomorphism (sphere 0 1) (path_image \<gamma>) (\<gamma> \<circ> (\<lambda>z. Arg2pi z / (2*pi))) g"
   proof (rule homeomorphism_compact)
-    show "continuous_on (sphere 0 1) (\<gamma> \<circ> (\<lambda>z. Arg z / (2*pi)))"
+    show "continuous_on (sphere 0 1) (\<gamma> \<circ> (\<lambda>z. Arg2pi z / (2*pi)))"
       using hom homotopic_with_imp_continuous by blast
-    show "inj_on (\<gamma> \<circ> (\<lambda>z. Arg z / (2*pi))) (sphere 0 1)"
+    show "inj_on (\<gamma> \<circ> (\<lambda>z. Arg2pi z / (2*pi))) (sphere 0 1)"
     proof
       fix x y
       assume xy: "x \<in> sphere 0 1" "y \<in> sphere 0 1"
-         and eq: "(\<gamma> \<circ> (\<lambda>z. Arg z / (2*pi))) x = (\<gamma> \<circ> (\<lambda>z. Arg z / (2*pi))) y"
-      then have "(Arg x / (2*pi)) = (Arg y / (2*pi))"
+         and eq: "(\<gamma> \<circ> (\<lambda>z. Arg2pi z / (2*pi))) x = (\<gamma> \<circ> (\<lambda>z. Arg2pi z / (2*pi))) y"
+      then have "(Arg2pi x / (2*pi)) = (Arg2pi y / (2*pi))"
       proof -
-        have "(Arg x / (2*pi)) \<in> {0..1}" "(Arg y / (2*pi)) \<in> {0..1}"
-          using Arg_ge_0 Arg_lt_2pi dual_order.strict_iff_order by fastforce+
+        have "(Arg2pi x / (2*pi)) \<in> {0..1}" "(Arg2pi y / (2*pi)) \<in> {0..1}"
+          using Arg2pi_ge_0 Arg2pi_lt_2pi dual_order.strict_iff_order by fastforce+
         with eq show ?thesis
-          using \<open>simple_path \<gamma>\<close> Arg_lt_2pi unfolding simple_path_def o_def
+          using \<open>simple_path \<gamma>\<close> Arg2pi_lt_2pi unfolding simple_path_def o_def
           by (metis eq_divide_eq_1 not_less_iff_gr_or_eq)
       qed
       with xy show "x = y"
-        by (metis Arg Arg_0 dist_0_norm divide_cancel_right dual_order.strict_iff_order mem_sphere)
+        by (metis Arg2pi Arg2pi_0 dist_0_norm divide_cancel_right dual_order.strict_iff_order mem_sphere)
     qed
-    have "\<And>z. cmod z = 1 \<Longrightarrow> \<exists>x\<in>{0..1}. \<gamma> (Arg z / (2*pi)) = \<gamma> x"
-       by (metis Arg_ge_0 Arg_lt_2pi atLeastAtMost_iff divide_less_eq_1 less_eq_real_def zero_less_mult_iff pi_gt_zero zero_le_divide_iff zero_less_numeral)
-     moreover have "\<exists>z\<in>sphere 0 1. \<gamma> x = \<gamma> (Arg z / (2*pi))" if "0 \<le> x" "x \<le> 1" for x
+    have "\<And>z. cmod z = 1 \<Longrightarrow> \<exists>x\<in>{0..1}. \<gamma> (Arg2pi z / (2*pi)) = \<gamma> x"
+       by (metis Arg2pi_ge_0 Arg2pi_lt_2pi atLeastAtMost_iff divide_less_eq_1 less_eq_real_def zero_less_mult_iff pi_gt_zero zero_le_divide_iff zero_less_numeral)
+     moreover have "\<exists>z\<in>sphere 0 1. \<gamma> x = \<gamma> (Arg2pi z / (2*pi))" if "0 \<le> x" "x \<le> 1" for x
      proof (cases "x=1")
        case True
        then show ?thesis
          apply (rule_tac x=1 in bexI)
-         apply (metis loop Arg_of_real divide_eq_0_iff of_real_1 pathfinish_def pathstart_def \<open>0 \<le> x\<close>, auto)
+         apply (metis loop Arg2pi_of_real divide_eq_0_iff of_real_1 pathfinish_def pathstart_def \<open>0 \<le> x\<close>, auto)
          done
      next
        case False
-       then have *: "(Arg (exp (\<i>*(2* of_real pi* of_real x))) / (2*pi)) = x"
-         using that by (auto simp: Arg_exp divide_simps)
+       then have *: "(Arg2pi (exp (\<i>*(2* of_real pi* of_real x))) / (2*pi)) = x"
+         using that by (auto simp: Arg2pi_exp divide_simps)
        show ?thesis
          by (rule_tac x="exp(\<i> * of_real(2*pi*x))" in bexI) (auto simp: *)
     qed
-    ultimately show "(\<gamma> \<circ> (\<lambda>z. Arg z / (2*pi))) ` sphere 0 1 = path_image \<gamma>"
+    ultimately show "(\<gamma> \<circ> (\<lambda>z. Arg2pi z / (2*pi))) ` sphere 0 1 = path_image \<gamma>"
       by (auto simp: path_image_def image_iff)
     qed auto
     then have "path_image \<gamma> homeomorphic sphere (0::complex) 1"