author paulson Mon, 04 Nov 2019 17:06:18 +0000 changeset 71029 934e0044e94b parent 71017 c85efa2be619 child 71030 b6e69c71a9f6
Moved or deleted some out of place material, also eliminating obsolete naming conventions
 src/HOL/Analysis/Cauchy_Integral_Theorem.thy file | annotate | diff | comparison | revisions src/HOL/Analysis/Complex_Analysis_Basics.thy file | annotate | diff | comparison | revisions src/HOL/Analysis/Complex_Transcendental.thy file | annotate | diff | comparison | revisions src/HOL/Analysis/Convex_Euclidean_Space.thy file | annotate | diff | comparison | revisions src/HOL/Analysis/Great_Picard.thy file | annotate | diff | comparison | revisions src/HOL/Analysis/Riemann_Mapping.thy file | annotate | diff | comparison | revisions src/HOL/Analysis/Topology_Euclidean_Space.thy file | annotate | diff | comparison | revisions src/HOL/Analysis/Winding_Numbers.thy file | annotate | diff | comparison | revisions src/HOL/Deriv.thy file | annotate | diff | comparison | revisions
```--- 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>
```