# HG changeset patch
# User paulson
# Date 1625255019 -3600
# Node ID 5b5e015189a4c871dfda515753ced5f9c83e60c7
# Parent  3556303bd38553d37d1a51e9b5d3ba219ad58652# Parent  5f71c16f0b37a2d0b26a713fa06a82aaa4df56d2
merged

diff -r 3556303bd385 -r 5b5e015189a4 src/HOL/Analysis/Complex_Transcendental.thy
--- a/src/HOL/Analysis/Complex_Transcendental.thy	Fri Jul 02 14:08:45 2021 +0200
+++ b/src/HOL/Analysis/Complex_Transcendental.thy	Fri Jul 02 20:43:39 2021 +0100
@@ -1781,7 +1781,7 @@
 text\<open>Unlike in HOL Light, it's defined for the same interval as the complex logarithm: \<open>(-\<pi>,\<pi>]\<close>.\<close>
 
 lemma Arg_eq_Im_Ln:
-  assumes "z \<noteq> 0" shows "arg z = Im (Ln z)"
+  assumes "z \<noteq> 0" shows "Arg z = Im (Ln z)"
 proof (rule arg_unique)
   show "sgn z = cis (Im (Ln z))"
     by (metis assms exp_Ln exp_eq_polar nonzero_mult_div_cancel_left norm_eq_zero 
@@ -1793,11 +1793,9 @@
 qed
 
 text \<open>The 1990s definition of argument coincides with the more recent one\<close>
-lemma Arg_definition_equivalence:
-  shows "arg z = (if z = 0 then 0 else Im (Ln z))"
-  by (simp add: Arg_eq_Im_Ln arg_zero)
-
-definition\<^marker>\<open>tag important\<close> Arg :: "complex \<Rightarrow> real" where "Arg z \<equiv> (if z = 0 then 0 else Im (Ln z))"
+lemma\<^marker>\<open>tag important\<close> Arg_def:
+  shows "Arg z = (if z = 0 then 0 else Im (Ln z))"
+  by (simp add: Arg_eq_Im_Ln Arg_zero)
 
 lemma Arg_of_real: "Arg (of_real r) = (if r<0 then pi else 0)"
   by (simp add: Im_Ln_eq_pi Arg_def)
diff -r 3556303bd385 -r 5b5e015189a4 src/HOL/Complex.thy
--- a/src/HOL/Complex.thy	Fri Jul 02 14:08:45 2021 +0200
+++ b/src/HOL/Complex.thy	Fri Jul 02 20:43:39 2021 +0100
@@ -888,7 +888,6 @@
 lemma rcis_divide: "rcis r1 a / rcis r2 b = rcis (r1 / r2) (a - b)"
   by (simp add: rcis_def cis_divide [symmetric])
 
-
 subsubsection \<open>Complex exponential\<close>
 
 lemma exp_Reals_eq:
@@ -957,15 +956,15 @@
 
 subsubsection \<open>Complex argument\<close>
 
-definition arg :: "complex \<Rightarrow> real"
-  where "arg z = (if z = 0 then 0 else (SOME a. sgn z = cis a \<and> - pi < a \<and> a \<le> pi))"
+definition Arg :: "complex \<Rightarrow> real"
+  where "Arg z = (if z = 0 then 0 else (SOME a. sgn z = cis a \<and> - pi < a \<and> a \<le> pi))"
 
-lemma arg_zero: "arg 0 = 0"
-  by (simp add: arg_def)
+lemma Arg_zero: "Arg 0 = 0"
+  by (simp add: Arg_def)
 
 lemma arg_unique:
   assumes "sgn z = cis x" and "-pi < x" and "x \<le> pi"
-  shows "arg z = x"
+  shows "Arg z = x"
 proof -
   from assms have "z \<noteq> 0" by auto
   have "(SOME a. sgn z = cis a \<and> -pi < a \<and> a \<le> pi) = x"
@@ -987,14 +986,14 @@
     then show "a = x"
       by (simp add: d_def)
   qed (simp add: assms del: Re_sgn Im_sgn)
-  with \<open>z \<noteq> 0\<close> show "arg z = x"
-    by (simp add: arg_def)
+  with \<open>z \<noteq> 0\<close> show "Arg z = x"
+    by (simp add: Arg_def)
 qed
 
 lemma arg_correct:
   assumes "z \<noteq> 0"
-  shows "sgn z = cis (arg z) \<and> -pi < arg z \<and> arg z \<le> pi"
-proof (simp add: arg_def assms, rule someI_ex)
+  shows "sgn z = cis (Arg z) \<and> -pi < Arg z \<and> Arg z \<le> pi"
+proof (simp add: Arg_def assms, rule someI_ex)
   obtain r a where z: "z = rcis r a"
     using rcis_Ex by fast
   with assms have "r \<noteq> 0" by auto
@@ -1016,22 +1015,26 @@
     by fast
 qed
 
-lemma arg_bounded: "- pi < arg z \<and> arg z \<le> pi"
-  by (cases "z = 0") (simp_all add: arg_zero arg_correct)
+lemma Arg_bounded: "- pi < Arg z \<and> Arg z \<le> pi"
+  by (cases "z = 0") (simp_all add: Arg_zero arg_correct)
 
-lemma cis_arg: "z \<noteq> 0 \<Longrightarrow> cis (arg z) = sgn z"
+lemma cis_Arg: "z \<noteq> 0 \<Longrightarrow> cis (Arg z) = sgn z"
   by (simp add: arg_correct)
 
-lemma rcis_cmod_arg: "rcis (cmod z) (arg z) = z"
-  by (cases "z = 0") (simp_all add: rcis_def cis_arg sgn_div_norm of_real_def)
+lemma rcis_cmod_Arg: "rcis (cmod z) (Arg z) = z"
+  by (cases "z = 0") (simp_all add: rcis_def cis_Arg sgn_div_norm of_real_def)
 
-lemma cos_arg_i_mult_zero [simp]: "y \<noteq> 0 \<Longrightarrow> Re y = 0 \<Longrightarrow> cos (arg y) = 0"
-  using cis_arg [of y] by (simp add: complex_eq_iff)
+lemma rcis_cnj:
+  shows "cnj a = rcis (cmod a) (- Arg a)"
+  by (metis cis_cnj complex_cnj_complex_of_real complex_cnj_mult rcis_cmod_Arg rcis_def)
 
-lemma arg_ii [simp]: "arg \<i> = pi/2"
+lemma cos_Arg_i_mult_zero [simp]: "y \<noteq> 0 \<Longrightarrow> Re y = 0 \<Longrightarrow> cos (Arg y) = 0"
+  using cis_Arg [of y] by (simp add: complex_eq_iff)
+
+lemma Arg_ii [simp]: "Arg \<i> = pi/2"
   by (rule arg_unique; simp add: sgn_eq)
 
-lemma arg_minus_ii [simp]: "arg (-\<i>) = -pi/2"
+lemma Arg_minus_ii [simp]: "Arg (-\<i>) = -pi/2"
 proof (rule arg_unique)
   show "sgn (- \<i>) = cis (- pi / 2)"
     by (simp add: sgn_eq)
@@ -1097,23 +1100,23 @@
 lemma bij_betw_nth_root_unity:
   fixes c :: complex and n :: nat
   assumes c: "c \<noteq> 0" and n: "n > 0"
-  defines "c' \<equiv> root n (norm c) * cis (arg c / n)"
+  defines "c' \<equiv> root n (norm c) * cis (Arg c / n)"
   shows "bij_betw (\<lambda>z. c' * z) {z. z ^ n = 1} {z. z ^ n = c}"
 proof -
-  have "c' ^ n = of_real (root n (norm c) ^ n) * cis (arg c)"
+  have "c' ^ n = of_real (root n (norm c) ^ n) * cis (Arg c)"
     unfolding of_real_power using n by (simp add: c'_def power_mult_distrib DeMoivre)
   also from n have "root n (norm c) ^ n = norm c" by simp
-  also from c have "of_real \<dots> * cis (arg c) = c" by (simp add: cis_arg Complex.sgn_eq)
+  also from c have "of_real \<dots> * cis (Arg c) = c" by (simp add: cis_Arg Complex.sgn_eq)
   finally have [simp]: "c' ^ n = c" .
 
   show ?thesis unfolding bij_betw_def inj_on_def
   proof safe
     fix z :: complex assume "z ^ n = 1"
     hence "(c' * z) ^ n = c' ^ n" by (simp add: power_mult_distrib)
-    also have "c' ^ n = of_real (root n (norm c) ^ n) * cis (arg c)"
+    also have "c' ^ n = of_real (root n (norm c) ^ n) * cis (Arg c)"
       unfolding of_real_power using n by (simp add: c'_def power_mult_distrib DeMoivre)
     also from n have "root n (norm c) ^ n = norm c" by simp
-    also from c have "\<dots> * cis (arg c) = c" by (simp add: cis_arg Complex.sgn_eq)
+    also from c have "\<dots> * cis (Arg c) = c" by (simp add: cis_Arg Complex.sgn_eq)
     finally show "(c' * z) ^ n = c" .
   next
     fix z assume z: "c = z ^ n"
@@ -1188,7 +1191,7 @@
   finally show ?thesis .
 next
   case False
-  define c' where "c' = root n (norm c) * cis (arg c / n)"
+  define c' where "c' = root n (norm c) * cis (Arg c / n)"
   from False and assms have "(\<Sum>{z. z ^ n = c}) = (\<Sum>z | z ^ n = 1. c' * z)"
     by (subst sum.reindex_bij_betw [OF bij_betw_nth_root_unity, symmetric])
        (auto simp: sum_distrib_left finite_roots_unity c'_def)
diff -r 3556303bd385 -r 5b5e015189a4 src/HOL/Complex_Analysis/Complex_Residues.thy
--- a/src/HOL/Complex_Analysis/Complex_Residues.thy	Fri Jul 02 14:08:45 2021 +0200
+++ b/src/HOL/Complex_Analysis/Complex_Residues.thy	Fri Jul 02 20:43:39 2021 +0100
@@ -11,11 +11,6 @@
   "residue f z = (SOME int. \<exists>e>0. \<forall>\<epsilon>>0. \<epsilon><e
     \<longrightarrow> (f has_contour_integral 2*pi* \<i> *int) (circlepath z \<epsilon>))"
 
-lemma Eps_cong:
-  assumes "\<And>x. P x = Q x"
-  shows   "Eps P = Eps Q"
-  using ext[of P Q, OF assms] by simp
-
 lemma residue_cong:
   assumes eq: "eventually (\<lambda>z. f z = g z) (at z)" and "z = z'"
   shows   "residue f z = residue g z'"
@@ -542,4 +537,4 @@
     using Gamma_residues[of n] by simp
 qed auto
 
-end
\ No newline at end of file
+end
diff -r 3556303bd385 -r 5b5e015189a4 src/HOL/Nonstandard_Analysis/NSComplex.thy
--- a/src/HOL/Nonstandard_Analysis/NSComplex.thy	Fri Jul 02 14:08:45 2021 +0200
+++ b/src/HOL/Nonstandard_Analysis/NSComplex.thy	Fri Jul 02 20:43:39 2021 +0100
@@ -45,7 +45,7 @@
   where "hsgn = *f* sgn"
 
 definition harg :: "hcomplex \<Rightarrow> hypreal"
-  where "harg = *f* arg"
+  where "harg = *f* Arg"
 
 definition  \<comment> \<open>abbreviation for \<open>cos a + i sin a\<close>\<close>
   hcis :: "hypreal \<Rightarrow> hcomplex"
diff -r 3556303bd385 -r 5b5e015189a4 src/HOL/Series.thy
--- a/src/HOL/Series.thy	Fri Jul 02 14:08:45 2021 +0200
+++ b/src/HOL/Series.thy	Fri Jul 02 20:43:39 2021 +0100
@@ -58,7 +58,7 @@
   by simp
 
 lemma sums_cong: "(\<And>n. f n = g n) \<Longrightarrow> f sums c \<longleftrightarrow> g sums c"
-  by (drule ext) simp
+  by presburger
 
 lemma sums_summable: "f sums l \<Longrightarrow> summable f"
   by (simp add: sums_def summable_def, blast)
@@ -67,8 +67,7 @@
   by (simp add: summable_def sums_def convergent_def)
 
 lemma summable_iff_convergent': "summable f \<longleftrightarrow> convergent (\<lambda>n. sum f {..n})"
-  by (simp_all only: summable_iff_convergent convergent_def
-        lessThan_Suc_atMost [symmetric] filterlim_sequentially_Suc[of "\<lambda>n. sum f {..<n}"])
+  by (simp add: convergent_def summable_def sums_def_le)
 
 lemma suminf_eq_lim: "suminf f = lim (\<lambda>n. \<Sum>i<n. f i)"
   by (simp add: suminf_def sums_def lim_def)
@@ -82,11 +81,10 @@
 lemma sums_group: "f sums s \<Longrightarrow> 0 < k \<Longrightarrow> (\<lambda>n. sum f {n * k ..< n * k + k}) sums s"
   apply (simp only: sums_def sum.nat_group tendsto_def eventually_sequentially)
   apply (erule all_forward imp_forward exE| assumption)+
-  apply (rule_tac x="N" in exI)
   by (metis le_square mult.commute mult.left_neutral mult_le_cancel2 mult_le_mono)
 
 lemma suminf_cong: "(\<And>n. f n = g n) \<Longrightarrow> suminf f = suminf g"
-  by (rule arg_cong[of f g], rule ext) simp
+  by presburger
 
 lemma summable_cong:
   fixes f g :: "nat \<Rightarrow> 'a::real_normed_vector"
@@ -225,16 +223,13 @@
   assumes "summable f" and pos: "\<And>n. 0 \<le> f n"
   shows "suminf f = 0 \<longleftrightarrow> (\<forall>n. f n = 0)"
 proof
-  assume "suminf f = 0" 
+  assume L: "suminf f = 0" 
   then have f: "(\<lambda>n. \<Sum>i<n. f i) \<longlonglongrightarrow> 0"
     using summable_LIMSEQ[of f] assms by simp
   then have "\<And>i. (\<Sum>n\<in>{i}. f n) \<le> 0"
-  proof (rule LIMSEQ_le_const)
-    show "\<exists>N. \<forall>n\<ge>N. (\<Sum>n\<in>{i}. f n) \<le> sum f {..<n}" for i
-      using pos by (intro exI[of _ "Suc i"] allI impI sum_mono2) auto
-  qed
+    by (metis L \<open>summable f\<close> order_refl pos sum.infinite sum_le_suminf)
   with pos show "\<forall>n. f n = 0"
-    by (auto intro!: antisym)
+    by (simp add: order.antisym)
 qed (metis suminf_zero fun_eq_iff)
 
 lemma suminf_pos_iff: "summable f \<Longrightarrow> (\<And>n. 0 \<le> f n) \<Longrightarrow> 0 < suminf f \<longleftrightarrow> (\<exists>i. 0 < f i)"
@@ -735,11 +730,11 @@
     proof (cases m n rule: linorder_class.le_cases)
       assume "m \<le> n"
       then show ?thesis
-        by (metis Groups_Big.sum_diff N finite_lessThan lessThan_minus_lessThan lessThan_subset_iff norm_minus_commute \<open>m\<ge>N\<close>)
+        by (metis N finite_lessThan lessThan_minus_lessThan lessThan_subset_iff norm_minus_commute sum_diff \<open>m\<ge>N\<close>)
     next
       assume "n \<le> m"
       then show ?thesis
-        by (metis Groups_Big.sum_diff N finite_lessThan lessThan_minus_lessThan lessThan_subset_iff \<open>n\<ge>N\<close>)
+        by (metis N finite_lessThan lessThan_minus_lessThan lessThan_subset_iff sum_diff \<open>n\<ge>N\<close>)
     qed
     then show "\<exists>M. \<forall>m\<ge>M. \<forall>n\<ge>M. norm (sum f {..<m} - sum f {..<n}) < e"
       by blast
@@ -748,13 +743,14 @@
 
 lemma summable_Cauchy':
   fixes f :: "nat \<Rightarrow> 'a :: banach"
-  assumes "eventually (\<lambda>m. \<forall>n\<ge>m. norm (sum f {m..<n}) \<le> g m) sequentially"
-  assumes "filterlim g (nhds 0) sequentially"
+  assumes ev: "eventually (\<lambda>m. \<forall>n\<ge>m. norm (sum f {m..<n}) \<le> g m) sequentially"
+  assumes g0: "g \<longlonglongrightarrow> 0"
   shows "summable f"
 proof (subst summable_Cauchy, intro allI impI, goal_cases)
   case (1 e)
-  from order_tendstoD(2)[OF assms(2) this] and assms(1)
-  have "eventually (\<lambda>m. \<forall>n. norm (sum f {m..<n}) < e) at_top"
+  then have "\<forall>\<^sub>F x in sequentially. g x < e"
+    using g0 order_tendstoD(2) by blast
+  with ev have "eventually (\<lambda>m. \<forall>n. norm (sum f {m..<n}) < e) at_top"
   proof eventually_elim
     case (elim m)
     show ?case