# HG changeset patch
# User paulson
# Date 1653911182 -3600
# Node ID 4f9809edf95ad18fd15499ecff7e4937039c01c1
# Parent  f775dfb556552be002c3e5e9b15f7fe4c91199e1# Parent  eded3fe9e600f04a4d9d8930908b6cf45d4ea3e6
merged

diff -r f775dfb55655 -r 4f9809edf95a src/HOL/Analysis/Complex_Transcendental.thy
--- a/src/HOL/Analysis/Complex_Transcendental.thy	Mon May 30 11:51:34 2022 +0200
+++ b/src/HOL/Analysis/Complex_Transcendental.thy	Mon May 30 12:46:22 2022 +0100
@@ -491,6 +491,27 @@
   finally show ?thesis .
 qed
 
+lemma cos_gt_neg1:
+  assumes "(t::real) \<in> {-pi<..<pi}"
+  shows   "cos t > -1"
+proof -
+  have "cos t \<ge> -1"
+    by simp
+  moreover have "cos t \<noteq> -1"
+  proof
+    assume "cos t = -1"
+    then obtain n where n: "t = (2 * of_int n + 1) * pi"
+      by (subst (asm) cos_eq_minus1) auto
+    from assms have "t / pi \<in> {-1<..<1}"
+      by (auto simp: field_simps)
+    also from n have "t / pi = of_int (2 * n + 1)"
+      by auto
+    finally show False
+      by auto
+  qed
+  ultimately show ?thesis by linarith
+qed
+
 lemma dist_exp_i_1: "norm(exp(\<i> * of_real t) - 1) = 2 * \<bar>sin(t / 2)\<bar>"
 proof -
   have "sqrt (2 - cos t * 2) = 2 * \<bar>sin (t / 2)\<bar>"
@@ -529,7 +550,7 @@
   qed
 next
   assume ?rhs
-  then consider n::int where "w = z + of_real (2 * of_int n * pi)" 
+  then consider n::int where "w = z + of_real (2 * of_int n * pi)"
               | n::int where  " w = -z + of_real ((2 * of_int n + 1) * pi)"
     using Ints_cases by blast
   then show ?lhs
@@ -540,7 +561,7 @@
       by (auto simp: algebra_simps)
   next
     case 2
-    then show ?thesis 
+    then show ?thesis
       using Periodic_Fun.sin.plus_of_int [of "-z" "n"]
       apply (simp add: algebra_simps)
       by (metis add.commute add.inverse_inverse add_diff_cancel_left diff_add_cancel sin_plus_pi)
@@ -1051,7 +1072,7 @@
   unfolding nonneg_Reals_def by fastforce
 
 lemma Arg2pi_eq_pi: "Arg2pi z = pi \<longleftrightarrow> z \<in> \<real> \<and> Re z < 0"
-    using Arg2pi_le_pi [of z] Arg2pi_lt_pi [of z] Arg2pi_eq_0 [of z] Arg2pi_ge_0 [of z] 
+    using Arg2pi_le_pi [of z] Arg2pi_lt_pi [of z] Arg2pi_eq_0 [of z] Arg2pi_ge_0 [of z]
     by (fastforce simp: complex_is_Real_iff)
 
 lemma Arg2pi_eq_0_pi: "Arg2pi z = 0 \<or> Arg2pi z = pi \<longleftrightarrow> z \<in> \<real>"
@@ -1303,7 +1324,7 @@
   have 1: "open ?U"
     by (simp add: open_Collect_conj open_halfspace_Im_gt open_halfspace_Im_lt)
   have 2: "\<And>x. x \<in> ?U \<Longrightarrow> (exp has_derivative blinfun_apply(Blinfun ((*) (exp x)))) (at x)"
-    by (simp add: bounded_linear_Blinfun_apply bounded_linear_mult_right has_field_derivative_imp_has_derivative)   
+    by (simp add: bounded_linear_Blinfun_apply bounded_linear_mult_right has_field_derivative_imp_has_derivative)
   have 3: "continuous_on ?U (\<lambda>x. Blinfun ((*) (exp x)))"
     unfolding blinfun_mult_right.abs_eq [symmetric] by (intro continuous_intros)
   have 4: "Ln z \<in> ?U"
