Theory Winding_Number_Eval.Missing_Transcendental

(*
    Author:     Wenda Li <wl302@cam.ac.uk / liwenda1990@hotmail.com>
*)

section ‹Some useful lemmas about transcendental functions›

theory Missing_Transcendental imports
  Missing_Topology
  Missing_Algebraic
begin

subsection ‹Misc›

lemma exp_Arg2pi2pi_multivalue:
  assumes "exp (𝗂 * of_real x) = z"
  shows "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) 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'0" and "x'<2*pi" by (auto simp add:field_simps)
  moreover have "exp (𝗂 * 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 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  (x1 = pi/2 + k1*pi  y=0)"
      using tan_eq_arctan_Ex tan x1=y by auto
    obtain k2::int where x2:"x2 = arctan y + k2*pi  (x2 = pi/2 + k2*pi  y=0)"
      using tan_eq_arctan_Ex tan x2=y by auto
    let ?xk1="x1 = arctan y + k1*pi" and ?xk1'="x1 = pi/2 + k1*pi  y=0"
    let ?xk2="x2 = arctan y + k2*pi" and ?xk2'="x2 = pi/2 + k2*pi  y=0"
    have ?thesis when "(?xk1  ?xk2)  (?xk1'  ?xk2')"
    proof -
      have "x1-x2= (k1 - k2) *pi" when ?xk1 ?xk2
        using arg_cong2[where f=minus,OF ?xk1 ?xk2]
        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 ?xk1'] conjunct1[OF ?xk2']]
        by (auto simp add:algebra_simps)
      ultimately have "x1-x2= (k1 - k2) *pi" using that by auto
      then have "¦k1 - k2¦ < 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 ?xk2' ?xk1 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 "¦(k1 - k2) * pi -pi/2¦ < 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 ?xk2 ?xk1' 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 "¦(k1 - k2) * pi + pi/2¦ < pi/2" using dist[unfolded dist_real_def] by auto
      then have "¦(k1 - k2 + 1/2)*pi¦ < pi/2" by (auto simp add:algebra_simps)
      then have "¦(k1 - k2 + 1/2)¦ < 1/2" by (auto simp add:abs_mult)
      then have "-1<k1-k2  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" "a0a1" "a1<a0+pp"
proof -
  define k where "k=floor ((a-a0)/pp)"
  define a1 where "a1=a-(of_int k)*pp"
  have "of_int (a - a0) / pp * pp  a- a0" 
    using assms by (meson le_divide_eq of_int_floor_le)
  moreover have "a-a0 < of_int ((a - a0) / pp+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 a0"
  shows "filtermap tan (at_right a) = at_right (tan a)"
