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