# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1676641722 0
# Node ID c16d423c9cb1f7f1f6d3a908da568a8b0708192e
# Parent  e20f5b9ad776211013a40184dad1a21f78ea9110
Moved up a theorem

diff -r e20f5b9ad776 -r c16d423c9cb1 src/HOL/Analysis/Complex_Transcendental.thy
--- a/src/HOL/Analysis/Complex_Transcendental.thy	Thu Feb 16 12:54:24 2023 +0000
+++ b/src/HOL/Analysis/Complex_Transcendental.thy	Fri Feb 17 13:48:42 2023 +0000
@@ -3693,38 +3693,6 @@
 lemma holomorphic_on_Arccos: "(\<And>z. z \<in> s \<Longrightarrow> Im z = 0 \<Longrightarrow> \<bar>Re z\<bar> < 1) \<Longrightarrow> Arccos holomorphic_on s"
   by (simp add: field_differentiable_within_Arccos holomorphic_on_def)
 
-text \<open>This theorem is about REAL cos/arccos but relies on theorems about @{term Arg}\<close>
-lemma cos_eq_arccos_Ex:
-  "cos x = y \<longleftrightarrow> -1\<le>y \<and> y\<le>1 \<and> (\<exists>k::int. x = arccos y + 2*k*pi \<or> x = - arccos y + 2*k*pi)" (is "?L=?R")
-proof
-  assume R: ?R
-  then obtain k::int where "x = arccos y + 2*k*pi \<or> x = - arccos y + 2*k*pi" by auto
-  moreover have "cos x = y" when "x = arccos y + 2*k*pi"
-    by (metis (no_types) R cos_arccos cos_eq_periodic_intro cos_minus minus_add_cancel)
-  moreover have "cos x = y" when "x = -arccos y + 2*k*pi"
-    by (metis add_minus_cancel R cos_arccos cos_eq_periodic_intro uminus_add_conv_diff)
-  ultimately show "cos x = y" by auto
-next
-  assume L: ?L
-  let ?goal = "(\<exists>k::int. x = arccos y + 2*k*pi \<or> x = - arccos y + 2*k*pi)"
-  obtain k::int where k: "-pi < x - k*(2*pi)" "x - k*(2*pi) \<le> pi"
-    using ceiling_divide_lower [of "2*pi" "x-pi"] ceiling_divide_upper [of "2*pi" "x-pi"] 
-    by (simp add: divide_simps algebra_simps) (metis mult.commute)
-  have *: "cos (x - k * 2*pi) = y"
-    using cos.periodic_simps(3)[of x "-k"] L by (auto simp add:field_simps)
-  then have \<section>: ?goal when "x-k*2*pi \<ge> 0"
-    using arccos_cos k that by force
-  moreover have ?goal when "\<not> x-k*2*pi \<ge>0"
-  proof -
-    have "cos (k * 2*pi - x) = y"
-      by (metis * cos_minus minus_diff_eq)
-    then show ?goal
-      using arccos_cos \<section> k by fastforce 
-  qed
-  ultimately show "-1\<le>y \<and> y\<le>1 \<and> ?goal"
-    using L by auto
-qed
-
 subsection\<^marker>\<open>tag unimportant\<close>\<open>Upper and Lower Bounds for Inverse Sine and Cosine\<close>
 
 lemma Arcsin_bounds: "\<bar>Re z\<bar> < 1 \<Longrightarrow> \<bar>Re(Arcsin z)\<bar> < pi/2"
diff -r e20f5b9ad776 -r c16d423c9cb1 src/HOL/Library/Periodic_Fun.thy
--- a/src/HOL/Library/Periodic_Fun.thy	Thu Feb 16 12:54:24 2023 +0000
+++ b/src/HOL/Library/Periodic_Fun.thy	Fri Feb 17 13:48:42 2023 +0000
@@ -147,6 +147,26 @@
 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)
+  by (smt (verit, best) assms cos_eq_neg_periodic_intro cos_minus_pi cos_periodic_pi)
+
+lemma cos_eq_arccos_Ex:
+  "cos x = y \<longleftrightarrow> -1\<le>y \<and> y\<le>1 \<and> (\<exists>k::int. x = arccos y + 2*k*pi \<or> x = - arccos y + 2*k*pi)" (is "?L=?R")
+proof
+  assume ?R then show "cos x = y"
+    by (metis cos.plus_of_int cos_arccos cos_minus id_apply mult.assoc mult.left_commute of_real_eq_id)
+next
+  assume L: ?L
+  let ?goal = "(\<exists>k::int. x = arccos y + 2*k*pi \<or> x = - arccos y + 2*k*pi)"
+  obtain k::int where k: "-pi < x - k*(2*pi)" "x - k*(2*pi) \<le> pi"
+    using ceiling_divide_lower [of "2*pi" "x-pi"] ceiling_divide_upper [of "2*pi" "x-pi"] 
+    by (simp add: divide_simps algebra_simps) (metis mult.commute)
+  have *: "cos (x - k * 2*pi) = y"
+    using cos.periodic_simps(3)[of x "-k"] L by (auto simp add:field_simps)
+  then have **: ?goal when "x-k*2*pi \<ge> 0"
+    using arccos_cos k that by force
+  then show "-1\<le>y \<and> y\<le>1 \<and> ?goal"
+    using "*" arccos_cos2 k(1) by force
+qed
+
 
 end