# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1457366222 0
# Node ID 6855b348e828081db1614200ea3f9c418cc904f6
# Parent  bc25f3916a99c0369ace28fb12e4987487d83884
complex_differentiable -> field_differentiable, etc. (making these theorems also available for type real)

diff -r bc25f3916a99 -r 6855b348e828 src/HOL/Multivariate_Analysis/Cauchy_Integral_Thm.thy
--- a/src/HOL/Multivariate_Analysis/Cauchy_Integral_Thm.thy	Mon Mar 07 14:34:45 2016 +0000
+++ b/src/HOL/Multivariate_Analysis/Cauchy_Integral_Thm.thy	Mon Mar 07 15:57:02 2016 +0000
@@ -208,7 +208,7 @@
 the Riemann or Lebesgue theory (but in common with a simple notion based on antiderivatives), this
 can integrate all derivatives.''
 
-"Formalizing basic complex analysis." From Insight to Proof: Festschrift in Honour of Andrzej Trybulec. 
+"Formalizing basic complex analysis." From Insight to Proof: Festschrift in Honour of Andrzej Trybulec.
 Studies in Logic, Grammar and Rhetoric 10.23 (2007): 151-165.
 
 And indeed he does not assume that his derivatives are continuous, but the penalty is unreasonably
@@ -645,7 +645,7 @@
   where "contour_integral g f \<equiv> @i. (f has_contour_integral i) g \<or> ~ f contour_integrable_on g \<and> i=0"
 
 lemma not_integrable_contour_integral: "~ f contour_integrable_on g \<Longrightarrow> contour_integral g f = 0"
-  unfolding contour_integrable_on_def contour_integral_def by blast 
+  unfolding contour_integrable_on_def contour_integral_def by blast
 
 lemma contour_integral_unique: "(f has_contour_integral i) g \<Longrightarrow> contour_integral g f = i"
   apply (simp add: contour_integral_def has_contour_integral_def contour_integrable_on_def)
@@ -1113,7 +1113,7 @@
 lemma contour_integral_shiftpath:
   assumes "valid_path g" "pathfinish g = pathstart g" "a \<in> {0..1}"
     shows "contour_integral (shiftpath a g) f = contour_integral g f"
-   using assms   
+   using assms
    by (simp add: contour_integral_def contour_integrable_on_def has_contour_integral_shiftpath_eq)
 
 
@@ -1398,7 +1398,7 @@
   have cfg: "continuous_on {a..b} (\<lambda>x. f (g x))"
     apply (rule continuous_on_compose [OF cg, unfolded o_def])
     using assms
-    apply (metis complex_differentiable_def complex_differentiable_imp_continuous_at continuous_on_eq_continuous_within continuous_on_subset image_subset_iff)
+    apply (metis field_differentiable_def field_differentiable_imp_continuous_at continuous_on_eq_continuous_within continuous_on_subset image_subset_iff)
     done
   { fix x::real
     assume a: "a < x" and b: "x < b" and xk: "x \<notin> k"
@@ -2034,7 +2034,7 @@
 lemma holomorphic_point_small_triangle:
   assumes x: "x \<in> s"
       and f: "continuous_on s f"
-      and cd: "f complex_differentiable (at x within s)"
+      and cd: "f field_differentiable (at x within s)"
       and e: "0 < e"
     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>
               x \<in> convex hull {a,b,c} \<and> convex hull {a,b,c} \<subseteq> s
@@ -2089,7 +2089,7 @@
   } note * = this
   show ?thesis
     using cd e
-    apply (simp add: complex_differentiable_def has_field_derivative_def has_derivative_within_alt approachable_lt_le2 Ball_def)
+    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 *
     apply (simp add: dist_norm, blast)
@@ -2204,7 +2204,7 @@
     then obtain x where x: "\<And>n. x \<in> convex hull {fa n, fb n, fc n}" by auto
     then have xin: "x \<in> convex hull {a,b,c}"
       using assms f0 by blast