@@ -1486,7 +1507,7 @@
   also have A: "summable (\<lambda>n. norm z^2 * (inverse (real_of_nat (Suc (Suc n))) * cmod z ^ n))"
     by (rule summable_mult, rule summable_comparison_test_ev[OF _ summable_geometric[of "norm z"]])
        (auto simp: assms field_simps intro!: always_eventually)
-  hence "norm (\<Sum>i. (-(z^2)) * inverse (of_nat (i+2)) * (-z)^i) 
+  hence "norm (\<Sum>i. (-(z^2)) * inverse (of_nat (i+2)) * (-z)^i)
       \<le> (\<Sum>i. norm (-(z^2) * inverse (of_nat (i+2)) * (-z)^i))"
     by (intro summable_norm)
        (auto simp: norm_power norm_inverse norm_mult mult_ac simp del: of_nat_add of_nat_Suc)
@@ -1525,10 +1546,10 @@
       by auto
     have "\<bar>Im w\<bar> < pi/2 \<longleftrightarrow> 0 < Re(exp w)"
     proof
-      assume "\<bar>Im w\<bar> < pi/2" then show "0 < Re(exp w)" 
+      assume "\<bar>Im w\<bar> < pi/2" then show "0 < Re(exp w)"
         by (auto simp: Re_exp cos_gt_zero_pi split: if_split_asm)
     next
-      assume R: "0 < Re(exp w)" then 
+      assume R: "0 < Re(exp w)" then
       have "\<bar>Im w\<bar> \<noteq> pi/2"
         by (metis cos_minus cos_pi_half mult_eq_0_iff Re_exp abs_if order_less_irrefl)
       then show "\<bar>Im w\<bar> < pi/2"