proof -
  obtain k::int and a1 where aa1:"a=k*pi+a1" and pi_a1: "-pi/2a1" "a1<pi/2"
    using get_norm_value[of pi a "-pi/2"] by auto
  have "-pi/2 < a1" 
  using assms
    by (smt (verit, ccfv_SIG) pi_a1 aa1 cos_2pi_minus cos_diff cos_pi_half cos_two_pi divide_minus_left mult_of_int_commute sin_add sin_npi_int sin_pi_half sin_two_pi)
  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:" y>a. y < b1  P (tan y)"
      by (metis Sturm_Tarski.eventually_at_right eventually P (filtermap tan (at_right a)) eventually_filtermap)
    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 b1>a aa1 a1<pi/2 unfolding b2_def b3_def by (auto simp add:field_simps)
      then show "-pi/2 < b3" using -pi/2a1 by auto
      show "b3 < pi/2"
        using b2_def b3_def pi_a1(2) by linarith
    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 b1>a aa1 a1<pi/2 unfolding b2_def b3_def by (auto simp add:field_simps)
        then show ?thesis
          using tan_monotone -pi/2 < a1 b3 < pi/2 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 y>tan a arctan_monotone by auto
        then have "a1<arctan y"
          using arctan_tan -pi/2 < a1 a1<pi/2 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 y < tan b2 arctan_monotone by auto
        moreover have "arctan (tan b2) = b3"
          using arctan_tan[of b3] -pi/2 < b3 b3<pi/2 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 "y>a. y < b2  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:"y>tan a. y < b1  P y" 
      using eventually P (at_right (tan a)) unfolding eventually_at_right 
      by (metis eventually_at_right_field)
    define b2 where "b2=arctan b1 + k*pi" 
    have "a1 < arctan b1" 
      by (metis - pi / 2 < a1 a1 < pi / 2 tan a < b1 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 y>a unfolding aa1 by auto
        subgoal using b2_def that(2) by linarith
        done
      then have "tan a1 < tan y1" "tan y1< b1"
        subgoal using a1>-pi/2
          apply (intro tan_monotone,simp,simp)
          using arctan_ubound less_trans by blast
        subgoal 
          by (metis - pi / 2 < a1 a1 < y1 y1 < arctan b1 arctan_less_iff arctan_tan 
              arctan_ubound divide_minus_left less_trans)
        done
      have "tan y>tan a" 
        by (metis tan a1 < tan y1 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 tan y1 < b1 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 a0"
  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 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:"y>a. y < b1  P (tan y)" 
      using eventually P (filtermap tan (at_right a)) 
      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 b1>a 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 y<tan b2] 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:"n<b1. P n"
      using eventually P at_bot 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 a<y unfolding y1_def ak by (auto simp add:algebra_simps)
        subgoal using y < b2 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 ‹Periodic set›

(*Devised to characterize roots of Trigonometric equations, which are usually uniformly discrete.*)
definition periodic_set:: "real set  real  bool" where
  "periodic_set S δ  (B. finite B  (xS. bB. k::int. x =b + k * δ ))"

lemma periodic_set_multiple:
  assumes "k0"
  shows "periodic_set S δ  periodic_set S (of_int k*δ)"
proof
  assume asm:"periodic_set S δ "
  then obtain B1 where "finite B1" and B1_def:"xS. bB1. (k::int. x = b + k * δ)"
    unfolding periodic_set_def by metis
  define B where "B = B1  {b+i*δ | b i. bB1  i{0..<¦k¦}}"
  have "bB. k'. x = b + real_of_int k' * (real_of_int k * δ)" when "xS" for x
  proof -
    obtain b1 and k1::int where "b1B1" and x_δ:"x = b1 + k1 * δ"
      using B1_def[rule_format, OF xS] by auto
    define r d where "r= k1 mod ¦k¦" and "d = k1 div ¦k¦"
    define b kk where "b=b1+r*δ" and "kk = (if k>0 then d else -d)"
    have "x = b1 + (r+¦k¦*d)*δ" using x_δ unfolding r_def d_def by auto
    then have "x = b + kk*(k*δ)" unfolding b_def kk_def using k0
      by (auto simp add:algebra_simps)
    moreover have "bB"
    proof -
      have "r  {0..<¦k¦}" unfolding r_def by (simp add: k0)
      then show ?thesis unfolding b_def B_def using b1B1 by blast
    qed
    ultimately show ?thesis by auto
  qed
  moreover have "finite B" unfolding B_def using finite B1
    by (simp add: finite_image_set2)
  ultimately show "periodic_set S (real_of_int k * δ)" unfolding periodic_set_def by auto
next
  assume "periodic_set S (real_of_int k * δ)"
  then show "periodic_set S δ" unfolding periodic_set_def
    by (metis mult.commute mult.left_commute of_int_mult)
qed

lemma periodic_set_empty[simp]: "periodic_set {} δ"
  unfolding periodic_set_def by auto

lemma periodic_set_finite:
  assumes "finite S"
  shows "periodic_set S δ"
unfolding periodic_set_def using assms mult.commute by force

lemma periodic_set_subset[elim]:
  assumes "periodic_set S δ" "T  S"
  shows "periodic_set T δ"
using assms unfolding periodic_set_def by (meson subsetCE)

lemma periodic_set_union:
  assumes "periodic_set S δ" "periodic_set T δ"
  shows "periodic_set (S  T) δ"
using assms unfolding periodic_set_def by (metis Un_iff infinite_Un)

lemma periodic_imp_uniform_discrete:
  assumes "periodic_set S δ"
  shows "uniform_discrete S"
proof -
  have ?thesis when "S{}" "δ0"
  proof -
    obtain B g where "finite B" and g_def:"xS. g xB  (k::int. x = g x + k * δ)"
      using assms unfolding periodic_set_def by metis
    define P where "P = ((*) δ) ` Ints"
    define B_diff where "B_diff = {¦x-y¦ | x y.  xB  yB} - P"
    have "finite B_diff" unfolding B_diff_def using finite B
      by (simp add: finite_image_set2)
    define e where "e = (if setdist B_diff P = 0 then ¦δ¦ else min (setdist B_diff P) (¦δ¦))"
    have "e>0"
      unfolding e_def using setdist_pos_le[unfolded order_class.le_less] δ0
      by auto
    moreover have "x=y" when "xS" "yS" "dist x y<e" for x y
    proof -
      obtain k1::int where k1:"x = g x + k1 * δ" and "g xB" using g_def xS by auto
      obtain k2::int where k2:"y = g y + k2 * δ" and "g yB" using g_def yS by auto
      have ?thesis when "¦g x - g y¦  P"
      proof -
        obtain k::int where k:"g x - g y = k * δ"
        proof -
          obtain k' where "k'Ints" and *:"¦g x - g y¦ = δ * k'"
            using ¦g x - g y¦  P 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  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 = ¦(g x - g y)+(k1-k2)*δ¦"
          unfolding dist_real_def by (subst k1,subst k2,simp add:algebra_simps)
        also have "... = ¦(k+k1-k2)*δ¦"
          by (subst k,simp add:algebra_simps)
        also have "... = ¦k+k1-k2¦*¦δ¦" by (simp add: abs_mult)
        finally have *:"dist x y = ¦k+k1-k2¦*¦δ¦" .
        then have "¦k+k1-k2¦*¦δ¦ < e" using dist x y<e by auto
        then have "¦k+k1-k2¦*¦δ¦ < ¦δ¦"
          by (simp add: e_def split: if_splits)
        then have "¦k+k1-k2¦ = 0" unfolding e_def using δ0 by force
        then have "dist x y=0" using * by auto
        then show ?thesis by auto
      qed
      moreover have ?thesis when "¦g x - g y¦  P"
      proof -
        have "¦g x - g y¦  B_diff" unfolding B_diff_def using g xB g yB that by auto
        have "e  ¦¦g x - g y¦ - ¦(k1-k2)*䦦"
        proof -
          have "¦g x - g y¦  B_diff" unfolding B_diff_def using g xB g yB that by auto
          moreover have "¦(k1-k2)*δ¦  P" unfolding P_def
            apply (intro rev_image_eqI[of "(if δ0 then ¦of_int(k1-k2)¦ else - ¦of_int(k1-k2)¦)"])
            apply (metis Ints_minus Ints_of_int of_int_abs)
            by (auto simp add:abs_mult)
          ultimately have "¦¦g x - g y¦ - ¦(k1-k2)*䦦  setdist B_diff P"
            using setdist_le_dist[of _ B_diff  _ P] dist_real_def by auto
          moreover have "setdist B_diff P  0"
          proof -
            have "compact B_diff " using  finite B_diff using finite_imp_compact by blast
            moreover have "closed P"
              unfolding P_def using closed_scaling[OF closed_Ints[where 'a=real], of δ] by auto
            moreover have "P  {}" using Ints_0 unfolding P_def by blast
            moreover have "B_diff  P = {}" unfolding B_diff_def by auto
            moreover have "B_diff {}" unfolding B_diff_def using g xB g yB 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 "...  ¦(g x - g y) + (k1-k2)*δ¦"
        proof -
          define t1 where "t1=g x - g y"
          define t2 where "t2 = of_int (k1 - k2) * δ"
          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 ye" .
        then have False using dist x y<e 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 "δ=0"
  proof -
    obtain B g where "finite B" and g_def:"xS. g xB  (k::int. x = g x + k * δ)"
      using assms unfolding periodic_set_def by metis
    then have "xS. g xB  (x = g x)" using that by fastforce
    then have "S  g ` B" by auto
    then have "finite S" using finite B 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 "a0" "c0"
  shows "periodic_set (roots (λx. a*tan (x/c) + b)) (c*pi)"
proof -
  define B where "B = { c*arctan (- b / a), c*pi/2}"
  have "bB. k::int. x = b + k * (c*pi)" when "xroots (λx. a * tan (x/c) + b)" for x
  proof -
    define C1 where "C1 = (k::int. x = c*arctan (- b / a) + k * (c*pi))"
    define C2 where "C2 = (k::int. x = c*pi / 2 + k  * (c*pi)  - b / a = 0)"
    have "tan (x/c) = - b/a" using that a0 unfolding roots_within_def
      by (auto simp add:field_simps)
    then have "C1  C2" unfolding C1_def C2_def using tan_eq_arctan_Ex[of "x/c" "-b/a"]  c0
      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 "a0" "c0"
  shows "periodic_set (roots (λx. a*cos (x/c) + b)) (2*c*pi)"
proof -
  define B where "B = { c*arccos (- b / a), - c*arccos (- b / a)}"
  have "bB. k::int. x = b + k * (2*c*pi)"
    when "xroots (λx. a * cos (x/c) + b)" for x
  proof -
    define C1 where "C1 = (k::int. x = c*arccos (- b / a) + k * (2*c*pi))"
    define C2 where "C2 = (k::int. x = - c*arccos (- b / a) + k * (2*c*pi))"
    have "cos (x/c) = - b/a" using that a0 unfolding roots_within_def
      by (auto simp add:field_simps)
    then have "C1  C2"
      unfolding cos_eq_arccos_Ex ex_disj_distrib C1_def C2_def using c0
      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 "p0" "c0"
  shows "periodic_set (roots (λ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 (λx. poly ([:- a, 1:] * p) (tan (x/c))) = roots (λx. tan (x/c) - a)
           roots (λx. poly p (tan (x/c)))"
    unfolding roots_within_def by auto
  moreover have "periodic_set (roots (λx. tan (x/c) - a)) (c*pi)"
    using periodic_set_tan_linear[OF _ c0 ,of 1 "-a",simplified] .
  moreover have "periodic_set (roots (λ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 "a0  b0  c0"
  shows "periodic_set (roots (λ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  {x. cos (x/2) = 0})  (roots f  {x. cos (x/2)  0})"
    by auto
  moreover have "periodic_set (roots f  {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  {x. cos (x/2)  0}) (4*pi)"
  proof -
    define p where "p=[:a+c,2*b,c-a:]"
    have "poly p (tan (x/2)) = 0  f x=0" when "cos (x/2) 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 "tt0" 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  {x. cos (x/2)  0} = roots (λx. poly p (tan (x/2)))  {x. cos (x/2)  0}"
      unfolding roots_within_def by auto
    moreover have "periodic_set (roots (λx. poly p (tan (x/2)))  {x. cos (x/2)  0}) (4*pi)"
    proof -
      have "p0" unfolding p_def using assms by auto
      then have "periodic_set (roots (λ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