-    then have fx: "f complex_differentiable at x within (convex hull {a,b,c})"
+    then have fx: "f field_differentiable at x within (convex hull {a,b,c})"
       using assms holomorphic_on_def by blast
     { fix k n
       assume k: "0 < k"
@@ -2506,7 +2506,7 @@
 lemma Cauchy_theorem_triangle_cofinite:
   assumes "continuous_on (convex hull {a,b,c}) f"
       and "finite s"
-      and "(\<And>x. x \<in> interior(convex hull {a,b,c}) - s \<Longrightarrow> f complex_differentiable (at x))"
+      and "(\<And>x. x \<in> interior(convex hull {a,b,c}) - s \<Longrightarrow> f field_differentiable (at x))"
      shows "(f has_contour_integral 0) (linepath a b +++ linepath b c +++ linepath c a)"
 using assms
 proof (induction "card s" arbitrary: a b c s rule: less_induct)
@@ -2514,7 +2514,7 @@
   show ?case
   proof (cases "s={}")
     case True with less show ?thesis
-      by (fastforce simp: holomorphic_on_def complex_differentiable_at_within
+      by (fastforce simp: holomorphic_on_def field_differentiable_at_within
                     Cauchy_theorem_triangle_interior)
   next
     case False
@@ -2682,7 +2682,7 @@
   assumes contf: "continuous_on s f"
       and s: "starlike s" and os: "open s"
       and k: "finite k"
-      and fcd: "\<And>x. x \<in> s - k \<Longrightarrow> f complex_differentiable at x"
+      and fcd: "\<And>x. x \<in> s - k \<Longrightarrow> f field_differentiable at x"
     shows "\<exists>g. \<forall>x \<in> s. (g has_field_derivative f x) (at x)"
 proof -
   obtain a where a: "a\<in>s" and a_cs: "\<And>x. x\<in>s \<Longrightarrow> closed_segment a x \<subseteq> s"
@@ -2709,7 +2709,7 @@
 
 lemma Cauchy_theorem_starlike:
  "\<lbrakk>open s; starlike s; finite k; continuous_on s f;
-   \<And>x. x \<in> s - k \<Longrightarrow> f complex_differentiable at x;
+   \<And>x. x \<in> s - k \<Longrightarrow> f field_differentiable at x;
    valid_path g; path_image g \<subseteq> s; pathfinish g = pathstart g\<rbrakk>
    \<Longrightarrow> (f has_contour_integral 0)  g"
   by (metis holomorphic_starlike_primitive Cauchy_theorem_primitive at_within_open)
@@ -2800,7 +2800,7 @@
   fixes f :: "complex \<Rightarrow> complex"
   shows
   "\<lbrakk>convex s; finite k; continuous_on s f;
-    \<And>x. x \<in> interior s - k \<Longrightarrow> f complex_differentiable at x\<rbrakk>
+    \<And>x. x \<in> interior s - k \<Longrightarrow> f field_differentiable at x\<rbrakk>
    \<Longrightarrow> \<exists>g. \<forall>x \<in> s. (g has_field_derivative f x) (at x within s)"
 apply (rule contour_integral_convex_primitive [OF _ _ Cauchy_theorem_triangle_cofinite])
 prefer 3
@@ -2810,7 +2810,7 @@
 
 lemma Cauchy_theorem_convex:
     "\<lbrakk>continuous_on s f; convex s; finite k;
-      \<And>x. x \<in> interior s - k \<Longrightarrow> f complex_differentiable at x;
+      \<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> \<Longrightarrow> (f has_contour_integral 0) g"
   by (metis holomorphic_convex_primitive Cauchy_theorem_primitive)
@@ -2828,7 +2828,7 @@
 text\<open>In particular for a disc\<close>
 lemma Cauchy_theorem_disc:
     "\<lbrakk>finite k; continuous_on (cball a e) f;
-      \<And>x. x \<in> ball a e - k \<Longrightarrow> f complex_differentiable at x;
+      \<And>x. x \<in> ball a e - k \<Longrightarrow> f field_differentiable at x;
      valid_path g; path_image g \<subseteq> cball a e;
      pathfinish g = pathstart g\<rbrakk> \<Longrightarrow> (f has_contour_integral 0) g"
   apply (rule Cauchy_theorem_convex)
@@ -2914,7 +2914,7 @@
       and os: "open s"
       and k: "finite k"
       and g: "valid_path g" "path_image g \<subseteq> s"
-      and fcd: "\<And>x. x \<in> s - k \<Longrightarrow> f complex_differentiable at x"
+      and fcd: "\<And>x. x \<in> s - k \<Longrightarrow> f field_differentiable at x"
     shows "f contour_integrable_on g"
 proof -
   { fix z
@@ -2944,7 +2944,7 @@
     shows "f contour_integrable_on g"
   apply (rule contour_integrable_holomorphic [OF _ os Finite_Set.finite.emptyI g])
   apply (simp add: fh holomorphic_on_imp_continuous_on)
-  using fh  by (simp add: complex_differentiable_def holomorphic_on_open os)
+  using fh  by (simp add: field_differentiable_def holomorphic_on_open os)
 
 lemma continuous_on_inversediff:
   fixes z:: "'a::real_normed_field" shows "z \<notin> s \<Longrightarrow> continuous_on s (\<lambda>w. 1 / (w - z))"
@@ -3819,7 +3819,7 @@
       by (auto simp: intro!: derivative_eq_intros)
     ultimately have "\<exists>h. \<forall>y. norm(y - w) < norm(w - z) \<longrightarrow> (h has_field_derivative 1/(y - z)) (at y)"
       using holomorphic_convex_primitive [of "ball w (norm(w - z))" "{}" "\<lambda>w. 1/(w - z)"]
-      by (simp add: complex_differentiable_def Ball_def dist_norm at_within_open_NO_MATCH norm_minus_commute)
+      by (simp add: field_differentiable_def Ball_def dist_norm at_within_open_NO_MATCH norm_minus_commute)
   }
   then obtain h where h: "\<And>w y. w \<noteq> z \<Longrightarrow> norm(y - w) < norm(w - z) \<Longrightarrow> (h w has_field_derivative 1/(y - z)) (at y)"
     by meson
@@ -3840,8 +3840,8 @@
     assume t: "t \<in> {a..b}"
     have cball: "continuous_on (ball (\<gamma> t) (dist (\<gamma> t) z)) (\<lambda>x. inverse (x - z))"
         using z by (auto intro!: continuous_intros simp: dist_norm)
-    have icd: "\<And>x. cmod (\<gamma> t - x) < cmod (\<gamma> t - z) \<Longrightarrow> (\<lambda>w. inverse (w - z)) complex_differentiable at x"
-      unfolding complex_differentiable_def by (force simp: intro!: derivative_eq_intros)
+    have icd: "\<And>x. cmod (\<gamma> t - x) < cmod (\<gamma> t - z) \<Longrightarrow> (\<lambda>w. inverse (w - z)) field_differentiable at x"
+      unfolding field_differentiable_def by (force simp: intro!: derivative_eq_intros)
     obtain h where h: "\<And>x. cmod (\<gamma> t - x) < cmod (\<gamma> t - z) \<Longrightarrow>
                        (h has_field_derivative inverse (x - z)) (at x within {y. cmod (\<gamma> t - y) < cmod (\<gamma> t - z)})"
       using holomorphic_convex_primitive [where f = "\<lambda>w. inverse(w - z)", OF convex_ball finite.emptyI cball icd]
@@ -4492,13 +4492,13 @@
 
 lemma Cauchy_integral_formula_weak:
     assumes s: "convex s" and "finite k" and conf: "continuous_on s f"
-        and fcd: "(\<And>x. x \<in> interior s - k \<Longrightarrow> f complex_differentiable at x)"
+        and fcd: "(\<And>x. x \<in> interior s - k \<Longrightarrow> f field_differentiable at x)"
         and z: "z \<in> interior s - k" and vpg: "valid_path \<gamma>"
         and pasz: "path_image \<gamma> \<subseteq> s - {z}" and loop: "pathfinish \<gamma> = pathstart \<gamma>"
       shows "((\<lambda>w. f w / (w - z)) has_contour_integral (2*pi * ii * winding_number \<gamma> z * f z)) \<gamma>"
 proof -
   obtain f' where f': "(f has_field_derivative f') (at z)"
-    using fcd [OF z] by (auto simp: complex_differentiable_def)
+    using fcd [OF z] by (auto simp: field_differentiable_def)
   have pas: "path_image \<gamma> \<subseteq> s" and znotin: "z \<notin> path_image \<gamma>" using pasz by blast+
   have c: "continuous (at x within s) (\<lambda>w. if w = z then f' else (f w - f z) / (w - z))" if "x \<in> s" for x
   proof (cases "x = z")
@@ -4525,7 +4525,7 @@
     apply (rule Cauchy_theorem_convex [OF _ s fink' _ vpg pas loop])
     using c apply (force simp: continuous_on_eq_continuous_within)
     apply (rename_tac w)
-    apply (rule_tac d="dist w z" and f = "\<lambda>w. (f w - f z)/(w - z)" in complex_differentiable_transform_within)
+    apply (rule_tac d="dist w z" and f = "\<lambda>w. (f w - f z)/(w - z)" in field_differentiable_transform_within)
     apply (simp_all add: dist_pos_lt dist_commute)
     apply (metis less_irrefl)
     apply (rule derivative_intros fcd | simp)+
@@ -5675,7 +5675,7 @@
       using open_contains_cball \<open>z \<in> s\<close> \<open>open s\<close> by blast
     then have holf_cball: "f holomorphic_on cball z r"
       apply (simp add: holomorphic_on_def)
-      using complex_differentiable_at_within complex_differentiable_def fder by blast
+      using field_differentiable_at_within field_differentiable_def fder by blast
     then have "continuous_on (path_image (circlepath z r)) f"
       using \<open>r > 0\<close> by (force elim: holomorphic_on_subset [THEN holomorphic_on_imp_continuous_on])
     then have contfpi: "continuous_on (path_image (circlepath z r)) (\<lambda>x. 1/(2 * of_real pi*ii) * f x)"
@@ -5715,7 +5715,7 @@
 
 lemma holomorphic_deriv [holomorphic_intros]:
     "\<lbrakk>f holomorphic_on s; open s\<rbrakk> \<Longrightarrow> (deriv f) holomorphic_on s"
-by (metis DERIV_deriv_iff_complex_differentiable at_within_open derivative_is_holomorphic holomorphic_on_def)
+by (metis DERIV_deriv_iff_field_differentiable at_within_open derivative_is_holomorphic holomorphic_on_def)
 
 lemma analytic_deriv: "f analytic_on s \<Longrightarrow> (deriv f) analytic_on s"
   using analytic_on_holomorphic holomorphic_deriv by auto
@@ -5729,7 +5729,7 @@
 lemma has_field_derivative_higher_deriv:
      "\<lbrakk>f holomorphic_on s; open s; x \<in> s\<rbrakk>
       \<Longrightarrow> ((deriv ^^ n) f has_field_derivative (deriv ^^ (Suc n)) f x) (at x)"
-by (metis (no_types, hide_lams) DERIV_deriv_iff_complex_differentiable at_within_open comp_apply
+by (metis (no_types, hide_lams) DERIV_deriv_iff_field_differentiable at_within_open comp_apply
          funpow.simps(2) holomorphic_higher_deriv holomorphic_on_def)
 
 
@@ -5968,7 +5968,7 @@
     apply (simp add: Suc.IH)
     done
   also have "... = u^n * deriv (\<lambda>z. (deriv ^^ n) f (u * z)) z"
-    apply (rule complex_derivative_cmult)
+    apply (rule deriv_cmult)
     apply (rule analytic_on_imp_differentiable_at [OF _ Suc.prems])
     apply (rule analytic_on_compose_gen [where g="(deriv ^^ n) f" and t=t, unfolded o_def])
     apply (simp add: analytic_on_linear)
@@ -5978,7 +5978,7 @@
   also have "... = u * u ^ n * deriv ((deriv ^^ n) f) (u * z)"
       apply (subst complex_derivative_chain [where g = "(deriv ^^ n) f" and f = "op*u", unfolded o_def])
       apply (rule derivative_intros)
-      using Suc.prems complex_differentiable_def f fg has_field_derivative_higher_deriv t apply blast
+      using Suc.prems field_differentiable_def f fg has_field_derivative_higher_deriv t apply blast
       apply (simp add: deriv_linear)
       done
   finally show ?case
@@ -6030,8 +6030,8 @@
     shows "f holomorphic_on s"
 proof -
   { fix z
-    assume "z \<in> s" and cdf: "\<And>x. x\<in>s - k \<Longrightarrow> f complex_differentiable at x"
-    have "f complex_differentiable at z"
+    assume "z \<in> s" and cdf: "\<And>x. x\<in>s - k \<Longrightarrow> f field_differentiable at x"
+    have "f field_differentiable at z"
     proof (cases "z \<in> k")
       case False then show ?thesis by (blast intro: cdf \<open>z \<in> s\<close>)
     next
@@ -6059,19 +6059,19 @@
     qed
   }
   with holf s k show ?thesis
-    by (simp add: holomorphic_on_open open_Diff finite_imp_closed complex_differentiable_def [symmetric])
+    by (simp add: holomorphic_on_open open_Diff finite_imp_closed field_differentiable_def [symmetric])
 qed
 
 proposition Cauchy_integral_formula_convex:
     assumes s: "convex s" and k: "finite k" and contf: "continuous_on s f"
-        and fcd: "(\<And>x. x \<in> interior s - k \<Longrightarrow> f complex_differentiable at x)"
+        and fcd: "(\<And>x. x \<in> interior s - k \<Longrightarrow> f field_differentiable at x)"
         and z: "z \<in> interior s" and vpg: "valid_path \<gamma>"
         and pasz: "path_image \<gamma> \<subseteq> s - {z}" and loop: "pathfinish \<gamma> = pathstart \<gamma>"
       shows "((\<lambda>w. f w / (w - z)) has_contour_integral (2*pi * ii * winding_number \<gamma> z * f z)) \<gamma>"
   apply (rule Cauchy_integral_formula_weak [OF s finite.emptyI contf])
-  apply (simp add: holomorphic_on_open [symmetric] complex_differentiable_def)
+  apply (simp add: holomorphic_on_open [symmetric] field_differentiable_def)
   using no_isolated_singularity [where s = "interior s"]
-  apply (metis k contf fcd holomorphic_on_open complex_differentiable_def continuous_on_subset
+  apply (metis k contf fcd holomorphic_on_open field_differentiable_def continuous_on_subset
                has_field_derivative_at_within holomorphic_on_def interior_subset open_interior)
   using assms
   apply auto
@@ -6103,8 +6103,8 @@
     by (rule contour_integral_unique)
   have "\<And>n. ((deriv ^^ n) f has_field_derivative deriv ((deriv ^^ n) f) w) (at w)"
     using Suc.prems assms has_field_derivative_higher_deriv by auto
-  then have dnf_diff: "\<And>n. (deriv ^^ n) f complex_differentiable (at w)"
-    by (force simp add: complex_differentiable_def)
+  then have dnf_diff: "\<And>n. (deriv ^^ n) f field_differentiable (at w)"
+    by (force simp add: field_differentiable_def)
   have "deriv (\<lambda>w. complex_of_real (2 * pi) * \<i> / (fact k) * (deriv ^^ k) f w) w =
           of_nat (Suc k) * contour_integral (circlepath z r) (\<lambda>u. f u / (u - w) ^ Suc (Suc k))"
     by (force intro!: DERIV_imp_deriv Cauchy_next_derivative_circlepath [OF f Suc.IH _ Suc.prems])
@@ -6112,7 +6112,7 @@
     by (simp only: con)
   finally have "deriv (\<lambda>w. ((2 * pi) * \<i> / (fact k)) * (deriv ^^ k) f w) w = of_nat (Suc k) * X" .
   then have "((2 * pi) * \<i> / (fact k)) * deriv (\<lambda>w. (deriv ^^ k) f w) w = of_nat (Suc k) * X"
-    by (metis complex_derivative_cmult dnf_diff)
+    by (metis deriv_cmult dnf_diff)
   then have "deriv (\<lambda>w. (deriv ^^ k) f w) w = of_nat (Suc k) * X / ((2 * pi) * \<i> / (fact k))"
     by (simp add: field_simps)
   then show ?case
@@ -6432,7 +6432,7 @@
   let ?conint = "contour_integral (circlepath z r)"
   have g: "continuous_on (cball z r) g" "g holomorphic_on ball z r"
     by (rule holomorphic_uniform_limit [OF eventually_mono [OF cont] lim F];
-             auto simp: holomorphic_on_open complex_differentiable_def)+
+             auto simp: holomorphic_on_open field_differentiable_def)+
   then obtain g' where g': "\<And>x. x \<in> ball z r \<Longrightarrow> (g has_field_derivative g' x) (at x)"
     using DERIV_deriv_iff_has_field_derivative
     by (fastforce simp add: holomorphic_on_open)
@@ -6845,54 +6845,54 @@
     shows "(\<lambda>z. if z = a then deriv f a
                  else (f z - f a) / (z - a)) holomorphic_on s" (is "?F holomorphic_on s")
 proof -
-  have F1: "?F complex_differentiable (at u within s)" if "u \<in> s" "u \<noteq> a" for u
+  have F1: "?F field_differentiable (at u within s)" if "u \<in> s" "u \<noteq> a" for u
   proof -
-    have fcd: "f complex_differentiable at u within s"
+    have fcd: "f field_differentiable at u within s"
       using holf holomorphic_on_def by (simp add: \<open>u \<in> s\<close>)
-    have cd: "(\<lambda>z. (f z - f a) / (z - a)) complex_differentiable at u within s"
+    have cd: "(\<lambda>z. (f z - f a) / (z - a)) field_differentiable at u within s"
       by (rule fcd derivative_intros | simp add: that)+
     have "0 < dist a u" using that dist_nz by blast
     then show ?thesis
-      by (rule complex_differentiable_transform_within [OF _ _ _ cd]) (auto simp: \<open>u \<in> s\<close>)
+      by (rule field_differentiable_transform_within [OF _ _ _ cd]) (auto simp: \<open>u \<in> s\<close>)
   qed
-  have F2: "?F complex_differentiable at a" if "0 < e" "ball a e \<subseteq> s" for e
+  have F2: "?F field_differentiable at a" if "0 < e" "ball a e \<subseteq> s" for e
   proof -
     have holfb: "f holomorphic_on ball a e"
       by (rule holomorphic_on_subset [OF holf \<open>ball a e \<subseteq> s\<close>])
     have 2: "?F holomorphic_on ball a e - {a}"
       apply (rule holomorphic_on_subset [where s = "s - {a}"])
-      apply (simp add: holomorphic_on_def complex_differentiable_def [symmetric])
+      apply (simp add: holomorphic_on_def field_differentiable_def [symmetric])
       using mem_ball that
-      apply (auto intro: F1 complex_differentiable_within_subset)
+      apply (auto intro: F1 field_differentiable_within_subset)
       done
     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 then show ?thesis
       using holfb \<open>0 < e\<close>
-      apply (simp add: holomorphic_on_open complex_differentiable_def [symmetric])
+      apply (simp add: holomorphic_on_open field_differentiable_def [symmetric])
       apply (drule_tac x=a in bspec)
-      apply (auto simp: DERIV_deriv_iff_complex_differentiable [symmetric] continuous_at DERIV_iff2
+      apply (auto simp: DERIV_deriv_iff_field_differentiable [symmetric] continuous_at DERIV_iff2
                 elim: rev_iffD1 [OF _ LIM_equal])
       done
     next
       case False with 2 that show ?thesis
-        by (force simp: holomorphic_on_open open_Diff complex_differentiable_def [symmetric] complex_differentiable_imp_continuous_at)
+        by (force simp: holomorphic_on_open open_Diff field_differentiable_def [symmetric] field_differentiable_imp_continuous_at)
     qed
     then have 1: "continuous_on (ball a e) ?F"
       by (clarsimp simp:  continuous_on_eq_continuous_at)
     have "?F holomorphic_on ball a e"
       by (auto intro: no_isolated_singularity [OF 1 2])
     with that show ?thesis
-      by (simp add: holomorphic_on_open complex_differentiable_def [symmetric]
-                    complex_differentiable_at_within)
+      by (simp add: holomorphic_on_open field_differentiable_def [symmetric]
+                    field_differentiable_at_within)
   qed
   show ?thesis
   proof
-    fix x assume "x \<in> s" show "?F complex_differentiable at x within s"
+    fix x assume "x \<in> s" show "?F field_differentiable at x within s"
     proof (cases "x=a")
       case True then show ?thesis
-      using a by (auto simp: mem_interior intro: complex_differentiable_at_within F2)
+      using a by (auto simp: mem_interior intro: field_differentiable_at_within F2)
     next
       case False with F1 \<open>x \<in> s\<close>
       show ?thesis by blast
@@ -6916,8 +6916,8 @@
     show ?thesis by fastforce
 next
   case False with assms show ?thesis
-    apply (simp add: holomorphic_on_def complex_differentiable_def [symmetric], clarify)
-    apply (rule complex_differentiable_transform_within [where f = "\<lambda>z. (f z - f a)/(z - a)" and d = 1])
+    apply (simp add: holomorphic_on_def field_differentiable_def [symmetric], clarify)
+    apply (rule field_differentiable_transform_within [where f = "\<lambda>z. (f z - f a)/(z - a)" and d = 1])
     apply (rule derivative_intros | force)+
     done
 qed
@@ -7082,16 +7082,16 @@
     have *: "(\<lambda>c. if c = y then deriv f y else (f c - f y) / (c - y)) holomorphic_on u"
       by (simp add: holf pole_lemma_open u)
     then have "isCont (\<lambda>x. if x = y then deriv f y else (f x - f y) / (x - y)) y"
-      using at_within_open complex_differentiable_imp_continuous_at holomorphic_on_def that u by fastforce
+      using at_within_open field_differentiable_imp_continuous_at holomorphic_on_def that u by fastforce
     then have "continuous_on u (d y)"
       apply (simp add: d_def continuous_on_eq_continuous_at u, clarify)
       using * holomorphic_on_def
-      by (meson complex_differentiable_within_open complex_differentiable_imp_continuous_at u)
+      by (meson field_differentiable_within_open field_differentiable_imp_continuous_at u)
     moreover have "d y holomorphic_on u - {y}"
-      apply (simp add: d_def holomorphic_on_open u open_delete complex_differentiable_def [symmetric])
+      apply (simp add: d_def holomorphic_on_open u open_delete field_differentiable_def [symmetric])
       apply (intro ballI)
       apply (rename_tac w)
-      apply (rule_tac d="dist w y" and f = "\<lambda>w. (f w - f y)/(w - y)" in complex_differentiable_transform_within)
+      apply (rule_tac d="dist w y" and f = "\<lambda>w. (f w - f y)/(w - y)" in field_differentiable_transform_within)
       apply (auto simp: dist_pos_lt dist_commute intro!: derivative_intros)
       using analytic_on_imp_differentiable_at analytic_on_open holf u apply blast
       done
@@ -7262,7 +7262,7 @@
         have derf_le: "w \<in> closed_segment x' z' \<Longrightarrow> z' \<noteq> x' \<Longrightarrow> cmod (deriv f w - deriv f x) \<le> e" for w
           by (blast intro: cs_less less_k1 k1 [unfolded divide_const_simps dist_norm] less_imp_le le_less_trans)
         have f_has_der: "\<And>x. x \<in> u \<Longrightarrow> (f has_field_derivative deriv f x) (at x within u)"
-          by (metis DERIV_deriv_iff_complex_differentiable at_within_open holf holomorphic_on_def u)
+          by (metis DERIV_deriv_iff_field_differentiable at_within_open holf holomorphic_on_def u)
         have "closed_segment x' z' \<subseteq> u"
           by (rule order_trans [OF _ k2]) (simp add: cs_less  le_less_trans [OF _ less_k2] dist_complex_def norm_minus_commute subset_iff)
         then have cint_derf: "(deriv f has_contour_integral f z' - f x') (linepath x' z')"
@@ -7306,14 +7306,14 @@
         by (rule continuous_on_compose continuous_intros continuous_on_subset [OF cond_uu] | force intro: that)+
       then have *: "continuous_on u (\<lambda>z. if w = z then deriv f z else (f w - f z) / (w - z))"
         by (rule rev_iffD1 [OF _ continuous_on_cong [OF refl]]) (simp add: d_def field_simps)
-      have **: "\<And>x. \<lbrakk>x \<in> u; x \<noteq> w\<rbrakk> \<Longrightarrow> (\<lambda>z. if w = z then deriv f z else (f w - f z) / (w - z)) complex_differentiable at x"
-        apply (rule_tac f = "\<lambda>x. (f w - f x)/(w - x)" and d = "dist x w" in complex_differentiable_transform_within)
+      have **: "\<And>x. \<lbrakk>x \<in> u; x \<noteq> w\<rbrakk> \<Longrightarrow> (\<lambda>z. if w = z then deriv f z else (f w - f z) / (w - z)) field_differentiable at x"
+        apply (rule_tac f = "\<lambda>x. (f w - f x)/(w - x)" and d = "dist x w" in field_differentiable_transform_within)
         apply (rule u derivative_intros holomorphic_on_imp_differentiable_at [OF holf] | force simp add: dist_commute)+
         done
       show ?thesis
         unfolding d_def
         apply (rule no_isolated_singularity [OF * _ u, where k = "{w}"])
-        apply (auto simp: complex_differentiable_def [symmetric] holomorphic_on_open open_Diff u **)
+        apply (auto simp: field_differentiable_def [symmetric] holomorphic_on_open open_Diff u **)
         done
     qed
     { fix a b
@@ -7388,14 +7388,14 @@
         by (simp add: h_def x au o_def)
     qed
     show ?thesis
-    proof (simp add: holomorphic_on_open complex_differentiable_def [symmetric], clarify)
+    proof (simp add: holomorphic_on_open field_differentiable_def [symmetric], clarify)
       fix z0
       consider "z0 \<in> v" | "z0 \<in> u" using uv_Un by blast
-      then show "h complex_differentiable at z0"
+      then show "h field_differentiable at z0"
       proof cases
         assume "z0 \<in> v" then show ?thesis
           using Cauchy_next_derivative [OF con_pa_f le_B f_has_cint _ ov] V f_has_cint \<open>valid_path \<gamma>\<close>
-          by (auto simp: complex_differentiable_def v_def)
+          by (auto simp: field_differentiable_def v_def)
       next
         assume "z0 \<in> u" then
         obtain e where "e>0" and e: "ball z0 e \<subseteq> u" by (blast intro: openE [OF u])
diff -r bc25f3916a99 -r 6855b348e828 src/HOL/Multivariate_Analysis/Complex_Analysis_Basics.thy
--- a/src/HOL/Multivariate_Analysis/Complex_Analysis_Basics.thy	Mon Mar 07 14:34:45 2016 +0000
+++ b/src/HOL/Multivariate_Analysis/Complex_Analysis_Basics.thy	Mon Mar 07 15:57:02 2016 +0000
@@ -277,159 +277,159 @@
 
 subsection\<open>Holomorphic functions\<close>
 
-definition complex_differentiable :: "['a \<Rightarrow> 'a::real_normed_field, 'a filter] \<Rightarrow> bool"
-           (infixr "(complex'_differentiable)" 50)
-  where "f complex_differentiable F \<equiv> \<exists>f'. (f has_field_derivative f') F"
+definition field_differentiable :: "['a \<Rightarrow> 'a::real_normed_field, 'a filter] \<Rightarrow> bool"
+           (infixr "(field'_differentiable)" 50)
+  where "f field_differentiable F \<equiv> \<exists>f'. (f has_field_derivative f') F"
 
-lemma complex_differentiable_derivI:
-    "f complex_differentiable (at x) \<Longrightarrow> (f has_field_derivative deriv f x) (at x)"
-by (simp add: complex_differentiable_def DERIV_deriv_iff_has_field_derivative)
+lemma field_differentiable_derivI:
+    "f field_differentiable (at x) \<Longrightarrow> (f has_field_derivative deriv f x) (at x)"
+by (simp add: field_differentiable_def DERIV_deriv_iff_has_field_derivative)
 
-lemma complex_differentiable_imp_continuous_at:
-    "f complex_differentiable (at x within s) \<Longrightarrow> continuous (at x within s) f"
-  by (metis DERIV_continuous complex_differentiable_def)
+lemma field_differentiable_imp_continuous_at:
+    "f field_differentiable (at x within s) \<Longrightarrow> continuous (at x within s) f"
+  by (metis DERIV_continuous field_differentiable_def)
 
-lemma complex_differentiable_within_subset:
-    "\<lbrakk>f complex_differentiable (at x within s); t \<subseteq> s\<rbrakk>
-     \<Longrightarrow> f complex_differentiable (at x within t)"
-  by (metis DERIV_subset complex_differentiable_def)
+lemma field_differentiable_within_subset:
+    "\<lbrakk>f field_differentiable (at x within s); t \<subseteq> s\<rbrakk>
+     \<Longrightarrow> f field_differentiable (at x within t)"
+  by (metis DERIV_subset field_differentiable_def)
 
-lemma complex_differentiable_at_within:
-    "\<lbrakk>f complex_differentiable (at x)\<rbrakk>
-     \<Longrightarrow> f complex_differentiable (at x within s)"
-  unfolding complex_differentiable_def
+lemma field_differentiable_at_within:
+    "\<lbrakk>f field_differentiable (at x)\<rbrakk>
+     \<Longrightarrow> f field_differentiable (at x within s)"
+  unfolding field_differentiable_def
   by (metis DERIV_subset top_greatest)
 
-lemma complex_differentiable_linear [simp,derivative_intros]: "(op * c) complex_differentiable F"
+lemma field_differentiable_linear [simp,derivative_intros]: "(op * c) field_differentiable F"
 proof -
   show ?thesis
-    unfolding complex_differentiable_def has_field_derivative_def mult_commute_abs
+    unfolding field_differentiable_def has_field_derivative_def mult_commute_abs
     by (force intro: has_derivative_mult_right)
 qed
 
-lemma complex_differentiable_const [simp,derivative_intros]: "(\<lambda>z. c) complex_differentiable F"
-  unfolding complex_differentiable_def has_field_derivative_def
+lemma field_differentiable_const [simp,derivative_intros]: "(\<lambda>z. c) field_differentiable F"
+  unfolding field_differentiable_def has_field_derivative_def
   by (rule exI [where x=0])
      (metis has_derivative_const lambda_zero)
 
-lemma complex_differentiable_ident [simp,derivative_intros]: "(\<lambda>z. z) complex_differentiable F"
-  unfolding complex_differentiable_def has_field_derivative_def
+lemma field_differentiable_ident [simp,derivative_intros]: "(\<lambda>z. z) field_differentiable F"
+  unfolding field_differentiable_def has_field_derivative_def
   by (rule exI [where x=1])
      (simp add: lambda_one [symmetric])
 
-lemma complex_differentiable_id [simp,derivative_intros]: "id complex_differentiable F"
-  unfolding id_def by (rule complex_differentiable_ident)
+lemma field_differentiable_id [simp,derivative_intros]: "id field_differentiable F"
+  unfolding id_def by (rule field_differentiable_ident)
 
-lemma complex_differentiable_minus [derivative_intros]:
-  "f complex_differentiable F \<Longrightarrow> (\<lambda>z. - (f z)) complex_differentiable F"
-  using assms unfolding complex_differentiable_def
+lemma field_differentiable_minus [derivative_intros]:
+  "f field_differentiable F \<Longrightarrow> (\<lambda>z. - (f z)) field_differentiable F"
+  using assms unfolding field_differentiable_def
   by (metis field_differentiable_minus)
 
-lemma complex_differentiable_add [derivative_intros]:
-  assumes "f complex_differentiable F" "g complex_differentiable F"
-    shows "(\<lambda>z. f z + g z) complex_differentiable F"
-  using assms unfolding complex_differentiable_def
+lemma field_differentiable_add [derivative_intros]:
+  assumes "f field_differentiable F" "g field_differentiable F"
+    shows "(\<lambda>z. f z + g z) field_differentiable F"
+  using assms unfolding field_differentiable_def
   by (metis field_differentiable_add)
 
-lemma complex_differentiable_add_const [simp,derivative_intros]:
-     "op + c complex_differentiable F"
-  by (simp add: complex_differentiable_add)
+lemma field_differentiable_add_const [simp,derivative_intros]:
+     "op + c field_differentiable F"
+  by (simp add: field_differentiable_add)
 
-lemma complex_differentiable_setsum [derivative_intros]:
-  "(\<And>i. i \<in> I \<Longrightarrow> (f i) complex_differentiable F) \<Longrightarrow> (\<lambda>z. \<Sum>i\<in>I. f i z) complex_differentiable F"
+lemma field_differentiable_setsum [derivative_intros]:
+  "(\<And>i. i \<in> I \<Longrightarrow> (f i) field_differentiable F) \<Longrightarrow> (\<lambda>z. \<Sum>i\<in>I. f i z) field_differentiable F"
   by (induct I rule: infinite_finite_induct)
-     (auto intro: complex_differentiable_add complex_differentiable_const)
+     (auto intro: field_differentiable_add field_differentiable_const)
 
-lemma complex_differentiable_diff [derivative_intros]:
-  assumes "f complex_differentiable F" "g complex_differentiable F"
-    shows "(\<lambda>z. f z - g z) complex_differentiable F"
-  using assms unfolding complex_differentiable_def
+lemma field_differentiable_diff [derivative_intros]:
+  assumes "f field_differentiable F" "g field_differentiable F"
+    shows "(\<lambda>z. f z - g z) field_differentiable F"
+  using assms unfolding field_differentiable_def
   by (metis field_differentiable_diff)
 
-lemma complex_differentiable_inverse [derivative_intros]:
-  assumes "f complex_differentiable (at a within s)" "f a \<noteq> 0"
-  shows "(\<lambda>z. inverse (f z)) complex_differentiable (at a within s)"
-  using assms unfolding complex_differentiable_def
+lemma field_differentiable_inverse [derivative_intros]:
+  assumes "f field_differentiable (at a within s)" "f a \<noteq> 0"
+  shows "(\<lambda>z. inverse (f z)) field_differentiable (at a within s)"
+  using assms unfolding field_differentiable_def
   by (metis DERIV_inverse_fun)
 
-lemma complex_differentiable_mult [derivative_intros]:
-  assumes "f complex_differentiable (at a within s)"
-          "g complex_differentiable (at a within s)"
-    shows "(\<lambda>z. f z * g z) complex_differentiable (at a within s)"
-  using assms unfolding complex_differentiable_def
+lemma field_differentiable_mult [derivative_intros]:
+  assumes "f field_differentiable (at a within s)"
+          "g field_differentiable (at a within s)"
+    shows "(\<lambda>z. f z * g z) field_differentiable (at a within s)"
+  using assms unfolding field_differentiable_def
   by (metis DERIV_mult [of f _ a s g])
 
-lemma complex_differentiable_divide [derivative_intros]:
-  assumes "f complex_differentiable (at a within s)"
-          "g complex_differentiable (at a within s)"
+lemma field_differentiable_divide [derivative_intros]:
+  assumes "f field_differentiable (at a within s)"
+          "g field_differentiable (at a within s)"
           "g a \<noteq> 0"
-    shows "(\<lambda>z. f z / g z) complex_differentiable (at a within s)"
-  using assms unfolding complex_differentiable_def
+    shows "(\<lambda>z. f z / g z) field_differentiable (at a within s)"
+  using assms unfolding field_differentiable_def
   by (metis DERIV_divide [of f _ a s g])
 
-lemma complex_differentiable_power [derivative_intros]:
-  assumes "f complex_differentiable (at a within s)"
-    shows "(\<lambda>z. f z ^ n) complex_differentiable (at a within s)"
-  using assms unfolding complex_differentiable_def
+lemma field_differentiable_power [derivative_intros]:
+  assumes "f field_differentiable (at a within s)"
+    shows "(\<lambda>z. f z ^ n) field_differentiable (at a within s)"
+  using assms unfolding field_differentiable_def
   by (metis DERIV_power)
 
-lemma complex_differentiable_transform_within:
+lemma field_differentiable_transform_within:
   "0 < d \<Longrightarrow>
         x \<in> s \<Longrightarrow>
         (\<And>x'. x' \<in> s \<Longrightarrow> dist x' x < d \<Longrightarrow> f x' = g x') \<Longrightarrow>
-        f complex_differentiable (at x within s)
-        \<Longrightarrow> g complex_differentiable (at x within s)"
-  unfolding complex_differentiable_def has_field_derivative_def
+        f field_differentiable (at x within s)
+        \<Longrightarrow> g field_differentiable (at x within s)"
+  unfolding field_differentiable_def has_field_derivative_def
   by (blast intro: has_derivative_transform_within)
 
-lemma complex_differentiable_compose_within:
-  assumes "f complex_differentiable (at a within s)"
-          "g complex_differentiable (at (f a) within f`s)"
-    shows "(g o f) complex_differentiable (at a within s)"
-  using assms unfolding complex_differentiable_def
+lemma field_differentiable_compose_within:
+  assumes "f field_differentiable (at a within s)"
+          "g field_differentiable (at (f a) within f`s)"
+    shows "(g o f) field_differentiable (at a within s)"
+  using assms unfolding field_differentiable_def
   by (metis DERIV_image_chain)
 
-lemma complex_differentiable_compose:
-  "f complex_differentiable at z \<Longrightarrow> g complex_differentiable at (f z)
-          \<Longrightarrow> (g o f) complex_differentiable at z"
-by (metis complex_differentiable_at_within complex_differentiable_compose_within)
+lemma field_differentiable_compose:
+  "f field_differentiable at z \<Longrightarrow> g field_differentiable at (f z)
+          \<Longrightarrow> (g o f) field_differentiable at z"
+by (metis field_differentiable_at_within field_differentiable_compose_within)
 
-lemma complex_differentiable_within_open:
-     "\<lbrakk>a \<in> s; open s\<rbrakk> \<Longrightarrow> f complex_differentiable at a within s \<longleftrightarrow>
-                          f complex_differentiable at a"
-  unfolding complex_differentiable_def
+lemma field_differentiable_within_open:
+     "\<lbrakk>a \<in> s; open s\<rbrakk> \<Longrightarrow> f field_differentiable at a within s \<longleftrightarrow>
+                          f field_differentiable at a"
+  unfolding field_differentiable_def
   by (metis at_within_open)
 
 subsection\<open>Caratheodory characterization\<close>
 
-lemma complex_differentiable_caratheodory_at:
-  "f complex_differentiable (at z) \<longleftrightarrow>
+lemma field_differentiable_caratheodory_at:
+  "f field_differentiable (at z) \<longleftrightarrow>
          (\<exists>g. (\<forall>w. f(w) - f(z) = g(w) * (w - z)) \<and> continuous (at z) g)"
   using CARAT_DERIV [of f]
-  by (simp add: complex_differentiable_def has_field_derivative_def)
+  by (simp add: field_differentiable_def has_field_derivative_def)
 
-lemma complex_differentiable_caratheodory_within:
-  "f complex_differentiable (at z within s) \<longleftrightarrow>
+lemma field_differentiable_caratheodory_within:
+  "f field_differentiable (at z within s) \<longleftrightarrow>
          (\<exists>g. (\<forall>w. f(w) - f(z) = g(w) * (w - z)) \<and> continuous (at z within s) g)"
   using DERIV_caratheodory_within [of f]
-  by (simp add: complex_differentiable_def has_field_derivative_def)
+  by (simp add: field_differentiable_def has_field_derivative_def)
 
 subsection\<open>Holomorphic\<close>
 
 definition holomorphic_on :: "[complex \<Rightarrow> complex, complex set] \<Rightarrow> bool"
            (infixl "(holomorphic'_on)" 50)
-  where "f holomorphic_on s \<equiv> \<forall>x\<in>s. f complex_differentiable (at x within s)"
+  where "f holomorphic_on s \<equiv> \<forall>x\<in>s. f field_differentiable (at x within s)"
 
 named_theorems holomorphic_intros "structural introduction rules for holomorphic_on"
 
-lemma holomorphic_onI [intro?]: "(\<And>x. x \<in> s \<Longrightarrow> f complex_differentiable (at x within s)) \<Longrightarrow> f holomorphic_on s"
+lemma holomorphic_onI [intro?]: "(\<And>x. x \<in> s \<Longrightarrow> f field_differentiable (at x within s)) \<Longrightarrow> f holomorphic_on s"
   by (simp add: holomorphic_on_def)
 
-lemma holomorphic_onD [dest?]: "\<lbrakk>f holomorphic_on s; x \<in> s\<rbrakk> \<Longrightarrow> f complex_differentiable (at x within s)"
+lemma holomorphic_onD [dest?]: "\<lbrakk>f holomorphic_on s; x \<in> s\<rbrakk> \<Longrightarrow> f field_differentiable (at x within s)"
   by (simp add: holomorphic_on_def)
 
 lemma holomorphic_on_imp_differentiable_at:
-   "\<lbrakk>f holomorphic_on s; open s; x \<in> s\<rbrakk> \<Longrightarrow> f complex_differentiable (at x)"
+   "\<lbrakk>f holomorphic_on s; open s; x \<in> s\<rbrakk> \<Longrightarrow> f field_differentiable (at x)"
 using at_within_open holomorphic_on_def by fastforce
 
 lemma holomorphic_on_empty [holomorphic_intros]: "f holomorphic_on {}"
@@ -437,38 +437,38 @@
 
 lemma holomorphic_on_open:
     "open s \<Longrightarrow> f holomorphic_on s \<longleftrightarrow> (\<forall>x \<in> s. \<exists>f'. DERIV f x :> f')"
-  by (auto simp: holomorphic_on_def complex_differentiable_def has_field_derivative_def at_within_open [of _ s])
+  by (auto simp: holomorphic_on_def field_differentiable_def has_field_derivative_def at_within_open [of _ s])
 
 lemma holomorphic_on_imp_continuous_on:
     "f holomorphic_on s \<Longrightarrow> continuous_on s f"
-  by (metis complex_differentiable_imp_continuous_at continuous_on_eq_continuous_within holomorphic_on_def)
+  by (metis field_differentiable_imp_continuous_at continuous_on_eq_continuous_within holomorphic_on_def)
 
 lemma holomorphic_on_subset:
     "f holomorphic_on s \<Longrightarrow> t \<subseteq> s \<Longrightarrow> f holomorphic_on t"
   unfolding holomorphic_on_def
-  by (metis complex_differentiable_within_subset subsetD)
+  by (metis field_differentiable_within_subset subsetD)
 
 lemma holomorphic_transform: "\<lbrakk>f holomorphic_on s; \<And>x. x \<in> s \<Longrightarrow> f x = g x\<rbrakk> \<Longrightarrow> g holomorphic_on s"
-  by (metis complex_differentiable_transform_within linordered_field_no_ub holomorphic_on_def)
+  by (metis field_differentiable_transform_within linordered_field_no_ub holomorphic_on_def)
 
 lemma holomorphic_cong: "s = t ==> (\<And>x. x \<in> s \<Longrightarrow> f x = g x) \<Longrightarrow> f holomorphic_on s \<longleftrightarrow> g holomorphic_on t"
   by (metis holomorphic_transform)
 
 lemma holomorphic_on_linear [simp, holomorphic_intros]: "(op * c) holomorphic_on s"
-  unfolding holomorphic_on_def by (metis complex_differentiable_linear)
+  unfolding holomorphic_on_def by (metis field_differentiable_linear)
 
 lemma holomorphic_on_const [simp, holomorphic_intros]: "(\<lambda>z. c) holomorphic_on s"
-  unfolding holomorphic_on_def by (metis complex_differentiable_const)
+  unfolding holomorphic_on_def by (metis field_differentiable_const)
 
 lemma holomorphic_on_ident [simp, holomorphic_intros]: "(\<lambda>x. x) holomorphic_on s"
-  unfolding holomorphic_on_def by (metis complex_differentiable_ident)
+  unfolding holomorphic_on_def by (metis field_differentiable_ident)
 
 lemma holomorphic_on_id [simp, holomorphic_intros]: "id holomorphic_on s"
   unfolding id_def by (rule holomorphic_on_ident)
 
 lemma holomorphic_on_compose:
   "f holomorphic_on s \<Longrightarrow> g holomorphic_on (f ` s) \<Longrightarrow> (g o f) holomorphic_on s"
-  using complex_differentiable_compose_within[of f _ s g]
+  using field_differentiable_compose_within[of f _ s g]
   by (auto simp: holomorphic_on_def)
 
 lemma holomorphic_on_compose_gen:
@@ -476,49 +476,49 @@
   by (metis holomorphic_on_compose holomorphic_on_subset)
 
 lemma holomorphic_on_minus [holomorphic_intros]: "f holomorphic_on s \<Longrightarrow> (\<lambda>z. -(f z)) holomorphic_on s"
-  by (metis complex_differentiable_minus holomorphic_on_def)
+  by (metis field_differentiable_minus holomorphic_on_def)
 
 lemma holomorphic_on_add [holomorphic_intros]:
   "\<lbrakk>f holomorphic_on s; g holomorphic_on s\<rbrakk> \<Longrightarrow> (\<lambda>z. f z + g z) holomorphic_on s"
-  unfolding holomorphic_on_def by (metis complex_differentiable_add)
+  unfolding holomorphic_on_def by (metis field_differentiable_add)
 
 lemma holomorphic_on_diff [holomorphic_intros]:
   "\<lbrakk>f holomorphic_on s; g holomorphic_on s\<rbrakk> \<Longrightarrow> (\<lambda>z. f z - g z) holomorphic_on s"
-  unfolding holomorphic_on_def by (metis complex_differentiable_diff)
+  unfolding holomorphic_on_def by (metis field_differentiable_diff)
 
 lemma holomorphic_on_mult [holomorphic_intros]:
   "\<lbrakk>f holomorphic_on s; g holomorphic_on s\<rbrakk> \<Longrightarrow> (\<lambda>z. f z * g z) holomorphic_on s"
-  unfolding holomorphic_on_def by (metis complex_differentiable_mult)
+  unfolding holomorphic_on_def by (metis field_differentiable_mult)
 
 lemma holomorphic_on_inverse [holomorphic_intros]:
   "\<lbrakk>f holomorphic_on s; \<And>z. z \<in> s \<Longrightarrow> f z \<noteq> 0\<rbrakk> \<Longrightarrow> (\<lambda>z. inverse (f z)) holomorphic_on s"
-  unfolding holomorphic_on_def by (metis complex_differentiable_inverse)
+  unfolding holomorphic_on_def by (metis field_differentiable_inverse)
 
 lemma holomorphic_on_divide [holomorphic_intros]:
   "\<lbrakk>f holomorphic_on s; g holomorphic_on s; \<And>z. z \<in> s \<Longrightarrow> g z \<noteq> 0\<rbrakk> \<Longrightarrow> (\<lambda>z. f z / g z) holomorphic_on s"
-  unfolding holomorphic_on_def by (metis complex_differentiable_divide)
+  unfolding holomorphic_on_def by (metis field_differentiable_divide)
 
 lemma holomorphic_on_power [holomorphic_intros]:
   "f holomorphic_on s \<Longrightarrow> (\<lambda>z. (f z)^n) holomorphic_on s"
-  unfolding holomorphic_on_def by (metis complex_differentiable_power)
+  unfolding holomorphic_on_def by (metis field_differentiable_power)
 
 lemma holomorphic_on_setsum [holomorphic_intros]:
   "(\<And>i. i \<in> I \<Longrightarrow> (f i) holomorphic_on s) \<Longrightarrow> (\<lambda>x. setsum (\<lambda>i. f i x) I) holomorphic_on s"
-  unfolding holomorphic_on_def by (metis complex_differentiable_setsum)
+  unfolding holomorphic_on_def by (metis field_differentiable_setsum)
 
-lemma DERIV_deriv_iff_complex_differentiable:
-  "DERIV f x :> deriv f x \<longleftrightarrow> f complex_differentiable at x"
-  unfolding complex_differentiable_def by (metis DERIV_imp_deriv)
+lemma DERIV_deriv_iff_field_differentiable:
+  "DERIV f x :> deriv f x \<longleftrightarrow> f field_differentiable at x"
+  unfolding field_differentiable_def by (metis DERIV_imp_deriv)
 
 lemma holomorphic_derivI:
      "\<lbrakk>f holomorphic_on S; open S; x \<in> S\<rbrakk>
       \<Longrightarrow> (f has_field_derivative deriv f x) (at x within T)"
-by (metis DERIV_deriv_iff_complex_differentiable at_within_open  holomorphic_on_def has_field_derivative_at_within)
+by (metis DERIV_deriv_iff_field_differentiable at_within_open  holomorphic_on_def has_field_derivative_at_within)
 
 lemma complex_derivative_chain:
-  "f complex_differentiable at x \<Longrightarrow> g complex_differentiable at (f x)
+  "f field_differentiable at x \<Longrightarrow> g field_differentiable at (f x)
     \<Longrightarrow> deriv (g o f) x = deriv g (f x) * deriv f x"
-  by (metis DERIV_deriv_iff_complex_differentiable DERIV_chain DERIV_imp_deriv)
+  by (metis DERIV_deriv_iff_field_differentiable DERIV_chain DERIV_imp_deriv)
 
 lemma deriv_linear [simp]: "deriv (\<lambda>w. c * w) = (\<lambda>z. c)"
   by (metis DERIV_imp_deriv DERIV_cmult_Id)
@@ -532,50 +532,50 @@
 lemma deriv_const [simp]: "deriv (\<lambda>w. c) = (\<lambda>z. 0)"
   by (metis DERIV_imp_deriv DERIV_const)
 
-lemma complex_derivative_add [simp]:
-  "\<lbrakk>f complex_differentiable at z; g complex_differentiable at z\<rbrakk>
+lemma deriv_add [simp]:
+  "\<lbrakk>f field_differentiable at z; g field_differentiable at z\<rbrakk>
    \<Longrightarrow> deriv (\<lambda>w. f w + g w) z = deriv f z + deriv g z"
-  unfolding DERIV_deriv_iff_complex_differentiable[symmetric]
+  unfolding DERIV_deriv_iff_field_differentiable[symmetric]
   by (auto intro!: DERIV_imp_deriv derivative_intros)
 
-lemma complex_derivative_diff [simp]:
-  "\<lbrakk>f complex_differentiable at z; g complex_differentiable at z\<rbrakk>
+lemma deriv_diff [simp]:
+  "\<lbrakk>f field_differentiable at z; g field_differentiable at z\<rbrakk>
    \<Longrightarrow> deriv (\<lambda>w. f w - g w) z = deriv f z - deriv g z"
-  unfolding DERIV_deriv_iff_complex_differentiable[symmetric]
+  unfolding DERIV_deriv_iff_field_differentiable[symmetric]
   by (auto intro!: DERIV_imp_deriv derivative_intros)
 
-lemma complex_derivative_mult [simp]:
-  "\<lbrakk>f complex_differentiable at z; g complex_differentiable at z\<rbrakk>
+lemma deriv_mult [simp]:
+  "\<lbrakk>f field_differentiable at z; g field_differentiable at z\<rbrakk>
    \<Longrightarrow> deriv (\<lambda>w. f w * g w) z = f z * deriv g z + deriv f z * g z"
-  unfolding DERIV_deriv_iff_complex_differentiable[symmetric]
+  unfolding DERIV_deriv_iff_field_differentiable[symmetric]
   by (auto intro!: DERIV_imp_deriv derivative_eq_intros)
 
-lemma complex_derivative_cmult [simp]:
-  "f complex_differentiable at z \<Longrightarrow> deriv (\<lambda>w. c * f w) z = c * deriv f z"
-  unfolding DERIV_deriv_iff_complex_differentiable[symmetric]
+lemma deriv_cmult [simp]:
+  "f field_differentiable at z \<Longrightarrow> deriv (\<lambda>w. c * f w) z = c * deriv f z"
+  unfolding DERIV_deriv_iff_field_differentiable[symmetric]
   by (auto intro!: DERIV_imp_deriv derivative_eq_intros)
 
-lemma complex_derivative_cmult_right [simp]:
-  "f complex_differentiable at z \<Longrightarrow> deriv (\<lambda>w. f w * c) z = deriv f z * c"
-  unfolding DERIV_deriv_iff_complex_differentiable[symmetric]
+lemma deriv_cmult_right [simp]:
+  "f field_differentiable at z \<Longrightarrow> deriv (\<lambda>w. f w * c) z = deriv f z * c"
+  unfolding DERIV_deriv_iff_field_differentiable[symmetric]
   by (auto intro!: DERIV_imp_deriv derivative_eq_intros)
 
-lemma complex_derivative_cdivide_right [simp]:
-  "f complex_differentiable at z \<Longrightarrow> deriv (\<lambda>w. f w / c) z = deriv f z / c"
+lemma deriv_cdivide_right [simp]:
+  "f field_differentiable at z \<Longrightarrow> deriv (\<lambda>w. f w / c) z = deriv f z / c"
   unfolding Fields.field_class.field_divide_inverse
-  by (blast intro: complex_derivative_cmult_right)
+  by (blast intro: deriv_cmult_right)
 
 lemma complex_derivative_transform_within_open:
   "\<lbrakk>f holomorphic_on s; g holomorphic_on s; open s; z \<in> s; \<And>w. w \<in> s \<Longrightarrow> f w = g w\<rbrakk>
    \<Longrightarrow> deriv f z = deriv g z"
   unfolding holomorphic_on_def
   by (rule DERIV_imp_deriv)
-     (metis DERIV_deriv_iff_complex_differentiable DERIV_transform_within_open at_within_open)
+     (metis DERIV_deriv_iff_field_differentiable DERIV_transform_within_open at_within_open)
 
-lemma complex_derivative_compose_linear:
-  "f complex_differentiable at (c * z) \<Longrightarrow> deriv (\<lambda>w. f (c * w)) z = c * deriv f (c * z)"
+lemma deriv_compose_linear:
+  "f field_differentiable at (c * z) \<Longrightarrow> deriv (\<lambda>w. f (c * w)) z = c * deriv f (c * z)"
 apply (rule DERIV_imp_deriv)
-apply (simp add: DERIV_deriv_iff_complex_differentiable [symmetric])
+apply (simp add: DERIV_deriv_iff_field_differentiable [symmetric])
 apply (drule DERIV_chain' [of "times c" c z UNIV f "deriv f (c * z)", OF DERIV_cmult_Id])
 apply (simp add: algebra_simps)
 done
@@ -602,7 +602,7 @@
 
 lemma analytic_imp_holomorphic: "f analytic_on s \<Longrightarrow> f holomorphic_on s"
   by (simp add: at_within_open [OF _ open_ball] analytic_on_def holomorphic_on_def)
-     (metis centre_in_ball complex_differentiable_at_within)
+     (metis centre_in_ball field_differentiable_at_within)
 
 lemma analytic_on_open: "open s \<Longrightarrow> f analytic_on s \<longleftrightarrow> f holomorphic_on s"
 apply (auto simp: analytic_imp_holomorphic)
@@ -610,9 +610,9 @@
 by (metis holomorphic_on_def holomorphic_on_subset open_contains_ball)
 
 lemma analytic_on_imp_differentiable_at:
-  "f analytic_on s \<Longrightarrow> x \<in> s \<Longrightarrow> f complex_differentiable (at x)"
+  "f analytic_on s \<Longrightarrow> x \<in> s \<Longrightarrow> f field_differentiable (at x)"
  apply (auto simp: analytic_on_def holomorphic_on_def)
-by (metis Topology_Euclidean_Space.open_ball centre_in_ball complex_differentiable_within_open)
+by (metis Topology_Euclidean_Space.open_ball centre_in_ball field_differentiable_within_open)
 
 lemma analytic_on_subset: "f analytic_on s \<Longrightarrow> t \<subseteq> s \<Longrightarrow> f analytic_on t"
   by (auto simp: analytic_on_def)
@@ -674,7 +674,7 @@
   obtain e' where e': "0 < e'" and gh: "g holomorphic_on ball (f x) e'" using g
     by (metis analytic_on_def g image_eqI x)
   have "isCont f x"
-    by (metis analytic_on_imp_differentiable_at complex_differentiable_imp_continuous_at f x)
+    by (metis analytic_on_imp_differentiable_at field_differentiable_imp_continuous_at f x)
   with e' obtain d where d: "0 < d" and fd: "f ` ball x d \<subseteq> ball (f x) e'"
      by (auto simp: continuous_at_ball)
   have "g \<circ> f holomorphic_on ball x (min d e)"
@@ -864,25 +864,25 @@
   show "deriv (\<lambda>w. f w + g w) z = deriv f z + deriv g z"
     apply (rule DERIV_imp_deriv [OF DERIV_add])
     using s
-    apply (auto simp: holomorphic_on_open complex_differentiable_def DERIV_deriv_iff_complex_differentiable)
+    apply (auto simp: holomorphic_on_open field_differentiable_def DERIV_deriv_iff_field_differentiable)
     done
   show "deriv (\<lambda>w. f w - g w) z = deriv f z - deriv g z"
     apply (rule DERIV_imp_deriv [OF DERIV_diff])
     using s
-    apply (auto simp: holomorphic_on_open complex_differentiable_def DERIV_deriv_iff_complex_differentiable)
+    apply (auto simp: holomorphic_on_open field_differentiable_def DERIV_deriv_iff_field_differentiable)
     done
   show "deriv (\<lambda>w. f w * g w) z = f z * deriv g z + deriv f z * g z"
     apply (rule DERIV_imp_deriv [OF DERIV_mult'])
     using s
-    apply (auto simp: holomorphic_on_open complex_differentiable_def DERIV_deriv_iff_complex_differentiable)
+    apply (auto simp: holomorphic_on_open field_differentiable_def DERIV_deriv_iff_field_differentiable)
     done
 qed
 
-lemma complex_derivative_cmult_at:
+lemma deriv_cmult_at:
   "f analytic_on {z} \<Longrightarrow>  deriv (\<lambda>w. c * f w) z = c * deriv f z"
 by (auto simp: complex_derivative_mult_at deriv_const analytic_on_const)
 
-lemma complex_derivative_cmult_right_at:
+lemma deriv_cmult_right_at:
   "f analytic_on {z} \<Longrightarrow>  deriv (\<lambda>w. f w * c) z = deriv f z * c"
 by (auto simp: complex_derivative_mult_at deriv_const analytic_on_const)
 
@@ -927,7 +927,6 @@
   qed
 qed
 
-
 lemma has_complex_derivative_series:
   fixes s :: "complex set"
   assumes cvs: "convex s"
@@ -970,13 +969,13 @@
 qed
 
 
-lemma complex_differentiable_series:
+lemma field_differentiable_series:
   fixes f :: "nat \<Rightarrow> complex \<Rightarrow> complex"
   assumes "convex s" "open s"
   assumes "\<And>n x. x \<in> s \<Longrightarrow> (f n has_field_derivative f' n x) (at x)"
   assumes "uniformly_convergent_on s (\<lambda>n x. \<Sum>i<n. f' i x)"
   assumes "x0 \<in> s" "summable (\<lambda>n. f n x0)" and x: "x \<in> s"
-  shows   "summable (\<lambda>n. f n x)" and "(\<lambda>x. \<Sum>n. f n x) complex_differentiable (at x)"
+  shows   "summable (\<lambda>n. f n x)" and "(\<lambda>x. \<Sum>n. f n x) field_differentiable (at x)"
 proof -
   from assms(4) obtain g' where A: "uniform_limit s (\<lambda>n x. \<Sum>i<n. f' i x) g' sequentially"
     unfolding uniformly_convergent_on_def by blast
@@ -991,22 +990,22 @@
   have "((\<lambda>x. \<Sum>n. f n x) has_derivative op * (g' x)) (at x)"
     by (rule has_derivative_transform_within_open[OF g' \<open>open s\<close> x])
        (insert g, auto simp: sums_iff)
-  thus "(\<lambda>x. \<Sum>n. f n x) complex_differentiable (at x)" unfolding differentiable_def
-    by (auto simp: summable_def complex_differentiable_def has_field_derivative_def)
+  thus "(\<lambda>x. \<Sum>n. f n x) field_differentiable (at x)" unfolding differentiable_def
+    by (auto simp: summable_def field_differentiable_def has_field_derivative_def)
 qed
 
-lemma complex_differentiable_series':
+lemma field_differentiable_series':
   fixes f :: "nat \<Rightarrow> complex \<Rightarrow> complex"
   assumes "convex s" "open s"
   assumes "\<And>n x. x \<in> s \<Longrightarrow> (f n has_field_derivative f' n x) (at x)"
   assumes "uniformly_convergent_on s (\<lambda>n x. \<Sum>i<n. f' i x)"
   assumes "x0 \<in> s" "summable (\<lambda>n. f n x0)"
-  shows   "(\<lambda>x. \<Sum>n. f n x) complex_differentiable (at x0)"
-  using complex_differentiable_series[OF assms, of x0] \<open>x0 \<in> s\<close> by blast+
+  shows   "(\<lambda>x. \<Sum>n. f n x) field_differentiable (at x0)"
+  using field_differentiable_series[OF assms, of x0] \<open>x0 \<in> s\<close> by blast+
 
 subsection\<open>Bound theorem\<close>
 
-lemma complex_differentiable_bound:
+lemma field_differentiable_bound:
   fixes s :: "complex set"
   assumes cvs: "convex s"
       and df:  "\<And>z. z \<in> s \<Longrightarrow> (f has_field_derivative f' z) (at z within s)"
@@ -1155,7 +1154,7 @@
                         (\<Sum>i\<le>n. f i z * (z - z) ^ i / (fact i)))"
     by (simp add: norm_minus_commute)
   also have "... \<le> B * cmod (z - w) ^ n / (fact n) * cmod (w - z)"
-    apply (rule complex_differentiable_bound
+    apply (rule field_differentiable_bound
       [where f' = "\<lambda>w. f (Suc n) w * (z - w)^n / (fact n)"
          and s = "closed_segment w z", OF convex_closed_segment])
     apply (auto simp: ends_in_segment DERIV_subset [OF sum_deriv wzs]
diff -r bc25f3916a99 -r 6855b348e828 src/HOL/Multivariate_Analysis/Complex_Transcendental.thy
--- a/src/HOL/Multivariate_Analysis/Complex_Transcendental.thy	Mon Mar 07 14:34:45 2016 +0000
+++ b/src/HOL/Multivariate_Analysis/Complex_Transcendental.thy	Mon Mar 07 15:57:02 2016 +0000
@@ -3,7 +3,7 @@
 text\<open>By John Harrison et al.  Ported from HOL Light by L C Paulson (2015)\<close>
 
 theory Complex_Transcendental
-imports 
+imports
   Complex_Analysis_Basics
   Summation
 begin
@@ -11,7 +11,7 @@
 (* TODO: Figure out what to do with Möbius transformations *)
 definition "moebius a b c d = (\<lambda>z. (a*z+b) / (c*z+d :: 'a :: field))"
 
-lemma moebius_inverse: 
+lemma moebius_inverse:
   assumes "a * d \<noteq> b * c" "c * z + d \<noteq> 0"
   shows   "moebius d (-b) (-c) a (moebius a b c d z) = z"
 proof -
@@ -21,7 +21,7 @@
     unfolding moebius_def by (simp add: moebius_def divide_simps) (simp add: algebra_simps)?
 qed
 
-lemma moebius_inverse': 
+lemma moebius_inverse':
   assumes "a * d \<noteq> b * c" "c * z - a \<noteq> 0"
   shows   "moebius a b c d (moebius d (-b) (-c) a z) = z"
   using assms moebius_inverse[of d a "-b" "-c" z]
@@ -61,21 +61,16 @@
 
 subsection\<open>The Exponential Function is Differentiable and Continuous\<close>
 
-lemma complex_differentiable_within_exp: "exp complex_differentiable (at z within s)"
-  using DERIV_exp complex_differentiable_at_within complex_differentiable_def by blast
+lemma field_differentiable_within_exp: "exp field_differentiable (at z within s)"
+  using DERIV_exp field_differentiable_at_within field_differentiable_def by blast
 
 lemma continuous_within_exp:
   fixes z::"'a::{real_normed_field,banach}"
   shows "continuous (at z within s) exp"
 by (simp add: continuous_at_imp_continuous_within)
 
-lemma continuous_on_exp:
-  fixes s::"'a::{real_normed_field,banach} set"
-  shows "continuous_on s exp"
-by (simp add: continuous_on_exp continuous_on_id)
-
 lemma holomorphic_on_exp [holomorphic_intros]: "exp holomorphic_on s"
-  by (simp add: complex_differentiable_within_exp holomorphic_on_def)
+  by (simp add: field_differentiable_within_exp holomorphic_on_def)
 
 subsection\<open>Euler and de Moivre formulas.\<close>
 
@@ -158,23 +153,23 @@
 lemma cnj_cos: "cnj(cos z) = cos(cnj z)"
   by (simp add: cos_exp_eq exp_cnj field_simps)
 
-lemma complex_differentiable_at_sin: "sin complex_differentiable at z"
-  using DERIV_sin complex_differentiable_def by blast
-
-lemma complex_differentiable_within_sin: "sin complex_differentiable (at z within s)"
-  by (simp add: complex_differentiable_at_sin complex_differentiable_at_within)
-
-lemma complex_differentiable_at_cos: "cos complex_differentiable at z"
-  using DERIV_cos complex_differentiable_def by blast
-
-lemma complex_differentiable_within_cos: "cos complex_differentiable (at z within s)"
-  by (simp add: complex_differentiable_at_cos complex_differentiable_at_within)
+lemma field_differentiable_at_sin: "sin field_differentiable at z"
+  using DERIV_sin field_differentiable_def by blast
+
+lemma field_differentiable_within_sin: "sin field_differentiable (at z within s)"
+  by (simp add: field_differentiable_at_sin field_differentiable_at_within)
+
+lemma field_differentiable_at_cos: "cos field_differentiable at z"
+  using DERIV_cos field_differentiable_def by blast
+
+lemma field_differentiable_within_cos: "cos field_differentiable (at z within s)"
+  by (simp add: field_differentiable_at_cos field_differentiable_at_within)
 
 lemma holomorphic_on_sin: "sin holomorphic_on s"
-  by (simp add: complex_differentiable_within_sin holomorphic_on_def)
+  by (simp add: field_differentiable_within_sin holomorphic_on_def)
 
 lemma holomorphic_on_cos: "cos holomorphic_on s"
-  by (simp add: complex_differentiable_within_cos holomorphic_on_def)
+  by (simp add: field_differentiable_within_cos holomorphic_on_def)
 
 subsection\<open>Get a nice real/imaginary separation in Euler's formula.\<close>
 
@@ -887,13 +882,13 @@
 lemma cnj_tan: "cnj(tan z) = tan(cnj z)"
   by (simp add: cnj_cos cnj_sin tan_def)
 
-lemma complex_differentiable_at_tan: "~(cos z = 0) \<Longrightarrow> tan complex_differentiable at z"
-  unfolding complex_differentiable_def
+lemma field_differentiable_at_tan: "~(cos z = 0) \<Longrightarrow> tan field_differentiable at z"
+  unfolding field_differentiable_def
   using DERIV_tan by blast
 
-lemma complex_differentiable_within_tan: "~(cos z = 0)
-         \<Longrightarrow> tan complex_differentiable (at z within s)"
-  using complex_differentiable_at_tan complex_differentiable_at_within by blast
+lemma field_differentiable_within_tan: "~(cos z = 0)
+         \<Longrightarrow> tan field_differentiable (at z within s)"
+  using field_differentiable_at_tan field_differentiable_at_within by blast
 
 lemma continuous_within_tan: "~(cos z = 0) \<Longrightarrow> continuous (at z within s) tan"
   using continuous_at_imp_continuous_within isCont_tan by blast
@@ -902,7 +897,7 @@
   by (simp add: continuous_at_imp_continuous_on)
 
 lemma holomorphic_on_tan: "(\<And>z. z \<in> s \<Longrightarrow> ~(cos z = 0)) \<Longrightarrow> tan holomorphic_on s"
-  by (simp add: complex_differentiable_within_tan holomorphic_on_def)
+  by (simp add: field_differentiable_within_tan holomorphic_on_def)
 
 
 subsection\<open>Complex logarithms (the conventional principal value)\<close>
@@ -1033,28 +1028,28 @@
     by (metis (no_types) Im_exp Ln_in_Reals assms complex_nonpos_Reals_iff complex_is_Real_iff exp_Ln mult_zero_right not_less pi_neq_zero sin_pi znz)
   then show *: "Im (Ln z) < pi" using assms Im_Ln_le_pi
     by (simp add: le_neq_trans znz)
-  show "(Ln has_field_derivative inverse(z)) (at z)"
+  have "(exp has_field_derivative z) (at (Ln z))"
+    by (metis znz DERIV_exp exp_Ln)
+  then show "(Ln has_field_derivative inverse(z)) (at z)"
     apply (rule has_complex_derivative_inverse_strong_x
-              [where f = exp and s = "{w. -pi < Im(w) & Im(w) < pi}"])
+              [where s = "{w. -pi < Im(w) \<and> Im(w) < pi}"])
     using znz *
-    apply (auto simp: continuous_on_exp open_Collect_conj open_halfspace_Im_gt open_halfspace_Im_lt)
-    apply (metis DERIV_exp exp_Ln)
-    apply (metis mpi_less_Im_Ln)
+    apply (auto simp: Transcendental.continuous_on_exp [OF continuous_on_id] open_Collect_conj open_halfspace_Im_gt open_halfspace_Im_lt mpi_less_Im_Ln)
     done
 qed
 
 declare has_field_derivative_Ln [derivative_intros]
 declare has_field_derivative_Ln [THEN DERIV_chain2, derivative_intros]
 
-lemma complex_differentiable_at_Ln: "z \<notin> \<real>\<^sub>\<le>\<^sub>0 \<Longrightarrow> Ln complex_differentiable at z"
-  using complex_differentiable_def has_field_derivative_Ln by blast
-
-lemma complex_differentiable_within_Ln: "z \<notin> \<real>\<^sub>\<le>\<^sub>0
-         \<Longrightarrow> Ln complex_differentiable (at z within s)"
-  using complex_differentiable_at_Ln complex_differentiable_within_subset by blast
+lemma field_differentiable_at_Ln: "z \<notin> \<real>\<^sub>\<le>\<^sub>0 \<Longrightarrow> Ln field_differentiable at z"
+  using field_differentiable_def has_field_derivative_Ln by blast
+
+lemma field_differentiable_within_Ln: "z \<notin> \<real>\<^sub>\<le>\<^sub>0
+         \<Longrightarrow> Ln field_differentiable (at z within s)"
+  using field_differentiable_at_Ln field_differentiable_within_subset by blast
 
 lemma continuous_at_Ln: "z \<notin> \<real>\<^sub>\<le>\<^sub>0 \<Longrightarrow> continuous (at z) Ln"
-  by (simp add: complex_differentiable_imp_continuous_at complex_differentiable_within_Ln)
+  by (simp add: field_differentiable_imp_continuous_at field_differentiable_within_Ln)
 
 lemma isCont_Ln' [simp]:
    "\<lbrakk>isCont f z; f z \<notin> \<real>\<^sub>\<le>\<^sub>0\<rbrakk> \<Longrightarrow> isCont (\<lambda>x. Ln (f x)) z"
@@ -1067,7 +1062,7 @@
   by (simp add: continuous_at_imp_continuous_on continuous_within_Ln)
 
 lemma holomorphic_on_Ln: "(\<And>z. z \<in> s \<Longrightarrow> z \<notin> \<real>\<^sub>\<le>\<^sub>0) \<Longrightarrow> Ln holomorphic_on s"
-  by (simp add: complex_differentiable_within_Ln holomorphic_on_def)
+  by (simp add: field_differentiable_within_Ln holomorphic_on_def)
 
 
 subsection\<open>Quadrant-type results for Ln\<close>
@@ -1163,11 +1158,11 @@
 
 text\<open>A reference to the set of positive real numbers\<close>
 lemma Im_Ln_eq_0: "z \<noteq> 0 \<Longrightarrow> (Im(Ln z) = 0 \<longleftrightarrow> 0 < Re(z) \<and> Im(z) = 0)"
-by (metis Im_complex_of_real Im_exp Ln_in_Reals Re_Ln_pos_lt Re_Ln_pos_lt_imp 
+by (metis Im_complex_of_real Im_exp Ln_in_Reals Re_Ln_pos_lt Re_Ln_pos_lt_imp
           Re_complex_of_real complex_is_Real_iff exp_Ln exp_of_real pi_gt_zero)
 
 lemma Im_Ln_eq_pi: "z \<noteq> 0 \<Longrightarrow> (Im(Ln z) = pi \<longleftrightarrow> Re(z) < 0 \<and> Im(z) = 0)"
-by (metis Im_Ln_eq_0 Im_Ln_pos_le Im_Ln_pos_lt add.left_neutral complex_eq less_eq_real_def 
+by (metis Im_Ln_eq_0 Im_Ln_pos_le Im_Ln_pos_lt add.left_neutral complex_eq less_eq_real_def
     mult_zero_right not_less_iff_gr_or_eq pi_ge_zero pi_neq_zero rcis_zero_arg rcis_zero_mod)
 
 
@@ -1178,7 +1173,7 @@
   apply (rule exp_complex_eqI)
   apply (auto simp: abs_if split: if_split_asm)
   using Im_Ln_less_pi Im_Ln_le_pi apply force
-  apply (metis complex_cnj_zero_iff diff_minus_eq_add diff_strict_mono minus_less_iff 
+  apply (metis complex_cnj_zero_iff diff_minus_eq_add diff_strict_mono minus_less_iff
           mpi_less_Im_Ln mult.commute mult_2_right)
   by (metis exp_Ln exp_cnj)
 
@@ -1267,7 +1262,7 @@
     done
   also have "... = - Ln (- z) + \<i> * complex_of_real pi"
     apply (subst Ln_inverse)
-    using z by (auto simp add: complex_nonneg_Reals_iff) 
+    using z by (auto simp add: complex_nonneg_Reals_iff)
   also have "... = - (Ln z) + \<i> * 2 * complex_of_real pi"
     apply (subst Ln_minus [OF assms])
     using assms z
@@ -1340,7 +1335,7 @@
   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
   consider "Re z < 0" | "Im z \<noteq> 0" using assms
-    using complex_nonneg_Reals_iff not_le by blast 
+    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)
   show ?thesis
@@ -1375,7 +1370,7 @@
       by (auto intro!: derivative_eq_intros simp: complex_nonpos_Reals_iff)
     moreover have "(?F has_field_derivative ?F' z) (at z)" using t r
       by (intro termdiffs_strong[of _ t] summable_in_conv_radius) simp_all
-    ultimately have "((\<lambda>z. ln (1 + z) - ?F z) has_field_derivative (inverse (1 + z) - ?F' z)) 
+    ultimately have "((\<lambda>z. ln (1 + z) - ?F z) has_field_derivative (inverse (1 + z) - ?F' z))
                        (at z within ball 0 1)"
       by (intro derivative_intros) (simp_all add: at_within_open[OF z'])
     also have "(\<lambda>n. of_nat n * ?f n * z ^ (n - Suc 0)) sums ?F' z" using t r
@@ -1412,13 +1407,13 @@
   also have A: "summable (\<lambda>n. norm z^2 * (inverse (real_of_nat (Suc (Suc n))) * cmod z ^ n))"
     by (rule summable_mult, rule summable_comparison_test_ev[OF _ summable_geometric[of "norm z"]])
        (auto simp: assms field_simps intro!: always_eventually)
-  hence "norm (\<Sum>i. (-(z^2)) * inverse (of_nat (i+2)) * (-z)^i) \<le> 
+  hence "norm (\<Sum>i. (-(z^2)) * inverse (of_nat (i+2)) * (-z)^i) \<le>
              (\<Sum>i. norm (-(z^2) * inverse (of_nat (i+2)) * (-z)^i))"
     by (intro summable_norm)
        (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> 
+  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)
@@ -1632,16 +1627,16 @@
   apply (intro derivative_eq_intros | simp add: assms)+
   done
 
-lemma complex_differentiable_powr_right:
+lemma field_differentiable_powr_right:
   fixes w::complex
   shows
-    "w \<noteq> 0 \<Longrightarrow> (\<lambda>z. w powr z) complex_differentiable (at z)"
-using complex_differentiable_def has_field_derivative_powr_right by blast
+    "w \<noteq> 0 \<Longrightarrow> (\<lambda>z. w powr z) field_differentiable (at z)"
+using field_differentiable_def has_field_derivative_powr_right by blast
 
 lemma holomorphic_on_powr_right:
     "f holomorphic_on s \<Longrightarrow> w \<noteq> 0 \<Longrightarrow> (\<lambda>z. w powr (f z)) holomorphic_on s"
-    unfolding holomorphic_on_def complex_differentiable_def
-by (metis (full_types) DERIV_chain' has_field_derivative_powr_right) 
+    unfolding holomorphic_on_def field_differentiable_def
+by (metis (full_types) DERIV_chain' has_field_derivative_powr_right)
 
 lemma norm_powr_real_powr:
   "w \<in> \<real> \<Longrightarrow> 0 < Re w \<Longrightarrow> norm(w powr z) = Re w powr Re z"
@@ -1814,7 +1809,7 @@
 proof (cases "z=0", simp)
   assume "z \<noteq> 0"
   then show ?thesis
-     by (simp add: assms cnj_Ln csqrt_exp_Ln exp_cnj) 
+     by (simp add: assms cnj_Ln csqrt_exp_Ln exp_cnj)
 qed
 
 lemma has_field_derivative_csqrt:
@@ -1839,17 +1834,17 @@
     done
 qed
 
-lemma complex_differentiable_at_csqrt:
-    "z \<notin> \<real>\<^sub>\<le>\<^sub>0 \<Longrightarrow> csqrt complex_differentiable at z"
-  using complex_differentiable_def has_field_derivative_csqrt by blast
-
-lemma complex_differentiable_within_csqrt:
-    "z \<notin> \<real>\<^sub>\<le>\<^sub>0 \<Longrightarrow> csqrt complex_differentiable (at z within s)"
-  using complex_differentiable_at_csqrt complex_differentiable_within_subset by blast
+lemma field_differentiable_at_csqrt:
+    "z \<notin> \<real>\<^sub>\<le>\<^sub>0 \<Longrightarrow> csqrt field_differentiable at z"
+  using field_differentiable_def has_field_derivative_csqrt by blast
+
+lemma field_differentiable_within_csqrt:
+    "z \<notin> \<real>\<^sub>\<le>\<^sub>0 \<Longrightarrow> csqrt field_differentiable (at z within s)"
+  using field_differentiable_at_csqrt field_differentiable_within_subset by blast
 
 lemma continuous_at_csqrt:
     "z \<notin> \<real>\<^sub>\<le>\<^sub>0 \<Longrightarrow> continuous (at z) csqrt"
-  by (simp add: complex_differentiable_within_csqrt complex_differentiable_imp_continuous_at)
+  by (simp add: field_differentiable_within_csqrt field_differentiable_imp_continuous_at)
 
 corollary isCont_csqrt' [simp]:
    "\<lbrakk>isCont f z; f z \<notin> \<real>\<^sub>\<le>\<^sub>0\<rbrakk> \<Longrightarrow> isCont (\<lambda>x. csqrt (f x)) z"
@@ -1857,7 +1852,7 @@
 
 lemma continuous_within_csqrt:
     "z \<notin> \<real>\<^sub>\<le>\<^sub>0 \<Longrightarrow> continuous (at z within s) csqrt"
-  by (simp add: complex_differentiable_imp_continuous_at complex_differentiable_within_csqrt)
+  by (simp add: field_differentiable_imp_continuous_at field_differentiable_within_csqrt)
 
 lemma continuous_on_csqrt [continuous_intros]:
     "(\<And>z. z \<in> s \<Longrightarrow> z \<notin> \<real>\<^sub>\<le>\<^sub>0) \<Longrightarrow> continuous_on s csqrt"
@@ -1865,7 +1860,7 @@
 
 lemma holomorphic_on_csqrt:
     "(\<And>z. z \<in> s \<Longrightarrow> z \<notin> \<real>\<^sub>\<le>\<^sub>0) \<Longrightarrow> csqrt holomorphic_on s"
-  by (simp add: complex_differentiable_within_csqrt holomorphic_on_def)
+  by (simp add: field_differentiable_within_csqrt holomorphic_on_def)
 
 lemma continuous_within_closed_nontrivial:
     "closed s \<Longrightarrow> a \<notin> s ==> continuous (at a within s) f"
@@ -1875,7 +1870,7 @@
 lemma continuous_within_csqrt_posreal:
     "continuous (at z within (\<real> \<inter> {w. 0 \<le> Re(w)})) csqrt"
 proof (cases "z \<in> \<real>\<^sub>\<le>\<^sub>0")
-  case True 
+  case True
   then have "Im z = 0" "Re z < 0 \<or> z = 0"
     using cnj.code complex_cnj_zero_iff  by (auto simp: complex_nonpos_Reals_iff) fastforce
   then show ?thesis
@@ -2013,20 +2008,20 @@
     done
 qed
 
-lemma complex_differentiable_at_Arctan: "(Re z = 0 \<Longrightarrow> \<bar>Im z\<bar> < 1) \<Longrightarrow> Arctan complex_differentiable at z"
+lemma field_differentiable_at_Arctan: "(Re z = 0 \<Longrightarrow> \<bar>Im z\<bar> < 1) \<Longrightarrow> Arctan field_differentiable at z"
   using has_field_derivative_Arctan
-  by (auto simp: complex_differentiable_def)
-
-lemma complex_differentiable_within_Arctan:
-    "(Re z = 0 \<Longrightarrow> \<bar>Im z\<bar> < 1) \<Longrightarrow> Arctan complex_differentiable (at z within s)"
-  using complex_differentiable_at_Arctan complex_differentiable_at_within by blast
+  by (auto simp: field_differentiable_def)
+
+lemma field_differentiable_within_Arctan:
+    "(Re z = 0 \<Longrightarrow> \<bar>Im z\<bar> < 1) \<Longrightarrow> Arctan field_differentiable (at z within s)"
+  using field_differentiable_at_Arctan field_differentiable_at_within by blast
 
 declare has_field_derivative_Arctan [derivative_intros]
 declare has_field_derivative_Arctan [THEN DERIV_chain2, derivative_intros]
 
 lemma continuous_at_Arctan:
     "(Re z = 0 \<Longrightarrow> \<bar>Im z\<bar> < 1) \<Longrightarrow> continuous (at z) Arctan"
-  by (simp add: complex_differentiable_imp_continuous_at complex_differentiable_within_Arctan)
+  by (simp add: field_differentiable_imp_continuous_at field_differentiable_within_Arctan)
 
 lemma continuous_within_Arctan:
     "(Re z = 0 \<Longrightarrow> \<bar>Im z\<bar> < 1) \<Longrightarrow> continuous (at z within s) Arctan"
@@ -2038,7 +2033,7 @@
 
 lemma holomorphic_on_Arctan:
     "(\<And>z. z \<in> s \<Longrightarrow> Re z = 0 \<Longrightarrow> \<bar>Im z\<bar> < 1) \<Longrightarrow> Arctan holomorphic_on s"
-  by (simp add: complex_differentiable_within_Arctan holomorphic_on_def)
+  by (simp add: field_differentiable_within_Arctan holomorphic_on_def)
 
 lemma Arctan_series:
   assumes z: "norm (z :: complex) < 1"
@@ -2051,20 +2046,20 @@
   have summable: "summable (\<lambda>n. g n * u^n)" if "norm u < 1" for u
   proof (cases "u = 0")
     assume u: "u \<noteq> 0"
-    have "(\<lambda>n. ereal (norm (h u n) / norm (h u (Suc n)))) = (\<lambda>n. ereal (inverse (norm u)^2) * 
+    have "(\<lambda>n. ereal (norm (h u n) / norm (h u (Suc n)))) = (\<lambda>n. ereal (inverse (norm u)^2) *
               ereal ((2 + inverse (real (Suc n))) / (2 - inverse (real (Suc n)))))"
     proof
       fix n
-      have "ereal (norm (h u n) / norm (h u (Suc n))) = 
-             ereal (inverse (norm u)^2) * ereal ((of_nat (2*Suc n+1) / of_nat (Suc n)) / 
+      have "ereal (norm (h u n) / norm (h u (Suc n))) =
+             ereal (inverse (norm u)^2) * ereal ((of_nat (2*Suc n+1) / of_nat (Suc n)) /
                  (of_nat (2*Suc n-1) / of_nat (Suc n)))"
-      by (simp add: h_def norm_mult norm_power norm_divide divide_simps 
+      by (simp add: h_def norm_mult norm_power norm_divide divide_simps
                     power2_eq_square eval_nat_numeral del: of_nat_add of_nat_Suc)
       also have "of_nat (2*Suc n+1) / of_nat (Suc n) = (2::real) + inverse (real (Suc n))"
         by (auto simp: divide_simps simp del: of_nat_Suc) simp_all?
       also have "of_nat (2*Suc n-1) / of_nat (Suc n) = (2::real) - inverse (real (Suc n))"
-        by (auto simp: divide_simps simp del: of_nat_Suc) simp_all?      
-      finally show "ereal (norm (h u n) / norm (h u (Suc n))) = ereal (inverse (norm u)^2) * 
+        by (auto simp: divide_simps simp del: of_nat_Suc) simp_all?
+      finally show "ereal (norm (h u n) / norm (h u (Suc n))) = ereal (inverse (norm u)^2) *
               ereal ((2 + inverse (real (Suc n))) / (2 - inverse (real (Suc n))))" .
     qed
     also have "\<dots> \<longlonglongrightarrow> ereal (inverse (norm u)^2) * ereal ((2 + 0) / (2 - 0))"
@@ -2076,7 +2071,7 @@
     ultimately have A: "liminf (\<lambda>n. ereal (cmod (h u n) / cmod (h u (Suc n)))) > 1" by simp
     from u have "summable (h u)"
       by (intro summable_norm_cancel[OF ratio_test_convergence[OF _ A]])
-         (auto simp: h_def norm_divide norm_mult norm_power simp del: of_nat_Suc 
+         (auto simp: h_def norm_divide norm_mult norm_power simp del: of_nat_Suc
                intro!: mult_pos_pos divide_pos_pos always_eventually)
     thus "summable (\<lambda>n. g n * u^n)"
       by (subst summable_mono_reindex[of "\<lambda>n. 2*n+1", symmetric])
@@ -2095,10 +2090,10 @@
     also have "(\<lambda>n. diffs g n * u^n) = (\<lambda>n. if even n then (\<i>*u)^n else 0)"
       by (intro ext) (simp_all del: of_nat_Suc add: g_def diffs_def power_mult_distrib)
     also have "suminf \<dots> = (\<Sum>n. (-(u^2))^n)"
-      by (subst suminf_mono_reindex[of "\<lambda>n. 2*n", symmetric]) 
+      by (subst suminf_mono_reindex[of "\<lambda>n. 2*n", symmetric])
          (auto elim!: evenE simp: subseq_def power_mult power_mult_distrib)
     also from u have "norm u^2 < 1^2" by (intro power_strict_mono) simp_all
-    hence "(\<Sum>n. (-(u^2))^n) = inverse (1 + u^2)" 
+    hence "(\<Sum>n. (-(u^2))^n) = inverse (1 + u^2)"
       by (subst suminf_geometric) (simp_all add: norm_power inverse_eq_divide)
     finally have "(G has_field_derivative inverse (1 + u\<^sup>2)) (at u)" .
     from DERIV_diff[OF has_field_derivative_Arctan this] Im_u u
@@ -2126,12 +2121,12 @@
   hence "norm (\<i> * y) < 1" unfolding y_def by (subst norm_mult) simp
   hence "(\<lambda>n. (-2*\<i>) * ((-1)^n / of_nat (2*n+1) * (\<i>*y)^(2*n+1))) sums ((-2*\<i>) * Arctan (\<i>*y))"
     by (intro Arctan_series sums_mult) simp_all
-  also have "(\<lambda>n. (-2*\<i>) * ((-1)^n / of_nat (2*n+1) * (\<i>*y)^(2*n+1))) = 
+  also have "(\<lambda>n. (-2*\<i>) * ((-1)^n / of_nat (2*n+1) * (\<i>*y)^(2*n+1))) =
                  (\<lambda>n. (-2*\<i>) * ((-1)^n * (\<i>*y*(-y\<^sup>2)^n)/of_nat (2*n+1)))"
     by (intro ext) (simp_all add: power_mult power_mult_distrib)
   also have "\<dots> = (\<lambda>n. 2*y* ((-1) * (-y\<^sup>2))^n/of_nat (2*n+1))"
     by (intro ext, subst power_mult_distrib) (simp add: algebra_simps power_mult)
-  also have "\<dots> = (\<lambda>n. 2*y^(2*n+1) / of_nat (2*n+1))" 
+  also have "\<dots> = (\<lambda>n. 2*y^(2*n+1) / of_nat (2*n+1))"
     by (subst power_add, subst power_mult) (simp add: mult_ac)
   also have "\<dots> = (\<lambda>n. of_real (2*((x-1)/(x+1))^(2*n+1) / of_nat (2*n+1)))"
     by (intro ext) (simp add: y_def)
@@ -2261,7 +2256,7 @@
   { fix w::complex and z::complex
     assume *: "w \<in> \<real>" "z \<in> \<real>"
     have "cmod (Arctan w - Arctan z) \<le> 1 * cmod (w-z)"
-      apply (rule complex_differentiable_bound [OF convex_Reals, of Arctan _ 1])
+      apply (rule field_differentiable_bound [OF convex_Reals, of Arctan _ 1])
       apply (rule has_field_derivative_at_within [OF has_field_derivative_Arctan])
       apply (force simp add: Reals_def)
       apply (simp add: norm_divide divide_simps in_Reals_norm complex_is_Real_iff power2_eq_square)
@@ -2303,7 +2298,7 @@
 lemma one_minus_z2_notin_nonpos_Reals:
   assumes "(Im z = 0 \<Longrightarrow> \<bar>Re z\<bar> < 1)"
   shows "1 - z\<^sup>2 \<notin> \<real>\<^sub>\<le>\<^sub>0"
-    using assms  
+    using assms
     apply (auto simp: complex_nonpos_Reals_iff Re_power2 Im_power2)
     using power2_less_0 [of "Im z"] apply force
     using abs_square_less_1 not_le by blast
@@ -2441,13 +2436,13 @@
 declare has_field_derivative_Arcsin [derivative_intros]
 declare has_field_derivative_Arcsin [THEN DERIV_chain2, derivative_intros]
 
-lemma complex_differentiable_at_Arcsin:
-    "(Im z = 0 \<Longrightarrow> \<bar>Re z\<bar> < 1) \<Longrightarrow> Arcsin complex_differentiable at z"
-  using complex_differentiable_def has_field_derivative_Arcsin by blast
-
-lemma complex_differentiable_within_Arcsin:
-    "(Im z = 0 \<Longrightarrow> \<bar>Re z\<bar> < 1) \<Longrightarrow> Arcsin complex_differentiable (at z within s)"
-  using complex_differentiable_at_Arcsin complex_differentiable_within_subset by blast
+lemma field_differentiable_at_Arcsin:
+    "(Im z = 0 \<Longrightarrow> \<bar>Re z\<bar> < 1) \<Longrightarrow> Arcsin field_differentiable at z"
+  using field_differentiable_def has_field_derivative_Arcsin by blast
+
+lemma field_differentiable_within_Arcsin:
+    "(Im z = 0 \<Longrightarrow> \<bar>Re z\<bar> < 1) \<Longrightarrow> Arcsin field_differentiable (at z within s)"
+  using field_differentiable_at_Arcsin field_differentiable_within_subset by blast
 
 lemma continuous_within_Arcsin:
     "(Im z = 0 \<Longrightarrow> \<bar>Re z\<bar> < 1) \<Longrightarrow> continuous (at z within s) Arcsin"
@@ -2458,7 +2453,7 @@
   by (simp add: continuous_at_imp_continuous_on)
 
 lemma holomorphic_on_Arcsin: "(\<And>z. z \<in> s \<Longrightarrow> Im z = 0 \<Longrightarrow> \<bar>Re z\<bar> < 1) \<Longrightarrow> Arcsin holomorphic_on s"
-  by (simp add: complex_differentiable_within_Arcsin holomorphic_on_def)
+  by (simp add: field_differentiable_within_Arcsin holomorphic_on_def)
 
 
 subsection\<open>Inverse Cosine\<close>
@@ -2483,7 +2478,7 @@
 
 text\<open>A very tricky argument to find!\<close>
 lemma isCont_Arccos_lemma:
-  assumes eq0: "Im (z + \<i> * csqrt (1 - z\<^sup>2)) = 0" and "(Im z = 0 \<Longrightarrow> \<bar>Re z\<bar> < 1)" 
+  assumes eq0: "Im (z + \<i> * csqrt (1 - z\<^sup>2)) = 0" and "(Im z = 0 \<Longrightarrow> \<bar>Re z\<bar> < 1)"
     shows False
 proof (cases "Im z = 0")
   case True
@@ -2608,13 +2603,13 @@
 declare has_field_derivative_Arcsin [derivative_intros]
 declare has_field_derivative_Arcsin [THEN DERIV_chain2, derivative_intros]
 
-lemma complex_differentiable_at_Arccos:
-    "(Im z = 0 \<Longrightarrow> \<bar>Re z\<bar> < 1) \<Longrightarrow> Arccos complex_differentiable at z"
-  using complex_differentiable_def has_field_derivative_Arccos by blast
-
-lemma complex_differentiable_within_Arccos:
-    "(Im z = 0 \<Longrightarrow> \<bar>Re z\<bar> < 1) \<Longrightarrow> Arccos complex_differentiable (at z within s)"
-  using complex_differentiable_at_Arccos complex_differentiable_within_subset by blast
+lemma field_differentiable_at_Arccos:
+    "(Im z = 0 \<Longrightarrow> \<bar>Re z\<bar> < 1) \<Longrightarrow> Arccos field_differentiable at z"
+  using field_differentiable_def has_field_derivative_Arccos by blast
+
+lemma field_differentiable_within_Arccos:
+    "(Im z = 0 \<Longrightarrow> \<bar>Re z\<bar> < 1) \<Longrightarrow> Arccos field_differentiable (at z within s)"
+  using field_differentiable_at_Arccos field_differentiable_within_subset by blast
 
 lemma continuous_within_Arccos:
     "(Im z = 0 \<Longrightarrow> \<bar>Re z\<bar> < 1) \<Longrightarrow> continuous (at z within s) Arccos"
@@ -2625,7 +2620,7 @@
   by (simp add: continuous_at_imp_continuous_on)
 
 lemma holomorphic_on_Arccos: "(\<And>z. z \<in> s \<Longrightarrow> Im z = 0 \<Longrightarrow> \<bar>Re z\<bar> < 1) \<Longrightarrow> Arccos holomorphic_on s"
-  by (simp add: complex_differentiable_within_Arccos holomorphic_on_def)
+  by (simp add: field_differentiable_within_Arccos holomorphic_on_def)
 
 
 subsection\<open>Upper and Lower Bounds for Inverse Sine and Cosine\<close>
diff -r bc25f3916a99 -r 6855b348e828 src/HOL/Multivariate_Analysis/Conformal_Mappings.thy
--- a/src/HOL/Multivariate_Analysis/Conformal_Mappings.thy	Mon Mar 07 14:34:45 2016 +0000
+++ b/src/HOL/Multivariate_Analysis/Conformal_Mappings.thy	Mon Mar 07 15:57:02 2016 +0000
@@ -671,7 +671,7 @@
     by (auto intro: holomorphic_factor_order_of_zero [OF assms])
   have con: "continuous_on (ball \<xi> r) (\<lambda>z. deriv g z / g z)"
     by (rule continuous_intros) (auto simp: gne holg holomorphic_deriv holomorphic_on_imp_continuous_on)
-  have cd: "\<And>x. dist \<xi> x < r \<Longrightarrow> (\<lambda>z. deriv g z / g z) complex_differentiable at x"
+  have cd: "\<And>x. dist \<xi> x < r \<Longrightarrow> (\<lambda>z. deriv g z / g z) field_differentiable at x"
     apply (rule derivative_intros)+
     using holg mem_ball apply (blast intro: holomorphic_deriv holomorphic_on_imp_differentiable_at)
     apply (metis Topology_Euclidean_Space.open_ball at_within_open holg holomorphic_on_def mem_ball)
@@ -687,7 +687,7 @@
     by (auto intro!: continuous_intros simp add: holg holomorphic_on_imp_continuous_on gne)
   have 0: "dist \<xi> x < r \<Longrightarrow> ((\<lambda>x. exp (h x) / g x) has_field_derivative 0) (at x)" for x
     apply (rule h derivative_eq_intros | simp)+
-    apply (rule DERIV_deriv_iff_complex_differentiable [THEN iffD2])
+    apply (rule DERIV_deriv_iff_field_differentiable [THEN iffD2])
     using holg apply (auto simp: holomorphic_on_imp_differentiable_at gne h)
     done
   obtain c where c: "\<And>x. x \<in> ball \<xi> r \<Longrightarrow> exp (h x) / g x = c"
@@ -852,15 +852,15 @@
     have holh: "h holomorphic_on S"
     proof (simp add: holomorphic_on_def, clarify)
       fix z assume "z \<in> S"
-      show "h complex_differentiable at z within S"
+      show "h field_differentiable at z within S"
       proof (cases "z = \<xi>")
         case True then show ?thesis
-          using complex_differentiable_at_within complex_differentiable_def h0 by blast
+          using field_differentiable_at_within field_differentiable_def h0 by blast
       next
         case False
-        then have "f complex_differentiable at z within S"
+        then have "f field_differentiable at z within S"
           using holomorphic_onD [OF holf, of z] \<open>z \<in> S\<close>
-          unfolding complex_differentiable_def DERIV_within_iff
+          unfolding field_differentiable_def DERIV_within_iff
           by (force intro: exI [where x="dist \<xi> z"] elim: Lim_transform_within_set [unfolded eventually_at])
         then show ?thesis
           by (simp add: h_def power2_eq_square derivative_intros)
@@ -1131,7 +1131,7 @@
     apply (rule has_derivative_locally_injective [OF S, where f=f and f' = "\<lambda>z h. deriv f z * h" and g' = g'])
     using g' *
     apply (simp_all add: linear_conv_bounded_linear that)
-    using DERIV_deriv_iff_complex_differentiable has_field_derivative_imp_has_derivative holf
+    using DERIV_deriv_iff_field_differentiable has_field_derivative_imp_has_derivative holf
         holomorphic_on_imp_differentiable_at \<open>open S\<close> apply blast
     done
 qed
@@ -1204,7 +1204,7 @@
         using holg by (simp add: holomorphic_on_subset subset_ball)
       have gd: "\<And>w. dist \<xi> w < \<delta> \<Longrightarrow> (g has_field_derivative deriv g w) (at w)"
         using holg
-        by (simp add: DERIV_deriv_iff_complex_differentiable holomorphic_on_def at_within_open_NO_MATCH)
+        by (simp add: DERIV_deriv_iff_field_differentiable holomorphic_on_def at_within_open_NO_MATCH)
       have *: "\<And>w. w \<in> ball \<xi> (min r \<delta>)
             \<Longrightarrow> ((\<lambda>w. (w - \<xi>) * g w) has_field_derivative ((w - \<xi>) * deriv g w + g w))
                 (at w)"
@@ -1266,7 +1266,7 @@
   have *: "(the_inv_into S f has_field_derivative inverse (deriv f z)) (at (f z))" if "z \<in> S" for z
   proof -
     have 1: "(f has_field_derivative deriv f z) (at z)"
-      using DERIV_deriv_iff_complex_differentiable \<open>z \<in> S\<close> \<open>open S\<close> holf holomorphic_on_imp_differentiable_at
+      using DERIV_deriv_iff_field_differentiable \<open>z \<in> S\<close> \<open>open S\<close> holf holomorphic_on_imp_differentiable_at
       by blast
     have 2: "deriv f z \<noteq> 0"
       using \<open>z \<in> S\<close> \<open>open S\<close> holf holomorphic_injective_imp_regular injf by blast
@@ -1524,7 +1524,7 @@
   have 3: "contour_integral (reversepath (linepath b' a')) f =
                 - contour_integral (linepath b' a') f"
     by (rule contour_integral_reversepath [OF valid_path_linepath])
-  have fcd_le: "f complex_differentiable at x"
+  have fcd_le: "f field_differentiable at x"
                if "x \<in> interior S \<and> x \<in> interior {x. d \<bullet> x \<le> k}" for x
   proof -
     have "f holomorphic_on S \<inter> {c. d \<bullet> c < k}"
@@ -1532,7 +1532,7 @@
     then have "\<exists>C D. x \<in> interior C \<inter> interior D \<and> f holomorphic_on interior C \<inter> interior D"
       using that
       by (metis Collect_mem_eq Int_Collect \<open>d \<noteq> 0\<close> interior_halfspace_le interior_open \<open>open S\<close>)
-    then show "f complex_differentiable at x"
+    then show "f field_differentiable at x"
       by (metis at_within_interior holomorphic_on_def interior_Int interior_interior)
   qed
   have ab_le: "\<And>x. x \<in> closed_segment a b \<Longrightarrow> d \<bullet> x \<le> k"
@@ -1557,7 +1557,7 @@
                 contour_integral (linepath a' b') f +
                 contour_integral (linepath b' a) f = 0"
     by (rule has_chain_integral_chain_integral4)
-  have fcd_ge: "f complex_differentiable at x"
+  have fcd_ge: "f field_differentiable at x"
                if "x \<in> interior S \<and> x \<in> interior {x. k \<le> d \<bullet> x}" for x
   proof -
     have f2: "f holomorphic_on S \<inter> {c. k < d \<bullet> c}"
@@ -1566,7 +1566,7 @@
       by (simp add: interior_open \<open>open S\<close>)
     then have "x \<in> S \<inter> interior {c. k \<le> d \<bullet> c}"
       using that by simp
-    then show "f complex_differentiable at x"
+    then show "f field_differentiable at x"
       using f3 f2 unfolding holomorphic_on_def
       by (metis (no_types) \<open>d \<noteq> 0\<close> at_within_interior interior_Int interior_halfspace_ge interior_interior)
   qed
@@ -1688,10 +1688,10 @@
     apply (intro continuous_intros continuous_on_compose continuous_on_subset [OF contf])
     using cnjs apply auto
     done
-  have "cnj \<circ> f \<circ> cnj complex_differentiable at x within S \<inter> {z. Im z < 0}"
-        if "x \<in> S" "Im x < 0" "f complex_differentiable at (cnj x) within S \<inter> {z. 0 < Im z}" for x
+  have "cnj \<circ> f \<circ> cnj field_differentiable at x within S \<inter> {z. Im z < 0}"
+        if "x \<in> S" "Im x < 0" "f field_differentiable at (cnj x) within S \<inter> {z. 0 < Im z}" for x
     using that
-    apply (simp add: complex_differentiable_def Derivative.DERIV_within_iff Lim_within dist_norm, clarify)
+    apply (simp add: field_differentiable_def Derivative.DERIV_within_iff Lim_within dist_norm, clarify)
     apply (rule_tac x="cnj f'" in exI)
     apply (elim all_forward ex_forward conj_forward imp_forward asm_rl, clarify)
     apply (drule_tac x="cnj xa" in bspec)
@@ -1902,11 +1902,11 @@
     by (simp add: o_def)
   have hol0: "(\<lambda>z. f (a + z)) holomorphic_on cball 0 r"
     unfolding fz by (intro holomorphic_intros holf holomorphic_on_compose | simp)+
-  then have [simp]: "\<And>x. norm x < r \<Longrightarrow> (\<lambda>z. f (a + z)) complex_differentiable at x"
+  then have [simp]: "\<And>x. norm x < r \<Longrightarrow> (\<lambda>z. f (a + z)) field_differentiable at x"
     by (metis Topology_Euclidean_Space.open_ball at_within_open ball_subset_cball diff_0 dist_norm holomorphic_on_def holomorphic_on_subset mem_ball norm_minus_cancel)
-  have [simp]: "\<And>z. norm z < r \<Longrightarrow> f complex_differentiable at (a + z)"
+  have [simp]: "\<And>z. norm z < r \<Longrightarrow> f field_differentiable at (a + z)"
     by (metis holf open_ball add_diff_cancel_left' dist_complex_def holomorphic_on_imp_differentiable_at holomorphic_on_subset interior_cball interior_subset mem_ball norm_minus_commute)
-  then have [simp]: "f complex_differentiable at a"
+  then have [simp]: "f field_differentiable at a"
     by (metis add.comm_neutral \<open>0 < r\<close> norm_eq_zero)
   have hol1: "(\<lambda>z. f (a + z) - f a) holomorphic_on cball 0 r"
     by (intro holomorphic_intros hol0)
@@ -1920,7 +1920,7 @@
   then show ?thesis
     apply clarify
     apply (drule_tac c="x - f a" in subsetD)
-     apply (force simp: fz \<open>0 < r\<close> dist_norm complex_derivative_chain complex_differentiable_compose)+
+     apply (force simp: fz \<open>0 < r\<close> dist_norm complex_derivative_chain field_differentiable_compose)+
     done
 qed
 
@@ -2026,7 +2026,7 @@
   case False
     def C \<equiv> "deriv f a"
     have "0 < norm C" using False by (simp add: C_def)
-    have dfa: "f complex_differentiable at a"
+    have dfa: "f field_differentiable at a"
       apply (rule holomorphic_on_imp_differentiable_at [OF holf])
       using \<open>0 < r\<close> by auto
     have fo: "(\<lambda>z. f (a + of_real r * z)) = f o (\<lambda>z. (a + of_real r * z))"
@@ -2045,7 +2045,7 @@
     have *: "((\<lambda>x. f (a + of_real r * x)) has_field_derivative
              (deriv f (a + of_real r * z) * of_real r)) (at z)"
         apply (simp add: fo)
-        apply (rule DERIV_chain [OF complex_differentiable_derivI])
+        apply (rule DERIV_chain [OF field_differentiable_derivI])
         apply (rule holomorphic_on_imp_differentiable_at [OF holf], simp)
         using \<open>0 < r\<close> apply (simp add: dist_norm norm_mult that)
         apply (rule derivative_eq_intros | simp)+
@@ -2055,10 +2055,10 @@
         using \<open>0 < r\<close> by (auto simp: C_def False)
     qed
     have 2: "deriv (\<lambda>z. f (a + of_real r * z) / (C * of_real r)) 0 = 1"
-      apply (subst complex_derivative_cdivide_right)
-      apply (simp add: complex_differentiable_def fo)
+      apply (subst deriv_cdivide_right)
+      apply (simp add: field_differentiable_def fo)
       apply (rule exI)
-      apply (rule DERIV_chain [OF complex_differentiable_derivI])
+      apply (rule DERIV_chain [OF field_differentiable_derivI])
       apply (simp add: dfa)
       apply (rule derivative_eq_intros | simp add: C_def False fo)+
       using \<open>0 < r\<close> 
diff -r bc25f3916a99 -r 6855b348e828 src/HOL/Multivariate_Analysis/Gamma.thy
--- a/src/HOL/Multivariate_Analysis/Gamma.thy	Mon Mar 07 14:34:45 2016 +0000
+++ b/src/HOL/Multivariate_Analysis/Gamma.thy	Mon Mar 07 15:57:02 2016 +0000
@@ -1355,21 +1355,21 @@
   "z \<in> \<real> \<Longrightarrow> Gamma z \<in> (\<real> :: complex set)" and rGamma_complex_real: "z \<in> \<real> \<Longrightarrow> rGamma z \<in> \<real>"
   by (simp_all add: Reals_cnj_iff cnj_Gamma cnj_rGamma)
 
-lemma complex_differentiable_rGamma: "rGamma complex_differentiable (at z within A)"
-  using has_field_derivative_rGamma[of z] unfolding complex_differentiable_def by blast
+lemma field_differentiable_rGamma: "rGamma field_differentiable (at z within A)"
+  using has_field_derivative_rGamma[of z] unfolding field_differentiable_def by blast
 
 lemma holomorphic_on_rGamma: "rGamma holomorphic_on A"
-  unfolding holomorphic_on_def by (auto intro!: complex_differentiable_rGamma)
+  unfolding holomorphic_on_def by (auto intro!: field_differentiable_rGamma)
 
 lemma analytic_on_rGamma: "rGamma analytic_on A"
   unfolding analytic_on_def by (auto intro!: exI[of _ 1] holomorphic_on_rGamma)
 
 
-lemma complex_differentiable_Gamma: "z \<notin> \<int>\<^sub>\<le>\<^sub>0 \<Longrightarrow> Gamma complex_differentiable (at z within A)"
-  using has_field_derivative_Gamma[of z] unfolding complex_differentiable_def by auto
+lemma field_differentiable_Gamma: "z \<notin> \<int>\<^sub>\<le>\<^sub>0 \<Longrightarrow> Gamma field_differentiable (at z within A)"
+  using has_field_derivative_Gamma[of z] unfolding field_differentiable_def by auto
 
 lemma holomorphic_on_Gamma: "A \<inter> \<int>\<^sub>\<le>\<^sub>0 = {} \<Longrightarrow> Gamma holomorphic_on A"
-  unfolding holomorphic_on_def by (auto intro!: complex_differentiable_Gamma)
+  unfolding holomorphic_on_def by (auto intro!: field_differentiable_Gamma)
 
 lemma analytic_on_Gamma: "A \<inter> \<int>\<^sub>\<le>\<^sub>0 = {} \<Longrightarrow> Gamma analytic_on A"
   by (rule analytic_on_subset[of _ "UNIV - \<int>\<^sub>\<le>\<^sub>0"], subst analytic_on_open)
@@ -1383,14 +1383,14 @@
 declare has_field_derivative_rGamma_complex'[THEN DERIV_chain2, derivative_intros]
 
 
-lemma complex_differentiable_Polygamma:
+lemma field_differentiable_Polygamma:
   fixes z::complex
   shows
-  "z \<notin> \<int>\<^sub>\<le>\<^sub>0 \<Longrightarrow> Polygamma n complex_differentiable (at z within A)"
-  using has_field_derivative_Polygamma[of z n] unfolding complex_differentiable_def by auto
+  "z \<notin> \<int>\<^sub>\<le>\<^sub>0 \<Longrightarrow> Polygamma n field_differentiable (at z within A)"
+  using has_field_derivative_Polygamma[of z n] unfolding field_differentiable_def by auto
 
 lemma holomorphic_on_Polygamma: "A \<inter> \<int>\<^sub>\<le>\<^sub>0 = {} \<Longrightarrow> Polygamma n holomorphic_on A"
-  unfolding holomorphic_on_def by (auto intro!: complex_differentiable_Polygamma)
+  unfolding holomorphic_on_def by (auto intro!: field_differentiable_Polygamma)
 
 lemma analytic_on_Polygamma: "A \<inter> \<int>\<^sub>\<le>\<^sub>0 = {} \<Longrightarrow> Polygamma n analytic_on A"
   by (rule analytic_on_subset[of _ "UNIV - \<int>\<^sub>\<le>\<^sub>0"], subst analytic_on_open)