author paulson Sat, 26 May 2018 08:36:19 +0100 changeset 68285 9d93b13f07ce parent 68278 23e12da0866c (current diff) parent 68284 5e4e006f9552 (diff) child 68286 b9160ca067ae
merged
```--- a/src/HOL/Analysis/Cauchy_Integral_Theorem.thy	Fri May 25 23:11:06 2018 +0200
+++ b/src/HOL/Analysis/Cauchy_Integral_Theorem.thy	Sat May 26 08:36:19 2018 +0100
@@ -91,14 +91,14 @@
(infixr "piecewise'_differentiable'_on" 50)
where "f piecewise_differentiable_on i  \<equiv>
continuous_on i f \<and>
-           (\<exists>s. finite s \<and> (\<forall>x \<in> i - s. f differentiable (at x within i)))"
+           (\<exists>S. finite S \<and> (\<forall>x \<in> i - S. f differentiable (at x within i)))"

lemma piecewise_differentiable_on_imp_continuous_on:
-    "f piecewise_differentiable_on s \<Longrightarrow> continuous_on s f"
+    "f piecewise_differentiable_on S \<Longrightarrow> continuous_on S f"

lemma piecewise_differentiable_on_subset:
-    "f piecewise_differentiable_on s \<Longrightarrow> t \<le> s \<Longrightarrow> f piecewise_differentiable_on t"
+    "f piecewise_differentiable_on S \<Longrightarrow> T \<le> S \<Longrightarrow> f piecewise_differentiable_on T"
using continuous_on_subset
unfolding piecewise_differentiable_on_def
apply safe
@@ -113,29 +113,29 @@
done

lemma differentiable_imp_piecewise_differentiable:
-    "(\<And>x. x \<in> s \<Longrightarrow> f differentiable (at x within s))
-         \<Longrightarrow> f piecewise_differentiable_on s"
+    "(\<And>x. x \<in> S \<Longrightarrow> f differentiable (at x within S))
+         \<Longrightarrow> f piecewise_differentiable_on S"
by (auto simp: piecewise_differentiable_on_def differentiable_imp_continuous_on differentiable_on_def
intro: differentiable_within_subset)

-lemma piecewise_differentiable_const [iff]: "(\<lambda>x. z) piecewise_differentiable_on s"
+lemma piecewise_differentiable_const [iff]: "(\<lambda>x. z) piecewise_differentiable_on S"

lemma piecewise_differentiable_compose:
-    "\<lbrakk>f piecewise_differentiable_on s; g piecewise_differentiable_on (f ` s);
-      \<And>x. finite (s \<inter> f-`{x})\<rbrakk>
-      \<Longrightarrow> (g o f) piecewise_differentiable_on s"
+    "\<lbrakk>f piecewise_differentiable_on S; g piecewise_differentiable_on (f ` S);
+      \<And>x. finite (S \<inter> f-`{x})\<rbrakk>
+      \<Longrightarrow> (g o f) piecewise_differentiable_on S"
apply (blast intro: continuous_on_compose2)
apply (rename_tac A B)
-  apply (rule_tac x="A \<union> (\<Union>x\<in>B. s \<inter> f-`{x})" in exI)
+  apply (rule_tac x="A \<union> (\<Union>x\<in>B. S \<inter> f-`{x})" in exI)
apply (blast intro!: differentiable_chain_within)
done

