# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1717444581 -3600
# Node ID 92a66f1df06e3aedcd4307625aa2c05855096865
# Parent  d562aabcc8680f5011f5cc116b6ab1ae83cde8d6
Simplification of sin, cos, exp of multiples of pi

diff -r d562aabcc868 -r 92a66f1df06e src/HOL/Analysis/Complex_Transcendental.thy
--- a/src/HOL/Analysis/Complex_Transcendental.thy	Sun Jun 02 14:11:09 2024 +0200
+++ b/src/HOL/Analysis/Complex_Transcendental.thy	Mon Jun 03 20:56:21 2024 +0100
@@ -63,6 +63,9 @@
 
 subsection\<^marker>\<open>tag unimportant\<close>\<open>The Exponential Function\<close>
 
+lemma exp_npi_numeral: "exp (\<i> * pi * Num.numeral n)  = (-1) ^ Num.numeral n"
+  by (metis exp_of_nat2_mult exp_pi_i' of_nat_numeral)
+
 lemma norm_exp_i_times [simp]: "norm (exp(\<i> * of_real y)) = 1"
   by simp
 
diff -r d562aabcc868 -r 92a66f1df06e src/HOL/Transcendental.thy
--- a/src/HOL/Transcendental.thy	Sun Jun 02 14:11:09 2024 +0200
+++ b/src/HOL/Transcendental.thy	Mon Jun 03 20:56:21 2024 +0100
@@ -3878,6 +3878,18 @@
   for n :: nat
   by (simp add: mult.commute [of pi])
 
+lemma sin_npi_numeral [simp]: "sin(Num.numeral n * pi) = 0"
+  by (metis of_nat_numeral sin_npi)
+
+lemma sin_npi2_numeral [simp]: "sin (pi * Num.numeral n) = 0"
+  by (metis of_nat_numeral sin_npi2)
+
+lemma cos_npi_numeral [simp]: "cos (Num.numeral n * pi) = (- 1) ^ Num.numeral n"
+  by (metis cos_npi of_nat_numeral)
+
+lemma cos_npi2_numeral [simp]: "cos (pi * Num.numeral n) = (- 1) ^ Num.numeral n"
+  by (metis cos_npi2 of_nat_numeral)
+
 lemma cos_two_pi [simp]: "cos (2 * pi) = 1"
   by (simp add: cos_double)