# HG changeset patch
# User immler
# Date 1572966129 18000
# Node ID ddd4aefc540f9f121c807711198014d089d199d9
# Parent  bd3d4702b4f2998ba6607d5a9dc8a583c70284bf# Parent  c1b63124245ca28d52af8273f9caeb8e4ecf4911
merged

diff -r bd3d4702b4f2 -r ddd4aefc540f src/HOL/Analysis/Cauchy_Integral_Theorem.thy
--- a/src/HOL/Analysis/Cauchy_Integral_Theorem.thy	Mon Nov 04 21:41:55 2019 -0500
+++ b/src/HOL/Analysis/Cauchy_Integral_Theorem.thy	Tue Nov 05 10:02:09 2019 -0500
@@ -3,7 +3,11 @@
 text\<open>By John Harrison et al.  Ported from HOL Light by L C Paulson (2015)\<close>
 
 theory Cauchy_Integral_Theorem
-imports Complex_Transcendental Henstock_Kurzweil_Integration Weierstrass_Theorems Retracts
+imports
+  Complex_Transcendental
+  Henstock_Kurzweil_Integration
+  Weierstrass_Theorems
+  Retracts
 begin
 
 lemma leibniz_rule_holomorphic:
@@ -4306,7 +4310,7 @@
     by (auto simp: open_dist)
 qed
 
-subsection\<open>Winding number is zero "outside" a curve, in various senses\<close>
+subsection\<open>Winding number is zero "outside" a curve\<close>
 
 proposition winding_number_zero_in_outside:
   assumes \<gamma>: "path \<gamma>" and loop: "pathfinish \<gamma> = pathstart \<gamma>" and z: "z \<in> outside (path_image \<gamma>)"
@@ -6054,7 +6058,7 @@
 lemma has_complex_derivative_funpow_1:
      "\<lbrakk>(f has_field_derivative 1) (at z); f z = z\<rbrakk> \<Longrightarrow> (f^^n has_field_derivative 1) (at z)"
   apply (induction n, auto)
-  apply (metis DERIV_ident DERIV_transform_at id_apply zero_less_one)
+  apply (simp add: id_def)
   by (metis DERIV_chain comp_funpow comp_id funpow_swap1 mult.right_neutral)
 
 lemma higher_deriv_uminus:
@@ -6068,7 +6072,7 @@
   have *: "((deriv ^^ n) f has_field_derivative deriv ((deriv ^^ n) f) z) (at z)"
     using Suc.prems assms has_field_derivative_higher_deriv by auto
   have "((deriv ^^ n) (\<lambda>w. - f w) has_field_derivative - deriv ((deriv ^^ n) f) z) (at z)"
-    apply (rule DERIV_transform_within_open [of "\<lambda>w. -((deriv ^^ n) f w)"])
+    apply (rule has_field_derivative_transform_within_open [of "\<lambda>w. -((deriv ^^ n) f w)"])
        apply (rule derivative_eq_intros | rule * refl assms)+
      apply (auto simp add: Suc)
     done
@@ -6090,7 +6094,7 @@
     using Suc.prems assms has_field_derivative_higher_deriv by auto
   have "((deriv ^^ n) (\<lambda>w. f w + g w) has_field_derivative
         deriv ((deriv ^^ n) f) z + deriv ((deriv ^^ n) g) z) (at z)"
-    apply (rule DERIV_transform_within_open [of "\<lambda>w. (deriv ^^ n) f w + (deriv ^^ n) g w"])
+    apply (rule has_field_derivative_transform_within_open [of "\<lambda>w. (deriv ^^ n) f w + (deriv ^^ n) g w"])
        apply (rule derivative_eq_intros | rule * refl assms)+
      apply (auto simp add: Suc)
     done
@@ -6133,7 +6137,7 @@
   have "((deriv ^^ n) (\<lambda>w. f w * g w) has_field_derivative
          (\<Sum>i = 0..Suc n. (Suc n choose i) * (deriv ^^ i) f z * (deriv ^^ (Suc n - i)) g z))
         (at z)"