lemma piecewise_differentiable_affine:
fixes m::real
-  assumes "f piecewise_differentiable_on ((\<lambda>x. m *\<^sub>R x + c) ` s)"
-  shows "(f o (\<lambda>x. m *\<^sub>R x + c)) piecewise_differentiable_on s"
+  assumes "f piecewise_differentiable_on ((\<lambda>x. m *\<^sub>R x + c) ` S)"
+  shows "(f o (\<lambda>x. m *\<^sub>R x + c)) piecewise_differentiable_on S"
proof (cases "m = 0")
case True
then show ?thesis
@@ -156,13 +156,13 @@
"a \<le> c" "c \<le> b" "f c = g c"
shows "(\<lambda>x. if x \<le> c then f x else g x) piecewise_differentiable_on {a..b}"
proof -
-  obtain s t where st: "finite s" "finite t"
-                       "\<forall>x\<in>{a..c} - s. f differentiable at x within {a..c}"
-                       "\<forall>x\<in>{c..b} - t. g differentiable at x within {c..b}"
+  obtain S T where st: "finite S" "finite T"
+               and fd: "\<And>x. x \<in> {a..c} - S \<Longrightarrow> f differentiable at x within {a..c}"
+               and gd: "\<And>x. x \<in> {c..b} - T \<Longrightarrow> g differentiable at x within {c..b}"
using assms
by (auto simp: piecewise_differentiable_on_def)
-  have finabc: "finite ({a,b,c} \<union> (s \<union> t))"
-    by (metis \<open>finite s\<close> \<open>finite t\<close> finite_Un finite_insert finite.emptyI)
+  have finabc: "finite ({a,b,c} \<union> (S \<union> T))"
+    by (metis \<open>finite S\<close> \<open>finite T\<close> finite_Un finite_insert finite.emptyI)
have "continuous_on {a..c} f" "continuous_on {c..b} g"
using assms piecewise_differentiable_on_def by auto
then have "continuous_on {a..b} (\<lambda>x. if x \<le> c then f x else g x)"
@@ -172,43 +172,35 @@
by (force simp: ivl_disj_un_two_touch)
moreover
{ fix x
-    assume x: "x \<in> {a..b} - ({a,b,c} \<union> (s \<union> t))"
+    assume x: "x \<in> {a..b} - ({a,b,c} \<union> (S \<union> T))"
have "(\<lambda>x. if x \<le> c then f x else g x) differentiable at x within {a..b}" (is "?diff_fg")
proof (cases x c rule: le_cases)
case le show ?diff_fg
-      proof (rule differentiable_transform_within [where d = "dist x c" and f = f])
-        have "f differentiable at x within ({a<..<c} - s)"
-          apply (rule differentiable_at_withinI)
-          using x le st
-          by (metis (no_types, lifting) DiffD1 DiffD2 DiffI UnCI atLeastAtMost_diff_ends atLeastAtMost_iff at_within_interior insert_iff interior_atLeastAtMost_real le st(3) x)
-        moreover have "open ({a<..<c} - s)"
-          by (blast intro: open_greaterThanLessThan \<open>finite s\<close> finite_imp_closed)
-        ultimately show "f differentiable at x within {a..b}"
-          using x le by (auto simp add: at_within_open_NO_MATCH differentiable_at_withinI)
+      proof (rule differentiable_transform_within [where d = "dist x c"])
+        have "f differentiable at x"
+          using x le fd [of x] at_within_interior [of x "{a..c}"] by simp
+        then show "f differentiable at x within {a..b}"
qed (use x le st dist_real_def in auto)
next
case ge show ?diff_fg
-      proof (rule differentiable_transform_within [where d = "dist x c" and f = g])
-        have "g differentiable at x within ({c<..<b} - t)"
-          apply (rule differentiable_at_withinI)
-          using x ge st
-          by (metis DiffD1 DiffD2 DiffI UnCI atLeastAtMost_diff_ends atLeastAtMost_iff at_within_interior insert_iff interior_atLeastAtMost_real)
-        moreover have "open ({c<..<b} - t)"
-          by (blast intro: open_greaterThanLessThan \<open>finite t\<close> finite_imp_closed)
-        ultimately show "g differentiable at x within {a..b}"
-          using x ge by (auto simp add: at_within_open_NO_MATCH differentiable_at_withinI)
+      proof (rule differentiable_transform_within [where d = "dist x c"])
+        have "g differentiable at x"
+          using x ge gd [of x] at_within_interior [of x "{c..b}"] by simp
+        then show "g differentiable at x within {a..b}"
qed (use x ge st dist_real_def in auto)
qed
}
-  then have "\<exists>s. finite s \<and>
-                 (\<forall>x\<in>{a..b} - s. (\<lambda>x. if x \<le> c then f x else g x) differentiable at x within {a..b})"
+  then have "\<exists>S. finite S \<and>
+                 (\<forall>x\<in>{a..b} - S. (\<lambda>x. if x \<le> c then f x else g x) differentiable at x within {a..b})"
by (meson finabc)
ultimately show ?thesis
qed

lemma piecewise_differentiable_neg:
-    "f piecewise_differentiable_on s \<Longrightarrow> (\<lambda>x. -(f x)) piecewise_differentiable_on s"
+    "f piecewise_differentiable_on S \<Longrightarrow> (\<lambda>x. -(f x)) piecewise_differentiable_on S"
by (auto simp: piecewise_differentiable_on_def continuous_on_minus)

@@ -216,11 +208,11 @@
"g piecewise_differentiable_on i"
shows "(\<lambda>x. f x + g x) piecewise_differentiable_on i"
proof -
-  obtain s t where st: "finite s" "finite t"
-                       "\<forall>x\<in>i - s. f differentiable at x within i"
-                       "\<forall>x\<in>i - t. g differentiable at x within i"
+  obtain S T where st: "finite S" "finite T"
+                       "\<forall>x\<in>i - S. f differentiable at x within i"
+                       "\<forall>x\<in>i - T. g differentiable at x within i"
using assms by (auto simp: piecewise_differentiable_on_def)
-  then have "finite (s \<union> t) \<and> (\<forall>x\<in>i - (s \<union> t). (\<lambda>x. f x + g x) differentiable at x within i)"
+  then have "finite (S \<union> T) \<and> (\<forall>x\<in>i - (S \<union> T). (\<lambda>x. f x + g x) differentiable at x within i)"
by auto
moreover have "continuous_on i f" "continuous_on i g"
using assms piecewise_differentiable_on_def by auto
@@ -229,8 +221,8 @@
qed

lemma piecewise_differentiable_diff:
-    "\<lbrakk>f piecewise_differentiable_on s;  g piecewise_differentiable_on s\<rbrakk>
-     \<Longrightarrow> (\<lambda>x. f x - g x) piecewise_differentiable_on s"
+    "\<lbrakk>f piecewise_differentiable_on S;  g piecewise_differentiable_on S\<rbrakk>
+     \<Longrightarrow> (\<lambda>x. f x - g x) piecewise_differentiable_on S"

@@ -249,33 +241,63 @@
done

