diff --git a/thys/Winding_Number_Eval/Missing_Algebraic.thy b/thys/Winding_Number_Eval/Missing_Algebraic.thy
--- a/thys/Winding_Number_Eval/Missing_Algebraic.thy
+++ b/thys/Winding_Number_Eval/Missing_Algebraic.thy
@@ -1,335 +1,315 @@
 (*
     Author:     Wenda Li <wl302@cam.ac.uk / liwenda1990@hotmail.com>
 *)
 
 section \<open>Some useful lemmas in algebra\<close>
 
 theory Missing_Algebraic imports
   "HOL-Computational_Algebra.Polynomial_Factorial"
   "HOL-Computational_Algebra.Fundamental_Theorem_Algebra"
   "HOL-Complex_Analysis.Complex_Analysis"
   Missing_Topology
   "Budan_Fourier.BF_Misc"
 begin
 
 subsection \<open>Misc\<close>
 
-lemma poly_holomorphic_on[simp]:
-  "(poly p) holomorphic_on s"
-  apply (rule holomorphic_onI)
-  apply (unfold field_differentiable_def)
-  apply (rule_tac x="poly (pderiv p) x" in exI)
-  by (simp add:has_field_derivative_at_within)
+lemma poly_holomorphic_on[simp]: "(poly p) holomorphic_on s"
+  by (meson field_differentiable_def has_field_derivative_at_within holomorphic_onI poly_DERIV)
 
 lemma order_zorder:
   fixes p::"complex poly" and z::complex
   assumes "p\<noteq>0"
   shows "order z p = nat (zorder (poly p) z)"
 proof -
   define n where "n=nat (zorder (poly p) z)" 
   define h where "h=zor_poly (poly p) z"
   have "\<exists>w. poly p w \<noteq> 0" using assms poly_all_0_iff_0 by auto
   then obtain r where "0 < r" "cball z r \<subseteq> UNIV" and 
       h_holo: "h holomorphic_on cball z r" and
       poly_prod:"(\<forall>w\<in>cball z r. poly p w = h w * (w - z) ^ n \<and> h w \<noteq> 0)"
     using zorder_exist_zero[of "poly p" UNIV z,folded h_def] poly_holomorphic_on
     unfolding n_def by auto
   then have "h holomorphic_on ball z r"
     and "(\<forall>w\<in>ball z r. poly p w = h w * (w - z) ^ n)" 
     and "h z\<noteq>0"
     by auto
   then have "order z p = n" using \<open>p\<noteq>0\<close>
   proof (induct n arbitrary:p h)
     case 0
     then have "poly p z=h z" using \<open>r>0\<close> by auto 
     then have "poly p z\<noteq>0" using \<open>h z\<noteq>0\<close> by auto
     then show ?case using order_root by blast
   next
     case (Suc n)
     define sn where "sn=Suc n"
     define h' where "h'\<equiv> \<lambda>w. deriv h w * (w-z)+ sn * h w"
     have "(poly p has_field_derivative poly (pderiv p) w) (at w)" for w
       using poly_DERIV[of p w] .
     moreover have "(poly p has_field_derivative (h' w)*(w-z)^n ) (at w)" when "w\<in>ball z r" for w
     proof (subst DERIV_cong_ev[of w w "poly p" "\<lambda>w.  h w * (w - z) ^ Suc n" ],simp_all)
       show "\<forall>\<^sub>F x in nhds w. poly p x = h x * ((x - z) * (x - z) ^ n)"
         unfolding eventually_nhds using Suc(3) \<open>w\<in>ball z r\<close>
-        apply (intro exI[where x="ball z r"])
-        by auto
+        by (metis Elementary_Metric_Spaces.open_ball power_Suc)
       next
         have "(h has_field_derivative deriv h w) (at w)" 
           using \<open>h holomorphic_on ball z r\<close> \<open>w\<in>ball z r\<close> holomorphic_on_imp_differentiable_at 
           by (simp add: holomorphic_derivI)
         then have "((\<lambda>w. h w * ((w - z) ^ sn)) 
                       has_field_derivative h' w * (w - z) ^ (sn - 1)) (at w)"
           unfolding h'_def
           apply (auto intro!: derivative_eq_intros simp add:field_simps)
           by (auto simp add:field_simps sn_def)
         then show "((\<lambda>w. h w * ((w - z) * (w - z) ^ n)) 
                       has_field_derivative h' w * (w - z) ^ n) (at w)"
           unfolding sn_def by auto
       qed
     ultimately have "\<forall>w\<in>ball z r. poly (pderiv p) w = h' w * (w - z) ^ n"
       using DERIV_unique by blast  
     moreover have "h' holomorphic_on ball z r"
       unfolding h'_def using \<open>h holomorphic_on ball z r\<close>
       by (auto intro!: holomorphic_intros)
     moreover have "h' z\<noteq>0" unfolding h'_def sn_def using \<open>h z \<noteq> 0\<close> of_nat_neq_0 by auto
     moreover have "pderiv p \<noteq> 0"  
     proof 
       assume "pderiv p = 0"
       obtain c where "p=[:c:]" using \<open>pderiv p = 0\<close> using pderiv_iszero by blast
       then have "c=0"
         using Suc(3)[rule_format,of z] \<open>r>0\<close> by auto
       then show False using \<open>p\<noteq>0\<close> using \<open>p=[:c:]\<close> by auto
     qed
     ultimately have "order z (pderiv p) = n" by (auto elim: Suc.hyps)
     moreover have "order z p \<noteq> 0"
       using Suc(3)[rule_format,of z] \<open>r>0\<close> order_root \<open>p\<noteq>0\<close> by auto
     ultimately show ?case using order_pderiv[OF \<open>pderiv p \<noteq> 0\<close>] by auto
   qed
   then show ?thesis unfolding n_def .
 qed  
 
 lemma pcompose_pCons_0:"pcompose p [:a:] = [:poly p a:]"