-    apply (rule DERIV_transform_within_open
+    apply (rule has_field_derivative_transform_within_open
         [of "\<lambda>w. (\<Sum>i = 0..n. of_nat (n choose i) * (deriv ^^ i) f w * (deriv ^^ (n - i)) g w)"])
        apply (simp add: algebra_simps)
        apply (rule DERIV_cong [OF DERIV_sum])
@@ -6847,7 +6851,7 @@
       using  summable_sums centre_in_ball \<open>0 < d\<close> \<open>summable h\<close> le_h
       by (metis (full_types) Int_iff gg' summable_def that)
     moreover have "((\<lambda>x. \<Sum>n. f n x) has_field_derivative g' z) (at z)"
-    proof (rule DERIV_transform_at)
+    proof (rule has_field_derivative_transform_within)
       show "\<And>x. dist x z < r \<Longrightarrow> g x = (\<Sum>n. f n x)"
         by (metis subsetD dist_commute gg' mem_ball r sums_unique)
     qed (use \<open>0 < r\<close> gg' \<open>z \<in> S\<close> \<open>0 < d\<close> in auto)
@@ -6975,7 +6979,7 @@
         done
     qed
     have "(f has_field_derivative g' w) (at w)"
-      by (rule DERIV_transform_at [where d="(r - norm(z - w))/2"])
+      by (rule has_field_derivative_transform_within [where d="(r - norm(z - w))/2"])
       (use w gg' [of w] in \<open>(force simp: dist_norm)+\<close>)
     then show ?thesis ..
   qed
diff -r bd3d4702b4f2 -r ddd4aefc540f src/HOL/Analysis/Complex_Analysis_Basics.thy
--- a/src/HOL/Analysis/Complex_Analysis_Basics.thy	Mon Nov 04 21:41:55 2019 -0500
+++ b/src/HOL/Analysis/Complex_Analysis_Basics.thy	Tue Nov 05 10:02:09 2019 -0500
@@ -55,59 +55,9 @@
     shows "uniformly_continuous_on s (\<lambda>x. c * f x)"
 by (metis assms bounded_linear.uniformly_continuous_on bounded_linear_mult_right)
 
-lemma continuous_within_norm_id [continuous_intros]: "continuous (at x within S) norm"
-  by (rule continuous_norm [OF continuous_ident])
-
 lemma continuous_on_norm_id [continuous_intros]: "continuous_on S norm"
   by (intro continuous_on_id continuous_on_norm)
 
-lemma DERIV_zero_unique:
-  assumes "convex S"
-      and d0: "\<And>x. x\<in>S \<Longrightarrow> (f has_field_derivative 0) (at x within S)"
-      and "a \<in> S"
-      and "x \<in> S"
-    shows "f x = f a"
-  by (rule has_derivative_zero_unique [OF assms(1) _ assms(4,3)])
-     (metis d0 has_field_derivative_imp_has_derivative lambda_zero)
-
-lemma DERIV_zero_connected_unique:
-  assumes "connected S"
-      and "open S"
-      and d0: "\<And>x. x\<in>S \<Longrightarrow> DERIV f x :> 0"
-      and "a \<in> S"
-      and "x \<in> S"
-    shows "f x = f a"
-    by (rule has_derivative_zero_unique_connected [OF assms(2,1) _ assms(5,4)])
-       (metis has_field_derivative_def lambda_zero d0)
-
-lemma DERIV_transform_within:
-  assumes "(f has_field_derivative f') (at a within S)"
-      and "0 < d" "a \<in> S"
-      and "\<And>x. x\<in>S \<Longrightarrow> dist x a < d \<Longrightarrow> f x = g x"
-    shows "(g has_field_derivative f') (at a within S)"
-  using assms unfolding has_field_derivative_def
-  by (blast intro: has_derivative_transform_within)
-
-lemma DERIV_transform_within_open:
-  assumes "DERIV f a :> f'"
-      and "open S" "a \<in> S"
-      and "\<And>x. x\<in>S \<Longrightarrow> f x = g x"
-    shows "DERIV g a :> f'"
-  using assms unfolding has_field_derivative_def
-by (metis has_derivative_transform_within_open)
-
-lemma DERIV_transform_at:
-  assumes "DERIV f a :> f'"
-      and "0 < d"
-      and "\<And>x. dist x a < d \<Longrightarrow> f x = g x"
-    shows "DERIV g a :> f'"
-  by (blast intro: assms DERIV_transform_within)
-
-(*generalising DERIV_isconst_all, which requires type real (using the ordering)*)
-lemma DERIV_zero_UNIV_unique:
-  "(\<And>x. DERIV f x :> 0) \<Longrightarrow> f x = f a"
-  by (metis DERIV_zero_unique UNIV_I convex_UNIV)
-
 lemma
   shows open_halfspace_Re_lt: "open {z. Re(z) < b}"
     and open_halfspace_Re_gt: "open {z. Re(z) > b}"
@@ -185,6 +135,43 @@
   assumes "eventually (\<lambda>x. norm(f x) \<le> Re(g x)) F" "(g \<longlongrightarrow> 0) F" shows "(f \<longlongrightarrow> 0) F"
   by (rule Lim_null_comparison[OF assms(1)] tendsto_eq_intros assms(2))+ simp
 
+
+lemma closed_segment_same_Re:
+  assumes "Re a = Re b"
+  shows   "closed_segment a b = {z. Re z = Re a \<and> Im z \<in> closed_segment (Im a) (Im b)}"
+proof safe
+  fix z assume "z \<in> closed_segment a b"
+  then obtain u where u: "u \<in> {0..1}" "z = a + of_real u * (b - a)"
+    by (auto simp: closed_segment_def scaleR_conv_of_real algebra_simps)
+  from assms show "Re z = Re a" by (auto simp: u)
+  from u(1) show "Im z \<in> closed_segment (Im a) (Im b)"
+    by (force simp: u closed_segment_def algebra_simps)
+next
+  fix z assume [simp]: "Re z = Re a" and "Im z \<in> closed_segment (Im a) (Im b)"
+  then obtain u where u: "u \<in> {0..1}" "Im z = Im a + of_real u * (Im b - Im a)"
+    by (auto simp: closed_segment_def scaleR_conv_of_real algebra_simps)
+  from u(1) show "z \<in> closed_segment a b" using assms
+    by (force simp: u closed_segment_def algebra_simps scaleR_conv_of_real complex_eq_iff)
+qed
+
+lemma closed_segment_same_Im:
+  assumes "Im a = Im b"
+  shows   "closed_segment a b = {z. Im z = Im a \<and> Re z \<in> closed_segment (Re a) (Re b)}"
+proof safe
+  fix z assume "z \<in> closed_segment a b"
+  then obtain u where u: "u \<in> {0..1}" "z = a + of_real u * (b - a)"
+    by (auto simp: closed_segment_def scaleR_conv_of_real algebra_simps)
+  from assms show "Im z = Im a" by (auto simp: u)
+  from u(1) show "Re z \<in> closed_segment (Re a) (Re b)"
+    by (force simp: u closed_segment_def algebra_simps)
+next
+  fix z assume [simp]: "Im z = Im a" and "Re z \<in> closed_segment (Re a) (Re b)"
+  then obtain u where u: "u \<in> {0..1}" "Re z = Re a + of_real u * (Re b - Re a)"
+    by (auto simp: closed_segment_def scaleR_conv_of_real algebra_simps)
+  from u(1) show "z \<in> closed_segment a b" using assms
+    by (force simp: u closed_segment_def algebra_simps scaleR_conv_of_real complex_eq_iff)
+qed
+
 subsection\<open>Holomorphic functions\<close>
 
 definition\<^marker>\<open>tag important\<close> holomorphic_on :: "[complex \<Rightarrow> complex, complex set] \<Rightarrow> bool"
@@ -418,7 +405,7 @@
    \<Longrightarrow> deriv f z = deriv g z"
   unfolding holomorphic_on_def
   by (rule DERIV_imp_deriv)
-     (metis DERIV_deriv_iff_field_differentiable DERIV_transform_within_open at_within_open)
+     (metis DERIV_deriv_iff_field_differentiable has_field_derivative_transform_within_open at_within_open)
 
 lemma deriv_compose_linear:
   "f field_differentiable at (c * z) \<Longrightarrow> deriv (\<lambda>w. f (c * w)) z = c * deriv f (c * z)"
@@ -431,7 +418,7 @@
   assumes df: "DERIV f \<xi> :> df" and S: "open S" "\<xi> \<in> S" and "df \<noteq> 0"
     shows "\<not> f constant_on S"
 unfolding constant_on_def
-by (metis \<open>df \<noteq> 0\<close> DERIV_transform_within_open [OF df S] DERIV_const DERIV_unique)
+by (metis \<open>df \<noteq> 0\<close> has_field_derivative_transform_within_open [OF df S] DERIV_const DERIV_unique)
 
 lemma holomorphic_nonconstant:
   assumes holf: "f holomorphic_on S" and "open S" "\<xi> \<in> S" "deriv f \<xi> \<noteq> 0"
diff -r bd3d4702b4f2 -r ddd4aefc540f src/HOL/Analysis/Complex_Transcendental.thy
--- a/src/HOL/Analysis/Complex_Transcendental.thy	Mon Nov 04 21:41:55 2019 -0500
+++ b/src/HOL/Analysis/Complex_Transcendental.thy	Tue Nov 05 10:02:09 2019 -0500
@@ -2269,7 +2269,7 @@
   case False
   show ?thesis
     unfolding powr_def
-  proof (rule DERIV_transform_at)
+  proof (rule has_field_derivative_transform_within)
     show "((\<lambda>z. exp (s * Ln z)) has_field_derivative s * (if z = 0 then 0 else exp ((s - 1) * Ln z)))
            (at z)"
       apply (intro derivative_eq_intros | simp add: assms)+
@@ -2761,7 +2761,7 @@
   with z have "((\<lambda>z. exp (Ln z / 2)) has_field_derivative inverse (2 * csqrt z)) (at z)"
     by (force intro: derivative_eq_intros * simp add: assms)
   then show ?thesis
-  proof (rule DERIV_transform_at)
+  proof (rule has_field_derivative_transform_within)
     show "\<And>x. dist x z < cmod z \<Longrightarrow> exp (Ln x / 2) = csqrt x"
       by (metis csqrt_exp_Ln dist_0_norm less_irrefl)
   qed (use z in auto)
diff -r bd3d4702b4f2 -r ddd4aefc540f src/HOL/Analysis/Convex_Euclidean_Space.thy
diff -r bd3d4702b4f2 -r ddd4aefc540f src/HOL/Analysis/Great_Picard.thy
--- a/src/HOL/Analysis/Great_Picard.thy	Mon Nov 04 21:41:55 2019 -0500
+++ b/src/HOL/Analysis/Great_Picard.thy	Tue Nov 05 10:02:09 2019 -0500
@@ -1136,7 +1136,7 @@
         apply (metis Suc_pred mult.commute power_Suc)
         done
       then show ?thesis
-        apply (rule DERIV_imp_deriv [OF DERIV_transform_within_open [where S = "ball z0 r"]])
+        apply (rule DERIV_imp_deriv [OF has_field_derivative_transform_within_open [where S = "ball z0 r"]])
         using that \<open>m > 0\<close> \<open>0 < r\<close>
           apply (simp_all add: hnz geq)
         done
diff -r bd3d4702b4f2 -r ddd4aefc540f src/HOL/Analysis/Lindelof_Spaces.thy
--- a/src/HOL/Analysis/Lindelof_Spaces.thy	Mon Nov 04 21:41:55 2019 -0500
+++ b/src/HOL/Analysis/Lindelof_Spaces.thy	Tue Nov 05 10:02:09 2019 -0500
@@ -1,4 +1,4 @@
-section\<open>Lindelof spaces\<close>
+section\<open>Lindel\"of spaces\<close>
 
 theory Lindelof_Spaces
 imports T1_Spaces
diff -r bd3d4702b4f2 -r ddd4aefc540f src/HOL/Analysis/Retracts.thy
--- a/src/HOL/Analysis/Retracts.thy	Mon Nov 04 21:41:55 2019 -0500
+++ b/src/HOL/Analysis/Retracts.thy	Tue Nov 05 10:02:09 2019 -0500
@@ -1,10 +1,12 @@
 section \<open>Absolute Retracts, Absolute Neighbourhood Retracts and Euclidean Neighbourhood Retracts\<close>
 
 theory Retracts
-  imports Brouwer_Fixpoint Continuous_Extension Ordered_Euclidean_Space
+imports
+  Brouwer_Fixpoint
+  Continuous_Extension
+  Ordered_Euclidean_Space
 begin
 
-
 text \<open>Absolute retracts (AR), absolute neighbourhood retracts (ANR) and also Euclidean neighbourhood
 retracts (ENR). We define AR and ANR by specializing the standard definitions for a set to embedding
 in spaces of higher dimension.
diff -r bd3d4702b4f2 -r ddd4aefc540f src/HOL/Analysis/Riemann_Mapping.thy
--- a/src/HOL/Analysis/Riemann_Mapping.thy	Mon Nov 04 21:41:55 2019 -0500
+++ b/src/HOL/Analysis/Riemann_Mapping.thy	Tue Nov 05 10:02:09 2019 -0500
@@ -234,7 +234,7 @@
       have False if "\<And>x. x \<in> S \<Longrightarrow> f x = c" for c
       proof -
         have "deriv f 0 = 0"
-          by (metis that \<open>open S\<close> \<open>0 \<in> S\<close> DERIV_imp_deriv [OF DERIV_transform_within_open [OF DERIV_const]])
+          by (metis that \<open>open S\<close> \<open>0 \<in> S\<close> DERIV_imp_deriv [OF has_field_derivative_transform_within_open [OF DERIV_const]])
         with no_df0 have "l = 0"
           by auto
         with eql [OF _ idF] show False by auto
@@ -420,7 +420,7 @@
         have "norm (deriv (k \<circ> power2 \<circ> q) 0) < 1"
           using that by simp
         moreover have eq: "deriv f 0 = deriv (k \<circ> (\<lambda>z. z ^ 2) \<circ> q) 0 * deriv (p \<circ> \<psi> \<circ> h \<circ> f) 0"
-        proof (intro DERIV_imp_deriv DERIV_transform_within_open [OF DERIV_chain])
+        proof (intro DERIV_imp_deriv has_field_derivative_transform_within_open [OF DERIV_chain])
           show "(k \<circ> power2 \<circ> q has_field_derivative deriv (k \<circ> power2 \<circ> q) 0) (at ((p \<circ> \<psi> \<circ> h \<circ> f) 0))"
             using "1" holomorphic_derivI p0 by auto
           show "(p \<circ> \<psi> \<circ> h \<circ> f has_field_derivative deriv (p \<circ> \<psi> \<circ> h \<circ> f) 0) (at 0)"
diff -r bd3d4702b4f2 -r ddd4aefc540f src/HOL/Analysis/Topology_Euclidean_Space.thy
--- a/src/HOL/Analysis/Topology_Euclidean_Space.thy	Mon Nov 04 21:41:55 2019 -0500
+++ b/src/HOL/Analysis/Topology_Euclidean_Space.thy	Tue Nov 05 10:02:09 2019 -0500
@@ -32,7 +32,7 @@
     by (auto intro!: real_le_rsqrt)
 qed
 
-subsection \<open>Continuity of the representation WRT an orthogonal basis\<close>
+subsection\<^marker>\<open>tag unimportant\<close> \<open>Continuity of the representation WRT an orthogonal basis\<close>
 
 lemma orthogonal_Basis: "pairwise orthogonal Basis"
   by (simp add: inner_not_same_Basis orthogonal_def pairwise_def)
@@ -353,8 +353,8 @@
 
 subsection \<open>Boxes\<close>
 
-abbreviation One :: "'a::euclidean_space"
-  where "One \<equiv> \<Sum>Basis"
+abbreviation\<^marker>\<open>tag important\<close> One :: "'a::euclidean_space" where
+"One \<equiv> \<Sum>Basis"
 
 lemma One_non_0: assumes "One = (0::'a::euclidean_space)" shows False
 proof -
@@ -366,14 +366,14 @@
   with independent_Basis show False by force
 qed
 
-corollary One_neq_0[iff]: "One \<noteq> 0"
+corollary\<^marker>\<open>tag unimportant\<close> One_neq_0[iff]: "One \<noteq> 0"
   by (metis One_non_0)
 
-corollary Zero_neq_One[iff]: "0 \<noteq> One"
+corollary\<^marker>\<open>tag unimportant\<close> Zero_neq_One[iff]: "0 \<noteq> One"
   by (metis One_non_0)
 
-definition\<^marker>\<open>tag important\<close> (in euclidean_space) eucl_less (infix "<e" 50)
-  where "eucl_less a b \<longleftrightarrow> (\<forall>i\<in>Basis. a \<bullet> i < b \<bullet> i)"
+definition\<^marker>\<open>tag important\<close> (in euclidean_space) eucl_less (infix "<e" 50) where 
+"eucl_less a b \<longleftrightarrow> (\<forall>i\<in>Basis. a \<bullet> i < b \<bullet> i)"
 
 definition\<^marker>\<open>tag important\<close> box_eucl_less: "box a b = {x. a <e x \<and> x <e b}"
 definition\<^marker>\<open>tag important\<close> "cbox a b = {x. \<forall>i\<in>Basis. a \<bullet> i \<le> x \<bullet> i \<and> x \<bullet> i \<le> b \<bullet> i}"
@@ -811,6 +811,18 @@
       (Re a < Re b \<and> Im a < Im b) \<longrightarrow> Re a \<ge> Re c \<and> Im a \<ge> Im c \<and> Re b \<le> Re d \<and> Im b \<le> Im d"
   by (subst subset_box; force simp: Basis_complex_def)+
 
+lemma in_cbox_complex_iff:
+  "x \<in> cbox a b \<longleftrightarrow> Re x \<in> {Re a..Re b} \<and> Im x \<in> {Im a..Im b}"
+  by (cases x; cases a; cases b) (auto simp: cbox_Complex_eq)
+
+lemma box_Complex_eq:
+  "box (Complex a c) (Complex b d) = (\<lambda>(x,y). Complex x y) ` (box a b \<times> box c d)"
+  by (auto simp: box_def Basis_complex_def image_iff complex_eq_iff)
+
+lemma in_box_complex_iff:
+  "x \<in> box a b \<longleftrightarrow> Re x \<in> {Re a<..<Re b} \<and> Im x \<in> {Im a<..<Im b}"
+  by (cases x; cases a; cases b) (auto simp: box_Complex_eq)
+
 lemma Int_interval:
   fixes a :: "'a::euclidean_space"
   shows "cbox a b \<inter> cbox c d =
diff -r bd3d4702b4f2 -r ddd4aefc540f src/HOL/Analysis/Winding_Numbers.thy
--- a/src/HOL/Analysis/Winding_Numbers.thy	Mon Nov 04 21:41:55 2019 -0500
+++ b/src/HOL/Analysis/Winding_Numbers.thy	Tue Nov 05 10:02:09 2019 -0500
@@ -3,7 +3,10 @@
 text\<open>By John Harrison et al.  Ported from HOL Light by L C Paulson (2017)\<close>
 
 theory Winding_Numbers
-imports Polytope Jordan_Curve Riemann_Mapping
+imports
+  Polytope
+  Jordan_Curve
+  Riemann_Mapping
 begin
 
 lemma simply_connected_inside_simple_path:
@@ -785,60 +788,6 @@
 
 subsection \<open>Winding number for rectangular paths\<close>
 
-(* TODO: Move *)
-lemma closed_segmentI:
-  "u \<in> {0..1} \<Longrightarrow> z = (1 - u) *\<^sub>R a + u *\<^sub>R b \<Longrightarrow> z \<in> closed_segment a b"
-  by (auto simp: closed_segment_def)
-
-lemma in_cbox_complex_iff:
-  "x \<in> cbox a b \<longleftrightarrow> Re x \<in> {Re a..Re b} \<and> Im x \<in> {Im a..Im b}"
-  by (cases x; cases a; cases b) (auto simp: cbox_Complex_eq)
-
-lemma box_Complex_eq:
-  "box (Complex a c) (Complex b d) = (\<lambda>(x,y). Complex x y) ` (box a b \<times> box c d)"
-  by (auto simp: box_def Basis_complex_def image_iff complex_eq_iff)
-
-lemma in_box_complex_iff:
-  "x \<in> box a b \<longleftrightarrow> Re x \<in> {Re a<..<Re b} \<and> Im x \<in> {Im a<..<Im b}"
-  by (cases x; cases a; cases b) (auto simp: box_Complex_eq)
-(* END TODO *)
-
-lemma closed_segment_same_Re:
-  assumes "Re a = Re b"
-  shows   "closed_segment a b = {z. Re z = Re a \<and> Im z \<in> closed_segment (Im a) (Im b)}"
-proof safe
-  fix z assume "z \<in> closed_segment a b"
-  then obtain u where u: "u \<in> {0..1}" "z = a + of_real u * (b - a)"
-    by (auto simp: closed_segment_def scaleR_conv_of_real algebra_simps)
-  from assms show "Re z = Re a" by (auto simp: u)
-  from u(1) show "Im z \<in> closed_segment (Im a) (Im b)"
-    by (intro closed_segmentI[of u]) (auto simp: u algebra_simps)
-next
-  fix z assume [simp]: "Re z = Re a" and "Im z \<in> closed_segment (Im a) (Im b)"
-  then obtain u where u: "u \<in> {0..1}" "Im z = Im a + of_real u * (Im b - Im a)"
-    by (auto simp: closed_segment_def scaleR_conv_of_real algebra_simps)
-  from u(1) show "z \<in> closed_segment a b" using assms
-    by (intro closed_segmentI[of u]) (auto simp: u algebra_simps scaleR_conv_of_real complex_eq_iff)
-qed
-
-lemma closed_segment_same_Im:
-  assumes "Im a = Im b"
-  shows   "closed_segment a b = {z. Im z = Im a \<and> Re z \<in> closed_segment (Re a) (Re b)}"
-proof safe
-  fix z assume "z \<in> closed_segment a b"
-  then obtain u where u: "u \<in> {0..1}" "z = a + of_real u * (b - a)"
-    by (auto simp: closed_segment_def scaleR_conv_of_real algebra_simps)
-  from assms show "Im z = Im a" by (auto simp: u)
-  from u(1) show "Re z \<in> closed_segment (Re a) (Re b)"
-    by (intro closed_segmentI[of u]) (auto simp: u algebra_simps)
-next
-  fix z assume [simp]: "Im z = Im a" and "Re z \<in> closed_segment (Re a) (Re b)"
-  then obtain u where u: "u \<in> {0..1}" "Re z = Re a + of_real u * (Re b - Re a)"
-    by (auto simp: closed_segment_def scaleR_conv_of_real algebra_simps)
-  from u(1) show "z \<in> closed_segment a b" using assms
-    by (intro closed_segmentI[of u]) (auto simp: u algebra_simps scaleR_conv_of_real complex_eq_iff)
-qed
-
 definition\<^marker>\<open>tag important\<close> rectpath where
   "rectpath a1 a3 = (let a2 = Complex (Re a3) (Im a1); a4 = Complex (Re a1) (Im a3)
                       in linepath a1 a2 +++ linepath a2 a3 +++ linepath a3 a4 +++ linepath a4 a1)"
diff -r bd3d4702b4f2 -r ddd4aefc540f src/HOL/Deriv.thy
--- a/src/HOL/Deriv.thy	Mon Nov 04 21:41:55 2019 -0500
+++ b/src/HOL/Deriv.thy	Tue Nov 05 10:02:09 2019 -0500
@@ -278,6 +278,23 @@
   show ?thesis .
 qed
 
+lemma has_field_derivative_transform_within:
+  assumes "(f has_field_derivative f') (at a within S)"
+    and "0 < d"
+    and "a \<in> S"
+    and "\<And>x. \<lbrakk>x \<in> S; dist x a < d\<rbrakk> \<Longrightarrow> f x = g x"
+  shows "(g has_field_derivative f') (at a within S)"
+  using assms unfolding has_field_derivative_def
+  by (metis has_derivative_transform_within)
+
+lemma has_field_derivative_transform_within_open:
+  assumes "(f has_field_derivative f') (at a)"
+    and "open S" "a \<in> S"
+    and "\<And>x. x \<in> S \<Longrightarrow> f x = g x"
+  shows "(g has_field_derivative f') (at a)"
+  using assms unfolding has_field_derivative_def
+  by (metis has_derivative_transform_within_open)
+
 
 subsection \<open>Continuity\<close>