lemma piecewise_differentiable_D1:
-    "(g1 +++ g2) piecewise_differentiable_on {0..1} \<Longrightarrow> g1 piecewise_differentiable_on {0..1}"
-  apply (clarsimp simp add: piecewise_differentiable_on_def dest!: continuous_on_joinpaths_D1)
-  apply (rule_tac x="insert 1 ((( * )2)`s)" in exI)
-  apply simp
-  apply (intro ballI)
-  apply (rule_tac d="dist (x/2) (1/2)" and f = "(g1 +++ g2) o (( * )(inverse 2))"
-       in differentiable_transform_within)
-  apply (auto simp: dist_real_def joinpaths_def)
-  apply (rule differentiable_chain_within derivative_intros | simp)+
-  apply (rule differentiable_subset)
-  apply (force simp:)+
-  done
+  assumes "(g1 +++ g2) piecewise_differentiable_on {0..1}"
+  shows "g1 piecewise_differentiable_on {0..1}"
+proof -
+  obtain S where cont: "continuous_on {0..1} g1" and "finite S"
+    and S: "\<And>x. x \<in> {0..1} - S \<Longrightarrow> g1 +++ g2 differentiable at x within {0..1}"
+    using assms unfolding piecewise_differentiable_on_def
+    by (blast dest!: continuous_on_joinpaths_D1)
+  show ?thesis
+    unfolding piecewise_differentiable_on_def
+  proof (intro exI conjI ballI cont)
+    show "finite (insert 1 ((( * )2) ` S))"
+      by (simp add: \<open>finite S\<close>)
+    show "g1 differentiable at x within {0..1}" if "x \<in> {0..1} - insert 1 (( * ) 2 ` S)" for x
+    proof (rule_tac d="dist (x/2) (1/2)" in differentiable_transform_within)
+      have "g1 +++ g2 differentiable at (x / 2) within {0..1 / 2}"
+        by (rule differentiable_subset [OF S [of "x/2"]] | use that in force)+
+      then show "g1 +++ g2 \<circ> ( * ) (inverse 2) differentiable at x within {0..1}"
+        by (auto intro: differentiable_chain_within)
+    qed (use that in \<open>auto simp: joinpaths_def\<close>)
+  qed
+qed

lemma piecewise_differentiable_D2:
-    "\<lbrakk>(g1 +++ g2) piecewise_differentiable_on {0..1}; pathfinish g1 = pathstart g2\<rbrakk>
-    \<Longrightarrow> g2 piecewise_differentiable_on {0..1}"
-  apply (clarsimp simp add: piecewise_differentiable_on_def dest!: continuous_on_joinpaths_D2)
-  apply (rule_tac x="insert 0 ((\<lambda>x. 2*x-1)`s)" in exI)
-  apply simp
-  apply (intro ballI)
-  apply (rule_tac d="dist ((x+1)/2) (1/2)" and f = "(g1 +++ g2) o (\<lambda>x. (x+1)/2)"
-          in differentiable_transform_within)
-  apply (auto simp: dist_real_def joinpaths_def abs_if field_simps split: if_split_asm)
-  apply (rule differentiable_chain_within derivative_intros | simp)+
-  apply (rule differentiable_subset)
-  apply (force simp: divide_simps)+
-  done
+  assumes "(g1 +++ g2) piecewise_differentiable_on {0..1}" and eq: "pathfinish g1 = pathstart g2"
+  shows "g2 piecewise_differentiable_on {0..1}"
+proof -
+  have [simp]: "g1 1 = g2 0"
+    using eq by (simp add: pathfinish_def pathstart_def)
+  obtain S where cont: "continuous_on {0..1} g2" and "finite S"
+    and S: "\<And>x. x \<in> {0..1} - S \<Longrightarrow> g1 +++ g2 differentiable at x within {0..1}"
+    using assms unfolding piecewise_differentiable_on_def
+    by (blast dest!: continuous_on_joinpaths_D2)
+  show ?thesis
+    unfolding piecewise_differentiable_on_def
+  proof (intro exI conjI ballI cont)
+    show "finite (insert 0 ((\<lambda>x. 2*x-1)`S))"
+      by (simp add: \<open>finite S\<close>)
+    show "g2 differentiable at x within {0..1}" if "x \<in> {0..1} - insert 0 ((\<lambda>x. 2*x-1)`S)" for x
+    proof (rule_tac d="dist ((x+1)/2) (1/2)" in differentiable_transform_within)
+      have x2: "(x + 1) / 2 \<notin> S"
+        using that
+        apply (clarsimp simp: image_iff)
+      have "g1 +++ g2 \<circ> (\<lambda>x. (x+1) / 2) differentiable at x within {0..1}"
+        by (rule differentiable_chain_within differentiable_subset [OF S [of "(x+1)/2"]] | use x2 that in force)+
+      then show "g1 +++ g2 \<circ> (\<lambda>x. (x+1) / 2) differentiable at x within {0..1}"
+        by (auto intro: differentiable_chain_within)
+      show "(g1 +++ g2 \<circ> (\<lambda>x. (x + 1) / 2)) x' = g2 x'" if "x' \<in> {0..1}" "dist x' x < dist ((x + 1) / 2) (1 / 2)" for x'
+      proof -
+        have [simp]: "(2*x'+2)/2 = x'+1"
+        show ?thesis
+          using that by (auto simp: joinpaths_def)
+      qed
+    qed (use that in \<open>auto simp: joinpaths_def\<close>)
+  qed
+qed

subsubsection\<open>The concept of continuously differentiable\<close>
@@ -590,7 +612,7 @@
apply (auto simp: dist_real_def joinpaths_def field_simps)
apply (rule differentiable_chain_at derivative_intros | force)+
-    apply (drule_tac x= "(x + 1) / 2" in bspec, force simp: divide_simps)
+    apply (drule_tac x= "(x+1) / 2" in bspec, force simp: divide_simps)
apply assumption
done
have [simp]: "vector_derivative (g2 \<circ> (\<lambda>x. 2*x-1)) (at ((x+1)/2)) = 2 *\<^sub>R vector_derivative g2 (at x)"
@@ -604,7 +626,7 @@
apply (auto simp: dist_real_def field_simps joinpaths_def vector_derivative_works [symmetric]
intro!: g2D differentiable_chain_at)
done
-  have [simp]: "((\<lambda>x. (x + 1) / 2) ` ({0..1} - insert 0 ((\<lambda>x. 2 * x - 1) ` s))) = ({1/2..1} - insert (1/2) s)"
+  have [simp]: "((\<lambda>x. (x+1) / 2) ` ({0..1} - insert 0 ((\<lambda>x. 2 * x - 1) ` s))) = ({1/2..1} - insert (1/2) s)"
apply (simp add: image_set_diff inj_on_def image_image)
done```
```--- a/src/HOL/Analysis/Complex_Transcendental.thy	Fri May 25 23:11:06 2018 +0200
+++ b/src/HOL/Analysis/Complex_Transcendental.thy	Sat May 26 08:36:19 2018 +0100
@@ -1796,8 +1796,7 @@

