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