Moved or deleted some out of place material, also eliminating obsolete naming conventions
--- a/src/HOL/Analysis/Cauchy_Integral_Theorem.thy Sun Nov 03 20:38:08 2019 +0100
+++ b/src/HOL/Analysis/Cauchy_Integral_Theorem.thy Mon Nov 04 17:06:18 2019 +0000
@@ -6054,7 +6054,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 +6068,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 +6090,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 +6133,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 +6847,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 +6975,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 Sun Nov 03 20:38:08 2019 +0100
+++ b/src/HOL/Analysis/Complex_Analysis_Basics.thy Mon Nov 04 17:06:18 2019 +0000
@@ -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 (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
+
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 Sun Nov 03 20:38:08 2019 +0100
+++ b/src/HOL/Analysis/Complex_Transcendental.thy Mon Nov 04 17:06:18 2019 +0000
@@ -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/Convex_Euclidean_Space.thy Sun Nov 03 20:38:08 2019 +0100
+++ b/src/HOL/Analysis/Convex_Euclidean_Space.thy Mon Nov 04 17:06:18 2019 +0000
@@ -2615,6 +2615,10 @@
"x \<in> open_segment a b \<longleftrightarrow> a \<noteq> b \<and> (\<exists>u. 0 < u \<and> u < 1 \<and> x = (1 - u) *\<^sub>R a + u *\<^sub>R b)"
using less_eq_real_def by (auto simp: segment algebra_simps)
+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 closed_segment_linear_image:
"closed_segment (f a) (f b) = f ` (closed_segment a b)" if "linear f"
proof -
--- a/src/HOL/Analysis/Great_Picard.thy Sun Nov 03 20:38:08 2019 +0100
+++ b/src/HOL/Analysis/Great_Picard.thy Mon Nov 04 17:06:18 2019 +0000
@@ -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/Riemann_Mapping.thy Sun Nov 03 20:38:08 2019 +0100
+++ b/src/HOL/Analysis/Riemann_Mapping.thy Mon Nov 04 17:06:18 2019 +0000
@@ -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 Sun Nov 03 20:38:08 2019 +0100
+++ b/src/HOL/Analysis/Topology_Euclidean_Space.thy Mon Nov 04 17:06:18 2019 +0000
@@ -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 Sun Nov 03 20:38:08 2019 +0100
+++ b/src/HOL/Analysis/Winding_Numbers.thy Mon Nov 04 17:06:18 2019 +0000
@@ -785,60 +785,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 Sun Nov 03 20:38:08 2019 +0100
+++ b/src/HOL/Deriv.thy Mon Nov 04 17:06:18 2019 +0000
@@ -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>