lemma norm_powr_real: "w \<in> \<real> \<Longrightarrow> 0 < Re w \<Longrightarrow> norm(w powr z) = exp(Re z * ln(Re w))"
-  using Im_Ln_eq_0 complex_is_Real_iff norm_complex_def
-  by auto
+  using Im_Ln_eq_0 complex_is_Real_iff norm_complex_def  by auto

lemma powr_complexpow [simp]:
fixes x::complex shows "x \<noteq> 0 \<Longrightarrow> x powr (of_nat n) = x^n"
@@ -1817,10 +1816,14 @@
qed simp

lemma powr_real_real:
-    "\<lbrakk>w \<in> \<real>; z \<in> \<real>; 0 < Re w\<rbrakk> \<Longrightarrow> w powr z = exp(Re z * ln(Re w))"
-  by (metis complex_eq complex_is_Real_iff diff_0 diff_0_right diff_minus_eq_add exp_ln exp_not_eq_zero
-       exp_of_real Ln_of_real mult_zero_right of_real_0 of_real_mult)
+  assumes "w \<in> \<real>" "z \<in> \<real>" "0 < Re w"
+  shows "w powr z = exp(Re z * ln(Re w))"
+proof -
+  have "w \<noteq> 0"
+    using assms by auto
+  with assms show ?thesis
+    by (simp add: powr_def Ln_Reals_eq of_real_exp)
+qed