-  apply (induct p)
-  by (auto simp add:pcompose_pCons algebra_simps)       
+  by (metis (no_types, lifting) coeff_pCons_0 pcompose_0' pcompose_assoc poly_0_coeff_0 poly_pcompose)
    
 lemma pcompose_coeff_0:
   "coeff (pcompose p q) 0 = poly p (coeff q 0)"
-  apply (induct p)
-  by (auto simp add:pcompose_pCons coeff_mult)  
+  by (metis poly_0_coeff_0 poly_pcompose)
     
 lemma poly_field_differentiable_at[simp]:
   "poly p field_differentiable (at x within s)"
-apply (unfold field_differentiable_def)
-apply (rule_tac x="poly (pderiv p) x" in exI)
-by (simp add:has_field_derivative_at_within)  
+  using field_differentiable_at_within field_differentiable_def poly_DERIV by blast
   
 lemma deriv_pderiv:
   "deriv (poly p) = poly (pderiv p)"
-apply (rule ext)  
-apply (rule DERIV_imp_deriv)  
-  using poly_DERIV . 
+  by (meson ext DERIV_imp_deriv poly_DERIV)
     
 lemma lead_coeff_map_poly_nz:
   assumes "f (lead_coeff p) \<noteq>0" "f 0=0"
-  shows "lead_coeff (map_poly f p) = f (lead_coeff p) "
-proof -
-  have "lead_coeff (Poly (map f (coeffs p))) = f (lead_coeff p)"
-    by (metis (mono_tags, lifting) antisym assms(1) assms(2) coeff_0_degree_minus_1 coeff_map_poly 
-        degree_Poly degree_eq_length_coeffs le_degree length_map map_poly_def)
-  then show ?thesis
-    by (simp add: map_poly_def)
-qed 
+  shows "lead_coeff (map_poly f p) = f (lead_coeff p)"
+  by (metis (no_types, lifting) antisym assms coeff_0 coeff_map_poly le_degree leading_coeff_0_iff)
 
 lemma filterlim_poly_at_infinity:
   fixes p::"'a::real_normed_field poly"
   assumes "degree p>0"
   shows "filterlim (poly p) at_infinity at_infinity"
 using assms
 proof (induct p)
   case 0
   then show ?case by auto
 next
   case (pCons a p)
   have ?case when "degree p=0"
   proof -
     obtain c where c_def:"p=[:c:]" using \<open>degree p = 0\<close> degree_eq_zeroE by blast
     then have "c\<noteq>0" using \<open>0 < degree (pCons a p)\<close> by auto
     then show ?thesis unfolding c_def 
       apply (auto intro!:tendsto_add_filterlim_at_infinity)
       apply (subst mult.commute)
       by (auto intro!:tendsto_mult_filterlim_at_infinity filterlim_ident)
   qed
   moreover have ?case when "degree p\<noteq>0"
   proof -
     have "filterlim (poly p) at_infinity at_infinity"
       using that by (auto intro:pCons)
     then show ?thesis 
       by (auto intro!:tendsto_add_filterlim_at_infinity filterlim_at_infinity_times filterlim_ident)
   qed
   ultimately show ?case by auto
 qed  
        
 lemma poly_divide_tendsto_aux:
   fixes p::"'a::real_normed_field poly"
   shows "((\<lambda>x. poly p x/x^(degree p)) \<longlongrightarrow> lead_coeff p) at_infinity"  
 proof (induct p)
   case 0
   then show ?case by (auto intro:tendsto_eq_intros)
 next
   case (pCons a p)
   have ?case when "p=0"
     using that by auto
   moreover have ?case when "p\<noteq>0"
   proof -
     define g where "g=(\<lambda>x. a/(x*x^degree p))"
     define f where "f=(\<lambda>x. poly p x/x^degree p)"
     have "\<forall>\<^sub>Fx in at_infinity. poly (pCons a p) x / x ^ degree (pCons a p) = g x + f x"
     proof (rule eventually_at_infinityI[of 1])
       fix x::'a assume "norm x\<ge>1"
       then have "x\<noteq>0" by auto
       then show "poly (pCons a p) x / x ^ degree (pCons a p) = g x + f x"
         using that unfolding g_def f_def by (auto simp add:field_simps)
     qed
     moreover have "((\<lambda>x. g x+f x) \<longlongrightarrow>  lead_coeff (pCons a p)) at_infinity"
     proof -
       have "(g \<longlongrightarrow>  0) at_infinity"
         unfolding g_def using filterlim_poly_at_infinity[of "monom 1 (Suc (degree p))"]
         apply (auto intro!:tendsto_intros tendsto_divide_0 simp add: degree_monom_eq)
         apply (subst filterlim_cong[where g="poly (monom 1 (Suc (degree p)))"])
         by (auto simp add:poly_monom)
       moreover have "(f \<longlongrightarrow>  lead_coeff (pCons a p)) at_infinity"
         using pCons \<open>p\<noteq>0\<close> unfolding f_def by auto
       ultimately show ?thesis by (auto intro:tendsto_eq_intros)
     qed
     ultimately show ?thesis by (auto dest:tendsto_cong)  
   qed
   ultimately show ?case by auto  
 qed
   
 lemma filterlim_power_at_infinity:
   assumes "n\<noteq>0"
   shows "filterlim (\<lambda>x::'a::real_normed_field. x^n) at_infinity at_infinity" 
   using filterlim_poly_at_infinity[of "monom 1 n"] assms
   apply (subst filterlim_cong[where g="poly (monom 1 n)"])
   by (auto simp add:poly_monom degree_monom_eq)
    
 lemma poly_divide_tendsto_0_at_infinity: 
   fixes p::"'a::real_normed_field poly"
   assumes "degree p > degree q" 
   shows "((\<lambda>x. poly q x / poly p x) \<longlongrightarrow> 0 ) at_infinity" 
 proof -
   define pp where "pp=(\<lambda>x. x^(degree p) / poly p x)"    
   define qq where "qq=(\<lambda>x. poly q x/x^(degree q))"
   define dd where "dd=(\<lambda>x::'a. 1/x^(degree p - degree q))"
   have "\<forall>\<^sub>Fx in at_infinity.  poly q x / poly p x = qq x * pp x * dd x"
   proof (rule eventually_at_infinityI[of 1])
     fix x::'a assume "norm x\<ge>1"
     then have "x\<noteq>0" by auto
     then show "poly q x / poly p x = qq x * pp x * dd x"
       unfolding qq_def pp_def dd_def using assms 
       by (auto simp add:field_simps divide_simps power_diff) 
   qed
   moreover have "((\<lambda>x. qq x * pp x * dd x) \<longlongrightarrow> 0) at_infinity"
   proof -
     have "(qq \<longlongrightarrow> lead_coeff q) at_infinity" 
       unfolding qq_def using poly_divide_tendsto_aux[of q] .
     moreover have "(pp \<longlongrightarrow> 1/lead_coeff p) at_infinity"
     proof -
       have "p\<noteq>0" using assms by auto
       then show ?thesis
         unfolding pp_def using poly_divide_tendsto_aux[of p] 
         apply (drule_tac tendsto_inverse)
         by (auto simp add:inverse_eq_divide)
     qed  
     moreover have "(dd \<longlongrightarrow> 0) at_infinity" 
       unfolding dd_def
       apply (rule tendsto_divide_0)
       by (auto intro!: filterlim_power_at_infinity simp add:assms)
     ultimately show ?thesis by (auto intro:tendsto_eq_intros)
   qed
   ultimately show ?thesis by (auto dest:tendsto_cong)
 qed
-    
+
 lemma lead_coeff_list_def:
   "lead_coeff p= (if coeffs p=[] then 0 else last (coeffs p))"
-by (simp add: last_coeffs_eq_coeff_degree)
-  
+  by (simp add: last_coeffs_eq_coeff_degree)
+
 lemma poly_linepath_comp: 
   fixes a::"'a::{real_normed_vector,comm_semiring_0,real_algebra_1}"
   shows "poly p o (linepath a b) = poly (p \<circ>\<^sub>p [:a, b-a:]) o of_real"
-  apply rule
-  by (auto simp add:poly_pcompose linepath_def scaleR_conv_of_real algebra_simps)
+  by (force simp add:poly_pcompose linepath_def scaleR_conv_of_real algebra_simps)
 
 lemma poly_eventually_not_zero:
   fixes p::"real poly"
   assumes "p\<noteq>0"
   shows "eventually (\<lambda>x. poly p x\<noteq>0) at_infinity"
 proof (rule eventually_at_infinityI[of "Max (norm ` {x. poly p x=0}) + 1"])
   fix x::real assume asm:"Max (norm ` {x. poly p x=0}) + 1 \<le> norm x" 
   have False when "poly p x=0"
   proof - 
     define S where "S=norm `{x. poly p x = 0}"
     have "norm x\<in>S" using that unfolding S_def by auto
     moreover have "finite S" using \<open>p\<noteq>0\<close> poly_roots_finite unfolding S_def by blast
     ultimately have "norm x\<le>Max S" by simp
     moreover have "Max S + 1 \<le> norm x" using asm unfolding S_def by simp
     ultimately show False by argo
   qed
   then show "poly p x \<noteq> 0" by auto
 qed
     
 subsection \<open>More about @{term degree}\<close>
    
 lemma map_poly_degree_eq:
   assumes "f (lead_coeff p) \<noteq>0"
   shows "degree (map_poly f p) = degree p"  
   using assms
   unfolding map_poly_def degree_eq_length_coeffs coeffs_Poly lead_coeff_list_def
   by (metis (full_types) last_conv_nth_default length_map no_trailing_unfold nth_default_coeffs_eq 
       nth_default_map_eq strip_while_idem)
   
 lemma map_poly_degree_less:
   assumes "f (lead_coeff p) =0" "degree p\<noteq>0"
   shows "degree (map_poly f p) < degree p" 
 proof -
   have "length (coeffs p) >1" 
     using \<open>degree p\<noteq>0\<close> by (simp add: degree_eq_length_coeffs)  
-  then obtain xs x where xs_def:"coeffs p=xs@[x]" "length xs>0"  
-    by (metis One_nat_def add.commute add_diff_cancel_left' append_Nil assms(2) 
-        degree_eq_length_coeffs length_greater_0_conv list.size(3) list.size(4) not_less_zero
-        rev_exhaust) 
+  then obtain xs x where xs_def:"coeffs p=xs@[x]" "length xs>0"
+    by (metis One_nat_def add_0 append_Nil length_greater_0_conv list.size(4) nat_neq_iff not_less_zero rev_exhaust)
   have "f x=0" using assms(1) by (simp add: lead_coeff_list_def xs_def(1))
   have "degree (map_poly f p) = length (strip_while ((=) 0) (map f (xs@[x]))) - 1" 
     unfolding map_poly_def degree_eq_length_coeffs coeffs_Poly
     by (subst xs_def,auto)
   also have "... = length (strip_while ((=) 0) (map f xs)) - 1"   
     using \<open>f x=0\<close> by simp
   also have "... \<le> length xs -1"
     using length_strip_while_le by (metis diff_le_mono length_map)
   also have "... < length (xs@[x]) - 1"
     using xs_def(2) by auto
   also have "... = degree p"
     unfolding degree_eq_length_coeffs xs_def by simp
   finally show ?thesis .
 qed
   
 lemma map_poly_degree_leq[simp]:
   shows "degree (map_poly f p) \<le> degree p"
   unfolding map_poly_def degree_eq_length_coeffs
   by (metis coeffs_Poly diff_le_mono length_map length_strip_while_le)  
     
 subsection \<open>roots / zeros of a univariate function\<close>
 
 definition roots_within::"('a \<Rightarrow> 'b::zero) \<Rightarrow> 'a set \<Rightarrow> 'a set" where
   "roots_within f s = {x\<in>s. f x = 0}"
   
 abbreviation roots::"('a \<Rightarrow> 'b::zero) \<Rightarrow> 'a set" where
   "roots f \<equiv> roots_within f UNIV"
 
 subsection \<open>The argument principle specialised to polynomials.\<close>
 
 lemma argument_principle_poly:
   assumes "p\<noteq>0" and valid:"valid_path g" and loop: "pathfinish g = pathstart g" 
     and no_proots:"path_image g \<subseteq> - proots p"  
   shows "contour_integral g (\<lambda>x. deriv (poly p) x / poly p x) = 2 * of_real pi * \<i> * 
             (\<Sum>x\<in>proots p. winding_number g x * of_nat (order x p))"  
 proof -
   have "contour_integral g (\<lambda>x. deriv (poly p) x / poly p x) = 2 * of_real pi * \<i> * 
           (\<Sum>x | poly p x = 0. winding_number g x * of_int (zorder (poly p) x))"
     apply (rule argument_principle[of UNIV "poly p" "{}" "\<lambda>_. 1" g,simplified,OF _ valid loop])
     using no_proots[unfolded proots_def] by (auto simp add:poly_roots_finite[OF \<open>p\<noteq>0\<close>] )
   also have "... =  2 * of_real pi * \<i> * (\<Sum>x\<in>proots p. winding_number g x * of_nat (order x p))"
   proof -
     have "nat (zorder (poly p) x) = order x p" when "x\<in>proots p" for x 
       using order_zorder[OF \<open>p\<noteq>0\<close>] that unfolding proots_def by auto
     then show ?thesis unfolding proots_def 
-      apply (auto intro!:comm_monoid_add_class.sum.cong)
+      apply (auto intro!: sum.cong)
       by (metis assms(1) nat_eq_iff2 of_nat_nat order_root)
   qed
   finally show ?thesis . 
 qed  
   
 end
diff --git a/thys/Winding_Number_Eval/Missing_Transcendental.thy b/thys/Winding_Number_Eval/Missing_Transcendental.thy
--- a/thys/Winding_Number_Eval/Missing_Transcendental.thy
+++ b/thys/Winding_Number_Eval/Missing_Transcendental.thy
@@ -1,714 +1,713 @@
 (*
     Author:     Wenda Li <wl302@cam.ac.uk / liwenda1990@hotmail.com>
 *)
 
 section \<open>Some useful lemmas about transcendental functions\<close>
 
 theory Missing_Transcendental imports
   Missing_Topology
   Missing_Algebraic
 begin
 
 subsection \<open>Misc\<close>
 
 lemma exp_Arg2pi2pi_multivalue:
   assumes "exp (\<i> * of_real x) = z"
   shows "\<exists>k::int. x = Arg2pi z + 2*k*pi"
 proof -
   define k where "k=floor( x/(2*pi))"
   define x' where "x'= x - (2*k*pi)"
   have "x'/(2*pi) \<ge>0"  unfolding x'_def k_def by (simp add: diff_divide_distrib)
   moreover have "x'/(2*pi) < 1"
   proof -
     have "x/(2*pi) - k < 1" unfolding k_def by linarith
     thus ?thesis unfolding k_def x'_def by (auto simp add:field_simps)
   qed
   ultimately have "x'\<ge>0" and "x'<2*pi" by (auto simp add:field_simps)
   moreover have "exp (\<i> * complex_of_real x') = z"
     using assms x'_def by  (auto simp add:field_simps )
   ultimately have "Arg2pi z = x'" using Arg2pi_unique[of 1 x' z,simplified] by auto
   hence " x = Arg2pi z + 2*k*pi" unfolding x'_def by auto
   thus ?thesis by auto
 qed
 
 lemma tan_eq_arctan_Ex:
   shows "tan x = y \<longleftrightarrow> (\<exists>k::int. x = arctan y + k*pi \<or> (x = pi/2 + k*pi \<and> y=0))"
 proof
   assume asm:"tan x = y"
   obtain k::int where k:"-pi/2 < x-k*pi" "x-k*pi \<le> pi/2"
   proof -
     define k where "k=ceiling (x/pi - 1/2)"
     have "(x/pi - 1/2)\<le>k" unfolding k_def by auto
     then have "x-k*pi \<le> pi/2" by (auto simp add:field_simps)
     moreover have "k-1 < x/pi - 1/2" unfolding k_def by linarith
     then have "-pi/2 < x-k*pi"  by (auto simp add:field_simps)
     ultimately show ?thesis using that by auto
   qed
   have "x = arctan y + of_int k * pi" when "x \<noteq> pi/2 + k*pi"
   proof -
     have "tan (x - k * pi) = y" using asm tan_periodic_int[of _ "-k"] by auto
     then have "arctan y = x - real_of_int k * pi"
-      apply (intro arctan_unique)
-      using k that by (auto simp add:field_simps)
+      using arctan_tan k that by force
     then show ?thesis by auto
   qed
   moreover have "y=0" when "x = pi/2 + k*pi"
     using asm that by auto (simp add: tan_def)
   ultimately show "\<exists>k. x = arctan y + of_int k * pi \<or> (x = pi/2 + k*pi \<and> y=0)"
     using k by auto
 next
   assume "\<exists>k::int. x = arctan y +  k * pi \<or> x = pi / 2 + k * pi \<and> y = 0"
   then show "tan x = y"
     by (metis arctan_unique cos_pi_half division_ring_divide_zero tan_def tan_periodic_int tan_total)
 qed
 
 lemma arccos_unique:
   assumes "0 \<le> x"
     and "x \<le> pi"
     and "cos x = y"
   shows "arccos y = x"
 using arccos_cos assms by blast
 
 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)"
 proof
   assume asm:"-1\<le>y \<and> y\<le>1 \<and> (\<exists>k::int. x = arccos y + 2*k*pi \<or> x = - arccos y + 2*k*pi)"
   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"
   proof -
     have "cos x = cos (arccos y + k*(2*pi))"
       using that by (auto simp add:algebra_simps)
     also have "... = cos (arccos y)"
       using cos.periodic_simps(3)[of "arccos y" k] by auto
     also have "... = y"
       using asm by auto
     finally show ?thesis .
   qed
   moreover have "cos x = y" when "x = -arccos y + 2*k*pi"
   proof -
     have "cos x = cos (- arccos y + k*2*pi)"
       unfolding that by (auto simp add:algebra_simps)
     also have "... = cos (arccos y - k*2*pi)"
       by (metis cos_minus minus_diff_eq uminus_add_conv_diff)
     also have "... = cos (arccos y)"
       using cos.periodic_simps(3)[of "arccos y" "-k"]
       by (auto simp add:algebra_simps)
     also have "... = y"
       using asm by auto
     finally show ?thesis .
   qed
   ultimately show "cos x = y" by auto
 next
   assume asm:"cos x =y"
   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"
   proof -
     define k where "k=ceiling (x/(2*pi) - 1/2)"
     have "(x/(2*pi) - 1/2)\<le>k" unfolding k_def by auto
     then have "x-k*2*pi \<le> pi" by (auto simp add:field_simps)
     moreover have "k-1 < x/(2*pi) - 1/2" unfolding k_def by linarith
     then have "-pi < x-k*2*pi"  by (auto simp add:field_simps)
     ultimately show ?thesis using that by auto
   qed
   have ?goal when "x-k*2*pi\<ge>0"
   proof -
     have "cos (x - k * 2*pi) = y"
       using cos.periodic_simps(3)[of x "-k"] asm by (auto simp add:field_simps)
     then have "arccos y = x - k * 2*pi"
       apply (intro arccos_unique)
       using k that by auto
     then show ?goal by auto
   qed
   moreover have ?goal when "\<not> x-k*2*pi \<ge>0"
   proof -
     have "cos (x - k * 2*pi) = y"
       using cos.periodic_simps(3)[of x "-k"] asm by (auto simp add:field_simps)
     then have "cos (k * 2*pi - x) = y"
       by (metis cos_minus minus_diff_eq)
     then have "arccos y = k * 2*pi - x"
       apply (intro arccos_unique)
       using k that by auto
     then show ?goal by auto
   qed
   ultimately have ?goal by auto
   moreover have "-1\<le>y \<and> y\<le>1" using asm by auto
   ultimately show "-1\<le>y \<and> y\<le>1 \<and> ?goal" by auto
 qed
 
 lemma uniform_discrete_tan_eq:
   "uniform_discrete {x::real. tan x = y}"
 proof -
   have "x1=x2" when dist:"dist x1 x2<pi/2" and "tan x1=y" "tan x2=y" for x1 x2
   proof -
     obtain k1::int where x1:"x1 = arctan y + k1*pi \<or> (x1 = pi/2 + k1*pi \<and> y=0)"
       using tan_eq_arctan_Ex \<open>tan x1=y\<close> by auto
     obtain k2::int where x2:"x2 = arctan y + k2*pi \<or> (x2 = pi/2 + k2*pi \<and> y=0)"
       using tan_eq_arctan_Ex \<open>tan x2=y\<close> by auto
     let ?xk1="x1 = arctan y + k1*pi" and ?xk1'="x1 = pi/2 + k1*pi \<and> y=0"
     let ?xk2="x2 = arctan y + k2*pi" and ?xk2'="x2 = pi/2 + k2*pi \<and> y=0"
     have ?thesis when "(?xk1 \<and> ?xk2) \<or> (?xk1' \<and> ?xk2')"
     proof -
       have "x1-x2= (k1 - k2) *pi" when ?xk1 ?xk2
         using arg_cong2[where f=minus,OF \<open>?xk1\<close> \<open>?xk2\<close>]
         by (auto simp add:algebra_simps)
       moreover have "x1-x2= (k1 - k2) *pi" when ?xk1' ?xk2'
         using arg_cong2[where f=minus,OF conjunct1[OF \<open>?xk1'\<close>] conjunct1[OF \<open>?xk2'\<close>]]
         by (auto simp add:algebra_simps)
       ultimately have "x1-x2= (k1 - k2) *pi" using that by auto
       then have "\<bar>k1 - k2\<bar> < 1/2"
         using dist[unfolded dist_real_def] by (auto simp add:abs_mult)
       then have "k1=k2" by linarith
       then show ?thesis using that by auto
     qed
     moreover have ?thesis when ?xk1 ?xk2'
     proof -
       have "x1 = k1*pi" "x2 = pi / 2 + k2 * pi" using \<open>?xk2'\<close> \<open>?xk1\<close> by auto
       from arg_cong2[where f=minus,OF this] have "x1 - x2 = (k1 - k2) * pi -pi/2"
         by (auto simp add:algebra_simps)
       then have "\<bar>(k1 - k2) * pi -pi/2\<bar> < pi/2" using dist[unfolded dist_real_def] by auto
       then have "0<k1-k2" "k1-k2<1"
         unfolding abs_less_iff  by (auto simp add: zero_less_mult_iff)
       then have False by simp
       then show ?thesis by auto
     qed
     moreover have ?thesis when ?xk1' ?xk2
     proof -
       have "x1 = pi / 2 + k1*pi" "x2 = k2 * pi" using \<open>?xk2\<close> \<open>?xk1'\<close> by auto
       from arg_cong2[where f=minus,OF this] have "x1 - x2 = (k1 - k2) * pi + pi/2"
         by (auto simp add:algebra_simps)
       then have "\<bar>(k1 - k2) * pi + pi/2\<bar> < pi/2" using dist[unfolded dist_real_def] by auto
       then have "\<bar>(k1 - k2 + 1/2)*pi\<bar> < pi/2" by (auto simp add:algebra_simps)
       then have "\<bar>(k1 - k2 + 1/2)\<bar> < 1/2" by (auto simp add:abs_mult)
       then have "-1<k1-k2 \<and> k1-k2<0"
         unfolding abs_less_iff by linarith
       then have False by auto
       then show ?thesis by auto
     qed
     ultimately show ?thesis using x1 x2 by blast
   qed
   then show ?thesis unfolding uniform_discrete_def
     apply (intro exI[where x="pi/2"])
     by auto
 qed
 
 lemma get_norm_value:
   fixes a::"'a::{floor_ceiling}"
   assumes "pp>0"
   obtains k::int and a1 where "a=(of_int k)*pp+a1" "a0\<le>a1" "a1<a0+pp"
 proof -
   define k where "k=floor ((a-a0)/pp)"
   define a1 where "a1=a-(of_int k)*pp"
   have "of_int \<lfloor>(a - a0) / pp\<rfloor> * pp \<le> a- a0" 
     using assms by (meson le_divide_eq of_int_floor_le)
   moreover have "a-a0 < of_int (\<lfloor>(a - a0) / pp\<rfloor>+1) * pp" 
     using assms by (meson divide_less_eq floor_correct)
   ultimately show ?thesis 
     apply (intro that[of k a1])
     unfolding k_def a1_def using assms by (auto simp add:algebra_simps)
 qed
 
 (*Is it possible to generalise or simplify this messy proof?*)
 lemma filtermap_tan_at_right:
   fixes a::real
   assumes "cos a\<noteq>0"
   shows "filtermap tan (at_right a) = at_right (tan a)"
 proof -
   obtain k::int and a1 where aa1:"a=k*pi+a1" and "-pi/2\<le>a1" "a1<pi/2"
     using get_norm_value[of pi a "-pi/2"] by auto
   have "-pi/2 < a1" 
   proof (rule ccontr)
     assume "\<not> - pi / 2 < a1"
     then have "a1=- pi / 2" using \<open>-pi/2\<le>a1\<close> by auto
     then have "cos a = 0" unfolding aa1
       by (metis (no_types, opaque_lifting) add.commute add_0_left cos_pi_half 
               diff_eq_eq mult.left_neutral mult_minus_right mult_zero_left 
               sin_add sin_pi_half sin_zero_iff_int2 times_divide_eq_left uminus_add_conv_diff)
     then show False using assms by auto
   qed
   have "eventually P (at_right (tan a))" 
     when "eventually P (filtermap tan (at_right a))" for P
   proof -
     obtain b1 where "b1>a" and b1_imp:" \<forall>y>a. y < b1 \<longrightarrow> P (tan y)"
       using \<open>eventually P (filtermap tan (at_right a))\<close>
       unfolding eventually_filtermap eventually_at_right 
       by (metis eventually_at_right_field)
     define b2 where "b2=min b1 (k*pi+pi/4+a1/2)"  
     define b3 where "b3=b2 - k*pi"
     have "-pi/2 < b3" "b3<pi/2" 
     proof -
       have "a1<b3"
         using \<open>b1>a\<close> aa1 \<open>a1<pi/2\<close> unfolding b2_def b3_def by (auto simp add:field_simps)
       then show "-pi/2 < b3" using \<open>-pi/2\<le>a1\<close> by auto
       show "b3 < pi/2"
         unfolding b2_def b3_def
         apply (subst min_diff_distrib_left)
         apply (rule min.strict_coboundedI2)
         using \<open>b1>a\<close> aa1 \<open>a1<pi/2\<close> \<open>-pi/2<a1\<close> by auto
     qed
     have "tan b2 > tan a" 
     proof -
       have "tan a = tan a1"
         using aa1 by (simp add: add.commute)
       also have "... < tan b3"
       proof -
         have "a1<b3"
           using \<open>b1>a\<close> aa1 \<open>a1<pi/2\<close> unfolding b2_def b3_def by (auto simp add:field_simps)
         then show ?thesis
           using tan_monotone \<open>-pi/2 < a1\<close> \<open>b3 < pi/2\<close> by simp
       qed
       also have "... = tan b2" unfolding b3_def
         by (metis Groups.mult_ac(2) add_uminus_conv_diff mult_minus_right of_int_minus 
           tan_periodic_int)
       finally show ?thesis .
     qed
     moreover have "P y" when "y>tan a" "y < tan b2" for y
     proof -
       define y1 where "y1=arctan y+ k * pi"
       have "a<y1" 
       proof -
         have "arctan (tan a) < arctan y" using \<open>y>tan a\<close> arctan_monotone by auto
         then have "a1<arctan y"
           using arctan_tan \<open>-pi/2 < a1\<close> \<open>a1<pi/2\<close> unfolding aa1 by (simp add: add.commute)
         then show ?thesis unfolding y1_def aa1 by auto
       qed
       moreover have "y1<b2"
       proof - 
         have "arctan y < arctan (tan b2)"
           using \<open>y < tan b2\<close> arctan_monotone by auto
         moreover have "arctan (tan b2) = b3"
           using arctan_tan[of b3] \<open>-pi/2 < b3\<close> \<open>b3<pi/2\<close> unfolding b3_def 
           by (metis add.inverse_inverse diff_minus_eq_add divide_minus_left mult.commute 
             mult_minus_right of_int_minus tan_periodic_int)
         ultimately have "arctan y < b3" by auto
         then show ?thesis unfolding y1_def b3_def by auto
       qed
       moreover have "\<forall>y>a. y < b2 \<longrightarrow> P (tan y)"
         using b1_imp unfolding b2_def by auto
       moreover have "tan y1=y" unfolding y1_def by (auto simp add:tan_arctan)
       ultimately show ?thesis by auto
     qed
     ultimately show "eventually P (at_right (tan a))" 
       unfolding eventually_at_right by (metis eventually_at_right_field)
   qed
   moreover have "eventually P (filtermap tan (at_right a))" 
     when "eventually P (at_right (tan a))" for P
   proof -
     obtain b1 where "b1>tan a" and b1_imp:"\<forall>y>tan a. y < b1 \<longrightarrow> P y" 
       using \<open>eventually P (at_right (tan a))\<close> unfolding eventually_at_right 
       by (metis eventually_at_right_field)
     define b2 where "b2=arctan b1 + k*pi" 
     have "a1 < arctan b1" 
       by (metis \<open>- pi / 2 < a1\<close> \<open>a1 < pi / 2\<close> \<open>tan a < b1\<close> aa1 add.commute arctan_less_iff 
             arctan_tan divide_minus_left tan_periodic_int)
     then have "b2>a" unfolding aa1 b2_def by auto
     moreover have "P (tan y)" when "y>a" "y < b2" for y
     proof -
       define y1 where "y1 = y - k*pi"
       have "a1 < y1" "y1 < arctan b1" unfolding y1_def
         subgoal using \<open>y>a\<close> unfolding aa1 by auto
         subgoal using b2_def that(2) by linarith
         done
       then have "tan a1 < tan y1" "tan y1< b1"
         subgoal using \<open>a1>-pi/2\<close>
           apply (intro tan_monotone,simp,simp)
           using arctan_ubound less_trans by blast
         subgoal 
           by (metis \<open>- pi / 2 < a1\<close> \<open>a1 < y1\<close> \<open>y1 < arctan b1\<close> arctan_less_iff arctan_tan 
               arctan_ubound divide_minus_left less_trans)
         done
       have "tan y>tan a" 
         by (metis \<open>tan a1 < tan y1\<close> aa1 add.commute add_uminus_conv_diff mult.commute 
             mult_minus_right of_int_minus tan_periodic_int y1_def)
       moreover have "tan y<b1" 
         by (metis \<open>tan y1 < b1\<close> add_uminus_conv_diff mult.commute mult_minus_right 
             of_int_minus tan_periodic_int y1_def)
       ultimately show ?thesis using b1_imp by auto
     qed
     ultimately show ?thesis unfolding eventually_filtermap eventually_at_right 
       by (metis eventually_at_right_field)
   qed
   ultimately show ?thesis unfolding filter_eq_iff by blast
 qed
 
 lemma filtermap_tan_at_left:
   fixes a::real
   assumes "cos a\<noteq>0"
   shows "filtermap tan (at_left a) = at_left (tan a)"
 proof -
   have "filtermap tan (at_right (- a)) = at_right (tan (- a))" 
     using filtermap_tan_at_right[of "-a"] assms by auto
   then have "filtermap (uminus o tan) (at_left a) = filtermap uminus (at_left (tan a))"
     unfolding at_right_minus filtermap_filtermap comp_def by auto
   then have "filtermap uminus (filtermap (uminus o tan) (at_left a)) 
       = filtermap uminus (filtermap uminus (at_left (tan a)))"
     by auto
   then show ?thesis 
     unfolding filtermap_filtermap comp_def by auto
 qed
 
 lemma cos_zero_iff_int2:
   fixes x::real
   shows "cos x = 0 \<longleftrightarrow> (\<exists>n::int. x = n * pi +  pi/2)"
   using sin_zero_iff_int2[of "x-pi/2"] unfolding sin_cos_eq 
   by (auto simp add:algebra_simps)
 
 lemma filtermap_tan_at_right_inf:
   fixes a::real
   assumes "cos a=0"
   shows "filtermap tan (at_right a) = at_bot"
 proof -
   obtain k::int where ak:"a=k*pi + pi/2"
     using cos_zero_iff_int2 assms by auto
   have "eventually P at_bot" when "eventually P (filtermap tan (at_right a))" for P 
   proof -
     obtain b1 where "b1>a" and b1_imp:"\<forall>y>a. y < b1 \<longrightarrow> P (tan y)" 
       using \<open>eventually P (filtermap tan (at_right a))\<close> 
       unfolding eventually_filtermap eventually_at_right 
       by (metis eventually_at_right_field)
     define b2 where "b2=min (k*pi+pi) b1"
     have "P y" when "y<tan b2" for y
     proof -
       define y1 where "y1=(k+1)*pi+arctan y"
       have "a < y1" 
         unfolding ak y1_def using arctan_lbound[of y]
         by (auto simp add:field_simps)
       moreover have "y1 < b2" 
       proof -
         define b3 where "b3=b2-(k+1) * pi"
         have "-pi/2 < b3" "b3<pi/2"
           using \<open>b1>a\<close> unfolding b3_def b2_def ak 
           by (auto simp add:field_simps min_mult_distrib_left intro!:min.strict_coboundedI1)
         then have "arctan (tan b3) = b3"
           by (simp add: arctan_tan)
         then have "arctan (tan b2) = b3" 
           unfolding b3_def by (metis diff_eq_eq tan_periodic_int)
         then have "arctan y < b3"
           using arctan_monotone[OF \<open>y<tan b2\<close>] by simp
         then show ?thesis
           unfolding y1_def b3_def by auto
       qed
       then have "y1<b1" unfolding b2_def by auto
       ultimately have " P (tan y1)" using b1_imp[rule_format,of y1,simplified] by auto
       then show ?thesis unfolding y1_def by (metis add.commute arctan tan_periodic_int)
     qed
     then show ?thesis unfolding eventually_at_bot_dense by auto
   qed
   moreover have "eventually P (filtermap tan (at_right a))" when "eventually P at_bot" for P 
   proof -
     obtain b1 where b1_imp:"\<forall>n<b1. P n"
       using \<open>eventually P at_bot\<close> unfolding eventually_at_bot_dense by auto
     define b2 where "b2=arctan b1 + (k+1)*pi"
     have "b2>a" unfolding ak b2_def using arctan_lbound[of b1]
       by (auto simp add:algebra_simps)
     moreover have "P (tan y)" when "a < y" " y < b2 " for y
     proof -
       define y1 where "y1=y-(k+1)*pi"
       have "tan y1 < tan (arctan b1)"
         apply (rule tan_monotone)
         subgoal using \<open>a<y\<close> unfolding y1_def ak by (auto simp add:algebra_simps)
         subgoal using \<open>y < b2\<close> unfolding y1_def b2_def by (auto simp add:algebra_simps)
         subgoal using arctan_ubound by auto
         done
       then have "tan y1<b1" by (simp add: arctan)
       then have "tan y < b1" unfolding y1_def 
         by (metis diff_eq_eq tan_periodic_int)
       then show ?thesis using b1_imp by auto
     qed
     ultimately show "eventually P (filtermap tan (at_right a))"
       unfolding eventually_filtermap eventually_at_right 
       by (metis eventually_at_right_field)
   qed
   ultimately show ?thesis unfolding filter_eq_iff by auto
 qed
 
 lemma filtermap_tan_at_left_inf:
   fixes a::real
   assumes "cos a=0"
   shows "filtermap tan (at_left a) = at_top"
 proof -
   have "filtermap tan (at_right (- a)) = at_bot"
     using filtermap_tan_at_right_inf[of "-a"] assms by auto
   then have "filtermap (uminus o tan) (at_left a) = at_bot"
     unfolding at_right_minus filtermap_filtermap comp_def by auto
   then have "filtermap uminus (filtermap (uminus o tan) (at_left a)) = filtermap uminus at_bot"
     by auto
   then show ?thesis 
     unfolding filtermap_filtermap comp_def using at_top_mirror[where 'a=real] by auto
 qed
 
 subsection \<open>Periodic set\<close>
 
 (*Devised to characterize roots of Trigonometric equations, which are usually uniformly discrete.*)
 definition periodic_set:: "real set \<Rightarrow> real \<Rightarrow> bool" where
   "periodic_set S \<delta> \<longleftrightarrow> (\<exists>B. finite B \<and> (\<forall>x\<in>S. \<exists>b\<in>B. \<exists>k::int. x =b + k * \<delta> ))"
 
 lemma periodic_set_multiple:
   assumes "k\<noteq>0"
   shows "periodic_set S \<delta> \<longleftrightarrow> periodic_set S (of_int k*\<delta>)"
 proof
   assume asm:"periodic_set S \<delta> "
   then obtain B1 where "finite B1" and B1_def:"\<forall>x\<in>S. \<exists>b\<in>B1. (\<exists>k::int. x = b + k * \<delta>)"
     unfolding periodic_set_def by metis
   define B where "B = B1 \<union> {b+i*\<delta> | b i. b\<in>B1 \<and> i\<in>{0..<\<bar>k\<bar>}}"
   have "\<exists>b\<in>B. \<exists>k'. x = b + real_of_int k' * (real_of_int k * \<delta>)" when "x\<in>S" for x
   proof -
     obtain b1 and k1::int where "b1\<in>B1" and x_\<delta>:"x = b1 + k1 * \<delta>"
       using B1_def[rule_format, OF \<open>x\<in>S\<close>] by auto
     define r d where "r= k1 mod \<bar>k\<bar>" and "d = k1 div \<bar>k\<bar>"
     define b kk where "b=b1+r*\<delta>" and "kk = (if k>0 then d else -d)"
     have "x = b1 + (r+\<bar>k\<bar>*d)*\<delta>" using x_\<delta> unfolding r_def d_def by auto
     then have "x = b + kk*(k*\<delta>)" unfolding b_def kk_def using \<open>k\<noteq>0\<close>
       by (auto simp add:algebra_simps)
     moreover have "b\<in>B"
     proof -
       have "r \<in> {0..<\<bar>k\<bar>}" unfolding r_def by (simp add: \<open>k\<noteq>0\<close>)
       then show ?thesis unfolding b_def B_def using \<open>b1\<in>B1\<close> by blast
     qed
     ultimately show ?thesis by auto
   qed
   moreover have "finite B" unfolding B_def using \<open>finite B1\<close>
     by (simp add: finite_image_set2)
   ultimately show "periodic_set S (real_of_int k * \<delta>)" unfolding periodic_set_def by auto
 next
   assume "periodic_set S (real_of_int k * \<delta>)"
   then show "periodic_set S \<delta>" unfolding periodic_set_def
     by (metis mult.commute mult.left_commute of_int_mult)
 qed
 
 lemma periodic_set_empty[simp]: "periodic_set {} \<delta>"
   unfolding periodic_set_def by auto
 
 lemma periodic_set_finite:
   assumes "finite S"
   shows "periodic_set S \<delta>"
 unfolding periodic_set_def using assms mult.commute by force
 
 lemma periodic_set_subset[elim]:
   assumes "periodic_set S \<delta>" "T \<subseteq> S"
   shows "periodic_set T \<delta>"
 using assms unfolding periodic_set_def by (meson subsetCE)
 
 lemma periodic_set_union:
   assumes "periodic_set S \<delta>" "periodic_set T \<delta>"
   shows "periodic_set (S \<union> T) \<delta>"
 using assms unfolding periodic_set_def by (metis Un_iff infinite_Un)
 
 lemma periodic_imp_uniform_discrete:
   assumes "periodic_set S \<delta>"
   shows "uniform_discrete S"
 proof -
   have ?thesis when "S\<noteq>{}" "\<delta>\<noteq>0"
   proof -
     obtain B g where "finite B" and g_def:"\<forall>x\<in>S. g x\<in>B \<and> (\<exists>k::int. x = g x + k * \<delta>)"
       using assms unfolding periodic_set_def by metis
     define P where "P = ((*) \<delta>) ` Ints"
     define B_diff where "B_diff = {\<bar>x-y\<bar> | x y.  x\<in>B \<and> y\<in>B} - P"
     have "finite B_diff" unfolding B_diff_def using \<open>finite B\<close>
       by (simp add: finite_image_set2)
     define e where "e = (if setdist B_diff P = 0 then \<bar>\<delta>\<bar> else min (setdist B_diff P) (\<bar>\<delta>\<bar>))"
     have "e>0"
       unfolding e_def using setdist_pos_le[unfolded order_class.le_less] \<open>\<delta>\<noteq>0\<close>
       by auto
     moreover have "x=y" when "x\<in>S" "y\<in>S" "dist x y<e" for x y
     proof -
       obtain k1::int where k1:"x = g x + k1 * \<delta>" and "g x\<in>B" using g_def \<open>x\<in>S\<close> by auto
       obtain k2::int where k2:"y = g y + k2 * \<delta>" and "g y\<in>B" using g_def \<open>y\<in>S\<close> by auto
       have ?thesis when "\<bar>g x - g y\<bar> \<in> P"
       proof -
         obtain k::int where k:"g x - g y = k * \<delta>"
         proof -
           obtain k' where "k'\<in>Ints" and *:"\<bar>g x - g y\<bar> = \<delta> * k'"
             using \<open>\<bar>g x - g y\<bar> \<in> P\<close> unfolding P_def image_iff by auto
           then obtain k where **:"k' = of_int k" using Ints_cases by auto
           show ?thesis
             apply (cases "g x - g y \<ge> 0")
             subgoal using that[of k] * ** by simp
             subgoal using that[of "-k"] * ** by (auto simp add:algebra_simps)
             done
         qed
         have "dist x y = \<bar>(g x - g y)+(k1-k2)*\<delta>\<bar>"
           unfolding dist_real_def by (subst k1,subst k2,simp add:algebra_simps)
         also have "... = \<bar>(k+k1-k2)*\<delta>\<bar>"
           by (subst k,simp add:algebra_simps)
         also have "... = \<bar>k+k1-k2\<bar>*\<bar>\<delta>\<bar>" by (simp add: abs_mult)
         finally have *:"dist x y = \<bar>k+k1-k2\<bar>*\<bar>\<delta>\<bar>" .
         then have "\<bar>k+k1-k2\<bar>*\<bar>\<delta>\<bar> < e" using \<open>dist x y<e\<close> by auto
         then have "\<bar>k+k1-k2\<bar>*\<bar>\<delta>\<bar> < \<bar>\<delta>\<bar>"
           by (simp add: e_def split: if_splits)
         then have "\<bar>k+k1-k2\<bar> = 0" unfolding e_def using \<open>\<delta>\<noteq>0\<close> by force
         then have "dist x y=0" using * by auto
         then show ?thesis by auto
       qed
       moreover have ?thesis when "\<bar>g x - g y\<bar> \<notin> P"
       proof -
         have "\<bar>g x - g y\<bar> \<in> B_diff" unfolding B_diff_def using \<open>g x\<in>B\<close> \<open>g y\<in>B\<close> that by auto
         have "e \<le> \<bar>\<bar>g x - g y\<bar> - \<bar>(k1-k2)*\<delta>\<bar>\<bar>"
         proof -
           have "\<bar>g x - g y\<bar> \<in> B_diff" unfolding B_diff_def using \<open>g x\<in>B\<close> \<open>g y\<in>B\<close> that by auto
           moreover have "\<bar>(k1-k2)*\<delta>\<bar> \<in> P" unfolding P_def
             apply (intro rev_image_eqI[of "(if \<delta>\<ge>0 then \<bar>of_int(k1-k2)\<bar> else - \<bar>of_int(k1-k2)\<bar>)"])
             apply (metis Ints_minus Ints_of_int of_int_abs)
             by (auto simp add:abs_mult)
           ultimately have "\<bar>\<bar>g x - g y\<bar> - \<bar>(k1-k2)*\<delta>\<bar>\<bar> \<ge> setdist B_diff P"
             using setdist_le_dist[of _ B_diff  _ P] dist_real_def by auto
           moreover have "setdist B_diff P \<noteq> 0"
           proof -
             have "compact B_diff " using  \<open>finite B_diff\<close> using finite_imp_compact by blast
             moreover have "closed P"
               unfolding P_def using closed_scaling[OF closed_Ints[where 'a=real], of \<delta>] by auto
             moreover have "P \<noteq> {}" using Ints_0 unfolding P_def by blast
             moreover have "B_diff \<inter> P = {}" unfolding B_diff_def by auto
             moreover have "B_diff \<noteq>{}" unfolding B_diff_def using \<open>g x\<in>B\<close> \<open>g y\<in>B\<close> that by auto
             ultimately show ?thesis using setdist_eq_0_compact_closed[of B_diff P] by auto
           qed
           ultimately show ?thesis unfolding e_def by argo
         qed
         also have "... \<le> \<bar>(g x - g y) + (k1-k2)*\<delta>\<bar>"
         proof -
           define t1 where "t1=g x - g y"
           define t2 where "t2 = of_int (k1 - k2) * \<delta>"
           show ?thesis
             apply (fold t1_def t2_def)
             by linarith
         qed
         also have "... = dist x y"
           unfolding dist_real_def
           by (subst (2) k1,subst (2) k2,simp add:algebra_simps)
         finally have "dist x y\<ge>e" .
         then have False using \<open>dist x y<e\<close> by auto
         then show ?thesis by auto
       qed
       ultimately show ?thesis by auto
     qed
     ultimately show ?thesis unfolding uniform_discrete_def by auto
   qed
   moreover have ?thesis when "S={}" using that by auto
   moreover have ?thesis when "\<delta>=0"
   proof -
     obtain B g where "finite B" and g_def:"\<forall>x\<in>S. g x\<in>B \<and> (\<exists>k::int. x = g x + k * \<delta>)"
       using assms unfolding periodic_set_def by metis
     then have "\<forall>x\<in>S. g x\<in>B \<and> (x = g x)" using that by fastforce
     then have "S \<subseteq> g ` B" by auto
     then have "finite S" using \<open>finite B\<close> by (auto elim:finite_subset)
     then show ?thesis using uniform_discrete_finite_iff by blast
   qed
   ultimately show ?thesis by blast
 qed
 
 lemma periodic_set_tan_linear:
   assumes "a\<noteq>0" "c\<noteq>0"
   shows "periodic_set (roots (\<lambda>x. a*tan (x/c) + b)) (c*pi)"
 proof -
   define B where "B = { c*arctan (- b / a), c*pi/2}"
   have "\<exists>b\<in>B. \<exists>k::int. x = b + k * (c*pi)" when "x\<in>roots (\<lambda>x. a * tan (x/c) + b)" for x
   proof -
     define C1 where "C1 = (\<exists>k::int. x = c*arctan (- b / a) + k * (c*pi))"
     define C2 where "C2 = (\<exists>k::int. x = c*pi / 2 + k  * (c*pi) \<and> - b / a = 0)"
     have "tan (x/c) = - b/a" using that \<open>a\<noteq>0\<close> unfolding roots_within_def
       by (auto simp add:field_simps)
     then have "C1 \<or> C2" unfolding C1_def C2_def using tan_eq_arctan_Ex[of "x/c" "-b/a"]  \<open>c\<noteq>0\<close>
       by (auto simp add:field_simps)
     moreover have ?thesis when C1 using that unfolding C1_def B_def by blast
     moreover have ?thesis when C2 using that unfolding C2_def B_def by blast
     ultimately show ?thesis by auto
   qed
   moreover have "finite B" unfolding B_def by auto
   ultimately show ?thesis unfolding periodic_set_def by auto
 qed
 
 lemma periodic_set_cos_linear:
   assumes "a\<noteq>0" "c\<noteq>0"
   shows "periodic_set (roots (\<lambda>x. a*cos (x/c) + b)) (2*c*pi)"
 proof -
   define B where "B = { c*arccos (- b / a), - c*arccos (- b / a)}"
   have "\<exists>b\<in>B. \<exists>k::int. x = b + k * (2*c*pi)"
     when "x\<in>roots (\<lambda>x. a * cos (x/c) + b)" for x
   proof -
     define C1 where "C1 = (\<exists>k::int. x = c*arccos (- b / a) + k * (2*c*pi))"
     define C2 where "C2 = (\<exists>k::int. x = - c*arccos (- b / a) + k * (2*c*pi))"
     have "cos (x/c) = - b/a" using that \<open>a\<noteq>0\<close> unfolding roots_within_def
       by (auto simp add:field_simps)
     then have "C1 \<or> C2"
       unfolding cos_eq_arccos_Ex ex_disj_distrib C1_def C2_def using \<open>c\<noteq>0\<close>
       apply (auto simp add:divide_simps)
       by (auto simp add:algebra_simps)
     moreover have ?thesis when C1 using that unfolding C1_def B_def by blast
     moreover have ?thesis when C2 using that unfolding C2_def B_def by blast
     ultimately show ?thesis by auto
   qed
   moreover have "finite B" unfolding B_def by auto
   ultimately show ?thesis unfolding periodic_set_def by auto
 qed
 
 lemma periodic_set_tan_poly:
   assumes "p\<noteq>0" "c\<noteq>0"
   shows "periodic_set (roots (\<lambda>x. poly p (tan (x/c)))) (c*pi)"
   using assms
 proof (induct rule:poly_root_induct_alt)
   case 0
   then show ?case by simp
 next
   case (no_proots p)
   then show ?case unfolding roots_within_def by simp
 next
   case (root a p)
   have "roots (\<lambda>x. poly ([:- a, 1:] * p) (tan (x/c))) = roots (\<lambda>x. tan (x/c) - a)
           \<union> roots (\<lambda>x. poly p (tan (x/c)))"
     unfolding roots_within_def by auto
   moreover have "periodic_set (roots (\<lambda>x. tan (x/c) - a)) (c*pi)"
     using periodic_set_tan_linear[OF _ \<open>c\<noteq>0\<close> ,of 1 "-a",simplified] .
   moreover have "periodic_set (roots (\<lambda>x. poly p (tan (x/c)))) (c*pi)" using root by fastforce
   ultimately show ?case using periodic_set_union by simp
 qed
 
 lemma periodic_set_sin_cos_linear:
   fixes a b c ::real
   assumes "a\<noteq>0 \<or> b\<noteq>0 \<or> c\<noteq>0"
   shows "periodic_set (roots (\<lambda>x. a * cos x + b * sin x + c)) (4*pi)"
 proof -
   define f where "f x= a * cos x + b * sin x + c" for x
   have "roots f = (roots f \<inter> {x. cos (x/2) = 0}) \<union> (roots f \<inter> {x. cos (x/2) \<noteq> 0})"
     by auto
   moreover have "periodic_set (roots f \<inter> {x. cos (x/2) = 0}) (4*pi)"
   proof -
     have "periodic_set ({x. cos (x/2) = 0}) (4*pi)"
       using periodic_set_cos_linear[of 1 2 0,unfolded roots_within_def,simplified] by simp
     then show ?thesis by auto
   qed
   moreover have "periodic_set (roots f \<inter> {x. cos (x/2) \<noteq> 0}) (4*pi)"
   proof -
     define p where "p=[:a+c,2*b,c-a:]"
     have "poly p (tan (x/2)) = 0 \<longleftrightarrow> f x=0" when "cos (x/2) \<noteq>0" for x
     proof -
       define t where "t=tan (x/2)"
       define tt where "tt = 1+t^2"
       have "cos x = (1-t^2) / tt" unfolding tt_def t_def
         using cos_tan_half[OF that,simplified] by simp
       moreover have "sin x = 2*t / tt" unfolding tt_def t_def
         using sin_tan_half[of "x/2",simplified] by simp
       moreover have "tt\<noteq>0" unfolding tt_def
         by (metis power_one sum_power2_eq_zero_iff zero_neq_one)
       ultimately show ?thesis
         unfolding f_def p_def
         apply (fold t_def)
         apply simp
         apply (auto simp add:field_simps)
         by (auto simp add:algebra_simps tt_def power2_eq_square)
     qed
     then have "roots f \<inter> {x. cos (x/2) \<noteq> 0} = roots (\<lambda>x. poly p (tan (x/2))) \<inter> {x. cos (x/2) \<noteq> 0}"
       unfolding roots_within_def by auto
     moreover have "periodic_set (roots (\<lambda>x. poly p (tan (x/2))) \<inter> {x. cos (x/2) \<noteq> 0}) (4*pi)"
     proof -
       have "p\<noteq>0" unfolding p_def using assms by auto
       then have "periodic_set (roots (\<lambda>x. poly p (tan (x/2)))) (4*pi)"
         using periodic_set_tan_poly[of p 2,simplified]
           periodic_set_multiple[of 2 _ "2*pi",simplified]
         by auto
       then show ?thesis by auto
     qed
     ultimately show ?thesis by auto
   qed
   ultimately show "periodic_set (roots f) (4*pi)" using periodic_set_union by metis
 qed
 
 end