# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1674653864 0
# Node ID b4f892d0625d66226855ff0180a2ddd1cbc89822
# Parent  6e2c6ccc5dc02e6d62b7463b96a61381a3a4c7f8
Some new material from the AFP

diff -r 6e2c6ccc5dc0 -r b4f892d0625d src/HOL/Algebra/Algebra.thy
--- a/src/HOL/Algebra/Algebra.thy	Tue Jan 24 23:05:32 2023 +0100
+++ b/src/HOL/Algebra/Algebra.thy	Wed Jan 25 13:37:44 2023 +0000
@@ -3,5 +3,6 @@
 theory Algebra
   imports Sylow Chinese_Remainder Zassenhaus Galois_Connection Generated_Fields Free_Abelian_Groups
      Divisibility Embedded_Algebras IntRing Sym_Groups Exact_Sequence Polynomials Algebraic_Closure
+     Left_Coset
 begin
 end
diff -r 6e2c6ccc5dc0 -r b4f892d0625d src/HOL/Algebra/Left_Coset.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Algebra/Left_Coset.thy	Wed Jan 25 13:37:44 2023 +0000
@@ -0,0 +1,137 @@
+theory Left_Coset
+imports Coset
+
+(*This instance of Coset.thy but for left cosets is due to Jonas Rädle and has been imported
+  from the AFP entry Orbit_Stabiliser. *)
+
+begin
+
+definition
+  LCOSETS  :: "[_, 'a set] \<Rightarrow> ('a set)set"   ("lcosets\<index> _" [81] 80)
+  where "lcosets\<^bsub>G\<^esub> H = (\<Union>a\<in>carrier G. {a <#\<^bsub>G\<^esub> H})"
+
+definition
+  LFactGroup :: "[('a,'b) monoid_scheme, 'a set] \<Rightarrow> ('a set) monoid" (infixl "LMod" 65)
+    \<comment> \<open>Actually defined for groups rather than monoids\<close>
+   where "LFactGroup G H = \<lparr>carrier = lcosets\<^bsub>G\<^esub> H, mult = set_mult G, one = H\<rparr>"
+
+lemma (in group) lcos_self: "[| x \<in> carrier G; subgroup H G |] ==> x \<in> x <# H"
+  by (simp add: group_l_invI subgroup.lcos_module_rev subgroup.one_closed)
+
+text \<open>Elements of a left coset are in the carrier\<close>
+lemma (in subgroup) elemlcos_carrier:
+  assumes "group G" "a \<in> carrier G" "a' \<in> a <# H"
+  shows "a' \<in> carrier G"
+  by (meson assms group.l_coset_carrier subgroup_axioms)
+
+text \<open>Step one for lemma \<open>rcos_module\<close>\<close>
+lemma (in subgroup) lcos_module_imp:
+  assumes "group G"
+  assumes xcarr: "x \<in> carrier G"
+      and x'cos: "x' \<in> x <# H"
+  shows "(inv x \<otimes> x') \<in> H"
+proof -
+  interpret group G by fact
+  obtain h
+    where hH: "h \<in> H" and x': "x' = x \<otimes> h" and hcarr: "h \<in> carrier G"
+    using assms by (auto simp: l_coset_def)
+  have "(inv x) \<otimes> x' = (inv x) \<otimes> (x \<otimes> h)"
+    by (simp add: x')
+  have "\<dots> = (x \<otimes> inv x) \<otimes> h"
+    by (metis hcarr inv_closed inv_inv l_inv m_assoc xcarr)
+  also have "\<dots> = h"
+    by (simp add: hcarr xcarr)
+  finally have "(inv x) \<otimes> x' = h"
+    using x' by metis
+  then show "(inv x) \<otimes> x' \<in> H"
+    using hH by force
+qed
+
+text \<open>Left cosets are subsets of the carrier.\<close> 
+lemma (in subgroup) lcosets_carrier:
+  assumes "group G"
+  assumes XH: "X \<in> lcosets H"
+  shows "X \<subseteq> carrier G"
+proof -
+  interpret group G by fact
+  show "X \<subseteq> carrier G"
+    using XH l_coset_subset_G subset by (auto simp: LCOSETS_def)
+qed
+
+lemma (in group) lcosets_part_G:
+  assumes "subgroup H G"
+  shows "\<Union>(lcosets H) = carrier G"
+proof -
+  interpret subgroup H G by fact
+  show ?thesis
+  proof
+    show "\<Union> (lcosets H) \<subseteq> carrier G"
+      by (force simp add: LCOSETS_def l_coset_def)
+    show "carrier G \<subseteq> \<Union> (lcosets H)"
+      by (auto simp add: LCOSETS_def intro: lcos_self assms)
+  qed
+qed
+
+lemma (in group) lcosets_subset_PowG:
+     "subgroup H G  \<Longrightarrow> lcosets H \<subseteq> Pow(carrier G)"
+  using lcosets_part_G subset_Pow_Union by blast
+
+lemma (in group) lcos_disjoint:
+  assumes "subgroup H G"
+  assumes p: "a \<in> lcosets H" "b \<in> lcosets H" "a\<noteq>b"
+  shows "a \<inter> b = {}"
+proof -
+  interpret subgroup H G by fact
+  show ?thesis
+    using p l_repr_independence subgroup_axioms unfolding LCOSETS_def disjoint_iff
+    by blast
+qed
+
+text\<open>The next two lemmas support the proof of \<open>card_cosets_equal\<close>.\<close>
+lemma (in group) inj_on_f':
+    "\<lbrakk>H \<subseteq> carrier G;  a \<in> carrier G\<rbrakk> \<Longrightarrow> inj_on (\<lambda>y. y \<otimes> inv a) (a <# H)"
+  by (simp add: inj_on_g l_coset_subset_G)
+
+lemma (in group) inj_on_f'':
+    "\<lbrakk>H \<subseteq> carrier G;  a \<in> carrier G\<rbrakk> \<Longrightarrow> inj_on (\<lambda>y. inv a \<otimes> y) (a <# H)"
+  by (meson inj_on_cmult inv_closed l_coset_subset_G subset_inj_on)
+
+lemma (in group) inj_on_g':
+    "\<lbrakk>H \<subseteq> carrier G;  a \<in> carrier G\<rbrakk> \<Longrightarrow> inj_on (\<lambda>y. a \<otimes> y) H"
+  using inj_on_cmult inj_on_subset by blast
+
+lemma (in group) l_card_cosets_equal:
+  assumes "c \<in> lcosets H" and H: "H \<subseteq> carrier G" and fin: "finite(carrier G)"
+  shows "card H = card c"
+proof -
+  obtain x where x: "x \<in> carrier G" and c: "c = x <# H"
+    using assms by (auto simp add: LCOSETS_def)
+  have "inj_on ((\<otimes>) x) H"
+    by (simp add: H group.inj_on_g' x)
+  moreover
+  have "(\<otimes>) x ` H \<subseteq> x <# H"
+    by (force simp add: m_assoc subsetD l_coset_def)
+  moreover
+  have "inj_on ((\<otimes>) (inv x)) (x <# H)"
+    by (simp add: H group.inj_on_f'' x)
+  moreover
+  have "\<And>h. h \<in> H \<Longrightarrow> inv x \<otimes> (x \<otimes> h) \<in> H"
+    by (metis H in_mono inv_solve_left m_closed x)
+  then have "(\<otimes>) (inv x) ` (x <# H) \<subseteq> H"
+    by (auto simp: l_coset_def)
+  ultimately show ?thesis
+    by (metis H fin c card_bij_eq finite_imageD finite_subset)
+qed
+
+theorem (in group) l_lagrange:
+  assumes "finite(carrier G)" "subgroup H G"
+  shows "card(lcosets H) * card(H) = order(G)"
+proof -
+  have "card H * card (lcosets H) = card (\<Union> (lcosets H))"
+    using card_partition
+    by (metis (no_types, lifting) assms finite_UnionD l_card_cosets_equal lcos_disjoint lcosets_part_G subgroup.subset)
+  then show ?thesis
+    by (simp add: assms(2) lcosets_part_G mult.commute order_def)
+qed
+
+end
diff -r 6e2c6ccc5dc0 -r b4f892d0625d src/HOL/Analysis/Complex_Transcendental.thy
--- a/src/HOL/Analysis/Complex_Transcendental.thy	Tue Jan 24 23:05:32 2023 +0100
+++ b/src/HOL/Analysis/Complex_Transcendental.thy	Wed Jan 25 13:37:44 2023 +0000
@@ -2369,6 +2369,97 @@
    by (smt (verit, best) arctan field_sum_of_halves)
 qed
 
+
+subsection \<open>Characterisation of @{term "Im (Ln z)"} (Wenda Li)\<close>
+
+lemma Im_Ln_eq_pi_half:
+    "z \<noteq> 0 \<Longrightarrow> (Im(Ln z) = pi/2 \<longleftrightarrow> 0 < Im(z) \<and> Re(z) = 0)"
+    "z \<noteq> 0 \<Longrightarrow> (Im(Ln z) = -pi/2 \<longleftrightarrow> Im(z) < 0 \<and> Re(z) = 0)"
+proof -
+  show "z \<noteq> 0 \<Longrightarrow> (Im(Ln z) = pi/2 \<longleftrightarrow> 0 < Im(z) \<and> Re(z) = 0)"
+    by (metis Im_Ln_eq_pi Im_Ln_le_pi Im_Ln_pos_lt Re_Ln_pos_le Re_Ln_pos_lt
+      abs_of_nonneg less_eq_real_def order_less_irrefl pi_half_gt_zero)
+next
+  assume "z\<noteq>0"
+  have "Im (Ln z) = - pi / 2 \<Longrightarrow> Im z < 0 \<and> Re z = 0"
+    by (metis Im_Ln_pos_le Re_Ln_pos_le Re_Ln_pos_lt_imp \<open>z \<noteq> 0\<close> abs_if
+     add.inverse_inverse divide_minus_left less_eq_real_def linorder_not_le minus_pi_half_less_zero)
+  moreover have "Im (Ln z) = - pi / 2" when "Im z < 0" "Re z = 0"
+  proof -
+    obtain r::real where "r>0" "z=r * (-\<i>)"
+      by (smt (verit) \<open>Im z < 0\<close> \<open>Re z = 0\<close> add_0 complex_eq mult.commute mult_minus_right of_real_0 of_real_minus)
+    then have "Im (Ln z) = Im (Ln (r*(-\<i>)))" by auto
+    also have "... = Im (Ln (complex_of_real r) + Ln (- \<i>))"
+      by (metis Ln_times_of_real \<open>0 < r\<close> add.inverse_inverse add.inverse_neutral complex_i_not_zero)
+    also have "... = - pi/2"
+      using \<open>r>0\<close> by simp
+    finally show "Im (Ln z) = - pi / 2" .
+  qed
+  ultimately show "(Im(Ln z) = -pi/2 \<longleftrightarrow> Im(z) < 0 \<and> Re(z) = 0)" by auto
+qed
+
+lemma Im_Ln_eq:
+  assumes "z\<noteq>0"
+  shows "Im (Ln z) = (if Re z\<noteq>0 then
+                        if Re z>0 then
+                           arctan (Im z/Re z)
+                        else if Im z\<ge>0 then
+                           arctan (Im z/Re z) + pi
+                        else
+                           arctan (Im z/Re z) - pi
+                      else
+                        if Im z>0 then pi/2 else -pi/2)"
+proof -
+  have eq_arctan_pos:"Im (Ln z) = arctan (Im z/Re z)" when "Re z>0" for z
+  proof -
+    define wR where "wR \<equiv> Re (Ln z)"
+    define \<theta> where "\<theta> \<equiv> arctan (Im z/Re z)"
+    have "z\<noteq>0" using that by auto
+    have "exp (Complex wR \<theta>) = z"
+    proof (rule complex_eqI)
+      have "Im (exp (Complex wR \<theta>)) =exp wR * sin \<theta> "
+        unfolding Im_exp by simp
+      also have "... = Im z"
+        unfolding wR_def Re_Ln[OF \<open>z\<noteq>0\<close>] \<theta>_def using \<open>z\<noteq>0\<close> \<open>Re z>0\<close>
+        by (auto simp add:sin_arctan divide_simps complex_neq_0 cmod_def real_sqrt_divide)
+      finally show "Im (exp (Complex wR \<theta>)) = Im z" .
+    next
+      have "Re (exp (Complex wR \<theta>)) = exp wR * cos \<theta> "
+        unfolding Re_exp by simp
+      also have "... = Re z"
+        by (metis Arg_eq_Im_Ln Re_exp \<open>z \<noteq> 0\<close> \<theta>_def arg_conv_arctan exp_Ln that wR_def)
+      finally show "Re (exp (Complex wR \<theta>)) = Re z" .
+    qed
+    moreover have "-pi<\<theta>" "\<theta>\<le>pi"
+      using arctan_lbound [of \<open>Im z / Re z\<close>] arctan_ubound [of \<open>Im z / Re z\<close>]
+      by (simp_all add: \<theta>_def)
+    ultimately have "Ln z = Complex wR \<theta>" using Ln_unique by auto
+    then show ?thesis using that unfolding \<theta>_def by auto
+  qed
+  have ?thesis when "Re z=0"
+    using Im_Ln_eq_pi_half[OF \<open>z\<noteq>0\<close>] that
+    using assms complex_eq_iff by auto
+  moreover have ?thesis when "Re z>0"
+    using eq_arctan_pos[OF that] that by auto
+  moreover have ?thesis when "Re z<0" "Im z\<ge>0"
+  proof -
+    have "Im (Ln (- z)) = arctan (Im (- z) / Re (- z))"
+      by (simp add: eq_arctan_pos that(1))
+    moreover have "Ln (- z) = Ln z - \<i> * complex_of_real pi"
+      using Ln_minus assms that by fastforce
+    ultimately show ?thesis using that by auto
+  qed
+  moreover have ?thesis when "Re z<0" "Im z<0"
+  proof -
+    have "Im (Ln (- z)) = arctan (Im (- z) / Re (- z))"
+      by (simp add: eq_arctan_pos that(1))
+    moreover have "Ln (- z) = Ln z + \<i> * complex_of_real pi"
+      using Ln_minus assms that by auto
+    ultimately show ?thesis using that by auto
+  qed
+  ultimately show ?thesis by linarith
+qed
+
 subsection\<^marker>\<open>tag unimportant\<close>\<open>Relation between Ln and Arg2pi, and hence continuity of Arg2pi\<close>
 
 lemma Arg2pi_Ln: "0 < Arg2pi z \<Longrightarrow> Arg2pi z = Im(Ln(-z)) + pi"
diff -r 6e2c6ccc5dc0 -r b4f892d0625d src/HOL/Library/Periodic_Fun.thy
--- a/src/HOL/Library/Periodic_Fun.thy	Tue Jan 24 23:05:32 2023 +0100
+++ b/src/HOL/Library/Periodic_Fun.thy	Wed Jan 25 13:37:44 2023 +0000
@@ -128,5 +128,25 @@
 
 interpretation cot: periodic_fun_simple cot "2 * of_real pi :: 'a :: {real_normed_field,banach}"
   by standard (simp only: cot_def [abs_def] sin.plus_1 cos.plus_1)
-  
+
+lemma cos_eq_neg_periodic_intro:
+  assumes "x - y = 2*(of_int k)*pi + pi \<or> x + y = 2*(of_int k)*pi + pi"
+  shows "cos x = - cos y" using assms
+proof
+  assume "x - y = 2 * (of_int k) * pi + pi" 
+  then show ?thesis
+    using cos.periodic_simps[of "y+pi"]
+    by (auto simp add:algebra_simps)
+next
+  assume "x + y = 2 * real_of_int k * pi + pi "
+  then show ?thesis
+    using cos.periodic_simps[of "-y+pi"]
+    by (clarsimp simp add: algebra_simps) (smt (verit))
+qed
+
+lemma cos_eq_periodic_intro:
+  assumes "x - y = 2*(of_int k)*pi \<or> x + y = 2*(of_int k)*pi"
+  shows "cos x = cos y"
+  by (smt (verit, ccfv_SIG) assms cos_eq_neg_periodic_intro cos_minus_pi cos_periodic_pi)
+
 end
diff -r 6e2c6ccc5dc0 -r b4f892d0625d src/HOL/Transcendental.thy
--- a/src/HOL/Transcendental.thy	Tue Jan 24 23:05:32 2023 +0100
+++ b/src/HOL/Transcendental.thy	Wed Jan 25 13:37:44 2023 +0000
@@ -4826,10 +4826,17 @@
   using cos_gt_zero_pi [of x]
   by (simp add: field_split_simps tan_def real_sqrt_divide abs_if split: if_split_asm)
 
+lemma cos_tan_half: "cos x \<noteq>0 \<Longrightarrow>  cos (2*x) = (1 - (tan x)^2) / (1 + (tan x)^2)"
+  unfolding cos_double tan_def by (auto simp add:field_simps )
+
 lemma sin_tan: "\<bar>x\<bar> < pi/2 \<Longrightarrow> sin x = tan x / sqrt (1 + tan x ^ 2)"
   using cos_gt_zero [of "x"] cos_gt_zero [of "-x"]
   by (force simp: field_split_simps tan_def real_sqrt_divide abs_if split: if_split_asm)
 
+lemma sin_tan_half: "sin (2*x) = 2 * tan x / (1 + (tan x)^2)"
+  unfolding sin_double tan_def
+  by (cases "cos x=0") (auto simp add:field_simps power2_eq_square)
+
 lemma tan_mono_le: "-(pi/2) < x \<Longrightarrow> x \<le> y \<Longrightarrow> y < pi/2 \<Longrightarrow> tan x \<le> tan y"
   using less_eq_real_def tan_monotone by auto