lemma powr_of_real:
fixes x::real and y::real
@@ -1874,13 +1877,14 @@
shows "((\<lambda>z. z powr s) has_field_derivative (s * z powr (s - 1))) (at z)"
proof (cases "z=0")
case False
-  with assms show ?thesis
-  apply (rule DERIV_transform_at [where d = "norm z" and f = "\<lambda>z. exp (s * Ln z)"])
-  apply (auto simp: dist_complex_def)
-    apply (intro derivative_eq_intros | simp)+
-  apply (simp add: field_simps exp_diff)
-  done
+  show ?thesis
+    unfolding powr_def
+  proof (rule DERIV_transform_at)
+    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)+
+      by (simp add: False divide_complex_def exp_diff left_diff_distrib')
+  qed (use False in auto)
qed (use assms in auto)

declare has_field_derivative_powr[THEN DERIV_chain2, derivative_intros]
@@ -1908,12 +1912,12 @@
\<longleftrightarrow> ((\<lambda>z. g z powr of_int n) has_field_derivative dd') (at z within s)"
by simp
also have "... \<longleftrightarrow> ((\<lambda>z. g z ^ nat n) has_field_derivative dd') (at z within s)"
-      apply (rule has_field_derivative_cong_eventually)
-      subgoal unfolding eventually_at
+    proof (rule has_field_derivative_cong_eventually)
+      show "\<forall>\<^sub>F x in at z within s. g x powr of_int n = g x ^ nat n"
+        unfolding eventually_at
apply (rule exI[where x=e])
using powr_of_int that \<open>e>0\<close> e_dist by (simp add: dist_commute)
-      subgoal using powr_of_int \<open>g z\<noteq>0\<close> that by simp
-      done
+    qed (use powr_of_int \<open>g z\<noteq>0\<close> that in simp)
also have "..." unfolding dd'_def using gderiv that
by (auto intro!: derivative_eq_intros)
finally have "((\<lambda>z. g z powr of_int n) has_field_derivative dd) (at z within s)" .
@@ -1933,17 +1937,20 @@
\<longleftrightarrow> ((\<lambda>z. g z powr of_int n) has_field_derivative dd') (at z within s)"
by simp
also have "... \<longleftrightarrow> ((\<lambda>z. inverse (g z ^ nat (-n))) has_field_derivative dd') (at z within s)"
-      apply (rule has_field_derivative_cong_eventually)
-      subgoal unfolding eventually_at
+    proof (rule has_field_derivative_cong_eventually)
+      show "\<forall>\<^sub>F x in at z within s. g x powr of_int n = inverse (g x ^ nat (- n))"
+         unfolding eventually_at
apply (rule exI[where x=e])
using powr_of_int that \<open>e>0\<close> e_dist by (simp add: dist_commute)
-      subgoal using powr_of_int \<open>g z\<noteq>0\<close> that by simp
-      done
-    also have "..." unfolding dd'_def using gderiv that \<open>g z\<noteq>0\<close>
-      apply (auto intro!: derivative_eq_intros)
-      apply (subgoal_tac "nat (- n) + nat (1 - n) - Suc 0 = nat (- n) + nat (- n)")
-      by auto
+    qed (use powr_of_int \<open>g z\<noteq>0\<close> that in simp)
+    also have "..."
+    proof -
+      have "nat (- n) + nat (1 - n) - Suc 0 = nat (- n) + nat (- n)"
+        by auto
+      then show ?thesis
+        unfolding dd'_def using gderiv that \<open>g z\<noteq>0\<close>
+    qed
finally have "((\<lambda>z. g z powr of_int n) has_field_derivative dd) (at z within s)" .
then show ?thesis unfolding dd_def by simp
qed
@@ -1990,15 +1997,11 @@
assumes "f holomorphic_on s"
shows "(\<lambda>z. w powr (f z)) holomorphic_on s"
proof (cases "w = 0")
-  case True
-  then show ?thesis
-    by simp
-next
case False
with assms show ?thesis
unfolding holomorphic_on_def field_differentiable_def
by (metis (full_types) DERIV_chain' has_field_derivative_powr_right)
-qed
+qed simp

lemma holomorphic_on_divide_gen [holomorphic_intros]:
assumes f: "f holomorphic_on s" and g: "g holomorphic_on s" and 0: "\<And>z z'. \<lbrakk>z \<in> s; z' \<in> s\<rbrakk> \<Longrightarrow> g z = 0 \<longleftrightarrow> g z' = 0"
@@ -2019,14 +2022,7 @@

lemma norm_powr_real_powr:
"w \<in> \<real> \<Longrightarrow> 0 \<le> Re w \<Longrightarrow> cmod (w powr z) = Re w powr Re z"
-  by (cases "w = 0")
-     (auto simp add: norm_powr_real powr_def Im_Ln_eq_0
-                     complex_is_Real_iff in_Reals_norm complex_eq_iff)
-
-lemma tendsto_ln_complex [tendsto_intros]:
-  assumes "(f \<longlongrightarrow> a) F" "a \<notin> \<real>\<^sub>\<le>\<^sub>0"
-  shows   "((\<lambda>z. ln (f z :: complex)) \<longlongrightarrow> ln a) F"
-  using tendsto_compose[OF continuous_at_Ln[of a, unfolded isCont_def] assms(1)] assms(2) by simp
+  by (metis dual_order.order_iff_strict norm_powr_real norm_zero of_real_0 of_real_Re powr_def)

lemma tendsto_powr_complex:
fixes f g :: "_ \<Rightarrow> complex"
@@ -2095,16 +2091,9 @@

lemma tendsto_powr_complex' [tendsto_intros]:
fixes f g :: "_ \<Rightarrow> complex"
-  assumes fz: "a \<notin> \<real>\<^sub>\<le>\<^sub>0 \<or> (a = 0 \<and> Re b > 0)"
-  assumes fg: "(f \<longlongrightarrow> a) F" "(g \<longlongrightarrow> b) F"
+  assumes "a \<notin> \<real>\<^sub>\<le>\<^sub>0 \<or> (a = 0 \<and> Re b > 0)" and "(f \<longlongrightarrow> a) F" "(g \<longlongrightarrow> b) F"
shows   "((\<lambda>z. f z powr g z) \<longlongrightarrow> a powr b) F"
-proof (cases "a = 0")
-  case True
-  with assms show ?thesis by (auto intro!: tendsto_powr_complex_0)
-next
-  case False
-  with assms show ?thesis by (auto intro!: tendsto_powr_complex elim!: nonpos_Reals_cases)
-qed
+  using assms tendsto_powr_complex tendsto_powr_complex_0 by fastforce

lemma tendsto_neg_powr_complex_of_real:
assumes "filterlim f at_top F" and "Re s < 0"
@@ -2185,12 +2174,13 @@
using e assms by simp
with x have "x > 0"
by linarith
-    then show "0 < e * 2 + (e * Re s * 2 - 2) * x + e * (Re s)\<^sup>2 * x\<^sup>2"
-      using e assms x
-      apply (auto simp: field_simps)
-      apply (rule_tac y = "e * (x\<^sup>2 * (Re s)\<^sup>2)" in le_less_trans)
-      apply (auto simp: power2_eq_square field_simps add_pos_pos)
-      done
+    then have "x * 2 \<le> e * (x\<^sup>2 * (Re s)\<^sup>2)"
+      using e assms x by (auto simp: power2_eq_square field_simps)
+    also have "... < e * (2 + (x * (Re s * 2) + x\<^sup>2 * (Re s)\<^sup>2))"
+      using e assms \<open>x > 0\<close>
+      by (auto simp: power2_eq_square field_simps add_pos_pos)
+    finally show "0 < e * 2 + (e * Re s * 2 - 2) * x + e * (Re s)\<^sup>2 * x\<^sup>2"
+      by (auto simp: algebra_simps)
qed
then have "\<exists>xo>0. \<forall>x\<ge>xo. x / e < 1 + (Re s * x) + (1/2) * (Re s * x)^2"
using e  by (simp add: field_simps)
@@ -2217,8 +2207,7 @@
shows "((\<lambda>n. ln n / (n powr s)) \<longlongrightarrow> 0) sequentially"
using lim_Ln_over_power [of "of_real s", THEN filterlim_sequentially_Suc [THEN iffD2]] assms
apply (subst filterlim_sequentially_Suc [symmetric])
-  apply (simp add: lim_sequentially dist_norm
-          Ln_Reals_eq norm_powr_real_powr norm_divide)
+  apply (simp add: lim_sequentially dist_norm Ln_Reals_eq norm_powr_real_powr norm_divide)
done

lemma lim_ln_over_n: "((\<lambda>n. ln(real_of_nat n) / of_nat n) \<longlongrightarrow> 0) sequentially"
@@ -2414,14 +2403,15 @@
"continuous (at z within (\<real> \<inter> {w. 0 \<le> Re(w)})) csqrt"
proof (cases "z \<in> \<real>\<^sub>\<le>\<^sub>0")
case True
-  then have "Im z = 0" "Re z < 0 \<or> z = 0"
-    using cnj.code complex_cnj_zero_iff  by (auto simp: Complex_eq complex_nonpos_Reals_iff) fastforce
-  then show ?thesis
+  have *: "\<And>e. \<lbrakk>0 < e\<rbrakk>
+         \<Longrightarrow> \<forall>x'\<in>\<real> \<inter> {w. 0 \<le> Re w}. cmod x' < e^2 \<longrightarrow> cmod (csqrt x') < e"
+    by (auto simp: Reals_def real_less_lsqrt)
+  have "Im z = 0" "Re z < 0 \<or> z = 0"
+    using True cnj.code complex_cnj_zero_iff  by (auto simp: Complex_eq complex_nonpos_Reals_iff) fastforce
+  with * show ?thesis
apply (auto simp: continuous_within_closed_nontrivial [OF closed_Real_halfspace_Re_ge])
-    apply (auto simp: continuous_within_eps_delta norm_conv_dist [symmetric])
-    apply (rule_tac x="e^2" in exI)
-    apply (auto simp: Reals_def)
-    by (metis linear not_less real_sqrt_less_iff real_sqrt_pow2_iff real_sqrt_power)
+    apply (auto simp: continuous_within_eps_delta)
+    using zero_less_power by blast
next
case False
then show ?thesis   by (blast intro: continuous_within_csqrt)
@@ -2514,8 +2504,8 @@
proof -
have nz0: "1 + \<i>*z \<noteq> 0"
using assms
-    by (metis abs_one complex_i_mult_minus diff_0_right diff_minus_eq_add imaginary_unit.simps
-              less_irrefl minus_diff_eq mult.right_neutral right_minus_eq)
+    by (metis abs_one add_diff_cancel_left' complex_i_mult_minus diff_0 i_squared imaginary_unit.simps
+                less_asym neg_equal_iff_equal)
have "z \<noteq> -\<i>" using assms
by auto
then have zz: "1 + z * z \<noteq> 0"
@@ -2543,11 +2533,10 @@
done
show "(Arctan has_field_derivative inverse(1 + z\<^sup>2)) (at z)"
unfolding Arctan_def scaleR_conv_of_real
-    apply (rule DERIV_cong)
apply (intro derivative_eq_intros | simp add: nz0 *)+
using nz0 nz1 zz
-    apply (simp add: divide_simps power2_eq_square)
-    apply (auto simp: algebra_simps)
+    apply (simp add: algebra_simps divide_simps power2_eq_square)
+    apply algebra
done
qed

@@ -2594,8 +2583,8 @@
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)) /
-                 (of_nat (2*Suc n-1) / of_nat (Suc n)))"
+             ereal (inverse (norm u)^2) * ereal (((2*Suc n+1) / (Suc n)) /
+                 ((2*Suc n-1) / (Suc n)))"
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))"
@@ -2641,10 +2630,10 @@
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
show "((\<lambda>u. Arctan u - G u) has_field_derivative 0) (at u within ball 0 1)"
-      by (simp_all add: dist_0_norm at_within_open[OF _ open_ball])
+      by (simp_all add: at_within_open[OF _ open_ball])
qed simp_all
-  then obtain c where c: "\<And>u. norm u < 1 \<Longrightarrow> Arctan u - G u = c" by (auto simp: dist_0_norm)
-  from this[of 0] have "c = 0" by (simp add: G_def g_def powser_zero)
+  then obtain c where c: "\<And>u. norm u < 1 \<Longrightarrow> Arctan u - G u = c" by auto
+  from this[of 0] have "c = 0" by (simp add: G_def g_def)
with c z have "Arctan z = G z" by simp
with summable[OF z] show "(\<lambda>n. g n * z^n) sums Arctan z" unfolding G_def by (simp add: sums_iff)
thus "h z sums Arctan z" by (subst (asm) sums_mono_reindex[of "\<lambda>n. 2*n+1", symmetric])
@@ -2690,14 +2679,19 @@
by simp

