# HG changeset patch
# User Manuel Eberl <eberlm@in.tum.de>
# Date 1745422326 -7200
# Node ID d96623e4defeb2fc22de24e2da9418e2b6520a6e
# Parent  32a6228f543d89b45c5e4d15def8f76abfe1c03f
injectivity results about sin, cos, cis

diff -r 32a6228f543d -r d96623e4defe src/HOL/Library/Real_Mod.thy
--- a/src/HOL/Library/Real_Mod.thy	Wed Apr 23 14:42:38 2025 +0200
+++ b/src/HOL/Library/Real_Mod.thy	Wed Apr 23 17:32:06 2025 +0200
@@ -238,4 +238,90 @@
   shows   "[a / c = b / c] (rmod m)"
   using rcong_mult_modulus[of a b m "1 / c"] assms by (auto simp: field_simps)
 
+lemma sin_rmod [simp]: "sin (x rmod (2*pi)) = sin x"
+  and cos_rmod [simp]: "cos (x rmod (2*pi)) = cos x"
+  by (simp_all add: rmod_def sin_diff cos_diff)
+
+lemma tan_rmod [simp]: "tan (x rmod (2*pi)) = tan x"
+  and cot_rmod [simp]: "cot (x rmod (2*pi)) = cot x"
+  and cis_rmod [simp]: "cis (x rmod (2*pi)) = cis x"
+  and rcis_rmod [simp]: "rcis r (x rmod (2*pi)) = rcis r x"
+  by (simp_all add: tan_def cot_def complex_eq_iff)
+
+lemma cis_eq_iff: "cis a = cis b \<longleftrightarrow> [a = b] (rmod (2 * pi))"
+proof -
+  have "cis a = cis b \<longleftrightarrow> sin a = sin b \<and> cos a = cos b"
+    by (auto simp: complex_eq_iff)
+  also have "\<dots> \<longleftrightarrow> (\<exists>x. a = b + 2 * pi * real_of_int x)"
+    by (rule sin_cos_eq_iff)
+  also have "\<dots> \<longleftrightarrow> [b = a] (rmod (2 * pi))"
+    by (simp add: rcong_altdef mult_ac)
+  finally show ?thesis
+    by (simp add: rcong_sym_iff)
+qed
+
+lemma cis_eq_1_iff: "cis a = 1 \<longleftrightarrow> (\<exists>n. a = of_int n * (2 * pi))"
+proof -
+  have "cis 0 = cis a \<longleftrightarrow> [0 = a] (rmod (2 * pi))"
+    by (rule cis_eq_iff)
+  also have "\<dots> \<longleftrightarrow> (\<exists>n. a = of_int n * (2 * pi))"
+    unfolding rcong_altdef by simp
+  finally show ?thesis
+    by simp
+qed
+
+lemma cis_cong:
+  assumes "[a = b] (rmod 2 * pi)"
+  shows   "cis a = cis b"
+  using cis_eq_iff assms by blast
+
+lemma rcis_cong:
+  assumes "[a = b] (rmod 2 * pi)"
+  shows   "rcis r a = rcis r b"
+  using assms by (auto simp: rcis_def intro!: cis_cong)
+
+lemma sin_rcong: "[x = y] (rmod (2 * pi)) \<Longrightarrow> sin x = sin y"
+  and cos_rcong: "[x = y] (rmod (2 * pi)) \<Longrightarrow> cos x = cos y"
+  using cis_cong[of x y] by (simp_all add: complex_eq_iff)
+
+lemma sin_eq_sin_conv_rmod:
+  assumes "sin x = sin y"
+  shows   "[x = y] (rmod 2 * pi) \<or> [x = pi - y] (rmod 2 * pi)"
+proof -
+  have "0 = sin y - sin x"
+    using assms by simp
+  hence "sin ((y - x) / 2) = 0 \<or> cos ((y + x) / 2) = 0"
+    unfolding sin_diff_sin by simp
+  hence "(\<exists>i. y = x + real_of_int i * (2 * pi)) \<or>
+         (\<exists>i. pi - y = x + real_of_int (-i) * (2 * pi))"
+    unfolding sin_zero_iff_int2 cos_zero_iff_int2
+    by (auto simp: algebra_simps)
+  thus ?thesis
+    unfolding rcong_altdef by blast
+qed
+
+lemma cos_eq_cos_conv_rmod:
+  assumes "cos x = cos y"
+  shows   "[x = y] (rmod 2 * pi) \<or> [x = -y] (rmod 2 * pi)"
+proof -
+  have "0 = cos y - cos x"
+    using assms by simp
+  hence "sin ((y + x) / 2) = 0 \<or> sin ((x - y) / 2) = 0"
+    unfolding cos_diff_cos by simp
+  hence "(\<exists>i. -y = x + real_of_int (-i) * (2 * pi)) \<or>
+         (\<exists>i. y = x + real_of_int (-i) * (2 * pi))"
+    unfolding sin_zero_iff_int2
+    by (auto simp: algebra_simps)
+  thus ?thesis
+    unfolding rcong_altdef by blast
+qed
+
+lemma sin_eq_sin_conv_rmod_iff:
+  "sin x = sin y \<longleftrightarrow> [x = y] (rmod 2 * pi) \<or> [x = pi - y] (rmod 2 * pi)"
+  by (metis sin_eq_sin_conv_rmod sin_pi_minus sin_rcong)
+
+lemma cos_eq_cos_conv_rmod_iff:
+  "cos x = cos y \<longleftrightarrow> [x = y] (rmod 2 * pi) \<or> [x = -y] (rmod 2 * pi)"
+  by (metis cos_eq_cos_conv_rmod cos_minus cos_rcong)
+
 end
\ No newline at end of file