@@ -1788,7 +1809,7 @@
   assumes "z \<noteq> 0" shows "Arg z = Im (Ln z)"
 proof (rule cis_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 
+    by (metis assms exp_Ln exp_eq_polar nonzero_mult_div_cancel_left norm_eq_zero
               norm_exp_eq_Re of_real_eq_0_iff sgn_eq)
   show "- pi < Im (Ln z)"
     by (simp add: assms mpi_less_Im_Ln)
@@ -2127,7 +2148,7 @@
   consider "Re z < 0" | "Im z \<noteq> 0" using assms
     using complex_nonneg_Reals_iff not_le by blast
   then have [simp]: "(\<lambda>z. Im (Ln (- z)) + pi) \<midarrow>z\<rightarrow> Arg2pi z"
-    using "*" by (simp add: Arg2pi_Ln Arg2pi_gt_0 assms continuous_within) 
+    using "*" by (simp add: Arg2pi_Ln Arg2pi_gt_0 assms continuous_within)
   show ?thesis
     unfolding continuous_at
   proof (rule Lim_transform_within_open)
@@ -3143,7 +3164,7 @@
   have ne: "1 + x\<^sup>2 \<noteq> 0"
     by (metis power_one sum_power2_eq_zero_iff zero_neq_one)
   have ne1: "1 + \<i> * complex_of_real x \<noteq> 0"
-    using Complex_eq complex_eq_cancel_iff2 by fastforce 
+    using Complex_eq complex_eq_cancel_iff2 by fastforce
   have "Re (Ln ((1 - \<i> * x) * inverse (1 + \<i> * x))) = 0"
     apply (rule norm_exp_imaginary)
     using ne
@@ -3822,7 +3843,7 @@
   fix x'
   assume "- (pi / 2) \<le> x'" "x' \<le> pi / 2" "x = sin x'"
   then show "x' = Re (Arcsin (complex_of_real (sin x')))"
-    unfolding sin_of_real [symmetric] 
+    unfolding sin_of_real [symmetric]
     by (subst Arcsin_sin) auto
 qed
 
diff -r f775dfb55655 -r 4f9809edf95a src/HOL/Complex.thy
--- a/src/HOL/Complex.thy	Mon May 30 11:51:34 2022 +0200
+++ b/src/HOL/Complex.thy	Mon May 30 12:46:22 2022 +0100
@@ -729,6 +729,12 @@
 lemma Im_sum[simp]: "Im (sum f s) = (\<Sum>x\<in>s. Im(f x))"
   by (induct s rule: infinite_finite_induct) auto
 
+lemma sum_Re_le_cmod: "(\<Sum>i\<in>I. Re (z i)) \<le> cmod (\<Sum>i\<in>I. z i)"
+  by (metis Re_sum complex_Re_le_cmod)
+
+lemma sum_Im_le_cmod: "(\<Sum>i\<in>I. Im (z i)) \<le> cmod (\<Sum>i\<in>I. z i)"
+  by (smt (verit, best) Im_sum abs_Im_le_cmod sum.cong)
+
 lemma sums_complex_iff: "f sums x \<longleftrightarrow> ((\<lambda>x. Re (f x)) sums Re x) \<and> ((\<lambda>x. Im (f x)) sums Im x)"
   unfolding sums_def tendsto_complex_iff Im_sum Re_sum ..
 
diff -r f775dfb55655 -r 4f9809edf95a src/HOL/Conditionally_Complete_Lattices.thy
--- a/src/HOL/Conditionally_Complete_Lattices.thy	Mon May 30 11:51:34 2022 +0200
+++ b/src/HOL/Conditionally_Complete_Lattices.thy	Mon May 30 12:46:22 2022 +0100
@@ -47,6 +47,8 @@
 
 end
 
+subsection \<open>Preorders\<close>
+
 context preorder
 begin
 
@@ -172,6 +174,8 @@
   using bdd_below_image_antimono[of uminus X] bdd_above_image_antimono[of uminus "uminus`X"]
   by (auto simp: antimono_def image_image)
 
+subsection \<open>Lattices\<close>
+
 context lattice
 begin
 
@@ -231,6 +235,8 @@
 
 \<close>
 
+subsection \<open>Conditionally complete lattices\<close>
+
 class conditionally_complete_lattice = lattice + Sup + Inf +
   assumes cInf_lower: "x \<in> X \<Longrightarrow> bdd_below X \<Longrightarrow> Inf X \<le> x"
     and cInf_greatest: "X \<noteq> {} \<Longrightarrow> (\<And>x. x \<in> X \<Longrightarrow> z \<le> x) \<Longrightarrow> z \<le> Inf X"
@@ -448,6 +454,21 @@
 
 end
 
+text \<open>The special case of well-orderings\<close>
+
+lemma wellorder_InfI:
+  fixes k :: "'a::{wellorder,conditionally_complete_lattice}"
+  assumes "k \<in> A" shows "Inf A \<in> A" 
+  using wellorder_class.LeastI [of "\<lambda>x. x \<in> A" k]
+  by (simp add: Least_le assms cInf_eq_minimum)
+
+lemma wellorder_Inf_le1:
+  fixes k :: "'a::{wellorder,conditionally_complete_lattice}"
+  assumes "k \<in> A" shows "Inf A \<le> k"
+  by (meson Least_le assms bdd_below.I cInf_lower)
+
+subsection \<open>Complete lattices\<close>
+
 instance complete_lattice \<subseteq> conditionally_complete_lattice
   by standard (auto intro: Sup_upper Sup_least Inf_lower Inf_greatest)
 
@@ -530,6 +551,8 @@
 
 end
 
+subsection \<open>Instances\<close>
+
 instance complete_linorder < conditionally_complete_linorder
   ..
 
@@ -763,11 +786,12 @@
      and bdd: "bdd_above (f ` A)" "bdd_below (f ` A)"
      and a: "a \<in> A"
   shows "f a = (\<Sqinter>x\<in>A. f x)"
-apply (rule antisym)
-using a bdd
-apply (auto simp: cINF_lower)
-apply (metis eq cSUP_upper)
-done
+proof (rule antisym)
+  show "f a \<le> \<Sqinter> (f ` A)"
+    by (metis a bdd(1) eq cSUP_upper)
+  show "\<Sqinter> (f ` A) \<le> f a"
+    using a bdd by (auto simp: cINF_lower)
+qed
 
 lemma cSUP_UNION:
   fixes f :: "_ \<Rightarrow> 'b::conditionally_complete_lattice"