author paulson Mon, 07 Mar 2016 15:57:02 +0000 changeset 62534 6855b348e828 parent 62533 bc25f3916a99 child 62535 cb262f03ac12
complex_differentiable -> field_differentiable, etc. (making these theorems also available for type real)
```--- 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 *
@@ -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])
-  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 (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"
-      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 @@
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])
@@ -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
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))"
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
@@ -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])```
```--- 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)"
+lemma field_differentiable_derivI:
+    "f field_differentiable (at x) \<Longrightarrow> (f has_field_derivative deriv f x) (at x)"

-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])

-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)

-  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
+  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

-     "op + c complex_differentiable F"
+     "op + c field_differentiable F"

-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)

-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"

-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)"

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)

"\<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)

-  "\<lbrakk>f complex_differentiable at z; g complex_differentiable at z\<rbrakk>
+  "\<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 (drule DERIV_chain' [of "times c" c z UNIV f "deriv f (c * z)", OF DERIV_cmult_Id])
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"
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)))"
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]```
```--- 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 @@
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"

-lemma continuous_on_exp:
-  fixes s::"'a::{real_normed_field,banach} set"
-  shows "continuous_on s exp"
-
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 @@

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
-  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 @@

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)

@@ -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
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))"
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 (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 @@

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 @@

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>```
```--- 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"
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' *
-    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 @@
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 (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 (rule derivative_eq_intros | simp add: C_def False fo)+
using \<open>0 < r\<close> ```
```--- 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)```