--- 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
--- /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
--- 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"
--- 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
--- 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