lemma Im_Arctan_of_real [simp]: "Im (Arctan (of_real x)) = 0"
-  unfolding Arctan_def divide_complex_def
-  apply (rule norm_exp_imaginary)
-  apply (subst exp_Ln, auto)
-  apply (simp_all add: cmod_def complex_eq_iff)
-  apply (auto simp: divide_simps)
-  apply (metis power_one sum_power2_eq_zero_iff zero_neq_one, algebra)
-  done
+proof -
+  have ne: "1 + x\<^sup>2 \<noteq> 0"
+    by (metis power_one sum_power2_eq_zero_iff zero_neq_one)
+  have "Re (Ln ((1 - \<i> * x) * inverse (1 + \<i> * x))) = 0"
+    apply (rule norm_exp_imaginary)
+    apply (subst exp_Ln)
+    using ne apply (simp_all add: cmod_def complex_eq_iff)
+    apply (auto simp: divide_simps)
+    apply algebra
+    done
+  then show ?thesis
+    unfolding Arctan_def divide_complex_def by (simp add: complex_eq_iff)
+qed

lemma arctan_eq_Re_Arctan: "arctan x = Re (Arctan (of_real x))"
proof (rule arctan_unique)
@@ -2796,15 +2790,13 @@
lemma abs_arctan_le:
fixes x::real shows "\<bar>arctan x\<bar> \<le> \<bar>x\<bar>"
proof -
-  { 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 field_differentiable_bound [OF convex_Reals, of Arctan _ 1])
-      apply (rule has_field_derivative_at_within [OF has_field_derivative_Arctan])
-      apply (force simp add: Reals_def)
-      apply (simp add: norm_divide divide_simps in_Reals_norm complex_is_Real_iff power2_eq_square)
-      using * by auto
-  }
+  have 1: "\<And>x. x \<in> \<real> \<Longrightarrow> cmod (inverse (1 + x\<^sup>2)) \<le> 1"
+    by (simp add: norm_divide divide_simps in_Reals_norm complex_is_Real_iff power2_eq_square)
+  have "cmod (Arctan w - Arctan z) \<le> 1 * cmod (w-z)" if "w \<in> \<real>" "z \<in> \<real>" for w z
+    apply (rule field_differentiable_bound [OF convex_Reals, of Arctan _ 1])
+       apply (rule has_field_derivative_at_within [OF has_field_derivative_Arctan])
+    using 1 that apply (auto simp: Reals_def)
+    done
then have "cmod (Arctan (of_real x) - Arctan 0) \<le> 1 * cmod (of_real x -0)"
using Reals_0 Reals_of_real by blast
then show ?thesis
@@ -2826,15 +2818,14 @@
"arctan x \<le> (\<Sum>k<2 * n + 1. (- 1) ^ k * (1 / real (k * 2 + 1) * x ^ (k * 2 + 1)))"
proof -
have tendsto_zero: "?a \<longlonglongrightarrow> 0"
-    using assms
-    apply -
-    apply (rule tendsto_eq_rhs[where x="0 * 0"])
-    subgoal by (intro tendsto_mult real_tendsto_divide_at_top)
+  proof (rule tendsto_eq_rhs)
+    show "(\<lambda>k. 1 / real (k * 2 + 1) * x ^ (k * 2 + 1)) \<longlonglongrightarrow> 0 * 0"
+      using assms
+      by (intro tendsto_mult real_tendsto_divide_at_top)
(auto simp: filterlim_real_sequentially filterlim_sequentially_iff_filterlim_real
intro!: real_tendsto_divide_at_top tendsto_power_zero filterlim_real_sequentially
-    subgoal by simp
-    done
+  qed simp
have nonneg: "0 \<le> ?a n" for n
by (force intro!: divide_nonneg_nonneg mult_nonneg_nonneg zero_le_power assms)
have le: "?a (Suc n) \<le> ?a n" for n
@@ -2849,8 +2840,7 @@
subsection \<open>Bounds on pi using real arctangent\<close>

lemma pi_machin: "pi = 16 * arctan (1 / 5) - 4 * arctan (1 / 239)"
-  using machin
-  by simp
+  using machin by simp

lemma pi_approx: "3.141592653588 \<le> pi" "pi \<le> 3.1415926535899"
unfolding pi_machin
@@ -2885,10 +2875,10 @@
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
-    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
+  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

lemma isCont_Arcsin_lemma:
assumes le0: "Re (\<i> * z + csqrt (1 - z\<^sup>2)) \<le> 0" and "(Im z = 0 \<Longrightarrow> \<bar>Re z\<bar> < 1)"
@@ -2899,6 +2889,8 @@
using assms by (fastforce simp: cmod_def abs_square_less_1 [symmetric])
next
case False
+  have leim: "(cmod (1 - z\<^sup>2) + (1 - Re (z\<^sup>2))) / 2 \<le> (Im z)\<^sup>2"
+    using le0 sqrt_le_D by fastforce
have neq: "(cmod z)\<^sup>2 \<noteq> 1 + cmod (1 - z\<^sup>2)"
assume "(Re z)\<^sup>2 + (Im z)\<^sup>2 = 1 + sqrt ((1 - Re (z\<^sup>2))\<^sup>2 + (Im (z\<^sup>2))\<^sup>2)"
@@ -2908,12 +2900,8 @@
qed
moreover have 2: "(Im z)\<^sup>2 = (1 + ((Im z)\<^sup>2 + cmod (1 - z\<^sup>2)) - (Re z)\<^sup>2) / 2"
-    using le0
-    apply simp
-    apply (drule sqrt_le_D)
-    using cmod_power2 [of z] norm_triangle_ineq2 [of "z^2" 1]
-    apply (simp add: norm_power Re_power2 norm_minus_commute [of 1])
-    done
+    using leim cmod_power2 [of z] norm_triangle_ineq2 [of "z^2" 1]
+    by (simp add: norm_power Re_power2 norm_minus_commute [of 1])
ultimately show False
by (simp add: Re_power2 Im_power2 cmod_power2)
qed
@@ -2922,15 +2910,12 @@
assumes "(Im z = 0 \<Longrightarrow> \<bar>Re z\<bar> < 1)"
shows "isCont Arcsin z"
proof -
-  have *: "\<i> * z + csqrt (1 - z\<^sup>2) \<notin> \<real>\<^sub>\<le>\<^sub>0"
+  have 1: "\<i> * z + csqrt (1 - z\<^sup>2) \<notin> \<real>\<^sub>\<le>\<^sub>0"
by (metis isCont_Arcsin_lemma assms complex_nonpos_Reals_iff)
+  have 2: "1 - z\<^sup>2 \<notin> \<real>\<^sub>\<le>\<^sub>0"
+    by (simp add: one_minus_z2_notin_nonpos_Reals assms)
show ?thesis
-    using assms
-    apply (rule isCont_Ln' isCont_csqrt' continuous_intros)+
-    apply (simp add: one_minus_z2_notin_nonpos_Reals assms)
-    apply (rule *)
-    done
+    using assms unfolding Arcsin_def by (intro isCont_Ln' isCont_csqrt' continuous_intros 1 2)
qed

lemma isCont_Arcsin' [simp]:
@@ -2982,10 +2967,7 @@
also have "... =  - (\<i> * Ln (exp (\<i>*z)))"
also have "... = z"
-    apply (subst Complex_Transcendental.Ln_exp)
-    using assms
-    apply (auto simp: abs_if simp del: eq_divide_eq_numeral1 split: if_split_asm)
-    done
+    using assms by (auto simp: abs_if simp del: eq_divide_eq_numeral1 split: if_split_asm)
finally show ?thesis .
qed

@@ -3003,21 +2985,15 @@
by (metis Arcsin_1 Arcsin_sin Im_complex_of_real Re_complex_of_real abs_of_nonneg of_real_minus pi_half_ge_zero power2_minus real_sqrt_abs sin_Arcsin sin_minus)

lemma has_field_derivative_Arcsin:
-  assumes "(Im z = 0 \<Longrightarrow> \<bar>Re z\<bar> < 1)"
+  assumes "Im z = 0 \<Longrightarrow> \<bar>Re z\<bar> < 1"
shows "(Arcsin has_field_derivative inverse(cos(Arcsin z))) (at z)"
-proof -
+proof -
have "(sin (Arcsin z))\<^sup>2 \<noteq> 1"
-    using assms
-    apply atomize
-    apply (auto simp: complex_eq_iff Re_power2 Im_power2 abs_square_eq_1)
-    apply (metis abs_minus_cancel abs_one abs_power2 numeral_One numeral_neq_neg_one)
-    by (metis abs_minus_cancel abs_one abs_power2 one_neq_neg_one)
+    using assms one_minus_z2_notin_nonpos_Reals by force
then have "cos (Arcsin z) \<noteq> 0"
by (metis diff_0_right power_zero_numeral sin_squared_eq)
then show ?thesis
-    apply (rule has_field_derivative_inverse_basic [OF DERIV_sin _ _ open_ball [of z 1]])
-    apply (auto intro: isCont_Arcsin assms)
-    done
+    by (rule has_field_derivative_inverse_basic [OF DERIV_sin _ _ open_ball [of z 1]]) (auto intro: isCont_Arcsin assms)
qed

declare has_field_derivative_Arcsin [derivative_intros]
@@ -3049,13 +3025,11 @@
"Arccos \<equiv> \<lambda>z. -\<i> * Ln(z + \<i> * csqrt(1 - z\<^sup>2))"

lemma Arccos_range_lemma: "\<bar>Re z\<bar> < 1 \<Longrightarrow> 0 < Im(z + \<i> * csqrt(1 - z\<^sup>2))"
-  using Arcsin_range_lemma [of "-z"]
-  by simp
+  using Arcsin_range_lemma [of "-z"]  by simp

lemma Arccos_body_lemma: "z + \<i> * csqrt(1 - z\<^sup>2) \<noteq> 0"
using Arcsin_body_lemma [of z]
-  by (metis complex_i_mult_minus diff_add_cancel minus_diff_eq minus_unique mult.assoc mult.left_commute
-           power2_csqrt power2_eq_square zero_neq_one)
+  by (metis Arcsin_body_lemma complex_i_mult_minus diff_minus_eq_add power2_minus right_minus_eq)

lemma Re_Arccos: "Re(Arccos z) = Im (Ln (z + \<i> * csqrt(1 - z\<^sup>2)))"
@@ -3158,7 +3132,7 @@
using Arccos_cos by blast

lemma Arccos_0 [simp]: "Arccos 0 = pi/2"
-  by (rule Arccos_unique) (auto simp: of_real_numeral)
+  by (rule Arccos_unique) auto

lemma Arccos_1 [simp]: "Arccos 1 = 0"
by (rule Arccos_unique) auto
@@ -3170,19 +3144,15 @@
assumes "(Im z = 0 \<Longrightarrow> \<bar>Re z\<bar> < 1)"
shows "(Arccos has_field_derivative - inverse(sin(Arccos z))) (at z)"
proof -
-  have "(cos (Arccos z))\<^sup>2 \<noteq> 1"
-    using assms
-    apply atomize
-    apply (auto simp: complex_eq_iff Re_power2 Im_power2 abs_square_eq_1)
-    apply (metis abs_minus_cancel abs_one abs_power2 numeral_One numeral_neq_neg_one)
-    apply (metis left_minus less_irrefl power_one sum_power2_gt_zero_iff zero_neq_neg_one)
-    done
+  have "x\<^sup>2 \<noteq> -1" for x::real
+    by (sos "((R<1 + (([~1] * A=0) + (R<1 * (R<1 * [x__]^2)))))")
+  with assms have "(cos (Arccos z))\<^sup>2 \<noteq> 1"
+    by (auto simp: complex_eq_iff Re_power2 Im_power2 abs_square_eq_1)
then have "- sin (Arccos z) \<noteq> 0"
by (metis cos_squared_eq diff_0_right mult_zero_left neg_0_equal_iff_equal power2_eq_square)
then have "(Arccos has_field_derivative inverse(- sin(Arccos z))) (at z)"
-    apply (rule has_field_derivative_inverse_basic [OF DERIV_cos _ _ open_ball [of z 1]])
-    apply (auto intro: isCont_Arccos assms)
-    done
+    by (rule has_field_derivative_inverse_basic [OF DERIV_cos _ _ open_ball [of z 1]])
+       (auto intro: isCont_Arccos assms)
then show ?thesis
by simp
qed```